In[]:=
FindEquationalProof[a·bb·a,ForAll[{a,b,c},((a·b)·c)·(a·((a·c)·a))c]]
In[]:=
CountsFirst/@KeysNormalProofObject
Logic: EquationalLogic
Steps: 102
Theorem: a·bb·a
["ProofDataset"]
Out[]=
Axiom1,Hypothesis1,CriticalPairLemma52,SubstitutionLemma47,Conclusion1
​