YES

TRS:

  a__and(true(),X) -> mark(X)
  a__and(false(),Y) -> false()
  a__if(true(),X,Y) -> mark(X)
  a__if(false(),X,Y) -> mark(Y)
  a__add(0(),X) -> mark(X)
  a__add(s(X),Y) -> s(add(X,Y))
  a__first(0(),X) -> nil()
  a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
  a__from(X) -> cons(X,from(s(X)))
  mark(and(X1,X2)) -> a__and(mark(X1),X2)
  mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
  mark(add(X1,X2)) -> a__add(mark(X1),X2)
  mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
  mark(from(X)) -> a__from(X)
  mark(true()) -> true()
  mark(false()) -> false()
  mark(0()) -> 0()
  mark(s(X)) -> s(X)
  mark(nil()) -> nil()
  mark(cons(X1,X2)) -> cons(X1,X2)
  a__and(X1,X2) -> and(X1,X2)
  a__if(X1,X2,X3) -> if(X1,X2,X3)
  a__add(X1,X2) -> add(X1,X2)
  a__first(X1,X2) -> first(X1,X2)
  a__from(X) -> from(X)

max/plus interpretations on N:

  a__and_A(x1,x2) = max{29, 34 + x1, 35 + x2}
  a__and#_A(x1,x2) = max{29, 34 + x1, 35 + x2}
  true_A = 0
  true#_A = 0
  mark_A(x1) = max{30, 32 + x1}
  mark#_A(x1) = max{30, 32 + x1}
  false_A = 0
  false#_A = 0
  a__if_A(x1,x2,x3) = max{67, 34 + x1, 33 + x2, 33 + x3}
  a__if#_A(x1,x2,x3) = max{67, 34 + x1, 33 + x2, 33 + x3}
  a__add_A(x1,x2) = max{64, 44 + x1, 63 + x2}
  a__add#_A(x1,x2) = max{64, 44 + x1, 63 + x2}
  0_A = 1
  0#_A = 1
  s_A(x1) = max{21, 11 + x1}
  s#_A(x1) = max{21, 11 + x1}
  add_A(x1,x2) = max{54, 44 + x1, 31 + x2}
  add#_A(x1,x2) = max{54, 44 + x1, 31 + x2}
  a__first_A(x1,x2) = max{35, 34 + x1, 31 + x2}
  a__first#_A(x1,x2) = max{35, 34 + x1, 31 + x2}
  nil_A = 0
  nil#_A = 0
  cons_A(x1,x2) = max{29, x1, 8 + x2}
  cons#_A(x1,x2) = max{29, x1, 8 + x2}
  first_A(x1,x2) = max{28, 34 + x1, 31 + x2}
  first#_A(x1,x2) = max{28, 34 + x1, 31 + x2}
  a__from_A(x1) = max{29, 20 + x1}
  a__from#_A(x1) = max{29, 20 + x1}
  from_A(x1) = max{21, x1}
  from#_A(x1) = max{21, x1}
  and_A(x1,x2) = max{35, 34 + x1, 31 + x2}
  and#_A(x1,x2) = max{35, 34 + x1, 31 + x2}
  if_A(x1,x2,x3) = max{35, 34 + x1, 31 + x2, 31 + x3}
  if#_A(x1,x2,x3) = max{35, 34 + x1, 31 + x2, 31 + x3}

precedence:

  nil > mark > true = false = a__if = a__add = 0 = a__first = a__from > a__and = s = add = cons = first = from = if > and