We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We add the following dependency tuples:

Strict DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w))
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(f1(w, w), x, y, z, f2(w, w), w) ->
    c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w))
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  , e4^#(g1(w, w),
         x1,
         g2(w, w),
         x1,
         g1(w, w),
         x1,
         g2(w, w),
         x1,
         x,
         y,
         z,
         w)
    -> c_20(e1^#(x1, x1, x, y, z, w))
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w))
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(f1(w, w), x, y, z, f2(w, w), w) ->
    c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w))
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  , e4^#(g1(w, w),
         x1,
         g2(w, w),
         x1,
         g1(w, w),
         x1,
         g2(w, w),
         x1,
         x,
         y,
         z,
         w)
    -> c_20(e1^#(x1, x1, x, y, z, w))
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }
Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Consider the dependency graph:

  1: f1^#(x, a()) -> c_1(g2^#(x, x))
     -->_1 g2^#(a(), x) -> c_6(h1^#(x)) :4
     -->_1 g2^#(x, a()) -> c_5(h2^#(x)) :3
  
  2: f1^#(a(), x) -> c_2(g1^#(x, x))
     -->_1 g1^#(a(), x) -> c_4(h1^#(x)) :6
     -->_1 g1^#(x, a()) -> c_3(h2^#(x)) :5
  
  3: g2^#(x, a()) -> c_5(h2^#(x)) -->_1 h2^#(a()) -> c_10() :7
  
  4: g2^#(a(), x) -> c_6(h1^#(x)) -->_1 h1^#(a()) -> c_9() :8
  
  5: g1^#(x, a()) -> c_3(h2^#(x)) -->_1 h2^#(a()) -> c_10() :7
  
  6: g1^#(a(), x) -> c_4(h1^#(x)) -->_1 h1^#(a()) -> c_9() :8
  
  7: h2^#(a()) -> c_10()
  
  8: h1^#(a()) -> c_9()
  
  9: f2^#(x, a()) -> c_7(g2^#(x, x))
     -->_1 g2^#(a(), x) -> c_6(h1^#(x)) :4
     -->_1 g2^#(x, a()) -> c_5(h2^#(x)) :3
  
  10: f2^#(a(), x) -> c_8(g1^#(x, x))
     -->_1 g1^#(a(), x) -> c_4(h1^#(x)) :6
     -->_1 g1^#(x, a()) -> c_3(h2^#(x)) :5
  
  11: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
     -->_1 e5^#(i(), x, y, z) -> c_16() :13
  
  12: e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w))
     -->_1 e2^#(f1(w, w), x, y, z, f2(w, w), w) ->
           c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) :15
  
  13: e5^#(i(), x, y, z) -> c_16()
  
  14: e2^#(x, x, y, z, z, a()) -> c_13()
  
  15: e2^#(f1(w, w), x, y, z, f2(w, w), w) ->
      c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w))
     -->_1 e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
           c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) :17
  
  16: e2^#(i(), x, y, z, i(), a()) -> c_15()
  
  17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
      c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
     -->_1 e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
           c_21(e5^#(x1, x, y, z)) :21
     -->_1 e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() :19
  
  18: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  
  19: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  
  20: e4^#(g1(w, w),
           x1,
           g2(w, w),
           x1,
           g1(w, w),
           x1,
           g2(w, w),
           x1,
           x,
           y,
           z,
           w)
      -> c_20(e1^#(x1, x1, x, y, z, w))
  
  21: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
      c_21(e5^#(x1, x, y, z))
     -->_1 e5^#(i(), x, y, z) -> c_16() :13
  

Only the nodes {1,4,8,3,7,2,6,5,9,10,11,13,14,16,17,21,19,18} are
reachable from nodes {1,2,3,4,5,6,7,8,9,10,11,13,14,16,17,18,19,21}
that start derivation from marked basic terms. The nodes not
reachable are removed from the problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }
Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {7,8,12,13,14,16,17} by
applications of Pre({7,8,12,13,14,16,17}) = {3,4,5,6,11,15,18}.
Here rules are labeled as follows:

  DPs:
    { 1: f1^#(x, a()) -> c_1(g2^#(x, x))
    , 2: f1^#(a(), x) -> c_2(g1^#(x, x))
    , 3: g2^#(x, a()) -> c_5(h2^#(x))
    , 4: g2^#(a(), x) -> c_6(h1^#(x))
    , 5: g1^#(x, a()) -> c_3(h2^#(x))
    , 6: g1^#(a(), x) -> c_4(h1^#(x))
    , 7: h2^#(a()) -> c_10()
    , 8: h1^#(a()) -> c_9()
    , 9: f2^#(x, a()) -> c_7(g2^#(x, x))
    , 10: f2^#(a(), x) -> c_8(g1^#(x, x))
    , 11: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
    , 12: e5^#(i(), x, y, z) -> c_16()
    , 13: e2^#(x, x, y, z, z, a()) -> c_13()
    , 14: e2^#(i(), x, y, z, i(), a()) -> c_15()
    , 15: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
          c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
    , 16: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
    , 17: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
    , 18: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
          c_21(e5^#(x1, x, y, z)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }
Weak DPs:
  { h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() }
Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {3,4,5,6,9,11} by
applications of Pre({3,4,5,6,9,11}) = {1,2,7,8,10}. Here rules are
labeled as follows:

  DPs:
    { 1: f1^#(x, a()) -> c_1(g2^#(x, x))
    , 2: f1^#(a(), x) -> c_2(g1^#(x, x))
    , 3: g2^#(x, a()) -> c_5(h2^#(x))
    , 4: g2^#(a(), x) -> c_6(h1^#(x))
    , 5: g1^#(x, a()) -> c_3(h2^#(x))
    , 6: g1^#(a(), x) -> c_4(h1^#(x))
    , 7: f2^#(x, a()) -> c_7(g2^#(x, x))
    , 8: f2^#(a(), x) -> c_8(g1^#(x, x))
    , 9: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
    , 10: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
          c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
    , 11: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
          c_21(e5^#(x1, x, y, z))
    , 12: h2^#(a()) -> c_10()
    , 13: h1^#(a()) -> c_9()
    , 14: e5^#(i(), x, y, z) -> c_16()
    , 15: e2^#(x, x, y, z, z, a()) -> c_13()
    , 16: e2^#(i(), x, y, z, i(), a()) -> c_15()
    , 17: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
    , 18: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) }
Weak DPs:
  { g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }
Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1,2,3,4,5} by
applications of Pre({1,2,3,4,5}) = {}. Here rules are labeled as
follows:

  DPs:
    { 1: f1^#(x, a()) -> c_1(g2^#(x, x))
    , 2: f1^#(a(), x) -> c_2(g1^#(x, x))
    , 3: f2^#(x, a()) -> c_7(g2^#(x, x))
    , 4: f2^#(a(), x) -> c_8(g1^#(x, x))
    , 5: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
         c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
    , 6: g2^#(x, a()) -> c_5(h2^#(x))
    , 7: g2^#(a(), x) -> c_6(h1^#(x))
    , 8: g1^#(x, a()) -> c_3(h2^#(x))
    , 9: g1^#(a(), x) -> c_4(h1^#(x))
    , 10: h2^#(a()) -> c_10()
    , 11: h1^#(a()) -> c_9()
    , 12: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
    , 13: e5^#(i(), x, y, z) -> c_16()
    , 14: e2^#(x, x, y, z, z, a()) -> c_13()
    , 15: e2^#(i(), x, y, z, i(), a()) -> c_15()
    , 16: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
    , 17: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
    , 18: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
          c_21(e5^#(x1, x, y, z)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
  { f1^#(x, a()) -> c_1(g2^#(x, x))
  , f1^#(a(), x) -> c_2(g1^#(x, x))
  , g2^#(x, a()) -> c_5(h2^#(x))
  , g2^#(a(), x) -> c_6(h1^#(x))
  , g1^#(x, a()) -> c_3(h2^#(x))
  , g1^#(a(), x) -> c_4(h1^#(x))
  , h2^#(a()) -> c_10()
  , h1^#(a()) -> c_9()
  , f2^#(x, a()) -> c_7(g2^#(x, x))
  , f2^#(a(), x) -> c_8(g1^#(x, x))
  , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
  , e5^#(i(), x, y, z) -> c_16()
  , e2^#(x, x, y, z, z, a()) -> c_13()
  , e2^#(i(), x, y, z, i(), a()) -> c_15()
  , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
  , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
  , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
  , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    c_21(e5^#(x1, x, y, z)) }
Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ f1^#(x, a()) -> c_1(g2^#(x, x))
, f1^#(a(), x) -> c_2(g1^#(x, x))
, g2^#(x, a()) -> c_5(h2^#(x))
, g2^#(a(), x) -> c_6(h1^#(x))
, g1^#(x, a()) -> c_3(h2^#(x))
, g1^#(a(), x) -> c_4(h1^#(x))
, h2^#(a()) -> c_10()
, h1^#(a()) -> c_9()
, f2^#(x, a()) -> c_7(g2^#(x, x))
, f2^#(a(), x) -> c_8(g1^#(x, x))
, e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_16()
, e2^#(x, x, y, z, z, a()) -> c_13()
, e2^#(i(), x, y, z, i(), a()) -> c_15()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
  c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))
, e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18()
, e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
  c_21(e5^#(x1, x, y, z)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { f1(x, a()) -> g2(x, x)
  , f1(a(), x) -> g1(x, x)
  , g1(x, a()) -> h2(x)
  , g1(a(), x) -> h1(x)
  , g2(x, a()) -> h2(x)
  , g2(a(), x) -> h1(x)
  , f2(x, a()) -> g2(x, x)
  , f2(a(), x) -> g1(x, x)
  , h1(a()) -> i()
  , h2(a()) -> i()
  , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z)
  , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w)
  , e2(x, x, y, z, z, a()) -> e6(x, y, z)
  , e2(f1(w, w), x, y, z, f2(w, w), w) ->
    e3(x, y, x, y, y, z, y, z, x, y, z, w)
  , e2(i(), x, y, z, i(), a()) -> e6(x, y, z)
  , e5(i(), x, y, z) -> e6(x, y, z)
  , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) ->
    e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
  , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z)
  , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x)
  , e4(g1(w, w),
       x1,
       g2(w, w),
       x1,
       g1(w, w),
       x1,
       g2(w, w),
       x1,
       x,
       y,
       z,
       w)
    -> e1(x1, x1, x, y, z, w)
  , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) ->
    e5(x1, x, y, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(1))