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