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)))
  EDG 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)))
   graph:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(x3,a(x2)),p(b(a(x1)),b(x0))) ->
    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#(p(x3,a(x2)),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))) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(x3,a(x2)),p(b(a(x1)),b(x0)))
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 3/9
    DPs:
     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#(p(x3,a(x2)),p(b(a(x1)),b(x0)))
     TRS:
      
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {6}
       transitions:
        p{#,1}(18,16) -> 6*
        p1(13,19) -> 18*
        p1(15,13) -> 16*
        p1(5,17) -> 18*
        a1(15) -> 19*
        a1(5) -> 17,14
        a1(17) -> 14*
        a1(19) -> 14*
        b1(5) -> 13*
        b1(14) -> 15*
        p{#,0}(5,5) -> 6*
        p0(5,5) -> 5*
        b0(5) -> 5*
        a0(5) -> 5*
      problem:
       DPs:
        
       TRS:
        
      Qed