*** 1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        e1(x1,x1,x,y,z) -> e5(x1,x,y,z)
        e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z)
        e2(x,x,y,z,z) -> e6(x,y,z)
        e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z)
        e2(i(),x,y,z,i()) -> e6(x,y,z)
        e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z)
        e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)
        e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x)
        e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z)
        e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z)
        e5(i(),x,y,z) -> e6(x,y,z)
        f1() -> g1()
        f1() -> g2()
        f2() -> g1()
        f2() -> g2()
        g1() -> h1()
        g1() -> h2()
        g2() -> h1()
        g2() -> h2()
        h1() -> i()
        h2() -> i()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0} / {e6/3,i/0}
      Obligation:
        Innermost
        basic terms: {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2}/{e6,i}
    Applied Processor:
      InnermostRuleRemoval
    Proof:
      Arguments of following rules are not normal-forms.
        e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z)
        e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z)
        e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z)
      All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        e1(x1,x1,x,y,z) -> e5(x1,x,y,z)
        e2(x,x,y,z,z) -> e6(x,y,z)
        e2(i(),x,y,z,i()) -> e6(x,y,z)
        e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z)
        e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)
        e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x)
        e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z)
        e5(i(),x,y,z) -> e6(x,y,z)
        f1() -> g1()
        f1() -> g2()
        f2() -> g1()
        f2() -> g2()
        g1() -> h1()
        g1() -> h2()
        g2() -> h1()
        g2() -> h2()
        h1() -> i()
        h2() -> i()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0} / {e6/3,i/0}
      Obligation:
        Innermost
        basic terms: {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2}/{e6,i}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z))
        e2#(x,x,y,z,z) -> c_2()
        e2#(i(),x,y,z,i()) -> c_3()
        e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4()
        e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z))
        e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6()
        e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z))
        e5#(i(),x,y,z) -> c_8()
        f1#() -> c_9(g1#())
        f1#() -> c_10(g2#())
        f2#() -> c_11(g1#())
        f2#() -> c_12(g2#())
        g1#() -> c_13(h1#())
        g1#() -> c_14(h2#())
        g2#() -> c_15(h1#())
        g2#() -> c_16(h2#())
        h1#() -> c_17()
        h2#() -> c_18()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z))
        e2#(x,x,y,z,z) -> c_2()
        e2#(i(),x,y,z,i()) -> c_3()
        e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4()
        e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z))
        e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6()
        e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z))
        e5#(i(),x,y,z) -> c_8()
        f1#() -> c_9(g1#())
        f1#() -> c_10(g2#())
        f2#() -> c_11(g1#())
        f2#() -> c_12(g2#())
        g1#() -> c_13(h1#())
        g1#() -> c_14(h2#())
        g2#() -> c_15(h1#())
        g2#() -> c_16(h2#())
        h1#() -> c_17()
        h2#() -> c_18()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        e1(x1,x1,x,y,z) -> e5(x1,x,y,z)
        e2(x,x,y,z,z) -> e6(x,y,z)
        e2(i(),x,y,z,i()) -> e6(x,y,z)
        e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z)
        e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)
        e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x)
        e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z)
        e5(i(),x,y,z) -> e6(x,y,z)
        f1() -> g1()
        f1() -> g2()
        f2() -> g1()
        f2() -> g2()
        g1() -> h1()
        g1() -> h2()
        g2() -> h1()
        g2() -> h2()
        h1() -> i()
        h2() -> i()
      Signature:
        {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
      Obligation:
        Innermost
        basic terms: {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#,h2#}/{e6,i}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z))
        e2#(x,x,y,z,z) -> c_2()
        e2#(i(),x,y,z,i()) -> c_3()
        e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4()
        e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z))
        e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6()
        e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z))
        e5#(i(),x,y,z) -> c_8()
        f1#() -> c_9(g1#())
        f1#() -> c_10(g2#())
        f2#() -> c_11(g1#())
        f2#() -> c_12(g2#())
        g1#() -> c_13(h1#())
        g1#() -> c_14(h2#())
        g2#() -> c_15(h1#())
        g2#() -> c_16(h2#())
        h1#() -> c_17()
        h2#() -> c_18()
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z))
        e2#(x,x,y,z,z) -> c_2()
        e2#(i(),x,y,z,i()) -> c_3()
        e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4()
        e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z))
        e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6()
        e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z))
        e5#(i(),x,y,z) -> c_8()
        f1#() -> c_9(g1#())
        f1#() -> c_10(g2#())
        f2#() -> c_11(g1#())
        f2#() -> c_12(g2#())
        g1#() -> c_13(h1#())
        g1#() -> c_14(h2#())
        g2#() -> c_15(h1#())
        g2#() -> c_16(h2#())
        h1#() -> c_17()
        h2#() -> c_18()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
      Obligation:
        Innermost
        basic terms: {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#,h2#}/{e6,i}
    Applied Processor:
      Trivial
    Proof:
      Consider the dependency graph
        1:S:e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z))
           -->_1 e5#(i(),x,y,z) -> c_8():8
        
        2:S:e2#(x,x,y,z,z) -> c_2()
           
        
        3:S:e2#(i(),x,y,z,i()) -> c_3()
           
        
        4:S:e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4()
           
        
        5:S:e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z))
           -->_1 e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)):7
           -->_1 e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6():6
        
        6:S:e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6()
           
        
        7:S:e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z))
           -->_1 e5#(i(),x,y,z) -> c_8():8
        
        8:S:e5#(i(),x,y,z) -> c_8()
           
        
        9:S:f1#() -> c_9(g1#())
           -->_1 g1#() -> c_14(h2#()):14
           -->_1 g1#() -> c_13(h1#()):13
        
        10:S:f1#() -> c_10(g2#())
           -->_1 g2#() -> c_16(h2#()):16
           -->_1 g2#() -> c_15(h1#()):15
        
        11:S:f2#() -> c_11(g1#())
           -->_1 g1#() -> c_14(h2#()):14
           -->_1 g1#() -> c_13(h1#()):13
        
        12:S:f2#() -> c_12(g2#())
           -->_1 g2#() -> c_16(h2#()):16
           -->_1 g2#() -> c_15(h1#()):15
        
        13:S:g1#() -> c_13(h1#())
           -->_1 h1#() -> c_17():17
        
        14:S:g1#() -> c_14(h2#())
           -->_1 h2#() -> c_18():18
        
        15:S:g2#() -> c_15(h1#())
           -->_1 h1#() -> c_17():17
        
        16:S:g2#() -> c_16(h2#())
           -->_1 h2#() -> c_18():18
        
        17:S:h1#() -> c_17()
           
        
        18:S:h2#() -> c_18()
           
        
      The dependency graph contains no loops, we remove all dependency pairs.
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
      Obligation:
        Innermost
        basic terms: {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#,h2#}/{e6,i}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).