begin_problem(benchmark). list_of_descriptions. name({**}). author({**}). status(unknown). description({**}). end_of_list. list_of_symbols. functions [(z,0), (s,1), (p, 2+2), (cons, 1+2), (nil, 1+0), (append, 1+2), (rev, 1+1), (zip, 1+2), (len,1+1)]. predicates [(p,0)]. sorts [(pair,2),(list,1),(nat,0)]. end_of_list. list_of_declarations. function(z, nat). function(s, (nat) nat). function(p, [A,B], (A,B) pair(A,B)). function(cons, [A], (A,list(A)) list(A)). function(nil, [A], list(A)). function(append, [A], (list(A),list(A)) list(A)). function(rev, [A], (list(A)) list(A)). function(zip, [A,B], (list(A),list(B)) list(pair(A,B))). function(len, [A], (list(A)) nat). datatype(pair, p). datatype(nat, z, s). datatype(list, nil, cons). end_of_list. list_of_formulae(axioms). formula(forall_sorts([A],forall([LS:list(A)],equal:lr(append(nil,LS),LS))),append_nil). formula(forall_sorts([A],forall([LS:list(A),Y:A,YS:list(A)],equal:lr(append(cons(Y,YS),LS),cons(Y,append(YS,LS))))),append_cons). formula(forall_sorts([A],equal:lr(rev(nil),nil)),rev_nil). formula(forall_sorts([A],forall([Y:A,YS:list(A)],equal:lr(rev(cons(Y,YS)),append(rev(YS),cons(Y,nil))))),rev_cons). formula(forall_sorts([A],equal:lr(len(nil),z)),len_nil). formula(forall_sorts([A],forall([L:A,LS:list(A)],equal:lr(len(cons(L,LS)),s(len(LS))))),len_cons). formula(forall_sorts([A],forall([XS:list(A)],equal:lr(zip(XS,nil),nil))), zip_nil_right). formula(forall_sorts([A],forall([YS:list(A)],equal:lr(zip(nil,YS),nil))), zip_nil_left). formula(forall_sorts([A],forall([X:A,XS:list(A),Y:A,YS:list(A)], equal:lr(zip(cons(X,XS),cons(Y,YS)),cons(p(X,Y),zip(XS,YS))))), zip_cons). end_of_list. list_of_formulae(conjectures). formula(forall_sorts([A],forall([X:A,XS:list(A),Y:A,YS:list(A)], implies(equal(len(XS),len(YS)), equal(zip(rev(XS),rev(YS)),rev(zip(XS,YS)))))), conj_prob85). end_of_list. end_problem.