============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 15261 was started by mccune on cleo, Fri Jun 15 14:08:14 2007 The command was "prover9 -f t2_23.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file t2_23.in assign(max_seconds,60). set(expand_relational_defs). formulas(assumptions). x ^ y = y ^ x # label("commutativity_meet"). x v y = y v x # label("commutativity_join"). (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). (x v y) v z = x v (y v z) # label("associativity_join"). (x v y) ^ x = x # label("absorption_1"). (x ^ y) v x = x # label("absorption_2"). end_of_list. formulas(assumptions). (all x all y (x <= y <-> x ^ y = x)). (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)). (all x all y all z (C(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x ^ z) v y = y)). (all x all y all z (CS(x,y,z) <-> (x v y) ^ (y v z) = y & (x v z) ^ y = y)). (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). end_of_list. formulas(assumptions). -D(x,y,z) | A(x,y,z). end_of_list. formulas(goals). B(x,y,z) & B(y,z,u) & y != z -> B(x,z,u). end_of_list. ============================== end of input ========================== ============================== EXPAND RELATIONAL DEFINITIONS ========= % Relational Definitions: 1 (all x all y (x <= y <-> x ^ y = x)). [assumption]. 2 (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). [assumption]. 3 (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)). [assumption]. 4 (all x all y all z (C(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x ^ z) v y = y)). [assumption]. 5 (all x all y all z (CS(x,y,z) <-> (x v y) ^ (y v z) = y & (x v z) ^ y = y)). [assumption]. 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). [assumption]. % Relational Definitions, Expanded: 7 (all x all y all z (A(x,y,z) <-> x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y)). [expand_def(2,1)]. 8 (all x all y all z (D(x,y,z) <-> (x ^ z) ^ y = x ^ z & y ^ (x v z) = y)). [expand_def(6,1)]. % Formulas Being Expanded: 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). [assumption]. 2 (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). [assumption]. 9 -D(x,y,z) | A(x,y,z). [assumption]. 10 -D(x,y,z) | x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y. [expand_def(9,7)]. 11 B(x,y,z) & B(y,z,u) & y != z -> B(x,z,u). [goal]. ============================== end of expand relational definitions == ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 12 -((x ^ z) ^ y = x ^ z & y ^ (x v z) = y) | x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y # label(non_clause). [expand_def(10,8)]. 13 ((x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y) & ((y ^ z) v (z ^ u) = z & (y v z) ^ (z v u) = z) & y != z -> (x ^ z) v (z ^ u) = z & (x v z) ^ (z v u) = z # label(non_clause) # label(goal). [expand_def(11,3)]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | x ^ z = x | y ^ z = y. [clausify(12)]. (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | x ^ z = x | z ^ x = z. [clausify(12)]. (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | z ^ y = z | y ^ z = y. [clausify(12)]. (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | z ^ y = z | z ^ x = z. [clausify(12)]. (x ^ y) v x = x # label("absorption_2"). [assumption]. (x v y) ^ x = x # label("absorption_1"). [assumption]. (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. x v y = y v x # label("commutativity_join"). [assumption]. x ^ y = y ^ x # label("commutativity_meet"). [assumption]. (c1 ^ c2) v (c2 ^ c3) = c2. [deny(13)]. (c1 v c2) ^ (c2 v c3) = c2. [deny(13)]. (c2 ^ c3) v (c3 ^ c4) = c3. [deny(13)]. (c2 v c3) ^ (c3 v c4) = c3. [deny(13)]. c3 != c2. [deny(13)]. (c1 ^ c3) v (c3 ^ c4) != c3 | (c1 v c3) ^ (c3 v c4) != c3. [deny(13)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(positive_inference). % (non-Horn) % set(positive_inference) -> assign(literal_selection, maximal_negative). % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 20 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 21 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 22 x v y = y v x # label("commutativity_join"). [assumption]. 23 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 24 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(13)]. 25 (c1 v c2) ^ (c2 v c3) = c2. [deny(13)]. 26 (c2 ^ c3) v (c3 ^ c4) = c3. [deny(13)]. 27 (c2 v c3) ^ (c3 v c4) = c3. [deny(13)]. 28 c3 != c2. [deny(13)]. 29 (c1 ^ c3) v (c3 ^ c4) != c3 | (c1 v c3) ^ (c3 v c4) != c3. [deny(13)]. 30 x ^ (x ^ y) != x ^ x | y ^ (x v x) != y | x ^ y = x. [factor(14,c,d),rewrite([21(2)])]. 32 x ^ (y ^ x) != y ^ x | x ^ (y v x) != x | x ^ x = x. [factor(16,c,d),rewrite([23(2)])]. 33 x ^ (x ^ y) != x ^ x | y ^ (x v x) != y | y ^ x = y. [factor(17,c,d),rewrite([21(2)])]. 34 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | z ^ y = z | z ^ x = z. [back_rewrite(17),rewrite([21(2)])]. 35 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | z ^ y = z | y ^ z = y. [back_rewrite(16),rewrite([21(2)])]. 36 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | x ^ z = x | z ^ x = z. [back_rewrite(15),rewrite([21(2)])]. 37 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | x ^ z = x | y ^ z = y. [back_rewrite(14),rewrite([21(2)])]. 38 x v (x ^ y) = x. [back_rewrite(18),rewrite([22(2)])]. 39 x ^ (x v y) = x. [back_rewrite(19),rewrite([23(2)])]. 40 x ^ (y ^ y) != x ^ y | y ^ (x v y) != y | y ^ y = y. [factor(35,c,d)]. 41 x ^ (y ^ x) != x ^ y | x ^ x = x. [factor(36,c,d),rewrite([39(6)]),xx(b)]. 42 x ^ (x ^ y) != x ^ y | x ^ x = x. [back_rewrite(31),rewrite([39(6)]),xx(b)]. end_of_list. formulas(demodulators). 20 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 21 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 22 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 23 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 24 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(13)]. 25 (c1 v c2) ^ (c2 v c3) = c2. [deny(13)]. 26 (c2 ^ c3) v (c3 ^ c4) = c3. [deny(13)]. 27 (c2 v c3) ^ (c3 v c4) = c3. [deny(13)]. 38 x v (x ^ y) = x. [back_rewrite(18),rewrite([22(2)])]. 39 x ^ (x v y) = x. [back_rewrite(19),rewrite([23(2)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 20 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. given #2 (I,wt=11): 21 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. given #3 (I,wt=7): 22 x v y = y v x # label("commutativity_join"). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. given #4 (I,wt=7): 23 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. given #5 (I,wt=9): 24 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(13)]. given #6 (I,wt=9): 25 (c1 v c2) ^ (c2 v c3) = c2. [deny(13)]. given #7 (I,wt=9): 26 (c2 ^ c3) v (c3 ^ c4) = c3. [deny(13)]. given #8 (I,wt=9): 27 (c2 v c3) ^ (c3 v c4) = c3. [deny(13)]. given #9 (I,wt=3): 28 c3 != c2. [deny(13)]. given #10 (I,wt=18): 29 (c1 ^ c3) v (c3 ^ c4) != c3 | (c1 v c3) ^ (c3 v c4) != c3. [deny(13)]. given #11 (I,wt=21): 30 x ^ (x ^ y) != x ^ x | y ^ (x v x) != y | x ^ y = x. [factor(14,c,d),rewrite([21(2)])]. given #12 (I,wt=21): 32 x ^ (y ^ x) != y ^ x | x ^ (y v x) != x | x ^ x = x. [factor(16,c,d),rewrite([23(2)])]. given #13 (I,wt=21): 33 x ^ (x ^ y) != x ^ x | y ^ (x v x) != y | y ^ x = y. [factor(17,c,d),rewrite([21(2)])]. given #14 (I,wt=26): 34 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | z ^ y = z | z ^ x = z. [back_rewrite(17),rewrite([21(2)])]. given #15 (I,wt=26): 35 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | z ^ y = z | y ^ z = y. [back_rewrite(16),rewrite([21(2)])]. given #16 (I,wt=26): 36 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | x ^ z = x | z ^ x = z. [back_rewrite(15),rewrite([21(2)])]. given #17 (I,wt=26): 37 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | x ^ z = x | y ^ z = y. [back_rewrite(14),rewrite([21(2)])]. given #18 (I,wt=7): 38 x v (x ^ y) = x. [back_rewrite(18),rewrite([22(2)])]. given #19 (I,wt=7): 39 x ^ (x v y) = x. [back_rewrite(19),rewrite([23(2)])]. given #20 (A,wt=11): 43 x v (y v z) = y v (x v z). [para(22(a,1),20(a,1,1)),rewrite([20(2)])]. given #21 (T,wt=5): 173 x v x = x. [para(39(a,1),38(a,1,2))]. given #22 (T,wt=5): 174 x ^ x = x. [para(38(a,1),39(a,1,2))]. given #23 (T,wt=7): 152 x v (y ^ x) = x. [para(23(a,1),38(a,1,2))]. given #24 (T,wt=7): 165 x ^ (y v x) = x. [para(22(a,1),39(a,1,2))]. given #25 (A,wt=11): 44 x ^ (y ^ z) = y ^ (x ^ z). [para(23(a,1),21(a,1,1)),rewrite([21(2)])]. given #26 (T,wt=9): 192 x ^ (y v (x v z)) = x. [para(43(a,1),39(a,1,2))]. given #27 (T,wt=9): 193 x v (x v y) = x v y. [para(173(a,1),20(a,1,1)),flip(a)]. given #28 (T,wt=9): 195 x v (y v x) = y v x. [para(173(a,1),20(a,2,2)),rewrite([22(2)])]. given #29 (T,wt=9): 205 x ^ (x ^ y) = x ^ y. [para(174(a,1),21(a,1,1)),flip(a)]. given #30 (A,wt=13): 45 (c1 ^ c2) v ((c2 ^ c3) v x) = c2 v x. [para(24(a,1),20(a,1,1)),flip(a)]. given #31 (T,wt=9): 207 x ^ (y ^ x) = y ^ x. [para(174(a,1),21(a,2,2)),rewrite([23(2)])]. given #32 (T,wt=9): 221 x v (y ^ (z ^ x)) = x. [para(21(a,1),152(a,1,2))]. given #33 (T,wt=9): 224 x ^ (y v (z v x)) = x. [para(20(a,1),165(a,1,2))]. given #34 (T,wt=9): 237 x v (y ^ (x ^ z)) = x. [para(44(a,1),38(a,1,2))]. given #35 (A,wt=13): 46 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(24(a,1),20(a,2,2)),rewrite([22(8)])]. given #36 (T,wt=9): 291 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),46(a,1,2)),rewrite([22(5)])]. given #37 (T,wt=10): 204 x v y = y | x v y = x. [resolve(174,a,34,b),rewrite([165(2),23(5),165(5),23(7),39(7)]),flip(b),flip(c),xx(a)]. given #38 (T,wt=10): 208 x ^ y = x | y ^ x = y. [para(174(a,1),36(a,1,2)),rewrite([165(5)]),xx(a),xx(b)]. given #39 (T,wt=10): 306 x v y = x | y v x = y. [para(204(a,1),22(a,1)),flip(b)]. given #40 (A,wt=13): 47 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(25(a,1),21(a,1,1)),flip(a)]. given #41 (T,wt=10): 307 x v y = y | y v x = x. [para(204(b,1),22(a,1)),flip(b)]. given #42 (T,wt=10): 308 c1 ^ c2 = c2 | c2 ^ c3 = c2. [para(204(a,1),24(a,1)),rewrite([24(7)]),flip(a)]. given #43 (T,wt=10): 311 c2 ^ c3 = c3 | c3 ^ c4 = c3. [para(204(a,1),26(a,1)),rewrite([26(7)]),flip(a)]. given #44 (T,wt=10): 318 x v y = x | x ^ y = x. [para(204(a,1),39(a,1,2))]. given #45 (A,wt=13): 48 (c2 ^ c3) v ((c3 ^ c4) v x) = c3 v x. [para(26(a,1),20(a,1,1)),flip(a)]. given #46 (T,wt=10): 323 x v y = y | y ^ x = y. [para(204(b,1),165(a,1,2))]. given #47 (T,wt=10): 340 x ^ y = x | x ^ y = y. [para(208(a,1),23(a,1)),flip(b)]. given #48 (T,wt=10): 341 c1 ^ c2 = c2 | c1 v c2 = c2. [para(208(a,1),24(a,1,1)),rewrite([23(3),291(10)])]. given #49 (T,wt=10): 342 c2 v c3 = c2 | c1 v c2 = c2. [para(208(a,1),25(a,1)),rewrite([23(7),25(7)]),flip(a)]. given #50 (A,wt=13): 49 (c3 ^ c4) v (x v (c2 ^ c3)) = x v c3. [para(26(a,1),20(a,2,2)),rewrite([22(8)])]. given #51 (T,wt=9): 491 c2 v (c3 ^ c4) = c2 v c3. [para(38(a,1),49(a,1,2)),rewrite([22(5)])]. given #52 (T,wt=9): 496 c1 v (c2 v c3) = c1 v c3. [para(291(a,1),49(a,1,2)),rewrite([43(7),22(6),491(6)])]. given #53 (T,wt=7): 529 c2 ^ (c1 v c3) = c2. [para(496(a,1),192(a,1,2))]. given #54 (T,wt=9): 510 c3 v (c1 ^ c2) = c2 v c3. [back_rewrite(260),rewrite([491(10)])]. given #55 (A,wt=13): 50 (c2 v c3) ^ ((c3 v c4) ^ x) = c3 ^ x. [para(27(a,1),21(a,1,1)),flip(a)]. given #56 (T,wt=10): 344 c3 v c4 = c3 | c2 v c3 = c3. [para(208(a,1),27(a,1)),rewrite([23(7),27(7)]),flip(a)]. given #57 (T,wt=10): 388 c1 ^ c2 = c2 | c2 v c3 = c3. [para(308(b,1),152(a,1,2)),rewrite([22(8)])]. given #58 (T,wt=10): 396 c2 ^ c3 = c3 | c3 v c4 = c4. [para(311(b,1),152(a,1,2)),rewrite([22(8)])]. given #59 (T,wt=10): 453 x ^ y = y | y ^ x = x. [para(340(a,1),23(a,1)),flip(b)]. given #60 (A,wt=34): 70 (x v y) ^ (z ^ u) != (x v y) ^ z | u ^ (x v (y v z)) != u | u ^ z = u | u ^ (x v y) = u. [para(20(a,1),34(b,1,2))]. given #61 (T,wt=10): 463 x ^ y = y | y v x = y. [para(340(a,1),152(a,1,2))]. given #62 (T,wt=10): 486 c1 v c2 = c2 | c2 ^ c3 = c3. [para(342(a,1),165(a,1,2)),rewrite([23(8)])]. given #63 (T,wt=10): 540 c1 v c3 = c1 | c2 ^ c3 = c2. [para(204(a,1),529(a,1,2))]. given #64 (T,wt=10): 541 c1 v c3 = c3 | c1 ^ c2 = c2. [para(204(b,1),529(a,1,2)),rewrite([23(8)])]. given #65 (A,wt=40): 73 x ^ (y ^ (z ^ u)) != x ^ y | z ^ (u ^ (x v y)) != z ^ u | z ^ (u ^ y) = z ^ u | z ^ (u ^ x) = z ^ u. [para(21(a,1),34(b,1)),rewrite([21(12),21(16)])]. given #66 (T,wt=10): 542 c1 ^ c3 = c1 | c1 ^ c2 = c2. [para(318(a,1),529(a,1,2)),rewrite([23(8)])]. given #67 (T,wt=10): 543 c1 ^ c3 = c3 | c2 ^ c3 = c2. [para(323(a,1),529(a,1,2)),rewrite([23(3)])]. given #68 (T,wt=10): 571 c2 v c3 = c3 | c3 ^ c4 = c4. [para(344(a,1),165(a,1,2)),rewrite([23(8)])]. given #69 (T,wt=10): 667 x ^ y = y | x v y = y. [para(463(b,1),22(a,1)),flip(b)]. given #70 (A,wt=26): 78 x ^ (y ^ z) != x ^ y | (x v y) ^ z != z | z ^ y = z | z ^ x = z. [para(23(a,1),34(b,1))]. given #71 (T,wt=10): 679 c2 ^ c3 = c3 | c1 ^ c2 = c1. [para(486(a,1),39(a,1,2))]. given #72 (T,wt=10): 767 c1 ^ c3 = c3 | c2 v c3 = c3. [para(543(b,1),26(a,1,1)),rewrite([491(10)])]. given #73 (T,wt=10): 778 c3 ^ c4 = c4 | c2 ^ c3 = c2. [para(571(a,1),39(a,1,2))]. given #74 (T,wt=10): 782 c3 ^ c4 = c4 | c1 v c2 = c2. [para(571(a,1),342(a,1)),unit_del(b,28)]. given #75 (A,wt=36): 80 x ^ (c1 v c2) != x ^ c2 | (c2 v c3) ^ (x v (c1 v c2)) != c2 v c3 | c2 v c3 = c2 | (c2 v c3) ^ x = c2 v c3. [para(25(a,1),34(a,1,2)),rewrite([23(26),25(26)]),flip(a),flip(c)]. given #76 (T,wt=10): 838 c1 ^ c2 = c1 | c2 v c3 = c2. [para(679(a,1),24(a,1,2)),rewrite([22(10),510(10)])]. given #77 (T,wt=10): 846 c1 ^ c2 = c1 | c1 ^ c3 = c3. [para(679(a,1),543(b,1)),unit_del(c,28)]. given #78 (T,wt=10): 852 c1 ^ c3 = c3 | c1 v c2 = c2. [para(767(b,1),342(a,1)),unit_del(b,28)]. given #79 (T,wt=10): 859 c2 ^ c3 = c2 | c3 v c4 = c3. [para(778(a,1),38(a,1,2))]. given #80 (A,wt=36): 84 x ^ (c2 v c3) != x ^ c3 | (c3 v c4) ^ (x v (c2 v c3)) != c3 v c4 | c3 v c4 = c3 | (c3 v c4) ^ x = c3 v c4. [para(27(a,1),34(a,1,2)),rewrite([23(26),27(26)]),flip(a),flip(c)]. given #81 (T,wt=10): 869 c3 ^ c4 = c4 | c1 ^ c2 = c1. [para(782(b,1),39(a,1,2))]. given #82 (T,wt=10): 892 c1 ^ c2 = c1 | c1 v c3 = c1. [para(846(b,1),38(a,1,2))]. given #83 (T,wt=10): 923 c1 ^ c2 = c1 | c3 v c4 = c3. [para(869(a,1),38(a,1,2))]. given #84 (T,wt=11): 149 x v ((x ^ y) v z) = x v z. [para(38(a,1),20(a,1,1)),flip(a)]. given #85 (A,wt=36): 132 (x v y) ^ (z ^ u) != (x v y) ^ z | u ^ (x v (y v z)) != u | (x v y) ^ u = x v y | z ^ u = z. [para(20(a,1),37(b,1,2))]. given #86 (T,wt=11): 163 x ^ ((x v y) ^ z) = x ^ z. [para(39(a,1),21(a,1,1)),flip(a)]. given #87 (T,wt=9): 1145 c1 ^ (c2 v c3) = c1 ^ c2. [para(25(a,1),163(a,1,2)),flip(a)]. given #88 (T,wt=9): 1146 c3 ^ (c1 v c2) = c2 ^ c3. [para(27(a,1),163(a,1,2)),rewrite([366(8)]),flip(a)]. given #89 (T,wt=9): 1175 c2 ^ (c3 v c4) = c2 ^ c3. [back_rewrite(366),rewrite([1146(10)])]. given #90 (A,wt=36): 133 x ^ (y ^ (z ^ u)) != x ^ (y ^ z) | u ^ (x v (y ^ z)) != u | x ^ u = x | y ^ (z ^ u) = y ^ z. [para(21(a,1),37(a,1,2)),rewrite([21(14)])]. given #91 (T,wt=11): 191 x v (y v (x ^ z)) = y v x. [para(38(a,1),43(a,1,2)),flip(a)]. given #92 (T,wt=11): 219 x v ((y ^ x) v z) = x v z. [para(152(a,1),20(a,1,1)),flip(a)]. given #93 (T,wt=11): 223 x v (y v (z ^ x)) = y v x. [para(152(a,1),43(a,1,2)),flip(a)]. given #94 (T,wt=9): 1328 c4 v (c2 ^ c3) = c3 v c4. [para(26(a,1),223(a,1,2)),rewrite([22(3),22(8)]),flip(a)]. given #95 (A,wt=36): 134 x ^ (y ^ (z ^ u)) != x ^ (y ^ z) | u ^ ((x ^ y) v z) != u | x ^ (y ^ u) = x ^ y | z ^ u = z. [para(21(a,1),37(a,1)),rewrite([21(5),21(12)])]. given #96 (T,wt=9): 1340 c2 v (c3 v c4) = c2 v c4. [para(491(a,1),223(a,1,2)),rewrite([43(5),22(4)])]. given #97 (T,wt=7): 1466 c3 ^ (c2 v c4) = c3. [para(1340(a,1),192(a,1,2))]. given #98 (T,wt=10): 1470 c2 v c4 = c2 | c2 ^ c3 = c2. [para(1340(a,1),318(a,1)),rewrite([1175(10)])]. given #99 (T,wt=10): 1479 c2 v c4 = c2 | c3 ^ c4 = c3. [para(204(a,1),1466(a,1,2))]. given #100 (A,wt=36): 135 x ^ (y ^ (z ^ u)) != x ^ y | z ^ (u ^ (x v y)) != z ^ u | x ^ (z ^ u) = x | y ^ (z ^ u) = y. [para(21(a,1),37(b,1))]. given #101 (T,wt=10): 1480 c2 v c4 = c4 | c2 ^ c3 = c3. [para(204(b,1),1466(a,1,2)),rewrite([23(8)])]. given #102 (T,wt=10): 1481 c2 ^ c4 = c2 | c2 ^ c3 = c3. [para(318(a,1),1466(a,1,2)),rewrite([23(8)])]. given #103 (T,wt=10): 1482 c2 ^ c4 = c4 | c3 ^ c4 = c3. [para(323(a,1),1466(a,1,2)),rewrite([23(3)])]. given #104 (T,wt=10): 1488 c2 ^ c3 = c2 | c2 ^ c4 = c4. [para(1470(a,1),165(a,1,2)),rewrite([23(8)])]. given #105 (A,wt=26): 137 x ^ (y ^ z) != x ^ z | y ^ (x v z) != y | x ^ y = x | z ^ y = z. [para(23(a,1),37(a,1,2))]. given #106 (T,wt=10): 1609 c2 ^ c4 = c4 | c3 v c4 = c4. [para(1482(b,1),152(a,1,2)),rewrite([22(8)])]. given #107 (T,wt=10): 1736 x ^ y != y | y ^ x = y. [factor(1632,b,c),rewrite([207(2),174(2),173(5),173(6)]),merge(c)]. given #108 (T,wt=8): 1745 x ^ y = x | y != x. [para(208(a,1),1736(a,1)),merge(c)]. given #109 (T,wt=11): 225 x ^ ((y v x) ^ z) = x ^ z. [para(165(a,1),21(a,1,1)),flip(a)]. given #110 (A,wt=26): 138 x ^ (y ^ z) != z ^ x | y ^ (z v x) != y | z ^ y = z | x ^ y = x. [para(23(a,1),37(a,1)),rewrite([21(2)])]. given #111 (T,wt=11): 238 x ^ (y ^ (x v z)) = y ^ x. [para(39(a,1),44(a,1,2)),flip(a)]. given #112 (T,wt=9): 1911 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(1146(a,1),238(a,1,2)),rewrite([23(8)])]. given #113 (T,wt=7): 1955 c2 v (c1 ^ c3) = c2. [para(1911(a,1),237(a,1,2))]. given #114 (T,wt=10): 1945 c1 ^ c3 = c1 | c1 v c2 = c1. [back_rewrite(414),rewrite([1911(5)])]. given #115 (A,wt=26): 139 x ^ (y ^ z) != y ^ x | z ^ (x v y) != z | x ^ z = x | y ^ z = y. [para(23(a,1),37(a,2))]. given #116 (T,wt=10): 1986 c1 ^ c3 = c1 | c2 v c3 = c2. [para(340(b,1),1955(a,1,2))]. given #117 (T,wt=10): 2039 c1 ^ c3 = c1 | c2 ^ c3 = c3. [para(1986(b,1),27(a,1,1)),rewrite([1175(10)])]. given #118 (T,wt=10): 2044 c1 ^ c3 = c1 | c3 ^ c4 = c4. [para(1986(b,1),571(a,1)),flip(b),unit_del(b,28)]. given #119 (T,wt=10): 2064 c1 ^ c3 = c1 | c3 v c4 = c3. [para(2044(b,1),26(a,1,2)),rewrite([22(10),1328(10)])]. given #120 (A,wt=34): 142 x ^ (c1 v c2) != x ^ c2 | (c2 v c3) ^ (x v (c1 v c2)) != c2 v c3 | x ^ (c2 v c3) = x | c1 v c2 = c2. [para(25(a,1),37(a,1,2)),rewrite([25(31)]),flip(a),flip(d)]. given #121 (T,wt=11): 240 x ^ (y ^ (z v x)) = y ^ x. [para(165(a,1),44(a,1,2)),flip(a)]. given #122 (T,wt=9): 2107 c4 ^ (c2 v c3) = c3 ^ c4. [para(27(a,1),240(a,1,2)),rewrite([23(3),23(8)]),flip(a)]. given #123 (T,wt=9): 2123 c2 ^ (c3 ^ c4) = c2 ^ c4. [para(1175(a,1),240(a,1,2)),rewrite([44(5),23(4)])]. given #124 (T,wt=7): 2191 c3 v (c2 ^ c4) = c3. [para(2123(a,1),237(a,1,2))]. given #125 (A,wt=34): 146 x ^ (c2 v c3) != x ^ c3 | (c3 v c4) ^ (x v (c2 v c3)) != c3 v c4 | x ^ (c3 v c4) = x | c2 v c3 = c3. [para(27(a,1),37(a,1,2)),rewrite([27(31)]),flip(a),flip(d)]. given #126 (T,wt=10): 2162 c2 v c3 = c2 | c2 ^ c4 = c2. [back_rewrite(518),rewrite([2123(10)])]. given #127 (T,wt=10): 2221 c2 ^ c4 = c4 | c2 v c3 = c3. [para(208(a,1),2191(a,1,2)),rewrite([23(3),22(8)])]. given #128 (T,wt=10): 2222 c2 ^ c4 = c2 | c3 v c4 = c3. [para(340(b,1),2191(a,1,2))]. given #129 (T,wt=10): 2252 c2 ^ c4 = c2 | c1 ^ c2 = c2. [para(2162(a,1),388(b,1)),flip(c),unit_del(c,28)]. given #130 (A,wt=13): 150 x v (y v ((x v y) ^ z)) = x v y. [para(38(a,1),20(a,1)),flip(a)]. given #131 (T,wt=10): 2253 c2 ^ c4 = c2 | c3 ^ c4 = c4. [para(2162(a,1),571(a,1)),flip(b),unit_del(b,28)]. given #132 (T,wt=10): 2254 c2 ^ c4 = c2 | c1 ^ c3 = c3. [para(2162(a,1),767(b,1)),flip(c),unit_del(c,28)]. given #133 (T,wt=10): 2264 c2 ^ c4 = c4 | c1 v c2 = c2. [para(2221(b,1),342(a,1)),unit_del(b,28)]. given #134 (T,wt=10): 2265 c2 ^ c4 = c4 | c1 ^ c2 = c1. [para(2221(b,1),838(b,1)),unit_del(c,28)]. given #135 (A,wt=13): 151 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(21(a,1),38(a,1,2))]. given #136 (T,wt=10): 2270 c2 ^ c4 = c4 | c1 ^ c3 = c1. [para(2221(b,1),1986(b,1)),unit_del(c,28)]. given #137 (T,wt=10): 2282 c1 ^ c2 = c2 | c2 v c4 = c4. [para(2252(a,1),152(a,1,2)),rewrite([22(8)])]. given #138 (T,wt=10): 2335 c1 ^ c3 = c3 | c2 v c4 = c4. [para(2254(a,1),152(a,1,2)),rewrite([22(8)])]. given #139 (T,wt=10): 2361 c1 ^ c2 = c1 | c2 v c4 = c2. [para(2265(a,1),38(a,1,2))]. given #140 (A,wt=13): 162 (x v y) ^ (x v (y v z)) = x v y. [para(20(a,1),39(a,1,2))]. given #141 (T,wt=10): 2405 c1 ^ c3 = c1 | c2 v c4 = c2. [para(2270(a,1),38(a,1,2))]. given #142 (T,wt=10): 2423 c1 ^ c2 = c2 | c3 ^ c4 = c3. [para(2282(b,1),1466(a,1,2))]. given #143 (T,wt=10): 2428 c1 ^ c3 = c3 | c3 ^ c4 = c3. [para(2335(b,1),1466(a,1,2))]. given #144 (T,wt=10): 2484 c1 ^ c2 = c2 | c3 v c4 = c4. [para(2423(b,1),152(a,1,2)),rewrite([22(8)])]. given #145 (A,wt=13): 164 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(39(a,1),21(a,1)),flip(a)]. given #146 (T,wt=10): 2504 c1 ^ c3 = c3 | c3 v c4 = c4. [para(2428(b,1),152(a,1,2)),rewrite([22(8)])]. given #147 (T,wt=11): 246 x ^ (y v (z v (x v u))) = x. [para(20(a,1),192(a,1,2))]. given #148 (T,wt=9): 2579 c2 ^ (x v (c1 v c3)) = c2. [para(496(a,1),246(a,1,2,2))]. given #149 (T,wt=9): 2592 c3 ^ (x v (c2 v c4)) = c3. [para(1340(a,1),246(a,1,2,2))]. given #150 (A,wt=25): 169 (y v z) ^ (x v y) != y v z | y v z = y | (y v z) ^ x = y v z. [para(39(a,1),34(a,1,2)),rewrite([23(10),39(10)]),flip(c),xx(a)]. given #151 (T,wt=9): 2611 c2 ^ (c1 v (c3 v x)) = c2. [para(22(a,1),2579(a,1,2)),rewrite([20(5)])]. given #152 (T,wt=9): 2612 c2 ^ (c1 v (x v c3)) = c2. [para(43(a,1),2579(a,1,2))]. given #153 (T,wt=9): 2633 c3 ^ (c2 v (c4 v x)) = c3. [para(22(a,1),2592(a,1,2)),rewrite([20(5)])]. given #154 (T,wt=9): 2634 c3 ^ (c2 v (x v c4)) = c3. [para(43(a,1),2592(a,1,2))]. given #155 (A,wt=13): 185 (c1 ^ c2) v (x v (c2 ^ c3)) = x v c2. [para(24(a,1),43(a,1,2)),flip(a)]. given #156 (T,wt=11): 270 x v (y ^ (z ^ (u ^ x))) = x. [para(21(a,1),221(a,1,2,2))]. given #157 (T,wt=11): 276 x ^ (y v (z v (u v x))) = x. [para(20(a,1),224(a,1,2,2))]. given #158 (T,wt=11): 286 x v (y ^ (z ^ (x ^ u))) = x. [para(21(a,1),237(a,1,2))]. given #159 (T,wt=9): 2879 c2 v (x ^ (c1 ^ c3)) = c2. [para(1911(a,1),286(a,1,2,2))]. given #160 (A,wt=13): 186 (c2 ^ c3) v (x v (c3 ^ c4)) = x v c3. [para(26(a,1),43(a,1,2)),flip(a)]. given #161 (T,wt=9): 2882 c3 v (x ^ (c2 ^ c4)) = c3. [para(2123(a,1),286(a,1,2,2))]. given #162 (T,wt=9): 2888 c2 v (c1 ^ (c3 ^ x)) = c2. [para(23(a,1),2879(a,1,2)),rewrite([21(5)])]. given #163 (T,wt=9): 2891 c2 v (c1 ^ (x ^ c3)) = c2. [para(44(a,1),2879(a,1,2))]. given #164 (T,wt=9): 2930 c3 v (c2 ^ (c4 ^ x)) = c3. [para(23(a,1),2882(a,1,2)),rewrite([21(5)])]. given #165 (A,wt=34): 187 x ^ ((y v z) ^ u) != x ^ (y v z) | u ^ (y v (x v z)) != u | u ^ (y v z) = u | u ^ x = u. [para(43(a,1),34(b,1,2))]. given #166 (T,wt=9): 2933 c3 v (c2 ^ (x ^ c4)) = c3. [para(44(a,1),2882(a,1,2))]. given #167 (T,wt=11): 528 (c1 v c3) ^ (c2 v c3) = c2 v c3. [para(496(a,1),165(a,1,2)),rewrite([23(7)])]. given #168 (T,wt=10): 3112 c1 v c3 = c1 | c2 v c3 = c3. [para(204(a,1),528(a,1,1)),rewrite([165(10)]),flip(b)]. given #169 (T,wt=10): 3127 c1 v c3 = c1 | c1 v c2 = c2. [para(3112(b,1),342(a,1)),unit_del(b,28)]. given #170 (A,wt=13): 220 x v (y v (z ^ (x v y))) = x v y. [para(152(a,1),20(a,1)),flip(a)]. given #171 (T,wt=10): 3132 c1 v c3 = c1 | c2 ^ c4 = c2. [para(3112(b,1),2162(a,1)),unit_del(b,28)]. given #172 (T,wt=11): 537 c2 ^ ((c1 v c3) ^ x) = c2 ^ x. [para(529(a,1),21(a,1,1)),flip(a)]. given #173 (T,wt=11): 538 c2 ^ (x ^ (c1 v c3)) = x ^ c2. [para(529(a,1),44(a,1,2)),flip(a)]. given #174 (T,wt=11): 539 c1 v (c3 v (x ^ c2)) = c1 v c3. [para(529(a,1),221(a,1,2,2)),rewrite([20(6)])]. given #175 (A,wt=13): 226 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(165(a,1),21(a,1)),flip(a)]. given #176 (T,wt=11): 947 (x ^ y) v (z v x) = z v x. [para(195(a,1),149(a,2)),rewrite([254(4)])]. given #177 (T,wt=11): 1151 (x v y) ^ (z ^ x) = z ^ x. [para(207(a,1),163(a,2)),rewrite([266(4)])]. given #178 (T,wt=11): 1311 (x ^ y) v (z v y) = z v y. [para(195(a,1),219(a,2)),rewrite([254(4)])]. given #179 (T,wt=11): 1465 (c2 v c4) ^ (c3 v c4) = c3 v c4. [para(1340(a,1),165(a,1,2)),rewrite([23(7)])]. given #180 (A,wt=25): 227 (z v y) ^ (x v y) != z v y | z v y = y | (z v y) ^ x = z v y. [para(165(a,1),34(a,1,2)),rewrite([23(10),165(10)]),flip(c),xx(a)]. given #181 (T,wt=10): 3434 c2 v c4 = c2 | c3 v c4 = c4. [para(204(a,1),1465(a,1,1)),rewrite([165(10)]),flip(b)]. given #182 (T,wt=11): 1476 c3 ^ ((c2 v c4) ^ x) = c3 ^ x. [para(1466(a,1),21(a,1,1)),flip(a)]. given #183 (T,wt=11): 1477 c3 ^ (x ^ (c2 v c4)) = x ^ c3. [para(1466(a,1),44(a,1,2)),flip(a)]. given #184 (T,wt=11): 1478 c2 v (c4 v (x ^ c3)) = c2 v c4. [para(1466(a,1),221(a,1,2,2)),rewrite([20(6)])]. given #185 (A,wt=13): 228 (x v y) ^ (x v (z v y)) = x v y. [para(43(a,1),165(a,1,2))]. given #186 (T,wt=11): 1751 (x v y) ^ (y v x) = x v y. [resolve(1745,b,22,a)]. given #187 (T,wt=11): 1759 (x v y) ^ (z ^ y) = z ^ y. [para(207(a,1),225(a,2)),rewrite([266(4)])]. given #188 (T,wt=11): 1952 (c1 ^ c3) v (c2 ^ c3) = c2 ^ c3. [para(1911(a,1),152(a,1,2)),rewrite([22(7)])]. given #189 (T,wt=11): 1982 c2 v ((c1 ^ c3) v x) = c2 v x. [para(1955(a,1),20(a,1,1)),flip(a)]. given #190 (A,wt=13): 229 (c1 v c2) ^ (x ^ (c2 v c3)) = x ^ c2. [para(25(a,1),44(a,1,2)),flip(a)]. given #191 (T,wt=11): 1983 (c1 ^ c3) v (x v c2) = x v c2. [para(1955(a,1),20(a,2,2)),rewrite([22(6)])]. given #192 (T,wt=11): 1984 c2 v (x v (c1 ^ c3)) = x v c2. [para(1955(a,1),43(a,1,2)),flip(a)]. given #193 (T,wt=11): 1985 c1 ^ (c3 ^ (x v c2)) = c1 ^ c3. [para(1955(a,1),224(a,1,2,2)),rewrite([21(6)])]. given #194 (T,wt=11): 2188 (c2 ^ c4) v (c3 ^ c4) = c3 ^ c4. [para(2123(a,1),152(a,1,2)),rewrite([22(7)])]. given #195 (A,wt=13): 230 (c2 v c3) ^ (x ^ (c3 v c4)) = x ^ c3. [para(27(a,1),44(a,1,2)),flip(a)]. given #196 (T,wt=11): 2217 c3 v ((c2 ^ c4) v x) = c3 v x. [para(2191(a,1),20(a,1,1)),flip(a)]. given #197 (T,wt=11): 2218 (c2 ^ c4) v (x v c3) = x v c3. [para(2191(a,1),20(a,2,2)),rewrite([22(6)])]. given #198 (T,wt=11): 2219 c3 v (x v (c2 ^ c4)) = x v c3. [para(2191(a,1),43(a,1,2)),flip(a)]. given #199 (T,wt=11): 2220 c2 ^ (c4 ^ (x v c3)) = c2 ^ c4. [para(2191(a,1),224(a,1,2,2)),rewrite([21(6)])]. given #200 (A,wt=36): 234 x ^ (y ^ (z ^ u)) != x ^ z | y ^ (u ^ (x v z)) != y ^ u | x ^ (y ^ u) = x | z ^ (y ^ u) = z. [para(44(a,1),37(a,1,2)),rewrite([21(8)])]. given #201 (T,wt=11): 2381 (x ^ y) v (y ^ x) = x ^ y. [para(207(a,1),151(a,1,2))]. given #202 (T,wt=11): 2396 (c1 ^ c2) v (c1 ^ c3) = c1 ^ c2. [para(1911(a,1),151(a,1,2))]. given #203 (T,wt=11): 2400 (c2 ^ c3) v (c2 ^ c4) = c2 ^ c3. [para(2123(a,1),151(a,1,2))]. given #204 (T,wt=11): 2454 (c1 v c2) ^ (c1 v c3) = c1 v c2. [para(496(a,1),162(a,1,2))]. given #205 (A,wt=26): 235 x ^ (y ^ z) != y ^ x | z ^ (y v x) != z | y ^ z = y | x ^ z = x. [para(44(a,1),37(a,1))]. given #206 (T,wt=10): 4383 c1 v c3 = c3 | c1 v c2 = c1. [para(204(b,1),2454(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #207 (T,wt=10): 4384 c2 ^ c3 = c2 | c1 v c2 = c1. [para(540(a,1),2454(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #208 (T,wt=10): 4391 c2 ^ c4 = c2 | c1 v c2 = c1. [para(3132(a,1),2454(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #209 (T,wt=10): 4459 c1 v c2 = c1 | c2 v c3 = c3. [para(4383(a,1),528(a,1,1)),rewrite([165(10)]),flip(b)]. given #210 (A,wt=36): 236 x ^ (y ^ (z ^ u)) != y ^ (x ^ z) | u ^ (x v (y ^ z)) != u | x ^ u = x | y ^ (z ^ u) = y ^ z. [para(44(a,1),37(a,2)),rewrite([21(2),21(14)])]. given #211 (T,wt=11): 2467 (c2 v c3) ^ (c2 v c4) = c2 v c3. [para(1340(a,1),162(a,1,2))]. given #212 (T,wt=10): 4688 c2 v c4 = c4 | c2 v c3 = c2. [para(204(b,1),2467(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #213 (T,wt=10): 4691 c3 ^ c4 = c3 | c2 v c3 = c2. [para(1479(a,1),2467(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #214 (T,wt=10): 4716 c2 v c3 = c2 | c3 v c4 = c4. [para(4688(a,1),1465(a,1,1)),rewrite([165(10)]),flip(b)]. given #215 (A,wt=13): 239 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(44(a,1),152(a,1,2))]. given #216 (T,wt=10): 4727 c3 ^ c4 = c3 | c1 v c3 = c1. [para(4691(b,1),3112(b,1)),flip(c),unit_del(c,28)]. given #217 (T,wt=10): 4734 c3 ^ c4 = c3 | c1 v c2 = c1. [para(4691(b,1),4459(b,1)),flip(c),unit_del(c,28)]. given #218 (T,wt=11): 2609 c2 ^ (x v (y v (c1 v c3))) = c2. [para(20(a,1),2579(a,1,2))]. given #219 (T,wt=11): 2631 c3 ^ (x v (y v (c2 v c4))) = c3. [para(20(a,1),2592(a,1,2))]. given #220 (A,wt=19): 244 x ^ (y v z) != x ^ y | x ^ y = x | y v z = y. [resolve(192,a,37,b),rewrite([23(2),39(2),23(8),39(8)]),flip(a),flip(c)]. given #221 (T,wt=11): 2687 c2 ^ (c1 v (x v (c3 v y))) = c2. [para(43(a,1),2611(a,1,2,2))]. given #222 (T,wt=11): 2702 c2 ^ (c1 v (x v (y v c3))) = c2. [para(20(a,1),2612(a,1,2,2))]. given #223 (T,wt=11): 2716 c3 ^ (c2 v (x v (c4 v y))) = c3. [para(43(a,1),2633(a,1,2,2))]. given #224 (T,wt=11): 2731 c3 ^ (c2 v (x v (y v c4))) = c3. [para(20(a,1),2634(a,1,2,2))]. given #225 (A,wt=15): 245 (x v y) ^ (z v (x v (y v u))) = x v y. [para(20(a,1),192(a,1,2,2))]. given #226 (T,wt=11): 2887 c2 v (x ^ (y ^ (c1 ^ c3))) = c2. [para(21(a,1),2879(a,1,2))]. given #227 (T,wt=11): 2929 c3 v (x ^ (y ^ (c2 ^ c4))) = c3. [para(21(a,1),2882(a,1,2))]. given #228 (T,wt=11): 2945 c2 v (c1 ^ (x ^ (c3 ^ y))) = c2. [para(44(a,1),2888(a,1,2,2))]. given #229 (T,wt=11): 2956 c2 v (c1 ^ (x ^ (y ^ c3))) = c2. [para(21(a,1),2891(a,1,2,2))]. given #230 (A,wt=13): 247 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(192(a,1),21(a,1,1)),flip(a)]. given #231 (T,wt=11): 2971 c3 v (c2 ^ (x ^ (c4 ^ y))) = c3. [para(44(a,1),2930(a,1,2,2))]. given #232 (T,wt=11): 3097 c3 v (c2 ^ (x ^ (y ^ c4))) = c3. [para(21(a,1),2933(a,1,2,2))]. given #233 (T,wt=11): 3179 c2 ^ (x v (c1 v (c3 v y))) = c2. [para(192(a,1),537(a,1,2)),rewrite([529(5),20(6)]),flip(a)]. given #234 (T,wt=11): 3180 (c1 v c3) ^ (x ^ c2) = x ^ c2. [para(207(a,1),537(a,2)),rewrite([266(8)])]. given #235 (A,wt=15): 248 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(192(a,1),21(a,1)),flip(a)]. given #236 (T,wt=11): 3182 c1 v (c3 v (c2 ^ x)) = c1 v c3. [para(537(a,1),237(a,1,2)),rewrite([20(6)])]. given #237 (T,wt=11): 3311 c2 v (x ^ (c1 ^ (c3 ^ y))) = c2. [para(2879(a,1),947(a,1,2)),rewrite([21(5),21(4),22(7),2879(13)])]. given #238 (T,wt=11): 3312 c3 v (x ^ (c2 ^ (c4 ^ y))) = c3. [para(2882(a,1),947(a,1,2)),rewrite([21(5),21(4),22(7),2882(13)])]. given #239 (T,wt=11): 3359 c3 ^ (x v (c2 v (c4 v y))) = c3. [para(2592(a,1),1151(a,1,2)),rewrite([20(5),20(4),23(7),2592(13)])]. given #240 (A,wt=35): 249 (z v (y v u)) ^ (x v y) != z v (y v u) | z v (y v u) = y | (z v (y v u)) ^ x = z v (y v u). [para(192(a,1),34(a,1,2)),rewrite([23(13),192(13)]),flip(c),xx(a)]. given #241 (T,wt=11): 3420 c2 v (x ^ (c1 ^ (y ^ c3))) = c2. [para(2891(a,1),1311(a,1,2)),rewrite([22(7),2891(13)])]. given #242 (T,wt=11): 3421 c3 v (x ^ (c2 ^ (y ^ c4))) = c3. [para(2933(a,1),1311(a,1,2)),rewrite([22(7),2933(13)])]. given #243 (T,wt=11): 3526 (c2 v c4) ^ (x ^ c3) = x ^ c3. [para(207(a,1),1476(a,2)),rewrite([266(8)])]. given #244 (T,wt=11): 3528 c2 v (c4 v (c3 ^ x)) = c2 v c4. [para(1476(a,1),237(a,1,2)),rewrite([20(6)])]. given #245 (A,wt=13): 251 x v (y v (x v z)) = y v (x v z). [para(192(a,1),152(a,1,2)),rewrite([22(3)])]. given #246 (T,wt=11): 3715 c2 ^ (x v (c1 v (y v c3))) = c2. [para(2612(a,1),1759(a,1,2)),rewrite([23(7),2612(13)])]. given #247 (T,wt=11): 3716 c3 ^ (x v (c2 v (y v c4))) = c3. [para(2634(a,1),1759(a,1,2)),rewrite([23(7),2634(13)])]. given #248 (T,wt=11): 3749 c1 ^ (c3 ^ (c2 v x)) = c1 ^ c3. [para(1982(a,1),192(a,1,2)),rewrite([21(6)])]. given #249 (T,wt=11): 3881 c2 ^ (c4 ^ (c3 v x)) = c2 ^ c4. [para(2217(a,1),192(a,1,2)),rewrite([21(6)])]. given #250 (A,wt=13): 252 x ^ (y ^ (z v (x v u))) = y ^ x. [para(192(a,1),44(a,1,2)),flip(a)]. given #251 (T,wt=12): 324 x v y = x | x ^ (z v y) = x. [para(204(a,1),192(a,1,2,2))]. given #252 (T,wt=10): 6247 c1 ^ c3 = c1 | c1 v c4 = c1. [factor(6109,a,c)]. given #253 (T,wt=10): 6248 c1 ^ c2 = c1 | c1 v c4 = c1. [factor(6120,a,c)]. given #254 (T,wt=10): 6255 c1 ^ c3 = c1 | c1 ^ c4 = c4. [para(6247(b,1),165(a,1,2)),rewrite([23(8)])]. given #255 (A,wt=13): 254 x v (y v (z v x)) = y v (z v x). [para(20(a,1),195(a,1,2)),rewrite([20(5)])]. given #256 (T,wt=9): 6316 c2 ^ (c3 v (x v c1)) = c2. [para(254(a,1),2611(a,1,2))]. given #257 (T,wt=9): 6317 c3 ^ (c4 v (x v c2)) = c3. [para(254(a,1),2633(a,1,2))]. given #258 (T,wt=10): 6274 c1 ^ c2 = c1 | c1 ^ c4 = c4. [para(6248(b,1),165(a,1,2)),rewrite([23(8)])]. given #259 (T,wt=11): 6333 c2 ^ (x v (c3 v (y v c1))) = c2. [para(254(a,1),3179(a,1,2,2))]. given #260 (A,wt=13): 256 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(205(a,1),21(a,2,2)),rewrite([44(3),21(2)])]. given #261 (T,wt=11): 6337 c3 ^ (x v (c4 v (y v c2))) = c3. [para(254(a,1),3359(a,1,2,2))]. given #262 (T,wt=11): 6344 c2 ^ (c3 v (x v (y v c1))) = c2. [para(20(a,1),6316(a,1,2,2))]. given #263 (T,wt=11): 6360 c2 ^ (c3 v (x v (c1 v y))) = c2. [para(6316(a,1),1151(a,1,2)),rewrite([20(5),20(4),23(7),6316(13)])]. given #264 (T,wt=11): 6370 c3 ^ (c4 v (x v (y v c2))) = c3. [para(20(a,1),6317(a,1,2,2))]. given #265 (A,wt=21): 257 x ^ (y ^ z) != x ^ y | x ^ (y ^ z) = x | y ^ z = y. [para(205(a,1),37(a,1,2)),rewrite([21(7),240(7),205(12)]),unit_del(b,23)]. given #266 (T,wt=11): 6386 c3 ^ (c4 v (x v (c2 v y))) = c3. [para(6317(a,1),1151(a,1,2)),rewrite([20(5),20(4),23(7),6317(13)])]. given #267 (T,wt=12): 329 x v y = y | y ^ (z v x) = y. [para(204(b,1),224(a,1,2,2))]. given #268 (T,wt=12): 334 c1 v c2 = c1 | c1 v c2 = c2 ^ c3. [para(204(a,1),291(a,1)),rewrite([291(5)]),flip(b)]. given #269 (T,wt=12): 352 x ^ y = x | x v (z ^ y) = x. [para(208(a,1),221(a,1,2,2))]. given #270 (A,wt=23): 258 x ^ (y ^ z) != y | x ^ (z ^ y) != x ^ z | y ^ (x ^ z) = y. [back_rewrite(241),rewrite([256(3)])]. given #271 (T,wt=12): 390 c1 ^ c2 = c2 | c3 v (x ^ c2) = c3. [para(308(b,1),221(a,1,2,2))]. given #272 (T,wt=12): 398 c2 ^ c3 = c3 | c4 v (x ^ c3) = c4. [para(311(b,1),221(a,1,2,2))]. given #273 (T,wt=12): 409 x ^ (y v z) = x | y ^ x = y. [para(318(a,1),192(a,1,2))]. given #274 (T,wt=12): 411 x ^ y = x | y ^ (z v x) = y. [para(318(a,1),224(a,1,2,2))]. given #275 (A,wt=17): 259 (c2 ^ c3) v (x v ((c1 ^ c2) v y)) = x v (c2 v y). [para(45(a,1),20(a,2,2)),rewrite([43(9),20(8)])]. given #276 (T,wt=10): 7608 c2 ^ c4 = c2 | c1 ^ c4 = c4. [factor(7541,a,b),rewrite([23(8)])]. given #277 (T,wt=10): 7609 c3 ^ c4 = c3 | c1 ^ c4 = c4. [factor(7546,a,b),rewrite([23(8)])]. given #278 (T,wt=10): 7679 c1 ^ c4 = c4 | c2 v c4 = c4. [para(7608(a,1),152(a,1,2)),rewrite([22(8)])]. given #279 (T,wt=10): 7686 c1 ^ c4 = c4 | c2 v c3 = c3. [para(7608(a,1),2191(a,1,2)),rewrite([22(8)])]. given #280 (A,wt=44): 261 c1 ^ (c2 ^ (((c2 ^ c3) v x) ^ y)) != c1 ^ (c2 ^ ((c2 ^ c3) v x)) | y ^ (c2 v x) != y | y ^ ((c2 ^ c3) v x) = y | y ^ (c1 ^ c2) = y. [para(45(a,1),34(b,1,2)),rewrite([21(9),21(17)])]. given #281 (T,wt=10): 7699 c1 ^ c4 = c4 | c2 ^ c3 = c2. [para(7608(a,1),2400(a,1,2)),rewrite([22(10),38(10)]),flip(b)]. given #282 (T,wt=10): 7709 c1 ^ c4 = c4 | c3 v c4 = c4. [para(7609(a,1),152(a,1,2)),rewrite([22(8)])]. given #283 (T,wt=10): 7743 c1 ^ c4 = c4 | c1 v c2 = c2. [para(7686(b,1),342(a,1)),unit_del(b,28)]. given #284 (T,wt=12): 469 x ^ y = y | y v (z ^ x) = y. [para(340(a,1),221(a,1,2,2))]. given #285 (A,wt=17): 263 (c1 ^ c2) v (x v ((c2 ^ c3) v y)) = x v (c2 v y). [para(45(a,1),43(a,1,2)),flip(a)]. given #286 (T,wt=12): 473 c2 ^ c3 = c2 | c1 v c3 = c1 v c2. [para(340(b,1),291(a,1,2))]. given #287 (T,wt=12): 488 c1 v c2 = c2 | c3 ^ (x v c2) = c3. [para(342(a,1),224(a,1,2,2))]. given #288 (T,wt=12): 517 c2 v c3 = c3 ^ c4 | c2 v c3 = c2. [para(491(a,1),204(a,1)),rewrite([491(12)])]. given #289 (T,wt=12): 520 c3 ^ c4 = c3 | c2 v c4 = c2 v c3. [para(340(b,1),491(a,1,2))]. given #290 (A,wt=13): 266 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(21(a,1),207(a,1,2)),rewrite([21(5)])]. given #291 (T,wt=9): 8201 c2 v (c3 ^ (x ^ c1)) = c2. [para(266(a,1),2888(a,1,2))]. given #292 (T,wt=9): 8202 c3 v (c4 ^ (x ^ c2)) = c3. [para(266(a,1),2930(a,1,2))]. given #293 (T,wt=11): 8217 c2 v (x ^ (c3 ^ (y ^ c1))) = c2. [para(266(a,1),3311(a,1,2,2))]. given #294 (T,wt=11): 8218 c3 v (x ^ (c4 ^ (y ^ c2))) = c3. [para(266(a,1),3312(a,1,2,2))]. given #295 (A,wt=21): 267 x ^ (y ^ z) != x ^ z | x ^ (y ^ z) = x | y ^ z = z. [para(207(a,1),37(a,1,2)),rewrite([21(7),165(6),207(12)]),xx(b)]. given #296 (T,wt=11): 8257 c2 v (c3 ^ (x ^ (y ^ c1))) = c2. [para(21(a,1),8201(a,1,2,2))]. given #297 (T,wt=11): 8267 c2 v (c3 ^ (x ^ (c1 ^ y))) = c2. [para(8201(a,1),947(a,1,2)),rewrite([21(5),21(4),22(7),8201(13)])]. given #298 (T,wt=11): 8283 c3 v (c4 ^ (x ^ (y ^ c2))) = c3. [para(21(a,1),8202(a,1,2,2))]. given #299 (T,wt=11): 8293 c3 v (c4 ^ (x ^ (c2 ^ y))) = c3. [para(8202(a,1),947(a,1,2)),rewrite([21(5),21(4),22(7),8202(13)])]. given #300 (A,wt=13): 268 x v ((y ^ (z ^ x)) v u) = x v u. [para(221(a,1),20(a,1,1)),flip(a)]. given #301 (T,wt=12): 531 c2 v c3 = c1 v c3 | c1 v c3 = c1. [para(496(a,1),204(a,1)),rewrite([496(12)]),flip(a)]. given #302 (T,wt=12): 532 c2 v c3 = c3 | c1 v c3 = c1 v c2. [para(204(b,1),496(a,1,2)),flip(b)]. given #303 (T,wt=12): 535 c1 v c2 = c2 | c1 v c3 = c1 v c2. [para(342(a,1),496(a,1,2)),flip(b)]. given #304 (T,wt=12): 547 c2 v c3 = c1 ^ c2 | c2 v c3 = c3. [para(510(a,1),204(a,1)),rewrite([510(12)])]. given #305 (A,wt=15): 269 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(221(a,1),20(a,1)),flip(a)]. given #306 (T,wt=12): 548 c1 ^ c2 = c2 | c2 v c3 = c1 v c3. [para(208(a,1),510(a,1,2)),rewrite([23(3),22(8)]),flip(b)]. given #307 (T,wt=12): 572 c2 v c3 = c3 | c4 ^ (x v c3) = c4. [para(344(a,1),224(a,1,2,2))]. given #308 (T,wt=12): 577 c1 ^ c2 = c2 | c2 ^ (x v c3) = c2. [para(388(b,1),192(a,1,2,2))]. given #309 (T,wt=12): 583 c2 ^ c3 = c3 | c3 ^ (x v c4) = c3. [para(396(b,1),192(a,1,2,2))]. given #310 (A,wt=13): 272 x v (y v (z ^ (u ^ x))) = y v x. [para(221(a,1),43(a,1,2)),flip(a)]. given #311 (T,wt=12): 671 (x v y) ^ z = z | x ^ z = x. [para(463(b,1),192(a,1,2))]. given #312 (T,wt=10): 9119 c2 ^ c4 = c4 | c1 ^ c4 = c1. [factor(9054,a,b)]. given #313 (T,wt=10): 9122 c1 ^ c4 = c1 | c2 v c4 = c2. [para(9119(a,1),38(a,1,2))]. given #314 (T,wt=10): 9128 c1 ^ c4 = c1 | c3 v c4 = c3. [para(9119(a,1),2191(a,1,2))]. given #315 (A,wt=15): 273 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(44(a,1),221(a,1,2,2))]. given #316 (T,wt=10): 9135 c1 ^ c4 = c1 | c3 ^ c4 = c4. [para(9119(a,1),2188(a,1,1)),rewrite([152(10)]),flip(b)]. given #317 (T,wt=10): 9150 c1 ^ c4 = c1 | c2 ^ c3 = c3. [para(9122(b,1),1466(a,1,2)),rewrite([23(8)])]. given #318 (T,wt=10): 9159 c1 ^ c4 = c1 | c2 v c3 = c2. [para(9122(b,1),2467(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. given #319 (T,wt=10): 9320 c1 ^ c4 = c1 | c1 ^ c2 = c2. [para(9150(b,1),308(b,1)),unit_del(c,28)]. given #320 (A,wt=19): 275 x ^ (y v z) != x ^ z | x ^ z = x | y v z = z. [resolve(224,a,37,b),rewrite([23(2),165(2),23(8),165(8)]),flip(a),flip(c)]. given #321 (T,wt=10): 9321 c1 ^ c4 = c1 | c1 ^ c3 = c3. [para(9150(b,1),543(b,1)),unit_del(c,28)]. given #322 (T,wt=10): 9336 c1 ^ c4 = c1 | c1 v c3 = c1. [para(9159(b,1),3112(b,1)),flip(c),unit_del(c,28)]. given #323 (T,wt=10): 9341 c1 ^ c4 = c1 | c1 v c2 = c1. [para(9159(b,1),4459(b,1)),flip(c),unit_del(c,28)]. given #324 (T,wt=10): 9350 c1 ^ c2 = c2 | c1 v c4 = c4. [para(9320(a,1),152(a,1,2)),rewrite([22(8)])]. given #325 (A,wt=13): 277 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(224(a,1),21(a,1,1)),flip(a)]. given #326 (T,wt=10): 9516 c1 ^ c3 = c3 | c1 v c4 = c4. [para(9321(a,1),152(a,1,2)),rewrite([22(8)])]. given #327 (T,wt=12): 672 x ^ y = y | x ^ (z v y) = x. [para(463(b,1),224(a,1,2,2))]. given #328 (T,wt=12): 673 (x v y) ^ z = z | y ^ z = y. [para(463(b,1),224(a,1,2))]. given #329 (T,wt=12): 681 c2 ^ c3 = c3 | c1 ^ (x v c2) = c1. [para(486(a,1),192(a,1,2,2))]. given #330 (A,wt=15): 278 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(224(a,1),21(a,1)),flip(a)]. given #331 (T,wt=12): 686 c2 ^ c3 = c2 | c3 ^ (x v c1) = c3. [para(540(a,1),224(a,1,2,2))]. given #332 (T,wt=12): 691 c1 ^ c2 = c2 | c1 ^ (x v c3) = c1. [para(541(a,1),192(a,1,2,2))]. given #333 (T,wt=12): 764 c1 ^ c2 = c2 | c3 v (x ^ c1) = c3. [para(542(a,1),221(a,1,2,2))]. given #334 (T,wt=12): 770 c1 ^ c3 = c3 | c3 v (x ^ c2) = c3. [para(543(b,1),221(a,1,2,2))]. given #335 (A,wt=35): 279 (z v (u v y)) ^ (x v y) != z v (u v y) | z v (u v y) = y | (z v (u v y)) ^ x = z v (u v y). [para(224(a,1),34(a,1,2)),rewrite([23(13),224(13)]),flip(c),xx(a)]. given #336 (T,wt=12): 780 c3 ^ c4 = c4 | c2 ^ (x v c3) = c2. [para(571(a,1),192(a,1,2,2))]. given #337 (T,wt=12): 842 c1 ^ c2 = c1 | c2 v (x ^ c3) = c2. [para(679(a,1),237(a,1,2,2))]. given #338 (T,wt=12): 844 c1 ^ c2 = c1 | c1 v c3 = c1 v c2. [para(679(a,1),291(a,1,2))]. given #339 (T,wt=12): 850 c1 ^ c3 = c3 | c2 ^ (x v c3) = c2. [para(767(b,1),192(a,1,2,2))]. given #340 (A,wt=15): 280 (x v y) ^ (z v (x v (u v y))) = x v y. [para(43(a,1),224(a,1,2,2))]. given #341 (T,wt=12): 861 c2 ^ c3 = c2 | c3 v (x ^ c4) = c3. [para(778(a,1),237(a,1,2,2))]. given #342 (T,wt=12): 864 c2 ^ c3 = c2 | c2 v c4 = c2 v c3. [para(778(a,1),491(a,1,2))]. given #343 (T,wt=12): 871 c3 ^ c4 = c4 | c1 ^ (x v c2) = c1. [para(782(b,1),192(a,1,2,2))]. given #344 (T,wt=12): 885 c1 ^ c2 = c1 | c3 ^ (x v c2) = c3. [para(838(b,1),224(a,1,2,2))]. given #345 (A,wt=13): 281 x ^ (y ^ (z v (u v x))) = y ^ x. [para(224(a,1),44(a,1,2)),flip(a)]. given #346 (T,wt=12): 894 c1 ^ c2 = c1 | c1 v (x ^ c3) = c1. [para(846(b,1),237(a,1,2,2))]. given #347 (T,wt=12): 899 c1 ^ c3 = c3 | c1 ^ (x v c2) = c1. [para(852(b,1),192(a,1,2,2))]. given #348 (T,wt=12): 905 c2 ^ c3 = c2 | c4 ^ (x v c3) = c4. [para(859(b,1),224(a,1,2,2))]. given #349 (T,wt=12): 925 c1 ^ c2 = c1 | c3 v (x ^ c4) = c3. [para(869(a,1),237(a,1,2,2))]. given #350 (A,wt=13): 283 x v ((y ^ (x ^ z)) v u) = x v u. [para(237(a,1),20(a,1,1)),flip(a)]. given #351 (T,wt=12): 928 c1 ^ c2 = c1 | c2 v c4 = c2 v c3. [para(869(a,1),491(a,1,2))]. given #352 (T,wt=12): 934 c1 ^ c2 = c1 | c3 ^ (x v c1) = c3. [para(892(b,1),224(a,1,2,2))]. given #353 (T,wt=12): 940 c1 ^ c2 = c1 | c4 ^ (x v c3) = c4. [para(923(b,1),224(a,1,2,2))]. given #354 (T,wt=12): 950 (x ^ y) v z = z | x v z = x. [para(204(b,1),149(a,1,2)),rewrite([38(5)]),flip(b)]. given #355 (A,wt=15): 284 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(237(a,1),20(a,1)),flip(a)]. given #356 (T,wt=12): 951 x v (y ^ z) = x | y v x = y. [para(306(a,1),149(a,1,2)),rewrite([38(5)]),flip(b)]. given #357 (T,wt=12): 1185 c2 v c3 = c2 | c1 ^ c3 = c1 ^ c2. [para(204(a,1),1145(a,1,2))]. given #358 (T,wt=12): 1186 c1 ^ c2 = c1 | c2 v c3 = c1 ^ c2. [para(1145(a,1),208(a,1)),rewrite([23(10),1145(10)]),flip(b)]. given #359 (T,wt=12): 1187 c2 ^ c3 = c3 | c1 ^ c3 = c1 ^ c2. [para(323(a,1),1145(a,1,2)),rewrite([23(3)])]. given #360 (A,wt=15): 285 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(21(a,1),237(a,1,2,2))]. given #361 (T,wt=12): 1188 c1 ^ c2 = c2 | c1 ^ c3 = c1 ^ c2. [para(388(b,1),1145(a,1,2))]. given #362 (T,wt=12): 1189 c3 ^ c4 = c4 | c1 ^ c3 = c1 ^ c2. [para(571(a,1),1145(a,1,2))]. given #363 (T,wt=12): 1190 c1 ^ c3 = c3 | c1 ^ c3 = c1 ^ c2. [para(767(b,1),1145(a,1,2))]. given #364 (T,wt=10): 11853 c1 ^ c3 = c3 | c1 ^ c2 != c3. [para(1190(b,1),1736(a,1)),rewrite([23(13)]),merge(c)]. given #365 (A,wt=13): 287 x v (y v (z ^ (x ^ u))) = y v x. [para(237(a,1),43(a,1,2)),flip(a)]. Low Water (keep, True_semantics): wt=71 given #366 (T,wt=12): 1195 c1 v c2 = c2 | c2 ^ c3 = c1 ^ c3. [para(204(b,1),1146(a,1,2)),rewrite([23(8)]),flip(b)]. given #367 (T,wt=12): 1196 c2 ^ c3 = c3 | c1 v c2 = c2 ^ c3. [para(1146(a,1),208(a,1)),rewrite([23(10),1146(10)]),flip(b)]. given #368 (T,wt=12): 1197 c1 ^ c2 = c1 | c2 ^ c3 = c1 ^ c3. [para(318(a,1),1146(a,1,2)),rewrite([23(8)]),flip(b)]. given #369 (T,wt=12): 1203 c3 v c4 = c3 | c2 ^ c4 = c2 ^ c3. [para(204(a,1),1175(a,1,2))]. given #370 (A,wt=17): 288 (c2 ^ c3) v (x v (y v (c1 ^ c2))) = c2 v (x v y). [para(20(a,1),46(a,1,2)),rewrite([22(12)])]. Low Water (keep, True_semantics): wt=65 given #371 (T,wt=12): 1204 c2 ^ c3 = c2 | c3 v c4 = c2 ^ c3. [para(1175(a,1),208(a,1)),rewrite([23(10),1175(10)]),flip(b)]. given #372 (T,wt=12): 1205 c3 ^ c4 = c4 | c2 ^ c4 = c2 ^ c3. [para(323(a,1),1175(a,1,2)),rewrite([23(3)])]. given #373 (T,wt=12): 1206 c2 ^ c3 = c3 | c2 ^ c4 = c2 ^ c3. [para(396(b,1),1175(a,1,2))]. given #374 (T,wt=12): 1298 x v (y ^ z) = x | x v y = y. [para(204(a,1),191(a,1,2)),rewrite([38(5)]),flip(b)]. given #375 (A,wt=44): 289 c2 ^ (c3 ^ ((x v (c1 ^ c2)) ^ y)) != c2 ^ (c3 ^ (x v (c1 ^ c2))) | y ^ (x v c2) != y | y ^ (x v (c1 ^ c2)) = y | y ^ (c2 ^ c3) = y. [para(46(a,1),34(b,1,2)),rewrite([21(9),21(17)])]. Low Water (keep, True_semantics): wt=58 Low Water (keep, True_semantics): wt=55 Low Water (keep, True_semantics): wt=54 given #376 (T,wt=12): 1299 (x ^ y) v z = z | z v x = x. [para(307(a,1),191(a,1,2)),rewrite([38(5)]),flip(b)]. given #377 (T,wt=12): 1316 (x ^ y) v z = z | y v z = y. [para(204(b,1),219(a,1,2)),rewrite([152(5)]),flip(b)]. Low Water (keep, True_semantics): wt=50 given #378 (T,wt=12): 1317 x v (y ^ z) = x | z v x = z. [para(306(a,1),219(a,1,2)),rewrite([152(5)]),flip(b)]. given #379 (T,wt=12): 1334 x v (y ^ z) = x | x v z = z. [para(204(a,1),223(a,1,2)),rewrite([152(5)]),flip(b)]. Low Water (keep, True_semantics): wt=47 given #380 (A,wt=13): 296 c1 v ((c2 ^ c3) v x) = c1 v (c2 v x). [para(291(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. given #381 (T,wt=11): 13170 c1 v (c3 v c4) = c1 v (c2 v c4). [para(1340(a,1),296(a,2,2)),rewrite([43(8),22(7),1328(7),193(6)])]. given #382 (T,wt=12): 1336 (x ^ y) v z = z | z v y = y. [para(307(a,1),223(a,1,2)),rewrite([152(5)]),flip(b)]. given #383 (T,wt=12): 1355 c3 v c4 = c2 ^ c3 | c3 v c4 = c4. [para(1328(a,1),204(a,1)),rewrite([1328(12)])]. given #384 (T,wt=12): 1356 c2 ^ c3 = c3 | c3 v c4 = c2 v c4. [para(208(a,1),1328(a,1,2)),rewrite([23(3),22(8)]),flip(b)]. given #385 (A,wt=14): 301 x v y = x | x v (y v z) = y v z. [para(204(a,1),20(a,1,1)),flip(b)]. given #386 (T,wt=12): 1357 c1 ^ c2 = c2 | c3 v c4 = c2 v c4. [para(308(b,1),1328(a,1,2)),rewrite([22(8)]),flip(b)]. given #387 (T,wt=12): 1360 c1 ^ c3 = c3 | c3 v c4 = c2 v c4. [para(543(b,1),1328(a,1,2)),rewrite([22(8)]),flip(b)]. given #388 (T,wt=12): 1468 c3 v c4 = c2 v c4 | c2 v c4 = c2. [para(1340(a,1),204(a,1)),rewrite([1340(12)]),flip(a)]. Low Water (keep, True_semantics): wt=41 given #389 (T,wt=10): 13969 c2 v c4 = c2 | c2 v c3 = c3. [para(1468(a,1),27(a,1,2)),rewrite([2467(12)])]. given #390 (A,wt=16): 302 x v (y v z) = x v y | x v (y v z) = z. [para(204(a,1),20(a,1)),rewrite([20(2)]),flip(b)]. given #391 (T,wt=12): 1469 c3 v c4 = c4 | c2 v c4 = c2 v c3. [para(204(b,1),1340(a,1,2)),flip(b)]. Low Water (keep, True_semantics): wt=40 given #392 (T,wt=12): 1472 c2 v c3 = c3 | c2 v c4 = c2 v c3. [para(344(a,1),1340(a,1,2)),flip(b)]. given #393 (T,wt=12): 1489 c2 ^ c3 = c2 | c4 ^ (x v c2) = c4. [para(1470(a,1),224(a,1,2,2))]. given #394 (T,wt=12): 1500 c3 ^ c4 = c3 | c4 ^ (x v c2) = c4. [para(1479(a,1),224(a,1,2,2))]. given #395 (A,wt=14): 303 x v y = x | z v (x v y) = z v y. [para(204(a,1),20(a,2,2)),rewrite([20(4)])]. Low Water (keep, True_semantics): wt=39 given #396 (T,wt=12): 1595 c2 ^ c3 = c3 | c2 ^ (x v c4) = c2. [para(1480(a,1),192(a,1,2,2))]. given #397 (T,wt=12): 1600 c2 ^ c3 = c3 | c4 v (x ^ c2) = c4. [para(1481(a,1),221(a,1,2,2))]. given #398 (T,wt=12): 1611 c2 ^ c4 = c4 | c4 v (x ^ c3) = c4. [para(1482(b,1),221(a,1,2,2))]. given #399 (T,wt=12): 1624 c2 ^ c3 = c2 | c2 v (x ^ c4) = c2. [para(1488(b,1),237(a,1,2,2))]. given #400 (A,wt=14): 304 x v y = y | x v (y v z) = x v z. [para(204(b,1),20(a,1,1)),flip(b)]. given #401 (T,wt=12): 1738 c2 ^ c4 = c4 | c3 ^ (x v c4) = c3. [para(1609(b,1),192(a,1,2,2))]. given #402 (T,wt=12): 1741 c2 ^ c4 = c4 | c2 ^ c4 = c2 ^ c3. [para(1609(b,1),1175(a,1,2))]. given #403 (T,wt=10): 15348 c2 ^ c4 = c4 | c2 ^ c3 != c4. [para(1741(b,1),1736(a,1)),rewrite([23(13)]),merge(c)]. given #404 (T,wt=12): 1903 x ^ (y v z) = x | x ^ y = y. [para(340(b,1),238(a,1,2)),rewrite([39(5)]),flip(b)]. given #405 (A,wt=14): 305 x v y = y | z v (x v y) = z v x. [para(204(b,1),20(a,2,2)),rewrite([20(4)])]. Low Water (keep, True_semantics): wt=38 given #406 (T,wt=12): 1905 (x v y) ^ z = z | z ^ x = x. [para(453(a,1),238(a,1,2)),rewrite([39(5)]),flip(b)]. Low Water (keep, True_semantics): wt=36 given #407 (T,wt=12): 1944 c2 ^ c3 = c1 ^ c3 | c2 ^ c3 = c2. [back_rewrite(432),rewrite([1911(5)]),flip(a)]. given #408 (T,wt=12): 1956 c1 ^ c3 = c1 | c2 ^ c3 = c1 ^ c3. [para(1911(a,1),208(a,1)),rewrite([23(10),1911(10)]),flip(b)]. given #409 (T,wt=12): 1992 c1 ^ c3 = c1 | c2 ^ (x v c1) = c2. [para(1945(b,1),224(a,1,2,2))]. given #410 (A,wt=25): 314 (c1 ^ c3) v (c3 ^ c4) = c1 ^ c3 | c3 ^ c4 != c3 | (c1 v c3) ^ (c3 v c4) != c3. [para(204(a,1),29(a,1))]. Low Water (keep, True_semantics): wt=34 given #411 (T,wt=12): 2041 c1 ^ c3 = c1 | c3 ^ (x v c2) = c3. [para(1986(b,1),224(a,1,2,2))]. Low Water (keep, True_semantics): wt=32 given #412 (T,wt=12): 2042 c1 ^ c3 = c1 | c1 v c3 = c1 v c2. [para(1986(b,1),496(a,1,2)),flip(b)]. given #413 (T,wt=12): 2050 c1 ^ c3 = c1 | c2 v (x ^ c3) = c2. [para(2039(b,1),237(a,1,2,2))]. given #414 (T,wt=12): 2066 c1 ^ c3 = c1 | c3 v (x ^ c4) = c3. [para(2044(b,1),237(a,1,2,2))]. given #415 (A,wt=25): 315 (c1 ^ c3) v (c3 ^ c4) = c3 ^ c4 | c1 ^ c3 != c3 | (c1 v c3) ^ (c3 v c4) != c3. [para(204(b,1),29(a,1))]. given #416 (T,wt=12): 2069 c1 ^ c3 = c1 | c2 v c4 = c2 v c3. [para(2044(b,1),491(a,1,2))]. Low Water (keep, True_semantics): wt=31 given #417 (T,wt=12): 2083 c1 ^ c3 = c1 | c4 ^ (x v c3) = c4. [para(2064(b,1),224(a,1,2,2))]. given #418 (T,wt=12): 2119 (x v y) ^ z = z | z ^ y = y. [para(453(a,1),240(a,1,2)),rewrite([165(5)]),flip(b)]. given #419 (T,wt=12): 2164 c3 ^ c4 = c2 ^ c4 | c3 ^ c4 = c3. [back_rewrite(434),rewrite([2123(5)]),flip(a)]. given #420 (A,wt=14): 319 x v y = x | x v (z v y) = z v y. [para(204(a,1),43(a,1,2)),flip(b)]. given #421 (T,wt=12): 2169 c2 v c3 = c3 | c3 ^ c4 = c2 ^ c4. [para(204(b,1),2107(a,1,2)),rewrite([23(8)]),flip(b)]. Low Water (keep, True_semantics): wt=30 given #422 (T,wt=12): 2170 c3 ^ c4 = c4 | c2 v c3 = c3 ^ c4. [para(2107(a,1),208(a,1)),rewrite([23(10),2107(10)]),flip(b)]. given #423 (T,wt=12): 2171 c2 ^ c3 = c2 | c3 ^ c4 = c2 ^ c4. [para(318(a,1),2107(a,1,2)),rewrite([23(8)]),flip(b)]. Low Water (keep, True_semantics): wt=28 given #424 (T,wt=12): 2172 c1 v c2 = c2 | c3 ^ c4 = c2 ^ c4. [para(342(a,1),2107(a,1,2)),rewrite([23(8)]),flip(b)]. given #425 (A,wt=16): 320 x v (y v z) = x | y v (x v z) = y v z. [para(204(a,1),43(a,1)),flip(b)]. given #426 (T,wt=12): 2173 c1 ^ c2 = c1 | c3 ^ c4 = c2 ^ c4. [para(838(b,1),2107(a,1,2)),rewrite([23(8)]),flip(b)]. Low Water (keep, True_semantics): wt=26 given #427 (T,wt=12): 2184 c1 ^ c3 = c1 | c3 ^ c4 = c2 ^ c4. [para(1986(b,1),2107(a,1,2)),rewrite([23(8)]),flip(b)]. given #428 (T,wt=12): 2192 c2 ^ c4 = c2 | c3 ^ c4 = c2 ^ c4. [para(2123(a,1),208(a,1)),rewrite([23(10),2123(10)]),flip(b)]. given #429 (T,wt=12): 2249 c2 ^ c4 = c2 | c3 ^ (x v c2) = c3. [para(2162(a,1),224(a,1,2,2))]. given #430 (A,wt=14): 321 x v y = y | x v (z v y) = z v x. [para(204(b,1),43(a,1,2)),flip(b)]. Low Water (keep, True_semantics): wt=25 given #431 (T,wt=12): 2250 c2 ^ c4 = c2 | c1 v c3 = c1 v c2. [para(2162(a,1),496(a,1,2)),flip(b)]. Low Water (keep, True_semantics): wt=24 given #432 (T,wt=12): 2262 c2 ^ c4 = c4 | c2 ^ (x v c3) = c2. [para(2221(b,1),192(a,1,2,2))]. given #433 (T,wt=12): 2266 c2 ^ c4 = c4 | c1 ^ c3 = c1 ^ c2. [para(2221(b,1),1145(a,1,2))]. given #434 (T,wt=12): 2274 c2 ^ c4 = c2 | c4 ^ (x v c3) = c4. [para(2222(b,1),224(a,1,2,2))]. given #435 (A,wt=16): 322 x v (y v z) = y v z | y v (x v z) = x. [para(204(b,1),43(a,1)),flip(b)]. given #436 (T,wt=12): 2275 c2 ^ c4 = c2 | c2 v c4 = c2 v c3. [para(2222(b,1),1340(a,1,2)),flip(b)]. given #437 (T,wt=12): 2284 c1 ^ c2 = c2 | c4 v (x ^ c2) = c4. [para(2252(a,1),221(a,1,2,2))]. Low Water (keep, True_semantics): wt=23 given #438 (T,wt=12): 2321 c2 ^ c4 = c2 | c3 v (x ^ c4) = c3. [para(2253(b,1),237(a,1,2,2))]. given #439 (T,wt=12): 2337 c1 ^ c3 = c3 | c4 v (x ^ c2) = c4. [para(2254(a,1),221(a,1,2,2))]. given #440 (A,wt=14): 325 x v (y v z) = y v z | y ^ x = y. [para(204(b,1),192(a,1,2))]. Low Water (keep, True_semantics): wt=22 given #441 (T,wt=12): 2354 c2 ^ c4 = c4 | c1 ^ (x v c2) = c1. [para(2264(b,1),192(a,1,2,2))]. given #442 (T,wt=12): 2363 c1 ^ c2 = c1 | c2 v (x ^ c4) = c2. [para(2265(a,1),237(a,1,2,2))]. given #443 (T,wt=12): 2407 c1 ^ c3 = c1 | c2 v (x ^ c4) = c2. [para(2270(a,1),237(a,1,2,2))]. given #444 (T,wt=12): 2422 c1 ^ c2 = c2 | c2 ^ (x v c4) = c2. [para(2282(b,1),192(a,1,2,2))]. given #445 (A,wt=18): 326 (c2 ^ c3) v x = c2 ^ c3 | (c1 ^ c2) v x = c2 v x. [para(204(a,1),45(a,1,2))]. given #446 (T,wt=12): 2427 c1 ^ c3 = c3 | c2 ^ (x v c4) = c2. [para(2335(b,1),192(a,1,2,2))]. Low Water (keep, True_semantics): wt=21 given #447 (T,wt=12): 2432 c1 ^ c2 = c1 | c4 ^ (x v c2) = c4. [para(2361(b,1),224(a,1,2,2))]. given #448 (T,wt=12): 2448 x ^ (y v z) = x | x v y = x. [para(318(a,1),162(a,1,2)),rewrite([23(5),39(5)]),flip(b)]. given #449 (T,wt=10): 19087 c1 v c3 = c3 | c2 ^ c3 = c3. [para(2448(a,1),1146(a,1)),rewrite([22(3)]),flip(b)]. given #450 (A,wt=16): 327 c2 v x = c1 ^ c2 | (c2 ^ c3) v x = c2 v x. [para(204(a,1),45(a,1)),rewrite([45(8)])]. given #451 (T,wt=10): 19093 c2 v c4 = c4 | c3 ^ c4 = c4. [para(2448(a,1),2107(a,1)),rewrite([22(3)]),flip(b)]. given #452 (T,wt=12): 2457 (x v y) ^ z = z | z v x = z. [para(463(b,1),162(a,1,2)),rewrite([23(5),39(5)]),flip(b)]. given #453 (T,wt=10): 19516 c2 ^ c4 = c4 | c1 v c4 = c4. [factor(19386,a,b),rewrite([22(8)])]. given #454 (T,wt=12): 2478 c1 ^ c3 = c1 | c4 ^ (x v c2) = c4. [para(2405(b,1),224(a,1,2,2))]. given #455 (A,wt=14): 330 x v (y v z) = y v z | z ^ x = z. [para(204(b,1),224(a,1,2))]. given #456 (T,wt=12): 2486 c1 ^ c2 = c2 | c4 v (x ^ c3) = c4. [para(2423(b,1),221(a,1,2,2))]. Low Water (keep, True_semantics): wt=20 given #457 (T,wt=12): 2500 c1 ^ c2 = c2 | c2 ^ c4 = c2 ^ c3. [para(2423(b,1),2123(a,1,2)),flip(b)]. given #458 (T,wt=12): 2506 c1 ^ c3 = c3 | c4 v (x ^ c3) = c4. [para(2428(b,1),221(a,1,2,2))]. given #459 (T,wt=12): 2520 c1 ^ c3 = c3 | c2 ^ c4 = c2 ^ c3. [para(2428(b,1),2123(a,1,2)),flip(b)]. given #460 (A,wt=16): 332 x v c2 = c2 ^ c3 | x v (c1 ^ c2) = x v c2. [para(204(a,1),46(a,1)),rewrite([46(8)])]. given #461 (T,wt=12): 2522 c1 ^ c2 = c2 | c3 ^ (x v c4) = c3. [para(2484(b,1),192(a,1,2,2))]. given #462 (T,wt=12): 2557 c1 ^ c3 = c3 | c3 ^ (x v c4) = c3. [para(2504(b,1),192(a,1,2,2))]. given #463 (T,wt=12): 2615 c1 v c3 = c1 | c2 ^ (x v c3) = c2. [para(204(a,1),2579(a,1,2,2))]. given #464 (T,wt=12): 2616 c1 v c3 = c3 | c2 ^ (x v c1) = c2. [para(204(b,1),2579(a,1,2,2))]. given #465 (A,wt=18): 333 x v (c1 ^ c2) = c1 ^ c2 | (c2 ^ c3) v x = x v c2. [para(204(b,1),46(a,1,2))]. given #466 (T,wt=12): 2619 x ^ (c1 v c3) = x | c2 ^ x = c2. [para(318(a,1),2579(a,1,2))]. given #467 (T,wt=12): 2620 (c1 v c3) ^ x = x | c2 ^ x = c2. [para(463(b,1),2579(a,1,2))]. given #468 (T,wt=12): 2621 c2 ^ c3 = c2 | c2 ^ (x v c1) = c2. [para(540(a,1),2579(a,1,2,2))]. given #469 (T,wt=12): 2627 c1 ^ c2 = c1 | c3 v c4 = c2 ^ c3. [back_rewrite(1172),rewrite([2611(12)]),xx(b)]. given #470 (A,wt=28): 336 (x v y) ^ z = x v y | x ^ (y ^ z) != x ^ y | z ^ y = z | z ^ x = z. [resolve(208,a,34,b)]. given #471 (T,wt=12): 2637 c2 v c4 = c2 | c3 ^ (x v c4) = c3. [para(204(a,1),2592(a,1,2,2))]. given #472 (T,wt=12): 2638 c2 v c4 = c4 | c3 ^ (x v c2) = c3. [para(204(b,1),2592(a,1,2,2))]. given #473 (T,wt=12): 2641 x ^ (c2 v c4) = x | c3 ^ x = c3. [para(318(a,1),2592(a,1,2))]. given #474 (T,wt=12): 2642 (c2 v c4) ^ x = x | c3 ^ x = c3. [para(463(b,1),2592(a,1,2))]. given #475 (A,wt=14): 337 x ^ y = x | y ^ (x ^ z) = y ^ z. [para(208(a,1),21(a,1,1)),flip(b)]. given #476 (T,wt=12): 2645 c3 ^ c4 = c3 | c3 ^ (x v c2) = c3. [para(1479(a,1),2592(a,1,2,2))]. Low Water (keep, True_semantics): wt=19 given #477 (T,wt=12): 2690 c3 v x = c3 | c2 ^ (c1 v x) = c2. [para(204(a,1),2611(a,1,2,2))]. given #478 (T,wt=12): 2692 x v c3 = c3 | c2 ^ (c1 v x) = c2. [para(307(a,1),2611(a,1,2,2))]. given #479 (T,wt=12): 2693 c1 ^ (c3 v x) = c1 | c1 ^ c2 = c2. [para(318(a,1),2611(a,1,2)),rewrite([23(9)])]. given #480 (A,wt=16): 338 x ^ (y ^ z) = x | y ^ (z ^ x) = y ^ z. [para(208(a,1),21(a,1)),flip(b)]. given #481 (T,wt=12): 2694 x ^ c3 = x | c2 ^ (c1 v x) = c2. [para(323(a,1),2611(a,1,2,2))]. given #482 (T,wt=12): 2696 c3 ^ x = x | c2 ^ (c1 v x) = c2. [para(667(b,1),2611(a,1,2,2))]. given #483 (T,wt=12): 2719 c4 v x = c4 | c3 ^ (c2 v x) = c3. [para(204(a,1),2633(a,1,2,2))]. given #484 (T,wt=12): 2721 x v c4 = c4 | c3 ^ (c2 v x) = c3. [para(307(a,1),2633(a,1,2,2))]. given #485 (A,wt=14): 339 x ^ y = x | z ^ (y ^ x) = z ^ y. [para(208(a,1),21(a,2,2)),rewrite([21(4)])]. given #486 (T,wt=12): 2722 c2 ^ (c4 v x) = c2 | c2 ^ c3 = c3. [para(318(a,1),2633(a,1,2)),rewrite([23(9)])]. given #487 (T,wt=12): 2723 x ^ c4 = x | c3 ^ (c2 v x) = c3. [para(323(a,1),2633(a,1,2,2))]. given #488 (T,wt=12): 2725 c4 ^ x = x | c3 ^ (c2 v x) = c3. [para(667(b,1),2633(a,1,2,2))]. given #489 (T,wt=12): 2892 c1 ^ c3 = c3 | c2 v (x ^ c1) = c2. [para(208(a,1),2879(a,1,2,2)),rewrite([23(3)])]. given #490 (A,wt=14): 346 c3 ^ c4 = c4 | (c1 v c3) ^ (c3 v c4) != c3. [para(208(a,1),29(a,1,2)),rewrite([23(3),22(10),152(10)]),xx(b)]. given #491 (T,wt=10): 21374 c1 v c3 = c1 | c3 ^ c4 = c4. [para(204(a,1),346(b,1,1)),rewrite([39(15)]),xx(c)]. given #492 (T,wt=10): 21377 c1 ^ c3 = c3 | c3 ^ c4 = c4. [para(323(a,1),346(b,1,1)),rewrite([23(3),39(15)]),xx(c)]. given #493 (T,wt=8): 21443 c1 ^ c3 = c3 | c4 = c3. [para(21377(b,1),2428(b,1)),merge(b)]. given #494 (T,wt=8): 21459 c4 = c3 | c1 v c3 = c1. [para(21443(a,1),38(a,1,2))]. given #495 (A,wt=17): 347 x ^ y = x | x ^ (z v y) != x | x ^ z = x. [para(208(a,1),34(a,1,2)),xx(b),merge(c)]. given #496 (T,wt=8): 21465 c4 = c3 | c2 v c3 = c2. [para(21443(a,1),1955(a,1,2))]. given #497 (T,wt=8): 21470 c4 = c3 | c2 ^ c3 = c3. [para(21443(a,1),1952(a,1,1)),rewrite([152(8)]),flip(b)]. given #498 (T,wt=8): 21492 c4 = c3 | c1 ^ c2 = c2. [para(21459(b,1),529(a,1,2)),rewrite([23(6)])]. given #499 (T,wt=8): 21501 c4 = c3 | c1 v c2 = c1. [para(21459(b,1),2454(a,1,2)),rewrite([23(8),39(8)]),flip(b)]. given #500 (A,wt=29): 348 x ^ y = x | y ^ (x ^ z) != y | z ^ (y v x) != z | y ^ z = y | x ^ z = x. [para(208(a,1),37(a,2))]. given #501 (T,wt=8): 21540 c4 = c3 | c3 ^ c4 = c4. [para(21465(b,1),571(a,1)),flip(b),unit_del(b,28)]. given #502 (T,wt=8): 21543 c4 = c3 | c2 ^ c4 = c4. [para(21465(b,1),2221(b,1)),flip(c),unit_del(c,28)]. given #503 (T,wt=8): 21554 c4 = c3 | c1 ^ c4 = c4. [para(21465(b,1),7686(b,1)),flip(c),unit_del(c,28)]. given #504 (T,wt=8): 21650 c4 = c3 | c3 v c4 = c3. [para(21540(b,1),26(a,1,2)),rewrite([22(8),1328(8)])]. given #505 (A,wt=14): 349 x ^ y = x | y ^ (z ^ x) = z ^ y. [para(208(a,1),44(a,1,2)),flip(b)]. given #506 (T,wt=8): 21677 c4 = c3 | c2 v c4 = c2. [para(21543(b,1),38(a,1,2))]. given #507 (T,wt=8): 21703 c4 = c3 | c1 v c4 = c1. [para(21554(b,1),38(a,1,2))]. given #508 (T,wt=10): 21379 c1 ^ c2 = c2 | c3 ^ c4 = c4. [para(541(a,1),346(b,1,1)),rewrite([39(15)]),xx(c)]. given #509 (T,wt=10): 21380 c1 v c2 = c1 | c3 ^ c4 = c4. [para(4383(a,1),346(b,1,1)),rewrite([39(15)]),xx(c)]. given #510 (A,wt=16): 350 x ^ (y ^ z) = x ^ y | x ^ (z ^ y) = z. [para(208(a,1),44(a,1)),rewrite([21(2)]),flip(b)]. given #511 (T,wt=8): 21972 c3 ^ c4 = c4 | c2 = c1. [para(21380(a,1),782(b,1)),flip(c),merge(b)]. given #512 (T,wt=8): 22109 c2 = c1 | c3 v c4 = c3. [para(21972(a,1),26(a,1,2)),rewrite([22(8),1328(8)])]. given #513 (T,wt=10): 21386 c2 ^ c3 = c3 | c3 ^ c4 = c4. [para(19087(a,1),346(b,1,1)),rewrite([39(15)]),xx(c)]. given #514 (T,wt=10): 21432 c1 ^ c3 = c3 | c3 v c4 = c3. [para(21377(b,1),26(a,1,2)),rewrite([22(10),1328(10)])]. Low Water (keep, True_semantics): wt=18 given #515 (A,wt=14): 353 x ^ (y ^ z) = x ^ y | y v z = y. [para(208(a,1),221(a,1,2)),rewrite([21(2)])]. given #516 (T,wt=10): 21461 c4 = c3 | c1 v (x ^ c3) = c1. [para(21443(a,1),237(a,1,2,2))]. given #517 (T,wt=10): 21468 c4 = c3 | c2 v (x ^ c3) = c2. [para(21443(a,1),2879(a,1,2,2))]. given #518 (T,wt=10): 21474 c4 = c3 | c2 v c3 = c1 ^ c2. [para(21443(a,1),2396(a,1,2)),rewrite([22(8),510(8)])]. given #519 (T,wt=10): 21491 c4 = c3 | c3 ^ (x v c1) = c3. [para(21459(b,1),224(a,1,2,2))]. given #520 (A,wt=14): 354 x ^ (y ^ z) = x ^ y | x v z = x. [para(208(a,1),237(a,1,2)),rewrite([21(2)])]. Low Water (displace, True_semantics): id=12342, wt=53 Low Water (displace, True_semantics): id=12300, wt=52 Low Water (displace, True_semantics): id=12341, wt=51 Low Water (displace, True_semantics): id=12476, wt=50 Low Water (displace, True_semantics): id=12343, wt=49 Low Water (displace, True_semantics): id=12708, wt=48 Low Water (displace, True_semantics): id=12853, wt=47 Low Water (displace, True_semantics): id=13473, wt=46 Low Water (displace, True_semantics): id=12338, wt=44 Low Water (displace, True_semantics): id=13477, wt=42 Low Water (displace, True_semantics): id=13949, wt=41 Low Water (displace, True_semantics): id=14245, wt=40 given #521 (T,wt=10): 21493 c4 = c3 | c2 ^ (x v c1) = c2. [para(21459(b,1),2579(a,1,2,2))]. Low Water (displace, True_semantics): id=14094, wt=39 given #522 (T,wt=10): 21513 c4 = c3 | c1 v c3 = c1 v c2. [para(21459(b,1),288(a,2,2)),rewrite([510(12),496(11),43(10),22(9),152(9),22(9)])]. Low Water (displace, True_semantics): id=15220, wt=38 Low Water (displace, True_semantics): id=15497, wt=37 Low Water (displace, True_semantics): id=13222, wt=35 Low Water (displace, True_semantics): id=15873, wt=34 Low Water (displace, True_semantics): id=14371, wt=33 given #523 (T,wt=10): 21538 c4 = c3 | c3 ^ (x v c2) = c3. [para(21465(b,1),224(a,1,2,2))]. Low Water (displace, True_semantics): id=16065, wt=32 given #524 (T,wt=10): 21542 c4 = c3 | c3 ^ c4 = c2 ^ c4. [para(21465(b,1),2107(a,1,2)),rewrite([23(6)]),flip(b)]. Low Water (displace, True_semantics): id=16130, wt=31 Low Water (displace, True_semantics): id=16535, wt=30 given #525 (A,wt=14): 356 x v y = x | y v (x v z) = y v z. [para(306(a,1),20(a,1,1)),flip(b)]. Low Water (displace, True_semantics): id=13231, wt=29 Low Water (displace, True_semantics): id=16606, wt=28 Low Water (displace, True_semantics): id=17495, wt=27 Low Water (displace, True_semantics): id=17348, wt=26 given #526 (T,wt=10): 21555 c4 = c3 | c4 ^ (x v c3) = c4. [para(21465(b,1),572(a,1)),flip(b),unit_del(b,28)]. given #527 (T,wt=10): 21561 c4 = c3 | c2 v (c3 ^ x) = c2. [para(21465(b,1),1299(b,1)),rewrite([22(7)]),flip(c),unit_del(c,28)]. Low Water (displace, True_semantics): id=17487, wt=25 given #528 (T,wt=10): 21581 c4 = c3 | c3 ^ (c2 v x) = c3. [para(21470(b,1),409(b,1)),unit_del(c,28)]. given #529 (T,wt=10): 21597 c4 = c3 | c1 v (x ^ c2) = c1. [para(21492(b,1),237(a,1,2,2))]. given #530 (A,wt=16): 357 x v (y v z) = x | y v (z v x) = y v z. [para(306(a,1),20(a,1)),flip(b)]. Low Water (displace, True_semantics): id=17789, wt=24 given #531 (T,wt=10): 21616 c4 = c3 | c2 ^ c3 = c1 ^ c3. [para(21501(b,1),1146(a,1,2)),rewrite([23(6)]),flip(b)]. given #532 (T,wt=10): 21652 c4 = c3 | c3 v (x ^ c4) = c3. [para(21540(b,1),237(a,1,2,2))]. given #533 (T,wt=10): 21655 c4 = c3 | c2 v c4 = c2 v c3. [para(21540(b,1),491(a,1,2))]. given #534 (T,wt=10): 21663 c4 = c3 | c4 ^ (c3 v x) = c4. [para(21540(b,1),409(b,1)),merge(c)]. given #535 (A,wt=14): 358 x v y = x | z v (y v x) = z v y. [para(306(a,1),20(a,2,2)),rewrite([20(4)])]. Low Water (displace, True_semantics): id=18375, wt=23 given #536 (T,wt=10): 21679 c4 = c3 | c2 v (x ^ c4) = c2. [para(21543(b,1),237(a,1,2,2))]. given #537 (T,wt=10): 21685 c4 = c3 | c3 v c4 = c2 ^ c3. [para(21543(b,1),2400(a,1,2)),rewrite([22(8),1328(8)])]. given #538 (T,wt=10): 21705 c4 = c3 | c1 v (x ^ c4) = c1. [para(21554(b,1),237(a,1,2,2))]. given #539 (T,wt=10): 21738 c4 = c3 | c3 v (c4 ^ x) = c3. [para(21650(b,1),1299(b,1)),rewrite([22(7)]),flip(c),merge(c)]. given #540 (A,wt=14): 360 x v y = x | y v (z v x) = z v y. [para(306(a,1),43(a,1,2)),flip(b)]. given #541 (T,wt=10): 21878 c4 = c3 | c4 ^ (x v c2) = c4. [para(21677(b,1),224(a,1,2,2))]. Low Water (displace, True_semantics): id=18497, wt=22 given #542 (T,wt=10): 21912 c4 = c3 | c4 ^ (x v c1) = c4. [para(21703(b,1),224(a,1,2,2))]. given #543 (T,wt=10): 21947 c1 ^ c2 = c2 | c3 v c4 = c3. [para(21379(b,1),26(a,1,2)),rewrite([22(10),1328(10)])]. given #544 (T,wt=10): 22111 c2 = c1 | c3 v (x ^ c4) = c3. [para(21972(a,1),237(a,1,2,2))]. given #545 (A,wt=16): 361 x v (y v z) = x v y | x v (z v y) = z. [para(306(a,1),43(a,1)),rewrite([20(2)]),flip(b)]. given #546 (T,wt=10): 22114 c2 = c1 | c2 v c4 = c2 v c3. [para(21972(a,1),491(a,1,2))]. given #547 (T,wt=10): 22118 c2 = c1 | c2 v (c1 ^ c4) = c2. [para(21972(a,1),2888(a,1,2,2))]. given #548 (T,wt=10): 22137 c2 = c1 | c4 ^ (x v c3) = c4. [para(22109(b,1),224(a,1,2,2))]. given #549 (T,wt=10): 22176 c2 ^ c3 = c3 | c3 v c4 = c3. [para(21386(b,1),26(a,1,2)),rewrite([22(10),1328(10)])]. given #550 (A,wt=14): 362 x v (y v z) = x v y | x ^ z = x. [para(306(a,1),192(a,1,2)),rewrite([20(2)])]. Low Water (displace, True_semantics): id=19024, wt=21 given #551 (T,wt=10): 22218 c1 ^ c3 = c3 | c2 v c4 = c3. [para(21432(b,1),1360(b,1)),flip(c),merge(b)]. given #552 (T,wt=10): 22344 c4 = c3 | c1 v (c3 ^ x) = c1. [para(23(a,1),21461(b,1,2))]. given #553 (T,wt=10): 22453 c4 = c3 | c3 ^ (c1 v x) = c3. [para(22(a,1),21491(b,1,2))]. given #554 (T,wt=10): 22644 c4 = c3 | c2 ^ (c1 v x) = c2. [para(22(a,1),21493(b,1,2))]. given #555 (A,wt=14): 364 x v (y v z) = x v y | y ^ z = y. [para(306(a,1),224(a,1,2)),rewrite([20(2)])]. given #556 (T,wt=10): 22939 c4 = c3 | c1 ^ (c2 ^ c4) = c4. [para(21474(b,1),21555(b,1,2)),rewrite([44(11),23(10)]),merge(b)]. given #557 (T,wt=10): 22993 c4 = c3 | c1 v (c2 ^ x) = c1. [para(23(a,1),21597(b,1,2))]. given #558 (T,wt=10): 23119 c4 = c3 | c2 v c4 = c1 ^ c2. [para(21474(b,1),21655(b,2)),merge(b)]. given #559 (T,wt=10): 23262 c4 = c3 | c2 v (c4 ^ x) = c2. [para(23(a,1),21679(b,1,2))]. given #560 (A,wt=18): 365 (c1 ^ c2) v x = c1 ^ c2 | (c2 ^ c3) v x = x v c2. [para(306(a,1),46(a,1,2))]. given #561 (T,wt=10): 23337 c4 = c3 | c3 v c4 = c1 ^ c3. [para(21616(b,1),21685(b,2)),merge(b)]. given #562 (T,wt=10): 23340 c4 = c3 | c1 v (c4 ^ x) = c1. [para(23(a,1),21705(b,1,2))]. given #563 (T,wt=10): 23469 c4 = c3 | c4 ^ (c2 v x) = c4. [para(22(a,1),21878(b,1,2))]. Low Water (keep, True_semantics): wt=17 given #564 (T,wt=10): 23498 c4 = c3 | c4 ^ (c1 v x) = c4. [para(22(a,1),21912(b,1,2))]. given #565 (A,wt=44): 367 x ^ (c1 v c2) != x ^ (c2 ^ y) | (c2 v c3) ^ (y ^ (x v (c1 v c2))) != (c2 v c3) ^ y | x ^ ((c2 v c3) ^ y) = x | c1 v c2 = c2 ^ y. [para(47(a,1),37(a,1,2)),rewrite([21(17),47(36)]),flip(a),flip(d)]. given #566 (T,wt=10): 23544 c1 ^ c2 = c2 | c2 v c4 = c3. [para(21947(b,1),1357(b,1)),flip(c),merge(b)]. given #567 (T,wt=10): 23560 c2 = c1 | c3 v (c4 ^ x) = c3. [para(23(a,1),22111(b,1,2))]. given #568 (T,wt=10): 23709 c2 = c1 | c4 ^ (c3 v x) = c4. [para(22(a,1),22137(b,1,2))]. given #569 (T,wt=10): 23753 c2 ^ c3 = c3 | c2 v c4 = c3. [para(22176(b,1),1356(b,1)),flip(c),merge(b)]. Low Water (displace, True_semantics): id=19819, wt=20 given #570 (A,wt=44): 368 c2 ^ (x ^ y) != c2 ^ x | y ^ (c1 v (c2 v ((c2 v c3) ^ x))) != y | (c1 v c2) ^ y = c1 v c2 | (c2 v c3) ^ (x ^ y) = (c2 v c3) ^ x. [para(47(a,1),37(a,2)),rewrite([21(8),47(9),20(14),21(29)])]. given #571 (T,wt=10): 24199 c4 = c3 | c1 v (c2 v c4) = c1. [para(23119(b,1),296(a,2,2)),rewrite([22(9),1328(9),13170(8),38(13)])]. given #572 (T,wt=10): 24250 c4 = c3 | c1 ^ (c3 ^ c4) = c4. [para(23337(b,1),165(a,1,2)),rewrite([44(8),23(7)])]. given #573 (T,wt=12): 2934 c2 ^ c4 = c4 | c3 v (x ^ c2) = c3. [para(208(a,1),2882(a,1,2,2)),rewrite([23(3)])]. given #574 (T,wt=12): 2948 c3 ^ x = c3 | c2 v (c1 ^ x) = c2. [para(340(b,1),2888(a,1,2,2))]. given #575 (A,wt=17): 370 (c1 v c2) ^ (x ^ ((c2 v c3) ^ y)) = x ^ (c2 ^ y). [para(47(a,1),44(a,1,2)),flip(a)]. given #576 (T,wt=12): 2950 x ^ c3 = c3 | c2 v (c1 ^ x) = c2. [para(453(a,1),2888(a,1,2,2))]. given #577 (T,wt=12): 2974 c4 ^ x = c4 | c3 v (c2 ^ x) = c3. [para(340(b,1),2930(a,1,2,2))]. given #578 (T,wt=12): 2976 x ^ c4 = c4 | c3 v (c2 ^ x) = c3. [para(453(a,1),2930(a,1,2,2))]. given #579 (T,wt=12): 3113 c1 v c3 = c3 | c2 v c3 = c1 ^ c2. [para(204(b,1),528(a,1,1)),rewrite([1145(10)]),flip(b)]. given #580 (A,wt=16): 374 c1 v c2 = c2 ^ x | (c2 v c3) ^ x = c2 ^ x. [para(47(a,1),208(a,1)),rewrite([23(14),47(14)]),flip(a),flip(b)]. given #581 (T,wt=10): 24500 c1 v c3 = c3 | c2 v c3 = c2. [para(3113(b,1),193(a,1,2)),rewrite([152(10)]),flip(b)]. given #582 (T,wt=10): 24535 c1 v c3 = c3 | c3 ^ c4 = c4. [para(24500(b,1),571(a,1)),flip(b),unit_del(b,28)]. ============================== PROOF ================================= % Proof 1 at 15.29 (+ 0.04) seconds. % Length of proof is 101. % Level of proof is 21. % Maximum clause weight is 26. % Given clauses 582. 1 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause). [assumption]. 2 (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)) # label(non_clause). [assumption]. 3 (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)) # label(non_clause). [assumption]. 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)) # label(non_clause). [assumption]. 7 (all x all y all z (A(x,y,z) <-> x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y)) # label(non_clause). [expand_def(2,1)]. 8 (all x all y all z (D(x,y,z) <-> (x ^ z) ^ y = x ^ z & y ^ (x v z) = y)) # label(non_clause). [expand_def(6,1)]. 9 -D(x,y,z) | A(x,y,z) # label(non_clause). [assumption]. 10 -D(x,y,z) | x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y # label(non_clause). [expand_def(9,7)]. 11 B(x,y,z) & B(y,z,u) & y != z -> B(x,z,u) # label(non_clause). [goal]. 12 -((x ^ z) ^ y = x ^ z & y ^ (x v z) = y) | x ^ y = x & y ^ z = y | z ^ y = z & y ^ x = y # label(non_clause). [expand_def(10,8)]. 13 ((x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y) & ((y ^ z) v (z ^ u) = z & (y v z) ^ (z v u) = z) & y != z -> (x ^ z) v (z ^ u) = z & (x v z) ^ (z v u) = z # label(non_clause) # label(goal). [expand_def(11,3)]. 15 (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | x ^ z = x | z ^ x = z. [clausify(12)]. 17 (x ^ y) ^ z != x ^ y | z ^ (x v y) != z | z ^ y = z | z ^ x = z. [clausify(12)]. 18 (x ^ y) v x = x # label("absorption_2"). [assumption]. 19 (x v y) ^ x = x # label("absorption_1"). [assumption]. 20 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 21 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 22 x v y = y v x # label("commutativity_join"). [assumption]. 23 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 24 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(13)]. 25 (c1 v c2) ^ (c2 v c3) = c2. [deny(13)]. 26 (c2 ^ c3) v (c3 ^ c4) = c3. [deny(13)]. 27 (c2 v c3) ^ (c3 v c4) = c3. [deny(13)]. 28 c3 != c2. [deny(13)]. 29 (c1 ^ c3) v (c3 ^ c4) != c3 | (c1 v c3) ^ (c3 v c4) != c3. [deny(13)]. 34 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | z ^ y = z | z ^ x = z. [back_rewrite(17),rewrite([21(2)])]. 36 x ^ (y ^ z) != x ^ y | z ^ (x v y) != z | x ^ z = x | z ^ x = z. [back_rewrite(15),rewrite([21(2)])]. 38 x v (x ^ y) = x. [back_rewrite(18),rewrite([22(2)])]. 39 x ^ (x v y) = x. [back_rewrite(19),rewrite([23(2)])]. 43 x v (y v z) = y v (x v z). [para(22(a,1),20(a,1,1)),rewrite([20(2)])]. 44 x ^ (y ^ z) = y ^ (x ^ z). [para(23(a,1),21(a,1,1)),rewrite([21(2)])]. 46 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(24(a,1),20(a,2,2)),rewrite([22(8)])]. 47 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(25(a,1),21(a,1,1)),flip(a)]. 49 (c3 ^ c4) v (x v (c2 ^ c3)) = x v c3. [para(26(a,1),20(a,2,2)),rewrite([22(8)])]. 152 x v (y ^ x) = x. [para(23(a,1),38(a,1,2))]. 162 (x v y) ^ (x v (y v z)) = x v y. [para(20(a,1),39(a,1,2))]. 163 x ^ ((x v y) ^ z) = x ^ z. [para(39(a,1),21(a,1,1)),flip(a)]. 165 x ^ (y v x) = x. [para(22(a,1),39(a,1,2))]. 173 x v x = x. [para(39(a,1),38(a,1,2))]. 174 x ^ x = x. [para(38(a,1),39(a,1,2))]. 192 x ^ (y v (x v z)) = x. [para(43(a,1),39(a,1,2))]. 193 x v (x v y) = x v y. [para(173(a,1),20(a,1,1)),flip(a)]. 204 x v y = y | x v y = x. [resolve(174,a,34,b),rewrite([165(2),23(5),165(5),23(7),39(7)]),flip(b),flip(c),xx(a)]. 208 x ^ y = x | y ^ x = y. [para(174(a,1),36(a,1,2)),rewrite([165(5)]),xx(a),xx(b)]. 223 x v (y v (z ^ x)) = y v x. [para(152(a,1),43(a,1,2)),flip(a)]. 224 x ^ (y v (z v x)) = x. [para(20(a,1),165(a,1,2))]. 240 x ^ (y ^ (z v x)) = y ^ x. [para(165(a,1),44(a,1,2)),flip(a)]. 291 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),46(a,1,2)),rewrite([22(5)])]. 318 x v y = x | x ^ y = x. [para(204(a,1),39(a,1,2))]. 323 x v y = y | y ^ x = y. [para(204(b,1),165(a,1,2))]. 340 x ^ y = x | x ^ y = y. [para(208(a,1),23(a,1)),flip(b)]. 344 c3 v c4 = c3 | c2 v c3 = c3. [para(208(a,1),27(a,1)),rewrite([23(7),27(7)]),flip(a)]. 346 c3 ^ c4 = c4 | (c1 v c3) ^ (c3 v c4) != c3. [para(208(a,1),29(a,1,2)),rewrite([23(3),22(10),152(10)]),xx(b)]. 366 c2 ^ (c3 v c4) = c3 ^ (c1 v c2). [para(27(a,1),47(a,1,2)),rewrite([23(5)]),flip(a)]. 411 x ^ y = x | y ^ (z v x) = y. [para(318(a,1),224(a,1,2,2))]. 456 c1 ^ c3 = c1 | (c1 v c3) ^ (c3 v c4) != c3. [para(340(b,1),29(a,1,1)),rewrite([38(10)]),xx(b)]. 491 c2 v (c3 ^ c4) = c2 v c3. [para(38(a,1),49(a,1,2)),rewrite([22(5)])]. 496 c1 v (c2 v c3) = c1 v c3. [para(291(a,1),49(a,1,2)),rewrite([43(7),22(6),491(6)])]. 518 c2 v c3 = c2 | c2 ^ (c3 ^ c4) = c2. [para(491(a,1),318(a,1))]. 528 (c1 v c3) ^ (c2 v c3) = c2 v c3. [para(496(a,1),165(a,1,2)),rewrite([23(7)])]. 529 c2 ^ (c1 v c3) = c2. [para(496(a,1),192(a,1,2))]. 543 c1 ^ c3 = c3 | c2 ^ c3 = c2. [para(323(a,1),529(a,1,2)),rewrite([23(3)])]. 571 c2 v c3 = c3 | c3 ^ c4 = c4. [para(344(a,1),165(a,1,2)),rewrite([23(8)])]. 767 c1 ^ c3 = c3 | c2 v c3 = c3. [para(543(b,1),26(a,1,1)),rewrite([491(10)])]. 1145 c1 ^ (c2 v c3) = c1 ^ c2. [para(25(a,1),163(a,1,2)),flip(a)]. 1146 c3 ^ (c1 v c2) = c2 ^ c3. [para(27(a,1),163(a,1,2)),rewrite([366(8)]),flip(a)]. 1175 c2 ^ (c3 v c4) = c2 ^ c3. [back_rewrite(366),rewrite([1146(10)])]. 1328 c4 v (c2 ^ c3) = c3 v c4. [para(26(a,1),223(a,1,2)),rewrite([22(3),22(8)]),flip(a)]. 1340 c2 v (c3 v c4) = c2 v c4. [para(491(a,1),223(a,1,2)),rewrite([43(5),22(4)])]. 1466 c3 ^ (c2 v c4) = c3. [para(1340(a,1),192(a,1,2))]. 1479 c2 v c4 = c2 | c3 ^ c4 = c3. [para(204(a,1),1466(a,1,2))]. 2123 c2 ^ (c3 ^ c4) = c2 ^ c4. [para(1175(a,1),240(a,1,2)),rewrite([44(5),23(4)])]. 2162 c2 v c3 = c2 | c2 ^ c4 = c2. [back_rewrite(518),rewrite([2123(10)])]. 2254 c2 ^ c4 = c2 | c1 ^ c3 = c3. [para(2162(a,1),767(b,1)),flip(c),unit_del(c,28)]. 2335 c1 ^ c3 = c3 | c2 v c4 = c4. [para(2254(a,1),152(a,1,2)),rewrite([22(8)])]. 2428 c1 ^ c3 = c3 | c3 ^ c4 = c3. [para(2335(b,1),1466(a,1,2))]. 2454 (c1 v c2) ^ (c1 v c3) = c1 v c2. [para(496(a,1),162(a,1,2))]. 2467 (c2 v c3) ^ (c2 v c4) = c2 v c3. [para(1340(a,1),162(a,1,2))]. 3112 c1 v c3 = c1 | c2 v c3 = c3. [para(204(a,1),528(a,1,1)),rewrite([165(10)]),flip(b)]. 3113 c1 v c3 = c3 | c2 v c3 = c1 ^ c2. [para(204(b,1),528(a,1,1)),rewrite([1145(10)]),flip(b)]. 4691 c3 ^ c4 = c3 | c2 v c3 = c2. [para(1479(a,1),2467(a,1,2)),rewrite([23(10),39(10)]),flip(b)]. 4727 c3 ^ c4 = c3 | c1 v c3 = c1. [para(4691(b,1),3112(b,1)),flip(c),unit_del(c,28)]. 7546 c3 ^ c4 = c3 | c3 ^ x = c3 | x ^ c1 = x. [para(4727(b,1),411(b,1,2))]. 7609 c3 ^ c4 = c3 | c1 ^ c4 = c4. [factor(7546,a,b),rewrite([23(8)])]. 7708 c1 ^ c4 = c4 | (c1 v c3) ^ (c3 v c4) != c3. [para(7609(a,1),29(a,1,2)),rewrite([22(10),152(10)]),xx(b)]. 21377 c1 ^ c3 = c3 | c3 ^ c4 = c4. [para(323(a,1),346(b,1,1)),rewrite([23(3),39(15)]),xx(c)]. 21443 c1 ^ c3 = c3 | c4 = c3. [para(21377(b,1),2428(b,1)),merge(b)]. 21459 c4 = c3 | c1 v c3 = c1. [para(21443(a,1),38(a,1,2))]. 21501 c4 = c3 | c1 v c2 = c1. [para(21459(b,1),2454(a,1,2)),rewrite([23(8),39(8)]),flip(b)]. 21616 c4 = c3 | c2 ^ c3 = c1 ^ c3. [para(21501(b,1),1146(a,1,2)),rewrite([23(6)]),flip(b)]. 23043 c4 = c3 | c4 v (c1 ^ c3) = c3 v c4. [para(21616(b,1),1328(a,1,2))]. 24500 c1 v c3 = c3 | c2 v c3 = c2. [para(3113(b,1),193(a,1,2)),rewrite([152(10)]),flip(b)]. 24535 c1 v c3 = c3 | c3 ^ c4 = c4. [para(24500(b,1),571(a,1)),flip(b),unit_del(b,28)]. 24579 c3 ^ c4 = c4. [para(24535(a,1),346(b,1,1)),rewrite([39(15)]),xx(c),merge(b)]. 24790 c4 v (c1 ^ c3) != c3 | (c1 v c3) ^ (c3 v c4) != c3. [back_rewrite(29),rewrite([24579(6),22(5)])]. 24791 c3 v c4 = c3. [back_rewrite(26),rewrite([24579(6),22(5),1328(5)])]. 25258 c4 v (c1 ^ c3) != c3. [back_rewrite(24790),rewrite([24791(13),23(12),165(12)]),xx(b)]. 25281 c4 = c3. [back_rewrite(23043),rewrite([24791(11)]),unit_del(b,25258)]. 25299 c1 ^ c3 = c3. [back_rewrite(7708),rewrite([25281(2),25281(4),25281(10),173(11),23(10),165(10)]),xx(b)]. 25306 c3 = c1. [back_rewrite(456),rewrite([25299(3),25281(8),173(9),23(8),165(8)]),xx(b)]. 25307 $F. [back_rewrite(25258),rewrite([25281(1),25306(1),25306(3),174(4),173(3),25306(2)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=582. Generated=146576. Kept=25293. proofs=1. Usable=377. Sos=15218. Demods=1474. Limbo=26, Disabled=9688. Hints=0. Weight_deleted=3. Literals_deleted=0. Forward_subsumed=101949. Back_subsumed=3564. Sos_limit_deleted=19330. Sos_displaced=1911. Sos_removed=0. New_demodulators=1878 (6 lex), Back_demodulated=4193. Back_unit_deleted=4. Demod_attempts=2440891. Demod_rewrites=189636. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=5541286. Nonunit_bsub_feature_tests=3607992. Megabytes=20.90. User_CPU=15.30, System_CPU=0.04, Wall_clock=15. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 15261 exit (max_proofs) Fri Jun 15 14:08:29 2007