YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  prime(0()) -> false()
     , prime(s(0())) -> false()
     , prime(s(s(x))) -> prime1(s(s(x)), s(x))
     , prime1(x, 0()) -> false()
     , prime1(x, s(0())) -> true()
     , prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
     , divp(x, y) -> =(rem(x, y), 0())}

Proof Output:    
  Strict Rules in Predicative Notation:
   {  prime(0();) -> false()
    , prime(s(; 0());) -> false()
    , prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
    , prime1(0(); x) -> false()
    , prime1(s(; 0()); x) -> true()
    , prime1(s(; s(; y)); x) ->
      and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
    , divp(; x, y) -> =(; rem(; x, y), 0())}
  Safe Mapping:
   safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
   safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
   safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
   safe(rem) = {1, 2}
  Argument Permutation:
   mu(prime) = [1], mu(prime1) = [1, 2], mu(divp) = [2, 1]
  Precedence:
   divp ~ divp, prime1 > divp, prime1 ~ prime1, prime > divp,
   prime > prime1, prime ~ prime