P is not equal to NP

The problem of computing whether any formula of propositional logic is satisfiable is not in P. Therefore, P is not equal to NP. The proofs are informal about formal proofs in a first-order theory B axiomatizing Turing’s theory of computing. However, the informal proofs can be converted into formal proofs in Hilbert’s proof theory, and proved using a theorem prover.This report is an updated version of a report with the same title published in 2008. (See http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-86762.)