ag-gipp/GoUldI

<math 
  xmlns="http://www.w3.org/1998/Math/MathML" display="block" alttext="upper C o n left-parenthesis upper Z upper F plus normal not-sign upper A upper C right-parenthesis">
  <semantics>
    <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="21" data-semantic-children="0,1,2,17" data-semantic-content="18,19,20">
      <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="0" data-semantic-parent="21">C</mi>
      <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="18" data-semantic-parent="21" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
      <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="1" data-semantic-parent="21">o</mi>
      <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="19" data-semantic-parent="21" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
      <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="2" data-semantic-parent="21">n</mi>
      <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="20" data-semantic-parent="21" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
      <mrow data-semantic-type="fenced" data-semantic-role="leftright" data-semantic-id="17" data-semantic-children="16" data-semantic-content="3,10" data-semantic-parent="21">
        <mo stretchy="false" data-semantic-type="fence" data-semantic-role="open" data-semantic-id="3" data-semantic-parent="17" data-semantic-operator="fenced">(</mo>
        <mrow data-semantic-type="infixop" data-semantic-role="addition" data-semantic-id="16" data-semantic-children="12,15" data-semantic-content="6" data-semantic-parent="17">
          <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="12" data-semantic-children="4,5" data-semantic-content="11" data-semantic-parent="16">
            <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="4" data-semantic-parent="12">Z</mi>
            <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="11" data-semantic-parent="12" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
            <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="5" data-semantic-parent="12">F</mi>
          </mrow>
          <mo data-semantic-type="operator" data-semantic-role="addition" data-semantic-id="6" data-semantic-parent="16" data-semantic-operator="infixop,+">+</mo>
          <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="15" data-semantic-children="7,8,9" data-semantic-content="13,14" data-semantic-parent="16">
            <mi mathvariant="normal" data-semantic-type="identifier" data-semantic-role="unknown" data-semantic-font="normal" data-semantic-id="7" data-semantic-parent="15">¬
              <!-- ¬ -->
            </mi>
            <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="13" data-semantic-parent="15" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
            <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="8" data-semantic-parent="15">A</mi>
            <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="14" data-semantic-parent="15" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
            <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="9" data-semantic-parent="15">C</mi>
          </mrow>
        </mrow>
        <mo stretchy="false" data-semantic-type="fence" data-semantic-role="close" data-semantic-id="10" data-semantic-parent="17" data-semantic-operator="fenced">)</mo>
      </mrow>
    </mrow>
    <annotation encoding="application/x-tex">Con(ZF+\neg AC)</annotation>
  </semantics>
</math>