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