(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D)
(RULES
  f0(A, B, C, D) -> Com_1(f1(A, B, 2, D)) [ A >= 0 /\ 3 >= A /\ 3 >= B /\ B >= 0 ]
  f1(A, B, C, D) -> Com_1(f1(A, B + 1, C, B + 1)) [ -C + 2 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 5 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 5 >= 0 /\ C - 2 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -A + C + 1 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ C + A >= 2*B + 1 ]
  f1(A, B, C, D) -> Com_1(f1(A, B - 1, C, B - 1)) [ -C + 2 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 5 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 5 >= 0 /\ C - 2 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -A + C + 1 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ 2*B >= C + A + 2 ]
)