============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11455 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:39 2006 The command was "/home/mccune/bin/prover9 -f head.in t4_12.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file head.in clear(auto_inference). % clear(auto_inference) -> clear(predicate_elim). % clear(auto_inference) -> assign(eq_defs, pass). set(predicate_elim). set(paramodulation). % set(paramodulation) -> set(back_demod). set(hyper_resolution). formulas(sos). 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(sos). (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)). (all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)). (all xa all xx all xb (C(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa ^ xb) v xx = xx)). (all xa all xx all xb (CS(xa,xx,xb) <-> (xa v xx) ^ (xx v xb) = xx & (xa v xb) ^ xx = xx)). (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)). (all x all y (x <= y <-> x ^ y = x)). end_of_list. % Reading from file t4_12.in formulas(sos). x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). x ^ (y v (x ^ z)) = (x ^ y) v (x ^ z) # label("modularity_2"). B(ca,cy,cx). B(ca,cx,cb). -B(ca,cy,cb). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)). [assumption]. 2 (all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)). [assumption]. 3 (all xa all xx all xb (C(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa ^ xb) v xx = xx)). [assumption]. 4 (all xa all xx all xb (CS(xa,xx,xb) <-> (xa v xx) ^ (xx v xb) = xx & (xa v xb) ^ xx = xx)). [assumption]. 5 (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)). [assumption]. 6 (all x all y (x <= y <-> x ^ y = x)). [assumption]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x ^ y = y ^ x # label("commutativity_meet"). [assumption]. x v y = y v x # label("commutativity_join"). [assumption]. (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. (x v y) ^ x = x # label("absorption_1"). [assumption]. (x ^ y) v x = x # label("absorption_2"). [assumption]. -A(x,y,z) | x <= y | z <= y. [clausify(1)]. -A(x,y,z) | x <= y | y <= x. [clausify(1)]. -A(x,y,z) | y <= z | z <= y. [clausify(1)]. -A(x,y,z) | y <= z | y <= x. [clausify(1)]. A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. -D(x,y,z) | x ^ z <= y. [clausify(5)]. -D(x,y,z) | y <= x v z. [clausify(5)]. D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. -(x <= y) | x ^ y = x. [clausify(6)]. x <= y | x ^ y != x. [clausify(6)]. x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). [assumption]. x ^ (y v (x ^ z)) = (x ^ y) v (x ^ z) # label("modularity_2"). [assumption]. B(ca,cy,cx). [assumption]. B(ca,cx,cb). [assumption]. -B(ca,cy,cb). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating A/3 7 A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. 8 -A(x,y,z) | x <= y | z <= y. [clausify(1)]. 9 -A(x,y,z) | x <= y | y <= x. [clausify(1)]. 10 -A(x,y,z) | y <= z | z <= y. [clausify(1)]. 11 -A(x,y,z) | y <= z | y <= x. [clausify(1)]. 12 A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. Eliminating C/3 13 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 14 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 15 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. Eliminating CS/3 16 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 17 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 18 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. Eliminating D/3 19 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. 20 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 21 -D(x,y,z) | y <= x v z. [clausify(5)]. Eliminating <=/2 22 x <= y | x ^ y != x. [clausify(6)]. 23 -(x <= y) | x ^ y = x. [clausify(6)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ B, =, D, CS, C, A, <= ]). Function symbol precedence: lex([ ca, cx, cb, cy, ^, v ]). After inverse_order: (no changes). Auto_process settings: (no changes). % Operation ^ is commutative; C redundancy checks enabled. % Operation v 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). 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 25 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 32 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 35 x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). [assumption]. 37 (x ^ y) v (x ^ z) = x ^ (y v (x ^ z)). [copy(36),flip(a)]. 38 B(ca,cy,cx). [assumption]. 39 B(ca,cx,cb). [assumption]. 40 -B(ca,cy,cb). [assumption]. end_of_list. formulas(demodulators). 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 25 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 35 x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). [assumption]. 37 (x ^ y) v (x ^ z) = x ^ (y v (x ^ z)). [copy(36),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. given #2 (I,wt=7): 25 x v y = y v x # label("commutativity_join"). [assumption]. given #3 (I,wt=11): 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 41 x ^ (y ^ z) = z ^ (x ^ y). [para(26(a,1),24(a,1))]. given #4 (I,wt=11): 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 43 x v (y v z) = z v (x v y). [para(27(a,1),25(a,1))]. given #5 (I,wt=7): 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. given #6 (I,wt=7): 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. given #7 (I,wt=13): 32 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. given #8 (I,wt=13): 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. given #9 (I,wt=22): 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. given #10 (I,wt=15): 35 x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). [assumption]. given #11 (I,wt=15): 37 (x ^ y) v (x ^ z) = x ^ (y v (x ^ z)). [copy(36),flip(a)]. given #12 (I,wt=4): 38 B(ca,cy,cx). [assumption]. given #13 (I,wt=4): 39 B(ca,cx,cb). [assumption]. given #14 (I,wt=4): 40 -B(ca,cy,cb). [assumption]. given #15 (T,wt=4): 84 B(x,x,y). [para(37(a,1),34(b,1)),rewrite(31(3),53(2),54(3),29(4)),xx(b),xx(c)]. given #16 (A,wt=11): 42 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. given #17 (F,wt=5): 53 x ^ x = x. [para(31(a,1),29(a,1,2))]. given #18 (F,wt=5): 54 x v x = x. [para(29(a,1),31(a,1,2))]. given #19 (T,wt=7): 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. given #20 (T,wt=7): 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. given #21 (A,wt=11): 44 x v (y v z) = y v (x v z). [para(25(a,1),27(a,1,1)),rewrite(27(2))]. given #22 (F,wt=9): 83 x ^ (x ^ y) = x ^ y. [para(37(a,1),29(a,1,2)),rewrite(42(5),26(4),29(3))]. given #23 (F,wt=9): 99 (ca v cy) ^ (cx v cy) = cy. [hyper(33,a,38,a),rewrite(25(6))]. given #24 (T,wt=9): 100 (ca v cx) ^ (cx v cb) = cx. [hyper(33,a,39,a)]. given #25 (T,wt=9): 102 x v (y ^ (x ^ z)) = x. [para(42(a,1),31(a,1,2))]. given #26 (A,wt=11): 46 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. given #27 (F,wt=9): 111 x ^ (y ^ x) = y ^ x. [para(53(a,1),26(a,2,2)),rewrite(24(2))]. given #28 (F,wt=9): 112 x v (x v y) = x v y. [para(53(a,1),35(a,1,2)),rewrite(24(6),45(6))]. given #29 (T,wt=9): 116 x v (y v x) = y v x. [para(54(a,1),27(a,2,2)),rewrite(25(2))]. given #30 (T,wt=9): 119 x ^ (y v (z v x)) = x. [para(27(a,1),45(a,1,2))]. given #31 (A,wt=13): 47 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(29(a,1),26(a,1)),flip(a)]. given #32 (F,wt=9): 121 x v (y ^ (z ^ x)) = x. [para(26(a,1),49(a,1,2))]. given #33 (F,wt=9): 124 x ^ (y v (x v z)) = x. [para(44(a,1),29(a,1,2))]. given #34 (T,wt=9): 152 ca ^ (cx v cy) = ca ^ cy. [para(99(a,1),46(a,1,2)),flip(a)]. given #35 (T,wt=9): 153 ca ^ (cx v cb) = ca ^ cx. [para(100(a,1),46(a,1,2)),flip(a)]. given #36 (A,wt=13): 48 (x v y) ^ (x v (y v z)) = x v y. [para(27(a,1),29(a,1,2))]. given #37 (F,wt=11): 51 x v ((x ^ y) v z) = x v z. [para(31(a,1),27(a,1,1)),flip(a)]. given #38 (F,wt=11): 101 x ^ (y ^ (x v z)) = y ^ x. [para(29(a,1),42(a,1,2)),flip(a)]. given #39 (T,wt=9): 217 cx ^ (ca v cy) = cx ^ cy. [para(99(a,1),101(a,1,2)),rewrite(24(8)),flip(a)]. given #40 (T,wt=9): 218 ca ^ (cx ^ cy) = ca ^ cx. [para(152(a,1),101(a,1,2)),rewrite(42(5))]. given #41 (A,wt=13): 52 x v (y v ((x v y) ^ z)) = x v y. [para(31(a,1),27(a,1)),flip(a)]. given #42 (F,wt=7): 228 cy v (ca ^ cx) = cy. [para(218(a,1),121(a,1,2))]. given #43 (F,wt=11): 117 x ^ ((y v x) ^ z) = x ^ z. [para(45(a,1),26(a,1,1)),flip(a)]. given #44 (T,wt=11): 120 x ^ (y ^ (z v x)) = y ^ x. [para(45(a,1),42(a,1,2)),flip(a)]. given #45 (T,wt=9): 256 cb ^ (ca v cx) = cx ^ cb. [para(100(a,1),120(a,1,2)),rewrite(24(3),24(8)),flip(a)]. given #46 (A,wt=22): 55 B(x,y,z) | y ^ (x v (y ^ z)) != y | (x v y) ^ (y v z) != y. [para(24(a,1),34(b,1,1)),rewrite(37(4))]. given #47 (F,wt=4): 275 B(x,y,y). [para(53(a,1),55(b,1,2,2)),rewrite(45(3),54(4),24(4),45(4)),xx(b),xx(c)]. given #48 (F,wt=9): 257 ca ^ (cx ^ cb) = ca ^ cb. [para(153(a,1),120(a,1,2)),rewrite(42(5),24(4))]. given #49 (T,wt=7): 319 cx v (ca ^ cb) = cx. [para(257(a,1),102(a,1,2))]. given #50 (T,wt=11): 122 x v ((y ^ x) v z) = x v z. [para(49(a,1),27(a,1,1)),flip(a)]. given #51 (A,wt=22): 56 B(x,y,z) | (x ^ y) v (z ^ y) != y | (x v y) ^ (y v z) != y. [para(24(a,1),34(b,1,2))]. given #52 (F,wt=11): 125 x v (y v (x ^ z)) = y v x. [para(31(a,1),44(a,1,2)),flip(a)]. given #53 (F,wt=11): 130 x v (y v (z ^ x)) = y v x. [para(49(a,1),44(a,1,2)),flip(a)]. given #54 (T,wt=11): 142 x v (y ^ (z ^ (x ^ u))) = x. [para(26(a,1),102(a,1,2))]. given #55 (T,wt=9): 454 cx v (x ^ (ca ^ cb)) = cx. [para(257(a,1),142(a,1,2,2))]. given #56 (A,wt=28): 61 B(x ^ y,z,u) | (x ^ (y ^ z)) v (z ^ u) != z | ((x ^ y) v z) ^ (z v u) != z. [para(26(a,1),34(b,1,1))]. given #57 (F,wt=9): 456 cx v (ca ^ (cb ^ x)) = cx. [para(24(a,1),454(a,1,2)),rewrite(26(5))]. given #58 (F,wt=9): 460 cx v (ca ^ (x ^ cb)) = cx. [para(42(a,1),454(a,1,2))]. given #59 (T,wt=11): 156 (x v y) ^ (z ^ x) = z ^ x. [para(111(a,1),46(a,2)),rewrite(155(4))]. given #60 (T,wt=11): 164 x ^ (y v (z v (u v x))) = x. [para(27(a,1),119(a,1,2,2))]. given #61 (A,wt=15): 69 x v ((x v y) ^ z) = (x v z) ^ (x v y). [para(24(a,1),35(a,1,2))]. given #62 (F,wt=11): 169 x ^ (y v (z v (x v u))) = x. [para(119(a,1),46(a,1,2)),rewrite(29(2)),flip(a)]. given #63 (F,wt=11): 177 x v (y ^ (z ^ (u ^ x))) = x. [para(26(a,1),121(a,1,2,2))]. given #64 (T,wt=9): 674 cy v (x ^ (ca ^ cx)) = cy. [para(218(a,1),177(a,1,2,2))]. given #65 (T,wt=9): 688 cy v (ca ^ (cx ^ x)) = cy. [para(24(a,1),674(a,1,2)),rewrite(26(5))]. given #66 (A,wt=15): 70 x v (y ^ (z v x)) = (x v y) ^ (x v z). [para(25(a,1),35(a,1,2,2))]. given #67 (F,wt=7): 711 cy v (ca ^ cb) = cy. [para(257(a,1),688(a,1,2))]. given #68 (F,wt=9): 692 cy v (ca ^ (x ^ cx)) = cy. [para(42(a,1),674(a,1,2))]. given #69 (T,wt=9): 797 ca ^ (cb ^ cy) = ca ^ cb. [para(711(a,1),45(a,1,2)),rewrite(24(5),42(5),24(4))]. given #70 (T,wt=9): 834 cy v (x ^ (ca ^ cb)) = cy. [para(797(a,1),177(a,1,2,2))]. given #71 (A,wt=19): 71 x v (y ^ (z ^ (x v u))) = (x v (y ^ z)) ^ (x v u). [para(26(a,1),35(a,1,2))]. given #72 (F,wt=9): 835 cy v (ca ^ (cb ^ x)) = cy. [para(24(a,1),834(a,1,2)),rewrite(26(5))]. given #73 (F,wt=9): 839 cy v (ca ^ (x ^ cb)) = cy. [para(42(a,1),834(a,1,2))]. given #74 (T,wt=11): 204 (x v y) ^ (y v x) = x v y. [para(116(a,1),48(a,1,2))]. given #75 (T,wt=8): 909 B(x,y v z,z v y). [para(204(a,1),55(b,1,2,2)),rewrite(45(7),44(11),25(10),112(10),116(10),24(10),45(10)),xx(b),xx(c)]. given #76 (A,wt=19): 72 ((x v y) ^ (x v z)) v u = x v ((y ^ (x v z)) v u). [para(35(a,1),27(a,1,1))]. given #77 (F,wt=11): 212 (x ^ y) v (z v x) = z v x. [para(116(a,1),51(a,2)),rewrite(160(4))]. given #78 (F,wt=11): 237 cy v ((ca ^ cx) v x) = cy v x. [para(228(a,1),27(a,1,1)),flip(a)]. given #79 (T,wt=11): 238 (ca ^ cx) v (x v cy) = x v cy. [para(228(a,1),27(a,2,2)),rewrite(25(6))]. given #80 (T,wt=11): 239 cy v (x v (ca ^ cx)) = x v cy. [para(228(a,1),44(a,1,2)),flip(a)]. given #81 (A,wt=15): 78 (x ^ y) v (y ^ z) = y ^ (x v (y ^ z)). [para(24(a,1),37(a,1,1))]. given #82 (F,wt=11): 240 ca ^ (cx ^ (x v cy)) = ca ^ cx. [para(228(a,1),119(a,1,2,2)),rewrite(26(6))]. given #83 (F,wt=11): 246 (x v y) ^ (z ^ y) = z ^ y. [para(111(a,1),117(a,2)),rewrite(155(4))]. given #84 (T,wt=11): 276 B(x ^ y,x,y) | x ^ y != x. [para(54(a,1),55(b,1,2)),rewrite(83(4),25(6),31(6),29(6)),xx(c)]. given #85 (T,wt=11): 278 B(x,y,x v y) | x v y != y. [para(45(a,1),55(c,1)),rewrite(45(4),45(4)),xx(b)]. given #86 (A,wt=15): 79 (x ^ y) v (z ^ x) = x ^ (y v (x ^ z)). [para(24(a,1),37(a,1,2))]. given #87 (F,wt=11): 322 cx v ((ca ^ cb) v x) = cx v x. [para(319(a,1),27(a,1,1)),flip(a)]. given #88 (F,wt=11): 323 (ca ^ cb) v (x v cx) = x v cx. [para(319(a,1),27(a,2,2)),rewrite(25(6))]. given #89 (T,wt=11): 324 cx v (x v (ca ^ cb)) = x v cx. [para(319(a,1),44(a,1,2)),flip(a)]. given #90 (T,wt=11): 325 ca ^ (cb ^ (x v cx)) = ca ^ cb. [para(319(a,1),119(a,1,2,2)),rewrite(26(6))]. given #91 (A,wt=15): 80 x ^ (y v (x ^ z)) = x ^ (z v (x ^ y)). [para(37(a,1),25(a,1)),rewrite(37(6))]. given #92 (F,wt=11): 338 (x ^ y) v (z v y) = z v y. [para(116(a,1),122(a,2)),rewrite(160(4))]. given #93 (F,wt=11): 361 B(x,y,x ^ y) | x ^ y != y. [para(31(a,1),56(b,1)),rewrite(49(7),24(6),45(6)),xx(c)]. given #94 (T,wt=11): 457 cx v (x ^ (y ^ (ca ^ cb))) = cx. [para(26(a,1),454(a,1,2))]. given #95 (T,wt=11): 554 cx v (ca ^ (x ^ (cb ^ y))) = cx. [para(42(a,1),456(a,1,2,2))]. given #96 (A,wt=19): 82 (x ^ (y v (x ^ z))) v u = (x ^ y) v ((x ^ z) v u). [para(37(a,1),27(a,1,1))]. given #97 (F,wt=11): 563 cx v (ca ^ (x ^ (y ^ cb))) = cx. [para(26(a,1),460(a,1,2,2))]. given #98 (F,wt=11): 689 cy v (x ^ (y ^ (ca ^ cx))) = cy. [para(26(a,1),674(a,1,2))]. given #99 (T,wt=11): 704 cy v (ca ^ (x ^ (cx ^ y))) = cy. [para(42(a,1),688(a,1,2,2))]. given #100 (T,wt=11): 794 cy v ((ca ^ cb) v x) = cy v x. [para(711(a,1),27(a,1,1)),flip(a)]. given #101 (A,wt=15): 90 B(x,y,y ^ z) | y ^ (x v (y ^ z)) != y. [back_rewrite(68),rewrite(83(5),78(5))]. given #102 (F,wt=11): 795 (ca ^ cb) v (x v cy) = x v cy. [para(711(a,1),27(a,2,2)),rewrite(25(6))]. given #103 (F,wt=11): 796 ca ^ (cb v (ca ^ cy)) = ca ^ cy. [para(711(a,1),37(a,2,2)),rewrite(25(7),37(7))]. given #104 (T,wt=11): 798 cy v (x v (ca ^ cb)) = x v cy. [para(711(a,1),44(a,1,2)),flip(a)]. given #105 (T,wt=11): 799 ca ^ (cb ^ (x v cy)) = ca ^ cb. [para(711(a,1),119(a,1,2,2)),rewrite(26(6))]. given #106 (A,wt=36): 91 B(x,y v z,u) | (y v z) ^ (x v ((y v z) ^ u)) != y v z | (x v (y v z)) ^ (y v (z v u)) != y v z. [back_rewrite(64),rewrite(78(7))]. given #107 (F,wt=11): 808 cy v (ca ^ (x ^ (y ^ cx))) = cy. [para(26(a,1),692(a,1,2,2))]. given #108 (F,wt=11): 824 cb ^ (ca v (cb ^ cy)) = cb ^ cy. [para(797(a,1),49(a,1,2)),rewrite(25(7),78(7))]. given #109 (T,wt=11): 836 cy v (x ^ (y ^ (ca ^ cb))) = cy. [para(26(a,1),834(a,1,2))]. given #110 (T,wt=11): 861 (cx v cb) ^ (cx v (x ^ ca)) = cx. [para(153(a,1),71(a,1,2,2)),rewrite(121(6),24(9)),flip(a)]. given #111 (A,wt=28): 92 B(x v y,z,u) | z ^ (x v (y v (z ^ u))) != z | (x v (y v z)) ^ (z v u) != z. [back_rewrite(63),rewrite(78(6),27(5))]. given #112 (F,wt=11): 880 cy v (ca ^ (x ^ (cb ^ y))) = cy. [para(42(a,1),835(a,1,2,2))]. given #113 (F,wt=11): 890 cy v (ca ^ (x ^ (y ^ cb))) = cy. [para(26(a,1),839(a,1,2,2))]. given #114 (T,wt=11): 979 cx v (x ^ (ca ^ (cb ^ y))) = cx. [para(454(a,1),212(a,1,2)),rewrite(26(5),26(4),25(7),454(13))]. given #115 (T,wt=11): 984 cy v (x ^ (ca ^ (cx ^ y))) = cy. [para(674(a,1),212(a,1,2)),rewrite(26(5),26(4),25(7),674(13))]. given #116 (A,wt=22): 93 B(x,y,z) | y ^ (x v (y ^ z)) != y | (x v y) ^ (z v y) != y. [back_rewrite(60),rewrite(78(4))]. given #117 (F,wt=11): 985 cy v (x ^ (ca ^ (cb ^ y))) = cy. [para(834(a,1),212(a,1,2)),rewrite(26(5),26(4),25(7),834(13))]. given #118 (F,wt=11): 1001 ca ^ (cx ^ (cy v x)) = ca ^ cx. [para(237(a,1),124(a,1,2)),rewrite(26(6))]. given #119 (T,wt=11): 1178 B(x ^ y,x,y) | y ^ x != x. [para(24(a,1),276(b,1))]. given #120 (T,wt=11): 1199 B(x,y,x v y) | y v x != y. [para(25(a,1),278(b,1))]. given #121 (A,wt=22): 94 B(x,y,z) | y ^ (x v (y ^ z)) != y | (y v x) ^ (y v z) != y. [back_rewrite(59),rewrite(78(4))]. given #122 (F,wt=11): 1201 B(x,x ^ y,x) | x ^ y != x. [para(31(a,1),278(b,1)),rewrite(31(3)),flip(b)]. given #123 (F,wt=11): 1204 B(x,y ^ x,x) | y ^ x != x. [para(49(a,1),278(b,1)),rewrite(49(3)),flip(b)]. given #124 (T,wt=11): 1209 B(cy,ca ^ cx,cy) | ca ^ cx != cy. [para(228(a,1),278(b,1)),rewrite(228(9)),flip(b)]. given #125 (T,wt=11): 1210 B(cx,ca ^ cb,cx) | ca ^ cb != cx. [para(319(a,1),278(b,1)),rewrite(319(9)),flip(b)]. given #126 (A,wt=22): 95 B(x,y,z) | y ^ (x v (y ^ z)) != y | (y v z) ^ (x v y) != y. [back_rewrite(57),rewrite(78(4))]. given #127 (F,wt=11): 1223 B(cy,ca ^ cb,cy) | ca ^ cb != cy. [para(711(a,1),278(b,1)),rewrite(711(9)),flip(b)]. given #128 (F,wt=11): 1277 ca ^ (cb ^ (cx v x)) = ca ^ cb. [para(322(a,1),124(a,1,2)),rewrite(26(6))]. given #129 (T,wt=11): 1379 cx v (x ^ (ca ^ (y ^ cb))) = cx. [para(460(a,1),338(a,1,2)),rewrite(25(7),460(13))]. given #130 (T,wt=11): 1383 cy v (x ^ (ca ^ (y ^ cx))) = cy. [para(692(a,1),338(a,1,2)),rewrite(25(7),692(13))]. given #131 (A,wt=13): 96 -B(x,y,z) | y ^ (x v (y ^ z)) = y. [back_rewrite(32),rewrite(78(4))]. given #132 (F,wt=7): 2610 cx ^ (ca v cb) = cx. [hyper(96,a,39,a),rewrite(262(6),117(9))]. given #133 (F,wt=7): 2611 cy ^ (ca v cx) = cy. [hyper(96,a,38,a),rewrite(24(5),220(6),120(9),24(5))]. given #134 (T,wt=9): 2617 ca v (cx v cb) = ca v cb. [para(2610(a,1),49(a,1,2)),rewrite(25(5),44(5))]. given #135 (T,wt=9): 2622 cx ^ (ca v (cb v x)) = cx. [para(2610(a,1),156(a,1,2)),rewrite(27(4),24(6),2610(11))]. given #136 (A,wt=22): 97 B(x,y,z) | y ^ (z v (y ^ x)) != y | (x v y) ^ (y v z) != y. [back_rewrite(58),rewrite(79(4))]. given #137 (F,wt=8): 2829 B(x v y,y v x,z). [para(204(a,1),97(b,1,2,2)),rewrite(45(7),44(9),25(8),112(8),116(8),27(9),194(10)),xx(b),xx(c)]. given #138 (F,wt=9): 2627 cx ^ (x v (ca v cb)) = cx. [para(2610(a,1),246(a,1,2)),rewrite(24(6),2610(11))]. given #139 (T,wt=9): 2640 ca v (cx ^ cb) = ca v cx. [back_rewrite(262),rewrite(2614(12))]. given #140 (T,wt=4): 2940 B(cb,cx,ca). [para(2640(a,1),97(b,1,2)),rewrite(45(9),25(10),25(13),24(14),100(14)),xx(b),xx(c)]. given #141 (A,wt=19): 103 (x ^ (y ^ z)) v (y ^ u) = y ^ ((x ^ z) v (y ^ u)). [para(42(a,1),37(a,1,1))]. given #142 (F,wt=6): 2931 B(ca,cx,cx ^ cb). [para(2640(a,1),90(b,1,2)),rewrite(45(11)),xx(b)]. given #143 (F,wt=9): 2659 cb v (ca ^ cx) = cx v cb. [back_rewrite(728),rewrite(2624(12))]. given #144 (T,wt=9): 2664 ca v (cx v cy) = ca v cx. [para(2611(a,1),49(a,1,2)),rewrite(25(5),44(5),25(4))]. given #145 (T,wt=9): 2669 cy ^ (ca v (cx v x)) = cy. [para(2611(a,1),156(a,1,2)),rewrite(27(4),24(6),2611(11))]. given #146 (A,wt=19): 104 (x ^ y) v (z ^ (x ^ u)) = x ^ (y v (x ^ (z ^ u))). [para(42(a,1),37(a,1,2))]. given #147 (F,wt=7): 3106 cy ^ (ca v cb) = cy. [para(2617(a,1),2669(a,1,2))]. given #148 (F,wt=9): 2674 cy ^ (x v (ca v cx)) = cy. [para(2611(a,1),246(a,1,2)),rewrite(24(6),2611(11))]. given #149 (T,wt=9): 2687 ca v (cx ^ cy) = ca v cy. [back_rewrite(220),rewrite(2661(12))]. given #150 (T,wt=9): 2703 cx v (ca ^ cy) = cx v cy. [back_rewrite(188),rewrite(2671(12))]. given #151 (A,wt=30): 105 B(x,y,z ^ (y v u)) | y ^ (x v (z ^ y)) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [back_rewrite(89),rewrite(101(6))]. given #152 (F,wt=8): 3436 B(cb,cx,ca ^ (cx v x)). [para(2659(a,1),105(b,1,2)),rewrite(29(12),25(13),25(16),42(20),137(20),29(14)),xx(b),xx(c)]. given #153 (F,wt=6): 3454 B(cb,cx,ca ^ cx). [para(31(a,1),3436(a,3,2))]. given #154 (T,wt=6): 3457 B(cb,cx,ca ^ cy). [para(152(a,1),3436(a,3))]. given #155 (T,wt=8): 3447 B(ca,cy,cx ^ (cy v x)). [para(2687(a,1),105(b,1,2)),rewrite(45(12),25(16),133(20),29(14)),xx(b),xx(c)]. given #156 (A,wt=27): 109 x ^ (((x ^ y) v z) ^ (y v (x ^ u))) = x ^ ((y v (x ^ z)) ^ (y v (x ^ u))). [back_rewrite(87),rewrite(104(6),71(5)),flip(a)]. given #157 (F,wt=6): 3461 B(ca,cy,cx ^ cy). [para(31(a,1),3447(a,3,2))]. given #158 (F,wt=8): 3450 B(cx,cy,ca ^ (cy v x)). [para(2703(a,1),105(b,1,2)),rewrite(45(12),25(16),42(20),133(20),29(14)),xx(b),xx(c)]. given #159 (T,wt=4): 3569 B(cx,cy,ca). [para(45(a,1),3450(a,3))]. given #160 (T,wt=6): 3567 B(cx,cy,ca ^ cy). [para(31(a,1),3450(a,3,2))]. given #161 (A,wt=17): 113 B(x,x v y,z) | (x v z) ^ (x v y) != x v y. [back_rewrite(77),rewrite(112(9),48(11)),xx(c)]. given #162 (F,wt=6): 3572 B(x,x v y,y). [hyper(113,b,53,a)]. given #163 (F,wt=6): 3658 B(x,y v x,y). [para(25(a,1),3572(a,2))]. given #164 (T,wt=8): 3453 B(cb,cx,ca ^ (x v cx)). [para(25(a,1),3436(a,3,2))]. given #165 (T,wt=8): 3460 B(ca,cy,cx ^ (x v cy)). [para(25(a,1),3447(a,3,2))]. given #166 (A,wt=15): 114 B(x,y,y v z) | (x v y) ^ (y v z) != y. [back_rewrite(66),rewrite(112(5))]. given #167 (F,wt=6): 3719 B(ca,cx,cx v cb). [hyper(114,b,100,a)]. given #168 (F,wt=8): 3566 B(cx,cy,ca ^ (x v cy)). [para(25(a,1),3450(a,3,2))]. given #169 (T,wt=8): 3680 B(ca,ca v cb,cx v cb). [para(2617(a,1),3572(a,2))]. given #170 (T,wt=8): 3681 B(ca,ca v cx,cx ^ cb). [para(2640(a,1),3572(a,2))]. given #171 (A,wt=13): 118 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(45(a,1),26(a,1)),flip(a)]. given #172 (F,wt=8): 3683 B(cb,cx v cb,ca ^ cx). [para(2659(a,1),3572(a,2))]. given #173 (F,wt=8): 3684 B(ca,ca v cx,cx v cy). [para(2664(a,1),3572(a,2))]. given #174 (T,wt=8): 3686 B(ca,ca v cy,cx ^ cy). [para(2687(a,1),3572(a,2))]. given #175 (T,wt=8): 3687 B(cx,cx v cy,ca ^ cy). [para(2703(a,1),3572(a,2))]. given #176 (A,wt=19): 126 x v (y ^ (z v (x v u))) = (x v y) ^ (x v (z v u)). [para(44(a,1),35(a,1,2,2))]. given #177 (F,wt=8): 3709 B(cx v cb,ca v cb,ca). [para(2617(a,1),3658(a,2))]. given #178 (F,wt=8): 3710 B(cx ^ cb,ca v cx,ca). [para(2640(a,1),3658(a,2))]. given #179 (T,wt=8): 3712 B(ca ^ cx,cx v cb,cb). [para(2659(a,1),3658(a,2))]. given #180 (T,wt=8): 3713 B(cx v cy,ca v cx,ca). [para(2664(a,1),3658(a,2))]. given #181 (A,wt=19): 127 x v (y v (z ^ (x v u))) = y v ((x v z) ^ (x v u)). [para(35(a,1),44(a,1,2)),flip(a)]. given #182 (F,wt=8): 3715 B(cx ^ cy,ca v cy,ca). [para(2687(a,1),3658(a,2))]. given #183 (F,wt=8): 3716 B(ca ^ cy,cx v cy,cx). [para(2703(a,1),3658(a,2))]. given #184 (T,wt=9): 2725 cx ^ (ca v (x v cb)) = cx. [para(25(a,1),2622(a,1,2,2))]. given #185 (T,wt=9): 3046 cx v (cb v cy) = cb v cy. [para(2659(a,1),239(a,1,2)),rewrite(44(5),25(4))]. given #186 (A,wt=19): 128 (x ^ y) v (z v (x ^ u)) = z v (x ^ (y v (x ^ u))). [para(37(a,1),44(a,1,2)),flip(a)]. given #187 (F,wt=7): 4124 cx ^ (cb v cy) = cx. [para(3046(a,1),29(a,1,2))]. given #188 (F,wt=8): 4155 B(cb,cx,ca ^ (cb v cy)). [para(3046(a,1),3436(a,3,2))]. given #189 (T,wt=9): 3085 cy ^ (ca v (x v cx)) = cy. [para(25(a,1),2669(a,1,2,2))]. given #190 (T,wt=9): 3169 ca v (cb v cy) = ca v cb. [para(3106(a,1),49(a,1,2)),rewrite(25(5),44(5),25(4))]. given #191 (A,wt=13): 129 (x v y) ^ (x v (z v y)) = x v y. [para(44(a,1),45(a,1,2))]. given #192 (F,wt=8): 4443 B(ca,ca v cb,cb v cy). [para(3169(a,1),3572(a,2))]. given #193 (F,wt=8): 4444 B(cb v cy,ca v cb,ca). [para(3169(a,1),3658(a,2))]. given #194 (T,wt=9): 3174 cy ^ (ca v (cb v x)) = cy. [para(3106(a,1),156(a,1,2)),rewrite(27(4),24(6),3106(11))]. given #195 (T,wt=9): 3179 cy ^ (x v (ca v cb)) = cy. [para(3106(a,1),246(a,1,2)),rewrite(24(6),3106(11))]. given #196 (A,wt=13): 132 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(83(a,1),26(a,2,2)),rewrite(42(3),26(2))]. given #197 (F,wt=9): 3459 (cx v cb) ^ (cx v cy) = cx. [hyper(33,a,3457,a),rewrite(25(3),2703(8))]. given #198 (F,wt=9): 4128 cx ^ (x v (cb v cy)) = cx. [para(3046(a,1),124(a,1,2,2))]. given #199 (T,wt=9): 4386 cx ^ (cb v (cy v x)) = cx. [para(4124(a,1),156(a,1,2)),rewrite(27(4),24(6),4124(11))]. given #200 (T,wt=9): 4538 cy ^ (ca v (x v cb)) = cy. [para(25(a,1),3174(a,1,2,2))]. given #201 (A,wt=13): 133 (ca v cy) ^ ((cx v cy) ^ x) = cy ^ x. [para(99(a,1),26(a,1,1)),flip(a)]. given #202 (F,wt=9): 4590 cb ^ (cx v cy) = cx ^ cb. [para(3459(a,1),117(a,1,2)),rewrite(24(3)),flip(a)]. given #203 (F,wt=9): 4591 cy ^ (cx v cb) = cx ^ cy. [para(3459(a,1),120(a,1,2)),rewrite(24(3),24(8)),flip(a)]. given #204 (T,wt=4): 4738 B(cb,cx,cy). [back_rewrite(4599),rewrite(4723(10),29(9)),xx(b)]. given #205 (T,wt=9): 4609 cx ^ (cb v (x v cy)) = cx. [para(44(a,1),4128(a,1,2))]. given #206 (A,wt=13): 136 (ca v cy) ^ (x ^ (cx v cy)) = x ^ cy. [para(99(a,1),42(a,1,2)),flip(a)]. given #207 (F,wt=9): 4702 cx ^ (cb ^ cy) = cb ^ cy. [para(4590(a,1),120(a,1,2)),rewrite(42(5),24(4))]. given #208 (F,wt=7): 4781 cx v (cb ^ cy) = cx. [para(4702(a,1),31(a,1,2))]. given #209 (T,wt=9): 4704 cy v (cx ^ cb) = cx v cy. [para(4590(a,1),70(a,1,2)),rewrite(25(8),25(11),24(12),4388(12))]. given #210 (T,wt=4): 4834 B(cy,cx,cb). [para(4704(a,1),55(b,1,2)),rewrite(29(9),25(10),24(14),3459(14)),xx(b),xx(c)]. given #211 (A,wt=13): 137 (ca v cx) ^ ((cx v cb) ^ x) = cx ^ x. [para(100(a,1),26(a,1,1)),flip(a)]. given #212 (F,wt=6): 4841 B(cy,cx,cx ^ cb). [para(4704(a,1),90(b,1,2)),rewrite(29(11)),xx(b)]. given #213 (F,wt=8): 4860 B(cy,cx v cy,cx ^ cb). [para(4704(a,1),3572(a,2))]. given #214 (T,wt=8): 4861 B(cx ^ cb,cx v cy,cy). [para(4704(a,1),3658(a,2))]. given #215 (T,wt=8): 4894 B(ca,cx,cb ^ (cx v x)). [para(137(a,1),105(c,1)),rewrite(24(12),2640(13),45(12),29(14)),xx(b),xx(c)]. given #216 (A,wt=13): 140 (ca v cx) ^ (x ^ (cx v cb)) = x ^ cx. [para(100(a,1),42(a,1,2)),flip(a)]. given #217 (F,wt=8): 4897 B(ca,cx,cb ^ (x v cx)). [para(25(a,1),4894(a,3,2))]. given #218 (F,wt=9): 4723 cb v (cx ^ cy) = cx v cb. [para(4591(a,1),70(a,1,2)),rewrite(25(11),24(12),4130(12))]. given #219 (T,wt=6): 4927 B(cb,cx,cx ^ cy). [para(4723(a,1),90(b,1,2)),rewrite(29(11)),xx(b)]. given #220 (T,wt=8): 4944 B(cb,cx v cb,cx ^ cy). [para(4723(a,1),3572(a,2))]. given #221 (A,wt=13): 143 x v ((y ^ (x ^ z)) v u) = x v u. [para(102(a,1),27(a,1,1)),flip(a)]. given #222 (F,wt=8): 4945 B(cx ^ cy,cx v cb,cb). [para(4723(a,1),3658(a,2))]. given #223 (F,wt=9): 4785 cx v (x ^ (cb ^ cy)) = cx. [para(4702(a,1),102(a,1,2,2))]. given #224 (T,wt=9): 4811 cx v (cb ^ (cy ^ x)) = cx. [para(4781(a,1),212(a,1,2)),rewrite(26(4),25(6),4781(11))]. given #225 (T,wt=9): 5001 cx v (cb ^ (x ^ cy)) = cx. [para(42(a,1),4785(a,1,2))]. given #226 (A,wt=15): 144 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(102(a,1),27(a,1)),flip(a)]. given #227 (F,wt=10): 3456 B(cb,cx,ca ^ (x v (cx v y))). [para(44(a,1),3436(a,3,2))]. given #228 (F,wt=10): 3458 B(cb,cx,ca ^ (x v (ca ^ cx))). [para(80(a,1),3436(a,3))]. given #229 (T,wt=10): 3463 B(ca,cy,cx ^ (x v (cy v y))). [para(44(a,1),3447(a,3,2))]. given #230 (T,wt=10): 3464 B(ca,cy,cx ^ (x v (cx ^ cy))). [para(80(a,1),3447(a,3))]. given #231 (A,wt=13): 145 x v (y v (z ^ (x ^ u))) = y v x. [para(102(a,1),44(a,1,2)),flip(a)]. given #232 (F,wt=10): 3570 B(cx,cy,ca ^ (x v (cy v y))). [para(44(a,1),3450(a,3,2))]. given #233 (F,wt=10): 3571 B(cx,cy,ca ^ (x v (ca ^ cy))). [para(80(a,1),3450(a,3))]. given #234 (T,wt=10): 3659 B(x v y,x v (y v z),z). [para(27(a,1),3572(a,2))]. given #235 (T,wt=8): 5267 B(ca v cx,ca v cb,cb). [para(2617(a,1),3659(a,2))]. given #236 (A,wt=17): 146 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(46(a,1),26(a,1)),rewrite(26(2)),flip(a)]. given #237 (F,wt=8): 5284 B(cx v cb,cb v cy,cy). [para(3046(a,1),3659(a,2))]. given #238 (F,wt=10): 3662 B(x,y v (x v z),y v z). [para(44(a,1),3572(a,2))]. given #239 (T,wt=8): 5404 B(cx,ca v cx,ca v cy). [para(2664(a,1),3662(a,2))]. given #240 (T,wt=8): 5417 B(cb,cb v cy,cx v cy). [para(3046(a,1),3662(a,2))]. given #241 (A,wt=17): 147 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(27(a,1),46(a,1,2,1))]. given #242 (F,wt=8): 5423 B(cb,ca v cb,ca v cy). [para(3169(a,1),3662(a,2))]. given #243 (F,wt=10): 3663 B(x,x v y,(x ^ z) v y). [para(51(a,1),3572(a,2))]. given #244 (T,wt=10): 3664 B(x,x v y,(z ^ x) v y). [para(122(a,1),3572(a,2))]. given #245 (T,wt=10): 3665 B(x,y v x,y v (x ^ z)). [para(125(a,1),3572(a,2))]. given #246 (A,wt=15): 149 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(46(a,1),42(a,1,2)),flip(a)]. given #247 (F,wt=10): 3666 B(x,y v x,y v (z ^ x)). [para(130(a,1),3572(a,2))]. given #248 (F,wt=8): 5807 B(cb,ca v cb,ca v cx). [para(2640(a,1),3666(a,3))]. given #249 (T,wt=8): 5840 B(cy,cb v cy,cx v cb). [para(4723(a,1),3666(a,3))]. given #250 (T,wt=10): 3671 B(cy,cy v x,(ca ^ cx) v x). [para(237(a,1),3572(a,2))]. given #251 (A,wt=13): 151 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(44(a,1),46(a,1,2,1))]. given #252 (F,wt=10): 3672 B(cy,x v cy,x v (ca ^ cx)). [para(239(a,1),3572(a,2))]. given #253 (F,wt=10): 3675 B(cx,cx v x,(ca ^ cb) v x). [para(322(a,1),3572(a,2))]. given #254 (T,wt=10): 3676 B(cx,x v cx,x v (ca ^ cb)). [para(324(a,1),3572(a,2))]. given #255 (T,wt=10): 3678 B(cy,cy v x,(ca ^ cb) v x). [para(794(a,1),3572(a,2))]. given #256 (A,wt=13): 155 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(26(a,1),111(a,1,2)),rewrite(26(5))]. given #257 (F,wt=9): 5994 cx v (cb ^ (x ^ ca)) = cx. [para(155(a,1),456(a,1,2))]. given #258 (F,wt=9): 5996 cy v (cx ^ (x ^ ca)) = cy. [para(155(a,1),688(a,1,2))]. given #259 (T,wt=9): 5997 cy v (cb ^ (x ^ ca)) = cy. [para(155(a,1),835(a,1,2))]. given #260 (T,wt=9): 6035 cx v (cy ^ (x ^ cb)) = cx. [para(155(a,1),4811(a,1,2))]. given #261 (A,wt=13): 158 x v (y v (x v z)) = y v (x v z). [para(112(a,1),27(a,2,2)),rewrite(44(3),27(2))]. given #262 (F,wt=10): 3679 B(cy,x v cy,x v (ca ^ cb)). [para(798(a,1),3572(a,2))]. given #263 (F,wt=10): 3688 B(x,y v (z v x),y v z). [para(27(a,1),3658(a,2))]. given #264 (T,wt=10): 3691 B(x v y,x v (z v y),z). [para(44(a,1),3658(a,2))]. given #265 (T,wt=8): 6370 B(ca v cy,ca v cx,cx). [para(2664(a,1),3691(a,2))]. given #266 (A,wt=13): 160 x v (y v (z v x)) = y v (z v x). [para(27(a,1),116(a,1,2)),rewrite(27(5))]. given #267 (F,wt=8): 6383 B(cx v cy,cb v cy,cb). [para(3046(a,1),3691(a,2))]. given #268 (F,wt=8): 6389 B(ca v cy,ca v cb,cb). [para(3169(a,1),3691(a,2))]. given #269 (T,wt=9): 6445 cx ^ (cb v (x v ca)) = cx. [para(160(a,1),2622(a,1,2))]. given #270 (T,wt=9): 6447 cy ^ (cx v (x v ca)) = cy. [para(160(a,1),2669(a,1,2))]. given #271 (A,wt=13): 162 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(119(a,1),26(a,1,1)),flip(a)]. given #272 (F,wt=9): 6460 cy ^ (cb v (x v ca)) = cy. [para(160(a,1),3174(a,1,2))]. given #273 (F,wt=9): 6461 cx ^ (cy v (x v cb)) = cx. [para(160(a,1),4386(a,1,2))]. given #274 (T,wt=10): 3692 B((x ^ y) v z,x v z,x). [para(51(a,1),3658(a,2))]. given #275 (T,wt=10): 3693 B((x ^ y) v z,y v z,y). [para(122(a,1),3658(a,2))]. given #276 (A,wt=15): 163 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(119(a,1),26(a,1)),flip(a)]. given #277 (F,wt=10): 3694 B(x v (y ^ z),x v y,y). [para(125(a,1),3658(a,2))]. given #278 (F,wt=10): 3695 B(x v (y ^ z),x v z,z). [para(130(a,1),3658(a,2))]. given #279 (T,wt=10): 3700 B((ca ^ cx) v x,cy v x,cy). [para(237(a,1),3658(a,2))]. given #280 (T,wt=10): 3701 B(x v (ca ^ cx),x v cy,cy). [para(239(a,1),3658(a,2))]. given #281 (A,wt=17): 166 x ^ (y ^ (z v (x ^ (u v (x ^ y))))) = x ^ y. [para(37(a,1),119(a,1,2,2)),rewrite(26(6))]. given #282 (F,wt=10): 3704 B((ca ^ cb) v x,cx v x,cx). [para(322(a,1),3658(a,2))]. given #283 (F,wt=10): 3705 B(x v (ca ^ cb),x v cx,cx). [para(324(a,1),3658(a,2))]. given #284 (T,wt=10): 3707 B((ca ^ cb) v x,cy v x,cy). [para(794(a,1),3658(a,2))]. given #285 (T,wt=10): 3708 B(x v (ca ^ cb),x v cy,cy). [para(798(a,1),3658(a,2))]. given #286 (A,wt=13): 167 x ^ (y ^ (z v (u v x))) = y ^ x. [para(119(a,1),42(a,1,2)),flip(a)]. given #287 (F,wt=10): 3717 B(cb,cx,ca ^ (x v (y v cx))). [para(27(a,1),3453(a,3,2))]. given #288 (F,wt=10): 3718 B(ca,cy,cx ^ (x v (y v cy))). [para(27(a,1),3460(a,3,2))]. given #289 (T,wt=10): 3728 B(x,x v y,x v (y v z)). [para(112(a,1),114(b,1,1)),rewrite(27(3),27(7),48(8)),xx(b)]. given #290 (T,wt=8): 7301 B(ca,ca v cx,ca v cb). [para(2617(a,1),3728(a,3))]. given #291 (A,wt=15): 168 (x v y) ^ (z v (x v (u v y))) = x v y. [para(44(a,1),119(a,1,2,2))]. given #292 (F,wt=8): 7310 B(cx,cx v cb,cb v cy). [para(3046(a,1),3728(a,3))]. given #293 (F,wt=10): 3729 B(x,y v x,y v (x v z)). [para(116(a,1),114(b,1,1)),rewrite(27(3),27(7),48(8)),xx(b)]. given #294 (T,wt=8): 7436 B(x ^ y,x,x v z). [para(31(a,1),3729(a,2)),rewrite(51(4))]. given #295 (T,wt=8): 7441 B(x ^ y,y,y v z). [para(49(a,1),3729(a,2)),rewrite(122(4))]. given #296 (A,wt=15): 175 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(44(a,1),47(a,1,2,2))]. given #297 (F,wt=8): 7447 B(ca ^ cx,cy,cy v x). [para(228(a,1),3729(a,2)),rewrite(237(10))]. given #298 (F,wt=8): 7448 B(ca ^ cb,cx,cx v x). [para(319(a,1),3729(a,2)),rewrite(322(10))]. given #299 (T,wt=8): 7461 B(ca ^ cb,cy,cy v x). [para(711(a,1),3729(a,2)),rewrite(794(10))]. given #300 (T,wt=8): 7503 B(cx,ca v cx,ca v cb). [para(2617(a,1),3729(a,3))]. given #301 (A,wt=13): 178 x v ((y ^ (z ^ x)) v u) = x v u. [para(121(a,1),27(a,1,1)),flip(a)]. given #302 (F,wt=8): 7515 B(cb,cx v cb,cb v cy). [para(3046(a,1),3729(a,3))]. given #303 (F,wt=8): 7521 B(cb ^ cy,cx,cx v x). [para(4781(a,1),3729(a,2)),rewrite(4786(10))]. given #304 (T,wt=8): 7535 B(x ^ y,x,z v x). [para(25(a,1),7436(a,3))]. given #305 (T,wt=8): 7552 B(cx ^ x,cx,cb v cy). [para(3046(a,1),7436(a,3))]. given #306 (A,wt=13): 180 x v (y v (z ^ (u ^ x))) = y v x. [para(121(a,1),44(a,1,2)),flip(a)]. given #307 (F,wt=8): 7555 B(x ^ y,y,z v y). [para(25(a,1),7441(a,3))]. given #308 (F,wt=8): 7595 B(x ^ cx,cx,cb v cy). [para(3046(a,1),7441(a,3))]. given #309 (T,wt=8): 7651 B(ca ^ cx,cy,x v cy). [para(25(a,1),7447(a,3))]. given #310 (T,wt=8): 7656 B(ca ^ cb,cx,x v cx). [para(25(a,1),7448(a,3))]. given #311 (A,wt=15): 183 (x v y) ^ (z v (x v (y v u))) = x v y. [para(27(a,1),124(a,1,2,2))]. given #312 (F,wt=8): 7660 B(ca ^ cb,cx,cb v cy). [para(3046(a,1),7448(a,3))]. given #313 (F,wt=8): 7662 B(ca ^ cb,cy,x v cy). [para(25(a,1),7461(a,3))]. given #314 (T,wt=8): 7761 B(cb ^ cy,cx,x v cx). [para(25(a,1),7521(a,3))]. given #315 (T,wt=8): 7765 B(cb ^ cy,cx,cb v cy). [para(3046(a,1),7521(a,3))]. given #316 (A,wt=13): 184 x ^ (y v ((x v z) ^ (x v u))) = x. [para(35(a,1),124(a,1,2,2))]. given #317 (F,wt=10): 3794 B(cx,cy,ca ^ (x v (y v cy))). [para(27(a,1),3566(a,3,2))]. given #318 (F,wt=10): 4157 B(cx,cb v cy,cb v (cy v x)). [para(3046(a,1),114(b,1,1)),rewrite(27(8),27(16),48(17)),xx(b)]. given #319 (T,wt=10): 4899 B(ca,cx,cb ^ (x v (cx v y))). [para(44(a,1),4894(a,3,2))]. given #320 (T,wt=10): 4900 B(ca,cx,cb ^ (x v (cx ^ cb))). [para(80(a,1),4894(a,3)),rewrite(24(6))]. given #321 (A,wt=13): 186 x ^ (y ^ (z v (x v u))) = y ^ x. [para(124(a,1),42(a,1,2)),flip(a)]. given #322 (F,wt=10): 4919 B(ca,cx,cb ^ (x v (y v cx))). [para(27(a,1),4897(a,3,2))]. given #323 (F,wt=10): 5160 B(cb,cx,ca ^ (x v (cb v cy))). [para(3046(a,1),3456(a,3,2,2))]. given #324 (T,wt=10): 5225 B(x v y,y v (x v z),z). [para(25(a,1),3659(a,1))]. given #325 (T,wt=10): 5226 B(x v y,y v (z v x),z). [para(25(a,1),3659(a,2)),rewrite(27(3))]. given #326 (A,wt=13): 187 ca ^ ((cx v cy) ^ x) = ca ^ (cy ^ x). [para(152(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #327 (F,wt=10): 5246 B((x ^ y) v z,z v x,x). [para(212(a,1),3659(a,2))]. given #328 (F,wt=10): 5249 B((ca ^ cx) v x,x v cy,cy). [para(238(a,1),3659(a,2))]. given #329 (T,wt=10): 5257 B((ca ^ cb) v x,x v cx,cx). [para(323(a,1),3659(a,2))]. given #330 (T,wt=10): 5260 B((x ^ y) v z,z v y,y). [para(338(a,1),3659(a,2))]. given #331 (A,wt=17): 189 ca ^ (cx v (cy v (ca ^ x))) = ca ^ (cy v (ca ^ x)). [para(152(a,1),37(a,1,1)),rewrite(37(6),27(13)),flip(a)]. given #332 (F,wt=10): 5264 B((ca ^ cb) v x,x v cy,cy). [para(795(a,1),3659(a,2))]. given #333 (F,wt=10): 5343 B(x,x v (y v z),z v y). [para(25(a,1),3662(a,2)),rewrite(27(2))]. given #334 (T,wt=10): 5344 B(x,y v (x v z),z v y). [para(25(a,1),3662(a,3))]. given #335 (T,wt=10): 5424 B(cx,x v cx,x v (cb ^ cy)). [para(4781(a,1),3662(a,2,2))]. given #336 (A,wt=13): 190 ca ^ (x ^ (cx v cy)) = x ^ (ca ^ cy). [para(152(a,1),42(a,1,2)),flip(a)]. given #337 (F,wt=10): 5513 B(x,y v x,(x ^ z) v y). [para(25(a,1),3663(a,2))]. given #338 (F,wt=10): 5514 B(x,x v y,y v (x ^ z)). [para(25(a,1),3663(a,3))]. given #339 (T,wt=10): 5566 B(cx,cx v x,(cb ^ cy) v x). [para(4702(a,1),3663(a,3,1))]. given #340 (T,wt=10): 5572 B(x,y v x,(z ^ x) v y). [para(25(a,1),3664(a,2))]. given #341 (A,wt=13): 191 ca ^ ((cx v cb) ^ x) = ca ^ (cx ^ x). [para(153(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #342 (F,wt=10): 5573 B(x,x v y,y v (z ^ x)). [para(25(a,1),3664(a,3))]. given #343 (F,wt=10): 5847 B(cy,x v cy,(ca ^ cx) v x). [para(25(a,1),3671(a,2))]. given #344 (T,wt=10): 5848 B(cy,cy v x,x v (ca ^ cx)). [para(25(a,1),3671(a,3))]. given #345 (T,wt=10): 5927 B(cx,x v cx,(ca ^ cb) v x). [para(25(a,1),3675(a,2))]. given #346 (A,wt=17): 192 ca ^ (cx v (cb v (ca ^ x))) = ca ^ (cx v (ca ^ x)). [para(153(a,1),37(a,1,1)),rewrite(37(6),27(13)),flip(a)]. given #347 (F,wt=10): 5928 B(cx,cx v x,x v (ca ^ cb)). [para(25(a,1),3675(a,3))]. given #348 (F,wt=10): 5964 B(cy,x v cy,(ca ^ cb) v x). [para(25(a,1),3678(a,2))]. given #349 (T,wt=10): 5965 B(cy,cy v x,x v (ca ^ cb)). [para(25(a,1),3678(a,3))]. given #350 (T,wt=10): 6251 B(x,y v (z v x),z v y). [para(25(a,1),3688(a,3))]. given #351 (A,wt=13): 193 ca ^ (x ^ (cx v cb)) = x ^ (ca ^ cx). [para(153(a,1),42(a,1,2)),flip(a)]. given #352 (F,wt=10): 6310 B(x v y,z v (y v x),z). [para(25(a,1),3691(a,2)),rewrite(27(3))]. given #353 (F,wt=10): 6390 B(x v (cb ^ cy),x v cx,cx). [para(4781(a,1),3691(a,2,2))]. given #354 (T,wt=10): 6675 B(x v (y ^ z),y v x,y). [para(25(a,1),3692(a,1))]. given #355 (T,wt=10): 6725 B((cb ^ cy) v x,cx v x,cx). [para(4702(a,1),3692(a,1,1))]. given #356 (A,wt=13): 194 (x v y) ^ (y v (x v z)) = y v x. [para(25(a,1),48(a,1,1))]. given #357 (F,wt=10): 6732 B(x v (y ^ z),z v x,z). [para(25(a,1),3693(a,1))]. given #358 (F,wt=10): 6997 B(x v (ca ^ cx),cy v x,cy). [para(25(a,1),3700(a,1))]. given #359 (T,wt=10): 7120 B(x v (ca ^ cb),cx v x,cx). [para(25(a,1),3704(a,1))]. given #360 (T,wt=10): 7156 B(x v (ca ^ cb),cy v x,cy). [para(25(a,1),3707(a,1))]. given #361 (A,wt=13): 195 (x v y) ^ (y v (z v x)) = x v y. [para(25(a,1),48(a,1,2)),rewrite(27(3))]. given #362 (F,wt=10): 7269 B(x,y v x,x v (y v z)). [para(25(a,1),3728(a,2))]. given #363 (F,wt=10): 7270 B(x,x v y,x v (z v y)). [para(25(a,1),3728(a,3,2))]. given #364 (T,wt=8): 9385 B(ca,ca v cy,ca v cx). [para(2664(a,1),7270(a,3))]. given #365 (T,wt=8): 9396 B(cx,cx v cy,cb v cy). [para(3046(a,1),7270(a,3))]. given #366 (A,wt=19): 196 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(27(a,1),48(a,1,1)),rewrite(27(5),27(8))]. given #367 (F,wt=8): 9401 B(ca,ca v cy,ca v cb). [para(3169(a,1),7270(a,3))]. given #368 (F,wt=10): 7271 B(x,x v y,y v (z v x)). [para(25(a,1),3728(a,3)),rewrite(27(3))]. given #369 (T,wt=8): 9503 B(cy,ca v cy,ca v cx). [para(2664(a,1),7271(a,3)),rewrite(25(4))]. given #370 (T,wt=8): 9510 B(cy,cx v cy,cb v cy). [para(3046(a,1),7271(a,3)),rewrite(25(4))]. given #371 (A,wt=25): 197 (x v y) ^ ((x v z) ^ (x v ((y ^ (x v z)) v u))) = (x v y) ^ (x v z). [para(35(a,1),48(a,1,1)),rewrite(26(8),35(11))]. given #372 (F,wt=8): 9513 B(cy,ca v cy,ca v cb). [para(3169(a,1),7271(a,3)),rewrite(25(4))]. given #373 (F,wt=10): 7280 B(x,x v y,y v (x v z)). [para(44(a,1),3728(a,3))]. given #374 (T,wt=10): 7309 B(x,x v cx,x v (cb v cy)). [para(3046(a,1),3728(a,3,2))]. given #375 (T,wt=10): 7367 B(x,y v x,z v (y v x)). [para(168(a,1),91(c,1)),rewrite(45(9),116(7),53(7),116(9)),xx(b),xx(c)]. given #376 (A,wt=17): 198 (x v y) ^ (x v ((y v z) ^ (y v u))) = x v y. [para(35(a,1),48(a,1,2,2))]. given #377 (F,wt=8): 9606 B(cb,cx v cb,ca v cb). [para(2617(a,1),7367(a,3))]. given #378 (F,wt=8): 9608 B(cy,cx v cy,ca v cx). [para(2664(a,1),7367(a,3))]. given #379 (T,wt=8): 9612 B(cy,cb v cy,ca v cb). [para(3169(a,1),7367(a,3))]. given #380 (T,wt=10): 7433 B(x,y v x,y v (z v x)). [para(25(a,1),3729(a,3,2))]. given #381 (A,wt=21): 200 (x v (y ^ z)) ^ (x v (y ^ (z v (y ^ u)))) = x v (y ^ z). [para(37(a,1),48(a,1,2,2))]. given #382 (F,wt=10): 7434 B(x,y v x,x v (z v y)). [para(25(a,1),3729(a,3)),rewrite(27(3))]. given #383 (F,wt=10): 7444 B(x ^ (y ^ z),y,y v u). [para(102(a,1),3729(a,2)),rewrite(143(6))]. given #384 (T,wt=10): 7445 B(x ^ (y ^ z),z,z v u). [para(121(a,1),3729(a,2)),rewrite(178(6))]. given #385 (T,wt=10): 7453 B(x ^ (ca ^ cb),cx,cx v y). [para(454(a,1),3729(a,2)),rewrite(458(12))]. given #386 (A,wt=17): 201 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(48(a,1),42(a,1,2)),flip(a)]. given #387 (F,wt=10): 7454 B(ca ^ (cb ^ x),cx,cx v y). [para(456(a,1),3729(a,2)),rewrite(553(12))]. given #388 (F,wt=10): 7455 B(ca ^ (x ^ cb),cx,cx v y). [para(460(a,1),3729(a,2)),rewrite(564(12))]. given #389 (T,wt=10): 7458 B(x ^ (ca ^ cx),cy,cy v y). [para(674(a,1),3729(a,2)),rewrite(690(12))]. given #390 (T,wt=10): 7459 B(ca ^ (cx ^ x),cy,cy v y). [para(688(a,1),3729(a,2)),rewrite(703(12))]. given #391 (A,wt=19): 202 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(44(a,1),48(a,1,1)),rewrite(27(4))]. given #392 (F,wt=10): 7462 B(ca ^ (x ^ cx),cy,cy v y). [para(692(a,1),3729(a,2)),rewrite(809(12))]. given #393 (F,wt=10): 7463 B(x ^ (ca ^ cb),cy,cy v y). [para(834(a,1),3729(a,2)),rewrite(837(12))]. given #394 (T,wt=10): 7465 B(ca ^ (cb ^ x),cy,cy v y). [para(835(a,1),3729(a,2)),rewrite(879(12))]. given #395 (T,wt=10): 7466 B(ca ^ (x ^ cb),cy,cy v y). [para(839(a,1),3729(a,2)),rewrite(891(12))]. given #396 (A,wt=15): 203 (x v y) ^ (x v (z v (y v u))) = x v y. [para(44(a,1),48(a,1,2,2))]. given #397 (F,wt=10): 7469 B(x,(y ^ z) v x,x v y). [para(212(a,1),3729(a,3))]. given #398 (F,wt=10): 7472 B(x,(ca ^ cx) v x,x v cy). [para(238(a,1),3729(a,3))]. given #399 (T,wt=10): 7479 B(x,(ca ^ cb) v x,x v cx). [para(323(a,1),3729(a,3))]. given #400 (T,wt=10): 7482 B(x,(y ^ z) v x,x v z). [para(338(a,1),3729(a,3))]. given #401 (A,wt=17): 205 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(48(a,1),121(a,1,2,2)),rewrite(27(5),27(4))]. given #402 (F,wt=10): 7491 B(x,(ca ^ cb) v x,x v cy). [para(795(a,1),3729(a,3))]. given #403 (F,wt=10): 7514 B(cx,x v cx,x v (cb v cy)). [para(3046(a,1),3729(a,3,2))]. given #404 (T,wt=10): 7525 B(x ^ (cb ^ cy),cx,cx v y). [para(4785(a,1),3729(a,2)),rewrite(4999(12))]. given #405 (T,wt=10): 7526 B(cb ^ (cy ^ x),cx,cx v y). [para(4811(a,1),3729(a,2)),rewrite(5037(12))]. given #406 (A,wt=17): 206 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(26(a,1),51(a,1,2,1))]. given #407 (F,wt=10): 7527 B(cb ^ (x ^ cy),cx,cx v y). [para(5001(a,1),3729(a,2)),rewrite(5068(12))]. given #408 (F,wt=10): 7530 B(cb ^ (x ^ ca),cx,cx v y). [para(5994(a,1),3729(a,2)),rewrite(6075(12))]. given #409 (T,wt=10): 7531 B(cx ^ (x ^ ca),cy,cy v y). [para(5996(a,1),3729(a,2)),rewrite(6111(12))]. given #410 (T,wt=10): 7532 B(cb ^ (x ^ ca),cy,cy v y). [para(5997(a,1),3729(a,2)),rewrite(6147(12))]. given #411 (A,wt=17): 207 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(51(a,1),27(a,1)),rewrite(27(2)),flip(a)]. given #412 (F,wt=10): 7533 B(cy ^ (x ^ cb),cx,cx v y). [para(6035(a,1),3729(a,2)),rewrite(6185(12))]. given #413 (F,wt=10): 7540 B(x ^ y,x,z v (x v u)). [para(44(a,1),7436(a,3))]. given #414 (T,wt=8): 10460 B(cx ^ x,cx,ca v cb). [para(2617(a,1),7540(a,3))]. given #415 (T,wt=8): 10472 B(x ^ cx,cx,ca v cb). [para(24(a,1),10460(a,1))]. given #416 (A,wt=23): 208 x v (((x ^ y) v z) ^ ((x ^ y) v u)) = x v (z ^ ((x ^ y) v u)). [para(35(a,1),51(a,1,2))]. given #417 (F,wt=8): 10474 B(cb ^ cy,cx,ca v cb). [para(4702(a,1),10460(a,1))]. given #418 (F,wt=10): 7554 B(x ^ y,x,z v (u v x)). [para(160(a,1),7436(a,3))]. given #419 (T,wt=8): 10521 B(cy ^ x,cy,ca v cx). [para(2664(a,1),7554(a,3))]. given #420 (T,wt=8): 10523 B(cy ^ x,cy,ca v cb). [para(3169(a,1),7554(a,3))]. given #421 (A,wt=15): 210 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(51(a,1),45(a,1,2)),rewrite(24(4))]. given #422 (F,wt=8): 10536 B(x ^ cy,cy,ca v cx). [para(24(a,1),10521(a,1))]. given #423 (F,wt=8): 10539 B(x ^ cy,cy,ca v cb). [para(24(a,1),10523(a,1))]. given #424 (T,wt=10): 7560 B(x ^ y,y,z v (y v u)). [para(44(a,1),7441(a,3))]. given #425 (T,wt=10): 7584 B(cx,ca v cb,ca v (cb v x)). [para(2610(a,1),7441(a,1)),rewrite(27(8))]. given #426 (A,wt=15): 211 x v (y v ((x ^ z) v u)) = y v (x v u). [para(51(a,1),44(a,1,2)),flip(a)]. given #427 (F,wt=10): 7585 B(cy,ca v cx,ca v (cx v x)). [para(2611(a,1),7441(a,1)),rewrite(27(8))]. given #428 (F,wt=8): 10715 B(cy,ca v cx,ca v cb). [para(2617(a,1),7585(a,3))]. given #429 (T,wt=10): 7590 B(cy,ca v cb,ca v (cb v x)). [para(3106(a,1),7441(a,1)),rewrite(27(8))]. given #430 (T,wt=10): 7609 B(x ^ y,y,z v (u v y)). [para(160(a,1),7441(a,3))]. given #431 (A,wt=17): 213 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(51(a,1),119(a,1,2,2))]. given #432 (F,wt=10): 7653 B(ca ^ cx,cy,x v (cy v y)). [para(44(a,1),7447(a,3))]. given #433 (F,wt=10): 7655 B(ca ^ cx,cy,x v (y v cy)). [para(160(a,1),7447(a,3))]. given #434 (T,wt=8): 10824 B(ca ^ cx,cy,ca v cx). [para(2664(a,1),7655(a,3))]. given #435 (T,wt=8): 10825 B(ca ^ cx,cy,ca v cb). [para(3169(a,1),7655(a,3))]. given #436 (A,wt=17): 214 x ^ (y ^ (z ^ ((x ^ y) v u))) = z ^ (x ^ y). [para(101(a,1),26(a,1)),flip(a)]. given #437 (F,wt=10): 7658 B(ca ^ cb,cx,x v (cx v y)). [para(44(a,1),7448(a,3))]. given #438 (F,wt=8): 10827 B(ca ^ cb,cx,ca v cb). [para(2617(a,1),7658(a,3))]. given #439 (T,wt=10): 7661 B(ca ^ cb,cx,x v (y v cx)). [para(160(a,1),7448(a,3))]. given #440 (T,wt=10): 7664 B(ca ^ cb,cy,x v (cy v y)). [para(44(a,1),7461(a,3))]. given #441 (A,wt=15): 215 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(26(a,1),101(a,1,2)),rewrite(26(6))]. given #442 (F,wt=10): 7666 B(ca ^ cb,cy,x v (y v cy)). [para(160(a,1),7461(a,3))]. given #443 (F,wt=8): 10838 B(ca ^ cb,cy,ca v cx). [para(2664(a,1),7666(a,3))]. given #444 (T,wt=8): 10839 B(ca ^ cb,cy,ca v cb). [para(3169(a,1),7666(a,3))]. given #445 (T,wt=10): 7763 B(cb ^ cy,cx,x v (cx v y)). [para(44(a,1),7521(a,3))]. given #446 (A,wt=19): 216 x ^ ((y ^ (x v z)) v (x ^ u)) = x ^ (y v (x ^ u)). [para(101(a,1),37(a,1,1)),rewrite(78(3)),flip(a)]. given #447 (F,wt=10): 7766 B(cb ^ cy,cx,x v (y v cx)). [para(160(a,1),7521(a,3))]. given #448 (F,wt=10): 7768 B(x ^ (y ^ z),x ^ y,x). [para(31(a,1),7535(a,3)),rewrite(26(2))]. given #449 (T,wt=8): 10854 B(x ^ y,y ^ x,y). [para(111(a,1),7768(a,1))]. given #450 (T,wt=8): 10855 B(ca ^ cb,ca ^ cx,ca). [para(257(a,1),7768(a,1))]. given #451 (A,wt=13): 219 cx ^ ((ca v cy) ^ x) = cx ^ (cy ^ x). [para(217(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #452 (F,wt=8): 10864 B(cb ^ cy,cx ^ cb,cx). [para(4702(a,1),7768(a,1))]. given #453 (F,wt=10): 7771 B(x ^ (y ^ z),y,u v y). [para(42(a,1),7535(a,1))]. given #454 (T,wt=10): 7772 B(x ^ (y ^ z),x ^ y,y). [para(49(a,1),7535(a,3)),rewrite(26(2))]. given #455 (T,wt=8): 10940 B(x ^ y,y ^ x,x). [para(111(a,1),7772(a,1))]. given #456 (A,wt=17): 221 cx ^ (ca v (cy v (cx ^ x))) = cx ^ (cy v (cx ^ x)). [para(217(a,1),37(a,1,1)),rewrite(37(6),27(13)),flip(a)]. given #457 (F,wt=8): 10945 B(ca ^ cb,ca ^ cx,cx). [para(257(a,1),7772(a,1))]. given #458 (F,wt=8): 10972 B(cb ^ cy,cx ^ cb,cb). [para(4702(a,1),7772(a,1))]. given #459 (T,wt=10): 7777 B(ca ^ (cx ^ x),ca ^ cx,cy). [para(228(a,1),7535(a,3)),rewrite(26(4))]. given #460 (T,wt=8): 11007 B(ca ^ cb,ca ^ cx,cy). [para(257(a,1),7777(a,1))]. given #461 (A,wt=13): 222 cx ^ (x ^ (ca v cy)) = x ^ (cx ^ cy). [para(217(a,1),42(a,1,2)),flip(a)]. given #462 (F,wt=10): 7778 B(ca ^ (cb ^ x),ca ^ cb,cx). [para(319(a,1),7535(a,3)),rewrite(26(4))]. given #463 (F,wt=10): 7792 B(ca ^ (cb ^ x),ca ^ cb,cy). [para(711(a,1),7535(a,3)),rewrite(26(4))]. given #464 (T,wt=10): 7832 B(cb ^ (cy ^ x),cb ^ cy,cx). [para(4781(a,1),7535(a,3)),rewrite(26(4))]. given #465 (T,wt=10): 7842 B(x ^ (y ^ z),z,u v z). [para(155(a,1),7535(a,1))]. given #466 (A,wt=13): 223 ca ^ (cx ^ (cy ^ x)) = ca ^ (cx ^ x). [para(218(a,1),26(a,1,1)),rewrite(26(4),26(9)),flip(a)]. given #467 (F,wt=10): 7848 B(x ^ (cx ^ y),cx,cb v cy). [para(42(a,1),7552(a,1))]. given #468 (F,wt=10): 7849 B(x ^ (y ^ cx),cx,cb v cy). [para(155(a,1),7552(a,1))]. given #469 (T,wt=10): 7932 B(x,x v y,z v (x v y)). [para(29(a,1),7555(a,1))]. given #470 (T,wt=8): 11139 B(cx,cx v cb,ca v cb). [para(2617(a,1),7932(a,3))]. given #471 (A,wt=17): 225 ca ^ ((cx ^ cy) v (ca ^ x)) = ca ^ (cx v (ca ^ x)). [para(218(a,1),37(a,1,1)),rewrite(37(6)),flip(a)]. given #472 (F,wt=8): 11140 B(cx,cx v cy,ca v cx). [para(2664(a,1),7932(a,3))]. given #473 (F,wt=8): 11141 B(cb,cb v cy,ca v cb). [para(3169(a,1),7932(a,3))]. given #474 (T,wt=10): 7933 B(x ^ (y ^ z),y ^ z,y). [para(31(a,1),7555(a,3))]. given #475 (T,wt=8): 11160 B(ca ^ cx,cx ^ cy,cx). [para(218(a,1),7933(a,1))]. given #476 (A,wt=13): 226 ca ^ (x ^ (cx ^ cy)) = x ^ (ca ^ cx). [para(218(a,1),42(a,1,2)),flip(a)]. given #477 (F,wt=8): 11163 B(ca ^ cb,cx ^ cb,cx). [para(257(a,1),7933(a,1))]. given #478 (F,wt=8): 11164 B(ca ^ cb,cb ^ cy,cb). [para(797(a,1),7933(a,1))]. given #479 (T,wt=10): 7937 B(x ^ (y ^ z),y ^ z,z). [para(49(a,1),7555(a,3))]. given #480 (T,wt=8): 11205 B(ca ^ cx,cx ^ cy,cy). [para(218(a,1),7937(a,1))]. given #481 (A,wt=17): 241 x ^ (y ^ ((z v (x ^ y)) ^ u)) = x ^ (y ^ u). [para(117(a,1),26(a,1)),rewrite(26(2)),flip(a)]. given #482 (F,wt=8): 11211 B(ca ^ cb,cx ^ cb,cb). [para(257(a,1),7937(a,1))]. given #483 (F,wt=8): 11213 B(ca ^ cb,cb ^ cy,cy). [para(797(a,1),7937(a,1))]. given #484 (T,wt=10): 7948 B(x ^ (ca ^ cx),ca ^ cx,cy). [para(228(a,1),7555(a,3))]. given #485 (T,wt=10): 7952 B(x ^ (ca ^ cb),ca ^ cb,cx). [para(319(a,1),7555(a,3))]. given #486 (A,wt=15): 243 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(117(a,1),42(a,1,2)),flip(a)]. given #487 (F,wt=10): 7967 B(x ^ (ca ^ cb),ca ^ cb,cy). [para(711(a,1),7555(a,3))]. given #488 (F,wt=10): 8001 B(cx,ca v cb,x v (ca v cb)). [para(2610(a,1),7555(a,1))]. given #489 (T,wt=10): 8002 B(cy,ca v cx,x v (ca v cx)). [para(2611(a,1),7555(a,1))]. given #490 (T,wt=10): 8010 B(cy,ca v cb,x v (ca v cb)). [para(3106(a,1),7555(a,1))]. given #491 (A,wt=17): 245 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u. [para(44(a,1),117(a,1,2,1))]. given #492 (F,wt=10): 8019 B(cx,cb v cy,x v (cb v cy)). [para(4124(a,1),7555(a,1))]. given #493 (F,wt=8): 11296 B(cx,cb v cy,ca v cb). [para(3169(a,1),8019(a,3))]. given #494 (T,wt=10): 8031 B(x ^ (cb ^ cy),cb ^ cy,cx). [para(4781(a,1),7555(a,3))]. given #495 (T,wt=8): 11297 B(ca ^ cb,cb ^ cy,cx). [para(797(a,1),8031(a,1))]. given #496 (A,wt=17): 249 x ^ (y ^ (z ^ (x ^ u))) = y ^ (z ^ (x ^ u)). [para(121(a,1),117(a,1,2,1)),rewrite(42(4),26(3),26(2),26(7),26(6))]. low water: id=6227, wt=46 low water: id=6215, wt=42 low water: id=6575, wt=40 low water: id=6847, wt=39 low water: id=6858, wt=38 given #497 (F,wt=10): 8155 B(cx,cb v cy,cb v (x v cy)). [para(25(a,1),4157(a,3,2))]. given #498 (F,wt=10): 8161 B(cx,cb v cy,cy v (x v cb)). [para(160(a,1),4157(a,3))]. given #499 (T,wt=10): 8202 B(cb,cx,ca ^ (cb v (cy v x))). [para(25(a,1),5160(a,3,2)),rewrite(27(7))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 91 (0.00 of 2.45 sec). given #500 (T,wt=10): 8204 B(cb,cx,ca ^ (cb v (x v cy))). [para(44(a,1),5160(a,3,2))]. given #501 (A,wt=19): 250 (x v y) ^ (((x ^ z) v y) ^ u) = ((x ^ z) v y) ^ u. [para(51(a,1),117(a,1,2,1)),rewrite(42(5))]. low water: id=6449, wt=37 low water: id=7091, wt=36 low water: id=7069, wt=35 low water: id=7239, wt=34 given #502 (F,wt=10): 8347 B((cb ^ cy) v x,x v cx,cx). [para(4781(a,1),5226(a,2,2))]. given #503 (F,wt=10): 8484 B(cb,cx,ca ^ (cy v (ca ^ x))). [para(189(a,1),3436(a,3))]. low water: id=7409, wt=33 given #504 (T,wt=8): 11379 B(cb,cx,ca ^ (cy v x)). [para(35(a,1),8484(a,3,2)),rewrite(25(6),46(10))]. given #505 (T,wt=8): 11382 B(cb,cx,ca ^ (x v cy)). [para(25(a,1),11379(a,3,2))]. given #506 (A,wt=17): 252 x ^ (y ^ (z ^ (u v (x ^ y)))) = z ^ (x ^ y). [para(120(a,1),26(a,1)),flip(a)]. given #507 (F,wt=10): 8594 B(cx,x v cx,(cb ^ cy) v x). [para(4781(a,1),5344(a,2,2))]. given #508 (F,wt=10): 8614 B(cx,cx v x,x v (cb ^ cy)). [para(25(a,1),5424(a,2))]. given #509 (T,wt=10): 9014 B(x v (cb ^ cy),cx v x,cx). [para(25(a,1),6390(a,2))]. given #510 (T,wt=10): 9314 B(x,cx v x,x v (cb v cy)). [para(3046(a,1),7269(a,3,2))]. low water: id=6860, wt=32 low water: id=7422, wt=31 given #511 (A,wt=15): 253 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(26(a,1),120(a,1,2)),rewrite(26(6))]. given #512 (F,wt=10): 9317 B(x,x v y,z v (y v x)). [para(25(a,1),7270(a,3)),rewrite(27(3))]. low water: id=7119, wt=30 given #513 (F,wt=10): 9319 B(x,x v (y ^ z),x v y). [para(31(a,1),7270(a,3,2))]. low water: id=7929, wt=29 given #514 (T,wt=10): 9324 B(x,x v (y ^ z),x v z). [para(49(a,1),7270(a,3,2))]. low water: id=8054, wt=28 low water: id=8183, wt=27 given #515 (T,wt=10): 9330 B(x,x v (ca ^ cx),x v cy). [para(228(a,1),7270(a,3,2))]. given #516 (A,wt=19): 254 x ^ ((y ^ (z v x)) v (x ^ u)) = x ^ (y v (x ^ u)). [para(120(a,1),37(a,1,1)),rewrite(78(3)),flip(a)]. given #517 (F,wt=10): 9331 B(x,x v (ca ^ cb),x v cx). [para(319(a,1),7270(a,3,2))]. given #518 (F,wt=10): 9346 B(x,x v (ca ^ cb),x v cy). [para(711(a,1),7270(a,3,2))]. given #519 (T,wt=10): 9402 B(x,x v (cb ^ cy),x v cx). [para(4781(a,1),7270(a,3,2))]. given #520 (T,wt=10): 9549 B(cx,cx v x,x v (cb v cy)). [para(3046(a,1),7280(a,3,2))]. given #521 (A,wt=17): 255 (x v y) ^ (z ^ (x v (u v y))) = z ^ (x v y). [para(44(a,1),120(a,1,2,2))]. given #522 (F,wt=10): 9551 B(x,x v cx,cb v (cy v x)). [para(25(a,1),7309(a,3)),rewrite(27(6))]. given #523 (F,wt=10): 9554 B(x,x v cx,cb v (x v cy)). [para(44(a,1),7309(a,3))]. given #524 (T,wt=10): 9557 B(x,y v x,z v (x v y)). [para(25(a,1),7367(a,3,2))]. given #525 (T,wt=10): 9563 B(x,(y ^ z) v x,y v x). [para(51(a,1),7367(a,3))]. low water: id=8493, wt=26 given #526 (A,wt=19): 258 ((x ^ y) v z) ^ (u ^ (x v z)) = u ^ ((x ^ y) v z). [para(51(a,1),120(a,1,2,2))]. given #527 (F,wt=10): 9565 B(x,(y ^ z) v x,z v x). [para(122(a,1),7367(a,3))]. low water: id=8632, wt=25 given #528 (F,wt=10): 9569 B(x ^ (ca ^ cb),cx,y v cx). [para(454(a,1),7367(a,2)),rewrite(454(11))]. given #529 (T,wt=10): 9570 B(ca ^ (cb ^ x),cx,y v cx). [para(456(a,1),7367(a,2)),rewrite(456(11))]. given #530 (T,wt=10): 9571 B(ca ^ (x ^ cb),cx,y v cx). [para(460(a,1),7367(a,2)),rewrite(460(11))]. given #531 (A,wt=13): 261 cb ^ ((ca v cx) ^ x) = cx ^ (cb ^ x). [para(256(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #532 (F,wt=9): 11726 cb ^ (ca v cy) = cb ^ cy. [para(222(a,1),261(a,2)),rewrite(2661(8),42(10),4702(10))]. given #533 (F,wt=9): 11733 ca v (cb ^ cy) = ca v cy. [para(11726(a,1),35(a,1,2)),rewrite(3166(12))]. low water: id=8904, wt=24 given #534 (T,wt=8): 11748 B(ca,ca v cy,cb ^ cy). [para(11733(a,1),3572(a,2))]. given #535 (T,wt=8): 11749 B(cb ^ cy,ca v cy,ca). [para(11733(a,1),3658(a,2))]. given #536 (A,wt=17): 263 cb ^ (ca v (cx v (cb ^ x))) = cb ^ (cx v (cb ^ x)). [para(256(a,1),37(a,1,1)),rewrite(78(6),27(13)),flip(a)]. given #537 (F,wt=9): 11736 (ca v cy) ^ (cb v cy) = cy. [para(11726(a,1),70(a,1,2)),rewrite(49(5),25(4),25(7),24(8)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 2.72 (+ 0.03) seconds. % Length of proof is 72. % Level of proof is 17. % Maximum clause weight is 34. % Given clauses 537. 2 (all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)) # label(non_clause). [assumption]. 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 25 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 28 (x v y) ^ x = x # label("absorption_1"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 30 (x ^ y) v x = x # label("absorption_2"). [assumption]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 32 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 35 x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1"). [assumption]. 36 x ^ (y v (x ^ z)) = (x ^ y) v (x ^ z) # label("modularity_2"). [assumption]. 37 (x ^ y) v (x ^ z) = x ^ (y v (x ^ z)). [copy(36),flip(a)]. 38 B(ca,cy,cx). [assumption]. 39 B(ca,cx,cb). [assumption]. 40 -B(ca,cy,cb). [assumption]. 42 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. 44 x v (y v z) = y v (x v z). [para(25(a,1),27(a,1,1)),rewrite(27(2))]. 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. 46 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. 53 x ^ x = x. [para(31(a,1),29(a,1,2))]. 60 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (z v y) != y. [para(25(a,1),34(c,1,2))]. 70 x v (y ^ (z v x)) = (x v y) ^ (x v z). [para(25(a,1),35(a,1,2,2))]. 76 B(x,y,z ^ (y v u)) | (x ^ y) v (y ^ (z ^ (y v u))) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [para(35(a,1),34(c,1,2))]. 78 (x ^ y) v (y ^ z) = y ^ (x v (y ^ z)). [para(24(a,1),37(a,1,1))]. 89 B(x,y,z ^ (y v u)) | y ^ (x v (y ^ (z ^ (y v u)))) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [back_rewrite(76),rewrite(78(8))]. 93 B(x,y,z) | y ^ (x v (y ^ z)) != y | (x v y) ^ (z v y) != y. [back_rewrite(60),rewrite(78(4))]. 96 -B(x,y,z) | y ^ (x v (y ^ z)) = y. [back_rewrite(32),rewrite(78(4))]. 99 (ca v cy) ^ (cx v cy) = cy. [hyper(33,a,38,a),rewrite(25(6))]. 100 (ca v cx) ^ (cx v cb) = cx. [hyper(33,a,39,a)]. 101 x ^ (y ^ (x v z)) = y ^ x. [para(29(a,1),42(a,1,2)),flip(a)]. 105 B(x,y,z ^ (y v u)) | y ^ (x v (z ^ y)) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [back_rewrite(89),rewrite(101(6))]. 111 x ^ (y ^ x) = y ^ x. [para(53(a,1),26(a,2,2)),rewrite(24(2))]. 117 x ^ ((y v x) ^ z) = x ^ z. [para(45(a,1),26(a,1,1)),flip(a)]. 120 x ^ (y ^ (z v x)) = y ^ x. [para(45(a,1),42(a,1,2)),flip(a)]. 137 (ca v cx) ^ ((cx v cb) ^ x) = cx ^ x. [para(100(a,1),26(a,1,1)),flip(a)]. 152 ca ^ (cx v cy) = ca ^ cy. [para(99(a,1),46(a,1,2)),flip(a)]. 153 ca ^ (cx v cb) = ca ^ cx. [para(100(a,1),46(a,1,2)),flip(a)]. 155 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(26(a,1),111(a,1,2)),rewrite(26(5))]. 156 (x v y) ^ (z ^ x) = z ^ x. [para(111(a,1),46(a,2)),rewrite(155(4))]. 188 cx v (ca ^ cy) = (ca v cx) ^ (cx v cy). [para(152(a,1),35(a,1,2)),rewrite(25(8))]. 217 cx ^ (ca v cy) = cx ^ cy. [para(99(a,1),101(a,1,2)),rewrite(24(8)),flip(a)]. 220 ca v (cx ^ cy) = (ca v cx) ^ (ca v cy). [para(217(a,1),35(a,1,2))]. 222 cx ^ (x ^ (ca v cy)) = x ^ (cx ^ cy). [para(217(a,1),42(a,1,2)),flip(a)]. 256 cb ^ (ca v cx) = cx ^ cb. [para(100(a,1),120(a,1,2)),rewrite(24(3),24(8)),flip(a)]. 261 cb ^ ((ca v cx) ^ x) = cx ^ (cb ^ x). [para(256(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. 262 ca v (cx ^ cb) = (ca v cx) ^ (ca v cb). [para(256(a,1),35(a,1,2)),rewrite(24(12))]. 728 cb v (ca ^ cx) = (ca v cb) ^ (cx v cb). [para(153(a,1),70(a,1,2)),rewrite(25(8),25(11))]. 2610 cx ^ (ca v cb) = cx. [hyper(96,a,39,a),rewrite(262(6),117(9))]. 2611 cy ^ (ca v cx) = cy. [hyper(96,a,38,a),rewrite(24(5),220(6),120(9),24(5))]. 2617 ca v (cx v cb) = ca v cb. [para(2610(a,1),49(a,1,2)),rewrite(25(5),44(5))]. 2624 (ca v cb) ^ (cx v cb) = cx v cb. [para(2610(a,1),70(a,1,2)),rewrite(25(3),25(6),25(9),24(10)),flip(a)]. 2659 cb v (ca ^ cx) = cx v cb. [back_rewrite(728),rewrite(2624(12))]. 2661 (ca v cx) ^ (ca v cy) = ca v cy. [para(2611(a,1),35(a,1,2)),rewrite(24(10)),flip(a)]. 2669 cy ^ (ca v (cx v x)) = cy. [para(2611(a,1),156(a,1,2)),rewrite(27(4),24(6),2611(11))]. 2671 (ca v cx) ^ (cx v cy) = cx v cy. [para(2611(a,1),70(a,1,2)),rewrite(25(9),24(10)),flip(a)]. 2703 cx v (ca ^ cy) = cx v cy. [back_rewrite(188),rewrite(2671(12))]. 3106 cy ^ (ca v cb) = cy. [para(2617(a,1),2669(a,1,2))]. 3166 (ca v cb) ^ (ca v cy) = ca v cy. [para(3106(a,1),35(a,1,2)),rewrite(24(10)),flip(a)]. 3436 B(cb,cx,ca ^ (cx v x)). [para(2659(a,1),105(b,1,2)),rewrite(29(12),25(13),25(16),42(20),137(20),29(14)),xx(b),xx(c)]. 3457 B(cb,cx,ca ^ cy). [para(152(a,1),3436(a,3))]. 3459 (cx v cb) ^ (cx v cy) = cx. [hyper(33,a,3457,a),rewrite(25(3),2703(8))]. 4590 cb ^ (cx v cy) = cx ^ cb. [para(3459(a,1),117(a,1,2)),rewrite(24(3)),flip(a)]. 4702 cx ^ (cb ^ cy) = cb ^ cy. [para(4590(a,1),120(a,1,2)),rewrite(42(5),24(4))]. 11726 cb ^ (ca v cy) = cb ^ cy. [para(222(a,1),261(a,2)),rewrite(2661(8),42(10),4702(10))]. 11733 ca v (cb ^ cy) = ca v cy. [para(11726(a,1),35(a,1,2)),rewrite(3166(12))]. 11736 (ca v cy) ^ (cb v cy) = cy. [para(11726(a,1),70(a,1,2)),rewrite(49(5),25(4),25(7),24(8)),flip(a)]. 11800 B(ca,cy,cb). [para(11736(a,1),93(c,1)),rewrite(24(9),11733(10),45(9)),xx(b),xx(c)]. 11801 $F. [resolve(11800,a,40,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=537. Generated=74637. Kept=11774. proofs=1. Usable=527. Sos=9999. Demods=2753. Limbo=6, Disabled=1272. Hints=0. Weight_deleted=4. Literals_deleted=0. Forward_subsumed=55991. Back_subsumed=124. Sos_limit_deleted=6868. Sos_displaced=380. Sos_removed=0. New_demodulators=3180 (6 lex), Back_demodulated=735. Back_unit_deleted=0. Demod_attempts=1187397. Demod_rewrites=149405. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=422357. Nonunit_bsub_feature_tests=261383. Megabytes=10.06. User_CPU=2.72, System_CPU=0.03, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11455 exit (max_proofs) Sat Aug 12 21:01:42 2006