YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (1,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(3,9)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (1,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] 10. 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) 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) -> 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) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9,11},3->{5,6,7,8,9,11},4->{2,3,4},5->{5,6,7,8,9,11},6->{5,6,7,8,9,11},7->{5 ,6,7,8,9,11},8->{5,6,7,8,9,11},9->{},10->{},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(3,9)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] 10. 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) 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) -> 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) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,11},3->{5,6,7,8,11},4->{2,3,4},5->{5,6,7,8,9,11},6->{5,6,7,8,9,11},7->{5,6,7 ,8,9,11},8->{5,6,7,8,9,11},9->{},10->{},11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [8] | `- p:[5,6,7] c: [7] | `- p:[5,6] c: [6] | `- p:[5] c: [5] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. 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) 1. 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) 2. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. 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) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. 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 >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 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) -> 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) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] 10. 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) 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) -> 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) Signature: {(exitus616,24);(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,11},3->{5,6,7,8,11},4->{2,3,4},5->{5,6,7,8,9,11},6->{5,6,7,8,9,11},7->{5,6,7 ,8,9,11},8->{5,6,7,8,9,11},9->{},10->{},11->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [8] | `- p:[5,6,7] c: [7] | `- p:[5,6] c: [6] | `- p:[5] c: [5]) + 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,X,0.0,0.1,0.1.0,0.1.0.0,0.1.0.0.0] 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] 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] 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] 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] 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] 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] + Loop: [0.0 <= K + 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 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,X,0.0,0.1,0.1.0,0.1.0.0,0.1.0.0.0] f3 ~> f1 [K ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> G ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> X] f3 ~> f4 [K ~=> B ,K ~=> C ,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] 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] f3 ~> exitus616 [] f10 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 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.0 ,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.0 ,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 ,K ~+> 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 ,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)