input_clause(o_even, axiom,
	     [++even(o)]).

input_clause(suc_even_odd, axiom,
	     [--even(X), ++odd(s(X))]).

input_clause(suc_odd_even, axiom,
	     [--odd(X), ++even(s(X))]).

input_clause(nil_even_list, axiom,
	     [++list_even(nil)]).

input_clause(cons_even_list, axiom,
	     [--even(X), --list_even(Y),
	      ++list_even(cons(X,Y))]).
   

input_clause(o_zero_mod_3, axiom,
	     [++zero_mod_3(o)]).

input_clause(suc_zero_one_mod_3, axiom,
	     [--zero_mod_3(X), ++one_mod_3(s(X))]).

input_clause(suc_one_two_mod_3, axiom,
	     [--one_mod_3(X), ++two_mod_3(s(X))]).

input_clause(suc_two_zero_mod_3, axiom,
	     [--two_mod_3(X), ++zero_mod_3(s(X))]).

input_clause(nil_3n_plus_2_tree, axiom,
	     [++tree_3n_plus_2(nil)]).

input_clause(two_mod_3_3n_plus_2_tree, axiom,
	     [--two_mod_3(X), ++tree_3n_plus_2(X)]).

input_clause(cons_3n_plus_2_tree, axiom,
	     [--tree_3n_plus_2(X), --tree_3n_plus_2(Y),
	      ++tree_3n_plus_2(cons(X,Y))]).

input_clause (list_even_inter_tree3plus2, axiom, 	[++q(X), --list_even(X),	--tree_3n_plus_2(X)])