%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : MED009+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 : n011.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:56:01 EDT 2022 % Result : Theorem 117.43s 117.69s % Output : Proof 117.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MED009+1 : TPTP v8.1.0. Released v3.2.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 5 01:46:52 EDT 2022 % 0.13/0.34 % CPUTime : % 117.43/117.69 % SZS status Theorem % 117.43/117.69 (* PROOF-FOUND *) % 117.43/117.69 (* BEGIN-PROOF *) % 117.43/117.69 % SZS output start Proof % 117.43/117.69 1. (s1 (n0)) (-. (s1 (n0))) ### Axiom % 117.43/117.69 2. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1)))) ### Axiom % 117.43/117.69 3. (-. (bcapacitysn (n0))) (bcapacitysn (n0)) ### Axiom % 117.43/117.69 4. ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ ((bcapacitysn (n0)) /\ ((qilt27 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (-. (bcapacitysn (n0))) ### ConjTree 3 % 117.43/117.69 5. (-. (bcapacitysn (n0))) (bcapacitysn (n0)) ### Axiom % 117.43/117.69 6. ((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) /\ ((bcapacitysn (n0)) /\ ((-. (qilt27 (n0))) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (-. (bcapacitysn (n0))) ### ConjTree 5 % 117.43/117.69 7. (-. (gt (n0) T_0)) (gt (n0) T_0) ### Axiom % 117.43/117.69 8. (-. (gt (n0) T_0)) (gt (n0) T_0) ### Axiom % 117.43/117.69 9. (-. (-. (gt (n0) T_0))) (-. (gt (n0) T_0)) ### NotNot 8 % 117.43/117.69 10. (releaselg T_0) (-. (releaselg T_0)) ### Axiom % 117.43/117.69 11. ((-. (gt (n0) T_0)) => (-. (releaselg T_0))) (releaselg T_0) (-. (gt (n0) T_0)) ### Imply 9 10 % 117.43/117.69 12. (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) (releaselg T_0) ### All 11 % 117.43/117.69 13. (-. (uptakelg T_0)) (uptakelg T_0) ### Axiom % 117.43/117.69 14. ((-. (gt (n0) T_0)) => ((-. (releaselg T_0)) => (uptakelg T_0))) (-. (uptakelg T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) ### DisjTree 7 12 13 % 117.43/117.69 15. (All X1, ((-. (gt (n0) X1)) => ((-. (releaselg X1)) => (uptakelg X1)))) (-. (gt (n0) T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (uptakelg T_0)) ### All 14 % 117.43/117.69 16. (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (-. (uptakelg T_0)) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (-. (gt (n0) T_0)) ### All 15 % 117.43/117.69 17. (-. ((-. (gt (n0) T_0)) => (uptakelg T_0))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) ### NotImply 16 % 117.43/117.69 18. (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) ### NotAllEx 17 % 117.43/117.69 19. (-. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) ### NotOr 18 % 117.43/117.69 20. (-. (gt (n0) (n0))) (gt (n0) (n0)) ### Axiom % 117.43/117.69 21. (-. (-. (gt (n0) (n0)))) (-. (gt (n0) (n0))) ### NotNot 20 % 117.43/117.69 22. (-. (drugi (n0))) (drugi (n0)) ### Axiom % 117.43/117.69 23. ((-. (gt (n0) (n0))) => (drugi (n0))) (-. (drugi (n0))) (-. (gt (n0) (n0))) ### Imply 21 22 % 117.43/117.69 24. (All X1, ((-. (gt (n0) X1)) => (drugi X1))) (-. (gt (n0) (n0))) (-. (drugi (n0))) ### All 23 % 117.43/117.69 25. (((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) => (All X1, ((-. (gt (n0) X1)) => (drugi X1)))) (-. (drugi (n0))) (-. (gt (n0) (n0))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) ### Imply 19 24 % 117.43/117.69 26. (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)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (-. (gt (n0) (n0))) (-. (drugi (n0))) ### All 25 % 117.43/117.69 27. (s1 (n0)) (-. (s1 (n0))) ### Axiom % 117.43/117.69 28. (s3 (n0)) (-. (s3 (n0))) ### Axiom % 117.43/117.69 29. ((-. (s1 (n0))) \/ (-. (s3 (n0)))) (s3 (n0)) (s1 (n0)) ### Or 27 28 % 117.43/117.69 30. (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) (s3 (n0)) ### All 29 % 117.43/117.69 31. ((drugi (n0)) => (s3 (n0))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (-. (gt (n0) (n0))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg 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 26 30 % 117.43/117.69 32. (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)) => (-. (releaselg X1)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (-. (gt (n0) (n0))) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) ### All 31 % 117.43/117.69 33. (All X, (-. (gt X X))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (All X0, (All X1, ((-. (gt X0 X1)) => ((-. (releaselg X1)) => (uptakelg X1))))) (All X1, ((-. (gt (n0) X1)) => (-. (releaselg 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))) ### All 32 % 117.43/117.69 34. (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) (-. (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) ### Axiom % 117.43/117.69 35. (-. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) ### NotOr 34 % 117.43/117.69 36. (((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) => (All X1, ((-. (gt (n0) X1)) => (drugi X1)))) (-. (drugi (n0))) (-. (gt (n0) (n0))) (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) ### Imply 35 24 % 117.43/117.69 37. (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)) => (uptakepg X1))) (-. (gt (n0) (n0))) (-. (drugi (n0))) ### All 36 % 117.43/117.69 38. ((drugi (n0)) => (s3 (n0))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (-. (gt (n0) (n0))) (All X1, ((-. (gt (n0) X1)) => (uptakepg 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 37 30 % 117.43/117.69 39. (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)) => (uptakepg X1))) (-. (gt (n0) (n0))) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) ### All 38 % 117.43/117.69 40. (All X, (-. (gt X X))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (All X1, ((-. (gt (n0) X1)) => (uptakepg 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))) ### All 39 % 117.43/117.69 41. ((All X1, ((-. (gt (n0) X1)) => (-. (releaselg X1)))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) (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 X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) (All X, (-. (gt X X))) ### Or 33 40 % 117.43/117.69 42. (((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 X, (-. (gt X X))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 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 X0, ((drugi X0) => (s3 X0))) ### ConjTree 41 % 117.43/117.69 43. (s1 (n0)) (-. (s1 (n0))) ### Axiom % 117.43/117.69 44. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1)))) ### Axiom % 117.43/117.69 45. (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) ### Axiom % 117.43/117.69 46. ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) /\ ((bcapacitysn (n0)) /\ ((qilt27 (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) ### ConjTree 45 % 117.43/117.69 47. (-. (bcapacityne (n0))) (bcapacityne (n0)) ### Axiom % 117.43/117.69 48. (((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)))))) (-. (bcapacityne (n0))) ### ConjTree 47 % 117.43/117.69 49. (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) (All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) ### Axiom % 117.43/117.69 50. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) /\ ((All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) /\ ((bcapacityex (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) ### ConjTree 49 % 117.43/117.69 51. ((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 X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) (-. (bcapacityne (n0))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) ### DisjTree 44 46 6 48 50 % 117.43/117.69 52. (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 X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (-. (bcapacityne (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (uptakelg X1)))) ### All 51 % 117.43/117.69 53. (-. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1))))) (-. (bcapacityne (n0))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (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))))))))))) ### NotOr 52 % 117.43/117.69 54. (((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt (n0) X1)) => (uptakepg X1)))) => (All X1, ((-. (gt (n0) X1)) => (drugi X1)))) (-. (drugi (n0))) (-. (gt (n0) (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 X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (-. (bcapacityne (n0))) ### Imply 53 24 % 117.43/117.69 55. (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) (-. (bcapacityne (n0))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (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))))))))))) (-. (gt (n0) (n0))) (-. (drugi (n0))) ### All 54 % 117.43/117.69 56. (All X, (-. (gt X X))) (-. (drugi (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 X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (-. (bcapacityne (n0))) (All X0, (((All X1, ((-. (gt X0 X1)) => (uptakelg X1))) \/ (All X1, ((-. (gt X0 X1)) => (uptakepg X1)))) => (All X1, ((-. (gt X0 X1)) => (drugi X1))))) ### All 55 % 117.43/117.69 57. ((drugi (n0)) => (s3 (n0))) (s1 (n0)) (All X0, ((-. (s1 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))))) (-. (bcapacityne (n0))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (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 X, (-. (gt X X))) ### Imply 56 30 % 117.43/117.69 58. (All X0, ((drugi X0) => (s3 X0))) (All X, (-. (gt X X))) (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 X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (-. (bcapacityne (n0))) (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, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) ### All 57 % 117.43/117.69 59. (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0)))))) ### Axiom % 117.43/117.69 60. (((s1 (n0)) /\ (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))))) => (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (All X0, ((-. (s1 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))))) (-. (bcapacityne (n0))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (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 X, (-. (gt X X))) (All X0, ((drugi X0) => (s3 X0))) (s1 (n0)) ### DisjTree 43 58 59 % 117.43/117.69 61. (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (s1 (n0)) (All X0, ((drugi X0) => (s3 X0))) (All X, (-. (gt X X))) (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)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (-. (bcapacityne (n0))) (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, ((-. (s1 X0)) \/ (-. (s3 X0)))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) ### All 60 % 117.43/117.69 62. (bcapacityex (n0)) (-. (bcapacityex (n0))) ### Axiom % 117.43/117.69 63. ((-. (bcapacityne (n0))) \/ (-. (bcapacityex (n0)))) (bcapacityex (n0)) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (All X0, ((-. (s1 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))))) (-. (bcapacitysn (n0))) (-. (All X1, ((-. (gt (n0) X1)) => (bsecretioni X1)))) (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 X, (-. (gt X X))) (All X0, ((drugi X0) => (s3 X0))) (s1 (n0)) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) ### Or 61 62 % 117.43/117.69 64. (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (s1 (n0)) (All X0, ((drugi X0) => (s3 X0))) (All X, (-. (gt X X))) (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)) => (bsecretioni X1)))) (-. (bcapacitysn (n0))) (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, ((-. (s1 X0)) \/ (-. (s3 X0)))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (bcapacityex (n0)) ### All 63 % 117.43/117.69 65. (bcapacityex (n0)) (-. (bcapacityex (n0))) ### Axiom % 117.43/117.69 66. ((All X1, ((-. (gt (n0) X1)) => (drugsu X1))) /\ (-. (bcapacityex (n0)))) (bcapacityex (n0)) ### And 65 % 117.43/117.69 67. ((All X1, ((-. (gt (n0) X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt (n0) X1)) => (drugsu X1))) /\ (-. (bcapacityex (n0))))) (bcapacityex (n0)) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (All X0, ((-. (s1 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))))) (-. (bcapacitysn (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 X, (-. (gt X X))) (All X0, ((drugi X0) => (s3 X0))) (s1 (n0)) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) ### Imply 64 66 % 117.43/117.69 68. (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (s1 (n0)) (All X0, ((drugi X0) => (s3 X0))) (All X, (-. (gt X X))) (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))))))))))) (-. (bcapacitysn (n0))) (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, ((-. (s1 X0)) \/ (-. (s3 X0)))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (bcapacityex (n0)) ### All 67 % 117.43/117.69 69. ((All X1, ((-. (gt (n0) X1)) => (uptakelg X1))) /\ ((All X1, ((-. (gt (n0) X1)) => (uptakepg X1))) /\ ((bcapacityex (n0)) /\ (All X0, ((gt (n0) X0) => (conditionhyper X0)))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (All X0, ((-. (s1 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))))) (-. (bcapacitysn (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 X, (-. (gt X X))) (All X0, ((drugi X0) => (s3 X0))) (s1 (n0)) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) ### ConjTree 68 % 117.43/117.69 70. ((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)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (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))))))))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (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 X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (s1 (n0)) (All X, (-. (gt X X))) (-. (bcapacitysn (n0))) (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) ### DisjTree 2 4 6 42 69 % 117.43/117.69 71. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))) (-. (bcapacitysn (n0))) (All X, (-. (gt X X))) (s1 (n0)) (All X0, ((-. (s1 X0)) \/ (-. (s3 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 X0, ((drugi X0) => (s3 X0))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex 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, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) ### All 70 % 117.50/117.69 72. (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0)))))) ### Axiom % 117.50/117.69 73. (((s1 (n0)) /\ (-. (All X1, ((-. (gt (n0) X1)) => (conditionnormo X1))))) => (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (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))))))))))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0))))))) (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 X0, ((-. (s1 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) (-. (bcapacitysn (n0))) (s1 (n0)) ### DisjTree 1 71 72 % 117.50/117.69 74. (s1 (n0)) (-. (bcapacitysn (n0))) (All X, (-. (gt X X))) (All X0, ((-. (s1 X0)) \/ (-. (s3 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 X0, ((drugi X0) => (s3 X0))) (-. (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex 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, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) ### All 73 % 117.50/117.69 75. (-. (((s1 (n0)) /\ ((All X0, ((gt (n0) X0) => (conditionhyper X0))) /\ ((-. (bcapacitysn (n0))) /\ (-. (qilt27 (n0)))))) => (Ex X0, ((-. (gt (n0) X0)) /\ ((s2 X0) /\ ((All X1, ((gt X0 X1) => (conditionhyper X1))) /\ ((bcapacityne X0) \/ (bcapacityex X0)))))))) (All X0, ((All X1, ((-. (gt X0 X1)) => (bsecretioni X1))) => ((All X1, ((-. (gt X0 X1)) => (drugsu X1))) /\ (-. (bcapacityex X0))))) (All X0, ((-. (bcapacityne X0)) \/ (-. (bcapacityex X0)))) (All X0, (((s1 X0) /\ (-. (All X1, ((-. (gt X0 X1)) => (conditionnormo X1))))) => (Ex X1, ((-. (gt X0 X1)) /\ ((s2 X1) /\ ((All X2, ((gt X1 X2) => (conditionhyper X2))) /\ ((bcapacityne X1) \/ (bcapacityex X1)))))))) (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, (((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, ((-. (s1 X0)) \/ (-. (s3 X0)))) (All X, (-. (gt X X))) ### ConjTree 74 % 117.50/117.69 % SZS output end Proof % 117.50/117.69 (* END-PROOF *) %------------------------------------------------------------------------------