begin_problem(example). list_of_descriptions. name({**}). author({**}). status(unknown). description({**}). end_of_list. list_of_symbols. functions [(zero, 0), (s, 1), (nil, 1+0), (cons, 1+2), (list_length, 1+1), (x, 1), (y, 1), (plus, 2), (frac, 2)]. predicates [(even, 1),(greater, 2)]. types [nat, (list, 1)]. classes [ordered,superordered]. end_of_list. list_of_declarations. function(zero, nat). function(x, nat). function(nil, [A], list(A)). function(cons,[A], (A, list(A)) list(A)). function(list_length, [A], (list(A)) nat). function(y, nat). function(s, (nat) nat). function(plus, (nat,nat) nat). predicate(greater, nat,nat). predicate(even, nat). type(nat, ordered). type([A:superordered], list(A), superordered). subclass(ordered, superordered). end_of_list. list_of_formulae(axioms). formula(forall_types([A],equal(list_length(nil),zero)), length_nil_zero). formula(forall_types([A],forall([X:A,XS:list(A)],equal(list_length(cons(X,XS)),s(list_length(XS))))), length_cons). formula(not(even(s(zero))),even_not_one). formula(even(zero),even_zero). formula(forall([X:nat],implies(even(X),even(s(s(X))))), even_ss). formula(forall([X:nat],implies(not(even(X)),not(even(s(s(X)))))), even_not_ss). formula(forall([X:nat],equal(plus(zero,X),X)), plus_zero). formula(forall([X:nat,Y:nat],equal:lr(plus(s(X),Y),s(plus(X,Y)))), plus_s). end_of_list. list_of_formulae(conjectures). formula(forall([X:nat],equal(plus(zero,X),X)), conjecture). end_of_list. end_problem.