============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11450 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:21 2006 The command was "/home/mccune/bin/prover9 -f head.in csd.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 csd.in formulas(goals). (all a all x all b (CS(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 (CS(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)]. CS(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)]. Eliminating CS/3 20 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 21 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 22 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. 23 CS(c1,c2,c3). [deny(7)]. Derived: (c1 v c2) ^ (c2 v c3) = c2. [resolve(23,a,21,a)]. Derived: (c1 v c3) ^ c2 = c2. [resolve(23,a,22,a)]. ============================== 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 v c2) ^ (c2 v c3) = c2. [resolve(23,a,21,a)]. 40 c2 ^ (c1 v c3) = c2. [copy(39),rewrite(24(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 v c2) ^ (c2 v c3) = c2. [resolve(23,a,21,a)]. 40 c2 ^ (c1 v c3) = c2. [copy(39),rewrite(24(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 v c2) ^ (c2 v c3) = c2. [resolve(23,a,21,a)]. given #14 (I,wt=7): 40 c2 ^ (c1 v c3) = c2. [copy(39),rewrite(24(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): 67 c2 <= c1 v c3. [hyper(36,b,40,a)]. 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 x <= y v x. [para(25(a,1),61(a,2))]. given #23 (F,wt=5): 94 x ^ y <= x. [para(31(a,1),87(a,2))]. given #24 (T,wt=4): 97 D(x,x,y). [hyper(34,b,94,a,c,61,a)]. given #25 (T,wt=5): 98 x ^ y <= y. [para(24(a,1),94(a,1))]. given #26 (A,wt=7): 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. given #27 (F,wt=4): 101 D(x,y,y). [hyper(34,b,98,a,c,87,a)]. given #28 (F,wt=7): 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. given #29 (T,wt=7): 92 x <= y v (x v z). [para(44(a,1),61(a,2))]. given #30 (T,wt=7): 93 x <= y v (z v x). [para(27(a,1),87(a,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): 100 x ^ (y ^ z) <= y. [para(42(a,1),94(a,1))]. given #33 (F,wt=7): 102 x ^ (y ^ z) <= z. [para(26(a,1),98(a,1))]. given #34 (T,wt=7): 122 x ^ y <= z v x. [para(31(a,1),93(a,2,2))]. given #35 (T,wt=7): 124 x ^ y <= z v y. [para(49(a,1),93(a,2,2))]. 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=6): 150 D(x,x ^ y,y). [hyper(34,b,70,a,c,124,a)]. given #38 (F,wt=6): 151 D(x,x v y,y). [hyper(34,b,124,a,c,70,a)]. given #39 (T,wt=6): 170 D(x,y ^ x,y). [para(24(a,1),150(a,2))]. given #40 (T,wt=6): 176 D(x,y v x,y). [para(25(a,1),151(a,2))]. 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=7): 137 x ^ y <= x v z. [para(46(a,1),100(a,1))]. given #43 (F,wt=7): 140 x ^ y <= y v z. [para(29(a,1),102(a,1,2))]. given #44 (T,wt=7): 141 x ^ c2 <= c1 v c3. [para(40(a,1),102(a,1,2))]. given #45 (T,wt=7): 154 c2 <= x v (c1 v c3). [para(40(a,1),124(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): 179 x ^ y <= y ^ x. [hyper(32,a,170,a)]. given #48 (F,wt=7): 185 x v y <= y v x. [hyper(33,a,176,a)]. given #49 (T,wt=7): 209 c2 <= c1 v (c3 v x). [para(40(a,1),140(a,1)),rewrite(27(5))]. given #50 (T,wt=7): 214 c2 ^ x <= c1 v c3. [para(24(a,1),141(a,1))]. 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): 218 c2 <= c1 v (x v c3). [para(44(a,1),154(a,2))]. given #53 (F,wt=8): 62 x <= y | y ^ x != x. [para(24(a,1),36(b,1))]. given #54 (T,wt=8): 172 D(c1 v c2,c2,c2 v c3). [para(38(a,1),150(a,2))]. given #55 (T,wt=8): 181 D(c2 v c3,c2,c1 v c2). [para(38(a,1),170(a,2))]. 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=9): 71 x ^ (x ^ y) = x ^ y. [para(53(a,1),26(a,1,1)),flip(a)]. given #58 (F,wt=9): 73 x ^ (y ^ x) = y ^ x. [para(53(a,1),26(a,2,2)),rewrite(24(2))]. given #59 (T,wt=9): 77 x v (y ^ (x ^ z)) = x. [para(42(a,1),31(a,1,2))]. given #60 (T,wt=9): 82 x v (x v y) = x v y. [para(54(a,1),27(a,1,1)),flip(a)]. 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): 285 D(x ^ c2,c2,c1 v c3). [hyper(55,b,102,a,c,154,a)]. given #63 (F,wt=8): 288 D(x ^ y,y,z v y). [hyper(55,b,102,a,c,93,a)]. given #64 (T,wt=8): 289 D(x ^ y,y,y v z). [hyper(55,b,102,a,c,92,a)]. given #65 (T,wt=8): 290 D(c2 ^ x,c2,c1 v c3). [hyper(55,b,100,a,c,154,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,z v x). [hyper(55,b,100,a,c,93,a)]. given #68 (F,wt=8): 294 D(x ^ y,x,x v z). [hyper(55,b,100,a,c,92,a)]. given #69 (T,wt=8): 335 D(c1 v c3,c2,x ^ c2). [hyper(56,b,102,a,c,154,a)]. given #70 (T,wt=8): 336 D(x v y,y,z ^ y). [hyper(56,b,102,a,c,93,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): 337 D(x v y,x,z ^ x). [hyper(56,b,102,a,c,92,a)]. given #73 (F,wt=8): 338 D(c1 v c3,c2,c2 ^ x). [hyper(56,b,100,a,c,154,a)]. given #74 (T,wt=8): 339 D(x v y,y,y ^ z). [hyper(56,b,100,a,c,93,a)]. given #75 (T,wt=8): 340 D(x v y,x,x ^ z). [hyper(56,b,100,a,c,92,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): 380 D(x ^ y,y ^ z,z). [hyper(57,b,98,a,c,124,a)]. given #78 (F,wt=8): 422 D(x v y,y v z,z). [hyper(58,b,124,a,c,87,a)]. given #79 (T,wt=8): 444 D(x ^ y,x ^ z,z). [para(24(a,1),380(a,1))]. given #80 (T,wt=8): 445 D(x ^ y,z ^ y,z). [para(24(a,1),380(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): 448 D(x,(x v y) ^ z,z). [para(29(a,1),380(a,1))]. given #83 (F,wt=6): 504 D(c1,c2,c2 v c3). [para(38(a,1),448(a,2))]. given #84 (T,wt=8): 450 D(c2,(c1 v c3) ^ x,x). [para(40(a,1),380(a,1))]. given #85 (T,wt=8): 453 D(x,(y v x) ^ z,z). [para(45(a,1),380(a,1))]. given #86 (A,wt=13): 64 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(38(a,1),26(a,1,1)),flip(a)]. given #87 (F,wt=8): 459 D(x v y,x v z,z). [para(25(a,1),422(a,1))]. given #88 (F,wt=8): 460 D(x v y,z v y,z). [para(25(a,1),422(a,2))]. given #89 (T,wt=8): 463 D(x,(x ^ y) v z,z). [para(31(a,1),422(a,1))]. given #90 (T,wt=8): 466 D(x,(y ^ x) v z,z). [para(49(a,1),422(a,1))]. given #91 (A,wt=12): 66 c1 v c2 <= c2 v c3 | c1 v c2 != c2. [para(38(a,1),36(b,1)),flip(b)]. given #92 (F,wt=8): 473 D(x ^ y,z ^ x,z). [para(24(a,1),444(a,2))]. given #93 (F,wt=8): 483 D(x,y ^ (x v z),y). [para(29(a,1),445(a,1))]. given #94 (T,wt=8): 485 D(c2,x ^ (c1 v c3),x). [para(40(a,1),445(a,1))]. given #95 (T,wt=8): 488 D(x,y ^ (z v x),y). [para(45(a,1),445(a,1))]. given #96 (A,wt=11): 68 c2 ^ ((c1 v c3) ^ x) = c2 ^ x. [para(40(a,1),26(a,1,1)),flip(a)]. given #97 (F,wt=6): 589 D(c3,c2,c1 v c2). [para(38(a,1),488(a,2))]. given #98 (F,wt=7): 618 c3 ^ (c1 v c2) <= c2. [hyper(32,a,589,a)]. given #99 (T,wt=8): 540 D(x v y,z v x,z). [para(25(a,1),459(a,2))]. given #100 (T,wt=8): 549 D(x,y v (x ^ z),y). [para(31(a,1),460(a,1))]. given #101 (A,wt=10): 74 D(x,y,x) | -(x <= y) | -(y <= x). [para(53(a,1),34(b,1)),rewrite(54(3))]. given #102 (F,wt=8): 552 D(x,y v (z ^ x),y). [para(49(a,1),460(a,1))]. given #103 (F,wt=8): 565 D(c1 v c3,c2 v x,x). [para(40(a,1),466(a,2,1))]. given #104 (T,wt=8): 633 D(c1 v c3,x v c2,x). [para(40(a,1),552(a,2,2))]. given #105 (T,wt=9): 84 x v (y v x) = y v x. [para(54(a,1),27(a,2,2)),rewrite(25(2))]. given #106 (A,wt=14): 75 D(x,y,x ^ z) | -(x ^ z <= y) | -(y <= x). [back_rewrite(60),rewrite(71(4))]. given #107 (F,wt=8): 649 D(x,y ^ x,x ^ y). [hyper(75,b,179,a,c,98,a)]. given #108 (F,wt=9): 88 x v y <= x v (y v z). [para(27(a,1),61(a,2))]. given #109 (T,wt=8): 690 D(x,x v y,y v z). [hyper(55,b,140,a,c,88,a)]. given #110 (T,wt=8): 695 D(x,y v x,y v z). [para(25(a,1),690(a,2))]. given #111 (A,wt=11): 76 x ^ (y ^ (x v z)) = y ^ x. [para(29(a,1),42(a,1,2)),flip(a)]. given #112 (F,wt=8): 696 D(x,x v y,z v y). [para(25(a,1),690(a,3))]. given #113 (F,wt=8): 701 D(x,y v x,z v y). [para(25(a,1),695(a,3))]. given #114 (T,wt=8): 740 D(x,x v (y ^ z),y). [para(31(a,1),696(a,3))]. given #115 (T,wt=8): 743 D(x,x v (y ^ z),z). [para(49(a,1),696(a,3))]. given #116 (A,wt=20): 78 D(x,y,z ^ u) | -(z ^ (x ^ u) <= y) | -(y <= x v (z ^ u)). [para(42(a,1),34(b,1))]. given #117 (F,wt=8): 750 D(x,(y ^ z) v x,y). [para(31(a,1),701(a,3))]. given #118 (F,wt=8): 753 D(x,(y ^ z) v x,z). [para(49(a,1),701(a,3))]. given #119 (T,wt=8): 766 D(x,x v c2,c1 v c3). [para(40(a,1),743(a,2,2))]. given #120 (T,wt=8): 772 D(x,x ^ y,z ^ y). [hyper(78,b,98,a,c,137,a)]. given #121 (A,wt=12): 79 x <= y ^ z | y ^ (x ^ z) != x. [para(42(a,1),36(b,1))]. given #122 (F,wt=8): 799 D(x,c2 v x,c1 v c3). [para(40(a,1),753(a,2,1))]. given #123 (F,wt=8): 810 D(x,y ^ x,z ^ y). [para(24(a,1),772(a,2))]. given #124 (T,wt=8): 811 D(x,x ^ y,y ^ z). [para(24(a,1),772(a,3))]. given #125 (T,wt=8): 814 D(x,x ^ (y v z),y). [para(29(a,1),772(a,3))]. given #126 (A,wt=13): 80 (c1 v c2) ^ (x ^ (c2 v c3)) = x ^ c2. [para(38(a,1),42(a,1,2)),flip(a)]. given #127 (F,wt=8): 816 D(x,x ^ (c1 v c3),c2). [para(40(a,1),772(a,3))]. given #128 (F,wt=8): 819 D(x,x ^ (y v z),z). [para(45(a,1),772(a,3))]. given #129 (T,wt=6): 918 D(c1 v c2,c2,c3). [para(38(a,1),819(a,2))]. given #130 (T,wt=8): 850 D(x,y ^ x,y ^ z). [para(24(a,1),810(a,3))]. given #131 (A,wt=11): 81 c2 ^ (x ^ (c1 v c3)) = x ^ c2. [para(40(a,1),42(a,1,2)),flip(a)]. given #132 (F,wt=8): 853 D(x,(y v z) ^ x,y). [para(29(a,1),810(a,3))]. given #133 (F,wt=6): 964 D(c2 v c3,c2,c1). [para(38(a,1),853(a,2))]. given #134 (T,wt=8): 855 D(x,(c1 v c3) ^ x,c2). [para(40(a,1),810(a,3))]. given #135 (T,wt=8): 858 D(x,(y v z) ^ x,z). [para(45(a,1),810(a,3))]. given #136 (A,wt=14): 86 D(x,y,x v z) | -(x <= y) | -(y <= x v z). [back_rewrite(59),rewrite(82(5))]. given #137 (F,wt=9): 89 x ^ (y v (x v z)) = x. [para(44(a,1),29(a,1,2))]. given #138 (F,wt=9): 95 x v y <= x v (z v y). [para(44(a,1),87(a,2))]. given #139 (T,wt=9): 99 x ^ (y ^ z) <= x ^ y. [para(26(a,1),94(a,1))]. given #140 (T,wt=9): 103 x ^ (y ^ z) <= x ^ z. [para(42(a,1),98(a,1))]. given #141 (A,wt=11): 90 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): 110 x v (y ^ (z ^ x)) = x. [para(26(a,1),49(a,1,2))]. given #144 (T,wt=9): 114 c1 v (c2 v c3) = c1 v c3. [para(40(a,1),49(a,1,2)),rewrite(25(5),44(5))]. given #145 (T,wt=7): 1161 c2 v c3 <= c1 v c3. [para(114(a,1),87(a,2))]. given #146 (A,wt=20): 91 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): 1193 D(c3,c2 v c3,c1). [hyper(56,b,122,a,c,1161,a)]. given #148 (F,wt=6): 1194 D(c1,c2 v c3,c3). [hyper(55,b,122,a,c,1161,a)]. given #149 (T,wt=7): 1180 c1 v c2 <= c1 v c3. [para(114(a,1),88(a,2))]. given #150 (T,wt=6): 1212 D(c3,c1 v c2,c1). [hyper(56,b,140,a,c,1180,a)]. given #151 (A,wt=11): 104 x ^ ((y v x) ^ z) = x ^ z. [para(45(a,1),26(a,1,1)),flip(a)]. given #152 (F,wt=6): 1213 D(c1,c1 v c2,c3). [hyper(55,b,140,a,c,1180,a)]. given #153 (F,wt=9): 120 x <= y v (z v (x v u)). [para(27(a,1),92(a,2))]. given #154 (T,wt=9): 121 x <= y v (z v (u v x)). [para(27(a,1),93(a,2,2))]. given #155 (T,wt=9): 129 c1 ^ (c2 v c3) = c1 ^ c2. [para(38(a,1),46(a,1,2)),flip(a)]. given #156 (A,wt=13): 105 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(45(a,1),26(a,1)),flip(a)]. given #157 (F,wt=6): 1371 D(c3,c1 ^ c2,c1). [para(129(a,1),488(a,2))]. given #158 (F,wt=6): 1382 D(c1,c1 ^ c2,c3). [para(129(a,1),819(a,2))]. given #159 (T,wt=7): 1433 c1 ^ c3 <= c1 ^ c2. [hyper(32,a,1371,a),rewrite(24(3))]. given #160 (T,wt=8): 1356 D(c1,c1 ^ c2,c2 v c3). [para(129(a,1),150(a,2))]. given #161 (A,wt=14): 107 D(x,y,z v x) | -(x <= y) | -(y <= z v x). [para(45(a,1),34(b,1)),rewrite(84(5))]. given #162 (F,wt=8): 1357 D(c2 v c3,c1 ^ c2,c1). [para(129(a,1),170(a,2))]. given #163 (F,wt=8): 1435 D(c1 ^ c3,c1 ^ c2,c1). [hyper(86,b,1433,a,c,122,a),rewrite(25(11),31(11))]. given #164 (T,wt=8): 1444 D(c1,c1 ^ c2,c1 ^ c3). [hyper(75,b,1433,a,c,94,a)]. given #165 (T,wt=9): 132 x ^ y <= (x v z) ^ y. [para(46(a,1),98(a,1))]. given #166 (A,wt=11): 108 x ^ (y ^ (z v x)) = y ^ x. [para(45(a,1),42(a,1,2)),flip(a)]. given #167 (F,wt=9): 136 x ^ (y ^ (z ^ u)) <= z. [para(26(a,1),100(a,1))]. given #168 (F,wt=9): 139 x ^ (y ^ (z ^ u)) <= u. [para(26(a,1),102(a,1,2))]. given #169 (T,wt=9): 147 x ^ y <= z v (u v x). [para(27(a,1),122(a,2))]. given #170 (T,wt=9): 148 x ^ (y ^ z) <= u v y. [para(42(a,1),122(a,1))]. given #171 (A,wt=13): 109 (x v y) ^ (x v (z v y)) = x v y. [para(44(a,1),45(a,1,2))]. given #172 (F,wt=9): 152 x ^ (y ^ z) <= u v z. [para(26(a,1),124(a,1))]. given #173 (F,wt=9): 153 x ^ y <= z v (u v y). [para(27(a,1),124(a,2))]. given #174 (T,wt=9): 204 x ^ (y ^ z) <= y v u. [para(42(a,1),137(a,1))]. given #175 (T,wt=9): 205 x ^ y <= z v (x v u). [para(44(a,1),137(a,2))]. given #176 (A,wt=11): 111 x v ((y ^ x) v z) = x v z. [para(49(a,1),27(a,1,1)),flip(a)]. given #177 (F,wt=9): 208 x ^ (y ^ z) <= z v u. [para(26(a,1),140(a,1))]. given #178 (F,wt=9): 211 x ^ y <= z v (y v u). [para(44(a,1),140(a,2))]. given #179 (T,wt=9): 215 x ^ (y ^ c2) <= c1 v c3. [para(26(a,1),141(a,1))]. given #180 (T,wt=9): 216 c2 ^ (x v (c1 v c3)) = c2. [hyper(35,a,154,a)]. given #181 (A,wt=13): 112 x v (y v (z ^ (x v y))) = x v y. [para(49(a,1),27(a,1)),flip(a)]. given #182 (F,wt=9): 217 c2 <= x v (y v (c1 v c3)). [para(27(a,1),154(a,2))]. given #183 (F,wt=9): 235 c2 ^ (c1 v (c3 v x)) = c2. [hyper(35,a,209,a)]. given #184 (T,wt=9): 236 c2 <= c1 v (x v (c3 v y)). [para(44(a,1),209(a,2,2))]. given #185 (T,wt=9): 239 x ^ (c2 ^ y) <= c1 v c3. [para(42(a,1),214(a,1))]. given #186 (A,wt=14): 113 D(x,y,z ^ x) | -(z ^ x <= y) | -(y <= x). [para(49(a,1),34(c,2)),rewrite(73(4))]. given #187 (F,wt=9): 244 (x ^ y) v z <= x v z. [para(51(a,1),87(a,2))]. given #188 (F,wt=9): 251 c2 ^ (c1 v (x v c3)) = c2. [hyper(35,a,218,a)]. given #189 (T,wt=9): 252 c2 <= c1 v (x v (y v c3)). [para(27(a,1),218(a,2,2))]. given #190 (T,wt=9): 480 x ^ (y ^ z) <= z ^ y. [hyper(32,a,445,a),rewrite(26(2))]. given #191 (A,wt=13): 115 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(42(a,1),49(a,1,2))]. given #192 (F,wt=9): 509 c2 ^ x <= (c1 v c3) ^ x. [hyper(32,a,450,a)]. given #193 (F,wt=9): 513 x ^ y <= (z v x) ^ y. [hyper(32,a,453,a)]. given #194 (T,wt=9): 546 x v y <= z v (y v x). [hyper(33,a,460,a),rewrite(27(3))]. given #195 (T,wt=9): 563 (x ^ y) v z <= y v z. [hyper(33,a,466,a)]. given #196 (A,wt=11): 116 x v (y v (z ^ x)) = y v x. [para(49(a,1),44(a,1,2)),flip(a)]. given #197 (F,wt=9): 573 x ^ (y ^ z) <= z ^ x. [hyper(32,a,473,a),rewrite(26(2))]. given #198 (F,wt=9): 581 x ^ y <= y ^ (x v z). [hyper(32,a,483,a)]. given #199 (T,wt=9): 584 c2 ^ x <= x ^ (c1 v c3). [hyper(32,a,485,a)]. given #200 (T,wt=9): 586 x ^ y <= y ^ (z v x). [hyper(32,a,488,a)]. given #201 (A,wt=16): 117 D(c1 v c2,x,c2 v c3) | -(c2 <= x) | -(x <= c1 v c3). [back_rewrite(85),rewrite(114(14))]. given #202 (F,wt=9): 619 c3 ^ (c1 v c2) = c2 ^ c3. [hyper(35,a,618,a),rewrite(24(7),108(7),24(3)),flip(a)]. given #203 (F,wt=6): 2851 D(c1,c2 ^ c3,c3). [para(619(a,1),483(a,2))]. given #204 (T,wt=6): 2857 D(c3,c2 ^ c3,c1). [para(619(a,1),814(a,2))]. given #205 (T,wt=7): 2864 c1 ^ c3 <= c2 ^ c3. [para(619(a,1),581(a,2))]. given #206 (A,wt=14): 118 D(c2,x,c1 v c3) | -(c2 <= x) | -(x <= c1 v c3). [back_rewrite(69),rewrite(114(12))]. given #207 (F,wt=8): 2842 D(c3,c2 ^ c3,c1 v c2). [para(619(a,1),150(a,2))]. given #208 (F,wt=8): 2843 D(c1 v c2,c2 ^ c3,c3). [para(619(a,1),170(a,2))]. given #209 (T,wt=8): 2866 D(c3,c2 ^ c3,c1 ^ c3). [hyper(113,b,2864,a,c,98,a)]. given #210 (T,wt=8): 2867 D(c1 ^ c3,c2 ^ c3,c3). [hyper(107,b,2864,a,c,140,a),rewrite(49(11))]. given #211 (A,wt=11): 119 x v y <= z v (x v (y v u)). [para(27(a,1),92(a,2,2))]. given #212 (F,wt=9): 620 x v y <= y v (z v x). [hyper(33,a,540,a),rewrite(27(3))]. given #213 (F,wt=9): 625 x v (y ^ z) <= y v x. [hyper(33,a,549,a)]. given #214 (T,wt=9): 630 x v (y ^ z) <= z v x. [hyper(33,a,552,a)]. given #215 (T,wt=9): 638 c2 v x <= c1 v (c3 v x). [hyper(33,a,565,a),rewrite(27(6))]. given #216 (A,wt=11): 123 x v y <= z v (x v (u v y)). [para(44(a,1),93(a,2,2))]. given #217 (F,wt=9): 642 x v c2 <= c1 v (c3 v x). [hyper(33,a,633,a),rewrite(27(6))]. given #218 (F,wt=9): 691 x v y <= y v (x v z). [para(25(a,1),88(a,1))]. given #219 (T,wt=9): 712 x ^ y <= x ^ (y v z). [para(76(a,1),98(a,1))]. given #220 (T,wt=9): 760 x v (y ^ z) <= x v y. [hyper(33,a,740,a)]. given #221 (A,wt=17): 125 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): 763 x v (y ^ z) <= x v z. [hyper(33,a,743,a)]. given #223 (F,wt=9): 791 (x ^ y) v z <= z v x. [hyper(33,a,750,a)]. given #224 (T,wt=9): 797 (x ^ y) v z <= z v y. [hyper(33,a,753,a)]. given #225 (T,wt=9): 808 x v c2 <= x v (c1 v c3). [hyper(33,a,766,a)]. given #226 (A,wt=17): 126 (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): 846 c2 v x <= x v (c1 v c3). [hyper(33,a,799,a)]. given #228 (F,wt=9): 913 x ^ c2 <= x ^ (c1 v c3). [hyper(32,a,816,a)]. given #229 (T,wt=9): 915 x ^ y <= x ^ (z v y). [hyper(32,a,819,a)]. given #230 (T,wt=9): 922 x ^ (y ^ z) <= y ^ x. [hyper(32,a,850,a)]. given #231 (A,wt=22): 127 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): 963 x ^ y <= (y v z) ^ x. [hyper(32,a,853,a)]. given #233 (F,wt=9): 972 x ^ c2 <= (c1 v c3) ^ x. [hyper(32,a,855,a)]. given #234 (T,wt=9): 977 x ^ y <= (z v y) ^ x. [hyper(32,a,858,a)]. given #235 (T,wt=9): 1163 c2 v c3 <= x v (c1 v c3). [para(114(a,1),93(a,2,2))]. given #236 (A,wt=12): 128 x <= (x v y) ^ z | x ^ z != x. [para(46(a,1),36(b,1))]. given #237 (F,wt=8): 3793 D(x v c1,c2 v c3,c3). [hyper(58,b,124,a,c,1163,a)]. given #238 (F,wt=8): 3818 D(c1 v x,c2 v c3,c3). [para(25(a,1),3793(a,1))]. given #239 (T,wt=9): 1164 (c2 v c3) ^ x <= c1 v c3. [para(114(a,1),122(a,2))]. given #240 (T,wt=9): 1165 x ^ (c2 v c3) <= c1 v c3. [para(114(a,1),124(a,2))]. given #241 (A,wt=15): 130 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(46(a,1),42(a,1,2)),flip(a)]. given #242 (F,wt=9): 1445 c1 ^ (c2 ^ c3) = c1 ^ c3. [hyper(35,a,1433,a),rewrite(24(7),42(7),24(6),42(6),24(5),71(7))]. given #243 (F,wt=5): 3975 c1 ^ c3 <= c2. [para(1445(a,1),100(a,1))]. ============================== PROOF ================================= % Proof 1 at 0.37 (+ 0.00) seconds. % Length of proof is 48. % Level of proof is 14. % Maximum clause weight is 20. % Given clauses 243. 4 (all xa all xx all xb (CS(xa,xx,xb) <-> (xa v xx) ^ (xx v xb) = xx & (xa v xb) ^ 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 (CS(a,x,b) -> D(a,x,b))). [goal]. 21 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 22 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. 23 CS(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)]. 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 v c2) ^ (c2 v c3) = c2. [resolve(23,a,21,a)]. 39 (c1 v c3) ^ c2 = c2. [resolve(23,a,22,a)]. 40 c2 ^ (c1 v c3) = c2. [copy(39),rewrite(24(5))]. 42 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. 45 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. 46 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. 49 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. 53 x ^ x = x. [para(31(a,1),29(a,1,2))]. 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)]. 67 c2 <= c1 v c3. [hyper(36,b,40,a)]. 71 x ^ (x ^ y) = x ^ y. [para(53(a,1),26(a,1,1)),flip(a)]. 87 x <= y v x. [para(25(a,1),61(a,2))]. 93 x <= y v (z v x). [para(27(a,1),87(a,2))]. 94 x ^ y <= x. [para(31(a,1),87(a,2))]. 98 x ^ y <= y. [para(24(a,1),94(a,1))]. 100 x ^ (y ^ z) <= y. [para(42(a,1),94(a,1))]. 124 x ^ y <= z v y. [para(49(a,1),93(a,2,2))]. 129 c1 ^ (c2 v c3) = c1 ^ c2. [para(38(a,1),46(a,1,2)),flip(a)]. 380 D(x ^ y,y ^ z,z). [hyper(57,b,98,a,c,124,a)]. 445 D(x ^ y,z ^ y,z). [para(24(a,1),380(a,2))]. 488 D(x,y ^ (z v x),y). [para(45(a,1),445(a,1))]. 1371 D(c3,c1 ^ c2,c1). [para(129(a,1),488(a,2))]. 1433 c1 ^ c3 <= c1 ^ c2. [hyper(32,a,1371,a),rewrite(24(3))]. 1445 c1 ^ (c2 ^ c3) = c1 ^ c3. [hyper(35,a,1433,a),rewrite(24(7),42(7),24(6),42(6),24(5),71(7))]. 3975 c1 ^ c3 <= c2. [para(1445(a,1),100(a,1))]. 4044 D(c1,c2,c3). [hyper(34,b,3975,a,c,67,a)]. 4045 $F. [resolve(4044,a,37,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=243. Generated=15583. Kept=4018. proofs=1. Usable=241. Sos=3508. Demods=336. Limbo=10, Disabled=288. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=11565. Back_subsumed=118. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=344 (6 lex), Back_demodulated=138. Back_unit_deleted=0. Demod_attempts=140122. Demod_rewrites=19436. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=20190. Nonunit_bsub_feature_tests=11561. Megabytes=2.70. User_CPU=0.37, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11450 exit (max_proofs) Sat Aug 12 21:01:21 2006