MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(A,1 + B,D,O,D,P,B,H,I,J,K,L,M,N) [A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,O,S,V,W,C,M,N) [B >= A && B >= 0 && Q >= O && O >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(R,S,Q,V,U,F,G,P,T,W,Y,0,O,N) [0 >= P && 0 >= X] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(P,2,R,Q,R,F,G,P,R,J,K,L,O,S) [P >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,1,S,V,W,D,O,N) True (1,1) Signature: {(f1,14);(f3,14);(f4,14)} Flow Graph: [0->{0,1},1->{},2->{},3->{0,1},4->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(A,1 + B,D,O,D,P,B,H,I,J,K,L,M,N) [A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,O,S,V,W,C,M,N) [B >= A && B >= 0 && Q >= O && O >= 2] (1,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(R,S,Q,V,U,F,G,P,T,W,Y,0,O,N) [0 >= P && 0 >= X] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(P,2,R,Q,R,F,G,P,R,J,K,L,O,S) [P >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,1,S,V,W,D,O,N) True (1,1) Signature: {(f1,14);(f3,14);(f4,14)} Flow Graph: [0->{0,1},1->{},2->{},3->{0,1},4->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(A,1 + B,D,O,D,P,B,H,I,J,K,L,M,N) [A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,O,S,V,W,C,M,N) [B >= A && B >= 0 && Q >= O && O >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(R,S,Q,V,U,F,G,P,T,W,Y,0,O,N) [0 >= P && 0 >= X] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(P,2,R,Q,R,F,G,P,R,J,K,L,O,S) [P >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,1,S,V,W,D,O,N) True (1,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (?,1) Signature: {(exitus616,14);(f1,14);(f3,14);(f4,14)} Flow Graph: [0->{0,1,6},1->{},2->{},3->{0,1,6},4->{},5->{},6->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[0] c: [0] * Step 4: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(A,1 + B,D,O,D,P,B,H,I,J,K,L,M,N) [A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,O,S,V,W,C,M,N) [B >= A && B >= 0 && Q >= O && O >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(R,S,Q,V,U,F,G,P,T,W,Y,0,O,N) [0 >= P && 0 >= X] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(P,2,R,Q,R,F,G,P,R,J,K,L,O,S) [P >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,1,S,V,W,D,O,N) True (1,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (?,1) Signature: {(exitus616,14);(f1,14);(f3,14);(f4,14)} Flow Graph: [0->{0,1,6},1->{},2->{},3->{0,1,6},4->{},5->{},6->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[0] c: [0]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,M,N,0.0] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= D, F <= unknown, G <= B, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N] f1 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= unknown, I <= unknown, J <= unknown, K <= unknown, L <= C, M <= M, N <= N] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= unknown, I <= unknown, J <= unknown, K <= unknown, L <= 0*K, M <= unknown, N <= N] f3 ~> f1 [A <= unknown, B <= 2*K, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= unknown, I <= unknown, J <= J, K <= K, L <= L, M <= unknown, N <= unknown] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= K, I <= unknown, J <= unknown, K <= unknown, L <= D, M <= unknown, N <= N] f3 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N] f1 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N] + Loop: [0.0 <= A + B] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= D, F <= unknown, G <= B, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N] + Applied Processor: FlowAbstraction + Details: () * Step 6: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,huge ~=> D,huge ~=> F] f1 ~> f4 [C ~=> L ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K] f3 ~> f4 [K ~=> L ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> M] f3 ~> f1 [K ~=> B ,huge ~=> A ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> M ,huge ~=> N] f3 ~> f4 [D ~=> L ,K ~=> H ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> M] f3 ~> exitus616 [] f1 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,huge ~=> D,huge ~=> F] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE