============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 6683 was started by mccune on cleo, Tue Nov 3 10:21:09 2009 The command was "/home/mccune/LADR/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(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,y) = f(y,x) # label(commutativity). [assumption]. f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [assumption]. f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) % Operation f is commutative; C redundancy checks enabled. kept: 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. kept: 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [assumption]. 4 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. kept: 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [copy(4),rewrite([2(25),2(30)]),flip(c)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 5 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) != f(f(c1,f(c2,c2)),f(c1,f(c3,c3))) # answer("Sheffer"). [copy(4),rewrite([2(25),2(30)]),flip(c)]. end_of_list. formulas(sos). 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [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.01 seconds. given #1 (I,wt=7): 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. given #2 (I,wt=11): 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [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)])]. 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,w))))))) = 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)])]. 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,w)))))) = f(f(x,y),f(u,f(x,f(y,w)))). [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,w))))))) = 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)])]. 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: function_order([ c1, c2, c3, c_0, f ]). given #48 (A,wt=27): 32 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(w,f(x,f(y,v5))))))))) = f(x,y). [para(7(a,1),7(a,1,2,1)),rewrite([2(7),7(17)])]. given #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(w,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(w,f(x,y))))) = f(f(x,f(y,z)),f(w,f(x,y))). [para(11(a,1),6(a,1,1)),rewrite([2(9)])]. given #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,w)))))) = f(f(x,y),f(u,f(y,f(x,w)))). [para(6(a,1),11(a,1,2,2,2)),rewrite([2(5),2(7),2(8),2(13)])]. given #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(w,f(f(x,f(y,z)),f(v5,f(x,y)))))))) = f(x,f(y,z)). [para(11(a,1),7(a,1,2,1)),rewrite([2(8),11(18)])]. given #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(w,f(x,f(z,v5)))))))) = f(x,f(u,f(f(x,z),f(w,f(x,f(z,v5)))))). [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(w,f(f(x,f(z,u)),f(v5,f(x,z))))))) = f(x,f(w,f(f(x,f(z,u)),f(v5,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,w))))))) = 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,w))))))) = 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,w)))))) = f(x,f(u,f(f(x,z),f(z,w)))). [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(w,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,w))))) = 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,w)))) = 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(w,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(w,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(w,z)))))) = f(x,f(u,f(f(x,z),f(w,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(w,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(w,f(x,f(x,y)))))))) = f(f(x,y),f(u,f(x,f(w,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(691),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(w,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(w,f(x,x))))))) = f(x,f(u,f(f(x,z),f(w,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): 11676 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): 12182 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): 12206 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(w,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(w,f(x,z))))) = f(f(x,f(y,z)),f(w,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): 13029 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(w,f(f(x,f(y,z)),f(v5,f(x,z)))))))) = f(x,f(y,z)). [para(23(a,1),7(a,1,2,1)),rewrite([2(8),23(18)])]. 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,w))))))) = f(x,y). [para(7(a,1),23(a,1,2,1)),rewrite([7(14)])]. 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(w,f(f(x,f(z,u)),f(v5,f(x,u))))))) = f(x,f(w,f(f(x,f(z,u)),f(v5,f(x,u))))). [para(23(a,1),11(a,1,2,2,2)),rewrite([2(6),2(11),2(18)])]. Low Water (keep): wt=93.000, iters=6679 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): wt=79.000, iters=6711 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,w)))))) = 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)]. given #253 (A,wt=23): 101 f(x,f(f(x,f(y,z)),f(u,f(x,f(w,f(x,y)))))) = f(x,f(y,z)). [para(11(a,1),23(a,1,2,1)),rewrite([11(14)])]. Low Water (keep): wt=67.000, iters=6741 Low Water (keep): wt=65.000, iters=6687 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)])]. 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)])]. Low Water (keep): wt=63.000, iters=6771 Low Water (keep): wt=61.000, iters=6686 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): wt=59.000, iters=6697 given #258 (A,wt=27): 102 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(w,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): wt=55.000, iters=6736 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): wt=53.000, iters=6668 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,w))))) = x. [para(1953(a,1),2255(a,1,1,2,2)),rewrite([2(3),756(3),2(5)])]. Low Water (keep): wt=51.000, iters=6746 given #263 (A,wt=27): 103 f(f(f(x,y),f(x,f(z,u))),f(f(x,f(z,u)),f(w,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): wt=49.000, iters=6770 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): wt=47.000, iters=6747 given #268 (A,wt=23): 105 f(x,f(f(x,f(y,z)),f(u,f(x,f(w,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(w,v5))))) = 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)]. Low Water (keep): wt=45.000, iters=6716 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,w)))) = 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(w,f(x,z)))) = f(x,f(y,f(x,f(z,u)))). [para(31(a,1),6(a,1,1)),rewrite([2(6)])]. given #274 (T,wt=17): 6722 f(f(x,y),f(y,f(z,f(f(x,u),f(x,w))))) = 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)])]. Low Water (keep): wt=43.000, iters=6679 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)]. given #278 (A,wt=25): 108 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(w,f(x,f(y,v5))))))))) = 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): 18743 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6406),rewrite([18323(7)])]. Low Water (keep): wt=41.000, iters=6803 given #282 (T,wt=15): 18761 f(x,f(c_0,f(y,z))) = f(y,f(c_0,f(x,z))). [para(18743(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(w,f(x,f(y,v5))))))))) = x. [para(7(a,1),31(a,1,1)),rewrite([2(7)])]. given #284 (T,wt=15): 18762 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(y,x))). [para(18743(a,1),2(a,2)),rewrite([2(4),2(6)])]. given #285 (T,wt=15): 18770 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))). [para(18743(a,1),8(a,2)),rewrite([1521(5)]),flip(a)]. given #286 (T,wt=15): 18771 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))). [para(18743(a,2),8(a,2)),rewrite([1521(5),2(5)]),flip(a)]. Low Water (keep): wt=39.000, iters=6762 given #287 (T,wt=15): 18774 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x. [para(18743(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(w,f(x,f(y,v5)))))))) = f(f(x,y),f(u,f(x,f(w,f(x,f(y,v5)))))). [para(31(a,1),11(a,1,2,2,2)),rewrite([2(7),2(9),2(10),2(17)])]. given #289 (T,wt=15): 18775 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x. [para(18743(a,2),9(a,1,2)),rewrite([2(4)])]. given #290 (T,wt=15): 18781 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x. [para(18743(a,1),12(a,1,2)),rewrite([2(2),2(4)])]. given #291 (T,wt=15): 18782 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x. [para(18743(a,2),12(a,1,2)),rewrite([2(2)])]. given #292 (T,wt=15): 18985 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))). [para(18743(a,2),1519(a,1))]. given #293 (A,wt=27): 111 f(f(x,f(y,z)),f(x,f(u,f(x,f(w,f(f(x,f(y,z)),f(v5,f(x,y)))))))) = x. [para(11(a,1),31(a,1,1)),rewrite([2(8)])]. given #294 (T,wt=15): 18986 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(18743(a,2),1519(a,2,2)),rewrite([970(5),2(4)]),flip(a)]. given #295 (T,wt=15): 19018 f(f(x,y),f(c_0,f(x,f(c_0,f(z,y))))) = c_0. [para(18743(a,1),2061(a,1,1,2)),rewrite([2(9),970(11),2(8)])]. given #296 (T,wt=15): 19175 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))). [para(18743(a,1),364(a,2)),rewrite([2(12),9819(15),2(5)]),flip(a)]. given #297 (T,wt=15): 19225 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)). [para(18743(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,w))))))) = x. [para(31(a,1),22(a,1,2,1)),rewrite([2(6),31(14)])]. given #299 (T,wt=15): 19880 f(f(x,f(x,y)),f(c_0,f(z,y))) = f(z,y). [back_rewrite(14738),rewrite([19850(12)])]. given #300 (T,wt=15): 19887 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))). [para(18770(a,1),8(a,2)),rewrite([1521(5),2(4)])]. given #301 (T,wt=15): 19894 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z. [para(18770(a,1),12(a,1,2)),rewrite([2(2),2(6)])]. given #302 (T,wt=15): 19939 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))). [para(748(a,1),18770(a,2,2,2)),rewrite([2(5),18987(7),2368(6)])]. given #303 (A,wt=19): 114 f(f(x,f(y,f(x,f(z,u)))),f(x,f(w,f(x,z)))) = x. [para(31(a,1),24(a,1,2,1)),rewrite([2(6),31(14)])]. given #304 (T,wt=15): 20046 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))). [para(18770(a,1),1519(a,1))]. given #305 (T,wt=15): 20048 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)). [para(18770(a,1),1519(a,2,2)),rewrite([970(5),2(3)]),flip(a)]. given #306 (T,wt=15): 20181 f(f(x,y),f(c_0,f(y,f(c_0,f(z,x))))) = c_0. [para(18770(a,2),5019(a,1,2,2,2,2)),rewrite([2349(11)])]. given #307 (T,wt=15): 20241 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)). [para(18770(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,w))))) = f(x,f(y,f(x,z))). [para(48(a,1),3(a,1,1)),rewrite([2(6)])]. given #309 (T,wt=15): 20785 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y. [para(18771(a,1),18774(a,1,1)),rewrite([763(7),756(7),2(5)])]. given #310 (T,wt=15): 21001 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z. [para(18985(a,1),12(a,1,2)),rewrite([2(2),2(3),2(6)])]. given #311 (T,wt=15): 21298 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),18986(a,1,2,2,2)),rewrite([18986(5)]),flip(a)]. given #312 (T,wt=15): 21306 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))). [para(223(a,1),18986(a,1,2,2,2)),rewrite([2(2),18986(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,w))))) = f(x,y). [para(6(a,1),48(a,1,1,2,2)),rewrite([2(2),2(7)])]. given #314 (T,wt=15): 23068 f(f(x,y),f(c_0,f(y,f(y,f(z,x))))) = c_0. [para(19939(a,1),5019(a,1,2,2,2,2)),rewrite([2(4),5873(10)])]. given #315 (T,wt=15): 23790 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(21298(a,1),7453(a,1,2,2,2)),rewrite([2(4),2257(8)])]. ============================== PROOF ================================= % Proof 1 at 96.52 (+ 0.20) seconds: "Sheffer". % Length of proof is 75. % Level of proof is 24. % Maximum clause weight is 43.000. % 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(non_clause) # label(goal). [goal]. 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [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)]. 18323 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)]. 18743 f(x,f(c_0,f(y,z))) = f(z,f(c_0,f(x,y))). [back_rewrite(6406),rewrite([18323(7)])]. 18986 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)). [para(18743(a,2),1519(a,2,2)),rewrite([970(5),2(4)]),flip(a)]. 21298 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)). [para(8(a,1),18986(a,1,2,2,2)),rewrite([18986(5)]),flip(a)]. 23790 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))). [para(21298(a,1),7453(a,1,2,2,2)),rewrite([2(4),2257(8)])]. 24821 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))). [para(21298(a,1),23790(a,1,2)),rewrite([2(3),796(5)]),flip(a)]. 24822 $F # answer("Sheffer"). [resolve(24821,a,778,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=315. Generated=389256. Kept=24819. proofs=1. Usable=225. Sos=12843. Demods=11780. Limbo=150, Disabled=11603. Hints=0. Kept_by_rule=0, Deleted_by_rule=374. Forward_subsumed=358978. Back_subsumed=2715. Sos_limit_deleted=5085. Sos_displaced=0. Sos_removed=0. New_demodulators=22739 (5 lex), Back_demodulated=8884. Back_unit_deleted=1. Demod_attempts=8827639. Demod_rewrites=1908173. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=28.68. User_CPU=96.52, System_CPU=0.20, Wall_clock=98. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6683 exit (max_proofs) Tue Nov 3 10:22:47 2009