============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5131 was started by mccune on cleo, Tue Nov 3 09:45:23 2009 The command was "/home/mccune/LADR/bin/prover9 -f head.in bcs.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 bcs.in formulas(goals). (all a all x all b (B(a,x,b) -> CS(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 (B(a,x,b) -> CS(a,x,b))). [goal]. 10 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a v x4) ^ (x4 v b) = x4 -> CS(a,x4,b))). [expand_def(9,3)]. ============================== 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 v x4) ^ (x4 v b) = x4 -> (a v x4) ^ (x4 v b) = x4 & (a v b) ^ x4 = x4)) # label(non_clause) # label(goal). [expand_def(10,5)]. ============================== 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. (c1 v c2) ^ (c2 v c3) != c2 | (c1 v c3) ^ c2 != 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)]. kept: 19 (c1 v c2) ^ (c2 v c3) = c2. [deny(11)]. 20 (c1 v c2) ^ (c2 v c3) != c2 | (c1 v c3) ^ c2 != c2. [deny(11)]. kept: 21 c2 ^ (c1 v c3) != c2. [copy(20),rewrite([19(7),17(8)]),xx(a)]. kept: 22 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. kept: 23 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)]. 19 (c1 v c2) ^ (c2 v c3) = c2. [deny(11)]. 21 c2 ^ (c1 v c3) != c2. [copy(20),rewrite([19(7),17(8)]),xx(a)]. 22 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 23 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)]. 19 (c1 v c2) ^ (c2 v c3) = c2. [deny(11)]. 22 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 23 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=9): 19 (c1 v c2) ^ (c2 v c3) = c2. [deny(11)]. given #7 (I,wt=7): 21 c2 ^ (c1 v c3) != c2. [copy(20),rewrite([19(7),17(8)]),xx(a)]. given #8 (I,wt=7): 22 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. given #9 (I,wt=7): 23 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. given #10 (A,wt=11): 24 x v (y v z) = y v (x v z). [para(16(a,1),14(a,1,1)),rewrite([14(2)])]. given #11 (T,wt=5): 39 x v x = x. [para(23(a,1),22(a,1,2))]. given #12 (T,wt=5): 40 x ^ x = x. [para(22(a,1),23(a,1,2))]. given #13 (T,wt=7): 32 x v (y ^ x) = x. [para(17(a,1),22(a,1,2))]. given #14 (T,wt=7): 37 x ^ (y v x) = x. [para(16(a,1),23(a,1,2))]. given #15 (A,wt=11): 25 x ^ (y ^ z) = y ^ (x ^ z). [para(17(a,1),15(a,1,1)),rewrite([15(2)])]. given #16 (T,wt=9): 43 x ^ (y v (x v z)) = x. [para(24(a,1),23(a,1,2))]. given #17 (T,wt=9): 44 x v (x v y) = x v y. [para(39(a,1),14(a,1,1)),flip(a)]. given #18 (T,wt=9): 46 x v (y v x) = y v x. [para(39(a,1),14(a,2,2)),rewrite([16(2)])]. given #19 (T,wt=9): 47 x ^ (x ^ y) = x ^ y. [para(40(a,1),15(a,1,1)),flip(a)]. given #20 (A,wt=13): 26 (c1 ^ c2) v ((c2 ^ c3) v x) = c2 v x. [para(18(a,1),14(a,1,1)),flip(a)]. given #21 (T,wt=9): 49 x ^ (y ^ x) = y ^ x. [para(40(a,1),15(a,2,2)),rewrite([17(2)])]. given #22 (T,wt=9): 52 x v (y ^ (z ^ x)) = x. [para(15(a,1),32(a,1,2))]. given #23 (T,wt=9): 54 x ^ (y v (z v x)) = x. [para(14(a,1),37(a,1,2))]. given #24 (T,wt=9): 59 x v (y ^ (x ^ z)) = x. [para(25(a,1),22(a,1,2))]. given #25 (A,wt=13): 27 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(18(a,1),14(a,2,2)),rewrite([16(8)])]. given #26 (T,wt=9): 96 c1 v (c2 ^ c3) = c1 v c2. [para(22(a,1),27(a,1,2)),rewrite([16(5)])]. given #27 (T,wt=11): 29 x v ((x ^ y) v z) = x v z. [para(22(a,1),14(a,1,1)),flip(a)]. given #28 (T,wt=11): 35 x ^ ((x v y) ^ z) = x ^ z. [para(23(a,1),15(a,1,1)),flip(a)]. given #29 (T,wt=9): 112 c1 ^ (c2 v c3) = c1 ^ c2. [para(19(a,1),35(a,1,2)),flip(a)]. given #30 (A,wt=13): 28 (c1 v c2) ^ ((c2 v c3) ^ x) = c2 ^ x. [para(19(a,1),15(a,1,1)),flip(a)]. given #31 (T,wt=11): 42 x v (y v (x ^ z)) = y v x. [para(22(a,1),24(a,1,2)),flip(a)]. given #32 (T,wt=11): 50 x v ((y ^ x) v z) = x v z. [para(32(a,1),14(a,1,1)),flip(a)]. given #33 (T,wt=11): 53 x v (y v (z ^ x)) = y v x. [para(32(a,1),24(a,1,2)),flip(a)]. given #34 (T,wt=9): 138 c3 v (c1 ^ c2) = c2 v c3. [para(18(a,1),53(a,1,2)),rewrite([16(3),16(8)]),flip(a)]. given #35 (A,wt=13): 30 x v (y v ((x v y) ^ z)) = x v y. [para(22(a,1),14(a,1)),flip(a)]. given #36 (T,wt=9): 142 c1 v (c2 v c3) = c1 v c3. [para(96(a,1),53(a,1,2)),rewrite([24(5),16(4)])]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 24. % Level of proof is 7. % Maximum clause weight is 13.000. % Given clauses 36. 3 (all x all y all z (B(x,y,z) <-> (x ^ y) v (y ^ z) = y & (x v y) ^ (y v z) = y)) # 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]. 9 (all a all x all b (B(a,x,b) -> CS(a,x,b))) # label(non_clause). [goal]. 10 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a v x4) ^ (x4 v b) = x4 -> CS(a,x4,b))) # label(non_clause). [expand_def(9,3)]. 11 (all a all x4 all b ((a ^ x4) v (x4 ^ b) = x4 & (a v x4) ^ (x4 v b) = x4 -> (a v x4) ^ (x4 v b) = x4 & (a v b) ^ x4 = x4)) # label(non_clause) # label(goal). [expand_def(10,5)]. 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]. 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 v c2) ^ (c2 v c3) = c2. [deny(11)]. 20 (c1 v c2) ^ (c2 v c3) != c2 | (c1 v c3) ^ c2 != c2. [deny(11)]. 21 c2 ^ (c1 v c3) != c2. [copy(20),rewrite([19(7),17(8)]),xx(a)]. 22 x v (x ^ y) = x. [back_rewrite(12),rewrite([16(2)])]. 23 x ^ (x v y) = x. [back_rewrite(13),rewrite([17(2)])]. 24 x v (y v z) = y v (x v z). [para(16(a,1),14(a,1,1)),rewrite([14(2)])]. 27 (c2 ^ c3) v (x v (c1 ^ c2)) = x v c2. [para(18(a,1),14(a,2,2)),rewrite([16(8)])]. 32 x v (y ^ x) = x. [para(17(a,1),22(a,1,2))]. 43 x ^ (y v (x v z)) = x. [para(24(a,1),23(a,1,2))]. 53 x v (y v (z ^ x)) = y v x. [para(32(a,1),24(a,1,2)),flip(a)]. 96 c1 v (c2 ^ c3) = c1 v c2. [para(22(a,1),27(a,1,2)),rewrite([16(5)])]. 142 c1 v (c2 v c3) = c1 v c3. [para(96(a,1),53(a,1,2)),rewrite([24(5),16(4)])]. 159 $F. [para(142(a,1),43(a,1,2)),unit_del(a,21)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=1096. Kept=146. proofs=1. Usable=36. Sos=89. Demods=123. Limbo=4, Disabled=26. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=949. Back_subsumed=8. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=140 (4 lex), Back_demodulated=9. Back_unit_deleted=0. Demod_attempts=10162. Demod_rewrites=1945. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.17. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5131 exit (max_proofs) Tue Nov 3 09:45:23 2009