YES

TRS:

  and(true(),y) -> y
  and(false(),y) -> false()
  eq(nil(),nil()) -> true()
  eq(cons(t,l),nil()) -> false()
  eq(nil(),cons(t,l)) -> 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(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),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)))

max/plus interpretations on N:

  and_A(x1,x2) = max{39, -38 + x1, x2}
  and#_A(x1,x2) = max{0, -1 + x1, 0}
  true_A = 39
  true#_A = 3
  false_A = 37
  false#_A = 35
  eq_A(x1,x2) = max{1, 39, -38}
  eq#_A(x1,x2) = max{39, 2, 1}
  nil_A = 1
  nil#_A = 4
  cons_A(x1,x2) = max{1, 1, 1}
  cons#_A(x1,x2) = max{50, 34, 50}
  var_A(x1) = max{18, -6}
  var#_A(x1) = max{36, 16}
  apply_A(x1,x2) = max{38, 17 + x1, 22 + x2}
  apply#_A(x1,x2) = max{23, 18 + x1, 0}
  lambda_A(x1,x2) = max{27, 4, 11 + x2}
  lambda#_A(x1,x2) = max{5, 5 + x1, 50}
  if_A(x1,x2,x3) = max{18, -45 + x1, -1 + x2, -6}
  if#_A(x1,x2,x3) = max{15, -2 + x1, 36, 5 + x3}
  ren_A(x1,x2,x3) = max{16, 5, -6, x3}
  ren#_A(x1,x2,x3) = max{26, 24, 25, 23 + x3}

precedence:

  ren > cons = lambda = if > nil = var > true = false > eq = apply > and