MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 6. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] 10. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 12. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{10,11},1->{2,3},2->{},3->{6,7},4->{4,5},5->{8,9},6->{4,5},7->{8,9},8->{1},9->{6,7},10->{},11->{6,7} ,12->{0}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,6),(11,6)] * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 6. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] 10. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [-1*I + J >= 0 (?,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 12. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{10,11},1->{2,3},2->{},3->{7},4->{4,5},5->{8,9},6->{4,5},7->{8,9},8->{1},9->{6,7},10->{},11->{7} ,12->{0}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (1,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 6. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] 10. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 12. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{10,11},1->{2,3},2->{},3->{7},4->{4,5},5->{8,9},6->{4,5},7->{8,9},8->{1},9->{6,7},10->{},11->{7} ,12->{0}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + x7 + x12 p(lbl121) = x7 + x12 p(lbl123) = 2*x1 + x12 p(lbl21) = 2*x12 p(lbl53) = 1 + x7 + x12 p(lbl71) = 1 + x7 + x12 p(start) = 3*x11 + -1*x12 p(start0) = 2*x12 p(stop) = -1 + 2*x7 + 2*x12 + -2*x15 Following rules are strictly oriented: [1 + -1*I + M >= 0 ==> && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L > G + L = lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) Following rules are weakly oriented: [-1*I + J >= 0 ==> && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 3*K + -1*L >= 2*L = lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [1 + -1*I + M >= 0 ==> && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = G + L >= 2*A + L = lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 ==> && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 2*A + L >= -1 + 2*G + 2*L + -2*O = stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 ==> && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 2*A + L >= 1 + G + L = lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 ==> && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L >= 1 + G + L = lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 ==> && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L >= 1 + G + L = lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 ==> && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L >= 1 + G + L = lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 ==> && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L >= 1 + G + L = lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + -1*I + M >= 0 ==> && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 1 + G + L >= 1 + G + L = lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 ==> && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 2*L >= -1 + 2*L = stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 ==> && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 2*L >= 1 + L + O = lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) True ==> start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) = 2*L >= 2*L = start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) * Step 4: KnowledgePropagation MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (1,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 6. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (2*L,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] 10. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 12. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{10,11},1->{2,3},2->{},3->{7},4->{4,5},5->{8,9},6->{4,5},7->{8,9},8->{1},9->{6,7},10->{},11->{7} ,12->{0}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: Failure MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && O + -1*P >= 0 && -1*O + P >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (2*L,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -3 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -2 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (1,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (2*L,1) && -1*I + L >= 0 && -1*I + K >= 0 && -2 + I >= 0 && -2 + G + I >= 0 && -2 + E + I >= 0 && -1 + -1*E + I >= 0 && -3 + I + O >= 0 && -3 + I + M >= 0 && -1 + I + -1*M >= 0 && -4 + I + L >= 0 && I + -1*L >= 0 && -4 + I + K >= 0 && I + -1*K >= 0 && -2 + A + I >= 0 && A + -1*G >= 0 && G >= 0 && E + G >= 0 && -1 + G + O >= 0 && -1 + G + M >= 0 && -2 + G + L >= 0 && -2 + G + K >= 0 && A + G >= 0 && -1*A + G >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && -1 + E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && A + E >= 0 && -1 + O >= 0 && -2 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + A + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && -1 + M >= 0 && -3 + L + M >= 0 && 1 + -1*L + M >= 0 && -3 + K + M >= 0 && 1 + -1*K + M >= 0 && -1 + A + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + A + L >= 0 && -2 + K >= 0 && -2 + A + K >= 0 && A >= 0 && L >= 1 && A >= 1 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [-1 + -1*I + L >= 0 (?,1) && -1 + -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1*G + I >= 0 && E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + -1*G + L >= 0 && -1 + -1*G + K >= 0 && -1 + G >= 0 && E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -2 + -1*E + L >= 0 && -2 + -1*E + K >= 0 && E + O >= 0 && -1 + E + L >= 0 && -1 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] 6. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && E >= G && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [E + -1*I >= 0 (?,1) && I >= 0 && -1 + G + I >= 0 && E + I >= 0 && -1*E + I >= 0 && -1 + I + O >= 0 && -2 + I + L >= 0 && -2 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && E >= 0 && -1 + E + O >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (2*L,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 1 + E && G >= 1 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [1 + -1*I + M >= 0 (?,1) && -1*I + L >= 0 && -1*I + K >= 0 && -1 + I >= 0 && -2 + G + I >= 0 && -1 + E + I >= 0 && -1 + -1*E + I >= 0 && -2 + I + O >= 0 && -1 + I + M >= 0 && -1 + I + -1*M >= 0 && -3 + I + L >= 0 && -3 + I + K >= 0 && -1*G + O >= 0 && -1 + G >= 0 && -1 + E + G >= 0 && -2 + G + O >= 0 && -1 + G + M >= 0 && -3 + G + L >= 0 && -3 + G + K >= 0 && -1*E + M >= 0 && -1 + -1*E + L >= 0 && -1 + -1*E + K >= 0 && E >= 0 && -1 + E + O >= 0 && E + M >= 0 && -2 + E + L >= 0 && -2 + E + K >= 0 && -1 + O >= 0 && -1 + M + O >= 0 && -3 + L + O >= 0 && -3 + K + O >= 0 && -1 + L + -1*M >= 0 && -1 + K + -1*M >= 0 && M >= 0 && -2 + L + M >= 0 && -2 + K + M >= 0 && K + -1*L >= 0 && -2 + L >= 0 && -4 + K + L >= 0 && -1*K + L >= 0 && -2 + K >= 0 && L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] 10. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [-1*I + J >= 0 (1,1) && I + -1*J >= 0 && G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && M + -1*N >= 0 && -1*M + N >= 0 && K + -1*L >= 0 && -1*K + L >= 0 && L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] 12. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{10,11},1->{2,3},2->{},3->{7},4->{4,5},5->{8,9},6->{4,5},7->{8,9},8->{1},9->{6,7},10->{},11->{7} ,12->{0}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE