YES * Step 1: UnsatPaths YES + 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: FromIts YES + 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: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: 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 && 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] 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*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] 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*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) -> lbl71(A,B,Q,D,0,F,G,H,0,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] 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*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) -> 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*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] 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 && 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) -> 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 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 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*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) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,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] 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 && 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) -> lbl71(A,B,Q,D,0,F,O,H,0,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] 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 Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Rule 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: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[7,3,1,8,5,4,6,9] c: [1,3,8] | `- p:[4,6,9,5,7] c: [5,6,7,9] | `- p:[4] c: [4] * Step 4: CloseWith YES + Considered Problem: (Rules: 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 && 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] 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*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] 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*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) -> lbl71(A,B,Q,D,0,F,G,H,0,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] 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*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) -> 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*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] 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 && 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) -> 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 && 1 + 2*O >= L && O >= G && G >= 1 && L >= 1 + E && I = E && K = L] 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*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) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,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] 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 && 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) -> lbl71(A,B,Q,D,0,F,O,H,0,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] 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 Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Rule 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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[7,3,1,8,5,4,6,9] c: [1,3,8] | `- p:[4,6,9,5,7] c: [5,6,7,9] | `- p:[4] c: [4]) + Applied Processor: CloseWith True + Details: () YES