MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] 1. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] 2. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] 3. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] 4. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] 5. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] 6. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] 7. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,B,C1,E1,B,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] 8. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f1(A,B,C,D,E,F,G,H,I,1 + J,L,C1,L,E1,J,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 9. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f1(A,B,C1,D,E,F,G,H,C1,2,D1,F1,D1,N,O,E1,D1,G1,2,T,U,V,W,X,Y,Z,A1,B1) [C1 >= 2] (1,1) 10. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f9(A,0,C1,0,E,F,G,H,N1,L1,O1,R1,Q1,N,O,M1,P1,R,S,E1,D1,F1,G1,K1,S1,T1,U1,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,K,C1,E1,E,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] 12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,K,C1,E1,E,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] 13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,K,C1,E1,E,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,K,C1,E1,E,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,1,2,3,4,5,6,7},1->{0,1,2,3,4,5,6,7},2->{0,1,2,3,4,5,6,7},3->{0,1,2,3,4,5,6,7},4->{0,1,2,3,4,5,6,7} ,5->{0,1,2,3,4,5,6,7},6->{0,1,2,3,4,5,6,7},7->{0,1,2,3,4,5,6,7},8->{8,11,12,13,14},9->{8,11,12,13,14},10->{} ,11->{0,1,2,3,4,5,6,7},12->{0,1,2,3,4,5,6,7},13->{0,1,2,3,4,5,6,7},14->{0,1,2,3,4,5,6,7}] + Applied Processor: ArgumentFilter [3,4,5,6,7,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26] + Details: We remove following argument positions: [3,4,5,6,7,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] 1. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] 2. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] 3. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] 4. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] 5. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] 6. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] 7. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] 8. f1(A,B,C,I,J,K,S,B1) -> f1(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 9. f8(A,B,C,I,J,K,S,B1) -> f1(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] (1,1) 10. f8(A,B,C,I,J,K,S,B1) -> f9(A,0,C1,N1,L1,O1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 11. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] 12. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] 13. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] 14. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,1,2,3,4,5,6,7},1->{0,1,2,3,4,5,6,7},2->{0,1,2,3,4,5,6,7},3->{0,1,2,3,4,5,6,7},4->{0,1,2,3,4,5,6,7} ,5->{0,1,2,3,4,5,6,7},6->{0,1,2,3,4,5,6,7},7->{0,1,2,3,4,5,6,7},8->{8,11,12,13,14},9->{8,11,12,13,14},10->{} ,11->{0,1,2,3,4,5,6,7},12->{0,1,2,3,4,5,6,7},13->{0,1,2,3,4,5,6,7},14->{0,1,2,3,4,5,6,7}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,1) ,(0,3) ,(0,5) ,(0,7) ,(1,0) ,(1,2) ,(1,4) ,(1,6) ,(2,1) ,(2,3) ,(2,5) ,(2,7) ,(3,0) ,(3,2) ,(3,4) ,(3,6) ,(4,1) ,(4,3) ,(4,5) ,(4,7) ,(5,0) ,(5,2) ,(5,4) ,(5,6) ,(6,1) ,(6,3) ,(6,5) ,(6,7) ,(7,0) ,(7,2) ,(7,4) ,(7,6) ,(11,1) ,(11,3) ,(11,5) ,(11,7) ,(12,1) ,(12,3) ,(12,5) ,(12,7) ,(13,0) ,(13,2) ,(13,4) ,(13,6) ,(14,0) ,(14,2) ,(14,4) ,(14,6)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] 1. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] 2. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] 3. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] 4. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] 5. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] 6. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] 7. f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 (?,1) && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] 8. f1(A,B,C,I,J,K,S,B1) -> f1(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 9. f8(A,B,C,I,J,K,S,B1) -> f1(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] (1,1) 10. f8(A,B,C,I,J,K,S,B1) -> f9(A,0,C1,N1,L1,O1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 11. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] 12. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] 13. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] 14. f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,2,4,6},1->{1,3,5,7},2->{0,2,4,6},3->{1,3,5,7},4->{0,2,4,6},5->{1,3,5,7},6->{0,2,4,6},7->{1,3,5,7} ,8->{8,11,12,13,14},9->{8,11,12,13,14},10->{},11->{0,2,4,6},12->{0,2,4,6},13->{1,3,5,7},14->{1,3,5,7}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12(A,B,C,I,J,K,S,B1) -> f12(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f1(A,B,C,I,J,K,S,B1) -> f1(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f8(A,B,C,I,J,K,S,B1) -> f1(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8(A,B,C,I,J,K,S,B1) -> f9(A,0,C1,N1,L1,O1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1(A,B,C,I,J,K,S,B1) -> f12(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Rule Graph: [0->{0,2,4,6},1->{1,3,5,7},2->{0,2,4,6},3->{1,3,5,7},4->{0,2,4,6},5->{1,3,5,7},6->{0,2,4,6},7->{1,3,5,7} ,8->{8,11,12,13,14},9->{8,11,12,13,14},10->{},11->{0,2,4,6},12->{0,2,4,6},13->{1,3,5,7},14->{1,3,5,7}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f12.0(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.1(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.2(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.3(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.4(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.5(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.6(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.7(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f1.8(A,B,C,I,J,K,S,B1) -> f1.8(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.11(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.12(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.13(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.14(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f8.9(A,B,C,I,J,K,S,B1) -> f1.8(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.11(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.12(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.13(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.14(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.10(A,B,C,I,J,K,S,B1) -> f9.15(A,0,C1,N1,L1,O1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] f1.11(A,B,C,I,J,K,S,B1) -> f12.0(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.2(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.4(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.6(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.12(A,B,C,I,J,K,S,B1) -> f12.0(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.2(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.4(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.6(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.13(A,B,C,I,J,K,S,B1) -> f12.1(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.3(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.5(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.7(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.14(A,B,C,I,J,K,S,B1) -> f12.1(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.3(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.5(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.7(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] Signature: {(f1.11,8) ;(f1.12,8) ;(f1.13,8) ;(f1.14,8) ;(f1.8,8) ;(f12.0,8) ;(f12.1,8) ;(f12.2,8) ;(f12.3,8) ;(f12.4,8) ;(f12.5,8) ;(f12.6,8) ;(f12.7,8) ;(f8.10,8) ;(f8.9,8) ;(f9.15,8)} Rule Graph: [0->{0,1,2,3},1->{8,9,10,11},2->{16,17,18,19},3->{24,25,26,27},4->{4,5,6,7},5->{12,13,14,15},6->{20,21,22 ,23},7->{28,29,30,31},8->{0,1,2,3},9->{8,9,10,11},10->{16,17,18,19},11->{24,25,26,27},12->{4,5,6,7},13->{12 ,13,14,15},14->{20,21,22,23},15->{28,29,30,31},16->{0,1,2,3},17->{8,9,10,11},18->{16,17,18,19},19->{24,25,26 ,27},20->{4,5,6,7},21->{12,13,14,15},22->{20,21,22,23},23->{28,29,30,31},24->{0,1,2,3},25->{8,9,10,11} ,26->{16,17,18,19},27->{24,25,26,27},28->{4,5,6,7},29->{12,13,14,15},30->{20,21,22,23},31->{28,29,30,31} ,32->{32,33,34,35,36},33->{43,44,45,46},34->{47,48,49,50},35->{51,52,53,54},36->{55,56,57,58},37->{32,33,34 ,35,36},38->{43,44,45,46},39->{47,48,49,50},40->{51,52,53,54},41->{55,56,57,58},42->{},43->{0,1,2,3},44->{8 ,9,10,11},45->{16,17,18,19},46->{24,25,26,27},47->{0,1,2,3},48->{8,9,10,11},49->{16,17,18,19},50->{24,25,26 ,27},51->{4,5,6,7},52->{12,13,14,15},53->{20,21,22,23},54->{28,29,30,31},55->{4,5,6,7},56->{12,13,14,15} ,57->{20,21,22,23},58->{28,29,30,31}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f12.0(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.0(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.1(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.1(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && 0 >= 1 + E1 && B >= 1] f12.2(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.2(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && 0 >= 1 + B] f12.3(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.3(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && 0 >= 1 + D1 && E1 >= 1 && B >= 1] f12.4(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.4(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && 0 >= 1 + B] f12.5(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.5(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && 0 >= 1 + E1 && B >= 1] f12.6(A,B,C,I,J,K,S,B1) -> f12.0(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.2(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.4(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.6(A,B,C,I,J,K,S,B1) -> f12.6(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && 0 >= 1 + B] f12.7(A,B,C,I,J,K,S,B1) -> f12.1(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.3(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.5(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f12.7(A,B,C,I,J,K,S,B1) -> f12.7(A,B,C1,I,J,K,S,B1) [-2 + C >= 0 && -4 + B1 + C >= 0 && -4 + C + S >= 0 && C + -1*S >= 0 && -4 + C + J >= 0 && -2 + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2 && D1 >= 1 && E1 >= 1 && B >= 1] f1.8(A,B,C,I,J,K,S,B1) -> f1.8(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.11(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.12(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.13(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f1.8(A,B,C,I,J,K,S,B1) -> f1.14(A,B,C,I,1 + J,L,S,B1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] f8.9(A,B,C,I,J,K,S,B1) -> f1.8(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.11(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.12(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.13(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.9(A,B,C,I,J,K,S,B1) -> f1.14(A,B,C1,C1,2,D1,2,B1) [C1 >= 2] f8.10(A,B,C,I,J,K,S,B1) -> f9.15(A,0,C1,N1,L1,O1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] f1.11(A,B,C,I,J,K,S,B1) -> f12.0(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.2(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.4(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.11(A,B,C,I,J,K,S,B1) -> f12.6(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && 0 >= 1 + E1] f1.12(A,B,C,I,J,K,S,B1) -> f12.0(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.2(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.4(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.12(A,B,C,I,J,K,S,B1) -> f12.6(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && 0 >= 1 + K && E1 >= 1] f1.13(A,B,C,I,J,K,S,B1) -> f12.1(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.3(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.5(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.13(A,B,C,I,J,K,S,B1) -> f12.7(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && 0 >= 1 + E1] f1.14(A,B,C,I,J,K,S,B1) -> f12.1(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.3(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.5(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f1.14(A,B,C,I,J,K,S,B1) -> f12.7(A,K,C1,G1,F1,K1,S,D1) [-2 + I >= 0 && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && D1 >= C1 && C1 >= 2 && K >= 1 && E1 >= 1] f9.15(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.1(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.3(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.5(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.7(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.0(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.2(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.4(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True f12.6(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True Signature: {(exitus616,8) ;(f1.11,8) ;(f1.12,8) ;(f1.13,8) ;(f1.14,8) ;(f1.8,8) ;(f12.0,8) ;(f12.1,8) ;(f12.2,8) ;(f12.3,8) ;(f12.4,8) ;(f12.5,8) ;(f12.6,8) ;(f12.7,8) ;(f8.10,8) ;(f8.9,8) ;(f9.15,8)} Rule Graph: [0->{0,1,2,3,188,204,220,236,252,268,284,300,444,460,476,492,508,524,540,556},1->{8,9,10,11,190,206,222 ,238,254,270,286,302,446,462,478,494,510,526,542,558},2->{16,17,18,19,192,208,224,240,256,272,288,304,448 ,464,480,496,512,528,544,560},3->{24,25,26,27,194,210,226,242,258,274,290,306,450,466,482,498,514,530,546 ,562},4->{4,5,6,7,60,76,92,108,124,140,156,172,316,332,348,364,380,396,412,428},5->{12,13,14,15,62,78,94,110 ,126,142,158,174,318,334,350,366,382,398,414,430},6->{20,21,22,23,64,80,96,112,128,144,160,176,320,336,352 ,368,384,400,416,432},7->{28,29,30,31,66,82,98,114,130,146,162,178,322,338,354,370,386,402,418,434},8->{0,1 ,2,3,189,205,221,237,253,269,285,301,445,461,477,493,509,525,541,557},9->{8,9,10,11,196,212,228,244,260,276 ,292,308,452,468,484,500,516,532,548,564},10->{16,17,18,19,198,214,230,246,262,278,294,310,454,470,486,502 ,518,534,550,566},11->{24,25,26,27,195,211,227,243,259,275,291,307,451,467,483,499,515,531,547,563},12->{4,5 ,6,7,61,77,93,109,125,141,157,173,317,333,349,365,381,397,413,429},13->{12,13,14,15,68,84,100,116,132,148 ,164,180,324,340,356,372,388,404,420,436},14->{20,21,22,23,70,86,102,118,134,150,166,182,326,342,358,374,390 ,406,422,438},15->{28,29,30,31,67,83,99,115,131,147,163,179,323,339,355,371,387,403,419,435},16->{0,1,2,3 ,191,207,223,239,255,271,287,303,447,463,479,495,511,527,543,559},17->{8,9,10,11,197,213,229,245,261,277,293 ,309,453,469,485,501,517,533,549,565},18->{16,17,18,19,201,217,233,249,265,281,297,313,457,473,489,505,521 ,537,553,569},19->{24,25,26,27,200,216,232,248,264,280,296,312,456,472,488,504,520,536,552,568},20->{4,5,6,7 ,63,79,95,111,127,143,159,175,319,335,351,367,383,399,415,431},21->{12,13,14,15,69,85,101,117,133,149,165 ,181,325,341,357,373,389,405,421,437},22->{20,21,22,23,73,89,105,121,137,153,169,185,329,345,361,377,393,409 ,425,441},23->{28,29,30,31,72,88,104,120,136,152,168,184,328,344,360,376,392,408,424,440},24->{0,1,2,3,193 ,209,225,241,257,273,289,305,449,465,481,497,513,529,545,561},25->{8,9,10,11,199,215,231,247,263,279,295,311 ,455,471,487,503,519,535,551,567},26->{16,17,18,19,202,218,234,250,266,282,298,314,458,474,490,506,522,538 ,554,570},27->{24,25,26,27,203,219,235,251,267,283,299,315,459,475,491,507,523,539,555,571},28->{4,5,6,7,65 ,81,97,113,129,145,161,177,321,337,353,369,385,401,417,433},29->{12,13,14,15,71,87,103,119,135,151,167,183 ,327,343,359,375,391,407,423,439},30->{20,21,22,23,74,90,106,122,138,154,170,186,330,346,362,378,394,410,426 ,442},31->{28,29,30,31,75,91,107,123,139,155,171,187,331,347,363,379,395,411,427,443},32->{32,33,34,35,36} ,33->{43,44,45,46},34->{47,48,49,50},35->{51,52,53,54},36->{55,56,57,58},37->{32,33,34,35,36},38->{43,44,45 ,46},39->{47,48,49,50},40->{51,52,53,54},41->{55,56,57,58},42->{59},43->{0,1,2,3},44->{8,9,10,11},45->{16,17 ,18,19},46->{24,25,26,27},47->{0,1,2,3},48->{8,9,10,11},49->{16,17,18,19},50->{24,25,26,27},51->{4,5,6,7} ,52->{12,13,14,15},53->{20,21,22,23},54->{28,29,30,31},55->{4,5,6,7},56->{12,13,14,15},57->{20,21,22,23} ,58->{28,29,30,31}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571] | +- p:[32] c: [32] | +- p:[4,12,5,20,6,28,7,15,13,21,14,29,23,22,30,31] c: [] | `- p:[0,8,1,16,2,24,3,11,9,17,10,25,19,18,26,27] c: [] MAYBE