============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27051 was started by mccune on cleo, Fri Apr 13 09:19:46 2007 The command was "/home/mccune/bin/prover9 -f head.in bc.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 bc.in formulas(goals). (all a all x all b (B(a,x,b) -> C(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) -> C(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)]. B(c1,c2,c3). [deny(7)]. -C(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 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)]. 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([ C, =, D, CS, 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 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 35 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. 36 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 37 -C(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 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. given #8 (I,wt=11): 35 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. given #9 (I,wt=20): 36 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. given #10 (I,wt=4): 37 -C(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 (A,wt=11): 41 x ^ (y ^ z) = y ^ (x ^ z). [para(26(a,1),28(a,1,1)),rewrite(28(2))]. given #14 (T,wt=5): 52 x ^ x = x. [para(33(a,1),31(a,1,2))]. given #15 (T,wt=4): 82 C(x,x,y). [para(52(a,1),36(b,1,1)),rewrite(33(3),27(4),33(4)),xx(b),xx(c)]. given #16 (T,wt=4): 83 C(x,y,y). [para(52(a,1),36(b,1,2)),rewrite(27(3),48(3),27(4),48(4)),xx(b),xx(c)]. given #17 (T,wt=5): 53 x v x = x. [para(31(a,1),33(a,1,2))]. given #18 (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 #19 (T,wt=6): 90 C(x,x ^ y,y). [para(53(a,1),36(c,1)),rewrite(79(4),26(5),81(5),53(5)),xx(b),xx(c)]. given #20 (T,wt=6): 95 C(x,y ^ x,y). [para(26(a,1),90(a,2))]. given #21 (T,wt=7): 44 x ^ (y v x) = x. [para(27(a,1),31(a,1,2))]. given #22 (T,wt=7): 48 x v (y ^ x) = x. [para(26(a,1),33(a,1,2))]. given #23 (A,wt=11): 45 x ^ ((x v y) ^ z) = x ^ z. [para(31(a,1),28(a,1,1)),flip(a)]. given #24 (T,wt=8): 97 C(c1 v c2,c2,c2 v c3). [para(39(a,1),90(a,2))]. given #25 (T,wt=8): 101 C(c2 v c3,c2,c1 v c2). [para(39(a,1),95(a,2))]. given #26 (T,wt=9): 74 x v (y ^ (x ^ z)) = x. [para(41(a,1),33(a,1,2))]. given #27 (T,wt=9): 79 x ^ (x ^ y) = x ^ y. [para(52(a,1),28(a,1,1)),flip(a)]. given #28 (A,wt=13): 46 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(31(a,1),28(a,1)),flip(a)]. given #29 (T,wt=9): 81 x ^ (y ^ x) = y ^ x. [para(52(a,1),28(a,2,2)),rewrite(26(2))]. given #30 (T,wt=9): 87 x v (x v y) = x v y. [para(53(a,1),29(a,1,1)),flip(a)]. given #31 (T,wt=9): 89 x v (y v x) = y v x. [para(53(a,1),29(a,2,2)),rewrite(27(2))]. given #32 (T,wt=9): 91 x ^ (y v (x v z)) = x. [para(43(a,1),31(a,1,2))]. given #33 (A,wt=13): 47 (x v y) ^ (x v (y v z)) = x v y. [para(29(a,1),31(a,1,2))]. given #34 (T,wt=9): 106 x ^ (y v (z v x)) = x. [para(29(a,1),44(a,1,2))]. given #35 (T,wt=9): 112 x v (y ^ (z ^ x)) = x. [para(28(a,1),48(a,1,2))]. given #36 (T,wt=9): 124 c1 ^ (c2 v c3) = c1 ^ c2. [para(39(a,1),45(a,1,2)),flip(a)]. given #37 (T,wt=8): 207 C(c1,c1 ^ c2,c2 v c3). [para(124(a,1),90(a,2))]. given #38 (A,wt=13): 49 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(28(a,1),33(a,1,2))]. given #39 (T,wt=8): 208 C(c2 v c3,c1 ^ c2,c1). [para(124(a,1),95(a,2))]. given #40 (T,wt=10): 96 C(x ^ y,x ^ (y ^ z),z). [para(28(a,1),90(a,2))]. given #41 (T,wt=8): 230 C(x ^ y,y ^ x,x). [para(81(a,1),96(a,2))]. given #42 (T,wt=10): 98 C(x,y ^ (x ^ z),y ^ z). [para(41(a,1),90(a,2))]. given #43 (A,wt=11): 50 x v ((x ^ y) v z) = x v z. [para(33(a,1),29(a,1,1)),flip(a)]. given #44 (T,wt=9): 254 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),50(a,1,2)),flip(a)]. given #45 (T,wt=10): 100 C(x,y ^ (z ^ x),y ^ z). [para(28(a,1),95(a,2))]. given #46 (T,wt=8): 274 C(x,y ^ x,x ^ y). [para(81(a,1),100(a,2))]. given #47 (T,wt=10): 102 C(x ^ y,x ^ (z ^ y),z). [para(41(a,1),95(a,2))]. given #48 (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 #49 (T,wt=10): 127 C(x,x ^ y,(x v z) ^ y). [para(45(a,1),90(a,2))]. given #50 (T,wt=10): 128 C((x v y) ^ z,x ^ z,x). [para(45(a,1),95(a,2))]. given #51 (T,wt=10): 220 C(x ^ y,y ^ (x ^ z),z). [para(26(a,1),96(a,1))]. given #52 (T,wt=10): 221 C(x ^ y,y ^ (z ^ x),z). [para(26(a,1),96(a,2)),rewrite(28(3))]. given #53 (A,wt=20): 54 C(x,y,z) | (y ^ x) v (y ^ z) != y | (x ^ z) v y != y. [para(26(a,1),36(b,1,1))]. given #54 (T,wt=8): 356 C(x ^ y,y ^ x,y). [para(79(a,1),221(a,2))]. given #55 (T,wt=10): 237 C(x,x ^ (y ^ z),z ^ y). [para(26(a,1),98(a,2)),rewrite(28(2))]. given #56 (T,wt=8): 416 C(x,x ^ y,y ^ x). [para(79(a,1),237(a,2))]. given #57 (T,wt=10): 238 C(x,y ^ (x ^ z),z ^ y). [para(26(a,1),98(a,3))]. given #58 (A,wt=20): 55 C(x,y,z) | (x ^ y) v (z ^ y) != y | (x ^ z) v y != y. [para(26(a,1),36(b,1,2))]. given #59 (T,wt=10): 241 C(x,y ^ x,y ^ (x v z)). [para(31(a,1),98(a,2,2))]. given #60 (T,wt=10): 244 C(x,y ^ x,y ^ (z v x)). [para(44(a,1),98(a,2,2))]. given #61 (T,wt=8): 495 C(c3,c3 ^ (c1 v c2),c2). [para(39(a,1),244(a,3)),rewrite(26(6))]. given #62 (T,wt=8): 503 C(c3,c1 ^ c3,c1 ^ c2). [para(124(a,1),244(a,3))]. given #63 (A,wt=20): 56 C(x,y,z) | (x ^ y) v (y ^ z) != y | (z ^ x) v y != y. [para(26(a,1),36(c,1,1))]. given #64 (T,wt=10): 265 C(x,y ^ (z ^ x),z ^ y). [para(26(a,1),100(a,3))]. given #65 (T,wt=10): 281 C(x ^ y,z ^ (y ^ x),z). [para(26(a,1),102(a,2)),rewrite(28(3))]. given #66 (T,wt=10): 284 C(x ^ (y v z),x ^ y,y). [para(31(a,1),102(a,2,2))]. given #67 (T,wt=10): 287 C(x ^ (y v z),x ^ z,z). [para(44(a,1),102(a,2,2))]. given #68 (A,wt=20): 57 C(x,y,z) | (y ^ z) v (x ^ y) != y | (x ^ z) v y != y. [para(27(a,1),36(b,1))]. given #69 (T,wt=8): 584 C(c2,c3 ^ (c1 v c2),c3). [para(39(a,1),287(a,1)),rewrite(26(6))]. given #70 (T,wt=8): 592 C(c1 ^ c2,c1 ^ c3,c3). [para(124(a,1),287(a,1))]. given #71 (T,wt=10): 303 C(x,y ^ x,(x v z) ^ y). [para(26(a,1),127(a,2))]. given #72 (T,wt=10): 304 C(x,x ^ y,y ^ (x v z)). [para(26(a,1),127(a,3))]. given #73 (A,wt=20): 58 C(x,y,z) | (x ^ y) v (y ^ z) != y | y v (x ^ z) != y. [para(27(a,1),36(c,1))]. given #74 (T,wt=8): 665 C(x,x ^ y,y ^ z). [para(49(a,1),58(c,1)),rewrite(79(5),41(7),28(6),137(7),49(7)),xx(b),xx(c)]. given #75 (T,wt=8): 667 C(x,y ^ x,y ^ z). [para(26(a,1),665(a,2))]. given #76 (T,wt=8): 668 C(x,x ^ y,z ^ y). [para(26(a,1),665(a,3))]. given #77 (T,wt=8): 677 C(x,y ^ x,z ^ y). [para(26(a,1),667(a,3))]. given #78 (A,wt=26): 59 C(x ^ y,z,u) | (x ^ (y ^ z)) v (z ^ u) != z | (x ^ (y ^ u)) v z != z. [para(28(a,1),36(b,1,1)),rewrite(28(9))]. given #79 (T,wt=8): 679 C(x v y,x,x ^ z). [para(31(a,1),667(a,2))]. given #80 (T,wt=8): 684 C(x v y,y,y ^ z). [para(44(a,1),667(a,2))]. given #81 (T,wt=8): 693 C(x,x ^ (y v z),y). [para(31(a,1),668(a,3))]. given #82 (T,wt=8): 697 C(x,x ^ (y v z),z). [para(44(a,1),668(a,3))]. given #83 (A,wt=32): 60 C(x,y ^ z,u) | (x ^ (y ^ z)) v (y ^ (z ^ u)) != y ^ z | (x ^ u) v (y ^ z) != y ^ z. [para(28(a,1),36(b,1,2))]. given #84 (T,wt=6): 804 C(c1 v c2,c2,c3). [para(39(a,1),697(a,2))]. given #85 (T,wt=6): 806 C(c1,c1 ^ c2,c3). [para(124(a,1),697(a,2))]. given #86 (T,wt=8): 708 C(x v y,x,z ^ x). [para(31(a,1),677(a,2))]. given #87 (T,wt=8): 709 C(x,(y v z) ^ x,y). [para(31(a,1),677(a,3))]. given #88 (A,wt=17): 61 C(x,x v y,z) | x v ((x v y) ^ z) != x v y. [para(31(a,1),36(b,1,1)),rewrite(43(10),50(10)),xx(c)]. given #89 (T,wt=6): 862 C(c2 v c3,c2,c1). [para(39(a,1),709(a,2))]. given #90 (T,wt=8): 713 C(x v y,y,z ^ y). [para(44(a,1),677(a,2))]. given #91 (T,wt=8): 714 C(x,(y v z) ^ x,z). [para(44(a,1),677(a,3))]. given #92 (T,wt=8): 872 C(c1,c1 v c2,c2 v c3). [para(39(a,1),61(b,1,2)),xx(b)]. given #93 (A,wt=15): 62 C(x,y,y v z) | y v (x ^ (y v z)) != y. [para(31(a,1),36(b,1,2)),rewrite(27(4),48(4),27(6)),xx(b)]. given #94 (T,wt=6): 922 C(c1,c2,c2 v c3). [para(124(a,1),62(b,1,2)),rewrite(48(11)),xx(b)]. given #95 (T,wt=9): 848 c2 v (c3 ^ (c1 v c2)) = c2. [hyper(35,a,804,a),rewrite(26(5),27(7))]. given #96 (T,wt=6): 926 C(c3,c2,c1 v c2). [para(848(a,1),58(c,1)),rewrite(26(9),44(14),27(11),33(11)),xx(b),xx(c)]. given #97 (T,wt=9): 925 c3 ^ (c1 v c2) = c2 ^ c3. [para(848(a,1),44(a,1,2)),rewrite(26(7),110(7),26(3)),flip(a)]. given #98 (A,wt=22): 63 C(x,y,x v z) | (x ^ y) v (y ^ (x v z)) != y | x v y != y. [para(31(a,1),36(c,1,1))]. given #99 (T,wt=6): 967 C(c3,c2 ^ c3,c1). [para(925(a,1),693(a,2))]. given #100 (T,wt=8): 932 C(c3,c2 ^ c3,c1 v c2). [para(925(a,1),90(a,2))]. given #101 (T,wt=8): 933 C(c1 v c2,c2 ^ c3,c3). [para(925(a,1),95(a,2))]. given #102 (T,wt=8): 954 C(c2 ^ c3,c1 ^ c3,c1). [para(925(a,1),284(a,1)),rewrite(26(6))]. given #103 (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 #104 (T,wt=10): 315 C(x ^ (y v z),y ^ x,y). [para(26(a,1),128(a,1))]. given #105 (T,wt=10): 316 C((x v y) ^ z,z ^ x,x). [para(26(a,1),128(a,2))]. given #106 (T,wt=10): 317 C((x v y) ^ z,y ^ z,y). [para(27(a,1),128(a,1,1))]. given #107 (T,wt=10): 329 C(x ^ y,y ^ x,x v z). [para(31(a,1),220(a,2,2))]. given #108 (A,wt=13): 66 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(38(a,1),29(a,2,2)),rewrite(27(8))]. given #109 (T,wt=10): 333 C(x ^ y,y ^ x,z v x). [para(44(a,1),220(a,2,2))]. given #110 (T,wt=10): 350 C(x,(y v x) ^ (z ^ x),z). [para(44(a,1),221(a,1))]. given #111 (T,wt=10): 351 C((x v y) ^ z,z ^ y,y). [para(44(a,1),221(a,2,2))]. given #112 (T,wt=10): 354 C(x ^ y,y ^ x,y v z). [para(45(a,1),221(a,2))]. given #113 (A,wt=11): 67 C(c1,c2,c3) | c2 v (c1 ^ c3) != c2. [para(38(a,1),36(b,1)),rewrite(27(12)),xx(b)]. given #114 (T,wt=10): 430 C(x,(y v z) ^ (x ^ z),z). [para(44(a,1),238(a,3))]. given #115 (T,wt=10): 432 C(x v y,x ^ z,z ^ x). [para(45(a,1),238(a,2))]. given #116 (T,wt=10): 558 C(x v y,z ^ x,x ^ z). [para(31(a,1),265(a,2,2))]. given #117 (T,wt=10): 562 C(x v y,z ^ y,y ^ z). [para(44(a,1),265(a,2,2))]. given #118 (A,wt=13): 69 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(39(a,1),28(a,1,1)),flip(a)]. given #119 (T,wt=10): 582 C(x ^ (y v z),z ^ x,z). [para(26(a,1),287(a,2))]. given #120 (T,wt=10): 671 C(c1 v c2,c2,(c2 v c3) ^ x). [para(39(a,1),665(a,2))]. given #121 (T,wt=10): 674 C(x,x ^ y,z ^ (y ^ u)). [para(41(a,1),665(a,3))]. given #122 (T,wt=10): 675 C(c1,c1 ^ c2,(c2 v c3) ^ x). [para(124(a,1),665(a,2))]. given #123 (A,wt=32): 70 C(c1 v c2,c2 v c3,x) | c2 v ((c2 v c3) ^ x) != c2 v c3 | c2 v (c3 v ((c1 v c2) ^ x)) != c2 v c3. [para(39(a,1),36(b,1,1)),rewrite(43(25),27(24))]. given #124 (T,wt=8): 1253 C(c1 v c2,c2 v c3,c3). [para(48(a,1),70(c,1,2)),rewrite(26(14),44(14)),xx(b),xx(c)]. given #125 (T,wt=10): 680 C(c2 v c3,c2,(c1 v c2) ^ x). [para(39(a,1),667(a,2))]. given #126 (T,wt=10): 683 C(x,y ^ x,z ^ (y ^ u)). [para(41(a,1),667(a,3))]. given #127 (T,wt=10): 687 C(x v (y v z),y,y ^ u). [para(91(a,1),667(a,2))]. given #128 (A,wt=32): 71 C(x,c1 v c2,c2 v c3) | c2 v (x ^ (c1 v c2)) != c1 v c2 | c1 v (c2 v (x ^ (c2 v c3))) != c1 v c2. [para(39(a,1),36(b,1,2)),rewrite(27(13),27(25),29(25))]. given #129 (T,wt=10): 689 C(x v (y v z),z,z ^ u). [para(106(a,1),667(a,2))]. given #130 (T,wt=10): 690 C(c2 v c3,c1 ^ c2,c1 ^ x). [para(124(a,1),667(a,2))]. given #131 (T,wt=10): 692 C(x,x ^ y,z ^ (u ^ y)). [para(28(a,1),668(a,3))]. given #132 (T,wt=10): 694 C(c1 v c2,c2,x ^ (c2 v c3)). [para(39(a,1),668(a,2))]. given #133 (A,wt=26): 72 C(c1 v c2,x,c2 v c3) | ((c1 v c2) ^ x) v (x ^ (c2 v c3)) != x | c2 v x != x. [para(39(a,1),36(c,1,1))]. given #134 (T,wt=10): 700 C(x,x ^ (y v (z v u)),z). [para(91(a,1),668(a,3))]. given #135 (T,wt=10): 702 C(x,x ^ (y v (z v u)),u). [para(106(a,1),668(a,3))]. given #136 (T,wt=10): 703 C(c1,c1 ^ c2,x ^ (c2 v c3)). [para(124(a,1),668(a,2))]. given #137 (T,wt=10): 707 C(x,y ^ x,z ^ (u ^ y)). [para(28(a,1),677(a,3))]. given #138 (A,wt=11): 73 x ^ (y ^ (x v z)) = y ^ x. [para(31(a,1),41(a,1,2)),flip(a)]. given #139 (T,wt=9): 1429 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(925(a,1),73(a,1,2)),rewrite(26(8))]. ============================== PROOF ================================= % Proof 1 at 0.13 (+ 0.00) seconds. % Length of proof is 39. % Level of proof is 13. % Maximum clause weight is 20. % Given clauses 139. 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]. 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]. 7 (all a all x all b (B(a,x,b) -> C(a,x,b))) # label(goal). [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]. 28 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [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 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. 36 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 37 -C(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)]. 41 x ^ (y ^ z) = y ^ (x ^ z). [para(26(a,1),28(a,1,1)),rewrite(28(2))]. 44 x ^ (y v x) = x. [para(27(a,1),31(a,1,2))]. 49 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(28(a,1),33(a,1,2))]. 52 x ^ x = x. [para(33(a,1),31(a,1,2))]. 58 C(x,y,z) | (x ^ y) v (y ^ z) != y | y v (x ^ z) != y. [para(27(a,1),36(c,1))]. 67 C(c1,c2,c3) | c2 v (c1 ^ c3) != c2. [para(38(a,1),36(b,1)),rewrite(27(12)),xx(b)]. 73 x ^ (y ^ (x v z)) = y ^ x. [para(31(a,1),41(a,1,2)),flip(a)]. 74 x v (y ^ (x ^ z)) = x. [para(41(a,1),33(a,1,2))]. 79 x ^ (x ^ y) = x ^ y. [para(52(a,1),28(a,1,1)),flip(a)]. 110 x ^ (y ^ (z v x)) = y ^ x. [para(44(a,1),41(a,1,2)),flip(a)]. 137 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(74(a,1),44(a,1,2)),rewrite(26(3))]. 665 C(x,x ^ y,y ^ z). [para(49(a,1),58(c,1)),rewrite(79(5),41(7),28(6),137(7),49(7)),xx(b),xx(c)]. 668 C(x,x ^ y,z ^ y). [para(26(a,1),665(a,3))]. 697 C(x,x ^ (y v z),z). [para(44(a,1),668(a,3))]. 804 C(c1 v c2,c2,c3). [para(39(a,1),697(a,2))]. 848 c2 v (c3 ^ (c1 v c2)) = c2. [hyper(35,a,804,a),rewrite(26(5),27(7))]. 925 c3 ^ (c1 v c2) = c2 ^ c3. [para(848(a,1),44(a,1,2)),rewrite(26(7),110(7),26(3)),flip(a)]. 1429 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(925(a,1),73(a,1,2)),rewrite(26(8))]. 1450 c2 v (c1 ^ c3) = c2. [para(1429(a,1),74(a,1,2))]. 1498 C(c1,c2,c3). [back_rewrite(67),rewrite(1450(9)),xx(b)]. 1499 $F. [resolve(1498,a,37,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=139. Generated=5008. Kept=1471. proofs=1. Usable=125. Sos=1151. Demods=158. Limbo=48, Disabled=176. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=3537. Back_subsumed=108. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=171 (6 lex), Back_demodulated=36. Back_unit_deleted=0. Demod_attempts=53350. Demod_rewrites=6717. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46017. Nonunit_bsub_feature_tests=16131. Megabytes=1.28. User_CPU=0.14, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 27051 exit (max_proofs) Fri Apr 13 09:19:46 2007