MAYBE * Step 1: ArgumentFilter 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: ArgumentFilter [6,8,9,10,11,12,14,15] + Details: We remove following argument positions: [6,8,9,10,11,12,14,15]. * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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 4: AddSinks MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True (?,1) Signature: {(exitus616,10);(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 6: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True (?,1) Signature: {(exitus616,10);(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 7: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,Q,R) True (1,1) 6. f5(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True (?,1) Signature: {(exitus616,10);(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 8: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,H,N,Q,R,0.0,0.1] f9 ~> f9 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f5 ~> f0 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= unknown, N <= N, Q <= Q, R <= R] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, H <= 0*K, N <= unknown, Q <= Q, R <= R] f5 ~> f12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= 0*K, N <= 0*K, Q <= unknown, R <= R] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= unknown, H <= 0*K, N <= unknown, Q <= D, R <= B] f6 ~> f9 [A <= 17*K, B <= K, C <= 0*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f5 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= H, N <= N, 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, H <= H, N <= N, 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, H <= 0*K, N <= unknown, Q <= Q, R <= R] + Applied Processor: FlowAbstraction + Details: () * Step 9: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,H,N,Q,R,0.0,0.1] f9 ~> f9 [K ~=> B,K ~=> C,huge ~=> D] f5 ~> f0 [huge ~=> H] f5 ~> f5 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] f5 ~> f12 [K ~=> H,K ~=> N,huge ~=> Q] f9 ~> f5 [B ~=> R,D ~=> Q,K ~=> E,K ~=> H,huge ~=> F,huge ~=> N] f6 ~> f9 [K ~=> A,K ~=> B,K ~=> C,huge ~=> D] 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 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE