YES
Time: 0.012814
TRS:
 {       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())}
 DP:
  DP:
   {     prime# s s x -> prime1#(s s x, s x),
    prime1#(x, s s y) -> prime1#(x, s y),
    prime1#(x, s s y) -> divp#(s s y, x)}
  TRS:
  {       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())}
  EDG:
   {(prime# s s x -> prime1#(s s x, s x), prime1#(x, s s y) -> divp#(s s y, x))
    (prime# s s x -> prime1#(s s x, s x), prime1#(x, s s y) -> prime1#(x, s y))
    (prime1#(x, s s y) -> prime1#(x, s y), prime1#(x, s s y) -> prime1#(x, s y))
    (prime1#(x, s s y) -> prime1#(x, s y), prime1#(x, s s y) -> divp#(s s y, x))}
   STATUS:
    arrows: 0.555556
    SCCS (1):
     Scc:
      {prime1#(x, s s y) -> prime1#(x, s y)}
     
     
     SCC (1):
      Strict:
       {prime1#(x, s s y) -> prime1#(x, s y)}
      Weak:
      {       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())}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [prime1](x0, x1) = x0,
        
        [and](x0, x1) = x0 + 1,
        
        [divp](x0, x1) = x0 + 1,
        
        [=](x0, x1) = 1,
        
        [rem](x0, x1) = 0,
        
        [prime](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [not](x0) = x0,
        
        [false] = 0,
        
        [0] = 1,
        
        [true] = 0,
        
        [prime1#](x0, x1) = x0 + 1
       Strict:
        prime1#(x, s s y) -> prime1#(x, s y)
        3 + 0x + 1y >= 2 + 0x + 1y
       Weak:
        divp(x, y) -> =(rem(x, y), 0())
        1 + 1x + 0y >= 1 + 0x + 0y
        prime1(x, s s y) -> and(not divp(s s y, x), prime1(x, s y))
        0 + 1x + 0y >= 4 + 0x + 1y
        prime1(x, s 0()) -> true()
        0 + 1x >= 0
        prime1(x, 0()) -> false()
        0 + 1x >= 0
        prime s s x -> prime1(s s x, s x)
        0 + 0x >= 2 + 1x
        prime s 0() -> false()
        0 >= 0
        prime 0() -> false()
        0 >= 0
      Qed