%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : MED005+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 : n015.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:59 EDT 2022 % Result : Theorem 28.81s 29.04s % Output : Proof 28.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : MED005+1 : TPTP v8.1.0. Released v3.2.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n015.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:38:17 EDT 2022 % 0.12/0.34 % CPUTime : % 28.81/29.04 % SZS status Theorem % 28.81/29.04 (* PROOF-FOUND *) % 28.81/29.04 (* BEGIN-PROOF *) % 28.81/29.04 % SZS output start Proof % 28.81/29.04 1. (gt (n0) (n0)) (-. (gt (n0) (n0))) ### Axiom % 28.81/29.04 2. (All X, (-. (gt X X))) (gt (n0) (n0)) ### All 1 % 28.81/29.04 3. (s0 (n0)) (-. (s0 (n0))) ### Axiom % 28.81/29.04 4. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1)))) ### Axiom % 28.81/29.04 5. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) ### Axiom % 28.81/29.04 6. (-. (-. (gt (n0) (n0)))) (All X, (-. (gt X X))) ### NotNot 2 % 28.81/29.04 7. (-. (drugsu (n0))) (drugsu (n0)) ### Axiom % 28.81/29.04 8. ((-. (gt (n0) (n0))) => (drugsu (n0))) (-. (drugsu (n0))) (All X, (-. (gt X X))) ### Imply 6 7 % 28.81/29.04 9. (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X, (-. (gt X X))) (-. (drugsu (n0))) ### All 8 % 28.81/29.04 10. (-. (s1 (n0))) (s1 (n0)) ### Axiom % 28.81/29.04 11. ((s1 (n0)) /\ (qillt27 (n0))) (-. (s1 (n0))) ### And 10 % 28.81/29.04 12. (s0 (n0)) (-. (s0 (n0))) ### Axiom % 28.81/29.04 13. (s2 (n0)) (-. (s2 (n0))) ### Axiom % 28.81/29.04 14. ((-. (s0 (n0))) \/ (-. (s2 (n0)))) (s2 (n0)) (s0 (n0)) ### Or 12 13 % 28.81/29.04 15. (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (s2 (n0)) ### All 14 % 28.81/29.04 16. (-. (s3 (n0))) (s3 (n0)) ### Axiom % 28.81/29.04 17. ((drugsu (n0)) => (((s1 (n0)) /\ (qillt27 (n0))) \/ ((s2 (n0)) \/ (s3 (n0))))) (-. (s3 (n0))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) ### DisjTree 9 11 15 16 % 28.81/29.04 18. (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (-. (s3 (n0))) ### All 17 % 28.81/29.04 19. (-. (drugi (n0))) (drugi (n0)) ### Axiom % 28.81/29.04 20. ((drugi (n0)) /\ ((drugsu (n0)) \/ (drugbg (n0)))) (-. (drugi (n0))) ### And 19 % 28.81/29.04 21. (-. (drugi (n0))) (drugi (n0)) ### Axiom % 28.81/29.04 22. ((s3 (n0)) => (((drugi (n0)) /\ ((drugsu (n0)) \/ (drugbg (n0)))) \/ (drugi (n0)))) (-. (drugi (n0))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) ### DisjTree 18 20 21 % 28.81/29.04 23. (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (-. (drugi (n0))) ### All 22 % 28.81/29.04 24. (s0 (n0)) (-. (s0 (n0))) ### Axiom % 28.81/29.04 25. (s3 (n0)) (-. (s3 (n0))) ### Axiom % 28.81/29.04 26. ((-. (s0 (n0))) \/ (-. (s3 (n0)))) (s3 (n0)) (s0 (n0)) ### Or 24 25 % 28.81/29.04 27. (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) (s3 (n0)) ### All 26 % 28.81/29.04 28. ((drugi (n0)) => (s3 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) ### Imply 23 27 % 28.81/29.04 29. (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X1, ((-. (gt (n0) X1)) => (drugsu X1))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) ### All 28 % 28.81/29.04 30. ((All X1, ((-. (gt (n0) X1)) => (drugsu X1))) /\ (-. (bcapacityex (n0)))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) ### And 29 % 28.81/29.04 31. ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt (n0) X1)) => (drugsu X1))) /\ (-. (bcapacityex (n0))))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) ### Imply 5 30 % 28.81/29.04 32. (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) ### All 31 % 28.81/29.04 33. ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ ((bcapacitysn (n0)) /\ ((qilt27 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) ### ConjTree 32 % 28.81/29.04 34. (-. (gt T_0 T_0)) (gt T_0 T_0) ### Axiom % 28.81/29.04 35. (-. (gt (n0) T_0)) (gt (n0) T_0) ### Axiom % 28.81/29.04 36. (-. (-. (gt (n0) T_0))) (-. (gt (n0) T_0)) ### NotNot 35 % 28.81/29.04 37. (releaselg T_0) (-. (releaselg T_0)) ### Axiom % 28.81/29.04 38. ((-. (gt (n0) T_0)) => (-. (releaselg T_0))) (releaselg T_0) (-. (gt (n0) T_0)) ### Imply 36 37 % 28.81/29.04 39. (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) (releaselg T_0) ### All 38 % 28.81/29.04 40. (-. (uptakelg T_0)) (uptakelg T_0) ### Axiom % 28.81/29.04 41. ((-. (gt T_0 T_0)) => ((-. (releaselg T_0)) => (uptakelg T_0))) (-. (uptakelg T_0)) (-. (gt (n0) T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt T_0 T_0)) ### DisjTree 34 39 40 % 28.81/29.04 42. (All X1, ((-. (gt T_0 X1)) => ((-. (releaselg X1)) => (uptakelg X1)))) (-. (gt T_0 T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) (-. (uptakelg T_0)) ### All 41 % 28.81/29.04 43. (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (-. (uptakelg T_0)) (-. (gt (n0) T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt T_0 T_0)) ### All 42 % 28.81/29.04 44. (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) (-. (uptakelg T_0)) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) ### All 43 % 28.81/29.04 45. (-. ((-. (gt (n0) T_0)) => (uptakelg T_0))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X, (-. (gt X X))) ### NotImply 44 % 28.81/29.04 46. (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) ### NotAllEx 45 % 28.81/29.04 47. (-. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X, (-. (gt X X))) ### NotOr 46 % 28.81/29.04 48. (-. (drugi (n0))) (drugi (n0)) ### Axiom % 28.81/29.04 49. ((-. (gt (n0) (n0))) => (drugi (n0))) (-. (drugi (n0))) (All X, (-. (gt X X))) ### Imply 6 48 % 28.81/29.04 50. (All X1, ((-. (gt (n0) X1)) => (drugi X1))) (All X, (-. (gt X X))) (-. (drugi (n0))) ### All 49 % 28.81/29.04 51. (((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) => (All X1, ((-. (gt (n0) X1)) => (drugi X1)))) (-. (drugi (n0))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) ### Imply 47 50 % 28.81/29.04 52. (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X, (-. (gt X X))) (-. (drugi (n0))) ### All 51 % 28.81/29.04 53. ((drugi (n0)) => (s3 (n0))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) ### Imply 52 27 % 28.81/29.04 54. (All X0, ((drugi X0) => (s3 X0))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X, (-. (gt X X))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) ### All 53 % 28.81/29.04 55. ((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn (n0)) /\ ((-. (qilt27 (n0))) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, ((drugi X0) => (s3 X0))) ### ConjTree 54 % 28.81/29.04 56. (((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, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) ### ConjTree 32 % 28.81/29.04 57. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) ### Axiom % 28.81/29.04 58. (-. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) ### NotOr 57 % 28.81/29.04 59. (((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) => (All X1, ((-. (gt (n0) X1)) => (drugi X1)))) (-. (drugi (n0))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) ### Imply 58 50 % 28.81/29.04 60. (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) (All X, (-. (gt X X))) (-. (drugi (n0))) ### All 59 % 28.81/29.04 61. ((drugi (n0)) => (s3 (n0))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) ### Imply 60 27 % 28.81/29.04 62. (All X0, ((drugi X0) => (s3 X0))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) (All X, (-. (gt X X))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) ### All 61 % 28.81/29.04 63. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) /\ ((All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) /\ ((bcapacityex (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, ((drugi X0) => (s3 X0))) ### ConjTree 62 % 28.81/29.04 64. ((All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ ((bcapacitysn (n0)) /\ ((qilt27 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) \/ (((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn (n0)) /\ ((-. (qilt27 (n0))) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) \/ ((((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 X1, ((-. (gt (n0) X1)) => (uptakelg X1))) /\ ((All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) /\ ((bcapacityex (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) ### DisjTree 4 33 55 56 63 % 28.81/29.04 65. (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (s0 (n0)) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) ### All 64 % 28.81/29.04 66. (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) ### Axiom % 28.81/29.04 67. (((s0 (n0)) /\ (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))))) => (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (-. (s1 (n0))) (All X, (-. (gt X X))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (s0 (n0)) ### DisjTree 3 65 66 % 28.81/29.04 68. (All X0, (((s0 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s1 X1) /\ (All X2, ((gt X1 X2) => (conditionhyper X2)))))))) (s0 (n0)) (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X, (-. (gt X X))) (-. (s1 (n0))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) ### All 67 % 28.81/29.04 69. (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (All X0, ((gt (n0) X0) => (conditionhyper X0)))) ### Axiom % 28.81/29.04 70. (-. ((-. (gt (n0) (n0))) /\ ((s1 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (All X0, ((gt (n0) X0) => (conditionhyper X0))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (s0 (n0)) (All X0, (((s0 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s1 X1) /\ (All X2, ((gt X1 X2) => (conditionhyper X2)))))))) (All X, (-. (gt X X))) ### DisjTree 2 68 69 % 28.81/29.04 71. (All X, (-. (gt X X))) (All X0, (((s0 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s1 X1) /\ (All X2, ((gt X1 X2) => (conditionhyper X2)))))))) (s0 (n0)) (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))) (All X0, ((gt (n0) X0) => (conditionhyper X0))) ### NotExists 70 % 28.81/29.04 72. (-. (((s0 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))) => (Ex X0, ((-. (gt (n0) X0)) /\ ((s1 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (s0 X0)) \/ (-. (s3 X0)))) (All X0, ((-. (s0 X0)) \/ (-. (s2 X0)))) (All X0, ((drugsu X0) => (((s1 X0) /\ (qillt27 X0)) \/ ((s2 X0) \/ (s3 X0))))) (All X0, ((s3 X0) => (((drugi X0) /\ ((drugsu X0) \/ (drugbg X0))) \/ (drugi X0)))) (All X0, ((drugi X0) => (s3 X0))) (All X0, ((All X1, ((-. (gt X0 X1)) => (conditionnormo X1))) => (((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) /\ ((bcapacitysn X0) /\ ((qilt27 X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ (((All X1, ((-. (gt X0 X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn X0) /\ ((-. (qilt27 X0)) /\ (All X1, ((gt X0 X1) => (conditionhyper X1)))))) \/ ((((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)) => (uptakelg X1))) /\ ((All X1, ((-. (gt X0 X1)) => (uptakepg X1))) /\ ((bcapacityex X0) /\ (All X1, ((gt X0 X1) => (conditionhyper X1))))))))))) (All X0, (((s0 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s1 X1) /\ (All X2, ((gt X1 X2) => (conditionhyper X2)))))))) (All X, (-. (gt X X))) ### ConjTree 71 % 28.81/29.04 % SZS output end Proof % 28.81/29.04 (* END-PROOF *) %------------------------------------------------------------------------------