============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13676 was started by mccune on cleo.thornwood, Mon Jun 19 16:49:46 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H49.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in clauses(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 clauses(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 clauses(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 GOALS ========================= % Each goal formula was negated; the result (to be placed in sos): clauses(negated_goals). c1 ^ c2 = c1. c1 ' != c1 ' v c2 '. end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v y = y v x. [input]. 2 (x v y) v z = x v (y v z). [input]. 3 x ^ y = y ^ x. [input]. 4 (x ^ y) ^ z = x ^ (y ^ z). [input]. 5 x ^ (x v y) = x. [input]. 6 x v (x ^ y) = x. [input]. 7 x v x ' = 1. [input]. 8 x ^ x ' = 0. [input]. 9 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 10 x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [input]. 11 c1 ^ c2 = c1. [clausify]. 12 c1 ' != c1 ' v c2 '. [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). 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; redundancy checks enabled. % Operation v is associative-commutative; redundancy checks enabled. % Operation ^ is commutative; redundancy checks enabled. % Operation ^ is associative-commutative; redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 13 x v y = y v x. [input]. 14 (x v y) v z = x v (y v z). [input]. 15 x ^ y = y ^ x. [input]. 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. 17 x ^ (x v y) = x. [input]. 18 x v (x ^ y) = x. [input]. 19 x v x ' = 1. [input]. 20 x ^ x ' = 0. [input]. 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 22 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. 23 c1 ^ c2 = c1. [clausify]. 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. end_of_list. clauses(demodulators). 13 x v y = y v x. [input]. % (lex-dep) 14 (x v y) v z = x v (y v z). [input]. 15 x ^ y = y ^ x. [input]. % (lex-dep) 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. 17 x ^ (x v y) = x. [input]. 18 x v (x ^ y) = x. [input]. 19 x v x ' = 1. [input]. 20 x ^ x ' = 0. [input]. 22 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. 23 c1 ^ c2 = c1. [clausify]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 13 x v y = y v x. [input]. given #2 (I,wt=11): 14 (x v y) v z = x v (y v z). [input]. given #3 (I,wt=7): 15 x ^ y = y ^ x. [input]. given #4 (I,wt=11): 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. given #5 (I,wt=7): 17 x ^ (x v y) = x. [input]. given #6 (I,wt=7): 18 x v (x ^ y) = x. [input]. given #7 (I,wt=6): 19 x v x ' = 1. [input]. given #8 (I,wt=6): 20 x ^ x ' = 0. [input]. given #9 (I,wt=14): 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=23): 22 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. given #11 (I,wt=5): 23 c1 ^ c2 = c1. [clausify]. given #12 (I,wt=8): 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. given #13 (F,wt=5): 35 x ^ x = x. [para(18(a,1),17(a,1,2))]. given #14 (T,wt=5): 36 x v x = x. [para(17(a,1),18(a,1,2))]. given #15 (T,wt=5): 39 x ^ 1 = x. [para(19(a,1),17(a,1,2))]. given #16 (A,wt=11): 25 x v (y v z) = y v (x v z). [para(13(a,1),14(a,1,1)),demod(14(2))]. given #17 (F,wt=5): 42 x v 0 = x. [para(20(a,1),18(a,1,2))]. given #18 (F,wt=5): 81 1 ^ x = x. [para(39(a,1),15(a,1)),flip(a)]. given #19 (T,wt=4): 98 1 ' = 0. [hyper(21,a,42,a,b,81,a)]. given #20 (T,wt=5): 92 0 v x = x. [para(42(a,1),13(a,1)),flip(a)]. given #21 (A,wt=11): 26 x ^ (y ^ z) = y ^ (x ^ z). [para(15(a,1),16(a,1,1)),demod(16(2))]. given #22 (F,wt=4): 101 0 ' = 1. [hyper(21,a,92,a,b,39,a)]. given #23 (F,wt=5): 99 1 v x = 1. [para(81(a,1),17(a,1))]. given #24 (T,wt=5): 102 0 ^ x = 0. [para(92(a,1),17(a,1,2))]. given #25 (T,wt=5): 113 x v 1 = 1. [para(99(a,1),13(a,1)),flip(a)]. given #26 (A,wt=7): 27 x ^ (y v x) = x. [para(13(a,1),17(a,1,2))]. given #27 (F,wt=5): 116 x ^ 0 = 0. [para(102(a,1),15(a,1)),flip(a)]. given #28 (F,wt=7): 33 x v (y ^ x) = x. [para(15(a,1),18(a,1,2))]. given #29 (T,wt=5): 132 c1 v c2 = c2. [para(23(a,1),33(a,1,2)),demod(13(3))]. given #30 (T,wt=7): 115 0 != x | x ' = 1. [back_demod(82),demod(113(2)),xx(a)]. given #31 (A,wt=13): 28 (x v y) ^ (x v (y v z)) = x v y. [para(14(a,1),17(a,1,2))]. given #32 (F,wt=7): 118 1 != x | x ' = 0. [back_demod(93),demod(116(4)),xx(b)]. given #33 (F,wt=8): 100 x v (x ' v y) = 1. [back_demod(37),demod(99(5))]. given #34 (T,wt=8): 104 x ^ (x ' ^ y) = 0. [back_demod(40),demod(102(5))]. given #35 (T,wt=8): 114 x v (y v x ') = 1. [back_demod(86),demod(113(5))]. given #36 (A,wt=11): 29 x ^ ((x v y) ^ z) = x ^ z. [para(17(a,1),16(a,1,1)),flip(a)]. given #37 (F,wt=9): 153 c1 ^ (c1 ' v c2 ') != 0. [ur(21,a,100,a,c,24,a(flip))]. given #38 (F,wt=8): 117 x ^ (y ^ x ') = 0. [back_demod(107),demod(116(5))]. given #39 (T,wt=8): 167 x ^ (x v y) ' = 0. [para(20(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #40 (T,wt=6): 186 c1 ^ c2 ' = 0. [para(132(a,1),167(a,1,2,1))]. given #41 (A,wt=13): 30 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(17(a,1),16(a,1)),flip(a)]. given #42 (F,wt=8): 180 x ^ (y v x) ' = 0. [para(13(a,1),167(a,1,2,1))]. given #43 (F,wt=8): 187 c1 ^ (c2 ' ^ x) = 0. [para(186(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #44 (T,wt=8): 190 c1 ^ (x ^ c2 ') = 0. [para(186(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #45 (T,wt=9): 64 c1 ^ (c2 ^ x) = c1 ^ x. [para(23(a,1),16(a,1,1)),flip(a)]. given #46 (A,wt=11): 31 x v ((x ^ y) v z) = x v z. [para(18(a,1),14(a,1,1)),flip(a)]. given #47 (F,wt=7): 214 c1 ^ (c2 v x) = c1. [para(17(a,1),64(a,1,2)),demod(23(3)),flip(a)]. given #48 (F,wt=7): 219 c1 ^ (x v c2) = c1. [para(27(a,1),64(a,1,2)),demod(23(3)),flip(a)]. given #49 (T,wt=8): 222 c1 ^ (c2 v x) ' = 0. [para(167(a,1),64(a,1,2)),demod(15(3),102(3)),flip(a)]. given #50 (T,wt=8): 224 c1 ^ (x v c2) ' = 0. [para(180(a,1),64(a,1,2)),demod(15(3),102(3)),flip(a)]. given #51 (A,wt=13): 32 x v (y v ((x v y) ^ z)) = x v y. [para(18(a,1),14(a,1)),flip(a)]. given #52 (F,wt=8): 227 x v (x ^ y) ' = 1. [para(19(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #53 (F,wt=8): 268 x v (y ^ x) ' = 1. [para(15(a,1),227(a,1,2,1))]. given #54 (T,wt=6): 279 c2 v c1 ' = 1. [para(23(a,1),268(a,1,2,1))]. given #55 (T,wt=8): 285 c2 v (x v c1 ') = 1. [para(214(a,1),268(a,1,2,1)),demod(14(5))]. given #56 (A,wt=13): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(16(a,1),18(a,1,2))]. given #57 (F,wt=8): 286 c2 v (c1 ' v x) = 1. [para(279(a,1),14(a,1,1)),demod(99(2)),flip(a)]. given #58 (F,wt=9): 65 c2 ^ (x ^ c1) = x ^ c1. [para(23(a,1),16(a,2,2)),demod(15(4))]. given #59 (T,wt=7): 306 c2 v (x ^ c1) = c2. [para(65(a,1),18(a,1,2))]. given #60 (T,wt=7): 312 c2 v (c1 ^ x) = c2. [para(15(a,1),306(a,1,2))]. given #61 (A,wt=10): 38 x v (y v (x v y) ') = 1. [para(19(a,1),14(a,1)),flip(a)]. given #62 (F,wt=8): 309 c2 v (x ^ c1) ' = 1. [para(65(a,1),227(a,1,2,1))]. given #63 (F,wt=8): 329 c2 v (c1 ^ x) ' = 1. [para(15(a,1),309(a,1,2,1))]. given #64 (T,wt=9): 68 x ^ (x ^ y) = x ^ y. [para(35(a,1),16(a,1,1)),flip(a)]. given #65 (T,wt=9): 70 x ^ (y ^ x) = y ^ x. [para(35(a,1),16(a,2,2)),demod(15(2))]. given #66 (A,wt=10): 41 x ^ (y ^ (x ^ y) ') = 0. [para(20(a,1),16(a,1)),flip(a)]. given #67 (F,wt=9): 74 x v (x v y) = x v y. [para(36(a,1),14(a,1,1)),flip(a)]. given #68 (F,wt=9): 76 x v (y v x) = y v x. [para(36(a,1),14(a,2,2)),demod(13(2))]. given #69 (T,wt=9): 84 x ^ (y v (x v z)) = x. [para(25(a,1),17(a,1,2))]. given #70 (T,wt=9): 106 x v (y ^ (x ^ z)) = x. [para(26(a,1),18(a,1,2))]. given #71 (A,wt=14): 43 x v y != 1 | y ^ x != 0 | y ' = x. [para(13(a,1),21(a,1))]. given #72 (F,wt=5): 374 x ' ' = x. [para(19(a,1),43(a,1)),demod(15(5),20(5)),xx(a),xx(b)]. given #73 (F,wt=8): 397 x ' v (y v x) = 1. [para(374(a,1),114(a,1,2,2))]. given #74 (T,wt=8): 398 x ' ^ (y ^ x) = 0. [para(374(a,1),117(a,1,2,2))]. given #75 (T,wt=9): 111 c1 ^ (x ^ c2) = x ^ c1. [para(23(a,1),26(a,1,2)),flip(a)]. given #76 (A,wt=20): 44 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y) ' = z. [para(14(a,1),21(a,1))]. given #77 (F,wt=9): 119 x ^ (y v (z v x)) = x. [para(14(a,1),27(a,1,2))]. given #78 (F,wt=9): 128 x v (y ^ (z ^ x)) = x. [para(16(a,1),33(a,1,2))]. given #79 (T,wt=9): 136 c1 v (c2 v x) = c2 v x. [para(132(a,1),14(a,1,1)),flip(a)]. given #80 (T,wt=9): 137 c2 v (x v c1) = x v c2. [para(132(a,1),14(a,2,2)),demod(13(4))]. given #81 (A,wt=14): 45 x v y != 1 | y ^ x != 0 | x ' = y. [para(15(a,1),21(b,1))]. given #82 (F,wt=9): 139 c1 v (x v c2) = x v c2. [para(132(a,1),25(a,1,2)),flip(a)]. given #83 (F,wt=9): 240 c1 ^ (x v (c2 v y)) = c1. [para(25(a,1),214(a,1,2))]. given #84 (T,wt=9): 242 c1 ^ (x v (y v c2)) = c1. [para(14(a,1),219(a,1,2))]. given #85 (T,wt=9): 313 c2 v (x ^ (y ^ c1)) = c2. [para(16(a,1),306(a,1,2))]. given #86 (A,wt=20): 46 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(16(a,1),21(b,1))]. given #87 (F,wt=9): 320 c2 v (x ^ (c1 ^ y)) = c2. [para(26(a,1),312(a,1,2))]. given #88 (F,wt=9): 385 c2 ^ c1 ' != 0 | c2 = c1. [para(279(a,1),43(a,1)),demod(15(7),374(12)),flip(c),xx(a)]. given #89 (T,wt=9): 501 c2 v (x v c1) = c2 v x. [para(137(a,2),13(a,1))]. given #90 (T,wt=9): 524 c1 v c2 ' != 1 | c2 = c1. [para(186(a,1),45(b,1)),demod(13(4),374(12)),xx(b)]. given #91 (A,wt=23): 49 x ^ (y v ((x ^ z) v (z ^ (u v y)))) = x ^ (y v (z ^ (x v u))). [para(13(a,1),22(a,1,2,2,2,2))]. given #92 (F,wt=10): 71 1 != x | 0 != x | x ' = x. [para(35(a,1),21(b,1)),demod(36(1)),flip(a),flip(b)]. given #93 (F,wt=10): 135 c2 != 1 | c1 != 0 | c1 ' = c2. [back_demod(66),demod(132(3))]. given #94 (T,wt=10): 157 x v (y v (x ' v z)) = 1. [para(100(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #95 (T,wt=10): 161 x ^ (y ^ (x ' ^ z)) = 0. [para(104(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #96 (A,wt=23): 50 x ^ (y v ((z ^ (y v u)) v (x ^ z))) = x ^ (y v (z ^ (x v u))). [para(13(a,1),22(a,1,2,2))]. given #97 (F,wt=10): 163 x v (y v (z v x ')) = 1. [para(14(a,1),114(a,1,2))]. given #98 (F,wt=10): 174 x ^ ((x v y) ' ^ z) = 0. [para(104(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #99 (T,wt=10): 176 x ^ (y ^ (z ^ x ')) = 0. [para(16(a,1),117(a,1,2))]. given #100 (T,wt=10): 179 x ^ (y ^ (x v z) ') = 0. [para(117(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #101 (A,wt=29): 51 x ^ (y v (z v ((x ^ u) v (u ^ (y v (z v v)))))) = x ^ (y v (z v (u ^ (x v v)))). [para(14(a,1),22(a,1,2,2,2,2)),demod(14(7),14(12))]. given #102 (F,wt=10): 185 x ^ (y v (x v z)) ' = 0. [para(25(a,1),167(a,1,2,1))]. given #103 (F,wt=10): 200 x ^ (y v (z v x)) ' = 0. [para(14(a,1),180(a,1,2,1))]. given #104 (T,wt=10): 201 x ^ ((y v x) ' ^ z) = 0. [para(180(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #105 (T,wt=10): 206 x ^ (y ^ (z v x) ') = 0. [para(180(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #106 (A,wt=23): 52 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(15(a,1),22(a,1,2,2,1))]. given #107 (F,wt=10): 209 c1 ^ (x ^ (c2 ' ^ y)) = 0. [para(187(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #108 (F,wt=10): 210 c1 ^ (x ^ (y ^ c2 ')) = 0. [para(16(a,1),190(a,1,2))]. given #109 (T,wt=10): 233 x v ((x ^ y) ' v z) = 1. [para(100(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #110 (T,wt=10): 234 x v (y v (x ^ z) ') = 1. [para(114(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #111 (A,wt=23): 53 x ^ (y v ((x ^ z) v ((y v u) ^ z))) = x ^ (y v (z ^ (x v u))). [para(15(a,1),22(a,1,2,2,2))]. given #112 (F,wt=10): 247 c1 ^ ((c2 v x) ' ^ y) = 0. [para(222(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #113 (F,wt=10): 250 c1 ^ (x v (c2 v y)) ' = 0. [para(25(a,1),222(a,1,2,1))]. given #114 (T,wt=10): 251 c1 ^ (x ^ (c2 v y) ') = 0. [para(222(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #115 (T,wt=10): 252 c1 ^ (x v (y v c2)) ' = 0. [para(14(a,1),224(a,1,2,1))]. given #116 (A,wt=27): 54 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ v) = x ^ ((y v (z ^ (x v u))) ^ v). [para(22(a,1),16(a,1,1)),demod(16(5)),flip(a)]. given #117 (F,wt=10): 253 c1 ^ ((x v c2) ' ^ y) = 0. [para(224(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #118 (F,wt=10): 256 c1 ^ (x ^ (y v c2) ') = 0. [para(224(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #119 (T,wt=10): 272 x v (y ^ (x ^ z)) ' = 1. [para(26(a,1),227(a,1,2,1))]. given #120 (T,wt=10): 273 x v ((y ^ x) ' v z) = 1. [para(268(a,1),14(a,1,1)),demod(99(2)),flip(a)]. given #121 (A,wt=31): 55 x ^ (y ^ (z v ((x ^ (y ^ u)) v (u ^ (z v v))))) = x ^ (y ^ (z v (u ^ ((x ^ y) v v)))). [para(22(a,1),16(a,1)),demod(16(6),16(8)),flip(a)]. given #122 (F,wt=10): 275 x v (y ^ (z ^ x)) ' = 1. [para(16(a,1),268(a,1,2,1))]. given #123 (F,wt=10): 280 x v (y v (z ^ x) ') = 1. [para(268(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #124 (T,wt=10): 284 (c2 ^ x) v (c1 ^ x) ' = 1. [para(64(a,1),268(a,1,2,1))]. given #125 (T,wt=10): 289 c2 v (x v (c1 ' v y)) = 1. [para(285(a,1),14(a,1,1)),demod(99(2),14(6)),flip(a)]. given #126 (A,wt=29): 56 x ^ (y v ((x ^ (z ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))). [para(16(a,1),22(a,1,2,2,2)),demod(16(11))]. given #127 (F,wt=10): 290 c2 v (x v (y v c1 ')) = 1. [para(14(a,1),285(a,1,2))]. given #128 (F,wt=10): 321 x v (y v (y v x) ') = 1. [para(13(a,1),38(a,1,2,2,1))]. given #129 (T,wt=10): 328 c2 v ((x ^ c1) ' v y) = 1. [para(309(a,1),14(a,1,1)),demod(99(2)),flip(a)]. given #130 (T,wt=10): 330 c2 v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),309(a,1,2,1))]. given #131 (A,wt=16): 59 x ^ (y v (z ^ (x v y '))) = x ^ (y v z). [para(19(a,1),22(a,1,2,2,2,2)),demod(39(3),13(2),33(2)),flip(a)]. given #132 (F,wt=10): 333 c2 v (x v (y ^ c1) ') = 1. [para(309(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #133 (F,wt=10): 334 c2 v ((c1 ^ x) ' v y) = 1. [para(329(a,1),14(a,1,1)),demod(99(2)),flip(a)]. given #134 (T,wt=10): 337 c2 v (x v (c1 ^ y) ') = 1. [para(329(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #135 (T,wt=10): 338 c2 v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),329(a,1,2,1))]. given #136 (A,wt=49): 62 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(22(a,1),22(a,1,2,2,1))]. given #137 (F,wt=10): 344 x ^ (y ^ (y ^ x) ') = 0. [para(15(a,1),41(a,1,2,2,1))]. given #138 (F,wt=10): 351 c1 ^ (x ^ (c2 ^ x) ') = 0. [para(41(a,1),64(a,1,2)),demod(15(3),102(3)),flip(a)]. given #139 (T,wt=10): 378 c2 != 1 | c1 != 0 | c2 ' = c1. [para(132(a,1),43(a,1)),demod(15(6),23(6))]. given #140 (T,wt=10): 399 x ' v (y v (x v z)) = 1. [para(397(a,1),14(a,1,1)),demod(99(2),14(4)),flip(a)]. given #141 (A,wt=31): 63 x ^ (y v (z ^ (x v ((z ^ u) v (u ^ (y v v)))))) = x ^ (y v (z ^ (x v (u ^ (z v v))))). [para(22(a,1),22(a,1,2,2,2)),demod(22(8)),flip(a)]. given #142 (F,wt=8): 2077 c1 ' v (x v c2) = 1. [para(132(a,1),399(a,1,2,2))]. given #143 (F,wt=10): 400 x ' v (y v (z v x)) = 1. [para(14(a,1),397(a,1,2))]. given #144 (T,wt=10): 406 x ' ^ (y ^ (x ^ z)) = 0. [para(398(a,1),16(a,1,1)),demod(102(2),16(4)),flip(a)]. given #145 (T,wt=10): 407 x ' ^ (y ^ (z ^ x)) = 0. [para(16(a,1),398(a,1,2))]. given #146 (A,wt=14): 73 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(48),demod(68(4))]. given #147 (F,wt=7): 2344 c1 != 1 | c1 ' = 0. [para(186(a,1),73(b,1)),demod(186(12)),flip(a),xx(b)]. given #148 (F,wt=7): 2346 x ' != 1 | 0 = x. [para(398(a,1),73(b,1)),demod(374(8),398(9)),flip(a),flip(c),xx(b)]. given #149 (T,wt=8): 2303 c2 ' ^ (x ^ c1) = 0. [para(23(a,1),407(a,1,2,2))]. given #150 (T,wt=7): 2361 c2 ' != 1 | c2 = 0. [para(2303(a,1),73(b,1)),demod(374(10),2303(13)),flip(a),xx(b)]. given #151 (A,wt=17): 78 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_demod(72),demod(74(7))]. given #152 (F,wt=10): 2348 (c1 ^ (c1 ' v c2 ')) ' != 1. [ur(2346,b,153,a(flip))]. given #153 (F,wt=10): 418 (x ^ c2) v (x ^ c1) ' = 1. [para(111(a,1),268(a,1,2,1))]. given #154 (T,wt=10): 419 x ^ (c1 ^ (x ^ c2) ') = 0. [para(111(a,1),398(a,1,2)),demod(15(6),16(6))]. given #155 (T,wt=10): 505 (x v c1) ^ (x v c2) ' = 0. [para(137(a,1),180(a,1,2,1))]. given #156 (A,wt=14): 79 x v y != 1 | 0 != x | x ' = x v y. [back_demod(47),demod(74(2))]. given #157 (F,wt=7): 2473 c2 != 0 | c2 ' = 1. [para(279(a,1),79(a,1)),demod(279(12)),flip(b),xx(a)]. given #158 (F,wt=7): 2475 x ' != 0 | 1 = x. [para(397(a,1),79(a,1)),demod(374(8),397(9)),flip(b),flip(c),xx(a)]. given #159 (T,wt=7): 2477 c1 ' != 0 | c1 = 1. [para(2077(a,1),79(a,1)),demod(374(10),2077(13)),flip(b),xx(a)]. given #160 (T,wt=10): 509 x v (c2 v (x v c1) ') = 1. [para(137(a,1),397(a,1,2)),demod(13(6),14(6))]. given #161 (A,wt=11): 85 x v (y v (x ^ z)) = y v x. [para(18(a,1),25(a,1,2)),flip(a)]. given #162 (F,wt=10): 630 (x v c1) ^ (c2 v x) ' = 0. [para(501(a,1),180(a,1,2,1))]. given #163 (F,wt=10): 632 c2 v (x v (x v c1) ') = 1. [para(501(a,1),397(a,1,2)),demod(13(6),14(6))]. given #164 (T,wt=10): 1608 (x ^ c2) v (c1 ^ x) ' = 1. [para(15(a,1),284(a,1,1))]. given #165 (T,wt=10): 1609 (c2 ^ x) v (x ^ c1) ' = 1. [para(15(a,1),284(a,1,2,1))]. given #166 (A,wt=20): 87 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(25(a,1),21(a,1))]. given #167 (F,wt=10): 1610 (c2 ^ (c1 v x)) v c1 ' = 1. [para(17(a,1),284(a,1,2,1))]. given #168 (F,wt=10): 1616 (c2 ^ (x v c1)) v c1 ' = 1. [para(27(a,1),284(a,1,2,1))]. given #169 (T,wt=10): 2030 c1 ^ (x ^ (x ^ c2) ') = 0. [para(344(a,1),64(a,1,2)),demod(15(3),102(3)),flip(a)]. given #170 (T,wt=10): 2049 x ^ (c1 ^ (c2 ^ x) ') = 0. [para(351(a,1),26(a,1)),flip(a)]. given #171 (A,wt=27): 88 x ^ (y v ((x ^ z) v (z ^ (u v (y v v))))) = x ^ (y v (z ^ (x v (u v v)))). [para(25(a,1),22(a,1,2,2,2,2))]. given #172 (F,wt=10): 2051 c1 ^ (c2 ^ (c1 v x)) ' = 0. [para(351(a,1),29(a,1)),flip(a)]. given #173 (F,wt=10): 2081 c1 ' v (x v (c2 v y)) = 1. [para(136(a,1),399(a,1,2,2))]. given #174 (T,wt=10): 2083 c1 ' v (x v (y v c2)) = 1. [para(139(a,1),399(a,1,2,2))]. given #175 (T,wt=10): 2252 (x ^ y) ' v (z v x) = 1. [para(18(a,1),400(a,1,2,2))]. given #176 (A,wt=23): 89 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(25(a,1),22(a,1,2))]. given #177 (F,wt=10): 2256 (x ^ y) ' v (z v y) = 1. [para(33(a,1),400(a,1,2,2))]. given #178 (F,wt=10): 2260 (x ^ c1) ' v (y v c2) = 1. [para(306(a,1),400(a,1,2,2))]. given #179 (T,wt=10): 2261 (c1 ^ x) ' v (y v c2) = 1. [para(312(a,1),400(a,1,2,2))]. given #180 (T,wt=10): 2284 c2 ' ^ (x ^ (y ^ c1)) = 0. [para(65(a,1),406(a,1,2,2))]. given #181 (A,wt=11): 90 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [back_demod(67),demod(84(8)),flip(a)]. given #182 (F,wt=10): 2299 (x v y) ' ^ (z ^ x) = 0. [para(17(a,1),407(a,1,2,2))]. given #183 (F,wt=10): 2305 (x v y) ' ^ (z ^ y) = 0. [para(27(a,1),407(a,1,2,2))]. given #184 (T,wt=10): 2310 (c2 v x) ' ^ (y ^ c1) = 0. [para(214(a,1),407(a,1,2,2))]. given #185 (T,wt=10): 2311 (x v c2) ' ^ (y ^ c1) = 0. [para(219(a,1),407(a,1,2,2))]. given #186 (A,wt=13): 91 x ^ (y v ((x v z) ^ (x v u))) = x. [back_demod(57),demod(84(6)),flip(a)]. given #187 (F,wt=10): 2342 c1 != 1 | c1 != 0 | c1 ' = c1. [para(23(a,1),73(b,1)),demod(23(11)),flip(a)]. given #188 (F,wt=10): 2349 c2 ' ^ (x ^ (c1 ^ y)) = 0. [para(2303(a,1),16(a,1,1)),demod(102(2),16(6)),flip(a)]. given #189 (T,wt=10): 2453 (c1 v x) ^ (x v c2) ' = 0. [para(13(a,1),505(a,1,1))]. given #190 (T,wt=10): 2474 c2 != 1 | c2 != 0 | c2 ' = c2. [para(306(a,1),79(a,1)),demod(306(12)),flip(b)]. given #191 (A,wt=17): 94 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(42(a,1),22(a,1,2,2,2,2)),demod(77(5),42(6))]. given #192 (F,wt=10): 2478 x v (c2 v (c1 v x) ') = 1. [para(13(a,1),509(a,1,2,2,1))]. given #193 (F,wt=10): 2527 (c1 v x) ^ (c2 v x) ' = 0. [para(13(a,1),630(a,1,1))]. given #194 (T,wt=10): 2528 (c1 v (c2 ^ x)) ^ c2 ' = 0. [para(18(a,1),630(a,1,2,1)),demod(13(4))]. given #195 (T,wt=10): 2532 (c1 v (x ^ c2)) ^ c2 ' = 0. [para(33(a,1),630(a,1,2,1)),demod(13(4))]. given #196 (A,wt=21): 95 x ^ (y v (x ' ^ (y v z))) = x ^ (y v (x ' ^ (x v z))). [back_demod(60),demod(92(5))]. given #197 (F,wt=10): 2549 c2 v (x v (c1 v x) ') = 1. [para(13(a,1),632(a,1,2,2,1))]. given #198 (F,wt=10): 2554 c2 v (c1 v (c2 ^ x)) ' = 1. [para(632(a,1),31(a,1)),demod(13(6)),flip(a)]. given #199 (T,wt=10): 2649 c1 ' v (c2 ^ (c1 v x)) = 1. [para(1610(a,1),13(a,1)),flip(a)]. given #200 (T,wt=10): 2665 c1 ' v (c2 ^ (x v c1)) = 1. [para(1616(a,1),13(a,1)),flip(a)]. given #201 (A,wt=19): 96 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_demod(80),demod(94(9))]. given #202 (F,wt=10): 2867 c1 ^ (c2 ^ (x v c1)) ' = 0. [para(13(a,1),2051(a,1,2,1,2))]. given #203 (F,wt=10): 3599 c2 ' ^ (c1 v (c2 ^ x)) = 0. [para(2528(a,1),15(a,1)),flip(a)]. given #204 (T,wt=10): 3617 c2 ' ^ (c1 v (x ^ c2)) = 0. [para(2532(a,1),15(a,1)),flip(a)]. given #205 (T,wt=10): 3843 c2 v (c1 v (x ^ c2)) ' = 1. [para(15(a,1),2554(a,1,2,1,2))]. given #206 (A,wt=11): 105 x ^ (y ^ (x v z)) = y ^ x. [para(17(a,1),26(a,1,2)),flip(a)]. given #207 (F,wt=11): 120 x ^ ((y v x) ^ z) = x ^ z. [para(27(a,1),16(a,1,1)),flip(a)]. given #208 (F,wt=11): 125 x ^ (y ^ (z v x)) = y ^ x. [para(27(a,1),26(a,1,2)),flip(a)]. given #209 (T,wt=11): 126 x v ((y ^ x) v z) = x v z. [para(33(a,1),14(a,1,1)),flip(a)]. given #210 (T,wt=11): 133 x v (y v (z ^ x)) = y v x. [para(33(a,1),25(a,1,2)),flip(a)]. given #211 (A,wt=20): 108 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(26(a,1),21(b,1))]. given #212 (F,wt=11): 151 (x v c1) ^ (x v c2) = x v c1. [para(132(a,1),28(a,1,2,2))]. given #213 (F,wt=11): 188 c1 v c2 ' != 1 | c2 ' = c1 '. [para(186(a,1),21(b,1)),flip(c),xx(b)]. given #214 (T,wt=11): 220 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(64(a,1),33(a,1,2)),demod(13(5))]. given #215 (T,wt=11): 221 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(29(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #216 (A,wt=29): 109 x ^ (y v ((z ^ (x ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))). [para(26(a,1),22(a,1,2,2,1)),demod(16(5),16(11))]. given #217 (F,wt=11): 241 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(214(a,1),26(a,1,2)),flip(a)]. given #218 (F,wt=11): 243 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(219(a,1),16(a,1,1)),flip(a)]. given #219 (T,wt=11): 246 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(219(a,1),26(a,1,2)),flip(a)]. given #220 (T,wt=11): 287 c2 ^ c1 ' != 0 | c2 ' = c1 '. [para(279(a,1),21(a,1)),xx(a)]. given #221 (A,wt=27): 110 x ^ (y ^ (z v ((x ^ u) v (u ^ (z v v))))) = y ^ (x ^ (z v (u ^ (x v v)))). [para(22(a,1),26(a,1,2)),flip(a)]. given #222 (F,wt=11): 308 c2 v ((x ^ c1) v y) = c2 v y. [para(65(a,1),31(a,1,2,1))]. given #223 (F,wt=11): 311 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(65(a,1),34(a,1,2))]. given #224 (T,wt=11): 315 c2 v (x v (y ^ c1)) = x v c2. [para(306(a,1),25(a,1,2)),flip(a)]. given #225 (T,wt=11): 316 c2 v ((c1 ^ x) v y) = c2 v y. [para(312(a,1),14(a,1,1)),flip(a)]. given #226 (A,wt=13): 112 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [back_demod(103),demod(105(7))]. given #227 (F,wt=11): 319 c2 v (x v (c1 ^ y)) = x v c2. [para(312(a,1),25(a,1,2)),flip(a)]. given #228 (F,wt=11): 342 (x v y) ^ (z ^ x) = z ^ x. [para(70(a,1),29(a,2)),demod(341(4))]. given #229 (T,wt=11): 343 (x ^ y) v (y ^ x) = x ^ y. [para(70(a,1),34(a,1,2))]. given #230 (T,wt=10): 5337 (x ^ y) v (y ^ x) ' = 1. [para(343(a,1),397(a,1,2)),demod(13(4))]. given #231 (A,wt=13): 121 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(27(a,1),16(a,1)),flip(a)]. given #232 (F,wt=11): 357 (x v y) ^ (y v x) = x v y. [para(76(a,1),28(a,1,2))]. given #233 (F,wt=10): 5465 (x v y) ^ (y v x) ' = 0. [para(357(a,1),398(a,1,2)),demod(15(4))]. given #234 (T,wt=11): 358 (x ^ y) v (z v x) = z v x. [para(76(a,1),31(a,2)),demod(355(4))]. given #235 (T,wt=11): 360 x ^ (y v (z v (x v u))) = x. [para(14(a,1),84(a,1,2))]. given #236 (A,wt=14): 122 x v y != 1 | 0 != y | y ' = x v y. [para(27(a,1),21(b,1)),demod(76(2)),flip(b)]. given #237 (F,wt=11): 366 x v (y ^ (z ^ (x ^ u))) = x. [para(16(a,1),106(a,1,2))]. given #238 (F,wt=11): 417 (x ^ c1) v (x ^ c2) = x ^ c2. [para(111(a,1),33(a,1,2)),demod(13(5))]. given #239 (T,wt=11): 427 x v y != 0 | (x v y) ' = 1. [para(39(a,1),44(b,1)),demod(113(2),113(2)),xx(a)]. given #240 (T,wt=11): 431 x v y != 1 | (x v y) ' = 0. [para(42(a,1),44(a,1,2)),demod(15(6),102(6)),xx(b)]. given #241 (A,wt=13): 123 x ^ (y v ((z v x) ^ (x v u))) = x. [para(27(a,1),22(a,1,2,2,1)),demod(84(6)),flip(a)]. given #242 (F,wt=7): 5671 c2 != 1 | c2 ' = 0. [para(132(a,1),431(a,1)),demod(132(6))]. given #243 (F,wt=11): 468 x ^ (y v (z v (u v x))) = x. [para(14(a,1),119(a,1,2,2))]. given #244 (T,wt=11): 482 x v (y ^ (z ^ (u ^ x))) = x. [para(16(a,1),128(a,1,2,2))]. given #245 (T,wt=11): 543 (c1 v x) ^ (x v c2) = c1 v x. [para(139(a,1),28(a,1,2))]. given #246 (A,wt=13): 124 (x v y) ^ (x v (z v y)) = x v y. [para(25(a,1),27(a,1,2))]. given #247 (F,wt=11): 546 c1 ^ (x v (y v (c2 v z))) = c1. [para(14(a,1),240(a,1,2))]. given #248 (F,wt=11): 552 c1 ^ (x v (y v (z v c2))) = c1. [para(14(a,1),242(a,1,2,2))]. given #249 (T,wt=11): 559 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(16(a,1),313(a,1,2,2))]. given #250 (T,wt=11): 571 x ^ y != 0 | (x ^ y) ' = 1. [para(39(a,1),46(b,1,2)),demod(13(3),99(3)),xx(a)]. given #251 (A,wt=13): 127 x v (y v (z ^ (x v y))) = x v y. [para(33(a,1),14(a,1)),flip(a)]. given #252 (F,wt=7): 6013 c1 != 0 | c1 ' = 1. [para(23(a,1),571(a,1)),demod(23(6))]. given #253 (F,wt=11): 573 x ^ y != 1 | (x ^ y) ' = 0. [para(42(a,1),46(a,1)),demod(116(5),116(5)),xx(b)]. given #254 (T,wt=11): 621 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(16(a,1),320(a,1,2))]. given #255 (T,wt=11): 629 (x v c1) ^ (c2 v x) = x v c1. [para(501(a,1),27(a,1,2))]. given #256 (A,wt=14): 129 1 != x | y ^ x != 0 | x ' = y ^ x. [para(33(a,1),21(a,1)),demod(70(4)),flip(a)]. given #257 (F,wt=11): 2935 (x ^ y) ' != 0 | x ^ y = 1. [para(2252(a,1),79(a,1)),demod(374(10),2252(12)),flip(b),xx(a)]. given #258 (F,wt=11): 3238 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(13(a,1),90(a,1,2,2,2))]. given #259 (T,wt=11): 3239 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(13(a,1),90(a,1,2))]. given #260 (T,wt=11): 3289 (x v y) ' != 1 | x v y = 0. [para(2299(a,1),73(b,1)),demod(374(10),2299(12)),flip(a),xx(b)]. given #261 (A,wt=19): 130 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)). [para(33(a,1),22(a,1,2,2,2,2)),demod(97(5)),flip(a)]. given #262 (F,wt=11): 4094 (x v y) ^ (z ^ y) = z ^ y. [para(70(a,1),120(a,2)),demod(341(4))]. given #263 (F,wt=11): 4206 (x ^ y) v (z v y) = z v y. [para(76(a,1),126(a,2)),demod(355(4))]. given #264 (T,wt=11): 4458 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(15(a,1),220(a,1,1))]. given #265 (T,wt=11): 4459 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(15(a,1),220(a,1,2))]. given #266 (A,wt=33): 131 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(22(a,1),33(a,1,2)),demod(13(10),25(10),25(9),13(8))]. given #267 (F,wt=11): 4540 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(70(a,1),221(a,2)),demod(341(7))]. given #268 (F,wt=11): 4788 (x v c2) ^ (y ^ c1) = y ^ c1. [para(70(a,1),243(a,2)),demod(341(7))]. given #269 (T,wt=11): 5018 (x ^ c1) v (y v c2) = y v c2. [para(76(a,1),308(a,2)),demod(355(7))]. given #270 (T,wt=11): 5128 (c1 ^ x) v (y v c2) = y v c2. [para(76(a,1),316(a,2)),demod(355(7))]. given #271 (A,wt=13): 134 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(26(a,1),33(a,1,2))]. given #272 (F,wt=11): 5667 x v y != 0 | (y v x) ' = 1. [para(13(a,1),427(a,1))]. given #273 (F,wt=11): 5669 x v y != 1 | (y v x) ' = 0. [para(13(a,1),431(a,1))]. given #274 (T,wt=11): 5860 (c1 v x) ^ (c2 v x) = c1 v x. [para(13(a,1),543(a,1,2))]. given #275 (T,wt=11): 5861 (x v c2) ^ (c1 v x) = c1 v x. [para(543(a,1),15(a,1)),flip(a)]. given #276 (A,wt=21): 138 x ^ (c1 v ((x ^ y) v (y ^ c2))) = x ^ (c1 v (y ^ (x v c2))). [para(132(a,1),22(a,1,2,2,2,2))]. given #277 (F,wt=11): 6012 x ^ y != 0 | (y ^ x) ' = 1. [para(15(a,1),571(a,1))]. given #278 (F,wt=11): 6077 x ^ y != 1 | (y ^ x) ' = 0. [para(15(a,1),573(a,1))]. given #279 (T,wt=11): 6106 (c2 v x) ^ (x v c1) = x v c1. [para(629(a,1),15(a,1)),flip(a)]. given #280 (T,wt=11): 6179 (x ^ y) ' != 0 | y ^ x = 1. [para(15(a,1),2935(a,1,1))]. given #281 (A,wt=13): 140 (x v y) ^ (y v (x v z)) = y v x. [para(13(a,1),28(a,1,1))]. given #282 (F,wt=11): 6181 (x v y) ' != 0 | x v y = 1. [para(28(a,1),2935(a,1,1)),demod(28(8))]. given #283 (F,wt=7): 7119 c2 ' != 0 | c2 = 1. [para(132(a,1),6181(a,1,1)),demod(132(7))]. given #284 (T,wt=11): 6186 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(13(a,1),3238(a,1,2))]. given #285 (T,wt=11): 6251 (x v y) ' != 1 | y v x = 0. [para(13(a,1),3289(a,1,1))]. given #286 (A,wt=13): 141 (x v y) ^ (y v (z v x)) = x v y. [para(13(a,1),28(a,1,2)),demod(14(3))]. given #287 (F,wt=11): 6253 (x ^ y) ' != 1 | x ^ y = 0. [para(34(a,1),3289(a,1,1)),demod(34(8))]. given #288 (F,wt=7): 7231 c1 ' != 1 | c1 = 0. [para(23(a,1),6253(a,1,1)),demod(23(7))]. given #289 (T,wt=11): 6524 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(4459(a,1),13(a,1)),flip(a)]. given #290 (T,wt=11): 6572 x v (c2 ^ (x v c1)) = x v c1. [para(214(a,1),131(a,1,2,2,2,2,2)),demod(15(3),23(3),31(10),4468(6),15(8),23(8),18(10))]. given #291 (A,wt=19): 142 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(14(a,1),28(a,1,1)),demod(14(5),14(8))]. given #292 (F,wt=11): 7079 (x v y) ' != 0 | y v x = 1. [para(357(a,1),6179(a,1,1)),demod(357(7))]. given #293 (F,wt=11): 7157 (x ^ y) ' != 1 | y ^ x = 0. [para(343(a,1),6251(a,1,1)),demod(343(7))]. given #294 (T,wt=11): 7281 x v (c2 ^ (c1 v x)) = x v c1. [para(13(a,1),6572(a,1,2,2))]. given #295 (T,wt=11): 7287 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(6572(a,1),22(a,1,2,2)),demod(13(6),76(7),112(13))]. given #296 (A,wt=17): 143 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(28(a,1),16(a,1,1)),flip(a)]. given #297 (F,wt=11): 7294 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(6572(a,1),49(a,1,2,2)),demod(13(5),74(6),7287(5),18(7)),flip(a)]. given #298 (F,wt=12): 154 x v (y v ((x v y) ' v z)) = 1. [para(100(a,1),14(a,1)),flip(a)]. given #299 (T,wt=12): 158 x ^ (y ^ ((x ^ y) ' ^ z)) = 0. [para(104(a,1),16(a,1)),flip(a)]. given #300 (T,wt=12): 162 x v (y v (z v (x v y) ')) = 1. [para(114(a,1),14(a,1)),flip(a)]. given #301 (A,wt=19): 146 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(28(a,1),22(a,1,2,2,2)),demod(13(4),33(4),74(2)),flip(a)]. given #302 (F,wt=12): 175 x ^ (y ^ (z ^ (x ^ y) ')) = 0. [para(117(a,1),16(a,1)),flip(a)]. given #303 (F,wt=12): 181 (x v y) ^ (x v (y v z)) ' = 0. [para(14(a,1),167(a,1,2,1))]. given #304 (T,wt=12): 182 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(167(a,1),16(a,1)),flip(a)]. given #305 (T,wt=12): 202 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(180(a,1),16(a,1)),flip(a)]. given #306 (A,wt=19): 147 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(25(a,1),28(a,1,1)),demod(14(4))]. given #307 (F,wt=12): 205 (x v y) ^ (x v (z v y)) ' = 0. [para(25(a,1),180(a,1,2,1))]. given #308 (F,wt=12): 235 ((x ^ y) v z) ^ (x v z) ' = 0. [para(31(a,1),180(a,1,2,1))]. given #309 (T,wt=12): 267 x v (y v ((x v y) ^ z) ') = 1. [para(227(a,1),14(a,1)),flip(a)]. given #310 (T,wt=12): 269 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(16(a,1),227(a,1,2,1))]. given #311 (A,wt=15): 148 (x v y) ^ (x v (z v (y v u))) = x v y. [para(25(a,1),28(a,1,2,2))]. given #312 (F,wt=12): 274 x v (y v (z ^ (x v y)) ') = 1. [para(268(a,1),14(a,1)),flip(a)]. given #313 (F,wt=12): 281 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(26(a,1),268(a,1,2,1))]. given #314 (T,wt=12): 282 ((x v y) ^ z) v (x ^ z) ' = 1. [para(29(a,1),268(a,1,2,1))]. given #315 (T,wt=12): 325 x v (y v (z v (x v z) ')) = 1. [para(38(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #316 (A,wt=17): 149 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(28(a,1),26(a,1,2)),flip(a)]. given #317 (F,wt=12): 327 x v (y v ((x ^ z) v y) ') = 1. [para(38(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #318 (F,wt=12): 348 x ^ (y ^ (z ^ (x ^ z) ')) = 0. [para(41(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #319 (T,wt=12): 350 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(41(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #320 (T,wt=12): 403 x v ((x v y) ' v (z v y)) = 1. [para(25(a,1),397(a,1,2)),demod(25(5))]. given #321 (A,wt=22): 152 x v (y v z) != 1 | x v y != 0 | (x v y) ' = x v (y v z). [back_demod(144),demod(150(4))]. given #322 (F,wt=12): 411 x ^ ((x ^ y) ' ^ (z ^ y)) = 0. [para(26(a,1),398(a,1,2)),demod(26(5))]. given #323 (F,wt=12): 712 x v (y v (z v (x ' v u))) = 1. [para(14(a,1),157(a,1,2))]. given #324 (T,wt=12): 715 x v (y v ((x ^ z) ' v u)) = 1. [para(157(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #325 (T,wt=12): 723 x ^ (y ^ (z ^ (x ' ^ u))) = 0. [para(16(a,1),161(a,1,2))]. given #326 (A,wt=15): 155 x ^ (x ' v y) != 0 | x ' v y = x '. [para(100(a,1),21(a,1)),flip(c),xx(a)]. given #327 (F,wt=12): 726 x ^ (y ^ ((x v z) ' ^ u)) = 0. [para(161(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #328 (F,wt=12): 794 x v (y v (z v (u v x '))) = 1. [para(14(a,1),163(a,1,2,2))]. given #329 (T,wt=12): 797 x v (y v (z v (x ^ u) ')) = 1. [para(163(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #330 (T,wt=12): 808 x ^ ((y v (x v z)) ' ^ u) = 0. [para(25(a,1),174(a,1,2,1,1))]. given #331 (A,wt=18): 156 x ^ (y v (z ^ (x v (y ' v u)))) = x ^ (y v z). [para(100(a,1),22(a,1,2,2,2,2)),demod(39(3),13(2),33(2)),flip(a)]. given #332 (F,wt=12): 814 x ^ (y ^ (z ^ (u ^ x '))) = 0. [para(16(a,1),176(a,1,2,2))]. given #333 (F,wt=12): 817 x ^ (y ^ (z ^ (x v u) ')) = 0. [para(176(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #334 (T,wt=12): 827 x ^ (y ^ (z v (x v u)) ') = 0. [para(25(a,1),179(a,1,2,2,1))]. given #335 (T,wt=12): 941 x ^ (y v (z v (x v u))) ' = 0. [para(14(a,1),185(a,1,2,1))]. given #336 (A,wt=15): 159 x v (x ' ^ y) != 1 | x ' ^ y = x '. [para(104(a,1),21(b,1)),flip(c),xx(b)]. given #337 (F,wt=12): 950 x ^ (y v (z v (u v x))) ' = 0. [para(14(a,1),200(a,1,2,1,2))]. given #338 (F,wt=12): 951 x ^ ((y v (z v x)) ' ^ u) = 0. [para(200(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #339 (T,wt=12): 956 x ^ (y ^ (z v (u v x)) ') = 0. [para(200(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #340 (T,wt=12): 963 (x v c1) ^ (y v (c2 v x)) ' = 0. [para(501(a,1),200(a,1,2,1,2))]. given #341 (A,wt=25): 160 x ^ (y v (x ' ^ (z ^ (y v u)))) = x ^ (y v (x ' ^ (z ^ (x v u)))). [para(104(a,1),22(a,1,2,2,1)),demod(16(5),92(6),16(10))]. given #342 (F,wt=12): 970 x ^ (y ^ ((z v x) ' ^ u)) = 0. [para(201(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #343 (F,wt=12): 976 (x v c1) ^ ((c2 v x) ' ^ y) = 0. [para(501(a,1),201(a,1,2,1,1))]. given #344 (T,wt=12): 979 x ^ (y ^ (z ^ (u v x) ')) = 0. [para(16(a,1),206(a,1,2))]. given #345 (T,wt=12): 989 (x v c1) ^ (y ^ (c2 v x) ') = 0. [para(501(a,1),206(a,1,2,2,1))]. given #346 (A,wt=15): 164 x ^ (y v x ') != 0 | y v x ' = x '. [para(114(a,1),21(a,1)),flip(c),xx(a)]. given #347 (F,wt=12): 1059 c1 ^ (x ^ (y ^ (c2 ' ^ z))) = 0. [para(16(a,1),209(a,1,2))]. given #348 (F,wt=12): 1068 c1 ^ (x ^ (y ^ (z ^ c2 '))) = 0. [para(16(a,1),210(a,1,2,2))]. given #349 (T,wt=12): 1081 x v ((y ^ (x ^ z)) ' v u) = 1. [para(26(a,1),233(a,1,2,1,1))]. given #350 (T,wt=12): 1091 x v (y v (z ^ (x ^ u)) ') = 1. [para(26(a,1),234(a,1,2,2,1))]. given #351 (A,wt=18): 165 x ^ (y v (z ^ (x v (u v y ')))) = x ^ (y v z). [para(114(a,1),22(a,1,2,2,2,2)),demod(39(3),13(2),33(2)),flip(a)]. given #352 (F,wt=12): 1187 c1 ^ ((x v (c2 v y)) ' ^ z) = 0. [para(25(a,1),247(a,1,2,1,1))]. given #353 (F,wt=12): 1188 c1 ^ (x ^ ((c2 v y) ' ^ z)) = 0. [para(247(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #354 (T,wt=12): 1195 c1 ^ (x v (y v (c2 v z))) ' = 0. [para(14(a,1),250(a,1,2,1))]. given #355 (T,wt=12): 1198 c1 ^ (x ^ (y v (c2 v z)) ') = 0. [para(250(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #356 (A,wt=17): 166 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(29(a,1),16(a,1)),demod(16(2)),flip(a)]. given #357 (F,wt=12): 1205 c1 ^ (x ^ (y ^ (c2 v z) ')) = 0. [para(16(a,1),251(a,1,2))]. given #358 (F,wt=12): 1215 c1 ^ (x v (y v (z v c2))) ' = 0. [para(14(a,1),252(a,1,2,1,2))]. given #359 (T,wt=12): 1216 c1 ^ ((x v (y v c2)) ' ^ z) = 0. [para(252(a,1),16(a,1,1)),demod(102(2)),flip(a)]. given #360 (T,wt=12): 1219 c1 ^ (x ^ (y v (z v c2)) ') = 0. [para(252(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #361 (A,wt=22): 168 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(29(a,1),21(b,1))]. given #362 (F,wt=12): 1364 c1 ^ (x ^ ((y v c2) ' ^ z)) = 0. [para(253(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #363 (F,wt=12): 1372 c1 ^ (x ^ (y ^ (z v c2) ')) = 0. [para(16(a,1),256(a,1,2))]. given #364 (T,wt=12): 1385 x v (y ^ (z ^ (x ^ u))) ' = 1. [para(16(a,1),272(a,1,2,1))]. given #365 (T,wt=12): 1396 x v ((y ^ (z ^ x)) ' v u) = 1. [para(16(a,1),273(a,1,2,1,1))]. given #366 (A,wt=31): 169 x ^ (y v ((x ^ z) v ((x v u) ^ (z ^ (y v v))))) = x ^ (y v ((x v u) ^ (z ^ (x v v)))). [para(29(a,1),22(a,1,2,2,1)),demod(16(5),16(12))]. given #367 (F,wt=12): 1400 x v (y v ((z ^ x) ' v u)) = 1. [para(273(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #368 (F,wt=12): 1404 (c2 ^ x) v ((c1 ^ x) ' v y) = 1. [para(64(a,1),273(a,1,2,1,1))]. given #369 (T,wt=12): 1406 (x ^ c2) v ((x ^ c1) ' v y) = 1. [para(111(a,1),273(a,1,2,1,1))]. given #370 (T,wt=12): 1559 x v (y ^ (z ^ (u ^ x))) ' = 1. [para(16(a,1),275(a,1,2,1,2))]. given #371 (A,wt=27): 170 x ^ (y v (((x v z) ^ u) v (u ^ (y v v)))) = x ^ (y v (u ^ (x v (z v v)))). [para(22(a,1),29(a,1,2)),demod(14(3),29(7)),flip(a)]. given #372 (F,wt=12): 1563 x v (y v (z ^ (u ^ x)) ') = 1. [para(275(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #373 (F,wt=12): 1568 (c2 ^ x) v (y ^ (c1 ^ x)) ' = 1. [para(64(a,1),275(a,1,2,1,2))]. given #374 (T,wt=12): 1570 (x ^ c2) v (y ^ (x ^ c1)) ' = 1. [para(111(a,1),275(a,1,2,1,2))]. given #375 (T,wt=12): 1584 x v (y v (z v (u ^ x) ')) = 1. [para(14(a,1),280(a,1,2))]. given #376 (A,wt=13): 171 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(25(a,1),29(a,1,2,1))]. given #377 (F,wt=12): 1591 (c2 ^ x) v (y v (c1 ^ x) ') = 1. [para(64(a,1),280(a,1,2,2,1))]. given #378 (F,wt=12): 1593 (x ^ c2) v (y v (x ^ c1) ') = 1. [para(111(a,1),280(a,1,2,2,1))]. given #379 (T,wt=12): 1619 (c2 ^ (x v (c1 v y))) v c1 ' = 1. [para(84(a,1),284(a,1,2,1))]. given #380 (T,wt=12): 1622 (c2 ^ (x v (y v c1))) v c1 ' = 1. [para(119(a,1),284(a,1,2,1))]. given #381 (A,wt=15): 172 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(29(a,1),26(a,1,2)),flip(a)]. given #382 (F,wt=12): 1633 c2 v (x v (y v (c1 ' v z))) = 1. [para(14(a,1),289(a,1,2))]. given #383 (F,wt=12): 1737 c2 v (x v (y v (z v c1 '))) = 1. [para(14(a,1),290(a,1,2,2))]. given #384 (T,wt=12): 1750 x v (y v ((y v x) ' v z)) = 1. [para(321(a,1),14(a,1,1)),demod(99(2),14(5)),flip(a)]. given #385 (T,wt=12): 1755 x v (y v (z v (z v x) ')) = 1. [para(321(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #386 (A,wt=15): 173 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(29(a,1),33(a,1,2)),demod(13(4))]. given #387 (F,wt=12): 1757 x v (y v (y v (x ^ z)) ') = 1. [para(321(a,1),31(a,1,2)),demod(113(2)),flip(a)]. given #388 (F,wt=12): 1767 c2 v ((x ^ (y ^ c1)) ' v z) = 1. [para(16(a,1),328(a,1,2,1,1))]. given #389 (T,wt=12): 1770 c2 v (x v ((y ^ c1) ' v z)) = 1. [para(328(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #390 (T,wt=12): 1778 c2 v (x ^ (y ^ (z ^ c1))) ' = 1. [para(16(a,1),330(a,1,2,1,2))]. given #391 (A,wt=15): 177 x v (y ^ x ') != 1 | y ^ x ' = x '. [para(117(a,1),21(b,1)),flip(c),xx(b)]. given #392 (F,wt=12): 1781 c2 v (x v (y ^ (z ^ c1)) ') = 1. [para(330(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #393 (F,wt=12): 1821 c2 v (x v (y v (z ^ c1) ')) = 1. [para(14(a,1),333(a,1,2))]. given #394 (T,wt=12): 1835 c2 v (x v ((c1 ^ y) ' v z)) = 1. [para(334(a,1),25(a,1,2)),demod(113(2)),flip(a)]. given #395 (T,wt=12): 1836 c2 v ((x ^ (c1 ^ y)) ' v z) = 1. [para(26(a,1),334(a,1,2,1,1))]. given #396 (A,wt=25): 178 x ^ (y v (z ^ (x ' ^ (y v u)))) = x ^ (y v (z ^ (x ' ^ (x v u)))). [para(117(a,1),22(a,1,2,2,1)),demod(16(5),92(6),16(10))]. given #397 (F,wt=12): 1844 c2 v (x v (y v (c1 ^ z) ')) = 1. [para(14(a,1),337(a,1,2))]. given #398 (F,wt=12): 1847 c2 v (x v (y ^ (c1 ^ z)) ') = 1. [para(26(a,1),337(a,1,2,2,1))]. given #399 (T,wt=12): 1857 c2 v (x ^ (y ^ (c1 ^ z))) ' = 1. [para(16(a,1),338(a,1,2,1))]. given #400 (T,wt=12): 2022 x ^ (y ^ ((y ^ x) ' ^ z)) = 0. [para(344(a,1),16(a,1,1)),demod(102(2),16(5)),flip(a)]. given #401 (A,wt=15): 183 x v (x v y) ' != 1 | (x v y) ' = x '. [para(167(a,1),21(b,1)),flip(c),xx(b)]. given #402 (F,wt=12): 2027 x ^ (y ^ (z ^ (z ^ x) ')) = 0. [para(344(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #403 (F,wt=12): 2029 x ^ (y ^ (y ^ (x v z)) ') = 0. [para(344(a,1),29(a,1,2)),demod(116(2)),flip(a)]. given #404 (T,wt=12): 2044 c1 ^ (x ^ ((c2 ^ x) ' ^ y)) = 0. [para(351(a,1),16(a,1,1)),demod(102(2),16(7)),flip(a)]. given #405 (T,wt=12): 2048 c1 ^ (x ^ (y ^ (c2 ^ y) ')) = 0. [para(351(a,1),26(a,1,2)),demod(116(2)),flip(a)]. given #406 (A,wt=25): 184 x ^ (y v ((x v z) ' ^ (y v u))) = x ^ (y v ((x v z) ' ^ (x v u))). [para(167(a,1),22(a,1,2,2,1)),demod(92(6))]. given #407 (F,wt=12): 2074 x ' v (y v (z v (x v u))) = 1. [para(14(a,1),399(a,1,2))]. given #408 (F,wt=12): 2251 x ' v (y v (z v (u v x))) = 1. [para(14(a,1),400(a,1,2,2))]. given #409 (T,wt=12): 2262 (x ^ (y ^ z)) ' v (u v y) = 1. [para(106(a,1),400(a,1,2,2))]. given #410 (T,wt=12): 2266 (x ^ (y ^ z)) ' v (u v z) = 1. [para(128(a,1),400(a,1,2,2))]. given #411 (A,wt=21): 189 c1 ^ (x v (c2 ' ^ (c1 v y))) = c1 ^ (x v (c2 ' ^ (x v y))). [para(186(a,1),22(a,1,2,2,1)),demod(92(7)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 3.76 (+ 0.07) seconds. % Length of proof is 45. % Level of proof is 11. % Maximum clause weight is 23. % Given clauses 411. 10 x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [input]. 12 c1 ' != c1 ' v c2 '. [clausify]. 13 x v y = y v x. [input]. 14 (x v y) v z = x v (y v z). [input]. 15 x ^ y = y ^ x. [input]. 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. 17 x ^ (x v y) = x. [input]. 18 x v (x ^ y) = x. [input]. 19 x v x ' = 1. [input]. 20 x ^ x ' = 0. [input]. 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 22 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. 23 c1 ^ c2 = c1. [clausify]. 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. 26 x ^ (y ^ z) = y ^ (x ^ z). [para(15(a,1),16(a,1,1)),demod(16(2))]. 29 x ^ ((x v y) ^ z) = x ^ z. [para(17(a,1),16(a,1,1)),flip(a)]. 31 x v ((x ^ y) v z) = x v z. [para(18(a,1),14(a,1,1)),flip(a)]. 33 x v (y ^ x) = x. [para(15(a,1),18(a,1,2))]. 37 x v (x ' v y) = 1 v y. [para(19(a,1),14(a,1,1)),flip(a)]. 39 x ^ 1 = x. [para(19(a,1),17(a,1,2))]. 40 x ^ (x ' ^ y) = 0 ^ y. [para(20(a,1),16(a,1,1)),flip(a)]. 42 x v 0 = x. [para(20(a,1),18(a,1,2))]. 64 c1 ^ (c2 ^ x) = c1 ^ x. [para(23(a,1),16(a,1,1)),flip(a)]. 81 1 ^ x = x. [para(39(a,1),15(a,1)),flip(a)]. 92 0 v x = x. [para(42(a,1),13(a,1)),flip(a)]. 99 1 v x = 1. [para(81(a,1),17(a,1))]. 100 x v (x ' v y) = 1. [back_demod(37),demod(99(5))]. 102 0 ^ x = 0. [para(92(a,1),17(a,1,2))]. 104 x ^ (x ' ^ y) = 0. [back_demod(40),demod(102(5))]. 113 x v 1 = 1. [para(99(a,1),13(a,1)),flip(a)]. 116 x ^ 0 = 0. [para(102(a,1),15(a,1)),flip(a)]. 132 c1 v c2 = c2. [para(23(a,1),33(a,1,2)),demod(13(3))]. 153 c1 ^ (c1 ' v c2 ') != 0. [ur(21,a,100,a,c,24,a(flip))]. 167 x ^ (x v y) ' = 0. [para(20(a,1),29(a,1,2)),demod(116(2)),flip(a)]. 186 c1 ^ c2 ' = 0. [para(132(a,1),167(a,1,2,1))]. 189 c1 ^ (x v (c2 ' ^ (c1 v y))) = c1 ^ (x v (c2 ' ^ (x v y))). [para(186(a,1),22(a,1,2,2,1)),demod(92(7)),flip(a)]. 220 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(64(a,1),33(a,1,2)),demod(13(5))]. 227 x v (x ^ y) ' = 1. [para(19(a,1),31(a,1,2)),demod(113(2)),flip(a)]. 268 x v (y ^ x) ' = 1. [para(15(a,1),227(a,1,2,1))]. 284 (c2 ^ x) v (c1 ^ x) ' = 1. [para(64(a,1),268(a,1,2,1))]. 1610 (c2 ^ (c1 v x)) v c1 ' = 1. [para(17(a,1),284(a,1,2,1))]. 2649 c1 ' v (c2 ^ (c1 v x)) = 1. [para(1610(a,1),13(a,1)),flip(a)]. 4460 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(17(a,1),220(a,1,1))]. 10644 c1 ^ (c1 ' v c2 ') = 0. [para(2649(a,1),189(a,2,2,2,2)),demod(4460(11),26(10),104(10),13(5),92(5),20(4),15(8),81(8)),flip(a)]. 10645 $F. [resolve(10644,a,153,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=411. Generated=121763. Kept=10632. proofs=1. Usable=409. Sos=9783. Demods=7401. Denials=0. Limbo=38, Disabled=413. Hints=0. Weight_deleted=40. Literals_deleted=0. Forward_subsumed=105735. Back_subsumed=64. Sos_limit_deleted=5356. Sos_displaced=0. Sos_removed=0. New_demodulators=7645 (4 lex), Back_demodulated=337. Back_unit_deleted=0. Demod_attempts=2032212. Demod_rewrites=401165. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=122780. Nonunit_bsub_feature_tests=51826. Megabytes=14.00. User_CPU=3.76, System_CPU=0.07, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13676 exit (max_proofs) Mon Jun 19 16:49:49 2006