YES

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

Proof:
 DP Processor:
  DPs:
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(a(x1)),b(x0))
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,a(x2))
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(x3,a(x2)),p(b(a(x1)),b(x0)))
  TRS:
   p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(x3,a(x2)),p(b(a(x1)),b(x0)))
  Usable Rule Processor:
   DPs:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(a(x1)),b(x0))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,a(x2))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(x3,a(x2)),p(b(a(x1)),b(x0)))
   TRS:
    
   Matrix Interpretation Processor: dim=2
    
    usable rules:
     
    interpretation:
     [p#](x0, x1) = [2 0]x0 + [0 2]x1 + [3],
     
                   [0 1]     [0 0]  
     [p](x0, x1) = [2 0]x0 + [1 1]x1,
     
               [0 0]  
     [b](x0) = [1 2]x0,
     
               [2 2]     [1]
     [a](x0) = [0 0]x0 + [0]
    orientation:
     p#(p(b(a(x0)),x1),p(x2,x3)) = [4 4]x0 + [4 0]x2 + [2 2]x3 + [5] >= [2 4]x0 + [3] = p#(b(a(x1)),b(x0))
     
     p#(p(b(a(x0)),x1),p(x2,x3)) = [4 4]x0 + [4 0]x2 + [2 2]x3 + [5] >= [2 0]x3 + [3] = p#(x3,a(x2))
     
     p#(p(b(a(x0)),x1),p(x2,x3)) = [4 4]x0 + [4 0]x2 + [2 2]x3 + [5] >= [2 4]x0 + [0 2]x3 + [3] = p#(p(x3,a(x2)),p(b(a(x1)),b(x0)))
    problem:
     DPs:
      
     TRS:
      
    Qed