YES(?,O(n^1)) * Step 1: UnsatRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (?,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (?,1) 2. eval(A) -> eval(B) [1 >= 2*C (?,1) && 2*C >= 0 && 2*D >= 1 && 1 >= 2*D && 1 >= 2*E && 3*E >= 2 && B >= E && 1 >= 2*F && 3*F >= 2 && F >= B && A = 1] 3. eval(A) -> eval(B) [2*D >= 1 (?,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0,1,2,3},1->{0,1,2,3},2->{0,1,2,3},3->{0,1,2,3},4->{0,1,2,3}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [2] * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (?,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (?,1) 3. eval(A) -> eval(B) [2*D >= 1 (?,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0,1,3},1->{0,1,3},3->{0,1,3},4->{0,1,3}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,0),(0,1),(0,3)] * Step 3: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (?,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (?,1) 3. eval(A) -> eval(B) [2*D >= 1 (?,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{},1->{0,1,3},3->{0,1,3},4->{0,1,3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (1,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (?,1) 3. eval(A) -> eval(B) [2*D >= 1 (?,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{},1->{0,1,3},3->{0,1,3},4->{0,1,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval) = x1 p(start) = x1 Following rules are strictly oriented: [2*B >= 0 && 0 >= 2*B && A = 1] ==> eval(A) = A > 0 = eval(0) [2*D >= 1 ==> && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] eval(A) = A > B = eval(B) Following rules are weakly oriented: [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] ==> eval(A) = A >= 2*B = eval(2*B) True ==> start(A) = A >= A = eval(A) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (1,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (?,1) 3. eval(A) -> eval(B) [2*D >= 1 (A,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{},1->{0,1,3},3->{0,1,3},4->{0,1,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval) = x1 p(start) = x1 Following rules are strictly oriented: [2*B >= 0 && 0 >= 2*B && A = 1] ==> eval(A) = A > 0 = eval(0) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] ==> eval(A) = A > 2*B = eval(2*B) Following rules are weakly oriented: [2*D >= 1 ==> && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] eval(A) = A >= B = eval(B) True ==> start(A) = A >= A = eval(A) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(0) [2*B >= 0 && 0 >= 2*B && A = 1] (1,1) 1. eval(A) -> eval(2*B) [2*B >= 0 && 2 + 2*B >= 0 && A = 1 + 2*B] (A,1) 3. eval(A) -> eval(B) [2*D >= 1 (A,1) && 1 + 2*D >= 0 && 2*D >= 2*C && 1 + 2*C >= 2*D && 2*D >= 2*E && 3*E >= 1 + 2*D && B >= E && 2*D >= 2*F && 3*F >= 1 + 2*D && F >= B && A = 2*D] 4. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{},1->{0,1,3},3->{0,1,3},4->{0,1,3}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))