============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13955 was started by mccune on cleo.thornwood, Mon Jun 19 17:18:29 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). clauses(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,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long). end_of_list. clauses(goals). f(f(x,y,z),u,E) = f(x,f(y,u,E),f(z,u,E)) # answer(dist_short). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(f(c1,c2,c3),c4,E) != f(c1,f(c2,c4,E),f(c3,c4,E)) # answer(dist_short). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(x,x,y) = x # label(majority). [input]. 2 f(x,y,z) = f(z,x,y) # label(2a). [input]. 3 f(x,y,z) = f(x,z,y) # label(2b). [input]. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 5 f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long). [input]. 6 f(f(c1,c2,c3),c4,E) != f(c1,f(c2,c4,E),f(c3,c4,E)) # answer(dist_short). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Function symbol KB weights: E=1. c1=1. c2=1. c3=1. c4=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ E, c1, c2, c3, c4, 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: clauses(usable). end_of_list. clauses(sos). 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. 11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long). [copy(5),demod(8(2),8(2)),flip(a)]. 12 f(c1,f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_short). [copy(6),demod(8(7),9(7),8(12),8(16)),flip(a)]. end_of_list. clauses(demodulators). 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. % (lex-dep) 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. % (lex-dep) 11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long). [copy(5),demod(8(2),8(2)),flip(a)]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 7 f(x,x,y) = x # label(majority). [input]. given #2 (I,wt=9): 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. given #3 (I,wt=9): 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. given #4 (I,wt=15): 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. given #5 (I,wt=21): 11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long). [copy(5),demod(8(2),8(2)),flip(a)]. given #6 (I,wt=18): 12 f(c1,f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_short). [copy(6),demod(8(7),9(7),8(12),8(16)),flip(a)]. given #7 (F,wt=6): 13 f(x,y,y) = y. [para(8(a,1),7(a,1))]. given #8 (F,wt=12): 20 f(x,y,f(x,z,y)) = f(x,z,y). [para(10(a,2),10(a,1)),demod(8(1,R),13(1),8(2),9(2)),flip(a)]. given #9 (T,wt=12): 48 f(x,y,f(x,y,z)) = f(x,y,z). [para(13(a,1),10(a,2,3)),demod(8(1),8(1),8(3),8(3))]. given #10 (T,wt=15): 14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [para(10(a,2),8(a,1)),demod(8(1,R),9(1),9(3),8(4),9(4))]. given #11 (A,wt=15): 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(10(a,1),8(a,2)),demod(9(2),8(3))]. given #12 (F,wt=15): 16 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(10(a,2),8(a,2)),demod(9(2),8(3),8(3))]. given #13 (F,wt=15): 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(8(a,1),10(a,1,3)),demod(8(1),9(3),8(4,R),9(4))]. given #14 (T,wt=15): 39 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(10(a,1),11(a,2)),demod(7(2),8(2),8(2),8(3,R),24(3),9(3))]. given #15 (T,wt=18): 23 f(x,f(x,y,z),f(x,z,u)) = f(x,z,f(x,y,u)). [para(7(a,1),11(a,1,1)),demod(8(1,R),9(1),8(2),8(2))]. given #16 (A,wt=21): 18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(10(a,1),10(a,1,3)),demod(8(1),9(5),8(6,R),9(6))]. given #17 (F,wt=18): 24 f(x,f(x,y,z),f(u,x,y)) = f(x,y,f(u,x,z)). [para(7(a,1),11(a,1,2)),demod(8(2),8(2),8(3,R))]. given #18 (F,wt=18): 25 f(x,f(y,x,z),f(x,z,u)) = f(x,z,f(y,x,u)). [para(7(a,1),11(a,1,3)),demod(8(2),8(2),8(3),9(4))]. given #19 (T,wt=18): 50 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(20(a,1),10(a,1,3)),demod(8(1),8(3),9(4),8(5,R),9(5)),flip(a)]. given #20 (T,wt=18): 56 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(10(a,2),48(a,1,3)),demod(9(4))]. given #21 (A,wt=21): 19 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(10(a,2),10(a,1,3)),demod(8(1,R),9(1),9(4),9(5),8(6,R),9(6))]. given #22 (F,wt=18): 67 f(x,y,f(x,z,f(x,u,y))) = f(x,z,f(x,u,y)). [para(20(a,1),14(a,1,3)),flip(a)]. given #23 (F,wt=18): 77 f(x,f(y,x,z),f(u,y,x)) = f(u,x,f(y,x,z)). [para(15(a,1),11(a,2)),demod(8(2,R),13(2),8(2),8(2),8(3,R))]. given #24 (T,wt=15): 350 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [back_demod(234),demod(319(7),13(4)),flip(a)]. given #25 (T,wt=15): 353 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para(350(a,1),8(a,1)),demod(8(3,R),9(3),8(4),8(4)),flip(a)]. given #26 (A,wt=21): 26 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)). [para(11(a,1),8(a,1)),demod(8(3),8(3),8(4),8(4),8(5),8(5)),flip(a)]. given #27 (F,wt=12): 401 f(x,y,f(z,x,y)) = f(z,x,y). [para(353(a,1),15(a,1)),demod(48(3),8(3,R),9(3)),flip(a)]. given #28 (F,wt=15): 391 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [back_demod(349),demod(353(3)),flip(a)]. given #29 (T,wt=15): 392 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_demod(219),demod(9(1),142(4),9(1),9(4),353(6))]. given #30 (T,wt=15): 394 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_demod(209),demod(8(1,R),9(1),8(2,R),9(2),392(3),8(3,R),9(3),8(4,R),9(4)),flip(a)]. given #31 (A,wt=21): 27 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(11(a,1),8(a,2)),demod(8(2),8(2),8(3),8(3),8(5),8(5))]. given #32 (F,wt=15): 395 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [back_demod(157),demod(8(1,R),9(1),8(2,R),9(2),8(5,R),9(5),8(6,R),9(6),394(6))]. given #33 (F,wt=15): 434 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),26(a,2)),demod(13(2),8(3,R),310(3))]. given #34 (T,wt=15): 547 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(8(a,1),394(a,1)),demod(8(1,R),9(1),8(3),9(3),8(4),8(4))]. given #35 (T,wt=15): 555 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para(394(a,1),15(a,1)),flip(a)]. given #36 (A,wt=21): 28 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)). [para(8(a,1),11(a,1,1)),demod(8(2),9(2),8(3),9(3),8(6,R),9(6))]. given #37 (F,wt=15): 568 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(394(a,1),26(a,2)),demod(13(4),8(4),9(4),310(4),9(4))]. given #38 (F,wt=15): 598 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(434(a,1),8(a,2)),demod(9(2),8(3)),flip(a)]. given #39 (T,wt=15): 624 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(434(a,1),547(a,2)),demod(9(3),8(4,R),9(4),523(5),8(3)),flip(a)]. given #40 (T,wt=15): 690 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(568(a,1),8(a,2)),demod(9(2),8(3),9(4))]. given #41 (A,wt=33): 29 f(f(x,y,z),f(u,x,y),f(v,f(u,x,y),f(x,y,w))) = f(v,f(u,x,y),f(x,y,f(u,z,w))). [para(11(a,1),10(a,1,3)),demod(8(2,R),9(2),8(4,R),9(4),8(5),8(5),8(8),8(8),8(9)),flip(a)]. given #42 (F,wt=15): 691 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(8(a,1),568(a,1,2)),demod(8(2,R),9(2),8(4,R),9(4))]. given #43 (F,wt=15): 692 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(8(a,2),568(a,1,2)),demod(8(2),8(2),205(3),8(4),8(4))]. given #44 (T,wt=15): 748 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(598(a,1),8(a,2)),demod(9(2),8(3))]. given #45 (T,wt=15): 767 f(x,f(x,y,z),f(y,u,z)) = f(x,y,z). [para(26(a,1),598(a,1)),demod(9(2),429(3),13(1),310(5),446(5),8(3),8(3)),flip(a)]. given #46 (A,wt=33): 30 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(11(a,1),10(a,2,3)),demod(8(2),8(2),8(4),8(4),9(8))]. given #47 (F,wt=15): 788 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(624(a,1),8(a,2)),demod(9(2),8(3))]. given #48 (F,wt=15): 802 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [para(26(a,1),624(a,1)),demod(9(2),429(3),13(1),172(5),48(4),758(5),429(4)),flip(a)]. given #49 (T,wt=15): 805 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(624(a,1),547(a,2)),demod(9(3),8(4,R),9(4),773(5),8(3))]. given #50 (T,wt=15): 815 f(x,f(y,z,x),f(y,z,u)) = f(y,z,x). [para(690(a,1),9(a,1)),flip(a)]. given #51 (A,wt=33): 32 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(10(a,1),11(a,1,1)),demod(8(4,R),9(4),8(6,R),9(6))]. given #52 (F,wt=15): 1019 f(x,f(y,z,u),f(z,u,x)) = f(z,u,x). [para(691(a,1),8(a,2)),demod(8(2),8(2),8(3),8(4),8(4))]. given #53 (F,wt=15): 1027 f(x,f(x,y,z),f(u,y,z)) = f(x,y,z). [para(20(a,1),691(a,1,3)),demod(9(1),9(3),9(4),446(4),8(2),8(2),9(4),48(5))]. given #54 (T,wt=15): 1065 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(691(a,1),395(a,2)),demod(9(5),469(6),405(6))]. given #55 (T,wt=15): 1086 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(692(a,1),26(a,2)),demod(8(3),7(3),8(4),8(4),172(4),48(3))]. given #56 (A,wt=33): 33 f(f(x,y,f(z,u,v)),f(z,u,f(y,u,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,u,w)). [para(10(a,1),11(a,1,2)),demod(8(3),8(6,R),9(6))]. given #57 (F,wt=15): 1102 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(401(a,1),748(a,1,3)),demod(13(3),792(5),8(2,R),9(2)),flip(a)]. given #58 (F,wt=15): 1127 f(x,f(y,z,x),f(y,u,z)) = f(y,z,x). [para(8(a,1),767(a,1)),demod(8(2),8(2),8(3,R),8(4),8(4))]. given #59 (T,wt=15): 1331 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(401(a,1),788(a,1,3)),demod(13(3),835(5),8(3,R),9(3)),flip(a)]. given #60 (T,wt=15): 1342 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(10(a,1),802(a,1)),demod(9(2))]. given #61 (A,wt=33): 34 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,u,v))) = f(y,f(z,u,v),f(x,u,w)). [para(10(a,1),11(a,1,3)),demod(8(4,R),9(4),8(5),9(9))]. given #62 (F,wt=15): 1589 f(x,f(y,z,u),f(x,y,z)) = f(x,y,z). [back_demod(818),demod(8(2,R),9(2),172(5),391(4),8(4,R),9(4))]. given #63 (F,wt=15): 1596 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(8(a,1),1019(a,1,2)),demod(8(2),9(2),8(4),9(4))]. given #64 (T,wt=15): 1603 f(x,f(y,z,u),f(y,x,u)) = f(y,x,u). [para(1019(a,1),11(a,2)),demod(8(1,R),9(1),8(3,R),9(3),8(4,R),9(4),8(5,R),9(5),7(6),8(5),1482(5),1342(4),9(4))]. given #65 (T,wt=15): 2092 f(x,f(y,z,u),f(y,u,x)) = f(y,u,x). [para(1596(a,1),8(a,2)),demod(8(2),8(2),8(3),8(4),8(4))]. given #66 (A,wt=33): 35 f(f(x,y,f(x,z,u)),f(x,v,f(x,y,u)),f(x,w,f(x,y,u))) = f(x,f(x,y,u),f(z,v,w)). [para(10(a,2),11(a,1,1)),demod(8(1,R),9(1),9(3),8(4,R),9(4),9(5),8(6,R),9(6),9(8))]. given #67 (F,wt=18): 428 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)). [para(20(a,1),26(a,1,1)),demod(28(4)),flip(a)]. given #68 (F,wt=18): 429 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,v,u)). [para(20(a,1),26(a,1,2)),demod(9(2),26(4),8(1),9(3),8(4),9(4)),flip(a)]. given #69 (T,wt=18): 509 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(401(a,1),26(a,1,1)),demod(27(4)),flip(a)]. given #70 (T,wt=18): 548 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(10(a,1),394(a,1,3,3)),demod(9(1),8(2,R),9(2),8(3,R),9(3),9(5))]. given #71 (A,wt=21): 38 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(10(a,1),11(a,2,3)),demod(8(2),8(2),8(3,R),9(3),8(4),8(4),27(5),9(4),8(5,R),9(5))]. given #72 (F,wt=18): 549 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(10(a,2),394(a,1,3,3)),demod(8(3,R),9(3),9(5))]. given #73 (F,wt=18): 575 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)). [para(13(a,1),27(a,1,3)),demod(8(3),9(4))]. given #74 (T,wt=18): 647 f(x,f(y,z,x),f(y,x,u)) = f(y,x,f(z,x,u)). [para(13(a,1),28(a,1,3)),demod(8(3),9(4))]. given #75 (T,wt=18): 695 f(x,f(y,z,f(z,u,v)),f(x,z,v)) = f(x,z,v). [para(10(a,1),568(a,1,2)),demod(8(3,R),9(3),8(5,R),9(5))]. given #76 (A,wt=21): 40 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,w,u))). [para(10(a,2),11(a,2,3)),demod(8(2),8(2),8(4),8(4),27(5)),flip(a)]. given #77 (F,wt=18): 704 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(15(a,1),568(a,1,2)),demod(8(1,R),9(1),8(3),8(3),8(5),8(5))]. given #78 (F,wt=18): 706 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(16(a,1),568(a,1,2)),demod(8(3,R),9(3),205(4),8(5,R),9(5))]. given #79 (T,wt=18): 728 f(x,y,f(z,f(y,z,u),f(x,z,v))) = f(x,y,z). [para(568(a,1),391(a,2)),demod(8(1,R),9(1),8(4,R),9(4),8(5),703(6),446(5),485(4),8(5,R),9(5))]. given #80 (T,wt=18): 774 f(x,y,f(z,x,f(z,u,f(z,y,v)))) = f(z,x,y). [para(568(a,1),598(a,1,3)),demod(8(3,R),13(3),8(5),753(6),758(5)),flip(a)]. given #81 (A,wt=45): 42 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(11(a,1),11(a,1,1)),demod(8(3),8(3),8(4),8(4),8(6),8(6),8(7),8(7),8(10),8(10),8(11),8(11),8(12),8(12),8(13),8(13))]. given #82 (F,wt=18): 821 f(f(x,y,z),f(x,z,u),f(x,y,z)) = f(x,y,z). [para(20(a,1),690(a,1,3)),demod(20(6))]. given #83 (F,wt=18): 962 f(x,y,f(x,z,f(u,y,f(z,y,v)))) = f(x,z,y). [para(391(a,1),29(a,1,3)),demod(8(2),8(2),8(3),8(3),48(4),13(4),8(2),8(2),8(3),8(3),9(4),8(5,R),9(5),453(6),9(3),172(6),48(5)),flip(a)]. given #84 (T,wt=18): 967 f(x,y,f(z,x,f(y,u,f(z,y,v)))) = f(z,x,y). [para(394(a,1),29(a,2,3)),demod(13(1),8(1),8(1),8(2),8(2),468(5),758(5),48(4),8(5),8(5),9(6),13(7))]. given #85 (T,wt=18): 977 f(x,y,f(z,x,f(u,y,f(z,y,v)))) = f(z,x,y). [para(547(a,1),29(a,1,3)),demod(8(2),8(2),8(3),8(3),48(4),13(4),8(2),8(2),8(3),8(3),9(4),8(5,R),9(5),452(6),9(3),758(6),48(5)),flip(a)]. given #86 (A,wt=45): 43 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(11(a,1),11(a,1,2)),demod(8(2),8(2),8(4),8(4),8(7),8(7),8(11),8(11),8(12),8(12),9(13))]. given #87 (F,wt=18): 1079 f(x,y,f(x,z,f(u,y,f(v,z,y)))) = f(x,z,y). [para(691(a,1),691(a,1,3)),demod(9(5),446(5),8(3,R),9(3),579(4),691(7))]. given #88 (F,wt=18): 1109 f(x,y,f(z,x,f(u,z,f(z,y,v)))) = f(z,x,y). [para(568(a,1),748(a,1,3)),demod(13(3),792(6),8(3,R),9(3)),flip(a)]. given #89 (T,wt=18): 1122 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x). [back_demod(1072),demod(1110(5))]. given #90 (T,wt=18): 1126 f(x,y,f(z,f(x,y,z),f(x,u,v))) = f(x,y,z). [back_demod(390),demod(8(3,R),9(3),1110(4),9(2))]. given #91 (A,wt=45): 44 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(11(a,1),11(a,1,3)),demod(8(2),8(2),8(5),8(5),8(7),8(7),8(11),8(11),8(12),8(12))]. given #92 (F,wt=18): 1167 f(x,f(y,z,x),f(y,u,f(y,v,z))) = f(y,z,x). [para(767(a,1),690(a,1,3)),demod(8(2),8(2),9(3),8(4),8(4),9(5),1110(5),8(5),8(5),1127(7))]. given #93 (F,wt=18): 1351 f(x,y,f(z,f(x,y,z),f(y,u,v))) = f(x,y,z). [para(802(a,1),395(a,2)),demod(8(1),8(2,R),9(2),8(3),8(4,R),9(4),9(5),469(6),9(3),8(4,R),9(4),1091(4),1107(4),8(1,R),9(1),8(5),8(5))]. given #94 (T,wt=18): 1631 f(x,y,f(z,f(u,y,z),f(x,z,v))) = f(x,y,z). [para(691(a,1),1027(a,2)),demod(691(3),446(5),485(4))]. given #95 (T,wt=18): 1892 f(x,y,f(z,x,f(z,u,f(z,v,y)))) = f(z,x,y). [para(1102(a,1),690(a,1,3)),demod(8(1,R),9(1),8(5),1849(5),9(2),8(5,R),9(5),802(7))]. given #96 (A,wt=21): 58 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(14(a,1),10(a,1,3)),demod(8(1,R),9(1),9(5),8(6,R),9(6))]. given #97 (F,wt=18): 2083 f(x,f(y,z,f(y,u,v)),f(x,y,u)) = f(x,y,u). [para(10(a,2),1589(a,1,2)),demod(8(1,R),9(1),9(3),9(5))]. given #98 (F,wt=18): 2084 f(x,f(y,z,f(y,u,v)),f(x,y,v)) = f(x,y,v). [para(16(a,1),1589(a,1,2))]. given #99 (T,wt=18): 2115 f(x,y,f(x,z,f(u,y,f(z,v,y)))) = f(x,z,y). [para(1596(a,1),691(a,1,3)),demod(9(5),446(5),8(3,R),9(3),579(4),1596(7))]. given #100 (T,wt=18): 2122 f(x,y,f(z,f(y,u,z),f(x,z,v))) = f(x,y,z). [para(1596(a,1),1027(a,2)),demod(1596(3),446(5),485(4))]. given #101 (A,wt=21): 59 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,z,u))). [para(10(a,1),14(a,1,3)),demod(8(2,R),9(2),8(4,R),9(4))]. given #102 (F,wt=18): 2529 f(x,y,f(x,z,f(y,u,f(z,y,v)))) = f(x,z,y). [para(548(a,1),8(a,2)),demod(8(1,R),9(1),9(4),8(5),8(5))]. given #103 (F,wt=18): 2592 f(x,f(y,z,f(y,u,v)),f(y,x,u)) = f(y,x,u). [para(548(a,1),548(a,2)),demod(9(7),2154(9),2533(10))]. given #104 (T,wt=18): 2652 f(x,y,f(x,z,f(z,u,f(z,y,v)))) = f(x,z,y). [para(549(a,1),8(a,2)),demod(8(1,R),9(1),9(4),8(5),8(5))]. given #105 (T,wt=18): 2655 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(10(a,2),549(a,1,3))]. given #106 (A,wt=21): 60 f(x,y,f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,v,u))). [para(10(a,2),14(a,2,3)),flip(a)]. given #107 (F,wt=18): 2717 f(x,f(y,z,f(u,y,v)),f(u,x,y)) = f(u,x,y). [para(549(a,1),548(a,2)),demod(9(7),2154(9),2533(10))]. given #108 (F,wt=18): 2798 f(x,f(y,z,f(z,u,v)),f(z,v,x)) = f(z,v,x). [para(695(a,1),8(a,2)),demod(8(3),8(3),8(4),8(5),8(5))]. given #109 (T,wt=15): 5763 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(2798(a,1),748(a,1,3)),demod(13(3),9(3),8(4,R),9(4),835(7),8(5,R),9(5),4194(6),8(2),8(3,R),9(3)),flip(a)]. given #110 (T,wt=18): 2807 f(x,y,f(x,z,f(u,y,f(y,v,z)))) = f(x,y,z). [para(695(a,1),11(a,2)),demod(7(3),8(3,R),9(3),8(6,R),9(6),2154(7),20(6))]. given #111 (A,wt=33): 61 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(14(a,1),11(a,1,1)),demod(8(4,R),9(4),8(6,R),9(6))]. given #112 (F,wt=18): 2810 f(x,y,f(z,u,f(x,u,f(u,v,y)))) = f(x,u,y). [para(20(a,1),695(a,1,3)),demod(9(1),9(4),9(5),2154(5),2374(5),8(1),8(1),9(5),48(6))]. given #113 (F,wt=18): 2890 f(x,y,f(z,u,f(z,y,f(x,v,z)))) = f(x,z,y). [para(695(a,1),34(a,2)),demod(7(3),2154(7),1095(6),8(2),7(2),8(2),2154(3))]. given #114 (T,wt=18): 2980 f(x,f(y,z,f(z,u,v)),f(z,u,x)) = f(z,u,x). [para(704(a,1),8(a,2)),demod(8(3),8(3),8(4),8(5),8(5))]. given #115 (T,wt=18): 3032 f(x,y,f(z,y,f(z,u,f(x,v,z)))) = f(x,z,y). [para(704(a,1),34(a,2)),demod(7(3),2154(7),1095(6),8(2),7(2),8(2),2154(3))]. given #116 (A,wt=33): 62 f(f(x,y,f(z,u,v)),f(z,u,f(y,z,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)). [para(14(a,1),11(a,1,2)),demod(8(3,R),9(3),8(6,R),9(6))]. given #117 (F,wt=15): 6568 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(568(a,1),62(a,1,3)),demod(8(1,R),9(1),8(4,R),9(4),48(4),8(4,R),9(4),13(5),8(2,R),9(2),2154(5),2230(5),8(2,R),9(2),8(3,R),9(3)),flip(a)]. given #118 (F,wt=18): 3097 f(x,y,f(z,y,f(z,u,f(x,z,v)))) = f(x,z,y). [para(728(a,1),9(a,2)),demod(8(1,R),9(1),2154(3),9(4),9(5))]. given #119 (T,wt=18): 3108 f(x,y,f(z,y,f(z,u,f(z,x,v)))) = f(z,x,y). [para(728(a,1),11(a,2)),demod(8(2,R),9(2),8(3),8(3),8(4,R),9(4),8(5),8(5),27(6),2154(3),8(5))]. given #120 (T,wt=18): 3246 f(x,f(y,z,f(u,y,v)),f(x,u,y)) = f(x,u,y). [para(548(a,1),774(a,2)),demod(8(1,R),9(1),8(4,R),9(4),9(7),8(9,R),9(9),2154(10),3200(10),8(5),8(5))]. given #121 (A,wt=33): 63 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,z,v))) = f(y,f(z,u,v),f(x,z,w)). [para(14(a,1),11(a,1,3)),demod(8(4,R),9(4),8(5,R),9(5),9(9))]. given #122 (F,wt=18): 3259 f(x,y,f(z,y,f(x,u,f(z,x,v)))) = f(z,x,y). [para(774(a,1),774(a,2)),demod(8(1,R),9(1),8(4,R),9(4),9(7),8(9,R),9(9),3199(10),8(5))]. given #123 (F,wt=18): 3712 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(967(a,1),8(a,2)),demod(8(1,R),9(1),9(4),8(5))]. given #124 (T,wt=18): 3756 f(x,y,f(y,z,f(u,z,f(x,z,v)))) = f(x,y,z). [para(10(a,1),977(a,1)),demod(9(3))]. given #125 (T,wt=18): 4172 f(x,f(y,z,f(y,u,v)),f(y,u,x)) = f(y,u,x). [para(1122(a,1),9(a,1)),demod(8(2),8(2)),flip(a)]. given #126 (A,wt=21): 68 f(x,f(y,z,u),f(x,z,v)) = f(x,v,f(y,z,f(x,z,u))). [para(15(a,1),10(a,2,3)),demod(8(2),8(2),8(6,R),9(6))]. given #127 (F,wt=18): 4295 f(x,y,f(z,f(x,z,y),f(y,u,v))) = f(x,z,y). [para(1126(a,1),8(a,2)),demod(8(1),8(1),9(4),8(5),8(5))]. given #128 (F,wt=18): 4398 f(x,y,f(z,f(u,y,z),f(x,u,z))) = f(x,y,z). [para(13(a,1),44(a,2)),demod(8(1,R),9(1),48(3),2154(3),48(2),8(3,R),9(3),48(5),647(5),9(6),429(7),13(5),8(6),418(6),48(6))]. given #129 (T,wt=18): 4595 f(x,y,f(z,f(x,z,y),f(u,z,y))) = f(x,z,y). [para(1167(a,1),15(a,1,3)),demod(13(3),9(4),4194(7),8(3)),flip(a)]. given #130 (T,wt=18): 4698 f(x,y,f(z,f(x,z,u),f(y,v,z))) = f(x,y,z). [para(1631(a,1),428(a,2)),demod(8(1,R),9(1),9(3),429(5),8(3,R))]. given #131 (A,wt=21): 69 f(x,y,f(z,u,f(y,u,v))) = f(y,u,f(x,y,f(z,u,v))). [para(10(a,1),15(a,1,3)),demod(8(1),8(6,R),9(6))]. given #132 (F,wt=18): 4723 f(x,y,f(x,z,f(z,u,f(z,v,y)))) = f(x,z,y). [para(1892(a,1),9(a,2)),demod(8(3,R),9(3),9(4),8(5,R),9(5))]. given #133 (F,wt=18): 4726 f(x,y,f(y,z,f(x,u,f(x,v,z)))) = f(x,y,z). [para(10(a,1),1892(a,1)),demod(9(3))]. given #134 (T,wt=18): 5053 f(x,f(y,z,f(y,u,v)),f(y,v,x)) = f(y,v,x). [para(2084(a,1),8(a,2)),demod(8(3),8(3),8(4),8(5),8(5))]. given #135 (T,wt=18): 5058 f(x,y,f(z,u,f(x,z,f(z,v,y)))) = f(x,z,y). [para(20(a,1),2084(a,1,3)),demod(9(1),9(4),9(5),2154(5),4884(5),8(1),8(1),9(5),48(6))]. given #136 (A,wt=21): 70 f(x,y,f(z,x,f(x,u,v))) = f(z,x,f(x,u,f(x,y,v))). [para(10(a,2),15(a,1,3)),demod(8(1,R),9(1),9(4),8(6,R),9(6)),flip(a)]. given #137 (F,wt=18): 5653 f(x,f(y,z,f(u,z,v)),f(x,u,z)) = f(x,u,z). [para(8(a,2),2717(a,1,2)),demod(9(2),8(3,R),9(3),8(5,R),9(5))]. given #138 (F,wt=18): 5745 f(x,f(y,z,f(y,u,v)),f(y,x,v)) = f(y,x,v). [para(2798(a,1),11(a,2)),demod(8(2,R),9(2),8(5,R),9(5),8(6,R),9(6),8(8,R),9(8),7(9),8(7),1482(7),4726(6),9(5))]. given #139 (T,wt=18): 5817 f(x,y,f(x,z,f(y,u,f(v,y,z)))) = f(x,y,z). [para(1331(a,1),5763(a,2)),demod(8(2),8(3),2154(6),1762(7),9(5),1632(5),428(4),8(5))]. given #140 (T,wt=18): 6132 f(x,y,f(z,u,f(u,x,f(u,v,y)))) = f(u,x,y). [para(8(a,1),2810(a,1)),demod(8(2,R),9(2),8(4),8(4),8(5,R),9(5))]. given #141 (A,wt=21): 71 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,u,v))). [para(10(a,1),15(a,2,3)),demod(8(1,R),9(1),8(2,R),9(2),9(4),8(5,R),9(5),8(6,R),9(6)),flip(a)]. given #142 (F,wt=18): 6452 f(x,f(y,z,f(u,y,v)),f(u,y,x)) = f(u,y,x). [para(728(a,1),3032(a,2)),demod(8(1,R),9(1),2154(3),8(4,R),9(4),2154(6),9(7),1482(9),412(10),8(5),967(6),9(5))]. given #143 (F,wt=18): 7832 f(x,f(y,x,z),f(u,x,z)) = f(y,x,f(u,x,z)). [para(691(a,1),69(a,2,3)),demod(8(3),8(3),401(3),20(4),8(5,R)),flip(a)]. given #144 (T,wt=18): 7857 f(x,f(y,z,x),f(u,z,x)) = f(y,x,f(u,z,x)). [para(1019(a,1),69(a,2,3)),demod(8(3),9(3),509(4),8(2,R),9(2),2511(4),13(2),9(2),8(4),8(5,R)),flip(a)]. given #145 (T,wt=18): 7880 f(x,f(y,z,x),f(z,u,x)) = f(y,x,f(z,u,x)). [para(2092(a,1),69(a,2,3)),demod(8(3),9(3),428(4),8(2,R),9(2),2436(4),13(2),9(2),8(4),8(5,R)),flip(a)]. given #146 (A,wt=21): 72 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,v,f(x,y,u))). [para(10(a,2),15(a,2,3)),demod(8(2,R),9(2),8(6,R),9(6))]. given #147 (F,wt=18): 8152 f(x,y,f(z,u,f(z,x,f(z,v,y)))) = f(z,x,y). [para(8(a,1),5058(a,1)),demod(8(2,R),9(2),8(4),8(4),8(5,R),9(5))]. given #148 (F,wt=18): 8389 f(x,y,f(x,z,f(u,z,f(z,y,v)))) = f(x,z,y). [para(5653(a,1),11(a,2)),demod(8(1,R),9(1),7(3),8(1,R),9(1),8(3,R),9(3),8(4,R),9(4),8(6,R),9(6),2154(7),20(6),9(5))]. given #149 (T,wt=21): 76 f(x,y,f(z,u,f(v,z,w))) = f(x,y,f(v,z,f(z,u,w))). [para(15(a,1),11(a,2,3)),demod(8(2),8(2),8(3,R),9(3),8(4),8(4),27(5),8(5,R),9(5)),flip(a)]. given #150 (T,wt=21): 81 f(x,y,f(z,u,f(y,z,v))) = f(y,z,f(x,y,f(z,u,v))). [para(14(a,1),15(a,1,3)),demod(8(1,R),9(1),8(6,R),9(6))]. given #151 (A,wt=33): 73 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(15(a,1),11(a,1,1)),demod(8(1,R),9(1),8(4,R),9(4),8(6,R),9(6))]. given #152 (F,wt=21): 82 f(x,y,f(y,z,f(y,u,v))) = f(y,z,f(y,u,f(x,y,v))). [para(15(a,1),15(a,2,3)),demod(8(1,R),9(1),8(2,R),9(2),8(5,R),9(5),8(6,R),9(6))]. given #153 (F,wt=21): 84 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,z,f(x,y,u))). [para(10(a,2),16(a,1,3)),demod(9(4),9(5)),flip(a)]. given #154 (T,wt=21): 89 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,u,v))). [para(16(a,1),11(a,2,3)),demod(8(2),8(2),8(4),8(4),27(5),9(4))]. given #155 (T,wt=21): 92 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,v,z))). [para(16(a,1),14(a,2,3)),demod(9(4)),flip(a)]. given #156 (A,wt=33): 86 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(16(a,1),11(a,1,1)),demod(9(3),8(4,R),9(4),9(5),8(6,R),9(6),9(8))]. given #157 (F,wt=21): 94 f(x,y,f(z,u,f(z,x,v))) = f(z,x,f(x,y,f(z,v,u))). [para(16(a,1),15(a,2,3)),demod(8(2,R),9(2),9(4),8(6,R),9(6)),flip(a)]. given #158 (F,wt=21): 95 f(x,f(y,z,u),f(x,v,z)) = f(x,v,f(y,z,f(x,z,u))). [para(15(a,1),16(a,1,3)),demod(9(5)),flip(a)]. given #159 (T,wt=21): 116 f(x,y,f(z,u,f(u,y,v))) = f(u,y,f(x,y,f(z,u,v))). [para(18(a,1),8(a,2)),demod(8(1,R),9(1),9(3),8(5,R),9(5),8(6,R),9(6))]. given #160 (T,wt=18): 10263 f(x,f(y,z,x),f(u,y,x)) = f(u,x,f(y,z,x)). [para(2092(a,1),116(a,2,3)),demod(8(3),428(4),8(2,R),9(2),2436(4),13(2),9(2),8(4)),flip(a)]. given #161 (A,wt=33): 87 f(f(x,y,f(z,u,v)),f(z,v,f(y,z,u)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)). [para(16(a,1),11(a,1,2)),demod(8(3),8(6,R),9(6))]. given #162 (F,wt=21): 117 f(x,y,f(z,u,f(u,x,v))) = f(u,x,f(x,y,f(z,u,v))). [para(8(a,1),18(a,1)),demod(8(1,R),9(1),8(3),8(3),8(6,R),9(6))]. given #163 (F,wt=18): 10453 f(x,y,f(y,z,f(z,u,f(x,v,z)))) = f(x,y,z). [para(117(a,1),5653(a,1)),demod(9(3),469(4),9(1),8(4,R),9(4),9(5),758(5),48(4),429(5),9(3),8(6,R),9(6),48(6))]. given #164 (T,wt=21): 173 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,y,f(x,u,z))). [para(10(a,2),24(a,2,3)),demod(8(3),8(3),41(4),8(4),8(4)),flip(a)]. given #165 (T,wt=21): 180 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,y,z))). [para(15(a,1),24(a,1,3)),demod(8(1,R),9(1),9(2),8(3),8(3),8(4,R),9(4),172(5),41(5),172(4),9(2),172(4),48(2),8(4,R),9(4),8(5),8(5),172(6)),flip(a)]. given #166 (A,wt=33): 88 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,v,f(y,z,u))) = f(y,f(z,u,v),f(x,z,w)). [para(16(a,1),11(a,1,3)),demod(8(4,R),9(4),8(5),9(9))]. given #167 (F,wt=18): 10642 f(x,y,f(z,u,f(z,v,f(z,x,y)))) = f(z,x,y). [para(180(a,1),69(a,2,3)),demod(392(4)),flip(a)]. given #168 (F,wt=18): 10726 f(x,y,f(z,u,f(z,v,f(x,z,y)))) = f(x,z,y). [para(2084(a,1),88(a,2)),demod(7(3),2154(6),2154(7),10523(6),8(1),20(2))]. given #169 (T,wt=18): 10736 f(x,y,f(z,f(x,y,z),f(z,u,v))) = f(x,y,z). [para(16(a,1),10642(a,1,3)),demod(8(1),8(1),8(5),8(5))]. given #170 (T,wt=21): 184 f(x,f(y,z,u),f(x,v,y)) = f(x,v,f(y,u,f(x,y,z))). [para(16(a,1),24(a,2,3)),demod(8(3),8(3),9(4),41(4),8(4))]. given #171 (A,wt=33): 100 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(39(a,1),11(a,1,1)),demod(8(4,R),9(4),8(6,R),9(6))]. given #172 (F,wt=18): 11099 f(x,y,f(z,x,f(u,z,f(z,v,y)))) = f(z,x,y). [para(2798(a,1),100(a,2)),demod(7(9),8(7),8660(7),7(4),9(3),9(5))]. given #173 (F,wt=21): 186 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,u,y))). [para(24(a,1),23(a,1,2)),demod(8(1,R),9(1),8(3),8(3),9(4),172(5),48(3),172(4),20(2),8(4),8(4),9(6),172(7),48(5))]. given #174 (T,wt=21): 187 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,u,f(x,z,y))). [para(24(a,1),23(a,1,3)),demod(8(3),8(3),172(5),41(5),172(4),172(4),20(2),8(5),8(5),172(7),48(5))]. given #175 (T,wt=21): 228 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,z,f(x,y,v))). [para(50(a,1),25(a,1,3)),demod(8(1,R),9(1),172(4),181(4),8(6,R),9(6),181(7))]. given #176 (A,wt=42): 108 f(f(x,y,f(x,z,u)),f(v,f(x,z,y),f(x,y,u)),f(w,f(x,z,y),f(x,y,u))) = f(f(x,z,y),f(x,y,u),f(w,x,v)). [para(23(a,1),11(a,1,2)),demod(8(9,R))]. given #177 (F,wt=21): 264 f(x,y,f(x,z,f(x,u,v))) = f(x,v,f(x,z,f(x,y,u))). [para(19(a,1),16(a,1)),demod(9(5),172(6))]. given #178 (F,wt=21): 267 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,v,f(x,y,z))). [para(19(a,1),16(a,2)),demod(172(3),9(4))]. given #179 (T,wt=21): 316 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,w,f(z,v,u))). [para(77(a,1),11(a,2,3)),demod(8(2,R),9(2),8(3),8(3),8(4),9(4),8(5),8(5),27(6),172(3),48(2),8(4,R),9(4),8(5,R),9(5))]. given #180 (T,wt=21): 377 f(x,y,f(x,z,f(u,v,f(x,v,y)))) = f(x,z,f(x,v,y)). [para(350(a,1),24(a,2,3)),demod(8(1),8(1),8(4),8(4),9(5),172(5),48(4),8(5),8(5))]. given #181 (A,wt=36): 109 f(f(x,y,z),f(u,f(y,z,v),f(x,y,z)),f(y,z,f(x,v,w))) = f(u,f(x,y,z),f(y,z,f(x,v,w))). [para(11(a,1),23(a,1,3)),demod(8(3),8(3),8(4,R),8(9),8(9),8(11),8(11),8(12,R),65(13))]. given #182 (F,wt=21): 398 f(x,f(y,z,u),f(x,v,f(x,y,u))) = f(x,v,f(x,y,u)). [para(353(a,1),10(a,2,3)),demod(9(1),8(3),8(3),203(4),9(5),8(6,R),9(6))]. given #183 (F,wt=21): 404 f(x,y,f(x,z,f(x,u,f(u,v,y)))) = f(x,z,f(x,u,y)). [para(353(a,1),24(a,1,3)),demod(8(1),8(1),9(3),8(4),8(4),9(5),172(5),56(3),8(5),8(5),8(7,R),9(7),203(8),398(8))]. given #184 (T,wt=21): 405 f(x,y,f(x,z,f(u,v,f(x,u,y)))) = f(x,z,f(x,u,y)). [para(353(a,1),24(a,2,3)),demod(8(1),8(1),8(4),8(4),9(5),172(5),48(4),8(5),8(5))]. given #185 (T,wt=21): 406 f(x,f(y,z,u),f(x,u,f(x,y,v))) = f(x,v,f(x,y,u)). [para(353(a,1),67(a,1,3,3)),demod(9(1),9(3),203(5),172(4),48(3),9(5),396(7))]. given #186 (A,wt=27): 118 f(x,y,f(z,u,f(x,z,f(u,v,w)))) = f(x,z,f(x,y,f(u,v,f(z,u,w)))). [para(18(a,1),10(a,1,3)),demod(8(1,R),9(1),8(2,R),9(2),8(6,R),9(6),9(7),8(8,R),9(8))]. given #187 (F,wt=18): 11932 f(f(x,y,z),f(y,u,v),f(x,y,z)) = f(x,y,z). [para(690(a,1),118(a,2,3)),demod(9(4),8(5,R),1589(5),48(4),8(8,R),9(8),2154(8),428(7),7(5),9(5),48(6))]. given #188 (F,wt=18): 11976 f(f(x,y,z),f(z,u,v),f(x,y,z)) = f(x,y,z). [para(8(a,1),11932(a,1,1)),demod(8(3),8(5))]. given #189 (T,wt=18): 11977 f(f(x,y,z),f(x,u,v),f(x,y,z)) = f(x,y,z). [para(8(a,2),11932(a,1,1)),demod(8(3),8(3),8(5),8(5))]. given #190 (T,wt=21): 437 f(x,f(y,z,u),f(v,x,y)) = f(v,x,f(y,z,f(x,y,u))). [para(26(a,1),18(a,2,3)),demod(8(4),8(4),56(5),9(3),26(5),8(2),8(5),8(7,R),9(7),310(7)),flip(a)]. given #191 (A,wt=27): 119 f(x,y,f(z,u,f(x,v,f(x,z,w)))) = f(x,z,f(x,y,f(z,u,f(x,v,w)))). [para(18(a,2),10(a,1,3)),demod(8(1,R),9(1),8(2,R),9(2),8(5,R),9(5),9(7),8(8,R),9(8))]. given #192 (F,wt=18): 12151 f(x,y,f(z,u,f(z,y,f(z,v,x)))) = f(z,x,y). [back_demod(5077),demod(12084(9),9(2))]. given #193 (F,wt=21): 473 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(y,v,u))). [back_demod(162),demod(469(4),9(1),48(4),428(6))]. given #194 (T,wt=18): 12275 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)). [para(11(a,1),473(a,2,3)),demod(8(2),8(2),8(4),8(4),8(5,R),2154(5),509(5),8(5,R),9(5),758(5),48(4),1102(4),8(3,R),9(5),8(7,R),9(7),11571(7))]. ============================== PROOF ================================= % Proof 1 at 55.10 (+ 0.09) seconds: dist_short. % Length of proof is 115. % Level of proof is 19. % Maximum clause weight is 45. % Given clauses 194. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 5 f(f(x,y,z),u,v) = f(f(x,u,v),f(y,u,v),f(z,u,v)) # label(dist_long). [input]. 6 f(f(c1,c2,c3),c4,E) != f(c1,f(c2,c4,E),f(c3,c4,E)) # answer(dist_short). [clausify]. 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. 11 f(f(x,y,z),f(u,y,z),f(v,y,z)) = f(y,z,f(x,u,v)) # label(dist_long). [copy(5),demod(8(2),8(2)),flip(a)]. 12 f(c1,f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_short). [copy(6),demod(8(7),9(7),8(12),8(16)),flip(a)]. 13 f(x,y,y) = y. [para(8(a,1),7(a,1))]. 14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [para(10(a,2),8(a,1)),demod(8(1,R),9(1),9(3),8(4),9(4))]. 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(10(a,1),8(a,2)),demod(9(2),8(3))]. 18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(10(a,1),10(a,1,3)),demod(8(1),9(5),8(6,R),9(6))]. 20 f(x,y,f(x,z,y)) = f(x,z,y). [para(10(a,2),10(a,1)),demod(8(1,R),13(1),8(2),9(2)),flip(a)]. 23 f(x,f(x,y,z),f(x,z,u)) = f(x,z,f(x,y,u)). [para(7(a,1),11(a,1,1)),demod(8(1,R),9(1),8(2),8(2))]. 24 f(x,f(x,y,z),f(u,x,y)) = f(x,y,f(u,x,z)). [para(7(a,1),11(a,1,2)),demod(8(2),8(2),8(3,R))]. 25 f(x,f(y,x,z),f(x,z,u)) = f(x,z,f(y,x,u)). [para(7(a,1),11(a,1,3)),demod(8(2),8(2),8(3),9(4))]. 26 f(f(x,y,z),f(x,y,u),f(x,y,v)) = f(x,y,f(u,v,z)). [para(11(a,1),8(a,1)),demod(8(3),8(3),8(4),8(4),8(5),8(5)),flip(a)]. 27 f(f(x,y,z),f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(11(a,1),8(a,2)),demod(8(2),8(2),8(3),8(3),8(5),8(5))]. 28 f(f(x,y,z),f(x,z,u),f(x,z,v)) = f(x,z,f(y,u,v)). [para(8(a,1),11(a,1,1)),demod(8(2),9(2),8(3),9(3),8(6,R),9(6))]. 30 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(11(a,1),10(a,2,3)),demod(8(2),8(2),8(4),8(4),9(8))]. 34 f(f(x,y,f(z,u,v)),f(y,w,f(z,u,v)),f(z,u,f(y,u,v))) = f(y,f(z,u,v),f(x,u,w)). [para(10(a,1),11(a,1,3)),demod(8(4,R),9(4),8(5),9(9))]. 35 f(f(x,y,f(x,z,u)),f(x,v,f(x,y,u)),f(x,w,f(x,y,u))) = f(x,f(x,y,u),f(z,v,w)). [para(10(a,2),11(a,1,1)),demod(8(1,R),9(1),9(3),8(4,R),9(4),9(5),8(6,R),9(6),9(8))]. 39 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(10(a,1),11(a,2)),demod(7(2),8(2),8(2),8(3,R),24(3),9(3))]. 41 f(x,f(x,y,z),f(x,y,u)) = f(x,u,f(x,y,z)). [para(10(a,2),11(a,2)),demod(8(1),7(1),8(1),9(1),8(2),9(2),8(4,R),9(4))]. 48 f(x,y,f(x,y,z)) = f(x,y,z). [para(13(a,1),10(a,2,3)),demod(8(1),8(1),8(3),8(3))]. 50 f(x,y,f(x,z,f(x,y,u))) = f(x,z,f(x,y,u)). [para(20(a,1),10(a,1,3)),demod(8(1),8(3),9(4),8(5,R),9(5)),flip(a)]. 53 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(20(a,1),11(a,1,1)),demod(8(3,R),9(3),8(5,R),9(5))]. 56 f(x,y,f(y,z,f(x,y,u))) = f(x,y,f(y,z,u)). [para(10(a,2),48(a,1,3)),demod(9(4))]. 57 f(f(x,y,z),f(y,u,f(x,y,z)),f(y,v,f(x,y,z))) = f(y,f(x,y,z),f(x,u,v)). [para(48(a,1),11(a,1,1)),demod(8(3,R),9(3),8(5,R),9(5))]. 62 f(f(x,y,f(z,u,v)),f(z,u,f(y,z,v)),f(y,w,f(z,u,v))) = f(y,f(z,u,v),f(x,z,w)). [para(14(a,1),11(a,1,2)),demod(8(3,R),9(3),8(6,R),9(6))]. 64 f(x,f(y,x,z),f(z,f(y,x,z),f(x,z,u))) = f(x,z,f(y,u,f(y,x,z))). [para(14(a,1),11(a,1)),demod(8(3),8(3),8(4),8(5,R),9(5))]. 65 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(11(a,1),14(a,1,3)),demod(8(4,R),9(4),8(6),8(6),8(8),8(8),8(9,R)),flip(a)]. 66 f(x,f(x,y,z),f(y,f(x,y,z),f(x,y,u))) = f(x,y,f(z,u,f(x,y,z))). [para(11(a,1),14(a,1)),demod(8(1),8(1),8(4),8(4),8(5),8(5),8(6),8(6),8(7),8(8,R),9(8)),flip(a)]. 77 f(x,f(y,x,z),f(u,y,x)) = f(u,x,f(y,x,z)). [para(15(a,1),11(a,2)),demod(8(2,R),13(2),8(2),8(2),8(3,R))]. 107 f(x,f(x,y,z),f(z,u,f(x,z,v))) = f(x,z,f(x,y,f(z,u,v))). [para(10(a,2),23(a,1,3)),demod(9(5))]. 109 f(f(x,y,z),f(u,f(y,z,v),f(x,y,z)),f(y,z,f(x,v,w))) = f(u,f(x,y,z),f(y,z,f(x,v,w))). [para(11(a,1),23(a,1,3)),demod(8(3),8(3),8(4,R),8(9),8(9),8(11),8(11),8(12,R),65(13))]. 121 f(x,f(y,z,u),f(x,y,z)) = f(y,z,f(x,y,f(x,z,u))). [para(18(a,1),10(a,2)),demod(8(2,R),9(2),8(5,R),9(5))]. 137 f(f(x,y,z),f(y,z,u),f(y,v,f(y,z,f(x,y,z)))) = f(y,z,f(x,y,f(x,u,v))). [para(11(a,1),18(a,2,3)),demod(8(2),8(2),8(4),8(4),8(5,R),9(5),8(10,R),9(10),25(10))]. 142 f(x,y,f(x,z,f(y,u,f(x,y,v)))) = f(x,y,f(x,z,f(y,u,v))). [para(18(a,2),48(a,1,3)),demod(8(2,R),9(2),8(5,R),9(5))]. 159 f(x,f(x,y,f(x,z,f(y,u,v))),f(x,w,f(y,u,f(x,y,v)))) = f(x,f(y,u,f(x,y,v)),f(x,z,w)). [para(18(a,1),23(a,1,2)),demod(8(1,R),9(1),8(5,R),9(5),9(6),8(9,R),9(9))]. 162 f(x,y,f(z,f(x,y,u),f(x,v,f(x,y,u)))) = f(x,y,f(x,u,f(z,v,f(x,y,u)))). [para(18(a,2),23(a,1)),demod(9(1),9(2),9(3),9(6),9(7))]. 168 f(x,f(x,y,z),f(u,f(x,y,z),f(x,y,v))) = f(u,f(x,y,z),f(x,y,f(x,z,v))). [para(24(a,1),10(a,1,3)),demod(8(2),8(2),8(4,R),9(4),8(7),8(7),8(8)),flip(a)]. 169 f(x,f(x,y,f(x,z,u)),f(x,u,v)) = f(x,u,f(x,v,f(x,y,z))). [para(10(a,1),24(a,1,2)),demod(8(2,R),9(2),8(3),8(3),8(5,R),9(5),8(6,R),9(6))]. 171 f(x,f(y,z,f(x,y,u)),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))). [para(10(a,2),24(a,1,2)),demod(8(3),8(3),9(5),8(6,R),9(6))]. 172 f(x,f(x,y,z),f(x,u,v)) = f(x,z,f(x,u,f(x,y,v))). [para(10(a,2),24(a,1,3)),demod(9(2),8(3),8(3),169(5),9(2),41(3),8(5),8(5)),flip(a)]. 197 f(x,y,f(x,z,f(x,u,f(x,v,y)))) = f(x,y,f(x,z,f(x,v,u))). [para(24(a,1),24(a,1,2)),demod(8(1,R),9(1),8(4,R),9(4),172(5),48(3),172(4),8(6),8(6),8(7,R),9(7),172(8),48(6))]. 200 f(x,f(y,x,z),f(y,x,f(y,z,u))) = f(y,x,f(z,u,f(y,x,z))). [back_demod(66),demod(168(5))]. 203 f(x,f(y,z,f(x,y,u)),f(x,v,w)) = f(x,f(y,z,u),f(x,w,f(x,y,v))). [back_demod(159),demod(172(7),56(5),172(6),197(6)),flip(a)]. 205 f(x,f(y,z,u),f(x,y,v)) = f(x,y,f(x,v,f(y,z,u))). [back_demod(171),demod(203(4),13(2),9(2))]. 209 f(x,y,f(z,x,f(z,y,u))) = f(z,x,f(z,y,f(x,y,u))). [back_demod(121),demod(205(3)),flip(a)]. 217 f(f(x,y,z),f(y,z,u),f(y,v,f(x,y,z))) = f(v,f(x,y,z),f(y,z,f(x,y,u))). [para(25(a,1),24(a,1,3)),demod(8(4),9(7),30(7),9(3),20(3),9(8)),flip(a)]. 219 f(x,y,f(x,z,f(y,u,f(x,z,y)))) = f(x,y,f(z,u,f(x,z,y))). [back_demod(64),demod(8(1,R),9(1),8(2,R),9(2),107(5),9(2),8(5,R),9(5))]. 234 f(f(x,y,z),f(y,z,u),f(y,f(y,z,u),f(z,f(x,y,z),f(y,z,u)))) = f(y,z,f(x,u,f(y,z,u))). [para(11(a,1),56(a,2)),demod(8(2),8(2),8(3),8(3),8(5),8(5),8(6),8(7,R),9(7),8(9),8(9))]. 310 f(x,f(y,x,z),f(y,x,u)) = f(x,u,f(y,x,z)). [para(77(a,1),8(a,2)),demod(8(2),8(2),8(3),8(5,R),9(5))]. 319 f(x,f(x,y,z),f(y,u,f(x,y,z))) = f(x,y,z). [para(48(a,1),77(a,1,3)),demod(9(3),8(5),7(5),9(4)),flip(a)]. 325 f(f(x,y,z),f(x,u,f(x,y,z)),f(x,y,f(x,z,v))) = f(v,f(x,y,z),f(x,u,f(x,y,z))). [para(39(a,2),77(a,1,3)),demod(9(3),8(4),8(4),9(9))]. 347 f(x,f(y,z,u),f(z,v,f(y,z,u))) = f(z,f(y,z,u),f(y,v,x)). [para(77(a,1),77(a,1,2)),demod(8(3,R),9(3),8(5,R),9(5),57(6),8(6),8(6),310(7)),flip(a)]. 349 f(x,y,f(z,u,f(x,y,z))) = f(x,z,f(x,y,f(y,z,u))). [back_demod(200),demod(8(1,R),9(1),8(3,R),9(3),172(4),48(3),8(4,R),9(4),8(6,R),9(6)),flip(a)]. 350 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [back_demod(234),demod(319(7),13(4)),flip(a)]. 353 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para(350(a,1),8(a,1)),demod(8(3,R),9(3),8(4),8(4)),flip(a)]. 391 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [back_demod(349),demod(353(3)),flip(a)]. 392 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [back_demod(219),demod(9(1),142(4),9(1),9(4),353(6))]. 394 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [back_demod(209),demod(8(1,R),9(1),8(2,R),9(2),392(3),8(3,R),9(3),8(4,R),9(4)),flip(a)]. 401 f(x,y,f(z,x,y)) = f(z,x,y). [para(353(a,1),15(a,1)),demod(48(3),8(3,R),9(3)),flip(a)]. 412 f(x,f(y,z,u),f(z,u,f(y,z,v))) = f(z,u,f(y,z,f(y,v,x))). [back_demod(137),demod(401(4),217(5))]. 418 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(10(a,1),26(a,1,2)),demod(9(2),8(3,R),9(3),8(6,R),9(6),8(7),9(7))]. 419 f(f(x,y,z),f(x,y,u),f(x,v,f(x,y,w))) = f(x,y,f(z,u,f(x,v,w))). [para(10(a,1),26(a,1,3)),demod(9(3),8(4,R),9(4),8(6,R),9(6),8(7))]. 420 f(f(x,y,f(x,z,u)),f(x,z,v),f(x,z,w)) = f(x,z,f(v,w,f(x,y,u))). [para(10(a,2),26(a,1,1)),demod(8(1,R),9(1),8(3,R),9(3),8(4,R),9(4),9(6),8(8,R),9(8))]. 428 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(v,z,u)). [para(20(a,1),26(a,1,1)),demod(28(4)),flip(a)]. 434 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(39(a,2),26(a,2)),demod(13(2),8(3,R),310(3))]. 452 f(x,y,f(z,u,f(x,v,f(x,y,w)))) = f(x,y,f(z,u,f(x,v,w))). [para(50(a,1),26(a,1,1)),demod(420(5)),flip(a)]. 469 f(x,f(y,z,u),f(y,v,f(y,z,u))) = f(y,z,f(u,v,f(y,u,x))). [back_demod(325),demod(418(6),9(2),310(3)),flip(a)]. 473 f(x,y,f(z,u,f(x,v,z))) = f(x,y,f(x,z,f(y,v,u))). [back_demod(162),demod(469(4),9(1),48(4),428(6))]. 509 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(v,z,u)). [para(401(a,1),26(a,1,1)),demod(27(4)),flip(a)]. 523 f(x,f(y,z,u),f(x,z,f(z,v,f(y,z,u)))) = f(y,z,f(x,z,u)). [para(15(a,1),391(a,2)),demod(9(3))]. 547 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(8(a,1),394(a,1)),demod(8(1,R),9(1),8(3),9(3),8(4),8(4))]. 568 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(394(a,1),26(a,2)),demod(13(4),8(4),9(4),310(4),9(4))]. 575 f(x,f(y,z,x),f(z,x,u)) = f(z,x,f(y,x,u)). [para(13(a,1),27(a,1,3)),demod(8(3),9(4))]. 598 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(434(a,1),8(a,2)),demod(9(2),8(3)),flip(a)]. 624 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(434(a,1),547(a,2)),demod(9(3),8(4,R),9(4),523(5),8(3)),flip(a)]. 636 f(f(x,y,f(y,z,u)),f(y,v,f(x,y,z)),f(y,w,f(x,y,z))) = f(y,f(x,y,z),f(u,v,w)). [para(10(a,1),28(a,1,1)),demod(9(4),9(6))]. 664 f(x,f(y,x,z),f(u,v,f(x,z,w))) = f(x,f(y,x,z),f(w,u,v)). [para(77(a,1),28(a,1,1)),demod(8(1,R),9(1),9(3),9(4),9(5),9(6),636(7),9(4),8(5,R),9(5),8(6),8(6)),flip(a)]. 690 f(x,f(y,z,u),f(y,z,x)) = f(y,z,x). [para(568(a,1),8(a,2)),demod(9(2),8(3),9(4))]. 691 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(8(a,1),568(a,1,2)),demod(8(2,R),9(2),8(4,R),9(4))]. 692 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(8(a,2),568(a,1,2)),demod(8(2),8(2),205(3),8(4),8(4))]. 704 f(x,f(y,z,f(z,u,v)),f(x,z,u)) = f(x,z,u). [para(15(a,1),568(a,1,2)),demod(8(1,R),9(1),8(3),8(3),8(5),8(5))]. 748 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(598(a,1),8(a,2)),demod(9(2),8(3))]. 752 f(x,f(y,z,u),f(y,z,f(z,u,v))) = f(z,f(y,z,u),f(y,x,v)). [para(15(a,1),598(a,1,3)),demod(8(2),8(2),8(4,R),9(4),9(7),347(8))]. 753 f(x,f(y,x,z),f(u,v,f(y,x,z))) = f(x,f(y,x,z),f(y,u,v)). [para(39(a,1),598(a,1,3)),demod(9(2),8(4,R),9(4),752(4),8(6)),flip(a)]. 758 f(x,f(y,x,z),f(y,u,v)) = f(x,z,f(y,x,f(y,u,v))). [para(24(a,1),598(a,1,3)),demod(8(4,R),9(4),412(4),9(1),8(7),753(8),664(7),8(5),8(5)),flip(a)]. 779 f(x,f(y,z,u),f(y,z,f(z,u,v))) = f(z,f(y,z,u),f(x,y,v)). [back_demod(752),demod(8(6,R),9(6))]. 783 f(x,f(y,z,u),f(z,v,f(y,z,u))) = f(z,f(y,z,u),f(x,y,v)). [back_demod(347),demod(8(6))]. 788 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(624(a,1),8(a,2)),demod(9(2),8(3))]. 792 f(x,f(y,x,z),f(u,v,f(y,x,z))) = f(x,z,f(y,x,f(y,u,v))). [para(15(a,1),624(a,1,3)),demod(8(2),8(2),8(4,R),9(4),779(4),8(2,R),9(2),758(3),8(6)),flip(a)]. 835 f(x,f(y,z,x),f(u,v,f(y,z,w))) = f(x,f(y,z,x),f(y,u,v)). [para(690(a,1),28(a,1,1)),demod(9(3),9(5),53(6),8(6),8(6)),flip(a)]. 1090 f(x,f(y,x,z),f(u,y,v)) = f(x,z,f(y,x,f(u,y,v))). [para(10(a,1),748(a,1,3)),demod(779(4),792(7),8(4,R),9(4))]. 1095 f(x,f(y,z,u),f(y,z,f(v,z,u))) = f(z,u,f(y,z,f(v,y,x))). [para(15(a,1),748(a,2,3)),demod(8(3,R),9(3),783(4),1090(3)),flip(a)]. 1102 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(401(a,1),748(a,1,3)),demod(13(3),792(5),8(2,R),9(2)),flip(a)]. 1331 f(x,f(y,z,x),f(u,y,z)) = f(y,z,x). [para(401(a,1),788(a,1,3)),demod(13(3),835(5),8(3,R),9(3)),flip(a)]. 2154 f(x,f(x,y,z),f(u,v,w)) = f(x,y,f(x,z,f(u,v,w))). [para(14(a,1),35(a,1,2)),demod(9(3),419(7),9(3),28(4)),flip(a)]. 2230 f(x,y,f(x,z,f(u,v,f(y,z,w)))) = f(x,y,f(z,v,f(x,u,z))). [para(691(a,1),35(a,1,2)),demod(469(6),428(3),8(1),8(1),452(4),9(1),8(5),8(5),9(6),2154(7)),flip(a)]. 2393 f(x,f(y,z,u),f(v,w,f(z,u,f(x,y,z)))) = f(x,f(y,z,u),f(z,v,w)). [para(598(a,2),428(a,1,3,3))]. 3032 f(x,y,f(z,y,f(z,u,f(x,v,z)))) = f(x,z,y). [para(704(a,1),34(a,2)),demod(7(3),2154(7),1095(6),8(2),7(2),8(2),2154(3))]. 6431 f(x,f(y,z,f(x,u,v)),f(z,v,f(x,u,v))) = f(x,v,f(y,z,u)). [para(691(a,1),3032(a,1,3)),demod(8(4,R),9(4),428(8),8(6),8(6))]. 6568 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(568(a,1),62(a,1,3)),demod(8(1,R),9(1),8(4,R),9(4),48(4),8(4,R),9(4),13(5),8(2,R),9(2),2154(5),2230(5),8(2,R),9(2),8(3,R),9(3)),flip(a)]. 6576 f(x,f(y,z,f(u,v,w)),f(x,f(z,v6,f(u,v,w)),f(z,f(u,v,w),f(y,u,v6)))) = f(x,f(y,z,f(u,v,w)),f(z,v6,f(u,v,w))). [para(62(a,1),692(a,1,3,3))]. 6794 f(x,f(y,z,u),f(u,v,f(z,u,f(y,z,x)))) = f(x,f(z,u,v),f(y,z,u)). [para(575(a,1),6568(a,1,3,3)),demod(1095(5),8(5,R),9(5),8(8,R))]. 11571 f(x,f(y,z,u),f(z,u,f(y,x,v))) = f(z,u,f(y,x,v)). [para(1331(a,1),109(a,1,2)),demod(27(5),48(2)),flip(a)]. 12275 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)). [para(11(a,1),473(a,2,3)),demod(8(2),8(2),8(4),8(4),8(5,R),2154(5),509(5),8(5,R),9(5),758(5),48(4),1102(4),8(3,R),9(5),8(7,R),9(7),11571(7))]. 12418 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [back_demod(6794),demod(8(2),2393(5),12275(6),8(4,R),9(4))]. 12864 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(8(a,2),12275(a,1,2)),demod(8(2),9(2),8(4),8(4),8(5,R),9(5))]. 13094 f(x,f(y,z,f(u,v,w)),f(z,v6,f(u,v,w))) = f(z,f(u,v,w),f(x,y,v6)). [back_demod(6576),demod(12864(8),12418(7),692(4)),flip(a)]. 13388 f(x,f(y,z,u),f(y,v,u)) = f(y,u,f(v,x,z)). [back_demod(6431),demod(13094(5))]. 13548 $F # answer(dist_short). [back_demod(12),demod(13388(10),8(6),8(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=194. Generated=192799. Kept=13541. proofs=1. Usable=125. Sos=6565. Demods=4749. Denials=0. Limbo=160, Disabled=6697. Hints=0. Weight_deleted=963. Literals_deleted=0. Forward_subsumed=162727. Back_subsumed=298. Sos_limit_deleted=15567. Sos_displaced=0. Sos_removed=0. New_demodulators=10879 (2 lex), Back_demodulated=6393. Back_unit_deleted=0. Demod_attempts=3960491. Demod_rewrites=1436964. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=15.86. User_CPU=55.10, System_CPU=0.09, Wall_clock=55. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13955 exit (max_proofs) Mon Jun 19 17:19:24 2006