examples_valid.js

var validExamples = [
    { label: 'simp', formula: '(p∨(q∧r))→((p∨q)∧(p∨r))' },
    { label: 'merg', formula: '¬((p∧¬(p→p))∨¬(p→p))' },
    { label: 'fun', formula: '∀ x F(x) → Ff(a)' },
    { label: 'func', formula: '¬(Pa∧¬Pf(f(a))∧∀x(Px→Pf(x)))' },
    { label: 'bost2nnf', formula: '¬(∀x(f(x)∧g(a)∨¬f(x)∧¬g(a)) ∧ ∀y∀z(f(b)∧¬g(y)∨g(z)∧¬f(b)) ∨ ∀w(f(d)∧¬g(w)∨¬f(d)∧g(w)) ∧ ∀s((¬f(s)∨g(e)) ∧ (¬g(k)∨f(s))))' },
    { label: 't5', formula: '∃x(P∧Fx)↔P∧∃xFx' },
    { label: 't6', formula: '∀x∃y(Fx↔Gy)→∃y∃z∀x((Fx→Gy)∧(Gz→Fx))' },
    { label: 't7', formula: '∃y∃z∀x((Fx→Gy)∧(Gz→Fx))→∀x∃y(Fx↔Gy)' },
    { label: 't8', formula: '∀x(Fx→Ff(x))∧Ff(a)→Ff(f(f(a)))' },
    { label: 't9', formula: '∀x(Fx→Ff(x))∧Ff(g(f(a),b))→Ff(f(f(g(f(a),b))))' },
    { label: 'ddelta', formula: '¬∀x(Fx∧∃y¬Fy)' },
    { label: 'b162.2', formula: '∀y∃x(Fx∧Gy)→∃x∀y(Fx∧Gy)' },
    { label: 'b164.1', formula: '∃x(Fx→∀xFx)' },
    { label: 'b164.k', formula: '∀x∃y(Fx↔Gy)↔∃y∀x(Fx→Gy)∧∃y∀x(Gy→Fx)' },
    { label: 'b164.l', formula: '∀x∃y(Fx↔Gy)↔∃y∃z∀x((Fx→Gy)∧(Gz→Fx))' },
    { label: 'conpos', formula: '∀y(Iy→∀x(Px↔Cxy))∧∃yIy→∀x(Px↔∀y(Iy→Cxy))' },
    { label: 'carnap', formula: '(∃xFx→Fw)∧(¬∃xFx∧∃xGx→Gw)↔(∃x(Fx∨(¬∃yFy∧Gx))→(Fw∨(¬∃yFy∧Gw)))' },
    { label: 'fd1eaff', formula: 'Ac, ∀x(Ax→Tx), ∀x(Mx→¬Tx), Mb, ∀xIxx, ∀x∀y(Ixy→Iyx), ∀x∀y(Ixy→(Ax→Ay)), ∀x∀y(Ixy→(Mx→My)), ∀x∀y(Ixy→(Tx→Ty)) |= ¬Ibc' },
    { label: 'id1', formula: 'c=b ∧ Fc → Fb' },
    { label: 'id2', formula: 'a=b ∧ b=c ∧ Paa → Pcc' },
    { label: 'id3', formula: '∀x∀y(f(x)=f(y)→x=y), f(a)=k, f(b)=k |= a=b' },
    { label: 'id4', formula: '∀x∀y(f(x)=f(y)→x=y), ∀x∃y(Ryx∧f(y)=k) |= ∃y∀xRyx' },
    { label: 'beckert97a', formula: '∀x(g(x)=f(x) ∨ ¬(x=a)) ∧ ∀x(g(f(x))=x) ∧ b=c ∧ Pg(g(a))b → Pac' },
    { label: 'beckert98ex4', formula: '∀x(g(x)=f(x) ∨ ¬(x=a)) ∧ ∀x(f(x)=x) ∧ Pg(a)f(b) → Pab' },
    { label: 'dv98ex1.1', formula: '∃x∃y∃u∃v((a = b → g(x, u, v) = g(y, f(c), f(d))) ∧ (c = d → g(u, x, y) = g(v, f(a), f(b))))' },
    { label: 'franssen08fibo', formula: '∀xp(x, z) = x ∧ ∀x∀yp(x,y) = p(y,x) ∧ f(z) = z ∧ f(s(z)) = s(z) ∧ ∀yf(s(s(y))) = p(f(y), f(s(y))) → f(s(s(z))) = s(z)' },
    { label: 'multiinst', formula: '(∀x(P(x)→P(f(x)))) ∧ P(d)→P(f(f(f(d))))' },
    { label: 'tseitin', formula: '((∃x∀y(Px↔Py)↔(∃zQz↔∀wQw))↔(∃x2∀x3(Qx2↔Qx3)↔(∃x4Px4↔∀x5Px5)))' },
    { label: 'pel1', formula: '((p→q)↔(¬q→¬p))' },
    { label: 'pel2', formula: '(¬¬p↔p)' },
    { label: 'pel3', formula: '(¬(p→q)→(q→p))' },
    { label: 'pel4', formula: '((¬p→q)↔(¬q→p))' },
    { label: 'pel5', formula: '(((p∨q)→(p∨r))→(p∨(q→r)))' },
    { label: 'pel6', formula: '(p∨¬p)' },
    { label: 'pel7', formula: '(p∨¬(¬(¬p)))' },
    { label: 'pel8', formula: '(((p→q)→p)→p)' },
    { label: 'pel9', formula: '((((p∨q)∧(¬p∨q))∧(p∨¬q)) → ¬(¬p∨¬q))' },
    { label: 'pel10', formula: '¬(¬(p↔q)∧(q→r) ∧(r→(p∧q))∧(p→(q∨r)))' },
    { label: 'pel11', formula: '(p↔p)' },
    { label: 'pel12', formula: '(((p↔q)↔r) ↔ (p↔(q↔r)))' },
    { label: 'pel13', formula: '((p∨(q∧r))↔((p∨q)∧(p∨r)))' },
    { label: 'pel14', formula: '((p↔q)↔((q∨¬p)∧(¬q∨p)))' },
    { label: 'pel15', formula: '((p→q)↔(¬p∨q))' },
    { label: 'pel16', formula: '((p→q)∨(q→p))' },
    { label: 'pel17', formula: '(((p∧(q→r))→s) ↔ (((¬p∨q)∨s)∧((¬p∨¬r)∨s)))' },
    { label: 'pel18', formula: '∃y∀x(Fy→Fx)' },
    { label: 'pel19', formula: '∃x∀y∀z((Py→Qz)→(Px→Qx))' },
    { label: 'pel20', formula: '(∀x∀y∃z∀w((Px∧Qy)→(Rz∧Sw)) → ∃x1∃y1((Px1∧Qy1)→∃z1(Rz1)))' },
    { label: 'pel21', formula: '¬(¬∃x(P↔Fx) ∧∃x1(P→Fx1)∧∃x2(Fx2→P))' },
    { label: 'pel22', formula: '∀x(P↔Fx)→(P↔∀yFy)' },
    { label: 'pel23', formula: '∀x(P∨Fx)↔(P∨∀yFy)' },
    { label: 'pel24', formula: '¬(¬∃x(Px∧Rx) ∧ ¬∃y(Sy∧Qy) ∧ ∀v(Pv→(Qv∨Rv)) ∧ (¬∃yPy→∃zQz) ∧ ∀w((Qw∨Rw)→Sw))' },
    { label: 'pel25', formula: '¬(¬∃x(Qx∧Px) ∧ ∃yPy ∧ ∀y(Fy→(¬Gy∧Ry)) ∧ ∀y(Py→(Gy∧Fy)) ∧ (∀y(Py→Qy)∨∃z(Pz∧Rz)))' },
    { label: 'pel26', formula: '¬(¬(∀x(Px→Rx)↔∀y(Qy→Sy)) ∧ (∃zPz↔∃zQz) ∧ ∀x∀y((Px∧Qy)→(Rx↔Sy)))' },
    { label: 'pel26nnf', formula: '¬(((q(a)∧ ¬s(a))∧ ∀x(¬p(x)∨r(x))∨ (p(b)∧ ¬r(b))∧ ∀y(¬q(y)∨s(y)))∧ (p(c)∧ q(d)∨∀z¬p(z)∧ ∀w¬q(w))∧ ∀v∀w((¬p(v)∨¬q(w))∨r(v)∧ s(w)∨¬r(v)∧ ¬s(w)))' },
    { label: 'pel27', formula: '¬(¬∀x (J(x) → ¬I(x)) ∧ ∃y (F(y) ∧ ¬G(y)) ∧ ∀z (F(z) → H(z)) ∧ ∀w ((J(w) ∧ I(w)) → F(w)) ∧ (∃x2 (H(x2) ∧ ¬G(x2)) → ∀x3 (I(x3) → ¬H(x3))))' },
    { label: 'pel28', formula: '¬(¬∀x ((P(x) ∧ F(x)) → G(x)) ∧ ∀y (P(y) → ∀z (Q(z))) ∧ (∀w (Q(w) ∨ R(w)) → ∃x2 (Q(x2) ∧ S(x2))) ∧ (∃x3 (S(x3)) → ∀x4 (F(x4) → G(x4))))' },
    { label: 'pel29', formula: '¬(¬((∀x (F(x) → H(x)) ∧ ∀y (G(y) → J(y))) ↔ ∀z ∀w ((F(z) ∧ G(w)) → (H(z) ∧ J(w)))) ∧ (∃x2 (F(x2)) ∧ ∃x3 (G(x3))))' },
    { label: 'pel30', formula: '¬(¬∀x (I(x)) ∧ ∀y ((F(y) ∨ G(y)) → ¬H(y)) ∧ ∀z ((G(z) → ¬I(z)) → (F(z) ∧ H(z))))' },
    { label: 'pel31', formula: '¬(¬∃x (I(x) ∧ J(x)) ∧ ¬∃y (F(y) ∧ (G(y) ∨ H(y))) ∧ ∃z (I(z) ∧ F(z)) ∧ ∀w (¬H(w) → J(w)))' },
    { label: 'pel32', formula: '¬(¬∀x ((F(x) ∧ K(x)) → J(x)) ∧ ∀y ((F(y) ∧ (G(y) ∨ H(y))) → I(y)) ∧ ∀z ((I(z) ∧ H(z)) → J(z)) ∧ ∀w (K(w) → H(w)))' },
    { label: 'pel33', formula: '∀x ((P(a) ∧ (P(x) → P(b))) → P(c)) ↔ ∀y ((¬P(a) ∨ (P(y) ∨ P(c))) ∧ (¬P(a) ∨ (¬P(b) ∨ P(c))))' },
    { label: 'pel34', formula: '(∃x ∀y (P(x) ↔ P(y)) ↔ (∃z (Q(z)) ↔ ∀w (Q(w)))) ↔ (∃x2 ∀x3 (Q(x2) ↔ Q(x3)) ↔ (∃x4 (P(x4)) ↔ ∀x5 (P(x5))))' },
    { label: 'pel35', formula: '∃x ∃y (P(x,y) → ∀z ∀w (P(z,w)))' },
    { label: 'pel36', formula: '¬(¬∀x ∃y (H(x,y)) ∧ ∀z ∃w (F(z,w)) ∧ ∀x2 ∃x3 (G(x2,x3)) ∧ ∀x4 ∀x5 ((F(x4,x5) ∨ G(x4,x5)) → ∀x6 ((F(x5,x6) ∨ G(x5,x6)) → H(x4,x6))))' },
    { label: 'pel37', formula: '¬(¬∀x ∃y (R(x,y)) ∧ ∀z ∃w ∀x2 ∃x3 (P(x2,z) → ((P(x3,w) ∧ P(x3,z)) ∧ (P(x3,w) → ∃x4 (Q(x4,w))))) ∧ ∀x5 ∀x6 (¬P(x5,x6) →∃x7 (Q(x7,x6))) ∧ (∃x8 ∃x9 (Q(x8,x9)) → ∀y1 (R(y1,y1))))' },
    { label: 'pel38', formula: '∀x ((P(a) ∧ (P(x) → ∃y (P(y) ∧ R(x,y)))) → ∃z ∃w ((P(z) ∧ R(x,w)) ∧ R(w,z))) ↔ ∀x2 ((((¬P(a)) ∨ P(x2)) ∨ ∃x3 ∃x4 ((P(x3) ∧ R(x2,x4)) ∧ R(x4,x3))) ∧ (((¬P(a)) ∨ (¬∃x5 (P(x5) ∧ R(x2,x5)))) ∨ ∃x6 ∃x7 ((P(x6) ∧ R(x2,x7)) ∧ R(x7,x6))))' },
    { label: 'pel39', formula: '¬∃x ∀y (F(y,x) ↔ ¬F(y,y))' },
    { label: 'pel40', formula: '∃x ∀y (F(y,x) ↔ F(y,y)) → ¬∀z ∃w ∀x2 (F(x2,w) ↔ ¬F(x2,z))' },
    { label: 'pel43', formula: '∀x∀y(Qxy ↔ ∀z(Fzx ↔ Fzy)) |= ∀x∀y(Qxy ↔ Qyx)' },
    { label: 'pel48', formula: '(a=b ∨ c=d) ∧ (a=c ∨ b=d) → (a=d ∨ b=c)' },
    { label: 'pel49', formula: '∃x∃y∀z(z=x ∨ z=y) ∧ Pa ∧ Pb ∧ ¬(a=b) → ∀xPx' },
    { label: 'pel51', formula: '∃z∃w∀x∀y(Fxy ↔ (x=z ∧ y=w)) |= ∃z∀x(∃w∀y(Fxy ↔ y=w) ↔ x=z)' },
    { label: 'pel52', formula: '∃z∃w∀x∀y(Fxy ↔ (x=z ∧ y=w)) |= ∃w∀y(∃z∀x(Fxy ↔ x=z) ↔ y=w)' },
    { label: 'pel55', formula: '∃x(Lx ∧ Kxa), La ∧ Lb ∧ Lc, ∀x∀y(Kxy → Hxy), ∀x∀y(Kxy → ¬ Rxy), ∀x (Hax → ¬ Hcx), ∀x(¬x=b → Hax), ∀x(¬ Rxa → Hbx), ∀x(Hax → Hbx), ∀x(Lx → (x=a ∨ x=b ∨ x=c)),  ∀x∃y(¬Hxy), ¬(a=b) |= Kaa' },
    { label: 'pel56', formula: '∀x(∃y(Fy ∧ x=f(y)) →Fx) ↔ ∀x(Fx →  Ff(x))' },
    { label: 'pel57', formula: 'Ff(a,b)f(b,c), Ff(b,c)f(a,c), ∀x∀y∀z(Fxy ∧ Fyz → Fxz) |= Ff(a,b)f(a,c)' },
    { label: 'pel58', formula: '∀x∀yf(x)=g(y) |= ∀x∀yf(f(x))=f(g(y))' },
    { label: 'pel59', formula: '∀x(P(x) ↔ ¬P(f(x))) → ∃x(P(x) ∧ ¬P(f(x)))' },
    { label: 'pel61', formula: '∀x∀y∀zf(x,f(y,z))=f(f(x,y),z) |= ∀x∀y∀z∀wf(x,f(y,f(z,w)))=f(f(f(x,y),z),w)' },
    { label: 'rel1', formula: '(∀x∃yCxy∧∀x∀y(Cxy→Cyx)∧∀x∀y∀z((Cxy∧Cyz)→Cxz)) → ∀xCxx' },
    { label: 'issue23a', formula: '∀x∀y∃z∀v(Evz ↔ (Ivx ∨ Ivy)) → ∀y∃z∀v(Evz ↔ Ivy)' },
    { label: 'issue23b', formula: '∀x∀y∃z∀v(Evz ↔ (v=x ∨ v=y)) → ∀y∃z∀v(Evz ↔ v=y)' },
    { label: 'issue23c', formula: '∀x∀y∃z∀v(Evz ↔ (v=x ∨ v=y)) → ∀y∃z∀v(Evz ↔ (v=y ∨ v=y))' },
    { label: 'mod1', formula: '(□p ∧ ◇q)→◇(p∧q)' },
    { label: 'mod2', formula: '◇(p ∨ q)↔(◇p ∨ ◇q)' },
    { label: 's5', formula: 'p→◇p||universality' },
    { label: 'narrow_D', formula: '(p→□r)→((p∧q)→□r)||seriality' },
    { label: 'BFCBF', formula: '∀x□Fx ↔ □∀xFx' },
    { label: 'BFCBF2', formula: '∀x□□∀y□□Fxy ↔ □∀y□∀x□□Fxy' },
    { label: 'ex5.3', formula: '□(N → (s → p)) ∧ N |= □(N → (s → (□(N → (s → p)) ∧ N))) ∧ N||universality' },
    { label: 'ex10.2d', formula: '□◇∃xFx → □∃x◇(Fx ∨ Gx)' },
    { label: 'nni', formula: '∀x∀y(¬x=y ↔ □¬x=y)||reflexivity' },
    { label: 'emil_S5', formula: '◇□A→(◇□B→◇□(A∧B))||reflexivity|symmetry|transitivity' },
    { label: 'withee', formula: '□∀x□∀y(□Fx∨□Gy)→(□∀x□Fx∨□∀x□Gx)||reflexivity|transitivity' },
    { label: 'witheeKon', formula: '(□∀x□Fx∨□∀x□Gx) → □∀x□∀y(□Fx∨□Gy)||reflexivity|transitivity' },
    { label: '04vsG0_S4', formula: '((A ∧ ¬□A)→□¬□A) ∧ ((¬A ∧ ◇A) →□◇A) → (◇□A→□◇A)||reflexivity|transitivity' },
    { label: 'pel54', formula: '∀y∃z∀x(Fxz ↔ x=y) |= ¬∃w∀x(Fxw ↔ ∀u(Fxu → ∃y(Fyu ∧ ¬∃z(Fzu ∧ Fzy))))' },
    { label: 'beckert97bid', formula: '∀x(i(u,x)=x) ∧ ∀x∀y∀z(i(i(x,y),i(i(y,z),i(x,z)))=u) ∧ ∀x∀y(i(i(x,y),y) = i(i(y,x),x)) → ∀x∀y∀z∃w(i(x,w)=u ∧ w=i(y,i(z,y)))' },
    { label: 'tseitin_mixed_args', formula: '□∀x(Fx↔□∀y(Fy↔□∀z(Fz↔□Fx)))|=◇∀x(Fx↔□∀y(Fy↔□∀z(Fz↔□Fx)))  [reflexivity]' },
    { label: 'log2', formula: '□(□¬□¬□(□p→□q)→□(□¬□¬□p→□¬□¬□q))  [reflexivity, transitivity]' },
    { label: 'log3', formula: '∀x∀y((□(Pv↔Qx)∧□(Py↔¬Qz)∧∀n∀u(□(Pn→Pu)∨□(Pu→Pn))∧∀n∀u(□(Qn→Qu)∨□(Qu→Qn)))→(¬(¬□Pv∧¬□¬Pv)∧¬(¬□Qx∧¬□¬Qx))∨(¬(¬□Py∧¬□¬Py)∧¬(¬□Qz∧¬□¬Qz)))' },
    { label: 'log4', formula: '¬(¬◇∃x∀y(Wx∧¬Eyx)∧◇∃x∃y(Wx∧Eyx)∧∃x∃y(Wx∧Eyx))∧□∃x∀y(Wx↔y=x)∧□∃x∃y(Wx∧Eyx)→□∃y∀x(Wx∧Eyx)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log6', formula: '∀x∀y((Pxy∧Pyx)→x=y),∀x∀y∀z((Pxy∧Pyz)→Pxz),∀x∀y∀z((Pzx↔Pzy)→x=y)|=¬∃x∃y∃z(¬x=y∧¬x=z∧¬y=z∧¬z=y)' },
    { label: 'log9', formula: '∀x(Axb↔Rx),∀x(Sx→Rx),∀a∃y∀x(Axy↔∃z(Aza∧x=z∧Sx))|=∃y∀x(Axy↔Sx)' },
    { label: 'log12', formula: '∃y∀x(Axy↔Rx),∀x(Sx→Rx),∀z∃u∀x(Axu↔∃y(Axz∧x=y∧Sx))|=∃y∀x(Axy↔Sx)' },
    { label: 'log15', formula: '∀A∃B∀x(LxB↔LxA∧¬Lxx),∀w(Pw↔(w=e∨∃xLxw)),∀x¬Lxe,∀y∀A(o=y↔((∀x(Lxy↔LxA∧¬Lxx)∧Py))∨(y=e∧¬∃C∀x(LxC↔LxA∧¬Lxx)))|=∀A∀y(LyA∧¬Lyy→Loy)' },
    { label: 'log16', formula: '∀A(∀x¬LxA↔A=e),∀y(o=y↔(∀x(Lxy↔Qx)∧(y=e∨∃xLxy))∨(y=e∧¬∃C((C=e∨∃xLxC)∧∀x(LxC↔Qx))))|=∀y(o=y↔(∀x(Lxy↔Qx))∨(y=e∧¬∃C(∀x(LxC↔Qx))))' },
    { label: 'log22', formula: '∀A(∀x¬LxA↔A=e),∀y(m=y↔(∀x(Lxy↔Fx)∧(y=e∨∃zLzy))∨(y=e∧¬∃C∀x(LxC↔Fx))),∃zLzm|=∃B(∃zLzB∧∀x(LxB↔Fx))' },
    { label: 'log23', formula: '∃B(LmB∧LnB),∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))|=∃B∀x(LxB↔x=m∨x=n)' },
    { label: 'log26', formula: '∀A¬(∀B¬(∀x(LxB→LxA∧(x=m∨x=n))∧∀x(LxA∧(x=m∨x=n)→LxB))∨∀x(LxA↔x=m∨x=n))|=∀A¬(LmA∧LnA)' },
    { label: 'log27', formula: '∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))|=∃A(LmA∧LnA)↔∃C∀x(LxC↔x=m∨x=n)' },
    { label: 'log28', formula: '∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))|=∃A(LmA∧LnA)→∃B∀x(LxB↔(x=m∨x=n))' },
    { label: 'log29', formula: '(∀A∃B∀x(LxB↔LxA∧(x=m∨x=n))∧∃B∀x(LxB↔(x=m∨x=n))→∃C(LmC∧LnC))' },
    { label: 'log31', formula: '∀x2∃B∀x(LxB↔Lxx2∧∃x4(Lx4x1∧Lxx4))|=∃x2∀x3(∃x4(Lx4x1∧Lx3x4)→Lx3x2)→∃B∀x(LxB↔∃x4(Lx4x1∧Lxx4))' },
    { label: 'log37', formula: '∀B¬∀y(LyB↔∃x4(Lx4x1∧Lyx4))|=∃x2(∃B∀y(LyB↔Lyx2∧∃x4(Lx4x1∧Lyx4))→∀B¬∀y(∃x4(Lx4x1∧Lyx4)→LyB))' },
    { label: 'log41', formula: 'Nh,Nd,Nl,∃x(Nx∧(Thx∧Gx)),∃x(Nx∧(Axf∧Cx)),Yd,Gl,∀x((Wx→¬Px)∧(Px→¬Wx)),∀x(Nx→¬(Gx↔¬(Yx↔Wx))),∀x(Nx→¬(Rx↔¬(Cx↔Px))),∀x∀y(Nx→(Axy∧¬((y=e)↔¬((y=f)↔(y=g)))))|=(Ale∧Ahf∧Adg)' },
    { label: 'log43', formula: '∀A∃B∀x(LxB↔LxA∧(x=a∨x=b)),∃A(LaA∧LbA)|=∃B∀x(LxB↔(x=a∨x=b))' },
    { label: 'log45', formula: '∀U(∀x(∃X(LXC∧LxX)→LxU)→(∃B∀x(LxB↔LxU∧∃X(LXC∧LxX))→∃B∀x(LxB↔∃X(LXC∧LxX))))' },
    { label: 'log49', formula: '∀A∀B∀x(Lxf(A,B)↔LxA∨LxB)|=∀x(Lxf(a,f(b,c))→Lxf(f(a,b),c))' },
    { label: 'log50', formula: '∀a∀b∀x(Lxp(a,b)↔(x=a∨x=b))|=∀x((LxA∨LxB)↔∃X(LXp(A,B)∧LxX))' },
    { label: 'log52', formula: '∀X(X=b(C,D)↔∀y(LyX↔Lyb(C,D))),∀w(Lwb(C,D)↔LwC∨LwD),LxA∨(LxC∨LxD)|=∃X((X=A∨∀y(LyX↔LyC∨LyD))∧LxX)' },
    { label: 'log53', formula: '∀X(X=m↔∀y(LyX↔Lym)),∀w(Lwm↔LwC∨LwD),LxA∨LxC∨LxD|=∃X((X=A∨∀y(LyX↔LyC∨LyD))∧LxX)' },
    { label: 'log55', formula: '∀a(s(a)=p(a,a)),∀x(Lxu(s(A),s(B))↔Lxs(A)∨Lxs(B))|=∀x(Lxu(p(A,A),p(B,B))↔Lxp(A,A)∨Lxp(B,B))' },
    { label: 'log59', formula: '∀x∃y((¬Rx∧Wy)→∃z(((Rz↔z=y)↔∀z∀y((Rz∧Ry)→z=y))→(Rz∧¬Wz)))' },
    { label: 'log60', formula: '∀x∃y((¬Rxo∧Wyd)→∃z((¬Wzr↔z=y)↔Rzr))' },
    { label: 'log61', formula: '∀x∃y((¬Rox∧Wwy)→∃z((¬Wza↔z=y)↔Rza))' },
    { label: 'log64', formula: '(∀x(∃y∃zS(x,y,z)∧∃y∃zS(y,x,z)∧∃y∃zS(y,z,x))∧∀x∀y∀u∀v((S(x,y,u)∧S(x,y,v))→(u=v))∧∀x∀y∀z(S(x,y,z)→S(y,x,z))∧∃x∀yS(x,y,y)∧∀x(∃y∃zP(x,y,z)∧∃y∃zP(y,x,z)∧∃y∃zP(y,z,x))∧∀x∀y∀u∀v((P(x,y,u)∧P(x,y,v))→(u=v))∧∀x∀y∀z(∃u∃v(S(y,z,u)∧P(x,u,v))→∃u∃t∃q∃w(S(y,z,u)∧P(x,u,w)∧P(x,y,t)∧P(x,z,q)∧S(t,q,w))))→∀t∀u∀v∀w∀x∀y∀z((S(y,z,t)∧P(x,t,w)∧P(x,y,u)∧P(x,z,v))→S(u,v,w))' },
    { label: 'log65', formula: '∀a(s(a)=p(a,a)),∀a∀b∀y(p(a,b)=y↔∀x(Lxy↔x=a∨x=b)),∀A∀B(IAB↔∀x(LxA→LxB))|=∀a∀A(LaA↔Is(a)A)' },
    { label: 'log66', formula: '∃X∀Y∀Z(((f(Y)→g(Y))↔f(X))→(((f(Y)→h(Y))↔g(X))→((((f(Y)→g(Y))→h(Y))↔h(X))→(f(Z)∧g(Z)∧h(Z)))))' },
    { label: 'log68', formula: '∀x∀y(∀z(Azx→Axy)→x=y),∀u∀z(Azu→∃x∃y(z=f(xy)))|=∀x∀y(∀m∀n(Af(mn)x↔Af(mn)y)→x=y)' },
    { label: 'log70', formula: '((∀x(Qaxx))∧(∀x∀y∀z(Qxyz→Qxs(y)s(z)))∧(∀x∀y∀z((Qxyz)→(Qyxz))))→∃xQs(s(a))s(s(s(a)))x' },
    { label: 'log71', formula: '∀x(Q(a,x,x))∧∀x∀y∀z(Q(x,y,z)→Q(x,s(y),s(z)))∧∀x∀y∀z(Q(x,y,z)→Q(y,x,z))→∃xQ(s(s(a)),s(s(s(a))),x)' },
    { label: 'log72', formula: '∀a∀b∃C∀x(LxC↔x=a∨x=b)→∀a∀b∀c∃A∀x(LxA↔x=p(a,b)∨x=s(c))' },
    { label: 'log75', formula: '∀A∀B∀x(Lxu(A,B)↔LxA∨LxB)|=∀x(Lxu(u(M,N),K)↔(LxM∨LxN∨LxK))' },
    { label: 'log77', formula: '∀a∀b∃U∀x(LxU↔Lxa∨Lxb)|=∀x(LxA→∃X(∀y(LyX↔LyA∨LyB)∧LxX))' },
    { label: 'log78', formula: '∀a∀b∃U∀x(LxU↔Lxa∨Lxb),∀a∀b∃P∀x(LxP↔x=a∨x=b)|=∀x(LxB→∃X(∀y(LyX↔LyB∨LyA)∧LxX))' },
    { label: 'log79', formula: '∀a∀y(y=s(a)↔∀x(Lxy↔x=a)),∀x(LxC↔x=s(1)∨x=s(2))|=∀x(∃X(LXC∧LxX)↔x=1∨x=2)' },
    { label: 'log80', formula: '∀a∀y(s(a)=y↔∀x(Lxy↔x=a))|=∀x(∃X((X=s(m)∨X=s(n))∧LxX)↔x=m∨x=n)' },
    { label: 'log81', formula: '∀a∀y(s(a)=y↔∀x(Lxy↔x=a))|=∀x(x=m∨x=n→∃X((∀y(LyX↔y=m)∨∀y(LyX↔y=n))∧LxX))' },
    { label: 'log82', formula: '∀a∀x(Lxs(a)↔x=a)|=∀a∀b∀x(∃X((X=s(a)∨X=s(b))∧LxX)↔x=a∨x=b)' },
    { label: 'log84', formula: '∀b∀y(p(a,b)=y↔(Lxy↔x=a∨x=b)),(s(a)=p(a,a))|=∀y(s(a)=y↔(Lxy↔x=a))' },
    { label: 'log88', formula: '∀a∀b∀y(p(a,b)=y↔∀x(Lxy↔x=a∨x=b))|=∀a∀y(∀x(Lxy↔x=a)→p(a,a)=y)' },
    { label: 'log98', formula: '□◇□□□□□◇□□□(¬(□p→p)→□(p↔□p)→□p)  [reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log99', formula: '□□□□□□□□□◇□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□(¬(□p→p)→□(p↔□p)→□p)  [euclidity]' },
    { label: 'log100', formula: '∀x∀y(Fxy→y=f(x)),∀x∀y(f(x)=f(y)→x=y)|=∀x∀y∀z(Fxy∧Fxz→y=z)∧∀x∀y∀z∀u(Fxy∧F(zu)→(y=u→x=z))' },
    { label: 'log104', formula: '∀a∀b∀c(Fab∧Fac→b=c),∀z(Azl↔Azx∧∃aFza),∀z(Azr↔Azy∧∃aFaz),∀a∀b(∀c(Aca↔Acb)→a=b),l=x,r=y,∀a∀b(Fab↔Gba),∀a∀b(Fab↔b=f(a)),∀a∀b∀c(Gab∧Gac→b=c),f(n)=f(m)|=n=m' },
    { label: 'log105', formula: '∀a∀b∀c(Fab∧Fac→b=c),∀a∀b(∀c(Aca↔Acb)→a=b),∀a∀b(Fab↔b=f(a)),∀a∀b∀c(Fba∧Fca→b=c),f(n)=f(m)|=n=m' },
    { label: 'log106', formula: '∀a∀b∀z(Lzp(a,b)↔z=a∨z=b),∀a∀b∀z(Lzu(a,b)↔Lza∨Lzb)|=∃X((X=u(A,B)∨X=C)∧LxX)↔LxA∨LxB∨LxC' },
    { label: 'log107', formula: '∀a∀b∃B∀x(Lxa∨Lxb→LxB)→∀a∀b∀c∃B∀x(Lxa∨Lxb∨Lxc→LxB)' },
    { label: 'log108', formula: '∀a∀b∃B∀x(Lxa∨Lxb→LxB)|=∀d∀e∀f∃B∀x(Lxd∨Lxe∨Lxf→LxB)' },
    { label: 'log110', formula: '∃a∃b(∃B1∀x(Lxa∨Lxb→LxB1)→∃B∀x(Lxd∨Lxe∨Lxf→LxB))' },
    { label: 'log111', formula: '∃a∃b∃B∀B1(∀x(Lxa∨Lxb→LxB1)→∀x(Lxd∨Lxe∨Lxf→LxB))→∃a∃b(∃B1∀x(Lxa∨Lxb→LxB1)→∃B∀x(Lxd∨Lxe∨Lxf→LxB))' },
    { label: 'log112', formula: '∃a∃b∀B((∀x(Lxa∨Lxb→LxB)→∀x(Lxd∨Lxe→LxB))∧(∀x(Lxa∨Lxb→LxB)→∀x(Lxf→LxB)))→∃a∃b∀B(∀x(Lxa∨Lxb→LxB)→∀x(Lxd∨Lxe∨Lxf→LxB))' },
    { label: 'log113', formula: '∀a∀b∃B∀x(Lxa∨Lxb→LxB)|=∃B∀x((Lxd∨Lxe→LxB)∧(Lxf→LxB))' },
    { label: 'log119', formula: '∀U0∃U1∀x(Lxa1∨Lxb1→LxU1)∧∀U1∃U2∀x(LxU1∨Lxb2→LxU2)→∃U1∃U2(∀x(Lxa1∨Lxb1→LxU1)∧∀x(LxU1∨Lxb2→LxU2))' },
    { label: 'log121', formula: '((o11∨o12∨o13∨o14)∧(o21∨o22∨o23∨o24)∧(o31∨o32∨o33∨o34)∧(o41∨o42∨o43∨o44)∧(o51∨o52∨o53∨o54))→((o11∧o21)∨(o11∧o31)∨(o11∧o41)∨(o11∧o51)∨(o21∧o31)∨(o21∧o41)∨(o21∧o51)∨(o31∧o41)∨(o31∧o51)∨(o41∧o51)∨(o12∧o22)∨(o12∧o32)∨(o12∧o42)∨(o12∧o52)∨(o22∧o32)∨(o22∧o42)∨(o22∧o52)∨(o32∧o42)∨(o32∧o52)∨(o42∧o52)∨(o13∧o23)∨(o13∧o33)∨(o13∧o43)∨(o13∧o53)∨(o23∧o33)∨(o23∧o43)∨(o23∧o53)∨(o33∧o43)∨(o33∧o53)∨(o43∧o53)∨(o14∧o24)∨(o14∧o34)∨(o14∧o44)∨(o14∧o54)∨(o24∧o34)∨(o24∧o44)∨(o24∧o54)∨(o34∧o44)∨(o34∧o54)∨(o44∧o54))' },
    { label: 'log122', formula: '∀a1∀b1∀b2(∀a∀b∃B∀x(Lxa∨Lxb→LxB)→∃U∀x(Lxa1∨Lxb1∨Lxb2→LxU))' },
    { label: 'log123', formula: '∀a∀b∃B∀x(Lxa∨Lxb→LxB)→∃u3∀x(Lxu1∨Lxb1∨Lxb2→Lxu3)' },
    { label: 'log125', formula: '∀a∀b∃P∀x(x=a∨x=b→LxP),∀a∀b∀c∃X∀x(Lxa∨Lxb∨Lxc→LxX)|=∃T∀x(x=e∨x=f∨x=g→LxT)' },
    { label: 'log126', formula: '∀a∀b∃U∀x(Lxa∨Lxb→LxU)|=∀a∀b∀c∃B∀x(Lxa∨Lxb∨Lxc→LxB)' },
    { label: 'log127', formula: '∀a∀b∀c∃U∀x(Lxa∨Lxb∨Lxc→LxU),∀a∀b∃p∀x(x=a∨x=b→Lxp)|=∃T∀x(x=A∨x=B∨x=C→LxT)' },
    { label: 'log130', formula: '∃P∀x(x=A∨x=B→LxP),∃S∀x(x=C→LxS),∀P∀S∃U∀x(LxP∨LxS→LxU)|=∃T∀x(x=A∨x=B∨x=C→LxT)' },
    { label: 'log131', formula: '∀x(Cx↔Lx),∀x(Lx↔∃y(Ry∧Sxy)),∀x(Ax↔∃y(Ry∧Eyx)),∀y∀x(Eyx↔(Ry∧Sxy)),∀x((Dx∧Hx)→¬Lx)|=∀x(Ax↔Lx)' },
    { label: 'log135', formula: '∀A∀B∃C∀x(LxC↔LxA∧LxB)|=∀A∀B∃U∀x(LxU→LxA∧LxB)' },
    { label: 'log137', formula: '∀A∃B∀x(LxA∧Fx↔LxB),∃A∀x(Fx→LxA)|=∃A∀x(Fx↔LxA)' },
    { label: 'log138', formula: '∃P1∀X(FXE→LXP1)|=∃P1(∃P∀X(LXP↔LXP1∧FXE)↔∃P∀X(LXP↔FXE))' },
    { label: 'log139', formula: '∀E∃P1∀X(FXE→LXP1)|=∀E∀A∃B∀x(LxA∧FxE↔LxB)→∀E∃P∀X(LXP↔FXE)' },
    { label: 'log141', formula: '∀A∀B(A=B↔∀x(LxA↔LxB)),∀B∀x(Lxc(B)↔LxE∧¬LxB),∀X∀x(LxX→LxE)|=∀A(c(c(A))=A)' },
    { label: 'log143', formula: '∀x∀y(∀z(Azx↔Azy)→x=y),∀x∀y∀z(Rxy∧Ryz→Rxz),∀x∀y(Rxy→Ryx),∀xRxx,¬g(a)=g(b),∀z∀x(Azg(x)↔Azd∧Rzx)|=¬∃z(Azg(a)∧Azg(b))' },
    { label: 'log145', formula: '∀m∀n∀x(Lxp(m,n)↔x=m∨x=n),∀k∀x(Lxs(k)↔Lxp(k,k)),C=p(s(a),p(a,c))|=∀x(Lxs(a)→∀X(LXC→LxX))' },
    { label: 'log146', formula: '∀A∀B(A=B↔∀x(LxA↔LxB)),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n),∀k∀x(Lxs(k)↔Lxp(k,k))|=∀x∀X(Lxs(a)→(X=p(a,c)→LxX))' },
    { label: 'log149', formula: '∀A∀B(A=B↔∀x(LxA↔LxB)),∀A∀x(Lxc(A)↔LxE∧¬LxA)|=(∀y(LyY↔LyE∧¬LyX)↔Y=c(X))' },
    { label: 'log150', formula: '∀A(c(c(A))=A),∀A∀x(Lxc(A)↔LxE∧¬LxA)|=∀x(LxX↔LxE∧¬LxY)↔∀x(LxY↔LxE∧¬LxX)' },
    { label: 'log154', formula: '∀A∀x(Lxc(A)↔LxE∧¬LxA),∀A∀B(A=B↔∀x(LxA↔LxB))|=X=c(Y)↔∀x(LxX↔LxE∧¬LxY)' },
    { label: 'log158', formula: '∀A∀B(A=B↔∀x(LxA↔LxB)),∀M∀N∀x(Lxp(M,N)↔x=M∨x=N),∀K∀x(Lxs(K)↔Lxp(K,K))|=s(m)=s(r)↔m=r' },
    { label: 'log159', formula: '∀M∀N∀x(Lxp(M,N)↔x=M∨x=N),∀K∀x(Lxs(K)↔Lxp(K,K))|=∀x(Lxs(m)↔Lxp(r,t))↔∀x(x=m↔x=r∨x=t)' },
    { label: 'log160', formula: '∀m∀n∀r∀t(p(m,n)=p(r,t)↔(m=r∧n=t)∨(m=t∧n=r)),∀m∀r(s(m)=s(r)↔m=r)|=(s(a)=s(x)∧p(a,b)=p(x,y))∨(s(a)=p(x,y)∧p(a,b)=s(x))→((a=x)∧((a=x∧b=y)∨(a=y∧b=x)))∨(s(a)=p(x,y)∧p(a,b)=s(x))' },
    { label: 'log162', formula: '∀m∀n∀x(x=p(m,n)↔x=m∨x=n),∀k∀x(Lxs(k)↔x=k),∀X∀Y(IXY↔∀x(LxX→LxY))|=Is(a)A∧Is(b)B→∀x(Lxp(A,B)→∃X(LXp(A,B)∧LxX))' },
    { label: 'log163', formula: '∀X∀Y(IXY↔∀x(LxX→LxY)),∀k∀x(Lxs(k)↔x=k)|=LaA∧LbB↔Is(a)A∧Is(b)B' },
    { label: 'log165', formula: '∀X∀Y(IXY↔∀x(LxX→LxY)),∀k∀x(Lxs(k)↔x=k),∀E∃T∀X(IXE→LXT)|=∀A∃T∀x(∃a(LaA∧∀y(Lyx↔Lys(a)))→LxT)' },
    { label: 'log175', formula: '∀x∀y∃w∀z(Rzw↔(z=x∨z=y))|=∀x∃y∀z(Rzy↔z=x)' },
    { label: 'log176', formula: '∀x∀y∀z(c(c(x,y),c(z,c(x,y)))=1),∀x∀y∀z(c(c(x,c(y,z)),c(c(x,y),c(x,z)))=1),∀x∀y(x=1→(c(x,y)=1→y=1))|=c(c(b,d),c(c(a,b),c(a,d)))=1' },
    { label: 'log177', formula: '∀x∀y(c(c(x,c(x,y)),c(x,y))=1),∀x∀yc(n(c(x,y)),n(y))=1,∀x∀y∀z(c(c(c(x,y),z),c(n(z),n(y)))=1),∀x∀y(c(c(n(c(x,y)),y),c(x,y))=1),∀x∀y(c(n(c(x,x)),y)=1),∀x∀y∀z(c(c(x,y),c(z,c(x,y)))=1),∀x∀y∀z(c(c(x,c(y,z)),c(c(x,y),c(x,z)))=1),∀x∀y((x=1∧c(x,y)=1)→y=1)|=c(c(n(a),a),a)=1' },
    { label: 'log178', formula: '□(p↔□P),□(q↔□Q)|=□◇(p∧q)→◇□(p∧q)  [reflexivity, transitivity]' },
    { label: 'log185', formula: '∀A∀B(A=B↔∃x(LAx↔LBx)),∀k∀x(Lxs(k)↔x=k)|=∀A∀B(A=B↔∀x(LxA↔LxB))' },
    { label: 'log186', formula: '∀x∀y∀zc(c(c(x,y),z),c(n(z),n(y)))=1,∀x∀y∀zc(c(x,c(y,z)),c(c(x,y),c(x,z)))=1,∀x∀y∀zc(c(x,y),c(z,c(x,y)))=1,∀x∀yc(c(n(c(x,y)),y),c(x,y))=1,∀x∀yc(n(c(x,x)),y)=1,∀x∀y((c(x,y)=1∧x=1)→y=1),∀x∀y∀z∀wc(c(x,c(c(y,z),w)),c(c(y,z),c(x,w)))=1|=c(c(p,q),c(c(q,r),c(p,r)))=1' },
    { label: 'log187', formula: '∀A∀B(∀x(LxA→LxB)→A=B),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n),∀k∀x(Lxs(k)↔Lxp(k,k))|=∃x(x=o(a,b)∧∃m∃n(LmR∧LnT∧x=o(m,n)))→(LaR∧LbT)' },
    { label: 'log190', formula: '∀x∀y∀z(I(x,y)=1→I(z,I(x,y))=1),∀x∀yI(N(I(x,x)),y)=1,∀x∀y∀z(I(x,I(y,z))=1→I(I(x,y),I(x,z))=1),∀x∀y(I(N(I(x,y)),y)=1→I(x,y)=1),∀x∀y∀z(I(I(x,y),z)=1→I(N(z),N(y))=1),∀x∀y((I(x,y)=1∧x=1)→y=1)|=I(p,p)=1' },
    { label: 'log193', formula: '∀x∀y∀z∀w(Ti(c(x,y),c(z,w))→(Tc(n(c(x,y)),f)→Tc(n(c(z,w)),f))),∀x∀y(Ti(x,y)↔(Tn(c(x,y))→(Tx→Ty))),∀x∀y((Tx→Ty)↔Tc(x,y)),∀x(Tx↔¬(Tx→Tf)),∀x(Td(x)↔¬Tx),∀x(Tn(x)↔¬Ti(d(f),x))|=Ti(a,b)→Ti(b,e)→Ti(a,e)' },
    { label: 'log194', formula: '∀x∀y∀z∀w(Ti(c(x,y),c(z,w))→(Tc(n(c(x,y)),f)→(Tn(c(z,w))→Tf))),∀x∀y(Ti(x,y)↔(Tn(c(x,y))→(Tx→Ty))),∀x∀y((Tx→Ty)↔Tc(x,y)),∀x(Tx↔¬(Tx→Tf)),∀x(Td(x)↔¬Tx),∀x(Tn(x)↔¬Ti(d(f),x))|=Ti(a,b)→Ti(b,e)→Ti(a,e)' },
    { label: 'log195', formula: '∀x∀y∀z(Ti(y,z)→Ti(x,i(y,z))),∀x∀y∀z∀w(Ti(c(x,y),c(z,w))→((Tn(c(x,y))→Tf)→(Tn(c(z,w))→Tf))),∀x∀y(Ti(x,y)↔(Tn(c(x,y))→(Tx→Ty))),∀x∀y((Tx→Ty)↔Tc(x,y)),∀x(Tx↔¬(Tx→Tf)),∀x(Td(x)↔¬Tx),∀x(Tn(x)↔¬Ti(d(f),x))|=Ti(a,b)→Ti(b,e)→Ti(a,e)' },
    { label: 'log196', formula: '□∀x∀y(Tc(x,y)↔(Tx→Ty)),□∀x∀y(Ti(x,y)↔□(Tx→Ty)),□∀x(Td(x)↔¬Tx)|=Ti(p,q)→Ti(q,r)→□(Tp→Tr)  [reflexivity, transitivity]' },
    { label: 'log197', formula: '□∀x∀y(Tc(x,y)↔(Tx→Ty)),□∀x∀y(Ti(x,y)↔□(Tx→Ty)),□∀x(Td(x)↔¬Tx)|=□(Tp→Tq)→□(Tq→Tr)→□(Tp→Tr)  [reflexivity, transitivity]' },
    { label: 'log198', formula: '∀M∀m(LmM→LmE),∀M∀m(Lmc(M)↔LmE∧¬LmM),∀M∀N(∀z(LzM→LzN)→M=N)|=c(c(Y))=Y' },
    { label: 'log199', formula: '(a=1↔¬a=0),∀x+(x,0)=x,∀x+(x,1)=1,∀x(n(x)=0↔x=1),∀x(n(x)=1↔x=0),∀x∀y+(x,y)=n(*(n(x),n(y)))|=n(n(a))=a' },
    { label: 'log200', formula: 'c=0,a=0,b=0,∀x+(x,0)=x,∀x+(x,1)=1,∀x*(x,0)=0,∀x*(x,1)=x|=*(a,+(b,c))=+(*(a,b),*(a,c))' },
    { label: 'log201', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(¬x=0↔x=1)|=c(a,c(b,b))=1' },
    { label: 'log202', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(¬x=0↔x=1)|=c(a,c(c(a,0),b))=1' },
    { label: 'log203', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(x=0↔¬x=1)|=c(b,c(a,a))=1' },
    { label: 'log204', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(x=0↔¬x=1)|=c(a,c(b,a))=1' },
    { label: 'log205', formula: '∀x∀y(Tc(x,y)↔(Tx→Ty)),¬Tf|=Tc(c(b,f),c(a,f))→Tc(a,b)' },
    { label: 'log208', formula: '∀x(A→∃y∀a((Eax∧∃nEna)→∃s∀t((Eta∧Ety)↔s=t)))|=∀x(∃o(Eox∧∀n¬Eno)∨¬A∨∃y∀e(Eex→∃a(Eae∧Eay∧∀b((Ebe∧Eby)→a=b))))' },
    { label: 'log210', formula: '∀x∀y∀e((Eex↔Eey)→x=y),∀x(∃yEyx→∃y(Eyx∧∀z(Ezy→¬Ezx))),∀x(¬∃o(Eox∧¬∃nEno)→∀e(Eex→∃c(Ece∧∃r(Ecr∧∀x(Exe∧Exr→x=c))))),∀x∃u∀y(Eyu↔∃e(Eex∧Eye)),∀x∃p∀y(∀e(Eey→Eex)→Eyp),∃i(∃o(Eoi∧¬∃nEno)∧∀x(Exi→∃s(Esi∧∀a(Eas↔(Eax∨a=x)))))|=A∧¬A' },
    { label: 'log211', formula: '∀x(∀e(Eex→∃nEne)→(∃a∃b∃c(Eax∧Ebx∧Eca∧Ecb∧¬(a=b))∨∃r∀e(Eex→∃a(Eae∧Ear∧∀b((Ebe∧Ebr)→a=b)))))|=∀x(∀e(Eex→∃nEne)→(∃a∃b∃c(Eax∧Ebx∧Eca∧Ecb∧¬(a=b))∨∃r∀e(Eex→∃a(Eae∧Ear∧∀b((Ebe∧Ebr)→a=b)))))' },
    { label: 'log212', formula: '∀x(∀e(Eex→∃nEne)→(∃a∃b∃c(Eax∧Ebx∧Eca∧Ecb∧¬(a=b))∨∃r∀e(Eex→∃a(Eae∧Ear∧∀b((Ebe∧Ebr)→a=b)))))|=∀x(∀e(Eex→∃nEne)→∃r(∃b∃c(Erx∧Erx∧Ecr∧Ecb∧¬(r=b))∨∀e(Eex→∃a(Eae∧Ear∧∀b((Ebe∧Ebr)→a=b)))))' },
    { label: 'log213', formula: '∀x∃y∀e(∃z(Eze∧Eex)→∃v∀u(∃t((Eue∧Eet)∧(Eut∧Ety))↔u=v))|=∀x∃y∀e(∃z(Eze∧Eex)→∃v∀u(∃t((Eue∧Eet)∧(Eut∧Ety))↔u=v))' },
    { label: 'log214', formula: '¬∃V∀x(LxV↔∀X(LXC→LxX)),∃yLyC→∃V∀x(LxV↔∀X(LXC→LxX))|=∀x∀X(LXC→LxX)' },
    { label: 'log215', formula: '∀X∀x(LxX→LxE),∀A∀x(Lxc(A)↔LxE∧¬LxA),∀m∀n(m=n↔∀x(Lxm↔Lxn))|=∀A(c(c(A))=A)' },
    { label: 'log216', formula: '(Na∧Nv∧Nm),(Dve∧Bav),(∀x∀y((Nx∧Ny)→(Bxy↔∃z(Dxz∧Dyz)))),(∀x∀y((Nx∧Dxy)→∀z(Dxz→(z=y))))|=(Bma→Dme)' },
    { label: 'log217', formula: '∀e∃T∀X(∀x(LxX→Lxe)→LXT),∀m∀x(Lxc(m)↔LxE∧¬Lxm)|=∀C∃B∀X(∃Y(LYC∧∀x(Lxc(Y)↔LxX))→LXB)' },
    { label: 'log218', formula: '∀e∃T∀X(∀x(LxX→Lxe)→LXT),∀m∀x(Lxc(m)→LxE∧¬Lxm),∀m∀x(LxE∧¬Lxm→Lxc(m))|=∀C∃B∀X(∃Y(LYC∧∀x(Lxc(Y)↔LxX))→LXB)' },
    { label: 'log220', formula: '(Dve∧Bav),(Na∧Nv∧Nm),∀x∀y((Nx∧Ny)→((Bxy↔∃z(Dxz∧Dyz))∧(Bxy↔Byx))),∀x∀y((Nx∧Dxy)→∀z(Dxz→(z=y)))|=(Bma→Dme)' },
    { label: 'log221', formula: '∀x∀y∀z((Nx∧Ny)→(Bxy↔∃p(Dxp∧Dyp))),(∀x∀y((Nx∧Dxy)→∀z(Dxz→(z=y)))),(Dve∧Bav),(Na∧Nv∧Nm)|=(Bma→Dme)' },
    { label: 'log222', formula: '(∀x(Ux→Ex∧Sx)→∃xMx)∧(∀x((Ux→¬Ex∧Sx∧Tx)→◇∃xCx))∧∀x(Ux→Sx∧Tx)∧¬(∃xIx∨∃xLx∨∃xMx)→(∃x(◇Cx∧¬(Ix∨Lx)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log225', formula: '(Na∧Nv∧Nm),(Dve∧Bav),(∀x∀y((Nx∧Ny)→(Bxy↔∃z(Dxz∧Dyz)))),(∀x∀y∀z((Nx∧Dxy∧Dxz)→z=y)),Bmv|=Dme∧Bmv' },
    { label: 'log230', 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(y=t(Y)→Lyu)∧∀z(LzA→Lzu)))' },
    { label: 'log234', formula: '∀n∃p∀x(x=A∨x=n→Lxp),∀y∀x(Lyt(x)↔LyA∨Lyx)|=∀n∃u(∀y(y=t(Y)→Lyu)∧∀z(LzA→Lzu))' },
    { label: 'log235', formula: '∀n∃p∀x(x=A∨x=n→Lxp),∀y∀x(Lyt(x)↔LyA∨Lyx)|=∀n∃u(∀y(y=t(n)→Lyu)∧∀z(LzA→Lzu))' },
    { label: 'log236', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X∀y(t(X)=y↔∀x(Lxy↔LxA∧LxX)∧(∃zLzy∨∀z¬Lzy)),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzA→Lzu)))' },
    { label: 'log237', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X(∀x(Lxt(X)↔LxA∧LxX)∧(∃zLzt(X)∨∀z¬Lzt(X))),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzX→Lzu)))' },
    { label: 'log239', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X(∀x(Lxt(X)↔LxA∧LxX)∧(∃zLzt(X)∨∀z¬Lzt(X))),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∀X(∃u(Lt(X)u∧∀z(LzA→Lzu)∧∀z(LzX→Lzu)))' },
    { label: 'log240', formula: '∀n∃P∀x(x=A∨x=n→LxP),∀X(∀x(Lxt(X)↔LxA∧LxX)∧(∃zLzt(X)∨∀z¬Lzt(X))),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzA∨LzX→Lzu)))' },
    { label: 'log241', formula: '∀X∃u∀z(z=A∨z=X→Lzu),∀X(∀z(Lzt(X)↔LzA∧LzX)∧(∃zLzt(X)∨∀z¬Lzt(X))),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzX→Lzu)))' },
    { label: 'log242', formula: '∀X∃u∀z(z=A∨z=X→Lzu),∀X(∀z(Lzt(X)↔LzA∧LzX)∧(∃zLzt(X)∨∀z¬Lzt(X))),∀m∀X∃u∀x(Lxm∨LxX→Lxu)|=∀X(LXC→∃u(Lt(X)u∧∀z(LzX→Lzu)))' },
    { label: 'log247', formula: '∀k∀z(Lzs(k)↔z=k),∀E∃T∀x(∀y(Lyx→LyE)→LxT),∀a∀b(a=b↔∀x(Lxa↔Lxb))|=∃D∀y(∃Y(y=s(Y)∧LYC)→LyD)' },
    { label: 'log250', formula: '∀x∀y(Lym(x)↔y=x∧¬LyB),∀E∃T∀x(∀y(Lyx→LyE)→LxT),∀r∀t(∀x(Lxr→Lxt)→r=t)|=∃D∀x(∃A(A=m(x)∧LAD))' },
    { label: 'log258', formula: '((((∀x(Sx↔(¬◇∃y(Gyx)∧¬◇∃y(¬(x=y)∧¬(Gxy)))))→□(∀x(Sx↔(¬◇∃y(Gyx)∧¬◇∃y(¬(x=y)∧¬(Gxy))))))))∧◇∃xSx∧(∀x(Sx↔(¬◇∃y(Gyx)∧¬◇∃y(¬(x=y)∧¬(Gxy)))))→□∃xSx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log261', formula: '∀x(x=0↔¬x=1),∀x∀y(c(x,y)=1↔(x=0∨y=1))|=c(c(a,0),0)=a' },
    { label: 'log268', formula: '∃E∀T∃Y((LEm(Y)↔E=Y∧¬LEB)→∀w(∀x(Lxm(w)→LxE)∨Lm(w)T))→∃E∀T∃Y∀w((LEm(Y)↔E=Y∧¬LEB)→∀x(Lxm(w)→LxE)∨Lm(w)T)' },
    { label: 'log270', formula: '∃E∀T∃Y∀w((LEm(Y)↔E=Y∧¬LEB)→∀x(Lxm(w)→LxE)∨Lm(w)T)→∃E∃Y∀w((LEm(Y)↔E=Y∧¬LEB)→∀x(Lxm(w)→LxE))' },
    { label: 'log271', formula: '∀x∃y∀z(Lzy↔Lzx∧Fz)|=∃y∀z(Fz→Lzy)↔∃y∀z(Fz↔Lzy)' },
    { label: 'log274', formula: '∃E∀T∃Y∃y∀w((∀x(Lxm(w)→LxE)→Lm(w)T)→((Lym(Y)↔y=Y∧¬LyB)→Lm(w)E))|=∃E∀T∃D∃Y∃y∀w((∀x(Lxm(w)→LxE)→Lm(w)T)→((Lym(Y)↔y=Y∧¬LyB)→Lm(w)D))' },
    { label: 'log279', formula: '∀k∀x(Lxs(k)↔x=k)|=LaA→∃x(∀y(Lyx↔y=a)∧∀y(Lyx→LyA))' },
    { label: 'log280', formula: '∀k∀x(∃TLxT↔x=a),∀k∀x(∃TLxT↔x=A),∀k∀x(∃TLxT↔x=x)|=(∀y∀x(Lxy↔x=a)→∀y∀x(Lxy→LxA))→LaA' },
    { label: 'log281', formula: '∀x∀y(t(x)∧t(i(x,y))→t(y)),∀x∀yt(i(x,i(y,x))),∀x∀y∀zt(i(i(x,i(y,z)),i(i(x,y),i(x,z)))),∀x∀yt(i(i(n(x),n(y)),i(y,x)))|=t(i(p,n(n(p))))' },
    { label: 'log287', formula: '∀k∀x(Lxs(k)↔x=k)|=∀x(∀y(Lyx↔Lys(a))→LxP(A))↔∀x(∀y(Lyx↔y=a)→LxP(A))' },
    { label: 'log288', formula: '∀x∀O((ExX↔x=O)∧(ExO↔x=f∨x=s)∧(Exf↔ExA)∧(Exs↔ExA∨ExB))∧(EmA∧EnA∧¬m=n∧¬m=j∧¬m=k∧¬n=j∧¬n=k∧¬j=k∧∀x(ExA→x=m∨x=n))∧(EjB∧EkB∧¬j=k∧∀x(ExB→x=j∨x=k))|=∃p∃q∃r∃t(EpX∧(EqX∧(ErX∧(EtX∧(¬p=q∧(¬p=r∧(¬p=t∧(¬q=r∧(¬q=t∧(¬r=t∧∀y(EyX→(y=p∨(y=q∨(y=r∨y=t))))))))))))))' },
    { label: 'log289', formula: '∀x∀y∀zI(I(x,y),I(z,I(x,y)))=1,∀x∀y∀zI(I(x,I(y,z)),I(I(x,y),I(x,z)))=1,∀x∀yI(n(I(x,x)),y)=1,∀x∀y∀zI(I(I(x,y),z),I(n(z),n(y)))=1,∀x∀yI(I(n(I(x,y)),y),I(x,y))=1,∀x∀y((I(x,y)=1∧x=1)→y=1)|=I(p,q)=1→I(q,r)=1→I(p,r)=1' },
    { label: 'log290', formula: 'P(A)=t,∀x(Lxt↔IxA),∀M∀N(IMN↔∀x(LxM→LxN)),∀m∀x(Lxs(m)↔x=m)|=∀y(∀x(Lxy↔x=a)→∀x(Lxy→LxA))→Is(a)A' },
    { label: 'log291', formula: '∀y∃x∀x1∀y1((((Wy→Rx1)→(Rx1∧¬Wy))∧x1=x)∧(((Wy1→Rx)→(Rx∧¬Wy1))∧y1=y))↔∃x∀x1∀y1∀y((((Wy→Rx1)→(Rx1∧¬Wy))∧x1=x)∧(((Wy1→Rx)→(Rx∧¬Wy1))∧y1=y))' },
    { label: 'log292', formula: '(∃x)(∃y)(Rax∧Ray∧¬x=y∧(∃w)(Gaw∧(w=x∨w=y))∧¬(∃z)((Raz∨Gaz)∧¬z=x∧¬z=y))→(∃x)(∃y)(Rax∧Ray∧¬x=y∧¬(∃z)(Raz∧¬z=x∧¬z=y)∧(∃w)(Gaw∧(w=x∨w=y))∧¬(∃z)(Gaz∧¬z=x∧¬z=y))' },
    { label: 'log293', formula: '∀A∃B∀x(LxB↔LxA∧Fx),∃A∀x(Fx→LxA)|=∃A∀x(Fx↔LxA)' },
    { label: 'log294', formula: '(□◇□(□◇□(◇□A→A)→A))→◇□A  [reflexivity, transitivity]' },
    { label: 'log297', formula: '(∀x(Lxt↔x=a)∧St)∨(Et∧¬∃B∀x(LxB↔x=a)),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=∀x(Lxt↔Lxs(a))→∀x(x=a↔Lxs(a))' },
    { label: 'log298', formula: '∀y(y=t↔(∀x(Lxy↔x=a)∧Sy)∨¬(Ey∧¬∃B∀x(LxB↔x=a))),∀m∀n∃p∀x(x=m∨x=n↔Lxp)|=∀x(Lxt→x=a)' },
    { label: 'log300', formula: '∀y(y=t↔(∀x(Lxy↔x=a)∧Sy)∨¬(Ey∧¬∃B∀x(LxB↔x=a)))→(∀m∀n∃p∀x(x=m∨x=n↔Lxp)→∀x(x=a→Lxt))' },
    { label: 'log302', formula: '∀C∃U∀x(∃X(LXC∧LxX)→LxU),∀m∀n∃p∀x(x=m∨x=n→Lxp)|=∃p∀x(Lxa∨Lxb∨Lxc→Lxp)' },
    { label: 'log303', formula: '∃p∀x(x=a∨x=b↔Lxp),∀p∃u∀x(∃X(LXp∧LxX)↔Lxu)|=∃V∀x(Lxa∨Lxb↔LxV)' },
    { label: 'log304', formula: '∃p∃u(∀x(x=a∨x=b↔Lxp)∧∀x(∃X(LXp∧LxX)↔Lxu))|=∃V∀x(Lxa∨Lxb↔LxV)' },
    { label: 'log305', formula: '¬∀x(Lxa∨Lxb↔Lxu)→¬∃p(∀x(x=a∨x=b↔Lxp)∧∀x(∃X(LXp∧LxX)↔Lxu))' },
    { label: 'log306', formula: '∀x(x=a∨x=b↔Lxp),∀x(∃X(LXp∧LxX)↔Lxu)|=∀x(Lxa∨Lxb↔Lxu)' },
    { label: 'log307', formula: '∀m∀n∀k∃u∀x(Lxm∨Lxn∨Lxk→Lxu),∀a∃s∀x(x=a→Lxs)|=∀a∀n∀k∃u∀x(x=a∨x=n∨Lxk→Lxu)' },
    { label: 'log309', formula: '∀A∀B∀x(Lxu(A,B)↔LxA∨LxB),∀A∀B∀x(Lxv(A,B)↔LxA∧LxB),∀A∀B∀x(Lxr(A,B)↔LxA∧¬LxB),∀A(c(A)=r(E,A)),∀x(LxE),∀X∀x(LxX→LxE)|=Lyv(m,n)→Lyu(v(m,k),v(n,c(k)))' },
    { label: 'log311', formula: '∀M∀N∀x(Lxu(M,N)↔LxM∨LxN),∀M∀N(IMN↔∀x(LxM→LxN))|=IAX∧IBX→Iu(A,B)X' },
    { label: 'log313', formula: '∀X∀Y(IXY↔∀x(LxX→LxY)),∀A∀B∀x(Lxr(A,B)↔LxA∧¬LxB),∀x¬Lxe|=(∀y(Lyr(M,N)↔Lye)→IMN)' },
    { label: 'log314', formula: '∀A∀x(Lxc(A)↔LxE∧¬LxA),∀A∀B∀x(Lxu(A,B)↔LxA∨LxB),∀A∀B∀x(Lxv(A,B)↔LxA∧LxB)|=(Lyv(c(m),c(n))→Lyc(u(m,n)))' },
    { label: 'log323', formula: '(◇∃x(Ex∧∀y(Ey→(Py→□(Ey→Hxy))))∧□∀x(Ex→(∀y(Ey→(Py→Hxy))→□Ex))∧□∀x(Ex→(Px→□(Px∧Ex))))→□∃x(Ex∧∀y(Ey→(Py→□(Ey→Hxy))))  [universality]' },
    { label: 'log324', formula: '(∃y4∀y5∀x∀x1(((¬Wy5→Rx1)∧y5=y4)∧((¬Wy4→Rx)∧x1=x)))↔(∃x∀x1∀y5∀y4(((¬Wy5→Rx1)∧y5=y4)∧((¬Wy4→Rx)∧x1=x)))' },
    { label: 'log325', formula: '∀m∀n(∀x(Lxm↔Lxn)→m=n)|=∃y(y=r(A,B)∧LyX)↔∃y(∀x(Lxy↔Lxr(A,B))∧LyX)' },
    { label: 'log326', formula: '∀m∀n(∀x(Lxm↔Lxn)→m=n)|=∃y(∀x(Lxy↔Lxr(A,B))∧LyX)↔∃y(y=r(A,B)∧LyX)' },
    { label: 'log332', formula: '∀A∀x(Lxc(A)↔Lxe∧¬LxA)|=∀x(LxX↔Lxc(Y))↔∀x(LxX↔Lxe∧¬LxY)' },
    { label: 'log333', formula: '(∃Y(LYC∧∀x(LxX↔LxE∧¬LxY))→LXD)|=∀M∀x(Lxc(M)↔LxE∧¬LxM)→(∃Y(LYC∧∀x(LxX↔Lxc(Y)))→LXD)' },
    { label: 'log334', formula: '∀xP(x,x)∧∀x∀y(P(x,y)∧P(y,x)→x=y)∧∀x∀y∀z(P(x,y)∧P(y,z)→P(x,z))∧∀x∀y(D(x,y)↔∀z(P(z,x)→¬P(z,y)))∧∀x∀y∀s(Sum(s,x,y)↔P(x,s)∧P(y,s)∧∀z(D(x,z)∧D(y,z)→D(s,z))∧∀v(P(x,v)∧P(y,v)→D(s,v)))∧∀x∀y∃s(Sum(s,x,y))∧∀x∀y∀z∀s∀t(P(x,z)∧¬(x=z)∧D(x,y)∧D(x,y)∧Sum(s,x,y)∧Sum(t,z,y)→P(s,t)∧¬(s=t))→∀x∀y∀s∀t(Sum(s,x,y)∧P(t,s)∧D(t,x)→P(t,y))' },
    { label: 'log335', formula: '□∀x∀y((Px∧Py)→(Fxy→□(∃z(Bz∧Szy)→∃w(Bw∧Swx)))),□∀x∀y((Bx∧By)→x=y)|=□∀x∀y((Px∧Py)→(Fxy→□∀z((Bz∧Szy)→Szx)))  [transitivity]' },
    { label: 'log337', formula: '(∀x¬Rxx∧∀a∀b∀x∀y((Rax∧Rby)→(Ray∨Rbx)))↔(∀x¬Rxx∧∀x∀y∀z(Rxy→Ryz→Rxz)∧¬∃a∃b∃x∃y(Rax∧Rby∧(¬Rbx∧¬Rxb)∧(¬Ray∧¬Rya)))' },
    { label: 'log338', formula: '∀x∀y(Exy↔∀z(Rzy↔Rzx)),∀x∀y(∀z(Rzy↔Rzx)→∀u(Rxu→Ryu))|=(Eab∧Eac)→Ebc' },
    { label: 'log343', formula: '∀xExx,∀x∀y∀z((Exy∧Exz)→Eyz),∀x∀y(Exy→Fx→Fy),¬∀x∀yExy,∀x(Fx↔(Gx∨Hx))|=Eab→Hb→Ecb→Eac' },
    { label: 'log345', formula: '∀M∀N∃B1∃B2(∀x(∃X(LXM∧LxX)→LxB1)∧∀X((X=N→LXB2)∧(X=B1→LXB2))),∀m∀n∃p∀x(Lxm∨Lxn→Lxp)|=∃B2∀x(LxA∨∃X(LXC∧LxX)→LxB2)' },
    { label: 'log351', formula: '∀m∀n(∀z(Lzm↔Lzn)→m=n),∀z(Lzt↔∃X(LXC∧LzX))|=(x=A∨x=t)↔(x=A∨∀y(Lyx↔∃X(LXC∧LyX)))' },
    { label: 'log353', formula: '∀A∃B1∀x(LxB1↔LxA∧Fx),∃B2∀x(Fx→LxB2)|=∃B1∀x(Fx↔LxB1)' },
    { label: 'log356', formula: '∀x¬s(x)=0,∀x∀y(s(x)=s(y)→x=y),∀x(Ix↔(E(0,x)∧∀z(¬z=s(z)∧(Ezx→E(s(z),x))))),Ia|=¬∃x∃z∃w∀y(Eya↔((y=x∨y=z∨y=w)∧¬x=z∧¬x=w∧¬z=w))' },
    { label: 'log357', formula: '(∀x(Lxf↔Fx)∧Sf)∨(¬∃yLyf∧¬∃B∀x(LxB↔Fx)),(∀x(Lxg↔Gx)∧Sg)∨(¬∃yLyg∧¬∃B∀x(LxB↔Gx)),∀m∀n(∀x(Lxm↔Lxn)→m=n)|=∀x(Fx↔Gx)→f=g' },
    { label: 'log358', formula: '(∀x(Lxf↔Fx))∨(¬∃yLyf∧¬∃B∀x(LxB↔Fx)),(∀x(Lxg↔Gx))∨(¬∃yLyg∧¬∃B∀x(LxB↔Gx)),∀x(Fx↔Gx)|=∀m∀n(∀x(Lxm↔Lxn)→m=n)→f=g' },
    { label: 'log360', formula: '∀X(t(X)=v(A,X)),∀X∀x(Lxv(A,X)↔LxA∧LxX)|=LzA∧∃X(LXC∧LzX)→∃X(∃Y(∀y(LyX↔LyA∧LyY)∧LYC)∧LzX)' },
    { label: 'log361', formula: '∀X∀x(Lxt(X)↔LxA∧LxX)|=LzA∧∃X(LXC∧LzX)→∃X(∃Y(∀y(LyX↔LyA∧LyY)∧LYC)∧LzX)' },
    { label: 'log362', formula: '∀x(∃y(¬x=y∧Fxy∧Fyx)∧∃y(¬x=y∧¬Fxy∧¬Fyx))→∃w∃x∃y∃z¬(w=x∨w=y∨w=z∨x=y∨x=z∨y=z)' },
    { label: 'log363', formula: '∃x∀y(Fy↔y=x),∃x∀y(Gy↔y=x),∃x∀y(Hy↔y=x),∀x((Fx∨Gx)→¬Hx),∀x((Fx∨Hx)→¬Gx)|=∃x∃y∃z∀w((Fw∨Gw∨Hw)↔((w=x∨w=y∨w=z)∧¬(x=y∨y=z∨x=z)))' },
    { label: 'log364', formula: '∀X¬∃Y((∀y(LyY↔LyA∧LyX)∧LXC)∧LzY)→∀X¬(LXC∧LzX)|=∃X(LXC∧LzX)→∃X∃Y((∀y(LyY↔LyA∧LyX)∧LXC)∧LzY)' },
    { label: 'log365', formula: '∀X∀x(Lxv(A,X)↔LxA∧LxX)|=∃X(LXC∧Lzv(A,X))↔∃Y(∃X(∀y(LyY↔LyA∧LyX)∧LXC)∧LzY)' },
    { label: 'log366', formula: '∀X∃b∀x(Lxb↔LxA∧LxX)|=∃X(LXC∧LzA∧LzX)→∃Y(∃X(∀y(LyY↔LyA∧LyX)∧LXC)∧LzY)' },
    { label: 'log367', formula: '∀X∀x(Lxt(X)↔LxA∧LxX)|=∃X(LXC∧LzA∧LzX)→∃Y(∃X(∀y(LyY↔LyA∧LyX)∧LXC)∧LzY)' },
    { label: 'log370', formula: '∀E∃T∀x(IxE→LxT),∀M∀N(IMN↔∀x(LxM→LxN)),∀X∀x(Lxt(X)↔LxA∧LxX)|=∃T∀x(∃X(Ixt(X)∧It(X)x∧LXC)→LxT)' },
    { label: 'log372', formula: '∀M∀z(Lzt(M)↔LzA∧LzM),∀M∀N(∀z(LzM→LzN)↔IMN)|=IxA∧IxX→Ixt(X)' },
    { label: 'log373', formula: '∃YLYC,∀Y∀z(Lzt(Y)↔LzA∨LzY)|=∀X(∃Y(∀y(LyX↔LyA∨LyY)∧LYC)→LxX)∧∃Z∃Y(∀y(LyZ↔LyA∨LyY)∧LYC)→LxA∨(∀X(LXC→LxX)∧∃ZLZC)' },
    { label: 'log375', formula: '∃B1∀y(∃X(LXC∧LyX)→LyB1),∀B1∃B2∀x(∀y(Lyx→LyB1)→LxB2)|=∃B2∀x(∃X(∀y(Lyx↔∀z(Lzy↔LzX))∧LXC)→LxB2)' },
    { label: 'log376', formula: '∃B2∀Y(∀x(LxY→∃X(LXC∧LxX))→LYB2),∀B2∃B3∀Z(∀Y(LYZ→LYB2)→LZB3)|=∃B2∃B3(∀Y(∀x(LxY→∃X(LXC∧LxX))→LYB2)∧∀Z(∀Y(LYZ→LYB2)→LZB3))' },
    { label: 'log377', formula: '∃a∀Y(∀x(LxY→∃X(LXC∧LxX))→LYa),∀a∃b∀Z(∀Y(LYZ→LYa)→LZb)|=∃a∃b(∀Y(∀x(LxY→∃X(LXC∧LxX))→LYa)∧∀Z(∀Y(LYZ→LYa)→LZb))' },
    { label: 'log379', formula: '(Pm∧∀x((Px→¬∀t∀y(Wxyt→Gxyt))∧∃t∀y((Nxyt∧Txyt)→Gxyt))∧∀x∀y∀t(((Nxyt∨Wxyt)∧Gxyt)→Sxyt)∧∀x∀t(∃y(Nxyt∧¬Gxyt)→¬∃ySxyt)∧∀x∀y∃t((Wxyt∨Nxyt)↔Txyt)∧∀x∀y∃t(Sxyt→(Wxyt∨Nxyt))∧∀x∀y∀t((Gxyt∨Nxyt∨Sxyt∨Txyt∨Wxyt)→(Px∧Oy∧Ct))∧∀x¬(Px∧Cx)∧∀x¬(Px∧Ox)∧∀x¬(Cx∧Ox)∧∃tWmht∧∀x∃y∃t(Wxyt∧¬Gxyt))→(∀t∀x¬Smxt)' },
    { label: 'log380', formula: '(Pm∧∀x((Px→¬∀t∀y(Wxyt→Gxyt))∧∃t∀y((Nxyt∧Txyt)→Gxyt))∧∀x∀y∀t((Nxyt∧Gxyt)→Sxyt)∧∀x∀t(∃y(Nxyt∧¬Gxyt)→¬∃ySxyt)∧∀x∀y∃t((Wxyt∨Nxyt)↔Txyt)∧∀x∀y∃t(Sxyt→(Wxyt∨Nxyt))∧∀x∀y∀t((Gxyt∨Nxyt∨Sxyt∨Txyt∨Wxyt)→(Px∧Oy∧Ct))∧∀x¬(Px∧Cx)∧∀x¬(Px∧Ox)∧∀x¬(Cx∧Ox)∧∀x∃y∃t(Wxyt∧¬Gxyt))→(∀t∀x¬Smxt)' },
    { label: 'log381', formula: '∀x∃y∀z(Fxz↔y=z),∀x∀y∀z(Fxz∧Fyz→x=y),∃x(∀y¬Fyx)|=∃x∃y∃z(¬x=y∧¬x=z∧¬y=z)' },
    { label: 'log384', formula: '∀x¬s(x)=0,∀x∀y(s(x)=s(y)→x=y)|=¬∃x∃y∀z(¬x=y∧(z=x∨z=y))' },
    { label: 'log385', formula: '∀X∀y(Lyt(X)↔LyA∧LyX)|=∃X(LXC∧LTA∧LTX)→∃X((∀y(Lyt(X)↔LyA∧LyX)∧LXC)∧LTt(X))' },
    { label: 'log386', formula: '∀M∀x(Lxt(M)↔∀w(Lwx→LwM))|=∀X((∀y(Lyt(X)↔∀w(Lwy→LwX))∧LXC)→LTt(X))→∀X(LXC→LTt(X))' },
    { label: 'log387', formula: '∃XLXC,∀Y(∃X(∀y(LyY↔LyE∧¬LyX)∧LXC)→LTY),∃Y∃X(∀y(LyY↔LyE∧¬LyX)∧LXC),∀M∀x(Lxt(M)↔LxE∧¬LxM)|=∀X(LXC→¬LTX)' },
    { label: 'log388', formula: '(∀x)(∀y)(∀z)((Pxy↔Pyz)→Pxz),(∀x)(∀y)(∀z)((Qxy↔Qyz)→Qxz),(∀x)(∀y)(Qxy→Qyx),(∀x)(∀y)(¬Pxy→Qxy),¬Pab|=Qcd' },
    { label: 'log389', formula: '∀X(∀Y((∀y(LyY↔LyE∧¬LyX)∧LXC)→LTY)∧∀y(Lyt(X)↔LyE∧¬LyX))|=∀X(LXC→¬LTX)' },
    { label: 'log391', formula: '∀x∀y(s(x)=s(y)→x=y),∀x(s(x)=x→∀yy=x),∀x((P(0)∧∀y(Py→P(s(y))))→Px),∀x+(x,0)=x,∀x∀y+(x,s(y))=s(+(x,y)),∀x(Px↔+(0,x)=x)|=Pa' },
    { label: 'log394', formula: '(∀y(Lyx↔(∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b)))∧LaA∧LbB)|=(∀y(Lyx→(∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b)))∧LaA∧LbB)' },
    { label: 'log397', formula: '∃x(∃a∃b(∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b))∧LaA∧LbB)∧LXx)|=∃x(∀y(Lyx→∀z(Lzy→LzA∨LzB))∧LXx)' },
    { label: 'log398', formula: '∀M∀N∀x(Lxu(M,N)↔LxM∨LxN),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=LYA→∃X(∃x(∀y(Lyx→∀z(Lzy→LzA∨LzB))∧LXx)∧LYX)' },
    { label: 'log399', formula: '∃X(∃x(∃a∃b(∀y(Lyx↔∀z(Lzy↔z=a)∨∀z(Lzy↔z=a∨z=b))∧LaA∧LbB)∧LXx)∧LYX)|=∃X(∃x(∀y(Lyx→∀z(Lzy→LzA∨LzB))∧LXx)∧LYX)' },
    { label: 'log405', formula: '∀M∀z(Lzt(M)↔∀y(Lyz→LyM))|=Lxu(A,B)→∃X(∃Y(∀z(LzY→∀w(Lwz→Lwu(A,B)))∧LXY)∧LxX)' },
    { label: 'log408', formula: '∀y∀z((Gy∧Gz)→y=z)↔((¬∃yGy)∨∃y(Gy∧∀z(Gz→z=y)))' },
    { label: 'log410', formula: '∀M∀N∀x(IMN↔∀x(LxM→LxN)),∀m∀x(Lxs(m)↔x=m)|=Is(a)A↔LaA' },
    { label: 'log412', formula: '∀m(s(m)=p(m,m)),∀M∀N∀x(IMN↔∀x(LxM→LxN)),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=Ip(b,c)s(a)→Is(a)p(b,c)' },
    { label: 'log420', formula: '∀M∀z(Lzt(M)↔LzM),∀m∀n(∀x(Lxm↔Lxn)→m=n),∀X(Lt(X)D1↔LXC),∀x(LxD2↔∃X(x=t(X)∧LXC))|=∀y(LyD1↔LyD2)' },
    { label: 'log424', formula: '∀M∀N∀x(Lxd(M,N)↔∃a∃b(LaM∧LbN∧x=o(a,b))),∀a∀b∀m∀n(o(a,b)=o(m,n)↔a=m∧b=n),∀x(Lxd(A,B)↔Lxd(B,A)),∃xLxA∧∃xLxB|=LzA→LzB' },
    { label: 'log425', formula: '∀M∀N∀x(Lxd(M,N)↔∃a∃b(LaM∧LbN∧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: 'log433', formula: '∃s(∀x(Lxs↔x=m)∧∀t(∀x(Lxt↔x=m)→s=t))|=∃s(∀x(Lxs↔x=m)∧(∀x(Lxr↔x=m)→s=r)∧(∀x(Lxk↔x=m)→s=k))' },
    { label: 'log434', formula: '∀t(∀x(Lxt↔x=m)→s=t),∀x(Lxr↔x=m),∀x(Lxk↔x=m)|=r=k' },
    { label: 'log435', formula: '∀m∀n∀x(Lxp(m,n)↔x=m∨x=n),∀k∀x(Lxs(k)↔Lxp(k,k)),∀A∀B(o(A,B)=p(s(A),p(A,B)))|=∀a∀b(∃m∃n(o(a,b)=p(s(m),p(m,n)))→∃k(Ls(k)o(a,b)∧∀r(Ls(r)o(a,b)→s(r)=s(k))))' },
    { label: 'log438', formula: '∀x∀y((Tx∧Ti(x,y))→Ty),∀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,b)→Ti(b,c)→Ta→Tc' },
    { label: 'log439', formula: '∀m∀n∀x(x=m∨x=n↔Lxp(m,n)),∀m(s(m)=p(m,m))|=∃k(s(k)=D)→∃m(LmD∧∀x(LxD→x=m))' },
    { label: 'log440', formula: '∀C∃P∀x(∀y(Lyx→LyC)→LxP)|=∀P∃D∀x(∃X(LXP∧∀w(Lwx↔w=X))→LxD)' },
    { label: 'log441', formula: '∀r∀s(o(a,b)=o(r,s)↔a=r∧b=s)|=(Lo(a,b)d(A,B)↔∃r∃s(LrA∧LsB∧o(a,b)=o(r,s)))→(Lo(a,b)d(A,B)↔∃r∃s(LrA∧LsB∧(a=r∧b=s)))' },
    { label: 'log450', formula: '∀w∀M(Lwt(M)↔LwA∧LwM)|=LxA∧∃X(LXC∧LxX)→∃Y(∃X(∀y(LyY↔LyA∧LyX)∧LXC)∧LxY)' },
    { label: 'log457', formula: '∀X∀Y∀m∀n(Lo(m,n)d(X,Y)↔LmX∧LnY),∀X∀Y∀w(Lwd(X,Y)↔∃m∃n(LmX∧LnY∧w=o(m,n))),∃xLxA|=∀y(Lyd(A,B)→Lyd(A,C))↔∀y(LyB→LyC)' },
    { label: 'log458', formula: '∀X∀Y(IXY↔∀x(LxX→LxY)),∀X∀Y(IXY∧IYX↔X=Y),∀X∀Y∀m∀n(Lo(m,n)d(X,Y)↔LmX∧LnY),∃xLxa,∃xLxb,∃xLxr,∃xLxt|=Id(a,b)d(r,t)→Iar' },
    { label: 'log459', formula: '∀X∀Y(IXY↔∀x(LxX→LxY)),∀X∀Y∀m∀n(Lo(m,n)d(X,Y)↔LmX∧LnY),∀X∀Y∀w(Lwd(X,Y)↔∃m∃n(LmX∧LnY∧w=o(m,n))),∃xLxa,∃xLxb,∃xLxr,∃xLxt|=Id(a,b)d(r,t)→Iar' },
    { label: 'log461', formula: '∀X∀Y∀m∀n(Lo(m,n)d(X,Y)↔LmX∧LnY),∃xLxA,∃xLxB|=∀y(Lyd(A,B)↔Lyd(C,D))→∀z(LzB↔LzD)' },
    { label: 'log463', formula: '∀m∀n∀k(Lkp(m,n)↔k=m∨k=n),∀m∀n(o(m,n)=p(s(m),p(m,n))),∀k(s(k)=p(k,k))|=(∃a∃b(X=o(a,b)∧LaA∧LbB)∧LyX)→(Lxy→LxA∨LxB)' },
    { label: 'log466', formula: '∀m∀n∀k(Lkp(m,n)↔k=m∨k=n),∀k(s(k)=p(k,k))|=s(x)=p(a,b)→(x=a∧x=b)' },
    { label: 'log475', formula: '∀x∀T(LxT↔∀X(LXD→LxX)∧∃XLXD),∀x(LxD→∃M∃N(x=d(M,N)))|=∃M∃N(∀x(Lxd(M,N)→∀X(LXD→LxX)∧∃XLXD))' },
    { label: 'log476', formula: '∀M∀N∀x(Lxv(M,N)↔LxM∧LxN)|=∃M∃N(∀a∀b(LaX∧LbA∧LaY∧LbA↔LaM∧LbN)∧∀x(LxN↔LxA))' },
    { label: 'log477', formula: '∀R∀S∀m∀n(Lo(m,n)d(R,S)↔LmR∧LnS),∀M∀N∀x(Lxv(M,N)↔LxM∧LxN)|=∃M∃N∀x(∃a∃b(x=o(a,b)∧LaM∧LbN)→∃a∃b(x=o(a,b)∧LaA∧LbB)∧∃a∃b(x=o(a,b)∧LaX∧LbY))' },
    { label: 'log478', formula: '∀N∀w(Lwv(A,N)↔LwA∧LwN),∃X(∃Y(∀y(LyX↔Lyv(A,Y))∧LYC)∧LxX)|=∃X(∃Y(∀y(LyX↔LyA∧LyY)∧LYC)∧LxX)' },
    { label: 'log480', formula: '∀N∀m∀n(Lo(m,n)d(A,N)↔LmA∧LnN)|=∀X(LXC→∃a∃b(x=o(a,b)∧LaA∧LbX))∧∃XLXC→∃a∃b(x=o(a,b)∧LaA∧∀X(LXC→LbX))' },
    { label: 'log481', formula: '∀N∀m∀n(Lo(m,n)d↔LmA∧LnN),∃XLXC|=∀X(LXC→∃a∃b(x=o(a,b)∧LaA∧LbX))→∃a∃b(x=o(a,b)∧LaA∧∀X(LXC→LbX))' },
    { label: 'log482', 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∀zTi(i(i(x,y),z),i(n(z),n(y))),∀xTi(x,x),∀x∀y(Ti(x,y)→(Tx→Ty))|=Ti(i(a,b),i(n(b),n(a)))' },
    { label: 'log483', formula: '∀xTi(x,x),∀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∀zTi(i(i(x,y),z),i(n(z),n(y))),∀x∀y(Ti(x,y)→(Tx→Ty))|=Ti(i(a,b),i(n(b),n(a)))' },
    { label: 'log484', formula: '∀x∀yCi(x,y),∀x(C(0)∧∀y(Cy→Cs(y))),∀x∀y(Cx→Ti(x,i(y,x))),∀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∀yTi(n(i(x,x)),y),∀x∀y(Ti(k(x,y),x)∧Ti(k(x,y),y)),∀x∀y(Ti(x,a(x,y))∧Ti(y,a(x,y))),∀x∀y∀zTi(i(x,y),i(i(x,z),i(x,k(y,z)))),∀x∀y∀zTi(i(x,z),i(i(y,z),i(a(x,y),z))),∀x∀y∀zTi(k(x,a(y,z)),a(k(x,y),k(x,z))),∀x∀y(Tx→(Ti(x,y)→Ty))|=Ti(k(p,q),k(q,p))' },
    { label: 'log485', formula: '∀x∀yCi(x,y),∀x(C(0)∧∀y(Cy→Cs(y))),∀x∀y(Cx→Ti(x,i(y,x))),∀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∀yTi(n(i(x,x)),y),∀x∀y(Ti(k(x,y),x)∧Ti(k(x,y),y)),∀x∀y(Ti(x,a(x,y))∧Ti(y,a(x,y))),∀x∀y∀zTi(i(x,y),i(i(x,z),i(x,k(y,z)))),∀x∀y∀zTi(i(x,z),i(i(y,z),i(a(x,y),z))),∀x∀y∀zTi(k(x,a(y,z)),a(k(x,y),k(x,z))),∀x∀y(Tx→(Ti(x,y)→Ty))|=Ti(p,k(p,a(q,n(q))))' },
    { label: 'log486', formula: '∀x(x=0∨∃yx=s(y)),∀x¬s(x)=0,∀x∀y(s(x)=s(y)→x=y),∀x+(x,0)=x,∀x∀y+(x,s(y))=s(+(x,y)),∀x*(x,0)=0,∀x∀y*(x,s(y))=+(*(x,y),x)|=+(a,b)=+(b,a)' },
    { label: 'log488', formula: '∀A(∃xLxA→∃x(LxA∧∀y(Lyx→¬LyA))),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=¬LBB' },
    { label: 'log489', formula: '∀M∀N∀x(Lxv(M,N)↔LxM∧LxN)|=(∃xLxA→∃B(LBA∧¬∃y(Lyv(A,B))))↔(∃xLxA→∃B(LBA∧∀y(LyB→¬LyA)))' },
    { label: 'log490', formula: '∀M∀N∀w(Lwv(M,N)↔LwM∧LwN)|=∀y¬(Lyx∧LyS)↔∀y¬Lyv(x,S)' },
    { label: 'log493', formula: '∀x(x=a→x=s(s(a)))↔∀x(a=s(s(a)))' },
    { label: 'log494', formula: '∀x(Lxs(A)↔x=A),(∃xLxs(A)→∃x(Lxs(A)∧¬∃yLyv(x,s(A)))),∀M∀N∀x(Lxv(M,N)↔LxM∧LxN),(IAs(A)↔∀x(LxA→Lxs(A)))|=∃xLxA↔¬IAs(A)' },
    { label: 'log497', formula: '∀M∀N∀x(Lxv(M,N)↔LxM∧LxN),¬∃xLxe,∀r∀t(∀x(Lxr↔Lxt)→r=t)|=(∃y(Lyw∧Lyd(A,A))→¬LwA)→(LwA→v(w,d(A,A))=e)' },
    { label: 'log499', formula: '∃u1∀y∀X(LXR∧LyX→∃a∃bX=o(a,b)∧Lyu1),∀u1∃u2∀x∀y((Lyu1∧Lxy)→Lxu2)|=∃u1∃u2∀y∀X∀x((LXR∧LyX→∃a∃bX=o(a,b))∧(LXR∧LyX∧Lxy)→Lxu2)' },
    { label: 'log500', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(x=0↔¬x=1)|=c(c(p,0),0)=p' },
    { label: 'log504', formula: '∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=∀y(Lyp(s(a),p(a,b))→¬Lyd(A,A))↔∀y((y=s(a)∨y=p(a,b))→¬Lyd(A,A))' },
    { label: 'log507', formula: '∀x(Lxa→Ixa)∧∀y∀z(Lzy∧Lya→Izy),∀X∀Y(IXY↔∀x(LxX→LxY))|=∀x∀y∀z(Lxz∧Lzy∧Lya→Ixa)' },
    { label: 'log508', formula: 'n2=u(n1,s(n1)),n3=u(n2,s(n2)),∀k∀x(Lxs(k)↔x=k),∀A∀B∀x(Lxu(A,B)↔LxA∨LxB),∀r∀t(∀x(Lxr↔Lxt)→r=t)|=u(n2,n3)=n3' },
    { label: 'log509', formula: 'n3=u(n2,s(n2)),∀k∀x(Lxs(k)↔x=k),∀A∀B∀x(Lxu(A,B)↔LxA∨LxB)|=Lwu(n2,n3)↔Lwn3' },
    { label: 'log511', formula: '(∀x∀y∀z(Mxyz↔(Lyx∧Lxz))∧∀x∀y∀z((Lxy∧Lyz)→Lxz))→∀x∀y∀z∀w((Mxyz∧Mwxz)→Mwyz)' },
    { label: 'log512', formula: '∀B∃t∀x(x=a∨x=b∨LxB→Lxt),∀k∀x(Lxs(k)↔x=k)|=∃t∀x(x=a∨x=b∨x=c→Lxt)' },
    { label: 'log513', formula: '∀k∀x(Lxs(k)↔x=k),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∃t∀x(x=a∨x=b∨x=c→Lxt)' },
    { label: 'log514', formula: '∀k∃s∀x(x=k→Lxs),∀m∀n∃u∀x(Lxm∨Lxn→Lxu)|=∃t∀x(x=a∨x=b→Lxt)' },
    { label: 'log517', formula: '∀A∀B(o(A,B)=p(s(A),p(A,B))),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=∃m∃n(Lmz∧Lnz∧z=p(m,n)∧m=s(a)∧n=p(a,b))→∀x(Lxz↔(x=s(a)∨x=p(a,b)))' },
    { label: 'log518', formula: '∀x(LxU(A)→∃a∃b(x=s(a)∨x=p(a,b))),∀k∀x(Lxs(k)↔x=k),∀m∀n∀x(Lxp(m,n)↔x=m∨x=n)|=∀x(LxU(A)→∃a∃b(x=s(a)∨x=p(a,b)))→∀x(LxU(A)→∃yLyx)' },
    { label: 'log522', formula: '∀M∀N∀x(Lxp(M,N)↔x=M∨x=N)|=∀x(LxU(A)→∃a∃b((Lax∨x=p(a,b))∧LaA∧LbA))→∀x(LxU(A)→∃a∃b((Lax∨(Lax∧Lbx))∧LaA∧LbA))' },
    { label: 'log524', formula: '∀x∀y((x=y)→L(x,y)),∀x∀y(L(x,y)∧L(y,x)→(x=y)),∀x∀y(L(x,y)∨L(y,x)),∀x∀y∀z((L(x,y)∧L(y,z))→L(x,z)),∀x(L(Z,x)),∀x(∀y(L(x,y))→(Z=x)),∀x(¬(f(x)=x)∧L(x,f(x))∧∀z(L(x,z)→(z=x∨L(f(x),z))))|=Laf(f(a))' },
    { label: 'log525', formula: '∀x∀y((x=y)→L(x,y)),∀x∀y(L(x,y)∧L(y,x)→(x=y)),∀x∀y(L(x,y)∨L(y,x)),∀x∀y∀z((L(x,y)∧L(y,z))→L(x,z)),∀x(L(Z,x)),∀x(∀y(L(x,y))→(Z=x)),∀x(¬(f(x)=x)∧L(x,f(x))∧∀z(L(x,z)→(z=x∨L(f(x),z))))|=L(f(Z),f(f(f(Z))))' },
    { label: 'log526', formula: '∀x(W(0)∧(W(x)→W(s(x)))),∀x∀y((Wx∧Wy)→(W(n(x))∧W(k(x,y))∧Wi(x,y)∧W(a(x,y))))|=Ws(s(s(0)))' },
    { label: 'log529', formula: '∀x∀y(Exy→∀z(Rxz→Ryz)),∀x∀y(Exy↔∀z(Rzx↔Rzy)),Eab,Ebc|=Eac' },
    { label: 'log530', formula: '□((p→◇□(p∧q))→(q→◇□(p∧q)))→(□(p→◇□(p∧q))→□(q→◇□(p∧q)))  [reflexivity, transitivity]' },
    { label: 'log534', formula: '∀M∀N∀w(w=M∨w=N↔Lwp(M,N)),∀M∀x(Lxs(M)↔x=M),∀A∀B(∀x(LxA↔LxB)→A=B)|=p(m,m)=s(m)' },
    { label: 'log537', formula: 'LMA,LNA,SMN,∀m∀n(Smn→∃x1(Lx1A∧Rmx1∧Rx1n)),∀x∀y(LxA∧LyA→(Rxy→Ryx))|=∃x1(Lx1A∧Rx1M∧RNx1)' },
    { label: 'log538', formula: '∀M∀N(SMN→∃x1(Lx1A∧RMx1∧Rx1N))|=LmA∧LnA∧LkA∧Smn∧Snk→∃a∃b∃c(LaA∧LbA∧LcA∧Rma∧Rac∧Rcb∧Rbk)' },
    { label: 'log543', formula: '∀M∀N(∀x(LxM↔LxN)→M=N)|=∀x∃y(y=s(x)∧LyA)↔∀x∃y(∀z(Lzy↔Lzs(x))∧LyA)' },
    { label: 'log544', formula: '∀x∃y(∀z(Lzy↔z=x)∧LyA)→∀x∃y∀z((Lzy↔z=x)∧LyA)' },
    { label: 'log545', formula: '(◇∃xGx∨∃xGx↔◇∀x∃y((□Px↔Gy)))∧◇∃xGx∧(◇∀x∃y(□Px↔Gy)→◇∃x□Gx)→∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log546', 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(r1,r3)∨x=o(r3,r2)∨x=o(r1,r2)↔LxR),∀M∀N∀m∀N(o(M,N)=o(s,t)↔M=s∧N=t)|=Lo(r1,r2)C(R,R)' },
    { label: 'log547', formula: 'W(0)∧N(0)∧∀x(Nx→Ws(x)),∀x∀y(Wx→(Wy→Wk(x,y))),∀x∀y(Wx→(Wy→Wi(x,y))),∀x(Wx→Wn(x)),p=s(0)|=Wk(p,p)' },
    { label: 'log549', formula: '∀M∀a∀b(Lo(a,b)T(M)↔Lo(b,a)M),∀M∀N∀a∀b(Lo(a,b)U(M,N)↔Lo(a,b)M∧LaN),∀N∀x(LxR(N)↔∃aLo(a,x)N),∀M∀N(P(M,N)=R(U(M,N))),∀x(LxS↔x=o(1,f)∨x=o(2,f)),∀x(LxA↔x=1)|=LwD(S)∧LwA→LwP(T(S),P(S,A))' },
    { label: 'log551', formula: '∀M∀N∀w(Lwo(M,N)↔Lwp(s(M),p(M,N))),∀M∀N∀w(w=M∨w=N→Lwp(M,N)),∀M∀w(Lws(M)↔w=M)|=∃X∃Y(∃m∃nY=o(m,n)∧LXY∧LxX)→∃X∃Y∃m∃n(Y=o(m,n)∧Ls(m)Y∧Lp(m,n)Y∧LXY∧LxX)' },
    { label: 'log552', formula: 'N(0)∧∀i(N(i)→N(s(i)))→N(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))))))))))' },
    { label: 'log553', formula: '∀x∀yTi(n(i(x,x)),y),∀x∀y((Tx∧Ti(x,y))→Ty),∀x∀y∀zTi(i(x,i(y,z)),i(i(x,y),i(x,z))),∀x∀y∀zTi(i(x,y),i(z,i(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)),∀x∀yTi(i(x,y),i(i(y,x),e(x,y))),∀x∀yTi(e(x,y),i(x,y)),∀x∀yTi(e(x,y),i(y,x))|=Te(p,p)' },
    { label: 'log554', 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∀yTi(n(i(x,x)),y),∀x∀yTi(i(n(i(x,y)),y),i(x,y)),∀x∀y∀zTi(i(i(x,y),z),i(n(z),n(y)))|=Ti(n(p),p)→Tp' },
    { label: 'log556', formula: '∀x∀yTi(x,i(y,x)),∀x∀y∀zTi(i(x,i(y,z)),i(i(x,y),i(x,z))),∀x∀yTi(i(n(y),n(x)),i(x,y)),∀x∀y((Tx∧Ti(x,y))→Ty)|=Ti(p,q)→Ti(q,r)→Ti(p,r)' },
    { label: 'log557', formula: '∀x∀y(c(x,y)=1↔(x=0∨y=1)),∀x(x=0↔¬x=1)|=1=c(c(c(p,0),0),p)' },
    { label: 'log563', formula: '(∀x∀y∀z(□((Ex∧Ey)↔Ez)→x=y))↔(∀x∀y∀z(□(Ez↔(Ex∨Ey))→x=y))  [universality]' },
    { label: 'log579', formula: '∀M∀N∀w(Lwp(M,N)↔w=M∨w=N),∀M∀N(∀w(LwM→LwN)↔I(M,N))|=Ls(a)P(u(A,A))∧Lp(a,a)P(u(A,A))→Ip(s(a),p(a,a))P(u(A,A))' },
    { label: 'log584', formula: '(((P1∧P2∧P3∧Q1∧Q2∧Q3)∨(P1∧P2∧¬P3∧Q1∧Q2)∨(P1∧¬P2∧P3∧Q1∧Q3)∨(P1∧¬P2∧¬P3∧Q1)∨(¬P1∧P2∧P3∧Q2∧Q3)∨(¬P1∧P2∧¬P3∧Q2)∨(¬P1∧¬P2∧P3∧Q3))∨((P4∧Q4))∨(¬P1∧¬P2∧¬P3∧¬P4))↔((((P1→Q1)∧(P2→Q2)∧(P3→Q3))∨((P4→Q4)))∧(¬((P1∨P2∨P3))→(P4→Q4))∧(¬(P4)→((P1→Q1)∧(P2→Q2)∧(P3→Q3))))' },
    { label: 'log585', formula: '∀x(LxR→∃a∃bx=o(a,b)),∀M∀N∀r∀s(o(M,N)=o(r,t)→M=r∧N=s)|=∀w(LwR∧∃a∃b(w=o(a,b)∧Lo(b,a)R)↔∃a(w=o(a,a)∧∃nLo(a,n)R))' },
    { label: 'log587', formula: '∀M∀N∀r∀s(o(M,N)=o(r,t)↔M=r∧N=s)|=(LwR∧∃a∃b(w=o(a,b)∧Lo(b,a)R)→∃a(w=o(a,a)∧∃nLo(a,n)R))' },
    { label: 'log591', formula: '(Lpn∧Lan)→Lrn,(Lpv∧Lan)→Lrv,(Lpn∧Lav)→Lrd,(Lpv∧Lav)→Lrt,Lav↔(Liv∧Lev),Lav↔¬Lie,∀xLxx∧∀x∀y(Lxy↔Lyx)∧∀x∀y∀z∀w((Lxy∧Lzw∧¬Lyw)→¬Lxz)∧¬Lnv∧¬Lnd∧¬Lvd∧¬Lnt∧¬Lvt∧¬Ldt,¬Lid∧¬Lit∧¬Led∧¬Let∧¬Lpd∧¬Lpt∧¬Lad∧¬Lat|=(Liv∧Len)→Lrv' },
    { label: 'log596', formula: '∀x∀y∀zTc(c(x,y),c(z,c(x,y))),∀x∀y∀zTc(c(x,c(y,z)),c(c(x,y),c(x,z))),∀x∀y((Tx∧Tc(x,y))→Ty),∀xTc(x,x),∀xTc(0,x),∀x∀y∀zTc(c(c(x,y),z),c(n(z),n(y))),∀x∀yTc(c(n(c(x,y)),y),c(x,y))|=Tc(c(n(p),p),p)' },
    { label: 'log597', formula: '((∀xQ(a,x,x))∧(∀x∀y∀z(Q(x,y,z)→Q(x,s(y),s(z))))∧(∀x∀y∀z(Q(x,y,z)→Q(y,x,z))))→∃xQ(s(s(a)),s(s(s(a))),x)' },
    { label: 'log599', formula: '∀x∀y□((Ex∧Ey)↔Ef(x,y)),∀x∀y◇(Ex↔Ey)|=∀x∀y∀z□((Ex∧Ey∧Ez)↔Ef(x,f(y,z)))  [universality]' },
    { label: 'log602', formula: '∀x∀y(Kxy↔(□(Ey→Ex)∧◇(¬Ex↔Ey)))|=∀x∀y(Kxy↔(□(Ey→Ex)∧◇(¬Ex↔Ey)))  [universality]' },
    { label: 'log603', formula: '(∃xGx↔((∀x∃y(Gx↔x=y∧(□(Gy→□∃yGy∧□Py))))))→◇¬∃xGx→¬◇∀x∃y(Gx↔(x=y∧□(Gy→(□∃yGy∧□Py))))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log611', formula: '∀x(Rxx)→∀x∀y(Rxy→Ryx)→∀x∀y∀z(Rxy→Ryz→Rxz)→((∀z(Raz↔Rbz))∨(∀z(¬Raz∨¬Rbz)))' },
    { label: 'log612', formula: '(∀x((x=a)↔(∃y((Fy)∧(∀z(Fz↔z=y))∧(x=y)))))→(∃x(Fx∧∀y(Fy↔y=x)))' },
    { label: 'log614', formula: '∀x∀y(Wxy→((Fy∨Py)∧Hx)),∀x(Hx→¬(Fx∨Px)),∀x∀y(Wxy→Bxy),∀x(Cx→(∃y(Sxy∧∃z((Fz↔∀uBuy)∧Wxz)))),∃x(Cx∧∀y(Cy→y=x)),∀x(Cx→¬(Fx∨Px∨Hx)),∃xHx,∃xFx,∃xPx,∀x(Hx→∃yWxy),∀x∀y(Axy→□Wxy)|=∀x∀y((Cx∧Sxy)→∀u∃z((Fz↔Auy)∧Wxz))  [universality]' },
    { label: 'log625', formula: '(∀a∀b∀x∀y(P(S(a,b),S(x,y))↔(a=x∧b=y)∨(a=y∧b=x)))→(∀a∀b∀x∀y(P(S(S(a,a),S(a,b)),S(S(x,x),S(x,y)))↔(a=x∧b=y)))' },
    { label: 'log626', 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)))|=AN(I(a,b))→AI(a,N(b))' },
    { label: 'log639', formula: '∃xEx,∀x(Ex→Cx∨Nx),∀x(Ex∧Cx→∃y(Ey∧Kyx)),(∃x(Ex∧Cx))→(∃x(Ex∧Tx)),(∃x(Ex∧Tx∧∃y(Ey∧Kyx)))→(((∃x(Ex∧Tx∧(∃y(Ey∧Pyx∧Kyx))))∨(∃x(Ex∧Tx∧(∃y(Ey∧Nx∧Kyx)))))),¬(∃x(Ex∧Tx∧((∃y(Ey∧Pyx∧Kyx)))))|=∃x(Ex∧Nx)' },
    { label: 'log642', formula: '∀x∀y(Dx∧Dy→Dc(x,y)),∀x∀y(Dc(x,y)→Dx∧Dy),∀x∀y(Dx∨Dy→Dd(x,y)),∀x∀y∀z(Dd(x,y)∧(Dx→Dz)∧(Dy→Dz)→Dz),∀x∀y((Dx→Dy)→Di(x,y)),∀x∀y(Di(x,y)∧Dx→Dy),∀x∀y((Dx→Dy)∧(Dx→Dn(y))→Dn(x))|=Dd(a,n(a))' },
    { label: 'log645', formula: 'x=y→((p=F(x,z))↔∃t((t=y)∧(p=F(t,z))))' },
    { label: 'log646', formula: '∀m∀n(Lo(m,n)R↔Lo(n,m)c(R)),∀T∀k(LkF(T)↔∃nLo(k,n)T∨∃mLo(m,k)T)|=∀x(LxF(c(R))↔LxF(R))' },
    { label: 'log647', formula: '∀x((Exx∧∀y(Exy→y=x))∨∃y(Exy∧¬y=x)),∀x(Dx↔∀y(Exy→y=x)),∀x∀y(Exy→¬∃z(Exz∧¬z=y)),∀x∀y(¬x=y→∃z(Exz∧Eyz))|=∃xDx' },
    { label: 'log651', formula: '∀x(Lxd(R)↔∃nLo(x,n)R),∀x(Lxr(R)↔∃mLo(m,x)R),∀x(Lxf(R)↔Lxd(R)∨Lxr(R))|=∀z(∃n(Lnf(R)∧Lo(z,n)R)∨∃m(Lmf(R)∧Lo(m,z)R)→LzA)→∀k(Lkf(R)→LkA)' },
    { label: 'log652', formula: '∀x∀y(LxA∧LyA∧Lo(x,y)R→Lo(y,x)R),∀x∀y(LxA∧LyA∧¬x=y∧Lo(x,y)R→¬Lo(y,x)R),∀z(LzA→∃n(LnA∧Lo(z,n)R)∨∃m(LmA∧Lo(m,z)R))|=∀x∀y(LxA∧LyA∧x=y→Lo(x,y)R)' },
    { label: 'log653', formula: '∀x(Lxf(R)↔∃n(Lo(x,n)R)∨∃m(Lo(m,x)R))|=(Lzf(R)↔∃n(Lnf(R)∧Lo(z,n)R)∨∃m(Lmf(R)∧Lo(m,z)R))' },
    { label: 'log654', formula: '∀x(LxA→Lxf(R)),∀x(Lxf(R)↔∃n(Lo(x,n)R)∨∃m(Lo(m,x)R))|=∀x(Lxf(R)↔∃n(Lnf(R)∧Lo(x,n)R)∨∃m(Lmf(R)∧Lo(m,x)R))' },
    { label: 'log656', formula: '∀x∀y(Lxf(R)∧Lyf(R)∧Lo(x,y)R→x=y),∀x(Lxd(R)↔∃nLo(x,n)R),∀x(Lxr(R)↔∃mLo(m,x)R),∀x(Lxf(R)↔Lxd(R)∨Lxr(R))|=∀x(Lxf(R)→Lo(x,x)R)' },
    { label: 'log659', formula: 'Bi,∀x(Bx↔∃y(¬y=x∧Cyx)),∀x(Gx↔¬Bx),∀x∀y(Cxy→¬Cyx),∀x∀y∀z((Cyx∧Czy)→Czx),∀x∃y(Cyx∨Cxy),∀x∀y(Cxy→¬∃z(¬z=x∧Czy))|=∃xGx' },
    { label: 'log663', formula: '∃p∀x(x=a∨x=b→Lxp)∧∀p∀s∃U∀x(Lxp∨Lxs→LxU)|=∃p∀s∃U(∀x(x=a∨x=b→Lxp)∧∀x(Lxp∨Lxs→LxU))' },
    { label: 'log664', formula: '∃T(∀k(LkT→LkA)∧∃kLkT∧∀x(LxT→∃y(LyT∧Lo(y,x)R)))|=∃a∃b∃c(LaA∧LbA∧LcA∧Lo(b,a)R∧Lo(c,b)R)' },
    { label: 'log665', formula: '(∀k(LkT→LkA)∧LmT∧∀x(LxT→∃y(LyT∧Lo(y,x)R))),∀x∀y∀z(LxA∧LyA∧LzA∧Lo(x,y)R∧Lo(y,z)R→Lo(x,z)R)|=∃a∃b∃c(LaA∧LbA∧LcA∧Lo(b,a)R∧Lo(c,b)R∧Lo(c,a)R)' },
    { label: 'log666', formula: '(◇∃x∀y(My∧Gy↔x=y))∧□∀x(Gx∧Mx→□(Gx∧Mx))→□∃x∀y(Gy∧My↔x=y)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log668', formula: '∀k(LkT↔k=a∨k=b∨k=c)|=∀x(LxT→∃y(LyT∧Lo(y,x)R))↔(LaT→∃y(LyT∧Lo(y,a)R))∧(LbT→∃y(LyT∧Lo(y,b)R))∧(LcT→∃y(LyT∧Lo(y,c)R))' },
    { label: 'log669', formula: '◇∃x∀y(My↔x=y)∧∀x(◇Mx→□Mx)→□∃x(Mx∧∀y(□My↔x=y))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log670', formula: '∀x∀y(S(y,x)↔(Lo(x,y)R∧∀z(Lo(x,z)R→y=z∨Lo(y,z)R))),∀X(LXR↔X=o(a,b)),∀M∀N∀m∀n(o(M,N)=o(m,n)→M=m∧N=n)|=S(b,a)' },
    { label: 'log681', formula: '((∀xFxx)∧(∀x∀y(Fxy→Fyx))∧(∀x∀y∀z((Fxy∧Fyz)→Fxz))∧(∃x∃y∃z∀t(Ftx∨Fty∨Ftz)))→(¬(∀x∃y∃z∃t((¬Fxy)∧(¬Fxz)∧(¬Fxt)∧(¬Fyz)∧(¬Fyt)∧(¬Fzt))))' },
    { label: 'log683', formula: '∀x∀y(T*(x,y)↔(Tx∧Ty)),∀x∀y(T+(x,y)↔(Tx∨Ty)),∀x(TN(x)↔¬Tx)|=∀x((∀yT+(N(x),y))↔¬Tx)' },
    { label: 'log685', formula: '□∀x(Ox↔¬Px),□∀x∀y(Vxy→Px∧Oy),∀f(Bf→Pf),∀f∀x(Pf∧Ox→(Vfx↔¬Vn(f)x)),∀f(Pf→n(n(f))=f),∀f∀p(Pf∧Pp→(Bf∧□∀x(Vfx→Vpx)→Bp)),∀f(Bn(f)↔¬Bf)|=∀f(Bf→◇∃xVfx)  [reflexivity]' },
    { label: 'log692', formula: '□(EU↔∃x(Ex∧◇¬Ex)),∀x∀y◇(Ex↔Ey),∀x∀y(□(Ex↔Ey)→x=y),□∃xEx|=∃x□Ex  [universality]' },
    { label: 'log696', formula: '¬(∃y(Lo(a,y)R∧∀z(Lo(a,z)R∧¬y=z→Lo(y,z)R))),∀m∀n(LmA∧LnA→(¬m=n→Lo(m,n)R∨Lo(n,m)R)),∀k(Lkf(R)→LkA),∀k(Lkf(R)↔∃nLo(k,n)R∨∃mLo(m,k)R),LaA,¬(LaA∧∀y(LyA∧¬y=a→Lo(y,a)R))|=∃b(Lo(a,b)R∧¬a=b∧LbA∧∃z(Lo(a,z)R∧¬b=z∧Lo(z,b)R∧¬a=z))' },
    { label: 'log697', formula: '¬(∃y(Lo(a,y)R∧∀z(Lo(a,z)R∧¬y=z→Lo(y,z)R))),∀m∀n(LmA∧LnA→(¬m=n→Lo(m,n)R∨Lo(n,m)R)),∀k(Lkf(R)→LkA),∀k(Lkf(R)↔∃nLo(k,n)R∨∃mLo(m,k)R),LaA,¬(LaA∧∀y(LyA∧¬y=a→Lo(y,a)R))|=∃b∃c(Lo(a,b)R∧Lo(a,c)R∧Lo(c,b)R∧¬a=b∧¬b=c∧¬a=c)' },
    { label: 'log698', formula: '∀x∀y∀z((Rxy∧Rxz)→y=z),∀x(Dx→∃y(Fy∧Rxy))|=(∀x∀y(Rxy↔Syx)∧∀x(Fx→∃y(Dy∧Sxy))∧∀x∀y∀z((Sxy∧Sxz)→y=z))→∀y(Fy→∀x∀z((Rxy∧Rzy)→x=z))' },
    { label: 'log699', formula: '□(∃xNx↔∃x∀y(Nx↔y=x)∧(∃y∃z¬(Ny∧y=z)))→¬◇∃x∃y(Nx∧x=y)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log706', formula: '□Ed1,□Ed2,∀x(x=d1∨x=d2∨x=U),EU∧◇¬EU|=∀x∀y∃z□(Ez↔Ex∨Ey)  [universality]' },
    { label: 'log711', formula: '∀m∀n∃p∀x(Lxp↔x=m∨x=n),LaA∧LbA,Lo(a,b)R|=∃t(∀x(Lxt→x=a∨x=b)∧∀x(x=a∨x=b→Lxt)∧∀x(Lxt→LxA)∧∃kLkt∧Lo(a,b)R∧LaA∧LbA)' },
    { label: 'log714', formula: '|=◇◇□□◇◇A↔◇A  [reflexivity, symmetry, transitivity]' },
    { label: 'log721', formula: '□∃x∀y(Gy↔x=y)→(◇∃xGx∧□(∃xGx→□∃x∀y(Gy↔x=y)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log722', formula: '□∃x∀y(Gy↔x=y)→(◇∃x∀y(Gy↔x=y)∧(◇∃x∀y(Gy↔x=y)→□∃x∀y(Gy↔x=y)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log724', formula: '∀x∀y(Lo(x,y)R∧¬(x=y∧(∃nLo(x,n)R∨∃mLo(m,x)R))↔Lo(x,y)r)|=(∀a(LaA→Lo(a,a)R)∧∀a∀b(LaA∧LbA∧Lo(a,b)R∧Lo(b,a)R→a=b))→(∀a∀b(LaA∧LbA∧Lo(a,b)r→¬Lo(b,a)r))' },
    { label: 'log725', formula: '∀x(LxF(R)↔(∃nLo(x,n)R∨∃mLo(m,x)R)),∀x(LxF(r)→(∃nLo(x,n)r∨∃mLo(m,x)r)),∀x∀y(Lo(x,y)R∧¬(x=y∧(∃nLo(x,n)R∨∃mLo(m,x)R))↔Lo(x,y)r)|=(∀a(LaF(R)→Lo(a,a)R)∧∀a∀b(LaF(R)∧LbF(R)∧Lo(a,b)R∧Lo(b,a)R→a=b))→(∀a∀b(LaF(R)∧LbF(R)∧Lo(a,b)r→¬Lo(b,a)r))' },
    { label: 'log726', formula: '∀k(LkA→k=a∨k=b∨k=c),∀K(K=o(a,a)∨K=o(a,b)∨K=o(a,c)∨K=o(b,b)∨K=o(b,c)∨K=o(c,c)→LKR),LmA∧LnA|=∃y(LyA∧Lo(m,y)R∧Lo(n,y)R∧∀x(Lo(m,x)R∧Lo(n,x)R→Lo(y,x)R))' },
    { label: 'log728', formula: '∀k(LkA↔k=a∨k=b∨k=c),∀K(K=o(a,a)∨K=o(a,b)∨K=o(a,c)∨K=o(b,b)∨K=o(b,c)∨K=o(c,c)→LKR)|=m=a∧n=b→∃y(LyA∧Lo(m,y)R∧Lo(n,y)R∧∀x(Lo(m,x)R∧Lo(n,x)R→Lo(y,x)R))' },
    { label: 'log730', formula: '(∀x(◇◇Px→◇Qx))→□◇(∀x(◇◇Px→◇Qx))  [symmetry, transitivity]' },
    { label: 'log731', formula: '(∀x(□Px→□□Qx))→□◇(∀x(□Px→□□Qx))  [symmetry, transitivity]' },
    { label: 'log734', formula: '∀x∀y□(Ep(x,y)↔Ex∧Ey),∀x∀y(□(Ex↔Ey)→x=y),□ED,D=p(A,B)|=D=A∧D=B  [universality]' },
    { label: 'log736', formula: '□((□∀x(Gx→□Gx)↔∃x∀y(Gy↔x=y)))∧◇∃x∀y(Gy↔x=y)→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log737', formula: '(□((∃xGx∧□∀x(Gx→□Gx)↔∃x∀y(Gy↔x=y)))∧◇∃x∀y(Gy↔x=y))→∃x□Gx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log739', formula: '(□(∃x∀y(Gy↔x=y)↔(□∃xGx∧□∀x(Gx→□Gx)))∧◇∃x∀y(Gy↔x=y))→∃x□Gx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log740', formula: '□((∃x∀y(Gy↔x=y)↔(∃xGx∧□∀x(Gx→□Gx))))∧◇∃x∀y(□Gy↔x=y)→∃x∀y(□Gy↔x=y)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log742', formula: '∀x∀y(Gxy↔□(Cxy→¬Mxx)),∀x∀y(Gxy→◇Cxy),∀x(¬◇Fx→(□Mxx∨∃y(Py∧Dxy))),□∀x(Fx↔¬Sx),□∀x(¬Sx→¬Ax),□Aj,∀x(Px↔∃y□Dyx),∀x¬∃y□Dxy,∀x∃y◇Dxy|=¬∃xPx∧□Mjj' },
    { label: 'log749', formula: '∀y(Lyr1(m)↔Lo(m,y)R1),∀B(∃x(B=r1(x)∧∃kLkB)→∃y(B=r2(y)∧∃kLkB)),∀k(LkF(R1)↔∃bLo(k,b)R1∨∃aLo(a,k)R1),∀x(LxF(R1)→Lo(x,x)R1),∀x∀y(Lyr2(x)↔Lo(x,y)R2),∀x∀y(Lo(x,y)R2↔r2(x)=r2(y))|=Lo(m,n)R1→Lo(m,n)R2' },
    { label: 'log750', formula: '∀y(Lyr1(m)↔Lo(m,y)R1),∀B(∃x(B=r1(x)∧∃kLkB)↔∃y(B=r2(y)∧∃kLkB)),∀x(LxF(R1)→Lo(x,x)R1),∀x∀y(Lyr2(x)↔Lo(x,y)R2),∀x∀y(Lo(x,y)R2↔r2(x)=r2(y))|=∀k(LkF(R1)↔∃bLo(k,b)R1∨∃aLo(a,k)R1)→(Lo(m,n)R1→Lo(m,n)R2)' },
    { label: 'log753', formula: '∀w1∀x(S(w1,x)→H(w1,x))∧∀w1(D(w,w1)→(∀x((H(w,x))↔(H(w1,x))))∧∀x((H(w,x)∧(G(w,x))↔(H(w1,x)∧G(w1,x)))))∧∀w1(D(w,w1)→(∀x((H(w,x))↔(H(w1,x))))∧∀x((H(w,x)∧(S(w,x))↔(H(w1,x)∧S(w1,x)))))→∀w1(D(w,w1)→(∀x((S(w,x))↔(S(w1,x))))∧∀x((S(w,x)∧(G(w,x))↔(S(w1,x)∧G(w1,x)))))' },
    { label: 'log756', formula: '∀x(Lxf(R0)↔∃nLo(x,n)R0∨∃mLo(m,x)R0),(Laf(R0)→Lo(a,a)R0),(Lau(T)↔∃B(LaB∧LBT)),∀y(Lyr0(a)↔Lo(a,y)R0),∀B(LBT↔∃x(∀y(LyB↔Lo(x,y)R0)∧∃yLyB))|=Laf(R0)↔Lau(T)' },
    { label: 'log758', formula: '∀z∃A∀x(Fxz→LxA),∀z∀A∃B∀x(LxB↔LxA∧Fxz)|=∀z∀A∃B∀x(LxB↔Fxz)' },
    { label: 'log760', formula: '□∀x(Px↔(Hx∧□¬Bx)),□∀x∀y(Qxy↔∃z((Fxz→◇By)∧Fxz)),□(I↔¬∃xPx),□∀x∀y(Dxy↔(◇Bx↔∃zFzy)),□∀x(Kx↔(Hx∧¬◇∃yQxy)),□∀x((Hx∧¬Bx)↔∃y(Ry∧Sxy)),□∀x((Hx∧Bx)↔∃y(Gy∧Sxy)),□∀x∀y(Fxy→(Hx∧Ay)),□∀x(Hx→¬Ax),□∀x∀y(Dxy→(Hx∧Ay)),□∃x∃y((Hx∧Hy)∧¬x=y),∀x(Hx→◇∃yDxy),□∀x∀y(Sxy→(Hx∧Ey)),□∀x(Hx→¬Ex),□∀x((Gx∨Rx)→Ex)|=∀x(□∃yQyx→¬◇Px)  [transitivity]' },
    { label: 'log763', formula: '|=∀x∀f∀b(F(f,a)=b↔((Ta∧Lo(a,b)f)∨(¬Ta∧b=0)))↔∀x∀f∀b((Ta→(F(f,a)=b↔Lo(a,b)f))∧(¬Ta→F(f,a)=0))' },
    { label: 'log764', formula: '∀F∀x(Tx↔∃z(Lo(x,z)F∧∀y(Lo(x,y)F→z=y)))→∀f∀a(Ta↔∃b(Lo(a,b)f∧∀c(Lo(a,c)f→c=b)))' },
    { label: 'log765', formula: '∀x∀y∀z((Rxy∧Ryz)→Rxz),(∀x∀y(Rxy↔Ryx)),(∀x∀y(Pxy→x=y)),(¬Pfs∧(¬Pfh∧(¬Phs∧(Pff∧(Pss∧(Phh∧(∀x(Hx↔(Pfx∨(Psx∨Phx)))))))))),(∃x((Gx∧Tx)∧∀y((Gy∧Ty)→Ryx))),G(f)∧G(s)∧G(h)∧¬Tf∧¬Th∧¬Ts|=∃x(G(x)∧¬H(x))' },
    { label: 'log767', formula: '(□(∀x∃y∀z((Gx↔x=y)↔□(Gz→z=y))))∧◇(∃x∀y(Gy↔x=y))→∃x∀y(Gy↔x=y)  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log768', formula: '((□(∀x∃y∀z((Gx↔x=y)↔□(Gz→z=y))))∧◇(∃x∀y(Gy↔x=y)))→(□(∃x∀y(Gy↔x=y)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log769', formula: '((□∀z∃y(Gz↔(z=y↔□(Gz→z=y))))∧((◇∃x∀y(Gy↔x=y))))→((∃x∀y□(Gy↔x=y)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log770', formula: '□(∃x∀y((Gy↔x=y)↔□(Gx→x=z)))→□∃xGx  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log771', formula: '□∀x∃y∀z(□(Gz→z=y)↔((Gx↔x=y)))∧∃x□Gx→((∃x∀y(Gy↔x=y)))  [universality, reflexivity, symmetry, transitivity, euclidity, seriality]' },
    { label: 'log772', formula: '∀a∀b(Las(b)↔a=b)|=(∃XLXC∧(∃Y(LYC∧¬LYs(e))∨∃Z(¬LZC∧LZs(e)))→∃xLxU(C))↔(∃XLXC∧(∃Y(LYC∧¬Y=e)∨∃Z(¬LZC∧Z=e))→∃xLxU(C))' },
    { label: 'log773', formula: '∀x(Tx↔(Rx∧∃y(o(x)=y))),∀x(Fx↔(Rx∧¬∃y(o(x)=y))),∀x(Zx→Rx),∀x(Lx↔(Zx∧Fx)),∀x(Ex↔(Zx∧o(x)=f)),∀x(Px↔(Zx∧o(x)=n)),∀x(∃yb(x)=y→Rx),∀x(Xb(x)↔¬Ax),∀x(Lx→Ax),∀x(Mx↔((Zx∧Ax)∧∃yo(x)=y))|=∀x((Zx∧(¬Xb(x)∧o(x)=f))→(Mx∧Ex))' },
    { label: 'log777', formula: '∀x¬F(xx)∧∀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))))→∀x∀y(F(xy)↔x=y)∨∀x∀y(¬F(xy)↔x=y)' },
    { label: 'log778', formula: '∀x¬F(xx)∧∀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))))→∀x∀y(¬F(xy)↔x=y)' },
    { label: 'log779', formula: '∀x∃yy=n(x),∀x(Vx↔Fn(x)),∀x(Vx↔¬Fx),∀x∀y(Vi(x,y)↔(Fx∨Vy)),∀x∀y(Vc(x,y)↔(Vx∧Vy)),∀x∀y(Vd(x,y)↔(Vx∨Vy))|=∀xVn(n(i(x,x)))' },
    { label: 'log780', formula: '∀x∀w(Tl(n(x),w)↔¬Tl(x,w)),∀x∀y∀w(Tl(c(x,y),w)↔(Tl(x,w)∧Tl(y,w))),∀x∀y∀w(Tl(d(x,y),w)↔(Tl(x,w)∨Tl(y,w))),∀x∀y∀w(Tl(i(x,y),w)↔(¬Tl(x,w)∨Tl(y,w))),∀x∀y∀w(Tl(b(x,y),w)↔(Tl(x,w)↔Tl(y,w))),∀x∀w∀z(Tl(e(x),w)↔(Rwz→Tl(x,z))),∀x∀w∃z(Tl(p(x),w)↔(Rwz∧Tl(x,z)))|=(Tl(i(h,j),m)∧Tl(i(j,q),m))→Tl(i(h,q)m)' },
    { label: 'log781', formula: '□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□□((∀x(Z(x)↔∀y(¬R(y,x))))∧(∃x(Z(x)))∧(∀x¬(R(x,x)))→(∀x∀y(A(x)→R(y,x)→A(y)))∧(A(c))→((∀y(¬R(y,c)))↔(∀y(A(y)→¬R(y,c)))))  [euclidity]' },
    { label: 'log782', formula: '∀x∀y□(Ef(x,y)↔Ex∨Ey),∀x∀y□(Kxy↔□(Ey→Ex)∧¬□(Ex→Ey))|=□(Ef(a,b)↔Ef(b,a))  [universality]' },
    { label: 'log783', formula: '∀x(LxA↔x=k)|=∀M∀N(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→∀M∀N(M=k∧N=k→∃y(y=k∧Lo(k,k)R∧Lo(k,k)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(k,z)R)))' },
    { label: 'log784', formula: '∀x(LxA↔x=k)|=(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→(M=k∧N=k→∃y(y=k∧Lo(k,k)R∧Lo(k,k)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(k,z)R)))' },
    { label: 'log785', formula: '∀m∃s∀x(x=m→Lxs),∀m∀n∃p∀x(x=m∨x=n→Lxp),∀C∃U∀x(∃X(LXC∧LxX)→LxU)|=∃t∀x(x=a∨x=b∨x=c→Lxt)' },
    { label: 'log786', formula: '∀x(LxX↔x=a∨x=b),∀x(LxX→Lo(x,x)R)|=∀x∀y∀z(LxX∧LyX∧LzX→(Lo(x,y)R∧Lo(y,z)R→Lo(x,z)R))' },
    { label: 'log787', formula: '∀X(LXR→X=o(a,b)),¬a=b,∀x(LxB↔x=a∨x=b),∀M∀N∀m∀n(o(M,N)=o(m,n)→M=m∧N=n)|=(LrB∧LsB∧LtB→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R))' },
    { label: 'log790', formula: '¬a=b,∀M∀N∀m∀n(o(M,N)=o(m,n)→M=m∧N=n),∀X(LXR↔X=o(a,b)∨X=o(b,b))|=(r=a∧s=b∧t=a)→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)' },
    { label: 'log791', formula: '¬a=b,∀M∀N∀m∀n(o(M,N)=o(m,n)→M=m∧N=n),∀X(LXR↔X=o(b,b)∨X=o(b,a))|=(r=a∧s=b∧t=a)→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)' },
    { label: 'log796', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧M(x)∧x=o)),∃fH(f)∧∀f∀e(H(f)∧V(e)→¬∃x∃y(M(x)∧M(y)∧P(e,x)∧P(f,y)∧S(x,y))),∀e(V(e)→∃f(H(f)∧U(e,f)))|=¬(∀e∀f(U(e,f)→∃x∃y(M(x)∧M(y)∧P(e,x)∧P(f,y)∧S(x,y))))' },
    { label: 'log797', formula: '∀x(LxA→Lo(x,x)R),∀x(x=m∨x=n↔LxA)|=((LkA∧Lo(m,k)R∧Lo(n,k)R∧∀z(Lo(m,z)R∧Lo(n,z)R→Lo(k,z)R)))→(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))' },
    { label: 'log798', formula: '∀x(x=m∨x=n→LxA)|=∀M∀N(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→∃y(LyA∧Lo(m,y)R∧Lo(m,y)R∧∀z(Lo(m,z)R∧Lo(m,z)R→Lo(y,z)R))' },
    { label: 'log799', formula: '∀x(x=m∨x=n→LxA)|=∀M∀N(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→∃y(LyA∧Lo(m,y)R∧Lo(n,y)R∧∀z(Lo(m,z)R∧Lo(n,z)R→Lo(y,z)R))' },
    { label: 'log800', formula: '∀x(x=m∨x=n↔LxA)|=∀M∀N(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→∃y(LyA∧∀x(LxA→Lo(x,y)R))' },
    { label: 'log801', formula: '∃m∀x(x=m↔LxA)|=∀M∀N(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→∃y(LyA∧∀x(LxA→Lo(x,y)R))' },
    { label: 'log803', formula: '∀x∀y∀z(Lo(x,y)f∧Lo(x,z)f→y=z),∀x∀y∀z(Lo(x,y)g∧Lo(x,z)g→y=z),∀k∀h∀a∀b(Lo(a,b)r1(k,h)↔∃c(Lo(a,c)k∧Lo(c,b)h))|=∀x∀y∀z(Lo(x,y)r1(g,f)∧Lo(x,z)r1(g,f)→y=z)' },
    { label: 'log804', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧M(x)∧x=o)),∃fH(f)∧∀f∀e(H(f)∧V(e)→¬∃x∃y(M(x)∧P(e,x)∧P(f,y)∧S(x,y))),∀e∀f(U(e,f)→∃x∃y(M(x)∧P(e,x)∧P(f,y)∧S(x,y)))|=¬(∀e(V(e)→∃f(H(f)∧U(e,f))))' },
    { label: 'log805', formula: '∃fH(f)∧∀f∀y((H(f)∧P(f,y))→(¬(y=o)∧¬S(o,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)))),∀e∀x∀z((P(e,x)∧P(e,z))→x=z)|=¬(∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)))' },
    { label: 'log806', formula: '∃fH(f)∧∀f(H(f)→(∀y(P(f,y)→¬(y=o))∧∀c((∃g(V(g)∧P(g,c)∧S(c,o)))→∀y(P(f,y)→¬(y=c))))),∀e(V(e)→∃f(H(f)∧U(e,f)∧P(f,o))),∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,y)))),∀e∀x∀z((P(e,x)∧P(e,z))→x=z)|=¬(∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)))' },
    { label: 'log808', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∃fH(f)∧∀f∀e(H(f)∧V(e)→∀x∀y(P(e,x)∧(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: 'log809', formula: '∀h∀a(Tah↔∃b(Lo(a,b)h∧∀c(Lo(a,c)h→c=b))),∀a∀b∀c(Lo(a,b)f∧Lo(a,c)f→b=c)|=Lo(x,y)f↔Txf∧Lo(x,y)f' },
    { label: 'log810', formula: '∀a(Lad(f)↔∃bLo(a,b)f),d(f)=d(g),∀a(Lad(g)↔∃bLo(a,b)g),∀a∀b∀c(Lo(a,b)g∧Lo(a,c)g→b=c),∀a(Tag↔∃b(Lo(a,b)g∧∀c(Lo(a,c)g→c=b)))|=∀a∀b(Taf∧Lo(a,b)f∧¬Tag→b=e)' },
    { label: 'log811', formula: '∀a(Lad(f)↔∃bLo(a,b)f),d(f)=d(g),∀a(Lad(g)↔∃bLo(a,b)g),∀a∀b∀c(Lo(a,b)g∧Lo(a,c)g→b=c),∀a(Tag↔∃b(Lo(a,b)g∧∀c(Lo(a,c)g→c=b))),∀a(Taf↔∃b(Lo(a,b)f∧∀c(Lo(a,c)f→c=b)))|=∀a∀b(¬Tag∧b=e∧¬Lo(a,b)f→¬Taf)' },
    { label: 'log812', formula: '∀a(Lad(f)↔∃bLo(a,b)f),d(f)=d(g),∀a(Lad(g)↔∃bLo(a,b)g),∀a∀b∀c(Lo(a,b)g∧Lo(a,c)g→b=c),∀a(Tag↔∃b(Lo(a,b)g∧∀c(Lo(a,c)g→c=b))),∀a(Taf↔∃b(Lo(a,b)f∧∀c(Lo(a,c)f→c=b)))|=(¬Txg∧y=e∧¬Lo(x,y)f→¬Txf)' },
    { label: 'log814', formula: '□∃x∀y(Fy↔x=y),□∀y(Fy→□(∀x((□(Fy→Ex)→Ex)∧(□(Fy→¬Ex)→¬Ex))→Fy)),□∀x∃y(Fx↔Ey),∀x∀y∃z□(Ez↔Ex∨Ey)|=∀x∃y(◇¬Ex→□(Ex→Ey)∧¬□(Ey→Ex))  [universality]' },
    { label: 'log815', formula: '□∃x∀y(Fy↔x=y),□∀x∀y(Ex∧Fy→□(Fy→Ex)),□∀x∀y(¬Ex∧Fy→□(Fy→¬Ex)),□∀x∃y(Fx↔Ey),∀x∀y∃z□(Ez↔Ex∨Ey)|=∀x∃y(◇¬Ex→□(Ex→Ey)∧¬□(Ey→Ex))  [universality]' },
    { label: 'log817', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∀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))))|=¬(∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y((x=o∨S(x,y))→¬P(f,y))))' },
    { label: 'log818', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y((x=o∨S(o,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: 'log819', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∀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))))|=¬(∃fH(f)∧∀f∀e(V(e)∧H(f)→∀x∀y((x=o∨S(o,y))→¬P(f,y))))' },
    { label: 'log820', formula: '∃fH(f)∧∀f(H(f)→∀y((y=o∨S(o,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)))),∀e∀x∀z((P(e,x)∧P(e,z))→x=z)|=¬(∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)))' },
    { label: 'log822', formula: '∃x(∃y(Syx)∧∀z(Szx→∃w(Swx∧¬w=z∧∀v(Svw↔(Svz∨v=z)))))∧(∀x(∃ySyx→(∃z(Szx∧(∀w¬(Swz∧Swx))))))→∃x(∃y(Syx)∧∀z(Szx→∃w(Swx∧¬w=z∧∀v(Svw↔(Svz∨v=z)))))∧(∀x(∃ySyx→(∃z(Szx∧(∀w¬(Swz∧Swx))))))' },
    { label: 'log825', formula: '∃eV(e)∧∀e(V(e)→∃x(P(e,x)∧x=o)),∃fH(f)∧∀f∀e∀g((V(e)∧V(g)∧H(f))→(∀y((P(e,o)∧P(g,p)∧S(o,p)∧(y=o∨y=p))→¬P(f,y))∧∀x(P(f,x)→(¬(x=o)∧¬(x=p)))∧¬∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(x,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: 'log828', formula: '∀m∃s∀x(Lxs↔x=m)|=∀B(∃x(LxB∧∀y(LyB→y=x))∧∀x(LxB→LxA)→∀x(LxB→Lo(x,x)R))→(LbA→∀x(x=b→Lo(x,x)R))' },
    { label: 'log830', formula: '∀a(LaA→Lo(a,a)R),∀a∀b(LaA∧LbA→(Lo(a,b)R∧Lo(b,a)R→a=b))|=(LMA∧LNA→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))→(LMA∧LNA∧¬M=N→∃y(LyA∧Lo(M,y)R∧Lo(N,y)R∧∀z(Lo(M,z)R∧Lo(N,z)R→Lo(y,z)R)))' },
    { label: 'log838', formula: '∃eV(e)∧∀e(V(e)→∀x(P(e,x)→(M(x)∧x=o))),∃fH(f)∧∀f∀y(H(f)→(P(f,y)→(¬(o=y)∧(¬S(o,y)∨¬M(y))))),∀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)))|=¬(∀e(V(e)→∃f(H(f)∧U(e,f))))' },
    { label: 'log839', formula: '∀r∀s∀t(LrA∧LsA∧LtA→(Lo(r,s)R∧Lo(s,t)R→Lo(r,t)R)),∀r∀s(LrA∧LsA→(Lo(r,s)R∧Lo(s,r)R→r=s))|=LaA∧LbA∧LcA→(LmA∧Lo(m,b)R∧Lo(m,c)R∧∀k(Lo(k,b)R∧Lo(k,c)R→Lo(k,m)R)∧LnA∧Lo(n,a)R∧Lo(n,m)R∧∀k(Lo(k,a)R∧Lo(k,m)R→Lo(k,n)R)∧LhA∧Lo(h,a)R∧Lo(h,b)R∧∀k(Lo(k,a)R∧Lo(k,b)R→Lo(k,h)R)∧LgA∧Lo(g,h)R∧Lo(g,c)R∧∀k(Lo(k,h)R∧Lo(k,c)R→Lo(k,g)R)→n=g)' },
    { label: 'log840', formula: '∀M∀N∀x(Lxu(M,N)↔LxM∨LxN),∀h∀X(r1(h,X)↔∀a(LaX→Lo(a,a)h)),r1(R,A),r1(R,B)|=r1(R,u(A,B))' },
    { label: 'log842', formula: '(∀x(Fx↔x=A)∨(¬∃y∀x(Fx↔x=y)∧A=N))↔∀y(∀x(Fx↔x=y)→y=A)∧(¬∃y∀x(Fx↔x=y)→A=N)' },
    { label: 'log847', formula: '∀x(□Ex→x=d),∀x(◇¬Ex↔∃y(□Ey∧Dyx)),∀x(Hx→∃y(□Ey∧Dyx)),Hl∧Hj,∀x(∃yDyx→Nx),∀x(◇¬Ex→Rx),∀x((Rx∧Nx)→Ax)|=Aj∧Al' },
    { label: 'log848', formula: '∀x∀y∀z(Pxo(y)↔(Pzy→e(x,z)=a)),∀x∀y∀z(Cxy↔(Pzx→Pzy)),∀x∀y∀z(Pxi(y,z)↔(Pxy∧Pxz))|=Ci(o(m),o(n))o(i(m,n))' },
    { label: 'log858', formula: '□∀x∀y(Mxy↔□(Txy→◇Rx)),□∀x(Rx↔Ra(x)),□∀x(a(e(x))=v(x)),□∀x(◇Re(x)↔∃yFxy),□∀x((Fjx→◇∃y(Axy∧¬Bx))→¬Fjx),□∀x∀y(Fxy→◇∃zAyz),□∀x(∃yFyx→Ix),□¬Iw,∀x□∀y((Axy→By)→x=w),□∀xTxv(x),□∀x(Re(x)→◇∃yFxy)|=□¬Re(j)  [universality]' },
    { label: 'log859', formula: '□∀x∀y(Mxy↔□(Txy→◇Ry)),□∀x(Rx↔Ra(x)),□∀x(a(e(x))=v(x)),□∀x(◇Re(x)↔∃yFxy),□∀xTxv(x),□¬Re(j)|=□¬Mjv(j)  [universality]' },
    { label: 'log860', formula: '∀m∀n(Lms(n)↔m=n),∀M∀N(∀k(LkM↔LkN)→M=N)|=LxX∧∀y(LyX→y=x)→X=s(x)' },
    { label: 'log861', formula: '∀F(Q↔∃z(Lo(x,z)F∧∀y(Lo(x,y)F→z=y)))|=∀F∀y(f(x)=y↔((Q∧Lo(x,y)F)∨(¬Q∧y=0)))↔∀F∀y((Q→(f(x)=y↔Lo(x,y)F))∧(¬Q→f(x)=0))' },
    { label: 'log862', formula: '∀x5(Lx5P2↔∀x6(Lx6x5→Lx6P1))∧∀x3(Lx3P1↔∀x4(Lx4x3→Lx4A∨Lx4B))|=∀x5(∀x6(Lx6x5→∀x4(Lx4x6→Lx4A∨Lx4B))→Lx5P2)' },
    { label: 'log864', formula: '∀a(Lad(f)↔∃bLo(a,b)f),∀b(Lbr(f)↔∃aLo(a,b)f),∀a∀b∀c(Lo(a,b)f∧Lo(a,c)f→b=c)|=Lxd(f)∧∀y(Lyd(f)→y=x)→∃v(Lvr(f)∧∀w(Lwr(f)→w=v))' },
    { label: 'log869', formula: '□∀x∀y(∃zFxyz→(¬Ex∧Ey)),□∀x(Nx→Ex),□∀x(∃y¬Axy→◇∃z(Nz∧∃uFxzu)),□∀x(¬Ex→∃y∃zFxyz)|=□∀x(◇□∀y(∃zFxyz→¬Ny)→◇□∀y(∃zFxyz→Axy))  [transitivity]' },
    { label: 'log875', formula: '∀x(x=a),∀x∀y(□(Ex↔Ey)→x=y),∀x¬(□(Ea→Ex)∧¬□(Ex→Ea)),∀x∀y∃z□(Ez↔Ex∨Ey),◇∃xEx|=◇∀x(Ex↔x=a)  [universality]' },
    { label: 'log876', formula: '∀w(P(a,b)=w↔∀y(Lyw↔y=a∨y=b))|=∃r(∀y(Lyr↔y=a∨y=b)∧Lar)' },
    { label: 'log877', formula: '∀w(S(P(a,a))=w↔((Lo(a,a)R∧Lo(a,a)R→a=a)∧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↔((Lo(a,a)R∧Lo(a,a)R→a=a)∧Lo(a,a)R∧∀y(Lo(a,y)R→Lo(a,y)R)∧∀z(Lo(a,z)R∧∀y(Lo(a,y)R→Lo(z,y)R)→z=a)))' },
    { label: 'log878', formula: '□∀x(◇¬Dxv(x)→Mxx),(◇Aj∧◇Bj∧◇Cj∧□(Aj↔¬(Bj∨Cj))∧□(Bj↔¬(Cj∨Aj))∧□(Cj↔¬(Aj∨Bj))),□∀x((Ax∨Bx∨Cx)→◇¬Dxv(x))|=□Mjj  [transitivity]' },
    { label: 'log882', formula: '∀a1∀a2(La1A∧La2A→(Lo(a1,a2)R1∧Lo(a2,a1)R1→a1=a2)),∀b1∀b2(Lb1B∧Lb2B→(Lo(b1,b2)R2∧Lo(b2,b1)R2→b1=b2)),∀a1∀a2∀b1∀b2(La1A∧La2A∧Lb1B∧Lb2B→(Lo(o(a1,b1),o(a2,b2))R↔Lo(a1,a2)R1∧Lo(b1,b2)R2))|=(LmA∧LpA∧LnB∧LqB→(Lo(o(m,n),o(p,q))R∧Lo(o(p,q),o(m,n))R→o(m,n)=o(p,q)))' },
    { label: 'log895', formula: '∀ASA|=∀A(SA→∃B(SB∧∀x(LxB↔LxA∧Fx)))→∀A∃B∀x(LxB↔LxA∧Fx)' },
    { label: 'log896', formula: '∃fH(f)∧∀f∀y(H(f)→(P(f,y)→(¬(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)))|=¬(M(o)∧∃eV(e)∧∀e(V(e)→∀x(P(e,x)↔x=o)))' },
    { label: 'log899', formula: '∀x∀y∀z(FC(C(xy)C(C(yz)C(xz)))∧FC(C(N(x)x)x)∧FC(xC(N(x)y))),∀x∀y(FC(xy)∧Fx→Fy)|=FC(C(ab)C(N(b)N(a)))' },
    { label: 'log901', formula: '∀x∀y∀z(FC(xC(yx))∧FC(C(xC(yz))C(C(xy)C(xz)))∧FC(C(N(x)N(y))C(yx))),∀x∀y(FC(xy)∧Fx→Fy)|=FC(aC(N(a)b))' },
    { label: 'log902', formula: '∀m∀n(Lmn↔LnM)|=∀A∀B(A=B→∃C∃D(LAC∧LBD∧u(C,D)=e))→∀A∀B(A=B→∃C∃D(LCA∧LAD∧u(C,D)=e))' },
    { label: 'log905', formula: '∃xTx,∃xAx,∃xXx,∃t(Tt∧∀a∀b((Aa∧Ab∧∀x∀y((Xx∧Xy∧Laxt∧Layt)→x=y)∧∀x∀y((Xx∧Xy∧Lbxt∧Lbyt)→x=y))→a=b))|=∀a∀b((Aa∧Ab∧∀x∀y((Xx∧Xy∧∃t(Tt∧Laxt)∧∃t(Tt∧Layt))→x=y)∧∀x∀y((Xx∧Xy∧∃t(Tt∧Lbxt)∧∃t(Tt∧Lbyt))→x=y))→a=b)' },
    { label: 'log906', formula: '∃eV(e,o)∧∀e(V(e,o)→(P(e,o)∧∀y(P(e,y)→M(y)))),∀e(H(e,o)→¬∃y(P(e,y)∧M(y))),∀e(V(e,o)→∃f(H(f,o)∧U(e,f))),∀e∀f(U(e,f)→∃x∃y(P(e,x)∧P(f,y)∧(x=y∨S(e,f,x,y))))|=¬(∀e∀f∀x∀y((P(e,x)∧P(f,y)∧M(x)∧¬M(y))→¬(x=y∨S(e,f,x,y))))' },
    { label: 'log908', formula: '∀x(Px↔∀y(Bxy→¬Py)),∀x∃y(Bxy),∀x∀y∀z((Byx∧Bzy)→Bzx)|=¬∃xPx' },
    { label: 'log909', formula: '∀x(Px↔(∀y(Bxy→¬Py))),∀x∃yBxy,∀x∀y∀z((Bxy∧Byz)→Bxz),∀x∀y(Bxy→¬Byx)|=p' },
    { label: 'log910', formula: '∀x∃yBxy,∀x∀y∀z((Byx∧Bzy)→Bzx)|=¬∀x(Px↔(∀y(Bxy→¬Py)))' },
    { label: 'log916', formula: '∀a∀b∀c(Lo(a,b)f∧Lo(a,c)f→b=c),∀a∀b∀c(Lo(a,b)g∧Lo(a,c)g→b=c),∀X(LXf→∃a∃bX=o(a,b)),∀X(LXg→∃a∃bX=o(a,b)),d(f)=d(g),∀h∀a(Lad(h)↔∃bLo(a,b)h),∀x(Lxd(f)→∃y(Lo(x,y)f∧Lo(x,y)g))|=Lo(m,n)f→Lo(m,n)g' },
    { label: 'log918', formula: '∀x∀y∀zf(f(x,y),z)=f(x,f(y,z)),∀xf(x,e)=x,∀x∃yf(x,y)=e|=∀x∃yf(y,x)=e' },
    { label: 'log919', formula: '(∀x∀y∀z(Rxy→Ryz→Rxz))∧(∀x(¬Rxx))∧(∀x(Rxf(x)))→(∃x∃y∃z∃w(¬x=y∧¬x=z∧¬y=z∧¬w=x∧¬w=y∧¬w=z))' },
    { label: 'log921', formula: '∀x(Mx→¬Ix),∀x(Mx→∀y(Pxy→Iy)),∀x(Ix→∃y(My∧Pyx)),∀x∀y((Ix∧Iy)→Ic(x,y)),∀x(Ix→∃y∃z((¬y=x∧¬z=x)∧x=c(y,z))),∀x(Mx∨Ix),∀x(Mx↔∃yPxy)|=∀x(Ix↔∃yPyx)' },
    { label: 'log925', formula: '∀x(Sx↔∃kLkx∨x=e)|=(D=y↔((∃B(B=y∧TB)∧Sy)∨(y=e∧¬∃BTB)))→(¬y=e→(D=y↔∃B(B=y∧TB)∧∃kLky))' },
    { label: 'log926', formula: '∀m(Sm↔∃kLkm∨m=e),∀y(D=y↔((∀x(Lxy↔Fx)∧Sy)∨(y=e∧¬∃B∀x(LxB↔Fx))))|=D=e↔(∀x(Lxe↔Fx)∧Se)∨(¬∃B∀x(LxB↔Fx))' },
    { label: 'log927', formula: '∀m(Sm↔∃kLkm∨m=e),¬∃kLke,∀y(D=y↔((∀x(Lxy↔Fx)∧Sy)∨(y=e∧¬∃B∀x(LxB↔Fx))))|=D=e→(∀x¬Fx)∨(¬∃B∀x(LxB↔Fx))' },
    { label: 'log929', formula: '¬∃kLke,∀y(Sy↔∃kLky∨y=e)|=∃y(((∀x(Lxy↔Fx)∧Sy)∨(¬∃B∀x(LxB↔Fx)∧y=e))∧Lwy)↔∃b∀x(Lxb↔Fx)∧Fw' },
    { label: 'log930', formula: '∀xPxx,∀x∀y∀z((Pxy∧Pyz)→Pxz),∀x∀y((Pxy∧Pyx)→x=y)|=(∀x∀y((Pxy∧¬(x=y))→∃z(Pzy∧∀a(¬Paz∨¬Pax))))→(∀x∀y((Pxy∧¬(x=y))→∃z(Pzy∧∀a(¬Paz∨¬Pax))))' },
    { label: 'log932', formula: '∀X(LXf→∃a∃bX=o(a,b)),∀X(LXg→∃a∃bX=o(a,b))|=∀Y(LYf↔LYg)↔∀m∀n(Lo(m,n)f↔Lo(m,n)g)' },
    { label: 'log933', formula: '∀m∀n(F(f,m)=n↔(Tmf∧Lo(m,n)f)∨(¬Tmf∧n=e))|=((Taf∧Tbf)→∃y(Lo(a,y)f∧Lo(b,y)f))∧((Taf∧¬Tbf)→Lo(a,e)f)∧((¬Taf∧Tbf)→Lo(b,e)f)∧((¬Taf∧¬Tbf)→∃y(y=e∧y=e))→F(f,a)=F(f,b)' },
    { label: 'log939', formula: '□∃x∀y(Fy↔x=y),□∀s(Fs→∀x(Ex→□(Fs→Ex))),□∀s(Fs→∀x(¬Ex→□(Fs→¬Ex))),□∀x(Fx↔Ex),□∀x(Fx→Ex)|=□∃x∀y((Ey∧Fy)↔x=y)  [universality]' },
    { label: 'log941', formula: '¬∃x∃y((Gx∧Gy)→(Sxy∧Syx)),∀x(Ix↔Cxi),∀x(Gx→Ix),∀x∀y∀z(Cxy→(Gz→(Szx↔Szy)))|=¬∃x∃y(Gx∧(Iy∧Sxy))' },
    { label: 'log942', formula: '¬∃x∃y(Gx∧Gy∧Sxy∧Syx),∀x(Ix↔Cxi),∀x(Gx→Ix),∀x∀y∀z(Cxy→(Gz→(Szx↔Szy)))|=¬∃x∃y(Gx∧Iy∧Sxy)' },
    { label: 'log943', formula: '(∃x∃y∀z(x=z∨y=z)∧Fa∧Fb∧¬a=b)→(Fc∧(a=c∨b=c))' },
    { label: 'log946', formula: '□¬(a=b),a=c|=□¬(c=b)  [euclidity]' },
    { label: 'log948', formula: '∃x(Lx∧Kxa),La∧Lb∧Lc,∀x(Lx→(x=a∨x=b∨x=c)),∀x∀y(Kxy→Hxy),∀x∀y(Kxy→¬Rxy),∀x(Hax→¬Hcx),∀x(¬(x=b)→Hax),∀x(¬Rxa→Hbx),∀x(Hax→Hbx),∀x∃y¬Hxy,¬(a=b),¬(a=c)∧¬(b=c)|=Kaa' },
    { label: 'log955', formula: '∀x¬s(x)=0,∀x∀y((¬x=s(0)∧s(x)=s(y))→x=y),s(s(0))=s(s(s(0))),∀x∀y+(x,0)=x,∀x∀y+(x,s(y))=s(+(x,y))|=∃x∃y∃z∀w((w=x∨w=y∨w=z)∧¬((w=x∧w=y)∨(w=x∧w=z)∨(w=y∧w=z)))' },
    { label: 'log956', formula: 'X=o(o(a,c),o(F(g,c),F(f,a)))↔∃M∃N(X=o(M,N)∧M=o(a,c)∧N=o(F(g,c),F(f,a)))' },
    { label: 'log957', formula: '∃M∃N(X=o(M,N)∧M=o(a,c)∧N=o(F(g,c),F(f,a)))→X=o(o(a,c),o(F(g,c),F(f,a)))' },
    { label: 'log959', formula: '∃x∃y(¬(x=y)),∀x∀p(((Fxp)↔((Lxp)∧∃y(¬(y=x)∧¬(Lxp→(Rxy∧Oyp)))))),∀x∀p(((Dxp)↔((Lxp)∧∃y(¬(y=x)∧(Lxp→(Rxy∧Oyp))))))|=∀x∀p((Lxp→(Dxp∨Fxp)))' },
    { label: 'log960', formula: '∀x∀r(Xxr↔∀s(Ors↔Wxs)),∀x∀r(Pxr↔∀s(Ors→Wxs)),∀x∀r(Exr↔(Wxr∧∀s(Wxs→Ors))),∃x∃r(Wxr),∀x∀r(Wxr→(Tx∧Lr)),∀r∀s(Ors→(Lr∧Ls)),∀x∀y((Tx∧Ly)→¬x=y),∃r∃s(Ors),∀r(Lr→∃y(Oyr∧¬y=r)∧∃s(Ls∧¬Osr∧¬Ors∧¬s=r)),∀r∀s(Ors→Osr)|=∃x∃r(Xxr)' },
    { label: 'log962', formula: '□∀x∀y(Ixy→∀z(Ixz→z=y)),□∀x(¬Sx↔∀y(Ixy→◇∃z(¬z=y∧Ixz))),□∀x∃yIxy|=□∀x(Sx↔∀y(Ixy→□∀z(Ixz→z=y)))' },
    { label: 'log963', formula: '□∀x∀y(Ixy→∀z(Ixz→z=y)),□∀x∃yIxy,□∀x(Sx↔∀y(Ixy→□∀z(Ixz→z=y))),□∀x(Dx→□Sx),□∀x∀y(Eyx→(Sy↔Sx)),∀x∀y(Lxy→□(Dy→□(Sn(x)↔St(y)))),□∀x(Dx→□Ext(x))|=∀x∀y(Lxy→□(Dy→□(Sn(x)∧St(y))))  [transitivity]' },
    { label: 'log966', formula: '□∀x∀y(Axy↔∃z1∃z2∃z3(¬(z1=z2∨z1=z3∨z2=z3)∧(Ez1k(x,y)∧Ez2k(x,y)∧Ez3k(x,y)))),□∀x∀y∃z2(∀z1(Ez1k(x,y)→(¬z2=z1∧□(Fxy→Ez2k(x,y))))),□∀x∀y(Fxy→∃zEzk(x,y))|=□Fjf→◇Ajf  [transitivity, seriality]' },
    { label: 'log968', formula: '(∀x∀k(LxT2∧LkT3∧∀y∀r(Lyx∧LrT4∧∀z(Lzy→F(r,z)=t(z))→F(k,y)=r))→Mh)→(∀x∀k(LxT2∧LkT3∧∀y∀r(Lyx∧LrT4→(∀z(Lzy→F(r,z)=t(z))→F(k,y)=r)))→Mh)' },
    { label: 'log970', formula: '∀a∀b∀cf(f(ab)c)=f(af(bc)),∀a(f(ai)=a∧f(ia)=a),∀a∃b(f(ab)=i∧f(ba)=i)|=∀a∃c∀b(f(ab)=i∧f(ba)=i↔b=c)' },
    { label: 'log971', formula: '∀xP(x,x),∀x¬E(x,x),∀x∀y(P(y,f(x))↔E(y,x)),∀x∀y(P(y,x)↔E(y,d(x))),∀x∀y(∀z(P(z,x)↔P(z,y))→x=y),∀x∀y(E(x,p(y))↔∀z(E(z,x)→E(z,y))),∀x∀y(E(x,u(y))↔∃z(E(x,z)∧E(z,y))),∀x∀y∀z(E(x,b(y,z))↔(x=y∨x=z))|=R' },
    { label: 'log974', formula: '∀x∀y(Oxy↔∃z(Pzx∧Pzy)),∀x∀y∀z((Oxy∧Pxz)→Ozy),∀x∀y((Pxy∧Pyx)↔x=y),∀x(Oxx),∀x(Pxx),∀x∀y((Oxy↔Oyx))|=∀x∀y∀z((Oxy∧Pyz)→Oxz)' },
    { label: 'log975', formula: '∀x∀y(Vxy↔∀z(Oyz→Wxz)),∀x∀y∀z((Oxy∧Pxz)→Ozy),∀x∀y(Oxy↔∃z(Pzx∧Pzy)),∀x(Oxx),∀x(Pxx)|=∀x∀y∀z∀u(Vxy∧Vxz∧∀t(Ptu→(Oty∨Otz))→Vxu)' },
    { label: 'log976', formula: '∀x(Jx→Px),∃x∃y(((Px∧Py)∧¬x=y)∧∀z(Pz→(z=y∨z=x))),∃x∃y((Jx∧Jy)∧¬x=y)|=∀x(Px→Jx)' },
    { label: 'log977', formula: '∃a1∃b1(K=o(a1,b1)∧F(f1,c)=a1∧F(f2,c)=b1)→K=o(F(f1,c),F(f2,c))' },
    { label: 'log980', formula: '∀A∃B∀x(LxB↔LxA∧Fx)|=∃A∀x(Fx→LxA)↔∀A∃B∀x(LxB↔Fx)' },
    { label: 'log981', formula: '∀x(Pxx),∀x∀y(Oxy↔∃z(Pzx∧Pzy)),∀x∀y∀z((Oxy∧Pxz)→Ozy),∀x∀y((Pxy∧Pyx)↔x=y),∀x(Oxx),∀x∀y(Oxy↔Oyx),∀x∀y∀z((Pxy∧Pyz)→Pxz),∀x∀y(Vxy↔∀z(Oyz→Wxz)),∀x∀y(Wxy↔∃z(Szx∧Myz)),∀x∀y∀r((Wxy∧Pyr)→Wxr),∀x∀y(Mxy→¬(Myx)),∀x∀y∀z∀r(Szx→(Myz∧Pyr→Mrz)),∀x∀y(Sxy→¬(Syx)),∀x∀y∀z(Sxy→(¬(Pxz)∨x=z)),∀x∀y(Nxy↔Wxy∧∀z(Wxz→Oyz)),∀x∀y(Fxy↔(Vxy∧Nxy))|=∀x∀y∀z(Fxy∧Fxz→∀t(Oyt↔Ozt))' },
    { label: 'log983', formula: '¬∃kLke,∀M∀N(∀k(LkM↔LkN)→M=N),∀f∀m(Lmd(f)↔∃nLo(m,n)f)|=d(e)=e' },
    { label: 'log984', formula: '¬∃kLke,∀M∀N(∀k(LkM↔LkN)→M=N),∀m(Lmd(e)↔∃nLo(m,n)e)|=∃h(∀X(LXe→∃m∃nX=o(m,n))∧∀m∀n∀k(Lo(m,n)h∧Lo(m,k)h→k=n)∧d(h)=h)' },
    { label: 'log985', formula: '¬∃h(∀X(LXh→∃m∃nX=o(m,n))∧∀m∀n∀k(Lo(m,n)h∧Lo(m,k)h→k=n)∧d(h)=h),¬∃mLmd(e),¬∃kLke|=¬∀M∀N(∀k(LkM↔LkN)→M=N)' },
    { label: 'log986', formula: '∀h¬(∀X(LXh→∃m∃nX=o(m,n))∧d(h)=e)|=¬(¬∃kLke∧∀f∀a(Lad(f)↔∃bLo(a,b)f)∧∀M∀N(∀a(LaM↔LaN)→M=N))' },
    { label: 'log987', formula: '∀f∀a(Lad(f)↔∃bLo(a,b)f),∀f∀b(Lbr(f)↔∃aLo(a,b)f),∀M∀N(I(M,N)↔∀a(LaM→LaN)),∀M∀N(∀a(LaM↔LaN)→M=N),¬∃kLke|=∃h(I(r(h),A))' },
    { label: 'log988', formula: '∀m∃S∀x(LxS↔x=m),∀y((y=e↔¬∃xLxy))|=∃A(∃m(LmA∧∀n(LnA→m=n))∧¬A=e)' },
    { label: 'log989', formula: '∀m∃S∀x(LxS↔x=m),∀y((y=e↔¬∃xLxy))|=∃A(∃m(LmA∧∀n(LnA→m=n))∧∃xLxA)' },
    { label: 'log990', formula: '∀a(∃xLxa∨a=e→∃b((∃xLxb∨b=e)∧∀x(Lxb↔Lxa∧Fx)))|=∃B∀x(LxB↔LxA∧Fx)' },
    { label: 'log994', formula: '(∃x)(∃y)(((Px∧Py)∧¬x=y)∧(∀z)(Pz→(z=x∨z=y)))|=(∃x)(∃y)(((Px∧Py)∧¬x=y)∧(∀x)(∀y)(∀z)(((Px∧Py)∧Pz)→((x=y∨y=z)∨x=z)))' },
    { label: 'log996', formula: '∀A(∃m∀x(LxA↔x=m)→SA),∀m∃t∀x(Lxt↔x=m)|=∃A∃x(LxA∧Sx)' },
    { label: 'log997', formula: '∀A(SA↔∃m∀x(x=m↔LxA)),∀m∃t∀x(Lxt↔x=m)|=∃A(∃x(LxA∧Sx))' },
];

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