Prover9 に（その２）
前回の最後に MESON が証明した定理式を Prover9 に与えると．．．
瞬時に以下のように証明してくれます．
============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. ============================== end of head =========================== ============================== INPUT ================================= assign(report_stderr,2). set(ignore_option_dependencies). if(Prover9). % Conditional input included. assign(max_seconds,60). end_if. if(Mace4). % Conditional input omitted. end_if. formulas(assumptions). (all a all L all x all y (a <= L & L < x & x < y & y <= a -> $F)). end_of_list. formulas(goals). (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 < N * pow(n))) & (all n exists m N * pow(n) <= f(m)) & (all n N * pow(n) < SUC(N) * pow(n)) & (all n (N * pow(n) < SUC(N) * pow(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))). end_of_list. ============================== end of input ========================== % Enabling option dependencies (ignore applies only on input). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all a all L all x all y (a <= L & L < x & x < y & y <= a -> $F)) # label(non_clause). [assumption]. 2 (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 < N * pow(n))) & (all n exists m N * pow(n) <= f(m)) & (all n N * pow(n) < SUC(N) * pow(n)) & (all n (N * pow(n) < SUC(N) * pow(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]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -(x <= y) | -(y < z) | -(z < u) | -(u <= x). [clausify(1)]. -(SUC(N) * f(x) < N * f(SUC(x))) | x <= c1. [deny(2)]. -(x <= y) | f(SUC(x)) <= f1(y). [deny(2)]. f(0) < N * pow(f2(x)). [deny(2)]. x < N * pow(f2(x)). [deny(2)]. N * pow(x) <= f(f3(x)). [deny(2)]. N * pow(x) < SUC(N) * pow(x). [deny(2)]. -(N * pow(x) < SUC(N) * pow(x)) | -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [deny(2)]. -(N * pow(x) < SUC(N) * pow(x)) | -(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(2)]. -(N * pow(x) < SUC(N) * pow(x)) | -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [deny(2)]. -(N * pow(x) < SUC(N) * pow(x)) | -(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(2)]. -(f(x) < N * pow(y)) | -(SUC(N) * pow(y) <= f(SUC(x))) | SUC(N) * f(x) < N * f(SUC(x)). [deny(2)]. -(N * pow(x) <= f(y)) | -(f(y) < SUC(N) * pow(x)). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ <, <= ]). Function symbol precedence: function_order([ N, 0, c1, *, pow, f, SUC, f1, f2, f3, f4, f5 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 -(x <= y) | -(y < z) | -(z < u) | -(u <= x). [clausify(1)]. 4 -(SUC(N) * f(x) < N * f(SUC(x))) | x <= c1. [deny(2)]. 5 -(x <= y) | f(SUC(x)) <= f1(y). [deny(2)]. 6 f(0) < N * pow(f2(x)). [deny(2)]. 7 x < N * pow(f2(x)). [deny(2)]. 8 N * pow(x) <= f(f3(x)). [deny(2)]. 9 N * pow(x) < SUC(N) * pow(x). [deny(2)]. 11 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [copy(10),unit_del(a,9)]. 13 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [copy(12),unit_del(a,9)]. 15 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [copy(14),unit_del(a,9)]. 17 -(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))). [copy(16),unit_del(a,9)]. 18 -(f(x) < N * pow(y)) | -(SUC(N) * pow(y) <= f(SUC(x))) | SUC(N) * f(x) < N * f(SUC(x)). [deny(2)]. 19 -(N * pow(x) <= f(y)) | -(f(y) < SUC(N) * pow(x)). [deny(2)]. 20 -(x <= x) | -(x < y) | -(y < x). [factor(3,a,d)]. 21 -(x <= y) | -(y < y) | -(y <= x). [factor(3,b,c)]. 22 -(x <= x) | -(x < x). [factor(20,b,c)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=12): 3 -(x <= y) | -(y < z) | -(z < u) | -(u <= x). [clausify(1)]. given #2 (I,wt=14): 4 -(SUC(N) * f(x) < N * f(SUC(x))) | x <= c1. [deny(2)]. given #3 (I,wt=9): 5 -(x <= y) | f(SUC(x)) <= f1(y). [deny(2)]. given #4 (I,wt=8): 6 f(0) < N * pow(f2(x)). [deny(2)]. given #5 (I,wt=7): 7 x < N * pow(f2(x)). [deny(2)]. given #6 (I,wt=8): 8 N * pow(x) <= f(f3(x)). [deny(2)]. given #7 (I,wt=10): 9 N * pow(x) < SUC(N) * pow(x). [deny(2)]. given #8 (I,wt=30): 11 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [copy(10),unit_del(a,9)]. given #9 (I,wt=32): 13 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [copy(12),unit_del(a,9)]. given #10 (I,wt=31): 15 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [copy(14),unit_del(a,9)]. given #11 (I,wt=33): 17 -(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))). [copy(16),unit_del(a,9)]. given #12 (I,wt=27): 18 -(f(x) < N * pow(y)) | -(SUC(N) * pow(y) <= f(SUC(x))) | SUC(N) * f(x) < N * f(SUC(x)). [deny(2)]. given #13 (I,wt=15): 19 -(N * pow(x) <= f(y)) | -(f(y) < SUC(N) * pow(x)). [deny(2)]. given #14 (I,wt=9): 20 -(x <= x) | -(x < y) | -(y < x). [factor(3,a,d)]. given #15 (I,wt=9): 21 -(x <= y) | -(y < y) | -(y <= x). [factor(3,b,c)]. given #16 (I,wt=6): 22 -(x <= x) | -(x < x). [factor(20,b,c)]. given #17 (A,wt=11): 23 f(SUC(N * pow(x))) <= f1(f(f3(x))). [resolve(8,a,5,a)]. given #18 (F,wt=9): 37 -(f(f3(x)) < SUC(N) * pow(x)). [resolve(19,a,8,a)]. given #19 (F,wt=10): 26 -(f(f3(f2(N * pow(f2(x))))) <= x). [ur(3,b,7,a,c,7,a,d,8,a)]. given #20 (F,wt=11): 27 -(f(f3(f2(N * pow(f2(x))))) <= f(0)). [ur(3,b,6,a,c,7,a,d,8,a)]. given #21 (F,wt=13): 31 -(SUC(N) * pow(f2(f(f3(x)))) <= N * pow(x)). [ur(3,a,8,a,b,7,a,c,9,a)]. given #22 (T,wt=14): 40 f(SUC(f(SUC(N * pow(x))))) <= f1(f1(f(f3(x)))). [resolve(23,a,5,a)]. given #23 (T,wt=17): 48 f(SUC(f(SUC(f(SUC(N * pow(x))))))) <= f1(f1(f1(f(f3(x))))). [resolve(40,a,5,a)]. given #24 (T,wt=20): 55 f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))) <= f1(f1(f1(f1(f(f3(x)))))). [resolve(48,a,5,a)]. given #25 (T,wt=23): 33 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [resolve(11,b,8,a)]. given #26 (A,wt=14): 24 -(f(f3(x)) <= y) | -(y < z) | -(z < N * pow(x)). [resolve(8,a,3,d)]. given #27 (F,wt=13): 32 -(f(f3(f2(SUC(N) * pow(x)))) <= N * pow(x)). [ur(3,b,9,a,c,7,a,d,8,a)]. given #28 (F,wt=14): 25 -(f(f3(x)) < y) | -(y < z) | -(z <= N * pow(x)). [resolve(8,a,3,a)]. given #29 (F,wt=15): 30 -(f(f3(x)) < f(f3(x))) | -(f(f3(x)) <= N * pow(x)). [factor(25,a,b)]. given #30 (F,wt=16): 28 -(N * pow(f2(N * pow(f2(f(f3(x)))))) <= N * pow(x)). [ur(3,a,8,a,b,7,a,c,7,a)]. given #31 (T,wt=20): 68 N * pow(f2(x)) <= f(f4(f2(x))) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(33,a,6,a)]. given #32 (T,wt=21): 71 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) < SUC(N) * pow(f2(x))). [resolve(68,a,19,a)]. given #33 (T,wt=23): 62 f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))) <= f1(f1(f1(f1(f1(f(f3(x))))))). [resolve(55,a,5,a)]. given #34 (T,wt=23): 72 f(f5(f2(x))) < N * pow(f2(x)) | f(SUC(N * pow(f2(x)))) <= f1(f(f4(f2(x)))). [resolve(68,a,5,a)]. given #35 (A,wt=17): 29 -(f(f3(x)) <= N * pow(x)) | -(N * pow(x) < N * pow(x)). [factor(24,b,c)]. given #36 (F,wt=16): 43 -(SUC(N) * pow(f2(f1(f(f3(x))))) <= f(SUC(N * pow(x)))). [ur(3,a,23,a,b,7,a,c,9,a)]. given #37 (F,wt=17): 41 -(f1(f(f3(x))) <= y) | -(y < z) | -(z < f(SUC(N * pow(x)))). [resolve(23,a,3,d)]. given #38 (F,wt=17): 42 -(f1(f(f3(x))) < y) | -(y < z) | -(z <= f(SUC(N * pow(x)))). [resolve(23,a,3,a)]. given #39 (F,wt=19): 44 -(N * pow(f2(N * pow(f2(f1(f(f3(x))))))) <= f(SUC(N * pow(x)))). [ur(3,a,23,a,b,7,a,c,7,a)]. given #40 (T,wt=24): 35 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [resolve(15,b,8,a)]. given #41 (T,wt=21): 88 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(35,a,6,a)]. given #42 (T,wt=25): 34 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(13,b,8,a)]. given #43 (T,wt=22): 90 N * pow(f2(x)) <= f(f4(f2(x))) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(34,a,6,a)]. given #44 (A,wt=26): 36 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(17,b,8,a)]. given #45 (F,wt=19): 51 -(SUC(N) * pow(f2(f1(f1(f(f3(x)))))) <= f(SUC(f(SUC(N * pow(x)))))). [ur(3,a,40,a,b,7,a,c,9,a)]. given #46 (F,wt=20): 39 -(f1(f(f3(x))) < f1(f(f3(x)))) | -(f1(f(f3(x))) <= f(SUC(N * pow(x)))). [resolve(23,a,21,a)]. given #47 (F,wt=20): 49 -(f1(f1(f(f3(x)))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(N * pow(x)))))). [resolve(40,a,3,d)]. given #48 (F,wt=20): 50 -(f1(f1(f(f3(x)))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(N * pow(x)))))). [resolve(40,a,3,a)]. given #49 (T,wt=23): 98 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(36,a,6,a)]. given #50 (T,wt=25): 94 N * pow(f2(x)) <= f(f4(f2(x))) | f(SUC(SUC(N) * pow(f2(x)))) <= f1(f(SUC(f5(f2(x))))). [resolve(90,b,5,a)]. given #51 (T,wt=26): 73 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) <= y) | -(y < z) | -(z < N * pow(f2(x))). [resolve(68,a,3,d)]. given #52 (T,wt=26): 74 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) < y) | -(y < z) | -(z <= N * pow(f2(x))). [resolve(68,a,3,a)]. given #53 (A,wt=24): 38 -(f1(f(f3(x))) <= f(SUC(N * pow(x)))) | -(f(SUC(N * pow(x))) < f(SUC(N * pow(x)))). [resolve(23,a,21,c)]. given #54 (F,wt=22): 52 -(N * pow(f2(N * pow(f2(f1(f1(f(f3(x)))))))) <= f(SUC(f(SUC(N * pow(x)))))). [ur(3,a,40,a,b,7,a,c,7,a)]. given #55 (F,wt=22): 58 -(SUC(N) * pow(f2(f1(f1(f1(f(f3(x))))))) <= f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [ur(3,a,48,a,b,7,a,c,9,a)]. given #56 (F,wt=23): 56 -(f1(f1(f1(f(f3(x))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [resolve(48,a,3,d)]. given #57 (F,wt=23): 57 -(f1(f1(f1(f(f3(x))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [resolve(48,a,3,a)]. given #58 (T,wt=26): 77 f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))) <= f1(f1(f1(f1(f1(f1(f(f3(x)))))))). [resolve(62,a,5,a)]. given #59 (T,wt=26): 84 f(f5(f2(x))) < N * pow(f2(x)) | f(SUC(f(SUC(N * pow(f2(x)))))) <= f1(f1(f(f4(f2(x))))). [resolve(72,b,5,a)]. given #60 (T,wt=26): 102 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(SUC(N) * pow(f2(x)))) <= f1(f(SUC(f5(f2(x))))). [resolve(98,b,5,a)]. given #61 (T,wt=28): 95 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(SUC(f5(f2(x)))) <= y) | -(y < z) | -(z < SUC(N) * pow(f2(x))). [resolve(90,b,3,d)]. given #62 (A,wt=25): 45 -(SUC(N) * f(f(f3(f2(N * pow(f2(c1)))))) < N * f(SUC(f(f3(f2(N * pow(f2(c1)))))))). [ur(4,b,26,a)]. given #63 (F,wt=25): 47 -(f1(f1(f(f3(x)))) < f1(f1(f(f3(x))))) | -(f1(f1(f(f3(x)))) <= f(SUC(f(SUC(N * pow(x)))))). [resolve(40,a,21,a)]. given #64 (F,wt=25): 59 -(N * pow(f2(N * pow(f2(f1(f1(f1(f(f3(x))))))))) <= f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [ur(3,a,48,a,b,7,a,c,7,a)]. given #65 (F,wt=25): 65 -(SUC(N) * pow(f2(f1(f1(f1(f1(f(f3(x)))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [ur(3,a,55,a,b,7,a,c,9,a)]. given #66 (F,wt=25): 127 -(SUC(N) * pow(f2(f(f(f3(f2(N * pow(f2(c1)))))))) <= f(SUC(f(f3(f2(N * pow(f2(c1)))))))). [ur(18,a,7,a,c,45,a)]. given #67 (T,wt=28): 96 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(SUC(f5(f2(x)))) < y) | -(y < z) | -(z <= SUC(N) * pow(f2(x))). [resolve(90,b,3,a)]. given #68 (T,wt=28): 107 N * pow(f2(x)) <= f(f4(f2(x))) | f(SUC(f(SUC(SUC(N) * pow(f2(x)))))) <= f1(f1(f(SUC(f5(f2(x)))))). [resolve(94,b,5,a)]. given #69 (T,wt=29): 70 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) < f(f4(f2(x)))) | -(f(f4(f2(x))) <= N * pow(f2(x))). [resolve(68,a,21,a)]. given #70 (T,wt=29): 85 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f(f4(f2(x)))) <= y) | -(y < z) | -(z < f(SUC(N * pow(f2(x))))). [resolve(72,b,3,d)]. given #71 (A,wt=31): 46 -(f1(f1(f(f3(x)))) <= f(SUC(f(SUC(N * pow(x)))))) | -(f(SUC(f(SUC(N * pow(x))))) < f(SUC(f(SUC(N * pow(x)))))). [resolve(40,a,21,c)]. given #72 (F,wt=26): 63 -(f1(f1(f1(f1(f(f3(x)))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [resolve(55,a,3,d)]. given #73 (F,wt=26): 64 -(f1(f1(f1(f1(f(f3(x)))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [resolve(55,a,3,a)]. given #74 (F,wt=28): 66 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f(f3(x)))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [ur(3,a,55,a,b,7,a,c,7,a)]. given #75 (F,wt=28): 80 -(SUC(N) * pow(f2(f1(f1(f1(f1(f1(f(f3(x))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [ur(3,a,62,a,b,7,a,c,9,a)]. given #76 (T,wt=29): 86 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f(f4(f2(x)))) < y) | -(y < z) | -(z <= f(SUC(N * pow(f2(x))))). [resolve(72,b,3,a)]. given #77 (T,wt=29): 103 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) <= y) | -(y < z) | -(z < SUC(N) * pow(f2(x))). [resolve(98,b,3,d)]. given #78 (T,wt=29): 104 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) < y) | -(y < z) | -(z <= SUC(N) * pow(f2(x))). [resolve(98,b,3,a)]. given #79 (T,wt=29): 112 f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))) <= f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))). [resolve(77,a,5,a)]. given #80 (A,wt=38): 53 -(f1(f1(f1(f(f3(x))))) <= f(SUC(f(SUC(f(SUC(N * pow(x)))))))) | -(f(SUC(f(SUC(f(SUC(N * pow(x))))))) < f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [resolve(48,a,21,c)]. given #81 (F,wt=29): 78 -(f1(f1(f1(f1(f1(f(f3(x))))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [resolve(62,a,3,d)]. given #82 (F,wt=29): 79 -(f1(f1(f1(f1(f1(f(f3(x))))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [resolve(62,a,3,a)]. given #83 (F,wt=30): 54 -(f1(f1(f1(f(f3(x))))) < f1(f1(f1(f(f3(x)))))) | -(f1(f1(f1(f(f3(x))))) <= f(SUC(f(SUC(f(SUC(N * pow(x)))))))). [resolve(48,a,21,a)]. given #84 (F,wt=31): 81 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f1(f(f3(x))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [ur(3,a,62,a,b,7,a,c,7,a)]. given #85 (T,wt=29): 119 f(f5(f2(x))) < N * pow(f2(x)) | f(SUC(f(SUC(f(SUC(N * pow(f2(x)))))))) <= f1(f1(f1(f(f4(f2(x)))))). [resolve(84,b,5,a)]. given #86 (T,wt=29): 124 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f(SUC(SUC(N) * pow(f2(x)))))) <= f1(f1(f(SUC(f5(f2(x)))))). [resolve(102,b,5,a)]. given #87 (T,wt=31): 69 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) <= N * pow(f2(x))) | -(N * pow(f2(x)) < N * pow(f2(x))). [resolve(68,a,21,c)]. given #88 (T,wt=31): 108 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f(SUC(f5(f2(x))))) <= y) | -(y < z) | -(z < f(SUC(SUC(N) * pow(f2(x))))). [resolve(94,b,3,d)]. given #89 (A,wt=45): 60 -(f1(f1(f1(f1(f(f3(x)))))) <= f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [resolve(55,a,21,c)]. given #90 (F,wt=31): 115 -(SUC(N) * pow(f2(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [ur(3,a,77,a,b,7,a,c,9,a)]. given #91 (F,wt=32): 113 -(f1(f1(f1(f1(f1(f1(f(f3(x)))))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [resolve(77,a,3,d)]. given #92 (F,wt=32): 114 -(f1(f1(f1(f1(f1(f1(f(f3(x)))))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [resolve(77,a,3,a)]. given #93 (F,wt=34): 116 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [ur(3,a,77,a,b,7,a,c,7,a)]. given #94 (T,wt=31): 109 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f(SUC(f5(f2(x))))) < y) | -(y < z) | -(z <= f(SUC(SUC(N) * pow(f2(x))))). [resolve(94,b,3,a)]. given #95 (T,wt=31): 130 N * pow(f2(x)) <= f(f4(f2(x))) | f(SUC(f(SUC(f(SUC(SUC(N) * pow(f2(x)))))))) <= f1(f1(f1(f(SUC(f5(f2(x))))))). [resolve(107,b,5,a)]. given #96 (T,wt=32): 120 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f(f4(f2(x))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(N * pow(f2(x))))))). [resolve(84,b,3,d)]. given #97 (T,wt=32): 121 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f(f4(f2(x))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(N * pow(f2(x))))))). [resolve(84,b,3,a)]. given #98 (A,wt=35): 61 -(f1(f1(f1(f1(f(f3(x)))))) < f1(f1(f1(f1(f(f3(x))))))) | -(f1(f1(f1(f1(f(f3(x)))))) <= f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))). [resolve(55,a,21,a)]. given #99 (F,wt=34): 138 -(SUC(N) * pow(f2(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [ur(3,a,112,a,b,7,a,c,9,a)]. given #100 (F,wt=35): 136 -(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [resolve(112,a,3,d)]. given #101 (F,wt=35): 137 -(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [resolve(112,a,3,a)]. given #102 (F,wt=37): 139 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [ur(3,a,112,a,b,7,a,c,7,a)]. given #103 (T,wt=32): 125 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(f(SUC(f5(f2(x))))) <= y) | -(y < z) | -(z < f(SUC(SUC(N) * pow(f2(x))))). [resolve(102,b,3,d)]. given #104 (T,wt=32): 126 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(f(SUC(f5(f2(x))))) < y) | -(y < z) | -(z <= f(SUC(SUC(N) * pow(f2(x))))). [resolve(102,b,3,a)]. given #105 (T,wt=32): 135 f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))))) <= f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))). [resolve(112,a,5,a)]. given #106 (T,wt=32): 142 f(f5(f2(x))) < N * pow(f2(x)) | f(SUC(f(SUC(f(SUC(f(SUC(N * pow(f2(x)))))))))) <= f1(f1(f1(f1(f(f4(f2(x))))))). [resolve(119,b,5,a)]. given #107 (A,wt=52): 75 -(f1(f1(f1(f1(f1(f(f3(x))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [resolve(62,a,21,c)]. given #108 (F,wt=37): 160 -(SUC(N) * pow(f2(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [ur(3,a,135,a,b,7,a,c,9,a)]. given #109 (F,wt=38): 158 -(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [resolve(135,a,3,d)]. given #110 (F,wt=38): 159 -(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [resolve(135,a,3,a)]. given #111 (F,wt=40): 76 -(f1(f1(f1(f1(f1(f(f3(x))))))) < f1(f1(f1(f1(f1(f(f3(x)))))))) | -(f1(f1(f1(f1(f1(f(f3(x))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))). [resolve(62,a,21,a)]. given #112 (T,wt=32): 147 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f(SUC(f(SUC(SUC(N) * pow(f2(x)))))))) <= f1(f1(f1(f(SUC(f5(f2(x))))))). [resolve(124,b,5,a)]. given #113 (T,wt=33): 92 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(SUC(f5(f2(x)))) < f(SUC(f5(f2(x))))) | -(f(SUC(f5(f2(x)))) <= SUC(N) * pow(f2(x))). [resolve(90,b,21,a)]. given #114 (T,wt=34): 83 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f(f4(f2(x)))) < f1(f(f4(f2(x))))) | -(f1(f(f4(f2(x)))) <= f(SUC(N * pow(f2(x))))). [resolve(72,b,21,a)]. given #115 (T,wt=34): 100 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) < f(SUC(f5(f2(x))))) | -(f(SUC(f5(f2(x)))) <= SUC(N) * pow(f2(x))). [resolve(98,b,21,a)]. given #116 (A,wt=38): 82 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f(f4(f2(x)))) <= f(SUC(N * pow(f2(x))))) | -(f(SUC(N * pow(f2(x)))) < f(SUC(N * pow(f2(x))))). [resolve(72,b,21,c)]. given #117 (F,wt=40): 161 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [ur(3,a,135,a,b,7,a,c,7,a)]. given #118 (F,wt=45): 111 -(f1(f1(f1(f1(f1(f1(f(f3(x)))))))) < f1(f1(f1(f1(f1(f1(f(f3(x))))))))) | -(f1(f1(f1(f1(f1(f1(f(f3(x)))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [resolve(77,a,21,a)]. given #119 (F,wt=50): 134 -(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))) < f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) | -(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [resolve(112,a,21,a)]. given #120 (F,wt=55): 156 -(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) < f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) | -(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [resolve(135,a,21,a)]. given #121 (T,wt=34): 131 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f1(f(SUC(f5(f2(x)))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(SUC(N) * pow(f2(x))))))). [resolve(107,b,3,d)]. given #122 (T,wt=34): 132 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f1(f(SUC(f5(f2(x)))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(SUC(N) * pow(f2(x))))))). [resolve(107,b,3,a)]. given #123 (T,wt=34): 152 N * pow(f2(x)) <= f(f4(f2(x))) | f(SUC(f(SUC(f(SUC(f(SUC(SUC(N) * pow(f2(x)))))))))) <= f1(f1(f1(f1(f(SUC(f5(f2(x)))))))). [resolve(130,b,5,a)]. given #124 (T,wt=35): 91 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(SUC(f5(f2(x)))) <= SUC(N) * pow(f2(x))) | -(SUC(N) * pow(f2(x)) < SUC(N) * pow(f2(x))). [resolve(90,b,21,c)]. given #125 (A,wt=35): 93 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(f5(f2(x))) < N * pow(f2(x))) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(90,b,18,b)]. given #126 (F,wt=59): 110 -(f1(f1(f1(f1(f1(f1(f(f3(x)))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))). [resolve(77,a,21,c)]. given #127 (F,wt=66): 133 -(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))). [resolve(112,a,21,c)]. given #128 (F,wt=73): 155 -(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))). [resolve(135,a,21,c)]. given #129 (T,wt=35): 143 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f1(f(f4(f2(x)))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(N * pow(f2(x))))))))). [resolve(119,b,3,d)]. given #130 (T,wt=35): 144 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f1(f(f4(f2(x)))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(N * pow(f2(x))))))))). [resolve(119,b,3,a)]. given #131 (T,wt=35): 148 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(f1(f(SUC(f5(f2(x)))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(SUC(N) * pow(f2(x))))))). [resolve(124,b,3,d)]. given #132 (T,wt=35): 149 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(f1(f(SUC(f5(f2(x)))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(SUC(N) * pow(f2(x))))))). [resolve(124,b,3,a)]. given #133 (A,wt=36): 99 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) <= SUC(N) * pow(f2(x))) | -(SUC(N) * pow(f2(x)) < SUC(N) * pow(f2(x))). [resolve(98,b,21,c)]. given #134 (T,wt=35): 157 f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))))))) <= f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))). [resolve(135,a,5,a)]. given #135 (T,wt=35): 164 f(f5(f2(x))) < N * pow(f2(x)) | f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(f2(x)))))))))))) <= f1(f1(f1(f1(f1(f(f4(f2(x)))))))). [resolve(142,b,5,a)]. given #136 (T,wt=35): 169 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f(SUC(f(SUC(f(SUC(SUC(N) * pow(f2(x)))))))))) <= f1(f1(f1(f1(f(SUC(f5(f2(x)))))))). [resolve(147,b,5,a)]. given #137 (T,wt=36): 101 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(98,b,18,b)]. given #138 (A,wt=42): 105 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f(SUC(f5(f2(x))))) <= f(SUC(SUC(N) * pow(f2(x))))) | -(f(SUC(SUC(N) * pow(f2(x)))) < f(SUC(SUC(N) * pow(f2(x))))). [resolve(94,b,21,c)]. given #139 (F,wt=40): 183 -(SUC(N) * pow(f2(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [ur(3,a,157,a,b,7,a,c,9,a)]. given #140 (F,wt=41): 181 -(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) <= y) | -(y < z) | -(z < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [resolve(157,a,3,d)]. given #141 (F,wt=41): 182 -(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) < y) | -(y < z) | -(z <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [resolve(157,a,3,a)]. given #142 (F,wt=43): 184 -(N * pow(f2(N * pow(f2(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [ur(3,a,157,a,b,7,a,c,7,a)]. given #143 (T,wt=26): 195 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(101,b,88,b),merge(c)]. given #144 (T,wt=16): 196 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f5(f2(x)) <= c1. [resolve(195,b,4,a)]. given #145 (T,wt=19): 198 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(c1 < c1) | -(c1 <= f5(f2(x))). [resolve(196,b,21,a)]. given #146 (T,wt=19): 199 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) <= f1(c1). [resolve(196,b,5,a)]. given #147 (A,wt=38): 106 N * pow(f2(x)) <= f(f4(f2(x))) | -(f1(f(SUC(f5(f2(x))))) < f1(f(SUC(f5(f2(x)))))) | -(f1(f(SUC(f5(f2(x))))) <= f(SUC(SUC(N) * pow(f2(x))))). [resolve(94,b,21,a)]. given #148 (F,wt=60): 179 -(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) < f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x)))))))))))) | -(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [resolve(157,a,21,a)]. given #149 (F,wt=80): 178 -(f1(f1(f1(f1(f1(f1(f1(f1(f1(f(f3(x))))))))))) <= f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))) | -(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x))))))))))))))))))) < f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(f(SUC(N * pow(x)))))))))))))))))))). [resolve(157,a,21,c)]. given #150 (T,wt=22): 200 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(c1 <= y) | -(y < z) | -(z < f5(f2(x))). [resolve(196,b,3,d)]. given #151 (T,wt=22): 201 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(c1 < y) | -(y < z) | -(z <= f5(f2(x))). [resolve(196,b,3,a)]. given #152 (T,wt=22): 205 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f(SUC(f5(f2(x)))))) <= f1(f1(c1)). [resolve(199,b,5,a)]. given #153 (T,wt=23): 197 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(c1 <= f5(f2(x))) | -(f5(f2(x)) < f5(f2(x))). [resolve(196,b,21,c)]. given #154 (A,wt=45): 117 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f(f4(f2(x))))) <= f(SUC(f(SUC(N * pow(f2(x))))))) | -(f(SUC(f(SUC(N * pow(f2(x)))))) < f(SUC(f(SUC(N * pow(f2(x))))))). [resolve(84,b,21,c)]. given #155 (T,wt=23): 202 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(c1) < y) | -(y < SUC(N) * pow(f2(x))). [resolve(199,b,103,b),merge(b)]. given #156 (T,wt=19): 214 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(c1) < N * pow(f2(x))). [resolve(202,c,9,a)]. given #157 (T,wt=13): 215 f(f4(f2(f1(c1)))) < SUC(N) * pow(f2(f1(c1))). [resolve(214,b,7,a)]. given #158 (T,wt=12): 216 f(f5(f2(f1(c1)))) < N * pow(f2(f1(c1))). [resolve(215,a,71,b)]. given #159 (A,wt=39): 118 f(f5(f2(x))) < N * pow(f2(x)) | -(f1(f1(f(f4(f2(x))))) < f1(f1(f(f4(f2(x)))))) | -(f1(f1(f(f4(f2(x))))) <= f(SUC(f(SUC(N * pow(f2(x))))))). [resolve(84,b,21,a)]. given #160 (F,wt=12): 218 -(N * pow(f2(f1(c1))) <= f(f4(f2(f1(c1))))). [ur(19,b,215,a)]. given #161 (F,wt=9): 228 -(f(SUC(f5(f2(f1(c1))))) <= f1(c1)). [ur(95,a,218,a,c,7,a,d,9,a)]. given #162 (F,wt=6): 230 -(f5(f2(f1(c1))) <= c1). [ur(5,b,228,a)]. ============================== PROOF ================================= % Proof 1 at 0.05 (+ 0.01) seconds. % Length of proof is 44. % Level of proof is 15. % Maximum clause weight is 36. % Given clauses 162. 1 (all a all L all x all y (a <= L & L < x & x < y & y <= a -> $F)) # label(non_clause). [assumption]. 2 (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 < N * pow(n))) & (all n exists m N * pow(n) <= f(m)) & (all n N * pow(n) < SUC(N) * pow(n)) & (all n (N * pow(n) < SUC(N) * pow(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]. 3 -(x <= y) | -(y < z) | -(z < u) | -(u <= x). [clausify(1)]. 4 -(SUC(N) * f(x) < N * f(SUC(x))) | x <= c1. [deny(2)]. 5 -(x <= y) | f(SUC(x)) <= f1(y). [deny(2)]. 6 f(0) < N * pow(f2(x)). [deny(2)]. 7 x < N * pow(f2(x)). [deny(2)]. 8 N * pow(x) <= f(f3(x)). [deny(2)]. 9 N * pow(x) < SUC(N) * pow(x). [deny(2)]. 10 -(N * pow(x) < SUC(N) * pow(x)) | -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [deny(2)]. 11 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [copy(10),unit_del(a,9)]. 12 -(N * pow(x) < SUC(N) * pow(x)) | -(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(2)]. 13 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [copy(12),unit_del(a,9)]. 14 -(N * pow(x) < SUC(N) * pow(x)) | -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [deny(2)]. 15 -(f(0) < N * pow(x)) | -(N * pow(x) <= f(y)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [copy(14),unit_del(a,9)]. 16 -(N * pow(x) < SUC(N) * pow(x)) | -(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(2)]. 17 -(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))). [copy(16),unit_del(a,9)]. 18 -(f(x) < N * pow(y)) | -(SUC(N) * pow(y) <= f(SUC(x))) | SUC(N) * f(x) < N * f(SUC(x)). [deny(2)]. 19 -(N * pow(x) <= f(y)) | -(f(y) < SUC(N) * pow(x)). [deny(2)]. 33 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | f(f5(x)) < N * pow(x). [resolve(11,b,8,a)]. 34 -(f(0) < N * pow(x)) | N * pow(x) <= f(f4(x)) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(13,b,8,a)]. 35 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | f(f5(x)) < N * pow(x). [resolve(15,b,8,a)]. 36 -(f(0) < N * pow(x)) | f(f4(x)) < SUC(N) * pow(x) | SUC(N) * pow(x) <= f(SUC(f5(x))). [resolve(17,b,8,a)]. 68 N * pow(f2(x)) <= f(f4(f2(x))) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(33,a,6,a)]. 71 f(f5(f2(x))) < N * pow(f2(x)) | -(f(f4(f2(x))) < SUC(N) * pow(f2(x))). [resolve(68,a,19,a)]. 88 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(f5(f2(x))) < N * pow(f2(x)). [resolve(35,a,6,a)]. 90 N * pow(f2(x)) <= f(f4(f2(x))) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(34,a,6,a)]. 93 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(f5(f2(x))) < N * pow(f2(x))) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(90,b,18,b)]. 95 N * pow(f2(x)) <= f(f4(f2(x))) | -(f(SUC(f5(f2(x)))) <= y) | -(y < z) | -(z < SUC(N) * pow(f2(x))). [resolve(90,b,3,d)]. 98 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * pow(f2(x)) <= f(SUC(f5(f2(x)))). [resolve(36,a,6,a)]. 101 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(98,b,18,b)]. 103 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f(SUC(f5(f2(x)))) <= y) | -(y < z) | -(z < SUC(N) * pow(f2(x))). [resolve(98,b,3,d)]. 195 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | SUC(N) * f(f5(f2(x))) < N * f(SUC(f5(f2(x)))). [resolve(101,b,88,b),merge(c)]. 196 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f5(f2(x)) <= c1. [resolve(195,b,4,a)]. 199 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | f(SUC(f5(f2(x)))) <= f1(c1). [resolve(196,b,5,a)]. 202 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(c1) < y) | -(y < SUC(N) * pow(f2(x))). [resolve(199,b,103,b),merge(b)]. 214 f(f4(f2(x))) < SUC(N) * pow(f2(x)) | -(f1(c1) < N * pow(f2(x))). [resolve(202,c,9,a)]. 215 f(f4(f2(f1(c1)))) < SUC(N) * pow(f2(f1(c1))). [resolve(214,b,7,a)]. 216 f(f5(f2(f1(c1)))) < N * pow(f2(f1(c1))). [resolve(215,a,71,b)]. 218 -(N * pow(f2(f1(c1))) <= f(f4(f2(f1(c1))))). [ur(19,b,215,a)]. 219 SUC(N) * f(f5(f2(f1(c1)))) < N * f(SUC(f5(f2(f1(c1))))). [resolve(216,a,93,b),unit_del(a,218)]. 228 -(f(SUC(f5(f2(f1(c1))))) <= f1(c1)). [ur(95,a,218,a,c,7,a,d,9,a)]. 230 -(f5(f2(f1(c1))) <= c1). [ur(5,b,228,a)]. 231 $F. [ur(4,b,230,a),unit_del(a,219)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=162. Generated=315. Kept=224. proofs=1. Usable=157. Sos=57. Demods=0. Limbo=0, Disabled=23. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=90. Back_subsumed=10. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1128. Nonunit_bsub_feature_tests=254. Megabytes=0.48. User_CPU=0.05, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4540 exit (max_proofs) Tue Mar 5 15:34:00 2013
こうしたロジックの処理だけなら，HOL Light は不要です．
