NO
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/inc3.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,
     inc(dec(?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,
     inc(dec(?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,
     inc(dec(?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,
     inc(dec(?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,
     inc(dec(?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,
     inc(dec(?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(dec(?xs)) = ?xs,
     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(dec(?xs)) = ?xs,
     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(dec(?xs)) = ?xs,
     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(dec(?xs)) = ?xs,
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS1:
   [ dec(inc(?xs)) -> ?xs ]
Expand inc(dec(?xs)) = ?xs
   [ inc(nil) = nil,
     inc(cons(0,dec(?xs_3))) = cons(0,?xs_3),
     inc(cons(?x_4,dec(?xs_4))) = cons(s(?x_4),?xs_4) ]
ES2:
   [ nil = nil,
     cons(s(0),inc(dec(?xs_3))) = cons(0,?xs_3),
     cons(s(?x_4),inc(dec(?xs_4))) = cons(s(?x_4),?xs_4),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS2:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
STEP 2
ES:
   [ nil = nil,
     cons(s(0),inc(dec(?xs_3))) = cons(0,?xs_3),
     cons(s(?x_4),inc(dec(?xs_4))) = cons(s(?x_4),?xs_4),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ nil = nil,
     cons(s(0),?xs_3) = cons(0,?xs_3),
     cons(s(?x_4),?xs_4) = cons(s(?x_4),?xs_4),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS0:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ cons(s(0),?xs_3) = cons(0,?xs_3),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS1:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
: Success(not GCR)
(9 msec.)