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