MAYBE
LCTRS
  Theories
    Core, Ints
  Defines
    max: ((x Int) (y Int)) Int (ite (>= x y) x y)
  Signature
    build: Int -> Int
    cmod: (Int, Int) -> Int
    if_mod: (Int, Int) -> Int
    minus: (Int, Int) -> Int
    pred: Int -> Int
  Rules
    minus(!x, !y) -> !z [and(>=(!y, 0), and(>=(!x, !y), !z = max(-(!x, !y), 0)))]
    cmod(!x, !y) -> 0 [or(!x = 0, and(!y = 0, >(!x, 0)))]
    cmod(!x, !y) -> if_mod(!x, !y) [and(>(!x, 0), >(!y, 0))]
    if_mod(!x, !y) -> cmod(minus(-(!x, 1), -(!y, 1)), !y) [and(<=(-(!y, 1), -(!x, 1)), and(>(!x, 1), >(!y, 1)))]
    if_mod(!x, !y) -> !x [and(not(<=(-(!y, 1), -(!x, 1))), and(>(!x, 1), >(!y, 1)))]
No termination info given.

Elapsed Time:  76.22 ms