============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4110 was started by mccune on cleo.thornwood, Wed Nov 22 11:31:23 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H49.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 H49.in 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). (all x all y (x ^ y = x -> x' v y' = x')). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y (x ^ y = x -> x' v y' = x')) # 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 = c1. [deny(1)]. c1' != c1' v c2'. [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 0, 1, c1, c2, ^, v, ' ]). After inverse_order: Function symbol precedence: lex([ 0, 1, c1, c2, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(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 = c1. [deny(1)]. 15 c1' v c2' != c1'. [copy(14),flip(a)]. 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)]. 13 c1 ^ c2 = c1. [deny(1)]. 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: 16 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: 18 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=6): 8 x v x' = 1. [assumption]. given #8 (I,wt=6): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=14): 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=5): 13 c1 ^ c2 = c1. [deny(1)]. given #12 (I,wt=8): 15 c1' v c2' != c1'. [copy(14),flip(a)]. given #13 (F,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #14 (T,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #15 (T,wt=5): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #16 (A,wt=11): 17 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #17 (F,wt=5): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #18 (F,wt=5): 74 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #19 (T,wt=4): 91 1' = 0. [hyper(10,a,35,a,b,74,a)]. given #20 (T,wt=5): 85 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #21 (A,wt=11): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #22 (F,wt=4): 94 0' = 1. [hyper(10,a,85,a,b,32,a)]. given #23 (F,wt=5): 92 1 v x = 1. [para(74(a,1),6(a,1))]. given #24 (T,wt=5): 95 0 ^ x = 0. [para(85(a,1),6(a,1,2))]. given #25 (T,wt=5): 106 x v 1 = 1. [para(92(a,1),2(a,1)),flip(a)]. given #26 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #27 (F,wt=5): 109 x ^ 0 = 0. [para(95(a,1),4(a,1)),flip(a)]. given #28 (F,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #29 (T,wt=5): 125 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. given #30 (T,wt=7): 108 0 != x | x' = 1. [back_rewrite(75),rewrite(106(2)),xx(a)]. given #31 (A,wt=13): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #32 (F,wt=7): 111 1 != x | x' = 0. [back_rewrite(86),rewrite(109(4)),xx(b)]. given #33 (F,wt=8): 93 x v (x' v y) = 1. [back_rewrite(30),rewrite(92(5))]. given #34 (T,wt=8): 97 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(95(5))]. given #35 (T,wt=8): 107 x v (y v x') = 1. [back_rewrite(79),rewrite(106(5))]. given #36 (A,wt=11): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #37 (F,wt=9): 146 c1 ^ (c1' v c2') != 0. [ur(10,a,93,a,c,15,a(flip))]. given #38 (F,wt=8): 110 x ^ (y ^ x') = 0. [back_rewrite(100),rewrite(109(5))]. given #39 (T,wt=8): 160 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #40 (T,wt=6): 179 c1 ^ c2' = 0. [para(125(a,1),160(a,1,2,1))]. given #41 (A,wt=13): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #42 (F,wt=8): 173 x ^ (y v x)' = 0. [para(2(a,1),160(a,1,2,1))]. given #43 (F,wt=8): 180 c1 ^ (c2' ^ x) = 0. [para(179(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #44 (T,wt=8): 183 c1 ^ (x ^ c2') = 0. [para(179(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #45 (T,wt=9): 57 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #46 (A,wt=11): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #47 (F,wt=7): 207 c1 ^ (c2 v x) = c1. [para(6(a,1),57(a,1,2)),rewrite(13(3)),flip(a)]. given #48 (F,wt=7): 212 c1 ^ (x v c2) = c1. [para(20(a,1),57(a,1,2)),rewrite(13(3)),flip(a)]. given #49 (T,wt=8): 215 c1 ^ (c2 v x)' = 0. [para(160(a,1),57(a,1,2)),rewrite(4(3),95(3)),flip(a)]. given #50 (T,wt=8): 217 c1 ^ (x v c2)' = 0. [para(173(a,1),57(a,1,2)),rewrite(4(3),95(3)),flip(a)]. given #51 (A,wt=13): 25 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #52 (F,wt=8): 220 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #53 (F,wt=8): 261 x v (y ^ x)' = 1. [para(4(a,1),220(a,1,2,1))]. given #54 (T,wt=6): 272 c2 v c1' = 1. [para(13(a,1),261(a,1,2,1))]. given #55 (T,wt=8): 278 c2 v (x v c1') = 1. [para(207(a,1),261(a,1,2,1)),rewrite(3(5))]. given #56 (A,wt=13): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #57 (F,wt=8): 279 c2 v (c1' v x) = 1. [para(272(a,1),3(a,1,1)),rewrite(92(2)),flip(a)]. given #58 (F,wt=9): 58 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite(4(4))]. given #59 (T,wt=7): 299 c2 v (x ^ c1) = c2. [para(58(a,1),7(a,1,2))]. given #60 (T,wt=7): 305 c2 v (c1 ^ x) = c2. [para(4(a,1),299(a,1,2))]. given #61 (A,wt=10): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #62 (F,wt=8): 302 c2 v (x ^ c1)' = 1. [para(58(a,1),220(a,1,2,1))]. given #63 (F,wt=8): 322 c2 v (c1 ^ x)' = 1. [para(4(a,1),302(a,1,2,1))]. given #64 (T,wt=9): 61 x ^ (x ^ y) = x ^ y. [para(28(a,1),5(a,1,1)),flip(a)]. given #65 (T,wt=9): 63 x ^ (y ^ x) = y ^ x. [para(28(a,1),5(a,2,2)),rewrite(4(2))]. given #66 (A,wt=10): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #67 (F,wt=9): 67 x v (x v y) = x v y. [para(29(a,1),3(a,1,1)),flip(a)]. given #68 (F,wt=9): 69 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite(2(2))]. given #69 (T,wt=9): 77 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #70 (T,wt=9): 99 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #71 (A,wt=14): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #72 (F,wt=5): 367 x'' = x. [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #73 (F,wt=8): 390 x' v (y v x) = 1. [para(367(a,1),107(a,1,2,2))]. given #74 (T,wt=8): 391 x' ^ (y ^ x) = 0. [para(367(a,1),110(a,1,2,2))]. given #75 (T,wt=9): 104 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #76 (A,wt=20): 37 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #77 (F,wt=9): 112 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #78 (F,wt=9): 121 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #79 (T,wt=9): 129 c1 v (c2 v x) = c2 v x. [para(125(a,1),3(a,1,1)),flip(a)]. given #80 (T,wt=9): 130 c2 v (x v c1) = x v c2. [para(125(a,1),3(a,2,2)),rewrite(2(4))]. given #81 (A,wt=14): 38 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #82 (F,wt=9): 132 c1 v (x v c2) = x v c2. [para(125(a,1),17(a,1,2)),flip(a)]. given #83 (F,wt=9): 233 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),207(a,1,2))]. given #84 (T,wt=9): 235 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),212(a,1,2))]. given #85 (T,wt=9): 306 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),299(a,1,2))]. given #86 (A,wt=20): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #87 (F,wt=9): 313 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),305(a,1,2))]. given #88 (F,wt=9): 378 c2 ^ c1' != 0 | c2 = c1. [para(272(a,1),36(a,1)),rewrite(4(7),367(12)),flip(c),xx(a)]. given #89 (T,wt=9): 494 c2 v (x v c1) = c2 v x. [para(130(a,2),2(a,1))]. given #90 (T,wt=9): 517 c1 v c2' != 1 | c2 = c1. [para(179(a,1),38(b,1)),rewrite(2(4),367(12)),xx(b)]. given #91 (A,wt=23): 42 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 #92 (F,wt=10): 64 1 != x | 0 != x | x' = x. [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)]. given #93 (F,wt=10): 128 c2 != 1 | c1 != 0 | c1' = c2. [back_rewrite(59),rewrite(125(3))]. given #94 (T,wt=10): 150 x v (y v (x' v z)) = 1. [para(93(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #95 (T,wt=10): 154 x ^ (y ^ (x' ^ z)) = 0. [para(97(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #96 (A,wt=23): 43 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 #97 (F,wt=10): 156 x v (y v (z v x')) = 1. [para(3(a,1),107(a,1,2))]. given #98 (F,wt=10): 167 x ^ ((x v y)' ^ z) = 0. [para(97(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #99 (T,wt=10): 169 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),110(a,1,2))]. given #100 (T,wt=10): 172 x ^ (y ^ (x v z)') = 0. [para(110(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #101 (A,wt=29): 44 x ^ (y v (z v ((x ^ u) v (u ^ (y v (z v v)))))) = x ^ (y v (z v (u ^ (x v v)))). [para(3(a,1),12(a,1,2,2,2,2)),rewrite(3(7),3(12))]. given #102 (F,wt=10): 178 x ^ (y v (x v z))' = 0. [para(17(a,1),160(a,1,2,1))]. given #103 (F,wt=10): 193 x ^ (y v (z v x))' = 0. [para(3(a,1),173(a,1,2,1))]. given #104 (T,wt=10): 194 x ^ ((y v x)' ^ z) = 0. [para(173(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #105 (T,wt=10): 199 x ^ (y ^ (z v x)') = 0. [para(173(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #106 (A,wt=23): 45 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 #107 (F,wt=10): 202 c1 ^ (x ^ (c2' ^ y)) = 0. [para(180(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #108 (F,wt=10): 203 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),183(a,1,2))]. given #109 (T,wt=10): 226 x v ((x ^ y)' v z) = 1. [para(93(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #110 (T,wt=10): 227 x v (y v (x ^ z)') = 1. [para(107(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #111 (A,wt=23): 46 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 #112 (F,wt=10): 240 c1 ^ ((c2 v x)' ^ y) = 0. [para(215(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #113 (F,wt=10): 243 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),215(a,1,2,1))]. given #114 (T,wt=10): 244 c1 ^ (x ^ (c2 v y)') = 0. [para(215(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #115 (T,wt=10): 245 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),217(a,1,2,1))]. given #116 (A,wt=27): 47 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ v) = x ^ ((y v (z ^ (x v u))) ^ v). [para(12(a,1),5(a,1,1)),rewrite(5(5)),flip(a)]. given #117 (F,wt=10): 246 c1 ^ ((x v c2)' ^ y) = 0. [para(217(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #118 (F,wt=10): 249 c1 ^ (x ^ (y v c2)') = 0. [para(217(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #119 (T,wt=10): 265 x v (y ^ (x ^ z))' = 1. [para(19(a,1),220(a,1,2,1))]. given #120 (T,wt=10): 266 x v ((y ^ x)' v z) = 1. [para(261(a,1),3(a,1,1)),rewrite(92(2)),flip(a)]. given #121 (A,wt=31): 48 x ^ (y ^ (z v ((x ^ (y ^ u)) v (u ^ (z v v))))) = x ^ (y ^ (z v (u ^ ((x ^ y) v v)))). [para(12(a,1),5(a,1)),rewrite(5(6),5(8)),flip(a)]. given #122 (F,wt=10): 268 x v (y ^ (z ^ x))' = 1. [para(5(a,1),261(a,1,2,1))]. given #123 (F,wt=10): 273 x v (y v (z ^ x)') = 1. [para(261(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #124 (T,wt=10): 277 (c2 ^ x) v (c1 ^ x)' = 1. [para(57(a,1),261(a,1,2,1))]. given #125 (T,wt=10): 282 c2 v (x v (c1' v y)) = 1. [para(278(a,1),3(a,1,1)),rewrite(92(2),3(6)),flip(a)]. given #126 (A,wt=29): 49 x ^ (y v ((x ^ (z ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))). [para(5(a,1),12(a,1,2,2,2)),rewrite(5(11))]. given #127 (F,wt=10): 283 c2 v (x v (y v c1')) = 1. [para(3(a,1),278(a,1,2))]. given #128 (F,wt=10): 314 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #129 (T,wt=10): 321 c2 v ((x ^ c1)' v y) = 1. [para(302(a,1),3(a,1,1)),rewrite(92(2)),flip(a)]. given #130 (T,wt=10): 323 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),302(a,1,2,1))]. given #131 (A,wt=16): 52 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)]. given #132 (F,wt=10): 326 c2 v (x v (y ^ c1)') = 1. [para(302(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #133 (F,wt=10): 327 c2 v ((c1 ^ x)' v y) = 1. [para(322(a,1),3(a,1,1)),rewrite(92(2)),flip(a)]. given #134 (T,wt=10): 330 c2 v (x v (c1 ^ y)') = 1. [para(322(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #135 (T,wt=10): 331 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),322(a,1,2,1))]. given #136 (A,wt=49): 55 x ^ (y v ((x ^ (z v (u ^ (x v v)))) v ((z v ((x ^ u) v (u ^ (z v v)))) ^ (y v w)))) = x ^ (y v ((z v ((x ^ u) v (u ^ (z v v)))) ^ (x v w))). [para(12(a,1),12(a,1,2,2,1))]. given #137 (F,wt=10): 337 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),34(a,1,2,2,1))]. given #138 (F,wt=10): 344 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),57(a,1,2)),rewrite(4(3),95(3)),flip(a)]. given #139 (T,wt=10): 371 c2 != 1 | c1 != 0 | c2' = c1. [para(125(a,1),36(a,1)),rewrite(4(6),13(6))]. given #140 (T,wt=10): 392 x' v (y v (x v z)) = 1. [para(390(a,1),3(a,1,1)),rewrite(92(2),3(4)),flip(a)]. given #141 (A,wt=31): 56 x ^ (y v (z ^ (x v ((z ^ u) v (u ^ (y v v)))))) = x ^ (y v (z ^ (x v (u ^ (z v v))))). [para(12(a,1),12(a,1,2,2,2)),rewrite(12(8)),flip(a)]. given #142 (F,wt=8): 2070 c1' v (x v c2) = 1. [para(125(a,1),392(a,1,2,2))]. given #143 (F,wt=10): 393 x' v (y v (z v x)) = 1. [para(3(a,1),390(a,1,2))]. given #144 (T,wt=10): 399 x' ^ (y ^ (x ^ z)) = 0. [para(391(a,1),5(a,1,1)),rewrite(95(2),5(4)),flip(a)]. given #145 (T,wt=10): 400 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),391(a,1,2))]. given #146 (A,wt=14): 66 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(41),rewrite(61(4))]. given #147 (F,wt=7): 2337 c1 != 1 | c1' = 0. [para(179(a,1),66(b,1)),rewrite(179(12)),flip(a),xx(b)]. given #148 (F,wt=7): 2339 x' != 1 | 0 = x. [para(391(a,1),66(b,1)),rewrite(367(8),391(9)),flip(a),flip(c),xx(b)]. given #149 (T,wt=8): 2296 c2' ^ (x ^ c1) = 0. [para(13(a,1),400(a,1,2,2))]. given #150 (T,wt=7): 2354 c2' != 1 | c2 = 0. [para(2296(a,1),66(b,1)),rewrite(367(10),2296(13)),flip(a),xx(b)]. given #151 (A,wt=17): 71 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_rewrite(65),rewrite(67(7))]. given #152 (F,wt=10): 2341 (c1 ^ (c1' v c2'))' != 1. [ur(2339,b,146,a(flip))]. given #153 (F,wt=10): 411 (x ^ c2) v (x ^ c1)' = 1. [para(104(a,1),261(a,1,2,1))]. given #154 (T,wt=10): 412 x ^ (c1 ^ (x ^ c2)') = 0. [para(104(a,1),391(a,1,2)),rewrite(4(6),5(6))]. given #155 (T,wt=10): 498 (x v c1) ^ (x v c2)' = 0. [para(130(a,1),173(a,1,2,1))]. given #156 (A,wt=14): 72 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(40),rewrite(67(2))]. given #157 (F,wt=7): 2466 c2 != 0 | c2' = 1. [para(272(a,1),72(a,1)),rewrite(272(12)),flip(b),xx(a)]. given #158 (F,wt=7): 2468 x' != 0 | 1 = x. [para(390(a,1),72(a,1)),rewrite(367(8),390(9)),flip(b),flip(c),xx(a)]. given #159 (T,wt=7): 2470 c1' != 0 | c1 = 1. [para(2070(a,1),72(a,1)),rewrite(367(10),2070(13)),flip(b),xx(a)]. given #160 (T,wt=10): 502 x v (c2 v (x v c1)') = 1. [para(130(a,1),390(a,1,2)),rewrite(2(6),3(6))]. given #161 (A,wt=11): 78 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #162 (F,wt=10): 623 (x v c1) ^ (c2 v x)' = 0. [para(494(a,1),173(a,1,2,1))]. given #163 (F,wt=10): 625 c2 v (x v (x v c1)') = 1. [para(494(a,1),390(a,1,2)),rewrite(2(6),3(6))]. given #164 (T,wt=10): 1601 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),277(a,1,1))]. given #165 (T,wt=10): 1602 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),277(a,1,2,1))]. given #166 (A,wt=20): 80 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #167 (F,wt=10): 1603 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),277(a,1,2,1))]. given #168 (F,wt=10): 1609 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),277(a,1,2,1))]. given #169 (T,wt=10): 2023 c1 ^ (x ^ (x ^ c2)') = 0. [para(337(a,1),57(a,1,2)),rewrite(4(3),95(3)),flip(a)]. given #170 (T,wt=10): 2042 x ^ (c1 ^ (c2 ^ x)') = 0. [para(344(a,1),19(a,1)),flip(a)]. given #171 (A,wt=27): 81 x ^ (y v ((x ^ z) v (z ^ (u v (y v v))))) = x ^ (y v (z ^ (x v (u v v)))). [para(17(a,1),12(a,1,2,2,2,2))]. given #172 (F,wt=10): 2044 c1 ^ (c2 ^ (c1 v x))' = 0. [para(344(a,1),22(a,1)),flip(a)]. given #173 (F,wt=10): 2074 c1' v (x v (c2 v y)) = 1. [para(129(a,1),392(a,1,2,2))]. given #174 (T,wt=10): 2076 c1' v (x v (y v c2)) = 1. [para(132(a,1),392(a,1,2,2))]. given #175 (T,wt=10): 2245 (x ^ y)' v (z v x) = 1. [para(7(a,1),393(a,1,2,2))]. given #176 (A,wt=23): 82 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(17(a,1),12(a,1,2))]. given #177 (F,wt=10): 2249 (x ^ y)' v (z v y) = 1. [para(26(a,1),393(a,1,2,2))]. given #178 (F,wt=10): 2253 (x ^ c1)' v (y v c2) = 1. [para(299(a,1),393(a,1,2,2))]. given #179 (T,wt=10): 2254 (c1 ^ x)' v (y v c2) = 1. [para(305(a,1),393(a,1,2,2))]. given #180 (T,wt=10): 2277 c2' ^ (x ^ (y ^ c1)) = 0. [para(58(a,1),399(a,1,2,2))]. given #181 (A,wt=11): 83 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [back_rewrite(60),rewrite(77(8)),flip(a)]. given #182 (F,wt=10): 2292 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),400(a,1,2,2))]. given #183 (F,wt=10): 2298 (x v y)' ^ (z ^ y) = 0. [para(20(a,1),400(a,1,2,2))]. given #184 (T,wt=10): 2303 (c2 v x)' ^ (y ^ c1) = 0. [para(207(a,1),400(a,1,2,2))]. given #185 (T,wt=10): 2304 (x v c2)' ^ (y ^ c1) = 0. [para(212(a,1),400(a,1,2,2))]. given #186 (A,wt=13): 84 x ^ (y v ((x v z) ^ (x v u))) = x. [back_rewrite(50),rewrite(77(6)),flip(a)]. given #187 (F,wt=10): 2335 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),66(b,1)),rewrite(13(11)),flip(a)]. given #188 (F,wt=10): 2342 c2' ^ (x ^ (c1 ^ y)) = 0. [para(2296(a,1),5(a,1,1)),rewrite(95(2),5(6)),flip(a)]. given #189 (T,wt=10): 2446 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),498(a,1,1))]. given #190 (T,wt=10): 2467 c2 != 1 | c2 != 0 | c2' = c2. [para(299(a,1),72(a,1)),rewrite(299(12)),flip(b)]. given #191 (A,wt=17): 87 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(35(a,1),12(a,1,2,2,2,2)),rewrite(70(5),35(6))]. given #192 (F,wt=10): 2471 x v (c2 v (c1 v x)') = 1. [para(2(a,1),502(a,1,2,2,1))]. given #193 (F,wt=10): 2520 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),623(a,1,1))]. given #194 (T,wt=10): 2521 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),623(a,1,2,1)),rewrite(2(4))]. given #195 (T,wt=10): 2525 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),623(a,1,2,1)),rewrite(2(4))]. given #196 (A,wt=21): 88 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))). [back_rewrite(53),rewrite(85(5))]. given #197 (F,wt=10): 2542 c2 v (x v (c1 v x)') = 1. [para(2(a,1),625(a,1,2,2,1))]. given #198 (F,wt=10): 2547 c2 v (c1 v (c2 ^ x))' = 1. [para(625(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #199 (T,wt=10): 2642 c1' v (c2 ^ (c1 v x)) = 1. [para(1603(a,1),2(a,1)),flip(a)]. given #200 (T,wt=10): 2658 c1' v (c2 ^ (x v c1)) = 1. [para(1609(a,1),2(a,1)),flip(a)]. given #201 (A,wt=19): 89 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_rewrite(73),rewrite(87(9))]. given #202 (F,wt=10): 2860 c1 ^ (c2 ^ (x v c1))' = 0. [para(2(a,1),2044(a,1,2,1,2))]. given #203 (F,wt=10): 3592 c2' ^ (c1 v (c2 ^ x)) = 0. [para(2521(a,1),4(a,1)),flip(a)]. given #204 (T,wt=10): 3610 c2' ^ (c1 v (x ^ c2)) = 0. [para(2525(a,1),4(a,1)),flip(a)]. given #205 (T,wt=10): 3836 c2 v (c1 v (x ^ c2))' = 1. [para(4(a,1),2547(a,1,2,1,2))]. given #206 (A,wt=11): 98 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #207 (F,wt=11): 113 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #208 (F,wt=11): 118 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #209 (T,wt=11): 119 x v ((y ^ x) v z) = x v z. [para(26(a,1),3(a,1,1)),flip(a)]. given #210 (T,wt=11): 126 x v (y v (z ^ x)) = y v x. [para(26(a,1),17(a,1,2)),flip(a)]. given #211 (A,wt=20): 101 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(19(a,1),10(b,1))]. given #212 (F,wt=11): 144 (x v c1) ^ (x v c2) = x v c1. [para(125(a,1),21(a,1,2,2))]. given #213 (F,wt=11): 181 c1 v c2' != 1 | c2' = c1'. [para(179(a,1),10(b,1)),flip(c),xx(b)]. given #214 (T,wt=11): 213 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(57(a,1),26(a,1,2)),rewrite(2(5))]. given #215 (T,wt=11): 214 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),57(a,1,2)),rewrite(57(4)),flip(a)]. given #216 (A,wt=29): 102 x ^ (y v ((z ^ (x ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))). [para(19(a,1),12(a,1,2,2,1)),rewrite(5(5),5(11))]. given #217 (F,wt=11): 234 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(207(a,1),19(a,1,2)),flip(a)]. given #218 (F,wt=11): 236 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(212(a,1),5(a,1,1)),flip(a)]. given #219 (T,wt=11): 239 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(212(a,1),19(a,1,2)),flip(a)]. given #220 (T,wt=11): 280 c2 ^ c1' != 0 | c2' = c1'. [para(272(a,1),10(a,1)),xx(a)]. given #221 (A,wt=27): 103 x ^ (y ^ (z v ((x ^ u) v (u ^ (z v v))))) = y ^ (x ^ (z v (u ^ (x v v)))). [para(12(a,1),19(a,1,2)),flip(a)]. given #222 (F,wt=11): 301 c2 v ((x ^ c1) v y) = c2 v y. [para(58(a,1),24(a,1,2,1))]. given #223 (F,wt=11): 304 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(58(a,1),27(a,1,2))]. given #224 (T,wt=11): 308 c2 v (x v (y ^ c1)) = x v c2. [para(299(a,1),17(a,1,2)),flip(a)]. given #225 (T,wt=11): 309 c2 v ((c1 ^ x) v y) = c2 v y. [para(305(a,1),3(a,1,1)),flip(a)]. given #226 (A,wt=13): 105 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [back_rewrite(96),rewrite(98(7))]. given #227 (F,wt=11): 312 c2 v (x v (c1 ^ y)) = x v c2. [para(305(a,1),17(a,1,2)),flip(a)]. given #228 (F,wt=11): 335 (x v y) ^ (z ^ x) = z ^ x. [para(63(a,1),22(a,2)),rewrite(334(4))]. given #229 (T,wt=11): 336 (x ^ y) v (y ^ x) = x ^ y. [para(63(a,1),27(a,1,2))]. given #230 (T,wt=10): 5330 (x ^ y) v (y ^ x)' = 1. [para(336(a,1),390(a,1,2)),rewrite(2(4))]. given #231 (A,wt=13): 114 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #232 (F,wt=11): 350 (x v y) ^ (y v x) = x v y. [para(69(a,1),21(a,1,2))]. given #233 (F,wt=10): 5458 (x v y) ^ (y v x)' = 0. [para(350(a,1),391(a,1,2)),rewrite(4(4))]. given #234 (T,wt=11): 351 (x ^ y) v (z v x) = z v x. [para(69(a,1),24(a,2)),rewrite(348(4))]. given #235 (T,wt=11): 353 x ^ (y v (z v (x v u))) = x. [para(3(a,1),77(a,1,2))]. given #236 (A,wt=14): 115 x v y != 1 | 0 != y | y' = x v y. [para(20(a,1),10(b,1)),rewrite(69(2)),flip(b)]. given #237 (F,wt=11): 359 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),99(a,1,2))]. given #238 (F,wt=11): 410 (x ^ c1) v (x ^ c2) = x ^ c2. [para(104(a,1),26(a,1,2)),rewrite(2(5))]. given #239 (T,wt=11): 420 x v y != 0 | (x v y)' = 1. [para(32(a,1),37(b,1)),rewrite(106(2),106(2)),xx(a)]. given #240 (T,wt=11): 424 x v y != 1 | (x v y)' = 0. [para(35(a,1),37(a,1,2)),rewrite(4(6),95(6)),xx(b)]. given #241 (A,wt=13): 116 x ^ (y v ((z v x) ^ (x v u))) = x. [para(20(a,1),12(a,1,2,2,1)),rewrite(77(6)),flip(a)]. given #242 (F,wt=7): 5665 c2 != 1 | c2' = 0. [para(125(a,1),424(a,1)),rewrite(125(6))]. given #243 (F,wt=11): 461 x ^ (y v (z v (u v x))) = x. [para(3(a,1),112(a,1,2,2))]. given #244 (T,wt=11): 475 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),121(a,1,2,2))]. given #245 (T,wt=11): 536 (c1 v x) ^ (x v c2) = c1 v x. [para(132(a,1),21(a,1,2))]. given #246 (A,wt=13): 117 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #247 (F,wt=11): 539 c1 ^ (x v (y v (c2 v z))) = c1. [para(3(a,1),233(a,1,2))]. given #248 (F,wt=11): 545 c1 ^ (x v (y v (z v c2))) = c1. [para(3(a,1),235(a,1,2,2))]. given #249 (T,wt=11): 552 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(5(a,1),306(a,1,2,2))]. given #250 (T,wt=11): 564 x ^ y != 0 | (x ^ y)' = 1. [para(32(a,1),39(b,1,2)),rewrite(2(3),92(3)),xx(a)]. given #251 (A,wt=13): 120 x v (y v (z ^ (x v y))) = x v y. [para(26(a,1),3(a,1)),flip(a)]. given #252 (F,wt=7): 6009 c1 != 0 | c1' = 1. [para(13(a,1),564(a,1)),rewrite(13(6))]. given #253 (F,wt=11): 566 x ^ y != 1 | (x ^ y)' = 0. [para(35(a,1),39(a,1)),rewrite(109(5),109(5)),xx(b)]. given #254 (T,wt=11): 614 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(5(a,1),313(a,1,2))]. given #255 (T,wt=11): 622 (x v c1) ^ (c2 v x) = x v c1. [para(494(a,1),20(a,1,2))]. given #256 (A,wt=14): 122 1 != x | y ^ x != 0 | x' = y ^ x. [para(26(a,1),10(a,1)),rewrite(63(4)),flip(a)]. given #257 (F,wt=11): 2928 (x ^ y)' != 0 | x ^ y = 1. [para(2245(a,1),72(a,1)),rewrite(367(10),2245(12)),flip(b),xx(a)]. given #258 (F,wt=11): 3231 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),83(a,1,2,2,2))]. given #259 (T,wt=11): 3232 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(2(a,1),83(a,1,2))]. given #260 (T,wt=11): 3282 (x v y)' != 1 | x v y = 0. [para(2292(a,1),66(b,1)),rewrite(367(10),2292(12)),flip(a),xx(b)]. given #261 (A,wt=19): 123 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)). [para(26(a,1),12(a,1,2,2,2,2)),rewrite(90(5)),flip(a)]. given #262 (F,wt=11): 4087 (x v y) ^ (z ^ y) = z ^ y. [para(63(a,1),113(a,2)),rewrite(334(4))]. given #263 (F,wt=11): 4199 (x ^ y) v (z v y) = z v y. [para(69(a,1),119(a,2)),rewrite(348(4))]. given #264 (T,wt=11): 4451 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),213(a,1,1))]. given #265 (T,wt=11): 4452 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),213(a,1,2))]. given #266 (A,wt=33): 124 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u)))))) = x v ((y ^ z) v (z ^ (x v u))). [para(12(a,1),26(a,1,2)),rewrite(2(10),17(10),17(9),2(8))]. given #267 (F,wt=11): 4533 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(63(a,1),214(a,2)),rewrite(334(7))]. given #268 (F,wt=11): 4781 (x v c2) ^ (y ^ c1) = y ^ c1. [para(63(a,1),236(a,2)),rewrite(334(7))]. given #269 (T,wt=11): 5011 (x ^ c1) v (y v c2) = y v c2. [para(69(a,1),301(a,2)),rewrite(348(7))]. given #270 (T,wt=11): 5121 (c1 ^ x) v (y v c2) = y v c2. [para(69(a,1),309(a,2)),rewrite(348(7))]. given #271 (A,wt=13): 127 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(19(a,1),26(a,1,2))]. given #272 (F,wt=11): 5661 x v y != 0 | (y v x)' = 1. [para(2(a,1),420(a,1))]. given #273 (F,wt=11): 5663 x v y != 1 | (y v x)' = 0. [para(2(a,1),424(a,1))]. given #274 (T,wt=11): 5855 (c1 v x) ^ (c2 v x) = c1 v x. [para(2(a,1),536(a,1,2))]. given #275 (T,wt=11): 5856 (x v c2) ^ (c1 v x) = c1 v x. [para(536(a,1),4(a,1)),flip(a)]. given #276 (A,wt=21): 131 x ^ (c1 v ((x ^ y) v (y ^ c2))) = x ^ (c1 v (y ^ (x v c2))). [para(125(a,1),12(a,1,2,2,2,2))]. given #277 (F,wt=11): 6008 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),564(a,1))]. given #278 (F,wt=11): 6074 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),566(a,1))]. given #279 (T,wt=11): 6104 (c2 v x) ^ (x v c1) = x v c1. [para(622(a,1),4(a,1)),flip(a)]. given #280 (T,wt=11): 6184 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),2928(a,1,1))]. given #281 (A,wt=13): 133 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #282 (F,wt=11): 6186 (x v y)' != 0 | x v y = 1. [para(21(a,1),2928(a,1,1)),rewrite(21(8))]. given #283 (F,wt=7): 7316 c2' != 0 | c2 = 1. [para(125(a,1),6186(a,1,1)),rewrite(125(7))]. given #284 (T,wt=11): 6191 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),3231(a,1,2))]. given #285 (T,wt=11): 6256 (x v y)' != 1 | y v x = 0. [para(2(a,1),3282(a,1,1))]. given #286 (A,wt=13): 134 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite(3(3))]. given #287 (F,wt=11): 6258 (x ^ y)' != 1 | x ^ y = 0. [para(27(a,1),3282(a,1,1)),rewrite(27(8))]. given #288 (F,wt=7): 7434 c1' != 1 | c1 = 0. [para(13(a,1),6258(a,1,1)),rewrite(13(7))]. given #289 (T,wt=11): 6559 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(4452(a,1),2(a,1)),flip(a)]. given #290 (T,wt=11): 6613 x v (c2 ^ (x v c1)) = x v c1. [para(207(a,1),124(a,1,2,2,2,2,2)),rewrite(4(3),13(3),24(10),4461(6),4(8),13(8),7(10))]. given #291 (A,wt=19): 135 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),21(a,1,1)),rewrite(3(5),3(8))]. given #292 (F,wt=11): 7265 (x v y)' != 0 | y v x = 1. [para(350(a,1),6184(a,1,1)),rewrite(350(7))]. given #293 (F,wt=11): 7355 (x ^ y)' != 1 | y ^ x = 0. [para(336(a,1),6256(a,1,1)),rewrite(336(7))]. given #294 (T,wt=11): 7491 x v (c2 ^ (c1 v x)) = x v c1. [para(2(a,1),6613(a,1,2,2))]. given #295 (T,wt=11): 7497 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(6613(a,1),12(a,1,2,2)),rewrite(2(6),69(7),105(13))]. given #296 (A,wt=17): 136 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #297 (F,wt=11): 7504 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(6613(a,1),42(a,1,2,2)),rewrite(2(5),67(6),7497(5),7(7)),flip(a)]. given #298 (F,wt=12): 147 x v (y v ((x v y)' v z)) = 1. [para(93(a,1),3(a,1)),flip(a)]. given #299 (T,wt=12): 151 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(97(a,1),5(a,1)),flip(a)]. given #300 (T,wt=12): 155 x v (y v (z v (x v y)')) = 1. [para(107(a,1),3(a,1)),flip(a)]. given #301 (A,wt=19): 139 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(21(a,1),12(a,1,2,2,2)),rewrite(2(4),26(4),67(2)),flip(a)]. given #302 (F,wt=12): 168 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(110(a,1),5(a,1)),flip(a)]. given #303 (F,wt=12): 174 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),160(a,1,2,1))]. given #304 (T,wt=12): 175 x ^ (y ^ ((x ^ y) v z)') = 0. [para(160(a,1),5(a,1)),flip(a)]. given #305 (T,wt=12): 195 x ^ (y ^ (z v (x ^ y))') = 0. [para(173(a,1),5(a,1)),flip(a)]. given #306 (A,wt=19): 140 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(17(a,1),21(a,1,1)),rewrite(3(4))]. given #307 (F,wt=12): 198 (x v y) ^ (x v (z v y))' = 0. [para(17(a,1),173(a,1,2,1))]. given #308 (F,wt=12): 228 ((x ^ y) v z) ^ (x v z)' = 0. [para(24(a,1),173(a,1,2,1))]. given #309 (T,wt=12): 260 x v (y v ((x v y) ^ z)') = 1. [para(220(a,1),3(a,1)),flip(a)]. given #310 (T,wt=12): 262 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),220(a,1,2,1))]. given #311 (A,wt=15): 141 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #312 (F,wt=12): 267 x v (y v (z ^ (x v y))') = 1. [para(261(a,1),3(a,1)),flip(a)]. given #313 (F,wt=12): 274 (x ^ y) v (x ^ (z ^ y))' = 1. [para(19(a,1),261(a,1,2,1))]. given #314 (T,wt=12): 275 ((x v y) ^ z) v (x ^ z)' = 1. [para(22(a,1),261(a,1,2,1))]. given #315 (T,wt=12): 318 x v (y v (z v (x v z)')) = 1. [para(31(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #316 (A,wt=17): 142 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #317 (F,wt=12): 320 x v (y v ((x ^ z) v y)') = 1. [para(31(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #318 (F,wt=12): 341 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(34(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #319 (T,wt=12): 343 x ^ (y ^ ((x v z) ^ y)') = 0. [para(34(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #320 (T,wt=12): 396 x v ((x v y)' v (z v y)) = 1. [para(17(a,1),390(a,1,2)),rewrite(17(5))]. given #321 (A,wt=22): 145 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [back_rewrite(137),rewrite(143(4))]. given #322 (F,wt=12): 404 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(19(a,1),391(a,1,2)),rewrite(19(5))]. given #323 (F,wt=12): 705 x v (y v (z v (x' v u))) = 1. [para(3(a,1),150(a,1,2))]. given #324 (T,wt=12): 708 x v (y v ((x ^ z)' v u)) = 1. [para(150(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #325 (T,wt=12): 716 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),154(a,1,2))]. given #326 (A,wt=15): 148 x ^ (x' v y) != 0 | x' v y = x'. [para(93(a,1),10(a,1)),flip(c),xx(a)]. given #327 (F,wt=12): 719 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(154(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #328 (F,wt=12): 787 x v (y v (z v (u v x'))) = 1. [para(3(a,1),156(a,1,2,2))]. given #329 (T,wt=12): 790 x v (y v (z v (x ^ u)')) = 1. [para(156(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #330 (T,wt=12): 801 x ^ ((y v (x v z))' ^ u) = 0. [para(17(a,1),167(a,1,2,1,1))]. given #331 (A,wt=18): 149 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z). [para(93(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)]. given #332 (F,wt=12): 807 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),169(a,1,2,2))]. given #333 (F,wt=12): 810 x ^ (y ^ (z ^ (x v u)')) = 0. [para(169(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #334 (T,wt=12): 820 x ^ (y ^ (z v (x v u))') = 0. [para(17(a,1),172(a,1,2,2,1))]. given #335 (T,wt=12): 934 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),178(a,1,2,1))]. given #336 (A,wt=15): 152 x v (x' ^ y) != 1 | x' ^ y = x'. [para(97(a,1),10(b,1)),flip(c),xx(b)]. given #337 (F,wt=12): 943 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),193(a,1,2,1,2))]. given #338 (F,wt=12): 944 x ^ ((y v (z v x))' ^ u) = 0. [para(193(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #339 (T,wt=12): 949 x ^ (y ^ (z v (u v x))') = 0. [para(193(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #340 (T,wt=12): 956 (x v c1) ^ (y v (c2 v x))' = 0. [para(494(a,1),193(a,1,2,1,2))]. given #341 (A,wt=25): 153 x ^ (y v (x' ^ (z ^ (y v u)))) = x ^ (y v (x' ^ (z ^ (x v u)))). [para(97(a,1),12(a,1,2,2,1)),rewrite(5(5),85(6),5(10))]. given #342 (F,wt=12): 963 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(194(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #343 (F,wt=12): 969 (x v c1) ^ ((c2 v x)' ^ y) = 0. [para(494(a,1),194(a,1,2,1,1))]. given #344 (T,wt=12): 972 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),199(a,1,2))]. given #345 (T,wt=12): 982 (x v c1) ^ (y ^ (c2 v x)') = 0. [para(494(a,1),199(a,1,2,2,1))]. given #346 (A,wt=15): 157 x ^ (y v x') != 0 | y v x' = x'. [para(107(a,1),10(a,1)),flip(c),xx(a)]. given #347 (F,wt=12): 1052 c1 ^ (x ^ (y ^ (c2' ^ z))) = 0. [para(5(a,1),202(a,1,2))]. given #348 (F,wt=12): 1061 c1 ^ (x ^ (y ^ (z ^ c2'))) = 0. [para(5(a,1),203(a,1,2,2))]. given #349 (T,wt=12): 1074 x v ((y ^ (x ^ z))' v u) = 1. [para(19(a,1),226(a,1,2,1,1))]. given #350 (T,wt=12): 1084 x v (y v (z ^ (x ^ u))') = 1. [para(19(a,1),227(a,1,2,2,1))]. given #351 (A,wt=18): 158 x ^ (y v (z ^ (x v (u v y')))) = x ^ (y v z). [para(107(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)]. given #352 (F,wt=12): 1180 c1 ^ ((x v (c2 v y))' ^ z) = 0. [para(17(a,1),240(a,1,2,1,1))]. given #353 (F,wt=12): 1181 c1 ^ (x ^ ((c2 v y)' ^ z)) = 0. [para(240(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #354 (T,wt=12): 1188 c1 ^ (x v (y v (c2 v z)))' = 0. [para(3(a,1),243(a,1,2,1))]. given #355 (T,wt=12): 1191 c1 ^ (x ^ (y v (c2 v z))') = 0. [para(243(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #356 (A,wt=17): 159 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(22(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #357 (F,wt=12): 1198 c1 ^ (x ^ (y ^ (c2 v z)')) = 0. [para(5(a,1),244(a,1,2))]. given #358 (F,wt=12): 1208 c1 ^ (x v (y v (z v c2)))' = 0. [para(3(a,1),245(a,1,2,1,2))]. given #359 (T,wt=12): 1209 c1 ^ ((x v (y v c2))' ^ z) = 0. [para(245(a,1),5(a,1,1)),rewrite(95(2)),flip(a)]. given #360 (T,wt=12): 1212 c1 ^ (x ^ (y v (z v c2))') = 0. [para(245(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #361 (A,wt=22): 161 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(22(a,1),10(b,1))]. Low Water (keep): wt=82, part=1.00, limit=81 given #362 (F,wt=12): 1357 c1 ^ (x ^ ((y v c2)' ^ z)) = 0. [para(246(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #363 (F,wt=12): 1365 c1 ^ (x ^ (y ^ (z v c2)')) = 0. [para(5(a,1),249(a,1,2))]. given #364 (T,wt=12): 1378 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),265(a,1,2,1))]. given #365 (T,wt=12): 1389 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),266(a,1,2,1,1))]. given #366 (A,wt=31): 162 x ^ (y v ((x ^ z) v ((x v u) ^ (z ^ (y v v))))) = x ^ (y v ((x v u) ^ (z ^ (x v v)))). [para(22(a,1),12(a,1,2,2,1)),rewrite(5(5),5(12))]. Low Water (keep): wt=70, part=0.98, limit=65 Low Water (keep): wt=67, part=0.98, limit=65 Low Water (keep): wt=65, part=0.98, limit=65 given #367 (F,wt=12): 1393 x v (y v ((z ^ x)' v u)) = 1. [para(266(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #368 (F,wt=12): 1397 (c2 ^ x) v ((c1 ^ x)' v y) = 1. [para(57(a,1),266(a,1,2,1,1))]. given #369 (T,wt=12): 1399 (x ^ c2) v ((x ^ c1)' v y) = 1. [para(104(a,1),266(a,1,2,1,1))]. given #370 (T,wt=12): 1552 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),268(a,1,2,1,2))]. Low Water (keep): wt=59, part=0.97, limit=59 given #371 (A,wt=27): 163 x ^ (y v (((x v z) ^ u) v (u ^ (y v v)))) = x ^ (y v (u ^ (x v (z v v)))). [para(12(a,1),22(a,1,2)),rewrite(3(3),22(7)),flip(a)]. given #372 (F,wt=12): 1556 x v (y v (z ^ (u ^ x))') = 1. [para(268(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #373 (F,wt=12): 1561 (c2 ^ x) v (y ^ (c1 ^ x))' = 1. [para(57(a,1),268(a,1,2,1,2))]. given #374 (T,wt=12): 1563 (x ^ c2) v (y ^ (x ^ c1))' = 1. [para(104(a,1),268(a,1,2,1,2))]. given #375 (T,wt=12): 1577 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),273(a,1,2))]. given #376 (A,wt=13): 164 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),22(a,1,2,1))]. given #377 (F,wt=12): 1584 (c2 ^ x) v (y v (c1 ^ x)') = 1. [para(57(a,1),273(a,1,2,2,1))]. Low Water (keep): wt=54, part=0.93, limit=53 given #378 (F,wt=12): 1586 (x ^ c2) v (y v (x ^ c1)') = 1. [para(104(a,1),273(a,1,2,2,1))]. given #379 (T,wt=12): 1612 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(77(a,1),277(a,1,2,1))]. given #380 (T,wt=12): 1615 (c2 ^ (x v (y v c1))) v c1' = 1. [para(112(a,1),277(a,1,2,1))]. given #381 (A,wt=15): 165 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(22(a,1),19(a,1,2)),flip(a)]. given #382 (F,wt=12): 1626 c2 v (x v (y v (c1' v z))) = 1. [para(3(a,1),282(a,1,2))]. given #383 (F,wt=12): 1730 c2 v (x v (y v (z v c1'))) = 1. [para(3(a,1),283(a,1,2,2))]. given #384 (T,wt=12): 1743 x v (y v ((y v x)' v z)) = 1. [para(314(a,1),3(a,1,1)),rewrite(92(2),3(5)),flip(a)]. given #385 (T,wt=12): 1748 x v (y v (z v (z v x)')) = 1. [para(314(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #386 (A,wt=15): 166 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(22(a,1),26(a,1,2)),rewrite(2(4))]. Low Water (keep): wt=51, part=0.92, limit=49 Low Water (keep): wt=49, part=0.92, limit=49 given #387 (F,wt=12): 1750 x v (y v (y v (x ^ z))') = 1. [para(314(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. given #388 (F,wt=12): 1760 c2 v ((x ^ (y ^ c1))' v z) = 1. [para(5(a,1),321(a,1,2,1,1))]. given #389 (T,wt=12): 1763 c2 v (x v ((y ^ c1)' v z)) = 1. [para(321(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #390 (T,wt=12): 1771 c2 v (x ^ (y ^ (z ^ c1)))' = 1. [para(5(a,1),323(a,1,2,1,2))]. given #391 (A,wt=15): 170 x v (y ^ x') != 1 | y ^ x' = x'. [para(110(a,1),10(b,1)),flip(c),xx(b)]. given #392 (F,wt=12): 1774 c2 v (x v (y ^ (z ^ c1))') = 1. [para(323(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #393 (F,wt=12): 1814 c2 v (x v (y v (z ^ c1)')) = 1. [para(3(a,1),326(a,1,2))]. given #394 (T,wt=12): 1828 c2 v (x v ((c1 ^ y)' v z)) = 1. [para(327(a,1),17(a,1,2)),rewrite(106(2)),flip(a)]. given #395 (T,wt=12): 1829 c2 v ((x ^ (c1 ^ y))' v z) = 1. [para(19(a,1),327(a,1,2,1,1))]. given #396 (A,wt=25): 171 x ^ (y v (z ^ (x' ^ (y v u)))) = x ^ (y v (z ^ (x' ^ (x v u)))). [para(110(a,1),12(a,1,2,2,1)),rewrite(5(5),85(6),5(10))]. Low Water (keep): wt=47, part=0.90, limit=47 given #397 (F,wt=12): 1837 c2 v (x v (y v (c1 ^ z)')) = 1. [para(3(a,1),330(a,1,2))]. given #398 (F,wt=12): 1840 c2 v (x v (y ^ (c1 ^ z))') = 1. [para(19(a,1),330(a,1,2,2,1))]. given #399 (T,wt=12): 1850 c2 v (x ^ (y ^ (c1 ^ z)))' = 1. [para(5(a,1),331(a,1,2,1))]. given #400 (T,wt=12): 2015 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(337(a,1),5(a,1,1)),rewrite(95(2),5(5)),flip(a)]. Low Water (keep): wt=46, part=0.88, limit=43 given #401 (A,wt=15): 176 x v (x v y)' != 1 | (x v y)' = x'. [para(160(a,1),10(b,1)),flip(c),xx(b)]. given #402 (F,wt=12): 2020 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(337(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. given #403 (F,wt=12): 2022 x ^ (y ^ (y ^ (x v z))') = 0. [para(337(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. given #404 (T,wt=12): 2037 c1 ^ (x ^ ((c2 ^ x)' ^ y)) = 0. [para(344(a,1),5(a,1,1)),rewrite(95(2),5(7)),flip(a)]. given #405 (T,wt=12): 2041 c1 ^ (x ^ (y ^ (c2 ^ y)')) = 0. [para(344(a,1),19(a,1,2)),rewrite(109(2)),flip(a)]. Low Water (keep): wt=41, part=0.87, limit=41 given #406 (A,wt=25): 177 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))). [para(160(a,1),12(a,1,2,2,1)),rewrite(85(6))]. given #407 (F,wt=12): 2067 x' v (y v (z v (x v u))) = 1. [para(3(a,1),392(a,1,2))]. Low Water (keep): wt=39, part=0.85, limit=39 given #408 (F,wt=12): 2244 x' v (y v (z v (u v x))) = 1. [para(3(a,1),393(a,1,2,2))]. given #409 (T,wt=12): 2255 (x ^ (y ^ z))' v (u v y) = 1. [para(99(a,1),393(a,1,2,2))]. given #410 (T,wt=12): 2259 (x ^ (y ^ z))' v (u v z) = 1. [para(121(a,1),393(a,1,2,2))]. given #411 (A,wt=21): 182 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))). [para(179(a,1),12(a,1,2,2,1)),rewrite(85(7)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 4.10 (+ 0.06) seconds. % Length of proof is 46. % Level of proof is 11. % Maximum clause weight is 23. % Given clauses 411. 1 (all x all y (x ^ y = x -> x' v y' = x')) # 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 = c1. [deny(1)]. 14 c1' != c1' v c2'. [deny(1)]. 15 c1' v c2' != c1'. [copy(14),flip(a)]. 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 30 x v (x' v y) = 1 v y. [para(8(a,1),3(a,1,1)),flip(a)]. 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. 33 x ^ (x' ^ y) = 0 ^ y. [para(9(a,1),5(a,1,1)),flip(a)]. 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. 57 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. 74 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. 85 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. 92 1 v x = 1. [para(74(a,1),6(a,1))]. 93 x v (x' v y) = 1. [back_rewrite(30),rewrite(92(5))]. 95 0 ^ x = 0. [para(85(a,1),6(a,1,2))]. 97 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(95(5))]. 106 x v 1 = 1. [para(92(a,1),2(a,1)),flip(a)]. 109 x ^ 0 = 0. [para(95(a,1),4(a,1)),flip(a)]. 125 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. 146 c1 ^ (c1' v c2') != 0. [ur(10,a,93,a,c,15,a(flip))]. 160 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(109(2)),flip(a)]. 179 c1 ^ c2' = 0. [para(125(a,1),160(a,1,2,1))]. 182 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))). [para(179(a,1),12(a,1,2,2,1)),rewrite(85(7)),flip(a)]. 213 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(57(a,1),26(a,1,2)),rewrite(2(5))]. 220 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(106(2)),flip(a)]. 261 x v (y ^ x)' = 1. [para(4(a,1),220(a,1,2,1))]. 277 (c2 ^ x) v (c1 ^ x)' = 1. [para(57(a,1),261(a,1,2,1))]. 1603 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),277(a,1,2,1))]. 2642 c1' v (c2 ^ (c1 v x)) = 1. [para(1603(a,1),2(a,1)),flip(a)]. 4453 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),213(a,1,1))]. 14165 c1 ^ (c1' v c2') = 0. [para(2642(a,1),182(a,2,2,2,2)),rewrite(4453(11),19(10),97(10),2(5),85(5),9(4),4(8),74(8)),flip(a)]. 14166 $F. [resolve(14165,a,146,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=411. Generated=121810. Kept=14162. proofs=1. Usable=409. Sos=13187. Demods=9650. Limbo=106, Disabled=471. Hints=0. Weight_deleted=40. Literals_deleted=0. Forward_subsumed=107150. Back_subsumed=73. Sos_limit_deleted=458. Sos_displaced=0. Sos_removed=0. New_demodulators=9914 (6 lex), Back_demodulated=384. Back_unit_deleted=0. Demod_attempts=2037607. Demod_rewrites=401829. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=210596. Nonunit_bsub_feature_tests=71978. Megabytes=20.65. User_CPU=4.10, System_CPU=0.06, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4110 exit (max_proofs) Wed Nov 22 11:31:27 2006