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(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:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path order' as
induced by the precedence

 not > tt, not > ff, or > not, or > tt, or > ff, eq > not, eq > tt,
 eq > ff, eq > or, 0 > not, 0 > tt, 0 > ff, 0 > or, 0 > eq, 0 > ver,
 0 > in, 0 > cons, s > not, s > tt, s > ff, s > or, s > eq, s > ver,
 s > in, s > cons, main > not, main > tt, main > ff, main > or,
 main > eq, main > ver, main > in, main > cons, ver > not, ver > tt,
 ver > ff, ver > or, ver > eq, ver > in, ver > cons, nil > not,
 nil > tt, nil > ff, nil > or, nil > eq, nil > ver, nil > in,
 nil > cons, in > not, in > tt, in > ff, in > or, in > eq,
 in > cons, cons > not, cons > tt, cons > ff, cons > or, Var > not,
 Var > tt, Var > ff, Var > or, Var > eq, Var > ver, Var > in,
 Var > cons, t > not, t > tt, t > ff, t > or, t > eq, t > ver,
 t > in, t > cons, Or > not, Or > tt, Or > ff, Or > or, Or > eq,
 Or > ver, Or > in, Or > cons, Not > not, Not > tt, Not > ff,
 Not > or, Not > eq, Not > ver, Not > in, Not > cons, Exists > not,
 Exists > tt, Exists > ff, Exists > or, Exists > eq, Exists > ver,
 Exists > in, Exists > cons, eq ~ cons, 0 ~ s, 0 ~ main, 0 ~ nil,
 0 ~ Var, 0 ~ t, 0 ~ Or, 0 ~ Not, 0 ~ Exists, s ~ main, s ~ nil,
 s ~ Var, s ~ t, s ~ Or, s ~ Not, s ~ Exists, main ~ nil,
 main ~ Var, main ~ t, main ~ Or, main ~ Not, main ~ Exists,
 nil ~ Var, nil ~ t, nil ~ Or, nil ~ Not, nil ~ Exists, Var ~ t,
 Var ~ Or, Var ~ Not, Var ~ Exists, t ~ Or, t ~ Not, t ~ Exists,
 Or ~ Not, Or ~ Exists, Not ~ Exists .

Hurray, we answered YES(?,PRIMREC)