LMPO
| Execution Time (secs) | 0.074 |
| Answer | MAYBE |
| Input | TCT 09 qbf |
MAYBE
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
| Execution Time (secs) | 0.268 |
| Answer | YES(?,PRIMREC) |
| Input | TCT 09 qbf |
YES(?,PRIMREC)
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
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
tt > ff, main > ver, main > nil, ver > or, in > or, in > eq,
Var > in, Var > t, Or > or, Or > ver, Or > t, Not > not, Not > ver,
Not > t, Exists > ver, Exists > cons, Exists > t, not ~ tt, tt ~ 0,
ff ~ s, ff ~ nil .
Hurray, we answered YES(?,PRIMREC)
POP*
| Execution Time (secs) | 0.162 |
| Answer | MAYBE |
| Input | TCT 09 qbf |
MAYBE
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
| Execution Time (secs) | 0.100 |
| Answer | MAYBE |
| Input | TCT 09 qbf |
MAYBE
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
| Execution Time (secs) | 0.085 |
| Answer | MAYBE |
| Input | TCT 09 qbf |
MAYBE
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
| Execution Time (secs) | 0.177 |
| Answer | MAYBE |
| Input | TCT 09 qbf |
MAYBE
We consider the following Problem:
Strict Trs:
{ not(tt()) -> ff()
, not(ff()) -> tt()
, or(tt(), x) -> tt()
, or(ff(), x) -> x
, eq(0(), 0()) -> tt()
, eq(s(x), 0()) -> ff()
, eq(0(), s(y)) -> ff()
, eq(s(x), s(y)) -> eq(x, y)
, main(phi) -> ver(phi, nil())
, in(x, nil()) -> ff()
, in(x, cons(a, l)) -> or(eq(x, a), in(x, l))
, ver(Var(x), t()) -> in(x, t())
, ver(Or(phi, psi), t()) -> or(ver(phi, t()), ver(psi, t()))
, ver(Not(phi), t()) -> not(ver(phi, t()))
, ver(Exists(n, phi), t()) ->
or(ver(phi, cons(n, t())), ver(phi, t()))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..