Tool CaT
stdout:
MAYBE
Problem:
leq(0(),x) -> tt()
leq(s(x),0()) -> ff()
leq(s(x),s(y)) -> leq(x,y)
split(nil()) -> app(nil(),nil())
split(cons(x,nil())) -> app(cons(x,nil()),nil())
split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
merge([](),xs) -> xs
merge(xs,[]()) -> xs
merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
mergesort(xs) -> mergesort1(split(xs))
mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair3rc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool rc
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
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) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ leq^#(0(), x) -> c_1()
, leq^#(s(x), 0()) -> c_2()
, leq^#(s(x), s(y)) -> c_3(leq^#(x, y))
, split^#(nil()) -> c_4()
, split^#(cons(x, nil())) -> c_5(x)
, split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)))
, split1^#(x, y, app(xs, ys)) -> c_7(x, xs, y, ys)
, merge^#([](), xs) -> c_8(xs)
, merge^#(xs, []()) -> c_9(xs)
, merge^#(cons(x, xs), cons(y, ys)) ->
c_10(ifmerge^#(leq(x, y), x, y, xs, ys))
, ifmerge^#(tt(), x, y, xs, ys) ->
c_11(x, merge^#(xs, cons(y, ys)))
, ifmerge^#(ff(), x, y, xs, ys) ->
c_12(y, merge^#(cons(x, xs), ys))
, mergesort^#(xs) -> c_13(mergesort1^#(split(xs)))
, mergesort1^#(app(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)))}
We consider the following Problem:
Strict DPs:
{ leq^#(0(), x) -> c_1()
, leq^#(s(x), 0()) -> c_2()
, leq^#(s(x), s(y)) -> c_3(leq^#(x, y))
, split^#(nil()) -> c_4()
, split^#(cons(x, nil())) -> c_5(x)
, split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)))
, split1^#(x, y, app(xs, ys)) -> c_7(x, xs, y, ys)
, merge^#([](), xs) -> c_8(xs)
, merge^#(xs, []()) -> c_9(xs)
, merge^#(cons(x, xs), cons(y, ys)) ->
c_10(ifmerge^#(leq(x, y), x, y, xs, ys))
, ifmerge^#(tt(), x, y, xs, ys) ->
c_11(x, merge^#(xs, cons(y, ys)))
, ifmerge^#(ff(), x, y, xs, ys) ->
c_12(y, merge^#(cons(x, xs), ys))
, mergesort^#(xs) -> c_13(mergesort1^#(split(xs)))
, mergesort1^#(app(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)))}
Strict Trs:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'usablerules':
-----------------------------
All rules are usable.
No subproblems were generated.
Arrrr..Tool tup3irc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ leq(0(), x) -> tt()
, leq(s(x), 0()) -> ff()
, leq(s(x), s(y)) -> leq(x, y)
, split(nil()) -> app(nil(), nil())
, split(cons(x, nil())) -> app(cons(x, nil()), nil())
, split(cons(x, cons(y, xs))) -> split1(x, y, split(xs))
, split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys))
, merge([](), xs) -> xs
, merge(xs, []()) -> xs
, merge(cons(x, xs), cons(y, ys)) ->
ifmerge(leq(x, y), x, y, xs, ys)
, ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys)))
, ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys))
, mergesort(xs) -> mergesort1(split(xs))
, mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..