YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f67(5,19,0,0,E,F,G) True (1,1) 1. f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f67(A,B,C,D,E,F,G) -> f75(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f75(A,B,C,D,E,F,G) -> f89(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f75(A,B,C,D,E,F,G) -> f78(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f89(A,B,C,D,E,F,G) -> f99(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f89(A,B,C,D,E,F,G) -> f89(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f89(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f78(A,B,C,D,E,F,G) -> f75(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f78(A,B,C,D,E,F,G) -> f78(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f99(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f99(A,B,C,D,E,F,G) -> f99(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f67,7);(f75,7);(f78,7);(f89,7);(f95,7);(f99,7)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{4,5},3->{1,2,3},4->{6,7,8},5->{9,10},6->{11,12},7->{6,7,8},8->{},9->{4,5} ,10->{9,10},11->{},12->{11,12}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(1,1) ,(1,2) ,(2,4) ,(3,1) ,(4,6) ,(5,9) ,(6,11)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f67(5,19,0,0,E,F,G) True (1,1) 1. f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f67(A,B,C,D,E,F,G) -> f75(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f75(A,B,C,D,E,F,G) -> f89(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f75(A,B,C,D,E,F,G) -> f78(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f89(A,B,C,D,E,F,G) -> f99(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f89(A,B,C,D,E,F,G) -> f89(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f89(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f78(A,B,C,D,E,F,G) -> f75(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f78(A,B,C,D,E,F,G) -> f78(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f99(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f99(A,B,C,D,E,F,G) -> f99(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f67,7);(f75,7);(f78,7);(f89,7);(f95,7);(f99,7)} Flow Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{},9->{4,5},10->{9,10},11->{} ,12->{11,12}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G) -> f67(5,19,0,0,E,F,G) True f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + C,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f67(A,B,C,D,E,F,G) -> f75(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f75(A,B,C,D,E,F,G) -> f89(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f75(A,B,C,D,E,F,G) -> f78(A,B,C,D,0,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f89(A,B,C,D,E,F,G) -> f99(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f89(A,B,C,D,E,F,G) -> f89(A,B,C,1 + D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f89(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f78(A,B,C,D,E,F,G) -> f75(A,B,C,1 + D,E,F,G) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f78(A,B,C,D,E,F,G) -> f78(A,B,C,D,1 + E,H,I) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f99(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f99(A,B,C,D,E,F,G) -> f99(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f67,7);(f75,7);(f78,7);(f89,7);(f95,7);(f99,7)} Rule Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{},9->{4,5},10->{9,10},11->{} ,12->{11,12}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3] c: [3] | +- p:[5,9,10] c: [5,9] | | | `- p:[10] c: [10] | +- p:[7] c: [7] | `- p:[12] c: [12] * Step 4: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G) -> f67(5,19,0,0,E,F,G) True f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + C,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f67(A,B,C,D,E,F,G) -> f75(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f67(A,B,C,D,E,F,G) -> f67(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f75(A,B,C,D,E,F,G) -> f89(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f75(A,B,C,D,E,F,G) -> f78(A,B,C,D,0,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f89(A,B,C,D,E,F,G) -> f99(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f89(A,B,C,D,E,F,G) -> f89(A,B,C,1 + D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f89(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f78(A,B,C,D,E,F,G) -> f75(A,B,C,1 + D,E,F,G) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f78(A,B,C,D,E,F,G) -> f78(A,B,C,D,1 + E,H,I) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -19 + B + E >= 0 && 19 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f99(A,B,C,D,E,F,G) -> f95(A,B,C,D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f99(A,B,C,D,E,F,G) -> f99(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -19 + B + D >= 0 && 19 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -19 + B + -1*C >= 0 && 19 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -19 + B + C >= 0 && 19 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 19 + -1*B >= 0 && 14 + A + -1*B >= 0 && 24 + -1*A + -1*B >= 0 && -19 + B >= 0 && -24 + A + B >= 0 && -14 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f67,7);(f75,7);(f78,7);(f89,7);(f95,7);(f99,7)} Rule Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{},9->{4,5},10->{9,10},11->{} ,12->{11,12}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3] c: [3] | +- p:[5,9,10] c: [5,9] | | | `- p:[10] c: [10] | +- p:[7] c: [7] | `- p:[12] c: [12]) + Applied Processor: CloseWith True + Details: () YES