input_clause (clause1, conjecture,
	      [++p(a)]).
input_clause (clause2, conjecture,
	      [--p(X), ++p(f(X))]).
input_clause (clause3, conjecture,
	      [--p(f(f(X)))]).