============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4414 was started by mccune on cleo.thornwood, Wed Nov 22 12:04:19 2006 The command was "/home/mccune/bin/prover9 -f BA2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA2.in set(lex_order_vars). set(restrict_denials). assign(new_constants,1). assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_minutes,5). % assign(max_minutes, 5) -> assign(max_seconds, 300). 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. ============================== 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(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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, 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. restricted denial: (wt=43): 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). [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). [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). [assumption]. given #3 (F,wt=11): 6 f(f(x,y),f(y,f(x,z))) = y. [para(2(a,1),3(a,1,1))]. given #4 (F,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))]. restricted denial: (wt=34): 16 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(14(7)),xx(a)]. given #5 (F,wt=9): 14 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. given #6 (T,wt=11): 9 f(f(x,y),f(x,f(z,y))) = x. [para(6(a,1),3(a,1,2,2)),rewrite(2(4))]. given #7 (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 #8 (F,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 (F,wt=11): 12 f(f(x,y),f(y,f(z,x))) = y. [para(6(a,1),6(a,1,2,2)),rewrite(2(2),2(3),2(4))]. given #10 (F,wt=11): 21 f(x,f(y,f(x,x))) = f(x,x). [para(14(a,1),14(a,1,1)),rewrite(2(2))]. given #11 (F,wt=9): 36 f(f(x,y),f(y,y)) = y. [para(21(a,1),6(a,1,2))]. given #12 (T,wt=13): 18 f(x,f(f(x,y),f(x,y))) = f(x,y). [para(3(a,1),14(a,1,2)),rewrite(2(4))]. given #13 (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 #14 (F,wt=13): 22 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite(2(4))]. given #15 (F,wt=13): 24 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(6(a,1),9(a,1,2)),rewrite(2(4))]. given #16 (F,wt=13): 33 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 #17 (F,wt=13): 34 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 #18 (T,wt=13): 73 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(2(a,1),33(a,1,2,1)),rewrite(2(2),2(3),2(5))]. given #19 (A,wt=15): 13 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 #20 (F,wt=15): 17 f(x,f(f(x,x),f(y,f(x,z)))) = f(x,x). [para(14(a,1),3(a,1,1)),rewrite(2(3))]. given #21 (F,wt=13): 87 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(11(a,1),17(a,1,2))]. given #22 (F,wt=15): 19 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(14(a,1),6(a,1,1)),rewrite(2(3))]. given #23 (F,wt=15): 30 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): 48 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(11(a,1),9(a,1,2))]. given #25 (A,wt=19): 23 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 #26 (F,wt=11): 126 f(x,f(y,f(x,y))) = f(x,x). [para(48(a,1),73(a,1,2)),flip(a)]. given #27 (F,wt=11): 144 f(x,f(y,f(y,x))) = f(x,x). [para(126(a,1),2(a,2)),rewrite(2(1),2(3))]. given #28 (F,wt=15): 56 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),22(a,1,2,2)),rewrite(2(3))]. restricted denial: (wt=34): 199 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(16),rewrite(191(27),191(32))]. given #29 (F,wt=11): 191 f(x,f(y,y)) = f(x,f(x,y)). [para(126(a,1),56(a,1,2)),rewrite(2(3))]. given #30 (T,wt=11): 200 f(x,f(y,y)) = f(x,f(y,x)). [para(191(a,1),2(a,2)),rewrite(2(2),2(3))]. given #31 (A,wt=21): 25 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 #32 (F,wt=11): 203 f(x,f(x,f(y,y))) = f(y,x). [para(191(a,1),9(a,1)),rewrite(2(2),200(2,R),2(4),200(4,R),2(6),6(6),2(3))]. given #33 (F,wt=11): 206 f(x,f(y,f(y,x))) = f(x,x). [para(191(a,1),36(a,1,1)),rewrite(14(5),2(3))]. given #34 (F,wt=15): 58 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y. [para(6(a,1),22(a,1,2,1)),rewrite(2(4),6(10))]. given #35 (F,wt=15): 59 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(6(a,1),22(a,1,2,2)),rewrite(2(3))]. given #36 (T,wt=15): 67 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x. [para(3(a,1),24(a,1,2,1)),rewrite(2(4),3(10))]. given #37 (A,wt=31): 26 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 #38 (F,wt=15): 69 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x. [para(9(a,1),24(a,1,2,1)),rewrite(2(4),9(10))]. given #39 (F,wt=15): 113 f(f(x,y),f(x,f(z,f(x,f(u,y))))) = x. [para(6(a,1),48(a,1,2,2)),rewrite(2(6))]. given #40 (F,wt=15): 197 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x. [back_rewrite(148),rewrite(191(5),2(6))]. given #41 (F,wt=15): 198 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x. [back_rewrite(38),rewrite(191(5))]. given #42 (T,wt=15): 201 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x. [para(191(a,1),3(a,1,1)),rewrite(2(4))]. given #43 (A,wt=21): 27 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 #44 (F,wt=15): 216 f(x,f(f(x,f(x,y)),f(y,y))) = f(x,x). [para(191(a,1),126(a,1,2,2)),rewrite(2(4))]. given #45 (F,wt=15): 218 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x). [back_rewrite(190),rewrite(200(6,R),2(4))]. restricted denial: (wt=23): 625 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(199),unit_del(a,613)]. given #46 (F,wt=11): 613 f(x,f(y,f(y,y))) = f(x,x). [para(218(a,1),59(a,1)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(638)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, f ]). restricted denial: (wt=19): 750 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer"). [back_rewrite(625),rewrite(736(11,R),2(7)),flip(a)]. given #47 (F,wt=7): 686 f(x,f(x,x)) = c_0. [new_symbol(638)]. given #48 (T,wt=7): 728 f(c_0,f(x,x)) = x. [back_rewrite(630),rewrite(686(3),2(3))]. given #49 (A,wt=21): 29 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 #50 (F,wt=7): 736 f(x,c_0) = f(x,x). [back_rewrite(613),rewrite(686(2))]. given #51 (F,wt=9): 824 f(f(x,x),f(c_0,c_0)) = c_0. [para(728(a,1),200(a,2,2)),rewrite(2(7),686(7))]. given #52 (F,wt=11): 720 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(644),rewrite(686(3),2(3))]. given #53 (F,wt=9): 875 f(f(x,y),f(c_0,c_0)) = c_0. [para(87(a,1),720(a,1,2)),rewrite(736(7,R),2(5),686(5),2(6)),flip(a)]. given #54 (T,wt=11): 730 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(628),rewrite(686(4),2(4),686(7))]. given #55 (A,wt=27): 31 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 #56 (F,wt=11): 811 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(686(a,1),7(a,1,2,1)),rewrite(2(3),21(4),686(7))]. given #57 (F,wt=11): 822 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(728(a,1),48(a,1,2)),rewrite(2(3),736(3),200(3),2(2),2(5))]. given #58 (F,wt=11): 832 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(728(a,1),69(a,1,2)),rewrite(2(5),736(5),2(5))]. given #59 (F,wt=11): 880 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(720(a,1),203(a,2)),rewrite(2(8),730(8),2(5))]. given #60 (T,wt=11): 954 f(c_0,f(x,f(y,f(y,x)))) = x. [para(811(a,1),12(a,1,2)),rewrite(200(2),2(1),2(3),2(5))]. given #61 (A,wt=19): 35 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(21(a,1),6(a,1,1)),rewrite(2(5))]. given #62 (F,wt=11): 990 f(x,f(c_0,f(y,x))) = f(y,x). [para(832(a,1),200(a,2,2)),rewrite(736(6,R),2(6),728(6),2(4),2(9),880(9))]. given #63 (F,wt=11): 1021 f(x,f(y,f(y,x))) = f(x,x). [para(35(a,1),67(a,1,1)),rewrite(200(2),2(1),14(6),2(4),14(5),2(3))]. given #64 (F,wt=13): 869 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(7(a,1),720(a,1,2)),rewrite(2(2),736(2),2(3),736(3),736(3,R),2(3),728(3),2(2),736(2)),flip(a)]. given #65 (F,wt=13): 972 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(87(a,1),822(a,1,2,2,2)),rewrite(686(6),2(7))]. given #66 (T,wt=13): 989 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(87(a,1),832(a,1,2,2)),rewrite(736(7,R),2(5),728(8),2(6))]. given #67 (A,wt=19): 37 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,y)))))) = y. [para(36(a,1),7(a,1,2,1)),rewrite(2(4),36(11))]. given #68 (F,wt=13): 1082 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(869(a,1),822(a,1,2,2,2)),rewrite(2(7),686(7),2(8))]. given #69 (F,wt=13): 1083 f(f(c_0,c_0),f(f(x,y),f(z,z))) = c_0. [para(2(a,1),972(a,1,2))]. given #70 (F,wt=15): 221 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x. [para(200(a,2),9(a,1,2,2))]. given #71 (F,wt=15): 265 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x. [para(203(a,2),3(a,1,2,2))]. given #72 (T,wt=15): 266 f(f(x,y),f(y,f(z,f(z,f(x,x))))) = y. [para(203(a,2),6(a,1,2,2))]. given #73 (A,wt=19): 40 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 #74 (F,wt=15): 268 f(x,f(x,f(y,f(y,f(x,x))))) = f(x,y). [para(203(a,2),8(a,1,2,2))]. given #75 (F,wt=15): 273 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)). [para(203(a,1),11(a,1,2,1,2)),rewrite(23(6)),flip(a)]. given #76 (F,wt=15): 300 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x. [para(206(a,1),12(a,1,2,2)),rewrite(2(3))]. given #77 (F,wt=15): 305 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(3(a,1),58(a,1,2,2,2,2)),rewrite(2(2),2(3))]. given #78 (T,wt=15): 306 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x. [para(6(a,1),58(a,1,2,2,2,2)),rewrite(2(2),2(3))]. given #79 (A,wt=23): 41 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 #80 (F,wt=15): 319 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y. [para(58(a,1),19(a,1,2,1)),rewrite(200(5),2(3),58(12))]. given #81 (F,wt=15): 340 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x). [para(48(a,1),59(a,1,2)),flip(a)]. given #82 (F,wt=15): 495 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x). [para(6(a,1),198(a,1,2,2,2,2)),rewrite(6(4),2(2),200(3,R))]. given #83 (F,wt=15): 596 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x). [para(14(a,1),218(a,1,2,1)),rewrite(2(2))]. given #84 (T,wt=15): 712 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [back_rewrite(656),rewrite(686(3),686(5),2(5),686(10))]. given #85 (A,wt=33): 42 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 #86 (F,wt=15): 734 f(f(x,x),f(f(x,y),f(x,f(x,z)))) = c_0. [back_rewrite(615),rewrite(686(8))]. given #87 (F,wt=13): 1815 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(8(a,1),734(a,1,2,2))]. given #88 (F,wt=13): 1849 f(f(c_0,c_0),f(f(x,y),f(x,z))) = c_0. [para(1815(a,1),10(a,1,2,2)),rewrite(2(8),200(9,R),2(7),1815(12))]. given #89 (F,wt=13): 1867 f(f(c_0,c_0),f(f(x,y),f(y,z))) = c_0. [para(2(a,1),1849(a,1,2,1))]. given #90 (T,wt=15): 744 f(c_0,f(x,f(y,f(y,f(z,f(x,x)))))) = x. [back_rewrite(445),rewrite(686(2))]. given #91 (A,wt=31): 43 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 #92 (F,wt=15): 784 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(285),rewrite(200(2),2(1),736(5,R),2(5))]. given #93 (F,wt=13): 2037 f(f(x,x),f(y,f(y,f(x,z)))) = x. [para(3(a,1),784(a,1,2,2)),rewrite(2(5),736(5),2(5),3(9))]. given #94 (F,wt=13): 2039 f(f(x,f(x,f(y,z))),f(z,z)) = z. [para(6(a,1),784(a,1,2,2)),rewrite(2(5),736(5),6(9))]. given #95 (F,wt=15): 820 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(728(a,1),30(a,1,1)),rewrite(2(4))]. given #96 (T,wt=15): 821 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(728(a,1),48(a,1,1,2,2)),rewrite(2(6))]. given #97 (A,wt=17): 44 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 #98 (F,wt=15): 835 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x. [para(7(a,1),29(a,1,2,2,2,2)),rewrite(3(5),736(4,R),2(4),3(11))]. given #99 (F,wt=15): 840 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [para(29(a,1),30(a,1,2,2)),rewrite(2(2),736(5,R),2(5))]. given #100 (F,wt=13): 2338 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(840(a,1),972(a,1,2,1))]. given #101 (F,wt=15): 887 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(875(a,1),7(a,1,2,1)),rewrite(2(7),200(7),2(5),736(5),686(5),2(5),875(13))]. given #102 (T,wt=15): 964 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0. [para(3(a,1),822(a,1,2,2,2)),rewrite(2(5))]. given #103 (A,wt=31): 49 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 #104 (F,wt=15): 965 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0. [para(9(a,1),822(a,1,2,2,2)),rewrite(2(5))]. given #105 (F,wt=15): 984 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0. [para(201(a,1),822(a,1,2,2,2)),rewrite(200(2),2(1),2(7),8(7))]. given #106 (F,wt=15): 993 f(x,f(c_0,f(f(x,f(x,y)),f(y,y)))) = c_0. [para(216(a,1),832(a,1,2,2)),rewrite(736(9,R),2(6),728(9),2(7))]. given #107 (F,wt=15): 994 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0. [para(218(a,1),832(a,1,2,2)),rewrite(736(9,R),2(6),728(9),2(7))]. given #108 (T,wt=15): 995 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(29(a,1),832(a,1,2)),rewrite(2(4),736(4),728(4),2(8),736(8),728(8),736(9,R),2(6),2(8),736(8),2(8))]. given #109 (A,wt=39): 50 f(x,f(f(y,f(x,z)),f(x,f(u,f(f(x,z),f(v,f(x,f(z,w)))))))) = f(x,f(u,f(f(x,z),f(v,f(x,f(z,w)))))). [para(7(a,1),11(a,1,2,2,2)),rewrite(2(6),2(10),2(17))]. given #110 (F,wt=15): 996 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [para(11(a,1),880(a,1,2)),rewrite(880(5),2(6),736(6),2(7)),flip(a)]. given #111 (F,wt=13): 2895 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(6(a,1),996(a,1,2,2)),rewrite(736(3,R),2(3),2(6),736(6),2(6),6(10))]. given #112 (F,wt=15): 998 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y). [para(23(a,1),880(a,1,2)),rewrite(880(5),2(6),736(6),2(7)),flip(a)]. given #113 (F,wt=15): 1058 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x. [para(201(a,1),990(a,1,2,2)),rewrite(200(2),2(1),2(5),736(5),2(5),14(5),200(4),2(3)),flip(a)]. given #114 (T,wt=15): 1065 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x). [para(14(a,1),869(a,1,1)),rewrite(2(3))]. given #115 (A,wt=41): 54 f(x,f(f(y,f(x,f(z,u))),f(x,f(v,f(f(x,f(z,u)),f(w,f(x,z))))))) = f(x,f(v,f(f(x,f(z,u)),f(w,f(x,z))))). [para(11(a,1),11(a,1,2,2,2)),rewrite(2(6),2(11),2(18))]. given #116 (F,wt=15): 1066 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x. [para(869(a,1),9(a,1,2,2)),rewrite(2(7))]. given #117 (F,wt=15): 1067 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y. [para(869(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. given #118 (F,wt=15): 1123 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x). [para(37(a,1),218(a,1,2,2,2)),rewrite(736(3,R),2(3),2(5))]. given #119 (F,wt=15): 1131 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(1082(a,1),11(a,1,2,2,2)),rewrite(2(11),736(14),2(14),1084(15),2(9)),flip(a)]. given #120 (T,wt=15): 1145 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x. [para(19(a,1),221(a,1,1,2)),rewrite(2(8),35(8))]. given #121 (A,wt=17): 55 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x. [para(22(a,1),3(a,1,1)),rewrite(2(5))]. given #122 (F,wt=15): 1209 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x). [para(265(a,1),218(a,1,2,2,2)),rewrite(736(3,R),2(3),2(5))]. given #123 (F,wt=15): 1324 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))). [para(273(a,1),200(a,1,2)),rewrite(200(2),2(1),8(3),2(2),736(3,R),2(3),200(6),2(5),8(7),2(6))]. given #124 (F,wt=15): 1329 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)). [para(273(a,1),203(a,1,2,2)),rewrite(200(2),2(1),8(3),2(2),736(3,R),2(3),200(7),2(6),8(8),2(7))]. given #125 (F,wt=15): 1587 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)). [para(340(a,1),56(a,1,2)),rewrite(200(2),2(1),2(3)),flip(a)]. given #126 (T,wt=15): 1642 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x). [para(2(a,1),596(a,1,2)),rewrite(200(2),2(1),2(4))]. given #127 (A,wt=23): 57 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(22(a,1),6(a,1,1)),rewrite(2(6))]. given #128 (F,wt=15): 1651 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)). [para(596(a,1),56(a,1,2)),rewrite(200(2),2(1)),flip(a)]. given #129 (F,wt=15): 1660 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0. [para(596(a,1),832(a,1,2,2)),rewrite(736(9,R),2(6),728(9),2(7))]. given #130 (F,wt=15): 1663 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x). [para(596(a,1),40(a,1)),rewrite(736(6,R),2(5)),flip(a)]. given #131 (F,wt=15): 1845 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(3(a,1),1815(a,1,2,1)),rewrite(736(3,R),2(3),2(5),2(7))]. given #132 (T,wt=13): 4441 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(6(a,1),1845(a,1,1,2,2)),rewrite(2(2),6(8),2(5),736(5),2(5))]. given #133 (A,wt=23): 60 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(y,v))))))) = f(x,y). [para(22(a,1),7(a,1,2,1)),rewrite(2(5),22(13))]. given #134 (F,wt=15): 1847 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [para(6(a,1),1815(a,1,2,1)),rewrite(736(3,R),2(3),2(5),2(7))]. given #135 (F,wt=15): 1903 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0. [para(744(a,1),9(a,1,2)),rewrite(200(3),2(2),2(7))]. given #136 (F,wt=15): 1905 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x). [para(744(a,1),36(a,1,1)),rewrite(736(11,R),2(7),744(7)),flip(a)]. given #137 (F,wt=15): 1909 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(744(a,1),67(a,1,2)),rewrite(200(4),2(3),2(6),2(8))]. given #138 (T,wt=15): 2034 f(f(x,f(y,f(y,z))),f(x,f(z,u))) = x. [para(784(a,1),3(a,1,2,2))]. given #139 (A,wt=23): 61 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),22(a,1,2,1)),rewrite(2(7),7(15))]. given #140 (F,wt=15): 2135 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x. [para(2037(a,1),9(a,1,2,2)),rewrite(2(6))]. given #141 (F,wt=15): 2136 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y. [para(2037(a,1),12(a,1,2,2)),rewrite(2(4),2(5),2(6))]. given #142 (F,wt=15): 2151 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(2037(a,1),832(a,1,2,2)),rewrite(736(7,R),2(5),2(7),736(7),2(7))]. given #143 (F,wt=15): 2167 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x. [para(2039(a,1),3(a,1,2,2)),rewrite(2(6))]. given #144 (T,wt=15): 2169 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y. [para(2039(a,1),6(a,1,2,2)),rewrite(2(4),2(5),2(6))]. given #145 (A,wt=31): 63 f(x,f(f(y,f(x,z)),f(x,f(u,f(f(x,z),f(z,v)))))) = f(x,f(u,f(f(x,z),f(z,v)))). [para(22(a,1),11(a,1,2,2,2)),rewrite(2(4),2(8),2(13))]. given #146 (F,wt=15): 2172 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x). [para(14(a,1),2039(a,1,2)),rewrite(200(2),2(1),2(5))]. given #147 (F,wt=15): 2206 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(2039(a,1),730(a,1,2,2)),rewrite(736(7,R),2(5),2(7),736(7),2(7))]. given #148 (F,wt=15): 2351 f(f(c_0,c_0),f(x,f(f(y,z),f(u,v)))) = c_0. [para(2338(a,1),11(a,1,2,2,2)),rewrite(2(10),736(13),2(13),1084(14),2(8)),flip(a)]. given #149 (F,wt=15): 2360 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(2(a,1),964(a,1,1)),rewrite(2(2),2(4),200(5,R))]. given #150 (T,wt=15): 2362 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0. [para(3(a,1),964(a,1,1,2))]. given #151 (A,wt=27): 64 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),22(a,1,2,1)),rewrite(2(8),11(16))]. given #152 (F,wt=15): 2370 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(33(a,1),964(a,1,1))]. given #153 (F,wt=15): 2380 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(200(a,1),964(a,1,2,2,2)),rewrite(2(2),2(5),8(7))]. given #154 (F,wt=15): 2512 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(2(a,1),965(a,1,1)),rewrite(2(2),2(4),200(5,R))]. given #155 (F,wt=15): 2553 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0. [para(2(a,1),984(a,1,1)),rewrite(2(3),2(5))]. given #156 (T,wt=15): 2620 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(730(a,1),984(a,1,1,2,2)),rewrite(2(3),728(3))]. given #157 (A,wt=19): 65 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y). [para(22(a,1),22(a,1,2,1)),rewrite(2(5),22(11))]. given #158 (F,wt=15): 2721 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0. [para(3(a,1),994(a,1,2,2,2,2)),rewrite(736(4,R),2(4),2(6))]. given #159 (F,wt=15): 2723 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0. [para(6(a,1),994(a,1,2,2,2,2)),rewrite(736(4,R),2(4),2(6))]. given #160 (F,wt=15): 2903 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(2895(a,1),9(a,1,2,2)),rewrite(2(7))]. given #161 (F,wt=15): 2905 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y. [para(2895(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. given #162 (T,wt=15): 2936 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x). [para(21(a,1),998(a,1,2,2)),rewrite(200(2),2(1),200(4),2(3),736(5,R),2(4),728(8),2(6),200(8),2(7),1021(9))]. given #163 (A,wt=17): 66 f(f(x,y),f(y,f(z,f(f(x,y),f(x,u))))) = y. [para(24(a,1),3(a,1,1)),rewrite(2(5))]. given #164 (F,wt=15): 3158 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x. [para(6(a,1),1066(a,1,2,2,2,2)),rewrite(2(4),736(4))]. given #165 (F,wt=15): 3346 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x). [para(73(a,1),1123(a,1,2,2)),rewrite(2(4),736(4))]. given #166 (F,wt=15): 3399 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(1815(a,1),1123(a,1,2,1)),rewrite(880(9),736(9,R),2(9),728(9))]. given #167 (F,wt=15): 3669 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(1324(a,1),820(a,1,2,2))]. given #168 (T,wt=15): 3761 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)). [para(1587(a,1),2(a,2)),rewrite(2(1),2(4),2(5),200(6,R))]. given #169 (A,wt=23): 68 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(24(a,1),6(a,1,1)),rewrite(2(6))]. given #170 (F,wt=15): 3821 f(x,f(x,f(y,f(z,f(x,x))))) = f(x,y). [para(596(a,1),1587(a,1,2,2)),rewrite(2(5),14(5)),flip(a)]. given #171 (F,wt=15): 3858 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(1587(a,1),1324(a,2,2)),rewrite(8(9))]. given #172 (F,wt=15): 3883 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [back_rewrite(2595),rewrite(2(4),200(5,R),2(6),200(7,R),2(9),200(10,R),736(8,R),2(8),728(8),2(6),2(7))]. given #173 (F,wt=15): 3943 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). [para(1642(a,1),40(a,1)),flip(a)]. given #174 (T,wt=15): 4106 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)). [para(1651(a,1),2(a,2)),rewrite(200(2),2(1),2(4),2(5),200(6,R))]. given #175 (A,wt=23): 70 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),24(a,1,2,1)),rewrite(2(9),7(15))]. given #176 (F,wt=15): 4332 f(x,f(c_0,f(y,f(z,f(x,x))))) = f(x,y). [para(1651(a,1),1324(a,2,2)),rewrite(8(9))]. given #177 (F,wt=15): 4344 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0. [para(2(a,1),1660(a,1,2,2)),rewrite(200(3),2(2),2(5))]. given #178 (F,wt=15): 4350 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(1067(a,1),1660(a,1,2,2,2)),rewrite(2(6))]. given #179 (F,wt=15): 4353 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x). [para(1663(a,1),2(a,2)),rewrite(2(2),2(6))]. given #180 (T,wt=15): 4391 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0. [para(1663(a,1),832(a,1,2,2)),rewrite(2(2),2(7),736(11,R),2(7),728(10),2(8))]. given #181 (A,wt=27): 71 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),24(a,1,2,1)),rewrite(2(9),2(10),11(16))]. given #182 (F,wt=15): 4414 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0. [para(1663(a,1),993(a,1,2,2,1,2)),rewrite(686(3),736(13,R),2(9),880(10))]. given #183 (F,wt=15): 5243 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z). [para(37(a,1),2169(a,1,2)),rewrite(200(2),2(1),2(3),2(5),2(6))]. given #184 (F,wt=15): 6052 f(x,f(c_0,f(f(x,f(y,z)),f(z,z)))) = c_0. [para(6(a,1),2721(a,1,2,2,2,2)),rewrite(2(5),736(5))]. given #185 (F,wt=15): 6533 f(x,f(c_0,f(y,f(y,f(z,f(x,y)))))) = c_0. [para(48(a,1),3669(a,1,2,2,2)),rewrite(2(2),2(5))]. given #186 (T,wt=15): 6777 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(3858(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. given #187 (A,wt=19): 72 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y). [para(22(a,1),24(a,1,2,1)),rewrite(2(7),22(11))]. given #188 (F,wt=15): 6895 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x). [para(3943(a,1),2(a,2)),rewrite(2(1),2(5))]. given #189 (F,wt=15): 6911 f(x,f(c_0,f(y,f(y,f(z,f(y,x)))))) = c_0. [para(3943(a,1),832(a,1,2,2)),rewrite(2(1),2(5),736(9,R),2(6),728(9),2(7))]. given #190 (F,wt=15): 6944 f(x,f(y,f(z,f(x,x)))) = f(x,f(y,y)). [para(4106(a,2),2(a,2)),rewrite(2(2),2(3),200(4,R)),flip(a)]. given #191 (F,wt=15): 7267 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(y,x). [para(4332(a,1),2(a,2)),rewrite(200(3),2(2),2(6),2(7))]. given #192 (T,wt=17): 202 f(f(x,f(x,y)),f(f(x,z),f(y,y))) = f(y,y). [para(191(a,1),6(a,1,1)),rewrite(2(5))]. given #193 (A,wt=19): 74 f(f(f(x,y),f(x,z)),f(f(x,z),f(z,u))) = f(x,z). [para(33(a,1),24(a,1,2,1)),rewrite(33(11))]. given #194 (F,wt=17): 209 f(x,f(y,f(f(x,y),f(y,z)))) = f(x,f(x,y)). [para(22(a,1),191(a,2,2)),rewrite(195(7))]. given #195 (F,wt=17): 223 f(x,f(f(x,y),f(f(x,x),f(y,z)))) = f(x,y). [para(200(a,2),7(a,1,2,2)),rewrite(2(4))]. given #196 (F,wt=17): 247 f(f(x,f(y,y)),f(f(y,x),f(x,z))) = f(y,x). [para(22(a,1),25(a,1,2,2,2,2)),rewrite(2(2),200(2,R),2(5),200(5,R),2(7),6(7),2(4))]. given #197 (F,wt=17): 277 f(x,f(f(y,z),f(y,f(y,f(x,x))))) = f(x,y). [para(203(a,2),22(a,1,2,1)),rewrite(2(5))]. given #198 (T,wt=17): 308 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(58(a,1),9(a,1,2)),rewrite(2(6))]. given #199 (A,wt=23): 76 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(v,y))))))) = f(x,y). [para(34(a,1),7(a,2)),rewrite(2(2),2(3),73(4),2(3),2(4),2(5),2(10))]. given #200 (F,wt=17): 549 f(f(x,f(y,z)),f(f(x,u),f(y,z))) = f(y,z). [para(67(a,1),27(a,1,2,2,2)),rewrite(2(4),2(5))]. given #201 (F,wt=17): 608 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)). [para(218(a,1),56(a,1,2)),flip(a)]. given #202 (F,wt=17): 688 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)). [back_rewrite(666),rewrite(686(7),2(7),26(10))]. given #203 (F,wt=17): 743 f(c_0,f(x,f(y,f(y,f(f(x,x),f(z,u)))))) = x. [back_rewrite(455),rewrite(686(2))]. given #204 (T,wt=17): 795 f(f(x,y),f(y,f(y,f(x,z)))) = f(c_0,f(x,y)). [back_rewrite(147),rewrite(736(8,R),2(8))]. given #205 (A,wt=31): 77 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(34(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 #206 (F,wt=17): 796 f(f(x,y),f(x,f(x,f(y,z)))) = f(c_0,f(x,y)). [back_rewrite(145),rewrite(736(8,R),2(8))]. given #207 (F,wt=17): 1070 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(11(a,1),869(a,1,2,2)),rewrite(736(7,R),2(5),880(5))]. given #208 (F,wt=17): 1075 f(x,f(f(x,y),f(z,f(c_0,f(y,u))))) = f(x,y). [para(869(a,1),59(a,1,2,2,2)),rewrite(2(6),869(13))]. given #209 (F,wt=17): 1090 f(x,f(c_0,f(y,f(c_0,f(f(x,x),f(z,u)))))) = c_0. [para(989(a,1),22(a,1,2,1)),rewrite(2(7),989(15))]. given #210 (T,wt=17): 1404 f(f(x,f(x,y)),f(x,f(f(y,y),f(z,u)))) = x. [para(989(a,1),300(a,1,1,2,2)),rewrite(736(2),200(2),2(1),736(13,R),2(9),880(9))]. given #211 (A,wt=19): 78 f(x,f(f(x,y),f(z,f(f(x,y),f(u,y))))) = f(x,y). [para(34(a,1),22(a,2)),rewrite(2(2),2(3),73(4),2(3),2(4),2(5),2(8))]. given #212 (F,wt=17): 1767 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(880(a,1),42(a,1,2,1)),rewrite(2(9),736(9),2(10),996(10),2(6),2(12),736(12),2(13),996(13))]. given #213 (F,wt=17): 1811 f(f(c_0,f(x,y)),f(x,f(f(x,y),f(z,z)))) = c_0. [para(3(a,1),734(a,1,2,1)),rewrite(736(3,R),2(3),2(6),200(7,R))]. given #214 (F,wt=15): 10677 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0. [para(2039(a,1),1811(a,1,2,2)),rewrite(2(7))]. given #215 (F,wt=17): 1813 f(f(c_0,f(x,y)),f(y,f(f(x,y),f(z,z)))) = c_0. [para(6(a,1),734(a,1,2,1)),rewrite(736(3,R),2(3),2(6),200(7,R))]. given #216 (T,wt=17): 1851 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(1815(a,1),22(a,1,2,1)),rewrite(2(6),1815(13))]. given #217 (A,wt=19): 79 f(f(f(x,y),f(y,z)),f(f(y,z),f(z,u))) = f(y,z). [para(34(a,1),24(a,1,2,1)),rewrite(34(11))]. given #218 (F,wt=17): 1852 f(f(c_0,f(x,f(y,y))),f(f(y,z),f(y,u))) = c_0. [para(1815(a,1),24(a,1,2,1)),rewrite(2(6),2(8),1815(13))]. given #219 (F,wt=17): 1949 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)). [para(200(a,1),43(a,1,2,2)),rewrite(2(7),6(7),2(4),200(4,R),227(6),736(8,R),2(7)),flip(a)]. given #220 (F,wt=17): 2035 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)). [para(784(a,1),3(a,1,2)),rewrite(2(4),2(6))]. given #221 (F,wt=15): 11424 f(x,f(x,f(y,f(z,f(z,x))))) = f(y,x). [para(3821(a,1),2035(a,1,2,2)),rewrite(200(2),2(1),2(4),2(6),7310(8),200(3),2(2)),flip(a)]. given #222 (T,wt=15): 11448 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(247(a,1),2035(a,1,2,2,2)),rewrite(2(4),2(9),6(9),2(6),736(6),2(6),247(14),2(10),6(10))]. given #223 (A,wt=25): 81 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(v,f(x,f(x,y))))))))) = x. [para(13(a,1),7(a,1,2,1)),rewrite(2(7),13(17))]. given #224 (F,wt=17): 2062 f(f(x,y),f(c_0,f(z,f(y,y)))) = f(z,f(y,y)). [para(200(a,1),784(a,1,1,2)),rewrite(2(1),8(3),2(4),2(8))]. given #225 (F,wt=17): 2067 f(f(x,y),f(c_0,f(z,f(x,x)))) = f(z,f(x,x)). [para(203(a,1),784(a,1,1)),rewrite(2(4),2(8))]. given #226 (F,wt=17): 2144 f(x,f(f(x,y),f(z,f(z,f(y,u))))) = f(x,y). [para(2037(a,1),59(a,1,2,2,2)),rewrite(2(5),2037(11))]. given #227 (F,wt=17): 2185 f(x,f(f(x,y),f(z,f(z,f(u,y))))) = f(x,y). [para(2039(a,1),56(a,1,2,2,2)),rewrite(2(5),2039(11))]. given #228 (T,wt=17): 2236 f(f(x,f(x,f(y,f(y,f(z,u))))),f(u,u)) = u. [para(2039(a,1),784(a,1,2,2)),rewrite(2(7),736(7),2039(12))]. given #229 (A,wt=39): 82 f(f(x,y),f(f(x,z),f(f(x,y),f(u,f(x,f(v,f(x,f(x,y)))))))) = f(f(x,y),f(u,f(x,f(v,f(x,f(x,y)))))). [para(13(a,1),11(a,1,2,2,2)),rewrite(2(7),2(9),2(10),2(17))]. given #230 (F,wt=13): 12001 f(f(x,x),f(y,f(y,f(z,x)))) = x. [para(12(a,1),2236(a,1,1,2)),rewrite(2(2),2(3),2(5))]. given #231 (F,wt=17): 2566 f(f(x,x),f(f(y,x),f(z,f(z,f(x,x))))) = c_0. [para(36(a,1),984(a,1,2,2)),rewrite(2(7),736(7),2(7))]. given #232 (F,wt=17): 2645 f(f(x,y),f(c_0,f(x,f(f(y,z),f(y,u))))) = c_0. [para(1815(a,1),984(a,1,1,2,2)),rewrite(2(3),728(3))]. given #233 (F,wt=17): 2901 f(f(x,x),f(y,f(c_0,f(z,f(z,f(u,x)))))) = x. [para(2039(a,1),996(a,1,2,2)),rewrite(736(7,R),2(5),2(8),736(8),2(8),2039(13))]. given #234 (T,wt=17): 2913 f(x,f(f(x,y),f(z,f(c_0,f(u,y))))) = f(x,y). [para(2895(a,1),59(a,1,2,2,2)),rewrite(2(6),2895(13))]. given #235 (A,wt=19): 83 f(f(x,y),f(x,f(z,f(x,f(u,f(x,f(x,y))))))) = x. [para(13(a,1),22(a,1,2,1)),rewrite(2(6),13(14))]. given #236 (F,wt=17): 2934 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(x,u)))))) = x. [para(7(a,1),998(a,1,2)),rewrite(736(9,R),2(6),2(9),736(9),2(9),2(11),736(11),869(15))]. given #237 (F,wt=17): 2941 f(x,f(y,f(c_0,f(f(x,x),f(z,u))))) = f(x,x). [para(87(a,1),998(a,1,2,2)),rewrite(736(7,R),2(5),728(9),2(7),87(11))]. given #238 (F,wt=17): 2954 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(u,x)))))) = x. [para(29(a,1),998(a,1,2)),rewrite(2(4),736(4),728(4),2(8),736(8),728(8),736(9,R),2(6),2(9),736(9),2(9),2(11),736(11),2(14),736(14),728(14),2895(15))]. given #239 (F,wt=17): 2964 f(f(x,x),f(y,f(c_0,f(z,f(z,f(x,u)))))) = x. [para(2037(a,1),998(a,1,2,2)),rewrite(736(7,R),2(5),2(8),736(8),2(8),2037(13))]. given #240 (T,wt=17): 3163 f(x,f(f(y,x),f(z,f(c_0,f(y,u))))) = f(y,x). [para(1066(a,1),12(a,1,2)),rewrite(2(5),2(6),2(7),2(8))]. given #241 (A,wt=19): 90 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,x)))))) = x. [para(19(a,1),3(a,1,1)),rewrite(2(6))]. given #242 (F,wt=17): 3209 f(f(x,y),f(x,f(c_0,f(y,z)))) = f(c_0,f(x,y)). [para(1066(a,1),340(a,1,2,2)),rewrite(2(5),736(9,R),2(9))]. given #243 (F,wt=17): 3293 f(f(x,y),f(y,f(c_0,f(x,z)))) = f(c_0,f(x,y)). [para(1067(a,1),340(a,1,2,2)),rewrite(2(5),736(9,R),2(9))]. given #244 (F,wt=17): 3347 f(x,f(y,f(x,f(f(y,y),f(z,u))))) = f(x,x). [para(87(a,1),1123(a,1,2,2,2)),rewrite(728(7),2(5))]. given #245 (F,wt=17): 3435 f(f(c_0,c_0),f(x,f(y,f(z,f(c_0,f(u,v)))))) = c_0. [para(1131(a,1),11(a,1,2,2,2)),rewrite(2(12),736(15),2(15),2351(16),2(10)),flip(a)]. given #246 (T,wt=17): 3564 f(x,f(c_0,f(f(x,y),f(y,z)))) = f(x,f(x,y)). [para(22(a,1),1324(a,2,2))]. given #247 (A,wt=25): 92 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(v,f(x,x)))))))) = f(x,y). [para(19(a,1),7(a,1,2,1)),rewrite(2(6),19(15))]. Low Water (keep): wt=95, part=1.00, limit=89 given #248 (F,wt=17): 3570 f(x,f(c_0,f(f(x,y),f(z,y)))) = f(x,f(x,y)). [para(34(a,1),1324(a,2,2)),rewrite(2(3),2(4),2(7))]. given #249 (F,wt=17): 3775 f(x,f(f(y,f(x,x)),f(f(x,x),f(z,u)))) = c_0. [para(87(a,1),1587(a,1,2,2,2)),rewrite(2(6),87(11),686(9))]. given #250 (F,wt=17): 3784 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y). [para(200(a,1),1587(a,1,2,2,2)),rewrite(2(2),200(8),2(7),8(9))]. given #251 (F,wt=17): 3868 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)). [back_rewrite(3802),rewrite(3830(6))]. Low Water (keep): wt=79, part=0.98, limit=73 Low Water (keep): wt=75, part=0.98, limit=73 given #252 (T,wt=17): 3950 f(x,f(f(x,y),f(f(y,z),f(y,u)))) = f(x,x). [para(1815(a,1),1642(a,1,2,2,2,2)),rewrite(2(6),728(6),2(5))]. Low Water (keep): wt=73, part=0.96, limit=67 Low Water (keep): wt=69, part=0.96, limit=67 given #253 (A,wt=35): 93 f(x,f(f(y,f(x,z)),f(x,f(u,f(f(x,z),f(v,f(x,x))))))) = f(x,f(u,f(f(x,z),f(v,f(x,x))))). [para(19(a,1),11(a,1,2,2,2)),rewrite(2(5),2(9),2(15))]. Low Water (keep): wt=63, part=0.95, limit=63 given #254 (F,wt=17): 4478 f(f(c_0,f(x,f(y,y))),f(f(z,y),f(y,u))) = c_0. [para(4441(a,1),24(a,1,2,1)),rewrite(2(6),2(8),4441(13))]. given #255 (F,wt=17): 4503 f(x,f(f(x,y),f(f(z,y),f(y,u)))) = f(x,x). [para(4441(a,1),1642(a,1,2,2,2,2)),rewrite(2(6),728(6),2(5))]. given #256 (F,wt=17): 4825 f(f(x,y),f(x,f(z,f(f(y,u),f(y,v))))) = x. [para(1815(a,1),2034(a,1,1,2,2)),rewrite(2(3),728(3),2(5))]. Low Water (keep): wt=61, part=0.94, limit=61 given #257 (F,wt=17): 4988 f(x,f(f(y,f(y,f(z,u))),f(z,x))) = f(z,x). [para(2135(a,1),12(a,1,2)),rewrite(2(4),2(6),2(7))]. given #258 (T,wt=17): 5098 f(x,f(f(y,x),f(z,f(z,f(y,u))))) = f(y,x). [para(2136(a,1),9(a,1,2)),rewrite(2(6))]. given #259 (A,wt=21): 94 f(x,f(f(x,y),f(z,f(f(x,y),f(u,f(x,x)))))) = f(x,y). [para(19(a,1),22(a,1,2,1)),rewrite(2(6),19(13))]. Low Water (keep): wt=59, part=0.92, limit=59 given #260 (F,wt=17): 5206 f(x,f(f(y,f(y,f(z,u))),f(u,x))) = f(u,x). [para(2167(a,1),12(a,1,2)),rewrite(2(4),2(6),2(7))]. Low Water (keep): wt=57, part=0.92, limit=57 given #261 (F,wt=17): 5480 f(f(c_0,c_0),f(x,f(y,f(f(z,u),f(v,w))))) = c_0. [para(2351(a,1),11(a,1,2,2,2)),rewrite(2(11),736(14),2(14),2351(15),2(9)),flip(a)]. given #262 (F,wt=17): 5483 f(f(c_0,f(x,y)),f(f(x,x),f(z,u))) = f(x,y). [para(2351(a,1),42(a,1,2)),rewrite(2(5),880(5),2(7),736(7),2(7)),flip(a)]. given #263 (F,wt=17): 6111 f(x,f(c_0,f(y,f(x,f(f(y,y),f(z,u)))))) = c_0. [para(87(a,1),2723(a,1,2,2,2,2)),rewrite(728(8),2(6))]. given #264 (T,wt=17): 6140 f(x,f(f(y,x),f(z,f(c_0,f(u,y))))) = f(y,x). [para(2903(a,1),12(a,1,2)),rewrite(2(5),2(6),2(7),2(8))]. given #265 (A,wt=21): 96 f(x,f(f(x,y),f(z,f(x,f(u,f(x,f(y,v))))))) = f(x,y). [para(30(a,1),3(a,1,1)),rewrite(2(6))]. given #266 (F,wt=17): 6144 f(f(x,f(y,z)),f(x,f(f(y,y),f(u,v)))) = x. [para(87(a,1),2903(a,1,2,2,2,2)),rewrite(728(7),2(5),2(7))]. given #267 (F,wt=17): 6471 f(f(x,y),f(y,f(z,f(f(x,u),f(x,v))))) = y. [para(3399(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. Low Water (keep): wt=55, part=0.90, limit=55 given #268 (F,wt=17): 6519 f(x,f(c_0,f(f(x,y),f(f(y,z),f(y,u))))) = c_0. [para(3399(a,1),1660(a,1,2,2,2,2)),rewrite(2(6))]. Low Water (keep): wt=53, part=0.90, limit=53 given #269 (F,wt=17): 6778 f(f(x,y),f(c_0,f(f(x,z),f(x,f(y,u))))) = x. [para(3(a,1),3858(a,1,2,2,2,2)),rewrite(2(5),2(6),3(12))]. given #270 (T,wt=17): 6780 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,u))))) = y. [para(6(a,1),3858(a,1,2,2,2,2)),rewrite(2(5),2(6),6(12))]. Low Water (keep): wt=51, part=0.88, limit=51 given #271 (A,wt=27): 97 f(x,f(f(x,f(y,f(x,f(z,u)))),f(v,f(x,z)))) = f(x,f(y,f(x,f(z,u)))). [para(30(a,1),6(a,1,1)),rewrite(2(6))]. given #272 (F,wt=17): 6880 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)). [para(3346(a,1),3858(a,1,2,2,2)),rewrite(2(6),2909(8)),flip(a)]. Low Water (keep): wt=49, part=0.87, limit=49 given #273 (F,wt=15): 17176 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6172),rewrite(16698(7))]. Low Water (keep): wt=47, part=0.85, limit=47 given #274 (F,wt=15): 17196 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))). [para(17176(a,1),2(a,1)),rewrite(2(6),2(8))]. given #275 (F,wt=15): 17197 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))). [para(17176(a,1),2(a,2)),rewrite(2(4),2(6))]. given #276 (T,wt=15): 17205 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))). [para(17176(a,1),8(a,2)),rewrite(1329(5)),flip(a)]. given #277 (A,wt=25): 98 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(v,f(x,f(y,w))))))))) = x. [para(30(a,1),7(a,1,2,1)),rewrite(2(7),30(17))]. given #278 (F,wt=15): 17206 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))). [para(17176(a,2),8(a,2)),rewrite(1329(5),2(5)),flip(a)]. Low Water (keep): wt=45, part=0.85, limit=45 given #279 (F,wt=15): 17209 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x. [para(17176(a,1),9(a,1,2))]. given #280 (F,wt=15): 17210 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x. [para(17176(a,2),9(a,1,2)),rewrite(2(4))]. given #281 (F,wt=15): 17216 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x. [para(17176(a,1),12(a,1,2)),rewrite(2(2),2(4))]. given #282 (T,wt=15): 17217 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x. [para(17176(a,2),12(a,1,2)),rewrite(2(2))]. given #283 (A,wt=25): 99 f(f(x,y),f(x,f(z,f(x,f(u,f(f(x,y),f(v,f(x,f(y,w))))))))) = x. [para(7(a,1),30(a,1,1)),rewrite(2(7))]. Low Water (keep): wt=43, part=0.82, limit=43 given #284 (F,wt=15): 17427 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))). [para(17176(a,2),1324(a,1))]. given #285 (F,wt=15): 17429 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(17176(a,2),1324(a,2,2)),rewrite(880(5),2(4)),flip(a)]. given #286 (F,wt=15): 17460 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(17176(a,1),1845(a,1,1,2)),rewrite(2(9),880(11),2(8))]. given #287 (F,wt=15): 17613 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))). [para(17176(a,1),308(a,2)),rewrite(2(12),9151(15),2(5)),flip(a)]. given #288 (T,wt=15): 17673 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)). [para(17176(a,2),2035(a,2,2)),rewrite(2(4),1329(10),2337(9)),flip(a)]. given #289 (A,wt=19): 103 f(f(x,y),f(x,f(z,f(x,f(u,f(x,f(y,v))))))) = x. [para(30(a,1),22(a,1,2,1)),rewrite(2(6),30(14))]. given #290 (F,wt=15): 18194 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y). [back_rewrite(13203),rewrite(18164(12))]. given #291 (F,wt=15): 18201 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))). [para(17205(a,1),8(a,2)),rewrite(1329(5),2(4))]. given #292 (F,wt=15): 18208 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z. [para(17205(a,1),12(a,1,2)),rewrite(2(2),2(6))]. given #293 (F,wt=15): 18256 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))). [para(720(a,1),17205(a,2,2,2)),rewrite(2(5),17430(7),2137(6))]. given #294 (T,wt=15): 18375 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))). [para(17205(a,1),1324(a,1))]. given #295 (A,wt=19): 105 f(f(x,f(y,f(x,f(z,u)))),f(x,f(v,f(x,z)))) = x. [para(30(a,1),24(a,1,2,1)),rewrite(2(6),30(14))]. given #296 (F,wt=15): 18377 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)). [para(17205(a,1),1324(a,2,2)),rewrite(880(5),2(3)),flip(a)]. given #297 (F,wt=15): 18504 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(17205(a,2),4414(a,1,2,2,2,2)),rewrite(2116(11))]. given #298 (F,wt=15): 18587 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)). [para(17205(a,1),2035(a,2,2)),rewrite(2(4),1329(10),2337(9)),flip(a)]. given #299 (F,wt=15): 19278 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y. [para(17206(a,1),17209(a,1,1)),rewrite(736(7),728(7),2(5))]. given #300 (T,wt=15): 19582 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z. [para(17427(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #301 (A,wt=25): 110 f(x,f(f(x,f(y,f(x,z))),f(u,f(x,f(z,v))))) = f(x,f(y,f(x,z))). [para(48(a,1),3(a,1,1)),rewrite(2(6))]. given #302 (F,wt=15): 19770 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),17429(a,1,2,2,2)),rewrite(17429(5)),flip(a)]. given #303 (F,wt=15): 19779 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))). [para(200(a,1),17429(a,1,2,2,2)),rewrite(2(2),17429(6),200(5),2(4)),flip(a)]. given #304 (F,wt=15): 21504 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(18256(a,1),4414(a,1,2,2,2,2)),rewrite(2(4),5197(10))]. given #305 (F,wt=15): 22246 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(19770(a,1),6777(a,1,2,2,2)),rewrite(2(4),2036(8))]. ============================== PROOF ================================= % Proof 1 at 79.03 (+ 0.11) seconds: "Sheffer". % Length of proof is 77. % Level of proof is 25. % Maximum clause weight is 43. % Given clauses 305. 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). [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. [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. [para(6(a,1),3(a,1,2,2)),rewrite(2(4))]. 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. [para(6(a,1),6(a,1,2,2)),rewrite(2(2),2(3),2(4))]. 14 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. 16 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(14(7)),xx(a)]. 17 f(x,f(f(x,x),f(y,f(x,z)))) = f(x,x). [para(14(a,1),3(a,1,1)),rewrite(2(3))]. 19 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(14(a,1),6(a,1,1)),rewrite(2(3))]. 21 f(x,f(y,f(x,x))) = f(x,x). [para(14(a,1),14(a,1,1)),rewrite(2(2))]. 22 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite(2(4))]. 23 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))]. 24 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(6(a,1),9(a,1,2)),rewrite(2(4))]. 33 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))]. 35 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(21(a,1),6(a,1,1)),rewrite(2(5))]. 36 f(f(x,y),f(y,y)) = y. [para(21(a,1),6(a,1,2))]. 37 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,y)))))) = y. [para(36(a,1),7(a,1,2,1)),rewrite(2(4),36(11))]. 48 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(11(a,1),9(a,1,2))]. 56 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),22(a,1,2,2)),rewrite(2(3))]. 59 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(6(a,1),22(a,1,2,2)),rewrite(2(3))]. 73 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(2(a,1),33(a,1,2,1)),rewrite(2(2),2(3),2(5))]. 87 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(11(a,1),17(a,1,2))]. 126 f(x,f(y,f(x,y))) = f(x,x). [para(48(a,1),73(a,1,2)),flip(a)]. 144 f(x,f(y,f(y,x))) = f(x,x). [para(126(a,1),2(a,2)),rewrite(2(1),2(3))]. 164 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(x,y)),f(x,f(y,z))). [para(3(a,1),144(a,1,2,2)),rewrite(2(4),2(5)),flip(a)]. 190 f(x,f(f(x,f(y,z)),f(y,f(x,f(y,z))))) = f(x,x). [para(56(a,1),126(a,1,2,2)),rewrite(2(6))]. 191 f(x,f(y,y)) = f(x,f(x,y)). [para(126(a,1),56(a,1,2)),rewrite(2(3))]. 199 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(16),rewrite(191(27),191(32))]. 200 f(x,f(y,y)) = f(x,f(y,x)). [para(191(a,1),2(a,2)),rewrite(2(2),2(3))]. 203 f(x,f(x,f(y,y))) = f(y,x). [para(191(a,1),9(a,1)),rewrite(2(2),200(2,R),2(4),200(4,R),2(6),6(6),2(3))]. 218 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x). [back_rewrite(190),rewrite(200(6,R),2(4))]. 273 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)). [para(203(a,1),11(a,1,2,1,2)),rewrite(23(6)),flip(a)]. 285 f(f(x,f(y,y)),f(f(y,z),f(y,z))) = f(y,z). [para(203(a,2),19(a,1)),rewrite(2(10),35(10),2(7),200(7,R))]. 340 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x). [para(48(a,1),59(a,1,2)),flip(a)]. 596 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x). [para(14(a,1),218(a,1,2,1)),rewrite(2(2))]. 613 f(x,f(y,f(y,y))) = f(x,x). [para(218(a,1),59(a,1)),flip(a)]. 625 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(199),unit_del(a,613)]. 628 f(f(x,x),f(f(x,y),f(z,f(z,z)))) = f(z,f(z,z)). [para(613(a,1),6(a,1,1)),rewrite(2(5))]. 630 f(f(x,x),f(y,f(y,y))) = x. [para(613(a,2),14(a,1))]. 638 f(x,f(x,x)) = f(y,f(y,y)). [para(613(a,1),36(a,1,1)),rewrite(200(7),2(5),630(5),2(2))]. 644 f(x,f(f(x,y),f(z,f(z,z)))) = f(x,y). [para(613(a,2),24(a,1,2)),rewrite(2(1),2(6))]. 686 f(x,f(x,x)) = c_0. [new_symbol(638)]. 720 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(644),rewrite(686(3),2(3))]. 728 f(c_0,f(x,x)) = x. [back_rewrite(630),rewrite(686(3),2(3))]. 730 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(628),rewrite(686(4),2(4),686(7))]. 736 f(x,c_0) = f(x,x). [back_rewrite(613),rewrite(686(2))]. 750 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer"). [back_rewrite(625),rewrite(736(11,R),2(7)),flip(a)]. 767 f(f(x,f(x,y)),f(x,f(y,z))) = f(c_0,f(x,f(y,z))). [back_rewrite(164),rewrite(736(5,R),2(4)),flip(a)]. 784 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(285),rewrite(200(2),2(1),736(5,R),2(5))]. 880 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(720(a,1),203(a,2)),rewrite(2(8),730(8),2(5))]. 996 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [para(11(a,1),880(a,1,2)),rewrite(880(5),2(6),736(6),2(7)),flip(a)]. 1123 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x). [para(37(a,1),218(a,1,2,2,2)),rewrite(736(3,R),2(3),2(5))]. 1324 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))). [para(273(a,1),200(a,1,2)),rewrite(200(2),2(1),8(3),2(2),736(3,R),2(3),200(6),2(5),8(7),2(6))]. 1587 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)). [para(340(a,1),56(a,1,2)),rewrite(200(2),2(1),2(3)),flip(a)]. 1651 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)). [para(596(a,1),56(a,1,2)),rewrite(200(2),2(1)),flip(a)]. 2036 f(f(x,f(x,y)),f(c_0,f(z,f(x,f(y,u))))) = f(z,f(x,f(y,u))). [para(3(a,1),784(a,1,1,2)),rewrite(2(2),2(6),2(11))]. 2895 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(6(a,1),996(a,1,2,2)),rewrite(736(3,R),2(3),2(6),736(6),2(6),6(10))]. 2903 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(2895(a,1),9(a,1,2,2)),rewrite(2(7))]. 2909 f(f(x,y),f(c_0,f(f(x,x),f(z,u)))) = f(f(x,x),f(z,u)). [para(87(a,1),2895(a,1,2,2,2)),rewrite(736(7,R),2(5),728(8),2(6),2(7))]. 3346 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x). [para(73(a,1),1123(a,1,2,2)),rewrite(2(4),736(4))]. 3858 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(1587(a,1),1324(a,2,2)),rewrite(8(9))]. 6172 f(f(c_0,f(x,y)),f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [para(2903(a,1),1651(a,1,2)),rewrite(2(4),2(11),2(12),200(13,R),736(10,R),2(10)),flip(a)]. 6777 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(3858(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. 6880 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)). [para(3346(a,1),3858(a,1,2,2,2)),rewrite(2(6),2909(8)),flip(a)]. 16698 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),6880(a,1,1)),rewrite(736(3,R),2(3),736(7,R),2(7),736(10,R),2(10)),flip(a)]. 17176 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6172),rewrite(16698(7))]. 17429 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(17176(a,2),1324(a,2,2)),rewrite(880(5),2(4)),flip(a)]. 19770 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),17429(a,1,2,2,2)),rewrite(17429(5)),flip(a)]. 22246 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(19770(a,1),6777(a,1,2,2,2)),rewrite(2(4),2036(8))]. 23113 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))). [para(19770(a,1),22246(a,1,2)),rewrite(2(3),767(5)),flip(a)]. 23114 $F # answer("Sheffer"). [resolve(23113,a,750,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=305. Generated=353320. Kept=23111. proofs=1. Usable=220. Sos=12057. Demods=11011. Limbo=154, Disabled=10682. Hints=0. Weight_deleted=185. Literals_deleted=0. Forward_subsumed=328360. Back_subsumed=2597. Sos_limit_deleted=1664. Sos_displaced=0. Sos_removed=0. New_demodulators=21073 (5 lex), Back_demodulated=8081. Back_unit_deleted=1. Demod_attempts=7546057. Demod_rewrites=1718251. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=25.78. User_CPU=79.03, System_CPU=0.11, Wall_clock=79. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4414 exit (max_proofs) Wed Nov 22 12:05:38 2006