YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [H + -1*I >= 0 (?,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 (?,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: Looptree YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [H + -1*I >= 0 (1,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 (1,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [17] | `- p:[3,12,5,14,7,15,9,16,13] c: [16] | `- p:[3,12,5,14,7,15,13] c: [15] | `- p:[3,12,5,14,13] c: [14] | `- p:[3,12,13] c: [13] | `- p:[3,12] c: [12] YES