MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            check(free(x)) -> free(check(x))
            check(new(x)) -> new(check(x))
            check(old(x)) -> old(x)
            check(old(x)) -> old(check(x))
            new(free(x)) -> free(new(x))
            new(serve()) -> free(serve())
            old(free(x)) -> free(old(x))
            old(serve()) -> free(serve())
            top1(free(x),y) -> top2(x,check(new(y)))
            top1(free(x),y) -> top2(check(x),new(y))
            top1(free(x),y) -> top2(check(new(x)),y)
            top1(free(x),y) -> top2(new(x),check(y))
            top2(x,free(y)) -> top1(x,check(new(y)))
            top2(x,free(y)) -> top1(check(x),new(y))
            top2(x,free(y)) -> top1(check(new(x)),y)
            top2(x,free(y)) -> top1(new(x),check(y))
        - Signature:
            {check/1,new/1,old/1,top1/2,top2/2} / {free/1,serve/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {check,new,old,top1,top2} and constructors {free,serve}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          check#(free(x)) -> c_1(check#(x))
          check#(new(x)) -> c_2(new#(check(x)),check#(x))
          check#(old(x)) -> c_3(old#(x))
          check#(old(x)) -> c_4(old#(check(x)),check#(x))
          new#(free(x)) -> c_5(new#(x))
          new#(serve()) -> c_6()
          old#(free(x)) -> c_7(old#(x))
          old#(serve()) -> c_8()
          top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
          top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
          top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
          top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
          top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
          top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
          top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
          top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            check#(free(x)) -> c_1(check#(x))
            check#(new(x)) -> c_2(new#(check(x)),check#(x))
            check#(old(x)) -> c_3(old#(x))
            check#(old(x)) -> c_4(old#(check(x)),check#(x))
            new#(free(x)) -> c_5(new#(x))
            new#(serve()) -> c_6()
            old#(free(x)) -> c_7(old#(x))
            old#(serve()) -> c_8()
            top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
            top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
            top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
            top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
            top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
            top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
            top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
            top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
        - Weak TRS:
            check(free(x)) -> free(check(x))
            check(new(x)) -> new(check(x))
            check(old(x)) -> old(x)
            check(old(x)) -> old(check(x))
            new(free(x)) -> free(new(x))
            new(serve()) -> free(serve())
            old(free(x)) -> free(old(x))
            old(serve()) -> free(serve())
            top1(free(x),y) -> top2(x,check(new(y)))
            top1(free(x),y) -> top2(check(x),new(y))
            top1(free(x),y) -> top2(check(new(x)),y)
            top1(free(x),y) -> top2(new(x),check(y))
            top2(x,free(y)) -> top1(x,check(new(y)))
            top2(x,free(y)) -> top1(check(x),new(y))
            top2(x,free(y)) -> top1(check(new(x)),y)
            top2(x,free(y)) -> top1(new(x),check(y))
        - Signature:
            {check/1,new/1,old/1,top1/2,top2/2,check#/1,new#/1,old#/1,top1#/2,top2#/2} / {free/1,serve/0,c_1/1,c_2/2
            ,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1,c_8/0,c_9/3,c_10/3,c_11/3,c_12/3,c_13/3,c_14/3,c_15/3,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {check#,new#,old#,top1#,top2#} and constructors {free
            ,serve}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
          check(old(x)) -> old(x)
          check(old(x)) -> old(check(x))
          new(free(x)) -> free(new(x))
          new(serve()) -> free(serve())
          old(free(x)) -> free(old(x))
          old(serve()) -> free(serve())
          check#(free(x)) -> c_1(check#(x))
          check#(new(x)) -> c_2(new#(check(x)),check#(x))
          check#(old(x)) -> c_3(old#(x))
          check#(old(x)) -> c_4(old#(check(x)),check#(x))
          new#(free(x)) -> c_5(new#(x))
          new#(serve()) -> c_6()
          old#(free(x)) -> c_7(old#(x))
          old#(serve()) -> c_8()
          top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
          top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
          top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
          top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
          top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
          top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
          top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
          top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            check#(free(x)) -> c_1(check#(x))
            check#(new(x)) -> c_2(new#(check(x)),check#(x))
            check#(old(x)) -> c_3(old#(x))
            check#(old(x)) -> c_4(old#(check(x)),check#(x))
            new#(free(x)) -> c_5(new#(x))
            new#(serve()) -> c_6()
            old#(free(x)) -> c_7(old#(x))
            old#(serve()) -> c_8()
            top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
            top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
            top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
            top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
            top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
            top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
            top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
            top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
        - Weak TRS:
            check(free(x)) -> free(check(x))
            check(new(x)) -> new(check(x))
            check(old(x)) -> old(x)
            check(old(x)) -> old(check(x))
            new(free(x)) -> free(new(x))
            new(serve()) -> free(serve())
            old(free(x)) -> free(old(x))
            old(serve()) -> free(serve())
        - Signature:
            {check/1,new/1,old/1,top1/2,top2/2,check#/1,new#/1,old#/1,top1#/2,top2#/2} / {free/1,serve/0,c_1/1,c_2/2
            ,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1,c_8/0,c_9/3,c_10/3,c_11/3,c_12/3,c_13/3,c_14/3,c_15/3,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {check#,new#,old#,top1#,top2#} and constructors {free
            ,serve}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {6,8}
        by application of
          Pre({6,8}) = {2,3,4,5,7,9,10,11,12,13,14,15,16}.
        Here rules are labelled as follows:
          1: check#(free(x)) -> c_1(check#(x))
          2: check#(new(x)) -> c_2(new#(check(x)),check#(x))
          3: check#(old(x)) -> c_3(old#(x))
          4: check#(old(x)) -> c_4(old#(check(x)),check#(x))
          5: new#(free(x)) -> c_5(new#(x))
          6: new#(serve()) -> c_6()
          7: old#(free(x)) -> c_7(old#(x))
          8: old#(serve()) -> c_8()
          9: top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
          10: top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
          11: top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
          12: top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
          13: top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
          14: top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
          15: top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
          16: top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            check#(free(x)) -> c_1(check#(x))
            check#(new(x)) -> c_2(new#(check(x)),check#(x))
            check#(old(x)) -> c_3(old#(x))
            check#(old(x)) -> c_4(old#(check(x)),check#(x))
            new#(free(x)) -> c_5(new#(x))
            old#(free(x)) -> c_7(old#(x))
            top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
            top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
            top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
            top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
            top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
            top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
            top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
            top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
        - Weak DPs:
            new#(serve()) -> c_6()
            old#(serve()) -> c_8()
        - Weak TRS:
            check(free(x)) -> free(check(x))
            check(new(x)) -> new(check(x))
            check(old(x)) -> old(x)
            check(old(x)) -> old(check(x))
            new(free(x)) -> free(new(x))
            new(serve()) -> free(serve())
            old(free(x)) -> free(old(x))
            old(serve()) -> free(serve())
        - Signature:
            {check/1,new/1,old/1,top1/2,top2/2,check#/1,new#/1,old#/1,top1#/2,top2#/2} / {free/1,serve/0,c_1/1,c_2/2
            ,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1,c_8/0,c_9/3,c_10/3,c_11/3,c_12/3,c_13/3,c_14/3,c_15/3,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {check#,new#,old#,top1#,top2#} and constructors {free
            ,serve}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:check#(free(x)) -> c_1(check#(x))
             -->_1 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_1 check#(old(x)) -> c_3(old#(x)):3
             -->_1 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_1 check#(free(x)) -> c_1(check#(x)):1
          
          2:S:check#(new(x)) -> c_2(new#(check(x)),check#(x))
             -->_1 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_1 new#(serve()) -> c_6():15
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          3:S:check#(old(x)) -> c_3(old#(x))
             -->_1 old#(free(x)) -> c_7(old#(x)):6
             -->_1 old#(serve()) -> c_8():16
          
          4:S:check#(old(x)) -> c_4(old#(check(x)),check#(x))
             -->_1 old#(free(x)) -> c_7(old#(x)):6
             -->_1 old#(serve()) -> c_8():16
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          5:S:new#(free(x)) -> c_5(new#(x))
             -->_1 new#(serve()) -> c_6():15
             -->_1 new#(free(x)) -> c_5(new#(x)):5
          
          6:S:old#(free(x)) -> c_7(old#(x))
             -->_1 old#(serve()) -> c_8():16
             -->_1 old#(free(x)) -> c_7(old#(x)):6
          
          7:S:top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
             -->_1 top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y)):14
             -->_1 top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x)):13
             -->_1 top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y)):12
             -->_1 top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y)):11
             -->_3 new#(serve()) -> c_6():15
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          8:S:top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
             -->_1 top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y)):14
             -->_1 top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x)):13
             -->_1 top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y)):12
             -->_1 top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y)):11
             -->_3 new#(serve()) -> c_6():15
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          9:S:top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
             -->_1 top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y)):14
             -->_1 top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x)):13
             -->_1 top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y)):12
             -->_1 top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y)):11
             -->_3 new#(serve()) -> c_6():15
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          10:S:top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
             -->_1 top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y)):14
             -->_1 top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x)):13
             -->_1 top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y)):12
             -->_1 top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y)):11
             -->_2 new#(serve()) -> c_6():15
             -->_2 new#(free(x)) -> c_5(new#(x)):5
             -->_3 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_3 check#(old(x)) -> c_3(old#(x)):3
             -->_3 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_3 check#(free(x)) -> c_1(check#(x)):1
          
          11:S:top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
             -->_3 new#(serve()) -> c_6():15
             -->_1 top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y)):10
             -->_1 top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x)):9
             -->_1 top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y)):8
             -->_1 top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y)):7
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          12:S:top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
             -->_3 new#(serve()) -> c_6():15
             -->_1 top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y)):10
             -->_1 top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x)):9
             -->_1 top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y)):8
             -->_1 top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y)):7
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          13:S:top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
             -->_3 new#(serve()) -> c_6():15
             -->_1 top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y)):10
             -->_1 top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x)):9
             -->_1 top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y)):8
             -->_1 top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y)):7
             -->_3 new#(free(x)) -> c_5(new#(x)):5
             -->_2 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_2 check#(old(x)) -> c_3(old#(x)):3
             -->_2 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_2 check#(free(x)) -> c_1(check#(x)):1
          
          14:S:top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
             -->_2 new#(serve()) -> c_6():15
             -->_1 top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y)):10
             -->_1 top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x)):9
             -->_1 top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y)):8
             -->_1 top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y)):7
             -->_2 new#(free(x)) -> c_5(new#(x)):5
             -->_3 check#(old(x)) -> c_4(old#(check(x)),check#(x)):4
             -->_3 check#(old(x)) -> c_3(old#(x)):3
             -->_3 check#(new(x)) -> c_2(new#(check(x)),check#(x)):2
             -->_3 check#(free(x)) -> c_1(check#(x)):1
          
          15:W:new#(serve()) -> c_6()
             
          
          16:W:old#(serve()) -> c_8()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          15: new#(serve()) -> c_6()
          16: old#(serve()) -> c_8()
* Step 5: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          check#(free(x)) -> c_1(check#(x))
          check#(new(x)) -> c_2(new#(check(x)),check#(x))
          check#(old(x)) -> c_3(old#(x))
          check#(old(x)) -> c_4(old#(check(x)),check#(x))
          new#(free(x)) -> c_5(new#(x))
          old#(free(x)) -> c_7(old#(x))
          top1#(free(x),y) -> c_9(top2#(x,check(new(y))),check#(new(y)),new#(y))
          top1#(free(x),y) -> c_10(top2#(check(x),new(y)),check#(x),new#(y))
          top1#(free(x),y) -> c_11(top2#(check(new(x)),y),check#(new(x)),new#(x))
          top1#(free(x),y) -> c_12(top2#(new(x),check(y)),new#(x),check#(y))
          top2#(x,free(y)) -> c_13(top1#(x,check(new(y))),check#(new(y)),new#(y))
          top2#(x,free(y)) -> c_14(top1#(check(x),new(y)),check#(x),new#(y))
          top2#(x,free(y)) -> c_15(top1#(check(new(x)),y),check#(new(x)),new#(x))
          top2#(x,free(y)) -> c_16(top1#(new(x),check(y)),new#(x),check#(y))
      - Weak TRS:
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
          check(old(x)) -> old(x)
          check(old(x)) -> old(check(x))
          new(free(x)) -> free(new(x))
          new(serve()) -> free(serve())
          old(free(x)) -> free(old(x))
          old(serve()) -> free(serve())
      - Signature:
          {check/1,new/1,old/1,top1/2,top2/2,check#/1,new#/1,old#/1,top1#/2,top2#/2} / {free/1,serve/0,c_1/1,c_2/2
          ,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1,c_8/0,c_9/3,c_10/3,c_11/3,c_12/3,c_13/3,c_14/3,c_15/3,c_16/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {check#,new#,old#,top1#,top2#} and constructors {free
          ,serve}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE