MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M) True (1,1) 1. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M) [A >= B] (?,1) 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] Signature: {(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3},1->{4,5},2->{1,2,3},3->{},4->{6,7},5->{4,5},6->{4,5},7->{1,2,3}] + Applied Processor: ArgumentFilter [2,3,5,6,8,11] + Details: We remove following argument positions: [2,3,5,6,8,11]. * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True (1,1) 1. f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] (?,1) 4. f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] Signature: {(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3},1->{4,5},2->{1,2,3},3->{},4->{6,7},5->{4,5},6->{4,5},7->{1,2,3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True (1,1) 1. f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] (1,1) 4. f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] Signature: {(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3},1->{4,5},2->{1,2,3},3->{},4->{6,7},5->{4,5},6->{4,5},7->{1,2,3}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,1),(5,4),(6,5),(7,1),(7,3)] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True (1,1) 1. f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] (1,1) 4. f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] Signature: {(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3},1->{4,5},2->{2,3},3->{},4->{6,7},5->{5},6->{4},7->{2}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True (1,1) 1. f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] (?,1) 4. f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] 8. f1(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True (?,1) 9. f8(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True (?,1) Signature: {(exitus616,7);(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3,9},1->{4,5,8},2->{1,2,3,9},3->{},4->{6,7},5->{4,5,8},6->{4,5,8},7->{1,2,3,9},8->{},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,1),(5,4),(6,5),(7,1),(7,3)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True (1,1) 1. f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] (?,1) 2. f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] (?,1) 3. f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] (?,1) 4. f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && M >= 5] 5. f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 (?,1) && -1*H + K >= 0 && -1*H + -1*K >= 0 && -1*H + J >= 0 && -1*H + -1*J >= 0 && H >= 0 && H + K >= 0 && H + -1*K >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*B + E >= 0 && -2 + -1*A + E >= 0 && -1 + -1*A + B >= 0 && -1*K >= 0 && J + -1*K >= 0 && -1*J + -1*K >= 0 && K >= 0 && J + K >= 0 && -1*J + K >= 0 && -1*J >= 0 && J >= 0 && E >= 1 + B && 4 >= M] 6. f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && E >= 1 + B] 7. f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 (?,1) && -4 + -1*H + M >= 0 && -1*H + K >= 0 && 2 + -1*H + -1*K >= 0 && -1*H + J >= 0 && 2 + -1*H + -1*J >= 0 && -1 + H >= 0 && -6 + H + M >= 0 && -2 + H + K >= 0 && H + -1*K >= 0 && -2 + H + J >= 0 && H + -1*J >= 0 && -1*B + E >= 0 && -2 + -1*A + E >= 0 && -2 + -1*A + B >= 0 && -5 + M >= 0 && -6 + K + M >= 0 && -4 + -1*K + M >= 0 && -6 + J + M >= 0 && -4 + -1*J + M >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && -1 + K >= 0 && -2 + J + K >= 0 && -1*J + K >= 0 && 1 + -1*J >= 0 && -1 + J >= 0 && B >= E] 8. f1(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True (?,1) 9. f8(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True (?,1) Signature: {(exitus616,7);(f1,13);(f15,13);(f300,13);(f32,13);(f8,13)} Flow Graph: [0->{1,2,3,9},1->{4,5,8},2->{2,3,9},3->{},4->{6,7},5->{5,8},6->{4,8},7->{2,9},8->{},9->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | +- p:[5] c: [] | +- p:[4,6] c: [6] | `- p:[2] c: [2] MAYBE