MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (1,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (1,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (1,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,4)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (1,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (1,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (1,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) Signature: {(exitus616,18);(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3,6},3->{},4->{1,2,3,6},5->{0,4},6->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,4)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) Signature: {(exitus616,18);(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3,6},3->{},4->{1,2,3,6},5->{0},6->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[0] c: [0] | `- p:[2] c: [2] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (?,1) Signature: {(exitus616,18);(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3,6},3->{},4->{1,2,3,6},5->{0},6->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[0] c: [0] | `- p:[2] c: [2]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0.0,0.1] f9 ~> f9 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f5 ~> f0 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= unknown, H <= G, I <= unknown, J <= unknown, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, G <= M, H <= 0*K, I <= unknown, J <= unknown, K <= K, L <= M, M <= N, N <= unknown, O <= unknown, P <= E, Q <= Q, R <= R] f5 ~> f12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= unknown, J <= unknown, K <= K, L <= M, M <= M, N <= 0*K, O <= O, P <= E, Q <= unknown, R <= R] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= unknown, G <= unknown, H <= 0*K, I <= unknown, J <= unknown, K <= K, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= P, Q <= D, R <= B] f6 ~> f9 [A <= 17*K, B <= K, C <= 0*K, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] f5 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.0 <= A + B] f9 ~> f9 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R] + Loop: [0.1 <= K + F] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, G <= M, H <= 0*K, I <= unknown, J <= unknown, K <= K, L <= M, M <= N, N <= unknown, O <= unknown, P <= E, Q <= Q, R <= R] + Applied Processor: FlowAbstraction + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0.0,0.1] f9 ~> f9 [K ~=> B,K ~=> C,huge ~=> D] f5 ~> f0 [G ~=> H,huge ~=> G,huge ~=> I,huge ~=> J,huge ~=> K] f5 ~> f5 [E ~=> P ,M ~=> G ,M ~=> L ,N ~=> M ,K ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> N ,huge ~=> O ,B ~+> E ,E ~+> E ,F ~+> F ,K ~+> F] f5 ~> f12 [E ~=> P,M ~=> L,K ~=> H,K ~=> N,huge ~=> I,huge ~=> J,huge ~=> Q] f9 ~> f5 [B ~=> R ,D ~=> Q ,K ~=> E ,K ~=> H ,huge ~=> F ,huge ~=> G ,huge ~=> I ,huge ~=> J ,huge ~=> L ,huge ~=> M ,huge ~=> N ,huge ~=> O] f6 ~> f9 [K ~=> A,K ~=> B,K ~=> C,huge ~=> D,huge ~=> L] f5 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f9 ~> f9 [K ~=> B,K ~=> C,huge ~=> D] + Loop: [F ~+> 0.1,K ~+> 0.1] f5 ~> f5 [E ~=> P ,M ~=> G ,M ~=> L ,N ~=> M ,K ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> N ,huge ~=> O ,B ~+> E ,E ~+> E ,F ~+> F ,K ~+> F] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE