set(para_into). set(para_from). set(order_eq). set(ancestor_subsume). assign(max_weight,45). %assign(change_limit_after,50). %assign(new_max_weight,25). set(keep_hint_subsumers). set(input_sos_first). assign(bsub_hint_add_wt,-1024). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). assign(max_proofs,-1). assign(max_mem,440000). assign(report,3600). assign(max_seconds,180). assign(pick_given_ratio,2). weight_list(pick_and_purge). weight(junk,1000). end_of_list. list(usable). x=x. end_of_list. list(sos). % f(f(f(x,y),z),f(f(x,f(x,z)),x))=z # label("SING_1"). % f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. f(f(f(x,y),z),f(x,f(f(x,z),x)))=z. end_of_list. list(passive). % f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2"). % f(f(f(a,b),c),f(a,f(f(a,c),a)))!=c | $ANS(SING_3). f(f(f(a,f(b,a)),a),f(b,f(c,a)))!=b | $ANS(SING_4). end_of_list. list(demodulators). EQ(f(f(f(x,f(x,f(f(x,x),x))),x),f(f(x,f(f(x,x),x)),x))=x,junk). % EQ(f(f(f(f(x,f(f(x,y),x)),y),z),f(y,f(f(y,z),y)))=z,junk). % EQ(f(x,f(x,f(f(x,f(y,f(f(y,x),y))),x)))=f(y,f(f(y,x),y)),junk). % Following are to block various single axioms, in search of a circle of pure proofs. % EQ(f(f(f(x,y),z),f(f(x,f(x,z)),x))=z,junk). % EQ(f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y,junk). % % EQ(f(f(f(x,y),z),f(x,f(f(x,z),x)))=z,junk). % % EQ(f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y,junk). % Following to shoorten the proof of the second single axiom from the first, within a pure proof. % EQ(f(x,f(x,f(y,x)))=f(y,x),junk). % Following are to shorten the proof that deduces the three Sheffer. % EQ(f(f(x,y),f(y,f(x,z)))=y,junk). % EQ(f(f(x,f(y,f(z,x))),y)=f(y,f(z,x)),junk). % EQ(f(f(x,f(x,x)),x)=f(x,x),junk). % EQ(f(f(f(x,y),y),f(x,y))=y,junk). % EQ(f(f(x,f(y,y)),y)=f(y,y),junk). % EQ(f(f(x,f(y,f(z,y))),f(x,f(y,f(z,u))))=f(f(x,f(y,f(z,y))),f(x,z)),junk). % EQ(f(f(f(x,y),x),f(x,f(z,y)))=f(f(x,f(z,y)),f(x,f(z,y))),junk). % EQ(f(f(f(x,y),z),f(z,y))=z,junk). % EQ(f(x,f(f(f(y,z),f(f(y,z),f(f(z,f(z,x)),z))),f(y,z)))=f(f(z,f(z,x)),z),junk). % EQ(f(x,f(y,f(x,f(z,y))))=f(x,f(z,y)),junk). % EQ(f(f(f(x,f(x,x)),x),f(f(y,f(y,x)),y))=x,junk). % EQ(f(f(x,y),f(f(f(f(z,f(z,x)),z),f(f(f(z,f(z,x)),z),y)),f(f(z,f(z,x)),z)))=y,junk). % EQ(f(x,f(f(x,y),f(z,f(x,f(u,y)))))=f(x,y),junk). (f(x,junk) = junk). (f(junk,x) = junk). end_of_list. list(hints). % Following 66-step from wos f(f(x,y),f(f(f(z,u),x),f(f(f(f(z,u),x),y),f(f(z,u),x))))=y. f(x,f(f(y,z),f(f(f(y,z),f(y,f(f(y,x),y))),f(y,z))))=f(y,f(f(y,x),y)). f(f(f(f(x,f(f(x,y),x)),z),y),f(f(x,f(f(x,y),x)),y))=y. f(f(x,f(y,f(f(y,x),y))),f(f(f(y,z),x),f(x,f(f(y,z),x))))=f(y,f(f(y,x),y)). f(f(x,y),f(f(z,x),f(f(f(z,x),y),f(z,x))))=y. f(f(f(x,f(f(x,y),x)),z),f(y,f(f(y,z),y)))=z. f(f(x,f(f(y,z),f(f(f(y,z),x),f(y,z)))),f(f(z,x),f(x,f(z,x))))=f(f(y,z),f(f(f(y,z),x),f(y,z))). f(f(f(f(x,y),z),f(f(u,x),f(f(f(u,x),y),f(u,x)))),f(f(x,y),f(y,f(x,y))))=f(f(u,x),f(f(f(u,x),y),f(u,x))). f(x,f(f(y,f(f(y,z),y)),f(f(f(y,f(f(y,z),y)),f(z,f(f(z,x),z))),f(y,f(f(y,z),y)))))=f(z,f(f(z,x),z)). f(f(x,f(x,f(f(x,x),x))),x)=f(x,f(f(x,x),x)). f(f(f(x,y),f(x,f(f(x,x),x))),f(x,f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))=x. f(x,f(f(x,y),f(f(f(x,y),f(f(x,f(x,f(f(x,x),x))),x)),f(x,y))))=f(x,f(f(x,x),x)). f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(x,f(x,f(f(x,x),x)))),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). f(f(f(x,y),f(f(f(x,y),z),f(x,y))),f(z,f(f(z,f(f(y,z),f(z,f(y,z)))),z)))=f(f(y,z),f(z,f(y,z))). f(x,f(x,f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). f(f(x,y),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),y),f(x,f(f(x,x),x)))))=y. f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(f(x,x),x)),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). f(f(f(x,f(x,f(f(x,x),x))),x),f(f(x,f(f(x,f(x,f(f(x,x),x))),x)),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(x,f(f(x,x),x))),x)),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x))))=f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))). f(x,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). f(x,f(f(x,x),x))=f(x,x). f(f(x,x),f(f(x,f(f(x,f(f(x,x),x)),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). f(f(x,f(f(x,x),x)),f(x,x))=x. f(f(x,f(y,x)),f(f(y,x),f(y,x)))=f(y,x). f(f(f(x,y),x),f(x,x))=x. f(x,f(f(x,x),f(x,x)))=f(x,x). f(f(x,x),f(x,x))=x. f(f(x,x),f(x,f(x,x)))=f(f(x,x),f(x,x)). f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x))))=f(x,x). f(f(x,x),f(x,f(x,x)))=x. f(x,f(f(x,x),f(x,f(x,x))))=f(x,x). f(f(x,x),f(x,f(x,f(f(x,x),x))))=x. f(x,f(f(x,f(f(x,x),f(x,f(x,x)))),x))=f(x,x). f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))=x. f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(y,y))=f(f(y,y),f(y,f(y,y))). f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(y,y))=y. f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))))=f(x,x). f(f(x,x),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). f(x,f(x,f(f(x,x),x)))=f(f(x,x),x). f(f(x,x),x)=f(x,f(x,x)). f(f(x,f(x,x)),f(x,x))=x. f(f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))),f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))))=f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))). f(f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))),f(x,x))=f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))). f(f(x,y),f(f(f(x,y),f(y,y)),f(x,y)))=f(f(y,y),f(y,y)). f(f(x,y),f(f(f(x,y),f(y,y)),f(x,y)))=y. f(f(x,f(y,x)),f(f(y,x),f(x,f(y,x))))=f(y,x). f(f(f(x,y),x),f(x,f(f(x,y),x)))=x. f(x,f(f(f(f(y,x),f(x,x)),f(y,x)),f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))))=f(f(f(y,x),f(x,x)),f(y,x)). f(f(f(x,y),f(y,y)),f(x,y))=f(y,f(x,y)). f(f(x,y),f(y,f(x,y)))=y. f(f(x,f(y,x)),x)=f(y,x). f(x,f(f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). f(x,f(f(f(y,f(f(y,x),y)),f(f(f(y,x),y),f(y,f(f(y,x),y)))),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). f(x,f(f(f(y,x),y),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). f(x,f(f(f(y,x),y),f(y,f(f(y,x),y))))=f(y,f(f(y,x),y)). f(x,f(f(x,y),x))=f(y,x). f(f(x,y),f(y,f(z,x)))=y. f(f(f(x,y),z),f(z,x))=z. f(f(f(x,y),z),f(z,y))=z. f(x,f(f(x,y),x))=f(x,y). f(x,y)=f(y,x). f(f(x,f(y,x)),x)=f(x,y). f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y. end_of_list.