============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11447 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:20 2006 The command was "/home/mccune/bin/prover9 -f head.in bc.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 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))). [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 (F,wt=5): 52 x ^ x = x. [para(33(a,1),31(a,1,2))]. given #14 (T,wt=4): 76 C(x,x,y). [para(52(a,1),36(b,1,1)),rewrite(33(3),27(4),33(4)),xx(b),xx(c)]. given #15 (T,wt=4): 77 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 #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=5): 53 x v x = x. [para(31(a,1),33(a,1,2))]. given #18 (F,wt=6): 90 C(x,x ^ y,y). [para(53(a,1),36(c,1)),rewrite(73(4),26(5),75(5),53(5)),xx(b),xx(c)]. given #19 (T,wt=6): 91 C(x,y ^ x,y). [para(26(a,1),90(a,2))]. given #20 (T,wt=7): 44 x ^ (y v x) = x. [para(27(a,1),31(a,1,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): 48 x v (y ^ x) = x. [para(26(a,1),33(a,1,2))]. given #23 (F,wt=8): 93 C(c1 v c2,c2,c2 v c3). [para(39(a,1),90(a,2))]. given #24 (T,wt=8): 97 C(c2 v c3,c2,c1 v c2). [para(39(a,1),91(a,2))]. given #25 (T,wt=9): 73 x ^ (x ^ y) = x ^ y. [para(52(a,1),28(a,1,1)),flip(a)]. 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): 75 x ^ (y ^ x) = y ^ x. [para(52(a,1),28(a,2,2)),rewrite(26(2))]. given #28 (F,wt=9): 82 x v (y ^ (x ^ z)) = x. [para(41(a,1),33(a,1,2))]. given #29 (T,wt=9): 87 x v (x v y) = x v y. [para(53(a,1),29(a,1,1)),flip(a)]. given #30 (T,wt=9): 89 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): 102 x ^ (y v (z v x)) = x. [para(29(a,1),44(a,1,2))]. given #33 (F,wt=9): 107 x ^ (y v (x v z)) = x. [para(43(a,1),31(a,1,2))]. given #34 (T,wt=9): 112 x v (y ^ (z ^ x)) = x. [para(28(a,1),48(a,1,2))]. given #35 (T,wt=9): 130 c1 ^ (c2 v c3) = c1 ^ c2. [para(39(a,1),45(a,1,2)),flip(a)]. 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=8): 195 C(c1,c1 ^ c2,c2 v c3). [para(130(a,1),90(a,2))]. given #38 (F,wt=8): 196 C(c2 v c3,c1 ^ c2,c1). [para(130(a,1),91(a,2))]. given #39 (T,wt=10): 92 C(x ^ y,x ^ (y ^ z),z). [para(28(a,1),90(a,2))]. given #40 (T,wt=8): 218 C(x ^ y,y ^ x,x). [para(75(a,1),92(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=10): 94 C(x,y ^ (x ^ z),y ^ z). [para(41(a,1),90(a,2))]. given #43 (F,wt=10): 96 C(x,y ^ (z ^ x),y ^ z). [para(28(a,1),91(a,2))]. given #44 (T,wt=8): 261 C(x,y ^ x,x ^ y). [para(75(a,1),96(a,2))]. given #45 (T,wt=10): 98 C(x ^ y,x ^ (z ^ y),z). [para(41(a,1),91(a,2))]. 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): 285 c1 v (c2 ^ c3) = c1 v c2. [para(38(a,1),50(a,1,2)),flip(a)]. given #48 (F,wt=10): 132 C(x,x ^ y,(x v z) ^ y). [para(45(a,1),90(a,2))]. given #49 (T,wt=10): 133 C((x v y) ^ z,x ^ z,x). [para(45(a,1),91(a,2))]. given #50 (T,wt=10): 209 C(x ^ y,y ^ (x ^ z),z). [para(26(a,1),92(a,1))]. 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=10): 210 C(x ^ y,y ^ (z ^ x),z). [para(26(a,1),92(a,2)),rewrite(28(3))]. given #53 (F,wt=8): 353 C(x ^ y,y ^ x,y). [para(73(a,1),210(a,2))]. given #54 (T,wt=10): 237 C(x,x ^ (y ^ z),z ^ y). [para(26(a,1),94(a,2)),rewrite(28(2))]. given #55 (T,wt=8): 376 C(x,x ^ y,y ^ x). [para(73(a,1),237(a,2))]. given #56 (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 #57 (F,wt=10): 238 C(x,y ^ (x ^ z),z ^ y). [para(26(a,1),94(a,3))]. given #58 (F,wt=10): 241 C(x,y ^ x,y ^ (x v z)). [para(31(a,1),94(a,2,2))]. given #59 (T,wt=10): 244 C(x,y ^ x,y ^ (z v x)). [para(44(a,1),94(a,2,2))]. given #60 (T,wt=8): 455 C(c3,c3 ^ (c1 v c2),c2). [para(39(a,1),244(a,3)),rewrite(26(6))]. given #61 (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 #62 (F,wt=8): 463 C(c3,c1 ^ c3,c1 ^ c2). [para(130(a,1),244(a,3))]. given #63 (F,wt=10): 253 C(x,y ^ (z ^ x),z ^ y). [para(26(a,1),96(a,3))]. given #64 (T,wt=10): 269 C(x ^ y,z ^ (y ^ x),z). [para(26(a,1),98(a,2)),rewrite(28(3))]. given #65 (T,wt=10): 272 C(x ^ (y v z),x ^ y,y). [para(31(a,1),98(a,2,2))]. given #66 (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 #67 (F,wt=10): 275 C(x ^ (y v z),x ^ z,z). [para(44(a,1),98(a,2,2))]. given #68 (F,wt=8): 584 C(c2,c3 ^ (c1 v c2),c3). [para(39(a,1),275(a,1)),rewrite(26(6))]. given #69 (T,wt=8): 592 C(c1 ^ c2,c1 ^ c3,c3). [para(130(a,1),275(a,1))]. given #70 (T,wt=10): 295 C(x,y ^ x,(x v z) ^ y). [para(26(a,1),132(a,2))]. given #71 (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 #72 (F,wt=10): 296 C(x,x ^ y,y ^ (x v z)). [para(26(a,1),132(a,3))]. given #73 (F,wt=10): 297 C(x,x ^ y,(z v x) ^ y). [para(27(a,1),132(a,3,1))]. given #74 (T,wt=10): 307 C(x ^ (y v z),y ^ x,y). [para(26(a,1),133(a,1))]. given #75 (T,wt=10): 308 C((x v y) ^ z,z ^ x,x). [para(26(a,1),133(a,2))]. given #76 (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 #77 (F,wt=8): 696 C(x,x ^ y,y ^ z). [para(49(a,1),58(c,1)),rewrite(73(5),41(7),28(6),120(7),49(7)),xx(b),xx(c)]. given #78 (F,wt=8): 698 C(x,y ^ x,y ^ z). [para(26(a,1),696(a,2))]. given #79 (T,wt=8): 699 C(x,x ^ y,z ^ y). [para(26(a,1),696(a,3))]. given #80 (T,wt=8): 708 C(x,y ^ x,z ^ y). [para(26(a,1),698(a,3))]. given #81 (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 #82 (F,wt=8): 710 C(x v y,x,x ^ z). [para(31(a,1),698(a,2))]. given #83 (F,wt=8): 715 C(x v y,y,y ^ z). [para(44(a,1),698(a,2))]. given #84 (T,wt=8): 724 C(x,x ^ (y v z),y). [para(31(a,1),699(a,3))]. given #85 (T,wt=8): 728 C(x,x ^ (y v z),z). [para(44(a,1),699(a,3))]. given #86 (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 #87 (F,wt=6): 835 C(c1 v c2,c2,c3). [para(39(a,1),728(a,2))]. given #88 (F,wt=6): 837 C(c1,c1 ^ c2,c3). [para(130(a,1),728(a,2))]. given #89 (T,wt=8): 739 C(x v y,x,z ^ x). [para(31(a,1),708(a,2))]. given #90 (T,wt=8): 740 C(x,(y v z) ^ x,y). [para(31(a,1),708(a,3))]. given #91 (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 #92 (F,wt=6): 893 C(c2 v c3,c2,c1). [para(39(a,1),740(a,2))]. given #93 (F,wt=8): 744 C(x v y,y,z ^ y). [para(44(a,1),708(a,2))]. given #94 (T,wt=8): 745 C(x,(y v z) ^ x,z). [para(44(a,1),708(a,3))]. given #95 (T,wt=8): 903 C(c1,c1 v c2,c2 v c3). [para(39(a,1),61(b,1,2)),xx(b)]. given #96 (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 #97 (F,wt=6): 952 C(c1,c2,c2 v c3). [para(130(a,1),62(b,1,2)),rewrite(48(11)),xx(b)]. given #98 (F,wt=9): 879 c2 v (c3 ^ (c1 v c2)) = c2. [hyper(35,a,835,a),rewrite(26(5),27(7))]. given #99 (T,wt=6): 956 C(c3,c2,c1 v c2). [para(879(a,1),58(c,1)),rewrite(26(9),44(14),27(11),33(11)),xx(b),xx(c)]. given #100 (T,wt=9): 955 c3 ^ (c1 v c2) = c2 ^ c3. [para(879(a,1),44(a,1,2)),rewrite(26(7),106(7),26(3)),flip(a)]. given #101 (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 #102 (F,wt=6): 997 C(c3,c2 ^ c3,c1). [para(955(a,1),724(a,2))]. given #103 (F,wt=8): 962 C(c3,c2 ^ c3,c1 v c2). [para(955(a,1),90(a,2))]. given #104 (T,wt=8): 963 C(c1 v c2,c2 ^ c3,c3). [para(955(a,1),91(a,2))]. given #105 (T,wt=8): 981 C(c2 ^ c3,c1 ^ c3,c1). [para(955(a,1),272(a,1)),rewrite(26(6))]. 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): 309 C((x v y) ^ z,y ^ z,y). [para(27(a,1),133(a,1,1))]. given #108 (F,wt=10): 321 C(x ^ y,y ^ x,x v z). [para(31(a,1),209(a,2,2))]. given #109 (T,wt=10): 325 C(x ^ y,y ^ x,z v x). [para(44(a,1),209(a,2,2))]. given #110 (T,wt=10): 350 C(x,(y v x) ^ (z ^ x),z). [para(44(a,1),210(a,1))]. given #111 (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 #112 (F,wt=10): 351 C((x v y) ^ z,z ^ y,y). [para(44(a,1),210(a,2,2))]. given #113 (F,wt=10): 356 C(x ^ y,y ^ x,y v z). [para(45(a,1),210(a,2))]. 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): 433 C(x v y,x ^ z,z ^ x). [para(45(a,1),238(a,2))]. given #116 (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 #117 (F,wt=10): 512 C(x v y,z ^ x,x ^ z). [para(31(a,1),253(a,2,2))]. given #118 (F,wt=10): 516 C(x v y,z ^ y,y ^ z). [para(44(a,1),253(a,2,2))]. given #119 (T,wt=10): 582 C(x ^ (y v z),z ^ x,z). [para(26(a,1),275(a,2))]. given #120 (T,wt=10): 702 C(c1 v c2,c2,(c2 v c3) ^ x). [para(39(a,1),696(a,2))]. given #121 (A,wt=13): 69 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(39(a,1),28(a,1,1)),flip(a)]. given #122 (F,wt=10): 705 C(x,x ^ y,z ^ (y ^ u)). [para(41(a,1),696(a,3))]. given #123 (F,wt=10): 706 C(c1,c1 ^ c2,(c2 v c3) ^ x). [para(130(a,1),696(a,2))]. given #124 (T,wt=10): 711 C(c2 v c3,c2,(c1 v c2) ^ x). [para(39(a,1),698(a,2))]. given #125 (T,wt=10): 714 C(x,y ^ x,z ^ (y ^ u)). [para(41(a,1),698(a,3))]. given #126 (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 #127 (F,wt=8): 1287 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 #128 (F,wt=10): 718 C(x v (y v z),z,z ^ u). [para(102(a,1),698(a,2))]. given #129 (T,wt=10): 719 C(x v (y v z),y,y ^ u). [para(107(a,1),698(a,2))]. given #130 (T,wt=10): 720 C(c2 v c3,c1 ^ c2,c1 ^ x). [para(130(a,1),698(a,2))]. given #131 (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 #132 (F,wt=10): 723 C(x,x ^ y,z ^ (u ^ y)). [para(28(a,1),699(a,3))]. given #133 (F,wt=10): 725 C(c1 v c2,c2,x ^ (c2 v c3)). [para(39(a,1),699(a,2))]. given #134 (T,wt=10): 731 C(x,x ^ (y v (z v u)),u). [para(102(a,1),699(a,3))]. given #135 (T,wt=10): 732 C(x,x ^ (y v (z v u)),z). [para(107(a,1),699(a,3))]. given #136 (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 #137 (F,wt=10): 733 C(c1,c1 ^ c2,x ^ (c2 v c3)). [para(130(a,1),699(a,2))]. given #138 (F,wt=10): 738 C(x,y ^ x,z ^ (u ^ y)). [para(28(a,1),708(a,3))]. given #139 (T,wt=10): 741 C(c2 v c3,c2,x ^ (c1 v c2)). [para(39(a,1),708(a,2))]. given #140 (T,wt=10): 750 C(x v (y v z),z,u ^ z). [para(102(a,1),708(a,2))]. given #141 (A,wt=11): 79 C(c1,c2 ^ c3,c2) | c2 ^ c3 != c2. [back_rewrite(68),rewrite(73(16),27(15),48(15)),xx(b)]. given #142 (F,wt=10): 751 C(x,(y v (z v u)) ^ x,u). [para(102(a,1),708(a,3))]. given #143 (F,wt=10): 752 C(x v (y v z),y,u ^ y). [para(107(a,1),708(a,2))]. given #144 (T,wt=10): 753 C(x,(y v (z v u)) ^ x,z). [para(107(a,1),708(a,3))]. given #145 (T,wt=10): 754 C(c2 v c3,c1 ^ c2,x ^ c1). [para(130(a,1),708(a,2))]. given #146 (A,wt=17): 80 C(x,x ^ (y ^ z),y) | x ^ (y ^ z) != x ^ y. [back_rewrite(64),rewrite(73(6),48(9)),xx(b)]. given #147 (F,wt=10): 820 C(x v y,x,z ^ (x ^ u)). [para(41(a,1),710(a,3))]. given #148 (F,wt=10): 823 C(x v y,y,z ^ (y ^ u)). [para(41(a,1),715(a,3))]. given #149 (T,wt=10): 882 C(x v y,x,z ^ (u ^ x)). [para(28(a,1),739(a,3))]. given #150 (T,wt=10): 883 C(x v (y v z),x v y,x). [para(31(a,1),739(a,3)),rewrite(29(2))]. given #151 (A,wt=11): 81 x ^ (y ^ (x v z)) = y ^ x. [para(31(a,1),41(a,1,2)),flip(a)]. given #152 (F,wt=8): 1524 C(x v y,y v x,y). [para(89(a,1),883(a,1))]. given #153 (F,wt=9): 1574 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(955(a,1),81(a,1,2)),rewrite(26(8))]. ============================== PROOF ================================= % Proof 1 at 0.16 (+ 0.00) seconds. % Length of proof is 39. % Level of proof is 14. % Maximum clause weight is 20. % Given clauses 153. 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))). [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 ^ (x ^ y) = x ^ y. [para(52(a,1),28(a,1,1)),flip(a)]. 81 x ^ (y ^ (x v z)) = y ^ x. [para(31(a,1),41(a,1,2)),flip(a)]. 82 x v (y ^ (x ^ z)) = x. [para(41(a,1),33(a,1,2))]. 106 x ^ (y ^ (z v x)) = y ^ x. [para(44(a,1),41(a,1,2)),flip(a)]. 120 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(73(a,1),28(a,2,2)),rewrite(41(3),28(2))]. 696 C(x,x ^ y,y ^ z). [para(49(a,1),58(c,1)),rewrite(73(5),41(7),28(6),120(7),49(7)),xx(b),xx(c)]. 699 C(x,x ^ y,z ^ y). [para(26(a,1),696(a,3))]. 728 C(x,x ^ (y v z),z). [para(44(a,1),699(a,3))]. 835 C(c1 v c2,c2,c3). [para(39(a,1),728(a,2))]. 879 c2 v (c3 ^ (c1 v c2)) = c2. [hyper(35,a,835,a),rewrite(26(5),27(7))]. 955 c3 ^ (c1 v c2) = c2 ^ c3. [para(879(a,1),44(a,1,2)),rewrite(26(7),106(7),26(3)),flip(a)]. 1574 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(955(a,1),81(a,1,2)),rewrite(26(8))]. 1604 c2 v (c1 ^ c3) = c2. [para(1574(a,1),82(a,1,2))]. 1659 C(c1,c2,c3). [back_rewrite(67),rewrite(1604(9)),xx(b)]. 1660 $F. [resolve(1659,a,37,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=153. Generated=5538. Kept=1632. proofs=1. Usable=138. Sos=1263. Demods=164. Limbo=55, Disabled=205. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=3906. Back_subsumed=135. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=177 (6 lex), Back_demodulated=38. Back_unit_deleted=0. Demod_attempts=57437. Demod_rewrites=7073. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=47083. Nonunit_bsub_feature_tests=18395. Megabytes=1.31. User_CPU=0.16, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11447 exit (max_proofs) Sat Aug 12 21:01:20 2006