YES
TRS:
 {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
 DP:
  Strict:
   {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))))}
  Weak:
  {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
  EDG:
   {(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#(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#(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#(b(x2), a(a(b(x1)))))}
   SCCS:
    Scc:
     {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:
     Strict:
      {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))}
     Weak:
     {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
     POLY:
      Argument Filtering:
       pi(a) = 0, pi(b) = 0, pi(p#) = [0,1], pi(p) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [p#](x0, x1) = x0 + x1 + 1,
       [p](x0, x1) = x0 + x1 + 1
      Strict:
       {p#(p(b(a(x0)), x1), p(x2, x3)) -> p#(p(b(x2), a(a(b(x1)))), p(x3, x0))}
      Weak:
       {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
      EDG:
       {(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)))}
       SCCS:
        Scc:
         {p#(p(b(a(x0)), x1), p(x2, x3)) -> p#(p(b(x2), a(a(b(x1)))), p(x3, x0))}
        SCC:
         Strict:
          {p#(p(b(a(x0)), x1), p(x2, x3)) -> p#(p(b(x2), a(a(b(x1)))), p(x3, x0))}
         Weak:
         {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
         UR:
          {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
          BOUND:
           Bound: match(-raise)-DP-bounded by 0
           Automaton:
            {     c_0() -> 2*
                 a_0(5) -> 6*
                 a_0(4) -> 5*
                 b_0(8) -> 3*
                 b_0(7) -> 3*
                 b_0(6) -> 4*
                 b_0(2) -> 4 | 3
             p#_0(7, 8) -> 1*
              p_0(8, 2) -> 8*
              p_0(7, 8) -> 8*
              p_0(3, 6) -> 7*
              p_0(2, 2) -> 8*}
           Strict:
            {}
           Qed