YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     +(?x,?y) -> +(?y,?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
Apply Direct Methods...
Inner CPs:
   [ inc(?y) = +(inc(0),?y),
     inc(s(+(?x_1,?y_1))) = +(inc(s(?x_1)),?y_1),
     inc(+(?y_3,?x_3)) = +(inc(?x_3),?y_3) ]
Outer CPs:
   [ ?y = +(?y,0),
     s(+(?x_1,?y_1)) = +(?y_1,s(?x_1)),
     s(+(?x_4,?y_4)) = +(inc(?x_4),?y_4) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ +(?y,0) = ?y,
     +(inc(0),?y) = inc(?y),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(inc(s(?x)),?y) = inc(s(+(?x,?y))),
     +(inc(?x_4),?y_4) = s(+(?x_4,?y_4)),
     ?y = +(?y,0),
     s(+(?x_2,?y)) = +(?y,s(?x_2)),
     +(inc(?x),?y) = inc(+(?y,?x)),
     s(?y) = +(inc(0),?y),
     s(s(+(?x_3,?y))) = +(inc(s(?x_3)),?y),
     s(+(?y,?x)) = +(inc(?x),?y),
     s(+(?x,?y)) = +(inc(?x),?y),
     inc(?y) = +(inc(0),?y),
     inc(s(+(?x_3,?y))) = +(inc(s(?x_3)),?y),
     inc(+(?y,?x)) = +(inc(?x),?y) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <inc(?y), +(inc(0),?y)> by Rules <0, 4> preceded by [(inc,1)]
 joinable by a reduction of rules <[([],2)], [([(+,1)],2),([],1),([(s,1)],0)]>
Critical Pair <inc(s(+(?x_1,?y_1))), +(inc(s(?x_1)),?y_1)> by Rules <1, 4> preceded by [(inc,1)]
 joinable by a reduction of rules <[([],2)], [([(+,1)],2),([],1),([(s,1)],1)]>
 joinable by a reduction of rules <[([(inc,1),(s,1)],3),([],2),([(s,1),(s,1)],3)], [([(+,1)],2),([],1),([(s,1)],1)]>
Critical Pair <inc(+(?y_3,?x_3)), +(inc(?x_3),?y_3)> by Rules <3, 4> preceded by [(inc,1)]
 joinable by a reduction of rules <[([(inc,1)],3),([],4)], []>
 joinable by a reduction of rules <[([(inc,1)],3),([],2)], [([(+,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([(s,1)],3)], [([(+,1)],2),([],1)]>
Critical Pair <+(?y_3,0), ?y_3> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([],3),([],0)], []>
Critical Pair <+(?y_3,s(?x_1)), s(+(?x_1,?y_3))> by Rules <3, 1> preceded by []
 joinable by a reduction of rules <[([],3),([],1)], []>
Critical Pair <+(inc(?x_4),?y_4), s(+(?x_4,?y_4))> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([(+,1)],2),([],1)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten +(?x_8,0) and ?x_8
strenghten +(0,?x_6) and ?x_6
strenghten +(?x_11,?y_11) and +(?y_11,?x_11)
strenghten s(s(?x_2)) and inc(s(?x_2))
strenghten s(inc(?x_14)) and s(s(?x_14))
strenghten +(inc(?x_6),0) and inc(?x_6)
strenghten +(inc(0),?x_8) and inc(?x_8)
strenghten s(+(?x_1,0)) and s(?x_1)
strenghten +(inc(?x_3),?y_3) and inc(+(?y_3,?x_3))
strenghten +(inc(?x_4),?y_4) and s(+(?x_4,?y_4))
strenghten +(inc(?x_10),?y_10) and inc(+(?x_10,?y_10))
strenghten s(+(?x_1,?x_12)) and +(?x_12,s(?x_1))
strenghten s(+(?x_1,?x_13)) and +(s(?x_1),?x_13)
strenghten s(+(?x_4,?y_4)) and +(inc(?x_4),?y_4)
strenghten s(s(inc(?x))) and inc(s(s(?x)))
strenghten +(inc(s(?x_1)),?y_1) and inc(s(+(?x_1,?y_1)))
strenghten s(s(+(?x_4,?y_4))) and inc(+(inc(?x_4),?y_4))
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
   [ +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (2)*x1+(2)*x2
  0:= (9)
  s:= (1)*x1
  inc:= (3)+(3)*x1+(2)*x1*x1
retract +(0,?y) -> ?y
retract inc(?x) -> s(?x)
Polynomial Interpretation:
  +:= (2)*x1+(1)*x1*x2+(2)*x2
  0:= (9)
  s:= (6)+(4)*x1
  inc:= (1)+(3)*x1+(2)*x1*x1
retract +(0,?y) -> ?y
retract +(s(?x),?y) -> s(+(?x,?y))
retract inc(?x) -> s(?x)
Polynomial Interpretation:
  +:= (1)+(1)*x1+(1)*x2
  0:= (11)
  s:= (2)+(2)*x1+(6)*x1*x1
  inc:= (4)*x1*x1
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
P:
   [ +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<+(inc(?x_3),?y_3), s(+(?x_3,?y_3))> --> <s(+(?x_3,?y_3)), s(+(?x_3,?y_3))> => yes
<inc(?y), +(inc(0),?y)> --> <s(?y), s(?y)> => yes
<inc(s(+(?x_1,?y_1))), +(inc(s(?x_1)),?y_1)> --> <s(s(+(?x_1,?y_1))), s(s(+(?x_1,?y_1)))> => yes
PCP_in(symP,S):
<inc(+(?x_1,?y_1)), +(inc(?y_1),?x_1)> --> <s(+(?x_1,?y_1)), s(+(?y_1,?x_1))> => yes
CP(S,symP):
<?y, +(?y,0)> --> <?y, +(?y,0)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from ?y to +(?y,0): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
failed
failure(Step 1)
   [ +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added S-Rules:
   [ +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 2 (linear)
S:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
P:
   [ +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<+(inc(?x_3),?y_3), s(+(?x_3,?y_3))> --> <s(+(?x_3,?y_3)), s(+(?x_3,?y_3))> => yes
<inc(?y), +(inc(0),?y)> --> <s(?y), s(?y)> => yes
<inc(s(+(?x_1,?y_1))), +(inc(s(?x_1)),?y_1)> --> <s(s(+(?x_1,?y_1))), s(s(+(?x_1,?y_1)))> => yes
CP_in(symP,S):
<inc(+(?x,?y)), +(inc(?y),?x)> --> <s(+(?x,?y)), s(+(?y,?x))> => yes
CP(S,symP):
<?y, +(?y,0)> --> <?y, +(?y,0)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from ?y to +(?y,0): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
failed
failure(Step 2)
   [ +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added S-Rules:
   [ +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 3 (relative)
S:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
P:
   [ +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y) ]
   [ +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (2)*x1+(2)*x2
  0:= (9)
  s:= (1)*x1
  inc:= (3)+(3)*x1+(2)*x1*x1
retract +(0,?y) -> ?y
retract inc(?x) -> s(?x)
Polynomial Interpretation:
  +:= (2)*x1+(1)*x1*x2+(2)*x2
  0:= (9)
  s:= (6)+(4)*x1
  inc:= (1)+(3)*x1+(2)*x1*x1
retract +(0,?y) -> ?y
retract +(s(?x),?y) -> s(+(?x,?y))
retract inc(?x) -> s(?x)
Polynomial Interpretation:
  +:= (1)+(1)*x1+(1)*x2
  0:= (11)
  s:= (2)+(2)*x1+(6)*x1*x1
  inc:= (4)*x1*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y),
     +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
P:
   [ +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(?x_5,0)), s(?x_5)> --> <s(?x_5), s(?x_5)> => yes
<s(?x_1), s(+(?x_1,0))> --> <s(?x_1), s(?x_1)> => yes
<s(+(?x_5,s(?x_1))), s(+(?x_1,s(?x_5)))> --> <s(s(+(?x_1,?x_5))), s(s(+(?x_5,?x_1)))> => yes
<+(inc(?x_3),?y_3), s(+(?x_3,?y_3))> --> <s(+(?x_3,?y_3)), s(+(?x_3,?y_3))> => yes
<inc(?y), +(inc(0),?y)> --> <s(?y), s(?y)> => yes
<inc(s(+(?x_1,?y_1))), +(inc(s(?x_1)),?y_1)> --> <s(s(+(?x_1,?y_1))), s(s(+(?x_1,?y_1)))> => yes
<inc(?y_4), +(inc(?y_4),0)> --> <s(?y_4), s(?y_4)> => yes
<inc(s(+(?x_5,?y_5))), +(inc(?y_5),s(?x_5))> --> <s(s(+(?x_5,?y_5))), s(s(+(?x_5,?y_5)))> => yes
PCP_in(symP,S):
<inc(+(?x_1,?y_1)), +(inc(?y_1),?x_1)> --> <s(+(?x_1,?y_1)), s(+(?y_1,?x_1))> => yes
CP(S,symP):
<?y, +(?y,0)> --> <?y, ?y> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<?y, +(0,?y)> --> <?y, ?y> => yes
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
S:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     inc(?x) -> s(?x),
     inc(+(?x,?y)) -> +(inc(?x),?y),
     +(?y,0) -> ?y,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
P:
   [ +(?x,?y) -> +(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR

Final result: CR
141.trs: Success(CR)
(1465 msec.)