YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/inc2.trs
Input rules:
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     hd(nil) -> 0,
     hd(cons(?x:Nat,?xs:List)) -> ?x:Nat,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     inc(?xs:List) -> if(null(?xs:List),nil,cons(s(hd(?xs:List)),inc(tl(?xs:List)))),
     if(true,?ys:List,?zs:List) -> ?ys:List,
     if(false,?ys:List,?zs:List) -> ?zs:List,
     nil -> inc(nil),
     inc(cons(?x:Nat,?xs:List)) -> cons(s(?x:Nat),inc(?xs:List)) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     hd(nil) -> 0,
     hd(cons(?x:Nat,?xs:List)) -> ?x:Nat,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     inc(?xs:List) -> if(null(?xs:List),nil,cons(s(hd(?xs:List)),inc(tl(?xs:List)))),
     if(true,?ys:List,?zs:List) -> ?ys:List,
     if(false,?ys:List,?zs:List) -> ?zs:List,
     nil -> inc(nil),
     inc(cons(?x:Nat,?xs:List)) -> cons(s(?x:Nat),inc(?xs:List)) ]
Constructor pattern: [true,false,cons(?x_1,?x_2),s(?x_1),0]
Defined pattern: [nil,if(?x_3,?x_4,?x_5),inc(?x_1),tl(?x_1),hd(?x_1),null(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
No orientable rules for nil. Add rules, and retry...
failed to construct defining rules
Retry with a different D/C-partition.
Constructor pattern: [true,false,cons(?x_1,?x_2),s(?x_1),0,nil]
Defined pattern: [if(?x_3,?x_4,?x_5),inc(?x_1),tl(?x_1),hd(?x_1),null(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(true,?ys,?zs) -> ?ys,
     if(false,?ys,?zs) -> ?zs ]
candidate for inc(?x_1):
No canditates. Supplement rules, and retry...
patlist: 
{cons(?x,?xs)}
Required Patterns: {inc(nil)}
Added rules:
   [ inc(nil) -> nil ]
candidate for inc(?x_1):
   [ inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     inc(nil) -> nil ]
candidate for tl(?x_1):
   [ tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs ]
candidate for hd(?x_1):
   [ hd(nil) -> 0,
     hd(cons(?x,?xs)) -> ?x ]
candidate for null(?x_1):
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 null : Mul,  hd : Mul;
 if : Mul;
 false : Mul,  0 : Mul;
 tl : Mul;
 inc : Mul,  s : Mul;
 cons : Mul;
 true : Mul,  nil : Mul;
Rules:
   [ if(true,?ys,?zs) -> ?ys,
     if(false,?ys,?zs) -> ?zs,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     inc(nil) -> nil,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     hd(nil) -> 0,
     hd(cons(?x,?xs)) -> ?x,
     null(nil) -> true,
     null(cons(?x,?xs)) -> false ]
Conjectures:
   [ inc(?xs) = if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))),
     nil = inc(nil) ]
STEP 0
ES:
   [ inc(?xs) = if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))),
     nil = inc(nil) ]
HS:
   [ ]
ES0:
   [ inc(?xs) = if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))),
     nil = nil ]
HS0:
   [ ]
ES1:
   [ inc(?xs) = if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) ]
HS1:
   [ ]
Expand if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) = inc(?xs)
   [ if(true,nil,cons(s(hd(nil)),inc(tl(nil)))) = inc(nil),
     if(false,nil,cons(s(hd(cons(?x_6,?xs_6))),inc(tl(cons(?x_6,?xs_6))))) = inc(cons(?x_6,?xs_6)) ]
ES2:
   [ nil = inc(nil),
     cons(s(?x_6),inc(?xs_6)) = inc(cons(?x_6,?xs_6)) ]
HS2:
   [ if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) -> inc(?xs) ]
STEP 1
ES:
   [ nil = inc(nil),
     cons(s(?x_6),inc(?xs_6)) = inc(cons(?x_6,?xs_6)) ]
HS:
   [ if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) -> inc(?xs) ]
ES0:
   [ nil = nil,
     cons(s(?x_6),inc(?xs_6)) = cons(s(?x_6),inc(?xs_6)) ]
HS0:
   [ if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) -> inc(?xs) ]
ES1:
   [ ]
HS1:
   [ if(null(?xs),nil,cons(s(hd(?xs)),inc(tl(?xs)))) -> inc(?xs) ]
: Success(GCR)
(20 msec.)