============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 28060 was started by mccune on cleo, Fri Apr 13 09:56:39 2007 The command was "/home/mccune/bin/prover9 -f dist-long-short.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-long-short.in assign(max_seconds,300). assign(order,kbo). set(lex_order_vars). formulas(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long). end_of_list. formulas(goals). f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # answer(dist_short). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # answer(dist_short) # 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,x,y) = x # label(majority). [assumption]. f(x,y,z) = f(z,x,y) # label(2a). [assumption]. f(x,y,z) = f(x,z,y) # label(2b). [assumption]. f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long). [assumption]. f(f(c1,c2,c3),c4,c5) != f(c1,f(c2,c4,c5),f(c3,c4,c5)) # answer(dist_short). [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: Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. 8 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2),3(3),3(3))]. 10 f(c1,f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_short). [copy(9),rewrite(3(7),3(7)),flip(a)]. end_of_list. formulas(demodulators). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. % (lex-dep) 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. % (lex-dep) 8 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2),3(3),3(3))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 2 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=9): 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. given #3 (I,wt=9): 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. given #4 (I,wt=15): 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. given #5 (I,wt=21): 8 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2),3(3),3(3))]. given #6 (I,wt=18): 10 f(c1,f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_short). [copy(9),rewrite(3(7),3(7)),flip(a)]. given #7 (A,wt=6): 11 f(x,y,y) = y. [para(3(a,1),2(a,1))]. given #8 (T,wt=12): 28 f(x,y,f(x,z,y)) = f(x,z,y). [para(11(a,1),6(a,1,3)),flip(a)]. given #9 (T,wt=12): 29 f(x,y,f(x,y,z)) = f(x,y,z). [para(11(a,1),6(a,1)),rewrite(4(3),28(3)),flip(a)]. given #10 (T,wt=15): 12 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(6(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. given #11 (T,wt=15): 13 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(3(a,1),6(a,1,3)),rewrite(3(1,R),4(1))]. given #12 (A,wt=21): 14 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(6(a,1),6(a,1,3))]. given #13 (T,wt=15): 38 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(12(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3))]. given #14 (T,wt=15): 39 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(3(a,1),12(a,1)),rewrite(3(2),3(2),4(3))]. given #15 (T,wt=15): 51 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(3(a,1),13(a,1)),rewrite(3(2),3(2),4(3))]. given #16 (T,wt=18): 30 f(x,f(y,x,z),f(u,y,x)) = f(y,x,f(u,x,z)). [para(11(a,1),8(a,1,2)),rewrite(3(3,R))]. given #17 (A,wt=21): 16 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)). [para(8(a,1),3(a,1)),rewrite(3(4),3(4)),flip(a)]. given #18 (T,wt=15): 187 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_rewrite(135),rewrite(3(1,R),4(1),3(2,R),4(2),183(4),3(1,R),4(1),3(4,R),4(4))]. given #19 (T,wt=15): 189 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(187(a,1),3(a,2)),rewrite(4(3),3(4,R),4(4))]. given #20 (T,wt=15): 190 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(3(a,1),187(a,1)),rewrite(3(1,R),4(1),3(3),3(3),4(4))]. given #21 (T,wt=15): 200 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(187(a,1),13(a,1)),flip(a)]. given #22 (A,wt=21): 17 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)). [para(3(a,1),8(a,1,1)),rewrite(3(2,R),4(2),3(3,R),4(3),3(6,R),4(6))]. given #23 (T,wt=15): 204 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),187(a,2)),rewrite(4(3),198(5))]. given #24 (T,wt=12): 321 f(x,y,f(z,x,y)) = f(z,x,y). [para(11(a,1),204(a,1)),rewrite(29(3)),flip(a)]. given #25 (T,wt=15): 226 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(189(a,1),187(a,2)),rewrite(4(5),198(7))]. given #26 (T,wt=15): 236 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(200(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #27 (A,wt=33): 18 f(f(x,y,z),f(y,z,u),f(v,f(y,z,w),f(x,y,z))) = f(v,f(x,y,z),f(y,z,f(x,u,w))). [para(8(a,1),6(a,1,3)),rewrite(3(4,R),4(4),3(9,R)),flip(a)]. given #28 (T,wt=15): 237 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(3(a,1),200(a,1,2))]. given #29 (T,wt=15): 238 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(3(a,2),200(a,1,2)),rewrite(4(2),4(4))]. given #30 (T,wt=15): 239 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(200(a,1),4(a,1)),flip(a)]. given #31 (T,wt=15): 320 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(204(a,1),3(a,2)),rewrite(4(2),3(3)),flip(a)]. given #32 (A,wt=33): 19 f(f(x,y,f(x,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(x,v,w)). [para(6(a,1),8(a,1,1)),rewrite(4(4),4(6))]. given #33 (T,wt=15): 338 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para(226(a,1),3(a,2)),rewrite(3(1,R),4(1),4(3),3(4))]. given #34 (T,wt=15): 351 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(226(a,1),204(a,1)),flip(a)]. given #35 (T,wt=15): 353 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(204(a,1),226(a,2)),rewrite(4(3),3(4,R),4(4),233(5),3(3)),flip(a)]. given #36 (T,wt=15): 354 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para(226(a,1),226(a,2)),rewrite(3(1,R),4(1),3(3,R),4(3),4(5),3(6,R),4(6),233(7),3(4))]. given #37 (A,wt=27): 20 f(f(x,y,z),f(y,u,f(y,z,v)),f(y,z,w)) = f(y,z,f(x,w,f(y,u,v))). [para(6(a,1),8(a,1,2)),rewrite(4(7))]. given #38 (T,wt=15): 355 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(236(a,1),4(a,1)),flip(a)]. given #39 (T,wt=15): 497 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(237(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #40 (T,wt=15): 499 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(237(a,1),6(a,2)),rewrite(3(1,R),4(1),4(2))]. given #41 (T,wt=15): 505 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(237(a,1),8(a,2)),rewrite(2(2),4(2),4(4),83(5),11(3))]. given #42 (A,wt=27): 21 f(f(x,y,z),f(y,z,u),f(y,v,f(y,z,w))) = f(y,z,f(x,u,f(y,v,w))). [para(6(a,1),8(a,1,3))]. given #43 (T,wt=15): 533 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(189(a,1),237(a,1,3)),rewrite(4(5),315(5),3(2),3(2),189(6))]. given #44 (T,wt=15): 550 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(238(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #45 (T,wt=15): 619 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(320(a,1),3(a,2)),rewrite(4(2),3(3))]. given #46 (T,wt=15): 758 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(321(a,1),19(a,1,2)),rewrite(29(2),2(5)),flip(a)]. given #47 (A,wt=21): 22 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(6(a,1),8(a,2,3)),rewrite(8(5))]. given #48 (T,wt=15): 832 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(353(a,1),3(a,2)),rewrite(4(2),3(3))]. given #49 (T,wt=15): 838 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(16(a,1),353(a,1)),rewrite(4(2),36(3),11(1),83(5),29(5),125(5),4(3)),flip(a)]. given #50 (T,wt=15): 841 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(353(a,1),226(a,2)),rewrite(4(3),3(4,R),4(4),634(5),3(3))]. given #51 (T,wt=15): 1065 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(3(a,1),505(a,1)),rewrite(3(1),3(3),3(3),4(4))]. given #52 (A,wt=45): 23 f(f(x,y,f(z,u,v)),f(w,f(x,y,u),f(x,y,v)),f(v6,f(x,y,u),f(x,y,v))) = f(f(x,y,u),f(x,y,v),f(w,v6,f(x,y,z))). [para(8(a,1),8(a,1,1)),rewrite(3(5),3(8),3(12),3(12),3(13),3(13))]. given #53 (T,wt=15): 1199 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(3(a,1),533(a,1)),rewrite(3(2),3(2),3(3,R),3(4),3(4))]. given #54 (T,wt=15): 1247 f(x,f(y,x,z),f(u,y,z)) = f(y,x,z). [para(351(a,1),619(a,1,3)),rewrite(11(3),178(6),3(4,R),4(4),822(5),3(3,R),4(3)),flip(a)]. given #55 (T,wt=18): 31 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)). [para(11(a,1),8(a,1,3)),rewrite(3(3),4(4))]. given #56 (T,wt=18): 36 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,v,u)). [para(28(a,1),8(a,1,2)),rewrite(4(2),8(4),4(3),4(4)),flip(a)]. given #57 (A,wt=45): 24 f(f(x,f(y,z,u),f(z,u,v)),f(z,u,f(y,v,w)),f(v6,f(y,z,u),f(z,u,v))) = f(f(y,z,u),f(z,u,v),f(x,v6,f(z,u,w))). [para(8(a,1),8(a,1,2)),rewrite(3(8),4(13))]. given #58 (T,wt=18): 165 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)). [para(28(a,1),16(a,1,1)),rewrite(17(4)),flip(a)]. given #59 (T,wt=18): 212 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(6(a,1),189(a,1,3,3))]. given #60 (T,wt=18): 219 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(12(a,2),189(a,1,3,3))]. given #61 (T,wt=18): 249 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(12(a,1),200(a,1,2))]. given #62 (A,wt=45): 25 f(f(x,f(y,z,u),f(z,u,v)),f(w,f(y,z,u),f(z,u,v)),f(z,u,f(y,v,v6))) = f(f(y,z,u),f(z,u,v),f(x,w,f(z,u,v6))). [para(8(a,1),8(a,1,3)),rewrite(3(6))]. given #63 (T,wt=18): 261 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(39(a,1),200(a,1,2))]. given #64 (T,wt=18): 288 f(x,f(y,z,x),f(y,x,u)) = f(y,x,f(z,x,u)). [para(11(a,1),17(a,1,3)),rewrite(3(3),4(4))]. given #65 (T,wt=18): 335 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(321(a,1),16(a,1,1)),rewrite(8(4)),flip(a)]. given #66 (T,wt=18): 359 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(28(a,1),236(a,1,3)),rewrite(28(6))]. given #67 (A,wt=27): 26 f(x,y,f(f(z,u,v),f(z,u,w),f(v6,z,u))) = f(x,y,f(z,u,f(v6,v,w))). [para(8(a,1),8(a,2,3)),rewrite(3(2),3(2),16(7))]. given #68 (T,wt=18): 528 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(237(a,1),187(a,2)),rewrite(3(5),183(6),513(6))]. given #69 (T,wt=15): 2835 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(2(a,1),528(a,1,2,3)),rewrite(4(2),4(4))]. given #70 (T,wt=15): 2892 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(236(a,1),528(a,1,3)),rewrite(3(1),3(3),3(5,R),4(5),3(6),4(7),1318(7),2560(7),3(3)),flip(a)]. given #71 (T,wt=18): 535 f(x,y,f(x,z,f(z,u,f(v,y,z)))) = f(x,y,z). [para(237(a,1),200(a,1,3)),rewrite(3(3),4(5),183(5),237(7))]. given #72 (A,wt=21): 40 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(12(a,2),6(a,1,3))]. given #73 (T,wt=18): 545 f(x,y,f(x,z,f(u,z,f(v,y,z)))) = f(x,y,z). [para(237(a,1),237(a,1,3)),rewrite(4(5),183(5),3(2,R),4(2),237(7))]. given #74 (T,wt=18): 570 f(x,f(y,z,f(u,v,y)),f(x,u,y)) = f(x,u,y). [para(238(a,1),187(a,2)),rewrite(3(5),183(6),558(6))]. given #75 (T,wt=18): 575 f(x,y,f(x,z,f(z,u,f(y,v,z)))) = f(x,y,z). [para(238(a,1),200(a,1,3)),rewrite(3(3),4(5),183(5),238(7))]. given #76 (T,wt=18): 586 f(x,y,f(x,z,f(u,z,f(y,v,z)))) = f(x,y,z). [para(238(a,1),237(a,1,3)),rewrite(4(5),183(5),3(2,R),4(2),238(7))]. given #77 (A,wt=33): 41 f(f(x,y,f(y,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(y,v,w)). [para(12(a,1),8(a,1,1)),rewrite(4(4),4(6))]. given #78 (T,wt=15): 3604 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [para(528(a,1),41(a,2)),rewrite(3(1),2(2),11(1),3(1),3(4),3(6,R),4(6),29(6),4(6),28(6),3(4))]. given #79 (T,wt=18): 662 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [back_rewrite(252),rewrite(648(4))]. given #80 (T,wt=18): 857 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x). [back_rewrite(828),rewrite(849(5))]. given #81 (T,wt=18): 1221 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(550(a,1),351(a,1,3)),rewrite(4(3),4(5),849(5),550(7))]. given #82 (A,wt=27): 43 f(f(x,y,z),f(z,u,f(y,z,v)),f(y,z,w)) = f(y,z,f(x,w,f(z,u,v))). [para(12(a,2),8(a,1,2)),rewrite(4(7))]. given #83 (T,wt=18): 1369 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(351(a,1),832(a,1,3)),rewrite(11(3),1235(6)),flip(a)]. given #84 (T,wt=18): 1671 f(x,y,f(x,z,f(y,u,f(v,y,z)))) = f(x,y,z). [para(1199(a,1),1065(a,2)),rewrite(3(2),3(3),3(5,R),1318(6),165(5),513(6),648(4),3(5))]. given #85 (T,wt=18): 2135 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(212(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5),3(5))]. given #86 (T,wt=18): 2148 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y). [para(212(a,1),16(a,2)),rewrite(11(4),3(5),3(5),1711(5),29(4))]. given #87 (A,wt=27): 44 f(f(x,y,z),f(y,z,u),f(z,v,f(y,z,w))) = f(y,z,f(x,u,f(z,v,w))). [para(12(a,2),8(a,1,3))]. given #88 (T,wt=18): 2150 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(212(a,1),189(a,2)),rewrite(4(7),1318(8),165(7),3(3,R),4(3),1364(6))]. given #89 (T,wt=18): 2196 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(219(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5),3(5))]. given #90 (T,wt=18): 2207 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(39(a,2),219(a,1,3))]. given #91 (T,wt=18): 2209 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(219(a,1),16(a,2)),rewrite(11(4),3(5),3(5),1711(5),29(4))]. given #92 (A,wt=21): 46 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))). [para(12(a,2),8(a,2,3)),rewrite(8(5)),flip(a)]. given #93 (T,wt=18): 2212 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(219(a,1),189(a,2)),rewrite(4(7),1318(8),165(7),3(3,R),4(3),1364(6))]. given #94 (T,wt=18): 2254 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(249(a,1),3(a,2)),rewrite(3(3),3(3),3(4),3(5),3(5))]. given #95 (T,wt=15): 4798 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(2254(a,1),619(a,1,3)),rewrite(11(3),3(4,R),4(4),368(7),3(5,R),4(5),3748(6),3(2),3(3,R),4(3)),flip(a)]. given #96 (T,wt=18): 2372 f(x,y,f(z,f(u,y,z),f(x,u,z))) = f(x,y,z). [para(11(a,1),25(a,2)),rewrite(3(1,R),4(1),29(3),1318(3),29(2),3(3,R),4(3),29(5),288(5),4(6),36(7),11(5),3(6),157(6),29(6))]. given #97 (A,wt=33): 48 f(f(x,y,z),f(y,z,u),f(v,f(x,y,z),f(y,z,w))) = f(v,f(x,y,z),f(y,z,f(x,u,w))). [para(8(a,1),12(a,2,3))]. given #98 (T,wt=18): 2520 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(261(a,1),3(a,2)),rewrite(3(3),3(3),3(4),3(5),3(5))]. given #99 (T,wt=18): 2524 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(261(a,1),8(a,2)),rewrite(2(3),4(3),4(6),1318(7),28(6))]. given #100 (T,wt=18): 2836 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(528(a,1),3(a,1)),rewrite(3(3),3(3),3(5,R)),flip(a)]. given #101 (T,wt=18): 2837 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(528(a,1),3(a,2)),rewrite(3(1),3(3),4(3),3(4),3(5),4(5))]. given #102 (A,wt=21): 50 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(12(a,1),12(a,1,3)),rewrite(3(1,R),4(1),3(6,R),4(6))]. given #103 (T,wt=18): 2838 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(3(a,1),528(a,1,2,3)),rewrite(4(3),4(5))]. given #104 (T,wt=18): 2839 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(3(a,2),528(a,1,2,3)),rewrite(3(1,R),4(1),4(3),4(5))]. given #105 (T,wt=18): 2840 f(x,f(y,z,f(u,v,z)),f(x,v,z)) = f(x,v,z). [para(3(a,2),528(a,1,2)),rewrite(4(2))]. given #106 (T,wt=18): 2849 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(528(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1318(7),28(6),4(5))]. given #107 (A,wt=21): 52 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(13(a,2),6(a,1,3))]. given #108 (T,wt=18): 2992 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(39(a,2),535(a,1,3)),rewrite(3(1),3(1))]. given #109 (T,wt=18): 3297 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(570(a,1),3(a,2)),rewrite(3(1),3(3),4(3),3(4),3(5),4(5))]. given #110 (T,wt=18): 3298 f(x,f(y,z,f(u,v,z)),f(x,u,z)) = f(x,u,z). [para(3(a,2),570(a,1,2)),rewrite(4(2))]. given #111 (T,wt=18): 3653 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(3604(a,1),355(a,1,2)),rewrite(3(5,R),1188(5),3604(7))]. given #112 (A,wt=21): 53 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))). [para(13(a,1),6(a,2,3)),flip(a)]. given #113 (T,wt=18): 3845 f(x,y,f(z,f(x,z,y),f(u,z,y))) = f(x,z,y). [para(1221(a,1),38(a,1,3)),rewrite(11(3),4(4),3748(7),3(3)),flip(a)]. given #114 (T,wt=18): 4090 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [para(1369(a,1),16(a,2)),rewrite(11(4),3(5),3(5),1711(5),29(4))]. given #115 (T,wt=18): 4151 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(2148(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5))]. given #116 (T,wt=18): 4455 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(2207(a,1),4(a,2)),rewrite(3(2,R),4(2),3473(3),4(4),4(5))]. given #117 (A,wt=33): 55 f(f(x,y,f(x,z,u)),f(u,v,f(x,y,z)),f(u,w,f(x,y,z))) = f(u,f(x,y,z),f(x,v,w)). [para(13(a,2),8(a,1,1)),rewrite(4(4),4(6))]. given #118 (T,wt=18): 4582 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(2209(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5))]. given #119 (T,wt=18): 4718 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(3(a,2),2212(a,1,2)),rewrite(4(2),3(3,R),4(3),3(5,R),4(5))]. given #120 (T,wt=18): 4791 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(2254(a,1),353(a,1)),rewrite(3(3,R),4(3)),flip(a)]. given #121 (T,wt=18): 4823 f(x,f(y,z,f(z,u,v)),f(z,x,u)) = f(z,x,u). [para(2254(a,1),41(a,2)),rewrite(2(9),3(7),3388(7),4(5))]. given #122 (A,wt=21): 56 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))). [para(13(a,1),8(a,2,3)),rewrite(8(5))]. given #123 (T,wt=18): 4857 f(x,y,f(z,f(y,u,z),f(x,u,z))) = f(x,y,z). [para(3(a,1),2372(a,1,3)),rewrite(3(2,R),4(2),3(3,R))]. given #124 (T,wt=18): 4927 f(x,y,f(z,f(x,u,z),f(y,u,z))) = f(x,y,z). [para(2372(a,1),165(a,2)),rewrite(3(1,R),4(1),4(3),36(5),3(3,R))]. given #125 (T,wt=18): 5246 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(2520(a,1),8(a,2)),rewrite(3(2,R),4(2),3(5,R),4(5),4(6),3(8,R),4(8),3(9),2(9),3(7),3473(7),29(7),4(5))]. given #126 (T,wt=18): 5263 f(x,f(y,z,f(z,u,v)),f(z,x,v)) = f(z,x,v). [para(2520(a,1),41(a,2)),rewrite(2(9),3(7),3388(7),4(5))]. given #127 (A,wt=21): 60 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(12(a,2),13(a,1,3)),flip(a)]. given #128 (T,wt=18): 5272 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(3(a,1),2524(a,1)),rewrite(3(1),3(4),3(4),4(5))]. given #129 (T,wt=18): 5580 f(x,y,f(x,z,f(u,z,f(z,v,y)))) = f(x,z,y). [para(2840(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1318(7),28(6),4(5))]. given #130 (T,wt=18): 5914 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(3298(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1318(7),28(6),4(5))]. given #131 (T,wt=18): 6212 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y). [para(4151(a,1),38(a,1)),flip(a)]. given #132 (A,wt=21): 62 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(14(a,1),3(a,2)),rewrite(4(3),3(5,R),4(5)),flip(a)]. given #133 (T,wt=18): 6252 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(3(a,1),4455(a,1)),rewrite(3(1,R),4(1),3(4),3(4),3(5,R),4(5))]. given #134 (T,wt=18): 6261 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(13(a,1),4455(a,1,3)),rewrite(4(1),4(5))]. given #135 (T,wt=18): 6664 f(x,y,f(z,y,f(z,u,f(v,z,x)))) = f(z,x,y). [para(4823(a,1),41(a,2)),rewrite(2(6),3(7,R),1318(7),3656(6),11(2),1318(3))]. given #136 (T,wt=18): 6873 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(5246(a,1),8(a,2)),rewrite(3(6),2(6),4(6),3(7,R),1318(7),321(6))]. given #137 (A,wt=21): 63 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(14(a,2),3(a,2)),rewrite(4(3),3(4,R),4(4))]. given #138 (T,wt=18): 6875 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(12(a,1),5246(a,1)),rewrite(4(3))]. given #139 (T,wt=18): 6877 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(5246(a,1),19(a,2)),rewrite(2(6),3(7,R),1318(7),1378(6),4(3),321(4))]. given #140 (T,wt=18): 6895 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [para(28(a,1),5263(a,1,3)),rewrite(3(1),3(4),4(5),1318(5),5433(5),4(1),3(5),3(6,R),4(6),29(6))]. given #141 (T,wt=18): 6899 f(x,y,f(z,u,f(z,y,f(v,z,x)))) = f(z,x,y). [para(5263(a,1),41(a,2)),rewrite(2(6),3(7,R),1318(7),3656(6),11(2),1318(3))]. given #142 (A,wt=27): 64 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,u,f(x,y,f(x,v,f(x,z,w)))). [para(14(a,1),6(a,1,3))]. given #143 (T,wt=18): 7332 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [back_rewrite(4554),rewrite(7216(10))]. given #144 (T,wt=18): 8203 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(3(a,1),6895(a,1)),rewrite(3(2,R),4(2),3(4),3(4),3(5,R),4(5))]. given #145 (T,wt=21): 65 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,z,f(x,y,v))). [para(14(a,1),6(a,1))]. given #146 (T,wt=21): 87 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,v,f(x,y,z))). [para(13(a,1),14(a,2,3))]. given #147 (A,wt=27): 66 f(x,y,f(x,z,f(x,u,f(x,v,w)))) = f(x,v,f(x,y,f(x,z,f(x,u,w)))). [para(14(a,2),6(a,1,3))]. given #148 (T,wt=21): 96 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(6(a,1),38(a,1,3)),rewrite(3(1,R),4(1),3(6,R),4(6))]. given #149 (T,wt=18): 9590 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(497(a,1),96(a,2,3)),rewrite(3(3),4(3),335(4),3(2,R),4(2),2670(4),3(2),2(2),4(2),3(4),3(5,R)),flip(a)]. given #150 (T,wt=21): 97 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,u,v))). [para(6(a,1),38(a,2,3)),rewrite(3(2,R),4(2),3(6,R),4(6)),flip(a)]. given #151 (T,wt=21): 102 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(12(a,1),38(a,1,3)),rewrite(3(1,R),4(1),3(6,R),4(6))]. given #152 (A,wt=45): 67 f(f(x,y,f(x,z,f(x,u,v))),f(z,w,f(x,u,f(x,y,v))),f(z,v6,f(x,u,f(x,y,v)))) = f(z,f(x,u,f(x,y,v)),f(x,w,v6)). [para(14(a,1),8(a,1,1)),rewrite(4(6),4(9))]. given #153 (T,wt=18): 10151 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(497(a,1),102(a,2,3)),rewrite(3(3),4(3),335(4),3(2,R),4(2),2670(4),11(2),4(2),3(4),3(5,R)),flip(a)]. given #154 (T,wt=18): 10159 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(550(a,1),102(a,2,3)),rewrite(3(3),4(3),165(4),3(2,R),4(2),2128(4),11(2),4(2),3(4),3(5,R)),flip(a)]. given #155 (T,wt=21): 103 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))). [para(38(a,1),13(a,1,3)),flip(a)]. given #156 (T,wt=21): 104 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))). [para(13(a,1),38(a,2,3)),rewrite(3(2,R),4(2),3(6,R),4(6)),flip(a)]. given #157 (A,wt=45): 69 f(f(x,y,f(x,z,f(x,u,v))),f(u,w,f(x,y,f(x,z,v))),f(u,v6,f(x,y,f(x,z,v)))) = f(u,f(x,y,f(x,z,v)),f(x,w,v6)). [para(14(a,2),8(a,1,1)),rewrite(4(6),4(9))]. given #158 (T,wt=21): 110 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))). [para(39(a,2),6(a,2,3)),flip(a)]. Low Water (keep, True_semantics): wt=93 given #159 (T,wt=21): 112 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))). [para(39(a,2),8(a,2,3)),rewrite(8(5)),flip(a)]. given #160 (T,wt=21): 117 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))). [para(39(a,2),38(a,2,3)),rewrite(3(2,R),4(2),3(6,R),4(6))]. given #161 (T,wt=21): 118 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))). [para(38(a,1),39(a,2,3)),rewrite(3(2),3(2),3(6,R),4(6))]. given #162 (A,wt=33): 70 f(f(x,y,z),f(y,u,f(y,v,f(y,z,w))),f(y,z,v6)) = f(y,z,f(x,v6,f(y,u,f(y,v,w)))). [para(14(a,2),8(a,1,2)),rewrite(4(9))]. Low Water (keep, True_semantics): wt=90 given #163 (T,wt=21): 120 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))). [para(6(a,1),51(a,2,3)),rewrite(83(3),4(1),4(4))]. given #164 (T,wt=21): 121 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))). [para(13(a,1),51(a,2,3)),rewrite(83(3),4(1),4(4))]. given #165 (T,wt=21): 171 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(13(a,1),16(a,2,3)),rewrite(3(5,R),16(5),3(2),4(4))]. given #166 (T,wt=21): 194 f(x,y,f(z,u,f(x,v,f(y,v,w)))) = f(x,y,f(z,v,u)). [para(187(a,1),8(a,1,2)),rewrite(8(4),4(5)),flip(a)]. given #167 (A,wt=33): 71 f(f(x,y,z),f(y,z,u),f(y,v,f(y,w,f(y,z,v6)))) = f(y,z,f(x,u,f(y,v,f(y,w,v6)))). [para(14(a,2),8(a,1,3))]. Low Water (keep, True_semantics): wt=81 Low Water (keep, True_semantics): wt=78 Low Water (keep, True_semantics): wt=75 given #168 (T,wt=18): 13237 f(x,f(y,z,f(u,y,v)),f(x,y,v)) = f(x,y,v). [para(237(a,1),194(a,2)),rewrite(3(3),3(3),5984(6))]. given #169 (T,wt=18): 13640 f(x,f(y,z,f(u,z,v)),f(x,z,v)) = f(x,z,v). [para(3(a,2),13237(a,1,2)),rewrite(4(2))]. given #170 (T,wt=21): 215 f(x,y,f(z,u,f(y,v,f(x,v,w)))) = f(x,y,f(z,v,u)). [para(189(a,1),8(a,1,2)),rewrite(8(4),4(5)),flip(a)]. Low Water (keep, True_semantics): wt=72 given #171 (T,wt=18): 13743 f(x,y,f(z,u,f(v,z,f(x,z,y)))) = f(x,z,y). [para(237(a,1),215(a,2)),rewrite(3(4,R),11122(4),13700(6))]. given #172 (A,wt=27): 72 f(x,y,f(z,u,f(z,v,f(z,w,v6)))) = f(x,y,f(z,w,f(z,u,f(z,v,v6)))). [para(14(a,1),8(a,2,3)),rewrite(8(6))]. Low Water (keep, True_semantics): wt=69 given #173 (T,wt=21): 220 f(x,f(y,z,f(x,z,u)),f(x,v,y)) = f(x,v,f(x,y,z)). [para(189(a,1),13(a,1,3)),flip(a)]. given #174 (T,wt=21): 222 f(x,y,f(y,z,f(x,u,f(x,v,f(x,z,w))))) = f(x,y,z). [para(14(a,2),189(a,1,3,3))]. given #175 (T,wt=21): 235 f(x,y,f(z,u,f(x,v,f(v,y,w)))) = f(x,y,f(v,z,u)). [para(190(a,1),16(a,1,1)),rewrite(17(4)),flip(a)]. given #176 (T,wt=21): 271 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(200(a,1),187(a,1,3,3))]. given #177 (A,wt=24): 76 f(x,y,f(x,z,f(x,u,f(x,v,y)))) = f(x,z,f(x,u,f(x,v,y))). [para(28(a,1),14(a,1,3,3)),flip(a)]. given #178 (T,wt=18): 14714 f(x,y,f(z,f(x,y,z),f(u,v,w))) = f(x,y,z). [para(271(a,1),6261(a,1,3))]. given #179 (T,wt=18): 14909 f(x,y,f(z,f(x,z,y),f(u,v,w))) = f(x,z,y). [para(14714(a,1),3(a,2)),rewrite(3(1),3(1),4(4),3(5),3(5))]. given #180 (T,wt=21): 273 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(200(a,1),189(a,1,3,3))]. given #181 (T,wt=18): 15228 f(x,y,f(z,f(y,z,u),f(x,v,z))) = f(x,y,z). [para(6895(a,1),273(a,2)),rewrite(3(1),4(5),848(5),36(5),4(5))]. Low Water (keep, True_semantics): wt=66 given #182 (A,wt=27): 78 f(x,y,f(z,u,f(x,z,f(z,v,w)))) = f(x,z,f(x,y,f(z,v,f(z,u,w)))). [para(14(a,1),12(a,1,3)),rewrite(3(2,R),4(2),3(8,R),4(8))]. given #183 (T,wt=21): 275 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(200(a,1),190(a,1,3,3)),rewrite(3(2),3(2))]. Low Water (keep, True_semantics): wt=63 given #184 (T,wt=18): 15825 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,u,x)). [para(275(a,1),24(a,2)),rewrite(2(4),48(7),4(3),29(3),5050(4),3(5,R)),flip(a)]. given #185 (T,wt=18): 16006 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(9859),rewrite(15767(5),15825(3),3(1)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 78.24 (+ 0.11) seconds: dist_short. % Length of proof is 110. % Level of proof is 19. % Maximum clause weight is 45. % Given clauses 185. 1 f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # answer(dist_short) # label(goal). [goal]. 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 5 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. 7 f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long). [assumption]. 8 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2),3(3),3(3))]. 9 f(f(c1,c2,c3),c4,c5) != f(c1,f(c2,c4,c5),f(c3,c4,c5)) # answer(dist_short). [deny(1)]. 10 f(c1,f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_short). [copy(9),rewrite(3(7),3(7)),flip(a)]. 11 f(x,y,y) = y. [para(3(a,1),2(a,1))]. 12 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(6(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. 13 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(3(a,1),6(a,1,3)),rewrite(3(1,R),4(1))]. 14 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(6(a,1),6(a,1,3))]. 16 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)). [para(8(a,1),3(a,1)),rewrite(3(4),3(4)),flip(a)]. 17 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)). [para(3(a,1),8(a,1,1)),rewrite(3(2,R),4(2),3(3,R),4(3),3(6,R),4(6))]. 18 f(f(x,y,z),f(y,z,u),f(v,f(y,z,w),f(x,y,z))) = f(v,f(x,y,z),f(y,z,f(x,u,w))). [para(8(a,1),6(a,1,3)),rewrite(3(4,R),4(4),3(9,R)),flip(a)]. 19 f(f(x,y,f(x,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(x,v,w)). [para(6(a,1),8(a,1,1)),rewrite(4(4),4(6))]. 20 f(f(x,y,z),f(y,u,f(y,z,v)),f(y,z,w)) = f(y,z,f(x,w,f(y,u,v))). [para(6(a,1),8(a,1,2)),rewrite(4(7))]. 21 f(f(x,y,z),f(y,z,u),f(y,v,f(y,z,w))) = f(y,z,f(x,u,f(y,v,w))). [para(6(a,1),8(a,1,3))]. 22 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(6(a,1),8(a,2,3)),rewrite(8(5))]. 24 f(f(x,f(y,z,u),f(z,u,v)),f(z,u,f(y,v,w)),f(v6,f(y,z,u),f(z,u,v))) = f(f(y,z,u),f(z,u,v),f(x,v6,f(z,u,w))). [para(8(a,1),8(a,1,2)),rewrite(3(8),4(13))]. 28 f(x,y,f(x,z,y)) = f(x,z,y). [para(11(a,1),6(a,1,3)),flip(a)]. 29 f(x,y,f(x,y,z)) = f(x,y,z). [para(11(a,1),6(a,1)),rewrite(4(3),28(3)),flip(a)]. 30 f(x,f(y,x,z),f(u,y,x)) = f(y,x,f(u,x,z)). [para(11(a,1),8(a,1,2)),rewrite(3(3,R))]. 31 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)). [para(11(a,1),8(a,1,3)),rewrite(3(3),4(4))]. 36 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,v,u)). [para(28(a,1),8(a,1,2)),rewrite(4(2),8(4),4(3),4(4)),flip(a)]. 38 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(12(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3))]. 39 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(3(a,1),12(a,1)),rewrite(3(2),3(2),4(3))]. 41 f(f(x,y,f(y,z,u)),f(z,v,f(x,y,u)),f(z,w,f(x,y,u))) = f(z,f(x,y,u),f(y,v,w)). [para(12(a,1),8(a,1,1)),rewrite(4(4),4(6))]. 48 f(f(x,y,z),f(y,z,u),f(v,f(x,y,z),f(y,z,w))) = f(v,f(x,y,z),f(y,z,f(x,u,w))). [para(8(a,1),12(a,2,3))]. 83 f(x,f(x,y,z),f(x,u,v)) = f(x,y,f(x,u,f(x,v,z))). [para(14(a,1),13(a,1)),flip(a)]. 96 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(6(a,1),38(a,1,3)),rewrite(3(1,R),4(1),3(6,R),4(6))]. 98 f(f(x,y,f(y,z,u)),f(y,v,f(x,y,u)),f(y,w,f(x,y,u))) = f(y,f(x,y,u),f(z,v,w)). [para(38(a,1),8(a,1,1)),rewrite(3(1,R),4(1),4(4),4(6))]. 125 f(x,f(y,x,z),f(y,x,u)) = f(y,x,f(x,u,z)). [para(30(a,1),3(a,1)),rewrite(3(1,R),4(1),3(3),3(3),3(5,R)),flip(a)]. 135 f(x,f(y,x,z),f(y,u,f(y,x,z))) = f(y,x,z). [para(29(a,1),30(a,1,3)),rewrite(4(3),3(5),2(5),4(4)),flip(a)]. 139 f(f(x,y,z),f(x,u,f(x,y,z)),f(x,y,f(x,z,v))) = f(x,f(x,y,z),f(u,v,f(x,y,z))). [para(12(a,2),30(a,1,3)),rewrite(4(3),3(4),3(4),3(9))]. 149 f(x,f(y,x,z),f(u,f(y,x,z),f(y,x,v))) = f(u,f(y,x,z),f(y,x,f(x,z,v))). [para(30(a,1),38(a,1,3)),rewrite(3(2),3(2),3(7),3(7)),flip(a)]. 153 f(f(x,y,z),f(x,y,f(y,z,u)),f(y,v,f(x,y,z))) = f(v,f(x,y,z),f(x,y,f(y,z,u))). [para(30(a,1),30(a,1,2)),rewrite(3(2),3(2),3(5,R),4(5),3(9),3(9),149(11))]. 154 f(f(x,y,z),f(u,x,y),f(y,v,f(u,x,y))) = f(v,f(u,x,y),f(x,y,f(u,y,z))). [para(30(a,1),30(a,1,3)),rewrite(3(4),4(7),18(7),4(3),28(3),4(8)),flip(a)]. 157 f(f(x,y,z),f(x,u,f(x,y,v)),f(x,y,w)) = f(x,y,f(z,w,f(x,u,v))). [para(6(a,1),16(a,1,2)),rewrite(3(7),4(7))]. 165 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)). [para(28(a,1),16(a,1,1)),rewrite(17(4)),flip(a)]. 169 f(f(x,y,z),f(x,y,u),f(y,v,f(x,y,w))) = f(x,y,f(z,u,f(y,v,w))). [para(12(a,2),16(a,1,3)),rewrite(3(7))]. 178 f(x,f(y,x,z),f(u,v,f(y,x,w))) = f(x,f(y,x,z),f(w,u,v)). [para(30(a,1),16(a,1,1)),rewrite(3(1,R),4(1),4(4),4(6),98(7),3(5),3(5)),flip(a)]. 183 f(x,f(x,y,z),f(u,v,f(x,y,z))) = f(x,y,f(x,z,f(z,u,v))). [back_rewrite(139),rewrite(157(6),4(2),125(3)),flip(a)]. 185 f(x,f(y,z,u),f(y,z,f(z,u,v))) = f(y,z,f(z,u,f(u,v,x))). [back_rewrite(153),rewrite(169(6),4(2),125(3),4(1)),flip(a)]. 187 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_rewrite(135),rewrite(3(1,R),4(1),3(2,R),4(2),183(4),3(1,R),4(1),3(4,R),4(4))]. 189 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(187(a,1),3(a,2)),rewrite(4(3),3(4,R),4(4))]. 190 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(3(a,1),187(a,1)),rewrite(3(1,R),4(1),3(3),3(3),4(4))]. 198 f(x,y,f(x,f(y,z,u),f(y,v,f(y,z,u)))) = f(y,z,f(x,y,u)). [para(12(a,2),187(a,2)),rewrite(4(3))]. 200 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(187(a,1),13(a,1)),flip(a)]. 204 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),187(a,2)),rewrite(4(3),198(5))]. 226 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(189(a,1),187(a,2)),rewrite(4(5),198(7))]. 233 f(x,f(y,z,u),f(x,z,f(z,v,f(y,z,u)))) = f(y,z,f(x,z,u)). [para(38(a,1),190(a,2)),rewrite(4(3))]. 236 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(200(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. 237 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(3(a,1),200(a,1,2))]. 239 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(200(a,1),4(a,1)),flip(a)]. 249 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(12(a,1),200(a,1,2))]. 275 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(200(a,1),190(a,1,3,3)),rewrite(3(2),3(2))]. 295 f(f(x,y,f(x,z,u)),f(x,v,f(x,y,z)),f(x,w,f(x,y,z))) = f(x,f(x,y,z),f(u,v,w)). [para(13(a,2),17(a,1,1)),rewrite(4(4),4(6))]. 320 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(204(a,1),3(a,2)),rewrite(4(2),3(3)),flip(a)]. 321 f(x,y,f(z,x,y)) = f(z,x,y). [para(11(a,1),204(a,1)),rewrite(29(3)),flip(a)]. 335 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(321(a,1),16(a,1,1)),rewrite(8(4)),flip(a)]. 353 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(204(a,1),226(a,2)),rewrite(4(3),3(4,R),4(4),233(5),3(3)),flip(a)]. 370 f(f(x,y,z),f(y,z,u),f(x,y,z)) = f(x,y,z). [para(321(a,1),236(a,1,3)),rewrite(321(6))]. 403 f(x,f(y,x,z),f(z,u,f(x,z,v))) = f(y,x,f(x,z,f(z,u,v))). [para(12(a,1),18(a,2,3)),rewrite(3(2),2(2),3(5,R),4(5),178(5),185(8),4(5))]. 469 f(x,f(y,z,u),f(z,v,f(y,z,u))) = f(y,z,f(z,u,f(u,x,v))). [para(204(a,1),18(a,2,3)),rewrite(3(2),2(2),3(5,R),4(5),178(5),403(4)),flip(a)]. 497 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(237(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. 499 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(237(a,1),6(a,2)),rewrite(3(1,R),4(1),4(2))]. 505 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(237(a,1),8(a,2)),rewrite(2(2),4(2),4(4),83(5),11(3))]. 513 f(x,f(y,z,u),f(x,z,f(x,u,v))) = f(x,v,f(x,z,u)). [para(237(a,1),14(a,2,3)),rewrite(4(2))]. 528 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(237(a,1),187(a,2)),rewrite(3(5),183(6),513(6))]. 591 f(f(x,y,z),f(u,f(x,y,z),f(y,z,v)),f(w,f(x,y,z),f(y,z,v))) = f(f(x,y,z),f(y,z,v),f(x,u,w)). [para(239(a,1),8(a,1,1)),rewrite(3(4),3(7))]. 619 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(320(a,1),3(a,2)),rewrite(4(2),3(3))]. 620 f(x,f(y,z,u),f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(u,x,v))). [para(6(a,1),320(a,1,3)),rewrite(4(2),3(4,R),4(4),3(7),183(8))]. 622 f(x,f(y,z,u),f(y,v,f(y,z,u))) = f(y,z,f(y,u,f(u,v,x))). [para(12(a,2),320(a,1,3)),rewrite(3(2),3(2),3(4,R),4(4),620(4),4(6)),flip(a)]. 639 f(f(x,y,z),f(y,z,u),f(y,v,f(x,y,z))) = f(x,y,f(y,z,f(z,u,v))). [para(320(a,1),18(a,2,3)),rewrite(3(3),2(3),3(4,R),4(4),3(7),3(7),185(9))]. 756 f(x,y,f(y,z,f(z,u,f(x,y,v)))) = f(y,f(x,y,z),f(x,v,u)). [para(204(a,1),19(a,1,2)),rewrite(29(2),639(6),4(2))]. 791 f(x,f(y,z,u),f(y,z,f(z,v,u))) = f(z,f(y,z,u),f(y,v,x)). [back_rewrite(154),rewrite(3(2),3(2),3(3),3(3),469(5),4(2),756(4),3(4),3(4),3(5),3(5)),flip(a)]. 832 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(353(a,1),3(a,2)),rewrite(4(2),3(3))]. 1143 f(f(x,y,z),f(y,z,u),f(v,w,f(x,y,z))) = f(f(x,y,z),f(y,z,u),f(v,x,w)). [para(18(a,1),21(a,1,3)),rewrite(3(6),4(9),2(11),3(8),591(8),3(3,R),4(3),370(10)),flip(a)]. 1188 f(f(x,y,z),f(y,z,u),f(x,y,v)) = f(x,y,f(y,z,f(z,u,v))). [back_rewrite(639),rewrite(1143(5),3(3,R),4(3))]. 1233 f(x,f(y,z,u),f(v,y,f(y,z,u))) = f(y,z,f(y,u,f(v,u,x))). [para(12(a,2),619(a,1,3)),rewrite(3(2),3(2),620(4),3(1,R),4(1)),flip(a)]. 1234 f(x,f(y,z,u),f(y,z,f(v,y,u))) = f(y,z,f(y,u,f(v,u,x))). [para(12(a,2),619(a,2,3)),rewrite(3(3,R),4(3),622(4),3(1)),flip(a)]. 1308 f(f(x,y,z),f(x,u,f(x,y,v)),f(x,w,f(x,y,v6))) = f(x,y,f(z,f(x,w,v6),f(x,u,v))). [para(20(a,1),22(a,1)),rewrite(3(5),3(5)),flip(a)]. 1318 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [back_rewrite(295),rewrite(1308(7),4(2),4(3),16(4),3(1),4(1)),flip(a)]. 1375 f(x,y,f(x,f(y,z,u),f(y,u,v))) = f(y,f(x,y,u),f(x,z,v)). [para(505(a,1),832(a,2,3)),rewrite(3(1),3(3),1318(6),165(5),3(5),4(7),4(8),791(8))]. 1711 f(x,f(y,x,z),f(y,u,v)) = f(x,z,f(y,x,f(y,u,v))). [para(31(a,1),21(a,2,3)),rewrite(3(2),4(2),3(5,R),4(5),1188(6),36(4),756(4),3(4,R),4(4),3(5,R),4(5))]. 1735 f(x,y,f(x,f(y,z,u),f(y,u,v))) = f(y,u,f(x,y,f(x,z,v))). [back_rewrite(1375),rewrite(1711(7))]. 2254 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(249(a,1),3(a,2)),rewrite(3(3),3(3),3(4),3(5),3(5))]. 2670 f(x,f(y,z,u),f(z,u,f(x,y,v))) = f(x,f(y,z,u),f(z,u,v)). [para(335(a,1),165(a,1,3)),rewrite(3(2,R),4(2),3(6),3(6))]. 2835 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(2(a,1),528(a,1,2,3)),rewrite(4(2),4(4))]. 3388 f(x,f(y,z,f(z,x,u)),f(x,v,f(y,z,u))) = f(x,f(y,z,u),f(z,x,v)). [para(2(a,1),41(a,1,3)),rewrite(3(5),4(7))]. 3513 f(x,f(y,z,f(u,v,w)),f(x,f(y,v6,f(u,v,w)),f(y,f(u,v,w),f(z,v,v6)))) = f(x,f(y,z,f(u,v,w)),f(y,v6,f(u,v,w))). [para(41(a,1),505(a,1,3,3)),rewrite(3(6,R),4(6))]. 3604 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [para(528(a,1),41(a,2)),rewrite(3(1),2(2),11(1),3(1),3(4),3(6,R),4(6),29(6),4(6),28(6),3(4))]. 3656 f(x,f(y,z,u),f(y,z,f(z,v,u))) = f(z,u,f(y,z,f(y,v,x))). [para(3604(a,1),619(a,2,3)),rewrite(3(2,R),4(2),3(4,R),4(4),3(5,R),4(5),1318(6),165(5),1735(4),3(5,R),4(5),3(6,R),4(6),4(7)),flip(a)]. 4823 f(x,f(y,z,f(z,u,v)),f(z,x,u)) = f(z,x,u). [para(2254(a,1),41(a,2)),rewrite(2(9),3(7),3388(7),4(5))]. 5050 f(x,f(y,z,u),f(z,u,f(y,v,x))) = f(z,u,f(y,v,x)). [para(497(a,1),48(a,1,3)),rewrite(8(4)),flip(a)]. 6664 f(x,y,f(z,y,f(z,u,f(v,z,x)))) = f(z,x,y). [para(4823(a,1),41(a,2)),rewrite(2(6),3(7,R),1318(7),3656(6),11(2),1318(3))]. 7732 f(x,f(y,z,f(x,u,v)),f(y,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(2835(a,1),6664(a,1,3)),rewrite(3(1),3(3),3(4,R),4(4),3(6),3(8,R),4(8),165(8),3(6),3(6))]. 9590 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(497(a,1),96(a,2,3)),rewrite(3(3),4(3),335(4),3(2,R),4(2),2670(4),3(2),2(2),4(2),3(4),3(5,R)),flip(a)]. 9859 f(x,f(y,z,u),f(z,u,f(z,v,f(x,y,v)))) = f(x,f(y,z,u),f(z,u,v)). [para(9590(a,1),505(a,1,3,3)),rewrite(3(2),3(2),3(3),3(3),1233(5),3(2),3(7),3(7))]. 15767 f(x,f(y,z,u),f(z,v,f(z,w,f(x,y,w)))) = f(x,f(z,v,w),f(y,z,u)). [para(12(a,2),275(a,1,3,3)),rewrite(1234(5),3(2))]. 15825 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,u,x)). [para(275(a,1),24(a,2)),rewrite(2(4),48(7),4(3),29(3),5050(4),3(5,R)),flip(a)]. 16006 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(9859),rewrite(15767(5),15825(3),3(1)),flip(a)]. 18711 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(3(a,2),15825(a,1,2)),rewrite(3(2),4(2),3(4),4(4),3(5,R),4(5))]. 19118 f(x,f(y,z,f(u,v,w)),f(y,v6,f(u,v,w))) = f(y,f(u,v,w),f(x,z,v6)). [back_rewrite(3513),rewrite(18711(8),18711(7),499(4)),flip(a)]. 19770 f(x,f(y,z,u),f(y,v,u)) = f(y,u,f(x,v,z)). [back_rewrite(7732),rewrite(19118(5))]. 20100 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(v,x,y)). [para(16006(a,1),15825(a,2)),rewrite(4(2),3(4,R),4(4),19770(5),3(4))]. 20445 $F # answer(dist_short). [back_rewrite(10),rewrite(20100(10),3(6),3(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=185. Generated=176759. Kept=20440. proofs=1. Usable=113. Sos=8882. Demods=6758. Limbo=345, Disabled=11106. Hints=0. Weight_deleted=622. Literals_deleted=0. Forward_subsumed=155026. Back_subsumed=602. Sos_limit_deleted=670. Sos_displaced=0. Sos_removed=0. New_demodulators=16943 (2 lex), Back_demodulated=10498. Back_unit_deleted=0. Demod_attempts=3586438. Demod_rewrites=1247393. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=25.49. User_CPU=78.24, System_CPU=0.11, Wall_clock=80. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 28060 exit (max_proofs) Fri Apr 13 09:57:59 2007