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