cnf(an_4,negated_conjecture, ( ~ is_a_theorem(or(not(or(a,a)),a)) )).