\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{MED001+0.ax} Physiology Diabetes Mellitus type 2

Physiological mechanisms of diabetes mellitus type 2




$\forall x{:}\;\neg\,\mbox{gt}(x,x)\qquad\mbox{fof}(\mbox{irreflexivity\_gt},\mbox{axiom})$

$\forall x,y,z{:}\;( ( \mbox{gt}(x,y)\mbox{ and }\mbox{gt}(y,z) ) \ \Rightarrow \ \mbox{gt}(x,z) )\qquad\mbox{fof}(\mbox{transitivity\_gt},\mbox{axiom})$

$\forall x_0{:}\;( \mbox{bcapacityne}(x_0)\mbox{ or }\mbox{bcapacityex}(x_0)\mbox{ or }\mbox{bcapacitysn}(x_0) )\qquad\mbox{fof}(\mbox{xorcapacity}_1,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{bcapacityne}(x_0)\mbox{ or }\neg\,\mbox{bcapacityex}(x_0) )\qquad\mbox{fof}(\mbox{xorcapacity}_2,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{bcapacityne}(x_0)\mbox{ or }\neg\,\mbox{bcapacitysn}(x_0) )\qquad\mbox{fof}(\mbox{xorcapacity}_3,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{bcapacityex}(x_0)\mbox{ or }\neg\,\mbox{bcapacitysn}(x_0) )\qquad\mbox{fof}(\mbox{xorcapacity}_4,\mbox{axiom})$

$\forall x_0{:}\;( \mbox{conditionhyper}(x_0)\mbox{ or }\mbox{conditionhypo}(x_0)\mbox{ or }\mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{xorcondition}_1,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{conditionhyper}(x_0)\mbox{ or }\neg\,\mbox{conditionhypo}(x_0) )\qquad\mbox{fof}(\mbox{xorcondition}_2,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{conditionhyper}(x_0)\mbox{ or }\neg\,\mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{xorcondition}_3,\mbox{axiom})$

$\forall x_0{:}\;( \neg\,\mbox{conditionhypo}(x_0)\mbox{ or }\neg\,\mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{xorcondition}_4,\mbox{axiom})$

$\forall x_0{:}\;( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{drugi}(x_1) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ ( \mbox{uptakelg}(x_1)\mbox{ and }\mbox{uptakepg}(x_1) ) ) )\qquad\mbox{fof}(\mbox{insulin\_effect},\mbox{axiom})$

$\forall x_0,x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ ( \mbox{uptakelg}(x_1) \ \Rightarrow \ \neg\,\mbox{releaselg}(x_1) ) )\qquad\mbox{fof}(\mbox{liver\_glucose},\mbox{axiom})$

$\forall x_0{:}\;( ( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{drugsu}(x_1) )\mbox{ and }\neg\,\mbox{bcapacityex}(x_0) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{bsecretioni}(x_1) ) )\qquad\mbox{fof}(\mbox{sulfonylurea\_effect},\mbox{axiom})$

$\forall x_0{:}\;( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{drugbg}(x_1) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \neg\,\mbox{releaselg}(x_1) ) )\qquad\mbox{fof}(\mbox{biguanide\_effect},\mbox{axiom})$

$\forall x_0{:}\;( ( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{bsecretioni}(x_1) )\mbox{ and }\mbox{bcapacitysn}(x_0)\mbox{ and }\mbox{qilt}_{27}(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) ) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionnormo}(x_1) ) )\qquad\mbox{fof}(\mbox{sn\_cure}_1,\mbox{axiom})$

$\forall x_0{:}\;( ( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \neg\,\mbox{releaselg}(x_1) )\mbox{ and }\mbox{bcapacitysn}(x_0)\mbox{ and }\neg\,\mbox{qilt}_{27}(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) ) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionnormo}(x_1) ) )\qquad\mbox{fof}(\mbox{sn\_cure}_2,\mbox{axiom})$

$\forall x_0{:}\;( ( ( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \neg\,\mbox{releaselg}(x_1) )\mbox{ or }\forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{uptakepg}(x_1) ) )\mbox{ and }\mbox{bcapacityne}(x_0)\mbox{ and }\forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{bsecretioni}(x_1) )\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) ) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionnormo}(x_1) ) )\qquad\mbox{fof}(\mbox{ne\_cure},\mbox{axiom})$

$\forall x_0{:}\;( ( \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{uptakelg}(x_1) )\mbox{ and }\forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{uptakepg}(x_1) )\mbox{ and }\mbox{bcapacityex}(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) ) ) \ \Rightarrow \ \forall x_1{:}\;( \neg\,\mbox{gt}(x_0,x_1) \ \Rightarrow \ ( \mbox{conditionnormo}(x_1)\mbox{ or }\mbox{conditionhypo}(x_1) ) ) )\qquad\mbox{fof}(\mbox{ex\_cure},\mbox{axiom})$

\medskip\textbf{MED007+1.p} Unsuccessful s1-qilt27 treatment next step

After unsuccessful treatment with single oral anti-diabetic for
 patients with QI less than 27 medical management moves to next
 step.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_1(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\neg\,\mbox{bcapacitysn}(n_0)\mbox{ and }\mbox{qilt}_{27}(n_0) ) \ \Rightarrow \ \exists x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0)\mbox{ and }s_2(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) )\mbox{ and }( \mbox{bcapacityne}(x_0)\mbox{ or }\mbox{bcapacityex}(x_0) ) )\qquad\mbox{fof}(\mbox{transs1s2\_qilt}_{27},\mbox{conjecture})$

\medskip\textbf{MED006+1.p} Unsuccessful s1-qilt27 treatment - single oral anti-diabetic

Unsuccessful treatment with single oral anti-diabetic for patients
 with QI less than 27 deductively follows in completed theory.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_1(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\neg\,\mbox{bcapacitysn}(n_0)\mbox{ and }\mbox{qilt}_{27}(n_0) ) \ \Rightarrow \ \neg\,\forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{unsuccessfuls1\_qilt}_{27},\mbox{conjecture})$

\medskip\textbf{MED012+1.p} Physiology Diabetes Mellitus type 2






$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

\medskip\textbf{MED003+1.p} Insulin treatment

Whether or not patients with exhausted production of glucose in
 the B-cells are at least not hyperglycaemic afterwards.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$( \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{drugi}(x_0) )\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\mbox{bcapacityex}(n_0) ) \ \Rightarrow \ \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ ( \mbox{conditionnormo}(x_0)\mbox{ or }\mbox{conditionhypo}(x_0) ) )\qquad\mbox{fof}(\mbox{treatmentex},\mbox{conjecture})$

\medskip\textbf{MED009+1.p} Unsuccessful s1-qige27 treatment - next step

After unsuccessful treatment with single oral anti-diabetic for
 patients with QI greater equal than 27 medical management moves
 to next step.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_1(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\neg\,\mbox{bcapacitysn}(n_0)\mbox{ and }\neg\,\mbox{qilt}_{27}(n_0) ) \ \Rightarrow \ \exists x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0)\mbox{ and }s_2(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) )\mbox{ and }( \mbox{bcapacityne}(x_0)\mbox{ or }\mbox{bcapacityex}(x_0) ) )\qquad\mbox{fof}(\mbox{transs1s2\_qige}_{27},\mbox{conjecture})$

\medskip\textbf{MED002+1.p} Combined biguanide and sulfonylurea treatment

Whether or not patients with nearly-exhausted production of
 glucose in the B-cells are cured with a biguanide and sulfonylurea
 combination therapy.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$( \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ ( \mbox{drugbg}(x_0)\mbox{ and }\mbox{drugsu}(x_0) ) )\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\mbox{bcapacityne}(n_0) ) \ \Rightarrow \ \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{treatmentne},\mbox{conjecture})$

\medskip\textbf{MED005+1.p} Unsuccessful diet treatment

Unsuccessful treatment of diet requires that medical management
 moves to at least oral diabetics.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_0(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) ) ) \ \Rightarrow \ \exists x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0)\mbox{ and }s_1(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) ) )\qquad\mbox{fof}(\mbox{transs0s}_1,\mbox{conjecture})$

\medskip\textbf{MED001+1.p} Sulfonylurea treatment

Whether or not patients with subnormal production of glucose in
 the B-cells and a low QI index are cured with sulfonylurea.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$( \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{drugsu}(x_0) )\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\mbox{bcapacitysn}(n_0)\mbox{ and }\mbox{qilt}_{27}(n_0) ) \ \Rightarrow \ \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{treatmentsn}_2,\mbox{conjecture})$

\medskip\textbf{MED010+1.p} Unsuccessful s1-qilt27 treatment - two oral anti-diabetic

After unsuccessful treatment with two oral anti-diabetic medical
 management moves to next step.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_2(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\mbox{bcapacityex}(n_0) ) \ \Rightarrow \ \exists x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0)\mbox{ and }s_3(x_0)\mbox{ and }\forall x_1{:}\;( \mbox{gt}(x_0,x_1) \ \Rightarrow \ \mbox{conditionhyper}(x_1) )\mbox{ and }\mbox{bcapacityex}(x_0) )\qquad\mbox{fof}(\mbox{unsuccesfuls}_2,\mbox{conjecture})$

\medskip\textbf{MED008+1.p} Unsuccessful s1-qige27 treatment

Unsuccessful treatment with single oral anti-diabetic for patients
 with QI greater equal than 27 deductively follows in completed
 theory.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/MED001+1.ax'})$

$( s_1(n_0)\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\neg\,\mbox{bcapacitysn}(n_0)\mbox{ and }\neg\,\mbox{qilt}_{27}(n_0) ) \ \Rightarrow \ \neg\,\forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{unsuccessfuls1\_qige}_{27},\mbox{conjecture})$

\medskip\textbf{MED004+1.p} No suitable therapy for patients with exhausted B-cells

There is not a suitable therapy for patients with exhausted
 B-cells available.




$\mbox{include}(\mbox{'Axioms/MED001+0.ax'})$

$( \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ ( \mbox{drugi}(x_0)\mbox{ and }\mbox{drugsu}(x_0)\mbox{ and }\mbox{drugbg}(x_0) ) )\mbox{ and }\forall x_0{:}\;( \mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionhyper}(x_0) )\mbox{ and }\mbox{bcapacityex}(n_0) ) \ \Rightarrow \ \forall x_0{:}\;( \neg\,\mbox{gt}(n_0,x_0) \ \Rightarrow \ \mbox{conditionnormo}(x_0) )\qquad\mbox{fof}(\mbox{treatmentex\_sub},\mbox{conjecture})$

\medskip\textbf{MED011+1.p} Satisfiability of medical subject headings axioms






$\mbox{include}(\mbox{'Axioms/MED002+0.ax'})$

\medskip
\end{document}