============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13583 was started by mccune on cleo.thornwood, Mon Jun 19 16:43:06 2006 The command was "/home/mccune/bin/prover9 -f mol-ss1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mol-ss1.in assign(new_constants,1). clauses(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)). x ^ y = f(f(x,y),f(x,y)). c(x) = f(x,x). end_of_list. clauses(goals). x v (y v z) = y v (x v z) # answer(AJ). x v (x ^ y) = x # answer(B1). x ^ y = c(c(x) v c(y)) # answer(DM). c(c(x)) = x # answer(CC). x v c(x) = y v c(y) # answer(ONE). x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). f(x,y) = c(x) v c(y) # answer(DEF_SS). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). c4 v (c4 ^ c5) != c4 # answer(B1). c(c(c6) v c(c7)) != c6 ^ c7 # answer(DM). c(c(c8)) != c8 # answer(CC). c10 v c(c10) != c9 v c(c9) # answer(ONE). c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). f(c14,c15) != c(c14) v c(c15) # answer(DEF_SS). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [input]. 2 f(f(x,x),f(x,y)) = x. [input]. 3 f(x,f(x,x)) = f(y,f(y,y)). [input]. 4 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [input]. 5 x v y = f(f(x,x),f(y,y)). [input]. 6 x ^ y = f(f(x,y),f(x,y)). [input]. 7 c(x) = f(x,x). [input]. 8 c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [clausify]. 9 c4 v (c4 ^ c5) != c4 # answer(B1). [clausify]. 10 c(c(c6) v c(c7)) != c6 ^ c7 # answer(DM). [clausify]. 11 c(c(c8)) != c8 # answer(CC). [clausify]. 12 c10 v c(c10) != c9 v c(c9) # answer(ONE). [clausify]. 13 c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [clausify]. 14 f(c14,c15) != c(c14) v c(c15) # answer(DEF_SS). [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 c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [clausify]. 9 c4 v (c4 ^ c5) != c4 # answer(B1). [clausify]. 10 c(c(c6) v c(c7)) != c6 ^ c7 # answer(DM). [clausify]. 11 c(c(c8)) != c8 # answer(CC). [clausify]. 12 c10 v c(c10) != c9 v c(c9) # answer(ONE). [clausify]. 13 c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [clausify]. 14 f(c14,c15) != c(c14) v c(c15) # answer(DEF_SS). [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, f, ^, v, c ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, f, ^, v, c ]). Unfolding symbols: c/1 ^/2 v/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. NOTE: New constant: 0 f(x,f(x,x)) = c_0. [new_symbol(17)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c_0, f, ^, v, c ]). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: AJ. % Length of proof is 5. % Level of proof is 2. % Maximum clause weight is 19. % Given clauses 0. 8 c2 v (c1 v c3) != c1 v (c2 v c3) # answer(AJ). [clausify]. 15 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 23 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(8),demod(19(4),19(9),19(23),19(28)),flip(a)]. 24 $F # answer(AJ). [resolve(23,a,15,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 23. ============================== PROOF ================================= % Proof 2 at 0.00 (+ 0.00) seconds: B1. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 11. % Given clauses 0. 9 c4 v (c4 ^ c5) != c4 # answer(B1). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 20 x ^ y = f(f(x,y),f(x,y)). [input]. 25 $F # answer(B1). [copy(9),demod(20(4),19(9),16(18),16(7)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 3 at 0.00 (+ 0.00) seconds: DM. % Length of proof is 6. % Level of proof is 1. % Maximum clause weight is 11. % Given clauses 0. 10 c(c(c6) v c(c7)) != c6 ^ c7 # answer(DM). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 20 x ^ y = f(f(x,y),f(x,y)). [input]. 21 c(x) = f(x,x). [input]. 26 $F # answer(DM). [copy(10),demod(21(2),21(5),19(7),16(7),16(8),21(4),20(10)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 4 at 0.00 (+ 0.00) seconds: CC. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 9. % Given clauses 0. 11 c(c(c8)) != c8 # answer(CC). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 21 c(x) = f(x,x). [input]. 27 $F # answer(CC). [copy(11),demod(21(2),21(4),16(7)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 5 at 0.00 (+ 0.00) seconds: MOD. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 19. % Given clauses 0. 13 c11 v (c13 ^ (c11 v c12)) != c11 v (c12 ^ (c11 v c13)) # answer(MOD). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 18 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 20 x ^ y = f(f(x,y),f(x,y)). [input]. 29 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(13),demod(19(5),20(10),19(21),16(42),19(18),20(23),19(34),16(55)),flip(a)]. 30 $F # answer(MOD). [resolve(29,a,18,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 29. ============================== PROOF ================================= % Proof 6 at 0.00 (+ 0.00) seconds: DEF_SS. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 11. % Given clauses 0. 14 f(c14,c15) != c(c14) v c(c15) # answer(DEF_SS). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 21 c(x) = f(x,x). [input]. 31 $F # answer(DEF_SS). [copy(14),demod(21(5),21(8),19(10),16(10),16(11)),xx(a)]. ============================== end of proof ========================== ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 15 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [input]. 16 f(f(x,x),f(x,y)) = x. [input]. 18 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 20 x ^ y = f(f(x,y),f(x,y)). [input]. 21 c(x) = f(x,x). [input]. 22 f(x,f(x,x)) = c_0. [new_symbol(17)]. end_of_list. clauses(demodulators). 16 f(f(x,x),f(x,y)) = x. [input]. 19 x v y = f(f(x,x),f(y,y)). [input]. 20 x ^ y = f(f(x,y),f(x,y)). [input]. 21 c(x) = f(x,x). [input]. 22 f(x,f(x,x)) = c_0. [new_symbol(17)]. end_of_list. clauses(denials). 28 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(12),demod(21(3),19(5),16(10),21(8),19(10),16(15))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=19): 15 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). [input]. given #2 (I,wt=9): 16 f(f(x,x),f(x,y)) = x. [input]. given #3 (I,wt=19): 18 f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). [input]. given #4 (I,wt=11): 19 x v y = f(f(x,x),f(y,y)). [input]. given #5 (I,wt=11): 20 x ^ y = f(f(x,y),f(x,y)). [input]. given #6 (I,wt=6): 21 c(x) = f(x,x). [input]. given #7 (I,wt=7): 22 f(x,f(x,x)) = c_0. [new_symbol(17)]. ============================== PROOF ================================= % Proof 7 at 0.01 (+ 0.00) seconds: ONE. % Length of proof is 10. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 7. 3 f(x,f(x,x)) = f(y,f(y,y)). [input]. 12 c10 v c(c10) != c9 v c(c9) # answer(ONE). [clausify]. 16 f(f(x,x),f(x,y)) = x. [input]. 17 f(x,f(x,x)) = f(y,f(y,y)). [copy(3)]. 19 x v y = f(f(x,x),f(y,y)). [input]. 21 c(x) = f(x,x). [input]. 22 f(x,f(x,x)) = c_0. [new_symbol(17)]. 28 f(f(c10,c10),c10) != f(f(c9,c9),c9) # answer(ONE). [copy(12),demod(21(3),19(5),16(10),21(8),19(10),16(15))]. 57 f(f(x,x),x) = c_0. [para(16(a,1),22(a,1,2))]. 59 $F # answer(ONE). [back_demod(28),demod(57(5),57(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=7. Generated=124. Kept=36. proofs=7. Usable=7. Sos=21. Demods=16. Denials=0. Limbo=2, Disabled=20. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=81. 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=1573. Demod_rewrites=163. 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.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 13583 exit (max_proofs) Mon Jun 19 16:43:06 2006