============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4386 was started by mccune on cleo.thornwood, Wed Nov 22 12:03:36 2006 The command was "/home/mccune/bin/prover9 -t 7200 -f LT.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file LT.in set(lex_order_vars). assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_weight,30). assign(max_minutes,10). % assign(max_minutes, 10) -> assign(max_seconds, 600). 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. formulas(sos). (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). end_of_list. formulas(goals). x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2). end_of_list. ============================== end of input ========================== % From the command line: assign(max_seconds, 7200). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2) # label(goal). [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 (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [assumption]. c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label H2 to answer in negative clause 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]. 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. 5 x ^ y = y ^ x. [assumption]. 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. 13 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(12),rewrite(2(12))]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. % (lex-dep) 5 x ^ y = y ^ x. [assumption]. % (lex-dep) 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. % (lex-dep) 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. 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): 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. given #3 (I,wt=7): 5 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. given #5 (I,wt=7): 8 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 9 x v (x ^ y) = x. [assumption]. given #7 (I,wt=21): 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. given #8 (I,wt=23): 13 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(12),rewrite(2(12))]. given #9 (F,wt=5): 16 x ^ x = x. [para(9(a,1),8(a,1,2))]. given #10 (F,wt=5): 17 x v x = x. [para(8(a,1),9(a,1,2))]. given #11 (F,wt=11): 14 x v (y v z) = y v (x v z). [para(4(a,1),2(a,1)),rewrite(2(3),2(4))]. given #12 (T,wt=9): 26 x v (x v y) = x v y. [para(14(a,1),17(a,1)),rewrite(2(2),14(2),17(1))]. given #13 (A,wt=11): 15 x ^ (y ^ z) = y ^ (x ^ z). [para(7(a,1),5(a,1)),rewrite(5(3),5(4))]. given #14 (F,wt=9): 32 x ^ (x ^ y) = x ^ y. [para(15(a,1),16(a,1)),rewrite(5(2),15(2),16(1))]. given #15 (F,wt=11): 24 x v (y v (x ^ z)) = x v y. [para(9(a,1),14(a,2,2)),rewrite(2(4))]. given #16 (F,wt=11): 30 x ^ (y ^ (x v z)) = x ^ y. [para(8(a,1),15(a,2,2)),rewrite(5(4))]. given #17 (F,wt=13): 28 x ^ ((x v y) v (y ^ (x v y))) = x. [back_rewrite(22),rewrite(26(3))]. given #18 (T,wt=15): 37 x v (y v (z v (x ^ u))) = x v (y v z). [para(24(a,1),14(a,2,2)),rewrite(14(6))]. given #19 (A,wt=21): 18 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (z ^ x) v (x ^ y). [para(11(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. given #20 (F,wt=15): 41 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(30(a,1),15(a,2,2)),rewrite(15(6))]. given #21 (F,wt=15): 51 x ^ ((y ^ z) ^ (y v u)) = x ^ (y ^ z). [para(11(a,1),41(a,1,2,2)),rewrite(5(4),2(5),15(7),39(6),15(2),5(1),5(5),5(6),15(6)),flip(a)]. given #22 (F,wt=11): 57 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),51(a,2)),rewrite(32(5))]. given #23 (F,wt=11): 62 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),57(a,1,1)),rewrite(5(4))]. given #24 (T,wt=13): 69 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(57(a,1),57(a,1,1)),rewrite(2(3),57(7))]. given #25 (A,wt=27): 25 x ^ (((x v y) ^ (z v u)) v (y ^ (x v (z v u)))) = (x ^ y) v (x ^ (z v u)). [para(14(a,1),11(a,1,2,1,2)),rewrite(14(2),5(6),2(7),2(12))]. given #26 (F,wt=13): 82 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(69(a,1),18(a,1,2,1)),rewrite(17(5),15(4),5(3),8(6),15(3),5(2),16(6),2(5)),flip(a)]. given #27 (F,wt=15): 64 (x ^ (y ^ z)) ^ (y v u) = x ^ (y ^ z). [para(15(a,1),57(a,1,1)),rewrite(15(6))]. given #28 (F,wt=15): 74 (x ^ y) ^ (z v (y ^ (x v u))) = x ^ y. [para(30(a,1),62(a,1,1)),rewrite(2(4),30(8))]. given #29 (F,wt=13): 111 x ^ (y v ((x v z) ^ (x v u))) = x. [para(8(a,1),74(a,1,1)),rewrite(8(7))]. given #30 (T,wt=15): 75 x ^ (y v ((x v z) v (z ^ (x v z)))) = x. [para(28(a,1),62(a,1,1)),rewrite(2(5),28(11))]. given #31 (A,wt=25): 31 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(11(a,1),15(a,2,2)),rewrite(2(5),2(10))]. given #32 (F,wt=13): 135 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(31(a,1),9(a,1,2))]. given #33 (F,wt=15): 86 (x ^ y) ^ (z v (u v (x ^ y))) = x ^ y. [para(69(a,1),62(a,1,1)),rewrite(2(4),14(4),69(9))]. given #34 (F,wt=15): 90 x ^ ((x v y) v (y ^ (x v (y v z)))) = x. [para(8(a,1),25(a,1,2,1)),rewrite(2(3),14(3),2(2),26(4),2(9),14(9),2(8),8(10),2(8),9(8))]. given #35 (F,wt=15): 103 x v ((x ^ y) v (z ^ u)) = x v (z ^ u). [para(82(a,1),37(a,2,2)),rewrite(2(5),14(6),82(5))]. given #36 (T,wt=15): 105 (x ^ (y ^ z)) ^ (z v u) = x ^ (y ^ z). [para(5(a,1),64(a,1,1,2)),rewrite(5(5))]. given #37 (A,wt=17): 34 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(11(a,1),32(a,1,2)),rewrite(11(10))]. given #38 (F,wt=15): 110 (x ^ y) ^ (z v (x ^ (y v u))) = x ^ y. [para(74(a,1),5(a,2)),rewrite(5(4),5(5),5(6))]. given #39 (F,wt=15): 128 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(111(a,1),62(a,1,1)),rewrite(2(5),14(5),111(11))]. given #40 (F,wt=17): 39 (x ^ (y v z)) ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(11(a,1),30(a,1,2)),rewrite(5(4),2(5),5(9),15(9),8(8))]. given #41 (F,wt=11): 212 x ^ (y ^ (z v y)) = x ^ y. [para(2(a,1),39(a,1,1,2)),rewrite(5(4),50(6))]. given #42 (T,wt=15): 214 (x ^ (y v z)) ^ (y v (x ^ y)) = x ^ y. [para(8(a,1),39(a,1,2,2)),rewrite(26(2),2(4))]. given #43 (A,wt=29): 35 (x ^ y) v (x ^ (z v (x ^ u))) = x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ u)))). [para(24(a,1),11(a,1,2,1,2)),rewrite(5(6),2(13)),flip(a)]. given #44 (F,wt=11): 271 x ^ (y v (x ^ y)) = x ^ y. [para(111(a,1),214(a,1,1))]. given #45 (F,wt=15): 215 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(39(a,1),9(a,1,2)),rewrite(2(4))]. given #46 (F,wt=15): 262 (x ^ (y v z)) ^ (z v (x ^ z)) = x ^ z. [para(2(a,1),214(a,1,1,2))]. given #47 (F,wt=11): 317 x ^ (y ^ (z v x)) = x ^ y. [para(5(a,1),262(a,1,1)),rewrite(5(2),5(3),9(4),5(3),5(4))]. given #48 (T,wt=13): 321 x ^ ((x ^ y) ^ (z v y)) = x ^ y. [para(262(a,1),32(a,1,2)),rewrite(5(4),15(4),262(9))]. given #49 (A,wt=29): 38 x ^ ((y ^ ((x v z) ^ (x v u))) v (z ^ (x v (y ^ (x v u))))) = (x ^ z) v (x ^ y). [para(30(a,1),11(a,2,1)),rewrite(5(8),15(8),2(9),2(13))]. given #50 (F,wt=15): 294 x ^ (y ^ (z v (x ^ z))) = x ^ (y ^ z). [para(271(a,1),15(a,2,2)),rewrite(15(6))]. given #51 (F,wt=15): 300 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(5(a,1),215(a,1,1))]. given #52 (F,wt=7): 376 x v (y ^ x) = x. [para(111(a,1),300(a,1,2)),rewrite(2(2),111(7))]. given #53 (F,wt=9): 377 x ^ (y v (x v z)) = x. [para(75(a,1),300(a,1,2)),rewrite(2(2),376(2),376(4)),flip(a)]. given #54 (T,wt=15): 318 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(262(a,1),9(a,1,2)),rewrite(2(4))]. given #55 (A,wt=19): 40 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(11(a,1),30(a,2)),rewrite(2(5),5(7),31(8),2(8))]. given #56 (F,wt=13): 406 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(376(a,1),318(a,1,2,2)),rewrite(2(4),376(6))]. given #57 (F,wt=15): 323 (x ^ y) ^ (z v (x ^ (u v y))) = x ^ y. [para(262(a,1),57(a,2)),rewrite(262(5),2(4))]. given #58 (F,wt=15): 414 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(215(a,1),40(a,1,2)),rewrite(15(4),215(8))]. given #59 (F,wt=13): 440 (x v y) ^ (x v (y v z)) = x v y. [para(16(a,1),414(a,2)),rewrite(2(3),14(3),2(2),5(5),32(6))]. given #60 (T,wt=13): 458 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(98),rewrite(441(6))]. given #61 (A,wt=19): 46 x v (y v (z v (u v (x ^ v)))) = x v (y v (z v u)). [para(37(a,1),14(a,2,2)),rewrite(14(8))]. given #62 (F,wt=15): 457 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [back_rewrite(407),rewrite(441(7))]. given #63 (F,wt=17): 71 (x ^ (y ^ z)) ^ (u v (x ^ z)) = x ^ (y ^ z). [para(15(a,1),62(a,1,1)),rewrite(2(4),15(7))]. given #64 (F,wt=17): 72 (x ^ (y ^ z)) ^ (u v (y ^ z)) = x ^ (y ^ z). [para(15(a,1),62(a,2)),rewrite(2(4),15(7))]. given #65 (F,wt=17): 100 (x ^ y) v (x ^ ((y ^ z) v (y ^ u))) = x ^ y. [para(11(a,1),82(a,1,2,2))]. given #66 (T,wt=17): 121 (x ^ y) ^ (z v (u v (y ^ (x v v)))) = x ^ y. [para(74(a,1),62(a,1,1)),rewrite(2(5),14(5),74(11))]. given #67 (A,wt=21): 47 x ^ ((y ^ (z v x)) v (z ^ (y v x))) = (z ^ x) v (y ^ x). [para(18(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. given #68 (F,wt=15): 605 x ^ ((y ^ z) ^ (u v y)) = x ^ (y ^ z). [para(47(a,1),41(a,1,2,2)),rewrite(2(5),15(7),251(6),15(2),5(1),5(5),5(6),15(6)),flip(a)]. given #69 (F,wt=17): 127 x ^ (y ^ (z v ((x v u) ^ (x v v)))) = x ^ y. [para(111(a,1),15(a,2,2)),rewrite(5(7))]. given #70 (F,wt=17): 134 (x ^ (y v z)) ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(8(a,1),31(a,1,2)),rewrite(30(3),2(6)),flip(a)]. given #71 (F,wt=17): 139 x v (y v (z ^ ((x ^ u) v (x ^ v)))) = x v y. [para(31(a,1),24(a,1,2,2))]. given #72 (T,wt=17): 147 (x ^ y) v (y ^ ((x ^ z) v (x ^ u))) = x ^ y. [para(31(a,1),82(a,1,2))]. given #73 (A,wt=19): 48 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [para(8(a,1),18(a,2,1)),rewrite(26(3),2(5),14(5),2(4),8(6),2(4),5(7))]. given #74 (F,wt=15): 678 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(48(a,1),458(a,1,2))]. given #75 (F,wt=13): 696 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(147(a,1),678(a,1,2)),rewrite(5(1),32(2),5(2)),flip(a)]. given #76 (F,wt=15): 711 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(696(a,1),414(a,1,2)),rewrite(5(2),30(3),5(3),2(5)),flip(a)]. given #77 (F,wt=15): 720 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(5(a,1),711(a,1,2,1))]. given #78 (T,wt=13): 760 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(9(a,1),720(a,1,2,2,2)),rewrite(5(2),2(3))]. given #79 (A,wt=19): 54 x ^ (y ^ (z ^ (u ^ (x v v)))) = x ^ (y ^ (z ^ u)). [para(41(a,1),15(a,2,2)),rewrite(15(8))]. given #80 (F,wt=13): 1010 x ^ ((y ^ z) v (y ^ x)) = y ^ x. [back_rewrite(351),rewrite(965(9),5(8),834(8),834(7),40(6),40(5))]. given #81 (F,wt=13): 1011 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(1010(a,1),5(a,1)),rewrite(2(4),5(5)),flip(a)]. given #82 (F,wt=15): 834 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [back_rewrite(454),rewrite(814(6),15(6),459(5),15(4),32(3)),flip(a)]. given #83 (F,wt=15): 972 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [back_rewrite(323),rewrite(2(2),834(5))]. given #84 (T,wt=15): 1009 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [back_rewrite(74),rewrite(834(5))]. given #85 (A,wt=23): 67 (x v y) ^ ((x ^ z) v (u ^ (x v y))) = (x ^ z) v (u ^ (x v y)). [para(57(a,1),18(a,2,1)),rewrite(14(4),2(3),24(4),2(6),14(6),2(5),57(7),2(5),5(9))]. given #86 (F,wt=15): 1012 x ^ ((x ^ y) v (z ^ (y ^ u))) = x ^ y. [para(15(a,1),1010(a,1,2,1)),rewrite(5(3),2(4),5(6))]. given #87 (F,wt=15): 1029 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(834(a,1),135(a,1,2))]. given #88 (F,wt=15): 1033 (x v y) v (z ^ (u ^ (x v y))) = x v y. [para(834(a,1),376(a,1,2))]. given #89 (F,wt=15): 1114 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(1012(a,1),318(a,1,2)),rewrite(2(5),1012(10))]. given #90 (T,wt=17): 152 x v (y ^ ((x ^ z) v ((x ^ u) v (x ^ v)))) = x. [para(11(a,1),135(a,1,2,2,1)),rewrite(2(5),14(5),2(4))]. given #91 (A,wt=19): 68 (x v y) ^ ((z ^ x) v (x ^ u)) = (z ^ x) v (x ^ u). [para(18(a,1),57(a,1,1)),rewrite(5(5),18(11))]. given #92 (F,wt=17): 208 x ^ (y v (z v (u v ((x v v) ^ (x v w))))) = x. [para(128(a,1),62(a,1,1)),rewrite(2(6),14(6),14(5),128(13))]. given #93 (F,wt=17): 304 (x ^ (y ^ z)) v (x ^ (y v u)) = x ^ (y v u). [para(215(a,1),24(a,2)),rewrite(5(5),15(5),5(4),2(6),242(7))]. given #94 (F,wt=17): 362 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(8(a,1),300(a,1,1))]. given #95 (F,wt=17): 386 x ^ ((y v z) ^ (y v (u v z))) = x ^ (y v z). [back_rewrite(320),rewrite(376(7),5(5),15(5))]. given #96 (T,wt=17): 473 x ^ (y ^ (z ^ (u v (x ^ z)))) = x ^ (y ^ z). [para(458(a,1),15(a,2,2)),rewrite(15(7))]. given #97 (A,wt=29): 70 ((x ^ y) v (x ^ z)) ^ (u v ((z ^ (x v y)) v (y ^ (x v z)))) = (x ^ y) v (x ^ z). [para(11(a,1),62(a,1,1)),rewrite(2(9),11(16))]. given #98 (F,wt=17): 608 (x ^ (y ^ z)) v (x ^ (u v y)) = x ^ (u v y). [para(605(a,1),406(a,1,2)),rewrite(2(5))]. given #99 (F,wt=17): 670 (x v y) ^ (x v ((y v z) ^ (y v u))) = x v y. [para(111(a,1),48(a,1,2,2)),rewrite(5(6),111(11))]. given #100 (F,wt=17): 691 x ^ (y v ((x v z) ^ (y v u))) = x ^ (y v u). [para(678(a,1),414(a,1,2)),rewrite(414(4)),flip(a)]. given #101 (F,wt=17): 699 x ^ ((x ^ y) v ((y ^ z) v (y ^ u))) = x ^ y. [para(11(a,1),696(a,1,2,2))]. given #102 (T,wt=17): 700 x ^ (y ^ ((x ^ z) v (z ^ u))) = x ^ (y ^ z). [para(696(a,1),15(a,2,2)),rewrite(15(7))]. given #103 (A,wt=29): 77 ((x ^ y) v (y ^ z)) ^ (u v ((z ^ (x v y)) v (x ^ (y v z)))) = (x ^ y) v (y ^ z). [para(18(a,1),62(a,1,1)),rewrite(2(9),18(16))]. given #104 (F,wt=11): 1346 x ^ (y v (x ^ (z v x))) = x. [para(16(a,1),77(a,1,1,2)),rewrite(2(2),376(2),17(3),2(4),300(4),16(6),2(6),376(6))]. given #105 (F,wt=7): 1363 x ^ (y v x) = x. [para(1346(a,1),5(a,2)),rewrite(2(1),8(2),5(2))]. given #106 (F,wt=13): 1345 x ^ (y v ((z v x) ^ (x v u))) = x. [para(8(a,1),77(a,1,1,2)),rewrite(2(2),376(2),5(3),26(5),2(6),455(6),8(8),2(7),376(7))]. given #107 (F,wt=15): 1366 x ^ (y v (x ^ (z v y))) = x ^ (z v y). [para(1346(a,1),760(a,1,2,2)),rewrite(2(1),8(2),2(3),2(5),8(6))]. given #108 (T,wt=15): 1367 (x v y) ^ (y v (x ^ z)) = y v (x ^ z). [para(1346(a,1),67(a,1,2,2)),rewrite(2(1),8(2),2(3),2(6),8(7),1363(7),2(6))]. given #109 (A,wt=19): 101 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(15(a,1),82(a,1,1)),rewrite(5(4),15(4),5(3),15(5),15(8))]. given #110 (F,wt=15): 1369 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(24(a,1),1363(a,1,2)),rewrite(2(3),5(4))]. given #111 (F,wt=17): 724 x ^ ((y ^ (z ^ u)) v (z ^ (x v v))) = x ^ z. [para(15(a,1),711(a,1,2,1))]. given #112 (F,wt=9): 1505 x v (y ^ (x ^ z)) = x. [para(724(a,1),1369(a,1)),rewrite(2(3),5(4),8(4),2(5),2(6),14(6),8(7),2(3)),flip(a)]. given #113 (F,wt=13): 1507 (x v y) v (x ^ (z v u)) = x v y. [para(414(a,1),1505(a,1,2))]. given #114 (T,wt=13): 1513 (x v y) v (y ^ (z v u)) = x v y. [para(2(a,1),1507(a,1,1)),rewrite(2(5))]. given #115 (A,wt=19): 130 x ^ (y v ((x v z) ^ (u v ((x v v) ^ (x v w))))) = x. [para(111(a,1),74(a,1,1)),rewrite(5(6),111(13))]. given #116 (F,wt=15): 1480 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(724(a,1),300(a,1,2)),rewrite(5(3),15(3),15(2),5(1),5(4),2(5),724(11),5(6))]. given #117 (F,wt=15): 1511 (x v y) v (z ^ (y v (x ^ u))) = x v y. [para(1367(a,1),1505(a,1,2,2))]. given #118 (F,wt=15): 1512 (x v y) v (z ^ (x v (y ^ u))) = x v y. [para(1369(a,1),1505(a,1,2,2))]. given #119 (F,wt=15): 1517 (x v y) v (x ^ (z ^ (u v v))) = x v y. [para(215(a,1),1507(a,1,2,2))]. given #120 (T,wt=15): 1532 (x v y) v (y ^ (z ^ (u v v))) = x v y. [para(215(a,1),1513(a,1,2,2))]. given #121 (A,wt=21): 136 x ^ (y ^ ((x ^ z) v (x ^ u))) = y ^ ((x ^ z) v (x ^ u)). [para(9(a,1),31(a,1,2,2,1,2)),rewrite(5(1),57(4),32(7),2(8))]. given #122 (F,wt=15): 1573 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(1480(a,1),1367(a,1,2)),rewrite(5(4),1363(4),5(3)),flip(a)]. given #123 (F,wt=17): 747 x ^ ((y ^ (x v z)) v (y ^ (u v v))) = x ^ y. [para(414(a,1),711(a,1,2,1)),rewrite(2(5))]. given #124 (F,wt=17): 794 x ^ ((y ^ z) v (x ^ (y v u))) = x ^ (y v u). [para(57(a,1),760(a,1,2,2)),rewrite(2(4))]. given #125 (F,wt=17): 831 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [back_rewrite(503),rewrite(814(5))]. given #126 (T,wt=17): 945 x ^ (y ^ (z v (y ^ (u v (x ^ y))))) = x ^ y. [back_rewrite(477),rewrite(834(6))]. given #127 (A,wt=27): 137 ((x ^ y) v (x ^ z)) ^ ((z ^ (x v y)) v (y ^ (x v z))) = (x ^ y) v (x ^ z). [para(16(a,1),31(a,1,2)),rewrite(2(5),11(6),2(8),2(11),5(12)),flip(a)]. given #128 (F,wt=17): 978 x ^ (y ^ (z v (x ^ (y ^ z)))) = x ^ (y ^ z). [back_rewrite(269),rewrite(834(5))]. given #129 (F,wt=17): 984 x ^ (y ^ (z v (u v (x ^ (y v v))))) = x ^ y. [back_rewrite(203),rewrite(834(6))]. given #130 (F,wt=17): 987 x ^ (y ^ (z v (x ^ (u v (x ^ y))))) = x ^ y. [back_rewrite(198),rewrite(834(6))]. given #131 (F,wt=17): 997 x ^ (y ^ (z v (u v (v v (x ^ y))))) = x ^ y. [back_rewrite(159),rewrite(834(6))]. given #132 (T,wt=17): 1004 x ^ (y ^ (z v (u v (y ^ (x v v))))) = x ^ y. [back_rewrite(121),rewrite(834(6))]. given #133 (A,wt=29): 138 x ^ (y ^ (z ^ ((u ^ (x v v)) v (v ^ (x v u))))) = y ^ (z ^ ((x ^ v) v (x ^ u))). [para(31(a,1),15(a,2,2)),rewrite(2(5),2(11))]. given #134 (F,wt=17): 1013 x ^ ((x ^ y) v ((z ^ y) v (y ^ u))) = x ^ y. [para(18(a,1),1010(a,1,2,1)),rewrite(5(4),2(5),5(7))]. given #135 (F,wt=17): 1022 x ^ (y ^ ((x ^ z) v (u ^ z))) = x ^ (y ^ z). [para(1010(a,1),720(a,1,2,2)),rewrite(2(4),834(5),5(7),15(7),5(6))]. given #136 (F,wt=17): 1077 x ^ (y ^ (z v ((x ^ y) v (x ^ u)))) = x ^ y. [para(11(a,1),972(a,1,2,2,2)),rewrite(2(5),834(7),441(8),30(9))]. given #137 (F,wt=17): 1085 x ^ (y ^ (z v ((x ^ y) v (y ^ u)))) = x ^ y. [para(11(a,1),1009(a,1,2,2,2)),rewrite(5(4),2(5),15(8),834(7),15(8),414(7),5(9),15(9),8(8))]. given #138 (T,wt=17): 1101 (x v (y v z)) ^ (y v (x ^ u)) = y v (x ^ u). [para(377(a,1),67(a,1,2,2)),rewrite(2(4),377(9),2(7))]. given #139 (A,wt=21): 140 x v (y v (z v (u ^ ((x ^ v) v (x ^ w))))) = x v (y v z). [para(31(a,1),37(a,1,2,2,2))]. given #140 (F,wt=15): 1909 (x v y) ^ (z v (x v (y v u))) = x v y. [para(1033(a,1),1101(a,1,2)),rewrite(2(2),14(2),2(1),5(5),1033(10))]. given #141 (F,wt=17): 1131 x v (y ^ (z ^ (u ^ ((x ^ v) v (x ^ w))))) = x. [para(834(a,1),1029(a,1,2,2))]. given #142 (F,wt=17): 1137 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(440(a,1),1033(a,1,2,2)),rewrite(2(5),14(5),14(4),2(3))]. given #143 (F,wt=13): 1958 x v (y v (z ^ (x v y))) = x v y. [para(9(a,1),1137(a,2,2)),rewrite(103(5))]. given #144 (T,wt=13): 1974 x v ((y v x) ^ (y v z)) = y v x. [para(362(a,1),1137(a,1,2,2)),rewrite(5(3),1201(5),2(5),26(6))]. given #145 (A,wt=19): 146 (x ^ y) v (x ^ (z ^ ((y ^ u) v (y ^ v)))) = x ^ y. [para(31(a,1),82(a,1,2,2))]. given #146 (F,wt=13): 1999 x v ((x v y) ^ (y v z)) = x v y. [para(2(a,1),1974(a,1,2,1)),rewrite(2(5))]. given #147 (F,wt=15): 1993 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(834(a,1),1958(a,1,2,2))]. given #148 (F,wt=15): 2006 x v ((y v z) ^ (y v (x ^ u))) = x v y. [para(1974(a,1),103(a,1,2)),rewrite(24(3),5(5)),flip(a)]. given #149 (F,wt=13): 2093 (x v y) ^ (x v (z v y)) = x v y. [para(2006(a,1),1367(a,1,2)),rewrite(2(2),14(2),2(1),2(3),5(4),2006(9),2(5))]. given #150 (T,wt=15): 2013 x v (y ^ (x v (y ^ z))) = x v (y ^ z). [para(711(a,1),1974(a,1,2)),rewrite(2(2),5(3),2(6))]. given #151 (A,wt=29): 151 x ^ ((x ^ y) v (z ^ ((x ^ u) v (x ^ v)))) = (x ^ y) v (z ^ ((x ^ u) v (x ^ v))). [para(135(a,1),11(a,1,2,1,2)),rewrite(5(1),5(7),15(7),40(6),136(12),2(13))]. given #152 (F,wt=15): 2014 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(720(a,1),1974(a,1,2)),rewrite(2(2),5(3),2(6))]. given #153 (F,wt=13): 2195 x v ((x v y) ^ (z v y)) = x v y. [para(1363(a,1),2014(a,1,2,2,2)),rewrite(5(3),1363(6))]. given #154 (F,wt=15): 2072 x v ((y v z) ^ (z v (x ^ u))) = x v z. [para(2(a,1),2006(a,1,2,1))]. given #155 (F,wt=15): 2099 (x v y) ^ (x v (z v (y v u))) = x v y. [para(2006(a,1),1101(a,1,2)),rewrite(14(3),2(2),14(2),2(1),14(3),14(2),2(4),5(5),2006(10),2(6))]. given #156 (T,wt=15): 2111 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(376(a,1),2093(a,1,2,2)),rewrite(5(4))]. given #157 (A,wt=19): 153 x v (y ^ ((x ^ z) v (u ^ ((x ^ v) v (x ^ w))))) = x. [para(31(a,1),135(a,1,2,2,1)),rewrite(2(6))]. given #158 (F,wt=15): 2178 x v ((x v y) ^ (z v (y v u))) = x v y. [para(377(a,1),2014(a,1,2,2,2)),rewrite(5(4),377(8))]. given #159 (F,wt=17): 1141 (x v y) v (z ^ (u ^ (v ^ (x v y)))) = x v y. [para(834(a,1),1033(a,1,2,2))]. given #160 (F,wt=17): 1180 (x ^ (y ^ z)) v (x ^ (z v u)) = x ^ (z v u). [para(5(a,1),304(a,1,1,2))]. given #161 (F,wt=15): 2368 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(720(a,1),1180(a,1,2)),rewrite(2(5),720(10))]. given #162 (T,wt=17): 1181 (x ^ (y ^ z)) v (z ^ (x v u)) = z ^ (x v u). [para(5(a,1),304(a,1,1)),rewrite(5(2),15(2),5(1))]. given #163 (A,wt=27): 154 ((x ^ y) v (x ^ z)) ^ (u v (v v ((x ^ y) v (x ^ z)))) = (x ^ y) v (x ^ z). [para(11(a,1),86(a,1,1)),rewrite(11(9),11(15))]. given #164 (F,wt=9): 2412 x v (y ^ (z ^ x)) = x. [para(111(a,1),1181(a,1,2)),rewrite(2(3),111(8))]. given #165 (F,wt=15): 2454 x ^ ((x ^ y) v (z ^ (u ^ y))) = x ^ y. [para(2412(a,1),1366(a,1,2,2,2)),rewrite(2(4),2412(8))]. given #166 (F,wt=17): 1184 (x ^ (y ^ z)) v (y ^ (x v u)) = y ^ (x v u). [para(15(a,1),304(a,1,1))]. given #167 (F,wt=17): 1204 x ^ (y v ((x v z) ^ ((x v u) ^ (x v v)))) = x. [para(362(a,1),111(a,1,2,2,1)),rewrite(834(5))]. given #168 (T,wt=17): 1227 x v (y v (z v (u ^ (x v z)))) = x v (y v z). [para(386(a,1),1033(a,1,2)),rewrite(2(5),14(5),14(4),2(3))]. given #169 (A,wt=27): 157 ((x ^ y) v (y ^ z)) ^ (u v (v v ((x ^ y) v (y ^ z)))) = (x ^ y) v (y ^ z). [para(18(a,1),86(a,1,1)),rewrite(18(9),18(15))]. given #170 (F,wt=15): 2522 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(9(a,1),1227(a,2,2)),rewrite(103(6))]. given #171 (F,wt=15): 2545 x v (y v (z ^ (y v (x ^ u)))) = x v y. [para(2522(a,1),2(a,2)),rewrite(2(5),14(5),2(6))]. given #172 (F,wt=17): 1262 (x v y) ^ (y v ((x v z) ^ (x v u))) = x v y. [para(2(a,1),670(a,1,1)),rewrite(2(7))]. given #173 (F,wt=17): 1276 (x v y) v (z ^ (x v (u ^ (x v y)))) = x v y. [para(670(a,1),1029(a,1,2,2)),rewrite(5(3),2(4))]. given #174 (T,wt=17): 1281 x ^ (y v ((y v z) ^ (x v u))) = x ^ (y v z). [para(691(a,1),5(a,2)),rewrite(5(3),5(5))]. given #175 (A,wt=23): 169 x v ((x ^ y) v ((z ^ u) v (z ^ v))) = x v ((z ^ u) v (z ^ v)). [para(11(a,1),103(a,1,2,2)),rewrite(11(12))]. given #176 (F,wt=17): 1381 (x v y) ^ (x v ((z v y) ^ (y v u))) = x v y. [para(1345(a,1),48(a,1,2,2)),rewrite(5(6),1345(11))]. given #177 (F,wt=17): 1392 x ^ (y v ((x v z) ^ (u v y))) = x ^ (u v y). [para(1366(a,1),414(a,1,2)),rewrite(414(4)),flip(a)]. given #178 (F,wt=15): 2694 x ^ ((x v y) v ((y v z) ^ (y v u))) = x. [para(670(a,1),1392(a,1,2,2)),rewrite(2(5),8(11))]. given #179 (F,wt=15): 2706 x ^ ((x v y) v ((z v y) ^ (y v u))) = x. [para(1381(a,1),1392(a,1,2,2)),rewrite(2(5),8(11))]. given #180 (T,wt=15): 2716 x ^ (y v ((x v y) v (z ^ (y v u)))) = x. [para(48(a,1),2694(a,1,2,2)),rewrite(14(5))]. given #181 (A,wt=19): 170 x v (y v ((x ^ z) v (u ^ v))) = x v (y v (u ^ v)). [para(103(a,1),14(a,2,2)),rewrite(14(8))]. given #182 (F,wt=15): 2735 x ^ ((x v y) v ((z v u) ^ (z v v))) = x. [para(2694(a,1),1392(a,1,2,2)),rewrite(2(5),2(8),14(8),2(12),14(12),14(11),2(10),1201(11),8(12))]. given #183 (F,wt=15): 2747 x ^ ((x v y) v ((z v u) ^ (u v v))) = x. [para(2706(a,1),1392(a,1,2,2)),rewrite(2(5),2(8),14(8),2(12),14(12),14(11),2(10),1977(12),8(12))]. given #184 (F,wt=13): 2850 x ^ ((x v y) v (z ^ (u v v))) = x. [para(215(a,1),2747(a,1,2,2,1)),rewrite(2(6),1363(7))]. given #185 (F,wt=15): 2883 x ^ (y v ((x v z) v (u ^ (v v w)))) = x. [para(2850(a,1),215(a,1,1)),rewrite(2(5),9(7),2(5)),flip(a)]. given #186 (T,wt=15): 2885 x ^ ((x v y) v (z ^ (u ^ (v v w)))) = x. [para(215(a,1),2850(a,1,2,2,2))]. given #187 (A,wt=23): 171 x v ((x ^ y) v ((z ^ u) v (u ^ v))) = x v ((z ^ u) v (u ^ v)). [para(18(a,1),103(a,1,2,2)),rewrite(18(12))]. given #188 (F,wt=17): 1413 (x v (y ^ z)) ^ (x v (y v u)) = x v (y ^ z). [para(1367(a,1),300(a,1,1)),rewrite(2(5),2(6),14(6),2(5),9(8),2(5),2(6),14(6),2(5)),flip(a)]. given #189 (F,wt=17): 1468 x ^ ((y ^ (z ^ u)) v (u ^ (x v v))) = x ^ u. [para(5(a,1),724(a,1,2,1,2))]. given #190 (F,wt=17): 1506 (x v y) v (z ^ ((x ^ u) v (x ^ v))) = x v y. [para(40(a,1),1505(a,1,2,2))]. given #191 (F,wt=17): 1514 (x v (y v z)) v (y ^ (u v v)) = x v (y v z). [para(14(a,1),1507(a,1,1)),rewrite(14(7))]. given #192 (T,wt=17): 1528 (x v y) v ((y v (x ^ z)) ^ (u v v)) = x v y. [para(24(a,1),1513(a,1,1)),rewrite(24(9))]. given #193 (A,wt=25): 192 x ^ ((x ^ y) v ((x ^ z) v (x ^ u))) = (x ^ y) v ((x ^ z) v (x ^ u)). [para(34(a,1),11(a,2,1)),rewrite(24(4),9(2),5(1),5(6),40(6),2(11))]. given #194 (F,wt=17): 1590 (x v y) v (z ^ (u ^ (y v (x ^ v)))) = x v y. [para(834(a,1),1511(a,1,2))]. given #195 (F,wt=17): 1617 (x v y) v (z ^ (u ^ (x v (y ^ v)))) = x v y. [para(834(a,1),1512(a,1,2))]. given #196 (F,wt=13): 3194 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(68(a,1),1617(a,1,2,2)),rewrite(2(2),376(2),2(7),376(7))]. given #197 (F,wt=17): 1628 (x v y) v (x ^ (z ^ (u ^ (v v w)))) = x v y. [para(215(a,1),1517(a,1,2,2,2))]. given #198 (T,wt=17): 1641 (x v y) v (z ^ ((y ^ u) v (y ^ v))) = x v y. [para(31(a,1),1532(a,1,2))]. given #199 (A,wt=29): 194 x ^ (y ^ ((x ^ z) v ((x ^ u) v (x ^ v)))) = y ^ ((x ^ z) v ((x ^ u) v (x ^ v))). [para(34(a,1),31(a,2,2,1)),rewrite(24(4),9(2),5(1),5(6),40(6),2(12))]. given #200 (F,wt=17): 1644 (x v y) v (y ^ (z ^ (u ^ (v v w)))) = x v y. [para(215(a,1),1532(a,1,2,2,2))]. given #201 (F,wt=17): 1657 x ^ (y ^ ((z ^ x) v (z ^ u))) = z ^ (x ^ y). [back_rewrite(1000),rewrite(1656(6))]. given #202 (F,wt=17): 1683 x ^ ((y ^ z) v (x ^ (z v u))) = x ^ (z v u). [para(5(a,1),794(a,1,2,1))]. given #203 (F,wt=11): 3428 x v (y v (z ^ x)) = x v y. [para(1683(a,1),2111(a,1)),rewrite(14(3),2(2),5(5),440(5),14(5),2(4),5(7),440(7),14(4),2(3)),flip(a)]. given #204 (T,wt=15): 3427 (x v y) ^ (y v (z ^ x)) = y v (z ^ x). [para(2195(a,1),1683(a,1,2)),rewrite(2(2),2(4),16(5),2(4),5(6)),flip(a)]. given #205 (A,wt=29): 206 ((x ^ y) v (x ^ z)) ^ (u v (x ^ (v v ((x ^ y) v (x ^ z))))) = (x ^ y) v (x ^ z). [para(34(a,1),110(a,1,1)),rewrite(2(7),34(14))]. given #206 (F,wt=13): 3463 x v ((y v z) ^ (y v x)) = y v x. [para(1974(a,1),3427(a,1,2)),rewrite(2(2),14(2),2(1),5(4),2093(4),5(4)),flip(a)]. given #207 (F,wt=13): 3465 x v ((y v z) ^ (z v x)) = z v x. [para(2195(a,1),3427(a,1,2)),rewrite(2(2),14(2),2(1),2(3),5(4),1363(4),2(2),5(4)),flip(a)]. given #208 (F,wt=15): 3451 (x v y) ^ (z v (x v (u v y))) = x v y. [para(377(a,1),3427(a,1,2,2)),rewrite(2(3),14(3),14(2),2(1),2(4),5(5),377(8),2(6))]. given #209 (F,wt=15): 3452 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [para(318(a,1),3427(a,1,2)),rewrite(5(2),2(3),14(3),2(2),9(2),15(4),16(3),5(3)),flip(a)]. given #210 (T,wt=13): 3561 x ^ ((y ^ z) v (z ^ x)) = z ^ x. [para(760(a,1),3452(a,1,2)),rewrite(5(2),15(2),5(1),5(3),2(4),376(4),5(2),2(4)),flip(a)]. given #211 (A,wt=19): 207 x ^ (y ^ (z v (u v ((x v v) ^ (x v w))))) = x ^ y. [para(128(a,1),15(a,2,2)),rewrite(5(8))]. given #212 (F,wt=13): 3577 x v (y ^ (z ^ (x ^ (u v v)))) = x. [para(2885(a,1),3452(a,1,2)),rewrite(5(4),15(4),15(3),2(5),2(10),14(10),2(9),8(11))]. given #213 (F,wt=15): 3459 (x v y) ^ (z v (u v (x v y))) = x v y. [para(1507(a,1),3427(a,1,2)),rewrite(14(3),2(2),14(2),2(1),14(3),14(2),5(5),2(9),14(9),2(8),24(9))]. given #214 (F,wt=15): 3461 x v (y v (z ^ (x ^ (u v v)))) = x v y. [para(1517(a,1),3427(a,1,2)),rewrite(14(4),2(3),5(6),440(6),15(5),2(6),14(6),2(5)),flip(a)]. given #215 (F,wt=15): 3467 x v ((y v (z v u)) ^ (z v x)) = z v x. [para(2178(a,1),3427(a,1,2)),rewrite(2(3),14(3),14(2),2(1),2(4),5(5),3451(5),2(2),5(5)),flip(a)]. given #216 (T,wt=15): 3562 x ^ ((y ^ (z ^ u)) v (z ^ x)) = z ^ x. [para(1012(a,1),3452(a,1,2)),rewrite(5(3),15(3),15(2),5(1),5(4),2(5),1480(5),5(2),2(5)),flip(a)]. given #217 (A,wt=21): 210 x ^ (y v ((x v z) ^ (u v (v v ((x v w) ^ (x v v6)))))) = x. [para(128(a,1),74(a,1,1)),rewrite(5(7),128(15))]. given #218 (F,wt=15): 3574 x ^ ((y ^ (z ^ u)) v (u ^ x)) = u ^ x. [para(2454(a,1),3452(a,1,2)),rewrite(5(3),15(3),15(2),5(1),5(4),2(5),2412(5),5(2),2(5)),flip(a)]. given #219 (F,wt=15): 3642 x v ((x v y) ^ (z v (u v y))) = x v y. [para(2(a,1),3467(a,1,2,1,2)),rewrite(2(3),5(4),2(6))]. given #220 (F,wt=15): 3751 (x v y) ^ (x v (z v (u v y))) = x v y. [para(3642(a,1),2111(a,1,2)),rewrite(5(5),3642(10))]. given #221 (F,wt=15): 3756 x v ((y v (z v u)) ^ (u v x)) = u v x. [para(3642(a,1),3427(a,1,2)),rewrite(2(3),14(3),14(2),2(1),2(4),5(5),3459(5),2(2),5(5)),flip(a)]. given #222 (T,wt=17): 1722 x ^ ((y ^ z) v (y ^ (u v (x ^ y)))) = x ^ y. [para(34(a,1),945(a,1,2))]. given #223 (A,wt=21): 229 (x ^ (y ^ z)) v (x ^ (y ^ (z v u))) = x ^ (y ^ (z v u)). [para(39(a,1),82(a,1,2,2)),rewrite(2(6))]. given #224 (F,wt=17): 1785 x ^ ((y ^ z) v (y ^ (u v (y ^ x)))) = y ^ x. [para(987(a,1),136(a,1)),flip(a)]. given #225 (F,wt=17): 1840 (x ^ y) v (x ^ ((z ^ y) v (y ^ u))) = x ^ y. [para(1013(a,1),318(a,1,2)),rewrite(2(6),1013(12))]. given #226 (F,wt=17): 1844 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(1013(a,1),1363(a,1)),rewrite(5(4))]. given #227 (F,wt=17): 1886 (x v (y v z)) ^ (z v (x ^ u)) = z v (x ^ u). [para(2(a,1),1101(a,1,1,2))]. given #228 (T,wt=9): 3949 x ^ (y v (z v x)) = x. [para(135(a,1),1886(a,1,2)),rewrite(5(3),135(8))]. given #229 (A,wt=25): 238 (x ^ (y v z)) v (u ^ ((x ^ y) v (x ^ (v ^ (y v z))))) = x ^ (y v z). [para(39(a,1),135(a,1,2,2,1)),rewrite(5(6),15(6))]. given #230 (F,wt=17): 1887 (x v (y ^ z)) ^ (x v (u v y)) = x v (y ^ z). [para(2(a,1),1101(a,1,1)),rewrite(2(2),14(2),2(1),5(5))]. given #231 (F,wt=17): 2002 x v (y v ((x v z) ^ (z v u))) = x v (y v z). [para(1974(a,1),14(a,2,2)),rewrite(2(1),2(6),14(7))]. given #232 (F,wt=17): 2016 x v ((x v y) ^ ((y v z) ^ (y v u))) = x v y. [para(362(a,1),1974(a,1,2,2)),rewrite(2(1),2(7))]. given #233 (F,wt=17): 2026 x v ((x v (y ^ z)) ^ (y v u)) = x v (y ^ z). [para(794(a,1),1974(a,1,2)),rewrite(2(2),2(7))]. given #234 (T,wt=17): 2056 x v (y v (z ^ (u ^ (v ^ (x v y))))) = x v y. [para(834(a,1),1993(a,1,2,2,2))]. given #235 (A,wt=23): 242 (x ^ y) v ((z ^ u) v (x ^ (y v v))) = (z ^ u) v (x ^ (y v v)). [para(39(a,1),103(a,1,2,1)),rewrite(14(6),2(5),2(10))]. given #236 (F,wt=17): 2075 x v ((y v (z v u)) ^ (z v (x ^ v))) = x v z. [para(14(a,1),2006(a,1,2,1))]. given #237 (F,wt=17): 2077 x v ((y v (x ^ z)) ^ (y v (u v v))) = x v y. [para(37(a,1),2006(a,1,2,1)),rewrite(5(5))]. given #238 (F,wt=17): 2080 x v ((y v (x ^ z)) ^ (y v (u ^ v))) = x v y. [para(103(a,1),2006(a,1,2,1)),rewrite(5(5))]. given #239 (F,wt=17): 2107 (x v y) v ((x v z) ^ (z v u)) = x v (y v z). [para(2006(a,1),2006(a,1,2,2)),rewrite(2(3),5(4),2(7),14(7),2(6))]. given #240 (T,wt=17): 2133 x v (y ^ ((x ^ z) v (y ^ u))) = x v (y ^ u). [para(2013(a,1),103(a,1,2)),rewrite(103(4)),flip(a)]. given #241 (A,wt=29): 277 x ^ ((y ^ (x v z)) v ((y v x) ^ (z v (x ^ u)))) = (y ^ x) v (x ^ (z v (x ^ u))). [para(35(a,2),5(a,2)),rewrite(2(3),5(8),5(9))]. given #242 (F,wt=17): 2175 x v (y ^ ((x ^ z) v (u ^ y))) = x v (u ^ y). [para(2014(a,1),103(a,1,2)),rewrite(103(4)),flip(a)]. given #243 (F,wt=17): 2286 (x v (y ^ z)) ^ (x v (z v u)) = x v (y ^ z). [para(2111(a,1),300(a,1,1)),rewrite(2(6),14(6),2(5),9(8),2(6),14(6),2(5)),flip(a)]. given #244 (F,wt=17): 2352 (x ^ (y ^ z)) v (z ^ (y v u)) = z ^ (y v u). [para(5(a,1),1180(a,1,1)),rewrite(5(2),15(2),5(1))]. given #245 (F,wt=15): 4809 x v ((y ^ x) v (z ^ u)) = x v (z ^ u). [para(1367(a,1),2352(a,1,2)),rewrite(2(1),8(2),14(4),2(5),1369(8))]. given #246 (T,wt=17): 2355 (x ^ (y ^ z)) v (y ^ (z v u)) = y ^ (z v u). [para(15(a,1),1180(a,1,1))]. given #247 (A,wt=29): 293 x ^ ((x ^ y) v ((x ^ z) v ((z ^ (x v y)) v (y ^ (x v z))))) = (x ^ y) v (x ^ z). [para(11(a,1),271(a,1,2,2)),rewrite(2(5),2(8),2(9),14(9),2(8),14(8),2(7),14(9),14(8),2(15),11(16))]. given #248 (F,wt=17): 2381 (x ^ y) v (x ^ (z ^ (u ^ (y ^ v)))) = x ^ y. [para(724(a,1),1180(a,1,2)),rewrite(2(6),724(12))]. given #249 (F,wt=17): 2436 (x ^ y) v (z ^ (x ^ (u ^ (v ^ y)))) = x ^ y. [para(724(a,1),1181(a,1,2)),rewrite(15(4),5(3),15(3),15(2),5(1),15(4),15(3),15(2),5(5),2(6),724(12),5(7))]. given #250 (F,wt=17): 2460 x ^ ((y ^ z) v (x ^ (u v y))) = x ^ (u v y). [para(317(a,1),2454(a,1,2,2)),rewrite(2(4))]. given #251 (F,wt=17): 2496 (x ^ y) v (z ^ (x ^ (u ^ (y ^ v)))) = x ^ y. [para(724(a,1),1184(a,1,2)),rewrite(15(4),5(3),15(3),15(2),5(1),15(4),15(3),15(2),5(5),2(6),724(12),5(7))]. given #252 (T,wt=17): 2555 x v (y v (z ^ (u ^ (x v (y ^ v))))) = x v y. [para(834(a,1),2522(a,1,2,2))]. given #253 (A,wt=21): 302 (x ^ (y ^ z)) v (y ^ (u v (x ^ z))) = y ^ (u v (x ^ z)). [para(15(a,1),215(a,1,1)),rewrite(2(4),2(8))]. given #254 (F,wt=13): 5041 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(760(a,1),302(a,1,2)),rewrite(2(4),376(4),2(4)),flip(a)]. given #255 (F,wt=17): 2589 x v (y v (z ^ (u ^ (y v (x ^ v))))) = x v y. [para(834(a,1),2545(a,1,2,2))]. given #256 (F,wt=17): 2668 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(17(a,1),1381(a,1,2)),rewrite(2(4),5(8),1363(8),2(7)),flip(a)]. given #257 (F,wt=17): 2804 x v (y v (z ^ ((x ^ u) v (y ^ v)))) = x v y. [para(2545(a,1),170(a,1,2)),rewrite(24(3)),flip(a)]. given #258 (T,wt=17): 2896 x ^ (((x v y) ^ (x v z)) v (u ^ (v v w))) = x. [para(362(a,1),2850(a,1,2,1))]. given #259 (A,wt=19): 303 (x ^ y) v (x ^ (z v (x ^ y))) = x ^ (z v (x ^ y)). [para(32(a,1),215(a,1,1)),rewrite(2(3),2(7))]. given #260 (F,wt=17): 2920 x ^ (y v ((x v z) v (u ^ (v ^ (w v v6))))) = x. [para(215(a,1),2883(a,1,2,2,2,2))]. given #261 (F,wt=17): 2939 x ^ ((x v y) v (z ^ (u ^ (v ^ (w v v6))))) = x. [para(215(a,1),2885(a,1,2,2,2,2))]. given #262 (F,wt=15): 5292 x v (y ^ (z ^ (u ^ (x ^ (v v w))))) = x. [para(2939(a,1),3452(a,1,2)),rewrite(5(5),15(5),15(4),15(3),2(6),2(12),14(12),2(11),8(13))]. given #263 (F,wt=15): 5308 x v (y ^ (z ^ (x ^ (u ^ (v v w))))) = x. [para(5292(a,1),3427(a,1,2)),rewrite(2(5),3577(5),16(1),15(5),15(4),15(3)),flip(a)]. given #264 (T,wt=17): 3013 x ^ ((x ^ y) v (z ^ (u ^ (y ^ v)))) = x ^ y. [para(1468(a,1),794(a,1,2,2)),rewrite(5(3),15(3),15(2),5(1),2(5),1468(12))]. given #265 (A,wt=23): 305 (x ^ y) v (x ^ (z v (y ^ (x v u)))) = x ^ (z v (y ^ (x v u))). [para(30(a,1),215(a,1,1)),rewrite(2(4),2(9))]. given #266 (F,wt=17): 3015 (x ^ y) v (x ^ (z ^ (u ^ (v ^ y)))) = x ^ y. [para(1468(a,1),1180(a,1,2)),rewrite(2(6),1468(12))]. given #267 (F,wt=17): 3017 (x ^ y) v (z ^ (u ^ (x ^ (v ^ y)))) = x ^ y. [para(1468(a,1),1181(a,1,2)),rewrite(15(4),5(3),15(3),15(2),5(1),15(4),15(3),15(2),5(5),2(6),1468(12),5(7))]. given #268 (F,wt=17): 3019 (x ^ y) v (z ^ (u ^ (x ^ (y ^ v)))) = x ^ y. [para(1468(a,1),1184(a,1,2)),rewrite(15(4),5(3),15(3),15(2),5(1),15(4),15(3),15(2),5(5),2(6),1468(12),5(7))]. given #269 (F,wt=17): 3364 x ^ (y ^ ((z ^ u) v (z ^ x))) = z ^ (x ^ y). [para(1010(a,1),1657(a,1,2,2,1)),rewrite(15(8),1025(7),15(2),5(1),5(6)),flip(a)]. given #270 (T,wt=17): 3426 x v ((x v (y ^ z)) ^ (z v u)) = x v (y ^ z). [para(1683(a,1),1974(a,1,2)),rewrite(2(2),2(7))]. given #271 (A,wt=29): 306 (x ^ (y ^ z)) v (x ^ (u v (y ^ (z ^ (x v v))))) = x ^ (u v (y ^ (z ^ (x v v)))). [para(41(a,1),215(a,1,1)),rewrite(2(6),2(12))]. given #272 (F,wt=17): 3429 (x v (y v z)) ^ (y v (u ^ x)) = y v (u ^ x). [para(2178(a,1),1683(a,1,2)),rewrite(2(2),2(4),16(5),2(4),5(7)),flip(a)]. given #273 (F,wt=17): 3436 x ^ ((x ^ y) v (z ^ (u ^ (v ^ y)))) = x ^ y. [para(1468(a,1),1683(a,1,2,2)),rewrite(2(5),1468(12))]. given #274 (F,wt=17): 3455 (x ^ (y ^ z)) v (y ^ (u v x)) = y ^ (u v x). [para(608(a,1),3427(a,1,2)),rewrite(15(3),2(4),14(4),2(3),9(3),15(4),16(3),15(4)),flip(a)]. given #275 (F,wt=17): 3474 x v (y v (z ^ (u ^ (x ^ (v v w))))) = x v y. [para(1628(a,1),3427(a,1,2)),rewrite(14(5),2(4),5(7),440(7),15(6),15(5),2(7),14(7),2(6)),flip(a)]. given #276 (T,wt=17): 3491 x v (y v ((x v z) ^ (u v z))) = x v (y v z). [para(3465(a,1),14(a,2,2)),rewrite(2(2),5(3),2(6),14(7))]. given #277 (A,wt=21): 324 (x ^ (y ^ z)) v (x ^ (y ^ (u v z))) = x ^ (y ^ (u v z)). [para(262(a,1),82(a,1,2,2)),rewrite(2(6))]. given #278 (F,wt=17): 3565 x ^ ((y ^ z) v ((y ^ u) v (y ^ x))) = y ^ x. [para(699(a,1),3452(a,1,2)),rewrite(5(4),5(5),2(6),147(6),5(2),14(6),2(5)),flip(a)]. given #279 (F,wt=17): 3569 x ^ ((y ^ z) v ((z ^ u) v (z ^ x))) = z ^ x. [para(1013(a,1),3452(a,2)),rewrite(5(4),5(5),14(9),2(8),400(11),5(7))]. given #280 (F,wt=17): 3576 (x v y) ^ (y v ((z v x) ^ (x v u))) = x v y. [para(1381(a,1),3452(a,1,2)),rewrite(2(4),834(5),2(6),2(7),2412(7),2(2)),flip(a)]. given #281 (F,wt=17): 3582 x ^ ((y ^ x) v ((y ^ z) v (y ^ u))) = y ^ x. [back_rewrite(3568),rewrite(5(2),147(6),5(2),2(5),14(6)),flip(a)]. given #282 (T,wt=17): 3608 x ^ (y ^ ((z ^ u) v (u ^ x))) = u ^ (x ^ y). [para(3561(a,1),1657(a,1,2,2,1)),rewrite(15(8),3591(7),15(2),5(1),5(6)),flip(a)]. given #283 (A,wt=25): 329 (x ^ (y v z)) v (u ^ ((x ^ z) v (x ^ (v ^ (y v z))))) = x ^ (y v z). [para(262(a,1),135(a,1,2,2,1)),rewrite(5(6),15(6))]. given #284 (F,wt=15): 5705 x ^ (y ^ (z ^ (u v x))) = x ^ (y ^ z). [para(608(a,1),3608(a,1,2,2)),rewrite(834(4),317(4),15(3),5(4),834(4),834(3),5(7),15(8),834(7),317(7),15(6))]. given #285 (F,wt=17): 3644 x v ((x v y) ^ (z v (u v (y v v)))) = x v y. [para(14(a,1),3467(a,1,2,1,2)),rewrite(2(4),5(5),2(7))]. given #286 (F,wt=17): 3653 (x v y) ^ (z v (x v (u v (y v v)))) = x v y. [para(3467(a,1),1101(a,1,2)),rewrite(14(4),2(3),14(3),14(2),2(1),14(4),14(3),14(2),5(6),3467(11))]. given #287 (F,wt=17): 3770 x v ((x v (y ^ z)) ^ (u v y)) = x v (y ^ z). [para(9(a,1),3756(a,1,2,1,2)),rewrite(2(3),5(4),2(7))]. given #288 (T,wt=17): 3793 (x v y) ^ (z v (u v (x v (y v v)))) = x v y. [para(3756(a,1),1101(a,1,2)),rewrite(14(4),2(3),14(3),14(2),2(1),14(4),14(3),14(2),5(6),3756(11))]. given #289 (A,wt=23): 330 (x ^ y) v ((z ^ u) v (x ^ (v v y))) = (z ^ u) v (x ^ (v v y)). [para(262(a,1),103(a,1,2,1)),rewrite(14(6),2(5),2(10))]. given #290 (F,wt=17): 3813 (x v y) ^ (x v (z v (u v (y v v)))) = x v y. [para(3756(a,1),1413(a,2)),rewrite(2(3),5(4),3642(5),2(4),14(4),14(3),2(2),2(7))]. given #291 (F,wt=17): 3821 x ^ ((y ^ z) v (z ^ (u v (x ^ z)))) = x ^ z. [para(5(a,1),1722(a,1,2,1))]. given #292 (F,wt=17): 3939 (x ^ y) v (y ^ ((z ^ x) v (x ^ u))) = x ^ y. [para(1840(a,1),3427(a,1,2)),rewrite(5(4),2(5),14(5),2(4),5(6),5(7),834(7),3569(6),32(2),5(2)),flip(a)]. given #293 (F,wt=17): 3941 (x v (y v z)) ^ (y v (z ^ u)) = y v (z ^ u). [para(2(a,1),1886(a,1,1)),rewrite(2(2),14(2),2(1))]. given #294 (T,wt=15): 5896 x ^ ((y v x) ^ (z v u)) = x ^ (z v u). [para(215(a,1),3941(a,1,2)),rewrite(2(2),9(2),15(4),215(8))]. given #295 (A,wt=19): 337 ((x ^ y) v (x ^ z)) ^ ((x ^ z) v (y ^ z)) = x ^ z. [back_rewrite(216),rewrite(317(8),317(7))]. given #296 (F,wt=15): 5937 x v (y ^ (z v (x v (y v u)))) = x v y. [para(3941(a,1),305(a,1,2)),rewrite(5(3),3949(3),2(3),14(3),14(2),2(1),14(6),9(5),2(6),14(6),14(5),2(4),3941(9)),flip(a)]. given #297 (F,wt=15): 6006 x v (y ^ (x v (z v (y v u)))) = x v y. [para(5(a,1),5937(a,1,2)),rewrite(14(3),5(4))]. given #298 (F,wt=17): 3943 (x v (y v z)) ^ (z v (y ^ u)) = z v (y ^ u). [para(14(a,1),1886(a,1,1))]. given #299 (F,wt=17): 3987 (x v y) ^ (z v (x v (u v (v v y)))) = x v y. [para(3467(a,1),1886(a,1,2)),rewrite(14(4),2(3),14(3),14(2),2(1),14(4),14(3),14(2),5(6),3467(11))]. given #300 (T,wt=17): 3988 (x v y) ^ (z v (u v (x v (v v y)))) = x v y. [para(3756(a,1),1886(a,1,2)),rewrite(14(4),2(3),14(3),14(2),2(1),14(4),14(3),14(2),5(6),3756(11))]. given #301 (A,wt=23): 369 (x ^ y) v ((x v z) ^ (u v (x ^ y))) = (x v z) ^ (u v (x ^ y)). [para(57(a,1),300(a,1,1)),rewrite(2(4),2(9))]. given #302 (F,wt=17): 4102 x v ((y v z) ^ ((y v u) ^ (y v x))) = y v x. [para(2016(a,1),3427(a,1,2)),rewrite(2(4),2(5),5(6),1262(6),2(2),5(6),834(6)),flip(a)]. given #303 (F,wt=17): 4126 x v ((y v z) ^ (x v (y ^ u))) = x v (y ^ u). [para(2026(a,1),3427(a,1,2)),rewrite(2(2),14(2),2(1),1886(5),5(6)),flip(a)]. given #304 (F,wt=17): 4223 x v ((y v (z v u)) ^ (u v (x ^ v))) = x v u. [para(2(a,1),2075(a,1,2,1,2))]. given #305 (F,wt=17): 4361 x v (y v ((z v x) ^ (z v u))) = z v (x v y). [para(1974(a,1),2107(a,1,1)),rewrite(2267(5),2(6)),flip(a)]. given #306 (T,wt=17): 4394 x v (y v ((z v u) ^ (z v x))) = z v (x v y). [para(2107(a,1),3427(a,1,2)),rewrite(14(3),2(2),14(2),2(1),14(3),14(2),2(4),14(5),5(6),2093(6),2(4),5(6),2(7),14(7),2(6)),flip(a)]. given #307 (A,wt=23): 370 (x ^ y) v ((y v z) ^ (u v (x ^ y))) = (y v z) ^ (u v (x ^ y)). [para(62(a,1),300(a,1,1)),rewrite(2(4),2(9))]. given #308 (F,wt=17): 4505 x v (y v ((x v (y ^ z)) ^ (u v v))) = x v y. [back_rewrite(3067),rewrite(4402(6))]. given #309 (F,wt=15): 6398 x v (y v ((x v y) ^ (z v u))) = x v y. [para(8(a,1),4505(a,1,2,2,1,2))]. given #310 (F,wt=17): 4561 x v (y v (z ^ (y v (u ^ (x v y))))) = x v y. [back_rewrite(2235),rewrite(4402(6))]. given #311 (F,wt=17): 4608 x v (y v ((y v (x ^ z)) ^ (u v v))) = x v y. [back_rewrite(1528),rewrite(4402(6))]. given #312 (T,wt=17): 4615 x v (y v (z ^ (x v (u ^ (x v y))))) = x v y. [back_rewrite(1276),rewrite(4402(6))]. given #313 (A,wt=27): 371 (x ^ y) v ((z v (x ^ y)) ^ (u v (x ^ y))) = (z v (x ^ y)) ^ (u v (x ^ y)). [para(69(a,1),300(a,1,1)),rewrite(2(5),2(11))]. given #314 (F,wt=17): 4623 x v (y ^ ((y ^ z) v (x ^ u))) = x v (y ^ z). [para(2133(a,1),2(a,2)),rewrite(2(3),2(5))]. given #315 (F,wt=17): 4821 (x ^ y) v (z ^ (u ^ (v ^ (x ^ y)))) = x ^ y. [para(1468(a,1),2352(a,1,2)),rewrite(5(3),15(3),15(2),5(1),5(5),2(6),1468(12),5(7))]. given #316 (F,wt=17): 5087 x v ((y ^ z) v (z ^ (x ^ u))) = x v (y ^ z). [para(5041(a,1),1617(a,1,2,2)),rewrite(2(2),5(3),15(4),5(3),2(5),14(5),2(4),2(7))]. given #317 (F,wt=17): 5137 x v ((x v y) ^ ((z v y) ^ (y v u))) = x v y. [para(2668(a,1),3463(a,1,2,1)),rewrite(2(4),5(5),2(7))]. given #318 (T,wt=17): 5335 x ^ ((y ^ (z ^ (u ^ v))) v (u ^ x)) = u ^ x. [para(3013(a,1),3452(a,1,2)),rewrite(5(4),15(4),15(3),15(2),5(1),5(5),2(6),3017(6),5(2),2(6)),flip(a)]. given #319 (A,wt=29): 373 (x ^ (y ^ z)) v ((y v u) ^ (v v (x ^ (y ^ z)))) = (y v u) ^ (v v (x ^ (y ^ z))). [para(64(a,1),300(a,1,1)),rewrite(2(6),2(12))]. given #320 (F,wt=11): 6661 x v (y ^ (z ^ (x ^ u))) = x. [para(5937(a,1),5335(a,1,2)),rewrite(14(5),2(4),2(10),5(11),3451(11),14(9),2(8),377(11))]. given #321 (F,wt=13): 6662 x v (y v (z ^ (x ^ u))) = x v y. [para(8(a,1),373(a,1,2)),rewrite(14(4),2(3),2(9),14(9),2(8),440(10))]. given #322 (F,wt=15): 6672 (x v y) v (z ^ (x ^ (u v v))) = x v y. [para(2885(a,1),373(a,1,2)),rewrite(2(5),2(8),14(8),2(7),2(12),14(12),14(11),2(10),440(13))]. given #323 (F,wt=17): 5362 x ^ (y ^ (z v ((x v u) ^ (y v v)))) = x ^ y. [para(305(a,1),747(a,1,2))]. given #324 (T,wt=17): 5492 x v (y ^ (z ^ (x v (y v u)))) = x v (y ^ z). [para(1369(a,1),306(a,1,2)),rewrite(5(3),834(3),317(3),2(3),14(3),2(2),14(7),82(6),2(5),14(5),2(4),1369(9)),flip(a)]. given #325 (A,wt=29): 375 x v ((x v y) ^ (z v ((x v u) ^ (x v v)))) = (x v y) ^ (z v ((x v u) ^ (x v v))). [para(111(a,1),300(a,1,1)),rewrite(5(6),5(13))]. given #326 (F,wt=17): 5540 x ^ ((y ^ (z ^ (u ^ v))) v (v ^ x)) = v ^ x. [para(3436(a,1),3452(a,1,2)),rewrite(5(4),15(4),15(3),15(2),5(1),5(5),2(6),4821(6),5(2),2(6)),flip(a)]. given #327 (F,wt=11): 6883 x v (y ^ (z ^ (u ^ x))) = x. [para(5937(a,1),5540(a,1,2)),rewrite(14(5),2(4),2(10),5(11),3451(11),14(9),2(8),377(11))]. given #328 (F,wt=17): 5562 x v (y ^ (z ^ (u ^ (x ^ (v ^ (w v v6)))))) = x. [para(2939(a,1),3455(a,1,2)),rewrite(5(6),15(6),15(5),15(4),834(3),2(7),2(13),14(13),2(12),8(14))]. given #329 (F,wt=17): 5624 x ^ ((y ^ z) v ((y ^ x) v (y ^ u))) = y ^ x. [para(3565(a,1),300(a,1,2)),rewrite(5(2),15(2),5(1),2(4),406(4),2(5)),flip(a)]. given #330 (T,wt=17): 5663 x ^ ((y ^ z) v ((z ^ x) v (z ^ u))) = z ^ x. [para(3569(a,1),300(a,1,2)),rewrite(5(2),15(2),5(1),2(4),376(4),2(5)),flip(a)]. given #331 (A,wt=29): 378 (x ^ (y ^ z)) v ((z v u) ^ (v v (x ^ (y ^ z)))) = (z v u) ^ (v v (x ^ (y ^ z))). [para(105(a,1),300(a,1,1)),rewrite(2(6),2(12))]. given #332 (F,wt=13): 6910 x v (y v (z ^ (u ^ x))) = x v y. [para(8(a,1),378(a,1,2)),rewrite(14(4),2(3),2(9),14(9),2(8),440(10))]. given #333 (F,wt=17): 5754 x v ((y v (z v (u v v))) ^ (u v x)) = u v x. [para(3644(a,1),3427(a,1,2)),rewrite(2(4),14(4),14(3),14(2),2(1),2(5),5(6),3988(6),2(2),5(6)),flip(a)]. given #334 (F,wt=17): 5811 x v ((y v z) ^ (x v (z ^ u))) = x v (z ^ u). [para(3770(a,1),3427(a,1,2)),rewrite(2(2),14(2),2(1),3943(5),5(6)),flip(a)]. given #335 (F,wt=17): 5837 (x ^ (y ^ z)) v (x ^ (u v z)) = x ^ (u v z). [para(1180(a,1),330(a,2)),rewrite(2(4),242(7),2(6))]. given #336 (T,wt=17): 5861 x ^ ((y ^ z) v (z ^ (u v (z ^ x)))) = z ^ x. [para(3821(a,1),5(a,2)),rewrite(5(2),5(6),5(7))]. given #337 (A,wt=23): 380 (x ^ y) v (y ^ (z v (x ^ (y v u)))) = y ^ (z v (x ^ (y v u))). [para(214(a,1),300(a,1,1)),rewrite(376(3),2(4),376(8),2(9))]. given #338 (F,wt=17): 6052 (x v y) ^ (z v (u v (v v (x v y)))) = x v y. [para(3756(a,1),3943(a,1,2)),rewrite(2(3),14(3),14(2),2(1),5(6),3756(11))]. given #339 (F,wt=17): 6128 x v ((y v x) ^ ((y v z) ^ (y v u))) = y v x. [para(4102(a,1),2(a,1)),rewrite(5(5),15(6),2(7)),flip(a)]. given #340 (F,wt=17): 6135 x v ((y v z) ^ ((y v x) ^ (y v u))) = y v x. [para(4102(a,1),1367(a,1,2)),rewrite(2(2),14(2),2(1),5(4),2093(4),5(5)),flip(a)]. given #341 (F,wt=17): 6304 x v (y v ((z v u) ^ (u v x))) = u v (x v y). [para(3465(a,1),4361(a,1,2,2,1)),rewrite(14(8),3506(7),14(2),2(1),2(6)),flip(a)]. given #342 (T,wt=17): 6307 x v ((x v y) ^ (z v (u v (v v y)))) = x v y. [para(4361(a,2),3467(a,1,2,1,2)),rewrite(2(1),2002(5),2(4),5(5),2(7))]. given #343 (A,wt=21): 381 (x ^ (y ^ z)) v (x ^ (z ^ (y v u))) = x ^ (z ^ (y v u)). [para(300(a,1),215(a,1,2,2)),rewrite(300(10))]. given #344 (F,wt=17): 6443 x v (y v (z ^ ((x v y) ^ (u v v)))) = x v y. [para(215(a,1),6398(a,1,2,2,2)),rewrite(15(4))]. given #345 (F,wt=17): 6493 x v ((y v z) ^ (y v (u ^ (x v y)))) = x v y. [para(362(a,1),4561(a,1,2))]. given #346 (F,wt=17): 6513 x v ((y v z) ^ (z v (u ^ (x v z)))) = x v z. [para(2668(a,1),4561(a,1,2))]. given #347 (F,wt=17): 6630 x v ((y v z) ^ ((z v u) ^ (z v x))) = z v x. [para(5137(a,1),3427(a,1,2)),rewrite(2(4),2(5),5(6),3576(6),2(2),5(6),834(6)),flip(a)]. given #348 (T,wt=17): 7338 (x v y) ^ (x v (z v (u v (v v y)))) = x v y. [para(6307(a,1),2111(a,1,2)),rewrite(5(6),6307(12))]. given #349 (A,wt=21): 382 (x ^ (y ^ z)) v (y ^ (z ^ (x v u))) = y ^ (z ^ (x v u)). [para(300(a,1),300(a,1,2,2)),rewrite(5(2),15(2),5(1),15(5),300(10),15(9))]. given #350 (F,wt=17): 7340 x v ((y v (z v (u v v))) ^ (v v x)) = v v x. [para(6307(a,1),3427(a,1,2)),rewrite(2(4),14(4),14(3),14(2),2(1),2(5),5(6),6052(6),2(2),5(6)),flip(a)]. given #351 (F,wt=17): 7424 x v ((y v z) ^ (y v (u ^ (y v x)))) = y v x. [para(6493(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. given #352 (F,wt=17): 7456 x v ((y v z) ^ (z v (u ^ (z v x)))) = z v x. [para(6513(a,1),2(a,2)),rewrite(2(2),2(6),2(7))]. given #353 (F,wt=17): 7490 x v ((y v z) ^ ((z v x) ^ (z v u))) = z v x. [para(6630(a,1),1367(a,1,2)),rewrite(2(2),14(2),2(1),5(4),1363(4),5(5)),flip(a)]. given #354 (T,wt=19): 401 (x ^ (y v z)) v (x ^ (y v (z ^ u))) = x ^ (y v z). [para(24(a,1),318(a,1,2,2)),rewrite(2(4),2(6),14(9),9(8))]. given #355 (A,wt=27): 391 (x ^ y) v ((y ^ (z v x)) v (z ^ (x v y))) = (y ^ (z v x)) v (z ^ (x v y)). [para(11(a,1),376(a,1,2)),rewrite(2(3),2(5),5(7),2(8),2(9),14(9),2(8),14(8),2(7),242(8),14(7),2(10),2(12))]. given #356 (F,wt=19): 408 (x v y) ^ ((y ^ z) v (y ^ u)) = (y ^ z) v (y ^ u). [para(2(a,1),40(a,1,1))]. given #357 (F,wt=19): 422 (x ^ y) v (x ^ (z v (y v u))) = x ^ (z v (y v u)). [para(377(a,1),406(a,1,2,2)),rewrite(2(5))]. given #358 (F,wt=19): 423 (x ^ (y ^ z)) v (x ^ (y ^ (u ^ z))) = x ^ (y ^ z). [para(406(a,1),318(a,1,2,2)),rewrite(2(6),406(10))]. given #359 (F,wt=19): 441 x ^ (y ^ ((x v z) ^ (u v v))) = x ^ (y ^ (u v v)). [para(414(a,1),15(a,2,2)),rewrite(15(8))]. given #360 (T,wt=19): 462 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(14(a,1),440(a,1,1)),rewrite(2(4),14(4),2(3),14(5),14(8))]. given #361 (A,wt=27): 392 (x ^ y) v ((x ^ (z v y)) v (z ^ (x v y))) = (x ^ (z v y)) v (z ^ (x v y)). [para(18(a,1),376(a,1,2)),rewrite(2(3),2(5),5(7),2(8),2(9),14(9),2(8),14(8),2(7),330(8),14(7),2(10),2(12))]. given #362 (F,wt=15): 7861 x v (y v (z v (u ^ x))) = x v (y v z). [para(462(a,1),2352(a,1,2)),rewrite(8(3),14(4),14(3),2(2),462(10))]. given #363 (F,wt=19): 468 (x v (y ^ z)) ^ (x v (y ^ (z v u))) = x v (y ^ z). [para(215(a,1),440(a,1,2,2))]. given #364 (F,wt=19): 471 (x v (y ^ z)) ^ (x v (z ^ (y v u))) = x v (y ^ z). [para(300(a,1),440(a,1,2,2))]. given #365 (F,wt=19): 497 x ^ (y ^ (z ^ (u v (v v (x ^ z))))) = x ^ (y ^ z). [para(457(a,1),15(a,2,2)),rewrite(15(8))]. given #366 (T,wt=19): 607 ((x ^ y) v (y ^ z)) ^ ((x ^ z) v (y ^ z)) = y ^ z. [para(47(a,1),39(a,1,1)),rewrite(5(2),317(6),2(7),15(9),605(9),30(7),2(6),317(10))]. given #367 (A,wt=25): 394 (x v (y v z)) ^ (y v (u ^ (x v (y v z)))) = y v (u ^ (x v (y v z))). [para(377(a,1),18(a,2,1)),rewrite(14(5),26(4),2(8),14(8),14(7),2(6),377(9),2(6),5(10))]. given #368 (F,wt=19): 665 (x v y) ^ (y v (z ^ (x v y))) = y v (z ^ (x v y)). [para(2(a,1),48(a,1,1)),rewrite(2(2),2(6))]. given #369 (F,wt=19): 674 (x v y) ^ (x v (z v ((y v u) ^ (y v v)))) = x v y. [para(128(a,1),48(a,1,2,2)),rewrite(5(7),128(13))]. given #370 (F,wt=19): 677 (x v (y ^ z)) ^ (x v (y ^ (u v z))) = x v (y ^ z). [para(323(a,1),48(a,1,2,2)),rewrite(5(6),323(11))]. given #371 (F,wt=19): 684 x ^ (y ^ (z v (x ^ (z v u)))) = x ^ (y ^ (z v u)). [para(678(a,1),15(a,2,2)),rewrite(15(8))]. given #372 (T,wt=19): 701 x ^ ((x ^ (y ^ z)) v (y ^ (z ^ u))) = x ^ (y ^ z). [para(15(a,1),696(a,1,2,1)),rewrite(15(2),5(4),15(4),5(3))]. given #373 (A,wt=27): 397 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v (z v u)))))). [para(377(a,1),38(a,1,2,1,2)),rewrite(2(4),14(4),2(3),26(5),2(12)),flip(a)]. given #374 (F,wt=19): 703 x ^ ((x ^ y) v (z ^ ((y ^ u) v (y ^ v)))) = x ^ y. [para(31(a,1),696(a,1,2,2))]. given #375 (F,wt=19): 721 x ^ ((y ^ z) v ((y ^ u) v (y ^ (x v v)))) = x ^ y. [para(11(a,1),711(a,1,2,1)),rewrite(2(6),14(6),2(5))]. given #376 (F,wt=19): 723 x ^ (y ^ ((z ^ u) v (z ^ (x v v)))) = x ^ (y ^ z). [para(711(a,1),15(a,2,2)),rewrite(15(8))]. given #377 (F,wt=19): 727 x ^ ((y ^ z) v ((z ^ u) v (z ^ (x v v)))) = x ^ z. [para(18(a,1),711(a,1,2,1)),rewrite(2(6),14(6),2(5))]. given #378 (T,wt=19): 761 x ^ (y ^ ((z ^ u) v (u ^ (x v v)))) = x ^ (y ^ u). [para(720(a,1),15(a,2,2)),rewrite(15(8))]. given #379 (A,wt=27): 398 x ^ ((y ^ (x v z)) v (z ^ ((x v y) ^ (x v (z v u))))) = (x ^ z) v (x ^ y). [para(377(a,1),38(a,1,2,2,2,2)),rewrite(2(8),2(12))]. given #380 (F,wt=19): 764 x ^ ((y ^ z) v ((x v u) ^ (y v v))) = x ^ (y v v). [para(57(a,1),720(a,1,2,1)),rewrite(5(4))]. given #381 (F,wt=19): 765 x ^ ((y ^ z) v ((x v u) ^ (z v v))) = x ^ (z v v). [para(62(a,1),720(a,1,2,1)),rewrite(5(4))]. given #382 (F,wt=19): 802 x ^ (y v (x ^ (z v (y v u)))) = x ^ (z v (y v u)). [para(377(a,1),760(a,1,2,2)),rewrite(2(4))]. given #383 (F,wt=19): 833 x ^ (y ^ (z ^ (u v (x ^ (y ^ z))))) = x ^ (y ^ z). [back_rewrite(476),rewrite(814(8),814(7),822(8))]. given #384 (T,wt=19): 848 x ^ (y ^ (z v (u v (y ^ (v v (x ^ y)))))) = x ^ y. [back_rewrite(776),rewrite(834(7))]. given #385 (A,wt=21): 400 (x ^ (y v z)) v (x ^ (y v (z v u))) = x ^ (y v (z v u)). [para(14(a,1),318(a,1,2,2)),rewrite(2(3),14(8),2(7))]. given #386 (F,wt=19): 851 x ^ (y ^ ((x ^ (y ^ z)) v (z ^ u))) = x ^ (y ^ z). [back_rewrite(767),rewrite(5(4),834(6))]. given #387 (F,wt=17): 8613 x ^ (y ^ ((x ^ y) v (z ^ (y v u)))) = x ^ y. [para(8(a,1),851(a,1,2,2,1,2)),rewrite(5(3),8(8))]. given #388 (F,wt=15): 8718 x ^ (y ^ ((x ^ y) v (z ^ u))) = x ^ y. [para(3770(a,1),8613(a,1,2,2))]. given #389 (F,wt=17): 8735 x ^ (y ^ (z v ((x ^ y) v (u ^ v)))) = x ^ y. [para(1367(a,1),8718(a,1,2,2,2)),rewrite(14(4))]. given #390 (T,wt=19): 860 x ^ (y ^ (z v (u v (x ^ (v v (x ^ y)))))) = x ^ y. [back_rewrite(737),rewrite(834(7))]. given #391 (A,wt=25): 402 (x ^ (y v (z v u))) v (x ^ (y v (z v (u ^ v)))) = x ^ (y v (z v u)). [para(37(a,1),318(a,1,2,2)),rewrite(14(6),2(5),2(8),14(12),14(11),9(10))]. given #392 (F,wt=19): 913 x ^ (y ^ (z v (u v (v v (y ^ (x v w)))))) = x ^ y. [back_rewrite(575),rewrite(834(7))]. given #393 (F,wt=19): 921 x ^ (y ^ (z v (x ^ (u v (v v (x ^ y)))))) = x ^ y. [back_rewrite(543),rewrite(834(7))]. given #394 (F,wt=19): 935 x ^ (y ^ (z ^ (u v (x ^ (z v v))))) = x ^ (y ^ z). [back_rewrite(525),rewrite(834(6),834(5))]. given #395 (F,wt=19): 936 x ^ (y ^ (z ^ (u v (x ^ (y v v))))) = x ^ (y ^ z). [back_rewrite(523),rewrite(834(6),834(5))]. given #396 (T,wt=19): 941 x ^ (y ^ (z v (y ^ (u v (v v (x ^ y)))))) = x ^ y. [back_rewrite(501),rewrite(834(7))]. given #397 (A,wt=25): 405 (x ^ (y v (z ^ u))) v (x ^ ((y ^ v) v (z ^ u))) = x ^ (y v (z ^ u)). [para(103(a,1),318(a,1,2,2)),rewrite(2(8),103(12))]. given #398 (F,wt=19): 963 x ^ (y ^ (z v (y ^ (u v (x ^ (y v v)))))) = x ^ y. [back_rewrite(384),rewrite(834(7))]. given #399 (F,wt=19): 986 x ^ (y ^ (z v (x ^ (u v (y ^ (x v v)))))) = x ^ y. [back_rewrite(200),rewrite(834(7))]. given #400 (F,wt=19): 993 x ^ (y ^ (z ^ (u v (z ^ (x v v))))) = x ^ (y ^ z). [back_rewrite(181),rewrite(834(6),834(5))]. given #401 (F,wt=19): 1003 x ^ (y ^ (z v ((y v u) ^ (v v (x ^ y))))) = x ^ y. [back_rewrite(122),rewrite(834(7))]. given #402 (T,wt=19): 1005 x ^ (y ^ (z v ((x v u) ^ (v v (x ^ y))))) = x ^ y. [back_rewrite(120),rewrite(834(7))]. given #403 (A,wt=27): 409 (x v y) ^ ((x ^ z) v ((x ^ u) v (x ^ v))) = (x ^ z) v ((x ^ u) v (x ^ v)). [para(11(a,1),40(a,1,2,1)),rewrite(2(6),14(6),2(5),11(13),2(12),14(12),2(11))]. given #404 (F,wt=19): 1007 x ^ (y ^ (z v (y ^ ((x v u) ^ (x v v))))) = x ^ y. [back_rewrite(115),rewrite(834(5),834(7))]. given #405 (F,wt=19): 1020 ((x ^ y) v (x ^ z)) ^ ((x ^ y) v (y ^ u)) = x ^ y. [para(696(a,1),1010(a,1,2,2)),rewrite(2(6),5(7),696(11))]. given #406 (F,wt=19): 1025 ((x ^ y) v (x ^ z)) ^ ((x ^ z) v (z ^ u)) = x ^ z. [para(1010(a,1),1010(a,1,2,2)),rewrite(2(6),1010(11))]. given #407 (F,wt=19): 1043 x v (y v (z ^ (u ^ ((x ^ v) v (x ^ w))))) = x v y. [para(834(a,1),139(a,1,2,2))]. given #408 (T,wt=19): 1117 x ^ ((x ^ (y v z)) v (y ^ (u v v))) = x ^ (y v z). [para(414(a,1),1012(a,1,2,2))]. given #409 (A,wt=21): 410 (x v (y v z)) ^ ((y ^ u) v (y ^ v)) = (y ^ u) v (y ^ v). [para(14(a,1),40(a,1,1))]. given #410 (F,wt=13): 9331 x ^ (y ^ (z v (x v u))) = x ^ y. [para(17(a,1),410(a,1,2)),rewrite(5(4),834(4),17(7))]. given #411 (F,wt=17): 9335 x ^ ((y v (x v z)) ^ (u v v)) = x ^ (u v v). [para(215(a,1),410(a,1,2)),rewrite(15(5),215(9))]. given #412 (F,wt=17): 9339 x ^ (y ^ (z ^ (u v (x v v)))) = x ^ (y ^ z). [para(101(a,1),410(a,1,2)),rewrite(5(5),834(5),834(4),101(11))]. given #413 (F,wt=19): 1125 x v (y ^ (z ^ ((x ^ u) v ((x ^ v) v (x ^ w))))) = x. [para(11(a,1),1029(a,1,2,2,2,1)),rewrite(2(5),14(5),2(4))]. given #414 (T,wt=19): 1146 (x ^ (y v z)) v (x ^ (y ^ (u v v))) = x ^ (y v z). [para(414(a,1),1114(a,1,2,2))]. given #415 (A,wt=21): 411 (x ^ (y v z)) v (x ^ ((y ^ u) v (y ^ v))) = x ^ (y v z). [para(40(a,1),82(a,1,2,2))]. given #416 (F,wt=19): 1151 x ^ (y ^ ((x ^ (y ^ z)) v (u ^ z))) = x ^ (y ^ z). [para(1114(a,1),720(a,1,2,2,2)),rewrite(15(4),5(3),2(5),834(6),5(8),15(8),5(7))]. given #417 (F,wt=19): 1172 x ^ (y v (z v (u v (v v ((x v w) ^ (x v v6)))))) = x. [para(208(a,1),215(a,1,1)),rewrite(2(7),14(7),14(6),14(5),9(9),2(7),14(7),14(6),14(5)),flip(a)]. given #418 (F,wt=19): 1183 (x ^ (y ^ (z ^ u))) v (x ^ (z v v)) = x ^ (z v v). [para(15(a,1),304(a,1,1,2))]. given #419 (F,wt=11): 9544 x ^ (y v (z v (x v u))) = x. [para(1183(a,1),5754(a,1)),rewrite(15(8),5(9),834(9),834(8),9(10),5(4),15(9),5(10),834(10),834(9),9(11))]. given #420 (T,wt=11): 9545 x ^ (y v (z v (u v x))) = x. [para(1183(a,1),7340(a,1)),rewrite(15(8),5(9),834(9),834(8),9(10),5(4),15(9),5(10),834(10),834(9),9(11))]. given #421 (A,wt=27): 418 (x ^ (y ^ (z ^ u))) v (x ^ (y ^ (z ^ (u v v)))) = x ^ (y ^ (z ^ (u v v))). [para(41(a,1),406(a,1,2,2)),rewrite(15(6),5(5),2(8))]. given #422 (F,wt=19): 1202 (x ^ y) v ((x v z) ^ (x v u)) = (x v z) ^ (x v u). [para(362(a,1),24(a,2)),rewrite(2(5),1201(6))]. given #423 (F,wt=19): 1207 x ^ (y v (z v ((x v u) ^ ((x v v) ^ (x v w))))) = x. [para(362(a,1),128(a,1,2,2,2,1)),rewrite(834(5))]. given #424 (F,wt=19): 1212 x ^ ((y ^ z) v (y ^ ((x v u) ^ (x v v)))) = x ^ y. [para(362(a,1),711(a,1,2,2,2))]. given #425 (F,wt=19): 1213 x ^ ((y ^ z) v (z ^ ((x v u) ^ (x v v)))) = x ^ z. [para(362(a,1),720(a,1,2,2,2))]. given #426 (T,wt=19): 1214 x ^ (y ^ (z v (x ^ ((y v u) ^ (y v v))))) = x ^ y. [para(362(a,1),972(a,1,2,2,2,2))]. given #427 (A,wt=25): 419 (x ^ (y ^ z)) v (x ^ (u v (y ^ (z v v)))) = x ^ (u v (y ^ (z v v))). [para(74(a,1),406(a,1,2,2)),rewrite(5(5),2(7))]. given #428 (F,wt=19): 1350 x ^ (y v ((z v x) ^ (u v ((x v v) ^ (x v w))))) = x. [para(111(a,1),77(a,1,1,2)),rewrite(2(2),376(2),5(6),1201(11),2(12),455(12),111(14),2(10),376(10))]. given #429 (F,wt=17): 9783 x ^ (y v ((z v x) ^ ((x v u) ^ (x v v)))) = x. [para(1350(a,1),380(a,1,2)),rewrite(5(2),1363(2),17(1),362(5)),flip(a)]. given #430 (F,wt=19): 1385 x ^ (y v ((z ^ u) v (x ^ (y v z)))) = x ^ (y v z). [para(24(a,1),1366(a,1,2,2,2)),rewrite(2(3),2(5),14(5),2(4),14(9),9(8))]. given #431 (F,wt=19): 1391 x ^ ((x ^ (y ^ z)) v (y ^ (u ^ z))) = x ^ (y ^ z). [para(406(a,1),1366(a,1,2,2,2)),rewrite(2(5),406(10))]. given #432 (T,wt=19): 1407 (x ^ (y v z)) v (x ^ (z v (y ^ u))) = x ^ (y v z). [para(1367(a,1),82(a,1,2,2))]. given #433 (A,wt=27): 420 (x ^ y) v (x ^ (z v ((y v u) ^ (y v v)))) = x ^ (z v ((y v u) ^ (y v v))). [para(111(a,1),406(a,1,2,2)),rewrite(2(7))]. given #434 (F,wt=19): 1420 x ^ (y v ((z ^ u) v (x ^ (z v y)))) = x ^ (z v y). [para(1367(a,1),696(a,1,2,2)),rewrite(14(5),2(4))]. given #435 (F,wt=19): 1459 (x ^ y) v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x ^ y. [para(147(a,1),1369(a,1,1)),rewrite(5(7),15(7),8(9),5(7),15(7)),flip(a)]. given #436 (F,wt=19): 1470 x ^ ((y ^ (z ^ (u ^ v))) v (u ^ (x v w))) = x ^ u. [para(15(a,1),724(a,1,2,1,2))]. given #437 (F,wt=19): 1483 x ^ ((y ^ (x v z)) v (u ^ (y ^ (v v w)))) = x ^ y. [para(414(a,1),724(a,1,2,1,2)),rewrite(2(6))]. given #438 (T,wt=19): 1489 x ^ (y ^ ((x ^ z) v (u ^ (z ^ v)))) = x ^ (y ^ z). [para(711(a,1),724(a,1,2,2)),rewrite(5(4),2(5),834(6),5(8),15(8),5(7))]. given #439 (A,wt=25): 425 x ^ ((y ^ z) v (y ^ ((x v (y ^ z)) ^ (u v z)))) = x ^ (y ^ (u v z)). [para(323(a,1),11(a,1,2,2)),rewrite(5(5),15(5),2(7),324(14))]. given #440 (F,wt=19): 1518 (x ^ (y v z)) v (y ^ (x ^ (u v v))) = x ^ (y v z). [para(300(a,1),1507(a,2)),rewrite(300(4),834(5))]. given #441 (F,wt=19): 1519 (x ^ (y v z)) v (x ^ (z ^ (u v v))) = x ^ (y v z). [para(318(a,1),1507(a,1,1)),rewrite(834(5),318(10))]. given #442 (F,wt=19): 1666 x ^ ((y ^ (x v z)) v (y ^ (u ^ (v v w)))) = x ^ y. [para(215(a,1),747(a,1,2,2,2))]. given #443 (F,wt=19): 1685 x ^ ((y ^ (z ^ u)) v (x ^ (z v v))) = x ^ (z v v). [para(15(a,1),794(a,1,2,1))]. given #444 (T,wt=19): 1765 x ^ (y ^ (z ^ (u v (v v (x ^ y))))) = x ^ (y ^ z). [para(711(a,1),984(a,1,2,2,2,2)),rewrite(834(5))]. given #445 (A,wt=29): 433 x ^ (y ^ ((z ^ u) v (z ^ ((x v (z ^ u)) ^ (v v u))))) = x ^ (y ^ (z ^ (v v u))). [para(323(a,1),31(a,1,2,2,2)),rewrite(5(5),15(5),2(7),324(15),15(13))]. given #446 (F,wt=19): 1843 (x ^ y) v (x ^ (z ^ ((u ^ y) v (y ^ v)))) = x ^ y. [para(1013(a,1),608(a,1,2)),rewrite(5(4),2(7),1013(13))]. given #447 (F,wt=19): 1853 x ^ (y ^ (z v (x ^ (u v z)))) = x ^ (y ^ (u v z)). [para(1363(a,1),1022(a,1,2,2,2)),rewrite(2(3))]. given #448 (F,wt=19): 1889 (x v (y v (z v u))) ^ (z v (x ^ v)) = z v (x ^ v). [para(14(a,1),1101(a,1,1,2))]. given #449 (F,wt=19): 1891 (x v (y ^ z)) ^ (y v (x v (u v v))) = x v (y ^ z). [para(37(a,1),1101(a,1,1,2)),rewrite(5(6))]. given #450 (T,wt=19): 1897 (x v (y ^ z)) ^ (y v (x v (u ^ v))) = x v (y ^ z). [para(103(a,1),1101(a,1,1,2)),rewrite(5(6))]. given #451 (A,wt=29): 435 x ^ (y ^ ((z v (x ^ u)) ^ ((u ^ v) v (u ^ w)))) = x ^ (y ^ ((u ^ v) v (u ^ w))). [para(135(a,1),323(a,1,2,2,2)),rewrite(5(8),15(8),15(7))]. given #452 (F,wt=19): 1949 x v (y ^ (z ^ (u ^ (v ^ ((x ^ w) v (x ^ v6)))))) = x. [para(834(a,1),1131(a,1,2,2,2))]. given #453 (F,wt=19): 1973 x v (y v (z v (u ^ (v ^ (x v y))))) = x v (y v z). [para(834(a,1),1137(a,1,2,2,2))]. given #454 (F,wt=19): 1998 x v (y v (z v (u ^ (x v (y v z))))) = x v (y v z). [para(140(a,1),1958(a,1,2,2,2)),rewrite(2(10),14(10),14(9),492(11),140(13))]. given #455 (F,wt=19): 2008 x v (y ^ ((x v (y ^ z)) ^ (z v u))) = x v (y ^ z). [para(215(a,1),1974(a,1,2,2)),rewrite(2(2),15(5),2(8))]. given #456 (T,wt=19): 2009 x v (y ^ ((x v (z ^ y)) ^ (z v u))) = x v (z ^ y). [para(300(a,1),1974(a,1,2,2)),rewrite(2(2),15(5),2(8))]. given #457 (A,wt=29): 436 x ^ ((y v (x ^ (z v (u ^ v)))) ^ ((z ^ w) v (u ^ v))) = x ^ ((z ^ w) v (u ^ v)). [para(103(a,1),323(a,1,2,2,2)),rewrite(5(9),15(9))]. given #458 (F,wt=19): 2021 x v (y ^ (x v (z ^ (y ^ u)))) = x v (z ^ (y ^ u)). [para(724(a,1),1974(a,1,2)),rewrite(2(3),5(4),2(8))]. given #459 (F,wt=19): 2032 ((x v y) ^ (x v z)) v ((x v y) ^ (y v u)) = x v y. [para(1974(a,1),1974(a,1,2,1)),rewrite(1974(11))]. given #460 (F,wt=19): 2047 x v ((x v (y v z)) ^ (y v (z v u))) = x v (y v z). [para(14(a,1),1999(a,1,2,1)),rewrite(14(2),2(4),14(4),2(3))]. given #461 (F,wt=19): 2053 x v (y v (z v (u ^ (v ^ (x v z))))) = x v (y v z). [para(1993(a,1),14(a,2,2)),rewrite(14(8))]. given #462 (T,wt=19): 2073 x v ((y v z) ^ (y v ((x ^ u) v (x ^ v)))) = x v y. [para(11(a,1),2006(a,1,2,2,2))]. given #463 (A,wt=25): 438 (x ^ (y ^ z)) v (x ^ (u v (y ^ (v v z)))) = x ^ (u v (y ^ (v v z))). [para(323(a,1),406(a,1,2,2)),rewrite(2(7))]. given #464 (F,wt=17): 10811 x ^ ((y ^ z) v (x ^ (u v z))) = x ^ (u v z). [para(1683(a,1),438(a,2)),rewrite(32(2),2(3),1080(7),2(6))]. given #465 (F,wt=19): 2074 x v (y v ((z v u) ^ (z v (x ^ v)))) = x v (y v z). [para(2006(a,1),14(a,2,2)),rewrite(14(8))]. given #466 (F,wt=19): 2090 x v ((y v z) ^ ((y v u) ^ (y v (x ^ v)))) = x v y. [para(362(a,1),2006(a,1,2,1)),rewrite(834(6))]. given #467 (F,wt=19): 2119 (x v y) ^ (x v (z ^ (y ^ u))) = x v (z ^ (y ^ u)). [para(1505(a,1),2093(a,1,2,2)),rewrite(5(5))]. given #468 (T,wt=19): 2131 x v (y v (z ^ (x v (z ^ u)))) = x v (y v (z ^ u)). [para(2013(a,1),14(a,2,2)),rewrite(14(8))]. given #469 (A,wt=29): 451 (x ^ (y v z)) v (x ^ (u v ((x v v) ^ (y v z)))) = x ^ (u v ((x v v) ^ (y v z))). [para(414(a,1),215(a,1,1)),rewrite(2(6),2(12))]. given #470 (F,wt=19): 2174 x v ((x v y) ^ (z v ((y v u) ^ (y v v)))) = x v y. [para(111(a,1),2014(a,1,2,2,2)),rewrite(5(6),111(12))]. given #471 (F,wt=19): 2177 x v (y ^ ((x v (y ^ z)) ^ (u v z))) = x v (y ^ z). [para(317(a,1),2014(a,1,2,2,2)),rewrite(5(3),5(5),15(5),15(9),1363(8))]. given #472 (F,wt=19): 2196 x v ((x v y) ^ (z v ((u v y) ^ (y v v)))) = x v y. [para(1345(a,1),2014(a,1,2,2,2)),rewrite(5(6),1345(12))]. given #473 (F,wt=19): 2212 x v ((x v (y v z)) ^ (y v (u v z))) = x v (y v z). [para(2093(a,1),2014(a,1,2,2,2)),rewrite(5(5),2093(10))]. given #474 (T,wt=19): 2226 x v ((y v z) ^ (z v ((x ^ u) v (x ^ v)))) = x v z. [para(11(a,1),2072(a,1,2,2,2))]. given #475 (A,wt=29): 453 (x ^ (y v z)) v ((x v u) ^ ((x v v) ^ (y v z))) = (x v u) ^ ((x v v) ^ (y v z)). [para(414(a,1),300(a,1,1)),rewrite(5(7),15(7),5(13),15(13))]. given #476 (F,wt=19): 2227 x v (y v ((z v u) ^ (u v (x ^ v)))) = x v (y v u). [para(2072(a,1),14(a,2,2)),rewrite(14(8))]. given #477 (F,wt=19): 2291 x ^ (y v ((z ^ u) v (x ^ (y v u)))) = x ^ (y v u). [para(2111(a,1),1010(a,1,2,1)),rewrite(5(4),2(5),14(5),2(4),5(8))]. given #478 (F,wt=19): 2299 (x v y) ^ (x v (z v ((u v y) ^ (y v v)))) = x v y. [para(1345(a,1),2111(a,1,2,2)),rewrite(5(7),1345(12))]. given #479 (F,wt=19): 2314 (x v (y v z)) ^ (x v (y v (u v z))) = x v (y v z). [para(2093(a,1),2111(a,1,2,2)),rewrite(5(6),2093(10))]. given #480 (T,wt=19): 2340 (x v y) v (z ^ (u ^ (v ^ (w ^ (x v y))))) = x v y. [para(834(a,1),1141(a,1,2,2,2))]. given #481 (A,wt=21): 455 (x ^ (y v z)) v ((x v u) ^ (y v z)) = (x v u) ^ (y v z). [para(414(a,1),376(a,1,2)),rewrite(2(6))]. given #482 (F,wt=19): 2404 (x ^ y) v ((x v z) ^ (y v u)) = (x v z) ^ (y v u). [para(8(a,1),1181(a,1,1,2)),rewrite(5(4),5(8))]. given #483 (F,wt=19): 2405 (x ^ y) v (y ^ (z v (x ^ y))) = y ^ (z v (x ^ y)). [para(16(a,1),1181(a,1,1)),rewrite(2(3),2(7))]. given #484 (F,wt=19): 2443 (x ^ (y ^ (z ^ u))) v (u ^ (x v v)) = u ^ (x v v). [para(794(a,1),1181(a,1,2)),rewrite(15(3),5(2),15(2),5(1),15(3),15(2),794(11))]. given #485 (F,wt=19): 2455 (x v y) ^ (x v (z ^ (u ^ y))) = x v (z ^ (u ^ y)). [para(2412(a,1),2093(a,1,2,2)),rewrite(5(5))]. given #486 (T,wt=19): 2456 x v (y ^ (x v (z ^ (u ^ y)))) = x v (z ^ (u ^ y)). [para(2412(a,1),2195(a,1,2,2)),rewrite(5(4))]. given #487 (A,wt=27): 456 (x ^ (y ^ (z v u))) v (x ^ ((y v v) ^ (z v u))) = x ^ ((y v v) ^ (z v u)). [para(414(a,1),406(a,1,2,2)),rewrite(2(8))]. given #488 (F,wt=19): 2474 (x ^ (y ^ (z ^ u))) v (z ^ (x v v)) = z ^ (x v v). [para(15(a,1),1184(a,1,1,2))]. given #489 (F,wt=19): 2479 x ^ (y ^ (z ^ (u v (y ^ (x v v))))) = x ^ (y ^ z). [para(1184(a,1),377(a,1,2,2)),rewrite(834(6),834(5))]. given #490 (F,wt=19): 2546 x v (y v (z ^ (x v ((y ^ u) v (y ^ v))))) = x v y. [para(11(a,1),2522(a,1,2,2,2,2))]. given #491 (F,wt=19): 2547 x v (y v (z v (u ^ (x v (z ^ v))))) = x v (y v z). [para(2522(a,1),14(a,2,2)),rewrite(14(8))]. given #492 (T,wt=19): 2578 x v (y v (z ^ (y v ((x ^ u) v (x ^ v))))) = x v y. [para(11(a,1),2545(a,1,2,2,2,2))]. given #493 (A,wt=21): 466 (x v y) ^ (z v ((x v (y v u)) ^ (x v (y v v)))) = x v y. [para(440(a,1),74(a,1,1)),rewrite(2(5),14(5),2(4),440(12))]. given #494 (F,wt=19): 2579 x v (y v (z v (u ^ (z v (x ^ v))))) = x v (y v z). [para(2545(a,1),14(a,2,2)),rewrite(14(8))]. given #495 (F,wt=19): 2617 (x v y) ^ (y v (z v ((x v u) ^ (x v v)))) = x v y. [para(1262(a,1),215(a,1,1)),rewrite(2(7),14(7),9(9),2(7),14(7)),flip(a)]. given #496 (F,wt=19): 2884 x ^ (y ^ ((x ^ (y v z)) v (u ^ (v v w)))) = x ^ y. [para(215(a,1),2850(a,1,2,1)),rewrite(834(7))]. given #497 (F,wt=19): 2887 x ^ (y ^ ((y ^ (x v z)) v (u ^ (v v w)))) = x ^ y. [para(300(a,1),2850(a,1,2,1)),rewrite(834(7))]. given #498 (T,wt=19): 2927 x ^ (y v (((x v z) ^ (x v u)) v (v ^ (w v v6)))) = x. [para(362(a,1),2883(a,1,2,2,1))]. given #499 (A,wt=27): 484 (x ^ y) v (x ^ (z v (y ^ (u v (x ^ y))))) = x ^ (z v (y ^ (u v (x ^ y)))). [para(458(a,1),215(a,1,1)),rewrite(2(5),2(11))]. given #500 (F,wt=19): 2946 x ^ (((x v y) ^ (x v z)) v (u ^ (v ^ (w v v6)))) = x. [para(362(a,1),2885(a,1,2,1))]. given #501 (F,wt=19): 2979 x v (y v (z v (u ^ (x v (y ^ v))))) = x v (y v z). [para(1413(a,1),1993(a,1,2,2,2)),rewrite(2(5),14(5),2(4))]. given #502 (F,wt=19): 3001 x ^ (y ^ ((x ^ z) v (u ^ (v ^ z)))) = x ^ (y ^ z). [para(711(a,1),1468(a,1,2,2)),rewrite(5(4),2(5),834(6),5(8),15(8),5(7))]. given #503 (F,wt=19): 3225 x ^ ((x ^ y) v (z ^ ((u ^ y) v (y ^ v)))) = x ^ y. [para(3194(a,1),1366(a,1,2,2,2)),rewrite(2(6),3194(12))]. given #504 (T,wt=19): 3233 (x v y) v (x ^ (z ^ (u ^ (v ^ (w v v6))))) = x v y. [para(215(a,1),1628(a,1,2,2,2,2))]. given #505 (A,wt=27): 486 (x ^ y) v (y ^ ((x v z) ^ (u v (x ^ y)))) = y ^ ((x v z) ^ (u v (x ^ y))). [para(458(a,1),300(a,1,1)),rewrite(5(6),15(6),5(12),15(12))]. given #506 (F,wt=19): 3315 (x v y) v (y ^ (z ^ (u ^ (v ^ (w v v6))))) = x v y. [para(215(a,1),1644(a,1,2,2,2,2))]. given #507 (F,wt=19): 3368 (x ^ (y ^ (z ^ u))) v (x ^ (u v v)) = x ^ (u v v). [para(1657(a,2),304(a,1,1,2)),rewrite(5(1),700(5))]. given #508 (F,wt=19): 3379 x ^ ((y ^ (z ^ (u ^ v))) v (v ^ (x v w))) = x ^ v. [para(1657(a,2),724(a,1,2,1,2)),rewrite(5(1),700(5))]. given #509 (F,wt=19): 3382 x ^ ((y ^ (z ^ u)) v (x ^ (u v v))) = x ^ (u v v). [para(1657(a,2),794(a,1,2,1)),rewrite(5(1),700(5))]. given #510 (T,wt=19): 3431 (x ^ (y ^ (z ^ u))) v (u ^ (y v v)) = u ^ (y v v). [para(1683(a,1),1181(a,1,2)),rewrite(15(3),5(2),15(2),5(1),15(3),15(2),1683(11))]. given #511 (A,wt=25): 487 (x ^ (y ^ z)) v (x ^ (y ^ (u v (y ^ z)))) = x ^ (y ^ (u v (y ^ z))). [para(458(a,1),406(a,1,2,2)),rewrite(5(1),5(5),2(7),5(8))]. given #512 (F,wt=17): 12268 x v ((y ^ (x ^ z)) v (u ^ v)) = x v (u ^ v). [para(1367(a,1),3431(a,1,2)),rewrite(2(1),30(3),14(5),2(6),1369(9))]. given #513 (F,wt=17): 12284 x v (y v (z v (u ^ (x ^ v)))) = x v (y v z). [para(462(a,1),3431(a,1,2)),rewrite(30(4),14(5),14(4),2(3),462(11))]. given #514 (F,wt=19): 3433 (x ^ (y ^ (z ^ u))) v (z ^ (y v v)) = z ^ (y v v). [para(1683(a,1),1184(a,1,2)),rewrite(15(3),5(2),15(2),5(1),15(3),15(2),1683(11))]. given #515 (F,wt=19): 3437 (x ^ (y v z)) v (x ^ (y v (u ^ z))) = x ^ (y v z). [para(3428(a,1),318(a,1,2,2)),rewrite(2(4),2(6),14(9),376(8))]. given #516 (T,wt=19): 3447 (x v y) ^ (z v (y v ((x v u) ^ (x v v)))) = x v y. [para(111(a,1),3427(a,1,2,2)),rewrite(2(5),14(5),2(6),5(7),111(12),2(8))]. given #517 (A,wt=23): 491 x v (y v (z v (u v (v v (x ^ w))))) = x v (y v (z v (u v v))). [para(46(a,1),14(a,2,2)),rewrite(14(10))]. given #518 (F,wt=19): 3458 (x v y) ^ (z v (y v ((u v x) ^ (x v v)))) = x v y. [para(1345(a,1),3427(a,1,2,2)),rewrite(2(5),14(5),2(6),5(7),1345(12),2(8))]. given #519 (F,wt=19): 3464 (x ^ y) v (z ^ (y ^ ((x ^ u) v (x ^ v)))) = x ^ y. [para(146(a,1),3427(a,1,2)),rewrite(5(5),2(6),5(7),5(8),8(8),5(2),15(7)),flip(a)]. given #520 (F,wt=19): 3484 ((x v y) ^ (x v z)) v ((x v z) ^ (z v u)) = x v z. [para(3463(a,1),1974(a,1,2,1)),rewrite(3463(11))]. given #521 (F,wt=19): 3506 ((x v y) ^ (y v z)) v ((y v z) ^ (z v u)) = y v z. [para(3465(a,1),1974(a,1,2,1)),rewrite(3465(11))]. given #522 (T,wt=19): 3507 x v ((x v y) ^ (z v ((x v y) ^ (u v y)))) = x v y. [para(3465(a,1),1999(a,2)),rewrite(2(2),5(3),2195(4),2(3),5(4),2(5),2(8))]. given #523 (A,wt=25): 492 x v (y v (z v (u v (v ^ ((x ^ w) v (x ^ v6)))))) = x v (y v (z v u)). [para(31(a,1),46(a,1,2,2,2,2))]. given #524 (F,wt=19): 3580 (x ^ y) v (z ^ (y ^ ((u ^ x) v (x ^ v)))) = x ^ y. [para(3194(a,1),3452(a,1,2,2)),rewrite(5(5),15(5),5(6),2(7),3194(12),5(8))]. given #525 (F,wt=19): 3590 x ^ ((x ^ y) v (z ^ ((x ^ y) v (u ^ y)))) = x ^ y. [para(3561(a,1),696(a,2)),rewrite(5(2),2(3),760(4),5(3),2(4),5(5),5(8))]. given #526 (F,wt=19): 3591 ((x ^ y) v (y ^ z)) ^ ((y ^ z) v (z ^ u)) = y ^ z. [para(3561(a,1),1010(a,1,2,2)),rewrite(2(6),3561(11))]. given #527 (F,wt=19): 3592 x ^ (y ^ ((z ^ u) v (z ^ (x ^ y)))) = z ^ (x ^ y). [para(3561(a,1),834(a,1)),rewrite(5(3)),flip(a)]. given #528 (T,wt=19): 3643 x v (y v ((x v z) ^ (u v (z v v)))) = x v (y v z). [para(3467(a,1),14(a,2,2)),rewrite(2(3),5(4),2(7),14(8))]. given #529 (A,wt=23): 493 x v (y v (z v ((x ^ u) v (v ^ w)))) = x v (y v (z v (v ^ w))). [para(103(a,1),46(a,2,2,2)),rewrite(2(5),170(6))]. given #530 (F,wt=19): 3694 x ^ (y ^ ((z ^ (u ^ v)) v (u ^ x))) = u ^ (x ^ y). [para(3562(a,1),1657(a,1,2,2,1)),rewrite(15(9),3684(8),15(2),5(1),5(7)),flip(a)]. given #531 (F,wt=19): 3734 x ^ (y ^ ((z ^ (u ^ v)) v (v ^ x))) = v ^ (x ^ y). [para(3574(a,1),1657(a,1,2,2,1)),rewrite(15(9),3721(8),15(2),5(1),5(7)),flip(a)]. given #532 (F,wt=19): 3739 x ^ (y v (x ^ (z v (u v y)))) = x ^ (z v (u v y)). [para(3642(a,1),760(a,1,2)),rewrite(2(4))]. given #533 (F,wt=19): 3771 x v (y v ((x v z) ^ (u v (v v z)))) = x v (y v z). [para(3756(a,1),14(a,2,2)),rewrite(2(3),5(4),2(7),14(8))]. given #534 (T,wt=19): 3825 x ^ ((y ^ (z ^ u)) v (z ^ (v v (x ^ z)))) = x ^ z. [para(15(a,1),1722(a,1,2,1))]. given #535 (A,wt=25): 495 (x v (y v (z v u))) ^ (x v (y v (z v (u v v)))) = x v (y v (z v u)). [para(46(a,1),440(a,1,1)),rewrite(2(8),14(8),14(7),14(6),491(9),46(13))]. given #536 (F,wt=19): 3831 x ^ ((y ^ z) v (y ^ (u v (y ^ (x v v))))) = x ^ y. [para(1722(a,1),414(a,1,2)),rewrite(5(2),30(3),5(4)),flip(a)]. given #537 (F,wt=19): 3854 x ^ ((y ^ (z ^ u)) v (u ^ (v v (x ^ u)))) = x ^ u. [para(1657(a,2),1722(a,1,2,1)),rewrite(5(1),700(5))]. given #538 (F,wt=19): 3874 x ^ (y ^ (z v (u v (v v (x ^ (y v w)))))) = x ^ y. [para(984(a,1),229(a,1,1)),rewrite(2(6),14(6),14(5),82(9),2(6),14(6),14(5)),flip(a)]. given #539 (F,wt=19): 3875 x ^ (y ^ (z v (u v (v v (w v (x ^ y)))))) = x ^ y. [para(997(a,1),229(a,1,1)),rewrite(2(6),14(6),14(5),14(4),82(9),2(6),14(6),14(5),14(4)),flip(a)]. given #540 (T,wt=19): 3890 x ^ ((x v y) v (z ^ (u ^ (v ^ (w ^ (v6 v v7)))))) = x. [para(229(a,1),2885(a,1,2,2,2,2))]. given #541 (A,wt=27): 496 x v (y v (z v (u v (v v (w v (x ^ v6)))))) = x v (y v (z v (u v (v v w)))). [para(46(a,1),46(a,2,2,2)),rewrite(2(6),14(6),14(5),14(4),491(7))]. given #542 (F,wt=17): 13035 x v (y ^ (z ^ (u ^ (v ^ (x ^ (w v v6)))))) = x. [para(3890(a,1),3452(a,1,2)),rewrite(5(6),15(6),15(5),15(4),15(3),2(7),2(14),14(14),2(13),8(15))]. given #543 (F,wt=19): 3942 (x v y) ^ ((x ^ z) v (y ^ u)) = (x ^ z) v (y ^ u). [para(9(a,1),1886(a,1,1,2)),rewrite(2(4),2(8))]. given #544 (F,wt=19): 3991 (x ^ y) v (x ^ (z v (u v y))) = x ^ (z v (u v y)). [para(3949(a,1),406(a,1,2,2)),rewrite(2(5))]. given #545 (F,wt=19): 4037 x v (y v (z ^ (x v (u ^ z)))) = x v (y v (u ^ z)). [para(720(a,1),2002(a,1,2,2)),rewrite(5(3))]. given #546 (T,wt=19): 4107 x v ((y v z) ^ ((x ^ u) v (y ^ v))) = x v (y ^ v). [para(2026(a,1),103(a,1,2)),rewrite(103(4),5(7)),flip(a)]. given #547 (A,wt=23): 513 (x ^ y) v (x ^ (z v (u v (x ^ y)))) = x ^ (z v (u v (x ^ y))). [para(457(a,1),376(a,1,2)),rewrite(5(1),5(5),2(6),5(7))]. Low Water (keep): wt=29, part=1.00, limit=29 given #548 (F,wt=19): 4135 x v (y v (z ^ (u ^ (v ^ (w ^ (x v y)))))) = x v y. [para(834(a,1),2056(a,1,2,2,2,2))]. given #549 (F,wt=19): 4159 x v (y v (z ^ (u ^ (v ^ (y v (x ^ w)))))) = x v y. [para(2056(a,1),170(a,1,2)),rewrite(24(3)),flip(a)]. given #550 (F,wt=19): 4221 (x ^ y) v (x ^ z) = x ^ ((x ^ z) v (y ^ (x v z))). [back_rewrite(683),rewrite(4174(6)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 24.37 (+ 0.20) seconds: H2. % Length of proof is 82. % Level of proof is 19. % Maximum clause weight is 29. % Given clauses 550. 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2) # label(goal). [goal]. 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. 5 x ^ y = y ^ x. [assumption]. 6 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 10 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. 12 c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2) # answer(H2). [deny(1)]. 13 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(12),rewrite(2(12))]. 14 x v (y v z) = y v (x v z). [para(4(a,1),2(a,1)),rewrite(2(3),2(4))]. 15 x ^ (y ^ z) = y ^ (x ^ z). [para(7(a,1),5(a,1)),rewrite(5(3),5(4))]. 16 x ^ x = x. [para(9(a,1),8(a,1,2))]. 17 x v x = x. [para(8(a,1),9(a,1,2))]. 18 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (z ^ x) v (x ^ y). [para(11(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. 24 x v (y v (x ^ z)) = x v y. [para(9(a,1),14(a,2,2)),rewrite(2(4))]. 25 x ^ (((x v y) ^ (z v u)) v (y ^ (x v (z v u)))) = (x ^ y) v (x ^ (z v u)). [para(14(a,1),11(a,1,2,1,2)),rewrite(14(2),5(6),2(7),2(12))]. 26 x v (x v y) = x v y. [para(14(a,1),17(a,1)),rewrite(2(2),14(2),17(1))]. 30 x ^ (y ^ (x v z)) = x ^ y. [para(8(a,1),15(a,2,2)),rewrite(5(4))]. 31 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(11(a,1),15(a,2,2)),rewrite(2(5),2(10))]. 32 x ^ (x ^ y) = x ^ y. [para(15(a,1),16(a,1)),rewrite(5(2),15(2),16(1))]. 37 x v (y v (z v (x ^ u))) = x v (y v z). [para(24(a,1),14(a,2,2)),rewrite(14(6))]. 39 (x ^ (y v z)) ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(11(a,1),30(a,1,2)),rewrite(5(4),2(5),5(9),15(9),8(8))]. 40 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(11(a,1),30(a,2)),rewrite(2(5),5(7),31(8),2(8))]. 41 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(30(a,1),15(a,2,2)),rewrite(15(6))]. 48 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [para(8(a,1),18(a,2,1)),rewrite(26(3),2(5),14(5),2(4),8(6),2(4),5(7))]. 51 x ^ ((y ^ z) ^ (y v u)) = x ^ (y ^ z). [para(11(a,1),41(a,1,2,2)),rewrite(5(4),2(5),15(7),39(6),15(2),5(1),5(5),5(6),15(6)),flip(a)]. 54 x ^ (y ^ (z ^ (u ^ (x v v)))) = x ^ (y ^ (z ^ u)). [para(41(a,1),15(a,2,2)),rewrite(15(8))]. 57 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),51(a,2)),rewrite(32(5))]. 62 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),57(a,1,1)),rewrite(5(4))]. 65 (x ^ y) ^ ((x v z) ^ (u v (x ^ y))) = x ^ y. [para(57(a,1),30(a,2)),rewrite(2(4))]. 67 (x v y) ^ ((x ^ z) v (u ^ (x v y))) = (x ^ z) v (u ^ (x v y)). [para(57(a,1),18(a,2,1)),rewrite(14(4),2(3),24(4),2(6),14(6),2(5),57(7),2(5),5(9))]. 69 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(57(a,1),57(a,1,1)),rewrite(2(3),57(7))]. 74 (x ^ y) ^ (z v (y ^ (x v u))) = x ^ y. [para(30(a,1),62(a,1,1)),rewrite(2(4),30(8))]. 77 ((x ^ y) v (y ^ z)) ^ (u v ((z ^ (x v y)) v (x ^ (y v z)))) = (x ^ y) v (y ^ z). [para(18(a,1),62(a,1,1)),rewrite(2(9),18(16))]. 82 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(69(a,1),18(a,1,2,1)),rewrite(17(5),15(4),5(3),8(6),15(3),5(2),16(6),2(5)),flip(a)]. 93 ((x v y) ^ (z v u)) ^ ((x ^ y) v (x ^ (z v u))) = x ^ ((x v y) ^ (z v u)). [para(25(a,1),30(a,1,2)),rewrite(5(12))]. 94 (x ^ y) ^ ((x v z) ^ (u v v)) = x ^ (y ^ ((x v z) ^ (u v v))). [para(25(a,1),41(a,1,2,2)),rewrite(15(9),93(8),15(5),5(9),5(10)),flip(a)]. 98 x ^ (y ^ ((x v z) ^ (u v (x ^ y)))) = x ^ y. [back_rewrite(65),rewrite(94(6))]. 103 x v ((x ^ y) v (z ^ u)) = x v (z ^ u). [para(82(a,1),37(a,2,2)),rewrite(2(5),14(6),82(5))]. 111 x ^ (y v ((x v z) ^ (x v u))) = x. [para(8(a,1),74(a,1,1)),rewrite(8(7))]. 147 (x ^ y) v (y ^ ((x ^ z) v (x ^ u))) = x ^ y. [para(31(a,1),82(a,1,2))]. 215 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(39(a,1),9(a,1,2)),rewrite(2(4))]. 242 (x ^ y) v ((z ^ u) v (x ^ (y v v))) = (z ^ u) v (x ^ (y v v)). [para(39(a,1),103(a,1,2,1)),rewrite(14(6),2(5),2(10))]. 300 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(5(a,1),215(a,1,1))]. 362 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(8(a,1),300(a,1,1))]. 376 x v (y ^ x) = x. [para(111(a,1),300(a,1,2)),rewrite(2(2),111(7))]. 414 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(215(a,1),40(a,1,2)),rewrite(15(4),215(8))]. 416 ((x v y) ^ (z v u)) ^ ((x ^ y) v (x ^ (z v u))) = x ^ (z v u). [back_rewrite(93),rewrite(414(12))]. 440 (x v y) ^ (x v (y v z)) = x v y. [para(16(a,1),414(a,2)),rewrite(2(3),14(3),2(2),5(5),32(6))]. 441 x ^ (y ^ ((x v z) ^ (u v v))) = x ^ (y ^ (u v v)). [para(414(a,1),15(a,2,2)),rewrite(15(8))]. 454 (x ^ y) ^ ((y ^ (x v z)) ^ (u v v)) = (x ^ y) ^ (u v v). [para(300(a,1),414(a,1,2,1))]. 458 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(98),rewrite(441(6))]. 459 (x ^ y) ^ ((x v z) ^ (u v v)) = x ^ (y ^ (u v v)). [back_rewrite(94),rewrite(441(10))]. 678 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(48(a,1),458(a,1,2))]. 683 x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z). [para(11(a,1),678(a,1,2,2)),rewrite(2(5),14(6),2(5),2(12),11(13))]. 696 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(147(a,1),678(a,1,2)),rewrite(5(1),32(2),5(2)),flip(a)]. 711 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(696(a,1),414(a,1,2)),rewrite(5(2),30(3),5(3),2(5)),flip(a)]. 720 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(5(a,1),711(a,1,2,1))]. 760 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(9(a,1),720(a,1,2,2,2)),rewrite(5(2),2(3))]. 794 x ^ ((y ^ z) v (x ^ (y v u))) = x ^ (y v u). [para(57(a,1),760(a,1,2,2)),rewrite(2(4))]. 814 x ^ ((y ^ z) ^ (u v v)) = x ^ (y ^ (z ^ (u v v))). [para(25(a,1),54(a,1,2,2,2)),rewrite(15(10),15(9),416(8),15(3),15(4),5(8),15(9),5(10),459(10)),flip(a)]. 834 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [back_rewrite(454),rewrite(814(6),15(6),459(5),15(4),32(3)),flip(a)]. 1033 (x v y) v (z ^ (u ^ (x v y))) = x v y. [para(834(a,1),376(a,1,2))]. 1137 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(440(a,1),1033(a,1,2,2)),rewrite(2(5),14(5),14(4),2(3))]. 1201 x v (y v ((x v z) ^ (x v u))) = y v ((x v z) ^ (x v u)). [para(362(a,1),14(a,2,2))]. 1346 x ^ (y v (x ^ (z v x))) = x. [para(16(a,1),77(a,1,1,2)),rewrite(2(2),376(2),17(3),2(4),300(4),16(6),2(6),376(6))]. 1363 x ^ (y v x) = x. [para(1346(a,1),5(a,2)),rewrite(2(1),8(2),5(2))]. 1367 (x v y) ^ (y v (x ^ z)) = y v (x ^ z). [para(1346(a,1),67(a,1,2,2)),rewrite(2(1),8(2),2(3),2(6),8(7),1363(7),2(6))]. 1683 x ^ ((y ^ z) v (x ^ (z v u))) = x ^ (z v u). [para(5(a,1),794(a,1,2,1))]. 1974 x v ((y v x) ^ (y v z)) = y v x. [para(362(a,1),1137(a,1,2,2)),rewrite(5(3),1201(5),2(5),26(6))]. 2006 x v ((y v z) ^ (y v (x ^ u))) = x v y. [para(1974(a,1),103(a,1,2)),rewrite(24(3),5(5)),flip(a)]. 2093 (x v y) ^ (x v (z v y)) = x v y. [para(2006(a,1),1367(a,1,2)),rewrite(2(2),14(2),2(1),2(3),5(4),2006(9),2(5))]. 2111 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(376(a,1),2093(a,1,2,2)),rewrite(5(4))]. 3428 x v (y v (z ^ x)) = x v y. [para(1683(a,1),2111(a,1)),rewrite(14(3),2(2),5(5),440(5),14(5),2(4),5(7),440(7),14(4),2(3)),flip(a)]. 4174 (x ^ y) v ((z ^ u) v (y ^ (x v v))) = (z ^ u) v (y ^ (x v v)). [para(5(a,1),242(a,1,1))]. 4221 (x ^ y) v (x ^ z) = x ^ ((x ^ z) v (y ^ (x v z))). [back_rewrite(683),rewrite(4174(6)),flip(a)]. 13496 x v (y ^ ((x ^ y) v (z ^ (x v y)))) = x v (y ^ z). [para(4221(a,1),3428(a,1,2)),rewrite(5(1),2(2))]. 13559 $F # answer(H2). [back_rewrite(13),rewrite(13496(14),5(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=550. Generated=573208. Kept=13553. proofs=1. Usable=469. Sos=10119. Demods=10413. Limbo=63, Disabled=2910. Hints=0. Weight_deleted=100113. Literals_deleted=0. Forward_subsumed=459307. Back_subsumed=1143. Sos_limit_deleted=234. Sos_displaced=0. Sos_removed=0. New_demodulators=13233 (6 lex), Back_demodulated=1759. Back_unit_deleted=0. Demod_attempts=13871644. Demod_rewrites=3214006. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=14.89. User_CPU=24.37, System_CPU=0.20, Wall_clock=25. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4386 exit (max_proofs) Wed Nov 22 12:04:01 2006