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: {9,1}
       transitions:
        p1(7,14) -> 49*
        p1(2,14) -> 49*
        p1(13,7) -> 49*
        p1(3,7) -> 49*
        p1(13,13) -> 49*
        p1(3,13) -> 49*
        p1(49,4) -> 49*
        p1(14,4) -> 49*
        p1(4,4) -> 49*
        p1(49,14) -> 49*
        p1(14,14) -> 49*
        p1(4,14) -> 49*
        p1(5,7) -> 49*
        p1(5,13) -> 49*
        p1(7,7) -> 49*
        p1(2,7) -> 49*
        p1(7,13) -> 49*
        p1(2,13) -> 49*
        p1(13,4) -> 49*
        p1(3,4) -> 49*
        p1(13,14) -> 49*
        p1(3,14) -> 49*
        p1(49,7) -> 49*
        p1(49,13) -> 49*
        p1(14,7) -> 49*
        p1(4,7) -> 49*
        p1(14,13) -> 49*
        p1(4,13) -> 49*
        p1(53,52) -> 54*
        p1(5,4) -> 49*
        p1(5,14) -> 49*
        p1(54,49) -> 9,3
        p1(7,4) -> 49*
        p1(2,4) -> 49*
        b1(15) -> 50*
        b1(5) -> 53*
        b1(52) -> 50*
        b1(7) -> 53*
        b1(2) -> 53*
        b1(54) -> 53*
        b1(49) -> 53*
        b1(14) -> 53*
        b1(4) -> 53*
        b1(6) -> 50*
        b1(13) -> 53*
        b1(8) -> 53*
        b1(3) -> 53*
        a1(50) -> 51*
        a1(51) -> 52*
        p{#,1}(54,49) -> 1*
        f40() -> 2*
        p{#,0}(8,3) -> 1*
        p0(7,14) -> 3*
        p0(2,14) -> 3*
        p0(8,3) -> 9*
        p0(13,7) -> 3*
        p0(3,7) -> 3*
        p0(13,13) -> 3*
        p0(3,13) -> 3*
        p0(14,2) -> 3*
        p0(4,2) -> 3*
        p0(14,4) -> 3*
        p0(4,4) -> 3*
        p0(14,14) -> 3*
        p0(4,14) -> 3*
        p0(5,7) -> 3*
        p0(5,13) -> 3*
        p0(2,5) -> 3*
        p0(7,7) -> 3*
        p0(2,7) -> 3*
        p0(7,13) -> 3*
        p0(2,13) -> 3*
        p0(7,15) -> 8*
        p0(13,2) -> 3*
        p0(13,4) -> 3*
        p0(3,2) -> 3*
        p0(3,4) -> 3*
        p0(13,14) -> 3*
        p0(3,14) -> 3*
        p0(14,7) -> 3*
        p0(4,7) -> 3*
        p0(14,13) -> 3*
        p0(4,13) -> 3*
        p0(4,15) -> 8*
        p0(5,2) -> 3*
        p0(5,4) -> 3*
        p0(5,14) -> 3*
        p0(7,2) -> 3*
        p0(2,2) -> 3*
        p0(7,4) -> 3*
        p0(2,4) -> 3*
        p0(7,6) -> 8*
        b0(15) -> 4*
        b0(5) -> 7*
        b0(7) -> 7*
        b0(2) -> 7,4
        b0(14) -> 7*
        b0(4) -> 7*
        b0(6) -> 13*
        b0(13) -> 7*
        b0(8) -> 7*
        b0(3) -> 7*
        a0(5) -> 6*
        a0(7) -> 14*
        a0(14) -> 15*
        a0(4) -> 5*
        a0(13) -> 14*
        9 -> 3*
      problem:
       DPs:
        
       TRS:
        p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
      Qed