Problem TCT 09 qbf

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputTCT 09 qbf

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:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputTCT 09 qbf

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 09 qbf

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 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputTCT 09 qbf

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 09 qbf

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 seconds

Tool pair1rc

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 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: none

Certificate: TIMEOUT

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair2rc

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 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: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 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 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3rc

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 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: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool rc

Execution TimeUnknown
Answer
TIMEOUT
InputTCT 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: none

Certificate: TIMEOUT

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool tup3irc

Execution Time60.119022ms
Answer
TIMEOUT
InputTCT 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..