MAYBE

Problem:
 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(s(s(x))) -> s(p(s(x)))
 p(s(0())) -> 0()
 p(0()) -> 0()
 inc(s(x)) -> s(inc(x))
 inc(0()) -> s(0())
 sumList(xs,y) -> if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y))
 if(true(),b,y,xs,ys,x) -> y
 if(false(),true(),y,xs,ys,x) -> sumList(xs,y)
 if(false(),false(),y,xs,ys,x) -> sumList(ys,x)
 sum(xs) -> sumList(xs,0())

Proof:
 DP Processor:
  DPs:
   p#(s(s(x))) -> p#(s(x))
   inc#(s(x)) -> inc#(x)
   sumList#(xs,y) -> inc#(y)
   sumList#(xs,y) -> p#(head(xs))
   sumList#(xs,y) -> tail#(xs)
   sumList#(xs,y) -> head#(xs)
   sumList#(xs,y) -> isZero#(head(xs))
   sumList#(xs,y) -> isEmpty#(xs)
   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)
   if#(false(),false(),y,xs,ys,x) -> sumList#(ys,x)
   sum#(xs) -> sumList#(xs,0())
  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(s(s(x))) -> s(p(s(x)))
   p(s(0())) -> 0()
   p(0()) -> 0()
   inc(s(x)) -> s(inc(x))
   inc(0()) -> s(0())
   sumList(xs,y) -> if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y))
   if(true(),b,y,xs,ys,x) -> y
   if(false(),true(),y,xs,ys,x) -> sumList(xs,y)
   if(false(),false(),y,xs,ys,x) -> sumList(ys,x)
   sum(xs) -> sumList(xs,0())
  Usable Rule Processor:
   DPs:
    p#(s(s(x))) -> p#(s(x))
    inc#(s(x)) -> inc#(x)
    sumList#(xs,y) -> inc#(y)
    sumList#(xs,y) -> p#(head(xs))
    sumList#(xs,y) -> tail#(xs)
    sumList#(xs,y) -> head#(xs)
    sumList#(xs,y) -> isZero#(head(xs))
    sumList#(xs,y) -> isEmpty#(xs)
    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)
    if#(false(),false(),y,xs,ys,x) -> sumList#(ys,x)
    sum#(xs) -> sumList#(xs,0())
   TRS:
    head(cons(x,xs)) -> x
    inc(s(x)) -> s(inc(x))
    inc(0()) -> s(0())
    p(s(s(x))) -> s(p(s(x)))
    p(s(0())) -> 0()
    p(0()) -> 0()
    tail(cons(x,xs)) -> xs
    tail(nil()) -> nil()
    isZero(0()) -> true()
    isZero(s(x)) -> false()
    isEmpty(cons(x,xs)) -> false()
    isEmpty(nil()) -> true()
   Open