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