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 = Z3} + Details: Signatures used: ---------------- = :: [A(14) x A(14)] -(14)-> A(0) and :: [A(0) x A(0)] -(0)-> A(0) and :: [A(4) x A(0)] -(4)-> A(4) implies :: [A(6) x A(14)] -(14)-> A(0) not :: [A(12)] -(15)-> A(0) or :: [A(14) x A(14)] -(14)-> A(0) true :: [] -(0)-> A(10) true :: [] -(0)-> A(14) true :: [] -(0)-> A(8) xor :: [A(0) x A(0)] -(0)-> A(6) xor :: [A(0) x A(0)] -(0)-> A(14) xor :: [A(0) x A(0)] -(0)-> A(8) xor :: [A(0) x A(0)] -(0)-> A(4) xor :: [A(0) x A(0)] -(0)-> A(10) xor :: [A(0) x A(0)] -(0)-> A(0) xor :: [A(0) x A(0)] -(0)-> A(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- and_A :: [A(1) x A(0)] -(1)-> 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))