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