(STRATEGY
    INNERMOST)

(VAR
    w x x1 x2 x3 x4 y z)
(DATATYPES
    A = µX.< a, i, e6(X, X, X) >)
(SIGNATURES
    f1 :: [A x A] -> A
    f2 :: [A x A] -> A
    g1 :: [A x A] -> A
    g2 :: [A x A] -> A
    h1 :: [A] -> A
    h2 :: [A] -> A
    e1 :: [A x A x A x A x A x A] -> A
    e2 :: [A x A x A x A x A x A] -> A
    e3 :: [A x A x A x A x A x A x A x A x A x A x A x A] -> A
    e4 :: [A x A x A x A x A x A x A x A x A x A x A x A] -> A
    e5 :: [A x A x A x A] -> A)
(RULES
    f1(a(),x) -> g1(x,x)
    f1(x,a()) -> g2(x,x)
    f2(a(),x) -> g1(x,x)
    f2(x,a()) -> g2(x,x)
    g1(a(),x) -> h1(x)
    g1(x,a()) -> h2(x)
    g2(a(),x) -> h1(x)
    g2(x,a()) -> h2(x)
    h1(a()) -> i()
    h2(a()) -> i()
    e1(h1(w),h2(w),x,y,z,w) -> e2(x
                                 ,x
                                 ,y
                                 ,z
                                 ,z
                                 ,w)
    e1(x1,x1,x,y,z,a()) -> e5(x1
                             ,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(x,x,y,z,z,a()) -> e6(x,y,z)
    e2(i(),x,y,z,i(),a()) -> 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(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)
    e4(x,x,x,x,x,x,x,x,x,x,x,a()) ->
      e6(x,x,x)
    e5(i(),x,y,z) -> e6(x,y,z))