MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (?,1) 18. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (?,1) 19. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (?,1) 20. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (?,1) 21. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (?,1) 22. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (?,1) 23. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (?,1) 24. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (?,1) 25. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && U1 >= 1 && Z = X] (?,1) 26. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && 0 >= 1 + U1 && Z = X] (?,1) 27. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && U1 >= 1 && Z = X] (?,1) 28. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && 0 >= 1 + U1 && Z = X] (?,1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (?,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (?,1) ,M1,N1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && M >= 1 + K && 1 + I = Q && R = 0 && L = H] (?,1) ,M1,0) 47. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (?,1) ,M1,0) 48. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (?,1) ,M1,0) 49. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && K >= 1 + M && 1 + I = Q && R = 0 && L = H] (?,1) ,M1,0) 50. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && M >= 1 + K && L = H] (?,1) ,J1,K1,L1,M1,0) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 53. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && K >= 1 + M && L = H] (?,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) Signature: {(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45},1->{9,10,11,12,13,14,15,16,50,51,52,53},2->{9,10,11,12,13,14,15,16,50,51,52,53} ,3->{9,10,11,12,13,14,15,16,50,51,52,53},4->{9,10,11,12,13,14,15,16,50,51,52,53},5->{9,10,11,12,13,14,15,16 ,50,51,52,53},6->{9,10,11,12,13,14,15,16,50,51,52,53},7->{9,10,11,12,13,14,15,16,50,51,52,53},8->{9,10,11,12 ,13,14,15,16,50,51,52,53},9->{9,10,11,12,13,14,15,16,50,51,52,53},10->{9,10,11,12,13,14,15,16,50,51,52,53} ,11->{9,10,11,12,13,14,15,16,50,51,52,53},12->{9,10,11,12,13,14,15,16,50,51,52,53},13->{9,10,11,12,13,14,15 ,16,50,51,52,53},14->{9,10,11,12,13,14,15,16,50,51,52,53},15->{9,10,11,12,13,14,15,16,50,51,52,53},16->{9,10 ,11,12,13,14,15,16,50,51,52,53},17->{29,30,31,32,33,34,35,36,37,38},18->{29,30,31,32,33,34,35,36,37,38} ,19->{29,30,31,32,33,34,35,36,37,38},20->{29,30,31,32,33,34,35,36,37,38},21->{29,30,31,32,33,34,35,36,37,38} ,22->{29,30,31,32,33,34,35,36,37,38},23->{29,30,31,32,33,34,35,36,37,38},24->{29,30,31,32,33,34,35,36,37,38} ,25->{},26->{},27->{},28->{},29->{29,30,31,32,33,34,35,36,37,38},30->{29,30,31,32,33,34,35,36,37,38},31->{29 ,30,31,32,33,34,35,36,37,38},32->{29,30,31,32,33,34,35,36,37,38},33->{29,30,31,32,33,34,35,36,37,38},34->{29 ,30,31,32,33,34,35,36,37,38},35->{29,30,31,32,33,34,35,36,37,38},36->{29,30,31,32,33,34,35,36,37,38},37->{} ,38->{},39->{0,40,41,42,43,45},40->{9,10,11,12,13,14,15,16,50,51,52,53},41->{9,10,11,12,13,14,15,16,50,51,52 ,53},42->{9,10,11,12,13,14,15,16,50,51,52,53},43->{9,10,11,12,13,14,15,16,50,51,52,53},44->{},45->{},46->{29 ,30,31,32,33,34,35,36,37,38},47->{29,30,31,32,33,34,35,36,37,38},48->{29,30,31,32,33,34,35,36,37,38},49->{29 ,30,31,32,33,34,35,36,37,38},50->{29,30,31,32,33,34,35,36,37,38},51->{29,30,31,32,33,34,35,36,37,38},52->{29 ,30,31,32,33,34,35,36,37,38},53->{29,30,31,32,33,34,35,36,37,38},54->{},55->{},56->{},57->{},58->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (1,1) 18. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (1,1) 19. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (1,1) 20. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (1,1) 21. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (1,1) 22. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (1,1) 23. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (1,1) 24. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (1,1) 25. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && U1 >= 1 && Z = X] (1,1) 26. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && 0 >= 1 + U1 && Z = X] (1,1) 27. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && U1 >= 1 && Z = X] (1,1) 28. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && 0 >= 1 + U1 && Z = X] (1,1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (1,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (1,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (1,1) ,M1,N1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && M >= 1 + K && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 47. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 48. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 49. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && K >= 1 + M && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 50. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && M >= 1 + K && L = H] (1,1) ,J1,K1,L1,M1,0) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 53. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && K >= 1 + M && L = H] (1,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) Signature: {(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45},1->{9,10,11,12,13,14,15,16,50,51,52,53},2->{9,10,11,12,13,14,15,16,50,51,52,53} ,3->{9,10,11,12,13,14,15,16,50,51,52,53},4->{9,10,11,12,13,14,15,16,50,51,52,53},5->{9,10,11,12,13,14,15,16 ,50,51,52,53},6->{9,10,11,12,13,14,15,16,50,51,52,53},7->{9,10,11,12,13,14,15,16,50,51,52,53},8->{9,10,11,12 ,13,14,15,16,50,51,52,53},9->{9,10,11,12,13,14,15,16,50,51,52,53},10->{9,10,11,12,13,14,15,16,50,51,52,53} ,11->{9,10,11,12,13,14,15,16,50,51,52,53},12->{9,10,11,12,13,14,15,16,50,51,52,53},13->{9,10,11,12,13,14,15 ,16,50,51,52,53},14->{9,10,11,12,13,14,15,16,50,51,52,53},15->{9,10,11,12,13,14,15,16,50,51,52,53},16->{9,10 ,11,12,13,14,15,16,50,51,52,53},17->{29,30,31,32,33,34,35,36,37,38},18->{29,30,31,32,33,34,35,36,37,38} ,19->{29,30,31,32,33,34,35,36,37,38},20->{29,30,31,32,33,34,35,36,37,38},21->{29,30,31,32,33,34,35,36,37,38} ,22->{29,30,31,32,33,34,35,36,37,38},23->{29,30,31,32,33,34,35,36,37,38},24->{29,30,31,32,33,34,35,36,37,38} ,25->{},26->{},27->{},28->{},29->{29,30,31,32,33,34,35,36,37,38},30->{29,30,31,32,33,34,35,36,37,38},31->{29 ,30,31,32,33,34,35,36,37,38},32->{29,30,31,32,33,34,35,36,37,38},33->{29,30,31,32,33,34,35,36,37,38},34->{29 ,30,31,32,33,34,35,36,37,38},35->{29,30,31,32,33,34,35,36,37,38},36->{29,30,31,32,33,34,35,36,37,38},37->{} ,38->{},39->{0,40,41,42,43,45},40->{9,10,11,12,13,14,15,16,50,51,52,53},41->{9,10,11,12,13,14,15,16,50,51,52 ,53},42->{9,10,11,12,13,14,15,16,50,51,52,53},43->{9,10,11,12,13,14,15,16,50,51,52,53},44->{},45->{},46->{29 ,30,31,32,33,34,35,36,37,38},47->{29,30,31,32,33,34,35,36,37,38},48->{29,30,31,32,33,34,35,36,37,38},49->{29 ,30,31,32,33,34,35,36,37,38},50->{29,30,31,32,33,34,35,36,37,38},51->{29,30,31,32,33,34,35,36,37,38},52->{29 ,30,31,32,33,34,35,36,37,38},53->{29,30,31,32,33,34,35,36,37,38},54->{},55->{},56->{},57->{},58->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,50) ,(1,51) ,(1,53) ,(2,50) ,(2,53) ,(3,50) ,(3,51) ,(3,53) ,(4,50) ,(4,53) ,(5,50) ,(5,53) ,(6,50) ,(6,52) ,(6,53) ,(7,50) ,(7,53) ,(8,50) ,(8,52) ,(8,53) ,(9,50) ,(9,53) ,(10,50) ,(10,53) ,(11,50) ,(11,53) ,(12,50) ,(12,53) ,(13,50) ,(13,53) ,(14,50) ,(14,53) ,(15,50) ,(15,53) ,(16,50) ,(16,53) ,(17,36) ,(17,37) ,(17,38) ,(24,29) ,(24,37) ,(24,38) ,(29,36) ,(29,37) ,(29,38) ,(36,29) ,(36,37) ,(36,38) ,(40,50) ,(40,51) ,(40,52) ,(40,53) ,(41,50) ,(41,51) ,(41,52) ,(41,53) ,(42,50) ,(42,51) ,(42,52) ,(42,53) ,(43,50) ,(43,51) ,(43,52) ,(43,53) ,(46,29) ,(46,30) ,(46,31) ,(46,32) ,(46,33) ,(46,34) ,(46,35) ,(46,36) ,(46,37) ,(46,38) ,(47,36) ,(47,37) ,(47,38) ,(48,29) ,(48,37) ,(48,38) ,(49,29) ,(49,30) ,(49,31) ,(49,32) ,(49,33) ,(49,34) ,(49,35) ,(49,36) ,(49,37) ,(49,38) ,(50,29) ,(50,30) ,(50,31) ,(50,32) ,(50,33) ,(50,34) ,(50,35) ,(50,36) ,(50,37) ,(50,38) ,(51,36) ,(51,37) ,(51,38) ,(52,29) ,(52,37) ,(52,38) ,(53,29) ,(53,30) ,(53,31) ,(53,32) ,(53,33) ,(53,34) ,(53,35) ,(53,36) ,(53,37) ,(53,38)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 4. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Q1 >= 1 + H && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 5. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 6. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && Q1 >= 1 + R1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 7. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && P1 >= 1 + Q1 && O1 >= 2] (1,1) 8. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,S1,R1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [H >= 1 + Q1 && R1 >= 1 + Q1 && I >= 0 && Q1 >= 1 + P1 && O1 >= 2] (1,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (1,1) 18. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (1,1) 19. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (1,1) 20. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [S1 >= 1 + X && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (1,1) 21. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + S1] (1,1) 22. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && Z >= 1 + P1 && S1 >= 1 + P1] (1,1) 23. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + S1] (1,1) 24. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,P1,X,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [X >= 1 + S1 && Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + Z && S1 >= 1 + P1] (1,1) 25. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && U1 >= 1 && Z = X] (1,1) 26. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && P1 >= 1 + R1 && 0 >= 1 + U1 && Z = X] (1,1) 27. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && U1 >= 1 && Z = X] (1,1) 28. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(A,B,C,D,E,F,G,H,I,O1,P1,L,R1,N,O,P,Q,R,S,T,U,V,W,V1,Y,T1,Q1,W1,S1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [Y >= 0 && R >= 0 && O1 >= 2 && R1 >= 1 + P1 && 0 >= 1 + U1 && Z = X] (1,1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (1,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (1,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (1,1) ,M1,N1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && M >= 1 + K && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 47. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 48. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 49. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,-1 + Q,O1,K,S1,M,P1,O,P,1 + D1,0,S,T,U,V,W,M,D1,K,M,M,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 1 && K >= 1 + M && 1 + I = Q && R = 0 && L = H] (1,1) ,M1,0) 50. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && M >= 1 + K && L = H] (1,1) ,J1,K1,L1,M1,0) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 53. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && K >= 1 + M && L = H] (1,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) Signature: {(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45},1->{9,10,11,12,13,14,15,16,52},2->{9,10,11,12,13,14,15,16,51,52},3->{9,10,11,12,13 ,14,15,16,52},4->{9,10,11,12,13,14,15,16,51,52},5->{9,10,11,12,13,14,15,16,51,52},6->{9,10,11,12,13,14,15,16 ,51},7->{9,10,11,12,13,14,15,16,51,52},8->{9,10,11,12,13,14,15,16,51},9->{9,10,11,12,13,14,15,16,51,52} ,10->{9,10,11,12,13,14,15,16,51,52},11->{9,10,11,12,13,14,15,16,51,52},12->{9,10,11,12,13,14,15,16,51,52} ,13->{9,10,11,12,13,14,15,16,51,52},14->{9,10,11,12,13,14,15,16,51,52},15->{9,10,11,12,13,14,15,16,51,52} ,16->{9,10,11,12,13,14,15,16,51,52},17->{29,30,31,32,33,34,35},18->{29,30,31,32,33,34,35,36,37,38},19->{29 ,30,31,32,33,34,35,36,37,38},20->{29,30,31,32,33,34,35,36,37,38},21->{29,30,31,32,33,34,35,36,37,38},22->{29 ,30,31,32,33,34,35,36,37,38},23->{29,30,31,32,33,34,35,36,37,38},24->{30,31,32,33,34,35,36},25->{},26->{} ,27->{},28->{},29->{29,30,31,32,33,34,35},30->{29,30,31,32,33,34,35,36,37,38},31->{29,30,31,32,33,34,35,36 ,37,38},32->{29,30,31,32,33,34,35,36,37,38},33->{29,30,31,32,33,34,35,36,37,38},34->{29,30,31,32,33,34,35,36 ,37,38},35->{29,30,31,32,33,34,35,36,37,38},36->{30,31,32,33,34,35,36},37->{},38->{},39->{0,40,41,42,43,45} ,40->{9,10,11,12,13,14,15,16},41->{9,10,11,12,13,14,15,16},42->{9,10,11,12,13,14,15,16},43->{9,10,11,12,13 ,14,15,16},44->{},45->{},46->{},47->{29,30,31,32,33,34,35},48->{30,31,32,33,34,35,36},49->{},50->{},51->{29 ,30,31,32,33,34,35},52->{30,31,32,33,34,35,36},53->{},54->{},55->{},56->{},57->{},58->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ,17 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,26 ,27 ,28 ,46 ,47 ,48 ,49 ,50 ,53] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (1,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (1,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (1,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (1,1) ,M1,N1) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (1,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) Signature: {(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45},9->{9,10,11,12,13,14,15,16,51,52},10->{9,10,11,12,13,14,15,16,51,52},11->{9,10,11 ,12,13,14,15,16,51,52},12->{9,10,11,12,13,14,15,16,51,52},13->{9,10,11,12,13,14,15,16,51,52},14->{9,10,11,12 ,13,14,15,16,51,52},15->{9,10,11,12,13,14,15,16,51,52},16->{9,10,11,12,13,14,15,16,51,52},29->{29,30,31,32 ,33,34,35},30->{29,30,31,32,33,34,35,36,37,38},31->{29,30,31,32,33,34,35,36,37,38},32->{29,30,31,32,33,34,35 ,36,37,38},33->{29,30,31,32,33,34,35,36,37,38},34->{29,30,31,32,33,34,35,36,37,38},35->{29,30,31,32,33,34,35 ,36,37,38},36->{30,31,32,33,34,35,36},37->{},38->{},39->{0,40,41,42,43,45},40->{9,10,11,12,13,14,15,16} ,41->{9,10,11,12,13,14,15,16},42->{9,10,11,12,13,14,15,16},43->{9,10,11,12,13,14,15,16},44->{},45->{} ,51->{29,30,31,32,33,34,35},52->{30,31,32,33,34,35,36},54->{},55->{},56->{},57->{},58->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (?,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (?,1) ,M1,N1) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 59. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (1,1) ,N1) 60. 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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (?,1) ,N1) 61. 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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (?,1) ,N1) Signature: {(exitus616,40);(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45,60},9->{9,10,11,12,13,14,15,16,51,52},10->{9,10,11,12,13,14,15,16,51,52},11->{9,10 ,11,12,13,14,15,16,51,52},12->{9,10,11,12,13,14,15,16,51,52},13->{9,10,11,12,13,14,15,16,51,52},14->{9,10,11 ,12,13,14,15,16,51,52},15->{9,10,11,12,13,14,15,16,51,52},16->{9,10,11,12,13,14,15,16,51,52},29->{29,30,31 ,32,33,34,35,36,37,38,61},30->{29,30,31,32,33,34,35,36,37,38,61},31->{29,30,31,32,33,34,35,36,37,38,61} ,32->{29,30,31,32,33,34,35,36,37,38,61},33->{29,30,31,32,33,34,35,36,37,38,61},34->{29,30,31,32,33,34,35,36 ,37,38,61},35->{29,30,31,32,33,34,35,36,37,38,61},36->{29,30,31,32,33,34,35,36,37,38,61},37->{},38->{} ,39->{0,40,41,42,43,45,60},40->{9,10,11,12,13,14,15,16,51,52},41->{9,10,11,12,13,14,15,16,51,52},42->{9,10 ,11,12,13,14,15,16,51,52},43->{9,10,11,12,13,14,15,16,51,52},44->{},45->{},51->{29,30,31,32,33,34,35,36,37 ,38,61},52->{29,30,31,32,33,34,35,36,37,38,61},54->{},55->{},56->{},57->{},58->{},59->{},60->{},61->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(29,36) ,(29,37) ,(29,38) ,(36,29) ,(36,37) ,(36,38) ,(40,51) ,(40,52) ,(41,51) ,(41,52) ,(42,51) ,(42,52) ,(43,51) ,(43,52) ,(51,36) ,(51,37) ,(51,38) ,(52,29) ,(52,37) ,(52,38)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f9(A,1 + B,D,O1,D,P1,B,H,I,J,K,L,M,N,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) [A >= 1 + B && B >= 0] (?,1) 9. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 10. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 11. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 12. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [Q1 >= 1 + T1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 13. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 14. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && Q1 >= 1 + R1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 15. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && P1 >= 1 + Q1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 16. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f16(A,B,C,D,E,F,G,H,I,O1,L,L,P1,P1,O,P,1 + Q,-1 + R,S1,H,R1,1 + Q,-1 + R,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1 [T1 >= 1 + Q1 && R1 >= 1 + Q1 && Q >= 0 && R >= 0 && Q1 >= 1 + P1 && O1 >= 2] (?,1) ,I1,J1,K1,L1,M1,N1) 29. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 30. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 31. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 32. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [R1 >= 1 + X && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 33. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 34. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && Z >= 1 + P1 && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 35. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && P1 >= 1 + R1] (?,1) ,K1,L1,M1,N1) 36. 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) -> f7(A,B,C,D,E,F,G,H,I,O1,Z,L,P1,N,O,P,Q,0,S1,T,U,V,W,X,Y,Z,P1,X,C1,-1 + D1 + R,0,-1 + D1 + R,G1,H1,I1,J1 [X >= 1 + R1 && D1 >= 0 && Q1 >= 0 && O1 >= 2 && P1 >= 1 + Z && R1 >= 1 + P1] (?,1) ,K1,L1,M1,N1) 37. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && V1 >= 1 && O1 >= 2 && Z = X] (?,1) 38. 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) -> f18(A,B,C,D,E,F,G,H,I,O1,K,L,M,N,O,P,Q,R,S,T,U,V,W,Q1,Y,R1,S1,T1,P1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) [D1 >= 0 && R >= 0 && 0 >= 1 + V1 && O1 >= 2 && Z = X] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f9(P1,2,R1,Q1,R1,F,G,H,I,P1,S1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,O1,S1,R1,T1,K1,L1,M1,N1) [P1 >= 2] (1,1) 40. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 41. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && Z1 >= 1 + K && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 42. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && K >= 1 + C && Q1 >= 0 && O1 >= 2 && Q = 1] 43. 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) -> f16(P1,Q1,R1,A2,U1,F,G,C,R,O1,K,K,Z1,Z1,O,P,1,R,B2,T,U,V,W,X,Y,Z,A1,B1,V1,D1,E1,F1,G1,S1,W1,J1,T1,1 + R [X1 >= O1 (?,1) ,C2,N1) && Y1 >= 2 && Q1 >= Y1 && K >= 1 + Z1 && B >= A && B >= 0 && C >= 1 + K && Q1 >= 0 && O1 >= 2 && Q = 1] 44. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(S1,T1,Q1,Z1,A2,F,G,X1,I,P1,K,C2,K,B2,O,P,Q,R,S,T,U,V,W,H2,Y,G2,Y1,I2,W1,D1,E1,F1,O1,R1,U1,J1,V1,L1 [0 >= D2 && 0 >= E2 && 0 >= P1 && 0 >= F2] (1,1) ,M1,N1) 45. 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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,O1,C,B2,C,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,G1,S1,W1,J1,T1,L1 [I2 >= 2 && Q1 >= I2 && D2 >= 2 && Q1 >= D2 && B >= A && B >= 0 && Q1 >= O1 && O1 >= 2 && Q1 >= 0 && C = K] (?,1) ,M1,N1) 51. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && K >= 1 + M && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 52. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1) -> f7(A,B,C,D,E,F,G,R1,I,O1,K,S1,M,P1,O,P,1 + D1 + -1*R,R,S,T,U,V,W,M,D1 + -1*R,K,M,M,C1,D1,E1,F1,G1,H1,I1 [Q1 >= 2 && M >= 1 + K && O1 >= 2 && Q >= 0 && R >= 0 && L = H] (?,1) ,J1,K1,L1,M1,0) 54. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,A2,U1,F,G,C2,I,1,D,B2,D,Z1,O,P,Q,R,S,T,U,V,W,G2,Y,Y1,X1,H2,V1,D1,E1,F1,O1,S1,W1,J1,T1,L1,M1True (1,1) ,N1) 55. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 56. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 57. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && T1 >= 1 + B2] (1,1) ,M1,N1) 58. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> f18(P1,Q1,R1,Z1,A2,F,G,Y1,I,1,T1,X1,B2,C2,O,P,Q,R,S,T,U,V,W,I2,Y,H2,G2,D2,W1,D1,E1,F1,O1,S1,U1,J1,V1,L1 [0 >= 1 && B2 >= 1 + T1] (1,1) ,M1,N1) 59. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (1,1) ,N1) 60. 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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (?,1) ,N1) 61. 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) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,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 True (?,1) ,N1) Signature: {(exitus616,40);(f13,40);(f16,40);(f17,40);(f18,40);(f6,40);(f7,40);(f9,40)} Flow Graph: [0->{0,40,41,42,43,45,60},9->{9,10,11,12,13,14,15,16,51,52},10->{9,10,11,12,13,14,15,16,51,52},11->{9,10 ,11,12,13,14,15,16,51,52},12->{9,10,11,12,13,14,15,16,51,52},13->{9,10,11,12,13,14,15,16,51,52},14->{9,10,11 ,12,13,14,15,16,51,52},15->{9,10,11,12,13,14,15,16,51,52},16->{9,10,11,12,13,14,15,16,51,52},29->{29,30,31 ,32,33,34,35,61},30->{29,30,31,32,33,34,35,36,37,38,61},31->{29,30,31,32,33,34,35,36,37,38,61},32->{29,30,31 ,32,33,34,35,36,37,38,61},33->{29,30,31,32,33,34,35,36,37,38,61},34->{29,30,31,32,33,34,35,36,37,38,61} ,35->{29,30,31,32,33,34,35,36,37,38,61},36->{30,31,32,33,34,35,36,61},37->{},38->{},39->{0,40,41,42,43,45 ,60},40->{9,10,11,12,13,14,15,16},41->{9,10,11,12,13,14,15,16},42->{9,10,11,12,13,14,15,16},43->{9,10,11,12 ,13,14,15,16},44->{},45->{},51->{29,30,31,32,33,34,35,61},52->{30,31,32,33,34,35,36,61},54->{},55->{},56->{} ,57->{},58->{},59->{},60->{},61->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,9,10,11,12,13,14,15,16,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,51,52,54,55,56,57,58,59,60,61] | +- p:[0] c: [0] | +- p:[9,10,11,12,13,14,15,16] c: [16] | | | `- p:[9,10,11,12,13,14,15] c: [15] | | | `- p:[9,10,11,12,13,14] c: [14] | | | `- p:[9,10,11,12,13] c: [13] | | | `- p:[9,10,11,12] c: [12] | | | `- p:[9,10,11] c: [11] | | | `- p:[9,10] c: [10] | | | `- p:[9] c: [9] | `- p:[29,30,31,32,33,34,35,36] c: [] MAYBE