Using Leo II to prove Theorems in Frobenius Algebras

Question

Using the ATP Leo II with the TPTP thf language it is possible to prove many theorems in Frobenius algebras and open-closed cobordisms. I an using the following code

 thf(alpha_decl,type,(alpha: $aaxa > $axaa)).
thf(invalpha_decl,type,(invalpha: $axaa > $aaxa )).
thf(mu_decl,type,(mu: $aa > $a )).
thf(eta_decl,type,(eta: $i > $a )).
thf(muid_decl,type,(muid: $aaxa > $aa )).
thf(idmu_decl,type,(idmu: $axaa > $aa )).
thf(etaid_decl,type,(etaid: $ja > $aa )).
thf(ideta_decl,type,(ideta: $ai > $aa )).
thf(lamb_decl,type,(lamb: $ja > $a )).
thf(rho_decl,type,(rho: $ai > $a )).
thf(delta_decl,type,(delta: $a > $aa )).


thf(deltaid_decl,type,(deltaid: $aa > $aaxa )).
thf(iddelta_decl,type,(iddelta: $aa > $axaa )).
thf(epsilon_decl,type,(epsilon: $a > $i )).
thf(invlamb_decl,type,(invlamb: $a > $ja )).
thf(invrho_decl,type,(invrho: $a > $ai )).
thf(epsilonid_decl,type,(epsilonid: $aa > $ja )).
thf(idepsilon_decl,type,(idepsilon: $aa > $ai )).
thf(id_decl,type,(id: $a > $a )).
thf(beta1_decl,type,( beta1: $a > $ai )).
thf(beta2_decl,type,(beta2: $a > $ja )).
thf(invbeta1_decl,type,(invbeta1: $ai > $a )).
thf(invbeta2_decl,type,(invbeta2: $ja > $a )).
thf(axio1,axiom,(! [X: $ja] :
      ( (lamb @ X)  = (mu @ (etaid @ X ) )   )    )).
thf(axio2,axiom,(! [X: $ai] :
      ( (rho @ X)  = (mu @ (ideta @ X ) )   )    )).
thf(axio3,axiom,(! [X: $aaxa] :
      ( (mu @ (idmu @ (alpha @ X))   )  = (mu @ (muid @ X) )   )    )).
thf(axio4,axiom,(! [X: $a] :
      ( (iddelta @ (delta @ X) )  = (alpha @ (deltaid @ (delta @ X)) ) )   )).
thf(axio5,axiom,(! [X: $a] :
      (  (epsilonid @ (delta @ X) )  = (invlamb @ X )    )   )).
thf(axio6,axiom,(! [X: $a] :
      (  (idepsilon @ (delta @ X) )  = (invrho @ X )    )   )).
thf(axio7,axiom,(! [X: $aa] :
      (  (muid @ (invalpha @ (iddelta @ X))    )  = (delta @ (mu @ X))    )   )).
thf(axio8,axiom,(! [X: $aa] :
      (  (idmu @ (alpha @ (deltaid @ X))    )  = (delta @ (mu @ X))    )   )).
thf(axio9,axiom,(! [X: $a] :
      (  (mu @ (ideta @ (beta1 @ X))    )  = (id @ X)    )   )).
thf(axio10,axiom,(! [X: $a] :
      (  (mu @ (etaid @ (beta2 @ X))    )  = (id @ X)    )   )).
thf(axio11,axiom,(! [X: $a] :
      (  (invbeta1 @ (idepsilon @ (delta @ X))    )  = (id @ X)    )   )).
thf(axio12,axiom,(! [X: $a] :
      (  (invbeta2 @ (epsilonid @ (delta @ X))    )  = (id @ X)    )   )).
thf(axio13,axiom,(! [X: $a] :
      (  (id @ (id @ X)    )  = (id @ X)    )   )).

thf(axio14,axiom,(! [X: $a] :
      (  (delta @ (id @ X)    )  = (delta @ X)    )   )).

For example it is possible to prove that

using the previous code with the following sentences

    thf(conj,conjecture,(! [X: $ja] :
      ( (idepsilon @ (idmu @ (alpha @ (deltaid @ (etaid @ X))) )  ) = 
        (idepsilon @ (delta @ (mu @ (etaid @ X))))
                 )  )).
thf(conj2,conjecture,(! [X: $a] :
      ( (invbeta1 @ (idepsilon @ (delta @ (mu @ (etaid @ (beta2 @ X)))) )  ) = 
        (id @ X)
                 )  )).
thf(conj3,conjecture,(! [X: $ai] :
      ( (epsilonid @ (muid @ (invalpha @ (iddelta @ (ideta @ X))) )  ) = 
        (epsilonid @ (delta @ (mu @ (ideta @ X))))
                 )  )).
thf(conj4,conjecture,(! [X: $a] :
      ( (invbeta2 @ (epsilonid @ (delta @ (mu @ (ideta @ (beta1 @ X)))) )  ) = 
        (id @ X)
                 )  )).

and the output that Leo II generates is

 % END OF SYSTEM OUTPUT
% RESULT: SOT_RS_aB8 - LEO-II---1.6.2 says Theorem - CPU = 0.05 WC = 0.17 
% OUTPUT: SOT_RS_aB8 - LEO-II---1.6.2 says CNFRefutation - CPU = 0.05 WC = 0.17 

My questions is: How to extract a proof for humans from the output of Leo II using sledgehammer?

Please take a look at Frobenius algebras with Z3