YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
  Rules
    a -> ?2 [?2 = 0]
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        a -> ?2' [?2' = 0]
      Outer Rule
        a -> ?2" [?2" = 0]
      Pair
        ?2' ≈ ?2" [?2' = 0, ?2" = 0]
    which reaches the trivial constrained equation
      ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        ->^* ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        -o-> ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        -o-> ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        -o-> ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        -o-> ?2' ≈ ?2" [?2' = 0, ?2" = 0]
        -o-> ?2' ≈ ?2" [?2' = 0, ?2" = 0]

Elapsed Time:  78.97 ms