MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { start(i) -> busy(F(), closed(), stop(), false(), false(), false(), i) , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect() , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect() , busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i) , busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct() , busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) , busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i) , busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i) , busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i) , busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i) , busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i) , busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i) , busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i) , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect() , busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i) , busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i) , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect() , busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i) , busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i) , busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i) , busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct() , busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) , busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i) , busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i) , busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i) , busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i) , busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i) , busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i) , busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i) , busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i) , busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct() , busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) , busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i) , busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i) , busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i) , busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i) , busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i) , idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()) , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i) , or(false(), b) -> b , or(true(), b) -> true() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. Arrrr..