YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. 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) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 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) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 2. 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) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. 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) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12,13,14},4->{5,6,7,8,9,10,11,12,13,14},5->{5,6,7,8,9,10 ,11,12,13,14},6->{5,6,7,8,9,10,11,12,13,14},7->{5,6,7,8,9,10,11,12,13,14},8->{5,6,7,8,9,10,11,12,13,14} ,9->{5,6,7,8,9,10,11,12,13,14},10->{5,6,7,8,9,10,11,12,13,14},11->{5,6,7,8,9,10,11,12,13,14},12->{5,6,7,8,9 ,10,11,12,13,14},13->{15,16,17,18,19,20,21,22,23},14->{15,16,17,18,19,20,21,22,23},15->{15,16,17,18,19,20,21 ,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23} ,19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19,20,21,22,23},21->{15,16,17,18,19,20,21,22,23},22->{15 ,16,17,18,19,20,21,22,23},23->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. 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) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 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) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 2. 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) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. 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) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12,13,14},4->{5,6,7,8,9,10,11,12,13,14},5->{5,6,7,8,9,10 ,11,12,13,14},6->{5,6,7,8,9,10,11,12,13,14},7->{5,6,7,8,9,10,11,12,13,14},8->{5,6,7,8,9,10,11,12,13,14} ,9->{5,6,7,8,9,10,11,12,13,14},10->{5,6,7,8,9,10,11,12,13,14},11->{5,6,7,8,9,10,11,12,13,14},12->{5,6,7,8,9 ,10,11,12,13,14},13->{15,16,17,18,19,20,21,22,23},14->{15,16,17,18,19,20,21,22,23},15->{15,16,17,18,19,20,21 ,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23} ,19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19,20,21,22,23},21->{15,16,17,18,19,20,21,22,23},22->{15 ,16,17,18,19,20,21,22,23},23->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,13) ,(3,14) ,(4,13) ,(4,14) ,(5,14) ,(6,14) ,(7,13) ,(8,13) ,(9,14) ,(10,14) ,(11,13) ,(12,13) ,(13,21) ,(13,23) ,(14,22) ,(14,23) ,(21,22) ,(21,23) ,(22,21) ,(22,23)] * Step 3: Looptree YES + Considered Problem: Rules: 0. 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) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 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) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,M1,R1) [O1 >= 2] (1,1) 2. 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) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 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) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. 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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. 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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. 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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. 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) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [-2 + F >= 0 (1,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12},4->{5,6,7,8,9,10,11,12},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] + Applied Processor: Looptree + 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] | +- p:[2] c: [2] | +- p:[5,6,7,8,9,10,11,12] c: [12] | | | `- p:[5,6,7,8,9,10,11] c: [11] | | | `- p:[5,6,7,8,9,10] c: [10] | | | `- p:[5,6,7,8,9] c: [9] | | | `- p:[5,6,7,8] c: [8] | | | `- p:[5,6,7] c: [7] | | | `- p:[5,6] c: [6] | | | `- p:[5] c: [5] | `- p:[15,16,17,18,19,20,21,22] c: [22] | `- p:[15,16,17,18,19,20,21] c: [21] | `- p:[15,16,17,18,19,20] c: [20] | `- p:[15,16,17,18,19] c: [19] | `- p:[15,16,17,18] c: [18] | `- p:[15,16,17] c: [17] | `- p:[15,16] c: [16] | `- p:[15] c: [15] YES