MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            empty(cons(x,y)) -> false()
            empty(nil()) -> true()
            head(cons(x,y)) -> x
            if1(false(),x,y) -> cons(0(),int(s(0()),y))
            if1(true(),x,y) -> cons(0(),nil())
            if2(false(),x,y) -> intlist(int(p(x),p(y)))
            if2(true(),x,y) -> nil()
            if_int(false(),b,x,y) -> if2(b,x,y)
            if_int(true(),b,x,y) -> if1(b,x,y)
            if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
            if_intlist(true(),x) -> nil()
            int(x,y) -> if_int(zero(x),zero(y),x,y)
            intlist(x) -> if_intlist(empty(x),x)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(x))) -> s(p(s(x)))
            tail(cons(x,y)) -> y
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(x)) -> false()
        - Signature:
            {empty/1,head/1,if1/3,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1} / {0/0,cons/2,false/0
            ,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {empty,head,if1,if2,if_int,if_intlist,int,intlist,p,tail
            ,zero} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          empty#(cons(x,y)) -> c_1()
          empty#(nil()) -> c_2()
          head#(cons(x,y)) -> c_3()
          if1#(false(),x,y) -> c_4(int#(s(0()),y))
          if1#(true(),x,y) -> c_5()
          if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
          if2#(true(),x,y) -> c_7()
          if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
          if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
          if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
          if_intlist#(true(),x) -> c_11()
          int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
          intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
          p#(0()) -> c_14()
          p#(s(0())) -> c_15()
          p#(s(s(x))) -> c_16(p#(s(x)))
          tail#(cons(x,y)) -> c_17()
          tail#(nil()) -> c_18()
          zero#(0()) -> c_19()
          zero#(s(x)) -> c_20()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            empty#(cons(x,y)) -> c_1()
            empty#(nil()) -> c_2()
            head#(cons(x,y)) -> c_3()
            if1#(false(),x,y) -> c_4(int#(s(0()),y))
            if1#(true(),x,y) -> c_5()
            if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
            if2#(true(),x,y) -> c_7()
            if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
            if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
            if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
            if_intlist#(true(),x) -> c_11()
            int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
            intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
            p#(0()) -> c_14()
            p#(s(0())) -> c_15()
            p#(s(s(x))) -> c_16(p#(s(x)))
            tail#(cons(x,y)) -> c_17()
            tail#(nil()) -> c_18()
            zero#(0()) -> c_19()
            zero#(s(x)) -> c_20()
        - Weak TRS:
            empty(cons(x,y)) -> false()
            empty(nil()) -> true()
            head(cons(x,y)) -> x
            if1(false(),x,y) -> cons(0(),int(s(0()),y))
            if1(true(),x,y) -> cons(0(),nil())
            if2(false(),x,y) -> intlist(int(p(x),p(y)))
            if2(true(),x,y) -> nil()
            if_int(false(),b,x,y) -> if2(b,x,y)
            if_int(true(),b,x,y) -> if1(b,x,y)
            if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
            if_intlist(true(),x) -> nil()
            int(x,y) -> if_int(zero(x),zero(y),x,y)
            intlist(x) -> if_intlist(empty(x),x)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(x))) -> s(p(s(x)))
            tail(cons(x,y)) -> y
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(x)) -> false()
        - Signature:
            {empty/1,head/1,if1/3,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1,empty#/1,head#/1,if1#/3
            ,if2#/3,if_int#/4,if_intlist#/2,int#/2,intlist#/1,p#/1,tail#/1,zero#/1} / {0/0,cons/2,false/0,nil/0,s/1
            ,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/4,c_7/0,c_8/1,c_9/1,c_10/3,c_11/0,c_12/3,c_13/2,c_14/0,c_15/0
            ,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {empty#,head#,if1#,if2#,if_int#,if_intlist#,int#,intlist#
            ,p#,tail#,zero#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,3,5,7,11,14,15,17,18,19,20}
        by application of
          Pre({1,2,3,5,7,11,14,15,17,18,19,20}) = {6,8,9,10,12,13,16}.
        Here rules are labelled as follows:
          1: empty#(cons(x,y)) -> c_1()
          2: empty#(nil()) -> c_2()
          3: head#(cons(x,y)) -> c_3()
          4: if1#(false(),x,y) -> c_4(int#(s(0()),y))
          5: if1#(true(),x,y) -> c_5()
          6: if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
          7: if2#(true(),x,y) -> c_7()
          8: if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
          9: if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
          10: if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
          11: if_intlist#(true(),x) -> c_11()
          12: int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
          13: intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
          14: p#(0()) -> c_14()
          15: p#(s(0())) -> c_15()
          16: p#(s(s(x))) -> c_16(p#(s(x)))
          17: tail#(cons(x,y)) -> c_17()
          18: tail#(nil()) -> c_18()
          19: zero#(0()) -> c_19()
          20: zero#(s(x)) -> c_20()
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            if1#(false(),x,y) -> c_4(int#(s(0()),y))
            if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
            if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
            if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
            if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
            int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
            intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
            p#(s(s(x))) -> c_16(p#(s(x)))
        - Weak DPs:
            empty#(cons(x,y)) -> c_1()
            empty#(nil()) -> c_2()
            head#(cons(x,y)) -> c_3()
            if1#(true(),x,y) -> c_5()
            if2#(true(),x,y) -> c_7()
            if_intlist#(true(),x) -> c_11()
            p#(0()) -> c_14()
            p#(s(0())) -> c_15()
            tail#(cons(x,y)) -> c_17()
            tail#(nil()) -> c_18()
            zero#(0()) -> c_19()
            zero#(s(x)) -> c_20()
        - Weak TRS:
            empty(cons(x,y)) -> false()
            empty(nil()) -> true()
            head(cons(x,y)) -> x
            if1(false(),x,y) -> cons(0(),int(s(0()),y))
            if1(true(),x,y) -> cons(0(),nil())
            if2(false(),x,y) -> intlist(int(p(x),p(y)))
            if2(true(),x,y) -> nil()
            if_int(false(),b,x,y) -> if2(b,x,y)
            if_int(true(),b,x,y) -> if1(b,x,y)
            if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
            if_intlist(true(),x) -> nil()
            int(x,y) -> if_int(zero(x),zero(y),x,y)
            intlist(x) -> if_intlist(empty(x),x)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(x))) -> s(p(s(x)))
            tail(cons(x,y)) -> y
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(x)) -> false()
        - Signature:
            {empty/1,head/1,if1/3,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1,empty#/1,head#/1,if1#/3
            ,if2#/3,if_int#/4,if_intlist#/2,int#/2,intlist#/1,p#/1,tail#/1,zero#/1} / {0/0,cons/2,false/0,nil/0,s/1
            ,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/4,c_7/0,c_8/1,c_9/1,c_10/3,c_11/0,c_12/3,c_13/2,c_14/0,c_15/0
            ,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {empty#,head#,if1#,if2#,if_int#,if_intlist#,int#,intlist#
            ,p#,tail#,zero#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:if1#(false(),x,y) -> c_4(int#(s(0()),y))
             -->_1 int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y)):6
          
          2:S:if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
             -->_4 p#(s(s(x))) -> c_16(p#(s(x))):8
             -->_3 p#(s(s(x))) -> c_16(p#(s(x))):8
             -->_1 intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x)):7
             -->_2 int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y)):6
             -->_4 p#(s(0())) -> c_15():16
             -->_3 p#(s(0())) -> c_15():16
             -->_4 p#(0()) -> c_14():15
             -->_3 p#(0()) -> c_14():15
          
          3:S:if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
             -->_1 if2#(true(),x,y) -> c_7():13
             -->_1 if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y)):2
          
          4:S:if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
             -->_1 if1#(true(),x,y) -> c_5():12
             -->_1 if1#(false(),x,y) -> c_4(int#(s(0()),y)):1
          
          5:S:if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
             -->_2 intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x)):7
             -->_3 tail#(nil()) -> c_18():18
             -->_3 tail#(cons(x,y)) -> c_17():17
             -->_1 head#(cons(x,y)) -> c_3():11
          
          6:S:int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
             -->_3 zero#(s(x)) -> c_20():20
             -->_2 zero#(s(x)) -> c_20():20
             -->_3 zero#(0()) -> c_19():19
             -->_2 zero#(0()) -> c_19():19
             -->_1 if_int#(true(),b,x,y) -> c_9(if1#(b,x,y)):4
             -->_1 if_int#(false(),b,x,y) -> c_8(if2#(b,x,y)):3
          
          7:S:intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
             -->_1 if_intlist#(true(),x) -> c_11():14
             -->_2 empty#(nil()) -> c_2():10
             -->_2 empty#(cons(x,y)) -> c_1():9
             -->_1 if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x)):5
          
          8:S:p#(s(s(x))) -> c_16(p#(s(x)))
             -->_1 p#(s(0())) -> c_15():16
             -->_1 p#(s(s(x))) -> c_16(p#(s(x))):8
          
          9:W:empty#(cons(x,y)) -> c_1()
             
          
          10:W:empty#(nil()) -> c_2()
             
          
          11:W:head#(cons(x,y)) -> c_3()
             
          
          12:W:if1#(true(),x,y) -> c_5()
             
          
          13:W:if2#(true(),x,y) -> c_7()
             
          
          14:W:if_intlist#(true(),x) -> c_11()
             
          
          15:W:p#(0()) -> c_14()
             
          
          16:W:p#(s(0())) -> c_15()
             
          
          17:W:tail#(cons(x,y)) -> c_17()
             
          
          18:W:tail#(nil()) -> c_18()
             
          
          19:W:zero#(0()) -> c_19()
             
          
          20:W:zero#(s(x)) -> c_20()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          15: p#(0()) -> c_14()
          11: head#(cons(x,y)) -> c_3()
          17: tail#(cons(x,y)) -> c_17()
          18: tail#(nil()) -> c_18()
          9: empty#(cons(x,y)) -> c_1()
          10: empty#(nil()) -> c_2()
          14: if_intlist#(true(),x) -> c_11()
          16: p#(s(0())) -> c_15()
          13: if2#(true(),x,y) -> c_7()
          12: if1#(true(),x,y) -> c_5()
          19: zero#(0()) -> c_19()
          20: zero#(s(x)) -> c_20()
* Step 4: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            if1#(false(),x,y) -> c_4(int#(s(0()),y))
            if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
            if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
            if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
            if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
            int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
            intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
            p#(s(s(x))) -> c_16(p#(s(x)))
        - Weak TRS:
            empty(cons(x,y)) -> false()
            empty(nil()) -> true()
            head(cons(x,y)) -> x
            if1(false(),x,y) -> cons(0(),int(s(0()),y))
            if1(true(),x,y) -> cons(0(),nil())
            if2(false(),x,y) -> intlist(int(p(x),p(y)))
            if2(true(),x,y) -> nil()
            if_int(false(),b,x,y) -> if2(b,x,y)
            if_int(true(),b,x,y) -> if1(b,x,y)
            if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
            if_intlist(true(),x) -> nil()
            int(x,y) -> if_int(zero(x),zero(y),x,y)
            intlist(x) -> if_intlist(empty(x),x)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(x))) -> s(p(s(x)))
            tail(cons(x,y)) -> y
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(x)) -> false()
        - Signature:
            {empty/1,head/1,if1/3,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1,empty#/1,head#/1,if1#/3
            ,if2#/3,if_int#/4,if_intlist#/2,int#/2,intlist#/1,p#/1,tail#/1,zero#/1} / {0/0,cons/2,false/0,nil/0,s/1
            ,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/4,c_7/0,c_8/1,c_9/1,c_10/3,c_11/0,c_12/3,c_13/2,c_14/0,c_15/0
            ,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {empty#,head#,if1#,if2#,if_int#,if_intlist#,int#,intlist#
            ,p#,tail#,zero#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:if1#(false(),x,y) -> c_4(int#(s(0()),y))
             -->_1 int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y)):6
          
          2:S:if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
             -->_4 p#(s(s(x))) -> c_16(p#(s(x))):8
             -->_3 p#(s(s(x))) -> c_16(p#(s(x))):8
             -->_1 intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x)):7
             -->_2 int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y)):6
          
          3:S:if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
             -->_1 if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y)):2
          
          4:S:if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
             -->_1 if1#(false(),x,y) -> c_4(int#(s(0()),y)):1
          
          5:S:if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x))
             -->_2 intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x)):7
          
          6:S:int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y),zero#(x),zero#(y))
             -->_1 if_int#(true(),b,x,y) -> c_9(if1#(b,x,y)):4
             -->_1 if_int#(false(),b,x,y) -> c_8(if2#(b,x,y)):3
          
          7:S:intlist#(x) -> c_13(if_intlist#(empty(x),x),empty#(x))
             -->_1 if_intlist#(false(),x) -> c_10(head#(x),intlist#(tail(x)),tail#(x)):5
          
          8:S:p#(s(s(x))) -> c_16(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_16(p#(s(x))):8
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if_intlist#(false(),x) -> c_10(intlist#(tail(x)))
          int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y))
          intlist#(x) -> c_13(if_intlist#(empty(x),x))
* Step 5: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          if1#(false(),x,y) -> c_4(int#(s(0()),y))
          if2#(false(),x,y) -> c_6(intlist#(int(p(x),p(y))),int#(p(x),p(y)),p#(x),p#(y))
          if_int#(false(),b,x,y) -> c_8(if2#(b,x,y))
          if_int#(true(),b,x,y) -> c_9(if1#(b,x,y))
          if_intlist#(false(),x) -> c_10(intlist#(tail(x)))
          int#(x,y) -> c_12(if_int#(zero(x),zero(y),x,y))
          intlist#(x) -> c_13(if_intlist#(empty(x),x))
          p#(s(s(x))) -> c_16(p#(s(x)))
      - Weak TRS:
          empty(cons(x,y)) -> false()
          empty(nil()) -> true()
          head(cons(x,y)) -> x
          if1(false(),x,y) -> cons(0(),int(s(0()),y))
          if1(true(),x,y) -> cons(0(),nil())
          if2(false(),x,y) -> intlist(int(p(x),p(y)))
          if2(true(),x,y) -> nil()
          if_int(false(),b,x,y) -> if2(b,x,y)
          if_int(true(),b,x,y) -> if1(b,x,y)
          if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
          if_intlist(true(),x) -> nil()
          int(x,y) -> if_int(zero(x),zero(y),x,y)
          intlist(x) -> if_intlist(empty(x),x)
          p(0()) -> 0()
          p(s(0())) -> 0()
          p(s(s(x))) -> s(p(s(x)))
          tail(cons(x,y)) -> y
          tail(nil()) -> nil()
          zero(0()) -> true()
          zero(s(x)) -> false()
      - Signature:
          {empty/1,head/1,if1/3,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1,empty#/1,head#/1,if1#/3
          ,if2#/3,if_int#/4,if_intlist#/2,int#/2,intlist#/1,p#/1,tail#/1,zero#/1} / {0/0,cons/2,false/0,nil/0,s/1
          ,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0,c_6/4,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/0
          ,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {empty#,head#,if1#,if2#,if_int#,if_intlist#,int#,intlist#
          ,p#,tail#,zero#} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE