YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if7.trs
Input rules:
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
Constructor pattern: [cons(?x_1,?x_2),nil,0,s(?x_1),true,false]
Defined pattern: [tl(?x_1),if(?x_3,?x_4,?x_5),count(?x_1),null(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for tl(?x_1):
   [ tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z ]
No orientable rules for count(?x_1). Add rules, and retry...
Added rules:
   [ count(cons(?x_1,?x_2)) -> s(count(?x_2)),
     count(nil) -> 0 ]
candidate for count(?x_1):
   [ count(cons(?x_1,?x_2)) -> s(count(?x_2)),
     count(nil) -> 0 ]
candidate for null(?x_1):
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 nil : Mul;
 0 : Mul;
 count : Mul;
 null : Mul;
 s : Mul;
 if : Mul;
 cons : Mul;
 false : Mul,  true : Mul;
 tl : Mul;
Rules:
   [ tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     count(cons(?x_1,?x_2)) -> s(count(?x_2)),
     count(nil) -> 0,
     null(nil) -> true,
     null(cons(?x,?ys)) -> false ]
Conjectures:
   [ if(?x,?y,?y) = ?y,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
STEP 0
ES:
   [ if(?x,?y,?y) = ?y,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS:
   [ ]
ES0:
   [ if(?x,?y,?y) = ?y,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS0:
   [ ]
ES1:
   [ if(?x,?y,?y) = ?y,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS1:
   [ ]
Expand if(?x,?y,?y) = ?y
   [ ?z_2 = ?z_2,
     ?z_3 = ?z_3 ]
ES2:
   [ ?z_2 = ?z_2,
     ?z_3 = ?z_3,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS2:
   [ if(?x,?y,?y) -> ?y ]
STEP 1
ES:
   [ ?z_2 = ?z_2,
     ?z_3 = ?z_3,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS:
   [ if(?x,?y,?y) -> ?y ]
ES0:
   [ ?z_2 = ?z_2,
     ?z_3 = ?z_3,
     count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS0:
   [ if(?x,?y,?y) -> ?y ]
ES1:
   [ count(?xs) = if(null(?xs),0,s(count(tl(?xs)))) ]
HS1:
   [ if(?x,?y,?y) -> ?y ]
Expand if(null(?xs),0,s(count(tl(?xs)))) = count(?xs)
   [ if(true,0,s(count(tl(nil)))) = count(nil),
     if(false,0,s(count(tl(cons(?x_6,?ys_6))))) = count(cons(?x_6,?ys_6)) ]
ES2:
   [ 0 = count(nil),
     s(count(?ys_6)) = count(cons(?x_6,?ys_6)) ]
HS2:
   [ if(null(?xs),0,s(count(tl(?xs)))) -> count(?xs),
     if(?x,?y,?y) -> ?y ]
STEP 2
ES:
   [ 0 = count(nil),
     s(count(?ys_6)) = count(cons(?x_6,?ys_6)) ]
HS:
   [ if(null(?xs),0,s(count(tl(?xs)))) -> count(?xs),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ 0 = 0,
     s(count(?ys_6)) = s(count(?ys_6)) ]
HS0:
   [ if(null(?xs),0,s(count(tl(?xs)))) -> count(?xs),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ ]
HS1:
   [ if(null(?xs),0,s(count(tl(?xs)))) -> count(?xs),
     if(?x,?y,?y) -> ?y ]
: Success(GCR)
(28 msec.)