============================== Prover9 =============================== Prover9 (32) version 2008-04A, April 2008. Process 24350 was started by mccune on cleo, Fri Apr 4 11:36:56 2008 The command was "/home/mccune/LADR/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(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 w))) = 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 w)))) = x ^ (y v (z ^ (x v w))). [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) ^ w))))) = 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))]. 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))]. Low Water (keep): wt=25, iters=6675 ============================== SELECTOR REPORT ======================= Sos_deleted=0, Sos_displaced=0, Sos_size=10679 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 10679 94 F 4 low weight 0 0 T 4 low weight 10679 376 ============================== end of selector report ================ 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): 12143 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): 12202 x v (x' v y)' = x. [hyper(7145,a,12143,a),rewrite([2(4)])]. given #494 (T,wt=7): 12290 x v (y v x')' = x. [para(2(a,1),12202(a,1,2,1))]. given #495 (T,wt=7): 12301 x' v (x v y)' = x'. [para(259(a,1),12202(a,1,2,1,1))]. given #496 (T,wt=7): 12394 x' v (y v x)' = x'. [para(259(a,1),12290(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): 12296 x v (y v (x' v z))' = x. [para(15(a,1),12202(a,1,2,1))]. given #499 (T,wt=9): 12297 x ^ (x' v y)' = (x' v y)'. [para(12202(a,1),18(a,1,2)),rewrite([4(4)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 112 (0.00 of 6.86 sec). given #500 (T,wt=9): 12298 x v ((x ^ y)' v z)' = x. [para(12202(a,1),22(a,1,2)),rewrite([7(2)]),flip(a)]. given #501 (T,wt=9): 12303 (x' v y)' ^ (z v x)' = 0. [para(12202(a,1),141(a,1,2,1,2))]. given #502 (A,wt=15): 232 x ^ (y v ((z v (u v x)) ^ (x v w))) = x. [para(80(a,1),12(a,1,2,2,1)),rewrite([45(7)]),flip(a)]. given #503 (T,wt=9): 12305 x v ((x' v y)' ^ z)' = 1. [para(12202(a,1),544(a,1,2)),rewrite([2(6)])]. given #504 (T,wt=9): 12306 x v (y ^ (x' v z)')' = 1. [para(12202(a,1),548(a,1,2)),rewrite([2(6)])]. given #505 (T,wt=9): 12311 x v ((y ^ x)' v z)' = x. [para(12202(a,1),100(a,1,2)),rewrite([24(2)]),flip(a)]. given #506 (T,wt=9): 12315 x v ((x' v y)' ^ z) = x. [para(12202(a,1),214(a,1,2)),rewrite([2(5),12202(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))]. Low Water (keep): wt=24, iters=6685 ============================== SELECTOR REPORT ======================= Sos_deleted=177, Sos_displaced=0, Sos_size=12229 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 12229 100 F 4 low weight 0 0 T 4 low weight 12229 396 ============================== end of selector report ================ given #508 (T,wt=9): 12336 x v (y ^ (x' v z)') = x. [para(12202(a,1),824(a,1,2)),rewrite([2(5),12202(9)])]. given #509 (T,wt=9): 12363 x v (y v (z v x'))' = x. [para(210(a,1),12202(a,1,2,1))]. given #510 (T,wt=9): 12390 x ^ (y v x')' = (y v x')'. [para(12290(a,1),18(a,1,2)),rewrite([4(4)])]. given #511 (T,wt=9): 12391 x v (y v (x ^ z)')' = x. [para(12290(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))]. given #513 (T,wt=9): 12396 (x v y')' ^ (z v y)' = 0. [para(12290(a,1),141(a,1,2,1,2))]. given #514 (T,wt=9): 12398 x v ((y v x')' ^ z)' = 1. [para(12290(a,1),544(a,1,2)),rewrite([2(6)])]. Low Water (keep): wt=23, iters=6738 ============================== SELECTOR REPORT ======================= Sos_deleted=232, Sos_displaced=0, Sos_size=12688 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 12688 101 F 4 low weight 0 0 T 4 low weight 12688 402 ============================== end of selector report ================ given #515 (T,wt=9): 12399 x v (y ^ (z v x')')' = 1. [para(12290(a,1),548(a,1,2)),rewrite([2(6)])]. given #516 (T,wt=9): 12404 x v (y v (z ^ x)')' = x. [para(12290(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): 12409 x v ((y v x')' ^ z) = x. [para(12290(a,1),214(a,1,2)),rewrite([2(5),12290(9)])]. given #519 (T,wt=9): 12430 x v (y ^ (z v x')') = x. [para(12290(a,1),824(a,1,2)),rewrite([2(5),12290(9)])]. given #520 (T,wt=9): 12487 x' v (y v (x v z))' = x'. [para(15(a,1),12301(a,1,2,1))]. given #521 (T,wt=9): 12488 x' ^ (x v y)' = (x v y)'. [para(12301(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): 12492 (x v y)' ^ (z v x')' = 0. [para(12301(a,1),141(a,1,2,1,2))]. given #524 (T,wt=9): 12494 x' v ((x v y)' ^ z)' = 1. [para(12301(a,1),544(a,1,2)),rewrite([2(6)])]. given #525 (T,wt=9): 12495 x' v (y ^ (x v z)')' = 1. [para(12301(a,1),548(a,1,2)),rewrite([2(6)])]. given #526 (T,wt=9): 12504 x' v ((x v y)' ^ z) = x'. [para(12301(a,1),214(a,1,2)),rewrite([2(5),12301(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): 12526 x' v (y ^ (x v z)') = x'. [para(12301(a,1),824(a,1,2)),rewrite([2(5),12301(9)])]. given #529 (T,wt=9): 12552 x' != 1 | x' != 0 | x' = x. [para(12301(a,1),207(a,1)),rewrite([259(8),12301(10)]),flip(b),flip(c)]. given #530 (T,wt=9): 12554 x' v (y v (z v x))' = x'. [para(210(a,1),12301(a,1,2,1))]. given #531 (T,wt=9): 12582 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),12394(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): 14842 x' ^ (x ^ y)' = x'. [para(12582(a,1),6(a,1,2))]. given #534 (T,wt=7): 14946 x' ^ (y ^ x)' = x'. [para(4(a,1),14842(a,1,2,1))]. given #535 (T,wt=7): 14950 x ^ (x' ^ y)' = x. [para(259(a,1),14842(a,1,1)),rewrite([259(6)])]. given #536 (T,wt=7): 14994 x ^ (y ^ x')' = x. [para(259(a,1),14946(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): 12587 x' ^ (y v x)' = (y v x)'. [para(12394(a,1),18(a,1,2)),rewrite([4(4)])]. given #539 (T,wt=9): 12588 x' v (y ^ x)' = (y ^ x)'. [para(24(a,1),12394(a,1,2,1)),rewrite([2(4)])]. given #540 (T,wt=9): 12597 (x v y)' ^ (z v y')' = 0. [para(12394(a,1),141(a,1,2,1,2))]. given #541 (T,wt=9): 12599 x' v ((y v x)' ^ z)' = 1. [para(12394(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): 12600 x' v (y ^ (z v x)')' = 1. [para(12394(a,1),548(a,1,2)),rewrite([2(6)])]. Low Water (keep): wt=21, iters=6695 ============================== SELECTOR REPORT ======================= Sos_deleted=755, Sos_displaced=0, Sos_size=14241 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 14241 107 F 4 low weight 0 0 T 4 low weight 14241 425 ============================== end of selector report ================ given #544 (T,wt=9): 12612 x' v ((y v x)' ^ z) = x'. [para(12394(a,1),214(a,1,2)),rewrite([2(5),12394(9)])]. given #545 (T,wt=9): 12635 x' v (y ^ (z v x)') = x'. [para(12394(a,1),824(a,1,2)),rewrite([2(5),12394(9)])]. given #546 (T,wt=9): 12861 x ^ (y' v (x ^ y))' = 0. [para(12297(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): 12873 x ^ (y' v (y ^ x))' = 0. [para(12297(a,1),1041(a,1,2))]. given #549 (T,wt=9): 12932 x' ^ ((x ^ y)' v z)' = 0. [para(12298(a,1),129(a,1,2,1)),rewrite([4(6)])]. given #550 (T,wt=9): 13015 (x' v y)' ^ (x v z)' = 0. [para(2(a,1),12303(a,1,2,1))]. given #551 (T,wt=9): 13016 (x v y)' ^ (y' v z)' = 0. [para(12303(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): 13018 x' ^ ((y ^ x)' v z)' = 0. [para(24(a,1),12303(a,1,2,1)),rewrite([4(6)])]. given #554 (T,wt=9): 13595 x ^ ((x ^ y) v y')' = 0. [para(12390(a,1),131(a,1,2))]. given #555 (T,wt=9): 13606 x ^ ((y ^ x) v y')' = 0. [para(12390(a,1),986(a,1,2))]. given #556 (T,wt=9): 13657 x' ^ ((x ^ y)' v z) = x'. [para(12298(a,1),12390(a,1,2,1)),rewrite([4(5),12298(10)])]. 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): 13658 x' ^ ((y ^ x)' v z) = x'. [para(12311(a,1),12390(a,1,2,1)),rewrite([4(5),12311(10)])]. given #559 (T,wt=9): 13664 x' ^ (y v (x ^ z)')' = 0. [para(12391(a,1),129(a,1,2,1)),rewrite([4(6)])]. given #560 (T,wt=9): 13744 x' ^ (y v (x ^ z)') = x'. [para(12391(a,1),12390(a,1,2,1)),rewrite([4(5),12391(10)])]. given #561 (T,wt=9): 13834 (x v y')' ^ (y v z)' = 0. [para(2(a,1),12396(a,1,2,1))]. given #562 (A,wt=19): 252 x ^ (y v (z ^ (x v (u v (y' v w))))) = 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): 13836 x' ^ (y v (z ^ x)')' = 0. [para(24(a,1),12396(a,1,2,1)),rewrite([4(6)])]. given #564 (T,wt=9): 14024 x' ^ (y v (z ^ x)') = x'. [para(12404(a,1),12390(a,1,2,1)),rewrite([4(5),12404(10)])]. given #565 (T,wt=9): 14316 x ^ (y v (x ^ y'))' = 0. [para(12488(a,1),143(a,1,2))]. given #566 (T,wt=9): 14330 x ^ (y v (y' ^ x))' = 0. [para(12488(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): 14467 (x v y)' ^ (x' v z)' = 0. [para(2(a,1),12492(a,1,2,1))]. given #569 (T,wt=9): 14847 x v (x' ^ y)' = (x' ^ y)'. [para(259(a,1),12582(a,1,1))]. given #570 (T,wt=9): 14861 x v (y ^ (x v y'))' = 1. [para(12582(a,1),183(a,1,2))]. given #571 (T,wt=9): 14893 x v (y ^ (y' v x))' = 1. [para(12582(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): 14948 x' ^ (y ^ (x ^ z))' = x'. [para(17(a,1),14842(a,1,2,1))]. given #574 (T,wt=9): 14951 (x ^ y)' v (z ^ x')' = 1. [para(14842(a,1),184(a,1,2,1,2))]. given #575 (T,wt=9): 14974 x' ^ (y ^ (z ^ x))' = x'. [para(195(a,1),14842(a,1,2,1))]. given #576 (T,wt=9): 14995 (x ^ y)' v (z ^ y')' = 1. [para(14946(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): 15076 x ^ (y ^ (x' ^ z))' = x. [para(17(a,1),14950(a,1,2,1))]. given #579 (T,wt=9): 15077 x ^ ((x v y)' ^ z)' = x. [para(14950(a,1),20(a,1,2)),rewrite([6(2)]),flip(a)]. given #580 (T,wt=9): 15080 (x' ^ y)' v (z ^ x)' = 1. [para(14950(a,1),184(a,1,2,1,2))]. given #581 (T,wt=9): 15081 x ^ ((x' ^ y)' v z)' = 0. [para(14950(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): 15082 x ^ (y v (x' ^ z)')' = 0. [para(14950(a,1),563(a,1,2)),rewrite([4(6)])]. given #584 (T,wt=9): 15083 x ^ ((y v x)' ^ z)' = x. [para(14950(a,1),81(a,1,2)),rewrite([18(2)]),flip(a)]. given #585 (T,wt=9): 15088 x ^ ((x' ^ y)' v z) = x. [para(14950(a,1),196(a,1,2)),rewrite([4(5),14950(9)])]. given #586 (T,wt=9): 15103 x ^ (y v (x' ^ z)') = x. [para(14950(a,1),777(a,1,2)),rewrite([4(5),14950(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): 15129 x ^ (y ^ (z ^ x'))' = x. [para(195(a,1),14950(a,1,2,1))]. given #589 (T,wt=9): 15150 x v (y ^ x')' = (y ^ x')'. [para(14994(a,1),24(a,1,2)),rewrite([2(4)])]. given #590 (T,wt=9): 15151 x ^ (y ^ (x v z)')' = x. [para(14994(a,1),20(a,1,2)),rewrite([6(2)]),flip(a)]. given #591 (T,wt=9): 15154 (x ^ y')' v (z ^ y)' = 1. [para(14994(a,1),184(a,1,2,1,2))]. Low Water (keep): wt=20, iters=6697 ============================== SELECTOR REPORT ======================= Sos_deleted=2406, Sos_displaced=0, Sos_size=16010 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 16010 116 F 4 low weight 0 0 T 4 low weight 16010 464 ============================== end of selector report ================ 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): 15155 x ^ ((y ^ x')' v z)' = 0. [para(14994(a,1),560(a,1,2)),rewrite([4(6)])]. given #594 (T,wt=9): 15156 x ^ (y v (z ^ x')')' = 0. [para(14994(a,1),563(a,1,2)),rewrite([4(6)])]. given #595 (T,wt=9): 15157 x ^ (y ^ (z v x)')' = x. [para(14994(a,1),81(a,1,2)),rewrite([18(2)]),flip(a)]. given #596 (T,wt=9): 15162 x ^ ((y ^ x')' v z) = x. [para(14994(a,1),196(a,1,2)),rewrite([4(5),14994(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): 15176 x ^ (y v (z ^ x')') = x. [para(14994(a,1),777(a,1,2)),rewrite([4(5),14994(9)])]. given #599 (T,wt=9): 15438 (x ^ y)' v (x' ^ z)' = 1. [para(7(a,1),12599(a,1,2,1,1,1))]. given #600 (T,wt=9): 15442 (x ^ y)' v (y' ^ z)' = 1. [para(24(a,1),12599(a,1,2,1,1,1))]. given #601 (T,wt=9): 16503 x v (y' ^ (x v y))' = 1. [para(14847(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): 16525 x v (y' ^ (y v x))' = 1. [para(14847(a,1),1300(a,1,2))]. given #604 (T,wt=9): 16719 (x ^ y')' v (y ^ z)' = 1. [para(14951(a,1),2(a,1)),flip(a)]. given #605 (T,wt=9): 17019 (x' ^ y)' v (x ^ z)' = 1. [para(4(a,1),15080(a,1,2,1))]. given #606 (T,wt=9): 17387 x v ((x v y) ^ y')' = 1. [para(15150(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): 17408 x v ((y v x) ^ y')' = 1. [para(15150(a,1),1254(a,1,2))]. given #609 (T,wt=11): 12291 x v ((x' v y)' v z) = x v z. [para(12202(a,1),3(a,1,1)),flip(a)]. given #610 (T,wt=11): 12295 x v (y v (x' v z)') = y v x. [para(12202(a,1),15(a,1,2)),flip(a)]. Low Water (keep): wt=19, iters=6733 ============================== SELECTOR REPORT ======================= Sos_deleted=2921, Sos_displaced=0, Sos_size=16494 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 16494 120 F 4 low weight 0 0 T 4 low weight 16494 479 ============================== end of selector report ================ given #611 (T,wt=11): 12299 (x' v y)' ^ (z v x) = (x' v y)'. [para(12202(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): 12312 (x v (y' v z)') ^ (x v y)' = 0. [para(12202(a,1),145(a,1,2,1,2))]. given #614 (T,wt=11): 12314 x' ^ ((x ^ y) v (x' v z)') = 0. [para(12202(a,1),174(a,1,2,1)),rewrite([4(7)])]. given #615 (T,wt=11): 12319 x v (y v (x v (y' v z)')') = 1. [para(12202(a,1),282(a,1,2,2)),rewrite([2(6)])]. given #616 (T,wt=11): 12321 (x' v y)' ^ (z v (u v x))' = 0. [para(12202(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): 12322 (x' v y)' ^ ((z v x)' ^ u) = 0. [para(12202(a,1),372(a,1,2,1,1,2))]. given #619 (T,wt=11): 12323 (x' v y)' ^ (z ^ (u v x)') = 0. [para(12202(a,1),375(a,1,2,2,1,2))]. given #620 (T,wt=11): 12324 x v (y ^ ((x' v z)' ^ u))' = 1. [para(12202(a,1),551(a,1,2)),rewrite([2(7)])]. given #621 (T,wt=11): 12325 x v (y ^ (z ^ (x' v u)'))' = 1. [para(12202(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): 12326 (x v y)' ^ (z ^ (y' v u)') = 0. [para(12202(a,1),568(a,1,1,1,2))]. given #624 (T,wt=11): 12327 ((x' v y)' ^ z)' v (u v x) = 1. [para(12202(a,1),573(a,1,2,2))]. given #625 (T,wt=11): 12328 (x ^ (y' v z)')' v (u v y) = 1. [para(12202(a,1),600(a,1,2,2))]. given #626 (T,wt=11): 12329 (x' v y)' ^ (z ^ (x ^ z)') = 0. [para(12202(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): 12330 (x ^ y) v ((x' v z)' ^ y)' = 1. [para(12202(a,1),776(a,1,1,1))]. given #629 (T,wt=11): 12332 (x' v y)' ^ (z ^ (z ^ x)') = 0. [para(12202(a,1),781(a,1,2,2,1,2))]. given #630 (T,wt=11): 12333 (x ^ y) v (x ^ (y' v z)')' = 1. [para(12202(a,1),797(a,1,1,2))]. given #631 (T,wt=9): 18781 (x ^ y) v (y' v x') = 1. [para(12390(a,1),12333(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): 18782 (x' ^ y) v (y' v x) = 1. [para(12587(a,1),12333(a,1,2,1)),rewrite([259(6)])]. given #634 (T,wt=9): 18827 x v ((x' ^ y) v y') = 1. [hyper(207,a,18781,a,b,14330,a(flip)),rewrite([14330(5),76(2),14330(6),259(7),3(7),64(8)]),flip(a)]. given #635 (T,wt=9): 18828 x v ((y ^ x') v y') = 1. [hyper(207,a,18781,a,b,14316,a(flip)),rewrite([14316(5),76(2),14316(6),259(7),3(7),64(8)]),flip(a)]. given #636 (T,wt=9): 18829 (x ^ y) v (x' v y') = 1. [hyper(207,a,18781,a,b,13606,a(flip)),rewrite([13606(5),76(2),13606(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): 18830 x' v ((x ^ y) v y') = 1. [hyper(207,a,18781,a,b,12873,a(flip)),rewrite([12873(5),76(2),12873(6),259(7),3(7),64(8)]),flip(a)]. given #639 (T,wt=9): 18831 x' v ((y ^ x) v y') = 1. [hyper(207,a,18781,a,b,12861,a(flip)),rewrite([12861(5),76(2),12861(6),259(7),3(7),64(8)]),flip(a)]. given #640 (T,wt=9): 18864 x' v (y ^ (y ^ x)')' = 1. [hyper(207,a,18781,a,b,153,a(flip)),rewrite([153(4),76(2),153(5),2(8),64(9)]),flip(a)]. given #641 (T,wt=9): 18869 x' v (y ^ (x ^ y)')' = 1. [hyper(207,a,18781,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): 18902 x' v (y' v (y ^ x)) = 1. [para(18781(a,1),389(a,1,2,2,2,1)),rewrite([73(5),2(5),64(5)])]. given #644 (T,wt=9): 18954 x v (y v (y' ^ x')) = 1. [hyper(207,a,18782,a,b,14330,a(flip)),rewrite([14330(7),76(2),14330(8),259(8),2(7),64(8)]),flip(a)]. given #645 (T,wt=9): 18955 x v (y v (x' ^ y')) = 1. [hyper(207,a,18782,a,b,14316,a(flip)),rewrite([14316(7),76(2),14316(8),259(8),2(7),64(8)]),flip(a)]. given #646 (T,wt=9): 18956 x v (y' v (y ^ x')) = 1. [hyper(207,a,18782,a,b,12873,a(flip)),rewrite([12873(7),76(2),12873(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): 18957 x v (y' v (x' ^ y)) = 1. [hyper(207,a,18782,a,b,12861,a(flip)),rewrite([12861(7),76(2),12861(8),259(8),2(7),64(8)]),flip(a)]. given #649 (T,wt=9): 18988 x v (y ^ (y ^ x')')' = 1. [hyper(207,a,18782,a,b,153,a(flip)),rewrite([153(6),76(2),153(7),2(8),64(9)]),flip(a)]. given #650 (T,wt=9): 18993 x v (y ^ (x' ^ y)')' = 1. [hyper(207,a,18782,a,b,32,a(flip)),rewrite([32(6),76(2),32(7),2(8),64(9)]),flip(a)]. given #651 (T,wt=9): 19007 x' v (y v (y' ^ x)) = 1. [para(18782(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): 19008 (x ^ y') v (x' v y) = 1. [para(4(a,1),18782(a,1,1))]. given #654 (T,wt=9): 19104 x' v (y v (x ^ y')) = 1. [para(18828(a,1),390(a,1,2,2,2,1)),rewrite([73(5),2(5),64(5)])]. given #655 (T,wt=9): 19112 x' v (y' v (x ^ y)) = 1. [hyper(207,a,18829,a,b,12861,a(flip)),rewrite([12861(5),76(2),12861(6),259(8),64(8)]),flip(a)]. given #656 (T,wt=11): 12334 x ^ ((y' v z)' ^ (x ^ y)') = 0. [para(12202(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): 12335 x' ^ ((y ^ x) v (x' v z)') = 0. [para(12202(a,1),821(a,1,2,1)),rewrite([4(7)])]. given #659 (T,wt=11): 12337 ((x' v y)' v z) ^ (z v x)' = 0. [para(12202(a,1),975(a,1,2,1,2))]. given #660 (T,wt=11): 12339 x' ^ ((x' v y)' v (x ^ z)) = 0. [para(12202(a,1),1191(a,1,2,1)),rewrite([4(7)])]. given #661 (T,wt=11): 12346 x v (y v ((y' v z)' v x)') = 1. [para(12202(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): 12347 x ^ ((y' v z)' ^ (y ^ x)') = 0. [para(12202(a,1),2021(a,1,2,2,1,1))]. given #664 (T,wt=11): 12349 (x ^ y) v ((y' v z)' ^ x)' = 1. [para(12202(a,1),2970(a,1,1,2))]. given #665 (T,wt=11): 12350 (x ^ y) v (y ^ (x' v z)')' = 1. [para(12202(a,1),2971(a,1,1,1))]. given #666 (T,wt=11): 12352 x' ^ ((x' v y)' v (z ^ x)) = 0. [para(12202(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): 12358 x v ((y ^ (x ^ z))' v u)' = x. [para(12202(a,1),170(a,1,2)),rewrite([71(3)]),flip(a)]. given #669 (T,wt=11): 12362 (x' v y)' v (z v x) = z v x. [para(12202(a,1),210(a,1,2,2)),rewrite([12202(9)])]. given #670 (T,wt=11): 12368 x v ((y ^ (z ^ x))' v u)' = x. [para(12202(a,1),239(a,1,2)),rewrite([102(3)]),flip(a)]. given #671 (T,wt=11): 12385 x v ((y v x')' v z) = x v z. [para(12290(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): 12389 x v (y v (z v x')') = y v x. [para(12290(a,1),15(a,1,2)),flip(a)]. given #674 (T,wt=11): 12392 (x v y')' ^ (z v y) = (x v y')'. [para(12290(a,1),80(a,1,2,2))]. given #675 (T,wt=11): 12405 (x v (y v z')') ^ (x v z)' = 0. [para(12290(a,1),145(a,1,2,1,2))]. given #676 (T,wt=11): 12408 x' ^ ((x ^ y) v (z v x')') = 0. [para(12290(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): 12413 x v (y v (x v (z v y')')') = 1. [para(12290(a,1),282(a,1,2,2)),rewrite([2(6)])]. given #679 (T,wt=11): 12415 (x v y')' ^ (z v (u v y))' = 0. [para(12290(a,1),371(a,1,2,1,2,2))]. given #680 (T,wt=11): 12416 (x v y')' ^ ((z v y)' ^ u) = 0. [para(12290(a,1),372(a,1,2,1,1,2))]. given #681 (T,wt=11): 12417 (x v y')' ^ (z ^ (u v y)') = 0. [para(12290(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): 12418 x v (y ^ ((z v x')' ^ u))' = 1. [para(12290(a,1),551(a,1,2)),rewrite([2(7)])]. given #684 (T,wt=11): 12419 x v (y ^ (z ^ (u v x')'))' = 1. [para(12290(a,1),553(a,1,2)),rewrite([2(7)])]. given #685 (T,wt=11): 12420 (x v y)' ^ (z ^ (u v y')') = 0. [para(12290(a,1),568(a,1,1,1,2))]. given #686 (T,wt=11): 12421 ((x v y')' ^ z)' v (u v y) = 1. [para(12290(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): 12422 (x ^ (y v z')')' v (u v z) = 1. [para(12290(a,1),600(a,1,2,2))]. given #689 (T,wt=11): 12423 (x v y')' ^ (z ^ (y ^ z)') = 0. [para(12290(a,1),774(a,1,2,2,1,1))]. given #690 (T,wt=11): 12424 (x ^ y) v ((z v x')' ^ y)' = 1. [para(12290(a,1),776(a,1,1,1))]. Low Water (keep): wt=18, iters=6671 ============================== SELECTOR REPORT ======================= Sos_deleted=9364, Sos_displaced=0, Sos_size=18687 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 18687 136 F 4 low weight 0 0 T 4 low weight 18687 543 ============================== end of selector report ================ given #691 (T,wt=11): 12426 (x v y')' ^ (z ^ (z ^ y)') = 0. [para(12290(a,1),781(a,1,2,2,1,2))]. Low Water (keep): wt=17, iters=6692 ============================== SELECTOR REPORT ======================= Sos_deleted=9367, Sos_displaced=0, Sos_size=18730 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 18730 136 F 4 low weight 0 0 T 4 low weight 18730 544 ============================== end of selector report ================ 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): 12427 (x ^ y) v (x ^ (z v y')')' = 1. [para(12290(a,1),797(a,1,1,2))]. given #694 (T,wt=11): 12428 x ^ ((y v z')' ^ (x ^ z)') = 0. [para(12290(a,1),801(a,1,2,2,1,2))]. given #695 (T,wt=11): 12429 x' ^ ((y ^ x) v (z v x')') = 0. [para(12290(a,1),821(a,1,2,1)),rewrite([4(7)])]. given #696 (T,wt=11): 12431 ((x v y')' v z) ^ (z v y)' = 0. [para(12290(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): 12433 x' ^ ((y v x')' v (x ^ z)) = 0. [para(12290(a,1),1191(a,1,2,1)),rewrite([4(7)])]. given #699 (T,wt=11): 12441 x v (y v ((z v y')' v x)') = 1. [para(12290(a,1),1670(a,1,2,2)),rewrite([2(6)])]. given #700 (T,wt=11): 12442 x ^ ((y v z')' ^ (z ^ x)') = 0. [para(12290(a,1),2021(a,1,2,2,1,1))]. given #701 (T,wt=11): 12444 (x ^ y) v ((z v y')' ^ x)' = 1. [para(12290(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): 12445 (x ^ y) v (y ^ (z v x')')' = 1. [para(12290(a,1),2971(a,1,1,1))]. given #704 (T,wt=11): 12447 x' ^ ((y v x')' v (z ^ x)) = 0. [para(12290(a,1),3146(a,1,2,1)),rewrite([4(7)])]. given #705 (T,wt=11): 12453 x v (y v (z ^ (x ^ u))')' = x. [para(12290(a,1),170(a,1,2)),rewrite([71(3)]),flip(a)]. given #706 (T,wt=11): 12457 (x v y')' v (z v y) = z v y. [para(12290(a,1),210(a,1,2,2)),rewrite([12290(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): 12462 x v (y v (z ^ (u ^ x))')' = x. [para(12290(a,1),239(a,1,2)),rewrite([102(3)]),flip(a)]. given #709 (T,wt=11): 12482 x' v ((x v y)' v z) = x' v z. [para(12301(a,1),3(a,1,1)),flip(a)]. given #710 (T,wt=11): 12486 x' v (y v (x v z)') = y v x'. [para(12301(a,1),15(a,1,2)),flip(a)]. given #711 (T,wt=11): 12489 (x v y)' ^ (z v x') = (x v y)'. [para(12301(a,1),80(a,1,2,2))]. given #712 (A,wt=19): 319 x ^ (y v (z ^ (x v (u v (w 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): 12500 (x v (y v z)') ^ (x v y')' = 0. [para(12301(a,1),145(a,1,2,1,2))]. given #714 (T,wt=11): 12503 x ^ ((x' ^ y) v (x v z)') = 0. [para(12301(a,1),174(a,1,2,1)),rewrite([259(7),4(6)])]. given #715 (T,wt=11): 12505 (x ^ y)' v (z v x)' = (x ^ y)'. [para(214(a,1),12301(a,1,2,1))]. given #716 (T,wt=11): 12509 x v (y' v (x v (y v z)')') = 1. [para(12301(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): 21594 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): 21598 x ^ y != 0 | y ^ x = 0. [para(228(a,1),21594(a,1)),rewrite([228(6)])]. given #720 (T,wt=11): 12511 (x v y)' ^ (z v (u v x'))' = 0. [para(12301(a,1),371(a,1,2,1,2,2))]. given #721 (T,wt=11): 12512 (x v y)' ^ ((z v x')' ^ u) = 0. [para(12301(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): 12513 (x v y)' ^ (z ^ (u v x')') = 0. [para(12301(a,1),375(a,1,2,2,1,2))]. given #724 (T,wt=11): 12514 x' v (y ^ ((x v z)' ^ u))' = 1. [para(12301(a,1),551(a,1,2)),rewrite([2(7)])]. given #725 (T,wt=11): 12515 x' v (y ^ (z ^ (x v u)'))' = 1. [para(12301(a,1),553(a,1,2)),rewrite([2(7)])]. given #726 (T,wt=11): 12516 (x v y')' ^ (z ^ (y v u)') = 0. [para(12301(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): 12517 ((x v y)' ^ z)' v (u v x') = 1. [para(12301(a,1),573(a,1,2,2))]. given #729 (T,wt=11): 12518 (x ^ (y v z)')' v (u v y') = 1. [para(12301(a,1),600(a,1,2,2))]. given #730 (T,wt=11): 12519 (x v y)' ^ (z ^ (x' ^ z)') = 0. [para(12301(a,1),774(a,1,2,2,1,1))]. given #731 (T,wt=11): 12520 (x' ^ y) v ((x v z)' ^ y)' = 1. [para(12301(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): 12522 (x v y)' ^ (z ^ (z ^ x')') = 0. [para(12301(a,1),781(a,1,2,2,1,2))]. given #734 (T,wt=11): 12523 (x ^ y') v (x ^ (y v z)')' = 1. [para(12301(a,1),797(a,1,1,2))]. given #735 (T,wt=11): 12524 x ^ ((y v z)' ^ (x ^ y')') = 0. [para(12301(a,1),801(a,1,2,2,1,2))]. given #736 (T,wt=11): 12525 x ^ ((y ^ x') v (x v z)') = 0. [para(12301(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): 12527 (x ^ y)' v (z v y)' = (x ^ y)'. [para(824(a,1),12301(a,1,2,1))]. given #739 (T,wt=11): 12528 ((x v y)' v z) ^ (z v x')' = 0. [para(12301(a,1),975(a,1,2,1,2))]. given #740 (T,wt=11): 12531 x ^ ((x v y)' v (x' ^ z)) = 0. [para(12301(a,1),1191(a,1,2,1)),rewrite([259(7),4(6)])]. given #741 (T,wt=11): 12539 x v (y' v ((y v z)' v x)') = 1. [para(12301(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): 12540 x ^ ((y v z)' ^ (y' ^ x)') = 0. [para(12301(a,1),2021(a,1,2,2,1,1))]. given #744 (T,wt=11): 12542 (x ^ y') v ((y v z)' ^ x)' = 1. [para(12301(a,1),2970(a,1,1,2))]. given #745 (T,wt=11): 12543 (x' ^ y) v (y ^ (x v z)')' = 1. [para(12301(a,1),2971(a,1,1,1))]. given #746 (T,wt=11): 12545 x ^ ((x v y)' v (z ^ x')) = 0. [para(12301(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): 12553 (x v y)' v (z v x') = z v x'. [para(12301(a,1),210(a,1,2,2)),rewrite([12301(9)])]. given #749 (T,wt=11): 12557 (x ^ y)' v (y ^ x)' = (x ^ y)'. [para(220(a,1),12301(a,1,2,1))]. given #750 (T,wt=10): 22143 (x ^ y)' != 0 | (y ^ x)' = 0. [para(12557(a,1),21594(a,1)),rewrite([12557(9)])]. given #751 (T,wt=10): 22147 (x v y)' != 0 | (y v x)' = 0. [para(213(a,1),22143(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): 12579 (x v y) ^ (x v (y ^ x'))' = 0. [back_rewrite(12090),rewrite([12521(8)])]. Low Water (displace): id=11629, wt=25 given #754 (T,wt=9): 22247 (x v (y ^ x'))' = (x v y)'. [hyper(297,a,395,a,b,12579,a),flip(a)]. given #755 (T,wt=9): 22262 (x ^ y') v (y v x)' = y'. [back_rewrite(21810),rewrite([22247(6)])]. given #756 (T,wt=7): 22422 (x ^ y)' = x' v y'. [para(14842(a,1),22262(a,1,1)),rewrite([22297(5),22345(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): 26892 (x' v y)' = x ^ y'. [back_rewrite(19411),rewrite([22492(5)]),xx(a)]. given #759 (T,wt=7): 27532 (x v y)' = x' ^ y'. [para(259(a,1),26892(a,1,1,1))]. given #760 (T,wt=9): 22273 x v (y ^ x') = x v y. [para(22247(a,1),259(a,1,1)),rewrite([259(3)]),flip(a)]. given #761 (T,wt=9): 22431 x ^ ((x ^ y) v y') = x. [para(18830(a,1),22262(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): 22432 x ^ ((y ^ x) v y') = x. [para(18831(a,1),22262(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. given #764 (T,wt=9): 22433 x ^ (y' v (y ^ x)) = x. [para(18902(a,1),22262(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. given #765 (T,wt=9): 23578 x' ^ (y ^ (y' v x)) = 0. [back_rewrite(16524),rewrite([22422(4),259(3),3(5),46(5)])]. given #766 (T,wt=9): 27065 (x ^ y) v (x ^ y') = x. [back_rewrite(22327),rewrite([26892(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): 27072 (x ^ y) v (y ^ x') = y. [back_rewrite(22319),rewrite([26892(4)])]. given #769 (T,wt=9): 27524 x ^ ((x' v y) ^ y') = 0. [para(26892(a,1),9(a,1,2)),rewrite([17(5)])]. given #770 (T,wt=9): 27542 x ^ ((y v x') ^ y') = 0. [para(26892(a,1),979(a,1,2)),rewrite([17(5)])]. given #771 (T,wt=9): 30009 x' ^ (x v y') = x' ^ y'. [back_rewrite(22268),rewrite([27532(4),22422(4),259(3),27532(6)])]. given #772 (A,wt=21): 341 (x v y) ^ (z v ((x v (y v u)) ^ (x v (y v w)))) = 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): 33030 (x v y) ^ (y' ^ x') = 0. [back_rewrite(979),rewrite([27532(3)])]. given #774 (T,wt=9): 33193 (x v y) ^ (x' ^ y') = 0. [para(27532(a,1),9(a,1,2))]. given #775 (T,wt=9): 33269 x v (x' ^ y) = x v y. [para(4(a,1),22273(a,1,2))]. given #776 (T,wt=9): 33274 x' v (y ^ x) = x' v y. [para(259(a,1),22273(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): 33322 x' ^ (y' v x) = x' ^ y'. [para(22273(a,1),27532(a,1,1)),rewrite([27532(2),22422(7),259(7)]),flip(a)]. given #779 (T,wt=9): 33385 (x ^ y) v y' = x v y'. [para(22431(a,1),24(a,1,2)),rewrite([2(4),22(4)]),flip(a)]. given #780 (T,wt=9): 33533 (x ^ y) v x' = y v x'. [para(22432(a,1),24(a,1,2)),rewrite([2(4),100(4)]),flip(a)]. given #781 (T,wt=9): 33557 x' v (x ^ y) = x' v y. [para(22433(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): 33608 (x v y) ^ (y v x') = y. [hyper(34,a,2979,a,b,23578,a),rewrite([259(2),27532(3),2(5),22273(5)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 22.23 (+ 0.25) 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)])]. 12090 x' ^ ((x v y) ^ (x v (y ^ x'))') = 0. [para(589(a,1),276(a,1,2)),rewrite([4(8),5(8)])]. 12143 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)]. 12202 x v (x' v y)' = x. [hyper(7145,a,12143,a),rewrite([2(4)])]. 12290 x v (y v x')' = x. [para(2(a,1),12202(a,1,2,1))]. 12297 x ^ (x' v y)' = (x' v y)'. [para(12202(a,1),18(a,1,2)),rewrite([4(4)])]. 12301 x' v (x v y)' = x'. [para(259(a,1),12202(a,1,2,1,1))]. 12333 (x ^ y) v (x ^ (y' v z)')' = 1. [para(12202(a,1),797(a,1,1,2))]. 12335 x' ^ ((y ^ x) v (x' v z)') = 0. [para(12202(a,1),821(a,1,2,1)),rewrite([4(7)])]. 12390 x ^ (y v x')' = (y v x')'. [para(12290(a,1),18(a,1,2)),rewrite([4(4)])]. 12394 x' v (y v x)' = x'. [para(259(a,1),12290(a,1,2,1,2))]. 12521 x' ^ (y ^ (x v z)') = y ^ (x v z)'. [para(12301(a,1),777(a,1,1))]. 12525 x ^ ((y ^ x') v (x v z)') = 0. [para(12301(a,1),821(a,1,2,1)),rewrite([259(7),4(6)])]. 12579 (x v y) ^ (x v (y ^ x'))' = 0. [back_rewrite(12090),rewrite([12521(8)])]. 12582 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),12394(a,1,2,1)),rewrite([2(4)])]. 12587 x' ^ (y v x)' = (y v x)'. [para(12394(a,1),18(a,1,2)),rewrite([4(4)])]. 12873 x ^ (y' v (y ^ x))' = 0. [para(12297(a,1),1041(a,1,2))]. 13606 x ^ ((y ^ x) v y')' = 0. [para(12390(a,1),986(a,1,2))]. 14842 x' ^ (x ^ y)' = x'. [para(12582(a,1),6(a,1,2))]. 14847 x v (x' ^ y)' = (x' ^ y)'. [para(259(a,1),12582(a,1,1))]. 14946 x' ^ (y ^ x)' = x'. [para(4(a,1),14842(a,1,2,1))]. 14994 x ^ (y ^ x')' = x. [para(259(a,1),14946(a,1,1)),rewrite([259(6)])]. 15150 x v (y ^ x')' = (y ^ x')'. [para(14994(a,1),24(a,1,2)),rewrite([2(4)])]. 16524 x' ^ (y ^ ((x' ^ y)' v (x ^ z))) = 0. [para(14847(a,1),1191(a,1,2,1)),rewrite([259(9),4(8),5(8)])]. 17407 x ^ (y' ^ ((x ^ y')' v (y ^ z))) = 0. [para(15150(a,1),1191(a,1,2,1)),rewrite([259(9),4(8),5(8)])]. 18781 (x ^ y) v (y' v x') = 1. [para(12390(a,1),12333(a,1,2,1)),rewrite([259(6)])]. 18782 (x' ^ y) v (y' v x) = 1. [para(12587(a,1),12333(a,1,2,1)),rewrite([259(6)])]. 18830 x' v ((x ^ y) v y') = 1. [hyper(207,a,18781,a,b,12873,a(flip)),rewrite([12873(5),76(2),12873(6),259(7),3(7),64(8)]),flip(a)]. 19008 (x ^ y') v (x' v y) = 1. [para(4(a,1),18782(a,1,1))]. 19411 x ^ (y' ^ (x' v y)) != 0 | (x' v y)' = x ^ y'. [para(19008(a,1),264(a,1,2,2,1)),rewrite([73(6),2(6),64(6),5(5),19008(14),73(11),2(11),64(11)])]. 19458 (x ^ y) v (y' v (x ^ y))' = y. [hyper(149,a,12335,a),rewrite([259(8)])]. 21810 (x ^ y') v (y v (x ^ y'))' = y'. [hyper(149,a,12525,a)]. 22247 (x v (y ^ x'))' = (x v y)'. [hyper(297,a,395,a,b,12579,a),flip(a)]. 22262 (x ^ y') v (y v x)' = y'. [back_rewrite(21810),rewrite([22247(6)])]. 22273 x v (y ^ x') = x v y. [para(22247(a,1),259(a,1,1)),rewrite([259(3)]),flip(a)]. 22274 (x' v (y ^ x))' = (x' v y)'. [para(259(a,1),22247(a,1,1,2,2))]. 22297 ((x ^ y) v x')' = (y v x')'. [para(13606(a,1),22247(a,1,1,2)),rewrite([2(5),64(5),2(8),100(8)])]. 22319 (x ^ y) v (y' v x)' = y. [back_rewrite(19458),rewrite([22274(5)])]. 22345 x v (y v x)' = x v y'. [para(22262(a,1),22(a,1,2)),flip(a)]. 22422 (x ^ y)' = x' v y'. [para(14842(a,1),22262(a,1,1)),rewrite([22297(5),22345(5)]),flip(a)]. 22431 x ^ ((x ^ y) v y') = x. [para(18830(a,1),22262(a,1,2,1)),rewrite([259(5),4(4),73(6),2(6),64(6),259(6)])]. 22492 x ^ (y' ^ (x' v y)) = 0. [back_rewrite(17407),rewrite([22422(4),259(4),3(5),7(4)])]. 23578 x' ^ (y ^ (y' v x)) = 0. [back_rewrite(16524),rewrite([22422(4),259(3),3(5),46(5)])]. 26892 (x' v y)' = x ^ y'. [back_rewrite(19411),rewrite([22492(5)]),xx(a)]. 27072 (x ^ y) v (y ^ x') = y. [back_rewrite(22319),rewrite([26892(4)])]. 27532 (x v y)' = x' ^ y'. [para(259(a,1),26892(a,1,1,1))]. 33426 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(3154(a,1),22431(a,1,2,1)),rewrite([259(6),64(5),4(4)])]. 33608 (x v y) ^ (y v x') = y. [hyper(34,a,2979,a,b,23578,a),rewrite([259(2),27532(3),2(5),22273(5)]),flip(a)]. 33807 (x ^ y) v (x ^ ((y v z) ^ y')) = x ^ (y v z). [para(70(a,1),27072(a,1,1)),rewrite([5(5)])]. 33814 (x ^ y) v (((y ^ x) v (x ^ z)) ^ y') = (y ^ x) v (x ^ z). [para(78(a,1),27072(a,1,1))]. 33841 (x ^ y) v (((y ^ x) v (z ^ x)) ^ y') = (y ^ x) v (z ^ x). [para(522(a,1),27072(a,1,1))]. 33851 x ^ (x' v y) = x ^ y. [para(23578(a,1),27072(a,1,1)),rewrite([259(6),4(5),85(5),64(3)]),flip(a)]. 33909 x ^ (y v (z ^ x)) = x ^ (y v z). [back_rewrite(1002),rewrite([33851(5),33851(7)])]. 34094 (x ^ y) v (z ^ y) = y ^ ((x ^ y) v z). [back_rewrite(33426),rewrite([33909(4)]),flip(a)]. 34352 (x ^ y) v (x ^ (((y ^ x) v z) ^ y')) = x ^ ((y ^ x) v z). [back_rewrite(33841),rewrite([34094(4),5(6),34094(10)])]. 35814 (x v y) ^ x' = y ^ x'. [para(22273(a,1),33608(a,1,1)),rewrite([2(5),24(5)])]. 35831 (x ^ y) v (x ^ (z ^ y')) = x ^ (y v z). [back_rewrite(33807),rewrite([35814(4)])]. 35945 x ^ ((y ^ x) v z) = x ^ (y v z). [back_rewrite(34352),rewrite([35831(7),22(3)]),flip(a)]. 36053 (x ^ y) v (y ^ z) = y ^ (x v (y ^ z)). [back_rewrite(10006),rewrite([35945(4)]),flip(a)]. 36095 x ^ (y v (x ^ z)) = x ^ (y v z). [back_rewrite(33814),rewrite([36053(4),5(6),35814(5),5(4),51(5),35831(5),36053(5)]),flip(a)]. 36108 x ^ ((x ^ y) v z) = x ^ (y v z). [back_rewrite(4971),rewrite([36053(5),36095(5),100(3)]),flip(a)]. 36141 (x ^ y) v (x ^ z) = x ^ (y v z). [back_rewrite(8048),rewrite([36095(4),36108(3)]),flip(a)]. 36142 $F # answer(distributivity). [resolve(36141,a,13,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=783. Generated=768009. Kept=36139. proofs=1. Usable=160. Sos=6822. Demods=5914. Limbo=46, Disabled=29121. Hints=0. Kept_by_rule=0, Deleted_by_rule=26727. Forward_subsumed=688951. Back_subsumed=115. Sos_limit_deleted=16192. Sos_displaced=68. Sos_removed=0. New_demodulators=32406 (6 lex), Back_demodulated=28925. Back_unit_deleted=0. Demod_attempts=15195905. Demod_rewrites=3716782. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=363311. Nonunit_bsub_feature_tests=38708. Megabytes=27.24. User_CPU=22.23, System_CPU=0.25, Wall_clock=23. ============================== end of statistics ===================== ============================== SELECTOR REPORT ======================= Sos_deleted=16192, Sos_displaced=68, Sos_size=6822 SELECTOR PART PRIORITY ORDER SIZE SELECTED I 2147483647 high age 0 11 H 1 high weight 0 0 A 1 low age 6822 155 F 4 low weight 0 0 T 4 low weight 6822 617 ============================== end of selector report ================ ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 24350 exit (max_proofs) Fri Apr 4 11:37:19 2008