Given a simple undirected graph G with at least 6 distinct vertices such that for every vertices x, y, z in G we have x ~ y or y ~ z or z ~ x (where "x~y" denotes "there is an edge between x,y"):
Let i,j,k,l,m,n be 6 distinct vertices of G.
If ¬i~k:
If ~k~m:
If ¬m~i:
¬i~k ∧ ¬k~m ∧ ¬m~i
¬(i~k ⋁ k~m ⋁ m~i)
i~k ⋁ k~m ⋁ m~i
⊥
m~i
If k~m:
...