============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11448 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:20 2006 The command was "/home/mccune/bin/prover9 -f head.in bcs.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 bcs.in formulas(goals). (all a all x all b (B(a,x,b) -> CS(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 (B(a,x,b) -> CS(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)]. B(c1,c2,c3). [deny(7)]. -CS(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)]. 17 B(c1,c2,c3). [deny(7)]. Derived: (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(17,a,15,a)]. Derived: (c1 v c2) ^ (c2 v c3) = c2. [resolve(17,a,16,a)]. Eliminating C/3 18 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 19 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 20 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. 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)]. Eliminating <=/2 24 x <= y | x ^ y != x. [clausify(6)]. 25 -(x <= y) | x ^ y = x. [clausify(6)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ CS, =, D, 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). 26 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 27 x v y = y v x # label("commutativity_join"). [assumption]. 28 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 29 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 31 x ^ (x v y) = x. [copy(30),rewrite(26(2))]. 33 x v (x ^ y) = x. [copy(32),rewrite(27(2))]. 34 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 35 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. 36 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 37 -CS(c1,c2,c3). [deny(7)]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(17,a,15,a)]. 39 (c1 v c2) ^ (c2 v c3) = c2. [resolve(17,a,16,a)]. end_of_list. formulas(demodulators). 26 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 27 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 28 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 29 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 31 x ^ (x v y) = x. [copy(30),rewrite(26(2))]. 33 x v (x ^ y) = x. [copy(32),rewrite(27(2))]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(17,a,15,a)]. 39 (c1 v c2) ^ (c2 v c3) = c2. [resolve(17,a,16,a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 26 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. given #2 (I,wt=7): 27 x v y = y v x # label("commutativity_join"). [assumption]. given #3 (I,wt=11): 28 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 40 x ^ (y ^ z) = z ^ (x ^ y). [para(28(a,1),26(a,1))]. given #4 (I,wt=11): 29 (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: 42 x v (y v z) = z v (x v y). [para(29(a,1),27(a,1))]. given #5 (I,wt=7): 31 x ^ (x v y) = x. [copy(30),rewrite(26(2))]. given #6 (I,wt=7): 33 x v (x ^ y) = x. [copy(32),rewrite(27(2))]. given #7 (I,wt=13): 34 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. given #8 (I,wt=11): 35 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. given #9 (I,wt=20): 36 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. given #10 (I,wt=4): 37 -CS(c1,c2,c3). [deny(7)]. given #11 (I,wt=9): 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(17,a,15,a)]. given #12 (I,wt=9): 39 (c1 v c2) ^ (c2 v c3) = c2. [resolve(17,a,16,a)]. given #13 (F,wt=5): 52 x ^ x = x. [para(33(a,1),31(a,1,2))]. given #14 (T,wt=4): 76 CS(x,x,x). [para(52(a,1),36(b,1)),rewrite(53(2),53(3),52(3)),xx(b),xx(c)]. given #15 (T,wt=5): 53 x v x = x. [para(31(a,1),33(a,1,2))]. given #16 (A,wt=11): 41 x ^ (y ^ z) = y ^ (x ^ z). [para(26(a,1),28(a,1,1)),rewrite(28(2))]. given #17 (F,wt=4): 81 CS(x,x,y). [para(53(a,1),36(b,1,1)),rewrite(31(3),26(4),31(4)),xx(b),xx(c)]. given #18 (F,wt=4): 82 CS(x,y,y). [para(53(a,1),36(b,1,2)),rewrite(26(3),44(3),26(4),44(4)),xx(b),xx(c)]. given #19 (T,wt=6): 84 CS(x,x v y,y). [back_rewrite(77),rewrite(78(4),80(5),52(5)),xx(b)]. given #20 (T,wt=6): 91 CS(x,y v x,y). [para(27(a,1),84(a,2))]. given #21 (A,wt=11): 43 x v (y v z) = y v (x v z). [para(27(a,1),29(a,1,1)),rewrite(29(2))]. given #22 (F,wt=7): 44 x ^ (y v x) = x. [para(27(a,1),31(a,1,2))]. given #23 (F,wt=7): 48 x v (y ^ x) = x. [para(26(a,1),33(a,1,2))]. given #24 (T,wt=8): 93 CS(c1 ^ c2,c2,c2 ^ c3). [para(38(a,1),84(a,2))]. given #25 (T,wt=8): 96 CS(c2 ^ c3,c2,c1 ^ c2). [para(38(a,1),91(a,2))]. given #26 (A,wt=11): 45 x ^ ((x v y) ^ z) = x ^ z. [para(31(a,1),28(a,1,1)),flip(a)]. given #27 (F,wt=9): 73 x ^ (x ^ y) = x ^ y. [para(52(a,1),28(a,1,1)),flip(a)]. given #28 (F,wt=9): 75 x ^ (y ^ x) = y ^ x. [para(52(a,1),28(a,2,2)),rewrite(26(2))]. given #29 (T,wt=9): 78 x v (x v y) = x v y. [para(53(a,1),29(a,1,1)),flip(a)]. given #30 (T,wt=9): 80 x v (y v x) = y v x. [para(53(a,1),29(a,2,2)),rewrite(27(2))]. given #31 (A,wt=13): 46 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(31(a,1),28(a,1)),flip(a)]. given #32 (F,wt=9): 88 x v (y ^ (x ^ z)) = x. [para(41(a,1),33(a,1,2))]. given #33 (F,wt=9): 98 x ^ (y v (x v z)) = x. [para(43(a,1),31(a,1,2))]. given #34 (T,wt=9): 108 x ^ (y v (z v x)) = x. [para(29(a,1),44(a,1,2))]. given #35 (T,wt=9): 113 x v (y ^ (z ^ x)) = x. [para(28(a,1),48(a,1,2))]. given #36 (A,wt=13): 47 (x v y) ^ (x v (y v z)) = x v y. [para(29(a,1),31(a,1,2))]. given #37 (F,wt=9): 124 c1 ^ (c2 v c3) = c1 ^ c2. [para(39(a,1),45(a,1,2)),flip(a)]. given #38 (F,wt=10): 92 CS(x v y,x v (y v z),z). [para(29(a,1),84(a,2))]. given #39 (T,wt=8): 206 CS(x v y,y v x,x). [para(80(a,1),92(a,2))]. given #40 (T,wt=10): 95 CS(x,y v (z v x),y v z). [para(29(a,1),91(a,2))]. given #41 (A,wt=13): 49 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(28(a,1),33(a,1,2))]. given #42 (F,wt=8): 220 CS(x,y v x,x v y). [para(80(a,1),95(a,2))]. given #43 (F,wt=10): 104 CS(x,y v (x v z),y v z). [para(43(a,1),84(a,2))]. given #44 (T,wt=10): 105 CS(x v y,x v (z v y),z). [para(43(a,1),91(a,2))]. given #45 (T,wt=10): 198 CS(x v y,y v (x v z),z). [para(27(a,1),92(a,1))]. given #46 (A,wt=11): 50 x v ((x ^ y) v z) = x v z. [para(33(a,1),29(a,1,1)),flip(a)]. given #47 (F,wt=9): 276 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),50(a,1,2)),flip(a)]. given #48 (F,wt=8): 292 CS(c1,c1 v c2,c2 ^ c3). [para(276(a,1),84(a,2))]. given #49 (T,wt=8): 293 CS(c2 ^ c3,c1 v c2,c1). [para(276(a,1),91(a,2))]. given #50 (T,wt=10): 199 CS(x v y,y v (z v x),z). [para(27(a,1),92(a,2)),rewrite(29(3))]. given #51 (A,wt=13): 51 x v (y v ((x v y) ^ z)) = x v y. [para(33(a,1),29(a,1)),flip(a)]. given #52 (F,wt=8): 311 CS(x v y,y v x,y). [para(78(a,1),199(a,2))]. given #53 (F,wt=10): 212 CS(x,y v (x v z),z v y). [para(27(a,1),95(a,2)),rewrite(29(2))]. given #54 (T,wt=8): 362 CS(x,x v y,y v x). [para(78(a,1),212(a,2))]. given #55 (T,wt=10): 213 CS(x,y v (z v x),z v y). [para(27(a,1),95(a,3))]. given #56 (A,wt=20): 54 CS(x,y,z) | (y v z) ^ (x v y) != y | (x v z) ^ y != y. [para(26(a,1),36(b,1))]. given #57 (F,wt=10): 239 CS(x,x v (y v z),z v y). [para(27(a,1),104(a,2)),rewrite(29(2))]. given #58 (F,wt=10): 242 CS(x,y v x,y v (x ^ z)). [para(33(a,1),104(a,2,2))]. given #59 (T,wt=10): 245 CS(x,y v x,y v (z ^ x)). [para(48(a,1),104(a,2,2))]. given #60 (T,wt=8): 445 CS(c3,c3 v (c1 ^ c2),c2). [para(38(a,1),245(a,3)),rewrite(27(6))]. given #61 (A,wt=20): 55 CS(x,y,z) | (x v y) ^ (y v z) != y | y ^ (x v z) != y. [para(26(a,1),36(c,1))]. given #62 (F,wt=8): 456 CS(c3,c1 v c3,c1 v c2). [para(276(a,1),245(a,3))]. given #63 (F,wt=8): 481 CS(x,x v y,y v z). [para(47(a,1),55(c,1)),rewrite(78(5),43(7),29(6),137(7),47(7)),xx(b),xx(c)]. given #64 (T,wt=8): 489 CS(x,y v x,y v z). [para(27(a,1),481(a,2))]. given #65 (T,wt=8): 490 CS(x,x v y,z v y). [para(27(a,1),481(a,3))]. given #66 (A,wt=20): 56 CS(x,y,z) | (y v x) ^ (y v z) != y | (x v z) ^ y != y. [para(27(a,1),36(b,1,1))]. given #67 (F,wt=8): 499 CS(x,y v x,z v y). [para(27(a,1),489(a,3))]. given #68 (F,wt=8): 501 CS(x ^ y,x,x v z). [para(33(a,1),489(a,2))]. given #69 (T,wt=8): 506 CS(x ^ y,y,y v z). [para(48(a,1),489(a,2))]. given #70 (T,wt=8): 516 CS(x,x v (y ^ z),y). [para(33(a,1),490(a,3))]. given #71 (A,wt=20): 57 CS(x,y,z) | (x v y) ^ (z v y) != y | (x v z) ^ y != y. [para(27(a,1),36(b,1,2))]. given #72 (F,wt=8): 520 CS(x,x v (y ^ z),z). [para(48(a,1),490(a,3))]. given #73 (F,wt=6): 641 CS(c1 ^ c2,c2,c3). [para(38(a,1),520(a,2))]. given #74 (T,wt=6): 646 CS(c1,c1 v c2,c3). [para(276(a,1),520(a,2))]. given #75 (T,wt=8): 569 CS(x ^ y,x,z v x). [para(33(a,1),499(a,2))]. given #76 (A,wt=20): 58 CS(x,y,z) | (x v y) ^ (y v z) != y | (z v x) ^ y != y. [para(27(a,1),36(c,1,1))]. given #77 (F,wt=8): 570 CS(x,(y ^ z) v x,y). [para(33(a,1),499(a,3))]. given #78 (F,wt=6): 705 CS(c2 ^ c3,c2,c1). [para(38(a,1),570(a,2))]. given #79 (T,wt=8): 574 CS(x ^ y,y,z v y). [para(48(a,1),499(a,2))]. given #80 (T,wt=8): 575 CS(x,(y ^ z) v x,z). [para(48(a,1),499(a,3))]. given #81 (A,wt=26): 59 CS(x v y,z,u) | (x v (y v z)) ^ (z v u) != z | (x v (y v u)) ^ z != z. [para(29(a,1),36(b,1,1)),rewrite(29(9))]. given #82 (F,wt=9): 648 c2 ^ (c3 v (c1 ^ c2)) = c2. [hyper(35,a,641,a),rewrite(27(5),26(7))]. given #83 (F,wt=6): 802 CS(c3,c2,c1 ^ c2). [para(648(a,1),55(c,1)),rewrite(27(9),48(14),26(11),31(11)),xx(b),xx(c)]. given #84 (T,wt=9): 801 c3 v (c1 ^ c2) = c2 v c3. [para(648(a,1),48(a,1,2)),rewrite(27(7),120(7),27(3)),flip(a)]. given #85 (T,wt=6): 830 CS(c3,c2 v c3,c1). [para(801(a,1),516(a,2))]. given #86 (A,wt=32): 60 CS(x,y v z,u) | (x v (y v z)) ^ (y v (z v u)) != y v z | (x v u) ^ (y v z) != y v z. [para(29(a,1),36(b,1,2))]. given #87 (F,wt=8): 807 CS(c3,c2 v c3,c1 ^ c2). [para(801(a,1),84(a,2))]. given #88 (F,wt=8): 808 CS(c1 ^ c2,c2 v c3,c3). [para(801(a,1),91(a,2))]. given #89 (T,wt=10): 250 CS(x v y,z v (y v x),z). [para(27(a,1),105(a,2)),rewrite(29(3))]. given #90 (T,wt=10): 253 CS(x v (y ^ z),x v y,y). [para(33(a,1),105(a,2,2))]. given #91 (A,wt=17): 62 CS(x,x ^ y,z) | x ^ ((x ^ y) v z) != x ^ y. [para(33(a,1),36(b,1,1)),rewrite(41(10),45(10)),xx(c)]. given #92 (F,wt=8): 893 CS(c2 v c3,c1 v c3,c1). [para(801(a,1),253(a,1)),rewrite(27(6))]. given #93 (F,wt=8): 898 CS(c1,c1 ^ c2,c2 ^ c3). [para(38(a,1),62(b,1,2)),xx(b)]. given #94 (T,wt=10): 256 CS(x v (y ^ z),x v z,z). [para(48(a,1),105(a,2,2))]. given #95 (T,wt=8): 924 CS(c1 v c2,c1 v c3,c3). [para(276(a,1),256(a,1))]. given #96 (A,wt=15): 63 CS(x,y,y ^ z) | y ^ (x v (y ^ z)) != y. [para(33(a,1),36(b,1,2)),rewrite(26(4),44(4),26(6)),xx(b)]. given #97 (F,wt=6): 936 CS(c1,c2,c2 ^ c3). [para(276(a,1),63(b,1,2)),rewrite(44(11)),xx(b)]. given #98 (F,wt=10): 262 CS(x v y,y v x,x ^ z). [para(33(a,1),198(a,2,2))]. given #99 (T,wt=10): 266 CS(x v y,y v x,z ^ x). [para(48(a,1),198(a,2,2))]. given #100 (T,wt=10): 278 CS((x ^ y) v z,x v z,x). [para(50(a,1),91(a,2))]. given #101 (A,wt=22): 64 CS(x,y,x ^ z) | (x v y) ^ (y v (x ^ z)) != y | x ^ y != y. [para(33(a,1),36(c,1,1))]. given #102 (F,wt=10): 303 CS((x ^ y) v z,z v x,x). [para(33(a,1),199(a,2,2))]. given #103 (F,wt=10): 308 CS(x,(y ^ x) v (z v x),z). [para(48(a,1),199(a,1))]. given #104 (T,wt=10): 309 CS((x ^ y) v z,z v y,y). [para(48(a,1),199(a,2,2))]. given #105 (T,wt=10): 321 CS(x v y,y v x,y ^ z). [para(50(a,1),199(a,2))]. given #106 (A,wt=13): 65 (c1 ^ c2) v ((c2 ^ c3) v x) = c2 v x. [para(38(a,1),29(a,1,1)),flip(a)]. given #107 (F,wt=10): 360 CS(x,(y ^ z) v (x v z),z). [para(48(a,1),212(a,3))]. given #108 (F,wt=10): 371 CS(x ^ y,x v z,z v x). [para(50(a,1),212(a,2))]. given #109 (T,wt=10): 384 CS(x ^ y,z v x,x v z). [para(33(a,1),213(a,2,2))]. given #110 (T,wt=10): 388 CS(x ^ y,z v y,y v z). [para(48(a,1),213(a,2,2))]. given #111 (A,wt=32): 66 CS(c1 ^ c2,c2 ^ c3,x) | c2 ^ ((c2 ^ c3) v x) != c2 ^ c3 | c2 ^ (c3 ^ ((c1 ^ c2) v x)) != c2 ^ c3. [para(38(a,1),36(b,1,1)),rewrite(41(25),26(24))]. given #112 (F,wt=8): 1120 CS(c1 ^ c2,c2 ^ c3,c3). [para(44(a,1),66(c,1,2)),rewrite(27(14),48(14)),xx(b),xx(c)]. given #113 (F,wt=10): 493 CS(c1 ^ c2,c2,(c2 ^ c3) v x). [para(38(a,1),481(a,2))]. given #114 (T,wt=10): 496 CS(x,x v y,z v (y v u)). [para(43(a,1),481(a,3))]. given #115 (T,wt=10): 497 CS(c1,c1 v c2,(c2 ^ c3) v x). [para(276(a,1),481(a,2))]. given #116 (A,wt=32): 67 CS(x,c1 ^ c2,c2 ^ c3) | c2 ^ (x v (c1 ^ c2)) != c1 ^ c2 | c1 ^ (c2 ^ (x v (c2 ^ c3))) != c1 ^ c2. [para(38(a,1),36(b,1,2)),rewrite(26(13),26(25),28(25))]. given #117 (F,wt=10): 502 CS(c2 ^ c3,c2,(c1 ^ c2) v x). [para(38(a,1),489(a,2))]. given #118 (F,wt=10): 505 CS(x,y v x,z v (y v u)). [para(43(a,1),489(a,3))]. given #119 (T,wt=10): 507 CS(x ^ (y ^ z),y,y v u). [para(88(a,1),489(a,2))]. given #120 (T,wt=10): 508 CS(x ^ (y ^ z),z,z v u). [para(113(a,1),489(a,2))]. given #121 (A,wt=26): 68 CS(c1 ^ c2,x,c2 ^ c3) | ((c1 ^ c2) v x) ^ (x v (c2 ^ c3)) != x | c2 ^ x != x. [para(38(a,1),36(c,1,1))]. given #122 (F,wt=10): 511 CS(c2 ^ c3,c1 v c2,c1 v x). [para(276(a,1),489(a,2))]. given #123 (F,wt=10): 515 CS(x,x v y,z v (u v y)). [para(29(a,1),490(a,3))]. given #124 (T,wt=10): 517 CS(c1 ^ c2,c2,x v (c2 ^ c3)). [para(38(a,1),490(a,2))]. given #125 (T,wt=10): 521 CS(x,x v (y ^ (z ^ u)),z). [para(88(a,1),490(a,3))]. given #126 (A,wt=13): 69 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(39(a,1),28(a,1,1)),flip(a)]. given #127 (F,wt=10): 522 CS(x,x v (y ^ (z ^ u)),u). [para(113(a,1),490(a,3))]. given #128 (F,wt=10): 525 CS(c1,c1 v c2,x v (c2 ^ c3)). [para(276(a,1),490(a,2))]. given #129 (T,wt=10): 568 CS(x,y v x,z v (u v y)). [para(29(a,1),499(a,3))]. given #130 (T,wt=10): 571 CS(c2 ^ c3,c2,x v (c1 ^ c2)). [para(38(a,1),499(a,2))]. given #131 (A,wt=13): 70 (c2 v c3) ^ (x ^ (c1 v c2)) = x ^ c2. [para(39(a,1),28(a,2,2)),rewrite(26(8))]. given #132 (F,wt=10): 576 CS(x ^ (y ^ z),y,u v y). [para(88(a,1),499(a,2))]. given #133 (F,wt=10): 577 CS(x,(y ^ (z ^ u)) v x,z). [para(88(a,1),499(a,3))]. given #134 (T,wt=10): 578 CS(x ^ (y ^ z),z,u v z). [para(113(a,1),499(a,2))]. given #135 (T,wt=10): 579 CS(x,(y ^ (z ^ u)) v x,u). [para(113(a,1),499(a,3))]. given #136 (A,wt=11): 71 CS(c1,c2,c3) | c2 ^ (c1 v c3) != c2. [para(39(a,1),36(b,1)),rewrite(26(12)),xx(b)]. given #137 (F,wt=10): 584 CS(c2 ^ c3,c1 v c2,x v c1). [para(276(a,1),499(a,2))]. given #138 (F,wt=10): 590 CS(x ^ y,x,z v (x v u)). [para(43(a,1),501(a,3))]. given #139 (T,wt=10): 594 CS(x ^ y,y,z v (y v u)). [para(43(a,1),506(a,3))]. given #140 (T,wt=10): 651 CS(x ^ y,x,z v (u v x)). [para(29(a,1),569(a,3))]. given #141 (A,wt=11): 85 CS(c1,c2 v c3,c2) | c2 v c3 != c2. [back_rewrite(72),rewrite(78(16),26(15),44(15)),xx(b)]. given #142 (F,wt=10): 652 CS(x ^ (y ^ z),x ^ y,x). [para(33(a,1),569(a,3)),rewrite(28(2))]. given #143 (F,wt=8): 1407 CS(x ^ y,y ^ x,y). [para(75(a,1),652(a,1))]. given #144 (T,wt=10): 654 CS(x ^ (y ^ z),x ^ y,y). [para(48(a,1),569(a,3)),rewrite(28(2))]. given #145 (T,wt=8): 1423 CS(x ^ y,y ^ x,x). [para(75(a,1),654(a,1))]. given #146 (A,wt=17): 86 CS(x,x v (y v z),y) | x v (y v z) != x v y. [back_rewrite(61),rewrite(78(6),44(9)),xx(b)]. given #147 (F,wt=10): 707 CS(x ^ (y ^ z),y ^ z,y). [para(48(a,1),570(a,2))]. given #148 (F,wt=10): 712 CS(x ^ y,y,z v (u v y)). [para(29(a,1),574(a,3))]. given #149 (T,wt=10): 715 CS(x ^ (y ^ z),y ^ z,z). [para(48(a,1),574(a,3))]. given #150 (T,wt=10): 823 CS(c3,c2 v c3,(c1 ^ c2) v x). [para(801(a,1),481(a,2))]. given #151 (A,wt=11): 87 x ^ (y ^ (x v z)) = y ^ x. [para(31(a,1),41(a,1,2)),flip(a)]. given #152 (F,wt=10): 824 CS(c1 ^ c2,c2 v c3,c3 v x). [para(801(a,1),489(a,2))]. given #153 (F,wt=10): 825 CS(c3,c2 v c3,x v (c1 ^ c2)). [para(801(a,1),490(a,2))]. given #154 (T,wt=10): 829 CS(c1 ^ c2,c2 v c3,x v c3). [para(801(a,1),499(a,2))]. given #155 (T,wt=10): 886 CS(x v (y ^ z),y v x,y). [para(50(a,1),250(a,2))]. given #156 (A,wt=32): 89 CS(x,y ^ z,u) | (x v (y ^ z)) ^ ((y ^ z) v u) != y ^ z | y ^ ((x v u) ^ z) != y ^ z. [para(41(a,1),36(c,1))]. given #157 (F,wt=10): 897 CS(x,x ^ y,x ^ (y ^ z)). [para(33(a,1),62(b,1,2)),rewrite(28(3),73(6)),xx(b)]. given #158 (F,wt=8): 1581 CS(c1 v c2,c2,c2 ^ x). [para(39(a,1),897(a,2)),rewrite(69(12))]. given #159 (T,wt=8): 1587 CS(x,x ^ y,y ^ x). [para(75(a,1),897(a,3))]. given #160 (T,wt=8): 1593 CS(c1 v c2,c2,x ^ c2). [para(26(a,1),1581(a,3))]. given #161 (A,wt=13): 90 (c1 v c2) ^ (x ^ (c2 v c3)) = x ^ c2. [para(39(a,1),41(a,1,2)),flip(a)]. given #162 (F,wt=9): 1601 c3 ^ (c1 v c2) = c2 ^ c3. [para(44(a,1),90(a,1,2)),rewrite(26(5),26(8))]. given #163 (F,wt=9): 1634 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(1601(a,1),87(a,1,2)),rewrite(26(8))]. given #164 (T,wt=7): 1649 c2 v (c1 ^ c3) = c2. [para(1634(a,1),88(a,1,2))]. given #165 (T,wt=8): 1660 CS(c1 ^ c3,c2,c2 v x). [para(1634(a,1),507(a,1))]. given #166 (A,wt=11): 94 (x v y) ^ (y v x) = y v x. [hyper(35,a,91,a)]. given #167 (F,wt=8): 1662 CS(x,x v (c1 ^ c3),c2). [para(1634(a,1),521(a,2,2))]. given #168 (F,wt=8): 1664 CS(c1 ^ c3,c2,x v c2). [para(1634(a,1),576(a,1))]. given #169 (T,wt=8): 1665 CS(x,(c1 ^ c3) v x,c2). [para(1634(a,1),577(a,2,1))]. given #170 (T,wt=8): 1669 CS(c1 ^ c3,c1 ^ c2,c1). [para(1634(a,1),652(a,1))]. given #171 (A,wt=14): 97 CS(x,y,x) | y v x != y | x ^ y != y. [back_rewrite(83),rewrite(94(4))]. given #172 (F,wt=8): 1670 CS(c1 ^ c3,c1 ^ c2,c2). [para(1634(a,1),654(a,1))]. given #173 (F,wt=8): 1672 CS(c1 ^ c3,c2 ^ c3,c2). [para(1634(a,1),707(a,1))]. given #174 (T,wt=8): 1675 CS(c1 ^ c3,c2 ^ c3,c3). [para(1634(a,1),715(a,1))]. given #175 (T,wt=8): 1676 CS(c1,c1 ^ c2,c1 ^ c3). [para(1634(a,1),897(a,3))]. given #176 (A,wt=11): 99 x v (y v (x ^ z)) = y v x. [para(33(a,1),43(a,1,2)),flip(a)]. given #177 (F,wt=8): 1728 CS(x v y,y v x,z). [para(94(a,1),62(b,1,2,1)),rewrite(94(4),29(6),185(7),94(7)),xx(b)]. given #178 (F,wt=9): 1821 c1 v (c2 v c3) = c1 v c3. [para(801(a,1),99(a,1,2)),rewrite(27(8))]. ============================== PROOF ================================= % Proof 1 at 0.20 (+ 0.00) seconds. % Length of proof is 39. % Level of proof is 14. % Maximum clause weight is 20. % Given clauses 178. 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]. 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]. 7 (all a all x all b (B(a,x,b) -> CS(a,x,b))). [goal]. 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)]. 17 B(c1,c2,c3). [deny(7)]. 26 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 27 x v y = y v x # label("commutativity_join"). [assumption]. 29 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 30 (x v y) ^ x = x # label("absorption_1"). [assumption]. 31 x ^ (x v y) = x. [copy(30),rewrite(26(2))]. 32 (x ^ y) v x = x # label("absorption_2"). [assumption]. 33 x v (x ^ y) = x. [copy(32),rewrite(27(2))]. 35 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. 36 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 37 -CS(c1,c2,c3). [deny(7)]. 38 (c1 ^ c2) v (c2 ^ c3) = c2. [resolve(17,a,15,a)]. 39 (c1 v c2) ^ (c2 v c3) = c2. [resolve(17,a,16,a)]. 43 x v (y v z) = y v (x v z). [para(27(a,1),29(a,1,1)),rewrite(29(2))]. 47 (x v y) ^ (x v (y v z)) = x v y. [para(29(a,1),31(a,1,2))]. 48 x v (y ^ x) = x. [para(26(a,1),33(a,1,2))]. 53 x v x = x. [para(31(a,1),33(a,1,2))]. 55 CS(x,y,z) | (x v y) ^ (y v z) != y | y ^ (x v z) != y. [para(26(a,1),36(c,1))]. 71 CS(c1,c2,c3) | c2 ^ (c1 v c3) != c2. [para(39(a,1),36(b,1)),rewrite(26(12)),xx(b)]. 78 x v (x v y) = x v y. [para(53(a,1),29(a,1,1)),flip(a)]. 98 x ^ (y v (x v z)) = x. [para(43(a,1),31(a,1,2))]. 99 x v (y v (x ^ z)) = y v x. [para(33(a,1),43(a,1,2)),flip(a)]. 120 x v (y v (z ^ x)) = y v x. [para(48(a,1),43(a,1,2)),flip(a)]. 137 x v (y v (x v z)) = y v (x v z). [para(78(a,1),29(a,2,2)),rewrite(43(3),29(2))]. 481 CS(x,x v y,y v z). [para(47(a,1),55(c,1)),rewrite(78(5),43(7),29(6),137(7),47(7)),xx(b),xx(c)]. 490 CS(x,x v y,z v y). [para(27(a,1),481(a,3))]. 520 CS(x,x v (y ^ z),z). [para(48(a,1),490(a,3))]. 641 CS(c1 ^ c2,c2,c3). [para(38(a,1),520(a,2))]. 648 c2 ^ (c3 v (c1 ^ c2)) = c2. [hyper(35,a,641,a),rewrite(27(5),26(7))]. 801 c3 v (c1 ^ c2) = c2 v c3. [para(648(a,1),48(a,1,2)),rewrite(27(7),120(7),27(3)),flip(a)]. 1821 c1 v (c2 v c3) = c1 v c3. [para(801(a,1),99(a,1,2)),rewrite(27(8))]. 1865 c2 ^ (c1 v c3) = c2. [para(1821(a,1),98(a,1,2))]. 1922 CS(c1,c2,c3). [back_rewrite(71),rewrite(1865(9)),xx(b)]. 1923 $F. [resolve(1922,a,37,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=178. Generated=6708. Kept=1895. proofs=1. Usable=162. Sos=1461. Demods=192. Limbo=57, Disabled=244. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=4813. Back_subsumed=159. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=207 (6 lex), Back_demodulated=53. Back_unit_deleted=0. Demod_attempts=74528. Demod_rewrites=9176. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=64625. Nonunit_bsub_feature_tests=25034. Megabytes=1.52. User_CPU=0.20, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11448 exit (max_proofs) Sat Aug 12 21:01:20 2006