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: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: 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,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,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,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,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 4: AddSinks 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,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,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,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,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: AddSinks + Details: () * Step 5: 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] 15. f8(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True (1,1) 16. f12(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True (?,1) Signature: {(exitus616,8);(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,1,2,3,4,5,6,7,16},1->{0,1,2,3,4,5,6,7,16},2->{0,1,2,3,4,5,6,7,16},3->{0,1,2,3,4,5,6,7,16},4->{0,1,2 ,3,4,5,6,7,16},5->{0,1,2,3,4,5,6,7,16},6->{0,1,2,3,4,5,6,7,16},7->{0,1,2,3,4,5,6,7,16},8->{8,11,12,13,14} ,9->{8,11,12,13,14},10->{},11->{0,1,2,3,4,5,6,7,16},12->{0,1,2,3,4,5,6,7,16},13->{0,1,2,3,4,5,6,7,16},14->{0 ,1,2,3,4,5,6,7,16},15->{},16->{}] + 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 6: Failure 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] 15. f8(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True (1,1) 16. f12(A,B,C,I,J,K,S,B1) -> exitus616(A,B,C,I,J,K,S,B1) True (?,1) Signature: {(exitus616,8);(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,2,4,6,16},1->{1,3,5,7,16},2->{0,2,4,6,16},3->{1,3,5,7,16},4->{0,2,4,6,16},5->{1,3,5,7,16},6->{0,2,4 ,6,16},7->{1,3,5,7,16},8->{8,11,12,13,14},9->{8,11,12,13,14},10->{},11->{0,2,4,6,16},12->{0,2,4,6,16},13->{1 ,3,5,7,16},14->{1,3,5,7,16},15->{},16->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[8] c: [8] | +- p:[1,3,5,7] c: [] | `- p:[0,2,4,6] c: [] MAYBE