(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f6))
(VAR A B C D)
(RULES
  f0(A,B,C) -> Com_1(f3(-A,B,C))
  f3(A,B,C) -> Com_1(f7(0,D,C)) :|: A = 0
  f4(A,B,C) -> Com_1(f7(0,D,C)) :|: A = 0
  f6(A,B,C) -> Com_1(f4(A,B,1)) :|: A >= 1
  f3(A,B,C) -> Com_1(f4(-1 - A,B,1)) :|: 0 >= A + 1 && 0 >= C
  f3(A,B,C) -> Com_1(f4(-1 - A,B,1)) :|: 0 >= A + 1 && C >= 2
  f3(A,B,C) -> Com_1(f4(-1 - A,B,1)) :|: A >= 1 && 0 >= C
  f3(A,B,C) -> Com_1(f4(-1 - A,B,1)) :|: A >= 1 && C >= 2
  f4(A,B,C) -> Com_1(f3(1 - A,B,0)) :|: 0 >= A + 1 && C = 1
  f4(A,B,C) -> Com_1(f3(1 - A,B,0)) :|: A >= 1 && C = 1
  f5(A,B,C) -> Com_1(f3(1 - A,B,0)) :|: 0 >= A + 1 && C = 1
  f5(A,B,C) -> Com_1(f3(1 - A,B,0)) :|: A >= 1 && C = 1
)