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