TPTP-NUM016-1 {
-l
-N
--SP
--ftl=TTProof.ftl
--tdir=TPTP
--tmpl=%@-P^.html
--id=TPTP-NUM016-1
-c
--ML=10000
--MT=0
-k
-v
-Dtau.ProverSR.condImpl=1
-Dtau.ProverSR.splitImpl=0
-Dtau.ProverSR.splitDACond=1
-Dtau.ProverSR.splitEquiv=1
-Dtau.ProverSR.splitAnd=1
-Dtau.ProverSR.minNeg=1
-Dtau.ProverSR.univInst=0
-Dtau.ProverSR.enumExists=0
-Dtau.ProverSR.enumForall=0
-Dtau.ProverSR.mInduction=0
-Dtau.PRMVInd.ctxPremise=0
-Dtau.PRMVInd.rewriteFurther=1
-Dtau.BrandX.keepUnflat=1
-Dtau.BrandX.stUnflat=1
-Dtau.ProverME.chRoots=0
-Dtau.ProverME.idTrans=1
-Dtau.ProverME.iSubsumption=0
-Dtau.ProverME.iASubsumption=1
-Dtau.ProverME.searchOrder=mH
-Dtau.ProverME.depthCutoff=35
-Dtau.ProverME.noFactors=1
-Dtau.ProverME.noCFactors=0
-Dtau.ProverME.UILeading=0
-Dtau.ProverME.nodeHeuristic=(+ (node nLiterals) (node termDepth))
-Dtau.ProverME.pairHeuristic=(+ (pair nLiterals) (pair termDepth))
-Dtau.ProverME.trace=0x803f
rrs.util.ResourceLimiter: CPU timing is unavailable.
Formulas.loadConfiguration: eqSort=L; cEqFormulaRank=3; cNeqFormulaRank=4

Premise:
(forall ?X (not (less ?X ?X)))

Premise Clauses:
{ (not (less ?X ?X)) }

Premise:
(forall ?X (forall ?Y (or (not (less ?X ?Y)) (not (less ?Y ?X)))))

Premise Clauses:
{ (not (less ?X ?Y));
(not (less ?Y ?X)) }

Premise:
(forall ?X (divides ?X ?X))

Premise Clauses:
{ (divides ?X ?X) }

Premise:
(forall ?X (forall ?Y (forall ?Z (=> (and (divides ?X ?Y) (divides ?Y ?Z)) (divides ?X ?Z)))))

Premise Clauses:
{ (not (divides ?X ?Y));
(not (divides ?Y ?Z));
(divides ?X ?Z) }

Premise:
(forall ?X (forall ?Y (or (not (divides ?X ?Y)) (not (less ?Y ?X)))))

Premise Clauses:
{ (not (divides ?X ?Y));
(not (less ?Y ?X)) }

Premise:
(forall ?X (less ?X (factorial_plus_one ?X)))

Premise Clauses:
{ (less ?X (factorial_plus_one ?X)) }

Premise:
(forall ?X (forall ?Y (or (not (divides ?X (factorial_plus_one ?Y))) (less ?Y ?X))))

Premise Clauses:
{ (not (divides ?X (factorial_plus_one ?Y)));
(less ?Y ?X) }

Premise:
(forall ?X (or (prime ?X) (divides (prime_divisor ?X) ?X)))

Premise Clauses:
{ (prime ?X);
(divides (prime_divisor ?X) ?X) }

Premise:
(forall ?X (or (prime ?X) (prime (prime_divisor ?X))))

Premise Clauses:
{ (prime ?X);
(prime (prime_divisor ?X)) }

Premise:
(forall ?X (or (prime ?X) (less (prime_divisor ?X) ?X)))

Premise Clauses:
{ (prime ?X);
(less (prime_divisor ?X) ?X) }

Premise:
(prime a)

Premise Clauses:
{ (prime a) }

Begin step 1
Search Order: Modified best-first
= / Identity: Unused
Depth cutoff: 35
Clause limit: 10000
Clock limit: 0.0

Conclusion:
(exists ?X (and (prime ?X) (less a ?X) (not (less (factorial_plus_one a) ?X))))

~Conclusion:
(not (exists ?X (and (prime ?X) (less a ?X) (not (less (factorial_plus_one a) ?X)))))

Conclusion Clauses:
{ (not (prime ?X));
(not (less a ?X));
(less (factorial_plus_one a) ?X) }

Root Clause:
{ (not (prime ?X));
(not (less a ?X));
(less (factorial_plus_one a) ?X) }

Proof Chain -- 9 steps:

Root:
{ (not (prime ?X));
(not (less a ?X));
(less (factorial_plus_one a) ?X) }

Extend:
{ (not (less ?X-2 ?Y-3));
(not (less ?Y-3 ?X-2)) }
2
[ ?Y-3 -> (factorial_plus_one a), ?X -> ?X-2 ]

Clause:
{ (not (prime ?X-2));
(not (less a ?X-2));
[(less (factorial_plus_one a) ?X-2)];
(not (less ?X-2 (factorial_plus_one a))) }

Reduce: 3; [ ?X-2 -> (factorial_plus_one a) ]

Clause:
{ (not (prime (factorial_plus_one a)));
(not (less a (factorial_plus_one a))) }

Extend:
{ (not (divides ?X-4y (factorial_plus_one ?Y-4z)));
(less ?Y-4z ?X-4y) }
2
[ ?Y-4z -> a, ?X-4y -> (factorial_plus_one a) ]

Clause:
{ (not (prime (factorial_plus_one a)));
[(not (less a (factorial_plus_one a)))];
(not (divides (factorial_plus_one a) (factorial_plus_one a))) }

Extend:
{ (divides ?X-6f ?X-6f) }
1
[ ?X-6f -> (factorial_plus_one a) ]

Clause:
{ (not (prime (factorial_plus_one a))) }

Extend:
{ (prime ?X-71);
(divides (prime_divisor ?X-71) ?X-71) }
1
[ ?X-71 -> (factorial_plus_one a) ]

Clause:
{ [(not (prime (factorial_plus_one a)))];
(divides (prime_divisor (factorial_plus_one a)) (factorial_plus_one a)) }

Extend:
{ (not (divides ?X-77 ?Y-78));
(not (less ?Y-78 ?X-77)) }
1
[ ?X-77 -> (prime_divisor (factorial_plus_one a)), ?Y-78 -> (factorial_plus_one a) ]

Clause:
{ [(not (prime (factorial_plus_one a)))];
[(divides (prime_divisor (factorial_plus_one a)) (factorial_plus_one a))];
(not (less (factorial_plus_one a) (prime_divisor (factorial_plus_one a)))) }

Extend:
{ (not (prime ?X-8c));
(not (less a ?X-8c));
(less (factorial_plus_one a) ?X-8c) }
3
[ ?X-8c -> (prime_divisor (factorial_plus_one a)) ]

Clause:
{ [(not (prime (factorial_plus_one a)))];
[(divides (prime_divisor (factorial_plus_one a)) (factorial_plus_one a))];
[(not (less (factorial_plus_one a) (prime_divisor (factorial_plus_one a))))];
(not (prime (prime_divisor (factorial_plus_one a))));
(not (less a (prime_divisor (factorial_plus_one a)))) }

Extend:
{ (not (divides ?X-r5 (factorial_plus_one ?Y-r6)));
(less ?Y-r6 ?X-r5) }
2
[ ?Y-r6 -> a, ?X-r5 -> (prime_divisor (factorial_plus_one a)) ]

Clause:
{ [(not (prime (factorial_plus_one a)))];
[(divides (prime_divisor (factorial_plus_one a)) (factorial_plus_one a))];
[(not (less (factorial_plus_one a) (prime_divisor (factorial_plus_one a))))];
(not (prime (prime_divisor (factorial_plus_one a)))) }

Extend:
{ (prime ?X-1cx);
(prime (prime_divisor ?X-1cx)) }
2
[ ?X-1cx -> (factorial_plus_one a) ]

Clause:
{ }

End step 1

Proved
Step Stats: elapsedTime=0.375; cpuTime=0.0; steps=9; roots=1; inputs=12; hornInputs=9; definiteInputs=6; generalInputs=3; factors=0; premiseLiterals=19; rootLiterals=3; generated=349; predicates=3; functions=2; constants=1; skFunctions=0; skConstants=0; expanded=348; derivations=348; factorizations=0; reductions=4; extensions=345; symIDUnif=0; outOrder=1.0; maxQueue=472; nResidual=468; nTooDeep=0; nUnacceptable=9; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=9

Proof Stats: proved=1; elapsedTime=0.375; cpuTime=0.0; subproofs=1; successes=1; steps=9; roots=1; inputs=12; hornInputs=9; definiteInputs=6; generalInputs=3; factors=0; premiseLiterals=19; rootLiterals=3; generated=349; predicates=3; functions=2; constants=1; skFunctions=0; skConstants=0; expanded=348; derivations=348; factorizations=0; reductions=4; extensions=345; symIDUnif=0; outOrder=1.0; maxQueue=472; nResidual=468; nTooDeep=0; nUnacceptable=9; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=9

Elapsed: 0m1s; User: 0m1.7s; System: 0m0.1s

} TPTP-NUM016-1