YES
LCTRS
  Theories
    Core, Ints
  Signature
    max: (Int, Int) -> Int
  Rules
    max(?12, ?13) -> max(?13, ?12)
    max(?14, ?15) -> ?14 [>=(?14, ?15)]
    max(?16, ?17) -> ?17 [>=(?17, ?16)]
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        max(?14', ?15') -> ?14' [>=(?14', ?15')]
      Outer Rule
        max(?12", ?13") -> max(?13", ?12")
      Pair
        ?12" ≈ max(?13", ?12") [>=(?12", ?13")]
    which reaches the trivial constrained equation
      ?12" ≈ max(?13", ?12") [>=(?12", ?13")]
        -o-> ?12" ≈ max(?13", ?12") [>=(?12", ?13")]
        -o-> ?12" ≈ ?12" [>=(?12", ?13")]
    * Critical Pair
      Inner Rule
        max(?16', ?17') -> ?17' [>=(?17', ?16')]
      Outer Rule
        max(?12", ?13") -> max(?13", ?12")
      Pair
        ?13" ≈ max(?13", ?12") [>=(?13", ?12")]
    which reaches the trivial constrained equation
      ?13" ≈ max(?13", ?12") [>=(?13", ?12")]
        -o-> ?13" ≈ max(?13", ?12") [>=(?13", ?12")]
        -o-> ?13" ≈ ?13" [>=(?13", ?12")]
    * Critical Pair
      Inner Rule
        max(?12', ?13') -> max(?13', ?12')
      Outer Rule
        max(?14", ?15") -> ?14" [>=(?14", ?15")]
      Pair
        max(?15", ?14") ≈ ?14" [>=(?14", ?15")]
    which reaches the trivial constrained equation
      max(?15", ?14") ≈ ?14" [>=(?14", ?15")]
        -o-> ?14" ≈ ?14" [>=(?14", ?15")]
        -o-> ?14" ≈ ?14" [>=(?14", ?15")]
    * Critical Pair
      Inner Rule
        max(?16', ?17') -> ?17' [>=(?17', ?16')]
      Outer Rule
        max(?14", ?15") -> ?14" [>=(?14", ?15")]
      Pair
        ?15" ≈ ?14" [>=(?15", ?14"), >=(?14", ?15")]
    which reaches the trivial constrained equation
      ?15" ≈ ?14" [>=(?15", ?14"), >=(?14", ?15")]
        -o-> ?15" ≈ ?14" [>=(?15", ?14"), >=(?14", ?15")]
        -o-> ?15" ≈ ?14" [>=(?15", ?14"), >=(?14", ?15")]
    * Critical Pair
      Inner Rule
        max(?12', ?13') -> max(?13', ?12')
      Outer Rule
        max(?16", ?17") -> ?17" [>=(?17", ?16")]
      Pair
        max(?17", ?16") ≈ ?17" [>=(?17", ?16")]
    which reaches the trivial constrained equation
      max(?17", ?16") ≈ ?17" [>=(?17", ?16")]
        -o-> ?17" ≈ ?17" [>=(?17", ?16")]
        -o-> ?17" ≈ ?17" [>=(?17", ?16")]
    * Critical Pair
      Inner Rule
        max(?14', ?15') -> ?14' [>=(?14', ?15')]
      Outer Rule
        max(?16", ?17") -> ?17" [>=(?17", ?16")]
      Pair
        ?16" ≈ ?17" [>=(?16", ?17"), >=(?17", ?16")]
    which reaches the trivial constrained equation
      ?16" ≈ ?17" [>=(?16", ?17"), >=(?17", ?16")]
        -o-> ?16" ≈ ?17" [>=(?16", ?17"), >=(?17", ?16")]
        -o-> ?16" ≈ ?17" [>=(?16", ?17"), >=(?17", ?16")]

Elapsed Time: 107.05 ms