YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f8(-1,-1,1,D,E,F,G) True (1,1) 1. f8(A,B,C,D,E,F,G) -> f8(A,B,1 + C,D,E,F,G) [-1 + C >= 0 (?,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 100 >= C] 2. f18(A,B,C,D,E,F,G) -> f22(A,B,C,D,1,1,G) [-1*E >= 0 (?,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= D] 3. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && F >= 100] 4. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && D + F >= 101] 5. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,E,1 + F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 6. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,0,1 + F,H) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 7. f33(A,B,C,D,E,F,G) -> f18(A,B,C,1 + D,0,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E = 0] 8. f18(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1*E >= 0 (?,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && D >= 100] 9. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 0 >= 1 + E] 10. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E >= 1] 11. f8(A,B,C,D,E,F,G) -> f18(A,B,C,1,0,F,G) [-1 + C >= 0 (?,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && C >= 101] Signature: {(f0,7);(f18,7);(f22,7);(f33,7);(f40,7);(f8,7)} Flow Graph: [0->{1,11},1->{1,11},2->{3,4,5,6},3->{7,9,10},4->{7,9,10},5->{3,4,5,6},6->{3,4,5,6},7->{2,8},8->{},9->{} ,10->{},11->{2,8}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f8(-1,-1,1,D,E,F,G) True (1,1) 1. f8(A,B,C,D,E,F,G) -> f8(A,B,1 + C,D,E,F,G) [-1 + C >= 0 (?,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 100 >= C] 2. f18(A,B,C,D,E,F,G) -> f22(A,B,C,D,1,1,G) [-1*E >= 0 (?,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= D] 3. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && F >= 100] 4. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && D + F >= 101] 5. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,E,1 + F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 6. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,0,1 + F,H) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 7. f33(A,B,C,D,E,F,G) -> f18(A,B,C,1 + D,0,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E = 0] 8. f18(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1*E >= 0 (1,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && D >= 100] 9. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (1,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 0 >= 1 + E] 10. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (1,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E >= 1] 11. f8(A,B,C,D,E,F,G) -> f18(A,B,C,1,0,F,G) [-1 + C >= 0 (1,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && C >= 101] Signature: {(f0,7);(f18,7);(f22,7);(f33,7);(f40,7);(f8,7)} Flow Graph: [0->{1,11},1->{1,11},2->{3,4,5,6},3->{7,9,10},4->{7,9,10},5->{3,4,5,6},6->{3,4,5,6},7->{2,8},8->{},9->{} ,10->{},11->{2,8}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,11),(2,3),(2,4),(11,8)] * Step 3: Looptree YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f8(-1,-1,1,D,E,F,G) True (1,1) 1. f8(A,B,C,D,E,F,G) -> f8(A,B,1 + C,D,E,F,G) [-1 + C >= 0 (?,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 100 >= C] 2. f18(A,B,C,D,E,F,G) -> f22(A,B,C,D,1,1,G) [-1*E >= 0 (?,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= D] 3. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && F >= 100] 4. f22(A,B,C,D,E,F,G) -> f33(A,B,C,D,E,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && D + F >= 101] 5. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,E,1 + F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 6. f22(A,B,C,D,E,F,G) -> f22(A,B,C,D,0,1 + F,H) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -2 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 99 >= F && 100 >= D + F] 7. f33(A,B,C,D,E,F,G) -> f18(A,B,C,1 + D,0,F,G) [-1 + F >= 0 (?,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E = 0] 8. f18(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1*E >= 0 (1,1) && -1 + D + -1*E >= 0 && -101 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && -1 + -1*B + -1*E >= 0 && 1 + A + -1*E >= 0 && -1 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && -101 + C + E >= 0 && 1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + A + E >= 0 && -1 + -1*A + E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && D >= 100] 9. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (1,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && 0 >= 1 + E] 10. f33(A,B,C,D,E,F,G) -> f40(A,B,C,D,E,F,G) [-1 + F >= 0 (1,1) && -2 + E + F >= 0 && -1*E + F >= 0 && -101 + D + F >= 0 && -102 + C + F >= 0 && B + F >= 0 && -2 + -1*B + F >= 0 && A + F >= 0 && -2 + -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && -100 + C + -1*E >= 0 && 2 + B + -1*E >= 0 && -1*B + -1*E >= 0 && 2 + A + -1*E >= 0 && -1*A + -1*E >= 0 && -1 + D >= 0 && -102 + C + D >= 0 && B + D >= 0 && -2 + -1*B + D >= 0 && A + D >= 0 && -2 + -1*A + D >= 0 && -101 + C >= 0 && -100 + B + C >= 0 && -102 + -1*B + C >= 0 && -100 + A + C >= 0 && -102 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && E >= 1] 11. f8(A,B,C,D,E,F,G) -> f18(A,B,C,1,0,F,G) [-1 + C >= 0 (1,1) && B + C >= 0 && -2 + -1*B + C >= 0 && A + C >= 0 && -2 + -1*A + C >= 0 && -1 + -1*B >= 0 && A + -1*B >= 0 && -2 + -1*A + -1*B >= 0 && 1 + B >= 0 && 2 + A + B >= 0 && -1*A + B >= 0 && -1 + -1*A >= 0 && 1 + A >= 0 && C >= 101] Signature: {(f0,7);(f18,7);(f22,7);(f33,7);(f40,7);(f8,7)} Flow Graph: [0->{1},1->{1,11},2->{5,6},3->{7,9,10},4->{7,9,10},5->{3,4,5,6},6->{3,4,5,6},7->{2,8},8->{},9->{},10->{} ,11->{2}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | +- p:[1] c: [1] | `- p:[2,7,3,5,6,4] c: [2] | `- p:[5,6] c: [6] | `- p:[5] c: [5] YES