Complexity of a satisfiability problem
This is NP-hard.
Here is a reduction from SAT.  Suppose you have a CNF formula $\varphi$ with variables $x_1,\dots,x_n$.  Add variables $x'_1,\dots,x'_n$ and clauses of the form $x_i \to \neg x'_i$ and $x_i \lor x'_i$.  For each clause in $\varphi$, we add a corresponding $\cdots \lor \cdots$ clause: e.g., if $x_i \lor \neg x_j \lor x_k$ is a clause in $\varphi$, then we add the clause $x_i \lor x'_j \lor x_k$.  Once you've added all these clauses, add up the total number of clauses; say you have at most $m$ of the first type of clause and at most $m$ of the second type of clause.  Now add unused variables $x_{n+1},\dots,x_m$.  The result is an instance of your problem with $m$ variables and at most $m$ clauses of each type.  Now $\varphi$ is satisfiable iff this instance is satisfiable.