YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f11(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,G1,H1,I1,J1) -> f15(A,B,C,D,2 + C,L1,M1,B,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && B >= 0 && K1 >= 1 && C >= 1 && D >= 0 && E = 1 + C] (?,1) 1. f11(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,G1,H1,I1,J1) -> f14(A,B,C,-1 + L1,E,0,M1,H,L1,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && I >= A && B >= 0 && L1 >= 1 && E >= 1 && F = 0] (?,1) 2. f13(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,G1,H1,I1,J1) -> f13(1,B,C,D,2 + K,L1,M1,H,I,J,K,M,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [K1 >= 1 && K >= 1 && E = 1 + K && A = 1] (?,1) 3. f14(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + N,L1,K1,H,I,J,K,L,M,N1,1 + N,M1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && N >= 1 && M1 >= 0 && D >= 0 && F = 0] (?,1) 4. f14(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,Q,L1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = R] (?,1) 5. f15(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + T,L1,K1,H,I,J,K,L,M,N,O,P,Q,R,S,T,M1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && T >= 1 && N1 >= 1 && M1 >= 0 && D >= 0 && E = 1 + T] (?,1) 6. f15(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,Q,L1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = V] (?,1) 7. f17(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,G1,H1,I1,J1) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,A,-1 + B,C1,Z,C1,L1,D1,E1,F1,G1,H1,I1,J1) [X >= B && X >= 1 + M1 && M1 >= 0 && X >= 2 && 1 + Y = B && A = X && Z = A1 && B1 = A1] (?,1) 8. f11(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [B >= A && B >= 0 && 0 >= E && A >= 2] (?,1) 9. f13(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,G1,H1,I1,J1) -> f7(1,B,C,D,E,0,M1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && Q = 0 && A = 1 && F = 0] (?,1) 10. f13(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,G1,H1,I1,J1) -> f7(1,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,L1,E1,F1,G1,H1,I1,J1) [0 >= E && A = 1] (?,1) 11. f14(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,G1,H1,I1,J1) -> f7(A,B,C,0,E,0,G,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && A >= 2 && Q = 0 && F = 0 && D = 0] (?,1) 12. f15(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [D >= 0 && 0 >= E && A >= 2] (?,1) 13. f6(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,G1,H1,I1,J1) -> f7(M1,K1,C,D,100,F,N1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,F1,G1,H1,I1,J1) [0 >= M1 && Q = 0 && E = 100 && B = 0 && A = X && Z = 0] (1,1) 14. f17(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,G1,H1,I1,J1) -> f15(A,K1,C,D,102,M1,N1,H,I,J,K,L,M,N,O,P,Z,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,101,K1,B,I1,J1) [D >= 0 && B >= X && B >= 0 && K1 >= X && K1 >= 0 && X >= 2 && E = 100 && A = X && Z = A1 && B1 = A1] (?,1) 15. f17(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,G1,H1,I1,J1) -> f14(A,M1,C,D,100,0,K1,H,I,J,K,L,M,N,O,P,J1,R,S,T,U,V,W,N1,Y,O1,R1,P1,Q1,L1,S1,F1,G1,B,I1,J1) [D >= 0 (?,1) && B >= X && B >= 0 && M1 >= X && M1 >= 0 && X >= 2 && I1 >= X && E = 100 && F = 0 && A = X && J1 = A1 && Z = A1 && B1 = A1] Signature: {(f11,36);(f13,36);(f14,36);(f15,36);(f17,36);(f6,36);(f7,36)} Flow Graph: [0->{5,6,12},1->{3,4,11},2->{2,9,10},3->{5,6,12},4->{3,4,11},5->{5,6,12},6->{3,4,11},7->{7,14,15},8->{} ,9->{},10->{},11->{},12->{},13->{},14->{5,6,12},15->{3,4,11}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f11(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,G1,H1,I1,J1) -> f15(A,B,C,D,2 + C,L1,M1,B,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && B >= 0 && K1 >= 1 && C >= 1 && D >= 0 && E = 1 + C] (1,1) 1. f11(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,G1,H1,I1,J1) -> f14(A,B,C,-1 + L1,E,0,M1,H,L1,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && I >= A && B >= 0 && L1 >= 1 && E >= 1 && F = 0] (1,1) 2. f13(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,G1,H1,I1,J1) -> f13(1,B,C,D,2 + K,L1,M1,H,I,J,K,M,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [K1 >= 1 && K >= 1 && E = 1 + K && A = 1] (?,1) 3. f14(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + N,L1,K1,H,I,J,K,L,M,N1,1 + N,M1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && N >= 1 && M1 >= 0 && D >= 0 && F = 0] (?,1) 4. f14(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,Q,L1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = R] (?,1) 5. f15(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + T,L1,K1,H,I,J,K,L,M,N,O,P,Q,R,S,T,M1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && T >= 1 && N1 >= 1 && M1 >= 0 && D >= 0 && E = 1 + T] (?,1) 6. f15(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,Q,L1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = V] (?,1) 7. f17(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,G1,H1,I1,J1) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,A,-1 + B,C1,Z,C1,L1,D1,E1,F1,G1,H1,I1,J1) [X >= B && X >= 1 + M1 && M1 >= 0 && X >= 2 && 1 + Y = B && A = X && Z = A1 && B1 = A1] (?,1) 8. f11(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [B >= A && B >= 0 && 0 >= E && A >= 2] (1,1) 9. f13(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,G1,H1,I1,J1) -> f7(1,B,C,D,E,0,M1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && Q = 0 && A = 1 && F = 0] (1,1) 10. f13(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,G1,H1,I1,J1) -> f7(1,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,L1,E1,F1,G1,H1,I1,J1) [0 >= E && A = 1] (1,1) 11. f14(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,G1,H1,I1,J1) -> f7(A,B,C,0,E,0,G,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && A >= 2 && Q = 0 && F = 0 && D = 0] (1,1) 12. f15(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [D >= 0 && 0 >= E && A >= 2] (1,1) 13. f6(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,G1,H1,I1,J1) -> f7(M1,K1,C,D,100,F,N1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,F1,G1,H1,I1,J1) [0 >= M1 && Q = 0 && E = 100 && B = 0 && A = X && Z = 0] (1,1) 14. f17(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,G1,H1,I1,J1) -> f15(A,K1,C,D,102,M1,N1,H,I,J,K,L,M,N,O,P,Z,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,101,K1,B,I1,J1) [D >= 0 && B >= X && B >= 0 && K1 >= X && K1 >= 0 && X >= 2 && E = 100 && A = X && Z = A1 && B1 = A1] (1,1) 15. f17(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,G1,H1,I1,J1) -> f14(A,M1,C,D,100,0,K1,H,I,J,K,L,M,N,O,P,J1,R,S,T,U,V,W,N1,Y,O1,R1,P1,Q1,L1,S1,F1,G1,B,I1,J1) [D >= 0 (1,1) && B >= X && B >= 0 && M1 >= X && M1 >= 0 && X >= 2 && I1 >= X && E = 100 && F = 0 && A = X && J1 = A1 && Z = A1 && B1 = A1] Signature: {(f11,36);(f13,36);(f14,36);(f15,36);(f17,36);(f6,36);(f7,36)} Flow Graph: [0->{5,6,12},1->{3,4,11},2->{2,9,10},3->{5,6,12},4->{3,4,11},5->{5,6,12},6->{3,4,11},7->{7,14,15},8->{} ,9->{},10->{},11->{},12->{},13->{},14->{5,6,12},15->{3,4,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12),(2,2),(2,10),(3,12),(5,5),(5,12),(7,7),(14,12)] * Step 3: UnreachableRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f11(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,G1,H1,I1,J1) -> f15(A,B,C,D,2 + C,L1,M1,B,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && B >= 0 && K1 >= 1 && C >= 1 && D >= 0 && E = 1 + C] (1,1) 1. f11(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,G1,H1,I1,J1) -> f14(A,B,C,-1 + L1,E,0,M1,H,L1,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && B >= A && I >= A && B >= 0 && L1 >= 1 && E >= 1 && F = 0] (1,1) 2. f13(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,G1,H1,I1,J1) -> f13(1,B,C,D,2 + K,L1,M1,H,I,J,K,M,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [K1 >= 1 && K >= 1 && E = 1 + K && A = 1] (?,1) 3. f14(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + N,L1,K1,H,I,J,K,L,M,N1,1 + N,M1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && N >= 1 && M1 >= 0 && D >= 0 && F = 0] (?,1) 4. f14(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,Q,L1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = R] (?,1) 5. f15(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,G1,H1,I1,J1) -> f15(A,B,C,M1,2 + T,L1,K1,H,I,J,K,L,M,N,O,P,Q,R,S,T,M1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && T >= 1 && N1 >= 1 && M1 >= 0 && D >= 0 && E = 1 + T] (?,1) 6. f15(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,G1,H1,I1,J1) -> f14(A,B,C,L1,E,0,M1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,Q,L1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1) [A >= 2 && E >= 1 && L1 >= 0 && D >= 0 && F = 0 && Q = V] (?,1) 7. f17(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,G1,H1,I1,J1) -> f17(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,A,-1 + B,C1,Z,C1,L1,D1,E1,F1,G1,H1,I1,J1) [X >= B && X >= 1 + M1 && M1 >= 0 && X >= 2 && 1 + Y = B && A = X && Z = A1 && B1 = A1] (?,1) 8. f11(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [B >= A && B >= 0 && 0 >= E && A >= 2] (1,1) 9. f13(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,G1,H1,I1,J1) -> f7(1,B,C,D,E,0,M1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && Q = 0 && A = 1 && F = 0] (1,1) 10. f13(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,G1,H1,I1,J1) -> f7(1,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,L1,E1,F1,G1,H1,I1,J1) [0 >= E && A = 1] (1,1) 11. f14(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,G1,H1,I1,J1) -> f7(A,B,C,0,E,0,G,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,L1,E1,F1,G1,H1,I1,J1) [E >= 1 && A >= 2 && Q = 0 && F = 0 && D = 0] (1,1) 12. f15(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,G1,H1,I1,J1) -> f7(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,L1,E1,F1,G1,H1,I1,J1) [D >= 0 && 0 >= E && A >= 2] (1,1) 13. f6(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,G1,H1,I1,J1) -> f7(M1,K1,C,D,100,F,N1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,F1,G1,H1,I1,J1) [0 >= M1 && Q = 0 && E = 100 && B = 0 && A = X && Z = 0] (1,1) 14. f17(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,G1,H1,I1,J1) -> f15(A,K1,C,D,102,M1,N1,H,I,J,K,L,M,N,O,P,Z,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,101,K1,B,I1,J1) [D >= 0 && B >= X && B >= 0 && K1 >= X && K1 >= 0 && X >= 2 && E = 100 && A = X && Z = A1 && B1 = A1] (1,1) 15. f17(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,G1,H1,I1,J1) -> f14(A,M1,C,D,100,0,K1,H,I,J,K,L,M,N,O,P,J1,R,S,T,U,V,W,N1,Y,O1,R1,P1,Q1,L1,S1,F1,G1,B,I1,J1) [D >= 0 (1,1) && B >= X && B >= 0 && M1 >= X && M1 >= 0 && X >= 2 && I1 >= X && E = 100 && F = 0 && A = X && J1 = A1 && Z = A1 && B1 = A1] Signature: {(f11,36);(f13,36);(f14,36);(f15,36);(f17,36);(f6,36);(f7,36)} Flow Graph: [0->{5,6},1->{3,4,11},2->{9},3->{5,6},4->{3,4,11},5->{6},6->{3,4,11},7->{14,15},8->{},9->{},10->{},11->{} ,12->{},13->{},14->{5,6},15->{3,4,11}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0 ,1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,14 ,15] * Step 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 13. f6(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,G1,H1,I1,J1) -> f7(M1,K1,C,D,100,F,N1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,F1,G1,H1,I1,J1) [0 >= M1 && Q = 0 && E = 100 && B = 0 && A = X && Z = 0] (1,1) Signature: {(f11,36);(f13,36);(f14,36);(f15,36);(f17,36);(f6,36);(f7,36)} Flow Graph: [13->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 13. f6(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,G1,H1,I1,J1) -> f7(M1,K1,C,D,100,F,N1,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,O1,Y,P1,S1,Q1,R1,L1,T1,F1,G1,H1,I1,J1) [0 >= M1 && Q = 0 && E = 100 && B = 0 && A = X && Z = 0] (1,1) 14. f6(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,G1,H1,I1,J1) -> exitus616(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,G1,H1,I1,J1) True (1,1) Signature: {(exitus616,36);(f11,36);(f13,36);(f14,36);(f15,36);(f17,36);(f6,36);(f7,36)} Flow Graph: [13->{},14->{}] + Applied Processor: UnsatPaths + Details: The problem is already solved. YES(?,O(1))