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