(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS divByTwo))
(VAR A B)
(RULES
  divByTwo(A) -> Com_1(m2(A)) :|: A >= 1
  m0(A) -> Com_1(m1(A))
  m5(A) -> Com_2(m3(A),m0(A)) :|: A >= 1
  m2(A) -> Com_1(m5(A)) :|: A >= 1
  m6(A) -> Com_1(m0(B)) :|: A >= 2*B && A >= 1
  m1(A) -> Com_1(m6(A))
  m1(A) -> Com_1(m4(A))
)