============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13584 was started by mccune on cleo.thornwood, Mon Jun 19 16:43:06 2006 The command was "/home/mccune/bin/prover9 -f mol-ss2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mol-ss2.in assign(new_constants,1). clauses(sos). x v (y v z) = y v (x v z). x v (x ^ y) = x. x ^ y = c(c(x) v c(y)). c(c(x)) = x. x v c(x) = y v c(y). x v (y ^ (x v z)) = x v (z ^ (x v y)). f(x,y) = c(x) v c(y). end_of_list. clauses(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). c(x) = f(x,x) # answer(DEF_C). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). f(c15,c15) != c(c15) # answer(DEF_C). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v (y v z) = y v (x v z). [input]. 2 x v (x ^ y) = x. [input]. 3 x ^ y = c(c(x) v c(y)). [input]. 4 c(c(x)) = x. [input]. 5 x v c(x) = y v c(y). [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 7 f(x,y) = c(x) v c(y). [input]. 8 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 9 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 10 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [clausify]. 11 f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [clausify]. 12 f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [clausify]. 13 f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [clausify]. 14 f(c15,c15) != c(c15) # answer(DEF_C). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 7). % (Horn set with more than one neg. clause) % assign(max_proofs, 7) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 8 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 9 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 10 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [clausify]. 11 f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [clausify]. 12 f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [clausify]. 13 f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [clausify]. 14 f(c15,c15) != c(c15) # answer(DEF_C). [clausify]. end_of_list. 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, c ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, v, ^, f, c ]). 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: 0 x v c(x) = c_0. [new_symbol(19)]. 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, c ]). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 15 x v (y v z) = y v (x v z). [input]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 23 x v c(x) = c_0. [new_symbol(19)]. end_of_list. clauses(demodulators). 15 x v (y v z) = y v (x v z). [input]. % (lex-dep) 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 23 x v c(x) = c_0. [new_symbol(19)]. end_of_list. clauses(denials). 24 c(c1) v c(c(c(c2) v c(c3)) v c(c(c2) v c(c3))) != c(c2) v c(c(c(c1) v c(c3)) v c(c(c1) v c(c3))) # answer(A_SS). [copy(8),demod(21(4),21(9),21(12),21(15),21(21),21(26),21(29),21(32)),flip(a)]. 25 c(c(c4) v c(c4)) v c(c(c4) v c(c5)) != c4 # answer(B_SS). [copy(9),demod(21(3),21(8),21(11))]. 26 c(c7) v c(c(c7) v c(c7)) != c(c6) v c(c(c6) v c(c6)) # answer(ONE_SS). [copy(10),demod(21(4),21(7),21(13),21(16))]. 27 c(c8) v c(c(c9) v c(c(c8) v c(c(c10) v c(c10)))) != c(c8) v c(c(c10) v c(c(c8) v c(c(c9) v c(c9)))) # answer(MOD_SS). [copy(11),demod(21(6),21(9),21(12),21(15),21(23),21(26),21(29),21(32)),flip(a)]. 28 c(c(c11) v c(c11)) v c(c(c12) v c(c12)) != c11 v c12 # answer(DEF_J). [copy(12),demod(21(3),21(8),21(11))]. 29 c(c(c13) v c(c14)) v c(c(c13) v c(c14)) != c(c(c13) v c(c14)) # answer(DEF_M). [copy(13),demod(21(3),21(8),21(11),17(16))]. 30 c(c15) v c(c15) != c(c15) # answer(DEF_C). [copy(14),demod(21(3))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 15 x v (y v z) = y v (x v z). [input]. given #2 (I,wt=10): 17 x ^ y = c(c(x) v c(y)). [input]. given #3 (I,wt=5): 18 c(c(x)) = x. [input]. given #4 (I,wt=21): 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. given #5 (I,wt=9): 21 f(x,y) = c(x) v c(y). [input]. given #6 (I,wt=10): 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: DEF_C. % Length of proof is 13. % Level of proof is 5. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 14 f(c15,c15) != c(c15) # answer(DEF_C). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 30 c(c15) v c(c15) != c(c15) # answer(DEF_C). [copy(14),demod(21(3))]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 45 $F # answer(DEF_C). [resolve(44,a,30,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 30. ============================== PROOF ================================= % Proof 2 at 0.00 (+ 0.00) seconds: DEF_M. % Length of proof is 13. % Level of proof is 5. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 13 f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 29 c(c(c13) v c(c14)) v c(c(c13) v c(c14)) != c(c(c13) v c(c14)) # answer(DEF_M). [copy(13),demod(21(3),21(8),21(11),17(16))]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 46 $F # answer(DEF_M). [resolve(44,a,29,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 29. ============================== PROOF ================================= % Proof 3 at 0.00 (+ 0.00) seconds: DEF_J. % Length of proof is 13. % Level of proof is 5. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 12 f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 28 c(c(c11) v c(c11)) v c(c(c12) v c(c12)) != c11 v c12 # answer(DEF_J). [copy(12),demod(21(3),21(8),21(11))]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 48 $F # answer(DEF_J). [back_demod(28),demod(44(5),18(3),44(6),18(4)),xx(a)]. ============================== end of proof ========================== uncompressing unused clause ============================== PROOF ================================= % Proof 4 at 0.00 (+ 0.00) seconds: MOD_SS. % Length of proof is 14. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 11 f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 27 c(c8) v c(c(c9) v c(c(c8) v c(c(c10) v c(c10)))) != c(c8) v c(c(c10) v c(c(c8) v c(c(c9) v c(c9)))) # answer(MOD_SS). [copy(11),demod(21(6),21(9),21(12),21(15),21(23),21(26),21(29),21(32)),flip(a)]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 49 c(c8) v c(c(c9) v c(c(c8) v c10)) != c(c8) v c(c(c10) v c(c(c8) v c9)) # answer(MOD_SS). [back_demod(27),demod(44(11),18(9),44(23),18(21))]. 50 $F # answer(MOD_SS). [resolve(49,a,20,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 49. ============================== PROOF ================================= % Proof 5 at 0.00 (+ 0.00) seconds: B_SS. % Length of proof is 14. % Level of proof is 5. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 9 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 25 c(c(c4) v c(c4)) v c(c(c4) v c(c5)) != c4 # answer(B_SS). [copy(9),demod(21(3),21(8),21(11))]. 41 x v c(c(x) v y) = x. [para(18(a,1),22(a,1,2,1,2))]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 52 $F # answer(B_SS). [back_demod(25),demod(44(5),18(3),41(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 5. % Maximum clause weight is 21. % Given clauses 6. 2 x v (x ^ y) = x. [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 8 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 15 x v (y v z) = y v (x v z). [input]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 24 c(c1) v c(c(c(c2) v c(c3)) v c(c(c2) v c(c3))) != c(c2) v c(c(c(c1) v c(c3)) v c(c(c1) v c(c3))) # answer(A_SS). [copy(8),demod(21(4),21(9),21(12),21(15),21(21),21(26),21(29),21(32)),flip(a)]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 53 $F # answer(A_SS). [back_demod(24),demod(44(15),18(9),44(23),18(17),15(16)),xx(a)]. ============================== end of proof ========================== given #7 (I,wt=6): 23 x v c(x) = c_0. [new_symbol(19)]. ============================== PROOF ================================= % Proof 7 at 0.00 (+ 0.00) seconds: ONE_SS. % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 7. 2 x v (x ^ y) = x. [input]. 5 x v c(x) = y v c(y). [input]. 6 x v (y ^ (x v z)) = x v (z ^ (x v y)). [input]. 10 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [clausify]. 16 x v (x ^ y) = x. [copy(2)]. 17 x ^ y = c(c(x) v c(y)). [input]. 18 c(c(x)) = x. [input]. 19 x v c(x) = y v c(y). [copy(5)]. 20 x v c(c(y) v c(x v z)) = x v c(c(z) v c(x v y)). [copy(6),demod(17(2),17(8))]. 21 f(x,y) = c(x) v c(y). [input]. 22 x v c(c(x) v c(y)) = x. [back_demod(16),demod(17(1))]. 23 x v c(x) = c_0. [new_symbol(19)]. 26 c(c7) v c(c(c7) v c(c7)) != c(c6) v c(c(c6) v c(c6)) # answer(ONE_SS). [copy(10),demod(21(4),21(7),21(13),21(16))]. 43 x v c(y v c(x v x)) = x v x. [para(22(a,1),20(a,1,2,1)),demod(18(2),18(2),18(3),18(3),18(3)),flip(a)]. 44 x v x = x. [para(22(a,1),20(a,1)),demod(43(6)),flip(a)]. 51 c(c7) v c7 != c(c6) v c6 # answer(ONE_SS). [back_demod(26),demod(44(7),18(5),44(11),18(9))]. 57 c(x) v x = c_0. [para(18(a,1),23(a,1,2))]. 59 $F # answer(ONE_SS). [back_demod(51),demod(57(4),57(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=7. Generated=89. Kept=37. proofs=7. Usable=6. Sos=14. Demods=15. Denials=0. Limbo=2, Disabled=29. 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=12. Back_unit_deleted=0. Demod_attempts=1136. Demod_rewrites=127. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.08. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 13584 exit (max_proofs) Mon Jun 19 16:43:06 2006