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())
  TDG 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())
   graph:
    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) -> isEmpty#(xs)
    sum#(xs) -> sumList#(xs,0()) -> sumList#(xs,y) -> isZero#(head(xs))
    sum#(xs) -> sumList#(xs,0()) -> sumList#(xs,y) -> head#(xs)
    sum#(xs) -> sumList#(xs,0()) -> sumList#(xs,y) -> tail#(xs)
    sum#(xs) -> sumList#(xs,0()) -> sumList#(xs,y) -> p#(head(xs))
    sum#(xs) -> sumList#(xs,0()) ->
    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))
    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(),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(),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)
    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) ->
    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) -> inc#(y) -> inc#(s(x)) -> inc#(x)
    sumList#(xs,y) -> p#(head(xs)) -> p#(s(s(x))) -> p#(s(x))
    inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 27/144
    DPs:
     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)
    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())
    Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    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())
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      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())
     Qed
    
    DPs:
     inc#(s(x)) -> inc#(x)
    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())
    Subterm Criterion Processor:
     simple projection:
      pi(inc#) = 0
     problem:
      DPs:
       
      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())
     Qed