MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ eq(0,0) -> true,
     eq(s(?x),0) -> false,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     count(zero,?y,?z) -> eq(?y,?z),
     count(succ(?x),?y,?z) -> count(?x,s(?y),?z),
     count(pred(?x),?y,?z) -> count(?x,?y,s(?z)),
     intZero(?x) -> count(?x,0,0),
     succ(pred(?x)) -> ?x,
     pred(succ(?x)) -> ?x ]
Constructors: {0,s,pred,succ,true,zero,false}
Defined function symbols: {eq,count,intZero}
Constructor subsystem:
   [ succ(pred(?x)) -> ?x,
     pred(succ(?x)) -> ?x ]
Rule part & Conj Part:
   [ succ(pred(?x)) -> ?x,
     pred(succ(?x)) -> ?x,
     eq(0,0) -> true,
     eq(s(?x),0) -> false,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     count(zero,?y,?z) -> eq(?y,?z),
     count(succ(?x),?y,?z) -> count(?x,s(?y),?z),
     count(pred(?x),?y,?z) -> count(?x,?y,s(?z)),
     intZero(?x) -> count(?x,0,0) ]
   [ ]
Trying with:
R:
   [ succ(pred(?x)) -> ?x,
     pred(succ(?x)) -> ?x,
     eq(0,0) -> true,
     eq(s(?x),0) -> false,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     count(zero,?y,?z) -> eq(?y,?z),
     count(succ(?x),?y,?z) -> count(?x,s(?y),?z),
     count(pred(?x),?y,?z) -> count(?x,?y,s(?z)),
     intZero(?x) -> count(?x,0,0) ]
E:
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int,Nat,Bool}
Signature:
   [ eq : Nat,Nat -> Bool,
     count : Int,Nat,Nat -> Bool,
     intZero : Int -> Bool,
     true : Bool,
     false : Bool,
     pred : Int -> Int,
     succ : Int -> Int,
     zero : Int,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ succ(pred(?x)) -> ?x,
     pred(succ(?x)) -> ?x,
     eq(0,0) -> true,
     eq(s(?x),0) -> false,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     count(zero,?y,?z) -> eq(?y,?z),
     count(succ(?x),?y,?z) -> count(?x,s(?y),?z),
     count(pred(?x),?y,?z) -> count(?x,?y,s(?z)),
     intZero(?x) -> count(?x,0,0) ]
Conjecture Part:
   [ ]
Termination proof failed.
new/int3.trs: Failure(unknown)
(16 msec.)