MAYBE

Problem:
 f(f(f(f(j(),a),b),c),d) -> f(f(a,b),f(f(a,d),c))

Proof:
 Uncurry Processor:
  j4(a,b,c,d) -> f(f(a,b),f(f(a,d),c))
  f(j3(x6,x5,x4),x7) -> j4(x6,x5,x4,x7)
  f(j2(x6,x5),x7) -> j3(x6,x5,x7)
  f(j1(x6),x7) -> j2(x6,x7)
  f(j(),x7) -> j1(x7)
  DP Processor:
   DPs:
    j{4,#}(a,b,c,d) -> f#(a,d)
    j{4,#}(a,b,c,d) -> f#(f(a,d),c)
    j{4,#}(a,b,c,d) -> f#(a,b)
    j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c))
    f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
   TRS:
    j4(a,b,c,d) -> f(f(a,b),f(f(a,d),c))
    f(j3(x6,x5,x4),x7) -> j4(x6,x5,x4,x7)
    f(j2(x6,x5),x7) -> j3(x6,x5,x7)
    f(j1(x6),x7) -> j2(x6,x7)
    f(j(),x7) -> j1(x7)
   TDG Processor:
    DPs:
     j{4,#}(a,b,c,d) -> f#(a,d)
     j{4,#}(a,b,c,d) -> f#(f(a,d),c)
     j{4,#}(a,b,c,d) -> f#(a,b)
     j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c))
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
    TRS:
     j4(a,b,c,d) -> f(f(a,b),f(f(a,d),c))
     f(j3(x6,x5,x4),x7) -> j4(x6,x5,x4,x7)
     f(j2(x6,x5),x7) -> j3(x6,x5,x7)
     f(j1(x6),x7) -> j2(x6,x7)
     f(j(),x7) -> j1(x7)
    graph:
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7) ->
     j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c))
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7) ->
     j{4,#}(a,b,c,d) -> f#(a,b)
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7) ->
     j{4,#}(a,b,c,d) -> f#(f(a,d),c)
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7) ->
     j{4,#}(a,b,c,d) -> f#(a,d)
     j{4,#}(a,b,c,d) -> f#(f(a,d),c) ->
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
     j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c)) ->
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
     j{4,#}(a,b,c,d) -> f#(a,d) ->
     f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
     j{4,#}(a,b,c,d) -> f#(a,b) -> f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [f#](x0, x1) = 2x0 + -1x1 + -8,
      
      [j{4,#}](x0, x1, x2, x3) = 5x0 + x1 + -1x2 + -1x3 + 0,
      
      [j1](x0) = -3x0 + 4,
      
      [j2](x0, x1) = x0 + -3x1 + -3,
      
      [j4](x0, x1, x2, x3) = 6x0 + 1x1 + -6x2 + -3x3 + 1,
      
      [j3](x0, x1, x2) = 3x0 + -2x1 + -3x2 + -2,
      
      [f](x0, x1) = 3x0 + -3x1 + -2,
      
      [j] = 4
     orientation:
      j{4,#}(a,b,c,d) = 5a + b + -1c + -1d + 0 >= 2a + -1d + -8 = f#(a,d)
      
      j{4,#}(a,b,c,d) = 5a + b + -1c + -1d + 0 >= 5a + -1c + -1d + 0 = f#(f(a,d),c)
      
      j{4,#}(a,b,c,d) = 5a + b + -1c + -1d + 0 >= 2a + -1b + -8 = f#(a,b)
      
      j{4,#}(a,b,c,d) = 5a + b + -1c + -1d + 0 >= 5a + -1b + -4c + -1d + 0 = f#(f(a,b),f(f(a,d),c))
      
      f#(j3(x6,x5,x4),x7) = -1x4 + x5 + 5x6 + -1x7 + 0 >= -1x4 + x5 + 5x6 + -1x7 + 0 = j{4,#}(x6,x5,x4,x7)
      
      j4(a,b,c,d) = 6a + 1b + -6c + -3d + 1 >= 6a + b + -6c + -3d + 1 = f(f(a,b),f(f(a,d),c))
      
      f(j3(x6,x5,x4),x7) = x4 + 1x5 + 6x6 + -3x7 + 1 >= -6x4 + 1x5 + 6x6 + -3x7 + 1 = j4(x6,x5,x4,x7)
      
      f(j2(x6,x5),x7) = x5 + 3x6 + -3x7 + 0 >= -2x5 + 3x6 + -3x7 + -2 = j3(x6,x5,x7)
      
      f(j1(x6),x7) = x6 + -3x7 + 7 >= x6 + -3x7 + -3 = j2(x6,x7)
      
      f(j(),x7) = -3x7 + 7 >= -3x7 + 4 = j1(x7)
     problem:
      DPs:
       j{4,#}(a,b,c,d) -> f#(a,d)
       j{4,#}(a,b,c,d) -> f#(f(a,d),c)
       j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c))
       f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
      TRS:
       j4(a,b,c,d) -> f(f(a,b),f(f(a,d),c))
       f(j3(x6,x5,x4),x7) -> j4(x6,x5,x4,x7)
       f(j2(x6,x5),x7) -> j3(x6,x5,x7)
       f(j1(x6),x7) -> j2(x6,x7)
       f(j(),x7) -> j1(x7)
     Arctic Interpretation Processor:
      dimension: 2
      interpretation:
       [f#](x0, x1) = [-& 0 ]x0 + [0],
       
       [j{4,#}](x0, x1, x2, x3) = [0 1]x0 + [0  -&]x1 + [1],
       
                  [0  0 ]     [0 ]
       [j1](x0) = [-& -&]x0 + [-&],
       
                      [0  0 ]     [0  0 ]     [-&]
       [j2](x0, x1) = [-& 0 ]x0 + [-& -&]x1 + [0 ],
       
                              [2 3]     [2 0]     [0 0]     [0  0 ]     [0]
       [j4](x0, x1, x2, x3) = [1 2]x0 + [1 1]x1 + [0 0]x2 + [-& -&]x3 + [2],
       
                          [-& -&]     [-& 0 ]     [0  0 ]     [0]
       [j3](x0, x1, x2) = [0  1 ]x0 + [0  0 ]x1 + [-& -&]x2 + [1],
       
                     [0 2]     [0  0 ]     [0 ]
       [f](x0, x1) = [0 1]x0 + [-& -&]x1 + [-&],
       
             [2]
       [j] = [0]
      orientation:
       j{4,#}(a,b,c,d) = [0 1]a + [0  -&]b + [1] >= [-& 0 ]a + [0] = f#(a,d)
       
       j{4,#}(a,b,c,d) = [0 1]a + [0  -&]b + [1] >= [0 1]a + [0] = f#(f(a,d),c)
       
       j{4,#}(a,b,c,d) = [0 1]a + [0  -&]b + [1] >= [0 1]a + [0] = f#(f(a,b),f(f(a,d),c))
       
       f#(j3(x6,x5,x4),x7) = [0 0]x5 + [0 1]x6 + [1] >= [0  -&]x5 + [0 1]x6 + [1] = j{4,#}(x6,x5,x4,x7)
       
                     [2 3]    [2 0]    [0 0]    [0  0 ]    [0]    [2 3]    [0 0]    [0  0 ]    [0  0 ]    [0]                        
       j4(a,b,c,d) = [1 2]a + [1 1]b + [0 0]c + [-& -&]d + [2] >= [1 2]a + [0 0]b + [-& -&]c + [-& -&]d + [0] = f(f(a,b),f(f(a,d),c))
       
                            [0 0]     [2 2]     [2 3]     [0  0 ]     [3]    [0 0]     [2 0]     [2 3]     [0  0 ]     [0]                  
       f(j3(x6,x5,x4),x7) = [0 0]x4 + [1 1]x5 + [1 2]x6 + [-& -&]x7 + [2] >= [0 0]x4 + [1 1]x5 + [1 2]x6 + [-& -&]x7 + [2] = j4(x6,x5,x4,x7)
       
                         [0 0]     [0 2]     [0  0 ]     [2]    [-& 0 ]     [-& -&]     [0  0 ]     [0]               
       f(j2(x6,x5),x7) = [0 0]x5 + [0 1]x6 + [-& -&]x7 + [1] >= [0  0 ]x5 + [0  1 ]x6 + [-& -&]x7 + [1] = j3(x6,x5,x7)
       
                      [0 0]     [0  0 ]     [0]    [0  0 ]     [0  0 ]     [-&]            
       f(j1(x6),x7) = [0 0]x6 + [-& -&]x7 + [0] >= [-& 0 ]x6 + [-& -&]x7 + [0 ] = j2(x6,x7)
       
                   [0  0 ]     [2]    [0  0 ]     [0 ]         
       f(j(),x7) = [-& -&]x7 + [2] >= [-& -&]x7 + [-&] = j1(x7)
      problem:
       DPs:
        j{4,#}(a,b,c,d) -> f#(f(a,d),c)
        j{4,#}(a,b,c,d) -> f#(f(a,b),f(f(a,d),c))
        f#(j3(x6,x5,x4),x7) -> j{4,#}(x6,x5,x4,x7)
       TRS:
        j4(a,b,c,d) -> f(f(a,b),f(f(a,d),c))
        f(j3(x6,x5,x4),x7) -> j4(x6,x5,x4,x7)
        f(j2(x6,x5),x7) -> j3(x6,x5,x7)
        f(j1(x6),x7) -> j2(x6,x7)
        f(j(),x7) -> j1(x7)
      Open