YES(?,PRIMREC) * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{3,4,5 ,6,7,8},9->{2},10->{2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,3),(8,4),(8,5),(8,6),(8,7),(8,8)] * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{} ,9->{2},10->{2}] + Applied Processor: AddSinks + Details: () * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) 11. eval3(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4);(exitus616,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8,11},3->{9,10},4->{9,10},5->{3,4,5,6,7,8,11},6->{3,4,5,6,7,8,11},7->{9,10} ,8->{3,4,5,6,7,8,11},9->{2},10->{2},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,3),(8,4),(8,5),(8,6),(8,7),(8,8)] * Step 4: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) 11. eval3(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4);(exitus616,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8,11},3->{9,10},4->{9,10},5->{3,4,5,6,7,8,11},6->{3,4,5,6,7,8,11},7->{9,10} ,8->{11},9->{2},10->{2},11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[2,9,3,5,6,4,7,10] c: [10] | `- p:[2,9,3,5,6,4,7] c: [9] | `- p:[5,6] c: [6] | `- p:[5] c: [5] * Step 5: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) 11. eval3(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4);(exitus616,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8,11},3->{9,10},4->{9,10},5->{3,4,5,6,7,8,11},6->{3,4,5,6,7,8,11},7->{9,10} ,8->{11},9->{2},10->{2},11->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[2,9,3,5,6,4,7,10] c: [10] | `- p:[2,9,3,5,6,4,7] c: [9] | `- p:[5,6] c: [6] | `- p:[5] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 6: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0,0.0.0.0,0.0.0.0.0] eval1 ~> eval2 [A <= A, B <= B, C <= C, D <= D] eval1 ~> eval2 [A <= A, B <= K + B, C <= C, D <= D] eval2 ~> eval3 [A <= A, B <= B, C <= A, D <= 2*A] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= K + D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, C <= B, D <= K + B + D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] eval4 ~> eval2 [A <= A, B <= B, C <= C, D <= D] eval4 ~> eval2 [A <= A, B <= B, C <= C, D <= D] eval3 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= B] eval2 ~> eval3 [A <= A, B <= B, C <= A, D <= 2*A] eval4 ~> eval2 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, C <= B, D <= K + B + D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= K + D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] eval4 ~> eval2 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= A] eval2 ~> eval3 [A <= A, B <= B, C <= A, D <= 2*A] eval4 ~> eval2 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, C <= B, D <= K + B + D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= K + D] eval3 ~> eval4 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0.0 <= K + B + D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, C <= B, D <= K + B + D] + Loop: [0.0.0.0.0 <= B + D] eval3 ~> eval3 [A <= A, B <= B, C <= D, D <= B + D] + Applied Processor: FlowAbstraction + Details: () * Step 7: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0,0.0.0.0,0.0.0.0.0] eval1 ~> eval2 [] eval1 ~> eval2 [B ~+> B,K ~+> B] eval2 ~> eval3 [A ~=> C,A ~*> D] eval3 ~> eval4 [] eval3 ~> eval4 [D ~+> D,K ~+> D] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] eval3 ~> eval3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3 ~> eval4 [] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] eval4 ~> eval2 [] eval4 ~> eval2 [] eval3 ~> exitus616 [] + Loop: [B ~=> 0.0] eval2 ~> eval3 [A ~=> C,A ~*> D] eval4 ~> eval2 [] eval3 ~> eval4 [] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] eval3 ~> eval3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3 ~> eval4 [D ~+> D,K ~+> D] eval3 ~> eval4 [] eval4 ~> eval2 [] + Loop: [A ~=> 0.0.0] eval2 ~> eval3 [A ~=> C,A ~*> D] eval4 ~> eval2 [] eval3 ~> eval4 [] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] eval3 ~> eval3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3 ~> eval4 [D ~+> D,K ~+> D] eval3 ~> eval4 [] + Loop: [B ~+> 0.0.0.0,D ~+> 0.0.0.0,K ~+> 0.0.0.0] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] eval3 ~> eval3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] + Loop: [B ~+> 0.0.0.0.0,D ~+> 0.0.0.0.0] eval3 ~> eval3 [D ~=> C,B ~+> D,D ~+> D] + Applied Processor: LareProcessor + Details: eval1 ~> exitus616 [A ~=> C ,A ~=> 0.0.0 ,B ~=> C ,B ~=> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> C ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> D ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> tick] + eval3> [A ~=> C ,A ~=> 0.0.0 ,B ~=> C ,B ~=> 0.0 ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> C ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> D ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> tick] + eval3> [A ~=> C ,A ~=> 0.0.0 ,B ~=> C ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> C ,A ~*> D ,A ~*> 0.0.0.0 ,A ~*> 0.0.0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0.0 ,A ~^> 0.0.0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0.0 ,B ~^> 0.0.0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> D ,K ~^> 0.0.0.0 ,K ~^> 0.0.0.0.0 ,K ~^> tick] + eval3> [B ~=> C ,D ~=> C ,B ~+> C ,B ~+> D ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,D ~+> 0.0.0.0 ,D ~+> 0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0.0.0 ,D ~*> tick ,K ~*> D ,K ~*> tick ,B ~^> D ,D ~^> D ,K ~^> D] + eval3> [D ~=> C ,B ~+> C ,B ~+> D ,B ~+> 0.0.0.0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,D ~+> 0.0.0.0.0 ,D ~+> tick ,tick ~+> tick ,B ~*> C ,B ~*> D ,D ~*> D] YES(?,PRIMREC)