(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalterminatestart)) (VAR A B C) (RULES evalterminatestart(A, B, C) -> Com_1(evalterminateentryin(A, B, C)) evalterminateentryin(A, B, C) -> Com_1(evalterminatebb1in(B, A, C)) evalterminatebb1in(A, B, C) -> Com_1(evalterminatebbin(A, B, C)) [ 100 >= B /\ A >= C ] evalterminatebb1in(A, B, C) -> Com_1(evalterminatereturnin(A, B, C)) [ B >= 101 ] evalterminatebb1in(A, B, C) -> Com_1(evalterminatereturnin(A, B, C)) [ C >= A + 1 ] evalterminatebbin(A, B, C) -> Com_1(evalterminatebb1in(A - 1, C, B + 1)) [ A - C >= 0 /\ -B + 100 >= 0 ] evalterminatereturnin(A, B, C) -> Com_1(evalterminatestop(A, B, C)) )