YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    f: Int -> Unit
    product: (Unit, Unit) -> Unit
    start: Unit
  Rules
    f(!x) -> product(f(!y), f(!z)) [and(and(and(and(>(!x, !y), >(!y, 0)), >(!x, !z)), >(!z, 0)), !x = *(!y, !z))]
    start -> f(!input)
RPO with precedence:
  {start} > {f} > {and = product > 0 *}

Elapsed Time:  40.49 ms