set(para_into). set(para_from). set(order_eq). set(ancestor_subsume). assign(max_weight,20). %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,300000). % assign(max_seconds,30). 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"). end_of_list. list(passive). f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2"). end_of_list. list(demodulators). % 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(f(x,x),f(x,x))=x,junk). 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 hints from temp.ba.mirror.wos.out4ab 23-step proof. f(x,f(f(f(y,z),f(f(y,z),f(f(y,f(y,x)),y))),f(y,z)))=f(f(y,f(y,x)),y). f(f(f(f(x,f(x,y)),x),z),f(f(y,f(y,z)),y))=z. f(x,f(f(y,f(y,f(f(x,f(x,x)),x))),y))=f(f(x,f(x,x)),x). f(x,f(f(f(f(x,y),x),x),f(f(x,y),x)))=f(f(x,f(x,x)),x). f(f(x,f(x,x)),x)=f(x,x). f(f(f(x,y),x),f(x,x))=x. f(f(x,x),f(f(x,f(x,x)),x))=x. f(x,f(f(y,f(y,f(x,x))),y))=f(x,x). f(f(x,x),f(f(x,f(x,f(f(y,f(y,f(x,x))),y))),x))=x. f(f(x,f(x,f(f(x,y),f(x,y)))),x)=f(x,y). f(f(x,y),f(x,x))=x. f(x,f(f(x,y),f(x,y)))=f(x,y). f(f(x,f(x,y)),x)=f(x,y). f(f(f(x,y),z),f(x,z))=z. f(f(x,y),f(f(x,z),y))=y. f(f(x,x),f(x,y))=x. f(f(f(f(x,x),y),f(x,z)),x)=f(x,z). f(x,y)=f(y,x). f(f(f(x,y),z),f(z,x))=z. f(f(x,y),f(y,f(z,x)))=y. f(x,f(f(x,y),x))=f(x,y). f(x,f(f(y,x),x))=f(x,y). f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. % f(f(f(x,y),z),f(f(x,f(x,z)),x))=z # label("SING_1"). % f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2"). % f(f(x,y),f(f(f(f(z,u),x),f(f(f(z,u),x),y)),f(f(z,u),x)))=y # label("SING_1 => SING_2 3(91)"). % f(x,f(f(f(y,z),f(f(y,z),f(f(y,f(y,x)),y))),f(y,z)))=f(f(y,f(y,x)),y) # label("SING_1 => SING_2 4(92)"). % f(f(x,y),f(f(f(z,x),f(f(z,x),y)),f(z,x)))=y # label("SING_1 => SING_2 3(91)"). % f(f(f(f(x,f(x,y)),x),z),f(f(y,f(y,z)),y))=z # label("SING_1 => SING_2 6(96)"). % f(x,f(f(y,f(y,f(f(x,f(x,x)),x))),y))=f(f(x,f(x,x)),x) # label("SING_1 => SING_2 7(99)"). % f(x,f(f(f(f(x,y),x),x),f(f(x,y),x)))=f(f(x,f(x,x)),x) # label("SING_1 => SING_2 9(104)"). % f(f(x,f(x,x)),x)=f(x,x) # label("SING_1 => SING_2 10(113)"). % f(f(f(x,y),x),f(x,x))=x # label("SING_1 => SING_2 11(134)"). % f(f(x,x),f(x,x))=x # label("SING_1 => SING_2 12(152)"). % f(x,f(f(y,f(y,f(x,x))),y))=f(x,x) # label("SING_1 => SING_2 13(159)"). % f(f(f(f(x,x),y),f(x,x)),x)=f(x,x) # label("SING_1 => SING_2 14(166)"). % f(f(x,x),f(f(y,f(y,x)),y))=x # label("SING_1 => SING_2 16(220)"). % f(f(x,x),f(f(x,f(x,f(f(y,f(y,f(x,x))),y))),x))=x. % f(f(x,f(x,f(f(x,y),f(x,y)))),x)=f(x,y) # label("SING_1 => SING_2 17(286)"). % f(f(x,y),f(x,x))=x # label("SING_1 => SING_2 12(152)"). % f(x,f(f(x,y),f(x,y)))=f(x,y) # label("SING_1 => SING_2 19(379)"). % f(f(x,f(x,y)),x)=f(x,y) # label("SING_1 => SING_2 10(113)"). % f(f(x,x),f(y,x))=x # label("SING_1 => SING_2 12(152)"). % f(f(x,y),f(f(z,x),y))=y # label("SING_1 => SING_2 35(1742)"). % f(f(f(x,y),z),f(x,z))=z # label("SING_1 => SING_2 11(134)"). % f(f(x,x),f(x,y))=x # label("SING_1 => SING_2 12(152)"). % f(x,f(f(y,z),f(y,x)))=f(y,x) # label("SING_1 => SING_2 20(380)"). % f(x,f(x,f(y,x)))=f(y,x) # label("SING_1 => SING_2 36(1753)"). % f(f(x,y),y)=f(y,f(x,y)) # label("SING_1 => SING_2 28(1131)"). % f(x,f(f(y,x),x))=f(y,x) # label("SING_1 => SING_2 39(2197)"). % f(x,y)=f(y,x) # label("SING_1 => SING_2 28(1131)"). % f(f(x,y),f(y,f(z,x)))=y # label("SING_1 => SING_2 46(4961)"). % f(f(x,y),f(x,f(z,y)))=x # label("SING_1 => SING_2 44(4634)"). % f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y # label("SING_1 => SING_2 48(5227)"). end_of_list.