YES(?,PRIMREC)

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

Strict Trs:
  { not(x) -> xor(x, true())
  , implies(x, y) -> xor(and(x, y), xor(x, true()))
  , or(x, y) -> xor(and(x, y), xor(x, y))
  , =(x, y) -> xor(x, xor(y, true())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 not > xor, not > and, true > xor, true > and, implies > xor,
 implies > and, or > xor, or > and, = > xor, = > and, not ~ true,
 not ~ implies, not ~ or, not ~ =, xor ~ and, true ~ implies,
 true ~ or, true ~ =, implies ~ or, implies ~ =, or ~ = .

Hurray, we answered YES(?,PRIMREC)