YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,19,20,21},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10,11,12 ,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19,20,21} ,19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (1,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (1,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (1,1) Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,19,20,21},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10,11,12 ,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19,20,21} ,19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,19) ,(4,21) ,(11,9) ,(11,10) ,(11,12) ,(12,9) ,(12,10) ,(12,11) ,(12,13) ,(13,9) ,(13,10) ,(13,11) ,(13,13) ,(14,12) ,(15,11) ,(15,13) ,(16,11) ,(16,13) ,(23,5) ,(23,6) ,(23,7) ,(23,19) ,(23,21)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (1,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (1,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (1,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (1,1) Signature: {(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21},4->{5,6,7,20},5->{8,18},6->{8,18},7->{8,18},8->{9,10,11 ,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17},15->{9,10 ,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21},19->{},20->{},21->{},22->{1,23},23->{20}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) 24. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) Signature: {(exitus616,23);(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21,24},4->{5,6,7,19,20,21,24},5->{8,18},6->{8,18},7->{8,18} ,8->{9,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{9,10,11,12,13,17},12->{9,10,11,12,13,17},13->{9,10 ,11,12,13,17},14->{9,10,11,12,13,17},15->{9,10,11,12,13,17},16->{9,10,11,12,13,17},17->{8,18},18->{5,6,7,19 ,20,21,24},19->{},20->{},21->{},22->{1,23},23->{5,6,7,19,20,21,24},24->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,19) ,(4,21) ,(11,9) ,(11,10) ,(11,12) ,(12,9) ,(12,10) ,(12,11) ,(12,13) ,(13,9) ,(13,10) ,(13,11) ,(13,13) ,(14,12) ,(15,11) ,(15,13) ,(16,11) ,(16,13) ,(23,5) ,(23,6) ,(23,7) ,(23,19) ,(23,21)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) 24. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) Signature: {(exitus616,23);(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21,24},4->{5,6,7,20,24},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17} ,15->{9,10,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21,24},19->{},20->{},21->{},22->{1,23} ,23->{20,24},24->{}] + 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] | +- p:[5,18,6,7,17,8,11,14,9,15,10,16,12,13] c: [18] | | | `- p:[8,17,11,14,9,15,10,16,12,13] c: [8] | | | +- p:[9,14,10,15,16] c: [16] | | | | | `- p:[9,14,10,15] c: [15] | | | | | `- p:[9,14,10] c: [14] | | | +- p:[11] c: [11] | | | `- p:[12] c: [12] | `- p:[1,22,2] c: [22] | `- p:[2] c: [2] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(1,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A = 1] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && H >= I] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f18(A,B,C,D,E,F,G,H,I,J,1 + K,2 + L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && J >= K] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= A] (1,1) 4. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,X,Y,Z,A1,B1,C1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 2] (1,1) 5. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [0 >= I && H >= I] (?,1) 6. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,2 + H + -1*I,1,0,P,Q,R,S,T,U,V,W) [I >= 2 && H >= I] (?,1) 7. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,E,F,G,H,1,J,K,L,1,1,0,P,Q,R,S,T,U,V,W) [H >= 1 && I = 1] (?,1) 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && 1 + X >= Q] (?,1) 9. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 0 >= Q && J >= K] (?,1) 10. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && Q >= 2 && J >= K] (?,1) 11. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && 0 >= K && J >= K && Q = 1] (?,1) 12. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,X,M,N,O,P,1,Y,Z,A1,B1,V,W) [H + -1*I >= 0 && J >= K && K >= 2 && Q = 1] (?,1) 13. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,1,X,Y,Z,A1,V,W) [H + -1*I >= 0 && J >= 1 && K = 1 && Q = 1] (?,1) 14. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && 0 >= K] (?,1) 15. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,1 + K,2 + J + -1*K,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K >= 2] (?,1) 16. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,C,D,E,F,G,H,I,J,2,1,M,N,O,P,Q,X,Y,Z,A1,B1,W) [H + -1*I >= 0 && J + -1*K >= 0 && K = 1] (?,1) 17. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f35(A,B,C,D,N,F,G,H,I,J,K,L,M,X,Y,P,1 + Q,R,S,T,U,V,2 + W) [H + -1*I >= 0 && K >= 1 + J] (?,1) 18. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && P >= 2*X && 3*X >= 1 + P && Q >= 2 + X] (?,1) 19. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= 2 + A && I >= 1 + H] (?,1) 20. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= 0 && I >= 1 + H] (?,1) 21. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f76(-1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [I >= 1 + H && 1 + A = 0] (?,1) 22. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f16(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [H + -1*I >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && K >= 1 + J] (?,1) 23. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 + -1*A >= 0 && -1 + A >= 0 && I >= 1 + H] (?,1) 24. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) Signature: {(exitus616,23);(f0,23);(f16,23);(f18,23);(f28,23);(f35,23);(f37,23);(f52,23);(f76,23)} Flow Graph: [0->{1,23},1->{2,22},2->{2,22},3->{5,6,7,19,20,21,24},4->{5,6,7,20,24},5->{8,18},6->{8,18},7->{8,18},8->{9 ,10,11,12,13,17},9->{14,15,16},10->{14,15,16},11->{11,13,17},12->{12,17},13->{12,17},14->{9,10,11,13,17} ,15->{9,10,12,17},16->{9,10,12,17},17->{8,18},18->{5,6,7,19,20,21,24},19->{},20->{},21->{},22->{1,23} ,23->{20,24},24->{}] ,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] | +- p:[5,18,6,7,17,8,11,14,9,15,10,16,12,13] c: [18] | | | `- p:[8,17,11,14,9,15,10,16,12,13] c: [8] | | | +- p:[9,14,10,15,16] c: [16] | | | | | `- p:[9,14,10,15] c: [15] | | | | | `- p:[9,14,10] c: [14] | | | +- p:[11] c: [11] | | | `- p:[12] c: [12] | `- p:[1,22,2] c: [22] | `- p:[2] c: [2]) + 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 ,L ,M ,N ,O ,P ,Q ,R ,S ,T ,U ,V ,W ,0.0 ,0.0.0 ,0.0.0.0 ,0.0.0.0.0 ,0.0.0.0.0.0 ,0.0.0.1 ,0.0.0.2 ,0.1 ,0.1.0] f0 ~> f16 [A <= K, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f16 ~> f18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f18 ~> f18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f0 ~> f28 [A <= A, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f0 ~> f28 [A <= A, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= 2*K + H + I, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= H, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K, J <= J, K <= K, L <= L, M <= K, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f35 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= J, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= N, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= 2*K + W] f35 ~> f28 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K + I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f76 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f76 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f76 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f18 ~> f16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K + I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f16 ~> f28 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] + Loop: [0.0 <= K + H + I] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= 2*K + H + I, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f35 ~> f28 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K + I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= H, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f28 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K, J <= J, K <= K, L <= L, M <= K, N <= K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= N, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= 2*K + W] f35 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= J, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] + Loop: [0.0.0 <= 2*K + P + Q] f35 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f37 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= N, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= 2*K + W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= J, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] + Loop: [0.0.0.0 <= 2*K + K] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= J, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= 2*K, L <= K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] + Loop: [0.0.0.0.0 <= 2*J + K] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= J, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] + Loop: [0.0.0.0.0.0 <= K + K] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f52 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + J + K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= unknown, W <= W] f37 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] + Loop: [0.0.0.1 <= K + K] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] + Loop: [0.0.0.2 <= K + J + K] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= K, R <= unknown, S <= unknown, T <= unknown, U <= unknown, V <= V, W <= W] + Loop: [0.1 <= K + H + I] f16 ~> f18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f18 ~> f16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= K + I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] f18 ~> f18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] + Loop: [0.1.0 <= K + J + K] f18 ~> f18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K + K, L <= 2*K + L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W] + 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 ,L ,M ,N ,O ,P ,Q ,R ,S ,T ,U ,V ,W ,0.0 ,0.0.0 ,0.0.0.0 ,0.0.0.0.0 ,0.0.0.0.0.0 ,0.0.0.1 ,0.0.0.2 ,0.1 ,0.1.0] f0 ~> f16 [K ~=> A,huge ~=> B,huge ~=> C,huge ~=> D,huge ~=> E,huge ~=> F,huge ~=> G] f16 ~> f18 [] f18 ~> f18 [K ~+> K,L ~+> L,K ~+> K,K ~*> L] f0 ~> f28 [huge ~=> B,huge ~=> C,huge ~=> D,huge ~=> E,huge ~=> F,huge ~=> G] f0 ~> f28 [huge ~=> B,huge ~=> C,huge ~=> D,huge ~=> E,huge ~=> F,huge ~=> G] f28 ~> f35 [K ~=> N,K ~=> O,H ~+> M,I ~+> M,K ~*> M] f28 ~> f35 [H ~=> M,K ~=> N,K ~=> O] f28 ~> f35 [K ~=> I,K ~=> M,K ~=> N,K ~=> O] f35 ~> f37 [] f37 ~> f52 [] f37 ~> f52 [] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f37 ~> f37 [K ~=> K,K ~=> L,K ~=> Q,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f52 ~> f37 [J ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V,K ~+> K,K ~+> K] f52 ~> f37 [K ~=> K,K ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V] f37 ~> f35 [N ~=> E,huge ~=> N,huge ~=> O,Q ~+> Q,W ~+> W,K ~+> Q,K ~*> W] f35 ~> f28 [I ~+> I,K ~+> I] f28 ~> f76 [] f28 ~> f76 [] f28 ~> f76 [K ~=> A] f18 ~> f16 [I ~+> I,K ~+> I] f16 ~> f28 [] f28 ~> exitus616 [] + Loop: [H ~+> 0.0,I ~+> 0.0,K ~+> 0.0] f28 ~> f35 [K ~=> N,K ~=> O,H ~+> M,I ~+> M,K ~*> M] f35 ~> f28 [I ~+> I,K ~+> I] f28 ~> f35 [H ~=> M,K ~=> N,K ~=> O] f28 ~> f35 [K ~=> I,K ~=> M,K ~=> N,K ~=> O] f37 ~> f35 [N ~=> E,huge ~=> N,huge ~=> O,Q ~+> Q,W ~+> W,K ~+> Q,K ~*> W] f35 ~> f37 [] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f37 ~> f52 [] f52 ~> f37 [J ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V,K ~+> K,K ~+> K] f37 ~> f52 [] f52 ~> f37 [K ~=> K,K ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f37 ~> f37 [K ~=> K,K ~=> L,K ~=> Q,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U] + Loop: [P ~+> 0.0.0,Q ~+> 0.0.0,K ~*> 0.0.0] f35 ~> f37 [] f37 ~> f35 [N ~=> E,huge ~=> N,huge ~=> O,Q ~+> Q,W ~+> W,K ~+> Q,K ~*> W] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f37 ~> f52 [] f52 ~> f37 [J ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V,K ~+> K,K ~+> K] f37 ~> f52 [] f52 ~> f37 [K ~=> K,K ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] f37 ~> f37 [K ~=> K,K ~=> L,K ~=> Q,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U] + Loop: [K ~+> 0.0.0.0,K ~*> 0.0.0.0] f37 ~> f52 [] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f37 ~> f52 [] f52 ~> f37 [J ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V,K ~+> K,K ~+> K] f52 ~> f37 [K ~=> K,K ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V] + Loop: [K ~+> 0.0.0.0.0,J ~*> 0.0.0.0.0] f37 ~> f52 [] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f37 ~> f52 [] f52 ~> f37 [J ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,huge ~=> V,K ~+> K,K ~+> K] + Loop: [K ~+> 0.0.0.0.0.0,K ~+> 0.0.0.0.0.0] f37 ~> f52 [] f52 ~> f37 [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> K ,K ~*> L] f37 ~> f52 [] + Loop: [K ~+> 0.0.0.1,K ~+> 0.0.0.1] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] + Loop: [J ~+> 0.0.0.2,K ~+> 0.0.0.2,K ~+> 0.0.0.2] f37 ~> f37 [K ~=> Q,huge ~=> L,huge ~=> R,huge ~=> S,huge ~=> T,huge ~=> U,K ~+> K,K ~+> K] + Loop: [H ~+> 0.1,I ~+> 0.1,K ~+> 0.1] f16 ~> f18 [] f18 ~> f16 [I ~+> I,K ~+> I] f18 ~> f18 [K ~+> K,L ~+> L,K ~+> K,K ~*> L] + Loop: [J ~+> 0.1.0,K ~+> 0.1.0,K ~+> 0.1.0] f18 ~> f18 [K ~+> K,L ~+> L,K ~+> K,K ~*> L] + Applied Processor: LareProcessor + Details: f0 ~> f76 [H ~=> M ,J ~=> L ,K ~=> A ,K ~=> E ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> N ,K ~=> O ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> L ,huge ~=> N ,huge ~=> O ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,H ~+> M ,H ~+> 0.0 ,H ~+> 0.1 ,H ~+> tick ,I ~+> I ,I ~+> M ,I ~+> 0.0 ,I ~+> 0.1 ,I ~+> tick ,J ~+> L ,J ~+> 0.0.0.2 ,J ~+> 0.1.0 ,J ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> 0.1.0 ,K ~+> tick ,L ~+> L ,P ~+> 0.0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0.0 ,Q ~+> tick ,W ~+> W ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> L ,K ~+> M ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> L ,H ~*> M ,H ~*> Q ,H ~*> W ,H ~*> 0.0 ,H ~*> 0.0.0 ,H ~*> 0.0.0.0 ,H ~*> 0.0.0.0.0 ,H ~*> 0.0.0.0.0.0 ,H ~*> 0.0.0.1 ,H ~*> 0.0.0.2 ,H ~*> 0.1.0 ,H ~*> tick ,I ~*> I ,I ~*> K ,I ~*> L ,I ~*> M ,I ~*> Q ,I ~*> W ,I ~*> 0.0 ,I ~*> 0.0.0 ,I ~*> 0.0.0.0 ,I ~*> 0.0.0.0.0 ,I ~*> 0.0.0.0.0.0 ,I ~*> 0.0.0.1 ,I ~*> 0.0.0.2 ,I ~*> 0.1.0 ,I ~*> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0 ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> 0.0.0.1 ,J ~*> 0.0.0.2 ,J ~*> 0.1.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> 0.1.0 ,K ~*> tick ,P ~*> K ,P ~*> L ,P ~*> Q ,P ~*> W ,P ~*> 0.0.0 ,P ~*> 0.0.0.0 ,P ~*> 0.0.0.0.0 ,P ~*> 0.0.0.0.0.0 ,P ~*> 0.0.0.1 ,P ~*> 0.0.0.2 ,P ~*> tick ,Q ~*> K ,Q ~*> L ,Q ~*> Q ,Q ~*> W ,Q ~*> 0.0.0 ,Q ~*> 0.0.0.0 ,Q ~*> 0.0.0.0.0 ,Q ~*> 0.0.0.0.0.0 ,Q ~*> 0.0.0.1 ,Q ~*> 0.0.0.2 ,Q ~*> tick ,K ~*> I ,K ~*> K ,K ~*> L ,K ~*> M ,K ~*> Q ,K ~*> W ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> 0.1.0 ,K ~*> tick ,H ~^> K ,H ~^> L ,H ~^> Q ,H ~^> W ,H ~^> 0.0.0 ,H ~^> 0.0.0.0 ,H ~^> 0.0.0.0.0 ,H ~^> 0.0.0.0.0.0 ,H ~^> 0.0.0.1 ,H ~^> 0.0.0.2 ,H ~^> 0.1.0 ,H ~^> tick ,I ~^> K ,I ~^> L ,I ~^> Q ,I ~^> W ,I ~^> 0.0.0 ,I ~^> 0.0.0.0 ,I ~^> 0.0.0.0.0 ,I ~^> 0.0.0.0.0.0 ,I ~^> 0.0.0.1 ,I ~^> 0.0.0.2 ,I ~^> 0.1.0 ,I ~^> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0 ,J ~^> 0.0.0.0.0 ,J ~^> 0.0.0.0.0.0 ,J ~^> 0.0.0.1 ,J ~^> 0.0.0.2 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick ,P ~^> K ,P ~^> L ,P ~^> 0.0.0.0 ,P ~^> 0.0.0.0.0 ,P ~^> 0.0.0.0.0.0 ,P ~^> 0.0.0.1 ,P ~^> 0.0.0.2 ,P ~^> tick ,Q ~^> K ,Q ~^> L ,Q ~^> 0.0.0.0 ,Q ~^> 0.0.0.0.0 ,Q ~^> 0.0.0.0.0.0 ,Q ~^> 0.0.0.1 ,Q ~^> 0.0.0.2 ,Q ~^> tick ,K ~^> K ,K ~^> L ,K ~^> Q ,K ~^> W ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> 0.1.0 ,K ~^> tick] f0 ~> exitus616 [H ~=> M ,J ~=> L ,K ~=> A ,K ~=> E ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> N ,K ~=> O ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> L ,huge ~=> N ,huge ~=> O ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,H ~+> M ,H ~+> 0.0 ,H ~+> 0.1 ,H ~+> tick ,I ~+> I ,I ~+> M ,I ~+> 0.0 ,I ~+> 0.1 ,I ~+> tick ,J ~+> L ,J ~+> 0.0.0.2 ,J ~+> 0.1.0 ,J ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> 0.1.0 ,K ~+> tick ,L ~+> L ,P ~+> 0.0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0.0 ,Q ~+> tick ,W ~+> W ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> L ,K ~+> M ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> L ,H ~*> M ,H ~*> Q ,H ~*> W ,H ~*> 0.0 ,H ~*> 0.0.0 ,H ~*> 0.0.0.0 ,H ~*> 0.0.0.0.0 ,H ~*> 0.0.0.0.0.0 ,H ~*> 0.0.0.1 ,H ~*> 0.0.0.2 ,H ~*> 0.1.0 ,H ~*> tick ,I ~*> I ,I ~*> K ,I ~*> L ,I ~*> M ,I ~*> Q ,I ~*> W ,I ~*> 0.0 ,I ~*> 0.0.0 ,I ~*> 0.0.0.0 ,I ~*> 0.0.0.0.0 ,I ~*> 0.0.0.0.0.0 ,I ~*> 0.0.0.1 ,I ~*> 0.0.0.2 ,I ~*> 0.1.0 ,I ~*> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0 ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> 0.0.0.1 ,J ~*> 0.0.0.2 ,J ~*> 0.1.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> 0.1.0 ,K ~*> tick ,P ~*> K ,P ~*> L ,P ~*> Q ,P ~*> W ,P ~*> 0.0.0 ,P ~*> 0.0.0.0 ,P ~*> 0.0.0.0.0 ,P ~*> 0.0.0.0.0.0 ,P ~*> 0.0.0.1 ,P ~*> 0.0.0.2 ,P ~*> tick ,Q ~*> K ,Q ~*> L ,Q ~*> Q ,Q ~*> W ,Q ~*> 0.0.0 ,Q ~*> 0.0.0.0 ,Q ~*> 0.0.0.0.0 ,Q ~*> 0.0.0.0.0.0 ,Q ~*> 0.0.0.1 ,Q ~*> 0.0.0.2 ,Q ~*> tick ,K ~*> I ,K ~*> K ,K ~*> L ,K ~*> M ,K ~*> Q ,K ~*> W ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> 0.1.0 ,K ~*> tick ,H ~^> K ,H ~^> L ,H ~^> Q ,H ~^> W ,H ~^> 0.0.0 ,H ~^> 0.0.0.0 ,H ~^> 0.0.0.0.0 ,H ~^> 0.0.0.0.0.0 ,H ~^> 0.0.0.1 ,H ~^> 0.0.0.2 ,H ~^> 0.1.0 ,H ~^> tick ,I ~^> K ,I ~^> L ,I ~^> Q ,I ~^> W ,I ~^> 0.0.0 ,I ~^> 0.0.0.0 ,I ~^> 0.0.0.0.0 ,I ~^> 0.0.0.0.0.0 ,I ~^> 0.0.0.1 ,I ~^> 0.0.0.2 ,I ~^> 0.1.0 ,I ~^> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0 ,J ~^> 0.0.0.0.0 ,J ~^> 0.0.0.0.0.0 ,J ~^> 0.0.0.1 ,J ~^> 0.0.0.2 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick ,P ~^> K ,P ~^> L ,P ~^> 0.0.0.0 ,P ~^> 0.0.0.0.0 ,P ~^> 0.0.0.0.0.0 ,P ~^> 0.0.0.1 ,P ~^> 0.0.0.2 ,P ~^> tick ,Q ~^> K ,Q ~^> L ,Q ~^> 0.0.0.0 ,Q ~^> 0.0.0.0.0 ,Q ~^> 0.0.0.0.0.0 ,Q ~^> 0.0.0.1 ,Q ~^> 0.0.0.2 ,Q ~^> tick ,K ~^> K ,K ~^> L ,K ~^> Q ,K ~^> W ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> 0.1.0 ,K ~^> tick] + f28> [H ~=> M ,J ~=> L ,K ~=> E ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> N ,K ~=> O ,huge ~=> E ,huge ~=> L ,huge ~=> N ,huge ~=> O ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,H ~+> M ,H ~+> 0.0 ,H ~+> tick ,I ~+> I ,I ~+> M ,I ~+> 0.0 ,I ~+> tick ,J ~+> L ,J ~+> 0.0.0.2 ,J ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> tick ,P ~+> 0.0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0.0 ,Q ~+> tick ,W ~+> W ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> L ,K ~+> M ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> L ,H ~*> Q ,H ~*> W ,H ~*> 0.0.0 ,H ~*> 0.0.0.0 ,H ~*> 0.0.0.0.0 ,H ~*> 0.0.0.0.0.0 ,H ~*> 0.0.0.1 ,H ~*> 0.0.0.2 ,H ~*> tick ,I ~*> I ,I ~*> K ,I ~*> L ,I ~*> Q ,I ~*> W ,I ~*> 0.0.0 ,I ~*> 0.0.0.0 ,I ~*> 0.0.0.0.0 ,I ~*> 0.0.0.0.0.0 ,I ~*> 0.0.0.1 ,I ~*> 0.0.0.2 ,I ~*> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0 ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> 0.0.0.1 ,J ~*> 0.0.0.2 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> tick ,P ~*> K ,P ~*> L ,P ~*> Q ,P ~*> W ,P ~*> 0.0.0 ,P ~*> 0.0.0.0 ,P ~*> 0.0.0.0.0 ,P ~*> 0.0.0.0.0.0 ,P ~*> 0.0.0.1 ,P ~*> 0.0.0.2 ,P ~*> tick ,Q ~*> K ,Q ~*> L ,Q ~*> Q ,Q ~*> W ,Q ~*> 0.0.0 ,Q ~*> 0.0.0.0 ,Q ~*> 0.0.0.0.0 ,Q ~*> 0.0.0.0.0.0 ,Q ~*> 0.0.0.1 ,Q ~*> 0.0.0.2 ,Q ~*> tick ,K ~*> I ,K ~*> K ,K ~*> L ,K ~*> M ,K ~*> Q ,K ~*> W ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> tick ,H ~^> K ,H ~^> L ,H ~^> Q ,H ~^> W ,H ~^> 0.0.0 ,H ~^> 0.0.0.0 ,H ~^> 0.0.0.0.0 ,H ~^> 0.0.0.0.0.0 ,H ~^> 0.0.0.1 ,H ~^> 0.0.0.2 ,H ~^> tick ,I ~^> K ,I ~^> L ,I ~^> Q ,I ~^> W ,I ~^> 0.0.0 ,I ~^> 0.0.0.0 ,I ~^> 0.0.0.0.0 ,I ~^> 0.0.0.0.0.0 ,I ~^> 0.0.0.1 ,I ~^> 0.0.0.2 ,I ~^> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0 ,J ~^> 0.0.0.0.0 ,J ~^> 0.0.0.0.0.0 ,J ~^> 0.0.0.1 ,J ~^> 0.0.0.2 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick ,P ~^> K ,P ~^> L ,P ~^> 0.0.0.0 ,P ~^> 0.0.0.0.0 ,P ~^> 0.0.0.0.0.0 ,P ~^> 0.0.0.1 ,P ~^> 0.0.0.2 ,P ~^> tick ,Q ~^> K ,Q ~^> L ,Q ~^> 0.0.0.0 ,Q ~^> 0.0.0.0.0 ,Q ~^> 0.0.0.0.0.0 ,Q ~^> 0.0.0.1 ,Q ~^> 0.0.0.2 ,Q ~^> tick ,K ~^> K ,K ~^> L ,K ~^> Q ,K ~^> W ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick] + f35> [J ~=> L ,N ~=> E ,K ~=> K ,K ~=> L ,huge ~=> E ,huge ~=> L ,huge ~=> N ,huge ~=> O ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,J ~+> 0.0.0.2 ,J ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> tick ,P ~+> 0.0.0 ,P ~+> tick ,Q ~+> Q ,Q ~+> 0.0.0 ,Q ~+> tick ,W ~+> W ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> Q ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.1 ,K ~+> 0.0.0.2 ,K ~+> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0 ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> 0.0.0.1 ,J ~*> 0.0.0.2 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> tick ,P ~*> K ,P ~*> L ,P ~*> Q ,P ~*> W ,P ~*> 0.0.0.0 ,P ~*> 0.0.0.0.0 ,P ~*> 0.0.0.0.0.0 ,P ~*> 0.0.0.1 ,P ~*> 0.0.0.2 ,P ~*> tick ,Q ~*> K ,Q ~*> L ,Q ~*> Q ,Q ~*> W ,Q ~*> 0.0.0.0 ,Q ~*> 0.0.0.0.0 ,Q ~*> 0.0.0.0.0.0 ,Q ~*> 0.0.0.1 ,Q ~*> 0.0.0.2 ,Q ~*> tick ,K ~*> K ,K ~*> L ,K ~*> Q ,K ~*> W ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> 0.0.0.1 ,K ~*> 0.0.0.2 ,K ~*> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0 ,J ~^> 0.0.0.0.0 ,J ~^> 0.0.0.0.0.0 ,J ~^> 0.0.0.1 ,J ~^> 0.0.0.2 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick ,P ~^> K ,P ~^> L ,P ~^> 0.0.0.0 ,P ~^> 0.0.0.0.0 ,P ~^> 0.0.0.0.0.0 ,P ~^> 0.0.0.1 ,P ~^> 0.0.0.2 ,P ~^> tick ,Q ~^> K ,Q ~^> L ,Q ~^> 0.0.0.0 ,Q ~^> 0.0.0.0.0 ,Q ~^> 0.0.0.0.0.0 ,Q ~^> 0.0.0.1 ,Q ~^> 0.0.0.2 ,Q ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> 0.0.0.1 ,K ~^> 0.0.0.2 ,K ~^> tick] + f37> [J ~=> L ,K ~=> K ,K ~=> L ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0.0 ,J ~^> 0.0.0.0.0.0 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0.0 ,K ~^> 0.0.0.0.0.0 ,K ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] + f52> [J ~=> L ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0.0.0 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] f37> [J ~=> L ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,J ~*> K ,J ~*> L ,J ~*> 0.0.0.0.0 ,J ~*> 0.0.0.0.0.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.0.0.0.0.0 ,K ~*> tick ,J ~^> K ,J ~^> L ,J ~^> 0.0.0.0.0.0 ,J ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.0.0.0.0.0 ,K ~^> tick] + f52> [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,K ~*> K ,K ~*> K ,K ~*> L] f37> [huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,huge ~=> V ,J ~+> L ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> L ,K ~+> 0.0.0.0.0.0 ,K ~+> tick ,K ~*> K ,K ~*> L ,K ~*> K ,K ~*> L] + f37> [K ~=> Q ,huge ~=> L ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,K ~+> K ,K ~+> 0.0.0.1 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> 0.0.0.1 ,K ~+> tick ,K ~*> K ,K ~*> K] + f37> [K ~=> Q ,huge ~=> L ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> U ,J ~+> 0.0.0.2 ,J ~+> tick ,K ~+> K ,K ~+> 0.0.0.2 ,K ~+> tick ,tick ~+> tick ,K ~+> K ,K ~+> 0.0.0.2 ,K ~+> tick ,J ~*> K ,K ~*> K ,K ~*> K] + f16> [H ~+> 0.1 ,H ~+> tick ,I ~+> I ,I ~+> 0.1 ,I ~+> tick ,J ~+> 0.1.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.1.0 ,K ~+> tick ,L ~+> L ,tick ~+> tick ,K ~+> I ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,H ~*> I ,H ~*> K ,H ~*> L ,H ~*> 0.1.0 ,H ~*> tick ,I ~*> I ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> tick ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.1.0 ,K ~*> tick ,K ~*> I ,K ~*> K ,K ~*> L ,K ~*> 0.1.0 ,K ~*> tick ,H ~^> K ,H ~^> L ,H ~^> 0.1.0 ,H ~^> tick ,I ~^> K ,I ~^> L ,I ~^> 0.1.0 ,I ~^> tick ,K ~^> K ,K ~^> L ,K ~^> 0.1.0 ,K ~^> tick] + f18> [J ~+> 0.1.0 ,J ~+> tick ,K ~+> K ,K ~+> 0.1.0 ,K ~+> tick ,L ~+> L ,tick ~+> tick ,K ~+> K ,K ~+> 0.1.0 ,K ~+> tick ,J ~*> K ,J ~*> L ,K ~*> K ,K ~*> L ,K ~*> K ,K ~*> L] YES(?,PRIMREC)