============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13657 was started by mccune on cleo.thornwood, Mon Jun 19 16:45:34 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H27d.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 H27d.in assign(max_weight,25). terms(weights). weight(x ') = weight(x). end_of_list. clauses(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). end_of_list. clauses(goals). x ^ (y v z) = (x ^ y) v (x ^ z) # label(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) # label(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 ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [input]. 11 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. 22 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [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=5): 18 x v x ' = 1. [input]. given #8 (I,wt=5): 19 x ^ x ' = 0. [input]. given #9 (I,wt=13): 20 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=23): 21 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. given #11 (I,wt=13): 22 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(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): 68 1 ^ x = x. [para(37(a,1),14(a,1)),flip(a)]. given #18 (F,wt=3): 83 1 ' = 0. [hyper(20,a,40,a,b,68,a)]. given #19 (T,wt=5): 71 0 v x = x. [para(40(a,1),12(a,1)),flip(a)]. given #20 (T,wt=3): 86 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): 84 1 v x = 1. [para(68(a,1),16(a,1))]. given #23 (F,wt=5): 87 0 ^ x = 0. [para(71(a,1),16(a,1,2))]. given #24 (T,wt=5): 95 x v 1 = 1. [para(84(a,1),12(a,1)),flip(a)]. given #25 (T,wt=5): 98 x ^ 0 = 0. [para(87(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=6): 97 0 != x | x ' = 1. [back_demod(69),demod(95(2)),xx(a)]. given #28 (F,wt=6): 100 1 != x | x ' = 0. [back_demod(72),demod(98(4)),xx(b)]. given #29 (T,wt=7): 31 x v (y ^ x) = x. [para(14(a,1),17(a,1,2))]. given #30 (T,wt=7): 85 x v (x ' v y) = 1. [back_demod(35),demod(84(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=7): 89 x ^ (x ' ^ y) = 0. [back_demod(38),demod(87(5))]. given #33 (F,wt=7): 96 x v (y v x ') = 1. [back_demod(79),demod(95(5))]. given #34 (T,wt=7): 99 x ^ (y ^ x ') = 0. [back_demod(92),demod(98(5))]. given #35 (T,wt=9): 36 x v (y v (x v y) ') = 1. [para(18(a,1),13(a,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=7): 149 x ^ (x v y) ' = 0. [para(19(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #38 (F,wt=7): 156 x ^ (y v x) ' = 0. [para(12(a,1),149(a,1,2,1))]. given #39 (T,wt=9): 39 x ^ (y ^ (x ^ y) ') = 0. [para(19(a,1),15(a,1)),flip(a)]. given #40 (T,wt=9): 55 x ^ (x ^ y) = x ^ y. [para(33(a,1),15(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): 57 x ^ (y ^ x) = y ^ x. [para(33(a,1),15(a,2,2)),demod(14(2))]. given #43 (F,wt=9): 58 1 != x | 0 != x | x ' = x. [para(33(a,1),20(b,1)),demod(34(1)),flip(a),flip(b)]. given #44 (T,wt=9): 61 x v (x v y) = x v y. [para(34(a,1),13(a,1,1)),flip(a)]. given #45 (T,wt=9): 63 x v (y v x) = y v x. [para(34(a,1),13(a,2,2)),demod(12(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=7): 197 x v (x ^ y) ' = 1. [para(18(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #48 (F,wt=7): 209 x v (y ^ x) ' = 1. [para(14(a,1),197(a,1,2,1))]. given #49 (T,wt=9): 77 x ^ (y v (x v z)) = x. [para(23(a,1),16(a,1,2))]. given #50 (T,wt=9): 91 x v (y ^ (x ^ z)) = x. [para(24(a,1),17(a,1,2))]. 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=9): 101 x ^ (y v (z v x)) = x. [para(13(a,1),25(a,1,2))]. given #53 (F,wt=9): 110 x v (y ^ (z ^ x)) = x. [para(15(a,1),31(a,1,2))]. given #54 (T,wt=9): 118 x v (y v (x ' v z)) = 1. [para(85(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #55 (T,wt=9): 133 x ^ (y ^ (x ' ^ z)) = 0. [para(89(a,1),24(a,1,2)),demod(98(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=9): 135 x v (y v (z v x ')) = 1. [para(13(a,1),96(a,1,2))]. given #58 (F,wt=9): 139 x ^ (y ^ (z ^ x ')) = 0. [para(15(a,1),99(a,1,2))]. given #59 (T,wt=9): 142 x v (y v (y v x) ') = 1. [para(12(a,1),36(a,1,2,2,1))]. given #60 (T,wt=9): 154 x ^ ((x v y) ' ^ z) = 0. [para(89(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #61 (A,wt=13): 41 x v y != 1 | y ^ x != 0 | y ' = x. [para(12(a,1),20(a,1))]. given #62 (F,wt=3): 308 x ' ' = x. [para(18(a,1),41(a,1)),demod(14(5),19(5)),xx(a),xx(b)]. given #63 (F,wt=7): 327 x ' v (y v x) = 1. [para(308(a,1),96(a,1,2,2))]. given #64 (T,wt=7): 328 x ' ^ (y ^ x) = 0. [para(308(a,1),99(a,1,2,2))]. given #65 (T,wt=9): 155 x ^ (y ^ (x v z) ') = 0. [para(99(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #66 (A,wt=19): 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=9): 161 x ^ (y v (x v z)) ' = 0. [para(23(a,1),149(a,1,2,1))]. given #68 (F,wt=9): 162 x ^ (y v (z v x)) ' = 0. [para(13(a,1),156(a,1,2,1))]. given #69 (T,wt=9): 163 x ^ ((y v x) ' ^ z) = 0. [para(156(a,1),15(a,1,1)),demod(87(2)),flip(a)]. given #70 (T,wt=9): 168 x ^ (y ^ (z v x) ') = 0. [para(156(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #71 (A,wt=13): 43 x v y != 1 | y ^ x != 0 | x ' = y. [para(14(a,1),20(b,1))]. given #72 (F,wt=9): 169 x ^ (y ^ (y ^ x) ') = 0. [para(14(a,1),39(a,1,2,2,1))]. given #73 (F,wt=9): 203 x v ((x ^ y) ' v z) = 1. [para(85(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #74 (T,wt=9): 204 x v (y v (x ^ z) ') = 1. [para(96(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #75 (T,wt=9): 213 x v (y ^ (x ^ z)) ' = 1. [para(24(a,1),197(a,1,2,1))]. given #76 (A,wt=19): 44 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(15(a,1),20(b,1))]. given #77 (F,wt=9): 214 x v ((y ^ x) ' v z) = 1. [para(209(a,1),13(a,1,1)),demod(84(2)),flip(a)]. given #78 (F,wt=9): 216 x v (y ^ (z ^ x)) ' = 1. [para(15(a,1),209(a,1,2,1))]. given #79 (T,wt=9): 220 x v (y v (z ^ x) ') = 1. [para(209(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #80 (T,wt=9): 329 x ' v (y v (x v z)) = 1. [para(308(a,1),118(a,1,2,2,1))]. given #81 (A,wt=23): 47 x ^ (y v ((x ^ z) v (z ^ (u v y)))) = x ^ (y v (z ^ (x v u))). [para(12(a,1),21(a,1,2,2,2,2))]. given #82 (F,wt=9): 330 x ' ^ (y ^ (x ^ z)) = 0. [para(308(a,1),133(a,1,2,2,1))]. given #83 (F,wt=9): 331 x ' v (y v (z v x)) = 1. [para(308(a,1),135(a,1,2,2,2))]. given #84 (T,wt=9): 332 x ' ^ (y ^ (z ^ x)) = 0. [para(308(a,1),139(a,1,2,2,2))]. given #85 (T,wt=9): 630 (x ^ y) ' v (z v x) = 1. [para(17(a,1),331(a,1,2,2))]. given #86 (A,wt=23): 48 x ^ (y v ((z ^ (y v u)) v (x ^ z))) = x ^ (y v (z ^ (x v u))). [para(12(a,1),21(a,1,2,2))]. given #87 (F,wt=9): 634 (x ^ y) ' v (z v y) = 1. [para(31(a,1),331(a,1,2,2))]. given #88 (F,wt=9): 647 (x v y) ' ^ (z ^ x) = 0. [para(16(a,1),332(a,1,2,2))]. given #89 (T,wt=9): 651 (x v y) ' ^ (z ^ y) = 0. [para(25(a,1),332(a,1,2,2))]. given #90 (T,wt=10): 354 x v y != 0 | (x v y) ' = 1. [para(37(a,1),42(b,1)),demod(95(2),95(2)),xx(a)]. given #91 (A,wt=23): 49 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(14(a,1),21(a,1,2,2,1))]. given #92 (F,wt=10): 355 x v y != 1 | (x v y) ' = 0. [para(40(a,1),42(a,1,2)),demod(14(6),87(6)),xx(b)]. given #93 (F,wt=10): 477 x ^ y != 0 | (x ^ y) ' = 1. [para(37(a,1),44(b,1,2)),demod(12(3),84(3)),xx(a)]. given #94 (T,wt=10): 478 x ^ y != 1 | (x ^ y) ' = 0. [para(40(a,1),44(a,1)),demod(98(5),98(5)),xx(b)]. given #95 (T,wt=10): 734 x v y != 0 | (y v x) ' = 1. [para(12(a,1),354(a,1))]. given #96 (A,wt=23): 50 x ^ (y v ((x ^ z) v ((y v u) ^ z))) = x ^ (y v (z ^ (x v u))). [para(14(a,1),21(a,1,2,2,2))]. given #97 (F,wt=10): 761 x v y != 1 | (y v x) ' = 0. [para(12(a,1),355(a,1))]. given #98 (F,wt=10): 763 x ^ y != 0 | (y ^ x) ' = 1. [para(14(a,1),477(a,1))]. given #99 (T,wt=10): 765 x ^ y != 1 | (y ^ x) ' = 0. [para(14(a,1),478(a,1))]. given #100 (T,wt=11): 78 x v (y v (x ^ z)) = y v x. [para(17(a,1),23(a,1,2)),flip(a)]. given #101 (A,wt=15): 53 x ^ (y v (z ^ (x v y '))) = x ^ (y v z). [para(18(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #102 (F,wt=11): 90 x ^ (y ^ (x v z)) = y ^ x. [para(16(a,1),24(a,1,2)),flip(a)]. given #103 (F,wt=11): 102 x ^ ((y v x) ^ z) = x ^ z. [para(25(a,1),15(a,1,1)),flip(a)]. given #104 (T,wt=11): 107 x ^ (y ^ (z v x)) = y ^ x. [para(25(a,1),24(a,1,2)),flip(a)]. given #105 (T,wt=11): 108 x v ((y ^ x) v z) = x v z. [para(31(a,1),13(a,1,1)),flip(a)]. given #106 (A,wt=13): 60 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(46),demod(55(4))]. given #107 (F,wt=6): 937 x ' != 1 | 0 = x. [para(328(a,1),60(b,1)),demod(308(8),328(9)),flip(a),flip(c),xx(b)]. given #108 (F,wt=10): 938 (x v y) ' != 1 | x v y = 0. [para(647(a,1),60(b,1)),demod(308(10),647(12)),flip(a),xx(b)]. given #109 (T,wt=10): 939 (x v y) ' != 1 | y v x = 0. [para(12(a,1),938(a,1,1))]. given #110 (T,wt=10): 941 (x ^ y) ' != 1 | x ^ y = 0. [para(32(a,1),938(a,1,1)),demod(32(8))]. given #111 (A,wt=17): 65 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_demod(59),demod(61(7))]. given #112 (F,wt=10): 944 (x ^ y) ' != 1 | y ^ x = 0. [para(14(a,1),941(a,1,1))]. given #113 (F,wt=11): 113 x v (y v (z ^ x)) = y v x. [para(31(a,1),23(a,1,2)),flip(a)]. given #114 (T,wt=11): 115 x v (y v ((x v y) ' v z)) = 1. [para(85(a,1),13(a,1)),flip(a)]. given #115 (T,wt=11): 130 x ^ (y ^ ((x ^ y) ' ^ z)) = 0. [para(89(a,1),15(a,1)),flip(a)]. given #116 (A,wt=13): 66 x v y != 1 | 0 != x | x ' = x v y. [back_demod(45),demod(61(2))]. given #117 (F,wt=6): 1024 x ' != 0 | 1 = x. [para(327(a,1),66(a,1)),demod(308(8),327(9)),flip(b),flip(c),xx(a)]. given #118 (F,wt=10): 1025 (x ^ y) ' != 0 | x ^ y = 1. [para(630(a,1),66(a,1)),demod(308(10),630(12)),flip(b),xx(a)]. given #119 (T,wt=10): 1026 (x ^ y) ' != 0 | y ^ x = 1. [para(14(a,1),1025(a,1,1))]. given #120 (T,wt=10): 1028 (x v y) ' != 0 | x v y = 1. [para(26(a,1),1025(a,1,1)),demod(26(8))]. given #121 (A,wt=17): 73 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(40(a,1),21(a,1,2,2,2,2)),demod(64(5),40(6))]. given #122 (F,wt=10): 1031 (x v y) ' != 0 | y v x = 1. [para(12(a,1),1028(a,1,1))]. given #123 (F,wt=11): 134 x v (y v (z v (x v y) ')) = 1. [para(96(a,1),13(a,1)),flip(a)]. given #124 (T,wt=11): 138 x ^ (y ^ (z ^ (x ^ y) ')) = 0. [para(99(a,1),15(a,1)),flip(a)]. given #125 (T,wt=11): 146 x v (y v (z v (x v z) ')) = 1. [para(36(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #126 (A,wt=19): 74 x ^ (y v (x ' ^ (y v z))) = x ^ (y v (x ' ^ (x v z))). [back_demod(54),demod(71(5))]. given #127 (F,wt=11): 157 (x v y) ^ (x v (y v z)) ' = 0. [para(13(a,1),149(a,1,2,1))]. given #128 (F,wt=9): 1204 (x v y) ^ (y v x) ' = 0. [para(63(a,1),157(a,1,2,1))]. given #129 (T,wt=11): 158 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(149(a,1),15(a,1)),flip(a)]. given #130 (T,wt=11): 164 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(156(a,1),15(a,1)),flip(a)]. given #131 (A,wt=19): 75 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_demod(67),demod(73(9))]. given #132 (F,wt=11): 167 (x v y) ^ (x v (z v y)) ' = 0. [para(23(a,1),156(a,1,2,1))]. given #133 (F,wt=11): 173 x ^ (y ^ (z ^ (x ^ z) ')) = 0. [para(39(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #134 (T,wt=11): 175 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(39(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #135 (T,wt=11): 188 (x v y) ^ (z ^ x) = z ^ x. [para(57(a,1),27(a,2)),demod(187(4))]. given #136 (A,wt=19): 80 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(23(a,1),20(a,1))]. given #137 (F,wt=11): 194 (x v y) ^ (y v x) = x v y. [para(63(a,1),26(a,1,2))]. given #138 (F,wt=11): 205 x v (y v ((x ^ z) v y) ') = 1. [para(36(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #139 (T,wt=11): 206 ((x ^ y) v z) ^ (x v z) ' = 0. [para(29(a,1),156(a,1,2,1))]. given #140 (T,wt=11): 207 (x ^ y) v (z v x) = z v x. [para(63(a,1),29(a,2)),demod(192(4))]. given #141 (A,wt=23): 81 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(23(a,1),21(a,1,2))]. given #142 (F,wt=11): 208 x v (y v ((x v y) ^ z) ') = 1. [para(197(a,1),13(a,1)),flip(a)]. given #143 (F,wt=11): 210 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(15(a,1),197(a,1,2,1))]. given #144 (T,wt=9): 1510 (x ^ y) v (y ^ x) ' = 1. [para(57(a,1),210(a,1,2,1))]. given #145 (T,wt=11): 215 x v (y v (z ^ (x v y)) ') = 1. [para(209(a,1),13(a,1)),flip(a)]. given #146 (A,wt=13): 82 x ^ (y v ((x v z) ^ (x v u))) = x. [back_demod(51),demod(77(6)),flip(a)]. given #147 (F,wt=11): 221 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(24(a,1),209(a,1,2,1))]. given #148 (F,wt=11): 222 ((x v y) ^ z) v (x ^ z) ' = 1. [para(27(a,1),209(a,1,2,1))]. given #149 (T,wt=11): 225 x ^ (y v (z v (x v u))) = x. [para(13(a,1),77(a,1,2))]. given #150 (T,wt=11): 231 x v (y ^ (z ^ (x ^ u))) = x. [para(15(a,1),91(a,1,2))]. given #151 (A,wt=19): 93 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(24(a,1),20(b,1))]. given #152 (F,wt=11): 244 x ^ (y v (z v (u v x))) = x. [para(13(a,1),101(a,1,2,2))]. given #153 (F,wt=11): 256 x v (y ^ (z ^ (u ^ x))) = x. [para(15(a,1),110(a,1,2,2))]. given #154 (T,wt=11): 265 x v (y v (z v (x ' v u))) = 1. [para(13(a,1),118(a,1,2))]. given #155 (T,wt=11): 268 x v (y v ((x ^ z) ' v u)) = 1. [para(118(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #156 (A,wt=13): 94 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [back_demod(88),demod(90(7))]. given #157 (F,wt=11): 270 x ^ (y ^ (z ^ (x ' ^ u))) = 0. [para(15(a,1),133(a,1,2))]. given #158 (F,wt=11): 272 x ^ (y ^ ((x v z) ' ^ u)) = 0. [para(133(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #159 (T,wt=11): 281 (x ^ y) v (y ^ x) = x ^ y. [para(57(a,1),32(a,1,2))]. given #160 (T,wt=11): 284 x v (y v (z v (u v x '))) = 1. [para(13(a,1),135(a,1,2,2))]. given #161 (A,wt=13): 103 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(25(a,1),15(a,1)),flip(a)]. given #162 (F,wt=11): 287 x v (y v (z v (x ^ u) ')) = 1. [para(135(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #163 (F,wt=11): 289 x ^ (y ^ (z ^ (u ^ x '))) = 0. [para(15(a,1),139(a,1,2,2))]. given #164 (T,wt=11): 291 x ^ (y ^ (z ^ (x v u) ')) = 0. [para(139(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #165 (T,wt=11): 292 x v (y v ((y v x) ' v z)) = 1. [para(142(a,1),13(a,1,1)),demod(84(2),13(5)),flip(a)]. given #166 (A,wt=13): 104 x v y != 1 | 0 != y | y ' = x v y. [para(25(a,1),20(b,1)),demod(63(2)),flip(b)]. given #167 (F,wt=11): 297 x v (y v (z v (z v x) ')) = 1. [para(142(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #168 (F,wt=11): 299 x v (y v (y v (x ^ z)) ') = 1. [para(142(a,1),29(a,1,2)),demod(95(2)),flip(a)]. given #169 (T,wt=11): 303 x ^ ((y v (x v z)) ' ^ u) = 0. [para(23(a,1),154(a,1,2,1,1))]. given #170 (T,wt=11): 335 x v ((x v y) ' v (z v y)) = 1. [para(23(a,1),327(a,1,2)),demod(23(5))]. given #171 (A,wt=13): 105 x ^ (y v ((z v x) ^ (x v u))) = x. [para(25(a,1),21(a,1,2,2,1)),demod(77(6)),flip(a)]. given #172 (F,wt=11): 341 x ^ ((x ^ y) ' ^ (z ^ y)) = 0. [para(24(a,1),328(a,1,2)),demod(24(5))]. given #173 (F,wt=11): 347 x ^ (y ^ (z v (x v u)) ') = 0. [para(23(a,1),155(a,1,2,2,1))]. given #174 (T,wt=11): 391 x ^ (y v (z v (x v u))) ' = 0. [para(13(a,1),161(a,1,2,1))]. given #175 (T,wt=11): 395 x ^ (y v (z v (u v x))) ' = 0. [para(13(a,1),162(a,1,2,1,2))]. given #176 (A,wt=13): 106 (x v y) ^ (x v (z v y)) = x v y. [para(23(a,1),25(a,1,2))]. given #177 (F,wt=11): 396 x ^ ((y v (z v x)) ' ^ u) = 0. [para(162(a,1),15(a,1,1)),demod(87(2)),flip(a)]. given #178 (F,wt=11): 400 x ^ (y ^ (z v (u v x)) ') = 0. [para(162(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #179 (T,wt=11): 408 x ^ (y ^ ((z v x) ' ^ u)) = 0. [para(163(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #180 (T,wt=11): 412 x ^ (y ^ (z ^ (u v x) ')) = 0. [para(15(a,1),168(a,1,2))]. given #181 (A,wt=13): 109 x v (y v (z ^ (x v y))) = x v y. [para(31(a,1),13(a,1)),flip(a)]. given #182 (F,wt=11): 441 x ^ (y ^ ((y ^ x) ' ^ z)) = 0. [para(169(a,1),15(a,1,1)),demod(87(2),15(5)),flip(a)]. given #183 (F,wt=11): 445 x ^ (y ^ (z ^ (z ^ x) ')) = 0. [para(169(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #184 (T,wt=11): 447 x ^ (y ^ (y ^ (x v z)) ') = 0. [para(169(a,1),27(a,1,2)),demod(98(2)),flip(a)]. given #185 (T,wt=11): 454 x v ((y ^ (x ^ z)) ' v u) = 1. [para(24(a,1),203(a,1,2,1,1))]. given #186 (A,wt=13): 111 1 != x | y ^ x != 0 | x ' = y ^ x. [para(31(a,1),20(a,1)),demod(57(4)),flip(a)]. given #187 (F,wt=11): 461 x v (y v (z ^ (x ^ u)) ') = 1. [para(24(a,1),204(a,1,2,2,1))]. given #188 (F,wt=11): 467 x v (y ^ (z ^ (x ^ u))) ' = 1. [para(15(a,1),213(a,1,2,1))]. given #189 (T,wt=11): 524 x v ((y ^ (z ^ x)) ' v u) = 1. [para(15(a,1),214(a,1,2,1,1))]. given #190 (T,wt=11): 528 x v (y v ((z ^ x) ' v u)) = 1. [para(214(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #191 (A,wt=19): 112 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)). [para(31(a,1),21(a,1,2,2,2,2)),demod(76(5)),flip(a)]. given #192 (F,wt=11): 536 x v (y ^ (z ^ (u ^ x))) ' = 1. [para(15(a,1),216(a,1,2,1,2))]. given #193 (F,wt=11): 540 x v (y v (z ^ (u ^ x)) ') = 1. [para(216(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #194 (T,wt=11): 548 x v (y v (z v (u ^ x) ')) = 1. [para(13(a,1),220(a,1,2))]. given #195 (T,wt=11): 560 x ' v (y v (z v (x v u))) = 1. [para(13(a,1),329(a,1,2))]. given #196 (A,wt=13): 114 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(24(a,1),31(a,1,2))]. given #197 (F,wt=11): 623 x ' ^ (y ^ (z ^ (x ^ u))) = 0. [para(15(a,1),330(a,1,2))]. given #198 (F,wt=11): 629 x ' v (y v (z v (u v x))) = 1. [para(13(a,1),331(a,1,2,2))]. given #199 (T,wt=11): 636 (x ^ (y ^ z)) ' v (u v y) = 1. [para(91(a,1),331(a,1,2,2))]. given #200 (T,wt=11): 638 (x ^ (y ^ z)) ' v (u v z) = 1. [para(110(a,1),331(a,1,2,2))]. given #201 (A,wt=12): 116 x ^ (x ' v y) != 0 | x ' v y = x '. [para(85(a,1),20(a,1)),flip(c),xx(a)]. given #202 (F,wt=11): 646 x ' ^ (y ^ (z ^ (u ^ x))) = 0. [para(15(a,1),332(a,1,2,2))]. given #203 (F,wt=11): 655 (x v (y v z)) ' ^ (u ^ y) = 0. [para(77(a,1),332(a,1,2,2))]. given #204 (T,wt=11): 656 (x v (y v z)) ' ^ (u ^ z) = 0. [para(101(a,1),332(a,1,2,2))]. given #205 (T,wt=11): 662 (x ^ y) ' v (z v (x v u)) = 1. [para(630(a,1),13(a,1,1)),demod(84(2),13(5)),flip(a)]. given #206 (A,wt=17): 117 x ^ (y v (z ^ (x v (y ' v u)))) = x ^ (y v z). [para(85(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #207 (F,wt=11): 663 (x ^ y) ' v (z v (u v x)) = 1. [para(13(a,1),630(a,1,2))]. given #208 (F,wt=11): 696 (x ^ y) ' v (z v (y v u)) = 1. [para(634(a,1),13(a,1,1)),demod(84(2),13(5)),flip(a)]. given #209 (T,wt=11): 697 (x ^ y) ' v (z v (u v y)) = 1. [para(13(a,1),634(a,1,2))]. given #210 (T,wt=11): 711 (x v y) ' ^ (z ^ (x ^ u)) = 0. [para(647(a,1),15(a,1,1)),demod(87(2),15(5)),flip(a)]. given #211 (A,wt=13): 119 (x v y) ^ (y v (x v z)) = y v x. [para(12(a,1),26(a,1,1))]. given #212 (F,wt=11): 712 (x v y) ' ^ (z ^ (u ^ x)) = 0. [para(15(a,1),647(a,1,2))]. given #213 (F,wt=11): 721 (x v y) ' ^ (z ^ (y ^ u)) = 0. [para(651(a,1),15(a,1,1)),demod(87(2),15(5)),flip(a)]. given #214 (T,wt=11): 722 (x v y) ' ^ (z ^ (u ^ y)) = 0. [para(15(a,1),651(a,1,2))]. given #215 (T,wt=11): 806 (x v (y ^ z)) ^ (x v y) ' = 0. [para(78(a,1),156(a,1,2,1))]. given #216 (A,wt=13): 120 (x v y) ^ (y v (z v x)) = x v y. [para(12(a,1),26(a,1,2)),demod(13(3))]. given #217 (F,wt=11): 809 x v (y v (x v (y ^ z)) ') = 1. [para(78(a,1),327(a,1,2)),demod(12(5),13(5))]. given #218 (F,wt=11): 843 (x ^ (y v z)) v (x ^ y) ' = 1. [para(90(a,1),209(a,1,2,1))]. given #219 (T,wt=11): 845 x ^ (y ^ (x ^ (y v z)) ') = 0. [para(90(a,1),328(a,1,2)),demod(14(5),15(5))]. given #220 (T,wt=11): 860 x ^ (y ^ ((z v x) ^ y) ') = 0. [para(39(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #221 (A,wt=19): 121 (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 #222 (F,wt=11): 862 (x v y) ^ (z ^ y) = z ^ y. [para(57(a,1),102(a,2)),demod(187(4))]. given #223 (F,wt=11): 864 ((x v y) ^ z) v (y ^ z) ' = 1. [para(102(a,1),209(a,1,2,1))]. given #224 (T,wt=11): 869 x ^ (y ^ (y ^ (z v x)) ') = 0. [para(169(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #225 (T,wt=11): 886 (x ^ (y v z)) v (x ^ z) ' = 1. [para(107(a,1),209(a,1,2,1))]. given #226 (A,wt=17): 122 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(26(a,1),15(a,1,1)),flip(a)]. given #227 (F,wt=11): 890 x ^ (y ^ (x ^ (z v y)) ') = 0. [para(107(a,1),328(a,1,2)),demod(14(5),15(5))]. given #228 (F,wt=11): 910 x v (y v ((z ^ x) v y) ') = 1. [para(36(a,1),108(a,1,2)),demod(95(2)),flip(a)]. given #229 (T,wt=11): 912 ((x ^ y) v z) ^ (y v z) ' = 0. [para(108(a,1),156(a,1,2,1))]. given #230 (T,wt=11): 914 (x ^ y) v (z v y) = z v y. [para(63(a,1),108(a,2)),demod(192(4))]. given #231 (A,wt=19): 124 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(26(a,1),21(a,1,2,2,2)),demod(12(4),31(4),61(2)),flip(a)]. given #232 (F,wt=11): 918 x v (y v (y v (z ^ x)) ') = 1. [para(142(a,1),108(a,1,2)),demod(95(2)),flip(a)]. given #233 (F,wt=11): 984 (x v (y ^ z)) ^ (x v z) ' = 0. [para(113(a,1),156(a,1,2,1))]. given #234 (T,wt=11): 988 x v (y v (x v (z ^ y)) ') = 1. [para(113(a,1),327(a,1,2)),demod(12(5),13(5))]. given #235 (T,wt=11): 1085 x v (y v (z v (y v x) ')) = 1. [para(12(a,1),134(a,1,2,2,2,1))]. given #236 (A,wt=19): 125 (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 #237 (F,wt=11): 1097 x ^ (y ^ (z ^ (y ^ x) ')) = 0. [para(14(a,1),138(a,1,2,2,2,1))]. given #238 (F,wt=11): 1199 (x v y) ^ (y v (x v z)) ' = 0. [para(12(a,1),157(a,1,1))]. given #239 (T,wt=11): 1200 (x v y) ^ (y v (z v x)) ' = 0. [para(12(a,1),157(a,1,2,1)),demod(13(3))]. given #240 (T,wt=11): 1209 (x v y) ^ ((y v x) ' ^ z) = 0. [para(1204(a,1),15(a,1,1)),demod(87(2)),flip(a)]. given #241 (A,wt=15): 126 (x v y) ^ (x v (z v (y v u))) = x v y. [para(23(a,1),26(a,1,2,2))]. given #242 (F,wt=11): 1211 (x v y) ^ (z ^ (y v x) ') = 0. [para(1204(a,1),24(a,1,2)),demod(98(2)),flip(a)]. given #243 (F,wt=11): 1214 x ^ (y ^ ((y ^ x) v z) ') = 0. [para(14(a,1),158(a,1,2,2,1,1))]. given #244 (T,wt=11): 1223 x ^ (y ^ (z v (y ^ x)) ') = 0. [para(14(a,1),164(a,1,2,2,1,2))]. given #245 (T,wt=11): 1251 (x v y) ^ (z v (y v x)) ' = 0. [para(12(a,1),167(a,1,2,1)),demod(13(3))]. given #246 (A,wt=17): 127 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(26(a,1),24(a,1,2)),flip(a)]. given #247 (F,wt=11): 1291 x ^ (y ^ ((y v z) ^ x) ') = 0. [para(175(a,1),24(a,1)),flip(a)]. given #248 (F,wt=11): 1293 x ^ ((x v y) ^ (x v z)) ' = 0. [para(175(a,1),27(a,1)),flip(a)]. given #249 (T,wt=11): 1298 x ^ ((x v y) ^ (z v x)) ' = 0. [para(175(a,1),102(a,1)),flip(a)]. given #250 (T,wt=11): 1359 x v (y v (z ^ (y v x)) ') = 1. [para(194(a,1),216(a,1,2,1,2)),demod(13(5))]. given #251 (A,wt=21): 129 x v (y v z) != 1 | x v y != 0 | (x v y) ' = x v (y v z). [back_demod(123),demod(128(4))]. given #252 (F,wt=11): 1360 (x v y) ' ^ (z ^ (y v x)) = 0. [para(194(a,1),332(a,1,2,2))]. given #253 (F,wt=11): 1361 (x v y) ' v (z v (y v x)) = 1. [para(194(a,1),634(a,1,1,1))]. given #254 (T,wt=11): 1369 x v (y v ((y ^ z) v x) ') = 1. [para(205(a,1),23(a,1)),flip(a)]. given #255 (T,wt=11): 1372 x v ((x ^ y) v (x ^ z)) ' = 1. [para(205(a,1),29(a,1)),flip(a)]. given #256 (A,wt=12): 131 x v (x ' ^ y) != 1 | x ' ^ y = x '. [para(89(a,1),20(b,1)),flip(c),xx(b)]. given #257 (F,wt=11): 1377 x v ((x ^ y) v (z ^ x)) ' = 1. [para(205(a,1),108(a,1)),flip(a)]. given #258 (F,wt=11): 1384 (x v (y ^ z)) ^ (y v x) ' = 0. [para(12(a,1),206(a,1,1))]. given #259 (T,wt=11): 1385 ((x ^ y) v z) ^ (z v x) ' = 0. [para(12(a,1),206(a,1,2,1))]. given #260 (T,wt=11): 1387 (x v y) ' ^ ((x ^ z) v y) = 0. [para(206(a,1),14(a,1)),flip(a)]. given #261 (A,wt=23): 132 x ^ (y v (x ' ^ (z ^ (y v u)))) = x ^ (y v (x ' ^ (z ^ (x v u)))). [para(89(a,1),21(a,1,2,2,1)),demod(15(5),71(6),15(10))]. given #262 (F,wt=11): 1389 ((x ^ y) v (x ^ z)) ^ x ' = 0. [para(17(a,1),206(a,1,2,1))]. given #263 (F,wt=11): 1394 ((x ^ y) v (z ^ x)) ^ x ' = 0. [para(31(a,1),206(a,1,2,1))]. given #264 (T,wt=11): 1490 x v (y v ((y v x) ^ z) ') = 1. [para(12(a,1),208(a,1,2,2,1,1))]. given #265 (T,wt=11): 1504 (x ^ y) v (y ^ (x ^ z)) ' = 1. [para(14(a,1),210(a,1,1))]. given #266 (A,wt=12): 136 x ^ (y v x ') != 0 | y v x ' = x '. [para(96(a,1),20(a,1)),flip(c),xx(a)]. given #267 (F,wt=11): 1505 (x ^ y) v (y ^ (z ^ x)) ' = 1. [para(14(a,1),210(a,1,2,1)),demod(15(3))]. given #268 (F,wt=11): 1517 ((x v y) ^ z) v (z ^ x) ' = 1. [para(188(a,1),210(a,1,2,1))]. given #269 (T,wt=11): 1520 (x ^ y) v ((y ^ x) ' v z) = 1. [para(1510(a,1),13(a,1,1)),demod(84(2)),flip(a)]. given #270 (T,wt=11): 1524 (x ^ y) v (z v (y ^ x) ') = 1. [para(1510(a,1),23(a,1,2)),demod(95(2)),flip(a)]. given #271 (A,wt=17): 137 x ^ (y v (z ^ (x v (u v y ')))) = x ^ (y v z). [para(96(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #272 (F,wt=11): 1577 (x ^ y) v (z ^ (y ^ x)) ' = 1. [para(14(a,1),221(a,1,2,1)),demod(15(3))]. given #273 (F,wt=11): 1607 (x ^ y) ' v ((x v z) ^ y) = 1. [para(222(a,1),12(a,1)),flip(a)]. given #274 (T,wt=11): 1609 (x ^ (y v z)) v (y ^ x) ' = 1. [para(14(a,1),222(a,1,1))]. given #275 (T,wt=11): 1611 ((x v y) ^ (x v z)) v x ' = 1. [para(16(a,1),222(a,1,2,1))]. given #276 (A,wt=12): 140 x v (y ^ x ') != 1 | y ^ x ' = x '. [para(99(a,1),20(b,1)),flip(c),xx(b)]. given #277 (F,wt=11): 1617 ((x v y) ^ (z v x)) v x ' = 1. [para(25(a,1),222(a,1,2,1))]. given #278 (F,wt=11): 1854 (x ^ y) ' v (z v (y ^ x)) = 1. [para(281(a,1),331(a,1,2,2))]. given #279 (T,wt=11): 1855 (x ^ y) ' ^ (z ^ (y ^ x)) = 0. [para(281(a,1),651(a,1,1,1))]. given #280 (T,wt=11): 1968 x v ((y v x) ' v (z v y)) = 1. [para(36(a,1),297(a,1,2,2,2,1)),demod(83(5),40(5),13(5))]. given #281 (A,wt=23): 141 x ^ (y v (z ^ (x ' ^ (y v u)))) = x ^ (y v (z ^ (x ' ^ (x v u)))). [para(99(a,1),21(a,1,2,2,1)),demod(15(5),71(6),15(10))]. given #282 (F,wt=11): 1975 x v (y v ((z ^ y) v x) ') = 1. [para(108(a,1),297(a,1,2))]. given #283 (F,wt=11): 1997 x v ((y ^ x) v (x ^ z)) ' = 1. [para(299(a,1),108(a,1)),flip(a)]. given #284 (T,wt=11): 2093 x ^ ((y ^ x) ' ^ (z ^ y)) = 0. [para(14(a,1),341(a,1,2,1,1))]. given #285 (T,wt=11): 2304 x ^ (y ^ ((z v y) ^ x) ') = 0. [para(102(a,1),445(a,1,2))]. given #286 (A,wt=13): 143 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 #287 (F,wt=11): 2329 x ^ ((y v x) ^ (x v z)) ' = 0. [para(447(a,1),102(a,1)),flip(a)]. given #288 (F,wt=11): 3042 (x v y) ' ^ (x v (y ^ z)) = 0. [para(806(a,1),14(a,1)),flip(a)]. given #289 (T,wt=11): 3133 (x ^ y) ' v (x ^ (y v z)) = 1. [para(843(a,1),12(a,1)),flip(a)]. given #290 (T,wt=11): 3189 x ^ ((y v x) ^ (z v x)) ' = 0. [para(860(a,1),102(a,1)),flip(a)]. given #291 (A,wt=16): 144 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 #292 (F,wt=11): 3255 ((x v y) ^ z) v (z ^ y) ' = 1. [para(862(a,1),210(a,1,2,1))]. given #293 (F,wt=11): 3269 (x ^ y) ' v ((z v x) ^ y) = 1. [para(864(a,1),12(a,1)),flip(a)]. given #294 (T,wt=11): 3271 (x ^ (y v z)) v (z ^ x) ' = 1. [para(14(a,1),864(a,1,1))]. given #295 (T,wt=11): 3273 ((x v y) ^ (y v z)) v y ' = 1. [para(16(a,1),864(a,1,2,1))]. given #296 (A,wt=19): 145 x ^ (y v (z ^ (x v (u v (y v u) ')))) = x ^ (y v z). [para(36(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #297 (F,wt=11): 3279 ((x v y) ^ (z v y)) v y ' = 1. [para(25(a,1),864(a,1,2,1))]. given #298 (F,wt=11): 3345 (x ^ y) ' v (x ^ (z v y)) = 1. [para(886(a,1),12(a,1)),flip(a)]. given #299 (T,wt=11): 3491 x v ((y ^ x) v (z ^ x)) ' = 1. [para(910(a,1),108(a,1)),flip(a)]. given #300 (T,wt=11): 3513 (x v (y ^ z)) ^ (z v x) ' = 0. [para(12(a,1),912(a,1,1))]. given #301 (A,wt=13): 147 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 #302 (F,wt=11): 3514 ((x ^ y) v z) ^ (z v y) ' = 0. [para(12(a,1),912(a,1,2,1))]. given #303 (F,wt=11): 3516 (x v y) ' ^ ((z ^ x) v y) = 0. [para(912(a,1),14(a,1)),flip(a)]. given #304 (T,wt=11): 3518 ((x ^ y) v (y ^ z)) ^ y ' = 0. [para(17(a,1),912(a,1,2,1))]. given #305 (T,wt=11): 3523 ((x ^ y) v (z ^ y)) ^ y ' = 0. [para(31(a,1),912(a,1,2,1))]. given #306 (A,wt=17): 148 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(27(a,1),15(a,1)),demod(15(2)),flip(a)]. given #307 (F,wt=11): 3691 (x v y) ' ^ (x v (z ^ y)) = 0. [para(984(a,1),14(a,1)),flip(a)]. given #308 (F,wt=11): 4291 (x v y) ' ^ (y v (x ^ z)) = 0. [para(1384(a,1),14(a,1)),flip(a)]. given #309 (T,wt=11): 4326 (x v y) ' ^ ((y ^ z) v x) = 0. [para(1385(a,1),14(a,1)),flip(a)]. given #310 (T,wt=11): 4346 x ' ^ ((x ^ y) v (x ^ z)) = 0. [para(17(a,1),1387(a,1,1,1))]. given #311 (A,wt=21): 150 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(27(a,1),20(b,1))]. given #312 (F,wt=11): 4351 x ' ^ ((x ^ y) v (z ^ x)) = 0. [para(31(a,1),1387(a,1,1,1))]. given #313 (F,wt=11): 4551 x ^ ((x ' ^ y) v (x ' ^ z)) = 0. [para(308(a,1),1389(a,1,2)),demod(14(6))]. given #314 (T,wt=11): 4573 x ^ ((x ' ^ y) v (z ^ x ')) = 0. [para(308(a,1),1394(a,1,2)),demod(14(6))]. given #315 (T,wt=11): 4707 (x ^ y) ' v ((y v z) ^ x) = 1. [para(1517(a,1),12(a,1)),flip(a)]. given #316 (A,wt=13): 151 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(23(a,1),27(a,1,2,1))]. given #317 (F,wt=11): 4832 (x ^ y) ' v (y ^ (x v z)) = 1. [para(14(a,1),1607(a,1,2))]. given #318 (F,wt=11): 4834 x ' v ((x v y) ^ (x v z)) = 1. [para(16(a,1),1607(a,1,1,1))]. given #319 (T,wt=11): 4838 x ' v ((x v y) ^ (z v x)) = 1. [para(25(a,1),1607(a,1,1,1))]. given #320 (T,wt=11): 4939 x v ((x ' v y) ^ (x ' v z)) = 1. [para(308(a,1),1611(a,1,2)),demod(12(6))]. given #321 (A,wt=15): 152 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(27(a,1),24(a,1,2)),flip(a)]. given #322 (F,wt=11): 4965 x v ((x ' v y) ^ (z v x ')) = 1. [para(308(a,1),1617(a,1,2)),demod(12(6))]. given #323 (F,wt=11): 5488 (x ^ y) ' v ((z v y) ^ x) = 1. [para(3255(a,1),12(a,1)),flip(a)]. given #324 (T,wt=11): 5518 (x ^ y) ' v (y ^ (z v x)) = 1. [para(14(a,1),3269(a,1,2))]. given #325 (T,wt=11): 5520 x ' v ((y v x) ^ (x v z)) = 1. [para(16(a,1),3269(a,1,1,1))]. given #326 (A,wt=15): 153 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(27(a,1),31(a,1,2)),demod(12(4))]. given #327 (F,wt=11): 5524 x ' v ((y v x) ^ (z v x)) = 1. [para(25(a,1),3269(a,1,1,1))]. given #328 (F,wt=11): 5631 x v ((y v x ') ^ (x ' v z)) = 1. [para(308(a,1),3273(a,1,2)),demod(12(6))]. given #329 (T,wt=11): 5712 x v ((y v x ') ^ (z v x ')) = 1. [para(308(a,1),3279(a,1,2)),demod(12(6))]. given #330 (T,wt=11): 5805 (x v y) ' ^ (y v (z ^ x)) = 0. [para(3513(a,1),14(a,1)),flip(a)]. given #331 (A,wt=12): 159 x v (x v y) ' != 1 | (x v y) ' = x '. [para(149(a,1),20(b,1)),flip(c),xx(b)]. given #332 (F,wt=11): 5869 (x v y) ' ^ ((z ^ y) v x) = 0. [para(3514(a,1),14(a,1)),flip(a)]. given #333 (F,wt=11): 5911 x ' ^ ((y ^ x) v (x ^ z)) = 0. [para(17(a,1),3516(a,1,1,1))]. given #334 (T,wt=11): 5916 x ' ^ ((y ^ x) v (z ^ x)) = 0. [para(31(a,1),3516(a,1,1,1))]. given #335 (T,wt=11): 5949 x ^ ((y ^ x ') v (x ' ^ z)) = 0. [para(308(a,1),3518(a,1,2)),demod(14(6))]. given #336 (A,wt=23): 160 x ^ (y v ((x v z) ' ^ (y v u))) = x ^ (y v ((x v z) ' ^ (x v u))). [para(149(a,1),21(a,1,2,2,1)),demod(71(6))]. given #337 (F,wt=11): 5970 x ^ ((y ^ x ') v (z ^ x ')) = 0. [para(308(a,1),3523(a,1,2)),demod(14(6))]. given #338 (F,wt=12): 165 x v (y v x) ' != 1 | (y v x) ' = x '. [para(156(a,1),20(b,1)),flip(c),xx(b)]. given #339 (T,wt=12): 211 x ^ (x ^ y) ' != 0 | (x ^ y) ' = x '. [para(197(a,1),20(a,1)),flip(c),xx(a)]. given #340 (T,wt=12): 217 x ^ (y ^ x) ' != 0 | (y ^ x) ' = x '. [para(209(a,1),20(a,1)),flip(c),xx(a)]. given #341 (A,wt=23): 166 x ^ (y v ((z v x) ' ^ (y v u))) = x ^ (y v ((z v x) ' ^ (x v u))). [para(156(a,1),21(a,1,2,2,1)),demod(71(6))]. given #342 (F,wt=12): 312 x ^ (x ' v y) != 0 | (x ' v y) ' = x. [para(85(a,1),41(a,1)),demod(14(6)),xx(a)]. given #343 (F,wt=12): 313 x ^ (y v x ') != 0 | (y v x ') ' = x. [para(96(a,1),41(a,1)),demod(14(6)),xx(a)]. given #344 (T,wt=12): 318 x ^ (x ^ y) ' != 0 | x ^ y = x. [para(197(a,1),41(a,1)),demod(14(6),308(11)),xx(a)]. given #345 (T,wt=12): 319 x ^ (y ^ x) ' != 0 | y ^ x = x. [para(209(a,1),41(a,1)),demod(14(6),308(11)),xx(a)]. given #346 (A,wt=13): 170 x ^ (y ^ (z ^ (x ^ (y ^ z)) ')) = 0. [para(39(a,1),15(a,1)),demod(15(3)),flip(a)]. given #347 (F,wt=12): 333 x ' ^ (y v x) != 0 | y v x = x. [para(327(a,1),20(a,1)),demod(308(10)),flip(c),xx(a)]. given #348 (F,wt=12): 337 (x v y) ^ y ' != 0 | (x v y) ' = y '. [para(327(a,1),41(a,1)),xx(a)]. given #349 (T,wt=12): 338 x ' v (y ^ x) != 1 | y ^ x = x. [para(328(a,1),20(b,1)),demod(308(10)),flip(c),xx(b)]. given #350 (T,wt=12): 343 (x ^ y) v y ' != 1 | x ^ y = y. [para(328(a,1),41(b,1)),demod(308(10)),flip(c),xx(b)]. given #351 (A,wt=16): 171 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(39(a,1),20(b,1)),flip(c),xx(b)]. given #352 (F,wt=12): 365 (x v y) ^ x ' != 0 | (x v y) ' = x '. [para(96(a,1),42(a,1)),xx(a)]. given #353 (F,wt=12): 422 x v (x ' ^ y) != 1 | (x ' ^ y) ' = x. [para(89(a,1),43(b,1)),demod(12(3)),xx(b)]. given #354 (T,wt=12): 423 x v (y ^ x ') != 1 | (y ^ x ') ' = x. [para(99(a,1),43(b,1)),demod(12(3)),xx(b)]. given #355 (T,wt=12): 425 x v (x v y) ' != 1 | x v y = x. [para(149(a,1),43(b,1)),demod(12(3),308(11)),xx(b)]. given #356 (A,wt=25): 172 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ (x ^ (y v (z ^ (x v u)))) ') = 0. [para(21(a,1),39(a,1,2,2,1))]. given #357 (F,wt=12): 426 x v (y v x) ' != 1 | y v x = x. [para(156(a,1),43(b,1)),demod(12(3),308(11)),xx(b)]. given #358 (F,wt=12): 434 (x v y) ^ y ' != 0 | x v y = y. [para(327(a,1),43(a,1)),demod(308(10)),flip(c),xx(a)]. given #359 (T,wt=12): 435 (x ^ y) v y ' != 1 | (x ^ y) ' = y '. [para(328(a,1),43(b,1)),xx(b)]. given #360 (T,wt=12): 489 (x ^ y) v x ' != 1 | (x ^ y) ' = x '. [para(99(a,1),44(b,1)),xx(b)]. given #361 (A,wt=13): 174 x ^ (y ^ (z ^ (y ^ (x ^ z)) ')) = 0. [para(24(a,1),39(a,1,2,2,1)),demod(15(5))]. given #362 (F,wt=12): 1324 x ' ^ (x v y) != 0 | x v y = x. [para(85(a,1),80(a,1)),demod(308(10)),flip(c),xx(a)]. given #363 (F,wt=12): 1675 x ' v (x ^ y) != 1 | x ^ y = x. [para(89(a,1),93(b,1)),demod(308(10)),flip(c),xx(b)]. given #364 (T,wt=12): 2695 x ^ (y v x ') != 0 | x ' v y = x '. [para(12(a,1),116(a,1,2))]. given #365 (T,wt=12): 4233 x v (y ^ x ') != 1 | x ' ^ y = x '. [para(14(a,1),131(a,1,2))]. given #366 (A,wt=13): 177 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(55(a,1),15(a,2,2)),demod(24(3),15(2))]. given #367 (F,wt=12): 4642 x ^ (x ' v y) != 0 | y v x ' = x '. [para(12(a,1),136(a,1,2))]. given #368 (F,wt=12): 4949 x v (x ' ^ y) != 1 | y ^ x ' = x '. [para(14(a,1),140(a,1,2))]. given #369 (T,wt=12): 6765 x v (y v x) ' != 1 | (x v y) ' = x '. [para(12(a,1),159(a,1,2,1))]. given #370 (T,wt=12): 6902 x v (x v y) ' != 1 | (y v x) ' = x '. [para(12(a,1),165(a,1,2,1))]. given #371 (A,wt=13): 178 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(14(a,1),28(a,1,2,2,1))]. given #372 (F,wt=12): 6906 x ^ (y ^ x) ' != 0 | (x ^ y) ' = x '. [para(14(a,1),211(a,1,2,1))]. given #373 (F,wt=12): 6908 x ^ (x ^ y) ' != 0 | (y ^ x) ' = x '. [para(14(a,1),217(a,1,2,1))]. given #374 (T,wt=12): 6956 x ^ (y v x ') != 0 | (x ' v y) ' = x. [para(12(a,1),312(a,1,2))]. given #375 (T,wt=12): 6959 x ' ^ (x v y) != 0 | (x v y) ' = x '. [para(308(a,1),312(a,1,2,1)),demod(308(7))]. given #376 (A,wt=19): 179 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 #377 (F,wt=12): 6967 x ^ (x ' v y) != 0 | (y v x ') ' = x. [para(12(a,1),313(a,1,2))]. given #378 (F,wt=12): 6969 x ' ^ (y v x) != 0 | (y v x) ' = x '. [para(308(a,1),313(a,1,2,2)),demod(308(7))]. given #379 (T,wt=12): 6970 x ^ (y ^ x) ' != 0 | x ^ y = x. [para(14(a,1),318(a,1,2,1))]. given #380 (T,wt=12): 6973 x ^ (x ^ y) ' != 0 | y ^ x = x. [para(14(a,1),319(a,1,2,1))]. given #381 (A,wt=25): 180 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 #382 (F,wt=12): 6975 (x v y) ^ x ' != 0 | x v y = x. [para(16(a,1),319(a,1,2,1)),demod(16(7)),flip(b)]. given #383 (F,wt=12): 6985 x ' ^ (x v y) != 0 | y v x = x. [para(12(a,1),333(a,1,2))]. given #384 (T,wt=12): 6992 (x v y) ^ x ' != 0 | (y v x) ' = x '. [para(12(a,1),337(a,1,1))]. given #385 (T,wt=12): 6994 x ' v (x ^ y) != 1 | y ^ x = x. [para(14(a,1),338(a,1,2))]. given #386 (A,wt=15): 181 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(23(a,1),28(a,1,2,2))]. given #387 (F,wt=12): 7000 (x ^ y) v x ' != 1 | y ^ x = x. [para(14(a,1),343(a,1,1))]. given #388 (F,wt=12): 7003 (x v y) ^ y ' != 0 | (y v x) ' = y '. [para(12(a,1),365(a,1,1))]. given #389 (T,wt=12): 7006 x v (y ^ x ') != 1 | (x ' ^ y) ' = x. [para(14(a,1),422(a,1,2))]. given #390 (T,wt=12): 7008 x ' v (x ^ y) != 1 | (x ^ y) ' = x '. [para(308(a,1),422(a,1,2,1)),demod(308(7))]. given #391 (A,wt=17): 182 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(28(a,1),24(a,1,2)),flip(a)]. given #392 (F,wt=12): 7010 x v (x ' ^ y) != 1 | (y ^ x ') ' = x. [para(14(a,1),423(a,1,2))]. given #393 (F,wt=12): 7011 x ' v (y ^ x) != 1 | (y ^ x) ' = x '. [para(308(a,1),423(a,1,2,2)),demod(308(7))]. given #394 (T,wt=12): 7012 x v (y v x) ' != 1 | x v y = x. [para(12(a,1),425(a,1,2,1))]. given #395 (T,wt=12): 7041 x v (x v y) ' != 1 | y v x = x. [para(12(a,1),426(a,1,2,1))]. given #396 (A,wt=19): 183 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 #397 (F,wt=12): 7043 (x ^ y) v x ' != 1 | x ^ y = x. [para(17(a,1),426(a,1,2,1)),demod(17(7)),flip(b)]. given #398 (F,wt=12): 7047 (x v y) ^ x ' != 0 | y v x = x. [para(12(a,1),434(a,1,1))]. given #399 (T,wt=12): 7049 (x ^ y) v x ' != 1 | (y ^ x) ' = x '. [para(14(a,1),435(a,1,1))]. given #400 (T,wt=12): 7051 (x ^ y) v y ' != 1 | (y ^ x) ' = y '. [para(14(a,1),489(a,1,1))]. given #401 (A,wt=19): 184 (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 #402 (F,wt=12): 7067 x ' ^ (y v x) != 0 | x v y = x. [para(12(a,1),1324(a,1,2))]. given #403 (F,wt=12): 7082 x ' v (y ^ x) != 1 | x ^ y = x. [para(14(a,1),1675(a,1,2))]. given #404 (T,wt=12): 7194 x ' ^ (y v x) != 0 | (x v y) ' = x '. [para(308(a,1),6956(a,1,2,2)),demod(308(7))]. given #405 (T,wt=12): 7276 x ' ^ (x v y) != 0 | (y v x) ' = x '. [para(308(a,1),6967(a,1,2,1)),demod(308(7))]. given #406 (A,wt=15): 185 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(28(a,1),27(a,1,2)),demod(27(3)),flip(a)]. given #407 (F,wt=12): 7296 (x v y) ^ y ' != 0 | y v x = y. [para(12(a,1),6975(a,1,1))]. given #408 (F,wt=12): 7366 x ' v (y ^ x) != 1 | (x ^ y) ' = x '. [para(308(a,1),7006(a,1,2,2)),demod(308(7))]. given #409 (T,wt=12): 7486 x ' v (x ^ y) != 1 | (y ^ x) ' = x '. [para(308(a,1),7010(a,1,2,1)),demod(308(7))]. given #410 (T,wt=12): 7522 (x ^ y) v y ' != 1 | y ^ x = y. [para(14(a,1),7043(a,1,1))]. given #411 (A,wt=13): 187 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(15(a,1),57(a,1,2)),demod(15(5))]. given #412 (F,wt=13): 189 x v (y v (x v z)) = y v (x v z). [para(61(a,1),13(a,2,2)),demod(23(3),13(2))]. given #413 (F,wt=13): 192 x v (y v (z v x)) = y v (z v x). [para(13(a,1),63(a,1,2)),demod(13(5))]. given #414 (T,wt=13): 201 x v ((y ^ (x ^ z)) v u) = x v u. [para(24(a,1),29(a,1,2,1))]. given #415 (T,wt=13): 223 (x ^ ((y ^ x) v z)) v (y ^ x) ' = 1. [para(28(a,1),209(a,1,2,1))]. given #416 (A,wt=21): 190 x ^ (y v (z ^ (x v (y v u)))) = x ^ (y v (z ^ (x v u))). [para(61(a,1),21(a,1,2,2,2,2)),demod(21(6)),flip(a)]. given #417 (F,wt=13): 228 x ^ (y ^ (z v (x v u))) = y ^ x. [para(77(a,1),24(a,1,2)),flip(a)]. given #418 (F,wt=13): 234 x v (y v (z ^ (x ^ u))) = y v x. [para(91(a,1),23(a,1,2)),flip(a)]. given #419 (T,wt=13): 235 x v (y v ((y v x) ^ z)) = x v y. [para(12(a,1),30(a,1,2,2,1))]. given #420 (T,wt=13): 242 (x v ((y v x) ^ z)) ^ (y v x) ' = 0. [para(30(a,1),156(a,1,2,1))]. given #421 (A,wt=21): 193 x ^ (y v (z ^ (x v (u v y)))) = x ^ (y v (z ^ (x v u))). [para(63(a,1),21(a,1,2,2,2,2)),demod(47(6)),flip(a)]. given #422 (F,wt=13): 245 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(101(a,1),15(a,1,1)),flip(a)]. given #423 (F,wt=13): 251 x ^ (y ^ (z v (u v x))) = y ^ x. [para(101(a,1),24(a,1,2)),flip(a)]. given #424 (T,wt=13): 254 x v ((y ^ (z ^ x)) v u) = x v u. [para(110(a,1),13(a,1,1)),flip(a)]. given #425 (T,wt=13): 259 x v (y v (z ^ (u ^ x))) = y v x. [para(110(a,1),23(a,1,2)),flip(a)]. given #426 (A,wt=17): 195 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 #427 (F,wt=13): 264 x v (y v (z v ((x v y) ' v u))) = 1. [para(118(a,1),13(a,1)),flip(a)]. given #428 (F,wt=13): 269 x ^ (y ^ (z ^ ((x ^ y) ' ^ u))) = 0. [para(133(a,1),15(a,1)),flip(a)]. given #429 (T,wt=13): 273 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(14(a,1),32(a,1,1))]. given #430 (T,wt=13): 274 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(14(a,1),32(a,1,2)),demod(15(3))]. given #431 (A,wt=17): 196 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(15(a,1),29(a,1,2,1))]. given #432 (F,wt=13): 283 x v (y v (z v (u v (x v y) '))) = 1. [para(135(a,1),13(a,1)),flip(a)]. given #433 (F,wt=13): 288 x ^ (y ^ (z ^ (u ^ (x ^ y) '))) = 0. [para(139(a,1),15(a,1)),flip(a)]. given #434 (T,wt=13): 293 x v (y v (z v (z v (x v y)) ')) = 1. [para(142(a,1),13(a,1)),flip(a)]. given #435 (T,wt=13): 294 x v (y v (z v (y v (z v x)) ')) = 1. [para(13(a,1),142(a,1,2,2,1)),demod(13(5))]. given #436 (A,wt=21): 198 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x ' = (x ^ z) v y. [para(29(a,1),20(a,1))]. given #437 (F,wt=13): 298 x v (y v (z v (x v (z v y)) ')) = 1. [para(23(a,1),142(a,1,2,2,1)),demod(13(6))]. given #438 (F,wt=13): 300 (x v y) ^ ((x v (y v z)) ' ^ u) = 0. [para(13(a,1),154(a,1,2,1,1))]. given #439 (T,wt=13): 301 x ^ (y ^ (((x ^ y) v z) ' ^ u)) = 0. [para(154(a,1),15(a,1)),flip(a)]. given #440 (T,wt=13): 305 x v y != 1 | x ^ y != 0 | y ' = x. [para(14(a,1),41(b,1))]. given #441 (A,wt=23): 199 x ^ (y v (z ^ (x v ((y ^ u) v v)))) = x ^ (y v (z ^ (x v v))). [para(29(a,1),21(a,1,2,2,2,2)),demod(21(6)),flip(a)]. given #442 (F,wt=13): 307 1 != x | x ^ y != 0 | (x ^ y) ' = x. [para(17(a,1),41(a,1)),demod(14(4),55(4)),flip(a)]. given #443 (F,wt=13): 311 1 != x | y ^ x != 0 | (y ^ x) ' = x. [para(31(a,1),41(a,1)),demod(14(4),57(4)),flip(a)]. given #444 (T,wt=13): 315 x v y != 1 | 0 != x | (x v y) ' = x. [para(61(a,1),41(a,1)),demod(14(5),16(5)),flip(b)]. given #445 (T,wt=13): 316 x v y != 1 | 0 != y | (x v y) ' = y. [para(63(a,1),41(a,1)),demod(14(5),25(5)),flip(b)]. given #446 (A,wt=15): 200 x v (y v ((x ^ z) v u)) = y v (x v u). [para(29(a,1),23(a,1,2)),flip(a)]. given #447 (F,wt=13): 336 x v (y v (y v ((x v y) ^ z)) ') = 1. [para(30(a,1),327(a,1,2)),demod(12(6),13(6))]. given #448 (F,wt=13): 342 x ^ (y ^ (y ^ ((x ^ y) v z)) ') = 0. [para(28(a,1),328(a,1,2)),demod(14(6),15(6))]. given #449 (T,wt=13): 344 (x v y) ^ (z ^ (x v (y v u)) ') = 0. [para(13(a,1),155(a,1,2,2,1))]. given #450 (T,wt=13): 345 x ^ (y ^ (z ^ ((x ^ y) v u) ')) = 0. [para(155(a,1),15(a,1)),flip(a)]. given #451 (A,wt=15): 202 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(29(a,1),25(a,1,2)),demod(14(4))]. given #452 (F,wt=13): 375 x v y != 1 | 0 != y | (y v x) ' = y. [para(63(a,1),42(a,1)),demod(14(5),16(5)),flip(b)]. given #453 (F,wt=13): 390 (x v y) ^ (z v (x v (y v u))) ' = 0. [para(13(a,1),161(a,1,2,1,2))]. given #454 (T,wt=13): 392 x ^ (y ^ (z v ((x ^ y) v u)) ') = 0. [para(161(a,1),15(a,1)),flip(a)]. given #455 (T,wt=13): 397 x ^ (y ^ (z v (u v (x ^ y))) ') = 0. [para(162(a,1),15(a,1)),flip(a)]. given #456 (A,wt=17): 212 x ^ (y v (z ^ (x v (y ^ u) '))) = x ^ (y v z). [para(197(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #457 (F,wt=13): 399 (x v y) ^ (z v (x v (u v y))) ' = 0. [para(23(a,1),162(a,1,2,1,2))]. given #458 (F,wt=13): 401 ((x ^ y) v z) ^ (u v (x v z)) ' = 0. [para(29(a,1),162(a,1,2,1,2))]. given #459 (T,wt=13): 403 x ^ (y ^ (z ^ (u v (x ^ y)) ')) = 0. [para(32(a,1),162(a,1,2,1,2)),demod(15(6),15(5))]. given #460 (T,wt=13): 405 x ^ (y ^ ((z v (x ^ y)) ' ^ u)) = 0. [para(163(a,1),15(a,1)),flip(a)]. given #461 (A,wt=17): 218 x ^ (y v (z ^ (x v (u ^ y) '))) = x ^ (y v z). [para(209(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #462 (F,wt=13): 407 (x v y) ^ ((x v (z v y)) ' ^ u) = 0. [para(23(a,1),163(a,1,2,1,1))]. given #463 (F,wt=13): 409 ((x ^ y) v z) ^ ((x v z) ' ^ u) = 0. [para(29(a,1),163(a,1,2,1,1))]. given #464 (T,wt=13): 414 (x v y) ^ (z ^ (x v (u v y)) ') = 0. [para(23(a,1),168(a,1,2,2,1))]. given #465 (T,wt=13): 415 ((x ^ y) v z) ^ (u ^ (x v z) ') = 0. [para(29(a,1),168(a,1,2,2,1))]. given #466 (A,wt=23): 219 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u)))) ')) = 1. [para(21(a,1),209(a,1,2,1)),demod(13(11),13(10))]. given #467 (F,wt=13): 442 x ^ (y ^ (z ^ (z ^ (x ^ y)) ')) = 0. [para(169(a,1),15(a,1)),flip(a)]. given #468 (F,wt=13): 443 x ^ (y ^ (z ^ (y ^ (z ^ x)) ')) = 0. [para(15(a,1),169(a,1,2,2,1)),demod(15(5))]. given #469 (T,wt=13): 446 x ^ (y ^ (z ^ (x ^ (z ^ y)) ')) = 0. [para(24(a,1),169(a,1,2,2,1)),demod(15(6))]. given #470 (T,wt=13): 450 x v (y v (((x v y) ^ z) ' v u)) = 1. [para(203(a,1),13(a,1)),flip(a)]. given #471 (A,wt=15): 224 (x v y) ^ (z v (x v (y v u))) = x v y. [para(13(a,1),77(a,1,2,2))]. given #472 (F,wt=13): 451 (x ^ y) v ((x ^ (y ^ z)) ' v u) = 1. [para(15(a,1),203(a,1,2,1,1))]. given #473 (F,wt=13): 457 x v (y v (z v ((x v y) ^ u) ')) = 1. [para(204(a,1),13(a,1)),flip(a)]. given #474 (T,wt=13): 458 (x ^ y) v (z v (x ^ (y ^ u)) ') = 1. [para(15(a,1),204(a,1,2,2,1))]. given #475 (T,wt=13): 465 x v (y v (z ^ ((x v y) ^ u)) ') = 1. [para(213(a,1),13(a,1)),flip(a)]. given #476 (A,wt=17): 226 x v (y v z) != 1 | 0 != y | y ' = x v (y v z). [para(77(a,1),20(b,1)),demod(189(3)),flip(b)]. given #477 (F,wt=13): 466 (x ^ y) v (z ^ (x ^ (y ^ u))) ' = 1. [para(15(a,1),213(a,1,2,1,2))]. given #478 (F,wt=13): 497 1 != x | y ^ x != 0 | (x ^ y) ' = x. [para(57(a,1),44(b,1)),demod(12(2),17(2)),flip(a)]. given #479 (T,wt=13): 523 x v (y v ((z ^ (x v y)) ' v u)) = 1. [para(214(a,1),13(a,1)),flip(a)]. given #480 (T,wt=13): 529 (x ^ y) v ((x ^ (z ^ y)) ' v u) = 1. [para(24(a,1),214(a,1,2,1,1))]. given #481 (A,wt=15): 227 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(77(a,1),21(a,1,2,2,1)),demod(77(7)),flip(a)]. given #482 (F,wt=13): 530 ((x v y) ^ z) v ((x ^ z) ' v u) = 1. [para(27(a,1),214(a,1,2,1,1))]. given #483 (F,wt=13): 535 x v (y v (z ^ (u ^ (x v y))) ') = 1. [para(216(a,1),13(a,1)),flip(a)]. given #484 (T,wt=13): 541 (x ^ y) v (z ^ (x ^ (u ^ y))) ' = 1. [para(24(a,1),216(a,1,2,1,2))]. given #485 (T,wt=13): 542 x v (y v (z v (u ^ (x v y)) ')) = 1. [para(26(a,1),216(a,1,2,1,2)),demod(13(6),13(5))]. given #486 (A,wt=15): 229 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(91(a,1),13(a,1)),flip(a)]. given #487 (F,wt=13): 543 ((x v y) ^ z) v (u ^ (x ^ z)) ' = 1. [para(27(a,1),216(a,1,2,1,2))]. given #488 (F,wt=13): 552 (x ^ y) v (z v (x ^ (u ^ y)) ') = 1. [para(24(a,1),220(a,1,2,2,1))]. given #489 (T,wt=13): 553 ((x v y) ^ z) v (u v (x ^ z) ') = 1. [para(27(a,1),220(a,1,2,2,1))]. given #490 (T,wt=13): 559 (x v y) ' v (z v (x v (y v u))) = 1. [para(13(a,1),329(a,1,2,2))]. given #491 (A,wt=15): 230 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(15(a,1),91(a,1,2,2))]. given #492 (F,wt=13): 622 (x ^ y) ' ^ (z ^ (x ^ (y ^ u))) = 0. [para(15(a,1),330(a,1,2,2))]. given #493 (F,wt=13): 633 (x v y) ' v (z v (x v (u v y))) = 1. [para(23(a,1),331(a,1,2,2))]. given #494 (T,wt=13): 635 ((x ^ y) v z) ' v (u v (x v z)) = 1. [para(29(a,1),331(a,1,2,2))]. given #495 (T,wt=13): 639 (x ^ (y ^ z)) ' v (u v (x ^ y)) = 1. [para(32(a,1),331(a,1,2,2))]. given #496 (A,wt=17): 232 1 != x | y ^ (x ^ z) != 0 | x ' = y ^ (x ^ z). [para(91(a,1),20(a,1)),demod(177(5)),flip(a)]. given #497 (F,wt=13): 650 (x ^ y) ' ^ (z ^ (x ^ (u ^ y))) = 0. [para(24(a,1),332(a,1,2,2))]. given #498 (F,wt=13): 652 (x v (y v z)) ' ^ (u ^ (x v y)) = 0. [para(26(a,1),332(a,1,2,2))]. given #499 (T,wt=13): 653 ((x v y) ^ z) ' ^ (u ^ (x ^ z)) = 0. [para(27(a,1),332(a,1,2,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 117 (0.00 of 6.84 sec). given #500 (T,wt=13): 666 x v (((x v y) ^ z) ' v (u v y)) = 1. [para(23(a,1),630(a,1,2)),demod(23(6))]. given #501 (A,wt=19): 236 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 #502 (F,wt=13): 667 x v (y v (((x ^ z) v y) ^ u) ') = 1. [para(29(a,1),630(a,1,2)),demod(12(6),13(6))]. given #503 (F,wt=13): 675 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(71(a,1),48(a,1,2,2,1,2)),demod(71(5),71(8),90(7))]. given #504 (T,wt=13): 701 x v ((y ^ (x v z)) ' v (u v z)) = 1. [para(23(a,1),634(a,1,2)),demod(23(6))]. given #505 (T,wt=13): 702 (x ^ (y ^ z)) ' v (u v (x ^ z)) = 1. [para(24(a,1),634(a,1,1,1))]. given #506 (A,wt=25): 237 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 #507 (F,wt=13): 703 (x ^ y) ' v (z v ((x v u) ^ y)) = 1. [para(27(a,1),634(a,1,1,1))]. given #508 (F,wt=13): 705 x v (y v (z ^ ((x ^ u) v y)) ') = 1. [para(29(a,1),634(a,1,2)),demod(12(6),13(6))]. given #509 (T,wt=13): 715 x ^ (((x ^ y) v z) ' ^ (u ^ y)) = 0. [para(24(a,1),647(a,1,2)),demod(24(6))]. given #510 (T,wt=13): 716 x ^ (y ^ (((x v z) ^ y) v u) ') = 0. [para(27(a,1),647(a,1,2)),demod(14(6),15(6))]. given #511 (A,wt=25): 238 x ^ (y v (z ^ (x v (u v ((y v u) ^ v))))) = x ^ (y v (z ^ (x v u))). [para(30(a,1),21(a,1,2,2,2,2)),demod(21(6)),flip(a)]. given #512 (F,wt=13): 725 (x v (y v z)) ' ^ (u ^ (x v z)) = 0. [para(23(a,1),651(a,1,1,1))]. given #513 (F,wt=13): 726 x ^ ((y v (x ^ z)) ' ^ (u ^ z)) = 0. [para(24(a,1),651(a,1,2)),demod(24(6))]. given #514 (T,wt=13): 727 x ^ (y ^ (z v ((x v u) ^ y)) ') = 0. [para(27(a,1),651(a,1,2)),demod(14(6),15(6))]. given #515 (T,wt=13): 729 (x v y) ' ^ (z ^ ((x ^ u) v y)) = 0. [para(29(a,1),651(a,1,1,1))]. given #516 (A,wt=17): 239 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 #517 (F,wt=13): 740 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(71(a,1),49(a,1,2,2,2,2)),demod(71(5),71(8),90(7))]. given #518 (F,wt=13): 772 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(71(a,1),50(a,1,2,2,2,1)),demod(71(5),71(8),90(7))]. given #519 (T,wt=13): 811 (x v (y ^ z)) ^ (u v (x v y)) ' = 0. [para(78(a,1),162(a,1,2,1,2))]. given #520 (T,wt=13): 812 (x v (y ^ z)) ^ ((x v y) ' ^ u) = 0. [para(78(a,1),163(a,1,2,1,1))]. given #521 (A,wt=19): 240 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 #522 (F,wt=13): 813 (x v (y ^ z)) ^ (u ^ (x v y) ') = 0. [para(78(a,1),168(a,1,2,2,1))]. given #523 (F,wt=13): 814 (x v (y ^ z)) ' v (u v (x v y)) = 1. [para(78(a,1),331(a,1,2,2))]. given #524 (T,wt=13): 815 x v (y v ((x v (y ^ z)) ^ u) ') = 1. [para(78(a,1),630(a,1,2)),demod(12(6),13(6))]. given #525 (T,wt=13): 816 x v (y v (z ^ (x v (y ^ u))) ') = 1. [para(78(a,1),634(a,1,2)),demod(12(6),13(6))]. given #526 (A,wt=19): 241 (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 #527 (F,wt=13): 817 (x v y) ' ^ (z ^ (x v (y ^ u))) = 0. [para(78(a,1),651(a,1,1,1))]. given #528 (F,wt=13): 826 x ' ^ (x v (y ^ x ')) = x ' ^ (x v y). [para(34(a,1),53(a,1,2,2,2))]. given #529 (T,wt=9): 10458 x ' ^ (x v (x ' v y) ') = 0. [para(160(a,1),826(a,2)),demod(14(8),154(8),40(3),14(2),19(2),2824(10)),flip(a)]. given #530 (T,wt=7): 10472 x v (x ' v y) ' = x. [hyper(6985,a,10458,a),demod(12(4))]. given #531 (A,wt=15): 243 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 #532 (F,wt=7): 10482 x v (y v x ') ' = x. [para(12(a,1),10472(a,1,2,1))]. given #533 (F,wt=7): 10492 x ' v (x v y) ' = x '. [para(308(a,1),10472(a,1,2,1,1))]. given #534 (T,wt=7): 10619 x ' v (y v x) ' = x '. [para(308(a,1),10482(a,1,2,1,2))]. given #535 (T,wt=9): 10487 x v (y v (x ' v z)) ' = x. [para(23(a,1),10472(a,1,2,1))]. given #536 (A,wt=15): 246 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(101(a,1),15(a,1)),flip(a)]. given #537 (F,wt=9): 10488 x ^ (x ' v y) ' = (x ' v y) '. [para(10472(a,1),25(a,1,2)),demod(14(4))]. given #538 (F,wt=9): 10489 x v ((x ^ y) ' v z) ' = x. [para(10472(a,1),29(a,1,2)),demod(17(2)),flip(a)]. given #539 (T,wt=9): 10493 (x ' v y) ' ^ (z v x) ' = 0. [para(10472(a,1),162(a,1,2,1,2))]. given #540 (T,wt=9): 10495 x v ((x ' v y) ' ^ z) ' = 1. [para(10472(a,1),630(a,1,2)),demod(12(6))]. given #541 (A,wt=17): 247 x v (y v z) != 1 | 0 != z | z ' = x v (y v z). [para(101(a,1),20(b,1)),demod(192(3)),flip(b)]. given #542 (F,wt=9): 10496 x v (y ^ (x ' v z) ') ' = 1. [para(10472(a,1),634(a,1,2)),demod(12(6))]. given #543 (F,wt=9): 10499 x v ((y ^ x) ' v z) ' = x. [para(10472(a,1),108(a,1,2)),demod(31(2)),flip(a)]. given #544 (T,wt=9): 10503 x v ((x ' v y) ' ^ z) = x. [para(10472(a,1),207(a,1,2)),demod(12(5),10472(9))]. given #545 (T,wt=9): 10524 x v (y ^ (x ' v z) ') = x. [para(10472(a,1),914(a,1,2)),demod(12(5),10472(9))]. low water: id=6724, wt=24 given #546 (A,wt=15): 248 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(101(a,1),21(a,1,2,2,1)),demod(77(7)),flip(a)]. given #547 (F,wt=9): 10545 x v (y v (z v x ')) ' = x. [para(192(a,1),10472(a,1,2,1))]. low water: id=7273, wt=23 given #548 (F,wt=9): 10615 x ^ (y v x ') ' = (y v x ') '. [para(10482(a,1),25(a,1,2)),demod(14(4))]. given #549 (T,wt=9): 10616 x v (y v (x ^ z) ') ' = x. [para(10482(a,1),29(a,1,2)),demod(17(2)),flip(a)]. given #550 (T,wt=9): 10620 (x v y ') ' ^ (z v y) ' = 0. [para(10482(a,1),162(a,1,2,1,2))]. given #551 (A,wt=15): 250 (x v y) ^ (z v (x v (u v y))) = x v y. [para(23(a,1),101(a,1,2,2))]. given #552 (F,wt=9): 10622 x v ((y v x ') ' ^ z) ' = 1. [para(10482(a,1),630(a,1,2)),demod(12(6))]. given #553 (F,wt=9): 10623 x v (y ^ (z v x ') ') ' = 1. [para(10482(a,1),634(a,1,2)),demod(12(6))]. low water: id=8280, wt=21 given #554 (T,wt=9): 10626 x v (y v (z ^ x) ') ' = x. [para(10482(a,1),108(a,1,2)),demod(31(2)),flip(a)]. given #555 (T,wt=9): 10631 x v ((y v x ') ' ^ z) = x. [para(10482(a,1),207(a,1,2)),demod(12(5),10482(9))]. given #556 (A,wt=17): 252 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(29(a,1),101(a,1,2,2))]. given #557 (F,wt=9): 10652 x v (y ^ (z v x ') ') = x. [para(10482(a,1),914(a,1,2)),demod(12(5),10482(9))]. given #558 (F,wt=9): 10699 x ' v (y v (x v z)) ' = x '. [para(23(a,1),10492(a,1,2,1))]. given #559 (T,wt=9): 10700 x ' ^ (x v y) ' = (x v y) '. [para(10492(a,1),25(a,1,2)),demod(14(4))]. given #560 (T,wt=9): 10703 (x v y) ' ^ (z v x ') ' = 0. [para(10492(a,1),162(a,1,2,1,2))]. given #561 (A,wt=21): 253 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(30(a,1),101(a,1,2,2))]. given #562 (F,wt=9): 10705 x ' v ((x v y) ' ^ z) ' = 1. [para(10492(a,1),630(a,1,2)),demod(12(6))]. given #563 (F,wt=9): 10706 x ' v (y ^ (x v z) ') ' = 1. [para(10492(a,1),634(a,1,2)),demod(12(6))]. given #564 (T,wt=9): 10709 x ' != 1 | x ' != 0 | x ' = x. [para(10492(a,1),66(a,1)),demod(308(8),10492(10)),flip(b),flip(c)]. given #565 (T,wt=9): 10714 x ' v ((x v y) ' ^ z) = x '. [para(10492(a,1),207(a,1,2)),demod(12(5),10492(9))]. low water: id=8678, wt=20 given #566 (A,wt=15): 255 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(110(a,1),13(a,1)),flip(a)]. given #567 (F,wt=9): 10736 x ' v (y ^ (x v z) ') = x '. [para(10492(a,1),914(a,1,2)),demod(12(5),10492(9))]. given #568 (F,wt=9): 10762 x ' v (y v (z v x)) ' = x '. [para(192(a,1),10492(a,1,2,1))]. given #569 (T,wt=9): 10788 x ' v (x ^ y) ' = (x ^ y) '. [para(17(a,1),10619(a,1,2,1)),demod(12(4))]. low water: id=9736, wt=19 given #570 (T,wt=7): 11936 x ' ^ (x ^ y) ' = x '. [para(10788(a,1),16(a,1,2))]. given #571 (A,wt=17): 257 1 != x | y ^ (z ^ x) != 0 | x ' = y ^ (z ^ x). [para(110(a,1),20(a,1)),demod(187(5)),flip(a)]. given #572 (F,wt=7): 12019 x ' ^ (y ^ x) ' = x '. [para(14(a,1),11936(a,1,2,1))]. given #573 (F,wt=7): 12023 x ^ (x ' ^ y) ' = x. [para(308(a,1),11936(a,1,1)),demod(308(6))]. given #574 (T,wt=7): 12066 x ^ (y ^ x ') ' = x. [para(308(a,1),12019(a,1,1)),demod(308(6))]. given #575 (T,wt=9): 10792 x ' ^ (y v x) ' = (y v x) '. [para(10619(a,1),25(a,1,2)),demod(14(4))]. given #576 (A,wt=15): 260 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(24(a,1),110(a,1,2,2))]. given #577 (F,wt=9): 10793 x ' v (y ^ x) ' = (y ^ x) '. [para(31(a,1),10619(a,1,2,1)),demod(12(4))]. given #578 (F,wt=9): 10800 (x v y) ' ^ (z v y ') ' = 0. [para(10619(a,1),162(a,1,2,1,2))]. given #579 (T,wt=9): 10802 x ' v ((y v x) ' ^ z) ' = 1. [para(10619(a,1),630(a,1,2)),demod(12(6))]. given #580 (T,wt=9): 10803 x ' v (y ^ (z v x) ') ' = 1. [para(10619(a,1),634(a,1,2)),demod(12(6))]. given #581 (A,wt=17): 261 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(26(a,1),110(a,1,2,2)),demod(13(5),13(4))]. given #582 (F,wt=9): 10813 x ' v ((y v x) ' ^ z) = x '. [para(10619(a,1),207(a,1,2)),demod(12(5),10619(9))]. given #583 (F,wt=9): 10835 x ' v (y ^ (z v x) ') = x '. [para(10619(a,1),914(a,1,2)),demod(12(5),10619(9))]. given #584 (T,wt=9): 10934 x ^ (y ' v (x ^ y)) ' = 0. [para(10488(a,1),164(a,1,2))]. given #585 (T,wt=9): 10943 x ^ (y ' v (y ^ x)) ' = 0. [para(10488(a,1),1223(a,1,2))]. given #586 (A,wt=17): 262 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(27(a,1),110(a,1,2,2))]. given #587 (F,wt=9): 10990 x ' ^ ((x ^ y) ' v z) ' = 0. [para(10489(a,1),156(a,1,2,1)),demod(14(6))]. given #588 (F,wt=9): 11050 (x ' v y) ' ^ (x v z) ' = 0. [para(12(a,1),10493(a,1,2,1))]. given #589 (T,wt=9): 11051 (x v y) ' ^ (y ' v z) ' = 0. [para(10493(a,1),14(a,1)),flip(a)]. given #590 (T,wt=9): 11054 x ' ^ ((y ^ x) ' v z) ' = 0. [para(31(a,1),10493(a,1,2,1)),demod(14(6))]. given #591 (A,wt=21): 263 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(28(a,1),110(a,1,2,2))]. given #592 (F,wt=9): 11307 x ^ ((x ^ y) v y ') ' = 0. [para(10615(a,1),158(a,1,2))]. given #593 (F,wt=9): 11315 x ^ ((y ^ x) v y ') ' = 0. [para(10615(a,1),1214(a,1,2))]. given #594 (T,wt=9): 11356 x ' ^ ((x ^ y) ' v z) = x '. [para(10489(a,1),10615(a,1,2,1)),demod(14(5),10489(10))]. given #595 (T,wt=9): 11357 x ' ^ ((y ^ x) ' v z) = x '. [para(10499(a,1),10615(a,1,2,1)),demod(14(5),10499(10))]. given #596 (A,wt=16): 266 x ^ (y v (x ' v z)) != 0 | y v (x ' v z) = x '. [para(118(a,1),20(a,1)),flip(c),xx(a)]. given #597 (F,wt=9): 11361 x ' ^ (y v (x ^ z) ') ' = 0. [para(10616(a,1),156(a,1,2,1)),demod(14(6))]. given #598 (F,wt=9): 11418 x ' ^ (y v (x ^ z) ') = x '. [para(10616(a,1),10615(a,1,2,1)),demod(14(5),10616(10))]. given #599 (T,wt=9): 11419 (x v y ') ' ^ (y v z) ' = 0. [para(12(a,1),10620(a,1,2,1))]. given #600 (T,wt=9): 11422 x ' ^ (y v (z ^ x) ') ' = 0. [para(31(a,1),10620(a,1,2,1)),demod(14(6))]. given #601 (A,wt=19): 267 x ^ (y v (z ^ (x v (u v (y ' v v))))) = x ^ (y v z). [para(118(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #602 (F,wt=9): 11543 x ' ^ (y v (z ^ x) ') = x '. [para(10626(a,1),10615(a,1,2,1)),demod(14(5),10626(10))]. given #603 (F,wt=9): 11700 x ^ (y v (x ^ y ')) ' = 0. [para(10700(a,1),164(a,1,2))]. given #604 (T,wt=9): 11713 x ^ (y v (y ' ^ x)) ' = 0. [para(10700(a,1),1223(a,1,2))]. given #605 (T,wt=9): 11753 (x v y) ' ^ (x ' v z) ' = 0. [para(12(a,1),10703(a,1,2,1))]. given #606 (A,wt=16): 271 x v (y ^ (x ' ^ z)) != 1 | y ^ (x ' ^ z) = x '. [para(133(a,1),20(b,1)),flip(c),xx(b)]. given #607 (F,wt=9): 11941 x v (x ' ^ y) ' = (x ' ^ y) '. [para(308(a,1),10788(a,1,1))]. low water: id=7202, wt=18 low water: id=10873, wt=17 given #608 (F,wt=9): 11948 x v (y ^ (x v y ')) ' = 1. [para(10788(a,1),215(a,1,2))]. given #609 (T,wt=9): 11971 x v (y ^ (y ' v x)) ' = 1. [para(10788(a,1),1359(a,1,2))]. given #610 (T,wt=9): 12021 x ' ^ (y ^ (x ^ z)) ' = x '. [para(24(a,1),11936(a,1,2,1))]. given #611 (A,wt=19): 275 (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 #612 (F,wt=9): 12024 (x ^ y) ' v (z ^ x ') ' = 1. [para(11936(a,1),216(a,1,2,1,2))]. given #613 (F,wt=9): 12041 x ' ^ (y ^ (z ^ x)) ' = x '. [para(187(a,1),11936(a,1,2,1))]. given #614 (T,wt=9): 12068 (x ^ y) ' v (z ^ y ') ' = 1. [para(12019(a,1),216(a,1,2,1,2))]. given #615 (T,wt=9): 12121 x ^ (y ^ (x ' ^ z)) ' = x. [para(24(a,1),12023(a,1,2,1))]. given #616 (A,wt=21): 276 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),177(6),55(6))]. given #617 (F,wt=9): 12122 x ^ ((x v y) ' ^ z) ' = x. [para(12023(a,1),27(a,1,2)),demod(16(2)),flip(a)]. given #618 (F,wt=9): 12125 (x ' ^ y) ' v (z ^ x) ' = 1. [para(12023(a,1),216(a,1,2,1,2))]. given #619 (T,wt=9): 12126 x ^ ((x ' ^ y) ' v z) ' = 0. [para(12023(a,1),647(a,1,2)),demod(14(6))]. given #620 (T,wt=9): 12127 x ^ (y v (x ' ^ z) ') ' = 0. [para(12023(a,1),651(a,1,2)),demod(14(6))]. given #621 (A,wt=17): 278 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(32(a,1),23(a,1,2)),flip(a)]. given #622 (F,wt=9): 12128 x ^ ((y v x) ' ^ z) ' = x. [para(12023(a,1),102(a,1,2)),demod(25(2)),flip(a)]. given #623 (F,wt=9): 12131 x ^ ((x ' ^ y) ' v z) = x. [para(12023(a,1),188(a,1,2)),demod(14(5),12023(9))]. given #624 (T,wt=9): 12144 x ^ (y v (x ' ^ z) ') = x. [para(12023(a,1),862(a,1,2)),demod(14(5),12023(9))]. given #625 (T,wt=9): 12168 x ^ (y ^ (z ^ x ')) ' = x. [para(187(a,1),12023(a,1,2,1))]. given #626 (A,wt=19): 279 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(24(a,1),32(a,1,1)),demod(15(4))]. given #627 (F,wt=9): 12193 x v (y ^ x ') ' = (y ^ x ') '. [para(12066(a,1),31(a,1,2)),demod(12(4))]. given #628 (F,wt=9): 12194 x ^ (y ^ (x v z) ') ' = x. [para(12066(a,1),27(a,1,2)),demod(16(2)),flip(a)]. given #629 (T,wt=9): 12198 (x ^ y ') ' v (z ^ y) ' = 1. [para(12066(a,1),216(a,1,2,1,2))]. given #630 (T,wt=9): 12199 x ^ ((y ^ x ') ' v z) ' = 0. [para(12066(a,1),647(a,1,2)),demod(14(6))]. given #631 (A,wt=15): 280 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(24(a,1),32(a,1,2,2))]. given #632 (F,wt=9): 12200 x ^ (y v (z ^ x ') ') ' = 0. [para(12066(a,1),651(a,1,2)),demod(14(6))]. given #633 (F,wt=9): 12201 x ^ (y ^ (z v x) ') ' = x. [para(12066(a,1),102(a,1,2)),demod(25(2)),flip(a)]. given #634 (T,wt=9): 12204 x ^ ((y ^ x ') ' v z) = x. [para(12066(a,1),188(a,1,2)),demod(14(5),12066(9))]. given #635 (T,wt=9): 12216 x ^ (y v (z ^ x ') ') = x. [para(12066(a,1),862(a,1,2)),demod(14(5),12066(9))]. given #636 (A,wt=17): 282 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(32(a,1),101(a,1,2,2)),demod(15(5),15(4))]. given #637 (F,wt=9): 12389 (x ^ y) ' v (x ' ^ z) ' = 1. [para(17(a,1),10802(a,1,2,1,1,1))]. given #638 (F,wt=9): 12392 (x ^ y) ' v (y ' ^ z) ' = 1. [para(31(a,1),10802(a,1,2,1,1,1))]. given #639 (T,wt=9): 12986 x v (y ' ^ (x v y)) ' = 1. [para(11941(a,1),215(a,1,2))]. given #640 (T,wt=9): 12999 x v (y ' ^ (y v x)) ' = 1. [para(11941(a,1),1359(a,1,2))]. given #641 (A,wt=16): 285 x ^ (y v (z v x ')) != 0 | y v (z v x ') = x '. [para(135(a,1),20(a,1)),flip(c),xx(a)]. given #642 (F,wt=9): 13149 (x ^ y ') ' v (y ^ z) ' = 1. [para(12024(a,1),12(a,1)),flip(a)]. given #643 (F,wt=9): 13326 (x ' ^ y) ' v (x ^ z) ' = 1. [para(14(a,1),12125(a,1,2,1))]. given #644 (T,wt=9): 13474 x v ((x v y) ^ y ') ' = 1. [para(12193(a,1),208(a,1,2))]. given #645 (T,wt=9): 13487 x v ((y v x) ^ y ') ' = 1. [para(12193(a,1),1490(a,1,2))]. given #646 (A,wt=19): 286 x ^ (y v (z ^ (x v (u v (v v y '))))) = x ^ (y v z). [para(135(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #647 (F,wt=9): 13653 (x ' ^ (x v y)) ' = (y ^ x ') '. [hyper(44,a,12986,a,b,342,a),demod(12(7),826(8)),flip(a)]. given #648 (F,wt=9): 13736 (x ' ^ (y v x)) ' = (y ^ x ') '. [para(12(a,1),13653(a,1,1,2))]. given #649 (T,wt=9): 13737 ((x v y) ^ x ') ' = (y ^ x ') '. [para(14(a,1),13653(a,1,1))]. given #650 (T,wt=9): 13738 (x ' ^ (x v y)) ' = (x ' ^ y) '. [para(14(a,1),13653(a,2,1))]. given #651 (A,wt=16): 290 x v (y ^ (z ^ x ')) != 1 | y ^ (z ^ x ') = x '. [para(139(a,1),20(b,1)),flip(c),xx(b)]. given #652 (F,wt=9): 13743 (x ' ^ (y v (x v y) ')) ' = x. [para(36(a,1),13653(a,1,1,2)),demod(14(3),68(3),308(2),14(5)),flip(a)]. given #653 (F,wt=9): 13746 (x ' ^ (y v (y v x) ')) ' = x. [para(142(a,1),13653(a,1,1,2)),demod(14(3),68(3),308(2),14(5)),flip(a)]. given #654 (T,wt=9): 13748 (x ^ (x ' v y)) ' = (y ^ x) '. [para(308(a,1),13653(a,1,1,1)),demod(308(6))]. given #655 (T,wt=9): 13807 (x v y) ^ (x ' ^ y) ' = x. [para(13653(a,1),171(a,1,2,2)),demod(12206(7),13738(8),308(10)),xx(a)]. given #656 (A,wt=16): 295 x ^ (y v (y v x) ') != 0 | y v (y v x) ' = x '. [para(142(a,1),20(a,1)),flip(c),xx(a)]. given #657 (F,wt=9): 13888 ((x v y) ^ y ') ' = (x ^ y ') '. [para(14(a,1),13736(a,1,1))]. given #658 (F,wt=9): 13889 (x ' ^ (y v x)) ' = (x ' ^ y) '. [para(14(a,1),13736(a,2,1))]. given #659 (T,wt=9): 13896 (x ^ (y v x ')) ' = (y ^ x) '. [para(308(a,1),13736(a,1,1,1)),demod(308(6))]. given #660 (T,wt=9): 13920 (x v y) ^ (y ' ^ x) ' = y. [para(13736(a,1),171(a,1,2,2)),demod(12217(7),13889(8),308(10)),xx(a)]. given #661 (A,wt=19): 296 x ^ (y v (z ^ (x v (u v (u v y) ')))) = x ^ (y v z). [para(142(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. given #662 (F,wt=9): 13935 (x v y) ^ x ' = y ^ x '. [para(13737(a,1),308(a,1,1)),demod(308(4)),flip(a)]. given #663 (F,wt=9): 13955 x ' ^ (x v y) = x ' ^ y. [para(13738(a,1),308(a,1,1)),demod(308(4)),flip(a)]. given #664 (T,wt=9): 14003 x ' ^ (y v (x v y) ') = x '. [para(13743(a,1),308(a,1,1)),flip(a)]. given #665 (T,wt=9): 14020 x ' ^ (y v (y v x) ') = x '. [para(13746(a,1),308(a,1,1)),flip(a)]. given #666 (A,wt=16): 302 x v ((x v y) ' ^ z) != 1 | (x v y) ' ^ z = x '. [para(154(a,1),20(b,1)),flip(c),xx(b)]. given #667 (F,wt=9): 14041 x ^ (x ' v y) = y ^ x. [para(13748(a,1),308(a,1,1)),demod(308(3)),flip(a)]. given #668 (F,wt=9): 14084 (x ' v y) ^ (y ^ x) ' = x '. [para(13748(a,1),171(a,1,2,2)),demod(12074(6),14041(8)),xx(a)]. given #669 (T,wt=7): 14732 (x v y) ' = y ' ^ x '. [para(16(a,1),14084(a,1,2,1)),demod(12(3),14609(3),13935(4)),flip(a)]. given #670 (T,wt=7): 14934 (x ' ^ y ') ' = y v x. [back_demod(13909),demod(14732(5),24(7),13153(7))]. given #671 (A,wt=19): 304 x v (y v z) != 1 | z ^ (x v y) != 0 | z ' = x v y. [para(13(a,1),41(a,1))]. given #672 (F,wt=7): 16865 (x ^ y ') ' = y v x '. [para(308(a,1),14934(a,1,1,1))]. given #673 (F,wt=7): 17186 (x ^ y) ' = y ' v x '. [para(308(a,1),16865(a,1,1,2))]. given #674 (T,wt=9): 14213 (x v y) ^ y ' = x ^ y '. [para(13888(a,1),308(a,1,1)),demod(308(4)),flip(a)]. given #675 (T,wt=9): 14219 x ' ^ (y v x) = x ' ^ y. [para(13889(a,1),308(a,1,1)),demod(308(4)),flip(a)]. given #676 (A,wt=19): 310 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z ' = x ^ y. [para(24(a,1),41(b,1))]. given #677 (F,wt=9): 14241 x ^ (y v x ') = y ^ x. [para(13896(a,1),308(a,1,1)),demod(308(3)),flip(a)]. given #678 (F,wt=9): 14638 (x v y) ^ (x v y ') = x. [para(16(a,1),14041(a,2)),demod(12(4),14609(4))]. given #679 (T,wt=9): 14641 (x v y) ^ (y v x ') = y. [para(25(a,1),14041(a,2)),demod(12(4),14580(4))]. given #680 (T,wt=9): 14868 x v (y ' ^ x ') = x v y '. [back_demod(14609),demod(14732(2))]. given #681 (A,wt=19): 418 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x ' = y ^ z. [para(15(a,1),43(b,1))]. given #682 (F,wt=9): 14875 x v (x ' ^ y ') = x v y '. [back_demod(14580),demod(14732(2))]. given #683 (F,wt=9): 16629 (x ^ y) v (x ^ y ') = x. [back_demod(12929),demod(14742(4))]. given #684 (T,wt=9): 16691 x ^ ((y ^ x) v y ') = x. [back_demod(12928),demod(14800(4),14621(4))]. given #685 (T,wt=9): 16882 (x v y ') ^ (y v x) = x. [para(14934(a,1),13807(a,1,2))]. given #686 (A,wt=19): 419 x v (y v z) != 1 | (x v z) ^ y != 0 | y ' = x v z. [para(23(a,1),43(a,1))]. given #687 (F,wt=9): 16884 (x v y) ^ (x ' v y) = y. [para(14934(a,1),13920(a,1,2)),demod(14(4))]. given #688 (F,wt=9): 17072 (x v y) ^ (y ' v x) = x. [back_demod(13807),demod(16866(4))]. given #689 (T,wt=9): 19372 (x ^ y) v (x ' v y ') = 1. [back_demod(1510),demod(17186(3))]. given #690 (T,wt=9): 19861 (x ' v y) ^ (y v x) = y. [para(308(a,1),14641(a,1,2,2))]. given #691 (A,wt=19): 576 x ^ (y ' v (z v (u ^ (x v y)))) = x ^ (y ' v (z v u)). [para(85(a,1),47(a,1,2,2,2,2)),demod(37(5),12(4),31(4),13(3),13(9)),flip(a)]. given #692 (F,wt=9): 19900 x v (y ^ x ') = x v y. [para(308(a,1),14868(a,1,2,1)),demod(308(5))]. given #693 (F,wt=9): 20245 x ' v (x ^ y ') = x ' v y '. [para(308(a,1),14875(a,1,2,1))]. given #694 (T,wt=9): 20246 x v (x ' ^ y) = x v y. [para(308(a,1),14875(a,1,2,2)),demod(308(5))]. given #695 (T,wt=9): 20300 (x ^ y) v (y ^ x ') = y. [para(14(a,1),16629(a,1,1))]. ============================== PROOF ================================= % Proof 1 at 13.67 (+ 0.20) seconds. % Length of proof is 96. % Level of proof is 24. % Maximum clause weight is 23. % Given clauses 695. 10 x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [input]. 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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))) # label(H49). [copy(10),flip(a)]. 22 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity). [clausify]. 23 x v (y v z) = y v (x v z). [para(12(a,1),13(a,1,1)),demod(13(2))]. 24 x ^ (y ^ z) = y ^ (x ^ z). [para(14(a,1),15(a,1,1)),demod(15(2))]. 25 x ^ (y v x) = x. [para(12(a,1),16(a,1,2))]. 27 x ^ ((x v y) ^ z) = x ^ z. [para(16(a,1),15(a,1,1)),flip(a)]. 28 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(16(a,1),15(a,1)),flip(a)]. 29 x v ((x ^ y) v z) = x v z. [para(17(a,1),13(a,1,1)),flip(a)]. 31 x v (y ^ x) = x. [para(14(a,1),17(a,1,2))]. 34 x v x = x. [para(16(a,1),17(a,1,2))]. 35 x v (x ' v y) = 1 v y. [para(18(a,1),13(a,1,1)),flip(a)]. 36 x v (y v (x v y) ') = 1. [para(18(a,1),13(a,1)),flip(a)]. 37 x ^ 1 = x. [para(18(a,1),16(a,1,2))]. 38 x ^ (x ' ^ y) = 0 ^ y. [para(19(a,1),15(a,1,1)),flip(a)]. 39 x ^ (y ^ (x ^ y) ') = 0. [para(19(a,1),15(a,1)),flip(a)]. 40 x v 0 = x. [para(19(a,1),17(a,1,2))]. 41 x v y != 1 | y ^ x != 0 | y ' = x. [para(12(a,1),20(a,1))]. 44 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(15(a,1),20(b,1))]. 49 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(14(a,1),21(a,1,2,2,1))]. 53 x ^ (y v (z ^ (x v y '))) = x ^ (y v z). [para(18(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. 61 x v (x v y) = x v y. [para(34(a,1),13(a,1,1)),flip(a)]. 68 1 ^ x = x. [para(37(a,1),14(a,1)),flip(a)]. 71 0 v x = x. [para(40(a,1),12(a,1)),flip(a)]. 79 x v (y v x ') = y v 1. [para(18(a,1),23(a,1,2)),flip(a)]. 84 1 v x = 1. [para(68(a,1),16(a,1))]. 85 x v (x ' v y) = 1. [back_demod(35),demod(84(5))]. 87 0 ^ x = 0. [para(71(a,1),16(a,1,2))]. 89 x ^ (x ' ^ y) = 0. [back_demod(38),demod(87(5))]. 90 x ^ (y ^ (x v z)) = y ^ x. [para(16(a,1),24(a,1,2)),flip(a)]. 92 x ^ (y ^ x ') = y ^ 0. [para(19(a,1),24(a,1,2)),flip(a)]. 95 x v 1 = 1. [para(84(a,1),12(a,1)),flip(a)]. 96 x v (y v x ') = 1. [back_demod(79),demod(95(5))]. 98 x ^ 0 = 0. [para(87(a,1),14(a,1)),flip(a)]. 99 x ^ (y ^ x ') = 0. [back_demod(92),demod(98(5))]. 102 x ^ ((y v x) ^ z) = x ^ z. [para(25(a,1),15(a,1,1)),flip(a)]. 108 x v ((y ^ x) v z) = x v z. [para(31(a,1),13(a,1,1)),flip(a)]. 117 x ^ (y v (z ^ (x v (y ' v u)))) = x ^ (y v z). [para(85(a,1),21(a,1,2,2,2,2)),demod(37(3),12(2),31(2)),flip(a)]. 149 x ^ (x v y) ' = 0. [para(19(a,1),27(a,1,2)),demod(98(2)),flip(a)]. 154 x ^ ((x v y) ' ^ z) = 0. [para(89(a,1),27(a,1,2)),demod(98(2)),flip(a)]. 156 x ^ (y v x) ' = 0. [para(12(a,1),149(a,1,2,1))]. 160 x ^ (y v ((x v z) ' ^ (y v u))) = x ^ (y v ((x v z) ' ^ (x v u))). [para(149(a,1),21(a,1,2,2,1)),demod(71(6))]. 164 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(156(a,1),15(a,1)),flip(a)]. 171 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(39(a,1),20(b,1)),flip(c),xx(b)]. 197 x v (x ^ y) ' = 1. [para(18(a,1),29(a,1,2)),demod(95(2)),flip(a)]. 205 x v (y v ((x ^ z) v y) ') = 1. [para(36(a,1),29(a,1,2)),demod(95(2)),flip(a)]. 209 x v (y ^ x) ' = 1. [para(14(a,1),197(a,1,2,1))]. 215 x v (y v (z ^ (x v y)) ') = 1. [para(209(a,1),13(a,1)),flip(a)]. 222 ((x v y) ^ z) v (x ^ z) ' = 1. [para(27(a,1),209(a,1,2,1))]. 305 x v y != 1 | x ^ y != 0 | y ' = x. [para(14(a,1),41(b,1))]. 308 x ' ' = x. [para(18(a,1),41(a,1)),demod(14(5),19(5)),xx(a),xx(b)]. 327 x ' v (y v x) = 1. [para(308(a,1),96(a,1,2,2))]. 328 x ' ^ (y ^ x) = 0. [para(308(a,1),99(a,1,2,2))]. 333 x ' ^ (y v x) != 0 | y v x = x. [para(327(a,1),20(a,1)),demod(308(10)),flip(c),xx(a)]. 342 x ^ (y ^ (y ^ ((x ^ y) v z)) ') = 0. [para(28(a,1),328(a,1,2)),demod(14(6),15(6))]. 740 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(71(a,1),49(a,1,2,2,2,2)),demod(71(5),71(8),90(7))]. 826 x ' ^ (x v (y ^ x ')) = x ' ^ (x v y). [para(34(a,1),53(a,1,2,2,2))]. 1372 x v ((x ^ y) v (x ^ z)) ' = 1. [para(205(a,1),29(a,1)),flip(a)]. 2824 x ' ^ (x v (y ^ (x ' v z))) = x ' ^ (x v y). [para(61(a,1),117(a,1,2,2,2))]. 6985 x ' ^ (x v y) != 0 | y v x = x. [para(12(a,1),333(a,1,2))]. 10458 x ' ^ (x v (x ' v y) ') = 0. [para(160(a,1),826(a,2)),demod(14(8),154(8),40(3),14(2),19(2),2824(10)),flip(a)]. 10472 x v (x ' v y) ' = x. [hyper(6985,a,10458,a),demod(12(4))]. 10482 x v (y v x ') ' = x. [para(12(a,1),10472(a,1,2,1))]. 10492 x ' v (x v y) ' = x '. [para(308(a,1),10472(a,1,2,1,1))]. 10619 x ' v (y v x) ' = x '. [para(308(a,1),10482(a,1,2,1,2))]. 10700 x ' ^ (x v y) ' = (x v y) '. [para(10492(a,1),25(a,1,2)),demod(14(4))]. 10788 x ' v (x ^ y) ' = (x ^ y) '. [para(17(a,1),10619(a,1,2,1)),demod(12(4))]. 11700 x ^ (y v (x ^ y ')) ' = 0. [para(10700(a,1),164(a,1,2))]. 11936 x ' ^ (x ^ y) ' = x '. [para(10788(a,1),16(a,1,2))]. 11941 x v (x ' ^ y) ' = (x ' ^ y) '. [para(308(a,1),10788(a,1,1))]. 12019 x ' ^ (y ^ x) ' = x '. [para(14(a,1),11936(a,1,2,1))]. 12074 x v ((x ' v y) ^ (z ^ x) ') = 1. [para(12019(a,1),222(a,1,2,1)),demod(308(7),12(6))]. 12929 (x ^ y) v (x ^ (x ^ y) ') = x. [hyper(305,a,1372,a,b,11700,a),demod(308(7))]. 12986 x v (y ' ^ (x v y)) ' = 1. [para(11941(a,1),215(a,1,2))]. 13653 (x ' ^ (x v y)) ' = (y ^ x ') '. [hyper(44,a,12986,a,b,342,a),demod(12(7),826(8)),flip(a)]. 13737 ((x v y) ^ x ') ' = (y ^ x ') '. [para(14(a,1),13653(a,1,1))]. 13748 (x ^ (x ' v y)) ' = (y ^ x) '. [para(308(a,1),13653(a,1,1,1)),demod(308(6))]. 13935 (x v y) ^ x ' = y ^ x '. [para(13737(a,1),308(a,1,1)),demod(308(4)),flip(a)]. 14041 x ^ (x ' v y) = y ^ x. [para(13748(a,1),308(a,1,1)),demod(308(3)),flip(a)]. 14084 (x ' v y) ^ (y ^ x) ' = x '. [para(13748(a,1),171(a,1,2,2)),demod(12074(6),14041(8)),xx(a)]. 14387 ((x ^ y) v z) ^ y ' = z ^ y '. [para(108(a,1),13935(a,1,1)),demod(13935(3)),flip(a)]. 14742 x ^ (x ^ y) ' = x ^ y '. [para(14084(a,1),102(a,1,2)),flip(a)]. 16629 (x ^ y) v (x ^ y ') = x. [back_demod(12929),demod(14742(4))]. 20300 (x ^ y) v (y ^ x ') = y. [para(14(a,1),16629(a,1,1))]. 21106 (x ^ y) v (x ^ (z ^ y ')) = x ^ (y v z). [para(90(a,1),20300(a,1,1)),demod(15(5),13935(4))]. 21134 (x ^ y) v (x ^ z) = x ^ (y v z). [para(740(a,1),20300(a,1,1)),demod(14387(6),15(4),21106(5)),flip(a)]. 21135 $F. [resolve(21134,a,22,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=695. Generated=534647. Kept=21123. proofs=1. Usable=188. Sos=3747. Demods=2947. Denials=0. Limbo=37, Disabled=17161. Hints=0. Weight_deleted=18349. Literals_deleted=0. Forward_subsumed=476168. Back_subsumed=83. Sos_limit_deleted=19007. Sos_displaced=2337. Sos_removed=0. New_demodulators=17715 (4 lex), Back_demodulated=14730. Back_unit_deleted=0. Demod_attempts=9924500. Demod_rewrites=2503304. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=276905. Nonunit_bsub_feature_tests=59964. Megabytes=11.79. User_CPU=13.67, System_CPU=0.20, Wall_clock=13. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13657 exit (max_proofs) Mon Jun 19 16:45:47 2006