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