MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [0 >= S && K >= 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [S >= 1 && K >= 1] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,K,R,K,N,O,P,Q) [0 >= K] (1,1) 3. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f29(0,B,R,D,E,F,G,0,R,R,K,L,M,N,O,P,Q) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (?,1) 5. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (?,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] Signature: {(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3},1->{4},2->{4},3->{3},4->{5,6},5->{3},6->{3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [0 >= S && K >= 1] (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,S,R,0,1,S,S,S) [S >= 1 && K >= 1] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f21(1,B,C,D,E,F,G,H,I,J,K,R,K,N,O,P,Q) [0 >= K] (1,1) 3. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [-1*M >= 0 && A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && A >= 0] (?,1) 4. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f29(0,B,R,D,E,F,G,0,R,R,K,L,M,N,O,P,Q) [-1*M >= 0 && -1 + A + -1*M >= 0 && 1 + -1*A + -1*M >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && A >= 1] (1,1) 5. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(1,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (1,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && R >= 1000 + C] 6. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(A,S,C,0,R,R,R,H,I,J,K,L,M,N,O,P,Q) [-1*H >= 0 (1,1) && -1*H + -1*M >= 0 && A + -1*H >= 0 && -1*A + -1*H >= 0 && H >= 0 && H + -1*M >= 0 && A + H >= 0 && -1*A + H >= 0 && -1*M >= 0 && A + -1*M >= 0 && -1*A + -1*M >= 0 && -1*A >= 0 && A >= 0 && 0 >= A && 999 + C >= R] Signature: {(f0,17);(f21,17);(f29,17);(f41,17)} Flow Graph: [0->{3},1->{4},2->{4},3->{3},4->{5,6},5->{3},6->{3}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE