MAYBE

Problem:
 f(g(x)) -> g(f(f(x)))
 f(h(x)) -> h(g(x))
 f'(s(x),y,y) -> f'(y,x,s(x))

Proof:
 DP Processor:
  DPs:
   f#(g(x)) -> f#(x)
   f#(g(x)) -> f#(f(x))
   f'#(s(x),y,y) -> f'#(y,x,s(x))
  TRS:
   f(g(x)) -> g(f(f(x)))
   f(h(x)) -> h(g(x))
   f'(s(x),y,y) -> f'(y,x,s(x))
  Usable Rule Processor:
   DPs:
    f#(g(x)) -> f#(x)
    f#(g(x)) -> f#(f(x))
    f'#(s(x),y,y) -> f'#(y,x,s(x))
   TRS:
    f7(x,y) -> x
    f7(x,y) -> y
    f(g(x)) -> g(f(f(x)))
    f(h(x)) -> h(g(x))
   TDG Processor:
    DPs:
     f#(g(x)) -> f#(x)
     f#(g(x)) -> f#(f(x))
     f'#(s(x),y,y) -> f'#(y,x,s(x))
    TRS:
     f7(x,y) -> x
     f7(x,y) -> y
     f(g(x)) -> g(f(f(x)))
     f(h(x)) -> h(g(x))
    graph:
     f'#(s(x),y,y) -> f'#(y,x,s(x)) -> f'#(s(x),y,y) -> f'#(y,x,s(x))
     f#(g(x)) -> f#(f(x)) -> f#(g(x)) -> f#(f(x))
     f#(g(x)) -> f#(f(x)) -> f#(g(x)) -> f#(x)
     f#(g(x)) -> f#(x) -> f#(g(x)) -> f#(f(x))
     f#(g(x)) -> f#(x) -> f#(g(x)) -> f#(x)
    Restore Modifier:
     DPs:
      f#(g(x)) -> f#(x)
      f#(g(x)) -> f#(f(x))
      f'#(s(x),y,y) -> f'#(y,x,s(x))
     TRS:
      f(g(x)) -> g(f(f(x)))
      f(h(x)) -> h(g(x))
      f'(s(x),y,y) -> f'(y,x,s(x))
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 5/9
      DPs:
       f#(g(x)) -> f#(f(x))
       f#(g(x)) -> f#(x)
      TRS:
       f(g(x)) -> g(f(f(x)))
       f(h(x)) -> h(g(x))
       f'(s(x),y,y) -> f'(y,x,s(x))
      Open
      
      DPs:
       f'#(s(x),y,y) -> f'#(y,x,s(x))
      TRS:
       f(g(x)) -> g(f(f(x)))
       f(h(x)) -> h(g(x))
       f'(s(x),y,y) -> f'(y,x,s(x))
      Open