set(anl_eq). % We'll keep only clauses that subsume hints. assign(bsub_hint_add_wt, -1000). set(keep_hint_subsumers). assign(max_weight, 0). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(sigint_interact). clear(detailed_history). list(usable). x = x. end_of_list. list(sos). f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x. % OML_Sh end_of_list. assign(max_proofs, 3). list(passive). f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))) | $Ans(A_SS). f(f(A,A),f(A,B)) != A | $Ans(B_SS). f(A,f(A,f(A,B))) != f(A,B) | $Ans(OM_SS). end_of_list. list(hints2). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. f(x,f(f(x,y),f(f(z,f(f(f(x,y),f(x,y)),z)),z)))=f(x,y). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(v,f(f(y,y),v)),v)))=y. f(f(x,y),f(x,f(f(z,f(f(x,x),z)),z)))=x. f(f(x,y),f(x,f(f(z,f(f(x,x),z)),z)))=x. f(f(x,y),f(y,f(f(z,f(f(y,y),z)),z)))=y. f(f(x,y),f(y,y))=y. f(f(x,y),f(y,y))=y. f(f(x,y),f(y,f(f(y,y),z)))=y. f(f(x,y),f(x,x))=x. f(f(f(f(x,y),f(y,z)),u),f(y,y))=y. f(x,f(f(x,y),f(x,y)))=f(x,y). f(x,f(f(y,x),f(f(z,f(f(f(y,x),f(y,x)),z)),z)))=f(y,x). f(x,f(f(y,f(f(x,x),y)),y))=f(x,x). f(x,f(f(y,x),f(y,x)))=f(y,x). f(f(f(x,x),y),x)=f(x,x). f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y)))=x. f(x,f(f(x,x),y))=f(x,x). f(f(x,x),f(x,y))=x. f(f(f(x,y),f(x,y)),x)=f(x,y). f(f(x,x),f(y,x))=x. f(f(f(x,f(f(y,x),z)),u),f(f(y,x),f(y,x)))=f(y,x). f(f(f(f(x,y),f(x,z)),u),f(x,x))=x. f(f(f(x,f(f(x,y),z)),u),f(f(x,y),f(x,y)))=f(x,y). f(f(f(f(x,y),f(z,y)),u),f(y,y))=y. f(f(x,f(f(y,z),f(z,u))),f(z,z))=z. f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))). f(x,f(f(f(y,x),x),f(y,x)))=f(x,x). f(f(x,f(f(y,z),f(y,u))),f(y,y))=y. f(f(x,f(f(y,z),f(u,z))),f(z,z))=z. f(f(x,f(y,f(f(z,y),u))),f(f(z,y),f(z,y)))=f(z,y). f(f(f(x,y),y),f(x,y))=y. f(f(f(x,y),x),f(x,y))=x. f(f(x,f(x,y)),x)=f(x,y). f(f(x,y),f(x,f(x,y)))=x. f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x). f(f(x,y),f(y,x))=f(f(y,x),f(y,x)). f(x,f(f(y,x),f(x,y)))=f(y,x). f(x,y)=f(y,x). f(f(f(f(x,y),f(y,x)),z),f(x,y))=f(f(y,x),f(x,y)). f(x,f(x,f(x,y)))=f(x,y). f(f(x,f(y,x)),f(y,x))=x. f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(y,x). f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(y,x). f(f(x,f(x,y)),f(y,x))=x. f(f(f(x,y),f(y,x)),f(f(y,x),z))=f(y,x). f(f(f(x,y),z),f(f(x,f(f(y,u),f(y,v))),f(x,f(f(y,u),f(y,v)))))=f(x,f(f(y,u),f(y,v))). f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,u),f(z,v)),y)))=f(f(f(z,u),f(z,v)),y). f(f(x,y),f(y,f(f(x,y),f(y,z))))=f(f(x,y),f(y,z)). f(f(x,y),f(y,f(f(x,y),f(z,y))))=f(f(x,y),f(y,z)). f(f(x,y),f(y,z))=f(f(x,y),f(z,y)). f(x,f(f(y,x),z))=f(x,f(z,f(y,x))). f(x,f(y,z))=f(x,f(z,y)). f(f(x,y),z)=f(z,f(y,x)). f(x,f(y,z))=f(f(z,y),x). f(x,f(f(y,z),u))=f(f(f(z,y),u),x). f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). f(f(f(f(x,y),z),u),f(f(f(y,x),z),f(f(x,y),z)))=f(z,f(x,y)). f(f(f(f(x,y),f(z,u)),v),f(f(f(y,x),f(u,z)),f(f(z,u),f(x,y))))=f(f(z,u),f(x,y)). f(f(f(f(x,f(y,f(f(z,y),u))),z),v),f(f(z,y),f(z,y)))=f(z,y). f(f(x,f(f(f(y,f(f(z,y),u)),v),z)),f(f(z,y),f(z,y)))=f(z,y). f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,v),f(z,u)),y)))=f(f(f(z,v),f(z,u)),y). f(f(f(f(f(x,y),f(x,z)),u),f(f(f(x,z),f(x,y)),u)),f(f(u,x),v))=f(f(f(x,z),f(x,y)),u). f(f(f(x,f(f(y,x),z)),f(x,u)),y)=f(y,x). f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(f(f(u,y),f(v,y)),x). f(f(f(x,y),f(z,y)),f(f(u,v),f(u,y)))=f(f(f(x,y),f(z,y)),u). f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(f(f(x,y),f(z,y)),u). f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(x,f(f(u,y),f(v,y))). f(f(f(x,y),f(x,y)),z)=f(x,f(f(z,y),f(z,y))). f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). end_of_list.