MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f12(H,I,J,0,E,F,G) True (1,1) 1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D] (?,1) 2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1) 3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] (?,1) 4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H) [D >= 0 && D >= C] (?,1) Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Flow Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] + Applied Processor: ArgumentFilter [1,6] + Details: We remove following argument positions: [1,6]. * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,C,D,E,F) -> f12(H,J,0,E,F) True (1,1) 1. f12(A,C,D,E,F) -> f12(A,C,1 + D,E,F) [D >= 0 && C >= 1 + D] (?,1) 2. f25(A,C,D,E,F) -> f25(A,C,D,E,1 + F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1) 3. f25(A,C,D,E,F) -> f34(A,C,D,E,F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] (?,1) 4. f12(A,C,D,E,F) -> f25(A,C,D,A,0) [D >= 0 && D >= C] (?,1) Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Flow Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks MAYBE + Considered Problem: Rules: f0(A,C,D,E,F) -> f12(H,J,0,E,F) True f12(A,C,D,E,F) -> f12(A,C,1 + D,E,F) [D >= 0 && C >= 1 + D] f25(A,C,D,E,F) -> f25(A,C,D,E,1 + F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] f25(A,C,D,E,F) -> f34(A,C,D,E,F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] f12(A,C,D,E,F) -> f25(A,C,D,A,0) [D >= 0 && D >= C] Signature: {(f0,7);(f12,7);(f25,7);(f34,7)} Rule Graph: [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}] + Applied Processor: AddSinks + Details: () * Step 4: Decompose MAYBE + Considered Problem: Rules: f0(A,C,D,E,F) -> f12(H,J,0,E,F) True f12(A,C,D,E,F) -> f12(A,C,1 + D,E,F) [D >= 0 && C >= 1 + D] f25(A,C,D,E,F) -> f25(A,C,D,E,1 + F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] f25(A,C,D,E,F) -> f34(A,C,D,E,F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] f12(A,C,D,E,F) -> f25(A,C,D,A,0) [D >= 0 && D >= C] f34(A,C,D,E,F) -> exitus616(A,C,D,E,F) True Signature: {(exitus616,5);(f0,7);(f12,7);(f25,7);(f34,7)} Rule Graph: [0->{1,4},1->{1,4},2->{2,3},3->{5},4->{2,3}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5] | +- p:[1] c: [1] | `- p:[2] c: [2] * Step 5: AbstractSize MAYBE + Considered Problem: (Rules: f0(A,C,D,E,F) -> f12(H,J,0,E,F) True f12(A,C,D,E,F) -> f12(A,C,1 + D,E,F) [D >= 0 && C >= 1 + D] f25(A,C,D,E,F) -> f25(A,C,D,E,1 + F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] f25(A,C,D,E,F) -> f34(A,C,D,E,F) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E] f12(A,C,D,E,F) -> f25(A,C,D,A,0) [D >= 0 && D >= C] f34(A,C,D,E,F) -> exitus616(A,C,D,E,F) True Signature: {(exitus616,5);(f0,7);(f12,7);(f25,7);(f34,7)} Rule Graph: [0->{1,4},1->{1,4},2->{2,3},3->{5},4->{2,3}] ,We construct a looptree: P: [0,1,2,3,4,5] | +- p:[1] c: [1] | `- p:[2] c: [2]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,C,D,E,F,0.0,0.1] f0 ~> f12 [A <= unknown, C <= unknown, D <= 0*K, E <= E, F <= F] f12 ~> f12 [A <= A, C <= C, D <= C, E <= E, F <= F] f25 ~> f25 [A <= A, C <= C, D <= D, E <= E, F <= E] f25 ~> f34 [A <= A, C <= C, D <= D, E <= E, F <= F] f12 ~> f25 [A <= A, C <= C, D <= D, E <= A, F <= 0*K] f34 ~> exitus616 [A <= A, C <= C, D <= D, E <= E, F <= F] + Loop: [0.0 <= K + C + D] f12 ~> f12 [A <= A, C <= C, D <= C, E <= E, F <= F] + Loop: [0.1 <= K + E + F] f25 ~> f25 [A <= A, C <= C, D <= D, E <= E, F <= E] + Applied Processor: AbstractFlow + Details: () * Step 7: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,C,D,E,F,0.0,0.1] f0 ~> f12 [K ~=> D,huge ~=> A,huge ~=> C] f12 ~> f12 [C ~=> D] f25 ~> f25 [E ~=> F] f25 ~> f34 [] f12 ~> f25 [A ~=> E,K ~=> F] f34 ~> exitus616 [] + Loop: [C ~+> 0.0,D ~+> 0.0,K ~+> 0.0] f12 ~> f12 [C ~=> D] + Loop: [E ~+> 0.1,F ~+> 0.1,K ~+> 0.1] f25 ~> f25 [E ~=> F] + Applied Processor: Lare + Details: Unknown bound. MAYBE