YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f61(5,17,0,0,E,F,G) True (1,1) 1. f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f61(A,B,C,D,E,F,G) -> f69(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f69(A,B,C,D,E,F,G) -> f83(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f69(A,B,C,D,E,F,G) -> f72(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f83(A,B,C,D,E,F,G) -> f93(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f83(A,B,C,D,E,F,G) -> f83(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f83(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f72(A,B,C,D,E,F,G) -> f69(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f72(A,B,C,D,E,F,G) -> f72(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f93(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f93(A,B,C,D,E,F,G) -> f93(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f61,7);(f69,7);(f72,7);(f83,7);(f89,7);(f93,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) -> f61(5,17,0,0,E,F,G) True (1,1) 1. f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f61(A,B,C,D,E,F,G) -> f69(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f69(A,B,C,D,E,F,G) -> f83(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f69(A,B,C,D,E,F,G) -> f72(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f83(A,B,C,D,E,F,G) -> f93(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f83(A,B,C,D,E,F,G) -> f83(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f83(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f72(A,B,C,D,E,F,G) -> f69(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f72(A,B,C,D,E,F,G) -> f72(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f93(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f93(A,B,C,D,E,F,G) -> f93(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f61,7);(f69,7);(f72,7);(f83,7);(f89,7);(f93,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) -> f61(5,17,0,0,E,F,G) True f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + C,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f61(A,B,C,D,E,F,G) -> f69(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f69(A,B,C,D,E,F,G) -> f83(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f69(A,B,C,D,E,F,G) -> f72(A,B,C,D,0,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f83(A,B,C,D,E,F,G) -> f93(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f83(A,B,C,D,E,F,G) -> f83(A,B,C,1 + D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f83(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f72(A,B,C,D,E,F,G) -> f69(A,B,C,1 + D,E,F,G) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f72(A,B,C,D,E,F,G) -> f72(A,B,C,D,1 + E,H,I) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f93(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f93(A,B,C,D,E,F,G) -> f93(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f61,7);(f69,7);(f72,7);(f83,7);(f89,7);(f93,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) -> f61(5,17,0,0,E,F,G) True f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + C,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f61(A,B,C,D,E,F,G) -> f69(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f61(A,B,C,D,E,F,G) -> f61(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f69(A,B,C,D,E,F,G) -> f83(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f69(A,B,C,D,E,F,G) -> f72(A,B,C,D,0,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f83(A,B,C,D,E,F,G) -> f93(A,B,C,0,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f83(A,B,C,D,E,F,G) -> f83(A,B,C,1 + D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f83(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,H,I) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f72(A,B,C,D,E,F,G) -> f69(A,B,C,1 + D,E,F,G) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f72(A,B,C,D,E,F,G) -> f72(A,B,C,D,1 + E,H,I) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -17 + B + E >= 0 && 17 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f93(A,B,C,D,E,F,G) -> f89(A,B,C,D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f93(A,B,C,D,E,F,G) -> f93(A,B,C,1 + D,E,F,G) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -17 + B + D >= 0 && 17 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -17 + B + -1*C >= 0 && 17 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -17 + B + C >= 0 && 17 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 17 + -1*B >= 0 && 12 + A + -1*B >= 0 && 22 + -1*A + -1*B >= 0 && -17 + B >= 0 && -22 + A + B >= 0 && -12 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f61,7);(f69,7);(f72,7);(f83,7);(f89,7);(f93,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