MAYBE

Problem:
 p(0(x1)) -> 0(s(s(p(x1))))
 p(s(x1)) -> x1
 p(p(s(x1))) -> p(x1)
 f(s(x1)) -> g(s(x1))
 g(x1) -> i(s(half(x1)))
 i(x1) -> f(p(x1))
 half(0(x1)) -> 0(s(s(half(x1))))
 half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
 0(x1) -> x1
 rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))

Proof:
 DP Processor:
  DPs:
   p#(0(x1)) -> p#(x1)
   p#(0(x1)) -> 0#(s(s(p(x1))))
   p#(p(s(x1))) -> p#(x1)
   f#(s(x1)) -> g#(s(x1))
   g#(x1) -> half#(x1)
   g#(x1) -> i#(s(half(x1)))
   i#(x1) -> p#(x1)
   i#(x1) -> f#(p(x1))
   half#(0(x1)) -> half#(x1)
   half#(0(x1)) -> 0#(s(s(half(x1))))
   half#(s(s(x1))) -> p#(s(s(x1)))
   half#(s(s(x1))) -> p#(p(s(s(x1))))
   half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
   rd#(0(x1)) -> rd#(x1)
   rd#(0(x1)) -> 0#(rd(x1))
   rd#(0(x1)) -> 0#(0(rd(x1)))
   rd#(0(x1)) -> 0#(0(0(rd(x1))))
   rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
   rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
   rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
  TRS:
   p(0(x1)) -> 0(s(s(p(x1))))
   p(s(x1)) -> x1
   p(p(s(x1))) -> p(x1)
   f(s(x1)) -> g(s(x1))
   g(x1) -> i(s(half(x1)))
   i(x1) -> f(p(x1))
   half(0(x1)) -> 0(s(s(half(x1))))
   half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
   0(x1) -> x1
   rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
  TDG Processor:
   DPs:
    p#(0(x1)) -> p#(x1)
    p#(0(x1)) -> 0#(s(s(p(x1))))
    p#(p(s(x1))) -> p#(x1)
    f#(s(x1)) -> g#(s(x1))
    g#(x1) -> half#(x1)
    g#(x1) -> i#(s(half(x1)))
    i#(x1) -> p#(x1)
    i#(x1) -> f#(p(x1))
    half#(0(x1)) -> half#(x1)
    half#(0(x1)) -> 0#(s(s(half(x1))))
    half#(s(s(x1))) -> p#(s(s(x1)))
    half#(s(s(x1))) -> p#(p(s(s(x1))))
    half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
    rd#(0(x1)) -> rd#(x1)
    rd#(0(x1)) -> 0#(rd(x1))
    rd#(0(x1)) -> 0#(0(rd(x1)))
    rd#(0(x1)) -> 0#(0(0(rd(x1))))
    rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
    rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
    rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
   TRS:
    p(0(x1)) -> 0(s(s(p(x1))))
    p(s(x1)) -> x1
    p(p(s(x1))) -> p(x1)
    f(s(x1)) -> g(s(x1))
    g(x1) -> i(s(half(x1)))
    i(x1) -> f(p(x1))
    half(0(x1)) -> 0(s(s(half(x1))))
    half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
    0(x1) -> x1
    rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
   graph:
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(rd(x1))))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(rd(x1)))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(rd(x1))
    rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> rd#(x1)
    i#(x1) -> f#(p(x1)) -> f#(s(x1)) -> g#(s(x1))
    i#(x1) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
    i#(x1) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
    i#(x1) -> p#(x1) -> p#(0(x1)) -> p#(x1)
    half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
    half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
    half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
    half#(s(s(x1))) -> p#(p(s(s(x1))))
    half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
    half#(s(s(x1))) -> p#(s(s(x1)))
    half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
    half#(0(x1)) -> 0#(s(s(half(x1))))
    half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
    half#(0(x1)) -> half#(x1)
    half#(s(s(x1))) -> p#(s(s(x1))) -> p#(p(s(x1))) -> p#(x1)
    half#(s(s(x1))) -> p#(s(s(x1))) -> p#(0(x1)) -> 0#(s(s(p(x1))))
    half#(s(s(x1))) -> p#(s(s(x1))) -> p#(0(x1)) -> p#(x1)
    half#(s(s(x1))) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1)
    half#(s(s(x1))) -> p#(p(s(s(x1)))) ->
    p#(0(x1)) -> 0#(s(s(p(x1))))
    half#(s(s(x1))) -> p#(p(s(s(x1)))) -> p#(0(x1)) -> p#(x1)
    half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
    half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> p#(p(s(s(x1))))
    half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> p#(s(s(x1)))
    half#(0(x1)) -> half#(x1) -> half#(0(x1)) -> 0#(s(s(half(x1))))
    half#(0(x1)) -> half#(x1) -> half#(0(x1)) -> half#(x1)
    g#(x1) -> i#(s(half(x1))) -> i#(x1) -> f#(p(x1))
    g#(x1) -> i#(s(half(x1))) -> i#(x1) -> p#(x1)
    g#(x1) -> half#(x1) -> half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
    g#(x1) -> half#(x1) -> half#(s(s(x1))) -> p#(p(s(s(x1))))
    g#(x1) -> half#(x1) -> half#(s(s(x1))) -> p#(s(s(x1)))
    g#(x1) -> half#(x1) -> half#(0(x1)) -> 0#(s(s(half(x1))))
    g#(x1) -> half#(x1) -> half#(0(x1)) -> half#(x1)
    f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> i#(s(half(x1)))
    f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> half#(x1)
    p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
    p#(p(s(x1))) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
    p#(p(s(x1))) -> p#(x1) -> p#(0(x1)) -> p#(x1)
    p#(0(x1)) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
    p#(0(x1)) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
    p#(0(x1)) -> p#(x1) -> p#(0(x1)) -> p#(x1)
   EDG Processor:
    DPs:
     p#(0(x1)) -> p#(x1)
     p#(0(x1)) -> 0#(s(s(p(x1))))
     p#(p(s(x1))) -> p#(x1)
     f#(s(x1)) -> g#(s(x1))
     g#(x1) -> half#(x1)
     g#(x1) -> i#(s(half(x1)))
     i#(x1) -> p#(x1)
     i#(x1) -> f#(p(x1))
     half#(0(x1)) -> half#(x1)
     half#(0(x1)) -> 0#(s(s(half(x1))))
     half#(s(s(x1))) -> p#(s(s(x1)))
     half#(s(s(x1))) -> p#(p(s(s(x1))))
     half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
     rd#(0(x1)) -> rd#(x1)
     rd#(0(x1)) -> 0#(rd(x1))
     rd#(0(x1)) -> 0#(0(rd(x1)))
     rd#(0(x1)) -> 0#(0(0(rd(x1))))
     rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
     rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
     rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
    TRS:
     p(0(x1)) -> 0(s(s(p(x1))))
     p(s(x1)) -> x1
     p(p(s(x1))) -> p(x1)
     f(s(x1)) -> g(s(x1))
     g(x1) -> i(s(half(x1)))
     i(x1) -> f(p(x1))
     half(0(x1)) -> 0(s(s(half(x1))))
     half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
     0(x1) -> x1
     rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
    graph:
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> rd#(x1)
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(rd(x1))
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(rd(x1)))
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(rd(x1))))
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
     rd#(0(x1)) -> rd#(x1) -> rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
     i#(x1) -> f#(p(x1)) -> f#(s(x1)) -> g#(s(x1))
     i#(x1) -> p#(x1) -> p#(0(x1)) -> p#(x1)
     i#(x1) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
     i#(x1) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
     half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
     half#(0(x1)) -> half#(x1)
     half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
     half#(0(x1)) -> 0#(s(s(half(x1))))
     half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
     half#(s(s(x1))) -> p#(s(s(x1)))
     half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
     half#(s(s(x1))) -> p#(p(s(s(x1))))
     half#(s(s(x1))) -> half#(p(p(s(s(x1))))) ->
     half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
     half#(s(s(x1))) -> p#(p(s(s(x1)))) -> p#(0(x1)) -> p#(x1)
     half#(s(s(x1))) -> p#(p(s(s(x1)))) ->
     p#(0(x1)) -> 0#(s(s(p(x1))))
     half#(s(s(x1))) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1)
     half#(0(x1)) -> half#(x1) -> half#(0(x1)) -> half#(x1)
     half#(0(x1)) -> half#(x1) -> half#(0(x1)) -> 0#(s(s(half(x1))))
     half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> p#(s(s(x1)))
     half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> p#(p(s(s(x1))))
     half#(0(x1)) -> half#(x1) -> half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
     g#(x1) -> i#(s(half(x1))) -> i#(x1) -> p#(x1)
     g#(x1) -> i#(s(half(x1))) -> i#(x1) -> f#(p(x1))
     g#(x1) -> half#(x1) -> half#(0(x1)) -> half#(x1)
     g#(x1) -> half#(x1) -> half#(0(x1)) -> 0#(s(s(half(x1))))
     g#(x1) -> half#(x1) -> half#(s(s(x1))) -> p#(s(s(x1)))
     g#(x1) -> half#(x1) -> half#(s(s(x1))) -> p#(p(s(s(x1))))
     g#(x1) -> half#(x1) -> half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
     f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> half#(x1)
     f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> i#(s(half(x1)))
     p#(p(s(x1))) -> p#(x1) -> p#(0(x1)) -> p#(x1)
     p#(p(s(x1))) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
     p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
     p#(0(x1)) -> p#(x1) -> p#(0(x1)) -> p#(x1)
     p#(0(x1)) -> p#(x1) -> p#(0(x1)) -> 0#(s(s(p(x1))))
     p#(0(x1)) -> p#(x1) -> p#(p(s(x1))) -> p#(x1)
    CDG Processor:
     DPs:
      p#(0(x1)) -> p#(x1)
      p#(0(x1)) -> 0#(s(s(p(x1))))
      p#(p(s(x1))) -> p#(x1)
      f#(s(x1)) -> g#(s(x1))
      g#(x1) -> half#(x1)
      g#(x1) -> i#(s(half(x1)))
      i#(x1) -> p#(x1)
      i#(x1) -> f#(p(x1))
      half#(0(x1)) -> half#(x1)
      half#(0(x1)) -> 0#(s(s(half(x1))))
      half#(s(s(x1))) -> p#(s(s(x1)))
      half#(s(s(x1))) -> p#(p(s(s(x1))))
      half#(s(s(x1))) -> half#(p(p(s(s(x1)))))
      rd#(0(x1)) -> rd#(x1)
      rd#(0(x1)) -> 0#(rd(x1))
      rd#(0(x1)) -> 0#(0(rd(x1)))
      rd#(0(x1)) -> 0#(0(0(rd(x1))))
      rd#(0(x1)) -> 0#(0(0(0(rd(x1)))))
      rd#(0(x1)) -> 0#(0(0(0(0(rd(x1))))))
      rd#(0(x1)) -> 0#(0(0(0(0(0(rd(x1)))))))
     TRS:
      p(0(x1)) -> 0(s(s(p(x1))))
      p(s(x1)) -> x1
      p(p(s(x1))) -> p(x1)
      f(s(x1)) -> g(s(x1))
      g(x1) -> i(s(half(x1)))
      i(x1) -> f(p(x1))
      half(0(x1)) -> 0(s(s(half(x1))))
      half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
      0(x1) -> x1
      rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
     graph:
      i#(x1) -> f#(p(x1)) -> f#(s(x1)) -> g#(s(x1))
      half#(s(s(x1))) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1)
      g#(x1) -> i#(s(half(x1))) -> i#(x1) -> f#(p(x1))
      g#(x1) -> i#(s(half(x1))) -> i#(x1) -> p#(x1)
      f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> i#(s(half(x1)))
      f#(s(x1)) -> g#(s(x1)) -> g#(x1) -> half#(x1)
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 6/400
      DPs:
       i#(x1) -> f#(p(x1))
       f#(s(x1)) -> g#(s(x1))
       g#(x1) -> i#(s(half(x1)))
      TRS:
       p(0(x1)) -> 0(s(s(p(x1))))
       p(s(x1)) -> x1
       p(p(s(x1))) -> p(x1)
       f(s(x1)) -> g(s(x1))
       g(x1) -> i(s(half(x1)))
       i(x1) -> f(p(x1))
       half(0(x1)) -> 0(s(s(half(x1))))
       half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
       0(x1) -> x1
       rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
      Open