(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval_random2d_start)) (VAR v_1 v_2 v_N v_i_0) (RULES eval_random2d_start(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb0_in(v_1, v_2, v_N, v_i_0)) eval_random2d_bb0_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_0(v_1, v_2, v_N, v_i_0)) eval_random2d_0(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_1(v_1, v_2, v_N, v_i_0)) eval_random2d_1(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_2(v_1, v_2, v_N, v_i_0)) eval_random2d_2(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_3(v_1, v_2, v_N, v_i_0)) eval_random2d_3(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_4(v_1, v_2, v_N, v_i_0)) eval_random2d_4(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_5(v_1, v_2, v_N, v_i_0)) eval_random2d_5(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_6(v_1, v_2, v_N, v_i_0)) eval_random2d_6(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_7(v_1, v_2, v_N, v_i_0)) eval_random2d_7(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_8(v_1, v_2, v_N, v_i_0)) eval_random2d_8(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_9(v_1, v_2, v_N, v_i_0)) eval_random2d_9(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_10(v_1, v_2, v_N, v_i_0)) eval_random2d_10(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, 0)) eval_random2d_bb1_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb8_in(v_1, v_2, v_N, v_i_0)) [ v_i_0 >= 0 /\ v_i_0 >= v_N ] eval_random2d_bb1_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb2_in(v_1, v_2, v_N, v_i_0)) [ v_i_0 >= 0 /\ v_i_0 < v_N ] eval_random2d_bb8_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_stop(v_1, v_2, v_N, v_i_0)) [ v_i_0 >= 0 /\ -v_N + v_i_0 >= 0 ] eval_random2d_bb2_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_12(v_i_0 + 1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_N - 1 >= 0 ] eval_random2d_12(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_13(v_1, nondef_0, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ v_1 - 1 >= 0 ] eval_random2d_13(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ v_1 - 1 >= 0 /\ v_2 > 3 ] eval_random2d_13(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ v_1 - 1 >= 0 /\ v_2 < 0 ] eval_random2d_13(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb3_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ v_1 - 1 >= 0 /\ v_2 >= 0 /\ v_2 <= 3 ] eval_random2d_bb3_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_NodeBlock9_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 ] eval_random2d_NodeBlock9_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_NodeBlock7_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 /\ v_2 >= 2 ] eval_random2d_NodeBlock9_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_NodeBlock_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 /\ v_2 < 2 ] eval_random2d_NodeBlock7_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_LeafBlock5_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 3 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 - 2 >= 0 /\ v_1 + v_2 - 3 >= 0 /\ v_1 - 1 >= 0 /\ v_2 >= 3 ] eval_random2d_NodeBlock7_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_LeafBlock3_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 3 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 - 2 >= 0 /\ v_1 + v_2 - 3 >= 0 /\ v_1 - 1 >= 0 /\ v_2 < 3 ] eval_random2d_NodeBlock_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_LeafBlock1_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 + 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 1 >= 0 /\ v_1 - v_2 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 /\ v_2 >= 1 ] eval_random2d_NodeBlock_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_LeafBlock_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 + 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 1 >= 0 /\ v_1 - v_2 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 /\ v_2 < 1 ] eval_random2d_LeafBlock5_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb7_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 4 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 - 3 >= 0 /\ v_1 + v_2 - 4 >= 0 /\ v_1 - 1 >= 0 /\ v_2 = 3 ] eval_random2d_LeafBlock3_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb6_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ -v_2 + v_i_0 + 2 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 3 >= 0 /\ -v_2 + v_N + 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 2 >= 0 /\ v_1 - v_2 + 1 >= 0 /\ v_2 - 2 >= 0 /\ v_1 + v_2 - 3 >= 0 /\ v_1 - 1 >= 0 /\ v_2 = 2 ] eval_random2d_LeafBlock1_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb5_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 1 >= 0 /\ -v_2 + v_i_0 + 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 2 >= 0 /\ -v_2 + v_N >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 1 >= 0 /\ v_1 - v_2 >= 0 /\ v_2 - 1 >= 0 /\ v_1 + v_2 - 2 >= 0 /\ v_1 - 1 >= 0 /\ v_2 = 1 ] eval_random2d_LeafBlock_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb4_in(v_1, v_2, v_N, v_i_0)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 >= 0 /\ v_1 - v_2 - 1 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 /\ v_2 = 0 ] eval_random2d_bb7_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ -v_2 + v_i_0 + 3 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 4 >= 0 /\ -v_2 + v_N + 2 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 3 >= 0 /\ v_1 - v_2 + 2 >= 0 /\ v_2 - 3 >= 0 /\ v_1 + v_2 - 4 >= 0 /\ v_1 - 1 >= 0 ] eval_random2d_bb6_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ -v_2 + v_i_0 + 2 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 3 >= 0 /\ -v_2 + v_N + 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 2 >= 0 /\ v_1 - v_2 + 1 >= 0 /\ v_2 - 2 >= 0 /\ v_1 + v_2 - 3 >= 0 /\ v_1 - 1 >= 0 ] eval_random2d_bb5_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 1 >= 0 /\ -v_2 + v_i_0 + 1 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 2 >= 0 /\ -v_2 + v_N >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 + 1 >= 0 /\ v_1 - v_2 >= 0 /\ v_2 - 1 >= 0 /\ v_1 + v_2 - 2 >= 0 /\ v_1 - 1 >= 0 ] eval_random2d_bb4_in(v_1, v_2, v_N, v_i_0) -> Com_1(eval_random2d_bb1_in(v_1, v_2, v_N, v_1)) [ v_N - v_i_0 - 1 >= 0 /\ v_1 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_N + v_i_0 - 1 >= 0 /\ v_2 + v_i_0 >= 0 /\ -v_2 + v_i_0 >= 0 /\ v_1 + v_i_0 - 1 >= 0 /\ -v_1 + v_i_0 + 1 >= 0 /\ v_N - 1 >= 0 /\ v_2 + v_N - 1 >= 0 /\ -v_2 + v_N - 1 >= 0 /\ v_1 + v_N - 2 >= 0 /\ -v_1 + v_N >= 0 /\ -v_2 >= 0 /\ v_1 - v_2 - 1 >= 0 /\ v_2 >= 0 /\ v_1 + v_2 - 1 >= 0 /\ v_1 - 1 >= 0 ] )