MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: ack_in(0(),n) -> ack_out(s(n)) ack_in(s(m),0()) -> u11(ack_in(m,s(0()))) ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) u11(ack_out(n)) -> ack_out(n) u21(ack_out(n),m) -> u22(ack_in(m,n)) u22(ack_out(n)) -> ack_out(n) - Signature: {ack_in/2,u11/1,u21/2,u22/1} / {0/0,ack_out/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack_in,u11,u21,u22} and constructors {0,ack_out,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: The input can not be schown compatible. MAYBE