MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: f(x) -> g(f(x)) g(x) -> a() g(f(x)) -> x - Signature: {f/1,g/1} / {a/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {a} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. g(f(x)) -> x All above mentioned rules can be savely removed. * Step 2: Failure MAYBE timed out MAYBE