MAYBE
Time: 0.008203
TRS:
 {            p 0() -> 0(),
              p s x -> x,
       plus(x, 0()) -> x,
       plus(x, s y) -> s plus(x, p s y),
       plus(0(), y) -> y,
       plus(s x, y) -> s plus(x, y),
       plus(s x, y) -> s plus(p s x, y),
      times(0(), y) -> 0(),
      times(s x, y) -> plus(y, times(x, y)),
    times(s 0(), y) -> y,
          div(x, y) -> quot(x, y, y),
        div(0(), y) -> 0(),
  div(div(x, y), z) -> div(x, times(y, z)),
  quot(x, 0(), s z) -> s div(x, s z),
  quot(0(), s y, z) -> 0(),
  quot(s x, s y, z) -> quot(x, y, z),
       eq(0(), 0()) -> true(),
       eq(0(), s y) -> false(),
       eq(s x, 0()) -> false(),
       eq(s x, s y) -> eq(x, y),
      divides(y, x) -> eq(x, times(div(x, y), y)),
       pr(x, s 0()) -> true(),
       pr(x, s s y) -> if(divides(s s y, x), x, s y),
        prime s s x -> pr(s s x, s x),
   if(true(), x, y) -> false(),
  if(false(), x, y) -> pr(x, y)}
 DP:
  DP:
   {     plus#(x, s y) -> p# s y,
         plus#(x, s y) -> plus#(x, p s y),
         plus#(s x, y) -> p# s x,
         plus#(s x, y) -> plus#(x, y),
         plus#(s x, y) -> plus#(p s x, y),
        times#(s x, y) -> plus#(y, times(x, y)),
        times#(s x, y) -> times#(x, y),
            div#(x, y) -> quot#(x, y, y),
    div#(div(x, y), z) -> times#(y, z),
    div#(div(x, y), z) -> div#(x, times(y, z)),
    quot#(x, 0(), s z) -> div#(x, s z),
    quot#(s x, s y, z) -> quot#(x, y, z),
         eq#(s x, s y) -> eq#(x, y),
        divides#(y, x) -> times#(div(x, y), y),
        divides#(y, x) -> div#(x, y),
        divides#(y, x) -> eq#(x, times(div(x, y), y)),
         pr#(x, s s y) -> divides#(s s y, x),
         pr#(x, s s y) -> if#(divides(s s y, x), x, s y),
          prime# s s x -> pr#(s s x, s x),
    if#(false(), x, y) -> pr#(x, y)}
  TRS:
  {            p 0() -> 0(),
               p s x -> x,
        plus(x, 0()) -> x,
        plus(x, s y) -> s plus(x, p s y),
        plus(0(), y) -> y,
        plus(s x, y) -> s plus(x, y),
        plus(s x, y) -> s plus(p s x, y),
       times(0(), y) -> 0(),
       times(s x, y) -> plus(y, times(x, y)),
     times(s 0(), y) -> y,
           div(x, y) -> quot(x, y, y),
         div(0(), y) -> 0(),
   div(div(x, y), z) -> div(x, times(y, z)),
   quot(x, 0(), s z) -> s div(x, s z),
   quot(0(), s y, z) -> 0(),
   quot(s x, s y, z) -> quot(x, y, z),
        eq(0(), 0()) -> true(),
        eq(0(), s y) -> false(),
        eq(s x, 0()) -> false(),
        eq(s x, s y) -> eq(x, y),
       divides(y, x) -> eq(x, times(div(x, y), y)),
        pr(x, s 0()) -> true(),
        pr(x, s s y) -> if(divides(s s y, x), x, s y),
         prime s s x -> pr(s s x, s x),
    if(true(), x, y) -> false(),
   if(false(), x, y) -> pr(x, y)}
  UR:
   {            p s x -> x,
         plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, p s y),
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(x, y),
         plus(s x, y) -> s plus(p s x, y),
        times(0(), y) -> 0(),
        times(s x, y) -> plus(y, times(x, y)),
      times(s 0(), y) -> y,
            div(x, y) -> quot(x, y, y),
          div(0(), y) -> 0(),
    div(div(x, y), z) -> div(x, times(y, z)),
    quot(x, 0(), s z) -> s div(x, s z),
    quot(0(), s y, z) -> 0(),
    quot(s x, s y, z) -> quot(x, y, z),
         eq(0(), 0()) -> true(),
         eq(0(), s y) -> false(),
         eq(s x, 0()) -> false(),
         eq(s x, s y) -> eq(x, y),
        divides(y, x) -> eq(x, times(div(x, y), y)),
              a(w, v) -> w,
              a(w, v) -> v}
   EDG:
    {(quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> div#(x, times(y, z)))
     (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> times#(y, z))
     (quot#(x, 0(), s z) -> div#(x, s z), div#(x, y) -> quot#(x, y, y))
     (divides#(y, x) -> times#(div(x, y), y), times#(s x, y) -> times#(x, y))
     (divides#(y, x) -> times#(div(x, y), y), times#(s x, y) -> plus#(y, times(x, y)))
     (quot#(s x, s y, z) -> quot#(x, y, z), quot#(s x, s y, z) -> quot#(x, y, z))
     (quot#(s x, s y, z) -> quot#(x, y, z), quot#(x, 0(), s z) -> div#(x, s z))
     (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))
     (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> times#(y, z))
     (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
     (plus#(x, s y) -> plus#(x, p s y), plus#(s x, y) -> plus#(p s x, y))
     (plus#(x, s y) -> plus#(x, p s y), plus#(s x, y) -> plus#(x, y))
     (plus#(x, s y) -> plus#(x, p s y), plus#(s x, y) -> p# s x)
     (plus#(x, s y) -> plus#(x, p s y), plus#(x, s y) -> plus#(x, p s y))
     (plus#(x, s y) -> plus#(x, p s y), plus#(x, s y) -> p# s y)
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(p s x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> p# s x)
     (plus#(s x, y) -> plus#(x, y), plus#(x, s y) -> plus#(x, p s y))
     (plus#(s x, y) -> plus#(x, y), plus#(x, s y) -> p# s y)
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (if#(false(), x, y) -> pr#(x, y), pr#(x, s s y) -> if#(divides(s s y, x), x, s y))
     (if#(false(), x, y) -> pr#(x, y), pr#(x, s s y) -> divides#(s s y, x))
     (div#(x, y) -> quot#(x, y, y), quot#(s x, s y, z) -> quot#(x, y, z))
     (div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s z) -> div#(x, s z))
     (pr#(x, s s y) -> if#(divides(s s y, x), x, s y), if#(false(), x, y) -> pr#(x, y))
     (divides#(y, x) -> div#(x, y), div#(x, y) -> quot#(x, y, y))
     (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> times#(y, z))
     (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> div#(x, times(y, z)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
     (div#(div(x, y), z) -> times#(y, z), times#(s x, y) -> plus#(y, times(x, y)))
     (div#(div(x, y), z) -> times#(y, z), times#(s x, y) -> times#(x, y))
     (divides#(y, x) -> eq#(x, times(div(x, y), y)), eq#(s x, s y) -> eq#(x, y))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(x, s y) -> p# s y)
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(x, s y) -> plus#(x, p s y))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> p# s x)
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(p s x, y))
     (pr#(x, s s y) -> divides#(s s y, x), divides#(y, x) -> times#(div(x, y), y))
     (pr#(x, s s y) -> divides#(s s y, x), divides#(y, x) -> div#(x, y))
     (pr#(x, s s y) -> divides#(s s y, x), divides#(y, x) -> eq#(x, times(div(x, y), y)))
     (plus#(s x, y) -> plus#(p s x, y), plus#(x, s y) -> p# s y)
     (plus#(s x, y) -> plus#(p s x, y), plus#(x, s y) -> plus#(x, p s y))
     (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> p# s x)
     (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> plus#(p s x, y))
     (prime# s s x -> pr#(s s x, s x), pr#(x, s s y) -> divides#(s s y, x))
     (prime# s s x -> pr#(s s x, s x), pr#(x, s s y) -> if#(divides(s s y, x), x, s y))}
    STATUS:
     arrows: 0.877500
     SCCS (5):
      Scc:
       {     pr#(x, s s y) -> if#(divides(s s y, x), x, s y),
        if#(false(), x, y) -> pr#(x, y)}
      Scc:
       {eq#(s x, s y) -> eq#(x, y)}
      Scc:
       {        div#(x, y) -> quot#(x, y, y),
        div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s z) -> div#(x, s z),
        quot#(s x, s y, z) -> quot#(x, y, z)}
      Scc:
       {times#(s x, y) -> times#(x, y)}
      Scc:
       {plus#(x, s y) -> plus#(x, p s y),
        plus#(s x, y) -> plus#(x, y),
        plus#(s x, y) -> plus#(p s x, y)}
      
      
      SCC (2):
       Strict:
        {     pr#(x, s s y) -> if#(divides(s s y, x), x, s y),
         if#(false(), x, y) -> pr#(x, y)}
       Weak:
       {            p 0() -> 0(),
                    p s x -> x,
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, p s y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
             plus(s x, y) -> s plus(p s x, y),
            times(0(), y) -> 0(),
            times(s x, y) -> plus(y, times(x, y)),
          times(s 0(), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
        quot(x, 0(), s z) -> s div(x, s z),
        quot(0(), s y, z) -> 0(),
        quot(s x, s y, z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
             eq(0(), s y) -> false(),
             eq(s x, 0()) -> false(),
             eq(s x, s y) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
             pr(x, s 0()) -> true(),
             pr(x, s s y) -> if(divides(s s y, x), x, s y),
              prime s s x -> pr(s s x, s x),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
       Open
      
      
      SCC (1):
       Strict:
        {eq#(s x, s y) -> eq#(x, y)}
       Weak:
       {            p 0() -> 0(),
                    p s x -> x,
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, p s y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
             plus(s x, y) -> s plus(p s x, y),
            times(0(), y) -> 0(),
            times(s x, y) -> plus(y, times(x, y)),
          times(s 0(), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
        quot(x, 0(), s z) -> s div(x, s z),
        quot(0(), s y, z) -> 0(),
        quot(s x, s y, z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
             eq(0(), s y) -> false(),
             eq(s x, 0()) -> false(),
             eq(s x, s y) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
             pr(x, s 0()) -> true(),
             pr(x, s s y) -> if(divides(s s y, x), x, s y),
              prime s s x -> pr(s s x, s x),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
       Open
      
      
      SCC (4):
       Strict:
        {        div#(x, y) -> quot#(x, y, y),
         div#(div(x, y), z) -> div#(x, times(y, z)),
         quot#(x, 0(), s z) -> div#(x, s z),
         quot#(s x, s y, z) -> quot#(x, y, z)}
       Weak:
       {            p 0() -> 0(),
                    p s x -> x,
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, p s y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
             plus(s x, y) -> s plus(p s x, y),
            times(0(), y) -> 0(),
            times(s x, y) -> plus(y, times(x, y)),
          times(s 0(), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
        quot(x, 0(), s z) -> s div(x, s z),
        quot(0(), s y, z) -> 0(),
        quot(s x, s y, z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
             eq(0(), s y) -> false(),
             eq(s x, 0()) -> false(),
             eq(s x, s y) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
             pr(x, s 0()) -> true(),
             pr(x, s s y) -> if(divides(s s y, x), x, s y),
              prime s s x -> pr(s s x, s x),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
       Open
      
      SCC (1):
       Strict:
        {times#(s x, y) -> times#(x, y)}
       Weak:
       {            p 0() -> 0(),
                    p s x -> x,
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, p s y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
             plus(s x, y) -> s plus(p s x, y),
            times(0(), y) -> 0(),
            times(s x, y) -> plus(y, times(x, y)),
          times(s 0(), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
        quot(x, 0(), s z) -> s div(x, s z),
        quot(0(), s y, z) -> 0(),
        quot(s x, s y, z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
             eq(0(), s y) -> false(),
             eq(s x, 0()) -> false(),
             eq(s x, s y) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
             pr(x, s 0()) -> true(),
             pr(x, s s y) -> if(divides(s s y, x), x, s y),
              prime s s x -> pr(s s x, s x),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
       Open
      
      SCC (3):
       Strict:
        {plus#(x, s y) -> plus#(x, p s y),
         plus#(s x, y) -> plus#(x, y),
         plus#(s x, y) -> plus#(p s x, y)}
       Weak:
       {            p 0() -> 0(),
                    p s x -> x,
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, p s y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
             plus(s x, y) -> s plus(p s x, y),
            times(0(), y) -> 0(),
            times(s x, y) -> plus(y, times(x, y)),
          times(s 0(), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
        quot(x, 0(), s z) -> s div(x, s z),
        quot(0(), s y, z) -> 0(),
        quot(s x, s y, z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
             eq(0(), s y) -> false(),
             eq(s x, 0()) -> false(),
             eq(s x, s y) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
             pr(x, s 0()) -> true(),
             pr(x, s s y) -> if(divides(s s y, x), x, s y),
              prime s s x -> pr(s s x, s x),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
       Open