YES(O(1),O(n^2)) 1177.80/297.26 YES(O(1),O(n^2)) 1177.80/297.26 1177.80/297.26 We are left with following problem, upon which TcT provides the 1177.80/297.26 certificate YES(O(1),O(n^2)). 1177.80/297.26 1177.80/297.26 Strict Trs: 1177.80/297.26 { start(i) -> 1177.80/297.26 busy(F(), closed(), stop(), false(), false(), false(), i) 1177.80/297.26 , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(F(), d, stop(), b1, true(), b3, i) -> 1177.80/297.26 idle(F(), open(), stop(), b1, false(), b3, i) 1177.80/297.26 , busy(F(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(F(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 -> 1177.80/297.26 idle(F(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 , busy(F(), closed(), stop(), false(), false(), true(), i) -> 1177.80/297.26 idle(F(), closed(), up(), false(), false(), true(), i) 1177.80/297.26 , busy(F(), closed(), stop(), true(), false(), b3, i) -> 1177.80/297.26 idle(F(), closed(), down(), true(), false(), b3, i) 1177.80/297.26 , busy(F(), closed(), up(), b1, false(), b3, i) -> 1177.80/297.26 idle(FS(), closed(), up(), b1, false(), b3, i) 1177.80/297.26 , busy(F(), closed(), up(), b1, true(), b3, i) -> 1177.80/297.26 idle(F(), closed(), stop(), b1, true(), b3, i) 1177.80/297.26 , busy(F(), closed(), down(), b1, false(), b3, i) -> 1177.80/297.26 idle(BF(), closed(), down(), b1, false(), b3, i) 1177.80/297.26 , busy(F(), closed(), down(), b1, true(), b3, i) -> 1177.80/297.26 idle(F(), closed(), stop(), b1, true(), b3, i) 1177.80/297.26 , busy(F(), open(), stop(), b1, false(), b3, i) -> 1177.80/297.26 idle(F(), closed(), stop(), b1, false(), b3, i) 1177.80/297.26 , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(BF(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.26 idle(F(), closed(), up(), b1, b2, b3, i) 1177.80/297.26 , busy(BF(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.26 idle(B(), closed(), down(), b1, b2, b3, i) 1177.80/297.26 , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(FS(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.26 idle(S(), closed(), up(), b1, b2, b3, i) 1177.80/297.26 , busy(FS(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.26 idle(F(), closed(), down(), b1, b2, b3, i) 1177.80/297.26 , busy(B(), d, stop(), true(), b2, b3, i) -> 1177.80/297.26 idle(B(), open(), stop(), false(), b2, b3, i) 1177.80/297.26 , busy(B(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(B(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 -> 1177.80/297.26 idle(B(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 , busy(B(), closed(), stop(), false(), false(), true(), i) -> 1177.80/297.26 idle(B(), closed(), up(), false(), false(), true(), i) 1177.80/297.26 , busy(B(), closed(), stop(), false(), true(), b3, i) -> 1177.80/297.26 idle(B(), closed(), up(), false(), true(), b3, i) 1177.80/297.26 , busy(B(), closed(), up(), false(), b2, b3, i) -> 1177.80/297.26 idle(BF(), closed(), up(), false(), b2, b3, i) 1177.80/297.26 , busy(B(), closed(), up(), true(), b2, b3, i) -> 1177.80/297.26 idle(B(), closed(), stop(), true(), b2, b3, i) 1177.80/297.26 , busy(B(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.26 idle(B(), closed(), stop(), b1, b2, b3, i) 1177.80/297.26 , busy(B(), open(), stop(), false(), b2, b3, i) -> 1177.80/297.26 idle(B(), closed(), stop(), false(), b2, b3, i) 1177.80/297.26 , busy(S(), d, stop(), b1, b2, true(), i) -> 1177.80/297.26 idle(S(), open(), stop(), b1, b2, false(), i) 1177.80/297.26 , busy(S(), closed(), stop(), b1, true(), false(), i) -> 1177.80/297.26 idle(S(), closed(), down(), b1, true(), false(), i) 1177.80/297.26 , busy(S(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(S(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 -> 1177.80/297.26 idle(S(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i)) 1177.80/297.26 , busy(S(), closed(), stop(), true(), false(), false(), i) -> 1177.80/297.26 idle(S(), closed(), down(), true(), false(), false(), i) 1177.80/297.26 , busy(S(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.26 idle(S(), closed(), stop(), b1, b2, b3, i) 1177.80/297.26 , busy(S(), closed(), down(), b1, b2, false(), i) -> 1177.80/297.26 idle(FS(), closed(), down(), b1, b2, false(), i) 1177.80/297.26 , busy(S(), closed(), down(), b1, b2, true(), i) -> 1177.80/297.26 idle(S(), closed(), stop(), b1, b2, true(), i) 1177.80/297.26 , busy(S(), open(), stop(), b1, b2, false(), i) -> 1177.80/297.26 idle(S(), closed(), stop(), b1, b2, false(), i) 1177.80/297.26 , idle(fl, d, m, b1, b2, b3, empty()) -> 1177.80/297.26 busy(fl, d, m, b1, b2, b3, empty()) 1177.80/297.26 , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> 1177.80/297.26 busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i) 1177.80/297.26 , or(false(), b) -> b 1177.80/297.26 , or(true(), b) -> true() } 1177.80/297.26 Obligation: 1177.80/297.26 derivational complexity 1177.80/297.26 Answer: 1177.80/297.26 YES(O(1),O(n^2)) 1177.80/297.26 1177.80/297.26 We use the processor 'matrix interpretation of dimension 1' to 1177.80/297.26 orient following rules strictly. 1177.80/297.26 1177.80/297.26 Trs: 1177.80/297.26 { start(i) -> 1177.80/297.26 busy(F(), closed(), stop(), false(), false(), false(), i) 1177.80/297.26 , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(F(), d, stop(), b1, true(), b3, i) -> 1177.80/297.26 idle(F(), open(), stop(), b1, false(), b3, i) 1177.80/297.26 , busy(F(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(F(), open(), stop(), b1, false(), b3, i) -> 1177.80/297.26 idle(F(), closed(), stop(), b1, false(), b3, i) 1177.80/297.26 , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect() 1177.80/297.26 , busy(B(), d, stop(), true(), b2, b3, i) -> 1177.80/297.26 idle(B(), open(), stop(), false(), b2, b3, i) 1177.80/297.26 , busy(B(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(B(), open(), stop(), false(), b2, b3, i) -> 1177.80/297.26 idle(B(), closed(), stop(), false(), b2, b3, i) 1177.80/297.26 , busy(S(), d, stop(), b1, b2, true(), i) -> 1177.80/297.26 idle(S(), open(), stop(), b1, b2, false(), i) 1177.80/297.26 , busy(S(), closed(), stop(), false(), false(), false(), empty()) 1177.80/297.26 -> correct() 1177.80/297.26 , busy(S(), open(), stop(), b1, b2, false(), i) -> 1177.80/297.26 idle(S(), closed(), stop(), b1, b2, false(), i) 1177.80/297.26 , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> 1177.80/297.26 busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i) } 1177.80/297.26 1177.80/297.26 The induced complexity on above rules (modulo remaining rules) is 1177.80/297.26 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1177.80/297.26 none of the weakly oriented rules is size-increasing. The overall 1177.80/297.26 complexity is obtained by composition . 1177.80/297.26 1177.80/297.26 Sub-proof: 1177.80/297.26 ---------- 1177.80/297.26 TcT has computed the following triangular matrix interpretation. 1177.80/297.26 1177.80/297.26 [start](x1) = [1] x1 + [2] 1177.80/297.26 1177.80/297.26 [busy](x1, x2, x3, x4, x5, x6, x7) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [1] x6 + [1] x7 + [1] 1177.80/297.26 1177.80/297.26 [F] = [0] 1177.80/297.26 1177.80/297.26 [closed] = [0] 1177.80/297.26 1177.80/297.26 [stop] = [0] 1177.80/297.26 1177.80/297.26 [false] = [0] 1177.80/297.26 1177.80/297.26 [BF] = [0] 1177.80/297.26 1177.80/297.26 [incorrect] = [0] 1177.80/297.26 1177.80/297.26 [FS] = [0] 1177.80/297.26 1177.80/297.26 [open] = [1] 1177.80/297.26 1177.80/297.26 [up] = [0] 1177.80/297.26 1177.80/297.26 [down] = [0] 1177.80/297.26 1177.80/297.26 [B] = [0] 1177.80/297.26 1177.80/297.26 [empty] = [0] 1177.80/297.26 1177.80/297.26 [correct] = [0] 1177.80/297.26 1177.80/297.26 [S] = [0] 1177.80/297.26 1177.80/297.26 [newbuttons](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] 1177.80/297.26 1177.80/297.26 [idle](x1, x2, x3, x4, x5, x6, x7) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [1] x6 + [1] x7 + [1] 1177.80/297.26 1177.80/297.26 [true] = [2] 1177.80/297.26 1177.80/297.26 [or](x1, x2) = [1] x1 + [1] x2 + [0] 1177.80/297.26 1177.80/297.26 The order satisfies the following ordering constraints: 1177.80/297.26 1177.80/297.26 [start(i)] = [1] i + [2] 1177.80/297.26 > [1] i + [1] 1177.80/297.26 = [busy(F(), closed(), stop(), false(), false(), false(), i)] 1177.80/297.26 1177.80/297.26 [busy(fl, open(), up(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] fl + [2] 1177.80/297.26 > [0] 1177.80/297.26 = [incorrect()] 1177.80/297.26 1177.80/297.26 [busy(fl, open(), down(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] fl + [2] 1177.80/297.26 > [0] 1177.80/297.26 = [incorrect()] 1177.80/297.26 1177.80/297.26 [busy(F(), d, stop(), b1, true(), b3, i)] = [1] i + [1] d + [1] b1 + [1] b3 + [3] 1177.80/297.26 > [1] i + [1] b1 + [1] b3 + [2] 1177.80/297.26 = [idle(F(), open(), stop(), b1, false(), b3, i)] 1177.80/297.26 1177.80/297.26 [busy(F(), closed(), stop(), false(), false(), false(), empty())] = [1] 1177.80/297.26 > [0] 1177.80/297.26 = [correct()] 1177.80/297.26 1177.80/297.26 [busy(F(), = [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i))] 1177.80/297.26 >= [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.26 = [idle(F(), 1177.80/297.26 closed(), 1177.80/297.26 stop(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 false(), 1177.80/297.26 newbuttons(i1, i2, i3, i))] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), stop(), false(), false(), true(), i)] = [1] i + [3] 1177.80/297.27 >= [1] i + [3] 1177.80/297.27 = [idle(F(), closed(), up(), false(), false(), true(), i)] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), stop(), true(), false(), b3, i)] = [1] i + [1] b3 + [3] 1177.80/297.27 >= [1] i + [1] b3 + [3] 1177.80/297.27 = [idle(F(), closed(), down(), true(), false(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), up(), b1, false(), b3, i)] = [1] i + [1] b1 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b3 + [1] 1177.80/297.27 = [idle(FS(), closed(), up(), b1, false(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), up(), b1, true(), b3, i)] = [1] i + [1] b1 + [1] b3 + [3] 1177.80/297.27 >= [1] i + [1] b1 + [1] b3 + [3] 1177.80/297.27 = [idle(F(), closed(), stop(), b1, true(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), down(), b1, false(), b3, i)] = [1] i + [1] b1 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b3 + [1] 1177.80/297.27 = [idle(BF(), closed(), down(), b1, false(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(F(), closed(), down(), b1, true(), b3, i)] = [1] i + [1] b1 + [1] b3 + [3] 1177.80/297.27 >= [1] i + [1] b1 + [1] b3 + [3] 1177.80/297.27 = [idle(F(), closed(), stop(), b1, true(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(F(), open(), stop(), b1, false(), b3, i)] = [1] i + [1] b1 + [1] b3 + [2] 1177.80/297.27 > [1] i + [1] b1 + [1] b3 + [1] 1177.80/297.27 = [idle(F(), closed(), stop(), b1, false(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(BF(), d, stop(), b1, b2, b3, i)] = [1] i + [1] d + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 > [0] 1177.80/297.27 = [incorrect()] 1177.80/297.27 1177.80/297.27 [busy(BF(), closed(), up(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(F(), closed(), up(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(BF(), closed(), down(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(B(), closed(), down(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(FS(), d, stop(), b1, b2, b3, i)] = [1] i + [1] d + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 > [0] 1177.80/297.27 = [incorrect()] 1177.80/297.27 1177.80/297.27 [busy(FS(), closed(), up(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(S(), closed(), up(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(FS(), closed(), down(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(F(), closed(), down(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), d, stop(), true(), b2, b3, i)] = [1] i + [1] d + [1] b2 + [1] b3 + [3] 1177.80/297.27 > [1] i + [1] b2 + [1] b3 + [2] 1177.80/297.27 = [idle(B(), open(), stop(), false(), b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), stop(), false(), false(), false(), empty())] = [1] 1177.80/297.27 > [0] 1177.80/297.27 = [correct()] 1177.80/297.27 1177.80/297.27 [busy(B(), = [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.27 closed(), 1177.80/297.27 stop(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 newbuttons(i1, i2, i3, i))] 1177.80/297.27 >= [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.27 = [idle(B(), 1177.80/297.27 closed(), 1177.80/297.27 stop(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 newbuttons(i1, i2, i3, i))] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), stop(), false(), false(), true(), i)] = [1] i + [3] 1177.80/297.27 >= [1] i + [3] 1177.80/297.27 = [idle(B(), closed(), up(), false(), false(), true(), i)] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), stop(), false(), true(), b3, i)] = [1] i + [1] b3 + [3] 1177.80/297.27 >= [1] i + [1] b3 + [3] 1177.80/297.27 = [idle(B(), closed(), up(), false(), true(), b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), up(), false(), b2, b3, i)] = [1] i + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(BF(), closed(), up(), false(), b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), up(), true(), b2, b3, i)] = [1] i + [1] b2 + [1] b3 + [3] 1177.80/297.27 >= [1] i + [1] b2 + [1] b3 + [3] 1177.80/297.27 = [idle(B(), closed(), stop(), true(), b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), closed(), down(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(B(), closed(), stop(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(B(), open(), stop(), false(), b2, b3, i)] = [1] i + [1] b2 + [1] b3 + [2] 1177.80/297.27 > [1] i + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(B(), closed(), stop(), false(), b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(S(), d, stop(), b1, b2, true(), i)] = [1] i + [1] d + [1] b1 + [1] b2 + [3] 1177.80/297.27 > [1] i + [1] b1 + [1] b2 + [2] 1177.80/297.27 = [idle(S(), open(), stop(), b1, b2, false(), i)] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), stop(), b1, true(), false(), i)] = [1] i + [1] b1 + [3] 1177.80/297.27 >= [1] i + [1] b1 + [3] 1177.80/297.27 = [idle(S(), closed(), down(), b1, true(), false(), i)] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), stop(), false(), false(), false(), empty())] = [1] 1177.80/297.27 > [0] 1177.80/297.27 = [correct()] 1177.80/297.27 1177.80/297.27 [busy(S(), = [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.27 closed(), 1177.80/297.27 stop(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 newbuttons(i1, i2, i3, i))] 1177.80/297.27 >= [1] i + [1] i1 + [1] i2 + [1] i3 + [3] 1177.80/297.27 = [idle(S(), 1177.80/297.27 closed(), 1177.80/297.27 stop(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 false(), 1177.80/297.27 newbuttons(i1, i2, i3, i))] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), stop(), true(), false(), false(), i)] = [1] i + [3] 1177.80/297.27 >= [1] i + [3] 1177.80/297.27 = [idle(S(), closed(), down(), true(), false(), false(), i)] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), up(), b1, b2, b3, i)] = [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] b3 + [1] 1177.80/297.27 = [idle(S(), closed(), stop(), b1, b2, b3, i)] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), down(), b1, b2, false(), i)] = [1] i + [1] b1 + [1] b2 + [1] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [1] 1177.80/297.27 = [idle(FS(), closed(), down(), b1, b2, false(), i)] 1177.80/297.27 1177.80/297.27 [busy(S(), closed(), down(), b1, b2, true(), i)] = [1] i + [1] b1 + [1] b2 + [3] 1177.80/297.27 >= [1] i + [1] b1 + [1] b2 + [3] 1177.80/297.27 = [idle(S(), closed(), stop(), b1, b2, true(), i)] 1177.80/297.27 1177.80/297.27 [busy(S(), open(), stop(), b1, b2, false(), i)] = [1] i + [1] b1 + [1] b2 + [2] 1177.80/297.27 > [1] i + [1] b1 + [1] b2 + [1] 1177.80/297.27 = [idle(S(), closed(), stop(), b1, b2, false(), i)] 1177.80/297.28 1177.80/297.28 [idle(fl, d, m, b1, b2, b3, empty())] = [1] d + [1] b1 + [1] b2 + [1] b3 + [1] fl + [1] m + [1] 1177.80/297.28 >= [1] d + [1] b1 + [1] b2 + [1] b3 + [1] fl + [1] m + [1] 1177.80/297.28 = [busy(fl, d, m, b1, b2, b3, empty())] 1177.80/297.28 1177.80/297.28 [idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i))] = [1] i + [1] d + [1] b1 + [1] b2 + [1] b3 + [1] fl + [1] i1 + [1] i2 + [1] i3 + [1] m + [3] 1177.80/297.28 > [1] i + [1] d + [1] b1 + [1] b2 + [1] b3 + [1] fl + [1] i1 + [1] i2 + [1] i3 + [1] m + [1] 1177.80/297.28 = [busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)] 1177.80/297.28 1177.80/297.28 [or(false(), b)] = [1] b + [0] 1177.80/297.28 >= [1] b + [0] 1177.80/297.28 = [b] 1177.80/297.28 1177.80/297.28 [or(true(), b)] = [1] b + [2] 1177.80/297.28 >= [2] 1177.80/297.28 = [true()] 1177.80/297.28 1177.80/297.28 1177.80/297.28 We return to the main proof. 1177.80/297.28 1177.80/297.28 We are left with following problem, upon which TcT provides the 1177.80/297.28 certificate YES(?,O(n^1)). 1177.80/297.28 1177.80/297.28 Strict Trs: 1177.80/297.28 { busy(F(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 -> 1177.80/297.28 idle(F(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 , busy(F(), closed(), stop(), false(), false(), true(), i) -> 1177.80/297.28 idle(F(), closed(), up(), false(), false(), true(), i) 1177.80/297.28 , busy(F(), closed(), stop(), true(), false(), b3, i) -> 1177.80/297.28 idle(F(), closed(), down(), true(), false(), b3, i) 1177.80/297.28 , busy(F(), closed(), up(), b1, false(), b3, i) -> 1177.80/297.28 idle(FS(), closed(), up(), b1, false(), b3, i) 1177.80/297.28 , busy(F(), closed(), up(), b1, true(), b3, i) -> 1177.80/297.28 idle(F(), closed(), stop(), b1, true(), b3, i) 1177.80/297.28 , busy(F(), closed(), down(), b1, false(), b3, i) -> 1177.80/297.28 idle(BF(), closed(), down(), b1, false(), b3, i) 1177.80/297.28 , busy(F(), closed(), down(), b1, true(), b3, i) -> 1177.80/297.28 idle(F(), closed(), stop(), b1, true(), b3, i) 1177.80/297.28 , busy(BF(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.28 idle(F(), closed(), up(), b1, b2, b3, i) 1177.80/297.28 , busy(BF(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.28 idle(B(), closed(), down(), b1, b2, b3, i) 1177.80/297.28 , busy(FS(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.28 idle(S(), closed(), up(), b1, b2, b3, i) 1177.80/297.28 , busy(FS(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.28 idle(F(), closed(), down(), b1, b2, b3, i) 1177.80/297.28 , busy(B(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 -> 1177.80/297.28 idle(B(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 , busy(B(), closed(), stop(), false(), false(), true(), i) -> 1177.80/297.28 idle(B(), closed(), up(), false(), false(), true(), i) 1177.80/297.28 , busy(B(), closed(), stop(), false(), true(), b3, i) -> 1177.80/297.28 idle(B(), closed(), up(), false(), true(), b3, i) 1177.80/297.28 , busy(B(), closed(), up(), false(), b2, b3, i) -> 1177.80/297.28 idle(BF(), closed(), up(), false(), b2, b3, i) 1177.80/297.28 , busy(B(), closed(), up(), true(), b2, b3, i) -> 1177.80/297.28 idle(B(), closed(), stop(), true(), b2, b3, i) 1177.80/297.28 , busy(B(), closed(), down(), b1, b2, b3, i) -> 1177.80/297.28 idle(B(), closed(), stop(), b1, b2, b3, i) 1177.80/297.28 , busy(S(), closed(), stop(), b1, true(), false(), i) -> 1177.80/297.28 idle(S(), closed(), down(), b1, true(), false(), i) 1177.80/297.28 , busy(S(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 -> 1177.80/297.28 idle(S(), 1177.80/297.28 closed(), 1177.80/297.28 stop(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 false(), 1177.80/297.28 newbuttons(i1, i2, i3, i)) 1177.80/297.28 , busy(S(), closed(), stop(), true(), false(), false(), i) -> 1177.80/297.28 idle(S(), closed(), down(), true(), false(), false(), i) 1177.80/297.28 , busy(S(), closed(), up(), b1, b2, b3, i) -> 1177.80/297.28 idle(S(), closed(), stop(), b1, b2, b3, i) 1177.80/297.28 , busy(S(), closed(), down(), b1, b2, false(), i) -> 1177.80/297.28 idle(FS(), closed(), down(), b1, b2, false(), i) 1177.80/297.28 , busy(S(), closed(), down(), b1, b2, true(), i) -> 1177.80/297.28 idle(S(), closed(), stop(), b1, b2, true(), i) 1177.80/297.28 , idle(fl, d, m, b1, b2, b3, empty()) -> 1177.80/297.28 busy(fl, d, m, b1, b2, b3, empty()) 1177.80/297.28 , or(false(), b) -> b 1177.80/297.28 , or(true(), b) -> true() } 1177.80/297.28 Obligation: 1177.80/297.28 derivational complexity 1177.80/297.28 Answer: 1177.80/297.28 YES(?,O(n^1)) 1177.80/297.28 1177.80/297.28 The problem is match-bounded by 6. The enriched problem is 1177.80/297.28 compatible with the following automaton. 1177.80/297.28 { busy_0(1, 1, 1, 1, 1, 1, 1) -> 1 1177.80/297.28 , busy_1(1, 1, 1, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 4, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 4, 1, 1, 10, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 4, 1, 10, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 9, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 9, 7, 7, 10, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 11, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 11, 1, 10, 7, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 11, 10, 7, 1, 15) -> 1 1177.80/297.28 , busy_1(2, 3, 11, 10, 7, 7, 15) -> 1 1177.80/297.28 , busy_1(12, 3, 9, 1, 7, 1, 15) -> 1 1177.80/297.28 , busy_1(12, 3, 11, 1, 1, 7, 15) -> 1 1177.80/297.28 , busy_1(13, 3, 9, 7, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(13, 3, 11, 1, 7, 1, 15) -> 1 1177.80/297.28 , busy_1(14, 3, 4, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(14, 3, 4, 10, 1, 1, 15) -> 1 1177.80/297.28 , busy_1(14, 3, 9, 7, 7, 10, 15) -> 1 1177.80/297.28 , busy_1(14, 3, 9, 7, 10, 1, 15) -> 1 1177.80/297.28 , busy_1(14, 3, 11, 1, 1, 1, 15) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 1, 1, 10, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 1, 10, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 1, 10, 7, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 7, 10, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 4, 10, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 9, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 9, 7, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 1, 10, 7, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 7, 10, 7, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 10, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 10, 7, 7, 27) -> 1 1177.80/297.28 , busy_2(2, 3, 11, 10, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(12, 3, 9, 1, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(12, 3, 9, 7, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(12, 3, 11, 1, 1, 7, 27) -> 1 1177.80/297.28 , busy_2(12, 3, 11, 10, 7, 7, 27) -> 1 1177.80/297.28 , busy_2(13, 3, 9, 7, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(13, 3, 11, 1, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(13, 3, 11, 1, 7, 7, 27) -> 1 1177.80/297.28 , busy_2(14, 3, 4, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(14, 3, 4, 10, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(14, 3, 9, 7, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(14, 3, 9, 7, 10, 1, 27) -> 1 1177.80/297.28 , busy_2(14, 3, 11, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(16, 17, 18, 7, 19, 10, 27) -> 1 1177.80/297.28 , busy_2(16, 17, 24, 1, 10, 19, 27) -> 1 1177.80/297.28 , busy_2(16, 17, 24, 10, 7, 19, 27) -> 1 1177.80/297.28 , busy_2(20, 17, 18, 7, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(20, 17, 21, 1, 22, 1, 27) -> 1 1177.80/297.28 , busy_2(20, 17, 21, 1, 22, 7, 27) -> 1 1177.80/297.28 , busy_2(20, 17, 24, 1, 1, 7, 27) -> 1 1177.80/297.28 , busy_2(23, 17, 18, 19, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(23, 17, 18, 19, 10, 1, 27) -> 1 1177.80/297.28 , busy_2(23, 17, 24, 10, 19, 1, 27) -> 1 1177.80/297.28 , busy_2(23, 17, 24, 10, 19, 7, 27) -> 1 1177.80/297.28 , busy_2(25, 17, 21, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(25, 17, 24, 1, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(26, 17, 18, 1, 7, 1, 27) -> 1 1177.80/297.28 , busy_2(26, 17, 21, 1, 1, 1, 27) -> 1 1177.80/297.28 , busy_2(26, 17, 21, 1, 1, 22, 27) -> 1 1177.80/297.28 , busy_2(26, 17, 21, 7, 7, 10, 27) -> 1 1177.80/297.28 , busy_2(26, 17, 21, 10, 7, 22, 27) -> 1 1177.80/297.28 , busy_3(16, 17, 18, 7, 19, 10, 35) -> 1 1177.80/297.28 , busy_3(16, 17, 18, 19, 19, 10, 35) -> 1 1177.80/297.28 , busy_3(16, 17, 24, 1, 10, 19, 35) -> 1 1177.80/297.28 , busy_3(16, 17, 24, 7, 10, 19, 35) -> 1 1177.80/297.28 , busy_3(16, 17, 24, 10, 7, 19, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 18, 7, 1, 1, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 1, 22, 1, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 1, 22, 7, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 1, 22, 19, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 7, 22, 1, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 7, 22, 7, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 7, 22, 19, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 21, 19, 22, 1, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 24, 1, 1, 7, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 24, 10, 7, 7, 35) -> 1 1177.80/297.28 , busy_3(20, 17, 24, 22, 19, 10, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 18, 19, 7, 10, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 18, 19, 10, 1, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 24, 10, 19, 1, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 24, 10, 19, 7, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 24, 10, 19, 10, 35) -> 1 1177.80/297.28 , busy_3(23, 17, 24, 10, 19, 19, 35) -> 1 1177.80/297.28 , busy_3(25, 17, 21, 1, 1, 1, 35) -> 1 1177.80/297.28 , busy_3(25, 17, 24, 1, 7, 1, 35) -> 1 1177.80/297.28 , busy_3(25, 17, 24, 1, 7, 7, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 18, 1, 7, 1, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 18, 7, 7, 1, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 21, 1, 1, 1, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 21, 1, 1, 22, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 21, 7, 7, 10, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 21, 10, 7, 22, 35) -> 1 1177.80/297.28 , busy_3(26, 17, 24, 1, 22, 19, 35) -> 1 1177.80/297.28 , busy_3(28, 29, 30, 19, 7, 10, 35) -> 1 1177.80/297.28 , busy_3(28, 29, 30, 19, 10, 1, 35) -> 1 1177.80/297.28 , busy_3(28, 29, 32, 1, 10, 19, 35) -> 1 1177.80/297.28 , busy_3(28, 29, 32, 10, 7, 19, 35) -> 1 1177.80/297.28 , busy_3(31, 29, 32, 10, 19, 1, 35) -> 1 1177.80/297.28 , busy_3(31, 29, 32, 10, 19, 7, 35) -> 1 1177.80/297.28 , busy_3(31, 29, 34, 1, 7, 1, 35) -> 1 1177.80/297.28 , busy_3(33, 29, 30, 7, 19, 10, 35) -> 1 1177.80/297.28 , busy_3(33, 29, 34, 1, 7, 1, 35) -> 1 1177.80/297.28 , busy_4(28, 29, 30, 19, 7, 10, 42) -> 1 1177.80/297.28 , busy_4(28, 29, 30, 19, 10, 1, 42) -> 1 1177.80/297.28 , busy_4(28, 29, 32, 1, 10, 19, 42) -> 1 1177.80/297.28 , busy_4(28, 29, 32, 7, 10, 19, 42) -> 1 1177.80/297.28 , busy_4(28, 29, 32, 10, 7, 19, 42) -> 1 1177.80/297.28 , busy_4(28, 29, 34, 1, 51, 37, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 32, 10, 19, 1, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 32, 10, 19, 7, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 32, 10, 19, 10, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 32, 10, 19, 19, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 34, 1, 7, 1, 42) -> 1 1177.80/297.28 , busy_4(31, 29, 34, 1, 7, 7, 42) -> 1 1177.80/297.28 , busy_4(33, 29, 30, 7, 19, 10, 42) -> 1 1177.80/297.28 , busy_4(33, 29, 30, 19, 19, 10, 42) -> 1 1177.80/297.28 , busy_4(33, 29, 34, 1, 7, 1, 42) -> 1 1177.80/297.28 , busy_4(33, 29, 34, 7, 7, 1, 42) -> 1 1177.80/297.28 , busy_4(36, 29, 32, 22, 37, 10, 42) -> 1 1177.80/297.28 , busy_4(38, 39, 40, 10, 19, 1, 42) -> 1 1177.80/297.28 , busy_4(38, 39, 40, 10, 19, 7, 42) -> 1 1177.80/297.28 , busy_4(41, 39, 40, 7, 19, 10, 42) -> 1 1177.80/297.28 , busy_4(44, 29, 32, 1, 22, 37, 42) -> 1 1177.80/297.28 , busy_5(38, 39, 40, 10, 19, 1, 45) -> 1 1177.80/297.28 , busy_5(38, 39, 40, 10, 19, 7, 45) -> 1 1177.80/297.28 , busy_5(38, 39, 40, 10, 19, 10, 45) -> 1 1177.80/297.28 , busy_5(38, 39, 40, 10, 19, 19, 45) -> 1 1177.80/297.28 , busy_5(38, 39, 43, 22, 37, 10, 45) -> 1 1177.80/297.28 , busy_5(41, 39, 40, 7, 19, 10, 45) -> 1 1177.80/297.28 , busy_5(41, 39, 40, 19, 19, 10, 45) -> 1 1177.80/297.28 , busy_5(46, 39, 43, 1, 22, 37, 45) -> 1 1177.80/297.28 , busy_6(47, 48, 49, 22, 37, 10, 50) -> 1 1177.80/297.28 , F_0() -> 1 1177.80/297.28 , F_1() -> 2 1177.80/297.28 , F_2() -> 20 1177.80/297.28 , F_3() -> 28 1177.80/297.28 , F_4() -> 46 1177.80/297.28 , closed_0() -> 1 1177.80/297.28 , closed_1() -> 3 1177.80/297.28 , closed_2() -> 17 1177.80/297.28 , closed_3() -> 29 1177.80/297.28 , closed_4() -> 39 1177.80/297.28 , closed_5() -> 48 1177.80/297.28 , stop_0() -> 1 1177.80/297.28 , stop_1() -> 4 1177.80/297.28 , stop_2() -> 21 1177.80/297.28 , stop_3() -> 34 1177.80/297.28 , stop_4() -> 40 1177.80/297.28 , stop_5() -> 49 1177.80/297.28 , false_0() -> 1 1177.80/297.28 , false_1() -> 5 1177.80/297.28 , false_1() -> 6 1177.80/297.28 , false_1() -> 7 1177.80/297.28 , false_2() -> 19 1177.80/297.28 , false_3() -> 37 1177.80/297.28 , BF_0() -> 1 1177.80/297.28 , BF_1() -> 13 1177.80/297.28 , BF_2() -> 23 1177.80/297.28 , BF_3() -> 36 1177.80/297.28 , FS_0() -> 1 1177.80/297.28 , FS_1() -> 12 1177.80/297.28 , FS_2() -> 16 1177.80/297.28 , FS_3() -> 44 1177.80/297.28 , up_0() -> 1 1177.80/297.28 , up_1() -> 9 1177.80/297.28 , up_2() -> 18 1177.80/297.28 , up_3() -> 30 1177.80/297.28 , down_0() -> 1 1177.80/297.28 , down_1() -> 11 1177.80/297.28 , down_2() -> 24 1177.80/297.28 , down_3() -> 32 1177.80/297.28 , down_4() -> 43 1177.80/297.28 , B_0() -> 1 1177.80/297.28 , B_1() -> 14 1177.80/297.28 , B_2() -> 25 1177.80/297.28 , B_3() -> 31 1177.80/297.28 , B_4() -> 38 1177.80/297.28 , B_5() -> 47 1177.80/297.28 , empty_0() -> 1 1177.80/297.28 , empty_1() -> 15 1177.80/297.28 , empty_2() -> 27 1177.80/297.28 , empty_3() -> 35 1177.80/297.28 , empty_4() -> 42 1177.80/297.28 , empty_5() -> 45 1177.80/297.28 , empty_6() -> 50 1177.80/297.28 , S_0() -> 1 1177.80/297.28 , S_1() -> 2 1177.80/297.28 , S_2() -> 26 1177.80/297.28 , S_3() -> 33 1177.80/297.28 , S_4() -> 41 1177.80/297.28 , newbuttons_0(1, 1, 1, 1) -> 1 1177.80/297.28 , newbuttons_1(1, 1, 1, 1) -> 8 1177.80/297.28 , idle_0(1, 1, 1, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 1, 10, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 1, 10, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 10, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 10, 1, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 10, 1, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 10, 7, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 1, 10, 7, 35) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 5, 6, 7, 8) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 7, 10, 1, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 7, 10, 1, 35) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 10, 7, 10, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 4, 10, 7, 10, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 9, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 9, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 9, 7, 7, 10, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 9, 7, 7, 10, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 9, 7, 7, 10, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 10, 7, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 10, 7, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 10, 7, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 1, 10, 7, 35) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 7, 10, 7, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 1, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 1, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 1, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 7, 1) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 7, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 7, 27) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 7, 35) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 7, 42) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 10, 15) -> 1 1177.80/297.28 , idle_1(2, 3, 11, 10, 7, 10, 27) -> 1 1177.80/297.28 , idle_1(12, 3, 9, 1, 7, 1, 1) -> 1 1177.80/297.28 , idle_1(12, 3, 9, 1, 7, 1, 15) -> 1 1177.80/297.28 , idle_1(12, 3, 9, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_1(12, 3, 9, 7, 7, 1, 27) -> 1 1177.80/297.28 , idle_1(12, 3, 9, 7, 7, 1, 35) -> 1 1177.80/297.28 , idle_1(12, 3, 11, 1, 1, 7, 1) -> 1 1177.80/297.28 , idle_1(12, 3, 11, 1, 1, 7, 15) -> 1 1177.80/297.28 , idle_1(12, 3, 11, 1, 1, 7, 27) -> 1 1177.80/297.28 , idle_1(12, 3, 11, 10, 7, 7, 15) -> 1 1177.80/297.28 , idle_1(12, 3, 11, 10, 7, 7, 27) -> 1 1177.80/297.28 , idle_1(13, 3, 9, 7, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(13, 3, 9, 7, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(13, 3, 11, 1, 7, 1, 1) -> 1 1177.80/297.28 , idle_1(13, 3, 11, 1, 7, 1, 15) -> 1 1177.80/297.28 , idle_1(13, 3, 11, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_1(13, 3, 11, 1, 7, 7, 27) -> 1 1177.80/297.28 , idle_1(13, 3, 11, 1, 7, 7, 35) -> 1 1177.80/297.28 , idle_1(14, 3, 4, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(14, 3, 4, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(14, 3, 4, 7, 7, 7, 8) -> 1 1177.80/297.28 , idle_1(14, 3, 4, 10, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(14, 3, 4, 10, 1, 1, 15) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 7, 10, 1) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 7, 10, 15) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 7, 10, 27) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 7, 10, 35) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 7, 10, 42) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 10, 1, 1) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 10, 1, 15) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 10, 1, 27) -> 1 1177.80/297.28 , idle_1(14, 3, 9, 7, 10, 1, 35) -> 1 1177.80/297.28 , idle_1(14, 3, 11, 1, 1, 1, 1) -> 1 1177.80/297.28 , idle_1(14, 3, 11, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_2(16, 17, 18, 7, 19, 10, 15) -> 1 1177.80/297.28 , idle_2(16, 17, 18, 7, 19, 10, 27) -> 1 1177.80/297.28 , idle_2(16, 17, 18, 19, 19, 10, 35) -> 1 1177.80/297.28 , idle_2(16, 17, 18, 19, 19, 10, 42) -> 1 1177.80/297.28 , idle_2(16, 17, 24, 1, 10, 19, 15) -> 1 1177.80/297.28 , idle_2(16, 17, 24, 1, 10, 19, 27) -> 1 1177.80/297.28 , idle_2(16, 17, 24, 7, 10, 19, 27) -> 1 1177.80/297.28 , idle_2(16, 17, 24, 10, 7, 19, 15) -> 1 1177.80/297.28 , idle_2(16, 17, 24, 10, 7, 19, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 18, 7, 1, 1, 15) -> 1 1177.80/297.28 , idle_2(20, 17, 18, 7, 1, 1, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 1, 15) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 1, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 7, 15) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 7, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 7, 35) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 19, 35) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 1, 22, 19, 42) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 7, 22, 1, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 7, 22, 1, 35) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 7, 22, 7, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 7, 22, 19, 42) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 19, 22, 1, 35) -> 1 1177.80/297.28 , idle_2(20, 17, 21, 19, 22, 1, 42) -> 1 1177.80/297.28 , idle_2(20, 17, 24, 1, 1, 7, 15) -> 1 1177.80/297.28 , idle_2(20, 17, 24, 1, 1, 7, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 24, 10, 7, 7, 27) -> 1 1177.80/297.28 , idle_2(20, 17, 24, 22, 19, 10, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 18, 19, 7, 10, 15) -> 1 1177.80/297.28 , idle_2(23, 17, 18, 19, 7, 10, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 18, 19, 10, 1, 15) -> 1 1177.80/297.28 , idle_2(23, 17, 18, 19, 10, 1, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 1, 15) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 1, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 7, 15) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 7, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 7, 35) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 10, 27) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 19, 35) -> 1 1177.80/297.28 , idle_2(23, 17, 24, 10, 19, 19, 42) -> 1 1177.80/297.28 , idle_2(25, 17, 21, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_2(25, 17, 21, 1, 1, 1, 27) -> 1 1177.80/297.28 , idle_2(25, 17, 24, 1, 7, 1, 15) -> 1 1177.80/297.28 , idle_2(25, 17, 24, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_2(25, 17, 24, 1, 7, 7, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 18, 1, 7, 1, 15) -> 1 1177.80/297.28 , idle_2(26, 17, 18, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 18, 7, 7, 1, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 1, 1, 1, 15) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 1, 1, 1, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 1, 1, 22, 15) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 1, 1, 22, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 7, 7, 10, 15) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 7, 7, 10, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 10, 7, 22, 15) -> 1 1177.80/297.28 , idle_2(26, 17, 21, 10, 7, 22, 27) -> 1 1177.80/297.28 , idle_2(26, 17, 24, 1, 22, 19, 27) -> 1 1177.80/297.28 , idle_3(28, 29, 30, 19, 7, 10, 27) -> 1 1177.80/297.28 , idle_3(28, 29, 30, 19, 7, 10, 35) -> 1 1177.80/297.28 , idle_3(28, 29, 30, 19, 10, 1, 27) -> 1 1177.80/297.28 , idle_3(28, 29, 30, 19, 10, 1, 35) -> 1 1177.80/297.28 , idle_3(28, 29, 32, 1, 10, 19, 27) -> 1 1177.80/297.28 , idle_3(28, 29, 32, 1, 10, 19, 35) -> 1 1177.80/297.28 , idle_3(28, 29, 32, 7, 10, 19, 35) -> 1 1177.80/297.28 , idle_3(28, 29, 32, 10, 7, 19, 27) -> 1 1177.80/297.28 , idle_3(28, 29, 32, 10, 7, 19, 35) -> 1 1177.80/297.28 , idle_3(28, 29, 34, 1, 51, 37, 45) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 1, 27) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 1, 35) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 7, 27) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 7, 35) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 10, 35) -> 1 1177.80/297.28 , idle_3(31, 29, 32, 10, 19, 19, 35) -> 1 1177.80/297.28 , idle_3(31, 29, 34, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_3(31, 29, 34, 1, 7, 1, 35) -> 1 1177.80/297.28 , idle_3(31, 29, 34, 1, 7, 7, 35) -> 1 1177.80/297.28 , idle_3(33, 29, 30, 7, 19, 10, 27) -> 1 1177.80/297.28 , idle_3(33, 29, 30, 7, 19, 10, 35) -> 1 1177.80/297.28 , idle_3(33, 29, 30, 19, 19, 10, 35) -> 1 1177.80/297.28 , idle_3(33, 29, 34, 1, 7, 1, 27) -> 1 1177.80/297.28 , idle_3(33, 29, 34, 1, 7, 1, 35) -> 1 1177.80/297.28 , idle_3(33, 29, 34, 7, 7, 1, 35) -> 1 1177.80/297.28 , idle_3(36, 29, 32, 22, 37, 10, 35) -> 1 1177.80/297.28 , idle_3(44, 29, 32, 1, 22, 37, 35) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 1, 35) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 1, 42) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 7, 35) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 7, 42) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 10, 42) -> 1 1177.80/297.28 , idle_4(38, 39, 40, 10, 19, 19, 42) -> 1 1177.80/297.28 , idle_4(38, 39, 43, 22, 37, 10, 42) -> 1 1177.80/297.28 , idle_4(41, 39, 40, 7, 19, 10, 35) -> 1 1177.80/297.28 , idle_4(41, 39, 40, 7, 19, 10, 42) -> 1 1177.80/297.28 , idle_4(41, 39, 40, 19, 19, 10, 42) -> 1 1177.80/297.28 , idle_4(46, 39, 43, 1, 22, 37, 42) -> 1 1177.80/297.28 , idle_5(47, 48, 49, 22, 37, 10, 45) -> 1 1177.80/297.28 , true_0() -> 1 1177.80/297.28 , true_1() -> 1 1177.80/297.28 , true_1() -> 10 1177.80/297.28 , true_2() -> 22 1177.80/297.28 , true_3() -> 51 1177.80/297.28 , or_0(1, 1) -> 1 } 1177.80/297.28 1177.80/297.28 Hurray, we answered YES(O(1),O(n^2)) 1178.53/297.70 EOF