============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27044 was started by mccune on cleo, Fri Apr 13 09:19:39 2007 The command was "/home/mccune/bin/prover9 -f mol-ss2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mol-ss2.in assign(max_seconds,30). assign(new_constants,1). formulas(sos). x v (y v z) = y v (x v z). x v (x ^ y) = x. x ^ y = (x' v y')'. x'' = x. x v x' = y v y'. x v (y ^ (x v z)) = x v (z ^ (x v y)). f(x,y) = x' v y' # label(definition_sheffer). end_of_list. formulas(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS). f(f(x,x),f(x,y)) = x # answer(B_SS). f(x,f(x,x)) = f(y,f(y,y)) # answer(ONE_SS). f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS). x v y = f(f(x,x),f(y,y)) # answer(DEF_J). x ^ y = f(f(x,y),f(x,y)) # answer(DEF_M). x' = f(x,x) # answer(DEF_C). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(goal). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(B_SS) # label(goal). [goal]. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(ONE_SS) # label(goal). [goal]. 4 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS) # label(goal). [goal]. 5 x v y = f(f(x,x),f(y,y)) # answer(DEF_J) # label(goal). [goal]. 6 x ^ y = f(f(x,y),f(x,y)) # answer(DEF_M) # label(goal). [goal]. 7 x' = f(x,x) # answer(DEF_C) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v (y v z) = y v (x v z). [assumption]. x v (x ^ y) = x. [assumption]. x ^ y = (x' v y')'. [assumption]. x'' = x. [assumption]. x v x' = y v y'. [assumption]. x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. f(x,y) = x' v y' # label(definition_sheffer). [assumption]. f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [deny(1)]. f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [deny(2)]. f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [deny(3)]. f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [deny(4)]. f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [deny(5)]. f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [deny(6)]. f(c15,c15) != c15' # answer(DEF_C). [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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, v, ^, f, ' ]). After inverse_order: (no changes). Unfolding symbols: ^/2 f/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). NOTE: New constant: x v x' = c_0. [new_symbol(12)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c_0, v, ^, f, ' ]). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 8 x v (y v z) = y v (x v z). [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 17 c1' v ((c2' v c3')' v (c2' v c3')')' != c2' v ((c1' v c3')' v (c1' v c3')')' # answer(A_SS). [copy(16),rewrite(15(4),15(9),15(12),15(15),15(21),15(26),15(29),15(32)),flip(a)]. 19 (c4' v c4')' v (c4' v c5')' != c4 # answer(B_SS). [copy(18),rewrite(15(3),15(8),15(11))]. 21 c7' v (c7' v c7')' != c6' v (c6' v c6')' # answer(ONE_SS). [copy(20),rewrite(15(4),15(7),15(13),15(16))]. 23 c8' v (c9' v (c8' v (c10' v c10')')')' != c8' v (c10' v (c8' v (c9' v c9')')')' # answer(MOD_SS). [copy(22),rewrite(15(6),15(9),15(12),15(15),15(23),15(26),15(29),15(32)),flip(a)]. 25 (c11' v c11')' v (c12' v c12')' != c11 v c12 # answer(DEF_J). [copy(24),rewrite(15(3),15(8),15(11))]. 27 (c13' v c14')' v (c13' v c14')' != (c13' v c14')' # answer(DEF_M). [copy(26),rewrite(15(3),15(8),15(11),10(16))]. 29 c15' v c15' != c15' # answer(DEF_C). [copy(28),rewrite(15(3))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 31 x v x' = c_0. [new_symbol(12)]. end_of_list. formulas(demodulators). 8 x v (y v z) = y v (x v z). [assumption]. % (lex-dep) 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 31 x v x' = c_0. [new_symbol(12)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 8 x v (y v z) = y v (x v z). [assumption]. given #2 (I,wt=10): 10 x ^ y = (x' v y')'. [assumption]. given #3 (I,wt=5): 11 x'' = x. [assumption]. given #4 (I,wt=21): 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. given #5 (I,wt=9): 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. given #6 (I,wt=35): 17 c1' v ((c2' v c3')' v (c2' v c3')')' != c2' v ((c1' v c3')' v (c1' v c3')')' # answer(A_SS). [copy(16),rewrite(15(4),15(9),15(12),15(15),15(21),15(26),15(29),15(32)),flip(a)]. given #7 (I,wt=15): 19 (c4' v c4')' v (c4' v c5')' != c4 # answer(B_SS). [copy(18),rewrite(15(3),15(8),15(11))]. given #8 (I,wt=19): 21 c7' v (c7' v c7')' != c6' v (c6' v c6')' # answer(ONE_SS). [copy(20),rewrite(15(4),15(7),15(13),15(16))]. given #9 (I,wt=35): 23 c8' v (c9' v (c8' v (c10' v c10')')')' != c8' v (c10' v (c8' v (c9' v c9')')')' # answer(MOD_SS). [copy(22),rewrite(15(6),15(9),15(12),15(15),15(23),15(26),15(29),15(32)),flip(a)]. given #10 (I,wt=17): 25 (c11' v c11')' v (c12' v c12')' != c11 v c12 # answer(DEF_J). [copy(24),rewrite(15(3),15(8),15(11))]. given #11 (I,wt=20): 27 (c13' v c14')' v (c13' v c14')' != (c13' v c14')' # answer(DEF_M). [copy(26),rewrite(15(3),15(8),15(11),10(16))]. given #12 (I,wt=8): 29 c15' v c15' != c15' # answer(DEF_C). [copy(28),rewrite(15(3))]. given #13 (I,wt=10): 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: DEF_C. % Length of proof is 13. % Level of proof is 4. % Maximum clause weight is 21. % Given clauses 13. 7 x' = f(x,x) # answer(DEF_C) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 28 f(c15,c15) != c15' # answer(DEF_C). [deny(7)]. 29 c15' v c15' != c15' # answer(DEF_C). [copy(28),rewrite(15(3))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 48 $F # answer(DEF_C). [resolve(47,a,29,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 2 at 0.00 (+ 0.00) seconds: DEF_M. % Length of proof is 13. % Level of proof is 4. % Maximum clause weight is 21. % Given clauses 13. 6 x ^ y = f(f(x,y),f(x,y)) # answer(DEF_M) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 26 f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [deny(6)]. 27 (c13' v c14')' v (c13' v c14')' != (c13' v c14')' # answer(DEF_M). [copy(26),rewrite(15(3),15(8),15(11),10(16))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 49 $F # answer(DEF_M). [resolve(47,a,27,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 3 at 0.00 (+ 0.00) seconds: MOD_SS. % Length of proof is 14. % Level of proof is 4. % Maximum clause weight is 35. % Given clauses 13. 4 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 22 f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [deny(4)]. 23 c8' v (c9' v (c8' v (c10' v c10')')')' != c8' v (c10' v (c8' v (c9' v c9')')')' # answer(MOD_SS). [copy(22),rewrite(15(6),15(9),15(12),15(15),15(23),15(26),15(29),15(32)),flip(a)]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 40 c8' v (c9' v (c8' v (c10' v c10')')')' != c8' v ((c9' v c9') v (c8' v c10)')' # answer(MOD_SS). [para(14(a,1),23(a,2)),rewrite(11(26))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 51 $F # answer(MOD_SS). [back_rewrite(40),rewrite(47(11),11(9),47(19)),xx(a)]. ============================== end of proof ========================== % Redundant proof: 52 $F # answer(MOD_SS). [back_rewrite(39),rewrite(47(11),11(9),47(19)),xx(a)]. % Redundant proof: 53 $F # answer(DEF_C). [back_rewrite(29),rewrite(47(5)),xx(a)]. % Redundant proof: 54 $F # answer(DEF_M). [back_rewrite(27),rewrite(47(13)),xx(a)]. ============================== PROOF ================================= % Proof 4 at 0.00 (+ 0.00) seconds: DEF_J. % Length of proof is 13. % Level of proof is 4. % Maximum clause weight is 21. % Given clauses 13. 5 x v y = f(f(x,x),f(y,y)) # answer(DEF_J) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 24 f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [deny(5)]. 25 (c11' v c11')' v (c12' v c12')' != c11 v c12 # answer(DEF_J). [copy(24),rewrite(15(3),15(8),15(11))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 55 $F # answer(DEF_J). [back_rewrite(25),rewrite(47(5),11(3),47(6),11(4)),xx(a)]. ============================== end of proof ========================== % Redundant proof: 57 $F # answer(MOD_SS). [resolve(56,a,14,a)]. % Redundant proof: 58 $F # answer(MOD_SS). [resolve(56,a,14,a(flip))]. ============================== PROOF ================================= % Proof 5 at 0.00 (+ 0.00) seconds: B_SS. % Length of proof is 14. % Level of proof is 4. % Maximum clause weight is 21. % Given clauses 13. 2 f(f(x,x),f(x,y)) = x # answer(B_SS) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 18 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [deny(2)]. 19 (c4' v c4')' v (c4' v c5')' != c4 # answer(B_SS). [copy(18),rewrite(15(3),15(8),15(11))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 44 x v (x' v y)' = x. [para(11(a,1),30(a,1,2,1,2))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 60 $F # answer(B_SS). [back_rewrite(19),rewrite(47(5),11(3),44(8)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 6 at 0.00 (+ 0.00) seconds: A_SS. % Length of proof is 14. % Level of proof is 4. % Maximum clause weight is 35. % Given clauses 13. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(goal). [goal]. 8 x v (y v z) = y v (x v z). [assumption]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 16 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [deny(1)]. 17 c1' v ((c2' v c3')' v (c2' v c3')')' != c2' v ((c1' v c3')' v (c1' v c3')')' # answer(A_SS). [copy(16),rewrite(15(4),15(9),15(12),15(15),15(21),15(26),15(29),15(32)),flip(a)]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 61 $F # answer(A_SS). [back_rewrite(17),rewrite(47(15),11(9),47(23),11(17),8(16)),xx(a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 16x 17x 18x 19x 24x 25x 22x 23x 39x 40x 56 26x 27x 28x 29x given #14 (I,wt=6): 31 x v x' = c_0. [new_symbol(12)]. ============================== PROOF ================================= % Proof 7 at 0.00 (+ 0.00) seconds: ONE_SS. % Length of proof is 17. % Level of proof is 5. % Maximum clause weight is 21. % Given clauses 14. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(ONE_SS) # label(goal). [goal]. 9 x v (x ^ y) = x. [assumption]. 10 x ^ y = (x' v y')'. [assumption]. 11 x'' = x. [assumption]. 12 x v x' = y v y'. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite(10(2),10(8))]. 15 f(x,y) = x' v y' # label(definition_sheffer). [assumption]. 20 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [deny(3)]. 21 c7' v (c7' v c7')' != c6' v (c6' v c6')' # answer(ONE_SS). [copy(20),rewrite(15(4),15(7),15(13),15(16))]. 30 x v (x' v y')' = x. [back_rewrite(9),rewrite(10(1))]. 31 x v x' = c_0. [new_symbol(12)]. 46 x v (y v (x v x)')' = x v x. [para(30(a,1),14(a,1,2,1)),rewrite(11(2),11(2),11(3),11(3),11(3)),flip(a)]. 47 x v x = x. [para(30(a,1),14(a,1)),rewrite(46(6)),flip(a)]. 59 c7' v c7 != c6' v c6 # answer(ONE_SS). [back_rewrite(21),rewrite(47(7),11(5),47(11),11(9))]. 65 x' v x = c_0. [para(11(a,1),31(a,1,2))]. 67 $F # answer(ONE_SS). [back_rewrite(59),rewrite(65(4),65(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=14. Generated=95. Kept=40. proofs=7. Usable=6. Sos=14. Demods=15. Limbo=2, Disabled=32. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=47. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=21 (1 lex), Back_demodulated=16. Back_unit_deleted=0. Demod_attempts=1484. Demod_rewrites=137. 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.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 27044 exit (max_proofs) Fri Apr 13 09:19:39 2007