MAYBE 1109.91/298.01 MAYBE 1109.91/298.01 1109.91/298.01 We are left with following problem, upon which TcT provides the 1109.91/298.01 certificate MAYBE. 1109.91/298.01 1109.91/298.01 Strict Trs: 1109.91/298.01 { start(i) -> 1109.91/298.01 busy(F(), closed(), stop(), false(), false(), false(), i) 1109.91/298.01 , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(F(), d, stop(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), open(), stop(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(F(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(F(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(F(), closed(), stop(), false(), false(), true(), i) -> 1109.91/298.01 idle(F(), closed(), up(), false(), false(), true(), i) 1109.91/298.01 , busy(F(), closed(), stop(), true(), false(), b3, i) -> 1109.91/298.01 idle(F(), closed(), down(), true(), false(), b3, i) 1109.91/298.01 , busy(F(), closed(), up(), b1, false(), b3, i) -> 1109.91/298.01 idle(FS(), closed(), up(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), up(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, true(), b3, i) 1109.91/298.01 , busy(F(), closed(), down(), b1, false(), b3, i) -> 1109.91/298.01 idle(BF(), closed(), down(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), down(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, true(), b3, i) 1109.91/298.01 , busy(F(), open(), stop(), b1, false(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, false(), b3, i) 1109.91/298.01 , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(BF(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(F(), closed(), up(), b1, b2, b3, i) 1109.91/298.01 , busy(BF(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), down(), b1, b2, b3, i) 1109.91/298.01 , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(FS(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(S(), closed(), up(), b1, b2, b3, i) 1109.91/298.01 , busy(FS(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(F(), closed(), down(), b1, b2, b3, i) 1109.91/298.01 , busy(B(), d, stop(), true(), b2, b3, i) -> 1109.91/298.01 idle(B(), open(), stop(), false(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(B(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(B(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(B(), closed(), stop(), false(), false(), true(), i) -> 1109.91/298.01 idle(B(), closed(), up(), false(), false(), true(), i) 1109.91/298.01 , busy(B(), closed(), stop(), false(), true(), b3, i) -> 1109.91/298.01 idle(B(), closed(), up(), false(), true(), b3, i) 1109.91/298.01 , busy(B(), closed(), up(), false(), b2, b3, i) -> 1109.91/298.01 idle(BF(), closed(), up(), false(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), up(), true(), b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), true(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), b1, b2, b3, i) 1109.91/298.01 , busy(B(), open(), stop(), false(), b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), false(), b2, b3, i) 1109.91/298.01 , busy(S(), d, stop(), b1, b2, true(), i) -> 1109.91/298.01 idle(S(), open(), stop(), b1, b2, false(), i) 1109.91/298.01 , busy(S(), closed(), stop(), b1, true(), false(), i) -> 1109.91/298.01 idle(S(), closed(), down(), b1, true(), false(), i) 1109.91/298.01 , busy(S(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(S(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(S(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(S(), closed(), stop(), true(), false(), false(), i) -> 1109.91/298.01 idle(S(), closed(), down(), true(), false(), false(), i) 1109.91/298.01 , busy(S(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, b3, i) 1109.91/298.01 , busy(S(), closed(), down(), b1, b2, false(), i) -> 1109.91/298.01 idle(FS(), closed(), down(), b1, b2, false(), i) 1109.91/298.01 , busy(S(), closed(), down(), b1, b2, true(), i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, true(), i) 1109.91/298.01 , busy(S(), open(), stop(), b1, b2, false(), i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, false(), i) 1109.91/298.01 , idle(fl, d, m, b1, b2, b3, empty()) -> 1109.91/298.01 busy(fl, d, m, b1, b2, b3, empty()) 1109.91/298.01 , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> 1109.91/298.01 busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i) 1109.91/298.01 , or(false(), b) -> b 1109.91/298.01 , or(true(), b) -> true() } 1109.91/298.01 Obligation: 1109.91/298.01 runtime complexity 1109.91/298.01 Answer: 1109.91/298.01 MAYBE 1109.91/298.01 1109.91/298.01 The input is overlay and right-linear. Switching to innermost 1109.91/298.01 rewriting. 1109.91/298.01 1109.91/298.01 We are left with following problem, upon which TcT provides the 1109.91/298.01 certificate MAYBE. 1109.91/298.01 1109.91/298.01 Strict Trs: 1109.91/298.01 { start(i) -> 1109.91/298.01 busy(F(), closed(), stop(), false(), false(), false(), i) 1109.91/298.01 , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(F(), d, stop(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), open(), stop(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(F(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(F(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(F(), closed(), stop(), false(), false(), true(), i) -> 1109.91/298.01 idle(F(), closed(), up(), false(), false(), true(), i) 1109.91/298.01 , busy(F(), closed(), stop(), true(), false(), b3, i) -> 1109.91/298.01 idle(F(), closed(), down(), true(), false(), b3, i) 1109.91/298.01 , busy(F(), closed(), up(), b1, false(), b3, i) -> 1109.91/298.01 idle(FS(), closed(), up(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), up(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, true(), b3, i) 1109.91/298.01 , busy(F(), closed(), down(), b1, false(), b3, i) -> 1109.91/298.01 idle(BF(), closed(), down(), b1, false(), b3, i) 1109.91/298.01 , busy(F(), closed(), down(), b1, true(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, true(), b3, i) 1109.91/298.01 , busy(F(), open(), stop(), b1, false(), b3, i) -> 1109.91/298.01 idle(F(), closed(), stop(), b1, false(), b3, i) 1109.91/298.01 , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(BF(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(F(), closed(), up(), b1, b2, b3, i) 1109.91/298.01 , busy(BF(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), down(), b1, b2, b3, i) 1109.91/298.01 , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect() 1109.91/298.01 , busy(FS(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(S(), closed(), up(), b1, b2, b3, i) 1109.91/298.01 , busy(FS(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(F(), closed(), down(), b1, b2, b3, i) 1109.91/298.01 , busy(B(), d, stop(), true(), b2, b3, i) -> 1109.91/298.01 idle(B(), open(), stop(), false(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(B(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(B(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(B(), closed(), stop(), false(), false(), true(), i) -> 1109.91/298.01 idle(B(), closed(), up(), false(), false(), true(), i) 1109.91/298.01 , busy(B(), closed(), stop(), false(), true(), b3, i) -> 1109.91/298.01 idle(B(), closed(), up(), false(), true(), b3, i) 1109.91/298.01 , busy(B(), closed(), up(), false(), b2, b3, i) -> 1109.91/298.01 idle(BF(), closed(), up(), false(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), up(), true(), b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), true(), b2, b3, i) 1109.91/298.01 , busy(B(), closed(), down(), b1, b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), b1, b2, b3, i) 1109.91/298.01 , busy(B(), open(), stop(), false(), b2, b3, i) -> 1109.91/298.01 idle(B(), closed(), stop(), false(), b2, b3, i) 1109.91/298.01 , busy(S(), d, stop(), b1, b2, true(), i) -> 1109.91/298.01 idle(S(), open(), stop(), b1, b2, false(), i) 1109.91/298.01 , busy(S(), closed(), stop(), b1, true(), false(), i) -> 1109.91/298.01 idle(S(), closed(), down(), b1, true(), false(), i) 1109.91/298.01 , busy(S(), closed(), stop(), false(), false(), false(), empty()) 1109.91/298.01 -> correct() 1109.91/298.01 , busy(S(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 -> 1109.91/298.01 idle(S(), 1109.91/298.01 closed(), 1109.91/298.01 stop(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 false(), 1109.91/298.01 newbuttons(i1, i2, i3, i)) 1109.91/298.01 , busy(S(), closed(), stop(), true(), false(), false(), i) -> 1109.91/298.01 idle(S(), closed(), down(), true(), false(), false(), i) 1109.91/298.01 , busy(S(), closed(), up(), b1, b2, b3, i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, b3, i) 1109.91/298.01 , busy(S(), closed(), down(), b1, b2, false(), i) -> 1109.91/298.01 idle(FS(), closed(), down(), b1, b2, false(), i) 1109.91/298.01 , busy(S(), closed(), down(), b1, b2, true(), i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, true(), i) 1109.91/298.01 , busy(S(), open(), stop(), b1, b2, false(), i) -> 1109.91/298.01 idle(S(), closed(), stop(), b1, b2, false(), i) 1109.91/298.01 , idle(fl, d, m, b1, b2, b3, empty()) -> 1109.91/298.01 busy(fl, d, m, b1, b2, b3, empty()) 1109.91/298.01 , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> 1109.91/298.01 busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i) 1109.91/298.01 , or(false(), b) -> b 1109.91/298.01 , or(true(), b) -> true() } 1109.91/298.01 Obligation: 1109.91/298.01 innermost runtime complexity 1109.91/298.01 Answer: 1109.91/298.01 MAYBE 1109.91/298.01 1109.91/298.01 None of the processors succeeded. 1109.91/298.01 1109.91/298.01 Details of failed attempt(s): 1109.91/298.01 ----------------------------- 1109.91/298.01 1) 'empty' failed due to the following reason: 1109.91/298.01 1109.91/298.01 Empty strict component of the problem is NOT empty. 1109.91/298.01 1109.91/298.01 2) 'Best' failed due to the following reason: 1109.91/298.01 1109.91/298.01 None of the processors succeeded. 1109.91/298.01 1109.91/298.01 Details of failed attempt(s): 1109.91/298.01 ----------------------------- 1109.91/298.01 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1109.91/298.01 following reason: 1109.91/298.01 1109.91/298.01 Computation stopped due to timeout after 297.0 seconds. 1109.91/298.01 1109.91/298.01 2) 'Best' failed due to the following reason: 1109.91/298.01 1109.91/298.01 None of the processors succeeded. 1109.91/298.01 1109.91/298.01 Details of failed attempt(s): 1109.91/298.01 ----------------------------- 1109.91/298.01 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1109.91/298.01 seconds)' failed due to the following reason: 1109.91/298.01 1109.91/298.01 Computation stopped due to timeout after 148.0 seconds. 1109.91/298.01 1109.91/298.01 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1109.91/298.01 failed due to the following reason: 1109.91/298.01 1109.91/298.01 Computation stopped due to timeout after 24.0 seconds. 1109.91/298.01 1109.91/298.01 3) 'Best' failed due to the following reason: 1109.91/298.01 1109.91/298.01 None of the processors succeeded. 1109.91/298.01 1109.91/298.01 Details of failed attempt(s): 1109.91/298.01 ----------------------------- 1109.91/298.01 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1109.91/298.01 to the following reason: 1109.91/298.01 1109.91/298.01 The input cannot be shown compatible 1109.91/298.01 1109.91/298.01 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1109.91/298.01 following reason: 1109.91/298.01 1109.91/298.01 The input cannot be shown compatible 1109.91/298.01 1109.91/298.01 1109.91/298.01 1109.91/298.01 1109.91/298.01 1109.91/298.01 Arrrr.. 1110.06/298.13 EOF