MAYBE
TRS:
 {              isEmpty(cons(x, xs)) -> false(),
                      isEmpty(nil()) -> true(),
                         isZero(0()) -> true(),
                        isZero(s(x)) -> false(),
                   head(cons(x, xs)) -> x,
                   tail(cons(x, xs)) -> xs,
                         tail(nil()) -> nil(),
                              p(0()) -> 0(),
                           p(s(0())) -> 0(),
                          p(s(s(x))) -> s(p(s(x))),
                            inc(0()) -> s(0()),
                           inc(s(x)) -> s(inc(x)),
  if(false(), false(), y, xs, ys, x) -> sumList(ys, x),
   if(false(), true(), y, xs, ys, x) -> sumList(xs, y),
         if(true(), b, y, xs, ys, x) -> y,
                      sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                             sum(xs) -> sumList(xs, 0())}
 DP:
  Strict:
   {                        p#(s(s(x))) -> p#(s(x)),
                             inc#(s(x)) -> inc#(x),
    if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x),
     if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y),
                        sumList#(xs, y) -> isEmpty#(xs),
                        sumList#(xs, y) -> isZero#(head(xs)),
                        sumList#(xs, y) -> head#(xs),
                        sumList#(xs, y) -> tail#(xs),
                        sumList#(xs, y) -> p#(head(xs)),
                        sumList#(xs, y) -> inc#(y),
                        sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                               sum#(xs) -> sumList#(xs, 0())}
  Weak:
  {              isEmpty(cons(x, xs)) -> false(),
                       isEmpty(nil()) -> true(),
                          isZero(0()) -> true(),
                         isZero(s(x)) -> false(),
                    head(cons(x, xs)) -> x,
                    tail(cons(x, xs)) -> xs,
                          tail(nil()) -> nil(),
                               p(0()) -> 0(),
                            p(s(0())) -> 0(),
                           p(s(s(x))) -> s(p(s(x))),
                             inc(0()) -> s(0()),
                            inc(s(x)) -> s(inc(x)),
   if(false(), false(), y, xs, ys, x) -> sumList(ys, x),
    if(false(), true(), y, xs, ys, x) -> sumList(xs, y),
          if(true(), b, y, xs, ys, x) -> y,
                       sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                              sum(xs) -> sumList(xs, 0())}
  EDG:
   {(sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y))
    (sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x))
    (sumList#(xs, y) -> inc#(y), inc#(s(x)) -> inc#(x))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> inc#(y))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> p#(head(xs)))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> tail#(xs))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> head#(xs))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> isZero#(head(xs)))
    (sum#(xs) -> sumList#(xs, 0()), sumList#(xs, y) -> isEmpty#(xs))
    (p#(s(s(x))) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (sumList#(xs, y) -> p#(head(xs)), p#(s(s(x))) -> p#(s(x)))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> isEmpty#(xs))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> isZero#(head(xs)))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> head#(xs))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> tail#(xs))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> p#(head(xs)))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> inc#(y))
    (if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x), sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> isEmpty#(xs))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> isZero#(head(xs)))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> head#(xs))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> tail#(xs))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> p#(head(xs)))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> inc#(y))
    (if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y), sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)))
    (inc#(s(x)) -> inc#(x), inc#(s(x)) -> inc#(x))}
   SCCS:
    Scc:
     {if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x),
       if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y),
                          sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))}
    Scc:
     {inc#(s(x)) -> inc#(x)}
    Scc:
     {p#(s(s(x))) -> p#(s(x))}
    SCC:
     Strict:
      {if#(false(), false(), y, xs, ys, x) -> sumList#(ys, x),
        if#(false(), true(), y, xs, ys, x) -> sumList#(xs, y),
                           sumList#(xs, y) -> if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))}
     Weak:
     {              isEmpty(cons(x, xs)) -> false(),
                          isEmpty(nil()) -> true(),
                             isZero(0()) -> true(),
                            isZero(s(x)) -> false(),
                       head(cons(x, xs)) -> x,
                       tail(cons(x, xs)) -> xs,
                             tail(nil()) -> nil(),
                                  p(0()) -> 0(),
                               p(s(0())) -> 0(),
                              p(s(s(x))) -> s(p(s(x))),
                                inc(0()) -> s(0()),
                               inc(s(x)) -> s(inc(x)),
      if(false(), false(), y, xs, ys, x) -> sumList(ys, x),
       if(false(), true(), y, xs, ys, x) -> sumList(xs, y),
             if(true(), b, y, xs, ys, x) -> y,
                          sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                                 sum(xs) -> sumList(xs, 0())}
     Fail
    SCC:
     Strict:
      {inc#(s(x)) -> inc#(x)}
     Weak:
     {              isEmpty(cons(x, xs)) -> false(),
                          isEmpty(nil()) -> true(),
                             isZero(0()) -> true(),
                            isZero(s(x)) -> false(),
                       head(cons(x, xs)) -> x,
                       tail(cons(x, xs)) -> xs,
                             tail(nil()) -> nil(),
                                  p(0()) -> 0(),
                               p(s(0())) -> 0(),
                              p(s(s(x))) -> s(p(s(x))),
                                inc(0()) -> s(0()),
                               inc(s(x)) -> s(inc(x)),
      if(false(), false(), y, xs, ys, x) -> sumList(ys, x),
       if(false(), true(), y, xs, ys, x) -> sumList(xs, y),
             if(true(), b, y, xs, ys, x) -> y,
                          sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                                 sum(xs) -> sumList(xs, 0())}
     SPSC:
      Simple Projection:
       pi(inc#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {p#(s(s(x))) -> p#(s(x))}
     Weak:
     {              isEmpty(cons(x, xs)) -> false(),
                          isEmpty(nil()) -> true(),
                             isZero(0()) -> true(),
                            isZero(s(x)) -> false(),
                       head(cons(x, xs)) -> x,
                       tail(cons(x, xs)) -> xs,
                             tail(nil()) -> nil(),
                                  p(0()) -> 0(),
                               p(s(0())) -> 0(),
                              p(s(s(x))) -> s(p(s(x))),
                                inc(0()) -> s(0()),
                               inc(s(x)) -> s(inc(x)),
      if(false(), false(), y, xs, ys, x) -> sumList(ys, x),
       if(false(), true(), y, xs, ys, x) -> sumList(xs, y),
             if(true(), b, y, xs, ys, x) -> y,
                          sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)),
                                 sum(xs) -> sumList(xs, 0())}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed