============================== Prover9 =============================== Prover9 (32) version 22-May-2007, May 2007. Process 27627 was started by mccune on cleo, Tue May 22 14:49:40 2007 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H27d.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 uc.in formulas(sos). x v x' = 1. x ^ x' = 0. x v y != 1 | x ^ y != 0 | x' = y. end_of_list. % Reading from file H27d.in assign(max_seconds,60). assign(max_weight,25). list(weights). weight(x') = weight(x). end_of_list. formulas(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). end_of_list. formulas(goals). x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity) # label(non_clause) # 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 v x' = 1. [assumption]. x ^ x' = 0. [assumption]. x v y != 1 | x ^ y != 0 | x' = y. [assumption]. x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label distributivity to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, ^, v, ' ]). After inverse_order: Function symbol precedence: function_order([ 0, 1, c1, c2, c3, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) 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]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # answer(distributivity). [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]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 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: 14 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: 16 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=5): 8 x v x' = 1. [assumption]. given #8 (I,wt=5): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=13): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=23): 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. given #11 (I,wt=13): 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # answer(distributivity). [deny(1)]. given #12 (A,wt=11): 15 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])]. given #13 (T,wt=5): 26 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #14 (T,wt=5): 27 x v x = x. [para(6(a,1),7(a,1,2))]. given #15 (T,wt=5): 30 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #16 (T,wt=5): 33 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #17 (A,wt=11): 17 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. given #18 (T,wt=5): 63 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. given #19 (T,wt=3): 73 1' = 0. [hyper(10,a,33,a,b,63,a)]. given #20 (T,wt=5): 64 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. given #21 (T,wt=3): 76 0' = 1. [hyper(10,a,64,a,b,30,a)]. given #22 (A,wt=7): 18 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #23 (T,wt=5): 74 1 v x = 1. [para(63(a,1),6(a,1))]. given #24 (T,wt=5): 77 0 ^ x = 0. [para(64(a,1),6(a,1,2))]. given #25 (T,wt=5): 86 x v 1 = 1. [para(18(a,1),63(a,1)),flip(a)]. given #26 (T,wt=5): 88 x ^ 0 = 0. [para(77(a,1),4(a,1)),flip(a)]. given #27 (A,wt=13): 19 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #28 (T,wt=6): 90 1 != x | x' = 0. [back_rewrite(65),rewrite([88(4)]),xx(b)]. given #29 (T,wt=6): 91 0 != x | x' = 1. [para(86(a,1),10(a,1)),rewrite([30(5)]),flip(b),xx(a)]. given #30 (T,wt=7): 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #31 (T,wt=7): 75 x v (x' v y) = 1. [back_rewrite(28),rewrite([74(5)])]. given #32 (A,wt=11): 20 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #33 (T,wt=7): 79 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite([77(5)])]. given #34 (T,wt=7): 87 x v (y v x') = 1. [back_rewrite(47),rewrite([86(5)])]. given #35 (T,wt=7): 89 x ^ (y ^ x') = 0. [back_rewrite(72),rewrite([88(5)])]. given #36 (T,wt=7): 113 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #37 (A,wt=13): 21 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #38 (T,wt=7): 129 x ^ (y v x)' = 0. [para(2(a,1),113(a,1,2,1))]. given #39 (T,wt=9): 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #40 (T,wt=9): 32 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #41 (T,wt=9): 45 x ^ (y v (x v z)) = x. [para(15(a,1),6(a,1,2))]. given #42 (A,wt=11): 22 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #43 (T,wt=7): 166 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #44 (T,wt=7): 177 x v (y ^ x)' = 1. [para(4(a,1),166(a,1,2,1))]. given #45 (T,wt=9): 51 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. given #46 (T,wt=9): 53 x ^ (y ^ x) = y ^ x. [para(26(a,1),5(a,2,2)),rewrite([4(2)])]. given #47 (A,wt=13): 23 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #48 (T,wt=9): 56 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. given #49 (T,wt=9): 58 x v (y v x) = y v x. [para(27(a,1),3(a,2,2)),rewrite([2(2)])]. given #50 (T,wt=9): 59 1 != x | 0 != x | x' = x. [para(27(a,1),10(a,1)),rewrite([26(3)]),flip(a),flip(b)]. given #51 (T,wt=9): 71 x v (y ^ (x ^ z)) = x. [para(17(a,1),7(a,1,2))]. given #52 (A,wt=13): 25 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #53 (T,wt=9): 80 x ^ (y v (z v x)) = x. [para(3(a,1),18(a,1,2))]. given #54 (T,wt=9): 102 x v (y ^ (z ^ x)) = x. [para(5(a,1),24(a,1,2))]. given #55 (T,wt=9): 111 x v (y v (x' v z)) = 1. [para(75(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #56 (T,wt=9): 119 x ^ (y ^ (x' ^ z)) = 0. [para(79(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #57 (A,wt=13): 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #58 (T,wt=3): 259 x'' = x. [para(8(a,1),34(a,1)),rewrite([4(5),9(5)]),xx(a),xx(b)]. given #59 (T,wt=7): 275 x' v (y v x) = 1. [para(259(a,1),87(a,1,2,2))]. given #60 (T,wt=7): 276 x' ^ (y ^ x) = 0. [para(259(a,1),89(a,1,2,2))]. given #61 (T,wt=9): 120 x ^ ((x v y)' ^ z) = 0. [para(79(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #62 (A,wt=19): 35 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #63 (T,wt=9): 122 x v (y v (z v x')) = 1. [para(3(a,1),87(a,1,2))]. given #64 (T,wt=9): 126 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),89(a,1,2))]. given #65 (T,wt=9): 128 x ^ (y ^ (x v z)') = 0. [para(89(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #66 (T,wt=9): 133 x ^ (y v (x v z))' = 0. [para(15(a,1),113(a,1,2,1))]. given #67 (A,wt=23): 37 x ^ (y v ((x ^ z) v (z ^ (u v y)))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2,2,2))]. given #68 (T,wt=9): 141 x ^ (y v (z v x))' = 0. [para(3(a,1),129(a,1,2,1))]. given #69 (T,wt=9): 142 x ^ ((y v x)' ^ z) = 0. [para(129(a,1),5(a,1,1)),rewrite([77(2)]),flip(a)]. given #70 (T,wt=9): 146 x ^ (y ^ (z v x)') = 0. [para(129(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #71 (T,wt=9): 147 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. given #72 (A,wt=23): 38 x ^ (y v ((z ^ (y v u)) v (x ^ z))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2))]. given #73 (T,wt=9): 153 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),32(a,1,2,2,1))]. given #74 (T,wt=9): 172 x v ((x ^ y)' v z) = 1. [para(75(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #75 (T,wt=9): 173 x v (y v (x ^ z)') = 1. [para(87(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #76 (T,wt=9): 181 x v (y ^ (x ^ z))' = 1. [para(17(a,1),166(a,1,2,1))]. given #77 (A,wt=23): 39 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,1))]. given #78 (T,wt=9): 182 x v ((y ^ x)' v z) = 1. [para(177(a,1),3(a,1,1)),rewrite([74(2)]),flip(a)]. given #79 (T,wt=9): 184 x v (y ^ (z ^ x))' = 1. [para(5(a,1),177(a,1,2,1))]. given #80 (T,wt=9): 188 x v (y v (z ^ x)') = 1. [para(177(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #81 (T,wt=9): 277 x' v (y v (x v z)) = 1. [para(259(a,1),111(a,1,2,2,1))]. given #82 (A,wt=23): 40 x ^ (y v ((x ^ z) v ((y v u) ^ z))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,2))]. given #83 (T,wt=9): 278 x' ^ (y ^ (x ^ z)) = 0. [para(259(a,1),119(a,1,2,2,1))]. given #84 (T,wt=9): 279 x' v (y v (z v x)) = 1. [para(3(a,1),275(a,1,2))]. given #85 (T,wt=9): 285 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),276(a,1,2))]. given #86 (T,wt=9): 544 (x ^ y)' v (z v x) = 1. [para(7(a,1),279(a,1,2,2))]. given #87 (A,wt=15): 43 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #88 (T,wt=9): 548 (x ^ y)' v (z v y) = 1. [para(24(a,1),279(a,1,2,2))]. given #89 (T,wt=9): 560 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),285(a,1,2,2))]. given #90 (T,wt=9): 563 (x v y)' ^ (z ^ y) = 0. [para(18(a,1),285(a,1,2,2))]. given #91 (T,wt=10): 298 x v y != 1 | (x v y)' = 0. [para(33(a,1),35(a,1,2)),rewrite([4(6),77(6)]),xx(b)]. given #92 (A,wt=11): 46 x v (y v (x ^ z)) = y v x. [para(7(a,1),15(a,1,2)),flip(a)]. given #93 (T,wt=10): 299 x v y != 0 | (x v y)' = 1. [para(86(a,1),35(a,1,2)),rewrite([86(2),4(6),63(6)]),xx(a)]. given #94 (T,wt=10): 639 x v y != 1 | (y v x)' = 0. [para(2(a,1),298(a,1))]. given #95 (T,wt=10): 641 x ^ y != 1 | (x ^ y)' = 0. [para(25(a,1),298(a,1)),rewrite([25(7)])]. given #96 (T,wt=10): 659 x v y != 0 | (y v x)' = 1. [para(2(a,1),299(a,1))]. given #97 (A,wt=19): 48 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(15(a,1),10(a,1))]. given #98 (T,wt=10): 661 x ^ y != 0 | (x ^ y)' = 1. [para(25(a,1),299(a,1)),rewrite([25(7)])]. given #99 (T,wt=10): 664 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),641(a,1))]. given #100 (T,wt=10): 695 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),661(a,1))]. given #101 (T,wt=11): 70 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. given #102 (A,wt=23): 49 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(15(a,1),12(a,1,2))]. given #103 (T,wt=11): 81 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. given #104 (T,wt=11): 85 x ^ (y ^ (z v x)) = y ^ x. [para(18(a,1),17(a,1,2)),flip(a)]. given #105 (T,wt=11): 100 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. given #106 (T,wt=11): 105 x v (y v (z ^ x)) = y v x. [para(24(a,1),15(a,1,2)),flip(a)]. given #107 (A,wt=13): 50 x ^ (y v ((x v z) ^ (x v u))) = x. [back_rewrite(41),rewrite([45(6)]),flip(a)]. given #108 (T,wt=11): 108 x v (y v ((x v y)' v z)) = 1. [para(75(a,1),3(a,1)),flip(a)]. given #109 (T,wt=11): 117 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(79(a,1),5(a,1)),flip(a)]. given #110 (T,wt=11): 121 x v (y v (z v (x v y)')) = 1. [para(87(a,1),3(a,1)),flip(a)]. given #111 (T,wt=11): 125 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(89(a,1),5(a,1)),flip(a)]. given #112 (A,wt=13): 55 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(36),rewrite([51(4)])]. given #113 (T,wt=6): 933 x' != 1 | 0 = x. [para(276(a,1),55(b,1)),rewrite([259(8),276(9)]),flip(a),flip(c),xx(b)]. given #114 (T,wt=10): 934 (x v y)' != 1 | x v y = 0. [para(560(a,1),55(b,1)),rewrite([259(10),560(12)]),flip(a),xx(b)]. given #115 (T,wt=10): 935 (x v y)' != 1 | y v x = 0. [para(2(a,1),934(a,1,1))]. given #116 (T,wt=10): 937 (x ^ y)' != 1 | x ^ y = 0. [para(25(a,1),934(a,1,1)),rewrite([25(8)])]. given #117 (A,wt=17): 61 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_rewrite(54),rewrite([56(7)])]. given #118 (T,wt=10): 940 (x ^ y)' != 1 | y ^ x = 0. [para(4(a,1),937(a,1,1))]. given #119 (T,wt=11): 130 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),113(a,1,2,1))]. given #120 (T,wt=9): 979 (x v y) ^ (y v x)' = 0. [para(58(a,1),130(a,1,2,1))]. given #121 (T,wt=11): 131 x ^ (y ^ ((x ^ y) v z)') = 0. [para(113(a,1),5(a,1)),flip(a)]. given #122 (A,wt=17): 66 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(33(a,1),12(a,1,2,2,2,2)),rewrite([60(5),33(6)])]. given #123 (T,wt=11): 143 x ^ (y ^ (z v (x ^ y))') = 0. [para(129(a,1),5(a,1)),flip(a)]. given #124 (T,wt=11): 145 (x v y) ^ (x v (z v y))' = 0. [para(15(a,1),129(a,1,2,1))]. given #125 (T,wt=11): 151 x v (y v (z v (x v z)')) = 1. [para(29(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #126 (T,wt=11): 156 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(32(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #127 (A,wt=19): 67 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))). [back_rewrite(44),rewrite([64(5)])]. given #128 (T,wt=11): 158 x ^ (y ^ ((x v z) ^ y)') = 0. [para(32(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #129 (T,wt=11): 160 x ^ (y v (z v (x v u))) = x. [para(3(a,1),45(a,1,2))]. given #130 (T,wt=11): 174 ((x ^ y) v z) ^ (x v z)' = 0. [para(22(a,1),129(a,1,2,1))]. given #131 (T,wt=11): 175 x v (y v ((x ^ z) v y)') = 1. [para(29(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #132 (A,wt=19): 68 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_rewrite(62),rewrite([66(9)])]. given #133 (T,wt=11): 176 x v (y v ((x v y) ^ z)') = 1. [para(166(a,1),3(a,1)),flip(a)]. given #134 (T,wt=11): 178 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),166(a,1,2,1))]. given #135 (T,wt=9): 1275 (x ^ y) v (y ^ x)' = 1. [para(53(a,1),178(a,1,2,1))]. given #136 (T,wt=11): 183 x v (y v (z ^ (x v y))') = 1. [para(177(a,1),3(a,1)),flip(a)]. given #137 (A,wt=13): 78 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [para(64(a,1),12(a,1,2,2,2,2)),rewrite([64(5),64(8),70(7)])]. given #138 (T,wt=11): 189 (x ^ y) v (x ^ (z ^ y))' = 1. [para(17(a,1),177(a,1,2,1))]. given #139 (T,wt=11): 190 ((x v y) ^ z) v (x ^ z)' = 1. [para(20(a,1),177(a,1,2,1))]. given #140 (T,wt=11): 196 (x v y) ^ (z ^ x) = z ^ x. [para(53(a,1),20(a,2)),rewrite([195(4)])]. given #141 (T,wt=11): 213 (x v y) ^ (y v x) = x v y. [para(58(a,1),19(a,1,2))]. given #142 (A,wt=13): 82 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(18(a,1),5(a,1)),flip(a)]. given #143 (T,wt=11): 214 (x ^ y) v (z v x) = z v x. [para(58(a,1),22(a,2)),rewrite([210(4)])]. given #144 (T,wt=11): 216 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),71(a,1,2))]. given #145 (T,wt=11): 228 (x ^ y) v (y ^ x) = x ^ y. [para(53(a,1),25(a,1,2))]. given #146 (T,wt=11): 229 x ^ (y v (z v (u v x))) = x. [para(3(a,1),80(a,1,2,2))]. given #147 (A,wt=13): 83 x ^ (y v ((z v x) ^ (x v u))) = x. [para(18(a,1),12(a,1,2,2,1)),rewrite([45(6)]),flip(a)]. given #148 (T,wt=11): 241 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),102(a,1,2,2))]. given #149 (T,wt=11): 250 x v (y v (z v (x' v u))) = 1. [para(3(a,1),111(a,1,2))]. given #150 (T,wt=11): 253 x v (y v ((x ^ z)' v u)) = 1. [para(111(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #151 (T,wt=11): 255 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),119(a,1,2))]. given #152 (A,wt=13): 84 (x v y) ^ (x v (z v y)) = x v y. [para(15(a,1),18(a,1,2))]. given #153 (T,wt=11): 256 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(119(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #154 (T,wt=11): 282 x v ((x v y)' v (z v y)) = 1. [para(15(a,1),275(a,1,2)),rewrite([15(5)])]. given #155 (T,wt=11): 288 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(17(a,1),276(a,1,2)),rewrite([17(5)])]. given #156 (T,wt=11): 292 x ^ ((y v (x v z))' ^ u) = 0. [para(15(a,1),120(a,1,2,1,1))]. given #157 (A,wt=13): 92 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),19(a,1,1))]. given #158 (T,wt=11): 317 x v (y v (z v (u v x'))) = 1. [para(3(a,1),122(a,1,2,2))]. given #159 (T,wt=11): 320 x v (y v (z v (x ^ u)')) = 1. [para(122(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #160 (T,wt=11): 325 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),126(a,1,2,2))]. given #161 (T,wt=11): 326 x ^ (y ^ (z ^ (x v u)')) = 0. [para(126(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #162 (A,wt=13): 93 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),19(a,1,2)),rewrite([3(3)])]. given #163 (T,wt=11): 329 x ^ (y ^ (z v (x v u))') = 0. [para(15(a,1),128(a,1,2,2,1))]. given #164 (T,wt=11): 331 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),133(a,1,2,1))]. given #165 (T,wt=11): 371 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),141(a,1,2,1,2))]. given #166 (T,wt=11): 372 x ^ ((y v (z v x))' ^ u) = 0. [para(141(a,1),5(a,1,1)),rewrite([77(2)]),flip(a)]. given #167 (A,wt=19): 94 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),19(a,1,1)),rewrite([3(5),3(8)])]. given #168 (T,wt=11): 375 x ^ (y ^ (z v (u v x))') = 0. [para(141(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #169 (T,wt=11): 381 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(142(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #170 (T,wt=11): 384 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),146(a,1,2))]. given #171 (T,wt=11): 388 x v (y v ((y v x)' v z)) = 1. [para(147(a,1),3(a,1,1)),rewrite([74(2),3(5)]),flip(a)]. given #172 (A,wt=17): 95 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(19(a,1),5(a,1,1)),flip(a)]. given #173 (T,wt=11): 393 x v (y v (z v (z v x)')) = 1. [para(147(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #174 (T,wt=11): 395 x v (y v (y v (x ^ z))') = 1. [para(147(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. given #175 (T,wt=11): 415 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(153(a,1),5(a,1,1)),rewrite([77(2),5(5)]),flip(a)]. given #176 (T,wt=11): 418 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(153(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #177 (A,wt=19): 96 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(19(a,1),12(a,1,2,2,2)),rewrite([2(4),24(4),56(2)]),flip(a)]. given #178 (T,wt=11): 420 x ^ (y ^ (y ^ (x v z))') = 0. [para(153(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. given #179 (T,wt=11): 425 x v ((y ^ (x ^ z))' v u) = 1. [para(17(a,1),172(a,1,2,1,1))]. given #180 (T,wt=11): 434 x v (y v (z ^ (x ^ u))') = 1. [para(17(a,1),173(a,1,2,2,1))]. given #181 (T,wt=11): 442 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),181(a,1,2,1))]. given #182 (A,wt=19): 97 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(15(a,1),19(a,1,1)),rewrite([3(4)])]. given #183 (T,wt=11): 467 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),182(a,1,2,1,1))]. given #184 (T,wt=11): 471 x v (y v ((z ^ x)' v u)) = 1. [para(182(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #185 (T,wt=11): 482 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),184(a,1,2,1,2))]. given #186 (T,wt=11): 486 x v (y v (z ^ (u ^ x))') = 1. [para(184(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #187 (A,wt=15): 98 (x v y) ^ (x v (z v (y v u))) = x v y. [para(15(a,1),19(a,1,2,2))]. given #188 (T,wt=11): 496 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),188(a,1,2))]. given #189 (T,wt=11): 511 x' v (y v (z v (x v u))) = 1. [para(3(a,1),277(a,1,2))]. given #190 (T,wt=11): 542 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),278(a,1,2))]. given #191 (T,wt=11): 543 x' v (y v (z v (u v x))) = 1. [para(3(a,1),279(a,1,2,2))]. given #192 (A,wt=17): 99 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(19(a,1),17(a,1,2)),flip(a)]. given #193 (T,wt=11): 551 (x ^ (y ^ z))' v (u v y) = 1. [para(71(a,1),279(a,1,2,2))]. given #194 (T,wt=11): 553 (x ^ (y ^ z))' v (u v z) = 1. [para(102(a,1),279(a,1,2,2))]. given #195 (T,wt=11): 559 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),285(a,1,2,2))]. given #196 (T,wt=11): 567 (x v (y v z))' ^ (u ^ y) = 0. [para(45(a,1),285(a,1,2,2))]. given #197 (A,wt=13): 101 x v (y v (z ^ (x v y))) = x v y. [para(24(a,1),3(a,1)),flip(a)]. given #198 (T,wt=11): 568 (x v (y v z))' ^ (u ^ z) = 0. [para(80(a,1),285(a,1,2,2))]. given #199 (T,wt=11): 572 (x ^ y)' v (z v (x v u)) = 1. [para(544(a,1),3(a,1,1)),rewrite([74(2),3(5)]),flip(a)]. given #200 (T,wt=11): 573 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),544(a,1,2))]. given #201 (T,wt=11): 599 (x ^ y)' v (z v (y v u)) = 1. [para(548(a,1),3(a,1,1)),rewrite([74(2),3(5)]),flip(a)]. given #202 (A,wt=13): 103 1 != x | y ^ x != 0 | x' = y ^ x. [para(24(a,1),10(a,1)),rewrite([53(4)]),flip(a)]. given #203 (T,wt=11): 600 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),548(a,1,2))]. given #204 (T,wt=11): 616 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(560(a,1),5(a,1,1)),rewrite([77(2),5(5)]),flip(a)]. given #205 (T,wt=11): 617 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),560(a,1,2))]. given #206 (T,wt=11): 626 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(563(a,1),5(a,1,1)),rewrite([77(2),5(5)]),flip(a)]. given #207 (A,wt=19): 104 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)). [para(24(a,1),12(a,1,2,2,2,2)),rewrite([69(5)]),flip(a)]. given #208 (T,wt=11): 627 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),563(a,1,2))]. given #209 (T,wt=11): 647 (x v (y ^ z)) ^ (x v y)' = 0. [para(46(a,1),129(a,1,2,1))]. given #210 (T,wt=11): 650 x v (y v (x v (y ^ z))') = 1. [para(46(a,1),275(a,1,2)),rewrite([2(5),3(5)])]. given #211 (T,wt=11): 704 (x ^ (y v z)) v (x ^ y)' = 1. [para(70(a,1),177(a,1,2,1))]. given #212 (A,wt=13): 106 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(17(a,1),24(a,1,2))]. given #213 (T,wt=11): 706 x ^ (y ^ (x ^ (y v z))') = 0. [para(70(a,1),276(a,1,2)),rewrite([4(5),5(5)])]. given #214 (T,wt=11): 774 x ^ (y ^ ((z v x) ^ y)') = 0. [para(32(a,1),81(a,1,2)),rewrite([88(2)]),flip(a)]. given #215 (T,wt=11): 776 ((x v y) ^ z) v (y ^ z)' = 1. [para(81(a,1),177(a,1,2,1))]. given #216 (T,wt=11): 777 (x v y) ^ (z ^ y) = z ^ y. [para(53(a,1),81(a,2)),rewrite([195(4)])]. given #217 (A,wt=12): 109 x ^ (x' v y) != 0 | x' v y = x'. [para(75(a,1),10(a,1)),flip(c),xx(a)]. given #218 (T,wt=11): 781 x ^ (y ^ (y ^ (z v x))') = 0. [para(153(a,1),81(a,1,2)),rewrite([88(2)]),flip(a)]. given #219 (T,wt=11): 797 (x ^ (y v z)) v (x ^ z)' = 1. [para(85(a,1),177(a,1,2,1))]. given #220 (T,wt=11): 801 x ^ (y ^ (x ^ (z v y))') = 0. [para(85(a,1),276(a,1,2)),rewrite([4(5),5(5)])]. given #221 (T,wt=11): 821 ((x ^ y) v z) ^ (y v z)' = 0. [para(100(a,1),129(a,1,2,1))]. given #222 (A,wt=17): 110 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z). [para(75(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #223 (T,wt=11): 822 x v (y v ((z ^ x) v y)') = 1. [para(29(a,1),100(a,1,2)),rewrite([86(2)]),flip(a)]. given #224 (T,wt=11): 824 (x ^ y) v (z v y) = z v y. [para(58(a,1),100(a,2)),rewrite([210(4)])]. given #225 (T,wt=11): 831 x v (y v (y v (z ^ x))') = 1. [para(147(a,1),100(a,1,2)),rewrite([86(2)]),flip(a)]. given #226 (T,wt=11): 852 (x v (y ^ z)) ^ (x v z)' = 0. [para(105(a,1),129(a,1,2,1))]. given #227 (A,wt=17): 112 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(20(a,1),5(a,1)),rewrite([5(2)]),flip(a)]. given #228 (T,wt=11): 855 x v (y v (x v (z ^ y))') = 1. [para(105(a,1),275(a,1,2)),rewrite([2(5),3(5)])]. given #229 (T,wt=11): 910 x v (y v (z v (y v x)')) = 1. [para(2(a,1),121(a,1,2,2,2,1))]. given #230 (T,wt=11): 924 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(4(a,1),125(a,1,2,2,2,1))]. given #231 (T,wt=11): 974 (x v y) ^ (y v (x v z))' = 0. [para(2(a,1),130(a,1,1))]. given #232 (A,wt=13): 114 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(15(a,1),20(a,1,2,1))]. given #233 (T,wt=11): 975 (x v y) ^ (y v (z v x))' = 0. [para(2(a,1),130(a,1,2,1)),rewrite([3(3)])]. given #234 (T,wt=11): 982 (x v y) ^ ((y v x)' ^ z) = 0. [para(979(a,1),5(a,1,1)),rewrite([77(2)]),flip(a)]. given #235 (T,wt=11): 984 (x v y) ^ (z ^ (y v x)') = 0. [para(979(a,1),17(a,1,2)),rewrite([88(2)]),flip(a)]. given #236 (T,wt=11): 986 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),131(a,1,2,2,1,1))]. given #237 (A,wt=15): 115 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(20(a,1),17(a,1,2)),flip(a)]. given #238 (T,wt=11): 1041 x ^ (y ^ (z v (y ^ x))') = 0. [para(4(a,1),143(a,1,2,2,1,2))]. given #239 (T,wt=11): 1045 (x v y) ^ (z v (y v x))' = 0. [para(2(a,1),145(a,1,2,1)),rewrite([3(3)])]. given #240 (T,wt=11): 1173 x ^ (y ^ ((y v z) ^ x)') = 0. [para(158(a,1),17(a,1)),flip(a)]. given #241 (T,wt=11): 1175 x ^ ((x v y) ^ (x v z))' = 0. [para(158(a,1),20(a,1)),flip(a)]. given #242 (A,wt=15): 116 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(20(a,1),24(a,1,2)),rewrite([2(4)])]. given #243 (T,wt=11): 1177 x ^ ((x v y) ^ (z v x))' = 0. [para(158(a,1),81(a,1)),flip(a)]. given #244 (T,wt=11): 1191 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),174(a,1,1))]. given #245 (T,wt=11): 1192 ((x ^ y) v z) ^ (z v x)' = 0. [para(2(a,1),174(a,1,2,1))]. given #246 (T,wt=11): 1194 (x v y)' ^ ((x ^ z) v y) = 0. [para(174(a,1),4(a,1)),flip(a)]. given #247 (A,wt=23): 118 x ^ (y v (x' ^ (z ^ (y v u)))) = x ^ (y v (x' ^ (z ^ (x v u)))). [para(79(a,1),12(a,1,2,2,1)),rewrite([5(5),64(6),5(10)])]. given #248 (T,wt=11): 1196 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),174(a,1,2,1))]. given #249 (T,wt=11): 1200 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(24(a,1),174(a,1,2,1))]. given #250 (T,wt=11): 1216 x v (y v ((y ^ z) v x)') = 1. [para(175(a,1),15(a,1)),flip(a)]. given #251 (T,wt=11): 1219 x v ((x ^ y) v (x ^ z))' = 1. [para(175(a,1),22(a,1)),flip(a)]. given #252 (A,wt=12): 123 x ^ (y v x') != 0 | y v x' = x'. [para(87(a,1),10(a,1)),flip(c),xx(a)]. given #253 (T,wt=11): 1227 x v ((x ^ y) v (z ^ x))' = 1. [para(175(a,1),100(a,1)),flip(a)]. given #254 (T,wt=11): 1254 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),176(a,1,2,2,1,1))]. given #255 (T,wt=11): 1268 (x ^ y) v (y ^ (x ^ z))' = 1. [para(4(a,1),178(a,1,1))]. given #256 (T,wt=11): 1269 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),178(a,1,2,1)),rewrite([5(3)])]. given #257 (A,wt=17): 124 x ^ (y v (z ^ (x v (u v y')))) = x ^ (y v z). [para(87(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #258 (T,wt=11): 1284 (x ^ y) v ((y ^ x)' v z) = 1. [para(1275(a,1),3(a,1,1)),rewrite([74(2)]),flip(a)]. given #259 (T,wt=11): 1288 (x ^ y) v (z v (y ^ x)') = 1. [para(1275(a,1),15(a,1,2)),rewrite([86(2)]),flip(a)]. given #260 (T,wt=11): 1300 x v (y v (z ^ (y v x))') = 1. [para(2(a,1),183(a,1,2,2,1,2))]. given #261 (T,wt=11): 1345 (x ^ y) v (z ^ (y ^ x))' = 1. [para(4(a,1),189(a,1,2,1)),rewrite([5(3)])]. given #262 (A,wt=23): 127 x ^ (y v (z ^ (x' ^ (y v u)))) = x ^ (y v (z ^ (x' ^ (x v u)))). [para(89(a,1),12(a,1,2,2,1)),rewrite([5(5),64(6),5(10)])]. given #263 (T,wt=11): 1376 (x ^ y)' v ((x v z) ^ y) = 1. [para(190(a,1),2(a,1)),flip(a)]. given #264 (T,wt=11): 1378 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),190(a,1,1))]. given #265 (T,wt=11): 1379 ((x v y) ^ z) v (z ^ x)' = 1. [para(4(a,1),190(a,1,2,1))]. given #266 (T,wt=11): 1381 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),190(a,1,2,1))]. given #267 (A,wt=23): 132 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))). [para(113(a,1),12(a,1,2,2,1)),rewrite([64(6)])]. given #268 (T,wt=11): 1387 ((x v y) ^ (z v x)) v x' = 1. [para(18(a,1),190(a,1,2,1))]. given #269 (T,wt=11): 1437 (x v y)' ^ (z ^ (y v x)) = 0. [para(213(a,1),285(a,1,2,2))]. given #270 (T,wt=11): 1438 (x v y)' v (z v (y v x)) = 1. [para(213(a,1),548(a,1,1,1))]. given #271 (T,wt=11): 1517 (x ^ y)' v (z v (y ^ x)) = 1. [para(228(a,1),279(a,1,2,2))]. given #272 (A,wt=13): 134 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. given #273 (T,wt=11): 1518 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(228(a,1),563(a,1,1,1))]. given #274 (T,wt=11): 1670 x v ((y v x)' v (z v y)) = 1. [para(2(a,1),282(a,1,2,1,1))]. given #275 (T,wt=11): 1702 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),288(a,1,2,1,1))]. given #276 (T,wt=11): 1985 x v (y v ((z ^ y) v x)') = 1. [para(100(a,1),393(a,1,2))]. given #277 (A,wt=19): 135 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(21(a,1),5(a,1)),rewrite([5(2),5(4)]),flip(a)]. given #278 (T,wt=11): 2002 x v ((y ^ x) v (x ^ z))' = 1. [para(395(a,1),100(a,1)),flip(a)]. given #279 (T,wt=11): 2021 x ^ (y ^ ((z v y) ^ x)') = 0. [para(81(a,1),418(a,1,2))]. given #280 (T,wt=11): 2076 x ^ ((y v x) ^ (x v z))' = 0. [para(420(a,1),81(a,1)),flip(a)]. given #281 (T,wt=11): 2836 (x v y)' ^ (x v (y ^ z)) = 0. [para(647(a,1),4(a,1)),flip(a)]. given #282 (A,wt=15): 136 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(15(a,1),21(a,1,2,2))]. given #283 (T,wt=11): 2870 (x ^ y)' v (x ^ (y v z)) = 1. [para(704(a,1),2(a,1)),flip(a)]. given #284 (T,wt=11): 2955 x ^ ((y v x) ^ (z v x))' = 0. [para(774(a,1),81(a,1)),flip(a)]. given #285 (T,wt=11): 2968 (x ^ y)' v ((z v x) ^ y) = 1. [para(776(a,1),2(a,1)),flip(a)]. given #286 (T,wt=11): 2970 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),776(a,1,1))]. given #287 (A,wt=17): 137 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(21(a,1),17(a,1,2)),flip(a)]. given #288 (T,wt=11): 2971 ((x v y) ^ z) v (z ^ y)' = 1. [para(4(a,1),776(a,1,2,1))]. given #289 (T,wt=11): 2973 ((x v y) ^ (y v z)) v y' = 1. [para(6(a,1),776(a,1,2,1))]. given #290 (T,wt=11): 2979 ((x v y) ^ (z v y)) v y' = 1. [para(18(a,1),776(a,1,2,1))]. given #291 (T,wt=11): 3092 (x ^ y)' v (x ^ (z v y)) = 1. [para(797(a,1),2(a,1)),flip(a)]. given #292 (A,wt=19): 138 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(17(a,1),21(a,1,2,2,1)),rewrite([5(5)])]. given #293 (T,wt=11): 3146 (x v (y ^ z)) ^ (z v x)' = 0. [para(2(a,1),821(a,1,1))]. given #294 (T,wt=11): 3147 ((x ^ y) v z) ^ (z v y)' = 0. [para(2(a,1),821(a,1,2,1))]. given #295 (T,wt=11): 3148 (x v y)' ^ ((z ^ x) v y) = 0. [para(821(a,1),4(a,1)),flip(a)]. given #296 (T,wt=11): 3150 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(7(a,1),821(a,1,2,1))]. given #297 (A,wt=19): 139 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(21(a,1),24(a,1,2)),rewrite([2(5)])]. given #298 (T,wt=11): 3154 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(24(a,1),821(a,1,2,1))]. given #299 (T,wt=11): 3272 x v ((y ^ x) v (z ^ x))' = 1. [para(822(a,1),100(a,1)),flip(a)]. given #300 (T,wt=11): 3382 (x v y)' ^ (x v (z ^ y)) = 0. [para(852(a,1),4(a,1)),flip(a)]. given #301 (T,wt=11): 3877 (x v y)' ^ (y v (x ^ z)) = 0. [para(1191(a,1),4(a,1)),flip(a)]. given #302 (A,wt=15): 140 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(21(a,1),20(a,1,2)),rewrite([20(3)]),flip(a)]. given #303 (T,wt=11): 3906 (x v y)' ^ ((y ^ z) v x) = 0. [para(1192(a,1),4(a,1)),flip(a)]. given #304 (T,wt=11): 3921 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),1194(a,1,1,1))]. given #305 (T,wt=11): 3926 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(24(a,1),1194(a,1,1,1))]. given #306 (T,wt=11): 4109 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(259(a,1),1196(a,1,2)),rewrite([4(6)])]. given #307 (A,wt=23): 144 x ^ (y v ((z v x)' ^ (y v u))) = x ^ (y v ((z v x)' ^ (x v u))). [para(129(a,1),12(a,1,2,2,1)),rewrite([64(6)])]. given #308 (T,wt=11): 4123 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(259(a,1),1200(a,1,2)),rewrite([4(6)])]. given #309 (T,wt=11): 4659 (x ^ y)' v ((y v z) ^ x) = 1. [para(4(a,1),1376(a,1,1,1))]. given #310 (T,wt=11): 4660 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),1376(a,1,2))]. given #311 (T,wt=11): 4662 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),1376(a,1,1,1))]. given #312 (A,wt=13): 148 x v (y v (z v (x v (y v z))')) = 1. [para(29(a,1),3(a,1)),rewrite([3(3)]),flip(a)]. given #313 (T,wt=11): 4666 x' v ((x v y) ^ (z v x)) = 1. [para(18(a,1),1376(a,1,1,1))]. given #314 (T,wt=11): 4793 x v ((x' v y) ^ (x' v z)) = 1. [para(259(a,1),1381(a,1,2)),rewrite([2(6)])]. given #315 (T,wt=11): 4913 x v ((x' v y) ^ (z v x')) = 1. [para(259(a,1),1387(a,1,2)),rewrite([2(6)])]. given #316 (T,wt=11): 5442 (x ^ y)' v ((z v y) ^ x) = 1. [para(4(a,1),2968(a,1,1,1))]. given #317 (A,wt=16): 149 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(29(a,1),10(a,1)),flip(c),xx(a)]. given #318 (T,wt=11): 5443 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),2968(a,1,2))]. given #319 (T,wt=11): 5445 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),2968(a,1,1,1))]. given #320 (T,wt=11): 5449 x' v ((y v x) ^ (z v x)) = 1. [para(18(a,1),2968(a,1,1,1))]. given #321 (T,wt=11): 5700 x v ((y v x') ^ (x' v z)) = 1. [para(259(a,1),2973(a,1,2)),rewrite([2(6)])]. given #322 (A,wt=19): 150 x ^ (y v (z ^ (x v (u v (y v u)')))) = x ^ (y v z). [para(29(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #323 (T,wt=11): 5722 x v ((y v x') ^ (z v x')) = 1. [para(259(a,1),2979(a,1,2)),rewrite([2(6)])]. given #324 (T,wt=11): 5861 (x v y)' ^ (y v (z ^ x)) = 0. [para(3146(a,1),4(a,1)),flip(a)]. given #325 (T,wt=11): 5917 (x v y)' ^ ((z ^ y) v x) = 0. [para(3147(a,1),4(a,1)),flip(a)]. given #326 (T,wt=11): 5962 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(7(a,1),3148(a,1,1,1))]. given #327 (A,wt=13): 152 x v (y v (z v (y v (x v z))')) = 1. [para(15(a,1),29(a,1,2,2,1)),rewrite([3(5)])]. given #328 (T,wt=11): 5967 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(24(a,1),3148(a,1,1,1))]. given #329 (T,wt=11): 5992 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(259(a,1),3150(a,1,2)),rewrite([4(6)])]. given #330 (T,wt=11): 6046 x ^ ((y ^ x') v (z ^ x')) = 0. [para(259(a,1),3154(a,1,2)),rewrite([4(6)])]. given #331 (T,wt=12): 179 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(166(a,1),10(a,1)),flip(c),xx(a)]. given #332 (A,wt=13): 154 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(32(a,1),5(a,1)),rewrite([5(3)]),flip(a)]. given #333 (T,wt=6): 6984 x' != 0 | 1 = x. [para(276(a,1),179(a,1,2,1)),rewrite([76(3),4(3),63(3),276(6),76(5),259(6)])]. given #334 (T,wt=10): 6985 (x v y)' != 0 | x v y = 1. [para(560(a,1),179(a,1,2,1)),rewrite([76(4),4(4),63(4),560(8),76(6),259(8)]),flip(b)]. given #335 (T,wt=10): 6988 (x ^ y)' != 0 | x ^ y = 1. [para(1518(a,1),179(a,1,2,1)),rewrite([76(4),4(4),63(4),1518(9),76(6),259(8)]),flip(b)]. given #336 (T,wt=10): 6998 (x v y)' != 0 | y v x = 1. [para(2(a,1),6985(a,1,1))]. given #337 (A,wt=25): 155 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ (x ^ (y v (z ^ (x v u))))') = 0. [para(12(a,1),32(a,1,2,2,1))]. given #338 (T,wt=10): 7000 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),6988(a,1,1))]. given #339 (T,wt=12): 185 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(177(a,1),10(a,1)),flip(c),xx(a)]. given #340 (T,wt=12): 262 x ^ (x' v y) != 0 | (x' v y)' = x. [para(75(a,1),34(a,1)),rewrite([4(6)]),xx(a)]. given #341 (T,wt=12): 263 x ^ (y v x') != 0 | (y v x')' = x. [para(87(a,1),34(a,1)),rewrite([4(6)]),xx(a)]. given #342 (A,wt=13): 157 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(17(a,1),32(a,1,2,2,1)),rewrite([5(5)])]. given #343 (T,wt=12): 266 x ^ (x ^ y)' != 0 | x ^ y = x. [para(166(a,1),34(a,1)),rewrite([4(6),259(11)]),xx(a)]. given #344 (T,wt=12): 267 x ^ (y ^ x)' != 0 | y ^ x = x. [para(177(a,1),34(a,1)),rewrite([4(6),259(11)]),xx(a)]. given #345 (T,wt=12): 280 x' ^ (y v x) != 0 | y v x = x. [para(275(a,1),10(a,1)),rewrite([259(10)]),flip(c),xx(a)]. given #346 (T,wt=12): 284 (x v y) ^ y' != 0 | (x v y)' = y'. [para(275(a,1),34(a,1)),xx(a)]. given #347 (A,wt=15): 159 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),45(a,1,2,2))]. given #348 (T,wt=12): 303 (x v y) ^ x' != 0 | (x v y)' = x'. [para(87(a,1),35(a,1)),xx(a)]. given #349 (T,wt=12): 672 x' ^ (x v y) != 0 | x v y = x. [para(75(a,1),48(a,1)),rewrite([259(10)]),flip(c),xx(a)]. given #350 (T,wt=12): 3056 x ^ (y v x') != 0 | x' v y = x'. [para(2(a,1),109(a,1,2))]. given #351 (T,wt=12): 4204 x ^ (x' v y) != 0 | y v x' = x'. [para(2(a,1),123(a,1,2))]. given #352 (A,wt=15): 161 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(45(a,1),12(a,1,2,2,1)),rewrite([45(7)]),flip(a)]. given #353 (T,wt=12): 6982 x ^ (y ^ x)' != 0 | (x ^ y)' = x'. [para(4(a,1),179(a,1,2,1))]. given #354 (T,wt=12): 7055 x ^ (x ^ y)' != 0 | (y ^ x)' = x'. [para(4(a,1),185(a,1,2,1))]. given #355 (T,wt=12): 7066 x ^ (y v x') != 0 | (x' v y)' = x. [para(2(a,1),262(a,1,2))]. given #356 (T,wt=12): 7070 x' ^ (x v y) != 0 | (x v y)' = x'. [para(259(a,1),262(a,1,2,1)),rewrite([259(7)])]. given #357 (A,wt=13): 162 x ^ (y ^ (z v (x v u))) = y ^ x. [para(45(a,1),17(a,1,2)),flip(a)]. given #358 (T,wt=12): 7086 x ^ (x' v y) != 0 | (y v x')' = x. [para(2(a,1),263(a,1,2))]. given #359 (T,wt=12): 7088 x' ^ (y v x) != 0 | (y v x)' = x'. [para(259(a,1),263(a,1,2,2)),rewrite([259(7)])]. given #360 (T,wt=12): 7115 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),266(a,1,2,1))]. given #361 (T,wt=12): 7121 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),267(a,1,2,1))]. given #362 (A,wt=13): 163 x v (y v (x v z)) = y v (x v z). [para(45(a,1),24(a,1,2)),rewrite([2(3)])]. given #363 (T,wt=12): 7123 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),267(a,1,2,1)),rewrite([6(7)]),flip(b)]. given #364 (T,wt=12): 7125 (x v y) ^ y' != 0 | x v y = y. [para(18(a,1),267(a,1,2,1)),rewrite([18(7)]),flip(b)]. given #365 (T,wt=12): 7145 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),280(a,1,2))]. given #366 (T,wt=12): 7154 (x v y) ^ x' != 0 | (y v x)' = x'. [para(2(a,1),284(a,1,1))]. given #367 (A,wt=17): 164 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(22(a,1),3(a,1)),rewrite([3(2)]),flip(a)]. given #368 (T,wt=12): 7201 (x v y) ^ y' != 0 | (y v x)' = y'. [para(2(a,1),303(a,1,1))]. given #369 (T,wt=12): 7203 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),672(a,1,2))]. given #370 (T,wt=12): 7300 x' ^ (y v x) != 0 | (x v y)' = x'. [para(259(a,1),7066(a,1,2,2)),rewrite([259(7)])]. given #371 (T,wt=12): 7389 x' ^ (x v y) != 0 | (y v x)' = x'. [para(259(a,1),7086(a,1,2,1)),rewrite([259(7)])]. given #372 (A,wt=17): 165 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),22(a,1,2,1))]. given #373 (T,wt=12): 7411 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),7123(a,1,1))]. given #374 (T,wt=12): 7414 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),7125(a,1,1))]. given #375 (T,wt=13): 170 x v ((y ^ (x ^ z)) v u) = x v u. [para(17(a,1),22(a,1,2,1))]. given #376 (T,wt=13): 191 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(21(a,1),177(a,1,2,1))]. given #377 (A,wt=21): 167 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(22(a,1),10(a,1))]. given #378 (T,wt=12): 7811 x v (y v x)' != 1 | y v x = x. [para(3148(a,1),167(b,1)),rewrite([2(3),259(11),4(12),113(12),64(11)]),xx(b)]. given #379 (T,wt=12): 7813 x v (x v y)' != 1 | x v y = x. [para(5917(a,1),167(b,1)),rewrite([2(3),259(11),4(12),129(12),64(11)]),xx(b)]. given #380 (T,wt=12): 7814 x' v (x ^ y) != 1 | x ^ y = x. [para(5962(a,1),167(b,1)),rewrite([259(10),4(10),9(10),64(11)]),flip(c),xx(b)]. given #381 (T,wt=12): 7815 x' v (y ^ x) != 1 | y ^ x = x. [para(5967(a,1),167(b,1)),rewrite([259(10),4(10),9(10),64(11)]),flip(c),xx(b)]. given #382 (A,wt=23): 168 x ^ (y v (z ^ (x v ((y ^ u) v v)))) = x ^ (y v (z ^ (x v v))). [para(22(a,1),12(a,1,2,2,2,2)),rewrite([12(6)]),flip(a)]. given #383 (T,wt=12): 7816 x v (x' ^ y) != 1 | x' ^ y = x'. [para(5992(a,1),167(b,1)),rewrite([9(11),64(13)]),flip(c),xx(b)]. given #384 (T,wt=12): 7817 x v (y ^ x') != 1 | y ^ x' = x'. [para(6046(a,1),167(b,1)),rewrite([9(11),64(13)]),flip(c),xx(b)]. given #385 (T,wt=12): 7818 x v (x v y)' != 1 | y v x = x. [para(2(a,1),7811(a,1,2,1))]. given #386 (T,wt=12): 7821 (x ^ y) v x' != 1 | x ^ y = x. [para(7(a,1),7811(a,1,2,1)),rewrite([7(7)]),flip(b)]. given #387 (A,wt=15): 169 x v (y v ((x ^ z) v u)) = y v (x v u). [para(22(a,1),15(a,1,2)),flip(a)]. given #388 (T,wt=12): 7823 (x ^ y) v y' != 1 | x ^ y = y. [para(24(a,1),7811(a,1,2,1)),rewrite([24(7)]),flip(b)]. given #389 (T,wt=12): 7837 x v (y v x)' != 1 | x v y = x. [para(2(a,1),7813(a,1,2,1))]. given #390 (T,wt=12): 7845 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),7814(a,1,2))]. given #391 (T,wt=12): 7853 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),7815(a,1,2))]. given #392 (A,wt=15): 171 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite([4(4)])]. given #393 (T,wt=12): 7955 x v (y ^ x') != 1 | x' ^ y = x'. [para(4(a,1),7816(a,1,2))]. given #394 (T,wt=12): 7961 x v (x' ^ y) != 1 | y ^ x' = x'. [para(4(a,1),7817(a,1,2))]. given #395 (T,wt=12): 7965 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),7821(a,1,1))]. given #396 (T,wt=12): 8036 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),7823(a,1,1))]. given #397 (A,wt=17): 180 x ^ (y v (z ^ (x v (y ^ u)'))) = x ^ (y v z). [para(166(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #398 (T,wt=13): 193 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(51(a,1),5(a,2,2)),rewrite([17(3),5(2)])]. given #399 (T,wt=13): 195 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),53(a,1,2)),rewrite([5(5)])]. given #400 (T,wt=13): 197 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),23(a,1,2,2,1))]. given #401 (T,wt=13): 205 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(23(a,1),129(a,1,2,1))]. given #402 (A,wt=17): 186 x ^ (y v (z ^ (x v (u ^ y)'))) = x ^ (y v z). [para(177(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #403 (T,wt=13): 207 x v y != 1 | 0 != x | x' = x v y. [para(56(a,1),10(a,1)),rewrite([6(5)]),flip(b)]. given #404 (T,wt=13): 210 x v (y v (z v x)) = y v (z v x). [para(3(a,1),58(a,1,2)),rewrite([3(5)])]. given #405 (T,wt=13): 211 x v y != 1 | 0 != y | y' = x v y. [para(58(a,1),10(a,1)),rewrite([18(5)]),flip(b)]. given #406 (T,wt=13): 219 x v (y v (z ^ (x ^ u))) = y v x. [para(71(a,1),15(a,1,2)),flip(a)]. given #407 (A,wt=23): 187 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u))))')) = 1. [para(12(a,1),177(a,1,2,1)),rewrite([3(11),3(10)])]. given #408 (T,wt=13): 220 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),25(a,1,1))]. given #409 (T,wt=13): 221 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),25(a,1,2)),rewrite([5(3)])]. given #410 (T,wt=13): 230 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(80(a,1),5(a,1,1)),flip(a)]. given #411 (T,wt=13): 235 x ^ (y ^ (z v (u v x))) = y ^ x. [para(80(a,1),17(a,1,2)),flip(a)]. given #412 (A,wt=19): 198 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(23(a,1),3(a,1)),rewrite([3(2),3(4)]),flip(a)]. given #413 (T,wt=13): 239 x v ((y ^ (z ^ x)) v u) = x v u. [para(102(a,1),3(a,1,1)),flip(a)]. given #414 (T,wt=13): 244 x v (y v (z ^ (u ^ x))) = y v x. [para(102(a,1),15(a,1,2)),flip(a)]. given #415 (T,wt=13): 249 x v (y v (z v ((x v y)' v u))) = 1. [para(111(a,1),3(a,1)),flip(a)]. given #416 (T,wt=13): 254 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0. [para(119(a,1),5(a,1)),flip(a)]. given #417 (A,wt=25): 199 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x' = y v ((x v y) ^ z). [para(23(a,1),10(a,1))]. given #418 (T,wt=13): 258 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),34(a,1)),rewrite([4(4),51(4)]),flip(a)]. given #419 (T,wt=13): 261 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(24(a,1),34(a,1)),rewrite([4(4),53(4)]),flip(a)]. given #420 (T,wt=13): 269 x v y != 1 | 0 != x | (x v y)' = x. [para(56(a,1),34(a,1)),rewrite([4(5),6(5)]),flip(b)]. given #421 (T,wt=13): 270 x v y != 1 | 0 != y | (x v y)' = y. [para(58(a,1),34(a,1)),rewrite([4(5),18(5)]),flip(b)]. given #422 (A,wt=25): 200 x ^ (y v (z ^ (x v (u v ((y v u) ^ v))))) = x ^ (y v (z ^ (x v u))). [para(23(a,1),12(a,1,2,2,2,2)),rewrite([12(6)]),flip(a)]. given #423 (T,wt=13): 283 x v (y v (y v ((x v y) ^ z))') = 1. [para(23(a,1),275(a,1,2)),rewrite([2(6),3(6)])]. given #424 (T,wt=13): 289 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(21(a,1),276(a,1,2)),rewrite([4(6),5(6)])]. given #425 (T,wt=13): 290 (x v y) ^ ((x v (y v z))' ^ u) = 0. [para(3(a,1),120(a,1,2,1,1))]. given #426 (T,wt=13): 291 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0. [para(120(a,1),5(a,1)),flip(a)]. given #427 (A,wt=17): 201 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(23(a,1),15(a,1,2)),flip(a)]. given #428 (T,wt=13): 310 x v y != 1 | 0 != y | (y v x)' = y. [para(58(a,1),35(a,1)),rewrite([4(5),6(5)]),flip(b)]. given #429 (T,wt=13): 316 x v (y v (z v (u v (x v y)'))) = 1. [para(122(a,1),3(a,1)),flip(a)]. given #430 (T,wt=13): 324 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0. [para(126(a,1),5(a,1)),flip(a)]. given #431 (T,wt=13): 327 (x v y) ^ (z ^ (x v (y v u))') = 0. [para(3(a,1),128(a,1,2,2,1))]. given #432 (A,wt=19): 202 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(15(a,1),23(a,1,2,2,1)),rewrite([3(5)])]. given #433 (T,wt=13): 328 x ^ (y ^ (z ^ ((x ^ y) v u)')) = 0. [para(128(a,1),5(a,1)),flip(a)]. given #434 (T,wt=13): 330 (x v y) ^ (z v (x v (y v u)))' = 0. [para(3(a,1),133(a,1,2,1,2))]. given #435 (T,wt=13): 332 x ^ (y ^ (z v ((x ^ y) v u))') = 0. [para(133(a,1),5(a,1)),flip(a)]. given #436 (T,wt=13): 373 x ^ (y ^ (z v (u v (x ^ y)))') = 0. [para(141(a,1),5(a,1)),flip(a)]. given #437 (A,wt=15): 203 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(17(a,1),23(a,1,2,2))]. given #438 (T,wt=13): 374 (x v y) ^ (z v (x v (u v y)))' = 0. [para(15(a,1),141(a,1,2,1,2))]. given #439 (T,wt=13): 376 ((x ^ y) v z) ^ (u v (x v z))' = 0. [para(22(a,1),141(a,1,2,1,2))]. given #440 (T,wt=13): 378 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0. [para(25(a,1),141(a,1,2,1,2)),rewrite([5(6),5(5)])]. given #441 (T,wt=13): 379 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0. [para(142(a,1),5(a,1)),flip(a)]. given #442 (A,wt=19): 204 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(23(a,1),18(a,1,2)),rewrite([4(5)])]. given #443 (T,wt=13): 380 (x v y) ^ ((x v (z v y))' ^ u) = 0. [para(15(a,1),142(a,1,2,1,1))]. given #444 (T,wt=13): 382 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0. [para(22(a,1),142(a,1,2,1,1))]. given #445 (T,wt=13): 385 (x v y) ^ (z ^ (x v (u v y))') = 0. [para(15(a,1),146(a,1,2,2,1))]. given #446 (T,wt=13): 386 ((x ^ y) v z) ^ (u ^ (x v z)') = 0. [para(22(a,1),146(a,1,2,2,1))]. given #447 (A,wt=15): 206 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(23(a,1),22(a,1,2)),rewrite([22(3)]),flip(a)]. given #448 (T,wt=13): 389 x v (y v (z v (z v (x v y))')) = 1. [para(147(a,1),3(a,1)),flip(a)]. given #449 (T,wt=13): 390 x v (y v (z v (y v (z v x))')) = 1. [para(3(a,1),147(a,1,2,2,1)),rewrite([3(5)])]. given #450 (T,wt=13): 394 x v (y v (z v (x v (z v y))')) = 1. [para(15(a,1),147(a,1,2,2,1)),rewrite([3(6)])]. given #451 (T,wt=13): 403 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(64(a,1),38(a,1,2,2,1,2)),rewrite([64(5),64(8),70(7)])]. given #452 (A,wt=21): 208 x ^ (y v (z ^ (x v (y v u)))) = x ^ (y v (z ^ (x v u))). [para(56(a,1),12(a,1,2,2,2,2)),rewrite([12(6)]),flip(a)]. given #453 (T,wt=13): 416 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0. [para(153(a,1),5(a,1)),flip(a)]. given #454 (T,wt=13): 417 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0. [para(5(a,1),153(a,1,2,2,1)),rewrite([5(5)])]. given #455 (T,wt=13): 419 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0. [para(17(a,1),153(a,1,2,2,1)),rewrite([5(6)])]. given #456 (T,wt=13): 421 x v (y v (((x v y) ^ z)' v u)) = 1. [para(172(a,1),3(a,1)),flip(a)]. given #457 (A,wt=21): 212 x ^ (y v (z ^ (x v (u v y)))) = x ^ (y v (z ^ (x v u))). [para(58(a,1),12(a,1,2,2,2,2)),rewrite([37(6)]),flip(a)]. given #458 (T,wt=13): 422 (x ^ y) v ((x ^ (y ^ z))' v u) = 1. [para(5(a,1),172(a,1,2,1,1))]. given #459 (T,wt=13): 430 x v (y v (z v ((x v y) ^ u)')) = 1. [para(173(a,1),3(a,1)),flip(a)]. given #460 (T,wt=13): 431 (x ^ y) v (z v (x ^ (y ^ u))') = 1. [para(5(a,1),173(a,1,2,2,1))]. given #461 (T,wt=13): 440 x v (y v (z ^ ((x v y) ^ u))') = 1. [para(181(a,1),3(a,1)),flip(a)]. given #462 (A,wt=15): 215 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),71(a,1,2,2))]. given #463 (T,wt=13): 441 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1. [para(5(a,1),181(a,1,2,1,2))]. given #464 (T,wt=13): 452 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(64(a,1),39(a,1,2,2,2,2)),rewrite([64(5),64(8),70(7)])]. given #465 (T,wt=13): 466 x v (y v ((z ^ (x v y))' v u)) = 1. [para(182(a,1),3(a,1)),flip(a)]. given #466 (T,wt=13): 472 (x ^ y) v ((x ^ (z ^ y))' v u) = 1. [para(17(a,1),182(a,1,2,1,1))]. Low Water (keep, True_semantics): wt=25 given #467 (A,wt=17): 217 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(71(a,1),10(a,1)),rewrite([193(5)]),flip(a)]. given #468 (T,wt=13): 473 ((x v y) ^ z) v ((x ^ z)' v u) = 1. [para(20(a,1),182(a,1,2,1,1))]. given #469 (T,wt=13): 481 x v (y v (z ^ (u ^ (x v y)))') = 1. [para(184(a,1),3(a,1)),flip(a)]. given #470 (T,wt=13): 487 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1. [para(17(a,1),184(a,1,2,1,2))]. given #471 (T,wt=13): 488 x v (y v (z v (u ^ (x v y))')) = 1. [para(19(a,1),184(a,1,2,1,2)),rewrite([3(6),3(5)])]. given #472 (A,wt=19): 222 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),25(a,1,1)),rewrite([5(5),5(8)])]. given #473 (T,wt=13): 489 ((x v y) ^ z) v (u ^ (x ^ z))' = 1. [para(20(a,1),184(a,1,2,1,2))]. given #474 (T,wt=13): 500 (x ^ y) v (z v (x ^ (u ^ y))') = 1. [para(17(a,1),188(a,1,2,2,1))]. given #475 (T,wt=13): 501 ((x v y) ^ z) v (u v (x ^ z)') = 1. [para(20(a,1),188(a,1,2,2,1))]. given #476 (T,wt=13): 510 (x v y)' v (z v (x v (y v u))) = 1. [para(3(a,1),277(a,1,2,2))]. given #477 (A,wt=21): 223 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [para(25(a,1),10(a,1)),rewrite([17(7),17(6),5(5),193(6),51(6)])]. given #478 (T,wt=13): 522 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(64(a,1),40(a,1,2,2,2,1)),rewrite([64(5),64(8),70(7)])]. given #479 (T,wt=13): 541 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0. [para(5(a,1),278(a,1,2,2))]. given #480 (T,wt=13): 547 (x v y)' v (z v (x v (u v y))) = 1. [para(15(a,1),279(a,1,2,2))]. given #481 (T,wt=13): 549 ((x ^ y) v z)' v (u v (x v z)) = 1. [para(22(a,1),279(a,1,2,2))]. given #482 (A,wt=17): 225 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(25(a,1),15(a,1,2)),flip(a)]. given #483 (T,wt=13): 552 (x ^ (y ^ z))' v (u v (x ^ y)) = 1. [para(25(a,1),279(a,1,2,2))]. given #484 (T,wt=13): 562 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0. [para(17(a,1),285(a,1,2,2))]. given #485 (T,wt=13): 564 (x v (y v z))' ^ (u ^ (x v y)) = 0. [para(19(a,1),285(a,1,2,2))]. given #486 (T,wt=13): 565 ((x v y) ^ z)' ^ (u ^ (x ^ z)) = 0. [para(20(a,1),285(a,1,2,2))]. given #487 (A,wt=19): 226 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(17(a,1),25(a,1,1)),rewrite([5(4)])]. given #488 (T,wt=13): 576 x v (((x v y) ^ z)' v (u v y)) = 1. [para(15(a,1),544(a,1,2)),rewrite([15(6)])]. given #489 (T,wt=13): 577 x v (y v (((x ^ z) v y) ^ u)') = 1. [para(22(a,1),544(a,1,2)),rewrite([2(6),3(6)])]. given #490 (T,wt=13): 589 x' ^ (x v (y ^ x')) = x' ^ (x v y). [para(27(a,1),43(a,1,2,2,2))]. given #491 (T,wt=9): 12014 x' ^ (x v (x' v y)') = 0. [para(132(a,1),589(a,2)),rewrite([4(8),120(8),33(3),4(2),9(2),3205(10)]),flip(a)]. given #492 (A,wt=15): 227 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(17(a,1),25(a,1,2,2))]. given #493 (T,wt=7): 12073 x v (x' v y)' = x. [hyper(7145,a,12014,a),rewrite([2(4)])]. given #494 (T,wt=7): 12161 x v (y v x')' = x. [para(2(a,1),12073(a,1,2,1))]. given #495 (T,wt=7): 12172 x' v (x v y)' = x'. [para(259(a,1),12073(a,1,2,1,1))]. given #496 (T,wt=7): 12265 x' v (y v x)' = x'. [para(259(a,1),12161(a,1,2,1,2))]. given #497 (A,wt=15): 231 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(80(a,1),5(a,1)),flip(a)]. given #498 (T,wt=9): 12167 x v (y v (x' v z))' = x. [para(15(a,1),12073(a,1,2,1))]. given #499 (T,wt=9): 12168 x ^ (x' v y)' = (x' v y)'. [para(12073(a,1),18(a,1,2)),rewrite([4(4)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 111 (0.00 of 6.72 sec). given #500 (T,wt=9): 12169 x v ((x ^ y)' v z)' = x. [para(12073(a,1),22(a,1,2)),rewrite([7(2)]),flip(a)]. given #501 (T,wt=9): 12174 (x' v y)' ^ (z v x)' = 0. [para(12073(a,1),141(a,1,2,1,2))]. given #502 (A,wt=15): 232 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(80(a,1),12(a,1,2,2,1)),rewrite([45(7)]),flip(a)]. given #503 (T,wt=9): 12176 x v ((x' v y)' ^ z)' = 1. [para(12073(a,1),544(a,1,2)),rewrite([2(6)])]. given #504 (T,wt=9): 12177 x v (y ^ (x' v z)')' = 1. [para(12073(a,1),548(a,1,2)),rewrite([2(6)])]. given #505 (T,wt=9): 12182 x v ((y ^ x)' v z)' = x. [para(12073(a,1),100(a,1,2)),rewrite([24(2)]),flip(a)]. given #506 (T,wt=9): 12186 x v ((x' v y)' ^ z) = x. [para(12073(a,1),214(a,1,2)),rewrite([2(5),12073(9)])]. given #507 (A,wt=15): 234 (x v y) ^ (z v (x v (u v y))) = x v y. [para(15(a,1),80(a,1,2,2))]. given #508 (T,wt=9): 12207 x v (y ^ (x' v z)') = x. [para(12073(a,1),824(a,1,2)),rewrite([2(5),12073(9)])]. given #509 (T,wt=9): 12234 x v (y v (z v x'))' = x. [para(210(a,1),12073(a,1,2,1))]. given #510 (T,wt=9): 12261 x ^ (y v x')' = (y v x')'. [para(12161(a,1),18(a,1,2)),rewrite([4(4)])]. given #511 (T,wt=9): 12262 x v (y v (x ^ z)')' = x. [para(12161(a,1),22(a,1,2)),rewrite([7(2)]),flip(a)]. given #512 (A,wt=17): 236 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(22(a,1),80(a,1,2,2))]. Low Water (keep, True_semantics): wt=24 given #513 (T,wt=9): 12267 (x v y')' ^ (z v y)' = 0. [para(12161(a,1),141(a,1,2,1,2))]. given #514 (T,wt=9): 12269 x v ((y v x')' ^ z)' = 1. [para(12161(a,1),544(a,1,2)),rewrite([2(6)])]. given #515 (T,wt=9): 12270 x v (y ^ (z v x')')' = 1. [para(12161(a,1),548(a,1,2)),rewrite([2(6)])]. given #516 (T,wt=9): 12275 x v (y v (z ^ x)')' = x. [para(12161(a,1),100(a,1,2)),rewrite([24(2)]),flip(a)]. given #517 (A,wt=21): 237 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(23(a,1),80(a,1,2,2))]. given #518 (T,wt=9): 12280 x v ((y v x')' ^ z) = x. [para(12161(a,1),214(a,1,2)),rewrite([2(5),12161(9)])]. Low Water (keep, True_semantics): wt=23 given #519 (T,wt=9): 12301 x v (y ^ (z v x')') = x. [para(12161(a,1),824(a,1,2)),rewrite([2(5),12161(9)])]. given #520 (T,wt=9): 12358 x' v (y v (x v z))' = x'. [para(15(a,1),12172(a,1,2,1))]. given #521 (T,wt=9): 12359 x' ^ (x v y)' = (x v y)'. [para(12172(a,1),18(a,1,2)),rewrite([4(4)])]. given #522 (A,wt=17): 238 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(25(a,1),80(a,1,2,2)),rewrite([5(5),5(4)])]. given #523 (T,wt=9): 12363 (x v y)' ^ (z v x')' = 0. [para(12172(a,1),141(a,1,2,1,2))]. given #524 (T,wt=9): 12365 x' v ((x v y)' ^ z)' = 1. [para(12172(a,1),544(a,1,2)),rewrite([2(6)])]. given #525 (T,wt=9): 12366 x' v (y ^ (x v z)')' = 1. [para(12172(a,1),548(a,1,2)),rewrite([2(6)])]. given #526 (T,wt=9): 12375 x' v ((x v y)' ^ z) = x'. [para(12172(a,1),214(a,1,2)),rewrite([2(5),12172(9)])]. given #527 (A,wt=15): 240 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(102(a,1),3(a,1)),flip(a)]. given #528 (T,wt=9): 12397 x' v (y ^ (x v z)') = x'. [para(12172(a,1),824(a,1,2)),rewrite([2(5),12172(9)])]. given #529 (T,wt=9): 12423 x' != 1 | x' != 0 | x' = x. [para(12172(a,1),207(a,1)),rewrite([259(8),12172(10)]),flip(b),flip(c)]. given #530 (T,wt=9): 12425 x' v (y v (z v x))' = x'. [para(210(a,1),12172(a,1,2,1))]. given #531 (T,wt=9): 12453 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),12265(a,1,2,1)),rewrite([2(4)])]. given #532 (A,wt=17): 242 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(102(a,1),10(a,1)),rewrite([195(5)]),flip(a)]. given #533 (T,wt=7): 14769 x' ^ (x ^ y)' = x'. [para(12453(a,1),6(a,1,2))]. given #534 (T,wt=7): 14873 x' ^ (y ^ x)' = x'. [para(4(a,1),14769(a,1,2,1))]. given #535 (T,wt=7): 14877 x ^ (x' ^ y)' = x. [para(259(a,1),14769(a,1,1)),rewrite([259(6)])]. given #536 (T,wt=7): 14921 x ^ (y ^ x')' = x. [para(259(a,1),14873(a,1,1)),rewrite([259(6)])]. given #537 (A,wt=15): 245 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(17(a,1),102(a,1,2,2))]. given #538 (T,wt=9): 12458 x' ^ (y v x)' = (y v x)'. [para(12265(a,1),18(a,1,2)),rewrite([4(4)])]. given #539 (T,wt=9): 12459 x' v (y ^ x)' = (y ^ x)'. [para(24(a,1),12265(a,1,2,1)),rewrite([2(4)])]. given #540 (T,wt=9): 12468 (x v y)' ^ (z v y')' = 0. [para(12265(a,1),141(a,1,2,1,2))]. given #541 (T,wt=9): 12470 x' v ((y v x)' ^ z)' = 1. [para(12265(a,1),544(a,1,2)),rewrite([2(6)])]. given #542 (A,wt=17): 246 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(19(a,1),102(a,1,2,2)),rewrite([3(5),3(4)])]. given #543 (T,wt=9): 12471 x' v (y ^ (z v x)')' = 1. [para(12265(a,1),548(a,1,2)),rewrite([2(6)])]. given #544 (T,wt=9): 12483 x' v ((y v x)' ^ z) = x'. [para(12265(a,1),214(a,1,2)),rewrite([2(5),12265(9)])]. given #545 (T,wt=9): 12506 x' v (y ^ (z v x)') = x'. [para(12265(a,1),824(a,1,2)),rewrite([2(5),12265(9)])]. given #546 (T,wt=9): 12732 x ^ (y' v (x ^ y))' = 0. [para(12168(a,1),143(a,1,2))]. given #547 (A,wt=17): 247 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(20(a,1),102(a,1,2,2))]. given #548 (T,wt=9): 12744 x ^ (y' v (y ^ x))' = 0. [para(12168(a,1),1041(a,1,2))]. given #549 (T,wt=9): 12803 x' ^ ((x ^ y)' v z)' = 0. [para(12169(a,1),129(a,1,2,1)),rewrite([4(6)])]. given #550 (T,wt=9): 12886 (x' v y)' ^ (x v z)' = 0. [para(2(a,1),12174(a,1,2,1))]. given #551 (T,wt=9): 12887 (x v y)' ^ (y' v z)' = 0. [para(12174(a,1),4(a,1)),flip(a)]. given #552 (A,wt=21): 248 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(21(a,1),102(a,1,2,2))]. given #553 (T,wt=9): 12889 x' ^ ((y ^ x)' v z)' = 0. [para(24(a,1),12174(a,1,2,1)),rewrite([4(6)])]. given #554 (T,wt=9): 13468 x ^ ((x ^ y) v y')' = 0. [para(12261(a,1),131(a,1,2))]. given #555 (T,wt=9): 13479 x ^ ((y ^ x) v y')' = 0. [para(12261(a,1),986(a,1,2))]. given #556 (T,wt=9): 13530 x' ^ ((x ^ y)' v z) = x'. [para(12169(a,1),12261(a,1,2,1)),rewrite([4(5),12169(10)])]. Low Water (keep, True_semantics): wt=21 given #557 (A,wt=16): 251 x ^ (y v (x' v z)) != 0 | y v (x' v z) = x'. [para(111(a,1),10(a,1)),flip(c),xx(a)]. given #558 (T,wt=9): 13531 x' ^ ((y ^ x)' v z) = x'. [para(12182(a,1),12261(a,1,2,1)),rewrite([4(5),12182(10)])]. given #559 (T,wt=9): 13537 x' ^ (y v (x ^ z)')' = 0. [para(12262(a,1),129(a,1,2,1)),rewrite([4(6)])]. given #560 (T,wt=9): 13617 x' ^ (y v (x ^ z)') = x'. [para(12262(a,1),12261(a,1,2,1)),rewrite([4(5),12262(10)])]. given #561 (T,wt=9): 13707 (x v y')' ^ (y v z)' = 0. [para(2(a,1),12267(a,1,2,1))]. given #562 (A,wt=19): 252 x ^ (y v (z ^ (x v (u v (y' v v))))) = x ^ (y v z). [para(111(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #563 (T,wt=9): 13709 x' ^ (y v (z ^ x)')' = 0. [para(24(a,1),12267(a,1,2,1)),rewrite([4(6)])]. given #564 (T,wt=9): 13925 x' ^ (y v (z ^ x)') = x'. [para(12275(a,1),12261(a,1,2,1)),rewrite([4(5),12275(10)])]. given #565 (T,wt=9): 14243 x ^ (y v (x ^ y'))' = 0. [para(12359(a,1),143(a,1,2))]. given #566 (T,wt=9): 14257 x ^ (y v (y' ^ x))' = 0. [para(12359(a,1),1041(a,1,2))]. given #567 (A,wt=19): 257 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),34(a,1))]. given #568 (T,wt=9): 14394 (x v y)' ^ (x' v z)' = 0. [para(2(a,1),12363(a,1,2,1))]. given #569 (T,wt=9): 14774 x v (x' ^ y)' = (x' ^ y)'. [para(259(a,1),12453(a,1,1))]. given #570 (T,wt=9): 14788 x v (y ^ (x v y'))' = 1. [para(12453(a,1),183(a,1,2))]. given #571 (T,wt=9): 14820 x v (y ^ (y' v x))' = 1. [para(12453(a,1),1300(a,1,2))]. given #572 (A,wt=19): 260 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(15(a,1),34(a,1))]. given #573 (T,wt=9): 14875 x' ^ (y ^ (x ^ z))' = x'. [para(17(a,1),14769(a,1,2,1))]. given #574 (T,wt=9): 14878 (x ^ y)' v (z ^ x')' = 1. [para(14769(a,1),184(a,1,2,1,2))]. given #575 (T,wt=9): 14901 x' ^ (y ^ (z ^ x))' = x'. [para(195(a,1),14769(a,1,2,1))]. given #576 (T,wt=9): 14922 (x ^ y)' v (z ^ y')' = 1. [para(14873(a,1),184(a,1,2,1,2))]. given #577 (A,wt=16): 264 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x. [para(29(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #578 (T,wt=9): 15003 x ^ (y ^ (x' ^ z))' = x. [para(17(a,1),14877(a,1,2,1))]. given #579 (T,wt=9): 15004 x ^ ((x v y)' ^ z)' = x. [para(14877(a,1),20(a,1,2)),rewrite([6(2)]),flip(a)]. given #580 (T,wt=9): 15007 (x' ^ y)' v (z ^ x)' = 1. [para(14877(a,1),184(a,1,2,1,2))]. given #581 (T,wt=9): 15008 x ^ ((x' ^ y)' v z)' = 0. [para(14877(a,1),560(a,1,2)),rewrite([4(6)])]. given #582 (A,wt=21): 265 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x. [para(22(a,1),34(a,1)),rewrite([4(6)])]. given #583 (T,wt=9): 15009 x ^ (y v (x' ^ z)')' = 0. [para(14877(a,1),563(a,1,2)),rewrite([4(6)])]. given #584 (T,wt=9): 15010 x ^ ((y v x)' ^ z)' = x. [para(14877(a,1),81(a,1,2)),rewrite([18(2)]),flip(a)]. given #585 (T,wt=9): 15015 x ^ ((x' ^ y)' v z) = x. [para(14877(a,1),196(a,1,2)),rewrite([4(5),14877(9)])]. given #586 (T,wt=9): 15030 x ^ (y v (x' ^ z)') = x. [para(14877(a,1),777(a,1,2)),rewrite([4(5),14877(9)])]. given #587 (A,wt=25): 268 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x. [para(23(a,1),34(a,1)),rewrite([4(7)])]. given #588 (T,wt=9): 15056 x ^ (y ^ (z ^ x'))' = x. [para(195(a,1),14877(a,1,2,1))]. given #589 (T,wt=9): 15077 x v (y ^ x')' = (y ^ x')'. [para(14921(a,1),24(a,1,2)),rewrite([2(4)])]. given #590 (T,wt=9): 15078 x ^ (y ^ (x v z)')' = x. [para(14921(a,1),20(a,1,2)),rewrite([6(2)]),flip(a)]. given #591 (T,wt=9): 15081 (x ^ y')' v (z ^ y)' = 1. [para(14921(a,1),184(a,1,2,1,2))]. given #592 (A,wt=17): 271 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(71(a,1),34(a,1)),rewrite([4(5),193(5)]),flip(a)]. given #593 (T,wt=9): 15082 x ^ ((y ^ x')' v z)' = 0. [para(14921(a,1),560(a,1,2)),rewrite([4(6)])]. given #594 (T,wt=9): 15083 x ^ (y v (z ^ x')')' = 0. [para(14921(a,1),563(a,1,2)),rewrite([4(6)])]. given #595 (T,wt=9): 15084 x ^ (y ^ (z v x)')' = x. [para(14921(a,1),81(a,1,2)),rewrite([18(2)]),flip(a)]. given #596 (T,wt=9): 15089 x ^ ((y ^ x')' v z) = x. [para(14921(a,1),196(a,1,2)),rewrite([4(5),14921(9)])]. given #597 (A,wt=21): 272 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z))' = x ^ y. [para(25(a,1),34(a,1)),rewrite([4(7),17(7),17(6),5(5),193(6),51(6)])]. given #598 (T,wt=9): 15103 x ^ (y v (z ^ x')') = x. [para(14921(a,1),777(a,1,2)),rewrite([4(5),14921(9)])]. given #599 (T,wt=9): 15365 (x ^ y)' v (x' ^ z)' = 1. [para(7(a,1),12470(a,1,2,1,1,1))]. given #600 (T,wt=9): 15369 (x ^ y)' v (y' ^ z)' = 1. [para(24(a,1),12470(a,1,2,1,1,1))]. given #601 (T,wt=9): 16533 x v (y' ^ (x v y))' = 1. [para(14774(a,1),183(a,1,2))]. given #602 (A,wt=17): 273 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x. [para(102(a,1),34(a,1)),rewrite([4(5),195(5)]),flip(a)]. given #603 (T,wt=9): 16555 x v (y' ^ (y v x))' = 1. [para(14774(a,1),1300(a,1,2))]. given #604 (T,wt=9): 16749 (x ^ y')' v (y ^ z)' = 1. [para(14878(a,1),2(a,1)),flip(a)]. given #605 (T,wt=9): 17049 (x' ^ y)' v (x ^ z)' = 1. [para(4(a,1),15007(a,1,2,1))]. given #606 (T,wt=9): 17417 x v ((x v y) ^ y')' = 1. [para(15077(a,1),176(a,1,2))]. given #607 (A,wt=16): 274 x ^ (y v (x' v z)) != 0 | (y v (x' v z))' = x. [para(111(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #608 (T,wt=9): 17438 x v ((y v x) ^ y')' = 1. [para(15077(a,1),1254(a,1,2))]. given #609 (T,wt=11): 12162 x v ((x' v y)' v z) = x v z. [para(12073(a,1),3(a,1,1)),flip(a)]. given #610 (T,wt=11): 12166 x v (y v (x' v z)') = y v x. [para(12073(a,1),15(a,1,2)),flip(a)]. Low Water (keep, True_semantics): wt=20 given #611 (T,wt=11): 12170 (x' v y)' ^ (z v x) = (x' v y)'. [para(12073(a,1),80(a,1,2,2))]. given #612 (A,wt=17): 281 x ^ (y' v (z ^ (x v (u v y)))) = x ^ (y' v z). [para(275(a,1),12(a,1,2,2,2,2)),rewrite([30(4),2(3),24(3)]),flip(a)]. given #613 (T,wt=11): 12183 (x v (y' v z)') ^ (x v y)' = 0. [para(12073(a,1),145(a,1,2,1,2))]. given #614 (T,wt=11): 12185 x' ^ ((x ^ y) v (x' v z)') = 0. [para(12073(a,1),174(a,1,2,1)),rewrite([4(7)])]. given #615 (T,wt=11): 12190 x v (y v (x v (y' v z)')') = 1. [para(12073(a,1),282(a,1,2,2)),rewrite([2(6)])]. given #616 (T,wt=11): 12192 (x' v y)' ^ (z v (u v x))' = 0. [para(12073(a,1),371(a,1,2,1,2,2))]. given #617 (A,wt=23): 286 x' ^ (y v (z ^ (x ^ (x' v u)))) = x' ^ (y v (z ^ (x ^ (y v u)))). [para(276(a,1),12(a,1,2,2,1)),rewrite([5(5),64(6),5(11)]),flip(a)]. given #618 (T,wt=11): 12193 (x' v y)' ^ ((z v x)' ^ u) = 0. [para(12073(a,1),372(a,1,2,1,1,2))]. Low Water (keep, True_semantics): wt=19 given #619 (T,wt=11): 12194 (x' v y)' ^ (z ^ (u v x)') = 0. [para(12073(a,1),375(a,1,2,2,1,2))]. given #620 (T,wt=11): 12195 x v (y ^ ((x' v z)' ^ u))' = 1. [para(12073(a,1),551(a,1,2)),rewrite([2(7)])]. given #621 (T,wt=11): 12196 x v (y ^ (z ^ (x' v u)'))' = 1. [para(12073(a,1),553(a,1,2)),rewrite([2(7)])]. given #622 (A,wt=23): 287 x ^ ((y v (z ^ (x v u))) ^ (y v ((x ^ z) v (z ^ (y v u))))') = 0. [para(12(a,1),276(a,1,2)),rewrite([4(11),5(11)])]. given #623 (T,wt=11): 12197 (x v y)' ^ (z ^ (y' v u)') = 0. [para(12073(a,1),568(a,1,1,1,2))]. given #624 (T,wt=11): 12198 ((x' v y)' ^ z)' v (u v x) = 1. [para(12073(a,1),573(a,1,2,2))]. given #625 (T,wt=11): 12199 (x ^ (y' v z)')' v (u v y) = 1. [para(12073(a,1),600(a,1,2,2))]. given #626 (T,wt=11): 12200 (x' v y)' ^ (z ^ (x ^ z)') = 0. [para(12073(a,1),774(a,1,2,2,1,1))]. given #627 (A,wt=19): 293 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x)' = y. [para(2(a,1),35(a,1)),rewrite([3(2)])]. given #628 (T,wt=11): 12201 (x ^ y) v ((x' v z)' ^ y)' = 1. [para(12073(a,1),776(a,1,1,1))]. given #629 (T,wt=11): 12203 (x' v y)' ^ (z ^ (z ^ x)') = 0. [para(12073(a,1),781(a,1,2,2,1,2))]. given #630 (T,wt=11): 12204 (x ^ y) v (x ^ (y' v z)')' = 1. [para(12073(a,1),797(a,1,1,2))]. given #631 (T,wt=9): 18950 (x ^ y) v (y' v x') = 1. [para(12261(a,1),12204(a,1,2,1)),rewrite([259(6)])]. given #632 (A,wt=25): 294 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z))' = u. [para(3(a,1),35(a,1,2))]. given #633 (T,wt=9): 18951 (x' ^ y) v (y' v x) = 1. [para(12458(a,1),12204(a,1,2,1)),rewrite([259(6)])]. given #634 (T,wt=9): 18996 x v ((x' ^ y) v y') = 1. [hyper(207,a,18950,a,b,14257,a(flip)),rewrite([14257(5),76(2),14257(6),259(7),3(7),64(8)]),flip(a)]. given #635 (T,wt=9): 18997 x v ((y ^ x') v y') = 1. [hyper(207,a,18950,a,b,14243,a(flip)),rewrite([14243(5),76(2),14243(6),259(7),3(7),64(8)]),flip(a)]. given #636 (T,wt=9): 18998 (x ^ y) v (x' v y') = 1. [hyper(207,a,18950,a,b,13479,a(flip)),rewrite([13479(5),76(2),13479(6),259(7),3(7),64(8)]),flip(a)]. given #637 (A,wt=17): 295 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),35(a,1,2)),rewrite([17(6),81(6)])]. given #638 (T,wt=9): 18999 x' v ((x ^ y) v y') = 1. [hyper(207,a,18950,a,b,12744,a(flip)),rewrite([12744(5),76(2),12744(6),259(7),3(7),64(8)]),flip(a)]. given #639 (T,wt=9): 19000 x' v ((y ^ x) v y') = 1. [hyper(207,a,18950,a,b,12732,a(flip)),rewrite([12732(5),76(2),12732(6),259(7),3(7),64(8)]),flip(a)]. given #640 (T,wt=9): 19033 x' v (y ^ (y ^ x)')' = 1. [hyper(207,a,18950,a,b,153,a(flip)),rewrite([153(4),76(2),153(5),2(8),64(9)]),flip(a)]. given #641 (T,wt=9): 19038 x' v (y ^ (x ^ y)')' = 1. [hyper(207,a,18950,a,b,32,a(flip)),rewrite([32(4),76(2),32(5),2(8),64(9)]),flip(a)]. given #642 (A,wt=25): 296 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z)' = y v u. [para(15(a,1),35(a,1,2))]. given #643 (T,wt=9): 19071 x' v (y' v (y ^ x)) = 1. [para(18950(a,1),389(a,1,2,2,2,1)),rewrite([73(5),2(5),64(5)])]. given #644 (T,wt=9): 19123 x v (y v (y' ^ x')) = 1. [hyper(207,a,18951,a,b,14257,a(flip)),rewrite([14257(7),76(2),14257(8),259(8),2(7),64(8)]),flip(a)]. given #645 (T,wt=9): 19124 x v (y v (x' ^ y')) = 1. [hyper(207,a,18951,a,b,14243,a(flip)),rewrite([14243(7),76(2),14243(8),259(8),2(7),64(8)]),flip(a)]. given #646 (T,wt=9): 19125 x v (y' v (y ^ x')) = 1. [hyper(207,a,18951,a,b,12744,a(flip)),rewrite([12744(7),76(2),12744(8),259(8),2(7),64(8)]),flip(a)]. given #647 (A,wt=19): 297 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(15(a,1),35(a,1))]. given #648 (T,wt=9): 19126 x v (y' v (x' ^ y)) = 1. [hyper(207,a,18951,a,b,12732,a(flip)),rewrite([12732(7),76(2),12732(8),259(8),2(7),64(8)]),flip(a)]. given #649 (T,wt=9): 19157 x v (y ^ (y ^ x')')' = 1. [hyper(207,a,18951,a,b,153,a(flip)),rewrite([153(6),76(2),153(7),2(8),64(9)]),flip(a)]. given #650 (T,wt=9): 19162 x v (y ^ (x' ^ y)')' = 1. [hyper(207,a,18951,a,b,32,a(flip)),rewrite([32(6),76(2),32(7),2(8),64(9)]),flip(a)]. given #651 (T,wt=9): 19176 x' v (y v (y' ^ x)) = 1. [para(18951(a,1),2(a,1)),rewrite([3(6)]),flip(a)]. given #652 (A,wt=16): 301 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z. [para(75(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #653 (T,wt=9): 19177 (x ^ y') v (x' v y) = 1. [para(4(a,1),18951(a,1,1))]. given #654 (T,wt=9): 19273 x' v (y v (x ^ y')) = 1. [para(18997(a,1),390(a,1,2,2,2,1)),rewrite([73(5),2(5),64(5)])]. given #655 (T,wt=9): 19281 x' v (y' v (x ^ y)) = 1. [hyper(207,a,18998,a,b,12732,a(flip)),rewrite([12732(5),76(2),12732(6),259(8),64(8)]),flip(a)]. given #656 (T,wt=11): 12205 x ^ ((y' v z)' ^ (x ^ y)') = 0. [para(12073(a,1),801(a,1,2,2,1,2))]. given #657 (A,wt=16): 302 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'. [para(87(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #658 (T,wt=11): 12206 x' ^ ((y ^ x) v (x' v z)') = 0. [para(12073(a,1),821(a,1,2,1)),rewrite([4(7)])]. given #659 (T,wt=11): 12208 ((x' v y)' v z) ^ (z v x)' = 0. [para(12073(a,1),975(a,1,2,1,2))]. given #660 (T,wt=11): 12210 x' ^ ((x' v y)' v (x ^ z)) = 0. [para(12073(a,1),1191(a,1,2,1)),rewrite([4(7)])]. given #661 (T,wt=11): 12217 x v (y v ((y' v z)' v x)') = 1. [para(12073(a,1),1670(a,1,2,2)),rewrite([2(6)])]. given #662 (A,wt=20): 304 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'. [para(29(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #663 (T,wt=11): 12218 x ^ ((y' v z)' ^ (y ^ x)') = 0. [para(12073(a,1),2021(a,1,2,2,1,1))]. given #664 (T,wt=11): 12220 (x ^ y) v ((y' v z)' ^ x)' = 1. [para(12073(a,1),2970(a,1,1,2))]. given #665 (T,wt=11): 12221 (x ^ y) v (y ^ (x' v z)')' = 1. [para(12073(a,1),2971(a,1,1,1))]. given #666 (T,wt=11): 12223 x' ^ ((x' v y)' v (z ^ x)) = 0. [para(12073(a,1),3146(a,1,2,1)),rewrite([4(7)])]. given #667 (A,wt=16): 305 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(166(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #668 (T,wt=11): 12229 x v ((y ^ (x ^ z))' v u)' = x. [para(12073(a,1),170(a,1,2)),rewrite([71(3)]),flip(a)]. given #669 (T,wt=11): 12233 (x' v y)' v (z v x) = z v x. [para(12073(a,1),210(a,1,2,2)),rewrite([12073(9)])]. given #670 (T,wt=11): 12239 x v ((y ^ (z ^ x))' v u)' = x. [para(12073(a,1),239(a,1,2)),rewrite([102(3)]),flip(a)]. given #671 (T,wt=11): 12256 x v ((y v x')' v z) = x v z. [para(12161(a,1),3(a,1,1)),flip(a)]. given #672 (A,wt=16): 306 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(177(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #673 (T,wt=11): 12260 x v (y v (z v x')') = y v x. [para(12161(a,1),15(a,1,2)),flip(a)]. given #674 (T,wt=11): 12263 (x v y')' ^ (z v y) = (x v y')'. [para(12161(a,1),80(a,1,2,2))]. given #675 (T,wt=11): 12276 (x v (y v z')') ^ (x v z)' = 0. [para(12161(a,1),145(a,1,2,1,2))]. given #676 (T,wt=11): 12279 x' ^ ((x ^ y) v (z v x')') = 0. [para(12161(a,1),174(a,1,2,1)),rewrite([4(7)])]. given #677 (A,wt=21): 307 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(23(a,1),35(a,1)),rewrite([51(7)])]. given #678 (T,wt=11): 12284 x v (y v (x v (z v y')')') = 1. [para(12161(a,1),282(a,1,2,2)),rewrite([2(6)])]. given #679 (T,wt=11): 12286 (x v y')' ^ (z v (u v y))' = 0. [para(12161(a,1),371(a,1,2,1,2,2))]. given #680 (T,wt=11): 12287 (x v y')' ^ ((z v y)' ^ u) = 0. [para(12161(a,1),372(a,1,2,1,1,2))]. given #681 (T,wt=11): 12288 (x v y')' ^ (z ^ (u v y)') = 0. [para(12161(a,1),375(a,1,2,2,1,2))]. given #682 (A,wt=23): 308 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z. [para(56(a,1),35(a,1,2))]. given #683 (T,wt=11): 12289 x v (y ^ ((z v x')' ^ u))' = 1. [para(12161(a,1),551(a,1,2)),rewrite([2(7)])]. given #684 (T,wt=11): 12290 x v (y ^ (z ^ (u v x')'))' = 1. [para(12161(a,1),553(a,1,2)),rewrite([2(7)])]. given #685 (T,wt=11): 12291 (x v y)' ^ (z ^ (u v y')') = 0. [para(12161(a,1),568(a,1,1,1,2))]. given #686 (T,wt=11): 12292 ((x v y')' ^ z)' v (u v y) = 1. [para(12161(a,1),573(a,1,2,2))]. given #687 (A,wt=23): 309 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z. [para(58(a,1),35(a,1,2))]. given #688 (T,wt=11): 12293 (x ^ (y v z')')' v (u v z) = 1. [para(12161(a,1),600(a,1,2,2))]. given #689 (T,wt=11): 12294 (x v y')' ^ (z ^ (y ^ z)') = 0. [para(12161(a,1),774(a,1,2,2,1,1))]. Low Water (keep, True_semantics): wt=17 given #690 (T,wt=11): 12295 (x ^ y) v ((z v x')' ^ y)' = 1. [para(12161(a,1),776(a,1,1,1))]. given #691 (T,wt=11): 12297 (x v y')' ^ (z ^ (z ^ y)') = 0. [para(12161(a,1),781(a,1,2,2,1,2))]. given #692 (A,wt=20): 313 (x v y) ^ (z v (y' v u)) != 0 | (x v y)' = z v (y' v u). [para(111(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #693 (T,wt=11): 12298 (x ^ y) v (x ^ (z v y')')' = 1. [para(12161(a,1),797(a,1,1,2))]. given #694 (T,wt=11): 12299 x ^ ((y v z')' ^ (x ^ z)') = 0. [para(12161(a,1),801(a,1,2,2,1,2))]. given #695 (T,wt=11): 12300 x' ^ ((y ^ x) v (z v x')') = 0. [para(12161(a,1),821(a,1,2,1)),rewrite([4(7)])]. given #696 (T,wt=11): 12302 ((x v y')' v z) ^ (z v y)' = 0. [para(12161(a,1),975(a,1,2,1,2))]. given #697 (A,wt=16): 314 (x v y) ^ (x' v z) != 0 | (x v y)' = x' v z. [para(111(a,1),35(a,1)),xx(a)]. given #698 (T,wt=11): 12304 x' ^ ((y v x')' v (x ^ z)) = 0. [para(12161(a,1),1191(a,1,2,1)),rewrite([4(7)])]. given #699 (T,wt=11): 12312 x v (y v ((z v y')' v x)') = 1. [para(12161(a,1),1670(a,1,2,2)),rewrite([2(6)])]. given #700 (T,wt=11): 12313 x ^ ((y v z')' ^ (z ^ x)') = 0. [para(12161(a,1),2021(a,1,2,2,1,1))]. given #701 (T,wt=11): 12315 (x ^ y) v ((z v y')' ^ x)' = 1. [para(12161(a,1),2970(a,1,1,2))]. given #702 (A,wt=16): 315 (x v y') ^ (z v y) != 0 | (x v y')' = z v y. [para(275(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #703 (T,wt=11): 12316 (x ^ y) v (y ^ (z v x')')' = 1. [para(12161(a,1),2971(a,1,1,1))]. given #704 (T,wt=11): 12318 x' ^ ((y v x')' v (z ^ x)) = 0. [para(12161(a,1),3146(a,1,2,1)),rewrite([4(7)])]. given #705 (T,wt=11): 12324 x v (y v (z ^ (x ^ u))')' = x. [para(12161(a,1),170(a,1,2)),rewrite([71(3)]),flip(a)]. given #706 (T,wt=11): 12328 (x v y')' v (z v y) = z v y. [para(12161(a,1),210(a,1,2,2)),rewrite([12161(9)])]. given #707 (A,wt=16): 318 x ^ (y v (z v x')) != 0 | y v (z v x') = x'. [para(122(a,1),10(a,1)),flip(c),xx(a)]. given #708 (T,wt=11): 12333 x v (y v (z ^ (u ^ x))')' = x. [para(12161(a,1),239(a,1,2)),rewrite([102(3)]),flip(a)]. given #709 (T,wt=11): 12353 x' v ((x v y)' v z) = x' v z. [para(12172(a,1),3(a,1,1)),flip(a)]. given #710 (T,wt=11): 12357 x' v (y v (x v z)') = y v x'. [para(12172(a,1),15(a,1,2)),flip(a)]. given #711 (T,wt=11): 12360 (x v y)' ^ (z v x') = (x v y)'. [para(12172(a,1),80(a,1,2,2))]. given #712 (A,wt=19): 319 x ^ (y v (z ^ (x v (u v (v v y'))))) = x ^ (y v z). [para(122(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. given #713 (T,wt=11): 12371 (x v (y v z)') ^ (x v y')' = 0. [para(12172(a,1),145(a,1,2,1,2))]. given #714 (T,wt=11): 12374 x ^ ((x' ^ y) v (x v z)') = 0. [para(12172(a,1),174(a,1,2,1)),rewrite([259(7),4(6)])]. given #715 (T,wt=11): 12376 (x ^ y)' v (z v x)' = (x ^ y)'. [para(214(a,1),12172(a,1,2,1))]. given #716 (T,wt=11): 12380 x v (y' v (x v (y v z)')') = 1. [para(12172(a,1),282(a,1,2,2)),rewrite([2(6)])]. given #717 (A,wt=16): 321 x ^ (y v (z v x')) != 0 | (y v (z v x'))' = x. [para(122(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #718 (T,wt=10): 21740 x v y != 0 | y v x = 0. [para(92(a,1),321(a,1)),rewrite([147(7),73(5)]),flip(b)]. given #719 (T,wt=10): 21744 x ^ y != 0 | y ^ x = 0. [para(228(a,1),21740(a,1)),rewrite([228(6)])]. given #720 (T,wt=11): 12382 (x v y)' ^ (z v (u v x'))' = 0. [para(12172(a,1),371(a,1,2,1,2,2))]. given #721 (T,wt=11): 12383 (x v y)' ^ ((z v x')' ^ u) = 0. [para(12172(a,1),372(a,1,2,1,1,2))]. given #722 (A,wt=20): 322 (x v y) ^ (z v (u v y')) != 0 | (x v y)' = z v (u v y'). [para(122(a,1),35(a,1,2)),rewrite([86(2)]),xx(a)]. given #723 (T,wt=11): 12384 (x v y)' ^ (z ^ (u v x')') = 0. [para(12172(a,1),375(a,1,2,2,1,2))]. given #724 (T,wt=11): 12385 x' v (y ^ ((x v z)' ^ u))' = 1. [para(12172(a,1),551(a,1,2)),rewrite([2(7)])]. given #725 (T,wt=11): 12386 x' v (y ^ (z ^ (x v u)'))' = 1. [para(12172(a,1),553(a,1,2)),rewrite([2(7)])]. given #726 (T,wt=11): 12387 (x v y')' ^ (z ^ (y v u)') = 0. [para(12172(a,1),568(a,1,1,1,2))]. given #727 (A,wt=16): 323 (x v y) ^ (z v x') != 0 | (x v y)' = z v x'. [para(122(a,1),35(a,1)),xx(a)]. given #728 (T,wt=11): 12388 ((x v y)' ^ z)' v (u v x') = 1. [para(12172(a,1),573(a,1,2,2))]. given #729 (T,wt=11): 12389 (x ^ (y v z)')' v (u v y') = 1. [para(12172(a,1),600(a,1,2,2))]. given #730 (T,wt=11): 12390 (x v y)' ^ (z ^ (x' ^ z)') = 0. [para(12172(a,1),774(a,1,2,2,1,1))]. given #731 (T,wt=11): 12391 (x' ^ y) v ((x v z)' ^ y)' = 1. [para(12172(a,1),776(a,1,1,1))]. given #732 (A,wt=23): 333 x ^ (y v ((z ^ (u v y)) v (x ^ z))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),37(a,1,2,2))]. given #733 (T,wt=11): 12393 (x v y)' ^ (z ^ (z ^ x')') = 0. [para(12172(a,1),781(a,1,2,2,1,2))]. given #734 (T,wt=11): 12394 (x ^ y') v (x ^ (y v z)')' = 1. [para(12172(a,1),797(a,1,1,2))]. given #735 (T,wt=11): 12395 x ^ ((y v z)' ^ (x ^ y')') = 0. [para(12172(a,1),801(a,1,2,2,1,2))]. given #736 (T,wt=11): 12396 x ^ ((y ^ x') v (x v z)') = 0. [para(12172(a,1),821(a,1,2,1)),rewrite([259(7),4(6)])]. given #737 (A,wt=23): 334 x ^ (y v ((z ^ x) v (z ^ (u v y)))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),37(a,1,2,2,1))]. given #738 (T,wt=11): 12398 (x ^ y)' v (z v y)' = (x ^ y)'. [para(824(a,1),12172(a,1,2,1))]. given #739 (T,wt=11): 12399 ((x v y)' v z) ^ (z v x')' = 0. [para(12172(a,1),975(a,1,2,1,2))]. given #740 (T,wt=11): 12402 x ^ ((x v y)' v (x' ^ z)) = 0. [para(12172(a,1),1191(a,1,2,1)),rewrite([259(7),4(6)])]. given #741 (T,wt=11): 12410 x v (y' v ((y v z)' v x)') = 1. [para(12172(a,1),1670(a,1,2,2)),rewrite([2(6)])]. given #742 (A,wt=23): 335 x ^ (y v ((x ^ z) v ((u v y) ^ z))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),37(a,1,2,2,2))]. given #743 (T,wt=11): 12411 x ^ ((y v z)' ^ (y' ^ x)') = 0. [para(12172(a,1),2021(a,1,2,2,1,1))]. Low Water (displace, True_semantics): id=13293, wt=24 given #744 (T,wt=11): 12413 (x ^ y') v ((y v z)' ^ x)' = 1. [para(12172(a,1),2970(a,1,1,2))]. given #745 (T,wt=11): 12414 (x' ^ y) v (y ^ (x v z)')' = 1. [para(12172(a,1),2971(a,1,1,1))]. Low Water (displace, True_semantics): id=13993, wt=23 given #746 (T,wt=11): 12416 x ^ ((x v y)' v (z ^ x')) = 0. [para(12172(a,1),3146(a,1,2,1)),rewrite([259(7),4(6)])]. given #747 (A,wt=25): 336 x ^ ((y ^ z) v ((x ^ u) v (u ^ y))) = x ^ ((y ^ z) v (u ^ (x v y))). [para(7(a,1),37(a,1,2,2,2,2))]. given #748 (T,wt=11): 12424 (x v y)' v (z v x') = z v x'. [para(12172(a,1),210(a,1,2,2)),rewrite([12172(9)])]. given #749 (T,wt=11): 12428 (x ^ y)' v (y ^ x)' = (x ^ y)'. [para(220(a,1),12172(a,1,2,1))]. given #750 (T,wt=10): 22289 (x ^ y)' != 0 | (y ^ x)' = 0. [para(12428(a,1),21740(a,1)),rewrite([12428(9)])]. given #751 (T,wt=10): 22293 (x v y)' != 0 | (y v x)' = 0. [para(213(a,1),22289(a,1,1)),rewrite([213(7)])]. given #752 (A,wt=15): 337 x ^ (y' v (z ^ (x v y))) = x ^ (y' v z). [para(8(a,1),37(a,1,2,2,2,2)),rewrite([30(4),2(3),24(3)]),flip(a)]. given #753 (T,wt=11): 12450 (x v y) ^ (x v (y ^ x'))' = 0. [back_rewrite(11961),rewrite([12392(8)])]. given #754 (T,wt=9): 22393 (x v (y ^ x'))' = (x v y)'. [hyper(297,a,395,a,b,12450,a),flip(a)]. given #755 (T,wt=9): 22408 (x ^ y') v (y v x)' = y'. [back_rewrite(21956),rewrite([22393(6)])]. given #756 (T,wt=7): 22566 (x ^ y)' = x' v y'. [para(14769(a,1),22408(a,1,1)),rewrite([22442(5),22489(5)]),flip(a)]. given #757 (A,wt=19): 338 x ^ (y v (x' ^ (z v y))) = x ^ (y v (x' ^ (x v z))). [para(9(a,1),37(a,1,2,2,1)),rewrite([64(5)])]. given #758 (T,wt=7): 27099 (x' v y)' = x ^ y'. [back_rewrite(19580),rewrite([22636(5)]),xx(a)]. given #759 (T,wt=7): 27749 (x v y)' = x' ^ y'. [para(259(a,1),27099(a,1,1,1))]. given #760 (T,wt=9): 22418 x v (y ^ x') = x v y. [para(22393(a,1),259(a,1,1)),rewrite([259(3)]),flip(a)]. given #761 (T,wt=9): 22575 x ^ ((x ^ y) v y') = x. [para(18999(a,1),22408(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. given #762 (A,wt=23): 339 x ^ ((x ^ y) v (z v (y ^ (u v z)))) = x ^ (z v (y ^ (x v u))). [para(15(a,1),37(a,1,2))]. given #763 (T,wt=9): 22576 x ^ ((y ^ x) v y') = x. [para(19000(a,1),22408(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. given #764 (T,wt=9): 22577 x ^ (y' v (y ^ x)) = x. [para(19071(a,1),22408(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. given #765 (T,wt=9): 23745 x' ^ (y ^ (y' v x)) = 0. [back_rewrite(16554),rewrite([22566(4),259(3),3(5),46(5)])]. given #766 (T,wt=9): 27274 (x ^ y) v (x ^ y') = x. [back_rewrite(22471),rewrite([27099(4)])]. given #767 (A,wt=17): 340 x ^ (y v ((z v y) ^ (x v z))) = x ^ (z v y). [para(26(a,1),37(a,1,2,2,2)),rewrite([2(4),24(4),58(2)]),flip(a)]. given #768 (T,wt=9): 27281 (x ^ y) v (y ^ x') = y. [back_rewrite(22463),rewrite([27099(4)])]. given #769 (T,wt=9): 27741 x ^ ((x' v y) ^ y') = 0. [para(27099(a,1),9(a,1,2)),rewrite([17(5)])]. given #770 (T,wt=9): 27759 x ^ ((y v x') ^ y') = 0. [para(27099(a,1),979(a,1,2)),rewrite([17(5)])]. given #771 (T,wt=9): 30256 x' ^ (x v y') = x' ^ y'. [back_rewrite(22413),rewrite([27749(4),22566(4),259(3),27749(6)])]. given #772 (A,wt=21): 341 (x v y) ^ (z v ((x v (y v u)) ^ (x v (y v v)))) = x v y. [para(19(a,1),37(a,1,2,2,1)),rewrite([3(7),159(9),3(6)]),flip(a)]. given #773 (T,wt=9): 33257 (x v y) ^ (y' ^ x') = 0. [back_rewrite(979),rewrite([27749(3)])]. given #774 (T,wt=9): 33421 (x v y) ^ (x' ^ y') = 0. [para(27749(a,1),9(a,1,2))]. given #775 (T,wt=9): 33497 x v (x' ^ y) = x v y. [para(4(a,1),22418(a,1,2))]. given #776 (T,wt=9): 33502 x' v (y ^ x) = x' v y. [para(259(a,1),22418(a,1,2,2))]. given #777 (A,wt=21): 342 x ^ (y v (z v ((u v y) ^ (x v u)))) = x ^ (z v (u v y)). [para(19(a,1),37(a,1,2,2,2)),rewrite([2(5),24(5),3(3),210(3),3(8)]),flip(a)]. given #778 (T,wt=9): 33551 x' ^ (y' v x) = x' ^ y'. [para(22418(a,1),27749(a,1,1)),rewrite([27749(2),22566(7),259(7)]),flip(a)]. given #779 (T,wt=9): 33614 (x ^ y) v y' = x v y'. [para(22575(a,1),24(a,1,2)),rewrite([2(4),22(4)]),flip(a)]. given #780 (T,wt=9): 33763 (x ^ y) v x' = y v x'. [para(22576(a,1),24(a,1,2)),rewrite([2(4),100(4)]),flip(a)]. given #781 (T,wt=9): 33787 x' v (x ^ y) = x' v y. [para(22577(a,1),24(a,1,2)),rewrite([2(4),105(4)]),flip(a)]. given #782 (A,wt=19): 344 x ^ (y' v (z v (u ^ (x v y)))) = x ^ (y' v (z v u)). [para(75(a,1),37(a,1,2,2,2,2)),rewrite([30(5),2(4),24(4),3(3),3(9)]),flip(a)]. given #783 (T,wt=9): 33837 (x v y) ^ (y v x') = y. [hyper(34,a,2979,a,b,23745,a),rewrite([259(2),27749(3),2(5),22418(5)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 21.97 (+ 0.14) seconds: distributivity. % Length of proof is 160. % Level of proof is 29. % Maximum clause weight is 23. % Given clauses 783. 1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity) # label(non_clause) # 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 ^ 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 v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. 11 x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # answer(distributivity). [deny(1)]. 15 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])]. 17 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. 18 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. 20 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 21 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. 22 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. 23 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 26 x ^ x = x. [para(7(a,1),6(a,1,2))]. 27 x v x = x. [para(6(a,1),7(a,1,2))]. 28 x v (x' v y) = 1 v y. [para(8(a,1),3(a,1,1)),flip(a)]. 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. 30 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. 31 x ^ (x' ^ y) = 0 ^ y. [para(9(a,1),5(a,1,1)),flip(a)]. 33 x v 0 = x. [para(9(a,1),7(a,1,2))]. 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. 35 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. 40 x ^ (y v ((x ^ z) v ((y v u) ^ z))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,2))]. 43 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. 46 x v (y v (x ^ z)) = y v x. [para(7(a,1),15(a,1,2)),flip(a)]. 47 x v (y v x') = y v 1. [para(8(a,1),15(a,1,2)),flip(a)]. 51 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. 53 x ^ (y ^ x) = y ^ x. [para(26(a,1),5(a,2,2)),rewrite([4(2)])]. 56 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. 60 x ^ (y v ((x ^ z) v (z ^ y))) = x ^ (y v (z ^ (x v y))). [para(27(a,1),12(a,1,2,2,2,2))]. 63 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. 64 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. 66 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(33(a,1),12(a,1,2,2,2,2)),rewrite([60(5),33(6)])]. 70 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. 72 x ^ (y ^ x') = y ^ 0. [para(9(a,1),17(a,1,2)),flip(a)]. 73 1' = 0. [hyper(10,a,33,a,b,63,a)]. 74 1 v x = 1. [para(63(a,1),6(a,1))]. 75 x v (x' v y) = 1. [back_rewrite(28),rewrite([74(5)])]. 76 0' = 1. [hyper(10,a,64,a,b,30,a)]. 77 0 ^ x = 0. [para(64(a,1),6(a,1,2))]. 78 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [para(64(a,1),12(a,1,2,2,2,2)),rewrite([64(5),64(8),70(7)])]. 79 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite([77(5)])]. 81 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. 85 x ^ (y ^ (z v x)) = y ^ x. [para(18(a,1),17(a,1,2)),flip(a)]. 86 x v 1 = 1. [para(18(a,1),63(a,1)),flip(a)]. 87 x v (y v x') = 1. [back_rewrite(47),rewrite([86(5)])]. 88 x ^ 0 = 0. [para(77(a,1),4(a,1)),flip(a)]. 89 x ^ (y ^ x') = 0. [back_rewrite(72),rewrite([88(5)])]. 100 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. 110 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z). [para(75(a,1),12(a,1,2,2,2,2)),rewrite([30(3),2(2),24(2)]),flip(a)]. 113 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. 120 x ^ ((x v y)' ^ z) = 0. [para(79(a,1),20(a,1,2)),rewrite([88(2)]),flip(a)]. 129 x ^ (y v x)' = 0. [para(2(a,1),113(a,1,2,1))]. 131 x ^ (y ^ ((x ^ y) v z)') = 0. [para(113(a,1),5(a,1)),flip(a)]. 132 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))). [para(113(a,1),12(a,1,2,2,1)),rewrite([64(6)])]. 134 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. 143 x ^ (y ^ (z v (x ^ y))') = 0. [para(129(a,1),5(a,1)),flip(a)]. 147 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. 149 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(29(a,1),10(a,1)),flip(c),xx(a)]. 166 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. 171 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite([4(4)])]. 174 ((x ^ y) v z) ^ (x v z)' = 0. [para(22(a,1),129(a,1,2,1))]. 177 x v (y ^ x)' = 1. [para(4(a,1),166(a,1,2,1))]. 195 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),53(a,1,2)),rewrite([5(5)])]. 204 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(23(a,1),18(a,1,2)),rewrite([4(5)])]. 207 x v y != 1 | 0 != x | x' = x v y. [para(56(a,1),10(a,1)),rewrite([6(5)]),flip(b)]. 259 x'' = x. [para(8(a,1),34(a,1)),rewrite([4(5),9(5)]),xx(a),xx(b)]. 264 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x. [para(29(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. 275 x' v (y v x) = 1. [para(259(a,1),87(a,1,2,2))]. 276 x' ^ (y ^ x) = 0. [para(259(a,1),89(a,1,2,2))]. 280 x' ^ (y v x) != 0 | y v x = x. [para(275(a,1),10(a,1)),rewrite([259(10)]),flip(c),xx(a)]. 297 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(15(a,1),35(a,1))]. 395 x v (y v (y v (x ^ z))') = 1. [para(147(a,1),22(a,1,2)),rewrite([86(2)]),flip(a)]. 522 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(64(a,1),40(a,1,2,2,2,1)),rewrite([64(5),64(8),70(7)])]. 589 x' ^ (x v (y ^ x')) = x' ^ (x v y). [para(27(a,1),43(a,1,2,2,2))]. 776 ((x v y) ^ z) v (y ^ z)' = 1. [para(81(a,1),177(a,1,2,1))]. 777 (x v y) ^ (z ^ y) = z ^ y. [para(53(a,1),81(a,2)),rewrite([195(4)])]. 797 (x ^ (y v z)) v (x ^ z)' = 1. [para(85(a,1),177(a,1,2,1))]. 821 ((x ^ y) v z) ^ (y v z)' = 0. [para(100(a,1),129(a,1,2,1))]. 986 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),131(a,1,2,2,1,1))]. 1002 x ^ (x' v (y v (z ^ x))) = x ^ (x' v (y v z)). [para(75(a,1),66(a,1,2,2,2)),rewrite([30(4),3(3),3(8)]),flip(a)]. 1041 x ^ (y ^ (z v (y ^ x))') = 0. [para(4(a,1),143(a,1,2,2,1,2))]. 1191 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),174(a,1,1))]. 2979 ((x v y) ^ (z v y)) v y' = 1. [para(18(a,1),776(a,1,2,1))]. 3154 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(24(a,1),821(a,1,2,1))]. 3205 x' ^ (x v (y ^ (x' v z))) = x' ^ (x v y). [para(56(a,1),110(a,1,2,2,2))]. 4971 (x ^ y) v (y ^ ((y ^ x) v z)) = y ^ ((y ^ x) v z). [para(134(a,1),24(a,1,2)),rewrite([2(5)])]. 7145 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),280(a,1,2))]. 8048 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(7(a,1),171(a,1,1))]. 10006 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(24(a,1),204(a,1,1)),rewrite([24(3),24(7)])]. 11961 x' ^ ((x v y) ^ (x v (y ^ x'))') = 0. [para(589(a,1),276(a,1,2)),rewrite([4(8),5(8)])]. 12014 x' ^ (x v (x' v y)') = 0. [para(132(a,1),589(a,2)),rewrite([4(8),120(8),33(3),4(2),9(2),3205(10)]),flip(a)]. 12073 x v (x' v y)' = x. [hyper(7145,a,12014,a),rewrite([2(4)])]. 12161 x v (y v x')' = x. [para(2(a,1),12073(a,1,2,1))]. 12168 x ^ (x' v y)' = (x' v y)'. [para(12073(a,1),18(a,1,2)),rewrite([4(4)])]. 12172 x' v (x v y)' = x'. [para(259(a,1),12073(a,1,2,1,1))]. 12204 (x ^ y) v (x ^ (y' v z)')' = 1. [para(12073(a,1),797(a,1,1,2))]. 12206 x' ^ ((y ^ x) v (x' v z)') = 0. [para(12073(a,1),821(a,1,2,1)),rewrite([4(7)])]. 12261 x ^ (y v x')' = (y v x')'. [para(12161(a,1),18(a,1,2)),rewrite([4(4)])]. 12265 x' v (y v x)' = x'. [para(259(a,1),12161(a,1,2,1,2))]. 12392 x' ^ (y ^ (x v z)') = y ^ (x v z)'. [para(12172(a,1),777(a,1,1))]. 12396 x ^ ((y ^ x') v (x v z)') = 0. [para(12172(a,1),821(a,1,2,1)),rewrite([259(7),4(6)])]. 12450 (x v y) ^ (x v (y ^ x'))' = 0. [back_rewrite(11961),rewrite([12392(8)])]. 12453 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),12265(a,1,2,1)),rewrite([2(4)])]. 12458 x' ^ (y v x)' = (y v x)'. [para(12265(a,1),18(a,1,2)),rewrite([4(4)])]. 12744 x ^ (y' v (y ^ x))' = 0. [para(12168(a,1),1041(a,1,2))]. 13479 x ^ ((y ^ x) v y')' = 0. [para(12261(a,1),986(a,1,2))]. 14769 x' ^ (x ^ y)' = x'. [para(12453(a,1),6(a,1,2))]. 14774 x v (x' ^ y)' = (x' ^ y)'. [para(259(a,1),12453(a,1,1))]. 14873 x' ^ (y ^ x)' = x'. [para(4(a,1),14769(a,1,2,1))]. 14921 x ^ (y ^ x')' = x. [para(259(a,1),14873(a,1,1)),rewrite([259(6)])]. 15077 x v (y ^ x')' = (y ^ x')'. [para(14921(a,1),24(a,1,2)),rewrite([2(4)])]. 16554 x' ^ (y ^ ((x' ^ y)' v (x ^ z))) = 0. [para(14774(a,1),1191(a,1,2,1)),rewrite([259(9),4(8),5(8)])]. 17437 x ^ (y' ^ ((x ^ y')' v (y ^ z))) = 0. [para(15077(a,1),1191(a,1,2,1)),rewrite([259(9),4(8),5(8)])]. 18950 (x ^ y) v (y' v x') = 1. [para(12261(a,1),12204(a,1,2,1)),rewrite([259(6)])]. 18951 (x' ^ y) v (y' v x) = 1. [para(12458(a,1),12204(a,1,2,1)),rewrite([259(6)])]. 18999 x' v ((x ^ y) v y') = 1. [hyper(207,a,18950,a,b,12744,a(flip)),rewrite([12744(5),76(2),12744(6),259(7),3(7),64(8)]),flip(a)]. 19177 (x ^ y') v (x' v y) = 1. [para(4(a,1),18951(a,1,1))]. 19580 x ^ (y' ^ (x' v y)) != 0 | (x' v y)' = x ^ y'. [para(19177(a,1),264(a,1,2,2,1)),rewrite([73(6),2(6),64(6),5(5),19177(14),73(11),2(11),64(11)])]. 19627 (x ^ y) v (y' v (x ^ y))' = y. [hyper(149,a,12206,a),rewrite([259(8)])]. 21956 (x ^ y') v (y v (x ^ y'))' = y'. [hyper(149,a,12396,a)]. 22393 (x v (y ^ x'))' = (x v y)'. [hyper(297,a,395,a,b,12450,a),flip(a)]. 22408 (x ^ y') v (y v x)' = y'. [back_rewrite(21956),rewrite([22393(6)])]. 22418 x v (y ^ x') = x v y. [para(22393(a,1),259(a,1,1)),rewrite([259(3)]),flip(a)]. 22419 (x' v (y ^ x))' = (x' v y)'. [para(259(a,1),22393(a,1,1,2,2))]. 22442 ((x ^ y) v x')' = (y v x')'. [para(13479(a,1),22393(a,1,1,2)),rewrite([2(5),64(5),2(8),100(8)])]. 22463 (x ^ y) v (y' v x)' = y. [back_rewrite(19627),rewrite([22419(5)])]. 22489 x v (y v x)' = x v y'. [para(22408(a,1),22(a,1,2)),flip(a)]. 22566 (x ^ y)' = x' v y'. [para(14769(a,1),22408(a,1,1)),rewrite([22442(5),22489(5)]),flip(a)]. 22575 x ^ ((x ^ y) v y') = x. [para(18999(a,1),22408(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. 22636 x ^ (y' ^ (x' v y)) = 0. [back_rewrite(17437),rewrite([22566(4),259(4),3(5),7(4)])]. 23745 x' ^ (y ^ (y' v x)) = 0. [back_rewrite(16554),rewrite([22566(4),259(3),3(5),46(5)])]. 27099 (x' v y)' = x ^ y'. [back_rewrite(19580),rewrite([22636(5)]),xx(a)]. 27281 (x ^ y) v (y ^ x') = y. [back_rewrite(22463),rewrite([27099(4)])]. 27749 (x v y)' = x' ^ y'. [para(259(a,1),27099(a,1,1,1))]. 33655 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(3154(a,1),22575(a,1,2,1)),rewrite([259(6),64(5),4(4)])]. 33837 (x v y) ^ (y v x') = y. [hyper(34,a,2979,a,b,23745,a),rewrite([259(2),27749(3),2(5),22418(5)]),flip(a)]. 34034 (x ^ y) v (x ^ ((y v z) ^ y')) = x ^ (y v z). [para(70(a,1),27281(a,1,1)),rewrite([5(5)])]. 34041 (x ^ y) v (((y ^ x) v (x ^ z)) ^ y') = (y ^ x) v (x ^ z). [para(78(a,1),27281(a,1,1))]. 34068 (x ^ y) v (((y ^ x) v (z ^ x)) ^ y') = (y ^ x) v (z ^ x). [para(522(a,1),27281(a,1,1))]. 34078 x ^ (x' v y) = x ^ y. [para(23745(a,1),27281(a,1,1)),rewrite([259(6),4(5),85(5),64(3)]),flip(a)]. 34138 x ^ (y v (z ^ x)) = x ^ (y v z). [back_rewrite(1002),rewrite([34078(5),34078(7)])]. 34321 (x ^ y) v (z ^ y) = y ^ ((x ^ y) v z). [back_rewrite(33655),rewrite([34138(4)]),flip(a)]. 34549 (x ^ y) v (x ^ (((y ^ x) v z) ^ y')) = x ^ ((y ^ x) v z). [back_rewrite(34068),rewrite([34321(4),5(6),34321(10)])]. 35979 (x v y) ^ x' = y ^ x'. [para(22418(a,1),33837(a,1,1)),rewrite([2(5),24(5)])]. 35996 (x ^ y) v (x ^ (z ^ y')) = x ^ (y v z). [back_rewrite(34034),rewrite([35979(4)])]. 36110 x ^ ((y ^ x) v z) = x ^ (y v z). [back_rewrite(34549),rewrite([35996(7),22(3)]),flip(a)]. 36217 (x ^ y) v (y ^ z) = y ^ (x v (y ^ z)). [back_rewrite(10006),rewrite([36110(4)]),flip(a)]. 36259 x ^ (y v (x ^ z)) = x ^ (y v z). [back_rewrite(34041),rewrite([36217(4),5(6),35979(5),5(4),51(5),35996(5),36217(5)]),flip(a)]. 36272 x ^ ((x ^ y) v z) = x ^ (y v z). [back_rewrite(4971),rewrite([36217(5),36259(5),100(3)]),flip(a)]. 36306 (x ^ y) v (x ^ z) = x ^ (y v z). [back_rewrite(8048),rewrite([36259(4),36272(3)]),flip(a)]. 36307 $F # answer(distributivity). [resolve(36306,a,13,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=783. Generated=768037. Kept=36304. proofs=1. Usable=160. Sos=6831. Demods=5920. Limbo=47, Disabled=29276. Hints=0. Weight_deleted=26737. Literals_deleted=0. Forward_subsumed=689118. Back_subsumed=115. Sos_limit_deleted=15878. Sos_displaced=198. Sos_removed=0. New_demodulators=32534 (6 lex), Back_demodulated=28950. Back_unit_deleted=0. Demod_attempts=15197424. Demod_rewrites=3717367. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=375292. Nonunit_bsub_feature_tests=38561. Megabytes=27.21. User_CPU=21.97, System_CPU=0.14, Wall_clock=22. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 27627 exit (max_proofs) Tue May 22 14:50:02 2007