============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11887 was started by mccune on cleo, Wed Feb 25 09:48:31 2009 The command was "/home/mccune/bin/prover9 -f sh1-def.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file sh1-def.in assign(max_seconds,60). 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). x' = f(x,x). end_of_list. formulas(goals). f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer"). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer") # label(non_clause) # label(goal). [goal]. ============================== 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]. x' = f(x,x). [assumption]. f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, f, ' ]). After inverse_order: (no changes). Folding symbols: '/1. After fold_eq: Function symbol precedence: function_order([ c1, c2, c3, ', f ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 2 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. 3 x' = f(x,x). [assumption]. kept: 4 f(x,x) = x'. [copy(3),flip(a)]. 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. kept: 6 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(5),rewrite([4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34)])]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 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)]. 6 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(5),rewrite([4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34)])]. end_of_list. formulas(demodulators). 2 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.01 seconds. given #1 (I,wt=15): 2 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): 6 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(5),rewrite([4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34)])]. given #4 (A,wt=37): 7 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(2(a,1),2(a,1,1,2,1))]. given #5 (T,wt=9): 13 f(x,f(x',x))' = x. [para(4(a,1),2(a,1)),rewrite([4(1)])]. given #6 (T,wt=14): 10 f(f(x,f(x',x)),f(x,f(y,x))) = x. [para(4(a,1),2(a,1,1,2,1))]. given #7 (T,wt=13): 27 f(f(x,f(x',x)),f(x,x')) = x. [para(4(a,1),10(a,1,2,2))]. given #8 (T,wt=14): 11 f(f(x,f(f(y,x),x)),f(y,x')) = y. [para(4(a,1),2(a,1,2,2))]. given #9 (A,wt=25): 8 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(2(a,1),2(a,1,2,2))]. given #10 (T,wt=15): 40 f(f(x,f(f(x',x),x)),x'') = x'. [para(4(a,1),11(a,1,2))]. given #11 (T,wt=18): 12 f(f(x,f(f(f(y,x),x),x)),f(y,x)') = f(y,x). [para(4(a,1),2(a,1,2))]. given #12 (T,wt=18): 60 f(f(x,f(f(y,x),x)),f(y,f(x,f(x',x)))) = y. [para(10(a,1),8(a,1,1,1)),rewrite([10(6),10(7)])]. given #13 (T,wt=5): 110 x'' = x. [back_rewrite(13),rewrite([87(3)])]. given #14 (A,wt=29): 9 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(2(a,1),2(a,1,2))]. given #15 (F,wt=25): 120 f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(6),rewrite([110(3)]),xx(a)]. given #16 (T,wt=9): 87 f(x,f(x',x)) = x'. [para(60(a,1),7(a,1,2)),rewrite([85(8),4(1),4(2)]),flip(a)]. given #17 (T,wt=9): 95 f(x',f(x,x')) = x. [back_rewrite(85),rewrite([87(3),87(4)])]. given #18 (T,wt=10): 111 f(x',f(x,f(y,x))) = x. [back_rewrite(10),rewrite([87(3)])]. given #19 (T,wt=12): 135 f(x,f(x',f(y,x'))) = x'. [para(87(a,1),7(a,1,1,1)),rewrite([87(4),95(4),4(1),87(3),87(4),4(6),87(8)])]. given #20 (A,wt=85): 14 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(w,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(7(a,1),2(a,1,1,2,1))]. given #21 (T,wt=13): 92 f(f(x,f(f(x',x),x)),x) = x'. [para(10(a,1),60(a,1,2)),rewrite([87(3),87(8)])]. given #22 (T,wt=14): 100 f(f(x,y)',f(f(x,y),x)) = f(x,y). [back_rewrite(59),rewrite([87(6)])]. given #23 (T,wt=14): 142 f(x',f(x,f(y,f(f(x,y),y)))) = x. [para(9(a,1),111(a,1,2,2))]. given #24 (T,wt=15): 113 f(f(x',f(f(x,x'),x')),x') = x. [back_rewrite(88),rewrite([95(5),95(12)])]. given #25 (A,wt=59): 15 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(7(a,1),2(a,1,2))]. given #26 (T,wt=16): 112 f(f(x',f(f(y,x'),x')),f(y,x)) = y. [back_rewrite(89),rewrite([95(10)])]. given #27 (T,wt=16): 151 f(x,f(x',f(y,f(f(x',y),y)))) = x'. [para(9(a,1),135(a,1,2,2))]. given #28 (T,wt=18): 233 f(f(f(x,y),f(f(x,f(x,y)),f(x,y))),x') = x. [para(112(a,1),12(a,1,1,2,1,1)),rewrite([112(14),112(16)])]. given #29 (T,wt=19): 49 f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. [para(8(a,1),2(a,1,2,2))]. given #30 (A,wt=55): 17 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(2(a,1),7(a,1,1,1)),rewrite([2(9),2(20)])]. given #31 (T,wt=19): 51 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(2(a,1),8(a,1,1,1)),rewrite([2(6),2(7)])]. given #32 (T,wt=12): 312 f(f(x,f(f(y,x),x)),y') = y. [para(7(a,1),51(a,1,2)),rewrite([4(1),87(3),4(2),87(4),95(4),4(4),87(6),4(6),87(8),4(7),87(9),95(9)])]. given #33 (T,wt=13): 311 f(f(x,f(f(y',x),x)),y) = y'. [para(2(a,1),51(a,1,2)),rewrite([4(1),87(3),4(6),87(8)])]. given #34 (T,wt=14): 411 f(x,f(x',f(x,f(y,x))')) = x'. [back_rewrite(91),rewrite([400(6)])]. given #35 (A,wt=31): 18 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(2(a,1),7(a,1,2,2))]. given #36 (T,wt=12): 441 f(x',f(x,f(x',x)')) = x. [para(312(a,1),411(a,1,2,2,1,2)),rewrite([110(3),110(8)])]. given #37 (T,wt=13): 425 f(x,f(x',f(x,x')')) = x'. [para(4(a,1),411(a,1,2,2,1,2))]. given #38 (T,wt=14): 417 f(x,f(f(f(y,x)',x),x)) = f(y,x). [para(311(a,1),9(a,1,1,2,1)),rewrite([87(6),4(5),110(3)]),flip(a)]. given #39 (T,wt=8): 491 f(x',f(y,x)) = x. [para(417(a,1),2(a,1,2)),rewrite([4(1),87(3)])]. % Operation f is commutative; C redundancy checks enabled. given #40 (A,wt=9): 498 f(x,f(y,x')) = x'. [para(417(a,1),7(a,1,2)),rewrite([4(1),87(3),4(2),87(4),95(4),4(1),87(3),4(4),87(6)])]. given #41 (F,wt=25): 813 f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(120),rewrite([783(13),783(17)])]. given #42 (T,wt=7): 783 f(x,y) = f(y,x). [back_rewrite(39),rewrite([662(4),766(4,R),491(4),679(4),662(4)])]. given #43 (T,wt=8): 679 f(x',f(x,y)) = x. [back_rewrite(603),rewrite([662(4)])]. given #44 (T,wt=9): 645 f(x,f(x',y)) = x'. [back_rewrite(616),rewrite([624(4)])]. given #45 (T,wt=10): 721 f(x,f(x,y)') = f(x,y). [back_rewrite(381),rewrite([662(3),662(6)])]. given #46 (A,wt=11): 624 f(f(x,y),f(y,f(x,y))) = y. [para(491(a,1),417(a,1,2,1,1,1)),rewrite([491(4),491(7)])]. given #47 (T,wt=10): 812 f(x,f(y,x)') = f(y,x). [back_rewrite(626),rewrite([783(3)])]. given #48 (T,wt=10): 814 f(f(x,y),f(x,y')) = x. [back_rewrite(778),rewrite([805(6),783(4)])]. given #49 (T,wt=10): 842 f(f(x,y),f(y,x')) = y. [para(783(a,1),814(a,1,1))]. given #50 (T,wt=10): 843 f(f(x,y),f(y',x)) = x. [para(783(a,1),814(a,1,2))]. given #51 (A,wt=16): 700 f(x',f(f(x',y),f(x,z))) = f(x',y). [back_rewrite(421),rewrite([662(5),662(6),662(10)])]. given #52 (T,wt=10): 844 f(f(x',y),f(y,x)) = y. [para(110(a,1),842(a,1,2,2))]. given #53 (T,wt=10): 845 f(f(x,y'),f(y,x)) = x. [para(842(a,1),783(a,1)),flip(a)]. given #54 (T,wt=10): 846 f(f(x,y),f(x',y)) = y. [para(783(a,1),842(a,1,2))]. given #55 (T,wt=11): 709 f(f(x,y),f(y,f(z,x))) = y. [back_rewrite(397),rewrite([662(3),662(5),654(5),679(5),662(8),654(8),679(8)])]. given #56 (A,wt=21): 704 f(f(x',y),f(x',f(z,f(f(x',y),f(u,x))))) = x'. [back_rewrite(415),rewrite([662(4),662(8),662(10),694(12),662(7)])]. given #57 (T,wt=11): 747 f(f(x,y),f(x,f(y,z))) = x. [back_rewrite(278),rewrite([694(6),694(6),694(7),662(3),662(4),662(9),662(10),694(14)])]. given #58 (T,wt=11): 802 f(f(x,y),f(x,f(z,y))) = x. [back_rewrite(674),rewrite([694(6),783(4),694(10)])]. given #59 (T,wt=11): 805 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(652),rewrite([783(2),783(6),694(10),783(2)])]. given #60 (T,wt=11): 826 f(x,f(x,f(x,y))) = f(x,y). [back_rewrite(727),rewrite([783(2),783(3)])]. given #61 (A,wt=16): 707 f(x',f(f(x',y),f(z,x))) = f(x',y). [back_rewrite(412),rewrite([662(5),662(10)])]. given #62 (T,wt=11): 861 f(f(f(x,y),z),f(z,y)) = z. [para(491(a,1),709(a,1,2,2))]. given #63 (T,wt=11): 863 f(f(x,f(y,z)),f(z,x)) = x. [para(709(a,1),783(a,1)),flip(a)]. given #64 (T,wt=11): 864 f(f(x,y),f(y,f(x,z))) = y. [para(783(a,1),709(a,1,2,2))]. given #65 (T,wt=11): 865 f(f(x,y),f(f(z,x),y)) = y. [para(783(a,1),709(a,1,2))]. given #66 (A,wt=23): 708 f(f(x,y),f(f(f(x,y),f(z,y)),f(u,x))) = f(f(x,y),f(z,y)). [back_rewrite(398),rewrite([662(3),662(5),662(8),662(11),662(14)])]. given #67 (T,wt=11): 866 f(f(f(x,y),z),f(z,x)) = z. [para(679(a,1),709(a,1,2,2))]. given #68 (T,wt=11): 894 f(f(x,y),f(f(y,z),x)) = x. [para(783(a,1),747(a,1,2))]. given #69 (T,wt=11): 906 f(f(x,y),f(f(z,y),x)) = x. [para(783(a,1),802(a,1,2))]. given #70 (T,wt=11): 932 f(f(x,f(y,z)),f(y,x)) = x. [para(783(a,1),863(a,1,1,2))]. given #71 (A,wt=19): 711 f(f(f(x,y),f(z,x)),f(f(x,y),f(u,y))) = f(x,y). [back_rewrite(395),rewrite([662(4),662(7),662(7),662(10),662(10)])]. given #72 (T,wt=11): 936 f(f(x,y),f(f(x,z),y)) = y. [para(783(a,1),864(a,1,2))]. given #73 (T,wt=13): 797 f(x,f(f(x,y),f(z,y))) = f(x,y). [back_rewrite(681),rewrite([694(6)])]. given #74 (T,wt=13): 818 f(x,f(f(x,y),f(y,z))) = f(x,y). [back_rewrite(772),rewrite([783(4)])]. given #75 (T,wt=13): 830 f(x,f(f(y,x),f(z,y))) = f(y,x). [back_rewrite(713),rewrite([783(4)])]. given #76 (A,wt=23): 717 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)). [back_rewrite(388),rewrite([662(3),662(4),662(5),662(6),662(8),662(8),662(10),662(11),662(12),662(14),662(14)])]. given #77 (T,wt=13): 878 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(709(a,1),709(a,1,2)),rewrite([783(4)])]. given #78 (T,wt=13): 903 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(747(a,1),709(a,1,2)),rewrite([783(4)])]. given #79 (T,wt=13): 911 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(802(a,1),709(a,1,2)),rewrite([783(4)])]. given #80 (T,wt=13): 944 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(864(a,1),709(a,1,2)),rewrite([783(4)])]. given #81 (A,wt=23): 718 f(f(x,y),f(f(f(x,y),f(z,y)),f(x,u))) = f(f(x,y),f(z,y)). [back_rewrite(387),rewrite([662(3),662(5),662(8),662(7),662(11),662(14)])]. given #82 (T,wt=13): 948 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(864(a,1),802(a,1,2)),rewrite([783(4)])]. given #83 (T,wt=14): 723 f(x,f(f(x,y),f(x',z))) = f(x,y). [back_rewrite(378),rewrite([662(3),662(5),662(8)])]. given #84 (T,wt=14): 730 f(x,f(f(x,y),f(z,x'))) = f(x,y). [back_rewrite(356),rewrite([662(3),662(8)])]. given #85 (T,wt=14): 817 f(f(x,y),f(x,f(z,f(x,y')))) = x. [back_rewrite(773),rewrite([783(6)])]. given #86 (A,wt=19): 719 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y). [back_rewrite(384),rewrite([662(4),662(7),662(6),662(7),662(8),662(10),662(10),662(10)])]. given #87 (T,wt=12): 1540 f(f(x,y),f(y,x)) = f(x,y)'. [para(719(a,1),797(a,1,2)),rewrite([4(3)]),flip(a)]. given #88 (T,wt=13): 1558 f(f(x,y)',f(y,x)') = f(x,y). [para(1540(a,1),491(a,1,2))]. given #89 (T,wt=14): 821 f(f(x,y'),f(x,f(z,f(x,y)))) = x. [back_rewrite(762),rewrite([783(6)])]. given #90 (T,wt=14): 860 f(x,f(f(y,x),f(z,x'))) = f(y,x). [para(491(a,1),709(a,1,1))]. given #91 (A,wt=18): 729 f(f(x,y),f(x,f(z,f(f(x,y),f(u,x'))))) = x. [back_rewrite(358),rewrite([662(3),662(7),662(8),694(11),662(4)])]. given #92 (T,wt=14): 895 f(f(x,y),f(x,f(f(x,y)',z))) = x. [para(721(a,1),747(a,1,1))]. given #93 (T,wt=14): 896 f(f(x,y),f(y,f(f(x,y)',z))) = y. [para(812(a,1),747(a,1,1))]. given #94 (T,wt=14): 907 f(f(x,y),f(x,f(z,f(x,y)'))) = x. [para(721(a,1),802(a,1,1))]. given #95 (T,wt=14): 908 f(f(x,y),f(y,f(z,f(x,y)'))) = y. [para(812(a,1),802(a,1,1))]. given #96 (A,wt=17): 731 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [back_rewrite(353),rewrite([662(3),662(5),694(6),662(3),662(4),662(6),662(9)])]. given #97 (T,wt=14): 935 f(x,f(f(y,x),f(x',z))) = f(y,x). [para(491(a,1),864(a,1,1))]. given #98 (T,wt=14): 954 f(x,f(f(y,x'),f(z,x))) = f(z,x). [para(491(a,1),865(a,1,1))]. given #99 (T,wt=14): 956 f(x,f(f(y,x'),f(x,z))) = f(x,z). [para(679(a,1),865(a,1,1))]. given #100 (T,wt=12): 1925 f(x,f(f(x,x')',y)) = x'. [para(895(a,1),956(a,1,2)),rewrite([4(1)]),flip(a)]. given #101 (A,wt=19): 733 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [back_rewrite(349),rewrite([694(4),662(6),662(6),662(12)])]. given #102 (T,wt=10): 1958 f(x,f(y,f(x,y))) = x'. [para(863(a,1),733(a,1,2)),rewrite([4(1)]),flip(a)]. given #103 (T,wt=10): 2014 f(x,f(y,f(y,x))) = x'. [para(783(a,1),1958(a,1,2,2))]. given #104 (T,wt=12): 1926 f(x,f(y,f(x,x')')) = x'. [para(907(a,1),956(a,1,2)),rewrite([4(1)]),flip(a)]. NOTE: New constant: f(x,x') = c_0. [new_symbol(2182)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, ', f ]). given #105 (T,wt=6): 2184 f(x,x') = c_0. [new_symbol(2182)]. given #106 (A,wt=17): 736 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [back_rewrite(340),rewrite([694(4),662(6),662(6),662(12)])]. given #107 (F,wt=16): 2183 f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(813),rewrite([2180(6)]),xx(a)]. given #108 (T,wt=6): 2185 f(x,c_0) = x'. [back_rewrite(2180),rewrite([2184(2)])]. given #109 (T,wt=6): 2190 f(x,c_0') = c_0. [back_rewrite(2172),rewrite([2184(2),2184(5)])]. given #110 (T,wt=6): 2193 f(c_0',x) = c_0. [back_rewrite(1930),rewrite([2184(2),2184(5)])]. given #111 (T,wt=6): 2197 f(c_0,x) = x'. [para(2184(a,1),842(a,1,1)),rewrite([4(4),110(3)])]. given #112 (A,wt=16): 740 f(x,f(f(x,y),f(f(x,y'),z))) = f(x,y). [back_rewrite(314),rewrite([694(6),662(3),662(6),662(9)])]. given #113 (T,wt=9): 2186 f(x',f(x,y)') = c_0. [back_rewrite(2177),rewrite([2184(6)])]. given #114 (T,wt=9): 2189 f(x',f(y,x)') = c_0. [back_rewrite(2174),rewrite([2184(6)])]. given #115 (T,wt=9): 2192 f(x,f(y,x')') = c_0. [back_rewrite(2092),rewrite([2184(6)])]. given #116 (T,wt=9): 2201 f(x,f(x',y)') = c_0. [para(2184(a,1),818(a,1,2,1)),rewrite([2197(4),2184(6)])]. given #117 (A,wt=16): 741 f(x,f(f(x,y),f(x,f(y,z))')) = f(x,y). [back_rewrite(313),rewrite([662(3),662(5),694(6),662(3),662(4),662(9)])]. given #118 (T,wt=10): 2393 f(f(x,y)',f(y,x)) = c_0. [para(1540(a,1),2189(a,1,2,1)),rewrite([110(5)])]. given #119 (T,wt=10): 2394 f(f(x,y),f(y,x)') = c_0. [para(1558(a,1),2189(a,1,2,1)),rewrite([110(3)])]. given #120 (T,wt=10): 2397 f(x,f(y,f(x,y))') = c_0. [para(1958(a,1),2189(a,1,2,1)),rewrite([110(5),783(4)])]. given #121 (T,wt=10): 2398 f(x,f(y,f(y,x))') = c_0. [para(2014(a,1),2189(a,1,2,1)),rewrite([110(5),783(4)])]. given #122 (A,wt=24): 743 f(x,f(f(x,f(y,f(x,z))),f(u,f(x,z')))) = f(x,f(y,f(x,z))). [back_rewrite(306),rewrite([662(6),694(6),662(8),694(6),694(6),662(9),662(9),694(14),662(17)])]. given #123 (T,wt=11): 2206 f(x',f(y,f(z,x)')) = x. [back_rewrite(2195),rewrite([2197(4)])]. given #124 (T,wt=10): 2796 f(x,f(x,y)) = f(x,y'). [para(2206(a,1),741(a,1,2,2,1,2)),rewrite([783(5),2761(5)])]. given #125 (T,wt=10): 2800 f(x,f(y,x)) = f(x,y'). [back_rewrite(857),rewrite([2765(5)])]. given #126 (T,wt=11): 2763 f(x',f(y,f(x,z)')) = x. [para(783(a,1),2206(a,1,2,2,1))]. given #127 (A,wt=15): 754 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [back_rewrite(245),rewrite([694(6),662(9),662(9),694(10)])]. given #128 (T,wt=11): 2764 f(x',f(f(y,x)',z)) = x. [para(783(a,1),2206(a,1,2))]. given #129 (T,wt=11): 3138 f(x',f(f(x,y)',z)) = x. [para(783(a,1),2763(a,1,2))]. given #130 (T,wt=12): 2200 f(f(x,y)',f(z,y')') = c_0. [para(2184(a,1),711(a,1,1,1)),rewrite([2197(3),2184(4),2197(6),2184(8)])]. given #131 (T,wt=12): 2204 f(f(x,y)',f(y',z)') = c_0. [para(2184(a,1),719(a,1,1,1)),rewrite([2197(3),2184(4),2197(6),2184(8)])]. given #132 (A,wt=23): 755 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(w,f(x,y)))))) = x. [back_rewrite(241),rewrite([662(6),662(11),662(13),694(14),694(6),662(8),694(14)])]. given #133 (T,wt=12): 2207 f(x,f(y,f(z,x')')) = x'. [back_rewrite(2194),rewrite([2197(4)])]. given #134 (T,wt=12): 2372 f(x',f(y,f(x,z)')') = c_0. [para(2186(a,1),797(a,1,2,1)),rewrite([2197(6),2186(10)])]. given #135 (T,wt=12): 2373 f(x',f(f(x,y)',z)') = c_0. [para(2186(a,1),818(a,1,2,1)),rewrite([2197(6),2186(10)])]. given #136 (T,wt=12): 2374 f(f(x,y)',f(z,x')') = c_0. [para(2186(a,1),830(a,1,2,1)),rewrite([2197(6),2186(10)])]. given #137 (A,wt=21): 765 f(f(x,y'),f(x,f(z,f(f(x,y'),f(u,f(x,y)))))) = x. [back_rewrite(199),rewrite([662(6),662(11),662(13),694(14),694(6),662(8),694(14)])]. given #138 (T,wt=12): 2376 f(f(x,y)',f(x',z)') = c_0. [para(2186(a,1),944(a,1,2,2)),rewrite([783(6),2197(6),2186(10)])]. given #139 (T,wt=12): 2388 f(x',f(y,f(z,x)')') = c_0. [para(2189(a,1),797(a,1,2,1)),rewrite([2197(6),2189(10)])]. given #140 (T,wt=12): 2389 f(x',f(f(y,x)',z)') = c_0. [para(2189(a,1),818(a,1,2,1)),rewrite([2197(6),2189(10)])]. given #141 (T,wt=12): 2406 f(x,f(y,f(z,x')')') = c_0. [para(2192(a,1),797(a,1,2,1)),rewrite([2197(6),2192(10)])]. given #142 (A,wt=21): 769 f(f(x,y),f(x,f(f(f(x,y),f(z,f(x,f(u,y)))),w))) = x. [back_rewrite(155),rewrite([662(3),662(8),662(9),694(13),694(7),662(4),662(9),694(15)])]. given #143 (T,wt=12): 2407 f(x,f(f(y,x')',z)') = c_0. [para(2192(a,1),818(a,1,2,1)),rewrite([2197(6),2192(10)])]. given #144 (T,wt=12): 2408 f(f(x,y')',f(z,y)') = c_0. [para(2192(a,1),830(a,1,2,1)),rewrite([2197(6),2192(10)])]. given #145 (T,wt=12): 2410 f(f(x,y')',f(y,z)') = c_0. [para(2192(a,1),944(a,1,2,2)),rewrite([783(6),2197(6),2192(10)])]. given #146 (T,wt=12): 2424 f(x,f(y,f(x',z)')') = c_0. [para(2201(a,1),797(a,1,2,1)),rewrite([2197(6),2201(10)])]. given #147 (A,wt=21): 770 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(u,y)),w))))) = x. [back_rewrite(154),rewrite([662(3),662(6),662(8),662(9),662(12),694(13),694(7),662(4),662(7),694(15)])]. given #148 (T,wt=12): 2425 f(x,f(f(x',y)',z)') = c_0. [para(2201(a,1),818(a,1,2,1)),rewrite([2197(6),2201(10)])]. given #149 (T,wt=12): 2426 f(f(x',y)',f(z,x)') = c_0. [para(2201(a,1),830(a,1,2,1)),rewrite([2197(6),2201(10)])]. given #150 (T,wt=12): 2428 f(f(x',y)',f(x,z)') = c_0. [para(2201(a,1),944(a,1,2,2)),rewrite([783(6),2197(6),2201(10)])]. given #151 (T,wt=12): 3136 f(x,f(y,f(x',z)')) = x'. [para(110(a,1),2763(a,1,1))]. given #152 (A,wt=17): 775 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [back_rewrite(123),rewrite([694(6),662(3),662(6),662(9)])]. given #153 (T,wt=12): 3251 f(x,f(f(y,x')',z)) = x'. [para(110(a,1),2764(a,1,1))]. given #154 (T,wt=12): 3290 f(x,f(f(x',y)',z)) = x'. [para(110(a,1),3138(a,1,1))]. given #155 (T,wt=13): 2521 f(f(x,y)',f(z,f(y,x))') = c_0. [para(2393(a,1),797(a,1,2,1)),rewrite([2197(6),2393(10)])]. given #156 (T,wt=13): 2522 f(f(x,y)',f(f(y,x),z)') = c_0. [para(2393(a,1),818(a,1,2,1)),rewrite([2197(6),2393(10)])]. given #157 (A,wt=17): 776 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [back_rewrite(122),rewrite([662(3),662(5),694(6),662(3),662(4),662(9)])]. given #158 (T,wt=13): 2523 f(f(x,y),f(z,f(y,x)')') = c_0. [para(2393(a,1),830(a,1,2,1)),rewrite([2197(6),2393(10)])]. given #159 (T,wt=13): 2525 f(f(x,y),f(f(y,x)',z)') = c_0. [para(2393(a,1),944(a,1,2,2)),rewrite([783(6),2197(6),2393(10)])]. given #160 (T,wt=13): 2761 f(f(x,y)',f(z,y')) = f(x,y). [para(491(a,1),2206(a,1,2,2,1))]. given #161 (T,wt=13): 2765 f(f(x,y)',f(z,x')) = f(x,y). [para(679(a,1),2206(a,1,2,2,1))]. given #162 (A,wt=19): 779 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [back_rewrite(55),rewrite([694(4),662(6),662(12)])]. given #163 (T,wt=13): 2826 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(2618),rewrite([2796(4),783(6)])]. given #164 (T,wt=13): 2827 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(2616),rewrite([2796(4),783(6)])]. given #165 (T,wt=13): 3040 f(f(x',y),f(x,z)') = f(x,z). [para(700(a,1),2800(a,1,2)),rewrite([783(7),2796(7),110(11),783(10),1075(10)])]. given #166 (T,wt=13): 3049 f(f(x',y),f(z,x)') = f(z,x). [para(707(a,1),2800(a,1,2)),rewrite([783(7),2796(7),110(11),783(10),1073(10)])]. given #167 (A,wt=20): 781 f(f(x,y),f(x,f(f(x,y),f(z,f(x,f(u,y))))')) = x. [back_rewrite(44),rewrite([662(3),662(8),662(9),694(13),694(7),662(4),694(15)])]. given #168 (T,wt=13): 3252 f(f(x,y)',f(y',z)) = f(x,y). [para(491(a,1),2764(a,1,2,1,1))]. given #169 (T,wt=13): 3254 f(f(x,y)',f(x',z)) = f(x,y). [para(679(a,1),2764(a,1,2,1,1))]. given #170 (T,wt=13): 3328 f(f(x,f(y,z))',f(z,y)') = c_0. [para(1558(a,1),2200(a,1,2,1))]. given #171 (T,wt=13): 3817 f(f(x,f(y,z)')',f(z,y)) = c_0. [para(1540(a,1),2408(a,1,2,1)),rewrite([110(7)])]. given #172 (A,wt=20): 782 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,y')))))) = x. [back_rewrite(43),rewrite([662(3),662(8),662(9),694(13),694(7),662(4),694(15)])]. given #173 (T,wt=13): 4361 f(f(x,y'),f(z,y)') = f(z,y). [para(2761(a,1),783(a,1)),flip(a)]. given #174 (T,wt=13): 4406 f(f(x,y'),f(y,z)') = f(y,z). [para(2765(a,1),783(a,1)),flip(a)]. given #175 (T,wt=13): 4525 f(f(x,y)',f(x,f(z,y'))) = c_0. [para(110(a,1),2826(a,1,1,1,2))]. given #176 (T,wt=13): 4526 f(f(x',y)',f(y,f(z,x))) = c_0. [para(783(a,1),2826(a,1,1,1))]. given #177 (A,wt=19): 796 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [back_rewrite(682),rewrite([694(4)])]. given #178 (T,wt=12): 5070 f(x',f(f(y,x),f(z,x))) = c_0. [para(491(a,1),4526(a,1,1,1))]. given #179 (T,wt=12): 5074 f(x',f(f(x,y),f(z,x))) = c_0. [para(679(a,1),4526(a,1,1,1))]. given #180 (T,wt=12): 5291 f(x',f(f(y,x),f(x,z))) = c_0. [para(783(a,1),5070(a,1,2,2))]. given #181 (T,wt=12): 5340 f(x',f(f(x,y),f(x,z))) = c_0. [para(783(a,1),5074(a,1,2,2))]. given #182 (A,wt=23): 798 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(w,f(x,z)))))) = x. [back_rewrite(678),rewrite([694(14),694(6),694(14)])]. given #183 (T,wt=13): 4527 f(f(x,y')',f(f(z,y),x)) = c_0. [para(783(a,1),2826(a,1,2))]. given #184 (T,wt=13): 4534 f(x,f(y',f(f(z,y),x))') = c_0. [para(861(a,1),2826(a,1,2)),rewrite([783(4),783(6)])]. given #185 (T,wt=13): 4539 f(x,f(y',f(f(y,z),x))') = c_0. [para(866(a,1),2826(a,1,2)),rewrite([783(4),783(6)])]. given #186 (T,wt=13): 4546 f(f(x,f(y,z)')',f(z,x)) = c_0. [para(830(a,1),2826(a,1,2))]. given #187 (A,wt=17): 799 f(f(x,y),f(x,f(z,f(f(x,y),f(u,y))))) = x. [back_rewrite(677),rewrite([694(9),694(7),694(13)])]. given #188 (T,wt=13): 4552 f(f(x,f(y,z)')',f(y,x)) = c_0. [para(948(a,1),2826(a,1,2))]. given #189 (T,wt=13): 4599 f(f(x,y)',f(x,f(y',z))) = c_0. [para(110(a,1),2827(a,1,1,1,2))]. given #190 (T,wt=13): 4600 f(f(x',y)',f(y,f(x,z))) = c_0. [para(783(a,1),2827(a,1,1,1))]. given #191 (T,wt=13): 4601 f(f(x,y')',f(f(y,z),x)) = c_0. [para(783(a,1),2827(a,1,2))]. given #192 (A,wt=15): 800 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [back_rewrite(676),rewrite([694(13),694(7),694(12)])]. given #193 (T,wt=13): 4608 f(x,f(y',f(x,f(z,y)))') = c_0. [para(863(a,1),2827(a,1,2)),rewrite([783(4),783(6)])]. given #194 (T,wt=13): 4612 f(x,f(y',f(x,f(y,z)))') = c_0. [para(932(a,1),2827(a,1,2)),rewrite([783(4),783(6)])]. given #195 (T,wt=13): 4977 f(f(x,y)',f(y,f(z,x'))) = c_0. [para(783(a,1),4525(a,1,1,1))]. given #196 (T,wt=13): 4978 f(f(x,y)',f(f(z,y'),x)) = c_0. [para(783(a,1),4525(a,1,2))]. given #197 (A,wt=15): 801 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [back_rewrite(675),rewrite([694(4),694(10)])]. given #198 (T,wt=13): 4997 f(x,f(y,f(f(z,y'),x))') = c_0. [para(861(a,1),4525(a,1,2)),rewrite([783(4),783(6)])]. given #199 (T,wt=13): 5006 f(x,f(y,f(f(y',z),x))') = c_0. [para(866(a,1),4525(a,1,2)),rewrite([783(4),783(6)])]. given #200 (T,wt=13): 5071 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(491(a,1),4526(a,1,2,2))]. given #201 (T,wt=13): 5073 f(f(x',y)',f(f(z,x),y)) = c_0. [para(783(a,1),4526(a,1,2))]. given #202 (A,wt=22): 808 f(f(x,y),f(x',f(f(x,y),f(z,y)))) = f(f(x,y),f(z,y)). [back_rewrite(756),rewrite([783(5),783(7)])]. given #203 (T,wt=13): 5075 f(f(f(x,y)',z)',f(z,x)) = c_0. [para(679(a,1),4526(a,1,2,2))]. given #204 (T,wt=13): 5082 f(x,f(f(y,z)',f(z,x))') = c_0. [para(709(a,1),4526(a,1,2)),rewrite([783(6)])]. given #205 (T,wt=13): 5084 f(x,f(f(y,z)',f(x,y))') = c_0. [para(747(a,1),4526(a,1,2)),rewrite([783(6)])]. given #206 (T,wt=13): 5086 f(x,f(f(y,z)',f(x,z))') = c_0. [para(802(a,1),4526(a,1,2)),rewrite([783(6)])]. given #207 (A,wt=20): 810 f(f(x,y)',f(y,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(706),rewrite([783(4),783(7)])]. given #208 (T,wt=13): 5090 f(x,f(f(y,z)',f(y,x))') = c_0. [para(864(a,1),4526(a,1,2)),rewrite([783(6)])]. given #209 (T,wt=13): 5290 f(x,f(f(y,x'),f(z,x'))) = c_0. [para(110(a,1),5070(a,1,1))]. given #210 (T,wt=13): 5317 f(x',f(f(y,x),f(z,x))') = x. [para(5070(a,1),2796(a,1,2)),rewrite([783(3),2197(3),110(2)]),flip(a)]. given #211 (T,wt=13): 5339 f(x,f(f(x',y),f(z,x'))) = c_0. [para(110(a,1),5074(a,1,1))]. given #212 (A,wt=20): 811 f(f(x,y)',f(x,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(699),rewrite([783(4),783(7)])]. given #213 (T,wt=13): 5366 f(x',f(f(x,y),f(z,x))') = x. [para(5074(a,1),2796(a,1,2)),rewrite([783(3),2197(3),110(2)]),flip(a)]. given #214 (T,wt=13): 5382 f(x,f(f(y,x'),f(x',z))) = c_0. [para(110(a,1),5291(a,1,1))]. given #215 (T,wt=13): 5407 f(x',f(f(y,x),f(x,z))') = x. [para(5291(a,1),2796(a,1,2)),rewrite([783(3),2197(3),110(2)]),flip(a)]. given #216 (T,wt=13): 5420 f(x,f(f(x',y),f(x',z))) = c_0. [para(110(a,1),5340(a,1,1))]. given #217 (A,wt=27): 815 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(777),rewrite([783(5),783(8)])]. given #218 (T,wt=13): 5445 f(x',f(f(x,y),f(x,z))') = x. [para(5340(a,1),2796(a,1,2)),rewrite([783(3),2197(3),110(2)]),flip(a)]. given #219 (T,wt=13): 5699 f(f(x',y)',f(f(x,z),y)) = c_0. [para(894(a,1),4534(a,1,2,1,2)),rewrite([783(6)])]. given #220 (T,wt=13): 5744 f(x,f(y',f(f(z,y),x))) = x'. [para(4534(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #221 (T,wt=13): 5828 f(x,f(y',f(f(y,z),x))) = x'. [para(4539(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #222 (A,wt=24): 816 f(f(x',y),f(x,f(f(x',y),f(z,y)))) = f(f(x',y),f(z,y)). [back_rewrite(774),rewrite([783(5),783(8)])]. given #223 (T,wt=13): 5849 f(f(x,y)',f(f(y',z),x)) = c_0. [para(645(a,1),4546(a,1,1,1,2,1)),rewrite([110(2)])]. given #224 (T,wt=13): 5944 f(f(x,y)',f(y,f(x',z))) = c_0. [para(3040(a,1),4546(a,1,1,1))]. given #225 (T,wt=13): 6183 f(x,f(y,f(x,f(z,y')))') = c_0. [para(863(a,1),4599(a,1,2)),rewrite([783(4),783(6)])]. given #226 (T,wt=13): 6194 f(x,f(y,f(x,f(y',z)))') = c_0. [para(932(a,1),4599(a,1,2)),rewrite([783(4),783(6)])]. given #227 (A,wt=15): 819 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [back_rewrite(764),rewrite([783(6)])]. given #228 (T,wt=13): 6547 f(x,f(y',f(x,f(z,y)))) = x'. [para(4608(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #229 (T,wt=13): 6609 f(x,f(y',f(x,f(y,z)))) = x'. [para(4612(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #230 (T,wt=13): 6623 f(f(x,y)',f(f(z,x'),y)) = c_0. [para(783(a,1),4977(a,1,2))]. given #231 (T,wt=13): 6949 f(f(x,y)',f(f(x',z),y)) = c_0. [para(894(a,1),4997(a,1,2,1,2)),rewrite([783(6)])]. given #232 (A,wt=15): 820 f(f(x,y),f(x,f(f(x,f(z,y)),u))) = x. [back_rewrite(763),rewrite([783(6)])]. given #233 (T,wt=13): 6987 f(x,f(y,f(f(z,y'),x))) = x'. [para(4997(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #234 (T,wt=13): 7060 f(x,f(y,f(f(y',z),x))) = x'. [para(5006(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #235 (T,wt=13): 7585 f(x,f(f(y,z)',f(z,x))) = x'. [para(5082(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #236 (T,wt=13): 7703 f(x,f(f(y,z)',f(x,y))) = x'. [para(5084(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #237 (A,wt=15): 823 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [back_rewrite(757),rewrite([783(3),783(4)])]. given #238 (T,wt=13): 7799 f(x,f(f(y,z)',f(x,z))) = x'. [para(5086(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #239 (T,wt=13): 7951 f(x,f(f(y,z)',f(y,x))) = x'. [para(5090(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #240 (T,wt=13): 9168 f(x,f(y,f(x,f(z,y')))) = x'. [para(6183(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #241 (T,wt=13): 9218 f(x,f(y,f(x,f(y',z)))) = x'. [para(6194(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. given #242 (A,wt=27): 824 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(739),rewrite([783(5),783(8)])]. given #243 (T,wt=13): 11183 f(x,f(y,f(z,x'))) = f(x,y'). [para(9168(a,1),823(a,1,2)),flip(a)]. given #244 (T,wt=13): 11250 f(x,f(y,f(x',z))) = f(x,y'). [para(9218(a,1),823(a,1,2)),flip(a)]. given #245 (T,wt=13): 11388 f(x,f(f(y,x'),z)) = f(x,z'). [para(783(a,1),11183(a,1,2))]. given #246 (T,wt=13): 11393 f(x,f(f(y,x'),z)') = f(x,z). [para(861(a,1),11183(a,1,2)),flip(a)]. given #247 (A,wt=20): 827 f(f(x,y),f(y,f(f(x,y),z))) = f(y,f(f(x,y),z))'. [back_rewrite(720),rewrite([783(3),783(5),783(8)])]. given #248 (T,wt=13): 11401 f(x,f(f(x',y),z)') = f(x,z). [para(866(a,1),11183(a,1,2)),flip(a)]. given #249 (T,wt=13): 11429 f(x,f(y,f(z,x'))') = f(x,y). [para(11183(a,1),2796(a,1,2)),rewrite([2796(3),110(2)]),flip(a)]. given #250 (T,wt=13): 11534 f(x,f(f(x',y),z)) = f(x,z'). [para(783(a,1),11250(a,1,2))]. given #251 (T,wt=13): 11547 f(x,f(y,f(x',z))') = f(x,y). [para(932(a,1),11250(a,1,2)),flip(a)]. given #252 (A,wt=23): 828 f(f(x,f(y,f(x,z))),f(f(y,f(x,z)),f(u,y))) = f(y,f(x,z)). [back_rewrite(716),rewrite([783(7),783(8)])]. given #253 (T,wt=13): 11798 f(x,f(y,f(z,f(x,y))'))' = x. [para(11388(a,1),765(a,1,2,2)),rewrite([2877(8)])]. given #254 (T,wt=13): 13565 f(x,f(y,f(z,f(x,y))')) = x'. [para(11798(a,1),110(a,1,1)),flip(a)]. given #255 (T,wt=13): 13589 f(x,f(y,f(z,f(x,y))')') = c_0. [para(11798(a,1),2189(a,1,2)),rewrite([783(6)])]. given #256 (T,wt=13): 13625 f(x,f(y,f(z,f(y,x))')) = x'. [para(783(a,1),13565(a,1,2,2,1,2))]. given #257 (A,wt=25): 829 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(714),rewrite([783(5),783(11)])]. given #258 (T,wt=13): 13626 f(x,f(y,f(f(x,y),z)')) = x'. [para(783(a,1),13565(a,1,2,2,1))]. given #259 (T,wt=13): 14806 f(x,f(y,f(z,f(y,x))')') = c_0. [para(783(a,1),13589(a,1,2,1,2,1,2))]. given #260 (T,wt=13): 14807 f(x,f(y,f(f(x,y),z)')') = c_0. [para(783(a,1),13589(a,1,2,1,2,1))]. given #261 (T,wt=13): 14837 f(x,f(y,f(f(y,x),z)')) = x'. [para(783(a,1),13625(a,1,2,2,1))]. given #262 (A,wt=31): 832 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(705),rewrite([783(7),783(16)])]. given #263 (T,wt=13): 15034 f(x,f(y,f(f(y,x),z)')') = c_0. [para(13626(a,1),13589(a,1,2,1,2,1)),rewrite([110(5),783(4)])]. given #264 (T,wt=14): 1096 f(f(x,y),f(x,f(z,f(y',x)))) = x. [para(843(a,1),797(a,1,2,1)),rewrite([843(10)])]. given #265 (T,wt=14): 1099 f(f(x,y'),f(x,f(z,f(y,x)))) = x. [para(845(a,1),797(a,1,2,1)),rewrite([845(10)])]. given #266 (T,wt=14): 1119 f(f(x,y),f(x,f(f(x,y'),z))) = x. [para(814(a,1),818(a,1,2,1)),rewrite([814(10)])]. given #267 (A,wt=15): 834 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [back_rewrite(680),rewrite([783(3),783(4)])]. given #268 (T,wt=13): 15690 f(f(x,y)',z) = f(y,f(x,z)'). [back_rewrite(10785),rewrite([15505(4),15672(9)])]. given #269 (T,wt=13): 16707 f(x,f(y,z)') = f(z,f(x,y)'). [back_rewrite(11065),rewrite([15690(3),15690(7),15690(7),10773(5),15690(6)]),flip(a)]. given #270 (T,wt=13): 16735 f(x,f(y,z)') = f(y,f(x,z)'). [back_rewrite(10942),rewrite([15690(5),15690(6),2796(4),110(3),15905(4),15905(7),110(4),2796(3),110(2),15690(6)])]. ============================== PROOF ================================= % Proof 1 at 9.69 (+ 0.04) seconds: "Sheffer". % Length of proof is 181. % Level of proof is 43. % Maximum clause weight is 87. % Given clauses 270. 1 f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer") # label(non_clause) # label(goal). [goal]. 2 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label(Sh_1). [assumption]. 3 x' = f(x,x). [assumption]. 4 f(x,x) = x'. [copy(3),flip(a)]. 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. 6 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(5),rewrite([4(3),4(5),4(5),4(10),4(14),4(17),4(21),4(34)])]. 7 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(2(a,1),2(a,1,1,2,1))]. 8 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(2(a,1),2(a,1,2,2))]. 9 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(2(a,1),2(a,1,2))]. 10 f(f(x,f(x',x)),f(x,f(y,x))) = x. [para(4(a,1),2(a,1,1,2,1))]. 11 f(f(x,f(f(y,x),x)),f(y,x')) = y. [para(4(a,1),2(a,1,2,2))]. 13 f(x,f(x',x))' = x. [para(4(a,1),2(a,1)),rewrite([4(1)])]. 14 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(w,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(7(a,1),2(a,1,1,2,1))]. 15 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(7(a,1),2(a,1,2))]. 17 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(2(a,1),7(a,1,1,1)),rewrite([2(9),2(20)])]. 18 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(2(a,1),7(a,1,2,2))]. 39 f(f(x',f(f(f(x,f(f(y,x),x)),x'),x')),y) = f(x,f(f(y,x),x)). [para(11(a,1),2(a,1,2))]. 42 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(11(a,1),7(a,1,1,1)),rewrite([11(9),11(20)])]. 49 f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),f(z,x)) = z. [para(8(a,1),2(a,1,2,2))]. 51 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(2(a,1),8(a,1,1,1)),rewrite([2(6),2(7)])]. 59 f(f(f(x,y),f(f(x,y)',f(x,y))),f(f(x,y),x)) = f(x,y). [para(8(a,1),10(a,1,2,2))]. 60 f(f(x,f(f(y,x),x)),f(y,f(x,f(x',x)))) = y. [para(10(a,1),8(a,1,1,1)),rewrite([10(6),10(7)])]. 85 f(f(x,f(x',x)),f(x,f(x,f(x',x)))) = x. [para(4(a,1),60(a,1,1,2,1))]. 87 f(x,f(x',x)) = x'. [para(60(a,1),7(a,1,2)),rewrite([85(8),4(1),4(2)]),flip(a)]. 88 f(f(x',f(f(f(x',f(x,x')),x'),x')),x') = f(x',f(x,x')). [para(7(a,1),60(a,1,2)),rewrite([4(1),87(3),4(2),87(4),4(3),87(5),4(6),87(8),4(8),87(10),4(11),87(13),4(13),87(15),4(14),87(16)])]. 89 f(f(x',f(f(y,x'),x')),f(y,f(x',f(x,x')))) = y. [para(13(a,1),60(a,1,2,2,2,1)),rewrite([87(3),87(4),87(6),87(9),87(10)])]. 95 f(x',f(x,x')) = x. [back_rewrite(85),rewrite([87(3),87(4)])]. 100 f(f(x,y)',f(f(x,y),x)) = f(x,y). [back_rewrite(59),rewrite([87(6)])]. 110 x'' = x. [back_rewrite(13),rewrite([87(3)])]. 112 f(f(x',f(f(y,x'),x')),f(y,x)) = y. [back_rewrite(89),rewrite([95(10)])]. 113 f(f(x',f(f(x,x'),x')),x') = x. [back_rewrite(88),rewrite([95(5),95(12)])]. 120 f(c1,f(c2,c2')) != c1' | f(f(c2',c1),f(c3',c1)) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(6),rewrite([110(3)]),xx(a)]. 197 f(f(x,f(f(f(x',f(f(y,x'),x')),x),x)),y) = f(x',f(f(y,x'),x')). [para(113(a,1),9(a,1,1,1)),rewrite([113(14),113(15)])]. 234 f(f(x,f(f(f(f(x,y),f(f(z,f(x,y)),f(x,y))),x),x)),z) = f(f(x,y),f(f(z,f(x,y)),f(x,y))). [para(112(a,1),9(a,1,1,1)),rewrite([112(14),112(15)])]. 278 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(w,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(f(z,f(f(x,z),z)),f(w,f(x,f(y,z)))))))) = u. [para(14(a,1),49(a,1,1,1)),rewrite([14(41),14(48)])]. 298 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(9(a,1),17(a,1,2,1,1)),rewrite([9(21),9(25),9(33),9(39),9(43)])]. 311 f(f(x,f(f(y',x),x)),y) = y'. [para(2(a,1),51(a,1,2)),rewrite([4(1),87(3),4(6),87(8)])]. 312 f(f(x,f(f(y,x),x)),y') = y. [para(7(a,1),51(a,1,2)),rewrite([4(1),87(3),4(2),87(4),95(4),4(4),87(6),4(6),87(8),4(7),87(9),95(9)])]. 313 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(51(a,1),11(a,1,1,2,1))]. 337 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(51(a,1),15(a,1,1,1,2)),rewrite([51(9),51(12),51(14),51(16),51(35),51(38)])]. 349 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(49(a,1),51(a,1,1,2,1))]. 360 f(x,f(f(y,f(f(x,y),y)),x)) = f(y,f(f(x,y),y)). [para(312(a,1),11(a,1,1,2,1)),rewrite([95(4),110(5)])]. 381 f(x,f(y,f(f(x,y),y))') = f(y,f(f(x,y),y)). [para(312(a,1),312(a,1,1,2,1)),rewrite([95(4)])]. 384 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(337),rewrite([360(6),360(30)])]. 388 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(298),rewrite([360(5)])]. 397 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(42),rewrite([360(5)])]. 413 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(311(a,1),2(a,1,2))]. 415 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(311(a,1),7(a,1,2,1,2,1)),rewrite([87(21),311(33),87(31)])]. 417 f(x,f(f(f(y,x)',x),x)) = f(y,x). [para(311(a,1),9(a,1,1,2,1)),rewrite([87(6),4(5),110(3)]),flip(a)]. 422 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(311(a,1),51(a,1,2))]. 491 f(x',f(y,x)) = x. [para(417(a,1),2(a,1,2)),rewrite([4(1),87(3)])]. 498 f(x,f(y,x')) = x'. [para(417(a,1),7(a,1,2)),rewrite([4(1),87(3),4(2),87(4),95(4),4(1),87(3),4(4),87(6)])]. 505 f(f(x',x),x) = x'. [para(87(a,1),417(a,1,2,1,1,1)),rewrite([110(4),87(5),491(6),87(6)])]. 506 f(f(x,x'),x') = x. [para(95(a,1),417(a,1,2,1,1,1)),rewrite([95(6),498(5),95(8)])]. 511 f(f(x,y)',f(f(x,y),y)) = f(x,y). [para(417(a,1),100(a,1,1,1)),rewrite([417(7),417(10)])]. 521 f(f(x,y),f(f(x',f(x,y)),f(x,y))) = x. [para(112(a,1),417(a,1,2,1,1,1)),rewrite([112(15)])]. 530 f(f(f(f(f(x,y)',y),y),f(f(x,y),f(f(f(x,y)',y),y))),y') = y. [para(417(a,1),312(a,1,1,2,1))]. 531 f(f(f(f(f(x,y')',y'),y'),f(f(x,y'),f(f(f(x,y')',y'),y'))),y) = y'. [para(417(a,1),311(a,1,1,2,1))]. 537 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(417(a,1),18(a,1,2,1,2,1)),rewrite([417(36)])]. 542 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(417(a,1),417(a,1,2,1,1,1)),rewrite([417(22)])]. 599 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(491(a,1),7(a,1,2,2))]. 602 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(491(a,1),9(a,1,1,1)),rewrite([491(9),491(10)])]. 603 f(x',f(y,f(f(x,y),y))) = x. [para(9(a,1),491(a,1,2))]. 610 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(491(a,1),15(a,1,1,1,2,2)),rewrite([491(5),491(6),491(9),491(12),491(23),491(24)])]. 612 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(491(a,1),15(a,1,1,1)),rewrite([491(12),491(14)])]. 622 f(x',x) = f(x,x'). [para(491(a,1),18(a,1,1,1)),rewrite([491(4),87(3),505(4),506(5),505(5)])]. 626 f(f(x,y)',y) = f(x,y). [para(491(a,1),491(a,1,2))]. 651 f(f(f(x,y),y),f(f(x,y),f(f(x,y),y))) = f(x,y). [back_rewrite(542),rewrite([626(3),626(7),511(7),626(6)])]. 652 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(537),rewrite([626(3),626(7),626(13),626(16),651(17),626(16),626(19),651(20)])]. 653 f(f(x,y'),y) = y'. [back_rewrite(531),rewrite([626(5),626(11),651(12)])]. 654 f(f(x,y),y') = y. [back_rewrite(530),rewrite([626(3),626(6),651(7)])]. 662 f(x,f(f(y,x),x)) = f(y,x). [back_rewrite(417),rewrite([626(3)])]. 674 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(612),rewrite([662(12),662(11)])]. 675 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(610),rewrite([662(13),662(13)])]. 679 f(x',f(x,y)) = x. [back_rewrite(603),rewrite([662(4)])]. 680 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). [back_rewrite(602),rewrite([662(6),662(5),662(10)])]. 681 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(599),rewrite([662(9),662(13)])]. 694 f(f(x,y),f(x,f(x,y))) = x. [back_rewrite(521),rewrite([679(4)])]. 699 f(f(f(f(x,y)',z),x),f(x,y)') = f(f(x,y)',z). [back_rewrite(422),rewrite([662(3),662(5),662(6),662(7),662(10),662(12)])]. 704 f(f(x',y),f(x',f(z,f(f(x',y),f(u,x))))) = x'. [back_rewrite(415),rewrite([662(4),662(8),662(10),694(12),662(7)])]. 706 f(f(f(f(x,y)',z),y),f(x,y)') = f(f(x,y)',z). [back_rewrite(413),rewrite([662(5),662(6),662(12)])]. 709 f(f(x,y),f(y,f(z,x))) = y. [back_rewrite(397),rewrite([662(3),662(5),654(5),679(5),662(8),654(8),679(8)])]. 717 f(f(x,y),f(f(f(x,y),f(y,z)),f(u,x))) = f(f(x,y),f(y,z)). [back_rewrite(388),rewrite([662(3),662(4),662(5),662(6),662(8),662(8),662(10),662(11),662(12),662(14),662(14)])]. 719 f(f(f(x,y),f(z,x)),f(f(x,y),f(y,u))) = f(x,y). [back_rewrite(384),rewrite([662(4),662(7),662(6),662(7),662(8),662(10),662(10),662(10)])]. 721 f(x,f(x,y)') = f(x,y). [back_rewrite(381),rewrite([662(3),662(6)])]. 733 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [back_rewrite(349),rewrite([694(4),662(6),662(6),662(12)])]. 741 f(x,f(f(x,y),f(x,f(y,z))')) = f(x,y). [back_rewrite(313),rewrite([662(3),662(5),694(6),662(3),662(4),662(9)])]. 747 f(f(x,y),f(x,f(y,z))) = x. [back_rewrite(278),rewrite([694(6),694(6),694(7),662(3),662(4),662(9),662(10),694(14)])]. 757 f(f(f(x,f(y,z)),y),x) = f(x,f(y,z)). [back_rewrite(234),rewrite([662(6),662(5),662(10)])]. 766 f(x',y) = f(y,x'). [back_rewrite(197),rewrite([662(6),653(3),622(2),498(3),662(8)])]. 778 f(f(x',f(x',f(y,x'))),f(y,x)) = y. [back_rewrite(112),rewrite([766(5,R)])]. 783 f(x,y) = f(y,x). [back_rewrite(39),rewrite([662(4),766(4,R),491(4),679(4),662(4)])]. 797 f(x,f(f(x,y),f(z,y))) = f(x,y). [back_rewrite(681),rewrite([694(6)])]. 801 f(f(x,f(y,f(x,z))),f(x,f(u,z))) = x. [back_rewrite(675),rewrite([694(4),694(10)])]. 802 f(f(x,y),f(x,f(z,y))) = x. [back_rewrite(674),rewrite([694(6),783(4),694(10)])]. 805 f(x,f(x,f(y,x))) = f(y,x). [back_rewrite(652),rewrite([783(2),783(6),694(10),783(2)])]. 810 f(f(x,y)',f(y,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(706),rewrite([783(4),783(7)])]. 811 f(f(x,y)',f(x,f(f(x,y)',z))) = f(f(x,y)',z). [back_rewrite(699),rewrite([783(4),783(7)])]. 812 f(x,f(y,x)') = f(y,x). [back_rewrite(626),rewrite([783(3)])]. 813 f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(120),rewrite([783(13),783(17)])]. 814 f(f(x,y),f(x,y')) = x. [back_rewrite(778),rewrite([805(6),783(4)])]. 823 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [back_rewrite(757),rewrite([783(3),783(4)])]. 834 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [back_rewrite(680),rewrite([783(3),783(4)])]. 842 f(f(x,y),f(y,x')) = y. [para(783(a,1),814(a,1,1))]. 843 f(f(x,y),f(y',x)) = x. [para(783(a,1),814(a,1,2))]. 845 f(f(x,y'),f(y,x)) = x. [para(842(a,1),783(a,1)),flip(a)]. 857 f(x,f(f(y,x)',f(x,y'))) = f(x,y'). [para(845(a,1),843(a,1,1))]. 860 f(x,f(f(y,x),f(z,x'))) = f(y,x). [para(491(a,1),709(a,1,1))]. 861 f(f(f(x,y),z),f(z,y)) = z. [para(491(a,1),709(a,1,2,2))]. 863 f(f(x,f(y,z)),f(z,x)) = x. [para(709(a,1),783(a,1)),flip(a)]. 864 f(f(x,y),f(y,f(x,z))) = y. [para(783(a,1),709(a,1,2,2))]. 865 f(f(x,y),f(f(z,x),y)) = y. [para(783(a,1),709(a,1,2))]. 907 f(f(x,y),f(x,f(z,f(x,y)'))) = x. [para(721(a,1),802(a,1,1))]. 936 f(f(x,y),f(f(x,z),y)) = y. [para(783(a,1),864(a,1,2))]. 944 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(864(a,1),709(a,1,2)),rewrite([783(4)])]. 955 f(x',f(f(y,x),f(z,x'))) = f(z,x'). [para(498(a,1),865(a,1,1))]. 956 f(x,f(f(y,x'),f(x,z))) = f(x,z). [para(679(a,1),865(a,1,1))]. 1196 f(f(x,y),f(x,f(f(x,y),z))) = f(x,f(f(x,y),z))'. [para(747(a,1),717(a,1,2)),rewrite([783(3),783(6),4(7),783(7),783(9)]),flip(a)]. 1540 f(f(x,y),f(y,x)) = f(x,y)'. [para(719(a,1),797(a,1,2)),rewrite([4(3)]),flip(a)]. 1904 f(x',f(y,f(f(x,x'),f(z,x)))) = x. [para(704(a,1),956(a,1,2)),rewrite([4(3),110(2),110(4),783(3)]),flip(a)]. 1926 f(x,f(y,f(x,x')')) = x'. [para(907(a,1),956(a,1,2)),rewrite([4(1)]),flip(a)]. 1958 f(x,f(y,f(x,y))) = x'. [para(863(a,1),733(a,1,2)),rewrite([4(1)]),flip(a)]. 2014 f(x,f(y,f(y,x))) = x'. [para(783(a,1),1958(a,1,2,2))]. 2015 f(x,f(f(x,y),f(x,y)')) = x'. [para(721(a,1),1958(a,1,2,2)),rewrite([783(4)])]. 2016 f(x,f(f(y,x),f(y,x)')) = x'. [para(812(a,1),1958(a,1,2,2)),rewrite([783(4)])]. 2097 f(f(x,y),f(y,y')) = f(x,y)'. [para(491(a,1),2014(a,1,2,2)),rewrite([783(3)])]. 2099 f(f(x,y),f(x,x')) = f(x,y)'. [para(679(a,1),2014(a,1,2,2)),rewrite([783(3)])]. 2170 f(x',f(y,f(x,x')')) = x. [para(110(a,1),1926(a,1,2,2,1,2)),rewrite([783(3),110(8)])]. 2172 f(x,f(y,y')') = f(y,y'). [para(1926(a,1),842(a,1,1)),rewrite([783(7),2170(7),783(2)]),flip(a)]. 2173 f(f(x,y),f(x,y)') = f(y',f(x,y)'). [para(1926(a,1),861(a,1,1)),rewrite([2172(8),783(7),2016(7),783(4),2172(10)]),flip(a)]. 2174 f(x',f(y,x)') = f(x,x'). [para(1926(a,1),865(a,1,1)),rewrite([2172(6),2097(5),2172(8)])]. 2177 f(x',f(x,y)') = f(x,x'). [para(1926(a,1),936(a,1,1)),rewrite([2172(6),2099(5),2172(8)])]. 2178 f(f(x,y)',f(x,f(y,y'))) = f(y,y'). [para(1926(a,1),936(a,1,2)),rewrite([2173(4),2174(4),2172(4),783(6),2173(10),2174(10),2172(10)])]. 2180 f(x,f(y,y')) = x'. [back_rewrite(2015),rewrite([2173(4),2174(4)])]. 2182 f(x,x') = f(y,y'). [back_rewrite(2178),rewrite([2180(5),783(4),2177(4)])]. 2183 f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(813),rewrite([2180(6)]),xx(a)]. 2184 f(x,x') = c_0. [new_symbol(2182)]. 2185 f(x,c_0) = x'. [back_rewrite(2180),rewrite([2184(2)])]. 2189 f(x',f(y,x)') = c_0. [back_rewrite(2174),rewrite([2184(6)])]. 2195 f(x',f(y,f(c_0,f(z,x)))) = x. [back_rewrite(1904),rewrite([2184(3)])]. 2197 f(c_0,x) = x'. [para(2184(a,1),842(a,1,1)),rewrite([4(4),110(3)])]. 2206 f(x',f(y,f(z,x)')) = x. [back_rewrite(2195),rewrite([2197(4)])]. 2393 f(f(x,y)',f(y,x)) = c_0. [para(1540(a,1),2189(a,1,2,1)),rewrite([110(5)])]. 2398 f(x,f(y,f(y,x))') = c_0. [para(2014(a,1),2189(a,1,2,1)),rewrite([110(5),783(4)])]. 2525 f(f(x,y),f(f(y,x)',z)') = c_0. [para(2393(a,1),944(a,1,2,2)),rewrite([783(6),2197(6),2393(10)])]. 2618 f(f(x,f(y,z)),f(x,f(x,z))') = c_0. [para(802(a,1),2398(a,1,2,1,2)),rewrite([783(4)])]. 2761 f(f(x,y)',f(z,y')) = f(x,y). [para(491(a,1),2206(a,1,2,2,1))]. 2765 f(f(x,y)',f(z,x')) = f(x,y). [para(679(a,1),2206(a,1,2,2,1))]. 2796 f(x,f(x,y)) = f(x,y'). [para(2206(a,1),741(a,1,2,2,1,2)),rewrite([783(5),2761(5)])]. 2800 f(x,f(y,x)) = f(x,y'). [back_rewrite(857),rewrite([2765(5)])]. 2826 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(2618),rewrite([2796(4),783(6)])]. 3070 f(f(x,y)',f(f(x,z),y)) = f(y,f(x,z)'). [para(936(a,1),2800(a,1,2)),rewrite([783(3),2800(3),783(8)]),flip(a)]. 3096 f(f(x,y),f(z,y')') = f(z,y'). [para(860(a,1),2800(a,1,2)),rewrite([783(6),2796(6),783(11),955(11)])]. 4354 f(f(x,y)',f(f(y,x)',z)') = f(f(y,x)',z). [para(2525(a,1),2800(a,1,2)),rewrite([783(6),2197(6),110(5),783(10)]),flip(a)]. 4526 f(f(x',y)',f(y,f(z,x))) = c_0. [para(783(a,1),2826(a,1,1,1))]. 5082 f(x,f(f(y,z)',f(z,x))') = c_0. [para(709(a,1),4526(a,1,2)),rewrite([783(6)])]. 5086 f(x,f(f(y,z)',f(x,z))') = c_0. [para(802(a,1),4526(a,1,2)),rewrite([783(6)])]. 5090 f(x,f(f(y,z)',f(y,x))') = c_0. [para(864(a,1),4526(a,1,2)),rewrite([783(6)])]. 6771 f(x,f(f(x,f(y,z))',f(x,f(u,f(x,z))))) = f(x,f(u,f(x,z))). [para(801(a,1),843(a,1,1))]. 7585 f(x,f(f(y,z)',f(z,x))) = x'. [para(5082(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. 7799 f(x,f(f(y,z)',f(x,z))) = x'. [para(5086(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. 7951 f(x,f(f(y,z)',f(y,x))) = x'. [para(5090(a,1),2796(a,1,2)),rewrite([2185(2),110(7)]),flip(a)]. 8163 f(f(x,y)',f(x,f(f(x,y)',z))') = f(f(x,y)',z'). [para(811(a,1),2796(a,1,2)),rewrite([2796(6)]),flip(a)]. 10765 f(f(x,y)',f(z,y)) = f(f(x,y)',z'). [para(7799(a,1),823(a,1,2)),flip(a)]. 10771 f(f(x,y)',f(x,z)') = f(y,f(x,z)'). [back_rewrite(3070),rewrite([10765(5)])]. 10774 f(f(x,y)',z') = f(y,f(x,f(f(x,y)',z))'). [back_rewrite(8163),rewrite([10771(8)]),flip(a)]. 10785 f(x,f(y,f(f(y,x)',f(y,z)))') = f(x,f(y,z)'). [back_rewrite(10771),rewrite([10774(5)])]. 10942 f(x,f(y,f(f(y,x)',f(f(x,y)',z)))') = f(f(x,y)',z). [back_rewrite(4354),rewrite([10774(7)])]. 15501 f(f(x,y)',f(y,z)) = f(y,f(x,f(f(x,y)',z))'). [para(7585(a,1),834(a,1,2)),rewrite([10774(4)]),flip(a)]. 15505 f(f(x,y)',f(x,z)) = f(y,f(x,f(f(x,y)',z))'). [para(7951(a,1),834(a,1,2)),rewrite([10774(4)]),flip(a)]. 15672 f(x,f(y,f(x,f(y,f(f(y,x)',z))'))') = f(f(y,x)',z). [back_rewrite(810),rewrite([15501(7),2796(6),10774(4)])]. 15690 f(f(x,y)',z) = f(y,f(x,z)'). [back_rewrite(10785),rewrite([15505(4),15672(9)])]. 15717 f(x,f(f(y,z),f(x,f(u,f(x,z))')')) = f(x,f(u,f(x,z))). [back_rewrite(6771),rewrite([15690(7),2796(5)])]. 15904 f(x,f(y,f(x,f(y,z)'))') = f(x,f(y,z')'). [back_rewrite(15505),rewrite([15690(4),2796(2),15690(7)]),flip(a)]. 15905 f(x,f(y,f(x,z))') = f(x,f(y,z')'). [back_rewrite(15501),rewrite([15690(4),15690(7),15904(10)])]. 16735 f(x,f(y,z)') = f(y,f(x,z)'). [back_rewrite(10942),rewrite([15690(5),15690(6),2796(4),110(3),15905(4),15905(7),110(4),2796(3),110(2),15690(6)])]. 17169 f(x,f(f(y,z),f(x,f(u,z')')')) = f(x,f(u,f(x,z))). [back_rewrite(15717),rewrite([15905(5)])]. 17895 f(x,f(y,f(x,z)')) = f(x,f(y,z)). [para(16735(a,1),2796(a,1,2)),rewrite([110(7)])]. 17980 f(x,f(y,f(x,z))) = f(x,f(y,z')). [back_rewrite(17169),rewrite([17895(8),3096(5)]),flip(a)]. 19211 f(f(x,y),f(x,z')) = f(x,f(f(x,y),z))'. [back_rewrite(1196),rewrite([17980(5)])]. 19675 $F # answer("Sheffer"). [back_rewrite(2183),rewrite([19211(9),783(7),17980(8),110(5),783(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=270. Generated=126836. Kept=19671. proofs=1. Usable=57. Sos=3106. Demods=3417. Limbo=464, Disabled=16047. Hints=0. Kept_by_rule=0, Deleted_by_rule=605. Forward_subsumed=106559. Back_subsumed=862. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=19213 (2 lex), Back_demodulated=15182. Back_unit_deleted=0. Demod_attempts=2351463. Demod_rewrites=352706. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=5. Nonunit_bsub_feature_tests=3. Megabytes=17.28. User_CPU=9.69, System_CPU=0.04, Wall_clock=10. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11887 exit (max_proofs) Wed Feb 25 09:48:41 2009