MAYBE

Problem:
 gt(s(x),0()) -> true()
 gt(0(),y) -> false()
 gt(s(x),s(y)) -> gt(x,y)
 divides(x,y) -> div(x,y,y)
 div(0(),0(),z) -> true()
 div(0(),s(x),z) -> false()
 div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
 div(s(x),s(y),z) -> div(x,y,z)
 prime(x) -> test(x,s(s(0())))
 test(x,y) -> if1(gt(x,y),x,y)
 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))

Proof:
 DP Processor:
  DPs:
   gt#(s(x),s(y)) -> gt#(x,y)
   divides#(x,y) -> div#(x,y,y)
   div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
   div#(s(x),s(y),z) -> div#(x,y,z)
   prime#(x) -> test#(x,s(s(0())))
   test#(x,y) -> gt#(x,y)
   test#(x,y) -> if1#(gt(x,y),x,y)
   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))
  TRS:
   gt(s(x),0()) -> true()
   gt(0(),y) -> false()
   gt(s(x),s(y)) -> gt(x,y)
   divides(x,y) -> div(x,y,y)
   div(0(),0(),z) -> true()
   div(0(),s(x),z) -> false()
   div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
   div(s(x),s(y),z) -> div(x,y,z)
   prime(x) -> test(x,s(s(0())))
   test(x,y) -> if1(gt(x,y),x,y)
   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))
  TDG Processor:
   DPs:
    gt#(s(x),s(y)) -> gt#(x,y)
    divides#(x,y) -> div#(x,y,y)
    div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
    div#(s(x),s(y),z) -> div#(x,y,z)
    prime#(x) -> test#(x,s(s(0())))
    test#(x,y) -> gt#(x,y)
    test#(x,y) -> if1#(gt(x,y),x,y)
    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))
   TRS:
    gt(s(x),0()) -> true()
    gt(0(),y) -> false()
    gt(s(x),s(y)) -> gt(x,y)
    divides(x,y) -> div(x,y,y)
    div(0(),0(),z) -> true()
    div(0(),s(x),z) -> false()
    div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
    div(s(x),s(y),z) -> div(x,y,z)
    prime(x) -> test(x,s(s(0())))
    test(x,y) -> if1(gt(x,y),x,y)
    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))
   graph:
    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)
    if1#(true(),x,y) -> if2#(divides(x,y),x,y) ->
    if2#(false(),x,y) -> test#(x,s(y))
    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)
    test#(x,y) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    prime#(x) -> test#(x,s(s(0()))) ->
    test#(x,y) -> if1#(gt(x,y),x,y)
    prime#(x) -> test#(x,s(s(0()))) ->
    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)
    div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(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)
    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) -> div#(s(x),s(y),z) -> div#(x,y,z)
    divides#(x,y) -> div#(x,y,y) ->
    div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
    gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
   EDG Processor:
    DPs:
     gt#(s(x),s(y)) -> gt#(x,y)
     divides#(x,y) -> div#(x,y,y)
     div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
     div#(s(x),s(y),z) -> div#(x,y,z)
     prime#(x) -> test#(x,s(s(0())))
     test#(x,y) -> gt#(x,y)
     test#(x,y) -> if1#(gt(x,y),x,y)
     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))
    TRS:
     gt(s(x),0()) -> true()
     gt(0(),y) -> false()
     gt(s(x),s(y)) -> gt(x,y)
     divides(x,y) -> div(x,y,y)
     div(0(),0(),z) -> true()
     div(0(),s(x),z) -> false()
     div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
     div(s(x),s(y),z) -> div(x,y,z)
     prime(x) -> test(x,s(s(0())))
     test(x,y) -> if1(gt(x,y),x,y)
     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))
    graph:
     if2#(false(),x,y) -> test#(x,s(y)) -> test#(x,y) -> gt#(x,y)
     if2#(false(),x,y) -> test#(x,s(y)) ->
     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))
     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) -> divides#(x,y)
     test#(x,y) -> if1#(gt(x,y),x,y) ->
     if1#(true(),x,y) -> if2#(divides(x,y),x,y)
     test#(x,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)
     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) ->
     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)
     divides#(x,y) -> div#(x,y,y) -> div#(s(x),s(y),z) -> div#(x,y,z)
     gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    SCC Processor:
     #sccs: 3
     #rules: 6
     #arcs: 14/100
     DPs:
      if2#(false(),x,y) -> test#(x,s(y))
      test#(x,y) -> if1#(gt(x,y),x,y)
      if1#(true(),x,y) -> if2#(divides(x,y),x,y)
     TRS:
      gt(s(x),0()) -> true()
      gt(0(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      divides(x,y) -> div(x,y,y)
      div(0(),0(),z) -> true()
      div(0(),s(x),z) -> false()
      div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
      div(s(x),s(y),z) -> div(x,y,z)
      prime(x) -> test(x,s(s(0())))
      test(x,y) -> if1(gt(x,y),x,y)
      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))
     Open
     
     DPs:
      gt#(s(x),s(y)) -> gt#(x,y)
     TRS:
      gt(s(x),0()) -> true()
      gt(0(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      divides(x,y) -> div(x,y,y)
      div(0(),0(),z) -> true()
      div(0(),s(x),z) -> false()
      div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
      div(s(x),s(y),z) -> div(x,y,z)
      prime(x) -> test(x,s(s(0())))
      test(x,y) -> if1(gt(x,y),x,y)
      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))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [gt#](x0, x1) = x0 + 2x1,
       
       [if2](x0, x1, x2) = 2x1,
       
       [if1](x0, x1, x2) = 2x1,
       
       [test](x0, x1) = 2x0,
       
       [prime](x0) = 3x0 + 1,
       
       [div](x0, x1, x2) = 4x2,
       
       [divides](x0, x1) = 5x1 + 4,
       
       [false] = 0,
       
       [true] = 0,
       
       [gt](x0, x1) = 7x0 + 2x1 + 5,
       
       [0] = 0,
       
       [s](x0) = 2x0 + 2
      orientation:
       gt#(s(x),s(y)) = 2x + 4y + 6 >= x + 2y = gt#(x,y)
       
       gt(s(x),0()) = 14x + 19 >= 0 = true()
       
       gt(0(),y) = 2y + 5 >= 0 = false()
       
       gt(s(x),s(y)) = 14x + 4y + 23 >= 7x + 2y + 5 = gt(x,y)
       
       divides(x,y) = 5y + 4 >= 4y = div(x,y,y)
       
       div(0(),0(),z) = 4z >= 0 = true()
       
       div(0(),s(x),z) = 4z >= 0 = false()
       
       div(s(x),0(),s(z)) = 8z + 8 >= 8z + 8 = div(s(x),s(z),s(z))
       
       div(s(x),s(y),z) = 4z >= 4z = div(x,y,z)
       
       prime(x) = 3x + 1 >= 2x = test(x,s(s(0())))
       
       test(x,y) = 2x >= 2x = if1(gt(x,y),x,y)
       
       if1(true(),x,y) = 2x >= 2x = if2(divides(x,y),x,y)
       
       if1(false(),x,y) = 2x >= 0 = true()
       
       if2(true(),x,y) = 2x >= 0 = false()
       
       if2(false(),x,y) = 2x >= 2x = test(x,s(y))
      problem:
       DPs:
        
       TRS:
        gt(s(x),0()) -> true()
        gt(0(),y) -> false()
        gt(s(x),s(y)) -> gt(x,y)
        divides(x,y) -> div(x,y,y)
        div(0(),0(),z) -> true()
        div(0(),s(x),z) -> false()
        div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
        div(s(x),s(y),z) -> div(x,y,z)
        prime(x) -> test(x,s(s(0())))
        test(x,y) -> if1(gt(x,y),x,y)
        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))
      Qed
     
     DPs:
      div#(s(x),s(y),z) -> div#(x,y,z)
      div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
     TRS:
      gt(s(x),0()) -> true()
      gt(0(),y) -> false()
      gt(s(x),s(y)) -> gt(x,y)
      divides(x,y) -> div(x,y,y)
      div(0(),0(),z) -> true()
      div(0(),s(x),z) -> false()
      div(s(x),0(),s(z)) -> div(s(x),s(z),s(z))
      div(s(x),s(y),z) -> div(x,y,z)
      prime(x) -> test(x,s(s(0())))
      test(x,y) -> if1(gt(x,y),x,y)
      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))
     Open