cnf(antecedent,negated_conjecture, ( ordered(x,implies(y,z)) | ordered(y,implies(x,z)) )). cnf(prove_wajsberg_theorem,negated_conjecture, ( ~ ordered(x,implies(y,z)) | ~ ordered(y,implies(x,z)) )).