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)-bounded by 1
           Automaton:
            {    a_1(4) -> 5*
                 a_1(3) -> 4*
                 a_0(1) -> 1*
                 b_1(7) -> 2*
                 b_1(6) -> 2*
                 b_1(5) -> 3*
                 b_1(1) -> 3 | 2
                 b_0(1) -> 1*
             p#_1(6, 7) -> 1*
             p#_0(1, 1) -> 1*
              p_1(7, 1) -> 7*
              p_1(6, 7) -> 7 | 1
              p_1(2, 5) -> 6*
              p_1(1, 1) -> 7*
              p_0(1, 1) -> 1*}
           Strict:
            {}
           Qed