MAYBE
Time: 0.032449
TRS:
 {p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))}
 DP:
  DP:
   {p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))),
    p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)),
    p#(a x0, p(b x1, p(a x2, x3))) -> p#(b x1, x3)}
  TRS:
  {p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))}
  UR:
   {p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))}
   EDG:
    {(p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)), p#(a x0, p(b x1, p(a x2, x3))) -> p#(b x1, x3))
     (p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)), p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)))
     (p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)), p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))))
     (p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))), p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))))
     (p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))), p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3)))
     (p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))), p#(a x0, p(b x1, p(a x2, x3))) -> p#(b x1, x3))}
    STATUS:
     arrows: 0.333333
     SCCS (1):
      Scc:
       {p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))),
        p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3))}
      
      SCC (2):
       Strict:
        {p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3))),
         p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3))}
       Weak:
       {p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [p](x0, x1) = x0 + 1,
         
         [a](x0) = 0,
         
         [b](x0) = 0,
         
         [p#](x0, x1) = x0
        Strict:
         p#(a x0, p(b x1, p(a x2, x3))) -> p#(a a x0, p(b x1, x3))
         2 + 0x2 + 0x0 + 0x1 + 1x3 >= 1 + 0x0 + 0x1 + 1x3
         p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3)))
         2 + 0x2 + 0x0 + 0x1 + 1x3 >= 2 + 0x2 + 0x0 + 0x1 + 1x3
        Weak:
         p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))
         3 + 0x2 + 0x0 + 0x1 + 1x3 >= 3 + 0x2 + 0x0 + 0x1 + 1x3
       SCCS (1):
        Scc:
         {p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3)))}
        
        SCC (1):
         Strict:
          {p#(a x0, p(b x1, p(a x2, x3))) -> p#(x2, p(a a x0, p(b x1, x3)))}
         Weak:
         {p(a x0, p(b x1, p(a x2, x3))) -> p(x2, p(a a x0, p(b x1, x3)))}
         Fail