YES
LCTRS
  Theories
    Core, Ints
  Signature
    max: (Int, Int) -> Int
  Rules
    max(?8, ?9) -> ?8 [>=(?8, ?9)]
    max(?10, ?11) -> ?11 [>=(?11, ?10)]
Confluent by Weak Orthogonality with proof:
  * Critical Pair
    Inner Rule
      max(?10', ?11') -> ?11' [>=(?11', ?10')]
    Outer Rule
      max(?8", ?9") -> ?8" [>=(?8", ?9")]
    Pair
      ?9" ≈ ?8" [>=(?9", ?8"), >=(?8", ?9")]
  but it is a trivial constrained equation
    ?9" ≈ ?8" [>=(?9", ?8"), >=(?8", ?9")]
  * Critical Pair
    Inner Rule
      max(?8', ?9') -> ?8' [>=(?8', ?9')]
    Outer Rule
      max(?10", ?11") -> ?11" [>=(?11", ?10")]
    Pair
      ?10" ≈ ?11" [>=(?10", ?11"), >=(?11", ?10")]
  but it is a trivial constrained equation
    ?10" ≈ ?11" [>=(?10", ?11"), >=(?11", ?10")]

Elapsed Time:  79.39 ms