MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f16(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f16(A,1 + B,D,N2,D,O2,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [A >= 1 + B && B >= 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 1. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 2. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 3. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 4. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 5. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 6. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 7. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 8. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 9. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 10. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 11. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 12. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 13. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 14. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 15. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 16. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,1 + S,K,L,1,N2,O2,K,O2,K,S,R2,V,V,I,L,S2,T2,U2,Q2,S,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && K >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && 0 >= 1 + K] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && K >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 22. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && K >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 23. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && 0 >= 1 + K] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 24. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O2,K,O2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,R2,S2,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && K >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 25. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 26. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 27. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 28. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 29. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 30. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 31. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 32. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 33. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 34. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 35. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 36. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 37. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 38. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 39. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 40. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f4(A,B,C,D,E,F,G,H,I,J,K,L,1 + M,N2,O2,K,O2,K,-1 + S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,R2,S2,V,I,L,1 + M [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,-1 + S,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 41. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 42. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 43. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 44. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 45. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 46. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 47. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 48. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2 [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 49. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,Q2,N1,U2,R2 [N1 >= 0 && 0 >= 1 + V2 && N2 >= 2 && O1 = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S2,T2,P2,W2,O2,V2,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 50. f13(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,Q2,N1,U2,R2 [N1 >= 0 && V2 >= 1 && N2 >= 2 && O1 = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S2,T2,P2,W2,O2,V2,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 51. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 52. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 53. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 54. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 55. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 56. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 57. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 58. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,R2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,0,O2[M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,0,O2,O2,M1,U1,V1,-1 + W1,I,-1 + W1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 59. f14(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,Q2,N1,U2,R2 [N2 >= 2 && W1 >= 0 && O1 = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S2,T2,P2,W2,O2,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 60. f0(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f16(O2,2,R2,S2,R2,F,G,H,I,J,K,L,M,O2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [O2 >= 2] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,N2,R2,T2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) 61. f16(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f4(O2,S2,R2,W2,P2,F,G,H,I,S,K,K,0,N2,V2,K,V2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,O1,P1,Q1,R1,S1,T1,U2,V1,W1,X1,Y1,Z1,Q2,B2,1 + S,T2,V,I,Y2,Z2,I2,J2,K2,L2,M2) 62. f16(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f4(O2,S2,R2,W2,P2,F,G,H,I,S,K,K,0,N2,V2,K,V2,K,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,O1,P1,Q1,R1,S1,T1,U2,V1,W1,X1,Y1,Z1,Q2,B2,1 + S,T2,V,I,Y2,Z2,I2,J2,K2,L2,M2) 63. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && 0 >= 1 + S1 && K = 0 && I2 = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,I,I,U2,M2) 64. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && K = 0 && I2 = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,I,I,U2,M2) 65. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && K = 0 && I2 = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,I,I,U2,M2) 66. f2(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && S1 >= 1 && K = 0 && I2 = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,I,I,U2,M2) 67. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 68. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 69. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 70. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 71. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 72. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 73. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 74. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,I) 75. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && 1 + M = I2 && K = 0] 76. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + S1 && L >= 1 && 1 + M = I2 && K = 0] 77. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) 78. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) 79. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) 80. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) 81. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && S1 >= 1 && 0 >= 1 + L && 1 + M = I2 && K = 0] 82. f4(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f14(A,B,C,D,E,F,G,H,I,J,O2,L,M,N2,R2,S2,Q,T2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,S1,W1,0[Q2 >= 2 (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,S1,0,S1,S1,S1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,1 + W1,J2,I,U2,M2) && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && S1 >= 1 && L >= 1 && 1 + M = I2 && K = 0] 83. f0(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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(R2,T2,S2,Y2,V2,F,G,H,I,J,U2,L,M,O2,Z2,X2,Q,D3,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,I3 [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] (1,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2) ,N1,H3,E3,F3,G3,J3,K3,P2,V1,W1,X1,Y1,N2,W2,B2,C2,Q2,E2,F2,G2,H2,I2,J2,K2,L2,M2) Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Flow Graph: [0->{0,61,62},1->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},2->{25,26,27,28 ,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},3->{25,26,27,28,29,30,31,32,33,34,35,36,37,38 ,39,40,75,76,77,78,79,80,81,82},4->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,5->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},6->{25,26,27,28,29,30,31,32,33 ,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},7->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77 ,78,79,80,81,82},8->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},9->{25,26,27 ,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},10->{25,26,27,28,29,30,31,32,33,34,35,36,37 ,38,39,40,75,76,77,78,79,80,81,82},11->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81 ,82},12->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},13->{25,26,27,28,29,30,31 ,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},14->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75 ,76,77,78,79,80,81,82},15->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},16->{25 ,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},17->{25,26,27,28,29,30,31,32,33,34,35 ,36,37,38,39,40,75,76,77,78,79,80,81,82},18->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79 ,80,81,82},19->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},20->{25,26,27,28,29 ,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},21->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39 ,40,75,76,77,78,79,80,81,82},22->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,23->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},24->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},25->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76 ,77,78,79,80,81,82},26->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},27->{25,26 ,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},28->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,75,76,77,78,79,80,81,82},29->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},30->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},31->{25,26,27,28,29,30 ,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},32->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40 ,75,76,77,78,79,80,81,82},33->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,34->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},35->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},36->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76 ,77,78,79,80,81,82},37->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},38->{25,26 ,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},39->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,75,76,77,78,79,80,81,82},40->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},41->{51,52,53,54,55,56,57,58,59},42->{51,52,53,54,55,56,57,58,59},43->{51,52,53,54,55,56,57,58,59} ,44->{51,52,53,54,55,56,57,58,59},45->{51,52,53,54,55,56,57,58,59},46->{51,52,53,54,55,56,57,58,59},47->{51 ,52,53,54,55,56,57,58,59},48->{51,52,53,54,55,56,57,58,59},49->{},50->{},51->{51,52,53,54,55,56,57,58,59} ,52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51 ,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58,59},57->{51,52,53,54,55,56,57,58,59},58->{51,52,53,54 ,55,56,57,58,59},59->{},60->{0,61,62},61->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},62->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},63->{51,52,53,54,55,56 ,57,58,59},64->{51,52,53,54,55,56,57,58,59},65->{51,52,53,54,55,56,57,58,59},66->{51,52,53,54,55,56,57,58 ,59},67->{51,52,53,54,55,56,57,58,59},68->{51,52,53,54,55,56,57,58,59},69->{51,52,53,54,55,56,57,58,59} ,70->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55,56,57,58,59},72->{51,52,53,54,55,56,57,58,59},73->{51 ,52,53,54,55,56,57,58,59},74->{51,52,53,54,55,56,57,58,59},75->{51,52,53,54,55,56,57,58,59},76->{51,52,53,54 ,55,56,57,58,59},77->{51,52,53,54,55,56,57,58,59},78->{51,52,53,54,55,56,57,58,59},79->{51,52,53,54,55,56,57 ,58,59},80->{51,52,53,54,55,56,57,58,59},81->{51,52,53,54,55,56,57,58,59},82->{51,52,53,54,55,56,57,58,59} ,83->{}] + Applied Processor: ArgumentFilter [2,3,4,5,6,7,8,13,14,15,16,17,19,20,21,22,23,24,25,26,27,29,30,31,32,33,34,35,36,37,41,42,43,45,46,47,49,50,51,52,53,55,56,57,58,59,61,62,63,64] + Details: We remove following argument positions: [2 ,3 ,4 ,5 ,6 ,7 ,8 ,13 ,14 ,15 ,16 ,17 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,26 ,27 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,41 ,42 ,43 ,45 ,46 ,47 ,49 ,50 ,51 ,52 ,53 ,55 ,56 ,57 ,58 ,59 ,61 ,62 ,63 ,64]. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] (?,1) 1. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 2. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 3. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 4. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 5. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 6. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 7. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 8. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 9. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 10. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 11. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 12. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 13. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 14. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 15. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 16. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 17. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 18. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && K >= 1] (?,1) 19. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && 0 >= 1 + K] (?,1) 20. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && K >= 1] (?,1) 21. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 22. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && K >= 1] (?,1) 23. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && 0 >= 1 + K] (?,1) 24. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && K >= 1] (?,1) 25. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 26. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 27. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 28. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 29. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 30. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 31. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 32. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 33. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 34. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 35. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 36. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 37. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 38. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 39. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 40. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 41. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 42. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 43. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 44. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 45. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 46. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 47. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 48. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 49. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && 0 >= 1 + V2 && N2 >= 2 && O1 = M1] (?,1) 50. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && V2 >= 1 && N2 >= 2 && O1 = M1] (?,1) 51. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 52. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 53. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 54. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 55. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 56. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 57. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 58. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 59. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N2 >= 2 && W1 >= 0 && O1 = M1] (?,1) 60. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] (1,1) 61. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] (?,1) 62. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] (?,1) 63. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && 0 >= 1 + S1 && K = 0 && I2 = 1] (?,1) 64. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && K = 0 && I2 = 1] (?,1) 65. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && K = 0 && I2 = 1] (?,1) 66. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && S1 >= 1 && K = 0 && I2 = 1] (?,1) 67. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 68. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) 69. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 70. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) 71. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 72. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) 73. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 74. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) 75. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 (?,1) && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && 1 + M = I2 && K = 0] 76. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 (?,1) && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + S1 && L >= 1 && 1 + M = I2 && K = 0] 77. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 78. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 79. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 80. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 81. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 (?,1) && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && S1 >= 1 && 0 >= 1 + L && 1 + M = I2 && K = 0] 82. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 (?,1) && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && S1 >= 1 && L >= 1 && 1 + M = I2 && K = 0] 83. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] (1,1) Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Flow Graph: [0->{0,61,62},1->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},2->{25,26,27,28 ,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},3->{25,26,27,28,29,30,31,32,33,34,35,36,37,38 ,39,40,75,76,77,78,79,80,81,82},4->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,5->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},6->{25,26,27,28,29,30,31,32,33 ,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},7->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77 ,78,79,80,81,82},8->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},9->{25,26,27 ,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},10->{25,26,27,28,29,30,31,32,33,34,35,36,37 ,38,39,40,75,76,77,78,79,80,81,82},11->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81 ,82},12->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},13->{25,26,27,28,29,30,31 ,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},14->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75 ,76,77,78,79,80,81,82},15->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},16->{25 ,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},17->{25,26,27,28,29,30,31,32,33,34,35 ,36,37,38,39,40,75,76,77,78,79,80,81,82},18->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79 ,80,81,82},19->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},20->{25,26,27,28,29 ,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},21->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39 ,40,75,76,77,78,79,80,81,82},22->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,23->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},24->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},25->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76 ,77,78,79,80,81,82},26->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},27->{25,26 ,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},28->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,75,76,77,78,79,80,81,82},29->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},30->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},31->{25,26,27,28,29,30 ,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},32->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40 ,75,76,77,78,79,80,81,82},33->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82} ,34->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},35->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},36->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76 ,77,78,79,80,81,82},37->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},38->{25,26 ,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},39->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,75,76,77,78,79,80,81,82},40->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},41->{51,52,53,54,55,56,57,58,59},42->{51,52,53,54,55,56,57,58,59},43->{51,52,53,54,55,56,57,58,59} ,44->{51,52,53,54,55,56,57,58,59},45->{51,52,53,54,55,56,57,58,59},46->{51,52,53,54,55,56,57,58,59},47->{51 ,52,53,54,55,56,57,58,59},48->{51,52,53,54,55,56,57,58,59},49->{},50->{},51->{51,52,53,54,55,56,57,58,59} ,52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51 ,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58,59},57->{51,52,53,54,55,56,57,58,59},58->{51,52,53,54 ,55,56,57,58,59},59->{},60->{0,61,62},61->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80 ,81,82},62->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,75,76,77,78,79,80,81,82},63->{51,52,53,54,55,56 ,57,58,59},64->{51,52,53,54,55,56,57,58,59},65->{51,52,53,54,55,56,57,58,59},66->{51,52,53,54,55,56,57,58 ,59},67->{51,52,53,54,55,56,57,58,59},68->{51,52,53,54,55,56,57,58,59},69->{51,52,53,54,55,56,57,58,59} ,70->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55,56,57,58,59},72->{51,52,53,54,55,56,57,58,59},73->{51 ,52,53,54,55,56,57,58,59},74->{51,52,53,54,55,56,57,58,59},75->{51,52,53,54,55,56,57,58,59},76->{51,52,53,54 ,55,56,57,58,59},77->{51,52,53,54,55,56,57,58,59},78->{51,52,53,54,55,56,57,58,59},79->{51,52,53,54,55,56,57 ,58,59},80->{51,52,53,54,55,56,57,58,59},81->{51,52,53,54,55,56,57,58,59},82->{51,52,53,54,55,56,57,58,59} ,83->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [63,66,67,68,73,74,75,76,81,82] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] (?,1) 1. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 2. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 3. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 4. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 5. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 6. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 7. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 8. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 9. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 10. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 11. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 12. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 13. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 14. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 15. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 16. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 17. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 18. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && K >= 1] (?,1) 19. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && 0 >= 1 + K] (?,1) 20. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && K >= 1] (?,1) 21. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 22. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && K >= 1] (?,1) 23. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && 0 >= 1 + K] (?,1) 24. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && K >= 1] (?,1) 25. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 26. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 27. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 28. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 29. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 30. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 31. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 32. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 33. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 34. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 35. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 36. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 37. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 38. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 39. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 40. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 41. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 42. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 43. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 44. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 45. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 46. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 47. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 48. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 49. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && 0 >= 1 + V2 && N2 >= 2 && O1 = M1] (?,1) 50. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && V2 >= 1 && N2 >= 2 && O1 = M1] (?,1) 51. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 52. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 53. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 54. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 55. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 56. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 57. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 58. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 59. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N2 >= 2 && W1 >= 0 && O1 = M1] (?,1) 60. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] (1,1) 61. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] (?,1) 62. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] (?,1) 64. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && K = 0 && I2 = 1] (?,1) 65. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && K = 0 && I2 = 1] (?,1) 69. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 70. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) 71. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 72. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) 77. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 78. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 79. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 80. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 83. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] (1,1) Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Flow Graph: [0->{0,61,62},1->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},2->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,77,78,79,80},3->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80} ,4->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},5->{25,26,27,28,29,30,31,32,33,34,35,36,37 ,38,39,40,77,78,79,80},6->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},7->{25,26,27,28,29 ,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},8->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79 ,80},9->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},10->{25,26,27,28,29,30,31,32,33,34,35 ,36,37,38,39,40,77,78,79,80},11->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},12->{25,26,27 ,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},13->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77 ,78,79,80},14->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},15->{25,26,27,28,29,30,31,32,33 ,34,35,36,37,38,39,40,77,78,79,80},16->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},17->{25 ,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},18->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39 ,40,77,78,79,80},19->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},20->{25,26,27,28,29,30,31 ,32,33,34,35,36,37,38,39,40,77,78,79,80},21->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80} ,22->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},23->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,77,78,79,80},24->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},25->{25,26,27,28 ,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},26->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78 ,79,80},27->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},28->{25,26,27,28,29,30,31,32,33,34 ,35,36,37,38,39,40,77,78,79,80},29->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},30->{25,26 ,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},31->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40 ,77,78,79,80},32->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},33->{25,26,27,28,29,30,31,32 ,33,34,35,36,37,38,39,40,77,78,79,80},34->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80} ,35->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},36->{25,26,27,28,29,30,31,32,33,34,35,36 ,37,38,39,40,77,78,79,80},37->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},38->{25,26,27,28 ,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},39->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78 ,79,80},40->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},41->{51,52,53,54,55,56,57,58,59} ,42->{51,52,53,54,55,56,57,58,59},43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51 ,52,53,54,55,56,57,58,59},46->{51,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{51,52,53,54 ,55,56,57,58,59},49->{},50->{},51->{51,52,53,54,55,56,57,58,59},52->{51,52,53,54,55,56,57,58,59},53->{51,52 ,53,54,55,56,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55 ,56,57,58,59},57->{51,52,53,54,55,56,57,58,59},58->{51,52,53,54,55,56,57,58,59},59->{},60->{0,61,62},61->{25 ,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,77,78,79,80},62->{25,26,27,28,29,30,31,32,33,34,35,36,37,38,39 ,40,77,78,79,80},64->{51,52,53,54,55,56,57,58,59},65->{51,52,53,54,55,56,57,58,59},69->{51,52,53,54,55,56,57 ,58,59},70->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55,56,57,58,59},72->{51,52,53,54,55,56,57,58,59} ,77->{51,52,53,54,55,56,57,58,59},78->{51,52,53,54,55,56,57,58,59},79->{51,52,53,54,55,56,57,58,59},80->{51 ,52,53,54,55,56,57,58,59},83->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,27) ,(1,28) ,(1,29) ,(1,30) ,(1,31) ,(1,32) ,(1,35) ,(1,36) ,(1,37) ,(1,38) ,(1,39) ,(1,40) ,(1,77) ,(1,78) ,(1,79) ,(1,80) ,(2,25) ,(2,26) ,(2,29) ,(2,30) ,(2,31) ,(2,32) ,(2,33) ,(2,34) ,(2,37) ,(2,38) ,(2,39) ,(2,40) ,(2,77) ,(2,78) ,(2,79) ,(2,80) ,(3,27) ,(3,28) ,(3,29) ,(3,30) ,(3,31) ,(3,32) ,(3,35) ,(3,36) ,(3,37) ,(3,38) ,(3,39) ,(3,40) ,(3,77) ,(3,78) ,(3,79) ,(3,80) ,(4,25) ,(4,26) ,(4,29) ,(4,30) ,(4,31) ,(4,32) ,(4,33) ,(4,34) ,(4,37) ,(4,38) ,(4,39) ,(4,40) ,(4,77) ,(4,78) ,(4,79) ,(4,80) ,(5,25) ,(5,26) ,(5,27) ,(5,28) ,(5,31) ,(5,32) ,(5,33) ,(5,34) ,(5,35) ,(5,36) ,(5,39) ,(5,40) ,(5,77) ,(5,78) ,(5,79) ,(5,80) ,(6,25) ,(6,26) ,(6,27) ,(6,28) ,(6,29) ,(6,30) ,(6,33) ,(6,34) ,(6,35) ,(6,36) ,(6,37) ,(6,38) ,(6,77) ,(6,78) ,(6,79) ,(6,80) ,(7,25) ,(7,26) ,(7,27) ,(7,28) ,(7,31) ,(7,32) ,(7,33) ,(7,34) ,(7,35) ,(7,36) ,(7,39) ,(7,40) ,(7,77) ,(7,78) ,(7,79) ,(7,80) ,(8,25) ,(8,26) ,(8,27) ,(8,28) ,(8,29) ,(8,30) ,(8,33) ,(8,34) ,(8,35) ,(8,36) ,(8,37) ,(8,38) ,(8,77) ,(8,78) ,(8,79) ,(8,80) ,(9,27) ,(9,28) ,(9,29) ,(9,30) ,(9,31) ,(9,32) ,(9,35) ,(9,36) ,(9,37) ,(9,38) ,(9,39) ,(9,40) ,(9,77) ,(9,78) ,(9,79) ,(9,80) ,(10,25) ,(10,26) ,(10,29) ,(10,30) ,(10,31) ,(10,32) ,(10,33) ,(10,34) ,(10,37) ,(10,38) ,(10,39) ,(10,40) ,(10,77) ,(10,78) ,(10,79) ,(10,80) ,(11,27) ,(11,28) ,(11,29) ,(11,30) ,(11,31) ,(11,32) ,(11,35) ,(11,36) ,(11,37) ,(11,38) ,(11,39) ,(11,40) ,(11,77) ,(11,78) ,(11,79) ,(11,80) ,(12,25) ,(12,26) ,(12,29) ,(12,30) ,(12,31) ,(12,32) ,(12,33) ,(12,34) ,(12,37) ,(12,38) ,(12,39) ,(12,40) ,(12,77) ,(12,78) ,(12,79) ,(12,80) ,(13,25) ,(13,26) ,(13,27) ,(13,28) ,(13,31) ,(13,32) ,(13,33) ,(13,34) ,(13,35) ,(13,36) ,(13,39) ,(13,40) ,(13,77) ,(13,78) ,(13,79) ,(13,80) ,(14,25) ,(14,26) ,(14,27) ,(14,28) ,(14,29) ,(14,30) ,(14,33) ,(14,34) ,(14,35) ,(14,36) ,(14,37) ,(14,38) ,(14,77) ,(14,78) ,(14,79) ,(14,80) ,(15,25) ,(15,26) ,(15,27) ,(15,28) ,(15,31) ,(15,32) ,(15,33) ,(15,34) ,(15,35) ,(15,36) ,(15,39) ,(15,40) ,(15,77) ,(15,78) ,(15,79) ,(15,80) ,(16,25) ,(16,26) ,(16,27) ,(16,28) ,(16,29) ,(16,30) ,(16,33) ,(16,34) ,(16,35) ,(16,36) ,(16,37) ,(16,38) ,(16,77) ,(16,78) ,(16,79) ,(16,80) ,(17,27) ,(17,28) ,(17,29) ,(17,30) ,(17,31) ,(17,32) ,(17,35) ,(17,36) ,(17,37) ,(17,38) ,(17,39) ,(17,40) ,(17,77) ,(17,78) ,(17,79) ,(17,80) ,(18,25) ,(18,26) ,(18,27) ,(18,28) ,(18,31) ,(18,32) ,(18,33) ,(18,34) ,(18,35) ,(18,36) ,(18,39) ,(18,40) ,(18,77) ,(18,78) ,(18,79) ,(18,80) ,(19,27) ,(19,28) ,(19,29) ,(19,30) ,(19,31) ,(19,32) ,(19,35) ,(19,36) ,(19,37) ,(19,38) ,(19,39) ,(19,40) ,(19,77) ,(19,78) ,(19,79) ,(19,80) ,(20,25) ,(20,26) ,(20,27) ,(20,28) ,(20,31) ,(20,32) ,(20,33) ,(20,34) ,(20,35) ,(20,36) ,(20,39) ,(20,40) ,(20,77) ,(20,78) ,(20,79) ,(20,80) ,(21,25) ,(21,26) ,(21,29) ,(21,30) ,(21,31) ,(21,32) ,(21,33) ,(21,34) ,(21,37) ,(21,38) ,(21,39) ,(21,40) ,(21,77) ,(21,78) ,(21,79) ,(21,80) ,(22,25) ,(22,26) ,(22,27) ,(22,28) ,(22,29) ,(22,30) ,(22,33) ,(22,34) ,(22,35) ,(22,36) ,(22,37) ,(22,38) ,(22,77) ,(22,78) ,(22,79) ,(22,80) ,(23,25) ,(23,26) ,(23,29) ,(23,30) ,(23,31) ,(23,32) ,(23,33) ,(23,34) ,(23,37) ,(23,38) ,(23,39) ,(23,40) ,(23,77) ,(23,78) ,(23,79) ,(23,80) ,(24,25) ,(24,26) ,(24,27) ,(24,28) ,(24,29) ,(24,30) ,(24,33) ,(24,34) ,(24,35) ,(24,36) ,(24,37) ,(24,38) ,(24,77) ,(24,78) ,(24,79) ,(24,80) ,(25,27) ,(25,28) ,(25,29) ,(25,30) ,(25,31) ,(25,32) ,(25,35) ,(25,36) ,(25,37) ,(25,38) ,(25,39) ,(25,40) ,(25,77) ,(25,78) ,(25,79) ,(25,80) ,(26,27) ,(26,28) ,(26,29) ,(26,30) ,(26,31) ,(26,32) ,(26,35) ,(26,36) ,(26,37) ,(26,38) ,(26,39) ,(26,40) ,(26,77) ,(26,78) ,(26,79) ,(26,80) ,(27,25) ,(27,26) ,(27,29) ,(27,30) ,(27,31) ,(27,32) ,(27,33) ,(27,34) ,(27,37) ,(27,38) ,(27,39) ,(27,40) ,(27,77) ,(27,78) ,(27,79) ,(27,80) ,(28,25) ,(28,26) ,(28,29) ,(28,30) ,(28,31) ,(28,32) ,(28,33) ,(28,34) ,(28,37) ,(28,38) ,(28,39) ,(28,40) ,(28,77) ,(28,78) ,(28,79) ,(28,80) ,(29,25) ,(29,26) ,(29,27) ,(29,28) ,(29,31) ,(29,32) ,(29,33) ,(29,34) ,(29,35) ,(29,36) ,(29,39) ,(29,40) ,(29,77) ,(29,78) ,(29,79) ,(29,80) ,(30,25) ,(30,26) ,(30,27) ,(30,28) ,(30,31) ,(30,32) ,(30,33) ,(30,34) ,(30,35) ,(30,36) ,(30,39) ,(30,40) ,(30,77) ,(30,78) ,(30,79) ,(30,80) ,(31,25) ,(31,26) ,(31,27) ,(31,28) ,(31,29) ,(31,30) ,(31,33) ,(31,34) ,(31,35) ,(31,36) ,(31,37) ,(31,38) ,(31,77) ,(31,78) ,(31,79) ,(31,80) ,(32,25) ,(32,26) ,(32,27) ,(32,28) ,(32,29) ,(32,30) ,(32,33) ,(32,34) ,(32,35) ,(32,36) ,(32,37) ,(32,38) ,(32,77) ,(32,78) ,(32,79) ,(32,80) ,(33,27) ,(33,28) ,(33,29) ,(33,30) ,(33,31) ,(33,32) ,(33,35) ,(33,36) ,(33,37) ,(33,38) ,(33,39) ,(33,40) ,(33,77) ,(33,78) ,(33,79) ,(33,80) ,(34,27) ,(34,28) ,(34,29) ,(34,30) ,(34,31) ,(34,32) ,(34,35) ,(34,36) ,(34,37) ,(34,38) ,(34,39) ,(34,40) ,(34,77) ,(34,78) ,(34,79) ,(34,80) ,(35,25) ,(35,26) ,(35,29) ,(35,30) ,(35,31) ,(35,32) ,(35,33) ,(35,34) ,(35,37) ,(35,38) ,(35,39) ,(35,40) ,(35,77) ,(35,78) ,(35,79) ,(35,80) ,(36,25) ,(36,26) ,(36,29) ,(36,30) ,(36,31) ,(36,32) ,(36,33) ,(36,34) ,(36,37) ,(36,38) ,(36,39) ,(36,40) ,(36,77) ,(36,78) ,(36,79) ,(36,80) ,(37,25) ,(37,26) ,(37,27) ,(37,28) ,(37,31) ,(37,32) ,(37,33) ,(37,34) ,(37,35) ,(37,36) ,(37,39) ,(37,40) ,(37,77) ,(37,78) ,(37,79) ,(37,80) ,(38,25) ,(38,26) ,(38,27) ,(38,28) ,(38,31) ,(38,32) ,(38,33) ,(38,34) ,(38,35) ,(38,36) ,(38,39) ,(38,40) ,(38,77) ,(38,78) ,(38,79) ,(38,80) ,(39,25) ,(39,26) ,(39,27) ,(39,28) ,(39,29) ,(39,30) ,(39,33) ,(39,34) ,(39,35) ,(39,36) ,(39,37) ,(39,38) ,(39,77) ,(39,78) ,(39,79) ,(39,80) ,(40,25) ,(40,26) ,(40,27) ,(40,28) ,(40,29) ,(40,30) ,(40,33) ,(40,34) ,(40,35) ,(40,36) ,(40,37) ,(40,38) ,(40,77) ,(40,78) ,(40,79) ,(40,80) ,(41,58) ,(41,59) ,(48,51) ,(48,59) ,(51,58) ,(51,59) ,(58,51) ,(58,59) ,(61,27) ,(61,28) ,(61,29) ,(61,30) ,(61,31) ,(61,32) ,(61,35) ,(61,36) ,(61,37) ,(61,38) ,(61,39) ,(61,40) ,(61,77) ,(61,78) ,(61,79) ,(61,80) ,(62,25) ,(62,26) ,(62,27) ,(62,28) ,(62,29) ,(62,30) ,(62,33) ,(62,34) ,(62,35) ,(62,36) ,(62,37) ,(62,38) ,(62,77) ,(62,78) ,(62,79) ,(62,80) ,(64,51) ,(64,59) ,(65,58) ,(65,59) ,(69,51) ,(69,59) ,(70,51) ,(70,59) ,(71,58) ,(71,59) ,(72,58) ,(72,59) ,(77,51) ,(77,59) ,(78,51) ,(78,59) ,(79,58) ,(79,59) ,(80,58) ,(80,59)] * Step 4: UnreachableRules MAYBE + Considered Problem: Rules: 0. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] (?,1) 1. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 2. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 3. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 4. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 5. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 6. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 7. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 8. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && 0 >= 1 + P2 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 9. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 10. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 11. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 12. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && 0 >= 1 + K && Q2 >= 1 && L >= 1 && M = 1] (?,1) 13. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && 0 >= 1 + L && M = 1] (?,1) 14. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && 0 >= 1 + Q2 && L >= 1 && M = 1] (?,1) 15. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && 0 >= 1 + L && M = 1] (?,1) 16. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,1 + S,K,L,1,S,S,M1,N1,O1,S1,W1,C2,I2) [J >= 0 && N2 >= 2 && P2 >= 1 && K >= 1 && Q2 >= 1 && L >= 1 && M = 1] (?,1) 17. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 18. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && 0 >= 1 + S2 && K >= 1] (?,1) 19. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && 0 >= 1 + K] (?,1) 20. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && 0 >= 1 + L && S2 >= 1 && K >= 1] (?,1) 21. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && 0 >= 1 + K] (?,1) 22. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && 0 >= 1 + S2 && K >= 1] (?,1) 23. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && 0 >= 1 + K] (?,1) 24. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [C1 >= 0 && N2 >= 2 && L >= 1 && S2 >= 1 && K >= 1] (?,1) 25. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 26. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 27. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 28. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 29. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 30. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 31. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 32. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 33. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 34. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 35. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && 0 >= 1 + S2] (?,1) 36. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && L >= 1 && S2 >= 1] (?,1) 37. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 38. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && 0 >= 1 + L && S2 >= 1] (?,1) 39. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 40. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 41. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 42. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 43. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 44. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [R2 >= 1 + M1 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 45. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && 0 >= 1 + O2 && O1 = 0] (?,1) 46. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && O2 >= 1 + R2 && O2 >= 1 && O1 = 0] (?,1) 47. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 48. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,W1,C2,I2) [M1 >= 1 + R2 && N1 >= 0 && N2 >= 2 && R2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 49. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && 0 >= 1 + V2 && N2 >= 2 && O1 = M1] (?,1) 50. f13(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N1 >= 0 && V2 >= 1 && N2 >= 2 && O1 = M1] (?,1) 51. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 52. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 53. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 54. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [S2 >= 1 + M1 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 55. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && 0 >= 1 + O2 && O1 = 0] (?,1) 56. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && O2 >= 1 + S2 && O2 >= 1 && O1 = 0] (?,1) 57. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && 0 >= 1 + O2 && O1 = 0] (?,1) 58. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,K,L,M,S,C1,M1,N1,0,O2,-1 + W1,C2,I2) [M1 >= 1 + S2 && W1 >= 0 && N2 >= 2 && S2 >= 1 + O2 && O2 >= 1 && O1 = 0] (?,1) 59. f14(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(A,B,J,K,L,M,S,C1,Q2,N1,U2,P2,W1,C2,I2) [N2 >= 2 && W1 >= 0 && O1 = M1] (?,1) 60. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] (1,1) 61. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] (?,1) 62. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] (?,1) 64. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && S1 >= 1 && J >= 0 && K = 0 && I2 = 1] (?,1) 65. f2(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && 0 >= 1 + S1 && J >= 0 && K = 0 && I2 = 1] (?,1) 69. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 70. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && S1 >= 1 && L >= 1 && K = 0 && I2 = 2] (?,1) 71. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && 0 >= 1 + L && K = 0 && I2 = 2] (?,1) 72. f3(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && C1 >= 0 && 0 >= 1 + S1 && L >= 1 && K = 0 && I2 = 2] (?,1) 77. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 78. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && S1 >= 1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 79. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && 0 >= 1 + L && 1 + M = I2 && K = 0] (?,1) 80. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f14(A,B,J,O2,L,M,S,C1,S1,W1,0,S1,W1,C2,1 + W1) [Q2 >= 2 && N2 >= 2 && I2 >= 1 && S >= 0 && 0 >= 1 + S1 && I2 >= 0 && L >= 1 && 1 + M = I2 && K = 0] (?,1) 83. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] (1,1) Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Flow Graph: [0->{0,61,62},1->{25,26,33,34},2->{27,28,35,36},3->{25,26,33,34},4->{27,28,35,36},5->{29,30,37,38},6->{31 ,32,39,40},7->{29,30,37,38},8->{31,32,39,40},9->{25,26,33,34},10->{27,28,35,36},11->{25,26,33,34},12->{27,28 ,35,36},13->{29,30,37,38},14->{31,32,39,40},15->{29,30,37,38},16->{31,32,39,40},17->{25,26,33,34},18->{29,30 ,37,38},19->{25,26,33,34},20->{29,30,37,38},21->{27,28,35,36},22->{31,32,39,40},23->{27,28,35,36},24->{31,32 ,39,40},25->{25,26,33,34},26->{25,26,33,34},27->{27,28,35,36},28->{27,28,35,36},29->{29,30,37,38},30->{29,30 ,37,38},31->{31,32,39,40},32->{31,32,39,40},33->{25,26,33,34},34->{25,26,33,34},35->{27,28,35,36},36->{27,28 ,35,36},37->{29,30,37,38},38->{29,30,37,38},39->{31,32,39,40},40->{31,32,39,40},41->{51,52,53,54,55,56,57} ,42->{51,52,53,54,55,56,57,58,59},43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51 ,52,53,54,55,56,57,58,59},46->{51,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{52,53,54,55 ,56,57,58},49->{},50->{},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{},60->{0,61,62},61->{25,26,33,34} ,62->{31,32,39,40},64->{52,53,54,55,56,57,58},65->{51,52,53,54,55,56,57},69->{52,53,54,55,56,57,58},70->{52 ,53,54,55,56,57,58},71->{51,52,53,54,55,56,57},72->{51,52,53,54,55,56,57},77->{52,53,54,55,56,57,58},78->{52 ,53,54,55,56,57,58},79->{51,52,53,54,55,56,57},80->{51,52,53,54,55,56,57},83->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,14 ,15 ,16 ,17 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,27 ,28 ,29 ,30 ,35 ,36 ,37 ,38 ,41 ,42 ,43 ,44 ,45 ,46 ,47 ,48 ,49 ,50 ,51 ,52 ,53 ,54 ,55 ,56 ,57 ,58 ,59 ,64 ,65 ,69 ,70 ,71 ,72 ,77 ,78 ,79 ,80] * Step 5: FromIts MAYBE + Considered Problem: Rules: 0. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] (?,1) 25. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 26. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 31. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 32. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 33. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] (?,1) 34. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] (?,1) 39. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] (?,1) 40. f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] (?,1) 60. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] (1,1) 61. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] (?,1) 62. f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] (?,1) 83. f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] (1,1) Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Flow Graph: [0->{0,61,62},25->{25,26,33,34},26->{25,26,33,34},31->{31,32,39,40},32->{31,32,39,40},33->{25,26,33,34} ,34->{25,26,33,34},39->{31,32,39,40},40->{31,32,39,40},60->{0,61,62},61->{25,26,33,34},62->{31,32,39,40} ,83->{}] + Applied Processor: FromIts + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] Signature: {(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Rule Graph: [0->{0,61,62},25->{25,26,33,34},26->{25,26,33,34},31->{31,32,39,40},32->{31,32,39,40},33->{25,26,33,34} ,34->{25,26,33,34},39->{31,32,39,40},40->{31,32,39,40},60->{0,61,62},61->{25,26,33,34},62->{31,32,39,40} ,83->{}] + Applied Processor: AddSinks + Details: () * Step 7: Decompose MAYBE + Considered Problem: Rules: f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] f1(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True Signature: {(exitus616,15);(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Rule Graph: [0->{0,61,62},25->{25,26,33,34,89},26->{25,26,33,34,90},31->{31,32,39,40,85},32->{31,32,39,40,86},33->{25 ,26,33,34,91},34->{25,26,33,34,92},39->{31,32,39,40,87},40->{31,32,39,40,88},60->{0,61,62},61->{25,26,33,34} ,62->{31,32,39,40},83->{84}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,25,26,31,32,33,34,39,40,60,61,62,83,84,85,86,87,88,89,90,91,92] | +- p:[0] c: [0] | +- p:[31,32,39,40] c: [31,32,39,40] | `- p:[25,26,33,34] c: [25,26,33,34] * Step 8: AbstractSize MAYBE + Considered Problem: (Rules: f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(A,1 + B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [A >= 1 + B && B >= 0] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && 0 >= 1 + U2 && K >= 1 && L >= 1 && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && 0 >= 1 + K && 0 >= 1 + L && S2 >= 1] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && 0 >= 1 + S2] f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(A,B,J,K,L,1 + M,-1 + S,C1,M1,N1,O1,S1,W1,C2,I2) [T2 >= 0 && S >= 0 && N2 >= 2 && U2 >= 1 && K >= 1 && L >= 1 && S2 >= 1] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f16(O2,2,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) [O2 >= 2] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && 0 >= 1 + L && M = 0 && K = L] f16(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f4(O2,S2,S,K,K,0,S,C1,M1,N1,O1,S1,W1,1 + S,I2) [X2 >= 2 && C2 >= X2 && N2 >= 2 && C2 >= N2 && B >= A && B >= 0 && C2 >= 0 && L >= 1 && M = 0 && K = L] f0(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> f1(R2,T2,J,U2,L,M,S,C1,I3,N1,H3,J3,W1,C2,I2) [0 >= A3 && 0 >= B3 && 0 >= O2 && 0 >= C3 && S1 = 0] f1(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True f4(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) -> exitus616(A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2) True Signature: {(exitus616,15);(f0,65);(f1,65);(f13,65);(f14,65);(f16,65);(f2,65);(f3,65);(f4,65)} Rule Graph: [0->{0,61,62},25->{25,26,33,34,89},26->{25,26,33,34,90},31->{31,32,39,40,85},32->{31,32,39,40,86},33->{25 ,26,33,34,91},34->{25,26,33,34,92},39->{31,32,39,40,87},40->{31,32,39,40,88},60->{0,61,62},61->{25,26,33,34} ,62->{31,32,39,40},83->{84}] ,We construct a looptree: P: [0,25,26,31,32,33,34,39,40,60,61,62,83,84,85,86,87,88,89,90,91,92] | +- p:[0] c: [0] | +- p:[31,32,39,40] c: [31,32,39,40] | `- p:[25,26,33,34] c: [25,26,33,34]) + Applied Processor: AbstractSize Minimize + Details: () * Step 9: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2,0.0,0.1,0.2] f16 ~> f16 [A <= A, B <= A, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f0 ~> f16 [A <= unknown, B <= 2*K, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f16 ~> f4 [A <= unknown, B <= unknown, J <= S, K <= K, L <= K, M <= 0*K, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= K + S, I2 <= I2] f16 ~> f4 [A <= unknown, B <= unknown, J <= S, K <= K, L <= K, M <= 0*K, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= K + S, I2 <= I2] f0 ~> f1 [A <= unknown, B <= unknown, J <= J, K <= unknown, L <= L, M <= M, S <= S, C1 <= C1, M1 <= unknown, N1 <= N1, O1 <= unknown, S1 <= unknown, W1 <= W1, C2 <= C2, I2 <= I2] f1 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> exitus616 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] + Loop: [0.0 <= K + A + B] f16 ~> f16 [A <= A, B <= A, J <= J, K <= K, L <= L, M <= M, S <= S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] + Loop: [0.1 <= S] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] + Loop: [0.2 <= S] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] f4 ~> f4 [A <= A, B <= B, J <= J, K <= K, L <= L, M <= K + M, S <= K + S, C1 <= C1, M1 <= M1, N1 <= N1, O1 <= O1, S1 <= S1, W1 <= W1, C2 <= C2, I2 <= I2] + Applied Processor: AbstractFlow + Details: () * Step 10: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,J,K,L,M,S,C1,M1,N1,O1,S1,W1,C2,I2,0.0,0.1,0.2] f16 ~> f16 [A ~=> B] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f0 ~> f16 [K ~=> B,huge ~=> A] f16 ~> f4 [K ~=> L,S ~=> J,K ~=> M,huge ~=> A,huge ~=> B,S ~+> C2,K ~+> C2] f16 ~> f4 [K ~=> L,S ~=> J,K ~=> M,huge ~=> A,huge ~=> B,S ~+> C2,K ~+> C2] f0 ~> f1 [huge ~=> A,huge ~=> B,huge ~=> K,huge ~=> M1,huge ~=> O1,huge ~=> S1] f1 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f16 ~> f16 [A ~=> B] + Loop: [S ~=> 0.1] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] + Loop: [S ~=> 0.2] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] f4 ~> f4 [M ~+> M,S ~+> S,K ~+> M,K ~+> S] + Applied Processor: Lare + Details: Unknown bound. MAYBE