============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5124 was started by mccune on cleo, Tue Nov 3 09:45:16 2009 The command was "/home/mccune/LADR/bin/prover9 -f mol-ss1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mol-ss1.in assign(max_seconds,30). assign(new_constants,1). formulas(sos). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). f(f(x,x),f(x,y)) = x. f(x,f(x,x)) = f(y,f(y,y)). f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). x v y = f(f(x,x),f(y,y)) # label(definition_join). x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). x' = f(x,x) # label(definition_complementation). end_of_list. formulas(goals). x v (y v z) = y v (x v z) # answer(AJ). x v (x ^ y) = x # answer(B1). x ^ y = (x' v y')' # answer(DM). x'' = x # answer(CC). x v x' = y v y' # answer(ONE). x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). f(x,y) = x' v y' # answer(DEF_SS). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x v (y v z) = y v (x v z) # answer(AJ) # label(non_clause) # label(goal). [goal]. 2 x v (x ^ y) = x # answer(B1) # label(non_clause) # label(goal). [goal]. 3 x ^ y = (x' v y')' # answer(DM) # label(non_clause) # label(goal). [goal]. 4 x'' = x # answer(CC) # label(non_clause) # label(goal). [goal]. 5 x v x' = y v y' # answer(ONE) # label(non_clause) # label(goal). [goal]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD) # label(non_clause) # label(goal). [goal]. 7 f(x,y) = x' v y' # answer(DEF_SS) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [assumption]. f(f(x,x),f(x,y)) = x. [assumption]. f(x,f(x,x)) = f(y,f(y,y)). [assumption]. f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [assumption]. x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. x' = f(x,x) # label(definition_complementation). [assumption]. c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [deny(1)]. c4 v (c4 ^ c5) != c4 # answer(B1). [deny(2)]. (c6' v c7')' != c6 ^ c7 # answer(DM). [deny(3)]. c8'' != c8 # answer(CC). [deny(4)]. c10 v c10' != c9 v c9' # answer(ONE). [deny(5)]. c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [deny(6)]. f(c14,c15) != c14' v c15' # answer(DEF_SS). [deny(7)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 7). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, f, ^, v, ' ]). After inverse_order: (no changes). Unfolding symbols: '/1 ^/2 v/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 8 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [assumption]. kept: 9 f(f(x,x),f(x,y)) = x. [assumption]. kept: 10 f(x,f(x,x)) = f(y,f(y,y)). [assumption]. kept: 11 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [assumption]. kept: 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. kept: 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. kept: 14 x' = f(x,x) # label(definition_complementation). [assumption]. 15 c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [deny(1)]. kept: 16 f(f(c1,c1),f(f(f(c2,c2),f(c3,c3)),f(f(c2,c2),f(c3,c3)))) != f(f(c2,c2),f(f(f(c1,c1),f(c3,c3)),f(f(c1,c1),f(c3,c3)))) # answer(AJ). [copy(15),rewrite([12(4),12(9),12(23),12(28)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: AJ. % Length of proof is 6. % Level of proof is 3. % Maximum clause weight is 39.000. % Given clauses 0. 1 x v (y v z) = y v (x v z) # answer(AJ) # label(non_clause) # label(goal). [goal]. 8 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 15 c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [deny(1)]. 16 f(f(c1,c1),f(f(f(c2,c2),f(c3,c3)),f(f(c2,c2),f(c3,c3)))) != f(f(c2,c2),f(f(f(c1,c1),f(c3,c3)),f(f(c1,c1),f(c3,c3)))) # answer(AJ). [copy(15),rewrite([12(4),12(9),12(23),12(28)]),flip(a)]. 17 $F # answer(AJ). [resolve(16,a,8,a)]. ============================== end of proof ========================== % Redundant proof: 18 $F # answer(AJ). [resolve(16,a,8,a(flip))]. 19 c4 v (c4 ^ c5) != c4 # answer(B1). [deny(2)]. ============================== PROOF ================================= % Proof 2 at 0.01 (+ 0.00) seconds: B1. % Length of proof is 6. % Level of proof is 2. % Maximum clause weight is 11.000. % Given clauses 0. 2 x v (x ^ y) = x # answer(B1) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 19 c4 v (c4 ^ c5) != c4 # answer(B1). [deny(2)]. 20 $F # answer(B1). [copy(19),rewrite([13(4),12(9),9(18),9(7)]),xx(a)]. ============================== end of proof ========================== 21 (c6' v c7')' != c6 ^ c7 # answer(DM). [deny(3)]. ============================== PROOF ================================= % Proof 3 at 0.01 (+ 0.00) seconds: DM. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 11.000. % Given clauses 0. 3 x ^ y = (x' v y')' # answer(DM) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 21 (c6' v c7')' != c6 ^ c7 # answer(DM). [deny(3)]. 22 $F # answer(DM). [copy(21),rewrite([14(2),14(5),12(7),9(7),9(8),14(4),13(10)]),xx(a)]. ============================== end of proof ========================== 23 c8'' != c8 # answer(CC). [deny(4)]. ============================== PROOF ================================= % Proof 4 at 0.01 (+ 0.00) seconds: CC. % Length of proof is 5. % Level of proof is 2. % Maximum clause weight is 9.000. % Given clauses 0. 4 x'' = x # answer(CC) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 23 c8'' != c8 # answer(CC). [deny(4)]. 24 $F # answer(CC). [copy(23),rewrite([14(2),14(4),9(7)]),xx(a)]. ============================== end of proof ========================== 25 c10 v c10' != c9 v c9' # answer(ONE). [deny(5)]. kept: 26 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(25),rewrite([14(3),12(5),9(10),14(8),12(10),9(15)])]. 27 c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [deny(6)]. kept: 28 f(f(c11,c11),f(c12,f(f(c11,c11),f(c13,c13)))) != f(f(c11,c11),f(c13,f(f(c11,c11),f(c12,c12)))) # answer(MOD). [copy(27),rewrite([12(5),13(10),12(21),9(42),12(18),13(23),12(34),9(55)]),flip(a)]. ============================== PROOF ================================= % Proof 5 at 0.01 (+ 0.00) seconds: MOD. % Length of proof is 8. % Level of proof is 3. % Maximum clause weight is 27.000. % Given clauses 0. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 11 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 27 c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [deny(6)]. 28 f(f(c11,c11),f(c12,f(f(c11,c11),f(c13,c13)))) != f(f(c11,c11),f(c13,f(f(c11,c11),f(c12,c12)))) # answer(MOD). [copy(27),rewrite([12(5),13(10),12(21),9(42),12(18),13(23),12(34),9(55)]),flip(a)]. 29 $F # answer(MOD). [resolve(28,a,11,a)]. ============================== end of proof ========================== % Redundant proof: 30 $F # answer(MOD). [resolve(28,a,11,a(flip))]. 31 f(c14,c15) != c14' v c15' # answer(DEF_SS). [deny(7)]. ============================== PROOF ================================= % Proof 6 at 0.01 (+ 0.00) seconds: DEF_SS. % Length of proof is 6. % Level of proof is 2. % Maximum clause weight is 11.000. % Given clauses 0. 7 f(x,y) = x' v y' # answer(DEF_SS) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 31 f(c14,c15) != c14' v c15' # answer(DEF_SS). [deny(7)]. 32 $F # answer(DEF_SS). [copy(31),rewrite([14(5),14(8),12(10),9(10),9(11)]),xx(a)]. ============================== end of proof ========================== NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(10)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c_0, f, ^, v, ' ]). kept: 33 f(x,f(x,x)) = c_0. [new_symbol(10)]. % Disable descendants (x means already disabled): 31x 27x 28 23x 21x 19x 15x 16 ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 8 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [assumption]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 11 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 26 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(25),rewrite([14(3),12(5),9(10),14(8),12(10),9(15)])]. 33 f(x,f(x,x)) = c_0. [new_symbol(10)]. end_of_list. formulas(demodulators). 9 f(f(x,x),f(x,y)) = x. [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 33 f(x,f(x,x)) = c_0. [new_symbol(10)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=19): 8 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [assumption]. given #2 (I,wt=9): 9 f(f(x,x),f(x,y)) = x. [assumption]. given #3 (I,wt=19): 11 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [assumption]. given #4 (I,wt=11): 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. given #5 (I,wt=11): 13 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. given #6 (I,wt=6): 14 x' = f(x,x) # label(definition_complementation). [assumption]. given #7 (I,wt=11): 26 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(25),rewrite([14(3),12(5),9(10),14(8),12(10),9(15)])]. given #8 (I,wt=7): 33 f(x,f(x,x)) = c_0. [new_symbol(10)]. ============================== PROOF ================================= % Proof 7 at 0.02 (+ 0.00) seconds: ONE. % Length of proof is 10. % Level of proof is 3. % Maximum clause weight is 11.000. % Given clauses 8. 5 x v x' = y v y' # answer(ONE) # label(non_clause) # label(goal). [goal]. 9 f(f(x,x),f(x,y)) = x. [assumption]. 10 f(x,f(x,x)) = f(y,f(y,y)). [assumption]. 12 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 14 x' = f(x,x) # label(definition_complementation). [assumption]. 25 c10 v c10' != c9 v c9' # answer(ONE). [deny(5)]. 26 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(25),rewrite([14(3),12(5),9(10),14(8),12(10),9(15)])]. 33 f(x,f(x,x)) = c_0. [new_symbol(10)]. 59 f(f(x,x),x) = c_0. [para(9(a,1),33(a,1,2))]. 61 $F # answer(ONE). [back_rewrite(26),rewrite([59(5),59(6)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=8. Generated=118. Kept=38. proofs=7. Usable=7. Sos=21. Demods=16. Limbo=2, Disabled=22. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=75. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=18 (0 lex), Back_demodulated=3. Back_unit_deleted=0. Demod_attempts=1615. Demod_rewrites=159. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.09. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 5124 exit (max_proofs) Tue Nov 3 09:45:16 2009