LMPO
| Execution Time (secs) | 0.052 |
| Answer | MAYBE |
| Input | SK90 2.12 |
MAYBE
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
| Execution Time (secs) | 0.084 |
| Answer | YES(?,PRIMREC) |
| Input | SK90 2.12 |
YES(?,PRIMREC)
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,PRIMREC)
Proof:
The input was oriented with the instance of
'multiset path orders' as induced by the precedence
+ > s, + > p, minus > s, minus > p, * > +, * > minus .
Hurray, we answered YES(?,PRIMREC)
POP*
| Execution Time (secs) | 0.051 |
| Answer | MAYBE |
| Input | SK90 2.12 |
MAYBE
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
| Execution Time (secs) | 0.107 |
| Answer | MAYBE |
| Input | SK90 2.12 |
MAYBE
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
| Execution Time (secs) | 0.059 |
| Answer | MAYBE |
| Input | SK90 2.12 |
MAYBE
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
| Execution Time (secs) | 0.071 |
| Answer | MAYBE |
| Input | SK90 2.12 |
MAYBE
We consider the following Problem:
Strict Trs:
{ +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(p(x), y) -> p(+(x, y))
, minus(0()) -> 0()
, minus(s(x)) -> p(minus(x))
, minus(p(x)) -> s(minus(x))
, *(0(), y) -> 0()
, *(s(x), y) -> +(*(x, y), y)
, *(p(x), y) -> +(*(x, y), minus(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..