MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f29(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 -> f34(A,B,1,B4,D4,0,H,H,E4,1 + H,F4,G4,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 [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 1. f29(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 -> f29(A,-1 + B,C,B4,M,D4,G,H,I,J,K,E4,M,B,A,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 2. f30(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 -> f35(A,-1 + E4,1,B4,D4,F4,G,G,I,J,K,G4,M,N,O,E4,C4,-1 + E4,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 [B >= 1 && H >= 0 && B4 >= 2 && E4 >= 1 && G = H && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,K1,L1,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,N2,O2,P2,Q2,R2,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 3. f30(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 -> f34(A,B,2,B4,D4,0,G,-1 + G,I,J,K,E4,M,N,O,P,Q,R,M,F4,G4,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[B >= 1 && B4 >= 2 && G >= 0 && 1 + H = G && C = 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 4. f31(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 -> f35(A,-1 + B,1,B4,D4,E4,G,G,I,J,K,F4,M,N,O,P,Q,R,S,T,U,G4,B,I,G,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[B >= 1 && G >= 0 && B4 >= 2 && H = G && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 5. f31(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 -> f34(A,B,C,B4,D4,0,G,H,I,J,K,E4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,F4,G4,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 1 && B4 >= 2 && G >= 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 6. f32(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 -> f32(A,-1 + B,C,1,M,B4,G,H,I,J,K,D4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B,D1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [B >= 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 7. f34(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 -> f35(A,-1 + E4,C,B4,D4,F4,G,H,I,J,K,G4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E4,-1 + E4,G1,H1,I1,J1,K1 [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,L1,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,N2,O2,P2,Q2,R2,S2,T2,U2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 8. f34(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 -> f34(A,B,1 + C,B4,D4,0,G,-1 + H,E4,J,K,F4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,M,G4,1 + C,-1 + H[C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,K1,L1,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,N2,O2,P2,Q2,R2,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 9. f35(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 -> f35(A,-1 + B,C,B4,D4,E4,G,H,I,J,K,F4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,G4,B,C,H [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,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,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 10. f35(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 -> f34(A,B,1 + C,B4,D4,0,G,-1 + H,E4,J,K,F4,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,G4,L1[C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,M1,N1,M,C4,1 + C,-1 + H,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(1 + 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 [S1 >= 1 + A && A >= 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,P1,Q1,R1,S1,U1,B4,U1,D4,A,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f29(D4,B,C,B4,T1,F,G,H,I,J,K,L,T1,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[A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,B3,P1,Q1,R1,E4,F4,H4,C4,W1,X1,G4,I4,J4,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 13. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,1 + G2,B4,C2,E4,G,H,I,J,K,L,C2,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[G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,G2,H,F4,-1 + F4,H,G2,O2,P2,Q2,R2,S2,T2,U2,V2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 14. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,E4,1 + G2,B4,C2,F4,G,G4,I,J,K,L,D4,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 [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,G2,H,G4,L2,H,G2,-1 + C,G4,Q2,R2,S2,T2,U2,V2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 15. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,0,B4,C2,E4,G,F4,I,J,K,L,C2,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 [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,G2,J2,G4,-1 + G4,H,N2,O2,P2,-1 + F4,-1 + F4,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 16. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,C,B4,C2,E4,G,F4,I,J,K,L,C2,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 [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,G2,J2,F4,L2,H,N2,-1 + C,F4,-1 + G4,-1 + G4,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 17. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,F4,B4,C2,E4,G,H,I,J,K,L,C2,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 [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,-1 + F4,H,G4,-1 + G4,M2,-1 + F4,O2,P2,S2,R2,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 18. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,F4,B4,C2,E4,G,G4,I,J,K,L,C2,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[C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,-1 + F4,H,G4,L2,M2,-1 + F4,-1 + C,G4,S2,R2,S2,T2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 19. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,0,B4,C2,E4,G,1 + S2,I,J,K,L,C2,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[G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,F4,-1 + F4,M2,N2,O2,P2,S2,S2,S2,T2,U2,V2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,C,B4,C2,E4,G,F4,I,J,K,L,C2,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 [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,F4,L2,M2,N2,-1 + C,F4,S2,S2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,F4,B4,C2,E4,G,H,I,J,K,L,C2,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 [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,-1 + F4,H,G4,-1 + G4,M2,-1 + F4,O2,P2,Q2,R2,S2,U2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 22. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,F4,B4,C2,E4,G,G4,I,J,K,L,C2,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[C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,-1 + F4,H,G4,L2,M2,-1 + F4,-1 + C,G4,Q2,R2,S2,U2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,0,B4,C2,E4,G,F4,I,J,K,L,C2,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 [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,G4,-1 + G4,M2,N2,O2,P2,-1 + F4,-1 + F4,S2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 24. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(A,D4,C,B4,C2,E4,G,F4,I,J,K,L,C2,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 [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,F4,L2,M2,N2,-1 + C,F4,-1 + G4,-1 + G4,S2,U2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,U2,V2,W2,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 25. f11(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 -> f13(A,E4,C,B4,D4,F4,G,H,I,J,K,L,C2,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 [0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,G2,J2,K2,L2,H,1 + G2,O2,P2,Q2,R2,S2,T2,U2,G4 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + G4,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 26. f11(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 -> f13(A,F4,C,B4,E4,G4,G,C4,I,J,K,L,D4,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 [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,G2,C2,G2,J2,K2,L2,H,1 + G2,O2,P2,Q2,R2,S2,T2,U2,C4,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + N2,C4,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 27. f11(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 -> f13(A,E4,C,B4,D4,F4,G,H,I,J,K,L,D4,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 [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,G2,J2,K2,L2,H,1 + G2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,-1 + R2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 28. f11(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 -> f13(A,E4,C,B4,D4,F4,G,1 + S2,I,J,K,L,C2,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[0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,0,O2,P2,S2,R2,S2,T2,U2,G4 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + G4,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 29. f11(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 -> f13(A,E4,C,B4,D4,F4,G,G4,I,J,K,L,C2,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 [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,S2,R2,S2,T2,U2,G4,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + N2,G4,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 30. f11(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 -> f13(A,D4,C,B4,C2,E4,G,1 + S2,I,J,K,L,C2,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[0 >= D4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,S2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,-1 + R2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 31. f11(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 -> f13(A,D4,C,B4,C2,E4,G,H,I,J,K,L,C2,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 [0 >= D4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,C2,0,C2,G2,C2,I2,J2,K2,L2,M2,0,O2,P2,Q2,1 + U2,S2,U2,U2,F4 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + F4,X2,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 32. f11(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 -> f13(A,E4,C,B4,D4,F4,G,G4,I,J,K,L,D4,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 [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,1 + U2,S2,U2,U2,G4,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,-1 + N2,G4,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 33. f11(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 -> f13(A,E4,C,B4,D4,F4,G,H,I,J,K,L,D4,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 [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,1 + U2,S2,U2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,-1 + R2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 34. f11(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 -> f27(A,I4,C,B4,D4,J4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,K4,C4,H4,E4,F4,G4,G2,L4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 35. f12(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 -> f13(A,E4,C,B4,D4,F4,G,H,I,J,K,L,C2,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 [0 >= E4 && B4 >= 2 && B2 = 0 && I2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,0,J2,K2,L2,M2,N2,O2,P2,Q2,R2,-1 + H,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,G4,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 36. f12(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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,-1 + I2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,C4,H,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 37. f12(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 -> f13(A,E4,C,B4,D4,F4,G,H,I,J,K,L,D4,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 [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,T2,R2,S2,T2,-1 + T2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,G4,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 38. f12(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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,-1 + Q2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,D4,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 39. f12(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 -> f27(A,J4,C,B4,I4,K4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= J4 && B2 = C2 && Q2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,L4,C4,H4,E4,F4,G4,G2,D4,I2,J2,K2,L2,M2,N2,O2,P2,0,R2,S2,T2,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 40. f12(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 -> f27(A,I4,C,B4,D4,J4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= I4 && B2 = C2 && T2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,K4,C4,H4,E4,F4,G4,G2,L4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,0,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,0,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,-1 + H,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C4,H4,I4,J4,-1 + H,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,-1 + G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C4,H4,E3,F3,G3,I4,J4,H,-1 + G2,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f13(A,E4,C,B4,D4,F4,G,H,G4,J,K,L,D4,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 [B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,-1 + L3,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C4,H4,E3,F3,G3,H3,I3,J3,K3,L3,I4,-1 + L3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,-1 + S2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,D4,C4,E3,F3,G3,H3,I3,J3,K3,L3,M3,-1 + S2,H4,I4,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f13(A,F4,C,B4,E4,G4,G,H,I,J,K,L,D4,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 [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,E4,0,E4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,-1 + U2,V2,W2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,X2,Y2,Z2,A3,B3,C4,H4,E3,F3,G3,H3,I3,J3,K3,L3,M3,-1 + U2,O3,P3,I4,J4,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 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 -> f27(A,B,C,B4,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[B4 >= 2 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,H4,G4,C4,D4,E4,F4,G2,I4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 47. 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 -> f15(A,E4,C,B4,D4,0,G,H,I,J,K,L,0,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 [S3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 48. 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 -> f27(A,I4,C,B4,H4,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 [S3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,J4,G4,C4,D4,E4,F4,G2,K4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 49. f15(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 -> f15(A,E4,C,B4,D4,0,G,H,F4,J,K,L,0,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[T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,-1 + T3,-1 + T3,V3,W3,X3,Y3,Z3,A4) 50. f15(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 -> f27(A,I4,C,B4,H4,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 [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,J4,G4,C4,D4,E4,F4,G2,K4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 51. 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 -> f17(A,E4,C,B4,D4,F,G,H,I,J,K,L,D4,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[V3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 52. 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 -> f27(A,I4,C,B4,E,F,G,H,I,J,K,L,D4,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 [V3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,J4,C4,H4,E4,F4,G4,G2,K4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 53. f17(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 -> f17(A,E4,C,B4,D4,F,G,H,F4,J,K,L,D4,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 [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,C2,D4,0,D4,G2,C2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Y2,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,-1 + W3,-1 + W3,Y3,Z3,A4) 54. f17(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 -> f27(A,I4,C,B4,E,F,G,H,I,J,K,L,D4,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 [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,J4,C4,H4,E4,F4,G4,G2,K4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 55. f29(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 -> f17(A,D4,C,B4,E,F,G,H,I,J,K,L,E,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 [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,E,E,0,E,G2,E,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,W3,W3,X3,1 + W3,Z3,A4) 56. f30(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 -> f15(A,D4,1 + T3,B4,E,0,0,H,I,J,K,L,0,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[E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0 && G = 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,E,E,0,E,G2,E,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,T3,T3,U3,V3,W3,X3,Y3,Z3,A4) 57. f31(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 -> f10(A,E4,1,B4,E,F4,G,G,I,J,K,L,D4,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[0 >= B && H >= 0 && 0 >= E4 && B4 >= 2 && C = 1 && G = H] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,E,E,0,E,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 58. f34(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 -> f15(A,D4,1 + T3,B4,E,0,G,H,I,J,K,L,0,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[H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,E,E,0,E,G2,E,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,T3,T3,U3,V3,W3,X3,Y3,Z3,A4) 59. f35(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 -> f10(A,E4,C,B4,E,F4,G,H,I,J,K,L,D4,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[0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,0,E,E,0,E,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 60. f26(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(2,B,C,B4,E,F,G,H,I,J,K,D4,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[B4 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,Q1,R1,B4,E4,F4,E4,W1,X1,E4,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,G4,2) 61. f26(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 -> f32(B4,B,C,1,U1,F,G,H,I,J,K,D4,U1,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,O1True (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,E4,F4,H4,C4,W1,X1,G4,I4,J4,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 62. f26(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 -> f27(H4,B,C,B4,0,F,G,H,I,J,K,I4,0,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 [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,J4,K4,Q4,P4,W1,X1,L4,R4,S4,G4,C4,D4,E4,F4,G2,T4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 63. f32(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 -> f27(A,H4,C,1,0,F,G,H,I,J,K,L,B4,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 [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,I4,G4,C4,D4,E4,F4,G2,J4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) 64. f32(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 -> f27(A,H4,C,1,C4,0,G,H,I,J,K,I4,0,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 [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2,B2,C2,D2,E2,F2,G2,H2,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2,Z2,A3,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,J4,F4,G4,B4,D4,E4,G2,K4,I2,J2,K2,L2,M2,N2,O2,P2,Q2,R2,S2,T2,U2,V2,W2,X2,Y2 ,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) ,Z2,A3,B3,C3,D3,E3,F3,G3,H3,I3,J3,K3,L3,M3,N3,O3,P3,Q3,R3,S3,T3,U3,V3,W3,X3,Y3,Z3,A4) Signature: {(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Flow Graph: [0->{7,8,58},1->{0,1,55},2->{9,10,59},3->{7,8,58},4->{9,10,59},5->{7,8,58},6->{6,63,64},7->{9,10,59},8->{7 ,8,58},9->{9,10,59},10->{7,8,58},11->{11,12},12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46} ,15->{41,42,43,44,45,46},16->{41,42,43,44,45,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42 ,43,44,45,46},20->{41,42,43,44,45,46},21->{41,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45 ,46},24->{41,42,43,44,45,46},25->{41,42,43,44,45,46},26->{41,42,43,44,45,46},27->{41,42,43,44,45,46},28->{41 ,42,43,44,45,46},29->{41,42,43,44,45,46},30->{41,42,43,44,45,46},31->{41,42,43,44,45,46},32->{41,42,43,44,45 ,46},33->{41,42,43,44,45,46},34->{},35->{41,42,43,44,45,46},36->{41,42,43,44,45,46},37->{41,42,43,44,45,46} ,38->{41,42,43,44,45,46},39->{},40->{},41->{41,42,43,44,45,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45 ,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{},47->{49,50},48->{},49->{49,50},50->{},51->{53 ,54},52->{},53->{53,54},54->{},55->{53,54},56->{49,50},57->{13,14,15,16,17,18,19,20,21,22,23,24},58->{49,50} ,59->{13,14,15,16,17,18,19,20,21,22,23,24},60->{11,12},61->{6,63,64},62->{},63->{},64->{}] + Applied Processor: ArgumentFilter [3,5,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,45,46,47,48,49,50,51,52,55,56,57,59,61,62,63,64,66,67,69,70,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,98,101,102,103,104] + Details: We remove following argument positions: [3 ,5 ,8 ,9 ,10 ,11 ,13 ,14 ,15 ,16 ,17 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,38 ,39 ,40 ,41 ,42 ,43 ,45 ,46 ,47 ,48 ,49 ,50 ,51 ,52 ,55 ,56 ,57 ,59 ,61 ,62 ,63 ,64 ,66 ,67 ,69 ,70 ,72 ,73 ,74 ,75 ,76 ,77 ,78 ,79 ,80 ,81 ,82 ,83 ,84 ,85 ,86 ,87 ,88 ,89 ,90 ,91 ,92 ,93 ,94 ,95 ,98 ,101 ,102 ,103 ,104]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1,D4,H,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] (?,1) 1. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] (?,1) 2. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,1,D4,G,G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && H >= 0 && B4 >= 2 && E4 >= 1 && G = H && C = 1] (?,1) 3. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,2,D4,G,-1 + G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && B4 >= 2 && G >= 0 && 1 + H = G && C = 2] (?,1) 4. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,1,D4,G,G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && G >= 0 && B4 >= 2 && H = G && C = 1] (?,1) 5. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && B4 >= 2 && G >= 0] (?,1) 6. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1] (?,1) 7. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] (?,1) 8. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 9. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 10. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 11. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(1 + A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S1 >= 1 + A && A >= 0] (?,1) 12. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(D4,B,C,T1,G,H,T1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] (?,1) 13. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,1 + G2,C2,G,H,C2,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 14. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,1 + G2,C2,G,G4,D4,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 15. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + F4,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 16. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + G4,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 17. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 18. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 19. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 20. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 21. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 22. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 23. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + F4,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 24. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + G4,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 25. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,C2,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 26. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,C4,D4,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 27. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 28. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,1 + S2,C2,S1,0,C2,G2,I2,0,S2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 29. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,G4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 30. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 31. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,H,C2,S1,0,C2,G2,I2,0,Q2,U2,S3,T3,V3,W3) [0 >= D4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 32. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,G4,D4,S1,0,C2,G2,I2,N2,Q2,U2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 33. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,U2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 34. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,D4,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 35. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,C2,S1,0,C2,G2,0,N2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && I2 = 0] (?,1) 36. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + I2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 37. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,T2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 38. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 39. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,J4,C,I4,G,H,D4,S1,C4,H4,G2,I2,N2,0,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= J4 && B2 = C2 && Q2 = 0] (?,1) 40. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,D4,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,0,S3,T3,V3,W3) [B4 >= 2 && 0 >= I4 && B2 = C2 && T2 = 0] (?,1) 41. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,0,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] (?,1) 42. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 43. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 44. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 45. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 46. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,B,C,E,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && B2 = C2] (?,1) 47. f14(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) 48. f14(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) 49. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3,-1 + T3,V3,W3) [T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) 50. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) 51. f16(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [V3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 52. f16(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [V3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 53. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,-1 + W3) [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 54. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 55. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,D4,C,E,G,H,E,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,W3,W3) [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] (?,1) 56. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,0,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3,T3,V3,W3) [E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0 && G = 0 && C = 1] (?,1) 57. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,1,E,G,G,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && H >= 0 && 0 >= E4 && B4 >= 2 && C = 1 && G = H] (?,1) 58. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,G,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3,T3,V3,W3) [H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] (?,1) 59. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,C,E,G,H,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] (?,1) 60. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(2,B,C,E,G,H,M,B4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2] (1,1) 61. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(B4,B,C,U1,G,H,U1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) True (1,1) 62. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(H4,B,C,0,G,H,0,J4,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] (1,1) 63. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,0,G,H,B4,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] (?,1) 64. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,C4,G,H,0,S1,F4,G4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] (?,1) Signature: {(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Flow Graph: [0->{7,8,58},1->{0,1,55},2->{9,10,59},3->{7,8,58},4->{9,10,59},5->{7,8,58},6->{6,63,64},7->{9,10,59},8->{7 ,8,58},9->{9,10,59},10->{7,8,58},11->{11,12},12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46} ,15->{41,42,43,44,45,46},16->{41,42,43,44,45,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42 ,43,44,45,46},20->{41,42,43,44,45,46},21->{41,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45 ,46},24->{41,42,43,44,45,46},25->{41,42,43,44,45,46},26->{41,42,43,44,45,46},27->{41,42,43,44,45,46},28->{41 ,42,43,44,45,46},29->{41,42,43,44,45,46},30->{41,42,43,44,45,46},31->{41,42,43,44,45,46},32->{41,42,43,44,45 ,46},33->{41,42,43,44,45,46},34->{},35->{41,42,43,44,45,46},36->{41,42,43,44,45,46},37->{41,42,43,44,45,46} ,38->{41,42,43,44,45,46},39->{},40->{},41->{41,42,43,44,45,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45 ,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{},47->{49,50},48->{},49->{49,50},50->{},51->{53 ,54},52->{},53->{53,54},54->{},55->{53,54},56->{49,50},57->{13,14,15,16,17,18,19,20,21,22,23,24},58->{49,50} ,59->{13,14,15,16,17,18,19,20,21,22,23,24},60->{11,12},61->{6,63,64},62->{},63->{},64->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(57,13),(57,15),(57,17),(57,19),(57,21),(57,23)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1,D4,H,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] (?,1) 1. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] (?,1) 2. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,1,D4,G,G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && H >= 0 && B4 >= 2 && E4 >= 1 && G = H && C = 1] (?,1) 3. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,2,D4,G,-1 + G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && B4 >= 2 && G >= 0 && 1 + H = G && C = 2] (?,1) 4. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,1,D4,G,G,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && G >= 0 && B4 >= 2 && H = G && C = 1] (?,1) 5. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && B4 >= 2 && G >= 0] (?,1) 6. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1] (?,1) 7. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] (?,1) 8. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 9. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 10. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 11. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(1 + A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S1 >= 1 + A && A >= 0] (?,1) 12. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(D4,B,C,T1,G,H,T1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] (?,1) 13. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,1 + G2,C2,G,H,C2,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 14. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,1 + G2,C2,G,G4,D4,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 15. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + F4,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 16. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + G4,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 17. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 18. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 19. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 20. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 21. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 22. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 23. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + F4,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 24. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + G4,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 25. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,C2,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 26. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,C4,D4,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 27. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,G2,1 + G2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 28. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,1 + S2,C2,S1,0,C2,G2,I2,0,S2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 29. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,G4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 30. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 31. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,H,C2,S1,0,C2,G2,I2,0,Q2,U2,S3,T3,V3,W3) [0 >= D4 && B4 >= 2 && B2 = 0 && N2 = 0] (?,1) 32. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,G4,D4,S1,0,C2,G2,I2,N2,Q2,U2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 33. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,U2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 34. f11(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,D4,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 35. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,C2,S1,0,C2,G2,0,N2,Q2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0 && I2 = 0] (?,1) 36. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + I2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 37. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,T2,T2,S3,T3,V3,W3) [0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 38. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 39. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,J4,C,I4,G,H,D4,S1,C4,H4,G2,I2,N2,0,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= J4 && B2 = C2 && Q2 = 0] (?,1) 40. f12(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,D4,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,0,S3,T3,V3,W3) [B4 >= 2 && 0 >= I4 && B2 = C2 && T2 = 0] (?,1) 41. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,0,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] (?,1) 42. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 43. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 44. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 45. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 46. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,B,C,E,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && B2 = C2] (?,1) 47. f14(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) 48. f14(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) 49. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3,-1 + T3,V3,W3) [T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) 50. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) 51. f16(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [V3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 52. f16(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [V3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 53. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,-1 + W3) [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 54. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 55. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,D4,C,E,G,H,E,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,W3,W3) [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] (?,1) 56. f30(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,0,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3,T3,V3,W3) [E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0 && G = 0 && C = 1] (?,1) 57. f31(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,1,E,G,G,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && H >= 0 && 0 >= E4 && B4 >= 2 && C = 1 && G = H] (?,1) 58. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,G,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3,T3,V3,W3) [H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] (?,1) 59. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,C,E,G,H,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] (?,1) 60. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(2,B,C,E,G,H,M,B4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2] (1,1) 61. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(B4,B,C,U1,G,H,U1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) True (1,1) 62. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(H4,B,C,0,G,H,0,J4,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] (1,1) 63. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,0,G,H,B4,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] (?,1) 64. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,C4,G,H,0,S1,F4,G4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] (?,1) Signature: {(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Flow Graph: [0->{7,8,58},1->{0,1,55},2->{9,10,59},3->{7,8,58},4->{9,10,59},5->{7,8,58},6->{6,63,64},7->{9,10,59},8->{7 ,8,58},9->{9,10,59},10->{7,8,58},11->{11,12},12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46} ,15->{41,42,43,44,45,46},16->{41,42,43,44,45,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42 ,43,44,45,46},20->{41,42,43,44,45,46},21->{41,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45 ,46},24->{41,42,43,44,45,46},25->{41,42,43,44,45,46},26->{41,42,43,44,45,46},27->{41,42,43,44,45,46},28->{41 ,42,43,44,45,46},29->{41,42,43,44,45,46},30->{41,42,43,44,45,46},31->{41,42,43,44,45,46},32->{41,42,43,44,45 ,46},33->{41,42,43,44,45,46},34->{},35->{41,42,43,44,45,46},36->{41,42,43,44,45,46},37->{41,42,43,44,45,46} ,38->{41,42,43,44,45,46},39->{},40->{},41->{41,42,43,44,45,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45 ,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{},47->{49,50},48->{},49->{49,50},50->{},51->{53 ,54},52->{},53->{53,54},54->{},55->{53,54},56->{49,50},57->{14,16,18,20,22,24},58->{49,50},59->{13,14,15,16 ,17,18,19,20,21,22,23,24},60->{11,12},61->{6,63,64},62->{},63->{},64->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [2 ,3 ,4 ,5 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,38 ,39 ,40 ,47 ,48 ,51 ,52 ,56 ,57] * Step 4: FromIts MAYBE + Considered Problem: Rules: 0. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1,D4,H,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] (?,1) 1. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] (?,1) 6. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1] (?,1) 7. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] (?,1) 8. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 9. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 10. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] (?,1) 11. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(1 + A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [S1 >= 1 + A && A >= 0] (?,1) 12. f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(D4,B,C,T1,G,H,T1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] (?,1) 13. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,1 + G2,C2,G,H,C2,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 14. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,1 + G2,C2,G,G4,D4,S1,0,C2,G2,G2,G2,Q2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] (?,1) 15. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + F4,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 16. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + G4,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 17. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 18. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 19. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 20. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 21. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 22. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4,Q2,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 23. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + F4,U2,S3,T3,V3,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] (?,1) 24. f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + G4,U2,S3,T3,V3,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] (?,1) 41. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,0,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] (?,1) 42. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= F4 && B4 >= 2 && B2 = 0] (?,1) 43. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 44. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 45. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] (?,1) 46. f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,B,C,E,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2 && B2 = C2] (?,1) 49. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3,-1 + T3,V3,W3) [T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] (?,1) 50. f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] (?,1) 53. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3,V3,-1 + W3) [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] (?,1) 54. f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] (?,1) 55. f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,D4,C,E,G,H,E,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,W3,W3) [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] (?,1) 58. f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,G,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3,T3,V3,W3) [H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] (?,1) 59. f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,C,E,G,H,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] (?,1) 60. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(2,B,C,E,G,H,M,B4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B4 >= 2] (1,1) 61. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(B4,B,C,U1,G,H,U1,E4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) True (1,1) 62. f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(H4,B,C,0,G,H,0,J4,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] (1,1) 63. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,0,G,H,B4,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] (?,1) 64. f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,C4,G,H,0,S1,F4,G4,G2,I2,N2,Q2,T2,S3,T3,V3,W3) [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] (?,1) Signature: {(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Flow Graph: [0->{7,8,58},1->{0,1,55},6->{6,63,64},7->{9,10,59},8->{7,8,58},9->{9,10,59},10->{7,8,58},11->{11,12} ,12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46},15->{41,42,43,44,45,46},16->{41,42,43,44,45 ,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42,43,44,45,46},20->{41,42,43,44,45,46},21->{41 ,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45,46},24->{41,42,43,44,45,46},41->{41,42,43,44,45 ,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{} ,49->{49,50},50->{},53->{53,54},54->{},55->{53,54},58->{49,50},59->{13,14,15,16,17,18,19,20,21,22,23,24} ,60->{11,12},61->{6,63,64},62->{},63->{},64->{}] + Applied Processor: FromIts + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1,D4,H,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [B >= 1] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2 ,T2,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2 ,T2,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(1 + A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [S1 >= 1 + A && A >= 0] f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(D4,B,C,T1,G,H,T1,E4,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,1 + G2,C2,G,H,C2,S1,0,C2,G2,G2,G2,Q2,T2 ,S3,T3,V3 ,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,1 + G2,C2,G,G4,D4,S1,0,C2,G2,G2,G2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + F4,T2 ,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + G4,T2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,S2,T2,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,S2,T2,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2 ,S3,T3,V3 ,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3 ,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,Q2,U2,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,Q2,U2,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + F4,U2 ,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + G4,U2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,0,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [0 >= F4 && B4 >= 2 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= E4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,B,C,E,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && B2 = C2] f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3 ,-1 + T3,V3 ,W3) [T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,-1 + W3) [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,D4,C,E,G,H,E,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,W3 ,W3) [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,G,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3 ,T3,V3 ,W3) [H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,C,E,G,H,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(2,B,C,E,G,H,M,B4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3 ,W3) [B4 >= 2] f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(B4,B,C,U1,G,H,U1,E4,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) True f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(H4,B,C,0,G,H,0,J4,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,0,G,H,B4,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,C4,G,H,0,S1,F4,G4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] Signature: {(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Rule Graph: [0->{7,8,58},1->{0,1,55},6->{6,63,64},7->{9,10,59},8->{7,8,58},9->{9,10,59},10->{7,8,58},11->{11,12} ,12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46},15->{41,42,43,44,45,46},16->{41,42,43,44,45 ,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42,43,44,45,46},20->{41,42,43,44,45,46},21->{41 ,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45,46},24->{41,42,43,44,45,46},41->{41,42,43,44,45 ,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{} ,49->{49,50},50->{},53->{53,54},54->{},55->{53,54},58->{49,50},59->{13,14,15,16,17,18,19,20,21,22,23,24} ,60->{11,12},61->{6,63,64},62->{},63->{},64->{}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1,D4,H,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= 0 && B >= 1 && B4 >= 2 && C4 >= B4 && C = 1] f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= B4 && A >= 0 && B >= 1 && B4 >= 2] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(A,-1 + B,C,M,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [B >= 1] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + E4,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && E4 >= 1 && B4 >= 2] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2 ,T2,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f35(A,-1 + B,C,D4,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f34(A,B,1 + C,D4,G,-1 + H,M,S1,B2,C2,G2,I2,N2,Q2 ,T2,S3,T3,V3 ,W3) [C >= 0 && B >= 1 && H >= 0 && B4 >= 2] f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(1 + A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [S1 >= 1 + A && A >= 0] f1(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f29(D4,B,C,T1,G,H,T1,E4,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) [A >= S1 && A >= 0 && D4 >= B4 && B4 >= 2] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,1 + G2,C2,G,H,C2,S1,0,C2,G2,G2,G2,Q2,T2 ,S3,T3,V3 ,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,1 + G2,C2,G,G4,D4,S1,0,C2,G2,G2,G2,Q2,T2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= E4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + F4,T2 ,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,G2,N2,-1 + G4,T2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,S2,T2,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,S2,T2,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,1 + S2,C2,S1,0,C2,G2,I2,N2,S2,T2 ,S3,T3,V3 ,W3) [G4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,S2,T2,S3 ,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,H,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,Q2,U2,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,F4,C2,G,G4,C2,S1,0,C2,G2,-1 + F4,-1 + F4 ,Q2,U2,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,0,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + F4,U2 ,S3,T3,V3 ,W3) [C4 >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0 && C = 0] f10(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,D4,C,C2,G,F4,C2,S1,0,C2,G2,I2,N2,-1 + G4,U2 ,S3,T3,V3 ,W3) [C >= 0 && H >= 0 && 0 >= D4 && B4 >= 2 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,0,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0 && G2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,-1 + G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) [0 >= F4 && B4 >= 2 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= E4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f13(A,F4,C,E4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && 0 >= F4 && B2 = 0] f13(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,B,C,E,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B4 >= 2 && B2 = C2] f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,E4,C,D4,G,H,0,S1,0,C2,G2,I2,N2,Q2,T2,S3 ,-1 + T3,V3 ,W3) [T3 >= 0 && E4 >= 1 && B4 >= 2 && B2 = 0] f15(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,H4,G,H,M,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [T3 >= 0 && I4 >= 1 && B4 >= 2 && B2 = C2] f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,E4,C,D4,G,H,D4,S1,0,C2,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,-1 + W3) [W3 >= 0 && B4 >= 2 && 0 >= E4 && B2 = 0] f17(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,I4,C,E,G,H,D4,S1,C4,H4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [W3 >= 0 && B4 >= 2 && 0 >= I4 && B2 = C2] f29(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f17(A,D4,C,E,G,H,E,S1,0,E,G2,I2,N2,Q2,T2,S3,T3,W3 ,W3) [A >= E4 && A >= 0 && 0 >= B && F4 >= B4 && 0 >= G4 && E4 >= 2 && 0 >= D4 && B4 >= 2] f34(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f15(A,D4,1 + T3,E,G,H,0,S1,0,E,G2,I2,N2,Q2,T2,T3 ,T3,V3 ,W3) [H >= 0 && C >= 0 && E4 >= 1 && F4 >= 2 && D4 >= 1 && B4 >= 2 && M = 0] f35(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f10(A,E4,C,E,G,H,D4,S1,0,E,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= B && H >= 0 && C >= 0 && B4 >= 2 && 0 >= E4] f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f1(2,B,C,E,G,H,M,B4,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3 ,W3) [B4 >= 2] f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f32(B4,B,C,U1,G,H,U1,E4,B2,C2,G2,I2,N2,Q2,T2,S3 ,T3,V3 ,W3) True f26(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(H4,B,C,0,G,H,0,J4,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= M4 && 0 >= N4 && 0 >= B4 && 0 >= O4] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,0,G,H,B4,S1,G4,C4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [0 >= B && 0 >= K4 && 0 >= H4 && 0 >= L4 && E = 0] f32(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> f27(A,H4,C,C4,G,H,0,S1,F4,G4,G2,I2,N2,Q2,T2,S3,T3 ,V3 ,W3) [B >= 1 && L4 >= 1 && H4 >= 1 && P4 >= 1 && M = 0] f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True f27(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2,S3,T3,V3,W3) -> exitus616(A,B,C,E,G,H,M,S1,B2,C2,G2,I2,N2,Q2,T2 ,S3,T3,V3 ,W3) True Signature: {(exitus616,19) ;(f1,105) ;(f10,105) ;(f11,105) ;(f12,105) ;(f13,105) ;(f14,105) ;(f15,105) ;(f16,105) ;(f17,105) ;(f26,105) ;(f27,105) ;(f29,105) ;(f30,105) ;(f31,105) ;(f32,105) ;(f34,105) ;(f35,105)} Rule Graph: [0->{7,8,58},1->{0,1,55},6->{6,63,64},7->{9,10,59},8->{7,8,58},9->{9,10,59},10->{7,8,58},11->{11,12} ,12->{0,1,55},13->{41,42,43,44,45,46},14->{41,42,43,44,45,46},15->{41,42,43,44,45,46},16->{41,42,43,44,45 ,46},17->{41,42,43,44,45,46},18->{41,42,43,44,45,46},19->{41,42,43,44,45,46},20->{41,42,43,44,45,46},21->{41 ,42,43,44,45,46},22->{41,42,43,44,45,46},23->{41,42,43,44,45,46},24->{41,42,43,44,45,46},41->{41,42,43,44,45 ,46},42->{41,42,43,44,45,46},43->{41,42,43,44,45,46},44->{41,42,43,44,45,46},45->{41,42,43,44,45,46},46->{69 ,70,71,72,73,74,75,76,77,78,79,80},49->{49,50},50->{81},53->{53,54},54->{68},55->{53,54},58->{49,50},59->{13 ,14,15,16,17,18,19,20,21,22,23,24},60->{11,12},61->{6,63,64},62->{65},63->{67},64->{66}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,41,42,43,44,45,46,49,50,53,54,55,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81] | +- p:[11] c: [11] | +- p:[6] c: [6] | +- p:[1] c: [1] | +- p:[53] c: [53] | +- p:[7,8,10,9] c: [7,8,10] | | | `- p:[9] c: [9] | +- p:[41,42,43,44,45] c: [] | `- p:[49] c: [49] MAYBE