a conjunctive normal form that is a tautology Are there any examples of CNF formulas that are tautologies?
Such that every clause contains different variables so phrases like (a or not a) are rejected?
Take any clause in the formula. If all variables in that clause are different, we can always assign $0$ to a non-negated variable and $1$ to a negated variable. This makes that clause $0$. Therefore, it makes the CNF formula $0$. Thus, tautology is not possible unless there is $A \vee \neg A$ in every clause.
This is probably what Kyle Jones stated in his comment.