Prover9 に（その３）
仮定が親切過ぎたかと思い
formulas(assumptions). all x all y all z (x <= y <-> (x < y | x = y)). all x all y all z (x < y & y < z -> x < z). all x -(x < x). end_of_list.
に変更しても，ご覧の通りです．
============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 2.84 (+ 0.14) seconds. % Length of proof is 63. % Level of proof is 25. % Maximum clause weight is 39. % Given clauses 1195. 1 (all x all y all z (x <= y <-> x < y | x = y)) # label(non_clause). [assumption]. 2 (all x all y all z (x < y & y < z -> x < z)) # label(non_clause). [assumption]. 3 (all x -(x < x)) # label(non_clause). [assumption]. 4 (exists M all m (SUC(N) * f(m) < N * f(SUC(m)) -> m < M)) & (all M exists L all m (m < M -> f(SUC(m)) <= L)) & (all L exists n (f(0) < N * pow(n) & L < SUC(N) * pow(n))) & (all n exists m N * pow(n) <= f(m)) & (all n (f(0) < N * pow(n) -> ((exists m N * pow(n) <= f(m)) -> ((all m -(N * pow(n) <= f(m) & f(m) < SUC(N) * pow(n))) -> (exists m (f(m) < N * pow(n) & SUC(N) * pow(n) <= f(SUC(m)))))))) & (all n all m (f(m) < N * pow(n) & SUC(N) * pow(n) <= f(SUC(m)) -> SUC(N) * f(m) < N * f(SUC(m)))) -> (exists n exists m (N * pow(n) <= f(m) & f(m) < SUC(N) * pow(n))) # label(non_clause) # label(goal). [goal]. 5 -(x <= y) | x < y | y = x. [clausify(1)]. 6 x <= y | -(x < y). [clausify(1)]. 7 x <= y | y != x. [clausify(1)]. 8 -(x < y) | -(y < z) | x < z. [clausify(2)]. 9 -(x < x). [clausify(3)]. 10 -(SUC(N) * f(x) < N * f(SUC(x))) | x < c1. [deny(4)]. 11 -(x < y) | f(SUC(x)) <= f1(y). [deny(4)]. 12 f(0) < N * pow(f2(x)). [deny(4)]. 13 x < SUC(N) * pow(f2(x)). [deny(4)]. 14 N * pow(x) <= f(f3(x)). [deny(4)]. 15 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [deny(4)]. 16 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [deny(4)]. 17 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [deny(4)]. 18 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | SUC(N) * pow(x) <= f(SUC(f5(x))). [deny(4)]. 19 -(f(x) < N * pow(y)) | -(SUC(N) * pow(y) <= f(SUC(x))) | SUC(N) * f(x) < N * f(SUC(x)). [deny(4)]. 20 -(N * pow(x) <= f(y)) | -(f(y) < SUC(N) * pow(x)). [deny(4)]. 30 -(SUC(N) * pow(f2(x)) < y) | x < y. [resolve(13,a,8,a)]. 32 -(SUC(N) * pow(f2(x)) < x). [ur(8,b,13,a,c,9,a)]. 34 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [resolve(15,b,14,a)]. 35 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(16,b,14,a)]. 36 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [resolve(17,b,14,a)]. 37 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(18,b,14,a)]. 96 N * pow(f2(x)) <= f(f4(f2(x))) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(34,a,12,a)]. 103 N * pow(f2(x)) <= f(f4(f2(x))) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(35,a,12,a)]. 117 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(36,a,12,a)]. 155 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(37,a,12,a)]. 166 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) < SUC(N) * pow(f2(x))). [resolve(96,a,20,a)]. 235 N * pow(f2(x)) <= f(f4(f2(x))) | SUC(N) * pow(f2(x)) < f(SUC(f5(f2(x)))) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)). [resolve(103,b,5,a)]. 287 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(f5(f2(x))) < N * pow(f2(x))) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(155,b,19,b)]. 288 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * pow(f2(x)) < f(SUC(f5(f2(x)))) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)). [resolve(155,b,5,a)]. 718 SUC(N) * pow(f2(x)) < f(SUC(f5(f2(x)))) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | -(f(f4(f2(x))) < SUC(N) * pow(f2(x))). [resolve(235,a,20,a)]. 869 SUC(N) * pow(f2(x)) < f(SUC(f5(f2(x)))) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)). [resolve(718,c,288,a),merge(c),merge(d)]. 898 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | x < f(SUC(f5(f2(x)))). [resolve(869,a,30,a)]. 903 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(869,a,6,b)]. 928 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) < y) | x < y. [resolve(898,b,8,a)]. 980 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | -(f(f5(f2(x))) < N * pow(f2(x))) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(903,b,19,b)]. 1204 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(287,b,117,b),merge(c)]. 1224 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f5(f2(x)) < c1. [resolve(1204,b,10,a)]. 1235 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) <= f1(c1). [resolve(1224,b,11,a)]. 1239 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) < f1(c1) | f(SUC(f5(f2(x)))) = f1(c1). [resolve(1235,b,5,a),flip(c)]. 1291 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) = f1(c1) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | x < f1(c1). [resolve(1239,b,928,b)]. 1620 f(SUC(f5(f2(x)))) = f1(c1) | f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | x < f1(c1) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(1291,a,166,b)]. 1912 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))) | f(SUC(f5(f2(x)))) = f1(c1) | x < f1(c1). [resolve(980,b,1620,d),merge(d)]. 2568 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) = f1(c1) | x < f1(c1) | f5(f2(x)) < c1. [resolve(1912,b,10,a)]. 2597 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) = f1(c1) | x < f1(c1) | f(SUC(f5(f2(x)))) <= f1(c1). [resolve(2568,d,11,a)]. 2606 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) = f1(c1) | x < f1(c1) | f(SUC(f5(f2(x)))) < f1(c1). [resolve(2597,d,5,a),flip(e),merge(e)]. 2630 f(SUC(f5(f2(x)))) = SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) = f1(c1) | x < f1(c1). [resolve(2606,d,928,b),merge(d),merge(e)]. 2722 f(SUC(f5(f2(f1(c1))))) = SUC(N) * pow(f2(f1(c1))) | f(SUC(f5(f2(f1(c1))))) = f1(c1). [resolve(2630,c,9,a)]. 2726 f(SUC(f5(f2(f1(c1))))) = f1(c1) | SUC(N) * pow(f2(f1(c1))) <= f(SUC(f5(f2(f1(c1))))). [resolve(2722,a,7,b)]. 2860 f(SUC(f5(f2(f1(c1))))) = f1(c1) | f(f4(f2(f1(c1)))) < SUC(N) * pow(f2(f1(c1))). [para(2722(a,1),1239(b,1)),merge(d),unit_del(c,32)]. 2973 f(SUC(f5(f2(f1(c1))))) = f1(c1) | f(f5(f2(f1(c1)))) < N * pow(f2(f1(c1))). [resolve(2860,b,166,b)]. 3008 f(SUC(f5(f2(f1(c1))))) = f1(c1) | -(f(f5(f2(f1(c1)))) < N * pow(f2(f1(c1)))) | SUC(N) * f(f5(f2(f1(c1)))) < N * f(SUC(f5(f2(f1(c1))))). [resolve(2726,b,19,b)]. 4301 f(SUC(f5(f2(f1(c1))))) = f1(c1) | SUC(N) * f(f5(f2(f1(c1)))) < N * f(SUC(f5(f2(f1(c1))))). [resolve(3008,b,2973,b),merge(c)]. 4317 f(SUC(f5(f2(f1(c1))))) = f1(c1) | f5(f2(f1(c1))) < c1. [resolve(4301,b,10,a)]. 4394 f(SUC(f5(f2(f1(c1))))) = f1(c1) | f(SUC(f5(f2(f1(c1))))) <= f1(c1). [resolve(4317,b,11,a)]. 4398 f(SUC(f5(f2(f1(c1))))) = f1(c1) | f(SUC(f5(f2(f1(c1))))) < f1(c1). [resolve(4394,b,5,a),flip(c),merge(c)]. 4442 f(SUC(f5(f2(f1(c1))))) = f1(c1). [para(2722(a,1),4398(b,1)),merge(b),unit_del(b,32)]. 4515 SUC(N) * pow(f2(f1(c1))) = f1(c1). [para(4442(a,1),869(a,2)),rewrite([4442(16)]),flip(b),unit_del(a,32)]. 4569 $F. [para(4515(a,1),13(a,2)),unit_del(a,9)]. ============================== end of proof ==========================
