============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13659 was started by mccune on cleo.thornwood, Mon Jun 19 16:45:47 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H65d.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 H65d.in clauses(sos). x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). end_of_list. clauses(goals). x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v y = y v x. [input]. 2 (x v y) v z = x v (y v z). [input]. 3 x ^ y = y ^ x. [input]. 4 (x ^ y) ^ z = x ^ (y ^ z). [input]. 5 x ^ (x v y) = x. [input]. 6 x v (x ^ y) = x. [input]. 7 x v x ' = 1. [input]. 8 x ^ x ' = 0. [input]. 9 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 10 x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). [input]. 11 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [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, c3, ^, v, ' ]). After inverse_order: Function symbol precedence: lex([ 0, 1, c1, c2, c3, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(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). 12 x v y = y v x. [input]. 13 (x v y) v z = x v (y v z). [input]. 14 x ^ y = y ^ x. [input]. 15 (x ^ y) ^ z = x ^ (y ^ z). [input]. 16 x ^ (x v y) = x. [input]. 17 x v (x ^ y) = x. [input]. 18 x v x ' = 1. [input]. 19 x ^ x ' = 0. [input]. 20 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 21 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)) # label(H65). [copy(10),flip(a)]. 22 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [clausify]. end_of_list. clauses(demodulators). 12 x v y = y v x. [input]. % (lex-dep) 13 (x v y) v z = x v (y v z). [input]. 14 x ^ y = y ^ x. [input]. % (lex-dep) 15 (x ^ y) ^ z = x ^ (y ^ z). [input]. 16 x ^ (x v y) = x. [input]. 17 x v (x ^ y) = x. [input]. 18 x v x ' = 1. [input]. 19 x ^ x ' = 0. [input]. 21 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)) # label(H65). [copy(10),flip(a)]. 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): 12 x v y = y v x. [input]. given #2 (I,wt=11): 13 (x v y) v z = x v (y v z). [input]. given #3 (I,wt=7): 14 x ^ y = y ^ x. [input]. given #4 (I,wt=11): 15 (x ^ y) ^ z = x ^ (y ^ z). [input]. given #5 (I,wt=7): 16 x ^ (x v y) = x. [input]. given #6 (I,wt=7): 17 x v (x ^ y) = x. [input]. given #7 (I,wt=6): 18 x v x ' = 1. [input]. given #8 (I,wt=6): 19 x ^ x ' = 0. [input]. given #9 (I,wt=14): 20 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=21): 21 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)) # label(H65). [copy(10),flip(a)]. given #11 (I,wt=13): 22 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [clausify]. given #12 (F,wt=5): 33 x ^ x = x. [para(17(a,1),16(a,1,2))]. given #13 (F,wt=5): 34 x v x = x. [para(16(a,1),17(a,1,2))]. given #14 (T,wt=5): 37 x ^ 1 = x. [para(18(a,1),16(a,1,2))]. given #15 (T,wt=5): 40 x v 0 = x. [para(19(a,1),17(a,1,2))]. given #16 (A,wt=11): 23 x v (y v z) = y v (x v z). [para(12(a,1),13(a,1,1)),demod(13(2))]. given #17 (F,wt=5): 69 1 ^ x = x. [para(37(a,1),14(a,1)),flip(a)]. given #18 (F,wt=4): 79 1 ' = 0. [hyper(20,a,40,a,b,69,a)]. given #19 (T,wt=5): 71 0 v x = x. [para(40(a,1),12(a,1)),flip(a)]. given #20 (T,wt=4): 82 0 ' = 1. [hyper(20,a,71,a,b,37,a)]. given #21 (A,wt=11): 24 x ^ (y ^ z) = y ^ (x ^ z). [para(14(a,1),15(a,1,1)),demod(15(2))]. given #22 (F,wt=5): 80 1 v x = 1. [para(69(a,1),16(a,1))]. given #23 (F,wt=5): 83 0 ^ x = 0. [para(71(a,1),16(a,1,2))]. given #24 (T,wt=5): 89 x v 1 = 1. [para(80(a,1),12(a,1)),flip(a)]. given #25 (T,wt=5): 92 x ^ 0 = 0. [para(83(a,1),14(a,1)),flip(a)]. given #26 (A,wt=7): 25 x ^ (y v x) = x. [para(12(a,1),16(a,1,2))]. given #27 (F,wt=7): 31 x v (y ^ x) = x. [para(14(a,1),17(a,1,2))]. given #28 (F,wt=7): 91 0 != x | x ' = 1. [back_demod(70),demod(89(2)),xx(a)]. given #29 (T,wt=7): 94 1 != x | x ' = 0. [back_demod(72),demod(92(4)),xx(b)]. given #30 (T,wt=8): 81 x v (x ' v y) = 1. [back_demod(35),demod(80(5))]. given #31 (A,wt=13): 26 (x v y) ^ (x v (y v z)) = x v y. [para(13(a,1),16(a,1,2))]. given #32 (F,wt=8): 84 x ^ (x ' ^ y) = 0. [back_demod(38),demod(83(5))]. given #33 (F,wt=8): 90 x v (y v x ') = 1. [back_demod(76),demod(89(5))]. given #34 (T,wt=8): 93 x ^ (y ^ x ') = 0. [back_demod(87),demod(92(5))]. given #35 (T,wt=9): 59 x ^ (x ^ y) = x ^ y. [para(33(a,1),15(a,1,1)),flip(a)]. given #36 (A,wt=11): 27 x ^ ((x v y) ^ z) = x ^ z. [para(16(a,1),15(a,1,1)),flip(a)]. given #37 (F,wt=8): 132 x ^ (x v y) ' = 0. [para(19(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #38 (F,wt=8): 139 x ^ (y v x) ' = 0. [para(12(a,1),132(a,1,2,1))]. given #39 (T,wt=9): 61 x ^ (y ^ x) = y ^ x. [para(33(a,1),15(a,2,2)),demod(14(2))]. given #40 (T,wt=9): 65 x v (x v y) = x v y. [para(34(a,1),13(a,1,1)),flip(a)]. given #41 (A,wt=13): 28 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(16(a,1),15(a,1)),flip(a)]. given #42 (F,wt=9): 67 x v (y v x) = y v x. [para(34(a,1),13(a,2,2)),demod(12(2))]. given #43 (F,wt=9): 74 x ^ (y v (x v z)) = x. [para(23(a,1),16(a,1,2))]. given #44 (T,wt=9): 86 x v (y ^ (x ^ z)) = x. [para(24(a,1),17(a,1,2))]. given #45 (T,wt=9): 95 x ^ (y v (z v x)) = x. [para(13(a,1),25(a,1,2))]. given #46 (A,wt=11): 29 x v ((x ^ y) v z) = x v z. [para(17(a,1),13(a,1,1)),flip(a)]. given #47 (F,wt=8): 183 x v (x ^ y) ' = 1. [para(18(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #48 (F,wt=8): 193 x v (y ^ x) ' = 1. [para(14(a,1),183(a,1,2,1))]. given #49 (T,wt=9): 103 x v (y ^ (z ^ x)) = x. [para(15(a,1),31(a,1,2))]. given #50 (T,wt=10): 36 x v (y v (x v y) ') = 1. [para(18(a,1),13(a,1)),flip(a)]. given #51 (A,wt=13): 30 x v (y v ((x v y) ^ z)) = x v y. [para(17(a,1),13(a,1)),flip(a)]. given #52 (F,wt=10): 39 x ^ (y ^ (x ^ y) ') = 0. [para(19(a,1),15(a,1)),flip(a)]. given #53 (F,wt=10): 62 1 != x | 0 != x | x ' = x. [para(33(a,1),20(b,1)),demod(34(1)),flip(a),flip(b)]. given #54 (T,wt=10): 109 x v (y v (x ' v z)) = 1. [para(81(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #55 (T,wt=10): 122 x ^ (y ^ (x ' ^ z)) = 0. [para(84(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #56 (A,wt=13): 32 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(15(a,1),17(a,1,2))]. given #57 (F,wt=10): 124 x v (y v (z v x ')) = 1. [para(13(a,1),90(a,1,2))]. given #58 (F,wt=10): 127 x ^ (y ^ (z ^ x ')) = 0. [para(15(a,1),93(a,1,2))]. given #59 (T,wt=10): 137 x ^ ((x v y) ' ^ z) = 0. [para(84(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #60 (T,wt=10): 138 x ^ (y ^ (x v z) ') = 0. [para(93(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #61 (A,wt=14): 41 x v y != 1 | y ^ x != 0 | y ' = x. [para(12(a,1),20(a,1))]. given #62 (F,wt=5): 272 x ' ' = x. [para(18(a,1),41(a,1)),demod(14(5),19(5)),xx(a),xx(b)]. given #63 (F,wt=8): 290 x ' v (y v x) = 1. [para(272(a,1),90(a,1,2,2))]. given #64 (T,wt=8): 291 x ' ^ (y ^ x) = 0. [para(272(a,1),93(a,1,2,2))]. given #65 (T,wt=10): 143 x ^ (y v (x v z)) ' = 0. [para(23(a,1),132(a,1,2,1))]. given #66 (A,wt=20): 42 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y) ' = z. [para(13(a,1),20(a,1))]. given #67 (F,wt=10): 144 x ^ (y v (z v x)) ' = 0. [para(13(a,1),139(a,1,2,1))]. given #68 (F,wt=10): 145 x ^ ((y v x) ' ^ z) = 0. [para(139(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #69 (T,wt=10): 149 x ^ (y ^ (z v x) ') = 0. [para(139(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #70 (T,wt=10): 187 x v ((x ^ y) ' v z) = 1. [para(81(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #71 (A,wt=14): 43 x v y != 1 | y ^ x != 0 | x ' = y. [para(14(a,1),20(b,1))]. given #72 (F,wt=10): 188 x v (y v (x ^ z) ') = 1. [para(90(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #73 (F,wt=10): 196 x v (y ^ (x ^ z)) ' = 1. [para(24(a,1),183(a,1,2,1))]. given #74 (T,wt=10): 197 x v ((y ^ x) ' v z) = 1. [para(193(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #75 (T,wt=10): 199 x v (y ^ (z ^ x)) ' = 1. [para(15(a,1),193(a,1,2,1))]. given #76 (A,wt=20): 44 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(15(a,1),20(b,1))]. given #77 (F,wt=10): 201 x v (y v (z ^ x) ') = 1. [para(193(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #78 (F,wt=10): 214 x v (y v (y v x) ') = 1. [para(12(a,1),36(a,1,2,2,1))]. given #79 (T,wt=10): 229 x ^ (y ^ (y ^ x) ') = 0. [para(14(a,1),39(a,1,2,2,1))]. given #80 (T,wt=10): 292 x ' v (y v (x v z)) = 1. [para(272(a,1),109(a,1,2,2,1))]. given #81 (A,wt=21): 47 x ^ (y v (x ^ ((z ^ u) v (x ^ y)))) = x ^ (y v (z ^ u)). [para(12(a,1),21(a,1,2,2,2))]. given #82 (F,wt=10): 293 x ' ^ (y ^ (x ^ z)) = 0. [para(272(a,1),122(a,1,2,2,1))]. given #83 (F,wt=10): 294 x ' v (y v (z v x)) = 1. [para(272(a,1),124(a,1,2,2,2))]. given #84 (T,wt=10): 295 x ' ^ (y ^ (z ^ x)) = 0. [para(272(a,1),127(a,1,2,2,2))]. given #85 (T,wt=10): 586 (x ^ y) ' v (z v x) = 1. [para(17(a,1),294(a,1,2,2))]. given #86 (A,wt=27): 48 x ^ (y v (z v (x ^ ((x ^ (y v z)) v (u ^ v))))) = x ^ (y v (z v (u ^ v))). [para(13(a,1),21(a,1,2)),demod(13(11))]. given #87 (F,wt=10): 589 (x ^ y) ' v (z v y) = 1. [para(31(a,1),294(a,1,2,2))]. given #88 (F,wt=10): 600 (x v y) ' ^ (z ^ x) = 0. [para(16(a,1),295(a,1,2,2))]. given #89 (T,wt=10): 603 (x v y) ' ^ (z ^ y) = 0. [para(25(a,1),295(a,1,2,2))]. given #90 (T,wt=11): 75 x v (y v (x ^ z)) = y v x. [para(17(a,1),23(a,1,2)),flip(a)]. given #91 (A,wt=21): 49 x ^ (y v (x ^ ((y ^ x) v (z ^ u)))) = x ^ (y v (z ^ u)). [para(14(a,1),21(a,1,2,2,2,1))]. given #92 (F,wt=11): 85 x ^ (y ^ (x v z)) = y ^ x. [para(16(a,1),24(a,1,2)),flip(a)]. given #93 (F,wt=11): 96 x ^ ((y v x) ^ z) = x ^ z. [para(25(a,1),15(a,1,1)),flip(a)]. given #94 (T,wt=11): 100 x ^ (y ^ (z v x)) = y ^ x. [para(25(a,1),24(a,1,2)),flip(a)]. given #95 (T,wt=11): 101 x v ((y ^ x) v z) = x v z. [para(31(a,1),13(a,1,1)),flip(a)]. given #96 (A,wt=25): 50 x ^ ((y v (x ^ ((x ^ y) v (z ^ u)))) ^ v) = x ^ ((y v (z ^ u)) ^ v). [para(21(a,1),15(a,1,1)),demod(15(4)),flip(a)]. given #97 (F,wt=11): 105 x v (y v (z ^ x)) = y v x. [para(31(a,1),23(a,1,2)),flip(a)]. given #98 (F,wt=11): 152 (x v y) ^ (z ^ x) = z ^ x. [para(61(a,1),27(a,2)),demod(151(4))]. given #99 (T,wt=11): 164 (x v y) ^ (y v x) = x v y. [para(67(a,1),26(a,1,2))]. given #100 (T,wt=10): 972 (x v y) ^ (y v x) ' = 0. [para(164(a,1),291(a,1,2)),demod(14(4))]. given #101 (A,wt=29): 51 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (y ^ z)) v (u ^ v)))))) = x ^ (y ^ (z v (u ^ v))). [para(21(a,1),15(a,1)),demod(15(4),15(7),15(10)),flip(a)]. given #102 (F,wt=11): 166 x ^ (y v (z v (x v u))) = x. [para(13(a,1),74(a,1,2))]. given #103 (F,wt=11): 172 x v (y ^ (z ^ (x ^ u))) = x. [para(15(a,1),86(a,1,2))]. given #104 (T,wt=11): 175 x ^ (y v (z v (u v x))) = x. [para(13(a,1),95(a,1,2,2))]. given #105 (T,wt=11): 190 (x ^ y) v (z v x) = z v x. [para(67(a,1),29(a,2)),demod(163(4))]. given #106 (A,wt=17): 52 x ^ (y v (x ^ ((x ^ y) v z))) = x ^ (y v z). [para(16(a,1),21(a,1,2,2,2,2)),demod(16(7))]. given #107 (F,wt=11): 207 x v (y ^ (z ^ (u ^ x))) = x. [para(15(a,1),103(a,1,2,2))]. given #108 (F,wt=11): 250 (x ^ y) v (y ^ x) = x ^ y. [para(61(a,1),32(a,1,2))]. given #109 (T,wt=10): 1219 (x ^ y) v (y ^ x) ' = 1. [para(250(a,1),290(a,1,2)),demod(12(4))]. given #110 (T,wt=11): 314 x v y != 0 | (x v y) ' = 1. [para(37(a,1),42(b,1)),demod(89(2),89(2)),xx(a)]. given #111 (A,wt=14): 64 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(46),demod(59(4))]. given #112 (F,wt=7): 1239 x ' != 1 | 0 = x. [para(291(a,1),64(b,1)),demod(272(8),291(9)),flip(a),flip(c),xx(b)]. given #113 (F,wt=11): 315 x v y != 1 | (x v y) ' = 0. [para(40(a,1),42(a,1,2)),demod(14(6),83(6)),xx(b)]. given #114 (T,wt=11): 446 x ^ y != 0 | (x ^ y) ' = 1. [para(37(a,1),44(b,1,2)),demod(12(3),80(3)),xx(a)]. given #115 (T,wt=11): 447 x ^ y != 1 | (x ^ y) ' = 0. [para(40(a,1),44(a,1)),demod(92(5),92(5)),xx(b)]. given #116 (A,wt=14): 68 x v y != 1 | 0 != x | x ' = x v y. [back_demod(45),demod(65(2))]. given #117 (F,wt=7): 1249 x ' != 0 | 1 = x. [para(290(a,1),68(a,1)),demod(272(8),290(9)),flip(b),flip(c),xx(a)]. given #118 (F,wt=11): 768 (x v y) ^ (z ^ y) = z ^ y. [para(61(a,1),96(a,2)),demod(151(4))]. given #119 (T,wt=11): 821 (x ^ y) v (z v y) = z v y. [para(67(a,1),101(a,2)),demod(163(4))]. given #120 (T,wt=11): 1235 x v y != 0 | (y v x) ' = 1. [para(12(a,1),314(a,1))]. given #121 (A,wt=20): 77 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(23(a,1),20(a,1))]. given #122 (F,wt=11): 1240 (x v y) ' != 1 | x v y = 0. [para(600(a,1),64(b,1)),demod(272(10),600(12)),flip(a),xx(b)]. given #123 (F,wt=11): 1241 x v y != 1 | (y v x) ' = 0. [para(12(a,1),315(a,1))]. given #124 (T,wt=11): 1243 x ^ y != 0 | (y ^ x) ' = 1. [para(14(a,1),446(a,1))]. given #125 (T,wt=11): 1245 x ^ y != 1 | (y ^ x) ' = 0. [para(14(a,1),447(a,1))]. given #126 (A,wt=20): 88 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(24(a,1),20(b,1))]. given #127 (F,wt=11): 1250 (x ^ y) ' != 0 | x ^ y = 1. [para(586(a,1),68(a,1)),demod(272(10),586(12)),flip(b),xx(a)]. given #128 (F,wt=11): 1336 (x v y) ' != 1 | y v x = 0. [para(12(a,1),1240(a,1,1))]. given #129 (T,wt=11): 1338 (x ^ y) ' != 1 | x ^ y = 0. [para(32(a,1),1240(a,1,1)),demod(32(8))]. given #130 (T,wt=11): 1382 (x ^ y) ' != 0 | y ^ x = 1. [para(14(a,1),1250(a,1,1))]. given #131 (A,wt=13): 97 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(25(a,1),15(a,1)),flip(a)]. given #132 (F,wt=11): 1384 (x v y) ' != 0 | x v y = 1. [para(26(a,1),1250(a,1,1)),demod(26(8))]. given #133 (F,wt=11): 1387 (x ^ y) ' != 1 | y ^ x = 0. [para(250(a,1),1336(a,1,1)),demod(250(7))]. given #134 (T,wt=11): 1391 (x v y) ' != 0 | y v x = 1. [para(164(a,1),1382(a,1,1)),demod(164(7))]. given #135 (T,wt=12): 107 x v (y v ((x v y) ' v z)) = 1. [para(81(a,1),13(a,1)),flip(a)]. given #136 (A,wt=14): 98 x v y != 1 | 0 != y | y ' = x v y. [para(25(a,1),20(b,1)),demod(67(2)),flip(b)]. given #137 (F,wt=12): 120 x ^ (y ^ ((x ^ y) ' ^ z)) = 0. [para(84(a,1),15(a,1)),flip(a)]. given #138 (F,wt=12): 123 x v (y v (z v (x v y) ')) = 1. [para(90(a,1),13(a,1)),flip(a)]. given #139 (T,wt=12): 126 x ^ (y ^ (z ^ (x ^ y) ')) = 0. [para(93(a,1),15(a,1)),flip(a)]. given #140 (T,wt=12): 140 (x v y) ^ (x v (y v z)) ' = 0. [para(13(a,1),132(a,1,2,1))]. given #141 (A,wt=13): 99 (x v y) ^ (x v (z v y)) = x v y. [para(23(a,1),25(a,1,2))]. given #142 (F,wt=12): 141 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(132(a,1),15(a,1)),flip(a)]. given #143 (F,wt=12): 146 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(139(a,1),15(a,1)),flip(a)]. given #144 (T,wt=12): 148 (x v y) ^ (x v (z v y)) ' = 0. [para(23(a,1),139(a,1,2,1))]. given #145 (T,wt=12): 189 ((x ^ y) v z) ^ (x v z) ' = 0. [para(29(a,1),139(a,1,2,1))]. given #146 (A,wt=13): 102 x v (y v (z ^ (x v y))) = x v y. [para(31(a,1),13(a,1)),flip(a)]. given #147 (F,wt=12): 192 x v (y v ((x v y) ^ z) ') = 1. [para(183(a,1),13(a,1)),flip(a)]. given #148 (F,wt=12): 194 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(15(a,1),183(a,1,2,1))]. given #149 (T,wt=12): 198 x v (y v (z ^ (x v y)) ') = 1. [para(193(a,1),13(a,1)),flip(a)]. given #150 (T,wt=12): 202 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(24(a,1),193(a,1,2,1))]. given #151 (A,wt=14): 104 1 != x | y ^ x != 0 | x ' = y ^ x. [para(31(a,1),20(a,1)),demod(61(4)),flip(a)]. given #152 (F,wt=12): 203 ((x v y) ^ z) v (x ^ z) ' = 1. [para(27(a,1),193(a,1,2,1))]. given #153 (F,wt=12): 217 x v (y v (z v (x v z) ')) = 1. [para(36(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #154 (T,wt=12): 219 x v (y v ((x ^ z) v y) ') = 1. [para(36(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #155 (T,wt=12): 232 x ^ (y ^ (z ^ (x ^ z) ')) = 0. [para(39(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #156 (A,wt=13): 106 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(24(a,1),31(a,1,2))]. given #157 (F,wt=12): 234 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(39(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #158 (F,wt=12): 236 x v (y v (z v (x ' v u))) = 1. [para(13(a,1),109(a,1,2))]. given #159 (T,wt=12): 238 x v (y v ((x ^ z) ' v u)) = 1. [para(109(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #160 (T,wt=12): 240 x ^ (y ^ (z ^ (x ' ^ u))) = 0. [para(15(a,1),122(a,1,2))]. given #161 (A,wt=15): 108 x ^ (x ' v y) != 0 | x ' v y = x '. [para(81(a,1),20(a,1)),flip(c),xx(a)]. given #162 (F,wt=12): 242 x ^ (y ^ ((x v z) ' ^ u)) = 0. [para(122(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #163 (F,wt=12): 253 x v (y v (z v (u v x '))) = 1. [para(13(a,1),124(a,1,2,2))]. given #164 (T,wt=12): 255 x v (y v (z v (x ^ u) ')) = 1. [para(124(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #165 (T,wt=12): 257 x ^ (y ^ (z ^ (u ^ x '))) = 0. [para(15(a,1),127(a,1,2,2))]. given #166 (A,wt=13): 110 (x v y) ^ (y v (x v z)) = y v x. [para(12(a,1),26(a,1,1))]. given #167 (F,wt=12): 259 x ^ (y ^ (z ^ (x v u) ')) = 0. [para(127(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #168 (F,wt=12): 263 x ^ ((y v (x v z)) ' ^ u) = 0. [para(23(a,1),137(a,1,2,1,1))]. given #169 (T,wt=12): 267 x ^ (y ^ (z v (x v u)) ') = 0. [para(23(a,1),138(a,1,2,2,1))]. given #170 (T,wt=12): 297 x v ((x v y) ' v (z v y)) = 1. [para(23(a,1),290(a,1,2)),demod(23(5))]. given #171 (A,wt=13): 111 (x v y) ^ (y v (z v x)) = x v y. [para(12(a,1),26(a,1,2)),demod(13(3))]. given #172 (F,wt=12): 301 x ^ ((x ^ y) ' ^ (z ^ y)) = 0. [para(24(a,1),291(a,1,2)),demod(24(5))]. given #173 (F,wt=12): 305 x ^ (y v (z v (x v u))) ' = 0. [para(13(a,1),143(a,1,2,1))]. given #174 (T,wt=12): 357 x ^ (y v (z v (u v x))) ' = 0. [para(13(a,1),144(a,1,2,1,2))]. given #175 (T,wt=12): 358 x ^ ((y v (z v x)) ' ^ u) = 0. [para(144(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #176 (A,wt=19): 112 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(13(a,1),26(a,1,1)),demod(13(5),13(8))]. given #177 (F,wt=12): 362 x ^ (y ^ (z v (u v x)) ') = 0. [para(144(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #178 (F,wt=12): 370 x ^ (y ^ ((z v x) ' ^ u)) = 0. [para(145(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #179 (T,wt=12): 374 x ^ (y ^ (z ^ (u v x) ')) = 0. [para(15(a,1),149(a,1,2))]. given #180 (T,wt=12): 383 x v ((y ^ (x ^ z)) ' v u) = 1. [para(24(a,1),187(a,1,2,1,1))]. given #181 (A,wt=17): 113 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(26(a,1),15(a,1,1)),flip(a)]. given #182 (F,wt=12): 412 x v (y v (z ^ (x ^ u)) ') = 1. [para(24(a,1),188(a,1,2,2,1))]. given #183 (F,wt=12): 418 x v (y ^ (z ^ (x ^ u))) ' = 1. [para(15(a,1),196(a,1,2,1))]. given #184 (T,wt=12): 423 x v ((y ^ (z ^ x)) ' v u) = 1. [para(15(a,1),197(a,1,2,1,1))]. given #185 (T,wt=12): 425 x v (y v ((z ^ x) ' v u)) = 1. [para(197(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #186 (A,wt=19): 115 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(23(a,1),26(a,1,1)),demod(13(4))]. given #187 (F,wt=12): 432 x v (y ^ (z ^ (u ^ x))) ' = 1. [para(15(a,1),199(a,1,2,1,2))]. given #188 (F,wt=12): 434 x v (y v (z ^ (u ^ x)) ') = 1. [para(199(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #189 (T,wt=12): 499 x v (y v (z v (u ^ x) ')) = 1. [para(13(a,1),201(a,1,2))]. given #190 (T,wt=12): 508 x v (y v ((y v x) ' v z)) = 1. [para(214(a,1),13(a,1,1)),demod(80(2),13(5)),flip(a)]. given #191 (A,wt=15): 116 (x v y) ^ (x v (z v (y v u))) = x v y. [para(23(a,1),26(a,1,2,2))]. given #192 (F,wt=12): 512 x v (y v (z v (z v x) ')) = 1. [para(214(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #193 (F,wt=12): 514 x v (y v (y v (x ^ z)) ') = 1. [para(214(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #194 (T,wt=12): 518 x ^ (y ^ ((y ^ x) ' ^ z)) = 0. [para(229(a,1),15(a,1,1)),demod(83(2),15(5)),flip(a)]. given #195 (T,wt=12): 522 x ^ (y ^ (z ^ (z ^ x) ')) = 0. [para(229(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #196 (A,wt=17): 117 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(26(a,1),24(a,1,2)),flip(a)]. given #197 (F,wt=12): 524 x ^ (y ^ (y ^ (x v z)) ') = 0. [para(229(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #198 (F,wt=12): 529 x ' v (y v (z v (x v u))) = 1. [para(13(a,1),292(a,1,2))]. given #199 (T,wt=12): 579 x ' ^ (y ^ (z ^ (x ^ u))) = 0. [para(15(a,1),293(a,1,2))]. given #200 (T,wt=12): 585 x ' v (y v (z v (u v x))) = 1. [para(13(a,1),294(a,1,2,2))]. given #201 (A,wt=22): 119 x v (y v z) != 1 | x v y != 0 | (x v y) ' = x v (y v z). [back_demod(114),demod(118(4))]. given #202 (F,wt=12): 590 (x ^ (y ^ z)) ' v (u v y) = 1. [para(86(a,1),294(a,1,2,2))]. given #203 (F,wt=12): 592 (x ^ (y ^ z)) ' v (u v z) = 1. [para(103(a,1),294(a,1,2,2))]. given #204 (T,wt=12): 599 x ' ^ (y ^ (z ^ (u ^ x))) = 0. [para(15(a,1),295(a,1,2,2))]. given #205 (T,wt=12): 607 (x v (y v z)) ' ^ (u ^ y) = 0. [para(74(a,1),295(a,1,2,2))]. given #206 (A,wt=15): 121 x v (x ' ^ y) != 1 | x ' ^ y = x '. [para(84(a,1),20(b,1)),flip(c),xx(b)]. given #207 (F,wt=12): 608 (x v (y v z)) ' ^ (u ^ z) = 0. [para(95(a,1),295(a,1,2,2))]. given #208 (F,wt=12): 613 (x ^ y) ' v (z v (x v u)) = 1. [para(586(a,1),13(a,1,1)),demod(80(2),13(5)),flip(a)]. given #209 (T,wt=12): 614 (x ^ y) ' v (z v (u v x)) = 1. [para(13(a,1),586(a,1,2))]. given #210 (T,wt=12): 645 (x ^ y) ' v (z v (y v u)) = 1. [para(589(a,1),13(a,1,1)),demod(80(2),13(5)),flip(a)]. given #211 (A,wt=15): 125 x ^ (y v x ') != 0 | y v x ' = x '. [para(90(a,1),20(a,1)),flip(c),xx(a)]. given #212 (F,wt=12): 646 (x ^ y) ' v (z v (u v y)) = 1. [para(13(a,1),589(a,1,2))]. given #213 (F,wt=12): 656 (x v y) ' ^ (z ^ (x ^ u)) = 0. [para(600(a,1),15(a,1,1)),demod(83(2),15(5)),flip(a)]. given #214 (T,wt=12): 657 (x v y) ' ^ (z ^ (u ^ x)) = 0. [para(15(a,1),600(a,1,2))]. given #215 (T,wt=12): 664 (x v y) ' ^ (z ^ (y ^ u)) = 0. [para(603(a,1),15(a,1,1)),demod(83(2),15(5)),flip(a)]. given #216 (A,wt=15): 128 x v (y ^ x ') != 1 | y ^ x ' = x '. [para(93(a,1),20(b,1)),flip(c),xx(b)]. given #217 (F,wt=12): 665 (x v y) ' ^ (z ^ (u ^ y)) = 0. [para(15(a,1),603(a,1,2))]. given #218 (F,wt=12): 679 (x v (y ^ z)) ^ (x v y) ' = 0. [para(75(a,1),139(a,1,2,1))]. given #219 (T,wt=12): 682 x v (y v (x v (y ^ z)) ') = 1. [para(75(a,1),290(a,1,2)),demod(12(5),13(5))]. given #220 (T,wt=12): 748 (x ^ (y v z)) v (x ^ y) ' = 1. [para(85(a,1),193(a,1,2,1))]. given #221 (A,wt=13): 130 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(59(a,1),15(a,2,2)),demod(24(3),15(2))]. given #222 (F,wt=12): 750 x ^ (y ^ (x ^ (y v z)) ') = 0. [para(85(a,1),291(a,1,2)),demod(14(5),15(5))]. given #223 (F,wt=12): 771 ((x v y) ^ z) v (y ^ z) ' = 1. [para(96(a,1),193(a,1,2,1))]. given #224 (T,wt=12): 775 x ^ (y ^ ((z v x) ^ y) ') = 0. [para(39(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #225 (T,wt=12): 782 x ^ (y ^ (y ^ (z v x)) ') = 0. [para(229(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #226 (A,wt=17): 131 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(27(a,1),15(a,1)),demod(15(2)),flip(a)]. given #227 (F,wt=12): 796 (x ^ (y v z)) v (x ^ z) ' = 1. [para(100(a,1),193(a,1,2,1))]. given #228 (F,wt=12): 800 x ^ (y ^ (x ^ (z v y)) ') = 0. [para(100(a,1),291(a,1,2)),demod(14(5),15(5))]. given #229 (T,wt=12): 819 ((x ^ y) v z) ^ (y v z) ' = 0. [para(101(a,1),139(a,1,2,1))]. given #230 (T,wt=12): 824 x v (y v ((z ^ x) v y) ') = 1. [para(36(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #231 (A,wt=22): 133 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(27(a,1),20(b,1))]. given #232 (F,wt=12): 832 x v (y v (y v (z ^ x)) ') = 1. [para(214(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #233 (F,wt=12): 930 (x v (y ^ z)) ^ (x v z) ' = 0. [para(105(a,1),139(a,1,2,1))]. given #234 (T,wt=12): 934 x v (y v (x v (z ^ y)) ') = 1. [para(105(a,1),290(a,1,2)),demod(12(5),13(5))]. given #235 (T,wt=12): 974 x v (y v (z ^ (y v x)) ') = 1. [para(164(a,1),199(a,1,2,1,2)),demod(13(5))]. given #236 (A,wt=13): 134 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(23(a,1),27(a,1,2,1))]. given #237 (F,wt=12): 976 x v (y v (z v (y v x) ')) = 1. [para(164(a,1),201(a,1,2,2,1)),demod(13(5))]. given #238 (F,wt=12): 977 (x v y) ' ^ (z ^ (y v x)) = 0. [para(164(a,1),295(a,1,2,2))]. given #239 (T,wt=12): 978 (x v y) ' v (z v (y v x)) = 1. [para(164(a,1),589(a,1,1,1))]. given #240 (T,wt=12): 979 (x v y) ^ (y v (x v z)) ' = 0. [para(164(a,1),600(a,1,2)),demod(13(2),14(5))]. given #241 (A,wt=15): 135 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(27(a,1),24(a,1,2)),flip(a)]. given #242 (F,wt=12): 980 (x v y) ^ (z v (y v x)) ' = 0. [para(164(a,1),603(a,1,2)),demod(14(5))]. given #243 (F,wt=12): 984 (x v y) ^ ((y v x) ' ^ z) = 0. [para(972(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #244 (T,wt=12): 986 (x v y) ^ (z ^ (y v x) ') = 0. [para(972(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #245 (T,wt=12): 1221 x ^ (y ^ (z v (y ^ x)) ') = 0. [para(250(a,1),144(a,1,2,1,2)),demod(15(5))]. given #246 (A,wt=15): 136 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(27(a,1),31(a,1,2)),demod(12(4))]. given #247 (F,wt=12): 1222 x ^ (y ^ (z ^ (y ^ x) ')) = 0. [para(250(a,1),149(a,1,2,2,1)),demod(15(5))]. given #248 (F,wt=12): 1224 (x ^ y) ' v (z v (y ^ x)) = 1. [para(250(a,1),294(a,1,2,2))]. given #249 (T,wt=12): 1225 (x ^ y) v (y ^ (x ^ z)) ' = 1. [para(250(a,1),586(a,1,2)),demod(15(2),12(5))]. given #250 (T,wt=12): 1226 (x ^ y) v (z ^ (y ^ x)) ' = 1. [para(250(a,1),589(a,1,2)),demod(12(5))]. given #251 (A,wt=15): 142 x v (x v y) ' != 1 | (x v y) ' = x '. [para(132(a,1),20(b,1)),flip(c),xx(b)]. given #252 (F,wt=12): 1227 (x ^ y) ' ^ (z ^ (y ^ x)) = 0. [para(250(a,1),603(a,1,1,1))]. given #253 (F,wt=12): 1229 (x ^ y) v ((y ^ x) ' v z) = 1. [para(1219(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #254 (T,wt=12): 1232 (x ^ y) v (z v (y ^ x) ') = 1. [para(1219(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #255 (T,wt=12): 1476 (x v y) ^ (y v (z v x)) ' = 0. [para(12(a,1),140(a,1,2,1)),demod(13(3))]. given #256 (A,wt=15): 147 x v (y v x) ' != 1 | (y v x) ' = x '. [para(139(a,1),20(b,1)),flip(c),xx(b)]. given #257 (F,wt=12): 1483 ((x ^ y) v z) ^ (z v x) ' = 0. [para(190(a,1),140(a,1,2,1))]. given #258 (F,wt=12): 1486 ((x ^ y) v z) ^ (z v y) ' = 0. [para(821(a,1),140(a,1,2,1))]. given #259 (T,wt=12): 1510 x ^ (y ^ ((y ^ x) v z) ') = 0. [para(14(a,1),141(a,1,2,2,1,1))]. given #260 (T,wt=12): 1552 (x v (y ^ z)) ^ (y v x) ' = 0. [para(12(a,1),189(a,1,1))]. given #261 (A,wt=13): 151 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(15(a,1),61(a,1,2)),demod(15(5))]. given #262 (F,wt=12): 1554 (x v y) ' ^ ((x ^ z) v y) = 0. [para(189(a,1),14(a,1)),flip(a)]. given #263 (F,wt=12): 1556 ((x ^ y) v (x ^ z)) ^ x ' = 0. [para(17(a,1),189(a,1,2,1))]. given #264 (T,wt=12): 1561 ((x ^ y) v (z ^ x)) ^ x ' = 0. [para(31(a,1),189(a,1,2,1))]. given #265 (T,wt=12): 1610 x v (y v ((y v x) ^ z) ') = 1. [para(12(a,1),192(a,1,2,2,1,1))]. given #266 (A,wt=13): 153 x v (y v (x v z)) = y v (x v z). [para(65(a,1),13(a,2,2)),demod(23(3),13(2))]. given #267 (F,wt=12): 1620 (x ^ y) v (y ^ (z ^ x)) ' = 1. [para(14(a,1),194(a,1,2,1)),demod(15(3))]. given #268 (F,wt=12): 1627 ((x v y) ^ z) v (z ^ x) ' = 1. [para(152(a,1),194(a,1,2,1))]. given #269 (T,wt=12): 1629 ((x v y) ^ z) v (z ^ y) ' = 1. [para(768(a,1),194(a,1,2,1))]. given #270 (T,wt=12): 1671 (x ^ y) ' v ((x v z) ^ y) = 1. [para(203(a,1),12(a,1)),flip(a)]. given #271 (A,wt=13): 154 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(14(a,1),28(a,1,2,2,1))]. given #272 (F,wt=12): 1673 (x ^ (y v z)) v (y ^ x) ' = 1. [para(14(a,1),203(a,1,1))]. given #273 (F,wt=12): 1675 ((x v y) ^ (x v z)) v x ' = 1. [para(16(a,1),203(a,1,2,1))]. given #274 (T,wt=12): 1680 ((x v y) ^ (z v x)) v x ' = 1. [para(25(a,1),203(a,1,2,1))]. given #275 (T,wt=12): 1719 x v (y v ((y ^ z) v x) ') = 1. [para(219(a,1),23(a,1)),flip(a)]. given #276 (A,wt=19): 155 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(28(a,1),15(a,1)),demod(15(2),15(4)),flip(a)]. given #277 (F,wt=12): 1722 x v ((x ^ y) v (x ^ z)) ' = 1. [para(219(a,1),29(a,1)),flip(a)]. given #278 (F,wt=12): 1727 x v ((x ^ y) v (z ^ x)) ' = 1. [para(219(a,1),101(a,1)),flip(a)]. given #279 (T,wt=12): 1782 x ^ (y ^ ((y v z) ^ x) ') = 0. [para(234(a,1),24(a,1)),flip(a)]. given #280 (T,wt=12): 1784 x ^ ((x v y) ^ (x v z)) ' = 0. [para(234(a,1),27(a,1)),flip(a)]. given #281 (A,wt=26): 156 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x ' = y ^ ((x ^ y) v z). [para(28(a,1),20(b,1))]. given #282 (F,wt=12): 1789 x ^ ((x v y) ^ (z v x)) ' = 0. [para(234(a,1),96(a,1)),flip(a)]. given #283 (F,wt=12): 1927 x v ((y v x) ' v (z v y)) = 1. [para(12(a,1),297(a,1,2,1,1))]. given #284 (T,wt=12): 2005 x ^ ((y ^ x) ' ^ (z ^ y)) = 0. [para(14(a,1),301(a,1,2,1,1))]. given #285 (T,wt=12): 2401 x v (y v ((z ^ y) v x) ') = 1. [para(821(a,1),508(a,1,2)),demod(12(4))]. given #286 (A,wt=15): 157 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(23(a,1),28(a,1,2,2))]. given #287 (F,wt=12): 2457 x v ((y ^ x) v (x ^ z)) ' = 1. [para(514(a,1),101(a,1)),flip(a)]. given #288 (F,wt=12): 2478 x ^ (y ^ ((z v y) ^ x) ') = 0. [para(768(a,1),518(a,1,2)),demod(14(4))]. given #289 (T,wt=12): 2553 x ^ ((y v x) ^ (x v z)) ' = 0. [para(524(a,1),96(a,1)),flip(a)]. given #290 (T,wt=12): 2888 (x v y) ' ^ (x v (y ^ z)) = 0. [para(679(a,1),14(a,1)),flip(a)]. given #291 (A,wt=17): 158 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(28(a,1),24(a,1,2)),flip(a)]. given #292 (F,wt=12): 2925 (x ^ y) ' v (x ^ (y v z)) = 1. [para(748(a,1),12(a,1)),flip(a)]. given #293 (F,wt=12): 2973 (x ^ y) ' v ((z v x) ^ y) = 1. [para(771(a,1),12(a,1)),flip(a)]. given #294 (T,wt=12): 2975 (x ^ (y v z)) v (z ^ x) ' = 1. [para(14(a,1),771(a,1,1))]. given #295 (T,wt=12): 2977 ((x v y) ^ (y v z)) v y ' = 1. [para(16(a,1),771(a,1,2,1))]. given #296 (A,wt=19): 159 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(24(a,1),28(a,1,2,2,1)),demod(15(5))]. given #297 (F,wt=12): 2982 ((x v y) ^ (z v y)) v y ' = 1. [para(25(a,1),771(a,1,2,1))]. given #298 (F,wt=12): 3030 x ^ ((y v x) ^ (z v x)) ' = 0. [para(775(a,1),96(a,1)),flip(a)]. given #299 (T,wt=12): 3172 (x ^ y) ' v (x ^ (z v y)) = 1. [para(796(a,1),12(a,1)),flip(a)]. given #300 (T,wt=12): 3230 (x v (y ^ z)) ^ (z v x) ' = 0. [para(12(a,1),819(a,1,1))]. given #301 (A,wt=19): 160 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(28(a,1),31(a,1,2)),demod(12(5))]. given #302 (F,wt=12): 3231 (x v y) ' ^ ((z ^ x) v y) = 0. [para(819(a,1),14(a,1)),flip(a)]. given #303 (F,wt=12): 3233 ((x ^ y) v (y ^ z)) ^ y ' = 0. [para(17(a,1),819(a,1,2,1))]. given #304 (T,wt=12): 3238 ((x ^ y) v (z ^ y)) ^ y ' = 0. [para(31(a,1),819(a,1,2,1))]. given #305 (T,wt=12): 3287 x v ((y ^ x) v (z ^ x)) ' = 1. [para(824(a,1),101(a,1)),flip(a)]. given #306 (A,wt=15): 161 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(28(a,1),27(a,1,2)),demod(27(3)),flip(a)]. given #307 (F,wt=12): 3370 (x v y) ' ^ (x v (z ^ y)) = 0. [para(930(a,1),14(a,1)),flip(a)]. given #308 (F,wt=12): 3877 (x v y) ' ^ ((y ^ z) v x) = 0. [para(1483(a,1),14(a,1)),flip(a)]. given #309 (T,wt=12): 3902 (x v y) ' ^ ((z ^ y) v x) = 0. [para(1486(a,1),14(a,1)),flip(a)]. given #310 (T,wt=12): 3962 (x v y) ' ^ (y v (x ^ z)) = 0. [para(1552(a,1),14(a,1)),flip(a)]. given #311 (A,wt=13): 163 x v (y v (z v x)) = y v (z v x). [para(13(a,1),67(a,1,2)),demod(13(5))]. given #312 (F,wt=12): 4014 x ' ^ ((x ^ y) v (x ^ z)) = 0. [para(17(a,1),1554(a,1,1,1))]. given #313 (F,wt=12): 4018 x ' ^ ((x ^ y) v (z ^ x)) = 0. [para(31(a,1),1554(a,1,1,1))]. given #314 (T,wt=12): 4164 (x ^ y) ' v ((y v z) ^ x) = 1. [para(1627(a,1),12(a,1)),flip(a)]. given #315 (T,wt=12): 4187 (x ^ y) ' v ((z v y) ^ x) = 1. [para(1629(a,1),12(a,1)),flip(a)]. given #316 (A,wt=15): 165 (x v y) ^ (z v (x v (y v u))) = x v y. [para(13(a,1),74(a,1,2,2))]. given #317 (F,wt=12): 4213 (x ^ y) ' v (y ^ (x v z)) = 1. [para(14(a,1),1671(a,1,2))]. given #318 (F,wt=12): 4215 x ' v ((x v y) ^ (x v z)) = 1. [para(16(a,1),1671(a,1,1,1))]. given #319 (T,wt=12): 4219 x ' v ((x v y) ^ (z v x)) = 1. [para(25(a,1),1671(a,1,1,1))]. given #320 (T,wt=12): 5146 (x ^ y) ' v (y ^ (z v x)) = 1. [para(14(a,1),2973(a,1,2))]. given #321 (A,wt=18): 167 x v (y v z) != 1 | 0 != y | y ' = x v (y v z). [para(74(a,1),20(b,1)),demod(153(3)),flip(b)]. given #322 (F,wt=12): 5148 x ' v ((y v x) ^ (x v z)) = 1. [para(16(a,1),2973(a,1,1,1))]. given #323 (F,wt=12): 5152 x ' v ((y v x) ^ (z v x)) = 1. [para(25(a,1),2973(a,1,1,1))]. given #324 (T,wt=12): 5476 (x v y) ' ^ (y v (z ^ x)) = 0. [para(3230(a,1),14(a,1)),flip(a)]. given #325 (T,wt=12): 5591 x ' ^ ((y ^ x) v (x ^ z)) = 0. [para(17(a,1),3231(a,1,1,1))]. given #326 (A,wt=13): 168 x ^ (y ^ (z v (x v u))) = y ^ x. [para(74(a,1),24(a,1,2)),flip(a)]. given #327 (F,wt=12): 5595 x ' ^ ((y ^ x) v (z ^ x)) = 0. [para(31(a,1),3231(a,1,1,1))]. given #328 (F,wt=13): 169 x v ((y ^ (x ^ z)) v u) = x v u. [para(86(a,1),13(a,1,1)),flip(a)]. given #329 (T,wt=13): 174 x v (y v (z ^ (x ^ u))) = y v x. [para(86(a,1),23(a,1,2)),flip(a)]. given #330 (T,wt=13): 176 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(95(a,1),15(a,1,1)),flip(a)]. given #331 (A,wt=15): 170 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(86(a,1),13(a,1)),flip(a)]. given #332 (F,wt=13): 180 x ^ (y ^ (z v (u v x))) = y ^ x. [para(95(a,1),24(a,1,2)),flip(a)]. given #333 (F,wt=13): 205 x v ((y ^ (z ^ x)) v u) = x v u. [para(103(a,1),13(a,1,1)),flip(a)]. given #334 (T,wt=13): 209 x v (y v (z ^ (u ^ x))) = y v x. [para(103(a,1),23(a,1,2)),flip(a)]. given #335 (T,wt=13): 220 x v (y v ((y v x) ^ z)) = x v y. [para(12(a,1),30(a,1,2,2,1))]. given #336 (A,wt=15): 171 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(15(a,1),86(a,1,2,2))]. given #337 (F,wt=13): 243 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(14(a,1),32(a,1,1))]. given #338 (F,wt=13): 244 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(14(a,1),32(a,1,2)),demod(15(3))]. given #339 (T,wt=13): 282 x ^ (x ^ y) ' != 0 | x ^ y = x. [para(183(a,1),41(a,1)),demod(14(6),272(11)),xx(a)]. given #340 (T,wt=13): 283 x ^ (y ^ x) ' != 0 | y ^ x = x. [para(193(a,1),41(a,1)),demod(14(6),272(11)),xx(a)]. given #341 (A,wt=18): 173 1 != x | y ^ (x ^ z) != 0 | x ' = y ^ (x ^ z). [para(86(a,1),20(a,1)),demod(130(5)),flip(a)]. given #342 (F,wt=13): 296 x ' ^ (y v x) != 0 | y v x = x. [para(290(a,1),20(a,1)),demod(272(10)),flip(c),xx(a)]. given #343 (F,wt=13): 300 x ' v (y ^ x) != 1 | y ^ x = x. [para(291(a,1),20(b,1)),demod(272(10)),flip(c),xx(b)]. given #344 (T,wt=13): 303 (x ^ y) v y ' != 1 | x ^ y = y. [para(291(a,1),41(b,1)),demod(272(10)),flip(c),xx(b)]. given #345 (T,wt=13): 393 x v (x v y) ' != 1 | x v y = x. [para(132(a,1),43(b,1)),demod(12(3),272(11)),xx(b)]. given #346 (A,wt=15): 177 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(95(a,1),15(a,1)),flip(a)]. given #347 (F,wt=13): 394 x v (y v x) ' != 1 | y v x = x. [para(139(a,1),43(b,1)),demod(12(3),272(11)),xx(b)]. given #348 (F,wt=13): 403 (x v y) ^ y ' != 0 | x v y = y. [para(290(a,1),43(a,1)),demod(272(10)),flip(c),xx(a)]. given #349 (T,wt=13): 953 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(23(a,1),152(a,1,1))]. given #350 (T,wt=13): 970 x v (y v (z ^ (y v x))) = x v y. [para(164(a,1),103(a,1,2,2)),demod(13(4))]. given #351 (A,wt=18): 178 x v (y v z) != 1 | 0 != z | z ' = x v (y v z). [para(95(a,1),20(b,1)),demod(163(3)),flip(b)]. given #352 (F,wt=13): 981 (x v (y v z)) ^ (y v x) = y v x. [para(164(a,1),152(a,1,2)),demod(13(2),164(7))]. given #353 (F,wt=13): 1066 x ^ (y v (z v (u v (x v v)))) = x. [para(13(a,1),166(a,1,2,2))]. given #354 (T,wt=13): 1080 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(15(a,1),172(a,1,2,2))]. given #355 (T,wt=13): 1090 x ^ (y v (z v (u v (v v x)))) = x. [para(13(a,1),175(a,1,2,2,2))]. given #356 (A,wt=15): 179 (x v y) ^ (z v (x v (u v y))) = x v y. [para(23(a,1),95(a,1,2,2))]. given #357 (F,wt=13): 1117 (x ^ (y ^ z)) v (u v y) = u v y. [para(24(a,1),190(a,1,1))]. given #358 (F,wt=13): 1188 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(15(a,1),207(a,1,2,2,2))]. given #359 (T,wt=13): 1216 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(250(a,1),95(a,1,2,2)),demod(15(4))]. given #360 (T,wt=13): 1217 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(250(a,1),29(a,2)),demod(15(3),1211(6))]. given #361 (A,wt=17): 181 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(29(a,1),13(a,1)),demod(13(2)),flip(a)]. given #362 (F,wt=13): 1251 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(13(a,1),768(a,1,1))]. given #363 (F,wt=13): 1269 (x v (y v z)) ^ (z v y) = z v y. [para(164(a,1),768(a,1,2)),demod(164(7))]. given #364 (T,wt=13): 1276 (x ^ (y ^ z)) v (u v z) = u v z. [para(15(a,1),821(a,1,1))]. given #365 (T,wt=13): 1296 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(250(a,1),821(a,1,2)),demod(250(7))]. given #366 (A,wt=17): 182 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(15(a,1),29(a,1,2,1))]. given #367 (F,wt=13): 1305 x ' ^ (x v y) != 0 | x v y = x. [para(81(a,1),77(a,1)),demod(272(10)),flip(c),xx(a)]. given #368 (F,wt=13): 1350 x ' v (x ^ y) != 1 | x ^ y = x. [para(84(a,1),88(b,1)),demod(272(10)),flip(c),xx(b)]. given #369 (T,wt=13): 1487 (x v y) ^ (z v (y v x)) = x v y. [para(12(a,1),99(a,1,2)),demod(13(3))]. given #370 (T,wt=13): 1748 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(14(a,1),106(a,1,2)),demod(15(3))]. given #371 (A,wt=22): 184 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x ' = (x ^ z) v y. [para(29(a,1),20(a,1))]. given #372 (F,wt=13): 1960 (x v (y v z)) ^ (z v x) = z v x. [para(111(a,1),14(a,1)),flip(a)]. given #373 (F,wt=13): 4047 x ^ ((x ' ^ y) v (x ' ^ z)) = 0. [para(272(a,1),1556(a,1,2)),demod(14(6))]. given #374 (T,wt=13): 4069 x ^ ((x ' ^ y) v (z ^ x ')) = 0. [para(272(a,1),1561(a,1,2)),demod(14(6))]. given #375 (T,wt=13): 4373 x v ((x ' v y) ^ (x ' v z)) = 1. [para(272(a,1),1675(a,1,2)),demod(12(6))]. given #376 (A,wt=15): 185 x v (y v ((x ^ z) v u)) = y v (x v u). [para(29(a,1),23(a,1,2)),flip(a)]. given #377 (F,wt=13): 4396 x v ((x ' v y) ^ (z v x ')) = 1. [para(272(a,1),1680(a,1,2)),demod(12(6))]. given #378 (F,wt=13): 5247 x v ((y v x ') ^ (x ' v z)) = 1. [para(272(a,1),2977(a,1,2)),demod(12(6))]. given #379 (T,wt=13): 5384 x v ((y v x ') ^ (z v x ')) = 1. [para(272(a,1),2982(a,1,2)),demod(12(6))]. given #380 (T,wt=13): 5625 x ^ ((y ^ x ') v (x ' ^ z)) = 0. [para(272(a,1),3233(a,1,2)),demod(14(6))]. given #381 (A,wt=15): 186 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(29(a,1),25(a,1,2)),demod(14(4))]. given #382 (F,wt=13): 5645 x ^ ((y ^ x ') v (z ^ x ')) = 0. [para(272(a,1),3238(a,1,2)),demod(14(6))]. given #383 (F,wt=13): 5723 x ^ (((x v y) ^ (x v z)) v u) = x. [para(161(a,1),27(a,1)),demod(16(2)),flip(a)]. given #384 (T,wt=13): 5738 x ^ (((x v y) ^ (z v x)) v u) = x. [para(161(a,1),96(a,1)),demod(25(2)),flip(a)]. given #385 (T,wt=13): 7133 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(244(a,1),12(a,1)),flip(a)]. given #386 (A,wt=17): 191 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(29(a,1),95(a,1,2,2))]. given #387 (F,wt=13): 7210 x ^ (y ^ x) ' != 0 | x ^ y = x. [para(14(a,1),282(a,1,2,1))]. given #388 (F,wt=13): 7213 x ^ (x ^ y) ' != 0 | y ^ x = x. [para(14(a,1),283(a,1,2,1))]. given #389 (T,wt=13): 7215 (x v y) ^ x ' != 0 | x v y = x. [para(16(a,1),283(a,1,2,1)),demod(16(7)),flip(b)]. given #390 (T,wt=13): 7238 x ' ^ (x v y) != 0 | y v x = x. [para(12(a,1),296(a,1,2))]. given #391 (A,wt=15): 195 x ^ (x ^ y) ' != 0 | (x ^ y) ' = x '. [para(183(a,1),20(a,1)),flip(c),xx(a)]. given #392 (F,wt=13): 7252 x ' v (x ^ y) != 1 | y ^ x = x. [para(14(a,1),300(a,1,2))]. given #393 (F,wt=13): 7267 (x ^ y) v x ' != 1 | y ^ x = x. [para(14(a,1),303(a,1,1))]. given #394 (T,wt=13): 7269 x v (y v x) ' != 1 | x v y = x. [para(12(a,1),393(a,1,2,1))]. given #395 (T,wt=13): 7332 x v (x v y) ' != 1 | y v x = x. [para(12(a,1),394(a,1,2,1))]. given #396 (A,wt=15): 200 x ^ (y ^ x) ' != 0 | (y ^ x) ' = x '. [para(193(a,1),20(a,1)),flip(c),xx(a)]. given #397 (F,wt=13): 7334 (x ^ y) v x ' != 1 | x ^ y = x. [para(17(a,1),394(a,1,2,1)),demod(17(7)),flip(b)]. given #398 (F,wt=13): 7347 (x v y) ^ x ' != 0 | y v x = x. [para(12(a,1),403(a,1,1))]. given #399 (T,wt=13): 8321 x ' ^ (y v x) != 0 | x v y = x. [para(12(a,1),1305(a,1,2))]. given #400 (T,wt=13): 8325 x ' v (y ^ x) != 1 | x ^ y = x. [para(14(a,1),1350(a,1,2))]. given #401 (A,wt=14): 204 (x ^ ((y ^ x) v z)) v (y ^ x) ' = 1. [para(28(a,1),193(a,1,2,1))]. given #402 (F,wt=13): 8618 x ^ (((y v x) ^ (x v z)) v u) = x. [para(12(a,1),5723(a,1,2,1,1))]. given #403 (F,wt=13): 8619 x ^ (y v ((x v z) ^ (x v u))) = x. [para(12(a,1),5723(a,1,2))]. given #404 (T,wt=13): 8675 x ^ (((y v x) ^ (z v x)) v u) = x. [para(12(a,1),5738(a,1,2,1,1))]. given #405 (T,wt=13): 8676 x ^ (y v ((x v z) ^ (u v x))) = x. [para(12(a,1),5738(a,1,2))]. given #406 (A,wt=15): 206 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(103(a,1),13(a,1)),flip(a)]. given #407 (F,wt=13): 8793 (x v y) ^ y ' != 0 | y v x = y. [para(12(a,1),7215(a,1,1))]. given #408 (F,wt=13): 8810 (x ^ y) v y ' != 1 | y ^ x = y. [para(14(a,1),7334(a,1,1))]. given #409 (T,wt=13): 8829 x ^ (y v ((z v x) ^ (x v u))) = x. [para(12(a,1),8618(a,1,2))]. given #410 (T,wt=13): 8935 x ^ (y v ((z v x) ^ (u v x))) = x. [para(12(a,1),8675(a,1,2))]. given #411 (A,wt=18): 208 1 != x | y ^ (z ^ x) != 0 | x ' = y ^ (z ^ x). [para(103(a,1),20(a,1)),demod(151(5)),flip(a)]. given #412 (F,wt=14): 215 x v (y v (z v (x v (y v z)) ')) = 1. [para(36(a,1),13(a,1)),demod(13(3)),flip(a)]. given #413 (F,wt=14): 218 x v (y v (z v (y v (x v z)) ')) = 1. [para(23(a,1),36(a,1,2,2,1)),demod(13(5))]. given #414 (T,wt=14): 226 (x v ((y v x) ^ z)) ^ (y v x) ' = 0. [para(30(a,1),139(a,1,2,1))]. given #415 (T,wt=14): 230 x ^ (y ^ (z ^ (x ^ (y ^ z)) ')) = 0. [para(39(a,1),15(a,1)),demod(15(3)),flip(a)]. given #416 (A,wt=15): 210 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(24(a,1),103(a,1,2,2))]. given #417 (F,wt=14): 233 x ^ (y ^ (z ^ (y ^ (x ^ z)) ')) = 0. [para(24(a,1),39(a,1,2,2,1)),demod(15(5))]. given #418 (F,wt=14): 235 x v (y v (z v ((x v y) ' v u))) = 1. [para(109(a,1),13(a,1)),flip(a)]. given #419 (T,wt=14): 239 x ^ (y ^ (z ^ ((x ^ y) ' ^ u))) = 0. [para(122(a,1),15(a,1)),flip(a)]. given #420 (T,wt=14): 252 x v (y v (z v (u v (x v y) '))) = 1. [para(124(a,1),13(a,1)),flip(a)]. given #421 (A,wt=17): 211 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(26(a,1),103(a,1,2,2)),demod(13(5),13(4))]. given #422 (F,wt=14): 256 x ^ (y ^ (z ^ (u ^ (x ^ y) '))) = 0. [para(127(a,1),15(a,1)),flip(a)]. given #423 (F,wt=14): 260 (x v y) ^ ((x v (y v z)) ' ^ u) = 0. [para(13(a,1),137(a,1,2,1,1))]. given #424 (T,wt=14): 261 x ^ (y ^ (((x ^ y) v z) ' ^ u)) = 0. [para(137(a,1),15(a,1)),flip(a)]. given #425 (T,wt=14): 264 (x v y) ^ (z ^ (x v (y v u)) ') = 0. [para(13(a,1),138(a,1,2,2,1))]. given #426 (A,wt=17): 212 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(27(a,1),103(a,1,2,2))]. given #427 (F,wt=14): 265 x ^ (y ^ (z ^ ((x ^ y) v u) ')) = 0. [para(138(a,1),15(a,1)),flip(a)]. given #428 (F,wt=14): 269 x v y != 1 | x ^ y != 0 | y ' = x. [para(14(a,1),41(b,1))]. given #429 (T,wt=14): 271 1 != x | x ^ y != 0 | (x ^ y) ' = x. [para(17(a,1),41(a,1)),demod(14(4),59(4)),flip(a)]. given #430 (T,wt=14): 275 1 != x | y ^ x != 0 | (y ^ x) ' = x. [para(31(a,1),41(a,1)),demod(14(4),61(4)),flip(a)]. given #431 (A,wt=21): 213 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(28(a,1),103(a,1,2,2))]. given #432 (F,wt=14): 278 x v y != 1 | 0 != x | (x v y) ' = x. [para(65(a,1),41(a,1)),demod(14(5),16(5)),flip(b)]. given #433 (F,wt=14): 279 x v y != 1 | 0 != y | (x v y) ' = y. [para(67(a,1),41(a,1)),demod(14(5),25(5)),flip(b)]. given #434 (T,wt=14): 298 x v (y v (y v ((x v y) ^ z)) ') = 1. [para(30(a,1),290(a,1,2)),demod(12(6),13(6))]. given #435 (T,wt=14): 302 x ^ (y ^ (y ^ ((x ^ y) v z)) ') = 0. [para(28(a,1),291(a,1,2)),demod(14(6),15(6))]. given #436 (A,wt=19): 216 x ^ (y v (x v y) ') != 0 | y v (x v y) ' = x '. [para(36(a,1),20(a,1)),flip(c),xx(a)]. given #437 (F,wt=14): 304 (x v y) ^ (z v (x v (y v u))) ' = 0. [para(13(a,1),143(a,1,2,1,2))]. given #438 (F,wt=14): 306 x ^ (y ^ (z v ((x ^ y) v u)) ') = 0. [para(143(a,1),15(a,1)),flip(a)]. given #439 (T,wt=14): 335 x v y != 1 | 0 != y | (y v x) ' = y. [para(67(a,1),42(a,1)),demod(14(5),16(5)),flip(b)]. given #440 (T,wt=14): 359 x ^ (y ^ (z v (u v (x ^ y))) ') = 0. [para(144(a,1),15(a,1)),flip(a)]. given #441 (A,wt=19): 221 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(30(a,1),13(a,1)),demod(13(2),13(4)),flip(a)]. given #442 (F,wt=14): 361 (x v y) ^ (z v (x v (u v y))) ' = 0. [para(23(a,1),144(a,1,2,1,2))]. given #443 (F,wt=14): 363 ((x ^ y) v z) ^ (u v (x v z)) ' = 0. [para(29(a,1),144(a,1,2,1,2))]. given #444 (T,wt=14): 365 x ^ (y ^ (z ^ (u v (x ^ y)) ')) = 0. [para(32(a,1),144(a,1,2,1,2)),demod(15(6),15(5))]. given #445 (T,wt=14): 367 x ^ (y ^ ((z v (x ^ y)) ' ^ u)) = 0. [para(145(a,1),15(a,1)),flip(a)]. given #446 (A,wt=26): 222 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x ' = y v ((x v y) ^ z). [para(30(a,1),20(a,1))]. given #447 (F,wt=14): 369 (x v y) ^ ((x v (z v y)) ' ^ u) = 0. [para(23(a,1),145(a,1,2,1,1))]. given #448 (F,wt=14): 371 ((x ^ y) v z) ^ ((x v z) ' ^ u) = 0. [para(29(a,1),145(a,1,2,1,1))]. given #449 (T,wt=14): 376 (x v y) ^ (z ^ (x v (u v y)) ') = 0. [para(23(a,1),149(a,1,2,2,1))]. given #450 (T,wt=14): 377 ((x ^ y) v z) ^ (u ^ (x v z) ') = 0. [para(29(a,1),149(a,1,2,2,1))]. given #451 (A,wt=17): 223 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(30(a,1),23(a,1,2)),flip(a)]. given #452 (F,wt=14): 380 x v (y v (((x v y) ^ z) ' v u)) = 1. [para(187(a,1),13(a,1)),flip(a)]. given #453 (F,wt=14): 381 (x ^ y) v ((x ^ (y ^ z)) ' v u) = 1. [para(15(a,1),187(a,1,2,1,1))]. given #454 (T,wt=14): 409 x v (y v (z v ((x v y) ^ u) ')) = 1. [para(188(a,1),13(a,1)),flip(a)]. given #455 (T,wt=14): 410 (x ^ y) v (z v (x ^ (y ^ u)) ') = 1. [para(15(a,1),188(a,1,2,2,1))]. given #456 (A,wt=19): 224 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(23(a,1),30(a,1,2,2,1)),demod(13(5))]. given #457 (F,wt=14): 416 x v (y v (z ^ ((x v y) ^ u)) ') = 1. [para(196(a,1),13(a,1)),flip(a)]. given #458 (F,wt=14): 417 (x ^ y) v (z ^ (x ^ (y ^ u))) ' = 1. [para(15(a,1),196(a,1,2,1,2))]. given #459 (T,wt=14): 422 x v (y v ((z ^ (x v y)) ' v u)) = 1. [para(197(a,1),13(a,1)),flip(a)]. given #460 (T,wt=14): 426 (x ^ y) v ((x ^ (z ^ y)) ' v u) = 1. [para(24(a,1),197(a,1,2,1,1))]. given #461 (A,wt=19): 225 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(30(a,1),25(a,1,2)),demod(14(5))]. given #462 (F,wt=14): 427 ((x v y) ^ z) v ((x ^ z) ' v u) = 1. [para(27(a,1),197(a,1,2,1,1))]. given #463 (F,wt=14): 431 x v (y v (z ^ (u ^ (x v y))) ') = 1. [para(199(a,1),13(a,1)),flip(a)]. given #464 (T,wt=14): 435 (x ^ y) v (z ^ (x ^ (u ^ y))) ' = 1. [para(24(a,1),199(a,1,2,1,2))]. given #465 (T,wt=14): 436 x v (y v (z v (u ^ (x v y)) ')) = 1. [para(26(a,1),199(a,1,2,1,2)),demod(13(6),13(5))]. given #466 (A,wt=21): 227 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(30(a,1),95(a,1,2,2))]. given #467 (F,wt=14): 437 ((x v y) ^ z) v (u ^ (x ^ z)) ' = 1. [para(27(a,1),199(a,1,2,1,2))]. given #468 (F,wt=14): 465 1 != x | y ^ x != 0 | (x ^ y) ' = x. [para(61(a,1),44(b,1)),demod(12(2),17(2)),flip(a)]. given #469 (T,wt=14): 501 (x ^ y) v (z v (x ^ (u ^ y)) ') = 1. [para(24(a,1),201(a,1,2,2,1))]. given #470 (T,wt=14): 502 ((x v y) ^ z) v (u v (x ^ z) ') = 1. [para(27(a,1),201(a,1,2,2,1))]. given #471 (A,wt=15): 228 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(30(a,1),29(a,1,2)),demod(29(3)),flip(a)]. given #472 (F,wt=13): 9960 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(228(a,1),29(a,1)),demod(17(2)),flip(a)]. given #473 (F,wt=13): 9970 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(228(a,1),101(a,1)),demod(31(2)),flip(a)]. given #474 (T,wt=13): 10011 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(14(a,1),9960(a,1,2,1,1))]. given #475 (T,wt=13): 10012 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(14(a,1),9960(a,1,2))]. given #476 (A,wt=19): 231 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(39(a,1),20(b,1)),flip(c),xx(b)]. given #477 (F,wt=13): 10063 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(14(a,1),9970(a,1,2,1,1))]. given #478 (F,wt=13): 10064 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(14(a,1),9970(a,1,2))]. given #479 (T,wt=13): 10113 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(14(a,1),10011(a,1,2))]. given #480 (T,wt=13): 10206 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(14(a,1),10063(a,1,2))]. given #481 (A,wt=19): 237 x ^ (y v (x ' v z)) != 0 | y v (x ' v z) = x '. [para(109(a,1),20(a,1)),flip(c),xx(a)]. given #482 (F,wt=14): 509 x v (y v (z v (z v (x v y)) ')) = 1. [para(214(a,1),13(a,1)),flip(a)]. given #483 (F,wt=14): 510 x v (y v (z v (y v (z v x)) ')) = 1. [para(13(a,1),214(a,1,2,2,1)),demod(13(5))]. given #484 (T,wt=14): 513 x v (y v (z v (x v (z v y)) ')) = 1. [para(23(a,1),214(a,1,2,2,1)),demod(13(6))]. given #485 (T,wt=14): 519 x ^ (y ^ (z ^ (z ^ (x ^ y)) ')) = 0. [para(229(a,1),15(a,1)),flip(a)]. given #486 (A,wt=19): 241 x v (y ^ (x ' ^ z)) != 1 | y ^ (x ' ^ z) = x '. [para(122(a,1),20(b,1)),flip(c),xx(b)]. given #487 (F,wt=14): 520 x ^ (y ^ (z ^ (y ^ (z ^ x)) ')) = 0. [para(15(a,1),229(a,1,2,2,1)),demod(15(5))]. given #488 (F,wt=14): 523 x ^ (y ^ (z ^ (x ^ (z ^ y)) ')) = 0. [para(24(a,1),229(a,1,2,2,1)),demod(15(6))]. given #489 (T,wt=14): 528 (x v y) ' v (z v (x v (y v u))) = 1. [para(13(a,1),292(a,1,2,2))]. given #490 (T,wt=14): 578 (x ^ y) ' ^ (z ^ (x ^ (y ^ u))) = 0. [para(15(a,1),293(a,1,2,2))]. given #491 (A,wt=19): 245 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(15(a,1),32(a,1,1)),demod(15(5),15(8))]. given #492 (F,wt=14): 588 (x v y) ' v (z v (x v (u v y))) = 1. [para(23(a,1),294(a,1,2,2))]. given #493 (F,wt=14): 591 ((x ^ y) v z) ' v (u v (x v z)) = 1. [para(29(a,1),294(a,1,2,2))]. given #494 (T,wt=14): 594 (x ^ (y ^ z)) ' v (u v (x ^ y)) = 1. [para(32(a,1),294(a,1,2,2))]. given #495 (T,wt=14): 602 (x ^ y) ' ^ (z ^ (x ^ (u ^ y))) = 0. [para(24(a,1),295(a,1,2,2))]. given #496 (A,wt=22): 246 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = x ^ (y ^ z). [para(32(a,1),20(a,1)),demod(24(7),24(6),15(5),130(6),59(6))]. given #497 (F,wt=14): 604 (x v (y v z)) ' ^ (u ^ (x v y)) = 0. [para(26(a,1),295(a,1,2,2))]. given #498 (F,wt=14): 605 ((x v y) ^ z) ' ^ (u ^ (x ^ z)) = 0. [para(27(a,1),295(a,1,2,2))]. given #499 (T,wt=14): 616 x v (((x v y) ^ z) ' v (u v y)) = 1. [para(23(a,1),586(a,1,2)),demod(23(6))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 156 (0.00 of 7.58 sec). given #500 (T,wt=14): 617 x v (y v (((x ^ z) v y) ^ u) ') = 1. [para(29(a,1),586(a,1,2)),demod(12(6),13(6))]. given #501 (A,wt=17): 247 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(32(a,1),23(a,1,2)),flip(a)]. given #502 (F,wt=14): 648 x v ((y ^ (x v z)) ' v (u v z)) = 1. [para(23(a,1),589(a,1,2)),demod(23(6))]. given #503 (F,wt=14): 649 (x ^ (y ^ z)) ' v (u v (x ^ z)) = 1. [para(24(a,1),589(a,1,1,1))]. given #504 (T,wt=14): 650 (x ^ y) ' v (z v ((x v u) ^ y)) = 1. [para(27(a,1),589(a,1,1,1))]. given #505 (T,wt=14): 652 x v (y v (z ^ ((x ^ u) v y)) ') = 1. [para(29(a,1),589(a,1,2)),demod(12(6),13(6))]. given #506 (A,wt=19): 248 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(24(a,1),32(a,1,1)),demod(15(4))]. given #507 (F,wt=14): 659 x ^ (((x ^ y) v z) ' ^ (u ^ y)) = 0. [para(24(a,1),600(a,1,2)),demod(24(6))]. given #508 (F,wt=14): 660 x ^ (y ^ (((x v z) ^ y) v u) ') = 0. [para(27(a,1),600(a,1,2)),demod(14(6),15(6))]. given #509 (T,wt=14): 667 (x v (y v z)) ' ^ (u ^ (x v z)) = 0. [para(23(a,1),603(a,1,1,1))]. given #510 (T,wt=14): 668 x ^ ((y v (x ^ z)) ' ^ (u ^ z)) = 0. [para(24(a,1),603(a,1,2)),demod(24(6))]. given #511 (A,wt=15): 249 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(24(a,1),32(a,1,2,2))]. given #512 (F,wt=14): 669 x ^ (y ^ (z v ((x v u) ^ y)) ') = 0. [para(27(a,1),603(a,1,2)),demod(14(6),15(6))]. given #513 (F,wt=14): 671 (x v y) ' ^ (z ^ ((x ^ u) v y)) = 0. [para(29(a,1),603(a,1,1,1))]. given #514 (T,wt=14): 685 (x v (y ^ z)) ^ (u v (x v y)) ' = 0. [para(75(a,1),144(a,1,2,1,2))]. given #515 (T,wt=14): 686 (x v (y ^ z)) ^ ((x v y) ' ^ u) = 0. [para(75(a,1),145(a,1,2,1,1))]. given #516 (A,wt=17): 251 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(32(a,1),95(a,1,2,2)),demod(15(5),15(4))]. given #517 (F,wt=14): 687 (x v (y ^ z)) ^ (u ^ (x v y) ') = 0. [para(75(a,1),149(a,1,2,2,1))]. given #518 (F,wt=14): 689 (x v (y ^ z)) ' v (u v (x v y)) = 1. [para(75(a,1),294(a,1,2,2))]. given #519 (T,wt=14): 690 x v (y v ((x v (y ^ z)) ^ u) ') = 1. [para(75(a,1),586(a,1,2)),demod(12(6),13(6))]. given #520 (T,wt=14): 691 x v (y v (z ^ (x v (y ^ u))) ') = 1. [para(75(a,1),589(a,1,2)),demod(12(6),13(6))]. given #521 (A,wt=19): 254 x ^ (y v (z v x ')) != 0 | y v (z v x ') = x '. [para(124(a,1),20(a,1)),flip(c),xx(a)]. given #522 (F,wt=14): 692 (x v y) ' ^ (z ^ (x v (y ^ u))) = 0. [para(75(a,1),603(a,1,1,1))]. given #523 (F,wt=14): 753 (x ^ (y v z)) v ((x ^ y) ' v u) = 1. [para(85(a,1),197(a,1,2,1,1))]. given #524 (T,wt=14): 754 (x ^ (y v z)) v (u ^ (x ^ y)) ' = 1. [para(85(a,1),199(a,1,2,1,2))]. given #525 (T,wt=14): 757 (x ^ (y v z)) v (u v (x ^ y) ') = 1. [para(85(a,1),201(a,1,2,2,1))]. given #526 (A,wt=19): 258 x v (y ^ (z ^ x ')) != 1 | y ^ (z ^ x ') = x '. [para(127(a,1),20(b,1)),flip(c),xx(b)]. given #527 (F,wt=14): 758 (x ^ (y v z)) ' ^ (u ^ (x ^ y)) = 0. [para(85(a,1),295(a,1,2,2))]. given #528 (F,wt=14): 759 (x ^ y) ' v (z v (x ^ (y v u))) = 1. [para(85(a,1),589(a,1,1,1))]. given #529 (T,wt=14): 760 x ^ (y ^ ((x ^ (y v z)) v u) ') = 0. [para(85(a,1),600(a,1,2)),demod(14(6),15(6))]. given #530 (T,wt=14): 761 x ^ (y ^ (z v (x ^ (y v u))) ') = 0. [para(85(a,1),603(a,1,2)),demod(14(6),15(6))]. given #531 (A,wt=19): 262 x v ((x v y) ' ^ z) != 1 | (x v y) ' ^ z = x '. [para(137(a,1),20(b,1)),flip(c),xx(b)]. given #532 (F,wt=14): 778 ((x v y) ^ z) v ((y ^ z) ' v u) = 1. [para(96(a,1),197(a,1,2,1,1))]. given #533 (F,wt=14): 779 ((x v y) ^ z) v (u ^ (y ^ z)) ' = 1. [para(96(a,1),199(a,1,2,1,2))]. given #534 (T,wt=14): 781 ((x v y) ^ z) v (u v (y ^ z) ') = 1. [para(96(a,1),201(a,1,2,2,1))]. given #535 (T,wt=14): 783 ((x v y) ^ z) ' ^ (u ^ (y ^ z)) = 0. [para(96(a,1),295(a,1,2,2))]. given #536 (A,wt=19): 266 x v (y ^ (x v z) ') != 1 | y ^ (x v z) ' = x '. [para(138(a,1),20(b,1)),flip(c),xx(b)]. given #537 (F,wt=14): 784 (x ^ y) ' v (z v ((u v x) ^ y)) = 1. [para(96(a,1),589(a,1,1,1))]. given #538 (F,wt=14): 785 x ^ (y ^ (((z v x) ^ y) v u) ') = 0. [para(96(a,1),600(a,1,2)),demod(14(6),15(6))]. given #539 (T,wt=14): 786 x ^ (y ^ (z v ((u v x) ^ y)) ') = 0. [para(96(a,1),603(a,1,2)),demod(14(6),15(6))]. given #540 (T,wt=14): 803 (x ^ (y v z)) v ((x ^ z) ' v u) = 1. [para(100(a,1),197(a,1,2,1,1))]. given #541 (A,wt=20): 268 x v (y v z) != 1 | z ^ (x v y) != 0 | z ' = x v y. [para(13(a,1),41(a,1))]. given #542 (F,wt=14): 804 (x ^ (y v z)) v (u ^ (x ^ z)) ' = 1. [para(100(a,1),199(a,1,2,1,2))]. given #543 (F,wt=14): 807 (x ^ (y v z)) v (u v (x ^ z) ') = 1. [para(100(a,1),201(a,1,2,2,1))]. given #544 (T,wt=14): 808 (x ^ (y v z)) ' ^ (u ^ (x ^ z)) = 0. [para(100(a,1),295(a,1,2,2))]. given #545 (T,wt=14): 809 (x ^ y) ' v (z v (x ^ (u v y))) = 1. [para(100(a,1),589(a,1,1,1))]. given #546 (A,wt=20): 270 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z) ' = x. [para(15(a,1),41(b,1))]. given #547 (F,wt=14): 810 x ^ (y ^ ((x ^ (z v y)) v u) ') = 0. [para(100(a,1),600(a,1,2)),demod(14(6),15(6))]. given #548 (F,wt=14): 811 x ^ (y ^ (z v (x ^ (u v y))) ') = 0. [para(100(a,1),603(a,1,2)),demod(14(6),15(6))]. given #549 (T,wt=14): 828 ((x ^ y) v z) ^ (u v (y v z)) ' = 0. [para(101(a,1),144(a,1,2,1,2))]. given #550 (T,wt=14): 829 ((x ^ y) v z) ^ ((y v z) ' ^ u) = 0. [para(101(a,1),145(a,1,2,1,1))]. given #551 (A,wt=20): 273 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z) ' = y. [para(23(a,1),41(a,1))]. given #552 (F,wt=14): 830 ((x ^ y) v z) ^ (u ^ (y v z) ') = 0. [para(101(a,1),149(a,1,2,2,1))]. given #553 (F,wt=14): 833 ((x ^ y) v z) ' v (u v (y v z)) = 1. [para(101(a,1),294(a,1,2,2))]. given #554 (T,wt=14): 834 x v (y v (((z ^ x) v y) ^ u) ') = 1. [para(101(a,1),586(a,1,2)),demod(12(6),13(6))]. given #555 (T,wt=14): 835 x v (y v (z ^ ((u ^ x) v y)) ') = 1. [para(101(a,1),589(a,1,2)),demod(12(6),13(6))]. given #556 (A,wt=20): 274 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z ' = x ^ y. [para(24(a,1),41(b,1))]. given #557 (F,wt=14): 836 (x v y) ' ^ (z ^ ((u ^ x) v y)) = 0. [para(101(a,1),603(a,1,1,1))]. given #558 (F,wt=14): 937 (x v (y ^ z)) ^ (u v (x v z)) ' = 0. [para(105(a,1),144(a,1,2,1,2))]. given #559 (T,wt=14): 938 (x v (y ^ z)) ^ ((x v z) ' ^ u) = 0. [para(105(a,1),145(a,1,2,1,1))]. given #560 (T,wt=14): 939 (x v (y ^ z)) ^ (u ^ (x v z) ') = 0. [para(105(a,1),149(a,1,2,2,1))]. given #561 (A,wt=15): 276 x ^ (x ' v y) != 0 | (x ' v y) ' = x. [para(81(a,1),41(a,1)),demod(14(6)),xx(a)]. given #562 (F,wt=14): 941 (x v (y ^ z)) ' v (u v (x v z)) = 1. [para(105(a,1),294(a,1,2,2))]. given #563 (F,wt=14): 942 x v (y v ((x v (z ^ y)) ^ u) ') = 1. [para(105(a,1),586(a,1,2)),demod(12(6),13(6))]. given #564 (T,wt=14): 943 x v (y v (z ^ (x v (u ^ y))) ') = 1. [para(105(a,1),589(a,1,2)),demod(12(6),13(6))]. given #565 (T,wt=14): 944 (x v y) ' ^ (z ^ (x v (u ^ y))) = 0. [para(105(a,1),603(a,1,1,1))]. given #566 (A,wt=15): 277 x ^ (y v x ') != 0 | (y v x ') ' = x. [para(90(a,1),41(a,1)),demod(14(6)),xx(a)]. given #567 (F,wt=14): 982 (x v (y v z)) ^ (z v (x v y)) ' = 0. [para(13(a,1),972(a,1,1))]. given #568 (F,wt=14): 983 (x v (y v z)) ^ (y v (z v x)) ' = 0. [para(13(a,1),972(a,1,2,1))]. given #569 (T,wt=14): 985 (x v (y v z)) ^ (x v (z v y)) ' = 0. [para(23(a,1),972(a,1,1)),demod(13(4))]. given #570 (T,wt=14): 1074 (x v (y v (z v u))) ' ^ (v ^ z) = 0. [para(166(a,1),295(a,1,2,2))]. given #571 (A,wt=18): 280 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z)) ' = x. [para(86(a,1),41(a,1)),demod(14(5),130(5)),flip(a)]. given #572 (F,wt=14): 1075 x ' v (y v (z v (u v (x v v)))) = 1. [para(166(a,1),589(a,1,1,1))]. given #573 (F,wt=14): 1076 x ^ (y v (z v (u v (x v v)))) ' = 0. [para(166(a,1),603(a,1,2)),demod(14(6))]. given #574 (T,wt=14): 1086 (x ^ (y ^ (z ^ u))) ' v (v v z) = 1. [para(172(a,1),294(a,1,2,2))]. given #575 (T,wt=14): 1087 x v (y ^ (z ^ (u ^ (x ^ v)))) ' = 1. [para(172(a,1),589(a,1,2)),demod(12(6))]. given #576 (A,wt=22): 281 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y) ' = x. [para(29(a,1),41(a,1)),demod(14(6))]. given #577 (F,wt=14): 1088 x ' ^ (y ^ (z ^ (u ^ (x ^ v)))) = 0. [para(172(a,1),603(a,1,1,1))]. given #578 (F,wt=14): 1104 (x v (y v (z v u))) ' ^ (v ^ u) = 0. [para(175(a,1),295(a,1,2,2))]. given #579 (T,wt=14): 1105 x ' v (y v (z v (u v (v v x)))) = 1. [para(175(a,1),589(a,1,1,1))]. given #580 (T,wt=14): 1106 x ^ (y v (z v (u v (v v x)))) ' = 0. [para(175(a,1),603(a,1,2)),demod(14(6))]. given #581 (A,wt=18): 284 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x)) ' = x. [para(103(a,1),41(a,1)),demod(14(5),151(5)),flip(a)]. given #582 (F,wt=14): 1199 (x ^ (y ^ (z ^ u))) ' v (v v u) = 1. [para(207(a,1),294(a,1,2,2))]. given #583 (F,wt=14): 1200 x v (y ^ (z ^ (u ^ (v ^ x)))) ' = 1. [para(207(a,1),589(a,1,2)),demod(12(6))]. given #584 (T,wt=14): 1201 x ' ^ (y ^ (z ^ (u ^ (v ^ x)))) = 0. [para(207(a,1),603(a,1,1,1))]. given #585 (T,wt=14): 1230 (x ^ (y ^ z)) v (z ^ (x ^ y)) ' = 1. [para(15(a,1),1219(a,1,1))]. given #586 (A,wt=19): 285 x ^ (y v (x v y) ') != 0 | (y v (x v y) ') ' = x. [para(36(a,1),41(a,1)),demod(14(7)),xx(a)]. given #587 (F,wt=14): 1231 (x ^ (y ^ z)) v (y ^ (z ^ x)) ' = 1. [para(15(a,1),1219(a,1,2,1))]. given #588 (F,wt=14): 1233 (x ^ (y ^ z)) v (x ^ (z ^ y)) ' = 1. [para(24(a,1),1219(a,1,1)),demod(15(4))]. given #589 (T,wt=14): 1237 1 != x | y ^ x != 0 | x ' = x ^ y. [para(14(a,1),64(b,1))]. given #590 (T,wt=14): 1247 x v y != 1 | 0 != y | y ' = y v x. [para(12(a,1),68(a,1))]. given #591 (A,wt=26): 286 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z)) ' = x. [para(30(a,1),41(a,1)),demod(14(7))]. given #592 (F,wt=14): 1396 (x ^ (y v (z ^ x))) v (z ^ x) ' = 1. [para(97(a,1),193(a,1,2,1))]. given #593 (F,wt=14): 1398 x ^ (y ^ (y ^ (z v (x ^ y))) ') = 0. [para(97(a,1),291(a,1,2)),demod(14(6),15(6))]. given #594 (T,wt=14): 1425 x v (y v (z v ((x v z) ' v u))) = 1. [para(107(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #595 (T,wt=14): 1427 x v (y v (((x ^ z) v y) ' v u)) = 1. [para(107(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #596 (A,wt=19): 287 x ^ (y v (x ' v z)) != 0 | (y v (x ' v z)) ' = x. [para(109(a,1),41(a,1)),demod(14(7)),xx(a)]. given #597 (F,wt=14): 1431 x v (y v (((z ^ x) v y) ' v u)) = 1. [para(107(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #598 (F,wt=14): 1434 x v y != 1 | 0 != x | x ' = y v x. [para(12(a,1),98(a,1))]. given #599 (T,wt=14): 1443 x ^ (y ^ (z ^ ((x ^ z) ' ^ u))) = 0. [para(120(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #600 (T,wt=14): 1445 x ^ (y ^ (((x v z) ^ y) ' ^ u)) = 0. [para(120(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #601 (A,wt=22): 288 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z)) ' = x ^ y. [para(32(a,1),41(a,1)),demod(14(7),24(7),24(6),15(5),130(6),59(6))]. given #602 (F,wt=14): 1449 x ^ (y ^ (((z v x) ^ y) ' ^ u)) = 0. [para(120(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #603 (F,wt=14): 1455 x v (y v (z v (u v (x v z) '))) = 1. [para(123(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #604 (T,wt=14): 1457 x v (y v (z v ((x ^ u) v y) ')) = 1. [para(123(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #605 (T,wt=14): 1461 x v (y v (z v ((u ^ x) v y) ')) = 1. [para(123(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #606 (A,wt=19): 289 x ^ (y v (z v x ')) != 0 | (y v (z v x ')) ' = x. [para(124(a,1),41(a,1)),demod(14(7)),xx(a)]. given #607 (F,wt=10): 11026 x v y != 0 | y v x = 0. [para(110(a,1),289(a,1)),demod(214(7),79(5)),flip(b)]. given #608 (F,wt=10): 11029 x ^ y != 0 | y ^ x = 0. [para(250(a,1),11026(a,1)),demod(250(6))]. given #609 (T,wt=14): 1466 x ^ (y ^ (z ^ (u ^ (x ^ z) '))) = 0. [para(126(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #610 (T,wt=14): 1468 x ^ (y ^ (z ^ ((x v u) ^ y) ')) = 0. [para(126(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #611 (A,wt=15): 299 (x v y) ^ y ' != 0 | (x v y) ' = y '. [para(290(a,1),41(a,1)),xx(a)]. given #612 (F,wt=14): 1472 x ^ (y ^ (z ^ ((u v x) ^ y) ')) = 0. [para(126(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #613 (F,wt=14): 1479 (x v y) ^ (x v (z v (y v u))) ' = 0. [para(23(a,1),140(a,1,2,1,2))]. given #614 (T,wt=14): 1482 (x v (y ^ z)) ^ (x v (u v y)) ' = 0. [para(190(a,1),140(a,1,2,1,2))]. given #615 (T,wt=14): 1485 (x v (y ^ z)) ^ (x v (u v z)) ' = 0. [para(821(a,1),140(a,1,2,1,2))]. given #616 (A,wt=19): 307 x v (y v (x v z)) ' != 1 | (y v (x v z)) ' = x '. [para(143(a,1),20(b,1)),flip(c),xx(b)]. given #617 (F,wt=14): 1500 x v (y v (z v (u ^ (x v z)) ')) = 1. [para(99(a,1),199(a,1,2,1,2)),demod(13(6),13(5))]. given #618 (F,wt=14): 1513 x ^ (y ^ (z ^ ((x ^ z) v u) ')) = 0. [para(141(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #619 (T,wt=14): 1523 x ^ (y ^ (z ^ (u v (x ^ z)) ')) = 0. [para(146(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #620 (T,wt=14): 1532 (x v y) ^ (x v (z v (u v y))) ' = 0. [para(13(a,1),148(a,1,2,1,2))]. given #621 (A,wt=20): 308 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x) ' = y. [para(12(a,1),42(a,1)),demod(13(2))]. given #622 (F,wt=14): 1535 (x v (y ^ (z ^ u))) ^ (x v z) ' = 0. [para(86(a,1),148(a,1,2,1,2))]. given #623 (F,wt=14): 1537 (x v (y ^ (z ^ u))) ^ (x v u) ' = 0. [para(103(a,1),148(a,1,2,1,2))]. given #624 (T,wt=14): 1539 (x v ((x v y) ^ z)) ^ (x v y) ' = 0. [para(30(a,1),148(a,1,2,1))]. given #625 (T,wt=14): 1549 (x v (y ^ z)) ^ (x v (z ^ y)) ' = 0. [para(250(a,1),148(a,1,2,1,2))]. given #626 (A,wt=20): 309 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y) ' = z. [para(12(a,1),42(b,1,1))]. given #627 (F,wt=14): 1560 ((x ^ (y ^ z)) v u) ^ (y v u) ' = 0. [para(24(a,1),189(a,1,1,1))]. given #628 (F,wt=14): 1562 ((x ^ y) v (z ^ (x ^ u))) ^ x ' = 0. [para(86(a,1),189(a,1,2,1))]. given #629 (T,wt=14): 1564 ((x ^ y) v (z ^ (u ^ x))) ^ x ' = 0. [para(103(a,1),189(a,1,2,1))]. given #630 (T,wt=14): 1573 ((x ^ y) v z) ^ (y v (u v z)) ' = 0. [para(152(a,1),189(a,1,1,1)),demod(13(4))]. given #631 (A,wt=26): 310 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z)) ' = u. [para(13(a,1),42(a,1,2))]. given #632 (F,wt=14): 1582 (x v (y ^ (z v x))) ^ (z v x) ' = 0. [para(102(a,1),139(a,1,2,1))]. given #633 (F,wt=14): 1585 x v (y v (y v (z ^ (x v y))) ') = 1. [para(102(a,1),290(a,1,2)),demod(12(6),13(6))]. given #634 (T,wt=14): 1607 (x v (y ^ (x v z))) ^ (x v z) ' = 0. [para(102(a,1),148(a,1,2,1))]. given #635 (T,wt=14): 1613 x v (y v (z v ((x v z) ^ u) ')) = 1. [para(192(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #636 (A,wt=20): 311 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y) ' = z. [para(14(a,1),42(b,1))]. given #637 (F,wt=14): 1623 (x ^ y) v (x ^ (z ^ (y ^ u))) ' = 1. [para(24(a,1),194(a,1,2,1,2))]. given #638 (F,wt=14): 1626 (x ^ (y v z)) v (x ^ (u ^ y)) ' = 1. [para(152(a,1),194(a,1,2,1,2))]. given #639 (T,wt=14): 1628 (x ^ (y v z)) v (x ^ (u ^ z)) ' = 1. [para(768(a,1),194(a,1,2,1,2))]. given #640 (T,wt=14): 1639 (x ^ y) v (x ^ (z ^ (u ^ y))) ' = 1. [para(15(a,1),202(a,1,2,1,2))]. given #641 (A,wt=18): 312 x v y != 1 | y ^ z != 0 | (x v y) ' = y ^ z. [para(17(a,1),42(a,1,2)),demod(24(6),96(6))]. given #642 (F,wt=14): 1645 (x ^ ((x ^ y) v z)) v (x ^ y) ' = 1. [para(28(a,1),202(a,1,2,1))]. given #643 (F,wt=14): 1646 (x ^ (y v (z v u))) v (x ^ z) ' = 1. [para(74(a,1),202(a,1,2,1,2))]. given #644 (T,wt=14): 1647 (x ^ (y v (z v u))) v (x ^ u) ' = 1. [para(95(a,1),202(a,1,2,1,2))]. given #645 (T,wt=14): 1653 (x ^ (y v z)) v (x ^ (z v y)) ' = 1. [para(164(a,1),202(a,1,2,1,2))]. given #646 (A,wt=18): 313 x v y != 1 | x v y != 0 | (x v y) ' = x v y. [para(33(a,1),42(b,1)),demod(67(2),65(2))]. given #647 (F,wt=14): 1659 (x ^ (y v (x ^ z))) v (x ^ z) ' = 1. [para(97(a,1),202(a,1,2,1))]. given #648 (F,wt=14): 1661 1 != x | x ^ y != 0 | x ' = y ^ x. [para(14(a,1),104(b,1))]. given #649 (T,wt=14): 1677 ((x v (y v z)) ^ u) v (y ^ u) ' = 1. [para(23(a,1),203(a,1,1,1))]. given #650 (T,wt=14): 1684 ((x v y) ^ (z v (x v u))) v x ' = 1. [para(74(a,1),203(a,1,2,1))]. given #651 (A,wt=26): 316 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z) ' = y v u. [para(23(a,1),42(a,1,2))]. given #652 (F,wt=14): 1685 ((x v y) ^ (z v (u v x))) v x ' = 1. [para(95(a,1),203(a,1,2,1))]. given #653 (F,wt=14): 1694 ((x v y) ^ z) v (y ^ (u ^ z)) ' = 1. [para(190(a,1),203(a,1,1,1)),demod(15(4))]. given #654 (T,wt=14): 1703 x v (y v (z v (u v (x v u) '))) = 1. [para(13(a,1),217(a,1,2))]. given #655 (T,wt=14): 1705 x v (y v (z v ((x ^ u) v z) ')) = 1. [para(217(a,1),29(a,1,2)),demod(89(2)),flip(a)]. low water: id=6273, wt=31 low water: id=6306, wt=30 low water: id=6673, wt=29 given #656 (A,wt=20): 317 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x) ' = z. [para(23(a,1),42(a,1))]. given #657 (F,wt=14): 1711 x v (y v (z v ((u ^ x) v z) ')) = 1. [para(217(a,1),101(a,1,2)),demod(89(2)),flip(a)]. low water: id=6670, wt=28 given #658 (F,wt=14): 1721 x v (y v ((z ^ (x ^ u)) v y) ') = 1. [para(24(a,1),219(a,1,2,2,1,1))]. given #659 (T,wt=14): 1735 x ^ (y ^ (z ^ (u ^ (x ^ u) '))) = 0. [para(15(a,1),232(a,1,2))]. given #660 (T,wt=14): 1737 x ^ (y ^ (z ^ ((x v u) ^ z) ')) = 0. [para(232(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #661 (A,wt=26): 318 x v (y v (z v u)) != 1 | (y v (x v z)) ^ u != 0 | (x v (y v z)) ' = u. [para(23(a,1),42(b,1,1)),demod(13(2))]. given #662 (F,wt=14): 1743 x ^ (y ^ (z ^ ((u v x) ^ z) ')) = 0. [para(232(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #663 (F,wt=14): 1781 x ^ (y ^ ((z v (x v u)) ^ y) ') = 0. [para(23(a,1),234(a,1,2,2,1,1))]. given #664 (T,wt=14): 1798 x v (y v (z v (u v (x ' v v)))) = 1. [para(13(a,1),236(a,1,2,2))]. given #665 (T,wt=14): 1799 x v (y v (z v ((x ^ u) ' v v))) = 1. [para(236(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #666 (A,wt=26): 319 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y) ' = z ^ u. [para(24(a,1),42(b,1))]. given #667 (F,wt=14): 1804 x v (y v (z v ((u ^ x) ' v v))) = 1. [para(236(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #668 (F,wt=14): 1809 x v (y v ((z ^ (x ^ u)) ' v v)) = 1. [para(24(a,1),238(a,1,2,2,1,1))]. given #669 (T,wt=14): 1818 x ^ (y ^ (z ^ (u ^ (x ' ^ v)))) = 0. [para(15(a,1),240(a,1,2,2))]. given #670 (T,wt=14): 1819 x ^ (y ^ (z ^ ((x v u) ' ^ v))) = 0. [para(240(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #671 (A,wt=22): 320 x v (y v z) != 1 | y v z != 0 | (y v z) ' = x v (y v z). [para(25(a,1),42(b,1)),demod(163(3),153(3))]. given #672 (F,wt=14): 1824 x ^ (y ^ (z ^ ((u v x) ' ^ v))) = 0. [para(240(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #673 (F,wt=14): 1833 x ^ (y ^ ((z v (x v u)) ' ^ v)) = 0. [para(23(a,1),242(a,1,2,2,1,1))]. given #674 (T,wt=14): 1843 x v (y v (z v (u v (v v x ')))) = 1. [para(13(a,1),253(a,1,2,2,2))]. given #675 (T,wt=14): 1844 x v (y v (z v (u v (x ^ v) '))) = 1. [para(253(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #676 (A,wt=19): 322 (x v y) ^ (y ' v z) != 0 | (x v y) ' = y ' v z. [para(81(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #677 (F,wt=14): 1849 x v (y v (z v (u v (v ^ x) '))) = 1. [para(253(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #678 (F,wt=14): 1854 x v (y v (z v (u ^ (x ^ v)) ')) = 1. [para(24(a,1),255(a,1,2,2,2,1))]. given #679 (T,wt=14): 1863 x ^ (y ^ (z ^ (u ^ (v ^ x ')))) = 0. [para(15(a,1),257(a,1,2,2,2))]. given #680 (T,wt=14): 1864 x ^ (y ^ (z ^ (u ^ (x v v) '))) = 0. [para(257(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #681 (A,wt=23): 323 x v (y v ((x v y) ' ^ z)) != 1 | (x v y) ' ^ z = (x v y) '. [para(84(a,1),42(b,1)),flip(c),xx(b)]. given #682 (F,wt=14): 1869 x ^ (y ^ (z ^ (u ^ (v v x) '))) = 0. [para(257(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #683 (F,wt=14): 1885 (x v (y v z)) ^ (y v (x v z)) ' = 0. [para(110(a,1),189(a,1,1,1)),demod(13(2),13(4))]. given #684 (T,wt=14): 1887 (x ^ y) ' v (((x v z) ^ y) v u) = 1. [para(203(a,1),110(a,1,1)),demod(69(8),1671(11))]. given #685 (T,wt=14): 1889 x v (y v (z v ((y v x) ' v u))) = 1. [para(110(a,1),238(a,1,2,2,1,1)),demod(13(6))]. given #686 (A,wt=19): 324 (x v y) ^ (z v y ') != 0 | (x v y) ' = z v y '. [para(90(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #687 (F,wt=14): 1890 x v (y v (z v (u v (y v x) '))) = 1. [para(110(a,1),255(a,1,2,2,2,1)),demod(13(6))]. given #688 (F,wt=14): 1894 x ^ (y ^ (z ^ (u v (x v v)) ')) = 0. [para(23(a,1),259(a,1,2,2,2,1))]. given #689 (T,wt=14): 1903 x ^ ((y v (z v (x v u))) ' ^ v) = 0. [para(13(a,1),263(a,1,2,1,1))]. given #690 (T,wt=14): 1909 x ^ (y ^ ((z v (u v x)) ' ^ v)) = 0. [para(190(a,1),263(a,1,2,1,1,2)),demod(15(6))]. given #691 (A,wt=15): 325 (x v y) ^ x ' != 0 | (x v y) ' = x '. [para(90(a,1),42(a,1)),xx(a)]. given #692 (F,wt=14): 1915 x ^ (y ^ (z v (u v (x v v))) ') = 0. [para(13(a,1),267(a,1,2,2,1))]. given #693 (F,wt=14): 1921 x ^ (y ^ (z ^ (u v (v v x)) ')) = 0. [para(190(a,1),267(a,1,2,2,1,2)),demod(15(6))]. given #694 (T,wt=14): 1928 x v ((x v y) ' v (z v (y v u))) = 1. [para(297(a,1),13(a,1,1)),demod(80(2),13(6),13(5)),flip(a)]. given #695 (T,wt=14): 1930 x v ((x v y) ' v (z v (u v y))) = 1. [para(13(a,1),297(a,1,2,2))]. given #696 (A,wt=23): 326 x v (y v (z ^ (x v y) ')) != 1 | z ^ (x v y) ' = (x v y) '. [para(93(a,1),42(b,1)),flip(c),xx(b)]. given #697 (F,wt=14): 1932 x v (y v ((x v z) ' v (u v z))) = 1. [para(297(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #698 (F,wt=14): 1934 x v (y v (x v (z ^ (y ^ u))) ') = 1. [para(86(a,1),297(a,1,2,2)),demod(12(5))]. given #699 (T,wt=14): 1935 x v (((x ^ y) v z) ' v (u v z)) = 1. [para(297(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #700 (T,wt=14): 1937 x v (y v (x v (z ^ (u ^ y))) ') = 1. [para(103(a,1),297(a,1,2,2)),demod(12(5))]. given #701 (A,wt=22): 327 x v y != 1 | (x v y) ^ z != 0 | (x v y) ' = (x v y) ^ z. [para(59(a,1),42(b,1)),demod(30(4))]. given #702 (F,wt=14): 1946 x v (((y ^ x) v z) ' v (u v z)) = 1. [para(297(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #703 (F,wt=14): 1952 x v ((y ^ z) v (x v (z ^ y)) ') = 1. [para(250(a,1),297(a,1,2,2)),demod(12(5))]. given #704 (T,wt=14): 1973 x v (y v (z v ((z v x) ' v u))) = 1. [para(111(a,1),197(a,1,2,1,1)),demod(13(6),13(5))]. given #705 (T,wt=14): 1974 x v (y v (z v (u ^ (z v x)) ')) = 1. [para(111(a,1),199(a,1,2,1,2)),demod(13(6),13(5))]. given #706 (A,wt=32): 328 x v (y v ((x v (y v z)) ^ u)) != 1 | (x v y) ^ u != 0 | (x v y) ' = (x v (y v z)) ^ u. [para(27(a,1),42(b,1)),demod(13(2),13(15))]. given #707 (F,wt=14): 1976 x v (y v (z v (u v (z v x) '))) = 1. [para(111(a,1),201(a,1,2,2,1)),demod(13(6),13(5))]. given #708 (F,wt=14): 1977 (x v (y v z)) ' ^ (u ^ (z v x)) = 0. [para(111(a,1),295(a,1,2,2))]. given #709 (T,wt=14): 1978 (x v y) ' v (z v (y v (u v x))) = 1. [para(111(a,1),589(a,1,1,1))]. given #710 (T,wt=14): 1979 (x v y) ^ (y v (z v (x v u))) ' = 0. [para(111(a,1),600(a,1,2)),demod(13(3),13(2),14(6))]. given #711 (A,wt=23): 329 x v (y v (x v (y v z)) ') != 1 | (x v (y v z)) ' = (x v y) '. [para(132(a,1),42(b,1)),demod(13(2),13(14)),flip(c),xx(b)]. given #712 (F,wt=14): 1980 (x v y) ^ (z v (y v (u v x))) ' = 0. [para(111(a,1),603(a,1,2)),demod(14(6))]. low water: id=6835, wt=27 given #713 (F,wt=14): 1992 x v ((y v x) ' v (z v (u v y))) = 1. [para(107(a,1),111(a,1,1)),demod(13(7),13(6),69(8),107(11))]. given #714 (T,wt=14): 1993 x v (y v ((z v x) ' v (u v z))) = 1. [para(123(a,1),111(a,1,1)),demod(13(7),13(6),69(8),123(11))]. given #715 (T,wt=14): 1995 x v (((y v x) ^ z) ' v (u v y)) = 1. [para(192(a,1),111(a,1,1)),demod(13(7),69(8),192(11))]. given #716 (A,wt=23): 330 x v (y v (z v (x v y)) ') != 1 | (z v (x v y)) ' = (x v y) '. [para(139(a,1),42(b,1)),flip(c),xx(b)]. given #717 (F,wt=14): 1996 x v ((y ^ (z v x)) ' v (u v z)) = 1. [para(198(a,1),111(a,1,1)),demod(13(7),69(8),198(11))]. given #718 (F,wt=14): 1999 x v (((y ^ z) v x) ' v (u v y)) = 1. [para(219(a,1),111(a,1,1)),demod(13(7),69(8),219(11))]. low water: id=7412, wt=26 given #719 (T,wt=14): 2006 x ^ ((x ^ y) ' ^ (z ^ (y ^ u))) = 0. [para(301(a,1),15(a,1,1)),demod(83(2),15(6),15(5)),flip(a)]. given #720 (T,wt=14): 2008 x ^ ((x ^ y) ' ^ (z ^ (u ^ y))) = 0. [para(15(a,1),301(a,1,2,2))]. given #721 (A,wt=22): 331 x v y != 1 | z ^ (x v y) != 0 | (x v y) ' = z ^ (x v y). [para(61(a,1),42(b,1)),demod(102(4))]. given #722 (F,wt=14): 2010 x ^ (y ^ ((x ^ z) ' ^ (u ^ z))) = 0. [para(301(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #723 (F,wt=14): 2013 x ^ (((x v y) ^ z) ' ^ (u ^ z)) = 0. [para(301(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #724 (T,wt=14): 2016 x ^ (y ^ (x ^ (z v (y v u))) ') = 0. [para(74(a,1),301(a,1,2,2)),demod(14(5))]. given #725 (T,wt=14): 2017 x ^ (y ^ (x ^ (z v (u v y))) ') = 0. [para(95(a,1),301(a,1,2,2)),demod(14(5))]. given #726 (A,wt=24): 332 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y) ' = y v z. [para(65(a,1),42(a,1,2))]. given #727 (F,wt=14): 2024 x ^ (((y v x) ^ z) ' ^ (u ^ z)) = 0. [para(301(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #728 (F,wt=14): 2028 x ^ ((y v z) ^ (x ^ (z v y)) ') = 0. [para(164(a,1),301(a,1,2,2)),demod(14(5))]. given #729 (T,wt=14): 2046 x ^ (y ^ (z v (u v (v v x))) ') = 0. [para(190(a,1),305(a,1,2,1,2,2)),demod(15(6))]. given #730 (T,wt=14): 2050 x ^ ((y v (z v (u v x))) ' ^ v) = 0. [para(357(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #731 (A,wt=36): 333 x v (y v (z ^ (((x v y) ^ z) v u))) != 1 | (x v y) ^ z != 0 | (x v y) ' = z ^ (((x v y) ^ z) v u). [para(28(a,1),42(b,1))]. given #732 (F,wt=14): 2064 x ^ (y ^ (z v (u v (y ^ x))) ') = 0. [para(250(a,1),357(a,1,2,1,2,2)),demod(15(6))]. given #733 (F,wt=14): 2081 x ^ (y ^ ((z v (y ^ x)) ' ^ u)) = 0. [para(250(a,1),358(a,1,2,1,1,2)),demod(15(6))]. given #734 (T,wt=14): 2128 x ^ (y ^ (z ^ (u v (y ^ x)) ')) = 0. [para(250(a,1),362(a,1,2,2,1,2)),demod(15(6))]. given #735 (T,wt=14): 2143 x ^ (y ^ (z ^ ((y ^ x) ' ^ u))) = 0. [para(250(a,1),370(a,1,2,2,1,1)),demod(15(6))]. given #736 (A,wt=24): 334 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z) ' = y v z. [para(67(a,1),42(a,1,2))]. given #737 (F,wt=14): 2158 x ^ (y ^ (z ^ (u ^ (y ^ x) '))) = 0. [para(250(a,1),374(a,1,2,2,2,1)),demod(15(6))]. given #738 (F,wt=14): 2165 x v ((y ^ (z ^ (x ^ u))) ' v v) = 1. [para(15(a,1),383(a,1,2,1,1))]. given #739 (T,wt=14): 2170 x v (y v ((z ^ (u ^ x)) ' v v)) = 1. [para(152(a,1),383(a,1,2,1,1,2)),demod(13(6))]. given #740 (T,wt=14): 2173 x v (y v ((z ^ (y v x)) ' v u)) = 1. [para(110(a,1),383(a,1,2,1,1,2)),demod(13(6))]. given #741 (A,wt=28): 339 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y) ' = (y ^ u) v z. [para(29(a,1),42(a,1,2))]. given #742 (F,wt=14): 2174 (x ^ (y ^ z)) ' v (u v (v v y)) = 1. [para(383(a,1),111(a,1,1)),demod(13(7),69(8),383(11))]. given #743 (F,wt=14): 2210 ((x ^ y) v z) ^ (x v (z v u)) ' = 0. [para(189(a,1),113(a,1,2)),demod(14(4),83(4)),flip(a)]. given #744 (T,wt=14): 2229 x v (y v (z ^ (u ^ (x ^ v))) ') = 1. [para(15(a,1),412(a,1,2,2,1))]. given #745 (T,wt=14): 2234 x v (y v (z v (u ^ (v ^ x)) ')) = 1. [para(152(a,1),412(a,1,2,2,1,2)),demod(13(6))]. given #746 (A,wt=19): 340 (x v y) ^ (y ^ z) ' != 0 | (x v y) ' = (y ^ z) '. [para(183(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #747 (F,wt=14): 2236 x v (y v (z v (u ^ (y v x)) ')) = 1. [para(110(a,1),412(a,1,2,2,1,2)),demod(13(6))]. given #748 (F,wt=14): 2244 x v (y v (z ^ (u ^ (v ^ x))) ') = 1. [para(152(a,1),418(a,1,2,1,2,2)),demod(13(6))]. given #749 (T,wt=14): 2246 x v (y v (z ^ (u ^ (y v x))) ') = 1. [para(110(a,1),418(a,1,2,1,2,2)),demod(13(6))]. given #750 (T,wt=14): 2248 x v ((y ^ (z ^ (u ^ x))) ' v v) = 1. [para(15(a,1),423(a,1,2,1,1,2))]. given #751 (A,wt=19): 341 (x v y) ^ (z ^ y) ' != 0 | (x v y) ' = (z ^ y) '. [para(193(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #752 (F,wt=14): 2265 (x ^ (y ^ z)) ' v (u v (v v z)) = 1. [para(423(a,1),111(a,1,1)),demod(13(7),69(8),423(11))]. given #753 (F,wt=14): 2301 (x ^ y) ' v (z v (u v (x v v))) = 1. [para(586(a,1),115(a,1,1,2)),demod(89(2),13(5),69(8),614(11))]. given #754 (T,wt=14): 2302 (x ^ y) ' v (z v (u v (y v v))) = 1. [para(589(a,1),115(a,1,1,2)),demod(89(2),13(5),69(8),646(11))]. given #755 (T,wt=14): 2308 (x ^ y) v (z v ((y ^ x) ' v u)) = 1. [para(1219(a,1),115(a,1,1,2)),demod(89(2),69(8),1232(11))]. given #756 (A,wt=23): 343 (x v y) ^ (z v (y v z) ') != 0 | (x v y) ' = z v (y v z) '. [para(36(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #757 (F,wt=14): 2315 x v (y v (((y v x) ^ z) ' v u)) = 1. [para(192(a,1),115(a,1,1)),demod(69(8),1610(11))]. given #758 (F,wt=14): 2321 x v (y v (((y ^ z) v x) ' v u)) = 1. [para(219(a,1),115(a,1,1)),demod(69(8),1719(11))]. given #759 (T,wt=14): 2395 x v (y v ((y v (x ^ z)) ' v u)) = 1. [para(508(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #760 (T,wt=14): 2400 x v (y v ((y v (z ^ x)) ' v u)) = 1. [para(508(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #761 (A,wt=32): 344 x v (y v z) != 1 | (x v y) ^ (z v ((y v z) ^ u)) != 0 | (x v y) ' = z v ((y v z) ^ u). [para(30(a,1),42(a,1,2))]. given #762 (F,wt=14): 2437 x v (y v (z v (u v (u v x) '))) = 1. [para(13(a,1),512(a,1,2))]. given #763 (F,wt=14): 2439 x v (y v (z v (z v (x ^ u)) ')) = 1. [para(512(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #764 (T,wt=14): 2444 x v (y v (z v (z v (u ^ x)) ')) = 1. [para(512(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #765 (T,wt=14): 2452 x v (y v (y v (z ^ (x ^ u))) ') = 1. [para(24(a,1),514(a,1,2,2,1,2))]. given #766 (A,wt=27): 345 x v (y v (z ^ ((x v y) ^ z) ')) != 1 | z ^ ((x v y) ^ z) ' = (x v y) '. [para(39(a,1),42(b,1)),flip(c),xx(b)]. given #767 (F,wt=14): 2460 x v (y v (z v (z v (y v x)) ')) = 1. [para(110(a,1),514(a,1,2,2,1,2)),demod(13(6))]. given #768 (F,wt=14): 2461 x v ((x v (y ^ z)) ' v (u v y)) = 1. [para(514(a,1),111(a,1,1)),demod(13(7),69(8),514(11))]. given #769 (T,wt=14): 2463 x v (y v ((x v (y ^ z)) ' v u)) = 1. [para(514(a,1),115(a,1,1)),demod(69(8),682(11))]. given #770 (T,wt=14): 2469 x ^ (y ^ (z ^ ((z ^ x) ' ^ u))) = 0. [para(518(a,1),24(a,1,2)),demod(92(2)),flip(a)]. low water: id=7492, wt=25 given #771 (A,wt=23): 346 (x v y) ^ (z v (y ' v u)) != 0 | (x v y) ' = z v (y ' v u). [para(109(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #772 (F,wt=14): 2471 x ^ (y ^ ((y ^ (x v z)) ' ^ u)) = 0. [para(518(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #773 (F,wt=14): 2476 x ^ (y ^ ((y ^ (z v x)) ' ^ u)) = 0. [para(518(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #774 (T,wt=14): 2480 (x v y) ' ^ (((x ^ z) v y) ^ u) = 0. [para(189(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #775 (T,wt=14): 2487 x ^ (y ^ (z ^ (u ^ (u ^ x) '))) = 0. [para(15(a,1),522(a,1,2))]. given #776 (A,wt=19): 347 (x v y) ^ (x ' v z) != 0 | (x v y) ' = x ' v z. [para(109(a,1),42(a,1)),xx(a)]. given #777 (F,wt=14): 2489 x ^ (y ^ (z ^ (z ^ (x v u)) ')) = 0. [para(522(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #778 (F,wt=14): 2494 x ^ (y ^ (z ^ (z ^ (u v x)) ')) = 0. [para(522(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #779 (T,wt=14): 2498 x ^ ((y ^ x) ' ^ (z ^ (u ^ y))) = 0. [para(120(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6),15(5))]. given #780 (T,wt=14): 2499 x ^ (y ^ ((z ^ x) ' ^ (u ^ z))) = 0. [para(126(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6),15(5))]. given #781 (A,wt=27): 348 x v (y v (z ^ ((x v y) ' ^ u))) != 1 | z ^ ((x v y) ' ^ u) = (x v y) '. [para(122(a,1),42(b,1)),flip(c),xx(b)]. given #782 (F,wt=14): 2500 x ^ (((y ^ x) v z) ' ^ (u ^ y)) = 0. [para(141(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #783 (F,wt=14): 2501 x ^ ((y v (z ^ x)) ' ^ (u ^ z)) = 0. [para(146(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #784 (T,wt=14): 2502 x ^ (((y v z) ^ x) ' ^ (u ^ y)) = 0. [para(234(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #785 (T,wt=14): 2503 (x v (y v z)) ' ^ (u ^ (v ^ y)) = 0. [para(263(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #786 (A,wt=23): 350 (x v y) ^ (z v (u v y ')) != 0 | (x v y) ' = z v (u v y '). [para(124(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #787 (F,wt=14): 2504 (x ^ y) ' ^ (z ^ (y ^ (u ^ x))) = 0. [para(301(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6),15(5))]. given #788 (F,wt=14): 2505 (x v (y v z)) ' ^ (u ^ (v ^ z)) = 0. [para(358(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #789 (T,wt=14): 2548 x ^ (y ^ (y ^ (z v (x v u))) ') = 0. [para(23(a,1),524(a,1,2,2,1,2))]. given #790 (T,wt=14): 2557 x ^ ((x ^ (y v z)) ' ^ (u ^ y)) = 0. [para(524(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #791 (A,wt=19): 351 (x v y) ^ (z v x ') != 0 | (x v y) ' = z v x '. [para(124(a,1),42(a,1)),xx(a)]. given #792 (F,wt=14): 2563 (x ^ y) ' v (z v (u v (v v x))) = 1. [para(190(a,1),529(a,1,2,2,2))]. given #793 (F,wt=14): 2564 (x ^ y) ' v (z v (u v (v v y))) = 1. [para(821(a,1),529(a,1,2,2,2))]. given #794 (T,wt=14): 2571 (x v y) ' ^ (z ^ (u ^ (v ^ x))) = 0. [para(152(a,1),579(a,1,2,2,2))]. given #795 (T,wt=14): 2573 (x v y) ' ^ (z ^ (u ^ (v ^ y))) = 0. [para(768(a,1),579(a,1,2,2,2))]. given #796 (A,wt=27): 352 x v (y v (z ^ (u ^ (x v y) '))) != 1 | z ^ (u ^ (x v y) ') = (x v y) '. [para(127(a,1),42(b,1)),flip(c),xx(b)]. given #797 (F,wt=14): 2575 (x v y) ' ^ (z ^ (u ^ (y v x))) = 0. [para(110(a,1),579(a,1,2,2,2))]. given #798 (F,wt=14): 2591 (x ^ y) ' v (z v (u v (y ^ x))) = 1. [para(250(a,1),585(a,1,2,2,2))]. given #799 (T,wt=14): 2607 (x ^ (y ^ z)) ' v (u v (y v v)) = 1. [para(590(a,1),13(a,1,1)),demod(80(2),13(6)),flip(a)]. given #800 (T,wt=14): 2618 (x ^ (y ^ z)) ' v (u v (z v v)) = 1. [para(152(a,1),590(a,1,1,1,2))]. given #801 (A,wt=27): 353 x v (y v ((x v (y v z)) ' ^ u)) != 1 | (x v (y v z)) ' ^ u = (x v y) '. [para(137(a,1),42(b,1)),demod(13(2),13(15)),flip(c),xx(b)]. given #802 (F,wt=14): 2620 (x ^ y) v (z ^ (y ^ (x ^ u))) ' = 1. [para(250(a,1),590(a,1,2)),demod(15(2),12(6))]. given #803 (F,wt=14): 2624 (x ^ (y v z)) ' v (u v (z v y)) = 1. [para(110(a,1),590(a,1,1,1,2))]. given #804 (T,wt=14): 2648 (x ^ y) v (z ^ (u ^ (y ^ x))) ' = 1. [para(250(a,1),592(a,1,2)),demod(12(6))]. given #805 (T,wt=14): 2684 (x v (y v z)) ' ^ (u ^ (y ^ v)) = 0. [para(607(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #806 (A,wt=27): 354 x v (y v (z ^ (x v (y v u)) ')) != 1 | z ^ (x v (y v u)) ' = (x v y) '. [para(138(a,1),42(b,1)),demod(13(2),13(15)),flip(c),xx(b)]. given #807 (F,wt=14): 2694 (x v y) ^ (z v (y v (x v u))) ' = 0. [para(164(a,1),607(a,1,2)),demod(13(2),14(6))]. given #808 (F,wt=14): 2696 (x v (y v z)) ' ^ (u ^ (z ^ v)) = 0. [para(190(a,1),607(a,1,1,1,2))]. given #809 (T,wt=14): 2711 (x v y) ' ^ (z ^ (u ^ (y ^ v))) = 0. [para(86(a,1),608(a,1,1,1,2))]. given #810 (T,wt=14): 2723 (x v y) ^ (z v (u v (y v x))) ' = 0. [para(164(a,1),608(a,1,2)),demod(14(6))]. given #811 (A,wt=19): 355 (x v y ') ^ (z v y) != 0 | (x v y ') ' = z v y. [para(290(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #812 (F,wt=14): 2729 (x v (y ^ z)) ' ^ (u ^ (z ^ y)) = 0. [para(250(a,1),608(a,1,1,1,2))]. given #813 (F,wt=14): 2746 (x v y) ' v (z v (y v (x v u))) = 1. [para(110(a,1),613(a,1,1,1)),demod(13(4))]. given #814 (T,wt=14): 2759 (x ^ (y ^ z)) ' v (u v (y ^ x)) = 1. [para(250(a,1),614(a,1,2,2)),demod(15(2))]. given #815 (T,wt=14): 2763 (x v y) ' v (z v (u v (y v x))) = 1. [para(110(a,1),614(a,1,1,1))]. given #816 (A,wt=27): 356 x v (y v (z v (x v (y v u))) ') != 1 | (z v (x v (y v u))) ' = (x v y) '. [para(143(a,1),42(b,1)),demod(13(2),13(15)),flip(c),xx(b)]. given #817 (F,wt=14): 2801 (x ^ (y ^ z)) ' v (u v (z ^ y)) = 1. [para(250(a,1),646(a,1,2,2))]. given #818 (F,wt=14): 2812 (x v y) ' ^ (z ^ (u ^ (x ^ v))) = 0. [para(15(a,1),656(a,1,2))]. given #819 (T,wt=14): 2820 (x v (y v z)) ' ^ (u ^ (y v x)) = 0. [para(110(a,1),656(a,1,2,2)),demod(13(2))]. given #820 (T,wt=14): 2853 (x ^ y) ' ^ (z ^ (y ^ (x ^ u))) = 0. [para(250(a,1),664(a,1,1,1)),demod(15(4))]. given #821 (A,wt=19): 360 x v (y v (z v x)) ' != 1 | (y v (z v x)) ' = x '. [para(144(a,1),20(b,1)),flip(c),xx(b)]. given #822 (F,wt=14): 2857 (x v (y v z)) ' ^ (u ^ (z v y)) = 0. [para(110(a,1),664(a,1,2,2))]. given #823 (F,wt=14): 2878 (x ^ y) ' ^ (z ^ (u ^ (y ^ x))) = 0. [para(250(a,1),665(a,1,1,1))]. given #824 (T,wt=14): 2899 (x v (y ^ z)) ^ (x v (z v u)) ' = 0. [para(152(a,1),679(a,1,1,2))]. given #825 (T,wt=14): 2906 (x v y) ' ^ ((x v (y ^ z)) ^ u) = 0. [para(679(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #826 (A,wt=16): 364 (x v ((y v x) ^ z)) ^ (u v (y v x)) ' = 0. [para(30(a,1),144(a,1,2,1,2))]. given #827 (F,wt=14): 2910 x v (y v (z v (x v (z ^ u)) ')) = 1. [para(682(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #828 (F,wt=14): 2911 x v (y v ((x ^ z) v (y ^ u)) ') = 1. [para(682(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #829 (T,wt=14): 2916 x v (y v ((z ^ x) v (y ^ u)) ') = 1. [para(682(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #830 (T,wt=14): 2917 x v (y v (z v (x v (u ^ y)) ')) = 1. [para(152(a,1),682(a,1,2,2,1,2)),demod(13(5))]. given #831 (A,wt=27): 366 x v (y v (z v (u v (x v y))) ') != 1 | (z v (u v (x v y))) ' = (x v y) '. [para(144(a,1),42(b,1)),flip(c),xx(b)]. given #832 (F,wt=14): 2918 x v (y v (z v (x v (u ^ z)) ')) = 1. [para(768(a,1),682(a,1,2,2,1,2)),demod(13(5))]. given #833 (F,wt=14): 2920 x v ((y v (x ^ z)) ' v (u v y)) = 1. [para(682(a,1),111(a,1,1)),demod(13(7),69(8),682(11))]. given #834 (T,wt=14): 2937 (x ^ (y v z)) v (x ^ (z ^ u)) ' = 1. [para(190(a,1),748(a,1,1,2))]. given #835 (T,wt=14): 2942 (x ^ y) ' v ((x ^ (y v z)) v u) = 1. [para(748(a,1),110(a,1,1)),demod(69(8),2925(11))]. given #836 (A,wt=19): 368 x v ((y v x) ' ^ z) != 1 | (y v x) ' ^ z = x '. [para(145(a,1),20(b,1)),flip(c),xx(b)]. given #837 (F,wt=14): 2957 x ^ (y ^ ((x ^ (y v z)) ' ^ u)) = 0. [para(750(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #838 (F,wt=14): 2959 x ^ (y ^ (z ^ (x ^ (z v u)) ')) = 0. [para(750(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #839 (T,wt=14): 2960 x ^ (y ^ ((x v z) ^ (y v u)) ') = 0. [para(750(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #840 (T,wt=14): 2965 x ^ (y ^ ((z v x) ^ (y v u)) ') = 0. [para(750(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #841 (A,wt=16): 372 (x v ((y v x) ^ z)) ^ ((y v x) ' ^ u) = 0. [para(30(a,1),145(a,1,2,1,1))]. given #842 (F,wt=14): 2966 x ^ (y ^ (z ^ (x ^ (u v y)) ')) = 0. [para(190(a,1),750(a,1,2,2,1,2)),demod(15(5))]. given #843 (F,wt=14): 2968 x ^ (y ^ (z ^ (x ^ (u v z)) ')) = 0. [para(821(a,1),750(a,1,2,2,1,2)),demod(15(5))]. given #844 (T,wt=14): 2971 x ^ ((y ^ (x v z)) ' ^ (u ^ y)) = 0. [para(750(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #845 (T,wt=14): 2974 ((x v (y v z)) ^ u) v (z ^ u) ' = 1. [para(13(a,1),771(a,1,1,1))]. given #846 (A,wt=27): 373 x v (y v ((z v (x v y)) ' ^ u)) != 1 | (z v (x v y)) ' ^ u = (x v y) '. [para(145(a,1),42(b,1)),flip(c),xx(b)]. given #847 (F,wt=14): 2986 ((x v y) ^ (z v (y v u))) v y ' = 1. [para(74(a,1),771(a,1,2,1))]. given #848 (F,wt=14): 2987 ((x v y) ^ (z v (u v y))) v y ' = 1. [para(95(a,1),771(a,1,2,1))]. given #849 (T,wt=14): 3002 (x ^ (y ^ z)) v (y ^ (x ^ z)) ' = 1. [para(250(a,1),771(a,1,1,1)),demod(15(2),15(4))]. given #850 (T,wt=14): 3007 (x ^ y) ' v (((z v x) ^ y) v u) = 1. [para(771(a,1),110(a,1,1)),demod(69(8),2973(11))]. given #851 (A,wt=19): 375 x v (y ^ (z v x) ') != 1 | y ^ (z v x) ' = x '. [para(149(a,1),20(b,1)),flip(c),xx(b)]. given #852 (F,wt=14): 3016 x ^ (y ^ ((z v (u v x)) ^ y) ') = 0. [para(13(a,1),775(a,1,2,2,1,1))]. given #853 (F,wt=14): 3041 x ^ (((y v z) ^ x) ' ^ (u ^ z)) = 0. [para(775(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #854 (T,wt=14): 3043 x ^ (y ^ (y ^ (z v (u v x))) ') = 0. [para(13(a,1),782(a,1,2,2,1,2))]. given #855 (T,wt=14): 3059 x ^ (y ^ (z ^ (z ^ (y ^ x)) ')) = 0. [para(250(a,1),782(a,1,2,2,1,2)),demod(15(6))]. given #856 (A,wt=16): 378 (x v ((y v x) ^ z)) ^ (u ^ (y v x) ') = 0. [para(30(a,1),149(a,1,2,2,1))]. given #857 (F,wt=14): 3066 x ^ ((x ^ (y v z)) ' ^ (u ^ z)) = 0. [para(782(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #858 (F,wt=14): 3120 x ^ (y ^ (x ^ ((x ^ y) v z)) ') = 0. [para(131(a,1),232(a,1))]. given #859 (T,wt=14): 3196 (x ^ y) ' v ((x ^ (z v y)) v u) = 1. [para(796(a,1),110(a,1,1)),demod(69(8),3172(11))]. given #860 (T,wt=14): 3206 x ^ (y ^ ((x ^ (z v y)) ' ^ u)) = 0. [para(800(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #861 (A,wt=27): 379 x v (y v (z ^ (u v (x v y)) ')) != 1 | z ^ (u v (x v y)) ' = (x v y) '. [para(149(a,1),42(b,1)),flip(c),xx(b)]. given #862 (F,wt=14): 3208 x ^ (y ^ ((x v z) ^ (u v y)) ') = 0. [para(800(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #863 (F,wt=14): 3216 x ^ (y ^ ((z v x) ^ (u v y)) ') = 0. [para(800(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #864 (T,wt=14): 3226 x ^ ((y ^ (z v x)) ' ^ (u ^ y)) = 0. [para(800(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6),15(6))]. given #865 (T,wt=14): 3232 ((x ^ (y ^ z)) v u) ^ (z v u) ' = 0. [para(15(a,1),819(a,1,1,1))]. given #866 (A,wt=19): 382 x ^ ((x ^ y) ' v z) != 0 | (x ^ y) ' v z = x '. [para(187(a,1),20(a,1)),flip(c),xx(a)]. given #867 (F,wt=14): 3241 ((x ^ y) v (z ^ (y ^ u))) ^ y ' = 0. [para(86(a,1),819(a,1,2,1))]. given #868 (F,wt=14): 3243 ((x ^ y) v (z ^ (u ^ y))) ^ y ' = 0. [para(103(a,1),819(a,1,2,1))]. given #869 (T,wt=14): 3264 ((x ^ y) v z) ^ (y v (z v u)) ' = 0. [para(819(a,1),113(a,1,2)),demod(14(4),83(4)),flip(a)]. given #870 (T,wt=14): 3267 (x v y) ' ^ (((z ^ x) v y) ^ u) = 0. [para(819(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #871 (A,wt=19): 384 x ^ ((x ^ y) ' v z) != 0 | ((x ^ y) ' v z) ' = x. [para(187(a,1),41(a,1)),demod(14(7)),xx(a)]. given #872 (F,wt=14): 3273 x v (y v ((z ^ (u ^ x)) v y) ') = 1. [para(15(a,1),824(a,1,2,2,1,1))]. given #873 (F,wt=14): 3293 x v (((y ^ z) v x) ' v (u v z)) = 1. [para(824(a,1),111(a,1,1)),demod(13(7),69(8),824(11))]. given #874 (T,wt=14): 3297 x v (y v (((z ^ y) v x) ' v u)) = 1. [para(824(a,1),115(a,1,1)),demod(69(8),2401(11))]. given #875 (T,wt=14): 3343 x v (y v (y v (z ^ (u ^ x))) ') = 1. [para(15(a,1),832(a,1,2,2,1,2))]. given #876 (A,wt=23): 385 (x v y) ^ ((y ^ z) ' v u) != 0 | (x v y) ' = (y ^ z) ' v u. [para(187(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #877 (F,wt=14): 3360 x v ((x v (y ^ z)) ' v (u v z)) = 1. [para(832(a,1),111(a,1,1)),demod(13(7),69(8),832(11))]. given #878 (F,wt=14): 3365 x v (y v ((x v (z ^ y)) ' v u)) = 1. [para(832(a,1),115(a,1,1)),demod(69(8),934(11))]. given #879 (T,wt=14): 3399 (x v y) ' ^ ((x v (z ^ y)) ^ u) = 0. [para(930(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #880 (T,wt=14): 3406 x v (y v ((x ^ z) v (u ^ y)) ') = 1. [para(934(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #881 (A,wt=20): 386 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x ' = y ^ z. [para(15(a,1),43(b,1))]. given #882 (F,wt=14): 3414 x v (y v ((z ^ x) v (u ^ y)) ') = 1. [para(934(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #883 (F,wt=14): 3420 x v ((y v (z ^ x)) ' v (u v y)) = 1. [para(934(a,1),111(a,1,1)),demod(13(7),69(8),934(11))]. given #884 (T,wt=14): 3432 x v (y v (z ^ (y v (x ^ u))) ') = 1. [para(974(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #885 (T,wt=14): 3437 x v (y v (z ^ (y v (u ^ x))) ') = 1. [para(974(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #886 (A,wt=20): 387 x v (y v z) != 1 | (x v z) ^ y != 0 | y ' = x v z. [para(23(a,1),43(a,1))]. given #887 (F,wt=14): 3474 x ^ ((x v y) ^ (z v (x v u))) ' = 0. [para(134(a,1),234(a,1))]. given #888 (F,wt=14): 3490 x ^ (y ^ ((z v (y v u)) ^ x) ') = 0. [para(134(a,1),522(a,1,2))]. given #889 (T,wt=14): 3493 x ^ ((y v (x v z)) ^ (x v u)) ' = 0. [para(134(a,1),524(a,1))]. given #890 (T,wt=14): 3506 x ^ ((y v x) ^ (z v (x v u))) ' = 0. [para(134(a,1),775(a,1))]. given #891 (A,wt=20): 388 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z. [para(24(a,1),43(b,1))]. given #892 (F,wt=14): 3508 x ^ ((y v (x v z)) ^ (u v x)) ' = 0. [para(134(a,1),782(a,1))]. given #893 (F,wt=14): 3524 x v (y v (z v (y v (x ^ u)) ')) = 1. [para(976(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #894 (T,wt=14): 3529 x v (y v (z v (y v (u ^ x)) ')) = 1. [para(976(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #895 (T,wt=14): 3534 (x v y) ' ^ (z ^ ((y v x) ^ u)) = 0. [para(977(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #896 (A,wt=22): 389 x v (y v z) != 1 | x v y != 0 | (x v (y v z)) ' = x v y. [para(26(a,1),43(b,1)),demod(12(4),23(4),23(3),13(2),153(3),65(3))]. given #897 (F,wt=14): 3558 (x v y) ^ ((y v (x v z)) ' ^ u) = 0. [para(979(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #898 (F,wt=14): 3561 (x v y) ^ (z ^ (y v (x v u)) ') = 0. [para(979(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #899 (T,wt=14): 3564 ((x ^ y) v z) ^ (z v (u v x)) ' = 0. [para(190(a,1),979(a,1,2,1,2))]. given #900 (T,wt=14): 3566 ((x ^ y) v z) ^ (z v (u v y)) ' = 0. [para(821(a,1),979(a,1,2,1,2))]. given #901 (A,wt=15): 390 x v (x ' ^ y) != 1 | (x ' ^ y) ' = x. [para(84(a,1),43(b,1)),demod(12(3)),xx(b)]. given #902 (F,wt=14): 3589 x ^ (y ^ (z ^ (x ^ (y v u)) ')) = 0. [para(126(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #903 (F,wt=14): 3603 x ^ (y ^ (((y v z) ^ x) ' ^ u)) = 0. [para(518(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #904 (T,wt=14): 3605 x ^ (y ^ ((y v z) ^ (x v u)) ') = 0. [para(524(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #905 (T,wt=14): 3616 x ^ (y ^ ((y v z) ^ (u v x)) ') = 0. [para(782(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #906 (A,wt=15): 391 x v (y ^ x ') != 1 | (y ^ x ') ' = x. [para(93(a,1),43(b,1)),demod(12(3)),xx(b)]. given #907 (F,wt=14): 3629 (x v y) ^ ((z v (y v x)) ' ^ u) = 0. [para(980(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #908 (F,wt=14): 3632 (x v y) ^ (z ^ (u v (y v x)) ') = 0. [para(980(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #909 (T,wt=14): 3642 (x v y) ^ (z ^ ((y v x) ' ^ u)) = 0. [para(984(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #910 (T,wt=14): 3647 (x v y) ^ ((y v (z v x)) ' ^ u) = 0. [para(984(a,1),113(a,1,2)),demod(14(3),83(3),13(4)),flip(a)]. given #911 (A,wt=22): 392 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z) ' = x. [para(27(a,1),43(b,1)),demod(12(3))]. given #912 (F,wt=14): 3651 (x v y) ^ (z ^ (u ^ (y v x) ')) = 0. [para(15(a,1),986(a,1,2))]. given #913 (F,wt=14): 3658 (x v y) ^ (z ^ (y v (u v x)) ') = 0. [para(986(a,1),113(a,1,2)),demod(14(3),83(3),13(4)),flip(a)]. given #914 (T,wt=14): 3664 x ^ (y ^ (z ^ (u v (z ^ x)) ')) = 0. [para(1221(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #915 (T,wt=14): 3666 x ^ (y ^ (z v (y ^ (x v u))) ') = 0. [para(1221(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #916 (A,wt=26): 395 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z)) ' = x. [para(28(a,1),43(b,1)),demod(12(4))]. given #917 (F,wt=14): 3671 x ^ (y ^ (z v (y ^ (u v x))) ') = 0. [para(1221(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #918 (F,wt=14): 3678 x ^ (y ^ (z v ((y v u) ^ x)) ') = 0. [para(1221(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #919 (T,wt=14): 3753 x ^ (y ^ (z ^ (u ^ (z ^ x) '))) = 0. [para(1222(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #920 (T,wt=14): 3755 x ^ (y ^ (z ^ (y ^ (x v u)) ')) = 0. [para(1222(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #921 (A,wt=18): 396 x v (y v z) != 1 | 0 != y | (x v (y v z)) ' = y. [para(74(a,1),43(b,1)),demod(12(3),153(3)),flip(b)]. given #922 (F,wt=14): 3760 x ^ (y ^ (z ^ (y ^ (u v x)) ')) = 0. [para(1222(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #923 (F,wt=14): 3767 x ^ (y ^ (z ^ ((y v u) ^ x) ')) = 0. [para(1222(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #924 (T,wt=14): 3769 (x ^ y) ' v (z v ((y ^ x) v u)) = 1. [para(1224(a,1),13(a,1,1)),demod(80(2),13(6)),flip(a)]. given #925 (T,wt=14): 3781 (x ^ y) v ((y ^ (x ^ z)) ' v u) = 1. [para(1225(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #926 (A,wt=18): 397 x v (y v z) != 1 | 0 != z | (x v (y v z)) ' = z. [para(95(a,1),43(b,1)),demod(12(3),163(3)),flip(b)]. given #927 (F,wt=14): 3785 (x ^ y) v (z v (y ^ (x ^ u)) ') = 1. [para(1225(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #928 (F,wt=14): 3787 (x ^ y) v (y ^ (z ^ (x ^ u))) ' = 1. [para(24(a,1),1225(a,1,2,1,2))]. given #929 (T,wt=14): 3790 ((x v y) ^ z) v (z ^ (u ^ x)) ' = 1. [para(152(a,1),1225(a,1,2,1,2))]. given #930 (T,wt=14): 3791 ((x v y) ^ z) v (z ^ (u ^ y)) ' = 1. [para(768(a,1),1225(a,1,2,1,2))]. given #931 (A,wt=19): 398 x v (y ^ (x ^ y) ') != 1 | (y ^ (x ^ y) ') ' = x. [para(39(a,1),43(b,1)),demod(12(4)),xx(b)]. given #932 (F,wt=14): 3794 ((x v y) ^ z) v (z ^ (y v x)) ' = 1. [para(110(a,1),1225(a,1,2,1,2))]. low water: id=7860, wt=24 given #933 (F,wt=14): 3800 (x ^ y) v ((z ^ (y ^ x)) ' v u) = 1. [para(1226(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #934 (T,wt=14): 3804 (x ^ y) v (z v (u ^ (y ^ x)) ') = 1. [para(1226(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #935 (T,wt=14): 3812 (x ^ (y v (z v u))) v (z ^ x) ' = 1. [para(134(a,1),1226(a,1,2,1))]. given #936 (A,wt=19): 399 x v (y ^ (x ' ^ z)) != 1 | (y ^ (x ' ^ z)) ' = x. [para(122(a,1),43(b,1)),demod(12(4)),xx(b)]. given #937 (F,wt=14): 3835 (x ^ y) v (z v (u v (y ^ x) ')) = 1. [para(13(a,1),1232(a,1,2))]. given #938 (F,wt=14): 3845 (x v y) ^ (y v (z v (u v x))) ' = 0. [para(13(a,1),1476(a,1,2,1,2))]. given #939 (T,wt=14): 3848 ((x ^ (y ^ z)) v u) ^ (u v y) ' = 0. [para(86(a,1),1476(a,1,2,1,2))]. given #940 (T,wt=14): 3850 ((x ^ (y ^ z)) v u) ^ (u v z) ' = 0. [para(103(a,1),1476(a,1,2,1,2))]. given #941 (A,wt=19): 400 x v (y ^ (z ^ x ')) != 1 | (y ^ (z ^ x ')) ' = x. [para(127(a,1),43(b,1)),demod(12(4)),xx(b)]. given #942 (F,wt=10): 11954 x ^ y != 1 | y ^ x = 1. [para(243(a,1),400(a,1)),demod(229(7),82(5)),flip(b)]. given #943 (F,wt=10): 11957 x v y != 1 | y v x = 1. [para(164(a,1),11954(a,1)),demod(164(6))]. given #944 (T,wt=14): 3861 ((x ^ y) v z) ^ (z v (y ^ x)) ' = 0. [para(250(a,1),1476(a,1,2,1,2))]. given #945 (T,wt=14): 3878 ((x ^ y) v z) ^ ((z v x) ' ^ u) = 0. [para(1483(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #946 (A,wt=19): 401 x v ((x v y) ' ^ z) != 1 | ((x v y) ' ^ z) ' = x. [para(137(a,1),43(b,1)),demod(12(4)),xx(b)]. given #947 (F,wt=14): 3882 ((x ^ y) v z) ^ (u ^ (z v x) ') = 0. [para(1483(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #948 (F,wt=14): 3886 ((x ^ y) v z) ^ (z v (y v u)) ' = 0. [para(152(a,1),1483(a,1,1,1))]. given #949 (T,wt=14): 3891 (x v (y v z)) ^ (z v (y v x)) ' = 0. [para(110(a,1),1483(a,1,1,1)),demod(13(2))]. given #950 (T,wt=14): 3894 (x v y) ' ^ (((y ^ z) v x) ^ u) = 0. [para(1483(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #951 (A,wt=19): 402 x v (y ^ (x v z) ') != 1 | (y ^ (x v z) ') ' = x. [para(138(a,1),43(b,1)),demod(12(4)),xx(b)]. given #952 (F,wt=14): 3895 (x v y) ' ^ (z ^ ((y ^ u) v x)) = 0. [para(1483(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #953 (F,wt=14): 3903 ((x ^ y) v z) ^ ((z v y) ' ^ u) = 0. [para(1486(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #954 (T,wt=14): 3907 ((x ^ y) v z) ^ (u ^ (z v y) ') = 0. [para(1486(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #955 (T,wt=14): 3927 (x v y) ' ^ (((z ^ y) v x) ^ u) = 0. [para(1486(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #956 (A,wt=15): 404 (x ^ y) v y ' != 1 | (x ^ y) ' = y '. [para(291(a,1),43(b,1)),xx(b)]. given #957 (F,wt=14): 3928 (x v y) ' ^ (z ^ ((u ^ y) v x)) = 0. [para(1486(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #958 (F,wt=14): 3937 x ^ (y ^ (((y ^ x) v z) ' ^ u)) = 0. [para(1510(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #959 (T,wt=14): 3940 x ^ (y ^ (z v ((y ^ x) v u)) ') = 0. [para(23(a,1),1510(a,1,2,2,1))]. given #960 (T,wt=14): 3941 x ^ (y ^ (z ^ ((z ^ x) v u) ')) = 0. [para(1510(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #961 (A,wt=17): 405 x v (y v (x v z)) ' != 1 | y v (x v z) = x. [para(143(a,1),43(b,1)),demod(12(4),272(13)),xx(b)]. given #962 (F,wt=14): 3943 x ^ (y ^ ((y ^ (x v z)) v u) ') = 0. [para(1510(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #963 (F,wt=14): 3948 x ^ (y ^ ((y ^ (z v x)) v u) ') = 0. [para(1510(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #964 (T,wt=14): 3954 x ^ (y ^ (((y v z) ^ x) v u) ') = 0. [para(1510(a,1),135(a,1,2)),demod(92(2)),flip(a)]. given #965 (T,wt=14): 3963 (x v (y ^ z)) ^ ((y v x) ' ^ u) = 0. [para(1552(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #966 (A,wt=17): 406 x v (y v (z v x)) ' != 1 | y v (z v x) = x. [para(144(a,1),43(b,1)),demod(12(4),272(13)),xx(b)]. given #967 (F,wt=14): 3967 (x v (y ^ z)) ^ (u ^ (y v x) ') = 0. [para(1552(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #968 (F,wt=14): 3968 (x v (y ^ (z ^ u))) ^ (z v x) ' = 0. [para(24(a,1),1552(a,1,1,2))]. given #969 (T,wt=14): 3969 ((x ^ (y ^ z)) v (y ^ u)) ^ y ' = 0. [para(86(a,1),1552(a,1,2,1))]. given #970 (T,wt=14): 3971 ((x ^ (y ^ z)) v (z ^ u)) ^ z ' = 0. [para(103(a,1),1552(a,1,2,1))]. given #971 (A,wt=19): 407 x v ((y v x) ' ^ z) != 1 | ((y v x) ' ^ z) ' = x. [para(145(a,1),43(b,1)),demod(12(4)),xx(b)]. given #972 (F,wt=14): 3979 (x v (y ^ z)) ^ (z v (u v x)) ' = 0. [para(152(a,1),1552(a,1,1,2)),demod(13(4))]. given #973 (F,wt=14): 3983 (x v (y ^ z)) ^ (u v (z v x)) ' = 0. [para(768(a,1),1552(a,1,1,2)),demod(13(4))]. low water: id=8165, wt=23 given #974 (T,wt=14): 3989 (x v y) ' ^ ((y v (x ^ z)) ^ u) = 0. [para(1552(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #975 (T,wt=14): 3990 (x v y) ' ^ (z ^ (y v (x ^ u))) = 0. [para(1552(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #976 (A,wt=19): 408 x v (y ^ (z v x) ') != 1 | (y ^ (z v x) ') ' = x. [para(149(a,1),43(b,1)),demod(12(4)),xx(b)]. given #977 (F,wt=14): 4010 (x ^ y) v (y ^ (z ^ (u ^ x))) ' = 1. [para(151(a,1),1225(a,1,2,1,2))]. given #978 (F,wt=14): 4011 (x v (y ^ (z ^ u))) ^ (u v x) ' = 0. [para(151(a,1),1552(a,1,1,2))]. given #979 (T,wt=14): 4017 (x v y) ' ^ ((z ^ (x ^ u)) v y) = 0. [para(24(a,1),1554(a,1,2,1))]. given #980 (T,wt=14): 4019 x ' ^ ((x ^ y) v (z ^ (x ^ u))) = 0. [para(86(a,1),1554(a,1,1,1))]. given #981 (A,wt=19): 411 x ^ (y v (x ^ z) ') != 0 | y v (x ^ z) ' = x '. [para(188(a,1),20(a,1)),flip(c),xx(a)]. given #982 (F,wt=14): 4021 x ' ^ ((x ^ y) v (z ^ (u ^ x))) = 0. [para(103(a,1),1554(a,1,1,1))]. given #983 (F,wt=14): 4029 (x v (y v z)) ' ^ ((u ^ x) v z) = 0. [para(152(a,1),1554(a,1,2,1)),demod(13(2))]. given #984 (T,wt=14): 4033 (x v (y v z)) ' ^ ((u ^ y) v z) = 0. [para(768(a,1),1554(a,1,2,1)),demod(13(2))]. given #985 (T,wt=14): 4037 (x v (y v z)) ' ^ ((x ^ u) v y) = 0. [para(1554(a,1),117(a,1,2)),demod(14(4),83(4)),flip(a)]. given #986 (A,wt=19): 413 x ^ (y v (x ^ z) ') != 0 | (y v (x ^ z) ') ' = x. [para(188(a,1),41(a,1)),demod(14(7)),xx(a)]. given #987 (F,wt=14): 4039 (x v y) ' ^ ((z ^ (u ^ x)) v y) = 0. [para(151(a,1),1554(a,1,2,1))]. given #988 (F,wt=14): 4043 ((x ^ y) v (x ^ z)) ^ (x ' ^ u) = 0. [para(1556(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #989 (T,wt=14): 4045 ((x ^ y) v (x ^ z)) ^ (u ^ x ') = 0. [para(1556(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #990 (T,wt=14): 4054 x ' ^ (((x ^ y) v (x ^ z)) ^ u) = 0. [para(1556(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #991 (A,wt=23): 414 (x v y) ^ (z v (y ^ u) ') != 0 | (x v y) ' = z v (y ^ u) '. [para(188(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #992 (F,wt=14): 4055 x ' ^ (y ^ ((x ^ z) v (x ^ u))) = 0. [para(1556(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #993 (F,wt=14): 4059 ((x ^ y) v (z ^ x)) ^ (x ' ^ u) = 0. [para(1561(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #994 (T,wt=14): 4062 ((x ^ y) v (z ^ x)) ^ (u ^ x ') = 0. [para(1561(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #995 (T,wt=14): 4063 ((x ^ (y ^ z)) v (u ^ y)) ^ y ' = 0. [para(24(a,1),1561(a,1,1,1))]. given #996 (A,wt=19): 415 (x v y) ^ (x ^ z) ' != 0 | (x v y) ' = (x ^ z) '. [para(188(a,1),42(a,1)),xx(a)]. given #997 (F,wt=14): 4089 x ' ^ (((x ^ y) v (z ^ x)) ^ u) = 0. [para(1561(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #998 (F,wt=14): 4090 x ' ^ (y ^ ((x ^ z) v (u ^ x))) = 0. [para(1561(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #999 (T,wt=14): 4096 ((x ^ (y ^ z)) v (u ^ z)) ^ z ' = 0. [para(151(a,1),1561(a,1,1,1))]. given #1000 (T,wt=14): 4102 x v (y v (z v ((z v x) ^ u) ')) = 1. [para(1610(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1001 (A,wt=19): 419 x ^ (y ^ (x ^ z)) ' != 0 | (y ^ (x ^ z)) ' = x '. [para(196(a,1),20(a,1)),flip(c),xx(a)]. given #1002 (F,wt=14): 4104 x v (y v (z ^ ((y v x) ^ u)) ') = 1. [para(24(a,1),1610(a,1,2,2,1))]. given #1003 (F,wt=14): 4105 x v (y v ((y v (x ^ z)) ^ u) ') = 1. [para(1610(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #1004 (T,wt=14): 4110 x v (y v ((y v (z ^ x)) ^ u) ') = 1. [para(1610(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #1005 (T,wt=14): 4124 (x ^ y) v ((y ^ (z ^ x)) ' v u) = 1. [para(1620(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1006 (A,wt=17): 420 x ^ (y ^ (x ^ z)) ' != 0 | y ^ (x ^ z) = x. [para(196(a,1),41(a,1)),demod(14(7),272(13)),xx(a)]. given #1007 (F,wt=14): 4128 (x ^ y) v (z v (y ^ (u ^ x)) ') = 1. [para(1620(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1008 (F,wt=14): 4132 ((x v (y v z)) ^ u) v (u ^ y) ' = 1. [para(74(a,1),1620(a,1,2,1,2))]. given #1009 (T,wt=14): 4133 ((x v (y v z)) ^ u) v (u ^ z) ' = 1. [para(95(a,1),1620(a,1,2,1,2))]. given #1010 (T,wt=14): 4146 (x ^ (y ^ z)) ' v (u v (z ^ x)) = 1. [para(1620(a,1),111(a,1,1)),demod(69(8),1620(11))]. given #1011 (A,wt=23): 421 (x v y) ^ (z ^ (y ^ u)) ' != 0 | (x v y) ' = (z ^ (y ^ u)) '. [para(196(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #1012 (F,wt=14): 4165 ((x v y) ^ z) v ((z ^ x) ' v u) = 1. [para(1627(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1013 (F,wt=14): 4168 ((x v y) ^ z) v (u v (z ^ x) ') = 1. [para(1627(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1014 (T,wt=14): 4175 ((x v y) ^ z) v (z ^ (y ^ u)) ' = 1. [para(190(a,1),1627(a,1,1,1))]. given #1015 (T,wt=14): 4178 (x ^ y) ' v (((y v z) ^ x) v u) = 1. [para(1627(a,1),110(a,1,1)),demod(69(8),4164(11))]. given #1016 (A,wt=19): 424 x ^ ((y ^ x) ' v z) != 0 | (y ^ x) ' v z = x '. [para(197(a,1),20(a,1)),flip(c),xx(a)]. given #1017 (F,wt=14): 4179 (x ^ y) ' v (z v ((y v u) ^ x)) = 1. [para(1627(a,1),111(a,1,1)),demod(69(8),1627(11))]. given #1018 (F,wt=14): 4188 ((x v y) ^ z) v ((z ^ y) ' v u) = 1. [para(1629(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1019 (T,wt=14): 4191 ((x v y) ^ z) v (u v (z ^ y) ') = 1. [para(1629(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1020 (T,wt=14): 4205 (x ^ (y ^ z)) v (z ^ (y ^ x)) ' = 1. [para(250(a,1),1629(a,1,1,1)),demod(15(2))]. given #1021 (A,wt=16): 428 (x ^ ((y ^ x) v z)) v ((y ^ x) ' v u) = 1. [para(28(a,1),197(a,1,2,1,1))]. given #1022 (F,wt=14): 4209 (x ^ y) ' v (((z v y) ^ x) v u) = 1. [para(1629(a,1),110(a,1,1)),demod(69(8),4187(11))]. given #1023 (F,wt=14): 4210 (x ^ y) ' v (z v ((u v y) ^ x)) = 1. [para(1629(a,1),111(a,1,1)),demod(69(8),1629(11))]. given #1024 (T,wt=14): 4216 (x ^ y) ' v ((z v (x v u)) ^ y) = 1. [para(23(a,1),1671(a,1,2,1))]. given #1025 (T,wt=14): 4223 x ' v ((x v y) ^ (z v (x v u))) = 1. [para(74(a,1),1671(a,1,1,1))]. given #1026 (A,wt=19): 429 x ^ ((y ^ x) ' v z) != 0 | ((y ^ x) ' v z) ' = x. [para(197(a,1),41(a,1)),demod(14(7)),xx(a)]. given #1027 (F,wt=14): 4224 x ' v ((x v y) ^ (z v (u v x))) = 1. [para(95(a,1),1671(a,1,1,1))]. given #1028 (F,wt=14): 4232 (x ^ (y ^ z)) ' v ((u v x) ^ z) = 1. [para(190(a,1),1671(a,1,2,1)),demod(15(2))]. given #1029 (T,wt=14): 4234 (x ^ (y ^ z)) ' v ((u v y) ^ z) = 1. [para(821(a,1),1671(a,1,2,1)),demod(15(2))]. given #1030 (T,wt=14): 4258 (x ^ ((x ^ y) v z)) v (y ^ x) ' = 1. [para(154(a,1),193(a,1,2,1))]. given #1031 (A,wt=23): 430 (x v y) ^ ((z ^ y) ' v u) != 0 | (x v y) ' = (z ^ y) ' v u. [para(197(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #1032 (F,wt=14): 4260 x ^ (y ^ (y ^ ((y ^ x) v z)) ') = 0. [para(154(a,1),291(a,1,2)),demod(14(6),15(6))]. given #1033 (F,wt=14): 4284 (x ^ ((y ^ x) v z)) v (x ^ y) ' = 1. [para(154(a,1),202(a,1,2,1))]. given #1034 (T,wt=14): 4298 ((x ^ y) v z) ' ^ (u ^ (y ^ x)) = 0. [para(154(a,1),599(a,1,2,2))]. given #1035 (T,wt=14): 4327 (x ^ (y v z)) v ((y ^ x) ' v u) = 1. [para(1673(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1036 (A,wt=19): 433 x ^ (y ^ (z ^ x)) ' != 0 | (y ^ (z ^ x)) ' = x '. [para(199(a,1),20(a,1)),flip(c),xx(a)]. given #1037 (F,wt=14): 4331 (x ^ (y v z)) v (u v (y ^ x) ') = 1. [para(1673(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1038 (F,wt=14): 4335 ((x v (y v z)) ^ (y v u)) v y ' = 1. [para(74(a,1),1673(a,1,2,1))]. given #1039 (T,wt=14): 4336 ((x v (y v z)) ^ (z v u)) v z ' = 1. [para(95(a,1),1673(a,1,2,1))]. given #1040 (T,wt=14): 4345 (x ^ (y v z)) v (z ^ (u ^ x)) ' = 1. [para(190(a,1),1673(a,1,1,2)),demod(15(4))]. given #1041 (A,wt=16): 438 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) ' = 1. [para(28(a,1),199(a,1,2,1,2))]. given #1042 (F,wt=14): 4347 (x ^ (y v z)) v (u ^ (z ^ x)) ' = 1. [para(821(a,1),1673(a,1,1,2)),demod(15(4))]. given #1043 (F,wt=14): 4351 (x ^ y) ' v ((y ^ (x v z)) v u) = 1. [para(1673(a,1),110(a,1,1)),demod(69(8),4213(11))]. given #1044 (T,wt=14): 4353 (x ^ y) ' v (z v (y ^ (x v u))) = 1. [para(1673(a,1),111(a,1,1)),demod(69(8),1673(11))]. given #1045 (T,wt=14): 4369 ((x v y) ^ (x v z)) v (x ' v u) = 1. [para(1675(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1046 (A,wt=17): 439 x ^ (y ^ (z ^ x)) ' != 0 | y ^ (z ^ x) = x. [para(199(a,1),41(a,1)),demod(14(7),272(13)),xx(a)]. given #1047 (F,wt=14): 4371 ((x v y) ^ (x v z)) v (u v x ') = 1. [para(1675(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1048 (F,wt=14): 4379 x ' v (((x v y) ^ (x v z)) v u) = 1. [para(1675(a,1),110(a,1,1)),demod(69(8),4215(11))]. given #1049 (T,wt=14): 4380 x ' v (y v ((x v z) ^ (x v u))) = 1. [para(1675(a,1),111(a,1,1)),demod(69(8),1675(11))]. given #1050 (T,wt=14): 4387 ((x v y) ^ (z v x)) v (x ' v u) = 1. [para(1680(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1051 (A,wt=23): 440 (x v y) ^ (z ^ (u ^ y)) ' != 0 | (x v y) ' = (z ^ (u ^ y)) '. [para(199(a,1),42(a,1,2)),demod(89(2)),xx(a)]. given #1052 (F,wt=14): 4390 ((x v y) ^ (z v x)) v (u v x ') = 1. [para(1680(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1053 (F,wt=14): 4391 ((x v (y v z)) ^ (u v y)) v y ' = 1. [para(23(a,1),1680(a,1,1,1))]. given #1054 (T,wt=14): 4408 x ' v (((x v y) ^ (z v x)) v u) = 1. [para(1680(a,1),110(a,1,1)),demod(69(8),4219(11))]. given #1055 (T,wt=14): 4409 x ' v (y v ((x v z) ^ (u v x))) = 1. [para(1680(a,1),111(a,1,1)),demod(69(8),1680(11))]. given #1056 (A,wt=20): 441 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x) ' = z. [para(14(a,1),44(a,1,1))]. given #1057 (F,wt=14): 4417 x v (y v (z v ((z ^ u) v x) ')) = 1. [para(1719(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1058 (F,wt=14): 4419 x v (y v ((z ^ (y ^ u)) v x) ') = 1. [para(24(a,1),1719(a,1,2,2,1,1))]. given #1059 (T,wt=14): 4420 x v (y v ((y ^ z) v (x ^ u)) ') = 1. [para(1719(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #1060 (T,wt=14): 4425 x v (y v ((y ^ z) v (u ^ x)) ') = 1. [para(1719(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #1061 (A,wt=20): 442 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y) ' = z. [para(14(a,1),44(b,1)),demod(15(6))]. given #1062 (F,wt=14): 4426 x v (y v (z v ((u ^ y) v x) ')) = 1. [para(152(a,1),1719(a,1,2,2,1,1)),demod(13(5))]. given #1063 (F,wt=14): 4427 x v (y v (z v ((u ^ z) v x) ')) = 1. [para(768(a,1),1719(a,1,2,2,1,1)),demod(13(5))]. given #1064 (T,wt=14): 4433 x v (y v ((z ^ (u ^ y)) v x) ') = 1. [para(151(a,1),1719(a,1,2,2,1,1))]. given #1065 (T,wt=14): 4522 x v (((x ^ y) v (x ^ z)) ' v u) = 1. [para(1722(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1066 (A,wt=26): 443 (x ^ (y ^ z)) v u != 1 | x ^ (y ^ (z ^ u)) != 0 | (x ^ (y ^ z)) ' = u. [para(15(a,1),44(a,1,1)),demod(15(8),15(12))]. given #1067 (F,wt=14): 4526 x v (y v ((x ^ z) v (x ^ u)) ') = 1. [para(1722(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1068 (F,wt=14): 4527 x v ((y ^ (x ^ z)) v (x ^ u)) ' = 1. [para(24(a,1),1722(a,1,2,1,1))]. given #1069 (T,wt=14): 4528 x v ((x ^ y) v (z ^ (x ^ u))) ' = 1. [para(24(a,1),1722(a,1,2,1,2))]. given #1070 (T,wt=14): 4538 ((x ^ y) v (x ^ z)) ' v (u v x) = 1. [para(1722(a,1),111(a,1,1)),demod(69(8),1722(11))]. given #1071 (A,wt=18): 444 x v y != 1 | z ^ x != 0 | (z ^ x) ' = x v y. [para(16(a,1),44(b,1,2)),demod(23(3),101(3))]. given #1072 (F,wt=14): 4540 x v ((y ^ (z ^ x)) v (x ^ u)) ' = 1. [para(151(a,1),1722(a,1,2,1,1))]. given #1073 (F,wt=14): 4541 x v ((x ^ y) v (z ^ (u ^ x))) ' = 1. [para(151(a,1),1722(a,1,2,1,2))]. given #1074 (T,wt=14): 4546 x v (((x ^ y) v (z ^ x)) ' v u) = 1. [para(1727(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1075 (T,wt=14): 4549 x v (y v (x v ((x v y) ^ z)) ') = 1. [para(16(a,1),1727(a,1,2,1,2)),demod(12(4),13(6))]. given #1076 (A,wt=18): 445 x ^ y != 1 | x ^ y != 0 | (x ^ y) ' = x ^ y. [para(34(a,1),44(a,1)),demod(61(5),59(5))]. given #1077 (F,wt=14): 4551 x v (y v ((x ^ z) v (u ^ x)) ') = 1. [para(1727(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1078 (F,wt=14): 4552 x v ((y ^ (x ^ z)) v (u ^ x)) ' = 1. [para(24(a,1),1727(a,1,2,1,1))]. given #1079 (T,wt=14): 4576 ((x ^ y) v (z ^ x)) ' v (u v x) = 1. [para(1727(a,1),111(a,1,1)),demod(69(8),1727(11))]. given #1080 (T,wt=14): 4587 x v ((y ^ (z ^ x)) v (u ^ x)) ' = 1. [para(151(a,1),1727(a,1,2,1,1))]. given #1081 (A,wt=26): 448 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z) ' = x v u. [para(23(a,1),44(a,1))]. given #1082 (F,wt=14): 4593 x ^ (y ^ (z ^ ((z v u) ^ x) ')) = 0. [para(1782(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1083 (F,wt=14): 4599 x ^ (y ^ (z ^ ((u v y) ^ x) ')) = 0. [para(190(a,1),1782(a,1,2,2,1,1)),demod(15(5))]. given #1084 (T,wt=14): 4601 x ^ (y ^ (z ^ ((u v z) ^ x) ')) = 0. [para(821(a,1),1782(a,1,2,2,1,1)),demod(15(5))]. given #1085 (T,wt=14): 4610 x ^ (((x v y) ^ (x v z)) ' ^ u) = 0. [para(1784(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1086 (A,wt=26): 449 (x ^ (y ^ z)) v u != 1 | y ^ (x ^ (z ^ u)) != 0 | (y ^ (x ^ z)) ' = u. [para(24(a,1),44(a,1,1)),demod(15(7))]. given #1087 (F,wt=14): 4613 x ^ (y ^ ((x v z) ^ (x v u)) ') = 0. [para(1784(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1088 (F,wt=14): 4622 ((x v y) ^ (x v z)) ' ^ (u ^ x) = 0. [para(1784(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6))]. given #1089 (T,wt=14): 4696 x ^ ((x v y) ^ (z v (u v x))) ' = 0. [para(13(a,1),1789(a,1,2,1,2))]. given #1090 (T,wt=14): 4697 x ^ (((x v y) ^ (z v x)) ' ^ u) = 0. [para(1789(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1091 (A,wt=26): 450 (x ^ y) v (z ^ u) != 1 | x ^ (z ^ (y ^ u)) != 0 | (x ^ y) ' = z ^ u. [para(24(a,1),44(b,1,2))]. given #1092 (F,wt=14): 4701 x ^ (y ^ ((x v z) ^ (u v x)) ') = 0. [para(1789(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1093 (F,wt=14): 4722 ((x v y) ^ (z v x)) ' ^ (u ^ x) = 0. [para(1789(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6))]. given #1094 (T,wt=14): 4728 x v ((y v x) ' v (z v (y v u))) = 1. [para(1927(a,1),13(a,1,1)),demod(80(2),13(6),13(5)),flip(a)]. given #1095 (T,wt=14): 4745 x v ((y ^ z) v ((z ^ y) v x) ') = 1. [para(250(a,1),1927(a,1,2,2)),demod(12(5))]. given #1096 (A,wt=20): 451 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y) ' = z. [para(24(a,1),44(b,1))]. given #1097 (F,wt=14): 4752 x ^ ((y ^ x) ' ^ (z ^ (y ^ u))) = 0. [para(2005(a,1),15(a,1,1)),demod(83(2),15(6),15(5)),flip(a)]. given #1098 (F,wt=14): 4759 x ^ (y ^ ((z v (u v y)) ^ x) ') = 0. [para(95(a,1),2005(a,1,2,2)),demod(14(5))]. given #1099 (T,wt=14): 4767 x ^ ((y v z) ^ ((z v y) ^ x) ') = 0. [para(164(a,1),2005(a,1,2,2)),demod(14(5))]. given #1100 (T,wt=14): 4801 x v (y v ((z ^ y) v (x ^ u)) ') = 1. [para(2401(a,1),29(a,1,2)),demod(89(2)),flip(a)]. given #1101 (A,wt=22): 453 x ^ y != 1 | z ^ (x ^ y) != 0 | (x ^ y) ' = z ^ (x ^ y). [para(31(a,1),44(a,1)),demod(151(6),130(6))]. given #1102 (F,wt=14): 4809 x v (y v ((z ^ y) v (u ^ x)) ') = 1. [para(2401(a,1),101(a,1,2)),demod(89(2)),flip(a)]. given #1103 (F,wt=14): 4901 x v (((y ^ x) v (x ^ z)) ' v u) = 1. [para(2457(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1104 (T,wt=14): 4905 x v (y v ((z ^ x) v (x ^ u)) ') = 1. [para(2457(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1105 (T,wt=14): 4907 x v ((y ^ x) v (z ^ (x ^ u))) ' = 1. [para(24(a,1),2457(a,1,2,1,2))]. given #1106 (A,wt=23): 454 x ^ (y ^ ((x ^ y) ' v z)) != 0 | (x ^ y) ' v z = (x ^ y) '. [para(81(a,1),44(a,1)),flip(c),xx(a)]. given #1107 (F,wt=14): 4915 ((x ^ y) v (y ^ z)) ' v (u v y) = 1. [para(2457(a,1),111(a,1,1)),demod(69(8),2457(11))]. given #1108 (F,wt=14): 4917 x v ((y ^ x) v (z ^ (u ^ x))) ' = 1. [para(151(a,1),2457(a,1,2,1,2))]. given #1109 (T,wt=14): 4921 x ^ (y ^ (((z v y) ^ x) ' ^ u)) = 0. [para(2478(a,1),15(a,1,1)),demod(83(2),15(6)),flip(a)]. given #1110 (T,wt=14): 4925 x ^ (y ^ ((z v y) ^ (x v u)) ') = 0. [para(2478(a,1),27(a,1,2)),demod(92(2)),flip(a)]. given #1111 (A,wt=19): 456 (x ^ y) v (y ' ^ z) != 1 | (x ^ y) ' = y ' ^ z. [para(84(a,1),44(b,1,2)),demod(92(8)),xx(b)]. given #1112 (F,wt=14): 4933 x ^ (y ^ ((z v y) ^ (u v x)) ') = 0. [para(2478(a,1),96(a,1,2)),demod(92(2)),flip(a)]. given #1113 (F,wt=14): 4950 x ^ ((y v (z v x)) ^ (x v u)) ' = 0. [para(13(a,1),2553(a,1,2,1,1))]. given #1114 (T,wt=14): 4951 x ^ (((y v x) ^ (x v z)) ' ^ u) = 0. [para(2553(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1115 (T,wt=14): 4955 x ^ (y ^ ((z v x) ^ (x v u)) ') = 0. [para(2553(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1116 (A,wt=23): 457 x ^ (y ^ (z v (x ^ y) ')) != 0 | z v (x ^ y) ' = (x ^ y) '. [para(90(a,1),44(a,1)),flip(c),xx(a)]. given #1117 (F,wt=14): 4965 ((x v y) ^ (y v z)) ' ^ (u ^ y) = 0. [para(2553(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6))]. given #1118 (F,wt=14): 4973 (x v y) ' ^ (x v (z ^ (y ^ u))) = 0. [para(24(a,1),2888(a,1,2,2))]. given #1119 (T,wt=14): 4974 (x v y) ' ^ (x v ((x v y) ^ z)) = 0. [para(65(a,1),2888(a,1,1,1))]. given #1120 (T,wt=14): 4975 (x v y) ' ^ (y v ((x v y) ^ z)) = 0. [para(67(a,1),2888(a,1,1,1))]. given #1121 (A,wt=19): 458 (x ^ y) v (z ^ y ') != 1 | (x ^ y) ' = z ^ y '. [para(93(a,1),44(b,1,2)),demod(92(8)),xx(b)]. given #1122 (F,wt=14): 4983 (x v (y v z)) ' ^ (x v (u ^ y)) = 0. [para(152(a,1),2888(a,1,2,2))]. given #1123 (F,wt=14): 4986 (x v (y v z)) ' ^ (x v (u ^ z)) = 0. [para(768(a,1),2888(a,1,2,2))]. given #1124 (T,wt=14): 4991 (x v y) ' ^ (x v (z ^ (u ^ y))) = 0. [para(151(a,1),2888(a,1,2,2))]. given #1125 (T,wt=14): 5116 (x ^ y) ' v (x ^ (z v (y v u))) = 1. [para(23(a,1),2925(a,1,2,2))]. given #1126 (A,wt=15): 459 (x ^ y) v x ' != 1 | (x ^ y) ' = x '. [para(93(a,1),44(b,1)),xx(b)]. given #1127 (F,wt=14): 5118 (x ^ y) ' v (x ^ ((x ^ y) v z)) = 1. [para(59(a,1),2925(a,1,1,1))]. given #1128 (F,wt=14): 5120 (x ^ y) ' v (y ^ ((x ^ y) v z)) = 1. [para(61(a,1),2925(a,1,1,1))]. given #1129 (T,wt=14): 5128 (x ^ (y ^ z)) ' v (x ^ (u v y)) = 1. [para(190(a,1),2925(a,1,2,2))]. given #1130 (T,wt=14): 5131 (x ^ (y ^ z)) ' v (x ^ (u v z)) = 1. [para(821(a,1),2925(a,1,2,2))]. given #1131 (A,wt=24): 460 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = y ^ z. [para(59(a,1),44(b,1,2))]. given #1132 (F,wt=14): 5145 (x ^ y) ' v ((z v (u v x)) ^ y) = 1. [para(13(a,1),2973(a,1,2,1))]. given #1133 (F,wt=14): 5156 x ' v ((y v x) ^ (z v (x v u))) = 1. [para(74(a,1),2973(a,1,1,1))]. given #1134 (T,wt=14): 5157 x ' v ((y v x) ^ (z v (u v x))) = 1. [para(95(a,1),2973(a,1,1,1))]. given #1135 (T,wt=14): 5189 (x ^ (y v z)) v ((z ^ x) ' v u) = 1. [para(2975(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1136 (A,wt=28): 461 (x ^ y) v ((y v z) ^ u) != 1 | x ^ (y ^ u) != 0 | (x ^ y) ' = (y v z) ^ u. [para(27(a,1),44(b,1,2))]. given #1137 (F,wt=14): 5190 (x ^ (y v (z v u))) v (u ^ x) ' = 1. [para(13(a,1),2975(a,1,1,2))]. given #1138 (F,wt=14): 5194 (x ^ (y v z)) v (u v (z ^ x) ') = 1. [para(2975(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1139 (T,wt=14): 5199 (x ^ y) v (z ^ (y ^ (u ^ x))) ' = 1. [para(86(a,1),2975(a,1,1,2)),demod(15(4),15(3))]. given #1140 (T,wt=14): 5200 ((x v (y v z)) ^ (u v z)) v z ' = 1. [para(95(a,1),2975(a,1,2,1))]. given #1141 (A,wt=19): 462 (x ^ y) v (y v z) ' != 1 | (y v z) ' = (x ^ y) '. [para(132(a,1),44(b,1,2)),demod(92(8)),flip(c),xx(b)]. given #1142 (F,wt=14): 5222 (x ^ y) ' v ((y ^ (z v x)) v u) = 1. [para(2975(a,1),110(a,1,1)),demod(69(8),5146(11))]. given #1143 (F,wt=14): 5224 (x ^ y) ' v (z v (y ^ (u v x))) = 1. [para(2975(a,1),111(a,1,1)),demod(69(8),2975(11))]. given #1144 (T,wt=14): 5243 ((x v y) ^ (y v z)) v (y ' v u) = 1. [para(2977(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1145 (T,wt=14): 5245 ((x v y) ^ (y v z)) v (u v y ') = 1. [para(2977(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1146 (A,wt=19): 463 (x ^ y) v (z v y) ' != 1 | (z v y) ' = (x ^ y) '. [para(139(a,1),44(b,1,2)),demod(92(8)),flip(c),xx(b)]. given #1147 (F,wt=14): 5252 x ' v (((y v x) ^ (x v z)) v u) = 1. [para(2977(a,1),110(a,1,1)),demod(69(8),5148(11))]. given #1148 (F,wt=14): 5253 x ' v (y v ((z v x) ^ (x v u))) = 1. [para(2977(a,1),111(a,1,1)),demod(69(8),2977(11))]. given #1149 (T,wt=14): 5377 ((x v y) ^ (z v y)) v (y ' v u) = 1. [para(2982(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1150 (T,wt=14): 5379 ((x v y) ^ (z v y)) v (u v y ') = 1. [para(2982(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1151 (A,wt=24): 464 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z ^ y. [para(61(a,1),44(b,1,2))]. given #1152 (F,wt=14): 5395 x ' v (((y v x) ^ (z v x)) v u) = 1. [para(2982(a,1),110(a,1,1)),demod(69(8),5152(11))]. given #1153 (F,wt=14): 5396 x ' v (y v ((z v x) ^ (u v x))) = 1. [para(2982(a,1),111(a,1,1)),demod(69(8),2982(11))]. given #1154 (T,wt=14): 5403 x ^ ((y v (z v x)) ^ (u v x)) ' = 0. [para(13(a,1),3030(a,1,2,1,1))]. given #1155 (T,wt=14): 5404 x ^ ((y v x) ^ (z v (u v x))) ' = 0. [para(13(a,1),3030(a,1,2,1,2))]. given #1156 (A,wt=22): 466 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y) ' = (x ^ y) v z. [para(65(a,1),44(a,1)),demod(28(8))]. given #1157 (F,wt=14): 5405 x ^ (((y v x) ^ (z v x)) ' ^ u) = 0. [para(3030(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1158 (F,wt=14): 5407 x ^ (y ^ (x ^ (z v (x ^ y))) ') = 0. [para(17(a,1),3030(a,1,2,1,1)),demod(15(6))]. given #1159 (T,wt=14): 5411 x ^ (y ^ ((z v x) ^ (u v x)) ') = 0. [para(3030(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1160 (T,wt=14): 5432 ((x v y) ^ (z v y)) ' ^ (u ^ y) = 0. [para(3030(a,1),522(a,1,2,2,2,1)),demod(82(6),37(6))]. given #1161 (A,wt=32): 467 (x ^ y) v (z ^ ((y ^ z) v u)) != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z ^ ((y ^ z) v u). [para(28(a,1),44(b,1,2))]. given #1162 (F,wt=14): 5437 (x ^ y) ' v (x ^ (z v (u v y))) = 1. [para(13(a,1),3172(a,1,2,2))]. given #1163 (F,wt=14): 5440 (x ^ y) ' v (x ^ (z v (x ^ y))) = 1. [para(59(a,1),3172(a,1,1,1))]. given #1164 (T,wt=14): 5442 (x ^ y) ' v (y ^ (z v (x ^ y))) = 1. [para(61(a,1),3172(a,1,1,1))]. given #1165 (T,wt=14): 5477 (x v (y ^ z)) ^ ((z v x) ' ^ u) = 0. [para(3230(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1166 (A,wt=22): 468 x v (y ^ z) != 1 | y ^ z != 0 | (y ^ z) ' = x v (y ^ z). [para(67(a,1),44(a,1)),demod(97(8))]. given #1167 (F,wt=14): 5480 (x v (y ^ z)) ^ (u ^ (z v x) ') = 0. [para(3230(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1168 (F,wt=14): 5509 (x v y) ' ^ ((y v (z ^ x)) ^ u) = 0. [para(3230(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #1169 (T,wt=14): 5510 (x v y) ' ^ (z ^ (y v (u ^ x))) = 0. [para(3230(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #1170 (T,wt=14): 5566 x ^ (y ^ (x ^ ((y ^ x) v z)) ') = 0. [para(160(a,1),1510(a,1,2,2,1))]. given #1171 (A,wt=32): 472 (x ^ y) v z != 1 | x ^ (y ^ ((x ^ (y ^ u)) v z)) != 0 | (x ^ y) ' = (x ^ (y ^ u)) v z. [para(29(a,1),44(a,1)),demod(15(6),15(15))]. given #1172 (F,wt=14): 5596 x ' ^ ((y ^ x) v (z ^ (x ^ u))) = 0. [para(86(a,1),3231(a,1,1,1))]. given #1173 (F,wt=14): 5598 x ' ^ ((y ^ x) v (z ^ (u ^ x))) = 0. [para(103(a,1),3231(a,1,1,1))]. given #1174 (T,wt=14): 5612 (x v (y v z)) ' ^ ((u ^ x) v y) = 0. [para(3231(a,1),117(a,1,2)),demod(14(4),83(4)),flip(a)]. given #1175 (T,wt=14): 5621 ((x ^ y) v (y ^ z)) ^ (y ' ^ u) = 0. [para(3233(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1176 (A,wt=23): 473 x ^ (y ^ (x ^ (y ^ z)) ') != 0 | (x ^ (y ^ z)) ' = (x ^ y) '. [para(183(a,1),44(a,1)),demod(15(5),15(14)),flip(c),xx(a)]. given #1177 (F,wt=14): 5623 ((x ^ y) v (y ^ z)) ^ (u ^ y ') = 0. [para(3233(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1178 (F,wt=14): 5631 x ' ^ (((y ^ x) v (x ^ z)) ^ u) = 0. [para(3233(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #1179 (T,wt=14): 5632 x ' ^ (y ^ ((z ^ x) v (x ^ u))) = 0. [para(3233(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #1180 (T,wt=14): 5639 ((x ^ y) v (z ^ y)) ^ (y ' ^ u) = 0. [para(3238(a,1),15(a,1,1)),demod(83(2)),flip(a)]. given #1181 (A,wt=23): 474 x ^ (y ^ (z ^ (x ^ y)) ') != 0 | (z ^ (x ^ y)) ' = (x ^ y) '. [para(193(a,1),44(a,1)),flip(c),xx(a)]. given #1182 (F,wt=14): 5641 ((x ^ y) v (z ^ y)) ^ (u ^ y ') = 0. [para(3238(a,1),24(a,1,2)),demod(92(2)),flip(a)]. given #1183 (F,wt=14): 5662 x ' ^ (((y ^ x) v (z ^ x)) ^ u) = 0. [para(3238(a,1),518(a,1,2,2,1,1)),demod(82(6),69(6))]. given #1184 (T,wt=14): 5663 x ' ^ (y ^ ((z ^ x) v (u ^ x))) = 0. [para(3238(a,1),522(a,1,2,2,2,1)),demod(82(6),14(6),69(6))]. given #1185 (T,wt=14): 5680 x v (((y ^ x) v (z ^ x)) ' v u) = 1. [para(3287(a,1),13(a,1,1)),demod(80(2)),flip(a)]. given #1186 (A,wt=27): 476 x ^ (y ^ (z v ((x ^ y) v z) ')) != 0 | z v ((x ^ y) v z) ' = (x ^ y) '. [para(36(a,1),44(a,1)),flip(c),xx(a)]. given #1187 (F,wt=14): 5682 x v (y v (x v (z ^ (x v y))) ') = 1. [para(16(a,1),3287(a,1,2,1,1)),demod(13(6))]. given #1188 (F,wt=14): 5684 x v (y v ((z ^ x) v (u ^ x)) ') = 1. [para(3287(a,1),23(a,1,2)),demod(89(2)),flip(a)]. given #1189 (T,wt=14): 5706 ((x ^ y) v (z ^ y)) ' v (u v y) = 1. [para(3287(a,1),111(a,1,1)),demod(69(8),3287(11))]. given #1190 (T,wt=14): 5832 (x v y) ' ^ (x v (z ^ (x v y))) = 0. [para(65(a,1),3370(a,1,1,1))]. given #1191 (A,wt=36): 477 (x ^ y) v z != 1 | x ^ (y ^ (z v (((x ^ y) v z) ^ u))) != 0 | (x ^ y) ' = z v (((x ^ y) v z) ^ u). [para(30(a,1),44(a,1))]. given #1192 (F,wt=14): 5833 (x v y) ' ^ (y v (z ^ (x v y