TPA v.1.1

Result: Couldn't 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:
sort(l) -> st(0,l)
st(n,l) -> cond1(member(n,l),n,l)
cond1(true,n,l) -> cons(n,st(s(n),l))
cond1(false,n,l) -> cond2(gt(n,max(l)),n,l)
cond2(true,n,l) -> nil
cond2(false,n,l) -> st(s(n),l)
member(n,nil) -> false
member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
or(x,true) -> true
or(x,false) -> x
equal(0,0) -> true
equal(s(x),0) -> false
equal(0,s(y)) -> false
equal(s(x),s(y)) -> equal(x,y)
gt(0,v) -> false
gt(s(u),0) -> true
gt(s(u),s(v)) -> gt(u,v)
max(nil) -> 0
max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
if(true,u,v) -> u
if(false,u,v) -> v

[2]  TRS after applying termination preserving transformation to remove all the function symbol of arity >= 2: 
(1) sort(l) -> st(0,l)
(2) st(n,l) -> cond1`1(member(n,l),cond1`2(n,l))
(3) cond1`1(true,cond1`2(n,l)) -> cons(n,st(s(n),l))
(4) cond1`1(false,cond1`2(n,l)) -> cond2`1(gt(n,max(l)),cond2`2(n,l))
(5) cond2`1(true,cond2`2(n,l)) -> nil
(6) cond2`1(false,cond2`2(n,l)) -> st(s(n),l)
(7) member(n,nil) -> false
(8) member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
(9) or(x,true) -> true
(10) or(x,false) -> x
(11) equal(0,0) -> true
(12) equal(s(x),0) -> false
(13) equal(0,s(y)) -> false
(14) equal(s(x),s(y)) -> equal(x,y)
(15) gt(0,v) -> false
(16) gt(s(u),0) -> true
(17) gt(s(u),s(v)) -> gt(u,v)
(18) max(nil) -> 0
(19) max(cons(u,l)) -> if`1(gt(u,max(l)),if`2(u,max(l)))
(20) if`1(true,if`2(u,v)) -> u
(21) if`1(false,if`2(u,v)) -> v


/tmp/tmpAWe0aN/ex15.trs, 32.55, U
Couldn't open file <60>: 60: No such file or directory