============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 28115 was started by mccune on cleo, Fri Apr 13 09:58:24 2007 The command was "/home/mccune/bin/prover9 -f BA2.in BA2-interp.out13". ============================== 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.out13 list(interpretations). interpretation(6,[number = 1,seconds = 0],[function(c1,[0]),function(c2,[2]),function(c3,[1]),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(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(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # 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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c4, c5, c6, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). % Operation f is commutative; C redundancy checks enabled. not interpretable: c4 % Clause contains symbol not in interpretation: % f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [copy(4),rewrite(2(25),2(30)),flip(c)]. restricted denial: (wt=43): 5 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # 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(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # 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.00 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))]. not interpretable: c4 % Clause contains symbol not in interpretation: % f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [back_rewrite(5),rewrite(19(7)),xx(a)]. restricted denial: (wt=34): 20 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [back_rewrite(5),rewrite(19(7)),xx(a)]. 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)]. not interpretable: c4 % Clause contains symbol not in interpretation: % f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_rewrite(20),rewrite(160(27),160(32))]. restricted denial: (wt=34): 172 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_rewrite(20),rewrite(160(27),160(32))]. 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,v))))))) = 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))]. not interpretable: c4 % Clause contains symbol not in interpretation: % f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_unit_del(172),unit_del(a,439)]. restricted denial: (wt=23): 447 f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_unit_del(172),unit_del(a,439)]. 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: lex([ c4, c5, c6, c_0, f ]). NOTE: sn=91, num_tables=177 NOTE: updating interpretation 1: c_0=1. not interpretable: c4 % Clause contains symbol not in interpretation: % f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) != f(c_0,f(c4,f(c5,c6))) # answer("Sheffer"). [back_rewrite(447),rewrite(561(11,R),2(7)),flip(a)]. restricted denial: (wt=19): 571 f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) != f(c_0,f(c4,f(c5,c6))) # answer("Sheffer"). [back_rewrite(447),rewrite(561(11,R),2(7)),flip(a)]. 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,v)))))) = f(f(x,y),f(u,f(x,f(y,v)))). [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,v))))))) = 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(v,f(x,f(y,w))))))))) = 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,v))))))) = 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,v))))))) = 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,v)))) = 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,v))))) = 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): 5645 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),5625(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): 5977 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): 4886 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): 4910 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): 5041 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): 5678 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),4882(8)),flip(a)]. given #182 (F,wt=17): 5791 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(v,f(x,y)))))) = x. [para(11(a,1),3(a,1,1)),rewrite(2(8))]. given #188 (F,wt=17): 6381 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))]. given #189 (F,wt=17): 7038 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),5772(9),173(8),2(7))]. given #190 (F,wt=17): 7398 f(f(x,f(y,y)),f(x,f(f(y,x),f(x,z)))) = x # label(false). [para(4910(a,1),4261(a,1,2,2,1)),rewrite(2(4),4882(5),554(4),2(2),2(3),2(11),4882(12),554(11),2(9),2(11),19(11))]. given #191 (F,wt=17): 7400 f(x,f(f(y,y),f(c_0,f(x,f(y,z))))) = f(x,y) # label(false). [para(4813(a,2),4910(a,1,2,2)),rewrite(4882(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))]. 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(v,f(x,y))))) = f(f(x,f(y,z)),f(v,f(x,y))). [para(11(a,1),6(a,1,1)),rewrite(2(9))]. given #197 (F,wt=17): 7407 f(x,f(y,f(f(x,x),f(z,z)))) = f(x,f(y,y)) # label(false). [para(5041(a,1),2(a,2)),rewrite(2(5),2(6),173(7,R))]. given #198 (F,wt=17): 7410 f(x,f(x,f(y,f(f(x,x),f(z,z))))) = f(x,y) # label(false). [para(5041(a,2),6(a,1,1)),rewrite(3926(9))]. given #199 (F,wt=17): 7681 f(f(x,y),f(f(y,y),f(c_0,f(x,f(y,z))))) = x # label(false). [para(5678(a,2),9(a,1,2))]. given #200 (F,wt=17): 8007 f(f(x,f(y,y)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(19(a,1),5791(a,1,2,2,2,2)),rewrite(2(2),2(5),2(6))]. given #201 (T,wt=15): 5671 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): 6069 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),5772(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))]. 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,v)))))) = f(f(x,y),f(u,f(y,f(x,v)))). [para(6(a,1),11(a,1,2,2,2)),rewrite(2(5),2(7),2(8),2(13))]. given #206 (F,wt=17): 8128 f(f(x,x),f(f(y,y),f(x,z))) = f(y,f(y,x)) # label(false). [para(4910(a,1),5791(a,1,1)),rewrite(2(8),2(15),191(15),561(11,R),2(11),554(11),2(9),7375(11)),flip(a)]. given #207 (F,wt=17): 8611 f(f(x,x),f(c_0,f(y,f(z,x)))) = f(y,f(y,x)) # label(false). [para(7038(a,1),10(a,1,2,2)),rewrite(2(11),7880(11),173(10,R),2(6),7038(12))]. given #208 (F,wt=17): 8910 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): 11026 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_rewrite(7679),rewrite(10732(7))]. given #210 (T,wt=15): 11028 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(2630),rewrite(10732(7))]. given #211 (T,wt=15): 11115 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))). [para(11026(a,2),39(a,2)),rewrite(743(5),561(3,R),2(3),2(6))]. given #212 (T,wt=15): 11494 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(11026(a,2),2903(a,1,2,2,2,2)),rewrite(2(5),3313(9),2202(11))]. given #213 (T,wt=15): 11821 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))). [para(11028(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(v,f(f(x,f(y,z)),f(w,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): 11046 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(11026(a,1),2(a,1)),rewrite(2(5),2(7)),flip(a)]. given #216 (F,wt=15): 11047 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(11026(a,1),2(a,2)),rewrite(2(4),2(5))]. given #217 (F,wt=15): 11056 f(f(x,f(y,z)),f(z,f(z,f(x,y)))) = x # label(false). [para(11026(a,1),9(a,1,2))]. given #218 (F,wt=15): 11058 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x # label(false). [para(11026(a,2),9(a,1,2)),rewrite(2(4))]. given #219 (T,wt=15): 12844 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(11047(a,2),2903(a,1,2,2,2,2)),rewrite(2(5),3313(9),2202(11))]. 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(v,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): 11060 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z # label(false). [para(11026(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #225 (F,wt=15): 11061 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x # label(false). [para(11026(a,2),12(a,1,2)),rewrite(2(2))]. given #226 (F,wt=15): 11062 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(11026(a,2),8(a,1,2)),rewrite(2(2))]. given #227 (F,wt=15): 11063 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(11026(a,1),8(a,2)),rewrite(900(5))]. 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(v,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): 11119 f(f(x,f(y,z)),f(y,f(y,f(x,x)))) = x # label(false). [para(11026(a,1),46(a,1,2))]. given #234 (F,wt=15): 11125 f(f(x,f(y,z)),f(z,f(z,f(x,x)))) = x # label(false). [para(11026(a,1),48(a,1,2))]. given #235 (F,wt=15): 11203 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(11026(a,1),898(a,1)),rewrite(2(4))]. given #236 (F,wt=15): 11210 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)) # label(false). [para(11026(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))]. Low Water (keep, True_semantics): wt=79 Low Water (keep, True_semantics): wt=75 Low Water (keep, True_semantics): wt=71 Low Water (keep, True_semantics): wt=65 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))]. Low Water (keep, True_semantics): wt=63 Low Water (keep, True_semantics): wt=61 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(v,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): 15868 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): 11432 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0 # label(false). [para(11026(a,1),1824(a,1,1,2)),rewrite(2(8),809(10),2(7))]. given #244 (F,wt=15): 11554 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y # label(false). [para(11026(a,1),7681(a,1,1)),rewrite(2(5),2(8),561(10,R),2(8),809(8),2(7),2(9),3392(12))]. Low Water (keep, True_semantics): wt=59 given #245 (F,wt=15): 11593 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(11026(a,1),8611(a,1,2,2)),rewrite(561(3,R),2(3),2(5),5117(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))]. Low Water (keep, True_semantics): wt=57 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): 11820 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [back_rewrite(7311),rewrite(11591(8),11062(6)),flip(a)]. given #252 (F,wt=15): 11825 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x # label(false). [para(11028(a,1),9(a,1,2))]. given #253 (F,wt=15): 11826 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x # label(false). [para(11028(a,1),12(a,1,2)),rewrite(2(2),2(4))]. given #254 (F,wt=15): 11827 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))) # label(false). [para(11028(a,1),8(a,2)),rewrite(900(5)),flip(a)]. Low Water (keep, True_semantics): wt=53 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))]. Low Water (keep, True_semantics): wt=51 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))]. given #260 (F,wt=15): 12019 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)) # label(false). [para(11028(a,2),1057(a,2,2)),rewrite(2(4),900(10),1468(9)),flip(a)]. given #261 (F,wt=15): 12560 f(f(x,f(y,z)),f(y,f(y,f(x,z)))) = x # label(false). [para(11046(a,1),9(a,1,2))]. Low Water (keep, False_semantics): wt=25 given #262 (F,wt=15): 12561 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label(false). [para(11046(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #263 (F,wt=15): 12661 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)) # label(false). [para(11046(a,1),1057(a,2,2)),rewrite(2(4),900(10),1468(9),2(3)),flip(a)]. Low Water (keep, True_semantics): wt=47 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(v,z)))))) = f(x,f(u,f(f(x,z),f(v,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))]. Low Water (keep, True_semantics): wt=45 given #269 (F,wt=15): 14329 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),11062(a,1,2,2,2)),rewrite(11062(5)),flip(a)]. given #270 (F,wt=15): 14865 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0 # label(false). [para(11063(a,1),2903(a,1,2,2,2,2)),rewrite(3313(8),3659(10))]. given #271 (F,wt=15): 16770 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(11820(a,1),2(a,2)),rewrite(2(3),2(4)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 45.49 (+ 0.08) seconds: "Sheffer". % Length of proof is 94. % Level of proof is 25. % Maximum clause weight is 43. % 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(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(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # answer("Sheffer"). [deny(1)]. 5 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # 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(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # 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,v)))))) = f(f(x,y),f(u,f(x,f(y,v)))). [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(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # 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(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # 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(c4,f(c4,c5)),f(c4,f(c4,c6))) != f(c_0,f(c4,f(c5,c6))) # 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))]. 4882 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))]. 4910 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))]. 5678 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),4882(8)),flip(a)]. 5791 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))]. 7311 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),4910(a,1,2,2,2)),rewrite(561(5,R),2(4))]. 7375 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(4910(a,1),647(a,1,1)),rewrite(2(8),4910(17))]. 7679 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),5678(a,1,2,2,2)),rewrite(561(3,R),2(3),2(5))]. 8128 f(f(x,x),f(f(y,y),f(x,z))) = f(y,f(y,x)) # label(false). [para(4910(a,1),5791(a,1,1)),rewrite(2(8),2(15),191(15),561(11,R),2(11),554(11),2(9),7375(11)),flip(a)]. 8910 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)]. 10732 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),8910(a,1,1)),rewrite(561(3,R),2(3),561(7,R),2(7),561(10,R),2(10)),flip(a)]. 11026 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [back_rewrite(7679),rewrite(10732(7))]. 11062 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(11026(a,2),8(a,1,2)),rewrite(2(2))]. 11591 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(8128(a,1),11026(a,1,2,2)),rewrite(173(13),2(12),2(14),173(15,R),561(13,R),2(12),2(13)),flip(a)]. 11820 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [back_rewrite(7311),rewrite(11591(8),11062(6)),flip(a)]. 14329 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),11062(a,1,2,2,2)),rewrite(11062(5)),flip(a)]. 16770 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(11820(a,1),2(a,2)),rewrite(2(3),2(4)),flip(a)]. 19005 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))) # label(false). [para(14329(a,1),16770(a,1,2)),rewrite(2(3),581(5)),flip(a)]. 19006 $F # answer("Sheffer"). [resolve(19005,a,571,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=271. Generated=282895. Kept=19003. proofs=1. Usable=221. Sos=11945. Demods=10781. Limbo=160, Disabled=6679. Hints=0. Weight_deleted=22. Literals_deleted=0. Forward_subsumed=263117. Back_subsumed=1758. Sos_limit_deleted=753. Sos_displaced=0. Sos_removed=0. New_demodulators=17009 (5 lex), Back_demodulated=4917. Back_unit_deleted=1. Demod_attempts=5707962. Demod_rewrites=1382457. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=20.98. User_CPU=45.49, System_CPU=0.08, Wall_clock=46. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 28115 exit (max_proofs) Fri Apr 13 09:59:10 2007