I have given the following SAT variation:

Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated. Example:

$ F= (x_1\vee x_2 \vee x_4) \wedge (\neg x_2\vee \neg x_3 \vee \neg x_4) \wedge (x_3\vee x_4 \vee x_5)$

Is this variation of SAT tractable?

My findings so far:

I suspect the problem is NP-complete and therefore not tractable. Thus I would like to perform a poly-reduction from 3-SAT to the variation described above.

An arbitrary 3-SAT formula can be converted to monotone 3-SAT.

Take following example:

$ C_1=(x_1\vee x_2 \vee \neg x_3)$ and define $ z_3$ by $ \neg x_3 \leftrightarrow z_3$ and $ x_3 \leftrightarrow \neg z_3$ which is equivalent to $ (x_3\vee z_3)\wedge(\neg x_3 \vee \neg z_3)$ .

From that we get the monotone form of $ C_1$ by

$ (x_1\vee x_2 \vee \neg x_3) \leftrightarrow (x_1\vee x_2 \vee z_3)\wedge (x_3\vee z_3)\wedge(\neg x_3 \vee \neg z_3)$

By applying this transformation to all clauses I get a monotone 3-SAT formula which is equally satisfiable.

My reduction produces additional 2 clauses with 2 literals for each non-monotone clause, but how do I get only monotone clauses with exactly 3 distinct literals?