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