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))
  Usable Rule 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:
    f18(x,y) -> x
    f18(x,y) -> y
    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)
   CDG 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:
     f18(x,y) -> x
     f18(x,y) -> y
     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)
    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),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)
     gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
    Restore Modifier:
     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))
     SCC Processor:
      #sccs: 3
      #rules: 6
      #arcs: 15/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:
       dimension: 1
       interpretation:
        [gt#](x0, x1) = x1 + 1,
        
        [if2](x0, x1, x2) = 0,
        
        [if1](x0, x1, x2) = 0,
        
        [test](x0, x1) = 0,
        
        [prime](x0) = 0,
        
        [div](x0, x1, x2) = 0,
        
        [divides](x0, x1) = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [gt](x0, x1) = 0,
        
        [0] = 0,
        
        [s](x0) = x0 + 1
       orientation:
        gt#(s(x),s(y)) = y + 2 >= y + 1 = gt#(x,y)
        
        gt(s(x),0()) = 0 >= 0 = true()
        
        gt(0(),y) = 0 >= 0 = false()
        
        gt(s(x),s(y)) = 0 >= 0 = gt(x,y)
        
        divides(x,y) = 0 >= 0 = div(x,y,y)
        
        div(0(),0(),z) = 0 >= 0 = true()
        
        div(0(),s(x),z) = 0 >= 0 = false()
        
        div(s(x),0(),s(z)) = 0 >= 0 = div(s(x),s(z),s(z))
        
        div(s(x),s(y),z) = 0 >= 0 = div(x,y,z)
        
        prime(x) = 0 >= 0 = test(x,s(s(0())))
        
        test(x,y) = 0 >= 0 = if1(gt(x,y),x,y)
        
        if1(true(),x,y) = 0 >= 0 = if2(divides(x,y),x,y)
        
        if1(false(),x,y) = 0 >= 0 = true()
        
        if2(true(),x,y) = 0 >= 0 = false()
        
        if2(false(),x,y) = 0 >= 0 = 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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [div#](x0, x1, x2) = x0 + 1,
        
        [if2](x0, x1, x2) = 0,
        
        [if1](x0, x1, x2) = 0,
        
        [test](x0, x1) = 0,
        
        [prime](x0) = 0,
        
        [div](x0, x1, x2) = 0,
        
        [divides](x0, x1) = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [gt](x0, x1) = 0,
        
        [0] = 1,
        
        [s](x0) = x0 + 1
       orientation:
        div#(s(x),s(y),z) = x + 2 >= x + 1 = div#(x,y,z)
        
        div#(s(x),0(),s(z)) = x + 2 >= x + 2 = div#(s(x),s(z),s(z))
        
        gt(s(x),0()) = 0 >= 0 = true()
        
        gt(0(),y) = 0 >= 0 = false()
        
        gt(s(x),s(y)) = 0 >= 0 = gt(x,y)
        
        divides(x,y) = 0 >= 0 = div(x,y,y)
        
        div(0(),0(),z) = 0 >= 0 = true()
        
        div(0(),s(x),z) = 0 >= 0 = false()
        
        div(s(x),0(),s(z)) = 0 >= 0 = div(s(x),s(z),s(z))
        
        div(s(x),s(y),z) = 0 >= 0 = div(x,y,z)
        
        prime(x) = 0 >= 0 = test(x,s(s(0())))
        
        test(x,y) = 0 >= 0 = if1(gt(x,y),x,y)
        
        if1(true(),x,y) = 0 >= 0 = if2(divides(x,y),x,y)
        
        if1(false(),x,y) = 0 >= 0 = true()
        
        if2(true(),x,y) = 0 >= 0 = false()
        
        if2(false(),x,y) = 0 >= 0 = test(x,s(y))
       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))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [div#](x0, x1, x2) = x1,
         
         [if2](x0, x1, x2) = 0,
         
         [if1](x0, x1, x2) = 0,
         
         [test](x0, x1) = 0,
         
         [prime](x0) = 0,
         
         [div](x0, x1, x2) = 0,
         
         [divides](x0, x1) = 0,
         
         [false] = 0,
         
         [true] = 0,
         
         [gt](x0, x1) = 0,
         
         [0] = 1,
         
         [s](x0) = 0
        orientation:
         div#(s(x),0(),s(z)) = 1 >= 0 = div#(s(x),s(z),s(z))
         
         gt(s(x),0()) = 0 >= 0 = true()
         
         gt(0(),y) = 0 >= 0 = false()
         
         gt(s(x),s(y)) = 0 >= 0 = gt(x,y)
         
         divides(x,y) = 0 >= 0 = div(x,y,y)
         
         div(0(),0(),z) = 0 >= 0 = true()
         
         div(0(),s(x),z) = 0 >= 0 = false()
         
         div(s(x),0(),s(z)) = 0 >= 0 = div(s(x),s(z),s(z))
         
         div(s(x),s(y),z) = 0 >= 0 = div(x,y,z)
         
         prime(x) = 0 >= 0 = test(x,s(s(0())))
         
         test(x,y) = 0 >= 0 = if1(gt(x,y),x,y)
         
         if1(true(),x,y) = 0 >= 0 = if2(divides(x,y),x,y)
         
         if1(false(),x,y) = 0 >= 0 = true()
         
         if2(true(),x,y) = 0 >= 0 = false()
         
         if2(false(),x,y) = 0 >= 0 = 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