MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (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) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && 0 >= W && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && 0 >= A1] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && A1 >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && W >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && A >= B] 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && 1 >= E] 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E = 2] 8. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E >= 3] 9. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + V >= 0 && -1*D + -1*V >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + V >= 0 && D + -1*V >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0] Signature: {(f0,22);(f11,22);(f37,22);(f51,22)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6,7,8},3->{6,7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (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) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && 0 >= W && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && 0 >= A1] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && A1 >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && W >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && A >= B] 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && 1 >= E] 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E = 2] 8. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E >= 3] 9. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + V >= 0 && -1*D + -1*V >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + V >= 0 && D + -1*V >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0] Signature: {(f0,22);(f11,22);(f37,22);(f51,22)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6,7,8},3->{6,7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(2,8),(3,6)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (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) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && 0 >= W && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && 0 >= A1] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && A1 >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && W >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*C >= 0 (1,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && A >= B] 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && 1 >= E] 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E = 2] 8. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E >= 3] 9. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + V >= 0 && -1*D + -1*V >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + V >= 0 && D + -1*V >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0] Signature: {(f0,22);(f11,22);(f37,22);(f51,22)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6},3->{7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (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) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && 0 >= W && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && 0 >= A1] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && A1 >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && W >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && A >= B] 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && 1 >= E] 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E = 2] 8. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E >= 3] 9. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + V >= 0 && -1*D + -1*V >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + V >= 0 && D + -1*V >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0] 10. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) Signature: {(exitus616,22);(f0,22);(f11,22);(f37,22);(f51,22)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6,7,8},3->{6,7,8},4->{9,10},5->{9,10},6->{9,10},7->{9,10},8->{9,10} ,9->{9,10},10->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(2,8),(3,6)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (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) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && 0 >= W && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && 0 >= A1] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && B >= 1 + A && 0 >= W && A1 >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && W >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*C >= 0 (?,1) && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0 && A >= B] 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && 1 >= E] 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E = 2] 8. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && -1*C + U >= 0 && -1*C + -1*U >= 0 && -1*C + Q >= 0 && -1*C + -1*Q >= 0 && -1*C + -1*O >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && C + U >= 0 && C + -1*U >= 0 && C + Q >= 0 && C + -1*Q >= 0 && C + -1*O >= 0 && -1*V >= 0 && U + -1*V >= 0 && -1*U + -1*V >= 0 && Q + -1*V >= 0 && -1*Q + -1*V >= 0 && -1*O + -1*V >= 0 && V >= 0 && U + V >= 0 && -1*U + V >= 0 && Q + V >= 0 && -1*Q + V >= 0 && -1*O + V >= 0 && -1*U >= 0 && Q + -1*U >= 0 && -1*Q + -1*U >= 0 && -1*O + -1*U >= 0 && U >= 0 && Q + U >= 0 && -1*Q + U >= 0 && -1*O + U >= 0 && -1 + -1*A + B >= 0 && -1*Q >= 0 && -1*O + -1*Q >= 0 && Q >= 0 && -1*O + Q >= 0 && -1*O >= 0 && E >= 3] 9. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + V >= 0 && -1*D + -1*V >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + V >= 0 && D + -1*V >= 0 && -1*C >= 0 && -1*C + V >= 0 && -1*C + -1*V >= 0 && C >= 0 && C + V >= 0 && C + -1*V >= 0 && -1*V >= 0 && V >= 0] 10. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) Signature: {(exitus616,22);(f0,22);(f11,22);(f37,22);(f51,22)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6},3->{7,8},4->{9,10},5->{9,10},6->{9,10},7->{9,10},8->{9,10},9->{9,10} ,10->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | +- p:[1] c: [1] | `- p:[9] c: [] MAYBE