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{21, 21 + x1, 41 + x2}
  a__and#_A(x1,x2) = max{20, 21, 18 + x2}
  true_A = 1
  true#_A = 16
  mark_A(x1) = max{13, 22 + x1}
  mark#_A(x1) = max{16, 1 + x1}
  false_A = 42
  false#_A = 19
  a__if_A(x1,x2,x3) = max{0, 11 + x1, 40 + x2, 34 + x3}
  a__if#_A(x1,x2,x3) = max{11, 21, 19 + x2, 17 + x3}
  a__add_A(x1,x2) = max{41, x1, 41 + x2}
  a__add#_A(x1,x2) = max{17, -1, 18 + x2}
  0_A = 1
  0#_A = 15
  s_A(x1) = max{14, 1 + x1}
  s#_A(x1) = max{16, -2}
  add_A(x1,x2) = max{18, x1, 19 + x2}
  add#_A(x1,x2) = max{0, -2, 17}
  a__first_A(x1,x2) = max{81, 82 + x1, 58 + x2}
  a__first#_A(x1,x2) = max{18, 20, 26 + x2}
  nil_A = 0
  nil#_A = 14
  cons_A(x1,x2) = max{97, 10, -6 + x2}
  cons#_A(x1,x2) = max{13, 12, 15}
  first_A(x1,x2) = max{48, 82 + x1, 58 + x2}
  first#_A(x1,x2) = max{19, 17, x2}
  a__from_A(x1) = max{97, 9}
  a__from#_A(x1) = max{14, 16}
  from_A(x1) = max{75, 15}
  from#_A(x1) = max{16, 13}
  and_A(x1,x2) = max{18, 21 + x1, 21 + x2}
  and#_A(x1,x2) = max{21, 21, 17}
  if_A(x1,x2,x3) = max{1, 11 + x1, 21 + x2, 17 + x3}
  if#_A(x1,x2,x3) = max{15, 20, 18, 10}

precedence:

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