YES
O(n)
TRS:
 {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
 DUP: We consider a non-duplicating system.
  Trs:
   {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(b(x2), a(a(b(x1)))), p(x3, x0))}
  BOUND:
   Automaton:
    {
        a_1(6) -> 7,
        a_1(5) -> 6,
        a_0(3) -> 3,
        b_1(9) -> 4,
        b_1(8) -> 4,
        b_1(7) -> 5,
        b_1(3) -> 5 | 4,
        b_0(3) -> 3,
     p_1(9, 3) -> 9,
     p_1(8, 9) -> 9 | 3,
     p_1(4, 7) -> 8,
     p_1(3, 3) -> 9,
     p_0(3, 3) -> 3
    }
   Strict:
    {}
   Qed