This paper proves from scratch that the class of problems P is different from the class of problems NP. We define a sequence of sublanguages of the language SAT, which we will call languages of type A, consisting of logical formulas whose length is conditioned by the number and shape of the intersections of their clauses. As shown in the final sections, there exist formulas of that language of type A for which determining whether they are satisfiable is equivalent to determining whether the result of an arithmetic sum of a non-polynomial number of summands is greater than or equal to a natural number associated with each formula. It is shown that in order to obtain each of these summands at least one Turing machine step is required, which implies that this language of type A cannot be accepted by any deterministic Turing machine whose number of steps is bounded by a fixed polynomial as a function of the length of the input. It follows that this language of type A is not a language P but it is still a language NP, which leads to the conclusion that P is different from NP.