============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 28135 was started by mccune on cleo, Fri Apr 13 09:59:10 2007 The command was "/home/mccune/bin/prover9 -f BA2.in". ============================== 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. ============================== 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 (A,wt=11): 6 f(f(x,y),f(y,f(x,z))) = y. [para(2(a,1),3(a,1,1))]. given #4 (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))]. 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 (T,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 (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 #8 (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 #9 (T,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 (T,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 (T,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 (T,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 (T,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 (T,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 (T,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 (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 #19 (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 #20 (T,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 (T,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 (T,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 (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 #24 (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 #25 (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 #26 (T,wt=11): 136 f(x,f(y,f(x,y))) = f(x,x). [para(48(a,1),73(a,1,2)),flip(a)]. given #27 (T,wt=11): 145 f(x,f(y,f(y,x))) = f(x,x). [para(136(a,1),2(a,2)),rewrite(2(1),2(3))]. given #28 (A,wt=21): 27 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 #29 (T,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): 222 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(213(27),213(32))]. given #30 (T,wt=11): 213 f(x,f(y,y)) = f(x,f(x,y)). [para(136(a,1),56(a,1,2)),rewrite(2(3))]. given #31 (T,wt=11): 223 f(x,f(y,y)) = f(x,f(y,x)). [para(213(a,1),2(a,2)),rewrite(2(2),2(3))]. given #32 (T,wt=11): 226 f(x,f(x,f(y,y))) = f(y,x). [para(213(a,1),9(a,1)),rewrite(2(2),223(2,R),2(4),223(4,R),2(6),6(6),2(3))]. given #33 (A,wt=31): 28 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 #34 (T,wt=11): 229 f(x,f(y,f(y,x))) = f(x,x). [para(213(a,1),36(a,1,1)),rewrite(14(5),2(3))]. given #35 (T,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 #36 (T,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 #37 (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 #38 (A,wt=21): 29 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 #39 (T,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 #40 (T,wt=15): 122 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 #41 (T,wt=15): 220 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x. [back_rewrite(149),rewrite(213(5),2(6))]. given #42 (T,wt=15): 221 f(f(x,y),f(x,f(z,f(z,f(x,y))))) = x. [back_rewrite(38),rewrite(213(5))]. given #43 (A,wt=21): 30 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 #44 (T,wt=15): 224 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x. [para(213(a,1),3(a,1,1)),rewrite(2(4))]. given #45 (T,wt=15): 239 f(x,f(f(x,f(x,y)),f(y,y))) = f(x,x). [para(213(a,1),136(a,1,2,2)),rewrite(2(4))]. given #46 (T,wt=15): 244 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x). [back_rewrite(212),rewrite(223(6,R),2(4))]. restricted denial: (wt=23): 652 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(222),unit_del(a,642)]. given #47 (T,wt=11): 642 f(x,f(y,f(y,y))) = f(x,x). [para(244(a,1),59(a,1)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(665)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, f ]). restricted denial: (wt=19): 778 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer"). [back_rewrite(652),rewrite(763(11,R),2(7)),flip(a)]. given #48 (A,wt=27): 32 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 #49 (T,wt=7): 714 f(x,f(x,x)) = c_0. [new_symbol(665)]. given #50 (T,wt=7): 756 f(c_0,f(x,x)) = x. [back_rewrite(657),rewrite(714(3),2(3))]. given #51 (T,wt=7): 763 f(x,c_0) = f(x,x). [back_rewrite(642),rewrite(714(2))]. given #52 (T,wt=9): 911 f(f(x,x),f(c_0,c_0)) = c_0. [para(756(a,1),223(a,2,2)),rewrite(2(7),714(7))]. given #53 (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 #54 (T,wt=11): 748 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(671),rewrite(714(3),2(3))]. given #55 (T,wt=9): 973 f(f(x,y),f(c_0,c_0)) = c_0. [para(87(a,1),748(a,1,2)),rewrite(763(7,R),2(5),714(5),2(6)),flip(a)]. given #56 (T,wt=11): 758 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(655),rewrite(714(4),2(4),714(7))]. given #57 (T,wt=11): 897 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(714(a,1),7(a,1,2,1)),rewrite(2(3),21(4),714(7))]. given #58 (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 #59 (T,wt=11): 909 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(756(a,1),48(a,1,2)),rewrite(2(3),763(3),223(3),2(2),2(5))]. given #60 (T,wt=11): 917 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(756(a,1),69(a,1,2)),rewrite(2(5),763(5),2(5))]. given #61 (T,wt=11): 936 f(x,f(c_0,f(y,x))) = f(y,x). [para(24(a,1),35(a,1,2,2)),rewrite(763(3,R),2(3),2(5),2(7),223(7,R),931(7),763(4,R),2(4)),flip(a)]. given #62 (T,wt=11): 952 f(x,f(y,f(y,x))) = f(x,x). [para(35(a,1),67(a,1,1)),rewrite(223(2),2(1),14(6),2(4),14(5),2(3))]. given #63 (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 #64 (T,wt=11): 970 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(11(a,1),748(a,1,2)),rewrite(763(7,R),2(5),2(10),763(10),2(11),943(11))]. given #65 (T,wt=13): 968 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(7(a,1),748(a,1,2)),rewrite(2(2),763(2),2(3),763(3),763(3,R),2(3),756(3),2(2),763(2)),flip(a)]. given #66 (T,wt=13): 1044 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(87(a,1),909(a,1,2,2,2)),rewrite(714(6),2(7))]. given #67 (T,wt=13): 1062 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(87(a,1),917(a,1,2,2)),rewrite(763(7,R),2(5),756(8),2(6))]. given #68 (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 #69 (T,wt=13): 1142 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(968(a,1),909(a,1,2,2,2)),rewrite(2(7),714(7),2(8))]. given #70 (T,wt=13): 1144 f(f(c_0,c_0),f(f(x,y),f(z,z))) = c_0. [para(2(a,1),1044(a,1,2))]. given #71 (T,wt=15): 248 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x. [para(223(a,2),9(a,1,2,2))]. given #72 (T,wt=15): 267 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x. [para(226(a,2),3(a,1,2,2))]. given #73 (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 #74 (T,wt=15): 268 f(f(x,y),f(y,f(z,f(z,f(x,x))))) = y. [para(226(a,2),6(a,1,2,2))]. given #75 (T,wt=15): 270 f(x,f(x,f(y,f(y,f(x,x))))) = f(x,y). [para(226(a,2),8(a,1,2,2))]. given #76 (T,wt=15): 275 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)). [para(226(a,1),11(a,1,2,1,2)),rewrite(23(6)),flip(a)]. given #77 (T,wt=15): 356 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x. [para(229(a,1),12(a,1,2,2)),rewrite(2(3))]. given #78 (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 #79 (T,wt=15): 361 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 #80 (T,wt=15): 362 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 #81 (T,wt=15): 374 f(f(x,y),f(y,f(z,f(z,f(x,y))))) = y. [para(58(a,1),19(a,1,2,1)),rewrite(223(5),2(3),58(12))]. given #82 (T,wt=15): 400 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 #83 (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 #84 (T,wt=15): 543 f(x,f(f(y,x),f(z,f(x,x)))) = f(y,x). [para(6(a,1),221(a,1,2,2,2,2)),rewrite(6(4),2(2),223(3,R))]. given #85 (T,wt=15): 623 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x). [para(14(a,1),244(a,1,2,1)),rewrite(2(2))]. given #86 (T,wt=15): 730 f(f(x,x),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [back_rewrite(695),rewrite(714(3),714(5),2(5),714(10))]. given #87 (T,wt=15): 764 f(f(x,x),f(f(x,y),f(x,f(x,z)))) = c_0. [back_rewrite(637),rewrite(714(8))]. given #88 (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 #89 (T,wt=13): 1953 f(f(x,x),f(f(x,y),f(x,z))) = c_0. [para(8(a,1),764(a,1,2,2))]. given #90 (T,wt=13): 2064 f(f(c_0,c_0),f(f(x,y),f(x,z))) = c_0. [para(1953(a,1),10(a,1,2,2)),rewrite(2(8),223(9,R),2(7),1953(12))]. given #91 (T,wt=13): 2087 f(f(c_0,c_0),f(f(x,y),f(y,z))) = c_0. [para(2(a,1),2064(a,1,2,1))]. given #92 (T,wt=15): 772 f(c_0,f(x,f(y,f(y,f(z,f(x,x)))))) = x. [back_rewrite(490),rewrite(714(2))]. given #93 (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 #94 (T,wt=15): 815 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(287),rewrite(223(2),2(1),763(5,R),2(5))]. given #95 (T,wt=13): 2258 f(f(x,x),f(y,f(y,f(x,z)))) = x. [para(3(a,1),815(a,1,2,2)),rewrite(2(5),763(5),2(5),3(9))]. given #96 (T,wt=13): 2260 f(f(x,f(x,f(y,z))),f(z,z)) = z. [para(6(a,1),815(a,1,2,2)),rewrite(2(5),763(5),6(9))]. given #97 (T,wt=15): 858 f(f(x,f(y,z)),f(c_0,f(y,z))) = f(y,z). [para(32(a,1),31(a,1,2,2)),rewrite(2(2),763(5,R),2(5))]. given #98 (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 #99 (T,wt=13): 2496 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(858(a,1),1044(a,1,2,1))]. given #100 (T,wt=15): 889 f(f(x,y),f(x,f(z,f(c_0,f(x,y))))) = x. [para(32(a,1),30(a,1,2,2,2,2)),rewrite(27(10),763(4,R),2(4),27(16))]. given #101 (T,wt=15): 907 f(x,f(c_0,f(y,f(c_0,f(z,f(x,x)))))) = c_0. [para(756(a,1),31(a,1,1)),rewrite(2(4))]. given #102 (T,wt=15): 908 f(f(c_0,f(x,y)),f(c_0,f(z,f(y,y)))) = c_0. [para(756(a,1),48(a,1,1,2,2)),rewrite(2(6))]. given #103 (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 #104 (T,wt=15): 943 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [para(35(a,1),223(a,2,2)),rewrite(763(7,R),2(7),756(7),2(5),19(5),2(8),223(8,R),763(6,R),2(6)),flip(a)]. given #105 (T,wt=13): 2771 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(6(a,1),943(a,1,2,2)),rewrite(763(3,R),2(3),2(6),763(6),2(6),6(10))]. given #106 (T,wt=15): 974 f(f(x,f(y,y)),f(c_0,f(z,y))) = f(z,y). [para(23(a,1),748(a,1,2)),rewrite(763(7,R),2(5),970(5),2(6),763(6),2(7)),flip(a)]. given #107 (T,wt=15): 985 f(f(x,y),f(c_0,f(z,f(c_0,f(x,y))))) = c_0. [para(973(a,1),7(a,1,2,1)),rewrite(2(7),223(7),2(5),763(5),714(5),2(5),973(13))]. given #108 (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 #109 (T,wt=15): 1032 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x). [para(37(a,1),244(a,1,2,2,2)),rewrite(763(3,R),2(3),2(5))]. given #110 (T,wt=15): 1036 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0. [para(3(a,1),909(a,1,2,2,2)),rewrite(2(5))]. given #111 (T,wt=15): 1037 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0. [para(9(a,1),909(a,1,2,2,2)),rewrite(2(5))]. given #112 (T,wt=15): 1057 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0. [para(224(a,1),909(a,1,2,2,2)),rewrite(223(2),2(1),2(7),8(7))]. given #113 (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 #114 (T,wt=15): 1063 f(f(x,x),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(30(a,1),917(a,1,2)),rewrite(2(4),763(4),756(4),2(8),763(8),756(8),763(9,R),2(6),2(8),763(8),2(8))]. given #115 (T,wt=15): 1064 f(x,f(c_0,f(f(x,f(x,y)),f(y,y)))) = c_0. [para(239(a,1),917(a,1,2,2)),rewrite(763(9,R),2(6),756(9),2(7))]. given #116 (T,wt=15): 1065 f(x,f(c_0,f(f(y,y),f(x,f(y,z))))) = c_0. [para(244(a,1),917(a,1,2,2)),rewrite(763(9,R),2(6),756(9),2(7))]. given #117 (T,wt=15): 1082 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x. [para(224(a,1),936(a,1,2,2)),rewrite(223(2),2(1),2(5),763(5),2(5),14(5),223(4),2(3)),flip(a)]. given #118 (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 #119 (T,wt=15): 1123 f(x,f(y,f(c_0,f(z,f(x,x))))) = f(x,x). [para(14(a,1),968(a,1,1)),rewrite(2(3))]. given #120 (T,wt=15): 1124 f(f(x,y),f(x,f(z,f(c_0,f(y,u))))) = x. [para(968(a,1),9(a,1,2,2)),rewrite(2(7))]. given #121 (T,wt=15): 1125 f(f(x,y),f(y,f(z,f(c_0,f(x,u))))) = y. [para(968(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. given #122 (T,wt=15): 1227 f(f(c_0,c_0),f(x,f(y,f(c_0,f(z,u))))) = c_0. [para(1142(a,1),11(a,1,2,2,2)),rewrite(2(11),763(14),2(14),1145(15),2(9)),flip(a)]. given #123 (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 #124 (T,wt=15): 1241 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x. [para(19(a,1),248(a,1,1,2)),rewrite(2(8),35(8))]. given #125 (T,wt=15): 1308 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x). [para(267(a,1),244(a,1,2,2,2)),rewrite(763(3,R),2(3),2(5))]. given #126 (T,wt=15): 1519 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))). [para(275(a,1),223(a,1,2)),rewrite(223(2),2(1),8(3),2(2),763(3,R),2(3),223(6),2(5),8(7),2(6))]. given #127 (T,wt=15): 1521 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)). [para(275(a,1),226(a,1,2,2)),rewrite(223(2),2(1),8(3),2(2),763(3,R),2(3),223(7),2(6),8(8),2(7))]. given #128 (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 #129 (T,wt=15): 1819 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)). [para(400(a,1),56(a,1,2)),rewrite(223(2),2(1),2(3)),flip(a)]. given #130 (T,wt=15): 1897 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x). [para(2(a,1),623(a,1,2)),rewrite(223(2),2(1),2(4))]. given #131 (T,wt=15): 1906 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)). [para(623(a,1),56(a,1,2)),rewrite(223(2),2(1)),flip(a)]. given #132 (T,wt=15): 1916 f(x,f(c_0,f(y,f(x,f(z,f(y,y)))))) = c_0. [para(623(a,1),917(a,1,2,2)),rewrite(763(9,R),2(6),756(9),2(7))]. given #133 (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 #134 (T,wt=15): 1917 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x). [para(623(a,1),40(a,1)),rewrite(763(6,R),2(5)),flip(a)]. given #135 (T,wt=15): 2061 f(f(x,f(y,f(x,z))),f(c_0,f(x,z))) = c_0. [para(3(a,1),1953(a,1,2,1)),rewrite(763(3,R),2(3),2(5),2(7))]. given #136 (T,wt=13): 5041 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(6(a,1),2061(a,1,1,2,2)),rewrite(2(2),6(8),2(5),763(5),2(5))]. given #137 (T,wt=15): 2063 f(f(x,f(y,f(z,x))),f(c_0,f(z,x))) = c_0. [para(6(a,1),1953(a,1,2,1)),rewrite(763(3,R),2(3),2(5),2(7))]. given #138 (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 #139 (T,wt=15): 2124 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0. [para(772(a,1),9(a,1,2)),rewrite(223(3),2(2),2(7))]. given #140 (T,wt=15): 2126 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x). [para(772(a,1),36(a,1,1)),rewrite(763(11,R),2(7),772(7)),flip(a)]. given #141 (T,wt=15): 2130 f(x,f(c_0,f(y,f(c_0,f(z,f(z,x)))))) = c_0. [para(772(a,1),67(a,1,2)),rewrite(223(4),2(3),2(6),2(8))]. given #142 (T,wt=15): 2255 f(f(x,f(y,f(y,z))),f(x,f(z,u))) = x. [para(815(a,1),3(a,1,2,2))]. given #143 (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 #144 (T,wt=15): 2366 f(f(x,y),f(x,f(z,f(z,f(y,u))))) = x. [para(2258(a,1),9(a,1,2,2)),rewrite(2(6))]. given #145 (T,wt=15): 2367 f(f(x,y),f(y,f(z,f(z,f(x,u))))) = y. [para(2258(a,1),12(a,1,2,2)),rewrite(2(4),2(5),2(6))]. given #146 (T,wt=15): 2384 f(f(x,x),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(2258(a,1),917(a,1,2,2)),rewrite(763(7,R),2(5),2(7),763(7),2(7))]. given #147 (T,wt=15): 2402 f(f(x,y),f(x,f(z,f(z,f(u,y))))) = x. [para(2260(a,1),3(a,1,2,2)),rewrite(2(6))]. given #148 (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 #149 (T,wt=15): 2404 f(f(x,y),f(y,f(z,f(z,f(u,x))))) = y. [para(2260(a,1),6(a,1,2,2)),rewrite(2(4),2(5),2(6))]. given #150 (T,wt=15): 2407 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x). [para(14(a,1),2260(a,1,2)),rewrite(223(2),2(1),2(5))]. given #151 (T,wt=15): 2446 f(f(x,x),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(2260(a,1),758(a,1,2,2)),rewrite(763(7,R),2(5),2(7),763(7),2(7))]. given #152 (T,wt=15): 2632 f(f(c_0,c_0),f(x,f(f(y,z),f(u,v)))) = c_0. [para(2496(a,1),11(a,1,2,2,2)),rewrite(2(10),763(13),2(13),1145(14),2(8)),flip(a)]. given #153 (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 #154 (T,wt=15): 2780 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(2771(a,1),9(a,1,2,2)),rewrite(2(7))]. given #155 (T,wt=15): 2782 f(f(x,y),f(y,f(z,f(c_0,f(u,x))))) = y. [para(2771(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. given #156 (T,wt=15): 2814 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x). [para(21(a,1),974(a,1,2,2)),rewrite(223(2),2(1),223(4),2(3),763(5,R),2(4),756(8),2(6),223(8),2(7),952(9))]. given #157 (T,wt=15): 2984 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x). [para(73(a,1),1032(a,1,2,2)),rewrite(2(4),763(4))]. given #158 (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 #159 (T,wt=15): 3023 f(x,f(c_0,f(f(x,y),f(c_0,f(y,z))))) = c_0. [para(1032(a,1),917(a,1,2,2)),rewrite(2(3),2(8),763(11,R),2(7),756(10),2(8))]. given #160 (T,wt=15): 3049 f(f(x,x),f(y,f(f(x,z),f(x,u)))) = x. [para(1953(a,1),1032(a,1,2,1)),rewrite(970(9),763(9,R),2(9),756(9))]. given #161 (T,wt=15): 3069 f(f(x,f(y,z)),f(c_0,f(x,f(y,y)))) = c_0. [para(2(a,1),1036(a,1,1)),rewrite(2(2),2(4),223(5,R))]. given #162 (T,wt=15): 3071 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0. [para(3(a,1),1036(a,1,1,2))]. given #163 (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 #164 (T,wt=15): 3078 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0. [para(33(a,1),1036(a,1,1))]. given #165 (T,wt=15): 3089 f(f(x,f(y,f(z,z))),f(c_0,f(x,z))) = c_0. [para(223(a,1),1036(a,1,2,2,2)),rewrite(2(2),2(5),8(7))]. given #166 (T,wt=15): 3151 f(f(x,f(y,z)),f(c_0,f(x,f(z,z)))) = c_0. [para(2(a,1),1037(a,1,1)),rewrite(2(2),2(4),223(5,R))]. given #167 (T,wt=15): 3197 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0. [para(2(a,1),1057(a,1,1)),rewrite(2(3),2(5))]. given #168 (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 #169 (T,wt=15): 3269 f(f(x,y),f(c_0,f(x,f(c_0,f(y,z))))) = c_0. [para(758(a,1),1057(a,1,1,2,2)),rewrite(2(3),756(3))]. given #170 (T,wt=15): 3450 f(x,f(c_0,f(f(x,y),f(c_0,f(z,y))))) = c_0. [para(6(a,1),1065(a,1,2,2,2,2)),rewrite(763(4,R),2(4),2(6))]. given #171 (T,wt=15): 3616 f(f(x,f(y,z)),f(x,f(u,f(z,z)))) = x. [para(6(a,1),1124(a,1,2,2,2,2)),rewrite(2(4),763(4))]. given #172 (T,wt=15): 4135 f(x,f(c_0,f(y,f(y,f(z,f(x,x)))))) = c_0. [para(1519(a,1),907(a,1,2,2))]. given #173 (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 #174 (T,wt=15): 4336 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)). [para(1819(a,1),2(a,2)),rewrite(2(1),2(4),2(5),223(6,R))]. given #175 (T,wt=15): 4402 f(x,f(x,f(y,f(z,f(x,x))))) = f(x,y). [para(623(a,1),1819(a,1,2,2)),rewrite(2(5),14(5)),flip(a)]. given #176 (T,wt=15): 4444 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(1819(a,1),1519(a,2,2)),rewrite(8(9))]. given #177 (T,wt=15): 4481 f(f(x,f(y,f(z,z))),f(c_0,f(z,x))) = c_0. [back_rewrite(3239),rewrite(2(4),223(5,R),2(6),223(7,R),2(9),223(10,R),763(8,R),2(8),756(8),2(6),2(7))]. given #178 (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 #179 (T,wt=15): 4541 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). [para(1897(a,1),40(a,1)),flip(a)]. given #180 (T,wt=15): 4570 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)). [para(1906(a,1),2(a,2)),rewrite(223(2),2(1),2(4),2(5),223(6,R))]. given #181 (T,wt=15): 4824 f(x,f(c_0,f(y,f(z,f(x,x))))) = f(x,y). [para(1906(a,1),1519(a,2,2)),rewrite(8(9))]. given #182 (T,wt=15): 4839 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0. [para(2(a,1),1916(a,1,2,2)),rewrite(223(3),2(2),2(5))]. given #183 (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 #184 (T,wt=15): 4847 f(f(x,y),f(c_0,f(y,f(c_0,f(x,z))))) = c_0. [para(1125(a,1),1916(a,1,2,2,2)),rewrite(2(6))]. given #185 (T,wt=15): 4944 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x). [para(1917(a,1),2(a,2)),rewrite(2(2),2(6))]. given #186 (T,wt=15): 4985 f(x,f(c_0,f(y,f(c_0,f(z,f(y,x)))))) = c_0. [para(1917(a,1),917(a,1,2,2)),rewrite(2(2),2(7),763(11,R),2(7),756(10),2(8))]. given #187 (T,wt=15): 5019 f(x,f(c_0,f(y,f(c_0,f(z,f(x,y)))))) = c_0. [para(1917(a,1),1064(a,1,2,2,1,2)),rewrite(714(3),763(13,R),2(9),970(10))]. given #188 (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 #189 (T,wt=15): 6074 f(x,f(f(y,f(y,x)),f(x,z))) = f(x,z). [para(37(a,1),2404(a,1,2)),rewrite(223(2),2(1),2(3),2(5),2(6))]. given #190 (T,wt=15): 6486 f(x,f(c_0,f(f(x,f(y,z)),f(z,z)))) = c_0. [para(2984(a,1),917(a,1,2,2)),rewrite(763(9,R),2(6),756(9),2(7))]. given #191 (T,wt=15): 7327 f(x,f(c_0,f(y,f(y,f(z,f(x,y)))))) = c_0. [para(48(a,1),4135(a,1,2,2,2)),rewrite(2(2),2(5))]. given #192 (T,wt=15): 7453 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(4444(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. given #193 (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 #194 (T,wt=15): 7598 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x). [para(4541(a,1),2(a,2)),rewrite(2(1),2(5))]. given #195 (T,wt=15): 7615 f(x,f(c_0,f(y,f(y,f(z,f(y,x)))))) = c_0. [para(4541(a,1),917(a,1,2,2)),rewrite(2(1),2(5),763(9,R),2(6),756(9),2(7))]. given #196 (T,wt=15): 7653 f(x,f(y,f(z,f(x,x)))) = f(x,f(y,y)). [para(4570(a,2),2(a,2)),rewrite(2(2),2(3),223(4,R)),flip(a)]. given #197 (T,wt=15): 7827 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(y,x). [para(4824(a,1),2(a,2)),rewrite(223(3),2(2),2(6),2(7))]. given #198 (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 #199 (T,wt=17): 225 f(f(x,f(x,y)),f(f(x,z),f(y,y))) = f(y,y). [para(213(a,1),6(a,1,1)),rewrite(2(5))]. given #200 (T,wt=17): 232 f(x,f(y,f(f(x,y),f(y,z)))) = f(x,f(x,y)). [para(22(a,1),213(a,2,2)),rewrite(218(7))]. given #201 (T,wt=17): 250 f(x,f(f(x,y),f(f(x,x),f(y,z)))) = f(x,y). [para(223(a,2),7(a,1,2,2)),rewrite(2(4))]. given #202 (T,wt=17): 279 f(x,f(f(y,z),f(y,f(y,f(x,x))))) = f(x,y). [para(226(a,2),22(a,1,2,1)),rewrite(2(5))]. given #203 (A,wt=23): 88 f(f(x,x),f(f(x,y),f(f(x,x),f(z,u)))) = f(f(x,x),f(z,u)). [para(87(a,1),6(a,1,1)),rewrite(2(6))]. given #204 (T,wt=17): 364 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 #205 (T,wt=17): 377 f(f(x,f(y,y)),f(f(y,x),f(x,z))) = f(y,x). [para(58(a,1),31(a,1,2,2,2)),rewrite(2(2),223(2,R),2(4))]. given #206 (T,wt=17): 450 f(f(x,f(y,z)),f(f(x,u),f(y,z))) = f(y,z). [para(67(a,1),29(a,1,2,2,2)),rewrite(2(4),2(5))]. given #207 (T,wt=17): 635 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)). [para(244(a,1),56(a,1,2)),flip(a)]. given #208 (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 #209 (T,wt=17): 716 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)). [back_rewrite(690),rewrite(714(7),2(7),28(10))]. given #210 (T,wt=17): 827 f(f(x,y),f(y,f(y,f(x,z)))) = f(c_0,f(x,y)). [back_rewrite(148),rewrite(763(8,R),2(8))]. given #211 (T,wt=17): 828 f(f(x,y),f(x,f(x,f(y,z)))) = f(c_0,f(x,y)). [back_rewrite(146),rewrite(763(8,R),2(8))]. given #212 (T,wt=17): 1128 f(f(x,y),f(z,f(c_0,f(x,y)))) = f(c_0,f(x,y)). [para(11(a,1),968(a,1,2,2)),rewrite(763(7,R),2(5),970(5))]. given #213 (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))]. given #214 (T,wt=17): 1135 f(x,f(f(x,y),f(z,f(c_0,f(y,u))))) = f(x,y). [para(968(a,1),59(a,1,2,2,2)),rewrite(2(6),968(13))]. given #215 (T,wt=17): 1150 f(x,f(c_0,f(y,f(c_0,f(f(x,x),f(z,u)))))) = c_0. [para(1062(a,1),22(a,1,2,1)),rewrite(2(7),1062(15))]. given #216 (T,wt=17): 1413 f(f(c_0,f(x,y)),f(f(x,y),f(z,u))) = f(x,y). [para(970(a,1),42(a,1,2,1)),rewrite(2(9),763(9),2(10),943(10),2(6),2(12),763(12),2(13),943(13))]. given #217 (T,wt=17): 1647 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)). [para(223(a,1),43(a,1,2,2)),rewrite(2(7),6(7),2(4),223(4,R),254(6),763(8,R),2(7)),flip(a)]. given #218 (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))]. given #219 (T,wt=17): 1949 f(f(c_0,f(x,y)),f(x,f(f(x,y),f(z,z)))) = c_0. [para(3(a,1),764(a,1,2,1)),rewrite(763(3,R),2(3),2(6),223(7,R))]. given #220 (T,wt=15): 11677 f(f(x,y),f(c_0,f(x,f(x,f(z,y))))) = c_0. [para(2260(a,1),1949(a,1,2,2)),rewrite(2(7))]. given #221 (T,wt=17): 1951 f(f(c_0,f(x,y)),f(y,f(f(x,y),f(z,z)))) = c_0. [para(6(a,1),764(a,1,2,1)),rewrite(763(3,R),2(3),2(6),223(7,R))]. given #222 (T,wt=17): 2067 f(f(x,x),f(c_0,f(y,f(f(x,z),f(x,u))))) = c_0. [para(1953(a,1),22(a,1,2,1)),rewrite(2(6),1953(13))]. given #223 (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))]. given #224 (T,wt=17): 2068 f(f(c_0,f(x,f(y,y))),f(f(y,z),f(y,u))) = c_0. [para(1953(a,1),24(a,1,2,1)),rewrite(2(6),2(8),1953(13))]. given #225 (T,wt=17): 2256 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)). [para(815(a,1),3(a,1,2)),rewrite(2(4),2(6))]. given #226 (T,wt=15): 12183 f(x,f(x,f(y,f(z,f(z,x))))) = f(y,x). [para(4402(a,1),2256(a,1,2,2)),rewrite(223(2),2(1),2(4),2(6),7873(8),223(3),2(2)),flip(a)]. given #227 (T,wt=15): 12207 f(f(x,x),f(y,f(f(z,x),f(x,u)))) = x. [para(377(a,1),2256(a,1,2,2,2)),rewrite(2(4),2(9),6(9),2(6),763(6),2(6),377(14),2(10),6(10))]. given #228 (A,wt=23): 96 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,z)))))) = x. [para(23(a,1),3(a,1,1)),rewrite(2(8))]. given #229 (T,wt=17): 2287 f(f(x,y),f(c_0,f(z,f(y,y)))) = f(z,f(y,y)). [para(223(a,1),815(a,1,1,2)),rewrite(2(1),8(3),2(4),2(8))]. given #230 (T,wt=17): 2288 f(f(x,y),f(c_0,f(z,f(x,x)))) = f(z,f(x,x)). [para(226(a,1),815(a,1,1)),rewrite(2(4),2(8))]. given #231 (T,wt=17): 2377 f(x,f(f(x,y),f(z,f(z,f(y,u))))) = f(x,y). [para(2258(a,1),59(a,1,2,2,2)),rewrite(2(5),2258(11))]. given #232 (T,wt=17): 2423 f(x,f(f(x,y),f(z,f(z,f(u,y))))) = f(x,y). [para(2260(a,1),56(a,1,2,2,2)),rewrite(2(5),2260(11))]. given #233 (A,wt=33): 97 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(v,f(x,z))))) = f(f(x,f(y,z)),f(v,f(x,z))). [para(23(a,1),6(a,1,1)),rewrite(2(9))]. given #234 (T,wt=17): 2478 f(f(x,f(x,f(y,f(y,f(z,u))))),f(u,u)) = u. [para(2260(a,1),815(a,1,2,2)),rewrite(2(7),763(7),2260(12))]. given #235 (T,wt=13): 13030 f(f(x,x),f(y,f(y,f(z,x)))) = x. [para(12(a,1),2478(a,1,1,2)),rewrite(2(2),2(3),2(5))]. given #236 (T,wt=17): 2777 f(f(x,x),f(y,f(c_0,f(z,f(z,f(u,x)))))) = x. [para(2260(a,1),943(a,1,2,2)),rewrite(763(7,R),2(5),2(8),763(8),2(8),2260(13))]. given #237 (T,wt=17): 2790 f(x,f(f(x,y),f(z,f(c_0,f(u,y))))) = f(x,y). [para(2771(a,1),59(a,1,2,2,2)),rewrite(2(6),2771(13))]. given #238 (A,wt=31): 98 f(x,f(f(x,f(y,z)),f(u,f(x,f(v,f(f(x,f(y,z)),f(w,f(x,z)))))))) = f(x,f(y,z)). [para(23(a,1),7(a,1,2,1)),rewrite(2(8),23(18))]. Low Water (keep, True_semantics): wt=99 Low Water (keep, True_semantics): wt=95 given #239 (T,wt=17): 2812 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(x,u)))))) = x. [para(7(a,1),974(a,1,2)),rewrite(763(9,R),2(6),2(9),763(9),2(9),2(11),763(11),968(15))]. given #240 (T,wt=17): 2819 f(x,f(y,f(c_0,f(f(x,x),f(z,u))))) = f(x,x). [para(87(a,1),974(a,1,2,2)),rewrite(763(7,R),2(5),756(9),2(7),87(11))]. given #241 (T,wt=17): 2830 f(f(x,x),f(y,f(c_0,f(z,f(c_0,f(u,x)))))) = x. [para(30(a,1),974(a,1,2)),rewrite(2(4),763(4),756(4),2(8),763(8),756(8),763(9,R),2(6),2(9),763(9),2(9),2(11),763(11),2(14),763(14),756(14),2771(15))]. given #242 (T,wt=17): 2845 f(f(x,x),f(y,f(c_0,f(z,f(z,f(x,u)))))) = x. [para(2258(a,1),974(a,1,2,2)),rewrite(763(7,R),2(5),2(8),763(8),2(8),2258(13))]. given #243 (A,wt=21): 99 f(x,f(f(x,y),f(z,f(x,f(u,f(x,f(y,v))))))) = f(x,y). [para(7(a,1),23(a,1,2,1)),rewrite(7(14))]. Low Water (keep, True_semantics): wt=83 given #244 (T,wt=17): 2935 f(f(x,y),f(y,f(c_0,f(x,z)))) = f(c_0,f(x,y)). [para(57(a,1),623(a,1)),rewrite(763(4,R),2(4),763(9,R),2(9))]. given #245 (T,wt=17): 2985 f(x,f(y,f(x,f(f(y,y),f(z,u))))) = f(x,x). [para(87(a,1),1032(a,1,2,2,2)),rewrite(756(7),2(5))]. given #246 (T,wt=17): 3039 f(f(x,y),f(x,f(c_0,f(y,z)))) = f(c_0,f(x,y)). [para(1032(a,1),400(a,1,2,2,2)),rewrite(2(3),2(7),14(7),2(5),763(9,R),2(9))]. given #247 (T,wt=17): 3210 f(f(x,x),f(f(y,x),f(z,f(z,f(x,x))))) = c_0. [para(36(a,1),1057(a,1,2,2)),rewrite(2(7),763(7),2(7))]. given #248 (A,wt=41): 100 f(x,f(f(y,f(x,f(z,u))),f(x,f(v,f(f(x,f(z,u)),f(w,f(x,u))))))) = f(x,f(v,f(f(x,f(z,u)),f(w,f(x,u))))). [para(23(a,1),11(a,1,2,2,2)),rewrite(2(6),2(11),2(18))]. Low Water (keep, True_semantics): wt=69 given #249 (T,wt=17): 3297 f(f(x,y),f(c_0,f(x,f(f(y,z),f(y,u))))) = c_0. [para(1953(a,1),1057(a,1,1,2,2)),rewrite(2(3),756(3))]. Low Water (keep, True_semantics): wt=67 given #250 (T,wt=17): 3621 f(x,f(f(y,x),f(z,f(c_0,f(y,u))))) = f(y,x). [para(1124(a,1),12(a,1,2)),rewrite(2(5),2(6),2(7),2(8))]. given #251 (T,wt=17): 3789 f(f(c_0,c_0),f(x,f(y,f(z,f(c_0,f(u,v)))))) = c_0. [para(1227(a,1),11(a,1,2,2,2)),rewrite(2(12),763(15),2(15),2632(16),2(10)),flip(a)]. given #252 (T,wt=17): 3815 f(x,f(c_0,f(f(x,y),f(y,z)))) = f(x,f(x,y)). [para(223(a,1),63(a,1,2,2)),rewrite(2(6),22(6),2(5),73(6),763(9,R),2(7)),flip(a)]. Low Water (keep, True_semantics): wt=63 given #253 (A,wt=23): 101 f(x,f(f(x,f(y,z)),f(u,f(x,f(v,f(x,y)))))) = f(x,f(y,z)). [para(11(a,1),23(a,1,2,1)),rewrite(11(14))]. given #254 (T,wt=17): 4003 f(x,f(c_0,f(f(x,y),f(z,y)))) = f(x,f(x,y)). [para(34(a,1),1519(a,2,2)),rewrite(2(3),2(4),2(7))]. given #255 (T,wt=17): 4350 f(x,f(f(y,f(x,x)),f(f(x,x),f(z,u)))) = c_0. [para(87(a,1),1819(a,1,2,2,2)),rewrite(2(6),87(11),714(9))]. Low Water (keep, True_semantics): wt=61 given #256 (T,wt=17): 4361 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y). [para(223(a,1),1819(a,1,2,2,2)),rewrite(2(2),223(8),2(7),8(9))]. given #257 (T,wt=17): 4378 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)). [para(244(a,1),1819(a,1,2,2)),rewrite(2(5),14(5),2(2),4145(8)),flip(a)]. Low Water (keep, True_semantics): wt=59 given #258 (A,wt=27): 102 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(v,f(x,z)))))) = f(x,f(y,z)). [para(23(a,1),22(a,1,2,1)),rewrite(2(8),23(16))]. Low Water (keep, True_semantics): wt=57 given #259 (T,wt=17): 4550 f(x,f(f(x,y),f(f(y,z),f(y,u)))) = f(x,x). [para(1953(a,1),1897(a,1,2,2,2,2)),rewrite(2(6),756(6),2(5))]. Low Water (keep, True_semantics): wt=55 given #260 (T,wt=17): 5081 f(f(c_0,f(x,f(y,y))),f(f(z,y),f(y,u))) = c_0. [para(5041(a,1),24(a,1,2,1)),rewrite(2(6),2(8),5041(13))]. given #261 (T,wt=17): 5109 f(x,f(f(x,y),f(f(z,y),f(y,u)))) = f(x,x). [para(5041(a,1),1897(a,1,2,2,2,2)),rewrite(2(6),756(6),2(5))]. given #262 (T,wt=17): 5440 f(f(x,y),f(x,f(z,f(f(y,u),f(y,v))))) = x. [para(1953(a,1),2255(a,1,1,2,2)),rewrite(2(3),756(3),2(5))]. Low Water (keep, True_semantics): wt=53 given #263 (A,wt=27): 103 f(f(f(x,y),f(x,f(z,u))),f(f(x,f(z,u)),f(v,f(x,u)))) = f(x,f(z,u)). [para(23(a,1),24(a,1,2,1)),rewrite(2(9),2(10),23(16))]. given #264 (T,wt=17): 5648 f(x,f(f(y,f(y,f(z,u))),f(z,x))) = f(z,x). [para(2366(a,1),12(a,1,2)),rewrite(2(4),2(6),2(7))]. Low Water (keep, True_semantics): wt=51 given #265 (T,wt=17): 5766 f(x,f(f(y,x),f(z,f(z,f(y,u))))) = f(y,x). [para(2367(a,1),9(a,1,2)),rewrite(2(6))]. given #266 (T,wt=17): 5885 f(x,f(f(y,f(y,f(z,u))),f(u,x))) = f(u,x). [para(2402(a,1),12(a,1,2)),rewrite(2(4),2(6),2(7))]. given #267 (T,wt=17): 6044 f(f(x,f(y,z)),f(c_0,f(f(x,y),f(x,u)))) = x. [para(70(a,1),1906(a,1,2)),rewrite(2(4),3(4),4415(9)),flip(a)]. Low Water (keep, True_semantics): wt=49 given #268 (A,wt=23): 105 f(x,f(f(x,f(y,z)),f(u,f(x,f(v,f(x,z)))))) = f(x,f(y,z)). [para(23(a,1),23(a,1,2,1)),rewrite(23(14))]. given #269 (T,wt=17): 6143 f(f(c_0,c_0),f(x,f(y,f(f(z,u),f(v,w))))) = c_0. [para(2632(a,1),11(a,1,2,2,2)),rewrite(2(11),763(14),2(14),2632(15),2(9)),flip(a)]. given #270 (T,wt=17): 6145 f(f(c_0,f(x,y)),f(f(x,x),f(z,u))) = f(x,y). [para(2632(a,1),42(a,1,2)),rewrite(2(5),970(5),2(7),763(7),2(7)),flip(a)]. given #271 (T,wt=17): 6371 f(x,f(f(y,x),f(z,f(c_0,f(u,y))))) = f(y,x). [para(2780(a,1),12(a,1,2)),rewrite(2(5),2(6),2(7),2(8))]. given #272 (T,wt=17): 6374 f(f(x,f(y,z)),f(x,f(f(y,y),f(u,v)))) = x. [para(87(a,1),2780(a,1,2,2,2,2)),rewrite(756(7),2(5),2(7))]. given #273 (A,wt=27): 106 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(31(a,1),6(a,1,1)),rewrite(2(6))]. Low Water (keep, True_semantics): wt=47 given #274 (T,wt=17): 6722 f(f(x,y),f(y,f(z,f(f(x,u),f(x,v))))) = y. [para(3049(a,1),12(a,1,2,2)),rewrite(2(5),2(6),2(7))]. given #275 (T,wt=17): 6771 f(x,f(c_0,f(f(x,y),f(f(y,z),f(y,u))))) = c_0. [para(3049(a,1),1916(a,1,2,2,2,2)),rewrite(2(6))]. given #276 (T,wt=17): 7230 f(x,f(c_0,f(y,f(x,f(f(y,y),f(z,u)))))) = c_0. [para(87(a,1),3450(a,1,2,2,2,2)),rewrite(756(8),2(6))]. given #277 (T,wt=17): 7410 f(f(x,y),f(c_0,f(f(x,z),f(x,f(y,u))))) = x. [para(71(a,1),4336(a,1,2)),rewrite(3(4),763(10,R),2(7)),flip(a)]. Low Water (keep, True_semantics): wt=45 given #278 (A,wt=25): 108 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(31(a,1),7(a,1,2,1)),rewrite(2(7),31(17))]. given #279 (T,wt=17): 7455 f(f(x,y),f(c_0,f(f(y,z),f(y,f(x,u))))) = y. [para(6(a,1),4444(a,1,2,2,2,2)),rewrite(2(5),2(6),6(12))]. given #280 (T,wt=17): 7555 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)). [para(2984(a,1),4444(a,1,2,2,2)),rewrite(2(6),2786(8)),flip(a)]. given #281 (T,wt=15): 18789 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6406),rewrite(18336(7))]. Low Water (keep, True_semantics): wt=43 given #282 (T,wt=15): 18807 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))). [para(18789(a,1),2(a,1)),rewrite(2(6),2(8))]. given #283 (A,wt=25): 109 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),31(a,1,1)),rewrite(2(7))]. given #284 (T,wt=15): 18808 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))). [para(18789(a,1),2(a,2)),rewrite(2(4),2(6))]. given #285 (T,wt=15): 18816 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))). [para(18789(a,1),8(a,2)),rewrite(1521(5)),flip(a)]. given #286 (T,wt=15): 18817 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))). [para(18789(a,2),8(a,2)),rewrite(1521(5),2(5)),flip(a)]. Low Water (keep, True_semantics): wt=41 given #287 (T,wt=15): 18820 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x. [para(18789(a,1),9(a,1,2))]. given #288 (A,wt=39): 110 f(f(x,y),f(f(x,z),f(f(x,y),f(u,f(x,f(v,f(x,f(y,w)))))))) = f(f(x,y),f(u,f(x,f(v,f(x,f(y,w)))))). [para(31(a,1),11(a,1,2,2,2)),rewrite(2(7),2(9),2(10),2(17))]. given #289 (T,wt=15): 18821 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x. [para(18789(a,2),9(a,1,2)),rewrite(2(4))]. given #290 (T,wt=15): 18827 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x. [para(18789(a,1),12(a,1,2)),rewrite(2(2),2(4))]. given #291 (T,wt=15): 18828 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x. [para(18789(a,2),12(a,1,2)),rewrite(2(2))]. given #292 (T,wt=15): 19036 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))). [para(18789(a,2),1519(a,1))]. Low Water (keep, True_semantics): wt=39 given #293 (A,wt=27): 111 f(f(x,f(y,z)),f(x,f(u,f(x,f(v,f(f(x,f(y,z)),f(w,f(x,y)))))))) = x. [para(11(a,1),31(a,1,1)),rewrite(2(8))]. given #294 (T,wt=15): 19038 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(18789(a,2),1519(a,2,2)),rewrite(970(5),2(4)),flip(a)]. given #295 (T,wt=15): 19070 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(18789(a,1),2061(a,1,1,2)),rewrite(2(9),970(11),2(8))]. given #296 (T,wt=15): 19228 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))). [para(18789(a,1),364(a,2)),rewrite(2(12),9819(15),2(5)),flip(a)]. given #297 (T,wt=15): 19277 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)). [para(18789(a,2),2256(a,2,2)),rewrite(2(4),1521(10),2495(9)),flip(a)]. given #298 (A,wt=19): 112 f(f(x,y),f(x,f(z,f(x,f(u,f(x,f(y,v))))))) = x. [para(31(a,1),22(a,1,2,1)),rewrite(2(6),31(14))]. given #299 (T,wt=15): 19947 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y). [back_rewrite(14688),rewrite(19917(12))]. given #300 (T,wt=15): 19954 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))). [para(18816(a,1),8(a,2)),rewrite(1521(5),2(4))]. given #301 (T,wt=15): 19961 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z. [para(18816(a,1),12(a,1,2)),rewrite(2(2),2(6))]. given #302 (T,wt=15): 20010 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))). [para(748(a,1),18816(a,2,2,2)),rewrite(2(5),19039(7),2368(6))]. given #303 (A,wt=19): 114 f(f(x,f(y,f(x,f(z,u)))),f(x,f(v,f(x,z)))) = x. [para(31(a,1),24(a,1,2,1)),rewrite(2(6),31(14))]. given #304 (T,wt=15): 20118 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))). [para(18816(a,1),1519(a,1))]. given #305 (T,wt=15): 20120 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)). [para(18816(a,1),1519(a,2,2)),rewrite(970(5),2(3)),flip(a)]. given #306 (T,wt=15): 20254 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(18816(a,2),5019(a,1,2,2,2,2)),rewrite(2349(11))]. given #307 (T,wt=15): 20315 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)). [para(18816(a,1),2256(a,2,2)),rewrite(2(4),1521(10),2495(9)),flip(a)]. given #308 (A,wt=25): 120 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 #309 (T,wt=15): 20904 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y. [para(18817(a,1),18820(a,1,1)),rewrite(763(7),756(7),2(5))]. given #310 (T,wt=15): 21131 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z. [para(19036(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #311 (T,wt=15): 21428 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),19038(a,1,2,2,2)),rewrite(19038(5)),flip(a)]. given #312 (T,wt=15): 21436 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))). [para(223(a,1),19038(a,1,2,2,2)),rewrite(2(2),19038(6),223(5),2(4)),flip(a)]. given #313 (A,wt=23): 121 f(f(f(x,y),f(y,z)),f(f(x,y),f(u,f(y,f(x,v))))) = f(x,y). [para(6(a,1),48(a,1,1,2,2)),rewrite(2(2),2(7))]. given #314 (T,wt=15): 23213 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(20010(a,1),5019(a,1,2,2,2,2)),rewrite(2(4),5873(10))]. given #315 (T,wt=15): 23953 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(21428(a,1),7453(a,1,2,2,2)),rewrite(2(4),2257(8))]. ============================== PROOF ================================= % Proof 1 at 91.36 (+ 0.13) seconds: "Sheffer". % Length of proof is 75. % Level of proof is 24. % Maximum clause weight is 43. % Given clauses 315. 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))]. 136 f(x,f(y,f(x,y))) = f(x,x). [para(48(a,1),73(a,1,2)),flip(a)]. 145 f(x,f(y,f(y,x))) = f(x,x). [para(136(a,1),2(a,2)),rewrite(2(1),2(3))]. 165 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),145(a,1,2,2)),rewrite(2(4),2(5)),flip(a)]. 212 f(x,f(f(x,f(y,z)),f(y,f(x,f(y,z))))) = f(x,x). [para(56(a,1),136(a,1,2,2)),rewrite(2(6))]. 213 f(x,f(y,y)) = f(x,f(x,y)). [para(136(a,1),56(a,1,2)),rewrite(2(3))]. 222 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(213(27),213(32))]. 223 f(x,f(y,y)) = f(x,f(y,x)). [para(213(a,1),2(a,2)),rewrite(2(2),2(3))]. 226 f(x,f(x,f(y,y))) = f(y,x). [para(213(a,1),9(a,1)),rewrite(2(2),223(2,R),2(4),223(4,R),2(6),6(6),2(3))]. 244 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x). [back_rewrite(212),rewrite(223(6,R),2(4))]. 275 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)). [para(226(a,1),11(a,1,2,1,2)),rewrite(23(6)),flip(a)]. 287 f(f(x,f(y,y)),f(f(y,z),f(y,z))) = f(y,z). [para(226(a,2),19(a,1)),rewrite(2(10),35(10),2(7),223(7,R))]. 400 f(x,f(y,f(x,f(z,f(x,y))))) = f(x,x). [para(48(a,1),59(a,1,2)),flip(a)]. 623 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x). [para(14(a,1),244(a,1,2,1)),rewrite(2(2))]. 642 f(x,f(y,f(y,y))) = f(x,x). [para(244(a,1),59(a,1)),flip(a)]. 652 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(222),unit_del(a,642)]. 657 f(f(x,x),f(y,f(y,y))) = x. [para(642(a,2),14(a,1))]. 665 f(x,f(x,x)) = f(y,f(y,y)). [para(642(a,1),36(a,1,1)),rewrite(223(7),2(5),657(5),2(2))]. 671 f(x,f(f(x,y),f(z,f(z,z)))) = f(x,y). [para(642(a,2),24(a,1,2)),rewrite(2(1),2(6))]. 714 f(x,f(x,x)) = c_0. [new_symbol(665)]. 748 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(671),rewrite(714(3),2(3))]. 756 f(c_0,f(x,x)) = x. [back_rewrite(657),rewrite(714(3),2(3))]. 763 f(x,c_0) = f(x,x). [back_rewrite(642),rewrite(714(2))]. 778 f(f(c1,f(c1,c2)),f(c1,f(c1,c3))) != f(c_0,f(c1,f(c2,c3))) # answer("Sheffer"). [back_rewrite(652),rewrite(763(11,R),2(7)),flip(a)]. 796 f(f(x,f(x,y)),f(x,f(y,z))) = f(c_0,f(x,f(y,z))). [back_rewrite(165),rewrite(763(5,R),2(4)),flip(a)]. 815 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z). [back_rewrite(287),rewrite(223(2),2(1),763(5,R),2(5))]. 943 f(f(x,f(y,y)),f(c_0,f(y,z))) = f(y,z). [para(35(a,1),223(a,2,2)),rewrite(763(7,R),2(7),756(7),2(5),19(5),2(8),223(8,R),763(6,R),2(6)),flip(a)]. 970 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(11(a,1),748(a,1,2)),rewrite(763(7,R),2(5),2(10),763(10),2(11),943(11))]. 1032 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x). [para(37(a,1),244(a,1,2,2,2)),rewrite(763(3,R),2(3),2(5))]. 1519 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))). [para(275(a,1),223(a,1,2)),rewrite(223(2),2(1),8(3),2(2),763(3,R),2(3),223(6),2(5),8(7),2(6))]. 1819 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)). [para(400(a,1),56(a,1,2)),rewrite(223(2),2(1),2(3)),flip(a)]. 1906 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)). [para(623(a,1),56(a,1,2)),rewrite(223(2),2(1)),flip(a)]. 2257 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),815(a,1,1,2)),rewrite(2(2),2(6),2(11))]. 2771 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(6(a,1),943(a,1,2,2)),rewrite(763(3,R),2(3),2(6),763(6),2(6),6(10))]. 2780 f(f(x,y),f(x,f(z,f(c_0,f(u,y))))) = x. [para(2771(a,1),9(a,1,2,2)),rewrite(2(7))]. 2786 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),2771(a,1,2,2,2)),rewrite(763(7,R),2(5),756(8),2(6),2(7))]. 2984 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x). [para(73(a,1),1032(a,1,2,2)),rewrite(2(4),763(4))]. 4444 f(x,f(c_0,f(y,f(z,f(x,y))))) = f(x,y). [para(1819(a,1),1519(a,2,2)),rewrite(8(9))]. 6406 f(f(c_0,f(x,y)),f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [para(2780(a,1),1906(a,1,2)),rewrite(2(4),2(11),2(12),223(13,R),763(10,R),2(10)),flip(a)]. 7453 f(x,f(c_0,f(y,f(z,f(y,x))))) = f(y,x). [para(4444(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. 7555 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)). [para(2984(a,1),4444(a,1,2,2,2)),rewrite(2(6),2786(8)),flip(a)]. 18336 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),7555(a,1,1)),rewrite(763(3,R),2(3),763(7,R),2(7),763(10,R),2(10)),flip(a)]. 18789 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6406),rewrite(18336(7))]. 19038 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(18789(a,2),1519(a,2,2)),rewrite(970(5),2(4)),flip(a)]. 21428 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),19038(a,1,2,2,2)),rewrite(19038(5)),flip(a)]. 23953 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(21428(a,1),7453(a,1,2,2,2)),rewrite(2(4),2257(8))]. 25013 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))). [para(21428(a,1),23953(a,1,2)),rewrite(2(3),796(5)),flip(a)]. 25014 $F # answer("Sheffer"). [resolve(25013,a,778,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=315. Generated=395302. Kept=25011. proofs=1. Usable=225. Sos=12961. Demods=11879. Limbo=152, Disabled=11675. Hints=0. Weight_deleted=374. Literals_deleted=0. Forward_subsumed=365215. Back_subsumed=2725. Sos_limit_deleted=4702. Sos_displaced=0. Sos_removed=0. New_demodulators=22904 (5 lex), Back_demodulated=8946. Back_unit_deleted=1. Demod_attempts=8926589. Demod_rewrites=1938752. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=28.54. User_CPU=91.36, System_CPU=0.13, Wall_clock=94. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 28135 exit (max_proofs) Fri Apr 13 10:00:44 2007