(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G)
(RULES
  f0(A, B, C, D, E, F, G) -> Com_1(f12(2, H, I, 0, E, F, G))
  f12(A, B, C, D, E, F, G) -> Com_1(f15(A, B, C, D, 0, F, G)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ A >= D + 1 ]
  f15(A, B, C, D, E, F, G) -> Com_1(f15(A, B, C, D, E + 1, F, G)) [ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ A >= E + 1 ]
  f23(A, B, C, D, E, F, G) -> Com_1(f26(A, B, C, D, 0, F, G)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ A >= D + 1 ]
  f26(A, B, C, D, E, F, G) -> Com_1(f30(A, B, C, D, E, 0, G)) [ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ A >= E + 1 ]
  f30(A, B, C, D, E, F, G) -> Com_1(f30(A, B, C, D, E, F + 1, G)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ A + F - 2 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ A >= F + 1 ]
  f30(A, B, C, D, E, F, G) -> Com_1(f26(A, B, C, D, E + 1, F, G)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ A + F - 2 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ F >= A ]
  f26(A, B, C, D, E, F, G) -> Com_1(f23(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ E >= A ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 0)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 1)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A /\ 49 >= H ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 1)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 1)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A /\ 42 >= H ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 1)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A /\ 21 >= H ]
  f23(A, B, C, D, E, F, G) -> Com_1(f52(A, B, C, D, E, F, 1)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A /\ 18 >= H ]
  f15(A, B, C, D, E, F, G) -> Com_1(f12(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ A + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ E >= A ]
  f12(A, B, C, D, E, F, G) -> Com_1(f23(A, B, C, 0, E, F, G)) [ D >= 0 /\ A + D - 2 >= 0 /\ -A + D + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ D >= A ]
)