TPTP-NUM016-1
Premises:
(forall ?X (not (less ?X ?X))) (forall (?X ?Y) (or (not (less ?X ?Y)) (not (less ?Y ?X)))) (forall ?X (divides ?X ?X)) (forall (?X ?Y ?Z) (=> (and (divides ?X ?Y) (divides ?Y ?Z)) (divides ?X ?Z))) (forall (?X ?Y) (or (not (divides ?X ?Y)) (not (less ?Y ?X)))) (forall ?X (less ?X (factorial_plus_one ?X))) (forall (?X ?Y) (or (not (divides ?X (factorial_plus_one ?Y))) (less ?Y ?X))) (forall ?X (or (prime ?X) (divides (prime_divisor ?X) ?X))) (forall ?X (or (prime ?X) (prime (prime_divisor ?X)))) (forall ?X (or (prime ?X) (less (prime_divisor ?X) ?X))) (prime a)
Conclusion:
(exists ?X (and (prime ?X) (less a ?X) (not (less (factorial_plus_one a) ?X))))