MAYBE
Time: 0.012961
TRS:
 {                  and(true(), y) -> y,
                   and(false(), y) -> false(),
                  eq(nil(), nil()) -> true(),
             eq(nil(), cons(t, l)) -> false(),
             eq(cons(t, l), nil()) -> false(),
      eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')),
                 eq(var l, var l') -> eq(l, l'),
            eq(var l, apply(t, s)) -> false(),
           eq(var l, lambda(x, t)) -> false(),
            eq(apply(t, s), var l) -> false(),
    eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s')),
     eq(apply(t, s), lambda(x, t)) -> false(),
           eq(lambda(x, t), var l) -> false(),
     eq(lambda(x, t), apply(t, s)) -> false(),
  eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')),
         if(true(), var k, var l') -> var k,
        if(false(), var k, var l') -> var l',
            ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s)),
           ren(x, y, lambda(z, t)) -> lambda(var cons(x, cons(y, cons(lambda(z, t), nil()))), ren(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))),
         ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')}
 DP:
  DP:
   {    eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')),
        eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
        eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                   eq#(var l, var l') -> eq#(l, l'),
      eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')),
      eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
      eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
    eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')),
    eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
    eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'),
              ren#(x, y, apply(t, s)) -> ren#(x, y, t),
              ren#(x, y, apply(t, s)) -> ren#(x, y, s),
             ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
             ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t),
           ren#(var l, var k, var l') -> eq#(l, l'),
           ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l')}
  TRS:
  {                  and(true(), y) -> y,
                    and(false(), y) -> false(),
                   eq(nil(), nil()) -> true(),
              eq(nil(), cons(t, l)) -> false(),
              eq(cons(t, l), nil()) -> false(),
       eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')),
                  eq(var l, var l') -> eq(l, l'),
             eq(var l, apply(t, s)) -> false(),
            eq(var l, lambda(x, t)) -> false(),
             eq(apply(t, s), var l) -> false(),
     eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s')),
      eq(apply(t, s), lambda(x, t)) -> false(),
            eq(lambda(x, t), var l) -> false(),
      eq(lambda(x, t), apply(t, s)) -> false(),
   eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')),
          if(true(), var k, var l') -> var k,
         if(false(), var k, var l') -> var l',
             ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s)),
            ren(x, y, lambda(z, t)) -> lambda(var cons(x, cons(y, cons(lambda(z, t), nil()))), ren(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))),
          ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')}
  UR:
   {                  and(true(), y) -> y,
                     and(false(), y) -> false(),
                    eq(nil(), nil()) -> true(),
               eq(nil(), cons(t, l)) -> false(),
               eq(cons(t, l), nil()) -> false(),
        eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')),
                   eq(var l, var l') -> eq(l, l'),
              eq(var l, apply(t, s)) -> false(),
             eq(var l, lambda(x, t)) -> false(),
              eq(apply(t, s), var l) -> false(),
      eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s')),
       eq(apply(t, s), lambda(x, t)) -> false(),
             eq(lambda(x, t), var l) -> false(),
       eq(lambda(x, t), apply(t, s)) -> false(),
    eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')),
           if(true(), var k, var l') -> var k,
          if(false(), var k, var l') -> var l',
              ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s)),
             ren(x, y, lambda(z, t)) -> lambda(var cons(x, cons(y, cons(lambda(z, t), nil()))), ren(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))),
           ren(var l, var k, var l') -> if(eq(l, l'), var k, var l'),
                             a(w, v) -> w,
                             a(w, v) -> v}
   EDG:
    {
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(var l, var l') -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(var l, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(var l, var k, var l') -> eq#(l, l'))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
     (ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(s, s'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(var l, var k, var l') -> eq#(l, l'))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, t), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(apply(t, s), apply(t', s')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(t, t'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(var l, var k, var l') -> eq#(l, l'))
     (ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (ren#(var l, var k, var l') -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> and#(eq(t, t'), eq(l, l')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(cons(t, l), cons(t', l')) -> eq#(l, l'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(var l, var l') -> eq#(l, l'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> and#(eq(t, t'), eq(s, s')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(apply(t, s), apply(t', s')) -> eq#(s, s'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> and#(eq(x, x'), eq(t, t')))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'))
     (eq#(cons(t, l), cons(t', l')) -> eq#(l, l'), eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x'))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, apply(t, s)) -> ren#(x, y, t))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, apply(t, s)) -> ren#(x, y, s))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(var l, var k, var l') -> eq#(l, l'))
     (ren#(x, y, apply(t, s)) -> ren#(x, y, s), ren#(var l, var k, var l') -> if#(eq(l, l'), var k, var l'))
    }
    STATUS:
     arrows: 0.593750
     SCCS (2):
      Scc:
       { ren#(x, y, apply(t, s)) -> ren#(x, y, t),
         ren#(x, y, apply(t, s)) -> ren#(x, y, s),
        ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
        ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
      Scc:
       {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
            eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                       eq#(var l, var l') -> eq#(l, l'),
          eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
          eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
        eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
        eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
      
      SCC (4):
       Strict:
        { ren#(x, y, apply(t, s)) -> ren#(x, y, t),
          ren#(x, y, apply(t, s)) -> ren#(x, y, s),
         ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)),
         ren#(x, y, lambda(z, t)) -> ren#(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t)}
       Weak:
       {                  and(true(), y) -> y,
                         and(false(), y) -> false(),
                        eq(nil(), nil()) -> true(),
                   eq(nil(), cons(t, l)) -> false(),
                   eq(cons(t, l), nil()) -> false(),
            eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')),
                       eq(var l, var l') -> eq(l, l'),
                  eq(var l, apply(t, s)) -> false(),
                 eq(var l, lambda(x, t)) -> false(),
                  eq(apply(t, s), var l) -> false(),
          eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s')),
           eq(apply(t, s), lambda(x, t)) -> false(),
                 eq(lambda(x, t), var l) -> false(),
           eq(lambda(x, t), apply(t, s)) -> false(),
        eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')),
               if(true(), var k, var l') -> var k,
              if(false(), var k, var l') -> var l',
                  ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s)),
                 ren(x, y, lambda(z, t)) -> lambda(var cons(x, cons(y, cons(lambda(z, t), nil()))), ren(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))),
               ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')}
       Open
      
      
      SCC (7):
       Strict:
        {    eq#(cons(t, l), cons(t', l')) -> eq#(t, t'),
             eq#(cons(t, l), cons(t', l')) -> eq#(l, l'),
                        eq#(var l, var l') -> eq#(l, l'),
           eq#(apply(t, s), apply(t', s')) -> eq#(t, t'),
           eq#(apply(t, s), apply(t', s')) -> eq#(s, s'),
         eq#(lambda(x, t), lambda(x', t')) -> eq#(t, t'),
         eq#(lambda(x, t), lambda(x', t')) -> eq#(x, x')}
       Weak:
       {                  and(true(), y) -> y,
                         and(false(), y) -> false(),
                        eq(nil(), nil()) -> true(),
                   eq(nil(), cons(t, l)) -> false(),
                   eq(cons(t, l), nil()) -> false(),
            eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')),
                       eq(var l, var l') -> eq(l, l'),
                  eq(var l, apply(t, s)) -> false(),
                 eq(var l, lambda(x, t)) -> false(),
                  eq(apply(t, s), var l) -> false(),
          eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s')),
           eq(apply(t, s), lambda(x, t)) -> false(),
                 eq(lambda(x, t), var l) -> false(),
           eq(lambda(x, t), apply(t, s)) -> false(),
        eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')),
               if(true(), var k, var l') -> var k,
              if(false(), var k, var l') -> var l',
                  ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s)),
                 ren(x, y, lambda(z, t)) -> lambda(var cons(x, cons(y, cons(lambda(z, t), nil()))), ren(x, y, ren(z, var cons(x, cons(y, cons(lambda(z, t), nil()))), t))),
               ren(var l, var k, var l') -> if(eq(l, l'), var k, var l')}
       Open