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