TPA v.1.1 Result: Run out of time while trying to prove (non-)termination of that system. Only partial proof available. Default interpretations for symbols are not printed. For polynomial interpretations and semantic labelling over N{0,1} defaults are 2 for constants, identity for unary symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans) defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols. [1] TRS as loaded from the input file: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true,n,l) -> l cond(false,n,l) -> tail(nthtail(s(n),l)) tail(nil) -> nil tail(cons(x,l)) -> l length(nil) -> 0 length(cons(x,l)) -> s(length(l)) ge(u,0) -> true ge(0,s(v)) -> false ge(s(u),s(v)) -> ge(u,v) [2] TRS after applying termination preserving transformation to remove all the function symbol of arity >= 2:(1) nthtail(n,l) -> cond`1(ge(n,length(l)),cond`2(n,l)) (2) cond`1(true,cond`2(n,l)) -> l (3) cond`1(false,cond`2(n,l)) -> tail(nthtail(s(n),l)) (4) tail(nil) -> nil (5) tail(cons(x,l)) -> l (6) length(nil) -> 0 (7) length(cons(x,l)) -> s(length(l)) (8) ge(u,0) -> true (9) ge(0,s(v)) -> false (10) ge(s(u),s(v)) -> ge(u,v) /tmp/tmp2XeRdn/ex17.trs, 60.72, T Couldn't open file <60>: 60: No such file or directory