Input TRS:
    1: and(true(),y) -> y
    2: and(false(),y) -> false()
    3: eq(nil(),nil()) -> true()
    4: eq(cons(t,l),nil()) -> false()
    5: eq(nil(),cons(t,l)) -> false()
    6: eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
    7: eq(var(l),var(l')) -> eq(l,l')
    8: eq(var(l),apply(t,s)) -> false()
    9: eq(var(l),lambda(x,t)) -> false()
    10: eq(apply(t,s),var(l)) -> false()
    11: eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
    12: eq(apply(t,s),lambda(x,t)) -> false()
    13: eq(lambda(x,t),var(l)) -> false()
    14: eq(lambda(x,t),apply(t,s)) -> false()
    15: eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
    16: if(true(),var(k),var(l')) -> var(k)
    17: if(false(),var(k),var(l')) -> var(l')
    18: ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
    19: ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
    20: 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)))
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #eq(cons(t,l),cons(t',l')) -> #and(eq(t,t'),eq(l,l'))
   #2: #eq(cons(t,l),cons(t',l')) -> #eq(t,t')
   #3: #eq(cons(t,l),cons(t',l')) -> #eq(l,l')
   #4: #eq(apply(t,s),apply(t',s')) -> #and(eq(t,t'),eq(s,s'))
   #5: #eq(apply(t,s),apply(t',s')) -> #eq(t,t')
   #6: #eq(apply(t,s),apply(t',s')) -> #eq(s,s')
   #7: #ren(x,y,lambda(z,t)) -> #ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
   #8: #ren(x,y,lambda(z,t)) -> #ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
   #9: #eq(var(l),var(l')) -> #eq(l,l')
   #10: #ren(x,y,apply(t,s)) -> #ren(x,y,t)
   #11: #ren(x,y,apply(t,s)) -> #ren(x,y,s)
   #12: #eq(lambda(x,t),lambda(x',t')) -> #and(eq(x,x'),eq(t,t'))
   #13: #eq(lambda(x,t),lambda(x',t')) -> #eq(x,x')
   #14: #eq(lambda(x,t),lambda(x',t')) -> #eq(t,t')
   #15: #ren(var(l),var(k),var(l')) -> #if(eq(l,l'),var(k),var(l'))
   #16: #ren(var(l),var(k),var(l')) -> #eq(l,l')
Number of SCCs: 2, DPs: 11, edges: 65
	SCC { #7 #8 #10 #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 apply(x1,x2)	weight: (/ 1 4) + x1 + x2
   ren(x1,x2,x3)	weight: x3
   and(x1,x2)	weight: (/ 1 2)
    eq(x1,x2)	weight: (/ 1 4)
lambda(x1,x2)	weight: (/ 1 4) + x1 + x2
 false()	weight: 0
  true()	weight: 0
  #eq(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
   nil()	weight: 0
 #ren(x1,x2,x3)	weight: x3
  cons(x1,x2)	weight: (/ 1 4)
  #if(x1,x2,x3)	weight: 0
   var(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 16..20 }
    Removed DPs: #7 #8 #10 #11
Number of SCCs: 1, DPs: 7, edges: 49
	SCC { #2 #3 #5 #6 #9 #13 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 apply(x1,x2)	weight: (/ 1 8) + x1 + x2
   ren(x1,x2,x3)	weight: x3
   and(x1,x2)	weight: (/ 3 8)
    eq(x1,x2)	weight: (/ 1 8) + x2
lambda(x1,x2)	weight: (/ 1 8) + x1 + x2
 false()	weight: 0
  true()	weight: 0
  #eq(x1,x2)	weight: x1 + x2
    if(x1,x2,x3)	weight: (/ 1 8)
   nil()	weight: 0
 #ren(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
  #if(x1,x2,x3)	weight: 0
   var(x1)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #2 #3 #5 #6 #9 #13 #14
Number of SCCs: 0, DPs: 0, edges: 0
YES