MAYBE

Problem:
 h(f(f(x))) -> h(f(g(f(x))))
 f(g(f(x))) -> f(f(x))

Proof:
 DP Processor:
  DPs:
   h#(f(f(x))) -> f#(g(f(x)))
   h#(f(f(x))) -> h#(f(g(f(x))))
   f#(g(f(x))) -> f#(f(x))
  TRS:
   h(f(f(x))) -> h(f(g(f(x))))
   f(g(f(x))) -> f(f(x))
  Usable Rule Processor:
   DPs:
    h#(f(f(x))) -> f#(g(f(x)))
    h#(f(f(x))) -> h#(f(g(f(x))))
    f#(g(f(x))) -> f#(f(x))
   TRS:
    f(g(f(x))) -> f(f(x))
   TDG Processor:
    DPs:
     h#(f(f(x))) -> f#(g(f(x)))
     h#(f(f(x))) -> h#(f(g(f(x))))
     f#(g(f(x))) -> f#(f(x))
    TRS:
     f(g(f(x))) -> f(f(x))
    graph:
     f#(g(f(x))) -> f#(f(x)) -> f#(g(f(x))) -> f#(f(x))
     h#(f(f(x))) -> f#(g(f(x))) -> f#(g(f(x))) -> f#(f(x))
     h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> h#(f(g(f(x))))
     h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> f#(g(f(x)))
    EDG Processor:
     DPs:
      h#(f(f(x))) -> f#(g(f(x)))
      h#(f(f(x))) -> h#(f(g(f(x))))
      f#(g(f(x))) -> f#(f(x))
     TRS:
      f(g(f(x))) -> f(f(x))
     graph:
      h#(f(f(x))) -> f#(g(f(x))) -> f#(g(f(x))) -> f#(f(x))
      h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> f#(g(f(x)))
      h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> h#(f(g(f(x))))
     Restore Modifier:
      DPs:
       h#(f(f(x))) -> f#(g(f(x)))
       h#(f(f(x))) -> h#(f(g(f(x))))
       f#(g(f(x))) -> f#(f(x))
      TRS:
       h(f(f(x))) -> h(f(g(f(x))))
       f(g(f(x))) -> f(f(x))
      SCC Processor:
       #sccs: 1
       #rules: 1
       #arcs: 3/9
       DPs:
        h#(f(f(x))) -> h#(f(g(f(x))))
       TRS:
        h(f(f(x))) -> h(f(g(f(x))))
        f(g(f(x))) -> f(f(x))
       Open