MAYBE
Time: 0.002556
TRS:
 { 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(1(), p(x, y)) -> x,
     a(1(), id()) -> 1(),
  a(t(), p(x, y)) -> y,
     a(t(), id()) -> t(),
       a(id(), x) -> x}
 DP:
  DP:
   {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)}
  TRS:
  { 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(1(), p(x, y)) -> x,
      a(1(), id()) -> 1(),
   a(t(), p(x, y)) -> y,
      a(t(), id()) -> t(),
        a(id(), x) -> x}
  UR:
   { 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(1(), p(x, y)) -> x,
       a(1(), id()) -> 1(),
    a(t(), p(x, y)) -> y,
       a(t(), id()) -> t(),
         a(id(), x) -> x,
            b(w, v) -> w,
            b(w, v) -> v}
   EDG:
    {(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) -> 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#(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) -> a#(y, t()))
     (a#(p(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, p(1(), a(y, t()))))
     (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) -> a#(x, z))
     (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> 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#(y, t()), a#(lambda x, y) -> 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#(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#(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#(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#(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#(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) -> a#(y, t()))
     (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#(a(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#(p(x, y), z) -> a#(y, z))}
    STATUS:
     arrows: 0.000000
     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:
       { 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(1(), p(x, y)) -> x,
           a(1(), id()) -> 1(),
        a(t(), p(x, y)) -> y,
           a(t(), id()) -> t(),
             a(id(), x) -> x}
       Open