#include <stdio.h>
  #include <ctype.h>
 #include <stdlib.h>


typedef struct lit  {
    char name;
    int negative;
}literal;


typedef struct cl {
     literal  first_literal;
      struct cl * sub_clause;
      struct cl * parent;
} clause;


#define MAX_LINE_LENGTH 1000



void make_clause( clause * base, char * line)
{
    clause* current_clause = base;
    char * pos = line;
    while(*pos != 0)
    {
	if (*pos == '|') 
	{
	    // this is not the last literal allocate a new literal
	    // and fill out the pointers
	    
	    current_clause->sub_clause = (clause *)calloc(1,sizeof(clause));
	    if (  current_clause->sub_clause == NULL)
	    {
		fprintf(stderr, "Malloc Failure\n");
		exit(1);
	    }
	    current_clause->sub_clause->parent = current_clause;
	    
	    current_clause =  current_clause->sub_clause;
	    
	    
	    }

	if (*pos == '-') 
	{
	    current_clause->first_literal.negative = 1;
	}
	if (isalpha(*pos)) 
	{
	    current_clause->first_literal.name = *pos;
	}

	pos++;
	

    }


}


void print_clause(clause * cl)
{

    while(1)
    {
	if ( cl->first_literal.negative == 1)
	    fprintf(stdout, "-");
	
	fprintf(stdout, "%c ",cl->first_literal.name);


	if (cl->sub_clause != NULL)
	{
	    fprintf(stdout," | ");
	    cl = cl->sub_clause;
	}
	else
	    break;
	

	


    }
    fprintf(stdout, "\n");
}


int resolve( clause * one, clause * two, clause * out)
{
    return(1);
}

 int main(int argc, char **argv)
{

    char * read_val;
    char  line_one[MAX_LINE_LENGTH];
    char  line_two[MAX_LINE_LENGTH];
    

// read in from stdin

    if (NULL == fgets(line_one,MAX_LINE_LENGTH,stdin))
    {
	fprintf(stderr, "No input line\n"); 
	exit(1);
    }
    if (NULL == fgets(line_two,MAX_LINE_LENGTH,stdin))
    {
	fprintf(stderr, "No 2nd input line\n"); 
	exit(1);
    }
    

    // work out the lenght of the two clauses

    int length_one =1;
    int length_two = 1;
    char * pos;
    clause * clause_one;
    clause_one = calloc(1,sizeof(clause));
    clause * clause_two;
    clause_two = calloc(1,sizeof(clause));
    
    if (   clause_two == NULL ||  clause_one == NULL)
    {
	fprintf(stderr, "Malloc Failure\n");
	exit(1);
    }
    pos = line_one;
    int negative = 0;
   
    make_clause(clause_one,line_one);
    make_clause(clause_two,line_two);
    
    clause * clause_three;
    clause_three = calloc(1,sizeof(clause));
    int  ret;
    if (   clause_three == NULL)
    {
	fprintf(stderr, "Malloc Failure\n");
	exit(1);
    }
    ret = resolve(clause_one, clause_two,clause_three);

    
    print_clause(clause_one);
    print_clause(clause_two);
    if (ret == 0)
    {
     print_clause(clause_three);
    }
    else
    {
	fprintf(stdout, "Resolution Failed\n");
    }




//

}