Problem TCT 09 qbf

TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

Strict Trs:
  { not(tt()) -> ff()
  , not(ff()) -> tt()
  , or(tt(), x) -> tt()
  , or(ff(), x) -> x
  , eq(0(), 0()) -> tt()
  , eq(0(), s(y)) -> ff()
  , eq(s(x), 0()) -> ff()
  , eq(s(x), s(y)) -> eq(x, y)
  , main(phi) -> ver(phi, nil())
  , 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()))
  , in(x, nil()) -> ff()
  , in(x, cons(a, l)) -> or(eq(x, a), in(x, l)) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

YES(?,PRIMREC)

We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).

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())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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)

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..