WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: implies(x,or(y,z)) -> or(y,implies(x,z)) implies(not(x),y) -> or(x,y) implies(not(x),or(y,z)) -> implies(y,or(x,z)) - Signature: {implies/2} / {not/1,or/2} - Obligation: innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: Signatures used: ---------------- implies :: [A(2) x A(2)] -(0)-> A(0) not :: [A(2)] -(2)-> A(2) or :: [A(2) x A(2)] -(2)-> A(2) or :: [A(0) x A(0)] -(0)-> A(0) Cost-free Signatures used: -------------------------- implies :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) not :: [A_cf(0)] -(0)-> A_cf(0) or :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- not_A :: [A(1)] -(1)-> A(1) or_A :: [A(1) x A(1)] -(1)-> A(1) * Step 2: Open MAYBE - Strict TRS: implies(x,or(y,z)) -> or(y,implies(x,z)) implies(not(x),y) -> or(x,y) implies(not(x),or(y,z)) -> implies(y,or(x,z)) - Signature: {implies/2} / {not/1,or/2} - Obligation: innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or} Following problems could not be solved: - Strict TRS: implies(x,or(y,z)) -> or(y,implies(x,z)) implies(not(x),y) -> or(x,y) implies(not(x),or(y,z)) -> implies(y,or(x,z)) - Signature: {implies/2} / {not/1,or/2} - Obligation: innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or} WORST_CASE(?,O(n^1))