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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) Signature: {(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,27,28,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25} ,7->{8,24},8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15 ,17},16->{6,26},17->{6,26},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18},23->{0,1 ,12},24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26}] + 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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (1,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,27,28,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25} ,7->{8,24},8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15 ,17},16->{6,26},17->{6,26},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18},23->{0,1 ,12},24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,27),(3,28),(16,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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (1,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (1,1) Signature: {(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25},7->{8,24} ,8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15,17} ,16->{26},17->{6,26},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18},23->{0,1,12} ,24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26}] + 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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 31. f23(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) ;(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,27,28,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25} ,7->{8,24},8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15 ,17},16->{6,26,31},17->{6,26,31},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18} ,23->{0,1,12},24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26,31},31->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,27),(3,28),(16,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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 31. f23(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) ;(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25},7->{8,24} ,8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15,17} ,16->{26,31},17->{6,26,31},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18},23->{0,1 ,12},24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26,31},31->{}] + 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,31] | +- p:[3,27,4,5,28,29] c: [4] | | | `- p:[3,27,5,28,29] c: [5] | | | `- p:[3,29] c: [3] | `- p:[0,18,11,21,19,9,20,10,25,6,17,13,1,23,12,14,15,24,7,8,22] c: [13] | `- p:[0,18,11,21,19,9,20,10,25,6,17,14,1,23,12,15,24,7,8,22] c: [25] | +- p:[9,19,10,20] c: [10] | | | `- p:[9,19,20] c: [9] | +- p:[11] c: [11] | +- p:[15] c: [15] | `- p:[7,24,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) [L >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,B,C,D,E,F,G,H,I,J,K) True (1,1) 3. f5(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,0,D,E,F,G,H,I,J,K) [A >= B] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,C,1 + D,L,L,G,H,I,J,K) [C >= L && A >= D] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K) -> f9(A,B,L,1 + D,L,L,G,H,I,J,K) [L >= 1 + C && A >= D] (?,1) 6. f23(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,B,C,D,E,F,G,H,I,J,K) [A >= D] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,H,I,J,K) [D >= 1 + B] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K) -> f30(A,B,C,D,E,F,L,1 + H,I,J,K) [B >= 1 + H] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f44(A,B,C,D,E,F,L,H,I,J,K) [A >= B] (?,1) 10. f44(A,B,C,D,E,F,G,H,I,J,K) -> f44(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. 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) 13. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [A >= 1 + D] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,B,C,D,E,F,G,H,L,J,K) [D >= 1 + A] (?,1) 15. f74(A,B,C,D,E,F,G,H,I,J,K) -> f74(A,1 + B,C,D,E,F,G,H,I,J,K) [A >= B] (?,1) 16. f71(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + A,E,F,G,H,I,J,K) [A = D] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,1 + D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 18. 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) 19. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,C,D,E,F,G,H,M,L,K) [C >= 1 + M && H >= D] (?,1) 20. f44(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,1 + B,L,D,E,F,G,H,L,M,B) [L >= C && H >= D] (?,1) 21. f40(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) 22. f40(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) 23. f40(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) 24. f30(A,B,C,D,E,F,G,H,I,J,K) -> f26(A,1 + B,C,D,E,F,G,H,I,J,K) [H >= B] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,0,D,E,F,G,H,I,J,K) [B >= D] (?,1) 26. f23(A,B,C,D,E,F,G,H,I,J,K) -> f1(A,B,C,D,E,F,G,H,I,J,K) [D >= 1 + A] (?,1) 27. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [0 >= 1 + C && D >= 1 + A] (?,1) 28. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K) [C >= 1 && D >= 1 + A] (?,1) 29. f9(A,B,C,D,E,F,G,H,I,J,K) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K) [D >= 1 + A && C = 0] (?,1) 30. f5(A,B,C,D,E,F,G,H,I,J,K) -> f23(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 31. f23(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) ;(f1,11) ;(f2,11) ;(f23,11) ;(f26,11) ;(f30,11) ;(f40,11) ;(f44,11) ;(f5,11) ;(f59,11) ;(f69,11) ;(f71,11) ;(f74,11) ;(f9,11)} Flow Graph: [0->{13,14,16},1->{13,14,16},2->{3,30},3->{4,5,29},4->{4,5,27,28,29},5->{4,5,27,28,29},6->{7,25},7->{8,24} ,8->{8,24},9->{10,19,20},10->{10,19,20},11->{11,18},12->{13,14,16},13->{15,17},14->{15,17},15->{15,17} ,16->{26,31},17->{6,26,31},18->{0,1,12},19->{9,21,22,23},20->{9,21,22,23},21->{11,18},22->{11,18},23->{0,1 ,12},24->{7,25},25->{9,21,22,23},26->{},27->{3,30},28->{3,30},29->{3,30},30->{6,26,31},31->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31] | +- p:[3,27,4,5,28,29] c: [4] | | | `- p:[3,27,5,28,29] c: [5] | | | `- p:[3,29] c: [3] | `- p:[0,18,11,21,19,9,20,10,25,6,17,13,1,23,12,14,15,24,7,8,22] c: [13] | `- p:[0,18,11,21,19,9,20,10,25,6,17,14,1,23,12,15,24,7,8,22] c: [25] | +- p:[9,19,10,20] c: [10] | | | `- p:[9,19,20] c: [9] | +- p:[11] c: [11] | +- p:[15] c: [15] | `- p:[7,24,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] f2 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f9 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f9 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f23 ~> f26 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f26 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f30 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, J <= J, K <= K] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f44 ~> f44 [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] f69 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f74 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f71 ~> f74 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f74 ~> f74 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f23 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f74 ~> f23 [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] f44 ~> f40 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f40 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= D] f30 ~> f26 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f26 ~> f40 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f23 ~> f1 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f5 ~> f23 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f23 ~> 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] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f9 [A <= A, B <= B, C <= C, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f9 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [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] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f9 [A <= A, B <= B, C <= unknown, D <= K + D, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [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] f5 ~> f9 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f9 ~> f5 [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] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] f44 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + H, I <= I, J <= J, K <= K] f26 ~> f40 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f23 ~> f26 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f74 ~> f23 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f74 [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] f40 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 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] f71 ~> f74 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K] f74 ~> f74 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f26 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f26 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f30 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, J <= J, K <= K] f40 ~> 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] f40 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= B] f44 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + H, I <= I, J <= J, K <= K] f26 ~> f40 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f23 ~> f26 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f74 ~> f23 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f71 ~> f74 [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] f40 ~> f69 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 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] f74 ~> f74 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f26 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f26 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f30 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= B + H, I <= I, J <= J, K <= K] f40 ~> 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] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f44 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= D + H, I <= I, J <= J, K <= K] f44 ~> f40 [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] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f44 ~> f40 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= unknown, K <= K] f44 ~> f40 [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] f74 ~> f74 [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] f26 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= H, I <= I, J <= J, K <= K] f30 ~> f26 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K] f30 ~> f30 [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] f30 ~> f30 [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 [] f2 ~> f5 [] f5 ~> f9 [K ~=> C] f9 ~> f9 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f9 ~> f9 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f23 ~> f26 [] f26 ~> f30 [huge ~=> G] f30 ~> f30 [huge ~=> G,B ~+> H,H ~+> H] f40 ~> f44 [huge ~=> G] f44 ~> f44 [huge ~=> G,D ~+> H,H ~+> H] f59 ~> f59 [huge ~=> I,H ~+> H,K ~+> H] f69 ~> f71 [] f71 ~> f74 [huge ~=> I] f71 ~> f74 [huge ~=> I] f74 ~> f74 [B ~+> B,K ~+> B] f71 ~> f23 [D ~+> D,K ~+> D] f74 ~> f23 [D ~+> D,K ~+> D] f59 ~> f69 [] f44 ~> f40 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f44 ~> f40 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f40 ~> f59 [] f40 ~> f59 [] f40 ~> f69 [D ~=> K] f30 ~> f26 [B ~+> B,K ~+> B] f26 ~> f40 [K ~=> C] f23 ~> f1 [] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [K ~=> C,B ~+> B,K ~+> B] f5 ~> f23 [] f23 ~> exitus616 [] + Loop: [A ~+> 0.0,D ~+> 0.0,K ~+> 0.0] f5 ~> f9 [K ~=> C] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f9 [huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f9 ~> f9 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [K ~=> C,B ~+> B,K ~+> B] + Loop: [A ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] f5 ~> f9 [K ~=> C] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f9 [huge ~=> C,huge ~=> E,huge ~=> F,D ~+> D,K ~+> D] f9 ~> f5 [B ~+> B,K ~+> B] f9 ~> f5 [K ~=> C,B ~+> B,K ~+> B] + Loop: [A ~+> 0.0.0.0,B ~+> 0.0.0.0,K ~*> 0.0.0.0] f5 ~> f9 [K ~=> C] f9 ~> f5 [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] f40 ~> f59 [] f44 ~> f40 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f40 ~> f44 [huge ~=> G] f44 ~> f40 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f44 ~> f44 [huge ~=> G,D ~+> H,H ~+> H] f26 ~> f40 [K ~=> C] f23 ~> f26 [] f74 ~> f23 [D ~+> D,K ~+> D] f71 ~> f74 [huge ~=> I] f69 ~> f71 [] f40 ~> f69 [D ~=> K] f69 ~> f71 [] f71 ~> f74 [huge ~=> I] f74 ~> f74 [B ~+> B,K ~+> B] f30 ~> f26 [B ~+> B,K ~+> B] f26 ~> f30 [huge ~=> G] f30 ~> f30 [huge ~=> G,B ~+> H,H ~+> H] f40 ~> 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] f40 ~> f59 [] f44 ~> f40 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f40 ~> f44 [huge ~=> G] f44 ~> f40 [B ~=> K,huge ~=> C,huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f44 ~> f44 [huge ~=> G,D ~+> H,H ~+> H] f26 ~> f40 [K ~=> C] f23 ~> f26 [] f74 ~> f23 [D ~+> D,K ~+> D] f71 ~> f74 [huge ~=> I] f69 ~> f71 [] f40 ~> f69 [D ~=> K] f69 ~> f71 [] f74 ~> f74 [B ~+> B,K ~+> B] f30 ~> f26 [B ~+> B,K ~+> B] f26 ~> f30 [huge ~=> G] f30 ~> f30 [huge ~=> G,B ~+> H,H ~+> H] f40 ~> f59 [] + Loop: [D ~+> 0.1.0.0,H ~+> 0.1.0.0,K ~+> 0.1.0.0] f40 ~> f44 [huge ~=> G] f44 ~> f40 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f44 ~> f44 [huge ~=> G,D ~+> H,H ~+> H] f44 ~> f40 [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] f40 ~> f44 [huge ~=> G] f44 ~> f40 [huge ~=> I,huge ~=> J,B ~+> B,K ~+> B] f44 ~> f40 [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] f74 ~> f74 [B ~+> B,K ~+> B] + Loop: [B ~+> 0.1.0.3,D ~+> 0.1.0.3,K ~*> 0.1.0.3] f26 ~> f30 [huge ~=> G] f30 ~> f26 [B ~+> B,K ~+> B] f30 ~> f30 [huge ~=> G,B ~+> H,H ~+> H] + Loop: [B ~+> 0.1.0.3.0,H ~+> 0.1.0.3.0] f30 ~> f30 [huge ~=> G,B ~+> H,H ~+> H] + Applied Processor: LareProcessor + Details: f2 ~> f1 [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] f2 ~> 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] + f5> [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] + f9> [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] f5> [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] f9> [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] f5> [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] + f9> [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] f5> [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] f9> [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] f5> [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] f23> [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] f23> [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] + f40> [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] + f44> [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] f40> [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] f44> [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] f40> [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] + f74> [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] + f26> [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] + f30> [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)