YES
TRS:
 {              mark(true()) -> true(),
               mark(false()) -> false(),
                   mark(0()) -> 0(),
                  mark(s(X)) -> s(X),
           mark(add(X1, X2)) -> a__add(mark(X1), X2),
                 mark(nil()) -> nil(),
          mark(cons(X1, X2)) -> cons(X1, X2),
         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
               mark(from(X)) -> a__from(X),
           mark(and(X1, X2)) -> a__and(mark(X1), X2),
        mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
              a__and(X1, X2) -> and(X1, X2),
           a__and(true(), X) -> mark(X),
          a__and(false(), Y) -> false(),
           a__if(X1, X2, X3) -> if(X1, X2, X3),
         a__if(true(), X, Y) -> mark(X),
        a__if(false(), X, Y) -> mark(Y),
              a__add(X1, X2) -> add(X1, X2),
              a__add(0(), X) -> mark(X),
             a__add(s(X), Y) -> s(add(X, Y)),
            a__first(X1, X2) -> first(X1, X2),
            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))),
                  a__from(X) -> from(X)}
 DP:
  Strict:
   {   mark#(add(X1, X2)) -> mark#(X1),
       mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
     mark#(first(X1, X2)) -> mark#(X1),
     mark#(first(X1, X2)) -> mark#(X2),
     mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
           mark#(from(X)) -> a__from#(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),
       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)}
  Weak:
  {              mark(true()) -> true(),
                mark(false()) -> false(),
                    mark(0()) -> 0(),
                   mark(s(X)) -> s(X),
            mark(add(X1, X2)) -> a__add(mark(X1), X2),
                  mark(nil()) -> nil(),
           mark(cons(X1, X2)) -> cons(X1, X2),
          mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                mark(from(X)) -> a__from(X),
            mark(and(X1, X2)) -> a__and(mark(X1), X2),
         mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
               a__and(X1, X2) -> and(X1, X2),
            a__and(true(), X) -> mark(X),
           a__and(false(), Y) -> false(),
            a__if(X1, X2, X3) -> if(X1, X2, X3),
          a__if(true(), X, Y) -> mark(X),
         a__if(false(), X, Y) -> mark(Y),
               a__add(X1, X2) -> add(X1, X2),
               a__add(0(), X) -> mark(X),
              a__add(s(X), Y) -> s(add(X, Y)),
             a__first(X1, X2) -> first(X1, X2),
             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))),
                   a__from(X) -> from(X)}
  EDG:
   {(a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(from(X)) -> a__from#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), X2), a__add#(0(), X) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(and(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(from(X)) -> a__from#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(true(), X) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> a__from#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(true(), X, Y) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(false(), X, Y) -> mark#(Y))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(from(X)) -> a__from#(X))
    (a__add#(0(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__and#(true(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__and#(true(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
    (a__and#(true(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__and#(true(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__and#(true(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__and#(true(), X) -> mark#(X), mark#(from(X)) -> a__from#(X))
    (a__and#(true(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (a__and#(true(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__and#(true(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__and#(true(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), 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)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))}
   SCCS:
    Scc:
     {   mark#(add(X1, X2)) -> mark#(X1),
         mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
       mark#(first(X1, X2)) -> mark#(X1),
       mark#(first(X1, X2)) -> mark#(X2),
         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),
         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)}
    SCC:
     Strict:
      {   mark#(add(X1, X2)) -> mark#(X1),
          mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
        mark#(first(X1, X2)) -> mark#(X1),
        mark#(first(X1, X2)) -> mark#(X2),
          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),
          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)}
     Weak:
     {              mark(true()) -> true(),
                   mark(false()) -> false(),
                       mark(0()) -> 0(),
                      mark(s(X)) -> s(X),
               mark(add(X1, X2)) -> a__add(mark(X1), X2),
                     mark(nil()) -> nil(),
              mark(cons(X1, X2)) -> cons(X1, X2),
             mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                   mark(from(X)) -> a__from(X),
               mark(and(X1, X2)) -> a__and(mark(X1), X2),
            mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                  a__and(X1, X2) -> and(X1, X2),
               a__and(true(), X) -> mark(X),
              a__and(false(), Y) -> false(),
               a__if(X1, X2, X3) -> if(X1, X2, X3),
             a__if(true(), X, Y) -> mark(X),
            a__if(false(), X, Y) -> mark(Y),
                  a__add(X1, X2) -> add(X1, X2),
                  a__add(0(), X) -> mark(X),
                 a__add(s(X), Y) -> s(add(X, Y)),
                a__first(X1, X2) -> first(X1, X2),
                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))),
                      a__from(X) -> from(X)}
     POLY:
      Argument Filtering:
       pi(if) = [0,1,2], pi(and) = [0,1], pi(a__from) = [], pi(from) = [], pi(first) = [0,1], pi(cons) = [], pi(a__first) = [], pi(nil) = [], pi(add) = [0,1], pi(s) = [], pi(0) = [], pi(a__add#) = 1, pi(a__add) = [], pi(a__if#) = [1,2], pi(a__if) = [], pi(false) = [], pi(true) = [], pi(a__and#) = [1], pi(a__and) = [], pi(mark#) = 0, pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [a__if#](x0, x1) = x0 + x1,
       [a__and#](x0) = x0 + 1,
       [if](x0, x1, x2) = x0 + x1 + x2,
       [and](x0, x1) = x0 + x1 + 1,
       [first](x0, x1) = x0 + x1,
       [add](x0, x1) = x0 + x1
      Strict:
       {   mark#(add(X1, X2)) -> mark#(X1),
           mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
         mark#(first(X1, X2)) -> mark#(X1),
         mark#(first(X1, X2)) -> mark#(X2),
           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),
         a__if#(true(), X, Y) -> mark#(X),
        a__if#(false(), X, Y) -> mark#(Y),
              a__add#(0(), X) -> mark#(X)}
      Weak:
       {              mark(true()) -> true(),
                     mark(false()) -> false(),
                         mark(0()) -> 0(),
                        mark(s(X)) -> s(X),
                 mark(add(X1, X2)) -> a__add(mark(X1), X2),
                       mark(nil()) -> nil(),
                mark(cons(X1, X2)) -> cons(X1, X2),
               mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                     mark(from(X)) -> a__from(X),
                 mark(and(X1, X2)) -> a__and(mark(X1), X2),
              mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                    a__and(X1, X2) -> and(X1, X2),
                 a__and(true(), X) -> mark(X),
                a__and(false(), Y) -> false(),
                 a__if(X1, X2, X3) -> if(X1, X2, X3),
               a__if(true(), X, Y) -> mark(X),
              a__if(false(), X, Y) -> mark(Y),
                    a__add(X1, X2) -> add(X1, X2),
                    a__add(0(), X) -> mark(X),
                   a__add(s(X), Y) -> s(add(X, Y)),
                  a__first(X1, X2) -> first(X1, X2),
                  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))),
                        a__from(X) -> from(X)}
      EDG:
       {(a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> a__add#(mark(X1), X2), a__add#(0(), X) -> mark#(X))
        (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(false(), X, Y) -> mark#(Y))
        (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(true(), X, Y) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), 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)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
        (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
        (a__if#(true(), X, Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (a__if#(true(), X, Y) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (a__if#(true(), X, Y) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
        (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))}
       SCCS:
        Scc:
         {   mark#(add(X1, X2)) -> mark#(X1),
             mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
           mark#(first(X1, X2)) -> mark#(X1),
           mark#(first(X1, X2)) -> mark#(X2),
          mark#(if(X1, X2, X3)) -> mark#(X1),
          mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
           a__if#(true(), X, Y) -> mark#(X),
          a__if#(false(), X, Y) -> mark#(Y),
                a__add#(0(), X) -> mark#(X)}
        SCC:
         Strict:
          {   mark#(add(X1, X2)) -> mark#(X1),
              mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
            mark#(first(X1, X2)) -> mark#(X1),
            mark#(first(X1, X2)) -> mark#(X2),
           mark#(if(X1, X2, X3)) -> mark#(X1),
           mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
            a__if#(true(), X, Y) -> mark#(X),
           a__if#(false(), X, Y) -> mark#(Y),
                 a__add#(0(), X) -> mark#(X)}
         Weak:
         {              mark(true()) -> true(),
                       mark(false()) -> false(),
                           mark(0()) -> 0(),
                          mark(s(X)) -> s(X),
                   mark(add(X1, X2)) -> a__add(mark(X1), X2),
                         mark(nil()) -> nil(),
                  mark(cons(X1, X2)) -> cons(X1, X2),
                 mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                       mark(from(X)) -> a__from(X),
                   mark(and(X1, X2)) -> a__and(mark(X1), X2),
                mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                      a__and(X1, X2) -> and(X1, X2),
                   a__and(true(), X) -> mark(X),
                  a__and(false(), Y) -> false(),
                   a__if(X1, X2, X3) -> if(X1, X2, X3),
                 a__if(true(), X, Y) -> mark(X),
                a__if(false(), X, Y) -> mark(Y),
                      a__add(X1, X2) -> add(X1, X2),
                      a__add(0(), X) -> mark(X),
                     a__add(s(X), Y) -> s(add(X, Y)),
                    a__first(X1, X2) -> first(X1, X2),
                    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))),
                          a__from(X) -> from(X)}
         POLY:
          Argument Filtering:
           pi(if) = [0,1,2], pi(and) = [], pi(a__from) = [], pi(from) = [], pi(first) = [0,1], pi(cons) = [], pi(a__first) = [], pi(nil) = [], pi(add) = [0,1], pi(s) = [], pi(0) = [], pi(a__add#) = [1], pi(a__add) = [], pi(a__if#) = [1,2], pi(a__if) = [], pi(false) = [], pi(true) = [], pi(a__and) = [], pi(mark#) = [0], pi(mark) = []
          Usable Rules:
           {}
          Interpretation:
           [a__if#](x0, x1) = x0 + x1 + 1,
           [a__add#](x0) = x0 + 1,
           [mark#](x0) = x0 + 1,
           [if](x0, x1, x2) = x0 + x1 + x2 + 1,
           [first](x0, x1) = x0 + x1 + 1,
           [add](x0, x1) = x0 + x1
          Strict:
           {   mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
             a__if#(true(), X, Y) -> mark#(X),
            a__if#(false(), X, Y) -> mark#(Y),
                  a__add#(0(), X) -> mark#(X)}
          Weak:
           {              mark(true()) -> true(),
                         mark(false()) -> false(),
                             mark(0()) -> 0(),
                            mark(s(X)) -> s(X),
                     mark(add(X1, X2)) -> a__add(mark(X1), X2),
                           mark(nil()) -> nil(),
                    mark(cons(X1, X2)) -> cons(X1, X2),
                   mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                         mark(from(X)) -> a__from(X),
                     mark(and(X1, X2)) -> a__and(mark(X1), X2),
                  mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                        a__and(X1, X2) -> and(X1, X2),
                     a__and(true(), X) -> mark(X),
                    a__and(false(), Y) -> false(),
                     a__if(X1, X2, X3) -> if(X1, X2, X3),
                   a__if(true(), X, Y) -> mark(X),
                  a__if(false(), X, Y) -> mark(Y),
                        a__add(X1, X2) -> add(X1, X2),
                        a__add(0(), X) -> mark(X),
                       a__add(s(X), Y) -> s(add(X, Y)),
                      a__first(X1, X2) -> first(X1, X2),
                      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))),
                            a__from(X) -> from(X)}
          EDG:
           {(a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
            (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> a__add#(mark(X1), X2), a__add#(0(), X) -> mark#(X))
            (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
            (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))
            (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
            (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))}
           SCCS:
            Scc:
             {mark#(add(X1, X2)) -> mark#(X1),
              mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
                 a__add#(0(), X) -> mark#(X)}
            SCC:
             Strict:
              {mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
                  a__add#(0(), X) -> mark#(X)}
             Weak:
             {              mark(true()) -> true(),
                           mark(false()) -> false(),
                               mark(0()) -> 0(),
                              mark(s(X)) -> s(X),
                       mark(add(X1, X2)) -> a__add(mark(X1), X2),
                             mark(nil()) -> nil(),
                      mark(cons(X1, X2)) -> cons(X1, X2),
                     mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                           mark(from(X)) -> a__from(X),
                       mark(and(X1, X2)) -> a__and(mark(X1), X2),
                    mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                          a__and(X1, X2) -> and(X1, X2),
                       a__and(true(), X) -> mark(X),
                      a__and(false(), Y) -> false(),
                       a__if(X1, X2, X3) -> if(X1, X2, X3),
                     a__if(true(), X, Y) -> mark(X),
                    a__if(false(), X, Y) -> mark(Y),
                          a__add(X1, X2) -> add(X1, X2),
                          a__add(0(), X) -> mark(X),
                         a__add(s(X), Y) -> s(add(X, Y)),
                        a__first(X1, X2) -> first(X1, X2),
                        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))),
                              a__from(X) -> from(X)}
             SPSC:
              Simple Projection:
               pi(a__add#) = 1, pi(mark#) = 0
              Strict:
               {mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
                   a__add#(0(), X) -> mark#(X)}
              EDG:
               {(mark#(add(X1, X2)) -> a__add#(mark(X1), X2), a__add#(0(), X) -> mark#(X))
                (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), X2))}
               SCCS:
                Scc:
                 {mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
                     a__add#(0(), X) -> mark#(X)}
                SCC:
                 Strict:
                  {mark#(add(X1, X2)) -> a__add#(mark(X1), X2),
                      a__add#(0(), X) -> mark#(X)}
                 Weak:
                 {              mark(true()) -> true(),
                               mark(false()) -> false(),
                                   mark(0()) -> 0(),
                                  mark(s(X)) -> s(X),
                           mark(add(X1, X2)) -> a__add(mark(X1), X2),
                                 mark(nil()) -> nil(),
                          mark(cons(X1, X2)) -> cons(X1, X2),
                         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                               mark(from(X)) -> a__from(X),
                           mark(and(X1, X2)) -> a__and(mark(X1), X2),
                        mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
                              a__and(X1, X2) -> and(X1, X2),
                           a__and(true(), X) -> mark(X),
                          a__and(false(), Y) -> false(),
                           a__if(X1, X2, X3) -> if(X1, X2, X3),
                         a__if(true(), X, Y) -> mark(X),
                        a__if(false(), X, Y) -> mark(Y),
                              a__add(X1, X2) -> add(X1, X2),
                              a__add(0(), X) -> mark(X),
                             a__add(s(X), Y) -> s(add(X, Y)),
                            a__first(X1, X2) -> first(X1, X2),
                            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))),
                                  a__from(X) -> from(X)}
                 SPSC:
                  Simple Projection:
                   pi(a__add#) = 1, pi(mark#) = 0
                  Strict:
                   {a__add#(0(), X) -> mark#(X)}
                  EDG:
                   {}
                   SCCS:
                    
                    Qed