YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11} ,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (1,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (1,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (1,1) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (1,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (1,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11} ,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12) ,(0,15) ,(12,7) ,(12,8) ,(12,9) ,(12,10) ,(12,11) ,(13,11) ,(14,11) ,(15,7) ,(15,8) ,(15,9) ,(15,10) ,(15,11) ,(17,12) ,(17,15)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (1,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (1,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (1,1) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (1,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (1,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{7,8,9,10},14->{7,8,9,10},15->{} ,16->{},17->{0,13,14}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,3,4,5,6,12,15] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (1,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (1,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) Signature: {(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10} ,14->{7,8,9,10},16->{},17->{0,13,14}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 18. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (?,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (1,1) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11,18},8->{7,8,9,10,11,18},9->{7,8,9,10,11,18},10->{7,8,9,10,11,18},11->{} ,13->{7,8,9,10,11,18},14->{7,8,9,10,11,18},16->{},17->{0,13,14},18->{},19->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(13,11),(14,11)] * Step 6: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 18. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (?,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (1,1) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11,18},8->{7,8,9,10,11,18},9->{7,8,9,10,11,18},10->{7,8,9,10,11,18},11->{} ,13->{7,8,9,10,18},14->{7,8,9,10,18},16->{},17->{0,13,14},18->{},19->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,7,8,9,10,11,13,14,16,17,18,19] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7] * Step 7: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1) 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1) 16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 18. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (?,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) True (1,1) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)} Flow Graph: [0->{0,13,14},7->{7,8,9,10,11,18},8->{7,8,9,10,11,18},9->{7,8,9,10,11,18},10->{7,8,9,10,11,18},11->{} ,13->{7,8,9,10,18},14->{7,8,9,10,18},16->{},17->{0,13,14},18->{},19->{}] ,We construct a looptree: P: [0,7,8,9,10,11,13,14,16,17,18,19] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: 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,X,0.0,0.1,0.1.0,0.1.0.0,0.1.0.0.0] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= unknown, I <= unknown, J <= unknown, K <= D, L <= unknown, M <= B, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f4 [A <= unknown, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= unknown, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= unknown, U <= U, V <= V, W <= W, X <= X] f1 ~> f10 [A <= unknown, B <= K + U, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= C, L <= L, M <= M, N <= C, O <= U, P <= 0*K, Q <= C, R <= 0*K, S <= C, T <= C, U <= U, V <= V, W <= W, X <= X] f1 ~> f10 [A <= unknown, B <= K + U, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= C, L <= L, M <= M, N <= C, O <= U, P <= 0*K, Q <= C, R <= 0*K, S <= C, T <= C, U <= U, V <= V, W <= W, X <= X] f3 ~> f4 [A <= unknown, B <= 0*K, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= unknown, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= unknown, U <= U, V <= V, W <= W, X <= X] f3 ~> f1 [A <= A, B <= 2*K, C <= unknown, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= unknown, I <= unknown, J <= unknown, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= unknown] f10 ~> 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, X <= X] f3 ~> 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, X <= X] + Loop: [0.0 <= A + B] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= unknown, F <= unknown, G <= unknown, H <= unknown, I <= unknown, J <= unknown, K <= D, L <= unknown, M <= B, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X] + Loop: [0.1 <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] + Loop: [0.1.0 <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] + Loop: [0.1.0.0 <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] + Loop: [0.1.0.0.0 <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= unknown, R <= 0*K, S <= unknown, T <= N, U <= K + U, V <= unknown, W <= K + U, X <= X] + Applied Processor: FlowAbstraction + Details: () * Step 9: 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,X,0.0,0.1,0.1.0,0.1.0.0,0.1.0.0.0] f1 ~> f1 [A ~=> B ,B ~=> M ,D ~=> C ,D ~=> K ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> L] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f4 [huge ~=> A ,huge ~=> I ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> T] f1 ~> f10 [C ~=> K ,C ~=> N ,C ~=> Q ,C ~=> S ,C ~=> T ,U ~=> O ,K ~=> P ,K ~=> R ,huge ~=> A ,U ~+> B ,K ~+> B] f1 ~> f10 [C ~=> K ,C ~=> N ,C ~=> Q ,C ~=> S ,C ~=> T ,U ~=> O ,K ~=> P ,K ~=> R ,huge ~=> A ,U ~+> B ,K ~+> B] f3 ~> f4 [K ~=> B ,K ~=> C ,huge ~=> A ,huge ~=> I ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> T] f3 ~> f1 [K ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> X] f10 ~> exitus616 [] f3 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f1 ~> f1 [A ~=> B ,B ~=> M ,D ~=> C ,D ~=> K ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> L] + Loop: [U ~+> 0.1,K ~+> 0.1] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] + Loop: [U ~+> 0.1.0,K ~+> 0.1.0] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] + Loop: [U ~+> 0.1.0.0,K ~+> 0.1.0.0] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] + Loop: [U ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0] f10 ~> f10 [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,K ~+> U ,K ~+> W] + Applied Processor: LareProcessor + Details: f3 ~> f4 [A ~=> M ,U ~=> O ,K ~=> B ,K ~=> C ,K ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> V ,huge ~=> X ,A ~+> 0.0 ,A ~+> tick ,U ~+> B ,U ~+> U ,U ~+> W ,U ~+> 0.1 ,U ~+> 0.1.0 ,U ~+> 0.1.0.0 ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> U ,K ~+> W ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,U ~*> W ,U ~*> 0.1.0 ,U ~*> 0.1.0.0 ,U ~*> 0.1.0.0.0 ,U ~*> tick ,K ~*> U ,K ~*> W ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,U ~^> U ,U ~^> W ,U ~^> 0.1.0 ,U ~^> 0.1.0.0 ,U ~^> 0.1.0.0.0 ,U ~^> tick ,K ~^> U ,K ~^> W ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] f3 ~> exitus616 [A ~=> M ,U ~=> O ,K ~=> M ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> Q ,huge ~=> S ,huge ~=> T ,huge ~=> V ,huge ~=> X ,A ~+> 0.0 ,A ~+> tick ,U ~+> B ,U ~+> U ,U ~+> W ,U ~+> 0.1 ,U ~+> 0.1.0 ,U ~+> 0.1.0.0 ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> U ,K ~+> W ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,U ~*> W ,U ~*> 0.1.0 ,U ~*> 0.1.0.0 ,U ~*> 0.1.0.0.0 ,U ~*> tick ,K ~*> U ,K ~*> W ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,U ~^> U ,U ~^> W ,U ~^> 0.1.0 ,U ~^> 0.1.0.0 ,U ~^> 0.1.0.0.0 ,U ~^> tick ,K ~^> U ,K ~^> W ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f1> [A ~=> B ,A ~=> M ,B ~=> M ,D ~=> C ,D ~=> K ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick] + f10> [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,U ~+> 0.1 ,U ~+> 0.1.0 ,U ~+> 0.1.0.0 ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> W ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,U ~*> W ,U ~*> 0.1.0 ,U ~*> 0.1.0.0 ,U ~*> 0.1.0.0.0 ,U ~*> tick ,K ~*> U ,K ~*> W ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,U ~^> U ,U ~^> W ,U ~^> 0.1.0 ,U ~^> 0.1.0.0 ,U ~^> 0.1.0.0.0 ,U ~^> tick ,K ~^> U ,K ~^> W ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f10> [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,U ~+> 0.1.0 ,U ~+> 0.1.0.0 ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> W ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,U ~*> W ,U ~*> 0.1.0.0 ,U ~*> 0.1.0.0.0 ,U ~*> tick ,K ~*> U ,K ~*> W ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,U ~^> U ,U ~^> W ,U ~^> 0.1.0.0 ,U ~^> 0.1.0.0.0 ,U ~^> tick ,K ~^> U ,K ~^> W ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f10> [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,U ~+> 0.1.0.0 ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> W ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,U ~*> W ,U ~*> 0.1.0.0.0 ,U ~*> tick ,K ~*> U ,K ~*> W ,K ~*> 0.1.0.0.0 ,K ~*> tick ,U ~^> U ,K ~^> U] + f10> [N ~=> T ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> K ,huge ~=> Q ,huge ~=> S ,huge ~=> V ,U ~+> U ,U ~+> W ,U ~+> 0.1.0.0.0 ,U ~+> tick ,tick ~+> tick ,K ~+> U ,K ~+> W ,K ~+> 0.1.0.0.0 ,K ~+> tick ,U ~*> U ,K ~*> U ,K ~*> W] YES(?,PRIMREC)