YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f18(A,B,C,D,E,F) -> f18(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 1. f24(A,B,C,D,E,F) -> f24(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 2. f31(A,B,C,D,E,F) -> f31(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 3. f31(A,B,C,D,E,F) -> f39(A,B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 4. f24(A,B,C,D,E,F) -> f31(A,0,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 5. f18(A,B,C,D,E,F) -> f24(A,0,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 6. f0(A,B,C,D,E,F) -> f18(10,0,10,G,10,H) True (1,1) Signature: {(f0,6);(f18,6);(f24,6);(f31,6);(f39,6)} Flow Graph: [0->{0,5},1->{1,4},2->{2,3},3->{},4->{2,3},5->{1,4},6->{0,5}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,3),(5,4),(6,5)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f18(A,B,C,D,E,F) -> f18(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 1. f24(A,B,C,D,E,F) -> f24(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 2. f31(A,B,C,D,E,F) -> f31(A,1 + B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] 3. f31(A,B,C,D,E,F) -> f39(A,B,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 4. f24(A,B,C,D,E,F) -> f31(A,0,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 5. f18(A,B,C,D,E,F) -> f24(A,0,C,D,E,F) [10 + -1*E >= 0 (?,1) && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] 6. f0(A,B,C,D,E,F) -> f18(10,0,10,G,10,H) True (1,1) Signature: {(f0,6);(f18,6);(f24,6);(f31,6);(f39,6)} Flow Graph: [0->{0,5},1->{1,4},2->{2,3},3->{},4->{2},5->{1},6->{0}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f18(A,B,C,D,E,F) -> f18(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f24(A,B,C,D,E,F) -> f24(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f31(A,B,C,D,E,F) -> f31(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f31(A,B,C,D,E,F) -> f39(A,B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f24(A,B,C,D,E,F) -> f31(A,0,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f18(A,B,C,D,E,F) -> f24(A,0,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f0(A,B,C,D,E,F) -> f18(10,0,10,G,10,H) True Signature: {(f0,6);(f18,6);(f24,6);(f31,6);(f39,6)} Rule Graph: [0->{0,5},1->{1,4},2->{2,3},3->{},4->{2},5->{1},6->{0}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[0] c: [0] | +- p:[1] c: [1] | `- p:[2] c: [2] * Step 4: CloseWith YES + Considered Problem: (Rules: f18(A,B,C,D,E,F) -> f18(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f24(A,B,C,D,E,F) -> f24(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f31(A,B,C,D,E,F) -> f31(A,1 + B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && A >= 1 + B] f31(A,B,C,D,E,F) -> f39(A,B,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f24(A,B,C,D,E,F) -> f31(A,0,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f18(A,B,C,D,E,F) -> f24(A,0,C,D,E,F) [10 + -1*E >= 0 && C + -1*E >= 0 && 20 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && A + -1*E >= 0 && 20 + -1*A + -1*E >= 0 && -10 + E >= 0 && -20 + C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && -20 + A + E >= 0 && -1*A + E >= 0 && 10 + -1*C >= 0 && 10 + B + -1*C >= 0 && A + -1*C >= 0 && 20 + -1*A + -1*C >= 0 && -10 + C >= 0 && -10 + B + C >= 0 && -20 + A + C >= 0 && -1*A + C >= 0 && B >= 0 && -10 + A + B >= 0 && 10 + -1*A + B >= 0 && 10 + -1*A >= 0 && -10 + A >= 0 && B >= A] f0(A,B,C,D,E,F) -> f18(10,0,10,G,10,H) True Signature: {(f0,6);(f18,6);(f24,6);(f31,6);(f39,6)} Rule Graph: [0->{0,5},1->{1,4},2->{2,3},3->{},4->{2},5->{1},6->{0}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[0] c: [0] | +- p:[1] c: [1] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES