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