I fixed my own attempt :-)

If ∃ x,y,z,w,t∈V ( x ≠ y ∧ y ≠ z ∧ z ≠ w ∧ w ≠ t ∧ x ≠ z ∧ x ≠ w ∧ x ≠ t ∧ y ≠ w ∧ y ≠ t ∧ z ≠ t) ∧ ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ):
	∃ x,y,z,w,t∈V ( x ≠ y ∧ y ≠ z ∧ z ≠ w ∧ w ≠ t ∧ x ≠ z ∧ x ≠ w ∧ x ≠ t ∧ y ≠ w ∧ y ≠ t ∧ z ≠ t )
	∀ x,y∈V ( c(x,y) ⇒ c(y,x) )
	∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )
	Let a ≠ b ∧ b ≠ c' ∧ c' ≠ d ∧ d ≠ e ∧ a ≠ c' ∧ a ≠ d ∧ a ≠ e ∧ b ≠ d ∧ b ≠ e ∧ c' ≠ e
	c(a, b) ⋁ c(b, c') ⋁ c(c', a)
	c(b, c') ⋁ c(c', a) ⋁ c(a, b)
	c(c', a) ⋁ c(a, b) ⋁ c(b, c')

@F.Zer: So that's why you asked about using the symbol "c". Well haha you could have used i,j,k,l,m... hahaha...

Before you attempt to find a formal proof, you need to find an intuitive argument based on the graph interpretation.

You can very well write that intuitive argument in Fitch-style as well, to facilitate your later translation into a formal proof.

For example it might look like this:

Given a simple undirected graph G with at least 5 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 be 5 distinct vertices of G.
  If i~j:
    ...
  If ¬i~j:
    ...

Your splitting of cases according to the structure of the given conditions is actually doomed to fail. Not that you cannot get a proof with that outline, but that outline will never contribute to any proof. That is why I said you should first use the graph interpretation to intuitively solve the problem, before translating back to FOL.

@user21820 Hahaha. That's funny.

@user21820 Thank you ! Will work on the intuitive argument.