YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/inc.trs
Input rules:
   [ inc(nil) -> nil,
     inc(cons(?x:Nat,?xs:List)) -> cons(s(?x:Nat),inc(?xs:List)),
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     inc(app(?xs:List,?ys:List)) -> app(inc(?xs:List),inc(?ys:List)),
     dec(nil) -> nil,
     dec(cons(0,?xs:List)) -> cons(0,dec(?xs:List)),
     dec(cons(s(?x:Nat),?xs:List)) -> cons(?x:Nat,dec(?xs:List)),
     dec(app(?xs:List,?ys:List)) -> app(dec(?xs:List),dec(?ys:List)),
     dec(inc(?xs:List)) -> ?xs:List ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ inc(nil) -> nil,
     inc(cons(?x:Nat,?xs:List)) -> cons(s(?x:Nat),inc(?xs:List)),
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     inc(app(?xs:List,?ys:List)) -> app(inc(?xs:List),inc(?ys:List)),
     dec(nil) -> nil,
     dec(cons(0,?xs:List)) -> cons(0,dec(?xs:List)),
     dec(cons(s(?x:Nat),?xs:List)) -> cons(?x:Nat,dec(?xs:List)),
     dec(app(?xs:List,?ys:List)) -> app(dec(?xs:List),dec(?ys:List)),
     dec(inc(?xs:List)) -> ?xs:List ]
Constructor pattern: [cons(?x_1,?x_2),nil,s(?x_1),0]
Defined pattern: [app(?x_2,?x_3),dec(?x_1),inc(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for app(?x_2,?x_3):
   [ app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)) ]
candidate for dec(?x_1):
   [ dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)) ]
candidate for inc(?x_1):
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 dec : Mul;
 0 : Mul;
 app : Mul;
 inc : Mul;
 s : Mul;
 nil : Mul;
 cons : Mul;
Rules:
   [ app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)),
     inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)) ]
Conjectures:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs ]
STEP 0
ES:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs ]
HS:
   [ ]
ES0:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs ]
HS0:
   [ ]
ES1:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs ]
HS1:
   [ ]
Expand dec(inc(?xs)) = ?xs
   [ dec(nil) = nil,
     dec(cons(s(?x_5),inc(?xs_5))) = cons(?x_5,?xs_5) ]
ES2:
   [ nil = nil,
     cons(?x_5,dec(inc(?xs_5))) = cons(?x_5,?xs_5),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS2:
   [ dec(inc(?xs)) -> ?xs ]
STEP 1
ES:
   [ nil = nil,
     cons(?x_5,dec(inc(?xs_5))) = cons(?x_5,?xs_5),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS:
   [ dec(inc(?xs)) -> ?xs ]
ES0:
   [ nil = nil,
     cons(?x_5,?xs_5) = cons(?x_5,?xs_5),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS0:
   [ dec(inc(?xs)) -> ?xs ]
ES1:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS1:
   [ dec(inc(?xs)) -> ?xs ]
Expand app(inc(?xs),inc(?ys)) = inc(app(?xs,?ys))
   [ app(nil,inc(?ys)) = inc(app(nil,?ys)),
     app(cons(s(?x_5),inc(?xs_5)),inc(?ys)) = inc(app(cons(?x_5,?xs_5),?ys)) ]
ES2:
   [ inc(?ys) = inc(app(nil,?ys)),
     cons(s(?x_5),app(inc(?xs_5),inc(?ys))) = inc(app(cons(?x_5,?xs_5),?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS2:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
STEP 2
ES:
   [ inc(?ys) = inc(app(nil,?ys)),
     cons(s(?x_5),app(inc(?xs_5),inc(?ys))) = inc(app(cons(?x_5,?xs_5),?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ inc(?ys) = inc(?ys),
     cons(s(?x_5),inc(app(?xs_5,?ys))) = cons(s(?x_5),inc(app(?xs_5,?ys))),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS0:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS1:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
Expand dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys))
   [ dec(?ys_1) = app(dec(nil),dec(?ys_1)),
     dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)) ]
ES2:
   [ dec(?ys_1) = app(dec(nil),dec(?ys_1)),
     dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)) ]
HS2:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
STEP 3
ES:
   [ dec(?ys_1) = app(dec(nil),dec(?ys_1)),
     dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)) ]
HS:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ dec(?ys_1) = dec(?ys_1),
     dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)) ]
HS0:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)) ]
HS1:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
Expand dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2))
   [ cons(0,dec(app(?xs,?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_4,dec(app(?xs,?ys))) = app(dec(cons(s(?x_4),?xs)),dec(?ys)) ]
ES2:
   [ cons(0,app(dec(?xs),dec(?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_4,app(dec(?xs),dec(?ys))) = app(dec(cons(s(?x_4),?xs)),dec(?ys)) ]
HS2:
   [ dec(cons(?x_2,app(?xs_2,?ys_2))) -> app(dec(cons(?x_2,?xs_2)),dec(?ys_2)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
STEP 4
ES:
   [ cons(0,app(dec(?xs),dec(?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_4,app(dec(?xs),dec(?ys))) = app(dec(cons(s(?x_4),?xs)),dec(?ys)) ]
HS:
   [ dec(cons(?x_2,app(?xs_2,?ys_2))) -> app(dec(cons(?x_2,?xs_2)),dec(?ys_2)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ cons(0,app(dec(?xs),dec(?ys))) = cons(0,app(dec(?xs),dec(?ys))),
     cons(?x_4,app(dec(?xs),dec(?ys))) = cons(?x_4,app(dec(?xs),dec(?ys))) ]
HS0:
   [ dec(cons(?x_2,app(?xs_2,?ys_2))) -> app(dec(cons(?x_2,?xs_2)),dec(?ys_2)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ ]
HS1:
   [ dec(cons(?x_2,app(?xs_2,?ys_2))) -> app(dec(cons(?x_2,?xs_2)),dec(?ys_2)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     dec(inc(?xs)) -> ?xs ]
: Success(GCR)
(21 msec.)