YES

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

Proof:
 DP Processor:
  DPs:
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
  TRS:
   p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
  EDG Processor:
   DPs:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
   TRS:
    p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
   graph:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 6/9
    DPs:
     p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
     p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    TRS:
     p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [p#](x0, x1) = x0 + x1,
      
      [p](x0, x1) = x0 + x1 + 1,
      
      [b](x0) = x0,
      
      [a](x0) = x0
     orientation:
      p#(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 2 >= x0 + x1 + x2 + x3 + 2 = p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
      
      p#(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 2 >= x0 + x3 = p#(x3,x0)
      
      p(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 3 >= x0 + x1 + x2 + x3 + 3 = p(p(b(x2),a(a(b(x1)))),p(x3,x0))
     problem:
      DPs:
       p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
      TRS:
       p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {6}
       transitions:
        p1(17,16) -> 18*
        p1(13,5) -> 13*
        p1(18,13) -> 13,5
        p1(5,5) -> 13*
        p1(17,23) -> 18*
        p1(14,23) -> 18*
        b1(5) -> 17,14
        b1(16) -> 21*
        b1(23) -> 21*
        b1(18) -> 17*
        b1(13) -> 14*
        a1(15) -> 16*
        a1(22) -> 23*
        a1(14) -> 15*
        a1(21) -> 22*
        p{#,1}(18,13) -> 6*
        p{#,0}(5,5) -> 6*
        p0(5,5) -> 5*
        b0(5) -> 5*
        a0(5) -> 5*
      problem:
       DPs:
        
       TRS:
        p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
      Qed