============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11748 was started by mccune on cleo.thornwood, Sat Aug 12 21:31:40 2006 The command was "/home/mccune/bin/prover9 -f dist-long-short.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-long-short.in 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). [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 (F,wt=6): 11 f(x,y,y) = y. [para(3(a,1),2(a,1))]. given #8 (F,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 (A,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 (F,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 #13 (F,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 #14 (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 #15 (T,wt=18): 15 f(x,f(x,y,z),f(x,y,u)) = f(x,y,f(x,z,u)). [para(2(a,1),8(a,1,1))]. given #16 (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 #17 (F,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 #18 (F,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 #19 (T,wt=18): 33 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(28(a,1),6(a,1,3)),flip(a)]. given #20 (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 #21 (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 #22 (F,wt=15): 213 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(30(a,1),36(a,1,3)),rewrite(2(5))]. given #23 (F,wt=15): 254 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_rewrite(148),rewrite(3(1,R),4(1),3(2,R),4(2),94(4),4(1),3(4,R),4(4))]. given #24 (T,wt=15): 258 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(213(a,1),3(a,2)),rewrite(3(1,R),4(1),4(3),3(4),3(4))]. given #25 (T,wt=15): 271 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(213(a,1),39(a,2)),rewrite(3(2,R),4(2),3(4,R),4(4))]. given #26 (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 #27 (F,wt=15): 288 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),254(a,2)),rewrite(4(3),285(5))]. given #28 (F,wt=12): 394 f(x,y,f(z,x,y)) = f(z,x,y). [para(11(a,1),288(a,1)),rewrite(29(3)),flip(a)]. given #29 (T,wt=15): 294 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(213(a,1),254(a,2)),rewrite(4(5),285(7))]. given #30 (T,wt=15): 305 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(271(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #31 (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 #32 (F,wt=15): 306 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(3(a,1),271(a,1,2))]. given #33 (F,wt=15): 307 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(3(a,2),271(a,1,2)),rewrite(4(2),4(4))]. given #34 (T,wt=15): 308 f(x,f(x,y,z),f(y,z,u)) = f(x,y,z). [para(271(a,1),4(a,1)),flip(a)]. given #35 (T,wt=15): 393 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(288(a,1),3(a,2)),rewrite(4(2),3(3)),flip(a)]. given #36 (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 #37 (F,wt=15): 413 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para(294(a,1),3(a,2)),rewrite(3(1,R),4(1),4(3),3(4))]. given #38 (F,wt=15): 427 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(294(a,1),288(a,1)),flip(a)]. given #39 (T,wt=15): 429 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(288(a,1),294(a,2)),rewrite(4(3),3(4,R),4(4),298(5),3(3)),flip(a)]. given #40 (T,wt=15): 430 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para(294(a,1),294(a,2)),rewrite(3(1,R),4(1),3(3,R),4(3),4(5),3(6,R),4(6),298(7),3(4))]. given #41 (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 #42 (F,wt=15): 431 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(305(a,1),4(a,1)),flip(a)]. given #43 (F,wt=15): 586 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(306(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #44 (T,wt=15): 588 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(306(a,1),6(a,2)),rewrite(3(1,R),4(1),4(2))]. given #45 (T,wt=15): 594 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(306(a,1),8(a,2)),rewrite(2(2),4(2),4(4),115(5),11(3))]. given #46 (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 #47 (F,wt=15): 620 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(213(a,1),306(a,1,3)),rewrite(4(5),387(5),3(2),3(2),213(6))]. given #48 (F,wt=15): 639 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(307(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. given #49 (T,wt=15): 713 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(393(a,1),3(a,2)),rewrite(4(2),3(3))]. given #50 (T,wt=15): 858 f(x,f(y,x,z),f(y,z,u)) = f(y,x,z). [para(394(a,1),19(a,1,2)),rewrite(29(2),2(5)),flip(a)]. given #51 (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 #52 (F,wt=15): 929 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(429(a,1),3(a,2)),rewrite(4(2),3(3))]. given #53 (F,wt=15): 937 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(16(a,1),429(a,1)),rewrite(4(2),36(3),11(1),115(5),29(5),141(5),4(3)),flip(a)]. given #54 (T,wt=15): 940 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(429(a,1),294(a,2)),rewrite(4(3),3(4,R),4(4),729(5),3(3))]. given #55 (T,wt=15): 1182 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(3(a,1),594(a,1)),rewrite(3(1),3(3),3(3),4(4))]. given #56 (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 #57 (F,wt=15): 1318 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(3(a,1),620(a,1)),rewrite(3(2),3(2),3(3,R),3(4),3(4))]. given #58 (F,wt=15): 1369 f(x,f(y,x,z),f(u,y,z)) = f(y,x,z). [para(427(a,1),713(a,1,3)),rewrite(11(3),237(6),3(4,R),4(4),919(5),3(3,R),4(3)),flip(a)]. given #59 (T,wt=18): 141 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)]. given #60 (T,wt=18): 226 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 #61 (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 #62 (F,wt=18): 260 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(6(a,1),213(a,1,3,3))]. given #63 (F,wt=18): 268 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(12(a,2),213(a,1,3,3))]. given #64 (T,wt=18): 317 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(12(a,1),271(a,1,2))]. given #65 (T,wt=18): 323 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(39(a,1),271(a,1,2))]. given #66 (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 #67 (F,wt=18): 359 f(x,f(y,x,z),f(y,u,x)) = f(y,x,f(u,x,z)). [para(11(a,1),17(a,1,2)),rewrite(3(3,R))]. given #68 (F,wt=18): 360 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 #69 (T,wt=18): 410 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(394(a,1),16(a,1,1)),rewrite(8(4)),flip(a)]. given #70 (T,wt=18): 435 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(28(a,1),305(a,1,3)),rewrite(28(6))]. given #71 (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 #72 (F,wt=18): 622 f(x,f(y,z,f(u,v,y)),f(x,v,y)) = f(x,v,y). [para(306(a,1),254(a,2)),rewrite(3(5),249(6),607(6))]. given #73 (F,wt=15): 2860 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(2(a,1),622(a,1,2,3)),rewrite(4(2),4(4))]. given #74 (T,wt=15): 2923 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(305(a,1),622(a,1,3)),rewrite(3(1),3(3),3(5,R),4(5),3(6),4(7),1443(7),2425(7),3(3)),flip(a)]. given #75 (T,wt=18): 626 f(x,y,f(x,z,f(z,u,f(v,y,z)))) = f(x,y,z). [para(306(a,1),271(a,1,3)),rewrite(3(3),4(5),249(5),306(7))]. given #76 (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 #77 (F,wt=18): 634 f(x,y,f(x,z,f(u,z,f(v,y,z)))) = f(x,y,z). [para(306(a,1),306(a,1,3)),rewrite(4(5),249(5),3(2,R),4(2),306(7))]. given #78 (F,wt=18): 665 f(x,f(y,z,f(u,v,y)),f(x,u,y)) = f(x,u,y). [para(307(a,1),254(a,2)),rewrite(3(5),249(6),650(6))]. given #79 (T,wt=18): 669 f(x,y,f(x,z,f(z,u,f(y,v,z)))) = f(x,y,z). [para(307(a,1),271(a,1,3)),rewrite(3(3),4(5),249(5),307(7))]. given #80 (T,wt=18): 678 f(x,y,f(x,z,f(u,z,f(y,v,z)))) = f(x,y,z). [para(307(a,1),306(a,1,3)),rewrite(4(5),249(5),3(2,R),4(2),307(7))]. given #81 (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 #82 (F,wt=15): 3636 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [para(622(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 #83 (F,wt=18): 758 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [back_rewrite(320),rewrite(739(4))]. given #84 (T,wt=18): 959 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x). [back_rewrite(925),rewrite(948(5))]. given #85 (T,wt=18): 1340 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(639(a,1),427(a,1,3)),rewrite(4(3),4(5),948(5),639(7))]. given #86 (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 #87 (F,wt=18): 1506 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(427(a,1),929(a,1,3)),rewrite(11(3),1353(6)),flip(a)]. given #88 (F,wt=18): 1830 f(x,y,f(x,z,f(y,u,f(v,y,z)))) = f(x,y,z). [para(1318(a,1),1182(a,2)),rewrite(3(2),3(3),3(5,R),1443(6),226(5),607(6),739(4),3(5))]. given #89 (T,wt=18): 2166 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(260(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5),3(5))]. given #90 (T,wt=18): 2183 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(260(a,1),213(a,2)),rewrite(4(7),1443(8),226(7),3(3,R),4(3),1500(6))]. given #91 (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 #92 (F,wt=18): 2226 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y). [para(260(a,1),260(a,2)),rewrite(4(7),1443(9),2173(10))]. given #93 (F,wt=18): 2227 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(268(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5),3(5))]. given #94 (T,wt=18): 2236 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(39(a,2),268(a,1,3))]. given #95 (T,wt=18): 2242 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(268(a,1),213(a,2)),rewrite(4(7),1443(8),226(7),3(3,R),4(3),1500(6))]. given #96 (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 #97 (F,wt=18): 2285 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(268(a,1),260(a,2)),rewrite(4(7),1443(9),2173(10))]. given #98 (F,wt=18): 2286 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(317(a,1),3(a,2)),rewrite(3(3),3(3),3(4),3(5),3(5))]. given #99 (T,wt=15): 4826 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(2286(a,1),713(a,1,3)),rewrite(11(3),3(4,R),4(4),446(7),3(5,R),4(5),3784(6),3(2),3(3,R),4(3)),flip(a)]. given #100 (T,wt=18): 2382 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(323(a,1),3(a,2)),rewrite(3(3),3(3),3(4),3(5),3(5))]. given #101 (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 #102 (F,wt=18): 2386 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(323(a,1),8(a,2)),rewrite(2(3),4(3),4(6),1443(7),28(6))]. given #103 (F,wt=18): 2477 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),1443(3),29(2),3(3,R),4(3),29(5),360(5),4(6),36(7),11(5),3(6),218(6),29(6))]. given #104 (T,wt=18): 2861 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(622(a,1),3(a,1)),rewrite(3(3),3(3),3(5,R)),flip(a)]. given #105 (T,wt=18): 2862 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(622(a,1),3(a,2)),rewrite(3(1),3(3),4(3),3(4),3(5),4(5))]. given #106 (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 #107 (F,wt=18): 2863 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(3(a,1),622(a,1,2,3)),rewrite(4(3),4(5))]. given #108 (F,wt=18): 2864 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(3(a,2),622(a,1,2,3)),rewrite(3(1,R),4(1),4(3),4(5))]. given #109 (T,wt=18): 2865 f(x,f(y,z,f(u,v,z)),f(x,v,z)) = f(x,v,z). [para(3(a,2),622(a,1,2)),rewrite(4(2))]. given #110 (T,wt=18): 2874 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(622(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1443(7),28(6),4(5))]. given #111 (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 #112 (F,wt=18): 3017 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(39(a,2),626(a,1,3)),rewrite(3(1),3(1))]. given #113 (F,wt=18): 3325 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(665(a,1),3(a,2)),rewrite(3(1),3(3),4(3),3(4),3(5),4(5))]. given #114 (T,wt=18): 3326 f(x,f(y,z,f(u,v,z)),f(x,u,z)) = f(x,u,z). [para(3(a,2),665(a,1,2)),rewrite(4(2))]. given #115 (T,wt=18): 3685 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(3636(a,1),431(a,1,2)),rewrite(3(5,R),1306(5),3636(7))]. given #116 (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 #117 (F,wt=18): 3876 f(x,y,f(z,f(x,z,y),f(u,z,y))) = f(x,z,y). [para(1340(a,1),38(a,1,3)),rewrite(11(3),4(4),3784(7),3(3)),flip(a)]. given #118 (F,wt=18): 3979 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(429(a,1),43(a,1)),rewrite(3(1),3(2),3(3,R),4(3),1497(5),4(3),1443(5),2986(5),3(2),3344(4),3(5,R),4(5)),flip(a)]. given #119 (T,wt=18): 4118 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [para(1506(a,1),16(a,2)),rewrite(11(4),3(5),3(5),3344(5),29(4))]. given #120 (T,wt=18): 4387 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(2226(a,1),3(a,2)),rewrite(3(1,R),4(1),4(4),3(5))]. given #121 (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 #122 (F,wt=18): 4482 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(2236(a,1),4(a,2)),rewrite(3(2,R),4(2),3522(3),4(4),4(5))]. given #123 (F,wt=18): 4605 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(3(a,2),2242(a,1,2)),rewrite(4(2),3(3,R),4(3),3(5,R),4(5))]. given #124 (T,wt=18): 4819 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(2286(a,1),429(a,1)),rewrite(3(3,R),4(3)),flip(a)]. given #125 (T,wt=18): 4848 f(x,f(y,z,f(z,u,v)),f(z,x,u)) = f(z,x,u). [para(2286(a,1),41(a,2)),rewrite(2(9),3(7),3424(7),4(5))]. given #126 (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 #127 (F,wt=18): 4879 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(2382(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),3522(7),29(7),4(5))]. given #128 (F,wt=18): 4895 f(x,f(y,z,f(z,u,v)),f(z,x,v)) = f(z,x,v). [para(2382(a,1),41(a,2)),rewrite(2(9),3(7),3424(7),4(5))]. given #129 (T,wt=18): 5165 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(3(a,1),2386(a,1)),rewrite(3(1),3(4),3(4),4(5))]. given #130 (T,wt=18): 5185 f(x,y,f(z,f(y,u,z),f(x,u,z))) = f(x,y,z). [para(3(a,1),2477(a,1,3)),rewrite(3(2,R),4(2),3(3,R))]. given #131 (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 #132 (F,wt=18): 5246 f(x,y,f(z,f(x,u,z),f(y,u,z))) = f(x,y,z). [para(2477(a,1),226(a,2)),rewrite(3(1,R),4(1),4(3),36(5),3(3,R))]. given #133 (F,wt=18): 5586 f(x,y,f(x,z,f(u,z,f(z,v,y)))) = f(x,z,y). [para(2865(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1443(7),28(6),4(5))]. given #134 (T,wt=18): 5916 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(3326(a,1),8(a,2)),rewrite(3(1),2(3),3(1),4(3),3(4),4(6),1443(7),28(6),4(5))]. given #135 (T,wt=18): 6189 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y). [para(3979(a,1),8(a,2)),rewrite(11(2),3(2,R),4(2),3(5,R),4(5),31(5),3(5,R),4(5))]. given #136 (A,wt=21): 62 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 #137 (F,wt=18): 6494 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(3(a,1),4482(a,1)),rewrite(3(1,R),4(1),3(4),3(4),3(5,R),4(5))]. given #138 (F,wt=18): 6503 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(13(a,1),4482(a,1,3)),rewrite(4(1),4(5))]. given #139 (T,wt=18): 6775 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(4879(a,1),8(a,2)),rewrite(3(6),2(6),4(6),3(7,R),1443(7),394(6))]. given #140 (T,wt=18): 6777 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(12(a,1),4879(a,1)),rewrite(4(3))]. given #141 (A,wt=21): 63 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 #142 (F,wt=18): 6792 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [para(28(a,1),4895(a,1,3)),rewrite(3(1),3(4),4(5),1443(5),5364(5),4(1),3(5),3(6,R),4(6),29(6))]. given #143 (F,wt=18): 6796 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(4895(a,1),41(a,2)),rewrite(2(6),3(7,R),1443(7),891(6),3(3),2(3),4(2))]. given #144 (T,wt=18): 7238 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [back_rewrite(4577),rewrite(7123(10))]. given #145 (T,wt=18): 7393 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(586(a,1),62(a,2,3)),rewrite(3(3),4(3),410(4),3(2,R),4(2),2694(4),3(2),2(2),4(2),3(4),3(5,R)),flip(a)]. given #146 (A,wt=33): 64 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))]. given #147 (F,wt=18): 8125 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(3(a,1),7238(a,1)),rewrite(3(2,R),4(2),3(4),3(4),3(5,R),4(5))]. given #148 (F,wt=21): 68 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 #149 (T,wt=18): 8496 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(586(a,1),68(a,2,3)),rewrite(3(3),4(3),410(4),3(2,R),4(2),2694(4),11(2),4(2),3(4),3(5,R)),flip(a)]. given #150 (T,wt=18): 8504 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(639(a,1),68(a,2,3)),rewrite(3(3),4(3),226(4),3(2,R),4(2),1887(4),11(2),4(2),3(4),3(5,R)),flip(a)]. given #151 (A,wt=21): 69 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(12(a,2),38(a,1,3)),rewrite(3(1,R),4(1),3(6,R),4(6)),flip(a)]. given #152 (F,wt=21): 70 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(12(a,2),38(a,2,3)),rewrite(3(2,R),4(2),3(6,R),4(6))]. given #153 (F,wt=21): 71 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 #154 (T,wt=21): 72 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 #155 (T,wt=21): 73 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)]. given #156 (A,wt=33): 74 f(f(x,y,f(y,z,u)),f(u,v,f(x,y,z)),f(u,w,f(x,y,z))) = f(u,f(x,y,z),f(y,v,w)). [para(39(a,1),8(a,1,1)),rewrite(4(4),4(6))]. given #157 (F,wt=21): 75 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 #158 (F,wt=21): 80 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 #159 (T,wt=21): 81 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 #160 (T,wt=21): 99 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 #161 (A,wt=27): 98 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 #162 (F,wt=21): 119 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 #163 (F,wt=21): 138 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,y,u))). [back_rewrite(95),rewrite(115(4),33(3))]. given #164 (T,wt=21): 139 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))). [back_rewrite(85),rewrite(115(3),4(1))]. given #165 (T,wt=21): 140 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))). [back_rewrite(84),rewrite(115(3),4(1))]. given #166 (A,wt=27): 100 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 #167 (F,wt=21): 199 f(x,y,f(z,u,f(u,v,f(z,x,y)))) = f(x,y,f(z,u,v)). [para(36(a,1),8(a,1)),rewrite(4(3),8(4),3(5),198(7),3(4,R),4(4)),flip(a)]. given #168 (F,wt=21): 205 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(13(a,1),36(a,2,3)),rewrite(36(4),4(4))]. given #169 (T,wt=21): 206 f(x,y,f(z,u,f(v,u,w))) = f(x,y,f(v,u,f(z,u,w))). [para(38(a,1),36(a,2,3)),rewrite(36(4))]. given #170 (T,wt=21): 263 f(x,y,f(z,u,f(y,v,f(x,v,w)))) = f(x,y,f(z,v,u)). [para(213(a,1),8(a,1,2)),rewrite(8(4),4(5)),flip(a)]. given #171 (A,wt=45): 101 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 #172 (F,wt=21): 269 f(x,f(y,z,f(x,z,u)),f(x,v,y)) = f(x,v,f(x,y,z)). [para(213(a,1),13(a,1,3)),flip(a)]. given #173 (F,wt=21): 273 f(x,y,f(y,z,f(x,u,f(x,v,f(x,z,w))))) = f(x,y,z). [para(14(a,2),213(a,1,3,3))]. given #174 (T,wt=21): 282 f(x,y,f(z,u,f(x,v,f(y,v,w)))) = f(x,y,f(z,v,u)). [para(254(a,1),8(a,1,2)),rewrite(8(4),4(5)),flip(a)]. given #175 (T,wt=21): 304 f(x,y,f(z,u,f(x,v,f(v,y,w)))) = f(x,y,f(v,z,u)). [para(258(a,1),16(a,1,1)),rewrite(17(4)),flip(a)]. given #176 (A,wt=45): 103 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 #177 (F,wt=21): 309 f(x,f(y,z,u),f(x,v,f(x,y,z))) = f(x,v,f(x,y,z)). [para(271(a,1),6(a,1,3)),flip(a)]. given #178 (F,wt=21): 342 f(x,y,f(y,f(z,u,v),f(x,z,u))) = f(x,y,f(z,u,v)). [para(271(a,1),213(a,1,3,3))]. given #179 (T,wt=18): 11507 f(x,y,f(z,f(y,z,u),f(x,v,z))) = f(x,y,z). [para(6792(a,1),342(a,2)),rewrite(3(1),4(5),947(5),36(5),4(5))]. given #180 (T,wt=21): 344 f(x,y,f(x,f(z,u,v),f(y,z,u))) = f(x,y,f(z,u,v)). [para(271(a,1),254(a,1,3,3))]. given #181 (A,wt=33): 104 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))]. given #182 (F,wt=18): 11591 f(x,y,f(z,f(x,y,z),f(u,v,w))) = f(x,y,z). [para(344(a,1),6503(a,1,3))]. given #183 (F,wt=18): 11639 f(x,y,f(z,f(x,z,y),f(u,v,w))) = f(x,z,y). [para(11591(a,1),3(a,2)),rewrite(3(1),3(1),4(4),3(5),3(5))]. given #184 (T,wt=21): 346 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(271(a,1),258(a,1,3,3)),rewrite(3(2),3(2))]. given #185 (T,wt=18): 11769 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,u,x)). [para(346(a,1),24(a,2)),rewrite(2(4),48(7),4(3),29(3),4983(4),3(5,R)),flip(a)]. given #186 (A,wt=27): 106 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))]. given #187 (F,wt=18): 11840 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(8192),rewrite(11728(5),11769(3),3(1)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 48.08 (+ 0.06) seconds: dist_short. % Length of proof is 91. % Level of proof is 15. % Maximum clause weight is 54. % Given clauses 187. 1 f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # answer(dist_short). [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))]. 15 f(x,f(x,y,z),f(x,y,u)) = f(x,y,f(x,z,u)). [para(2(a,1),8(a,1,1))]. 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)]. 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))]. 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))]. 35 f(f(x,y,z),f(z,u,f(x,y,z)),f(z,v,f(x,y,z))) = f(z,f(x,y,z),f(x,u,v)). [para(28(a,1),8(a,1,1)),rewrite(4(3),4(5))]. 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))]. 45 f(x,f(x,y,z),f(u,x,y)) = f(u,x,f(x,y,z)). [para(12(a,1),8(a,2)),rewrite(3(2),2(2),3(3,R))]. 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))]. 62 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))]. 94 f(x,f(x,y,z),f(y,u,f(x,y,v))) = f(x,y,f(x,z,f(y,u,v))). [para(12(a,2),15(a,1,3))]. 115 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)]. 141 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)]. 148 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)]. 149 f(x,f(y,x,z),f(u,f(y,x,v),f(y,x,z))) = f(u,f(y,x,z),f(y,x,f(x,z,v))). [para(30(a,1),12(a,1,3)),rewrite(3(2),3(2),3(4,R),4(4),3(7),3(7),3(8,R)),flip(a)]. 151 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))]. 198 f(x,y,f(z,u,f(v,w,f(x,y,v6)))) = f(x,y,f(z,u,f(v,v6,w))). [para(36(a,1),8(a,1,2)),rewrite(8(5),4(2),4(6)),flip(a)]. 213 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(30(a,1),36(a,1,3)),rewrite(2(5))]. 218 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))]. 226 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)]. 249 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(151),rewrite(218(6),4(2),141(3)),flip(a)]. 253 f(x,f(y,z,u),f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(u,x,v))). [back_rewrite(149),rewrite(3(1,R),4(1),3(2,R),4(2),3(3,R),4(3),249(5),198(4),4(1),3(4,R),4(4),3(6,R),4(6)),flip(a)]. 254 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_rewrite(148),rewrite(3(1,R),4(1),3(2,R),4(2),94(4),4(1),3(4,R),4(4))]. 258 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(213(a,1),3(a,2)),rewrite(3(1,R),4(1),4(3),3(4),3(4))]. 271 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [para(213(a,1),39(a,2)),rewrite(3(2,R),4(2),3(4,R),4(4))]. 285 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),254(a,2)),rewrite(4(3))]. 288 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),254(a,2)),rewrite(4(3),285(5))]. 294 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(213(a,1),254(a,2)),rewrite(4(5),285(7))]. 298 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),258(a,2)),rewrite(4(3))]. 305 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(271(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. 306 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(3(a,1),271(a,1,2))]. 320 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(13(a,2),271(a,1,2))]. 346 f(x,f(y,z,u),f(x,v,f(y,z,v))) = f(x,v,f(y,z,u)). [para(271(a,1),258(a,1,3,3)),rewrite(3(2),3(2))]. 367 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))]. 393 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(288(a,1),3(a,2)),rewrite(4(2),3(3)),flip(a)]. 394 f(x,y,f(z,x,y)) = f(z,x,y). [para(11(a,1),288(a,1)),rewrite(29(3)),flip(a)]. 410 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(394(a,1),16(a,1,1)),rewrite(8(4)),flip(a)]. 427 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(294(a,1),288(a,1)),flip(a)]. 429 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(288(a,1),294(a,2)),rewrite(4(3),3(4,R),4(4),298(5),3(3)),flip(a)]. 446 f(x,f(y,z,x),f(u,v,f(y,z,w))) = f(x,f(y,z,x),f(y,u,v)). [para(305(a,1),17(a,1,1)),rewrite(4(3),4(5),35(6),3(6),3(6)),flip(a)]. 462 f(f(x,y,z),f(y,z,u),f(x,y,f(y,z,v))) = f(y,z,f(y,f(x,y,z),f(x,u,v))). [para(6(a,1),18(a,2)),rewrite(45(5))]. 490 f(x,y,f(x,f(z,x,y),f(z,u,v))) = f(x,f(z,u,v),f(z,x,y)). [para(13(a,1),18(a,2)),rewrite(45(5),462(5),4(7),394(7))]. 497 f(x,f(y,x,z),f(x,z,f(y,u,v))) = f(x,f(y,u,v),f(y,x,z)). [para(39(a,1),18(a,1,3)),rewrite(29(4),462(5),490(4)),flip(a)]. 586 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(306(a,1),3(a,2)),rewrite(3(2),3(2),3(3),3(4),3(4))]. 594 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(306(a,1),8(a,2)),rewrite(2(2),4(2),4(4),115(5),11(3))]. 713 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(393(a,1),3(a,2)),rewrite(4(2),3(3))]. 715 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),393(a,1,3)),rewrite(3(2),3(2),3(4,R),4(4),253(4),4(6)),flip(a)]. 738 f(x,f(y,z,u),f(y,u,f(z,u,v))) = f(u,f(y,z,u),f(y,x,v)). [para(393(a,1),393(a,1,3)),rewrite(3(4,R),4(4),3(7),446(8))]. 739 f(x,f(y,z,u),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))). [back_rewrite(497),rewrite(3(1,R),4(1),115(4),4(2),29(3),3(5,R),4(5)),flip(a)]. 758 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [back_rewrite(320),rewrite(739(4))]. 925 f(f(x,y,z),f(y,z,u),f(u,v,f(y,z,u))) = f(y,z,u). [para(306(a,1),427(a,1,3)),rewrite(3(2),3(2),4(3),3(4),3(4),4(5),3(7),3(7),586(8))]. 948 f(x,f(y,z,u),f(u,v,f(y,z,u))) = f(u,f(y,z,u),f(y,v,x)). [para(393(a,1),429(a,1,3)),rewrite(3(4,R),4(4),738(4),4(6)),flip(a)]. 959 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x). [back_rewrite(925),rewrite(948(5))]. 1351 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),713(a,1,3)),rewrite(3(2),3(2),253(4),3(1,R),4(1)),flip(a)]. 1352 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),713(a,2,3)),rewrite(3(3,R),4(3),715(4),3(1)),flip(a)]. 1432 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)]. 1443 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [back_rewrite(367),rewrite(1432(7),4(2),4(3),16(4),3(1),4(1)),flip(a)]. 2694 f(x,f(y,z,u),f(z,u,f(x,y,v))) = f(x,f(y,z,u),f(z,u,v)). [para(410(a,1),226(a,1,3)),rewrite(3(2,R),4(2),3(6),3(6))]. 3865 f(x,f(y,z,f(u,v,w)),f(x,f(y,v6,f(u,v,w)),f(v7,f(y,z,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),959(a,1,3,3)),rewrite(3(5),3(9,R),4(9),3(11,R),4(11),1443(12),3(17))]. 4983 f(x,f(y,z,u),f(z,u,f(y,v,x))) = f(z,u,f(y,v,x)). [para(586(a,1),48(a,1,3)),rewrite(8(4)),flip(a)]. 7393 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(586(a,1),62(a,2,3)),rewrite(3(3),4(3),410(4),3(2,R),4(2),2694(4),3(2),2(2),4(2),3(4),3(5,R)),flip(a)]. 8192 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(7393(a,1),594(a,1,3,3)),rewrite(3(2),3(2),3(3),3(3),1351(5),3(2),3(7),3(7))]. 11728 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),346(a,1,3,3)),rewrite(1352(5),3(2))]. 11769 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,u,x)). [para(346(a,1),24(a,2)),rewrite(2(4),48(7),4(3),29(3),4983(4),3(5,R)),flip(a)]. 11840 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_rewrite(8192),rewrite(11728(5),11769(3),3(1)),flip(a)]. 12331 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(3(a,2),11769(a,1,2)),rewrite(3(2),4(2),3(4),4(4),3(5,R),4(5))]. 12557 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(3865),rewrite(12331(10),3(7,R),4(7),12331(9),12331(8),758(5)),flip(a)]. 13185 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(v,x,y)). [para(11840(a,1),11769(a,2)),rewrite(4(2),3(4,R),4(4),12557(5),4(2),3(4))]. 13263 $F # answer(dist_short). [back_rewrite(10),rewrite(13185(10),3(6),3(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=187. Generated=171420. Kept=13258. proofs=1. Usable=113. Sos=6124. Demods=4146. Limbo=78, Disabled=6949. Hints=0. Weight_deleted=706. Literals_deleted=0. Forward_subsumed=147117. Back_subsumed=402. Sos_limit_deleted=10338. Sos_displaced=0. Sos_removed=0. New_demodulators=10512 (2 lex), Back_demodulated=6541. Back_unit_deleted=0. Demod_attempts=3439845. Demod_rewrites=1213805. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=14.97. User_CPU=48.08, System_CPU=0.06, Wall_clock=49. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11748 exit (max_proofs) Sat Aug 12 21:32:29 2006