YES
LCTRS
  Theories
    Core, Ints
  Sorts
    PCP, String
  Signature
    alpha: Int -> String
    beta: Int -> String
    bot: PCP
    e: String
    one: String -> String
    start: PCP
    test: (String, String, Int) -> PCP
    top: PCP
    zero: String -> String
  Rules
    start -> test(alpha(!n), beta(!n), !n) [>(!n, 0)]
    test(e, e, !n) -> top
    test(zero(!x), zero(!y), !n) -> test(!x, !y, !n)
    test(one(!x), one(!y), !n) -> test(!x, !y, !n)
    test(one(!x), zero(!y), !n) -> bot
    test(zero(!x), one(!y), !n) -> bot
    test(zero(!x), e, !n) -> bot
    test(one(!x), e, !n) -> bot
    test(e, zero(!y), !n) -> bot
    test(e, one(!y), !n) -> bot
    alpha(0) -> e
    beta(0) -> e
    alpha(!n) -> one(zero(alpha(!m))) [and(+(*(1, !m), 1) = !n, >(!n, 0))]
    beta(!n) -> zero(zero(beta(!m))) [and(+(*(1, !m), 1) = !n, >(!n, 0))]
RPO with precedence:
  {start} > {beta alpha} > {test e} > {and = zero top one bot > 1 0 + *}

Elapsed Time:  39.50 ms