A certified basis of 64 identities
This list of identities is a basis, proved in Lean, of [6, 5661], which generates the variety V[5661]. Removing the identities that follow from the others leaves 28 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-c1bd16aa0c3e707a in the data of the bases-min seal.
Certified for
The identities
- x³ ≈ x³
- x³ ≈ x⁴
- x²yx ≈ xyx²
- x²yx ≈ xyx²
- x²y² ≈ x²y²
- x²y² ≈ xyxy
- x²y² ≈ xy²x
- x²yx ≈ x²yx²
- xyx² ≈ xyx³
- x²yzy ≈ x²zy²
- x²yzy ≈ x²zy²
- x²yzy ≈ xyxzy
- x²yzy ≈ xyzyx
- x²yz² ≈ xyzxz
- x²yz² ≈ xyz²x
- xyxzx ≈ xzxyx
- xyxz² ≈ xyxz²
- xyxz² ≈ xzyxz
- xyxz² ≈ xz²yx
- xyxzx ≈ xyxzx²
- x²y²z² ≈ x²z²y²
- x²yztz ≈ x²tzyz
- x²yztz ≈ xyzxtz
- x²yztz ≈ xyztzx
- xyxztz ≈ xyxtz²
- xyxztz ≈ xyxtz²
- xyxztz ≈ xzyxtz
- xyxztz ≈ xztzyx
- xyxzt² ≈ xztyxt
- xyxzt² ≈ xzt²yx
- x²y²ztz ≈ x²ztzy²
- x²y²ztz ≈ x²ztzy²
- x²y²zt² ≈ x²zt²y²
- x²y²zt² ≈ x²zt²y²
- xyxz²t² ≈ xyxt²z²
- xyxztut ≈ xyxutzt
- xyxztut ≈ xztyxut
- xyxztut ≈ xztutyx
- x²y²ztut ≈ x²ztuty²
- x²y²ztut ≈ x²ztuty²
- x²yzytut ≈ x²tutyzy
- x²yzytu² ≈ x²tu²yzy
- x²yzytu² ≈ x²tu²yzy
- x²yz²tu² ≈ x²tu²yz²
- xyxz²tut ≈ xyxtutz²
- xyxz²tut ≈ xyxtutz²
- xyxz²tu² ≈ xyxtu²z²
- xyxz²tu² ≈ xyxtu²z²
- x²yzytuvu ≈ x²tuvuyzy
- x²yzytuvu ≈ x²tuvuyzy
- x²yz²tuvu ≈ x²tuvuyz²
- x²yz²tuvu ≈ x²tuvuyz²
- xyxz²tuvu ≈ xyxtuvuz²
- xyxz²tuvu ≈ xyxtuvuz²
- xyxztzuvu ≈ xyxuvuztz
- xyxztzuv² ≈ xyxuv²ztz
- xyxztzuv² ≈ xyxuv²ztz
- xyxzt²uv² ≈ xyxuv²zt²
- x²yztzuvwv ≈ x²uvwvyztz
- xyxztzuvwv ≈ xyxuvwvztz
- xyxztzuvwv ≈ xyxuvwvztz
- xyxzt²uvwv ≈ xyxuvwvzt²
- xyxzt²uvwv ≈ xyxuvwvzt²
- xyxztutvwsw ≈ xyxvwswztut