MAYBE
759.45/297.10 MAYBE
759.45/297.10
759.45/297.10 We are left with following problem, upon which TcT provides the
759.45/297.10 certificate MAYBE.
759.45/297.10
759.45/297.10 Strict Trs:
759.45/297.10 { merge#1(nil(), @l2) -> @l2
759.45/297.10 , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
759.45/297.10 , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
759.45/297.10 tuple#2(::(@x1, @l1), ::(@x2, @l2))
759.45/297.10 , mergesort#1(nil()) -> nil()
759.45/297.10 , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
759.45/297.10 , mergesort#2(nil(), @x1) -> ::(@x1, nil())
759.45/297.10 , mergesort#2(::(@x2, @xs'), @x1) ->
759.45/297.10 mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
759.45/297.10 , mergesort#3(tuple#2(@l1, @l2)) ->
759.45/297.10 merge(mergesort(@l1), mergesort(@l2))
759.45/297.10 , merge#3(#true(), @x, @xs, @y, @ys) ->
759.45/297.10 ::(@x, merge(@xs, ::(@y, @ys)))
759.45/297.10 , merge#3(#false(), @x, @xs, @y, @ys) ->
759.45/297.10 ::(@y, merge(::(@x, @xs), @ys))
759.45/297.10 , merge(@l1, @l2) -> merge#1(@l1, @l2)
759.45/297.10 , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
759.45/297.10 , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
759.45/297.10 , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
759.45/297.10 , merge#2(::(@y, @ys), @x, @xs) ->
759.45/297.10 merge#3(#less(@x, @y), @x, @xs, @y, @ys)
759.45/297.10 , msplit(@l) -> msplit#1(@l)
759.45/297.10 , msplit#1(nil()) -> tuple#2(nil(), nil())
759.45/297.10 , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
759.45/297.10 , mergesort(@l) -> mergesort#1(@l)
759.45/297.10 , #less(@x, @y) -> #cklt(#compare(@x, @y)) }
759.45/297.10 Weak Trs:
759.45/297.10 { #cklt(#EQ()) -> #false()
759.45/297.10 , #cklt(#LT()) -> #true()
759.45/297.10 , #cklt(#GT()) -> #false()
759.45/297.10 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
759.45/297.10 , #compare(#pos(@x), #0()) -> #GT()
759.45/297.10 , #compare(#pos(@x), #neg(@y)) -> #GT()
759.45/297.10 , #compare(#0(), #pos(@y)) -> #LT()
759.45/297.10 , #compare(#0(), #0()) -> #EQ()
759.45/297.10 , #compare(#0(), #neg(@y)) -> #GT()
759.45/297.10 , #compare(#0(), #s(@y)) -> #LT()
759.45/297.10 , #compare(#neg(@x), #pos(@y)) -> #LT()
759.45/297.10 , #compare(#neg(@x), #0()) -> #LT()
759.45/297.10 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
759.45/297.10 , #compare(#s(@x), #0()) -> #GT()
759.45/297.10 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
759.45/297.10 Obligation:
759.45/297.10 innermost runtime complexity
759.45/297.10 Answer:
759.45/297.10 MAYBE
759.45/297.10
759.45/297.10 None of the processors succeeded.
759.45/297.10
759.45/297.10 Details of failed attempt(s):
759.45/297.10 -----------------------------
759.45/297.10 1) 'empty' failed due to the following reason:
759.45/297.10
759.45/297.10 Empty strict component of the problem is NOT empty.
759.45/297.10
759.45/297.10 2) 'Best' failed due to the following reason:
759.45/297.10
759.45/297.10 None of the processors succeeded.
759.45/297.10
759.45/297.10 Details of failed attempt(s):
759.45/297.10 -----------------------------
759.45/297.10 1) 'With Problem ... (timeout of 297 seconds)' failed due to the
759.45/297.10 following reason:
759.45/297.10
759.45/297.10 Computation stopped due to timeout after 297.0 seconds.
759.45/297.10
759.45/297.10 2) 'Best' failed due to the following reason:
759.45/297.10
759.45/297.10 None of the processors succeeded.
759.45/297.10
759.45/297.10 Details of failed attempt(s):
759.45/297.10 -----------------------------
759.45/297.10 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
759.45/297.10 seconds)' failed due to the following reason:
759.45/297.10
759.45/297.10 Computation stopped due to timeout after 148.0 seconds.
759.45/297.10
759.45/297.10 2) 'Best' failed due to the following reason:
759.45/297.10
759.45/297.10 None of the processors succeeded.
759.45/297.10
759.45/297.10 Details of failed attempt(s):
759.45/297.10 -----------------------------
759.45/297.10 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
759.45/297.10 to the following reason:
759.45/297.10
759.45/297.10 The input cannot be shown compatible
759.45/297.10
759.45/297.10 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
759.45/297.10 following reason:
759.45/297.10
759.45/297.10 The input cannot be shown compatible
759.45/297.10
759.45/297.10
759.45/297.10 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
759.45/297.10 failed due to the following reason:
759.45/297.10
759.45/297.10 None of the processors succeeded.
759.45/297.10
759.45/297.10 Details of failed attempt(s):
759.45/297.10 -----------------------------
759.45/297.10 1) 'Bounds with minimal-enrichment and initial automaton 'match''
759.45/297.10 failed due to the following reason:
759.45/297.10
759.45/297.10 match-boundness of the problem could not be verified.
759.45/297.10
759.45/297.10 2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
759.45/297.10 failed due to the following reason:
759.45/297.10
759.45/297.10 match-boundness of the problem could not be verified.
759.45/297.10
759.45/297.10
759.45/297.10
759.45/297.10
759.45/297.10
759.45/297.10 Arrrr..
759.45/297.13 EOF