YES(?,ELEMENTARY) 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: YES(?,ELEMENTARY) Input Problem: innermost runtime-complexity with respect to Rules: { not(x) -> xor(x, true()) , implies(x, y) -> xor(and(x, y), xor(x, true())) , or(x, y) -> xor(and(x, y), xor(x, y)) , =(x, y) -> xor(x, xor(y, true()))} Proof Output: Strict Rules in Predicative Notation: { not(; x) -> xor(; x, true()) , implies(; x, y) -> xor(; and(; x, y), xor(; x, true())) , or(y; x) -> xor(; and(; x, y), xor(; x, y)) , =(x; y) -> xor(; x, xor(; y, true()))} Safe Mapping: safe(not) = {1}, safe(xor) = {1, 2}, safe(true) = {}, safe(implies) = {1, 2}, safe(and) = {1, 2}, safe(or) = {1}, safe(=) = {2} Argument Permutation: mu(not) = [1], mu(implies) = [1, 2], mu(or) = [2, 1], mu(=) = [2, 1] Precedence: = ~ =, = > or, = > implies, = > not, or ~ or, or > implies, or > not, implies ~ implies, implies > not, not ~ not