YES(?,PRIMREC) * Step 1: FromIts MAYBE + Considered Problem: Rules: 0. eval_counterex1b_start(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb0_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (1,1) 1. eval_counterex1b_bb0_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 2. eval_counterex1b_0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 3. eval_counterex1b_1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 4. eval_counterex1b_2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 5. eval_counterex1b_3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 6. eval_counterex1b_4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b__critedge2_in(v_x,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) True (?,1) 7. eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb1_in(v__0,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] (?,1) 8. eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb7_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [-1*v__0 + v_x >= 0 && -1 >= v__0] (?,1) 9. eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v__1 >= 0] (?,1) 10. eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b__critedge_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 >= v__1] (?,1) 11. eval_counterex1b_bb2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] 12. eval_counterex1b_5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_6(v__0,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] 13. eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb3_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && -1 + v_2 >= 0] 14. eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b__critedge_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && 0 >= v_2] 15. eval_counterex1b_bb3_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb1_in(v__0,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] 16. eval_counterex1b__critedge_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_10(v__0,v__01,v__1,v__2,v_2,-1 + v__0,v_7,v_n,v_x,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] (?,1) 17. eval_counterex1b_10(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 18. eval_counterex1b_11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 19. eval_counterex1b_12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb4_in(v__0,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 20. eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb5_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v_n >= v__2] 21. eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b__critedge2_in(v_5,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] 22. eval_counterex1b_bb5_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 23. eval_counterex1b_13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 24. eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb6_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v_7 >= 0] 25. eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b__critedge2_in(v_5,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] 26. eval_counterex1b_bb6_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_bb4_in(v__0,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x,v_y) [v_x >= 0 (?,1) && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] 27. eval_counterex1b_bb7_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_stop(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) [-1*v__0 + v_x >= 0 && -1 + -1*v__0 >= 0] (?,1) Signature: {(eval_counterex1b_0,10) ;(eval_counterex1b_1,10) ;(eval_counterex1b_10,10) ;(eval_counterex1b_11,10) ;(eval_counterex1b_12,10) ;(eval_counterex1b_13,10) ;(eval_counterex1b_14,10) ;(eval_counterex1b_2,10) ;(eval_counterex1b_3,10) ;(eval_counterex1b_4,10) ;(eval_counterex1b_5,10) ;(eval_counterex1b_6,10) ;(eval_counterex1b__critedge2_in,10) ;(eval_counterex1b__critedge_in,10) ;(eval_counterex1b_bb0_in,10) ;(eval_counterex1b_bb1_in,10) ;(eval_counterex1b_bb2_in,10) ;(eval_counterex1b_bb3_in,10) ;(eval_counterex1b_bb4_in,10) ;(eval_counterex1b_bb5_in,10) ;(eval_counterex1b_bb6_in,10) ;(eval_counterex1b_bb7_in,10) ;(eval_counterex1b_start,10) ;(eval_counterex1b_stop,10)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8},7->{9,10},8->{27},9->{11},10->{16},11->{12},12->{13 ,14},13->{15},14->{16},15->{9,10},16->{17},17->{18},18->{19},19->{20,21},20->{22},21->{7,8},22->{23},23->{24 ,25},24->{26},25->{7,8},26->{20,21},27->{}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks MAYBE + Considered Problem: Rules: eval_counterex1b_start(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb0_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_bb0_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_0(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_1(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_2(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_3(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_4(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb7_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 >= v__0] eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb2_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v__1 >= 0] eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 >= v__1] eval_counterex1b_bb2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_5(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_6(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb3_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && -1 + v_2 >= 0] eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && 0 >= v_2] eval_counterex1b_bb3_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b__critedge_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_10(v__0 ,v__01,v__1,v__2,v_2,-1 + v__0,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_10(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_11(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_12(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb5_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v_n >= v__2] eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb5_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_13(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_14(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb6_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v_7 >= 0] eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_bb6_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb7_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_stop(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 + -1*v__0 >= 0] Signature: {(eval_counterex1b_0,10) ;(eval_counterex1b_1,10) ;(eval_counterex1b_10,10) ;(eval_counterex1b_11,10) ;(eval_counterex1b_12,10) ;(eval_counterex1b_13,10) ;(eval_counterex1b_14,10) ;(eval_counterex1b_2,10) ;(eval_counterex1b_3,10) ;(eval_counterex1b_4,10) ;(eval_counterex1b_5,10) ;(eval_counterex1b_6,10) ;(eval_counterex1b__critedge2_in,10) ;(eval_counterex1b__critedge_in,10) ;(eval_counterex1b_bb0_in,10) ;(eval_counterex1b_bb1_in,10) ;(eval_counterex1b_bb2_in,10) ;(eval_counterex1b_bb3_in,10) ;(eval_counterex1b_bb4_in,10) ;(eval_counterex1b_bb5_in,10) ;(eval_counterex1b_bb6_in,10) ;(eval_counterex1b_bb7_in,10) ;(eval_counterex1b_start,10) ;(eval_counterex1b_stop,10)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8},7->{9,10},8->{27},9->{11},10->{16},11->{12},12->{13 ,14},13->{15},14->{16},15->{9,10},16->{17},17->{18},18->{19},19->{20,21},20->{22},21->{7,8},22->{23},23->{24 ,25},24->{26},25->{7,8},26->{20,21},27->{}] + Applied Processor: AddSinks + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: eval_counterex1b_start(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb0_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_bb0_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_0(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_1(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_2(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_3(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_4(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb7_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 >= v__0] eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb2_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v__1 >= 0] eval_counterex1b_bb1_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 >= v__1] eval_counterex1b_bb2_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_5(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_6(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb3_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && -1 + v_2 >= 0] eval_counterex1b_6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && 0 >= v_2] eval_counterex1b_bb3_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b__critedge_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_10(v__0 ,v__01,v__1,v__2,v_2,-1 + v__0,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_10(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_11(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_12(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb5_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v_n >= v__2] eval_counterex1b_bb4_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb5_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_13(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_14(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb6_in(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v_7 >= 0] eval_counterex1b_14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_bb6_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb7_in(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> eval_counterex1b_stop(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 + -1*v__0 >= 0] eval_counterex1b_stop(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> exitus616(v__0,v__01,v__1 ,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True Signature: {(eval_counterex1b_0,10) ;(eval_counterex1b_1,10) ;(eval_counterex1b_10,10) ;(eval_counterex1b_11,10) ;(eval_counterex1b_12,10) ;(eval_counterex1b_13,10) ;(eval_counterex1b_14,10) ;(eval_counterex1b_2,10) ;(eval_counterex1b_3,10) ;(eval_counterex1b_4,10) ;(eval_counterex1b_5,10) ;(eval_counterex1b_6,10) ;(eval_counterex1b__critedge2_in,10) ;(eval_counterex1b__critedge_in,10) ;(eval_counterex1b_bb0_in,10) ;(eval_counterex1b_bb1_in,10) ;(eval_counterex1b_bb2_in,10) ;(eval_counterex1b_bb3_in,10) ;(eval_counterex1b_bb4_in,10) ;(eval_counterex1b_bb5_in,10) ;(eval_counterex1b_bb6_in,10) ;(eval_counterex1b_bb7_in,10) ;(eval_counterex1b_start,10) ;(eval_counterex1b_stop,10) ;(exitus616,10)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8},7->{9,10},8->{27},9->{11},10->{16},11->{12},12->{13 ,14},13->{15},14->{16},15->{9,10},16->{17},17->{18},18->{19},19->{20,21},20->{22},21->{7,8},22->{23},23->{24 ,25},24->{26},25->{7,8},26->{20,21},27->{28}] + Applied Processor: Unfold + Details: () * Step 4: Decompose MAYBE + Considered Problem: Rules: eval_counterex1b_start.0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb0_in.1(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_bb0_in.1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_0.2(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_0.2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_1.3(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_1.3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_2.4(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_2.4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_3.5(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_3.5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_4.6(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4.6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4.6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b__critedge2_in.7(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.9(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in.7(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.10(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in.8(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb7_in.27(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 >= v__0] eval_counterex1b_bb1_in.9(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb2_in.11(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v__1 >= 0] eval_counterex1b_bb1_in.10(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in.16(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 >= v__1] eval_counterex1b_bb2_in.11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_5.12(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5.12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_6.13(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5.12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_6.14(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_6.13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb3_in.15(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && -1 + v_2 >= 0] eval_counterex1b_6.14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in.16(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && 0 >= v_2] eval_counterex1b_bb3_in.15(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.9(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_bb3_in.15(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.10(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b__critedge_in.16(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_10.17(v__0 ,v__01,v__1,v__2,v_2,-1 + v__0,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_10.17(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_11.18(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_11.18(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_12.19(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12.19(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.20(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12.19(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.21(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb4_in.20(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb5_in.22(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v_n >= v__2] eval_counterex1b_bb4_in.21(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb4_in.21(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb5_in.22(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_13.23(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13.23(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_14.24(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13.23(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_14.25(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_14.24(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb6_in.26(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v_7 >= 0] eval_counterex1b_14.25(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_14.25(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_bb6_in.26(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.20(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb6_in.26(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.21(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb7_in.27(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_stop.28(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 + -1*v__0 >= 0] eval_counterex1b_stop.28(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> exitus616.29(v__0,v__01 ,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True Signature: {(eval_counterex1b_0.2,10) ;(eval_counterex1b_1.3,10) ;(eval_counterex1b_10.17,10) ;(eval_counterex1b_11.18,10) ;(eval_counterex1b_12.19,10) ;(eval_counterex1b_13.23,10) ;(eval_counterex1b_14.24,10) ;(eval_counterex1b_14.25,10) ;(eval_counterex1b_2.4,10) ;(eval_counterex1b_3.5,10) ;(eval_counterex1b_4.6,10) ;(eval_counterex1b_5.12,10) ;(eval_counterex1b_6.13,10) ;(eval_counterex1b_6.14,10) ;(eval_counterex1b__critedge2_in.7,10) ;(eval_counterex1b__critedge2_in.8,10) ;(eval_counterex1b__critedge_in.16,10) ;(eval_counterex1b_bb0_in.1,10) ;(eval_counterex1b_bb1_in.10,10) ;(eval_counterex1b_bb1_in.9,10) ;(eval_counterex1b_bb2_in.11,10) ;(eval_counterex1b_bb3_in.15,10) ;(eval_counterex1b_bb4_in.20,10) ;(eval_counterex1b_bb4_in.21,10) ;(eval_counterex1b_bb5_in.22,10) ;(eval_counterex1b_bb6_in.26,10) ;(eval_counterex1b_bb7_in.27,10) ;(eval_counterex1b_start.0,10) ;(eval_counterex1b_stop.28,10) ;(exitus616.29,10)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6,7},6->{8,9},7->{10},8->{11},9->{12},10->{36},11->{13},12->{20} ,13->{14,15},14->{16},15->{17},16->{18,19},17->{20},18->{11},19->{12},20->{21},21->{22},22->{23,24},23->{25} ,24->{26,27},25->{28},26->{8,9},27->{10},28->{29,30},29->{31},30->{32,33},31->{34,35},32->{8,9},33->{10} ,34->{25},35->{26,27},36->{37},37->{}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37] | `- p:[8,26,24,22,21,20,12,9,32,30,28,25,23,34,31,29,19,16,14,13,11,18,17,15,35] c: [8,9,12,15,17,19,20,21,22,23,24,26,30,32,35] | +- p:[25,34,31,29,28] c: [25,28,29,31,34] | `- p:[11,18,16,14,13] c: [11,13,14,16,18] * Step 5: AbstractSize MAYBE + Considered Problem: (Rules: eval_counterex1b_start.0(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb0_in.1(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_bb0_in.1(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_0.2(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_0.2(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_1.3(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_1.3(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_2.4(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_2.4(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_3.5(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_3.5(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_4.6(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4.6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b_4.6(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_x ,v_y,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True eval_counterex1b__critedge2_in.7(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.9(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in.7(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.10(v__0 ,v__01,v__01,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && v__0 >= 0] eval_counterex1b__critedge2_in.8(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb7_in.27(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 >= v__0] eval_counterex1b_bb1_in.9(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb2_in.11(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v__1 >= 0] eval_counterex1b_bb1_in.10(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in.16(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 >= v__1] eval_counterex1b_bb2_in.11(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_5.12(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5.12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_6.13(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_5.12(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_6.14(v__0 ,v__01,v__1,v__2,nondef_0,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_6.13(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb3_in.15(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && -1 + v_2 >= 0] eval_counterex1b_6.14(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge_in.16(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0 && 0 >= v_2] eval_counterex1b_bb3_in.15(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.9(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b_bb3_in.15(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb1_in.10(v__0 ,v__01,-1 + v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_2 + v_x >= 0 && v__1 + v_x >= 0 && v__01 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + v_2 >= 0 && -1 + v_2 + v__1 >= 0 && -1 + v_2 + v__01 >= 0 && -1 + v_2 + v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__1 >= 0 && v__01 + v__1 >= 0 && v__0 + v__1 >= 0 && v__01 >= 0 && v__0 + v__01 >= 0 && v__0 >= 0] eval_counterex1b__critedge_in.16(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_10.17(v__0 ,v__01,v__1,v__2,v_2,-1 + v__0,v_7,v_n,v_x ,v_y) [v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_10.17(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_11.18(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_11.18(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_12.19(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12.19(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.20(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_12.19(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.21(v__0 ,v__01,v__1,v__1,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb4_in.20(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb5_in.22(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && v_n >= v__2] eval_counterex1b_bb4_in.21(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb4_in.21(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v__2 >= v_n] eval_counterex1b_bb5_in.22(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_13.23(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13.23(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_14.24(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_13.23(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_14.25(v__0 ,v__01,v__1,v__2,v_2,v_5,nondef_1,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_14.24(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb6_in.26(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && -1 + v_7 >= 0] eval_counterex1b_14.25(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.7(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_14.25(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b__critedge2_in.8(v_5 ,v__2,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0 && 0 >= v_7] eval_counterex1b_bb6_in.26(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.20(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb6_in.26(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_bb4_in.21(v__0 ,v__01,v__1,1 + v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [v_x >= 0 && -1 + v_7 + v_x >= 0 && 1 + v_5 + v_x >= 0 && -1 + -1*v_5 + v_x >= 0 && v__0 + v_x >= 0 && -1*v__0 + v_x >= 0 && -1*v__2 + v_n >= 0 && -1*v__1 + v_n >= 0 && -1 + v_7 >= 0 && v_5 + v_7 >= 0 && -1 + v_7 + v__0 >= 0 && -1 + -1*v_5 + v__0 >= 0 && 1 + v_5 >= 0 && 1 + v_5 + v__0 >= 0 && 1 + v_5 + -1*v__0 >= 0 && -1*v__1 + v__2 >= 0 && v__01 + -1*v__1 >= 0 && v__0 >= 0] eval_counterex1b_bb7_in.27(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) -> eval_counterex1b_stop.28(v__0 ,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) [-1*v__0 + v_x >= 0 && -1 + -1*v__0 >= 0] eval_counterex1b_stop.28(v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y) -> exitus616.29(v__0,v__01 ,v__1,v__2,v_2,v_5,v_7,v_n,v_x ,v_y) True Signature: {(eval_counterex1b_0.2,10) ;(eval_counterex1b_1.3,10) ;(eval_counterex1b_10.17,10) ;(eval_counterex1b_11.18,10) ;(eval_counterex1b_12.19,10) ;(eval_counterex1b_13.23,10) ;(eval_counterex1b_14.24,10) ;(eval_counterex1b_14.25,10) ;(eval_counterex1b_2.4,10) ;(eval_counterex1b_3.5,10) ;(eval_counterex1b_4.6,10) ;(eval_counterex1b_5.12,10) ;(eval_counterex1b_6.13,10) ;(eval_counterex1b_6.14,10) ;(eval_counterex1b__critedge2_in.7,10) ;(eval_counterex1b__critedge2_in.8,10) ;(eval_counterex1b__critedge_in.16,10) ;(eval_counterex1b_bb0_in.1,10) ;(eval_counterex1b_bb1_in.10,10) ;(eval_counterex1b_bb1_in.9,10) ;(eval_counterex1b_bb2_in.11,10) ;(eval_counterex1b_bb3_in.15,10) ;(eval_counterex1b_bb4_in.20,10) ;(eval_counterex1b_bb4_in.21,10) ;(eval_counterex1b_bb5_in.22,10) ;(eval_counterex1b_bb6_in.26,10) ;(eval_counterex1b_bb7_in.27,10) ;(eval_counterex1b_start.0,10) ;(eval_counterex1b_stop.28,10) ;(exitus616.29,10)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6,7},6->{8,9},7->{10},8->{11},9->{12},10->{36},11->{13},12->{20} ,13->{14,15},14->{16},15->{17},16->{18,19},17->{20},18->{11},19->{12},20->{21},21->{22},22->{23,24},23->{25} ,24->{26,27},25->{28},26->{8,9},27->{10},28->{29,30},29->{31},30->{32,33},31->{34,35},32->{8,9},33->{10} ,34->{25},35->{26,27},36->{37},37->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37] | `- p:[8,26,24,22,21,20,12,9,32,30,28,25,23,34,31,29,19,16,14,13,11,18,17,15,35] c: [8,9,12,15,17,19,20,21,22,23,24,26,30,32,35] | +- p:[25,34,31,29,28] c: [25,28,29,31,34] | `- p:[11,18,16,14,13] c: [11,13,14,16,18]) + Applied Processor: AbstractSize NoMinimize + Details: () * Step 6: AbstractFlow MAYBE + Considered Problem: Program: Domain: [v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y,0.0,0.0.0,0.0.1] eval_counterex1b_start.0 ~> eval_counterex1b_bb0_in.1 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb0_in.1 ~> eval_counterex1b_0.2 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_0.2 ~> eval_counterex1b_1.3 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_1.3 ~> eval_counterex1b_2.4 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_2.4 ~> eval_counterex1b_3.5 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_3.5 ~> eval_counterex1b_4.6 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_4.6 ~> eval_counterex1b__critedge2_in.7 [v__0 <= v_x, v__01 <= v_y, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_4.6 ~> eval_counterex1b__critedge2_in.8 [v__0 <= v_x, v__01 <= v_y, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.9 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__01, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.10 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__01, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge2_in.8 ~> eval_counterex1b_bb7_in.27 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb1_in.10 ~> eval_counterex1b__critedge_in.16 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= unknown, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_5.12 ~> eval_counterex1b_6.14 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= unknown, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_6.14 ~> eval_counterex1b__critedge_in.16 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__0 <= v__0, v__01 <= v__01, v__1 <= K + v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.10 [v__0 <= v__0, v__01 <= v__01, v__1 <= K + v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge_in.16 ~> eval_counterex1b_10.17 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= K + v__0, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_10.17 ~> eval_counterex1b_11.18 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_11.18 ~> eval_counterex1b_12.19 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.20 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__1, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.21 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__1, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.7 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.8 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= unknown, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_13.23 ~> eval_counterex1b_14.25 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= unknown, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.7 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.8 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= K + v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.21 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= K + v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb7_in.27 ~> eval_counterex1b_stop.28 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_stop.28 ~> exitus616.29 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] + Loop: [0.0 <= v__0] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.9 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__01, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.7 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.21 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__1, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_11.18 ~> eval_counterex1b_12.19 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_10.17 ~> eval_counterex1b_11.18 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge_in.16 ~> eval_counterex1b_10.17 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= K + v__0, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb1_in.10 ~> eval_counterex1b__critedge_in.16 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.10 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__01, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.7 [v__0 <= v_5, v__01 <= v__2, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_13.23 ~> eval_counterex1b_14.25 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= unknown, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.20 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__1, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= K + v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= unknown, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.10 [v__0 <= v__0, v__01 <= v__01, v__1 <= K + v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= unknown, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__0 <= v__0, v__01 <= v__01, v__1 <= K + v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_6.14 ~> eval_counterex1b__critedge_in.16 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_5.12 ~> eval_counterex1b_6.14 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= unknown, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.21 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= K + v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] + Loop: [0.0.0 <= v__2 + v_n] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= K + v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= unknown, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] + Loop: [0.0.1 <= v__1] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__0 <= v__0, v__01 <= v__01, v__1 <= K + v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= unknown, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [v__0 <= v__0, v__01 <= v__01, v__1 <= v__1, v__2 <= v__2, v_2 <= v_2, v_5 <= v_5, v_7 <= v_7, v_n <= v_n, v_x <= v_x, v_y <= v_y] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,v__0,v__01,v__1,v__2,v_2,v_5,v_7,v_n,v_x,v_y,0.0,0.0.0,0.0.1] eval_counterex1b_start.0 ~> eval_counterex1b_bb0_in.1 [] eval_counterex1b_bb0_in.1 ~> eval_counterex1b_0.2 [] eval_counterex1b_0.2 ~> eval_counterex1b_1.3 [] eval_counterex1b_1.3 ~> eval_counterex1b_2.4 [] eval_counterex1b_2.4 ~> eval_counterex1b_3.5 [] eval_counterex1b_3.5 ~> eval_counterex1b_4.6 [] eval_counterex1b_4.6 ~> eval_counterex1b__critedge2_in.7 [v_x ~=> v__0,v_y ~=> v__01] eval_counterex1b_4.6 ~> eval_counterex1b__critedge2_in.8 [v_x ~=> v__0,v_y ~=> v__01] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.9 [v__01 ~=> v__1] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.10 [v__01 ~=> v__1] eval_counterex1b__critedge2_in.8 ~> eval_counterex1b_bb7_in.27 [] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [] eval_counterex1b_bb1_in.10 ~> eval_counterex1b__critedge_in.16 [] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [huge ~=> v_2] eval_counterex1b_5.12 ~> eval_counterex1b_6.14 [huge ~=> v_2] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [] eval_counterex1b_6.14 ~> eval_counterex1b__critedge_in.16 [] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__1 ~+> v__1,K ~+> v__1] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.10 [v__1 ~+> v__1,K ~+> v__1] eval_counterex1b__critedge_in.16 ~> eval_counterex1b_10.17 [v__0 ~+> v_5,K ~+> v_5] eval_counterex1b_10.17 ~> eval_counterex1b_11.18 [] eval_counterex1b_11.18 ~> eval_counterex1b_12.19 [] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.20 [v__1 ~=> v__2] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.21 [v__1 ~=> v__2] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.7 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.8 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [huge ~=> v_7] eval_counterex1b_13.23 ~> eval_counterex1b_14.25 [huge ~=> v_7] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.7 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.8 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__2 ~+> v__2,K ~+> v__2] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.21 [v__2 ~+> v__2,K ~+> v__2] eval_counterex1b_bb7_in.27 ~> eval_counterex1b_stop.28 [] eval_counterex1b_stop.28 ~> exitus616.29 [] + Loop: [v__0 ~=> 0.0] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.9 [v__01 ~=> v__1] eval_counterex1b_bb4_in.21 ~> eval_counterex1b__critedge2_in.7 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.21 [v__1 ~=> v__2] eval_counterex1b_11.18 ~> eval_counterex1b_12.19 [] eval_counterex1b_10.17 ~> eval_counterex1b_11.18 [] eval_counterex1b__critedge_in.16 ~> eval_counterex1b_10.17 [v__0 ~+> v_5,K ~+> v_5] eval_counterex1b_bb1_in.10 ~> eval_counterex1b__critedge_in.16 [] eval_counterex1b__critedge2_in.7 ~> eval_counterex1b_bb1_in.10 [v__01 ~=> v__1] eval_counterex1b_14.25 ~> eval_counterex1b__critedge2_in.7 [v_5 ~=> v__0,v__2 ~=> v__01] eval_counterex1b_13.23 ~> eval_counterex1b_14.25 [huge ~=> v_7] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [] eval_counterex1b_12.19 ~> eval_counterex1b_bb4_in.20 [v__1 ~=> v__2] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__2 ~+> v__2,K ~+> v__2] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [huge ~=> v_7] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.10 [v__1 ~+> v__1,K ~+> v__1] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [huge ~=> v_2] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__1 ~+> v__1,K ~+> v__1] eval_counterex1b_6.14 ~> eval_counterex1b__critedge_in.16 [] eval_counterex1b_5.12 ~> eval_counterex1b_6.14 [huge ~=> v_2] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.21 [v__2 ~+> v__2,K ~+> v__2] + Loop: [v__2 ~+> 0.0.0,v_n ~+> 0.0.0] eval_counterex1b_bb4_in.20 ~> eval_counterex1b_bb5_in.22 [] eval_counterex1b_bb6_in.26 ~> eval_counterex1b_bb4_in.20 [v__2 ~+> v__2,K ~+> v__2] eval_counterex1b_14.24 ~> eval_counterex1b_bb6_in.26 [] eval_counterex1b_13.23 ~> eval_counterex1b_14.24 [huge ~=> v_7] eval_counterex1b_bb5_in.22 ~> eval_counterex1b_13.23 [] + Loop: [v__1 ~=> 0.0.1] eval_counterex1b_bb1_in.9 ~> eval_counterex1b_bb2_in.11 [] eval_counterex1b_bb3_in.15 ~> eval_counterex1b_bb1_in.9 [v__1 ~+> v__1,K ~+> v__1] eval_counterex1b_6.13 ~> eval_counterex1b_bb3_in.15 [] eval_counterex1b_5.12 ~> eval_counterex1b_6.13 [huge ~=> v_2] eval_counterex1b_bb2_in.11 ~> eval_counterex1b_5.12 [] + Applied Processor: Lare + Details: eval_counterex1b_start.0 ~> exitus616.29 [v_5 ~=> v__0 ,v__2 ~=> v__01 ,v__2 ~=> v__1 ,v__2 ~=> 0.0.1 ,v_x ~=> v__0 ,v_x ~=> 0.0 ,v_y ~=> v__01 ,v_y ~=> v__1 ,v_y ~=> v__2 ,v_y ~=> 0.0.1 ,huge ~=> v_2 ,huge ~=> v_7 ,v_5 ~+> v_5 ,v_5 ~+> v__0 ,v__2 ~+> v__01 ,v__2 ~+> v__1 ,v__2 ~+> v__2 ,v__2 ~+> 0.0.0 ,v__2 ~+> 0.0.1 ,v__2 ~+> tick ,v_n ~+> 0.0.0 ,v_n ~+> tick ,v_x ~+> v_5 ,v_x ~+> v__0 ,v_x ~+> tick ,v_y ~+> v__01 ,v_y ~+> v__1 ,v_y ~+> v__2 ,v_y ~+> 0.0.0 ,v_y ~+> 0.0.1 ,v_y ~+> tick ,tick ~+> tick ,K ~+> v_5 ,K ~+> v__0 ,K ~+> v__01 ,K ~+> v__1 ,K ~+> v__2 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,v__2 ~*> v__01 ,v__2 ~*> v__1 ,v__2 ~*> v__2 ,v__2 ~*> 0.0.0 ,v__2 ~*> 0.0.1 ,v__2 ~*> tick ,v_n ~*> v__01 ,v_n ~*> v__1 ,v_n ~*> v__2 ,v_n ~*> 0.0.0 ,v_n ~*> 0.0.1 ,v_n ~*> tick ,v_x ~*> v_5 ,v_x ~*> v__0 ,v_x ~*> v__01 ,v_x ~*> v__1 ,v_x ~*> v__2 ,v_x ~*> 0.0.0 ,v_x ~*> 0.0.1 ,v_x ~*> tick ,v_y ~*> v__01 ,v_y ~*> v__1 ,v_y ~*> v__2 ,v_y ~*> 0.0.0 ,v_y ~*> 0.0.1 ,v_y ~*> tick ,K ~*> v_5 ,K ~*> v__0 ,K ~*> v__01 ,K ~*> v__1 ,K ~*> v__2 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,v_x ~^> v__01 ,v_x ~^> v__1 ,v_x ~^> v__2 ,v_x ~^> 0.0.0 ,v_x ~^> 0.0.1 ,v_x ~^> tick] + eval_counterex1b_bb4_in.21> [v_5 ~=> v__0 ,v__0 ~=> 0.0 ,v__01 ~=> v__1 ,v__01 ~=> v__2 ,v__01 ~=> 0.0.1 ,v__2 ~=> v__01 ,v__2 ~=> v__1 ,v__2 ~=> 0.0.1 ,huge ~=> v_2 ,huge ~=> v_7 ,v_5 ~+> v_5 ,v_5 ~+> v__0 ,v__0 ~+> v_5 ,v__0 ~+> v__0 ,v__0 ~+> tick ,v__01 ~+> v__01 ,v__01 ~+> v__1 ,v__01 ~+> v__2 ,v__01 ~+> 0.0.0 ,v__01 ~+> 0.0.1 ,v__01 ~+> tick ,v__2 ~+> v__01 ,v__2 ~+> v__1 ,v__2 ~+> v__2 ,v__2 ~+> 0.0.0 ,v__2 ~+> 0.0.1 ,v__2 ~+> tick ,v_n ~+> 0.0.0 ,v_n ~+> tick ,tick ~+> tick ,K ~+> v_5 ,K ~+> v__0 ,K ~+> v__01 ,K ~+> v__1 ,K ~+> v__2 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,v__0 ~*> v_5 ,v__0 ~*> v__0 ,v__0 ~*> v__01 ,v__0 ~*> v__1 ,v__0 ~*> v__2 ,v__0 ~*> 0.0.0 ,v__0 ~*> 0.0.1 ,v__0 ~*> tick ,v__01 ~*> v__01 ,v__01 ~*> v__1 ,v__01 ~*> v__2 ,v__01 ~*> 0.0.0 ,v__01 ~*> 0.0.1 ,v__01 ~*> tick ,v__2 ~*> v__01 ,v__2 ~*> v__1 ,v__2 ~*> v__2 ,v__2 ~*> 0.0.0 ,v__2 ~*> 0.0.1 ,v__2 ~*> tick ,v_n ~*> v__01 ,v_n ~*> v__1 ,v_n ~*> v__2 ,v_n ~*> 0.0.0 ,v_n ~*> 0.0.1 ,v_n ~*> tick ,K ~*> v_5 ,K ~*> v__0 ,K ~*> v__01 ,K ~*> v__1 ,K ~*> v__2 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,v__0 ~^> v__01 ,v__0 ~^> v__1 ,v__0 ~^> v__2 ,v__0 ~^> 0.0.0 ,v__0 ~^> 0.0.1 ,v__0 ~^> tick] eval_counterex1b_14.25> [v_5 ~=> v__0 ,v__0 ~=> 0.0 ,v__01 ~=> v__1 ,v__01 ~=> v__2 ,v__01 ~=> 0.0.1 ,v__2 ~=> v__01 ,v__2 ~=> v__1 ,v__2 ~=> 0.0.1 ,huge ~=> v_2 ,huge ~=> v_7 ,v_5 ~+> v_5 ,v_5 ~+> v__0 ,v__0 ~+> v_5 ,v__0 ~+> v__0 ,v__0 ~+> tick ,v__01 ~+> v__01 ,v__01 ~+> v__1 ,v__01 ~+> v__2 ,v__01 ~+> 0.0.0 ,v__01 ~+> 0.0.1 ,v__01 ~+> tick ,v__2 ~+> v__01 ,v__2 ~+> v__1 ,v__2 ~+> v__2 ,v__2 ~+> 0.0.0 ,v__2 ~+> 0.0.1 ,v__2 ~+> tick ,v_n ~+> 0.0.0 ,v_n ~+> tick ,tick ~+> tick ,K ~+> v_5 ,K ~+> v__0 ,K ~+> v__01 ,K ~+> v__1 ,K ~+> v__2 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,v__0 ~*> v_5 ,v__0 ~*> v__0 ,v__0 ~*> v__01 ,v__0 ~*> v__1 ,v__0 ~*> v__2 ,v__0 ~*> 0.0.0 ,v__0 ~*> 0.0.1 ,v__0 ~*> tick ,v__01 ~*> v__01 ,v__01 ~*> v__1 ,v__01 ~*> v__2 ,v__01 ~*> 0.0.0 ,v__01 ~*> 0.0.1 ,v__01 ~*> tick ,v__2 ~*> v__01 ,v__2 ~*> v__1 ,v__2 ~*> v__2 ,v__2 ~*> 0.0.0 ,v__2 ~*> 0.0.1 ,v__2 ~*> tick ,v_n ~*> v__01 ,v_n ~*> v__1 ,v_n ~*> v__2 ,v_n ~*> 0.0.0 ,v_n ~*> 0.0.1 ,v_n ~*> tick ,K ~*> v_5 ,K ~*> v__0 ,K ~*> v__01 ,K ~*> v__1 ,K ~*> v__2 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,v__0 ~^> v__01 ,v__0 ~^> v__1 ,v__0 ~^> v__2 ,v__0 ~^> 0.0.0 ,v__0 ~^> 0.0.1 ,v__0 ~^> tick] + eval_counterex1b_bb6_in.26> [huge ~=> v_7 ,v__2 ~+> v__2 ,v__2 ~+> 0.0.0 ,v__2 ~+> tick ,v_n ~+> 0.0.0 ,v_n ~+> tick ,tick ~+> tick ,K ~+> v__2 ,v__2 ~*> v__2 ,v_n ~*> v__2 ,K ~*> v__2] eval_counterex1b_13.23> [huge ~=> v_7 ,v__2 ~+> v__2 ,v__2 ~+> 0.0.0 ,v__2 ~+> tick ,v_n ~+> 0.0.0 ,v_n ~+> tick ,tick ~+> tick ,K ~+> v__2 ,v__2 ~*> v__2 ,v_n ~*> v__2 ,K ~*> v__2] + eval_counterex1b_bb3_in.15> [v__1 ~=> 0.0.1 ,huge ~=> v_2 ,v__1 ~+> v__1 ,v__1 ~+> tick ,tick ~+> tick ,K ~+> v__1 ,v__1 ~*> v__1 ,K ~*> v__1] eval_counterex1b_5.12> [v__1 ~=> 0.0.1 ,huge ~=> v_2 ,v__1 ~+> v__1 ,v__1 ~+> tick ,tick ~+> tick ,K ~+> v__1 ,v__1 ~*> v__1 ,K ~*> v__1] YES(?,PRIMREC)