% non-tautologies

    p.
    not(p).
    and(p, q).
    not(not(p)).
    implies(or(p, q), and(p, q)).
    and(or(p, q), implies(not(p), q)).
    implies(or(implies(p, q), implies(r, s)), implies(or(p, q), or(r, s))).

%tautologies

    implies(p, p).
    or(not(p), p).
    not(and(p, not(p))).
    implies(p, not(not(p))).
    implies(not(not(p)), p).
    implies(and(p, q), or(p, q)).
    implies(and(p, q), and(q, p)).
    implies(p, implies(not(p), p)).
    implies(implies(p, q), implies(not(q), not(p))).
    implies(implies(not(q), not(p)), implies(p, q)).
    implies(implies(p, implies(q, r)), implies(and(p, q), r)).
    implies(not(and(p, q)), or(not(p), not(q))).
    implies(implies(and(p, q), r), implies(p, implies(q, r))).
    implies(implies(and(p, q), r), implies(q, implies(p, r))).
    or(implies(p, q), implies(q, r)).
    implies(or(p, q), or(p, and(q, not(p)))).
    implies(or(p, and(q, not(p))), or(p, q)).
    implies(not(and(p, q)), or(not(p), not(q))).
    implies(or(not(p), not(q)), not(and(p, q))).
    implies(not(or(p, q)), and(not(p), not(q))).
    implies(and(not(p), not(q)), not(or(p, q))).
    implies(and(p, or(q, r)), or(and(p, q), and(p, r))).
    implies(or(and(p, q), and(p, r)), and(p, or(q, r))).
    implies(and(or(q, r), p), or(and(q, p), and(r, p))).
    implies(or(and(q, p), and(r, p)), and(or(q, r), p)).
    implies(or(p, and(q, r)), and(or(p, q), or(p, r))).
    implies(and(or(p, q), or(p, r)), or(p, and(q, r))).
    implies(or(and(q, r), p), and(or(q, p), or(r, p))).
    implies(and(or(q, p), or(r, p)), or(and(q, r), p)).
    implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))).
    implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))).