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,
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(round(?xs)) -> len(?xs) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,nil,cons,true,false}
Defined function symbols: {if,tl,app,len,null,round}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(?xs) -> if(null(?xs),0,s(len(tl(?xs)))) ]
   [ len(round(?xs)) -> len(?xs) ]
Trying with:
R:
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(?xs) -> if(null(?xs),0,s(len(tl(?xs)))) ]
E:
   [ len(round(?xs)) = len(?xs) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool,List}
Signature:
   [ null : List -> Bool,
     tl : List -> List,
     len : List -> Nat,
     if : Bool,Nat,Nat -> Nat,
     round : List -> List,
     app : List,List -> List,
     cons : Nat,List -> List,
     nil : List,
     true : Bool,
     false : Bool,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(?xs) -> if(null(?xs),0,s(len(tl(?xs)))) ]
Conjecture Part:
   [ len(round(?xs)) = len(?xs) ]
Termination proof failed.
new/len-round2.trs: Failure(unknown)
(1815 msec.)