MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (?,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (?,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (?,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (?,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: PolyRank MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (1,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (1,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (1,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (1,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalEx2bb1in) = x2 p(evalEx2bb2in) = x2 p(evalEx2bb3in) = x2 p(evalEx2bbin) = x2 p(evalEx2entryin) = x1 p(evalEx2returnin) = x2 p(evalEx2start) = x1 p(evalEx2stop) = x2 Following rules are strictly oriented: [-1 + B + -1*D >= 0 ==> && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalEx2bb2in(A,B,C,D) = B > D = evalEx2bb3in(C,D,C,D) Following rules are weakly oriented: True ==> evalEx2start(A,B,C,D) = A >= A = evalEx2entryin(A,B,C,D) True ==> evalEx2entryin(A,B,C,D) = A >= A = evalEx2bb3in(B,A,C,D) [B >= 1 && A >= 1] ==> evalEx2bb3in(A,B,C,D) = B >= B = evalEx2bbin(A,B,C,D) [0 >= B] ==> evalEx2bb3in(A,B,C,D) = B >= B = evalEx2returnin(A,B,C,D) [0 >= A] ==> evalEx2bb3in(A,B,C,D) = B >= B = evalEx2returnin(A,B,C,D) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] ==> evalEx2bbin(A,B,C,D) = B >= B = evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B + -1*D >= 0 ==> && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] evalEx2bb2in(A,B,C,D) = B >= B = evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 ==> && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] evalEx2bb2in(A,B,C,D) = B >= B = evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 ==> && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalEx2bb1in(A,B,C,D) = B >= B = evalEx2bb2in(A,B,1 + C,-1 + D) True ==> evalEx2returnin(A,B,C,D) = B >= B = evalEx2stop(A,B,C,D) * Step 3: KnowledgePropagation MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (1,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (1,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (1,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (A,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (1,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 4: Failure MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (1,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (1 + A,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (1,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (1,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (1 + A,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (A,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (1,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE