============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11449 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:20 2006 The command was "/home/mccune/bin/prover9 -f head.in cd.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 cd.in formulas(goals). (all a all x all b (C(a,x,b) -> D(a,x,b))). 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]. 7 (all a all x all b (C(a,x,b) -> D(a,x,b))). [goal]. ============================== 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)]. C(c1,c2,c3). [deny(7)]. -D(c1,c2,c3). [deny(7)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating A/3 8 A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. 9 -A(x,y,z) | x <= y | z <= y. [clausify(1)]. 10 -A(x,y,z) | x <= y | y <= x. [clausify(1)]. 11 -A(x,y,z) | y <= z | z <= y. [clausify(1)]. 12 -A(x,y,z) | y <= z | y <= x. [clausify(1)]. 13 A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. Eliminating B/3 14 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 15 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. 16 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. Eliminating C/3 17 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 18 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 19 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. 20 C(c1,c2,c3). [deny(7)]. Derived: (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(20,a,18,a)]. Derived: (c1 ^ c3) v c2 = c2. [resolve(20,a,19,a)]. Eliminating CS/3 21 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 22 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 23 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ <=, D, =, CS, C, B, A ]). Function symbol precedence: lex([ c1, c2, c3, ^, v ]). After inverse_order: (no changes). Auto_process settings: (no changes). % Operation ^ is commutative; C redundancy checks enabled. % Operation v is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 25 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 32 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 33 -D(x,y,z) | y <= x v z. [clausify(5)]. 34 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. 35 -(x <= y) | x ^ y = x. [clausify(6)]. 36 x <= y | x ^ y != x. [clausify(6)]. 37 -D(c1,c2,c3). [deny(7)]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(20,a,18,a)]. 40 c2 v (c1 ^ c3) = c2. [copy(39),rewrite(25(5))]. end_of_list. formulas(demodulators). 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 25 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(20,a,18,a)]. 40 c2 v (c1 ^ c3) = c2. [copy(39),rewrite(25(5))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. given #2 (I,wt=7): 25 x v y = y v x # label("commutativity_join"). [assumption]. given #3 (I,wt=11): 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 41 x ^ (y ^ z) = z ^ (x ^ y). [para(26(a,1),24(a,1))]. given #4 (I,wt=11): 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 43 x v (y v z) = z v (x v y). [para(27(a,1),25(a,1))]. given #5 (I,wt=7): 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. given #6 (I,wt=7): 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. given #7 (I,wt=9): 32 -D(x,y,z) | x ^ z <= y. [clausify(5)]. given #8 (I,wt=9): 33 -D(x,y,z) | y <= x v z. [clausify(5)]. given #9 (I,wt=14): 34 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. given #10 (I,wt=8): 35 -(x <= y) | x ^ y = x. [clausify(6)]. given #11 (I,wt=8): 36 x <= y | x ^ y != x. [clausify(6)]. given #12 (I,wt=4): 37 -D(c1,c2,c3). [deny(7)]. given #13 (I,wt=9): 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(20,a,18,a)]. given #14 (I,wt=7): 40 c2 v (c1 ^ c3) = c2. [copy(39),rewrite(25(5))]. given #15 (T,wt=5): 53 x ^ x = x. [para(31(a,1),29(a,1,2))]. given #16 (A,wt=11): 42 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. given #17 (F,wt=3): 70 x <= x. [hyper(36,b,53,a)]. given #18 (F,wt=5): 54 x v x = x. [para(29(a,1),31(a,1,2))]. given #19 (T,wt=5): 61 x <= x v y. [hyper(36,b,29,a)]. given #20 (T,wt=5): 85 x <= y v x. [para(25(a,1),61(a,2))]. given #21 (A,wt=11): 44 x v (y v z) = y v (x v z). [para(25(a,1),27(a,1,1)),rewrite(27(2))]. given #22 (F,wt=5): 87 c1 ^ c2 <= c2. [para(38(a,1),61(a,2))]. given #23 (F,wt=4): 98 D(c1,c2,c2). [hyper(34,b,87,a,c,85,a)]. given #24 (T,wt=5): 89 x ^ y <= x. [para(31(a,1),85(a,2))]. given #25 (T,wt=4): 100 D(x,x,y). [hyper(34,b,89,a,c,61,a)]. given #26 (A,wt=7): 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. given #27 (F,wt=5): 90 c1 ^ c3 <= c2. [para(40(a,1),85(a,2))]. given #28 (F,wt=5): 101 x ^ y <= y. [para(24(a,1),89(a,1))]. given #29 (T,wt=4): 113 D(x,y,y). [hyper(34,b,101,a,c,85,a)]. given #30 (T,wt=7): 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. given #31 (A,wt=11): 46 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. given #32 (F,wt=7): 88 x <= y v (z v x). [para(27(a,1),85(a,2))]. given #33 (F,wt=7): 96 x <= y v (x v z). [para(44(a,1),61(a,2))]. given #34 (T,wt=7): 103 x ^ (y ^ z) <= y. [para(42(a,1),89(a,1))]. given #35 (T,wt=7): 114 x ^ (y ^ z) <= z. [para(26(a,1),101(a,1))]. given #36 (A,wt=13): 47 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(29(a,1),26(a,1)),flip(a)]. given #37 (F,wt=7): 131 x ^ y <= z v x. [para(31(a,1),88(a,2,2))]. given #38 (F,wt=7): 132 c1 ^ c3 <= x v c2. [para(40(a,1),88(a,2,2))]. given #39 (T,wt=7): 134 x ^ y <= z v y. [para(49(a,1),88(a,2,2))]. given #40 (T,wt=6): 167 D(x,x ^ y,y). [hyper(34,b,70,a,c,134,a)]. given #41 (A,wt=13): 48 (x v y) ^ (x v (y v z)) = x v y. [para(27(a,1),29(a,1,2))]. given #42 (F,wt=6): 168 D(x,x v y,y). [hyper(34,b,134,a,c,70,a)]. given #43 (F,wt=6): 176 D(x,y ^ x,y). [para(24(a,1),167(a,2))]. given #44 (T,wt=6): 192 D(x,y v x,y). [para(25(a,1),168(a,2))]. given #45 (T,wt=7): 140 x ^ y <= x v z. [para(46(a,1),103(a,1))]. given #46 (A,wt=13): 50 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(26(a,1),31(a,1,2))]. given #47 (F,wt=7): 143 x ^ y <= y v z. [para(29(a,1),114(a,1,2))]. given #48 (F,wt=7): 161 c1 ^ (c3 ^ x) <= c2. [para(40(a,1),131(a,2)),rewrite(26(4))]. given #49 (T,wt=7): 165 c1 ^ c3 <= c2 v x. [para(25(a,1),132(a,2))]. given #50 (T,wt=7): 171 x ^ (c1 ^ c3) <= c2. [para(40(a,1),134(a,2))]. given #51 (A,wt=11): 51 x v ((x ^ y) v z) = x v z. [para(31(a,1),27(a,1,1)),flip(a)]. given #52 (F,wt=7): 196 x ^ y <= y ^ x. [hyper(32,a,176,a)]. given #53 (F,wt=7): 201 x v y <= y v x. [hyper(33,a,192,a)]. given #54 (T,wt=7): 229 c1 ^ (x ^ c3) <= c2. [para(24(a,1),161(a,1,2))]. given #55 (T,wt=8): 62 x <= y | y ^ x != x. [para(24(a,1),36(b,1))]. given #56 (A,wt=13): 52 x v (y v ((x v y) ^ z)) = x v y. [para(31(a,1),27(a,1)),flip(a)]. given #57 (F,wt=8): 194 D(c1 ^ c2,c2,c2 ^ c3). [para(38(a,1),168(a,2))]. given #58 (F,wt=8): 203 D(c2 ^ c3,c2,c1 ^ c2). [para(38(a,1),192(a,2))]. given #59 (T,wt=9): 71 x ^ (x ^ y) = x ^ y. [para(53(a,1),26(a,1,1)),flip(a)]. given #60 (T,wt=9): 73 x ^ (y ^ x) = y ^ x. [para(53(a,1),26(a,2,2)),rewrite(24(2))]. given #61 (A,wt=14): 55 D(x,y,z) | -(z ^ x <= y) | -(y <= x v z). [para(24(a,1),34(b,1))]. given #62 (F,wt=8): 283 D(c1 ^ c3,c2,c2 v x). [hyper(55,b,171,a,c,96,a)]. given #63 (F,wt=8): 284 D(c1 ^ c3,c2,x v c2). [hyper(55,b,171,a,c,88,a)]. given #64 (T,wt=8): 288 D(x ^ y,y,y v z). [hyper(55,b,114,a,c,96,a)]. given #65 (T,wt=8): 289 D(x ^ y,y,z v y). [hyper(55,b,114,a,c,88,a)]. given #66 (A,wt=14): 56 D(x,y,z) | -(x ^ z <= y) | -(y <= z v x). [para(25(a,1),34(c,2))]. given #67 (F,wt=8): 293 D(x ^ y,x,x v z). [hyper(55,b,103,a,c,96,a)]. given #68 (F,wt=8): 294 D(x ^ y,x,z v x). [hyper(55,b,103,a,c,88,a)]. given #69 (T,wt=8): 326 D(c2 v x,c2,c1 ^ c3). [hyper(56,b,171,a,c,96,a)]. given #70 (T,wt=8): 327 D(x v c2,c2,c1 ^ c3). [hyper(56,b,171,a,c,88,a)]. given #71 (A,wt=20): 57 D(x ^ y,z,u) | -(x ^ (y ^ u) <= z) | -(z <= (x ^ y) v u). [para(26(a,1),34(b,1))]. given #72 (F,wt=8): 332 D(x v y,x,z ^ x). [hyper(56,b,114,a,c,96,a)]. given #73 (F,wt=8): 333 D(x v y,y,z ^ y). [hyper(56,b,114,a,c,88,a)]. given #74 (T,wt=8): 334 D(x v y,x,x ^ z). [hyper(56,b,103,a,c,96,a)]. given #75 (T,wt=8): 335 D(x v y,y,y ^ z). [hyper(56,b,103,a,c,88,a)]. given #76 (A,wt=20): 58 D(x v y,z,u) | -((x v y) ^ u <= z) | -(z <= x v (y v u)). [para(27(a,1),34(c,2))]. given #77 (F,wt=8): 363 D(x ^ y,y ^ z,z). [hyper(57,b,101,a,c,134,a)]. given #78 (F,wt=8): 410 D(x v y,y v z,z). [hyper(58,b,134,a,c,85,a)]. given #79 (T,wt=8): 434 D(x ^ y,x ^ z,z). [para(24(a,1),363(a,1))]. given #80 (T,wt=8): 435 D(x ^ y,z ^ y,z). [para(24(a,1),363(a,2))]. given #81 (A,wt=14): 63 x ^ y <= z | x ^ (y ^ z) != x ^ y. [para(26(a,1),36(b,1))]. given #82 (F,wt=8): 438 D(x,(x v y) ^ z,z). [para(29(a,1),363(a,1))]. given #83 (F,wt=8): 441 D(x,(y v x) ^ z,z). [para(45(a,1),363(a,1))]. given #84 (T,wt=8): 447 D(x v y,x v z,z). [para(25(a,1),410(a,1))]. given #85 (T,wt=8): 448 D(x v y,z v y,z). [para(25(a,1),410(a,2))]. given #86 (A,wt=13): 64 (c1 ^ c2) v ((c2 ^ c3) v x) = c2 v x. [para(38(a,1),27(a,1,1)),flip(a)]. given #87 (F,wt=8): 451 D(x,(x ^ y) v z,z). [para(31(a,1),410(a,1))]. given #88 (F,wt=6): 538 D(c1,c2,c2 ^ c3). [para(38(a,1),451(a,2))]. given #89 (T,wt=8): 453 D(c2,(c1 ^ c3) v x,x). [para(40(a,1),410(a,1))]. given #90 (T,wt=8): 456 D(x,(y ^ x) v z,z). [para(49(a,1),410(a,1))]. given #91 (A,wt=13): 65 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(38(a,1),27(a,2,2)),rewrite(25(8))]. given #92 (F,wt=8): 462 D(x ^ y,z ^ x,z). [para(24(a,1),434(a,2))]. given #93 (F,wt=8): 471 D(x,y ^ (x v z),y). [para(29(a,1),435(a,1))]. given #94 (T,wt=8): 474 D(x,y ^ (z v x),y). [para(45(a,1),435(a,1))]. given #95 (T,wt=8): 495 D(c1 ^ c3,c2 ^ x,x). [para(40(a,1),441(a,2,1))]. given #96 (A,wt=11): 67 c2 v ((c1 ^ c3) v x) = c2 v x. [para(40(a,1),27(a,1,1)),flip(a)]. given #97 (F,wt=8): 502 D(x v y,z v x,z). [para(25(a,1),447(a,2))]. given #98 (F,wt=8): 512 D(x,y v (x ^ z),y). [para(31(a,1),448(a,1))]. given #99 (T,wt=8): 514 D(c2,x v (c1 ^ c3),x). [para(40(a,1),448(a,1))]. given #100 (T,wt=8): 517 D(x,y v (z ^ x),y). [para(49(a,1),448(a,1))]. given #101 (A,wt=11): 68 (c1 ^ c3) v (x v c2) = x v c2. [para(40(a,1),27(a,2,2)),rewrite(25(6))]. given #102 (F,wt=6): 652 D(c3,c2,c1 ^ c2). [para(38(a,1),517(a,2))]. given #103 (F,wt=7): 675 c2 <= c3 v (c1 ^ c2). [hyper(33,a,652,a)]. given #104 (T,wt=8): 601 D(c1 ^ c3,x ^ c2,x). [para(40(a,1),474(a,2,2))]. given #105 (T,wt=9): 78 x v (y ^ (x ^ z)) = x. [para(42(a,1),31(a,1,2))]. given #106 (A,wt=10): 74 D(x,y,x) | -(x <= y) | -(y <= x). [para(53(a,1),34(b,1)),rewrite(54(3))]. given #107 (F,wt=9): 81 x v (x v y) = x v y. [para(54(a,1),27(a,1,1)),flip(a)]. given #108 (F,wt=9): 83 x v (y v x) = y v x. [para(54(a,1),27(a,2,2)),rewrite(25(2))]. given #109 (T,wt=9): 86 x v y <= x v (y v z). [para(27(a,1),61(a,2))]. given #110 (T,wt=8): 704 D(x,x v y,y v z). [hyper(55,b,143,a,c,86,a)]. given #111 (A,wt=14): 76 D(x,y,x ^ z) | -(x ^ z <= y) | -(y <= x). [back_rewrite(60),rewrite(71(4))]. given #112 (F,wt=8): 714 D(x,y v x,y v z). [para(25(a,1),704(a,2))]. given #113 (F,wt=8): 715 D(x,x v y,z v y). [para(25(a,1),704(a,3))]. given #114 (T,wt=8): 728 D(x,y ^ x,x ^ y). [hyper(76,b,196,a,c,101,a)]. given #115 (T,wt=8): 766 D(x,y v x,z v y). [para(25(a,1),714(a,3))]. given #116 (A,wt=11): 77 x ^ (y ^ (x v z)) = y ^ x. [para(29(a,1),42(a,1,2)),flip(a)]. given #117 (F,wt=8): 782 D(x,x v (y ^ z),y). [para(31(a,1),715(a,3))]. given #118 (F,wt=8): 784 D(x,x v (c1 ^ c3),c2). [para(40(a,1),715(a,3))]. given #119 (T,wt=8): 787 D(x,x v (y ^ z),z). [para(49(a,1),715(a,3))]. given #120 (T,wt=6): 859 D(c1 ^ c2,c2,c3). [para(38(a,1),787(a,2))]. given #121 (A,wt=20): 79 D(x,y,z ^ u) | -(z ^ (x ^ u) <= y) | -(y <= x v (z ^ u)). [para(42(a,1),34(b,1))]. given #122 (F,wt=8): 803 D(x,(y ^ z) v x,y). [para(31(a,1),766(a,3))]. given #123 (F,wt=6): 878 D(c2 ^ c3,c2,c1). [para(38(a,1),803(a,2))]. given #124 (T,wt=8): 805 D(x,(c1 ^ c3) v x,c2). [para(40(a,1),766(a,3))]. given #125 (T,wt=8): 808 D(x,(y ^ z) v x,z). [para(49(a,1),766(a,3))]. given #126 (A,wt=12): 80 x <= y ^ z | y ^ (x ^ z) != x. [para(42(a,1),36(b,1))]. given #127 (F,wt=8): 864 D(x,x ^ y,z ^ y). [hyper(79,b,101,a,c,140,a)]. given #128 (F,wt=8): 910 D(x,y ^ x,z ^ y). [para(24(a,1),864(a,2))]. given #129 (T,wt=8): 911 D(x,x ^ y,y ^ z). [para(24(a,1),864(a,3))]. given #130 (T,wt=8): 914 D(x,x ^ (y v z),y). [para(29(a,1),864(a,3))]. given #131 (A,wt=14): 84 D(x,y,x v z) | -(x <= y) | -(y <= x v z). [back_rewrite(59),rewrite(81(5))]. given #132 (F,wt=8): 917 D(x,x ^ (y v z),z). [para(45(a,1),864(a,3))]. given #133 (F,wt=8): 924 D(x,y ^ x,y ^ z). [para(24(a,1),910(a,3))]. given #134 (T,wt=8): 927 D(x,(y v z) ^ x,y). [para(29(a,1),910(a,3))]. given #135 (T,wt=8): 930 D(x,(y v z) ^ x,z). [para(45(a,1),910(a,3))]. given #136 (A,wt=9): 91 x ^ (y v (x v z)) = x. [para(44(a,1),29(a,1,2))]. given #137 (F,wt=8): 988 D(x,x ^ c2,c1 ^ c3). [para(40(a,1),917(a,2,2))]. given #138 (F,wt=8): 1012 D(x,c2 ^ x,c1 ^ c3). [para(40(a,1),930(a,2,1))]. given #139 (T,wt=9): 97 x v y <= x v (z v y). [para(44(a,1),85(a,2))]. given #140 (T,wt=9): 102 x ^ (y ^ z) <= x ^ y. [para(26(a,1),89(a,1))]. given #141 (A,wt=11): 92 x v (y v (x ^ z)) = y v x. [para(31(a,1),44(a,1,2)),flip(a)]. given #142 (F,wt=9): 106 x ^ (y v (z v x)) = x. [para(27(a,1),45(a,1,2))]. given #143 (F,wt=9): 108 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(40(a,1),45(a,1,2)),rewrite(24(5),42(5))]. given #144 (T,wt=7): 1124 c1 ^ c3 <= c2 ^ c3. [para(108(a,1),101(a,1))]. given #145 (T,wt=6): 1159 D(c1,c2 ^ c3,c3). [hyper(56,b,1124,a,c,143,a)]. given #146 (A,wt=20): 93 D(x,y,z v u) | -(x ^ (z v u) <= y) | -(y <= z v (x v u)). [para(44(a,1),34(c,2))]. given #147 (F,wt=6): 1160 D(c3,c2 ^ c3,c1). [hyper(55,b,1124,a,c,143,a)]. given #148 (F,wt=7): 1155 c1 ^ c3 <= c1 ^ c2. [para(108(a,1),102(a,1))]. given #149 (T,wt=6): 1185 D(c1,c1 ^ c2,c3). [hyper(56,b,1155,a,c,131,a)]. given #150 (T,wt=6): 1186 D(c3,c1 ^ c2,c1). [hyper(55,b,1155,a,c,131,a)]. given #151 (A,wt=13): 94 (c1 ^ c2) v (x v (c2 ^ c3)) = x v c2. [para(38(a,1),44(a,1,2)),flip(a)]. given #152 (F,wt=9): 115 x ^ (y ^ z) <= x ^ z. [para(42(a,1),101(a,1))]. given #153 (F,wt=9): 116 x v (y ^ (z ^ x)) = x. [para(26(a,1),49(a,1,2))]. given #154 (T,wt=9): 128 x ^ y <= (x v z) ^ y. [para(46(a,1),101(a,1))]. given #155 (T,wt=9): 130 x <= y v (z v (u v x)). [para(27(a,1),88(a,2,2))]. given #156 (A,wt=11): 95 c2 v (x v (c1 ^ c3)) = x v c2. [para(40(a,1),44(a,1,2)),flip(a)]. given #157 (F,wt=9): 136 x <= y v (z v (x v u)). [para(27(a,1),96(a,2))]. given #158 (F,wt=9): 139 x ^ (y ^ (z ^ u)) <= z. [para(26(a,1),103(a,1))]. given #159 (T,wt=9): 142 x ^ (y ^ (z ^ u)) <= u. [para(26(a,1),114(a,1,2))]. given #160 (T,wt=9): 160 x ^ y <= z v (u v x). [para(27(a,1),131(a,2))]. given #161 (A,wt=11): 104 x ^ ((y v x) ^ z) = x ^ z. [para(45(a,1),26(a,1,1)),flip(a)]. given #162 (F,wt=9): 162 x ^ (y ^ z) <= u v y. [para(42(a,1),131(a,1))]. given #163 (F,wt=9): 166 c1 ^ c3 <= x v (y v c2). [para(27(a,1),132(a,2))]. given #164 (T,wt=9): 169 x ^ (y ^ z) <= u v z. [para(26(a,1),134(a,1))]. given #165 (T,wt=9): 170 x ^ y <= z v (u v y). [para(27(a,1),134(a,2))]. given #166 (A,wt=13): 105 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(45(a,1),26(a,1)),flip(a)]. given #167 (F,wt=9): 211 x ^ (y ^ z) <= y v u. [para(42(a,1),140(a,1))]. given #168 (F,wt=9): 212 x ^ y <= z v (x v u). [para(44(a,1),140(a,2))]. given #169 (T,wt=9): 223 x ^ (y ^ z) <= z v u. [para(26(a,1),143(a,1))]. given #170 (T,wt=9): 225 x ^ y <= z v (y v u). [para(44(a,1),143(a,2))]. given #171 (A,wt=14): 107 D(x,y,z v x) | -(x <= y) | -(y <= z v x). [para(45(a,1),34(b,1)),rewrite(83(5))]. given #172 (F,wt=9): 230 c1 ^ (x ^ (c3 ^ y)) <= c2. [para(42(a,1),161(a,1,2))]. given #173 (F,wt=9): 234 c1 ^ c3 <= x v (c2 v y). [para(44(a,1),165(a,2))]. given #174 (T,wt=9): 236 x ^ (y ^ (c1 ^ c3)) <= c2. [para(26(a,1),171(a,1))]. given #175 (T,wt=9): 239 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),51(a,1,2)),flip(a)]. given #176 (A,wt=11): 109 x ^ (y ^ (z v x)) = y ^ x. [para(45(a,1),42(a,1,2)),flip(a)]. given #177 (F,wt=6): 2061 D(c3,c1 v c2,c1). [para(239(a,1),517(a,2))]. given #178 (F,wt=6): 2066 D(c1,c1 v c2,c3). [para(239(a,1),787(a,2))]. given #179 (T,wt=7): 2119 c1 v c2 <= c1 v c3. [hyper(33,a,2061,a),rewrite(25(6))]. given #180 (T,wt=8): 2054 D(c1,c1 v c2,c2 ^ c3). [para(239(a,1),168(a,2))]. given #181 (A,wt=13): 110 (x v y) ^ (x v (z v y)) = x v y. [para(44(a,1),45(a,1,2))]. given #182 (F,wt=8): 2055 D(c2 ^ c3,c1 v c2,c1). [para(239(a,1),192(a,2))]. given #183 (F,wt=8): 2121 D(c1,c1 v c2,c1 v c3). [hyper(84,b,61,a,c,2119,a)]. given #184 (T,wt=8): 2130 D(c1 v c3,c1 v c2,c1). [hyper(76,b,143,a,c,2119,a),rewrite(24(11),29(11))]. given #185 (T,wt=9): 241 (x ^ y) v z <= x v z. [para(51(a,1),85(a,2))]. given #186 (A,wt=16): 111 D(c1 ^ c2,x,c2 ^ c3) | -(c1 ^ c3 <= x) | -(x <= c2). [back_rewrite(75),rewrite(108(12))]. given #187 (F,wt=9): 257 c1 ^ (x ^ (y ^ c3)) <= c2. [para(26(a,1),229(a,1,2))]. given #188 (F,wt=9): 468 x ^ (y ^ z) <= z ^ y. [hyper(32,a,435,a),rewrite(26(2))]. given #189 (T,wt=9): 493 x ^ y <= (z v x) ^ y. [hyper(32,a,441,a)]. given #190 (T,wt=9): 509 x v y <= z v (y v x). [hyper(33,a,448,a),rewrite(27(3))]. given #191 (A,wt=14): 112 D(c2,x,c1 ^ c3) | -(c1 ^ c3 <= x) | -(x <= c2). [back_rewrite(69),rewrite(108(10))]. given #192 (F,wt=9): 544 (c1 ^ c3) v x <= c2 v x. [hyper(33,a,453,a)]. given #193 (F,wt=9): 548 (x ^ y) v z <= y v z. [hyper(33,a,456,a)]. given #194 (T,wt=9): 588 x ^ (y ^ z) <= z ^ x. [hyper(32,a,462,a),rewrite(26(2))]. given #195 (T,wt=9): 593 x ^ y <= y ^ (x v z). [hyper(32,a,471,a)]. given #196 (A,wt=11): 117 x v ((y ^ x) v z) = x v z. [para(49(a,1),27(a,1,1)),flip(a)]. given #197 (F,wt=9): 598 x ^ y <= y ^ (z v x). [hyper(32,a,474,a)]. given #198 (F,wt=9): 606 c1 ^ (c3 ^ x) <= c2 ^ x. [hyper(32,a,495,a),rewrite(26(4))]. given #199 (T,wt=9): 611 c2 v (c1 ^ (c3 ^ x)) = c2. [para(31(a,1),67(a,1,2)),rewrite(40(5),26(6)),flip(a)]. given #200 (T,wt=9): 615 c2 v (x ^ (c1 ^ c3)) = c2. [para(49(a,1),67(a,1,2)),rewrite(40(5)),flip(a)]. given #201 (A,wt=13): 118 x v (y v (z ^ (x v y))) = x v y. [para(49(a,1),27(a,1)),flip(a)]. given #202 (F,wt=9): 634 x v y <= y v (z v x). [hyper(33,a,502,a),rewrite(27(3))]. given #203 (F,wt=9): 644 x v (y ^ z) <= y v x. [hyper(33,a,512,a)]. given #204 (T,wt=9): 647 x v (c1 ^ c3) <= c2 v x. [hyper(33,a,514,a)]. given #205 (T,wt=9): 649 x v (y ^ z) <= z v x. [hyper(33,a,517,a)]. given #206 (A,wt=14): 119 D(x,y,z ^ x) | -(z ^ x <= y) | -(y <= x). [para(49(a,1),34(c,2)),rewrite(73(4))]. given #207 (F,wt=9): 661 c1 ^ (c3 ^ x) <= y v c2. [para(68(a,1),140(a,2)),rewrite(26(4))]. given #208 (F,wt=9): 662 x ^ (c1 ^ c3) <= y v c2. [para(68(a,1),143(a,2))]. given #209 (T,wt=9): 677 c1 ^ (c3 ^ x) <= x ^ c2. [hyper(32,a,601,a),rewrite(26(4))]. given #210 (T,wt=9): 705 x v y <= y v (x v z). [para(25(a,1),86(a,1))]. given #211 (A,wt=13): 120 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(42(a,1),49(a,1,2))]. given #212 (F,wt=9): 713 (c1 ^ c3) v x <= x v c2. [para(68(a,1),86(a,2))]. given #213 (F,wt=9): 825 x ^ y <= x ^ (y v z). [para(77(a,1),101(a,1))]. given #214 (T,wt=9): 852 x v (y ^ z) <= x v y. [hyper(33,a,782,a)]. given #215 (T,wt=9): 854 x v (c1 ^ c3) <= x v c2. [hyper(33,a,784,a)]. given #216 (A,wt=11): 121 x v (y v (z ^ x)) = y v x. [para(49(a,1),44(a,1,2)),flip(a)]. given #217 (F,wt=9): 856 x v (y ^ z) <= x v z. [hyper(33,a,787,a)]. given #218 (F,wt=9): 877 (x ^ y) v z <= z v x. [hyper(33,a,803,a)]. given #219 (T,wt=9): 888 (x ^ y) v z <= z v y. [hyper(33,a,808,a)]. given #220 (T,wt=9): 985 x ^ y <= x ^ (z v y). [hyper(32,a,917,a)]. given #221 (A,wt=17): 122 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(46(a,1),26(a,1)),rewrite(26(2)),flip(a)]. given #222 (F,wt=9): 994 x ^ (y ^ z) <= y ^ x. [hyper(32,a,924,a)]. given #223 (F,wt=9): 1001 x ^ y <= (y v z) ^ x. [hyper(32,a,927,a)]. given #224 (T,wt=9): 1010 x ^ y <= (z v y) ^ x. [hyper(32,a,930,a)]. given #225 (T,wt=9): 1038 x ^ (c1 ^ c3) <= x ^ c2. [hyper(32,a,988,a)]. given #226 (A,wt=17): 123 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(27(a,1),46(a,1,2,1))]. given #227 (F,wt=9): 1040 x ^ (c1 ^ c3) <= c2 ^ x. [hyper(32,a,1012,a)]. given #228 (F,wt=9): 1126 x ^ (c1 ^ c3) <= c2 ^ c3. [para(108(a,1),114(a,1,2))]. given #229 (T,wt=8): 3703 D(x ^ c1,c2 ^ c3,c3). [hyper(57,b,1126,a,c,134,a)]. given #230 (T,wt=8): 3711 D(c1 ^ x,c2 ^ c3,c3). [para(24(a,1),3703(a,1))]. given #231 (A,wt=22): 124 D(x,y,(x v z) ^ u) | -(x ^ u <= y) | -(y <= x v ((x v z) ^ u)). [para(46(a,1),34(b,1))]. given #232 (F,wt=9): 1127 c1 ^ c3 <= x v (c2 ^ c3). [para(108(a,1),134(a,1))]. given #233 (F,wt=9): 1129 c1 ^ c3 <= (c2 ^ c3) v x. [para(108(a,1),143(a,1))]. given #234 (T,wt=9): 1188 c3 v (c1 ^ c2) = c2 v c3. [para(49(a,1),94(a,1,2)),rewrite(25(5),25(8))]. given #235 (T,wt=6): 3807 D(c1,c2 v c3,c3). [para(1188(a,1),512(a,2))]. given #236 (A,wt=12): 125 x <= (x v y) ^ z | x ^ z != x. [para(46(a,1),36(b,1))]. given #237 (F,wt=6): 3812 D(c3,c2 v c3,c1). [para(1188(a,1),782(a,2))]. given #238 (F,wt=7): 3818 c2 v c3 <= c1 v c3. [para(1188(a,1),644(a,1))]. given #239 (T,wt=8): 3800 D(c3,c2 v c3,c1 ^ c2). [para(1188(a,1),168(a,2))]. given #240 (T,wt=8): 3801 D(c1 ^ c2,c2 v c3,c3). [para(1188(a,1),192(a,2))]. given #241 (A,wt=15): 126 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(46(a,1),42(a,1,2)),flip(a)]. given #242 (F,wt=8): 3832 D(c1 v c3,c2 v c3,c3). [hyper(119,b,131,a,c,3818,a),rewrite(45(11))]. given #243 (F,wt=8): 3834 D(c3,c2 v c3,c1 v c3). [hyper(107,b,85,a,c,3818,a)]. given #244 (T,wt=9): 1267 x <= (x v y) ^ (x v z). [para(29(a,1),128(a,1))]. given #245 (T,wt=9): 1271 x <= (x v y) ^ (z v x). [para(45(a,1),128(a,1))]. given #246 (A,wt=13): 127 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(44(a,1),46(a,1,2,1))]. given #247 (F,wt=9): 1651 x ^ (c1 ^ (c3 ^ y)) <= c2. [para(40(a,1),162(a,2)),rewrite(26(4))]. given #248 (F,wt=9): 1899 c1 ^ (c3 ^ x) <= c2 v y. [para(67(a,1),212(a,2)),rewrite(26(4))]. given #249 (T,wt=9): 1968 x ^ (c1 ^ c3) <= c2 v y. [para(67(a,1),225(a,2))]. given #250 (T,wt=9): 2049 x ^ (c1 ^ (y ^ c3)) <= c2. [para(42(a,1),236(a,1,2))]. given #251 (A,wt=15): 129 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(46(a,1),49(a,1,2)),rewrite(25(4))]. given #252 (F,wt=9): 2188 (x ^ y) v (x ^ z) <= x. [para(31(a,1),241(a,2))]. given #253 (F,wt=9): 2190 (c1 ^ c3) v (c2 ^ x) <= c2. [para(40(a,1),241(a,2)),rewrite(25(6))]. given #254 (T,wt=9): 2194 (x ^ y) v (z ^ x) <= x. [para(49(a,1),241(a,2))]. given #255 (T,wt=9): 2293 x <= (y v x) ^ (x v z). [para(29(a,1),493(a,1))]. given #256 (A,wt=11): 133 x v y <= z v (x v (u v y)). [para(44(a,1),88(a,2,2))]. given #257 (F,wt=9): 2297 x <= (y v x) ^ (z v x). [para(45(a,1),493(a,1))]. given #258 (F,wt=9): 2388 (c1 ^ c3) v (x ^ c2) <= c2. [para(49(a,1),544(a,2))]. given #259 (T,wt=9): 2419 (x ^ y) v (y ^ z) <= y. [para(31(a,1),548(a,2))]. given #260 (T,wt=9): 2421 (x ^ c2) v (c1 ^ c3) <= c2. [para(40(a,1),548(a,2))]. given #261 (A,wt=11): 135 x v y <= z v (x v (y v u)). [para(27(a,1),96(a,2,2))]. given #262 (F,wt=9): 2425 (x ^ y) v (z ^ y) <= y. [para(49(a,1),548(a,2))]. given #263 (F,wt=9): 2664 c1 ^ (x ^ c3) <= c2 ^ x. [para(24(a,1),606(a,1,2))]. given #264 (T,wt=9): 2665 c1 ^ c3 <= c2 ^ (c3 v x). [para(29(a,1),606(a,1,2))]. given #265 (T,wt=8): 4728 D(c1,c2 ^ (c1 v c3),c3). [hyper(56,b,2665,a,c,101,a),rewrite(25(5))]. given #266 (A,wt=13): 137 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [hyper(35,a,103,a),rewrite(24(3))]. given #267 (F,wt=8): 4729 D(c3,c2 ^ (c1 v c3),c1). [hyper(55,b,2665,a,c,101,a),rewrite(25(5))]. given #268 (F,wt=9): 2668 c1 ^ c3 <= c2 ^ (x v c3). [para(45(a,1),606(a,1,2))]. given #269 (T,wt=9): 2677 c1 ^ c3 <= c2 ^ (c1 v x). [para(77(a,1),606(a,1)),rewrite(24(3))]. given #270 (T,wt=9): 2686 c1 ^ c3 <= c2 ^ (x v c1). [para(109(a,1),606(a,1)),rewrite(24(3))]. given #271 (A,wt=11): 138 x ^ (y ^ (z ^ u)) <= y ^ z. [para(26(a,1),103(a,1,2))]. given #272 (F,wt=9): 2687 c2 v (c1 ^ (x ^ c3)) = c2. [para(24(a,1),611(a,1,2,2))]. given #273 (F,wt=9): 2981 c1 ^ (x ^ c3) <= y v c2. [para(24(a,1),661(a,1,2))]. given #274 (T,wt=9): 3037 c1 ^ (x ^ c3) <= x ^ c2. [para(24(a,1),677(a,1,2))]. given #275 (T,wt=9): 3231 c1 v (c2 v c3) = c1 v c3. [para(239(a,1),121(a,1,2)),rewrite(44(5),25(4))]. ============================== PROOF ================================= % Proof 1 at 0.48 (+ 0.01) seconds. % Length of proof is 47. % Level of proof is 13. % Maximum clause weight is 20. % Given clauses 275. 3 (all xa all xx all xb (C(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa ^ xb) v xx = xx)) # label(non_clause). [assumption]. 5 (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)) # label(non_clause). [assumption]. 6 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause). [assumption]. 7 (all a all x all b (C(a,x,b) -> D(a,x,b))). [goal]. 18 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 19 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. 20 C(c1,c2,c3). [deny(7)]. 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 25 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 28 (x v y) ^ x = x # label("absorption_1"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 30 (x ^ y) v x = x # label("absorption_2"). [assumption]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 32 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 34 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. 36 x <= y | x ^ y != x. [clausify(6)]. 37 -D(c1,c2,c3). [deny(7)]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(20,a,18,a)]. 39 (c1 ^ c3) v c2 = c2. [resolve(20,a,19,a)]. 40 c2 v (c1 ^ c3) = c2. [copy(39),rewrite(25(5))]. 44 x v (y v z) = y v (x v z). [para(25(a,1),27(a,1,1)),rewrite(27(2))]. 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. 51 x v ((x ^ y) v z) = x v z. [para(31(a,1),27(a,1,1)),flip(a)]. 56 D(x,y,z) | -(x ^ z <= y) | -(y <= z v x). [para(25(a,1),34(c,2))]. 57 D(x ^ y,z,u) | -(x ^ (y ^ u) <= z) | -(z <= (x ^ y) v u). [para(26(a,1),34(b,1))]. 61 x <= x v y. [hyper(36,b,29,a)]. 85 x <= y v x. [para(25(a,1),61(a,2))]. 88 x <= y v (z v x). [para(27(a,1),85(a,2))]. 89 x ^ y <= x. [para(31(a,1),85(a,2))]. 91 x ^ (y v (x v z)) = x. [para(44(a,1),29(a,1,2))]. 101 x ^ y <= y. [para(24(a,1),89(a,1))]. 121 x v (y v (z ^ x)) = y v x. [para(49(a,1),44(a,1,2)),flip(a)]. 134 x ^ y <= z v y. [para(49(a,1),88(a,2,2))]. 239 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),51(a,1,2)),flip(a)]. 363 D(x ^ y,y ^ z,z). [hyper(57,b,101,a,c,134,a)]. 441 D(x,(y v x) ^ z,z). [para(45(a,1),363(a,1))]. 495 D(c1 ^ c3,c2 ^ x,x). [para(40(a,1),441(a,2,1))]. 606 c1 ^ (c3 ^ x) <= c2 ^ x. [hyper(32,a,495,a),rewrite(26(4))]. 2665 c1 ^ c3 <= c2 ^ (c3 v x). [para(29(a,1),606(a,1,2))]. 3231 c1 v (c2 v c3) = c1 v c3. [para(239(a,1),121(a,1,2)),rewrite(44(5),25(4))]. 4728 D(c1,c2 ^ (c1 v c3),c3). [hyper(56,b,2665,a,c,101,a),rewrite(25(5))]. 4928 c2 ^ (c1 v c3) = c2. [para(3231(a,1),91(a,1,2))]. 4962 D(c1,c2,c3). [back_rewrite(4728),rewrite(4928(6))]. 4963 $F. [resolve(4962,a,37,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=275. Generated=19241. Kept=4936. proofs=1. Usable=269. Sos=4234. Demods=405. Limbo=34, Disabled=428. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=14305. Back_subsumed=186. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=424 (6 lex), Back_demodulated=210. Back_unit_deleted=0. Demod_attempts=185530. Demod_rewrites=25342. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=21770. Nonunit_bsub_feature_tests=12340. Megabytes=3.34. User_CPU=0.48, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11449 exit (max_proofs) Sat Aug 12 21:01:21 2006