============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13802 was started by mccune on cleo.thornwood, Mon Jun 19 16:51:07 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H7b.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 H7b.in assign(max_weight,25). assign(constant_weight,0). assign(nest_penalty,2). clauses(sos). x ^ (y v (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7). 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 (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7). [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 ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)) # label(H7). [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 ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)) # label(H7). [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=15): 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=15): 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=5): 19 x v x ' = 1. [input]. given #8 (I,wt=5): 20 x ^ x ' = 0. [input]. given #9 (I,wt=12): 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=23): 22 x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)) # label(H7). [copy(10),flip(a)]. given #11 (I,wt=2): 23 c1 ^ c2 = c1. [clausify]. given #12 (I,wt=5): 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. given #13 (F,wt=4): 39 x ^ 1 = x. [para(19(a,1),17(a,1,2))]. given #14 (T,wt=4): 42 x v 0 = x. [para(20(a,1),18(a,1,2))]. given #15 (T,wt=4): 57 1 ^ x = x. [para(39(a,1),15(a,1)),flip(a)]. given #16 (A,wt=15): 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=2): 63 1 ' = 0. [hyper(21,a,42,a,b,57,a)]. given #18 (F,wt=3): 64 1 v x = 1. [para(57(a,1),17(a,1))]. given #19 (T,wt=3): 72 x v 1 = 1. [para(64(a,1),13(a,1)),flip(a)]. given #20 (T,wt=2): 75 0 ' = 1. [hyper(21,a,72,a,b,39,a)]. given #21 (A,wt=15): 26 x ^ (y ^ z) = y ^ (x ^ z). [para(15(a,1),16(a,1,1)),demod(16(2))]. given #22 (F,wt=4): 60 0 v x = x. [para(42(a,1),13(a,1)),flip(a)]. given #23 (F,wt=3): 81 0 ^ x = 0. [para(60(a,1),17(a,1,2))]. given #24 (T,wt=3): 83 x ^ 0 = 0. [para(81(a,1),15(a,1)),flip(a)]. given #25 (T,wt=5): 35 x ^ x = x. [para(18(a,1),17(a,1,2))]. given #26 (A,wt=7): 27 x ^ (y v x) = x. [para(13(a,1),17(a,1,2))]. given #27 (F,wt=5): 36 x v x = x. [para(17(a,1),18(a,1,2))]. given #28 (F,wt=5): 55 c1 v c2 != 1 | c1 != 0 | c1 ' = c2. [para(23(a,1),21(b,1))]. given #29 (T,wt=5): 56 c1 ^ (c2 v (c1 ^ x)) = c1. [para(23(a,1),22(a,1,2,2,2,1)),demod(17(10),13(4),17(5)),flip(a)]. given #30 (T,wt=5): 74 0 != x | x ' = 1. [back_demod(58),demod(72(2)),xx(a)]. given #31 (A,wt=15): 28 (x v y) ^ (x v (y v z)) = x v y. [para(14(a,1),17(a,1,2))]. given #32 (F,wt=5): 87 1 != x | x ' = 0. [back_demod(61),demod(83(4)),xx(b)]. given #33 (F,wt=5): 103 c1 ^ (c2 v (x ^ c1)) = c1. [para(15(a,1),56(a,1,2,2))]. given #34 (T,wt=7): 33 x v (y ^ x) = x. [para(15(a,1),18(a,1,2))]. given #35 (T,wt=2): 124 c1 v c2 = c2. [para(23(a,1),33(a,1,2)),demod(13(3))]. given #36 (A,wt=13): 29 x ^ ((x v y) ^ z) = x ^ z. [para(17(a,1),16(a,1,1)),flip(a)]. given #37 (F,wt=4): 127 c2 v (c1 ^ x) = c2. [para(56(a,1),33(a,1,2)),demod(13(6),69(6),13(3),124(3)),flip(a)]. given #38 (F,wt=4): 129 c2 v (x ^ c1) = c2. [para(103(a,1),33(a,1,2)),demod(13(6),125(6),13(3),124(3)),flip(a)]. given #39 (T,wt=4): 130 c2 != 1 | c1 != 0 | c1 ' = c2. [back_demod(105),demod(124(3),127(12))]. given #40 (T,wt=7): 136 x ^ (x v y) ' = 0. [para(20(a,1),29(a,1,2)),demod(83(2)),flip(a)]. given #41 (A,wt=15): 30 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(17(a,1),16(a,1)),flip(a)]. given #42 (F,wt=3): 158 c1 ^ c2 ' = 0. [para(124(a,1),136(a,1,2,1))]. given #43 (F,wt=6): 166 c1 v c2 ' != 1 | c2 ' = c1 '. [para(158(a,1),21(b,1)),flip(c),xx(b)]. given #44 (T,wt=7): 151 x ^ (y v x) ' = 0. [para(13(a,1),136(a,1,2,1))]. given #45 (T,wt=7): 165 c1 ^ (c2 ' ^ x) = 0. [para(158(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #46 (A,wt=13): 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): 167 c1 ^ (x ^ c2 ') = 0. [para(158(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #48 (F,wt=7): 179 x v (x ^ y) ' = 1. [para(19(a,1),31(a,1,2)),demod(72(2)),flip(a)]. given #49 (T,wt=7): 190 x v (y ^ x) ' = 1. [para(15(a,1),179(a,1,2,1))]. given #50 (T,wt=3): 200 c2 v c1 ' = 1. [para(23(a,1),190(a,1,2,1))]. given #51 (A,wt=15): 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=6): 207 c2 ^ c1 ' != 0 | c2 ' = c1 '. [para(200(a,1),21(a,1)),xx(a)]. given #53 (F,wt=7): 206 c2 v (c1 ' v x) = 1. [para(200(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #54 (T,wt=7): 209 c2 v (x v c1 ') = 1. [para(200(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #55 (T,wt=8): 53 c1 ^ (c2 ^ x) = c1 ^ x. [para(23(a,1),16(a,1,1)),flip(a)]. given #56 (A,wt=15): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(16(a,1),18(a,1,2))]. given #57 (F,wt=4): 224 c1 ^ (c2 v x) = c1. [para(17(a,1),53(a,1,2)),demod(23(3)),flip(a)]. given #58 (F,wt=4): 230 c1 ^ (x v c2) = c1. [para(27(a,1),53(a,1,2)),demod(23(3)),flip(a)]. given #59 (T,wt=5): 233 c1 ^ (c2 v x) ' = 0. [para(136(a,1),53(a,1,2)),demod(15(3),81(3)),flip(a)]. given #60 (T,wt=5): 235 c1 ^ (x v c2) ' = 0. [para(151(a,1),53(a,1,2)),demod(15(3),81(3)),flip(a)]. given #61 (A,wt=11): 38 x v (y v (x v y) ') = 1. [para(19(a,1),14(a,1)),flip(a)]. given #62 (F,wt=7): 236 (c2 ^ x) v (c1 ^ x) ' = 1. [para(53(a,1),190(a,1,2,1))]. given #63 (F,wt=5): 279 c2 v (c1 ^ x) ' = 1. [para(236(a,1),31(a,1,2)),demod(13(3),64(3)),flip(a)]. given #64 (T,wt=5): 281 c2 v (x ^ c1) ' = 1. [para(15(a,1),279(a,1,2,1))]. given #65 (T,wt=6): 270 (c2 ^ (c1 v x)) v c1 ' = 1. [para(17(a,1),236(a,1,2,1))]. given #66 (A,wt=11): 41 x ^ (y ^ (x ^ y) ') = 0. [para(20(a,1),16(a,1)),flip(a)]. given #67 (F,wt=6): 276 (c2 ^ (x v c1)) v c1 ' = 1. [para(27(a,1),236(a,1,2,1))]. given #68 (F,wt=6): 291 c1 ' v (c2 ^ (c1 v x)) = 1. [para(270(a,1),13(a,1)),flip(a)]. given #69 (T,wt=6): 304 c1 ' v (c2 ^ (x v c1)) = 1. [para(276(a,1),13(a,1)),flip(a)]. given #70 (T,wt=7): 268 (x ^ c2) v (c1 ^ x) ' = 1. [para(15(a,1),236(a,1,1))]. given #71 (A,wt=12): 43 x v y != 1 | y ^ x != 0 | y ' = x. [para(13(a,1),21(a,1))]. given #72 (F,wt=4): 331 c2 != 1 | c1 != 0 | c2 ' = c1. [para(124(a,1),43(a,1)),demod(15(6),23(6))]. given #73 (F,wt=4): 337 c2 ^ c1 ' != 0 | c2 = c1. [para(200(a,1),43(a,1)),demod(15(7),326(12)),flip(c),xx(a)]. given #74 (T,wt=7): 269 (c2 ^ x) v (x ^ c1) ' = 1. [para(15(a,1),236(a,1,2,1))]. given #75 (T,wt=7): 318 (x ^ c2) v (x ^ c1) ' = 1. [para(15(a,1),268(a,1,2,1))]. 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=7): 326 x ' ' = x. [para(19(a,1),43(a,1)),demod(15(5),20(5)),xx(a),xx(b)]. given #78 (F,wt=8): 54 c2 ^ (x ^ c1) = x ^ c1. [para(23(a,1),16(a,2,2)),demod(15(4))]. given #79 (T,wt=8): 80 c1 ^ (x ^ c2) = x ^ c1. [para(23(a,1),26(a,1,2)),flip(a)]. given #80 (T,wt=8): 91 1 != x | 0 != x | x ' = x. [para(35(a,1),21(b,1)),demod(36(1)),flip(a),flip(b)]. given #81 (A,wt=12): 45 x v y != 1 | y ^ x != 0 | x ' = y. [para(15(a,1),21(b,1))]. given #82 (F,wt=4): 408 c1 v c2 ' != 1 | c2 = c1. [para(158(a,1),45(b,1)),demod(13(4),326(12)),xx(b)]. given #83 (F,wt=8): 131 c1 v (c2 v x) = c2 v x. [para(124(a,1),14(a,1,1)),flip(a)]. given #84 (T,wt=8): 132 c2 v (x v c1) = x v c2. [para(124(a,1),14(a,2,2)),demod(13(4))]. given #85 (T,wt=7): 433 (x v c1) ^ (x v c2) ' = 0. [para(132(a,1),151(a,1,2,1))]. 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=7): 441 (c1 v x) ^ (x v c2) ' = 0. [para(13(a,1),433(a,1,1))]. given #88 (F,wt=7): 442 (x v c1) ^ (c2 v x) ' = 0. [para(13(a,1),433(a,1,2,1))]. given #89 (T,wt=6): 486 (c1 v (c2 ^ x)) ^ c2 ' = 0. [para(18(a,1),442(a,1,2,1)),demod(13(4))]. given #90 (T,wt=6): 490 (c1 v (x ^ c2)) ^ c2 ' = 0. [para(33(a,1),442(a,1,2,1)),demod(13(4))]. given #91 (A,wt=23): 49 x ^ (y v (x ^ ((x ^ y) v (z ^ (y v x))))) = x ^ (y v (x ^ z)). [para(13(a,1),22(a,1,2,2,2,2,2))]. given #92 (F,wt=6): 495 c2 ' ^ (c1 v (c2 ^ x)) = 0. [para(486(a,1),15(a,1)),flip(a)]. given #93 (F,wt=6): 503 c2 ' ^ (c1 v (x ^ c2)) = 0. [para(490(a,1),15(a,1)),flip(a)]. given #94 (T,wt=7): 476 (c1 v x) ^ (c2 v x) ' = 0. [para(13(a,1),441(a,1,2,1))]. given #95 (T,wt=8): 133 c1 v (x v c2) = x v c2. [para(124(a,1),25(a,1,2)),flip(a)]. given #96 (A,wt=23): 50 x ^ (y v (x ^ ((y ^ x) v (z ^ (x v y))))) = x ^ (y v (x ^ z)). [para(15(a,1),22(a,1,2,2,2,1))]. given #97 (F,wt=8): 134 (x v c1) ^ (x v c2) = x v c1. [para(124(a,1),28(a,1,2,2))]. given #98 (F,wt=8): 142 c2 != 1 | c1 ^ x != 0 | c2 ' = c1 ^ x. [para(127(a,1),21(a,1)),demod(26(7),53(7))]. given #99 (T,wt=3): 572 c2 != 1 | c2 ' = 0. [para(20(a,1),142(b,1)),demod(20(12)),xx(b)]. given #100 (T,wt=8): 145 c2 v (x ^ (c1 ^ y)) = c2. [para(26(a,1),127(a,1,2))]. given #101 (A,wt=23): 51 x ^ (y v (x ^ ((x ^ y) v ((x v y) ^ z)))) = x ^ (y v (x ^ z)). [para(15(a,1),22(a,1,2,2,2,2))]. given #102 (F,wt=8): 147 c2 v (x ^ (y ^ c1)) = c2. [para(16(a,1),129(a,1,2))]. given #103 (F,wt=8): 148 c2 != 1 | x ^ c1 != 0 | c2 ' = x ^ c1. [para(129(a,1),21(a,1)),demod(54(7))]. given #104 (T,wt=8): 231 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(53(a,1),33(a,1,2)),demod(13(5))]. given #105 (T,wt=8): 243 c2 v x != 1 | c1 != 0 | c1 ' = c2 v x. [para(224(a,1),21(b,1)),demod(131(4))]. given #106 (A,wt=11): 65 x v (x v y) = x v y. [para(57(a,1),22(a,1,2,2,2,1)),demod(64(4),39(4),57(4),57(4),57(5),57(5))]. given #107 (F,wt=3): 617 c1 != 0 | c1 ' = 1. [para(19(a,1),243(a,1)),demod(19(12)),xx(a)]. given #108 (F,wt=8): 245 c1 ^ (x v (c2 v y)) = c1. [para(25(a,1),224(a,1,2))]. given #109 (T,wt=8): 247 c1 ^ (x v (y v c2)) = c1. [para(14(a,1),230(a,1,2))]. given #110 (T,wt=8): 249 x v c2 != 1 | c1 != 0 | c1 ' = x v c2. [para(230(a,1),21(b,1)),demod(133(4))]. given #111 (A,wt=9): 66 x v (x ' v y) = 1. [back_demod(37),demod(64(5))]. given #112 (F,wt=5): 641 c1 ^ (c1 ' v c2 ') != 0. [ur(45,a,66,a,c,24,a(flip)),demod(15(7))]. given #113 (F,wt=8): 332 c2 != 1 | c1 ^ x != 0 | (c1 ^ x) ' = c2. [para(127(a,1),43(a,1)),demod(15(7),26(7),53(7))]. given #114 (T,wt=8): 333 c2 != 1 | x ^ c1 != 0 | (x ^ c1) ' = c2. [para(129(a,1),43(a,1)),demod(15(7),54(7))]. given #115 (T,wt=8): 344 c2 ^ (c1 ^ x) ' != 0 | c1 ^ x = c2. [para(279(a,1),43(a,1)),demod(15(8),326(14)),xx(a)]. given #116 (A,wt=12): 67 x v y != 1 | 0 != x | x ' = x v y. [back_demod(47),demod(65(2))]. given #117 (F,wt=3): 655 c2 != 0 | c2 ' = 1. [para(200(a,1),67(a,1)),demod(200(12)),flip(b),xx(a)]. given #118 (F,wt=3): 656 c1 ' != 0 | c1 = 1. [para(291(a,1),67(a,1)),demod(326(10),291(15)),flip(b),xx(a)]. given #119 (T,wt=4): 654 c2 != 1 | c2 != 0 | c2 ' = c2. [para(127(a,1),67(a,1)),demod(127(12)),flip(b)]. given #120 (T,wt=8): 345 c2 ^ (x ^ c1) ' != 0 | x ^ c1 = c2. [para(281(a,1),43(a,1)),demod(15(8),326(14)),xx(a)]. given #121 (A,wt=11): 68 x ^ (y v (x v z)) = x. [para(25(a,1),17(a,1,2))]. given #122 (F,wt=8): 393 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(54(a,1),34(a,1,2))]. given #123 (F,wt=8): 398 (x ^ c1) v (x ^ c2) = x ^ c2. [para(80(a,1),33(a,1,2)),demod(13(5))]. given #124 (T,wt=8): 399 (c1 ^ x) v (x ^ c1) = c1 ^ x. [para(80(a,1),34(a,1,2))]. given #125 (T,wt=8): 414 c2 v x != 1 | c1 != 0 | (c2 v x) ' = c1. [para(224(a,1),45(b,1)),demod(13(4),131(4))]. given #126 (A,wt=13): 69 x v (y v (x ^ z)) = y v x. [para(18(a,1),25(a,1,2)),flip(a)]. given #127 (F,wt=8): 415 x v c2 != 1 | c1 != 0 | (x v c2) ' = c1. [para(230(a,1),45(b,1)),demod(13(4),133(4))]. given #128 (F,wt=8): 416 c1 v (c2 v x) ' != 1 | c2 v x = c1. [para(233(a,1),45(b,1)),demod(13(5),326(14)),xx(b)]. given #129 (T,wt=8): 417 c1 v (x v c2) ' != 1 | x v c2 = c1. [para(235(a,1),45(b,1)),demod(13(5),326(14)),xx(b)]. given #130 (T,wt=8): 428 c2 v (x v c1) = c2 v x. [para(132(a,2),13(a,1))]. given #131 (A,wt=20): 71 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(25(a,1),21(a,1))]. given #132 (F,wt=8): 438 x v c2 != 1 | c1 != 0 | (c2 v x) ' = c1. [para(132(a,1),44(a,1)),demod(15(8),224(8))]. given #133 (F,wt=8): 474 c2 != 1 | x ^ c1 != 0 | (c1 ^ x) ' = c2. [para(80(a,1),46(b,1)),demod(13(4),127(4))]. given #134 (T,wt=8): 541 (c1 v x) ^ (x v c2) = c1 v x. [para(133(a,1),28(a,1,2))]. given #135 (T,wt=8): 558 (x v c1) ^ (c2 v x) = x v c1. [para(13(a,1),134(a,1,2))]. given #136 (A,wt=9): 73 x v (y v x ') = 1. [back_demod(70),demod(72(5))]. given #137 (F,wt=8): 571 c2 != 1 | x ^ c1 != 0 | c2 ' = c1 ^ x. [para(15(a,1),142(b,1))]. given #138 (F,wt=8): 598 c2 != 1 | c1 ^ x != 0 | c2 ' = x ^ c1. [para(15(a,1),148(b,1))]. given #139 (T,wt=8): 602 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(15(a,1),231(a,1,1))]. given #140 (T,wt=8): 603 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(15(a,1),231(a,1,2))]. given #141 (A,wt=13): 76 x ^ (y ^ (x v z)) = y ^ x. [para(17(a,1),26(a,1,2)),flip(a)]. given #142 (F,wt=8): 604 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(17(a,1),231(a,1,1))]. given #143 (F,wt=6): 843 c1 ^ (c2 ^ (c1 v x)) ' = 0. [para(604(a,1),136(a,1,2,1))]. given #144 (T,wt=6): 848 c1 ^ (c2 ^ (x v c1)) ' = 0. [para(13(a,1),843(a,1,2,1,2))]. given #145 (T,wt=7): 846 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(604(a,1),68(a,1,2,2))]. given #146 (A,wt=11): 77 x v (y ^ (x ^ z)) = x. [para(26(a,1),18(a,1,2))]. given #147 (F,wt=7): 861 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(13(a,1),846(a,1,2,2,2))]. given #148 (F,wt=7): 862 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(13(a,1),846(a,1,2))]. given #149 (T,wt=7): 884 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(13(a,1),861(a,1,2))]. given #150 (T,wt=8): 609 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(27(a,1),231(a,1,1))]. given #151 (A,wt=20): 79 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(26(a,1),21(b,1))]. given #152 (F,wt=8): 616 x v c2 != 1 | c1 != 0 | c1 ' = c2 v x. [para(13(a,1),243(a,1))]. given #153 (F,wt=8): 639 c2 v x != 1 | c1 != 0 | c1 ' = x v c2. [para(13(a,1),249(a,1))]. given #154 (T,wt=8): 648 c2 != 1 | c1 ^ x != 0 | (x ^ c1) ' = c2. [para(15(a,1),333(b,1))]. given #155 (T,wt=8): 650 c2 ^ (x ^ c1) ' != 0 | c1 ^ x = c2. [para(15(a,1),344(a,1,2,1))]. given #156 (A,wt=9): 82 x ^ (x ' ^ y) = 0. [back_demod(40),demod(81(5))]. given #157 (F,wt=8): 657 c2 ^ (c1 ^ x) ' != 0 | x ^ c1 = c2. [para(15(a,1),345(a,1,2,1))]. given #158 (F,wt=8): 714 c2 v x != 1 | c1 != 0 | (x v c2) ' = c1. [para(13(a,1),415(a,1))]. given #159 (T,wt=8): 716 c1 v (x v c2) ' != 1 | c2 v x = c1. [para(13(a,1),416(a,1,2,1))]. given #160 (T,wt=8): 718 c1 v (c2 v x) ' != 1 | x v c2 = c1. [para(13(a,1),417(a,1,2,1))]. given #161 (A,wt=9): 85 x ^ (y ^ x ') = 0. [back_demod(78),demod(83(5))]. given #162 (F,wt=8): 727 c2 v x != 1 | c2 != 0 | c2 ' = c2 v x. [para(428(a,1),67(a,1)),demod(428(13)),flip(b)]. given #163 (F,wt=8): 739 c1 ' ^ (c2 v x) != 0 | c2 v x = c1. [para(206(a,1),71(a,1)),demod(326(13)),flip(c),xx(a)]. given #164 (T,wt=8): 764 (c1 v x) ^ (c2 v x) = c1 v x. [para(13(a,1),541(a,1,2))]. given #165 (T,wt=8): 765 (x v c2) ^ (c1 v x) = c1 v x. [para(541(a,1),15(a,1)),flip(a)]. given #166 (A,wt=11): 88 x ^ (x ^ y) = x ^ y. [para(35(a,1),16(a,1,1)),flip(a)]. given #167 (F,wt=8): 780 (c2 v x) ^ (x v c1) = x v c1. [para(558(a,1),15(a,1)),flip(a)]. given #168 (F,wt=8): 782 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(18(a,1),558(a,1,2)),demod(13(4),15(6),13(10))]. given #169 (T,wt=6): 1032 c2 v (c1 v (c2 ^ x)) ' = 1. [para(782(a,1),179(a,1,2,1))]. given #170 (T,wt=6): 1041 c2 v (c1 v (x ^ c2)) ' = 1. [para(15(a,1),1032(a,1,2,1,2))]. given #171 (A,wt=11): 90 x ^ (y ^ x) = y ^ x. [para(35(a,1),16(a,2,2)),demod(15(2))]. given #172 (F,wt=7): 1038 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(782(a,1),77(a,1,2,2))]. given #173 (F,wt=7): 1064 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(15(a,1),1038(a,1,2,2,2))]. given #174 (T,wt=7): 1065 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(15(a,1),1038(a,1,2))]. given #175 (T,wt=7): 1076 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(15(a,1),1064(a,1,2))]. given #176 (A,wt=12): 92 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(48),demod(88(4))]. given #177 (F,wt=3): 1114 c1 != 1 | c1 ' = 0. [para(158(a,1),92(b,1)),demod(158(12)),flip(a),xx(b)]. given #178 (F,wt=3): 1117 c2 ' != 1 | c2 = 0. [para(495(a,1),92(b,1)),demod(326(10),495(15)),flip(a),xx(b)]. given #179 (T,wt=4): 1112 c1 != 1 | c1 != 0 | c1 ' = c1. [para(23(a,1),92(b,1)),demod(23(11)),flip(a)]. given #180 (T,wt=8): 788 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(33(a,1),558(a,1,2)),demod(13(4),15(6),13(10))]. given #181 (A,wt=11): 93 x ^ (y v (z v x)) = x. [para(14(a,1),27(a,1,2))]. given #182 (F,wt=8): 811 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(603(a,1),13(a,1)),flip(a)]. given #183 (F,wt=8): 935 c2 ' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(165(a,1),79(b,1)),demod(326(13)),flip(c),xx(b)]. given #184 (T,wt=8): 987 x v c2 != 1 | c2 != 0 | c2 ' = c2 v x. [para(13(a,1),727(a,1))]. given #185 (T,wt=8): 989 x v c2 != 1 | c2 != 0 | c2 ' = x v c2. [para(69(a,1),727(a,1)),demod(69(14))]. given #186 (A,wt=13): 94 x ^ ((y v x) ^ z) = x ^ z. [para(27(a,1),16(a,1,1)),flip(a)]. given #187 (F,wt=8): 990 c1 ' ^ (x v c2) != 0 | c2 v x = c1. [para(13(a,1),739(a,1,2))]. given #188 (F,wt=8): 991 (c2 v x) ^ c1 ' != 0 | c2 v x = c1. [para(15(a,1),739(a,1))]. given #189 (T,wt=8): 994 c1 ' ^ (x v c2) != 0 | x v c2 = c1. [para(69(a,1),739(a,1,2)),demod(69(12))]. given #190 (T,wt=8): 1115 c1 != 1 | c1 ^ x != 0 | c1 ' = c1 ^ x. [para(53(a,1),92(b,1)),demod(53(13)),flip(a)]. given #191 (A,wt=15): 95 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(27(a,1),16(a,1)),flip(a)]. given #192 (F,wt=8): 1116 c1 != 1 | x ^ c1 != 0 | c1 ' = x ^ c1. [para(80(a,1),92(b,1)),demod(80(13)),flip(a)]. given #193 (F,wt=8): 1158 (c1 ^ x) v c2 ' != 1 | c1 ^ x = c2. [para(13(a,1),935(a,1))]. given #194 (T,wt=8): 1159 c2 ' v (x ^ c1) != 1 | c1 ^ x = c2. [para(15(a,1),935(a,1,2))]. given #195 (T,wt=8): 1161 c2 ' v (x ^ c1) != 1 | x ^ c1 = c2. [para(80(a,1),935(a,1,2)),demod(80(11))]. given #196 (A,wt=15): 97 (x v y) ^ (x v (z v y)) = x v y. [para(25(a,1),27(a,1,2))]. given #197 (F,wt=8): 1163 c2 v x != 1 | c2 != 0 | c2 ' = x v c2. [para(13(a,1),989(a,1))]. given #198 (F,wt=8): 1184 (x v c2) ^ c1 ' != 0 | c2 v x = c1. [para(15(a,1),990(a,1))]. given #199 (T,wt=8): 1186 (x v c2) ^ c1 ' != 0 | x v c2 = c1. [para(69(a,1),991(a,1,1)),demod(69(12))]. given #200 (T,wt=8): 1187 c1 ' ^ (c2 v x) != 0 | x v c2 = c1. [para(13(a,1),994(a,1,2))]. given #201 (A,wt=13): 98 x ^ (y ^ (z v x)) = y ^ x. [para(27(a,1),26(a,1,2)),flip(a)]. given #202 (F,wt=8): 1188 c1 != 1 | x ^ c1 != 0 | c1 ' = c1 ^ x. [para(15(a,1),1115(b,1))]. given #203 (F,wt=8): 1203 x ^ (c1 v (x ^ c2)) = x ^ c2. [para(788(a,1),95(a,1,2))]. given #204 (T,wt=8): 1207 c1 != 1 | c1 ^ x != 0 | c1 ' = x ^ c1. [para(15(a,1),1116(b,1))]. given #205 (T,wt=8): 1209 (x ^ c1) v c2 ' != 1 | c1 ^ x = c2. [para(15(a,1),1158(a,1,1))]. given #206 (A,wt=11): 100 x v (y v x) = y v x. [para(36(a,1),14(a,2,2)),demod(13(2))]. given #207 (F,wt=8): 1211 (x ^ c1) v c2 ' != 1 | x ^ c1 = c2. [para(80(a,1),1158(a,1,1)),demod(80(11))]. given #208 (F,wt=8): 1213 c2 ' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(15(a,1),1161(a,1,2))]. given #209 (T,wt=8): 1234 (c2 v x) ^ c1 ' != 0 | x v c2 = c1. [para(13(a,1),1186(a,1,1))]. given #210 (T,wt=8): 1247 x ^ (c1 v (c2 ^ x)) = x ^ c2. [para(15(a,1),1203(a,1,2,2))]. given #211 (A,wt=12): 102 x v y != 1 | 0 != y | y ' = x v y. [back_demod(96),demod(100(2))]. given #212 (F,wt=5): 1275 x ' != 0 | 1 = x. [para(19(a,1),102(a,1)),demod(326(8),19(8)),flip(b),flip(c),xx(a)]. given #213 (F,wt=8): 1261 (c1 ^ x) v c2 ' != 1 | x ^ c1 = c2. [para(15(a,1),1211(a,1,1))]. given #214 (T,wt=9): 252 c1 ^ ((c2 v x) ' ^ y) = 0. [para(233(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #215 (T,wt=9): 254 c1 ^ (x v (c2 v y)) ' = 0. [para(25(a,1),233(a,1,2,1))]. given #216 (A,wt=15): 109 (x v y) ^ (y v (x v z)) = y v x. [para(13(a,1),28(a,1,1))]. given #217 (F,wt=9): 255 c1 ^ (x ^ (c2 v y) ') = 0. [para(233(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #218 (F,wt=9): 256 c1 ^ (x v (y v c2)) ' = 0. [para(14(a,1),235(a,1,2,1))]. given #219 (T,wt=9): 257 c1 ^ ((x v c2) ' ^ y) = 0. [para(235(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #220 (T,wt=9): 259 c1 ^ (x ^ (y v c2) ') = 0. [para(235(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #221 (A,wt=15): 110 (x v y) ^ (y v (z v x)) = x v y. [para(13(a,1),28(a,1,2)),demod(14(3))]. given #222 (F,wt=7): 1363 c1 ' v (x v c2) = 1. [para(200(a,1),110(a,1,1)),demod(57(7),200(9))]. given #223 (F,wt=9): 280 c2 v ((c1 ^ x) ' v y) = 1. [para(279(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #224 (T,wt=9): 284 c2 v (x v (c1 ^ y) ') = 1. [para(279(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #225 (T,wt=9): 285 c2 v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),279(a,1,2,1))]. given #226 (A,wt=21): 111 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(28(a,1),16(a,1,1)),flip(a)]. given #227 (F,wt=9): 286 c2 v ((x ^ c1) ' v y) = 1. [para(281(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #228 (F,wt=9): 287 c2 v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),281(a,1,2,1))]. given #229 (T,wt=9): 290 c2 v (x v (y ^ c1) ') = 1. [para(281(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #230 (T,wt=9): 303 c1 ^ (x ^ (c2 ^ x) ') = 0. [para(41(a,1),53(a,1,2)),demod(15(3),81(3)),flip(a)]. given #231 (A,wt=19): 112 (x v y) ^ (x v (z v (y v u))) = x v y. [para(25(a,1),28(a,1,2,2))]. given #232 (F,wt=9): 363 x v y != 0 | (x v y) ' = 1. [para(39(a,1),44(b,1)),demod(72(2),72(2)),xx(a)]. given #233 (F,wt=9): 364 x v y != 1 | (x v y) ' = 0. [para(42(a,1),44(a,1,2)),demod(15(6),81(6)),xx(b)]. given #234 (T,wt=9): 453 x ^ y != 0 | (x ^ y) ' = 1. [para(39(a,1),46(b,1,2)),demod(13(3),64(3)),xx(a)]. given #235 (T,wt=9): 454 x ^ y != 1 | (x ^ y) ' = 0. [para(42(a,1),46(a,1)),demod(83(5),83(5)),xx(b)]. given #236 (A,wt=21): 113 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(28(a,1),26(a,1,2)),flip(a)]. given #237 (F,wt=9): 566 x v (c2 v (x v c1) ') = 1. [para(134(a,1),190(a,1,2,1)),demod(14(6))]. given #238 (F,wt=9): 675 x ^ (c1 ^ (c2 ^ x) ') = 0. [para(393(a,1),151(a,1,2,1)),demod(16(6))]. given #239 (T,wt=9): 688 x ^ (c1 ^ (x ^ c2) ') = 0. [para(398(a,1),136(a,1,2,1)),demod(16(6))]. given #240 (T,wt=9): 772 x v (c2 v (c1 v x) ') = 1. [para(541(a,1),190(a,1,2,1)),demod(14(6))]. given #241 (A,wt=13): 119 x v ((y ^ x) v z) = x v z. [para(33(a,1),14(a,1,1)),flip(a)]. given #242 (F,wt=9): 774 c2 v (x v (c1 v x) ') = 1. [para(38(a,1),541(a,1,1)),demod(13(7),57(8),38(12))]. given #243 (F,wt=9): 790 c2 v (x v (x v c1) ') = 1. [para(558(a,1),190(a,1,2,1)),demod(14(6))]. given #244 (T,wt=9): 801 x ' v (y v x) = 1. [para(326(a,1),73(a,1,2,2))]. given #245 (T,wt=7): 1650 (c2 ^ x) v (x ^ c2) ' = 1. [para(603(a,1),801(a,1,2)),demod(13(6))]. given #246 (A,wt=15): 120 x v (y v (z ^ (x v y))) = x v y. [para(33(a,1),14(a,1)),flip(a)]. given #247 (F,wt=8): 1651 c2 v (x ^ (c1 v (c2 ^ y))) ' = 1. [para(1038(a,1),801(a,1,2)),demod(13(8))]. given #248 (F,wt=8): 1652 c2 v (x ^ (c1 v (y ^ c2))) ' = 1. [para(1064(a,1),801(a,1,2)),demod(13(8))]. given #249 (T,wt=8): 1653 c2 v ((c1 v (c2 ^ x)) ^ y) ' = 1. [para(1065(a,1),801(a,1,2)),demod(13(8))]. given #250 (T,wt=8): 1654 c2 v ((c1 v (x ^ c2)) ^ y) ' = 1. [para(1076(a,1),801(a,1,2)),demod(13(8))]. given #251 (A,wt=11): 121 x v (y ^ (z ^ x)) = x. [para(16(a,1),33(a,1,2))]. given #252 (F,wt=8): 1677 x v (c2 ^ (x v c1)) = x v c1. [para(609(a,1),120(a,1,2))]. given #253 (F,wt=8): 1753 x v (c2 ^ (c1 v x)) = x v c1. [para(13(a,1),1677(a,1,2,2))]. given #254 (T,wt=9): 869 (c2 ^ (x v (c2 ^ (c1 v y)))) v c1 ' = 1. [para(846(a,1),236(a,1,2,1))]. given #255 (T,wt=9): 893 (c2 ^ (x v (c2 ^ (y v c1)))) v c1 ' = 1. [para(861(a,1),236(a,1,2,1))]. given #256 (A,wt=12): 122 1 != x | y ^ x != 0 | x ' = y ^ x. [para(33(a,1),21(a,1)),demod(90(4)),flip(a)]. given #257 (F,wt=5): 1817 x ' != 1 | 0 = x. [para(20(a,1),122(b,1)),demod(326(8),20(8)),flip(a),flip(c),xx(b)]. given #258 (F,wt=6): 1831 (c1 ^ (c1 ' v c2 ')) ' != 1. [ur(1817,b,641,a(flip))]. given #259 (T,wt=9): 904 (c2 ^ ((c2 ^ (c1 v x)) v y)) v c1 ' = 1. [para(862(a,1),236(a,1,2,1))]. given #260 (T,wt=9): 914 (c2 ^ ((c2 ^ (x v c1)) v y)) v c1 ' = 1. [para(884(a,1),236(a,1,2,1))]. given #261 (A,wt=13): 125 x v (y v (z ^ x)) = y v x. [para(33(a,1),25(a,1,2)),flip(a)]. given #262 (F,wt=9): 980 x ' ^ (y ^ x) = 0. [para(326(a,1),85(a,1,2,2))]. given #263 (F,wt=8): 1892 c1 ^ (x v (c2 ^ (c1 v y))) ' = 0. [para(846(a,1),980(a,1,2)),demod(15(8))]. given #264 (T,wt=8): 1893 c1 ^ (x v (c2 ^ (y v c1))) ' = 0. [para(861(a,1),980(a,1,2)),demod(15(8))]. given #265 (T,wt=8): 1894 c1 ^ ((c2 ^ (c1 v x)) v y) ' = 0. [para(862(a,1),980(a,1,2)),demod(15(8))]. given #266 (A,wt=15): 126 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(26(a,1),33(a,1,2))]. given #267 (F,wt=8): 1895 c1 ^ ((c2 ^ (x v c1)) v y) ' = 0. [para(884(a,1),980(a,1,2)),demod(15(8))]. given #268 (F,wt=9): 1071 (c1 v (x ^ (c1 v (c2 ^ y)))) ^ c2 ' = 0. [para(1038(a,1),442(a,1,2,1)),demod(13(7))]. given #269 (T,wt=9): 1085 (c1 v (x ^ (c1 v (y ^ c2)))) ^ c2 ' = 0. [para(1064(a,1),442(a,1,2,1)),demod(13(7))]. given #270 (T,wt=9): 1096 (c1 v ((c1 v (c2 ^ x)) ^ y)) ^ c2 ' = 0. [para(1065(a,1),442(a,1,2,1)),demod(13(7))]. given #271 (A,wt=23): 135 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(29(a,1),16(a,1)),demod(16(2)),flip(a)]. given #272 (F,wt=9): 1108 (c1 v ((c1 v (x ^ c2)) ^ y)) ^ c2 ' = 0. [para(1076(a,1),442(a,1,2,1)),demod(13(7))]. given #273 (F,wt=9): 1278 (x ^ y) ' != 0 | x ^ y = 1. [para(179(a,1),102(a,1)),demod(326(10),179(11)),flip(b),xx(a)]. given #274 (T,wt=9): 1368 (c1 ^ x) ' v (y v c2) = 1. [para(279(a,1),110(a,1,1)),demod(57(8),279(11))]. given #275 (T,wt=9): 1369 (x ^ c1) ' v (y v c2) = 1. [para(281(a,1),110(a,1,1)),demod(57(8),281(11))]. given #276 (A,wt=20): 137 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(29(a,1),21(b,1))]. given #277 (F,wt=8): 2048 c2 != 1 | c2 ^ x != 0 | c2 ' = c2 ^ x. [para(127(a,1),137(a,1,2,1)),demod(18(4),127(13))]. given #278 (F,wt=8): 2059 c1 v x != 1 | c1 != 0 | c1 ' = c1 v x. [para(541(a,1),137(a,1,2)),demod(65(4),230(8),541(14))]. given #279 (T,wt=8): 2073 c2 != 1 | x ^ c2 != 0 | c2 ' = c2 ^ x. [para(15(a,1),2048(b,1))]. given #280 (T,wt=8): 2075 c2 != 1 | x ^ c2 != 0 | c2 ' = x ^ c2. [para(76(a,1),2048(b,1)),demod(76(14))]. given #281 (A,wt=17): 138 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(25(a,1),29(a,1,2,1))]. given #282 (F,wt=8): 2076 x v c1 != 1 | c1 != 0 | c1 ' = c1 v x. [para(13(a,1),2059(a,1))]. given #283 (F,wt=8): 2078 x v c1 != 1 | c1 != 0 | c1 ' = x v c1. [para(69(a,1),2059(a,1)),demod(69(14))]. given #284 (T,wt=8): 2080 c2 != 1 | c2 ^ x != 0 | c2 ' = x ^ c2. [para(15(a,1),2075(b,1))]. given #285 (T,wt=8): 2104 c1 v x != 1 | c1 != 0 | c1 ' = x v c1. [para(13(a,1),2078(a,1))]. given #286 (A,wt=21): 139 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(29(a,1),26(a,1,2)),flip(a)]. given #287 (F,wt=9): 1461 c1 ^ (x ^ (x ^ c2) ') = 0. [para(15(a,1),303(a,1,2,2,1))]. given #288 (F,wt=9): 1517 x v y != 0 | (y v x) ' = 1. [para(13(a,1),363(a,1))]. given #289 (T,wt=9): 1519 x v y != 1 | (y v x) ' = 0. [para(13(a,1),364(a,1))]. given #290 (T,wt=9): 1521 x ^ y != 0 | (y ^ x) ' = 1. [para(15(a,1),453(a,1))]. given #291 (A,wt=15): 140 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(29(a,1),33(a,1,2)),demod(13(4))]. given #292 (F,wt=8): 2190 c1 ^ ((c2 v x) ^ (c1 v y)) ' = 0. [para(140(a,1),1894(a,1,2,1))]. given #293 (F,wt=8): 2191 c1 ^ ((c2 v x) ^ (y v c1)) ' = 0. [para(140(a,1),1895(a,1,2,1))]. given #294 (T,wt=8): 2203 c1 ^ ((x v c2) ^ (c1 v y)) ' = 0. [para(13(a,1),2190(a,1,2,1,1))]. given #295 (T,wt=8): 2204 c1 ^ ((c1 v x) ^ (c2 v y)) ' = 0. [para(15(a,1),2190(a,1,2,1))]. given #296 (A,wt=10): 141 c2 v ((c1 ^ x) v y) = c2 v y. [para(127(a,1),14(a,1,1)),flip(a)]. given #297 (F,wt=8): 2211 c1 ^ ((c2 v x) ^ (c2 v y)) ' = 0. [para(131(a,1),2190(a,1,2,1,2))]. given #298 (F,wt=8): 2213 c1 ^ ((c2 v x) ^ (y v c2)) ' = 0. [para(133(a,1),2190(a,1,2,1,2))]. given #299 (T,wt=8): 2216 c1 ^ ((x v c2) ^ (y v c1)) ' = 0. [para(13(a,1),2191(a,1,2,1,1))]. given #300 (T,wt=8): 2218 c1 ^ ((x v c1) ^ (c2 v y)) ' = 0. [para(15(a,1),2191(a,1,2,1))]. given #301 (A,wt=17): 143 c2 ^ ((c1 ^ x) v (c2 ^ ((c1 ^ x) v (y ^ c2)))) = c2 ^ ((c1 ^ x) v (c2 ^ y)). [para(127(a,1),22(a,1,2,2,2,2,2)),demod(26(8),53(8))]. given #302 (F,wt=8): 2228 c1 ^ ((c1 v x) ^ (y v c2)) ' = 0. [para(15(a,1),2203(a,1,2,1))]. given #303 (F,wt=8): 2234 c1 ^ ((x v c2) ^ (c2 v y)) ' = 0. [para(131(a,1),2203(a,1,2,1,2))]. given #304 (T,wt=8): 2236 c1 ^ ((x v c2) ^ (y v c2)) ' = 0. [para(133(a,1),2203(a,1,2,1,2))]. given #305 (T,wt=8): 2286 c1 ^ ((x v c1) ^ (y v c2)) ' = 0. [para(15(a,1),2216(a,1,2,1))]. given #306 (A,wt=10): 144 c2 v (x v (c1 ^ y)) = x v c2. [para(127(a,1),25(a,1,2)),flip(a)]. given #307 (F,wt=9): 1523 x ^ y != 1 | (y ^ x) ' = 0. [para(15(a,1),454(a,1))]. given #308 (F,wt=9): 1790 c1 ' v (c2 ^ (x v (c2 ^ (c1 v y)))) = 1. [para(869(a,1),13(a,1)),flip(a)]. given #309 (T,wt=9): 1803 c1 ' v (c2 ^ (x v (c2 ^ (y v c1)))) = 1. [para(893(a,1),13(a,1)),flip(a)]. given #310 (T,wt=9): 1820 (x v y) ' != 1 | x v y = 0. [para(136(a,1),122(b,1)),demod(326(10),136(11)),flip(a),xx(b)]. given #311 (A,wt=10): 146 c2 v ((x ^ c1) v y) = c2 v y. [para(129(a,1),14(a,1,1)),flip(a)]. given #312 (F,wt=9): 1832 c1 ' v (c2 ^ ((c2 ^ (c1 v x)) v y)) = 1. [para(904(a,1),13(a,1)),flip(a)]. given #313 (F,wt=9): 1845 c1 ' v (c2 ^ ((c2 ^ (x v c1)) v y)) = 1. [para(914(a,1),13(a,1)),flip(a)]. given #314 (T,wt=9): 1960 c2 ' ^ (c1 v (x ^ (c1 v (c2 ^ y)))) = 0. [para(1071(a,1),15(a,1)),flip(a)]. given #315 (T,wt=9): 1970 c2 ' ^ (c1 v (x ^ (c1 v (y ^ c2)))) = 0. [para(1085(a,1),15(a,1)),flip(a)]. given #316 (A,wt=17): 149 c2 ^ ((x ^ c1) v (c2 ^ ((x ^ c1) v (y ^ c2)))) = c2 ^ ((x ^ c1) v (c2 ^ y)). [para(129(a,1),22(a,1,2,2,2,2,2)),demod(54(8))]. given #317 (F,wt=9): 1980 c2 ' ^ (c1 v ((c1 v (c2 ^ x)) ^ y)) = 0. [para(1096(a,1),15(a,1)),flip(a)]. given #318 (F,wt=9): 2018 c2 ' ^ (c1 v ((c1 v (x ^ c2)) ^ y)) = 0. [para(1108(a,1),15(a,1)),flip(a)]. given #319 (T,wt=9): 2028 (x ^ y) ' != 0 | y ^ x = 1. [para(15(a,1),1278(a,1,1))]. given #320 (T,wt=9): 2030 (x v y) ' != 0 | x v y = 1. [para(28(a,1),1278(a,1,1)),demod(28(8))]. given #321 (A,wt=10): 150 c2 v (x v (y ^ c1)) = x v c2. [para(129(a,1),25(a,1,2)),flip(a)]. given #322 (F,wt=3): 2460 c2 ' != 0 | c2 = 1. [para(124(a,1),2030(a,1,1)),demod(124(7))]. given #323 (F,wt=9): 2251 ((c1 ^ x) v y) ^ (c2 v y) ' = 0. [para(141(a,1),151(a,1,2,1))]. given #324 (T,wt=8): 2478 ((c1 ^ x) v (c2 ^ y)) ^ c2 ' = 0. [para(18(a,1),2251(a,1,2,1))]. given #325 (T,wt=8): 2484 ((c1 ^ x) v (y ^ c2)) ^ c2 ' = 0. [para(33(a,1),2251(a,1,2,1))]. given #326 (A,wt=13): 152 (x v y) ^ (x v (y v z)) ' = 0. [para(14(a,1),136(a,1,2,1))]. given #327 (F,wt=8): 2485 ((c1 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(127(a,1),2251(a,1,2,1))]. given #328 (F,wt=8): 2486 ((c1 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(129(a,1),2251(a,1,2,1))]. given #329 (T,wt=8): 2512 ((c2 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(13(a,1),2478(a,1,1))]. given #330 (T,wt=8): 2513 c2 ' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(2478(a,1),15(a,1)),flip(a)]. given #331 (A,wt=11): 153 x ^ ((x v y) ' ^ z) = 0. [para(136(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #332 (F,wt=8): 2514 ((x ^ c1) v (c2 ^ y)) ^ c2 ' = 0. [para(15(a,1),2478(a,1,1,1))]. given #333 (F,wt=8): 2526 ((x ^ c2) v (c1 ^ y)) ^ c2 ' = 0. [para(13(a,1),2484(a,1,1))]. given #334 (T,wt=8): 2527 c2 ' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(2484(a,1),15(a,1)),flip(a)]. given #335 (T,wt=8): 2528 ((x ^ c1) v (y ^ c2)) ^ c2 ' = 0. [para(15(a,1),2484(a,1,1,1))]. given #336 (A,wt=13): 154 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(136(a,1),16(a,1)),flip(a)]. given #337 (F,wt=8): 2555 c2 ' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(2485(a,1),15(a,1)),flip(a)]. given #338 (F,wt=8): 2556 ((x ^ c1) v (c1 ^ y)) ^ c2 ' = 0. [para(15(a,1),2485(a,1,1,1))]. given #339 (T,wt=8): 2567 c2 ' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(2486(a,1),15(a,1)),flip(a)]. given #340 (T,wt=7): 2689 c2 ' ^ (x ^ c1) = 0. [para(20(a,1),2567(a,1,2,1)),demod(60(6))]. given #341 (A,wt=14): 155 x v (x v y) ' != 1 | (x v y) ' = x '. [para(136(a,1),21(b,1)),flip(c),xx(b)]. given #342 (F,wt=3): 2705 c1 ' != 1 | c1 = 0. [para(291(a,1),155(a,1,2,1)),demod(63(4),13(4),60(4),291(11),63(6),326(8)),flip(b)]. given #343 (F,wt=8): 2568 ((x ^ c1) v (y ^ c1)) ^ c2 ' = 0. [para(15(a,1),2486(a,1,1,1))]. given #344 (T,wt=8): 2579 c2 ' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(2512(a,1),15(a,1)),flip(a)]. given #345 (T,wt=8): 2580 ((c2 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(15(a,1),2512(a,1,1,2))]. given #346 (A,wt=11): 156 x ^ (y v (x v z)) ' = 0. [para(25(a,1),136(a,1,2,1))]. given #347 (F,wt=8): 2591 c2 ' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(15(a,1),2513(a,1,2,1))]. given #348 (F,wt=8): 2619 c2 ' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(2526(a,1),15(a,1)),flip(a)]. given #349 (T,wt=8): 2620 ((x ^ c2) v (y ^ c1)) ^ c2 ' = 0. [para(15(a,1),2526(a,1,1,2))]. given #350 (T,wt=8): 2631 c2 ' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(15(a,1),2527(a,1,2,1))]. given #351 (A,wt=11): 157 x ^ (y ^ (x v z) ') = 0. [para(136(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #352 (F,wt=8): 2667 c2 ' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(15(a,1),2555(a,1,2,1))]. given #353 (F,wt=8): 2686 c2 ' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(15(a,1),2567(a,1,2,1))]. given #354 (T,wt=8): 2717 c2 ' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(15(a,1),2579(a,1,2,2))]. given #355 (T,wt=8): 2752 c2 ' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(15(a,1),2619(a,1,2,2))]. given #356 (A,wt=15): 159 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(15(a,1),30(a,1,2,2,1))]. given #357 (F,wt=9): 2355 (x v (c1 ^ y)) ^ (x v c2) ' = 0. [para(144(a,1),151(a,1,2,1))]. given #358 (F,wt=9): 2381 (x v y) ' != 1 | y v x = 0. [para(13(a,1),1820(a,1,1))]. given #359 (T,wt=9): 2383 (x ^ y) ' != 1 | x ^ y = 0. [para(34(a,1),1820(a,1,1)),demod(34(8))]. given #360 (T,wt=9): 2387 ((x ^ c1) v y) ^ (c2 v y) ' = 0. [para(146(a,1),151(a,1,2,1))]. given #361 (A,wt=24): 160 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x ' = y ^ ((x ^ y) v z). [para(30(a,1),21(b,1))]. given #362 (F,wt=7): 2899 c2 ^ c1 ' != 0 | c1 v (c2 ^ c1 ') = c1. [para(304(a,1),160(a,1)),demod(15(7),326(12),15(15),13(17),782(18)),flip(c),xx(a)]. given #363 (F,wt=9): 2458 (x v y) ' != 0 | y v x = 1. [para(13(a,1),2030(a,1,1))]. given #364 (T,wt=9): 2462 (x v (y ^ c1)) ^ (x v c2) ' = 0. [para(150(a,1),151(a,1,2,1))]. given #365 (T,wt=9): 2474 (x v (c1 ^ y)) ^ (c2 v x) ' = 0. [para(13(a,1),2251(a,1,1))]. given #366 (A,wt=19): 161 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(25(a,1),30(a,1,2,2))]. given #367 (F,wt=9): 2475 ((c1 ^ x) v y) ^ (y v c2) ' = 0. [para(13(a,1),2251(a,1,2,1))]. given #368 (F,wt=9): 2476 (c2 v x) ' ^ ((c1 ^ y) v x) = 0. [para(2251(a,1),15(a,1)),flip(a)]. given #369 (T,wt=9): 2546 (x v y) ^ (y v x) ' = 0. [para(69(a,1),152(a,1,2,1))]. given #370 (T,wt=9): 2846 (x v c2) ' ^ (x v (c1 ^ y)) = 0. [para(2355(a,1),15(a,1)),flip(a)]. given #371 (A,wt=23): 162 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(30(a,1),26(a,1,2)),flip(a)]. given #372 (F,wt=9): 2859 (x ^ y) ' != 1 | y ^ x = 0. [para(15(a,1),2383(a,1,1))]. given #373 (F,wt=9): 2862 (x v (y ^ c1)) ^ (c2 v x) ' = 0. [para(13(a,1),2387(a,1,1))]. given #374 (T,wt=9): 2863 ((x ^ c1) v y) ^ (y v c2) ' = 0. [para(13(a,1),2387(a,1,2,1))]. given #375 (T,wt=9): 2864 (c2 v x) ' ^ ((y ^ c1) v x) = 0. [para(2387(a,1),15(a,1)),flip(a)]. given #376 (A,wt=19): 163 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(30(a,1),33(a,1,2)),demod(13(5))]. given #377 (F,wt=9): 2985 (x v c2) ' ^ (x v (y ^ c1)) = 0. [para(2462(a,1),15(a,1)),flip(a)]. given #378 (F,wt=9): 2998 (c2 v x) ' ^ (x v (c1 ^ y)) = 0. [para(2474(a,1),15(a,1)),flip(a)]. given #379 (T,wt=9): 3036 (x v c2) ' ^ ((c1 ^ y) v x) = 0. [para(2475(a,1),15(a,1)),flip(a)]. given #380 (T,wt=9): 3193 (c2 v x) ' ^ (x v (y ^ c1)) = 0. [para(2862(a,1),15(a,1)),flip(a)]. given #381 (A,wt=17): 164 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(30(a,1),29(a,1,2)),demod(29(3)),flip(a)]. given #382 (F,wt=9): 3223 (x v c2) ' ^ ((y ^ c1) v x) = 0. [para(2863(a,1),15(a,1)),flip(a)]. given #383 (F,wt=9): 3245 (c2 v x) ' ^ (y ^ c1) = 0. [para(2864(a,1),76(a,1,2)),demod(15(4),81(4)),flip(a)]. given #384 (T,wt=9): 3304 (x v c2) ' ^ (y ^ c1) = 0. [para(2985(a,1),98(a,1,2)),demod(15(4),81(4)),flip(a)]. given #385 (T,wt=10): 174 c1 v (c2 ' ^ x) != 1 | c2 ' ^ x = c1 '. [para(165(a,1),21(b,1)),flip(c),xx(b)]. given #386 (A,wt=11): 168 x ^ (y v (z v x)) ' = 0. [para(14(a,1),151(a,1,2,1))]. given #387 (F,wt=10): 186 c1 v (x ^ c2 ') != 1 | x ^ c2 ' = c1 '. [para(167(a,1),21(b,1)),flip(c),xx(b)]. given #388 (F,wt=10): 217 c2 ^ (c1 ' v x) != 0 | c2 ' = c1 ' v x. [para(206(a,1),21(a,1)),xx(a)]. given #389 (T,wt=10): 221 c2 ^ (x v c1 ') != 0 | c2 ' = x v c1 '. [para(209(a,1),21(a,1)),xx(a)]. given #390 (T,wt=10): 232 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(29(a,1),53(a,1,2)),demod(53(4)),flip(a)]. given #391 (A,wt=11): 169 x ^ ((y v x) ' ^ z) = 0. [para(151(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #392 (F,wt=9): 3455 ((c2 v x) ^ y) v (c1 ^ y) ' = 1. [para(232(a,1),190(a,1,2,1))]. given #393 (F,wt=8): 3498 ((c2 v x) ^ (c1 v y)) v c1 ' = 1. [para(17(a,1),3455(a,1,2,1))]. given #394 (T,wt=8): 3505 ((c2 v x) ^ (y v c1)) v c1 ' = 1. [para(27(a,1),3455(a,1,2,1))]. given #395 (T,wt=8): 3508 ((c2 v x) ^ (c2 v y)) v c1 ' = 1. [para(224(a,1),3455(a,1,2,1))]. given #396 (A,wt=13): 170 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(151(a,1),16(a,1)),flip(a)]. given #397 (F,wt=8): 3509 ((c2 v x) ^ (y v c2)) v c1 ' = 1. [para(230(a,1),3455(a,1,2,1))]. given #398 (F,wt=8): 3544 c1 ' v ((c2 v x) ^ (c1 v y)) = 1. [para(3498(a,1),13(a,1)),flip(a)]. given #399 (T,wt=8): 3545 ((x v c2) ^ (c1 v y)) v c1 ' = 1. [para(13(a,1),3498(a,1,1,1))]. given #400 (T,wt=8): 3547 ((c1 v x) ^ (c2 v y)) v c1 ' = 1. [para(15(a,1),3498(a,1,1))]. given #401 (A,wt=14): 171 x v (y v x) ' != 1 | (y v x) ' = x '. [para(151(a,1),21(b,1)),flip(c),xx(b)]. given #402 (F,wt=8): 3561 c1 ' v ((c2 v x) ^ (y v c1)) = 1. [para(3505(a,1),13(a,1)),flip(a)]. given #403 (F,wt=8): 3562 ((x v c2) ^ (y v c1)) v c1 ' = 1. [para(13(a,1),3505(a,1,1,1))]. given #404 (T,wt=8): 3564 ((x v c1) ^ (c2 v y)) v c1 ' = 1. [para(15(a,1),3505(a,1,1))]. given #405 (T,wt=8): 3578 c1 ' v ((c2 v x) ^ (c2 v y)) = 1. [para(3508(a,1),13(a,1)),flip(a)]. given #406 (A,wt=13): 172 (x v y) ^ (x v (z v y)) ' = 0. [para(25(a,1),151(a,1,2,1))]. given #407 (F,wt=8): 3579 ((x v c2) ^ (c2 v y)) v c1 ' = 1. [para(13(a,1),3508(a,1,1,1))]. given #408 (F,wt=8): 3609 c1 ' v ((c2 v x) ^ (y v c2)) = 1. [para(3509(a,1),13(a,1)),flip(a)]. given #409 (T,wt=8): 3610 ((x v c2) ^ (y v c2)) v c1 ' = 1. [para(13(a,1),3509(a,1,1,1))]. given #410 (T,wt=8): 3623 c1 ' v ((x v c2) ^ (c1 v y)) = 1. [para(13(a,1),3544(a,1,2,1))]. given #411 (A,wt=11): 173 x ^ (y ^ (z v x) ') = 0. [para(151(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #412 (F,wt=8): 3624 c1 ' v ((c1 v x) ^ (c2 v y)) = 1. [para(15(a,1),3544(a,1,2))]. given #413 (F,wt=8): 3635 ((c1 v x) ^ (y v c2)) v c1 ' = 1. [para(15(a,1),3545(a,1,1))]. given #414 (T,wt=8): 3672 c1 ' v ((x v c2) ^ (y v c1)) = 1. [para(13(a,1),3561(a,1,2,1))]. given #415 (T,wt=8): 3674 c1 ' v ((x v c1) ^ (c2 v y)) = 1. [para(15(a,1),3561(a,1,2))]. given #416 (A,wt=18): 175 c1 ^ (x v (c1 ^ ((c1 ^ x) v (c2 ' ^ (y ^ (c1 v x)))))) = c1 ^ x. [para(165(a,1),22(a,2,2,2)),demod(16(10),42(17))]. given #417 (F,wt=8): 3686 ((x v c1) ^ (y v c2)) v c1 ' = 1. [para(15(a,1),3562(a,1,1))]. given #418 (F,wt=8): 3710 c1 ' v ((x v c2) ^ (c2 v y)) = 1. [para(13(a,1),3578(a,1,2,1))]. given #419 (T,wt=8): 3760 c1 ' v ((x v c2) ^ (y v c2)) = 1. [para(13(a,1),3609(a,1,2,1))]. given #420 (T,wt=8): 3784 c1 ' v ((c1 v x) ^ (y v c2)) = 1. [para(15(a,1),3623(a,1,2))]. given #421 (A,wt=11): 176 c1 ^ (x ^ (c2 ' ^ y)) = 0. [para(165(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #422 (F,wt=8): 3833 c1 ' v ((x v c1) ^ (y v c2)) = 1. [para(15(a,1),3672(a,1,2))]. given #423 (F,wt=9): 3475 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(232(a,1),164(a,1)),demod(224(12))]. given #424 (T,wt=9): 3493 (c1 ^ x) ' v ((c2 v y) ^ x) = 1. [para(3455(a,1),13(a,1)),flip(a)]. given #425 (T,wt=9): 3494 ((x v c2) ^ y) v (c1 ^ y) ' = 1. [para(13(a,1),3455(a,1,1,1))]. given #426 (A,wt=23): 177 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(31(a,1),14(a,1)),demod(14(2)),flip(a)]. given #427 (F,wt=9): 3496 (x ^ (c2 v y)) v (c1 ^ x) ' = 1. [para(15(a,1),3455(a,1,1))]. given #428 (F,wt=7): 4108 (x ^ c1) v (c1 ^ x) ' = 1. [para(88(a,1),3496(a,1,2,1)),demod(16(5),246(5))]. given #429 (T,wt=9): 3497 ((c2 v x) ^ y) v (y ^ c1) ' = 1. [para(15(a,1),3455(a,1,2,1))]. given #430 (T,wt=9): 3520 (x ^ (c2 v y)) v (x ^ c1) ' = 1. [para(76(a,1),3455(a,1,1)),demod(14(7),246(9))]. given #431 (A,wt=21): 178 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(16(a,1),31(a,1,2,1))]. given #432 (F,wt=9): 3922 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(13(a,1),3475(a,1,2,1,1))]. given #433 (F,wt=9): 3923 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(13(a,1),3475(a,1,2,1,2))]. given #434 (T,wt=9): 3924 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(13(a,1),3475(a,1,2))]. given #435 (T,wt=9): 3925 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(15(a,1),3475(a,1,2,1))]. given #436 (A,wt=20): 180 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x ' = (x ^ z) v y. [para(31(a,1),21(a,1))]. given #437 (F,wt=9): 3936 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(131(a,1),3475(a,1,2,1,1))]. given #438 (F,wt=9): 3937 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(133(a,1),3475(a,1,2,1,1))]. given #439 (T,wt=9): 3951 (c1 ^ x) ' v ((y v c2) ^ x) = 1. [para(13(a,1),3493(a,1,2,1))]. given #440 (T,wt=9): 3952 (x ^ c1) ' v ((c2 v y) ^ x) = 1. [para(15(a,1),3493(a,1,1,1))]. given #441 (A,wt=21): 181 x v (y v ((x ^ z) v u)) = y v (x v u). [para(31(a,1),25(a,1,2)),flip(a)]. given #442 (F,wt=9): 3953 (c1 ^ x) ' v (x ^ (c2 v y)) = 1. [para(15(a,1),3493(a,1,2))]. given #443 (F,wt=9): 3969 (x ^ c1) ' v (x ^ (c2 v y)) = 1. [para(76(a,1),3493(a,1,2)),demod(14(4),246(6))]. given #444 (T,wt=9): 3995 (x ^ (y v c2)) v (c1 ^ x) ' = 1. [para(15(a,1),3494(a,1,1))]. given #445 (T,wt=9): 3996 ((x v c2) ^ y) v (y ^ c1) ' = 1. [para(15(a,1),3494(a,1,2,1))]. given #446 (A,wt=17): 182 x v ((y ^ (x ^ z)) v u) = x v u. [para(26(a,1),31(a,1,2,1))]. given #447 (F,wt=9): 4011 (x ^ (y v c2)) v (x ^ c1) ' = 1. [para(76(a,1),3494(a,1,1)),demod(14(7),625(9))]. given #448 (F,wt=9): 4193 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(13(a,1),3922(a,1,2,1,2))]. given #449 (T,wt=9): 4194 c1 ^ (x v ((y v c1) ^ (c2 v z))) = c1. [para(13(a,1),3922(a,1,2))]. given #450 (T,wt=9): 4196 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(15(a,1),3922(a,1,2,1))]. given #451 (A,wt=15): 183 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(31(a,1),27(a,1,2)),demod(15(4))]. given #452 (F,wt=8): 4774 c2 v ((c1 ^ x) v (c2 ^ y)) ' = 1. [para(183(a,1),1653(a,1,2,1))]. given #453 (F,wt=8): 4775 c2 v ((c1 ^ x) v (y ^ c2)) ' = 1. [para(183(a,1),1654(a,1,2,1))]. given #454 (T,wt=8): 4804 c2 v ((c2 ^ x) v (c1 ^ y)) ' = 1. [para(13(a,1),4774(a,1,2,1))]. given #455 (T,wt=8): 4806 c2 v ((x ^ c1) v (c2 ^ y)) ' = 1. [para(15(a,1),4774(a,1,2,1,1))]. given #456 (A,wt=11): 184 ((x ^ y) v z) ^ (x v z) ' = 0. [para(31(a,1),151(a,1,2,1))]. given #457 (F,wt=8): 4813 c2 v ((c1 ^ x) v (y ^ c1)) ' = 1. [para(54(a,1),4774(a,1,2,1,2))]. given #458 (F,wt=8): 4819 c2 v ((x ^ c2) v (c1 ^ y)) ' = 1. [para(13(a,1),4775(a,1,2,1))]. given #459 (T,wt=8): 4821 c2 v ((x ^ c1) v (y ^ c2)) ' = 1. [para(15(a,1),4775(a,1,2,1,1))]. given #460 (T,wt=8): 4834 c2 v ((c2 ^ x) v (y ^ c1)) ' = 1. [para(15(a,1),4804(a,1,2,1,2))]. given #461 (A,wt=11): 185 c1 ^ (x ^ (y ^ c2 ')) = 0. [para(16(a,1),167(a,1,2))]. given #462 (F,wt=8): 4841 c2 v ((x ^ c1) v (c1 ^ y)) ' = 1. [para(54(a,1),4804(a,1,2,1,1))]. given #463 (F,wt=8): 4854 c2 v ((x ^ c1) v (y ^ c1)) ' = 1. [para(54(a,1),4806(a,1,2,1,2))]. given #464 (T,wt=8): 4902 c2 v ((c1 ^ x) v (c1 ^ y)) ' = 1. [para(15(a,1),4813(a,1,2,1,2))]. given #465 (T,wt=8): 4915 c2 v ((x ^ c2) v (y ^ c1)) ' = 1. [para(15(a,1),4819(a,1,2,1,2))]. given #466 (A,wt=18): 187 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2 ' ^ (c1 v x)))))) = c1 ^ x. [para(167(a,1),22(a,2,2,2)),demod(16(10),42(17))]. given #467 (F,wt=9): 4222 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(13(a,1),3923(a,1,2))]. given #468 (F,wt=9): 4224 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(15(a,1),3923(a,1,2,1))]. given #469 (T,wt=9): 4234 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(131(a,1),3923(a,1,2,1,1))]. given #470 (T,wt=9): 4235 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(133(a,1),3923(a,1,2,1,1))]. given #471 (A,wt=11): 188 x v ((x ^ y) ' v z) = 1. [para(179(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #472 (F,wt=9): 4253 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(15(a,1),3924(a,1,2,2))]. given #473 (F,wt=9): 4263 c1 ^ (x v ((c2 v y) ^ (c2 v z))) = c1. [para(131(a,1),3924(a,1,2,2,1))]. given #474 (T,wt=9): 4264 c1 ^ (x v ((y v c2) ^ (c2 v z))) = c1. [para(133(a,1),3924(a,1,2,2,1))]. given #475 (T,wt=9): 4389 (x ^ c1) ' v ((y v c2) ^ x) = 1. [para(15(a,1),3951(a,1,1,1))]. given #476 (A,wt=13): 189 x v (y v ((x v y) ^ z) ') = 1. [para(179(a,1),14(a,1)),flip(a)]. given #477 (F,wt=9): 4390 (c1 ^ x) ' v (x ^ (y v c2)) = 1. [para(15(a,1),3951(a,1,2))]. given #478 (F,wt=9): 4405 (x ^ c1) ' v (x ^ (y v c2)) = 1. [para(76(a,1),3951(a,1,2)),demod(14(4),625(6))]. given #479 (T,wt=9): 4653 c1 ^ (x v ((y v c1) ^ (z v c2))) = c1. [para(13(a,1),4193(a,1,2))]. given #480 (T,wt=9): 4656 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(15(a,1),4193(a,1,2,1))]. given #481 (A,wt=13): 191 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(16(a,1),179(a,1,2,1))]. given #482 (F,wt=9): 4686 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(15(a,1),4194(a,1,2,2))]. given #483 (F,wt=9): 5025 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(15(a,1),4222(a,1,2,2))]. given #484 (T,wt=9): 5034 c1 ^ (x v ((c2 v y) ^ (z v c2))) = c1. [para(131(a,1),4222(a,1,2,2,1))]. given #485 (T,wt=9): 5035 c1 ^ (x v ((y v c2) ^ (z v c2))) = c1. [para(133(a,1),4222(a,1,2,2,1))]. given #486 (A,wt=14): 192 x ^ (x ^ y) ' != 0 | (x ^ y) ' = x '. [para(179(a,1),21(a,1)),flip(c),xx(a)]. given #487 (F,wt=9): 5330 c1 ^ (x v ((y v c2) ^ (z v c1))) = c1. [para(15(a,1),4653(a,1,2,2))]. given #488 (F,wt=9): 5397 (x ^ y) v (y ^ x) ' = 1. [para(76(a,1),191(a,1,2,1))]. given #489 (T,wt=10): 246 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(224(a,1),26(a,1,2)),flip(a)]. given #490 (T,wt=10): 248 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(230(a,1),16(a,1,1)),flip(a)]. given #491 (A,wt=11): 193 x v (y v (x ^ z) ') = 1. [para(179(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #492 (F,wt=10): 251 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(230(a,1),26(a,1,2)),flip(a)]. given #493 (F,wt=10): 253 c1 v (c2 v x) ' != 1 | (c2 v x) ' = c1 '. [para(233(a,1),21(b,1)),flip(c),xx(b)]. given #494 (T,wt=10): 258 c1 v (x v c2) ' != 1 | (x v c2) ' = c1 '. [para(235(a,1),21(b,1)),flip(c),xx(b)]. given #495 (T,wt=10): 282 c2 ^ (c1 ^ x) ' != 0 | (c1 ^ x) ' = c2 '. [para(279(a,1),21(a,1)),flip(c),xx(a)]. given #496 (A,wt=11): 194 x v (y ^ (x ^ z)) ' = 1. [para(26(a,1),179(a,1,2,1))]. given #497 (F,wt=10): 288 c2 ^ (x ^ c1) ' != 0 | (x ^ c1) ' = c2 '. [para(281(a,1),21(a,1)),flip(c),xx(a)]. given #498 (F,wt=10): 292 (c2 ^ (c1 v x)) v (c1 ' v y) = 1. [para(270(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #499 (T,wt=10): 294 (c2 ^ (c1 v x)) v (y v c1 ') = 1. [para(270(a,1),25(a,1,2)),demod(72(2)),flip(a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 87 (0.00 of 1.88 sec). given #500 (T,wt=10): 295 (c2 ^ (x v (c1 v y))) v c1 ' = 1. [para(25(a,1),270(a,1,1,2))]. given #501 (A,wt=11): 195 x v ((y ^ x) ' v z) = 1. [para(190(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #502 (F,wt=10): 305 (c2 ^ (x v c1)) v (c1 ' v y) = 1. [para(276(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #503 (F,wt=10): 306 (c2 ^ (x v (y v c1))) v c1 ' = 1. [para(14(a,1),276(a,1,1,2))]. given #504 (T,wt=10): 308 (c2 ^ (x v c1)) v (y v c1 ') = 1. [para(276(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #505 (T,wt=10): 309 c1 ' v ((c2 ^ (c1 v x)) v y) = 1. [para(291(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #506 (A,wt=13): 196 x v (y v (z ^ (x v y)) ') = 1. [para(190(a,1),14(a,1)),flip(a)]. given #507 (F,wt=10): 311 c1 ' v (x v (c2 ^ (c1 v y))) = 1. [para(291(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #508 (F,wt=10): 312 c1 ' v (c2 ^ (x v (c1 v y))) = 1. [para(25(a,1),291(a,1,2,2))]. given #509 (T,wt=10): 313 c1 ' v ((c2 ^ (x v c1)) v y) = 1. [para(304(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #510 (T,wt=10): 314 c1 ' v (c2 ^ (x v (y v c1))) = 1. [para(14(a,1),304(a,1,2,2))]. given #511 (A,wt=11): 197 x v (y ^ (z ^ x)) ' = 1. [para(16(a,1),190(a,1,2,1))]. given #512 (F,wt=10): 316 c1 ' v (x v (c2 ^ (y v c1))) = 1. [para(304(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #513 (F,wt=10): 339 c2 ^ (c1 ' v x) != 0 | (c1 ' v x) ' = c2. [para(206(a,1),43(a,1)),demod(15(8)),xx(a)]. given #514 (T,wt=10): 340 c2 ^ (x v c1 ') != 0 | (x v c1 ') ' = c2. [para(209(a,1),43(a,1)),demod(15(8)),xx(a)]. given #515 (T,wt=10): 374 (x v c2) ^ c1 ' != 0 | (x v c2) ' = c1 '. [para(200(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #516 (A,wt=14): 198 x ^ (y ^ x) ' != 0 | (y ^ x) ' = x '. [para(190(a,1),21(a,1)),flip(c),xx(a)]. given #517 (F,wt=10): 378 (c2 v x) ^ c1 ' != 0 | (c2 v x) ' = c1 '. [para(209(a,1),44(a,1)),xx(a)]. given #518 (F,wt=10): 410 c1 v (c2 ' ^ x) != 1 | (c2 ' ^ x) ' = c1. [para(165(a,1),45(b,1)),demod(13(5)),xx(b)]. given #519 (T,wt=10): 411 c1 v (x ^ c2 ') != 1 | (x ^ c2 ') ' = c1. [para(167(a,1),45(b,1)),demod(13(5)),xx(b)]. given #520 (T,wt=10): 460 (x ^ c1) v c2 ' != 1 | (x ^ c1) ' = c2 '. [para(158(a,1),46(b,1,2)),demod(83(9)),xx(b)]. given #521 (A,wt=25): 199 x v ((y ^ ((y ^ x) v (z ^ (y v x)))) v (y ^ (x v (y ^ z))) ') = 1. [para(22(a,1),190(a,1,2,1)),demod(14(11))]. given #522 (F,wt=10): 464 (c1 ^ x) v c2 ' != 1 | (c1 ^ x) ' = c2 '. [para(167(a,1),46(b,1)),xx(b)]. given #523 (F,wt=10): 496 (c1 v (c2 ^ x)) ^ (c2 ' ^ y) = 0. [para(486(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #524 (T,wt=10): 498 (c1 v (c2 ^ x)) ^ (y ^ c2 ') = 0. [para(486(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #525 (T,wt=10): 499 (c1 v (x ^ (c2 ^ y))) ^ c2 ' = 0. [para(26(a,1),486(a,1,1,2))]. given #526 (A,wt=11): 201 x v (y v (z ^ x) ') = 1. [para(190(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #527 (F,wt=10): 504 (c1 v (x ^ c2)) ^ (c2 ' ^ y) = 0. [para(490(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #528 (F,wt=10): 505 (c1 v (x ^ (y ^ c2))) ^ c2 ' = 0. [para(16(a,1),490(a,1,1,2))]. given #529 (T,wt=10): 507 (c1 v (x ^ c2)) ^ (y ^ c2 ') = 0. [para(490(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #530 (T,wt=10): 523 c2 ' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(495(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #531 (A,wt=13): 202 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(26(a,1),190(a,1,2,1))]. given #532 (F,wt=10): 524 c2 ' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(495(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #533 (F,wt=10): 525 c2 ' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(26(a,1),495(a,1,2,2))]. given #534 (T,wt=10): 528 c2 ' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(503(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #535 (T,wt=10): 529 c2 ' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(16(a,1),503(a,1,2,2))]. given #536 (A,wt=15): 203 x v (y v (z v (x v y) ')) = 1. [para(28(a,1),190(a,1,2,1)),demod(14(5),14(4))]. given #537 (F,wt=10): 530 c2 ' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(503(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #538 (F,wt=10): 839 c2 ^ (c1 v x) != 1 | c1 != 0 | c1 ' = c2 ^ (c1 v x). [para(604(a,1),21(a,1)),demod(76(12),15(9),23(9))]. given #539 (T,wt=10): 844 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (c1 v x)) ' = c1. [para(604(a,1),43(a,1)),demod(15(12),76(12),15(9),23(9))]. given #540 (T,wt=10): 849 c1 ^ ((c2 ^ (c1 v x)) ' ^ y) = 0. [para(843(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #541 (A,wt=11): 204 ((x v y) ^ z) v (x ^ z) ' = 1. [para(29(a,1),190(a,1,2,1))]. given #542 (F,wt=10): 851 c1 ^ (c2 ^ (x v (c1 v y))) ' = 0. [para(25(a,1),843(a,1,2,1,2))]. given #543 (F,wt=9): 6299 c1 ^ (c2 ^ (x v (c2 ^ (c1 v y)))) ' = 0. [para(604(a,1),851(a,1,2,1,2,2))]. given #544 (T,wt=9): 6300 c1 ^ (c2 ^ (x v (c2 ^ (y v c1)))) ' = 0. [para(609(a,1),851(a,1,2,1,2,2))]. given #545 (T,wt=9): 6306 c1 ^ (c2 ^ ((c2 ^ (c1 v x)) v y)) ' = 0. [para(13(a,1),6299(a,1,2,1,2))]. given #546 (A,wt=13): 205 (x ^ ((y ^ x) v z)) v (y ^ x) ' = 1. [para(30(a,1),190(a,1,2,1))]. given #547 (F,wt=9): 6319 c1 ^ (c2 ^ ((c2 ^ (x v c1)) v y)) ' = 0. [para(13(a,1),6300(a,1,2,1,2))]. given #548 (F,wt=10): 852 c1 ^ (x ^ (c2 ^ (c1 v y)) ') = 0. [para(843(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #549 (T,wt=10): 853 c1 v (c2 ^ (c1 v x)) ' != 1 | c2 ^ (c1 v x) = c1. [para(843(a,1),45(b,1)),demod(13(7),326(18)),xx(b)]. given #550 (T,wt=10): 855 c1 ^ (c2 ^ (x v (y v c1))) ' = 0. [para(14(a,1),848(a,1,2,1,2))]. given #551 (A,wt=14): 208 c2 ^ (c1 ' v (c2 ^ ((c2 ^ c1 ') v x))) = c2 ^ (c1 ' v (c2 ^ x)). [para(200(a,1),22(a,1,2,2,2,2,2)),demod(39(10))]. given #552 (F,wt=8): 6430 c2 ^ (c1 ' v (c2 ^ (c2 ^ c1 ') ')) = c2. [para(19(a,1),208(a,1,2,2,2)),demod(15(6),57(6),13(5),200(5),15(3),57(3)),flip(a)]. given #553 (F,wt=7): 6472 c1 ' v (c2 ^ (c2 ^ c1 ') ') = 1. [para(6430(a,1),33(a,1,2)),demod(13(12),69(12),13(4),200(4)),flip(a)]. given #554 (T,wt=5): 6475 c2 ^ (c2 ^ c1 ') ' = c1. [hyper(79,a,6472,a,b,41,a),demod(326(3)),flip(a)]. given #555 (T,wt=4): 6482 c1 != 0 | c2 ^ c1 ' = c2. [para(6475(a,1),45(b,1)),demod(13(7),179(7),326(12)),xx(a)]. given #556 (A,wt=15): 210 x v (y v ((y v x) ^ z)) = x v y. [para(13(a,1),32(a,1,2,2,1))]. given #557 (F,wt=5): 6481 c1 ^ (c2 ^ c1 ') ' = c1. [para(6475(a,1),53(a,1,2)),demod(35(3)),flip(a)]. given #558 (F,wt=6): 6477 c1 != 0 | (c2 ^ c1 ') ' = c2 '. [para(6475(a,1),21(b,1)),demod(179(7)),flip(c),xx(a)]. given #559 (T,wt=8): 6480 c1 v (c2 ^ c1 ') ' = (c2 ^ c1 ') '. [para(6475(a,1),33(a,1,2)),demod(13(7))]. given #560 (T,wt=7): 6553 c1 ^ (x v (c2 ^ c1 ') ') = c1. [para(6480(a,1),68(a,1,2,2))]. given #561 (A,wt=24): 211 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x ' = y v ((x v y) ^ z). [para(32(a,1),21(a,1))]. given #562 (F,wt=7): 6586 c1 ^ ((c2 ^ c1 ') ' v x) = c1. [para(13(a,1),6553(a,1,2))]. given #563 (F,wt=7): 6621 c1 v c2 ' != 1 | c2 ^ (c1 v c2 ') = c2. [para(503(a,1),211(b,1)),demod(13(4),326(12),13(15),15(17),604(18)),flip(c),xx(b)]. given #564 (T,wt=8): 6488 (c2 ^ c1 ') ' != 1 | c1 != 0 | c2 ^ c1 ' = c1. [para(6475(a,1),122(b,1)),demod(326(16),6475(21)),flip(a)]. given #565 (T,wt=8): 6496 (c2 ^ c1 ') ' v (x ^ c1) ' = 1. [para(6475(a,1),197(a,1,2,1,2))]. given #566 (A,wt=23): 212 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(32(a,1),25(a,1,2)),flip(a)]. given #567 (F,wt=8): 6570 c1 ^ (x v (c2 ^ c1 ') ') ' = 0. [para(6480(a,1),156(a,1,2,1,2))]. given #568 (F,wt=8): 6728 c1 ^ ((c2 ^ c1 ') ' v x) ' = 0. [para(6586(a,1),980(a,1,2)),demod(15(9))]. given #569 (T,wt=8): 6748 (x ^ c1) ' v (c2 ^ c1 ') ' = 1. [para(6496(a,1),13(a,1)),flip(a)]. given #570 (T,wt=8): 6750 (c2 ^ c1 ') ' v (c1 ^ x) ' = 1. [para(15(a,1),6496(a,1,2,1))]. given #571 (A,wt=19): 213 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(26(a,1),32(a,1,2,2))]. given #572 (F,wt=8): 6799 (c1 ^ x) ' v (c2 ^ c1 ') ' = 1. [para(15(a,1),6748(a,1,1,1))]. given #573 (F,wt=9): 6500 c1 ' v ((c2 v x) ^ (c2 ^ c1 ') ') = 1. [para(6475(a,1),204(a,1,2,1)),demod(13(11))]. given #574 (T,wt=9): 6501 c1 ' v ((c2 ^ c1 ') ' ^ (c1 v x)) = 1. [para(6475(a,1),205(a,1,1,2,1)),demod(6475(15),13(11))]. given #575 (T,wt=9): 6544 c1 ' v ((x v c2) ^ (c2 ^ c1 ') ') = 1. [para(6481(a,1),3494(a,1,2,1)),demod(13(11))]. given #576 (A,wt=19): 214 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(32(a,1),27(a,1,2)),demod(15(5))]. given #577 (F,wt=9): 6545 c1 ' v ((c2 ^ c1 ') ' ^ (c2 v x)) = 1. [para(6481(a,1),3496(a,1,2,1)),demod(13(11))]. given #578 (F,wt=9): 6546 c1 ' v ((c2 ^ c1 ') ' ^ (x v c2)) = 1. [para(6481(a,1),3995(a,1,2,1)),demod(13(11))]. given #579 (T,wt=9): 6548 c1 ' v ((c1 v x) ^ (c2 ^ c1 ') ') = 1. [para(6481(a,1),204(a,1,2,1)),demod(13(11))]. given #580 (T,wt=9): 6565 c1 ^ ((c2 v x) ^ (c2 ^ c1 ') ') ' = 0. [para(6480(a,1),2190(a,1,2,1,2))]. given #581 (A,wt=13): 215 (x v ((y v x) ^ z)) ^ (y v x) ' = 0. [para(32(a,1),151(a,1,2,1))]. given #582 (F,wt=9): 6566 c1 ^ ((x v c2) ^ (c2 ^ c1 ') ') ' = 0. [para(6480(a,1),2203(a,1,2,1,2))]. given #583 (F,wt=9): 6567 c1 ^ ((c2 ^ c1 ') ' ^ (c2 v x)) ' = 0. [para(6480(a,1),2204(a,1,2,1,1))]. given #584 (T,wt=9): 6568 c1 ^ ((c2 ^ c1 ') ' ^ (x v c2)) ' = 0. [para(6480(a,1),2228(a,1,2,1,1))]. given #585 (T,wt=9): 6583 c1 ' v (c2 ^ (x v (c2 ^ c1 ') ')) = 1. [para(6480(a,1),295(a,1,1,2,2)),demod(13(11))]. given #586 (A,wt=17): 216 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(32(a,1),31(a,1,2)),demod(31(3)),flip(a)]. given #587 (F,wt=9): 6585 c1 ^ (c2 ^ (x v (c2 ^ c1 ') ')) ' = 0. [para(6480(a,1),851(a,1,2,1,2,2))]. given #588 (F,wt=9): 6719 c1 ' v (c2 ^ ((c2 ^ c1 ') ' v x)) = 1. [para(6586(a,1),236(a,1,2,1)),demod(13(11))]. given #589 (T,wt=9): 6865 c1 ' v ((c2 ^ c1 ') ' ^ (x v c1)) = 1. [para(13(a,1),6501(a,1,2,2))]. given #590 (T,wt=9): 6984 c1 ' v ((x v c1) ^ (c2 ^ c1 ') ') = 1. [para(13(a,1),6548(a,1,2,1))]. given #591 (A,wt=24): 218 c2 ^ (c1 ' v (x v (c2 ^ ((c2 ^ (c1 ' v x)) v y)))) = c2 ^ (c1 ' v (x v (c2 ^ y))). [para(206(a,1),22(a,1,2,2,2,2,2)),demod(39(12),14(13),14(21))]. given #592 (F,wt=9): 7086 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(216(a,1),141(a,1)),demod(127(4)),flip(a)]. given #593 (F,wt=9): 7090 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(216(a,1),146(a,1)),demod(129(4)),flip(a)]. given #594 (T,wt=9): 7115 c1 ^ (c2 ^ ((c2 ^ c1 ') ' v x)) ' = 0. [para(13(a,1),6585(a,1,2,1,2))]. given #595 (T,wt=9): 7184 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(13(a,1),7086(a,1,2,1))]. given #596 (A,wt=11): 219 c2 v (x v (c1 ' v y)) = 1. [para(206(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #597 (F,wt=9): 7186 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(15(a,1),7086(a,1,2,1,1))]. given #598 (F,wt=9): 7187 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(15(a,1),7086(a,1,2))]. given #599 (T,wt=9): 7195 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(54(a,1),7086(a,1,2,1,1))]. given #600 (T,wt=9): 7220 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(13(a,1),7090(a,1,2,1))]. given #601 (A,wt=11): 220 c2 v (x v (y v c1 ')) = 1. [para(14(a,1),209(a,1,2))]. given #602 (F,wt=9): 7222 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(15(a,1),7090(a,1,2,1,1))]. given #603 (F,wt=9): 7223 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(15(a,1),7090(a,1,2))]. given #604 (T,wt=9): 7231 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(54(a,1),7090(a,1,2,1,1))]. given #605 (T,wt=9): 7265 c2 v (((c1 ^ x) v (y ^ c2)) ^ z) = c2. [para(15(a,1),7184(a,1,2,1,2))]. given #606 (A,wt=24): 222 c2 ^ (x v (c1 ' v (c2 ^ ((c2 ^ (x v c1 ')) v y)))) = c2 ^ (x v (c1 ' v (c2 ^ y))). [para(209(a,1),22(a,1,2,2,2,2,2)),demod(39(12),14(13),14(21))]. given #607 (F,wt=9): 7266 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(15(a,1),7184(a,1,2))]. given #608 (F,wt=9): 7274 c2 v (((c1 ^ x) v (y ^ c1)) ^ z) = c2. [para(54(a,1),7184(a,1,2,1,2))]. given #609 (T,wt=9): 7297 c2 v (x ^ ((y ^ c2) v (c1 ^ z))) = c2. [para(15(a,1),7186(a,1,2))]. given #610 (T,wt=9): 7333 c2 v (x ^ ((y ^ c1) v (c1 ^ z))) = c2. [para(54(a,1),7187(a,1,2,2,1))]. given #611 (A,wt=16): 223 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(53(a,1),16(a,2,2)),demod(26(5),16(4))]. given #612 (F,wt=9): 7354 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z) = c2. [para(15(a,1),7195(a,1,2,1,1))]. given #613 (F,wt=9): 7383 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(15(a,1),7220(a,1,2,1,2))]. given #614 (T,wt=9): 7384 c2 v (x ^ ((y ^ c1) v (c2 ^ z))) = c2. [para(15(a,1),7220(a,1,2))]. given #615 (T,wt=9): 7417 c2 v (x ^ ((y ^ c2) v (z ^ c1))) = c2. [para(15(a,1),7222(a,1,2))]. given #616 (A,wt=11): 225 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1 ' = c2 ^ x. [para(53(a,1),21(b,1))]. given #617 (F,wt=9): 7453 c2 v (x ^ ((y ^ c1) v (z ^ c1))) = c2. [para(54(a,1),7223(a,1,2,2,1))]. given #618 (F,wt=9): 7503 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(15(a,1),7265(a,1,2))]. given #619 (T,wt=9): 7554 c2 v (x ^ ((c1 ^ y) v (z ^ c1))) = c2. [para(54(a,1),7266(a,1,2,2,2))]. given #620 (T,wt=9): 7627 c2 v (x ^ ((c1 ^ y) v (c1 ^ z))) = c2. [para(15(a,1),7333(a,1,2,2,1))]. given #621 (A,wt=20): 226 c1 ^ ((c2 ^ x) v (c1 ^ ((c1 ^ x) v (y ^ (c1 v (c2 ^ x)))))) = c1 ^ ((c2 ^ x) v (c1 ^ y)). [para(53(a,1),22(a,1,2,2,2,1))]. given #622 (F,wt=9): 7696 c2 v (x ^ ((y ^ c1) v (z ^ c2))) = c2. [para(15(a,1),7383(a,1,2))]. given #623 (F,wt=10): 856 c1 ^ ((c2 ^ (x v c1)) ' ^ y) = 0. [para(848(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #624 (T,wt=10): 858 c1 ^ (x ^ (c2 ^ (y v c1)) ') = 0. [para(848(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #625 (T,wt=10): 859 c1 v (c2 ^ (x v c1)) ' != 1 | c2 ^ (x v c1) = c1. [para(848(a,1),45(b,1)),demod(13(7),326(18)),xx(b)]. given #626 (A,wt=20): 227 c1 ^ (x v (c1 ^ ((c1 ^ x) v (c2 ^ (y ^ (c1 v x)))))) = c1 ^ (x v (c1 ^ y)). [para(53(a,1),22(a,2,2,2)),demod(16(9))]. given #627 (F,wt=10): 923 c2 ^ (x v c1) != 1 | c1 != 0 | c1 ' = c2 ^ (x v c1). [para(609(a,1),21(a,1)),demod(98(12),15(9),23(9))]. given #628 (F,wt=10): 925 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (x v c1)) ' = c1. [para(609(a,1),43(a,1)),demod(15(12),98(12),15(9),23(9))]. given #629 (T,wt=10): 1029 c2 != 1 | c1 v (c2 ^ x) != 0 | c2 ' = c1 v (c2 ^ x). [para(782(a,1),21(b,1)),demod(25(6),18(5),124(3))]. given #630 (T,wt=10): 1034 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (c2 ^ x)) ' = c2. [para(782(a,1),45(b,1)),demod(13(6),25(6),18(5),124(3))]. given #631 (A,wt=17): 228 c1 ^ (x v (c2 ^ ((c2 ^ x) v (y ^ (c2 v x))))) = c1 ^ (x v (c2 ^ y)). [para(22(a,1),53(a,1,2)),demod(53(7)),flip(a)]. given #632 (F,wt=10): 1040 c2 v ((c1 v (c2 ^ x)) ' v y) = 1. [para(1032(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #633 (F,wt=10): 1044 c2 v (x v (c1 v (c2 ^ y)) ') = 1. [para(1032(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #634 (T,wt=10): 1045 c2 v (c1 v (x ^ (c2 ^ y))) ' = 1. [para(26(a,1),1032(a,1,2,1,2))]. given #635 (T,wt=9): 8048 c2 v (c1 v (x ^ (c1 v (c2 ^ y)))) ' = 1. [para(782(a,1),1045(a,1,2,1,2,2))]. given #636 (A,wt=16): 229 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(53(a,1),26(a,1,2)),flip(a)]. given #637 (F,wt=9): 8049 c2 v (c1 v (x ^ (c1 v (y ^ c2)))) ' = 1. [para(788(a,1),1045(a,1,2,1,2,2))]. given #638 (F,wt=9): 8055 c2 v (c1 v ((c1 v (c2 ^ x)) ^ y)) ' = 1. [para(15(a,1),8048(a,1,2,1,2))]. given #639 (T,wt=9): 8080 c2 v (c1 v ((c1 v (x ^ c2)) ^ y)) ' = 1. [para(15(a,1),8049(a,1,2,1,2))]. given #640 (T,wt=10): 1046 c2 ^ (c1 v (c2 ^ x)) ' != 0 | c1 v (c2 ^ x) = c2. [para(1032(a,1),43(a,1)),demod(15(10),326(18)),xx(a)]. given #641 (A,wt=12): 234 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(30(a,1),53(a,1,2)),demod(53(4)),flip(a)]. given #642 (F,wt=10): 1049 c2 v ((c1 v (x ^ c2)) ' v y) = 1. [para(1041(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #643 (F,wt=10): 1050 c2 v (c1 v (x ^ (y ^ c2))) ' = 1. [para(16(a,1),1041(a,1,2,1,2))]. given #644 (T,wt=10): 1053 c2 v (x v (c1 v (y ^ c2)) ') = 1. [para(1041(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #645 (T,wt=10): 1054 c2 ^ (c1 v (x ^ c2)) ' != 0 | c1 v (x ^ c2) = c2. [para(1041(a,1),43(a,1)),demod(15(10),326(18)),xx(a)]. given #646 (A,wt=15): 237 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(15(a,1),34(a,1,1))]. given #647 (F,wt=10): 1119 c2 != 1 | c1 v (x ^ c2) != 0 | c2 ' = c1 v (x ^ c2). [para(788(a,1),21(b,1)),demod(25(6),33(5),124(3))]. given #648 (F,wt=10): 1122 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (x ^ c2)) ' = c2. [para(788(a,1),45(b,1)),demod(13(6),25(6),33(5),124(3))]. given #649 (T,wt=10): 1253 x ^ (c1 v (c2 ^ (x v y))) = c2 ^ x. [para(1203(a,1),29(a,1,2)),demod(15(3),76(4),15(6)),flip(a)]. given #650 (T,wt=10): 1257 x ^ (c1 v (c2 ^ (y v x))) = c2 ^ x. [para(1203(a,1),94(a,1,2)),demod(15(3),98(4),15(6)),flip(a)]. given #651 (A,wt=15): 238 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(15(a,1),34(a,1,2)),demod(16(3))]. given #652 (F,wt=10): 1384 (c1 v (c2 ^ x)) ' v (y v c2) = 1. [para(1032(a,1),110(a,1,1)),demod(57(10),1032(15))]. given #653 (F,wt=10): 1385 (c1 v (x ^ c2)) ' v (y v c2) = 1. [para(1041(a,1),110(a,1,1)),demod(57(10),1041(15))]. given #654 (T,wt=10): 1760 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(1677(a,1),31(a,1,2)),demod(13(3),69(4),13(6)),flip(a)]. given #655 (T,wt=10): 1769 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(1677(a,1),119(a,1,2)),demod(13(3),125(4),13(6)),flip(a)]. given #656 (A,wt=21): 239 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(34(a,1),25(a,1,2)),flip(a)]. given #657 (F,wt=10): 2161 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(54(a,1),140(a,1,1)),demod(33(8)),flip(a)]. given #658 (F,wt=10): 2180 (c2 v x) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(782(a,1),140(a,1,1)),demod(33(12)),flip(a)]. given #659 (T,wt=10): 2181 (c2 v x) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(788(a,1),140(a,1,1)),demod(33(12)),flip(a)]. given #660 (T,wt=8): 8386 c2 v x != 1 | c2 != 0 | (c2 v x) ' = c2. [para(2181(a,1),211(b,1)),demod(13(4),131(4),13(9),131(9),15(9),17(9),124(7),13(15),131(15),15(15),17(15),124(13))]. given #661 (A,wt=19): 240 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(26(a,1),34(a,1,2,2))]. given #662 (F,wt=8): 8390 x v c2 != 1 | c2 != 0 | (c2 v x) ' = c2. [para(13(a,1),8386(a,1))]. given #663 (F,wt=8): 8392 x v c2 != 1 | c2 != 0 | (x v c2) ' = c2. [para(69(a,1),8386(a,1)),demod(69(12))]. given #664 (T,wt=8): 8410 c2 v x != 1 | c2 != 0 | (x v c2) ' = c2. [para(13(a,1),8392(a,1))]. given #665 (T,wt=10): 2256 (c1 ^ x) v (y v c2) = y v c2. [para(69(a,1),141(a,2)),demod(704(8))]. given #666 (A,wt=15): 242 x ^ (y ^ (z ^ (x ^ y) ')) = 0. [para(34(a,1),151(a,1,2,1)),demod(16(5),16(4))]. given #667 (F,wt=10): 2392 (x ^ c1) v (y v c2) = y v c2. [para(69(a,1),146(a,2)),demod(704(8))]. given #668 (F,wt=10): 2549 (x v c1) ^ (x v (c2 ^ (c1 v y))) ' = 0. [para(604(a,1),152(a,1,2,1,2))]. given #669 (T,wt=10): 2550 (x v c1) ^ (x v (c2 ^ (y v c1))) ' = 0. [para(609(a,1),152(a,1,2,1,2))]. given #670 (T,wt=10): 2942 c1 v (c2 ^ x) != 1 | c1 != 0 | c1 ' = c1 v (x ^ c2). [para(143(a,1),160(a,1,2)),demod(23(5),782(7),65(6),23(9),23(15),23(17),788(19),65(18),788(17))]. given #671 (A,wt=11): 260 x v (y v (y v x) ') = 1. [para(13(a,1),38(a,1,2,2,1))]. given #672 (F,wt=10): 3417 c1 v (x ^ c2 ') != 1 | c2 ' ^ x = c1 '. [para(15(a,1),174(a,1,2))]. given #673 (F,wt=10): 3449 c1 v (c2 ' ^ x) != 1 | x ^ c2 ' = c1 '. [para(15(a,1),186(a,1,2))]. given #674 (T,wt=10): 3450 c2 ^ (x v c1 ') != 0 | c2 ' = c1 ' v x. [para(13(a,1),217(a,1,2))]. given #675 (T,wt=10): 3453 c2 ^ (c1 ' v x) != 0 | c2 ' = x v c1 '. [para(13(a,1),221(a,1,2))]. given #676 (A,wt=15): 261 x v (y v ((x v y) ' v z)) = 1. [para(38(a,1),14(a,1,1)),demod(64(2),14(5)),flip(a)]. given #677 (F,wt=10): 3942 c1 ^ (((c1 v x) ^ (c2 v y)) v z) ' = 0. [para(3475(a,1),980(a,1,2)),demod(15(9))]. given #678 (F,wt=10): 4210 c1 ^ (((x v c1) ^ (c2 v y)) v z) ' = 0. [para(3922(a,1),980(a,1,2)),demod(15(9))]. given #679 (T,wt=10): 4240 c1 ^ (((c1 v x) ^ (y v c2)) v z) ' = 0. [para(3923(a,1),980(a,1,2)),demod(15(9))]. given #680 (T,wt=10): 4268 c1 ^ (x v ((c1 v y) ^ (c2 v z))) ' = 0. [para(3924(a,1),980(a,1,2)),demod(15(9))]. given #681 (A,wt=19): 262 x v (y v (z v (x v (y v z)) ')) = 1. [para(38(a,1),14(a,1)),demod(14(3)),flip(a)]. given #682 (F,wt=10): 4295 c1 ^ (((c2 v x) ^ (c1 v y)) v z) ' = 0. [para(3925(a,1),980(a,1,2)),demod(15(9))]. given #683 (F,wt=10): 4335 c2 != 1 | c1 v (c2 ^ x) != 0 | c2 ' = c1 v (x ^ c2). [para(149(a,1),180(b,1)),demod(15(5),23(5),788(7),25(6),33(5),124(3),15(7),23(7),782(9),15(14),23(14),15(16),23(16),788(18),65(17))]. given #684 (T,wt=10): 4350 c1 ^ (((c2 v x) ^ (c2 v y)) v z) ' = 0. [para(3936(a,1),980(a,1,2)),demod(15(9))]. given #685 (T,wt=10): 4376 c1 ^ (((x v c2) ^ (c2 v y)) v z) ' = 0. [para(3937(a,1),980(a,1,2)),demod(15(9))]. given #686 (A,wt=18): 263 x ^ (y v (x v y) ') != 0 | y v (x v y) ' = x '. [para(38(a,1),21(a,1)),flip(c),xx(a)]. given #687 (F,wt=10): 4669 c1 ^ (((x v c1) ^ (y v c2)) v z) ' = 0. [para(4193(a,1),980(a,1,2)),demod(15(9))]. given #688 (F,wt=10): 4700 c1 ^ (x v ((y v c1) ^ (c2 v z))) ' = 0. [para(4194(a,1),980(a,1,2)),demod(15(9))]. given #689 (T,wt=10): 4730 c1 ^ (((c2 v x) ^ (y v c1)) v z) ' = 0. [para(4196(a,1),980(a,1,2)),demod(15(9))]. given #690 (T,wt=10): 4763 (c1 ^ x) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(604(a,1),183(a,1,1)),demod(27(12)),flip(a)]. given #691 (A,wt=15): 264 x v (y v (z v (x v z) ')) = 1. [para(38(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #692 (F,wt=10): 4765 (c1 ^ x) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(609(a,1),183(a,1,1)),demod(27(12)),flip(a)]. given #693 (F,wt=8): 8670 c1 != 1 | c1 ^ x != 0 | (c1 ^ x) ' = c1. [para(4765(a,1),160(a,1)),demod(15(5),26(5),53(5),13(5),18(5),15(3),23(3),15(7),26(7),53(7),15(15),26(15),53(15),13(15),18(15),15(13),23(13))]. given #694 (T,wt=8): 8674 c1 != 1 | x ^ c1 != 0 | (c1 ^ x) ' = c1. [para(15(a,1),8670(b,1))]. given #695 (T,wt=8): 8676 c1 != 1 | x ^ c1 != 0 | (x ^ c1) ' = c1. [para(80(a,1),8670(b,1)),demod(80(11))]. given #696 (A,wt=19): 265 x v (y v (z v (y v (x v z)) ')) = 1. [para(25(a,1),38(a,1,2,2,1)),demod(14(5))]. given #697 (F,wt=8): 8679 c1 != 1 | c1 ^ x != 0 | (x ^ c1) ' = c1. [para(15(a,1),8676(b,1))]. given #698 (F,wt=10): 4789 c2 ^ c1 ' != 0 | (c2 ^ c1 ') v (c2 ^ (x v c1)) = c1. [back_demod(2948),demod(4747(17))]. given #699 (T,wt=10): 4790 c2 ^ c1 ' != 0 | (c2 ^ c1 ') v (c2 ^ (c1 v x)) = c1. [back_demod(2947),demod(4747(17))]. given #700 (T,wt=10): 5039 c1 ^ (x v ((c1 v y) ^ (z v c2))) ' = 0. [para(4222(a,1),980(a,1,2)),demod(15(9))]. given #701 (A,wt=13): 266 x v (y v ((x ^ z) v y) ') = 1. [para(38(a,1),31(a,1,2)),demod(72(2)),flip(a)]. given #702 (F,wt=10): 5069 c1 ^ (((x v c2) ^ (c1 v y)) v z) ' = 0. [para(4224(a,1),980(a,1,2)),demod(15(9))]. given #703 (F,wt=10): 5096 c1 ^ (((c2 v x) ^ (y v c2)) v z) ' = 0. [para(4234(a,1),980(a,1,2)),demod(15(9))]. given #704 (T,wt=10): 5125 c1 ^ (((x v c2) ^ (y v c2)) v z) ' = 0. [para(4235(a,1),980(a,1,2)),demod(15(9))]. given #705 (T,wt=10): 5160 c1 ^ (x v ((c2 v y) ^ (c1 v z))) ' = 0. [para(4253(a,1),980(a,1,2)),demod(15(9))]. given #706 (A,wt=11): 267 (c2 ^ x) v ((c1 ^ x) ' v y) = 1. [para(236(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #707 (F,wt=10): 5192 c1 ^ (x v ((c2 v y) ^ (c2 v z))) ' = 0. [para(4263(a,1),980(a,1,2)),demod(15(9))]. given #708 (F,wt=10): 5223 c1 ^ (x v ((y v c2) ^ (c2 v z))) ' = 0. [para(4264(a,1),980(a,1,2)),demod(15(9))]. given #709 (T,wt=10): 5343 c1 ^ (x v ((y v c1) ^ (z v c2))) ' = 0. [para(4653(a,1),980(a,1,2)),demod(15(9))]. given #710 (T,wt=10): 5374 c1 ^ (((x v c2) ^ (y v c1)) v z) ' = 0. [para(4656(a,1),980(a,1,2)),demod(15(9))]. given #711 (A,wt=16): 271 c2 ^ (x ^ (c1 ^ x) ') != 0 | (c2 ^ x) ' = (c1 ^ x) '. [para(236(a,1),21(a,1)),demod(16(9)),xx(a)]. given #712 (F,wt=10): 5400 (x ^ c2) v (x ^ (c1 v (c2 ^ y))) ' = 1. [para(782(a,1),191(a,1,2,1,2))]. given #713 (F,wt=10): 5401 (x ^ c2) v (x ^ (c1 v (y ^ c2))) ' = 1. [para(788(a,1),191(a,1,2,1,2))]. given #714 (T,wt=10): 5421 c1 ^ (x v ((c2 v y) ^ (z v c1))) ' = 0. [para(4686(a,1),980(a,1,2)),demod(15(9))]. given #715 (T,wt=10): 5451 c1 ^ (x v ((y v c2) ^ (c1 v z))) ' = 0. [para(5025(a,1),980(a,1,2)),demod(15(9))]. given #716 (A,wt=19): 272 (c2 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c1 v x)))))) v (c1 ^ (x v (c1 ^ y))) ' = 1. [para(22(a,1),236(a,1,2,1))]. given #717 (F,wt=10): 5483 c1 ^ (x v ((c2 v y) ^ (z v c2))) ' = 0. [para(5034(a,1),980(a,1,2)),demod(15(9))]. given #718 (F,wt=10): 5515 c1 ^ (x v ((y v c2) ^ (z v c2))) ' = 0. [para(5035(a,1),980(a,1,2)),demod(15(9))]. given #719 (T,wt=10): 5551 c1 ^ (x v ((y v c2) ^ (z v c1))) ' = 0. [para(5330(a,1),980(a,1,2)),demod(15(9))]. given #720 (T,wt=10): 5610 (x v c2) ^ (y ^ c1) = y ^ c1. [para(76(a,1),248(a,2)),demod(826(8))]. given #721 (A,wt=11): 273 (c2 ^ x) v (y v (c1 ^ x) ') = 1. [para(236(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #722 (F,wt=10): 5674 c1 v (x v c2) ' != 1 | (c2 v x) ' = c1 '. [para(13(a,1),253(a,1,2,1))]. given #723 (F,wt=10): 5676 c1 v (c2 v x) ' != 1 | (x v c2) ' = c1 '. [para(13(a,1),258(a,1,2,1))]. given #724 (T,wt=10): 5678 c2 ^ (x ^ c1) ' != 0 | (c1 ^ x) ' = c2 '. [para(15(a,1),282(a,1,2,1))]. given #725 (T,wt=10): 5687 c2 ^ (c1 ^ x) ' != 0 | (x ^ c1) ' = c2 '. [para(15(a,1),288(a,1,2,1))]. given #726 (A,wt=15): 274 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y)) ' = 1. [para(26(a,1),236(a,1,1))]. given #727 (F,wt=10): 5890 c2 ^ (x v c1 ') != 0 | (c1 ' v x) ' = c2. [para(13(a,1),339(a,1,2))]. given #728 (F,wt=10): 5894 c2 ^ (c1 ' v x) != 0 | (x v c1 ') ' = c2. [para(13(a,1),340(a,1,2))]. given #729 (T,wt=10): 5896 (c2 v x) ^ c1 ' != 0 | (x v c2) ' = c1 '. [para(13(a,1),374(a,1,1))]. given #730 (T,wt=10): 5898 c1 ' ^ (x v c2) != 0 | (x v c2) ' = c1 '. [para(15(a,1),374(a,1))]. given #731 (A,wt=15): 275 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),236(a,1,2,1))]. given #732 (F,wt=10): 5920 (x v c2) ^ c1 ' != 0 | (c2 v x) ' = c1 '. [para(13(a,1),378(a,1,1))]. given #733 (F,wt=10): 5921 c1 ' ^ (c2 v x) != 0 | (c2 v x) ' = c1 '. [para(15(a,1),378(a,1))]. given #734 (T,wt=10): 5923 c1 v (x ^ c2 ') != 1 | (c2 ' ^ x) ' = c1. [para(15(a,1),410(a,1,2))]. given #735 (T,wt=10): 5925 c1 v (c2 ' ^ x) != 1 | (x ^ c2 ') ' = c1. [para(15(a,1),411(a,1,2))]. given #736 (A,wt=12): 277 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y) ' = 1. [para(29(a,1),236(a,1,2,1))]. given #737 (F,wt=8): 9085 (c2 ^ (c1 v x)) v (c1 ^ y) ' = 1. [para(277(a,1),178(a,1,2)),demod(13(6),64(6)),flip(a)]. given #738 (F,wt=8): 9114 (c1 ^ x) ' v (c2 ^ (c1 v y)) = 1. [para(9085(a,1),13(a,1)),flip(a)]. given #739 (T,wt=8): 9115 (c2 ^ (x v c1)) v (c1 ^ y) ' = 1. [para(13(a,1),9085(a,1,1,2))]. given #740 (T,wt=8): 9117 (c2 ^ (c1 v x)) v (y ^ c1) ' = 1. [para(15(a,1),9085(a,1,2,1))]. given #741 (A,wt=14): 278 (c2 ^ (x ^ ((c1 ^ x) v y))) v (c1 ^ x) ' = 1. [para(30(a,1),236(a,1,2,1))]. given #742 (F,wt=8): 9127 (c1 ^ x) ' v (c2 ^ (y v c1)) = 1. [para(13(a,1),9114(a,1,2,2))]. given #743 (F,wt=8): 9128 (x ^ c1) ' v (c2 ^ (c1 v y)) = 1. [para(15(a,1),9114(a,1,1,1))]. given #744 (T,wt=8): 9139 (c2 ^ (x v c1)) v (y ^ c1) ' = 1. [para(15(a,1),9115(a,1,2,1))]. given #745 (T,wt=8): 9200 (x ^ c1) ' v (c2 ^ (y v c1)) = 1. [para(15(a,1),9127(a,1,1,1))]. given #746 (A,wt=20): 283 c2 ^ ((c1 ^ x) ' v (c2 ^ ((c2 ^ (c1 ^ x) ') v y))) = c2 ^ ((c1 ^ x) ' v (c2 ^ y)). [para(279(a,1),22(a,1,2,2,2,2,2)),demod(39(12))]. given #747 (F,wt=10): 5926 c2 ' v (x ^ c1) != 1 | (x ^ c1) ' = c2 '. [para(13(a,1),460(a,1))]. given #748 (F,wt=10): 5927 (c1 ^ x) v c2 ' != 1 | (x ^ c1) ' = c2 '. [para(15(a,1),460(a,1,1))]. given #749 (T,wt=10): 6021 c2 ' v (c1 ^ x) != 1 | (c1 ^ x) ' = c2 '. [para(13(a,1),464(a,1))]. given #750 (T,wt=10): 6022 (x ^ c1) v c2 ' != 1 | (c1 ^ x) ' = c2 '. [para(15(a,1),464(a,1,1))]. given #751 (A,wt=20): 289 c2 ^ ((x ^ c1) ' v (c2 ^ ((c2 ^ (x ^ c1) ') v y))) = c2 ^ ((x ^ c1) ' v (c2 ^ y)). [para(281(a,1),22(a,1,2,2,2,2,2)),demod(39(12))]. given #752 (F,wt=10): 6203 c2 ^ (x v c1) != 1 | c1 != 0 | c1 ' = c2 ^ (c1 v x). [para(13(a,1),839(a,1,2))]. given #753 (F,wt=10): 6206 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (c1 v x)) ' = c1. [para(13(a,1),844(a,1,2))]. given #754 (T,wt=10): 6207 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (x ^ c2)) ' = c1. [para(22(a,1),844(a,1)),demod(782(6),15(15),23(15),13(16),124(16),788(17),65(16),788(15))]. given #755 (T,wt=10): 6209 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (c2 ^ x)) ' = c1. [para(51(a,1),844(a,1)),demod(782(6),15(15),23(15),13(16),124(16),782(17),65(16),782(15))]. given #756 (A,wt=14): 293 c2 ^ ((c1 v x) ^ c1 ') != 0 | (c2 ^ (c1 v x)) ' = c1 '. [para(270(a,1),21(a,1)),demod(16(10)),xx(a)]. given #757 (F,wt=10): 6210 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (x ^ c2)) ' = c1. [para(788(a,1),844(a,1)),demod(788(15))]. given #758 (F,wt=10): 6417 c1 v (c2 ^ (x v c1)) ' != 1 | c2 ^ (c1 v x) = c1. [para(13(a,1),853(a,1,2,1,2))]. given #759 (T,wt=10): 6418 c1 v (c1 v (c2 ^ x)) ' != 1 | c1 v (x ^ c2) = c1. [para(22(a,1),853(a,1,2,1)),demod(782(7),15(15),23(15),13(16),124(16),788(17),65(16),788(15))]. given #760 (T,wt=10): 6487 (c2 ^ c1 ') ' v (x ^ c1) = (c2 ^ c1 ') '. [para(6475(a,1),121(a,1,2,2))]. given #761 (A,wt=11): 296 x ^ (y ^ (y ^ x) ') = 0. [para(15(a,1),41(a,1,2,2,1))]. given #762 (F,wt=10): 6499 (x ^ (c2 ^ c1 ') ') v (x ^ c1) ' = 1. [para(6475(a,1),202(a,1,2,1,2))]. given #763 (F,wt=10): 6536 (c2 ^ c1 ') ' != 1 | c1 != 0 | (c2 ^ c1 ') ' = c1 '. [para(6481(a,1),21(b,1)),demod(6480(7)),flip(c)]. given #764 (T,wt=10): 6569 (x v c1) ^ (x v (c2 ^ c1 ') ') ' = 0. [para(6480(a,1),152(a,1,2,1,2))]. given #765 (T,wt=10): 6572 c1 ^ (((c2 ^ c1 ') ' ^ (c2 v x)) v y) = c1. [para(6480(a,1),3475(a,1,2,1,1))]. given #766 (A,wt=15): 297 x ^ (y ^ ((x ^ y) ' ^ z)) = 0. [para(41(a,1),16(a,1,1)),demod(81(2),16(5)),flip(a)]. given #767 (F,wt=10): 6574 c1 ^ (((c2 ^ c1 ') ' ^ (x v c2)) v y) = c1. [para(6480(a,1),3923(a,1,2,1,1))]. given #768 (F,wt=10): 6575 c1 ^ (x v ((c2 ^ c1 ') ' ^ (c2 v y))) = c1. [para(6480(a,1),3924(a,1,2,2,1))]. given #769 (T,wt=10): 6576 c1 ^ (((c2 v x) ^ (c2 ^ c1 ') ') v y) = c1. [para(6480(a,1),3925(a,1,2,1,2))]. given #770 (T,wt=10): 6578 (c1 ^ x) v (c2 ^ c1 ') ' = (c2 ^ c1 ') '. [para(6480(a,1),183(a,1,1)),demod(27(14)),flip(a)]. given #771 (A,wt=19): 298 x ^ (y ^ (z ^ (x ^ (y ^ z)) ')) = 0. [para(41(a,1),16(a,1)),demod(16(3)),flip(a)]. given #772 (F,wt=10): 6579 c1 ^ (x v ((c2 ^ c1 ') ' ^ (y v c2))) = c1. [para(6480(a,1),4222(a,1,2,2,1))]. given #773 (F,wt=10): 6580 c1 ^ (((x v c2) ^ (c2 ^ c1 ') ') v y) = c1. [para(6480(a,1),4224(a,1,2,1,2))]. given #774 (T,wt=10): 6581 c1 ^ (x v ((c2 v y) ^ (c2 ^ c1 ') ')) = c1. [para(6480(a,1),4253(a,1,2,2,2))]. given #775 (T,wt=10): 6582 c1 ^ (x v ((y v c2) ^ (c2 ^ c1 ') ')) = c1. [para(6480(a,1),5025(a,1,2,2,2))]. given #776 (A,wt=18): 299 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(41(a,1),21(b,1)),flip(c),xx(b)]. given #777 (F,wt=10): 6584 ((c2 ^ c1 ') ' ^ x) v (c1 ^ x) ' = 1. [para(6480(a,1),204(a,1,1,1))]. given #778 (F,wt=10): 6647 c1 v c2 ' != 1 | (c1 v c2 ') ^ (c1 v (c2 ^ x)) = c2. [para(1960(a,1),211(b,1)),demod(13(4),326(12),13(15),2153(21)),flip(c),xx(b)]. given #779 (T,wt=10): 6648 c1 v c2 ' != 1 | (c1 v c2 ') ^ (c1 v (x ^ c2)) = c2. [para(1970(a,1),211(b,1)),demod(13(4),326(12),13(15),2153(21)),flip(c),xx(b)]. given #780 (T,wt=10): 6886 c1 ' ^ (c2 ^ c1 ') ' != 0 | (c2 ^ c1 ') ' = c1. [para(6544(a,1),137(a,1)),demod(326(16),13(18),200(18),57(21)),flip(c),xx(a)]. given #781 (A,wt=15): 300 x ^ (y ^ (z ^ (x ^ z) ')) = 0. [para(41(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #782 (F,wt=10): 7203 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) ' = 1. [para(7086(a,1),801(a,1,2)),demod(13(9))]. given #783 (F,wt=10): 7239 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) ' = 1. [para(7090(a,1),801(a,1,2)),demod(13(9))]. given #784 (T,wt=10): 7280 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) ' = 1. [para(7184(a,1),801(a,1,2)),demod(13(9))]. given #785 (T,wt=10): 7310 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) ' = 1. [para(7186(a,1),801(a,1,2)),demod(13(9))]. given #786 (A,wt=19): 301 x ^ (y ^ (z ^ (y ^ (x ^ z)) ')) = 0. [para(26(a,1),41(a,1,2,2,1)),demod(16(5))]. given #787 (F,wt=10): 7338 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) ' = 1. [para(7187(a,1),801(a,1,2)),demod(13(9))]. given #788 (F,wt=10): 7367 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) ' = 1. [para(7195(a,1),801(a,1,2)),demod(13(9))]. given #789 (T,wt=10): 7397 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) ' = 1. [para(7220(a,1),801(a,1,2)),demod(13(9))]. given #790 (T,wt=10): 7430 c2 v (((x ^ c2) v (y ^ c1)) ^ z) ' = 1. [para(7222(a,1),801(a,1,2)),demod(13(9))]. given #791 (A,wt=13): 302 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(41(a,1),29(a,1,2)),demod(83(2)),flip(a)]. given #792 (F,wt=10): 7458 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) ' = 1. [para(7223(a,1),801(a,1,2)),demod(13(9))]. given #793 (F,wt=10): 7487 c2 v (((x ^ c1) v (y ^ c1)) ^ z) ' = 1. [para(7231(a,1),801(a,1,2)),demod(13(9))]. given #794 (T,wt=10): 7516 c2 v (((c1 ^ x) v (y ^ c2)) ^ z) ' = 1. [para(7265(a,1),801(a,1,2)),demod(13(9))]. given #795 (T,wt=10): 7558 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) ' = 1. [para(7266(a,1),801(a,1,2)),demod(13(9))]. given #796 (A,wt=14): 307 c2 ^ ((x v c1) ^ c1 ') != 0 | (c2 ^ (x v c1)) ' = c1 '. [para(276(a,1),21(a,1)),demod(16(10)),xx(a)]. given #797 (F,wt=10): 7583 c2 v (((c1 ^ x) v (y ^ c1)) ^ z) ' = 1. [para(7274(a,1),801(a,1,2)),demod(13(9))]. given #798 (F,wt=10): 7612 c2 v (x ^ ((y ^ c2) v (c1 ^ z))) ' = 1. [para(7297(a,1),801(a,1,2)),demod(13(9))]. given #799 (T,wt=10): 7641 c2 v (x ^ ((y ^ c1) v (c1 ^ z))) ' = 1. [para(7333(a,1),801(a,1,2)),demod(13(9))]. given #800 (T,wt=10): 7680 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z) ' = 1. [para(7354(a,1),801(a,1,2)),demod(13(9))]. given #801 (A,wt=11): 317 (x ^ c2) v ((c1 ^ x) ' v y) = 1. [para(268(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #802 (F,wt=10): 7709 c2 v (((x ^ c1) v (y ^ c2)) ^ z) ' = 1. [para(7383(a,1),801(a,1,2)),demod(13(9))]. given #803 (F,wt=10): 7734 c2 v (x ^ ((y ^ c1) v (c2 ^ z))) ' = 1. [para(7384(a,1),801(a,1,2)),demod(13(9))]. given #804 (T,wt=10): 7762 c2 v (x ^ ((y ^ c2) v (z ^ c1))) ' = 1. [para(7417(a,1),801(a,1,2)),demod(13(9))]. given #805 (T,wt=10): 7831 c2 v (x ^ ((y ^ c1) v (z ^ c1))) ' = 1. [para(7453(a,1),801(a,1,2)),demod(13(9))]. given #806 (A,wt=15): 319 (x ^ (y ^ c2)) v (c1 ^ (x ^ y)) ' = 1. [para(16(a,1),268(a,1,1))]. given #807 (F,wt=10): 7859 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) ' = 1. [para(7503(a,1),801(a,1,2)),demod(13(9))]. given #808 (F,wt=10): 7884 c2 v (x ^ ((c1 ^ y) v (z ^ c1))) ' = 1. [para(7554(a,1),801(a,1,2)),demod(13(9))]. given #809 (T,wt=10): 7908 c2 v (x ^ ((c1 ^ y) v (c1 ^ z))) ' = 1. [para(7627(a,1),801(a,1,2)),demod(13(9))]. given #810 (T,wt=10): 7970 c2 v (x ^ ((y ^ c1) v (z ^ c2))) ' = 1. [para(7696(a,1),801(a,1,2)),demod(13(9))]. given #811 (A,wt=16): 320 x ^ (c2 ^ (c1 ^ x) ') != 0 | (c1 ^ x) ' = (x ^ c2) '. [para(268(a,1),21(a,1)),demod(16(9)),flip(c),xx(a)]. given #812 (F,wt=10): 7993 c1 v (c2 ^ (c1 v x)) ' != 1 | c2 ^ (x v c1) = c1. [para(13(a,1),859(a,1,2,1,2))]. given #813 (F,wt=10): 7995 x ^ ((x ^ c1) v (c1 ^ y)) = x ^ c1. [para(227(a,1),30(a,1,2)),demod(6889(7))]. given #814 (T,wt=10): 7999 x ^ ((c1 ^ x) v (c1 ^ y)) = x ^ c1. [para(227(a,1),159(a,1,2)),demod(4747(7))]. given #815 (T,wt=10): 8004 c2 ^ (c1 v x) != 1 | c1 != 0 | c1 ' = c2 ^ (x v c1). [para(13(a,1),923(a,1,2))]. given #816 (A,wt=11): 321 (x ^ c2) v (y v (c1 ^ x) ') = 1. [para(268(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #817 (F,wt=10): 8006 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (x v c1)) ' = c1. [para(13(a,1),925(a,1,2))]. given #818 (F,wt=10): 8008 c2 != 1 | c1 v (x ^ c2) != 0 | c2 ' = c1 v (c2 ^ x). [para(15(a,1),1029(b,1,2))]. given #819 (T,wt=10): 8011 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (c2 ^ x)) ' = c2. [para(15(a,1),1034(b,1,2))]. given #820 (T,wt=10): 8013 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (c1 v x)) ' = c2. [para(604(a,1),1034(b,1)),demod(604(15))]. given #821 (A,wt=20): 322 x v (y v z) != 1 | z ^ (x v y) != 0 | z ' = x v y. [para(14(a,1),43(a,1))]. given #822 (F,wt=10): 8014 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (x v c1)) ' = c2. [para(609(a,1),1034(b,1)),demod(609(15))]. given #823 (F,wt=10): 8108 c2 ^ (c1 v (x ^ c2)) ' != 0 | c1 v (c2 ^ x) = c2. [para(15(a,1),1046(a,1,2,1,2))]. given #824 (T,wt=10): 8111 c1 ^ ((c2 ^ x) v (x ^ y)) = c1 ^ x. [para(22(a,1),234(a,1,2)),demod(6889(6))]. given #825 (T,wt=10): 8143 (c1 ^ ((c2 ^ x) v y)) v (c1 ^ x) ' = 1. [para(234(a,1),202(a,1,2,1))]. given #826 (A,wt=12): 323 x v y != 1 | x ^ y != 0 | y ' = x. [para(15(a,1),43(b,1))]. given #827 (F,wt=10): 8164 c2 ^ (c1 v (c2 ^ x)) ' != 0 | c1 v (x ^ c2) = c2. [para(15(a,1),1054(a,1,2,1,2))]. given #828 (F,wt=10): 8184 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (x ^ c2)) ' = c2. [para(15(a,1),1122(b,1,2))]. given #829 (T,wt=10): 8231 (c2 ^ (c1 v x)) ' ^ (y ^ c1) = 0. [para(843(a,1),238(a,1,1)),demod(60(10),843(15))]. given #830 (T,wt=10): 8232 (c2 ^ (x v c1)) ' ^ (y ^ c1) = 0. [para(848(a,1),238(a,1,1)),demod(60(10),848(15))]. given #831 (A,wt=20): 324 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z) ' = x. [para(16(a,1),43(b,1))]. given #832 (F,wt=10): 8284 c1 v ((c2 ^ c1 ') ' ^ (x ^ c2)) = c1. [para(6475(a,1),238(a,1,1)),demod(6475(17))]. given #833 (F,wt=10): 8356 (x v c2) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(13(a,1),2180(a,1,1))]. given #834 (T,wt=10): 8357 (c1 v (c2 ^ x)) ^ (c2 v y) = c1 v (c2 ^ x). [para(2180(a,1),15(a,1)),flip(a)]. given #835 (T,wt=8): 10052 (c2 v x) ' ^ (c1 v (c2 ^ y)) = 0. [para(8357(a,1),980(a,1,2))]. given #836 (A,wt=12): 325 1 != x | x ^ y != 0 | (x ^ y) ' = x. [para(18(a,1),43(a,1)),demod(15(4),88(4)),flip(a)]. given #837 (F,wt=8): 10058 (x v c2) ' ^ (c1 v (c2 ^ y)) = 0. [para(13(a,1),10052(a,1,1,1))]. given #838 (F,wt=8): 10059 (c1 v (c2 ^ x)) ^ (c2 v y) ' = 0. [para(10052(a,1),15(a,1)),flip(a)]. given #839 (T,wt=8): 10060 (c2 v x) ' ^ (c1 v (y ^ c2)) = 0. [para(15(a,1),10052(a,1,2,2))]. given #840 (T,wt=8): 10076 (c1 v (c2 ^ x)) ^ (y v c2) ' = 0. [para(10058(a,1),15(a,1)),flip(a)]. given #841 (A,wt=20): 327 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z) ' = y. [para(25(a,1),43(a,1))]. given #842 (F,wt=8): 10077 (x v c2) ' ^ (c1 v (y ^ c2)) = 0. [para(15(a,1),10058(a,1,2,2))]. given #843 (F,wt=8): 10085 (c1 v (x ^ c2)) ^ (c2 v y) ' = 0. [para(15(a,1),10059(a,1,1,2))]. given #844 (T,wt=8): 10102 (c1 v (x ^ c2)) ^ (y v c2) ' = 0. [para(15(a,1),10076(a,1,1,2))]. given #845 (T,wt=10): 8373 (x v c2) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(13(a,1),2181(a,1,1))]. given #846 (A,wt=20): 328 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z ' = x ^ y. [para(26(a,1),43(b,1))]. given #847 (F,wt=10): 8374 (c1 v (x ^ c2)) ^ (c2 v y) = c1 v (x ^ c2). [para(2181(a,1),15(a,1)),flip(a)]. given #848 (F,wt=10): 8445 (c1 v x) ^ (x v (c2 ^ (c1 v y))) ' = 0. [para(13(a,1),2549(a,1,1))]. given #849 (T,wt=10): 8446 (x v c1) ^ ((c2 ^ (c1 v y)) v x) ' = 0. [para(13(a,1),2549(a,1,2,1))]. given #850 (T,wt=10): 8456 (c1 v x) ^ (x v (c2 ^ (y v c1))) ' = 0. [para(13(a,1),2550(a,1,1))]. given #851 (A,wt=24): 329 x v (y v z) != 1 | x v y != 0 | (x v y) ' = x v (y v z). [para(28(a,1),43(b,1)),demod(13(4),25(4),25(3),14(2),128(4))]. given #852 (F,wt=10): 8457 (x v c1) ^ ((c2 ^ (y v c1)) v x) ' = 0. [para(13(a,1),2550(a,1,2,1))]. given #853 (F,wt=10): 8623 (c2 ^ (c1 v x)) v (c1 ^ y) = c2 ^ (c1 v x). [para(4763(a,1),13(a,1)),flip(a)]. given #854 (T,wt=10): 8625 (x ^ c1) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(15(a,1),4763(a,1,1))]. given #855 (T,wt=10): 8656 (c2 ^ (x v c1)) v (c1 ^ y) = c2 ^ (x v c1). [para(4765(a,1),13(a,1)),flip(a)]. given #856 (A,wt=12): 330 1 != x | y ^ x != 0 | (y ^ x) ' = x. [para(33(a,1),43(a,1)),demod(15(4),90(4)),flip(a)]. given #857 (F,wt=10): 8659 (x ^ c1) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(15(a,1),4765(a,1,1))]. given #858 (F,wt=10): 8838 (c2 ^ x) v (x ^ (c1 v (c2 ^ y))) ' = 1. [para(15(a,1),5400(a,1,1))]. given #859 (T,wt=10): 8839 (x ^ c2) v ((c1 v (c2 ^ y)) ^ x) ' = 1. [para(15(a,1),5400(a,1,2,1))]. given #860 (T,wt=10): 8849 (c2 ^ x) v (x ^ (c1 v (y ^ c2))) ' = 1. [para(15(a,1),5401(a,1,1))]. given #861 (A,wt=20): 334 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y) ' = x. [para(31(a,1),43(a,1)),demod(15(6))]. given #862 (F,wt=8): 10301 c1 v x != 1 | c1 != 0 | (c1 v x) ' = c1. [para(23(a,1),334(b,1,2,1)),demod(17(8),23(10))]. given #863 (F,wt=8): 10307 c2 != 1 | c2 ^ x != 0 | (c2 ^ x) ' = c2. [para(393(a,1),334(b,1,2)),demod(129(4),88(7),393(12))]. given #864 (T,wt=8): 10314 x v c1 != 1 | c1 != 0 | (c1 v x) ' = c1. [para(13(a,1),10301(a,1))]. given #865 (T,wt=8): 10316 x v c1 != 1 | c1 != 0 | (x v c1) ' = c1. [para(69(a,1),10301(a,1)),demod(69(12))]. given #866 (A,wt=12): 335 x ^ (x ^ y) ' != 0 | x ^ y = x. [para(179(a,1),43(a,1)),demod(15(6),326(11)),xx(a)]. given #867 (F,wt=8): 10318 c2 != 1 | x ^ c2 != 0 | (c2 ^ x) ' = c2. [para(15(a,1),10307(b,1))]. given #868 (F,wt=8): 10320 c2 != 1 | x ^ c2 != 0 | (x ^ c2) ' = c2. [para(76(a,1),10307(b,1)),demod(76(12))]. given #869 (T,wt=8): 10323 c1 v x != 1 | c1 != 0 | (x v c1) ' = c1. [para(13(a,1),10316(a,1))]. given #870 (T,wt=8): 10329 c2 != 1 | c2 ^ x != 0 | (x ^ c2) ' = c2. [para(15(a,1),10320(b,1))]. given #871 (A,wt=12): 336 x ^ (y ^ x) ' != 0 | y ^ x = x. [para(190(a,1),43(a,1)),demod(15(6),326(11)),xx(a)]. given #872 (F,wt=10): 8850 (x ^ c2) v ((c1 v (y ^ c2)) ^ x) ' = 1. [para(15(a,1),5401(a,1,2,1))]. given #873 (F,wt=10): 9015 c1 ' ^ (c2 v x) != 0 | (x v c2) ' = c1 '. [para(15(a,1),5896(a,1))]. given #874 (T,wt=10): 9057 c1 ' ^ (x v c2) != 0 | (c2 v x) ' = c1 '. [para(15(a,1),5920(a,1))]. given #875 (T,wt=10): 9249 c2 ' v (c1 ^ x) != 1 | (x ^ c1) ' = c2 '. [para(15(a,1),5926(a,1,2))]. given #876 (A,wt=24): 338 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z)) ' = x. [para(32(a,1),43(a,1)),demod(15(7))]. given #877 (F,wt=9): 10345 c1 v c2 ' != 1 | (c2 ^ (c1 v c2 ')) ' = c2 '. [para(503(a,1),338(b,1)),demod(13(4),13(14),15(16),604(17)),xx(b)]. given #878 (F,wt=10): 9251 c2 ' v (x ^ c1) != 1 | (c1 ^ x) ' = c2 '. [para(15(a,1),6021(a,1,2))]. given #879 (T,wt=10): 9275 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (c2 ^ x)) ' = c1. [para(15(a,1),6209(a,1,2))]. given #880 (T,wt=10): 9279 (x ^ c1) v (c2 ^ c1 ') ' = (c2 ^ c1 ') '. [para(6487(a,1),13(a,1)),flip(a)]. given #881 (A,wt=24): 341 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z)) ' = x ^ y. [para(34(a,1),43(a,1)),demod(15(7),26(7),26(6),16(5),241(7))]. given #882 (F,wt=10): 9281 (c2 ^ c1 ') ' v (c1 ^ x) = (c2 ^ c1 ') '. [para(15(a,1),6487(a,1,2))]. given #883 (F,wt=10): 9309 (x ^ c1) ' v (x ^ (c2 ^ c1 ') ') = 1. [para(6499(a,1),13(a,1)),flip(a)]. given #884 (T,wt=10): 9311 ((c2 ^ c1 ') ' ^ x) v (x ^ c1) ' = 1. [para(15(a,1),6499(a,1,1))]. given #885 (T,wt=10): 9312 (x ^ (c2 ^ c1 ') ') v (c1 ^ x) ' = 1. [para(15(a,1),6499(a,1,2,1))]. given #886 (A,wt=18): 342 x ^ (y v (x v y) ') != 0 | (y v (x v y) ') ' = x. [para(38(a,1),43(a,1)),demod(15(7)),xx(a)]. given #887 (F,wt=10): 9321 (c1 v x) ^ (x v (c2 ^ c1 ') ') ' = 0. [para(13(a,1),6569(a,1,1))]. given #888 (F,wt=10): 9322 (x v c1) ^ ((c2 ^ c1 ') ' v x) ' = 0. [para(13(a,1),6569(a,1,2,1))]. given #889 (T,wt=10): 9529 (c1 ^ x) ' v ((c2 ^ c1 ') ' ^ x) = 1. [para(6584(a,1),13(a,1)),flip(a)]. given #890 (T,wt=10): 9826 x ^ ((c1 ^ y) v (x ^ c1)) = x ^ c1. [para(13(a,1),7995(a,1,2))]. given #891 (A,wt=14): 343 c2 ^ (x ^ (c1 ^ x) ') != 0 | c2 ^ x = c1 ^ x. [para(236(a,1),43(a,1)),demod(15(9),16(9),326(15)),flip(c),xx(a)]. given #892 (F,wt=10): 9827 x ^ ((x ^ c1) v (y ^ c1)) = x ^ c1. [para(15(a,1),7995(a,1,2,2))]. given #893 (F,wt=10): 9843 x ^ ((c1 ^ y) v (c1 ^ x)) = x ^ c1. [para(13(a,1),7999(a,1,2))]. given #894 (T,wt=10): 9844 x ^ ((c1 ^ x) v (y ^ c1)) = x ^ c1. [para(15(a,1),7999(a,1,2,2))]. given #895 (T,wt=10): 9870 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (c1 v x)) ' = c2. [para(13(a,1),8013(b,1,2))]. given #896 (A,wt=12): 346 c2 ^ (c1 ' ^ (c1 v x)) != 0 | c2 ^ (c1 v x) = c1. [para(270(a,1),43(a,1)),demod(26(10),326(15)),flip(c),xx(a)]. given #897 (F,wt=9): 10580 c2 ^ c1 ' != 0 | c1 v (c2 ^ (c1 ' v x)) = c1. [para(1253(a,1),346(a,1,2)),demod(88(6),782(15))]. given #898 (F,wt=9): 10581 c2 ^ c1 ' != 0 | c1 v (c2 ^ (x v c1 ')) = c1. [para(1257(a,1),346(a,1,2)),demod(88(6),782(15))]. given #899 (T,wt=10): 9893 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (x v c1)) ' = c2. [para(13(a,1),8014(b,1,2))]. given #900 (T,wt=10): 9894 c1 ^ ((x ^ y) v (c2 ^ x)) = c1 ^ x. [para(13(a,1),8111(a,1,2))]. given #901 (A,wt=12): 347 c2 ^ (c1 ' ^ (x v c1)) != 0 | c2 ^ (x v c1) = c1. [para(276(a,1),43(a,1)),demod(26(10),326(15)),flip(c),xx(a)]. given #902 (F,wt=10): 9895 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(15(a,1),8111(a,1,2,1))]. given #903 (F,wt=10): 9896 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(15(a,1),8111(a,1,2,2))]. given #904 (T,wt=10): 9931 (c1 ^ x) ' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(8143(a,1),13(a,1)),flip(a)]. given #905 (T,wt=10): 9932 (c1 ^ (x v (c2 ^ y))) v (c1 ^ y) ' = 1. [para(13(a,1),8143(a,1,1,2))]. given #906 (A,wt=14): 348 x ^ (c2 ^ (c1 ^ x) ') != 0 | c1 ^ x = x ^ c2. [para(268(a,1),43(a,1)),demod(15(9),16(9),326(15)),xx(a)]. given #907 (F,wt=8): 10758 c1 v ((x ^ c1) v (c1 ^ y)) ' = 1. [para(7333(a,1),9932(a,1,1,2)),demod(23(3),6889(8))]. given #908 (F,wt=8): 10779 c1 v ((x ^ c1) v (y ^ c1)) ' = 1. [para(15(a,1),10758(a,1,2,1,2))]. given #909 (T,wt=10): 9934 (c1 ^ ((x ^ c2) v y)) v (c1 ^ x) ' = 1. [para(15(a,1),8143(a,1,1,2,1))]. given #910 (T,wt=10): 9935 (c1 ^ ((c2 ^ x) v y)) v (x ^ c1) ' = 1. [para(15(a,1),8143(a,1,2,1))]. given #911 (A,wt=11): 349 (c2 ^ x) v ((x ^ c1) ' v y) = 1. [para(269(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #912 (F,wt=10): 9940 (c1 ^ ((x ^ c2) v y)) v (x ^ c1) ' = 1. [para(80(a,1),8143(a,1,2,1)),demod(90(5))]. given #913 (F,wt=10): 10039 (c1 v (c2 ^ x)) ^ (y v c2) = c1 v (c2 ^ x). [para(8356(a,1),15(a,1)),flip(a)]. given #914 (T,wt=10): 10130 (c1 v (x ^ c2)) ^ (y v c2) = c1 v (x ^ c2). [para(8373(a,1),15(a,1)),flip(a)]. given #915 (T,wt=10): 10164 (c1 v x) ^ ((c2 ^ (c1 v y)) v x) ' = 0. [para(13(a,1),8445(a,1,2,1))]. given #916 (A,wt=15): 350 (c2 ^ (x ^ y)) v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),269(a,1,2,1))]. given #917 (F,wt=10): 10192 (c1 v x) ^ ((c2 ^ (y v c1)) v x) ' = 0. [para(13(a,1),8456(a,1,2,1))]. given #918 (F,wt=10): 10214 (c2 ^ (c1 v x)) v (y ^ c1) = c2 ^ (c1 v x). [para(15(a,1),8623(a,1,2))]. given #919 (T,wt=10): 10230 (c2 ^ (x v c1)) v (y ^ c1) = c2 ^ (x v c1). [para(15(a,1),8656(a,1,2))]. given #920 (T,wt=10): 10260 (c2 ^ x) v ((c1 v (c2 ^ y)) ^ x) ' = 1. [para(15(a,1),8838(a,1,2,1))]. given #921 (A,wt=16): 351 c2 ^ (x ^ (x ^ c1) ') != 0 | (c2 ^ x) ' = (x ^ c1) '. [para(269(a,1),21(a,1)),demod(16(9)),xx(a)]. given #922 (F,wt=10): 10267 c1 v ((c2 ^ c1 ') ' ^ (c1 v (c2 ^ x))) ' = 1. [para(6475(a,1),8838(a,1,1))]. given #923 (F,wt=10): 10289 (c2 ^ x) v ((c1 v (y ^ c2)) ^ x) ' = 1. [para(15(a,1),8849(a,1,2,1))]. given #924 (T,wt=10): 10296 c1 v ((c2 ^ c1 ') ' ^ (c1 v (x ^ c2))) ' = 1. [para(6475(a,1),8849(a,1,1))]. given #925 (T,wt=10): 10346 x v c2 != 1 | 0 != x | (c2 v x) ' = x. [para(765(a,1),338(b,1,2,2)),demod(25(8),131(8),27(7),765(12),25(10),131(10)),flip(b)]. given #926 (A,wt=11): 352 (c2 ^ x) v (y v (x ^ c1) ') = 1. [para(269(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #927 (F,wt=10): 10385 (c1 ^ x) ' v (x ^ (c2 ^ c1 ') ') = 1. [para(15(a,1),9309(a,1,1,1))]. given #928 (F,wt=10): 10386 (x ^ c1) ' v ((c2 ^ c1 ') ' ^ x) = 1. [para(15(a,1),9309(a,1,2))]. given #929 (T,wt=10): 10454 (c1 v x) ^ ((c2 ^ c1 ') ' v x) ' = 0. [para(13(a,1),9321(a,1,2,1))]. given #930 (T,wt=10): 10483 x ^ ((y ^ c1) v (x ^ c1)) = x ^ c1. [para(15(a,1),9826(a,1,2,1))]. given #931 (A,wt=14): 353 c2 ^ (x ^ (x ^ c1) ') != 0 | c2 ^ x = x ^ c1. [para(269(a,1),43(a,1)),demod(15(9),16(9),326(15)),flip(c),xx(a)]. given #932 (F,wt=10): 10523 x ^ ((y ^ c1) v (c1 ^ x)) = x ^ c1. [para(15(a,1),9843(a,1,2,1))]. given #933 (F,wt=10): 10582 c1 ^ ((x ^ y) v (c2 ^ y)) = c1 ^ y. [para(15(a,1),9894(a,1,2,1))]. given #934 (T,wt=10): 10583 c1 ^ ((x ^ y) v (x ^ c2)) = c1 ^ x. [para(15(a,1),9894(a,1,2,2))]. given #935 (T,wt=10): 10612 c2 ^ c1 ' != 0 | c2 ^ (c1 v ((c2 v x) ^ c1 ')) = c1. [para(164(a,1),347(a,1)),demod(13(14))]. given #936 (A,wt=11): 354 (x ^ c2) v ((x ^ c1) ' v y) = 1. [para(318(a,1),14(a,1,1)),demod(64(2)),flip(a)]. given #937 (F,wt=10): 10613 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(15(a,1),9895(a,1,2,2))]. given #938 (F,wt=10): 10678 (c1 ^ x) ' v (c1 ^ (y v (c2 ^ x))) = 1. [para(13(a,1),9931(a,1,2,2))]. given #939 (T,wt=10): 10679 (x ^ c1) ' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(15(a,1),9931(a,1,1,1))]. given #940 (T,wt=10): 10680 (c1 ^ x) ' v (c1 ^ ((x ^ c2) v y)) = 1. [para(15(a,1),9931(a,1,2,2,1))]. given #941 (A,wt=16): 355 x ^ (c2 ^ (x ^ c1) ') != 0 | (x ^ c2) ' = (x ^ c1) '. [para(318(a,1),21(a,1)),demod(16(9)),xx(a)]. given #942 (F,wt=9): 11124 (c1 ^ x) ' v (c1 ^ (x v y)) = 1. [para(140(a,1),10680(a,1,2,2)),demod(15(7),53(8))]. given #943 (F,wt=9): 11127 (c1 ^ x) ' v (c1 ^ (y v x)) = 1. [para(13(a,1),11124(a,1,2,2))]. given #944 (T,wt=9): 11129 (x ^ c1) ' v (c1 ^ (x v y)) = 1. [para(15(a,1),11124(a,1,1,1))]. given #945 (T,wt=9): 11147 (x ^ c1) ' v (c1 ^ (y v x)) = 1. [para(15(a,1),11127(a,1,1,1))]. given #946 (A,wt=11): 356 (x ^ c2) v (y v (x ^ c1) ') = 1. [para(318(a,1),25(a,1,2)),demod(72(2)),flip(a)]. given #947 (F,wt=9): 11177 (c1 ^ (x v y)) v (y ^ c1) ' = 1. [para(11147(a,1),13(a,1)),flip(a)]. given #948 (F,wt=10): 10683 (x ^ c1) ' v (c1 ^ ((x ^ c2) v y)) = 1. [para(80(a,1),9931(a,1,1,1)),demod(90(8))]. given #949 (T,wt=10): 10689 (c1 ^ x) ' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(88(a,1),9931(a,1,1,1)),demod(26(8),53(8))]. given #950 (T,wt=10): 10721 (c1 ^ (x v (y ^ c2))) v (c1 ^ y) ' = 1. [para(15(a,1),9932(a,1,1,2,2))]. given #951 (A,wt=14): 357 x ^ (c2 ^ (x ^ c1) ') != 0 | x ^ c2 = x ^ c1. [para(318(a,1),43(a,1)),demod(15(9),16(9),326(15)),flip(c),xx(a)]. given #952 (F,wt=10): 10722 (c1 ^ (x v (c2 ^ y))) v (y ^ c1) ' = 1. [para(15(a,1),9932(a,1,2,1))]. given #953 (F,wt=10): 10724 (c1 ^ (x v (y ^ c2))) v (y ^ c1) ' = 1. [para(80(a,1),9932(a,1,2,1)),demod(90(5))]. given #954 (T,wt=10): 10887 c1 v ((c1 v (c2 ^ x)) ^ (c2 ^ c1 ') ') ' = 1. [para(6475(a,1),10260(a,1,1))]. given #955 (T,wt=10): 10912 c1 v ((c1 v (x ^ c2)) ^ (c2 ^ c1 ') ') ' = 1. [para(6475(a,1),10289(a,1,1))]. given #956 (A,wt=20): 358 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x) ' = y. [para(13(a,1),44(a,1)),demod(14(2))]. given #957 (F,wt=10): 10987 c1 ^ ((x ^ y) v (y ^ c2)) = c1 ^ y. [para(15(a,1),10582(a,1,2,2))]. given #958 (F,wt=10): 11080 (x ^ c1) ' v (c1 ^ (y v (c2 ^ x))) = 1. [para(15(a,1),10678(a,1,1,1))]. given #959 (T,wt=10): 11081 (c1 ^ x) ' v (c1 ^ (y v (x ^ c2))) = 1. [para(15(a,1),10678(a,1,2,2,2))]. given #960 (T,wt=10): 11083 (x ^ c1) ' v (c1 ^ (y v (x ^ c1))) = 1. [para(54(a,1),10678(a,1,2,2,2)),demod(90(4))]. given #961 (A,wt=20): 359 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y) ' = z. [para(13(a,1),44(b,1,1))]. given #962 (F,wt=10): 11084 (x ^ c1) ' v (c1 ^ (y v (x ^ c2))) = 1. [para(80(a,1),10678(a,1,1,1)),demod(90(8))]. given #963 (F,wt=10): 11090 (c1 ^ x) ' v (c1 ^ (y v (c1 ^ x))) = 1. [para(88(a,1),10678(a,1,1,1)),demod(26(8),53(8))]. given #964 (T,wt=10): 11189 (x ^ c1) ' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(15(a,1),10689(a,1,1,1))]. given #965 (T,wt=10): 11190 (c1 ^ x) ' v (c1 ^ ((x ^ c1) v y)) = 1. [para(15(a,1),10689(a,1,2,2,1))]. given #966 (A,wt=20): 360 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y) ' = z. [para(15(a,1),44(b,1))]. given #967 (F,wt=10): 11265 (c1 ^ x) ' v (c1 ^ (y v (x ^ c1))) = 1. [para(15(a,1),11083(a,1,1,1))]. given #968 (F,wt=10): 11266 (x ^ c1) ' v (c1 ^ (y v (c1 ^ x))) = 1. [para(15(a,1),11083(a,1,2,2,2))]. given #969 (T,wt=10): 11321 (c1 ^ (x v (y ^ c1))) v (c1 ^ y) ' = 1. [para(11265(a,1),13(a,1)),flip(a)]. given #970 (T,wt=10): 11329 (c1 ^ (x v (c1 ^ y))) v (y ^ c1) ' = 1. [para(11266(a,1),13(a,1)),flip(a)]. given #971 (A,wt=16): 361 x v y != 1 | y ^ z != 0 | (x v y) ' = y ^ z. [para(18(a,1),44(a,1,2)),demod(26(6),94(6))]. given #972 (F,wt=11): 369 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1) ' = c2. [para(124(a,1),44(a,1,2)),demod(15(8))]. given #973 (F,wt=11): 395 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1 ' = x ^ c2. [para(80(a,1),21(b,1))]. given #974 (T,wt=11): 412 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x) ' = c1. [para(53(a,1),45(b,1)),demod(13(4))]. given #975 (T,wt=11): 423 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2) ' = c1. [para(80(a,1),45(b,1)),demod(13(4))]. given #976 (A,wt=14): 362 (x v y) ^ y ' != 0 | (x v y) ' = y '. [para(19(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #977 (F,wt=11): 430 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2 ' = x v c1. [para(132(a,1),21(a,1))]. given #978 (F,wt=11): 445 (x v c1) ^ ((x v c2) ' ^ y) = 0. [para(433(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #979 (T,wt=11): 447 (x v c1) ^ (y ^ (x v c2) ') = 0. [para(433(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #980 (T,wt=11): 472 c1 v (c2 ^ x) != 1 | x ^ c1 != 0 | (c2 ^ x) ' = c1. [para(54(a,1),46(b,1)),demod(13(4))]. given #981 (A,wt=20): 365 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x) ' = z. [para(25(a,1),44(a,1))]. given #982 (F,wt=11): 477 (c1 v x) ^ ((x v c2) ' ^ y) = 0. [para(441(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #983 (F,wt=11): 480 (c1 v x) ^ (y ^ (x v c2) ') = 0. [para(441(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #984 (T,wt=11): 485 (x v c1) ^ ((c2 v x) ' ^ y) = 0. [para(442(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #985 (T,wt=11): 489 (x v c1) ^ (y ^ (c2 v x) ') = 0. [para(442(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #986 (A,wt=16): 366 x v y != 1 | x v y != 0 | (x v y) ' = x v y. [para(35(a,1),44(b,1)),demod(100(2),65(2))]. given #987 (F,wt=11): 533 (c1 v x) ^ ((c2 v x) ' ^ y) = 0. [para(476(a,1),16(a,1,1)),demod(81(2)),flip(a)]. given #988 (F,wt=11): 535 (c1 v x) ^ (y ^ (c2 v x) ') = 0. [para(476(a,1),26(a,1,2)),demod(83(2)),flip(a)]. given #989 (T,wt=11): 543 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x) ' = c2. [para(133(a,1),44(a,1)),demod(15(8))]. given #990 (T,wt=11): 708 (x v y) ^ (y v x) = x v y. [para(69(a,1),28(a,1,2))]. given #991 (A,wt=12): 367 x v y != 1 | 0 != y | (x v y) ' = y. [para(36(a,1),44(a,1,2)),demod(15(5),27(5)),flip(b)]. given #992 (F,wt=11): 709 (x v (y ^ z)) ^ (x v y) ' = 0. [para(69(a,1),151(a,1,2,1))]. given #993 (F,wt=10): 11398 (c1 v ((c2 v x) ^ y)) ^ (c2 v x) ' = 0. [para(131(a,1),709(a,1,2,1))]. given #994 (T,wt=10): 11399 (c1 v ((x v c2) ^ y)) ^ (x v c2) ' = 0. [para(133(a,1),709(a,1,2,1))]. given #995 (T,wt=10): 11402 (c2 v ((x v c1) ^ y)) ^ (c2 v x) ' = 0. [para(428(a,1),709(a,1,2,1))]. given #996 (A,wt=12): 370 x v c2 != 1 | c1 ^ y != 0 | (x v c2) ' = c1 ^ y. [para(127(a,1),44(a,1,2)),demod(26(9),248(9))]. given #997 (F,wt=10): 11423 (c1 v ((x v c2) ^ y)) ^ (c2 v x) ' = 0. [para(13(a,1),11398(a,1,1,2,1))]. given #998 (F,wt=10): 11424 (c1 v ((c2 v x) ^ y)) ^ (x v c2) ' = 0. [para(13(a,1),11398(a,1,2,1))]. given #999 (T,wt=10): 11425 (c2 v x) ' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(11398(a,1),15(a,1)),flip(a)]. given #1000 (T,wt=10): 11426 (c1 v (x ^ (c2 v y))) ^ (c2 v y) ' = 0. [para(15(a,1),11398(a,1,1,2))]. given #1001 (A,wt=18): 372 (x v y) ^ (y ^ z) ' != 0 | (x v y) ' = (y ^ z) '. [para(179(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1002 (F,wt=10): 11435 (x v c2) ' ^ (c1 v ((x v c2) ^ y)) = 0. [para(11399(a,1),15(a,1)),flip(a)]. given #1003 (F,wt=9): 11520 (x v c2) ' ^ (c2 v (x ^ y)) = 0. [para(183(a,1),11435(a,1,2,2)),demod(13(7),131(8))]. given #1004 (T,wt=9): 11524 (x v c2) ' ^ (c2 v (y ^ x)) = 0. [para(15(a,1),11520(a,1,2,2))]. given #1005 (T,wt=9): 11535 (c2 v x) ' ^ (c2 v (y ^ x)) = 0. [para(13(a,1),11524(a,1,1,1))]. given #1006 (A,wt=18): 373 (x v y) ^ (z ^ y) ' != 0 | (x v y) ' = (z ^ y) '. [para(190(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1007 (F,wt=9): 11537 (c2 v (x ^ y)) ^ (y v c2) ' = 0. [para(11524(a,1),15(a,1)),flip(a)]. given #1008 (F,wt=10): 11436 (c1 v (x ^ (y v c2))) ^ (y v c2) ' = 0. [para(15(a,1),11399(a,1,1,2))]. given #1009 (T,wt=10): 11445 (c2 v ((c1 v x) ^ y)) ^ (c2 v x) ' = 0. [para(13(a,1),11402(a,1,1,2,1))]. given #1010 (T,wt=10): 11446 (c2 v ((x v c1) ^ y)) ^ (x v c2) ' = 0. [para(13(a,1),11402(a,1,2,1))]. given #1011 (A,wt=20): 375 x v y != 1 | (x v y) ^ z != 0 | (x v y) ' = (x v y) ^ z. [para(32(a,1),44(a,1)),demod(88(7))]. given #1012 (F,wt=10): 11447 (c2 v x) ' ^ (c2 v ((x v c1) ^ y)) = 0. [para(11402(a,1),15(a,1)),flip(a)]. given #1013 (F,wt=10): 11448 (c2 v (x ^ (y v c1))) ^ (c2 v y) ' = 0. [para(15(a,1),11402(a,1,1,2))]. given #1014 (T,wt=8): 11647 c2 ^ ((x v c2) ^ (c2 v y)) ' = 0. [para(3937(a,1),11448(a,1,1,2)),demod(13(3),124(3),3263(8))]. given #1015 (T,wt=8): 11677 c2 ^ ((x v c2) ^ (y v c2)) ' = 0. [para(13(a,1),11647(a,1,2,1,2))]. given #1016 (A,wt=14): 376 (x v c2) ^ (c1 ' v y) != 0 | (x v c2) ' = c1 ' v y. [para(206(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1017 (F,wt=10): 11487 (c2 v x) ' ^ (c1 v ((x v c2) ^ y)) = 0. [para(11423(a,1),15(a,1)),flip(a)]. given #1018 (F,wt=10): 11488 (c1 v (x ^ (y v c2))) ^ (c2 v y) ' = 0. [para(15(a,1),11423(a,1,1,2))]. given #1019 (T,wt=10): 11497 (x v c2) ' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(11424(a,1),15(a,1)),flip(a)]. given #1020 (T,wt=10): 11498 (c1 v (x ^ (c2 v y))) ^ (y v c2) ' = 0. [para(15(a,1),11424(a,1,1,2))]. given #1021 (A,wt=14): 377 (x v c2) ^ (y v c1 ') != 0 | (x v c2) ' = y v c1 '. [para(209(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1022 (F,wt=10): 11506 (c2 v x) ' ^ (c1 v (y ^ (c2 v x))) = 0. [para(15(a,1),11425(a,1,2,2))]. given #1023 (F,wt=10): 11518 (x v c2) ' ^ (c1 v (y ^ (x v c2))) = 0. [para(15(a,1),11435(a,1,2,2))]. given #1024 (T,wt=10): 11558 (c2 v x) ' ^ (c2 v (y ^ (c2 v x))) = 0. [para(65(a,1),11535(a,1,1,1))]. given #1025 (T,wt=10): 11560 (c2 v x) ' ^ (c2 v (y ^ (x v c1))) = 0. [para(428(a,1),11535(a,1,1,1))]. given #1026 (A,wt=22): 379 (x v y) ^ (z v (y v z) ') != 0 | (x v y) ' = z v (y v z) '. [para(38(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1027 (F,wt=10): 11561 (x v c2) ' ^ (c2 v (y ^ (x v c2))) = 0. [para(100(a,1),11535(a,1,1,1))]. given #1028 (F,wt=10): 11583 (c2 v ((c1 v x) ^ y)) ^ (x v c2) ' = 0. [para(13(a,1),11445(a,1,2,1))]. given #1029 (T,wt=10): 11584 (c2 v x) ' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(11445(a,1),15(a,1)),flip(a)]. given #1030 (T,wt=10): 11585 (c2 v (x ^ (c1 v y))) ^ (c2 v y) ' = 0. [para(15(a,1),11445(a,1,1,2))]. given #1031 (A,wt=18): 380 (x v (c2 ^ y)) ^ (c1 ^ y) ' != 0 | (x v (c2 ^ y)) ' = (c1 ^ y) '. [para(236(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1032 (F,wt=10): 11594 (x v c2) ' ^ (c2 v ((x v c1) ^ y)) = 0. [para(11446(a,1),15(a,1)),flip(a)]. given #1033 (F,wt=10): 11595 (c2 v (x ^ (y v c1))) ^ (y v c2) ' = 0. [para(15(a,1),11446(a,1,1,2))]. given #1034 (T,wt=10): 11603 (c2 v x) ' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(65(a,1),11447(a,1,1,1)),demod(13(8),131(8))]. given #1035 (T,wt=10): 11697 (c2 v x) ' ^ (c1 v (y ^ (x v c2))) = 0. [para(15(a,1),11487(a,1,2,2))]. given #1036 (A,wt=14): 381 (x v c2) ^ (c1 ^ y) ' != 0 | (x v c2) ' = (c1 ^ y) '. [para(279(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1037 (F,wt=10): 11699 (c2 v x) ' ^ (c2 v ((x v c2) ^ y)) = 0. [para(214(a,1),11487(a,1,2,2)),demod(131(10))]. given #1038 (F,wt=10): 11707 (x v c2) ' ^ (c1 v (y ^ (c2 v x))) = 0. [para(15(a,1),11497(a,1,2,2))]. given #1039 (T,wt=10): 11725 (x v c2) ' ^ (c2 v (y ^ (c2 v x))) = 0. [para(13(a,1),11558(a,1,1,1))]. given #1040 (T,wt=10): 11726 (c2 v x) ' ^ (c2 v (y ^ (x v c2))) = 0. [para(13(a,1),11558(a,1,2,2,2))]. given #1041 (A,wt=14): 382 (x v c2) ^ (y ^ c1) ' != 0 | (x v c2) ' = (y ^ c1) '. [para(281(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1042 (F,wt=10): 11733 (x v c2) ' ^ (c2 v (y ^ (x v c1))) = 0. [para(13(a,1),11560(a,1,1,1))]. given #1043 (F,wt=10): 11734 (c2 v x) ' ^ (c2 v (y ^ (c1 v x))) = 0. [para(13(a,1),11560(a,1,2,2,2))]. given #1044 (T,wt=10): 11775 (x v c2) ' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(11583(a,1),15(a,1)),flip(a)]. given #1045 (T,wt=10): 11776 (c2 v (x ^ (c1 v y))) ^ (y v c2) ' = 0. [para(15(a,1),11583(a,1,1,2))]. given #1046 (A,wt=16): 383 (x v (c2 ^ (c1 v y))) ^ c1 ' != 0 | (x v (c2 ^ (c1 v y))) ' = c1 '. [para(270(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1047 (F,wt=10): 11800 (x v c2) ' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(13(a,1),11603(a,1,1,1))]. given #1048 (F,wt=10): 11821 (c2 v (x ^ (c2 v y))) ^ (y v c2) ' = 0. [para(11725(a,1),15(a,1)),flip(a)]. given #1049 (T,wt=10): 11831 (c2 v (x ^ (y v c2))) ^ (c2 v y) ' = 0. [para(11726(a,1),15(a,1)),flip(a)]. given #1050 (T,wt=10): 11839 (x v c2) ' ^ (c2 v (y ^ (c1 v x))) = 0. [para(13(a,1),11733(a,1,2,2,2))]. given #1051 (A,wt=16): 384 (x v (c2 ^ (y v c1))) ^ c1 ' != 0 | (x v (c2 ^ (y v c1))) ' = c1 '. [para(276(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1052 (F,wt=11): 721 c2 v x != 1 | c2 ^ (x v c1) != 0 | c2 ' = x v c1. [para(428(a,1),21(a,1))]. given #1053 (F,wt=11): 723 c2 v x != 1 | c2 ^ (x v c1) != 0 | (x v c1) ' = c2. [para(428(a,1),43(a,1)),demod(15(8))]. given #1054 (T,wt=11): 752 c2 v x != 1 | c2 ^ (c1 v x) != 0 | c2 ' = c1 v x. [para(131(a,1),71(a,1))]. given #1055 (T,wt=11): 830 (x ^ (y v z)) v (x ^ y) ' = 1. [para(76(a,1),190(a,1,2,1))]. given #1056 (A,wt=18): 385 c2 ^ ((x v c1 ') ^ (c1 v y)) != 0 | (x v c1 ') ' = c2 ^ (c1 v y). [para(291(a,1),44(a,1,2)),demod(72(2),26(11)),xx(a)]. given #1057 (F,wt=10): 11863 (c2 ^ ((x ^ c1) v y)) v (x ^ c1) ' = 1. [para(54(a,1),830(a,1,2,1))]. given #1058 (F,wt=10): 11886 (x ^ c1) ' v (c2 ^ ((x ^ c1) v y)) = 1. [para(11863(a,1),13(a,1)),flip(a)]. given #1059 (T,wt=10): 11887 (c2 ^ (x v (y ^ c1))) v (y ^ c1) ' = 1. [para(13(a,1),11863(a,1,1,2))]. given #1060 (T,wt=10): 11889 (c2 ^ ((c1 ^ x) v y)) v (x ^ c1) ' = 1. [para(15(a,1),11863(a,1,1,2,1))]. given #1061 (A,wt=18): 386 c2 ^ ((x v c1 ') ^ (y v c1)) != 0 | (x v c1 ') ' = c2 ^ (y v c1). [para(304(a,1),44(a,1,2)),demod(72(2),26(11)),xx(a)]. given #1062 (F,wt=10): 11890 (c2 ^ ((x ^ c1) v y)) v (c1 ^ x) ' = 1. [para(15(a,1),11863(a,1,2,1))]. given #1063 (F,wt=10): 11896 (x ^ c1) ' v (c2 ^ (y v (x ^ c1))) = 1. [para(13(a,1),11886(a,1,2,2))]. given #1064 (T,wt=10): 11897 (c1 ^ x) ' v (c2 ^ ((x ^ c1) v y)) = 1. [para(15(a,1),11886(a,1,1,1))]. given #1065 (T,wt=10): 11898 (x ^ c1) ' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(15(a,1),11886(a,1,2,2,1))]. given #1066 (A,wt=18): 387 (x v (y ^ c2)) ^ (c1 ^ y) ' != 0 | (x v (y ^ c2)) ' = (c1 ^ y) '. [para(268(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1067 (F,wt=10): 11904 (c2 ^ (x v (c1 ^ y))) v (y ^ c1) ' = 1. [para(15(a,1),11887(a,1,1,2,2))]. given #1068 (F,wt=10): 11905 (c2 ^ (x v (y ^ c1))) v (c1 ^ y) ' = 1. [para(15(a,1),11887(a,1,2,1))]. given #1069 (T,wt=10): 11913 (c2 ^ ((c1 ^ x) v y)) v (c1 ^ x) ' = 1. [para(15(a,1),11889(a,1,2,1))]. given #1070 (T,wt=10): 11928 (c1 ^ x) ' v (c2 ^ (y v (x ^ c1))) = 1. [para(15(a,1),11896(a,1,1,1))]. given #1071 (A,wt=18): 388 (x v (c2 ^ y)) ^ (y ^ c1) ' != 0 | (x v (c2 ^ y)) ' = (y ^ c1) '. [para(269(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1072 (F,wt=10): 11929 (x ^ c1) ' v (c2 ^ (y v (c1 ^ x))) = 1. [para(15(a,1),11896(a,1,2,2,2))]. given #1073 (F,wt=10): 11931 (c1 ^ x) ' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(15(a,1),11897(a,1,2,2,1))]. given #1074 (T,wt=10): 11940 (c2 ^ (x v (c1 ^ y))) v (c1 ^ y) ' = 1. [para(15(a,1),11904(a,1,2,1))]. given #1075 (T,wt=10): 11958 (c1 ^ x) ' v (c2 ^ (y v (c1 ^ x))) = 1. [para(15(a,1),11928(a,1,2,2,2))]. given #1076 (A,wt=18): 389 (x v (y ^ c2)) ^ (y ^ c1) ' != 0 | (x v (y ^ c2)) ' = (y ^ c1) '. [para(318(a,1),44(a,1,2)),demod(72(2)),xx(a)]. given #1077 (F,wt=11): 831 (x ^ y) v (y ^ x) = x ^ y. [para(76(a,1),34(a,1,2))]. given #1078 (F,wt=11): 842 (x v c1) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(604(a,1),28(a,1,2,2))]. given #1079 (T,wt=11): 863 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(14(a,1),846(a,1,2))]. given #1080 (T,wt=11): 867 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(25(a,1),846(a,1,2,2,2))]. given #1081 (A,wt=16): 390 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(16(a,1),54(a,1,2)),demod(15(8))]. given #1082 (F,wt=10): 11972 c1 ^ (x v (c2 ^ (y v (c2 ^ (c1 v z))))) = c1. [para(604(a,1),867(a,1,2,2,2,2))]. given #1083 (F,wt=10): 11973 c1 ^ (x v (c2 ^ (y v (c2 ^ (z v c1))))) = c1. [para(609(a,1),867(a,1,2,2,2,2))]. given #1084 (T,wt=10): 11974 c1 ^ (x v (c2 ^ (y v (c2 ^ c1 ') '))) = c1. [para(6480(a,1),867(a,1,2,2,2,2))]. given #1085 (T,wt=10): 11977 c1 ^ (x v (c2 ^ ((c2 ^ (c1 v y)) v z))) = c1. [para(13(a,1),11972(a,1,2,2,2))]. given #1086 (A,wt=12): 392 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(54(a,1),34(a,1,2,2))]. given #1087 (F,wt=10): 11978 c1 ^ ((c2 ^ (x v (c2 ^ (c1 v y)))) v z) = c1. [para(13(a,1),11972(a,1,2))]. given #1088 (F,wt=10): 11995 c1 ^ (x v (c2 ^ ((c2 ^ (y v c1)) v z))) = c1. [para(13(a,1),11973(a,1,2,2,2))]. given #1089 (T,wt=10): 11996 c1 ^ ((c2 ^ (x v (c2 ^ (y v c1)))) v z) = c1. [para(13(a,1),11973(a,1,2))]. given #1090 (T,wt=10): 12013 c1 ^ (x v (c2 ^ ((c2 ^ c1 ') ' v y))) = c1. [para(13(a,1),11974(a,1,2,2,2))]. given #1091 (A,wt=16): 394 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(16(a,1),80(a,1,2)),demod(15(8))]. given #1092 (F,wt=10): 12014 c1 ^ ((c2 ^ (x v (c2 ^ c1 ') ')) v y) = c1. [para(13(a,1),11974(a,1,2))]. given #1093 (F,wt=10): 12026 c1 ^ ((c2 ^ ((c2 ^ (c1 v x)) v y)) v z) = c1. [para(13(a,1),11977(a,1,2))]. given #1094 (T,wt=10): 12060 c1 ^ ((c2 ^ ((c2 ^ (x v c1)) v y)) v z) = c1. [para(13(a,1),11995(a,1,2))]. given #1095 (T,wt=10): 12093 c1 ^ ((c2 ^ ((c2 ^ c1 ') ' v x)) v y) = c1. [para(13(a,1),12013(a,1,2))]. given #1096 (A,wt=20): 396 c1 ^ ((x ^ c2) v (c1 ^ ((x ^ c1) v (y ^ (c1 v (x ^ c2)))))) = c1 ^ ((x ^ c2) v (c1 ^ y)). [para(80(a,1),22(a,1,2,2,2,1))]. given #1097 (F,wt=11): 885 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(14(a,1),861(a,1,2,2,2))]. given #1098 (F,wt=11): 886 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(14(a,1),861(a,1,2))]. given #1099 (T,wt=11): 901 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(25(a,1),862(a,1,2,1,2))]. given #1100 (T,wt=11): 902 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(25(a,1),862(a,1,2))]. given #1101 (A,wt=20): 397 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2 ^ (c1 v x)))))) = c1 ^ (x v (y ^ c1)). [para(80(a,1),22(a,2,2,2)),demod(16(9))]. given #1102 (F,wt=11): 908 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(14(a,1),884(a,1,2,1,2))]. given #1103 (F,wt=11): 911 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(25(a,1),884(a,1,2))]. given #1104 (T,wt=11): 924 (x v c1) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(609(a,1),28(a,1,2,2))]. given #1105 (T,wt=11): 1033 (x ^ c2) v (x ^ (c1 v (c2 ^ y))) = x ^ c2. [para(782(a,1),34(a,1,2,2))]. given #1106 (A,wt=20): 400 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x ' = y ^ z. [para(16(a,1),45(b,1))]. low water: id=6943, wt=23 given #1107 (F,wt=11): 1066 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(16(a,1),1038(a,1,2))]. given #1108 (F,wt=11): 1068 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(26(a,1),1038(a,1,2,2,2))]. given #1109 (T,wt=10): 12179 c2 v (x ^ (c1 v (y ^ (c1 v (c2 ^ z))))) = c2. [para(782(a,1),1068(a,1,2,2,2,2))]. given #1110 (T,wt=10): 12180 c2 v (x ^ (c1 v (y ^ (c1 v (z ^ c2))))) = c2. [para(788(a,1),1068(a,1,2,2,2,2))]. low water: id=7254, wt=22 given #1111 (A,wt=12): 401 x v y != 1 | 0 != x | (x v y) ' = x. [para(17(a,1),45(b,1)),demod(13(2),65(2)),flip(b)]. given #1112 (F,wt=10): 12181 c2 v (x ^ (c1 v ((c1 v (c2 ^ y)) ^ z))) = c2. [para(15(a,1),12179(a,1,2,2,2))]. given #1113 (F,wt=10): 12182 c2 v ((c1 v (x ^ (c1 v (c2 ^ y)))) ^ z) = c2. [para(15(a,1),12179(a,1,2))]. given #1114 (T,wt=10): 12198 c2 v (x ^ (c1 v ((c1 v (y ^ c2)) ^ z))) = c2. [para(15(a,1),12180(a,1,2,2,2))]. given #1115 (T,wt=10): 12199 c2 v ((c1 v (x ^ (c1 v (y ^ c2)))) ^ z) = c2. [para(15(a,1),12180(a,1,2))]. given #1116 (A,wt=20): 402 x v (y v z) != 1 | (x v z) ^ y != 0 | y ' = x v z. [para(25(a,1),45(a,1))]. given #1117 (F,wt=10): 12215 c2 v ((c1 v ((c1 v (c2 ^ x)) ^ y)) ^ z) = c2. [para(15(a,1),12181(a,1,2))]. low water: id=7784, wt=21 given #1118 (F,wt=10): 12246 c2 v ((c1 v ((c1 v (x ^ c2)) ^ y)) ^ z) = c2. [para(15(a,1),12198(a,1,2))]. given #1119 (T,wt=11): 1077 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(16(a,1),1064(a,1,2,2,2))]. given #1120 (T,wt=11): 1078 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(16(a,1),1064(a,1,2))]. given #1121 (A,wt=20): 403 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z. [para(26(a,1),45(b,1))]. given #1122 (F,wt=11): 1092 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(26(a,1),1065(a,1,2,1,2))]. given #1123 (F,wt=11): 1093 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(26(a,1),1065(a,1,2))]. given #1124 (T,wt=11): 1100 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(16(a,1),1076(a,1,2,1,2))]. given #1125 (T,wt=11): 1103 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(26(a,1),1076(a,1,2))]. given #1126 (A,wt=24): 404 x v (y v z) != 1 | x v y != 0 | (x v (y v z)) ' = x v y. [para(28(a,1),45(b,1)),demod(13(4),25(4),25(3),14(2),128(4))]. given #1127 (F,wt=11): 1121 (x ^ c2) v (x ^ (c1 v (y ^ c2))) = x ^ c2. [para(788(a,1),34(a,1,2,2))]. given #1128 (F,wt=11): 1171 ((x v y) ^ z) v (y ^ z) ' = 1. [para(94(a,1),190(a,1,2,1))]. low water: id=8230, wt=20 given #1129 (T,wt=11): 1238 (x ^ (y v z)) v (x ^ z) ' = 1. [para(98(a,1),190(a,1,2,1))]. given #1130 (T,wt=11): 1313 (c1 v x) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(604(a,1),109(a,1,2,2))]. given #1131 (A,wt=20): 405 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z) ' = x. [para(29(a,1),45(b,1)),demod(13(3))]. given #1132 (F,wt=11): 1315 (c1 v x) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(609(a,1),109(a,1,2,2))]. given #1133 (F,wt=11): 1360 (x ^ y) ' v (z v x) = 1. [para(179(a,1),110(a,1,1)),demod(57(6),179(7))]. given #1134 (T,wt=11): 1362 (x ^ y) ' v (z v y) = 1. [para(190(a,1),110(a,1,1)),demod(57(6),190(7))]. given #1135 (T,wt=11): 1364 c1 ' v (x v (y v c2)) = 1. [para(206(a,1),110(a,1,1)),demod(14(7),57(8),206(11))]. given #1136 (A,wt=12): 406 x v (x v y) ' != 1 | x v y = x. [para(136(a,1),45(b,1)),demod(13(3),326(11)),xx(b)]. given #1137 (F,wt=7): 12468 c1 ' v (c1 ' v c2 ') ' != 1. [ur(406,b,24,a)]. given #1138 (F,wt=8): 12472 (c1 ' v (c1 ' v c2 ') ') ' != 0. [ur(2458,b,12468,a),demod(13(9))]. given #1139 (T,wt=11): 1367 (c1 ^ x) ' v (y v (c2 ^ x)) = 1. [para(236(a,1),110(a,1,1)),demod(57(9),236(13))]. given #1140 (T,wt=11): 1370 (c1 ^ x) ' v (y v (x ^ c2)) = 1. [para(268(a,1),110(a,1,1)),demod(57(9),268(13))]. given #1141 (A,wt=24): 407 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z)) ' = x. [para(30(a,1),45(b,1)),demod(13(4))]. given #1142 (F,wt=9): 12473 c2 ^ c1 ' != 0 | (c1 v (c2 ^ c1 ')) ' = c1 '. [para(304(a,1),407(a,1)),demod(15(7),15(14),13(16),782(17)),xx(a)]. given #1143 (F,wt=11): 1371 (x ^ c1) ' v (y v (c2 ^ x)) = 1. [para(269(a,1),110(a,1,1)),demod(57(9),269(13))]. given #1144 (T,wt=11): 1372 (x ^ c1) ' v (y v (x ^ c2)) = 1. [para(318(a,1),110(a,1,1)),demod(57(9),318(13))]. given #1145 (T,wt=11): 1390 c1 ' v (x v (c2 v y)) = 1. [para(1363(a,1),14(a,1,1)),demod(64(2),14(6)),flip(a)]. given #1146 (A,wt=12): 409 x v (y v x) ' != 1 | y v x = x. [para(151(a,1),45(b,1)),demod(13(3),326(11)),xx(b)]. given #1147 (F,wt=11): 1421 (c1 v x) ^ (c2 v (x v y)) ' = 0. [para(441(a,1),111(a,1,2)),demod(15(4),81(4),13(6)),flip(a)]. given #1148 (F,wt=11): 1545 x v (c2 v (c1 v (x ^ y)) ') = 1. [para(566(a,1),31(a,1,2)),demod(72(2),13(5)),flip(a)]. given #1149 (T,wt=11): 1558 x ^ (c1 ^ (c2 ^ (x v y)) ') = 0. [para(675(a,1),29(a,1,2)),demod(83(2)),flip(a)]. given #1150 (T,wt=11): 1567 x ^ (c1 ^ (c2 ^ (y v x)) ') = 0. [para(675(a,1),94(a,1,2)),demod(83(2)),flip(a)]. given #1151 (A,wt=24): 413 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = x ^ (y ^ z). [para(34(a,1),45(a,1)),demod(15(7),26(7),26(6),16(5),241(7))]. given #1152 (F,wt=11): 1605 ((x ^ y) v z) ^ (y v z) ' = 0. [para(119(a,1),151(a,1,2,1))]. low water: id=9170, wt=19 given #1153 (F,wt=11): 1625 x v (c2 v (c1 v (y ^ x)) ') = 1. [para(566(a,1),119(a,1,2)),demod(72(2),13(5)),flip(a)]. given #1154 (T,wt=11): 1862 (x v (y ^ z)) ^ (x v z) ' = 0. [para(125(a,1),151(a,1,2,1))]. given #1155 (T,wt=11): 2131 c1 ^ (x ^ (c2 ^ (x v y)) ') = 0. [para(303(a,1),139(a,1,2)),demod(83(2)),flip(a)]. given #1156 (A,wt=14): 418 c2 ^ (c1 ' ^ (c1 v x)) != 0 | (c2 ^ (c1 v x)) ' = c1 '. [para(270(a,1),45(a,1)),demod(26(10)),xx(a)]. given #1157 (F,wt=11): 2253 c2 v (x v ((c1 ^ y) v x) ') = 1. [para(38(a,1),141(a,1,2)),demod(13(3),64(3)),flip(a)]. given #1158 (F,wt=11): 2366 x v (c2 v (x v (c1 ^ y)) ') = 1. [para(144(a,1),801(a,1,2)),demod(13(7),14(7))]. given #1159 (T,wt=11): 2389 c2 v (x v ((y ^ c1) v x) ') = 1. [para(38(a,1),146(a,1,2)),demod(13(3),64(3)),flip(a)]. given #1160 (T,wt=11): 2472 x v (c2 v (x v (y ^ c1)) ') = 1. [para(150(a,1),801(a,1,2)),demod(13(7),14(7))]. given #1161 (A,wt=18): 419 x v (y ^ (x ^ y) ') != 1 | (y ^ (x ^ y) ') ' = x. [para(41(a,1),45(b,1)),demod(13(4)),xx(b)]. given #1162 (F,wt=11): 2497 ((c1 ^ x) v (y ^ (c1 v (c2 ^ z)))) ^ c2 ' = 0. [para(1038(a,1),2251(a,1,2,1))]. given #1163 (F,wt=11): 2498 ((c1 ^ x) v (y ^ (c1 v (z ^ c2)))) ^ c2 ' = 0. [para(1064(a,1),2251(a,1,2,1))]. given #1164 (T,wt=11): 2499 ((c1 ^ x) v ((c1 v (c2 ^ y)) ^ z)) ^ c2 ' = 0. [para(1065(a,1),2251(a,1,2,1))]. given #1165 (T,wt=11): 2500 ((c1 ^ x) v ((c1 v (y ^ c2)) ^ z)) ^ c2 ' = 0. [para(1076(a,1),2251(a,1,2,1))]. given #1166 (A,wt=14): 420 c2 ^ (c1 ' ^ (x v c1)) != 0 | (c2 ^ (x v c1)) ' = c1 '. [para(276(a,1),45(a,1)),demod(26(10)),xx(a)]. given #1167 (F,wt=11): 2542 (x v c1) ^ (x v (c2 v y)) ' = 0. [para(131(a,1),152(a,1,2,1,2))]. given #1168 (F,wt=11): 2543 (x v c1) ^ (x v (y v c2)) ' = 0. [para(133(a,1),152(a,1,2,1,2))]. given #1169 (T,wt=11): 2544 (x v (c1 ^ y)) ^ (x v (c2 ^ y)) ' = 0. [para(231(a,1),152(a,1,2,1,2))]. given #1170 (T,wt=10): 12670 ((x ^ c1) ' v (c2 ^ (y v x))) ' = 0. [hyper(375,a,11147,a,b,2544,a),demod(11147(7),63(2),11147(8),57(11)),flip(a)]. given #1171 (A,wt=12): 421 c2 ^ ((c1 v x) ^ c1 ') != 0 | c2 ^ (c1 v x) = c1. [para(291(a,1),45(a,1)),demod(16(10),326(15)),flip(c),xx(a)]. given #1172 (F,wt=9): 12690 (c2 ^ (x v y)) v (y ^ c1) ' = 1. [hyper(2458,a,12670,a)]. given #1173 (F,wt=9): 12691 (x ^ c1) ' v (c2 ^ (y v x)) = 1. [hyper(2030,a,12670,a)]. given #1174 (T,wt=9): 12704 (c2 ^ (x v y)) v (x ^ c1) ' = 1. [para(13(a,1),12690(a,1,1,2))]. given #1175 (T,wt=9): 12707 (c2 ^ (x v y)) v (c1 ^ y) ' = 1. [para(15(a,1),12690(a,1,2,1))]. given #1176 (A,wt=12): 422 c2 ^ ((x v c1) ^ c1 ') != 0 | c2 ^ (x v c1) = c1. [para(304(a,1),45(a,1)),demod(16(10),326(15)),flip(c),xx(a)]. given #1177 (F,wt=9): 12715 (x ^ c1) ' v (c2 ^ (x v y)) = 1. [para(13(a,1),12691(a,1,2,2))]. given #1178 (F,wt=9): 12717 (c1 ^ x) ' v (c2 ^ (y v x)) = 1. [para(15(a,1),12691(a,1,1,1))]. low water: id=9491, wt=18 given #1179 (T,wt=9): 12721 (c2 ^ (x v y)) v (c1 ^ x) ' = 1. [para(15(a,1),12704(a,1,2,1))]. given #1180 (T,wt=9): 12750 (c1 ^ x) ' v (c2 ^ (x v y)) = 1. [para(15(a,1),12715(a,1,1,1))]. given #1181 (A,wt=16): 425 c1 v (x v (c2 v y)) = x v (c2 v y). [para(131(a,1),25(a,1,2)),flip(a)]. given #1182 (F,wt=10): 12734 (c2 ^ (x v (c2 ^ y))) v (c1 ^ y) ' = 1. [para(53(a,1),12707(a,1,2,1))]. given #1183 (F,wt=10): 12735 (c2 ^ (x v (y ^ c2))) v (y ^ c1) ' = 1. [para(80(a,1),12707(a,1,2,1))]. given #1184 (T,wt=10): 12755 (c1 ^ x) ' v (c2 ^ (y v (c2 ^ x))) = 1. [para(53(a,1),12717(a,1,1,1))]. given #1185 (T,wt=10): 12756 (x ^ c1) ' v (c2 ^ (y v (x ^ c2))) = 1. [para(80(a,1),12717(a,1,1,1))]. given #1186 (A,wt=12): 426 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(131(a,1),28(a,1,2,2))]. given #1187 (F,wt=10): 12774 (c2 ^ ((c2 ^ x) v y)) v (c1 ^ x) ' = 1. [para(53(a,1),12721(a,1,2,1))]. given #1188 (F,wt=10): 12775 (c2 ^ ((x ^ c2) v y)) v (x ^ c1) ' = 1. [para(80(a,1),12721(a,1,2,1))]. given #1189 (T,wt=10): 12792 (c1 ^ x) ' v (c2 ^ ((c2 ^ x) v y)) = 1. [para(53(a,1),12750(a,1,1,1))]. given #1190 (T,wt=10): 12793 (x ^ c1) ' v (c2 ^ ((x ^ c2) v y)) = 1. [para(80(a,1),12750(a,1,1,1))]. given #1191 (A,wt=19): 427 x v (c2 v y) != 1 | (x v c1) ^ (c2 v y) != 0 | (x v c1) ' = c2 v y. [para(131(a,1),44(a,1,2))]. given #1192 (F,wt=10): 12807 (c2 ^ (x v (y ^ c2))) v (c1 ^ y) ' = 1. [para(15(a,1),12734(a,1,1,2,2))]. given #1193 (F,wt=10): 12808 (c2 ^ (x v (c2 ^ y))) v (y ^ c1) ' = 1. [para(15(a,1),12734(a,1,2,1))]. given #1194 (T,wt=10): 12835 (x ^ c1) ' v (c2 ^ (y v (c2 ^ x))) = 1. [para(15(a,1),12755(a,1,1,1))]. given #1195 (T,wt=10): 12836 (c1 ^ x) ' v (c2 ^ (y v (x ^ c2))) = 1. [para(15(a,1),12755(a,1,2,2,2))]. given #1196 (A,wt=16): 429 c2 v (x v (y v c1)) = c2 v (x v y). [para(14(a,1),132(a,1,2)),demod(13(8))]. given #1197 (F,wt=10): 12843 (c2 ^ ((x ^ c2) v y)) v (c1 ^ x) ' = 1. [para(15(a,1),12774(a,1,1,2,1))]. given #1198 (F,wt=10): 12844 (c2 ^ ((c2 ^ x) v y)) v (x ^ c1) ' = 1. [para(15(a,1),12774(a,1,2,1))]. given #1199 (T,wt=10): 12847 (x ^ c1) ' v (c2 ^ ((c2 ^ x) v y)) = 1. [para(15(a,1),12792(a,1,1,1))]. given #1200 (T,wt=10): 12848 (c1 ^ x) ' v (c2 ^ ((x ^ c2) v y)) = 1. [para(15(a,1),12792(a,1,2,2,1))]. given #1201 (A,wt=19): 437 x v (y v c2) != 1 | (x v c2) ^ (y v c1) != 0 | (x v c2) ' = y v c1. [para(132(a,1),44(a,1,2))]. given #1202 (F,wt=11): 2545 (x v (y ^ c1)) ^ (x v (y ^ c2)) ' = 0. [para(398(a,1),152(a,1,2,1,2))]. given #1203 (F,wt=11): 2547 (x v (y ^ c1)) ^ (x v (c2 ^ y)) ' = 0. [para(602(a,1),152(a,1,2,1,2))]. given #1204 (T,wt=11): 2658 c1 ^ (x ^ ((c2 ^ x) v y) ') = 0. [para(154(a,1),53(a,1,2)),demod(15(3),81(3)),flip(a)]. given #1205 (T,wt=11): 2696 c2 ' ^ (x ^ (c1 ^ y)) = 0. [para(2689(a,1),16(a,1,1)),demod(81(2),16(6)),flip(a)]. given #1206 (A,wt=17): 439 x v (c2 v y) != 1 | c2 ^ (x v y) != 0 | (x v y) ' = c2. [para(132(a,2),44(a,1,2)),demod(428(4),15(8))]. given #1207 (F,wt=11): 2697 c2 ' ^ (x ^ (y ^ c1)) = 0. [para(16(a,1),2689(a,1,2))]. given #1208 (F,wt=11): 2738 c1 ^ (x ^ (y v (c2 ^ x)) ') = 0. [para(231(a,1),156(a,1,2,1,2)),demod(16(7))]. given #1209 (T,wt=11): 2739 x ^ (c1 ^ (y v (x ^ c2)) ') = 0. [para(398(a,1),156(a,1,2,1,2)),demod(16(7))]. given #1210 (T,wt=11): 2740 x ^ (c1 ^ (y v (c2 ^ x)) ') = 0. [para(602(a,1),156(a,1,2,1,2)),demod(16(7))]. given #1211 (A,wt=15): 443 (x v (y v c1)) ^ (c2 v (x v y)) ' = 0. [para(14(a,1),433(a,1,1)),demod(13(6))]. given #1212 (F,wt=11): 2878 ((x ^ c1) v (y ^ (c1 v (c2 ^ z)))) ^ c2 ' = 0. [para(1038(a,1),2387(a,1,2,1))]. given #1213 (F,wt=11): 2879 ((x ^ c1) v (y ^ (c1 v (z ^ c2)))) ^ c2 ' = 0. [para(1064(a,1),2387(a,1,2,1))]. given #1214 (T,wt=11): 2880 ((x ^ c1) v ((c1 v (c2 ^ y)) ^ z)) ^ c2 ' = 0. [para(1065(a,1),2387(a,1,2,1))]. given #1215 (T,wt=11): 2881 ((x ^ c1) v ((c1 v (y ^ c2)) ^ z)) ^ c2 ' = 0. [para(1076(a,1),2387(a,1,2,1))]. given #1216 (A,wt=1