MAYBE

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

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