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