NO
Rewrite Rules:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     inc(app(?xs,?ys)) -> app(inc(?xs),inc(?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) -> ?xs,
     inc(dec(?xs)) -> ?xs ]
Apply Direct Methods...
Inner CPs:
   [ inc(?ys_1) = app(inc(nil),inc(?ys_1)),
     inc(cons(?x_2,app(?xs_2,?ys_2))) = app(inc(cons(?x_2,?xs_2)),inc(?ys_2)),
     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)),
     dec(nil) = nil,
     dec(cons(s(?x),inc(?xs))) = cons(?x,?xs),
     dec(app(inc(?xs_3),inc(?ys_3))) = app(?xs_3,?ys_3),
     dec(?xs_8) = dec(?xs_8),
     inc(nil) = nil,
     inc(cons(0,dec(?xs_4))) = cons(0,?xs_4),
     inc(cons(?x_5,dec(?xs_5))) = cons(s(?x_5),?xs_5),
     inc(app(dec(?xs_6),dec(?ys_6))) = app(?xs_6,?ys_6),
     inc(?xs_7) = inc(?xs_7) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Final result: not CR
new/inc3.trs: Success(not CR)
(23 msec.)