let conj1 l x =
    if implies1 l x then l else
    x :: List.filter (fun y -> not (Disj.implies x y)) l