YES
(ignored inputs)COMMENT translated from Cops 173
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
Constructors: {0,s}
Defined function symbols: {max}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)) ]
   [ max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ 0 : Nat,
     s : Nat -> Nat,
     max : Nat,Nat -> Nat ]
Rule Part:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)) ]
Conjecture Part:
   [ max(?x,?y) = max(?y,?x),
     max(?x,?x) = ?x ]
Precedence (by weight): {(0,2),(s,0),(max,3)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)) ]
Conjectures:
   [ max(?x,?y) = max(?y,?x),
     max(?x,?x) = ?x ]
STEP 0
ES:
   [ max(?x,?y) = max(?y,?x),
     max(?x,?x) = ?x ]
HS:
   [ ]
ES0:
   [ max(?x,?y) = max(?y,?x),
     max(?x,?x) = ?x ]
HS0:
   [ ]
ES1:
   [ max(?x,?y) = max(?y,?x),
     max(?x,?x) = ?x ]
HS1:
   [ ]
Expand max(?x,?x) = ?x
   [ 0 = 0,
     0 = 0,
     s(max(?y_3,?y_3)) = s(?y_3) ]
ES2:
   [ 0 = 0,
     0 = 0,
     s(max(?y_3,?y_3)) = s(?y_3),
     max(?x,?y) = max(?y,?x) ]
HS2:
   [ max(?x,?x) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     0 = 0,
     s(max(?y_3,?y_3)) = s(?y_3),
     max(?x,?y) = max(?y,?x) ]
HS:
   [ max(?x,?x) -> ?x ]
ES0:
   [ 0 = 0,
     0 = 0,
     s(?y_3) = s(?y_3),
     max(?x,?y) = max(?y,?x) ]
HS0:
   [ max(?x,?x) -> ?x ]
ES1:
   [ max(?x,?y) = max(?y,?x) ]
HS1:
   [ max(?x,?x) -> ?x ]
Expand max(?x,?y) = max(?y,?x)
   [ ?x_1 = max(0,?x_1),
     ?y_2 = max(?y_2,0),
     s(max(?x_3,?y_3)) = max(s(?y_3),s(?x_3)) ]
ES2:
   [ ?x_1 = max(0,?x_1),
     ?y_2 = max(?y_2,0),
     s(max(?x_3,?y_3)) = max(s(?y_3),s(?x_3)) ]
HS2:
   [ max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
STEP 2
ES:
   [ ?x_1 = max(0,?x_1),
     ?y_2 = max(?y_2,0),
     s(max(?x_3,?y_3)) = max(s(?y_3),s(?x_3)) ]
HS:
   [ max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
ES0:
   [ ?x_1 = ?x_1,
     ?y_2 = ?y_2,
     s(max(?x_3,?y_3)) = s(max(?y_3,?x_3)) ]
HS0:
   [ max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
ES1:
   [ ]
HS1:
   [ max(?x,?y) -> max(?y,?x),
     max(?x,?x) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/open/173.trs: Success(GCR)
(5 msec.)