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