MAYBE

Problem:
 f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
 p(0()) -> g(0())
 g(s(p(x))) -> p(x)

Proof:
 DP Processor:
  DPs:
   f#(g(x),g(y)) -> p#(x)
   f#(g(x),g(y)) -> g#(s(p(x)))
   f#(g(x),g(y)) -> f#(g(x),s(y))
   f#(g(x),g(y)) -> p#(f(g(x),s(y)))
   f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
   p#(0()) -> g#(0())
  TRS:
   f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
   p(0()) -> g(0())
   g(s(p(x))) -> p(x)
  Usable Rule Processor:
   DPs:
    f#(g(x),g(y)) -> p#(x)
    f#(g(x),g(y)) -> g#(s(p(x)))
    f#(g(x),g(y)) -> f#(g(x),s(y))
    f#(g(x),g(y)) -> p#(f(g(x),s(y)))
    f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
    p#(0()) -> g#(0())
   TRS:
    p(0()) -> g(0())
    g(s(p(x))) -> p(x)
   TDG Processor:
    DPs:
     f#(g(x),g(y)) -> p#(x)
     f#(g(x),g(y)) -> g#(s(p(x)))
     f#(g(x),g(y)) -> f#(g(x),s(y))
     f#(g(x),g(y)) -> p#(f(g(x),s(y)))
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
     p#(0()) -> g#(0())
    TRS:
     p(0()) -> g(0())
     g(s(p(x))) -> p(x)
    graph:
     f#(g(x),g(y)) -> p#(f(g(x),s(y))) -> p#(0()) -> g#(0())
     f#(g(x),g(y)) -> p#(x) -> p#(0()) -> g#(0())
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x)))) ->
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x)))) ->
     f#(g(x),g(y)) -> p#(f(g(x),s(y)))
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x)))) ->
     f#(g(x),g(y)) -> f#(g(x),s(y))
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x)))) ->
     f#(g(x),g(y)) -> g#(s(p(x)))
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x)))) ->
     f#(g(x),g(y)) -> p#(x)
     f#(g(x),g(y)) -> f#(g(x),s(y)) ->
     f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
     f#(g(x),g(y)) -> f#(g(x),s(y)) ->
     f#(g(x),g(y)) -> p#(f(g(x),s(y)))
     f#(g(x),g(y)) -> f#(g(x),s(y)) -> f#(g(x),g(y)) -> f#(g(x),s(y))
     f#(g(x),g(y)) -> f#(g(x),s(y)) -> f#(g(x),g(y)) -> g#(s(p(x)))
     f#(g(x),g(y)) -> f#(g(x),s(y)) -> f#(g(x),g(y)) -> p#(x)
    Restore Modifier:
     DPs:
      f#(g(x),g(y)) -> p#(x)
      f#(g(x),g(y)) -> g#(s(p(x)))
      f#(g(x),g(y)) -> f#(g(x),s(y))
      f#(g(x),g(y)) -> p#(f(g(x),s(y)))
      f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
      p#(0()) -> g#(0())
     TRS:
      f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
      p(0()) -> g(0())
      g(s(p(x))) -> p(x)
     SCC Processor:
      #sccs: 1
      #rules: 2
      #arcs: 12/36
      DPs:
       f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
       f#(g(x),g(y)) -> f#(g(x),s(y))
      TRS:
       f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
       p(0()) -> g(0())
       g(s(p(x))) -> p(x)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x1,
        
        [0] = 0,
        
        [p](x0) = 1,
        
        [s](x0) = 0,
        
        [f](x0, x1) = 0,
        
        [g](x0) = 1
       orientation:
        f#(g(x),g(y)) = 1 >= 1 = f#(p(f(g(x),s(y))),g(s(p(x))))
        
        f#(g(x),g(y)) = 1 >= 0 = f#(g(x),s(y))
        
        f(g(x),g(y)) = 0 >= 0 = f(p(f(g(x),s(y))),g(s(p(x))))
        
        p(0()) = 1 >= 1 = g(0())
        
        g(s(p(x))) = 1 >= 1 = p(x)
       problem:
        DPs:
         f#(g(x),g(y)) -> f#(p(f(g(x),s(y))),g(s(p(x))))
        TRS:
         f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
         p(0()) -> g(0())
         g(s(p(x))) -> p(x)
       Open