(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalsipma91start))
(VAR A B C D)
(RULES
  evalsipma91start(A, B, C, D) -> Com_1(evalsipma91entryin(A, B, C, D))
  evalsipma91entryin(A, B, C, D) -> Com_1(evalsipma91bb3in(1, A, C, D)) [ 100 >= A ]
  evalsipma91entryin(A, B, C, D) -> Com_1(evalsipma91returnin(A, B, C, D)) [ A >= 101 ]
  evalsipma91bb3in(A, B, C, D) -> Com_1(evalsipma91bb2in(A, B, C, D)) [ A - 1 >= 0 /\ 100 >= B ]
  evalsipma91returnin(A, B, C, D) -> Com_1(evalsipma91stop(A, B, C, D)) [ A - 1 >= 0 ]
  evalsipma91bb2in(A, B, C, D) -> Com_1(evalsipma91bb3in(A + 1, B + 11, C, D)) [ -B + 100 >= 0 /\ A - B + 99 >= 0 /\ A - 1 >= 0 ]
  evalsipma91bb3in(A, B, C, D) -> Com_1(evalsipma91bb11in(A, B, C, D)) [ A - 1 >= 0 /\ B >= 101 ]
  evalsipma91bb11in(A, B, C, D) -> Com_1(evalsipma91returnin(A, B, C, D)) [ B - 101 >= 0 /\ A + B - 102 >= 0 /\ A - 1 >= 0 /\ 1 >= A ]
  evalsipma91bb11in(A, B, C, D) -> Com_1(evalsipma91bb5in(A, B, C, D)) [ B - 101 >= 0 /\ A + B - 102 >= 0 /\ A - 1 >= 0 /\ A >= 2 ]
  evalsipma91bb5in(A, B, C, D) -> Com_1(evalsipma91bb11in(A - 1, B - 10, C, D)) [ B - 101 >= 0 /\ A + B - 103 >= 0 /\ A - 2 >= 0 /\ B >= 111 /\ A = 2 ]
  evalsipma91bb5in(A, B, C, D) -> Com_1(evalsipma91bb8in(A, B, B - 10, A - 1)) [ B - 101 >= 0 /\ A + B - 103 >= 0 /\ A - 2 >= 0 /\ A >= 3 ]
  evalsipma91bb5in(A, B, C, D) -> Com_1(evalsipma91bb8in(A, B, B - 10, A - 1)) [ B - 101 >= 0 /\ A + B - 103 >= 0 /\ A - 2 >= 0 /\ 110 >= B ]
  evalsipma91bb8in(A, B, C, D) -> Com_1(evalsipma91bb11in(D + 1, C + 11, C, D)) [ A - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 92 >= 0 /\ B + D - 102 >= 0 /\ A + D - 3 >= 0 /\ -A + D + 1 >= 0 /\ B - C - 10 >= 0 /\ C - 91 >= 0 /\ B + C - 192 >= 0 /\ -B + C + 10 >= 0 /\ A + C - 93 >= 0 /\ B - 101 >= 0 /\ A + B - 103 >= 0 /\ A - 2 >= 0 /\ 100 >= C ]
  evalsipma91bb8in(A, B, C, D) -> Com_1(evalsipma91bb11in(D, C + 1, C, D)) [ A - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 92 >= 0 /\ B + D - 102 >= 0 /\ A + D - 3 >= 0 /\ -A + D + 1 >= 0 /\ B - C - 10 >= 0 /\ C - 91 >= 0 /\ B + C - 192 >= 0 /\ -B + C + 10 >= 0 /\ A + C - 93 >= 0 /\ B - 101 >= 0 /\ A + B - 103 >= 0 /\ A - 2 >= 0 /\ C >= 101 ]
)