diff --git a/blueprint/src/chapter/infinite_models.tex b/blueprint/src/chapter/infinite_models.tex
index aea5e32f..6de8091b 100644
--- a/blueprint/src/chapter/infinite_models.tex
+++ b/blueprint/src/chapter/infinite_models.tex
@@ -7,15 +7,15 @@ \chapter{Infinite models}\label{infinite-model-chapter}
 We note some selected laws of order more than $5$, used for such non-implications.
 
 \begin{definition}[Equation 5105]
-  \label{eq5105}\uses{magma-def}\lean{Equation28393}\leanok
+  \label{eq5105}\uses{magma-def}\lean{Equation5105}\leanok
   Equation 5105 is the law $0  \formaleq 1 \op (1 \op (1 \op (0 \op (2 \op 1))))$ (or the equation $x = y \op (y \op (y \op (x \op (z \op y))))$).
 \end{definition}
 
 This law of order $5$ was mentioned in \cite{Kisielewicz2}.
 
-\begin{definition}[Equation 28393]
-  \label{eq28393}\uses{magma-def}\lean{Equation28393}\leanok
-  Equation 28393 is the law $0  \formaleq  (((0 \op 0) \op 0) \op 1) \op (0 \op 2)$ (or the equation $x = (((x \op x) \op x) \op y) \op (x \op z)$).
+\begin{definition}[Equation 28770]
+  \label{eq28770}\uses{magma-def}\lean{Equation28770}\leanok
+  Equation 28770 is the law $0  \formaleq  (((1 \op 1) \op 1) \op 0) \op (1 \op 2)$ (or the equation $x = (((y \op y) \op y) \op x) \op (y \op z)$).
 \end{definition}
 
 This law of order $5$ was introduced by Kisielewicz \cite{Kisielewicz}.
@@ -65,7 +65,7 @@ \chapter{Infinite models}\label{infinite-model-chapter}
 
 An even shorter law (order $5$) was obtained by the same author in a follow-up paper \cite{Kisielewicz2}:
 
-\begin{theorem}[Kisielewicz's second Austin law]\label{kis-thm2}\uses{eq2, eq28393} \Cref{eq28393} is an Austin law.
+\begin{theorem}[Kisielewicz's second Austin law]\label{kis-thm2}\uses{eq2, eq28770} \Cref{eq28770} is an Austin law.
 \end{theorem}
 
 \begin{proof} Using the $y^2$ and $y^3$ notation as before, the law reads
diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean
index 156268e9..e10c8d54 100644
--- a/equational_theories/Equations.lean
+++ b/equational_theories/Equations.lean
@@ -123,8 +123,10 @@ abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x
 /-- Mentioned in a paper of Kisielewicz as a conjectural Austin law -/
 equation 5105  :=  x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))
 
+equation 28381  :=  x = (((x ◇ x) ◇ x) ◇ y) ◇ (x ◇ z)
+
 /-- Kisielewicz's second Austin law -/
-equation 28393  :=  x = (((x ◇ x) ◇ x) ◇ y) ◇ (x ◇ z)
+equation 28770  :=  x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z)
 
 /- Some order 6 laws -/
 
diff --git a/equational_theories/InfModel.lean b/equational_theories/InfModel.lean
index e45d5f04..167e47ac 100644
--- a/equational_theories/InfModel.lean
+++ b/equational_theories/InfModel.lean
@@ -123,6 +123,345 @@ theorem Finite.Equation5105_implies_Equation2 (G : Type*) [Magma G] [Finite G] (
       _= x ◇ (x ◇ (x ◇ (y ◇ (x ◇ x)))) := by rw [hhhh]
       _= y := by rw [←  h y x x]
 
+theorem Finite.Equation28770_implies_Equation2 (G : Type*) [Magma G] [Finite G] (h : Equation28770 G) :
+    Equation2 G := by
+    have : ∀ (y z u : G), y ◇ z = y ◇ u := by
+      intro y
+      let f (x : G) := ((y ◇ y) ◇ y) ◇ x
+      let g (x : G) := x ◇ (y ◇ y)
+      have : Function.RightInverse f g := by
+        intro x
+        simp [f, g, ← h]
+      intro z u
+      apply this.injective
+      obtain ⟨finv, hf⟩ := (Finite.surjective_of_injective this.injective).hasRightInverse
+      let fy := finv ((y ◇ y) ◇ y)
+      replace hf : ((y ◇ y) ◇ y) ◇ fy = (y ◇ y) ◇ y := hf _
+      have := h fy y
+      simp only [hf] at this
+      simp [f, ← this]
+    intro x u
+    have y := x
+    have z := x
+    rw [h x y z, this ((y ◇ y) ◇ y)  x u, ← this ((y ◇ y) ◇ y) u u, ← h]
+
+theorem Equation28770_not_implies_Equation2 : ∃ (G : Type) (_ : Magma G), Equation28770 G ∧ ¬Equation2 G := by
+  have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
+  have : Fact (Nat.Prime 3) := ⟨Nat.prime_three⟩
+  have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
+  letI : Magma ℕ+ := { op := fun a b ↦ if a = b then 2^b.val else
+        if a = 2^b.val then 3^b.val else
+        if a = 3^(padicValNat 3 a) then a * 5^b.val else
+        if a = 3^(padicValNat 3 a) * 5^(padicValNat 5 a) then Nat.toPNat' (padicValNat 5 a) else
+        if a = 2^(3^(padicValNat 3 (padicValNat 2 a))) then 3^(padicValNat 3 (padicValNat 2 a)) else 1}
+  refine ⟨ℕ+, this, ⟨?_, fun x ↦ nomatch (x 1 2)⟩⟩
+  intro x y z
+  -- t1 is from the proof of Equation374794_not_implies_Equation2
+  have t1 (y : ℕ+) : 2 ^ (y : ℕ) ≠ y := by
+    apply_fun PNat.val
+    simp [ne_of_gt, Nat.lt_pow_self]
+  have h1 : ∀ (y: ℕ+), y ◇ y = 2^y.val := by
+    intro y
+    unfold Magma.op
+    simp only [ite_true]
+  have h2 : ∀ (y: ℕ+), (2^y.val) ◇ y = 3^y.val := by
+    intro y
+    unfold Magma.op
+    simp [t1]
+  have h3 : ∀ (x y: ℕ+), x ≠ 3^y.val → (3^y.val) ◇ x = 3^y.val * 5^x.val := by
+    intro x y hxy
+    unfold Magma.op
+    simp
+    rw [if_neg]
+    case hnc =>
+      intro h''
+      apply hxy
+      simp [h'']
+    simp
+    contrapose
+    intro _
+    apply_fun PNat.val
+    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]
+    intro nh
+    apply eq_of_prime_pow_eq at nh
+    · contradiction
+    · exact Nat.prime_three.prime
+    · exact Nat.prime_two.prime
+    · simp
+  have h4 : ∀ (x y z: ℕ+), z ≠ 3^y.val * 5^x.val → (3^y.val * 5^x.val) ◇ z = x := by
+    intro x y z hxyz
+    unfold Magma.op
+    simp
+    rw [if_neg]
+    case hnc =>
+        intro h'
+        apply hxyz
+        simp [h']
+    rw [if_neg]
+    case hnc =>
+      apply_fun PNat.val
+      simp [PNat.pow_coe, PNat.val_ofNat, ne_eq]
+      intro nh
+      apply PNat.ne_zero z
+      calc ↑z
+        _ = padicValNat 2 (3^y.val * 5^x.val) := by simp [nh]
+        _ = 0 := by simp [padicValNat.mul, padicValNat_prime_prime_pow]
+    rw [if_neg]
+    case hnc =>
+      intro hc
+      apply PNat.ne_zero x
+      calc ↑x
+        _ = padicValNat 5 ↑((3: ℕ+)^y.val * (5: ℕ+)^x.val) := by simp [padicValNat_prime_prime_pow, padicValNat.mul]
+        _ = padicValNat 5 ((3: ℕ+)^(padicValNat (3: ℕ) ((3: ℕ)^y.val * (5: ℕ)^x.val))) := by simp [hc]
+        _ = 0 := by simp [padicValNat_prime_prime_pow]
+    rw [if_pos]
+    case hc =>
+      simp [padicValNat.mul, padicValNat_prime_prime_pow]
+    simp [this, Subtype.ext_iff, padicValNat.mul, padicValNat_prime_prime_pow]
+  have h5 : ∀ (y z: ℕ+), z ≠ 3^y.val ∧ z ≠ 2^(3^y.val) → (2^(3^y.val)) ◇ z = 3^y.val := by
+    intro y z hyz
+    unfold Magma.op
+    simp
+    rw [if_neg, if_neg, if_neg, if_neg]
+    .
+      intro hc
+      apply PNat.ne_zero ((3: ℕ+)^y.val)
+      calc ↑((3: ℕ+)^y.val)
+        _ = padicValNat 2 ↑(2^3^y.val: ℕ+) := by simp
+        _ = padicValNat 2 _ := by rw [hc]
+        _ = 0 := by simp [padicValNat_prime_prime_pow]
+    .
+      intro hc
+      apply PNat.ne_zero ((3: ℕ+)^y.val)
+      calc ↑((3: ℕ+)^y.val)
+        _ = padicValNat 2 ↑(2^3^y.val: ℕ+) := by simp
+        _ = padicValNat 2 _ := by rw [hc]
+        _ = 0 := by simp [padicValNat_prime_prime_pow]
+    .
+      intro hc
+      apply hyz.1
+      calc z
+        _ = z.val.toPNat' := by simp
+        _ = (padicValNat 2 (2^z.val: ℕ+)).toPNat' := by simp
+        _ = (padicValNat 2 ↑(2^3^y.val: ℕ+)).toPNat' := by rw [←hc]
+        _ = (3^y.val: ℕ).toPNat' := by simp
+        _ = 3^↑y := by rw [←PNat.coe_inj]; simp
+    .
+      intro hc
+      apply hyz.2
+      simp [hc]
+  rw [h1, h2]
+  by_cases hx : x = 3^y.val
+  .
+    rw [hx, h1]
+    by_cases hyz : y ◇ z = 2^(3^y.val)
+    .
+      simp [hyz, h1]
+      exfalso
+      have : padicValNat 2 ↑(y ◇ z) = ↑(3^y.val) := by simp [hyz]
+      unfold Magma.op at this
+      simp at this
+      repeat rw [apply_ite PNat.val] at this
+      repeat rw [apply_ite (padicValNat 2)] at this
+      simp only [PNat.pow_coe, PNat.val_ofNat] at this
+      simp only [padicValNat.prime_pow] at this
+      simp [padicValNat_prime_prime_pow] at this
+      repeat rw [apply_ite (padicValNat 2)] at this
+      simp [padicValNat.mul, padicValNat_prime_prime_pow] at this
+      repeat simp only [ite_eq_iff] at this
+      simp at this
+      have this' : (0: ℕ) = (3: ℕ)^y.val ↔ False := by
+        apply Iff.intro
+        .
+          simp
+          intro h
+          apply pow_ne_zero y.val (by simp: 3 ≠ 0)
+          simp [h]
+        .
+          intro h
+          contradiction
+      simp [this'] at this
+      repeat simp [and_or_left, and_or_left] at this
+      cases this with
+      | inl h =>
+        rw [h.1] at h
+        simp at h
+        have this2 := Nat.lt_pow_self (by simp: 1 < 3) z.val
+        have this3 := ne_of_gt this2
+        exact this3 (Eq.symm h)
+      | inr this => _
+      cases this with
+      | inl h =>
+        have h1 := h.2.2.1
+        have h2 := h.2.2.2
+        rw [h1] at h2
+        simp at h2
+        simp [padicValNat_prime_prime_pow] at h2
+        have h2 := Eq.symm h2
+        have := pow_ne_zero (3^padicValNat 3 y.val) (by simp: 3 ≠ 0)
+        apply pow_ne_zero y.val (by simp: 3 ≠ 0)
+        contradiction
+      | inr this => _
+      have this' := this.2.2.2.2.2
+      apply_fun padicValNat 3 at this'
+      simp [padicValNat.prime_pow] at this'
+      have this' := Eq.symm this'
+      have this2 := calc y.val
+        _ > Nat.log 5 y.val := by simp [Nat.log_lt_self]
+        _ ≥ padicValNat 5 y.val := by simp [padicValNat_le_nat_log]
+        _ ≥ Nat.log 2 (padicValNat 5 y.val) := by simp [Nat.log_le_self]
+        _ ≥ padicValNat 2 (padicValNat 5 y.val) := by simp [padicValNat_le_nat_log]
+        _ ≥ Nat.log 3 (padicValNat 2 (padicValNat 5 y.val)) := by simp [Nat.log_le_self]
+        _ ≥ padicValNat 3 (padicValNat 2 (padicValNat 5 y.val)) := by simp [padicValNat_le_nat_log]
+      have this3 := ne_of_gt this2
+      exact this3 this'
+    .
+      by_cases hyz' : y ◇ z = 3^y.val
+      .
+        rw [←hyz', h2, hyz']
+        exfalso
+        have : padicValNat 3 ↑(y ◇ z) = ↑y.val := by simp [hyz']
+        unfold Magma.op at this
+        simp at this
+        repeat rw [apply_ite PNat.val] at this
+        repeat rw [apply_ite (padicValNat 3)] at this
+        simp only [PNat.pow_coe, PNat.val_ofNat] at this
+        simp only [padicValNat.prime_pow] at this
+        simp [padicValNat_prime_prime_pow] at this
+        repeat rw [apply_ite (padicValNat 3)] at this
+        simp [padicValNat.mul, padicValNat_prime_prime_pow] at this
+        repeat simp only [ite_eq_iff] at this
+        simp at this
+        have this' : ((0: ℕ) = y.val) ↔ False := by
+          simp [false_iff]
+          intro hc
+          have hc := Eq.symm hc
+          have hc' := PNat.ne_zero y
+          contradiction
+        simp [this'] at this
+        repeat simp [and_or_left, and_or_left] at this
+        cases this with
+        | inl h =>
+          have h1 := h.2.1
+          have h2 := h.2.2
+          rw [h2] at h1
+          have h1 := Eq.symm h1
+          apply_fun PNat.val at h1
+          simp at h1
+          have this2 := Nat.lt_pow_self (by simp: 1 < 2) y.val
+          have this3 := ne_of_gt this2
+          exact this3 h1
+        | inr this => _
+        cases this with
+        | inl h =>
+          have h1 := h.2.2.1
+          have h2 := h.2.2.2
+          rw [h2] at h1
+          have h1 := Eq.symm h1
+          apply_fun PNat.val at h1
+          simp at h1
+          have this2 := Nat.lt_pow_self (by simp: 1 < 3) y.val
+          have this3 := ne_of_gt this2
+          exact this3 h1
+        | inr this => _
+        cases this with
+        | inl h =>
+          have h := Eq.symm h.2.2.2.2.2
+          have h' := calc y.val
+            _ > Nat.log 5 y.val := by simp [Nat.log_lt_self]
+            _ ≥ padicValNat 5 y.val := by simp [padicValNat_le_nat_log]
+            _ ≥ Nat.log 3 (padicValNat 5 y.val) := by simp [Nat.log_le_self]
+            _ ≥ padicValNat 3 (padicValNat 5 y.val) := by simp [padicValNat_le_nat_log]
+          exact (ne_of_gt h') h
+        | inr this => _
+        have this := Eq.symm this.2.2.2.2.2
+        have this' := calc y.val
+          _ > Nat.log 2 y.val := by simp [Nat.log_lt_self]
+          _ ≥ padicValNat 2 y.val := by simp [padicValNat_le_nat_log]
+          _ ≥ Nat.log 3 (padicValNat 2 y.val) := by simp [Nat.log_le_self]
+          _ ≥ padicValNat 3 (padicValNat 2 y.val) := by simp [padicValNat_le_nat_log]
+        exact (ne_of_gt this') this
+      .
+        have : (y ◇ z) ≠ 3^y.val ∧ (y ◇ z) ≠ 2^(3^y.val)  := And.intro hyz' hyz
+        simp [h5 y (y ◇ z) this]
+  .
+    rw [h3 x y hx]
+    by_cases hyz : y ◇ z = 3^y.val * 5^x.val
+    .
+      rw [hyz, h1]
+      exfalso
+      unfold Magma.op at hyz
+      simp at hyz
+      simp only [PNat.pow_coe, PNat.val_ofNat] at hyz
+      repeat simp only [ite_eq_iff] at hyz
+      cases hyz with
+      | inl h =>
+        have h' := h.2
+        apply_fun padicValNat 2 at h'
+        simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
+      | inr hyz => _
+      have hyz := hyz.2
+      cases hyz with
+      | inl h =>
+        have h' := Eq.symm h.2
+        apply_fun padicValNat 5 at h'
+        simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
+      | inr hyz => _
+      have hyz := hyz.2
+      cases hyz with
+      | inl h =>
+        rw [h.1] at h
+        have h' := h.2
+        apply_fun padicValNat 3 at h'
+        simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
+        have this2 := Nat.lt_pow_self (by simp: 1 < 3) (padicValNat 3 y.val)
+        have this2 := ne_of_gt this2
+        exact this2 (Eq.symm h')
+      | inr hyz => _
+      have hyz := hyz.2
+      cases hyz with
+      | inl h =>
+        rw [h.1] at h
+        have h' := h.2
+        simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h'
+        apply_fun PNat.val at h'
+        simp at h'
+        repeat simp only [ite_eq_iff] at h'
+        cases h' with
+        | inl this =>
+          have this := this.2
+          have this' := calc 3 ^ (3 ^ padicValNat 3 y.val * 5 ^ padicValNat 5 y.val) * 5 ^ x.val
+            _ ≥ 3 ^ (3 ^ padicValNat 3 y.val * 5 ^ padicValNat 5 y.val) := by simp [one_le_pow₀]
+            _ = 3 ^ (5 ^ padicValNat 5 y.val * 3 ^ padicValNat 3 y.val) := by simp [mul_comm]
+            _ = (3 ^ (5 ^ padicValNat 5 y.val)) ^ (3 ^ padicValNat 3 y.val) := by simp [pow_mul]
+            _ ≥ 3 ^ (5 ^ padicValNat 5 y.val) := by apply le_self_pow; simp [one_le_pow₀]; apply pow_ne_zero; simp
+            _ > 5 ^ padicValNat 5 y.val := by simp [Nat.lt_pow_self (by simp: 1 < 3)]
+            _ > padicValNat 5 y.val := by simp [Nat.lt_pow_self (by simp: 1 < 5)]
+          exact (ne_of_gt this') (Eq.symm this)
+        | inr this =>
+          have this := Eq.symm this.2
+          apply_fun padicValNat 5 at this
+          simp [padicValNat_prime_prime_pow, padicValNat.mul] at this
+      | inr hyz => _
+      have hyz := hyz.2
+      cases hyz with
+      | inl h =>
+        have h := Eq.symm h.2
+        apply_fun padicValNat 3 at h
+        simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h
+        have this' := calc y.val
+          _ > Nat.log 2 y.val := by simp [Nat.log_lt_self]
+          _ ≥ padicValNat 2 y.val := by simp [padicValNat_le_nat_log]
+          _ ≥ Nat.log 3 (padicValNat 2 y.val) := by simp [Nat.log_le_self]
+          _ ≥ padicValNat 3 (padicValNat 2 y.val) := by simp [padicValNat_le_nat_log]
+        exact (ne_of_gt this') h
+      | inr hyz => _
+      have h := Eq.symm hyz.2
+      apply_fun padicValNat 3 at h
+      simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h
+    .
+      rw [h4 x y (y ◇ z) hyz]
+
 theorem Finite.Equation3994_implies_Equation3588 (G : Type*) [Magma G] [Finite G] (h : Equation3994 G) :
     Equation3588 G := by
   intro x y z
diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index af258ea3..954888f5 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -460,7 +460,7 @@ theorem Equation2_implies_Equation5105 (G: Type _) [Magma G] (h: Equation2 G) :
   fun _ _ _ ↦ h _ _
 
 @[equational_result]
-theorem Equation2_implies_Equation28393 (G: Type _) [Magma G] (h: Equation2 G) : Equation28393 G :=
+theorem Equation2_implies_Equation28381 (G: Type _) [Magma G] (h: Equation2 G) : Equation28381 G :=
   fun _ _ _ ↦ h _ _
 
 @[equational_result]
@@ -488,7 +488,7 @@ theorem Equation4_implies_Equation3744 (G: Type _) [Magma G] (h: Equation4 G) :
     _ = (x ◇ z) ◇ (w ◇ y) := h (x ◇ z) (w ◇ y)
 
 @[equational_result]
-theorem Equation4_implies_Equation28393 (G: Type _) [Magma G] (h: Equation4 G) : Equation28393 G :=
+theorem Equation4_implies_Equation28381 (G: Type _) [Magma G] (h: Equation4 G) : Equation28381 G :=
   fun x y z ↦
     calc x
     _ = x ◇ x := (h x x)