MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    build: Int -> Int
    cmod: (Int, Int) -> Int
    if_mod: (Int, Int) -> Int
    minus: (Int, Int) -> Int
    pred: Int -> Int
  Rules
    build(0) -> 0
    build(!x) -> pred(build(-(!x, 1))) [>(!x, 0)]
    minus(!x, !y) -> -(!x, !y) [and(>=(!y, 0), >=(!x, !y))]
    minus(!x, !y) -> build(-(!y, !x)) [and(>=(!x, 0), >(!y, !x))]
    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: 103.27 ms