MAYBE

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

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