The logic that an inference engine uses is typically represented as IF-THEN rules. The general format of such rules is IF <logical expression> THEN <logical expression>. Prior to the development of expert systems and inference engines, artificial intelligence researchers focused on more powerful theorem prover environments that offered much fuller implementations of first-order logic. For example, general statements that included universal quantification (for all X some statement is true) and existential quantification (there exists some X such that some statement is true). What researchers discovered is that the power of these theorem-proving environments was also their drawback. Back in 1965, it was far too easy to create logical expressions that could take an indeterminate or even infinite time to terminate. For example, it is common in universal quantification to make statements over an infinite set such as the set of all natural numbers. Such statements are perfectly reasonable and even required in mathematical proofs but when included in an automated theorem prover executing on a computer may cause the computer to fall into an infinite loop. Focusing on IF-THEN statements (what logicians call "modus ponens") still gave developers a very powerful general mechanism to represent logic, but one that could be used efficiently with computational resources. What is more there is some psychological research that indicates humans also tend to favor IF-THEN representations when storing complex knowledge.