MAYBE
Time: 0.248697
TRS:
 {      lambda x -> x,
         a(x, y) -> x,
         a(x, y) -> y,
  a(lambda x, y) -> lambda a(x, p(1(), a(y, t()))),
   a(a(x, y), z) -> a(x, a(y, z)),
   a(p(x, y), z) -> p(a(x, z), a(y, z)),
         p(x, y) -> x,
         p(x, y) -> y}
 DP:
  DP:
   {a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))),
    a#(lambda x, y) -> a#(x, p(1(), a(y, t()))),
    a#(lambda x, y) -> a#(y, t()),
    a#(lambda x, y) -> p#(1(), a(y, t())),
     a#(a(x, y), z) -> a#(x, a(y, z)),
     a#(a(x, y), z) -> a#(y, z),
     a#(p(x, y), z) -> a#(x, z),
     a#(p(x, y), z) -> a#(y, z),
     a#(p(x, y), z) -> p#(a(x, z), a(y, z))}
  TRS:
  {      lambda x -> x,
          a(x, y) -> x,
          a(x, y) -> y,
   a(lambda x, y) -> lambda a(x, p(1(), a(y, t()))),
    a(a(x, y), z) -> a(x, a(y, z)),
    a(p(x, y), z) -> p(a(x, z), a(y, z)),
          p(x, y) -> x,
          p(x, y) -> y}
  UR:
   {      lambda x -> x,
           a(x, y) -> x,
           a(x, y) -> y,
    a(lambda x, y) -> lambda a(x, p(1(), a(y, t()))),
     a(a(x, y), z) -> a(x, a(y, z)),
     a(p(x, y), z) -> p(a(x, z), a(y, z)),
           p(x, y) -> x,
           p(x, y) -> y,
           b(w, v) -> w,
           b(w, v) -> v}
   EDG:
    {(a#(a(x, y), z) -> a#(y, z), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))
     (a#(a(x, y), z) -> a#(y, z), a#(p(x, y), z) -> a#(y, z))
     (a#(a(x, y), z) -> a#(y, z), a#(p(x, y), z) -> a#(x, z))
     (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z))
     (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t()))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(p(x, y), z) -> a#(y, z), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))
     (a#(p(x, y), z) -> a#(y, z), a#(p(x, y), z) -> a#(y, z))
     (a#(p(x, y), z) -> a#(y, z), a#(p(x, y), z) -> a#(x, z))
     (a#(p(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z))
     (a#(p(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(p(x, y), z) -> a#(y, z), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(p(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t()))
     (a#(p(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(p(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(p(x, y), z) -> a#(y, z))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(p(x, y), z) -> a#(x, z))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(y, t()))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(lambda x, y) -> a#(y, t()))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(a(x, y), z) -> a#(y, z))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(p(x, y), z) -> a#(x, z))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(p(x, y), z) -> a#(y, z))
     (a#(lambda x, y) -> a#(x, p(1(), a(y, t()))), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))
     (a#(p(x, y), z) -> a#(x, z), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(p(x, y), z) -> a#(x, z), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(p(x, y), z) -> a#(x, z), a#(lambda x, y) -> a#(y, t()))
     (a#(p(x, y), z) -> a#(x, z), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(p(x, y), z) -> a#(x, z), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(p(x, y), z) -> a#(x, z), a#(a(x, y), z) -> a#(y, z))
     (a#(p(x, y), z) -> a#(x, z), a#(p(x, y), z) -> a#(x, z))
     (a#(p(x, y), z) -> a#(x, z), a#(p(x, y), z) -> a#(y, z))
     (a#(p(x, y), z) -> a#(x, z), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, p(1(), a(y, t()))))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(y, t()))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> p#(1(), a(y, t())))
     (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z))
     (a#(lambda x, y) -> a#(y, t()), a#(p(x, y), z) -> a#(x, z))
     (a#(lambda x, y) -> a#(y, t()), a#(p(x, y), z) -> a#(y, z))
     (a#(lambda x, y) -> a#(y, t()), a#(p(x, y), z) -> p#(a(x, z), a(y, z)))}
    STATUS:
     arrows: 0.333333
     SCCS (1):
      Scc:
       {a#(lambda x, y) -> a#(x, p(1(), a(y, t()))),
        a#(lambda x, y) -> a#(y, t()),
         a#(a(x, y), z) -> a#(x, a(y, z)),
         a#(a(x, y), z) -> a#(y, z),
         a#(p(x, y), z) -> a#(x, z),
         a#(p(x, y), z) -> a#(y, z)}
      
      SCC (6):
       Strict:
        {a#(lambda x, y) -> a#(x, p(1(), a(y, t()))),
         a#(lambda x, y) -> a#(y, t()),
          a#(a(x, y), z) -> a#(x, a(y, z)),
          a#(a(x, y), z) -> a#(y, z),
          a#(p(x, y), z) -> a#(x, z),
          a#(p(x, y), z) -> a#(y, z)}
       Weak:
       {      lambda x -> x,
               a(x, y) -> x,
               a(x, y) -> y,
        a(lambda x, y) -> lambda a(x, p(1(), a(y, t()))),
         a(a(x, y), z) -> a(x, a(y, z)),
         a(p(x, y), z) -> p(a(x, z), a(y, z)),
               p(x, y) -> x,
               p(x, y) -> y}
       Open