YES
Time: 0.123496
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())}
  UR:
   {a(z, w) -> z,
    a(z, w) -> w}
   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