%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : MED002+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 : n008.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.18s 0.40s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : MED002+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.33 % Computer : n008.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Tue Jul 5 01:39:53 EDT 2022 % 0.11/0.33 % CPUTime : % 0.18/0.40 % SZS status Theorem % 0.18/0.40 (* PROOF-FOUND *) % 0.18/0.40 (* BEGIN-PROOF *) % 0.18/0.40 % SZS output start Proof % 0.18/0.40 1. (-. (gt (n0) T_0)) (gt (n0) T_0) ### Axiom % 0.18/0.40 2. (-. (-. (gt (n0) T_0))) (-. (gt (n0) T_0)) ### NotNot 1 % 0.18/0.40 3. (-. (drugbg T_0)) (drugbg T_0) ### Axiom % 0.18/0.40 4. ((drugbg T_0) /\ (drugsu T_0)) (-. (drugbg T_0)) ### And 3 % 0.18/0.40 5. ((-. (gt (n0) T_0)) => ((drugbg T_0) /\ (drugsu T_0))) (-. (drugbg T_0)) (-. (gt (n0) T_0)) ### Imply 2 4 % 0.18/0.40 6. (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (-. (gt (n0) T_0)) (-. (drugbg T_0)) ### All 5 % 0.18/0.40 7. (-. ((-. (gt (n0) T_0)) => (drugbg T_0))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### NotImply 6 % 0.18/0.40 8. (-. (All X1, ((-. (gt (n0) X1)) => (drugbg X1)))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### NotAllEx 7 % 0.18/0.40 9. (-. (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) ### Axiom % 0.18/0.40 10. ((All X1, ((-. (gt (n0) X1)) => (drugbg X1))) => (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1))))) (-. (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### Imply 8 9 % 0.18/0.40 11. (All X0, ((All X1, ((-. (gt X0 X1)) => (drugbg X1))) => (All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (-. (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1))))) ### All 10 % 0.18/0.40 12. (-. ((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (drugbg X1))) => (All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))))) ### NotOr 11 % 0.18/0.40 13. (bcapacityne (n0)) (-. (bcapacityne (n0))) ### Axiom % 0.18/0.40 14. (-. (gt (n0) T_1)) (gt (n0) T_1) ### Axiom % 0.18/0.40 15. (-. (-. (gt (n0) T_1))) (-. (gt (n0) T_1)) ### NotNot 14 % 0.18/0.40 16. (-. (drugsu T_1)) (drugsu T_1) ### Axiom % 0.18/0.40 17. ((drugbg T_1) /\ (drugsu T_1)) (-. (drugsu T_1)) ### And 16 % 0.18/0.40 18. ((-. (gt (n0) T_1)) => ((drugbg T_1) /\ (drugsu T_1))) (-. (drugsu T_1)) (-. (gt (n0) T_1)) ### Imply 15 17 % 0.18/0.40 19. (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (-. (gt (n0) T_1)) (-. (drugsu T_1)) ### All 18 % 0.18/0.40 20. (-. ((-. (gt (n0) T_1)) => (drugsu T_1))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### NotImply 19 % 0.18/0.40 21. (-. (All X1, ((-. (gt (n0) X1)) => (drugsu X1)))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### NotAllEx 20 % 0.18/0.40 22. (bcapacityne (n0)) (-. (bcapacityne (n0))) ### Axiom % 0.18/0.40 23. (bcapacityex (n0)) (-. (bcapacityex (n0))) ### Axiom % 0.18/0.40 24. ((-. (bcapacityne (n0))) \/ (-. (bcapacityex (n0)))) (bcapacityex (n0)) (bcapacityne (n0)) ### Or 22 23 % 0.18/0.40 25. (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (bcapacityne (n0)) (bcapacityex (n0)) ### All 24 % 0.18/0.40 26. (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) ### Axiom % 0.18/0.40 27. (((All X1, ((-. (gt (n0) X1)) => (drugsu X1))) /\ (-. (bcapacityex (n0)))) => (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (bcapacityne (n0)) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### DisjTree 21 25 26 % 0.18/0.40 28. (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (bcapacityne (n0)) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) ### All 27 % 0.18/0.40 29. (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((gt (n0) X0) => (conditionhyper X0)))) ### Axiom % 0.18/0.40 30. (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0))) ### Axiom % 0.18/0.40 31. ((((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) /\ ((bcapacityne (n0)) /\ ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ (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))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (bcapacityne (n0)) (All X0, ((All X1, ((-. (gt X0 X1)) => (drugbg X1))) => (All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) ### DisjTree 12 13 28 29 30 % 0.18/0.40 32. (All X0, ((((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) /\ ((bcapacityne X0) /\ ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) (All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (drugbg X1))) => (All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))))) (bcapacityne (n0)) (All X0, (((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))) => (All X1, ((-. (gt X0 X1)) => (bsecretioni X1))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0)))) ### All 31 % 0.18/0.40 33. (-. (((All X0, ((-. (gt (n0) X0)) => ((drugbg X0) /\ (drugsu X0)))) /\ ((All X0, ((gt (n0) X0) => (conditionhyper X0))) /\ (bcapacityne (n0)))) => (All X0, ((-. (gt (n0) X0)) => (conditionnormo X0))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex 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)) => (drugbg X1))) => (All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))))) (All X0, ((((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) /\ ((bcapacityne X0) /\ ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) => (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) ### ConjTree 32 % 0.18/0.40 % SZS output end Proof % 0.18/0.40 (* END-PROOF *) %------------------------------------------------------------------------------