MAYBE

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

Proof:
 DP Processor:
  DPs:
   f#(f(f(f(j(),a),b),c),d) -> f#(a,d)
   f#(f(f(f(j(),a),b),c),d) -> f#(f(a,d),c)
   f#(f(f(f(j(),a),b),c),d) -> f#(a,b)
   f#(f(f(f(j(),a),b),c),d) -> f#(f(a,b),f(f(a,d),c))
  TRS:
   f(f(f(f(j(),a),b),c),d) -> f(f(a,b),f(f(a,d),c))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [f#](x0, x1) = 1x0 + x1 + -16,
    
    [f](x0, x1) = 1x0 + -1x1 + -8,
    
    [j] = 0
   orientation:
    f#(f(f(f(j(),a),b),c),d) = 2a + 1b + c + d + 4 >= 1a + d + -16 = f#(a,d)
    
    f#(f(f(f(j(),a),b),c),d) = 2a + 1b + c + d + 4 >= 2a + c + d + -7 = f#(f(a,d),c)
    
    f#(f(f(f(j(),a),b),c),d) = 2a + 1b + c + d + 4 >= 1a + b + -16 = f#(a,b)
    
    f#(f(f(f(j(),a),b),c),d) = 2a + 1b + c + d + 4 >= 2a + b + -1c + d + -7 = f#(f(a,b),f(f(a,d),c))
    
    f(f(f(f(j(),a),b),c),d) = 2a + 1b + c + -1d + 4 >= 2a + b + -2c + -1d + -7 = f(f(a,b),f(f(a,d),c))
   problem:
    DPs:
     f#(f(f(f(j(),a),b),c),d) -> f#(a,d)
     f#(f(f(f(j(),a),b),c),d) -> f#(f(a,d),c)
     f#(f(f(f(j(),a),b),c),d) -> f#(f(a,b),f(f(a,d),c))
    TRS:
     f(f(f(f(j(),a),b),c),d) -> f(f(a,b),f(f(a,d),c))
   Open