MAYBE

Problem:
 p(a(x0),p(x1,p(x2,x3))) -> p(x1,p(x0,p(a(x3),x3)))

Proof:
 DP Processor:
  DPs:
   p#(a(x0),p(x1,p(x2,x3))) -> p#(a(x3),x3)
   p#(a(x0),p(x1,p(x2,x3))) -> p#(x0,p(a(x3),x3))
   p#(a(x0),p(x1,p(x2,x3))) -> p#(x1,p(x0,p(a(x3),x3)))
  TRS:
   p(a(x0),p(x1,p(x2,x3))) -> p(x1,p(x0,p(a(x3),x3)))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [p#](x0, x1) = 1x0 + 2x1,
    
    [p](x0, x1) = x0 + 1x1,
    
    [a](x0) = 1x0
   orientation:
    p#(a(x0),p(x1,p(x2,x3))) = 2x0 + 2x1 + 3x2 + 4x3 >= 2x3 = p#(a(x3),x3)
    
    p#(a(x0),p(x1,p(x2,x3))) = 2x0 + 2x1 + 3x2 + 4x3 >= 1x0 + 3x3 = p#(x0,p(a(x3),x3))
    
    p#(a(x0),p(x1,p(x2,x3))) = 2x0 + 2x1 + 3x2 + 4x3 >= 2x0 + 1x1 + 4x3 = p#(x1,p(x0,p(a(x3),x3)))
    
    p(a(x0),p(x1,p(x2,x3))) = 1x0 + 1x1 + 2x2 + 3x3 >= 1x0 + x1 + 3x3 = p(x1,p(x0,p(a(x3),x3)))
   problem:
    DPs:
     p#(a(x0),p(x1,p(x2,x3))) -> p#(x1,p(x0,p(a(x3),x3)))
    TRS:
     p(a(x0),p(x1,p(x2,x3))) -> p(x1,p(x0,p(a(x3),x3)))
   Open