Proof Generated By Lemma Propagation

Problem Statement

Let $*$ be a commutative and associative binary operation on a set $S.$ Assume that for every $x$ and $y$ in $S,$ there exists $z$ in $S$ such that $x*z=y.$ (This $z$ may depend on $x$ and $y.$) Show that if $p,q,r$ are in $S$ and $p*r=q*r,$ then $p=q.$

Definitions

1. Identity Element- A element $e$ is a Identity Element if $\exists x \in S$ such that $x*e=x$.
2. Universal Identity-A Identity Element $e$ is called a Universal Identity if $\forall x\in S \ \ x*e=x $ is satisfied.

Solving Strategy

Part1 : Proving the existence and uniqueness of universal identity

1. Prove that all identity elements are universal identities for the set $ S $ $i.e$
$\\$ $$\exists x \ \exists e \ [(x*e = e) \implies \forall y \in S \ (y*e \ = \ y)]\\$$
2. Prove that the set of all universal identities is singleton $i.e$
$\\$ $$\forall x \ \exists e_{1} \exists e_{2} \ [[(x*e_{1} = x) \land (x*e_{2} =x )] \implies (e_{1} = e_{2})]$$

</ol>

Part2 : Elimination

We have now proved the exists a unique Universal Identity, namely $e$ for the set $S$.Now for every pair $(x,e)$ we can find a $y$ (depending on $x$ and $e$) such that $x*y=e$ .Using this observation we can eliminate $c$ from the equation $a*c=b*c$.

Proof

import $cp.bin.`provingground-core-jvm-2312478e00.fat.jar`

import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

import provingground._ , interface._, HoTT._, learning._ 

import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
import FineDeducer.unif
import monix.execution.Scheduler.Implicits.global
import scala.concurrent._
import duration._

import provingground._ , interface._, HoTT._

import learning._

import library._, MonoidSimple._

import FineDeducer.unif

import monix.execution.Scheduler.Implicits.global

import scala.concurrent._

import duration._

In the following section we are defining all the variables we are going to use in the proof.All the variables are terms of type M

val M = "M" ::Type
val a = "a" :: M
val b = "b" :: M
val c = "c" :: M
val d = "d" :: M
val x = "x" :: M
val y = "y" :: M
val z = "z" :: M
val e = "e" :: M
val p = "p" :: M
val q = "q" :: M
val r = "r" :: M
val s = "s" :: M
val t = "t" :: M
val e1 = "e1" :: M
val e2 = "e2" :: M

M: Typ[Term] = M
a: Term = a
b: Term = b
c: Term = c
d: Term = d
x: Term = x
y: Term = y
z: Term = z
e: Term = e
p: Term = p
q: Term = q
r: Term = r
s: Term = s
t: Term = t
e1: Term = e1
e2: Term = e2

In the section below we define the following operators:-

1. eqM - This operation is defined on set $S$ and is equivalent to the Equality operator $i.e$, eqM$($a$)($b$) \iff a=b$.Bascillay treat it as truth assignment.
2. op - This operation is defined on set $S$ and is equivalent to the $*$ operation $i.e$, $op($a$)($b$) \iff a*b$.
3. op_2 - This opeartion is defined on the set $S$ and is used to encompass the associative nature of the binary operation $*$.op_2($a$)($b$)($c$) returns a term $a*b*c$.Now since the operation $*$ is associative therfore any order of bracketting will evalute the same result $i.e$, $(a*b)*c = a*(b*c)$.This is done to avoid the extra information of bracketing.
4. inv - This opeartion is defined on the set $S$ and takes in elements say $x$ and $y$ as inputs and returns the element $z$ such that $x*z=y$ is satisfied.We know that such a mapping exists because of the condition given in the question.

val eqM = "eqM" :: M ->: M ->: Type
val op  = "op" :: M ->: M ->: M
val op_2 = "op_2" :: M ->: M ->: M ->: M
val inv = "inv" :: M ->: M ->: M

eqM: Func[Term, Func[Term, Typ[Term]]] = eqM
op: Func[Term, Func[Term, Term]] = op
op_2: Func[Term, Func[Term, Func[Term, Term]]] = op_2
inv: Func[Term, Func[Term, Term]] = inv

One of the best festures of this notebook is that after this step every step of the proof can be executed independently.

Section0 : Existence Of Identity Element

For the existence of identity we have to prove there exists $x,e \in S $ such that $x*e=x$ then e is called the identity for x.

val one_ :FiniteDistribution[Term] = unif(a,b)(x,e,op,eqM,inv)(
    a ~>: b ~>: (eqM(op(a)(inv(a)(b)))(b))
)*0.5++(FiniteDistribution.unif(op:Term)*0.5)++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(inv:Term)*0.5)
val one_1 = one_.filter((t) => !Set(a, b).contains(t)).normalized()
val ts_0 = TermState(one_1,one_1.map(_.typ))

one_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(x, 0.0625),
    Weighted(e, 0.0625),
    Weighted(op, 0.0625),
    Weighted(eqM, 0.0625),
    Weighted(inv, 0.0625),
    Weighted(
      axiom_{(\prod\limits_{a : M} (\prod\limits_{b : M} eqM(op(a)(inv(a)(b)))(b)))},
      0.0625
    ),
    Weighted(op, 0.5),
    Weighted(eqM, 0.5),
    Weighted(inv, 0.5)
  )
)
one_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.03333333333333333),
    Weighted(e, 0.03333333333333333),
    Weighted(op, 0.03333333333333333),
    Weighted(eqM, 0.03333333333333333),
    Weighted(inv, 0.03333333333333333),
    Weighted(
      axiom_{(\prod\limits_{a : M} (\prod\limits_{b : M} eqM(op(a)(inv(a)(b)))(b)))},
      0.03333333333333333
    ),
    Weighted(op, 0.26666666666666666),
    Weighted(eqM, 0.26666666666666666),
    Weighted(inv, 0.26666666666666666)
  )
)
ts_0: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03333333333333333),
      Weighted(e, 0.03333333333333333),
      Weighted(op, 0.03333333333333333),
      Weighted(eqM, 0.03333333333333333),
      Weighted(inv, 0.03333333333333333),
      Weighted(
        axiom_{(\prod\limits_{a : M} (\prod\limits_{b : M} eqM(op(a)(inv(a)(b)))(b)))},
        0.03333333333333333
      ),
      Weighted(op, 0.26666666666666666),
      Weighted(eqM, 0.26666666666666666),
      Weighted(inv, 0.26666666666666666)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03333333333333333),
      Weighted(M, 0.03333333333333333),
      Weighted((M → (M → M)), 0.03333333333333333),
      Weighted((M → (M → 𝒰 )), 0.03333333333333333),
      Weighted((M → (M → M)), 0.03333333333333333),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(op(a)(inv(a)(b)))(b) } },
        0.03333333333333333
      ),
      Weighted((M → (M → M)), 0.26666666666666666),
      Weighted((M → (M → 𝒰 )), 0.26666666666666666),
      Weighted((M → (M → M)), 0.26666666666666666)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

val lp_0 = LocalProver(ts_0,cutoff = 5*math.pow(10,-6)).noIsles

lp_0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03333333333333333),
        Weighted(e, 0.03333333333333333),
        Weighted(op, 0.03333333333333333),
        Weighted(eqM, 0.03333333333333333),
        Weighted(inv, 0.03333333333333333),
        Weighted(
          axiom_{(\prod\limits_{a : M} (\prod\limits_{b : M} eqM(op(a)(inv(a)(b)))(b)))},
          0.03333333333333333
        ),
        Weighted(op, 0.26666666666666666),
        Weighted(eqM, 0.26666666666666666),
        Weighted(inv, 0.26666666666666666)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03333333333333333),
        Weighted(M, 0.03333333333333333),
        Weighted((M → (M → M)), 0.03333333333333333),
        Weighted((M → (M → 𝒰 )), 0.03333333333333333),
        Weighted((M → (M → M)), 0.03333333333333333),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(inv(a)(b)))(b) } },
          0.03333333333333333
        ),
        Weighted((M → (M → M)), 0.26666666666666666),
        Weighted((M → (M → 𝒰 )), 0.26666666666666666),
        Weighted((M → (M → M)), 0.26666666666666666)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
...

val lem_0 = lp_0.lemmas.runSyncUnsafe()

lem_0: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(e)(inv(e)(x)))(x), 9.774035574270451E-6),
  (eqM(op(x)(inv(x)(e)))(e), 9.774035574270451E-6),
  (eqM(op(x)(inv(x)(x)))(x), 9.774035574270451E-6),
  (eqM(op(e)(inv(e)(e)))(e), 9.774035574270451E-6)
)

Section1 : Existence Of Universal Identity

Step1:

$$(x*e)=x \implies (x*e)*inv(x)(y)=x*inv(x)(y)$$

val zero: FiniteDistribution[Term] = unif(a,b,c,d)(op(x)(e),x,inv(x)(y),op,eqM)(
    eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c)),
    eqM(op(x)(e))(x)
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term)*0.5) ++(FiniteDistribution.unif(op: Term)*0.25) 
val zero1 = zero.filter((t) => !Set(a, b, c, d).contains(t)).normalized()
val ts_ = TermState(zero1,zero1.map(_.typ))
val ts_1 = TermState(zero1,zero1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(e))(x) ->: eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))))

zero: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(d, 0.045454545454545456),
    Weighted(op(x)(e), 0.045454545454545456),
    Weighted(x, 0.045454545454545456),
    Weighted(inv(x)(y), 0.045454545454545456),
    Weighted(op, 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
      0.045454545454545456
    ),
    Weighted(axiom_{eqM(op(x)(e))(x)}, 0.045454545454545456),
    Weighted(eqM, 0.5),
    Weighted(op, 0.25)
  )
)
zero1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op(x)(e), 0.0425531914893617),
    Weighted(x, 0.0425531914893617),
    Weighted(inv(x)(y), 0.0425531914893617),
    Weighted(op, 0.0425531914893617),
    Weighted(eqM, 0.0425531914893617),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
      0.0425531914893617
    ),
    Weighted(axiom_{eqM(op(x)(e))(x)}, 0.0425531914893617),
    Weighted(eqM, 0.4680851063829787),
    Weighted(op, 0.23404255319148934)
  )
)
ts_: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(x)(e), 0.0425531914893617),
      Weighted(x, 0.0425531914893617),
      Weighted(inv(x)(y), 0.0425531914893617),
      Weighted(op, 0.0425531914893617),
      Weighted(eqM, 0.0425531914893617),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
        0.0425531914893617
      ),
      Weighted(axiom_{eqM(op(x)(e))(x)}, 0.0425531914893617),
      Weighted(eqM, 0.4680851063829787),
      Weighted(op, 0.23404255319148934)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.0425531914893617),
      Weighted(M, 0.0425531914893617),
      Weighted(M, 0.0425531914893617),
      Weighted((M → (M → M)), 0.0425531914893617),
      Weighted((M → (M → 𝒰 )), 0.0425531914893617),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
        0.0425531914893617
      ),
      Weighted(eqM(op(x)(e))(x), 0.0425531914893617),
      Weighted((M → (M → 𝒰 )), 0.4680851063829787),
      Weighted((M → (M → M)), 0.23404255319148934)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(x)(e), 0.0425531914893617),
      Weighted(x, 0.0425531914893617),
      Weighted(inv(x)(y), 0.0425531914893617),
      Weighted(op, 0.0425531914893617),
      Weighted(eqM, 0.0425531914893617),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
        0.0425531914893617
      ),
      Weighted(axiom_{eqM(op(x)(e))(x)}, 0.0425531914893617),
      Weighted(eqM, 0.4680851063829787),
      Weighted(op, 0.23404255319148934)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.0425531914893617),
      Weighted(M, 0.0425531914893617),
      Weighted(M, 0.0425531914893617),
      Weighted((M → (M → M)), 0.0425531914893617),
      Weighted((M → (M → 𝒰 )), 0.0425531914893617),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
        0.0425531914893617
      ),
      Weighted(eqM(op(x)(e))(x), 0.0425531914893617),
      Weighted((M → (M → 𝒰 )), 0.4680851063829787),
      Weighted((M → (M → M)), 0.23404255319148934)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(
...

val lp_ = LocalProver(ts_,cutoff=5*math.pow(10,-6)).noIsles
val lp_1 = LocalProver(ts_1,cutoff=5*math.pow(10,-6)).noIsles

lp_: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(x)(e), 0.0425531914893617),
        Weighted(x, 0.0425531914893617),
        Weighted(inv(x)(y), 0.0425531914893617),
        Weighted(op, 0.0425531914893617),
        Weighted(eqM, 0.0425531914893617),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
          0.0425531914893617
        ),
        Weighted(axiom_{eqM(op(x)(e))(x)}, 0.0425531914893617),
        Weighted(eqM, 0.4680851063829787),
        Weighted(op, 0.23404255319148934)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.0425531914893617),
        Weighted(M, 0.0425531914893617),
        Weighted(M, 0.0425531914893617),
        Weighted((M → (M → M)), 0.0425531914893617),
        Weighted((M → (M → 𝒰 )), 0.0425531914893617),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
          0.0425531914893617
        ),
        Weighted(eqM(op(x)(e))(x), 0.0425531914893617),
        Weighted((M → (M → 𝒰 )), 0.4680851063829787),
        Weighted((M → (M → M)), 0.23404255319148934)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
...
lp_1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(x)(e), 0.0425531914893617),
        Weighted(x, 0.0425531914893617),
        Weighted(inv(x)(y), 0.0425531914893617),
        Weighted(op, 0.0425531914893617),
        Weighted(eqM, 0.0425531914893617),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
          0.0425531914893617
        ),
        Weighted(axiom_{eqM(op(x)(e))(x)}, 0.0425531914893617),
        Weighted(eqM, 0.4680851063829787),
        Weighted(op, 0.23404255319148934)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.0425531914893617),
        Weighted(M, 0.0425531914893617),
        Weighted(M, 0.0425531914893617),
        Weighted((M → (M → M)), 0.0425531914893617),
        Weighted((M → (M → 𝒰 )), 0.0425531914893617),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
          0.0425531914893617
        ),
        Weighted(eqM(op(x)(e))(x), 0.0425531914893617),
        Weighted((M → (M → 𝒰 )), 0.4680851063829787),
        Weighted((M → (M → M)), 0.23404255319148934)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
...

Importance Of Including Goal in Term State

We will see that when we do not put goals in the TermState then the prover generates the desired lemma with low wieghtage or does not generate the desired and some time even does not genrate any lemma(this is the case is when the cutoff is set very low is order to capture the desired lemma but before the program could finish the generation of lemmas the program timeouts).This is common when many terms and axioms are given to the prover.Including goals becomes a crucial part in these cases as they drastically change the wieghtage of terms and hence change the generation process too.Thus helping the prover in generation of desired lemma.

val lem_ = lp_.lemmas.runSyncUnsafe()

lem_: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(e))(op(x)(e)))(op(x)(op(x)(e))), 1.0137580491037564E-5),
  (eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))), 1.0137580491037564E-5),
  (eqM(op(op(x)(e))(x))(op(x)(x)), 1.0137580491037564E-5)
)

val lem_1 = lp_1.lemmas.runSyncUnsafe()

lem_1: Vector[(Typ[Term], Double)] = Vector(
  (
    (eqM(op(x)(e))(x) → eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))),
    0.894125408326361
  ),
  (eqM(op(op(x)(e))(op(x)(e)))(op(x)(op(x)(e))), 9.207734038248953E-6),
  (eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))), 9.207734038248953E-6),
  (eqM(op(op(x)(e))(x))(op(x)(x)), 9.207734038248953E-6)
)

Step2:

$$(x*e)*inv(x)(y) = x*(e*inv(x)(y))$$

val negative1_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y),eqM,op)(
   eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative1_1 = negative1_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_3 = TermState(negative1_1,negative1_1.map(_.typ))
val ts_4 = TermState(negative1_1,negative1_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))))

negative1_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(x, 0.05555555555555555),
    Weighted(e, 0.05555555555555555),
    Weighted(inv(x)(y), 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(op, 0.05555555555555555),
    Weighted(axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))}, 0.05555555555555555),
    Weighted(eqM, 0.7),
    Weighted(op, 0.9)
  )
)
negative1_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.028735632183908046),
    Weighted(e, 0.028735632183908046),
    Weighted(inv(x)(y), 0.028735632183908046),
    Weighted(eqM, 0.028735632183908046),
    Weighted(op, 0.028735632183908046),
    Weighted(
      axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
      0.028735632183908046
    ),
    Weighted(eqM, 0.3620689655172414),
    Weighted(op, 0.4655172413793104)
  )
)
ts_3: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.028735632183908046),
      Weighted(e, 0.028735632183908046),
      Weighted(inv(x)(y), 0.028735632183908046),
      Weighted(eqM, 0.028735632183908046),
      Weighted(op, 0.028735632183908046),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.028735632183908046
      ),
      Weighted(eqM, 0.3620689655172414),
      Weighted(op, 0.4655172413793104)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.028735632183908046),
      Weighted(M, 0.028735632183908046),
      Weighted(M, 0.028735632183908046),
      Weighted((M → (M → 𝒰 )), 0.028735632183908046),
      Weighted((M → (M → M)), 0.028735632183908046),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.028735632183908046
      ),
      Weighted((M → (M → 𝒰 )), 0.3620689655172414),
      Weighted((M → (M → M)), 0.4655172413793104)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_4: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.028735632183908046),
      Weighted(e, 0.028735632183908046),
      Weighted(inv(x)(y), 0.028735632183908046),
      Weighted(eqM, 0.028735632183908046),
      Weighted(op, 0.028735632183908046),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.028735632183908046
      ),
      Weighted(eqM, 0.3620689655172414),
      Weighted(op, 0.4655172413793104)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.028735632183908046),
      Weighted(M, 0.028735632183908046),
      Weighted(M, 0.028735632183908046),
      Weighted((M → (M → 𝒰 )), 0.028735632183908046),
      Weighted((M → (M → M)), 0.028735632183908046),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.028735632183908046
      ),
      Weighted((M → (M → 𝒰 )), 0.3620689655172414),
      Weighted((M → (M → M)), 0.4655172413793104)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y)))), 1.0))
  ),
  Empty
)

val lp_2 = LocalProver(ts_3,cutoff=5*math.pow(10,-6)).noIsles
val lp_3 = LocalProver(ts_4,cutoff=5*math.pow(10,-6)).noIsles
val lp_4 = LocalProver(ts_3,cutoff=math.pow(10,-6)).noIsles

val lem_2 = lp_2.lemmas.runSyncUnsafe()

lem_3: Vector[(Typ[Term], Double)] = Vector()

There were a large number of terms in the term state so the expexted lemmas had too low wieghtage to get generated.Thus no lemma was generated.So now we try to generate the desired lemma by,

• Adding goal to the term state and not lowering the cutoff.
• Lowering the cutoff and not including goals as a part of Term State
.

val lem_3 = lp_3.lemmas.runSyncUnsafe()

lem_4: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y)))), 0.8884378382021705)
)

val lem_4 = lp_4.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd15$Helper.<init>(cmd15.sc:1)
  ammonite.$sess.cmd15$.<init>(cmd15.sc:7)
  ammonite.$sess.cmd15$.<clinit>(cmd15.sc:-1)

Step3:

$$e*inv(x)(y)=inv(x)(y)*e $$ $$\implies x*(e*inv(x)(y)) = x*(inv(x)(y)*e) \\$$

val negative2_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y),eqM,op)(
    eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
    eqM(op(a)(b))(op(b)(a))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.3)++(FiniteDistribution.unif(op:Term,eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)))*0.9)
val negative2_1 = negative2_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_5 = TermState(negative2_1,negative2_1.map(_.typ))
val ts_6 = TermState(negative2_1,negative2_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))))

negative2_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05),
    Weighted(b, 0.05),
    Weighted(c, 0.05),
    Weighted(x, 0.05),
    Weighted(e, 0.05),
    Weighted(inv(x)(y), 0.05),
    Weighted(eqM, 0.05),
    Weighted(op, 0.05),
    Weighted(axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))}, 0.05),
    Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05),
    Weighted(eqM, 0.3),
    Weighted(op, 0.45),
    Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.45)
  )
)
negative2_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.03225806451612904),
    Weighted(e, 0.03225806451612904),
    Weighted(inv(x)(y), 0.03225806451612904),
    Weighted(eqM, 0.03225806451612904),
    Weighted(op, 0.03225806451612904),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
      0.03225806451612904
    ),
    Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
    Weighted(eqM, 0.19354838709677422),
    Weighted(op, 0.29032258064516137),
    Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
  )
)
ts_5: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03225806451612904),
      Weighted(e, 0.03225806451612904),
      Weighted(inv(x)(y), 0.03225806451612904),
      Weighted(eqM, 0.03225806451612904),
      Weighted(op, 0.03225806451612904),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.03225806451612904
      ),
      Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
      Weighted(eqM, 0.19354838709677422),
      Weighted(op, 0.29032258064516137),
      Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03225806451612904),
      Weighted(M, 0.03225806451612904),
      Weighted(M, 0.03225806451612904),
      Weighted((M → (M → 𝒰 )), 0.03225806451612904),
      Weighted((M → (M → M)), 0.03225806451612904),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.03225806451612904
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
        0.03225806451612904
      ),
      Weighted((M → (M → 𝒰 )), 0.19354838709677422),
      Weighted((M → (M → M)), 0.29032258064516137),
      Weighted(𝒰 , 0.29032258064516137)
    )
  ),
...
ts_6: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03225806451612904),
      Weighted(e, 0.03225806451612904),
      Weighted(inv(x)(y), 0.03225806451612904),
      Weighted(eqM, 0.03225806451612904),
      Weighted(op, 0.03225806451612904),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.03225806451612904
      ),
      Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
      Weighted(eqM, 0.19354838709677422),
      Weighted(op, 0.29032258064516137),
      Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03225806451612904),
      Weighted(M, 0.03225806451612904),
      Weighted(M, 0.03225806451612904),
      Weighted((M → (M → 𝒰 )), 0.03225806451612904),
      Weighted((M → (M → M)), 0.03225806451612904),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.03225806451612904
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
        0.03225806451612904
      ),
      Weighted((M → (M → 𝒰 )), 0.19354838709677422),
      Weighted((M → (M → M)), 0.29032258064516137),
      Weighted(𝒰 , 0.29032258064516137)
    )
  ),
...

val tg = TermGenParams(unAppW=0.3)
val tg1 = TermGenParams(appW=0.3)
val tg2 = TermGenParams(unAppW=0.2,appW = 0.2)
val tg3 = TermGenParams(appW = 0.2)
val tg4 = TermGenParams(unAppW = 0.2)
val lp_5 = LocalProver(ts_6,cutoff=5*math.pow(10,-6)).noIsles
val lp_6 = LocalProver(ts_6,tg,cutoff=5*math.pow(10,-5)).noIsles
val lp_7 = LocalProver(ts_6,tg1,cutoff=5*math.pow(10,-6)).noIsles
val lp_8 = LocalProver(ts_6,tg2,cutoff=5*math.pow(10,-6)).noIsles
val lp_9 = LocalProver(ts_6,tg,cutoff=8*math.pow(10,-6)).noIsles
val lp_10 = LocalProver(ts_6,tg1,cutoff=8*math.pow(10,-6)).noIsles
val lp_11 = LocalProver(ts_6,tg2,cutoff=8*math.pow(10,-6)).noIsles
val lp_12 = LocalProver(ts_6,tg3,cutoff=math.pow(10,-5)).noIsles
val lp_13 = LocalProver(ts_6,tg3,cutoff=8*math.pow(10,-5)).noIsles
val lp_14 = LocalProver(ts_6,tg4,cutoff=5*math.pow(10,-5)).noIsles
val lp_15 = LocalProver(ts_6,tg4,cutoff=3*math.pow(10,-5)).noIsles

tg: TermGenParams = TermGenParams(
  0.1,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg1: TermGenParams = TermGenParams(
  0.3,
  0.1,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg2: TermGenParams = TermGenParams(
  0.2,
  0.2,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg3: TermGenParams = TermGenParams(
  0.2,
  0.1,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg4: TermGenParams = TermGenParams(
  0.1,
  0.2,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_5: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_6: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_7: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_8: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_9: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_10: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_11: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_12: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_13: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_14: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...
lp_15: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03225806451612904),
        Weighted(e, 0.03225806451612904),
        Weighted(inv(x)(y), 0.03225806451612904),
        Weighted(eqM, 0.03225806451612904),
        Weighted(op, 0.03225806451612904),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03225806451612904
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.03225806451612904),
        Weighted(eqM, 0.19354838709677422),
        Weighted(op, 0.29032258064516137),
        Weighted((eqM(a)(b) → eqM(op(c)(a))(op(c)(b))), 0.29032258064516137)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted(M, 0.03225806451612904),
        Weighted((M → (M → 𝒰 )), 0.03225806451612904),
        Weighted((M → (M → M)), 0.03225806451612904),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03225806451612904
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.03225806451612904
        ),
        Weighted((M → (M → 𝒰 )), 0.19354838709677422),
        Weighted((M → (M → M)), 0.29032258064516137),
        Weighted(𝒰 , 0.29032258064516137)
      )
...

val lem_5 = lp_5.lemmas.runSyncUnsafe()

lem_5: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(inv(x)(y)))(op(inv(x)(y))(x)), 1.0798085676176734E-5),
  (
    eqM(op(inv(x)(y))(inv(x)(y)))(op(inv(x)(y))(inv(x)(y))),
    1.0798085676176734E-5
  ),
  (eqM(op(x)(x))(op(x)(x)), 1.0798085676176734E-5),
  (eqM(op(x)(e))(op(e)(x)), 1.0798085676176734E-5),
  (eqM(op(e)(x))(op(x)(e)), 1.0798085676176734E-5),
  (eqM(op(e)(e))(op(e)(e)), 1.0798085676176734E-5),
  (eqM(op(inv(x)(y))(e))(op(e)(inv(x)(y))), 1.0798085676176734E-5),
  (eqM(op(inv(x)(y))(x))(op(x)(inv(x)(y))), 1.0798085676176734E-5),
  (eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 1.0798085676176734E-5)
)

val lem_6 = lp_6.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd18$Helper.<init>(cmd18.sc:1)
  ammonite.$sess.cmd18$.<init>(cmd18.sc:7)
  ammonite.$sess.cmd18$.<clinit>(cmd18.sc:-1)

val lem_7 = lp_7.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd23$Helper.<init>(cmd23.sc:1)
  ammonite.$sess.cmd23$.<init>(cmd23.sc:7)
  ammonite.$sess.cmd23$.<clinit>(cmd23.sc:-1)

val lem_8 = lp_8.lemmas.runSyncUnsafe()

val lem_9 = lp_9.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)
java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:633)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd26$Helper.<init>(cmd26.sc:1)
  ammonite.$sess.cmd26$.<init>(cmd26.sc:7)
  ammonite.$sess.cmd26$.<clinit>(cmd26.sc:-1)

val lem_10 = lp_10.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)
java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:633)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)
java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:633)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd25$Helper.<init>(cmd25.sc:1)
  ammonite.$sess.cmd25$.<init>(cmd25.sc:7)
  ammonite.$sess.cmd25$.<clinit>(cmd25.sc:-1)

val lem_11 = lp_11.lemmas.runSyncUnsafe()

val lem_12 = lp_12.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
	at monix.eval.Task.timeout(Task.scala:2220)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
	at provingground.learning.MonixFiniteDistributionEq.$anonfun$nodeDist$2(MonixFiniteDistributionEq.scala:584)
	at scala.Option.getOrElse(Option.scala:189)
	at provingground.learning.MonixFiniteDistributionEq.nodeDist(MonixFiniteDistributionEq.scala:350)
	at provingground.learning.GenMonixFiniteDistributionEq.nodeCoeffDist(MonixFiniteDistributionEq.scala:183)
	at provingground.learning.GenMonixFiniteDistributionEq.$anonfun$nodeCoeffDist$4(MonixFiniteDistributionEq.scala:197)
	at monix.eval.internal.TaskRunLoop$.startFull(TaskRunLoop.scala:170)
	at monix.eval.internal.TaskRunLoop$.$anonfun$restartAsync$1(TaskRunLoop.scala:222)
	at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(Unknown Source)
	at java.util.concurrent.ForkJoinTask.doExec(Unknown Source)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(Unknown Source)
	at java.util.concurrent.ForkJoinPool.runWorker(Unknown Source)
	at java.util.concurrent.ForkJoinWorkerThread.run(Unknown Source)

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd28$Helper.<init>(cmd28.sc:1)
  ammonite.$sess.cmd28$.<init>(cmd28.sc:7)
  ammonite.$sess.cmd28$.<clinit>(cmd28.sc:-1)

val lem_13 = lp_13.lemmas.runSyncUnsafe()

lem_13: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(inv(x)(y)))(op(inv(x)(y))(x)), 1.2228198738523114E-5),
  (
    eqM(op(inv(x)(y))(inv(x)(y)))(op(inv(x)(y))(inv(x)(y))),
    1.2228198738523114E-5
  ),
  (eqM(op(x)(x))(op(x)(x)), 1.2228198738523114E-5),
  (eqM(op(x)(e))(op(e)(x)), 1.2228198738523114E-5),
  (eqM(op(e)(x))(op(x)(e)), 1.2228198738523114E-5),
  (eqM(op(e)(e))(op(e)(e)), 1.2228198738523114E-5),
  (eqM(op(inv(x)(y))(e))(op(e)(inv(x)(y))), 1.2228198738523114E-5),
  (eqM(op(inv(x)(y))(x))(op(x)(inv(x)(y))), 1.2228198738523114E-5),
  (eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 1.2228198738523114E-5)
)

val lem_14 = lp_14.lemmas.runSyncUnsafe()

lem_14: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(inv(x)(y)))(op(inv(x)(y))(x)), 1.2153081495026338E-5),
  (
    eqM(op(inv(x)(y))(inv(x)(y)))(op(inv(x)(y))(inv(x)(y))),
    1.2153081495026338E-5
  ),
  (eqM(op(x)(x))(op(x)(x)), 1.2153081495026338E-5),
  (eqM(op(x)(e))(op(e)(x)), 1.2153081495026338E-5),
  (eqM(op(e)(x))(op(x)(e)), 1.2153081495026338E-5),
  (eqM(op(e)(e))(op(e)(e)), 1.2153081495026338E-5),
  (eqM(op(inv(x)(y))(e))(op(e)(inv(x)(y))), 1.2153081495026338E-5),
  (eqM(op(inv(x)(y))(x))(op(x)(inv(x)(y))), 1.2153081495026338E-5),
  (eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 1.2153081495026338E-5)
)

val lem_15=lp_15.lemmas.runSyncUnsafe()

lem_15: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(inv(x)(y)))(op(inv(x)(y))(x)), 1.2273495253360917E-5),
  (
    eqM(op(inv(x)(y))(inv(x)(y)))(op(inv(x)(y))(inv(x)(y))),
    1.2273495253360917E-5
  ),
  (eqM(op(x)(x))(op(x)(x)), 1.2273495253360917E-5),
  (eqM(op(x)(e))(op(e)(x)), 1.2273495253360917E-5),
  (eqM(op(e)(x))(op(x)(e)), 1.2273495253360917E-5),
  (eqM(op(e)(e))(op(e)(e)), 1.2273495253360917E-5),
  (eqM(op(inv(x)(y))(e))(op(e)(inv(x)(y))), 1.2273495253360917E-5),
  (eqM(op(inv(x)(y))(x))(op(x)(inv(x)(y))), 1.2273495253360917E-5),
  (eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 1.2273495253360917E-5)
)

In the above cases we could clearly see that either the prover is only using the commutivity axiom to produce lemmas or it is not producing any.In the above case various combination of Term generation parameters as well as cutoff levels were tested in hope of obtaining the desired lemma.In the coming sections of the proof we will see that a similar situation ocuurs where prover has to use a axiom to generate some terms which will be used with some other axiom to generate the desired lemma.In some cases the prover would succesfully generate the lemmas because the number of terms in the Term State were fairly less.

val negative3_ : FiniteDistribution[Term] = unif(a,b,c)(x,inv(x)(y),e,eqM,op)(
    eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
    eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))
)*0.5++(FiniteDistribution.unif(eqM:Term,op:Term)*0.5)
val negative3_1 = negative3_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_7 = TermState(negative3_1,negative3_1.map(_.typ))
val ts_8 = TermState(negative3_1,negative3_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))))

negative3_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05),
    Weighted(b, 0.05),
    Weighted(c, 0.05),
    Weighted(x, 0.05),
    Weighted(inv(x)(y), 0.05),
    Weighted(e, 0.05),
    Weighted(eqM, 0.05),
    Weighted(op, 0.05),
    Weighted(axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))}, 0.05),
    Weighted(axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))}, 0.05),
    Weighted(eqM, 0.25),
    Weighted(op, 0.25)
  )
)
negative3_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.05882352941176471),
    Weighted(inv(x)(y), 0.05882352941176471),
    Weighted(e, 0.05882352941176471),
    Weighted(eqM, 0.05882352941176471),
    Weighted(op, 0.05882352941176471),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
      0.05882352941176471
    ),
    Weighted(
      axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
      0.05882352941176471
    ),
    Weighted(eqM, 0.29411764705882354),
    Weighted(op, 0.29411764705882354)
  )
)
ts_7: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.05882352941176471),
      Weighted(inv(x)(y), 0.05882352941176471),
      Weighted(e, 0.05882352941176471),
      Weighted(eqM, 0.05882352941176471),
      Weighted(op, 0.05882352941176471),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.05882352941176471
      ),
      Weighted(
        axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
        0.05882352941176471
      ),
      Weighted(eqM, 0.29411764705882354),
      Weighted(op, 0.29411764705882354)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.05882352941176471),
      Weighted(M, 0.05882352941176471),
      Weighted(M, 0.05882352941176471),
      Weighted((M → (M → 𝒰 )), 0.05882352941176471),
      Weighted((M → (M → M)), 0.05882352941176471),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.05882352941176471
      ),
      Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
      Weighted((M → (M → 𝒰 )), 0.29411764705882354),
      Weighted((M → (M → M)), 0.29411764705882354)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...
ts_8: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.05882352941176471),
      Weighted(inv(x)(y), 0.05882352941176471),
      Weighted(e, 0.05882352941176471),
      Weighted(eqM, 0.05882352941176471),
      Weighted(op, 0.05882352941176471),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.05882352941176471
      ),
      Weighted(
        axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
        0.05882352941176471
      ),
      Weighted(eqM, 0.29411764705882354),
      Weighted(op, 0.29411764705882354)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.05882352941176471),
      Weighted(M, 0.05882352941176471),
      Weighted(M, 0.05882352941176471),
      Weighted((M → (M → 𝒰 )), 0.05882352941176471),
      Weighted((M → (M → M)), 0.05882352941176471),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.05882352941176471
      ),
      Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
      Weighted((M → (M → 𝒰 )), 0.29411764705882354),
      Weighted((M → (M → M)), 0.29411764705882354)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...

val tg5 = TermGenParams(unAppW=0.3)
val tg6 = TermGenParams(appW=0.2)
val lp_16 = LocalProver(ts_8,cutoff=5*math.pow(10,-6)).noIsles
val lp_17 = LocalProver(ts_7,cutoff=5*math.pow(10,-6)).noIsles
val lp_18 = LocalProver(ts_7,tg5,cutoff=5*math.pow(10,-6)).noIsles
val lp_19 = LocalProver(ts_7,tg6,cutoff=9*math.pow(10,-5)).noIsles

tg5: TermGenParams = TermGenParams(
  0.1,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg6: TermGenParams = TermGenParams(
  0.2,
  0.1,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_16: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.05882352941176471),
        Weighted(inv(x)(y), 0.05882352941176471),
        Weighted(e, 0.05882352941176471),
        Weighted(eqM, 0.05882352941176471),
        Weighted(op, 0.05882352941176471),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.05882352941176471
        ),
        Weighted(
          axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
          0.05882352941176471
        ),
        Weighted(eqM, 0.29411764705882354),
        Weighted(op, 0.29411764705882354)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.05882352941176471),
        Weighted((M → (M → M)), 0.05882352941176471),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.05882352941176471
        ),
        Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.29411764705882354),
        Weighted((M → (M → M)), 0.29411764705882354)
      )
    ),
    Vector(),
...
lp_17: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.05882352941176471),
        Weighted(inv(x)(y), 0.05882352941176471),
        Weighted(e, 0.05882352941176471),
        Weighted(eqM, 0.05882352941176471),
        Weighted(op, 0.05882352941176471),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.05882352941176471
        ),
        Weighted(
          axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
          0.05882352941176471
        ),
        Weighted(eqM, 0.29411764705882354),
        Weighted(op, 0.29411764705882354)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.05882352941176471),
        Weighted((M → (M → M)), 0.05882352941176471),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.05882352941176471
        ),
        Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.29411764705882354),
        Weighted((M → (M → M)), 0.29411764705882354)
      )
    ),
    Vector(),
...
lp_18: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.05882352941176471),
        Weighted(inv(x)(y), 0.05882352941176471),
        Weighted(e, 0.05882352941176471),
        Weighted(eqM, 0.05882352941176471),
        Weighted(op, 0.05882352941176471),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.05882352941176471
        ),
        Weighted(
          axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
          0.05882352941176471
        ),
        Weighted(eqM, 0.29411764705882354),
        Weighted(op, 0.29411764705882354)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.05882352941176471),
        Weighted((M → (M → M)), 0.05882352941176471),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.05882352941176471
        ),
        Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.29411764705882354),
        Weighted((M → (M → M)), 0.29411764705882354)
      )
    ),
    Vector(),
...
lp_19: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.05882352941176471),
        Weighted(inv(x)(y), 0.05882352941176471),
        Weighted(e, 0.05882352941176471),
        Weighted(eqM, 0.05882352941176471),
        Weighted(op, 0.05882352941176471),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.05882352941176471
        ),
        Weighted(
          axiom_{eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))},
          0.05882352941176471
        ),
        Weighted(eqM, 0.29411764705882354),
        Weighted(op, 0.29411764705882354)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted(M, 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.05882352941176471),
        Weighted((M → (M → M)), 0.05882352941176471),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.05882352941176471
        ),
        Weighted(eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e)), 0.05882352941176471),
        Weighted((M → (M → 𝒰 )), 0.29411764705882354),
        Weighted((M → (M → M)), 0.29411764705882354)
      )
    ),
    Vector(),
...

val lem_16 = lp_16.lemmas.runSyncUnsafe()

lem_16: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e))), 0.9019150346958225)
)

val lem_17 = lp_17.lemmas.runSyncUnsafe()

lem_17: Vector[(Typ[Term], Double)] = Vector()

val lem_18 = lp_18.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd24$Helper.<init>(cmd24.sc:1)
  ammonite.$sess.cmd24$.<init>(cmd24.sc:7)
  ammonite.$sess.cmd24$.<clinit>(cmd24.sc:-1)

val lem_19 = lp_19.lemmas.runSyncUnsafe()

lem_19: Vector[(Typ[Term], Double)] = Vector()

Step4:

$$x*(inv(x)(y)*e)=(x*inv(x)(y))*e$$

Part 1:

$$(x*inv(x)(y))*e=x*(inv(x)(y)*e)$$

val negative4_ : FiniteDistribution[Term] = unif(a,b,c)(x,inv(x)(y),e)(
   eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative4_1 = negative4_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_9 = TermState(negative4_1,negative4_1.map(_.typ))
val ts_10 = TermState(negative4_1,negative4_1.map(_.typ),goals = FiniteDistribution.unif(a ~>:  b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))))
val ts_11 = TermState(negative4_1,negative4_1.map(_.typ))
val ts_12 = TermState(negative4_1,negative4_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))))

negative4_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.07142857142857142),
    Weighted(b, 0.07142857142857142),
    Weighted(c, 0.07142857142857142),
    Weighted(x, 0.07142857142857142),
    Weighted(inv(x)(y), 0.07142857142857142),
    Weighted(e, 0.07142857142857142),
    Weighted(axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))}, 0.07142857142857142),
    Weighted(eqM, 0.7),
    Weighted(op, 0.9)
  )
)
negative4_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.03787878787878787),
    Weighted(inv(x)(y), 0.03787878787878787),
    Weighted(e, 0.03787878787878787),
    Weighted(axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))}, 0.03787878787878787),
    Weighted(eqM, 0.37121212121212116),
    Weighted(op, 0.47727272727272724)
  )
)
ts_9: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03787878787878787),
      Weighted(inv(x)(y), 0.03787878787878787),
      Weighted(e, 0.03787878787878787),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.03787878787878787
      ),
      Weighted(eqM, 0.37121212121212116),
      Weighted(op, 0.47727272727272724)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.03787878787878787
      ),
      Weighted((M → (M → 𝒰 )), 0.37121212121212116),
      Weighted((M → (M → M)), 0.47727272727272724)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_10: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03787878787878787),
      Weighted(inv(x)(y), 0.03787878787878787),
      Weighted(e, 0.03787878787878787),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.03787878787878787
      ),
      Weighted(eqM, 0.37121212121212116),
      Weighted(op, 0.47727272727272724)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.03787878787878787
      ),
      Weighted((M → (M → 𝒰 )), 0.37121212121212116),
      Weighted((M → (M → M)), 0.47727272727272724)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
        1.0
      )
    )
  ),
...
ts_11: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03787878787878787),
      Weighted(inv(x)(y), 0.03787878787878787),
      Weighted(e, 0.03787878787878787),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.03787878787878787
      ),
      Weighted(eqM, 0.37121212121212116),
      Weighted(op, 0.47727272727272724)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.03787878787878787
      ),
      Weighted((M → (M → 𝒰 )), 0.37121212121212116),
      Weighted((M → (M → M)), 0.47727272727272724)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_12: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03787878787878787),
      Weighted(inv(x)(y), 0.03787878787878787),
      Weighted(e, 0.03787878787878787),
      Weighted(
        axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
        0.03787878787878787
      ),
      Weighted(eqM, 0.37121212121212116),
      Weighted(op, 0.47727272727272724)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(M, 0.03787878787878787),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
        0.03787878787878787
      ),
      Weighted((M → (M → 𝒰 )), 0.37121212121212116),
      Weighted((M → (M → M)), 0.47727272727272724)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))), 1.0))
  ),
  Empty
)

val tg7= TermGenParams(unAppW=0.3)
val lp_20=LocalProver(ts_10,tg7,cutoff=3*math.pow(10,-6),limit=10000.minutes).noIsles
val lp_21=LocalProver(ts_10,tg7,cutoff=5*math.pow(10,-6),limit=1000.minutes).noIsles
val lp_22=LocalProver(ts_12,cutoff=5*math.pow(10,-6),limit=1000.minutes).noIsles
val lp_23=LocalProver(ts_12,tg7,cutoff=5*math.pow(10,-6)).noIsles
val lp_24 = LocalProver(ts_10,cutoff=5*math.pow(10,-6)).noIsles
val lp_25 = LocalProver(ts_9,cutoff =1*math.pow(10,-6)).noIsles

tg7: TermGenParams = TermGenParams(
  0.1,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg8: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.1,
  0.1,
  0.3,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_20: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
          1.0
        )
      )
    ),
...
lp_21: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
          1.0
        )
      )
    ),
...
lp_22: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))), 1.0)
      )
    ),
    Empty
  ),
  TermGenParams(
    0.1,
...
lp_23: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))), 1.0)
      )
    ),
    Empty
  ),
  TermGenParams(
    0.1,
...
lp_24: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
          1.0
        )
      )
    ),
...
lp_25: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))},
          0.05555555555555556
        ),
        Weighted(axiom_{eqM(op(a)(b))(op(b)(a))}, 0.05555555555555556),
        Weighted(eqM, 0.3888888888888889),
        Weighted(op, 0.5)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } },
          0.05555555555555556
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(op(a)(b))(op(b)(a)) } },
          0.05555555555555556
        ),
        Weighted((M → (M → 𝒰 )), 0.3888888888888889),
        Weighted((M → (M → M)), 0.5)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.0,
    0.0,
...

val lem_20 = lp_20.lemmas.runSyncUnsafe()

java.lang.OutOfMemoryError: Java heap space

val lem_22=lp_22.lemmas.runSyncUnsafe()

lem_22: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))), 0.8884378382021705)
)

val lem_21 = lp_21.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 60 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd13$Helper.<init>(cmd13.sc:1)
  ammonite.$sess.cmd13$.<init>(cmd13.sc:7)
  ammonite.$sess.cmd13$.<clinit>(cmd13.sc:-1)

val lem_25 = lp_25.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd20$Helper.<init>(cmd20.sc:1)
  ammonite.$sess.cmd20$.<init>(cmd20.sc:7)
  ammonite.$sess.cmd20$.<clinit>(cmd20.sc:-1)

Part 2:

$$x*(inv(x)(y)*e)=(x*inv(x)(y))*e$$

val negative5_ : FiniteDistribution[Term] = unif(a,b,c)()(
   eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
   eqM(a)(b) ->: eqM(b)(a)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.1)++(FiniteDistribution.unif(op:Term)*1)
val negative5_1 = negative5_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val negative6_ : FiniteDistribution[Term] = unif(a,b,c)()(
   eqM(op(op(a)(b))(c))(op(a)(op(b)(c))),
   eqM(a)(b) ->: eqM(b)(a)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative6_1 = negative6_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_13 = TermState(negative5_1,negative5_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))))
val ts_14 = TermState(negative5_1,negative5_1.map(_.typ),goals = FiniteDistribution.unif(a ~>:  b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))))
val ts_15 = TermState(negative5_1,negative5_1.map(_.typ))

negative5_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.1),
    Weighted(b, 0.1),
    Weighted(c, 0.1),
    Weighted(axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))}, 0.1),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.1),
    Weighted(eqM, 0.1),
    Weighted(op, 1.0)
  )
)
negative5_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
      0.07692307692307693
    ),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(op, 0.7692307692307692)
  )
)
negative6_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.1),
    Weighted(b, 0.1),
    Weighted(c, 0.1),
    Weighted(axiom_{eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))}, 0.1),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.1),
    Weighted(eqM, 0.7),
    Weighted(op, 0.9)
  )
)
negative6_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
      0.07692307692307693
    ),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(op, 0.7692307692307692)
  )
)
ts_13: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
        0.07692307692307693
      ),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(op, 0.7692307692307692)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(
        eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
        0.07692307692307693
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted((M → (M → M)), 0.7692307692307692)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)), 1.0))
  ),
  Empty
)
ts_14: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
        0.07692307692307693
      ),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(op, 0.7692307692307692)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(
        eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
        0.07692307692307693
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted((M → (M → M)), 0.7692307692307692)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
        1.0
      )
    )
  ),
  Empty
)
ts_15: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
        0.07692307692307693
      ),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(op, 0.7692307692307692)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(
        eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
        0.07692307692307693
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted((M → (M → M)), 0.7692307692307692)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

val tg8= TermGenParams(piW=0.3)
val tg9 = TermGenParams(unAppW=0.3,appW=0.2)
val lp_26 = LocalProver(ts_14,tg10,cutoff = 3*math.pow(10,-6))
val lp_27 = LocalProver(ts_13,cutoff = 5*math.pow(10,-6)).noIsles
val lp_28 = LocalProver(ts_15,tg9,cutoff = 2*math.pow(10,-6)).noIsles

tg8: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.1,
  0.1,
  0.3,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
tg9: TermGenParams = TermGenParams(
  0.2,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_26: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
          0.07692307692307693
        ),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(op, 0.7692307692307692)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
          0.07692307692307693
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted((M → (M → M)), 0.7692307692307692)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } },
          1.0
        )
      )
    ),
    Empty
...
lp_27: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
          0.07692307692307693
        ),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(op, 0.7692307692307692)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
          0.07692307692307693
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted((M → (M → M)), 0.7692307692307692)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)), 1.0)
      )
    ),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
...
lp_28: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))},
          0.07692307692307693
        ),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(op, 0.7692307692307692)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(
          eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
          0.07692307692307693
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted((M → (M → M)), 0.7692307692307692)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.2,
    0.3,
    0.1,
    0.0,
    0.0,
    0.05,
...

val lem_26 = lp_26.lemmas.runSyncUnsafe()

lem_26: Vector[(Typ[Term], Double)] = Vector(
  ((M → (M → M))×(M → (M → M)), 0.0038228191408910405),
  (((M → (M → M)) → (M → (M → M))×(M → (M → M))), 4.338708406827879E-4),
  (
    ((M → (M → M)) → ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }),
    1.0000839848925076E-5
  ),
  (
    ((M → (M → M)) → ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } }),
    1.0000839848925076E-5
  ),
  (((M → (M → M)) → (M → (M → 𝒰 ))), 1.0000839848925076E-5),
  (((M → (M → M))×(M → (M → M)) → (M → (M → M))), 9.8350338217578E-6),
  (((M → (M → 𝒰 )) → (M → (M → M))), 9.811279882485584E-6),
  (
    (∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → (M → (M → M))),
    9.811279882485584E-6
  ),
  (
    (∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } } → (M → (M → M))),
    9.811279882485584E-6
  ),
  (
    (((M → (M → M)) → (M → (M → M))) → ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }),
    9.809886052212806E-6
  ),
  (
    (((M → (M → M)) → (M → (M → M))) → ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) } } }),
    9.809886052212806E-6
  ),
  ((((M → (M → M)) → (M → (M → M))) → (M → (M → 𝒰 ))), 9.809886052212806E-6),
  (((M → (M → M)) → (M → (M → M))), 9.733083338990583E-6),
  (((M → (M → M)) → ((M → (M → M)) → (M → (M → M)))), 9.722946485130535E-6),
  ((((M → (M → M)) → (M → (M → 𝒰 ))) → (M → (M → M))), 9.648878913981793E-6),
  (
...

val goals = a ~>:  b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))

goals: GenFuncTyp[Term, FuncLike[Term, FuncLike[Term, Term]]] = ∏(a : M){ ∏(b : M){ ∏(c : M){ eqM(op(a)(op(b)(c)))(op(op(a)(b))(c)) } } }

val lem_27 = lp_27.lemmas.runSyncUnsafe()

lem_27: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)), 1.3749953944441501E-5)
)

val lem_28 = lp_28.lemmas.runSyncUnsafe()

lem_28: Vector[(Typ[Term], Double)] = Vector()

Step5:

$$(x*inv(x)(y))*e=(y*e)$$

val negative7_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
   eqM(op(x)(inv(x)(y)))(y),
   eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.3)++(FiniteDistribution.unif(op:Term)*0.4)
val negative7_1 = negative7_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_17 = TermState(negative7_1,negative7_1.map(_.typ))
val ts_16 = TermState(negative7_1,negative7_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))))

negative7_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(x, 0.0625),
    Weighted(e, 0.0625),
    Weighted(inv(x)(y), 0.0625),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.0625),
    Weighted(axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))}, 0.0625),
    Weighted(eqM, 0.3),
    Weighted(op, 0.4)
  )
)
negative7_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.061728395061728385),
    Weighted(e, 0.061728395061728385),
    Weighted(inv(x)(y), 0.061728395061728385),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.061728395061728385),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
      0.061728395061728385
    ),
    Weighted(eqM, 0.2962962962962962),
    Weighted(op, 0.3950617283950617)
  )
)
ts_17: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.061728395061728385),
      Weighted(e, 0.061728395061728385),
      Weighted(inv(x)(y), 0.061728395061728385),
      Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.061728395061728385),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
        0.061728395061728385
      ),
      Weighted(eqM, 0.2962962962962962),
      Weighted(op, 0.3950617283950617)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.061728395061728385),
      Weighted(M, 0.061728395061728385),
      Weighted(M, 0.061728395061728385),
      Weighted(eqM(op(x)(inv(x)(y)))(y), 0.061728395061728385),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
        0.061728395061728385
      ),
      Weighted((M → (M → 𝒰 )), 0.2962962962962962),
      Weighted((M → (M → M)), 0.3950617283950617)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_16: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.061728395061728385),
      Weighted(e, 0.061728395061728385),
      Weighted(inv(x)(y), 0.061728395061728385),
      Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.061728395061728385),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
        0.061728395061728385
      ),
      Weighted(eqM, 0.2962962962962962),
      Weighted(op, 0.3950617283950617)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.061728395061728385),
      Weighted(M, 0.061728395061728385),
      Weighted(M, 0.061728395061728385),
      Weighted(eqM(op(x)(inv(x)(y)))(y), 0.061728395061728385),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
        0.061728395061728385
      ),
      Weighted((M → (M → 𝒰 )), 0.2962962962962962),
      Weighted((M → (M → M)), 0.3950617283950617)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 1.0))
  ),
  Empty
)

val lp_28 = LocalProver(ts_16,cutoff=2*math.pow(10,-6)).noIsles

lp_28: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.061728395061728385),
        Weighted(e, 0.061728395061728385),
        Weighted(inv(x)(y), 0.061728395061728385),
        Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.061728395061728385),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
          0.061728395061728385
        ),
        Weighted(eqM, 0.2962962962962962),
        Weighted(op, 0.3950617283950617)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.061728395061728385),
        Weighted(M, 0.061728395061728385),
        Weighted(M, 0.061728395061728385),
        Weighted(eqM(op(x)(inv(x)(y)))(y), 0.061728395061728385),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
          0.061728395061728385
        ),
        Weighted((M → (M → 𝒰 )), 0.2962962962962962),
        Weighted((M → (M → M)), 0.3950617283950617)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 1.0))
    ),
    Empty
  ),
  TermGenParams(
...

val lem_28 = lp_28.lemmas.runSyncUnsafe()

lem_28: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 0.9024859640533102)
)

Step6:

$$(x*e)*inv(x)(y) = y*e$$

Basically we will prove $$\{(x*e)*inv(x)(y) = x*(e*inv(x)(y)) \ \ \land$$ $$x*(e*inv(x)(y)) = x*(inv(x)(y)*e) \ \ \land$$ $$x*(inv(x)(y)*e) = (x*inv(x)(y))*e \ \ \land$$ $$(x*inv(x)(y))*e = y*e \} \implies $$ $$(x*e)*inv(x)(y) = y*e$$

val negative8_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
   eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
   eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y)))),
   eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e))),
   eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)),
   eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))    
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative8_1 = negative8_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_18 = TermState(negative8_1,negative8_1.map(_.typ))
val ts_19 = TermState(negative8_1,negative8_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))))
val tg10 = TermGenParams(unAppW =0.2)

negative8_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(x, 0.045454545454545456),
    Weighted(e, 0.045454545454545456),
    Weighted(inv(x)(y), 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
      0.045454545454545456
    ),
    Weighted(eqM, 0.5),
    Weighted(op, 0.8)
  )
)
negative8_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.027322404371584695),
    Weighted(e, 0.027322404371584695),
    Weighted(inv(x)(y), 0.027322404371584695),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.027322404371584695
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))},
      0.027322404371584695
    ),
    Weighted(
      axiom_{eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))},
      0.027322404371584695
    ),
    Weighted(
      axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
      0.027322404371584695
    ),
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
      0.027322404371584695
    ),
    Weighted(eqM, 0.30054644808743164),
    Weighted(op, 0.48087431693989063)
  )
)
ts_18: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.027322404371584695),
      Weighted(e, 0.027322404371584695),
      Weighted(inv(x)(y), 0.027322404371584695),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.027322404371584695
      ),
      Weighted(eqM, 0.30054644808743164),
      Weighted(op, 0.48087431693989063)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.027322404371584695),
      Weighted(M, 0.027322404371584695),
      Weighted(M, 0.027322404371584695),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.027322404371584695
...
ts_19: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.027322404371584695),
      Weighted(e, 0.027322404371584695),
      Weighted(inv(x)(y), 0.027322404371584695),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
        0.027322404371584695
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.027322404371584695
      ),
      Weighted(eqM, 0.30054644808743164),
      Weighted(op, 0.48087431693989063)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.027322404371584695),
      Weighted(M, 0.027322404371584695),
      Weighted(M, 0.027322404371584695),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.027322404371584695
...
tg10: TermGenParams = TermGenParams(
  0.1,
  0.2,
  0.1,
  0.1,
  0.1,
  0.0,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)

val lp_29 = LocalProver(ts_19,tg10,cutoff=2*math.pow(10,-6)).noIsles

lp_29: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.027322404371584695),
        Weighted(e, 0.027322404371584695),
        Weighted(inv(x)(y), 0.027322404371584695),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.027322404371584695
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))},
          0.027322404371584695
        ),
        Weighted(
          axiom_{eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))},
          0.027322404371584695
        ),
        Weighted(
          axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
          0.027322404371584695
        ),
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
          0.027322404371584695
        ),
        Weighted(eqM, 0.30054644808743164),
        Weighted(op, 0.48087431693989063)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.027322404371584695),
        Weighted(M, 0.027322404371584695),
        Weighted(M, 0.027322404371584695),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
...

val lem_29 = lp_29.lemmas.runSyncUnsafe()

lem_29: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))), 0.9014148838516249)
)

val lem_30 = lp_29.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$4(MonixFiniteDistributionEq.scala:163)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:148)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:182)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:178)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:209)
  provingground.learning.LocalProver.nextState(LocalProver.scala:194)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:333)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:333)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:381)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:379)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd28$Helper.<init>(cmd28.sc:1)
  ammonite.$sess.cmd28$.<init>(cmd28.sc:7)
  ammonite.$sess.cmd28$.<clinit>(cmd28.sc:-1)

val negative9_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
   eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
   eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))),
   eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)),
   eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))    
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative9_1 = negative9_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_20 = TermState(negative9_1,negative9_1.map(_.typ))
val ts_21 = TermState(negative9_1,negative9_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))))
val negative10_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
   eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
   eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)),
   eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))    
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative10_1 = negative10_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_22 = TermState(negative10_1,negative10_1.map(_.typ))
val ts_23 = TermState(negative10_1,negative10_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))))

negative9_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05),
    Weighted(b, 0.05),
    Weighted(c, 0.05),
    Weighted(x, 0.05),
    Weighted(e, 0.05),
    Weighted(inv(x)(y), 0.05),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.05),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e)))},
      0.05
    ),
    Weighted(
      axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
      0.05
    ),
    Weighted(axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))}, 0.05),
    Weighted(eqM, 0.5),
    Weighted(op, 0.8)
  )
)
negative9_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.030303030303030304),
    Weighted(e, 0.030303030303030304),
    Weighted(inv(x)(y), 0.030303030303030304),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.030303030303030304
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e)))},
      0.030303030303030304
    ),
    Weighted(
      axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
      0.030303030303030304
    ),
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
      0.030303030303030304
    ),
    Weighted(eqM, 0.30303030303030304),
    Weighted(op, 0.48484848484848486)
  )
)
ts_20: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.030303030303030304),
      Weighted(e, 0.030303030303030304),
      Weighted(inv(x)(y), 0.030303030303030304),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e)))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.030303030303030304
      ),
      Weighted(eqM, 0.30303030303030304),
      Weighted(op, 0.48484848484848486)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.030303030303030304),
      Weighted(M, 0.030303030303030304),
      Weighted(M, 0.030303030303030304),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.030303030303030304
      ),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))),
        0.030303030303030304
...
ts_21: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.030303030303030304),
      Weighted(e, 0.030303030303030304),
      Weighted(inv(x)(y), 0.030303030303030304),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e)))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
        0.030303030303030304
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.030303030303030304
      ),
      Weighted(eqM, 0.30303030303030304),
      Weighted(op, 0.48484848484848486)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.030303030303030304),
      Weighted(M, 0.030303030303030304),
      Weighted(M, 0.030303030303030304),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.030303030303030304
      ),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))),
        0.030303030303030304
...
negative10_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(x, 0.05555555555555555),
    Weighted(e, 0.05555555555555555),
    Weighted(inv(x)(y), 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))},
      0.05555555555555555
    ),
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.5),
    Weighted(op, 0.8)
  )
)
negative10_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.03401360544217687),
    Weighted(e, 0.03401360544217687),
    Weighted(inv(x)(y), 0.03401360544217687),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.03401360544217687
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))},
      0.03401360544217687
    ),
    Weighted(
      axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
      0.03401360544217687
    ),
    Weighted(eqM, 0.30612244897959184),
    Weighted(op, 0.489795918367347)
  )
)
ts_22: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03401360544217687),
      Weighted(e, 0.03401360544217687),
      Weighted(inv(x)(y), 0.03401360544217687),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.03401360544217687
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))},
        0.03401360544217687
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.03401360544217687
      ),
      Weighted(eqM, 0.30612244897959184),
      Weighted(op, 0.489795918367347)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03401360544217687),
      Weighted(M, 0.03401360544217687),
      Weighted(M, 0.03401360544217687),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.03401360544217687
      ),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)),
        0.03401360544217687
      ),
      Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 0.03401360544217687),
      Weighted((M → (M → 𝒰 )), 0.30612244897959184),
      Weighted((M → (M → M)), 0.489795918367347)
...
ts_23: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.03401360544217687),
      Weighted(e, 0.03401360544217687),
      Weighted(inv(x)(y), 0.03401360544217687),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.03401360544217687
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))},
        0.03401360544217687
      ),
      Weighted(
        axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
        0.03401360544217687
      ),
      Weighted(eqM, 0.30612244897959184),
      Weighted(op, 0.489795918367347)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03401360544217687),
      Weighted(M, 0.03401360544217687),
      Weighted(M, 0.03401360544217687),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.03401360544217687
      ),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)),
        0.03401360544217687
      ),
      Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 0.03401360544217687),
      Weighted((M → (M → 𝒰 )), 0.30612244897959184),
      Weighted((M → (M → M)), 0.489795918367347)
...

val lp_30 = LocalProver(ts_21,cutoff=2*math.pow(10,-6)).noIsles
val lp_31 = LocalProver(ts_23,cutoff=2*math.pow(10,-6)).noIsles

lp_30: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.030303030303030304),
        Weighted(e, 0.030303030303030304),
        Weighted(inv(x)(y), 0.030303030303030304),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.030303030303030304
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e)))},
          0.030303030303030304
        ),
        Weighted(
          axiom_{eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))},
          0.030303030303030304
        ),
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
          0.030303030303030304
        ),
        Weighted(eqM, 0.30303030303030304),
        Weighted(op, 0.48484848484848486)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.030303030303030304),
        Weighted(M, 0.030303030303030304),
        Weighted(M, 0.030303030303030304),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.030303030303030304
        ),
        Weighted(
          eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))),
...
lp_31: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.03401360544217687),
        Weighted(e, 0.03401360544217687),
        Weighted(inv(x)(y), 0.03401360544217687),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.03401360544217687
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))},
          0.03401360544217687
        ),
        Weighted(
          axiom_{eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))},
          0.03401360544217687
        ),
        Weighted(eqM, 0.30612244897959184),
        Weighted(op, 0.489795918367347)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03401360544217687),
        Weighted(M, 0.03401360544217687),
        Weighted(M, 0.03401360544217687),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.03401360544217687
        ),
        Weighted(
          eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)),
          0.03401360544217687
        ),
        Weighted(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e)), 0.03401360544217687),
        Weighted((M → (M → 𝒰 )), 0.30612244897959184),
...

val lem_30 = lp_30.lemmas.runSyncUnsafe()
val lem_31 = lp_31.lemmas.runSyncUnsafe()

lem_30: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)), 0.9000270836056806)
)
lem_31: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.8983792913781188)
)

Step7:

$$(y*e) = y$$

Basically we wil prove $$[ \{ (x*e)*inv(x)(y) = (y*e) \} \land \{x*inv(x)(y) = y\} \land \{(x*e)*inv(x)(y)) = ((x*inv(x)(y))\} ] \implies (y*e=y)$$ $$\Updownarrow$$ $$\{(a=b) \land (c=d) \land (a=c)\} \implies (b=d)$$ where $$ a= (x*e)*inv(x)(y) \\ b= (y*e) \\ c= x*inv(x)(y) \\ d= y \\ $$

val negative11_ : FiniteDistribution[Term] = unif(a,b,c,d)(x,e,inv(x)(y),y)(
   eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
   eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
   eqM(op(x)(inv(x)(y)))(y),
   eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative11_1 = negative11_.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_24 = TermState(negative11_1,negative11_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))

val negative12_ : FiniteDistribution[Term] = unif(a,b,c,d)(op(op(x)(e))(inv(x)(y)),op(y)(e),op(x)(inv(x)(y)),y,eqM,op)(
   eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
   eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
   eqM(op(x)(inv(x)(y)))(y),
   eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative12_1 = negative12_.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_25 = TermState(negative12_1,negative12_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))

val negative13 : FiniteDistribution[Term] = unif(a,b,c,d)(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),eqM(op(x)(inv(x)(y)))(y),eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))))(
   eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
   eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
   eqM(op(x)(inv(x)(y)))(y),
   eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative13_1 = negative13.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_26 = TermState(negative13_1,negative13_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))

negative11_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.041666666666666664),
    Weighted(b, 0.041666666666666664),
    Weighted(c, 0.041666666666666664),
    Weighted(d, 0.041666666666666664),
    Weighted(x, 0.041666666666666664),
    Weighted(e, 0.041666666666666664),
    Weighted(inv(x)(y), 0.041666666666666664),
    Weighted(y, 0.041666666666666664),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.041666666666666664
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.041666666666666664
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.041666666666666664),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.041666666666666664
    ),
    Weighted(eqM, 0.5),
    Weighted(op, 0.8)
  )
)
negative11_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(x, 0.025510204081632654),
    Weighted(e, 0.025510204081632654),
    Weighted(inv(x)(y), 0.025510204081632654),
    Weighted(y, 0.025510204081632654),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.025510204081632654
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.025510204081632654
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.025510204081632654),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.025510204081632654
    ),
    Weighted(eqM, 0.30612244897959184),
    Weighted(op, 0.489795918367347)
  )
)
ts_24: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(x, 0.025510204081632654),
      Weighted(e, 0.025510204081632654),
      Weighted(inv(x)(y), 0.025510204081632654),
      Weighted(y, 0.025510204081632654),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
        0.025510204081632654
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
        0.025510204081632654
      ),
      Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.025510204081632654),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
        0.025510204081632654
      ),
      Weighted(eqM, 0.30612244897959184),
      Weighted(op, 0.489795918367347)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.025510204081632654),
      Weighted(M, 0.025510204081632654),
      Weighted(M, 0.025510204081632654),
      Weighted(M, 0.025510204081632654),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
        0.025510204081632654
      ),
      Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.025510204081632654),
      Weighted(eqM(op(x)(inv(x)(y)))(y), 0.025510204081632654),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
...
negative12_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.03571428571428571),
    Weighted(b, 0.03571428571428571),
    Weighted(c, 0.03571428571428571),
    Weighted(d, 0.03571428571428571),
    Weighted(op(op(x)(e))(inv(x)(y)), 0.03571428571428571),
    Weighted(op(y)(e), 0.03571428571428571),
    Weighted(op(x)(inv(x)(y)), 0.03571428571428571),
    Weighted(y, 0.03571428571428571),
    Weighted(eqM, 0.03571428571428571),
    Weighted(op, 0.03571428571428571),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.03571428571428571
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.03571428571428571
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.03571428571428571),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.03571428571428571
    ),
    Weighted(eqM, 0.9)
  )
)
negative12_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op(op(x)(e))(inv(x)(y)), 0.02840909090909091),
    Weighted(op(y)(e), 0.02840909090909091),
    Weighted(op(x)(inv(x)(y)), 0.02840909090909091),
    Weighted(y, 0.02840909090909091),
    Weighted(eqM, 0.02840909090909091),
    Weighted(op, 0.02840909090909091),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.02840909090909091
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.02840909090909091
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.02840909090909091),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.02840909090909091
    ),
    Weighted(eqM, 0.7159090909090909)
  )
)
ts_25: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(op(x)(e))(inv(x)(y)), 0.02840909090909091),
      Weighted(op(y)(e), 0.02840909090909091),
      Weighted(op(x)(inv(x)(y)), 0.02840909090909091),
      Weighted(y, 0.02840909090909091),
      Weighted(eqM, 0.02840909090909091),
      Weighted(op, 0.02840909090909091),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
        0.02840909090909091
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
        0.02840909090909091
      ),
      Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.02840909090909091),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
        0.02840909090909091
      ),
      Weighted(eqM, 0.7159090909090909)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.02840909090909091),
      Weighted(M, 0.02840909090909091),
      Weighted(M, 0.02840909090909091),
      Weighted(M, 0.02840909090909091),
      Weighted((M → (M → 𝒰 )), 0.02840909090909091),
      Weighted((M → (M → M)), 0.02840909090909091),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
        0.02840909090909091
      ),
      Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.02840909090909091),
...
negative13: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(d, 0.045454545454545456),
    Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.045454545454545456),
    Weighted(eqM(op(x)(inv(x)(y)))(y), 0.045454545454545456),
    Weighted(
      eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
      0.045454545454545456
    ),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.045454545454545456
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.045454545454545456),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.045454545454545456
    ),
    Weighted(eqM, 0.9)
  )
)
negative13_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.03731343283582089),
    Weighted(eqM(op(x)(inv(x)(y)))(y), 0.03731343283582089),
    Weighted(
      eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
      0.03731343283582089
    ),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
      0.03731343283582089
    ),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
      0.03731343283582089
    ),
    Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.03731343283582089),
    Weighted(
      axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
      0.03731343283582089
    ),
    Weighted(eqM, 0.7388059701492536)
  )
)
ts_26: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.03731343283582089),
      Weighted(eqM(op(x)(inv(x)(y)))(y), 0.03731343283582089),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
        0.03731343283582089
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
        0.03731343283582089
      ),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
        0.03731343283582089
      ),
      Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.03731343283582089),
      Weighted(
        axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
        0.03731343283582089
      ),
      Weighted(eqM, 0.7388059701492536)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.03731343283582089),
      Weighted(𝒰 , 0.03731343283582089),
      Weighted(𝒰 , 0.03731343283582089),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
        0.03731343283582089
      ),
      Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.03731343283582089),
      Weighted(eqM(op(x)(inv(x)(y)))(y), 0.03731343283582089),
      Weighted(
        eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
...

val tg11 = TermGenParams(unAppW=0.25)
val lp_32 = LocalProver(ts_24,cutoff=9*math.pow(10,-6)).noIsles
val lp_33 = LocalProver(ts_25,tg11,cutoff=9*math.pow(10,-6)).noIsles
val lp_34 = LocalProver(ts_26,cutoff=5*math.pow(10,-6)).noIsles

tg11: TermGenParams = TermGenParams(
  0.1,
  0.25,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_32: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(x, 0.025510204081632654),
        Weighted(e, 0.025510204081632654),
        Weighted(inv(x)(y), 0.025510204081632654),
        Weighted(y, 0.025510204081632654),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
          0.025510204081632654
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
          0.025510204081632654
        ),
        Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.025510204081632654),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
          0.025510204081632654
        ),
        Weighted(eqM, 0.30612244897959184),
        Weighted(op, 0.489795918367347)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.025510204081632654),
        Weighted(M, 0.025510204081632654),
        Weighted(M, 0.025510204081632654),
        Weighted(M, 0.025510204081632654),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
          0.025510204081632654
        ),
        Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.025510204081632654),
        Weighted(eqM(op(x)(inv(x)(y)))(y), 0.025510204081632654),
        Weighted(
...
lp_33: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(op(x)(e))(inv(x)(y)), 0.02840909090909091),
        Weighted(op(y)(e), 0.02840909090909091),
        Weighted(op(x)(inv(x)(y)), 0.02840909090909091),
        Weighted(y, 0.02840909090909091),
        Weighted(eqM, 0.02840909090909091),
        Weighted(op, 0.02840909090909091),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
          0.02840909090909091
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
          0.02840909090909091
        ),
        Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.02840909090909091),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
          0.02840909090909091
        ),
        Weighted(eqM, 0.7159090909090909)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.02840909090909091),
        Weighted(M, 0.02840909090909091),
        Weighted(M, 0.02840909090909091),
        Weighted(M, 0.02840909090909091),
        Weighted((M → (M → 𝒰 )), 0.02840909090909091),
        Weighted((M → (M → M)), 0.02840909090909091),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
          0.02840909090909091
        ),
...
lp_34: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.03731343283582089),
        Weighted(eqM(op(x)(inv(x)(y)))(y), 0.03731343283582089),
        Weighted(
          eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))),
          0.03731343283582089
        ),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(c)(d) \to (eqM(a)(c) \to eqM(b)(d))))},
          0.03731343283582089
        ),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))},
          0.03731343283582089
        ),
        Weighted(axiom_{eqM(op(x)(inv(x)(y)))(y)}, 0.03731343283582089),
        Weighted(
          axiom_{eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))},
          0.03731343283582089
        ),
        Weighted(eqM, 0.7388059701492536)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.03731343283582089),
        Weighted(𝒰 , 0.03731343283582089),
        Weighted(𝒰 , 0.03731343283582089),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(c)(d) → (eqM(a)(c) → eqM(b)(d)))) } } } },
          0.03731343283582089
        ),
        Weighted(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)), 0.03731343283582089),
        Weighted(eqM(op(x)(inv(x)(y)))(y), 0.03731343283582089),
        Weighted(
...

val lem_32 = lp_32.lemmas.runSyncUnsafe()

lem_32: Vector[(Typ[Term], Double)] = Vector()

val lem_33 = lp_33.lemmas.runSyncUnsafe()

java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  monix.eval.Task.timeout(Task.scala:2220)
  provingground.learning.GenMonixFiniteDistributionEq.$anonfun$varDist$2(MonixFiniteDistributionEq.scala:159)
  scala.Option.getOrElse(Option.scala:189)
  provingground.learning.GenMonixFiniteDistributionEq.varDist(MonixFiniteDistributionEq.scala:144)
  provingground.learning.LocalProver.tripleT$lzycompute(LocalProver.scala:178)
  provingground.learning.LocalProver.tripleT(LocalProver.scala:174)
  provingground.learning.LocalProver.nextState$lzycompute(LocalProver.scala:205)
  provingground.learning.LocalProver.nextState(LocalProver.scala:190)
  provingground.learning.LocalProverStep.evolvedState(LocalProver.scala:316)
  provingground.learning.LocalProverStep.evolvedState$(LocalProver.scala:316)
  provingground.learning.LocalProver.evolvedState$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.evolvedState(LocalProver.scala:25)
  provingground.learning.LocalProverStep.lemmas(LocalProver.scala:364)
  provingground.learning.LocalProverStep.lemmas$(LocalProver.scala:362)
  provingground.learning.LocalProver.lemmas$lzycompute(LocalProver.scala:25)
  provingground.learning.LocalProver.lemmas(LocalProver.scala:25)
  ammonite.$sess.cmd8$Helper.<init>(cmd8.sc:1)
  ammonite.$sess.cmd8$.<init>(cmd8.sc:7)
  ammonite.$sess.cmd8$.<clinit>(cmd8.sc:-1)

val lem_34 = lp_34.lemmas.runSyncUnsafe()

lem_34: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(y)(e))(y), 0.8510794075570274)
)

We have proved that all identity elements are universal identities.Now we have to prove that the cardinality of set of all the universal identity is 1.This proof goes similar to Monoid proof.The link to the Monoid proof notebook is https://github.com/siddhartha-gadgil/ProvingGround/blob/master/notes/2019-09-18-monoid.ipynb .

Section2 : Uniqueness Of Universal Identity

Assume $e_1$ and $e_2$ be two universal identies.

Step1:

$$(e_1*e_2=e_1) \land (e_2*e_1=e_2)$$

val negative14_ : FiniteDistribution[Term] = unif(a)(e1,e2)(
    eqM(op(a)(e1))(a),
    eqM(op(e2)(a))(a),
    eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.4)
val negative14_1 = negative14_.filter((t) => !Set(a).contains(t)).normalized()
val ts_27 = TermState(negative14_1,negative14_1.map(_.typ),goals = FiniteDistribution.unif(eqM(e1)(e2)))

negative14_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.08333333333333333),
    Weighted(e1, 0.08333333333333333),
    Weighted(e2, 0.08333333333333333),
    Weighted(axiom_{eqM(op(a)(e1))(a)}, 0.08333333333333333),
    Weighted(axiom_{eqM(op(e2)(a))(a)}, 0.08333333333333333),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
      0.08333333333333333
    ),
    Weighted(eqM, 0.5),
    Weighted(op, 0.4)
  )
)
negative14_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(e1, 0.06329113924050633),
    Weighted(e2, 0.06329113924050633),
    Weighted(axiom_{eqM(op(a)(e1))(a)}, 0.06329113924050633),
    Weighted(axiom_{eqM(op(e2)(a))(a)}, 0.06329113924050633),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
      0.06329113924050633
    ),
    Weighted(eqM, 0.379746835443038),
    Weighted(op, 0.30379746835443044)
  )
)
ts_27: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e1, 0.06329113924050633),
      Weighted(e2, 0.06329113924050633),
      Weighted(axiom_{eqM(op(a)(e1))(a)}, 0.06329113924050633),
      Weighted(axiom_{eqM(op(e2)(a))(a)}, 0.06329113924050633),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
        0.06329113924050633
      ),
      Weighted(eqM, 0.379746835443038),
      Weighted(op, 0.30379746835443044)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06329113924050633),
      Weighted(M, 0.06329113924050633),
      Weighted(∏(a : M){ eqM(op(a)(e1))(a) }, 0.06329113924050633),
      Weighted(∏(a : M){ eqM(op(e2)(a))(a) }, 0.06329113924050633),
      Weighted(
        ∏(a : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) },
        0.06329113924050633
      ),
      Weighted((M → (M → 𝒰 )), 0.379746835443038),
      Weighted((M → (M → M)), 0.30379746835443044)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(e1)(e2), 1.0))),
  Empty
)

val lp_35 = LocalProver(ts_27,cutoff = 5*math.pow(10,-6)).noIsles

lp_35: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e1, 0.06329113924050633),
        Weighted(e2, 0.06329113924050633),
        Weighted(axiom_{eqM(op(a)(e1))(a)}, 0.06329113924050633),
        Weighted(axiom_{eqM(op(e2)(a))(a)}, 0.06329113924050633),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
          0.06329113924050633
        ),
        Weighted(eqM, 0.379746835443038),
        Weighted(op, 0.30379746835443044)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06329113924050633),
        Weighted(M, 0.06329113924050633),
        Weighted(∏(a : M){ eqM(op(a)(e1))(a) }, 0.06329113924050633),
        Weighted(∏(a : M){ eqM(op(e2)(a))(a) }, 0.06329113924050633),
        Weighted(
          ∏(a : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) },
          0.06329113924050633
        ),
        Weighted((M → (M → 𝒰 )), 0.379746835443038),
        Weighted((M → (M → M)), 0.30379746835443044)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(eqM(e1)(e2), 1.0))),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
...

val lem_35 = lp_35.lemmas.runSyncUnsafe()

lem_35: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(e2)(e2))(e2), 1.1741048016619992E-5),
  (eqM(op(e2)(e1))(e2), 1.1741048016619992E-5),
  (eqM(op(e1)(e1))(e1), 1.1741048016619992E-5),
  (eqM(op(e2)(e1))(e1), 1.1741048016619992E-5)
)

Step2:

$$e_1=e_2$$

val negative15_ : FiniteDistribution[Term] = unif(a,b,c)(e1,e2,op)(
    eqM(op(e2)(e1))(e1),
    eqM(op(e2)(e1))(e2),
    eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.4)
val negative15_1 = negative15_.filter((t) => !Set(a,b,c).contains(t)).normalized()
val ts_28 = TermState(negative15_1,negative15_1.map(_.typ))
val ts_29 = TermState(negative15_1,negative15_1.map(_.typ),goals = FiniteDistribution.unif(eqM(e1)(e2)))

negative15_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(e1, 0.05555555555555555),
    Weighted(e2, 0.05555555555555555),
    Weighted(op, 0.05555555555555555),
    Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.05555555555555555),
    Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.5),
    Weighted(op, 0.4)
  )
)
negative15_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(e1, 0.045045045045045036),
    Weighted(e2, 0.045045045045045036),
    Weighted(op, 0.045045045045045036),
    Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.045045045045045036),
    Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.045045045045045036),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
      0.045045045045045036
    ),
    Weighted(eqM, 0.4054054054054054),
    Weighted(op, 0.32432432432432434)
  )
)
ts_28: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e1, 0.045045045045045036),
      Weighted(e2, 0.045045045045045036),
      Weighted(op, 0.045045045045045036),
      Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.045045045045045036),
      Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.045045045045045036),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
        0.045045045045045036
      ),
      Weighted(eqM, 0.4054054054054054),
      Weighted(op, 0.32432432432432434)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted((M → (M → M)), 0.045045045045045036),
      Weighted(eqM(op(e2)(e1))(e1), 0.045045045045045036),
      Weighted(eqM(op(e2)(e1))(e2), 0.045045045045045036),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
        0.045045045045045036
      ),
      Weighted((M → (M → 𝒰 )), 0.4054054054054054),
      Weighted((M → (M → M)), 0.32432432432432434)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_29: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e1, 0.045045045045045036),
      Weighted(e2, 0.045045045045045036),
      Weighted(op, 0.045045045045045036),
      Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.045045045045045036),
      Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.045045045045045036),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
        0.045045045045045036
      ),
      Weighted(eqM, 0.4054054054054054),
      Weighted(op, 0.32432432432432434)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted((M → (M → M)), 0.045045045045045036),
      Weighted(eqM(op(e2)(e1))(e1), 0.045045045045045036),
      Weighted(eqM(op(e2)(e1))(e2), 0.045045045045045036),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
        0.045045045045045036
      ),
      Weighted((M → (M → 𝒰 )), 0.4054054054054054),
      Weighted((M → (M → M)), 0.32432432432432434)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(e1)(e2), 1.0))),
  Empty
)

val lp_36 = LocalProver(ts_28,cutoff = 5*math.pow(10,-6)).noIsles
val lp_37 = LocalProver(ts_29,cutoff = 5*math.pow(10,-6)).noIsles

lp_36: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e1, 0.045045045045045036),
        Weighted(e2, 0.045045045045045036),
        Weighted(op, 0.045045045045045036),
        Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.045045045045045036),
        Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.045045045045045036),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
          0.045045045045045036
        ),
        Weighted(eqM, 0.4054054054054054),
        Weighted(op, 0.32432432432432434)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.045045045045045036),
        Weighted(M, 0.045045045045045036),
        Weighted((M → (M → M)), 0.045045045045045036),
        Weighted(eqM(op(e2)(e1))(e1), 0.045045045045045036),
        Weighted(eqM(op(e2)(e1))(e2), 0.045045045045045036),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
          0.045045045045045036
        ),
        Weighted((M → (M → 𝒰 )), 0.4054054054054054),
        Weighted((M → (M → M)), 0.32432432432432434)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
...
lp_37: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e1, 0.045045045045045036),
        Weighted(e2, 0.045045045045045036),
        Weighted(op, 0.045045045045045036),
        Weighted(axiom_{eqM(op(e2)(e1))(e1)}, 0.045045045045045036),
        Weighted(axiom_{eqM(op(e2)(e1))(e2)}, 0.045045045045045036),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
          0.045045045045045036
        ),
        Weighted(eqM, 0.4054054054054054),
        Weighted(op, 0.32432432432432434)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.045045045045045036),
        Weighted(M, 0.045045045045045036),
        Weighted((M → (M → M)), 0.045045045045045036),
        Weighted(eqM(op(e2)(e1))(e1), 0.045045045045045036),
        Weighted(eqM(op(e2)(e1))(e2), 0.045045045045045036),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
          0.045045045045045036
        ),
        Weighted((M → (M → 𝒰 )), 0.4054054054054054),
        Weighted((M → (M → M)), 0.32432432432432434)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(eqM(e1)(e2), 1.0))),
    Empty
  ),
  TermGenParams(
...

val lem_36 = lp_36.lemmas.runSyncUnsafe()

lem_36: Vector[(Typ[Term], Double)] = Vector(
  (eqM(e1)(e2), 0.004797460521354881),
  (eqM(e1)(e1), 0.004797460521354881),
  (eqM(e2)(e2), 0.004797460521354881),
  (eqM(e2)(e1), 0.004797460521354881)
)

val lem_37 = lp_37.lemmas.runSyncUnsafe()

lem_37: Vector[(Typ[Term], Double)] = Vector(
  (eqM(e1)(e2), 0.8930287033141091),
  (eqM(e1)(e1), 0.0016057097659929907),
  (eqM(e2)(e2), 0.0016057097659929907),
  (eqM(e2)(e1), 0.0016057097659929907)
)

Now we have successfully completed the prove for Part1.

Part2 : Elimination

Now we given for some $p,q,r \in S$, we are given $$p*r=q*r$$ holds. and now we have to prove $$p=q$$

Step1:

$$(p*r)*inv(r)(e) = (b*r)*inv(r)(e)$$ where e is the identity element for $r$.

val negative16_ : FiniteDistribution[Term] = unif(a,b,c)(op(p)(r),op(q)(r),inv(r)(e),op,eqM)(
    eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c)),
    eqM(op(p)(r))(op(q)(r))
  ) * 0.5++(FiniteDistribution.unif(eqM: Term)*0.5)++(FiniteDistribution.unif(op: Term)*0.25) 
val negative16_1 = negative16_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_30 = TermState(negative16_1,negative16_1.map(_.typ))

negative16_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05),
    Weighted(b, 0.05),
    Weighted(c, 0.05),
    Weighted(op(p)(r), 0.05),
    Weighted(op(q)(r), 0.05),
    Weighted(inv(r)(e), 0.05),
    Weighted(op, 0.05),
    Weighted(eqM, 0.05),
    Weighted(axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))}, 0.05),
    Weighted(axiom_{eqM(op(p)(r))(op(q)(r))}, 0.05),
    Weighted(eqM, 0.5),
    Weighted(op, 0.25)
  )
)
negative16_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op(p)(r), 0.045454545454545456),
    Weighted(op(q)(r), 0.045454545454545456),
    Weighted(inv(r)(e), 0.045454545454545456),
    Weighted(op, 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
      0.045454545454545456
    ),
    Weighted(axiom_{eqM(op(p)(r))(op(q)(r))}, 0.045454545454545456),
    Weighted(eqM, 0.45454545454545453),
    Weighted(op, 0.22727272727272727)
  )
)
ts_30: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(p)(r), 0.045454545454545456),
      Weighted(op(q)(r), 0.045454545454545456),
      Weighted(inv(r)(e), 0.045454545454545456),
      Weighted(op, 0.045454545454545456),
      Weighted(eqM, 0.045454545454545456),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
        0.045454545454545456
      ),
      Weighted(axiom_{eqM(op(p)(r))(op(q)(r))}, 0.045454545454545456),
      Weighted(eqM, 0.45454545454545453),
      Weighted(op, 0.22727272727272727)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.045454545454545456),
      Weighted(M, 0.045454545454545456),
      Weighted(M, 0.045454545454545456),
      Weighted((M → (M → M)), 0.045454545454545456),
      Weighted((M → (M → 𝒰 )), 0.045454545454545456),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
        0.045454545454545456
      ),
      Weighted(eqM(op(p)(r))(op(q)(r)), 0.045454545454545456),
      Weighted((M → (M → 𝒰 )), 0.45454545454545453),
      Weighted((M → (M → M)), 0.22727272727272727)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

val lp_38 = LocalProver(ts_30,cutoff = 5*math.pow(10,-6)).noIsles

lp_38: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(p)(r), 0.045454545454545456),
        Weighted(op(q)(r), 0.045454545454545456),
        Weighted(inv(r)(e), 0.045454545454545456),
        Weighted(op, 0.045454545454545456),
        Weighted(eqM, 0.045454545454545456),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(a)(c))(op(b)(c)))},
          0.045454545454545456
        ),
        Weighted(axiom_{eqM(op(p)(r))(op(q)(r))}, 0.045454545454545456),
        Weighted(eqM, 0.45454545454545453),
        Weighted(op, 0.22727272727272727)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.045454545454545456),
        Weighted(M, 0.045454545454545456),
        Weighted(M, 0.045454545454545456),
        Weighted((M → (M → M)), 0.045454545454545456),
        Weighted((M → (M → 𝒰 )), 0.045454545454545456),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(a)(c))(op(b)(c))) } } },
          0.045454545454545456
        ),
        Weighted(eqM(op(p)(r))(op(q)(r)), 0.045454545454545456),
        Weighted((M → (M → 𝒰 )), 0.45454545454545453),
        Weighted((M → (M → M)), 0.22727272727272727)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
...

val lem_38 = lp_38.lemmas.runSyncUnsafe()

lem_38: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(p)(r))(op(p)(r)))(op(op(q)(r))(op(p)(r))), 1.011659447219413E-5),
  (eqM(op(op(p)(r))(inv(r)(e)))(op(op(q)(r))(inv(r)(e))), 1.011659447219413E-5),
  (eqM(op(op(p)(r))(op(q)(r)))(op(op(q)(r))(op(q)(r))), 1.011659447219413E-5)
)

Step2:

$$(p*r)*inv(r)(e) = p*r*inv(r)(e)$$ and $$p*(r*inv(r)(e)) = p*r*inv(r)(e)$$ where e is the identity element for $r$.

In the above equation we haven't applied the bracketting on the first term, this is done to encompass the associative property of the operation *.

val negative17_ : FiniteDistribution[Term] = unif(a,b,c)(op(op(p)(r))(inv(r)(e)),op(p)(op(r)(inv(r)(e))),op_2(p)(r)(inv(r)(e)),eqM)(
eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) ->: eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)),
eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))
 )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative17_1 = negative17_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_31 = TermState(negative17_1,negative17_1.map(_.typ))
val ts_32= TermState(negative17_1,negative17_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))))

negative17_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(op(op(p)(r))(inv(r)(e)), 0.05555555555555555),
    Weighted(op(p)(op(r)(inv(r)(e))), 0.05555555555555555),
    Weighted(op_2(p)(r)(inv(r)(e)), 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) \to eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)))},
      0.05555555555555555
    ),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.9)
  )
)
negative17_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op(op(p)(r))(inv(r)(e)), 0.045045045045045036),
    Weighted(op(p)(op(r)(inv(r)(e))), 0.045045045045045036),
    Weighted(op_2(p)(r)(inv(r)(e)), 0.045045045045045036),
    Weighted(eqM, 0.045045045045045036),
    Weighted(
      axiom_{(eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) \to eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)))},
      0.045045045045045036
    ),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
      0.045045045045045036
    ),
    Weighted(eqM, 0.7297297297297297)
  )
)
ts_31: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(op(p)(r))(inv(r)(e)), 0.045045045045045036),
      Weighted(op(p)(op(r)(inv(r)(e))), 0.045045045045045036),
      Weighted(op_2(p)(r)(inv(r)(e)), 0.045045045045045036),
      Weighted(eqM, 0.045045045045045036),
      Weighted(
        axiom_{(eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) \to eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)))},
        0.045045045045045036
      ),
      Weighted(
        axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
        0.045045045045045036
      ),
      Weighted(eqM, 0.7297297297297297)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted((M → (M → 𝒰 )), 0.045045045045045036),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) → eqM(op(a)(op(b)(c)))(op_2(a)(b)(c))) } } },
        0.045045045045045036
      ),
      Weighted(
        eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
        0.045045045045045036
      ),
      Weighted((M → (M → 𝒰 )), 0.7297297297297297)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...
ts_32: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(op(p)(r))(inv(r)(e)), 0.045045045045045036),
      Weighted(op(p)(op(r)(inv(r)(e))), 0.045045045045045036),
      Weighted(op_2(p)(r)(inv(r)(e)), 0.045045045045045036),
      Weighted(eqM, 0.045045045045045036),
      Weighted(
        axiom_{(eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) \to eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)))},
        0.045045045045045036
      ),
      Weighted(
        axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
        0.045045045045045036
      ),
      Weighted(eqM, 0.7297297297297297)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted(M, 0.045045045045045036),
      Weighted((M → (M → 𝒰 )), 0.045045045045045036),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) → eqM(op(a)(op(b)(c)))(op_2(a)(b)(c))) } } },
        0.045045045045045036
      ),
      Weighted(
        eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
        0.045045045045045036
      ),
      Weighted((M → (M → 𝒰 )), 0.7297297297297297)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...

val lp_39 = LocalProver(ts_32,cutoff = 5*math.pow(10,-6)).noIsles

lp_39: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(op(p)(r))(inv(r)(e)), 0.045045045045045036),
        Weighted(op(p)(op(r)(inv(r)(e))), 0.045045045045045036),
        Weighted(op_2(p)(r)(inv(r)(e)), 0.045045045045045036),
        Weighted(eqM, 0.045045045045045036),
        Weighted(
          axiom_{(eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) \to eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)))},
          0.045045045045045036
        ),
        Weighted(
          axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
          0.045045045045045036
        ),
        Weighted(eqM, 0.7297297297297297)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.045045045045045036),
        Weighted(M, 0.045045045045045036),
        Weighted(M, 0.045045045045045036),
        Weighted((M → (M → 𝒰 )), 0.045045045045045036),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) → eqM(op(a)(op(b)(c)))(op_2(a)(b)(c))) } } },
          0.045045045045045036
        ),
        Weighted(
          eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
          0.045045045045045036
        ),
        Weighted((M → (M → 𝒰 )), 0.7297297297297297)
      )
    ),
    Vector(),
...

val lem_39= lp_39.lemmas.runSyncUnsafe()

lem_39: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))), 0.00285420901552047)
)

val negative18_ : FiniteDistribution[Term] = unif(a,b,c)(op(op(p)(r))(inv(r)(e)),op(p)(op(r)(inv(r)(e))),op_2(p)(r)(inv(r)(e)),eqM)(
eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e))),
eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
 )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative18_1 = negative18_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_33 = TermState(negative18_1,negative18_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(q)(inv(r)(e)))))

negative18_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05),
    Weighted(b, 0.05),
    Weighted(c, 0.05),
    Weighted(op(op(p)(r))(inv(r)(e)), 0.05),
    Weighted(op(p)(op(r)(inv(r)(e))), 0.05),
    Weighted(op_2(p)(r)(inv(r)(e)), 0.05),
    Weighted(eqM, 0.05),
    Weighted(axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))}, 0.05),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
      0.05
    ),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.05),
    Weighted(eqM, 0.9)
  )
)
negative18_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op(op(p)(r))(inv(r)(e)), 0.04000000000000001),
    Weighted(op(p)(op(r)(inv(r)(e))), 0.04000000000000001),
    Weighted(op_2(p)(r)(inv(r)(e)), 0.04000000000000001),
    Weighted(eqM, 0.04000000000000001),
    Weighted(
      axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))},
      0.04000000000000001
    ),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
      0.04000000000000001
    ),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.04000000000000001
    ),
    Weighted(eqM, 0.7200000000000001)
  )
)
ts_33: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op(op(p)(r))(inv(r)(e)), 0.04000000000000001),
      Weighted(op(p)(op(r)(inv(r)(e))), 0.04000000000000001),
      Weighted(op_2(p)(r)(inv(r)(e)), 0.04000000000000001),
      Weighted(eqM, 0.04000000000000001),
      Weighted(
        axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))},
        0.04000000000000001
      ),
      Weighted(
        axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
        0.04000000000000001
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.04000000000000001
      ),
      Weighted(eqM, 0.7200000000000001)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.04000000000000001),
      Weighted(M, 0.04000000000000001),
      Weighted(M, 0.04000000000000001),
      Weighted((M → (M → 𝒰 )), 0.04000000000000001),
      Weighted(
        eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e))),
        0.04000000000000001
      ),
      Weighted(
        eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
        0.04000000000000001
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
...

val lp_40 = LocalProver(ts_33,cutoff = 5*math.pow(10,-6)).noIsles

lp_40: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op(op(p)(r))(inv(r)(e)), 0.04000000000000001),
        Weighted(op(p)(op(r)(inv(r)(e))), 0.04000000000000001),
        Weighted(op_2(p)(r)(inv(r)(e)), 0.04000000000000001),
        Weighted(eqM, 0.04000000000000001),
        Weighted(
          axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))},
          0.04000000000000001
        ),
        Weighted(
          axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))},
          0.04000000000000001
        ),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.04000000000000001
        ),
        Weighted(eqM, 0.7200000000000001)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.04000000000000001),
        Weighted(M, 0.04000000000000001),
        Weighted(M, 0.04000000000000001),
        Weighted((M → (M → 𝒰 )), 0.04000000000000001),
        Weighted(
          eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e))),
          0.04000000000000001
        ),
        Weighted(
          eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
          0.04000000000000001
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } ...

val lem_40 = lp_40.lemmas.runSyncUnsafe()

lem_40: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(q)(inv(r)(e))), 0.8784421315181933)
)

Step3:

$$p*(r*inv(r)(e)) = p*e $$ $$\implies p*r*inv(r)(e) = p*e$$

val negative19_ : FiniteDistribution[Term] = unif(a,b,c)(p,r,e,inv,op,eqM)(
  eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
    eqM(op(a)(inv(a)(e)))(e)
 )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative19_1 = negative19_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_31 = TermState(negative19_1,negative19_1.map(_.typ))
val ts_32= TermState(negative19_1,negative19_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))))

negative19_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(p, 0.045454545454545456),
    Weighted(r, 0.045454545454545456),
    Weighted(e, 0.045454545454545456),
    Weighted(inv, 0.045454545454545456),
    Weighted(op, 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
      0.045454545454545456
    ),
    Weighted(axiom_{eqM(op(a)(inv(a)(e)))(e)}, 0.045454545454545456),
    Weighted(eqM, 0.9)
  )
)
negative19_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(p, 0.03597122302158273),
    Weighted(r, 0.03597122302158273),
    Weighted(e, 0.03597122302158273),
    Weighted(inv, 0.03597122302158273),
    Weighted(op, 0.03597122302158273),
    Weighted(eqM, 0.03597122302158273),
    Weighted(
      axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
      0.03597122302158273
    ),
    Weighted(axiom_{eqM(op(a)(inv(a)(e)))(e)}, 0.03597122302158273),
    Weighted(eqM, 0.7122302158273381)
  )
)
ts_31: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(p, 0.03597122302158273),
      Weighted(r, 0.03597122302158273),
      Weighted(e, 0.03597122302158273),
      Weighted(inv, 0.03597122302158273),
      Weighted(op, 0.03597122302158273),
      Weighted(eqM, 0.03597122302158273),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.03597122302158273
      ),
      Weighted(axiom_{eqM(op(a)(inv(a)(e)))(e)}, 0.03597122302158273),
      Weighted(eqM, 0.7122302158273381)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03597122302158273),
      Weighted(M, 0.03597122302158273),
      Weighted(M, 0.03597122302158273),
      Weighted((M → (M → M)), 0.03597122302158273),
      Weighted((M → (M → M)), 0.03597122302158273),
      Weighted((M → (M → 𝒰 )), 0.03597122302158273),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.03597122302158273
      ),
      Weighted(∏(a : M){ eqM(op(a)(inv(a)(e)))(e) }, 0.03597122302158273),
      Weighted((M → (M → 𝒰 )), 0.7122302158273381)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts_32: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(p, 0.03597122302158273),
      Weighted(r, 0.03597122302158273),
      Weighted(e, 0.03597122302158273),
      Weighted(inv, 0.03597122302158273),
      Weighted(op, 0.03597122302158273),
      Weighted(eqM, 0.03597122302158273),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
        0.03597122302158273
      ),
      Weighted(axiom_{eqM(op(a)(inv(a)(e)))(e)}, 0.03597122302158273),
      Weighted(eqM, 0.7122302158273381)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.03597122302158273),
      Weighted(M, 0.03597122302158273),
      Weighted(M, 0.03597122302158273),
      Weighted((M → (M → M)), 0.03597122302158273),
      Weighted((M → (M → M)), 0.03597122302158273),
      Weighted((M → (M → 𝒰 )), 0.03597122302158273),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
        0.03597122302158273
      ),
      Weighted(∏(a : M){ eqM(op(a)(inv(a)(e)))(e) }, 0.03597122302158273),
      Weighted((M → (M → 𝒰 )), 0.7122302158273381)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 1.0))
  ),
...

val lp_41 = LocalProver(ts_32,cutoff = 5*math.pow(10,-6)).noIsles

lp_41: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(p, 0.03597122302158273),
        Weighted(r, 0.03597122302158273),
        Weighted(e, 0.03597122302158273),
        Weighted(inv, 0.03597122302158273),
        Weighted(op, 0.03597122302158273),
        Weighted(eqM, 0.03597122302158273),
        Weighted(
          axiom_{(eqM(a)(b) \to eqM(op(c)(a))(op(c)(b)))},
          0.03597122302158273
        ),
        Weighted(axiom_{eqM(op(a)(inv(a)(e)))(e)}, 0.03597122302158273),
        Weighted(eqM, 0.7122302158273381)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.03597122302158273),
        Weighted(M, 0.03597122302158273),
        Weighted(M, 0.03597122302158273),
        Weighted((M → (M → M)), 0.03597122302158273),
        Weighted((M → (M → M)), 0.03597122302158273),
        Weighted((M → (M → 𝒰 )), 0.03597122302158273),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → eqM(op(c)(a))(op(c)(b))) } } },
          0.03597122302158273
        ),
        Weighted(∏(a : M){ eqM(op(a)(inv(a)(e)))(e) }, 0.03597122302158273),
        Weighted((M → (M → 𝒰 )), 0.7122302158273381)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 1.0))
...

val lem_41 = lp_41.lemmas.runSyncUnsafe()

lem_41: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.8855928793518824)
)

val negative20_ :FiniteDistribution[Term] = unif(a,b,c)(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)),eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))))(
    eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)),
    eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
    eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(op:Term)*0.6)
val negative20_1 = negative20_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_33 = TermState(negative20_1,negative20_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(inv(r)(e)))(op(p)(e))))

negative20_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.0625),
    Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))), 0.0625),
    Weighted(axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))}, 0.0625),
    Weighted(
      axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e)))},
      0.0625
    ),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))}, 0.0625),
    Weighted(eqM, 0.9),
    Weighted(op, 0.6)
  )
)
negative20_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.034482758620689655),
    Weighted(
      eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
      0.034482758620689655
    ),
    Weighted(
      axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))},
      0.034482758620689655
    ),
    Weighted(
      axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e)))},
      0.034482758620689655
    ),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
      0.034482758620689655
    ),
    Weighted(eqM, 0.496551724137931),
    Weighted(op, 0.3310344827586207)
  )
)
ts_33: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.034482758620689655),
      Weighted(
        eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
        0.034482758620689655
      ),
      Weighted(
        axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))},
        0.034482758620689655
      ),
      Weighted(
        axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e)))},
        0.034482758620689655
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
        0.034482758620689655
      ),
      Weighted(eqM, 0.496551724137931),
      Weighted(op, 0.3310344827586207)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.034482758620689655),
      Weighted(𝒰 , 0.034482758620689655),
      Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.034482758620689655),
      Weighted(
        eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
        0.034482758620689655
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
        0.034482758620689655
      ),
      Weighted((M → (M → 𝒰 )), 0.496551724137931),
...

val lp_42 = LocalProver(ts_33,cutoff = 5*math.pow(10,-6)).noIsles

lp_42: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.034482758620689655),
        Weighted(
          eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
          0.034482758620689655
        ),
        Weighted(
          axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))},
          0.034482758620689655
        ),
        Weighted(
          axiom_{eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e)))},
          0.034482758620689655
        ),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(a)(c) \to eqM(b)(c)))},
          0.034482758620689655
        ),
        Weighted(eqM, 0.496551724137931),
        Weighted(op, 0.3310344827586207)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.034482758620689655),
        Weighted(𝒰 , 0.034482758620689655),
        Weighted(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)), 0.034482758620689655),
        Weighted(
          eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
          0.034482758620689655
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(a)(c) → eqM(b)(c))) } } },
          0.034482758620689655
        ),
...

val lem_42 = lp_42.lemmas.runSyncUnsafe()

lem_42: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op_2(p)(r)(inv(r)(e)))(op(p)(e)), 0.8626794089428854)
)

Step4:

$$p*r*inv(r)(e) = p $$

val negative21_ :FiniteDistribution[Term] = unif(a,b,c)(p,eqM,op)(
    eqM(op(a)(e))(a),
    eqM(op_2(a)(r)(inv(r)(e))(op(a)(e)),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative21_1 = negative21_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_34 = TermState(negative21_1,negative21_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(s))(p)))

negative21_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(p, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(op, 0.05555555555555555),
    Weighted(axiom_{eqM(op(a)(e))(a)}, 0.05555555555555555),
    Weighted(axiom_{eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e))}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.9),
    Weighted(p, 0.6)
  )
)
negative21_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(p, 0.0303030303030303),
    Weighted(eqM, 0.0303030303030303),
    Weighted(op, 0.0303030303030303),
    Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
    Weighted(axiom_{eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e))}, 0.0303030303030303),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.0303030303030303
    ),
    Weighted(eqM, 0.4909090909090909),
    Weighted(p, 0.3272727272727272)
  )
)
ts_34: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(p, 0.0303030303030303),
      Weighted(eqM, 0.0303030303030303),
      Weighted(op, 0.0303030303030303),
      Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
      Weighted(axiom_{eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e))}, 0.0303030303030303),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.0303030303030303
      ),
      Weighted(eqM, 0.4909090909090909),
      Weighted(p, 0.3272727272727272)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.0303030303030303),
      Weighted((M → (M → 𝒰 )), 0.0303030303030303),
      Weighted((M → (M → M)), 0.0303030303030303),
      Weighted(∏(a : M){ eqM(op(a)(e))(a) }, 0.0303030303030303),
      Weighted(
        ∏(a : M){ eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e)) },
        0.0303030303030303
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.0303030303030303
      ),
      Weighted((M → (M → 𝒰 )), 0.4909090909090909),
      Weighted(M, 0.3272727272727272)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(op_2(p)(r)(s))(p), 1.0))),
...

val tg12 = TermGenParams(unAppW = 0.3)
val lp_43 = LocalProver(ts_34,tg12,cutoff = 5*math.pow(10,-6)).noIsles

tg12: TermGenParams = TermGenParams(
  0.1,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_43: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(p, 0.0303030303030303),
        Weighted(eqM, 0.0303030303030303),
        Weighted(op, 0.0303030303030303),
        Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
        Weighted(
          axiom_{eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e))},
          0.0303030303030303
        ),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.0303030303030303
        ),
        Weighted(eqM, 0.4909090909090909),
        Weighted(p, 0.3272727272727272)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.0303030303030303),
        Weighted((M → (M → 𝒰 )), 0.0303030303030303),
        Weighted((M → (M → M)), 0.0303030303030303),
        Weighted(∏(a : M){ eqM(op(a)(e))(a) }, 0.0303030303030303),
        Weighted(
          ∏(a : M){ eqM(op_2(a)(r)(inv(r)(e)))(op(a)(e)) },
          0.0303030303030303
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.0303030303030303
        ),
        Weighted((M → (M → 𝒰 )), 0.4909090909090909),
        Weighted(M, 0.3272727272727272)
      )
    ),
...

val lem_43 = lp_43.lemmas.runSyncUnsafe()

lem_43: Vector[(Typ[Term], Double)] = Vector()

In the following section below we are going to represent inv(r)(e) with variable s.Then we will see that after replacing the inv(r)(e) with s we were able to prove the theorem i.e we are defining $s$ such that $s \in M$ and $s=inv(r)(e)$.And by doing this we are able to get the desired lemma.

In the program below we have skipped a the following steps:- $$s=inv(r)(e) $$ $$\implies r*s = r*inv(r)(e)$$ $$\implies p*(r*s) = p*(r*inv(r)(e)) $$ $$\implies p*r*s = p*r*inv(r)(e) $$ But since we have done it several times previously we wont repeat it again.

val negative22_ :FiniteDistribution[Term] = unif(a,b,c)(p,eqM,op)(
    eqM(op(a)(e))(a),
    eqM(op_2(a)(r)(s))(op(a)(e)),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative22_1 = negative22_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_35 = TermState(negative22_1,negative22_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(s))(p)))

negative22_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(p, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(op, 0.05555555555555555),
    Weighted(axiom_{eqM(op(a)(e))(a)}, 0.05555555555555555),
    Weighted(axiom_{eqM(op_2(a)(r)(s))(op(a)(e))}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.9),
    Weighted(p, 0.6)
  )
)
negative22_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(p, 0.0303030303030303),
    Weighted(eqM, 0.0303030303030303),
    Weighted(op, 0.0303030303030303),
    Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
    Weighted(axiom_{eqM(op_2(a)(r)(s))(op(a)(e))}, 0.0303030303030303),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.0303030303030303
    ),
    Weighted(eqM, 0.4909090909090909),
    Weighted(p, 0.3272727272727272)
  )
)
ts_35: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(p, 0.0303030303030303),
      Weighted(eqM, 0.0303030303030303),
      Weighted(op, 0.0303030303030303),
      Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
      Weighted(axiom_{eqM(op_2(a)(r)(s))(op(a)(e))}, 0.0303030303030303),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.0303030303030303
      ),
      Weighted(eqM, 0.4909090909090909),
      Weighted(p, 0.3272727272727272)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.0303030303030303),
      Weighted((M → (M → 𝒰 )), 0.0303030303030303),
      Weighted((M → (M → M)), 0.0303030303030303),
      Weighted(∏(a : M){ eqM(op(a)(e))(a) }, 0.0303030303030303),
      Weighted(∏(a : M){ eqM(op_2(a)(r)(s))(op(a)(e)) }, 0.0303030303030303),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.0303030303030303
      ),
      Weighted((M → (M → 𝒰 )), 0.4909090909090909),
      Weighted(M, 0.3272727272727272)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(op_2(p)(r)(s))(p), 1.0))),
  Empty
)

val lp_44 = LocalProver(ts_35,tg12,cutoff = 5*math.pow(10,-6)).noIsles

tg12: TermGenParams = TermGenParams(
  0.1,
  0.3,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_43: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(p, 0.0303030303030303),
        Weighted(eqM, 0.0303030303030303),
        Weighted(op, 0.0303030303030303),
        Weighted(axiom_{eqM(op(a)(e))(a)}, 0.0303030303030303),
        Weighted(axiom_{eqM(op_2(a)(r)(s))(op(a)(e))}, 0.0303030303030303),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.0303030303030303
        ),
        Weighted(eqM, 0.4909090909090909),
        Weighted(p, 0.3272727272727272)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.0303030303030303),
        Weighted((M → (M → 𝒰 )), 0.0303030303030303),
        Weighted((M → (M → M)), 0.0303030303030303),
        Weighted(∏(a : M){ eqM(op(a)(e))(a) }, 0.0303030303030303),
        Weighted(∏(a : M){ eqM(op_2(a)(r)(s))(op(a)(e)) }, 0.0303030303030303),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.0303030303030303
        ),
        Weighted((M → (M → 𝒰 )), 0.4909090909090909),
        Weighted(M, 0.3272727272727272)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(eqM(op_2(p)(r)(s))(p), 1.0))),
    Empty
  ),
  TermGenParams(
...

val lem_44 = lp_44.lemmas.runSyncUnsafe()

lem_43: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op_2(p)(r)(s))(p), 0.9160071555311703)
)

val negative23_ :FiniteDistribution[Term] = unif(a,b,c)(eqM(op_2(p)(r)(s))(p),eqM(op_2(p)(r)(inv(r)(e)))(p))(
    eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s)),
    eqM(op_2(p)(r)(s))(p),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative23_1 = negative23_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_36 = TermState(negative23_1,negative23_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(a)(r)(inv(r)(e)))(p)))

negative23_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(eqM(op_2(p)(r)(s))(p), 0.0625),
    Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.0625),
    Weighted(axiom_{eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s))}, 0.0625),
    Weighted(axiom_{eqM(op_2(p)(r)(s))(p)}, 0.0625),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.0625),
    Weighted(eqM, 0.9),
    Weighted(p, 0.6)
  )
)
negative23_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(eqM(op_2(p)(r)(s))(p), 0.034482758620689655),
    Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.034482758620689655),
    Weighted(
      axiom_{eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s))},
      0.034482758620689655
    ),
    Weighted(axiom_{eqM(op_2(p)(r)(s))(p)}, 0.034482758620689655),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.034482758620689655
    ),
    Weighted(eqM, 0.496551724137931),
    Weighted(p, 0.3310344827586207)
  )
)
ts_36: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM(op_2(p)(r)(s))(p), 0.034482758620689655),
      Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.034482758620689655),
      Weighted(
        axiom_{eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s))},
        0.034482758620689655
      ),
      Weighted(axiom_{eqM(op_2(p)(r)(s))(p)}, 0.034482758620689655),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.034482758620689655
      ),
      Weighted(eqM, 0.496551724137931),
      Weighted(p, 0.3310344827586207)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.034482758620689655),
      Weighted(𝒰 , 0.034482758620689655),
      Weighted(eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s)), 0.034482758620689655),
      Weighted(eqM(op_2(p)(r)(s))(p), 0.034482758620689655),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.034482758620689655
      ),
      Weighted((M → (M → 𝒰 )), 0.496551724137931),
      Weighted(M, 0.3310344827586207)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(op_2(a)(r)(inv(r)(e)))(p), 1.0))),
  Empty
)

val lp_45 = LocalProver(ts_36,cutoff = 5*math.pow(10,-6)).noIsles

lp_45: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM(op_2(p)(r)(s))(p), 0.034482758620689655),
        Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.034482758620689655),
        Weighted(
          axiom_{eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s))},
          0.034482758620689655
        ),
        Weighted(axiom_{eqM(op_2(p)(r)(s))(p)}, 0.034482758620689655),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.034482758620689655
        ),
        Weighted(eqM, 0.496551724137931),
        Weighted(p, 0.3310344827586207)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.034482758620689655),
        Weighted(𝒰 , 0.034482758620689655),
        Weighted(
          eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s)),
          0.034482758620689655
        ),
        Weighted(eqM(op_2(p)(r)(s))(p), 0.034482758620689655),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.034482758620689655
        ),
        Weighted((M → (M → 𝒰 )), 0.496551724137931),
        Weighted(M, 0.3310344827586207)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
...

val lem_45 = lp_45.lemmas.runSyncUnsafe()

lem_45: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op_2(p)(r)(inv(r)(e)))(p), 6.694756034589538E-5)
)

Step5:

$$(p*r)*inv(r)(e) = p$$

Basically we will prove $$[ \{(p*r)*inv(r)(e) = p*r*inv(r)(e)\} \land$$ $$\{p*r*inv(r)(e) = p \}] \implies$$ $$(p*r)*inv(r)(e) = p$$

val negative24_ :FiniteDistribution[Term] = unif(a,b,c)(op_2(p)(r)(inv(r)(e)),op(op(p)(r))(inv(r)(e)))(
    eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e))),
    eqM(op_2(p)(r)(inv(r)(e)))(p),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative24_1 = negative24_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_37 = TermState(negative24_1,negative24_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(p)(r))(s))(p)))

negative24_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(op_2(p)(r)(inv(r)(e)), 0.0625),
    Weighted(op(op(p)(r))(inv(r)(e)), 0.0625),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e)))},
      0.0625
    ),
    Weighted(axiom_{eqM(op_2(p)(r)(inv(r)(e)))(p)}, 0.0625),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.0625),
    Weighted(eqM, 0.9),
    Weighted(p, 0.6)
  )
)
negative24_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(op_2(p)(r)(inv(r)(e)), 0.034482758620689655),
    Weighted(op(op(p)(r))(inv(r)(e)), 0.034482758620689655),
    Weighted(
      axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e)))},
      0.034482758620689655
    ),
    Weighted(axiom_{eqM(op_2(p)(r)(inv(r)(e)))(p)}, 0.034482758620689655),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.034482758620689655
    ),
    Weighted(eqM, 0.496551724137931),
    Weighted(p, 0.3310344827586207)
  )
)
ts_37: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(op_2(p)(r)(inv(r)(e)), 0.034482758620689655),
      Weighted(op(op(p)(r))(inv(r)(e)), 0.034482758620689655),
      Weighted(
        axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e)))},
        0.034482758620689655
      ),
      Weighted(axiom_{eqM(op_2(p)(r)(inv(r)(e)))(p)}, 0.034482758620689655),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.034482758620689655
      ),
      Weighted(eqM, 0.496551724137931),
      Weighted(p, 0.3310344827586207)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.034482758620689655),
      Weighted(M, 0.034482758620689655),
      Weighted(
        eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e))),
        0.034482758620689655
      ),
      Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.034482758620689655),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.034482758620689655
      ),
      Weighted((M → (M → 𝒰 )), 0.496551724137931),
      Weighted(M, 0.3310344827586207)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(op(op(p)(r))(s))(p), 1.0))),
...

val tg13 = TermGenParams(unAppW = 0.2)
val lp_46 = LocalProver(ts_37,tg13,cutoff = 2*math.pow(10,-6)).noIsles

tg13: TermGenParams = TermGenParams(
  0.1,
  0.2,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp_46: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(op_2(p)(r)(inv(r)(e)), 0.034482758620689655),
        Weighted(op(op(p)(r))(inv(r)(e)), 0.034482758620689655),
        Weighted(
          axiom_{eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e)))},
          0.034482758620689655
        ),
        Weighted(axiom_{eqM(op_2(p)(r)(inv(r)(e)))(p)}, 0.034482758620689655),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.034482758620689655
        ),
        Weighted(eqM, 0.496551724137931),
        Weighted(p, 0.3310344827586207)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.034482758620689655),
        Weighted(M, 0.034482758620689655),
        Weighted(
          eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e))),
          0.034482758620689655
        ),
        Weighted(eqM(op_2(p)(r)(inv(r)(e)))(p), 0.034482758620689655),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.034482758620689655
        ),
        Weighted((M → (M → 𝒰 )), 0.496551724137931),
        Weighted(M, 0.3310344827586207)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
...

val lem_46 = lp_46.lemmas.runSyncUnsafe()

lem_46: Vector[(Typ[Term], Double)] = Vector(
  (eqM(op(op(p)(r))(inv(r)(e)))(p), 0.007441767680437878)
)

If we follow the same set of steps for q then we will get the same set of resuts as we got for p. For this step let, $$t=inv(r)(e)$$

I have skipped the following steps:- $$t = inv(r)(e)$$ $$\implies r*t = r*inv(r)(e) $$ $$\implies p*(r*t) = p*(r*inv(r)(e))$$ $$\implies p*r*t = p*r*inv(r)(e) $$ Also, $$t = inv(r)(e)$$ $$\implies r*t = r*inv(r)(e) $$ $$\implies q*(r*t) = q*(r*inv(r)(e))$$ $$\implies q*r*t = q*r*inv(r)(e) $$ and, $$p*r*inv(r)(e) = q*r*inv(r)(e)$$ $$\implies p*r*t=q*r*t $$

val negative26_ :FiniteDistribution[Term] = unif(a,b,c,d)(eqM(op_2(q)(r)(t))(q),eqM(op_2(p)(r)(t))(p),eqM(op_2(p)(r)(t))(op_2(q)(r)(t)))(
    eqM(op_2(q)(r)(t))(q),
    eqM(op_2(p)(r)(t))(p),
    eqM(op_2(p)(r)(t))(op_2(q)(r)(t)),
    eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(d) ->: eqM(c)(d)
    )*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(op_2:Term)*0.6)
val negative26_1 = negative26_.filter((t) => !Set(a, b, c,d).contains(t)).normalized()
val ts_38 = TermState(negative26_1,negative26_1.map(_.typ),goals = FiniteDistribution.unif(eqM(p)(q)))

negative26_: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(d, 0.045454545454545456),
    Weighted(eqM(op_2(q)(r)(t))(q), 0.045454545454545456),
    Weighted(eqM(op_2(p)(r)(t))(p), 0.045454545454545456),
    Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.045454545454545456),
    Weighted(axiom_{eqM(op_2(q)(r)(t))(q)}, 0.045454545454545456),
    Weighted(axiom_{eqM(op_2(p)(r)(t))(p)}, 0.045454545454545456),
    Weighted(axiom_{eqM(op_2(p)(r)(t))(op_2(q)(r)(t))}, 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to (eqM(b)(d) \to eqM(c)(d))))},
      0.045454545454545456
    ),
    Weighted(eqM, 0.9),
    Weighted(op_2, 0.6)
  )
)
negative26_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(eqM(op_2(q)(r)(t))(q), 0.024999999999999998),
    Weighted(eqM(op_2(p)(r)(t))(p), 0.024999999999999998),
    Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.024999999999999998),
    Weighted(axiom_{eqM(op_2(q)(r)(t))(q)}, 0.024999999999999998),
    Weighted(axiom_{eqM(op_2(p)(r)(t))(p)}, 0.024999999999999998),
    Weighted(axiom_{eqM(op_2(p)(r)(t))(op_2(q)(r)(t))}, 0.024999999999999998),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(a)(c) \to (eqM(b)(d) \to eqM(c)(d))))},
      0.024999999999999998
    ),
    Weighted(eqM, 0.49499999999999994),
    Weighted(op_2, 0.32999999999999996)
  )
)
ts_38: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM(op_2(q)(r)(t))(q), 0.024999999999999998),
      Weighted(eqM(op_2(p)(r)(t))(p), 0.024999999999999998),
      Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.024999999999999998),
      Weighted(axiom_{eqM(op_2(q)(r)(t))(q)}, 0.024999999999999998),
      Weighted(axiom_{eqM(op_2(p)(r)(t))(p)}, 0.024999999999999998),
      Weighted(axiom_{eqM(op_2(p)(r)(t))(op_2(q)(r)(t))}, 0.024999999999999998),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(a)(c) \to (eqM(b)(d) \to eqM(c)(d))))},
        0.024999999999999998
      ),
      Weighted(eqM, 0.49499999999999994),
      Weighted(op_2, 0.32999999999999996)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.024999999999999998),
      Weighted(𝒰 , 0.024999999999999998),
      Weighted(𝒰 , 0.024999999999999998),
      Weighted(eqM(op_2(q)(r)(t))(q), 0.024999999999999998),
      Weighted(eqM(op_2(p)(r)(t))(p), 0.024999999999999998),
      Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.024999999999999998),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(a)(c) → (eqM(b)(d) → eqM(c)(d)))) } } } },
        0.024999999999999998
      ),
      Weighted((M → (M → 𝒰 )), 0.49499999999999994),
      Weighted((M → (M → (M → M))), 0.32999999999999996)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(eqM(p)(q), 1.0))),
  Empty
)

val lp_47 = LocalProver(ts_38,cutoff = 1.5*math.pow(10,-6)).noIsles

lp_47: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM(op_2(q)(r)(t))(q), 0.024999999999999998),
        Weighted(eqM(op_2(p)(r)(t))(p), 0.024999999999999998),
        Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.024999999999999998),
        Weighted(axiom_{eqM(op_2(q)(r)(t))(q)}, 0.024999999999999998),
        Weighted(axiom_{eqM(op_2(p)(r)(t))(p)}, 0.024999999999999998),
        Weighted(
          axiom_{eqM(op_2(p)(r)(t))(op_2(q)(r)(t))},
          0.024999999999999998
        ),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(a)(c) \to (eqM(b)(d) \to eqM(c)(d))))},
          0.024999999999999998
        ),
        Weighted(eqM, 0.49499999999999994),
        Weighted(op_2, 0.32999999999999996)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.024999999999999998),
        Weighted(𝒰 , 0.024999999999999998),
        Weighted(𝒰 , 0.024999999999999998),
        Weighted(eqM(op_2(q)(r)(t))(q), 0.024999999999999998),
        Weighted(eqM(op_2(p)(r)(t))(p), 0.024999999999999998),
        Weighted(eqM(op_2(p)(r)(t))(op_2(q)(r)(t)), 0.024999999999999998),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ ∏(d : M){ (eqM(a)(b) → (eqM(a)(c) → (eqM(b)(d) → eqM(c)(d)))) } } } },
          0.024999999999999998
        ),
        Weighted((M → (M → 𝒰 )), 0.49499999999999994),
        Weighted((M → (M → (M → M))), 0.32999999999999996)
      )
    ),
    Vector(),
...

val lem_47 = lp_47.lemmas.runSyncUnsafe()

lem_47: Vector[(Typ[Term], Double)] = Vector((eqM(p)(q), 0.8666263127340152))