MAYBE
Time: 0.018779
TRS:
 {           and(false(), false()) -> false(),
              and(false(), true()) -> false(),
              and(true(), false()) -> false(),
               and(true(), true()) -> true(),
                  eq(nil(), nil()) -> true(),
             eq(nil(), cons(T, L)) -> false(),
             eq(cons(T, L), nil()) -> false(),
      eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)),
                 eq(var L, var Lp) -> eq(L, Lp),
            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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)),
    eq(apply(T, S), lambda(X, Tp)) -> false(),
           eq(lambda(X, T), var L) -> false(),
   eq(lambda(X, T), apply(Tp, Sp)) -> false(),
  eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)),
         if(false(), var K, var L) -> var L,
          if(true(), var K, var L) -> var K,
            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 Lp) -> if(eq(L, Lp), var K, var Lp)}
 DP:
  DP:
   {    eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)),
        eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
        eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                   eq#(var L, var Lp) -> eq#(L, Lp),
      eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)),
      eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
      eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
    eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)),
    eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp),
    eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp),
              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 Lp) -> eq#(L, Lp),
           ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp)}
  TRS:
  {           and(false(), false()) -> false(),
               and(false(), true()) -> false(),
               and(true(), false()) -> false(),
                and(true(), true()) -> true(),
                   eq(nil(), nil()) -> true(),
              eq(nil(), cons(T, L)) -> false(),
              eq(cons(T, L), nil()) -> false(),
       eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)),
                  eq(var L, var Lp) -> eq(L, Lp),
             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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)),
     eq(apply(T, S), lambda(X, Tp)) -> false(),
            eq(lambda(X, T), var L) -> false(),
    eq(lambda(X, T), apply(Tp, Sp)) -> false(),
   eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)),
          if(false(), var K, var L) -> var L,
           if(true(), var K, var L) -> var K,
             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 Lp) -> if(eq(L, Lp), var K, var Lp)}
  EDG:
   {
    (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
    (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> eq#(L, Lp))
    (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#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (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 Lp) -> eq#(L, Lp))
    (ren#(X, Y, apply(T, S)) -> ren#(X, Y, S), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(var L, var Lp) -> eq#(L, Lp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
    (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
    (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, 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, 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#(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#(var L, var K, var Lp) -> eq#(L, Lp))
    (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
    (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 Lp) -> eq#(L, Lp))
    (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
   }
   EDG:
    {
     (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
     (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> eq#(L, Lp))
     (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#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (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 Lp) -> eq#(L, Lp))
     (ren#(X, Y, apply(T, S)) -> ren#(X, Y, S), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(var L, var Lp) -> eq#(L, Lp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
     (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
     (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, 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, 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#(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#(var L, var K, var Lp) -> eq#(L, Lp))
     (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
     (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 Lp) -> eq#(L, Lp))
     (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
    }
    EDG:
     {
      (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
      (ren#(X, Y, apply(T, S)) -> ren#(X, Y, T), ren#(var L, var K, var Lp) -> eq#(L, Lp))
      (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#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (ren#(var L, var K, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (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 Lp) -> eq#(L, Lp))
      (ren#(X, Y, apply(T, S)) -> ren#(X, Y, S), ren#(var L, var K, var Lp) -> if#(eq(L, Lp), var K, var Lp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(var L, var Lp) -> eq#(L, Lp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> and#(eq(T, Tp), eq(L, Lp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(var L, var Lp) -> eq#(L, Lp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> and#(eq(T, Tp), eq(S, Sp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> and#(eq(T, Tp), eq(X, Xp)))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp))
      (eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp), eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp))
      (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, 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, 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#(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#(var L, var K, var Lp) -> eq#(L, Lp))
      (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
      (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 Lp) -> eq#(L, Lp))
      (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 Lp) -> if#(eq(L, Lp), var K, var Lp))
     }
     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(Tp, Lp)) -> eq#(T, Tp),
             eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                        eq#(var L, var Lp) -> eq#(L, Lp),
           eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
           eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
         eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp),
         eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
       
       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(false(), false()) -> false(),
                     and(false(), true()) -> false(),
                     and(true(), false()) -> false(),
                      and(true(), true()) -> true(),
                         eq(nil(), nil()) -> true(),
                    eq(nil(), cons(T, L)) -> false(),
                    eq(cons(T, L), nil()) -> false(),
             eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)),
                        eq(var L, var Lp) -> eq(L, Lp),
                   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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)),
           eq(apply(T, S), lambda(X, Tp)) -> false(),
                  eq(lambda(X, T), var L) -> false(),
          eq(lambda(X, T), apply(Tp, Sp)) -> false(),
         eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)),
                if(false(), var K, var L) -> var L,
                 if(true(), var K, var L) -> var K,
                   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 Lp) -> if(eq(L, Lp), var K, var Lp)}
        Open
       
       
       SCC (7):
        Strict:
         {    eq#(cons(T, L), cons(Tp, Lp)) -> eq#(T, Tp),
              eq#(cons(T, L), cons(Tp, Lp)) -> eq#(L, Lp),
                         eq#(var L, var Lp) -> eq#(L, Lp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(T, Tp),
            eq#(apply(T, S), apply(Tp, Sp)) -> eq#(S, Sp),
          eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(T, Tp),
          eq#(lambda(X, T), lambda(Xp, Tp)) -> eq#(X, Xp)}
        Weak:
        {           and(false(), false()) -> false(),
                     and(false(), true()) -> false(),
                     and(true(), false()) -> false(),
                      and(true(), true()) -> true(),
                         eq(nil(), nil()) -> true(),
                    eq(nil(), cons(T, L)) -> false(),
                    eq(cons(T, L), nil()) -> false(),
             eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)),
                        eq(var L, var Lp) -> eq(L, Lp),
                   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(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)),
           eq(apply(T, S), lambda(X, Tp)) -> false(),
                  eq(lambda(X, T), var L) -> false(),
          eq(lambda(X, T), apply(Tp, Sp)) -> false(),
         eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)),
                if(false(), var K, var L) -> var L,
                 if(true(), var K, var L) -> var K,
                   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 Lp) -> if(eq(L, Lp), var K, var Lp)}
        Open