YES

Problem:
 active(and(true(),X)) -> mark(X)
 active(and(false(),Y)) -> mark(false())
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(add(0(),X)) -> mark(X)
 active(add(s(X),Y)) -> mark(s(add(X,Y)))
 active(first(0(),X)) -> mark(nil())
 active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
 active(from(X)) -> mark(cons(X,from(s(X))))
 mark(and(X1,X2)) -> active(and(mark(X1),X2))
 mark(true()) -> active(true())
 mark(false()) -> active(false())
 mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
 mark(add(X1,X2)) -> active(add(mark(X1),X2))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(X))
 mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
 mark(nil()) -> active(nil())
 mark(cons(X1,X2)) -> active(cons(X1,X2))
 mark(from(X)) -> active(from(X))
 and(mark(X1),X2) -> and(X1,X2)
 and(X1,mark(X2)) -> and(X1,X2)
 and(active(X1),X2) -> and(X1,X2)
 and(X1,active(X2)) -> and(X1,X2)
 if(mark(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,mark(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,mark(X3)) -> if(X1,X2,X3)
 if(active(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,active(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,active(X3)) -> if(X1,X2,X3)
 add(mark(X1),X2) -> add(X1,X2)
 add(X1,mark(X2)) -> add(X1,X2)
 add(active(X1),X2) -> add(X1,X2)
 add(X1,active(X2)) -> add(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 first(mark(X1),X2) -> first(X1,X2)
 first(X1,mark(X2)) -> first(X1,X2)
 first(active(X1),X2) -> first(X1,X2)
 first(X1,active(X2)) -> first(X1,X2)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)

Proof:
 DP Processor:
  DPs:
   active#(and(true(),X)) -> mark#(X)
   active#(and(false(),Y)) -> mark#(false())
   active#(if(true(),X,Y)) -> mark#(X)
   active#(if(false(),X,Y)) -> mark#(Y)
   active#(add(0(),X)) -> mark#(X)
   active#(add(s(X),Y)) -> add#(X,Y)
   active#(add(s(X),Y)) -> s#(add(X,Y))
   active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
   active#(first(0(),X)) -> mark#(nil())
   active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
   active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
   active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
   active#(from(X)) -> s#(X)
   active#(from(X)) -> from#(s(X))
   active#(from(X)) -> cons#(X,from(s(X)))
   active#(from(X)) -> mark#(cons(X,from(s(X))))
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(true()) -> active#(true())
   mark#(false()) -> active#(false())
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
   mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> add#(mark(X1),X2)
   mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> active#(s(X))
   mark#(first(X1,X2)) -> mark#(X2)
   mark#(first(X1,X2)) -> mark#(X1)
   mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
   mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
   mark#(nil()) -> active#(nil())
   mark#(cons(X1,X2)) -> active#(cons(X1,X2))
   mark#(from(X)) -> active#(from(X))
   and#(mark(X1),X2) -> and#(X1,X2)
   and#(X1,mark(X2)) -> and#(X1,X2)
   and#(active(X1),X2) -> and#(X1,X2)
   and#(X1,active(X2)) -> and#(X1,X2)
   if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
   if#(active(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,active(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
   add#(mark(X1),X2) -> add#(X1,X2)
   add#(X1,mark(X2)) -> add#(X1,X2)
   add#(active(X1),X2) -> add#(X1,X2)
   add#(X1,active(X2)) -> add#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   first#(mark(X1),X2) -> first#(X1,X2)
   first#(X1,mark(X2)) -> first#(X1,X2)
   first#(active(X1),X2) -> first#(X1,X2)
   first#(X1,active(X2)) -> first#(X1,X2)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   cons#(X1,mark(X2)) -> cons#(X1,X2)
   cons#(active(X1),X2) -> cons#(X1,X2)
   cons#(X1,active(X2)) -> cons#(X1,X2)
   from#(mark(X)) -> from#(X)
   from#(active(X)) -> from#(X)
  TRS:
   active(and(true(),X)) -> mark(X)
   active(and(false(),Y)) -> mark(false())
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   active(add(0(),X)) -> mark(X)
   active(add(s(X),Y)) -> mark(s(add(X,Y)))
   active(first(0(),X)) -> mark(nil())
   active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
   active(from(X)) -> mark(cons(X,from(s(X))))
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(true()) -> active(true())
   mark(false()) -> active(false())
   mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
   mark(add(X1,X2)) -> active(add(mark(X1),X2))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(X))
   mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
   mark(nil()) -> active(nil())
   mark(cons(X1,X2)) -> active(cons(X1,X2))
   mark(from(X)) -> active(from(X))
   and(mark(X1),X2) -> and(X1,X2)
   and(X1,mark(X2)) -> and(X1,X2)
   and(active(X1),X2) -> and(X1,X2)
   and(X1,active(X2)) -> and(X1,X2)
   if(mark(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,mark(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,mark(X3)) -> if(X1,X2,X3)
   if(active(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,active(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,active(X3)) -> if(X1,X2,X3)
   add(mark(X1),X2) -> add(X1,X2)
   add(X1,mark(X2)) -> add(X1,X2)
   add(active(X1),X2) -> add(X1,X2)
   add(X1,active(X2)) -> add(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   first(mark(X1),X2) -> first(X1,X2)
   first(X1,mark(X2)) -> first(X1,X2)
   first(active(X1),X2) -> first(X1,X2)
   first(X1,active(X2)) -> first(X1,X2)
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
  Matrix Interpretation Processor: dim=2
   
   usable rules:
    active(and(true(),X)) -> mark(X)
    active(and(false(),Y)) -> mark(false())
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    active(add(0(),X)) -> mark(X)
    active(add(s(X),Y)) -> mark(s(add(X,Y)))
    active(first(0(),X)) -> mark(nil())
    active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
    active(from(X)) -> mark(cons(X,from(s(X))))
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(true()) -> active(true())
    mark(false()) -> active(false())
    mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    mark(add(X1,X2)) -> active(add(mark(X1),X2))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(X))
    mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
    mark(nil()) -> active(nil())
    mark(cons(X1,X2)) -> active(cons(X1,X2))
    mark(from(X)) -> active(from(X))
    and(mark(X1),X2) -> and(X1,X2)
    and(X1,mark(X2)) -> and(X1,X2)
    and(active(X1),X2) -> and(X1,X2)
    and(X1,active(X2)) -> and(X1,X2)
    if(mark(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,mark(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,mark(X3)) -> if(X1,X2,X3)
    if(active(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,active(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,active(X3)) -> if(X1,X2,X3)
    add(mark(X1),X2) -> add(X1,X2)
    add(X1,mark(X2)) -> add(X1,X2)
    add(active(X1),X2) -> add(X1,X2)
    add(X1,active(X2)) -> add(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    first(mark(X1),X2) -> first(X1,X2)
    first(X1,mark(X2)) -> first(X1,X2)
    first(active(X1),X2) -> first(X1,X2)
    first(X1,active(X2)) -> first(X1,X2)
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
   interpretation:
    [if#](x0, x1, x2) = [1 0]x0 + [1 0]x1 + [3 0]x2 + [2],
    
    [and#](x0, x1) = [1 0]x0 + [1 0]x1,
    
    [from#](x0) = [2 0]x0 + [2],
    
    [cons#](x0, x1) = [2 0]x0 + [2 0]x1,
    
    [first#](x0, x1) = [2 0]x0 + [1 0]x1,
    
    [s#](x0) = [2 0]x0 + [1],
    
    [add#](x0, x1) = [1 0]x0 + [1 0]x1,
    
    [mark#](x0) = [0 2]x0 + [1],
    
    [active#](x0) = [0 1]x0,
    
                 [0 0]     [1]
    [from](x0) = [2 2]x0 + [3],
    
                     [0 0]     [1 0]  
    [cons](x0, x1) = [1 1]x0 + [0 0]x1,
    
            [0]
    [nil] = [0],
    
                      [0 0]     [0 0]     [0]
    [first](x0, x1) = [1 2]x0 + [1 2]x1 + [2],
    
              [0 0]  
    [s](x0) = [1 0]x0,
    
                    [0 0]     [1 0]     [0]
    [add](x0, x1) = [2 1]x0 + [2 2]x1 + [2],
    
          [1]
    [0] = [2],
    
                       [0 0]     [1 2]     [2 0]     [2]
    [if](x0, x1, x2) = [1 1]x0 + [2 3]x1 + [2 2]x2 + [3],
    
              [0]
    [false] = [0],
    
                 [1 0]     [1]
    [mark](x0) = [0 2]x0 + [0],
    
                        [1]
    [active](x0) = x0 + [0],
    
                    [0 0]     [1 0]     [3]
    [and](x0, x1) = [1 1]x0 + [2 3]x1 + [2],
    
             [0]
    [true] = [2]
   orientation:
    active#(and(true(),X)) = [2 3]X + [4] >= [0 2]X + [1] = mark#(X)
    
    active#(and(false(),Y)) = [2 3]Y + [2] >= [1] = mark#(false())
    
    active#(if(true(),X,Y)) = [2 3]X + [2 2]Y + [5] >= [0 2]X + [1] = mark#(X)
    
    active#(if(false(),X,Y)) = [2 3]X + [2 2]Y + [3] >= [0 2]Y + [1] = mark#(Y)
    
    active#(add(0(),X)) = [2 2]X + [6] >= [0 2]X + [1] = mark#(X)
    
    active#(add(s(X),Y)) = [1 0]X + [2 2]Y + [2] >= [1 0]X + [1 0]Y = add#(X,Y)
    
    active#(add(s(X),Y)) = [1 0]X + [2 2]Y + [2] >= [2 0]Y + [1] = s#(add(X,Y))
    
    active#(add(s(X),Y)) = [1 0]X + [2 2]Y + [2] >= [2 0]Y + [1] = mark#(s(add(X,Y)))
    
    active#(first(0(),X)) = [1 2]X + [7] >= [1] = mark#(nil())
    
    active#(first(s(X),cons(Y,Z))) = [2 0]X + [2 2]Y + [1 0]Z + [2] >= [2 0]X + [1 0]Z = first#(X,Z)
    
    active#(first(s(X),cons(Y,Z))) = [2 0]X + [2 2]Y + [1 0]Z + [2] >= [2 0]Y = cons#(Y,first(X,Z))
    
    active#(first(s(X),cons(Y,Z))) = [2 0]X + [2 2]Y + [1 0]Z + [2] >= [2 2]Y + [1] = mark#(cons(Y,first(X,Z)))
    
    active#(from(X)) = [2 2]X + [3] >= [2 0]X + [1] = s#(X)
    
    active#(from(X)) = [2 2]X + [3] >= [2] = from#(s(X))
    
    active#(from(X)) = [2 2]X + [3] >= [2 0]X + [2] = cons#(X,from(s(X)))
    
    active#(from(X)) = [2 2]X + [3] >= [2 2]X + [1] = mark#(cons(X,from(s(X))))
    
    mark#(and(X1,X2)) = [2 2]X1 + [4 6]X2 + [5] >= [0 2]X1 + [1] = mark#(X1)
    
    mark#(and(X1,X2)) = [2 2]X1 + [4 6]X2 + [5] >= [1 0]X1 + [1 0]X2 + [1] = and#(mark(X1),X2)
    
    mark#(and(X1,X2)) = [2 2]X1 + [4 6]X2 + [5] >= [1 2]X1 + [2 3]X2 + [3] = active#(and(mark(X1),X2))
    
    mark#(true()) = 5 >= 2 = active#(true())
    
    mark#(false()) = 1 >= 0 = active#(false())
    
    mark#(if(X1,X2,X3)) = [2 2]X1 + [4 6]X2 + [4 4]X3 + [7] >= [0 2]X1 + [1] = mark#(X1)
    
    mark#(if(X1,X2,X3)) = [2 2]X1 + [4 6]X2 + [4 4]X3 + [7] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [3] = if#(mark(X1),X2,X3)
    
    mark#(if(X1,X2,X3)) = [2 2]X1 + [4 6]X2 + [4 4]X3 + [7] >= [1 2]X1 + [2 3]X2 + [2 2]X3 + [4] = active#(if(mark(X1),X2,X3))
    
    mark#(add(X1,X2)) = [4 2]X1 + [4 4]X2 + [5] >= [0 2]X1 + [1] = mark#(X1)
    
    mark#(add(X1,X2)) = [4 2]X1 + [4 4]X2 + [5] >= [1 0]X1 + [1 0]X2 + [1] = add#(mark(X1),X2)
    
    mark#(add(X1,X2)) = [4 2]X1 + [4 4]X2 + [5] >= [2 2]X1 + [2 2]X2 + [4] = active#(add(mark(X1),X2))
    
    mark#(0()) = 5 >= 2 = active#(0())
    
    mark#(s(X)) = [2 0]X + [1] >= [1 0]X = active#(s(X))
    
    mark#(first(X1,X2)) = [2 4]X1 + [2 4]X2 + [5] >= [0 2]X2 + [1] = mark#(X2)
    
    mark#(first(X1,X2)) = [2 4]X1 + [2 4]X2 + [5] >= [0 2]X1 + [1] = mark#(X1)
    
    mark#(first(X1,X2)) = [2 4]X1 + [2 4]X2 + [5] >= [2 0]X1 + [1 0]X2 + [3] = first#(mark(X1),mark(X2))
    
    mark#(first(X1,X2)) = [2 4]X1 + [2 4]X2 + [5] >= [1 4]X1 + [1 4]X2 + [4] = active#(first(mark(X1),mark(X2)))
    
    mark#(nil()) = 1 >= 0 = active#(nil())
    
    mark#(cons(X1,X2)) = [2 2]X1 + [1] >= [1 1]X1 = active#(cons(X1,X2))
    
    mark#(from(X)) = [4 4]X + [7] >= [2 2]X + [3] = active#(from(X))
    
    and#(mark(X1),X2) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = and#(X1,X2)
    
    and#(X1,mark(X2)) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = and#(X1,X2)
    
    and#(active(X1),X2) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = and#(X1,X2)
    
    and#(X1,active(X2)) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = and#(X1,X2)
    
    if#(mark(X1),X2,X3) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [3] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    if#(X1,mark(X2),X3) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [3] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    if#(X1,X2,mark(X3)) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [5] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    if#(active(X1),X2,X3) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [3] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    if#(X1,active(X2),X3) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [3] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    if#(X1,X2,active(X3)) = [1 0]X1 + [1 0]X2 + [3 0]X3 + [5] >= [1 0]X1 + [1 0]X2 + [3 0]X3 + [2] = if#(X1,X2,X3)
    
    add#(mark(X1),X2) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = add#(X1,X2)
    
    add#(X1,mark(X2)) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = add#(X1,X2)
    
    add#(active(X1),X2) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = add#(X1,X2)
    
    add#(X1,active(X2)) = [1 0]X1 + [1 0]X2 + [1] >= [1 0]X1 + [1 0]X2 = add#(X1,X2)
    
    s#(mark(X)) = [2 0]X + [3] >= [2 0]X + [1] = s#(X)
    
    s#(active(X)) = [2 0]X + [3] >= [2 0]X + [1] = s#(X)
    
    first#(mark(X1),X2) = [2 0]X1 + [1 0]X2 + [2] >= [2 0]X1 + [1 0]X2 = first#(X1,X2)
    
    first#(X1,mark(X2)) = [2 0]X1 + [1 0]X2 + [1] >= [2 0]X1 + [1 0]X2 = first#(X1,X2)
    
    first#(active(X1),X2) = [2 0]X1 + [1 0]X2 + [2] >= [2 0]X1 + [1 0]X2 = first#(X1,X2)
    
    first#(X1,active(X2)) = [2 0]X1 + [1 0]X2 + [1] >= [2 0]X1 + [1 0]X2 = first#(X1,X2)
    
    cons#(mark(X1),X2) = [2 0]X1 + [2 0]X2 + [2] >= [2 0]X1 + [2 0]X2 = cons#(X1,X2)
    
    cons#(X1,mark(X2)) = [2 0]X1 + [2 0]X2 + [2] >= [2 0]X1 + [2 0]X2 = cons#(X1,X2)
    
    cons#(active(X1),X2) = [2 0]X1 + [2 0]X2 + [2] >= [2 0]X1 + [2 0]X2 = cons#(X1,X2)
    
    cons#(X1,active(X2)) = [2 0]X1 + [2 0]X2 + [2] >= [2 0]X1 + [2 0]X2 = cons#(X1,X2)
    
    from#(mark(X)) = [2 0]X + [4] >= [2 0]X + [2] = from#(X)
    
    from#(active(X)) = [2 0]X + [4] >= [2 0]X + [2] = from#(X)
    
                            [1 0]    [4]    [1 0]    [1]          
    active(and(true(),X)) = [2 3]X + [4] >= [0 2]X + [0] = mark(X)
    
                             [1 0]    [4]    [1]                
    active(and(false(),Y)) = [2 3]Y + [2] >= [0] = mark(false())
    
                             [1 2]    [2 0]    [3]    [1 0]    [1]          
    active(if(true(),X,Y)) = [2 3]X + [2 2]Y + [5] >= [0 2]X + [0] = mark(X)
    
                              [1 2]    [2 0]    [3]    [1 0]    [1]          
    active(if(false(),X,Y)) = [2 3]X + [2 2]Y + [3] >= [0 2]Y + [0] = mark(Y)
    
                         [1 0]    [1]    [1 0]    [1]          
    active(add(0(),X)) = [2 2]X + [6] >= [0 2]X + [0] = mark(X)
    
                          [0 0]    [1 0]    [1]    [0 0]    [1]                    
    active(add(s(X),Y)) = [1 0]X + [2 2]Y + [2] >= [2 0]Y + [0] = mark(s(add(X,Y)))
    
                           [0 0]    [1]    [1]              
    active(first(0(),X)) = [1 2]X + [7] >= [0] = mark(nil())
    
                                    [0 0]    [0 0]    [0 0]    [1]    [0 0]    [1]                           
    active(first(s(X),cons(Y,Z))) = [2 0]X + [2 2]Y + [1 0]Z + [2] >= [2 2]Y + [0] = mark(cons(Y,first(X,Z)))
    
                      [0 0]    [2]    [0 0]    [2]                           
    active(from(X)) = [2 2]X + [3] >= [2 2]X + [0] = mark(cons(X,from(s(X))))
    
                       [0 0]     [1 0]     [4]    [0 0]     [1 0]     [4]                           
    mark(and(X1,X2)) = [2 2]X1 + [4 6]X2 + [4] >= [1 2]X1 + [2 3]X2 + [3] = active(and(mark(X1),X2))
    
                   [1]    [1]                 
    mark(true()) = [4] >= [2] = active(true())
    
                    [1]    [1]                  
    mark(false()) = [0] >= [0] = active(false())
    
                         [0 0]     [1 2]     [2 0]     [3]    [0 0]     [1 2]     [2 0]     [3]                             
    mark(if(X1,X2,X3)) = [2 2]X1 + [4 6]X2 + [4 4]X3 + [6] >= [1 2]X1 + [2 3]X2 + [2 2]X3 + [4] = active(if(mark(X1),X2,X3))
    
                       [0 0]     [1 0]     [1]    [0 0]     [1 0]     [1]                           
    mark(add(X1,X2)) = [4 2]X1 + [4 4]X2 + [4] >= [2 2]X1 + [2 2]X2 + [4] = active(add(mark(X1),X2))
    
                [2]    [2]              
    mark(0()) = [4] >= [2] = active(0())
    
                 [0 0]    [1]    [0 0]    [1]               
    mark(s(X)) = [2 0]X + [0] >= [1 0]X + [0] = active(s(X))
    
                         [0 0]     [0 0]     [1]    [0 0]     [0 0]     [1]                                   
    mark(first(X1,X2)) = [2 4]X1 + [2 4]X2 + [4] >= [1 4]X1 + [1 4]X2 + [4] = active(first(mark(X1),mark(X2)))
    
                  [1]    [1]                
    mark(nil()) = [0] >= [0] = active(nil())
    
                        [0 0]     [1 0]     [1]    [0 0]     [1 0]     [1]                      
    mark(cons(X1,X2)) = [2 2]X1 + [0 0]X2 + [0] >= [1 1]X1 + [0 0]X2 + [0] = active(cons(X1,X2))
    
                    [0 0]    [2]    [0 0]    [2]                  
    mark(from(X)) = [4 4]X + [6] >= [2 2]X + [3] = active(from(X))
    
                       [0 0]     [1 0]     [3]    [0 0]     [1 0]     [3]             
    and(mark(X1),X2) = [1 2]X1 + [2 3]X2 + [3] >= [1 1]X1 + [2 3]X2 + [2] = and(X1,X2)
    
                       [0 0]     [1 0]     [4]    [0 0]     [1 0]     [3]             
    and(X1,mark(X2)) = [1 1]X1 + [2 6]X2 + [4] >= [1 1]X1 + [2 3]X2 + [2] = and(X1,X2)
    
                         [0 0]     [1 0]     [3]    [0 0]     [1 0]     [3]             
    and(active(X1),X2) = [1 1]X1 + [2 3]X2 + [3] >= [1 1]X1 + [2 3]X2 + [2] = and(X1,X2)
    
                         [0 0]     [1 0]     [4]    [0 0]     [1 0]     [3]             
    and(X1,active(X2)) = [1 1]X1 + [2 3]X2 + [4] >= [1 1]X1 + [2 3]X2 + [2] = and(X1,X2)
    
                         [0 0]     [1 2]     [2 0]     [2]    [0 0]     [1 2]     [2 0]     [2]               
    if(mark(X1),X2,X3) = [1 2]X1 + [2 3]X2 + [2 2]X3 + [4] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                         [0 0]     [1 4]     [2 0]     [3]    [0 0]     [1 2]     [2 0]     [2]               
    if(X1,mark(X2),X3) = [1 1]X1 + [2 6]X2 + [2 2]X3 + [5] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                         [0 0]     [1 2]     [2 0]     [4]    [0 0]     [1 2]     [2 0]     [2]               
    if(X1,X2,mark(X3)) = [1 1]X1 + [2 3]X2 + [2 4]X3 + [5] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                           [0 0]     [1 2]     [2 0]     [2]    [0 0]     [1 2]     [2 0]     [2]               
    if(active(X1),X2,X3) = [1 1]X1 + [2 3]X2 + [2 2]X3 + [4] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                           [0 0]     [1 2]     [2 0]     [3]    [0 0]     [1 2]     [2 0]     [2]               
    if(X1,active(X2),X3) = [1 1]X1 + [2 3]X2 + [2 2]X3 + [5] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                           [0 0]     [1 2]     [2 0]     [4]    [0 0]     [1 2]     [2 0]     [2]               
    if(X1,X2,active(X3)) = [1 1]X1 + [2 3]X2 + [2 2]X3 + [5] >= [1 1]X1 + [2 3]X2 + [2 2]X3 + [3] = if(X1,X2,X3)
    
                       [0 0]     [1 0]     [0]    [0 0]     [1 0]     [0]             
    add(mark(X1),X2) = [2 2]X1 + [2 2]X2 + [4] >= [2 1]X1 + [2 2]X2 + [2] = add(X1,X2)
    
                       [0 0]     [1 0]     [1]    [0 0]     [1 0]     [0]             
    add(X1,mark(X2)) = [2 1]X1 + [2 4]X2 + [4] >= [2 1]X1 + [2 2]X2 + [2] = add(X1,X2)
    
                         [0 0]     [1 0]     [0]    [0 0]     [1 0]     [0]             
    add(active(X1),X2) = [2 1]X1 + [2 2]X2 + [4] >= [2 1]X1 + [2 2]X2 + [2] = add(X1,X2)
    
                         [0 0]     [1 0]     [1]    [0 0]     [1 0]     [0]             
    add(X1,active(X2)) = [2 1]X1 + [2 2]X2 + [4] >= [2 1]X1 + [2 2]X2 + [2] = add(X1,X2)
    
                 [0 0]    [0]    [0 0]        
    s(mark(X)) = [1 0]X + [1] >= [1 0]X = s(X)
    
                   [0 0]    [0]    [0 0]        
    s(active(X)) = [1 0]X + [1] >= [1 0]X = s(X)
    
                         [0 0]     [0 0]     [0]    [0 0]     [0 0]     [0]               
    first(mark(X1),X2) = [1 4]X1 + [1 2]X2 + [3] >= [1 2]X1 + [1 2]X2 + [2] = first(X1,X2)
    
                         [0 0]     [0 0]     [0]    [0 0]     [0 0]     [0]               
    first(X1,mark(X2)) = [1 2]X1 + [1 4]X2 + [3] >= [1 2]X1 + [1 2]X2 + [2] = first(X1,X2)
    
                           [0 0]     [0 0]     [0]    [0 0]     [0 0]     [0]               
    first(active(X1),X2) = [1 2]X1 + [1 2]X2 + [3] >= [1 2]X1 + [1 2]X2 + [2] = first(X1,X2)
    
                           [0 0]     [0 0]     [0]    [0 0]     [0 0]     [0]               
    first(X1,active(X2)) = [1 2]X1 + [1 2]X2 + [3] >= [1 2]X1 + [1 2]X2 + [2] = first(X1,X2)
    
                        [0 0]     [1 0]     [0]    [0 0]     [1 0]                
    cons(mark(X1),X2) = [1 2]X1 + [0 0]X2 + [1] >= [1 1]X1 + [0 0]X2 = cons(X1,X2)
    
                        [0 0]     [1 0]     [1]    [0 0]     [1 0]                
    cons(X1,mark(X2)) = [1 1]X1 + [0 0]X2 + [0] >= [1 1]X1 + [0 0]X2 = cons(X1,X2)
    
                          [0 0]     [1 0]     [0]    [0 0]     [1 0]                
    cons(active(X1),X2) = [1 1]X1 + [0 0]X2 + [1] >= [1 1]X1 + [0 0]X2 = cons(X1,X2)
    
                          [0 0]     [1 0]     [1]    [0 0]     [1 0]                
    cons(X1,active(X2)) = [1 1]X1 + [0 0]X2 + [0] >= [1 1]X1 + [0 0]X2 = cons(X1,X2)
    
                    [0 0]    [1]    [0 0]    [1]          
    from(mark(X)) = [2 4]X + [5] >= [2 2]X + [3] = from(X)
    
                      [0 0]    [1]    [0 0]    [1]          
    from(active(X)) = [2 2]X + [5] >= [2 2]X + [3] = from(X)
   problem:
    DPs:
     
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
   Qed