MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f1(A,1 + B,D,Q,D,R,B,H,I,J,K,L,M,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,X,W,F,G,Q,T,V,Y,Z,C,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && S >= Q && Q >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(T,V,S,Y,X,F,G,R,U,W,Z,B1,O,Q,O,P) [0 >= R && 0 >= A1] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f1(R,2,U,S,U,F,G,R,T,U,K,L,M,Q,T,V) [R >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,Y,X,F,G,1,T,W,Z,B1,D,Q,V,P) True (1,1) Signature: {(f1,16);(f3,16);(f4,16)} 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,O,P) -> f1(A,1 + B,D,Q,D,R,B,H,I,J,K,L,M,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,X,W,F,G,Q,T,V,Y,Z,C,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && S >= Q && Q >= 2] (1,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(T,V,S,Y,X,F,G,R,U,W,Z,B1,O,Q,O,P) [0 >= R && 0 >= A1] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f1(R,2,U,S,U,F,G,R,T,U,K,L,M,Q,T,V) [R >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,Y,X,F,G,1,T,W,Z,B1,D,Q,V,P) True (1,1) Signature: {(f1,16);(f3,16);(f4,16)} 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,O,P) -> f1(A,1 + B,D,Q,D,R,B,H,I,J,K,L,M,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,X,W,F,G,Q,T,V,Y,Z,C,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && S >= Q && Q >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(T,V,S,Y,X,F,G,R,U,W,Z,B1,O,Q,O,P) [0 >= R && 0 >= A1] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f1(R,2,U,S,U,F,G,R,T,U,K,L,M,Q,T,V) [R >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,Y,X,F,G,1,T,W,Z,B1,D,Q,V,P) True (1,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True (1,1) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True (?,1) Signature: {(exitus616,16);(f1,16);(f3,16);(f4,16)} 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,O,P) -> f1(A,1 + B,D,Q,D,R,B,H,I,J,K,L,M,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && A >= 1 + B && B >= 0] (?,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,X,W,F,G,Q,T,V,Y,Z,C,N,O,P) [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && S >= Q && Q >= 2] (?,1) 2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(T,V,S,Y,X,F,G,R,U,W,Z,B1,O,Q,O,P) [0 >= R && 0 >= A1] (1,1) 3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f1(R,2,U,S,U,F,G,R,T,U,K,L,M,Q,T,V) [R >= 2] (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> f4(R,S,U,Y,X,F,G,1,T,W,Z,B1,D,Q,V,P) True (1,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True (1,1) 6. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True (?,1) Signature: {(exitus616,16);(f1,16);(f3,16);(f4,16)} 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,O,P,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, O <= O, P <= P] 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 <= unknown, M <= C, N <= N, O <= O, P <= P] 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 <= unknown, M <= O, N <= unknown, O <= O, P <= P] f3 ~> f1 [A <= unknown, B <= 2*K, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= unknown, I <= unknown, J <= unknown, K <= K, L <= L, M <= M, N <= unknown, O <= unknown, P <= 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 <= unknown, M <= D, N <= unknown, O <= unknown, P <= P] 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, O <= O, P <= P] 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, O <= O, P <= P] + 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, O <= O, P <= P] + 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,O,P,0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,huge ~=> D,huge ~=> F] f1 ~> f4 [C ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L] f3 ~> f4 [O ~=> M ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N] f3 ~> f1 [K ~=> B ,huge ~=> A ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> I ,huge ~=> J ,huge ~=> N ,huge ~=> O ,huge ~=> P] f3 ~> f4 [D ~=> M ,K ~=> H ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> I ,huge ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> O] 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