MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. 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 -> f14(E,C2,E2,D,E,0,D,A2,D2,F2,G2,H2,I2,J2,C,C,D,C,T,T,B2,K2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 1. 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 -> f14(E,C2,E2,D,E,0,D,A2,D2,F2,G2,H2,I2,J2,C,C,D,C,T,T,B2,K2,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 2. 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 -> f7(1 + A,B,N,D,E,F,G,H,I,J,K,L,N,A2,O,P,Q,R,S,T,U,V,C2,A,T,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [B >= 1 + A && A >= 0] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 3. 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 -> f14(A,B,C,Q,E,1,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,1 + E,T,E2,F2,E,F1,G1,H1,I1,J1,K1,L1,M1,N1 [G2 >= 1 + R && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 4. 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 -> f14(A,B,C,Q,E,1,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,1 + E,T,E2,F2,E,F1,G1,H1,I1,J1,K1,L1,M1,N1 [G2 >= 1 + R && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 5. 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 -> f14(A,B,C,Q,E,1,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,1 + E,T,E2,F2,E,F1,G1,H1,I1,J1,K1,L1,M1,N1 [R >= 1 + G2 && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 6. 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 -> f14(A,B,C,Q,E,1,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,1 + E,T,E2,F2,E,F1,G1,H1,I1,J1,K1,L1,M1,N1 [R >= 1 + G2 && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 9. 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 10. 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 11. 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 12. 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 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 13. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 14. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f14(A,B,C,Q,E,F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,D2,E2,H1,I1,J1,K1,L1,M1,N1,O1 [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 16. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 17. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 18. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 19. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 20. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 21. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 22. 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 -> f14(A,B,C,Q,-1 + E,1 + F,Q,A2,I,J,K,L,M,N,C2,C2,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,R,E2,T,1 + F [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,-1 + E,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 23. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 24. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 25. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 26. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 27. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 28. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 29. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 30. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,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 [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 31. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f16(A,B,C,D,E,F,A2,C2,I,J,D2,L,M,N,E2,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,H2,N1,G2[N1 >= 0 && A2 >= 1 + E2 && C2 >= 2 && O1 = M1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,F2,I2,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 32. f4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f16(A,B,C,D,E,F,A2,C2,I,J,D2,L,M,N,E2,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,H2,N1,G2[N1 >= 0 && E2 >= 1 + A2 && C2 >= 2 && O1 = M1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,F2,I2,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 33. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 34. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 35. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 36. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 37. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 38. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 39. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 40. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f5(A,B,C,O1,E,F,O1,A2,I,J,K,L,M,N,C2,P,Q,R,S,T,U,V,W,X,Y,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,C2,M1,-1 + R1,T,-1 + R1,U1,V1,W1,X1,Y1,Z1) 41. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,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 -> f16(A,B,C,D,E,F,G,A2,I,J,C2,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,F2,N1,E2 [A2 >= 2 && R1 >= 0 && O1 = M1] (?,1) ,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D2,G2,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) 42. 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 -> f7(2,E2,F2,A2,E,F,A2,E2,A2,J,K,F2,F2,G2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [E2 >= 2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,N1,O1,P1,Q1,R1,S1,T1,C2,D2,H2,X1,Y1,Z1) 43. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && D >= 1 + O && Q = R && F = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,T,T,F2) 44. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && Q = R && F = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,T,T,F2) 45. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && Q = R && F = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,T,T,F2) 46. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && O >= 1 + D && Q = R && F = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,T,T,F2) 47. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && D >= 1 + O && Q = R] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,X1,T,F2) 48. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,X1,T,F2) 49. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,X1,T,F2) 50. 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 -> f5(A,B,C,D,E,1 + R1,D,A2,I,J,K,L,M,N,O,C2,D2,E2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,O,R1[G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && O >= 1 + D && Q = R] (?,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,D,O,O,R1,S1,T1,U1,V1,W1,X1,T,F2) 51. 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 -> f16(H2,E2,G2,U1,E,F,U1,D2,F2,I2,J2,B2,K2,O2,U1,P2,Q2,R2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1[0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,L1,U2,N1,T2,S2,V2,R1,S1,T1,A2,C2,W1,X1,Y1,Z1) 52. 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 -> f16(H2,E2,G2,N,E,F,A2,1,F2,I2,J2,B2,K2,O2,P2,Q2,R2,S2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 [0 >= 1 && A2 >= 1 + P2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,L1,V2,N1,U2,T2,L2,R1,S1,T1,C2,D2,W1,X1,Y1,Z1) 53. 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 -> f16(H2,E2,G2,N,E,F,A2,1,F2,I2,J2,B2,K2,O2,P2,Q2,R2,S2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 [0 >= 1 && P2 >= 1 + A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,L1,V2,N1,U2,T2,L2,R1,S1,T1,C2,D2,W1,X1,Y1,Z1) 54. 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 -> f16(H2,E2,G2,N,E,F,A2,1,F2,I2,J2,B2,K2,O2,P2,Q2,R2,S2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 [0 >= 1 && A2 >= 1 + P2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,L1,V2,N1,U2,T2,L2,R1,S1,T1,C2,D2,W1,X1,Y1,Z1) 55. 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 -> f16(H2,E2,G2,N,E,F,A2,1,F2,I2,J2,B2,K2,O2,P2,Q2,R2,S2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1 [0 >= 1 && P2 >= 1 + A2] (1,1) ,R1,S1,T1,U1,V1,W1,X1,Y1,Z1) ,L1,V2,N1,U2,T2,L2,R1,S1,T1,C2,D2,W1,X1,Y1,Z1) Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Flow Graph: [0->{15,16,17,18,19,20,21,22,47,48,49,50},1->{15,16,17,18,19,20,21,22,47,48,49,50},2->{0,1,2},3->{15,16,17 ,18,19,20,21,22,47,48,49,50},4->{15,16,17,18,19,20,21,22,47,48,49,50},5->{15,16,17,18,19,20,21,22,47,48,49 ,50},6->{15,16,17,18,19,20,21,22,47,48,49,50},7->{15,16,17,18,19,20,21,22,47,48,49,50},8->{15,16,17,18,19,20 ,21,22,47,48,49,50},9->{15,16,17,18,19,20,21,22,47,48,49,50},10->{15,16,17,18,19,20,21,22,47,48,49,50} ,11->{15,16,17,18,19,20,21,22,47,48,49,50},12->{15,16,17,18,19,20,21,22,47,48,49,50},13->{15,16,17,18,19,20 ,21,22,47,48,49,50},14->{15,16,17,18,19,20,21,22,47,48,49,50},15->{15,16,17,18,19,20,21,22,47,48,49,50} ,16->{15,16,17,18,19,20,21,22,47,48,49,50},17->{15,16,17,18,19,20,21,22,47,48,49,50},18->{15,16,17,18,19,20 ,21,22,47,48,49,50},19->{15,16,17,18,19,20,21,22,47,48,49,50},20->{15,16,17,18,19,20,21,22,47,48,49,50} ,21->{15,16,17,18,19,20,21,22,47,48,49,50},22->{15,16,17,18,19,20,21,22,47,48,49,50},23->{33,34,35,36,37,38 ,39,40,41},24->{33,34,35,36,37,38,39,40,41},25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40 ,41},27->{33,34,35,36,37,38,39,40,41},28->{33,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41} ,30->{33,34,35,36,37,38,39,40,41},31->{},32->{},33->{33,34,35,36,37,38,39,40,41},34->{33,34,35,36,37,38,39 ,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41} ,38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{33,34,35,36,37,38,39,40,41},41->{} ,42->{0,1,2},43->{33,34,35,36,37,38,39,40,41},44->{33,34,35,36,37,38,39,40,41},45->{33,34,35,36,37,38,39,40 ,41},46->{33,34,35,36,37,38,39,40,41},47->{33,34,35,36,37,38,39,40,41},48->{33,34,35,36,37,38,39,40,41} ,49->{33,34,35,36,37,38,39,40,41},50->{33,34,35,36,37,38,39,40,41},51->{},52->{},53->{},54->{},55->{}] + Applied Processor: ArgumentFilter [6,7,8,9,10,11,12,13,15,18,19,20,21,22,23,24,25,26,27,28,29,31,32,33,34,35,36,37,41,42,44,45,46,47,48,49,50,51] + Details: We remove following argument positions: [6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,15 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,26 ,27 ,28 ,29 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,41 ,42 ,44 ,45 ,46 ,47 ,48 ,49 ,50 ,51]. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 1. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 2. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 4. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 5. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 6. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 7. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 8. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 9. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 10. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 11. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 12. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 13. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 14. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 15. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 16. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 17. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 18. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 19. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 20. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 21. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 22. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 23. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 24. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 25. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 26. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 27. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 28. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 29. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 30. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 31. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && A2 >= 1 + E2 && C2 >= 2 && O1 = M1] (?,1) 32. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && E2 >= 1 + A2 && C2 >= 2 && O1 = M1] (?,1) 33. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 34. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 35. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 36. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 37. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 38. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 39. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 40. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 41. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] (?,1) 42. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] (1,1) 43. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && D >= 1 + O && Q = R && F = 1] (?,1) 44. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && Q = R && F = 1] (?,1) 45. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && Q = R && F = 1] (?,1) 46. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && O >= 1 + D && Q = R && F = 1] (?,1) 47. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && D >= 1 + O && Q = R] (?,1) 48. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] (?,1) 49. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] (?,1) 50. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && O >= 1 + D && Q = R] (?,1) 51. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] (1,1) 52. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 53. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) 54. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 55. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Flow Graph: [0->{15,16,17,18,19,20,21,22,47,48,49,50},1->{15,16,17,18,19,20,21,22,47,48,49,50},2->{0,1,2},3->{15,16,17 ,18,19,20,21,22,47,48,49,50},4->{15,16,17,18,19,20,21,22,47,48,49,50},5->{15,16,17,18,19,20,21,22,47,48,49 ,50},6->{15,16,17,18,19,20,21,22,47,48,49,50},7->{15,16,17,18,19,20,21,22,47,48,49,50},8->{15,16,17,18,19,20 ,21,22,47,48,49,50},9->{15,16,17,18,19,20,21,22,47,48,49,50},10->{15,16,17,18,19,20,21,22,47,48,49,50} ,11->{15,16,17,18,19,20,21,22,47,48,49,50},12->{15,16,17,18,19,20,21,22,47,48,49,50},13->{15,16,17,18,19,20 ,21,22,47,48,49,50},14->{15,16,17,18,19,20,21,22,47,48,49,50},15->{15,16,17,18,19,20,21,22,47,48,49,50} ,16->{15,16,17,18,19,20,21,22,47,48,49,50},17->{15,16,17,18,19,20,21,22,47,48,49,50},18->{15,16,17,18,19,20 ,21,22,47,48,49,50},19->{15,16,17,18,19,20,21,22,47,48,49,50},20->{15,16,17,18,19,20,21,22,47,48,49,50} ,21->{15,16,17,18,19,20,21,22,47,48,49,50},22->{15,16,17,18,19,20,21,22,47,48,49,50},23->{33,34,35,36,37,38 ,39,40,41},24->{33,34,35,36,37,38,39,40,41},25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40 ,41},27->{33,34,35,36,37,38,39,40,41},28->{33,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41} ,30->{33,34,35,36,37,38,39,40,41},31->{},32->{},33->{33,34,35,36,37,38,39,40,41},34->{33,34,35,36,37,38,39 ,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41} ,38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{33,34,35,36,37,38,39,40,41},41->{} ,42->{0,1,2},43->{33,34,35,36,37,38,39,40,41},44->{33,34,35,36,37,38,39,40,41},45->{33,34,35,36,37,38,39,40 ,41},46->{33,34,35,36,37,38,39,40,41},47->{33,34,35,36,37,38,39,40,41},48->{33,34,35,36,37,38,39,40,41} ,49->{33,34,35,36,37,38,39,40,41},50->{33,34,35,36,37,38,39,40,41},51->{},52->{},53->{},54->{},55->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [43,46,47,50] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 1. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 2. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 4. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 5. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 6. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 7. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 8. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 9. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 10. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 11. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 12. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 13. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 14. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 15. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 16. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 17. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 18. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 19. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 20. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 21. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 22. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 23. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 24. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 25. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 26. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 27. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 28. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 29. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 30. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 31. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && A2 >= 1 + E2 && C2 >= 2 && O1 = M1] (?,1) 32. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && E2 >= 1 + A2 && C2 >= 2 && O1 = M1] (?,1) 33. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 34. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 35. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 36. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 37. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 38. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 39. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 40. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 41. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] (?,1) 42. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] (1,1) 44. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && Q = R && F = 1] (?,1) 45. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && Q = R && F = 1] (?,1) 48. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] (?,1) 49. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] (?,1) 51. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] (1,1) 52. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 53. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) 54. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 55. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Flow Graph: [0->{15,16,17,18,19,20,21,22,48,49},1->{15,16,17,18,19,20,21,22,48,49},2->{0,1,2},3->{15,16,17,18,19,20,21 ,22,48,49},4->{15,16,17,18,19,20,21,22,48,49},5->{15,16,17,18,19,20,21,22,48,49},6->{15,16,17,18,19,20,21,22 ,48,49},7->{15,16,17,18,19,20,21,22,48,49},8->{15,16,17,18,19,20,21,22,48,49},9->{15,16,17,18,19,20,21,22,48 ,49},10->{15,16,17,18,19,20,21,22,48,49},11->{15,16,17,18,19,20,21,22,48,49},12->{15,16,17,18,19,20,21,22,48 ,49},13->{15,16,17,18,19,20,21,22,48,49},14->{15,16,17,18,19,20,21,22,48,49},15->{15,16,17,18,19,20,21,22,48 ,49},16->{15,16,17,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48 ,49},19->{15,16,17,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48 ,49},22->{15,16,17,18,19,20,21,22,48,49},23->{33,34,35,36,37,38,39,40,41},24->{33,34,35,36,37,38,39,40,41} ,25->{33,34,35,36,37,38,39,40,41},26->{33,34,35,36,37,38,39,40,41},27->{33,34,35,36,37,38,39,40,41},28->{33 ,34,35,36,37,38,39,40,41},29->{33,34,35,36,37,38,39,40,41},30->{33,34,35,36,37,38,39,40,41},31->{},32->{} ,33->{33,34,35,36,37,38,39,40,41},34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33 ,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36 ,37,38,39,40,41},40->{33,34,35,36,37,38,39,40,41},41->{},42->{0,1,2},44->{33,34,35,36,37,38,39,40,41} ,45->{33,34,35,36,37,38,39,40,41},48->{33,34,35,36,37,38,39,40,41},49->{33,34,35,36,37,38,39,40,41},51->{} ,52->{},53->{},54->{},55->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,48) ,(0,49) ,(1,48) ,(1,49) ,(3,49) ,(6,48) ,(7,49) ,(9,49) ,(12,48) ,(14,48) ,(23,40) ,(23,41) ,(30,33) ,(30,41) ,(33,40) ,(33,41) ,(40,33) ,(40,41) ,(44,33) ,(44,41) ,(45,40) ,(45,41) ,(48,33) ,(48,41) ,(49,40) ,(49,41)] * Step 4: UnreachableRules MAYBE + Considered Problem: Rules: 0. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 1. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 2. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 4. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [G2 >= 1 + R && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 5. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && C2 >= 1 + G2 && H2 >= A2 && F = 1] (?,1) 6. f9(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,1,C2,Q,R,E,M1,N1,O1,R1) [R >= 1 + G2 && A >= 0 && A2 >= 2 && G2 >= 1 + C2 && H2 >= A2 && F = 1] (?,1) 7. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 8. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 9. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 10. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + R && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 11. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 12. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && F2 >= 1 + E2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 13. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 14. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,E,F,C2,Q,R,E1,M1,N1,O1,R1) [R >= 1 + F2 && E2 >= 1 + F2 && E1 >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 15. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 16. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 17. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 18. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 19. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 20. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 21. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 22. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 23. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 24. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 25. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 26. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [D2 >= 1 + M1 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 27. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + D2] (?,1) 28. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && D2 >= 1 + C2] (?,1) 29. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + D2] (?,1) 30. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,R1) [M1 >= 1 + D2 && N1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && D2 >= 1 + C2] (?,1) 31. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && A2 >= 1 + E2 && C2 >= 2 && O1 = M1] (?,1) 32. f4(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,E2,Q,R,E1,H2,N1,G2,R1) [N1 >= 0 && E2 >= 1 + A2 && C2 >= 2 && O1 = M1] (?,1) 33. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 34. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 35. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 36. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 37. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 38. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 39. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 40. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 41. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] (?,1) 42. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] (1,1) 44. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && O >= 1 + D && Q = R && F = 1] (?,1) 45. f10(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E1 >= 0 && D >= 1 + O && Q = R && F = 1] (?,1) 48. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] (?,1) 49. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] (?,1) 51. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] (1,1) 52. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 53. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) 54. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 55. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Flow Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},3->{15,16,17,18,19,20,21,22,48} ,4->{15,16,17,18,19,20,21,22,48,49},5->{15,16,17,18,19,20,21,22,48,49},6->{15,16,17,18,19,20,21,22,49} ,7->{15,16,17,18,19,20,21,22,48},8->{15,16,17,18,19,20,21,22,48,49},9->{15,16,17,18,19,20,21,22,48},10->{15 ,16,17,18,19,20,21,22,48,49},11->{15,16,17,18,19,20,21,22,48,49},12->{15,16,17,18,19,20,21,22,49},13->{15,16 ,17,18,19,20,21,22,48,49},14->{15,16,17,18,19,20,21,22,49},15->{15,16,17,18,19,20,21,22,48,49},16->{15,16,17 ,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48,49},19->{15,16,17 ,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48,49},22->{15,16,17 ,18,19,20,21,22,48,49},23->{33,34,35,36,37,38,39},24->{33,34,35,36,37,38,39,40,41},25->{33,34,35,36,37,38,39 ,40,41},26->{33,34,35,36,37,38,39,40,41},27->{33,34,35,36,37,38,39,40,41},28->{33,34,35,36,37,38,39,40,41} ,29->{33,34,35,36,37,38,39,40,41},30->{34,35,36,37,38,39,40},31->{},32->{},33->{33,34,35,36,37,38,39} ,34->{33,34,35,36,37,38,39,40,41},35->{33,34,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33 ,34,35,36,37,38,39,40,41},38->{33,34,35,36,37,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37 ,38,39,40},41->{},42->{0,1,2},44->{34,35,36,37,38,39,40},45->{33,34,35,36,37,38,39},48->{34,35,36,37,38,39 ,40},49->{33,34,35,36,37,38,39},51->{},52->{},53->{},54->{},55->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,14 ,23 ,24 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,44 ,45] * Step 5: FromIts MAYBE + Considered Problem: Rules: 0. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 1. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] (?,1) 2. f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] (?,1) 15. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 16. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 17. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 18. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 19. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 20. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 21. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] (?,1) 22. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] (?,1) 33. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 34. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 35. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 36. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 37. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] (?,1) 38. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] (?,1) 39. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] (?,1) 40. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] (?,1) 41. f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] (?,1) 42. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] (1,1) 48. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] (?,1) 49. f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] (?,1) 51. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] (1,1) 52. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 53. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) 54. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] (1,1) 55. f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] (1,1) Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Flow Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,48,49} ,16->{15,16,17,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48,49} ,19->{15,16,17,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48,49} ,22->{15,16,17,18,19,20,21,22,48,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34 ,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37 ,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},48->{34,35,36 ,37,38,39,40},49->{33,34,35,36,37,38,39},51->{},52->{},53->{},54->{},55->{}] + Applied Processor: FromIts + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] Signature: {(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Rule Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,48,49} ,16->{15,16,17,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48,49} ,19->{15,16,17,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48,49} ,22->{15,16,17,18,19,20,21,22,48,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34 ,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37 ,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{},42->{0,1,2},48->{34,35,36 ,37,38,39,40},49->{33,34,35,36,37,38,39},51->{},52->{},53->{},54->{},55->{}] + Applied Processor: AddSinks + Details: () * Step 7: Decompose MAYBE + Considered Problem: Rules: f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True Signature: {(exitus616,14);(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Rule Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,48,49} ,16->{15,16,17,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48,49} ,19->{15,16,17,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48,49} ,22->{15,16,17,18,19,20,21,22,48,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34 ,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37 ,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{61,62,63,64},42->{0,1,2} ,48->{34,35,36,37,38,39,40},49->{33,34,35,36,37,38,39},51->{60},52->{59},53->{58},54->{57},55->{56}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,33,34,35,36,37,38,39,40,41,42,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64] | +- p:[2] c: [2] | +- p:[15,16,17,18,19,20,21,22] c: [15,16,17,18,19,20,21,22] | `- p:[34,33,35,36,37,38,39,40] c: [33,34,35,36,37,38,39,40] * Step 8: AbstractSize MAYBE + Considered Problem: (Rules: f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && C >= 1 + D && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(E,C2,E2,D,E,0,C,D,C,E1,M1,N1,O1,R1) [A >= B && A >= 0 && D >= 1 + C && A2 >= 2 && B2 >= A2 && E >= A2 && F = 0] f7(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(1 + A,B,N,D,E,F,O,Q,R,E1,M1,N1,O1,R1) [B >= 1 + A && A >= 0] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [F2 >= 1 + G2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && F2 >= 1 + E2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && C2 >= 1 + F2 && A2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f14(A,B,C,Q,-1 + E,1 + F,C2,Q,R,E1,M1,N1,O1,R1) [G2 >= 1 + F2 && E2 >= 1 + F2 && F >= 0 && E >= 0 && F2 >= 1 + C2 && A2 >= 2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [E2 >= 1 + M1 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && O1 >= 1 + C2 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && C2 >= 1 + E2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,O1,E,F,C2,Q,R,E1,M1,N1,O1,-1 + R1) [M1 >= 1 + E2 && R1 >= 0 && A2 >= 2 && C2 >= 1 + O1 && E2 >= 1 + C2] f5(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(A,B,C,D,E,F,O,Q,R,E1,F2,N1,E2,R1) [A2 >= 2 && R1 >= 0 && O1 = M1] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f7(2,E2,F2,A2,E,F,O,Q,R,E1,M1,N1,O1,R1) [E2 >= 2] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && O >= 1 + D && Q = R] f14(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f5(A,B,C,D,E,1 + R1,O,D2,E2,E1,O,R1,D,R1) [G2 >= 2 && A2 >= 2 && E >= 0 && F >= 0 && D >= 1 + O && Q = R] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,U1,E,F,U1,Q2,R2,E1,U2,N1,T2,R1) [0 >= L2 && 0 >= M2 && 0 >= D2 && 0 >= N2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && A2 >= 1 + P2] f15(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> f16(H2,E2,G2,N,E,F,P2,R2,S2,E1,V2,N1,U2,R1) [0 >= 1 && P2 >= 1 + A2] f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True f16(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) -> exitus616(A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1) True Signature: {(exitus616,14);(f10,52);(f14,52);(f15,52);(f16,52);(f4,52);(f5,52);(f7,52);(f9,52)} Rule Graph: [0->{15,16,17,18,19,20,21,22},1->{15,16,17,18,19,20,21,22},2->{0,1,2},15->{15,16,17,18,19,20,21,22,48,49} ,16->{15,16,17,18,19,20,21,22,48,49},17->{15,16,17,18,19,20,21,22,48,49},18->{15,16,17,18,19,20,21,22,48,49} ,19->{15,16,17,18,19,20,21,22,48,49},20->{15,16,17,18,19,20,21,22,48,49},21->{15,16,17,18,19,20,21,22,48,49} ,22->{15,16,17,18,19,20,21,22,48,49},33->{33,34,35,36,37,38,39},34->{33,34,35,36,37,38,39,40,41},35->{33,34 ,35,36,37,38,39,40,41},36->{33,34,35,36,37,38,39,40,41},37->{33,34,35,36,37,38,39,40,41},38->{33,34,35,36,37 ,38,39,40,41},39->{33,34,35,36,37,38,39,40,41},40->{34,35,36,37,38,39,40},41->{61,62,63,64},42->{0,1,2} ,48->{34,35,36,37,38,39,40},49->{33,34,35,36,37,38,39},51->{60},52->{59},53->{58},54->{57},55->{56}] ,We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,33,34,35,36,37,38,39,40,41,42,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64] | +- p:[2] c: [2] | +- p:[15,16,17,18,19,20,21,22] c: [15,16,17,18,19,20,21,22] | `- p:[34,33,35,36,37,38,39,40] c: [33,34,35,36,37,38,39,40]) + Applied Processor: AbstractSize Minimize + Details: () * Step 9: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1,0.0,0.1,0.2] f7 ~> f14 [A <= E, B <= unknown, C <= unknown, D <= D, E <= E, F <= 0*K, O <= C, Q <= D, R <= C, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f7 ~> f14 [A <= E, B <= unknown, C <= unknown, D <= D, E <= E, F <= 0*K, O <= C, Q <= D, R <= C, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f7 ~> f7 [A <= B, B <= B, C <= unknown, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= M1 + O1, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= M1 + O1, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f15 ~> f7 [A <= 2*K, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + R1, O <= O, Q <= unknown, R <= unknown, E1 <= E1, M1 <= O, N1 <= R1, O1 <= D, R1 <= R1] f14 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + R1, O <= O, Q <= unknown, R <= unknown, E1 <= E1, M1 <= O, N1 <= R1, O1 <= D, R1 <= R1] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= unknown, Q <= unknown, R <= unknown, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= unknown, Q <= unknown, R <= unknown, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= unknown, Q <= unknown, R <= unknown, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= unknown, Q <= unknown, R <= unknown, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= E, F <= F, O <= unknown, Q <= unknown, R <= unknown, E1 <= E1, M1 <= unknown, N1 <= N1, O1 <= unknown, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] + Loop: [0.0 <= K + A + B] f7 ~> f7 [A <= B, B <= B, C <= unknown, D <= D, E <= E, F <= F, O <= O, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] + Loop: [0.1 <= E] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= Q, E <= K + E, F <= K + F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= R1] + Loop: [0.2 <= R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= M1 + O1, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= unknown, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= O1, E <= E, F <= F, O <= M1 + O1, Q <= Q, R <= R, E1 <= E1, M1 <= M1, N1 <= N1, O1 <= O1, R1 <= K + R1] + Applied Processor: AbstractFlow + Details: () * Step 10: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,O,Q,R,E1,M1,N1,O1,R1,0.0,0.1,0.2] f7 ~> f14 [C ~=> O,C ~=> R,D ~=> Q,E ~=> A,K ~=> F,huge ~=> B,huge ~=> C] f7 ~> f14 [C ~=> O,C ~=> R,D ~=> Q,E ~=> A,K ~=> F,huge ~=> B,huge ~=> C] f7 ~> f7 [B ~=> A,huge ~=> C] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f5 ~> f5 [O1 ~=> D,M1 ~+> O,O1 ~+> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,M1 ~+> O,O1 ~+> O,R1 ~+> R1,K ~+> R1] f5 ~> f16 [huge ~=> M1,huge ~=> O1] f15 ~> f7 [K ~=> A,huge ~=> B,huge ~=> C,huge ~=> D] f14 ~> f5 [D ~=> O1,O ~=> M1,R1 ~=> N1,huge ~=> Q,huge ~=> R,R1 ~+> F,K ~+> F] f14 ~> f5 [D ~=> O1,O ~=> M1,R1 ~=> N1,huge ~=> Q,huge ~=> R,R1 ~+> F,K ~+> F] f15 ~> f16 [huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> M1 ,huge ~=> O ,huge ~=> O1 ,huge ~=> Q ,huge ~=> R] f15 ~> f16 [huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> M1 ,huge ~=> O ,huge ~=> O1 ,huge ~=> Q ,huge ~=> R] f15 ~> f16 [huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> M1 ,huge ~=> O ,huge ~=> O1 ,huge ~=> Q ,huge ~=> R] f15 ~> f16 [huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> M1 ,huge ~=> O ,huge ~=> O1 ,huge ~=> Q ,huge ~=> R] f15 ~> f16 [huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> M1 ,huge ~=> O ,huge ~=> O1 ,huge ~=> Q ,huge ~=> R] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f7 ~> f7 [B ~=> A,huge ~=> C] + Loop: [E ~=> 0.1] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] f14 ~> f14 [Q ~=> D,huge ~=> O,E ~+> E,F ~+> F,K ~+> E,K ~+> F] + Loop: [R1 ~=> 0.2] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,M1 ~+> O,O1 ~+> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,huge ~=> O,R1 ~+> R1,K ~+> R1] f5 ~> f5 [O1 ~=> D,M1 ~+> O,O1 ~+> O,R1 ~+> R1,K ~+> R1] + Applied Processor: Lare + Details: Unknown bound. MAYBE