YES

Problem:
 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)

Proof:
 DP Processor:
  DPs:
   a__and#(true(),X) -> mark#(X)
   a__if#(true(),X,Y) -> mark#(X)
   a__if#(false(),X,Y) -> mark#(Y)
   a__add#(0(),X) -> mark#(X)
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> a__add#(mark(X1),X2)
   mark#(first(X1,X2)) -> mark#(X2)
   mark#(first(X1,X2)) -> mark#(X1)
   mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
   mark#(from(X)) -> a__from#(X)
  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)
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    
   interpretation:
    [a__from#](x0) = 0,
    
    [a__first#](x0, x1) = 2,
    
    [a__add#](x0, x1) = 4x1 + 0,
    
    [a__if#](x0, x1, x2) = 2x1 + 2x2,
    
    [mark#](x0) = x0,
    
    [a__and#](x0, x1) = 4x1 + 0,
    
    [if](x0, x1, x2) = 2x0 + 3x1 + 4x2 + 0,
    
    [and](x0, x1) = 2x0 + 7x1 + 7,
    
    [from](x0) = x0 + 1,
    
    [a__from](x0) = x0 + 0,
    
    [first](x0, x1) = 2x0 + 4x1 + 3,
    
    [cons](x0, x1) = x0 + x1 + 2,
    
    [nil] = 0,
    
    [a__first](x0, x1) = 1x0 + 2x1 + 4,
    
    [add](x0, x1) = 2x0 + 5x1 + 4,
    
    [s](x0) = x0 + 1,
    
    [a__add](x0, x1) = 2x0 + x1 + 8,
    
    [0] = 1,
    
    [a__if](x0, x1, x2) = 5x0 + x1 + x2 + 8,
    
    [false] = 0,
    
    [mark](x0) = 1,
    
    [a__and](x0, x1) = x1 + 4,
    
    [true] = 2
   orientation:
    a__and#(true(),X) = 4X + 0 >= X = mark#(X)
    
    a__if#(true(),X,Y) = 2X + 2Y >= X = mark#(X)
    
    a__if#(false(),X,Y) = 2X + 2Y >= Y = mark#(Y)
    
    a__add#(0(),X) = 4X + 0 >= X = mark#(X)
    
    mark#(and(X1,X2)) = 2X1 + 7X2 + 7 >= X1 = mark#(X1)
    
    mark#(and(X1,X2)) = 2X1 + 7X2 + 7 >= 4X2 + 0 = a__and#(mark(X1),X2)
    
    mark#(if(X1,X2,X3)) = 2X1 + 3X2 + 4X3 + 0 >= X1 = mark#(X1)
    
    mark#(if(X1,X2,X3)) = 2X1 + 3X2 + 4X3 + 0 >= 2X2 + 2X3 = a__if#(mark(X1),X2,X3)
    
    mark#(add(X1,X2)) = 2X1 + 5X2 + 4 >= X1 = mark#(X1)
    
    mark#(add(X1,X2)) = 2X1 + 5X2 + 4 >= 4X2 + 0 = a__add#(mark(X1),X2)
    
    mark#(first(X1,X2)) = 2X1 + 4X2 + 3 >= X2 = mark#(X2)
    
    mark#(first(X1,X2)) = 2X1 + 4X2 + 3 >= X1 = mark#(X1)
    
    mark#(first(X1,X2)) = 2X1 + 4X2 + 3 >= 2 = a__first#(mark(X1),mark(X2))
    
    mark#(from(X)) = X + 1 >= 0 = a__from#(X)
    
    a__and(true(),X) = X + 4 >= 1 = mark(X)
    
    a__and(false(),Y) = Y + 4 >= 0 = false()
    
    a__if(true(),X,Y) = X + Y + 8 >= 1 = mark(X)
    
    a__if(false(),X,Y) = X + Y + 8 >= 1 = mark(Y)
    
    a__add(0(),X) = X + 8 >= 1 = mark(X)
    
    a__add(s(X),Y) = 2X + Y + 8 >= 2X + 5Y + 4 = s(add(X,Y))
    
    a__first(0(),X) = 2X + 4 >= 0 = nil()
    
    a__first(s(X),cons(Y,Z)) = 1X + 2Y + 2Z + 4 >= 2X + Y + 4Z + 3 = cons(Y,first(X,Z))
    
    a__from(X) = X + 0 >= X + 2 = cons(X,from(s(X)))
    
    mark(and(X1,X2)) = 1 >= X2 + 4 = a__and(mark(X1),X2)
    
    mark(if(X1,X2,X3)) = 1 >= X2 + X3 + 8 = a__if(mark(X1),X2,X3)
    
    mark(add(X1,X2)) = 1 >= X2 + 8 = a__add(mark(X1),X2)
    
    mark(first(X1,X2)) = 1 >= 4 = a__first(mark(X1),mark(X2))
    
    mark(from(X)) = 1 >= X + 0 = a__from(X)
    
    mark(true()) = 1 >= 2 = true()
    
    mark(false()) = 1 >= 0 = false()
    
    mark(0()) = 1 >= 1 = 0()
    
    mark(s(X)) = 1 >= X + 1 = s(X)
    
    mark(nil()) = 1 >= 0 = nil()
    
    mark(cons(X1,X2)) = 1 >= X1 + X2 + 2 = cons(X1,X2)
    
    a__and(X1,X2) = X2 + 4 >= 2X1 + 7X2 + 7 = and(X1,X2)
    
    a__if(X1,X2,X3) = 5X1 + X2 + X3 + 8 >= 2X1 + 3X2 + 4X3 + 0 = if(X1,X2,X3)
    
    a__add(X1,X2) = 2X1 + X2 + 8 >= 2X1 + 5X2 + 4 = add(X1,X2)
    
    a__first(X1,X2) = 1X1 + 2X2 + 4 >= 2X1 + 4X2 + 3 = first(X1,X2)
    
    a__from(X) = X + 0 >= X + 1 = from(X)
   problem:
    DPs:
     
    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)
   Qed