MAYBE

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

Proof:
 Uncurry Processor (mirror):
  a3(a1(a()),a(),x) -> f(x,f(x,a()))
  f(a2(x4,x3),x5) -> a3(x4,x3,x5)
  f(a1(x4),x5) -> a2(x4,x5)
  f(a(),x5) -> a1(x5)
  DP Processor:
   DPs:
    a{3,#}(a1(a()),a(),x) -> f#(x,a())
    a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
    f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
   TRS:
    a3(a1(a()),a(),x) -> f(x,f(x,a()))
    f(a2(x4,x3),x5) -> a3(x4,x3,x5)
    f(a1(x4),x5) -> a2(x4,x5)
    f(a(),x5) -> a1(x5)
   TDG Processor:
    DPs:
     a{3,#}(a1(a()),a(),x) -> f#(x,a())
     a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
    TRS:
     a3(a1(a()),a(),x) -> f(x,f(x,a()))
     f(a2(x4,x3),x5) -> a3(x4,x3,x5)
     f(a1(x4),x5) -> a2(x4,x5)
     f(a(),x5) -> a1(x5)
    graph:
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5) ->
     a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5) ->
     a{3,#}(a1(a()),a(),x) -> f#(x,a())
     a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a())) ->
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
     a{3,#}(a1(a()),a(),x) -> f#(x,a()) -> f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [f#](x0, x1) = x0 + 1x1 + 0,
      
      [a{3,#}](x0, x1, x2) = 1x0 + 1x1 + 1x2 + 0,
      
      [a3](x0, x1, x2) = 1x0 + x1 + 1x2 + 0,
      
      [a2](x0, x1) = 1x0 + 1x1,
      
      [a1](x0) = 1x0 + 0,
      
      [f](x0, x1) = x0 + 1x1 + 0,
      
      [a] = 3
     orientation:
      a{3,#}(a1(a()),a(),x) = 1x + 5 >= x + 4 = f#(x,a())
      
      a{3,#}(a1(a()),a(),x) = 1x + 5 >= 1x + 5 = f#(x,f(x,a()))
      
      f#(a2(x4,x3),x5) = 1x3 + 1x4 + 1x5 + 0 >= 1x3 + 1x4 + 1x5 + 0 = a{3,#}(x4,x3,x5)
      
      a3(a1(a()),a(),x) = 1x + 5 >= 1x + 5 = f(x,f(x,a()))
      
      f(a2(x4,x3),x5) = 1x3 + 1x4 + 1x5 + 0 >= x3 + 1x4 + 1x5 + 0 = a3(x4,x3,x5)
      
      f(a1(x4),x5) = 1x4 + 1x5 + 0 >= 1x4 + 1x5 = a2(x4,x5)
      
      f(a(),x5) = 1x5 + 3 >= 1x5 + 0 = a1(x5)
     problem:
      DPs:
       a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
       f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
      TRS:
       a3(a1(a()),a(),x) -> f(x,f(x,a()))
       f(a2(x4,x3),x5) -> a3(x4,x3,x5)
       f(a1(x4),x5) -> a2(x4,x5)
       f(a(),x5) -> a1(x5)
     Open