MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + L1,G1,L,M,N,O,J1,K1,R,S,T,I1,N1,O1,P1,Q1,Z,A1,B1,C1,D1,E1,F1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] (?,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f18(G1,B,C,D,E,F,G,H,I,K1,K,L,0,N,0,H1,J1,0,S,T,U,V,W,X,Y,L1,A1,B1,C1,D1,E1,F1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] (?,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && B >= 1 && G1 >= 1] (?,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && 0 >= 1 + B && G1 >= 1] (?,1) 6. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(J,B,C,D,G1,H1,H1,H1,H1,1 + J,H1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) 7. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + J,G1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 0 && A >= 0] (?,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f22(G1,L,0,0,E,F,G,H,L,J,K,L,L,L,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 1 && A >= 1 && B = 0] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) Signature: {(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Flow Graph: [0->{0,1,2,3},1->{},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{},6->{0,1,2,3},7->{0,1,2,3},8->{},9->{4,5,6,7 ,8}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: Failure MAYBE + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + L1,G1,L,M,N,O,J1,K1,R,S,T,I1,N1,O1,P1,Q1,Z,A1,B1,C1,D1,E1,F1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] (?,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f18(G1,B,C,D,E,F,G,H,I,K1,K,L,0,N,0,H1,J1,0,S,T,U,V,W,X,Y,L1,A1,B1,C1,D1,E1,F1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] (1,1) 2. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] (?,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && B >= 1 && G1 >= 1] (1,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && 0 >= 1 + B && G1 >= 1] (1,1) 6. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(J,B,C,D,G1,H1,H1,H1,H1,1 + J,H1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) 7. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + J,G1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 0 && A >= 0] (?,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f22(G1,L,0,0,E,F,G,H,L,J,K,L,L,L,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 1 && A >= 1 && B = 0] (1,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) Signature: {(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Flow Graph: [0->{0,1,2,3},1->{},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{},6->{0,1,2,3},7->{0,1,2,3},8->{},9->{4,5,6,7 ,8}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE