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)
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 16/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:
     div#(s(x),0(),s(z)) -> div#(s(x),s(z),s(z))
     div#(s(x),s(y),z) -> div#(x,y,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))
    Subterm Criterion Processor:
     simple projection:
      pi(div#) = 0
     problem:
      DPs:
       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))
     EDG Processor:
      DPs:
       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))
      graph:
       
      Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(gt#) = 1
     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