LMPO
Execution Time (secs) | 0.080 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
Execution Time (secs) | 0.084 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
Execution Time (secs) | 0.095 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
Execution Time (secs) | 0.074 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
Execution Time (secs) | 0.079 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
Execution Time (secs) | 0.090 |
Answer | MAYBE |
Input | Der95 32 |
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..