a(n) is the number of tautologies and contradictions that are n symbols long in propositional calculus with the connectives not (~), and (*), or (+), implies (>) and if and only if (<>).
When measuring the length of a formula all brackets must be included. The connectives > and <> are counted as one symbol each (but writing them as such requires nonASCII characters).
Formally, the language used for this sequence contains the symbols az and AZ (the variables), ~, *, +, >, <>, ( and ).
The formulas are defined by the following rules:
 every variable is a formula;
 if A is a formula, then ~A is a formula;
 if A and B are formulas, then (A*B), (A+B), (A>B) and (A<>B) are all formulas.
A formula is a tautology if it is true for any assignment of truth values to the variables.
A formula is a contradiction if it is false for any assignment of truth values to the variables.
This sequence is increasing, as adding a ~ to the start of a tautology or contradiction gives a contradiction or tautology one symbol longer.
