MAYBE

Problem:
 f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
 f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))

Proof:
 DP Processor:
  DPs:
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(x,y))
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(x,y)))
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(a(),f(x,y))))
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(a(),f(a(),f(a(),f(x,y)))))
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(c(),f(b(),f(a(),f(a(),f(a(),f(x,y))))))
   f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
   f#(a(),f(c(),f(x,y))) -> f#(b(),f(x,y))
  TRS:
   f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
   f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))
  Restore Modifier:
   DPs:
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(x,y))
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(x,y)))
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(a(),f(x,y))))
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(a(),f(a(),f(a(),f(x,y)))))
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(c(),f(b(),f(a(),f(a(),f(a(),f(x,y))))))
    f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
    f#(a(),f(c(),f(x,y))) -> f#(b(),f(x,y))
   TRS:
    f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
    f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))
   SCC Processor:
    #sccs: 1
    #rules: 7
    #arcs: 49/49
    DPs:
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(x,y))
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(x,y)))
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(a(),f(a(),f(a(),f(x,y))))
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(a(),f(a(),f(a(),f(x,y)))))
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(c(),f(b(),f(a(),f(a(),f(a(),f(x,y))))))
     f#(a(),f(a(),f(b(),f(x,y)))) -> f#(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
     f#(a(),f(c(),f(x,y))) -> f#(b(),f(x,y))
    TRS:
     f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
     f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))
    Open