MAYBE

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

Proof:
 Uncurry Processor:
  a2(x,y) -> f(f(x,a1(y)),a())
  f(a1(x2),x3) -> a2(x2,x3)
  f(a(),x3) -> a1(x3)
  DP Processor:
   DPs:
    a{2,#}(x,y) -> f#(x,a1(y))
    a{2,#}(x,y) -> f#(f(x,a1(y)),a())
    f#(a1(x2),x3) -> a{2,#}(x2,x3)
   TRS:
    a2(x,y) -> f(f(x,a1(y)),a())
    f(a1(x2),x3) -> a2(x2,x3)
    f(a(),x3) -> a1(x3)
   TDG Processor:
    DPs:
     a{2,#}(x,y) -> f#(x,a1(y))
     a{2,#}(x,y) -> f#(f(x,a1(y)),a())
     f#(a1(x2),x3) -> a{2,#}(x2,x3)
    TRS:
     a2(x,y) -> f(f(x,a1(y)),a())
     f(a1(x2),x3) -> a2(x2,x3)
     f(a(),x3) -> a1(x3)
    graph:
     f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
     a{2,#}(x,y) -> f#(f(x,a1(y)),a())
     f#(a1(x2),x3) -> a{2,#}(x2,x3) -> a{2,#}(x,y) -> f#(x,a1(y))
     a{2,#}(x,y) -> f#(f(x,a1(y)),a()) -> f#(a1(x2),x3) -> a{2,#}(x2,x3)
     a{2,#}(x,y) -> f#(x,a1(y)) -> f#(a1(x2),x3) -> a{2,#}(x2,x3)
    Open