MAYBE

Problem:
 empty(nil()) -> true()
 empty(cons(x,y)) -> false()
 tail(nil()) -> nil()
 tail(cons(x,y)) -> y
 head(cons(x,y)) -> x
 zero(0()) -> true()
 zero(s(x)) -> false()
 p(0()) -> 0()
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))
 intlist(x) -> if_intlist(empty(x),x)
 if_intlist(true(),x) -> nil()
 if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
 int(x,y) -> if_int(zero(x),zero(y),x,y)
 if_int(true(),b,x,y) -> if1(b,x,y)
 if_int(false(),b,x,y) -> if2(b,x,y)
 if1(true(),x,y) -> cons(0(),nil())
 if1(false(),x,y) -> cons(0(),int(s(0()),y))
 if2(true(),x,y) -> nil()
 if2(false(),x,y) -> intlist(int(p(x),p(y)))

Proof:
 DP Processor:
  DPs:
   p#(s(s(x))) -> p#(s(x))
   intlist#(x) -> empty#(x)
   intlist#(x) -> if_intlist#(empty(x),x)
   if_intlist#(false(),x) -> tail#(x)
   if_intlist#(false(),x) -> intlist#(tail(x))
   if_intlist#(false(),x) -> head#(x)
   int#(x,y) -> zero#(y)
   int#(x,y) -> zero#(x)
   int#(x,y) -> if_int#(zero(x),zero(y),x,y)
   if_int#(true(),b,x,y) -> if1#(b,x,y)
   if_int#(false(),b,x,y) -> if2#(b,x,y)
   if1#(false(),x,y) -> int#(s(0()),y)
   if2#(false(),x,y) -> p#(y)
   if2#(false(),x,y) -> p#(x)
   if2#(false(),x,y) -> int#(p(x),p(y))
   if2#(false(),x,y) -> intlist#(int(p(x),p(y)))
  TRS:
   empty(nil()) -> true()
   empty(cons(x,y)) -> false()
   tail(nil()) -> nil()
   tail(cons(x,y)) -> y
   head(cons(x,y)) -> x
   zero(0()) -> true()
   zero(s(x)) -> false()
   p(0()) -> 0()
   p(s(0())) -> 0()
   p(s(s(x))) -> s(p(s(x)))
   intlist(x) -> if_intlist(empty(x),x)
   if_intlist(true(),x) -> nil()
   if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
   int(x,y) -> if_int(zero(x),zero(y),x,y)
   if_int(true(),b,x,y) -> if1(b,x,y)
   if_int(false(),b,x,y) -> if2(b,x,y)
   if1(true(),x,y) -> cons(0(),nil())
   if1(false(),x,y) -> cons(0(),int(s(0()),y))
   if2(true(),x,y) -> nil()
   if2(false(),x,y) -> intlist(int(p(x),p(y)))
  CDG Processor:
   DPs:
    p#(s(s(x))) -> p#(s(x))
    intlist#(x) -> empty#(x)
    intlist#(x) -> if_intlist#(empty(x),x)
    if_intlist#(false(),x) -> tail#(x)
    if_intlist#(false(),x) -> intlist#(tail(x))
    if_intlist#(false(),x) -> head#(x)
    int#(x,y) -> zero#(y)
    int#(x,y) -> zero#(x)
    int#(x,y) -> if_int#(zero(x),zero(y),x,y)
    if_int#(true(),b,x,y) -> if1#(b,x,y)
    if_int#(false(),b,x,y) -> if2#(b,x,y)
    if1#(false(),x,y) -> int#(s(0()),y)
    if2#(false(),x,y) -> p#(y)
    if2#(false(),x,y) -> p#(x)
    if2#(false(),x,y) -> int#(p(x),p(y))
    if2#(false(),x,y) -> intlist#(int(p(x),p(y)))
   TRS:
    empty(nil()) -> true()
    empty(cons(x,y)) -> false()
    tail(nil()) -> nil()
    tail(cons(x,y)) -> y
    head(cons(x,y)) -> x
    zero(0()) -> true()
    zero(s(x)) -> false()
    p(0()) -> 0()
    p(s(0())) -> 0()
    p(s(s(x))) -> s(p(s(x)))
    intlist(x) -> if_intlist(empty(x),x)
    if_intlist(true(),x) -> nil()
    if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
    int(x,y) -> if_int(zero(x),zero(y),x,y)
    if_int(true(),b,x,y) -> if1(b,x,y)
    if_int(false(),b,x,y) -> if2(b,x,y)
    if1(true(),x,y) -> cons(0(),nil())
    if1(false(),x,y) -> cons(0(),int(s(0()),y))
    if2(true(),x,y) -> nil()
    if2(false(),x,y) -> intlist(int(p(x),p(y)))
   graph:
    if2#(false(),x,y) -> int#(p(x),p(y)) ->
    int#(x,y) -> zero#(y)
    if2#(false(),x,y) -> int#(p(x),p(y)) ->
    int#(x,y) -> zero#(x)
    if2#(false(),x,y) -> int#(p(x),p(y)) ->
    int#(x,y) -> if_int#(zero(x),zero(y),x,y)
    if2#(false(),x,y) -> intlist#(int(p(x),p(y))) ->
    intlist#(x) -> empty#(x)
    if2#(false(),x,y) -> intlist#(int(p(x),p(y))) ->
    intlist#(x) -> if_intlist#(empty(x),x)
    if2#(false(),x,y) -> p#(y) -> p#(s(s(x))) -> p#(s(x))
    if2#(false(),x,y) -> p#(x) -> p#(s(s(x))) -> p#(s(x))
    if1#(false(),x,y) -> int#(s(0()),y) -> int#(x,y) -> zero#(y)
    if1#(false(),x,y) -> int#(s(0()),y) -> int#(x,y) -> zero#(x)
    if1#(false(),x,y) -> int#(s(0()),y) ->
    int#(x,y) -> if_int#(zero(x),zero(y),x,y)
    if_int#(false(),b,x,y) -> if2#(b,x,y) ->
    if2#(false(),x,y) -> p#(y)
    if_int#(false(),b,x,y) -> if2#(b,x,y) ->
    if2#(false(),x,y) -> p#(x)
    if_int#(false(),b,x,y) -> if2#(b,x,y) ->
    if2#(false(),x,y) -> int#(p(x),p(y))
    if_int#(false(),b,x,y) -> if2#(b,x,y) ->
    if2#(false(),x,y) -> intlist#(int(p(x),p(y)))
    if_int#(true(),b,x,y) -> if1#(b,x,y) ->
    if1#(false(),x,y) -> int#(s(0()),y)
    int#(x,y) -> if_int#(zero(x),zero(y),x,y) ->
    if_int#(true(),b,x,y) -> if1#(b,x,y)
    int#(x,y) -> if_int#(zero(x),zero(y),x,y) ->
    if_int#(false(),b,x,y) -> if2#(b,x,y)
    if_intlist#(false(),x) -> intlist#(tail(x)) ->
    intlist#(x) -> empty#(x)
    if_intlist#(false(),x) -> intlist#(tail(x)) ->
    intlist#(x) -> if_intlist#(empty(x),x)
    intlist#(x) -> if_intlist#(empty(x),x) ->
    if_intlist#(false(),x) -> tail#(x)
    intlist#(x) -> if_intlist#(empty(x),x) ->
    if_intlist#(false(),x) -> intlist#(tail(x))
    intlist#(x) -> if_intlist#(empty(x),x) ->
    if_intlist#(false(),x) -> head#(x)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
   Restore Modifier:
    DPs:
     p#(s(s(x))) -> p#(s(x))
     intlist#(x) -> empty#(x)
     intlist#(x) -> if_intlist#(empty(x),x)
     if_intlist#(false(),x) -> tail#(x)
     if_intlist#(false(),x) -> intlist#(tail(x))
     if_intlist#(false(),x) -> head#(x)
     int#(x,y) -> zero#(y)
     int#(x,y) -> zero#(x)
     int#(x,y) -> if_int#(zero(x),zero(y),x,y)
     if_int#(true(),b,x,y) -> if1#(b,x,y)
     if_int#(false(),b,x,y) -> if2#(b,x,y)
     if1#(false(),x,y) -> int#(s(0()),y)
     if2#(false(),x,y) -> p#(y)
     if2#(false(),x,y) -> p#(x)
     if2#(false(),x,y) -> int#(p(x),p(y))
     if2#(false(),x,y) -> intlist#(int(p(x),p(y)))
    TRS:
     empty(nil()) -> true()
     empty(cons(x,y)) -> false()
     tail(nil()) -> nil()
     tail(cons(x,y)) -> y
     head(cons(x,y)) -> x
     zero(0()) -> true()
     zero(s(x)) -> false()
     p(0()) -> 0()
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
     intlist(x) -> if_intlist(empty(x),x)
     if_intlist(true(),x) -> nil()
     if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
     int(x,y) -> if_int(zero(x),zero(y),x,y)
     if_int(true(),b,x,y) -> if1(b,x,y)
     if_int(false(),b,x,y) -> if2(b,x,y)
     if1(true(),x,y) -> cons(0(),nil())
     if1(false(),x,y) -> cons(0(),int(s(0()),y))
     if2(true(),x,y) -> nil()
     if2(false(),x,y) -> intlist(int(p(x),p(y)))
    SCC Processor:
     #sccs: 3
     #rules: 8
     #arcs: 23/256
     DPs:
      if2#(false(),x,y) -> int#(p(x),p(y))
      int#(x,y) -> if_int#(zero(x),zero(y),x,y)
      if_int#(false(),b,x,y) -> if2#(b,x,y)
      if_int#(true(),b,x,y) -> if1#(b,x,y)
      if1#(false(),x,y) -> int#(s(0()),y)
     TRS:
      empty(nil()) -> true()
      empty(cons(x,y)) -> false()
      tail(nil()) -> nil()
      tail(cons(x,y)) -> y
      head(cons(x,y)) -> x
      zero(0()) -> true()
      zero(s(x)) -> false()
      p(0()) -> 0()
      p(s(0())) -> 0()
      p(s(s(x))) -> s(p(s(x)))
      intlist(x) -> if_intlist(empty(x),x)
      if_intlist(true(),x) -> nil()
      if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
      int(x,y) -> if_int(zero(x),zero(y),x,y)
      if_int(true(),b,x,y) -> if1(b,x,y)
      if_int(false(),b,x,y) -> if2(b,x,y)
      if1(true(),x,y) -> cons(0(),nil())
      if1(false(),x,y) -> cons(0(),int(s(0()),y))
      if2(true(),x,y) -> nil()
      if2(false(),x,y) -> intlist(int(p(x),p(y)))
     Open
     
     DPs:
      p#(s(s(x))) -> p#(s(x))
     TRS:
      empty(nil()) -> true()
      empty(cons(x,y)) -> false()
      tail(nil()) -> nil()
      tail(cons(x,y)) -> y
      head(cons(x,y)) -> x
      zero(0()) -> true()
      zero(s(x)) -> false()
      p(0()) -> 0()
      p(s(0())) -> 0()
      p(s(s(x))) -> s(p(s(x)))
      intlist(x) -> if_intlist(empty(x),x)
      if_intlist(true(),x) -> nil()
      if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
      int(x,y) -> if_int(zero(x),zero(y),x,y)
      if_int(true(),b,x,y) -> if1(b,x,y)
      if_int(false(),b,x,y) -> if2(b,x,y)
      if1(true(),x,y) -> cons(0(),nil())
      if1(false(),x,y) -> cons(0(),int(s(0()),y))
      if2(true(),x,y) -> nil()
      if2(false(),x,y) -> intlist(int(p(x),p(y)))
     Open
     
     DPs:
      intlist#(x) -> if_intlist#(empty(x),x)
      if_intlist#(false(),x) -> intlist#(tail(x))
     TRS:
      empty(nil()) -> true()
      empty(cons(x,y)) -> false()
      tail(nil()) -> nil()
      tail(cons(x,y)) -> y
      head(cons(x,y)) -> x
      zero(0()) -> true()
      zero(s(x)) -> false()
      p(0()) -> 0()
      p(s(0())) -> 0()
      p(s(s(x))) -> s(p(s(x)))
      intlist(x) -> if_intlist(empty(x),x)
      if_intlist(true(),x) -> nil()
      if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
      int(x,y) -> if_int(zero(x),zero(y),x,y)
      if_int(true(),b,x,y) -> if1(b,x,y)
      if_int(false(),b,x,y) -> if2(b,x,y)
      if1(true(),x,y) -> cons(0(),nil())
      if1(false(),x,y) -> cons(0(),int(s(0()),y))
      if2(true(),x,y) -> nil()
      if2(false(),x,y) -> intlist(int(p(x),p(y)))
     Open