MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     len(?xs) -> if(null(?xs),0,s(len(tl(?xs)))),
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     len(app(?xs,?ys)) -> +(len(?xs),len(?ys)) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,nil,cons,true,false}
Defined function symbols: {+,if,tl,app,len,null}
Constructor subsystem:
   [ ]
no strongly quasi-reducible parts found
new/len-app.trs: Failure(unknown)
(1767 msec.)