MAYBE * Step 1: 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) 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 2: 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}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank 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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 14 + -1*x18 p(f12) = 14 + -1*x18 p(f5) = 14 + -1*x18 p(f6) = 16 p(f9) = 17 + -1*x2 Following rules are strictly oriented: [-1 + B + -1*C >= 0 ==> && 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] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 17 + -1*B > 16 + -1*B = f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) Following rules are weakly oriented: [-1*H >= 0 ==> && -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] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 14 + -1*R >= 14 + -1*R = f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 ==> && -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] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 14 + -1*R >= 14 + -1*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 + 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] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 14 + -1*R >= 14 + -1*R = f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1 + B + -1*C >= 0 ==> && 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] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 17 + -1*B >= 16 + -1*C = f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) True ==> f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) = 16 >= 16 = f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) * Step 4: Failure 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 (16,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: Failing "Open problems left." + Details: Open problems left. MAYBE