YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. 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 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,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 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. 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 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(A,B,C,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 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,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[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(A,B,C,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 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(A,B,C,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 -> 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,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(A,B,C,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 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(A,B,C,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 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. 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 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(A,B,C,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 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(A,B,C,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 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{2,10 ,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,2),(10,10),(10,11)] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. 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 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,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 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. 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 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(A,B,C,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 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,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[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(A,B,C,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 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(A,B,C,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 -> 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,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(A,B,C,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 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(A,B,C,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 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. 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 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(A,B,C,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 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(A,B,C,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 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{} ,11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0,1,5,6,9] * Step 3: FromIts YES + Considered Problem: Rules: 2. f116(A,B,C,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 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,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[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(A,B,C,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 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(A,B,C,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 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 10. f116(A,B,C,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 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(A,B,C,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 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f300(A ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,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,S1 ,T1,U1,V1,W1 ,X1) [F >= O && P = 1] 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 ,S1,T1,U1,V1,W1 ,X1) -> f1(A ,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1,W1 ,X1) [B >= 0 && Q >= 1 + B] 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 ,S1,T1,U1,V1,W1 ,X1) -> f116(A ,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 ,Q1,R1,S1,T1,U1,V1,W1 ,X1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8(A,B,C,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 ,S1,T1,U1,V1,W1 ,X1) -> f8(A ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1,N1,O1,P1 ,Q1,R1,S1,T1,U1,V1,W1 ,X1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8(A,B,C,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 ,S1,T1,U1,V1,W1 ,X1) -> f10(E2 ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1,Q1,R1,S1 ,T1,U1,V1,W1 ,X1) [E1 >= 0 && G1 = D1] f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f116(A ,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U,1 + C ,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1 ,X1) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f8(A ,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1,R1,S1 ,T1,U1,V1,W1 ,X1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f1(Z1 ,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,A2,Y1 ,D2,2,E2,V1,W1 ,X1) [Z1 >= 2 && S = W] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f10(F2 ,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1 ,Q1,G2,S1,T1,U1,V1,W1 ,X1) [0 >= F2] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f10(1 ,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1 ,G2,C2,L2,T1,U1,F2,G2 ,P2) [S = 0 && W = 0] Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Rule Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [2,3,4,7,8,10,11,12,13,14] | +- p:[3] c: [3] | `- p:[7] c: [7] * Step 5: CloseWith YES + Considered Problem: (Rules: f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f300(A ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,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,S1 ,T1,U1,V1,W1 ,X1) [F >= O && P = 1] 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 ,S1,T1,U1,V1,W1 ,X1) -> f1(A ,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 ,R1,S1,T1,U1,V1,W1 ,X1) [B >= 0 && Q >= 1 + B] 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 ,S1,T1,U1,V1,W1 ,X1) -> f116(A ,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1 ,Q1,R1,S1,T1,U1,V1,W1 ,X1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8(A,B,C,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 ,S1,T1,U1,V1,W1 ,X1) -> f8(A ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1,N1,O1,P1 ,Q1,R1,S1,T1,U1,V1,W1 ,X1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8(A,B,C,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 ,S1,T1,U1,V1,W1 ,X1) -> f10(E2 ,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1,Q1,R1,S1 ,T1,U1,V1,W1 ,X1) [E1 >= 0 && G1 = D1] f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f116(A ,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U,1 + C ,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1 ,X1) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116(A,B,C,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,S1,T1,U1,V1,W1 ,X1) -> f8(A ,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1,R1,S1 ,T1,U1,V1,W1 ,X1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f1(Z1 ,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,A2,Y1 ,D2,2,E2,V1,W1 ,X1) [Z1 >= 2 && S = W] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f10(F2 ,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1 ,Q1,G2,S1,T1,U1,V1,W1 ,X1) [0 >= F2] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 ,S1,T1,U1,V1,W1 ,X1) -> f10(1 ,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1 ,G2,C2,L2,T1,U1,F2,G2 ,P2) [S = 0 && W = 0] Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Rule Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] ,We construct a looptree: P: [2,3,4,7,8,10,11,12,13,14] | +- p:[3] c: [3] | `- p:[7] c: [7]) + Applied Processor: CloseWith True + Details: () YES