(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f2))
(VAR A B C D)
(RULES
  f1(A, B, C, D) -> Com_1(f300(A, B, C, E)) [ A >= B /\ A >= B + 1 ]
  f1(A, B, C, D) -> Com_1(f1(A, A, 0, D)) [ B >= E /\ A = B ]
  f1(A, B, C, D) -> Com_1(f1(A + 1, A, E, D)) [ 0 >= E + 1 /\ B >= F /\ A = B ]
  f1(A, B, C, D) -> Com_1(f1(A + 1, A, E, D)) [ E >= 1 /\ B >= F /\ A = B ]
  f1(A, B, C, D) -> Com_1(f1(A, B, 0, D)) [ B >= A + 1 ]
  f1(A, B, C, D) -> Com_1(f1(A + 1, B, E, D)) [ 0 >= E + 1 /\ B >= A + 1 ]
  f1(A, B, C, D) -> Com_1(f1(A + 1, B, E, D)) [ E >= 1 /\ B >= A + 1 ]
  f2(A, B, C, D) -> Com_1(f1(A, B, C, D))
)