YES
Trs:
 {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(x3, a(x2)), p(b(a(x1)), b(x0)))}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {     b_1(q6) -> q7,
          b_1(q3) -> q8,
          b_0(q3) -> q3,
         a_1(q16) -> q6,
          a_1(q7) -> q16,
          a_1(q5) -> q17,
          a_1(q4) -> q6,
          a_1(q3) -> q6 | q4,
          a_0(q3) -> q3,
     p_1(q9, q17) -> q5,
     p_1(q8, q16) -> q5,
      p_1(q7, q8) -> q9,
      p_1(q5, q9) -> q3,
      p_1(q3, q4) -> q5,
      p_0(q3, q3) -> q3}
   Strict:
   {}
   Qed