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: 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] 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 3: FromIts 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->{2,3},3->{},4->{6,7},5->{5},6->{4},7->{2}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f15(A,B,E,H,J,K,M) -> f8(A,B,E,H,J,K,M) True f8(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] f8(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] f8(A,B,E,H,J,K,M) -> f32(A,B,E,H,J,K,M) [A >= B] f1(A,B,E,H,J,K,M) -> f300(A,1 + B,E,1,1,1,M) [-1*H >= 0 && -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] f1(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [-1*H >= 0 && -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] f300(A,B,E,H,J,K,M) -> f1(A,B,E,0,0,0,M) [1 + -1*H >= 0 && -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] f300(A,B,E,H,J,K,M) -> f8(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 && -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)} Rule Graph: [0->{1,2,3},1->{4,5},2->{2,3},3->{},4->{6,7},5->{5},6->{4},7->{2}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f15.0(A,B,E,H,J,K,M) -> f8.1(A,B,E,H,J,K,M) True f15.0(A,B,E,H,J,K,M) -> f8.2(A,B,E,H,J,K,M) True f15.0(A,B,E,H,J,K,M) -> f8.3(A,B,E,H,J,K,M) True f8.1(A,B,E,H,J,K,M) -> f1.4(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] f8.1(A,B,E,H,J,K,M) -> f1.5(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] f8.2(A,B,E,H,J,K,M) -> f8.2(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] f8.2(A,B,E,H,J,K,M) -> f8.3(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] f8.3(A,B,E,H,J,K,M) -> f32.8(A,B,E,H,J,K,M) [A >= B] f1.4(A,B,E,H,J,K,M) -> f300.6(A,1 + B,E,1,1,1,M) [-1*H >= 0 && -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] f1.4(A,B,E,H,J,K,M) -> f300.7(A,1 + B,E,1,1,1,M) [-1*H >= 0 && -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] f1.5(A,B,E,H,J,K,M) -> f1.5(A,B,E,0,0,0,M) [-1*H >= 0 && -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] f300.6(A,B,E,H,J,K,M) -> f1.4(A,B,E,0,0,0,M) [1 + -1*H >= 0 && -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] f300.7(A,B,E,H,J,K,M) -> f8.2(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 && -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.4,7);(f1.5,7);(f15.0,7);(f300.6,7);(f300.7,7);(f32.8,7);(f8.1,7);(f8.2,7);(f8.3,7)} Rule Graph: [0->{3,4},1->{5,6},2->{7},3->{8,9},4->{10},5->{5,6},6->{7},7->{},8->{11},9->{12},10->{10},11->{8,9},12->{5 ,6}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f15.0(A,B,E,H,J,K,M) -> f8.1(A,B,E,H,J,K,M) True f15.0(A,B,E,H,J,K,M) -> f8.2(A,B,E,H,J,K,M) True f15.0(A,B,E,H,J,K,M) -> f8.3(A,B,E,H,J,K,M) True f8.1(A,B,E,H,J,K,M) -> f1.4(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] f8.1(A,B,E,H,J,K,M) -> f1.5(A,B,E,0,0,0,M) [B >= 1 + A && E >= 1 + B] f8.2(A,B,E,H,J,K,M) -> f8.2(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] f8.2(A,B,E,H,J,K,M) -> f8.3(1 + A,B,E,H,J,K,M) [B >= 1 + A && B >= E] f8.3(A,B,E,H,J,K,M) -> f32.8(A,B,E,H,J,K,M) [A >= B] f1.4(A,B,E,H,J,K,M) -> f300.6(A,1 + B,E,1,1,1,M) [-1*H >= 0 && -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] f1.4(A,B,E,H,J,K,M) -> f300.7(A,1 + B,E,1,1,1,M) [-1*H >= 0 && -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] f1.5(A,B,E,H,J,K,M) -> f1.5(A,B,E,0,0,0,M) [-1*H >= 0 && -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] f300.6(A,B,E,H,J,K,M) -> f1.4(A,B,E,0,0,0,M) [1 + -1*H >= 0 && -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] f300.7(A,B,E,H,J,K,M) -> f8.2(1 + A,B,E,H,J,K,M) [1 + -1*H >= 0 && -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] f32.8(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True f32.8(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True f1.5(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True f32.8(A,B,E,H,J,K,M) -> exitus616(A,B,E,H,J,K,M) True Signature: {(exitus616,7);(f1.4,7);(f1.5,7);(f15.0,7);(f300.6,7);(f300.7,7);(f32.8,7);(f8.1,7);(f8.2,7);(f8.3,7)} Rule Graph: [0->{3,4},1->{5,6},2->{7},3->{8,9},4->{10},5->{5,6},6->{7},7->{13,14,16},8->{11},9->{12},10->{10,15} ,11->{8,9},12->{5,6}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[10] c: [] | +- p:[8,11] c: [8,11] | `- p:[5] c: [5] MAYBE