============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11666 was started by mccune on cleo, Wed Feb 25 09:36:13 2009 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(non_clause) # label(goal). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(B_SS) # label(non_clause) # label(goal). [goal]. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(ONE_SS) # label(non_clause) # 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(non_clause) # label(goal). [goal]. 5 x v y = f(f(x,x),f(y,y)) # answer(DEF_J) # label(non_clause) # label(goal). [goal]. 6 x ^ y = f(f(x,y),f(x,y)) # answer(DEF_M) # label(non_clause) # label(goal). [goal]. 7 x' = f(x,x) # answer(DEF_C) # 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). 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: 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, v, ^, f, ' ]). After inverse_order: (no changes). Unfolding symbols: ^/2 f/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 8 x v (y v z) = y v (x v z). [assumption]. kept: 9 x v (x ^ y) = x. [assumption]. kept: 10 x ^ y = (x' v y')'. [assumption]. kept: 11 x'' = x. [assumption]. kept: 12 x v x' = y v y'. [assumption]. 13 x v (y ^ (x v z)) = x v (z ^ (x v y)). [assumption]. kept: 14 x v (y' v (x v z)')' = x v (z' v (x v y)')'. [copy(13),rewrite([10(2),10(8)])]. kept: 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)]. kept: 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)]. 18 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [deny(2)]. kept: 19 (c4' v c4')' v (c4' v c5')' != c4 # answer(B_SS). [copy(18),rewrite([15(3),15(8),15(11)])]. 20 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [deny(3)]. kept: 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)])]. 22 f(c8,f(c10,f(c8,f(c9,c9)))) != f(c8,f(c9,f(c8,f(c10,c10)))) # answer(MOD_SS). [deny(4)]. kept: 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)]. 24 f(f(c11,c11),f(c12,c12)) != c11 v c12 # answer(DEF_J). [deny(5)]. kept: 25 (c11' v c11')' v (c12' v c12')' != c11 v c12 # answer(DEF_J). [copy(24),rewrite([15(3),15(8),15(11)])]. 26 f(f(c13,c14),f(c13,c14)) != c13 ^ c14 # answer(DEF_M). [deny(6)]. kept: 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)])]. 28 f(c15,c15) != c15' # answer(DEF_C). [deny(7)]. kept: 29 c15' v c15' != c15' # answer(DEF_C). [copy(28),rewrite([15(3)])]. kept: 30 x v (x' v y')' = x. [back_rewrite(9),rewrite([10(1)])]. NOTE: New constant: x v x' = c_0. [new_symbol(12)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c_0, v, ^, f, ' ]). kept: 31 x v x' = c_0. [new_symbol(12)]. ============================== 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.01 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.01 (+ 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(non_clause) # 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.01 (+ 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(non_clause) # 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.01 (+ 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(non_clause) # 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.01 (+ 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(non_clause) # 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.02 (+ 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(non_clause) # 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.02 (+ 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(non_clause) # 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.02 (+ 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(non_clause) # 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=92. Kept=40. proofs=7. Usable=6. Sos=14. Demods=15. Limbo=2, Disabled=32. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=44. 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=1459. Demod_rewrites=135. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.10. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 11666 exit (max_proofs) Wed Feb 25 09:36:13 2009