============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11674 was started by mccune on cleo, Wed Feb 25 09:36:20 2009 The command was "/home/mccune/bin/prover9 -f head.in cd.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file head.in assign(max_seconds,60). set(expand_relational_defs). formulas(assumptions). 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(assumptions). (all x all y (x <= y <-> x ^ y = x)). (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)). (all x all y all z (C(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x ^ z) v y = y)). (all x all y all z (CS(x,y,z) <-> (x v y) ^ (y v z) = y & (x v z) ^ y = y)). (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). end_of_list. % Reading from file cd.in formulas(goals). (all a all x all b (C(a,x,b) -> D(a,x,b))). end_of_list. ============================== end of input ========================== ============================== EXPAND RELATIONAL DEFINITIONS ========= % Relational Definitions: 1 (all x all y (x <= y <-> x ^ y = x)). [assumption]. 2 (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). [assumption]. 3 (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)). [assumption]. 4 (all x all y all z (C(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x ^ z) v y = y)). [assumption]. 5 (all x all y all z (CS(x,y,z) <-> (x v y) ^ (y v z) = y & (x v z) ^ y = y)). [assumption]. 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). [assumption]. % Relational Definitions, Expanded: 7 (all x0 all x1 all z (A(x0,x1,z) <-> x0 ^ x1 = x0 & x1 ^ z = x1 | z ^ x1 = z & x1 ^ x0 = x1)). [expand_def(2,1)]. 8 (all x2 all x3 all z (D(x2,x3,z) <-> (x2 ^ z) ^ x3 = x2 ^ z & x3 ^ (x2 v z) = x3)). [expand_def(6,1)]. % Formulas Being Expanded: 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)). [assumption]. 2 (all x all y all z (A(x,y,z) <-> x <= y & y <= z | z <= y & y <= x)). [assumption]. 9 (all a all x all b (C(a,x,b) -> D(a,x,b))). [goal]. 10 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a ^ b) v x4 = x4 -> D(a,x4,b))). [expand_def(9,4)]. ============================== end of expand relational definitions == ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 11 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a ^ b) v x4 = x4 -> (a ^ b) ^ x4 = a ^ b & x4 ^ (a v b) = x4)) # label(non_clause) # label(goal). [expand_def(10,8)]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x ^ y) v x = x # label("absorption_2"). [assumption]. (x v y) ^ x = x # label("absorption_1"). [assumption]. (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. x v y = y v x # label("commutativity_join"). [assumption]. x ^ y = y ^ x # label("commutativity_meet"). [assumption]. (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. (c1 ^ c3) v c2 = c2. [deny(11)]. (c1 ^ c3) ^ c2 != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [deny(11)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 12 (x ^ y) v x = x # label("absorption_2"). [assumption]. kept: 13 (x v y) ^ x = x # label("absorption_1"). [assumption]. kept: 14 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. kept: 15 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. % Operation v is commutative; C redundancy checks enabled. kept: 16 x v y = y v x # label("commutativity_join"). [assumption]. % Operation ^ is commutative; C redundancy checks enabled. kept: 17 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. kept: 18 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. 19 (c1 ^ c3) v c2 = c2. [deny(11)]. kept: 20 c2 v (c1 ^ c3) = c2. [copy(19),rewrite([16(5)])]. 21 (c1 ^ c3) ^ c2 != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [deny(11)]. kept: 22 c2 ^ (c1 ^ c3) != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [copy(21),rewrite([17(5)])]. kept: 23 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. kept: 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 15 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 16 x v y = y v x # label("commutativity_join"). [assumption]. 17 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 18 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. 20 c2 v (c1 ^ c3) = c2. [copy(19),rewrite([16(5)])]. 22 c2 ^ (c1 ^ c3) != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [copy(21),rewrite([17(5)])]. 23 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. end_of_list. formulas(demodulators). 14 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 15 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 16 x v y = y v x # label("commutativity_join"). [assumption]. % (lex-dep) 17 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % (lex-dep) 18 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. 20 c2 v (c1 ^ c3) = c2. [copy(19),rewrite([16(5)])]. 23 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 14 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. given #2 (I,wt=11): 15 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. given #3 (I,wt=7): 16 x v y = y v x # label("commutativity_join"). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. given #4 (I,wt=7): 17 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. given #5 (I,wt=9): 18 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. given #6 (I,wt=7): 20 c2 v (c1 ^ c3) = c2. [copy(19),rewrite([16(5)])]. given #7 (I,wt=7): 23 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. given #8 (I,wt=7): 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. given #9 (A,wt=11): 25 x v (y v z) = y v (x v z). [para(16(a,1),14(a,1,1)),rewrite([14(2)])]. given #10 (F,wt=16): 27 c1 ^ (c2 ^ c3) != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [back_rewrite(22),rewrite([26(5)])]. given #11 (T,wt=5): 42 x v x = x. [para(24(a,1),23(a,1,2))]. given #12 (T,wt=5): 43 x ^ x = x. [para(23(a,1),24(a,1,2))]. given #13 (T,wt=7): 35 x v (y ^ x) = x. [para(17(a,1),23(a,1,2))]. given #14 (T,wt=7): 39 x ^ (y v x) = x. [para(16(a,1),24(a,1,2))]. given #15 (A,wt=11): 26 x ^ (y ^ z) = y ^ (x ^ z). [para(17(a,1),15(a,1,1)),rewrite([15(2)])]. given #16 (F,wt=7): 63 c2 ^ (c1 v c3) != c2. [back_rewrite(27),rewrite([61(5)]),xx(a)]. given #17 (T,wt=9): 47 x ^ (y v (x v z)) = x. [para(25(a,1),24(a,1,2))]. given #18 (T,wt=9): 48 x v (x v y) = x v y. [para(42(a,1),14(a,1,1)),flip(a)]. given #19 (T,wt=9): 50 x v (y v x) = y v x. [para(42(a,1),14(a,2,2)),rewrite([16(2)])]. given #20 (T,wt=9): 51 x ^ (x ^ y) = x ^ y. [para(43(a,1),15(a,1,1)),flip(a)]. given #21 (A,wt=13): 28 (c1 ^ c2) v ((c2 ^ c3) v x) = c2 v x. [para(18(a,1),14(a,1,1)),flip(a)]. given #22 (T,wt=9): 53 x ^ (y ^ x) = y ^ x. [para(43(a,1),15(a,2,2)),rewrite([17(2)])]. given #23 (T,wt=9): 56 x v (y ^ (z ^ x)) = x. [para(15(a,1),35(a,1,2))]. given #24 (T,wt=9): 58 x ^ (y v (z v x)) = x. [para(14(a,1),39(a,1,2))]. given #25 (T,wt=9): 61 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(20(a,1),39(a,1,2)),rewrite([17(5),26(5)])]. given #26 (A,wt=13): 29 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(18(a,1),14(a,2,2)),rewrite([16(8)])]. given #27 (T,wt=9): 64 x v (y ^ (x ^ z)) = x. [para(26(a,1),23(a,1,2))]. given #28 (T,wt=9): 102 c1 v (c2 ^ c3) = c1 v c2. [para(23(a,1),29(a,1,2)),rewrite([16(5)])]. given #29 (T,wt=11): 30 c2 v ((c1 ^ c3) v x) = c2 v x. [para(20(a,1),14(a,1,1)),flip(a)]. given #30 (T,wt=9): 116 c2 v (c1 ^ (c3 ^ x)) = c2. [para(23(a,1),30(a,1,2)),rewrite([20(5),15(6)]),flip(a)]. given #31 (A,wt=11): 31 (c1 ^ c3) v (x v c2) = x v c2. [para(20(a,1),14(a,2,2)),rewrite([16(6)])]. given #32 (T,wt=9): 118 c2 v (x ^ (c1 ^ c3)) = c2. [para(35(a,1),30(a,1,2)),rewrite([20(5)]),flip(a)]. given #33 (T,wt=9): 125 c2 v (c1 ^ (x ^ c3)) = c2. [para(17(a,1),116(a,1,2,2))]. given #34 (T,wt=11): 32 x v ((x ^ y) v z) = x v z. [para(23(a,1),14(a,1,1)),flip(a)]. given #35 (T,wt=11): 37 x ^ ((x v y) ^ z) = x ^ z. [para(24(a,1),15(a,1,1)),flip(a)]. given #36 (A,wt=13): 33 x v (y v ((x v y) ^ z)) = x v y. [para(23(a,1),14(a,1)),flip(a)]. given #37 (T,wt=11): 45 c2 v (x v (c1 ^ c3)) = x v c2. [para(20(a,1),25(a,1,2)),flip(a)]. given #38 (T,wt=11): 46 x v (y v (x ^ z)) = y v x. [para(23(a,1),25(a,1,2)),flip(a)]. given #39 (T,wt=11): 54 x v ((y ^ x) v z) = x v z. [para(35(a,1),14(a,1,1)),flip(a)]. given #40 (T,wt=11): 57 x v (y v (z ^ x)) = y v x. [para(35(a,1),25(a,1,2)),flip(a)]. given #41 (A,wt=13): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(15(a,1),23(a,1,2))]. given #42 (T,wt=9): 183 c3 v (c1 ^ c2) = c2 v c3. [para(18(a,1),57(a,1,2)),rewrite([16(3),16(8)]),flip(a)]. given #43 (T,wt=9): 188 c1 v (c2 v c3) = c1 v c3. [para(102(a,1),57(a,1,2)),rewrite([25(5),16(4)])]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 33. % Level of proof is 7. % Maximum clause weight is 16. % Given clauses 43. 1 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause). [assumption]. 4 (all x all y all z (C(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x ^ z) v y = y)) # label(non_clause). [assumption]. 6 (all x all y all z (D(x,y,z) <-> x ^ z <= y & y <= x v z)) # label(non_clause). [assumption]. 8 (all x2 all x3 all z (D(x2,x3,z) <-> (x2 ^ z) ^ x3 = x2 ^ z & x3 ^ (x2 v z) = x3)) # label(non_clause). [expand_def(6,1)]. 9 (all a all x all b (C(a,x,b) -> D(a,x,b))) # label(non_clause). [goal]. 10 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a ^ b) v x4 = x4 -> D(a,x4,b))) # label(non_clause). [expand_def(9,4)]. 11 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a ^ b) v x4 = x4 -> (a ^ b) ^ x4 = a ^ b & x4 ^ (a v b) = x4)) # label(non_clause) # label(goal). [expand_def(10,8)]. 12 (x ^ y) v x = x # label("absorption_2"). [assumption]. 13 (x v y) ^ x = x # label("absorption_1"). [assumption]. 14 (x v y) v z = x v (y v z) # label("associativity_join"). [assumption]. 15 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet"). [assumption]. 16 x v y = y v x # label("commutativity_join"). [assumption]. 17 x ^ y = y ^ x # label("commutativity_meet"). [assumption]. 18 (c1 ^ c2) v (c2 ^ c3) = c2. [deny(11)]. 19 (c1 ^ c3) v c2 = c2. [deny(11)]. 20 c2 v (c1 ^ c3) = c2. [copy(19),rewrite([16(5)])]. 21 (c1 ^ c3) ^ c2 != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [deny(11)]. 22 c2 ^ (c1 ^ c3) != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [copy(21),rewrite([17(5)])]. 23 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. 25 x v (y v z) = y v (x v z). [para(16(a,1),14(a,1,1)),rewrite([14(2)])]. 26 x ^ (y ^ z) = y ^ (x ^ z). [para(17(a,1),15(a,1,1)),rewrite([15(2)])]. 27 c1 ^ (c2 ^ c3) != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [back_rewrite(22),rewrite([26(5)])]. 29 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(18(a,1),14(a,2,2)),rewrite([16(8)])]. 35 x v (y ^ x) = x. [para(17(a,1),23(a,1,2))]. 39 x ^ (y v x) = x. [para(16(a,1),24(a,1,2))]. 47 x ^ (y v (x v z)) = x. [para(25(a,1),24(a,1,2))]. 57 x v (y v (z ^ x)) = y v x. [para(35(a,1),25(a,1,2)),flip(a)]. 61 c1 ^ (c2 ^ c3) = c1 ^ c3. [para(20(a,1),39(a,1,2)),rewrite([17(5),26(5)])]. 63 c2 ^ (c1 v c3) != c2. [back_rewrite(27),rewrite([61(5)]),xx(a)]. 102 c1 v (c2 ^ c3) = c1 v c2. [para(23(a,1),29(a,1,2)),rewrite([16(5)])]. 188 c1 v (c2 v c3) = c1 v c3. [para(102(a,1),57(a,1,2)),rewrite([25(5),16(4)])]. 204 $F. [para(188(a,1),47(a,1,2)),unit_del(a,63)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=43. Generated=1389. Kept=190. proofs=1. Usable=42. Sos=125. Demods=163. Limbo=4, Disabled=28. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1198. Back_subsumed=9. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=180 (4 lex), Back_demodulated=10. Back_unit_deleted=0. Demod_attempts=13543. Demod_rewrites=2514. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=2. Nonunit_bsub_feature_tests=2. Megabytes=0.21. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11674 exit (max_proofs) Wed Feb 25 09:36:20 2009