MAYBE
Time: 0.002494
TRS:
 {      lambda x -> x,
         a(x, y) -> x,
         a(x, y) -> y,
  a(lambda x, y) -> lambda a(x, a(y, t())),
  a(lambda x, y) -> lambda a(x, 1()),
   a(a(x, y), z) -> a(x, a(y, z))}
 DP:
  DP:
   {a#(lambda x, y) -> lambda# a(x, a(y, t())),
    a#(lambda x, y) -> lambda# a(x, 1()),
    a#(lambda x, y) -> a#(x, a(y, t())),
    a#(lambda x, y) -> a#(x, 1()),
    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)}
  TRS:
  {      lambda x -> x,
          a(x, y) -> x,
          a(x, y) -> y,
   a(lambda x, y) -> lambda a(x, a(y, t())),
   a(lambda x, y) -> lambda a(x, 1()),
    a(a(x, y), z) -> a(x, a(y, z))}
  UR:
   {      lambda x -> x,
           a(x, y) -> x,
           a(x, y) -> y,
    a(lambda x, y) -> lambda a(x, a(y, t())),
    a(lambda x, y) -> lambda a(x, 1()),
     a(a(x, y), z) -> a(x, a(y, z))}
   EDG:
    {(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, 1()))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, a(y, t())))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, 1()))
     (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, a(y, t())))
     (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, 1()))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, a(y, t())))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, 1()))
     (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, a(y, t())))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, a(y, t())))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1()))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, a(y, t())))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1()))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(y, t()))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, a(y, t())))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, 1()))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, a(y, t())))
     (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, 1()))
     (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#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, a(y, t())))
     (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, 1()))
     (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, a(y, t())))
     (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, 1()))
     (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t()))
     (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z)))
     (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))}
    STATUS:
     arrows: 0.285714
     SCCS (1):
      Scc:
       {a#(lambda x, y) -> a#(x, a(y, t())),
        a#(lambda x, y) -> a#(x, 1()),
        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)}
      
      SCC (5):
       Strict:
        {a#(lambda x, y) -> a#(x, a(y, t())),
         a#(lambda x, y) -> a#(x, 1()),
         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)}
       Weak:
       {      lambda x -> x,
               a(x, y) -> x,
               a(x, y) -> y,
        a(lambda x, y) -> lambda a(x, a(y, t())),
        a(lambda x, y) -> lambda a(x, 1()),
         a(a(x, y), z) -> a(x, a(y, z))}
       Open