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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,26,27,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24} ,7->{8,23},8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{6,25} ,16->{6,25},17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24},24->{9 ,20,21,22},25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25}] + 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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (1,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,26,27,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24} ,7->{8,23},8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{6,25} ,16->{6,25},17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24},24->{9 ,20,21,22},25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,26),(3,27),(15,6)] * 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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (1,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24},7->{8,23} ,8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{25},16->{6,25} ,17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24},24->{9,20,21,22} ,25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25}] + 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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) 30. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,26,27,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24} ,7->{8,23},8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{6,25 ,30},16->{6,25,30},17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24} ,24->{9,20,21,22},25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25,30},30->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,26),(3,27),(15,6)] * 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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) 30. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24},7->{8,23} ,8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{25,30},16->{6 ,25,30},17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24},24->{9,20 ,21,22},25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25,30},30->{}] + 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,22,23,24,25,26,27,28,29,30] | +- p:[3,26,4,5,27,28] c: [4] | | | `- p:[3,26,5,27,28] c: [5] | | | `- p:[3,28] c: [3] | `- p:[0,17,11,20,18,9,19,10,24,6,16,12,1,22,13,14,23,7,8,21] c: [12] | `- p:[0,17,11,20,18,9,19,10,24,6,16,13,1,22,14,23,7,8,21] c: [24] | +- p:[9,18,10,19] c: [10] | | | `- p:[9,18,19] c: [9] | +- p:[11] c: [11] | +- p:[14] c: [14] | `- p:[7,23,8] c: [7] | `- p:[8] c: [8] * 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) [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) True (?,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) [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) [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) [A >= D] (?,1) 7. f30(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K) -> f33(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f45(A,B,C,D,E,F,G,H,I,J,K) -> f45(A,B,C,D,E,F,L,1 + H,I,J,K) [D >= 1 + H] (?,1) 11. 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) [A >= H] (?,1) 12. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 14. f73(A,B,C,D,E,F,G,H,I,J,K) -> f73(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 15. 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) [A = D] (?,1) 16. 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) [B >= 1 + A] (?,1) 17. f59(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [H >= 1 + A] (?,1) 18. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 19. f45(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 20. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && K >= 1 + D] (?,1) 21. f42(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A && D >= 1 + K] (?,1) 22. f42(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,D) [B >= 1 + A && D = K] (?,1) 23. f33(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f42(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 25. f28(A,B,C,D,E,F,G,H,I,J,K) -> f82(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 26. 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) [0 >= 1 + C && D >= 1 + A] (?,1) 27. 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) [C >= 1 && D >= 1 + A] (?,1) 28. 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) [D >= 1 + A && C = 0] (?,1) 29. 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) 30. 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) ;(f33,11) ;(f42,11) ;(f45,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f73,11) ;(f82,11)} Flow Graph: [0->{12,13,15},1->{12,13,15},2->{3,29},3->{4,5,28},4->{4,5,26,27,28},5->{4,5,26,27,28},6->{7,24},7->{8,23} ,8->{8,23},9->{10,18,19},10->{10,18,19},11->{11,17},12->{14,16},13->{14,16},14->{14,16},15->{25,30},16->{6 ,25,30},17->{0,1},18->{9,20,21,22},19->{9,20,21,22},20->{11,17},21->{11,17},22->{0,1},23->{7,24},24->{9,20 ,21,22},25->{},26->{3,29},27->{3,29},28->{3,29},29->{6,25,30},30->{}] ,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] | +- p:[3,26,4,5,27,28] c: [4] | | | `- p:[3,26,5,27,28] c: [5] | | | `- p:[3,28] c: [3] | `- p:[0,17,11,20,18,9,19,10,24,6,16,12,1,22,13,14,23,7,8,21] c: [12] | `- p:[0,17,11,20,18,9,19,10,24,6,16,13,1,22,14,23,7,8,21] c: [24] | +- p:[9,18,10,19] c: [10] | | | `- p:[9,18,19] c: [9] | +- p:[11] c: [11] | +- p:[14] c: [14] | `- p:[7,23,8] c: [7] | `- p:[8] c: [8]) + 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.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.1 ,0.1.0.2 ,0.1.0.3 ,0.1.0.3.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] f30 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, J <= J, K <= K] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + 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 ~> f73 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f73 ~> f73 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f28 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f73 ~> f28 [A <= A, B <= B, C <= C, D <= K + 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] f45 ~> f42 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] 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] f33 ~> f30 [A <= A, B <= K + 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 ~> 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 + D] 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 + D] 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 <= 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.0 <= 2*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 <= 0*K, D <= D, E <= E, F <= F, 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] f45 ~> f42 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + 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 <= K + 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] f71 ~> f73 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f73 ~> f73 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f33 ~> f30 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + 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] + Loop: [0.1.0 <= 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] f45 ~> f42 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + 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 <= K + 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] f73 ~> f73 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f33 ~> f30 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + 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] + Loop: [0.1.0.0 <= K + D + H] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + H, I <= I, J <= J, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] + Loop: [0.1.0.0.0 <= 2*K + A + B] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f45 ~> f42 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] + Loop: [0.1.0.1 <= 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] + Loop: [0.1.0.2 <= K + A + B] f73 ~> f73 [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.1.0.3 <= 2*K + B + D] f30 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f33 ~> f30 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, J <= J, K <= K] + Loop: [0.1.0.3.0 <= B + H] f33 ~> f33 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, 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.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.1 ,0.1.0.2 ,0.1.0.3 ,0.1.0.3.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 [] f30 ~> f33 [huge ~=> G] f33 ~> f33 [huge ~=> G,B ~+> H,H ~+> H] f42 ~> f45 [huge ~=> G] f45 ~> f45 [huge ~=> G,D ~+> H,H ~+> H] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f71 ~> f73 [huge ~=> I] f71 ~> f73 [huge ~=> I] f73 ~> f73 [B ~+> B,K ~+> B] f71 ~> f28 [D ~+> D,K ~+> D] f73 ~> f28 [D ~+> D,K ~+> D] f59 ~> f69 [] f45 ~> f42 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f45 ~> f42 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f42 ~> f59 [] f42 ~> f59 [] f42 ~> f69 [D ~=> K] f33 ~> f30 [B ~+> B,K ~+> B] 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,D ~+> 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,D ~+> 0.0.0,K ~+> 0.0.0] f12 ~> f15 [K ~=> C] f15 ~> f12 [B ~+> B,K ~+> B] 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.0,B ~+> 0.0.0.0,K ~*> 0.0.0.0] f12 ~> f15 [K ~=> C] f15 ~> f12 [K ~=> C,B ~+> B,K ~+> B] + Loop: [A ~+> 0.1,D ~+> 0.1,K ~+> 0.1] f69 ~> f71 [] f59 ~> f69 [] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f42 ~> f59 [] f45 ~> f42 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f42 ~> f45 [huge ~=> G] f45 ~> f42 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f45 ~> f45 [huge ~=> G,D ~+> H,H ~+> H] f30 ~> f42 [K ~=> C] f28 ~> f30 [] f73 ~> f28 [D ~+> D,K ~+> D] f71 ~> f73 [huge ~=> I] f69 ~> f71 [] f42 ~> f69 [D ~=> K] f71 ~> f73 [huge ~=> I] f73 ~> f73 [B ~+> B,K ~+> B] f33 ~> f30 [B ~+> B,K ~+> B] f30 ~> f33 [huge ~=> G] f33 ~> f33 [huge ~=> G,B ~+> H,H ~+> H] f42 ~> f59 [] + Loop: [A ~+> 0.1.0,D ~+> 0.1.0,K ~+> 0.1.0] f69 ~> f71 [] f59 ~> f69 [] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f42 ~> f59 [] f45 ~> f42 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f42 ~> f45 [huge ~=> G] f45 ~> f42 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f45 ~> f45 [huge ~=> G,D ~+> H,H ~+> H] f30 ~> f42 [K ~=> C] f28 ~> f30 [] f73 ~> f28 [D ~+> D,K ~+> D] f71 ~> f73 [huge ~=> I] f69 ~> f71 [] f42 ~> f69 [D ~=> K] f73 ~> f73 [B ~+> B,K ~+> B] f33 ~> f30 [B ~+> B,K ~+> B] f30 ~> f33 [huge ~=> G] f33 ~> f33 [huge ~=> G,B ~+> H,H ~+> H] f42 ~> f59 [] + Loop: [D ~+> 0.1.0.0,H ~+> 0.1.0.0,K ~+> 0.1.0.0] f42 ~> f45 [huge ~=> G] f45 ~> f42 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f45 ~> f45 [huge ~=> G,D ~+> H,H ~+> H] f45 ~> f42 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] + Loop: [A ~+> 0.1.0.0.0,B ~+> 0.1.0.0.0,K ~*> 0.1.0.0.0] f42 ~> f45 [huge ~=> G] f45 ~> f42 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f45 ~> f42 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] + Loop: [A ~+> 0.1.0.1,H ~+> 0.1.0.1,K ~+> 0.1.0.1] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] + Loop: [A ~+> 0.1.0.2,B ~+> 0.1.0.2,K ~+> 0.1.0.2] f73 ~> f73 [B ~+> B,K ~+> B] + Loop: [B ~+> 0.1.0.3,D ~+> 0.1.0.3,K ~*> 0.1.0.3] f30 ~> f33 [huge ~=> G] f33 ~> f30 [B ~+> B,K ~+> B] f33 ~> f33 [huge ~=> G,B ~+> H,H ~+> H] + Loop: [B ~+> 0.1.0.3.0,H ~+> 0.1.0.3.0] f33 ~> f33 [huge ~=> G,B ~+> H,H ~+> H] + Applied Processor: LareProcessor + Details: f0 ~> f82 [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.0.0.0 ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> 0.1 ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.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.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.0.0.0 ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.0.0 ,D ~*> 0.0.0.0 ,D ~*> 0.1 ,D ~*> 0.1.0 ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.1.0 ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.0.0 ,D ~^> 0.0.0.0 ,D ~^> 0.1 ,D ~^> 0.1.0 ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.0 ,K ~^> tick] f0 ~> exitus616 [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.0.0.0 ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> 0.1 ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.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.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.0.0.0 ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.0.0 ,D ~*> 0.0.0.0 ,D ~*> 0.1 ,D ~*> 0.1.0 ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.1.0 ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.0.0 ,D ~^> 0.0.0.0 ,D ~^> 0.1 ,D ~^> 0.1.0 ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.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 ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> 0.0.0 ,D ~*> 0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> D ,D ~^> 0.0.0 ,D ~^> 0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> D ,K ~^> 0.0.0 ,K ~^> 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 ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> 0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> 0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> 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 ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> 0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> 0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> 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 ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> 0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> 0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> 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 ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> 0.0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> 0.0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> 0.0.0.0 ,K ~^> tick] + f15> [K ~=> C ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B ,K ~*> 0.0.0.0 ,K ~*> tick] f12> [K ~=> C ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B ,K ~*> 0.0.0.0 ,K ~*> tick] f15> [K ~=> C ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B ,K ~*> 0.0.0.0 ,K ~*> tick] f12> [K ~=> C ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B ,K ~*> 0.0.0.0 ,K ~*> tick] + f71> [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.1 ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1.0 ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1.0 ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.1.0 ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.1.0 ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.0 ,K ~^> tick] f28> [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.1 ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1.0 ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1.0 ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> D ,A ~^> H ,A ~^> K ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> D ,D ~^> H ,D ~^> K ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> D ,K ~^> H ,K ~^> K ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.0 ,K ~^> tick] + f71> [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> H ,A ~^> K ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> H ,D ~^> K ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> H ,K ~^> K ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.0 ,K ~^> tick] f28> [B ~=> K ,D ~=> K ,K ~=> C ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0 ,A ~+> 0.1.0.0.0 ,A ~+> 0.1.0.1 ,A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> H ,B ~+> K ,B ~+> 0.1.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.1 ,B ~+> 0.1.0.2 ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> D ,D ~+> H ,D ~+> K ,D ~+> 0.1.0 ,D ~+> 0.1.0.0 ,D ~+> 0.1.0.1 ,D ~+> 0.1.0.3 ,D ~+> 0.1.0.3.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> 0.1.0.1 ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> H ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.1 ,K ~+> 0.1.0.2 ,K ~+> 0.1.0.3 ,K ~+> 0.1.0.3.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> H ,A ~*> K ,A ~*> 0.1.0.0 ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.1 ,A ~*> 0.1.0.2 ,A ~*> 0.1.0.3 ,A ~*> 0.1.0.3.0 ,A ~*> tick ,B ~*> B ,B ~*> H ,B ~*> K ,B ~*> 0.1.0.0 ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.1 ,B ~*> 0.1.0.2 ,B ~*> 0.1.0.3 ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> H ,D ~*> K ,D ~*> 0.1.0.0 ,D ~*> 0.1.0.0.0 ,D ~*> 0.1.0.1 ,D ~*> 0.1.0.2 ,D ~*> 0.1.0.3 ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0 ,H ~*> 0.1.0.0.0 ,H ~*> 0.1.0.1 ,H ~*> 0.1.0.2 ,H ~*> 0.1.0.3 ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> H ,K ~*> K ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.1 ,K ~*> 0.1.0.2 ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,A ~^> B ,A ~^> H ,A ~^> K ,A ~^> 0.1.0.0 ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.1 ,A ~^> 0.1.0.2 ,A ~^> 0.1.0.3 ,A ~^> 0.1.0.3.0 ,A ~^> tick ,B ~^> B ,B ~^> H ,B ~^> K ,B ~^> 0.1.0.0 ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.1 ,B ~^> 0.1.0.2 ,B ~^> 0.1.0.3 ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> B ,D ~^> H ,D ~^> K ,D ~^> 0.1.0.0 ,D ~^> 0.1.0.0.0 ,D ~^> 0.1.0.1 ,D ~^> 0.1.0.2 ,D ~^> 0.1.0.3 ,D ~^> 0.1.0.3.0 ,D ~^> tick ,H ~^> B ,H ~^> H ,H ~^> K ,H ~^> 0.1.0.0 ,H ~^> 0.1.0.0.0 ,H ~^> 0.1.0.1 ,H ~^> 0.1.0.2 ,H ~^> 0.1.0.3 ,H ~^> 0.1.0.3.0 ,H ~^> tick ,K ~^> B ,K ~^> H ,K ~^> K ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.1 ,K ~^> 0.1.0.2 ,K ~^> 0.1.0.3 ,K ~^> 0.1.0.3.0 ,K ~^> tick] + f42> [B ~=> K ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> tick ,D ~+> H ,D ~+> 0.1.0.0 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> 0.1.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> 0.1.0.0.0 ,B ~*> tick ,D ~*> B ,D ~*> H ,D ~*> K ,D ~*> 0.1.0.0.0 ,D ~*> tick ,H ~*> B ,H ~*> H ,H ~*> K ,H ~*> 0.1.0.0.0 ,H ~*> tick ,K ~*> B ,K ~*> H ,K ~*> K ,K ~*> 0.1.0.0.0 ,K ~*> tick ,D ~^> B ,D ~^> K ,D ~^> 0.1.0.0.0 ,D ~^> tick ,H ~^> B ,H ~^> K ,H ~^> 0.1.0.0.0 ,H ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f45> [B ~=> K ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> K ,A ~*> B ,B ~*> B ,K ~*> B ,K ~*> 0.1.0.0.0 ,K ~*> tick] f42> [B ~=> K ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> K ,A ~*> B ,A ~*> K ,B ~*> B ,B ~*> K ,K ~*> B ,K ~*> K ,K ~*> 0.1.0.0.0 ,K ~*> tick] f45> [B ~=> K ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> K ,A ~*> B ,A ~*> K ,B ~*> B ,B ~*> K ,K ~*> B ,K ~*> K ,K ~*> 0.1.0.0.0 ,K ~*> tick] f42> [B ~=> K ,huge ~=> C ,huge ~=> G ,huge ~=> I ,huge ~=> J ,A ~+> 0.1.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> K ,A ~*> B ,A ~*> K ,B ~*> B ,B ~*> K ,K ~*> B ,K ~*> K ,K ~*> 0.1.0.0.0 ,K ~*> tick] + f59> [huge ~=> I ,A ~+> 0.1.0.1 ,A ~+> tick ,H ~+> H ,H ~+> 0.1.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,K ~+> 0.1.0.1 ,K ~+> tick ,A ~*> H ,H ~*> H ,K ~*> H] + f73> [A ~+> 0.1.0.2 ,A ~+> tick ,B ~+> B ,B ~+> 0.1.0.2 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.1.0.2 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] + f30> [huge ~=> G ,B ~+> B ,B ~+> H ,B ~+> 0.1.0.3 ,B ~+> 0.1.0.3.0 ,B ~+> tick ,D ~+> 0.1.0.3 ,D ~+> tick ,H ~+> H ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> H ,K ~+> 0.1.0.3.0 ,K ~+> tick ,B ~*> B ,B ~*> H ,B ~*> 0.1.0.3.0 ,B ~*> tick ,D ~*> B ,D ~*> H ,D ~*> 0.1.0.3.0 ,D ~*> tick ,H ~*> H ,H ~*> 0.1.0.3.0 ,H ~*> tick ,K ~*> B ,K ~*> H ,K ~*> 0.1.0.3 ,K ~*> 0.1.0.3.0 ,K ~*> tick ,B ~^> H ,B ~^> 0.1.0.3.0 ,B ~^> tick ,D ~^> H ,D ~^> 0.1.0.3.0 ,D ~^> tick ,K ~^> H ,K ~^> 0.1.0.3.0 ,K ~^> tick] + f33> [huge ~=> G ,B ~+> H ,B ~+> 0.1.0.3.0 ,B ~+> tick ,H ~+> H ,H ~+> 0.1.0.3.0 ,H ~+> tick ,tick ~+> tick ,B ~*> H ,H ~*> H] YES(?,PRIMREC)