MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(x,xs),Nil()) -> Nil()
            gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
            gcd(Nil(),Cons(x,xs)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            goal(x,y) -> gcd(x,y)
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            gcd[False][Ite](False(),x,y) -> gcd(monus(y,x),x)
            gcd[False][Ite](True(),x,y) -> gcd(y,monus(x,y))
            gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y)
            gcd[Ite](True(),x,y) -> x
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3} / {Cons/2
            ,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth
            ,monus,monus[Ite]} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
          @#(Nil(),ys) -> c_2()
          eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
          eqList#(Cons(x,xs),Nil()) -> c_4()
          eqList#(Nil(),Cons(y,ys)) -> c_5()
          eqList#(Nil(),Nil()) -> c_6()
          gcd#(Cons(x,xs),Nil()) -> c_7()
          gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                              ,eqList#(Cons(x',xs'),Cons(x,xs)))
          gcd#(Nil(),Cons(x,xs)) -> c_9()
          gcd#(Nil(),Nil()) -> c_10()
          goal#(x,y) -> c_11(gcd#(x,y))
          gt0#(Cons(x,xs),Nil()) -> c_12()
          gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
          gt0#(Nil(),y) -> c_14()
          lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
          lgth#(Nil()) -> c_16()
          monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                             ,eqList#(lgth(y),Cons(Nil(),Nil()))
                             ,lgth#(y))
        Weak DPs
          and#(False(),False()) -> c_18()
          and#(False(),True()) -> c_19()
          and#(True(),False()) -> c_20()
          and#(True(),True()) -> c_21()
          gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
          gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
          gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
          gcd[Ite]#(True(),x,y) -> c_25()
          monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
          monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            @#(Nil(),ys) -> c_2()
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
            eqList#(Cons(x,xs),Nil()) -> c_4()
            eqList#(Nil(),Cons(y,ys)) -> c_5()
            eqList#(Nil(),Nil()) -> c_6()
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            goal#(x,y) -> c_11(gcd#(x,y))
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            lgth#(Nil()) -> c_16()
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            and#(False(),False()) -> c_18()
            and#(False(),True()) -> c_19()
            and#(True(),False()) -> c_20()
            and#(True(),True()) -> c_21()
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            gcd[Ite]#(True(),x,y) -> c_25()
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
            monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(x,xs),Nil()) -> Nil()
            gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
            gcd(Nil(),Cons(x,xs)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            gcd[False][Ite](False(),x,y) -> gcd(monus(y,x),x)
            gcd[False][Ite](True(),x,y) -> gcd(y,monus(x,y))
            gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y)
            gcd[Ite](True(),x,y) -> x
            goal(x,y) -> gcd(x,y)
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
          @(Nil(),ys) -> ys
          and(False(),False()) -> False()
          and(False(),True()) -> False()
          and(True(),False()) -> False()
          and(True(),True()) -> True()
          eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
          eqList(Cons(x,xs),Nil()) -> False()
          eqList(Nil(),Cons(y,ys)) -> False()
          eqList(Nil(),Nil()) -> True()
          gt0(Cons(x,xs),Nil()) -> True()
          gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
          gt0(Nil(),y) -> False()
          lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
          lgth(Nil()) -> Nil()
          monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
          monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
          monus[Ite](True(),Cons(x,xs),y) -> xs
          @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
          @#(Nil(),ys) -> c_2()
          and#(False(),False()) -> c_18()
          and#(False(),True()) -> c_19()
          and#(True(),False()) -> c_20()
          and#(True(),True()) -> c_21()
          eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
          eqList#(Cons(x,xs),Nil()) -> c_4()
          eqList#(Nil(),Cons(y,ys)) -> c_5()
          eqList#(Nil(),Nil()) -> c_6()
          gcd#(Cons(x,xs),Nil()) -> c_7()
          gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                              ,eqList#(Cons(x',xs'),Cons(x,xs)))
          gcd#(Nil(),Cons(x,xs)) -> c_9()
          gcd#(Nil(),Nil()) -> c_10()
          gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
          gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
          gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
          gcd[Ite]#(True(),x,y) -> c_25()
          goal#(x,y) -> c_11(gcd#(x,y))
          gt0#(Cons(x,xs),Nil()) -> c_12()
          gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
          gt0#(Nil(),y) -> c_14()
          lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
          lgth#(Nil()) -> c_16()
          monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                             ,eqList#(lgth(y),Cons(Nil(),Nil()))
                             ,lgth#(y))
          monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
          monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            @#(Nil(),ys) -> c_2()
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
            eqList#(Cons(x,xs),Nil()) -> c_4()
            eqList#(Nil(),Cons(y,ys)) -> c_5()
            eqList#(Nil(),Nil()) -> c_6()
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            goal#(x,y) -> c_11(gcd#(x,y))
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            lgth#(Nil()) -> c_16()
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            and#(False(),False()) -> c_18()
            and#(False(),True()) -> c_19()
            and#(True(),False()) -> c_20()
            and#(True(),True()) -> c_21()
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            gcd[Ite]#(True(),x,y) -> c_25()
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
            monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,5,6,16}
        by application of
          Pre({2,4,5,6,16}) = {1,3,15,17}.
        Here rules are labelled as follows:
          1: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
          2: @#(Nil(),ys) -> c_2()
          3: eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
          4: eqList#(Cons(x,xs),Nil()) -> c_4()
          5: eqList#(Nil(),Cons(y,ys)) -> c_5()
          6: eqList#(Nil(),Nil()) -> c_6()
          7: gcd#(Cons(x,xs),Nil()) -> c_7()
          8: gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                 ,eqList#(Cons(x',xs'),Cons(x,xs)))
          9: gcd#(Nil(),Cons(x,xs)) -> c_9()
          10: gcd#(Nil(),Nil()) -> c_10()
          11: goal#(x,y) -> c_11(gcd#(x,y))
          12: gt0#(Cons(x,xs),Nil()) -> c_12()
          13: gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
          14: gt0#(Nil(),y) -> c_14()
          15: lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
          16: lgth#(Nil()) -> c_16()
          17: monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                 ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                 ,lgth#(y))
          18: and#(False(),False()) -> c_18()
          19: and#(False(),True()) -> c_19()
          20: and#(True(),False()) -> c_20()
          21: and#(True(),True()) -> c_21()
          22: gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
          23: gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
          24: gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
          25: gcd[Ite]#(True(),x,y) -> c_25()
          26: monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
          27: monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            goal#(x,y) -> c_11(gcd#(x,y))
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            @#(Nil(),ys) -> c_2()
            and#(False(),False()) -> c_18()
            and#(False(),True()) -> c_19()
            and#(True(),False()) -> c_20()
            and#(True(),True()) -> c_21()
            eqList#(Cons(x,xs),Nil()) -> c_4()
            eqList#(Nil(),Cons(y,ys)) -> c_5()
            eqList#(Nil(),Nil()) -> c_6()
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            gcd[Ite]#(True(),x,y) -> c_25()
            lgth#(Nil()) -> c_16()
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
            monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
             -->_1 @#(Nil(),ys) -> c_2():13
             -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
          
          2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
             -->_3 eqList#(Nil(),Nil()) -> c_6():20
             -->_2 eqList#(Nil(),Nil()) -> c_6():20
             -->_3 eqList#(Nil(),Cons(y,ys)) -> c_5():19
             -->_2 eqList#(Nil(),Cons(y,ys)) -> c_5():19
             -->_3 eqList#(Cons(x,xs),Nil()) -> c_4():18
             -->_2 eqList#(Cons(x,xs),Nil()) -> c_4():18
             -->_1 and#(True(),True()) -> c_21():17
             -->_1 and#(True(),False()) -> c_20():16
             -->_1 and#(False(),True()) -> c_19():15
             -->_1 and#(False(),False()) -> c_18():14
             -->_3 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          3:S:gcd#(Cons(x,xs),Nil()) -> c_7()
             
          
          4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                  ,eqList#(Cons(x',xs'),Cons(x,xs)))
             -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):23
             -->_1 gcd[Ite]#(True(),x,y) -> c_25():24
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          5:S:gcd#(Nil(),Cons(x,xs)) -> c_9()
             
          
          6:S:gcd#(Nil(),Nil()) -> c_10()
             
          
          7:S:goal#(x,y) -> c_11(gcd#(x,y))
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          8:S:gt0#(Cons(x,xs),Nil()) -> c_12()
             
          
          9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
             -->_1 gt0#(Nil(),y) -> c_14():10
             -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
             -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8
          
          10:S:gt0#(Nil(),y) -> c_14()
             
          
          11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
             -->_2 lgth#(Nil()) -> c_16():25
             -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
             -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
          
          12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                  ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                  ,lgth#(y))
             -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):26
             -->_1 monus[Ite]#(True(),Cons(x,xs),y) -> c_27():27
             -->_3 lgth#(Nil()) -> c_16():25
             -->_2 eqList#(Nil(),Cons(y,ys)) -> c_5():19
             -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          13:W:@#(Nil(),ys) -> c_2()
             
          
          14:W:and#(False(),False()) -> c_18()
             
          
          15:W:and#(False(),True()) -> c_19()
             
          
          16:W:and#(True(),False()) -> c_20()
             
          
          17:W:and#(True(),True()) -> c_21()
             
          
          18:W:eqList#(Cons(x,xs),Nil()) -> c_4()
             
          
          19:W:eqList#(Nil(),Cons(y,ys)) -> c_5()
             
          
          20:W:eqList#(Nil(),Nil()) -> c_6()
             
          
          21:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
             -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          22:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
             -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          23:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
             -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):22
             -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):21
             -->_2 gt0#(Nil(),y) -> c_14():10
             -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
             -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8
          
          24:W:gcd[Ite]#(True(),x,y) -> c_25()
             
          
          25:W:lgth#(Nil()) -> c_16()
             
          
          26:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
             -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
          
          27:W:monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          24: gcd[Ite]#(True(),x,y) -> c_25()
          25: lgth#(Nil()) -> c_16()
          27: monus[Ite]#(True(),Cons(x,xs),y) -> c_27()
          14: and#(False(),False()) -> c_18()
          15: and#(False(),True()) -> c_19()
          16: and#(True(),False()) -> c_20()
          17: and#(True(),True()) -> c_21()
          18: eqList#(Cons(x,xs),Nil()) -> c_4()
          19: eqList#(Nil(),Cons(y,ys)) -> c_5()
          20: eqList#(Nil(),Nil()) -> c_6()
          13: @#(Nil(),ys) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            goal#(x,y) -> c_11(gcd#(x,y))
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
             -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
          
          2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys))
             -->_3 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys))
                                                        ,eqList#(x,y)
                                                        ,eqList#(xs,ys)):2
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          3:S:gcd#(Cons(x,xs),Nil()) -> c_7()
             
          
          4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                  ,eqList#(Cons(x',xs'),Cons(x,xs)))
             -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):23
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          5:S:gcd#(Nil(),Cons(x,xs)) -> c_9()
             
          
          6:S:gcd#(Nil(),Nil()) -> c_10()
             
          
          7:S:goal#(x,y) -> c_11(gcd#(x,y))
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          8:S:gt0#(Cons(x,xs),Nil()) -> c_12()
             
          
          9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
             -->_1 gt0#(Nil(),y) -> c_14():10
             -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
             -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8
          
          10:S:gt0#(Nil(),y) -> c_14()
             
          
          11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
             -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
             -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
          
          12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                  ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                  ,lgth#(y))
             -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):26
             -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
             -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2
          
          21:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
             -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          22:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
             -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
             -->_1 gcd#(Nil(),Nil()) -> c_10():6
             -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
             -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                                 ,Cons(x',xs')
                                                                 ,Cons(x,xs))
                                                       ,eqList#(Cons(x',xs'),Cons(x,xs))):4
             -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
          
          23:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
             -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):22
             -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):21
             -->_2 gt0#(Nil(),y) -> c_14():10
             -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
             -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8
          
          26:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
             -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                      ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                      ,lgth#(y)):12
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            goal#(x,y) -> c_11(gcd#(x,y))
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
           -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
        
        2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
           -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2
           -->_1 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2
        
        3:S:gcd#(Cons(x,xs),Nil()) -> c_7()
           
        
        4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
           -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):15
           -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2
        
        5:S:gcd#(Nil(),Cons(x,xs)) -> c_9()
           
        
        6:S:gcd#(Nil(),Nil()) -> c_10()
           
        
        7:S:goal#(x,y) -> c_11(gcd#(x,y))
           -->_1 gcd#(Nil(),Nil()) -> c_10():6
           -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
           -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                               ,Cons(x',xs')
                                                               ,Cons(x,xs))
                                                     ,eqList#(Cons(x',xs'),Cons(x,xs))):4
           -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
        
        8:S:gt0#(Cons(x,xs),Nil()) -> c_12()
           
        
        9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
           -->_1 gt0#(Nil(),y) -> c_14():10
           -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
           -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8
        
        10:S:gt0#(Nil(),y) -> c_14()
           
        
        11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
           -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
           -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1
        
        12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                ,lgth#(y))
           -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):16
           -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11
           -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2
        
        13:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
           -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                    ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                    ,lgth#(y)):12
           -->_1 gcd#(Nil(),Nil()) -> c_10():6
           -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
           -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                               ,Cons(x',xs')
                                                               ,Cons(x,xs))
                                                     ,eqList#(Cons(x',xs'),Cons(x,xs))):4
           -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
        
        14:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
           -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                    ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                    ,lgth#(y)):12
           -->_1 gcd#(Nil(),Nil()) -> c_10():6
           -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5
           -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs))
                                                               ,Cons(x',xs')
                                                               ,Cons(x,xs))
                                                     ,eqList#(Cons(x',xs'),Cons(x,xs))):4
           -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3
        
        15:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
           -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):14
           -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):13
           -->_2 gt0#(Nil(),y) -> c_14():10
           -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9
           -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8
        
        16:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
           -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                                    ,eqList#(lgth(y),Cons(Nil(),Nil()))
                                    ,lgth#(y)):12
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(7,goal#(x,y) -> c_11(gcd#(x,y)))]
* Step 7: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1,2},
          uargs(c_8) = {1,2},
          uargs(c_13) = {1},
          uargs(c_15) = {1,2},
          uargs(c_17) = {1,2,3},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_24) = {1,2},
          uargs(c_26) = {1}
        
        Following symbols are considered usable:
          {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#}
        TcT has computed the following interpretation:
                         p(@) = [2] x1 + [3]                  
                      p(Cons) = [0]                           
                     p(False) = [0]                           
                       p(Nil) = [1]                           
                      p(True) = [0]                           
                       p(and) = [3] x1 + [0]                  
                    p(eqList) = [4] x2 + [5]                  
                       p(gcd) = [1] x1 + [0]                  
           p(gcd[False][Ite]) = [0]                           
                  p(gcd[Ite]) = [4]                           
                      p(goal) = [4]                           
                       p(gt0) = [0]                           
                      p(lgth) = [1] x1 + [0]                  
                     p(monus) = [0]                           
                p(monus[Ite]) = [4]                           
                        p(@#) = [0]                           
                      p(and#) = [0]                           
                   p(eqList#) = [0]                           
                      p(gcd#) = [1]                           
          p(gcd[False][Ite]#) = [2] x2 + [6] x3 + [1]         
                 p(gcd[Ite]#) = [4] x2 + [6] x3 + [1]         
                     p(goal#) = [1] x1 + [1]                  
                      p(gt0#) = [0]                           
                     p(lgth#) = [0]                           
                    p(monus#) = [0]                           
               p(monus[Ite]#) = [0]                           
                       p(c_1) = [2] x1 + [0]                  
                       p(c_2) = [1]                           
                       p(c_3) = [1] x1 + [4] x2 + [0]         
                       p(c_4) = [1]                           
                       p(c_5) = [0]                           
                       p(c_6) = [0]                           
                       p(c_7) = [0]                           
                       p(c_8) = [1] x1 + [1] x2 + [0]         
                       p(c_9) = [1]                           
                      p(c_10) = [1]                           
                      p(c_11) = [1]                           
                      p(c_12) = [0]                           
                      p(c_13) = [1] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [4] x1 + [1] x2 + [0]         
                      p(c_16) = [0]                           
                      p(c_17) = [4] x1 + [4] x2 + [1] x3 + [0]
                      p(c_18) = [4]                           
                      p(c_19) = [0]                           
                      p(c_20) = [0]                           
                      p(c_21) = [0]                           
                      p(c_22) = [1] x1 + [4] x2 + [0]         
                      p(c_23) = [1] x1 + [4] x2 + [0]         
                      p(c_24) = [1] x1 + [1] x2 + [0]         
                      p(c_25) = [0]                           
                      p(c_26) = [1] x1 + [0]                  
                      p(c_27) = [1]                           
        
        Following rules are strictly oriented:
        gcd#(Cons(x,xs),Nil()) = [1]  
                               > [0]  
                               = c_7()
        
        
        Following rules are (at-least) weakly oriented:
                                   @#(Cons(x,xs),ys) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_1(@#(xs,ys))                                                                                          
        
                      eqList#(Cons(x,xs),Cons(y,ys)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_3(eqList#(x,y),eqList#(xs,ys))                                                                        
        
                       gcd#(Cons(x',xs'),Cons(x,xs)) =  [1]                                                                                                     
                                                     >= [1]                                                                                                     
                                                     =  c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs)))
        
                              gcd#(Nil(),Cons(x,xs)) =  [1]                                                                                                     
                                                     >= [1]                                                                                                     
                                                     =  c_9()                                                                                                   
        
                                   gcd#(Nil(),Nil()) =  [1]                                                                                                     
                                                     >= [1]                                                                                                     
                                                     =  c_10()                                                                                                  
        
                       gcd[False][Ite]#(False(),x,y) =  [2] x + [6] y + [1]                                                                                     
                                                     >= [1]                                                                                                     
                                                     =  c_22(gcd#(monus(y,x),x),monus#(y,x))                                                                    
        
                        gcd[False][Ite]#(True(),x,y) =  [2] x + [6] y + [1]                                                                                     
                                                     >= [1]                                                                                                     
                                                     =  c_23(gcd#(y,monus(x,y)),monus#(x,y))                                                                    
        
                              gcd[Ite]#(False(),x,y) =  [4] x + [6] y + [1]                                                                                     
                                                     >= [2] x + [6] y + [1]                                                                                     
                                                     =  c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))                                                          
        
                              gt0#(Cons(x,xs),Nil()) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_12()                                                                                                  
        
                       gt0#(Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_13(gt0#(xs',xs))                                                                                      
        
                                       gt0#(Nil(),y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_14()                                                                                                  
        
                                   lgth#(Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))                                                          
        
                                         monus#(x,y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y))    
        
        monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_26(monus#(xs',xs))                                                                                    
        
* Step 8: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gcd#(Nil(),Nil()) -> c_10()
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1,2},
          uargs(c_8) = {1,2},
          uargs(c_13) = {1},
          uargs(c_15) = {1,2},
          uargs(c_17) = {1,2,3},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_24) = {1,2},
          uargs(c_26) = {1}
        
        Following symbols are considered usable:
          {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#}
        TcT has computed the following interpretation:
                         p(@) = [4]                           
                      p(Cons) = [0]                           
                     p(False) = [0]                           
                       p(Nil) = [0]                           
                      p(True) = [0]                           
                       p(and) = [4] x1 + [0]                  
                    p(eqList) = [1] x2 + [2]                  
                       p(gcd) = [1] x2 + [2]                  
           p(gcd[False][Ite]) = [1] x2 + [4] x3 + [1]         
                  p(gcd[Ite]) = [4] x1 + [2] x2 + [0]         
                      p(goal) = [4] x1 + [1]                  
                       p(gt0) = [0]                           
                      p(lgth) = [2] x1 + [7]                  
                     p(monus) = [2] x1 + [1] x2 + [4]         
                p(monus[Ite]) = [3] x1 + [1]                  
                        p(@#) = [0]                           
                      p(and#) = [1] x1 + [1]                  
                   p(eqList#) = [0]                           
                      p(gcd#) = [2]                           
          p(gcd[False][Ite]#) = [1] x3 + [2]                  
                 p(gcd[Ite]#) = [1] x2 + [2] x3 + [2]         
                     p(goal#) = [4] x1 + [2] x2 + [0]         
                      p(gt0#) = [0]                           
                     p(lgth#) = [0]                           
                    p(monus#) = [0]                           
               p(monus[Ite]#) = [0]                           
                       p(c_1) = [1] x1 + [0]                  
                       p(c_2) = [0]                           
                       p(c_3) = [2] x1 + [1] x2 + [0]         
                       p(c_4) = [4]                           
                       p(c_5) = [0]                           
                       p(c_6) = [0]                           
                       p(c_7) = [2]                           
                       p(c_8) = [1] x1 + [4] x2 + [0]         
                       p(c_9) = [2]                           
                      p(c_10) = [1]                           
                      p(c_11) = [4] x1 + [0]                  
                      p(c_12) = [0]                           
                      p(c_13) = [4] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [4] x1 + [4] x2 + [0]         
                      p(c_16) = [2]                           
                      p(c_17) = [4] x1 + [4] x2 + [4] x3 + [0]
                      p(c_18) = [1]                           
                      p(c_19) = [2]                           
                      p(c_20) = [1]                           
                      p(c_21) = [0]                           
                      p(c_22) = [1] x1 + [4] x2 + [0]         
                      p(c_23) = [1] x1 + [1] x2 + [0]         
                      p(c_24) = [1] x1 + [4] x2 + [0]         
                      p(c_25) = [2]                           
                      p(c_26) = [1] x1 + [0]                  
                      p(c_27) = [2]                           
        
        Following rules are strictly oriented:
        gcd#(Nil(),Nil()) = [2]   
                          > [1]   
                          = c_10()
        
        
        Following rules are (at-least) weakly oriented:
                                   @#(Cons(x,xs),ys) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_1(@#(xs,ys))                                                                                          
        
                      eqList#(Cons(x,xs),Cons(y,ys)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_3(eqList#(x,y),eqList#(xs,ys))                                                                        
        
                              gcd#(Cons(x,xs),Nil()) =  [2]                                                                                                     
                                                     >= [2]                                                                                                     
                                                     =  c_7()                                                                                                   
        
                       gcd#(Cons(x',xs'),Cons(x,xs)) =  [2]                                                                                                     
                                                     >= [2]                                                                                                     
                                                     =  c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs)))
        
                              gcd#(Nil(),Cons(x,xs)) =  [2]                                                                                                     
                                                     >= [2]                                                                                                     
                                                     =  c_9()                                                                                                   
        
                       gcd[False][Ite]#(False(),x,y) =  [1] y + [2]                                                                                             
                                                     >= [2]                                                                                                     
                                                     =  c_22(gcd#(monus(y,x),x),monus#(y,x))                                                                    
        
                        gcd[False][Ite]#(True(),x,y) =  [1] y + [2]                                                                                             
                                                     >= [2]                                                                                                     
                                                     =  c_23(gcd#(y,monus(x,y)),monus#(x,y))                                                                    
        
                              gcd[Ite]#(False(),x,y) =  [1] x + [2] y + [2]                                                                                     
                                                     >= [1] y + [2]                                                                                             
                                                     =  c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))                                                          
        
                              gt0#(Cons(x,xs),Nil()) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_12()                                                                                                  
        
                       gt0#(Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_13(gt0#(xs',xs))                                                                                      
        
                                       gt0#(Nil(),y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_14()                                                                                                  
        
                                   lgth#(Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))                                                          
        
                                         monus#(x,y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y))    
        
        monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_26(monus#(xs',xs))                                                                                    
        
* Step 9: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
            eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
            gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                                ,eqList#(Cons(x',xs'),Cons(x,xs)))
            gcd#(Nil(),Cons(x,xs)) -> c_9()
            gt0#(Cons(x,xs),Nil()) -> c_12()
            gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
            gt0#(Nil(),y) -> c_14()
            lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
            monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                               ,eqList#(lgth(y),Cons(Nil(),Nil()))
                               ,lgth#(y))
        - Weak DPs:
            gcd#(Cons(x,xs),Nil()) -> c_7()
            gcd#(Nil(),Nil()) -> c_10()
            gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
            gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
            gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
            monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
        - Weak TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
            ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
            ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
            ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
            ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1,2},
          uargs(c_8) = {1,2},
          uargs(c_13) = {1},
          uargs(c_15) = {1,2},
          uargs(c_17) = {1,2,3},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_24) = {1,2},
          uargs(c_26) = {1}
        
        Following symbols are considered usable:
          {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#}
        TcT has computed the following interpretation:
                         p(@) = [4] x2 + [0]                  
                      p(Cons) = [0]                           
                     p(False) = [0]                           
                       p(Nil) = [0]                           
                      p(True) = [0]                           
                       p(and) = [5] x1 + [2] x2 + [6]         
                    p(eqList) = [3] x2 + [1]                  
                       p(gcd) = [0]                           
           p(gcd[False][Ite]) = [2] x2 + [1]                  
                  p(gcd[Ite]) = [0]                           
                      p(goal) = [0]                           
                       p(gt0) = [0]                           
                      p(lgth) = [1] x1 + [0]                  
                     p(monus) = [0]                           
                p(monus[Ite]) = [1] x3 + [5]                  
                        p(@#) = [0]                           
                      p(and#) = [0]                           
                   p(eqList#) = [0]                           
                      p(gcd#) = [4]                           
          p(gcd[False][Ite]#) = [4]                           
                 p(gcd[Ite]#) = [4]                           
                     p(goal#) = [2] x2 + [1]                  
                      p(gt0#) = [0]                           
                     p(lgth#) = [0]                           
                    p(monus#) = [0]                           
               p(monus[Ite]#) = [0]                           
                       p(c_1) = [4] x1 + [0]                  
                       p(c_2) = [0]                           
                       p(c_3) = [1] x1 + [4] x2 + [0]         
                       p(c_4) = [0]                           
                       p(c_5) = [1]                           
                       p(c_6) = [2]                           
                       p(c_7) = [4]                           
                       p(c_8) = [1] x1 + [2] x2 + [0]         
                       p(c_9) = [3]                           
                      p(c_10) = [0]                           
                      p(c_11) = [1]                           
                      p(c_12) = [0]                           
                      p(c_13) = [4] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [2] x1 + [1] x2 + [0]         
                      p(c_16) = [1]                           
                      p(c_17) = [4] x1 + [4] x2 + [4] x3 + [0]
                      p(c_18) = [2]                           
                      p(c_19) = [1]                           
                      p(c_20) = [1]                           
                      p(c_21) = [0]                           
                      p(c_22) = [1] x1 + [2] x2 + [0]         
                      p(c_23) = [1] x1 + [2] x2 + [0]         
                      p(c_24) = [1] x1 + [4] x2 + [0]         
                      p(c_25) = [1]                           
                      p(c_26) = [1] x1 + [0]                  
                      p(c_27) = [1]                           
        
        Following rules are strictly oriented:
        gcd#(Nil(),Cons(x,xs)) = [4]  
                               > [3]  
                               = c_9()
        
        
        Following rules are (at-least) weakly oriented:
                                   @#(Cons(x,xs),ys) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_1(@#(xs,ys))                                                                                          
        
                      eqList#(Cons(x,xs),Cons(y,ys)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_3(eqList#(x,y),eqList#(xs,ys))                                                                        
        
                              gcd#(Cons(x,xs),Nil()) =  [4]                                                                                                     
                                                     >= [4]                                                                                                     
                                                     =  c_7()                                                                                                   
        
                       gcd#(Cons(x',xs'),Cons(x,xs)) =  [4]                                                                                                     
                                                     >= [4]                                                                                                     
                                                     =  c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs)))
        
                                   gcd#(Nil(),Nil()) =  [4]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_10()                                                                                                  
        
                       gcd[False][Ite]#(False(),x,y) =  [4]                                                                                                     
                                                     >= [4]                                                                                                     
                                                     =  c_22(gcd#(monus(y,x),x),monus#(y,x))                                                                    
        
                        gcd[False][Ite]#(True(),x,y) =  [4]                                                                                                     
                                                     >= [4]                                                                                                     
                                                     =  c_23(gcd#(y,monus(x,y)),monus#(x,y))                                                                    
        
                              gcd[Ite]#(False(),x,y) =  [4]                                                                                                     
                                                     >= [4]                                                                                                     
                                                     =  c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))                                                          
        
                              gt0#(Cons(x,xs),Nil()) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_12()                                                                                                  
        
                       gt0#(Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_13(gt0#(xs',xs))                                                                                      
        
                                       gt0#(Nil(),y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_14()                                                                                                  
        
                                   lgth#(Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))                                                          
        
                                         monus#(x,y) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y))    
        
        monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) =  [0]                                                                                                     
                                                     >= [0]                                                                                                     
                                                     =  c_26(monus#(xs',xs))                                                                                    
        
* Step 10: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          @#(Cons(x,xs),ys) -> c_1(@#(xs,ys))
          eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys))
          gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
                                              ,eqList#(Cons(x',xs'),Cons(x,xs)))
          gt0#(Cons(x,xs),Nil()) -> c_12()
          gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs))
          gt0#(Nil(),y) -> c_14()
          lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs))
          monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y)
                             ,eqList#(lgth(y),Cons(Nil(),Nil()))
                             ,lgth#(y))
      - Weak DPs:
          gcd#(Cons(x,xs),Nil()) -> c_7()
          gcd#(Nil(),Cons(x,xs)) -> c_9()
          gcd#(Nil(),Nil()) -> c_10()
          gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x))
          gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y))
          gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y))
          monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs))
      - Weak TRS:
          @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
          @(Nil(),ys) -> ys
          and(False(),False()) -> False()
          and(False(),True()) -> False()
          and(True(),False()) -> False()
          and(True(),True()) -> True()
          eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
          eqList(Cons(x,xs),Nil()) -> False()
          eqList(Nil(),Cons(y,ys)) -> False()
          eqList(Nil(),Nil()) -> True()
          gt0(Cons(x,xs),Nil()) -> True()
          gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
          gt0(Nil(),y) -> False()
          lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
          lgth(Nil()) -> Nil()
          monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
          monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
          monus[Ite](True(),Cons(x,xs),y) -> xs
      - Signature:
          {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2
          ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2
          ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1
          ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#
          ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE