Tool CaT
stdout:
MAYBE
Problem:
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()))
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:
{ 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()))}
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:
{ 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()))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
stdout:
TIMEOUT
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: none
Certificate: TIMEOUT
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair2rc
stdout:
TIMEOUT
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: none
Certificate: TIMEOUT
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3irc
stdout:
TIMEOUT
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: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3rc
stdout:
TIMEOUT
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: none
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool rc
stdout:
TIMEOUT
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: none
Certificate: TIMEOUT
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool tup3irc
Execution Time | 60.119022ms |
---|
Answer | TIMEOUT |
---|
Input | TCT 09 qbf |
---|
stdout:
TIMEOUT
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: TIMEOUT
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..