============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11621 was started by mccune on cleo.thornwood, Sat Aug 12 21:14:54 2006 The command was "/home/mccune/bin/prover9 -f sh1-def.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file sh1-def.in assign(new_constants,1). assign(eq_defs,fold). formulas(sos). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). x' = f(x,x). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). [assumption]. x' = f(x,x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ a, b, c, f, ' ]). After inverse_order: (no changes). Folding symbols: '/1. After fold_eq: Function symbol precedence: lex([ a, b, c, ', f ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. 4 f(x,x) = x'. [copy(3),flip(a)]. 5 a'' != a | f(a,f(b,b')) != a' | f(f(b',a),f(c',a)) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(2),rewrite(4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34))]. end_of_list. formulas(demodulators). 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. 4 f(x,x) = x'. [copy(3),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=15): 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. given #2 (I,wt=6): 4 f(x,x) = x'. [copy(3),flip(a)]. given #3 (I,wt=30): 5 a'' != a | f(a,f(b,b')) != a' | f(f(b',a),f(c',a)) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(2),rewrite(4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34))]. given #4 (T,wt=9): 12 f(x,f(x',x))' = x. [para(4(a,1),1(a,1)),rewrite(4(1))]. given #5 (T,wt=14): 9 f(f(x,f(x',x)),f(x,f(y,x))) = x. [para(4(a,1),1(a,1,1,2,1))]. given #6 (A,wt=37): 6 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(1(a,1),1(a,1,1,2,1))]. given #7 (F,wt=13): 17 f(f(x,f(x',x)),f(x,x')) = x. [para(4(a,1),9(a,1,2,2))]. given #8 (F,wt=14): 10 f(f(x,f(f(y,x),x)),f(y,x')) = y. [para(4(a,1),1(a,1,2,2))]. given #9 (T,wt=15): 39 f(f(x,f(f(x',x),x)),x'') = x'. [para(4(a,1),10(a,1,2))]. given #10 (T,wt=18): 11 f(f(x,f(f(f(y,x),x),x)),f(y,x)') = f(y,x). [para(4(a,1),1(a,1,2))]. given #11 (A,wt=25): 7 f(f(f(x,f(y,z)),f(f(u,f(x,f(y,z))),f(x,f(y,z)))),f(u,x)) = u. [para(1(a,1),1(a,1,2,2))]. given #12 (F,wt=18): 70 f(f(x,f(f(y,x),x)),f(y,f(x,f(x',x)))) = y. [para(9(a,1),7(a,1,1,1)),rewrite(9(6),9(7))]. given #13 (F,wt=25): 122 f(a,f(b,b')) != a' | f(f(b',a),f(c',a)) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(5),rewrite(112(3)),xx(a)]. given #14 (T,wt=5): 112 x'' = x. [back_rewrite(12),rewrite(91(3))]. given #15 (T,wt=9): 91 f(x,f(x',x)) = x'. [para(70(a,1),6(a,1,2)),rewrite(88(8),4(1),4(2)),flip(a)]. given #16 (A,wt=29): 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(1(a,1),1(a,1,2))]. given #17 (F,wt=9): 96 f(x',f(x,x')) = x. [back_rewrite(88),rewrite(91(3),91(4))]. given #18 (F,wt=10): 113 f(x',f(x,f(y,x))) = x. [back_rewrite(9),rewrite(91(3))]. given #19 (T,wt=12): 125 f(x,f(x',f(y,x'))) = x'. [para(91(a,1),6(a,1,1,1)),rewrite(91(4),96(4),4(1),91(3),91(4),4(6),91(8))]. given #20 (T,wt=13): 97 f(f(x,f(f(x',x),x)),x) = x'. [back_rewrite(87),rewrite(91(3),91(8))]. given #21 (A,wt=85): 18 f(f(f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x)))),f(f(x,f(f(y,x),x)),f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x)))))),f(f(f(y,f(u,x)),f(y,f(y,f(u,x)))),f(v,f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x))))))) = f(f(y,f(u,x)),f(y,f(y,f(u,x)))). [para(6(a,1),1(a,1,1,2,1))]. given #22 (F,wt=14): 100 f(f(x,y)',f(f(x,y),x)) = f(x,y). [back_rewrite(69),rewrite(91(6))]. given #23 (F,wt=14): 145 f(x',f(x,f(y,f(f(x,y),y)))) = x. [para(8(a,1),113(a,1,2,2))]. given #24 (T,wt=15): 114 f(f(x',f(f(x,x'),x')),x') = x. [back_rewrite(92),rewrite(96(5),96(12))]. given #25 (T,wt=16): 123 f(f(x',f(f(y,x'),x')),f(y,x)) = y. [para(112(a,1),10(a,1,2,2))]. given #26 (A,wt=59): 19 f(f(f(x,f(y,f(z,u))),f(f(f(f(y,f(z,u)),f(y,f(y,f(z,u)))),f(x,f(y,f(z,u)))),f(x,f(y,f(z,u))))),f(u,f(f(y,u),u))) = f(f(y,f(z,u)),f(y,f(y,f(z,u)))). [para(6(a,1),1(a,1,2))]. given #27 (F,wt=16): 154 f(x,f(x',f(y,f(f(x',y),y)))) = x'. [para(8(a,1),125(a,1,2,2))]. given #28 (F,wt=18): 80 f(f(f(x,y),f(f(x,f(x,y)),f(x,y))),x') = x. [para(7(a,1),11(a,1,1,2,1,1)),rewrite(65(17),65(19))]. given #29 (T,wt=19): 65 f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. [para(7(a,1),1(a,1,2,2))]. given #30 (T,wt=19): 67 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(1(a,1),7(a,1,1,1)),rewrite(1(6),1(7))]. given #31 (A,wt=55): 21 f(f(x,f(f(y,f(f(x,y),y)),x)),f(f(f(z,y),f(f(f(y,f(f(x,y),y)),f(z,y)),f(z,y))),f(u,x))) = f(f(z,y),f(f(f(y,f(f(x,y),y)),f(z,y)),f(z,y))). [para(1(a,1),6(a,1,1,1)),rewrite(1(9),1(20))]. given #32 (F,wt=12): 298 f(f(x,f(f(y,x),x)),y') = y. [para(6(a,1),67(a,1,2)),rewrite(4(1),91(3),4(2),91(4),96(4),4(4),91(6),4(6),91(8),4(7),91(9),96(9))]. given #33 (F,wt=13): 296 f(f(x,f(f(y',x),x)),y) = y'. [para(1(a,1),67(a,1,2)),rewrite(4(1),91(3),4(6),91(8))]. given #34 (T,wt=14): 405 f(x,f(x',f(x,f(y,x))')) = x'. [back_rewrite(95),rewrite(394(6))]. given #35 (T,wt=12): 435 f(x',f(x,f(x',x)')) = x. [para(298(a,1),405(a,1,2,2,1,2)),rewrite(112(3),112(8))]. given #36 (A,wt=31): 22 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). [para(1(a,1),6(a,1,2,2))]. given #37 (F,wt=13): 419 f(x,f(x',f(x,x')')) = x'. [para(4(a,1),405(a,1,2,2,1,2))]. given #38 (F,wt=14): 411 f(x,f(f(f(y,x)',x),x)) = f(y,x). [para(296(a,1),8(a,1,1,2,1)),rewrite(91(6),4(5),112(3)),flip(a)]. given #39 (T,wt=8): 485 f(x',f(y,x)) = x. [para(411(a,1),1(a,1,2)),rewrite(4(1),91(3))]. % Operation f is commutative; C redundancy checks enabled. given #40 (T,wt=7): 776 f(x,y) = f(y,x). [back_rewrite(38),rewrite(654(4),759(4,R),485(4),671(4),654(4))]. given #41 (A,wt=9): 492 f(x,f(y,x')) = x'. [para(411(a,1),6(a,1,2)),rewrite(4(1),91(3),4(2),91(4),96(4),4(1),91(3),4(4),91(6))]. given #42 (F,wt=25): 806 f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(122),rewrite(776(13),776(17))]. given #43 (F,wt=8): 671 f(x',f(x,y)) = x. [back_rewrite(596),rewrite(654(4))]. given #44 (T,wt=9): 637 f(x,f(x',y)) = x'. [back_rewrite(608),rewrite(616(4))]. given #45 (T,wt=10): 714 f(x,f(x,y)') = f(x,y). [back_rewrite(375),rewrite(654(3),654(6))]. given #46 (A,wt=11): 616 f(f(x,y),f(y,f(x,y))) = y. [para(485(a,1),411(a,1,2,1,1,1)),rewrite(485(4),485(7))]. given #47 (F,wt=10): 805 f(x,f(y,x)') = f(y,x). [back_rewrite(618),rewrite(776(3))]. given #48 (F,wt=10): 807 f(f(x,y),f(x,y')) = x. [back_rewrite(771),rewrite(798(6),776(4))]. given #49 (T,wt=10): 835 f(f(x,y),f(y,x')) = y. [para(776(a,1),807(a,1,1))]. given #50 (T,wt=10): 836 f(f(x,y),f(y',x)) = x. [para(776(a,1),807(a,1,2))]. given #51 (A,wt=16): 693 f(x',f(f(x',y),f(x,z))) = f(x',y). [back_rewrite(415),rewrite(654(5),654(6),654(10))]. given #52 (F,wt=10): 837 f(f(x',y),f(y,x)) = y. [para(112(a,1),835(a,1,2,2))]. given #53 (F,wt=10): 838 f(f(x,y'),f(y,x)) = x. [para(835(a,1),776(a,1)),flip(a)]. given #54 (T,wt=10): 839 f(f(x,y),f(x',y)) = y. [para(776(a,1),835(a,1,2))]. given #55 (T,wt=11): 702 f(f(x,y),f(y,f(z,x))) = y. [back_rewrite(391),rewrite(654(3),654(5),646(5),671(5),654(8),646(8),671(8))]. given #56 (A,wt=21): 697 f(f(x',y),f(x',f(z,f(f(x',y),f(u,x))))) = x'. [back_rewrite(409),rewrite(654(4),654(8),654(10),688(12),654(7))]. given #57 (F,wt=11): 740 f(f(x,y),f(x,f(y,z))) = x. [back_rewrite(280),rewrite(688(6),688(6),688(7),654(3),654(4),654(9),654(10),688(14))]. given #58 (F,wt=11): 795 f(f(x,y),f(x,f(z,y))) = x. [back_rewrite(666),rewrite(688(6),776(4),688(10))]. given #59 (T,wt=11): 798 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(644),rewrite(776(2),776(6),688(10),776(2))]. given #60 (T,wt=11): 819 f(x,f(x,f(x,y))) = f(x,y). [back_rewrite(720),rewrite(776(2),776(3))]. given #61 (A,wt=16): 700 f(x',f(f(x',y),f(z,x))) = f(x',y). [back_rewrite(406),rewrite(654(5),654(10))]. given #62 (F,wt=11): 854 f(f(f(x,y),z),f(z,y)) = z. [para(485(a,1),702(a,1,2,2))]. given #63 (F,wt=11): 855 f(f(x,f(y,z)),f(z,x)) = x. [para(702(a,1),776(a,1)),flip(a)]. given #64 (T,wt=11): 856 f(f(x,y),f(y,f(x,z))) = y. [para(776(a,1),702(a,1,2,2))]. given #65 (T,wt=11): 857 f(f(x,y),f(f(z,x),y)) = y. [para(776(a,1),702(a,1,2))]. given #66 (A,wt=23): 701 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)). [back_rewrite(392),rewrite(654(3),654(5),654(8),654(11),654(14))]. given #67 (F,wt=11): 859 f(f(f(x,y),z),f(z,x)) = z. [para(671(a,1),702(a,1,2,2))]. given #68 (F,wt=11): 887 f(f(x,y),f(f(y,z),x)) = x. [para(776(a,1),740(a,1,2))]. given #69 (T,wt=11): 899 f(f(x,y),f(f(z,y),x)) = x. [para(776(a,1),795(a,1,2))]. given #70 (T,wt=11): 925 f(f(x,f(y,z)),f(y,x)) = x. [para(776(a,1),855(a,1,1,2))]. given #71 (A,wt=19): 704 f(f(f(x,y),f(z,x)),f(f(x,y),f(u,y))) = f(x,y). [back_rewrite(389),rewrite(654(4),654(7),654(7),654(10),654(10))]. given #72 (F,wt=11): 929 f(f(x,y),f(f(x,z),y)) = y. [para(776(a,1),856(a,1,2))]. given #73 (F,wt=13): 790 f(x,f(f(x,y),f(z,y))) = f(x,y). [back_rewrite(673),rewrite(688(6))]. given #74 (T,wt=13): 811 f(x,f(f(x,y),f(y,z))) = f(x,y). [back_rewrite(765),rewrite(776(4))]. given #75 (T,wt=13): 823 f(x,f(f(y,x),f(z,y))) = f(y,x). [back_rewrite(706),rewrite(776(4))]. given #76 (A,wt=23): 710 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)). [back_rewrite(382),rewrite(654(3),654(4),654(5),654(6),654(8),654(8),654(10),654(11),654(12),654(14),654(14))]. given #77 (F,wt=13): 871 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(702(a,1),702(a,1,2)),rewrite(776(4))]. given #78 (F,wt=13): 896 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(740(a,1),702(a,1,2)),rewrite(776(4))]. given #79 (T,wt=13): 904 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(795(a,1),702(a,1,2)),rewrite(776(4))]. given #80 (T,wt=13): 937 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(856(a,1),702(a,1,2)),rewrite(776(4))]. given #81 (A,wt=23): 711 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)). [back_rewrite(381),rewrite(654(3),654(5),654(8),654(7),654(11),654(14))]. given #82 (F,wt=13): 941 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(856(a,1),795(a,1,2)),rewrite(776(4))]. given #83 (F,wt=14): 718 f(x,f(f(x,y),f(x',z))) = f(x,y). [back_rewrite(368),rewrite(654(3),654(5),654(8))]. given #84 (T,wt=14): 723 f(x,f(f(x,y),f(z,x'))) = f(x,y). [back_rewrite(350),rewrite(654(3),654(8))]. given #85 (T,wt=14): 810 f(f(x,y),f(x,f(z,f(x,y')))) = x. [back_rewrite(766),rewrite(776(6))]. given #86 (A,wt=19): 712 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y). [back_rewrite(380),rewrite(654(4),654(7),654(6),654(7),654(8),654(10),654(10),654(10))]. given #87 (F,wt=12): 1533 f(f(x,y),f(y,x)) = f(x,y)'. [para(712(a,1),790(a,1,2)),rewrite(4(3)),flip(a)]. given #88 (F,wt=13): 1551 f(f(x,y)',f(y,x)') = f(x,y). [para(1533(a,1),485(a,1,2))]. given #89 (T,wt=14): 813 f(f(x,y'),f(x,f(z,f(x,y)))) = x. [back_rewrite(753),rewrite(776(6))]. given #90 (T,wt=14): 853 f(x,f(f(y,x),f(z,x'))) = f(y,x). [para(485(a,1),702(a,1,1))]. given #91 (A,wt=18): 722 f(f(x,y),f(x,f(z,f(f(x,y),f(u,x'))))) = x. [back_rewrite(352),rewrite(654(3),654(7),654(8),688(11),654(4))]. given #92 (F,wt=14): 888 f(f(x,y),f(x,f(f(x,y)',z))) = x. [para(714(a,1),740(a,1,1))]. given #93 (F,wt=14): 889 f(f(x,y),f(y,f(f(x,y)',z))) = y. [para(805(a,1),740(a,1,1))]. given #94 (T,wt=14): 900 f(f(x,y),f(x,f(z,f(x,y)'))) = x. [para(714(a,1),795(a,1,1))]. given #95 (T,wt=14): 901 f(f(x,y),f(y,f(z,f(x,y)'))) = y. [para(805(a,1),795(a,1,1))]. given #96 (A,wt=24): 724 f(x,f(f(x,f(y,f(x,z))),f(u,f(x,z')))) = f(x,f(y,f(x,z))). [back_rewrite(346),rewrite(654(6),688(6),654(8),688(6),688(6),654(9),654(9),688(14),654(17))]. given #97 (F,wt=14): 928 f(x,f(f(y,x),f(x',z))) = f(y,x). [para(485(a,1),856(a,1,1))]. given #98 (F,wt=14): 947 f(x,f(f(y,x'),f(z,x))) = f(z,x). [para(485(a,1),857(a,1,1))]. given #99 (T,wt=14): 949 f(x,f(f(y,x'),f(x,z))) = f(x,z). [para(671(a,1),857(a,1,1))]. given #100 (T,wt=12): 1923 f(x,f(f(x,x')',y)) = x'. [para(888(a,1),949(a,1,2)),rewrite(4(1)),flip(a)]. given #101 (A,wt=17): 725 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [back_rewrite(340),rewrite(654(3),654(5),688(6),654(3),654(4),654(6),654(9))]. given #102 (F,wt=12): 1924 f(x,f(y,f(x,x')')) = x'. [para(900(a,1),949(a,1,2)),rewrite(4(1)),flip(a)]. given #103 (F,wt=12): 1928 f(f(x,x')',y) = f(x,x'). [para(1923(a,1),835(a,1,1)),rewrite(776(7),1926(7),776(2)),flip(a)]. NOTE: New constant: f(x,x') = c_0. [new_symbol(2016)]. NOTE: New Function symbol precedence: lex([ a, b, c, c_0, ', f ]). given #104 (T,wt=6): 2028 f(x,x') = c_0. [new_symbol(2016)]. given #105 (T,wt=6): 2042 f(c_0,x) = x'. [back_rewrite(2024),rewrite(2028(2))]. given #106 (A,wt=19): 727 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [back_rewrite(337),rewrite(688(4),654(6),654(6),654(12))]. given #107 (F,wt=16): 2027 f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(806),rewrite(2013(6)),xx(a)]. given #108 (F,wt=6): 2043 f(x,c_0) = x'. [back_rewrite(2013),rewrite(2028(2))]. given #109 (T,wt=6): 2044 f(x,c_0') = c_0. [back_rewrite(2009),rewrite(2028(2),2028(5))]. given #110 (T,wt=6): 2045 f(c_0',x) = c_0. [back_rewrite(1928),rewrite(2028(2),2028(5))]. given #111 (A,wt=17): 731 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [back_rewrite(326),rewrite(688(4),654(6),654(6),654(12))]. given #112 (F,wt=9): 2040 f(x,f(y,x')') = c_0. [back_rewrite(2026),rewrite(2028(6))]. given #113 (F,wt=9): 2041 f(x,f(x',y)') = c_0. [back_rewrite(2025),rewrite(2028(6))]. given #114 (T,wt=9): 2048 f(x',f(x,y)') = c_0. [para(2028(a,1),693(a,1,2,1)),rewrite(2042(4),112(7),776(6),2028(6))]. given #115 (T,wt=9): 2049 f(x',f(y,x)') = c_0. [para(2028(a,1),700(a,1,2,1)),rewrite(2042(4),112(7),776(6),2028(6))]. given #116 (A,wt=16): 734 f(x,f(f(x,y),f(f(x,y'),z))) = f(x,y). [back_rewrite(300),rewrite(688(6),654(3),654(6),654(9))]. given #117 (F,wt=10): 2080 f(x,f(y,f(x,y))) = x'. [para(855(a,1),727(a,1,2)),rewrite(4(1)),flip(a)]. given #118 (F,wt=10): 2230 f(f(x,y),f(y,x)') = c_0. [para(1551(a,1),2040(a,1,2,1))]. given #119 (T,wt=10): 2278 f(f(x,y)',f(y,x)) = c_0. [para(1533(a,1),2049(a,1,2,1)),rewrite(112(5))]. given #120 (T,wt=10): 2360 f(x,f(y,f(y,x))) = x'. [para(776(a,1),2080(a,1,2,2))]. given #121 (A,wt=16): 735 f(x,f(f(x,y),f(x,f(y,z))')) = f(x,y). [back_rewrite(299),rewrite(654(3),654(5),688(6),654(3),654(4),654(9))]. given #122 (F,wt=10): 2440 f(x,f(y,f(x,y))') = c_0. [para(2080(a,1),2049(a,1,2,1)),rewrite(112(5),776(4))]. given #123 (F,wt=10): 2534 f(x,f(y,f(y,x))') = c_0. [para(2360(a,1),2049(a,1,2,1)),rewrite(112(5),776(4))]. given #124 (T,wt=11): 2046 f(x',f(y,f(z,x)')) = x. [back_rewrite(2039),rewrite(2042(4))]. given #125 (T,wt=10): 2789 f(x,f(x,y)) = f(x,y'). [para(2046(a,1),735(a,1,2,2,1,2)),rewrite(776(5),2753(5))]. given #126 (A,wt=15): 746 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [back_rewrite(245),rewrite(688(6),654(9),654(9),688(10))]. given #127 (F,wt=10): 2792 f(x,f(y,x)) = f(x,y'). [back_rewrite(850),rewrite(2757(5))]. given #128 (F,wt=11): 2754 f(x',f(y,f(x,z)')) = x. [para(776(a,1),2046(a,1,2,2,1))]. given #129 (T,wt=11): 2755 f(x',f(f(y,x)',z)) = x. [para(776(a,1),2046(a,1,2))]. given #130 (T,wt=11): 3223 f(x',f(f(x,y)',z)) = x. [para(776(a,1),2754(a,1,2))]. given #131 (A,wt=23): 751 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,y)))))) = x. [back_rewrite(217),rewrite(654(6),654(11),654(13),688(14),688(6),654(8),688(14))]. given #132 (F,wt=12): 2047 f(x,f(y,f(z,x')')) = x'. [back_rewrite(2038),rewrite(2042(4))]. given #133 (F,wt=12): 2051 f(f(x,y)',f(z,y')') = c_0. [para(2028(a,1),704(a,1,1,1)),rewrite(2042(3),2028(4),2042(6),2028(8))]. given #134 (T,wt=12): 2054 f(f(x,y)',f(y',z)') = c_0. [para(2028(a,1),712(a,1,1,1)),rewrite(2042(3),2028(4),2042(6),2028(8))]. given #135 (T,wt=12): 2223 f(x,f(y,f(z,x')')') = c_0. [para(2040(a,1),790(a,1,2,1)),rewrite(2042(6),2040(10))]. given #136 (A,wt=21): 758 f(f(x,y'),f(x,f(z,f(f(x,y'),f(u,f(x,y)))))) = x. [back_rewrite(201),rewrite(654(6),654(11),654(13),688(14),688(6),654(8),688(14))]. given #137 (F,wt=12): 2224 f(x,f(f(y,x')',z)') = c_0. [para(2040(a,1),811(a,1,2,1)),rewrite(2042(6),2040(10))]. given #138 (F,wt=12): 2225 f(f(x,y')',f(z,y)') = c_0. [para(2040(a,1),823(a,1,2,1)),rewrite(2042(6),2040(10))]. given #139 (T,wt=12): 2227 f(f(x,y')',f(y,z)') = c_0. [para(2040(a,1),937(a,1,2,2)),rewrite(776(6),2042(6),2040(10))]. given #140 (T,wt=12): 2242 f(x,f(y,f(x',z)')') = c_0. [para(2041(a,1),790(a,1,2,1)),rewrite(2042(6),2041(10))]. given #141 (A,wt=21): 762 f(f(x,y),f(x,f(f(f(x,y),f(z,f(x,f(u,y)))),v))) = x. [back_rewrite(162),rewrite(654(3),654(8),654(9),688(13),688(7),654(4),654(9),688(15))]. given #142 (F,wt=12): 2243 f(x,f(f(x',y)',z)') = c_0. [para(2041(a,1),811(a,1,2,1)),rewrite(2042(6),2041(10))]. given #143 (F,wt=12): 2244 f(f(x',y)',f(z,x)') = c_0. [para(2041(a,1),823(a,1,2,1)),rewrite(2042(6),2041(10))]. given #144 (T,wt=12): 2246 f(f(x',y)',f(x,z)') = c_0. [para(2041(a,1),937(a,1,2,2)),rewrite(776(6),2042(6),2041(10))]. given #145 (T,wt=12): 2257 f(x',f(y,f(x,z)')') = c_0. [para(2048(a,1),790(a,1,2,1)),rewrite(2042(6),2048(10))]. given #146 (A,wt=21): 763 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(u,y)),v))))) = x. [back_rewrite(161),rewrite(654(3),654(6),654(8),654(9),654(12),688(13),688(7),654(4),654(7),688(15))]. given #147 (F,wt=12): 2258 f(x',f(f(x,y)',z)') = c_0. [para(2048(a,1),811(a,1,2,1)),rewrite(2042(6),2048(10))]. given #148 (F,wt=12): 2259 f(f(x,y)',f(z,x')') = c_0. [para(2048(a,1),823(a,1,2,1)),rewrite(2042(6),2048(10))]. given #149 (T,wt=12): 2261 f(f(x,y)',f(x',z)') = c_0. [para(2048(a,1),937(a,1,2,2)),rewrite(776(6),2042(6),2048(10))]. given #150 (T,wt=12): 2273 f(x',f(y,f(z,x)')') = c_0. [para(2049(a,1),790(a,1,2,1)),rewrite(2042(6),2049(10))]. given #151 (A,wt=17): 768 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [back_rewrite(130),rewrite(688(6),654(3),654(6),654(9))]. given #152 (F,wt=12): 2274 f(x',f(f(y,x)',z)') = c_0. [para(2049(a,1),811(a,1,2,1)),rewrite(2042(6),2049(10))]. given #153 (F,wt=12): 3221 f(x,f(y,f(x',z)')) = x'. [para(112(a,1),2754(a,1,1))]. given #154 (T,wt=12): 3250 f(x,f(f(y,x')',z)) = x'. [para(112(a,1),2755(a,1,1))]. given #155 (T,wt=12): 3289 f(x,f(f(x',y)',z)) = x'. [para(112(a,1),3223(a,1,1))]. given #156 (A,wt=17): 769 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [back_rewrite(129),rewrite(654(3),654(5),688(6),654(3),654(4),654(9))]. given #157 (F,wt=13): 2450 f(f(x,y),f(z,f(y,x)')') = c_0. [para(2230(a,1),790(a,1,2,1)),rewrite(2042(6),2230(10))]. given #158 (F,wt=13): 2451 f(f(x,y),f(f(y,x)',z)') = c_0. [para(2230(a,1),811(a,1,2,1)),rewrite(2042(6),2230(10))]. given #159 (T,wt=13): 2452 f(f(x,y)',f(z,f(y,x))') = c_0. [para(2230(a,1),823(a,1,2,1)),rewrite(2042(6),2230(10))]. given #160 (T,wt=13): 2454 f(f(x,y)',f(f(y,x),z)') = c_0. [para(2230(a,1),937(a,1,2,2)),rewrite(776(6),2042(6),2230(10))]. given #161 (A,wt=19): 772 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [back_rewrite(72),rewrite(688(4),654(6),654(12))]. given #162 (F,wt=13): 2753 f(f(x,y)',f(z,y')) = f(x,y). [para(485(a,1),2046(a,1,2,2,1))]. given #163 (F,wt=13): 2757 f(f(x,y)',f(z,x')) = f(x,y). [para(671(a,1),2046(a,1,2,2,1))]. given #164 (T,wt=13): 2815 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(2700),rewrite(2789(4),776(6))]. given #165 (T,wt=13): 2816 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(2698),rewrite(2789(4),776(6))]. given #166 (A,wt=20): 774 f(f(x,y),f(x,f(f(x,y),f(z,f(x,f(u,y))))')) = x. [back_rewrite(45),rewrite(654(3),654(8),654(9),688(13),688(7),654(4),688(15))]. given #167 (F,wt=13): 3127 f(f(x',y),f(x,z)') = f(x,z). [para(693(a,1),2792(a,1,2)),rewrite(776(7),2789(7),112(11),776(10),1068(10))]. given #168 (F,wt=13): 3136 f(f(x',y),f(z,x)') = f(z,x). [para(700(a,1),2792(a,1,2)),rewrite(776(7),2789(7),112(11),776(10),1066(10))]. given #169 (T,wt=13): 3251 f(f(x,y)',f(y',z)) = f(x,y). [para(485(a,1),2755(a,1,2,1,1))]. given #170 (T,wt=13): 3253 f(f(x,y)',f(x',z)) = f(x,y). [para(671(a,1),2755(a,1,2,1,1))]. given #171 (A,wt=20): 775 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,y')))))) = x. [back_rewrite(44),rewrite(654(3),654(8),654(9),688(13),688(7),654(4),688(15))]. given #172 (F,wt=13): 3440 f(f(x,f(y,z))',f(z,y)') = c_0. [para(1551(a,1),2051(a,1,2,1))]. given #173 (F,wt=13): 3579 f(f(x,f(y,z)')',f(z,y)) = c_0. [para(1533(a,1),2225(a,1,2,1)),rewrite(112(7))]. given #174 (T,wt=13): 4445 f(f(x,y'),f(z,y)') = f(z,y). [para(2753(a,1),776(a,1)),flip(a)]. given #175 (T,wt=13): 4491 f(f(x,y'),f(y,z)') = f(y,z). [para(2757(a,1),776(a,1)),flip(a)]. given #176 (A,wt=19): 789 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [back_rewrite(674),rewrite(688(4))]. given #177 (F,wt=13): 4527 f(f(x,y)',f(x,f(z,y'))) = c_0. [para(112(a,1),2815(a,1,1,1,2))]. given #178 (F,wt=13): 4528 f(f(x',y)',f(y,f(z,x))) = c_0. [para(776(a,1),2815(a,1,1,1))]. given #179 (T,wt=12): 5199 f(x',f(f(y,x),f(z,x))) = c_0. [para(485(a,1),4528(a,1,1,1))]. given #180 (T,wt=12): 5203 f(x',f(f(x,y),f(z,x))) = c_0. [para(671(a,1),4528(a,1,1,1))]. given #181 (A,wt=23): 791 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,z)))))) = x. [back_rewrite(670),rewrite(688(14),688(6),688(14))]. given #182 (F,wt=12): 5295 f(x',f(f(y,x),f(x,z))) = c_0. [para(776(a,1),5199(a,1,2,2))]. given #183 (F,wt=12): 5344 f(x',f(f(x,y),f(x,z))) = c_0. [para(776(a,1),5203(a,1,2,2))]. given #184 (T,wt=13): 4529 f(f(x,y')',f(f(z,y),x)) = c_0. [para(776(a,1),2815(a,1,2))]. given #185 (T,wt=13): 4536 f(x,f(y',f(f(z,y),x))') = c_0. [para(854(a,1),2815(a,1,2)),rewrite(776(4),776(6))]. given #186 (A,wt=17): 792 f(f(x,y),f(x,f(z,f(f(x,y),f(u,y))))) = x. [back_rewrite(669),rewrite(688(9),688(7),688(13))]. given #187 (F,wt=13): 4541 f(x,f(y',f(f(y,z),x))') = c_0. [para(859(a,1),2815(a,1,2)),rewrite(776(4),776(6))]. given #188 (F,wt=13): 4548 f(f(x,f(y,z)')',f(z,x)) = c_0. [para(823(a,1),2815(a,1,2))]. given #189 (T,wt=13): 4554 f(f(x,f(y,z)')',f(y,x)) = c_0. [para(941(a,1),2815(a,1,2))]. given #190 (T,wt=13): 4601 f(f(x,y)',f(x,f(y',z))) = c_0. [para(112(a,1),2816(a,1,1,1,2))]. given #191 (A,wt=15): 793 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [back_rewrite(668),rewrite(688(13),688(7),688(12))]. given #192 (F,wt=13): 4602 f(f(x',y)',f(y,f(x,z))) = c_0. [para(776(a,1),2816(a,1,1,1))]. given #193 (F,wt=13): 4603 f(f(x,y')',f(f(y,z),x)) = c_0. [para(776(a,1),2816(a,1,2))]. given #194 (T,wt=13): 4610 f(x,f(y',f(x,f(z,y)))') = c_0. [para(855(a,1),2816(a,1,2)),rewrite(776(4),776(6))]. given #195 (T,wt=13): 4614 f(x,f(y',f(x,f(y,z)))') = c_0. [para(925(a,1),2816(a,1,2)),rewrite(776(4),776(6))]. given #196 (A,wt=15): 794 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [back_rewrite(667),rewrite(688(4),688(10))]. given #197 (F,wt=13): 5104 f(f(x,y)',f(y,f(z,x'))) = c_0. [para(776(a,1),4527(a,1,1,1))]. given #198 (F,wt=13): 5105 f(f(x,y)',f(f(z,y'),x)) = c_0. [para(776(a,1),4527(a,1,2))]. given #199 (T,wt=13): 5124 f(x,f(y,f(f(z,y'),x))') = c_0. [para(854(a,1),4527(a,1,2)),rewrite(776(4),776(6))]. given #200 (T,wt=13): 5133 f(x,f(y,f(f(y',z),x))') = c_0. [para(859(a,1),4527(a,1,2)),rewrite(776(4),776(6))]. given #201 (A,wt=22): 801 f(f(x,y),f(x',f(f(x,y),f(z,y)))) = f(f(x,y),f(z,y)). [back_rewrite(752),rewrite(776(5),776(7))]. given #202 (F,wt=13): 5200 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(485(a,1),4528(a,1,2,2))]. given #203 (F,wt=13): 5202 f(f(x',y)',f(f(z,x),y)) = c_0. [para(776(a,1),4528(a,1,2))]. given #204 (T,wt=13): 5204 f(f(f(x,y)',z)',f(z,x)) = c_0. [para(671(a,1),4528(a,1,2,2))]. given #205 (T,wt=13): 5211 f(x,f(f(y,z)',f(z,x))') = c_0. [para(702(a,1),4528(a,1,2)),rewrite(776(6))]. given #206 (A,wt=20): 803 f(f(x,y)',f(y,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(699),rewrite(776(4),776(7))]. given #207 (F,wt=13): 5213 f(x,f(f(y,z)',f(x,y))') = c_0. [para(740(a,1),4528(a,1,2)),rewrite(776(6))]. given #208 (F,wt=13): 5215 f(x,f(f(y,z)',f(x,z))') = c_0. [para(795(a,1),4528(a,1,2)),rewrite(776(6))]. given #209 (T,wt=13): 5219 f(x,f(f(y,z)',f(y,x))') = c_0. [para(856(a,1),4528(a,1,2)),rewrite(776(6))]. given #210 (T,wt=13): 5294 f(x,f(f(y,x'),f(z,x'))) = c_0. [para(112(a,1),5199(a,1,1))]. given #211 (A,wt=20): 804 f(f(x,y)',f(x,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(692),rewrite(776(4),776(7))]. given #212 (F,wt=13): 5321 f(x',f(f(y,x),f(z,x))') = x. [para(5199(a,1),2789(a,1,2)),rewrite(776(3),2042(3),112(2)),flip(a)]. given #213 (F,wt=13): 5343 f(x,f(f(x',y),f(z,x'))) = c_0. [para(112(a,1),5203(a,1,1))]. given #214 (T,wt=13): 5370 f(x',f(f(x,y),f(z,x))') = x. [para(5203(a,1),2789(a,1,2)),rewrite(776(3),2042(3),112(2)),flip(a)]. given #215 (T,wt=13): 5531 f(x,f(f(y,x'),f(x',z))) = c_0. [para(112(a,1),5295(a,1,1))]. given #216 (A,wt=27): 808 f(f(f(x,y),z),f(y,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)). [back_rewrite(770),rewrite(776(5),776(8))]. given #217 (F,wt=13): 5556 f(x',f(f(y,x),f(x,z))') = x. [para(5295(a,1),2789(a,1,2)),rewrite(776(3),2042(3),112(2)),flip(a)]. given #218 (F,wt=13): 5570 f(x,f(f(x',y),f(x',z))) = c_0. [para(112(a,1),5344(a,1,1))]. given #219 (T,wt=13): 5595 f(x',f(f(x,y),f(x,z))') = x. [para(5344(a,1),2789(a,1,2)),rewrite(776(3),2042(3),112(2)),flip(a)]. given #220 (T,wt=13): 5703 f(f(x',y)',f(f(x,z),y)) = c_0. [para(887(a,1),4536(a,1,2,1,2)),rewrite(776(6))]. given #221 (A,wt=24): 809 f(f(x',y),f(x,f(f(x',y),f(z,y)))) = f(f(x',y),f(z,y)). [back_rewrite(767),rewrite(776(5),776(8))]. given #222 (F,wt=13): 5748 f(x,f(y',f(f(z,y),x))) = x'. [para(4536(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #223 (F,wt=13): 5947 f(x,f(y',f(f(y,z),x))) = x'. [para(4541(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #224 (T,wt=13): 5969 f(f(x,y)',f(f(y',z),x)) = c_0. [para(637(a,1),4548(a,1,1,1,2,1)),rewrite(112(2))]. given #225 (T,wt=13): 6064 f(f(x,y)',f(y,f(x',z))) = c_0. [para(3127(a,1),4548(a,1,1,1))]. given #226 (A,wt=15): 814 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [back_rewrite(749),rewrite(776(3),776(4))]. given #227 (F,wt=13): 6187 f(x,f(y,f(x,f(z,y')))') = c_0. [para(855(a,1),4601(a,1,2)),rewrite(776(4),776(6))]. given #228 (F,wt=13): 6198 f(x,f(y,f(x,f(y',z)))') = c_0. [para(925(a,1),4601(a,1,2)),rewrite(776(4),776(6))]. given #229 (T,wt=13): 6551 f(x,f(y',f(x,f(z,y)))) = x'. [para(4610(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #230 (T,wt=13): 6613 f(x,f(y',f(x,f(y,z)))) = x'. [para(4614(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #231 (A,wt=15): 815 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [back_rewrite(748),rewrite(776(6))]. given #232 (F,wt=13): 6796 f(f(x,y)',f(f(z,x'),y)) = c_0. [para(776(a,1),5104(a,1,2))]. given #233 (F,wt=13): 6953 f(f(x,y)',f(f(x',z),y)) = c_0. [para(887(a,1),5124(a,1,2,1,2)),rewrite(776(6))]. given #234 (T,wt=13): 6991 f(x,f(y,f(f(z,y'),x))) = x'. [para(5124(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #235 (T,wt=13): 7064 f(x,f(y,f(f(y',z),x))) = x'. [para(5133(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #236 (A,wt=15): 816 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x. [back_rewrite(747),rewrite(776(6))]. given #237 (F,wt=13): 7590 f(x,f(f(y,z)',f(z,x))) = x'. [para(5211(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #238 (F,wt=13): 7759 f(x,f(f(y,z)',f(x,y))) = x'. [para(5213(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #239 (T,wt=13): 7856 f(x,f(f(y,z)',f(x,z))) = x'. [para(5215(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #240 (T,wt=13): 7956 f(x,f(f(y,z)',f(y,x))) = x'. [para(5219(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #241 (A,wt=27): 817 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(u,z)))) = f(f(f(x,y),z),f(u,z)). [back_rewrite(733),rewrite(776(5),776(8))]. given #242 (F,wt=13): 9058 f(x,f(y,f(x,f(z,y')))) = x'. [para(6187(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #243 (F,wt=13): 9108 f(x,f(y,f(x,f(y',z)))) = x'. [para(6198(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. given #244 (T,wt=13): 9543 f(x',y) = f(y,f(f(z,y'),x)). [para(6991(a,1),835(a,1,1)),rewrite(776(7),9228(7),2789(5),112(3))]. given #245 (T,wt=13): 9618 f(x',y) = f(y,f(f(y',z),x)). [para(7064(a,1),835(a,1,1)),rewrite(776(7),9228(7),2789(5),112(3))]. given #246 (A,wt=20): 820 f(f(x,y),f(y,f(f(x,y),z))) = f(y,f(f(x,y),z))'. [back_rewrite(713),rewrite(776(3),776(5),776(8))]. given #247 (F,wt=13): 10749 f(x,f(y,f(z,x'))) = f(x,y'). [para(9058(a,1),814(a,1,2)),flip(a)]. given #248 (F,wt=13): 10801 f(x,f(y,f(x',z))) = f(x,y'). [para(9108(a,1),814(a,1,2)),flip(a)]. given #249 (T,wt=13): 10815 f(x,f(f(y,x'),z)) = f(x,z'). [para(9543(a,1),776(a,1))]. given #250 (T,wt=13): 10828 f(x,f(y,f(x',z))') = f(x,y). [para(740(a,1),9543(a,2,2)),rewrite(776(5))]. given #251 (A,wt=23): 821 f(f(x,f(y,f(x,z))),f(f(y,f(x,z)),f(u,y))) = f(y,f(x,z)). [back_rewrite(709),rewrite(776(7),776(8))]. given #252 (F,wt=13): 10830 f(x,f(y,f(z,x'))') = f(x,y). [para(795(a,1),9543(a,2,2)),rewrite(776(5))]. given #253 (F,wt=13): 10842 f(x,f(f(x',y),z)') = f(x,z). [para(887(a,1),9543(a,2,2)),rewrite(776(5))]. given #254 (T,wt=13): 10843 f(x,f(f(y,x'),z)') = f(x,z). [para(899(a,1),9543(a,2,2)),rewrite(776(5))]. given #255 (T,wt=13): 10904 f(x,f(y,f(z,f(x,y))'))' = x. [para(9543(a,2),758(a,1,2,2)),rewrite(776(6),2866(8))]. given #256 (A,wt=25): 822 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(u,x))) = f(y,f(x,f(y,z))). [back_rewrite(707),rewrite(776(5),776(11))]. given #257 (F,wt=13): 11023 f(x,f(f(x',y),z)) = f(x,z'). [para(9618(a,1),776(a,1))]. given #258 (F,wt=13): 12053 f(x,f(y,f(z,f(x,y))')) = x'. [para(10904(a,1),112(a,1,1)),flip(a)]. given #259 (T,wt=13): 12088 f(x,f(y,f(z,f(x,y))')') = c_0. [para(10904(a,1),2049(a,1,2)),rewrite(776(6))]. given #260 (T,wt=13): 12525 f(x,f(y,f(z,f(y,x))')) = x'. [para(776(a,1),12053(a,1,2,2,1,2))]. given #261 (A,wt=20): 824 f(f(x,y),f(y,f(z,f(x,y)))) = f(y,f(z,f(x,y)))'. [back_rewrite(705),rewrite(776(3),776(5),776(8))]. given #262 (F,wt=13): 12526 f(x,f(y,f(f(x,y),z)')) = x'. [para(776(a,1),12053(a,1,2,2,1))]. given #263 (F,wt=13): 13233 f(x,f(y,f(z,f(y,x))')') = c_0. [para(776(a,1),12088(a,1,2,1,2,1,2))]. given #264 (T,wt=13): 13234 f(x,f(y,f(f(x,y),z)')') = c_0. [para(776(a,1),12088(a,1,2,1,2,1))]. given #265 (T,wt=13): 13275 f(x,f(y,f(f(y,x),z)')) = x'. [para(776(a,1),12525(a,1,2,2,1))]. given #266 (A,wt=31): 825 f(f(f(x,y)',z),f(f(y,f(f(x,y)',z)),f(u,f(x,y)'))) = f(y,f(f(x,y)',z)). [back_rewrite(698),rewrite(776(7),776(16))]. given #267 (F,wt=13): 13488 f(x,f(y,f(f(y,x),z)')') = c_0. [para(12526(a,1),12088(a,1,2,1,2,1)),rewrite(112(5),776(4))]. given #268 (F,wt=14): 1088 f(f(x,y),f(y,f(z,f(y,x')))) = y. [para(835(a,1),790(a,1,2,1)),rewrite(835(10))]. given #269 (T,wt=14): 1089 f(f(x,y),f(x,f(z,f(y',x)))) = x. [para(836(a,1),790(a,1,2,1)),rewrite(836(10))]. given #270 (T,wt=14): 1091 f(f(x',y),f(y,f(z,f(y,x)))) = y. [para(837(a,1),790(a,1,2,1)),rewrite(837(10))]. given #271 (A,wt=15): 827 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [back_rewrite(672),rewrite(776(3),776(4))]. given #272 (F,wt=13): 14093 f(f(x,y)',z) = f(y,f(x,z)'). [back_rewrite(10358),rewrite(13933(4),14080(9))]. given #273 (F,wt=13): 14837 f(x,f(y,z)') = f(z,f(x,y)'). [back_rewrite(10610),rewrite(14093(3),14093(7),14093(7),10346(5),14093(6)),flip(a)]. given #274 (T,wt=13): 14862 f(x,f(y,z)') = f(y,f(x,z)'). [back_rewrite(10510),rewrite(14093(5),14093(6),2789(4),112(3),14272(4),14272(7),112(4),2789(3),112(2),14093(6))]. ============================== PROOF ================================= % Proof 1 at 8.36 (+ 0.05) seconds: "Sheffer". % Length of proof is 178. % Level of proof is 42. % Maximum clause weight is 95. % Given clauses 274. 1 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. 2 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). [assumption]. 3 x' = f(x,x). [assumption]. 4 f(x,x) = x'. [copy(3),flip(a)]. 5 a'' != a | f(a,f(b,b')) != a' | f(f(b',a),f(c',a)) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(2),rewrite(4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34))]. 6 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z))))) = f(z,f(f(x,z),z)). [para(1(a,1),1(a,1,1,2,1))]. 7 f(f(f(x,f(y,z)),f(f(u,f(x,f(y,z))),f(x,f(y,z)))),f(u,x)) = u. [para(1(a,1),1(a,1,2,2))]. 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(1(a,1),1(a,1,2))]. 9 f(f(x,f(x',x)),f(x,f(y,x))) = x. [para(4(a,1),1(a,1,1,2,1))]. 10 f(f(x,f(f(y,x),x)),f(y,x')) = y. [para(4(a,1),1(a,1,2,2))]. 12 f(x,f(x',x))' = x. [para(4(a,1),1(a,1)),rewrite(4(1))]. 18 f(f(f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x)))),f(f(x,f(f(y,x),x)),f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x)))))),f(f(f(y,f(u,x)),f(y,f(y,f(u,x)))),f(v,f(f(x,f(f(y,x),x)),f(z,f(y,f(u,x))))))) = f(f(y,f(u,x)),f(y,f(y,f(u,x)))). [para(6(a,1),1(a,1,1,2,1))]. 19 f(f(f(x,f(y,f(z,u))),f(f(f(f(y,f(z,u)),f(y,f(y,f(z,u)))),f(x,f(y,f(z,u)))),f(x,f(y,f(z,u))))),f(u,f(f(y,u),u))) = f(f(y,f(z,u)),f(y,f(y,f(z,u)))). [para(6(a,1),1(a,1,2))]. 22 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),x)) = f(z,f(f(x,z),z)). [para(1(a,1),6(a,1,2,2))]. 38 f(f(x',f(f(f(x,f(f(y,x),x)),x'),x')),y) = f(x,f(f(y,x),x)). [para(10(a,1),1(a,1,2))]. 43 f(f(x,f(f(y,f(f(x,y),y)),x)),f(f(y',f(f(f(y,f(f(x,y),y)),y'),y')),f(z,x))) = f(y',f(f(f(y,f(f(x,y),y)),y'),y')). [para(10(a,1),6(a,1,1,1)),rewrite(10(9),10(20))]. 65 f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. [para(7(a,1),1(a,1,2,2))]. 67 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(1(a,1),7(a,1,1,1)),rewrite(1(6),1(7))]. 69 f(f(f(x,y),f(f(x,y)',f(x,y))),f(f(x,y),x)) = f(x,y). [para(7(a,1),9(a,1,2,2))]. 70 f(f(x,f(f(y,x),x)),f(y,f(x,f(x',x)))) = y. [para(9(a,1),7(a,1,1,1)),rewrite(9(6),9(7))]. 88 f(f(x,f(x',x)),f(x,f(x,f(x',x)))) = x. [para(4(a,1),70(a,1,1,2,1))]. 91 f(x,f(x',x)) = x'. [para(70(a,1),6(a,1,2)),rewrite(88(8),4(1),4(2)),flip(a)]. 92 f(f(x',f(f(f(x',f(x,x')),x'),x')),x') = f(x',f(x,x')). [para(6(a,1),70(a,1,2)),rewrite(4(1),91(3),4(2),91(4),4(3),91(5),4(6),91(8),4(8),91(10),4(11),91(13),4(13),91(15),4(14),91(16))]. 96 f(x',f(x,x')) = x. [back_rewrite(88),rewrite(91(3),91(4))]. 100 f(f(x,y)',f(f(x,y),x)) = f(x,y). [back_rewrite(69),rewrite(91(6))]. 112 x'' = x. [back_rewrite(12),rewrite(91(3))]. 114 f(f(x',f(f(x,x'),x')),x') = x. [back_rewrite(92),rewrite(96(5),96(12))]. 122 f(a,f(b,b')) != a' | f(f(b',a),f(c',a)) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(5),rewrite(112(3)),xx(a)]. 123 f(f(x',f(f(y,x'),x')),f(y,x)) = y. [para(112(a,1),10(a,1,2,2))]. 140 f(f(f(x,f(f(y,x),x)),f(f(f(y,f(f(z,y),y)),f(x,f(f(y,x),x))),f(x,f(f(y,x),x)))),z) = f(y,f(f(z,y),y)). [para(8(a,1),8(a,1,1,1)),rewrite(8(16),8(20))]. 199 f(f(x,f(f(f(x',f(f(y,x'),x')),x),x)),y) = f(x',f(f(y,x'),x')). [para(114(a,1),8(a,1,1,1)),rewrite(114(14),114(15))]. 231 f(f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(f(f(z,f(f(x,z),z)),f(f(u,f(z,f(f(x,z),z))),f(z,f(f(x,z),z)))),f(f(x,f(y,z)),f(x,f(x,f(y,z))))),f(f(x,f(y,z)),f(x,f(x,f(y,z)))))),u) = f(f(z,f(f(x,z),z)),f(f(u,f(z,f(f(x,z),z))),f(z,f(f(x,z),z)))). [para(19(a,1),8(a,1,1,1)),rewrite(19(40),19(47))]. 280 f(f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(u,f(f(x,f(y,z)),f(x,f(x,f(y,z))))),f(f(x,f(y,z)),f(x,f(x,f(y,z)))))),f(u,f(f(f(z,f(f(x,z),z)),f(v,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(f(z,f(f(x,z),z)),f(v,f(x,f(y,z)))))))) = u. [para(18(a,1),65(a,1,1,1)),rewrite(18(41),18(48))]. 296 f(f(x,f(f(y',x),x)),y) = y'. [para(1(a,1),67(a,1,2)),rewrite(4(1),91(3),4(6),91(8))]. 297 f(f(x,f(f(y,f(f(x,y),y)),x)),f(f(f(z,f(f(y,z),z)),f(f(f(y,f(f(x,y),y)),f(z,f(f(y,z),z))),f(z,f(f(y,z),z)))),f(u,x))) = f(f(z,f(f(y,z),z)),f(f(f(y,f(f(x,y),y)),f(z,f(f(y,z),z))),f(z,f(f(y,z),z)))). [para(67(a,1),6(a,1,1,1)),rewrite(67(11),67(28))]. 298 f(f(x,f(f(y,x),x)),y') = y. [para(6(a,1),67(a,1,2)),rewrite(4(1),91(3),4(2),91(4),96(4),4(4),91(6),4(6),91(8),4(7),91(9),96(9))]. 299 f(f(f(x,f(y,f(f(z,y),y))),f(x,f(x,f(y,f(f(z,y),y))))),f(f(z,f(f(x,z),z)),f(x,f(y,f(f(z,y),y)))')) = f(z,f(f(x,z),z)). [para(67(a,1),10(a,1,1,2,1))]. 329 f(f(f(x,y),f(f(f(y,f(f(z,f(f(y,z),z)),y)),f(x,y)),f(x,y))),f(f(u,f(f(z,u),u)),f(f(f(z,f(f(y,z),z)),f(u,f(f(z,u),u))),f(u,f(f(z,u),u))))) = f(y,f(f(z,f(f(y,z),z)),y)). [para(67(a,1),19(a,1,1,1,2)),rewrite(67(9),67(12),67(14),67(16),67(35),67(38))]. 337 f(f(f(x,y),f(x,f(x,y))),f(f(f(y,z),f(f(x,f(y,z)),f(y,z))),f(u,f(f(f(x,y),u),u)))) = f(f(y,z),f(f(x,f(y,z)),f(y,z))). [para(65(a,1),67(a,1,1,2,1))]. 354 f(x,f(f(y,f(f(x,y),y)),x)) = f(y,f(f(x,y),y)). [para(298(a,1),10(a,1,1,2,1)),rewrite(96(4),112(5))]. 375 f(x,f(y,f(f(x,y),y))') = f(y,f(f(x,y),y)). [para(298(a,1),298(a,1,1,2,1)),rewrite(96(4))]. 380 f(f(f(x,y),f(f(f(z,f(f(y,z),z)),f(x,y)),f(x,y))),f(f(u,f(f(z,u),u)),f(f(f(z,f(f(y,z),z)),f(u,f(f(z,u),u))),f(u,f(f(z,u),u))))) = f(z,f(f(y,z),z)). [back_rewrite(329),rewrite(354(6),354(30))]. 382 f(f(x,f(f(y,x),x)),f(f(f(z,f(f(x,z),z)),f(f(f(x,f(f(y,x),x)),f(z,f(f(x,z),z))),f(z,f(f(x,z),z)))),f(u,y))) = f(f(z,f(f(x,z),z)),f(f(f(x,f(f(y,x),x)),f(z,f(f(x,z),z))),f(z,f(f(x,z),z)))). [back_rewrite(297),rewrite(354(5))]. 391 f(f(x,f(f(y,x),x)),f(f(x',f(f(f(x,f(f(y,x),x)),x'),x')),f(z,y))) = f(x',f(f(f(x,f(f(y,x),x)),x'),x')). [back_rewrite(43),rewrite(354(5))]. 406 f(x',f(f(y,f(f(x',y),y)),f(z,x))) = f(y,f(f(x',y),y)). [para(296(a,1),1(a,1,1,2,1)),rewrite(91(3))]. 407 f(f(x,f(f(f(y,f(f(f(z,x)',y),y)),x),x)),f(z,x)') = f(y,f(f(f(z,x)',y),y)). [para(296(a,1),1(a,1,2))]. 409 f(f(f(f(x,f(f(y',x),x)),f(z,y)),f(f(x,f(f(y',x),x)),f(f(x,f(f(y',x),x)),f(z,y)))),f(y',f(u,f(f(x,f(f(y',x),x)),f(z,y))))) = y'. [para(296(a,1),6(a,1,2,1,2,1)),rewrite(91(21),296(33),91(31))]. 411 f(x,f(f(f(y,x)',x),x)) = f(y,x). [para(296(a,1),8(a,1,1,2,1)),rewrite(91(6),4(5),112(3)),flip(a)]. 416 f(f(x,f(f(f(y,f(f(f(z,f(f(x,z),z))',y),y)),x),x)),f(z,f(f(x,z),z))') = f(y,f(f(f(z,f(f(x,z),z))',y),y)). [para(296(a,1),67(a,1,2))]. 485 f(x',f(y,x)) = x. [para(411(a,1),1(a,1,2)),rewrite(4(1),91(3))]. 492 f(x,f(y,x')) = x'. [para(411(a,1),6(a,1,2)),rewrite(4(1),91(3),4(2),91(4),96(4),4(1),91(3),4(4),91(6))]. 496 f(f(x',x),x) = x'. [para(91(a,1),411(a,1,2,1,1,1)),rewrite(112(4),91(5),485(6),91(6))]. 500 f(f(x,x'),x') = x. [para(96(a,1),411(a,1,2,1,1,1)),rewrite(96(6),492(5),96(8))]. 505 f(f(x,y)',f(f(x,y),y)) = f(x,y). [para(411(a,1),100(a,1,1,1)),rewrite(411(7),411(10))]. 511 f(f(x,y),f(f(x',f(x,y)),f(x,y))) = x. [para(123(a,1),411(a,1,2,1,1,1)),rewrite(123(15))]. 524 f(f(f(f(f(x,y)',y),y),f(f(x,y),f(f(f(x,y)',y),y))),y') = y. [para(411(a,1),298(a,1,1,2,1))]. 525 f(f(f(f(f(x,y')',y'),y'),f(f(x,y'),f(f(f(x,y')',y'),y'))),y) = y'. [para(411(a,1),296(a,1,1,2,1))]. 532 f(f(f(x,f(y,f(f(f(z,x)',x),x))),f(x,f(x,f(y,f(f(f(z,x)',x),x))))),f(f(f(f(f(z,x)',x),x),f(f(z,x),f(f(f(z,x)',x),x))),x)) = f(f(f(f(z,x)',x),x),f(f(z,x),f(f(f(z,x)',x),x))). [para(411(a,1),22(a,1,2,1,2,1)),rewrite(411(36))]. 536 f(f(f(f(x,y)',y),y),f(f(f(x,y)',f(f(f(x,y)',y),y)),f(f(f(x,y)',y),y))) = f(x,y). [para(411(a,1),411(a,1,2,1,1,1)),rewrite(411(22))]. 591 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(y,z))) = f(z,f(f(x,z),z)). [para(485(a,1),6(a,1,2,2))]. 595 f(f(x,f(f(f(f(y,x),f(f(z,f(y,x)),f(y,x))),x),x)),z) = f(f(y,x),f(f(z,f(y,x)),f(y,x))). [para(485(a,1),8(a,1,1,1)),rewrite(485(9),485(10))]. 596 f(x',f(y,f(f(x,y),y))) = x. [para(8(a,1),485(a,1,2))]. 603 f(f(f(x,f(y,z)),f(f(f(f(y,z),f(y,f(y,z))),f(x,f(y,z))),f(x,f(y,z)))),f(f(u,z),f(f(y,f(u,z)),f(u,z)))) = f(f(y,z),f(y,f(y,z))). [para(485(a,1),19(a,1,1,1,2,2)),rewrite(485(5),485(6),485(9),485(12),485(23),485(24))]. 605 f(f(f(x,y),f(f(f(f(z,f(x,y)),f(z,f(z,f(x,y)))),f(x,y)),f(x,y))),f(y,f(f(z,y),y))) = f(f(z,f(x,y)),f(z,f(z,f(x,y)))). [para(485(a,1),19(a,1,1,1)),rewrite(485(12),485(14))]. 614 f(x',x) = f(x,x'). [para(485(a,1),22(a,1,1,1)),rewrite(485(4),91(3),496(4),500(5),496(5))]. 618 f(f(x,y)',y) = f(x,y). [para(485(a,1),485(a,1,2))]. 643 f(f(f(x,y),y),f(f(x,y),f(f(x,y),y))) = f(x,y). [back_rewrite(536),rewrite(618(3),618(7),505(7),618(6))]. 644 f(f(f(x,f(y,f(f(z,x),x))),f(x,f(x,f(y,f(f(z,x),x))))),f(f(z,x),x)) = f(z,x). [back_rewrite(532),rewrite(618(3),618(7),618(13),618(16),643(17),618(16),618(19),643(20))]. 645 f(f(x,y'),y) = y'. [back_rewrite(525),rewrite(618(5),618(11),643(12))]. 646 f(f(x,y),y') = y. [back_rewrite(524),rewrite(618(3),618(6),643(7))]. 654 f(x,f(f(y,x),x)) = f(y,x). [back_rewrite(411),rewrite(618(3))]. 666 f(f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(y,z)),f(x,z)) = f(f(x,f(y,z)),f(x,f(x,f(y,z)))). [back_rewrite(605),rewrite(654(12),654(11))]. 667 f(f(f(f(x,y),f(x,f(x,y))),f(z,f(x,y))),f(x,f(u,y))) = f(f(x,y),f(x,f(x,y))). [back_rewrite(603),rewrite(654(13),654(13))]. 671 f(x',f(x,y)) = x. [back_rewrite(596),rewrite(654(4))]. 672 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). [back_rewrite(595),rewrite(654(6),654(5),654(10))]. 673 f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(x,z),f(y,z))) = f(x,z). [back_rewrite(591),rewrite(654(9),654(13))]. 688 f(f(x,y),f(x,f(x,y))) = x. [back_rewrite(511),rewrite(671(4))]. 692 f(f(f(f(x,y)',z),x),f(x,y)') = f(f(x,y)',z). [back_rewrite(416),rewrite(654(3),654(5),654(6),654(7),654(10),654(12))]. 697 f(f(x',y),f(x',f(z,f(f(x',y),f(u,x))))) = x'. [back_rewrite(409),rewrite(654(4),654(8),654(10),688(12),654(7))]. 699 f(f(f(f(x,y)',z),y),f(x,y)') = f(f(x,y)',z). [back_rewrite(407),rewrite(654(5),654(6),654(12))]. 700 f(x',f(f(x',y),f(z,x))) = f(x',y). [back_rewrite(406),rewrite(654(5),654(10))]. 702 f(f(x,y),f(y,f(z,x))) = y. [back_rewrite(391),rewrite(654(3),654(5),646(5),671(5),654(8),646(8),671(8))]. 710 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)). [back_rewrite(382),rewrite(654(3),654(4),654(5),654(6),654(8),654(8),654(10),654(11),654(12),654(14),654(14))]. 712 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y). [back_rewrite(380),rewrite(654(4),654(7),654(6),654(7),654(8),654(10),654(10),654(10))]. 714 f(x,f(x,y)') = f(x,y). [back_rewrite(375),rewrite(654(3),654(6))]. 727 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [back_rewrite(337),rewrite(688(4),654(6),654(6),654(12))]. 735 f(x,f(f(x,y),f(x,f(y,z))')) = f(x,y). [back_rewrite(299),rewrite(654(3),654(5),688(6),654(3),654(4),654(9))]. 740 f(f(x,y),f(x,f(y,z))) = x. [back_rewrite(280),rewrite(688(6),688(6),688(7),654(3),654(4),654(9),654(10),688(14))]. 749 f(f(f(x,f(y,z)),y),x) = f(x,f(y,z)). [back_rewrite(231),rewrite(688(6),654(3),654(4),654(6),654(6),688(8),688(9),654(5),654(7),654(8),654(10),654(10))]. 759 f(x',y) = f(y,x'). [back_rewrite(199),rewrite(654(6),645(3),614(2),492(3),654(8))]. 765 f(f(f(x,y),f(y,z)),x) = f(x,y). [back_rewrite(140),rewrite(654(3),654(4),654(5),654(7),654(7),654(7))]. 771 f(f(x',f(x',f(y,x'))),f(y,x)) = y. [back_rewrite(123),rewrite(759(5,R))]. 776 f(x,y) = f(y,x). [back_rewrite(38),rewrite(654(4),759(4,R),485(4),671(4),654(4))]. 790 f(x,f(f(x,y),f(z,y))) = f(x,y). [back_rewrite(673),rewrite(688(6))]. 794 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [back_rewrite(667),rewrite(688(4),688(10))]. 795 f(f(x,y),f(x,f(z,y))) = x. [back_rewrite(666),rewrite(688(6),776(4),688(10))]. 798 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(644),rewrite(776(2),776(6),688(10),776(2))]. 803 f(f(x,y)',f(y,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(699),rewrite(776(4),776(7))]. 804 f(f(x,y)',f(x,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(692),rewrite(776(4),776(7))]. 806 f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(122),rewrite(776(13),776(17))]. 807 f(f(x,y),f(x,y')) = x. [back_rewrite(771),rewrite(798(6),776(4))]. 811 f(x,f(f(x,y),f(y,z))) = f(x,y). [back_rewrite(765),rewrite(776(4))]. 814 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [back_rewrite(749),rewrite(776(3),776(4))]. 827 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [back_rewrite(672),rewrite(776(3),776(4))]. 835 f(f(x,y),f(y,x')) = y. [para(776(a,1),807(a,1,1))]. 836 f(f(x,y),f(y',x)) = x. [para(776(a,1),807(a,1,2))]. 838 f(f(x,y'),f(y,x)) = x. [para(835(a,1),776(a,1)),flip(a)]. 850 f(x,f(f(y,x)',f(x,y'))) = f(x,y'). [para(838(a,1),836(a,1,1))]. 853 f(x,f(f(y,x),f(z,x'))) = f(y,x). [para(485(a,1),702(a,1,1))]. 855 f(f(x,f(y,z)),f(z,x)) = x. [para(702(a,1),776(a,1)),flip(a)]. 856 f(f(x,y),f(y,f(x,z))) = y. [para(776(a,1),702(a,1,2,2))]. 857 f(f(x,y),f(f(z,x),y)) = y. [para(776(a,1),702(a,1,2))]. 888 f(f(x,y),f(x,f(f(x,y)',z))) = x. [para(714(a,1),740(a,1,1))]. 928 f(x,f(f(y,x),f(x',z))) = f(y,x). [para(485(a,1),856(a,1,1))]. 929 f(f(x,y),f(f(x,z),y)) = y. [para(776(a,1),856(a,1,2))]. 947 f(x,f(f(y,x'),f(z,x))) = f(z,x). [para(485(a,1),857(a,1,1))]. 948 f(x',f(f(y,x),f(z,x'))) = f(z,x'). [para(492(a,1),857(a,1,1))]. 949 f(x,f(f(y,x'),f(x,z))) = f(x,z). [para(671(a,1),857(a,1,1))]. 1189 f(f(x,y),f(x,f(f(x,y),z))) = f(x,f(f(x,y),z))'. [para(740(a,1),710(a,1,2)),rewrite(776(3),776(6),4(7),776(7),776(9)),flip(a)]. 1533 f(f(x,y),f(y,x)) = f(x,y)'. [para(712(a,1),790(a,1,2)),rewrite(4(3)),flip(a)]. 1551 f(f(x,y)',f(y,x)') = f(x,y). [para(1533(a,1),485(a,1,2))]. 1902 f(x',f(y,f(f(x,x'),f(z,x)))) = x. [para(697(a,1),949(a,1,2)),rewrite(4(3),112(2),112(4),776(3)),flip(a)]. 1923 f(x,f(f(x,x')',y)) = x'. [para(888(a,1),949(a,1,2)),rewrite(4(1)),flip(a)]. 1926 f(x',f(f(x,x')',y)) = x. [para(112(a,1),1923(a,1,2,1,1,2)),rewrite(776(3),112(8))]. 1928 f(f(x,x')',y) = f(x,x'). [para(1923(a,1),835(a,1,1)),rewrite(776(7),1926(7),776(2)),flip(a)]. 2013 f(x,f(y,y')) = x'. [para(1928(a,1),492(a,1,2))]. 2016 f(x,x') = f(y,y'). [para(1928(a,1),798(a,1,2,2)),rewrite(2013(3),1928(6))]. 2024 f(f(x,x'),y) = y'. [para(1928(a,1),928(a,1,2,2)),rewrite(2013(5),2013(6),112(4),2013(6))]. 2026 f(x,f(y,x')') = f(z,z'). [para(1928(a,1),947(a,1,2,2)),rewrite(2013(5),1928(8))]. 2027 f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(806),rewrite(2013(6)),xx(a)]. 2028 f(x,x') = c_0. [new_symbol(2016)]. 2039 f(x',f(y,f(c_0,f(z,x)))) = x. [back_rewrite(1902),rewrite(2028(3))]. 2040 f(x,f(y,x')') = c_0. [back_rewrite(2026),rewrite(2028(6))]. 2042 f(c_0,x) = x'. [back_rewrite(2024),rewrite(2028(2))]. 2043 f(x,c_0) = x'. [back_rewrite(2013),rewrite(2028(2))]. 2046 f(x',f(y,f(z,x)')) = x. [back_rewrite(2039),rewrite(2042(4))]. 2049 f(x',f(y,x)') = c_0. [para(2028(a,1),700(a,1,2,1)),rewrite(2042(4),112(7),776(6),2028(6))]. 2080 f(x,f(y,f(x,y))) = x'. [para(855(a,1),727(a,1,2)),rewrite(4(1)),flip(a)]. 2230 f(f(x,y),f(y,x)') = c_0. [para(1551(a,1),2040(a,1,2,1))]. 2360 f(x,f(y,f(y,x))) = x'. [para(776(a,1),2080(a,1,2,2))]. 2451 f(f(x,y),f(f(y,x)',z)') = c_0. [para(2230(a,1),811(a,1,2,1)),rewrite(2042(6),2230(10))]. 2534 f(x,f(y,f(y,x))') = c_0. [para(2360(a,1),2049(a,1,2,1)),rewrite(112(5),776(4))]. 2700 f(f(x,f(y,z)),f(x,f(x,z))') = c_0. [para(795(a,1),2534(a,1,2,1,2)),rewrite(776(4))]. 2753 f(f(x,y)',f(z,y')) = f(x,y). [para(485(a,1),2046(a,1,2,2,1))]. 2757 f(f(x,y)',f(z,x')) = f(x,y). [para(671(a,1),2046(a,1,2,2,1))]. 2789 f(x,f(x,y)) = f(x,y'). [para(2046(a,1),735(a,1,2,2,1,2)),rewrite(776(5),2753(5))]. 2792 f(x,f(y,x)) = f(x,y'). [back_rewrite(850),rewrite(2757(5))]. 2815 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(2700),rewrite(2789(4),776(6))]. 3157 f(f(x,y)',f(f(x,z),y)) = f(y,f(x,z)'). [para(929(a,1),2792(a,1,2)),rewrite(776(3),2792(3),776(8)),flip(a)]. 3182 f(f(x,y),f(z,y')') = f(z,y'). [para(853(a,1),2792(a,1,2)),rewrite(776(6),2789(6),776(11),948(11))]. 4310 f(f(x,y)',f(f(y,x)',z)') = f(f(y,x)',z). [para(2451(a,1),2792(a,1,2)),rewrite(776(6),2042(6),112(5),776(10)),flip(a)]. 4528 f(f(x',y)',f(y,f(z,x))) = c_0. [para(776(a,1),2815(a,1,1,1))]. 5211 f(x,f(f(y,z)',f(z,x))') = c_0. [para(702(a,1),4528(a,1,2)),rewrite(776(6))]. 5215 f(x,f(f(y,z)',f(x,z))') = c_0. [para(795(a,1),4528(a,1,2)),rewrite(776(6))]. 5219 f(x,f(f(y,z)',f(y,x))') = c_0. [para(856(a,1),4528(a,1,2)),rewrite(776(6))]. 6633 f(x,f(f(x,f(y,z))',f(x,f(u,f(x,z))))) = f(x,f(u,f(x,z))). [para(794(a,1),836(a,1,1))]. 7590 f(x,f(f(y,z)',f(z,x))) = x'. [para(5211(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. 7856 f(x,f(f(y,z)',f(x,z))) = x'. [para(5215(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. 7956 f(x,f(f(y,z)',f(y,x))) = x'. [para(5219(a,1),2789(a,1,2)),rewrite(2043(2),112(7)),flip(a)]. 8045 f(f(x,y)',f(x,f(f(x,y)',z))') = f(f(x,y)',z'). [para(804(a,1),2789(a,1,2)),rewrite(2789(6)),flip(a)]. 10329 f(f(x,y)',f(z,y)) = f(f(x,y)',z'). [para(7856(a,1),814(a,1,2)),flip(a)]. 10344 f(f(x,y)',f(x,z)') = f(y,f(x,z)'). [back_rewrite(3157),rewrite(10329(5))]. 10348 f(f(x,y)',z') = f(y,f(x,f(f(x,y)',z))'). [back_rewrite(8045),rewrite(10344(8)),flip(a)]. 10358 f(x,f(y,f(f(y,x)',f(y,z)))') = f(x,f(y,z)'). [back_rewrite(10344),rewrite(10348(5))]. 10510 f(x,f(y,f(f(y,x)',f(f(x,y)',z)))') = f(f(x,y)',z). [back_rewrite(4310),rewrite(10348(7))]. 13929 f(f(x,y)',f(y,z)) = f(y,f(x,f(f(x,y)',z))'). [para(7590(a,1),827(a,1,2)),rewrite(10348(4)),flip(a)]. 13933 f(f(x,y)',f(x,z)) = f(y,f(x,f(f(x,y)',z))'). [para(7956(a,1),827(a,1,2)),rewrite(10348(4)),flip(a)]. 14080 f(x,f(y,f(x,f(y,f(f(y,x)',z))'))') = f(f(y,x)',z). [back_rewrite(803),rewrite(13929(7),2789(6),10348(4))]. 14093 f(f(x,y)',z) = f(y,f(x,z)'). [back_rewrite(10358),rewrite(13933(4),14080(9))]. 14114 f(x,f(f(y,z),f(x,f(u,f(x,z))')')) = f(x,f(u,f(x,z))). [back_rewrite(6633),rewrite(14093(7),2789(5))]. 14271 f(x,f(y,f(x,f(y,z)'))') = f(x,f(y,z')'). [back_rewrite(13933),rewrite(14093(4),2789(2),14093(7)),flip(a)]. 14272 f(x,f(y,f(x,z))') = f(x,f(y,z')'). [back_rewrite(13929),rewrite(14093(4),14093(7),14271(10))]. 14862 f(x,f(y,z)') = f(y,f(x,z)'). [back_rewrite(10510),rewrite(14093(5),14093(6),2789(4),112(3),14272(4),14272(7),112(4),2789(3),112(2),14093(6))]. 15273 f(x,f(f(y,z),f(x,f(u,z')')')) = f(x,f(u,f(x,z))). [back_rewrite(14114),rewrite(14272(5))]. 16175 f(x,f(y,f(x,z)')) = f(x,f(y,z)). [para(14862(a,1),2789(a,1,2)),rewrite(112(7))]. 16253 f(x,f(y,f(x,z))) = f(x,f(y,z')). [back_rewrite(15273),rewrite(16175(8),3182(5)),flip(a)]. 17320 f(f(x,y),f(x,z')) = f(x,f(f(x,y),z))'. [back_rewrite(1189),rewrite(16253(5))]. 17670 $F # answer("Sheffer"). [back_rewrite(2027),rewrite(17320(9),776(7),16253(8),112(5),776(4)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=274. Generated=130381. Kept=17668. proofs=1. Usable=62. Sos=2967. Demods=3157. Limbo=350, Disabled=14292. Hints=0. Weight_deleted=605. Literals_deleted=0. Forward_subsumed=110211. Back_subsumed=821. Sos_limit_deleted=1896. Sos_displaced=0. Sos_removed=0. New_demodulators=17198 (2 lex), Back_demodulated=13468. Back_unit_deleted=0. Demod_attempts=2378913. Demod_rewrites=361556. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=4. Megabytes=10.16. User_CPU=8.36, System_CPU=0.05, Wall_clock=8. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11621 exit (max_proofs) Sat Aug 12 21:15:02 2006