YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    f: Int -> Int
    g: Int -> Int
  Rules
    f(?7) -> ?8 [?8 = 3]
    g(?9) -> a [?9 = 3]
    g(f(?10)) -> a
Confluent by Parallel Closedness with proof:
    * Critical Pair
      Inner Rule
        f(?7') -> ?8' [?8' = 3]
      Outer Rule
        f(?7") -> ?8" [?8" = 3]
      Pair
        ?8' ≈ ?8" [?8' = 3, ?8" = 3]
    which reaches the trivial constrained equation
      ?8' ≈ ?8" [?8' = 3, ?8" = 3]
        -||-> ?8' ≈ ?8" [?8' = 3, ?8" = 3]
    * Critical Pair
      Inner Rule
        f(?7') -> ?8' [?8' = 3]
      Outer Rule
        g(f(?10")) -> a
      Pair
        g(?8') ≈ a [?8' = 3]
    which reaches the trivial constrained equation
      g(?8') ≈ a [?8' = 3]
        -||-> a ≈ a [?8' = 3]

Elapsed Time:  77.95 ms