============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11537 was started by mccune on cleo.thornwood, Sat Aug 12 21:08:22 2006 The command was "/home/mccune/bin/prover9 -f lt.in H39-H3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in formulas(sos). x v y = y v x. (x v y) v z = x v (y v z). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. end_of_list. % Reading from file H39-H3.in formulas(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). end_of_list. formulas(goals). x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) # answer(H3). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) # answer(H3). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v y = y v x. [assumption]. (x v y) v z = x v (y v z). [assumption]. x ^ y = y ^ x. [assumption]. (x ^ y) ^ z = x ^ (y ^ z). [assumption]. x ^ (x v y) = x. [assumption]. x v (x ^ y) = x. [assumption]. x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). [assumption]. c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 9 x ^ (y v (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))). [copy(8),flip(a)]. 10 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [deny(1)]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. % (lex-dep) 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 x v y = y v x. [assumption]. given #2 (I,wt=11): 3 (x v y) v z = x v (y v z). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 11 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 13 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=21): 9 x ^ (y v (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))). [copy(8),flip(a)]. given #8 (I,wt=23): 10 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [deny(1)]. given #9 (T,wt=5): 23 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #10 (T,wt=5): 24 x v x = x. [para(6(a,1),7(a,1,2))]. given #11 (A,wt=11): 12 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #12 (F,wt=7): 15 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #13 (F,wt=7): 21 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #14 (T,wt=9): 38 x ^ (x ^ y) = x ^ y. [para(23(a,1),5(a,1,1)),flip(a)]. given #15 (T,wt=9): 40 x ^ (y ^ x) = y ^ x. [para(23(a,1),5(a,2,2)),rewrite(4(2))]. given #16 (A,wt=11): 14 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #17 (F,wt=9): 41 x v (x v y) = x v y. [para(24(a,1),3(a,1,1)),flip(a)]. given #18 (F,wt=9): 43 x v (y v x) = y v x. [para(24(a,1),3(a,2,2)),rewrite(2(2))]. given #19 (T,wt=9): 44 x ^ (y v (x v z)) = x. [para(12(a,1),6(a,1,2))]. given #20 (T,wt=9): 46 x ^ (y v (z v x)) = x. [para(3(a,1),15(a,1,2))]. given #21 (A,wt=13): 16 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #22 (F,wt=9): 52 x v (y ^ (z ^ x)) = x. [para(5(a,1),21(a,1,2))]. given #23 (F,wt=9): 59 x v (y ^ (x ^ z)) = x. [para(14(a,1),7(a,1,2))]. given #24 (T,wt=11): 17 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #25 (T,wt=11): 19 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #26 (A,wt=13): 18 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #27 (F,wt=11): 45 x v (y v (x ^ z)) = y v x. [para(7(a,1),12(a,1,2)),flip(a)]. given #28 (F,wt=11): 47 x ^ ((y v x) ^ z) = x ^ z. [para(15(a,1),5(a,1,1)),flip(a)]. given #29 (T,wt=11): 50 x v ((y ^ x) v z) = x v z. [para(21(a,1),3(a,1,1)),flip(a)]. given #30 (T,wt=11): 53 x v (y v (z ^ x)) = y v x. [para(21(a,1),12(a,1,2)),flip(a)]. given #31 (A,wt=13): 20 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #32 (F,wt=11): 58 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),14(a,1,2)),flip(a)]. given #33 (F,wt=11): 60 x ^ (y ^ (z v x)) = y ^ x. [para(15(a,1),14(a,1,2)),flip(a)]. given #34 (T,wt=11): 67 x ^ (y v (z v (x v u))) = x. [para(3(a,1),44(a,1,2))]. given #35 (T,wt=11): 71 x ^ (y v (z v (u v x))) = x. [para(3(a,1),46(a,1,2,2))]. given #36 (A,wt=13): 22 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #37 (F,wt=11): 83 (x v y) ^ (y v x) = x v y. [para(43(a,1),16(a,1,2))]. given #38 (F,wt=11): 86 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),52(a,1,2,2))]. given #39 (T,wt=11): 93 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),59(a,1,2))]. given #40 (T,wt=11): 97 (x v y) ^ (z ^ x) = z ^ x. [para(40(a,1),17(a,2)),rewrite(57(4))]. given #41 (A,wt=21): 25 x ^ (y v (z ^ ((x ^ z) v u))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),9(a,1,2,2,2))]. given #42 (F,wt=11): 104 (x ^ y) v (z v x) = z v x. [para(43(a,1),19(a,2)),rewrite(65(4))]. given #43 (F,wt=11): 121 (x v y) ^ (z ^ y) = z ^ y. [para(40(a,1),47(a,2)),rewrite(57(4))]. given #44 (T,wt=11): 132 (x ^ y) v (z v y) = z v y. [para(43(a,1),50(a,2)),rewrite(65(4))]. given #45 (T,wt=11): 196 (x ^ y) v (y ^ x) = x ^ y. [para(40(a,1),22(a,1,2))]. given #46 (A,wt=21): 26 x ^ ((y ^ (z v (x ^ y))) v u) = x ^ (u v (y ^ (x v z))). [para(2(a,1),9(a,1,2))]. given #47 (F,wt=25): 333 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ ((c1 ^ c2) v (c1 ^ c3)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [para(26(a,2),10(a,1,2,2)),rewrite(4(10),2(14))]. given #48 (F,wt=13): 48 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(15(a,1),5(a,1)),flip(a)]. given #49 (T,wt=13): 49 (x v y) ^ (x v (z v y)) = x v y. [para(12(a,1),15(a,1,2))]. given #50 (T,wt=13): 51 x v (y v (z ^ (x v y))) = x v y. [para(21(a,1),3(a,1)),flip(a)]. given #51 (A,wt=21): 27 x ^ (y v (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (u v x))). [para(2(a,1),9(a,2,2,2,2))]. given #52 (F,wt=13): 55 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(38(a,1),5(a,2,2)),rewrite(14(3),5(2))]. given #53 (F,wt=13): 57 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),40(a,1,2)),rewrite(5(5))]. given #54 (T,wt=13): 61 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(14(a,1),21(a,1,2))]. given #55 (T,wt=13): 63 x v (y v (x v z)) = y v (x v z). [para(41(a,1),3(a,2,2)),rewrite(12(3),3(2))]. given #56 (A,wt=43): 34 x ^ (y v ((z v (u ^ (v v (x ^ u)))) ^ (w v (x ^ (z v (u ^ (x v v))))))) = x ^ (y v ((z v (u ^ (v v (x ^ u)))) ^ (x v w))). [para(9(a,1),9(a,1,2,2,2,2))]. given #57 (F,wt=13): 65 x v (y v (z v x)) = y v (z v x). [para(3(a,1),43(a,1,2)),rewrite(3(5))]. given #58 (F,wt=13): 68 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(44(a,1),5(a,1,1)),flip(a)]. given #59 (T,wt=13): 70 x ^ (y ^ (z v (x v u))) = y ^ x. [para(44(a,1),14(a,1,2)),flip(a)]. given #60 (T,wt=13): 72 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(46(a,1),5(a,1,1)),flip(a)]. given #61 (A,wt=39): 35 x ^ (y v ((z v (u ^ (x v v))) ^ (w v (x ^ (z v (u ^ (v v x))))))) = x ^ (y v ((z v (u ^ (x v v))) ^ (x v w))). [para(9(a,2),9(a,1,2,2,2,2)),rewrite(27(8))]. given #62 (F,wt=13): 75 x ^ (y ^ (z v (u v x))) = y ^ x. [para(46(a,1),14(a,1,2)),flip(a)]. given #63 (F,wt=13): 76 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),16(a,1,1))]. given #64 (T,wt=13): 77 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),16(a,1,2)),rewrite(3(3))]. given #65 (T,wt=13): 84 x v ((y ^ (z ^ x)) v u) = x v u. [para(52(a,1),3(a,1,1)),flip(a)]. given #66 (A,wt=29): 37 x ^ (y v (z ^ ((u ^ (v v (z ^ u))) v x))) = x ^ (y v (z ^ (x v (u ^ (z v v))))). [para(9(a,1),9(a,2,2,2)),rewrite(27(8))]. given #67 (F,wt=13): 87 x v (y v (z ^ (u ^ x))) = y v x. [para(52(a,1),12(a,1,2)),flip(a)]. given #68 (F,wt=13): 90 x v ((y ^ (x ^ z)) v u) = x v u. [para(59(a,1),3(a,1,1)),flip(a)]. given #69 (T,wt=13): 94 x v (y v (z ^ (x ^ u))) = y v x. [para(59(a,1),12(a,1,2)),flip(a)]. given #70 (T,wt=13): 106 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),18(a,1,2,2,1))]. given #71 (A,wt=15): 66 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),44(a,1,2,2))]. given #72 (F,wt=13): 148 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),20(a,1,2,2,1))]. given #73 (F,wt=13): 177 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),67(a,1,2,2))]. given #74 (T,wt=13): 181 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),71(a,1,2,2,2))]. given #75 (T,wt=13): 193 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),22(a,1,1))]. given #76 (A,wt=15): 69 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(44(a,1),5(a,1)),flip(a)]. given #77 (F,wt=13): 194 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),22(a,1,2)),rewrite(5(3))]. given #78 (F,wt=13): 207 x v (y v (z ^ (y v x))) = x v y. [para(83(a,1),52(a,1,2,2)),rewrite(3(4))]. given #79 (T,wt=13): 210 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),86(a,1,2,2,2))]. given #80 (T,wt=13): 216 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(86(a,1),19(a,1,2)),rewrite(7(2)),flip(a)]. given #81 (A,wt=15): 73 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(46(a,1),5(a,1)),flip(a)]. given #82 (F,wt=13): 230 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(12(a,1),97(a,1,1))]. given #83 (F,wt=13): 237 (x v (y v z)) ^ (y v x) = y v x. [para(83(a,1),97(a,1,2)),rewrite(3(2),83(7))]. given #84 (T,wt=13): 267 (x ^ (y ^ z)) v (u v y) = u v y. [para(14(a,1),104(a,1,1))]. given #85 (T,wt=13): 275 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),121(a,1,1))]. given #86 (A,wt=15): 74 (x v y) ^ (z v (x v (u v y))) = x v y. [para(12(a,1),46(a,1,2,2))]. given #87 (F,wt=13): 290 (x v (y v z)) ^ (z v y) = z v y. [para(83(a,1),121(a,1,2)),rewrite(83(7))]. given #88 (F,wt=13): 294 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),132(a,1,1))]. given #89 (T,wt=13): 316 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(196(a,1),46(a,1,2,2)),rewrite(5(4))]. given #90 (T,wt=13): 317 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(196(a,1),19(a,2)),rewrite(5(3),312(6))]. given #91 (A,wt=19): 78 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),16(a,1,1)),rewrite(3(5),3(8))]. given #92 (F,wt=13): 319 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(196(a,1),132(a,1,2)),rewrite(196(7))]. given #93 (F,wt=13): 426 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),49(a,1,2)),rewrite(3(3))]. given #94 (T,wt=13): 507 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),61(a,1,2)),rewrite(5(3))]. given #95 (T,wt=13): 909 (x v (y v z)) ^ (z v x) = z v x. [para(77(a,1),4(a,1)),flip(a)]. given #96 (A,wt=17): 79 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(16(a,1),5(a,1,1)),flip(a)]. given #97 (F,wt=13): 1317 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(194(a,1),2(a,1)),flip(a)]. given #98 (F,wt=15): 81 (x v y) ^ (x v (z v (y v u))) = x v y. [para(12(a,1),16(a,1,2,2))]. given #99 (T,wt=15): 85 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(52(a,1),3(a,1)),flip(a)]. given #100 (T,wt=15): 88 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(14(a,1),52(a,1,2,2))]. given #101 (A,wt=19): 80 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(12(a,1),16(a,1,1)),rewrite(3(4))]. given #102 (F,wt=15): 91 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(59(a,1),3(a,1)),flip(a)]. given #103 (F,wt=15): 92 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),59(a,1,2,2))]. given #104 (T,wt=15): 96 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(17(a,1),21(a,1,2)),rewrite(2(4))]. given #105 (T,wt=15): 98 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(17(a,1),14(a,1,2)),flip(a)]. given #106 (A,wt=17): 82 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(16(a,1),14(a,1,2)),flip(a)]. given #107 (F,wt=15): 102 x v (y v ((x ^ z) v u)) = y v (x v u). [para(19(a,1),12(a,1,2)),flip(a)]. given #108 (F,wt=15): 103 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(19(a,1),15(a,1,2)),rewrite(4(4))]. given #109 (T,wt=15): 112 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(18(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #110 (T,wt=13): 2399 x ^ (((x v y) ^ (x v z)) v u) = x. [para(112(a,1),17(a,1)),rewrite(6(2)),flip(a)]. given #111 (A,wt=17): 89 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(16(a,1),52(a,1,2,2)),rewrite(3(5),3(4))]. given #112 (F,wt=13): 2400 x ^ (((x v y) ^ (z v x)) v u) = x. [para(112(a,1),47(a,1)),rewrite(15(2)),flip(a)]. given #113 (F,wt=13): 2453 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),2399(a,1,2,1,1))]. given #114 (T,wt=13): 2454 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),2399(a,1,2))]. given #115 (T,wt=13): 2553 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),2400(a,1,2,1,1))]. given #116 (A,wt=17): 95 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(17(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #117 (F,wt=13): 2554 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),2400(a,1,2))]. given #118 (F,wt=13): 2620 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),2453(a,1,2))]. given #119 (T,wt=13): 2700 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),2553(a,1,2))]. given #120 (T,wt=15): 114 x v (y v (z v (x ^ u))) = y v (z v x). [para(3(a,1),45(a,1,2)),rewrite(3(6))]. given #121 (A,wt=17): 99 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(17(a,1),52(a,1,2,2))]. given #122 (F,wt=15): 116 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(45(a,1),15(a,1,2)),rewrite(4(4))]. given #123 (F,wt=15): 120 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(47(a,1),21(a,1,2)),rewrite(2(4))]. given #124 (T,wt=15): 122 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(47(a,1),14(a,1,2)),flip(a)]. given #125 (T,wt=15): 126 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(18(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #126 (A,wt=17): 100 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(19(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #127 (F,wt=15): 129 x v (y v ((z ^ x) v u)) = y v (x v u). [para(50(a,1),12(a,1,2)),flip(a)]. given #128 (F,wt=15): 130 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(50(a,1),15(a,1,2)),rewrite(4(4))]. given #129 (T,wt=13): 3601 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(317(a,1),130(a,1,2)),rewrite(4(5),5(5),2340(4),317(8))]. given #130 (T,wt=13): 3633 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(2(a,1),3601(a,1,2))]. given #131 (A,wt=17): 101 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),19(a,1,2,1))]. given #132 (F,wt=13): 3634 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(4(a,1),3601(a,1,2,1))]. given #133 (F,wt=13): 3635 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(4(a,1),3601(a,1,2,2))]. given #134 (T,wt=13): 3720 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(4(a,1),3633(a,1,2,1))]. given #135 (T,wt=13): 3721 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(4(a,1),3633(a,1,2,2))]. given #136 (A,wt=17): 105 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(19(a,1),46(a,1,2,2))]. given #137 (F,wt=13): 3850 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(4(a,1),3634(a,1,2,2))]. given #138 (F,wt=13): 4019 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(4(a,1),3720(a,1,2,2))]. given #139 (T,wt=15): 139 x v (y v (z v (u ^ x))) = y v (z v x). [para(3(a,1),53(a,1,2)),rewrite(3(6))]. given #140 (T,wt=15): 140 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(53(a,1),15(a,1,2)),rewrite(4(4))]. given #141 (A,wt=19): 107 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(18(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #142 (F,wt=15): 154 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(20(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #143 (F,wt=13): 4541 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(154(a,1),19(a,1)),rewrite(7(2)),flip(a)]. given #144 (T,wt=13): 4543 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(154(a,1),50(a,1)),rewrite(21(2)),flip(a)]. given #145 (T,wt=13): 4610 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),4541(a,1,2,1,1))]. given #146 (A,wt=19): 108 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(18(a,1),21(a,1,2)),rewrite(2(5))]. given #147 (F,wt=13): 4611 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),4541(a,1,2))]. given #148 (F,wt=13): 4670 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),4543(a,1,2,1,1))]. given #149 (T,wt=13): 4671 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),4543(a,1,2))]. given #150 (T,wt=13): 4782 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(4(a,1),4610(a,1,2))]. given #151 (A,wt=17): 109 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(18(a,1),14(a,1,2)),flip(a)]. given #152 (F,wt=13): 4983 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),4670(a,1,2))]. given #153 (F,wt=15): 156 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(20(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #154 (T,wt=15): 158 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(5(a,1),58(a,1,2)),rewrite(5(6))]. given #155 (T,wt=15): 159 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(58(a,1),21(a,1,2)),rewrite(2(4))]. given #156 (A,wt=19): 110 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(14(a,1),18(a,1,2,2,1)),rewrite(5(5))]. given #157 (F,wt=15): 164 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(5(a,1),60(a,1,2)),rewrite(5(6))]. given #158 (F,wt=15): 166 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(60(a,1),21(a,1,2)),rewrite(2(4))]. given #159 (T,wt=13): 5888 x v ((y v x) ^ (y v z)) = x v y. [para(76(a,1),166(a,1,2)),rewrite(12(5),2(4),2170(4),76(8))]. given #160 (T,wt=13): 5968 x v ((x v y) ^ (y v z)) = x v y. [para(2(a,1),5888(a,1,2,1))]. given #161 (A,wt=21): 111 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(18(a,1),52(a,1,2,2))]. given #162 (F,wt=13): 5969 x v ((y v x) ^ (z v y)) = x v y. [para(2(a,1),5888(a,1,2,2))]. given #163 (F,wt=13): 5973 x v ((y v z) ^ (y v x)) = x v y. [para(4(a,1),5888(a,1,2))]. given #164 (T,wt=13): 6060 x v ((x v y) ^ (z v y)) = x v y. [para(2(a,1),5968(a,1,2,2))]. given #165 (T,wt=13): 6064 x v ((y v z) ^ (x v y)) = x v y. [para(4(a,1),5968(a,1,2))]. given #166 (A,wt=17): 113 x v (y v (z v ((x v y) ^ u))) = z v (x v y). [para(45(a,1),3(a,1)),flip(a)]. given #167 (F,wt=13): 6198 x v ((y v z) ^ (z v x)) = x v z. [para(4(a,1),5969(a,1,2))]. given #168 (F,wt=13): 6406 x v ((y v z) ^ (x v z)) = x v z. [para(4(a,1),6060(a,1,2))]. given #169 (T,wt=15): 169 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [para(18(a,1),60(a,2)),rewrite(25(8),14(8),5(7),95(8))]. given #170 (T,wt=15): 178 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(67(a,1),5(a,1,1)),flip(a)]. given #171 (A,wt=17): 115 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(5(a,1),45(a,1,2,2))]. given #172 (F,wt=15): 180 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(67(a,1),14(a,1,2)),flip(a)]. given #173 (F,wt=15): 182 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(71(a,1),5(a,1,1)),flip(a)]. given #174 (T,wt=15): 186 x ^ (y ^ (z v (u v (v v x)))) = y ^ x. [para(71(a,1),14(a,1,2)),flip(a)]. given #175 (T,wt=15): 198 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(14(a,1),22(a,1,2,2))]. given #176 (A,wt=17): 117 (x v (y ^ z)) ^ (u v (x v y)) = x v (y ^ z). [para(45(a,1),46(a,1,2,2))]. given #177 (F,wt=15): 203 (x v y) ^ ((y v x) ^ z) = (x v y) ^ z. [para(83(a,1),5(a,1,1)),flip(a)]. given #178 (F,wt=15): 208 x v ((y ^ (z ^ (u ^ x))) v v) = x v v. [para(86(a,1),3(a,1,1)),flip(a)]. given #179 (T,wt=15): 211 x v (y v (z ^ (u ^ (v ^ x)))) = y v x. [para(86(a,1),12(a,1,2)),flip(a)]. given #180 (T,wt=15): 222 x v (y v (z ^ (u ^ (y v x)))) = x v y. [para(83(a,1),86(a,1,2,2,2)),rewrite(3(5))]. given #181 (A,wt=17): 118 x ^ (y ^ ((z v (x ^ y)) ^ u)) = x ^ (y ^ u). [para(47(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #182 (F,wt=15): 223 x v ((y ^ (z ^ (x ^ u))) v v) = x v v. [para(93(a,1),3(a,1,1)),flip(a)]. given #183 (F,wt=15): 226 x v (y v (z ^ (u ^ (x ^ v)))) = y v x. [para(93(a,1),12(a,1,2)),flip(a)]. given #184 (T,wt=15): 228 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(97(a,1),5(a,1,1)),rewrite(5(2),5(5)),flip(a)]. given #185 (T,wt=15): 229 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(5(a,1),97(a,1,2)),rewrite(5(6))]. given #186 (A,wt=17): 119 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u. [para(12(a,1),47(a,1,2,1))]. given #187 (F,wt=15): 233 x ^ (y ^ ((x ^ (y v z)) v u)) = x ^ y. [para(58(a,1),97(a,1,2)),rewrite(4(5),5(5),58(8))]. given #188 (F,wt=15): 234 x ^ (y ^ ((x ^ (z v y)) v u)) = x ^ y. [para(60(a,1),97(a,1,2)),rewrite(4(5),5(5),60(8))]. given #189 (T,wt=15): 236 ((x v y) ^ z) v (z ^ x) = (x v y) ^ z. [para(97(a,1),22(a,1,2))]. given #190 (T,wt=15): 263 (x ^ y) v (z v (x v u)) = z v (x v u). [para(104(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. given #191 (A,wt=17): 123 ((x v y) ^ z) v (u ^ (y ^ z)) = (x v y) ^ z. [para(47(a,1),52(a,1,2,2))]. given #192 (F,wt=15): 264 (x ^ y) v (z v (u v x)) = z v (u v x). [para(3(a,1),104(a,1,2)),rewrite(3(6))]. given #193 (F,wt=15): 269 ((x ^ y) v z) ^ (z v x) = (x ^ y) v z. [para(104(a,1),16(a,1,2))]. given #194 (T,wt=15): 270 x v (y v ((x v (y ^ z)) ^ u)) = x v y. [para(45(a,1),104(a,1,2)),rewrite(2(5),3(5),45(8))]. given #195 (T,wt=15): 271 x v (y v ((x v (z ^ y)) ^ u)) = x v y. [para(53(a,1),104(a,1,2)),rewrite(2(5),3(5),53(8))]. given #196 (A,wt=17): 124 x ^ (y ^ (z ^ (x ^ u))) = y ^ (z ^ (x ^ u)). [para(52(a,1),47(a,1,2,1)),rewrite(14(4),5(3),5(2),5(7),5(6))]. given #197 (F,wt=15): 273 (x v y) ^ (z ^ (y ^ u)) = z ^ (y ^ u). [para(104(a,1),97(a,1,1))]. given #198 (F,wt=15): 274 (x ^ y) v (z v (y v u)) = z v (y v u). [para(97(a,1),104(a,1,1))]. given #199 (T,wt=15): 276 (x v y) ^ (z ^ (u ^ y)) = z ^ (u ^ y). [para(5(a,1),121(a,1,2)),rewrite(5(6))]. given #200 (T,wt=15): 279 x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y. [para(17(a,1),121(a,1,2)),rewrite(4(5),5(5),17(8))]. given #201 (A,wt=19): 125 (x v y) ^ (((x ^ z) v y) ^ u) = ((x ^ z) v y) ^ u. [para(19(a,1),47(a,1,2,1)),rewrite(14(5))]. given #202 (F,wt=15): 281 x ^ (y ^ (z v (x ^ (y v u)))) = y ^ x. [para(18(a,1),121(a,1,2)),rewrite(4(6),5(6),248(6),18(9))]. given #203 (F,wt=15): 283 x ^ (y ^ (z v ((u v x) ^ y))) = x ^ y. [para(47(a,1),121(a,1,2)),rewrite(4(5),5(5),47(8))]. given #204 (T,wt=15): 287 x ^ (y ^ (z v (x ^ (u v y)))) = x ^ y. [para(60(a,1),121(a,1,2)),rewrite(4(5),5(5),60(8))]. given #205 (T,wt=15): 289 ((x v y) ^ z) v (z ^ y) = (x v y) ^ z. [para(121(a,1),22(a,1,2))]. given #206 (A,wt=19): 127 (x v y) ^ ((x v (y ^ z)) ^ u) = (x v (y ^ z)) ^ u. [para(45(a,1),47(a,1,2,1)),rewrite(14(5))]. given #207 (F,wt=15): 293 (x ^ y) v (z v (u v y)) = z v (u v y). [para(121(a,1),104(a,1,1))]. given #208 (F,wt=15): 298 ((x ^ y) v z) ^ (z v y) = (x ^ y) v z. [para(132(a,1),16(a,1,2))]. given #209 (T,wt=15): 300 x v (y v (z ^ ((x ^ u) v y))) = x v y. [para(19(a,1),132(a,1,2)),rewrite(2(5),3(5),19(8))]. given #210 (T,wt=15): 302 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(45(a,1),132(a,1,2)),rewrite(2(5),3(5),45(8))]. given #211 (A,wt=17): 128 x v (y v ((z ^ (x v y)) v u)) = x v (y v u). [para(50(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #212 (F,wt=15): 304 x v (y v (z ^ ((u ^ x) v y))) = x v y. [para(50(a,1),132(a,1,2)),rewrite(2(5),3(5),50(8))]. given #213 (F,wt=15): 305 x v (y v (z ^ (x v (u ^ y)))) = x v y. [para(53(a,1),132(a,1,2)),rewrite(2(5),3(5),53(8))]. given #214 (T,wt=15): 311 (x ^ y) v ((y ^ x) v z) = (x ^ y) v z. [para(196(a,1),3(a,1,1)),flip(a)]. given #215 (T,wt=15): 312 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(196(a,1),3(a,2,2)),rewrite(2(4))]. given #216 (A,wt=17): 131 (x ^ y) v ((x ^ (z ^ y)) v u) = (x ^ y) v u. [para(14(a,1),50(a,1,2,1))]. given #217 (F,wt=15): 318 x ^ (y ^ (z v (u v (y ^ x)))) = x ^ y. [para(196(a,1),71(a,1,2,2,2)),rewrite(5(5))]. given #218 (F,wt=15): 417 x ^ (y ^ (z v (y ^ (u v x)))) = x ^ y. [para(48(a,1),60(a,2)),rewrite(27(8),14(8),5(7),118(8))]. given #219 (T,wt=15): 428 (x v y) ^ (x v (z v (u v y))) = x v y. [para(3(a,1),49(a,1,2,2))]. given #220 (T,wt=15): 499 (x v (y v (z v u))) ^ (v ^ z) = v ^ z. [para(67(a,1),57(a,1,2,2)),rewrite(67(9))]. given #221 (A,wt=17): 133 ((x ^ y) v z) ^ (u v (y v z)) = (x ^ y) v z. [para(50(a,1),46(a,1,2,2))]. given #222 (F,wt=15): 500 (x v (y v (z v u))) ^ (v ^ u) = v ^ u. [para(71(a,1),57(a,1,2,2)),rewrite(71(9))]. given #223 (F,wt=15): 501 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(57(a,1),22(a,1,2,2))]. given #224 (T,wt=15): 502 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(83(a,1),57(a,1,2,2)),rewrite(83(7))]. given #225 (T,wt=15): 681 (x ^ (y ^ (z ^ u))) v (v v u) = v v u. [para(86(a,1),65(a,1,2,2)),rewrite(86(9))]. given #226 (A,wt=17): 134 x v (y v (z v (x v u))) = y v (z v (x v u)). [para(46(a,1),50(a,1,2,1)),rewrite(12(4),3(3),3(2),3(7),3(6))]. given #227 (F,wt=15): 682 (x ^ (y ^ (z ^ u))) v (v v z) = v v z. [para(93(a,1),65(a,1,2,2)),rewrite(93(9))]. given #228 (F,wt=15): 692 x ^ (y v (z v (u v (v v (x v w))))) = x. [para(71(a,1),68(a,1,2)),rewrite(44(3)),flip(a)]. given #229 (T,wt=15): 693 (x v (y v (z v u))) ^ (z v y) = y v z. [para(83(a,1),68(a,2)),rewrite(3(3),502(7))]. given #230 (T,wt=15): 735 x ^ (y v (z v (u v (v v (w v x))))) = x. [para(71(a,1),72(a,1,2)),rewrite(46(3)),flip(a)]. given #231 (A,wt=19): 135 (x ^ y) v (((x v z) ^ y) v u) = ((x v z) ^ y) v u. [para(17(a,1),50(a,1,2,1)),rewrite(12(5))]. given #232 (F,wt=15): 900 (x v y) ^ (y v (z v (x v u))) = y v x. [para(12(a,1),76(a,1,2,2))]. given #233 (F,wt=15): 905 (x v y) ^ (y v (z v (u v x))) = y v x. [para(65(a,1),76(a,1,2,2))]. given #234 (T,wt=15): 926 (x v (y v (z v u))) ^ (z v x) = z v x. [para(77(a,1),97(a,1,2)),rewrite(3(3),3(2),77(9))]. given #235 (T,wt=15): 927 (x v (y v (z v u))) ^ (u v y) = u v y. [para(77(a,1),121(a,1,2)),rewrite(77(9))]. given #236 (A,wt=23): 136 (x ^ y) v ((y ^ ((x ^ y) v z)) v u) = (y ^ ((x ^ y) v z)) v u. [para(18(a,1),50(a,1,2,1)),rewrite(12(6))]. given #237 (F,wt=15): 953 x v (y ^ (z ^ (u ^ (v ^ (w ^ x))))) = x. [para(86(a,1),84(a,1,2)),rewrite(52(3)),flip(a)]. given #238 (F,wt=15): 954 x v (y ^ (z ^ (u ^ (v ^ (x ^ w))))) = x. [para(93(a,1),84(a,1,2)),rewrite(52(3),5(3),5(2)),flip(a)]. given #239 (T,wt=15): 1141 (x ^ (y ^ (z ^ u))) v (z ^ y) = y ^ z. [para(196(a,1),90(a,2)),rewrite(5(3),312(7))]. given #240 (T,wt=15): 1174 x ^ (y ^ (z v ((y ^ x) v u))) = x ^ y. [para(12(a,1),106(a,1,2,2))]. given #241 (A,wt=19): 137 (x v y) ^ (((z ^ x) v y) ^ u) = ((z ^ x) v y) ^ u. [para(50(a,1),47(a,1,2,1)),rewrite(14(5))]. given #242 (F,wt=15): 1179 x ^ (y ^ ((y ^ (x v z)) v u)) = x ^ y. [para(106(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #243 (F,wt=15): 1180 x ^ (y ^ ((y ^ (z v x)) v u)) = x ^ y. [para(106(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #244 (T,wt=15): 1200 (x v y) ^ (z v (y v (x v u))) = y v x. [para(2(a,1),66(a,1,1))]. given #245 (T,wt=15): 1201 (x v y) ^ (z v (y v (u v x))) = x v y. [para(2(a,1),66(a,1,2,2)),rewrite(3(3))]. given #246 (A,wt=19): 138 (x ^ y) v (((z v x) ^ y) v u) = ((z v x) ^ y) v u. [para(47(a,1),50(a,1,2,1)),rewrite(12(5))]. given #247 (F,wt=15): 1222 x v (y v (z ^ ((y v x) ^ u))) = x v y. [para(14(a,1),148(a,1,2,2))]. given #248 (F,wt=15): 1224 x v (y v ((y v (x ^ z)) ^ u)) = x v y. [para(148(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #249 (T,wt=15): 1226 x v (y v ((y v (z ^ x)) ^ u)) = x v y. [para(148(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #250 (T,wt=15): 1278 (x ^ y) v (y ^ (z ^ (x ^ u))) = y ^ x. [para(14(a,1),193(a,1,2,2))]. given #251 (A,wt=17): 141 (x ^ y) v (z v (x ^ (u ^ y))) = z v (x ^ y). [para(14(a,1),53(a,1,2,2))]. given #252 (F,wt=15): 1282 (x ^ y) v (y ^ (z ^ (u ^ x))) = y ^ x. [para(57(a,1),193(a,1,2,2))]. given #253 (F,wt=15): 1338 (x ^ (y ^ (z ^ u))) v (z ^ x) = z ^ x. [para(194(a,1),104(a,1,2)),rewrite(5(3),5(2),194(9))]. low water: id=5680, wt=51 low water: id=5599, wt=49 low water: id=5600, wt=47 low water: id=5760, wt=45 given #254 (T,wt=15): 1339 (x ^ (y ^ (z ^ u))) v (u ^ y) = u ^ y. [para(194(a,1),132(a,1,2)),rewrite(194(9))]. low water: id=5791, wt=43 low water: id=6187, wt=41 low water: id=6191, wt=39 low water: id=6192, wt=37 given #255 (T,wt=15): 1378 x v (y v (z ^ (y v (x ^ u)))) = x v y. [para(207(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. low water: id=6608, wt=35 given #256 (A,wt=17): 142 (x v (y ^ z)) ^ (u v (x v z)) = x v (y ^ z). [para(53(a,1),46(a,1,2,2))]. given #257 (F,wt=15): 1380 x v (y v (z ^ (y v (u ^ x)))) = x v y. [para(207(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. low water: id=6940, wt=33 given #258 (F,wt=15): 1510 (x v (y v (z v u))) ^ (u v x) = u v x. [para(65(a,1),237(a,1,1,2))]. given #259 (T,wt=15): 1555 (x v (y v (z v u))) ^ (u v z) = u v z. [para(83(a,1),275(a,1,2)),rewrite(83(8))]. given #260 (T,wt=15): 1586 (x v y) ^ (z v (u v (y v x))) = x v y. [para(2(a,1),74(a,1,2,2)),rewrite(3(3))]. given #261 (A,wt=23): 145 (x ^ ((y ^ x) v z)) v (u v (y ^ x)) = u v (x ^ ((y ^ x) v z)). [para(18(a,1),53(a,1,2,2))]. given #262 (F,wt=15): 1625 (x v y) ^ (y v (x ^ z)) = y v (x ^ z). [para(19(a,1),290(a,1,1))]. low water: id=7490, wt=31 given #263 (F,wt=15): 1626 (x v y) ^ ((y ^ z) v x) = (y ^ z) v x. [para(45(a,1),290(a,1,1))]. given #264 (T,wt=15): 1627 (x v y) ^ (y v (z ^ x)) = y v (z ^ x). [para(50(a,1),290(a,1,1))]. given #265 (T,wt=15): 1628 (x v y) ^ ((z ^ y) v x) = (z ^ y) v x. [para(53(a,1),290(a,1,1))]. given #266 (A,wt=19): 146 (x v y) ^ ((x v (z ^ y)) ^ u) = (x v (z ^ y)) ^ u. [para(53(a,1),47(a,1,2,1)),rewrite(14(5))]. given #267 (F,wt=15): 1656 (x ^ (y ^ (z ^ u))) v (u ^ z) = u ^ z. [para(196(a,1),294(a,1,2)),rewrite(196(8))]. low water: id=7906, wt=29 given #268 (F,wt=15): 1728 (x ^ (y ^ (z ^ u))) v (u ^ x) = x ^ u. [para(57(a,1),317(a,1,1,2))]. given #269 (T,wt=15): 1774 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(17(a,1),319(a,1,1))]. given #270 (T,wt=15): 1775 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [para(47(a,1),319(a,1,1))]. given #271 (A,wt=19): 149 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(20(a,1),3(a,1)),rewrite(3(2),3(4)),flip(a)]. given #272 (F,wt=15): 1776 (x ^ y) v ((y v z) ^ x) = (y v z) ^ x. [para(58(a,1),319(a,1,1))]. given #273 (F,wt=15): 1777 (x ^ y) v ((z v y) ^ x) = (z v y) ^ x. [para(60(a,1),319(a,1,1))]. given #274 (T,wt=15): 1804 (x v (y ^ z)) ^ (y v x) = x v (y ^ z). [para(19(a,1),426(a,1,2))]. given #275 (T,wt=15): 1805 (x v (y ^ z)) ^ (z v x) = x v (y ^ z). [para(50(a,1),426(a,1,2))]. given #276 (A,wt=17): 150 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(20(a,1),12(a,1,2)),flip(a)]. given #277 (F,wt=15): 1813 (x ^ y) v (z ^ (u ^ (y ^ x))) = x ^ y. [para(5(a,1),507(a,1,2))]. given #278 (F,wt=15): 1815 (x ^ (y v z)) v (y ^ x) = x ^ (y v z). [para(17(a,1),507(a,1,2))]. given #279 (T,wt=15): 1816 (x ^ y) v (z ^ (y ^ (x ^ u))) = x ^ y. [para(507(a,1),45(a,2)),rewrite(5(6),5(5),1768(8))]. given #280 (T,wt=15): 1817 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(47(a,1),507(a,1,2))]. low water: id=8585, wt=27 given #281 (A,wt=19): 151 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(12(a,1),20(a,1,2,2,1)),rewrite(3(5))]. given #282 (F,wt=15): 2010 (x ^ y) v (z ^ (y ^ (u ^ x))) = y ^ x. [para(4(a,1),88(a,1,1))]. given #283 (F,wt=15): 2260 x ^ (y ^ (((y v z) ^ x) v u)) = x ^ y. [para(106(a,1),98(a,1,2)),rewrite(58(3)),flip(a)]. given #284 (T,wt=15): 2267 x ^ (y ^ (z v ((y v u) ^ x))) = x ^ y. [para(316(a,1),98(a,1,2)),rewrite(58(3)),flip(a)]. given #285 (T,wt=15): 2329 x v (y v (((y ^ z) v x) ^ u)) = x v y. [para(148(a,1),102(a,1,2)),rewrite(45(3)),flip(a)]. given #286 (A,wt=19): 152 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(20(a,1),15(a,1,2)),rewrite(4(5))]. given #287 (F,wt=15): 2331 x v (y v (z ^ ((y ^ u) v x))) = x v y. [para(207(a,1),102(a,1,2)),rewrite(45(3)),flip(a)]. given #288 (F,wt=15): 2419 x ^ (((x v y) ^ (z v (x v u))) v v) = x. [para(112(a,1),68(a,1)),rewrite(44(3)),flip(a)]. given #289 (T,wt=15): 2421 x ^ (((x v y) ^ (z v (u v x))) v v) = x. [para(112(a,1),72(a,1)),rewrite(46(3)),flip(a)]. given #290 (T,wt=15): 2457 x ^ (((y v (x v z)) ^ (x v u)) v v) = x. [para(12(a,1),2399(a,1,2,1,1))]. given #291 (A,wt=21): 153 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(20(a,1),46(a,1,2,2))]. given #292 (F,wt=15): 2458 x ^ (y v (((x v z) ^ (x v u)) v v)) = x. [para(12(a,1),2399(a,1,2))]. given #293 (F,wt=15): 2473 x ^ (((y v (z v x)) ^ (x v u)) v v) = x. [para(65(a,1),2399(a,1,2,1,1))]. given #294 (T,wt=15): 2474 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(65(a,1),2399(a,1,2))]. given #295 (T,wt=15): 2559 x ^ (((y v (x v z)) ^ (u v x)) v v) = x. [para(12(a,1),2400(a,1,2,1,1))]. given #296 (A,wt=23): 155 (x v y) ^ ((y v ((x v y) ^ z)) ^ u) = (y v ((x v y) ^ z)) ^ u. [para(20(a,1),47(a,1,2,1)),rewrite(14(6))]. given #297 (F,wt=15): 2561 x ^ (y v (((x v z) ^ (u v x)) v v)) = x. [para(12(a,1),2400(a,1,2))]. given #298 (F,wt=15): 2585 x ^ (((y v (z v x)) ^ (u v x)) v v) = x. [para(65(a,1),2400(a,1,2,1,1))]. given #299 (T,wt=15): 2586 x ^ (y v (z v ((x v u) ^ (v v x)))) = x. [para(65(a,1),2400(a,1,2))]. given #300 (T,wt=15): 2625 x ^ (((y v x) ^ (z v (x v u))) v v) = x. [para(12(a,1),2453(a,1,2,1,2))]. given #301 (A,wt=17): 157 x ^ (y ^ (z ^ ((x ^ y) v u))) = z ^ (x ^ y). [para(58(a,1),5(a,1)),flip(a)]. given #302 (F,wt=15): 2626 x ^ (y v (((z v x) ^ (x v u)) v v)) = x. [para(12(a,1),2453(a,1,2))]. given #303 (F,wt=15): 2639 x ^ (((y v x) ^ (z v (u v x))) v v) = x. [para(65(a,1),2453(a,1,2,1,2))]. given #304 (T,wt=15): 2640 x ^ (y v (z v ((u v x) ^ (x v v)))) = x. [para(65(a,1),2453(a,1,2))]. given #305 (T,wt=15): 2662 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(12(a,1),2454(a,1,2,2,1))]. given #306 (A,wt=17): 160 (x ^ (y v z)) v (u ^ (x ^ y)) = x ^ (y v z). [para(58(a,1),52(a,1,2,2))]. given #307 (F,wt=15): 2663 x ^ (y v ((x v z) ^ (u v (x v v)))) = x. [para(12(a,1),2454(a,1,2,2,2))]. given #308 (F,wt=15): 2676 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(65(a,1),2454(a,1,2,2,1))]. given #309 (T,wt=15): 2677 x ^ (y v ((x v z) ^ (u v (v v x)))) = x. [para(65(a,1),2454(a,1,2,2,2))]. low water: id=9478, wt=25 given #310 (T,wt=15): 2706 x ^ (y v (((z v x) ^ (u v x)) v v)) = x. [para(12(a,1),2553(a,1,2))]. given #311 (A,wt=19): 161 (x ^ y) v ((x ^ (y v z)) v u) = (x ^ (y v z)) v u. [para(58(a,1),50(a,1,2,1)),rewrite(12(5))]. given #312 (F,wt=15): 2729 x ^ (y v (z v ((u v x) ^ (v v x)))) = x. [para(65(a,1),2553(a,1,2))]. given #313 (F,wt=15): 2842 x ^ (y v ((z v (x v u)) ^ (v v x))) = x. [para(12(a,1),2554(a,1,2,2,1))]. given #314 (T,wt=15): 2865 x ^ (y v ((z v (u v x)) ^ (v v x))) = x. [para(65(a,1),2554(a,1,2,2,1))]. given #315 (T,wt=15): 2902 x ^ (y v ((z v x) ^ (u v (x v v)))) = x. [para(12(a,1),2620(a,1,2,2,2))]. given #316 (A,wt=17): 163 x ^ (y ^ (z ^ (u v (x ^ y)))) = z ^ (x ^ y). [para(60(a,1),5(a,1)),flip(a)]. given #317 (F,wt=15): 2913 x ^ (y v ((z v x) ^ (u v (v v x)))) = x. [para(65(a,1),2620(a,1,2,2,2))]. given #318 (F,wt=15): 3300 x ^ (y ^ (((z v y) ^ x) v u)) = x ^ y. [para(106(a,1),122(a,1,2)),rewrite(60(3)),flip(a)]. given #319 (T,wt=15): 3308 x ^ (y ^ (z v ((u v y) ^ x))) = x ^ y. [para(316(a,1),122(a,1,2)),rewrite(60(3)),flip(a)]. given #320 (T,wt=15): 3509 x v (y v (((z ^ y) v x) ^ u)) = x v y. [para(148(a,1),129(a,1,2)),rewrite(53(3)),flip(a)]. given #321 (A,wt=17): 165 (x v y) ^ (z ^ (x v (u v y))) = z ^ (x v y). [para(12(a,1),60(a,1,2,2))]. given #322 (F,wt=15): 3512 x v (y v (z ^ ((u ^ y) v x))) = x v y. [para(207(a,1),129(a,1,2)),rewrite(53(3)),flip(a)]. given #323 (F,wt=15): 3640 x ^ ((y ^ (z ^ u)) v (z ^ x)) = x ^ z. [para(14(a,1),3601(a,1,2,1))]. given #324 (T,wt=15): 3642 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(3601(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #325 (T,wt=15): 3645 x ^ ((y ^ z) v (y ^ (u v x))) = x ^ y. [para(3601(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #326 (A,wt=17): 167 (x ^ (y v z)) v (u ^ (x ^ z)) = x ^ (y v z). [para(60(a,1),52(a,1,2,2))]. given #327 (F,wt=15): 3663 x ^ ((y ^ (z ^ u)) v (u ^ x)) = x ^ u. [para(57(a,1),3601(a,1,2,1))]. given #328 (F,wt=15): 3727 x ^ ((y ^ x) v (z ^ (y ^ u))) = x ^ y. [para(14(a,1),3633(a,1,2,2))]. given #329 (T,wt=15): 3728 x ^ ((y ^ (x v z)) v (y ^ u)) = x ^ y. [para(3633(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #330 (T,wt=15): 3729 x ^ ((y ^ (z v x)) v (y ^ u)) = x ^ y. [para(3633(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #331 (A,wt=19): 171 (x ^ y) v ((x ^ (z v y)) v u) = (x ^ (z v y)) v u. [para(60(a,1),50(a,1,2,1)),rewrite(12(5))]. given #332 (F,wt=15): 3741 x ^ ((y ^ x) v (z ^ (u ^ y))) = x ^ y. [para(57(a,1),3633(a,1,2,2))]. given #333 (F,wt=15): 3854 x ^ (y v ((y v z) ^ x)) = x ^ (y v z). [para(6(a,1),3634(a,1,2,1))]. given #334 (T,wt=15): 3855 x ^ (y v ((z v y) ^ x)) = x ^ (z v y). [para(15(a,1),3634(a,1,2,1))]. given #335 (T,wt=15): 3862 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(3634(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #336 (A,wt=23): 175 (x v ((y v x) ^ z)) ^ (u ^ (y v x)) = u ^ (x v ((y v x) ^ z)). [para(20(a,1),60(a,1,2,2))]. given #337 (F,wt=15): 3867 x ^ ((y ^ z) v (z ^ (u v x))) = x ^ z. [para(3634(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #338 (F,wt=15): 3981 x ^ ((y ^ (z ^ u)) v (x ^ z)) = x ^ z. [para(14(a,1),3635(a,1,2,1))]. given #339 (T,wt=15): 3983 x ^ ((y ^ z) v ((x v u) ^ y)) = x ^ y. [para(3635(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #340 (T,wt=15): 3984 x ^ ((y ^ z) v ((u v x) ^ y)) = x ^ y. [para(3635(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #341 (A,wt=17): 176 (x v y) ^ (z v (u v (x v (y v v)))) = x v y. [para(3(a,1),67(a,1,2,2,2))]. given #342 (F,wt=15): 3992 x ^ ((y ^ (z ^ u)) v (x ^ u)) = x ^ u. [para(57(a,1),3635(a,1,2,1))]. given #343 (F,wt=15): 4025 x ^ ((x ^ y) v (z ^ (y ^ u))) = x ^ y. [para(14(a,1),3720(a,1,2,2))]. given #344 (T,wt=15): 4026 x ^ (((x v y) ^ z) v (z ^ u)) = x ^ z. [para(3720(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #345 (T,wt=15): 4027 x ^ (((y v x) ^ z) v (z ^ u)) = x ^ z. [para(3720(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #346 (A,wt=17): 179 x ^ (y ^ (z v (u v ((x ^ y) v v)))) = x ^ y. [para(67(a,1),5(a,1)),flip(a)]. given #347 (F,wt=15): 4035 x ^ ((x ^ y) v (z ^ (u ^ y))) = x ^ y. [para(57(a,1),3720(a,1,2,2))]. given #348 (F,wt=15): 4065 x ^ ((y ^ (x v z)) v (u ^ y)) = x ^ y. [para(3721(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #349 (T,wt=15): 4066 x ^ ((y ^ (z v x)) v (u ^ y)) = x ^ y. [para(3721(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #350 (T,wt=15): 4204 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(6(a,1),3850(a,1,2,1))]. given #351 (A,wt=17): 183 x ^ (y ^ (z v (u v (v v (x ^ y))))) = x ^ y. [para(71(a,1),5(a,1)),flip(a)]. given #352 (F,wt=15): 4205 x ^ (y v (x ^ (z v y))) = x ^ (z v y). [para(15(a,1),3850(a,1,2,1))]. given #353 (F,wt=15): 4212 x ^ ((y ^ z) v ((x v u) ^ z)) = x ^ z. [para(3850(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #354 (T,wt=15): 4215 x ^ ((y ^ z) v ((u v x) ^ z)) = x ^ z. [para(3850(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #355 (T,wt=15): 4292 x ^ (((x v y) ^ z) v (u ^ z)) = x ^ z. [para(4019(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #356 (A,wt=17): 184 (x v y) ^ (z v (u v (x v (v v y)))) = x v y. [para(12(a,1),71(a,1,2,2,2))]. given #357 (F,wt=15): 4293 x ^ (((y v x) ^ z) v (u ^ z)) = x ^ z. [para(4019(a,1),47(a,1,2)),rewrite(47(3)),flip(a)]. given #358 (F,wt=15): 4560 x v (((x ^ y) v (z ^ (u ^ x))) ^ v) = x. [para(154(a,1),84(a,1)),rewrite(52(3)),flip(a)]. given #359 (T,wt=15): 4562 x v (((x ^ y) v (z ^ (x ^ u))) ^ v) = x. [para(154(a,1),90(a,1)),rewrite(59(3)),flip(a)]. given #360 (T,wt=15): 4614 x v (((y ^ (x ^ z)) v (x ^ u)) ^ v) = x. [para(14(a,1),4541(a,1,2,1,1))]. given #361 (A,wt=17): 185 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(71(a,1),21(a,1,2)),rewrite(2(4))]. given #362 (F,wt=15): 4615 x v (y ^ (((x ^ z) v (x ^ u)) ^ v)) = x. [para(14(a,1),4541(a,1,2))]. given #363 (F,wt=15): 4629 x v (((y ^ (z ^ x)) v (x ^ u)) ^ v) = x. [para(57(a,1),4541(a,1,2,1,1))]. given #364 (T,wt=15): 4630 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(57(a,1),4541(a,1,2))]. given #365 (T,wt=15): 4676 x v (((y ^ (x ^ z)) v (u ^ x)) ^ v) = x. [para(14(a,1),4543(a,1,2,1,1))]. given #366 (A,wt=19): 187 ((x ^ y) v z) ^ (u v (v v (x v z))) = (x ^ y) v z. [para(19(a,1),71(a,1,2,2,2))]. given #367 (F,wt=15): 4678 x v (y ^ (((x ^ z) v (u ^ x)) ^ v)) = x. [para(14(a,1),4543(a,1,2))]. given #368 (F,wt=15): 4706 x v (((y ^ (z ^ x)) v (u ^ x)) ^ v) = x. [para(57(a,1),4543(a,1,2,1,1))]. given #369 (T,wt=15): 4707 x v (y ^ (z ^ ((x ^ u) v (v ^ x)))) = x. [para(57(a,1),4543(a,1,2))]. given #370 (T,wt=15): 4787 x v (((y ^ x) v (z ^ (x ^ u))) ^ v) = x. [para(14(a,1),4610(a,1,2,1,2))]. given #371 (A,wt=19): 188 (x v (y ^ z)) ^ (u v (v v (x v y))) = x v (y ^ z). [para(45(a,1),71(a,1,2,2,2))]. given #372 (F,wt=15): 4788 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(14(a,1),4610(a,1,2))]. given #373 (F,wt=15): 4802 x v (((y ^ x) v (z ^ (u ^ x))) ^ v) = x. [para(57(a,1),4610(a,1,2,1,2))]. given #374 (T,wt=15): 4803 x v (y ^ (z ^ ((u ^ x) v (x ^ v)))) = x. [para(57(a,1),4610(a,1,2))]. given #375 (T,wt=15): 4882 x v (y ^ ((z ^ y) v x)) = x v (z ^ y). [para(108(a,1),207(a,1,2))]. given #376 (A,wt=21): 189 x v (y v (z v (u v (x v v)))) = y v (z v (u v (x v v))). [para(71(a,1),50(a,1,2,1)),rewrite(12(5),3(4),3(3),3(2),3(9),3(8),3(7))]. given #377 (F,wt=15): 4930 x v (y ^ ((z ^ (x ^ u)) v (x ^ v))) = x. [para(14(a,1),4611(a,1,2,2,1))]. given #378 (F,wt=15): 4931 x v (y ^ ((x ^ z) v (u ^ (x ^ v)))) = x. [para(14(a,1),4611(a,1,2,2,2))]. given #379 (T,wt=15): 4943 x v (y ^ ((z ^ (u ^ x)) v (x ^ v))) = x. [para(57(a,1),4611(a,1,2,2,1))]. given #380 (T,wt=15): 4944 x v (y ^ ((x ^ z) v (u ^ (v ^ x)))) = x. [para(57(a,1),4611(a,1,2,2,2))]. given #381 (A,wt=19): 190 ((x ^ y) v z) ^ (u v (v v (y v z))) = (x ^ y) v z. [para(50(a,1),71(a,1,2,2,2))]. given #382 (F,wt=15): 4989 x v (y ^ (((z ^ x) v (u ^ x)) ^ v)) = x. [para(14(a,1),4670(a,1,2))]. given #383 (F,wt=15): 5018 x v (y ^ (z ^ ((u ^ x) v (v ^ x)))) = x. [para(57(a,1),4670(a,1,2))]. given #384 (T,wt=15): 5091 x v (y ^ ((z ^ (x ^ u)) v (v ^ x))) = x. [para(14(a,1),4671(a,1,2,2,1))]. given #385 (T,wt=15): 5120 x v (y ^ ((z ^ (u ^ x)) v (v ^ x))) = x. [para(57(a,1),4671(a,1,2,2,1))]. given #386 (A,wt=19): 191 (x v (y ^ z)) ^ (u v (v v (x v z))) = x v (y ^ z). [para(53(a,1),71(a,1,2,2,2))]. given #387 (F,wt=15): 5196 x v (y ^ ((z ^ x) v (u ^ (x ^ v)))) = x. [para(14(a,1),4782(a,1,2,2,2))]. given #388 (F,wt=15): 5211 x v (y ^ ((z ^ x) v (u ^ (v ^ x)))) = x. [para(57(a,1),4782(a,1,2,2,2))]. given #389 (T,wt=15): 5976 x v ((y v x) ^ (z v (y v u))) = x v y. [para(12(a,1),5888(a,1,2,2))]. given #390 (T,wt=15): 5977 x v ((y v (x ^ z)) ^ (y v u)) = x v y. [para(5888(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #391 (A,wt=23): 192 (x v ((y v x) ^ z)) ^ (u v (v v (y v x))) = x v ((y v x) ^ z). [para(20(a,1),71(a,1,2,2,2))]. given #392 (F,wt=15): 5980 x v ((y v (z ^ x)) ^ (y v u)) = x v y. [para(5888(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #393 (F,wt=15): 5990 x v ((y v x) ^ (z v (u v y))) = x v y. [para(65(a,1),5888(a,1,2,2))]. given #394 (T,wt=15): 6043 x v (y ^ ((y ^ z) v x)) = x v (y ^ z). [para(3601(a,1),5888(a,1,2)),rewrite(4(3))]. given #395 (T,wt=15): 6066 x v ((x v y) ^ (z v (y v u))) = x v y. [para(12(a,1),5968(a,1,2,2))]. given #396 (A,wt=19): 195 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),22(a,1,1)),rewrite(5(5),5(8))]. given #397 (F,wt=15): 6067 x v (((x ^ y) v z) ^ (z v u)) = x v z. [para(5968(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #398 (F,wt=15): 6068 x v (((y ^ x) v z) ^ (z v u)) = x v z. [para(5968(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #399 (T,wt=15): 6073 x v ((x v y) ^ (z v (u v y))) = x v y. [para(65(a,1),5968(a,1,2,2))]. given #400 (T,wt=15): 6090 x v (y ^ (x v (y ^ z))) = x v (y ^ z). [para(3601(a,1),5968(a,1,2)),rewrite(4(3))]. given #401 (A,wt=19): 197 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(14(a,1),22(a,1,1)),rewrite(5(4))]. given #402 (F,wt=15): 6092 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(3634(a,1),5968(a,1,2)),rewrite(4(3))]. given #403 (F,wt=15): 6204 x v ((y v (x ^ z)) ^ (u v y)) = x v y. [para(5969(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #404 (T,wt=15): 6208 x v ((y v (z ^ x)) ^ (u v y)) = x v y. [para(5969(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #405 (T,wt=15): 6322 x v ((y v (z v u)) ^ (z v x)) = x v z. [para(12(a,1),5973(a,1,2,1))]. given #406 (A,wt=19): 200 x ^ (y ^ (z ^ (u v (v v (x ^ y))))) = x ^ (y ^ z). [para(22(a,1),71(a,1,2,2,2)),rewrite(5(6),5(5))]. given #407 (F,wt=15): 6324 x v ((y v z) ^ (y v (x ^ u))) = x v y. [para(5973(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #408 (F,wt=15): 6326 x v ((y v z) ^ (y v (u ^ x))) = x v y. [para(5973(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #409 (T,wt=15): 6338 x v ((y v (z v u)) ^ (u v x)) = x v u. [para(65(a,1),5973(a,1,2,1))]. given #410 (T,wt=15): 6412 x v (((x ^ y) v z) ^ (u v z)) = x v z. [para(6060(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #411 (A,wt=17): 201 (x v (y v z)) ^ (z v (x v y)) = x v (y v z). [para(3(a,1),83(a,1,1)),rewrite(3(7))]. given #412 (F,wt=15): 6415 x v (((y ^ x) v z) ^ (u v z)) = x v z. [para(6060(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #413 (F,wt=15): 6481 x v ((y v (z v u)) ^ (x v z)) = x v z. [para(12(a,1),6064(a,1,2,1))]. given #414 (T,wt=15): 6483 x v ((y v z) ^ ((x ^ u) v y)) = x v y. [para(6064(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #415 (T,wt=15): 6484 x v ((y v z) ^ ((u ^ x) v y)) = x v y. [para(6064(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #416 (A,wt=17): 202 (x v (y v z)) ^ (y v (z v x)) = x v (y v z). [para(3(a,1),83(a,1,2))]. given #417 (F,wt=15): 6490 x v ((y v (z v u)) ^ (x v u)) = x v u. [para(65(a,1),6064(a,1,2,1))]. given #418 (F,wt=15): 6593 x v ((y v z) ^ (z v (x ^ u))) = x v z. [para(6198(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #419 (T,wt=15): 6595 x v ((y v z) ^ (z v (u ^ x))) = x v z. [para(6198(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #420 (T,wt=15): 6682 x v ((y v z) ^ ((x ^ u) v z)) = x v z. [para(6406(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #421 (A,wt=17): 205 (x v (y v z)) ^ (x v (z v y)) = x v (y v z). [para(12(a,1),83(a,1,2)),rewrite(3(2),3(7))]. given #422 (F,wt=15): 6683 x v ((y v z) ^ ((u ^ x) v z)) = x v z. [para(6406(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #423 (F,wt=17): 209 x v (y v (z ^ (u ^ (v ^ (x v y))))) = x v y. [para(86(a,1),3(a,1)),flip(a)]. given #424 (T,wt=17): 212 x ^ (y ^ (z ^ (u ^ x))) = y ^ (z ^ (u ^ x)). [para(86(a,1),15(a,1,2)),rewrite(4(4))]. given #425 (T,wt=17): 213 (x ^ y) v (z ^ (u ^ (x ^ (v ^ y)))) = x ^ y. [para(14(a,1),86(a,1,2,2,2))]. given #426 (A,wt=19): 214 x v (y v (z v (u ^ (v ^ (x v y))))) = x v (y v z). [para(16(a,1),86(a,1,2,2,2)),rewrite(3(6),3(5))]. given #427 (F,wt=17): 224 x v (y v (z ^ (u ^ ((x v y) ^ v)))) = x v y. [para(93(a,1),3(a,1)),flip(a)]. given #428 (F,wt=17): 225 (x ^ y) v (z ^ (u ^ (x ^ (y ^ v)))) = x ^ y. [para(5(a,1),93(a,1,2,2,2))]. given #429 (T,wt=17): 227 (x v (y v z)) ^ (u ^ (x v y)) = u ^ (x v y). [para(3(a,1),97(a,1,1))]. given #430 (T,wt=17): 232 x ^ (y ^ ((y ^ ((x ^ y) v z)) v u)) = x ^ y. [para(18(a,1),97(a,1,2)),rewrite(4(6),5(6),18(10))]. given #431 (A,wt=19): 215 ((x v y) ^ z) v (u ^ (v ^ (x ^ z))) = (x v y) ^ z. [para(17(a,1),86(a,1,2,2,2))]. given #432 (F,wt=17): 235 (x ^ (y v z)) v (x ^ (u ^ y)) = x ^ (y v z). [para(97(a,1),22(a,1,2,2))]. given #433 (F,wt=17): 265 (x ^ (y ^ z)) v (u v (x ^ y)) = u v (x ^ y). [para(5(a,1),104(a,1,1))]. given #434 (T,wt=17): 268 (x v (y ^ z)) ^ (x v (u v y)) = x v (y ^ z). [para(104(a,1),16(a,1,2,2))]. given #435 (T,wt=17): 272 x v (y v ((y v ((x v y) ^ z)) ^ u)) = x v y. [para(20(a,1),104(a,1,2)),rewrite(2(6),3(6),20(10))]. given #436 (A,wt=23): 217 (x ^ ((y ^ x) v z)) v (u ^ (v ^ (y ^ x))) = x ^ ((y ^ x) v z). [para(18(a,1),86(a,1,2,2,2))]. given #437 (F,wt=17): 277 (x v (y v z)) ^ (u ^ (x v z)) = u ^ (x v z). [para(12(a,1),121(a,1,1))]. given #438 (F,wt=17): 288 (x ^ (y v z)) v (x ^ (u ^ z)) = x ^ (y v z). [para(121(a,1),22(a,1,2,2))]. given #439 (T,wt=17): 296 (x ^ (y ^ z)) v (u v (x ^ z)) = u v (x ^ z). [para(14(a,1),132(a,1,1))]. given #440 (T,wt=17): 297 (x v (y ^ z)) ^ (x v (u v z)) = x v (y ^ z). [para(132(a,1),16(a,1,2,2))]. given #441 (A,wt=21): 218 x ^ (y ^ (z ^ (u ^ (x ^ v)))) = y ^ (z ^ (u ^ (x ^ v))). [para(86(a,1),47(a,1,2,1)),rewrite(14(5),5(4),5(3),5(2),5(9),5(8),5(7))]. given #442 (F,wt=17): 306 x v (y v (z ^ (y v ((x v y) ^ u)))) = x v y. [para(20(a,1),132(a,1,2)),rewrite(2(6),3(6),20(10))]. given #443 (F,wt=17): 313 (x ^ (y ^ z)) v (z ^ (x ^ y)) = x ^ (y ^ z). [para(5(a,1),196(a,1,1)),rewrite(5(7))]. given #444 (T,wt=17): 314 (x ^ (y ^ z)) v (y ^ (z ^ x)) = x ^ (y ^ z). [para(5(a,1),196(a,1,2))]. given #445 (T,wt=17): 315 (x ^ (y ^ z)) v (x ^ (z ^ y)) = y ^ (x ^ z). [para(14(a,1),196(a,1,1)),rewrite(5(4))]. given #446 (A,wt=19): 219 ((x v y) ^ z) v (u ^ (v ^ (y ^ z))) = (x v y) ^ z. [para(47(a,1),86(a,1,2,2,2))]. given #447 (F,wt=17): 376 x ^ (y ^ ((x ^ (z v (y ^ x))) v u)) = x ^ y. [para(26(a,2),60(a,1,2)),rewrite(14(8),5(7),98(8),58(9))]. given #448 (F,wt=17): 412 x ^ (y ^ (z ^ (u v (x ^ z)))) = y ^ (x ^ z). [para(48(a,1),14(a,1,2)),flip(a)]. given #449 (T,wt=17): 419 x ^ (y ^ ((y ^ (z v (x ^ y))) v u)) = x ^ y. [para(48(a,1),97(a,1,2)),rewrite(4(6),5(6),48(10))]. given #450 (T,wt=17): 430 x v (y v (z v (u ^ (x v z)))) = x v (y v z). [para(49(a,1),52(a,1,2,2)),rewrite(3(5),3(4))]. given #451 (A,wt=19): 220 (x ^ (y v z)) v (u ^ (v ^ (x ^ y))) = x ^ (y v z). [para(58(a,1),86(a,1,2,2,2))]. given #452 (F,wt=17): 443 (x v (y ^ z)) ^ (x v (z ^ y)) = x v (y ^ z). [para(196(a,1),49(a,1,2,2))]. given #453 (F,wt=17): 452 x v (y v ((y v (z ^ (x v y))) ^ u)) = x v y. [para(51(a,1),104(a,1,2)),rewrite(2(6),3(6),51(10))]. given #454 (T,wt=17): 454 x v (y v (z ^ (y v (u ^ (x v y))))) = x v y. [para(51(a,1),132(a,1,2)),rewrite(2(6),3(6),51(10))]. given #455 (T,wt=17): 522 (x ^ (y v z)) v (x ^ (z v y)) = x ^ (y v z). [para(83(a,1),61(a,1,2,2))]. given #456 (A,wt=19): 221 (x ^ (y v z)) v (u ^ (v ^ (x ^ z))) = x ^ (y v z). [para(60(a,1),86(a,1,2,2,2))]. given #457 (F,wt=17): 687 x ^ (y ^ ((z v (x v u)) ^ v)) = y ^ (x ^ v). [para(68(a,1),14(a,1,2)),flip(a)]. given #458 (F,wt=17): 689 x ^ (y ^ (((z v (x v u)) ^ y) v v)) = x ^ y. [para(18(a,1),68(a,1,2)),rewrite(68(4)),flip(a)]. given #459 (T,wt=17): 697 x ^ (y ^ ((z v (u v x)) ^ v)) = x ^ (y ^ v). [para(104(a,1),68(a,1,2,1,2)),rewrite(5(5),5(7))]. given #460 (T,wt=17): 698 x ^ (y ^ (z v ((u v (x v v)) ^ y))) = x ^ y. [para(68(a,1),121(a,1,2)),rewrite(4(6),5(6),68(10))]. given #461 (A,wt=21): 238 x ^ ((y ^ ((x ^ y) v z)) v u) = x ^ (u v (y ^ (x v z))). [para(2(a,1),25(a,1,2))]. ============================== PROOF ================================= % Proof 1 at 13.52 (+ 0.13) seconds: H3. % Length of proof is 40. % Level of proof is 9. % Maximum clause weight is 23. % Given clauses 461. 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) # answer(H3). [goal]. 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). [assumption]. 9 x ^ (y v (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))). [copy(8),flip(a)]. 10 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [deny(1)]. 12 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. 14 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. 15 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. 16 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. 17 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 19 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. 21 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 22 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. 23 x ^ x = x. [para(7(a,1),6(a,1,2))]. 25 x ^ (y v (z ^ ((x ^ z) v u))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),9(a,1,2,2,2))]. 40 x ^ (y ^ x) = y ^ x. [para(23(a,1),5(a,2,2)),rewrite(4(2))]. 50 x v ((y ^ x) v z) = x v z. [para(21(a,1),3(a,1,1)),flip(a)]. 60 x ^ (y ^ (z v x)) = y ^ x. [para(15(a,1),14(a,1,2)),flip(a)]. 76 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),16(a,1,1))]. 96 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(17(a,1),21(a,1,2)),rewrite(2(4))]. 103 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(19(a,1),15(a,1,2)),rewrite(4(4))]. 130 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(50(a,1),15(a,1,2)),rewrite(4(4))]. 166 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(60(a,1),21(a,1,2)),rewrite(2(4))]. 196 (x ^ y) v (y ^ x) = x ^ y. [para(40(a,1),22(a,1,2))]. 238 x ^ ((y ^ ((x ^ y) v z)) v u) = x ^ (u v (y ^ (x v z))). [para(2(a,1),25(a,1,2))]. 312 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(196(a,1),3(a,2,2)),rewrite(2(4))]. 317 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(196(a,1),19(a,2)),rewrite(5(3),312(6))]. 2170 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(6(a,1),96(a,1,1))]. 2340 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(7(a,1),103(a,1,1))]. 3601 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(317(a,1),130(a,1,2)),rewrite(4(5),5(5),2340(4),317(8))]. 3634 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(4(a,1),3601(a,1,2,1))]. 5888 x v ((y v x) ^ (y v z)) = x v y. [para(76(a,1),166(a,1,2)),rewrite(12(5),2(4),2170(4),76(8))]. 5968 x v ((x v y) ^ (y v z)) = x v y. [para(2(a,1),5888(a,1,2,1))]. 6092 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(3634(a,1),5968(a,1,2)),rewrite(4(3))]. 12705 $F # answer(H3). [para(238(a,2),10(a,1,2,2)),rewrite(4(7),2(11),2340(12),2(12),50(12),6092(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=461. Generated=401184. Kept=12702. proofs=1. Usable=457. Sos=9996. Demods=9658. Limbo=0, Disabled=2257. Hints=0. Weight_deleted=14. Literals_deleted=0. Forward_subsumed=311448. Back_subsumed=234. Sos_limit_deleted=77019. Sos_displaced=1346. Sos_removed=0. New_demodulators=11462 (6 lex), Back_demodulated=667. Back_unit_deleted=0. Demod_attempts=6379817. Demod_rewrites=1024772. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=12.50. User_CPU=13.52, System_CPU=0.13, Wall_clock=16. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11537 exit (max_proofs) Sat Aug 12 21:08:38 2006