NO
LCTRS
  Theories
    Core, Ints
  Signature
    f: Int -> Int
  Rules
    f(?4) -> ?5 [?4 = *(?5, ?5)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      f(?4') -> ?5' [=(?4', *(?5', ?5'))]
    Outer Rule
      f(?4") -> ?5" [=(?4", *(?5", ?5"))]
    Pair
      ?5' ≈ ?5" [=(?4", *(?5', ?5')), =(?4", *(?5", ?5"))]
  reaches the non-trivial normal form
    ?5' ≈ ?5" [?4" = *(?5', ?5'), ?4" = *(?5", ?5")]

Elapsed Time:  82.01 ms