============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11451 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:21 2006 The command was "/home/mccune/bin/prover9 -f head.in t2_12.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 t2_12.in formulas(sos). x <= y | y <= x. D(ca,cx,cb). -A(ca,cx,cb). 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]. ============================== 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)]. x <= y | y <= x. [assumption]. D(ca,cx,cb). [assumption]. -A(ca,cx,cb). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating B/3 7 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y. [clausify(2)]. 8 -B(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(2)]. 9 -B(x,y,z) | (x v y) ^ (y v z) = y. [clausify(2)]. Eliminating C/3 10 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y. [clausify(3)]. 11 -C(x,y,z) | (x ^ y) v (y ^ z) = y. [clausify(3)]. 12 -C(x,y,z) | (x ^ z) v y = y. [clausify(3)]. Eliminating CS/3 13 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y. [clausify(4)]. 14 -CS(x,y,z) | (x v y) ^ (y v z) = y. [clausify(4)]. 15 -CS(x,y,z) | (x v z) ^ y = y. [clausify(4)]. Eliminating D/3 16 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z). [clausify(5)]. 17 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 18 -D(x,y,z) | y <= x v z. [clausify(5)]. 19 D(ca,cx,cb). [assumption]. Derived: ca ^ cb <= cx. [resolve(19,a,17,a)]. Derived: cx <= ca v cb. [resolve(19,a,18,a)]. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ <=, A, =, D, CS, C, B ]). Function symbol precedence: lex([ ca, cb, cx, ^, 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). 20 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 21 x v y = y v x # label("commutativity_join"). [assumption]. 22 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 23 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 25 x ^ (x v y) = x. [copy(24),rewrite(20(2))]. 27 x v (x ^ y) = x. [copy(26),rewrite(21(2))]. 28 -A(x,y,z) | x <= y | z <= y. [clausify(1)]. 31 -A(x,y,z) | y <= z | y <= x. [clausify(1)]. 32 A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. 33 A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. 34 -(x <= y) | x ^ y = x. [clausify(6)]. 35 x <= y | x ^ y != x. [clausify(6)]. 36 x <= y | y <= x. [assumption]. 37 -A(ca,cx,cb). [assumption]. 38 ca ^ cb <= cx. [resolve(19,a,17,a)]. 39 cx <= ca v cb. [resolve(19,a,18,a)]. 40 -A(x,y,x) | x <= y. [factor(28,b,c)]. 43 -A(x,y,x) | y <= x. [factor(31,b,c)]. 45 x <= x. [factor(36,a,b)]. 46 A(x,x,x). [back_unit_del(44),unit_del(b,45)]. end_of_list. formulas(demodulators). 20 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 21 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 22 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 23 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 25 x ^ (x v y) = x. [copy(24),rewrite(20(2))]. 27 x v (x ^ y) = x. [copy(26),rewrite(21(2))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 20 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. given #2 (I,wt=7): 21 x v y = y v x # label("commutativity_join"). [assumption]. given #3 (I,wt=11): 22 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 47 x ^ (y ^ z) = z ^ (x ^ y). [para(22(a,1),20(a,1))]. given #4 (I,wt=11): 23 (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: 49 x v (y v z) = z v (x v y). [para(23(a,1),21(a,1))]. given #5 (I,wt=7): 25 x ^ (x v y) = x. [copy(24),rewrite(20(2))]. given #6 (I,wt=7): 27 x v (x ^ y) = x. [copy(26),rewrite(21(2))]. given #7 (I,wt=10): 28 -A(x,y,z) | x <= y | z <= y. [clausify(1)]. given #8 (I,wt=10): 31 -A(x,y,z) | y <= z | y <= x. [clausify(1)]. given #9 (I,wt=10): 32 A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. given #10 (I,wt=10): 33 A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. given #11 (I,wt=8): 34 -(x <= y) | x ^ y = x. [clausify(6)]. given #12 (I,wt=8): 35 x <= y | x ^ y != x. [clausify(6)]. given #13 (I,wt=6): 36 x <= y | y <= x. [assumption]. given #14 (I,wt=4): 37 -A(ca,cx,cb). [assumption]. given #15 (I,wt=5): 38 ca ^ cb <= cx. [resolve(19,a,17,a)]. given #16 (I,wt=5): 39 cx <= ca v cb. [resolve(19,a,18,a)]. given #17 (I,wt=7): 40 -A(x,y,x) | x <= y. [factor(28,b,c)]. given #18 (I,wt=7): 43 -A(x,y,x) | y <= x. [factor(31,b,c)]. given #19 (I,wt=3): 45 x <= x. [factor(36,a,b)]. given #20 (I,wt=4): 46 A(x,x,x). [back_unit_del(44),unit_del(b,45)]. given #21 (A,wt=11): 48 x ^ (y ^ z) = y ^ (x ^ z). [para(20(a,1),22(a,1,1)),rewrite(22(2))]. given #22 (F,wt=5): 59 x ^ x = x. [para(27(a,1),25(a,1,2))]. given #23 (F,wt=5): 60 x v x = x. [para(25(a,1),27(a,1,2))]. given #24 (T,wt=5): 61 x <= x v y. [hyper(35,b,25,a)]. given #25 (T,wt=5): 114 x <= y v x. [para(21(a,1),61(a,2))]. given #26 (A,wt=11): 50 x v (y v z) = y v (x v z). [para(21(a,1),23(a,1,1)),rewrite(23(2))]. given #27 (F,wt=5): 135 x ^ y <= x. [para(27(a,1),114(a,2))]. given #28 (F,wt=5): 158 x ^ y <= y. [para(20(a,1),135(a,1))]. given #29 (T,wt=6): 80 A(cx,cx,ca ^ cb). [hyper(33,b,38,a,c,45,a)]. given #30 (T,wt=6): 82 A(ca v cb,cx,cx). [hyper(33,b,45,a,c,39,a)]. given #31 (A,wt=7): 51 x ^ (y v x) = x. [para(21(a,1),25(a,1,2))]. given #32 (F,wt=6): 86 A(ca ^ cb,cx,cx). [hyper(32,b,38,a,c,45,a)]. given #33 (F,wt=6): 88 A(cx,cx,ca v cb). [hyper(32,b,45,a,c,39,a)]. given #34 (T,wt=6): 101 A(x v y,x,x). [hyper(33,b,45,a,c,61,a)]. given #35 (T,wt=6): 108 A(x,x,x v y). [hyper(32,b,45,a,c,61,a)]. given #36 (A,wt=11): 52 x ^ ((x v y) ^ z) = x ^ z. [para(25(a,1),22(a,1,1)),flip(a)]. given #37 (F,wt=6): 118 A(x v y,y,y). [hyper(33,b,45,a,c,114,a)]. given #38 (F,wt=6): 127 A(x,x,y v x). [hyper(32,b,45,a,c,114,a)]. given #39 (T,wt=6): 145 A(x,x,x ^ y). [hyper(33,b,135,a,c,45,a)]. given #40 (T,wt=6): 154 A(x ^ y,x,x). [hyper(32,b,135,a,c,45,a)]. given #41 (A,wt=13): 53 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(25(a,1),22(a,1)),flip(a)]. given #42 (F,wt=6): 168 A(x,x,y ^ x). [hyper(33,b,158,a,c,45,a)]. given #43 (F,wt=6): 179 A(x ^ y,y,y). [hyper(32,b,158,a,c,45,a)]. given #44 (T,wt=7): 55 x v (y ^ x) = x. [para(20(a,1),27(a,1,2))]. given #45 (T,wt=7): 72 cx ^ (ca v cb) = cx. [hyper(34,a,39,a)]. given #46 (A,wt=13): 54 (x v y) ^ (x v (y v z)) = x v y. [para(23(a,1),25(a,1,2))]. given #47 (F,wt=7): 81 A(x,x,y) | x <= y. [hyper(33,b,36,b,c,45,a)]. given #48 (F,wt=7): 84 A(x,y,y) | x <= y. [hyper(33,b,45,a,c,36,b)]. given #49 (T,wt=7): 87 A(x,y,y) | y <= x. [hyper(32,b,36,b,c,45,a)]. given #50 (T,wt=7): 90 A(x,x,y) | y <= x. [hyper(32,b,45,a,c,36,b)]. given #51 (A,wt=13): 56 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(22(a,1),27(a,1,2))]. given #52 (F,wt=7): 134 x <= y v (z v x). [para(23(a,1),114(a,2))]. given #53 (F,wt=7): 138 x <= y v (x v z). [para(50(a,1),61(a,2))]. given #54 (T,wt=7): 160 x ^ (y ^ z) <= y. [para(48(a,1),135(a,1))]. given #55 (T,wt=7): 183 x ^ (y ^ z) <= z. [para(22(a,1),158(a,1))]. given #56 (A,wt=11): 57 x v ((x ^ y) v z) = x v z. [para(27(a,1),23(a,1,1)),flip(a)]. given #57 (F,wt=7): 278 x ^ y <= z v x. [para(27(a,1),134(a,2,2))]. given #58 (F,wt=7): 280 x ^ y <= z v y. [para(55(a,1),134(a,2,2))]. given #59 (T,wt=7): 343 x ^ y <= x v z. [para(52(a,1),160(a,1))]. given #60 (T,wt=7): 378 x ^ y <= y v z. [para(25(a,1),183(a,1,2))]. given #61 (A,wt=13): 58 x v (y v ((x v y) ^ z)) = x v y. [para(27(a,1),23(a,1)),flip(a)]. given #62 (F,wt=7): 382 x ^ cx <= ca v cb. [para(72(a,1),183(a,1,2))]. given #63 (F,wt=7): 450 cx <= x v (ca v cb). [para(72(a,1),280(a,1))]. given #64 (T,wt=7): 509 cx <= ca v (cb v x). [para(72(a,1),378(a,1)),rewrite(23(5))]. given #65 (T,wt=7): 547 cx ^ x <= ca v cb. [para(20(a,1),382(a,1))]. given #66 (A,wt=8): 62 x <= y | y ^ x != x. [para(20(a,1),35(b,1))]. given #67 (F,wt=7): 577 cx <= ca v (x v cb). [para(50(a,1),450(a,2))]. given #68 (F,wt=8): 64 x ^ y = x | y <= x. [hyper(34,a,36,a)]. given #69 (T,wt=6): 671 cb <= ca | ca <= cx. [para(64(a,1),38(a,1))]. given #70 (T,wt=6): 686 x <= y | y != x. [para(64(a,1),62(b,1)),merge(b)]. given #71 (A,wt=14): 63 x ^ y <= z | x ^ (y ^ z) != x ^ y. [para(22(a,1),35(b,1))]. given #72 (F,wt=7): 674 cb <= ca | A(cx,cx,ca). [para(64(a,1),80(a,3))]. given #73 (F,wt=7): 675 cb <= ca | A(ca,cx,cx). [para(64(a,1),86(a,1))]. given #74 (T,wt=7): 692 A(ca,cb,cb) | ca <= cx. [hyper(33,b,45,a,c,671,a)]. given #75 (T,wt=7): 698 A(ca,ca,cb) | ca <= cx. [hyper(33,b,671,a,c,45,a)]. given #76 (A,wt=10): 65 A(x,y,z) | y <= z | x <= y. [hyper(33,b,36,b,c,36,a)]. given #77 (F,wt=6): 727 cx <= cb | ca <= cx. [hyper(37,a,65,a)]. given #78 (F,wt=7): 704 A(cb,cb,ca) | ca <= cx. [hyper(32,b,45,a,c,671,a)]. given #79 (T,wt=7): 710 A(cb,ca,ca) | ca <= cx. [hyper(32,b,671,a,c,45,a)]. given #80 (T,wt=7): 715 x v y <= y v x. [hyper(686,b,21,a)]. given #81 (A,wt=10): 66 A(x,y,z) | y <= x | z <= y. [hyper(32,b,36,b,c,36,a)]. given #82 (F,wt=6): 802 cx <= ca | cb <= cx. [hyper(37,a,66,a)]. given #83 (F,wt=7): 716 x ^ y <= y ^ x. [hyper(686,b,20,a)]. given #84 (T,wt=7): 733 A(cb,cx,cx) | ca <= cx. [hyper(33,b,45,a,c,727,a)]. given #85 (T,wt=7): 736 A(ca,cb,cx) | ca <= cx. [hyper(33,b,727,a,c,671,a),merge(c)]. given #86 (A,wt=9): 67 ca ^ (cb ^ cx) = ca ^ cb. [hyper(34,a,38,a),rewrite(20(5),48(5),20(4))]. given #87 (F,wt=7): 741 A(cb,cb,cx) | ca <= cx. [hyper(33,b,727,a,c,45,a)]. given #88 (F,wt=7): 747 A(cx,cx,cb) | ca <= cx. [hyper(32,b,45,a,c,727,a)]. given #89 (T,wt=7): 750 A(cx,cb,ca) | ca <= cx. [hyper(32,b,727,a,c,671,a),merge(c)]. given #90 (T,wt=7): 755 A(cx,cb,cb) | ca <= cx. [hyper(32,b,727,a,c,45,a)]. given #91 (A,wt=11): 68 A(cx,ca ^ cb,x) | ca ^ cb <= x. [hyper(33,b,36,b,c,38,a)]. given #92 (F,wt=7): 808 A(ca,cx,cx) | cb <= cx. [hyper(33,b,45,a,c,802,a)]. given #93 (F,wt=7): 815 A(ca,ca,cx) | cb <= cx. [hyper(33,b,802,a,c,45,a)]. given #94 (T,wt=7): 821 A(cx,cx,ca) | cb <= cx. [hyper(32,b,45,a,c,802,a)]. given #95 (T,wt=7): 828 A(cx,ca,ca) | cb <= cx. [hyper(32,b,802,a,c,45,a)]. given #96 (A,wt=9): 69 A(x,cx,ca ^ cb) | x <= cx. [hyper(33,b,38,a,c,36,b)]. given #97 (F,wt=7): 881 ca ^ cb <= cb ^ cx. [para(67(a,1),158(a,1))]. given #98 (F,wt=8): 73 A(ca v cb,cx,ca ^ cb). [hyper(33,b,38,a,c,39,a)]. given #99 (T,wt=8): 76 A(ca ^ cb,cx,ca v cb). [hyper(32,b,38,a,c,39,a)]. given #100 (T,wt=8): 79 A(ca v cb,ca v cb,cx). [hyper(33,b,39,a,c,45,a)]. given #101 (A,wt=11): 70 A(x,ca ^ cb,cx) | ca ^ cb <= x. [hyper(32,b,36,b,c,38,a)]. given #102 (F,wt=8): 83 A(cx,ca ^ cb,ca ^ cb). [hyper(33,b,45,a,c,38,a)]. given #103 (F,wt=8): 85 A(cx,ca v cb,ca v cb). [hyper(32,b,39,a,c,45,a)]. given #104 (T,wt=8): 89 A(ca ^ cb,ca ^ cb,cx). [hyper(32,b,45,a,c,38,a)]. given #105 (T,wt=8): 103 A(cx v x,cx,ca ^ cb). [hyper(33,b,38,a,c,61,a)]. given #106 (A,wt=9): 71 A(ca ^ cb,cx,x) | x <= cx. [hyper(32,b,38,a,c,36,b)]. given #107 (F,wt=8): 105 A(x v y,x v y,x). [hyper(33,b,61,a,c,45,a)]. given #108 (F,wt=8): 110 A(ca ^ cb,cx,cx v x). [hyper(32,b,38,a,c,61,a)]. given #109 (T,wt=8): 112 A(x,x v y,x v y). [hyper(32,b,61,a,c,45,a)]. given #110 (T,wt=8): 120 A(x v cx,cx,ca ^ cb). [hyper(33,b,38,a,c,114,a)]. given #111 (A,wt=9): 74 A(ca v cb,cx,x) | cx <= x. [hyper(33,b,36,b,c,39,a)]. given #112 (F,wt=8): 123 A(x v y,x v y,y). [hyper(33,b,114,a,c,45,a)]. given #113 (F,wt=8): 129 A(ca ^ cb,cx,x v cx). [hyper(32,b,38,a,c,114,a)]. given #114 (T,wt=8): 132 A(x,y v x,y v x). [hyper(32,b,114,a,c,45,a)]. given #115 (T,wt=8): 141 A(x,x ^ y,x ^ y). [hyper(33,b,45,a,c,135,a)]. given #116 (A,wt=11): 75 A(x,ca v cb,cx) | x <= ca v cb. [hyper(33,b,39,a,c,36,b)]. given #117 (F,wt=8): 143 A(x v y,y,y ^ z). [hyper(33,b,135,a,c,114,a)]. given #118 (F,wt=8): 144 A(x v y,x,x ^ z). [hyper(33,b,135,a,c,61,a)]. given #119 (T,wt=8): 146 A(ca v cb,cx,cx ^ x). [hyper(33,b,135,a,c,39,a)]. given #120 (T,wt=8): 150 A(x ^ y,x ^ y,x). [hyper(32,b,45,a,c,135,a)]. given #121 (A,wt=9): 77 A(x,cx,ca v cb) | cx <= x. [hyper(32,b,36,b,c,39,a)]. given #122 (F,wt=8): 152 A(x ^ y,x,z v x). [hyper(32,b,135,a,c,114,a)]. given #123 (F,wt=8): 153 A(x ^ y,x,x v z). [hyper(32,b,135,a,c,61,a)]. given #124 (T,wt=8): 155 A(cx ^ x,cx,ca v cb). [hyper(32,b,135,a,c,39,a)]. given #125 (T,wt=8): 163 A(x,y ^ x,y ^ x). [hyper(33,b,45,a,c,158,a)]. given #126 (A,wt=11): 78 A(cx,ca v cb,x) | x <= ca v cb. [hyper(32,b,39,a,c,36,b)]. given #127 (F,wt=8): 166 A(x v y,y,z ^ y). [hyper(33,b,158,a,c,114,a)]. given #128 (F,wt=8): 167 A(x v y,x,z ^ x). [hyper(33,b,158,a,c,61,a)]. given #129 (T,wt=8): 169 A(ca v cb,cx,x ^ cx). [hyper(33,b,158,a,c,39,a)]. given #130 (T,wt=8): 174 A(x ^ y,x ^ y,y). [hyper(32,b,45,a,c,158,a)]. given #131 (A,wt=11): 91 x ^ (y ^ (x v z)) = y ^ x. [para(25(a,1),48(a,1,2)),flip(a)]. given #132 (F,wt=8): 177 A(x ^ y,y,z v y). [hyper(32,b,158,a,c,114,a)]. given #133 (F,wt=8): 178 A(x ^ y,y,y v z). [hyper(32,b,158,a,c,61,a)]. given #134 (T,wt=8): 180 A(x ^ cx,cx,ca v cb). [hyper(32,b,158,a,c,39,a)]. given #135 (T,wt=8): 191 A(x v (y v z),y,y). [para(50(a,1),101(a,1))]. given #136 (A,wt=9): 92 x v (y ^ (x ^ z)) = x. [para(48(a,1),27(a,1,2))]. given #137 (F,wt=8): 193 A(x,x,y v (x v z)). [para(50(a,1),108(a,3))]. given #138 (F,wt=8): 200 A(x v (y v z),z,z). [para(23(a,1),118(a,1))]. given #139 (T,wt=8): 202 A(x,x,y v (z v x)). [para(23(a,1),127(a,3))]. given #140 (T,wt=8): 205 A(x,x,y ^ (x ^ z)). [para(48(a,1),145(a,3))]. given #141 (A,wt=12): 93 x <= y ^ z | y ^ (x ^ z) != x. [para(48(a,1),35(b,1))]. given #142 (F,wt=8): 207 A(x ^ (y ^ z),y,y). [para(48(a,1),154(a,1))]. given #143 (F,wt=8): 216 A(x,x,y ^ (z ^ x)). [para(22(a,1),168(a,3))]. given #144 (T,wt=8): 220 A(x ^ (y ^ z),z,z). [para(22(a,1),179(a,1))]. given #145 (T,wt=8): 554 A(x v (ca v cb),cx,cx). [hyper(33,b,45,a,c,450,a)]. given #146 (A,wt=9): 94 x ^ (x ^ y) = x ^ y. [para(59(a,1),22(a,1,1)),flip(a)]. given #147 (F,wt=8): 567 A(cx,cx,x v (ca v cb)). [hyper(32,b,45,a,c,450,a)]. given #148 (F,wt=8): 583 A(ca v (cb v x),cx,cx). [hyper(33,b,45,a,c,509,a)]. given #149 (T,wt=8): 596 A(cx,cx,ca v (cb v x)). [hyper(32,b,45,a,c,509,a)]. given #150 (T,wt=8): 644 A(ca v (x v cb),cx,cx). [hyper(33,b,45,a,c,577,a)]. given #151 (A,wt=9): 96 x ^ (y ^ x) = y ^ x. [para(59(a,1),22(a,2,2)),rewrite(20(2))]. given #152 (F,wt=8): 657 A(cx,cx,ca v (x v cb)). [hyper(32,b,45,a,c,577,a)]. given #153 (F,wt=8): 667 x <= y | x ^ y = y. [para(64(a,1),20(a,1)),flip(b)]. given #154 (T,wt=6): 1100 ca <= cb | cb <= cx. [para(667(b,1),38(a,1))]. given #155 (T,wt=7): 1103 ca <= cb | A(cx,cx,cb). [para(667(b,1),80(a,3))]. given #156 (A,wt=9): 97 x v (x v y) = x v y. [para(60(a,1),23(a,1,1)),flip(a)]. given #157 (F,wt=7): 1104 ca <= cb | A(cb,cx,cx). [para(667(b,1),86(a,1))]. given #158 (F,wt=7): 1145 A(cx,cb,cb) | ca <= cb. [hyper(33,b,45,a,c,1100,b)]. given #159 (T,wt=7): 1157 A(cb,cb,cx) | ca <= cb. [hyper(32,b,45,a,c,1100,b)]. given #160 (T,wt=8): 679 x <= y | x v y = x. [para(64(a,1),55(a,1,2))]. given #161 (A,wt=9): 99 x v (y v x) = y v x. [para(60(a,1),23(a,2,2)),rewrite(21(2))]. given #162 (F,wt=6): 1168 ca <= cb | cx <= ca. [para(679(b,1),39(a,2))]. given #163 (F,wt=3): 1219 ca <= cb. [hyper(33,b,1100,b,c,1168,b),merge(c),unit_del(a,37)]. given #164 (T,wt=3): 1304 ca <= cx. [back_rewrite(748),rewrite(1220(3)),unit_del(a,37)]. given #165 (T,wt=4): 1227 A(cb,ca,ca). [hyper(33,b,45,a,c,1219,a)]. given #166 (A,wt=10): 100 A(x v (y v z),x v y,x). [hyper(33,b,61,a,c,61,a),rewrite(23(2))]. given #167 (F,wt=4): 1234 A(cb,cb,ca). [hyper(33,b,1219,a,c,45,a)]. given #168 (F,wt=4): 1241 A(ca,ca,cb). [hyper(32,b,45,a,c,1219,a)]. given #169 (T,wt=4): 1247 A(ca,cb,cb). [hyper(32,b,1219,a,c,45,a)]. given #170 (T,wt=4): 1327 A(ca,ca,cx). [back_rewrite(89),rewrite(1220(3),1220(4))]. given #171 (A,wt=10): 102 A(ca v (cb v x),ca v cb,cx). [hyper(33,b,39,a,c,61,a),rewrite(23(4))]. given #172 (F,wt=4): 1328 A(ca,cx,cx). [back_rewrite(86),rewrite(1220(3))]. given #173 (F,wt=4): 1329 A(cx,ca,ca). [back_rewrite(83),rewrite(1220(4),1220(5))]. given #174 (T,wt=4): 1330 A(cx,cx,ca). [back_rewrite(80),rewrite(1220(5))]. given #175 (T,wt=5): 1220 ca ^ cb = ca. [hyper(34,a,1219,a)]. ============================== PROOF ================================= % Proof 1 at 0.07 (+ 0.02) seconds. % Length of proof is 29. % Level of proof is 8. % Maximum clause weight is 10. % Given clauses 175. 1 (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)) # label(non_clause). [assumption]. 5 (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)) # label(non_clause). [assumption]. 6 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause). [assumption]. 17 -D(x,y,z) | x ^ z <= y. [clausify(5)]. 18 -D(x,y,z) | y <= x v z. [clausify(5)]. 19 D(ca,cx,cb). [assumption]. 20 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 21 x v y = y v x # label("commutativity_join"). [assumption]. 26 (x ^ y) v x = x # label("absorption_2"). [assumption]. 27 x v (x ^ y) = x. [copy(26),rewrite(21(2))]. 32 A(x,y,z) | -(x <= y) | -(y <= z). [clausify(1)]. 33 A(x,y,z) | -(z <= y) | -(y <= x). [clausify(1)]. 34 -(x <= y) | x ^ y = x. [clausify(6)]. 36 x <= y | y <= x. [assumption]. 37 -A(ca,cx,cb). [assumption]. 38 ca ^ cb <= cx. [resolve(19,a,17,a)]. 39 cx <= ca v cb. [resolve(19,a,18,a)]. 55 x v (y ^ x) = x. [para(20(a,1),27(a,1,2))]. 64 x ^ y = x | y <= x. [hyper(34,a,36,a)]. 76 A(ca ^ cb,cx,ca v cb). [hyper(32,b,38,a,c,39,a)]. 667 x <= y | x ^ y = y. [para(64(a,1),20(a,1)),flip(b)]. 679 x <= y | x v y = x. [para(64(a,1),55(a,1,2))]. 1100 ca <= cb | cb <= cx. [para(667(b,1),38(a,1))]. 1168 ca <= cb | cx <= ca. [para(679(b,1),39(a,2))]. 1219 ca <= cb. [hyper(33,b,1100,b,c,1168,b),merge(c),unit_del(a,37)]. 1220 ca ^ cb = ca. [hyper(34,a,1219,a)]. 1331 A(ca,cx,ca v cb). [back_rewrite(76),rewrite(1220(3))]. 1360 ca v cb = cb. [para(1220(a,1),55(a,1,2)),rewrite(21(3))]. 1375 $F. [back_rewrite(1331),rewrite(1360(5)),unit_del(a,37)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=175. Generated=3994. Kept=1353. proofs=1. Usable=134. Sos=929. Demods=104. Limbo=15, Disabled=306. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=2640. Back_subsumed=157. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=116 (6 lex), Back_demodulated=115. Back_unit_deleted=1. Demod_attempts=25880. Demod_rewrites=2410. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=8144. Nonunit_bsub_feature_tests=7836. Megabytes=0.74. User_CPU=0.07, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11451 exit (max_proofs) Sat Aug 12 21:01:21 2006