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: log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y) cond(true,x,y) -> s(0) cond(false,x,y) -> double(log(x,square(s(s(y))))) le(0,v) -> true le(s(u),0) -> false le(s(u),s(v)) -> le(u,v) double(0) -> 0 double(s(x)) -> s(s(double(x))) square(0) -> 0 square(s(x)) -> s(plus(square(x),double(x))) plus(n,0) -> n plus(n,s(m)) -> s(plus(n,m)) [2] TRS after applying termination preserving transformation to remove all the function symbol of arity >= 2:(1) log(x,s(s(y))) -> cond`1(le(x,s(s(y))),cond`2(x,y)) (2) cond`1(true,cond`2(x,y)) -> s(0) (3) cond`1(false,cond`2(x,y)) -> double(log(x,square(s(s(y))))) (4) le(0,v) -> true (5) le(s(u),0) -> false (6) le(s(u),s(v)) -> le(u,v) (7) double(0) -> 0 (8) double(s(x)) -> s(s(double(x))) (9) square(0) -> 0 (10) square(s(x)) -> s(plus(square(x),double(x))) (11) plus(n,0) -> n (12) plus(n,s(m)) -> s(plus(n,m)) /tmp/tmp94QRR6/ex18.trs, 67.37, T Couldn't open file <60>: 60: No such file or directory