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