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