============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5133 was started by mccune on cleo, Tue Nov 3 09:45:23 2009 The command was "/home/mccune/LADR/bin/prover9 -f head.in csd.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 csd.in formulas(goals). (all a all x all b (CS(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 (CS(a,x,b) -> D(a,x,b))). [goal]. 10 (all a all x4 all b ((a v x4) ^ (x4 v b) = x4 & (a v b) ^ x4 = x4 -> D(a,x4,b))). [expand_def(9,5)]. ============================== end of expand relational definitions == ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 11 (all a all x4 all b ((a v x4) ^ (x4 v b) = x4 & (a v b) ^ 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. (c1 v c3) ^ 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. 19 (c1 v c3) ^ c2 = c2. [deny(11)]. kept: 20 c2 ^ (c1 v c3) = c2. [copy(19),rewrite([17(5)])]. 21 (c1 ^ c3) ^ c2 != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [deny(11)]. kept: 22 c2 ^ (c1 ^ c3) != c1 ^ c3. [copy(21),rewrite([17(5),20(14)]),xx(b)]. 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. 20 c2 ^ (c1 v c3) = c2. [copy(19),rewrite([17(5)])]. 22 c2 ^ (c1 ^ c3) != c1 ^ c3. [copy(21),rewrite([17(5),20(14)]),xx(b)]. 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. 20 c2 ^ (c1 v c3) = c2. [copy(19),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. ============================== 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. given #6 (I,wt=7): 20 c2 ^ (c1 v c3) = c2. [copy(19),rewrite([17(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=9): 27 c1 ^ (c2 ^ c3) != c1 ^ c3. [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): 41 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 (T,wt=9): 45 x ^ (y v (x v z)) = x. [para(25(a,1),24(a,1,2))]. given #17 (T,wt=9): 46 x v (x v y) = x v y. [para(42(a,1),14(a,1,1)),flip(a)]. given #18 (T,wt=9): 48 x v (y v x) = y v x. [para(42(a,1),14(a,2,2)),rewrite([16(2)])]. given #19 (T,wt=9): 49 x ^ (x ^ y) = x ^ y. [para(43(a,1),15(a,1,1)),flip(a)]. given #20 (A,wt=13): 28 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(18(a,1),15(a,1,1)),flip(a)]. given #21 (T,wt=9): 51 x ^ (y ^ x) = y ^ x. [para(43(a,1),15(a,2,2)),rewrite([17(2)])]. given #22 (T,wt=9): 54 x v (y ^ (z ^ x)) = x. [para(15(a,1),35(a,1,2))]. given #23 (T,wt=9): 55 c1 v (c2 v c3) = c1 v c3. [para(20(a,1),35(a,1,2)),rewrite([16(5),25(5)])]. given #24 (T,wt=9): 57 x ^ (y v (z v x)) = x. [para(14(a,1),41(a,1,2))]. given #25 (A,wt=13): 29 (c2 v c3) ^ (x ^ (c1 v c2)) = x ^ c2. [para(18(a,1),15(a,2,2)),rewrite([17(8)])]. given #26 (T,wt=9): 63 x v (y ^ (x ^ z)) = x. [para(26(a,1),23(a,1,2))]. given #27 (T,wt=9): 100 c1 ^ (c2 v c3) = c1 ^ c2. [para(24(a,1),29(a,1,2)),rewrite([17(5)])]. given #28 (T,wt=11): 30 c2 ^ ((c1 v c3) ^ x) = c2 ^ x. [para(20(a,1),15(a,1,1)),flip(a)]. given #29 (T,wt=9): 114 c2 ^ (c1 v (c3 v x)) = c2. [para(24(a,1),30(a,1,2)),rewrite([20(5),14(6)]),flip(a)]. given #30 (A,wt=11): 31 (c1 v c3) ^ (x ^ c2) = x ^ c2. [para(20(a,1),15(a,2,2)),rewrite([17(6)])]. given #31 (T,wt=9): 116 c2 ^ (x v (c1 v c3)) = c2. [para(41(a,1),30(a,1,2)),rewrite([20(5)]),flip(a)]. given #32 (T,wt=9): 123 c2 ^ (c1 v (x v c3)) = c2. [para(16(a,1),114(a,1,2,2))]. given #33 (T,wt=11): 32 x v ((x ^ y) v z) = x v z. [para(23(a,1),14(a,1,1)),flip(a)]. given #34 (T,wt=11): 39 x ^ ((x v y) ^ z) = x ^ z. [para(24(a,1),15(a,1,1)),flip(a)]. given #35 (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 #36 (T,wt=11): 44 x v (y v (x ^ z)) = y v x. [para(23(a,1),25(a,1,2)),flip(a)]. given #37 (T,wt=11): 52 x v ((y ^ x) v z) = x v z. [para(35(a,1),14(a,1,1)),flip(a)]. given #38 (T,wt=11): 56 x v (y v (z ^ x)) = y v x. [para(35(a,1),25(a,1,2)),flip(a)]. given #39 (T,wt=11): 58 x ^ ((y v x) ^ z) = x ^ z. [para(41(a,1),15(a,1,1)),flip(a)]. given #40 (A,wt=13): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(15(a,1),23(a,1,2))]. given #41 (T,wt=11): 62 c2 ^ (x ^ (c1 v c3)) = x ^ c2. [para(20(a,1),26(a,1,2)),flip(a)]. given #42 (T,wt=11): 64 x ^ (y ^ (x v z)) = y ^ x. [para(24(a,1),26(a,1,2)),flip(a)]. given #43 (T,wt=11): 66 x ^ (y ^ (z v x)) = y ^ x. [para(41(a,1),26(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 24. % Level of proof is 7. % Maximum clause weight is 13.000. % Given clauses 43. 1 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause). [assumption]. 5 (all x all y all z (CS(x,y,z) <-> (x v y) ^ (y v z) = y & (x v z) ^ 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 (CS(a,x,b) -> D(a,x,b))) # label(non_clause). [goal]. 10 (all a all x4 all b ((a v x4) ^ (x4 v b) = x4 & (a v b) ^ x4 = x4 -> D(a,x4,b))) # label(non_clause). [expand_def(9,5)]. 11 (all a all x4 all b ((a v x4) ^ (x4 v b) = x4 & (a v b) ^ x4 = x4 -> (a ^ b) ^ x4 = a ^ b & x4 ^ (a v b) = x4)) # label(non_clause) # label(goal). [expand_def(10,8)]. 13 (x v y) ^ x = x # label("absorption_1"). [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 v c2) ^ (c2 v c3) = c2. [deny(11)]. 19 (c1 v c3) ^ c2 = c2. [deny(11)]. 20 c2 ^ (c1 v c3) = c2. [copy(19),rewrite([17(5)])]. 21 (c1 ^ c3) ^ c2 != c1 ^ c3 | c2 ^ (c1 v c3) != c2. [deny(11)]. 22 c2 ^ (c1 ^ c3) != c1 ^ c3. [copy(21),rewrite([17(5),20(14)]),xx(b)]. 24 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(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. [back_rewrite(22),rewrite([26(5)])]. 29 (c2 v c3) ^ (x ^ (c1 v c2)) = x ^ c2. [para(18(a,1),15(a,2,2)),rewrite([17(8)])]. 41 x ^ (y v x) = x. [para(16(a,1),24(a,1,2))]. 66 x ^ (y ^ (z v x)) = y ^ x. [para(41(a,1),26(a,1,2)),flip(a)]. 100 c1 ^ (c2 v c3) = c1 ^ c2. [para(24(a,1),29(a,1,2)),rewrite([17(5)])]. 237 $F. [para(100(a,1),66(a,1,2)),rewrite([26(5),17(4)]),unit_del(a,27)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=43. Generated=1585. Kept=223. proofs=1. Usable=43. Sos=156. Demods=190. Limbo=6, Disabled=27. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1361. Back_subsumed=7. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=206 (4 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=15064. Demod_rewrites=2861. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.24. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5133 exit (max_proofs) Tue Nov 3 09:45:23 2009