MAYBE
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:
  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}
  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))}
   SCCS:
    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:
     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}
     Fail