YES
LCTRS
  Theories
    Core, Ints
  Signature
    eval1: (Int, Int) -> Int
    eval2: (Int, Int) -> Int
    eval3: (Int, Int) -> Int
  Rules
    eval1(?24, ?25) -> eval2(?24, ?25) [and(and(>(?24, 0), >(?25, 0)), >(?24, ?25))]
    eval1(?26, ?27) -> eval3(?26, ?27) [and(and(>(?26, 0), >(?27, 0)), not(>(?26, ?27)))]
    eval2(?28, ?29) -> eval1(?28, ?29) [not(>(?28, 0))]
    eval2(?30, ?31) -> eval2(+(?30, -1), +(?31, 1)) [>(?30, 0)]
    eval3(?32, ?33) -> eval1(?32, ?33) [not(>(?33, 0))]
    eval3(?34, ?35) -> eval3(+(?34, 1), +(?35, -1)) [>(?35, 0)]
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  43.52 ms