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))]).