============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 6682 was started by mccune on cleo, Tue Nov 3 10:20:37 2009 The command was "/home/mccune/LADR/bin/prover9 -f BA2.in BA2-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA2.in assign(max_seconds,120). set(lex_order_vars). set(restrict_denials). assign(new_constants,1). formulas(sos). f(x,y) = f(y,x) # label(commutativity). f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). 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. % Reading from file BA2-interp.outx list(interpretations). interpretation(6,[number = 1,seconds = 0],[function(f(_,_),[3,3,1,1,1,1,3,4,5,0,1,2,1,5,5,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,1,2,1,1,1,2])]). 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(x,y) = f(y,x) # label(commutativity). [assumption]. f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [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). Unfolding symbols: (none). 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) % Operation f is commutative; C redundancy checks enabled. kept: 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. kept: 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [assumption]. 4 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: 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [copy(4),rewrite([2(25),2(30)]),flip(c)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [copy(4),rewrite([2(25),2(30)]),flip(c)]. end_of_list. formulas(sos). 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. end_of_list. formulas(demodulators). 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. % (lex-dep) 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. given #2 (I,wt=11): 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. given #3 (A,wt=11): 6 f(f(x,y),f(y,f(x,z))) = y # label(false). [para(2(a,1),3(a,1,1))]. given #4 (F,wt=11): 9 f(f(x,y),f(x,f(z,y))) = x # label(false). [para(6(a,1),3(a,1,2,2)),rewrite([2(4)])]. given #5 (F,wt=11): 12 f(f(x,y),f(y,f(z,x))) = y # label(false). [para(6(a,1),6(a,1,2,2)),rewrite([2(2),2(3),2(4)])]. given #6 (T,wt=11): 8 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. given #7 (T,wt=9): 19 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. given #8 (T,wt=11): 10 f(x,f(x,f(y,x))) = f(y,x). [para(6(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. given #9 (T,wt=11): 24 f(x,f(y,f(x,x))) = f(x,x). [para(19(a,1),9(a,1,2)),rewrite([2(2),2(3)])]. given #10 (A,wt=17): 7 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(3(a,1),3(a,1,1)),rewrite([2(4)])]. given #11 (T,wt=9): 27 f(f(x,y),f(y,y)) = y. [para(24(a,1),6(a,1,2))]. given #12 (T,wt=13): 13 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite([2(4)])]. given #13 (T,wt=13): 15 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(6(a,1),9(a,1,2)),rewrite([2(4)])]. given #14 (T,wt=13): 16 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(3(a,1),12(a,1,2)),rewrite([2(2),2(4),2(5)])]. given #15 (A,wt=19): 11 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(3(a,1),6(a,1,1)),rewrite([2(4)])]. given #16 (T,wt=13): 17 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(9(a,1),12(a,1,2)),rewrite([2(2),2(4),2(5)])]. given #17 (T,wt=13): 51 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(2(a,1),16(a,1,2,1)),rewrite([2(2),2(3),2(5)])]. given #18 (T,wt=15): 18 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x. [para(8(a,1),3(a,1,1)),rewrite([2(4)])]. given #19 (T,wt=15): 21 f(x,f(f(x,x),f(y,f(x,z)))) = f(x,x). [para(19(a,1),3(a,1,1)),rewrite([2(3)])]. given #20 (A,wt=19): 14 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(9(a,1),6(a,1,1)),rewrite([2(4)])]. given #21 (T,wt=13): 81 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(11(a,1),21(a,1,2))]. given #22 (T,wt=15): 23 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(19(a,1),6(a,1,1)),rewrite([2(3)])]. given #23 (T,wt=15): 31 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [para(7(a,1),9(a,1,2)),rewrite([2(6)])]. given #24 (T,wt=15): 36 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),13(a,1,2,2)),rewrite([2(3)])]. given #25 (A,wt=19): 26 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(24(a,1),6(a,1,1)),rewrite([2(5)])]. given #26 (F,wt=11): 117 f(x,f(y,f(x,y))) = f(x,x) # label(false). [para(9(a,1),36(a,1,2)),rewrite([2(3)]),flip(a)]. given #27 (F,wt=11): 160 f(x,f(y,y)) = f(x,f(x,y)) # label(false). [para(117(a,1),36(a,1,2)),rewrite([2(3)])]. given #28 (F,wt=11): 173 f(x,f(y,y)) = f(x,f(y,x)) # label(false). [para(160(a,1),2(a,2)),rewrite([2(2),2(3)])]. given #29 (F,wt=11): 176 f(x,f(x,f(y,y))) = f(y,x) # label(false). [para(160(a,1),9(a,1)),rewrite([2(2),173(2,R),2(4),173(4,R),2(6),6(6),2(3)])]. given #30 (T,wt=15): 38 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y. [para(6(a,1),13(a,1,2,1)),rewrite([2(4),6(10)])]. given #31 (T,wt=15): 39 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(6(a,1),13(a,1,2,2)),rewrite([2(3)])]. given #32 (T,wt=15): 46 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x. [para(3(a,1),15(a,1,2,1)),rewrite([2(4),3(10)])]. given #33 (T,wt=15): 48 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x. [para(9(a,1),15(a,1,2,1)),rewrite([2(4),9(10)])]. given #34 (A,wt=21): 28 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(y,w))))))) = x. [para(7(a,1),3(a,1,1)),rewrite([2(7)])]. given #35 (F,wt=11): 179 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(160(a,1),27(a,1,1)),rewrite([19(5),2(3)])]. given #36 (F,wt=15): 164 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [back_rewrite(143),rewrite([160(5),2(6)])]. given #37 (F,wt=15): 191 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x) # label(false). [back_rewrite(161),rewrite([173(6,R),2(4)])]. given #38 (F,wt=15): 194 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x # label(false). [para(173(a,2),9(a,1,2,2))]. given #39 (T,wt=11): 439 f(x,f(y,f(y,y))) = f(x,x). [para(191(a,1),39(a,1)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(496)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, f ]). NOTE: sn=114, num_tables=163 NOTE: updating interpretation 1: c_0=1. given #40 (T,wt=7): 528 f(x,f(x,x)) = c_0. [new_symbol(496)]. given #41 (T,wt=7): 554 f(c_0,f(x,x)) = x. [back_rewrite(490),rewrite([528(3),2(3)])]. given #42 (T,wt=7): 561 f(x,c_0) = f(x,x). [back_rewrite(439),rewrite([528(2)])]. given #43 (A,wt=31): 29 f(f(x,y),f(f(x,z),f(f(x,y),f(u,f(x,f(y,w)))))) = f(f(x,y),f(u,f(x,f(y,w)))). [para(7(a,1),6(a,1,1)),rewrite([2(8)])]. given #44 (F,wt=15): 211 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x # label(false). [para(176(a,2),3(a,1,2,2))]. given #45 (F,wt=15): 212 f(f(x,y),f(y,f(z,f(z,f(x,x))))) = y # label(false). [para(176(a,2),6(a,1,2,2))]. given #46 (F,wt=11): 743 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(3(a,1),212(a,1,2)),rewrite([173(2),2(1),2(3)])]. given #47 (F,wt=15): 214 f(x,f(x,f(y,f(y,f(x,x))))) = f(x,y) # label(false). [para(176(a,2),8(a,1,2,2))]. given #48 (T,wt=9): 615 f(f(x,x),f(c_0,c_0)) = c_0. [para(554(a,1),26(a,1,2,1)),rewrite([173(7),2(5),561(5),528(5),561(5),2(5),173(9),2(7),561(7),528(7)])]. given #49 (T,wt=11): 549 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(498),rewrite([528(3),2(3)])]. given #50 (T,wt=9): 807 f(f(x,y),f(c_0,c_0)) = c_0. [para(81(a,1),549(a,1,2)),rewrite([561(7,R),2(5),528(5),2(6)]),flip(a)]. given #51 (T,wt=11): 558 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(486),rewrite([528(4),2(4),528(7)])]. given #52 (A,wt=21): 30 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,f(x,w))))))) = y. [para(6(a,1),7(a,1,2,1)),rewrite([2(5),6(13)])]. given #53 (F,wt=15): 222 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)) # label(false). [para(176(a,1),11(a,1,2,1,2)),rewrite([14(6)]),flip(a)]. given #54 (F,wt=15): 354 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x # label(false). [para(179(a,1),12(a,1,2,2)),rewrite([2(3)])]. given #55 (F,wt=15): 428 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x) # label(false). [para(19(a,1),191(a,1,2,1)),rewrite([2(2)])]. given #56 (F,wt=15): 564 f(c_0,f(x,f(y,f(y,f(z,f(x,x)))))) = x # label(false). [back_rewrite(377),rewrite([528(2)])]. given #57 (T,wt=11): 608 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(528(a,1),7(a,1,2,1)),rewrite([2(3),24(4),528(7)])]. given #58 (T,wt=11): 617 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(554(a,1),48(a,1,2)),rewrite([2(5),561(5),2(5)])]. given #59 (T,wt=11): 746 f(x,f(c_0,f(y,x))) = f(y,x). [para(212(a,1),19(a,1,2)),rewrite([561(3,R),2(3),2(4)])]. given #60 (T,wt=11): 809 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(549(a,1),176(a,2)),rewrite([2(8),558(8),2(5)])]. given #61 (A,wt=21): 32 f(x,f(f(x,y),f(z,f(x,f(u,f(x,f(x,y))))))) = f(x,y). [para(8(a,1),7(a,1,2,1)),rewrite([2(4),8(11)])]. given #62 (F,wt=15): 591 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [back_rewrite(210),rewrite([173(2),2(1),561(5,R),2(5)])]. given #63 (F,wt=13): 1059 f(f(x,x),f(y,f(y,f(x,z)))) = x # label(false). [para(3(a,1),591(a,1,2,2)),rewrite([2(5),561(5),2(5),3(9)])]. given #64 (F,wt=13): 1061 f(f(x,f(x,f(y,z))),f(z,z)) = z # label(false). [para(6(a,1),591(a,1,2,2)),rewrite([2(5),561(5),6(9)])]. given #65 (F,wt=15): 738 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x) # label(false). [para(211(a,1),191(a,1,2,2,2)),rewrite([561(3,R),2(3),2(5)])]. given #66 (T,wt=11): 947 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(554(a,1),354(a,1,2)),rewrite([2(5)])]. given #67 (T,wt=13): 801 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(7(a,1),549(a,1,2)),rewrite([2(2),561(2),2(3),561(3),561(3,R),2(3),554(3),2(2),561(2)]),flip(a)]. given #68 (T,wt=13): 1003 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(81(a,1),617(a,1,2,2)),rewrite([561(7,R),2(5),554(8),2(6)])]. given #69 (T,wt=13): 1251 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(81(a,1),947(a,1,2,2,2)),rewrite([528(6),2(7)])]. given #70 (A,wt=27): 33 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(w,f(x,f(y,v5))))))))) = f(x,y). [para(7(a,1),7(a,1,2,1)),rewrite([2(7),7(17)])]. given #71 (F,wt=15): 770 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x) # label(false). [para(212(a,1),191(a,1,2,2,2)),rewrite([561(3,R),2(3),2(5)])]. given #72 (F,wt=15): 776 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [para(743(a,1),9(a,1,2,2)),rewrite([173(5),2(4),2(6)])]. given #73 (F,wt=15): 898 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))) # label(false). [para(222(a,1),173(a,1,2)),rewrite([173(2),2(1),8(3),2(2),561(3,R),2(3),173(6),2(5),8(7),2(6)])]. given #74 (F,wt=15): 900 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)) # label(false). [para(222(a,1),176(a,1,2,2)),rewrite([173(2),2(1),8(3),2(2),561(3,R),2(3),173(7),2(6),8(8),2(7)])]. given #75 (T,wt=13): 1274 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(809(a,1),801(a,1,2,2,2))]. given #76 (T,wt=13): 1471 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(898(a,2),1061(a,1,1)),rewrite([2(6)])]. given #77 (T,wt=13): 1475 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(898(a,1),1251(a,1,2,1)),rewrite([2(11),173(11,R),807(11),2(8),809(8)])]. given #78 (T,wt=15): 59 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(11(a,1),9(a,1,2))]. given #79 (A,wt=19): 34 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,y)))))) = y. [para(27(a,1),7(a,1,2,1)),rewrite([2(4),27(11)])]. given #80 (F,wt=15): 959 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x) # label(false). [para(2(a,1),428(a,1,2)),rewrite([173(2),2(1),2(4)])]. given #81 (F,wt=15): 969 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)) # label(false). [para(428(a,1),36(a,1,2)),rewrite([173(2),2(1)]),flip(a)]. given #82 (F,wt=15): 982 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0 # label(false). [para(564(a,1),9(a,1,2)),rewrite([173(3),2(2),2(7)])]. given #83 (F,wt=15): 984 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x) # label(false). [para(564(a,1),27(a,1,1)),rewrite([561(11,R),2(7),564(7)]),flip(a)]. given #84 (T,wt=13): 1630 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(19(a,1),969(a,2,2)),rewrite([561(5,R),2(5),554(5),2(3),2(7),528(7)])]. given #85 (T,wt=15): 174 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x. [para(160(a,1),3(a,1,1)),rewrite([2(4)])]. given #86 (T,wt=15): 239 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(3(a,1),38(a,1,2,2,2,2)),rewrite([2(2),2(3)])]. given #87 (T,wt=15): 240 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x. [para(6(a,1),38(a,1,2,2,2,2)),rewrite([2(2),2(3)])]. given #88 (A,wt=17): 35 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x. [para(13(a,1),3(a,1,1)),rewrite([2(5)])]. given #89 (F,wt=15): 1157 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x) # label(false). [para(19(a,1),1061(a,1,2)),rewrite([173(2),2(1),2(5)])]. given #90 (F,wt=15): 1200 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x) # label(false). [para(6(a,1),738(a,1,2,2,2)),rewrite([2(4),561(4)])]. given #91 (F,wt=15): 1241 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0 # label(false). [para(3(a,1),947(a,1,2,2,2)),rewrite([2(5)])]. given #92 (F,wt=15): 1242 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0 # label(false). [para(9(a,1),947(a,1,2,2,2)),rewrite([2(5)])]. given #93 (T,wt=15): 463 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x. [para(23(a,1),194(a,1,1,2)),rewrite([2(8),26(8)])]. given #94 (T,wt=15): 541 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [back_rewrite(514),rewrite([528(3),528(5),2(5),528(10)])]. given #95 (T,wt=15): 614 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(554(a,1),31(a,1,1)),rewrite([2(4)])]. given #96 (T,wt=15): 818 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(807(a,1),7(a,1,2,1)),rewrite([2(7),173(7),2(5),561(5),528(5),2(5),807(13)])]. given #97 (A,wt=23): 37 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(13(a,1),6(a,1,1)),rewrite([2(6)])]. given #98 (F,wt=15): 1382 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0 # label(false). [para(776(a,1),947(a,1,2,2,2)),rewrite([2(7),8(7)])]. given #99 (F,wt=15): 1537 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x) # label(false). [para(59(a,1),39(a,1,2)),flip(a)]. given #100 (F,wt=15): 1623 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)) # label(false). [para(969(a,1),2(a,2)),rewrite([173(2),2(1),2(4),2(5),173(6,R)])]. given #101 (F,wt=15): 1629 f(x,f(x,f(y,f(z,f(x,x))))) = f(x,y) # label(false). [para(969(a,2),8(a,1,2))]. given #102 (T,wt=15): 877 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [para(222(a,1),19(a,1,1)),rewrite([173(2),2(1),8(3),2(2),561(3,R),2(3),173(5),2(4),8(6),2(5),2(6),173(8),2(7),8(9)])]. given #103 (T,wt=15): 987 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(564(a,1),46(a,1,2)),rewrite([173(4),2(3),2(6),2(8)])]. given #104 (T,wt=15): 1005 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0. [para(191(a,1),617(a,1,2,2)),rewrite([561(9,R),2(6),554(9),2(7)])]. given #105 (T,wt=15): 1007 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0. [para(428(a,1),617(a,1,2,2)),rewrite([561(9,R),2(6),554(9),2(7)])]. given #106 (A,wt=23): 42 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(y,w))))))) = f(x,y). [para(13(a,1),7(a,1,2,1)),rewrite([2(5),13(13)])]. given #107 (F,wt=15): 1765 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0 # label(false). [para(11(a,1),982(a,1,2,2,2))]. given #108 (F,wt=15): 1819 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x) # label(false). [para(59(a,1),984(a,1,2,2)),rewrite([2(1),2(4)])]. given #109 (F,wt=15): 1894 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0 # label(false). [para(239(a,1),982(a,1,2,2,2)),rewrite([2(5)])]. given #110 (F,wt=15): 2207 f(c_0,f(x,f(y,f(c_0,f(z,f(z,x)))))) = x # label(false). [para(614(a,1),12(a,1,2)),rewrite([173(3),2(2),2(6),2(8)])]. given #111 (T,wt=15): 1023 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [para(11(a,1),809(a,1,2)),rewrite([809(5),2(6),561(6),2(7)]),flip(a)]. given #112 (T,wt=15): 1024 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y). [para(14(a,1),809(a,1,2)),rewrite([809(5),2(6),561(6),2(7)]),flip(a)]. given #113 (T,wt=15): 1054 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(32(a,1),617(a,1,2)),rewrite([2(4),561(4),554(4),2(8),561(8),554(8),561(9,R),2(6),2(8),561(8),2(8)])]. given #114 (T,wt=15): 1056 f(f(x,f(y,f(y,z))),f(x,f(z,u))) = x. [para(591(a,1),3(a,1,2,2))]. given #115 (A,wt=23): 43 f(x,f(f(x,y),f(z,f(f(x,y),f(u,f(x,f(y,w))))))) = f(x,y). [para(7(a,1),13(a,1,2,1)),rewrite([2(7),7(15)])]. given #116 (F,wt=15): 2361 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0 # label(false). [para(2(a,1),1382(a,1,1)),rewrite([2(3),2(5)])]. given #117 (F,wt=15): 2483 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)) # label(false). [para(1537(a,1),36(a,1,2)),rewrite([173(2),2(1),2(3)]),flip(a)]. given #118 (F,wt=15): 2530 f(x,f(y,f(z,f(x,x)))) = f(x,f(y,y)) # label(false). [para(1623(a,2),2(a,2)),rewrite([2(2),2(3),173(4,R)]),flip(a)]. given #119 (F,wt=15): 2705 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0 # label(false). [para(2(a,1),1007(a,1,2,2)),rewrite([173(3),2(2),2(5)])]. given #120 (T,wt=15): 1131 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x. [para(1059(a,1),9(a,1,2,2)),rewrite([2(6)])]. given #121 (T,wt=15): 1132 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y. [para(1059(a,1),12(a,1,2,2)),rewrite([2(4),2(5),2(6)])]. given #122 (T,wt=15): 1149 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(1059(a,1),617(a,1,2,2)),rewrite([561(7,R),2(5),2(7),561(7),2(7)])]. given #123 (T,wt=15): 1152 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x. [para(1061(a,1),3(a,1,2,2)),rewrite([2(6)])]. given #124 (A,wt=19): 44 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y). [para(13(a,1),13(a,1,2,1)),rewrite([2(5),13(11)])]. given #125 (F,wt=15): 2858 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x) # label(false). [para(1819(a,1),2(a,2)),rewrite([2(1),2(5)])]. given #126 (F,wt=15): 2906 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x) # label(false). [para(898(a,2),1819(a,1,2))]. given #127 (F,wt=15): 3014 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x) # label(false). [para(24(a,1),1024(a,1,2,2)),rewrite([173(2),2(1),173(4),2(3),561(5,R),2(4),554(8),2(6),173(8),2(7),743(9)])]. given #128 (F,wt=15): 3261 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)) # label(false). [para(2483(a,1),2(a,2)),rewrite([2(1),2(4),2(5),173(6,R)])]. given #129 (T,wt=15): 1154 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y. [para(1061(a,1),6(a,1,2,2)),rewrite([2(4),2(5),2(6)])]. given #130 (T,wt=15): 1186 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(1061(a,1),558(a,1,2,2)),rewrite([561(7,R),2(5),2(7),561(7),2(7)])]. given #131 (T,wt=15): 1235 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x). [para(608(a,1),738(a,1,2,1)),rewrite([2(7),809(9)])]. given #132 (T,wt=15): 1236 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0. [para(738(a,1),617(a,1,2,2)),rewrite([561(11,R),2(7),554(10),2(8)])]. given #133 (A,wt=17): 45 f(f(x,y),f(y,f(z,f(f(x,y),f(x,u))))) = y. [para(15(a,1),3(a,1,1)),rewrite([2(5)])]. given #134 (F,wt=15): 3835 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x) # label(false). [para(2906(a,1),2(a,2)),rewrite([2(2),2(6)])]. given #135 (F,wt=17): 175 f(f(x,f(x,y)),f(f(x,z),f(y,y))) = f(y,y) # label(false). [para(160(a,1),6(a,1,1)),rewrite([2(5)])]. given #136 (F,wt=17): 181 f(x,f(y,f(f(x,y),f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),160(a,2,2)),rewrite([125(7)])]. given #137 (F,wt=17): 256 f(f(x,f(y,y)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(38(a,1),31(a,1,2,2,2)),rewrite([2(2),173(2,R),2(4)])]. given #138 (T,wt=13): 4405 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(256(a,1),947(a,1,2,2,2)),rewrite([2(8),6(8),2(5),561(5),2(5)])]. given #139 (T,wt=15): 1264 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x. [para(801(a,1),9(a,1,2,2)),rewrite([2(7)])]. given #140 (T,wt=15): 1265 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y. [para(801(a,1),12(a,1,2,2)),rewrite([2(5),2(6),2(7)])]. given #141 (T,wt=15): 1501 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(1274(a,1),11(a,1,2,2,2)),rewrite([2(11),561(14),2(14),1291(15),2(9)]),flip(a)]. given #142 (A,wt=23): 47 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(15(a,1),6(a,1,1)),rewrite([2(6)])]. given #143 (F,wt=17): 435 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)) # label(false). [para(191(a,1),36(a,1,2)),flip(a)]. given #144 (F,wt=17): 600 f(f(x,y),f(y,f(y,f(x,z)))) = f(c_0,f(x,y)) # label(false). [back_rewrite(142),rewrite([561(8,R),2(8)])]. given #145 (F,wt=17): 601 f(f(x,y),f(x,f(x,f(y,z)))) = f(c_0,f(x,y)) # label(false). [back_rewrite(119),rewrite([561(8,R),2(8)])]. given #146 (F,wt=17): 647 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),29(a,1,2,2)),rewrite([2(4),16(6),2(5),581(8)]),flip(a)]. given #147 (T,wt=15): 1502 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(1471(a,1),9(a,1,2,2)),rewrite([2(7)])]. given #148 (T,wt=15): 1503 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y. [para(1471(a,1),12(a,1,2,2)),rewrite([2(5),2(6),2(7)])]. given #149 (T,wt=15): 1526 f(f(c_0,c_0),f(x,f(f(y,z),f(u,w)))) = c_0. [para(1475(a,1),11(a,1,2,2,2)),rewrite([2(10),561(13),2(13),1291(14),2(8)]),flip(a)]. given #150 (T,wt=15): 1528 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [para(6(a,1),59(a,1,2,2)),rewrite([2(6)])]. given #151 (A,wt=23): 49 f(f(f(x,y),f(x,z)),f(f(x,y),f(u,f(x,f(y,w))))) = f(x,y). [para(7(a,1),15(a,1,2,1)),rewrite([2(9),7(15)])]. given #152 (F,wt=17): 1057 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)) # label(false). [para(591(a,1),3(a,1,2)),rewrite([2(4),2(6)])]. given #153 (F,wt=15): 5644 f(x,f(x,f(y,f(z,f(z,x))))) = f(y,x) # label(false). [para(1629(a,1),1057(a,1,2,2)),rewrite([173(2),2(1),2(4),2(6),5624(8),173(3),2(2)]),flip(a)]. given #154 (F,wt=17): 1392 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)) # label(false). [para(6(a,1),898(a,2,2)),rewrite([2(8),173(8,R)])]. given #155 (F,wt=17): 1400 f(x,f(c_0,f(f(x,y),f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),898(a,2,2))]. given #156 (T,wt=15): 1735 f(x,f(c_0,f(y,f(z,f(x,x))))) = f(x,y). [para(969(a,1),898(a,2,2)),rewrite([8(9)])]. given #157 (T,wt=15): 1753 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(2(a,1),982(a,1,2,2,2,2,2)),rewrite([173(3,R)])]. given #158 (T,wt=15): 1824 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(3(a,1),1630(a,1,2,1)),rewrite([561(3,R),2(3),2(5),2(7)])]. given #159 (T,wt=15): 1826 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [para(6(a,1),1630(a,1,2,1)),rewrite([561(3,R),2(3),2(5),2(7)])]. given #160 (A,wt=19): 50 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y). [para(13(a,1),15(a,1,2,1)),rewrite([2(7),13(11)])]. given #161 (F,wt=15): 5976 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(y,x) # label(false). [para(1735(a,1),2(a,2)),rewrite([173(3),2(2),2(6),2(7)])]. given #162 (F,wt=17): 1412 f(x,f(c_0,f(f(x,y),f(z,y)))) = f(x,f(x,y)) # label(false). [para(17(a,1),898(a,2,2)),rewrite([2(3),2(4),2(7)])]. given #163 (F,wt=17): 2373 f(f(x,x),f(f(y,x),f(z,f(z,f(x,x))))) = c_0 # label(false). [para(27(a,1),1382(a,1,2,2)),rewrite([2(7),561(7),2(7)])]. given #164 (F,wt=17): 3281 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y) # label(false). [para(173(a,1),2483(a,1,2,2,2)),rewrite([2(2),173(8),2(7),8(9)])]. given #165 (T,wt=15): 1842 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(1630(a,1),738(a,1,2,1)),rewrite([2(7),809(9),561(9,R),2(9),554(9)])]. given #166 (T,wt=15): 2024 f(x,f(c_0,f(f(x,f(y,z)),f(z,z)))) = c_0. [para(1200(a,1),617(a,1,2,2)),rewrite([561(9,R),2(6),554(9),2(7)])]. given #167 (T,wt=15): 2046 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(2(a,1),1241(a,1,1)),rewrite([2(2),2(4),173(5,R)])]. given #168 (T,wt=15): 2064 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(173(a,1),1241(a,1,2,2,2)),rewrite([2(2),2(5),8(7)])]. given #169 (A,wt=19): 52 f(f(f(x,y),f(x,z)),f(f(x,z),f(z,u))) = f(x,z). [para(16(a,1),15(a,1,2,1)),rewrite([16(11)])]. given #170 (F,wt=17): 4149 f(f(x,f(x,y)),f(f(z,x),f(y,y))) = f(y,y) # label(false). [para(6(a,1),175(a,1,2,1)),rewrite([2(3),173(4,R),173(5),2(4),2(6)])]. given #171 (F,wt=17): 4261 f(x,f(y,f(f(y,x),f(y,z)))) = f(x,f(y,y)) # label(false). [para(181(a,1),2(a,2)),rewrite([2(1),2(5),2(6),173(7,R)])]. given #172 (F,wt=17): 4813 f(f(x,x),f(y,f(x,z))) = f(f(y,y),f(x,x)) # label(false). [para(435(a,1),2(a,2)),rewrite([2(4),2(7)])]. given #173 (F,wt=17): 4885 f(x,f(y,f(y,f(f(x,x),f(z,z))))) = f(x,x) # label(false). [para(435(a,1),1059(a,1,2,2,2)),rewrite([561(3,R),2(3),554(3)])]. given #174 (T,wt=15): 2108 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(2(a,1),1242(a,1,1)),rewrite([2(2),2(4),173(5,R)])]. given #175 (T,wt=15): 2155 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x. [para(2(a,1),463(a,1,1,2))]. given #176 (T,wt=15): 2409 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(558(a,1),1382(a,1,1,2,2)),rewrite([2(3),554(3)])]. given #177 (T,wt=15): 2679 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0. [para(6(a,1),1005(a,1,2,2,2,2)),rewrite([561(4,R),2(4),2(6)])]. given #178 (A,wt=19): 54 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)). [para(2(a,1),11(a,1,2))]. given #179 (F,wt=17): 4909 f(x,f(f(y,y),f(f(x,x),f(y,z)))) = f(x,y) # label(false). [para(435(a,2),969(a,1,2)),rewrite([173(8),2(7),8(9)])]. given #180 (F,wt=17): 5040 f(x,f(y,f(f(x,x),f(z,z)))) = f(x,f(x,y)) # label(false). [para(435(a,1),435(a,1,2,2)),rewrite([561(3,R),2(3),554(3),561(8,R),2(8),554(8),173(7),2(6)])]. given #181 (F,wt=17): 5677 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(y,x)) # label(false). [para(435(a,1),1057(a,1,2,2,2)),rewrite([2(3),2(8),173(9,R),561(8,R),2(8),554(8),2(6),173(6),2(5),2106(8),4881(8)]),flip(a)]. given #182 (F,wt=17): 5790 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,x))))) = y # label(false). [para(10(a,1),1392(a,1,1)),rewrite([173(4,R),2(6),173(10,R),2(12),19(12)])]. given #183 (T,wt=15): 2895 f(x,f(c_0,f(y,f(y,f(z,f(y,x)))))) = c_0. [para(1819(a,1),617(a,1,2,2)),rewrite([2(1),2(5),561(9,R),2(6),554(9),2(7)])]. given #184 (T,wt=15): 2903 f(x,f(c_0,f(y,f(y,f(z,f(x,y)))))) = c_0. [para(1819(a,1),898(a,2,2)),rewrite([528(9)])]. given #185 (T,wt=15): 2941 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(176(a,2),1894(a,1,2,2,2)),rewrite([1736(8)])]. given #186 (T,wt=15): 3221 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [para(2361(a,1),2(a,1)),rewrite([2(5),173(6,R),2(8)]),flip(a)]. given #187 (A,wt=23): 55 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(w,f(x,y)))))) = x. [para(11(a,1),3(a,1,1)),rewrite([2(8)])]. given #188 (F,wt=17): 6380 f(x,f(f(y,f(x,f(x,z))),f(z,z))) = f(x,z) # label(false). [para(2(a,1),3281(a,1,2))]. Low Water (keep): wt=51.000, iters=7192 Low Water (keep): wt=45.000, iters=6915 Low Water (keep): wt=43.000, iters=6778 given #189 (F,wt=17): 7037 f(f(x,y),f(c_0,f(x,f(z,y)))) = f(x,f(x,y)) # label(false). [para(2108(a,1),1061(a,1,1,2)),rewrite([2(4),173(6),2(5),173(8),2(7),561(9,R),2(8),2(9),5771(9),173(8),2(7)])]. given #190 (F,wt=17): 7397 f(f(x,f(y,y)),f(x,f(f(y,x),f(x,z)))) = x # label(false). [para(4909(a,1),4261(a,1,2,2,1)),rewrite([2(4),4881(5),554(4),2(2),2(3),2(11),4881(12),554(11),2(9),2(11),19(11)])]. Low Water (keep): wt=41.000, iters=6732 given #191 (F,wt=17): 7399 f(x,f(f(y,y),f(c_0,f(x,f(y,z))))) = f(x,y) # label(false). [para(4813(a,2),4909(a,1,2,2)),rewrite([4881(6)])]. given #192 (T,wt=15): 3310 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(2483(a,1),898(a,2,2)),rewrite([8(9)])]. Low Water (keep): wt=39.000, iters=6715 given #193 (T,wt=15): 3852 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0. [para(2906(a,1),617(a,1,2,2)),rewrite([2(2),2(7),561(11,R),2(7),554(10),2(8)])]. given #194 (T,wt=15): 3856 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0. [para(2906(a,1),898(a,2,2)),rewrite([528(10)])]. given #195 (T,wt=15): 3969 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z). [para(34(a,1),1154(a,1,2)),rewrite([173(2),2(1),2(3),2(5),2(6)])]. given #196 (A,wt=33): 56 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(w,f(x,y))))) = f(f(x,f(y,z)),f(w,f(x,y))). [para(11(a,1),6(a,1,1)),rewrite([2(9)])]. given #197 (F,wt=17): 7406 f(x,f(y,f(f(x,x),f(z,z)))) = f(x,f(y,y)) # label(false). [para(5040(a,1),2(a,2)),rewrite([2(5),2(6),173(7,R)])]. given #198 (F,wt=17): 7409 f(x,f(x,f(y,f(f(x,x),f(z,z))))) = f(x,y) # label(false). [para(5040(a,2),6(a,1,1)),rewrite([3926(9)])]. Low Water (keep): wt=37.000, iters=6757 given #199 (F,wt=17): 7680 f(f(x,y),f(f(y,y),f(c_0,f(x,f(y,z))))) = x # label(false). [para(5677(a,2),9(a,1,2))]. given #200 (F,wt=17): 8006 f(f(x,f(y,y)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(19(a,1),5790(a,1,2,2,2,2)),rewrite([2(2),2(5),2(6)])]. given #201 (T,wt=15): 5670 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(256(a,1),1057(a,1,2,2,2)),rewrite([2(4),2(9),6(9),2(6),561(6),2(6),256(14),2(10),6(10)])]. given #202 (T,wt=15): 6068 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(1824(a,1),173(a,2,2)),rewrite([561(10,R),2(8),5771(9),2(11),809(11)])]. given #203 (T,wt=17): 58 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(6(a,1),11(a,2,2)),rewrite([6(4)])]. Low Water (keep): wt=35.000, iters=6676 given #204 (T,wt=17): 196 f(x,f(f(x,y),f(f(x,x),f(y,z)))) = f(x,y). [para(173(a,2),7(a,1,2,2)),rewrite([2(4)])]. given #205 (A,wt=31): 57 f(f(x,y),f(f(y,z),f(f(x,y),f(u,f(y,f(x,w)))))) = f(f(x,y),f(u,f(y,f(x,w)))). [para(6(a,1),11(a,1,2,2,2)),rewrite([2(5),2(7),2(8),2(13)])]. given #206 (F,wt=17): 8127 f(f(x,x),f(f(y,y),f(x,z))) = f(y,f(y,x)) # label(false). [para(4909(a,1),5790(a,1,1)),rewrite([2(8),2(15),191(15),561(11,R),2(11),554(11),2(9),7374(11)]),flip(a)]. given #207 (F,wt=17): 8599 f(f(x,x),f(c_0,f(y,f(z,x)))) = f(y,f(y,x)) # label(false). [para(7037(a,1),10(a,1,2,2)),rewrite([2(11),7879(11),173(10,R),2(6),7037(12)])]. given #208 (F,wt=17): 8851 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)) # label(false). [para(1200(a,1),3310(a,1,2,2,2)),rewrite([2(6),1511(8)]),flip(a)]. given #209 (F,wt=15): 10062 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_rewrite(7678),rewrite([9874(7)])]. given #210 (T,wt=15): 10064 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(2630),rewrite([9874(7)])]. Low Water (keep): wt=33.000, iters=6756 given #211 (T,wt=15): 10149 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))). [para(10062(a,2),39(a,2)),rewrite([743(5),561(3,R),2(3),2(6)])]. given #212 (T,wt=15): 10482 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(10062(a,2),2903(a,1,2,2,2,2)),rewrite([2(5),3313(9),2202(11)])]. given #213 (T,wt=15): 10723 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))). [para(10064(a,1),2(a,2)),rewrite([2(4),2(6)])]. given #214 (A,wt=31): 62 f(x,f(f(x,f(y,z)),f(u,f(x,f(w,f(f(x,f(y,z)),f(v5,f(x,y)))))))) = f(x,f(y,z)). [para(11(a,1),7(a,1,2,1)),rewrite([2(8),11(18)])]. given #215 (F,wt=15): 10079 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(10062(a,1),2(a,1)),rewrite([2(5),2(7)]),flip(a)]. given #216 (F,wt=15): 10080 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(10062(a,1),2(a,2)),rewrite([2(4),2(5)])]. given #217 (F,wt=15): 10089 f(f(x,f(y,z)),f(z,f(z,f(x,y)))) = x # label(false). [para(10062(a,1),9(a,1,2))]. given #218 (F,wt=15): 10091 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x # label(false). [para(10062(a,2),9(a,1,2)),rewrite([2(4)])]. given #219 (T,wt=15): 11332 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(10080(a,2),2903(a,1,2,2,2,2)),rewrite([2(5),3313(9),2202(11)])]. Low Water (keep): wt=31.000, iters=6774 given #220 (T,wt=17): 219 f(x,f(f(y,z),f(y,f(y,f(x,x))))) = f(x,y). [para(176(a,2),13(a,1,2,1)),rewrite([2(5)])]. given #221 (T,wt=17): 241 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(38(a,1),9(a,1,2)),rewrite([2(6)])]. given #222 (T,wt=17): 861 f(f(x,f(y,z)),f(f(x,u),f(y,z))) = f(y,z). [para(46(a,1),30(a,1,2,2,2)),rewrite([2(4),2(5)])]. given #223 (A,wt=27): 65 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(w,f(x,y)))))) = f(x,f(y,z)). [para(11(a,1),13(a,1,2,1)),rewrite([2(8),11(16)])]. given #224 (F,wt=15): 10093 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z # label(false). [para(10062(a,1),12(a,1,2)),rewrite([2(2),2(3),2(6)])]. given #225 (F,wt=15): 10094 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x # label(false). [para(10062(a,2),12(a,1,2)),rewrite([2(2)])]. given #226 (F,wt=15): 10095 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(10062(a,1),8(a,2)),rewrite([900(5)])]. given #227 (F,wt=15): 10096 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(10062(a,2),8(a,1,2)),rewrite([2(2)])]. given #228 (T,wt=17): 880 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(222(a,1),24(a,1,2,2)),rewrite([173(2),2(1),8(3),173(3),2(2),8(4),2(3),561(4,R),2(4),173(8),2(7),8(9),173(9),2(8),8(10),561(9,R),2(9)])]. given #229 (T,wt=17): 1090 f(f(x,y),f(c_0,f(z,f(y,y)))) = f(z,f(y,y)). [para(26(a,1),591(a,1,2,2)),rewrite([173(2),2(1),8(3),26(12)])]. given #230 (T,wt=17): 1091 f(f(x,y),f(c_0,f(z,f(x,x)))) = f(z,f(x,x)). [para(176(a,1),591(a,1,1)),rewrite([2(4),2(8)])]. given #231 (T,wt=17): 1141 f(x,f(f(x,y),f(z,f(z,f(y,u))))) = f(x,y). [para(1059(a,1),39(a,1,2,2,2)),rewrite([2(5),1059(11)])]. given #232 (A,wt=27): 67 f(f(f(x,y),f(x,f(z,u))),f(f(x,f(z,u)),f(w,f(x,z)))) = f(x,f(z,u)). [para(11(a,1),15(a,1,2,1)),rewrite([2(9),2(10),11(16)])]. given #233 (F,wt=15): 10153 f(f(x,f(y,z)),f(y,f(y,f(x,x)))) = x # label(false). [para(10062(a,1),46(a,1,2))]. given #234 (F,wt=15): 10159 f(f(x,f(y,z)),f(z,f(z,f(x,x)))) = x # label(false). [para(10062(a,1),48(a,1,2))]. given #235 (F,wt=15): 10220 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(10062(a,1),898(a,1)),rewrite([2(4)])]. given #236 (F,wt=15): 10227 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)) # label(false). [para(10062(a,1),900(a,1,2)),rewrite([2(5)])]. given #237 (T,wt=17): 1171 f(x,f(f(x,y),f(z,f(z,f(u,y))))) = f(x,y). [para(1061(a,1),36(a,1,2,2,2)),rewrite([2(5),1061(11)])]. given #238 (T,wt=17): 1193 f(f(x,f(x,f(y,f(y,f(z,u))))),f(u,u)) = u. [para(1061(a,1),591(a,1,2,2)),rewrite([2(7),561(7),1061(12)])]. given #239 (T,wt=17): 1225 f(x,f(f(x,y),f(z,f(c_0,f(y,u))))) = f(x,y). [para(738(a,1),46(a,1,2,2)),rewrite([2(5),2(9),19(9),2(7)])]. given #240 (T,wt=17): 1280 f(x,f(c_0,f(y,f(c_0,f(f(x,x),f(z,u)))))) = c_0. [para(1003(a,1),13(a,1,2,1)),rewrite([2(7),1003(15)])]. given #241 (A,wt=23): 69 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(w,y))))))) = f(x,y). [para(17(a,1),7(a,2)),rewrite([2(2),2(3),51(4),2(3),2(4),2(5),2(10)])]. given #242 (F,wt=13): 12888 f(f(x,x),f(y,f(y,f(z,x)))) = x # label(false). [para(12(a,1),1193(a,1,1,2)),rewrite([2(2),2(3),2(5)])]. given #243 (F,wt=15): 10426 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0 # label(false). [para(10062(a,1),1824(a,1,1,2)),rewrite([2(8),809(10),2(7)])]. given #244 (F,wt=15): 10522 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y # label(false). [para(10062(a,1),7680(a,1,1)),rewrite([2(5),2(8),561(10,R),2(8),809(8),2(7),2(9),3392(12)])]. given #245 (F,wt=15): 10551 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(10062(a,1),8599(a,1,2,2)),rewrite([561(3,R),2(3),2(5),5116(9)])]. given #246 (T,wt=17): 1289 f(x,f(y,f(c_0,f(f(x,x),f(z,u))))) = f(x,x). [para(1003(a,1),738(a,1,2,1)),rewrite([2(8),809(10)])]. given #247 (T,wt=17): 1358 f(x,f(y,f(x,f(f(y,y),f(z,u))))) = f(x,x). [para(81(a,1),770(a,1,2,2,2)),rewrite([554(7),2(5)])]. given #248 (T,wt=17): 1417 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(898(a,1),81(a,1,2,1)),rewrite([2(11),173(11,R),807(11),2(8),809(8),561(14,R),2(12),809(12)])]. given #249 (T,wt=17): 1452 f(f(x,y),f(x,f(c_0,f(y,z)))) = f(c_0,f(x,y)). [para(898(a,2),29(a,2,2)),rewrite([601(7),880(7)]),flip(a)]. given #250 (A,wt=19): 70 f(x,f(f(x,y),f(z,f(f(x,y),f(u,y))))) = f(x,y). [para(17(a,1),13(a,2)),rewrite([2(2),2(3),51(4),2(3),2(4),2(5),2(8)])]. given #251 (F,wt=15): 10722 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [back_rewrite(7310),rewrite([10549(8),10096(6)]),flip(a)]. given #252 (F,wt=15): 10727 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x # label(false). [para(10064(a,1),9(a,1,2))]. given #253 (F,wt=15): 10728 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x # label(false). [para(10064(a,1),12(a,1,2)),rewrite([2(2),2(4)])]. given #254 (F,wt=15): 10729 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))) # label(false). [para(10064(a,1),8(a,2)),rewrite([900(5)]),flip(a)]. given #255 (T,wt=17): 1514 f(x,f(f(x,y),f(z,f(c_0,f(u,y))))) = f(x,y). [para(1471(a,1),39(a,1,2,2,2)),rewrite([2(6),1471(13)])]. given #256 (T,wt=17): 1828 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(1630(a,1),13(a,1,2,1)),rewrite([2(6),1630(13)])]. given #257 (T,wt=17): 1829 f(f(c_0,f(x,f(y,y))),f(f(y,z),f(y,u))) = c_0. [para(1630(a,1),15(a,1,2,1)),rewrite([2(6),2(8),1630(13)])]. given #258 (T,wt=17): 1845 f(x,f(f(x,y),f(f(y,z),f(y,u)))) = f(x,x). [para(1630(a,1),959(a,1,2,2,2,2)),rewrite([2(6),554(6),2(5)])]. given #259 (A,wt=19): 71 f(f(f(x,y),f(y,z)),f(f(y,z),f(z,u))) = f(y,z). [para(17(a,1),15(a,1,2,1)),rewrite([17(11)])]. Low Water (keep): wt=29.000, iters=6709 given #260 (F,wt=15): 10878 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)) # label(false). [para(10064(a,2),1057(a,2,2)),rewrite([2(4),900(10),1468(9)]),flip(a)]. given #261 (F,wt=15): 11114 f(f(x,f(y,z)),f(y,f(y,f(x,z)))) = x # label(false). [para(10079(a,1),9(a,1,2))]. given #262 (F,wt=15): 11115 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label(false). [para(10079(a,1),12(a,1,2)),rewrite([2(2),2(3),2(6)])]. given #263 (F,wt=15): 11196 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)) # label(false). [para(10079(a,1),1057(a,2,2)),rewrite([2(4),900(10),1468(9),2(3)]),flip(a)]. given #264 (T,wt=17): 1996 f(f(x,y),f(y,f(c_0,f(x,z)))) = f(c_0,f(x,y)). [para(6(a,1),1200(a,1,2,1)),rewrite([561(4,R),2(4),561(9,R),2(9)])]. given #265 (T,wt=17): 2204 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(x,u)))))) = x. [para(541(a,1),738(a,1,2,1)),rewrite([2(10),809(12),561(12,R),2(12),554(12)])]. given #266 (T,wt=17): 2360 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)). [back_rewrite(2185),rewrite([2317(6)])]. given #267 (T,wt=17): 2447 f(f(x,y),f(c_0,f(x,f(f(y,z),f(y,u))))) = c_0. [para(1630(a,1),1382(a,1,1,2,2)),rewrite([2(3),554(3)])]. given #268 (A,wt=31): 72 f(x,f(f(y,f(x,z)),f(x,f(u,f(f(x,z),f(w,z)))))) = f(x,f(u,f(f(x,z),f(w,z)))). [para(17(a,1),11(a,1,2,2,2)),rewrite([2(2),2(3),2(4),2(6),2(8),2(11),2(12),2(13)])]. given #269 (F,wt=15): 12206 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0 # label(false). [para(10095(a,1),2903(a,1,2,2,2,2)),rewrite([3313(8),3659(10)])]. given #270 (F,wt=15): 12283 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),10096(a,1,2,2,2)),rewrite([10096(5)]),flip(a)]. given #271 (F,wt=15): 13418 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(10722(a,1),2(a,2)),rewrite([2(3),2(4)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 31.84 (+ 0.12) seconds: "Sheffer". % Length of proof is 94. % Level of proof is 25. % Maximum clause weight is 43.000. % Given clauses 271. 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(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. 4 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)]. 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [copy(4),rewrite([2(25),2(30)]),flip(c)]. 6 f(f(x,y),f(y,f(x,z))) = y # label(false). [para(2(a,1),3(a,1,1))]. 7 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(3(a,1),3(a,1,1)),rewrite([2(4)])]. 8 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. 9 f(f(x,y),f(x,f(z,y))) = x # label(false). [para(6(a,1),3(a,1,2,2)),rewrite([2(4)])]. 10 f(x,f(x,f(y,x))) = f(y,x). [para(6(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. 11 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(3(a,1),6(a,1,1)),rewrite([2(4)])]. 12 f(f(x,y),f(y,f(z,x))) = y # label(false). [para(6(a,1),6(a,1,2,2)),rewrite([2(2),2(3),2(4)])]. 13 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite([2(4)])]. 14 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(9(a,1),6(a,1,1)),rewrite([2(4)])]. 15 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(6(a,1),9(a,1,2)),rewrite([2(4)])]. 16 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(3(a,1),12(a,1,2)),rewrite([2(2),2(4),2(5)])]. 19 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. 20 f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [back_rewrite(5),rewrite([19(7)]),xx(a)]. 21 f(x,f(f(x,x),f(y,f(x,z)))) = f(x,x). [para(19(a,1),3(a,1,1)),rewrite([2(3)])]. 23 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(19(a,1),6(a,1,1)),rewrite([2(3)])]. 24 f(x,f(y,f(x,x))) = f(x,x). [para(19(a,1),9(a,1,2)),rewrite([2(2),2(3)])]. 26 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(24(a,1),6(a,1,1)),rewrite([2(5)])]. 27 f(f(x,y),f(y,y)) = y. [para(24(a,1),6(a,1,2))]. 29 f(f(x,y),f(f(x,z),f(f(x,y),f(u,f(x,f(y,w)))))) = f(f(x,y),f(u,f(x,f(y,w)))). [para(7(a,1),6(a,1,1)),rewrite([2(8)])]. 36 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),13(a,1,2,2)),rewrite([2(3)])]. 39 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(6(a,1),13(a,1,2,2)),rewrite([2(3)])]. 59 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(11(a,1),9(a,1,2))]. 81 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(11(a,1),21(a,1,2))]. 117 f(x,f(y,f(x,y))) = f(x,x) # label(false). [para(9(a,1),36(a,1,2)),rewrite([2(3)]),flip(a)]. 124 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(x,y)),f(x,f(y,z))) # label(false). [para(11(a,1),36(a,1,2)),rewrite([2(10)])]. 160 f(x,f(y,y)) = f(x,f(x,y)) # label(false). [para(117(a,1),36(a,1,2)),rewrite([2(3)])]. 161 f(x,f(f(x,f(y,z)),f(y,f(x,f(y,z))))) = f(x,x) # label(false). [para(36(a,1),117(a,1,2,2)),rewrite([2(6)])]. 172 f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) # answer("Sheffer"). [back_rewrite(20),rewrite([160(27),160(32)])]. 173 f(x,f(y,y)) = f(x,f(y,x)) # label(false). [para(160(a,1),2(a,2)),rewrite([2(2),2(3)])]. 176 f(x,f(x,f(y,y))) = f(y,x) # label(false). [para(160(a,1),9(a,1)),rewrite([2(2),173(2,R),2(4),173(4,R),2(6),6(6),2(3)])]. 179 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(160(a,1),27(a,1,1)),rewrite([19(5),2(3)])]. 191 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x) # label(false). [back_rewrite(161),rewrite([173(6,R),2(4)])]. 210 f(f(x,f(y,y)),f(f(y,z),f(y,z))) = f(y,z). [para(26(a,1),173(a,2,2)),rewrite([19(7),2(5),23(5),2(8),173(8,R)]),flip(a)]. 211 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x # label(false). [para(176(a,2),3(a,1,2,2))]. 222 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)) # label(false). [para(176(a,1),11(a,1,2,1,2)),rewrite([14(6)]),flip(a)]. 354 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x # label(false). [para(179(a,1),12(a,1,2,2)),rewrite([2(3)])]. 428 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x) # label(false). [para(19(a,1),191(a,1,2,1)),rewrite([2(2)])]. 435 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)) # label(false). [para(191(a,1),36(a,1,2)),flip(a)]. 439 f(x,f(y,f(y,y))) = f(x,x). [para(191(a,1),39(a,1)),flip(a)]. 447 f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) # answer("Sheffer"). [back_unit_del(172),unit_del(a,439)]. 486 f(f(x,x),f(f(x,y),f(z,f(z,z)))) = f(z,f(z,z)). [para(439(a,1),6(a,1,1)),rewrite([2(5)])]. 490 f(f(x,x),f(y,f(y,y))) = x. [para(439(a,2),19(a,1))]. 496 f(x,f(x,x)) = f(y,f(y,y)). [para(439(a,1),27(a,1,1)),rewrite([173(7),2(5),490(5),2(2)])]. 498 f(x,f(f(x,y),f(z,f(z,z)))) = f(x,y). [para(439(a,2),15(a,1,2)),rewrite([2(1),2(6)])]. 528 f(x,f(x,x)) = c_0. [new_symbol(496)]. 549 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(498),rewrite([528(3),2(3)])]. 554 f(c_0,f(x,x)) = x. [back_rewrite(490),rewrite([528(3),2(3)])]. 558 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(486),rewrite([528(4),2(4),528(7)])]. 561 f(x,c_0) = f(x,x). [back_rewrite(439),rewrite([528(2)])]. 571 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer"). [back_rewrite(447),rewrite([561(11,R),2(7)]),flip(a)]. 581 f(f(x,f(x,y)),f(x,f(y,z))) = f(c_0,f(x,f(y,z))) # label(false). [back_rewrite(124),rewrite([561(5,R),2(4)]),flip(a)]. 591 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [back_rewrite(210),rewrite([173(2),2(1),561(5,R),2(5)])]. 647 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),29(a,1,2,2)),rewrite([2(4),16(6),2(5),581(8)]),flip(a)]. 738 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x) # label(false). [para(211(a,1),191(a,1,2,2,2)),rewrite([561(3,R),2(3),2(5)])]. 809 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(549(a,1),176(a,2)),rewrite([2(8),558(8),2(5)])]. 898 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))) # label(false). [para(222(a,1),173(a,1,2)),rewrite([173(2),2(1),8(3),2(2),561(3,R),2(3),173(6),2(5),8(7),2(6)])]. 900 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)) # label(false). [para(222(a,1),176(a,1,2,2)),rewrite([173(2),2(1),8(3),2(2),561(3,R),2(3),173(7),2(6),8(8),2(7)])]. 947 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(554(a,1),354(a,1,2)),rewrite([2(5)])]. 969 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)) # label(false). [para(428(a,1),36(a,1,2)),rewrite([173(2),2(1)]),flip(a)]. 1057 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)) # label(false). [para(591(a,1),3(a,1,2)),rewrite([2(4),2(6)])]. 1061 f(f(x,f(x,f(y,z))),f(z,z)) = z # label(false). [para(6(a,1),591(a,1,2,2)),rewrite([2(5),561(5),6(9)])]. 1157 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x) # label(false). [para(19(a,1),1061(a,1,2)),rewrite([173(2),2(1),2(5)])]. 1200 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x) # label(false). [para(6(a,1),738(a,1,2,2,2)),rewrite([2(4),561(4)])]. 1241 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0 # label(false). [para(3(a,1),947(a,1,2,2,2)),rewrite([2(5)])]. 1392 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)) # label(false). [para(6(a,1),898(a,2,2)),rewrite([2(8),173(8,R)])]. 1471 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(898(a,2),1061(a,1,1)),rewrite([2(6)])]. 1511 f(f(x,y),f(c_0,f(f(x,x),f(z,u)))) = f(f(x,x),f(z,u)). [para(81(a,1),1471(a,1,2,2,2)),rewrite([561(7,R),2(5),554(8),2(6),2(7)])]. 1537 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x) # label(false). [para(59(a,1),39(a,1,2)),flip(a)]. 2106 f(f(x,f(y,f(z,u))),f(c_0,f(y,f(y,z)))) = f(y,f(y,z)). [para(1241(a,1),1157(a,1,2,2,2,2)),rewrite([2(8),900(10),2(8),561(17,R),2(14),809(14)])]. 2483 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)) # label(false). [para(1537(a,1),36(a,1,2)),rewrite([173(2),2(1),2(3)]),flip(a)]. 3310 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(2483(a,1),898(a,2,2)),rewrite([8(9)])]. 4881 f(f(x,x),f(f(x,y),f(z,u))) = f(f(x,x),f(c_0,f(z,u))). [para(222(a,1),435(a,2,2)),rewrite([173(3),2(2),8(4),2(4),173(8),2(7),8(9),2(8),561(9,R),2(9)])]. 4909 f(x,f(f(y,y),f(f(x,x),f(y,z)))) = f(x,y) # label(false). [para(435(a,2),969(a,1,2)),rewrite([173(8),2(7),8(9)])]. 5677 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(y,x)) # label(false). [para(435(a,1),1057(a,1,2,2,2)),rewrite([2(3),2(8),173(9,R),561(8,R),2(8),554(8),2(6),173(6),2(5),2106(8),4881(8)]),flip(a)]. 5790 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,x))))) = y # label(false). [para(10(a,1),1392(a,1,1)),rewrite([173(4,R),2(6),173(10,R),2(12),19(12)])]. 7310 f(x,f(f(c_0,f(y,f(y,z))),f(f(x,x),f(z,u)))) = f(x,f(y,f(y,z))). [para(591(a,1),4909(a,1,2,2,2)),rewrite([561(5,R),2(4)])]. 7374 f(f(x,y),f(c_0,f(x,f(z,f(f(y,y),f(f(x,x),f(y,u))))))) = f(x,f(x,y)). [para(4909(a,1),647(a,1,1)),rewrite([2(8),4909(17)])]. 7678 f(f(c_0,f(x,y)),f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(6(a,1),5677(a,1,2,2,2)),rewrite([561(3,R),2(3),2(5)])]. 8127 f(f(x,x),f(f(y,y),f(x,z))) = f(y,f(y,x)) # label(false). [para(4909(a,1),5790(a,1,1)),rewrite([2(8),2(15),191(15),561(11,R),2(11),554(11),2(9),7374(11)]),flip(a)]. 8851 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)) # label(false). [para(1200(a,1),3310(a,1,2,2,2)),rewrite([2(6),1511(8)]),flip(a)]. 9874 f(f(c_0,f(x,y)),f(c_0,f(y,z))) = f(x,f(c_0,f(y,z))). [para(3(a,1),8851(a,1,1)),rewrite([561(3,R),2(3),561(7,R),2(7),561(10,R),2(10)]),flip(a)]. 10062 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_rewrite(7678),rewrite([9874(7)])]. 10096 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(10062(a,2),8(a,1,2)),rewrite([2(2)])]. 10549 f(f(c_0,f(x,f(x,y))),f(f(z,z),f(y,u))) = f(x,f(c_0,f(z,f(z,y)))). [para(8127(a,1),10062(a,1,2,2)),rewrite([173(13),2(12),2(14),173(15,R),561(13,R),2(12),2(13)]),flip(a)]. 10722 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [back_rewrite(7310),rewrite([10549(8),10096(6)]),flip(a)]. 12283 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),10096(a,1,2,2,2)),rewrite([10096(5)]),flip(a)]. 13418 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(10722(a,1),2(a,2)),rewrite([2(3),2(4)]),flip(a)]. 14590 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))) # label(false). [para(12283(a,1),13418(a,1,2)),rewrite([2(3),581(5)]),flip(a)]. 14591 $F # answer("Sheffer"). [resolve(14590,a,571,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=271. Generated=275550. Kept=14588. proofs=1. Usable=223. Sos=8797. Demods=7972. Limbo=82, Disabled=5488. Hints=0. Kept_by_rule=0, Deleted_by_rule=22. Forward_subsumed=250813. Back_subsumed=1529. Sos_limit_deleted=10127. Sos_displaced=0. Sos_removed=0. New_demodulators=13083 (5 lex), Back_demodulated=3955. Back_unit_deleted=1. Demod_attempts=5546948. Demod_rewrites=1340376. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=15.04. User_CPU=31.84, System_CPU=0.12, Wall_clock=32. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6682 exit (max_proofs) Tue Nov 3 10:21:09 2009