YES(?,POLY)

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           YES(?,POLY)
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:    
  The input was oriented with the instance of POP* as induced by the precedence
  
   prime > prime1, prime > divp, prime1 > divp
  
  and 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} .
  
  For your convenience, here is the input in predicative notation:
  
   Rules:
    {  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())}