YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) Signature: {(f0,11);(f12,11);(f15,11);(f28,11);(f30,11);(f42,11);(f59,11);(f69,11);(f71,11);(f73,11);(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,17,18,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11} ,8->{10},9->{6,16},10->{6,16},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3,20} ,18->{3,20},19->{3,20},20->{6,16}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f0,11);(f12,11);(f15,11);(f28,11);(f30,11);(f42,11);(f59,11);(f69,11);(f71,11);(f73,11);(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,17,18,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11} ,8->{10},9->{6,16},10->{6,16},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3,20} ,18->{3,20},19->{3,20},20->{6,16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,17),(3,18),(9,6),(10,16)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (1,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f0,11);(f12,11);(f15,11);(f28,11);(f30,11);(f42,11);(f59,11);(f69,11);(f71,11);(f73,11);(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11},8->{10} ,9->{16},10->{6},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3,20},18->{3,20} ,19->{3,20},20->{6,16}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True (?,1) Signature: {(exitus616,11) ;(f0,11) ;(f12,11) ;(f15,11) ;(f28,11) ;(f30,11) ;(f42,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,17,18,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11} ,8->{10},9->{6,16,21},10->{6,16,21},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3 ,20},18->{3,20},19->{3,20},20->{6,16,21},21->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,17),(3,18),(9,6),(10,16)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True (?,1) Signature: {(exitus616,11) ;(f0,11) ;(f12,11) ;(f15,11) ;(f28,11) ;(f30,11) ;(f42,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11},8->{10} ,9->{16,21},10->{6,21},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3,20},18->{3,20} ,19->{3,20},20->{6,16,21},21->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[3,17,4,5,18,19] c: [19] | | | `- p:[3,17,4,5,18] c: [18] | | | `- p:[3,17,4,5] c: [17] | | | `- p:[4,5] c: [5] | | | `- p:[4] c: [4] | `- p:[0,11,7,12,15,6,10,8,1,14,13] c: [15] | `- p:[7] c: [7] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + L] (?,1) 1. f69(A,B,C,D,E,F,G,H,I,J,K) -> f71(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f12(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,C,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && C >= L && A >= D] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K) -> f15(A,B,L,1 + D,L,L,G,H,I,J,K) [A + -1*B >= 0 && L >= 1 + C && A >= D] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && A >= D] (?,1) 7. f59(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,1 + H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= H] (?,1) 8. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A >= 1 + D] (?,1) 9. f71(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + A,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && A = D] (?,1) 10. f73(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,1 + D,E,F,G,H,I,J,K) [-2 + B + -1*D >= 0 && -1 + A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 11. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && H >= 1 + A] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && K >= 1 + D] 13. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 (?,1) && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D >= 1 + K] 14. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A && D = K] (?,1) 15. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [-1 + B + -1*D >= 0 && A + -1*D >= 0 && -1 + -1*A + B >= 0 && B >= D] (?,1) 16. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [-1 + -1*A + B >= 0 && D >= 1 + A] (?,1) 17. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && 0 >= 1 + C && D >= 1 + A] (?,1) 18. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,C,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && C >= 1 && D >= 1 + A] (?,1) 19. f15(A,B,C,D,E,F,G,H,I,J,K) -> f12(A,1 + B,0,D,E,F,G,H,I,J,K) [A + -1*B >= 0 && D >= 1 + A && C = 0] (?,1) 20. f12(A,B,C,D,E,F,G,H,I,J,K) -> f28(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True (?,1) Signature: {(exitus616,11) ;(f0,11) ;(f12,11) ;(f15,11) ;(f28,11) ;(f30,11) ;(f42,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{8,9},1->{8,9},2->{3,20},3->{4,5,19},4->{4,5,17,18,19},5->{4,5,17,18,19},6->{15},7->{7,11},8->{10} ,9->{16,21},10->{6,21},11->{0,1},12->{7,11},13->{7,11},14->{0,1},15->{12,13,14},16->{},17->{3,20},18->{3,20} ,19->{3,20},20->{6,16,21},21->{}] ,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] | +- p:[3,17,4,5,18,19] c: [19] | | | `- p:[3,17,4,5,18] c: [18] | | | `- p:[3,17,4,5] c: [17] | | | `- p:[4,5] c: [5] | | | `- p:[4] c: [4] | `- p:[0,11,7,12,15,6,10,8,1,14,13] c: [15] | `- p:[7] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.1,0.1.0] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f0 ~> f12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f12 ~> f15 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f28 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K] f71 ~> f73 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f71 ~> f28 [A <= A, B <= B, C <= C, D <= B + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f73 ~> f28 [A <= A, B <= B, C <= C, D <= B + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f59 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f42 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f42 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f42 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= D] f30 ~> f42 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f28 ~> f82 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f12 ~> f28 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f28 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.0 <= K + A + B] f12 ~> f15 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.0.0 <= K + A + B] f12 ~> f15 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.0.0.0 <= K + A + B] f12 ~> f15 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f12 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.0.0.0.0 <= K + A + D] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f15 ~> f15 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.0.0.0.0.0 <= K + A + D] f15 ~> f15 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.1 <= K + A + D] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f59 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K] f42 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f42 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f28 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f73 ~> f28 [A <= A, B <= B, C <= C, D <= B + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f73 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f42 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= D] f42 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] + Loop: [0.1.0 <= K + A + H] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= unknown, J <= J, K <= K] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.1,0.1.0] f69 ~> f71 [] f69 ~> f71 [] f0 ~> f12 [] f12 ~> f15 [K ~=> C] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f15 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f28 ~> f30 [] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f71 ~> f73 [huge ~=> I] f71 ~> f28 [B ~+> D,D ~+> D] f73 ~> f28 [B ~+> D,D ~+> D] f59 ~> f69 [] f42 ~> f59 [] f42 ~> f59 [] f42 ~> f69 [D ~=> K] f30 ~> f42 [K ~=> C] f28 ~> f82 [] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f12 [K ~=> C,B ~+> B,K ~+> B] f12 ~> f28 [] f28 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f12 ~> f15 [K ~=> C] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f15 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f12 [K ~=> C,B ~+> B,K ~+> B] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] f12 ~> f15 [K ~=> C] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f15 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f12 [B ~+> B,K ~+> B] + Loop: [A ~+> 0.0.0.0,B ~+> 0.0.0.0,K ~+> 0.0.0.0] f12 ~> f15 [K ~=> C] f15 ~> f12 [B ~+> B,K ~+> B] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f15 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] + Loop: [A ~+> 0.0.0.0.0,D ~+> 0.0.0.0.0,K ~+> 0.0.0.0.0] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f15 ~> f15 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] + Loop: [A ~+> 0.0.0.0.0.0,D ~+> 0.0.0.0.0.0,K ~+> 0.0.0.0.0.0] f15 ~> f15 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] + Loop: [A ~+> 0.1,D ~+> 0.1,K ~+> 0.1] f69 ~> f71 [] f59 ~> f69 [] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f42 ~> f59 [] f30 ~> f42 [K ~=> C] f28 ~> f30 [] f73 ~> f28 [B ~+> D,D ~+> D] f71 ~> f73 [huge ~=> I] f69 ~> f71 [] f42 ~> f69 [D ~=> K] f42 ~> f59 [] + Loop: [A ~+> 0.1.0,H ~+> 0.1.0,K ~+> 0.1.0] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] + Applied Processor: LareProcessor + Details: f0 ~> f82 [D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,huge ~=> I ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> K ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> K ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> H ,B ~*> K ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.1 ,B ~*> 0.1.0 ,B ~*> tick ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> 0.1 ,D ~*> 0.1.0 ,D ~*> tick ,H ~*> H ,H ~*> 0.1.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.1.0 ,A ~^> tick ,B ~^> B ,B ~^> D ,B ~^> H ,B ~^> K ,B ~^> 0.0.0 ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> 0.1 ,B ~^> 0.1.0 ,B ~^> tick ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> 0.1 ,D ~^> 0.1.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.1.0 ,K ~^> tick] f0 ~> exitus616 [D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,huge ~=> I ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> K ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> K ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> H ,B ~*> K ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.1 ,B ~*> 0.1.0 ,B ~*> tick ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> 0.1 ,D ~*> 0.1.0 ,D ~*> tick ,H ~*> H ,H ~*> 0.1.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.1.0 ,A ~^> tick ,B ~^> B ,B ~^> D ,B ~^> H ,B ~^> K ,B ~^> 0.0.0 ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> 0.1 ,B ~^> 0.1.0 ,B ~^> tick ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> 0.1 ,D ~^> 0.1.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.1.0 ,K ~^> tick] + f12> [K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> tick ,B ~^> B ,B ~^> D ,B ~^> 0.0.0 ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> tick ,D ~^> D ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] + f15> [K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> tick ,B ~^> B ,B ~^> D ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> tick ,D ~^> D ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] f12> [K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> tick ,B ~^> B ,B ~^> D ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> tick ,D ~^> D ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] + f15> [K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> tick ,D ~^> D ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> tick ,K ~^> D ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] f12> [K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0.0 ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0.0.0 ,A ~^> 0.0.0.0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0.0.0 ,B ~^> 0.0.0.0.0.0 ,B ~^> tick ,D ~^> D ,D ~^> 0.0.0.0.0 ,D ~^> 0.0.0.0.0.0 ,D ~^> tick ,K ~^> D ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] + f15> [huge ~=> C ,huge ~=> E ,huge ~=> F ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> D ,A ~*> 0.0.0.0.0.0 ,A ~*> tick ,D ~*> D ,D ~*> 0.0.0.0.0.0 ,D ~*> tick ,K ~*> D ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,A ~^> D ,D ~^> D ,K ~^> D] + f15> [huge ~=> E ,huge ~=> F ,A ~+> 0.0.0.0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,K ~*> D] + f71> [D ~=> K ,K ~=> C ,huge ~=> I ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> D ,B ~+> K ,D ~+> D ,D ~+> K ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> D ,A ~*> H ,A ~*> 0.1.0 ,A ~*> tick ,B ~*> D ,B ~*> K ,D ~*> D ,D ~*> H ,D ~*> 0.1.0 ,D ~*> tick ,H ~*> H ,H ~*> 0.1.0 ,H ~*> tick ,K ~*> D ,K ~*> H ,K ~*> 0.1.0 ,K ~*> tick ,A ~^> H ,A ~^> 0.1.0 ,A ~^> tick ,D ~^> H ,D ~^> 0.1.0 ,D ~^> tick ,K ~^> H ,K ~^> 0.1.0 ,K ~^> tick] f28> [D ~=> K ,K ~=> C ,huge ~=> I ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> D ,B ~+> K ,D ~+> D ,D ~+> K ,D ~+> 0.1 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1.0 ,A ~*> tick ,B ~*> D ,B ~*> K ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1.0 ,D ~*> tick ,H ~*> H ,H ~*> 0.1.0 ,H ~*> tick ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1.0 ,K ~*> tick ,A ~^> H ,A ~^> 0.1.0 ,A ~^> tick ,D ~^> H ,D ~^> 0.1.0 ,D ~^> tick ,K ~^> H ,K ~^> 0.1.0 ,K ~^> tick] + f59> [huge ~=> I ,A ~+> 0.1.0 ,A ~+> tick ,H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> H ,H ~*> H ,K ~*> H] YES(?,PRIMREC)