YES
Time: 0.216495
TRS:
 {     plus(x, 0()) -> x,
       plus(0(), y) -> y,
       plus(s x, y) -> s plus(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#(s x, y) -> plus#(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:
  {     plus(x, 0()) -> x,
        plus(0(), y) -> y,
        plus(s x, y) -> s plus(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)}
  EDG:
   {(times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
    (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> div#(x, times(y, z)))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> times#(y, z))
    (divides#(y, x) -> div#(x, y), div#(x, y) -> quot#(x, y, y))
    (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))
    (pr#(x, s s y) -> if#(divides(s s y, x), x, s y), if#(false(), x, y) -> pr#(x, 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)))
    (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))
    (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))
    (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) -> 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#(s x, y) -> plus#(x, y))
    (div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s z) -> div#(x, s z))
    (div#(x, y) -> quot#(x, y, y), quot#(s x, s y, z) -> quot#(x, y, z))
    (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))
    (if#(false(), x, y) -> pr#(x, y), pr#(x, s s y) -> divides#(s s y, x))
    (if#(false(), x, y) -> pr#(x, y), pr#(x, s s y) -> if#(divides(s s y, x), x, s y))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))}
   STATUS:
    arrows: 0.878906
    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:
      {        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:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {times#(s x, y) -> times#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(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:
      {     plus(x, 0()) -> x,
            plus(0(), y) -> y,
            plus(s x, y) -> s plus(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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [quot](x0, x1, x2) = x0 + x1 + 1,
        
        [if](x0, x1, x2) = 0,
        
        [plus](x0, x1) = 0,
        
        [times](x0, x1) = x0 + 1,
        
        [div](x0, x1) = 0,
        
        [eq](x0, x1) = 0,
        
        [divides](x0, x1) = 0,
        
        [pr](x0, x1) = 0,
        
        [s](x0) = x0 + 1,
        
        [prime](x0) = 0,
        
        [0] = 0,
        
        [true] = 0,
        
        [false] = 0,
        
        [if#](x0, x1, x2) = x0,
        
        [pr#](x0, x1) = x0
       Strict:
        if#(false(), x, y) -> pr#(x, y)
        0 + 0x + 1y >= 0 + 0x + 1y
        pr#(x, s s y) -> if#(divides(s s y, x), x, s y)
        2 + 0x + 1y >= 1 + 0x + 1y
       Weak:
        if(false(), x, y) -> pr(x, y)
        0 + 0x + 0y >= 0 + 0x + 0y
        if(true(), x, y) -> false()
        0 + 0x + 0y >= 0
        prime s s x -> pr(s s x, s x)
        0 + 0x >= 0 + 0x
        pr(x, s s y) -> if(divides(s s y, x), x, s y)
        0 + 0x + 0y >= 0 + 0x + 0y
        pr(x, s 0()) -> true()
        0 + 0x >= 0
        divides(y, x) -> eq(x, times(div(x, y), y))
        0 + 0x + 0y >= 0 + 0x + 0y
        eq(s x, s y) -> eq(x, y)
        0 + 0x + 0y >= 0 + 0x + 0y
        eq(s x, 0()) -> false()
        0 + 0x >= 0
        eq(0(), s y) -> false()
        0 + 0y >= 0
        eq(0(), 0()) -> true()
        0 >= 0
        quot(s x, s y, z) -> quot(x, y, z)
        2 + 0x + 1y + 1z >= 1 + 0x + 1y + 1z
        quot(0(), s y, z) -> 0()
        2 + 1y + 1z >= 0
        quot(x, 0(), s z) -> s div(x, s z)
        2 + 0x + 1z >= 1 + 0x + 0z
        div(div(x, y), z) -> div(x, times(y, z))
        0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
        div(0(), y) -> 0()
        0 + 0y >= 0
        div(x, y) -> quot(x, y, y)
        0 + 0x + 0y >= 1 + 0x + 2y
        times(s 0(), y) -> y
        2 + 0y >= 1y
        times(s x, y) -> plus(y, times(x, y))
        2 + 1x + 0y >= 0 + 0x + 0y
        times(0(), y) -> 0()
        1 + 0y >= 0
        plus(s x, y) -> s plus(x, y)
        0 + 0x + 0y >= 1 + 0x + 0y
        plus(0(), y) -> y
        0 + 0y >= 1y
        plus(x, 0()) -> x
        0 + 0x >= 1x
      SCCS (0):
       
       
    
    
    
    
    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:
     {     plus(x, 0()) -> x,
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [quot](x0, x1, x2) = x0 + x1 + x2,
       
       [if](x0, x1, x2) = x0 + x1 + x2,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = x0,
       
       [div](x0, x1) = x0,
       
       [eq](x0, x1) = x0 + 1,
       
       [divides](x0, x1) = x0 + 1,
       
       [pr](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1,
       
       [prime](x0) = 0,
       
       [0] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [quot#](x0, x1, x2) = x0 + 1,
       
       [div#](x0, x1) = x0 + 1
      Strict:
       quot#(s x, s y, z) -> quot#(x, y, z)
       2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
       quot#(x, 0(), s z) -> div#(x, s z)
       1 + 1x + 0z >= 1 + 1x + 0z
       div#(div(x, y), z) -> div#(x, times(y, z))
       1 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
       div#(x, y) -> quot#(x, y, y)
       1 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       if(false(), x, y) -> pr(x, y)
       0 + 1x + 1y >= 0 + 1x + 1y
       if(true(), x, y) -> false()
       0 + 1x + 1y >= 0
       prime s s x -> pr(s s x, s x)
       0 + 0x >= 3 + 2x
       pr(x, s s y) -> if(divides(s s y, x), x, s y)
       2 + 1x + 1y >= 2 + 2x + 1y
       pr(x, s 0()) -> true()
       2 + 1x >= 0
       divides(y, x) -> eq(x, times(div(x, y), y))
       1 + 1x + 0y >= 1 + 1x + 0y
       eq(s x, s y) -> eq(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
       eq(s x, 0()) -> false()
       2 + 1x >= 0
       eq(0(), s y) -> false()
       2 + 0y >= 0
       eq(0(), 0()) -> true()
       2 >= 0
       quot(s x, s y, z) -> quot(x, y, z)
       2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       quot(0(), s y, z) -> 0()
       2 + 1y + 1z >= 1
       quot(x, 0(), s z) -> s div(x, s z)
       2 + 1x + 1z >= 1 + 1x + 0z
       div(div(x, y), z) -> div(x, times(y, z))
       0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
       div(0(), y) -> 0()
       1 + 0y >= 1
       div(x, y) -> quot(x, y, y)
       0 + 1x + 0y >= 0 + 1x + 2y
       times(s 0(), y) -> y
       0 + 1y >= 1y
       times(s x, y) -> plus(y, times(x, y))
       0 + 0x + 1y >= 1 + 0x + 2y
       times(0(), y) -> 0()
       0 + 1y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 1y >= 2 + 1x + 1y
       plus(0(), y) -> y
       2 + 1y >= 1y
       plus(x, 0()) -> x
       2 + 1x >= 1x
     SCCS (1):
      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)}
      
      SCC (3):
       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)}
       Weak:
       {     plus(x, 0()) -> x,
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [quot](x0, x1, x2) = 0,
         
         [if](x0, x1, x2) = x0 + x1 + 1,
         
         [plus](x0, x1) = 0,
         
         [times](x0, x1) = x0 + 1,
         
         [div](x0, x1) = x0 + 1,
         
         [eq](x0, x1) = x0 + 1,
         
         [divides](x0, x1) = x0 + x1 + 1,
         
         [pr](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [prime](x0) = 0,
         
         [0] = 1,
         
         [true] = 1,
         
         [false] = 1,
         
         [quot#](x0, x1, x2) = x0,
         
         [div#](x0, x1) = x0
        Strict:
         quot#(x, 0(), s z) -> div#(x, s z)
         0 + 1x + 0z >= 0 + 1x + 0z
         div#(div(x, y), z) -> div#(x, times(y, z))
         1 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
         div#(x, y) -> quot#(x, y, y)
         0 + 1x + 0y >= 0 + 1x + 0y
        Weak:
         if(false(), x, y) -> pr(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
         if(true(), x, y) -> false()
         2 + 1x + 0y >= 1
         prime s s x -> pr(s s x, s x)
         0 + 0x >= 3 + 1x
         pr(x, s s y) -> if(divides(s s y, x), x, s y)
         1 + 1x + 0y >= 4 + 2x + 1y
         pr(x, s 0()) -> true()
         1 + 1x >= 1
         divides(y, x) -> eq(x, times(div(x, y), y))
         1 + 1x + 1y >= 1 + 1x + 0y
         eq(s x, s y) -> eq(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
         eq(s x, 0()) -> false()
         2 + 1x >= 1
         eq(0(), s y) -> false()
         2 + 0y >= 1
         eq(0(), 0()) -> true()
         2 >= 1
         quot(s x, s y, z) -> quot(x, y, z)
         0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
         quot(0(), s y, z) -> 0()
         0 + 0y + 0z >= 1
         quot(x, 0(), s z) -> s div(x, s z)
         0 + 0x + 0z >= 2 + 1x + 0z
         div(div(x, y), z) -> div(x, times(y, z))
         2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
         div(0(), y) -> 0()
         2 + 0y >= 1
         div(x, y) -> quot(x, y, y)
         1 + 1x + 0y >= 0 + 0x + 0y
         times(s 0(), y) -> y
         3 + 0y >= 1y
         times(s x, y) -> plus(y, times(x, y))
         2 + 1x + 0y >= 0 + 0x + 0y
         times(0(), y) -> 0()
         2 + 0y >= 1
         plus(s x, y) -> s plus(x, y)
         0 + 0x + 0y >= 1 + 0x + 0y
         plus(0(), y) -> y
         0 + 0y >= 1y
         plus(x, 0()) -> x
         0 + 0x >= 1x
       SCCS (1):
        Scc:
         {        div#(x, y) -> quot#(x, y, y),
          quot#(x, 0(), s z) -> div#(x, s z)}
        
        SCC (2):
         Strict:
          {        div#(x, y) -> quot#(x, y, y),
           quot#(x, 0(), s z) -> div#(x, s z)}
         Weak:
         {     plus(x, 0()) -> x,
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(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)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [quot](x0, x1, x2) = 0,
           
           [if](x0, x1, x2) = x0 + x1 + 1,
           
           [plus](x0, x1) = x0 + x1 + 1,
           
           [times](x0, x1) = x0 + x1 + 1,
           
           [div](x0, x1) = x0 + x1 + 1,
           
           [eq](x0, x1) = x0 + 1,
           
           [divides](x0, x1) = x0 + 1,
           
           [pr](x0, x1) = 0,
           
           [s](x0) = 0,
           
           [prime](x0) = 0,
           
           [0] = 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [quot#](x0, x1, x2) = x0 + 1,
           
           [div#](x0, x1) = x0 + 1
          Strict:
           quot#(x, 0(), s z) -> div#(x, s z)
           2 + 0x + 0z >= 1 + 0x + 0z
           div#(x, y) -> quot#(x, y, y)
           1 + 0x + 1y >= 1 + 0x + 1y
          Weak:
           if(false(), x, y) -> pr(x, y)
           2 + 1x + 0y >= 0 + 0x + 0y
           if(true(), x, y) -> false()
           2 + 1x + 0y >= 1
           prime s s x -> pr(s s x, s x)
           0 + 0x >= 0 + 0x
           pr(x, s s y) -> if(divides(s s y, x), x, s y)
           0 + 0x + 0y >= 2 + 2x + 0y
           pr(x, s 0()) -> true()
           0 + 0x >= 1
           divides(y, x) -> eq(x, times(div(x, y), y))
           1 + 1x + 0y >= 1 + 1x + 0y
           eq(s x, s y) -> eq(x, y)
           1 + 0x + 0y >= 1 + 1x + 0y
           eq(s x, 0()) -> false()
           1 + 0x >= 1
           eq(0(), s y) -> false()
           2 + 0y >= 1
           eq(0(), 0()) -> true()
           2 >= 1
           quot(s x, s y, z) -> quot(x, y, z)
           0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
           quot(0(), s y, z) -> 0()
           0 + 0y + 0z >= 1
           quot(x, 0(), s z) -> s div(x, s z)
           0 + 0x + 0z >= 0 + 0x + 0z
           div(div(x, y), z) -> div(x, times(y, z))
           2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
           div(0(), y) -> 0()
           2 + 1y >= 1
           div(x, y) -> quot(x, y, y)
           1 + 1x + 1y >= 0 + 0x + 0y
           times(s 0(), y) -> y
           1 + 1y >= 1y
           times(s x, y) -> plus(y, times(x, y))
           1 + 0x + 1y >= 2 + 1x + 2y
           times(0(), y) -> 0()
           2 + 1y >= 1
           plus(s x, y) -> s plus(x, y)
           1 + 0x + 1y >= 0 + 0x + 0y
           plus(0(), y) -> y
           2 + 1y >= 1y
           plus(x, 0()) -> x
           2 + 1x >= 1x
         SCCS (0):
          
          
   
   SCC (1):
    Strict:
     {eq#(s x, s y) -> eq#(x, y)}
    Weak:
    {     plus(x, 0()) -> x,
          plus(0(), y) -> y,
          plus(s x, y) -> s plus(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)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [quot](x0, x1, x2) = x0 + x1 + x2,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [plus](x0, x1) = x0 + x1 + 1,
      
      [times](x0, x1) = x0 + x1 + 1,
      
      [div](x0, x1) = x0 + x1 + 1,
      
      [eq](x0, x1) = x0 + 1,
      
      [divides](x0, x1) = x0 + x1,
      
      [pr](x0, x1) = x0,
      
      [s](x0) = x0 + 1,
      
      [prime](x0) = 0,
      
      [0] = 1,
      
      [true] = 0,
      
      [false] = 0,
      
      [eq#](x0, x1) = x0
     Strict:
      eq#(s x, s y) -> eq#(x, y)
      1 + 0x + 1y >= 0 + 0x + 1y
     Weak:
      if(false(), x, y) -> pr(x, y)
      0 + 1x + 1y >= 0 + 1x + 0y
      if(true(), x, y) -> false()
      0 + 1x + 1y >= 0
      prime s s x -> pr(s s x, s x)
      0 + 0x >= 2 + 1x
      pr(x, s s y) -> if(divides(s s y, x), x, s y)
      0 + 1x + 0y >= 3 + 2x + 2y
      pr(x, s 0()) -> true()
      0 + 1x >= 0
      divides(y, x) -> eq(x, times(div(x, y), y))
      0 + 1x + 1y >= 1 + 1x + 0y
      eq(s x, s y) -> eq(x, y)
      2 + 1x + 0y >= 1 + 1x + 0y
      eq(s x, 0()) -> false()
      2 + 1x >= 0
      eq(0(), s y) -> false()
      2 + 0y >= 0
      eq(0(), 0()) -> true()
      2 >= 0
      quot(s x, s y, z) -> quot(x, y, z)
      2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
      quot(0(), s y, z) -> 0()
      2 + 1y + 1z >= 1
      quot(x, 0(), s z) -> s div(x, s z)
      2 + 1x + 1z >= 3 + 1x + 1z
      div(div(x, y), z) -> div(x, times(y, z))
      2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
      div(0(), y) -> 0()
      2 + 1y >= 1
      div(x, y) -> quot(x, y, y)
      1 + 1x + 1y >= 0 + 1x + 2y
      times(s 0(), y) -> y
      3 + 1y >= 1y
      times(s x, y) -> plus(y, times(x, y))
      2 + 1x + 1y >= 2 + 1x + 2y
      times(0(), y) -> 0()
      2 + 1y >= 1
      plus(s x, y) -> s plus(x, y)
      2 + 1x + 1y >= 2 + 1x + 1y
      plus(0(), y) -> y
      2 + 1y >= 1y
      plus(x, 0()) -> x
      2 + 1x >= 1x
    Qed
  SCC (1):
   Strict:
    {times#(s x, y) -> times#(x, y)}
   Weak:
   {     plus(x, 0()) -> x,
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(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)}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [quot](x0, x1, x2) = x0 + x1 + x2,
     
     [if](x0, x1, x2) = x0 + x1 + 1,
     
     [plus](x0, x1) = x0 + x1 + 1,
     
     [times](x0, x1) = x0 + x1 + 1,
     
     [div](x0, x1) = x0 + x1 + 1,
     
     [eq](x0, x1) = x0 + 1,
     
     [divides](x0, x1) = x0 + 1,
     
     [pr](x0, x1) = x0,
     
     [s](x0) = x0 + 1,
     
     [prime](x0) = 0,
     
     [0] = 1,
     
     [true] = 1,
     
     [false] = 1,
     
     [times#](x0, x1) = x0
    Strict:
     times#(s x, y) -> times#(x, y)
     1 + 1x + 0y >= 0 + 1x + 0y
    Weak:
     if(false(), x, y) -> pr(x, y)
     2 + 0x + 1y >= 0 + 1x + 0y
     if(true(), x, y) -> false()
     2 + 0x + 1y >= 1
     prime s s x -> pr(s s x, s x)
     0 + 0x >= 2 + 1x
     pr(x, s s y) -> if(divides(s s y, x), x, s y)
     0 + 1x + 0y >= 5 + 0x + 2y
     pr(x, s 0()) -> true()
     0 + 1x >= 1
     divides(y, x) -> eq(x, times(div(x, y), y))
     1 + 0x + 1y >= 1 + 1x + 0y
     eq(s x, s y) -> eq(x, y)
     2 + 1x + 0y >= 1 + 1x + 0y
     eq(s x, 0()) -> false()
     2 + 1x >= 1
     eq(0(), s y) -> false()
     2 + 0y >= 1
     eq(0(), 0()) -> true()
     2 >= 1
     quot(s x, s y, z) -> quot(x, y, z)
     2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
     quot(0(), s y, z) -> 0()
     2 + 1y + 1z >= 1
     quot(x, 0(), s z) -> s div(x, s z)
     2 + 1x + 1z >= 3 + 1x + 1z
     div(div(x, y), z) -> div(x, times(y, z))
     2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
     div(0(), y) -> 0()
     2 + 1y >= 1
     div(x, y) -> quot(x, y, y)
     1 + 1x + 1y >= 0 + 1x + 2y
     times(s 0(), y) -> y
     3 + 1y >= 1y
     times(s x, y) -> plus(y, times(x, y))
     2 + 1x + 1y >= 2 + 1x + 2y
     times(0(), y) -> 0()
     2 + 1y >= 1
     plus(s x, y) -> s plus(x, y)
     2 + 1x + 1y >= 2 + 1x + 1y
     plus(0(), y) -> y
     2 + 1y >= 1y
     plus(x, 0()) -> x
     2 + 1x >= 1x
   Qed
  
  SCC (1):
   Strict:
    {plus#(s x, y) -> plus#(x, y)}
   Weak:
   {     plus(x, 0()) -> x,
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(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)}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [quot](x0, x1, x2) = x0 + x1 + x2,
     
     [if](x0, x1, x2) = x0 + x1 + 1,
     
     [plus](x0, x1) = x0 + x1 + 1,
     
     [times](x0, x1) = x0 + x1 + 1,
     
     [div](x0, x1) = x0 + x1 + 1,
     
     [eq](x0, x1) = x0 + 1,
     
     [divides](x0, x1) = x0 + 1,
     
     [pr](x0, x1) = x0,
     
     [s](x0) = x0 + 1,
     
     [prime](x0) = 0,
     
     [0] = 1,
     
     [true] = 1,
     
     [false] = 1,
     
     [plus#](x0, x1) = x0
    Strict:
     plus#(s x, y) -> plus#(x, y)
     1 + 1x + 0y >= 0 + 1x + 0y
    Weak:
     if(false(), x, y) -> pr(x, y)
     2 + 0x + 1y >= 0 + 1x + 0y
     if(true(), x, y) -> false()
     2 + 0x + 1y >= 1
     prime s s x -> pr(s s x, s x)
     0 + 0x >= 2 + 1x
     pr(x, s s y) -> if(divides(s s y, x), x, s y)
     0 + 1x + 0y >= 5 + 0x + 2y
     pr(x, s 0()) -> true()
     0 + 1x >= 1
     divides(y, x) -> eq(x, times(div(x, y), y))
     1 + 0x + 1y >= 1 + 1x + 0y
     eq(s x, s y) -> eq(x, y)
     2 + 1x + 0y >= 1 + 1x + 0y
     eq(s x, 0()) -> false()
     2 + 1x >= 1
     eq(0(), s y) -> false()
     2 + 0y >= 1
     eq(0(), 0()) -> true()
     2 >= 1
     quot(s x, s y, z) -> quot(x, y, z)
     2 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
     quot(0(), s y, z) -> 0()
     2 + 1y + 1z >= 1
     quot(x, 0(), s z) -> s div(x, s z)
     2 + 1x + 1z >= 3 + 1x + 1z
     div(div(x, y), z) -> div(x, times(y, z))
     2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
     div(0(), y) -> 0()
     2 + 1y >= 1
     div(x, y) -> quot(x, y, y)
     1 + 1x + 1y >= 0 + 1x + 2y
     times(s 0(), y) -> y
     3 + 1y >= 1y
     times(s x, y) -> plus(y, times(x, y))
     2 + 1x + 1y >= 2 + 1x + 2y
     times(0(), y) -> 0()
     2 + 1y >= 1
     plus(s x, y) -> s plus(x, y)
     2 + 1x + 1y >= 2 + 1x + 1y
     plus(0(), y) -> y
     2 + 1y >= 1y
     plus(x, 0()) -> x
     2 + 1x >= 1x
   Qed