TPTP-NUM015-1 {
-l
-N
--SP
--ftl=TTProof.ftl
--tdir=TPTP
--tmpl=%@-P^.html
--id=TPTP-NUM015-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 (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 (or (prime ?X) (divides (divisor ?X) ?X)))

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

Premise:
(forall ?X (or (prime ?X) (less n1 (divisor ?X))))

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

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

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

Premise:
(forall ?X (or (not (less n1 ?X)) (not (less ?X a)) (prime (factorOf ?X))))

Premise Clauses:
{ (not (less n1 ?X));
(not (less ?X a));
(prime (factorOf ?X)) }

Premise:
(forall ?X (or (not (less n1 ?X)) (not (less ?X a)) (divides (factorOf ?X) ?X)))

Premise Clauses:
{ (not (less n1 ?X));
(not (less ?X a));
(divides (factorOf ?X) ?X) }

Premise:
(less n1 a)

Premise Clauses:
{ (less n1 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) (divides ?X a)))

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

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

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

Proof Chain -- 18 steps:

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

Extend:
{ (not (divides ?X-2 ?Y-3));
(not (divides ?Y-3 ?Z-4));
(divides ?X-2 ?Z-4) }
3
[ ?X -> ?X-2, ?Z-4 -> a ]

Clause:
{ (not (prime ?X-2));
[(not (divides ?X-2 a))];
(not (divides ?X-2 ?Y-3));
(not (divides ?Y-3 a)) }

Extend:
{ (prime ?X-r);
(divides (divisor ?X-r) ?X-r) }
2
[ ?Y-3 -> (divisor a), ?X-r -> a ]

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

Extend:
{ (not (prime ?X-28));
(not (divides ?X-28 a)) }
1
[ ?X-28 -> a ]

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

Extend:
{ (divides ?X-3m ?X-3m) }
1
[ ?X-3m -> a ]

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

Extend:
{ (not (less n1 ?X-43));
(not (less ?X-43 a));
(divides (factorOf ?X-43) ?X-43) }
3
[ ?X-2 -> (factorOf (divisor a)), ?X-43 -> (divisor a) ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
(not (less n1 (divisor a)));
(not (less (divisor a) a)) }

Extend:
{ (prime ?X-51);
(less (divisor ?X-51) ?X-51) }
2
[ ?X-51 -> a ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
(not (less n1 (divisor a)));
[(not (less (divisor a) a))];
(prime a) }

Extend:
{ (not (prime ?X-60));
(not (divides ?X-60 a)) }
1
[ ?X-60 -> a ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
(not (less n1 (divisor a)));
[(not (less (divisor a) a))];
[(prime a)];
(not (divides a a)) }

Extend:
{ (divides ?X-9l ?X-9l) }
1
[ ?X-9l -> a ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
(not (less n1 (divisor a))) }

Extend:
{ (prime ?X-ak);
(less n1 (divisor ?X-ak)) }
2
[ ?X-ak -> a ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
[(not (less n1 (divisor a)))];
(prime a) }

Extend:
{ (not (prime ?X-am));
(not (divides ?X-am a)) }
1
[ ?X-am -> a ]

Clause:
{ (not (prime (factorOf (divisor a))));
[(not (divides (factorOf (divisor a)) a))];
[(not (divides (factorOf (divisor a)) (divisor a)))];
[(not (less n1 (divisor a)))];
[(prime a)];
(not (divides a a)) }

Extend:
{ (divides ?X-an ?X-an) }
1
[ ?X-an -> a ]

Clause:
{ (not (prime (factorOf (divisor a)))) }

Extend:
{ (not (less n1 ?X-aw));
(not (less ?X-aw a));
(prime (factorOf ?X-aw)) }
3
[ ?X-aw -> (divisor a) ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
(not (less n1 (divisor a)));
(not (less (divisor a) a)) }

Extend:
{ (prime ?X-b6);
(less (divisor ?X-b6) ?X-b6) }
2
[ ?X-b6 -> a ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
(not (less n1 (divisor a)));
[(not (less (divisor a) a))];
(prime a) }

Extend:
{ (not (prime ?X-b7));
(not (divides ?X-b7 a)) }
1
[ ?X-b7 -> a ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
(not (less n1 (divisor a)));
[(not (less (divisor a) a))];
[(prime a)];
(not (divides a a)) }

Extend:
{ (divides ?X-b8 ?X-b8) }
1
[ ?X-b8 -> a ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
(not (less n1 (divisor a))) }

Extend:
{ (prime ?X-be);
(less n1 (divisor ?X-be)) }
2
[ ?X-be -> a ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
[(not (less n1 (divisor a)))];
(prime a) }

Extend:
{ (not (prime ?X-bg));
(not (divides ?X-bg a)) }
1
[ ?X-bg -> a ]

Clause:
{ [(not (prime (factorOf (divisor a))))];
[(not (less n1 (divisor a)))];
[(prime a)];
(not (divides a a)) }

Extend:
{ (divides ?X-bh ?X-bh) }
1
[ ?X-bh -> a ]

Clause:
{ }

End step 1

Proved
Step Stats: elapsedTime=0.157; cpuTime=0.0; steps=18; roots=1; inputs=9; hornInputs=6; definiteInputs=5; generalInputs=3; factors=0; premiseLiterals=17; rootLiterals=2; generated=118; predicates=3; functions=2; constants=2; skFunctions=0; skConstants=0; expanded=118; derivations=117; factorizations=0; reductions=0; extensions=118; symIDUnif=0; outOrder=0.9915254; maxQueue=128; nResidual=127; nTooDeep=0; nUnacceptable=11; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=18

Proof Stats: proved=1; elapsedTime=0.157; cpuTime=0.0; subproofs=1; successes=1; steps=18; roots=1; inputs=9; hornInputs=6; definiteInputs=5; generalInputs=3; factors=0; premiseLiterals=17; rootLiterals=2; generated=118; predicates=3; functions=2; constants=2; skFunctions=0; skConstants=0; expanded=118; derivations=117; factorizations=0; reductions=0; extensions=118; symIDUnif=0; outOrder=0.9915254; maxQueue=128; nResidual=127; nTooDeep=0; nUnacceptable=11; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=18

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

} TPTP-NUM015-1

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

A_Disproof {
-l
-N
--SP
--ftl=TTProof.ftl
--tdir=TPTP
--tmpl=%@-P^.html
--id=A_Disproof
-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

Prepare Conclusion:
(<=> (forall ?X (=> (F ?X) (forall ?Y (G ?X ?Y)))) (forall ?Y (=> (F ?Y) (G ?Y ?Y))))

Conditional Hypothesis:
(forall ?X (=> (F ?X) (forall ?Y (G ?X ?Y))))

Conditional Hypothesis:
{ (not (F ?X));
(G ?X ?Y) }

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

Conclusion:
(forall ?Y-1 (=> (F ?Y-1) (G ?Y-1 ?Y-1)))

~Conclusion:
(not (forall ?Y-1 (=> (F ?Y-1) (G ?Y-1 ?Y-1))))

Conclusion Clauses:
{ (F skcY-1_1) }
{ (not (G skcY-1_1 skcY-1_1)) }

Root Clause:
{ (F skcY-1_1) }

Root Clause:
{ (not (G skcY-1_1 skcY-1_1)) }

Proof Chain -- 2 steps:

Root:
{ (F skcY-1_1) }

Extend:
{ (not (F ?X-1));
(G ?X-1 ?Y-2) }
1
[ ?X-1 -> skcY-1_1 ]

Clause:
{ [(F skcY-1_1)];
(G skcY-1_1 ?Y-2) }

Extend:
{ (not (G skcY-1_1 skcY-1_1)) }
1
[ ?Y-2 -> skcY-1_1 ]

Clause:
{ }

End step 4

Proved
Step Stats: elapsedTime=0.027; cpuTime=0.0; steps=2; roots=2; inputs=3; hornInputs=3; definiteInputs=2; generalInputs=0; factors=0; premiseLiterals=2; rootLiterals=2; generated=4; predicates=2; functions=0; constants=1; skFunctions=0; skConstants=1; expanded=4; derivations=2; factorizations=0; reductions=0; extensions=3; symIDUnif=0; outOrder=0.5; maxQueue=2; nResidual=1; nTooDeep=0; nUnacceptable=0; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=2

Conditional Hypothesis:
(forall ?Y-1 (=> (F ?Y-1) (G ?Y-1 ?Y-1)))

Conditional Hypothesis:
{ (not (F ?Y-1));
(G ?Y-1 ?Y-1) }

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

Conclusion:
(forall ?X (=> (F ?X) (forall ?Y (G ?X ?Y))))

~Conclusion:
(not (forall ?X (=> (F ?X) (forall ?Y (G ?X ?Y)))))

Conclusion Clauses:
{ (F skcX_2) }
{ (not (G skcX_2 skcY_3)) }

Root Clause:
{ (F skcX_2) }

Root Clause:
{ (not (G skcX_2 skcY_3)) }

End step 5

Disproved
Step Stats: elapsedTime=0.0020; cpuTime=0.0; steps=; roots=2; inputs=3; hornInputs=3; definiteInputs=2; generalInputs=0; factors=0; premiseLiterals=2; rootLiterals=2; generated=3; predicates=4; functions=0; constants=4; skFunctions=0; skConstants=4; expanded=3; derivations=1; factorizations=0; reductions=0; extensions=1; symIDUnif=0; outOrder=0.33333334; maxQueue=2; nResidual=0; nTooDeep=0; nUnacceptable=0; nXUnacceptable=0; nSubsumed=0; nVacuous=0

Proof Stats: proved=; elapsedTime=0.029000001; cpuTime=0.0; subproofs=2; successes=1; steps=2; roots=4; inputs=6; hornInputs=6; definiteInputs=4; generalInputs=0; factors=0; premiseLiterals=4; rootLiterals=4; generated=7; predicates=4; functions=0; constants=4; skFunctions=0; skConstants=4; expanded=7; derivations=3; factorizations=0; reductions=0; extensions=4; symIDUnif=0; outOrder=0.42857143; maxQueue=2; nResidual=1; nTooDeep=0; nUnacceptable=0; nXUnacceptable=0; nSubsumed=0; nVacuous=0

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

} A_Disproof