============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27050 was started by mccune on cleo, Fri Apr 13 09:19:46 2007 The command was "/home/mccune/bin/prover9 -f head.in ab.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file head.in assign(max_seconds,60). 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 ab.in formulas(goals). (all a all x all b (A(a,x,b) -> B(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 (A(a,x,b) -> B(a,x,b))) # label(goal). [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)]. A(c1,c2,c3). [deny(7)]. -B(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)]. 14 A(c1,c2,c3). [deny(7)]. Derived: c1 <= c2 | c3 <= c2. [resolve(14,a,9,a)]. Derived: c1 <= c2 | c2 <= c1. [resolve(14,a,10,a)]. Derived: c2 <= c3 | c3 <= c2. [resolve(14,a,11,a)]. Derived: c2 <= c3 | c2 <= c1. [resolve(14,a,12,a)]. Eliminating C/3 15 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 16 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 17 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. Eliminating CS/3 18 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 19 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 20 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. Eliminating D/3 21 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. 22 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 23 -D(x,y,z) | y <= x v z. [clausify(5)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ <=, B, =, D, CS, C, A ]). Function symbol precedence: lex([ c1, c2, c3, ^, v ]). After inverse_order: (no changes). Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). % Operation ^ is commutative; C redundancy checks enabled. % Operation v is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 24 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 25 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 27 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. 32 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 35 -(x <= y) | x ^ y = x. [clausify(6)]. 36 x <= y | x ^ y != x. [clausify(6)]. 37 -B(c1,c2,c3). [deny(7)]. 38 c1 <= c2 | c3 <= c2. [resolve(14,a,9,a)]. 39 c1 <= c2 | c2 <= c1. [resolve(14,a,10,a)]. 40 c2 <= c3 | c3 <= c2. [resolve(14,a,11,a)]. 41 c2 <= c3 | c2 <= c1. [resolve(14,a,12,a)]. 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))]. 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: 42 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: 44 x v (y v z) = z v (x v y). [para(27(a,1),25(a,1))]. given #5 (I,wt=7): 29 x ^ (x v y) = x. [copy(28),rewrite(24(2))]. given #6 (I,wt=7): 31 x v (x ^ y) = x. [copy(30),rewrite(25(2))]. given #7 (I,wt=13): 32 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. given #8 (I,wt=13): 33 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. given #9 (I,wt=22): 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. given #10 (I,wt=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 -B(c1,c2,c3). [deny(7)]. given #13 (I,wt=6): 38 c1 <= c2 | c3 <= c2. [resolve(14,a,9,a)]. given #14 (I,wt=6): 39 c1 <= c2 | c2 <= c1. [resolve(14,a,10,a)]. given #15 (I,wt=6): 40 c2 <= c3 | c3 <= c2. [resolve(14,a,11,a)]. given #16 (I,wt=6): 41 c2 <= c3 | c2 <= c1. [resolve(14,a,12,a)]. given #17 (A,wt=11): 43 x ^ (y ^ z) = y ^ (x ^ z). [para(24(a,1),26(a,1,1)),rewrite(26(2))]. given #18 (T,wt=5): 54 x ^ x = x. [para(31(a,1),29(a,1,2))]. given #19 (T,wt=3): 82 x <= x. [hyper(36,b,54,a)]. given #20 (T,wt=4): 86 B(x,x,y). [para(54(a,1),34(b,1,1)),rewrite(31(3),55(3),29(4)),xx(b),xx(c)]. given #21 (T,wt=4): 87 B(x,y,y). [para(54(a,1),34(b,1,2)),rewrite(25(3),50(3),55(4),24(4),46(4)),xx(b),xx(c)]. given #22 (A,wt=11): 45 x v (y v z) = y v (x v z). [para(25(a,1),27(a,1,1)),rewrite(27(2))]. given #23 (T,wt=5): 55 x v x = x. [para(29(a,1),31(a,1,2))]. given #24 (T,wt=5): 70 x <= x v y. [hyper(36,b,29,a)]. given #25 (T,wt=5): 99 x <= y v x. [para(25(a,1),70(a,2))]. given #26 (T,wt=5): 103 x ^ y <= x. [para(31(a,1),99(a,2))]. given #27 (A,wt=7): 46 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. given #28 (T,wt=5): 105 x ^ y <= y. [para(24(a,1),103(a,1))]. given #29 (T,wt=7): 50 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. given #30 (T,wt=7): 101 x <= y v (x v z). [para(45(a,1),70(a,2))]. given #31 (T,wt=7): 102 x <= y v (z v x). [para(27(a,1),99(a,2))]. given #32 (A,wt=11): 47 x ^ ((x v y) ^ z) = x ^ z. [para(29(a,1),26(a,1,1)),flip(a)]. given #33 (T,wt=7): 107 x ^ (y ^ z) <= y. [para(43(a,1),103(a,1))]. given #34 (T,wt=7): 116 x ^ (y ^ z) <= z. [para(26(a,1),105(a,1))]. given #35 (T,wt=7): 129 x ^ y <= z v x. [para(31(a,1),102(a,2,2))]. given #36 (T,wt=7): 131 x ^ y <= z v y. [para(50(a,1),102(a,2,2))]. given #37 (A,wt=13): 48 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(29(a,1),26(a,1)),flip(a)]. given #38 (T,wt=7): 144 x ^ y <= x v z. [para(47(a,1),107(a,1))]. given #39 (T,wt=7): 147 x ^ y <= y v z. [para(29(a,1),116(a,1,2))]. given #40 (T,wt=8): 71 x <= y | y ^ x != x. [para(24(a,1),36(b,1))]. given #41 (T,wt=8): 73 c2 ^ c3 = c3 | c1 <= c2. [hyper(35,a,38,b),rewrite(24(3))]. given #42 (A,wt=13): 49 (x v y) ^ (x v (y v z)) = x v y. [para(27(a,1),29(a,1,2))]. given #43 (T,wt=8): 74 c1 ^ c2 = c2 | c1 <= c2. [hyper(35,a,39,b),rewrite(24(3))]. given #44 (T,wt=6): 215 c1 <= c2 | c2 != c1. [para(74(a,1),36(b,1)),merge(b)]. given #45 (T,wt=8): 75 c2 ^ c3 = c3 | c2 <= c3. [hyper(35,a,40,b),rewrite(24(3))]. given #46 (T,wt=6): 225 c2 <= c3 | c3 != c2. [para(75(a,1),36(b,1)),merge(b)]. given #47 (A,wt=13): 51 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(26(a,1),31(a,1,2))]. given #48 (T,wt=8): 76 c2 ^ c3 = c2 | c2 <= c1. [hyper(35,a,41,a)]. given #49 (T,wt=8): 190 c1 <= c2 | c2 v c3 = c2. [para(73(a,1),31(a,1,2))]. given #50 (T,wt=8): 195 c1 <= c2 | x ^ c3 <= c2. [para(73(a,1),107(a,1,2))]. given #51 (T,wt=8): 196 c1 <= c2 | c3 <= x v c2. [para(73(a,1),129(a,1))]. given #52 (A,wt=11): 52 x v ((x ^ y) v z) = x v z. [para(31(a,1),27(a,1,1)),flip(a)]. given #53 (T,wt=8): 197 c1 <= c2 | c3 <= c2 v x. [para(73(a,1),144(a,1))]. given #54 (T,wt=8): 212 c1 <= c2 | c1 v c2 = c1. [para(74(a,1),31(a,1,2))]. given #55 (T,wt=6): 280 c1 <= c2 | c3 <= c1. [para(212(b,1),196(b,2)),merge(b)]. given #56 (T,wt=8): 217 c1 <= c2 | x ^ c2 <= c1. [para(74(a,1),107(a,1,2))]. given #57 (A,wt=13): 53 x v (y v ((x v y) ^ z)) = x v y. [para(31(a,1),27(a,1)),flip(a)]. given #58 (T,wt=8): 218 c1 <= c2 | c2 <= x v c1. [para(74(a,1),129(a,1))]. given #59 (T,wt=8): 219 c1 <= c2 | c2 <= c1 v x. [para(74(a,1),144(a,1))]. given #60 (T,wt=8): 222 c2 <= c3 | c2 v c3 = c2. [para(75(a,1),31(a,1,2))]. given #61 (T,wt=8): 227 c2 <= c3 | x ^ c3 <= c2. [para(75(a,1),107(a,1,2))]. given #62 (A,wt=22): 56 B(x,y,z) | (y ^ x) v (y ^ z) != y | (x v y) ^ (y v z) != y. [para(24(a,1),34(b,1,1))]. given #63 (T,wt=8): 228 c2 <= c3 | c3 <= x v c2. [para(75(a,1),129(a,1))]. given #64 (T,wt=8): 229 c2 <= c3 | c3 <= c2 v x. [para(75(a,1),144(a,1))]. given #65 (T,wt=8): 247 c2 <= c1 | c2 v c3 = c3. [para(76(a,1),50(a,1,2)),rewrite(25(6))]. given #66 (T,wt=8): 248 c2 <= c1 | x ^ c2 <= c3. [para(76(a,1),116(a,1,2))]. given #67 (A,wt=22): 57 B(x,y,z) | (x ^ y) v (z ^ y) != y | (x v y) ^ (y v z) != y. [para(24(a,1),34(b,1,2))]. given #68 (T,wt=8): 249 c2 <= c1 | c2 <= x v c3. [para(76(a,1),131(a,1))]. given #69 (T,wt=8): 250 c2 <= c1 | c2 <= c3 v x. [para(76(a,1),147(a,1))]. given #70 (T,wt=8): 257 c1 <= c2 | c3 ^ x <= c2. [para(190(b,1),129(a,2))]. given #71 (T,wt=8): 279 c1 <= c2 | c2 ^ x <= c1. [para(212(b,1),129(a,2))]. given #72 (A,wt=22): 58 B(x,y,z) | (x ^ y) v (y ^ z) != y | (y v z) ^ (x v y) != y. [para(24(a,1),34(c,1))]. given #73 (T,wt=8): 281 c1 ^ c3 = c3 | c1 <= c2. [hyper(35,a,280,b),rewrite(24(3))]. given #74 (T,wt=8): 304 c2 <= c3 | c3 ^ x <= c2. [para(222(b,1),129(a,2))]. given #75 (T,wt=8): 352 c2 <= c1 | c2 ^ x <= c3. [para(247(b,1),144(a,2))]. given #76 (T,wt=8): 421 c1 <= c2 | c1 v c3 = c1. [para(281(a,1),31(a,1,2))]. given #77 (A,wt=22): 59 B(x,y,z) | (y ^ z) v (x ^ y) != y | (x v y) ^ (y v z) != y. [para(25(a,1),34(b,1))]. given #78 (T,wt=8): 426 c1 <= c2 | x ^ c3 <= c1. [para(281(a,1),107(a,1,2))]. given #79 (T,wt=8): 427 c1 <= c2 | c3 <= x v c1. [para(281(a,1),129(a,1))]. given #80 (T,wt=8): 428 c1 <= c2 | c3 <= c1 v x. [para(281(a,1),144(a,1))]. given #81 (T,wt=8): 441 c1 <= c2 | c3 ^ x <= c1. [para(421(b,1),129(a,2))]. given #82 (A,wt=22): 60 B(x,y,z) | (x ^ y) v (y ^ z) != y | (y v x) ^ (y v z) != y. [para(25(a,1),34(c,1,1))]. given #83 (T,wt=9): 78 x v (y ^ (x ^ z)) = x. [para(43(a,1),31(a,1,2))]. given #84 (T,wt=9): 83 x ^ (x ^ y) = x ^ y. [para(54(a,1),26(a,1,1)),flip(a)]. given #85 (T,wt=9): 85 x ^ (y ^ x) = y ^ x. [para(54(a,1),26(a,2,2)),rewrite(24(2))]. given #86 (T,wt=9): 90 x ^ (y v (x v z)) = x. [para(45(a,1),29(a,1,2))]. given #87 (A,wt=22): 61 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (z v y) != y. [para(25(a,1),34(c,1,2))]. given #88 (T,wt=9): 94 x v (x v y) = x v y. [para(55(a,1),27(a,1,1)),flip(a)]. given #89 (T,wt=9): 96 x v (y v x) = y v x. [para(55(a,1),27(a,2,2)),rewrite(25(2))]. given #90 (T,wt=9): 100 x v y <= x v (y v z). [para(27(a,1),70(a,2))]. given #91 (T,wt=7): 590 x v y <= y v x. [para(96(a,1),100(a,2))]. given #92 (A,wt=28): 62 B(x ^ y,z,u) | (x ^ (y ^ z)) v (z ^ u) != z | ((x ^ y) v z) ^ (z v u) != z. [para(26(a,1),34(b,1,1))]. given #93 (T,wt=8): 594 c1 <= c2 | c2 v c3 <= c2. [para(190(b,1),590(a,2)),rewrite(25(6))]. given #94 (T,wt=8): 595 c1 <= c2 | c1 v c2 <= c1. [para(212(b,1),590(a,2)),rewrite(25(6))]. given #95 (T,wt=8): 596 c2 <= c3 | c2 v c3 <= c2. [para(222(b,1),590(a,2)),rewrite(25(6))]. given #96 (T,wt=8): 597 c2 <= c1 | c2 v c3 <= c3. [para(247(b,1),590(a,2)),rewrite(25(6))]. given #97 (A,wt=36): 63 B(x,y ^ z,u) | (x ^ (y ^ z)) v (y ^ (z ^ u)) != y ^ z | (x v (y ^ z)) ^ ((y ^ z) v u) != y ^ z. [para(26(a,1),34(b,1,2))]. given #98 (T,wt=8): 598 c1 <= c2 | c1 v c3 <= c1. [para(421(b,1),590(a,2)),rewrite(25(6))]. given #99 (T,wt=9): 104 x v y <= x v (z v y). [para(45(a,1),99(a,2))]. given #100 (T,wt=9): 106 x ^ (y ^ z) <= x ^ y. [para(26(a,1),103(a,1))]. given #101 (T,wt=7): 736 x ^ y <= y ^ x. [para(85(a,1),106(a,1))]. given #102 (A,wt=28): 64 B(x v y,z,u) | ((x v y) ^ z) v (z ^ u) != z | (x v (y v z)) ^ (z v u) != z. [para(27(a,1),34(c,1,1))]. given #103 (T,wt=8): 740 c1 <= c2 | c3 <= c2 ^ c3. [para(73(a,1),736(a,1)),rewrite(24(7))]. given #104 (T,wt=8): 741 c1 <= c2 | c2 <= c1 ^ c2. [para(74(a,1),736(a,1)),rewrite(24(7))]. given #105 (T,wt=8): 742 c2 <= c3 | c3 <= c2 ^ c3. [para(75(a,1),736(a,1)),rewrite(24(7))]. given #106 (T,wt=8): 743 c2 <= c1 | c2 <= c2 ^ c3. [para(76(a,1),736(a,1)),rewrite(24(7))]. given #107 (A,wt=36): 65 B(x,y v z,u) | (x ^ (y v z)) v ((y v z) ^ u) != y v z | (x v (y v z)) ^ (y v (z v u)) != y v z. [para(27(a,1),34(c,1,2))]. given #108 (T,wt=8): 744 c1 <= c2 | c3 <= c1 ^ c3. [para(281(a,1),736(a,1)),rewrite(24(7))]. given #109 (T,wt=9): 110 x ^ (y v (z v x)) = x. [para(27(a,1),46(a,1,2))]. given #110 (T,wt=9): 117 x ^ (y ^ z) <= x ^ z. [para(43(a,1),105(a,1))]. given #111 (T,wt=9): 118 x v (y ^ (z ^ x)) = x. [para(26(a,1),50(a,1,2))]. given #112 (A,wt=14): 72 x ^ y <= z | x ^ (y ^ z) != x ^ y. [para(26(a,1),36(b,1))]. given #113 (T,wt=9): 127 x <= y v (z v (x v u)). [para(27(a,1),101(a,2))]. given #114 (T,wt=9): 128 x <= y v (z v (u v x)). [para(27(a,1),102(a,2,2))]. given #115 (T,wt=9): 139 x ^ y <= (x v z) ^ y. [para(47(a,1),105(a,1))]. given #116 (T,wt=9): 143 x ^ (y ^ (z ^ u)) <= z. [para(26(a,1),107(a,1))]. given #117 (A,wt=11): 77 x ^ (y ^ (x v z)) = y ^ x. [para(29(a,1),43(a,1,2)),flip(a)]. given #118 (T,wt=9): 146 x ^ (y ^ (z ^ u)) <= u. [para(26(a,1),116(a,1,2))]. given #119 (T,wt=9): 151 x ^ y <= z v (u v x). [para(27(a,1),129(a,2))]. given #120 (T,wt=9): 152 x ^ (y ^ z) <= u v y. [para(43(a,1),129(a,1))]. given #121 (T,wt=9): 154 x ^ (y ^ z) <= u v z. [para(26(a,1),131(a,1))]. given #122 (A,wt=36): 79 B(x,y ^ z,u) | (y ^ (x ^ z)) v (y ^ (z ^ u)) != y ^ z | (x v (y ^ z)) ^ ((y ^ z) v u) != y ^ z. [para(43(a,1),34(b,1,1)),rewrite(26(6))]. given #123 (T,wt=9): 155 x ^ y <= z v (u v y). [para(27(a,1),131(a,2))]. given #124 (T,wt=9): 174 x ^ (y ^ z) <= y v u. [para(43(a,1),144(a,1))]. given #125 (T,wt=9): 175 x ^ y <= z v (x v u). [para(45(a,1),144(a,2))]. given #126 (T,wt=9): 176 x ^ (y ^ z) <= z v u. [para(26(a,1),147(a,1))]. given #127 (A,wt=28): 80 B(x,y,z ^ u) | (x ^ y) v (z ^ (y ^ u)) != y | (x v y) ^ (y v (z ^ u)) != y. [para(43(a,1),34(b,1,2))]. given #128 (T,wt=9): 179 x ^ y <= z v (y v u). [para(45(a,1),147(a,2))]. given #129 (T,wt=9): 251 c2 <= c1 | c3 <= c2 | c3 != c2. [para(76(a,1),71(b,1)),flip(c)]. given #130 (T,wt=9): 266 (x ^ y) v z <= x v z. [para(52(a,1),99(a,2))]. given #131 (T,wt=9): 424 c1 <= c2 | c1 <= c3 | c3 != c1. [para(281(a,1),36(b,1))]. given #132 (A,wt=12): 81 x <= y ^ z | y ^ (x ^ z) != x. [para(43(a,1),36(b,1))]. given #133 (T,wt=9): 584 x v y <= y v (x v z). [para(25(a,1),100(a,1))]. given #134 (T,wt=9): 585 x v y <= y v (z v x). [para(25(a,1),100(a,2)),rewrite(27(3))]. given #135 (T,wt=9): 712 x v y <= z v (y v x). [para(25(a,1),104(a,2)),rewrite(27(3))]. given #136 (T,wt=9): 715 x v (y ^ z) <= x v y. [para(31(a,1),104(a,2,2))]. given #137 (A,wt=15): 88 B(x,y,y ^ z) | (x ^ y) v (y ^ z) != y. [back_rewrite(69),rewrite(83(5))]. given #138 (T,wt=9): 717 x v (y ^ z) <= x v z. [para(50(a,1),104(a,2,2))]. given #139 (T,wt=9): 727 x ^ (y ^ z) <= z ^ x. [para(24(a,1),106(a,1)),rewrite(26(2))]. given #140 (T,wt=9): 728 x ^ (y ^ z) <= y ^ x. [para(24(a,1),106(a,2))]. given #141 (T,wt=9): 880 x ^ (y ^ z) <= z ^ y. [para(24(a,1),117(a,1)),rewrite(26(2))]. given #142 (A,wt=17): 89 B(x,x ^ y,z) | x ^ ((x ^ y) v z) != x ^ y. [back_rewrite(68),rewrite(83(4),51(6)),xx(b)]. given #143 (T,wt=9): 883 x ^ y <= x ^ (y v z). [para(29(a,1),117(a,1,2))]. given #144 (T,wt=9): 885 x ^ y <= x ^ (z v y). [para(46(a,1),117(a,1,2))]. given #145 (T,wt=9): 946 x ^ y <= (y v z) ^ x. [para(24(a,1),139(a,1))]. given #146 (T,wt=9): 947 x ^ y <= y ^ (x v z). [para(24(a,1),139(a,2))]. given #147 (A,wt=11): 91 x v (y v (x ^ z)) = y v x. [para(31(a,1),45(a,1,2)),flip(a)]. given #148 (T,wt=9): 948 x ^ y <= (z v x) ^ y. [para(25(a,1),139(a,2,1))]. given #149 (T,wt=9): 951 x <= (x v y) ^ (x v z). [para(29(a,1),139(a,1))]. given #150 (T,wt=9): 955 x <= (x v y) ^ (z v x). [para(46(a,1),139(a,1))]. given #151 (T,wt=9): 1178 (x ^ y) v z <= y v z. [para(24(a,1),266(a,1,1))]. given #152 (A,wt=36): 92 B(x,y v z,u) | (x ^ (y v z)) v ((y v z) ^ u) != y v z | (y v (x v z)) ^ (y v (z v u)) != y v z. [para(45(a,1),34(c,1,1)),rewrite(27(13))]. given #153 (T,wt=9): 1179 x v (y ^ z) <= y v x. [para(25(a,1),266(a,1))]. given #154 (T,wt=9): 1180 (x ^ y) v z <= z v x. [para(25(a,1),266(a,2))]. given #155 (T,wt=9): 1183 (x ^ y) v (x ^ z) <= x. [para(31(a,1),266(a,2))]. given #156 (T,wt=9): 1187 (x ^ y) v (z ^ x) <= x. [para(50(a,1),266(a,2))]. given #157 (A,wt=28): 93 B(x,y,z v u) | (x ^ y) v (y ^ (z v u)) != y | (x v y) ^ (z v (y v u)) != y. [para(45(a,1),34(c,1,2))]. given #158 (T,wt=9): 1231 (x ^ y) v z <= z v y. [para(50(a,1),585(a,2,2))]. given #159 (T,wt=9): 1268 c1 <= c2 | B(c2,c3,c3 ^ x). [para(73(a,1),88(b,1,1)),rewrite(31(12)),xx(c)]. given #160 (T,wt=9): 1271 c1 <= c2 | B(c1,c2,c2 ^ x). [para(74(a,1),88(b,1,1)),rewrite(31(12)),xx(c)]. given #161 (T,wt=3): 1642 c1 <= c2. [para(73(a,1),1271(b,3)),merge(b),unit_del(b,37)]. given #162 (A,wt=15): 97 B(x,y,y v z) | (x v y) ^ (y v z) != y. [back_rewrite(67),rewrite(94(5))]. given #163 (T,wt=5): 1643 c1 ^ c2 = c1. [hyper(35,a,1642,a)]. given #164 (T,wt=5): 1664 c1 v c2 = c2. [para(1643(a,1),50(a,1,2)),rewrite(25(3))]. given #165 (T,wt=5): 1665 x ^ c1 <= c2. [para(1643(a,1),116(a,1,2))]. given #166 (T,wt=5): 1666 c1 <= x v c2. [para(1643(a,1),131(a,1))]. given #167 (A,wt=17): 98 B(x,x v y,z) | x v ((x v y) ^ z) != x v y. [back_rewrite(66),rewrite(94(9),49(11)),xx(c)]. given #168 (T,wt=5): 1667 c1 <= c2 v x. [para(1643(a,1),147(a,1))]. given #169 (T,wt=5): 1705 c1 ^ x <= c2. [para(1664(a,1),144(a,2))]. given #170 (T,wt=6): 1668 c2 <= c1 | c2 != c1. [para(1643(a,1),71(b,1)),flip(b)]. given #171 (T,wt=6): 1671 c2 <= c1 | c1 <= c3. [para(1643(a,1),248(b,1))]. given #172 (A,wt=11): 108 x ^ ((y v x) ^ z) = x ^ z. [para(46(a,1),26(a,1,1)),flip(a)]. given #173 (T,wt=6): 1719 B(c1,c2,c2 v x). [para(1664(a,1),97(b,1,1)),rewrite(29(9)),xx(b)]. given #174 (T,wt=3): 1805 c2 <= c1. [para(247(b,1),1719(a,3)),unit_del(b,37)]. ============================== PROOF ================================= % Proof 1 at 0.22 (+ 0.01) seconds. % Length of proof is 45. % Level of proof is 12. % Maximum clause weight is 22. % Given clauses 174. 1 (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)) # label(non_clause). [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)) # 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 (A(a,x,b) -> B(a,x,b))) # label(goal). [goal]. 9 -A(x,y,z) | x <= y | z <= y. [clausify(1)]. 10 -A(x,y,z) | x <= y | y <= x. [clausify(1)]. 12 -A(x,y,z) | y <= z | y <= x. [clausify(1)]. 14 A(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))]. 34 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 35 -(x <= y) | x ^ y = x. [clausify(6)]. 37 -B(c1,c2,c3). [deny(7)]. 38 c1 <= c2 | c3 <= c2. [resolve(14,a,9,a)]. 39 c1 <= c2 | c2 <= c1. [resolve(14,a,10,a)]. 41 c2 <= c3 | c2 <= c1. [resolve(14,a,12,a)]. 46 x ^ (y v x) = x. [para(25(a,1),29(a,1,2))]. 50 x v (y ^ x) = x. [para(24(a,1),31(a,1,2))]. 54 x ^ x = x. [para(31(a,1),29(a,1,2))]. 55 x v x = x. [para(29(a,1),31(a,1,2))]. 67 B(x,y,y v z) | (x v y) ^ (y v (y v z)) != y. [para(29(a,1),34(b,1,2)),rewrite(25(4),50(4)),xx(b)]. 69 B(x,y,y ^ z) | (x ^ y) v (y ^ (y ^ z)) != y. [para(31(a,1),34(c,1,2)),rewrite(24(9),46(9)),xx(c)]. 73 c2 ^ c3 = c3 | c1 <= c2. [hyper(35,a,38,b),rewrite(24(3))]. 74 c1 ^ c2 = c2 | c1 <= c2. [hyper(35,a,39,b),rewrite(24(3))]. 76 c2 ^ c3 = c2 | c2 <= c1. [hyper(35,a,41,a)]. 83 x ^ (x ^ y) = x ^ y. [para(54(a,1),26(a,1,1)),flip(a)]. 86 B(x,x,y). [para(54(a,1),34(b,1,1)),rewrite(31(3),55(3),29(4)),xx(b),xx(c)]. 88 B(x,y,y ^ z) | (x ^ y) v (y ^ z) != y. [back_rewrite(69),rewrite(83(5))]. 94 x v (x v y) = x v y. [para(55(a,1),27(a,1,1)),flip(a)]. 97 B(x,y,y v z) | (x v y) ^ (y v z) != y. [back_rewrite(67),rewrite(94(5))]. 247 c2 <= c1 | c2 v c3 = c3. [para(76(a,1),50(a,1,2)),rewrite(25(6))]. 1271 c1 <= c2 | B(c1,c2,c2 ^ x). [para(74(a,1),88(b,1,1)),rewrite(31(12)),xx(c)]. 1642 c1 <= c2. [para(73(a,1),1271(b,3)),merge(b),unit_del(b,37)]. 1643 c1 ^ c2 = c1. [hyper(35,a,1642,a)]. 1664 c1 v c2 = c2. [para(1643(a,1),50(a,1,2)),rewrite(25(3))]. 1719 B(c1,c2,c2 v x). [para(1664(a,1),97(b,1,1)),rewrite(29(9)),xx(b)]. 1805 c2 <= c1. [para(247(b,1),1719(a,3)),unit_del(b,37)]. 1806 c2 = c1. [hyper(35,a,1805,a),rewrite(24(3),1643(3)),flip(a)]. 1916 $F. [back_rewrite(37),rewrite(1806(2)),unit_del(a,86)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=174. Generated=6490. Kept=1890. proofs=1. Usable=111. Sos=1035. Demods=131. Limbo=110, Disabled=666. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=4599. Back_subsumed=432. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=148 (6 lex), Back_demodulated=200. Back_unit_deleted=0. Demod_attempts=73230. Demod_rewrites=9351. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=103406. Nonunit_bsub_feature_tests=27921. Megabytes=1.61. User_CPU=0.22, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 27050 exit (max_proofs) Fri Apr 13 09:19:46 2007