MAYBE

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

Proof:
 Uncurry Processor:
  a3(a1(a()),a(),x) -> f(x,f(x,a()))
  f(a2(x2,x1),x3) -> a3(x2,x1,x3)
  f(a1(x2),x3) -> a2(x2,x3)
  f(a(),x3) -> a1(x3)
  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(x2,x1),x3) -> a{3,#}(x2,x1,x3)
   TRS:
    a3(a1(a()),a(),x) -> f(x,f(x,a()))
    f(a2(x2,x1),x3) -> a3(x2,x1,x3)
    f(a1(x2),x3) -> a2(x2,x3)
    f(a(),x3) -> a1(x3)
   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(x2,x1),x3) -> a{3,#}(x2,x1,x3)
    TRS:
     a3(a1(a()),a(),x) -> f(x,f(x,a()))
     f(a2(x2,x1),x3) -> a3(x2,x1,x3)
     f(a1(x2),x3) -> a2(x2,x3)
     f(a(),x3) -> a1(x3)
    graph:
     f#(a2(x2,x1),x3) -> a{3,#}(x2,x1,x3) ->
     a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
     f#(a2(x2,x1),x3) -> a{3,#}(x2,x1,x3) ->
     a{3,#}(a1(a()),a(),x) -> f#(x,a())
     a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a())) ->
     f#(a2(x2,x1),x3) -> a{3,#}(x2,x1,x3)
     a{3,#}(a1(a()),a(),x) -> f#(x,a()) -> f#(a2(x2,x1),x3) -> a{3,#}(x2,x1,x3)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [f#](x0, x1) = x0 + 1x1 + 0,
      
      [a{3,#}](x0, x1, x2) = 1x0 + 1x1 + 1x2 + 0,
      
      [a1](x0) = 1x0 + 0,
      
      [a3](x0, x1, x2) = 1x0 + x1 + 1x2 + 0,
      
      [a2](x0, x1) = 1x0 + 1x1,
      
      [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(x2,x1),x3) = 1x1 + 1x2 + 1x3 + 0 >= 1x1 + 1x2 + 1x3 + 0 = a{3,#}(x2,x1,x3)
      
      a3(a1(a()),a(),x) = 1x + 5 >= 1x + 5 = f(x,f(x,a()))
      
      f(a2(x2,x1),x3) = 1x1 + 1x2 + 1x3 + 0 >= x1 + 1x2 + 1x3 + 0 = a3(x2,x1,x3)
      
      f(a1(x2),x3) = 1x2 + 1x3 + 0 >= 1x2 + 1x3 = a2(x2,x3)
      
      f(a(),x3) = 1x3 + 3 >= 1x3 + 0 = a1(x3)
     problem:
      DPs:
       a{3,#}(a1(a()),a(),x) -> f#(x,f(x,a()))
       f#(a2(x2,x1),x3) -> a{3,#}(x2,x1,x3)
      TRS:
       a3(a1(a()),a(),x) -> f(x,f(x,a()))
       f(a2(x2,x1),x3) -> a3(x2,x1,x3)
       f(a1(x2),x3) -> a2(x2,x3)
       f(a(),x3) -> a1(x3)
     Open