MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f9(0,1,1,0,0,J,G,H,I) [J >= 1] (1,1) 1. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,-2 + A,1,-2 + A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 3 && C >= 1 && D = E && F = 0] 2. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,A,0,A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 2 >= A && C >= 1 && D = E && F = 0] 3. f9(A,B,C,D,E,F,G,H,I) -> f20(0,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && A >= 3 && 0 >= C && D = E && F = 0] 4. f9(A,B,C,D,E,F,G,H,I) -> f20(1 + A,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && 2 >= A && 0 >= C && D = E && F = 0] 5. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F && D = E] 6. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1 && D = E] 7. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,0,E,F,G,H,0) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I = 0] 8. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + I] 9. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I >= 1] 10. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,0,F,G,0,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H = 0] 11. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + H] 12. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H >= 1] 13. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] 14. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1 + E] Signature: {(f0,9);(f20,9);(f32,9);(f38,9);(f9,9)} Flow Graph: [0->{1,2,3,4,5,6,13,14},1->{7,8,9},2->{7,8,9},3->{7,8,9},4->{7,8,9},5->{7,8,9},6->{7,8,9},7->{10,11,12} ,8->{10,11,12},9->{10,11,12},10->{1,2,3,4,5,6,13,14},11->{1,2,3,4,5,6,13,14},12->{1,2,3,4,5,6,13,14},13->{} ,14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,1) ,(0,2) ,(0,3) ,(0,4) ,(0,5) ,(0,13) ,(0,14) ,(1,7) ,(1,8) ,(2,8) ,(10,13) ,(11,14) ,(12,14)] * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f9(0,1,1,0,0,J,G,H,I) [J >= 1] (1,1) 1. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,-2 + A,1,-2 + A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 3 && C >= 1 && D = E && F = 0] 2. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,A,0,A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 2 >= A && C >= 1 && D = E && F = 0] 3. f9(A,B,C,D,E,F,G,H,I) -> f20(0,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && A >= 3 && 0 >= C && D = E && F = 0] 4. f9(A,B,C,D,E,F,G,H,I) -> f20(1 + A,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && 2 >= A && 0 >= C && D = E && F = 0] 5. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F && D = E] 6. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1 && D = E] 7. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,0,E,F,G,H,0) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I = 0] 8. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + I] 9. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I >= 1] 10. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,0,F,G,0,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H = 0] 11. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + H] 12. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H >= 1] 13. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] 14. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1 + E] Signature: {(f0,9);(f20,9);(f32,9);(f38,9);(f9,9)} Flow Graph: [0->{6},1->{9},2->{7,9},3->{7,8,9},4->{7,8,9},5->{7,8,9},6->{7,8,9},7->{10,11,12},8->{10,11,12},9->{10,11 ,12},10->{1,2,3,4,5,6,14},11->{1,2,3,4,5,6,13},12->{1,2,3,4,5,6,13},13->{},14->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f9(0,1,1,0,0,J,G,H,I) [J >= 1] (1,1) 1. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,-2 + A,1,-2 + A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 3 && C >= 1 && D = E && F = 0] 2. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,-1 + C,D,D,0,A,0,A) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 2 >= A && C >= 1 && D = E && F = 0] 3. f9(A,B,C,D,E,F,G,H,I) -> f20(0,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && A >= 3 && 0 >= C && D = E && F = 0] 4. f9(A,B,C,D,E,F,G,H,I) -> f20(1 + A,1 + B,1 + B,D,D,J,G,H,I) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && J >= 1 && 2 >= A && 0 >= C && D = E && F = 0] 5. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F && D = E] 6. f9(A,B,C,D,E,F,G,H,I) -> f20(A,B,C,D,D,-1 + F,G,J,K) [E >= 0 (?,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1 && D = E] 7. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,0,E,F,G,H,0) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I = 0] 8. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + I] 9. f20(A,B,C,D,E,F,G,H,I) -> f32(A,B,C,1,E,F,G,H,I) [D + -1*E >= 0 (?,1) && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && I >= 1] 10. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,0,F,G,0,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H = 0] 11. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + H] 12. f32(A,B,C,D,E,F,G,H,I) -> f9(A,B,C,D,1,F,G,H,I) [E >= 0 (?,1) && D + E >= 0 && 1 + -1*D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && 1 + -1*D >= 0 && B + -1*D >= 0 && 1 + A + -1*D >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && H >= 1] 13. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (1,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] 14. f9(A,B,C,D,E,F,G,H,I) -> f38(A,B,C,D,E,F,G,H,I) [E >= 0 (1,1) && D + E >= 0 && -1 + B + E >= 0 && A + E >= 0 && D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1 + E] Signature: {(f0,9);(f20,9);(f32,9);(f38,9);(f9,9)} Flow Graph: [0->{6},1->{9},2->{7,9},3->{7,8,9},4->{7,8,9},5->{7,8,9},6->{7,8,9},7->{10,11,12},8->{10,11,12},9->{10,11 ,12},10->{1,2,3,4,5,6,14},11->{1,2,3,4,5,6,13},12->{1,2,3,4,5,6,13},13->{},14->{}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE