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