%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 21:55:58 EDT 2022 % Result : Theorem 0.12s 0.40s % Output : Proof 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jul 5 01:43:08 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.40 % SZS status Theorem % 0.12/0.40 (* PROOF-FOUND *) % 0.12/0.40 (* BEGIN-PROOF *) % 0.12/0.40 % SZS output start Proof % 0.12/0.40 1. (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (-. (All X0, ((-. (gt (n0) X0)) => (drugsu X0)))) ### Axiom % 0.12/0.40 2. (-. (bcapacityex (n0))) (bcapacityex (n0)) ### Axiom % 0.12/0.40 3. (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) ### Axiom % 0.12/0.40 4. (((All X0, ((-. (gt (n0) X0)) => (drugsu X0))) /\ (-. (bcapacityex (n0)))) => (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (bcapacityex (n0))) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) ### DisjTree 1 2 3 % 0.12/0.40 5. (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (-. (bcapacityex (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) ### All 4 % 0.12/0.40 6. (bcapacitysn (n0)) (-. (bcapacitysn (n0))) ### Axiom % 0.12/0.40 7. (qilt27 (n0)) (-. (qilt27 (n0))) ### Axiom % 0.12/0.40 8. (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((gt (n0) X0) => (conditionhyper X0)))) ### Axiom % 0.12/0.40 9. (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0))) ### Axiom % 0.12/0.40 10. (((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ ((bcapacitysn (n0)) /\ ((qilt27 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) => (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (qilt27 (n0)) (bcapacitysn (n0)) (-. (bcapacityex (n0))) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) ### DisjTree 5 6 7 8 9 % 0.12/0.40 11. (All X0, (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (-. (bcapacityex (n0))) (bcapacitysn (n0)) (qilt27 (n0)) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) ### All 10 % 0.12/0.40 12. (bcapacitysn (n0)) (-. (bcapacitysn (n0))) ### Axiom % 0.12/0.40 13. ((-. (bcapacityex (n0))) \/ (-. (bcapacitysn (n0)))) (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (qilt27 (n0)) (bcapacitysn (n0)) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) ### Or 11 12 % 0.12/0.40 14. (All X0, ((-. (bcapacityex X0)) \/ (-. (bcapacitysn X0)))) (All X0, (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, ((-. (gt (n0) X0)) => (drugsu X0))) (bcapacitysn (n0)) (qilt27 (n0)) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) ### All 13 % 0.12/0.40 15. (-. (((All X0, ((-. (gt (n0) X0)) => (drugsu X0))) /\ ((All X0, ((gt (n0) X0) => (conditionhyper X0))) /\ ((bcapacitysn (n0)) /\ (qilt27 (n0))))) => (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) (All X0, ((-. (bcapacityex X0)) \/ (-. (bcapacitysn X0)))) ### ConjTree 14 % 0.12/0.40 % SZS output end Proof % 0.12/0.40 (* END-PROOF *) %------------------------------------------------------------------------------