MAYBE
TRS:
 {      gt(s(x), s(y)) -> gt(x, y),
         gt(s(x), 0()) -> true(),
            gt(0(), y) -> false(),
    div(s(x), s(y), z) -> div(x, y, z),
  div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)),
     div(0(), s(x), z) -> false(),
      div(0(), 0(), z) -> true(),
         divides(x, y) -> div(x, y, y),
            test(x, y) -> if1(gt(x, y), x, y),
              prime(x) -> test(x, s(s(0()))),
     if1(true(), x, y) -> if2(divides(x, y), x, y),
    if1(false(), x, y) -> true(),
     if2(true(), x, y) -> false(),
    if2(false(), x, y) -> test(x, s(y))}
 DP:
  Strict:
   {      gt#(s(x), s(y)) -> gt#(x, y),
      div#(s(x), s(y), z) -> div#(x, y, z),
    div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z)),
           divides#(x, y) -> div#(x, y, y),
              test#(x, y) -> gt#(x, y),
              test#(x, y) -> if1#(gt(x, y), x, y),
                prime#(x) -> test#(x, s(s(0()))),
       if1#(true(), x, y) -> divides#(x, y),
       if1#(true(), x, y) -> if2#(divides(x, y), x, y),
      if2#(false(), x, y) -> test#(x, s(y))}
  Weak:
  {      gt(s(x), s(y)) -> gt(x, y),
          gt(s(x), 0()) -> true(),
             gt(0(), y) -> false(),
     div(s(x), s(y), z) -> div(x, y, z),
   div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)),
      div(0(), s(x), z) -> false(),
       div(0(), 0(), z) -> true(),
          divides(x, y) -> div(x, y, y),
             test(x, y) -> if1(gt(x, y), x, y),
               prime(x) -> test(x, s(s(0()))),
      if1(true(), x, y) -> if2(divides(x, y), x, y),
     if1(false(), x, y) -> true(),
      if2(true(), x, y) -> false(),
     if2(false(), x, y) -> test(x, s(y))}
  EDG:
   {(if2#(false(), x, y) -> test#(x, s(y)), test#(x, y) -> if1#(gt(x, y), x, y))
    (if2#(false(), x, y) -> test#(x, s(y)), test#(x, y) -> gt#(x, y))
    (div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z)), div#(s(x), s(y), z) -> div#(x, y, z))
    (if1#(true(), x, y) -> divides#(x, y), divides#(x, y) -> div#(x, y, y))
    (test#(x, y) -> if1#(gt(x, y), x, y), if1#(true(), x, y) -> if2#(divides(x, y), x, y))
    (test#(x, y) -> if1#(gt(x, y), x, y), if1#(true(), x, y) -> divides#(x, y))
    (div#(s(x), s(y), z) -> div#(x, y, z), div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z)))
    (div#(s(x), s(y), z) -> div#(x, y, z), div#(s(x), s(y), z) -> div#(x, y, z))
    (if1#(true(), x, y) -> if2#(divides(x, y), x, y), if2#(false(), x, y) -> test#(x, s(y)))
    (divides#(x, y) -> div#(x, y, y), div#(s(x), s(y), z) -> div#(x, y, z))
    (test#(x, y) -> gt#(x, y), gt#(s(x), s(y)) -> gt#(x, y))
    (gt#(s(x), s(y)) -> gt#(x, y), gt#(s(x), s(y)) -> gt#(x, y))
    (prime#(x) -> test#(x, s(s(0()))), test#(x, y) -> gt#(x, y))
    (prime#(x) -> test#(x, s(s(0()))), test#(x, y) -> if1#(gt(x, y), x, y))}
   SCCS:
    Scc:
     {        test#(x, y) -> if1#(gt(x, y), x, y),
       if1#(true(), x, y) -> if2#(divides(x, y), x, y),
      if2#(false(), x, y) -> test#(x, s(y))}
    Scc:
     {  div#(s(x), s(y), z) -> div#(x, y, z),
      div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z))}
    Scc:
     {gt#(s(x), s(y)) -> gt#(x, y)}
    SCC:
     Strict:
      {        test#(x, y) -> if1#(gt(x, y), x, y),
        if1#(true(), x, y) -> if2#(divides(x, y), x, y),
       if2#(false(), x, y) -> test#(x, s(y))}
     Weak:
     {      gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), 0()) -> true(),
                gt(0(), y) -> false(),
        div(s(x), s(y), z) -> div(x, y, z),
      div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)),
         div(0(), s(x), z) -> false(),
          div(0(), 0(), z) -> true(),
             divides(x, y) -> div(x, y, y),
                test(x, y) -> if1(gt(x, y), x, y),
                  prime(x) -> test(x, s(s(0()))),
         if1(true(), x, y) -> if2(divides(x, y), x, y),
        if1(false(), x, y) -> true(),
         if2(true(), x, y) -> false(),
        if2(false(), x, y) -> test(x, s(y))}
     Fail
    SCC:
     Strict:
      {  div#(s(x), s(y), z) -> div#(x, y, z),
       div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z))}
     Weak:
     {      gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), 0()) -> true(),
                gt(0(), y) -> false(),
        div(s(x), s(y), z) -> div(x, y, z),
      div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)),
         div(0(), s(x), z) -> false(),
          div(0(), 0(), z) -> true(),
             divides(x, y) -> div(x, y, y),
                test(x, y) -> if1(gt(x, y), x, y),
                  prime(x) -> test(x, s(s(0()))),
         if1(true(), x, y) -> if2(divides(x, y), x, y),
        if1(false(), x, y) -> true(),
         if2(true(), x, y) -> false(),
        if2(false(), x, y) -> test(x, s(y))}
     SPSC:
      Simple Projection:
       pi(div#) = 0
      Strict:
       {div#(s(x), 0(), s(z)) -> div#(s(x), s(z), s(z))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {gt#(s(x), s(y)) -> gt#(x, y)}
     Weak:
     {      gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), 0()) -> true(),
                gt(0(), y) -> false(),
        div(s(x), s(y), z) -> div(x, y, z),
      div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)),
         div(0(), s(x), z) -> false(),
          div(0(), 0(), z) -> true(),
             divides(x, y) -> div(x, y, y),
                test(x, y) -> if1(gt(x, y), x, y),
                  prime(x) -> test(x, s(s(0()))),
         if1(true(), x, y) -> if2(divides(x, y), x, y),
        if1(false(), x, y) -> true(),
         if2(true(), x, y) -> false(),
        if2(false(), x, y) -> test(x, s(y))}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed