MAYBE 891.05/297.10 MAYBE 891.05/297.10 891.05/297.10 We are left with following problem, upon which TcT provides the 891.05/297.10 certificate MAYBE. 891.05/297.10 891.05/297.10 Strict Trs: 891.05/297.10 { breadth(@breadth@1, @breadth@2) -> 891.05/297.10 breadth#1(dequeue(@breadth@1, @breadth@2)) 891.05/297.10 , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue') 891.05/297.10 , dequeue(@dequeue@1, @dequeue@2) -> 891.05/297.10 dequeue#1(tuple#2(@dequeue@1, @dequeue@2)) 891.05/297.10 , breadth#2(::(@z, @_@9), @queue') -> 891.05/297.10 breadth#3(breadth#4(@z), @queue') 891.05/297.10 , breadth#2(nil(), @queue') -> nil() 891.05/297.10 , breadth#3(tuple#2(@x, @ys), @queue') -> 891.05/297.10 ::(@x, breadth#5(enqueues(@ys, @queue'))) 891.05/297.10 , breadth#4(tuple#4(@children@3, 891.05/297.10 @children@4, 891.05/297.10 @children@5, 891.05/297.10 @children@6)) 891.05/297.10 -> children(@children@3, @children@4, @children@5, @children@6) 891.05/297.10 , breadth#5(tuple#2(@breadth@7, @breadth@8)) -> 891.05/297.10 breadth(@breadth@7, @breadth@8) 891.05/297.10 , enqueues(@l, @queue) -> enqueues#1(@l, @queue) 891.05/297.10 , children(@a, @b, @l1, @l2) -> 891.05/297.10 tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2)) 891.05/297.10 , children#1(::(@x, @xs), @b, @l2) -> children#3(@l2, @b, @x, @xs) 891.05/297.10 , children#1(nil(), @b, @l2) -> children#2(@l2, @b) 891.05/297.10 , children#3(::(@y, @ys), @b, @x, @xs) -> 891.05/297.10 ::(tuple#4(@x, @b, nil(), @xs), 891.05/297.10 ::(tuple#4(@x, @y, @xs, @ys), nil())) 891.05/297.10 , children#3(nil(), @b, @x, @xs) -> nil() 891.05/297.10 , children#2(::(@y, @ys), @b) -> 891.05/297.10 ::(tuple#4(@y, @b, nil(), @ys), nil()) 891.05/297.10 , children#2(nil(), @b) -> nil() 891.05/297.10 , copyover(@copyover@1, @copyover@2) -> 891.05/297.10 copyover#1(tuple#2(@copyover@1, @copyover@2)) 891.05/297.10 , copyover#1(tuple#2(@inq, @outq)) -> copyover#2(@inq, @outq) 891.05/297.10 , copyover#2(::(@x, @xs), @outq) -> copyover(@xs, ::(@x, @outq)) 891.05/297.10 , copyover#2(nil(), @outq) -> tuple#2(nil(), @outq) 891.05/297.10 , dequeue#1(tuple#2(@inq, @outq)) -> dequeue#2(@outq, @inq) 891.05/297.10 , dequeue#2(::(@y, @ys), @inq) -> 891.05/297.10 tuple#2(tuple#2(@inq, @ys), ::(@y, nil())) 891.05/297.10 , dequeue#2(nil(), @inq) -> dequeue#3(@inq) 891.05/297.10 , dequeue#3(::(@x, @xs)) -> dequeue#4(copyover(::(@x, @xs), nil())) 891.05/297.10 , dequeue#3(nil()) -> tuple#2(tuple#2(nil(), nil()), nil()) 891.05/297.10 , dequeue#4(tuple#2(@dequeue@3, @dequeue@4)) -> 891.05/297.10 dequeue(@dequeue@3, @dequeue@4) 891.05/297.10 , empty(@x) -> tuple#2(nil(), nil()) 891.05/297.10 , enqueue(@x, @queue) -> enqueue#1(@queue, @x) 891.05/297.10 , enqueue#1(tuple#2(@inq, @outq), @x) -> 891.05/297.10 tuple#2(::(@x, @inq), @outq) 891.05/297.10 , enqueues#1(::(@x, @xs), @queue) -> 891.05/297.10 enqueues(@xs, enqueue(@x, @queue)) 891.05/297.10 , enqueues#1(nil(), @queue) -> @queue 891.05/297.10 , startBreadth(@xs) -> startBreadth#1(@xs) 891.05/297.10 , startBreadth#1(::(@x, @xs)) -> 891.05/297.10 startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit()))) 891.05/297.10 , startBreadth#1(nil()) -> nil() 891.05/297.10 , startBreadth#2(tuple#2(@breadth@1, @breadth@2)) -> 891.05/297.10 breadth(@breadth@1, @breadth@2) } 891.05/297.10 Obligation: 891.05/297.10 innermost runtime complexity 891.05/297.10 Answer: 891.05/297.10 MAYBE 891.05/297.10 891.05/297.10 None of the processors succeeded. 891.05/297.10 891.05/297.10 Details of failed attempt(s): 891.05/297.10 ----------------------------- 891.05/297.10 1) 'empty' failed due to the following reason: 891.05/297.10 891.05/297.10 Empty strict component of the problem is NOT empty. 891.05/297.10 891.05/297.10 2) 'Best' failed due to the following reason: 891.05/297.10 891.05/297.10 None of the processors succeeded. 891.05/297.10 891.05/297.10 Details of failed attempt(s): 891.05/297.10 ----------------------------- 891.05/297.10 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 891.05/297.10 following reason: 891.05/297.10 891.05/297.10 Computation stopped due to timeout after 297.0 seconds. 891.05/297.10 891.05/297.10 2) 'Best' failed due to the following reason: 891.05/297.10 891.05/297.10 None of the processors succeeded. 891.05/297.10 891.05/297.10 Details of failed attempt(s): 891.05/297.10 ----------------------------- 891.05/297.10 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 891.05/297.10 seconds)' failed due to the following reason: 891.05/297.10 891.05/297.10 Computation stopped due to timeout after 148.0 seconds. 891.05/297.10 891.05/297.10 2) 'Best' failed due to the following reason: 891.05/297.10 891.05/297.10 None of the processors succeeded. 891.05/297.10 891.05/297.10 Details of failed attempt(s): 891.05/297.10 ----------------------------- 891.05/297.10 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 891.05/297.10 following reason: 891.05/297.10 891.05/297.10 The input cannot be shown compatible 891.05/297.10 891.05/297.10 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 891.05/297.10 to the following reason: 891.05/297.10 891.05/297.10 The input cannot be shown compatible 891.05/297.10 891.05/297.10 891.05/297.10 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 891.05/297.10 failed due to the following reason: 891.05/297.10 891.05/297.10 None of the processors succeeded. 891.05/297.10 891.05/297.10 Details of failed attempt(s): 891.05/297.10 ----------------------------- 891.05/297.10 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 891.05/297.10 failed due to the following reason: 891.05/297.10 891.05/297.10 match-boundness of the problem could not be verified. 891.05/297.10 891.05/297.10 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 891.05/297.10 failed due to the following reason: 891.05/297.10 891.05/297.10 match-boundness of the problem could not be verified. 891.05/297.10 891.05/297.10 891.05/297.10 891.05/297.10 891.05/297.10 891.05/297.10 Arrrr.. 891.19/297.28 EOF