MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))),
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,nil,cons,true,false}
Defined function symbols: {if,tl,null,count}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))) ]
   [ if(?x,?y,?y) -> ?y ]
Trying with:
R:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))) ]
E:
   [ if(?x,?y,?y) = ?y ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool,List}
Signature:
   [ null : List -> Bool,
     cons : Nat,List -> List,
     nil : List,
     0 : Nat,
     s : Nat -> Nat,
     true : Bool,
     false : Bool,
     count : List -> Nat,
     if : Bool,Nat,Nat -> Nat,
     tl : List -> List ]
Rule Part:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))) ]
Conjecture Part:
   [ if(?x,?y,?y) = ?y ]
Termination proof failed.
new/if7.trs: Failure(unknown)
(1903 msec.)