(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D)
(RULES
  f6(A, B, C, D) -> Com_1(f7(A, B, C, D)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ 0 >= A + 1 ]
  f6(A, B, C, D) -> Com_1(f7(A, B, C, D)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ A >= 1 ]
  f0(A, B, C, D) -> Com_1(f4(A, B, C, B + 1)) [ B >= 0 /\ C >= B ]
  f4(A, B, C, D) -> Com_1(f6(E, B, C, D)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ B >= D + 1 ]
  f4(A, B, C, D) -> Com_1(f6(E, B, C, D)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ D >= B + 1 ]
  f7(A, B, C, D) -> Com_1(f4(A, B, C, D + 1)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ C >= D ]
  f7(A, B, C, D) -> Com_1(f4(A, B, C, 0)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ D >= C + 1 ]
  f6(A, B, C, D) -> Com_1(f14(0, B, C, D)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ A = 0 ]
  f4(A, B, C, D) -> Com_1(f14(A, B, C, B)) [ C - D + 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ -B + C >= 0 /\ B >= 0 /\ B = D ]
)