YES(?,O(1)) * Step 1: UnsatRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A) -> a(A) [A >= 1] (1,1) 1. start(A) -> a(A) [A >= 2] (1,1) 2. start(A) -> a(A) [A >= 4] (1,1) 3. a(A) -> a(A*B) [1 >= 2*B && 3*B >= 2 && A >= 2] (?,1) Signature: {(a,1);(start,1)} Flow Graph: [0->{3},1->{3},2->{3},3->{3}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [3] * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A) -> a(A) [A >= 1] (1,1) 1. start(A) -> a(A) [A >= 2] (1,1) 2. start(A) -> a(A) [A >= 4] (1,1) Signature: {(a,1);(start,1)} Flow Graph: [0->{},1->{},2->{}] + Applied Processor: UnsatPaths + Details: The problem is already solved. YES(?,O(1))