============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11454 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:32 2006 The command was "/home/mccune/bin/prover9 -f head.in t3_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 t3_12.in formulas(sos). x ^ (y v z) = (x ^ y) v (x ^ z) # label(dist_1). x v (y ^ z) = (x v y) ^ (x v z) # label(dist_2). B(a,b,c). B(a,d,c). B(b,e,d). -B(a,e,c). 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 ^ (y v z) = (x ^ y) v (x ^ z) # label(dist_1). [assumption]. x v (y ^ z) = (x v y) ^ (x v z) # label(dist_2). [assumption]. B(a,b,c). [assumption]. B(a,d,c). [assumption]. B(b,e,d). [assumption]. -B(a,e,c). [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([ a, b, c, d, e, ^, 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))]. 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. 37 x v (y ^ z) = (x v y) ^ (x v z) # label(dist_2). [assumption]. 38 B(a,b,c). [assumption]. 39 B(a,d,c). [assumption]. 40 B(b,e,d). [assumption]. 41 -B(a,e,c). [assumption]. 42 x ^ ((x ^ y) v z) = x ^ (y v z). [back_rewrite(36),rewrite(37(3),25(2),31(2))]. 43 B(x,y,z) | (y v x) ^ ((y v y) ^ ((x ^ y) v z)) != y | (x v y) ^ (y v z) != y. [back_rewrite(34),rewrite(37(4),25(3),37(3),26(7))]. 44 -B(x,y,z) | (y v x) ^ ((y v y) ^ ((x ^ y) v z)) = y. [back_rewrite(32),rewrite(37(4),25(3),37(3),26(7))]. 45 (x v x) ^ (x v y) = x. [back_rewrite(31),rewrite(37(2))]. 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))]. 37 x v (y ^ z) = (x v y) ^ (x v z) # label(dist_2). [assumption]. 42 x ^ ((x ^ y) v z) = x ^ (y v z). [back_rewrite(36),rewrite(37(3),25(2),31(2))]. 45 (x v x) ^ (x v y) = x. [back_rewrite(31),rewrite(37(2))]. 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: 46 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: 48 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=13): 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. given #7 (I,wt=13): 37 x v (y ^ z) = (x v y) ^ (x v z) # label(dist_2). [assumption]. given #8 (I,wt=4): 38 B(a,b,c). [assumption]. given #9 (I,wt=4): 39 B(a,d,c). [assumption]. given #10 (I,wt=4): 40 B(b,e,d). [assumption]. given #11 (I,wt=4): 41 -B(a,e,c). [assumption]. given #12 (I,wt=13): 42 x ^ ((x ^ y) v z) = x ^ (y v z). [back_rewrite(36),rewrite(37(3),25(2),31(2))]. given #13 (I,wt=28): 43 B(x,y,z) | (y v x) ^ ((y v y) ^ ((x ^ y) v z)) != y | (x v y) ^ (y v z) != y. [back_rewrite(34),rewrite(37(4),25(3),37(3),26(7))]. given #14 (I,wt=19): 44 -B(x,y,z) | (y v x) ^ ((y v y) ^ ((x ^ y) v z)) = y. [back_rewrite(32),rewrite(37(4),25(3),37(3),26(7))]. given #15 (I,wt=9): 45 (x v x) ^ (x v y) = x. [back_rewrite(31),rewrite(37(2))]. given #16 (A,wt=11): 47 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. given #17 (F,wt=4): 89 B(x,x,y). [para(45(a,1),43(c,1)),rewrite(85(7),42(4),29(3)),xx(b),xx(c)]. given #18 (F,wt=7): 50 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. given #19 (T,wt=4): 108 B(x,y,y). [back_rewrite(102),rewrite(104(1),104(3),104(3),24(3),50(3)),xx(b)]. given #20 (T,wt=5): 100 x ^ x = x. [para(50(a,1),42(a,2)),rewrite(25(2),37(2),45(3))]. given #21 (A,wt=11): 49 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=5): 104 x v x = x. [para(50(a,1),45(a,1))]. given #23 (F,wt=7): 106 b ^ (a v c) = b. [back_rewrite(82),rewrite(95(9))]. given #24 (T,wt=7): 110 d ^ (a v c) = d. [back_rewrite(81),rewrite(104(12),24(11),50(11),24(8),50(8),24(5))]. given #25 (T,wt=7): 111 e ^ (b v d) = e. [back_rewrite(80),rewrite(104(12),24(11),50(11),24(8),50(8),24(5))]. given #26 (A,wt=11): 51 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. given #27 (F,wt=9): 56 (a v b) ^ (b v c) = b. [hyper(33,a,38,a)]. given #28 (F,wt=9): 57 (a v d) ^ (c v d) = d. [hyper(33,a,39,a),rewrite(25(6))]. given #29 (T,wt=9): 58 (b v e) ^ (d v e) = e. [hyper(33,a,40,a),rewrite(25(6))]. given #30 (T,wt=9): 97 x ^ (y v (z v x)) = x. [para(27(a,1),50(a,1,2))]. given #31 (A,wt=13): 53 (x v y) ^ (x v (y v z)) = x v y. [para(27(a,1),29(a,1,2))]. given #32 (F,wt=9): 99 x ^ (y v (x v z)) = x. [para(50(a,1),42(a,1,2,1)),rewrite(29(2),27(2)),flip(a)]. given #33 (F,wt=9): 120 x ^ (x ^ y) = x ^ y. [para(100(a,1),26(a,1,1)),flip(a)]. given #34 (T,wt=9): 122 x ^ (y ^ x) = y ^ x. [para(100(a,1),26(a,2,2)),rewrite(24(2))]. given #35 (T,wt=9): 124 x v (x v y) = x v y. [para(104(a,1),27(a,1,1)),flip(a)]. given #36 (A,wt=13): 54 (x ^ y) v z = (z v x) ^ (z v y). [para(37(a,1),25(a,1)),flip(a)]. given #37 (F,wt=9): 126 x v (y v x) = y v x. [para(104(a,1),27(a,2,2)),rewrite(25(2))]. given #38 (F,wt=9): 133 b ^ (a v (c v x)) = b. [para(106(a,1),42(a,1,2,1)),rewrite(29(4),27(6)),flip(a)]. given #39 (T,wt=9): 137 d ^ (a v (c v x)) = d. [para(110(a,1),42(a,1,2,1)),rewrite(29(4),27(6)),flip(a)]. given #40 (T,wt=9): 141 e ^ (b v (d v x)) = e. [para(111(a,1),42(a,1,2,1)),rewrite(29(4),27(6)),flip(a)]. given #41 (A,wt=17): 55 ((x v y) ^ (x v z)) v u = x v ((y ^ z) v u). [para(37(a,1),27(a,1,1))]. given #42 (F,wt=9): 155 a ^ (b v c) = a ^ b. [para(56(a,1),51(a,1,2)),flip(a)]. given #43 (F,wt=9): 160 a ^ (c v d) = a ^ d. [para(57(a,1),51(a,1,2)),flip(a)]. given #44 (T,wt=9): 165 b ^ (d v e) = b ^ e. [para(58(a,1),51(a,1,2)),flip(a)]. given #45 (T,wt=9): 221 b ^ (a v (x v c)) = b. [para(25(a,1),133(a,1,2,2))]. given #46 (A,wt=11): 65 x ^ (y ^ (x v z)) = x ^ y. [back_rewrite(52),rewrite(59(3))]. given #47 (F,wt=9): 227 d ^ (a v (x v c)) = d. [para(25(a,1),137(a,1,2,2))]. given #48 (F,wt=9): 233 e ^ (b v (x v d)) = e. [para(25(a,1),141(a,1,2,2))]. given #49 (T,wt=9): 279 b ^ (x v (a v c)) = b. [para(49(a,1),221(a,1,2))]. given #50 (T,wt=9): 282 c ^ (a v d) = c ^ d. [para(57(a,1),65(a,1,2)),flip(a)]. given #51 (A,wt=20): 93 B(x,y,z) | y ^ (x v z) != y | (x v y) ^ (y v z) != y. [para(47(a,1),43(b,1)),rewrite(85(7),59(4))]. given #52 (F,wt=6): 307 B(x,x v y,y). [para(100(a,1),93(b,1)),rewrite(124(7),25(8),126(8),100(8)),xx(b),xx(c)]. given #53 (F,wt=6): 333 B(x,y v x,y). [para(25(a,1),307(a,2))]. given #54 (T,wt=8): 317 B(x,x v y,y v z). [para(53(a,1),93(b,1)),rewrite(124(8),49(10),27(9),190(10),53(10)),xx(b),xx(c)]. given #55 (T,wt=8): 340 B(x,y v x,y v z). [para(25(a,1),317(a,2))]. given #56 (A,wt=11): 95 x ^ ((y v x) ^ z) = x ^ z. [para(50(a,1),26(a,1,1)),flip(a)]. given #57 (F,wt=8): 341 B(x,x v y,z v y). [para(25(a,1),317(a,3))]. given #58 (F,wt=8): 348 B(x,y v x,z v y). [para(25(a,1),340(a,3))]. given #59 (T,wt=9): 283 d ^ (b v e) = d ^ e. [para(58(a,1),65(a,1,2)),flip(a)]. given #60 (T,wt=9): 284 a ^ (c ^ d) = a ^ c. [para(160(a,1),65(a,1,2)),rewrite(47(5),24(8))]. given #61 (A,wt=13): 98 (x v y) ^ (x v (z v y)) = x v y. [para(50(a,1),37(a,1,2)),flip(a)]. given #62 (F,wt=9): 285 b ^ (d ^ e) = b ^ d. [para(165(a,1),65(a,1,2)),rewrite(47(5),24(8))]. given #63 (F,wt=9): 291 d ^ (x v (a v c)) = d. [para(49(a,1),227(a,1,2))]. given #64 (T,wt=9): 296 e ^ (x v (b v d)) = e. [para(49(a,1),233(a,1,2))]. given #65 (T,wt=10): 334 B(x v y,x v (y v z),z). [para(27(a,1),307(a,2))]. given #66 (A,wt=11): 103 B(x,y,x v y) | x v y != y. [para(50(a,1),43(c,1)),rewrite(49(7),25(6),37(6),83(7),84(6),24(4),29(4)),xx(b)]. given #67 (F,wt=8): 402 B(x v y,y v x,x). [para(126(a,1),334(a,2))]. given #68 (F,wt=10): 336 B(x,y v (x v z),y v z). [para(49(a,1),307(a,2))]. given #69 (T,wt=10): 337 B(x,y v (z v x),y v z). [para(27(a,1),333(a,2))]. given #70 (T,wt=10): 339 B(x v y,x v (z v y),z). [para(49(a,1),333(a,2))]. given #71 (A,wt=11): 105 x ^ (y ^ (z v x)) = y ^ x. [para(50(a,1),47(a,1,2)),flip(a)]. given #72 (F,wt=9): 432 c ^ (a v b) = b ^ c. [para(56(a,1),105(a,1,2)),rewrite(24(3),24(8)),flip(a)]. given #73 (F,wt=9): 433 a ^ (b ^ c) = a ^ c. [para(155(a,1),105(a,1,2)),rewrite(47(5),24(4))]. given #74 (T,wt=10): 347 B(x,x v y,z v (y v u)). [para(49(a,1),317(a,3))]. given #75 (T,wt=10): 353 B(x,y v x,z v (y v u)). [para(49(a,1),340(a,3))]. given #76 (A,wt=26): 113 B(x v y,z,u) | z ^ (x v (y v u)) != z | (x v (y v z)) ^ (z v u) != z. [back_rewrite(74),rewrite(104(5),59(8),27(6),47(8),51(8))]. given #77 (F,wt=8): 465 B(x v y,y v z,z). [para(50(a,1),113(b,1)),rewrite(124(8),25(10),126(10),24(10),50(10)),xx(b),xx(c)]. given #78 (F,wt=8): 491 B(x v y,x v z,z). [para(98(a,1),113(b,1)),rewrite(190(9),25(10),126(10),24(10),50(10)),xx(b),xx(c)]. given #79 (T,wt=8): 495 B(x v y,z v y,z). [para(25(a,1),465(a,2))]. given #80 (T,wt=8): 502 B(x v y,z v x,z). [para(25(a,1),491(a,2))]. given #81 (A,wt=20): 115 B(x,y,z) | y ^ (x v z) != y | (x v y) ^ (z v y) != y. [back_rewrite(71),rewrite(104(3),59(5),47(5),51(5))]. given #82 (F,wt=10): 359 B(x,x v y,z v (u v y)). [para(27(a,1),341(a,3))]. given #83 (F,wt=10): 364 B(x,y v x,z v (u v y)). [para(27(a,1),348(a,3))]. given #84 (T,wt=10): 395 B(x v y,y v (x v z),z). [para(25(a,1),334(a,1))]. given #85 (T,wt=10): 396 B(x v y,y v (z v x),z). [para(25(a,1),334(a,2)),rewrite(27(3))]. given #86 (A,wt=20): 116 B(x,y,z) | y ^ (x v z) != y | (y v x) ^ (y v z) != y. [back_rewrite(70),rewrite(104(3),59(5),47(5),51(5))]. given #87 (F,wt=10): 413 B(x,x v (y v z),z v y). [para(25(a,1),336(a,2)),rewrite(27(2))]. given #88 (F,wt=10): 414 B(x,y v (x v z),z v y). [para(25(a,1),336(a,3))]. given #89 (T,wt=10): 419 B(x,y v (z v x),z v y). [para(25(a,1),337(a,3))]. given #90 (T,wt=10): 425 B(x v y,z v (y v x),z). [para(25(a,1),339(a,2)),rewrite(27(3))]. given #91 (A,wt=20): 118 B(x,y,z) | y ^ (x v z) != y | (y v z) ^ (x v y) != y. [back_rewrite(67),rewrite(104(3),59(5),47(5),51(5))]. given #92 (F,wt=10): 496 B(x v (y v z),z v u,u). [para(27(a,1),465(a,1))]. given #93 (F,wt=10): 506 B(x v (y v z),y v u,u). [para(49(a,1),491(a,1))]. given #94 (T,wt=10): 508 B(x v (y v z),u v z,u). [para(27(a,1),495(a,1))]. given #95 (T,wt=10): 517 B(x v (y v z),u v y,u). [para(49(a,1),502(a,1))]. given #96 (A,wt=11): 119 -B(x,y,z) | y ^ (x v z) = y. [back_rewrite(44),rewrite(104(3),59(5),47(5),51(5))]. given #97 (F,wt=11): 131 b ^ ((a v c) ^ x) = b ^ x. [para(106(a,1),26(a,1,1)),flip(a)]. given #98 (F,wt=11): 134 b ^ (x ^ (a v c)) = x ^ b. [para(106(a,1),47(a,1,2)),flip(a)]. given #99 (T,wt=11): 135 d ^ ((a v c) ^ x) = d ^ x. [para(110(a,1),26(a,1,1)),flip(a)]. given #100 (T,wt=11): 138 d ^ (x ^ (a v c)) = x ^ d. [para(110(a,1),47(a,1,2)),flip(a)]. given #101 (A,wt=17): 127 B(x,x v y,z) | (x v y) ^ (x v z) != x v y. [back_rewrite(109),rewrite(124(4),124(4),126(5),124(5),120(7),124(9),124(9),53(11)),xx(c)]. given #102 (F,wt=11): 139 e ^ ((b v d) ^ x) = e ^ x. [para(111(a,1),26(a,1,1)),flip(a)]. given #103 (F,wt=11): 142 e ^ (x ^ (b v d)) = x ^ e. [para(111(a,1),47(a,1,2)),flip(a)]. given #104 (T,wt=11): 168 x ^ (y v (z v (u v x))) = x. [para(27(a,1),97(a,1,2,2))]. given #105 (T,wt=11): 170 x ^ (y v (z v (x v u))) = x. [para(97(a,1),42(a,1,2,1)),rewrite(29(2),27(3),27(2)),flip(a)]. given #106 (A,wt=17): 130 B(x,y v x,z) | (y v x) ^ (x v z) != y v x. [back_rewrite(101),rewrite(126(4),126(9),53(11)),xx(c)]. given #107 (F,wt=11): 187 (x v y) ^ (z ^ x) = z ^ x. [para(122(a,1),51(a,2)),rewrite(186(4))]. given #108 (F,wt=11): 219 (x v y) ^ (y v x) = x v y. [para(126(a,1),53(a,1,2))]. given #109 (T,wt=11): 226 b ^ (a v (x v (c v y))) = b. [para(49(a,1),133(a,1,2,2))]. given #110 (T,wt=11): 232 d ^ (a v (x v (c v y))) = d. [para(49(a,1),137(a,1,2,2))]. given #111 (A,wt=13): 132 (x v b) ^ (x v (a v c)) = x v b. [para(106(a,1),37(a,1,2)),flip(a)]. given #112 (F,wt=8): 752 B(x,x v b,a v c). [hyper(127,b,132,a)]. given #113 (F,wt=8): 773 B(x,b v x,a v c). [para(25(a,1),752(a,2))]. given #114 (T,wt=9): 762 a v (b v c) = a v c. [para(104(a,1),132(a,1,2)),rewrite(25(5),49(5),24(9),98(9),25(8),49(8)),flip(a)]. given #115 (T,wt=8): 823 B(a v c,b v x,x). [para(762(a,1),506(a,1))]. given #116 (A,wt=13): 136 (x v d) ^ (x v (a v c)) = x v d. [para(110(a,1),37(a,1,2)),flip(a)]. given #117 (F,wt=7): 849 e ^ (a v c) = e. [para(136(a,1),139(a,1,2)),rewrite(111(5),49(7),762(7)),flip(a)]. given #118 (F,wt=8): 826 B(a v c,x v b,x). [para(762(a,1),517(a,1))]. given #119 (T,wt=8): 834 B(x,x v d,a v c). [hyper(127,b,136,a)]. given #120 (T,wt=8): 862 B(x,d v x,a v c). [para(25(a,1),834(a,2))]. given #121 (A,wt=13): 140 (x v e) ^ (x v (b v d)) = x v e. [para(111(a,1),37(a,1,2)),flip(a)]. given #122 (F,wt=8): 866 B(x,x v e,b v d). [hyper(127,b,140,a)]. given #123 (F,wt=8): 887 B(x,e v x,b v d). [para(25(a,1),866(a,2))]. given #124 (T,wt=9): 844 a v (c v d) = a v c. [para(104(a,1),136(a,1,2)),rewrite(25(5),49(5),25(4),24(9),53(9),25(8),49(8),25(7)),flip(a)]. given #125 (T,wt=8): 933 B(a v c,d v x,x). [para(844(a,1),496(a,1))]. given #126 (A,wt=17): 144 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(27(a,1),51(a,1,2,1))]. given #127 (F,wt=8): 937 B(a v c,x v d,x). [para(844(a,1),508(a,1))]. given #128 (F,wt=9): 860 e ^ (a v (c v x)) = e. [para(849(a,1),187(a,1,2)),rewrite(27(4),24(6),849(11))]. given #129 (T,wt=9): 876 b v (d v e) = b v d. [para(104(a,1),140(a,1,2)),rewrite(25(5),49(5),25(4),24(9),53(9),25(8),49(8),25(7)),flip(a)]. given #130 (T,wt=8): 1005 B(b v d,e v x,x). [para(876(a,1),496(a,1))]. given #131 (A,wt=15): 146 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(51(a,1),47(a,1,2)),flip(a)]. given #132 (F,wt=8): 1009 B(b v d,x v e,x). [para(876(a,1),508(a,1))]. given #133 (F,wt=9): 956 e ^ (a v (x v c)) = e. [para(25(a,1),860(a,1,2,2))]. given #134 (T,wt=9): 1042 e ^ (x v (a v c)) = e. [para(49(a,1),956(a,1,2))]. given #135 (T,wt=10): 784 B(b v c,a v c,a v x). [para(762(a,1),340(a,2))]. given #136 (A,wt=13): 147 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(49(a,1),51(a,1,2,1))]. given #137 (F,wt=10): 786 B(x,x v (b v c),a v c). [para(762(a,1),341(a,3))]. given #138 (F,wt=10): 787 B(b v c,a v c,x v a). [para(762(a,1),348(a,2))]. given #139 (T,wt=10): 788 B(x,b v (c v x),a v c). [para(762(a,1),348(a,3)),rewrite(27(4))]. given #140 (T,wt=10): 800 B(a v c,b v (c v x),x). [para(762(a,1),465(a,1)),rewrite(27(7))]. given #141 (A,wt=32): 149 B(x,y v z,u) | (y v z) ^ (x v u) != y v z | (x v (y v z)) ^ (y v (z v u)) != y v z. [back_rewrite(129),rewrite(144(8))]. given #142 (F,wt=10): 801 B(x v a,a v c,b v c). [para(762(a,1),465(a,2))]. given #143 (F,wt=10): 802 B(a v x,a v c,b v c). [para(762(a,1),491(a,2))]. given #144 (T,wt=10): 803 B(a v c,x v (b v c),x). [para(762(a,1),495(a,1))]. given #145 (T,wt=10): 898 B(c v d,a v c,a v x). [para(844(a,1),340(a,2))]. given #146 (A,wt=13): 151 (a v b) ^ ((b v c) ^ x) = b ^ x. [para(56(a,1),26(a,1,1)),flip(a)]. given #147 (F,wt=10): 900 B(x,x v (c v d),a v c). [para(844(a,1),341(a,3))]. given #148 (F,wt=10): 901 B(c v d,a v c,x v a). [para(844(a,1),348(a,2))]. given #149 (T,wt=10): 902 B(x,c v (d v x),a v c). [para(844(a,1),348(a,3)),rewrite(27(4))]. given #150 (T,wt=10): 911 B(a v c,c v (d v x),x). [para(844(a,1),465(a,1)),rewrite(27(7))]. given #151 (A,wt=15): 152 (x v (a v b)) ^ (x v (b v c)) = x v b. [para(56(a,1),37(a,1,2)),flip(a)]. given #152 (F,wt=6): 1137 B(a,a v b,c). [para(152(a,1),149(c,1)),rewrite(763(13)),xx(b),xx(c)]. given #153 (F,wt=8): 1132 B(a v b,b,b v c). [para(152(a,1),113(c,1)),rewrite(25(3),762(15),49(14),762(14),106(13),104(14)),xx(b),xx(c)]. given #154 (T,wt=10): 912 B(x v a,a v c,c v d). [para(844(a,1),465(a,2))]. given #155 (T,wt=10): 913 B(a v x,a v c,c v d). [para(844(a,1),491(a,2))]. given #156 (A,wt=17): 153 (a v b) ^ (b v (c v x)) = (a v b) ^ (b v x). [para(56(a,1),42(a,1,2,1)),rewrite(27(13)),flip(a)]. given #157 (F,wt=10): 914 B(a v c,x v (c v d),x). [para(844(a,1),495(a,1))]. given #158 (F,wt=10): 970 B(d v e,b v d,b v x). [para(876(a,1),340(a,2))]. given #159 (T,wt=10): 972 B(x,x v (d v e),b v d). [para(876(a,1),341(a,3))]. given #160 (T,wt=10): 973 B(d v e,b v d,x v b). [para(876(a,1),348(a,2))]. given #161 (A,wt=13): 154 (a v b) ^ (x ^ (b v c)) = x ^ b. [para(56(a,1),47(a,1,2)),flip(a)]. given #162 (F,wt=10): 974 B(x,d v (e v x),b v d). [para(876(a,1),348(a,3)),rewrite(27(4))]. given #163 (F,wt=10): 983 B(b v d,d v (e v x),x). [para(876(a,1),465(a,1)),rewrite(27(7))]. given #164 (T,wt=10): 984 B(x v b,b v d,d v e). [para(876(a,1),465(a,2))]. given #165 (T,wt=10): 985 B(b v x,b v d,d v e). [para(876(a,1),491(a,2))]. given #166 (A,wt=13): 156 (a v d) ^ ((c v d) ^ x) = d ^ x. [para(57(a,1),26(a,1,1)),flip(a)]. given #167 (F,wt=10): 986 B(b v d,x v (d v e),x). [para(876(a,1),495(a,1))]. given #168 (F,wt=10): 1014 B(d v e,b v d,a v c). [para(876(a,1),773(a,2))]. given #169 (T,wt=10): 1015 B(a v c,b v d,d v e). [para(876(a,1),823(a,2))]. given #170 (T,wt=10): 1061 B(x,b v (x v c),a v c). [para(49(a,1),786(a,2))]. given #171 (A,wt=15): 157 (x v (a v d)) ^ (x v (c v d)) = x v d. [para(57(a,1),37(a,1,2)),flip(a)]. given #172 (F,wt=8): 1194 B(a v d,d,c v d). [para(157(a,1),113(c,1)),rewrite(25(3),844(15),49(14),25(13),844(14),110(13),104(14)),xx(b),xx(c)]. given #173 (F,wt=10): 1066 B(a v c,b v (x v c),x). [para(25(a,1),800(a,2,2))]. given #174 (T,wt=10): 1110 B(x,c v (x v d),a v c). [para(49(a,1),900(a,2))]. given #175 (T,wt=10): 1115 B(a v c,c v (x v d),x). [para(25(a,1),911(a,2,2))]. given #176 (A,wt=17): 158 (a v d) ^ (c v (d v x)) = (a v d) ^ (d v x). [para(57(a,1),42(a,1,2,1)),rewrite(27(13)),flip(a)]. given #177 (F,wt=10): 1161 B(x,d v (x v e),b v d). [para(49(a,1),972(a,2))]. given #178 (F,wt=10): 1167 B(b v d,d v (x v e),x). [para(25(a,1),983(a,2,2))]. given #179 (T,wt=11): 238 e ^ (b v (x v (d v y))) = e. [para(49(a,1),141(a,1,2,2))]. given #180 (T,wt=11): 276 b ^ (a v (x v (y v c))) = b. [para(27(a,1),221(a,1,2,2))]. given #181 (A,wt=13): 159 (a v d) ^ (x ^ (c v d)) = x ^ d. [para(57(a,1),47(a,1,2)),flip(a)]. given #182 (F,wt=11): 288 d ^ (a v (x v (y v c))) = d. [para(27(a,1),227(a,1,2,2))]. given #183 (F,wt=11): 293 e ^ (b v (x v (y v d))) = e. [para(27(a,1),233(a,1,2,2))]. given #184 (T,wt=11): 298 b ^ (x v (y v (a v c))) = b. [para(27(a,1),279(a,1,2))]. given #185 (T,wt=11): 312 B(b,a v b,c) | a v b != b. [para(56(a,1),93(b,1)),rewrite(126(16),25(19),49(19),25(18),53(20)),flip(b),xx(c)]. given #186 (A,wt=13): 161 (b v e) ^ ((d v e) ^ x) = e ^ x. [para(58(a,1),26(a,1,1)),flip(a)]. given #187 (F,wt=11): 313 B(c,a v d,d) | a v d != d. [para(57(a,1),93(b,1)),rewrite(49(16),25(21),126(21),24(20),98(20)),flip(b),xx(c)]. given #188 (F,wt=11): 314 B(d,b v e,e) | b v e != e. [para(58(a,1),93(b,1)),rewrite(49(16),25(21),126(21),24(20),98(20)),flip(b),xx(c)]. given #189 (T,wt=11): 357 (x v y) ^ (z ^ y) = z ^ y. [para(122(a,1),95(a,2)),rewrite(186(4))]. given #190 (T,wt=11): 386 d ^ (x v (y v (a v c))) = d. [para(27(a,1),291(a,1,2))]. given #191 (A,wt=15): 162 (x v (b v e)) ^ (x v (d v e)) = x v e. [para(58(a,1),37(a,1,2)),flip(a)]. given #192 (F,wt=8): 1307 B(b v e,e,d v e). [para(162(a,1),113(c,1)),rewrite(25(3),876(15),49(14),25(13),876(14),111(13),104(14)),xx(b),xx(c)]. given #193 (F,wt=11): 391 e ^ (x v (y v (b v d))) = e. [para(27(a,1),296(a,1,2))]. given #194 (T,wt=11): 403 B(x,y,x v y) | y v x != y. [para(25(a,1),103(b,1))]. given #195 (T,wt=11): 567 B(x,y,y v x) | y v x != y. [para(50(a,1),116(c,1)),rewrite(126(4),29(4)),xx(b)]. given #196 (A,wt=17): 163 (b v e) ^ (d v (e v x)) = (b v e) ^ (e v x). [para(58(a,1),42(a,1,2,1)),rewrite(27(13)),flip(a)]. given #197 (F,wt=11): 611 B(x v y,x,y) | x v y != x. [para(29(a,1),118(c,1)),rewrite(25(4),126(4),29(4)),xx(b)]. given #198 (F,wt=11): 655 b ^ (x v (a v (c v y))) = b. [para(99(a,1),131(a,1,2)),rewrite(106(5),27(6)),flip(a)]. given #199 (T,wt=11): 656 (a v c) ^ (x ^ b) = x ^ b. [para(122(a,1),131(a,2)),rewrite(186(8))]. given #200 (T,wt=11): 661 d ^ (x v (a v (c v y))) = d. [para(99(a,1),135(a,1,2)),rewrite(110(5),27(6)),flip(a)]. given #201 (A,wt=13): 164 (b v e) ^ (x ^ (d v e)) = x ^ e. [para(58(a,1),47(a,1,2)),flip(a)]. given #202 (F,wt=11): 662 (a v c) ^ (x ^ d) = x ^ d. [para(122(a,1),135(a,2)),rewrite(186(8))]. given #203 (F,wt=11): 675 B(x,x v y,x) | x v y != x. [para(104(a,1),127(b,1,2)),rewrite(24(4),29(4)),flip(b)]. given #204 (T,wt=11): 680 e ^ (x v (b v (d v y))) = e. [para(99(a,1),139(a,1,2)),rewrite(111(5),27(6)),flip(a)]. given #205 (T,wt=11): 681 (b v d) ^ (x ^ e) = x ^ e. [para(122(a,1),139(a,2)),rewrite(186(8))]. given #206 (A,wt=13): 166 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(97(a,1),26(a,1,1)),flip(a)]. given #207 (F,wt=11): 725 B(x,y v x,x) | y v x != x. [para(104(a,1),130(b,1,2)),rewrite(24(4),50(4)),flip(b)]. given #208 (F,wt=11): 732 a ^ (c ^ (d v x)) = a ^ c. [para(284(a,1),187(a,1,2)),rewrite(247(4),24(9),26(9),51(8),284(11))]. given #209 (T,wt=11): 733 b ^ (d ^ (e v x)) = b ^ d. [para(285(a,1),187(a,1,2)),rewrite(247(4),24(9),26(9),51(8),285(11))]. given #210 (T,wt=11): 734 a ^ (c ^ (b v x)) = a ^ c. [para(433(a,1),187(a,1,2)),rewrite(247(4),24(9),26(9),65(8),433(11))]. given #211 (A,wt=15): 169 (x v y) ^ (x v (z v (u v y))) = x v y. [para(97(a,1),37(a,1,2)),flip(a)]. given #212 (F,wt=11): 763 (a v b) ^ (a v c) = a v b. [para(124(a,1),132(a,1,2))]. given #213 (F,wt=11): 764 (a v c) ^ (b v c) = b v c. [para(126(a,1),132(a,1,2)),rewrite(25(3),24(7),25(10))]. given #214 (T,wt=11): 845 (a v c) ^ (a v d) = a v d. [para(124(a,1),136(a,1,2)),rewrite(24(7))]. given #215 (T,wt=11): 846 (a v c) ^ (c v d) = c v d. [para(126(a,1),136(a,1,2)),rewrite(24(7))]. given #216 (A,wt=13): 171 x ^ (y ^ (z v (u v x))) = y ^ x. [para(97(a,1),47(a,1,2)),flip(a)]. given #217 (F,wt=11): 856 e ^ ((a v c) ^ x) = e ^ x. [para(849(a,1),26(a,1,1)),flip(a)]. given #218 (F,wt=11): 858 e ^ (x ^ (a v c)) = x ^ e. [para(849(a,1),47(a,1,2)),flip(a)]. given #219 (T,wt=11): 877 (b v d) ^ (b v e) = b v e. [para(124(a,1),140(a,1,2)),rewrite(24(7))]. given #220 (T,wt=11): 878 (b v d) ^ (d v e) = d v e. [para(126(a,1),140(a,1,2)),rewrite(24(7))]. given #221 (A,wt=15): 172 (x v y) ^ (z v (x v (u v y))) = x v y. [para(49(a,1),97(a,1,2,2))]. given #222 (F,wt=11): 960 e ^ (a v (x v (c v y))) = e. [para(49(a,1),860(a,1,2,2))]. given #223 (F,wt=11): 1039 e ^ (a v (x v (y v c))) = e. [para(27(a,1),956(a,1,2,2))]. given #224 (T,wt=11): 1046 e ^ (x v (y v (a v c))) = e. [para(27(a,1),1042(a,1,2))]. given #225 (T,wt=11): 1053 e ^ (x v (a v (c v y))) = e. [para(1042(a,1),187(a,1,2)),rewrite(27(5),27(4),24(7),1042(13))]. given #226 (A,wt=13): 173 (x v y) ^ (y v (x v z)) = y v x. [para(25(a,1),53(a,1,1))]. given #227 (F,wt=11): 1177 (a v c) ^ (b v d) = b v d. [hyper(33,a,1014,a),rewrite(25(7),49(7),25(6),49(6),25(5),876(6),126(5),25(10),49(10),25(9),49(9),25(8),844(9),49(8),762(8),24(7))]. given #228 (F,wt=11): 1234 b ^ (x v (a v (y v c))) = b. [para(49(a,1),276(a,1,2))]. given #229 (T,wt=11): 1242 d ^ (x v (a v (y v c))) = d. [para(49(a,1),288(a,1,2))]. given #230 (T,wt=11): 1249 e ^ (x v (b v (y v d))) = e. [para(49(a,1),293(a,1,2))]. given #231 (A,wt=13): 174 (x v y) ^ (y v (z v x)) = x v y. [para(25(a,1),53(a,1,2)),rewrite(27(3))]. given #232 (F,wt=9): 1553 b ^ (c v (x v a)) = b. [para(174(a,1),131(a,1,2)),rewrite(106(5)),flip(a)]. given #233 (F,wt=9): 1554 d ^ (c v (x v a)) = d. [para(174(a,1),135(a,1,2)),rewrite(110(5)),flip(a)]. given #234 (T,wt=9): 1555 e ^ (d v (x v b)) = e. [para(174(a,1),139(a,1,2)),rewrite(111(5)),flip(a)]. given #235 (T,wt=9): 1558 e ^ (c v (x v a)) = e. [para(174(a,1),856(a,1,2)),rewrite(849(5)),flip(a)]. given #236 (A,wt=19): 175 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(27(a,1),53(a,1,1)),rewrite(27(5),27(8))]. given #237 (F,wt=11): 1266 a ^ (c ^ (x v d)) = a ^ c. [para(284(a,1),357(a,1,2)),rewrite(37(4),24(9),26(9),95(8),284(11))]. given #238 (F,wt=11): 1267 b ^ (d ^ (x v e)) = b ^ d. [para(285(a,1),357(a,1,2)),rewrite(37(4),24(9),26(9),95(8),285(11))]. given #239 (T,wt=11): 1268 a ^ (c ^ (x v b)) = a ^ c. [para(433(a,1),357(a,1,2)),rewrite(37(4),24(9),26(9),105(8),24(5),433(11))]. given #240 (T,wt=11): 1278 e ^ (x v (a v (y v c))) = e. [para(956(a,1),357(a,1,2)),rewrite(24(7),956(13))]. given #241 (A,wt=17): 177 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(53(a,1),47(a,1,2)),flip(a)]. given #242 (F,wt=11): 1330 B(x,y,y v x) | x v y != y. [para(25(a,1),567(b,1))]. given #243 (F,wt=11): 1346 B(x v y,x,y) | y v x != x. [para(25(a,1),611(b,1))]. given #244 (T,wt=11): 1370 B(x,x v y,x) | y v x != x. [para(25(a,1),675(b,1))]. given #245 (T,wt=11): 1396 B(x,y v x,x) | x v y != x. [para(25(a,1),725(b,1))]. given #246 (A,wt=19): 178 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(49(a,1),53(a,1,1)),rewrite(27(4))]. given #247 (F,wt=11): 1454 (a v c) ^ (x ^ e) = x ^ e. [para(122(a,1),856(a,2)),rewrite(186(8))]. given #248 (F,wt=11): 1561 b ^ (c v (x v (y v a))) = b. [para(27(a,1),1553(a,1,2,2))]. given #249 (T,wt=11): 1566 b ^ (c v (x v (a v y))) = b. [para(1553(a,1),187(a,1,2)),rewrite(27(5),27(4),24(7),1553(13))]. given #250 (T,wt=11): 1567 b ^ (x v (c v (y v a))) = b. [para(1553(a,1),357(a,1,2)),rewrite(24(7),1553(13))]. given #251 (A,wt=15): 179 (x v y) ^ (x v (z v (y v u))) = x v y. [para(49(a,1),53(a,1,2,2))]. given #252 (F,wt=11): 1569 d ^ (c v (x v (y v a))) = d. [para(27(a,1),1554(a,1,2,2))]. given #253 (F,wt=11): 1574 d ^ (c v (x v (a v y))) = d. [para(1554(a,1),187(a,1,2)),rewrite(27(5),27(4),24(7),1554(13))]. given #254 (T,wt=11): 1575 d ^ (x v (c v (y v a))) = d. [para(1554(a,1),357(a,1,2)),rewrite(24(7),1554(13))]. given #255 (T,wt=11): 1577 e ^ (d v (x v (y v b))) = e. [para(27(a,1),1555(a,1,2,2))]. given #256 (A,wt=15): 181 (x v y) ^ (z v (x v (y v u))) = x v y. [para(27(a,1),99(a,1,2,2))]. given #257 (F,wt=11): 1582 e ^ (d v (x v (b v y))) = e. [para(1555(a,1),187(a,1,2)),rewrite(27(5),27(4),24(7),1555(13))]. given #258 (F,wt=11): 1583 e ^ (x v (d v (y v b))) = e. [para(1555(a,1),357(a,1,2)),rewrite(24(7),1555(13))]. given #259 (T,wt=11): 1585 e ^ (c v (x v (y v a))) = e. [para(27(a,1),1558(a,1,2,2))]. given #260 (T,wt=11): 1590 e ^ (c v (x v (a v y))) = e. [para(1558(a,1),187(a,1,2)),rewrite(27(5),27(4),24(7),1558(13))]. given #261 (A,wt=13): 182 x ^ (y ^ (z v (x v u))) = y ^ x. [para(99(a,1),47(a,1,2)),flip(a)]. given #262 (F,wt=11): 1591 e ^ (x v (c v (y v a))) = e. [para(1558(a,1),357(a,1,2)),rewrite(24(7),1558(13))]. given #263 (F,wt=12): 335 B(x,(x v y) ^ (x v z),y ^ z). [para(37(a,1),307(a,2))]. given #264 (T,wt=8): 1797 B(a,a v b,b ^ c). [para(763(a,1),335(a,2))]. given #265 (T,wt=8): 1798 B(a,a v d,c ^ d). [para(845(a,1),335(a,2))]. given #266 (A,wt=13): 184 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(120(a,1),26(a,2,2)),rewrite(47(3),26(2))]. given #267 (F,wt=8): 1799 B(b,b v e,d ^ e). [para(877(a,1),335(a,2))]. given #268 (F,wt=12): 338 B(x ^ y,(z v x) ^ (z v y),z). [para(37(a,1),333(a,2))]. given #269 (T,wt=8): 1822 B(b ^ c,a v b,a). [para(763(a,1),338(a,2))]. given #270 (T,wt=8): 1823 B(c ^ d,a v d,a). [para(845(a,1),338(a,2))]. given #271 (A,wt=13): 186 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(26(a,1),122(a,1,2)),rewrite(26(5))]. given #272 (F,wt=8): 1824 B(d ^ e,b v e,b). [para(877(a,1),338(a,2))]. given #273 (F,wt=12): 342 B(x v y,x v (y v z),z v u). [para(27(a,1),317(a,2))]. given #274 (T,wt=10): 1912 B(x v y,y v x,x v z). [para(126(a,1),342(a,2))]. given #275 (T,wt=10): 1913 B(a v b,a v c,c v x). [para(762(a,1),342(a,2))]. given #276 (A,wt=20): 188 B(x,y,z) | (z v x) ^ y != y | (x v y) ^ (y v z) != y. [back_rewrite(117),rewrite(187(5))]. given #277 (F,wt=6): 1994 B(c,b v c,a). [para(764(a,1),188(b,1)),rewrite(126(18),25(21),762(21),24(20),764(20)),xx(b),xx(c)]. given #278 (F,wt=6): 1995 B(c,a v d,a). [para(845(a,1),188(b,1)),rewrite(49(18),844(18),25(21),124(21),845(20)),xx(b),xx(c)]. given #279 (T,wt=6): 1996 B(c,c v d,a). [para(846(a,1),188(b,1)),rewrite(124(18),25(21),844(21),24(20),846(20)),xx(b),xx(c)]. given #280 (T,wt=6): 1998 B(d,b v e,b). [para(877(a,1),188(b,1)),rewrite(49(18),876(18),25(21),124(21),877(20)),xx(b),xx(c)]. given #281 (A,wt=13): 190 x v (y v (x v z)) = y v (x v z). [para(124(a,1),27(a,2,2)),rewrite(49(3),27(2))]. given #282 (F,wt=6): 1999 B(d,d v e,b). [para(878(a,1),188(b,1)),rewrite(124(18),25(21),876(21),24(20),878(20)),xx(b),xx(c)]. given #283 (F,wt=6): 2003 B(c,b v d,a). [para(1177(a,1),188(b,1)),rewrite(49(18),25(23),24(24),1188(24)),xx(b),xx(c)]. given #284 (T,wt=10): 1914 B(x v y,y v x,z v x). [para(25(a,1),1912(a,3))]. given #285 (T,wt=10): 1923 B(a v b,a v c,x v c). [para(25(a,1),1913(a,3))]. given #286 (A,wt=13): 218 x v (y v (z v x)) = y v (z v x). [para(27(a,1),126(a,1,2)),rewrite(27(5))]. given #287 (F,wt=11): 1943 B(b,b v c,a) | b v c != b. [para(56(a,1),188(b,1)),rewrite(124(16),25(19),762(19),24(18),764(18)),flip(b),xx(c)]. given #288 (F,wt=11): 1944 B(d,c v d,a) | c v d != d. [para(57(a,1),188(b,1)),rewrite(126(16),25(19),844(19),24(18),846(18)),flip(b),xx(c)]. given #289 (T,wt=11): 1945 B(e,d v e,b) | d v e != e. [para(58(a,1),188(b,1)),rewrite(126(16),25(19),876(19),24(18),878(18)),flip(b),xx(c)]. given #290 (T,wt=12): 343 B(x,x v (y v z),y v (z v u)). [para(27(a,1),317(a,3))]. given #291 (A,wt=13): 222 b ^ ((a v (c v x)) ^ y) = b ^ y. [para(133(a,1),26(a,1,1)),flip(a)]. given #292 (F,wt=10): 2127 B(x,x v (a v b),a v c). [para(762(a,1),343(a,3))]. given #293 (F,wt=10): 2134 B(x,a v (b v x),a v c). [para(25(a,1),2127(a,2)),rewrite(27(4))]. given #294 (T,wt=10): 2136 B(x,a v (x v b),a v c). [para(49(a,1),2127(a,2))]. given #295 (T,wt=12): 345 B(x,x v y,(y v z) ^ (y v u)). [para(37(a,1),317(a,3))]. given #296 (A,wt=15): 223 (x v b) ^ (x v (a v (c v y))) = x v b. [para(133(a,1),37(a,1,2)),flip(a)]. given #297 (F,wt=10): 2154 B(x,x v b,a v (c v y)). [hyper(127,b,223,a)]. given #298 (F,wt=10): 2170 B(x,b v x,a v (c v y)). [para(25(a,1),2154(a,2))]. given #299 (T,wt=10): 2171 B(x,x v b,a v (y v c)). [para(25(a,1),2154(a,3,2))]. given #300 (T,wt=10): 2176 B(x,x v b,c v (y v a)). [para(218(a,1),2154(a,3))]. given #301 (A,wt=13): 225 b ^ (x ^ (a v (c v y))) = x ^ b. [para(133(a,1),47(a,1,2)),flip(a)]. given #302 (F,wt=10): 2178 B(x,b v x,a v (y v c)). [para(25(a,1),2170(a,3,2))]. given #303 (F,wt=10): 2185 B(x,b v x,c v (y v a)). [para(218(a,1),2170(a,3))]. given #304 (T,wt=10): 2187 B(x,x v b,y v (a v c)). [para(49(a,1),2171(a,3))]. given #305 (T,wt=10): 2194 B(x,b v x,y v (a v c)). [para(49(a,1),2178(a,3))]. given #306 (A,wt=13): 228 d ^ ((a v (c v x)) ^ y) = d ^ y. [para(137(a,1),26(a,1,1)),flip(a)]. given #307 (F,wt=12): 346 B(x,y v (x v z),y v (z v u)). [para(49(a,1),317(a,2)),rewrite(27(4))]. given #308 (F,wt=10): 2221 B(b,a v c,a v (c v x)). [para(762(a,1),346(a,2))]. given #309 (T,wt=10): 2225 B(b,a v c,a v (x v c)). [para(25(a,1),2221(a,3,2))]. given #310 (T,wt=10): 2229 B(b,a v c,c v (x v a)). [para(218(a,1),2221(a,3))]. given #311 (A,wt=15): 229 (x v d) ^ (x v (a v (c v y))) = x v d. [para(137(a,1),37(a,1,2)),flip(a)]. given #312 (F,wt=10): 2230 B(b,a v c,x v (a v c)). [para(49(a,1),2225(a,3))]. given #313 (F,wt=10): 2232 B(x,x v d,a v (c v y)). [hyper(127,b,229,a)]. given #314 (T,wt=10): 2249 B(x,d v x,a v (c v y)). [para(25(a,1),2232(a,2))]. given #315 (T,wt=10): 2250 B(x,x v d,a v (y v c)). [para(25(a,1),2232(a,3,2))]. given #316 (A,wt=13): 231 d ^ (x ^ (a v (c v y))) = x ^ d. [para(137(a,1),47(a,1,2)),flip(a)]. given #317 (F,wt=10): 2255 B(x,x v d,c v (y v a)). [para(218(a,1),2232(a,3))]. given #318 (F,wt=10): 2257 B(x,d v x,a v (y v c)). [para(25(a,1),2249(a,3,2))]. given #319 (T,wt=10): 2263 B(x,d v x,c v (y v a)). [para(218(a,1),2249(a,3))]. given #320 (T,wt=10): 2265 B(x,x v d,y v (a v c)). [para(49(a,1),2250(a,3))]. given #321 (A,wt=13): 234 e ^ ((b v (d v x)) ^ y) = e ^ y. [para(141(a,1),26(a,1,1)),flip(a)]. given #322 (F,wt=10): 2272 B(x,d v x,y v (a v c)). [para(49(a,1),2257(a,3))]. given #323 (F,wt=12): 349 B(x,y v (z v x),y v (z v u)). [para(27(a,1),340(a,2)),rewrite(27(4))]. given #324 (T,wt=10): 2297 B(d,a v c,a v (c v x)). [para(844(a,1),349(a,2))]. given #325 (T,wt=10): 2299 B(e,b v d,b v (d v x)). [para(876(a,1),349(a,2))]. given #326 (A,wt=15): 235 (x v e) ^ (x v (b v (d v y))) = x v e. [para(141(a,1),37(a,1,2)),flip(a)]. given #327 (F,wt=10): 2301 B(d,a v c,a v (x v c)). [para(25(a,1),2297(a,3,2))]. given #328 (F,wt=10): 2305 B(d,a v c,c v (x v a)). [para(218(a,1),2297(a,3))]. given #329 (T,wt=10): 2306 B(e,b v d,b v (x v d)). [para(25(a,1),2299(a,3,2))]. given #330 (T,wt=10): 2310 B(e,b v d,d v (x v b)). [para(218(a,1),2299(a,3))]. given #331 (A,wt=13): 237 e ^ (x ^ (b v (d v y))) = x ^ e. [para(141(a,1),47(a,1,2)),flip(a)]. given #332 (F,wt=10): 2311 B(x,x v e,b v (d v y)). [hyper(127,b,235,a)]. given #333 (F,wt=10): 2327 B(d,a v c,x v (a v c)). [para(49(a,1),2301(a,3))]. given #334 (T,wt=10): 2329 B(e,b v d,x v (b v d)). [para(49(a,1),2306(a,3))]. given #335 (T,wt=10): 2332 B(x,e v x,b v (d v y)). [para(25(a,1),2311(a,2))]. given #336 (A,wt=13): 247 (x ^ y) v z = (x v z) ^ (y v z). [para(104(a,1),55(a,2)),rewrite(25(3),245(3),25(4),246(4),25(4),37(4),126(2),126(3)),flip(a)]. given #337 (F,wt=10): 2333 B(x,x v e,b v (y v d)). [para(25(a,1),2311(a,3,2))]. given #338 (F,wt=10): 2338 B(x,x v e,d v (y v b)). [para(218(a,1),2311(a,3))]. given #339 (T,wt=10): 2342 B(x,e v x,b v (y v d)). [para(25(a,1),2332(a,3,2))]. given #340 (T,wt=10): 2348 B(x,e v x,d v (y v b)). [para(218(a,1),2332(a,3))]. given #341 (A,wt=46): 256 B(x,(x v y) ^ (z v y),u) | (x v y) ^ ((x v u) ^ (z v y)) != (x v y) ^ (z v y) | (x v y) ^ (z v (y v u)) != (x v y) ^ (z v y). [back_rewrite(128),rewrite(247(2),247(6),247(10),27(10),26(12),177(11),247(11),247(15),37(17),124(15),98(17),247(17),144(20),247(19))]. given #342 (F,wt=6): 2710 B(a,b v c,c). [para(764(a,1),256(b,1,2)),rewrite(764(8),764(13),764(16),104(20),764(20),764(23)),xx(b),xx(c)]. given #343 (F,wt=6): 2712 B(a,a v d,c). [para(845(a,1),256(b,1,2)),rewrite(100(8),100(13),100(16),25(20),844(21),24(20),845(20),100(23)),xx(b),xx(c)]. given #344 (T,wt=6): 2713 B(b,b v e,d). [para(877(a,1),256(b,1,2)),rewrite(100(8),100(13),100(16),25(20),876(21),24(20),877(20),100(23)),xx(b),xx(c)]. given #345 (T,wt=10): 2621 B(x,x v e,y v (b v d)). [para(49(a,1),2333(a,3))]. given #346 (A,wt=27): 259 (x v y) ^ ((z v y) ^ ((y v (u v x)) ^ (y v (u v z)))) = (x v y) ^ (z v y). [back_rewrite(209),rewrite(247(2),26(9),247(11))]. given #347 (F,wt=10): 2631 B(x,e v x,y v (b v d)). [para(49(a,1),2342(a,3))]. given #348 (F,wt=10): 2670 B(x,(x v y) ^ (z v y),y). [para(104(a,1),256(c,1,2,2)),rewrite(120(9)),xx(b),xx(c)]. given #349 (T,wt=10): 2714 B(a,(a v d) ^ (b v d),c). [para(1177(a,1),256(b,1,2)),rewrite(25(32),2355(34)),xx(b),xx(c)]. given #350 (T,wt=10): 2802 B(x,(y v z) ^ (x v z),z). [para(24(a,1),2670(a,2))]. given #351 (A,wt=36): 262 B(x,y ^ z,u) | y ^ (z ^ (x v u)) != y ^ z | (x v y) ^ ((x v z) ^ ((y v u) ^ (z v u))) != y ^ z. [back_rewrite(150),rewrite(247(11))]. given #352 (F,wt=6): 2869 B(x,x ^ y,y). [para(120(a,1),262(c,1,2)),rewrite(50(4),104(6),104(7),24(7),50(7)),xx(b),xx(c)]. given #353 (F,wt=6): 3132 B(x,y ^ x,y). [para(24(a,1),2869(a,2))]. given #354 (T,wt=8): 3136 B(a,a ^ b,b v c). [para(155(a,1),2869(a,2))]. given #355 (T,wt=8): 3137 B(a,a ^ d,c v d). [para(160(a,1),2869(a,2))]. given #356 (A,wt=30): 265 B(x,y,z ^ u) | (x v z) ^ (y ^ (x v u)) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [back_rewrite(112),rewrite(247(4),247(7),26(9),146(10),65(7))]. given #357 (F,wt=8): 3138 B(b,b ^ e,d v e). [para(165(a,1),2869(a,2))]. given #358 (F,wt=8): 3140 B(c,c ^ d,a v d). [para(282(a,1),2869(a,2))]. given #359 (T,wt=8): 3142 B(d,d ^ e,b v e). [para(283(a,1),2869(a,2))]. given #360 (T,wt=8): 3143 B(a,a ^ c,c ^ d). [para(284(a,1),2869(a,2))]. given #361 (A,wt=13): 266 a ^ ((b v c) ^ x) = a ^ (b ^ x). [para(155(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #362 (F,wt=8): 3144 B(b,b ^ d,d ^ e). [para(285(a,1),2869(a,2))]. given #363 (F,wt=8): 3146 B(c,b ^ c,a v b). [para(432(a,1),2869(a,2))]. given #364 (T,wt=8): 3147 B(a,a ^ c,b ^ c). [para(433(a,1),2869(a,2))]. given #365 (T,wt=8): 3192 B(b v c,b,a v b). [para(56(a,1),3132(a,2))]. given #366 (A,wt=17): 267 (x v a) ^ (x v (b v c)) = (x v a) ^ (x v b). [para(155(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #367 (F,wt=8): 3193 B(c v d,d,a v d). [para(57(a,1),3132(a,2))]. given #368 (F,wt=8): 3194 B(d v e,e,b v e). [para(58(a,1),3132(a,2))]. given #369 (T,wt=8): 3195 B(b v c,a ^ b,a). [para(155(a,1),3132(a,2))]. given #370 (T,wt=8): 3196 B(c v d,a ^ d,a). [para(160(a,1),3132(a,2))]. given #371 (A,wt=13): 268 a ^ (x ^ (b v c)) = x ^ (a ^ b). [para(155(a,1),47(a,1,2)),flip(a)]. given #372 (F,wt=8): 3197 B(d v e,b ^ e,b). [para(165(a,1),3132(a,2))]. given #373 (F,wt=8): 3199 B(a v d,c ^ d,c). [para(282(a,1),3132(a,2))]. given #374 (T,wt=8): 3201 B(b v e,d ^ e,d). [para(283(a,1),3132(a,2))]. given #375 (T,wt=8): 3202 B(c ^ d,a ^ c,a). [para(284(a,1),3132(a,2))]. given #376 (A,wt=13): 269 a ^ ((c v d) ^ x) = a ^ (d ^ x). [para(160(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #377 (F,wt=8): 3203 B(d ^ e,b ^ d,b). [para(285(a,1),3132(a,2))]. given #378 (F,wt=8): 3205 B(a v b,b ^ c,c). [para(432(a,1),3132(a,2))]. given #379 (T,wt=8): 3206 B(b ^ c,a ^ c,a). [para(433(a,1),3132(a,2))]. given #380 (T,wt=10): 2803 B(x,(y v x) ^ (z v y),y). [para(25(a,1),2670(a,2,1))]. given #381 (A,wt=17): 270 (x v a) ^ (x v (c v d)) = (x v a) ^ (x v d). [para(160(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #382 (F,wt=10): 2804 B(x,(x v y) ^ (y v z),y). [para(25(a,1),2670(a,2,2))]. given #383 (F,wt=6): 3525 B(a,c v d,c). [para(846(a,1),2804(a,2))]. given #384 (T,wt=6): 3526 B(b,d v e,d). [para(878(a,1),2804(a,2))]. given #385 (T,wt=10): 2818 B(x,(y v z) ^ (x v y),y). [para(25(a,1),2802(a,2,1))]. given #386 (A,wt=13): 271 a ^ (x ^ (c v d)) = x ^ (a ^ d). [para(160(a,1),47(a,1,2)),flip(a)]. given #387 (F,wt=10): 2819 B(x,(y v z) ^ (z v x),z). [para(25(a,1),2802(a,2,2))]. given #388 (F,wt=10): 3133 B(x ^ y,x ^ (y ^ z),z). [para(26(a,1),2869(a,2))]. given #389 (T,wt=8): 3568 B(x ^ y,y ^ x,x). [para(122(a,1),3133(a,2))]. given #390 (T,wt=8): 3582 B(a ^ b,a ^ c,c). [para(433(a,1),3133(a,2))]. given #391 (A,wt=13): 272 b ^ ((d v e) ^ x) = b ^ (e ^ x). [para(165(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #392 (F,wt=10): 3134 B(x,y ^ (x ^ z),y ^ z). [para(47(a,1),2869(a,2))]. given #393 (F,wt=8): 3701 B(c,a ^ c,a ^ d). [para(284(a,1),3134(a,2))]. given #394 (T,wt=8): 3704 B(d,b ^ d,b ^ e). [para(285(a,1),3134(a,2))]. given #395 (T,wt=10): 3135 B(x,x ^ y,(x v z) ^ y). [para(51(a,1),2869(a,2))]. given #396 (A,wt=17): 273 (x v b) ^ (x v (d v e)) = (x v b) ^ (x v e). [para(165(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #397 (F,wt=10): 3139 B(x,x ^ y,y ^ (x v z)). [para(65(a,1),2869(a,2))]. given #398 (F,wt=8): 3937 B(x,x ^ y,y ^ x). [para(104(a,1),3139(a,3,2))]. given #399 (T,wt=10): 3141 B(x,x ^ y,(z v x) ^ y). [para(95(a,1),2869(a,2))]. given #400 (T,wt=10): 3145 B(x,y ^ x,y ^ (z v x)). [para(105(a,1),2869(a,2))]. given #401 (A,wt=13): 274 b ^ (x ^ (d v e)) = x ^ (b ^ e). [para(165(a,1),47(a,1,2)),flip(a)]. given #402 (F,wt=8): 4087 B(c,a ^ c,a ^ b). [para(155(a,1),3145(a,3))]. given #403 (F,wt=10): 3148 B(b,b ^ x,(a v c) ^ x). [para(131(a,1),2869(a,2))]. given #404 (T,wt=10): 3149 B(b,x ^ b,x ^ (a v c)). [para(134(a,1),2869(a,2))]. given #405 (T,wt=10): 3150 B(d,d ^ x,(a v c) ^ x). [para(135(a,1),2869(a,2))]. given #406 (A,wt=13): 275 b ^ ((a v (x v c)) ^ y) = b ^ y. [para(221(a,1),26(a,1,1)),flip(a)]. given #407 (F,wt=10): 3151 B(d,x ^ d,x ^ (a v c)). [para(138(a,1),2869(a,2))]. given #408 (F,wt=10): 3152 B(e,e ^ x,(b v d) ^ x). [para(139(a,1),2869(a,2))]. given #409 (T,wt=10): 3153 B(e,x ^ e,x ^ (b v d)). [para(142(a,1),2869(a,2))]. given #410 (T,wt=10): 3170 B(a,a ^ c,c ^ (d v x)). [para(732(a,1),2869(a,2))]. given #411 (A,wt=15): 277 (x v b) ^ (x v (a v (y v c))) = x v b. [para(221(a,1),37(a,1,2)),flip(a)]. given #412 (F,wt=10): 3171 B(b,b ^ d,d ^ (e v x)). [para(733(a,1),2869(a,2))]. given #413 (F,wt=10): 3172 B(a,a ^ c,c ^ (b v x)). [para(734(a,1),2869(a,2))]. given #414 (T,wt=10): 3174 B(e,e ^ x,(a v c) ^ x). [para(856(a,1),2869(a,2))]. given #415 (T,wt=10): 3175 B(e,x ^ e,x ^ (a v c)). [para(858(a,1),2869(a,2))]. given #416 (A,wt=13): 278 b ^ (x ^ (a v (y v c))) = x ^ b. [para(221(a,1),47(a,1,2)),flip(a)]. given #417 (F,wt=10): 3176 B(a,a ^ c,c ^ (x v d)). [para(1266(a,1),2869(a,2))]. given #418 (F,wt=10): 3177 B(b,b ^ d,d ^ (x v e)). [para(1267(a,1),2869(a,2))]. given #419 (T,wt=10): 3178 B(a,a ^ c,c ^ (x v b)). [para(1268(a,1),2869(a,2))]. given #420 (T,wt=10): 3189 B(x,y ^ (z ^ x),y ^ z). [para(26(a,1),3132(a,2))]. given #421 (A,wt=15): 281 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(26(a,1),65(a,1,2))]. given #422 (F,wt=8): 4317 B(x,y ^ x,x ^ y). [para(122(a,1),3189(a,2))]. given #423 (F,wt=10): 3190 B(x ^ y,x ^ (z ^ y),z). [para(47(a,1),3132(a,2))]. given #424 (T,wt=8): 4464 B(a ^ d,a ^ c,c). [para(284(a,1),3190(a,2))]. given #425 (T,wt=8): 4467 B(b ^ e,b ^ d,d). [para(285(a,1),3190(a,2))]. given #426 (A,wt=30): 286 B(x ^ y,z,u) | z ^ ((x v u) ^ (y v u)) != z | (x v z) ^ ((y v z) ^ (z v u)) != z. [back_rewrite(264),rewrite(281(8))]. given #427 (F,wt=8): 4626 B(x ^ y,y,y v z). [para(53(a,1),286(c,1,2)),rewrite(124(7),24(7),50(7),29(5),104(6),24(6),50(6)),xx(b),xx(c)]. given #428 (F,wt=8): 4640 B(x ^ y,y,z v y). [para(98(a,1),286(c,1,2)),rewrite(126(7),24(7),50(7),50(5),104(6),24(6),50(6)),xx(b),xx(c)]. given #429 (T,wt=8): 4651 B(x ^ b,b,a v c). [para(132(a,1),286(c,1,2)),rewrite(49(17),762(17),24(16),50(16),106(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #430 (T,wt=8): 4657 B(x ^ d,d,a v c). [para(136(a,1),286(c,1,2)),rewrite(49(17),25(16),844(17),24(16),50(16),110(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #431 (A,wt=13): 287 d ^ ((a v (x v c)) ^ y) = d ^ y. [para(227(a,1),26(a,1,1)),flip(a)]. given #432 (F,wt=8): 4658 B(x ^ e,e,b v d). [para(140(a,1),286(c,1,2)),rewrite(49(17),25(16),876(17),24(16),50(16),111(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #433 (F,wt=8): 4693 B(x ^ y,x,x v z). [para(177(a,1),286(c,1)),rewrite(124(5),50(7),29(5),104(6),24(6),50(6)),xx(b),xx(c)]. given #434 (T,wt=8): 4851 B(x ^ y,x,z v x). [para(24(a,1),4640(a,1))]. given #435 (T,wt=8): 4983 B(b ^ x,b,a v c). [para(24(a,1),4651(a,1))]. given #436 (A,wt=15): 289 (x v d) ^ (x v (a v (y v c))) = x v d. [para(227(a,1),37(a,1,2)),flip(a)]. given #437 (F,wt=8): 4985 B(d ^ x,d,a v c). [para(24(a,1),4657(a,1))]. given #438 (F,wt=8): 5014 B(e ^ x,e,b v d). [para(24(a,1),4658(a,1))]. given #439 (T,wt=10): 3191 B((x v y) ^ z,x ^ z,x). [para(51(a,1),3132(a,2))]. given #440 (T,wt=10): 3198 B(x ^ (y v z),y ^ x,y). [para(65(a,1),3132(a,2))]. given #441 (A,wt=13): 290 d ^ (x ^ (a v (y v c))) = x ^ d. [para(227(a,1),47(a,1,2)),flip(a)]. given #442 (F,wt=8): 5178 B(x ^ y,y ^ x,y). [para(104(a,1),3198(a,1,2))]. given #443 (F,wt=10): 3200 B((x v y) ^ z,y ^ z,y). [para(95(a,1),3132(a,2))]. given #444 (T,wt=10): 3204 B(x ^ (y v z),x ^ z,z). [para(105(a,1),3132(a,2))]. given #445 (T,wt=10): 3207 B((a v c) ^ x,b ^ x,b). [para(131(a,1),3132(a,2))]. given #446 (A,wt=13): 292 e ^ ((b v (x v d)) ^ y) = e ^ y. [para(233(a,1),26(a,1,1)),flip(a)]. given #447 (F,wt=10): 3208 B(x ^ (a v c),x ^ b,b). [para(134(a,1),3132(a,2))]. given #448 (F,wt=10): 3209 B((a v c) ^ x,d ^ x,d). [para(135(a,1),3132(a,2))]. given #449 (T,wt=10): 3210 B(x ^ (a v c),x ^ d,d). [para(138(a,1),3132(a,2))]. given #450 (T,wt=10): 3211 B((b v d) ^ x,e ^ x,e). [para(139(a,1),3132(a,2))]. given #451 (A,wt=15): 294 (x v e) ^ (x v (b v (y v d))) = x v e. [para(233(a,1),37(a,1,2)),flip(a)]. given #452 (F,wt=10): 3212 B(x ^ (b v d),x ^ e,e). [para(142(a,1),3132(a,2))]. given #453 (F,wt=10): 3229 B(c ^ (d v x),a ^ c,a). [para(732(a,1),3132(a,2))]. given #454 (T,wt=10): 3230 B(d ^ (e v x),b ^ d,b). [para(733(a,1),3132(a,2))]. given #455 (T,wt=10): 3231 B(c ^ (b v x),a ^ c,a). [para(734(a,1),3132(a,2))]. given #456 (A,wt=13): 295 e ^ (x ^ (b v (y v d))) = x ^ e. [para(233(a,1),47(a,1,2)),flip(a)]. given #457 (F,wt=10): 3233 B((a v c) ^ x,e ^ x,e). [para(856(a,1),3132(a,2))]. given #458 (F,wt=10): 3234 B(x ^ (a v c),x ^ e,e). [para(858(a,1),3132(a,2))]. given #459 (T,wt=10): 3236 B(c ^ (x v d),a ^ c,a). [para(1266(a,1),3132(a,2))]. given #460 (T,wt=10): 3237 B(d ^ (x v e),b ^ d,b). [para(1267(a,1),3132(a,2))]. given #461 (A,wt=13): 297 b ^ ((x v (a v c)) ^ y) = b ^ y. [para(279(a,1),26(a,1,1)),flip(a)]. given #462 (F,wt=10): 3238 B(c ^ (x v b),a ^ c,a). [para(1268(a,1),3132(a,2))]. given #463 (F,wt=10): 3472 B(x,(y v x) ^ (y v z),y). [para(25(a,1),2803(a,2,2))]. given #464 (T,wt=10): 3528 B(x,(y v z) ^ (y v x),y). [para(25(a,1),2818(a,2,2))]. given #465 (T,wt=6): 5637 B(c,a v b,a). [para(763(a,1),3528(a,2))]. given #466 (A,wt=15): 299 (x v b) ^ (x v (y v (a v c))) = x v b. [para(279(a,1),37(a,1,2)),flip(a)]. given #467 (F,wt=10): 3557 B(x ^ y,y ^ (x ^ z),z). [para(24(a,1),3133(a,1))]. given #468 (F,wt=10): 3558 B(x ^ y,y ^ (z ^ x),z). [para(24(a,1),3133(a,2)),rewrite(26(3))]. given #469 (T,wt=10): 3579 B(x ^ y,y ^ x,z v x). [para(105(a,1),3133(a,2))]. given #470 (T,wt=10): 3585 B(b ^ x,x ^ b,a v c). [para(134(a,1),3133(a,2))]. given #471 (A,wt=13): 300 b ^ (x ^ (y v (a v c))) = x ^ b. [para(279(a,1),47(a,1,2)),flip(a)]. given #472 (F,wt=10): 3588 B(d ^ x,x ^ d,a v c). [para(138(a,1),3133(a,2))]. given #473 (F,wt=10): 3591 B(e ^ x,x ^ e,b v d). [para(142(a,1),3133(a,2))]. given #474 (T,wt=10): 3593 B((x v y) ^ z,z ^ x,x). [para(187(a,1),3133(a,2))]. given #475 (T,wt=10): 3610 B((x v y) ^ z,z ^ y,y). [para(357(a,1),3133(a,2))]. given #476 (A,wt=13): 301 c ^ ((a v d) ^ x) = c ^ (d ^ x). [para(282(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #477 (F,wt=10): 3614 B((a v c) ^ x,x ^ b,b). [para(656(a,1),3133(a,2))]. given #478 (F,wt=10): 3618 B((a v c) ^ x,x ^ d,d). [para(662(a,1),3133(a,2))]. given #479 (T,wt=10): 3620 B((b v d) ^ x,x ^ e,e). [para(681(a,1),3133(a,2))]. given #480 (T,wt=10): 3632 B(e ^ x,x ^ e,a v c). [para(858(a,1),3133(a,2))]. given #481 (A,wt=17): 302 (x v c) ^ (x v (a v d)) = (x v c) ^ (x v d). [para(282(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #482 (F,wt=10): 3644 B((a v c) ^ x,x ^ e,e). [para(1454(a,1),3133(a,2))]. given #483 (F,wt=10): 3685 B(x,x ^ (y ^ z),z ^ y). [para(24(a,1),3134(a,2)),rewrite(26(2))]. given #484 (T,wt=10): 3686 B(x,y ^ (x ^ z),z ^ y). [para(24(a,1),3134(a,3))]. given #485 (T,wt=10): 3689 B(x,y ^ x,y ^ (x v z)). [para(29(a,1),3134(a,2,2))]. given #486 (A,wt=13): 303 c ^ (x ^ (a v d)) = x ^ (c ^ d). [para(282(a,1),47(a,1,2)),flip(a)]. given #487 (F,wt=10): 3719 B(x,x ^ (y v z),z v y). [para(219(a,1),3134(a,3)),rewrite(1803(4))]. given #488 (F,wt=10): 3758 B(c,a ^ c,a ^ (d v x)). [para(732(a,1),3134(a,2))]. given #489 (T,wt=10): 3760 B(d,b ^ d,b ^ (e v x)). [para(733(a,1),3134(a,2))]. given #490 (T,wt=10): 3762 B(c,a ^ c,a ^ (b v x)). [para(734(a,1),3134(a,2))]. given #491 (A,wt=20): 304 B(x,y,z) | (x v z) ^ y != y | (x v y) ^ (y v z) != y. [para(24(a,1),93(b,1))]. given #492 (F,wt=6): 6642 B(a,b v d,c). [para(1177(a,1),304(b,1)),rewrite(25(23),49(23),1188(24)),xx(b),xx(c)]. given #493 (F,wt=10): 3785 B(c,a ^ c,a ^ (x v d)). [para(1266(a,1),3134(a,2))]. given #494 (T,wt=10): 3787 B(d,b ^ d,b ^ (x v e)). [para(1267(a,1),3134(a,2))]. given #495 (T,wt=10): 3789 B(c,a ^ c,a ^ (x v b)). [para(1268(a,1),3134(a,2))]. given #496 (A,wt=20): 305 B(x,y,z) | y ^ (z v x) != y | (x v y) ^ (y v z) != y. [para(25(a,1),93(b,1,2))]. given #497 (F,wt=4): 6656 B(c,b,a). [para(106(a,1),305(b,1)),rewrite(25(10),25(13),24(14),56(14)),xx(b),xx(c)]. given #498 (F,wt=4): 6657 B(c,d,a). [para(110(a,1),305(b,1)),rewrite(25(13),24(14),57(14)),xx(b),xx(c)]. given #499 (T,wt=4): 6658 B(d,e,b). [para(111(a,1),305(b,1)),rewrite(25(13),24(14),58(14)),xx(b),xx(c)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 95 (0.00 of 1.12 sec). given #500 (T,wt=10): 3829 B(x,y ^ x,(x v z) ^ y). [para(24(a,1),3135(a,2))]. given #501 (A,wt=30): 306 B(x,y,z ^ u) | y ^ ((x v z) ^ (x v u)) != y | (x v y) ^ ((y v z) ^ (y v u)) != y. [para(37(a,1),93(b,1,2)),rewrite(37(10))]. given #502 (F,wt=10): 3932 B(x,x ^ y,y ^ (z v x)). [para(25(a,1),3139(a,3,2))]. given #503 (F,wt=10): 4001 B(x,y ^ x,(z v x) ^ y). [para(24(a,1),3141(a,2))]. given #504 (T,wt=10): 4172 B(b,x ^ b,(a v c) ^ x). [para(24(a,1),3148(a,2))]. given #505 (T,wt=10): 4173 B(b,b ^ x,x ^ (a v c)). [para(24(a,1),3148(a,3))]. given #506 (A,wt=26): 308 B(x,y,z v u) | y ^ (z v (x v u)) != y | (x v y) ^ (y v (z v u)) != y. [para(49(a,1),93(b,1,2))]. given #507 (F,wt=8): 6901 B(x,y v z,z v y). [para(174(a,1),308(b,1)),rewrite(49(11),25(10),124(10),126(10),24(10),50(10)),xx(b),xx(c)]. given #508 (F,wt=10): 4188 B(d,x ^ d,(a v c) ^ x). [para(24(a,1),3150(a,2))]. given #509 (T,wt=10): 4189 B(d,d ^ x,x ^ (a v c)). [para(24(a,1),3150(a,3))]. given #510 (T,wt=10): 4223 B(e,x ^ e,(b v d) ^ x). [para(24(a,1),3152(a,2))]. given #511 (A,wt=32): 309 B(x,y v z,u) | (y v z) ^ (x v u) != y v z | (y v (x v z)) ^ (y v (z v u)) != y v z. [para(49(a,1),93(c,1,1)),rewrite(27(11))]. given #512 (F,wt=10): 4224 B(e,e ^ x,x ^ (b v d)). [para(24(a,1),3152(a,3))]. given #513 (F,wt=10): 4278 B(e,x ^ e,(a v c) ^ x). [para(24(a,1),3174(a,2))]. given #514 (T,wt=10): 4279 B(e,e ^ x,x ^ (a v c)). [para(24(a,1),3174(a,3))]. given #515 (T,wt=10): 4307 B(x,y ^ (z ^ x),z ^ y). [para(24(a,1),3189(a,3))]. given #516 (A,wt=26): 310 B(x,y,z v u) | y ^ (x v (z v u)) != y | (x v y) ^ (z v (y v u)) != y. [para(49(a,1),93(c,1,2))]. given #517 (F,wt=10): 4328 B(x v y,z ^ y,y ^ z). [para(105(a,1),3189(a,2))]. given #518 (F,wt=10): 4333 B(a v c,x ^ b,b ^ x). [para(134(a,1),3189(a,2))]. given #519 (T,wt=10): 4336 B(a v c,x ^ d,d ^ x). [para(138(a,1),3189(a,2))]. given #520 (T,wt=10): 4339 B(b v d,x ^ e,e ^ x). [para(142(a,1),3189(a,2))]. given #521 (A,wt=14): 311 B(x,y,x) | y ^ x != y | x v y != y. [para(104(a,1),93(b,1,2)),rewrite(219(6))]. given #522 (F,wt=10): 4373 B(a v c,x ^ e,e ^ x). [para(858(a,1),3189(a,2))]. given #523 (F,wt=10): 4451 B(x ^ y,z ^ (y ^ x),z). [para(24(a,1),3190(a,2)),rewrite(26(3))]. given #524 (T,wt=10): 4454 B(x ^ (y v z),x ^ y,y). [para(29(a,1),3190(a,2,2))]. given #525 (T,wt=10): 4481 B(x v y,z ^ (y v x),z). [para(219(a,1),3190(a,1)),rewrite(1803(5))]. given #526 (A,wt=15): 315 B(x,y,z v y) | (x v y) ^ (z v y) != y. [para(97(a,1),93(b,1)),rewrite(126(6)),xx(b)]. given #527 (F,wt=6): 7256 B(b,e,d v e). [hyper(315,b,58,a)]. given #528 (F,wt=6): 7257 B(a,d,c v d). [hyper(315,b,57,a)]. given #529 (T,wt=10): 4521 B(a ^ (d v x),a ^ c,c). [para(732(a,1),3190(a,2))]. given #530 (T,wt=10): 4523 B(b ^ (e v x),b ^ d,d). [para(733(a,1),3190(a,2))]. given #531 (A,wt=13): 316 B(x,y,z v (x v y)) | x v y != y. [para(97(a,1),93(c,1)),rewrite(190(6),97(6)),xx(b)]. given #532 (F,wt=10): 4525 B(a ^ (b v x),a ^ c,c). [para(734(a,1),3190(a,2))]. given #533 (F,wt=10): 4548 B(a ^ (x v d),a ^ c,c). [para(1266(a,1),3190(a,2))]. given #534 (T,wt=10): 4550 B(b ^ (x v e),b ^ d,d). [para(1267(a,1),3190(a,2))]. given #535 (T,wt=10): 4552 B(a ^ (x v b),a ^ c,c). [para(1268(a,1),3190(a,2))]. given #536 (A,wt=15): 318 B(x,y,y v z) | (x v y) ^ (y v z) != y. [para(99(a,1),93(b,1)),rewrite(124(6)),xx(b)]. given #537 (F,wt=6): 7286 B(a,b,b v c). [hyper(318,b,56,a)]. given #538 (F,wt=10): 4683 B(x ^ y,y,z v (u v y)). [para(169(a,1),286(c,1,2)),rewrite(218(10),24(10),50(10),97(7),104(7),24(7),50(7)),xx(b),xx(c)]. given #539 (T,wt=10): 4694 B(x ^ y,y,z v (y v u)). [para(179(a,1),286(c,1,2)),rewrite(190(10),24(10),50(10),99(7),104(7),24(7),50(7)),xx(b),xx(c)]. given #540 (T,wt=10): 4707 B(x ^ b,b,a v (c v y)). [para(223(a,1),286(c,1,2)),rewrite(49(20),777(20),24(19),50(19),133(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #541 (A,wt=13): 319 B(x,y,x v (y v z)) | x v y != y. [para(99(a,1),93(c,1)),rewrite(27(2),27(5),124(6),99(6)),xx(b)]. given #542 (F,wt=10): 4709 B(x ^ d,d,a v (c v y)). [para(229(a,1),286(c,1,2)),rewrite(49(20),49(19),891(20),24(19),50(19),137(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #543 (F,wt=10): 4712 B(x ^ e,e,b v (d v y)). [para(235(a,1),286(c,1,2)),rewrite(49(20),49(19),963(20),24(19),50(19),141(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #544 (T,wt=10): 4725 B(x ^ b,b,a v (y v c)). [para(277(a,1),286(c,1,2)),rewrite(49(20),4248(20),24(19),50(19),221(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #545 (T,wt=10): 4727 B(x ^ (y ^ z),z,z v u). [para(26(a,1),4626(a,1))]. given #546 (A,wt=18): 320 B(x,y,x v z) | y ^ (x v z) != y | y v x != y. [para(124(a,1),93(b,1,2)),rewrite(173(9))]. given #547 (F,wt=8): 7594 B(a ^ c,d,d v x). [para(284(a,1),4727(a,1))]. given #548 (F,wt=8): 7597 B(b ^ d,e,e v x). [para(285(a,1),4727(a,1))]. given #549 (T,wt=8): 7792 B(a ^ c,d,x v d). [para(25(a,1),7594(a,3))]. given #550 (T,wt=8): 7796 B(b ^ d,e,x v e). [para(25(a,1),7597(a,3))]. given #551 (A,wt=18): 321 B(x,y,z v x) | y ^ (z v x) != y | x v y != y. [para(126(a,1),93(b,1,2)),rewrite(174(9))]. given #552 (F,wt=10): 4763 B(e,a v c,a v (c v x)). [para(849(a,1),4626(a,1)),rewrite(27(8))]. given #553 (F,wt=10): 4852 B(x ^ (y ^ z),z,u v z). [para(26(a,1),4640(a,1))]. given #554 (T,wt=10): 4893 B(e,a v c,x v (a v c)). [para(849(a,1),4640(a,1))]. given #555 (T,wt=10): 4984 B(x ^ (y ^ b),b,a v c). [para(26(a,1),4651(a,1))]. given #556 (A,wt=15): 322 B(a,b,c v x) | (a v b) ^ (b v x) != b. [para(133(a,1),93(b,1)),rewrite(153(16)),xx(b)]. given #557 (F,wt=10): 4986 B(x ^ (y ^ d),d,a v c). [para(26(a,1),4657(a,1))]. given #558 (F,wt=8): 7978 B(a ^ c,d,a v c). [para(284(a,1),4986(a,1))]. given #559 (T,wt=10): 5015 B(x ^ (y ^ e),e,b v d). [para(26(a,1),4658(a,1))]. given #560 (T,wt=8): 7980 B(b ^ d,e,b v d). [para(285(a,1),5015(a,1))]. given #561 (A,wt=15): 323 B(a,d,c v x) | (a v d) ^ (d v x) != d. [para(137(a,1),93(b,1)),rewrite(49(15),158(16)),xx(b)]. given #562 (F,wt=10): 5019 B(x ^ (y ^ z),y,y v u). [para(47(a,1),4693(a,1))]. given #563 (F,wt=8): 7996 B(a ^ c,b,b v x). [para(433(a,1),5019(a,1))]. given #564 (T,wt=8): 8034 B(a ^ c,b,x v b). [para(25(a,1),7996(a,3))]. given #565 (T,wt=10): 5020 B(x ^ y,x,z v (x v u)). [para(49(a,1),4693(a,3))]. given #566 (A,wt=15): 324 B(b,e,d v x) | (b v e) ^ (e v x) != e. [para(141(a,1),93(b,1)),rewrite(49(15),163(16)),xx(b)]. given #567 (F,wt=10): 5035 B(x ^ y,x,z v (u v x)). [para(218(a,1),4693(a,3))]. given #568 (F,wt=10): 5037 B(x ^ (y ^ z),y,u v y). [para(47(a,1),4851(a,1))]. given #569 (T,wt=10): 5058 B(x ^ (b ^ y),b,a v c). [para(47(a,1),4983(a,1))]. given #570 (T,wt=8): 8138 B(a ^ c,b,a v c). [para(433(a,1),5058(a,1))]. given #571 (A,wt=17): 329 B(a,d,x v c) | (a v d) ^ (d v (x v c)) != d. [para(227(a,1),93(b,1)),xx(b)]. given #572 (F,wt=10): 5087 B(x ^ d,d,a v (y v c)). [para(289(a,1),286(c,1,2)),rewrite(49(20),5067(20),24(19),50(19),227(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #573 (F,wt=10): 5095 B(x ^ (d ^ y),d,a v c). [para(47(a,1),4985(a,1))]. given #574 (T,wt=10): 5096 B(x ^ (e ^ y),e,b v d). [para(47(a,1),5014(a,1))]. given #575 (T,wt=10): 5173 B(x ^ (y v z),z ^ x,z). [para(25(a,1),3198(a,1,2))]. given #576 (A,wt=17): 330 B(b,e,x v d) | (b v e) ^ (e v (x v d)) != e. [para(233(a,1),93(b,1)),xx(b)]. given #577 (F,wt=10): 5427 B(x ^ (a v c),b ^ x,b). [para(24(a,1),3207(a,1))]. given #578 (F,wt=10): 5474 B(x ^ (a v c),d ^ x,d). [para(24(a,1),3209(a,1))]. given #579 (T,wt=10): 5487 B(x ^ (b v d),e ^ x,e). [para(24(a,1),3211(a,1))]. given #580 (T,wt=10): 5528 B(x ^ e,e,b v (y v d)). [para(294(a,1),286(c,1,2)),rewrite(49(20),5508(20),24(19),50(19),233(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #581 (A,wt=16): 344 B(x,(x v y) ^ (x v z),(y v u) ^ (z v u)). [para(37(a,1),317(a,2)),rewrite(247(5))]. given #582 (F,wt=10): 5567 B(x ^ (a v c),e ^ x,e). [para(24(a,1),3233(a,1))]. given #583 (F,wt=10): 5640 B(a v (c v x),y v b,y). [para(223(a,1),3528(a,2))]. given #584 (T,wt=10): 5641 B(a v (c v x),y v d,y). [para(229(a,1),3528(a,2))]. given #585 (T,wt=10): 5642 B(b v (d v x),y v e,y). [para(235(a,1),3528(a,2))]. given #586 (A,wt=14): 350 B(x ^ y,(z v x) ^ (z v y),z v u). [para(37(a,1),340(a,2))]. given #587 (F,wt=10): 5647 B(a v (x v c),y v b,y). [para(277(a,1),3528(a,2))]. given #588 (F,wt=10): 5648 B(a v (x v c),y v d,y). [para(289(a,1),3528(a,2))]. given #589 (T,wt=10): 5649 B(b v (x v d),y v e,y). [para(294(a,1),3528(a,2))]. given #590 (T,wt=10): 5670 B(x ^ b,b,y v (a v c)). [para(299(a,1),286(c,1,2)),rewrite(2091(20),24(19),50(19),279(14),104(16),24(15),50(15)),xx(b),xx(c)]. given #591 (A,wt=12): 351 B(x,y v x,(y v z) ^ (y v u)). [para(37(a,1),340(a,3))]. given #592 (F,wt=10): 5673 B(x v (a v c),y v b,y). [para(299(a,1),3528(a,2))]. given #593 (F,wt=10): 5675 B(x ^ y,y ^ x,x v z). [para(29(a,1),3557(a,2,2))]. given #594 (T,wt=10): 5679 B(x ^ y,y ^ x,y v z). [para(65(a,1),3557(a,2))]. given #595 (T,wt=10): 5701 B(x v y,(y v x) ^ z,z). [para(219(a,1),3557(a,1)),rewrite(735(5))]. given #596 (A,wt=12): 352 B(x v y,x v (z v y),z v u). [para(49(a,1),340(a,2))]. given #597 (F,wt=10): 5858 B(x ^ y,y ^ x,z v y). [para(95(a,1),3558(a,2))]. given #598 (F,wt=10): 5872 B(x ^ b,b ^ x,a v c). [para(131(a,1),3558(a,2))]. given #599 (T,wt=10): 5875 B(x ^ d,d ^ x,a v c). [para(135(a,1),3558(a,2))]. given #600 (T,wt=10): 5878 B(x ^ e,e ^ x,b v d). [para(139(a,1),3558(a,2))]. given #601 (A,wt=15): 355 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(95(a,1),47(a,1,2)),flip(a)]. given #602 (F,wt=10): 5953 B(x ^ e,e ^ x,a v c). [para(856(a,1),3558(a,2))]. given #603 (F,wt=10): 6254 B(x v y,z ^ x,x ^ z). [para(187(a,1),3685(a,2))]. given #604 (T,wt=10): 6295 B(x v y,x ^ z,z ^ x). [para(51(a,1),3686(a,2))]. given #605 (T,wt=10): 6299 B(x v y,y ^ z,z ^ y). [para(95(a,1),3686(a,2))]. given #606 (A,wt=17): 356 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u. [para(49(a,1),95(a,1,2,1))]. given #607 (F,wt=10): 6312 B(a v c,b ^ x,x ^ b). [para(131(a,1),3686(a,2))]. given #608 (F,wt=10): 6315 B(a v c,d ^ x,x ^ d). [para(135(a,1),3686(a,2))]. given #609 (T,wt=10): 6318 B(b v d,e ^ x,x ^ e). [para(139(a,1),3686(a,2))]. given #610 (T,wt=10): 6393 B(a v c,e ^ x,x ^ e). [para(856(a,1),3686(a,2))]. given #611 (A,wt=12): 358 B(x v y,x v (y v z),u v z). [para(27(a,1),341(a,2))]. given #612 (F,wt=10): 6599 B(x,(y v z) ^ x,z v y). [para(24(a,1),3719(a,2))]. given #613 (F,wt=10): 7544 B(b ^ x,b,a v (c v y)). [para(24(a,1),4707(a,1))]. given #614 (T,wt=10): 7549 B(x ^ b,b,c v (y v a)). [para(218(a,1),4707(a,3))]. given #615 (T,wt=10): 7555 B(d ^ x,d,a v (c v y)). [para(24(a,1),4709(a,1))]. given #616 (A,wt=16): 360 B(x,(x v y) ^ (x v z),(u v y) ^ (u v z)). [para(37(a,1),341(a,2)),rewrite(37(5))]. given #617 (F,wt=10): 7560 B(x ^ d,d,c v (y v a)). [para(218(a,1),4709(a,3))]. given #618 (F,wt=10): 7561 B(e ^ x,e,b v (d v y)). [para(24(a,1),4712(a,1))]. given #619 (T,wt=10): 7566 B(x ^ e,e,d v (y v b)). [para(218(a,1),4712(a,3))]. given #620 (T,wt=10): 7567 B(b ^ x,b,a v (y v c)). [para(24(a,1),4725(a,1))]. given #621 (A,wt=12): 361 B(x,y v (x v z),u v (y v z)). [para(49(a,1),341(a,2))]. given #622 (F,wt=10): 7794 B(a ^ c,d,x v (d v y)). [para(49(a,1),7594(a,3))]. given #623 (F,wt=10): 7795 B(a ^ c,d,x v (y v d)). [para(218(a,1),7594(a,3))]. given #624 (T,wt=10): 7798 B(b ^ d,e,x v (e v y)). [para(49(a,1),7597(a,3))]. given #625 (T,wt=10): 7799 B(b ^ d,e,x v (y v e)). [para(218(a,1),7597(a,3))]. given #626 (A,wt=12): 362 B(x,x v (y v z),y v (u v z)). [para(49(a,1),341(a,3))]. given #627 (F,wt=10): 7856 B(e,a v c,a v (x v c)). [para(25(a,1),4763(a,3,2))]. given #628 (F,wt=10): 7860 B(e,a v c,c v (x v a)). [para(218(a,1),4763(a,3))]. given #629 (T,wt=10): 8036 B(a ^ c,b,x v (b v y)). [para(49(a,1),7996(a,3))]. given #630 (T,wt=10): 8037 B(a ^ c,b,x v (y v b)). [para(218(a,1),7996(a,3))]. given #631 (A,wt=12): 363 B(x,y v (z v x),u v (y v z)). [para(27(a,1),348(a,2))]. given #632 (F,wt=10): 8140 B(d ^ x,d,a v (y v c)). [para(24(a,1),5087(a,1))]. given #633 (F,wt=10): 8142 B(x ^ d,d,y v (a v c)). [para(49(a,1),5087(a,3))]. given #634 (T,wt=10): 8238 B(e ^ x,e,b v (y v d)). [para(24(a,1),5528(a,1))]. given #635 (T,wt=10): 8240 B(x ^ e,e,y v (b v d)). [para(49(a,1),5528(a,3))]. given #636 (A,wt=14): 365 B(x ^ y,(z v x) ^ (z v y),u v z). [para(37(a,1),348(a,2))]. given #637 (F,wt=10): 8253 B(x,(x v y) ^ (x v z),y). [para(104(a,1),344(a,3,1)),rewrite(50(5))]. given #638 (F,wt=10): 8254 B(x,(x v y) ^ (x v z),z). [para(104(a,1),344(a,3,2)),rewrite(24(5),50(5))]. given #639 (T,wt=10): 8255 B(x,(x v a) ^ (x v c),d). [para(57(a,1),344(a,3))]. given #640 (T,wt=10): 8256 B(x,(x v b) ^ (x v d),e). [para(58(a,1),344(a,3))]. given #641 (A,wt=16): 366 B(x,(y v x) ^ (z v x),(u v y) ^ (u v z)). [para(37(a,1),348(a,3)),rewrite(247(2))]. given #642 (F,wt=10): 8289 B(a v (c v x),b v y,y). [para(25(a,1),5640(a,2))]. given #643 (F,wt=10): 8294 B(c v (x v a),y v b,y). [para(218(a,1),5640(a,1))]. given #644 (T,wt=10): 8296 B(a v (c v x),d v y,y). [para(25(a,1),5641(a,2))]. given #645 (T,wt=10): 8301 B(c v (x v a),y v d,y). [para(218(a,1),5641(a,1))]. given #646 (A,wt=12): 367 B(x v y,x v (z v y),u v z). [para(49(a,1),348(a,2))]. given #647 (F,wt=10): 8303 B(b v (d v x),e v y,y). [para(25(a,1),5642(a,2))]. given #648 (F,wt=10): 8308 B(d v (x v b),y v e,y). [para(218(a,1),5642(a,1))]. given #649 (T,wt=10): 8328 B(b ^ c,a v b,a v x). [para(763(a,1),350(a,2))]. given #650 (T,wt=10): 8329 B(c ^ d,a v d,a v x). [para(845(a,1),350(a,2))]. given #651 (A,wt=12): 368 B(x,y v (z v x),y v (u v z)). [para(49(a,1),348(a,3)),rewrite(27(2))]. given #652 (F,wt=10): 8330 B(d ^ e,b v e,b v x). [para(877(a,1),350(a,2))]. given #653 (F,wt=10): 8336 B(a v (x v c),b v y,y). [para(25(a,1),5647(a,2))]. given #654 (T,wt=10): 8340 B(a v (x v c),d v y,y). [para(25(a,1),5648(a,2))]. given #655 (T,wt=10): 8342 B(x v (a v c),y v d,y). [para(49(a,1),5648(a,1))]. given #656 (A,wt=13): 369 d ^ ((b v e) ^ x) = d ^ (e ^ x). [para(283(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #657 (F,wt=10): 8345 B(b v (x v d),e v y,y). [para(25(a,1),5649(a,2))]. given #658 (F,wt=10): 8347 B(x v (b v d),y v e,y). [para(49(a,1),5649(a,1))]. given #659 (T,wt=10): 8350 B(b ^ x,b,y v (a v c)). [para(24(a,1),5670(a,1))]. given #660 (T,wt=10): 8362 B(x v (a v c),b v y,y). [para(25(a,1),5673(a,2))]. given #661 (A,wt=17): 370 (x v d) ^ (x v (b v e)) = (x v d) ^ (x v e). [para(283(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #662 (F,wt=10): 8423 B(a v d,a v c,c v x). [para(844(a,1),352(a,2))]. given #663 (F,wt=10): 8425 B(b v e,b v d,d v x). [para(876(a,1),352(a,2))]. given #664 (T,wt=10): 8565 B(b ^ x,b,c v (y v a)). [para(218(a,1),7544(a,3))]. given #665 (T,wt=10): 8573 B(d ^ x,d,c v (y v a)). [para(218(a,1),7555(a,3))]. given #666 (A,wt=13): 371 d ^ (x ^ (b v e)) = x ^ (d ^ e). [para(283(a,1),47(a,1,2)),flip(a)]. given #667 (F,wt=10): 8607 B(e ^ x,e,d v (y v b)). [para(218(a,1),7561(a,3))]. given #668 (F,wt=10): 8636 B(x,x v (a v d),a v c). [para(844(a,1),362(a,3))]. given #669 (T,wt=10): 8638 B(x,x v (b v e),b v d). [para(876(a,1),362(a,3))]. given #670 (T,wt=10): 8659 B(d ^ x,d,y v (a v c)). [para(49(a,1),8140(a,3))]. given #671 (A,wt=13): 373 a ^ (c ^ (d ^ x)) = a ^ (c ^ x). [para(284(a,1),26(a,1,1)),rewrite(26(4),26(9)),flip(a)]. given #672 (F,wt=9): 8942 a ^ (c ^ e) = a ^ c. [para(283(a,1),373(a,1,2,2)),rewrite(373(7),734(12))]. given #673 (F,wt=8): 8991 B(a,a ^ c,c ^ e). [para(8942(a,1),2869(a,2))]. given #674 (T,wt=8): 8992 B(c ^ e,a ^ c,a). [para(8942(a,1),3132(a,2))]. given #675 (T,wt=8): 8995 B(c,a ^ c,a ^ e). [para(8942(a,1),3134(a,2))]. given #676 (A,wt=19): 375 (x v a) ^ ((x v c) ^ (x v d)) = (x v a) ^ (x v c). [para(284(a,1),37(a,1,2)),rewrite(37(4),37(11)),flip(a)]. given #677 (F,wt=8): 9001 B(a ^ e,a ^ c,c). [para(8942(a,1),3190(a,2))]. given #678 (F,wt=8): 9018 B(a ^ c,e,e v x). [para(8942(a,1),4727(a,1))]. given #679 (T,wt=8): 9020 B(a ^ c,e,x v e). [para(8942(a,1),4852(a,1))]. given #680 (T,wt=8): 9021 B(a ^ c,e,b v d). [para(8942(a,1),5015(a,1))]. given #681 (A,wt=13): 376 a ^ (x ^ (c ^ d)) = x ^ (a ^ c). [para(284(a,1),47(a,1,2)),flip(a)]. given #682 (F,wt=10): 8665 B(e ^ x,e,y v (b v d)). [para(49(a,1),8238(a,3))]. given #683 (F,wt=10): 8685 B(b ^ c,a v b,x v a). [para(763(a,1),365(a,2))]. given #684 (T,wt=10): 8686 B(c ^ d,a v d,x v a). [para(845(a,1),365(a,2))]. given #685 (T,wt=10): 8687 B(d ^ e,b v e,x v b). [para(877(a,1),365(a,2))]. given #686 (A,wt=13): 377 (x v y) ^ (z v (y v x)) = x v y. [para(25(a,1),98(a,1,2)),rewrite(27(3))]. given #687 (F,wt=8): 9085 B(x v y,y v x,z). [para(377(a,1),305(b,1)),rewrite(49(9),25(8),124(8),126(8),27(9),173(10)),xx(b),xx(c)]. given #688 (F,wt=10): 8689 B(x,(y v x) ^ (x v z),y). [para(25(a,1),8253(a,2,1))]. given #689 (T,wt=10): 8690 B(x,(x v y) ^ (z v x),y). [para(25(a,1),8253(a,2,2))]. given #690 (T,wt=10): 8700 B(x,(y v x) ^ (x v z),z). [para(25(a,1),8254(a,2,1))]. given #691 (A,wt=19): 378 (x v (y v z)) ^ (x v (y v (u v z))) = x v (y v z). [para(27(a,1),98(a,1,1)),rewrite(27(5),27(8))]. given #692 (F,wt=10): 8701 B(x,(x v y) ^ (z v x),z). [para(25(a,1),8254(a,2,2))]. given #693 (F,wt=10): 8711 B(x,(a v x) ^ (x v c),d). [para(25(a,1),8255(a,2,1))]. given #694 (T,wt=10): 8712 B(x,(x v a) ^ (c v x),d). [para(25(a,1),8255(a,2,2))]. given #695 (T,wt=10): 8715 B(x,(b v x) ^ (x v d),e). [para(25(a,1),8256(a,2,1))]. given #696 (A,wt=17): 379 (x v y) ^ (z ^ (x v (u v y))) = z ^ (x v y). [para(98(a,1),47(a,1,2)),flip(a)]. given #697 (F,wt=10): 8716 B(x,(x v b) ^ (d v x),e). [para(25(a,1),8256(a,2,2))]. given #698 (F,wt=10): 8722 B(x,(y v x) ^ (z v x),y). [para(104(a,1),366(a,3,1)),rewrite(29(5))]. given #699 (T,wt=10): 8723 B(x,(y v x) ^ (z v x),z). [para(104(a,1),366(a,3,2)),rewrite(24(5),29(5))]. given #700 (T,wt=10): 8744 B(c v (x v a),b v y,y). [para(218(a,1),8289(a,1))]. given #701 (A,wt=19): 380 (x v (y v z)) ^ (y v (u v (x v z))) = y v (x v z). [para(49(a,1),98(a,1,1))]. given #702 (F,wt=10): 8756 B(c v (x v a),d v y,y). [para(218(a,1),8296(a,1))]. given #703 (F,wt=10): 8770 B(a v d,a v c,x v c). [para(844(a,1),367(a,2))]. given #704 (T,wt=10): 8773 B(b v e,b v d,x v d). [para(876(a,1),367(a,2))]. given #705 (T,wt=10): 8783 B(d v (x v b),e v y,y). [para(218(a,1),8303(a,1))]. given #706 (A,wt=13): 381 b ^ (d ^ (e ^ x)) = b ^ (d ^ x). [para(285(a,1),26(a,1,1)),rewrite(26(4),26(9)),flip(a)]. given #707 (F,wt=10): 8802 B(x,a v (d v x),a v c). [para(844(a,1),368(a,3))]. given #708 (F,wt=10): 8805 B(x,b v (e v x),b v d). [para(876(a,1),368(a,3))]. given #709 (T,wt=10): 8816 B(x v (a v c),d v y,y). [para(49(a,1),8340(a,1))]. given #710 (T,wt=10): 8856 B(x v (b v d),e v y,y). [para(49(a,1),8345(a,1))]. given #711 (A,wt=19): 383 (x v b) ^ ((x v d) ^ (x v e)) = (x v b) ^ (x v d). [para(285(a,1),37(a,1,2)),rewrite(37(4),37(11)),flip(a)]. given #712 (F,wt=10): 8929 B(x,a v (x v d),a v c). [para(49(a,1),8636(a,2))]. given #713 (F,wt=10): 8932 B(x,b v (x v e),b v d). [para(49(a,1),8638(a,2))]. given #714 (T,wt=10): 9037 B(a ^ c,e,x v (e v y)). [para(49(a,1),9018(a,3))]. given #715 (T,wt=10): 9038 B(a ^ c,e,x v (y v e)). [para(218(a,1),9018(a,3))]. given #716 (A,wt=13): 384 b ^ (x ^ (d ^ e)) = x ^ (b ^ d). [para(285(a,1),47(a,1,2)),flip(a)]. given #717 (F,wt=10): 9143 B(x,(x v c) ^ (a v x),d). [para(24(a,1),8711(a,2))]. given #718 (F,wt=10): 9144 B(x,(a v x) ^ (c v x),d). [para(25(a,1),8711(a,2,2))]. given #719 (T,wt=10): 9146 B(x,(c v x) ^ (x v a),d). [para(24(a,1),8712(a,2))]. given #720 (T,wt=10): 9148 B(x,(x v d) ^ (b v x),e). [para(24(a,1),8715(a,2))]. given #721 (A,wt=13): 385 d ^ ((x v (a v c)) ^ y) = d ^ y. [para(291(a,1),26(a,1,1)),flip(a)]. given #722 (F,wt=10): 9149 B(x,(b v x) ^ (d v x),e). [para(25(a,1),8715(a,2,2))]. given #723 (F,wt=10): 9159 B(x,(d v x) ^ (x v b),e). [para(24(a,1),8716(a,2))]. given #724 (T,wt=11): 2672 B(a,b v c,b) | b v c != b. [para(56(a,1),256(b,1,2)),rewrite(764(8),24(11),106(11),764(14),25(18),124(19),764(18),764(21)),flip(b),xx(c)]. given #725 (T,wt=11): 2871 B(x,y ^ x,x) | y ^ x != x. [para(122(a,1),262(c,1,2)),rewrite(104(3),100(3),104(8),24(8),50(8),24(7),29(7)),flip(c),xx(b)]. given #726 (A,wt=15): 387 (x v d) ^ (x v (y v (a v c))) = x v d. [para(291(a,1),37(a,1,2)),flip(a)]. given #727 (F,wt=11): 2970 B(a,c ^ d,d) | c ^ d != d. [para(156(a,1),262(c,1,2)),rewrite(50(12),104(20),100(19),24(18),110(18)),flip(c),xx(b)]. given #728 (F,wt=11): 2987 B(b,d ^ e,e) | d ^ e != e. [para(161(a,1),262(c,1,2)),rewrite(50(12),104(20),100(19),24(18),111(18)),flip(c),xx(b)]. given #729 (T,wt=11): 6626 B(a,c v d,d) | c v d != d. [para(57(a,1),304(b,1)),rewrite(844(16),25(19),126(19),846(18)),flip(b),xx(c)]. given #730 (T,wt=11): 6627 B(b,d v e,e) | d v e != e. [para(58(a,1),304(b,1)),rewrite(876(16),25(19),126(19),878(18)),flip(b),xx(c)]. given #731 (A,wt=13): 388 d ^ (x ^ (y v (a v c))) = x ^ d. [para(291(a,1),47(a,1,2)),flip(a)]. given #732 (F,wt=11): 6659 B(c,a v b,b) | a v b != b. [para(56(a,1),305(b,1)),rewrite(49(16),25(15),762(16),25(19),126(19),24(18),763(18)),flip(b),xx(c)]. given #733 (F,wt=11): 6660 B(d,a v d,c) | a v d != d. [para(57(a,1),305(b,1)),rewrite(126(16),25(19),49(19),844(19),24(18),845(18)),flip(b),xx(c)]. given #734 (T,wt=11): 6661 B(e,b v e,d) | b v e != e. [para(58(a,1),305(b,1)),rewrite(126(16),25(19),49(19),876(19),24(18),877(18)),flip(b),xx(c)]. given #735 (T,wt=11): 7266 B(a,c,b v c) | b v c != c. [para(764(a,1),315(b,1))]. given #736 (A,wt=13): 390 e ^ ((x v (b v d)) ^ y) = e ^ y. [para(296(a,1),26(a,1,1)),flip(a)]. given #737 (F,wt=11): 7294 B(a,c,c v d) | c v d != c. [para(846(a,1),318(b,1))]. given #738 (F,wt=11): 7295 B(b,d,d v e) | d v e != d. [para(878(a,1),318(b,1))]. given #739 (T,wt=11): 7701 B(a,b,a v c) | a v b != b. [para(106(a,1),320(b,1)),rewrite(25(12)),xx(b)]. given #740 (T,wt=11): 7702 B(a,d,a v c) | a v d != d. [para(110(a,1),320(b,1)),rewrite(25(12)),xx(b)]. given #741 (A,wt=15): 392 (x v e) ^ (x v (y v (b v d))) = x v e. [para(296(a,1),37(a,1,2)),flip(a)]. given #742 (F,wt=11): 7703 B(b,e,b v d) | b v e != e. [para(111(a,1),320(b,1)),rewrite(25(12)),xx(b)]. given #743 (F,wt=11): 7728 B(a,e,a v c) | a v e != e. [para(849(a,1),320(b,1)),rewrite(25(12)),xx(b)]. given #744 (T,wt=11): 7803 B(c,b,a v c) | b v c != b. [para(106(a,1),321(b,1)),rewrite(25(12)),xx(b)]. given #745 (T,wt=11): 7804 B(c,d,a v c) | c v d != d. [para(110(a,1),321(b,1)),xx(b)]. given #746 (A,wt=13): 393 e ^ (x ^ (y v (b v d))) = x ^ e. [para(296(a,1),47(a,1,2)),flip(a)]. given #747 (F,wt=11): 7805 B(d,e,b v d) | d v e != e. [para(111(a,1),321(b,1)),xx(b)]. given #748 (F,wt=11): 7830 B(c,e,a v c) | c v e != e. [para(849(a,1),321(b,1)),xx(b)]. given #749 (T,wt=11): 8987 a ^ (c ^ (e v x)) = a ^ c. [para(8942(a,1),187(a,1,2)),rewrite(247(4),24(9),26(9),51(8),8942(11))]. given #750 (T,wt=10): 9449 B(a,a ^ c,c ^ (e v x)). [para(8987(a,1),2869(a,2))]. given #751 (A,wt=14): 397 B(x v (y v z),x v (y v (z v u)),u). [para(27(a,1),334(a,1)),rewrite(27(5))]. given #752 (F,wt=10): 9450 B(c ^ (e v x),a ^ c,a). [para(8987(a,1),3132(a,2))]. given #753 (F,wt=10): 9453 B(c,a ^ c,a ^ (e v x)). [para(8987(a,1),3134(a,2))]. given #754 (T,wt=10): 9459 B(a ^ (e v x),a ^ c,c). [para(8987(a,1),3190(a,2))]. given #755 (T,wt=10): 9473 B(a,a ^ c,c ^ (x v e)). [para(25(a,1),9449(a,3,2))]. given #756 (A,wt=20): 398 B((x v y) ^ (x v z),(x v (y v u)) ^ (x v (z v u)),u). [para(37(a,1),334(a,1)),rewrite(247(5),37(7))]. given #757 (F,wt=10): 9477 B(c ^ (x v e),a ^ c,a). [para(25(a,1),9450(a,1,2))]. given #758 (F,wt=10): 9481 B(c,a ^ c,a ^ (x v e)). [para(25(a,1),9453(a,3,2))]. given #759 (T,wt=10): 9485 B(a ^ (x v e),a ^ c,c). [para(25(a,1),9459(a,1,2))]. given #760 (T,wt=11): 8988 a ^ (c ^ (x v e)) = a ^ c. [para(8942(a,1),357(a,1,2)),rewrite(37(4),24(9),26(9),95(8),8942(11))]. given #761 (A,wt=18): 399 B(x v y,(x v (y v z)) ^ (x v (y v u)),z ^ u). [para(37(a,1),334(a,2,2)),rewrite(37(5))]. given #762 (F,wt=11): 9335 B(x,y ^ x,x) | x ^ y != x. [para(24(a,1),2871(b,1))]. given #763 (F,wt=11): 9520 B(x,x ^ y,x) | x ^ y != x. [para(51(a,1),9335(b,1)),rewrite(24(3),51(3))]. given #764 (T,wt=11): 9539 B(x,x ^ y,x) | y ^ x != x. [para(24(a,1),9520(b,1))]. given #765 (T,wt=12): 444 B(x,x v y,z v (u v (y v v))). [para(27(a,1),347(a,3))]. given #766 (A,wt=14): 400 B(x v (y v z),y v (x v (z v u)),u). [para(49(a,1),334(a,1)),rewrite(27(4))]. given #767 (F,wt=12): 449 B(x,y v x,z v (u v (y v v))). [para(27(a,1),353(a,3))]. given #768 (F,wt=12): 497 B(x v (y v z),y v (z v u),u). [para(27(a,1),465(a,2))]. given #769 (T,wt=10): 9570 B(x v (a v c),a v c,d). [para(844(a,1),497(a,2))]. given #770 (T,wt=10): 9572 B(x v (b v d),b v d,e). [para(876(a,1),497(a,2))]. given #771 (A,wt=14): 401 B(x v y,x v (z v (y v u)),z v u). [para(49(a,1),334(a,2,2))]. given #772 (F,wt=10): 9573 B(a v (c v x),a v c,d). [para(25(a,1),9570(a,1)),rewrite(27(4))]. given #773 (F,wt=10): 9575 B(a v (x v c),a v c,d). [para(49(a,1),9570(a,1))]. given #774 (T,wt=10): 9577 B(b v (d v x),b v d,e). [para(25(a,1),9572(a,1)),rewrite(27(4))]. given #775 (T,wt=10): 9579 B(b v (x v d),b v d,e). [para(49(a,1),9572(a,1))]. given #776 (A,wt=17): 404 B(x v y,z,x v (y v z)) | x v (y v z) != z. [para(27(a,1),103(b,1)),rewrite(27(3))]. given #777 (F,wt=10): 9590 B(c v (x v a),a v c,d). [para(218(a,1),9573(a,1))]. given #778 (F,wt=10): 9595 B(d v (x v b),b v d,e). [para(218(a,1),9577(a,1))]. given #779 (T,wt=12): 500 B(x v (y v z),x v (z v u),u). [para(49(a,1),465(a,1)),rewrite(27(4))]. given #780 (T,wt=10): 9614 B(a v c,a v (d v x),x). [para(844(a,1),500(a,1))]. given #781 (A,wt=23): 405 B(x,y ^ z,(x v y) ^ (x v z)) | (x v y) ^ (x v z) != y ^ z. [para(37(a,1),103(b,1)),rewrite(37(3))]. given #782 (F,wt=10): 9617 B(b v d,b v (e v x),x). [para(876(a,1),500(a,1))]. given #783 (F,wt=10): 9619 B(a v c,a v (x v d),x). [para(25(a,1),9614(a,2,2))]. given #784 (T,wt=10): 9624 B(b v d,b v (x v e),x). [para(25(a,1),9617(a,2,2))]. given #785 (T,wt=10): 9628 B(a v c,x v (a v d),x). [para(49(a,1),9619(a,2))]. given #786 (A,wt=19): 406 B(x,y v z,x v (y v z)) | y v (x v z) != y v z. [para(49(a,1),103(b,1))]. given #787 (F,wt=10): 9631 B(b v d,x v (b v e),x). [para(49(a,1),9624(a,2))]. given #788 (F,wt=12): 501 B(x v y,z v (y v u),z v u). [para(49(a,1),465(a,2))]. given #789 (T,wt=10): 9648 B(x v c,a v c,a v d). [para(844(a,1),501(a,2))]. given #790 (T,wt=10): 9651 B(x v d,b v d,b v e). [para(876(a,1),501(a,2))]. given #791 (A,wt=18): 410 B((x v y) ^ (z v y),(y v x) ^ (y v z),x ^ z). [para(37(a,1),402(a,2)),rewrite(247(2))]. given #792 (F,wt=10): 9653 B(c v x,a v c,a v d). [para(25(a,1),9648(a,1))]. given #793 (F,wt=10): 9656 B(d v x,b v d,b v e). [para(25(a,1),9651(a,1))]. given #794 (T,wt=12): 503 B(x v (y v z),x v (y v u),u). [para(27(a,1),491(a,1)),rewrite(27(4))]. given #795 (T,wt=10): 9668 B(a v c,a v (b v x),x). [para(762(a,1),503(a,1))]. given #796 (A,wt=14): 415 B(x v y,z v (x v (y v u)),z v u). [para(27(a,1),336(a,2,2))]. given #797 (F,wt=10): 9672 B(a v c,a v (x v b),x). [para(25(a,1),9668(a,2,2))]. given #798 (F,wt=10): 9682 B(a v c,x v (a v b),x). [para(49(a,1),9672(a,2))]. given #799 (T,wt=12): 504 B((x v y) ^ (x v z),x v u,u). [para(37(a,1),491(a,1))]. given #800 (T,wt=12): 507 B(x v y,z v (x v u),z v u). [para(49(a,1),491(a,2))]. given #801 (A,wt=14): 416 B(x,y v (z v (x v u)),y v (z v u)). [para(27(a,1),336(a,2)),rewrite(27(5))]. given #802 (F,wt=12): 509 B(x v y,z v (u v y),z v u). [para(27(a,1),495(a,2))]. given #803 (F,wt=10): 9712 B(x v c,a v c,a v b). [para(762(a,1),509(a,2))]. given #804 (T,wt=10): 9716 B(c v x,a v c,a v b). [para(25(a,1),9712(a,1))]. given #805 (T,wt=12): 511 B(x v (y v z),u v (x v z),u). [para(49(a,1),495(a,1))]. given #806 (A,wt=20): 417 B(x,(y v (x v z)) ^ (y v (x v u)),(y v z) ^ (y v u)). [para(37(a,1),336(a,2,2)),rewrite(37(4),37(7))]. given #807 (F,wt=12): 512 B(x v (y v z),y v (u v z),u). [para(49(a,1),495(a,2))]. given #808 (F,wt=10): 9737 B(x v (a v c),a v c,b). [para(762(a,1),512(a,2))]. given #809 (T,wt=10): 9738 B(a v (c v x),a v c,b). [para(25(a,1),9737(a,1)),rewrite(27(4))]. given #810 (T,wt=10): 9740 B(a v (x v c),a v c,b). [para(49(a,1),9737(a,1))]. given #811 (A,wt=14): 418 B(x,y v (x v (z v u)),z v (y v u)). [para(49(a,1),336(a,3))]. given #812 (F,wt=10): 9745 B(c v (x v a),a v c,b). [para(218(a,1),9738(a,1))]. given #813 (F,wt=12): 513 B(x v (y v z),u v (x v y),u). [para(27(a,1),502(a,1))]. given #814 (T,wt=12): 514 B(x v y,z v (u v x),z v u). [para(27(a,1),502(a,2))]. given #815 (T,wt=12): 515 B((x v y) ^ (x v z),u v x,u). [para(37(a,1),502(a,1))]. given #816 (A,wt=14): 420 B(x,y v (z v (u v x)),y v (z v u)). [para(27(a,1),337(a,2,2))]. given #817 (F,wt=12): 518 B(x v (y v z),x v (u v y),u). [para(49(a,1),502(a,2)),rewrite(27(2))]. given #818 (F,wt=12): 533 B(x,x v y,z v (u v (v v y))). [para(27(a,1),359(a,3,2))]. given #819 (T,wt=12): 538 B(x,y v x,z v (u v (v v y))). [para(27(a,1),364(a,3,2))]. given #820 (T,wt=12): 557 B(x v (y v z),z v (x v y),x). [para(124(a,1),396(a,2,2)),rewrite(27(2))]. given #821 (A,wt=18): 421 B(x ^ y,(z v (u v x)) ^ (z v (u v y)),z v u). [para(37(a,1),337(a,2,2)),rewrite(37(5))]. given #822 (F,wt=12): 558 B(x v (y v z),z v (x v y),y). [para(126(a,1),396(a,2,2)),rewrite(27(2))]. given #823 (F,wt=12): 593 B(x,y v (x v z),x v (z v y)). [para(124(a,1),414(a,2,2)),rewrite(27(4))]. given #824 (T,wt=12): 623 B(x v (y v (z v u)),u v v,v). [para(27(a,1),496(a,1,2))]. given #825 (T,wt=12): 630 B(x v (y v (z v u)),z v v,v). [para(27(a,1),506(a,1))]. given #826 (A,wt=20): 422 B(x,(y v (z v x)) ^ (y v (u v x)),(y v z) ^ (y v u)). [para(37(a,1),337(a,3)),rewrite(247(2),37(4))]. given #827 (F,wt=12): 634 B(x v (y v (z v u)),v v u,v). [para(27(a,1),508(a,1,2))]. given #828 (F,wt=12): 640 B(x v (y v (z v u)),v v z,v). [para(27(a,1),517(a,1))]. given #829 (T,wt=12): 774 B(x v y,x v (y v b),a v c). [para(27(a,1),752(a,2))]. given #830 (T,wt=12): 776 B(x v y,x v (b v y),a v c). [para(49(a,1),773(a,2))]. given #831 (A,wt=14): 423 B(x v y,z v (x v (u v y)),z v u). [para(49(a,1),337(a,2,2))]. given #832 (F,wt=12): 792 B(x v (b v c),x v (a v c),a). [para(762(a,1),339(a,2,2))]. given #833 (F,wt=12): 794 B(b v c,a v c,x v (a v y)). [para(762(a,1),353(a,2))]. given #834 (T,wt=12): 807 B(x,x v (b v c),y v (a v c)). [para(762(a,1),359(a,3,2))]. given #835 (T,wt=12): 808 B(b v c,a v c,x v (y v a)). [para(762(a,1),364(a,2))]. given #836 (A,wt=14): 424 B(x,y v (z v (u v x)),z v (y v u)). [para(49(a,1),337(a,3)),rewrite(27(2))]. given #837 (F,wt=12): 809 B(x,b v (c v x),y v (a v c)). [para(762(a,1),364(a,3,2)),rewrite(27(4))]. given #838 (F,wt=12): 810 B(a v x,x v (a v c),b v c). [para(762(a,1),395(a,2,2))]. given #839 (T,wt=12): 811 B(a v c,b v (c v (x v a)),x). [para(762(a,1),396(a,1)),rewrite(27(9))]. given #840 (T,wt=12): 812 B(b v (c v x),x v (a v c),a). [para(762(a,1),396(a,2,2)),rewrite(27(4))]. given #841 (A,wt=14): 426 B(x v (y v z),x v (y v (u v z)),u). [para(27(a,1),339(a,1)),rewrite(27(5))]. given #842 (F,wt=12): 816 B(a,x v (a v c),b v (c v x)). [para(762(a,1),414(a,2,2)),rewrite(27(9))]. given #843 (F,wt=12): 817 B(x,b v (c v (x v a)),a v c). [para(762(a,1),414(a,3)),rewrite(27(6))]. given #844 (T,wt=12): 818 B(b v c,x v (a v c),a v x). [para(762(a,1),419(a,2,2))]. given #845 (T,wt=12): 821 B(x v (a v c),b v (c v y),y). [para(762(a,1),496(a,1,2)),rewrite(27(8))]. given #846 (A,wt=14): 427 B(x v y,x v (z v (u v y)),z v u). [para(27(a,1),339(a,2,2))]. given #847 (F,wt=12): 822 B(x v (y v a),a v c,b v c). [para(762(a,1),496(a,2))]. given #848 (F,wt=12): 824 B(x v (a v y),a v c,b v c). [para(762(a,1),506(a,2))]. given #849 (T,wt=12): 825 B(x v (a v c),y v (b v c),y). [para(762(a,1),508(a,1,2))]. given #850 (T,wt=12): 833 B(a v c,x v (b v y),x v y). [para(49(a,1),823(a,2))]. given #851 (A,wt=20): 428 B((x v y) ^ (x v z),(x v (u v y)) ^ (x v (u v z)),u). [para(37(a,1),339(a,1)),rewrite(37(5),37(7))]. given #852 (F,wt=12): 861 B(a v c,x v (y v b),x v y). [para(27(a,1),826(a,2))]. given #853 (F,wt=12): 863 B(x v y,x v (y v d),a v c). [para(27(a,1),834(a,2))]. given #854 (T,wt=12): 865 B(x v y,x v (d v y),a v c). [para(49(a,1),862(a,2))]. given #855 (T,wt=10): 9916 B(b v e,b v d,a v c). [para(876(a,1),865(a,2))]. given #856 (A,wt=14): 429 B(x v (y v z),y v (u v (x v z)),u). [para(49(a,1),339(a,1))]. given #857 (F,wt=12): 888 B(x v y,x v (y v e),b v d). [para(27(a,1),866(a,2))]. given #858 (F,wt=12): 890 B(x v y,x v (e v y),b v d). [para(49(a,1),887(a,2))]. given #859 (T,wt=12): 906 B(c v d,a v c,x v (a v y)). [para(844(a,1),353(a,2))]. given #860 (T,wt=12): 918 B(x,x v (c v d),y v (a v c)). [para(844(a,1),359(a,3,2))]. given #861 (A,wt=15): 431 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(26(a,1),105(a,1,2)),rewrite(26(6))]. given #862 (F,wt=12): 919 B(c v d,a v c,x v (y v a)). [para(844(a,1),364(a,2))]. given #863 (F,wt=12): 920 B(x,c v (d v x),y v (a v c)). [para(844(a,1),364(a,3,2)),rewrite(27(4))]. given #864 (T,wt=12): 922 B(a v c,c v (d v (x v a)),x). [para(844(a,1),396(a,1)),rewrite(27(9))]. given #865 (T,wt=12): 923 B(c v (d v x),x v (a v c),a). [para(844(a,1),396(a,2,2)),rewrite(27(4))]. given #866 (A,wt=13): 434 c ^ ((a v b) ^ x) = b ^ (c ^ x). [para(432(a,1),26(a,1,1)),rewrite(26(4)),flip(a)]. given #867 (F,wt=12): 928 B(x,c v (d v (x v a)),a v c). [para(844(a,1),414(a,3)),rewrite(27(6))]. given #868 (F,wt=12): 929 B(c v d,x v (a v c),a v x). [para(844(a,1),419(a,2,2))]. given #869 (T,wt=12): 932 B(x v (a v c),c v (d v y),y). [para(844(a,1),496(a,1,2)),rewrite(27(8))]. given #870 (T,wt=12): 934 B(x v (y v a),a v c,c v d). [para(844(a,1),496(a,2))]. given #871 (A,wt=17): 435 (x v c) ^ (x v (a v b)) = (x v b) ^ (x v c). [para(432(a,1),37(a,1,2)),rewrite(37(4)),flip(a)]. given #872 (F,wt=12): 935 B(x v (a v y),a v c,c v d). [para(844(a,1),506(a,2))]. given #873 (F,wt=12): 936 B(x v (a v c),y v (c v d),y). [para(844(a,1),508(a,1,2))]. given #874 (T,wt=12): 944 B(a v c,x v (d v y),x v y). [para(49(a,1),933(a,2))]. given #875 (T,wt=10): 10009 B(a v c,b v d,b v e). [para(876(a,1),944(a,2))]. given #876 (A,wt=13): 436 c ^ (x ^ (a v b)) = x ^ (b ^ c). [para(432(a,1),47(a,1,2)),flip(a)]. given #877 (F,wt=12): 955 B(a v c,x v (y v d),x v y). [para(27(a,1),937(a,2))]. given #878 (F,wt=12): 978 B(d v e,b v d,x v (b v y)). [para(876(a,1),353(a,2))]. given #879 (T,wt=12): 990 B(x,x v (d v e),y v (b v d)). [para(876(a,1),359(a,3,2))]. given #880 (T,wt=12): 991 B(d v e,b v d,x v (y v b)). [para(876(a,1),364(a,2))]. given #881 (A,wt=13): 438 a ^ (b ^ (c ^ x)) = a ^ (c ^ x). [para(433(a,1),26(a,1,1)),rewrite(26(4),26(9)),flip(a)]. given #882 (F,wt=10): 10061 B(a ^ (c ^ x),b,b v y). [para(438(a,1),5019(a,1))]. given #883 (F,wt=10): 10062 B(a ^ (c ^ x),b,y v b). [para(438(a,1),5037(a,1))]. given #884 (T,wt=10): 10063 B(a ^ (c ^ x),b,a v c). [para(438(a,1),5058(a,1))]. given #885 (T,wt=10): 10067 B(a ^ (x ^ c),b,b v y). [para(24(a,1),10061(a,1,2))]. given #886 (A,wt=19): 440 (x v a) ^ ((x v b) ^ (x v c)) = (x v a) ^ (x v c). [para(433(a,1),37(a,1,2)),rewrite(37(4),37(11)),flip(a)]. given #887 (F,wt=10): 10072 B(c ^ (x ^ a),b,b v y). [para(186(a,1),10061(a,1))]. given #888 (F,wt=10): 10074 B(x ^ (a ^ c),b,b v y). [para(303(a,1),10061(a,1,2)),rewrite(376(6))]. given #889 (T,wt=10): 10075 B(a ^ (x ^ c),b,y v b). [para(24(a,1),10062(a,1,2))]. given #890 (T,wt=10): 10078 B(c ^ (x ^ a),b,y v b). [para(186(a,1),10062(a,1))]. given #891 (A,wt=13): 441 a ^ (x ^ (b ^ c)) = x ^ (a ^ c). [para(433(a,1),47(a,1,2)),flip(a)]. given #892 (F,wt=10): 10080 B(x ^ (a ^ c),b,y v b). [para(303(a,1),10062(a,1,2)),rewrite(376(6))]. given #893 (F,wt=10): 10081 B(a ^ (x ^ c),b,a v c). [para(24(a,1),10063(a,1,2))]. given #894 (T,wt=10): 10084 B(c ^ (x ^ a),b,a v c). [para(186(a,1),10063(a,1))]. given #895 (T,wt=10): 10085 B(x ^ (a ^ c),b,a v c). [para(303(a,1),10063(a,1,2)),rewrite(376(6))]. given #896 (A,wt=14): 442 B(x v y,x v (y v z),u v (z v v)). [para(27(a,1),347(a,2))]. given #897 (F,wt=12): 992 B(x,d v (e v x),y v (b v d)). [para(876(a,1),364(a,3,2)),rewrite(27(4))]. given #898 (F,wt=12): 994 B(b v d,d v (e v (x v b)),x). [para(876(a,1),396(a,1)),rewrite(27(9))]. given #899 (T,wt=12): 995 B(d v (e v x),x v (b v d),b). [para(876(a,1),396(a,2,2)),rewrite(27(4))]. given #900 (T,wt=12): 1000 B(x,d v (e v (x v b)),b v d). [para(876(a,1),414(a,3)),rewrite(27(6))]. given #901 (A,wt=14): 443 B(x,x v (y v z),u v (y v (z v v))). [para(27(a,1),347(a,3,2))]. given #902 (F,wt=12): 1001 B(d v e,x v (b v d),b v x). [para(876(a,1),419(a,2,2))]. given #903 (F,wt=12): 1004 B(x v (b v d),d v (e v y),y). [para(876(a,1),496(a,1,2)),rewrite(27(8))]. given #904 (T,wt=12): 1006 B(x v (y v b),b v d,d v e). [para(876(a,1),496(a,2))]. given #905 (T,wt=12): 1007 B(x v (b v y),b v d,d v e). [para(876(a,1),506(a,2))]. given #906 (A,wt=20): 445 B(x,(x v y) ^ (x v z),(u v (y v v)) ^ (u v (z v v))). [para(37(a,1),347(a,2)),rewrite(247(5),37(7))]. given #907 (F,wt=12): 1008 B(x v (b v d),y v (d v e),y). [para(876(a,1),508(a,1,2))]. given #908 (F,wt=12): 1018 B(b v d,x v (e v y),x v y). [para(49(a,1),1005(a,2))]. given #909 (T,wt=12): 1037 B(b v d,x v (y v e),x v y). [para(27(a,1),1009(a,2))]. given #910 (T,wt=12): 1780 B(x,(x v y) ^ (x v z),z ^ y). [para(24(a,1),335(a,2))]. given #911 (A,wt=16): 446 B(x,x v y,(z v (y v u)) ^ (z v (y v v))). [para(37(a,1),347(a,3,2)),rewrite(37(5))]. given #912 (F,wt=12): 1781 B(x,(y v x) ^ (x v z),y ^ z). [para(25(a,1),335(a,2,1))]. given #913 (F,wt=8): 10193 B(c,c v d,a ^ d). [para(846(a,1),1781(a,2))]. given #914 (T,wt=8): 10194 B(d,d v e,b ^ e). [para(878(a,1),1781(a,2))]. given #915 (T,wt=12): 1782 B(x,(x v y) ^ (z v x),y ^ z). [para(25(a,1),335(a,2,2))]. given #916 (A,wt=14): 447 B(x,y v (x v z),u v (y v (z v v))). [para(49(a,1),347(a,2)),rewrite(27(4))]. given #917 (F,wt=12): 1805 B(x ^ y,(z v y) ^ (z v x),z). [para(24(a,1),338(a,1))]. given #918 (F,wt=12): 1806 B(x ^ y,(x v z) ^ (z v y),z). [para(25(a,1),338(a,2,1))]. given #919 (T,wt=8): 10285 B(a ^ d,c v d,c). [para(846(a,1),1806(a,2))]. given #920 (T,wt=8): 10286 B(b ^ e,d v e,d). [para(878(a,1),1806(a,2))]. given #921 (A,wt=14): 448 B(x,y v (z v x),u v (y v (z v v))). [para(27(a,1),353(a,2)),rewrite(27(4))]. given #922 (F,wt=12): 1807 B(x ^ y,(z v x) ^ (y v z),z). [para(25(a,1),338(a,2,2))]. given #923 (F,wt=12): 1903 B(x v y,y v (x v z),z v u). [para(25(a,1),342(a,1))]. given #924 (T,wt=12): 1904 B(x v y,y v (z v x),z v u). [para(25(a,1),342(a,2)),rewrite(27(3))]. given #925 (T,wt=12): 1922 B(x v y,y v x,z v (x v u)). [para(49(a,1),1912(a,3))]. given #926 (A,wt=16): 450 B(x ^ y,(z v x) ^ (z v y),u v (z v v)). [para(37(a,1),353(a,2))]. given #927 (F,wt=12): 1925 B(a v b,a v c,x v (c v y)). [para(49(a,1),1913(a,3))]. given #928 (F,wt=12): 2064 B(x v y,y v x,z v (u v x)). [para(27(a,1),1914(a,3))]. given #929 (T,wt=12): 2073 B(a v b,a v c,x v (y v c)). [para(27(a,1),1923(a,3))]. given #930 (T,wt=12): 2120 B(x,x v (y v z),z v (y v u)). [para(25(a,1),343(a,2,2))]. given #931 (A,wt=16): 451 B(x,y v x,(z v (y v u)) ^ (z v (y v v))). [para(37(a,1),353(a,3,2)),rewrite(37(5))]. given #932 (F,wt=12): 2121 B(x,x v (y v z),z v (u v y)). [para(25(a,1),343(a,3)),rewrite(27(4))]. given #933 (F,wt=12): 2141 B(d v e,a v (b v d),a v c). [para(876(a,1),2134(a,2,2))]. given #934 (T,wt=12): 2143 B(x,x v y,(z v y) ^ (y v u)). [para(25(a,1),345(a,3,1))]. given #935 (T,wt=12): 2144 B(x,x v y,(y v z) ^ (u v y)). [para(25(a,1),345(a,3,2))]. given #936 (A,wt=14): 452 B(x v y,x v (z v y),u v (z v v)). [para(49(a,1),353(a,2))]. given #937 (F,wt=12): 2174 B(x,x v b,a v (y v (c v z))). [para(49(a,1),2154(a,3,2))]. given #938 (F,wt=12): 2175 B(x,x v b,a v (y v (z v c))). [para(218(a,1),2154(a,3,2))]. given #939 (T,wt=12): 2182 B(x,b v x,a v (y v (c v z))). [para(49(a,1),2170(a,3,2))]. given #940 (T,wt=12): 2183 B(d v e,b v d,a v (c v x)). [para(876(a,1),2170(a,2))]. given #941 (A,wt=26): 453 B(x v y,z,u) | (x v (y v u)) ^ z != z | (x v (y v z)) ^ (z v u) != z. [para(24(a,1),113(b,1))]. given #942 (F,wt=12): 2184 B(x,b v x,a v (y v (z v c))). [para(218(a,1),2170(a,3,2))]. given #943 (F,wt=12): 2189 B(x,x v b,c v (y v (z v a))). [para(27(a,1),2176(a,3,2))]. given #944 (T,wt=12): 2195 B(d v e,b v d,a v (x v c)). [para(876(a,1),2178(a,2))]. given #945 (T,wt=12): 2197 B(x,b v x,c v (y v (z v a))). [para(27(a,1),2185(a,3,2))]. given #946 (A,wt=26): 454 B(x v y,z,u) | z ^ (x v (y v u)) != z | (z v u) ^ (x v (y v z)) != z. [para(24(a,1),113(c,1))]. given #947 (F,wt=6): 10456 B(c v d,d,a). [para(270(a,1),454(c,1)),rewrite(25(3),25(11),49(12),25(11),844(12),110(11),25(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #948 (F,wt=6): 10457 B(d v e,e,b). [para(273(a,1),454(c,1)),rewrite(25(3),25(11),49(12),25(11),876(12),111(11),25(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #949 (T,wt=6): 10458 B(a v d,d,c). [para(302(a,1),454(c,1)),rewrite(25(3),49(12),25(11),844(12),110(11),25(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #950 (T,wt=6): 10459 B(b v e,e,d). [para(370(a,1),454(c,1)),rewrite(25(3),49(12),25(11),876(12),111(11),25(12),104(15),24(14),50(14)),xx(b),xx(c)]. given #951 (A,wt=26): 455 B(x v y,z,u) | z ^ (x v (u v y)) != z | (x v (y v z)) ^ (z v u) != z. [para(25(a,1),113(b,1,2,2))]. given #952 (F,wt=6): 10460 B(a v b,b,c). [para(435(a,1),454(c,1)),rewrite(25(3),49(12),762(12),106(11),104(12),29(14)),xx(b),xx(c)]. given #953 (F,wt=11): 10447 B(a v c,c,b) | b v c != c. [para(132(a,1),454(c,1)),rewrite(25(3),49(12),25(11),762(12),50(11),25(12)),xx(b)]. given #954 (T,wt=11): 10448 B(a v c,c,d) | c v d != c. [para(136(a,1),454(c,1)),rewrite(25(3),49(12),844(12),50(11)),xx(b)]. given #955 (T,wt=11): 10449 B(b v d,d,e) | d v e != d. [para(140(a,1),454(c,1)),rewrite(25(3),49(12),876(12),50(11)),xx(b)]. given #956 (A,wt=26): 456 B(x v y,z,u) | z ^ (y v (u v x)) != z | (x v (y v z)) ^ (z v u) != z. [para(25(a,1),113(b,1,2)),rewrite(27(4))]. given #957 (F,wt=11): 10454 B(x v y,y,x) | x v y != y. [para(173(a,1),454(c,1)),rewrite(126(4),29(4)),xx(b)]. given #958 (F,wt=11): 10455 B(b v c,c,a) | b v c != c. [para(267(a,1),454(c,1)),rewrite(25(3),25(11),49(12),25(11),762(12),50(11),25(12),25(15),764(16)),xx(b)]. given #959 (T,wt=11): 10464 B(x v y,y,x) | y v x != y. [para(25(a,1),10454(b,1))]. given #960 (T,wt=12): 2200 B(d v e,b v d,c v (x v a)). [para(876(a,1),2185(a,2))]. given #961 (A,wt=26): 457 B(x v y,z,u) | z ^ (x v (y v u)) != z | (x v (z v y)) ^ (z v u) != z. [para(25(a,1),113(c,1,1,2))]. given #962 (F,wt=12): 2202 B(x,x v b,y v (z v (a v c))). [para(27(a,1),2187(a,3))]. given #963 (F,wt=12): 2204 B(x,b v x,y v (z v (a v c))). [para(27(a,1),2194(a,3))]. given #964 (T,wt=12): 2207 B(d v e,b v d,x v (a v c)). [para(876(a,1),2194(a,2))]. given #965 (T,wt=12): 2213 B(x,y v (x v z),y v (u v z)). [para(25(a,1),346(a,3,2))]. given #966 (A,wt=26): 458 B(x v y,z,u) | z ^ (x v (y v u)) != z | (y v (z v x)) ^ (z v u) != z. [para(25(a,1),113(c,1,1)),rewrite(27(8))]. given #967 (F,wt=12): 2214 B(x,y v (x v z),z v (u v y)). [para(25(a,1),346(a,3)),rewrite(27(4))]. given #968 (F,wt=10): 10495 B(x,d v (x v a),a v c). [para(844(a,1),2214(a,3))]. given #969 (T,wt=10): 10497 B(x,e v (x v b),b v d). [para(876(a,1),2214(a,3))]. given #970 (T,wt=12): 2220 B(x,y v (x v z),z v (y v u)). [para(49(a,1),346(a,3))]. given #971 (A,wt=26): 459 B(x v y,z,u) | z ^ (x v (y v u)) != z | (x v (y v z)) ^ (u v z) != z. [para(25(a,1),113(c,1,2))]. given #972 (F,wt=10): 10505 B(x,b v (x v a),a v c). [para(762(a,1),2220(a,3))]. given #973 (F,wt=12): 2227 B(b,a v c,a v (x v (c v y))). [para(49(a,1),2221(a,3,2))]. given #974 (T,wt=12): 2228 B(b,a v c,a v (x v (y v c))). [para(218(a,1),2221(a,3,2))]. given #975 (T,wt=12): 2231 B(b,a v c,c v (x v (y v a))). [para(27(a,1),2229(a,3,2))]. given #976 (A,wt=44): 460 B(x v y,z ^ u,v) | z ^ (u ^ (x v (y v v))) != z ^ u | (x v (y v z)) ^ ((x v (y v u)) ^ ((z v v) ^ (u v v))) != z ^ u. [para(26(a,1),113(b,1)),rewrite(37(11),37(13),247(16),26(18))]. given #977 (F,wt=12): 2248 B(b,a v c,x v (y v (a v c))). [para(27(a,1),2230(a,3))]. given #978 (F,wt=12): 2253 B(x,x v d,a v (y v (c v z))). [para(49(a,1),2232(a,3,2))]. given #979 (T,wt=12): 2254 B(x,x v d,a v (y v (z v c))). [para(218(a,1),2232(a,3,2))]. given #980 (T,wt=12): 2261 B(x,d v x,a v (y v (c v z))). [para(49(a,1),2249(a,3,2))]. given #981 (A,wt=32): 461 B(x v (y v z),u,v) | u ^ (x v (y v (z v v))) != u | (x v (y v (z v u))) ^ (u v v) != u. [para(27(a,1),113(b,1,2,2)),rewrite(27(10))]. given #982 (F,wt=12): 2262 B(x,d v x,a v (y v (z v c))). [para(218(a,1),2249(a,3,2))]. given #983 (F,wt=12): 2268 B(x,x v d,c v (y v (z v a))). [para(27(a,1),2255(a,3,2))]. given #984 (T,wt=12): 2274 B(x,d v x,c v (y v (z v a))). [para(27(a,1),2263(a,3,2))]. given #985 (T,wt=12): 2278 B(x,x v d,y v (z v (a v c))). [para(27(a,1),2265(a,3))]. given #986 (A,wt=38): 462 B(x v y,z v u,v) | (z v u) ^ (x v (y v v)) != z v u | (x v (y v (z v u))) ^ (z v (u v v)) != z v u. [para(27(a,1),113(c,1,2))]. given #987 (F,wt=8): 10536 B(x v a,x v b,c). [para(132(a,1),462(b,1)),rewrite(190(16),1126(20)),xx(b),xx(c)]. given #988 (F,wt=8): 10537 B(x v a,x v d,c). [para(136(a,1),462(b,1)),rewrite(190(16),25(18),1188(20)),xx(b),xx(c)]. given #989 (T,wt=8): 10538 B(x v b,x v e,d). [para(140(a,1),462(b,1)),rewrite(190(16),25(18),1301(20)),xx(b),xx(c)]. given #990 (T,wt=8): 10541 B(a v x,x v b,c). [para(25(a,1),10536(a,1))]. given #991 (A,wt=15): 463 B(x v y,x,z) | (y v x) ^ (x v z) != x. [para(29(a,1),113(b,1)),rewrite(126(5)),xx(b)]. given #992 (F,wt=8): 10542 B(x v a,b v x,c). [para(25(a,1),10536(a,2))]. given #993 (F,wt=8): 10547 B(a v x,x v d,c). [para(25(a,1),10537(a,1))]. given #994 (T,wt=8): 10548 B(x v a,d v x,c). [para(25(a,1),10537(a,2))]. given #995 (T,wt=8): 10553 B(b v x,x v e,d). [para(25(a,1),10538(a,1))]. given #996 (A,wt=38): 464 B(x v y,z,u ^ v) | z ^ ((x v (y v u)) ^ (x v (y v v))) != z | (x v (y v z)) ^ ((z v u) ^ (z v v)) != z. [para(37(a,1),113(b,1,2,2)),rewrite(37(7),37(14))]. given #997 (F,wt=8): 10554 B(x v b,e v x,d). [para(25(a,1),10538(a,2))]. given #998 (F,wt=8): 10558 B(a v x,b v x,c). [para(25(a,1),10541(a,2))]. given #999 (T,wt=8): 10576 B(a v x,d v x,c). [para(25(a,1),10547(a,2))]. given #1000 (T,wt=8): 10590 B(b v x,e v x,d). [para(25(a,1),10553(a,2))]. given #1001 (A,wt=13): 466 B(x v y,x,y v x) | y v x != x. [para(100(a,1),113(c,1)),rewrite(124(5),126(5),50(5),126(6)),xx(b)]. given #1002 (F,wt=8): 10596 B(x v y,y,z ^ y). [para(357(a,1),464(c,1)),rewrite(104(6),24(7),53(7),50(5),104(6),24(6),29(6)),xx(b),xx(c)]. given #1003 (F,wt=8): 10604 B(x v y,y,y ^ z). [para(24(a,1),10596(a,3))]. given #1004 (T,wt=8): 10605 B(x v y,x,z ^ x). [para(25(a,1),10596(a,1))]. given #1005 (T,wt=8): 10640 B(x v y,x,x ^ z). [para(25(a,1),10604(a,1))]. given #1006 (A,wt=32): 467 B(x v y,z,u v v) | z ^ (x v (u v (y v v))) != z | (x v (y v z)) ^ (z v (u v v)) != z. [para(49(a,1),113(b,1,2,2))]. given #1007 (F,wt=10): 10560 B(a v x,a v (b v x),c). [para(124(a,1),10541(a,1)),rewrite(25(6),49(6))]. given #1008 (F,wt=10): 10561 B(x v a,b v (x v a),c). [para(126(a,1),10541(a,1)),rewrite(25(6))]. given #1009 (T,wt=10): 10562 B(a v c,b v (c v d),c). [para(844(a,1),10541(a,1)),rewrite(25(8))]. given #1010 (T,wt=10): 10570 B(a v (b v x),b v x,c). [para(124(a,1),10542(a,2)),rewrite(25(4))]. given #1011 (A,wt=26): 468 B(x v y,z,u) | z ^ (y v (x v u)) != z | (x v (y v z)) ^ (z v u) != z. [para(49(a,1),113(b,1,2))]. given #1012 (F,wt=10): 10571 B(a v (x v b),x v b,c). [para(126(a,1),10542(a,2)),rewrite(25(4))]. given #1013 (F,wt=8): 10725 B(a,x v b,x v c). [back_rewrite(6891),rewrite(10721(15)),xx(b)]. given #1014 (T,wt=8): 10726 B(a,b v x,x v c). [para(25(a,1),10725(a,2))]. given #1015 (T,wt=8): 10727 B(a,x v b,c v x). [para(25(a,1),10725(a,3))]. given #1016 (A,wt=38): 469 B(x v y,z v u,v) | (z v u) ^ (x v (y v v)) != z v u | (x v (z v (y v u))) ^ (z v (u v v)) != z v u. [para(49(a,1),113(c,1,1,2)),rewrite(27(14))]. given #1017 (F,wt=8): 10731 B(a,b v x,c v x). [para(25(a,1),10726(a,3))]. given #1018 (F,wt=10): 10572 B(a v (d v e),b v d,c). [para(876(a,1),10542(a,2)),rewrite(25(5))]. given #1019 (T,wt=10): 10578 B(a v x,a v (d v x),c). [para(124(a,1),10547(a,1)),rewrite(25(6),49(6))]. given #1020 (T,wt=10): 10579 B(x v a,d v (x v a),c). [para(126(a,1),10547(a,1)),rewrite(25(6))]. given #1021 (A,wt=26): 470 B(x v y,z,u) | z ^ (x v (y v u)) != z | (y v (x v z)) ^ (z v u) != z. [para(49(a,1),113(c,1,1))]. given #1022 (F,wt=10): 10585 B(a v (d v x),d v x,c). [para(124(a,1),10548(a,2)),rewrite(25(4))]. given #1023 (F,wt=10): 10586 B(a v (x v d),x v d,c). [para(126(a,1),10548(a,2)),rewrite(25(4))]. given #1024 (T,wt=10): 10592 B(b v x,b v (e v x),d). [para(124(a,1),10553(a,1)),rewrite(25(6),49(6))]. given #1025 (T,wt=10): 10593 B(x v b,e v (x v b),d). [para(126(a,1),10553(a,1)),rewrite(25(6))]. given #1026 (A,wt=32): 471 B(x v y,z,u v v) | z ^ (x v (y v (u v v))) != z | (x v (y v z)) ^ (u v (z v v)) != z. [para(49(a,1),113(c,1,2))]. given #1027 (F,wt=10): 10600 B(b v (e v x),e v x,d). [para(124(a,1),10554(a,2)),rewrite(25(4))]. given #1028 (F,wt=10): 10601 B(b v (x v e),x v e,d). [para(126(a,1),10554(a,2)),rewrite(25(4))]. given #1029 (T,wt=10): 10606 B(x v y,y,z ^ (u ^ y)). [para(26(a,1),10596(a,3))]. given #1030 (T,wt=8): 10785 B(x v d,d,a ^ c). [para(284(a,1),10606(a,3))]. given #1031 (A,wt=15): 473 B(x v y,y,z) | (x v y) ^ (y v z) != y. [para(104(a,1),113(c,1,1,2)),rewrite(99(5)),xx(b)]. given #1032 (F,wt=8): 10786 B(x v e,e,b ^ d). [para(285(a,1),10606(a,3))]. given #1033 (F,wt=8): 10800 B(x v e,e,a ^ c). [para(8942(a,1),10606(a,3))]. given #1034 (T,wt=8): 10803 B(d v x,d,a ^ c). [para(25(a,1),10785(a,1))]. given #1035 (T,wt=8): 10808 B(e v x,e,b ^ d). [para(25(a,1),10786(a,1))]. given #1036 (A,wt=15): 475 B(x v y,x,y v (x v z)) | y v x != x. [para(53(a,1),113(c,1)),rewrite(27(3),27(6),124(7),190(7),99(7),126(7)),xx(b)]. given #1037 (F,wt=8): 10812 B(e v x,e,a ^ c). [para(25(a,1),10800(a,1))]. given #1038 (F,wt=10): 10607 B(x v (y v z),z,u ^ z). [para(27(a,1),10596(a,1))]. given #1039 (T,wt=8): 10832 B(a v c,d,x ^ d). [para(844(a,1),10607(a,1))]. given #1040 (T,wt=8): 10834 B(b v d,e,x ^ e). [para(876(a,1),10607(a,1))]. given #1041 (A,wt=19): 476 B(x v y,z,x v (y v (z v u))) | x v (y v z) != z. [para(99(a,1),113(c,1)),rewrite(27(4),27(3),27(8),27(7),190(9),124(9),170(9)),xx(b)]. given #1042 (F,wt=8): 10836 B(a v c,d,d ^ x). [para(24(a,1),10832(a,3))]. given #1043 (F,wt=8): 10838 B(b v d,e,e ^ x). [para(24(a,1),10834(a,3))]. given #1044 (T,wt=10): 10628 B(x v (a v c),a v c,e). [para(849(a,1),10596(a,3))]. given #1045 (T,wt=10): 10641 B(x v (y v z),z,z ^ u). [para(27(a,1),10604(a,1))]. given #1046 (A,wt=30): 477 B(x v y,z,y v u) | z ^ (x v (y v u)) != z | (x v (y v z)) ^ (z v (y v u)) != z. [para(124(a,1),113(b,1,2,2))]. given #1047 (F,wt=10): 10642 B(x v y,y,z ^ (y ^ u)). [para(47(a,1),10604(a,3))]. given #1048 (F,wt=8): 10870 B(x v b,b,a ^ c). [para(433(a,1),10642(a,3))]. given #1049 (T,wt=8): 10900 B(b v x,b,a ^ c). [para(25(a,1),10870(a,1))]. given #1050 (T,wt=10): 10660 B(x v y,x,z ^ (u ^ x)). [para(26(a,1),10605(a,3))]. given #1051 (A,wt=36): 478 B(x v y,y v z,u) | (y v z) ^ (x v (y v u)) != y v z | (x v (y v z)) ^ (y v (z v u)) != y v z. [para(124(a,1),113(c,1,1,2)),rewrite(27(13))]. given #1052 (F,wt=8): 10925 B(a,a v b,c v x). [para(223(a,1),478(b,1)),rewrite(104(3),124(19),777(23),1149(22)),xx(b),xx(c)]. given #1053 (F,wt=8): 10926 B(a,a v d,c v x). [para(229(a,1),478(b,1)),rewrite(104(3),124(19),49(22),891(23),1215(22)),xx(b),xx(c)]. given #1054 (T,wt=8): 10927 B(b,b v e,d v x). [para(235(a,1),478(b,1)),rewrite(104(3),124(19),49(22),963(23),1341(22)),xx(b),xx(c)]. given #1055 (T,wt=8): 10928 B(a,a v b,x v c). [para(277(a,1),478(b,1)),rewrite(104(3),124(19),4248(23),4249(22)),xx(b),xx(c)]. given #1056 (A,wt=19): 479 B(x v y,z,z v u) | (x v (y v z)) ^ (z v u) != z. [para(124(a,1),113(c,1,2)),rewrite(170(7)),xx(b)]. given #1057 (F,wt=8): 10929 B(a,a v d,x v c). [para(289(a,1),478(b,1)),rewrite(104(3),124(19),5067(23),5068(22)),xx(b),xx(c)]. given #1058 (F,wt=8): 10930 B(b,b v e,x v d). [para(294(a,1),478(b,1)),rewrite(104(3),124(19),5508(23),5509(22)),xx(b),xx(c)]. given #1059 (T,wt=10): 10663 B(x v (y v z),y,u ^ y). [para(49(a,1),10605(a,1))]. given #1060 (T,wt=8): 10953 B(a v c,b,x ^ b). [para(762(a,1),10663(a,1))]. given #1061 (A,wt=30): 480 B(x v y,z,u v y) | z ^ (x v (u v y)) != z | (x v (y v z)) ^ (z v (u v y)) != z. [para(126(a,1),113(b,1,2,2))]. given #1062 (F,wt=8): 10956 B(a v c,b,b ^ x). [para(24(a,1),10953(a,3))]. given #1063 (F,wt=10): 10682 B(a v (c v x),a v c,e). [para(849(a,1),10605(a,3)),rewrite(27(4))]. given #1064 (T,wt=10): 10693 B(x v y,x,z ^ (x ^ u)). [para(47(a,1),10640(a,3))]. given #1065 (T,wt=10): 10694 B(x v (y v z),y,y ^ u). [para(49(a,1),10640(a,1))]. given #1066 (A,wt=36): 482 B(x v y,z v y,u) | (z v y) ^ (x v (y v u)) != z v y | (x v (z v y)) ^ (z v (y v u)) != z v y. [para(126(a,1),113(c,1,1,2)),rewrite(27(13))]. given #1067 (F,wt=10): 10707 B(x v a,a v (b v x),c). [para(25(a,1),10560(a,1))]. given #1068 (F,wt=10): 10708 B(a v x,a v (x v b),c). [para(25(a,1),10560(a,2,2))]. given #1069 (T,wt=10): 10712 B(a v x,b v (x v a),c). [para(25(a,1),10561(a,1))]. given #1070 (T,wt=10): 10715 B(x v a,x v (a v b),c). [para(49(a,1),10561(a,2)),rewrite(25(5))]. given #1071 (A,wt=19): 483 B(x v y,z,u v z) | (x v (y v z)) ^ (u v z) != z. [para(126(a,1),113(c,1,2)),rewrite(168(7)),xx(b)]. given #1072 (F,wt=10): 10717 B(a v (x v b),b v x,c). [para(25(a,1),10570(a,1,2))]. given #1073 (F,wt=10): 10718 B(a v (b v x),x v b,c). [para(25(a,1),10570(a,2))]. given #1074 (T,wt=10): 10724 B(x v (a v b),x v b,c). [para(49(a,1),10571(a,1))]. given #1075 (T,wt=10): 10733 B(a,b v x,b v (c v x)). [para(124(a,1),10726(a,2)),rewrite(25(7),49(7))]. given #1076 (A,wt=17): 487 B(a v x,b,c) | (a v (x v b)) ^ (b v c) != b. [para(221(a,1),113(b,1)),xx(b)]. given #1077 (F,wt=10): 10734 B(a,x v b,c v (x v b)). [para(126(a,1),10726(a,2)),rewrite(25(7))]. given #1078 (F,wt=10): 10735 B(a,b v d,c v (d v e)). [para(876(a,1),10726(a,2)),rewrite(25(9))]. given #1079 (T,wt=10): 10739 B(a,b v (c v x),c v x). [para(124(a,1),10727(a,3)),rewrite(25(5))]. given #1080 (T,wt=10): 10740 B(a,b v (x v c),x v c). [para(126(a,1),10727(a,3)),rewrite(25(5))]. given #1081 (A,wt=17): 488 B(a v x,d,c) | (a v (x v d)) ^ (c v d) != d. [para(227(a,1),113(b,1)),rewrite(25(15)),xx(b)]. given #1082 (F,wt=10): 10743 B(x v a,a v (d v x),c). [para(25(a,1),10578(a,1))]. given #1083 (F,wt=10): 10744 B(a v x,a v (x v d),c). [para(25(a,1),10578(a,2,2))]. given #1084 (T,wt=10): 10747 B(a v x,d v (x v a),c). [para(25(a,1),10579(a,1))]. given #1085 (T,wt=10): 10750 B(x v a,x v (a v d),c). [para(49(a,1),10579(a,2)),rewrite(25(5))]. given #1086 (A,wt=17): 489 B(b v x,e,d) | (b v (x v e)) ^ (d v e) != e. [para(233(a,1),113(b,1)),rewrite(25(15)),xx(b)]. given #1087 (F,wt=10): 10752 B(a v (x v d),d v x,c). [para(25(a,1),10585(a,1,2))]. given #1088 (F,wt=10): 10753 B(a v (d v x),x v d,c). [para(25(a,1),10585(a,2))]. given #1089 (T,wt=10): 10759 B(x v (a v d),x v d,c). [para(49(a,1),10586(a,1))]. given #1090 (T,wt=10): 10760 B(x v b,b v (e v x),d). [para(25(a,1),10592(a,1))]. given #1091 (A,wt=17): 490 B(x v a,b,c) | (x v (a v b)) ^ (b v c) != b. [para(279(a,1),113(b,1)),xx(b)]. given #1092 (F,wt=10): 10761 B(b v x,b v (x v e),d). [para(25(a,1),10592(a,2,2))]. given #1093 (F,wt=10): 10764 B(b v x,e v (x v b),d). [para(25(a,1),10593(a,1))]. given #1094 (T,wt=10): 10767 B(x v b,x v (b v e),d). [para(49(a,1),10593(a,2)),rewrite(25(5))]. given #1095 (T,wt=10): 10769 B(b v (x v e),e v x,d). [para(25(a,1),10600(a,1,2))]. given #1096 (A,wt=15): 492 B(x v y,x,z v (y v x)) | y v x != x. [para(98(a,1),113(c,1)),rewrite(190(7),218(7),97(7),126(7)),xx(b)]. given #1097 (F,wt=10): 10770 B(b v (e v x),x v e,d). [para(25(a,1),10600(a,2))]. given #1098 (F,wt=10): 10776 B(x v (b v e),x v e,d). [para(49(a,1),10601(a,1))]. given #1099 (T,wt=10): 10804 B(x v (y v d),d,a ^ c). [para(27(a,1),10785(a,1))]. given #1100 (T,wt=8): 11048 B(a v c,d,a ^ c). [para(844(a,1),10804(a,1))]. given #1101 (A,wt=17): 493 B(x v a,d,c) | (x v (a v d)) ^ (c v d) != d. [para(291(a,1),113(b,1)),rewrite(25(15)),xx(b)]. given #1102 (F,wt=10): 10809 B(x v (y v e),e,b ^ d). [para(27(a,1),10786(a,1))]. given #1103 (F,wt=8): 11050 B(b v d,e,b ^ d). [para(876(a,1),10809(a,1))]. given #1104 (T,wt=10): 10813 B(x v (y v e),e,a ^ c). [para(27(a,1),10800(a,1))]. given #1105 (T,wt=8): 11053 B(b v d,e,a ^ c). [para(876(a,1),10813(a,1))]. given #1106 (A,wt=17): 494 B(x v b,e,d) | (x v (b v e)) ^ (d v e) != e. [para(296(a,1),113(b,1)),rewrite(25(15)),xx(b)]. given #1107 (F,wt=10): 10817 B(x v (d v y),d,a ^ c). [para(49(a,1),10803(a,1))]. given #1108 (F,wt=10): 10819 B(x v (e v y),e,b ^ d). [para(49(a,1),10808(a,1))]. given #1109 (T,wt=10): 10821 B(x v (e v y),e,a ^ c). [para(49(a,1),10812(a,1))]. given #1110 (T,wt=10): 10837 B(a v c,d,x ^ (y ^ d)). [para(26(a,1),10832(a,3))]. given #1111 (A,wt=16): 498 B((x v y) ^ (x v z),(y v u) ^ (z v u),u). [para(37(a,1),465(a,1)),rewrite(247(5))]. given #1112 (F,wt=10): 10839 B(b v d,e,x ^ (y ^ e)). [para(26(a,1),10834(a,3))]. given #1113 (F,wt=10): 10843 B(a v c,d,x ^ (d ^ y)). [para(47(a,1),10836(a,3))]. given #1114 (T,wt=10): 10844 B(b v d,e,x ^ (e ^ y)). [para(47(a,1),10838(a,3))]. given #1115 (T,wt=10): 10846 B(a v (x v c),a v c,e). [para(49(a,1),10628(a,1))]. given #1116 (A,wt=14): 499 B(x v y,(y v z) ^ (y v u),z ^ u). [para(37(a,1),465(a,2))]. given #1117 (F,wt=10): 10899 B(x v b,b,a ^ (c ^ y)). [para(438(a,1),10642(a,3))]. given #1118 (F,wt=10): 10901 B(x v (y v b),b,a ^ c). [para(27(a,1),10870(a,1))]. given #1119 (T,wt=10): 10904 B(x v (b v y),b,a ^ c). [para(49(a,1),10900(a,1))]. given #1120 (T,wt=8): 11081 B(a v c,b,a ^ c). [para(762(a,1),10904(a,1))]. given #1121 (A,wt=14): 505 B(x v y,(x v z) ^ (x v u),z ^ u). [para(37(a,1),491(a,2))]. given #1122 (F,wt=10): 10932 B(a,a v b,x v (c v y)). [para(49(a,1),10925(a,3))]. given #1123 (F,wt=10): 10933 B(a,a v b,x v (y v c)). [para(218(a,1),10925(a,3))]. given #1124 (T,wt=10): 10935 B(a,a v d,x v (c v y)). [para(49(a,1),10926(a,3))]. given #1125 (T,wt=10): 10936 B(a,a v d,x v (y v c)). [para(218(a,1),10926(a,3))]. given #1126 (A,wt=16): 510 B((x v y) ^ (x v z),(u v y) ^ (u v z),u). [para(37(a,1),495(a,1)),rewrite(37(5))]. given #1127 (F,wt=10): 10938 B(b,b v e,x v (d v y)). [para(49(a,1),10927(a,3))]. given #1128 (F,wt=10): 10939 B(b,b v e,x v (y v d)). [para(218(a,1),10927(a,3))]. given #1129 (T,wt=8): 11103 B(b,b v e,a v c). [para(844(a,1),10939(a,3))]. given #1130 (T,wt=10): 10957 B(a v c,b,x ^ (y ^ b)). [para(26(a,1),10953(a,3))]. given #1131 (A,wt=16): 516 B((x v y) ^ (z v y),(u v x) ^ (u v z),u). [para(37(a,1),502(a,2)),rewrite(247(2))]. given #1132 (F,wt=10): 10959 B(a v c,b,x ^ (b ^ y)). [para(47(a,1),10956(a,3))]. given #1133 (F,wt=10): 10963 B(c v (x v a),a v c,e). [para(218(a,1),10682(a,1))]. given #1134 (T,wt=10): 10992 B(b v x,b,a ^ (c ^ y)). [para(438(a,1),10693(a,3))]. given #1135 (T,wt=10): 11008 B(x v a,a v (x v b),c). [para(25(a,1),10707(a,2,2))]. given #1136 (A,wt=20): 519 B(x,y,z) | (x v z) ^ y != y | (x v y) ^ (z v y) != y. [para(24(a,1),115(b,1))]. given #1137 (F,wt=10): 11010 B(a v x,x v (a v b),c). [para(49(a,1),10708(a,2))]. given #1138 (F,wt=10): 11013 B(x v (a v b),b v x,c). [para(49(a,1),10717(a,1))]. given #1139 (T,wt=10): 11015 B(a,x v b,b v (c v x)). [para(25(a,1),10733(a,2))]. given #1140 (T,wt=10): 11016 B(a,b v x,b v (x v c)). [para(25(a,1),10733(a,3,2))]. given #1141 (A,wt=20): 520 B(x,y,z) | y ^ (x v z) != y | (z v y) ^ (x v y) != y. [para(24(a,1),115(c,1))]. given #1142 (F,wt=10): 11019 B(a,b v x,c v (x v b)). [para(25(a,1),10734(a,2))]. given #1143 (F,wt=10): 11022 B(a,x v b,x v (b v c)). [para(49(a,1),10734(a,3)),rewrite(25(6))]. given #1144 (T,wt=10): 11023 B(a,b v (x v c),c v x). [para(25(a,1),10739(a,2,2))]. given #1145 (T,wt=10): 11024 B(a,b v (c v x),x v c). [para(25(a,1),10739(a,3))]. given #1146 (A,wt=20): 521 B(x,y,z) | y ^ (z v x) != y | (x v y) ^ (z v y) != y. [para(25(a,1),115(b,1,2))]. given #1147 (F,wt=10): 11029 B(a,x v (b v c),x v c). [para(49(a,1),10740(a,2))]. given #1148 (F,wt=10): 11031 B(x v a,a v (x v d),c). [para(25(a,1),10743(a,2,2))]. given #1149 (T,wt=10): 11033 B(a v x,x v (a v d),c). [para(49(a,1),10744(a,2))]. given #1150 (T,wt=10): 11037 B(x v (a v d),d v x,c). [para(49(a,1),10752(a,1))]. given #1151 (A,wt=20): 522 B(x,y,z) | y ^ (x v z) != y | (y v x) ^ (z v y) != y. [para(25(a,1),115(c,1,1))]. given #1152 (F,wt=10): 11039 B(x v b,b v (x v e),d). [para(25(a,1),10760(a,2,2))]. given #1153 (F,wt=10): 11041 B(b v x,x v (b v e),d). [para(49(a,1),10761(a,2))]. given #1154 (T,wt=10): 11044 B(x v (b v e),e v x,d). [para(49(a,1),10769(a,1))]. given #1155 (T,wt=10): 11069 B(x v a,a v b,b ^ c). [para(763(a,1),499(a,2))]. given #1156 (A,wt=36): 523 B(x,y ^ z,u) | y ^ (z ^ (x v u)) != y ^ z | (x v y) ^ ((x v z) ^ ((u v y) ^ (u v z))) != y ^ z. [para(26(a,1),115(b,1)),rewrite(37(9),37(12),26(14))]. given #1157 (F,wt=10): 11070 B(x v a,a v d,c ^ d). [para(845(a,1),499(a,2))]. given #1158 (F,wt=10): 11071 B(x v b,b v e,d ^ e). [para(877(a,1),499(a,2))]. given #1159 (T,wt=10): 11072 B(x v b,b,a ^ (y ^ c)). [para(24(a,1),10899(a,3,2))]. given #1160 (T,wt=10): 11076 B(x v b,b,c ^ (y ^ a)). [para(186(a,1),10899(a,3))]. given #1161 (A,wt=26): 524 B(x,y,z v u) | y ^ (x v (z v u)) != y | (x v y) ^ (z v (u v y)) != y. [para(27(a,1),115(c,1,2))]. given #1162 (F,wt=10): 11078 B(x v b,b,y ^ (a ^ c)). [para(303(a,1),10899(a,3,2)),rewrite(376(9))]. given #1163 (F,wt=10): 11085 B(a v x,a v b,b ^ c). [para(763(a,1),505(a,2))]. given #1164 (T,wt=10): 11086 B(a v x,a v d,c ^ d). [para(845(a,1),505(a,2))]. given #1165 (T,wt=10): 11087 B(b v x,b v e,d ^ e). [para(877(a,1),505(a,2))]. given #1166 (A,wt=30): 525 B(x,y,z ^ u) | y ^ ((x v z) ^ (x v u)) != y | (x v y) ^ ((z v y) ^ (u v y)) != y. [para(37(a,1),115(b,1,2)),rewrite(247(10))]. given #1167 (F,wt=10): 11106 B(d,(x v a) ^ (x v c),x). [para(57(a,1),516(a,1))]. given #1168 (F,wt=10): 11107 B(e,(x v b) ^ (x v d),x). [para(58(a,1),516(a,1))]. given #1169 (T,wt=10): 11120 B(a v c,b,a ^ (c ^ x)). [para(438(a,1),10959(a,3))]. given #1170 (T,wt=10): 11122 B(b v x,b,a ^ (y ^ c)). [para(24(a,1),10992(a,3,2))]. given #1171 (A,wt=26): 526 B(x,y,z v u) | y ^ (z v (x v u)) != y | (x v y) ^ (z v (u v y)) != y. [para(49(a,1),115(b,1,2)),rewrite(27(9))]. given #1172 (F,wt=8): 11172 B(a,x v d,x v c). [para(136(a,1),526(b,1)),rewrite(190(20),10756(20)),xx(b),xx(c)]. given #1173 (F,wt=8): 11173 B(b,x v e,x v d). [para(140(a,1),526(b,1)),rewrite(190(20),10773(20)),xx(b),xx(c)]. given #1174 (T,wt=8): 11175 B(a,d v x,x v c). [para(25(a,1),11172(a,2))]. given #1175 (T,wt=8): 11176 B(a,x v d,c v x). [para(25(a,1),11172(a,3))]. given #1176 (A,wt=32): 527 B(x,y v z,u) | (y v z) ^ (x v u) != y v z | (y v (x v z)) ^ (u v (y v z)) != y v z. [para(49(a,1),115(c,1,1))]. given #1177 (F,wt=8): 11180 B(b,e v x,x v d). [para(25(a,1),11173(a,2))]. given #1178 (F,wt=8): 11181 B(b,x v e,d v x). [para(25(a,1),11173(a,3))]. given #1179 (T,wt=8): 11185 B(a,d v x,c v x). [para(25(a,1),11175(a,3))]. given #1180 (T,wt=8): 11197 B(b,e v x,d v x). [para(25(a,1),11180(a,3))]. given #1181 (A,wt=32): 528 B(x,y v z,u) | (y v z) ^ (x v u) != y v z | (x v (y v z)) ^ (y v (u v z)) != y v z. [para(49(a,1),115(c,1,2))]. given #1182 (F,wt=10): 11127 B(b v x,b,c ^ (y ^ a)). [para(186(a,1),10992(a,3))]. given #1183 (F,wt=10): 11128 B(b v x,b,y ^ (a ^ c)). [para(303(a,1),10992(a,3,2)),rewrite(376(9))]. given #1184 (T,wt=10): 11130 B(a,x v b,b v (x v c)). [para(25(a,1),11015(a,3,2))]. given #1185 (T,wt=10): 11132 B(a,b v x,x v (b v c)). [para(49(a,1),11016(a,3))]. given #1186 (A,wt=18): 529 B(x,y,x v z) | y ^ (x v z) != y | x v y != y. [para(124(a,1),115(b,1,2)),rewrite(27(8),98(9))]. given #1187 (F,wt=10): 11134 B(a,x v (b v c),c v x). [para(49(a,1),11023(a,2))]. given #1188 (F,wt=10): 11161 B(d,(a v x) ^ (x v c),x). [para(25(a,1),11106(a,2,1))]. given #1189 (T,wt=10): 11162 B(d,(x v a) ^ (c v x),x). [para(25(a,1),11106(a,2,2))]. given #1190 (T,wt=10): 11163 B(e,(b v x) ^ (x v d),x). [para(25(a,1),11107(a,2,1))]. given #1191 (A,wt=17): 530 B(x,y v z,y) | (y v z) ^ (x v y) != y v z. [para(124(a,1),115(c,1,2)),rewrite(24(11),50(11)),xx(c)]. given #1192 (F,wt=10): 11164 B(e,(x v b) ^ (d v x),x). [para(25(a,1),11107(a,2,2))]. given #1193 (F,wt=10): 11165 B(a v c,b,a ^ (x ^ c)). [para(24(a,1),11120(a,3,2))]. given #1194 (T,wt=10): 11168 B(a v c,b,c ^ (x ^ a)). [para(186(a,1),11120(a,3))]. given #1195 (T,wt=10): 11169 B(a v c,b,x ^ (a ^ c)). [para(303(a,1),11120(a,3,2)),rewrite(376(10))]. given #1196 (A,wt=17): 531 B(x,y v z,z) | (y v z) ^ (x v z) != y v z. [para(126(a,1),115(c,1,2)),rewrite(24(11),50(11)),xx(c)]. given #1197 (F,wt=10): 11187 B(a,d v x,c v (d v x)). [para(124(a,1),11175(a,2)),rewrite(25(7))]. given #1198 (F,wt=10): 11188 B(a,x v d,c v (x v d)). [para(126(a,1),11175(a,2)),rewrite(25(7))]. given #1199 (T,wt=10): 11192 B(a,c v (d v x),c v x). [para(124(a,1),11176(a,3)),rewrite(25(5),49(5))]. given #1200 (T,wt=10): 11193 B(a,d v (x v c),x v c). [para(126(a,1),11176(a,3)),rewrite(25(5))]. given #1201 (A,wt=14): 532 B(x v y,x v (y v z),u v (v v z)). [para(27(a,1),359(a,2))]. given #1202 (F,wt=10): 11199 B(b,e v x,d v (e v x)). [para(124(a,1),11180(a,2)),rewrite(25(7))]. given #1203 (F,wt=10): 11200 B(b,x v e,d v (x v e)). [para(126(a,1),11180(a,2)),rewrite(25(7))]. given #1204 (T,wt=10): 11204 B(b,d v (e v x),d v x). [para(124(a,1),11181(a,3)),rewrite(25(5),49(5))]. given #1205 (T,wt=10): 11205 B(b,e v (x v d),x v d). [para(126(a,1),11181(a,3)),rewrite(25(5))]. given #1206 (A,wt=20): 534 B(x,(x v y) ^ (x v z),(u v (v v y)) ^ (u v (v v z))). [para(37(a,1),359(a,2)),rewrite(37(5),37(7))]. given #1207 (F,wt=10): 11233 B(d,(x v c) ^ (a v x),x). [para(24(a,1),11161(a,2))]. given #1208 (F,wt=10): 11234 B(d,(a v x) ^ (c v x),x). [para(25(a,1),11161(a,2,2))]. given #1209 (T,wt=10): 11235 B(d,(c v x) ^ (x v a),x). [para(24(a,1),11162(a,2))]. given #1210 (T,wt=10): 11236 B(e,(x v d) ^ (b v x),x). [para(24(a,1),11163(a,2))]. given #1211 (A,wt=14): 535 B(x,y v (x v z),u v (v v (y v z))). [para(49(a,1),359(a,2))]. given #1212 (F,wt=10): 11237 B(e,(b v x) ^ (d v x),x). [para(25(a,1),11163(a,2,2))]. given #1213 (F,wt=10): 11238 B(e,(d v x) ^ (x v b),x). [para(24(a,1),11164(a,2))]. given #1214 (T,wt=10): 11241 B(a,x v d,c v (d v x)). [para(25(a,1),11187(a,2))]. given #1215 (T,wt=10): 11242 B(a,d v x,c v (x v d)). [para(25(a,1),11187(a,3,2))]. given #1216 (A,wt=14): 536 B(x,x v (y v z),u v (y v (v v z))). [para(49(a,1),359(a,3,2))]. given #1217 (F,wt=10): 11247 B(a,x v d,x v (c v d)). [para(49(a,1),11188(a,3))]. given #1218 (F,wt=10): 11248 B(a,c v (x v d),c v x). [para(25(a,1),11192(a,2,2))]. given #1219 (T,wt=10): 11249 B(a,c v (d v x),x v c). [para(25(a,1),11192(a,3))]. given #1220 (T,wt=10): 11252 B(a,d v (x v c),c v x). [para(25(a,1),11193(a,3))]. given #1221 (A,wt=14): 537 B(x,y v (z v x),u v (v v (y v z))). [para(27(a,1),364(a,2))]. given #1222 (F,wt=10): 11255 B(a,x v (c v d),x v c). [para(49(a,1),11193(a,2)),rewrite(25(4))]. given #1223 (F,wt=10): 11256 B(b,x v e,d v (e v x)). [para(25(a,1),11199(a,2))]. given #1224 (T,wt=10): 11257 B(b,e v x,d v (x v e)). [para(25(a,1),11199(a,3,2))]. given #1225 (T,wt=10): 11262 B(b,x v e,x v (d v e)). [para(49(a,1),11200(a,3))]. given #1226 (A,wt=16): 539 B(x ^ y,(z v x) ^ (z v y),u v (v v z)). [para(37(a,1),364(a,2))]. given #1227 (F,wt=10): 11263 B(b,d v (x v e),d v x). [para(25(a,1),11204(a,2,2))]. given #1228 (F,wt=10): 11264 B(b,d v (e v x),x v d). [para(25(a,1),11204(a,3))]. given #1229 (T,wt=10): 11267 B(b,e v (x v d),d v x). [para(25(a,1),11205(a,3))]. given #1230 (T,wt=10): 11270 B(b,x v (d v e),x v d). [para(49(a,1),11205(a,2)),rewrite(25(4))]. given #1231 (A,wt=20): 540 B(x,(y v x) ^ (z v x),(u v (v v y)) ^ (u v (v v z))). [para(37(a,1),364(a,3,2)),rewrite(247(2),37(7))]. given #1232 (F,wt=10): 11277 B(a,d v x,x v (c v d)). [para(49(a,1),11242(a,3))]. given #1233 (F,wt=10): 11281 B(a,c v (x v d),x v c). [para(25(a,1),11248(a,3))]. given #1234 (T,wt=10): 11283 B(a,x v (c v d),c v x). [para(49(a,1),11248(a,2))]. given #1235 (T,wt=10): 11286 B(b,e v x,x v (d v e)). [para(49(a,1),11257(a,3))]. given #1236 (A,wt=14): 541 B(x v y,x v (z v y),u v (v v z)). [para(49(a,1),364(a,2))]. given #1237 (F,wt=10): 11288 B(b,d v (x v e),x v d). [para(25(a,1),11263(a,3))]. given #1238 (F,wt=10): 11290 B(b,x v (d v e),d v x). [para(49(a,1),11263(a,2))]. given #1239 (T,wt=11): 11030 B(a v c,d,c) | c v d != d. [para(844(a,1),488(b,1,1)),rewrite(846(13))]. given #1240 (T,wt=11): 11035 B(b v d,e,d) | d v e != e. [para(876(a,1),489(b,1,1)),rewrite(878(13))]. given #1241 (A,wt=14): 542 B(x,y v (z v x),u v (y v (v v z))). [para(49(a,1),364(a,3,2)),rewrite(27(2))]. given #1242 (F,wt=11): 11104 (a v c) ^ (b v e) = b v e. [hyper(119,a,11103,a),rewrite(49(8),762(8),24(7))]. given #1243 (F,wt=6): 11307 B(c,b v e,a). [para(11104(a,1),188(b,1)),rewrite(49(18),25(23),24(24),2349(24)),xx(b),xx(c)]. given #1244 (T,wt=6): 11318 B(a,b v e,c). [para(11104(a,1),304(b,1)),rewrite(25(23),49(23),2349(24)),xx(b),xx(c)]. given #1245 (T,wt=10): 11308 B(a,(a v e) ^ (b v e),c). [para(11104(a,1),256(b,1,2)),rewrite(25(32),2355(34)),xx(b),xx(c)]. given #1246 (A,wt=17): 543 (x v (y v z)) ^ (y v (x v z)) = y v (x v z). [hyper(33,a,395,a),rewrite(49(4),49(3),27(2),124(3),190(3),25(5),218(5))]. given #1247 (F,wt=11): 11140 B(a,b ^ c,b) | b ^ c != b. [para(151(a,1),523(c,1,2)),rewrite(24(4),50(12),24(9),24(12),104(20),100(19),24(18),106(18),24(17)),flip(c),xx(b)]. given #1248 (F,wt=12): 2285 B(x,d v x,y v (z v (a v c))). [para(27(a,1),2272(a,3))]. given #1249 (T,wt=12): 2288 B(x,y v (z v x),z v (u v y)). [para(25(a,1),349(a,3)),rewrite(27(4))]. given #1250 (T,wt=12): 2293 B(x,y v (z v x),z v (y v u)). [para(49(a,1),349(a,2))]. given #1251 (A,wt=14): 544 B(x v (y v z),z v (x v (y v u)),u). [para(27(a,1),395(a,1)),rewrite(27(4))]. given #1252 (F,wt=12): 2303 B(d,a v c,a v (x v (c v y))). [para(49(a,1),2297(a,3,2))]. given #1253 (F,wt=12): 2304 B(d,a v c,a v (x v (y v c))). [para(218(a,1),2297(a,3,2))]. given #1254 (T,wt=12): 2308 B(e,b v d,b v (x v (d v y))). [para(49(a,1),2299(a,3,2))]. given #1255 (T,wt=12): 2309 B(e,b v d,b v (x v (y v d))). [para(218(a,1),2299(a,3,2))]. given #1256 (A,wt=14): 545 B(x v (y v z),y v (z v (x v u)),u). [para(27(a,1),395(a,2))]. given #1257 (F,wt=8): 11352 B(e,b v d,a v c). [para(844(a,1),2309(a,3,2)),rewrite(49(9),762(9))]. given #1258 (F,wt=12): 2328 B(d,a v c,c v (x v (y v a))). [para(27(a,1),2305(a,3,2))]. given #1259 (T,wt=12): 2330 B(e,b v d,d v (x v (y v b))). [para(27(a,1),2310(a,3,2))]. given #1260 (T,wt=12): 2336 B(x,x v e,b v (y v (d v z))). [para(49(a,1),2311(a,3,2))]. given #1261 (A,wt=20): 546 B((x v y) ^ (x v z),(y v (x v u)) ^ (z v (x v u)),u). [para(37(a,1),395(a,1)),rewrite(247(6))]. given #1262 (F,wt=12): 2337 B(x,x v e,b v (y v (z v d))). [para(218(a,1),2311(a,3,2))]. given #1263 (F,wt=8): 11363 B(x,x v e,a v c). [para(844(a,1),2337(a,3,2)),rewrite(49(7),762(7))]. given #1264 (T,wt=8): 11364 B(x,e v x,a v c). [para(25(a,1),11363(a,2))]. given #1265 (T,wt=12): 2339 B(d,a v c,x v (y v (a v c))). [para(27(a,1),2327(a,3))]. given #1266 (A,wt=18): 547 B(x v y,(y v (x v z)) ^ (y v (x v u)),z ^ u). [para(37(a,1),395(a,2,2)),rewrite(37(5))]. given #1267 (F,wt=12): 2340 B(e,b v d,x v (y v (b v d))). [para(27(a,1),2329(a,3))]. given #1268 (F,wt=12): 2346 B(x,e v x,b v (y v (d v z))). [para(49(a,1),2332(a,3,2))]. given #1269 (T,wt=12): 2347 B(x,e v x,b v (y v (z v d))). [para(218(a,1),2332(a,3,2))]. given #1270 (T,wt=12): 2363 B(x ^ y,(x v z) ^ (y v z),z). [para(247(a,1),307(a,2))]. given #1271 (A,wt=14): 548 B(x v (y v z),x v (z v (y v u)),u). [para(49(a,1),395(a,1)),rewrite(27(5))]. given #1272 (F,wt=8): 11376 B(a ^ b,b v c,c). [para(764(a,1),2363(a,2))]. given #1273 (F,wt=12): 2364 B(x,(y v x) ^ (z v x),y ^ z). [para(247(a,1),333(a,2))]. given #1274 (T,wt=8): 11377 B(c,b v c,a ^ b). [para(764(a,1),2364(a,2))]. given #1275 (T,wt=12): 2368 B(x,x v y,(z v y) ^ (u v y)). [para(247(a,1),341(a,3))]. given #1276 (A,wt=14): 549 B(x v y,y v (z v (x v u)),z v u). [para(49(a,1),395(a,2,2))]. given #1277 (F,wt=12): 2369 B(x,y v x,(z v y) ^ (u v y)). [para(247(a,1),348(a,3))]. given #1278 (F,wt=12): 2390 B((x v y) ^ (z v y),y v u,u). [para(247(a,1),465(a,1))]. given #1279 (T,wt=12): 2392 B((x v y) ^ (z v y),u v y,u). [para(247(a,1),495(a,1))]. given #1280 (T,wt=12): 2625 B(x,x v e,d v (y v (z v b))). [para(27(a,1),2338(a,3,2))]. given #1281 (A,wt=14): 550 B(x v (y v z),z v (u v (x v y)),u). [para(27(a,1),396(a,1))]. given #1282 (F,wt=12): 2634 B(x,e v x,d v (y v (z v b))). [para(27(a,1),2348(a,3,2))]. given #1283 (F,wt=12): 2732 B(x,x v e,y v (z v (b v d))). [para(27(a,1),2621(a,3))]. given #1284 (T,wt=12): 2798 B(x,e v x,y v (z v (b v d))). [para(27(a,1),2631(a,3))]. given #1285 (T,wt=12): 2806 B(x,(x v y) ^ (z v (u v y)),y). [para(27(a,1),2670(a,2,2))]. given #1286 (A,wt=14): 551 B(x v y,y v (z v (u v x)),z v u). [para(27(a,1),396(a,2,2))]. given #1287 (F,wt=10): 11397 B(x,(x v d) ^ (a v c),d). [para(844(a,1),2806(a,2,2))]. given #1288 (F,wt=10): 11398 B(x,(x v e) ^ (b v d),e). [para(876(a,1),2806(a,2,2))]. given #1289 (T,wt=10): 11400 B(x,(a v c) ^ (x v d),d). [para(24(a,1),11397(a,2))]. given #1290 (T,wt=10): 11401 B(x,(a v c) ^ (d v x),d). [para(25(a,1),11397(a,2,1)),rewrite(24(6))]. given #1291 (A,wt=14): 552 B(x v (y v z),y v (z v (u v x)),u). [para(27(a,1),396(a,2))]. given #1292 (F,wt=10): 11403 B(x,(b v d) ^ (x v e),e). [para(24(a,1),11398(a,2))]. given #1293 (F,wt=10): 11404 B(x,(b v d) ^ (e v x),e). [para(25(a,1),11398(a,2,1)),rewrite(24(6))]. given #1294 (T,wt=12): 2820 B(x,(y v (z v u)) ^ (x v u),u). [para(27(a,1),2802(a,2,1))]. given #1295 (T,wt=12): 3156 B(x,x ^ y,(z v (x v u)) ^ y). [para(147(a,1),2869(a,2))]. given #1296 (A,wt=20): 553 B((x v y) ^ (x v z),(y v (u v x)) ^ (z v (u v x)),u). [para(37(a,1),396(a,1)),rewrite(247(6))]. given #1297 (F,wt=12): 3157 B(a v b,b ^ x,(b v c) ^ x). [para(151(a,1),2869(a,2))]. given #1298 (F,wt=12): 3160 B(a v b,x ^ b,x ^ (b v c)). [para(154(a,1),2869(a,2))]. given #1299 (T,wt=12): 3161 B(a v d,d ^ x,(c v d) ^ x). [para(156(a,1),2869(a,2))]. given #1300 (T,wt=12): 3164 B(a v d,x ^ d,x ^ (c v d)). [para(159(a,1),2869(a,2))]. given #1301 (A,wt=20): 554 B((x v y) ^ (z v y),(y v (u v x)) ^ (y v (u v z)),u). [para(37(a,1),396(a,2,2)),rewrite(247(2),37(7))]. given #1302 (F,wt=12): 3165 B(b v e,e ^ x,(d v e) ^ x). [para(161(