MAYBE
Time: 1.010088
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(zero y, z)),
     quot(x, 0(), s z) -> s div(x, s z),
     quot(s x, s y, z) -> quot(x, y, z),
  quot(zero y, s y, z) -> 0(),
              zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
      zero times(x, x) -> x,
        zero div(x, x) -> x,
    zero quot(x, x, x) -> x,
    zero divides(x, x) -> x,
          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#(zero y, z),
    div#(div(x, y), z) -> div#(x, times(zero y, z)),
    div#(div(x, y), z) -> zero# y,
    quot#(x, 0(), s z) -> div#(x, s z),
    quot#(s x, s y, z) -> quot#(x, y, z),
             zero# s x -> plus#(0(), zero 0()),
             zero# s x -> plus#(zero 0(), 0()),
             zero# s x -> zero# 0(),
             zero# s x -> eq#(x, s 0()),
             zero# s x -> if#(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
         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(zero y, z)),
      quot(x, 0(), s z) -> s div(x, s z),
      quot(s x, s y, z) -> quot(x, y, z),
   quot(zero y, s y, z) -> 0(),
               zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
       zero times(x, x) -> x,
         zero div(x, x) -> x,
     zero quot(x, x, x) -> x,
     zero divides(x, x) -> x,
           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)}
  EDG:
   {(pr#(x, s s y) -> divides#(s s y, x), divides#(y, x) -> eq#(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) -> times#(div(x, y), y))
    (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> plus#(p s x, y))
    (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) -> p# s x)
    (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#(x, s y) -> p# s y)
    (div#(div(x, y), z) -> times#(zero y, z), times#(s x, y) -> times#(x, y))
    (div#(div(x, y), z) -> times#(zero y, z), times#(s x, y) -> plus#(y, times(x, y)))
    (zero# s x -> if#(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())), if#(false(), x, y) -> pr#(x, 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))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> zero# y)
    (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> div#(x, times(zero y, z)))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> times#(zero y, z))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(x, y) -> quot#(x, y, y))
    (div#(div(x, y), z) -> div#(x, times(zero y, z)), div#(div(x, y), z) -> zero# y)
    (div#(div(x, y), z) -> div#(x, times(zero y, z)), div#(div(x, y), z) -> div#(x, times(zero y, z)))
    (div#(div(x, y), z) -> div#(x, times(zero y, z)), div#(div(x, y), z) -> times#(zero y, z))
    (div#(div(x, y), z) -> div#(x, times(zero y, z)), div#(x, y) -> quot#(x, y, 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))
    (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))
    (div#(div(x, y), z) -> zero# y, zero# s x -> plus#(0(), zero 0()))
    (div#(div(x, y), z) -> zero# y, zero# s x -> plus#(zero 0(), 0()))
    (div#(div(x, y), z) -> zero# y, zero# s x -> zero# 0())
    (div#(div(x, y), z) -> zero# y, zero# s x -> eq#(x, s 0()))
    (div#(div(x, y), z) -> zero# y, zero# s x -> if#(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())))
    (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#(zero y, z))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> div#(x, times(zero y, z)))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> zero# y)
    (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))
    (quot#(s x, s y, z) -> quot#(x, y, z), quot#(x, 0(), s z) -> div#(x, s z))
    (quot#(s x, s y, z) -> quot#(x, y, z), quot#(s x, s y, z) -> quot#(x, y, z))
    (divides#(y, x) -> times#(div(x, y), y), times#(s x, y) -> plus#(y, times(x, y)))
    (divides#(y, x) -> times#(div(x, y), y), times#(s x, y) -> times#(x, y))
    (zero# s x -> eq#(x, s 0()), eq#(s x, s y) -> eq#(x, y))
    (plus#(x, s y) -> plus#(x, p s y), plus#(x, s y) -> 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) -> plus#(x, p s y), plus#(s x, y) -> p# s x)
    (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) -> plus#(p s x, y))}
   STATUS:
    arrows: 0.912722
    SCCS (4):
     Scc:
      {        div#(x, y) -> quot#(x, y, y),
       div#(div(x, y), z) -> div#(x, times(zero y, z)),
       div#(div(x, y), z) -> zero# y,
       quot#(x, 0(), s z) -> div#(x, s z),
       quot#(s x, s y, z) -> quot#(x, y, z),
                zero# s x -> if#(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
           divides#(y, x) -> div#(x, 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),
       if#(false(), x, y) -> pr#(x, y)}
     Scc:
      {times#(s x, y) -> times#(x, y)}
     Scc:
      {eq#(s x, s y) -> eq#(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 (10):
      Strict:
       {        div#(x, y) -> quot#(x, y, y),
        div#(div(x, y), z) -> div#(x, times(zero y, z)),
        div#(div(x, y), z) -> zero# y,
        quot#(x, 0(), s z) -> div#(x, s z),
        quot#(s x, s y, z) -> quot#(x, y, z),
                 zero# s x -> if#(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
            divides#(y, x) -> div#(x, 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),
        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(zero y, z)),
          quot(x, 0(), s z) -> s div(x, s z),
          quot(s x, s y, z) -> quot(x, y, z),
       quot(zero y, s y, z) -> 0(),
                   zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
           zero times(x, x) -> x,
             zero div(x, x) -> x,
         zero quot(x, x, x) -> x,
         zero divides(x, x) -> x,
               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(zero y, z)),
          quot(x, 0(), s z) -> s div(x, s z),
          quot(s x, s y, z) -> quot(x, y, z),
       quot(zero y, s y, z) -> 0(),
                   zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
           zero times(x, x) -> x,
             zero div(x, x) -> x,
         zero quot(x, x, x) -> x,
         zero divides(x, x) -> x,
               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(zero y, z)),
          quot(x, 0(), s z) -> s div(x, s z),
          quot(s x, s y, z) -> quot(x, y, z),
       quot(zero y, s y, z) -> 0(),
                   zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
           zero times(x, x) -> x,
             zero div(x, x) -> x,
         zero quot(x, x, x) -> x,
         zero divides(x, x) -> x,
               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(zero y, z)),
          quot(x, 0(), s z) -> s div(x, s z),
          quot(s x, s y, z) -> quot(x, y, z),
       quot(zero y, s y, z) -> 0(),
                   zero s x -> if(eq(x, s 0()), plus(zero 0(), 0()), s plus(0(), zero 0())),
           zero times(x, x) -> x,
             zero div(x, x) -> x,
         zero quot(x, x, x) -> x,
         zero divides(x, x) -> x,
               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