examples_invalid.js

var invalidExamples = [
    { label: 'i1', formula: 'p' },
    { label: 'i2', formula: '((p→q)↔(q→p))' },
    { label: 'i3', formula: '∀xFx' },
    { label: 'i4', formula: '∃xFx' },
    { label: 'i5', formula: '∀x∃yRxy' },
    { label: 'i6', formula: '∃y∀xFxy' },
    { label: 'ifun', formula: '∀x∃y (Fx → Ff(y)) → (¬Fa ∨ Ff(a))' },
    { label: 'Her', formula: '¬∀x((Fx ∧ ¬Fa)∨ Ga)' },
    { label: 'bost1', formula: '∀x∀y∀z(Fxy∧Fyz→Fxz) ∧ ∀x∀y(Fxy→Fyx) ∧ ∃x∃yFxy → ∀xFxx' },
    { label: '2ind', formula: '¬∃x∃y(Fx∧¬Fy)' },
    { label: '3ind', formula: '¬∀y∃x(Ryx ∧ ¬Rxy)' },
    { label: '4indsimp', formula: '¬(Fa ∧ Ga ∧ Fb ∧ ¬Gb ∧ ¬Fc ∧ Gc ∧ ¬Fd ∧ ¬Gd)' },
    { label: '4ind', formula: '∀z∀y∃x(Rzx ∧ ¬Rxy)' },
    { label: 'bx', formula: '∀y∃xFxy→∃x∀yFxy' },
    { label: 'bn', formula: '∃y∃z∀x((Fx→Gy)∧(Gz→Fx))→∀x∃y(Fy↔Gy)' },
    { label: 'conpos1', formula: '∀y(Iy→∀x(Px↔Cxy))→∀x(Px↔∀y(Iy→Cxy))' },
    { label: 'conpos2', formula: '∀x(Px↔∀y(Iy→Cxy))→∀y(Iy→∀x(Px↔Cxy))' },
    { label: 'github30', formula: '∃x∀y((Rxx∨¬Rxy∨Ryx∨Ryy)∧(¬Rxx∨Rxy∨Ryx∨Ryy)∧(¬Rxx∨¬Rxy∨Ryx∨Ryy))' },
    { label: 'pel48s', formula: '(a=b ∨ c=d) ∧ (a=c ∨ b=d) → a=d' },
    { label: 'T_in_K', formula: 'p→◇p' },
    { label: 'emil_in_K4', formula: '◇□A → (◇□B → ◇□(A ∧ B))||transitivity' },
    { label: 'parsercopy', formula: 'p → ◇□p↔□◇□p' },
    { label: '04vsG0_K4', formula: '((A ∧ ¬□A)→□¬□A) ∧ ((¬A ∧ ◇A) →□◇A) → (◇□A→□◇A)||transitivity' },
    { label: 'redinexD', formula: '◇(p→□◇p)||seriality' },
    { label: 'boxreds4', formula: '◇□p↔□◇□p||reflexivity|transitivity' },
    { label: 'github16', formula: '((∃x(◇(Ox∧Px)∧□(Ox→Mx)))∧(∀x(◇(Ox∧Mx)→□(Ox→Sx))∧◇∃x(Ox∧Mx)))→(∃x((Ox∧Sx)∧◇(Ox∧Px)))' },
    { label: 'withee_K4', formula: '□∀x□∀y(□Fx∨□Gy)→(□∀x□Fx∨□∀x□Gx)||transitivity' },
    { label: '7ind', formula: '¬∀z∀y∃x¬((Rxy → Ryx) ∨ Rzx)' },
    { label: 'logmod1', formula: '□◇p↔□◇□◇p  [reflexivity]' },
    { label: 'logmod2', formula: '(∃xDx↔∀x(□Gx→Dx))∧∀x(□Px↔□Nx)∧(□∃xGx↔□∀x(□Px↔Gx))∧(∀x(Gx→□Nx)↔∀x(Gx→□Gx))→∀x(¬Dx→□∃xNx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod3', formula: '(□(a∨b∨c)∧(□a↔□(b∨c))∧(□b↔□(a∨c))∧(□c↔□(a∨b)))→(□a∧□b∧□c)' },
    { label: 'logmod4', formula: '(□(a∨b∨c)∧(□a↔□(b∨c))∧(□b↔□(a∨c))∧(□c↔□(a∨b)))→(□a∧□b∧□c)  [reflexivity]' },
    { label: 'logmod5', formula: '□(a∨b∨c)∧(□a↔□(b∨c))∧(□b↔□(a∨c))∧(□c↔□(a∨b))∧¬□(a∧b∧c)|=¬◇(a∧b∧c)' },
    { label: 'logmod6', formula: '(A→□◇A)↔(◇A→□◇A)  [reflexivity, transitivity]' },
    { label: 'logmod7', formula: '((□¬□p→¬□p)∧(□¬□¬p→¬□¬p)∧(□¬□□p→¬□□p))→¬□(p∧□□¬p)  [seriality]' },
    { label: 'logmod8', formula: '(□p∨□q)↔□(□p∨□q)  [reflexivity, seriality]' },
    { label: 'logmod9', formula: '◇◇◇◇◇(a∨b∨c∨d∨e)↔◇◇◇◇¬(¬a∧¬b∧¬c∧¬d∧¬e)' },
    { label: 'logmod10', formula: '(∀x(◇Ex↔¬◇Ex)↔¬◇∃xEx)∧∀x(¬◇Ex↔◇¬∃xEx)∧∃xEx↔□∃xEx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod11', formula: '□◇□□◇□□◇□□□(¬(□p→p)→□(p↔□p)→□p)  [transitivity]' },
    { label: 'logmod12', formula: '((□□P→□P)∧(□P→□□P))∧((□P→◇□P)∧(◇□P→□P))  [reflexivity, symmetry, seriality]' },
    { label: 'logmod13', formula: '◇A↔□◇A∧◇G↔◇A∧A→◇G  [universality]' },
    { label: 'logmod14', formula: '(◇◇◇◇p∨◇◇◇◇◇q)↔◇◇◇◇◇(p∨q)' },
    { label: 'logmod15', formula: '(¬□¬p→¬□p∧□¬□p)↔¬□¬p→□¬□p  [euclidity]' },
    { label: 'logmod16', formula: '∀x(Px→◇Ex)∧(◇∃xGx↔∀x(Gx→Px)∧□∀x(Gx↔□Gx))∧(∀x(Gx→◇Ex)↔◇∃xGx)↔□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod17', formula: '(((□∀x(Vx↔∃yIyx))↔¬(◇∃x(Vx∧¬∃yIyx)))→□((□∀x(Vx↔∃yIyx))↔¬(◇∃x(Vx∧¬∃yIyx))))' },
    { label: 'logmod18', formula: '(□(p↔□p)→□p)↔(□(p→□p)→□p)  [seriality]' },
    { label: 'logmod19', formula: '◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇◇(◇□◇◇□◇p↔◇□◇□p)' },
    { label: 'logmod20', formula: '(□(□P∨□¬□P)→(□(□¬□P→P)→P))∧((□□(□¬□P→P)→P)→(□P∨□¬□P))  [reflexivity, transitivity]' },
    { label: 'logmod21', formula: '□(□(□A→□C)→□(□(□B→□C)→□(□(□A∨□B)→□C)))  [reflexivity, symmetry]' },
    { label: 'logmod22', formula: '◇∃x□Fx,∃x□Fx→□∃x□Fx,□(∃x□Fx→□∃x□Fx)→□(◇∃x□Fx→◇□∃x□Fx),◇□∃x□Fx→□∃x□Fx|=□∃x□Fx  [reflexivity, symmetry]' },
    { label: 'logmod23', formula: '□((□◇P∧(□◇Q∨□◇R))∨¬□((□◇P∧□◇Q)∨(□◇P∧□◇R)))  [symmetry]' },
    { label: 'logmod24', formula: '∀x∀y(((Py↔Rx)∨(Px↔Ry))→x=y),∀x(Px∧¬Px)→¬∀xPx,◇∃t(Pt→∀xPx)∧(∀t◇∃n(Pt↔(Pn→∃x¬Px)))|=□∃x¬Px' },
    { label: 'logmod25', formula: '(◇□□□a∧□◇◇◇(a∨¬a))→◇□◇□a' },
    { label: 'logmod26', formula: 'A,◇□A,◇□◇□A,◇□◇□◇□A,◇□◇□◇□◇□A|=□A  [reflexivity, symmetry]' },
    { label: 'logmod27', formula: 'A,◇□A,◇◇□□A,◇□◇□A,◇□◇□◇□A,◇□◇□◇□◇□A|=□A  [reflexivity]' },
    { label: 'logmod28', formula: '(□◇p→□p)→□◇(□◇p→□p)  [reflexivity, transitivity]' },
    { label: 'logmod29', formula: '((∃xGx↔□∃xGx)∧(∀x(Gx↔□Gx)→□∀x(Gx↔□Gx))∧◇∃xGx)↔∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod30', formula: '(□∃xGx↔□∃xGx)∧□∀x(Gx→□Gx)∧◇∃xGx↔□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod31', formula: '◇(◇¬A∧□◇□A)→(◇¬A∧□◇□A)  [transitivity, seriality]' },
    { label: 'logmod32', formula: '□◇□(□◇□(◇□A→A)→A)→◇□A  [reflexivity]' },
    { label: 'logmod33', formula: '(◇p→◇□p)→□◇(◇p→◇□p)  [reflexivity, transitivity]' },
    { label: 'logmod34', formula: '□∃xGx,□∀x(□Gx↔(Ox∧Sx∧Px)),□∀x∀y(□Gx→□∀x∀y(□Gy→y=x))|=∃x(□Gx→□∀x∀y(Ox↔Sx))  [reflexivity]' },
    { label: 'logmod35', formula: '□∃xGx,□∀x(□Gx↔(Ox∧Sx∧Px)),□∀x∀y(□Gx→□∀x∀y(□Gy→y=x))|=∃x(□Gx→□∀x∀y(Ox↔Sx))  [euclidity]' },
    { label: 'logmod36', formula: '□∃xGx→((∃xGx↔∃x(Gx↔x=x)↔□∀x(Gx→□Gx))∧◇∃xGx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod37', formula: '((∃xGx↔(∀x∃y(Gx↔y=y∧x=y)↔□∀x(Gx→□Gx)))∧◇∃xGx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod38', formula: '((∃xGx↔(∀x∀y(Gx↔y=y∧x=y)↔□∀x(Gx→□Gx)))∧◇∃xGx)→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod39', formula: '(∃xGx↔□((∃xGx∧∀xGx)↔□∀x(Gx→□Gx)))→∃xGx→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod40', formula: '(◇p→□(□(p↔◇r)↔□(q↔◇r)))↔(◇p→□(p↔◇q))  [universality]' },
    { label: 'logmod41', formula: '¬□□□□□□□□□□□□□□□□□□□□P→◇¬P' },
    { label: 'logmod42', formula: '□∃xGx→((∃xGx↔((∀x¬∃y(¬Gx→x=y)→∃xGx)→(∃xGx↔□∀x(Gx→□Gx))))∧◇∃xGx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod43', formula: '¬d=f,¬d=s,¬d=h,¬f=s,¬f=h,¬s=h,□¬∃xHxx,□¬Hdf,□¬Hds,□¬Hdh,□¬Hfd,□¬Hfs,□¬Hfh,□¬Hsd,□¬Hsf,□¬Hsh,□¬Hhd,□¬Hhf,□¬Hhs,□∀x(Hdx→(Hxf∨Hxs∨Hxh)),◇∃x(Hxd∧¬Hxf),◇∃x(Hxd∧¬Hxs),◇∃x(Hxd∧¬Hxh)|=¬□∃x(Hxd∧Hxf)∨¬□∃x(Hxd∧Hxs)∨¬□∃x(Hxd∧Hxh)' },
    { label: 'logmod44', formula: '(□((◇R∧(◇¬P∨□Q))→□(◇R∧(◇¬P∨□Q)))→(◇R∧(◇¬P∨□Q)))→(◇R∧(◇¬P∨□Q))  [reflexivity, transitivity]' },
    { label: 'logmod45', formula: '□∃xGx→(((∀x¬Gx↔¬∃x∃yx=y)↔(∃xGx↔□∀x(Gx→□Gx)))∧◇∃xGx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod46', formula: '(□◇p→◇□p)→□◇((□◇p→◇□p))  [reflexivity, transitivity]' },
    { label: 'logmod47', formula: '(◇□¬p∨□p)→□◇(◇□¬p∨□p)  [reflexivity, transitivity]' },
    { label: 'logmod48', formula: '◇□(p∧q)↔(◇□p∧◇□q)  [reflexivity]' },
    { label: 'logmod49', formula: '□(□(□P∨□Q)∧□¬(□P∧□Q))↔□(□P↔□¬□Q)  [reflexivity, transitivity]' },
    { label: 'logmod50', formula: '□□□p|=□□□□□□□□□p  [reflexivity]' },
    { label: 'logmod51', formula: '□∃xEx,∀x∀y∀z(□((Ex∧Ey)↔Ez)→x=y),∀x∀y¬□(Ex→¬Ey)|=□∀x∃y(¬Ex→(Ey∧¬□(Ex∨Ey)))' },
    { label: 'logmod52', formula: '∀x∀y∀z(□((Ex∧Ey)↔Ez)→x=y),∀x∀y¬□(Ex→¬Ey)|=∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y)' },
    { label: 'logmod53', formula: '¬a=b,□((Ea∧Eb)→Ec),◇¬(Ec→(Ea∧Eb)),∀z(□((Ea∧Eb)↔Ez)→a=b)|=∃x∃y□(Ex↔¬Ey)' },
    { label: 'logmod54', formula: '∃x∃y∃z¬(x=y∨y=z∨z=x),∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y∨y=z∨z=x)|=∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y)' },
    { label: 'logmod56', formula: '□(□p∨□q)↔(□p∨□q)  [transitivity, seriality]' },
    { label: 'logmod57', formula: '□◇p↔◇□◇p  [reflexivity, transitivity]' },
    { label: 'logmod58', formula: '(∃xGx↔∃z((Gz↔□∀y((Gz↔∃x□Py)∧z=y))))∧∀x(□Gx→□Px)∧◇∃xGx→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod59', formula: '◇□(◇g→g)↔□(◇g→g)  [reflexivity, symmetry]' },
    { label: 'logmod60', formula: '(((◇p∨◇¬p)→(□p∧□□q))↔((◇p∨◇¬p)→(□□p∧□q)))↔□((◇p∨◇¬p)→(□p∧□q))  [reflexivity, transitivity, seriality]' },
    { label: 'logmod61', formula: '((◇p∨◇¬p)→(□p→□□q))↔□((◇p∨◇¬p)→(□p→□q))  [reflexivity, transitivity, seriality]' },
    { label: 'logmod62', formula: '(◇□p→(□□p∧◇q))→(□p→◇(◇p→(□p∧◇q)))  [transitivity, seriality]' },
    { label: 'logmod63', formula: '(◇p→(□p→□(□q→(□q→□r))))→(□(□p∧(□p→(□p→□q)))→(□(□p∧(□p→(□p→□q)))→□r))  [transitivity, seriality]' },
    { label: 'logmod64', formula: '◇□p↔◇□◇□p  [reflexivity]' },
    { label: 'logmod65', formula: '(◇□◇(p∨¬p)→◇◇□(p∧¬p))→□(◇□◇(p∨¬p)→◇◇□(p∧¬p))' },
    { label: 'logmod66', formula: '(◇□(p∧¬p)∨□◇(p∧¬p))→□((◇□(p∧¬p)∨□◇(p∧¬p)))' },
    { label: 'logmod67', formula: '(□◇p→(◇□p∧p))→□◇(□◇p→(◇□p∧p))  [reflexivity, transitivity]' },
    { label: 'logmod68', formula: '□(A↔((□A∧¬□□A)∨(□¬A∧¬□□A)))→(□¬A∧¬□□¬A)  [seriality]' },
    { label: 'logmod69', formula: '∃U□(EU↔∃x(Ex∧◇¬Ex)),∀x(◇¬Ex→∃y□((Ey→Ex)∧◇¬(Ex→Ey)))|=∃x□Ex  [seriality]' },
    { label: 'logmod70', formula: '(□(□((□P∧(□P→□□P))→□(□P∧(□P→□□P)))→(□P∧(□P→□□P)))→(□P∧(□P→□□P)))→(□P→□□P)' },
    { label: 'logmod71', formula: '∀x∀y(□(Fd→□(Fx→Txy))→◇Txy),□(Fh→Thc(m))|=◇Thc(m)' },
    { label: 'logmod72', formula: '∀x∀y(□(Fd→□(Fx→Txy))→◇Txy),□(Fh→Thc(m))|=◇Thc(m)  [symmetry]' },
    { label: 'logmod73', formula: '◇◇◇◇(P∧Q∧R)↔(◇◇◇◇P∧◇◇◇◇Q∧◇◇◇◇R)' },
    { label: 'logmod74', formula: '(□∀x(◇Gx∧□Gx↔□Px)↔□∃xGx)→∀x(◇Gx→□Px)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod75', formula: '(∀x∀y(□Px→(□(Ex→¬Ey)→¬Py)))∧(∃xGx↔∀x(Gx↔Nx∧□Px))→∀x(◇Gx→Nx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod76', formula: '∀x∃y(Tx∧Wy∧Eyx)→((((◇∀y∃x(Tx∧Wy∧¬Eyx))∧∃x(Ix∧(Cx∨¬Cx)))→¬◇∃x∃y(Tx∧Wy∧Eyx))∧(∃x∃y(Tx∧Wy∧Eyx))∧(∃x¬∃y(Tx∧Wy∧Eyx)→¬◇∃x∃y(Tx∧Wy∧Eyx))∧(((◇∀y∃x(Tx∧Wy∧¬Eyx))∧∃x(¬Ix∧(Cx∨¬Cx)))→∃x¬∃y(Tx∧Wy∧Eyx)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod77', formula: '□◇p↔□◇□◇p' },
    { label: 'logmod78', formula: '(□(a∨b∨c)∧(□(a∨b)↔□c)∧(□(b∨c)↔□a)∧(□(a∨c)↔□b))→(□a∧□b∧□c)' },
    { label: 'logmod79', formula: '□(□p→□q)↔□(□p→q)  [reflexivity]' },
    { label: 'logmod80', formula: '(∀x(□Ax→□Lx)↔∀x¬◇(Ax→¬x=x))∧(∃x□Ax→∀x(□Ax→□Mx∧□Px))∧((∃x(Ax∧□Mx)→□∃xPx))→∀x(Ax→□Mx)→∀x(Ax→□Px)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'logmod81', formula: '◇◇◇◇◇p∨(q∧r)→((p∨q)∧(p∨r))↔p∧q→∀x(p∨q)' },
    { label: 'log1', formula: '∀x((∃x(Pxa→∀yRy))∧∀y∃zQxyz)↔∀x∃b∀y((Pba→Ry)∧Qxyf(x,y))' },
    { label: 'log2', formula: '∀x∀y(∀z(S(x,z)↔S(y,z))↔E(x,y))↔∀x∀y∀z((S(x,z)↔S(y,z))↔E(x,y))' },
    { label: 'log3', formula: '∀x∃y(y=f(x)∧∀z(f(z)=y→z=x))↔∀x∃y(x=f(y)∧∀z(f(z)=y→z=x))' },
    { label: 'log4', formula: '(∀x∃y(y=f(x)∧∀z(f(z)=y→z=x)))↔(∀x∃y(x=f(y)∧∀z(f(z)=y→z=x)))' },
    { label: 'log5', formula: '∀x∀y∀z(Kyzx↔□(Rx→(◇Ay∧□(Ay→◇Az)))),∀x∀y(Eyx↔∃z(Kyzx∨Kzyx)),∀x(Sx↔∃yEyx),∀x(Sx→∀y(y=f(x)↔(Eyx∧¬∃zKyzx))),∀x(Sx→∀y(y=i(x)↔(Eyx∧¬∃zKzyx))),∀x(Sx→□(Rx→¬◇◇Ai(x))),∀x¬∃yKyyx,∀x∀y(Exy↔□Exy)|=∀x(Sx→¬∃yExy)' },
    { label: 'log6', formula: '∀a∀b(Tab↔(a=b∧∀x(Lxa↔Fx)))|=∀y(D=y↔((∀x(Lxy↔Fx)∧Sy)∨(y=e∧¬∃B∀x(LxB↔Fx))))→∀y(D=y↔((∃B(B=y∧TBy)∧Sy)∨(y=e∧¬∃BTBy)))' },
    { label: 'log7', formula: '∀x(Ix↔Cxi),∀x∀y∃z∃w(Cxy→Gz∧Gw∧Szx∧Swy∧z=w),∀x∃y(Ix→(Gy∧Syx)),¬∃x∀y(Gx∧Iy∧Sxy),∀x(Gx→Ix),¬∃x∃y(Sxy∧Syx)|=¬∃x∃y(Gx∧Iy∧Sxy)' },
    { label: 'log8', formula: '∃a∃b∃c¬(a=b∨b=c∨a=c)→(∃y∀x(Fx↔x=y)↔(∀y(∀x(Fx↔x=y)→Gy)→∃y(∀x(Fx∧Gx↔x=y))))' },
    { label: 'log9', formula: '((∀x(Lxm↔Fx))∨(m=e∧¬∃C∀x(LxC↔Fx)))↔((∀x(Lxm↔Fx)∧m=e)∨(∀x(Lxm↔Fx)∧∃xLxm)∨(m=e∧¬∃C∀x(LxC↔Fx)))' },
    { label: 'log10', formula: '∀x∀y∃z(Uxy↔¬Sxz∧Bzy)↔∀x∀y(Uxy↔∃z(¬Sxz∧Bzy))' },
    { label: 'log11', formula: '∀y(m=y↔¬(∀x(Lxy↔Fx)∧∃zLzy)→((∀x(Lxy↔Fx)∨¬∃C∀x(LxC↔Fx))∧y=e))|=∀y(m=y↔¬(∀x(Lxy↔Fx)∧∃zLzy)→(y=e))' },
    { label: 'log12', formula: '∀C((C=e∨∃zLzC)→¬∀x(LxC↔Fx))↔∀C¬(∀x(LxC↔Fx)∧C=0)∧∀C¬(∀x(LxC↔Fx)∧∃zLzC)' },
    { label: 'log13', formula: '∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))↔∀A∃B∀x(LxB→LxA∧(x=m∨x=n))∧∀A∃B∀x(LxA∧(x=m∨x=n)→LxB)' },
    { label: 'log15', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀z(Aza↔(∀u(Auz→Auc)∧∃y(Ayc∧∀u(Auc→(Af(uy)r↔Auz))))),∀x(Axc→Af(xx)r),∀x∀y(Axc∧Ayc→(Af(xy)r→Af(yx)r)),∀x∀y∀z(Axc∧Ayc∧Azc→(Af(xy)r∧Af(yz)r→Af(xz)r)),∀x(Axd↔∃z(Axz∧Aza)),∀x¬Axq,¬q=c,∀x(Axc)|=d=c' },
    { label: 'log16', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀x∀y(Af(xy)r↔∃z(Aza∧Axz∧Ayz)),∀x∀y(Af(xy)s↔∃z(Azb∧Axz∧Ayz)),∀x∀y(Pxy↔∀z(Azx→Azy)),∀x(Axd↔∃z(Axz∧Aza)),Prs,Aga|=∃c(Pcb∧g=d)' },
    { label: 'log17', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀x∀y(Af(xy)r(a)↔∃z(Aza∧Axz∧Ayz)),∀x∀y(Af(xy)r(b)↔∃z(Azb∧Axz∧Ayz)),∀x∀y(Pxy↔∀z(Azx→Azy)),∀x∀y(Axs(y)↔∃z(Axz∧Azy)),∀z(Azr(a)→∃x∃y(z=f(xy))),∀z(Azr(b)→∃x∃y(z=f(xy))),∀z(Azr(a)→Azr(b))|=∀y(Aya→∃z(∀u(Auz→Aub)∧y=s(z)))' },
    { label: 'log18', formula: '∀a∃b∀z(Azb↔Aza),Arm→∀x(Axc→Af(x,x)r)∧∀x∀y(Axc∧Ayc→(Af(x,y)r→Af(y,x)r)∧∀x∀y∀z((Axc∧(Ayc∧Azc))→((Af(x,y)r∧Af(y,z)r)→Af(x,z)r))),∀z(Azm→∃x∃y(z=f(xy))),Arm|=∀x(Axc→Af(x,x)r)∧(∀x∀y((Axc∧Ayc)→(Af(x,y)r→Af(y,x)r))∧∀x∀y∀z((Axc∧(Ayc∧Azc))→((Af(x,y)r∧Af(y,z)r)→Af(x,z)r)))∧∀x(Axm→∀z(Azx→Azr))' },
    { label: 'log19', formula: '∀a∀b∀C∃D∀x(LxD↔LxC∧(x=a∨x=b))|=∀x(LxA→∃X(∀y(LyX↔LyA∨LyB)∧LxX))' },
    { label: 'log20', formula: '∀a∀b∀x((Lxs(a)∨Lxs(b))↔(x=a∨x=b))↔∀a∀b∀x((∃X(LXs(a)∧LxX)∨∃X(LXs(b)∧LxX))↔(x=a∨x=b))' },
    { label: 'log21', formula: '∀a∀b∀x(∃X((∀y(LyX↔Lys(a))∨∀y(LyX↔Lys(b)))∧LxX)→x=a∨x=b)↔∀a∀b∀x(∃X((∀y(LyX↔y=a)∨∀y(LyX↔y=b))∧LxX)→x=a∨x=b)' },
    { label: 'log22', formula: '∃B∀x(Lxd∨Lxe→LxB)∧∃B∀x(Lxd∨Lxf→LxB)∧∃B∀x(Lxe∨Lxf→LxB)→∃B∀x(Lxd∨Lxe∨Lxf→LxB)' },
    { label: 'log23', formula: '∀m∀n∃p(Lmp∧Lnp)|=∀x(LxR→∃a∃bFxa)→∃A∀x(LxR→∃a∃b(LaA∧LbA∧Fxa))' },
    { label: 'log24', formula: '∀x∀y∀z∀w(Tc(x,c(y,x))∧Tc(c(n(z),n(w)),c(w,z))∧Tc(c(t,c(u,v)),c(c(t,u),c(t,v)))),∀x∀y((Tx∧Tc(x,y))→Ty)|=Tc(b,c(a,a))' },
    { label: 'log25', formula: '¬(¬∃wLwT∧¬∃C∀x(LxC↔∃X((X=A∨X=B)∧LxX))∧∀M∀N(∀z(LzM↔LzN)↔M=N))' },
    { label: 'log26', formula: '∀a(Aaz↔Aaf(xy))↔∀a(Aaz↔Aaf(uv))|=∀a(Aaf(xy)↔Aaf(uv))' },
    { label: 'log27', formula: '∀A∀x(Fx↔∀B(LBA→LxB))|=∀C(∃yLyC→∃V∀x(Fx↔LxV))' },
    { label: 'log28', formula: '(∀x(LxT↔Fx)∧ST)∨(ET∧¬∃B∀x(LxB↔Fx)),∀x(Fx↔∃X(LXC∧LxX)),∃u∀x(∃X(LXC∧LxX)→Lxu)|=∀x(Fx→LxT)' },
    { label: 'log29', formula: '(ET∧¬∃B∀x(LxB↔Fx)),∀x(∃X(LXC∧LxX)↔Fx)|=∃u∀x(∃X(LXC∧LxX)→Lxu)→∀x(Fx→LxT)' },
    { label: 'log30', formula: '∀m∀n∃p∀x(x=m∨x=n→Lxp),∃U∀x(∃X(LXC∧LxX)→LxU),∀y∀x(Lyt(x)↔LyA∨Lyx)|=∃u∀y∀Y(y=t(Y)→Lyu)' },
    { label: 'log31', formula: '∀m∀n∃p∀x(x=m∨x=n→Lxp),∃U∀x(∃X(LXC∧LxX)→LxU),∀y∀x(Lyt(x)↔LyA∨Lyx)|=∀x(LxC→∃u∀y∀x(y=t(x)→Lyu))' },
    { label: 'log32', formula: '∀m∀n∃P(LmP∧LnP)|=∀C∃B∀X(LXC→Lt(X)B)' },
    { label: 'log33', formula: '∃E∀T∃D∀y((∀v(Lvy→LvE)→LyT)→(∀x∀Y(LYm(x)↔Y=x∧¬LYB)→Lm(y)D))' },
    { label: 'log34', formula: '∃x∀y∃z((Lxm(z)↔x=z∧¬Lxb)→∀r(∀t(Ltm(r)→Ltx)∨Lm(r)y))' },
    { label: 'log35', formula: '∀E∀Y(LEm(Y)↔E=Y∧¬LEB)|=∃E∀T∀w(∀x(Lxm(w)→LxE)∨(∃z(z=m(w)∧LzT)))' },
    { label: 'log36', formula: '∀y∃x∀x1∀y1(((¬Rx1↔Wy)↔x1=x)∧((¬Rx↔Wy1)↔y1=y))↔∃x∀x1∀y1∀y(((¬Rx1↔Wy)↔x1=x)∧((¬Rx↔Wy1)↔y1=y))' },
    { label: 'log37', formula: '|=∃X((X=A∨∀y(LyX↔∃Y(LYC∧LyY)))∧LxX)↔LxA∨∃X(LXC∧LxX)' },
    { label: 'log39', formula: '¬(∃x∀yFxy∧∃x∀y¬Fxy∧∀x(∃y(∃zFyz∧∃z¬Fyz∧Fyx)∧∃y(∃zFyz∧∃z¬Fyz∧¬Fyx)))' },
    { label: 'log40', formula: 'LYA|=∃X(∃x(∃a∃b(∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b))∧LaA∧LbB)∧LXx)∧LYX)' },
    { label: 'log41', formula: '∀A∀B∀x(Lxd(A,B)↔∃a∃b(LaB∧LbB∧x=o(a,b))),d(S,T)=d(T,S)|=∀r(LrS↔LrT)' },
    { label: 'log42', formula: '∀m∀n(∀x(Lxm↔Lxn)→m=n),∀M∀N∀z(Lzu(M,N)↔LzM∨LzN)|=LAX∧LBX→∃Y(Y=u(A,B)∧LYX)' },
    { label: 'log43', formula: '∀x(Lxd(A,B)↔∃a∃b(LaA∧LbB∧x=o(a,b))),∀x(Lxd(B,A)↔∃a∃b(LaA∧LbB∧x=o(a,b))),∀x(Lxd(A,B)↔Lxd(B,A))|=∀x(∃a∃b(LaA∧LbB∧x=o(a,b))↔∃a∃b(LaA∧LbB∧x=o(b,a)))' },
    { label: 'log44', formula: '((∃x)¬x=a∧(∃x)(∃y)¬x=y∧(∃x)(¬x=a∧(Fx→Fa))∧¬(∃x)(∃y)(¬x=y∧(Fx∧Fy)))↔((∃x)¬x=a∧(∀x)(Fx→x=a))' },
    { label: 'log45', formula: '∀x(LxC→∃A∃B∀z(Lzx↔∃a∃b(z=o(a,b)∧LaA∧LbB))),∀X(LXC→LyX),∃wLwC|=∃M∃N∀z(Lzy↔∃a∃b(z=o(a,b)∧LaM∧LbN))' },
    { label: 'log46', formula: '∀x(LxC→∃A∃B∀z(Lzx↔∃a∃b(z=o(a,b)∧LaA∧LbB)))|=∃M∃N∀w(∃m∃n(w=o(m,n)∧LmM∧LnN)→∀X(LXD→LwX)∧∃rLrD)' },
    { label: 'log47', formula: '(∀x)(Fx→x=a)↔(Fa↔((∃x)Fx∧¬(∃x)(∃y)(¬x=y∧(Fx∧Fy))))' },
    { label: 'log48', formula: '∀X∀Y∀w(Lwd(X,Y)↔∃m∃n(LmX∧LnY∧w=o(m,n))),∃aLaA,∃bLbB,∃cLcM,∃eLeN|=∀y(Lyd(A,B)↔Lyd(M,N))→∀y(Lyd(B,A)↔Lyd(N,M))' },
    { label: 'log49', formula: '∃a∃b(∀m(∀z(Lzm↔z=a)→Lmx)∧∀m(∀z(Lzm↔z=a∨z=b)→Lmx)∧∀m(Lmx→∀z(Lzm↔z=a)∨∀z(Lzm↔z=a∨z=b)))' },
    { label: 'log50', formula: '∀x∀yTi(n(i(x,x)),y),∀x∀y(Cx→Ti(x,i(y,x))),(C(0)∧∀y(C(y)→C(s(y)))),∀x∀yC(i(x,y)),∀x∀y∀zTi(i(x,i(y,z)),i(i(x,y),i(x,z))),∀x∀y∀zTi(i(i(x,y),z),i(n(z),n(y))),∀x∀yTi(i(n(i(x,y)),y),i(x,y)),∀x∀y(Tx→(Ti(x,y)→Ty))|=(Ta→Tb)→Ti(a,b)' },
    { label: 'log51', formula: '∃wWw,∀x(Wx→¬Px),∀x(Wx→Pf(x)),∀w∀u((Ww∧Wu)→(Vf(w)w∧(Vf(w)u→u=w))),∀w(Ww→VTw),∀x∀y(Vxy→(Px∧Wy)),∀X(X=T↔(∃w(Ww∧VZw)∧∃w(Ww∧(VZw↔¬VXw))∧∀w(Ww→(VZw→VXw))))|=∀w(Ww→VZw)' },
    { label: 'log52', formula: '∀x∀y((Lo(x,y)R→Lo(y,x)R))↔(∃x(x=o(a,a)∧∃m∃n(x=o(m,n)∧Lo(m,n)R))↔∃x(x=o(a,a)∧∃m∃n(x=o(m,n)∧Lo(n,m)R)))' },
    { label: 'log53', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X∀x(Lxt(X)↔LxA∧LxX),∀n∃u∀x(LxA∨Lxn→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzX→Lzu)))' },
    { label: 'log54', formula: '∃y∀x(Axy↔∀z(Azx↔Pz)∨∀z(Azx↔Qz)),∃y∀x(Axy↔Px),∃y∀x(Axy↔Qx)|=∃y∀x(Axy↔Px∨Qx)' },
    { label: 'log55', formula: '¬∃x¬∃y(Tx∧Wy∧Eyx)∧¬∀y∃x(Tx∧Wy∧¬Eyx)∧∀x∃y(Tx∧Wy∧Eyx)→∃y∀x(Tx∧Wy∧Eyx)' },
    { label: 'log56', formula: '∀x(Ix↔∃z∃y(Bzy∧¬Sxz))↔∀x∃z∃y(Ix↔Bzy∧¬Sxz)' },
    { label: 'log57', formula: '∀y(¬(∀x(Lxy↔Fx)∧∃zLzy)→((∀x(Lxy↔Fx)∧y=e)∨(y=e∧¬∃C∀x(LxC↔Fx)))↔m=y),∀y¬(∀x(Lxy↔Fx)∧∃zLzy)|=∀ym=y' },
    { label: 'log58', formula: '∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))↔∀A∃B∀x(LxB→LxA∧(x=m∨x=n))∧∀A∃B∀x(LxA∧(x=m∨x=n)→LxB)' },
    { label: 'log59', formula: '∃B∀x(LxB↔Fx)↔(∃B∀x(LxB→Fx)∧∃B∀x(Fx→LxB))' },
    { label: 'log60', formula: '∃A∃B∀x(LxB↔∃y(LyA∧Lxy))' },
    { label: 'log61', formula: '∀x1∃x2∀x3(∃x4(Lx4x1∧Lx3x4)→Lx3x2)|=∀x1∃x2∀x3(∃x4(Lx4x1∧Lx3x4)↔Lx3x2)' },
    { label: 'log62', formula: '∀x1∃x2∀x3(∃x4(Lx4x1∧Lx3x4)↔Lx3x2)↔∀x1∃x2∀x3∀x4((Lx4x1∧Lx3x4)↔Lx3x2)' },
    { label: 'log63', formula: '∃B∀x(LxB↔LxU∧∃X(LXC∧LxX))→∃B∀x(LxB↔∃X(LXC∧LxX))' },
    { label: 'log64', formula: '∀f∀g∃h∀s(Fghsf↔Pf)↔∀f(∀g∃h∀sFghsf↔Pf)' },
    { label: 'log65', formula: '∃x∃y(Fxy∧Gxyz)→((∀x∀y((Fxy∧Gxyz)→(foo↔Hxy)))↔(foo↔(∀x∀y((Fxy∧Gxyz)→Hxy))))' },
    { label: 'log66', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀z(Aza→Azd),∀z(Azb→Azd),∀x(Axc↔∃z(Axz∧Aza)),∀x(Axc↔∃z(Axz∧Azb)),∀x∀y(Af(xy)r↔∃z(Aza∧Axz∧Ayz)),∀x∀y(Af(xy)s↔∃z(Azb∧Axz∧Ayz)),∀z¬Azp,¬Apa,¬Apb,r=s|=a=b' },
    { label: 'log67', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀x∀y(Af(xy)r↔∃z(Aza∧Axz∧Ayz)),∀x∀y(Af(xy)s↔∃z(Azb∧Axz∧Ayz)),∀x∀y(Pxy↔∀z(Azx→Azy)),∀x(Axd↔∃z(Axz∧Aza)),Prs|=∀y(Aya→∃c(Pcb∧y=d))' },
    { label: 'log69', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀x∀y(Af(xy)r(a)↔∃z(Aza∧Axz∧Ayz)),∀x∀y(Af(xy)r(b)↔∃z(Azb∧Axz∧Ayz)),∀x∀y(Pxy↔∀z(Azx→Azy)),∀x∀y(Axs(y)↔∃z(Axz∧Azy)),∀z(Azr(a)→∃x∃y(z=f(xy))),∀z(Azr(b)→∃x∃y(z=f(xy))),∀z(Azr(a)→Azr(b))|=∀y(Aya→∃z(∀u(Auz→Aub)∧y=s(z)))' },
    { label: 'log74', formula: 'Arm→(∀x(Axc→Af(x,x)r)∧(∀x∀y((Axc∧Ayc)→(Af(x,y)r→Af(y,x)r))∧∀x∀y∀z((Axc∧(Ayc∧Azc))→((Af(x,y)r∧Af(y,z)r)→Af(x,z)r)))),∀z(Azm→∃x∃y(z=f(xy))),∃xAxm|=∃u(∀x(Axc→Af(x,x)u)∧(∀x∀y((Axc∧Ayc)→(Af(x,y)u→Af(y,x)u))∧∀x∀y∀z((Axc∧(Ayc∧Azc))→((Af(x,y)u∧Af(y,z)u)→Af(x,z)u)))∧∀x(Axm→∀z(Azx→Axu)))' },
    { label: 'log83', formula: '∀x(¬P(x,x)∧(∃y(P(x,y)↔¬P(y,x)))),∀x∀y(((¬(x=y))∧P(x,y))→∃z(P(x,z)∧P(z,y)∧¬(x=z)∧¬(y=z)))|=∀x∀y∃z(P(x,z)∧P(y,z)∧∀t(P(x,t)∧P(y,t)→((t=z)∨P(z,t))))' },
    { label: 'log85', formula: '∀b∀y(p(a,b)=y↔∀x(Lxy↔x=a∨x=b)),(s(a)=p(a,a))|=((X=s(a)∨X=s(m))↔LXp(a,m))' },
    { label: 'log90', formula: '|=∀a∀b∀x(∃X((∀y(LyX↔y=a)∨∀y(LyX↔y=b))∧LxX)↔x=a∨x=b)↔∀a∀b∀x(∃X((∀y(LyX↔Lys(a))∨∀y(LyX↔Lys(b)))∧LxX)↔x=a∨x=b)' },
    { label: 'log93', formula: '((◇(¬∃xEx↔¬∃x¬Ex)↔∀x(x=x→◇¬∃xEx))→¬∀x∃y(x=y))∧(∀x(x=x→◇¬∃xEx)→◇(¬∃xEx↔¬∃x¬Ex))↔□∃xEx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log94', formula: '□□□□□□□□□◇□□□□□□□□□□(¬(□p→p)→□(p↔□p)→□p)' },
    { label: 'log95', formula: '□□□□□□□□□◇□□□□□◇□□□□□□□◇□□□(¬(□p→p)→□(p↔□p)→□p)' },
    { label: 'log96', formula: '□◇□□□□◇□□□(¬(□p→p)→□(p↔□p)→□p)' },
    { label: 'log97', formula: '□◇□□□□□◇□□□(¬(□p→p)→□(p↔□p)→□p)  [transitivity]' },
    { label: 'log102', formula: '((□P→□□P)∧(□P→◇□P))∧((□□P→□P)∧(◇□P→□P))  [reflexivity, transitivity]' },
    { label: 'log103', formula: '◇□(P↔Q)→((□P→◇□Q)∧(□Q→◇□P))  [reflexivity, symmetry]' },
    { label: 'log109', formula: '∃a∃b∀B∀x((Lxa∨Lxb→LxB)→(Lxd∨Lxe∨Lxf→LxB))' },
    { label: 'log115', formula: '∃B3(∀B1∃B2∀x(LxB1∨Lxa2→LxB2)∧∀B2∃B3∀x(LxB2∨Lxa3→LxB3)→∀x(Lxb1∨Lxb2∨Lxb3→LxB3))' },
    { label: 'log116', formula: '∃B3(∃B2∀x(LxB1∨Lxa2→LxB2)∧∀B2∃B3∀x(LxB2∨Lxa3→LxB3)→∀x(Lxb1∨Lxb2∨Lxb3→LxB3))' },
    { label: 'log120', formula: '∀a∀b∃u∀x(x=a∨x=b→Lxu)→∀U0∃U1∀x(x=a1∨x=b1→LxU1)∧∀U1∃U2∀x(x=U1∨Lxb2→LxU2)' },
    { label: 'log128', formula: '∀a∀b∃P∀x(x=a∨x=b→LxP)|=∃U∀x(LxA∨LxB∨LxC→LxU)→∃T∀x(x=A∨x=B∨x=C→LxT)' },
    { label: 'log129', formula: '∃U∃U2(∀x(LxA∨LxB→LxU)∧∀x(LxU∨LxC→LxU2)),∀m∀n∃P∀x(x=m∨x=n→LxP)|=∃T∀x(x=A∨x=B∨x=C→LxT)' },
    { label: 'log132', formula: '□(□(P↔Q)↔R)↔□(P↔□(Q↔R))  [reflexivity, transitivity]' },
    { label: 'log144', formula: '∀A∀B(A=B↔∀x(LxA↔LxB))|=∀x(∀X((∀y(LyX↔y=a)→LxX)∧(∀y(LyX↔y=a∨y=c)→LxX))↔x=a)' },
    { label: 'log157', formula: '(∀xFx→∀x(Gx↔Hx))↔(∀xFx→(∀xGx↔∀xHx))' },
    { label: 'log161', formula: '|=□(□((□A∨□B)→C)↔(□□(A→C)∧□□(B→C)))  [reflexivity, transitivity]' },
    { label: 'log168', formula: '∃F∀x∀a∀b((LaA∧LbB→LxF)∨(∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b))→LxF))' },
    { label: 'log169', formula: '((LaA∧LbB∧∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b)))→∀y(Lyx→∀z(Lzy→LyA∨LyB)))' },
    { label: 'log170', formula: '∀y(f(ya)=f(ay)),∀x∀y∀z(f(f(xy),z)=f(x,f(yz)))|=f(n,f(ai))=f(f(ai),n)' },
    { label: 'log171', formula: '□((□◇P∧(□◇Q∨□◇R))→□((□◇P∧□◇Q)∨(□◇P∧□◇R)))  [symmetry]' },
    { label: 'log172', formula: '(∀x∀y(f(x)=f(y)→x=y))∧(∀y∃x(f(x)=y)→∀y∃x((f(x)=y)∧∀z(¬(z=x)→¬(f(z)=y))))' },
    { label: 'log173', formula: '∀Y(∃X(∀x(LxY→LxX)∧∀A∀B∀x(LxX↔∃a∃b(LaA∧LbB∧x=o(a,b))))↔∀x(LxY→∃a∃bx=o(a,b)))' },
    { label: 'log174', formula: '∀E∃T∀X(LXT→∀x(LxX→LxE))|=∀Y(∀x(LxY→∃a∃bx=o(a,b))→∃X(∀x(LxY→LxX)∧∀A∀B∀x(LxX↔∃a∃b(LaA∧LbB∧x=o(a,b)))))' },
    { label: 'log179', formula: '∃A∃B∃C∀x(∃a∃b(LaA∧LbB∧xo=(a,b))→LxC)→∃A∃C∀x(∃a∃b(LaA∧LbA∧xo=(a,b))→LxC)' },
    { label: 'log180', formula: '(◇□□□a∧□◇□◇(a∨¬a))→◇□◇□a' },
    { label: 'log181', formula: '(◇□□□a∧◇□◇□(a∨¬a))→◇□◇□a' },
    { label: 'log182', formula: '(◇□□□a∧□◇◇◇(a∨¬a))→◇□◇□a' },
    { label: 'log191', formula: '∀x∀y∀z∀w∀x∀y∀z∀rI(I(x,I(I(y,z),r)),I(I(y,z),I(x,r)))=1,I(I(p,q),I(p,q))=1,∀x∀y∀zI(I(I(x,y),z),I(N(z),N(y)))=1,∀x∀y((x=1∧I(x,y)=1)→y=1)|=I(I(p,q),I(N(q),N(p)))=1' },
    { label: 'log192', formula: '∀p∀q(c(p,q)=1↔(((p=1↔(P∨¬P))∧(q=1↔(P∨¬P)))))|=c(a,a)=1' },
    { label: 'log206', formula: '(∀x∀y∀e((Eex→Eey)↔x=y))↔(∀x∀y∀e((Eex↔Eey)↔x=y))' },
    { label: 'log207', formula: '∀x∃o∃a∃b∃c∃y∀e∃p∀q∀n((Eox∧¬Eno)∨(Eax∧Ebx∧Eca∧Ecb∧¬(a=b))∨(Eex→((¬Eqe∧Epe∧Epy)∨(¬Eqy∧Epe∧Epy)∨(p=q∧Epe∧Epy))))' },
    { label: 'log209', formula: '∀x∀y∀z((Czy∧Cyx)→¬Cxz),∀x∀y(Cyx→¬Cxy),∀x(Px→∃y(¬x=y∧Cyx)),∀y(∃x(¬x=y∧Cyx)→∃z(¬y=z∧Czy)),∃xPx|=¬∃xPx' },
    { label: 'log219', formula: '(∀x∀y(Rxy→∃z(Rxz∧Rzy∧¬Rzx∧¬Ryz))∧∃x∃yRxy)→∃x∀y¬Rxy' },
    { label: 'log229', formula: '∀m∀n∃p∀x(x=m∨x=n→Lxp),∃U∀x(∃X(LXC∧LxX)→LxU)|=∀m∀n∃u∀x(Lxm∨Lxn→Lxu)' },
    { label: 'log231', formula: '∀Y∃u∀y(y=t(Y)→Lyu),∀u∃D∀x(x=u→LxD),∀D∃U∀x(∃X(LXD∧LxX)→LxU)|=∃B∀x(LxC→Lt(x)B)' },
    { label: 'log233', formula: '∀n∃p∀x(x=A∨x=n→Lxp),∀p∃U∀x(∃X(LXp∧LxX)→LxU),∀y∀x(Lyt(x)↔LyA∨Lyx)|=∀Y∃u(∀y(y=t(Y)→Lyu)∧∀z(LzY→Lzu))' },
    { label: 'log238', formula: '¬f=s,¬f=h,¬s=h,¬(∃x)(Pxx),(∃x)(Ex∧Pxg∧Pfx),(∃x)(Ex∧Pxg∧Psx),(∃x)(Ex∧Pxg∧Phx),(∃u)(∀v)((∃w)(Ew∧Pwg∧Puw)∧((∃x)(Ex∧Pxg∧Pvx)→(∃y)(∀z)((Ey∧Pyg∧(Puy∨Pvy))∧((Ez∧Pzg∧(Puz∨Pvz))→y=z))))|=A∧¬A' },
    { label: 'log243', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X∀x(Lxt(X)↔LxA∨LxX),∀m∀n∃u∀x(LxA∨Lxn→Lxu)|=∀X(∃u(Lt(X)u∧∀x(LxX→Lxu)))' },
    { label: 'log244', formula: '∀X∃u∀x(x=A∨x=X→Lxu),∀X∀x(Lxt(X)↔LxA∨LxX)|=∀X∃u∀x(LxA∨LxX→Lxu)→∀X(∃u(Lt(X)u∧∀x(LxX→Lxu)))' },
    { label: 'log245', formula: '(∀x(Gx→□Gx))∧((∃xGx↔□∃xGx)→□(∃xGx→□∃xGx))∧◇∃xGx↔□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log252', formula: '∀y(t=y↔(∀x(Lxy↔Fx)∧Sy)∨(Ey∧¬∃B∀x(LxB↔Fx)))|=¬∃B∀x(LxB↔Fx)→∀y((Ey∧¬∃B∀x(LxB↔Fx)))' },
    { label: 'log262', formula: '∃E∀T∀y∃x((∀v(Lvm(y)→LvE)→Lm(y)T)→∃Y((LYm(x)↔Y=x∧¬LYB)→Lm(y)T))' },
    { label: 'log263', formula: '∃E∀T∀y∃x(¬Lm(y)T→(¬∀v(Lvm(y)→LvE)→¬(LEm(x)↔E=x∧¬LEB)))' },
    { label: 'log264', formula: '∀y∃x((Ax→By)∧¬∃z((Az→By)∧¬x=z))↔∃x(Ax→∀y(By∧¬∃z(Az→By∧¬x=z)))' },
    { label: 'log272', formula: '∀x∀y(Lym(x)↔y=x∧¬Lya),∀x∃y∀z(∀r(Lrz→Lry)→Lzy)|=∃x∀yLm(y)x' },
    { label: 'log273', formula: '∃E∀T∃Y∀w((LEm(Y)↔E=Y∧¬LEB)→∀x(Lxm(w)→LxE)∨Lm(w)E)' },
    { label: 'log275', formula: '∃x∀y(∀z(Lxm(z)↔x=z∧¬Lxb)→∀r(∀t(Ltm(r)→Ltx)∨Lm(r)y))' },
    { label: 'log276', formula: '∀x∀y(Gx→□Gy↔(x=y))∧◇∃xGx→□∀xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log382', formula: '□∃xGx,□∀x(□Gx↔(Ox∧Sx∧Px)),□∀x∀y(□Gx→□∀x∀y(□Gy→y=x))|=∃x(□Gx→□∀x∀y(Ox↔Sx))  [reflexivity]' },
    { label: 'log277', formula: '∀E∀Y(LEm(Y)↔E=Y∧¬LEB)→∃E∀w∀x(Lxm(w)→LxE)' },
    { label: 'log278', formula: '∃E∀w(∀Y(LEm(Y)↔E=Y∧¬LEB)→∀x(Lxm(w)→LxE))' },
    { label: 'log284', formula: '¬(◇∀xPx→□∃xQx)↔∀x(◇Px∧◇¬Qx)' },
    { label: 'log285', formula: '∀y(∃x(∀x1((Ax1→By)→x1=x)))↔∃x(∀x1((Ax1→∀yBy)→x1=x))' },
    { label: 'log286', formula: '∀y∃x∀x1((Ax1→By)→x1=x)↔∃x∀x1((Ax1→∀yBy)→x1=x)' },
    { label: 'log308', formula: '((∃x)(∃y)(Rax∧Ray∧¬x=y∧¬(∃z)(Raz∧¬z=x∧¬z=y)∧(∃u)(Gau∧(u=x∨u=y)∧¬(∃w)(Gaw∧¬w=u)))∧¬(∃x)Bax∧(∀x)(Rax∨Gax∨Bax))↔((∃x)(∃y)(Rax∧Ray∧¬x=y∧¬(∃z)(Raz∧¬z=x∧¬z=y)∧(Gax∨Gay)∧¬(∃w)(Gaw∧¬w=x∧¬w=y))∧¬(∃x)Bax∧(∀x)(Rax∨Gax∨Bax))' },
    { label: 'log319', formula: '((∀x(Sx↔(x=x∧¬∃y(Ryx)↔∀y(◇(Rxy)→¬(x=y))))))∧◇∃xSx→□∃xSx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log328', formula: '(¬∃x¬∃y((◇((x=x∧Dy)↔□x=0)))→¬∀x∀y((x=x∧Dx)→x=0))∧◇∃xGx→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log329', formula: '(∃xGx↔□∀x(Gx↔x=x∧¬x=0))∧◇∃xGx→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log330', formula: '(∃xGx↔□∀x∃y(Gx∧Gy↔(x=y∧¬y=0)))∧◇∃xGx→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log331', formula: '∀m∀n(∀x(Lxm↔Lxn)→m=n),∀A∀x(Lxc(A)↔Lxe∧¬LxA)|=∀x(LxY↔Lxe∧¬LxX)↔∀x(LxX↔Lxe∧¬LxY)' },
    { label: 'log336', formula: '∀M∀N∃u∀z(LzM∨LzN→Lzu)|=LxA∨∃X(LXC∧LxX)→∃X((X=A∨∀y(LyX↔∃Y(LYC∧LyY)))∧LxX)' },
    { label: 'log341', formula: '∀m∀n∃u∀x(Lxm∨Lxn→Lxu),¬LzA|=∃X(LXC∧LzX)→∃Y(∀y(LyY↔∃Z(LZC∧LyZ))∧LzY)' },
    { label: 'log346', formula: '(∃xGx↔(◇(∀y∃z((Gy∧Gz↔y=z)))))↔◇∃xGx→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log347', formula: '(∃xGx↔((∀y∃z((Gy∨Gz↔y=z)))))∧◇∃xGx↔∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log348', formula: '(∃xGx↔□((∀z∃y(Gz↔(Gy→y=z)))∨(∃y∀z(Gy↔(Gz→y=z)))))→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log349', formula: '◇∀x∃y(Cxy)∧(◇∀x∃y(Cxy)→∀x∃y□(Cxy))↔∀x□∃y(Cxy)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log368', formula: '∀E∃T∀x(IxE→LxT)|=∀C∃B∀x(∃X(Ixy(X)∧It(X)x∧LXC)→LxB)' },
    { label: 'log369', formula: '∀E∃T∀x(IxE→LxT),∀M∀N(IMN↔∀x(LxM→LxN))|=∃T∀x(∃X(Ixt(X)∧It(X)x∧LXC)→LxT)' },
    { label: 'log374', formula: '□p↔□□p  [transitivity, seriality]' },
    { label: 'log383', formula: '□(P↔Q)→□(□P↔□Q)  [reflexivity, seriality]' },
    { label: 'log396', formula: '|=(∃a∃b(∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b))∧LaA∧LbB)∧LXx)→(∀y(Lyx→∀z(Lzy→LyA∨LyB))∧LXx)' },
    { label: 'log404', formula: '∀x∀z∃y(Rxy∧¬Rxx∧(Ryz→Rxz))→∀x∃y∀z(Rxy∧¬Rxx∧(Ryz→Rxz))' },
    { label: 'log407', formula: '((∃xGx↔∀x∀y((y=y∧□Gx)↔x=y))∧◇∃xGx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log411', formula: '((∃xGx↔(∀x∃y(Gx↔y=y∧x=y)→□∀x(Gx→□Gx)))∧◇∃xGx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log413', formula: '(((∃xGx↔∀x(Gx↔□(Gx→□Gx)∧x=y)))∧◇∃xGx)→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log414', formula: '(□∀x∀y(Gx↔y=y∧x=y)↔□∀x(Gx→□Gx))∧∃xGx→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log415', formula: '(∃xGx↔□∀x∃y(Gx↔y=y→x=y))∧◇∃xGx→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log416', formula: '(∃xGx↔□(∀x∀y((Gx↔y=y)↔□x=y)))∧◇∃xGx→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log417', formula: '((∃xGx↔∀x∀y(Gx↔(y=y)∧x=y))∧◇∃xGx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log418', formula: '∃B∀x(∃X(∀y(Lyx↔Lyt(X))∧LXC)→LxB),∀m∀n(∀x(Lxm↔Lxn)→m=n),∀X(Lt(X)D1↔LXC)↔∀x(LxD2↔∃X(∀y(Lyx↔Lyt(X))∧LXC))|=∀y(LyD1→LyD2)' },
    { label: 'log419', formula: '∀M∀z(t(M)=M),∀X(Lt(X)D1↔LXC)↔∀x(LxD2↔∃X(x=t(X)∧LXC))|=∀y(LyD1↔LyD2)' },
    { label: 'log421', formula: '∀C∀x(LxD2↔∃X(x=t(X)∧LXC))→∀C∀X(∃x(x=t(X)∧LxD1)↔LXC)' },
    { label: 'log427', formula: '∀a∀b(o(a,b)=o(b,a)↔a=b),∀x(Lxd(A,B)↔∃a∃b(LaA∧LbB∧x=o(a,b))),∀x(Lxd(B,A)↔∃a∃b(LaB∧LbA∧x=o(a,b))),∀x(∃a∃b(LaA∧LbB∧x=o(a,b))↔∃a∃b(LaB∧LbA∧x=o(a,b)))|=LzA→LzB' },
    { label: 'log428', formula: '∃a∃b(LaA∧LbB),∀a∀b(o(a,b)=o(b,a)↔a=b),∀x(Lxd(A,B)↔∃a∃b(LaA∧LbB∧x=o(a,b))),∀x(Lxd(B,A)↔∃a∃b(LaB∧LbA∧x=o(a,b))),∀x(∃a∃b(LaA∧LbB∧x=o(a,b))↔∃a∃b(LaB∧LbA∧x=o(a,b)))|=LzA→LzB' },
    { label: 'log437', formula: '∀x∀y∀zTi(i(y,z),i(x,i(y,z))),∀x∀y∀zTi(i(x,i(y,z)),i(i(x,y),i(x,z))),∀x∀yTi(n(i(x,x)),y),∀x∀y∀zTi(i(i(x,y),z),i(n(z),n(y))),∀x∀yTi(i(n(i(x,y)),y),i(x,y))|=Ti(a,a)' },
    { label: 'log445', formula: '(∃xGx↔∀y∀z(Gz↔Py∧y=z))∧◇∃xGx∧∀x((Gx∧□Gx)→Px)→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log446', formula: '(LXC→∃a∃b(LaA∧LbX∧x=o(a,b)))→(x=o(m,n)∧LmA∧∀Y(LYC→LnY))↔∀a∀b(LXC→(LaA∧LbX∧x=o(a,b)))→(x=o(m,n)∧LmA∧∀Y(LYC→LnY))' },
    { label: 'log451', formula: '∀M∀N∀w(Lwt(M,N)↔LwM∧LwN)|=∃a∃b(x=o(a,b)∧LaA∧Lbx1)∧∃a∃b(x=o(a,b)∧LaA∧Lbx2)→∃a∃b(x=o(a,b)∧LaA∧Lbt(x1,x2))' },
    { label: 'log455', formula: '∀X∀Y∀x(Lxd(X,Y)↔∃m∃n(LmX∧LnY∧x=o(m,n)))|=∃a∃b(y=o(a,b))' },
    { label: 'log456', formula: '∀X∀Y∀w(Lwd(X,Y)↔∃m∃n(LmX∧LnY∧w=o(m,n)))|=∀y(Lyd(A,B)↔Lyd(M,N))→∀y(Lyd(B,A)↔Lyd(N,M))' },
    { label: 'log460', formula: '¬□∀x(Q(x,d)→Q(x,p)),¬□∀x(Q(x,d)→Q(x,f)),¬□∀x(Q(x,d)→Q(x,s)),□∃x(Q(x,d)∧Q(x,p)),□∃x(Q(x,d)∧Q(x,f)),□∃x(Q(x,d)∧Q(x,s)),□∀x(Qxd→(Qxs∨Qxp∨Qxf)),□∀x(¬Qxs∨¬Qxp),□∀x(¬Qxs∨¬Qxf),□∀x(¬Qxf∨¬Qxp)|=(A∧¬A)  [universality]' },
    { label: 'log468', formula: '∀m∀n∃p∀w(w=m∨w=n→Lwp),∀X(LXC→∃a∃b(x=o(a,b)∧LaA∧LbX))∧∃XLXC|=∃a∃b(x=o(a,b)∧LaA∧∀X(LXC→LbX))' },
    { label: 'log469', formula: '∀A∀B∀x(Lxv(A,B)↔LxA∧LxB),∀X∀Y∀m∀n(Lo(m,n)d(X,Y)↔LmX∧LnY),∀A∀B∀C(d(A,v(B,C))=v(d(A,B),d(A,C)))|=∀A∀B∀C∃M((d(A,v(B,C))=v(d(A,B),M))∧M=v(B,C))' },
    { label: 'log472', formula: '(∃xLxA→∃x(LxA∧∀y(Lyx→¬LyA))),¬∃V∀xLxV,∀x¬Lxe,∀m∀n∃p∀x(x=m∨x=n→Lxp)|=¬LBB' },
    { label: 'log473', formula: '∃a∃b(∀m(∀z(Lzm↔z=a)→Lmx)∧∀m(∀z(Lzm↔z=a∨z=b)→Lmx)∧∀m(Lmx→∀z(Lzm↔z=a)∨∀z(Lzm↔z=a∨z=b)))' },
    { label: 'log487', formula: '∃x(∀X(LXx↔X=m∨X=n)∧LxR)↔∃X(LXR∧LmX)∧∃X(LXR∧LnX)' },
    { label: 'log491', formula: '◇∃x∃y∀z(Gx↔((∃yy=y↔□(Gz→□Gz))∧z=y))→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log505', formula: '∀x(x=a∨x=b∨x=c∨x=d),∀x¬(x=a∧x=b),∀x¬(x=a∧x=c),∀x¬(x=a∧x=d),∀x¬(x=b∧x=c),∀x¬(x=b∧x=d),∀x¬(x=c∧x=d),Fb,Fd,Ga,Gc,Ha,Hc,(Hb∨Gb)|=¬∀x(Fx→(Hx∨Gx))' },
    { label: 'log506', formula: '∀x∀y(∃z(z=x∧z=y)→(y=x∧∃w(w=x∧w=y)))|=∃x(∀y(x=y∨y=a))∧∃y(∀x(x=y∨x=b))' },
    { label: 'log510', formula: '¬n=1∧∀x∀y(m(x,y)=n→(x=1∨y=1))↔∀x∀y(m(x,y)=n→((x=1∨y=1)∧¬(x=1∧y=1)))' },
    { label: 'log521', formula: '∃x∀y((¬Rxx∨Rxy∨Ryx∨Ryy)∧(Rxx∨¬Rxy∨Ryx∨Ryy)∧(¬Rxx∨¬Rxy∨Ryx∨Ryy))' },
    { label: 'log528', formula: '(□◇A→◇□A)→□◇(◇A→□A)  [reflexivity, transitivity]' },
    { label: 'log535', formula: '(◇□(p∨◇p∨□p))→□◇(◇□(p∨◇p∨□p))  [reflexivity, transitivity]' },
    { label: 'log539', formula: '∃a(∀x(Lxq↔∀y(LyR→Lyd(A,A))∧LaA∧Lo(x,a)R)),∀M∀N∀m∀n(Lo(m,n)d(M,N)↔LmM∧LnN),∀m∀n∀x(Lxo(m,n)↔x=s(m)∨x=p(m,n)),∃xLxA,∀x(LxA→Lo(xx)R)|=∃xLxq' },
    { label: 'log548', formula: '∀x∀y∀zTi(i(x,y),i(z,i(x,y))),∀x∀y∀zTi(i(x,i(y,z)),i(i(x,y),i(x,z))),∀x∀y(Tx→(Ti(x,y)→Ty)),∀x∀y∀zTi(i(i(x,y),z),i(n(z),n(y))),∀x∀yTi(i(n(i(x,y)),y),i(x,y)),∀xTi(x,x),∀xTi(n(1),x)|=Ti(n(a),a)→Ts' },
    { label: 'log558', formula: '∃Y(Y=o(a,c)∧∀X(LXA→LYZ)∧NA)↔∃Y∀X(Y=o(a,c)∧(LXA→LYX)∧NA)' },
    { label: 'log559', formula: '∀x∀y∀z(□((Ex∨Ey)↔Ez)→x=y)|=∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y)  [euclidity]' },
    { label: 'log560', formula: '∀x∀y¬□(Ex↔¬Ey),∀x∀y∀z(□(Ez↔(Ex∧Ey))→x=y)|=∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y)  [universality]' },
    { label: 'log561', formula: '∀x∀y¬□(¬Ey→Ex),∀x∀y∀z(□(Ez↔(Ex∧Ey))→x=y)|=∀x∀y∀z(□((Ex∧Ey)→Ez)→x=y)' },
    { label: 'log570', formula: '∀M∀N∀x(∃m∃n(x=o(m,n)∧∃k(Lo(m,k)M∧Lo(k,n)N))→LxC(M,N)),∀x(x=o(f,g)∨x=o(g,e)∨x=o(h,f)∨x=o(i,g)∨x=o(j,h)→LxR)|=Lo(j,e)C(R,R)' },
    { label: 'log571', formula: '∀M∀N∀x(∃m∃n(x=o(m,n)∧∃k(Lo(m,k)M∧Lo(k,n)N))→LxC(M,N)),∀x(x=o(a,a)∨x=o(b,b)∨x=o(b,c)∨x=o(c,a)∨x=o(j,h)→LxR),∀x(x=o(a,a)∨x=o(b,b)∨x=o(c,b)∨x=o(a,c)∨x=o(j,h)→Lxt(R))|=Lo(a,b)C(R,t(R))' },
    { label: 'log573', formula: '∀M∀N∀x(∃m∃n(x=o(m,n)∧∃k(Lo(m,k)M∧Lo(k,n)N))→LxC(M,N)),∀x(x=o(c,e)∨x=o(d,b)∨x=o(f,b)∨x=o(f,d)∨x=o(g,c)∨x=o(g,e)→LxR)|=Lo(g,c)C(R,R)' },
    { label: 'log575', formula: '∀x∀y∀z(□((Ex∧Ey)↔Ez)→x=y),∀x∀y¬□(Ex↔¬Ey)|=¬∃x∃y∃z(¬x=y∧□(Ez↔(¬Ex∧¬Ey)))  [universality]' },
    { label: 'log576', formula: '∀x∀y∀z(□(Ez→(Ex∧Ey))→x=y)|=¬∃x∃y∃z(¬x=y∧¬y=z∧¬z=x)' },
    { label: 'log577', formula: '∃x(◇Ex∧◇¬Ex),∀x∀y◇(Ex↔Ey),□∀x∃y(¬Ex→Ey∧¬□(Ex∨Ey))|=∀x∀y(□(Ex→Ey)→¬□(Ey→Ex))  [euclidity]' },
    { label: 'log578', formula: '∃x(◇Ex∧◇¬Ex),∀x∀y◇(Ex↔Ey),□∀x∃y(¬Ex→Ey∧¬□(Ex∨Ey))|=0' },
    { label: 'log592', formula: '(□∀y∃x((□Px↔Gy)∧x=y)↔∃xGx)∧∀x(¬◇Gx→¬Px)∧∀x(□Gx→□Px)→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log595', formula: '∀x∀y◇(Ex↔Ey)|=∀x∀y∃z□((Ex∧Ey)↔Ez)  [universality]' },
    { label: 'log607', formula: '¬∀x¬∀y¬∀z(z=x∨z=y)↔∃x∃y∃z(¬z=x∧¬z=y)' },
    { label: 'log608', formula: '∃x∃y(Rx∧Sxy∧∀z(Rz∧Szy→z=x)∧∀i¬(i=x↔i=y))↔∃x∃y(Rx∧Sxy∧∀z¬(z=x↔z=y))' },
    { label: 'log617', formula: '∀x∀y(∀z(S(x,z)↔S(y,z))↔E(x,y))↔∀x∀y∀z((S(x,z)↔S(y,z))↔E(x,y))' },
    { label: 'log619', formula: '◇□g↔(□g)  [reflexivity, symmetry]' },
    { label: 'log620', formula: '∃x∃yFxy→(∀x(∃yFyx)∧∀x(∀y∀z((Fyx∧Fzx)→y=z)))↔∀x∀y(∃z(Fxz∧Fyz)→x=y)' },
    { label: 'log621', formula: '∀x∃y(x=f(y)∧∀z(f(z)=y→z=x))↔∀x∀y(f(x)=f(y)→x=y)' },
    { label: 'log622', formula: '∀x(Jx↔Jm(x)),∃xJx,∀x¬(x=m(x)),∀x¬(x=m(m(x)))|=∀xJx' },
    { label: 'log623', formula: '∀x(Jx↔∃y(Ayx∧Jy)),∃xJx,∀x∀y∃z(Azx∧Azy),∀x¬Axx|=∀xJx' },
    { label: 'log627', formula: '((◇(p∨q)∨◇¬(p∨q))→(□(p∨q)∧□r))↔(((◇p∨◇¬p)→(□p∧□r))∨((◇q∨◇¬q)→(□q∧□r)))  [transitivity, seriality]' },
    { label: 'log628', formula: '(((◇p∨◇¬p)→(□p∧□□q))↔((◇p∨◇¬p)→(□□p∧□q)))↔□((◇p∨◇¬p)→(□p∧□q))  [reflexivity, transitivity, seriality]' },
    { label: 'log631', formula: '(□p→□(□q→□r))↔(□(p∧□(□p→□q))→□r)  [reflexivity, transitivity, seriality]' },
    { label: 'log632', formula: '(□p→□(□q→□r))↔((□p∧□(□p→□q))→□r)  [reflexivity, transitivity, seriality]' },
    { label: 'log635', formula: '(◇p→(□p∧◇◇q))↔(◇p→□(◇p→(□p∧◇q)))  [transitivity, seriality]' },
    { label: 'log636', formula: '(◇p→(□p∧◇□q))↔(◇p→◇(◇p→(□p→□q)))  [transitivity, seriality]' },
    { label: 'log640', formula: '(□p→□(□q→□r))↔((□p∧□□q)→(□q→□r))  [reflexivity, transitivity, seriality]' },
    { label: 'log643', formula: '∀T∀k(LkF(T)↔∃nLo(k,n)T∨∃mLo(m,k)T),∀k(Lka→LkF(R)),∀m∀n(Lo(m,n)r→Lo(n,m)R)|=∀x(LxF(R)↔LxF(r))' },
    { label: 'log658', formula: '□□p↔□p  [transitivity, seriality]' },
    { label: 'log661', formula: '∀a∀b(Ta∧Ti(a,b)→Tb),∀a∀bTi(a,i(b,a)),∀a∀b∀cTi(i(a,i(b,c)),i(i(a,b),i(a,c))),∀a∀b∀cTi(i(a,i(b,c)),i(b,i(a,c))),∀a∀bTi(i(a,b),i(n(b),n(a))),∀aTi(n(n(a)),a),∀aTi(a,n(n(a)))|=Ti(x,y)↔(Tx→Ty)' },
    { label: 'log671', formula: '∀x∀y(S(y,x)↔(Lo(x,y)R∧∀z(Lo(x,z)R→y=z∨Lo(y,z)R))),∀X(X=o(a,b)→LXR),∀M∀N(o(M,N)=o(a,b)→M=a∧N=b)|=S(b,a)' },
    { label: 'log672', formula: '(S(b,a)↔(Lo(a,b)R∧∀z(Lo(a,z)R→b=z∨Lo(b,z)R))),∀X(X=o(a,b)→LXR),∀M∀N(o(M,N)=o(a,b)→M=a∧N=b)|=S(b,a)' },
    { label: 'log677', formula: '∀X(X=o(a,b)∨X=o(a,c)→LXR),∀M∀N(o(M,N)=o(b,c)→M=b∧N=c),∀M∀N(o(M,N)=o(a,c)→M=a∧N=c),∀M∀N(o(M,N)=o(a,b)→M=a∧N=b),¬b=c|=¬Lo(b,c)R' },
    { label: 'log684', formula: '(◇□p→(□□p→◇q))→(◇p→(□p→◇q))  [seriality]' },
    { label: 'log687', formula: '◇∃xEx,∀x¬∃y□(Ex↔¬Ey),∀x∀y□(Ef(x,y)↔Ex∧Ey),∀x∀y(□(Ex↔Ey)→x=y)|=∃x□Ex  [reflexivity]' },
    { label: 'log689', formula: '◇∀x□(◇Ex∧◇¬Ex)|=□∀x□(◇Ex∧◇¬Ex)  [reflexivity]' },
    { label: 'log690', formula: '◇∀x□(◇¬Ex)|=□∀x□(◇¬Ex)  [reflexivity]' },
    { label: 'log691', formula: '◇∀x□◇¬Ex|=□∀x□◇¬Ex  [reflexivity]' },
    { label: 'log693', formula: '∀x∀y◇(Ex↔Ey),∀x∀y(□(Ex↔Ey)→x=y),□∃xEx|=∃x□Ex  [reflexivity, euclidity]' },
    { label: 'log694', formula: '∀x∀y◇(Ex↔Ey),∀x∀y(□(Ex↔Ey)→x=y),□∃xEx|=∃x□Ex  [universality]' },
    { label: 'log702', formula: '∀y(LyA∧Lo(y,x)R↔y=a∨y=b)↔∀y(LyS↔y=a∨y=b)' },
    { label: 'log703', formula: '∀X1∀X2(∃X3(X3=X2)∧AX2→BX1)↔∀X1(∃X2∃X3(X=X2∧AX2)→BX1)' },
    { label: 'log707', formula: '□(□p∨□q)↔(□p∨□q)  [reflexivity, seriality]' },
    { label: 'log708', formula: '∃T(∀k(LkT↔k=a∨k=b∨k=c)∧∃x(LxT∧∀y(LyT→¬Lo(y,x)R))),∀x∀y(LxA∧LyA∧¬x=y→Lo(x,y)R∨Lo(y,x)R),Lo(a,b)R,Lo(b,c)R,¬a=c,¬Lo(a,c)R|=Lo(c,a)R' },
    { label: 'log709', formula: '◇p↔□◇p  [euclidity, seriality]' },
    { label: 'log717', formula: '□(a↔¬c∨□b)↔(((□(a→b)∧□(a→¬c))→□(b→¬c))↔(((□(a→b)∧□(b→¬c))→□(a→¬c))))' },
    { label: 'log718', formula: '(□(a∨(¬b))∨□(a∨(¬c))∨◇(a∧c)∨◇(a∧¬b))↔(((□(a→b)∧□(b→¬c))→□(a→¬c))→((□(a→b)∧□(a→¬c))→□(b→¬c)))' },
    { label: 'log719', formula: '□¬b∨□¬c∨◇(a∧((b∧¬c)∨c))∨◇(a∧c)↔(((□¬a∨◇(a∧¬b))∧(□¬a∨◇(a∧b))∧◇b∧□(b→c))→¬(◇c∧□(c→¬a)))' },
    { label: 'log720', formula: '∀y∃x◇□(px∧¬□py)↔◇□∀y∃x(px∧¬□py)  [reflexivity, symmetry, euclidity]' },
    { label: 'log729', formula: '¬1=2,¬1=3,¬1=4,¬1=5,¬1=6,¬1=7,¬1=8,¬1=9,¬2=3,¬2=4,¬2=5,¬2=6,¬2=7,¬2=8,¬2=9,¬3=4,¬3=5,¬3=6,¬3=7,¬3=8,¬3=9,¬4=5,¬4=6,¬4=7,¬4=8,¬4=9,¬5=6,¬5=7,¬5=8,¬5=9,¬6=7,¬6=8,¬6=9,¬7=8,¬7=9,¬8=9|=p' },
    { label: 'log733', formula: '∀x∀y□(Es(x,y)↔Ex∨Ey),∀x∀y(□(Ex↔Ey)→x=y),∀x(□Ex↔x=D),D=s(A,B),◇¬EA,◇¬EB|=_  [universality]' },
    { label: 'log735', formula: '((□∀x(Gx→(∃yx=y↔□Gx))))↔□(∃xGx→□∃xGx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log738', formula: '∃x∀y(Gy↔x=y)→(□(∃x∀y(Gy↔x=y)↔(□∃xGx∧□∀x(Gx→□Gx)))∧◇∃x∀y(Gy↔x=y))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log741', formula: '∀x∀y(∃a∃b(x=o(a,b)∧LaA∧LbB)∧∃a∃b(y=o(a,b)∧LaA∧LbB)→(Lo(x,y)R∧Lo(y,x)R→x=y))|=∀r∀t(∃a∃b(r=o(a,b)∧LaA∧LbB)∧∃a∃b(t=o(a,b)∧LaA∧LbB)→(Lo(r,t)R∧Lo(r,t)R→r=t))' },
    { label: 'log745', formula: '∃x□Rx∧(□∃x(Rx∧Gx)∨□∃x(Rx∧¬Gx))∧∀x(Gx→□(Rx∧Gx))∧◇(∃x¬Gx→◇∃x(Gx∧Rx))→□∃x(Rx∧Gx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log746', formula: '∀x∀y(Lyr1(x)↔Lo(x,y)R1),∀x∀y(Lyr2(x)↔Lo(x,y)R2),∀x∀y(Lyr1(x)↔Lyr2(x)),¬∀K(LKR1↔LKR2)|=¬∀K(LKR1→∃m∃nK=o(m,n))' },
    { label: 'log747', formula: '∀x∀y(Lyr1(x)↔Lo(x,y)R1),∀k(LkF(R1)↔∃bLo(k,b)R1∨∃aLo(a,k)R1),∀x∀y(Lo(x,y)R2↔r2(x)=r2(y)),∀B(∃x(B=r1(x)∧∃kLkB)↔∃y(B=r2(y)∧∃kLkB))|=Lo(m,n)R1→Lo(m,n)R2' },
    { label: 'log748', formula: '∀x∀y(Lyr1(x)↔Lo(x,y)R1),∀k(LkF(R1)↔∃bLo(k,b)R1∨∃aLo(a,k)R1),∀x∀y(Lo(x,y)R2↔r2(x)=r2(y)),∀x(LxF(R1)→Lo(x,x)R1),∀B(∃x(B=r1(x)∧∃kLkB)↔∃y(B=r2(y)∧∃kLkB))|=Lo(m,n)R1→Lo(m,n)R2' },
    { label: 'log751', formula: '∃x∃y∀u(Fu→(u=x∨u=y))' },
    { label: 'log752', formula: '(∀x(∀y(x=y↔Rxy)→∀y(x=y↔Cxy)))↔(∀x∀y((x=y↔Rxy)→(x=y↔Cxy)))' },
    { label: 'log757', formula: '(∃b(a=b∧∀w(Fw→∀cQwc))→Pa)↔∀b∀w((a=b∧∀c(Fw→Qwc))→Pa)' },
    { label: 'log759', formula: '((Tx→(f(x)=y↔Lo(x,y)F))∧(¬Tx→(f(x)=y↔y=0)))↔((Tx→(f(x)=y↔Lo(x,y)F))∧(¬Tx→f(x)=0))' },
    { label: 'log761', formula: '|=∀F∀y(f(x)=y↔((Tx∧Lo(x,y)F)∨(¬Tx∧y=0)))↔∀F∀y(f(x)=y↔((Tx∧Lo(x,y)F)∨(¬Tx∧f(x)=0)))' },
    { label: 'log774', formula: '∃x∀y((Ly↔y=x)∧Jx)↔∀y∃x((Ly↔y=x)∧Jx)' },
    { label: 'log775', formula: '∀a∀H∀K(l(a,H,K)↔∀b(LbK→Lo(a,b)H)),∀a∀H∀K(i(a,H,K)↔l(a,H,K)∧∀b(l(b,H,K)→Lo(b,a)H)),∀K∀H(L(K,H)→P(H,K)∧∀a∀b(LaK∧LbK→∃n(LnK∧s(n,H,p(a,b)))∧∃m(LmK∧i(m,H,p(a,b)))))|=L(A,R)→P(R,A)∧∀m∀n(LmA∧LnA→∃y(LyA∧(∀x(Lxp(m,n)→Lo(x,y)R)∧∀x(∀z(Lzp(m,n)→Lo(z,x)R)→Lo(x,y)R)))∧∃x(LxA∧(∀y(Lyp(m,n)→Lo(x,y)R)∧∀y(∀z(Lzp(m,n)→Lo(y,z)R)→Lo(x,y)R))))' },
    { label: 'log776', formula: '¬(∃a∃b∃c¬(a=b∨a=c∨b=c)∧∀x∀y∀z(((F(xz)↔F(yz))∧(F(zx)↔F(zy)))∨((z=x∨z=y)∧(F(xx)↔F(yy))∧(F(xy)↔F(yx))))∧¬∃x∃y(¬x=y∧∀z((F(xz)↔F(yz))∧(F(zx)↔F(zy)))))' },
    { label: 'log802', formula: '∀x(Hx→◇Dx),∀x◇((∃yMyx∨∃ySxxy∨Ax)↔◇Dx),∀x(Ix→(¬◇(Ax∨∃y(¬y=x∧Myx))∧∀z(Sxxz→z=p(x))))|=∀x((Ix∧Hx)→◇(Mxx∨∃y(y=p(x)∧Sxxy)))  [transitivity, seriality]' },
    { label: 'log807', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧M(x)∧x=o)),∃fH(f)∧∀f(H(f)→∀e∀x∀y((V(e)∧P(e,x)∧M(x)∧x=o∧(x=y∨S(x,y)))→¬P(f,y))),∀e(V(e)→∃f(H(f)∧U(e,f)))|=¬(∀e∀f(U(e,f)→∃x∃y(M(x)∧P(e,x)∧P(f,y)∧(x=y∨S(x,y)))))' },
    { label: 'log813', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y(P(e,x)∧x=o∧(x=y∨S(x,y))→¬P(f,y))),∀e(V(e)→∃f(H(f)∧U(e,f)))|=¬(∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,y)))))' },
    { label: 'log826', formula: '□(□¬□¬□(□p∨□q)→□(□(□¬□p→□q)∨□(□¬□q→□p)))  [reflexivity, transitivity]' },
    { label: 'log829', formula: '∀a(LaA→∀x∀y∀z(x=a∧y=a∧z=a→(Lo(x,y)R∧Lo(y,z)R→Lo(x,z)R)))→∀a∀b(LaA∧LbA→∀x∀y∀z((x=a∨x=b)∧(y=a∨y=b)∧(z=a∨z=b)→(Lo(x,y)R∧Lo(y,z)R→Lo(x,z)R)))|=∀x∀y∀z(LxA∧LyA∧LzA→(Lo(x,y)R∧Lo(y,z)R→Lo(x,z)R))' },
    { label: 'log831', formula: '(□□p→□◇q)↔(◇p→(□p→◇q))  [transitivity, seriality]' },
    { label: 'log832', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y(P(e,x)∧x=o∧(x=y∨S(x,y))→¬P(f,y))),∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,y))))|=¬(∀e(V(e)→∃f(H(f)∧U(e,f))))' },
    { label: 'log833', formula: '∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y(P(e,x)∧x=o∧(x=y∨S(x,y))→¬P(f,y))),∀e(V(e)→∃f(H(f)∧U(e,f))),∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,y))))|=¬(∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)))' },
    { label: 'log836', formula: '∀t∀x∀y∃z∃w((¬(Sxt∧¬z=t)∧¬0=z∧(z=w→x=y)∧Sxz∧Syw))→∃xS0x' },
    { label: 'log843', formula: '(¬∀x(Fx↔x=A)→¬∃y∀x(Fx↔x=y)∧A=N)∧(¬∀x(Gx↔x=B)→¬∃y∀x(Gx↔x=y)∧B=N)∧(¬∀x(Fx∨Gx↔x=C)→¬∃y∀x(Fx∨Gx↔x=y)∧C=N)→(FA→FC∨GC)' },
    { label: 'log844', formula: '(¬∀x(Fx↔x=A)→¬∃y∀x(Fx↔x=y)∧A=N)∧(¬∀x(Gx↔x=B)→¬∃y∀x(Gx↔x=y)∧B=N)∧(¬∀x(Fx∨Gx↔x=C)→¬∃y∀x(Fx∨Gx↔x=y)∧C=N)→(GB→FC∨GC)' },
    { label: 'log845', formula: '(¬∀x(Fx↔x=A)→¬∃y∀x(Fx↔x=y)∧A=N)∧(¬∀x(Gx↔x=B)→¬∃y∀x(Gx↔x=y)∧B=N)∧(¬∀x((Fx→Gx)↔x=C)→¬∃y∀x((Fx→Gx)↔x=y)∧C=N)→(¬(FC→GC)→(FA→FB))' },
    { label: 'log846', formula: '(¬∀x(Fx↔x=A)→¬∃y∀x(Fx↔x=y)∧A=N)∧(¬∀x(Gx↔x=B)→¬∃y∀x(Gx↔x=y)∧B=N)∧(¬∀x((Fx∧Gx)↔x=C)→¬∃y∀x((Fx∧Gx)↔x=y)∧C=N)→(FC∨GC→FA∨GA)' },
    { label: 'log853', formula: '(□p→□q)↔(□□p→□(□p→q))  [transitivity, seriality]' },
    { label: 'log855', formula: '(¬∀x(∃yFxy↔x=A)→¬∃y∀x(∃yFxy↔x=y)∧A=N),∀y(¬∀x(Fxy↔x=B(y))→¬∃y∀x(Fxy↔x=y)∧B(y)=N)|=∃yFAy→∃yFB(y)y' },
    { label: 'log856', formula: '∀y(∃y(y=y∧∃x(x=y∧px))↔∃z(z=y∧∃x(x=z∧px)))' },
    { label: 'log857', formula: '∀X(LXC↔∃y∃x(X=o(y,x)∧LyB∧x=n))→∀X(LXC↔∃y∃x(X=o(y,x)∧LyB∧∃s(Lxs∧∀k(Lks↔k=n))))' },
    { label: 'log865', formula: '∀r∀s∀t(LrA∧LsA∧LtA→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)),Lc1A,Lc2A,Lo(a,c1)R,Lo(b,c1)R,∀k(Lo(a,k)R∧Lo(b,k)R→Lo(c1,k)R),Lo(a,c2)R,Lo(c1,c2)R,∀k(Lo(a,k)R∧Lo(c1,k)R→Lo(c2,k)R),Lo(b,c3)R,Lo(c1,c3)R,∀k(Lo(b,k)R∧Lo(c1,k)R→Lo(c3,k)R)|=Lo(c2,c3)R' },
    { label: 'log867', formula: '∀r∀s∀t(LrA∧LsA∧LtA→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)),Lc1A,Lc3A,Lo(a,c1)R,Lo(b,c1)R,∀k(Lo(a,k)R∧Lo(b,k)R→Lo(c1,k)R),Lo(a,c2)R,Lo(c1,c2)R,∀k(Lo(a,k)R∧Lo(c1,k)R→Lo(c2,k)R),Lo(b,c3)R,Lo(c1,c3)R,∀k(Lo(b,k)R∧Lo(c1,k)R→Lo(c3,k)R)|=Lo(c3,c2)R' },
    { label: 'log868', formula: '∀r∀s∀t(LrA∧LsA∧LtA→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)),Lc1A,Lc2A,Lc3A,Lo(b,c1)R,∀k(Lo(a,k)R∧Lo(b,k)R→Lo(c1,k)R),Lo(a,c2)R,Lo(c1,c2)R,∀k(Lo(a,k)R∧Lo(c1,k)R→Lo(c2,k)R),Lo(b,c3)R,Lo(c1,c3)R,∀k(Lo(b,k)R∧Lo(c1,k)R→Lo(c3,k)R)|=Lo(c3,c2)R' },
    { label: 'log870', formula: '□∃xGx→((∃xGx↔□∀x(Gx→□Gx))∧□∀x(Gx→□Gx))  [reflexivity]' },
    { label: 'log871', formula: '(∃xGx↔□∀x(Gx→□Gx))∧□∀x(Gx→□Gx)∧◇∃xGx↔□∃xGx  [reflexivity]' },
    { label: 'log872', formula: '(∀x(Gx→□Gx))∧(∃xGx↔∀x(Gx→□Gx))↔□∃xGx  [reflexivity]' },
    { label: 'log873', formula: '∀x(LxA→Lo(x,x)R),∀w(S(P(a,a))=w↔(∀m∀n(LmA∧LnA→(Lo(m,n)R∧Lo(n,m)R→m=n))∧Lo(a,w)R∧∀y(Lo(a,y)R→Lo(w,y)R)∧∀z(Lo(a,z)R∧∀y(Lo(a,y)R→Lo(z,y)R)→z=w)))|=S(P(a,a))=a' },
    { label: 'log874', formula: '∀x(LxA→Lo(x,x)R),∀w(S(P(a,a))=w→(Lo(a,w)R∧∀y(Lo(a,y)R→Lo(w,y)R)∧∀z(Lo(a,z)R∧∀y(Lo(a,y)R→Lo(z,y)R)→z=w)))|=S(P(a,a))=a' },
    { label: 'log883', formula: '∃x∀y(Sxa∧(Sya→x=y)),∃x∀y(Sxb∧(Syb→x=y)),¬∃x(Px∧Tx)∧Ra∧Rb,∀x(Rx→¬(Px∨Tx)),¬a=b,(∃x∃y(Px∧Ty∧Sxa∧Syb)∧¬∃x∃y∃z∃w(Rx∧Ry∧Pz∧Tw∧Szx∧Swy))∨(¬∃x∃y(Px∧Ty∧Sxa∧Syb)∧∃x∃y∃z∃w(Rx∧Ry∧Pz∧Tw∧Szx∧Swy)),∀x(Sxa∨Sxb→Px∨Tx),∀x∀y(Sxy→∃z∀w(Sxz∧(Sxw→z=w)))|=¬∃x(Px∧Sxa)' },
    { label: 'log885', formula: '(∃xGx↔□∀x(Gx→□∃xGx))↔◇∃xGx  [universality]' },
    { label: 'log886', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), ¬∃x(Ox∧∀y(Ny→Rxy)), ∀x(Ox→∃y(My∧(Qxy∧Qyx))), (∃x(Ox∧¬Qxb)∧∃x(Ox∧Rxa)) |= ∃x(Mx∧∀y(Oy→Qxy))' },
    { label: 'log887', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), (Jc∧Jb), (∃x(Ox∧Qxb)∨∀x(Hx→Mx)), (∃x(Ox∧¬Qxb)∧∃x(Ox∧Gx)) |= ∃x(Ox∧∀y((Oy∧Qyx)→Qxy))' },
    { label: 'log888', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), ¬∃x(Nx∧∀y(My→Qxy)), ∃x∃y((Nx∧Oy)∧Qxy), ∀x(Nx→∃y(My∧(Qxy∧Qyx))), (Lc→(∃x(Mx∧¬Qxc)→∀x(Ox→Pxc))), (Lb→(∀x(Ox→Qxb)→¬∃x(Ox∧Qxc))) |= ∃x(Mx∧∀y(Ny→Qxy))' },
    { label: 'log889', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), ¬Pba, ∀x(Ox→∃y(My∧(Rxy∧Ryx))), ∃x∃y∃z(((Nx∧Ny)∧Oz)∧(Qxy∧Qyz)), (∀x(Mx→Pxc)→∃x(Ox∧¬Rxb)) |= ∃x(Mx∧∀y(Oy→Rxy))' },
    { label: 'log890', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), (Jc∧Jb), (∃x(Ox∧Qxb)∨∀x(Hx→Mx)), (∃x(Ox∧¬Qxb)∧∃x(Ox∧Gx)) |= ∃x(Mx∧∀y((My∧Qyx)→Qxy))' },
    { label: 'log891', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), (Ja→∃x(Mx∧¬Lx)), (¬Pab→(∃x(Mx∧¬Pxc)→∀x(Ox→Qxb))), (∃x(Nx∧Pxb)∧Pca) |= ∃x(Ox∧∀y((Oy∧Pyx)→Pxy))' },
    { label: 'log893', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), (∃x(Mx∧¬Pxc)↔∃x(Mx∧Pxc)), (∀x(Mx→Fx)→Paa), (¬∃x(Mx∧Gx)→¬∃x(Ox∧Gx)) |= (¬Mc↔¬∃x(Mx∧Pxc))' },
    { label: 'log894', formula: '((∀x(Mx∨(Nx∨Ox))∧(¬∃x(Mx∧Nx)∧(¬∃x(Mx∧Ox)∧¬∃x(Nx∧Ox))))∧(∃xMx∧(∃xNx∧∃xOx))), (∀x(Ox→Hx)→¬∃x(Ox∧Rxb)), (¬∃x(Nx∧Rxc)↔∃x(Mx∧¬Rxb)), (¬∃x(Mx∧¬Rxc)→¬∃x(Mx∧Lx)) |= (¬∃x(Ox∧Rxb)↔∃x(Ox∧¬Rxb))' },
    { label: 'log898', formula: '∀x∀y∀zFC(C(xy)C(C(yz)C(xz))),∀xFC(C(N(x)x)x),∀x∀yFC(xC(N(x)y)),∀x∀y(FC(xy)∧Fx→Fy)|=(Fa→Fb)→FC(ab)' },
    { label: 'log900', formula: '∀x∀y∀z(FC(xC(yx))∧FC(C(xC(yz))C(C(xy)C(xz)))∧FC(C(N(x)N(y))C(yx)))|=FC(aa)' },
    { label: 'log903', formula: '∃A∀C∀D(LCA∧LAD→¬u(C,D)=e)↔∀C∀D(∀A(LCA∧LAD)→¬u(C,D)=e)' },
    { label: 'log904', formula: '∃eV(e)∧∀e(V(e)→∀x(P(e,x)→(M(x)∧(x=o∨R(o,x))))),∃fH(f)∧∀f∀y(H(f)→(P(f,y)→(¬(o=y∨R(o,y))∧(¬S(o,y)∨¬M(y))))),∀e(V(e)→∃f(H(f)∧U(e,f))),∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,y))))|=¬(∀x∀y((¬M(y)∧M(x))→¬(x=y∨S(x,y))))' },
    { label: 'log907', formula: '□(p→(q→r))↔(□(p→q)→□(p→r))↔(□p→□q→□r)' },
    { label: 'log911', formula: '◇□◇□p↔◇□p  [reflexivity]' },
    { label: 'log912', formula: '(◇□(p∧¬p)∨□◇(p∧¬p))→□(◇□(p∧¬p)∨□◇(p∧¬p))' },
    { label: 'log913', formula: '∃B(∀x(LxB↔Fx)∧∀C∀D(∀x(LxC↔Fx)∧∀x(LxD↔Fx)→C=D))|=∀y(∀x(Lxt↔Lxy)↔((∀x(Lxy↔Fx)∧∃l(Lly∨y=e))∨((¬∃B∀x(LxB↔Fx)∧y=e))))→∀x(Lkt→Ft)' },
    { label: 'log923', formula: '∀m∀n(Lo(m,n)f↔m=n∧LmA)↔∀X(LXf↔∃m(X=o(m,m)∧LmA))' },
    { label: 'log928', formula: '∀X(LXA→∃a∃bX=o(a,b)),∀X(LXA→∃a∃bX=o(a,b))|=∀m∀n(Lo(m,n)A↔Lo(m,n)B)→∀x(LxA↔LxB)' },
    { label: 'log931', formula: '◇(◇□p∧□p)↔(◇◇□p∧◇□p)' },
    { label: 'log944', formula: '(∃xFx∧∃xGx∧∃x∀y(Fy→¬Hxy)∧∀x∃y(Hyx→¬Gx))→∃x∃y∀z((¬Hxz∧Hzy)→¬(Fz∧Gz))' },
    { label: 'log945', formula: '∃x∃y∀z((Fz∧Hzy)→((Gz∧Hzx)→(Hxy∧Hyx)))' },
    { label: 'log964', formula: '((∃x)¬x=a∧(∃x)((¬x=a∧Fx)∨(Fa∧[p∧¬p])))↔((∃x)(∃y)¬x=y∧(Fa→(∃x)(∃y)((¬x=y∧Fx∧Fy)∨(Fy∧Fy)))∧(¬Fa→(∃x)Fx))' },
    { label: 'log965', formula: '□∀x∀y(Oxy→□Oxy),□∀xOxx,□∀x∀y(Oxy→Oyx),□∀x∀y(Oxy↔∃z(∀w(Owz→Owx)∧∀v(Ovz→Ovy)))|=∀x∀y(∃z(Ozx∧¬Ozy)∧∀z(¬□¬Ozx→¬□¬Ozy)→¬□∃z(Ozx∧¬Ozy))  [reflexivity, transitivity]' },
    { label: 'log967', formula: '∀h(LhA∧∀m∀k(LkC∧∀X(LXm→F(k,X)=e)∧LmB→F(h,m)=k)→Mh)↔∀h(LhA→(∀m∀k(LkC→(∀X(LXm→F(k,X)=e)∧LmB→F(h,m)=k)→Mh)))' },
    { label: 'log972', formula: '((◇□a)→(□◇b))↔((◇□¬a)∨(□◇b))' },
    { label: 'log973', formula: '((◇□a)→(□◇b))↔((◇□¬a)∨(◇□b))  [seriality]' },
    { label: 'log978', formula: '(∃a1∃b1(K=o(a1,b1)∧F(f1,c)=a1∧F(f2,c)=b1)∧LcC↔∃a2∃b2(K=o(a2,b2)∧F(f3,c)=a2∧F(f4,c)=b2))↔(LcC→(∃a1∃b1(K=o(a1,b1)∧F(f1,c)=a1∧F(f2,c)=b1)↔∃a2∃b2(K=o(a2,b2)∧F(f3,c)=a2∧F(f4,c)=b2)))' },
    { label: 'log982', formula: '∃y∀x(Fx↔x=y)↔(∀y(∀x(Fx↔x=y)→Gy)→∃y(∀x(Fx∧Gx↔x=y)))' },
    { label: 'log992', formula: '∀y(Sy↔∃xLxy∨y=e)|=∀a(Sa→∃b(Sb∧∀x(Lxb↔Fx)))↔∀A∃B∀x(LxB↔Fx)' },
    { label: 'log995', formula: '∀y(Fy↔∃xLxy∨y=e)↔(∀x∀y(Lxy→Fx)∧∀y(Fy∧¬y=e→∃xLxy)∧Fe)' },
    { label: 'log613', formula: '∀xAI(x,x),∀x∀yAI(*(x,y),x),∀x∀yAI(*(x,y),y),∀x∀y∀zAI(*(I(x,y),I(x,z)),I(x,*(y,z))),∀x∀yAI(x,+(x,y)),∀x∀yAI(y,+(x,y)),∀x∀y∀zAI(*(I(x,z),I(y,z)),I(+(x,y),z)),∀x∀y∀zAI(*(x,+(y,z)),+(*(x,y),*(x,z))),∀xAI(N(N(x)),x),∀x∀y((Ax∧AI(x,y))→Ay),∀x∀y((Ax∧Ay)→A*(x,y)),∀x∀y∀z((AI(x,y))→AI(I(z,x),I(z,y))),∀x∀y∀z((AI(x,y))→AI(I(y,z),I(x,z))),∀x∀y((AI(x,N(y)))→AI(y,N(x)))|=(AI(p,I(p,a)))→Aa' },
    { label: 'log14', formula: '∀x(Pxy)∨(y=e∧¬∃z∀x(Pxz))↔t=y,¬∃z(¬z=e∧∀x(Pxz))|=t=e' },
    { label: 'log30', formula: '□(A→B)|=¬◇□B→¬◇□A  [reflexivity, symmetry, seriality]' },
    { label: 'log189', formula: '◇◇□(a∧b),◇◇◇(a∧b),◇□a|=□((□(a∧b)∧◇(a∧b))→□a)∧◇◇((□(a∧b)∧◇(a∧b))∧□a)' },
    { label: 'log246', formula: 'A,◇□A,◇□◇□A,◇□◇□◇□A,◇□◇□◇□◇□A|=□A  [reflexivity, symmetry]' },
    { label: 'log251', formula: '∃y∀x(Axy↔(Axa∧¬Axb)),∃y∀x(Axy↔(¬Axa∧Axb)),∀x(Axz↔∀u(Aux↔Aua∧¬Aub)∨∀u(Aux↔¬Aua∧Aub))|=∃d∀x(Axd↔(Axa∧¬Axb)∨(¬Axa∧Axb))' },
    { label: 'log316', formula: '(¬∃x¬∃y((◇((x=x∧Dy)↔□x=0))→x=0))→(◇∃xDx→∃xDx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log317', formula: '(¬∃x¬∃y((◇((x=x∧Dy)↔□x=0))→x=0))∧◇∃x(Gx∧Dx)∧∀x(Dx→Gx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log318', formula: '((¬∃x¬∃y((◇((x=x∧Dy)↔□x=0))→x=0)))→◇∃xDx→□∃xDx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log342', formula: '∀m∀n∃u∀x(Lxm∨Lxn→Lxu),(LXC∧LzX)|=∀Y(∀y(LyY↔∃Z(LZC∧LyZ))→¬LzY)→LzA' },
    { label: 'log447', formula: '□∀x(□(□Tx→Tx)→□Tx),∀x(□(□Tx→Tx)→□Tx),□(Ta↔(P∧□P)),(Ta↔(P∧□P))|=□(□(P∧□P)→(P∧□P))→□(P∧□P)' },
    { label: 'log449', formula: '∀M∃T∀w(∀y(Lyw→LyM)→LwT),LxA∧∃X(LXC∧LxX)|=∃Y(∃X(∀y(LyY↔LyA∧LyX)∧LXC)∧LxY)' },
    { label: 'log467', formula: '∀w(Lwp(x,y)↔w=x∨w=y),∀w(Lwp(a,b)↔a=x∨b=y)|=p(x,y)=p(a,b)→∀w(w=x∨w=y↔a=w∨w=b)' },
    { label: 'log555', formula: '□□□p|=□□□□□□□□□p  [reflexivity]' },
    { label: 'log562', formula: '◇∃xEx,∀x∀y∀z(□((Ex∧Ey)→Ez)↔x=y),∀x∀y¬□(Ex↔¬Ey)|=□∀x∃y(¬Ex→(Ey∧¬□(Ex∨Ey)))' },
    { label: 'log569', formula: '∀x∀y¬(Ex↔¬Ey),∀x∀y∀z(□((Ex∧Ey)↔Ez)→x=y)|=∀x∀y∀z(□((Ex∨Ey)↔Ez)↔x=y)' },
    { label: 'log605', formula: '◇(◇(f(a,b,c,d)=e)↔◇(g(f(g(a),g(b),g(c),g(d)))=g(e))),□∀x∃y(y=g(x))|=◇∃x(□(x=e)→(∃y(¬((a=g(y)∨(g(b)=g(y)))→((c=g(y))∨(g(x)=y))))→(g(e)=g(f(a,b,c,x)))))' },
    { label: 'log641', formula: '∀x(Px↔(◇∃xPx∧◇¬∃xPx))∧∀x(Nx↔(¬◇¬∃xNx))∧∃x(Px∧¬Nx)∧∀x(¬Nx↔∃y(□Exy))|=∀x(Px→□∃y□Exy)' },
    { label: 'log688', formula: '□(a→□a)∧◇a|=□□□□□a  [reflexivity, symmetry]' },
    { label: 'log998', formula: '∀x∀y(□(Fd→□(Fx→Txy))→◇Txy),□(Fh→Thc(m))|=◇Thc(m)' },
    { label: 'McCuneGroup', formula: '(∀X(m(0,X)=X)∧∀X(m(i(X),X)=0)∧∀X∀Y∀Z(m(m(X,Y),Z)=m(X,m(Y,Z))))→(m(a,b)=m(b,a))' }, 
];

if (typeof module !== "undefined") module.exports = invalidExamples;