How to reconstruct with Agda the proof of a theorem produced by one ATP

Question

I am trying to prove a theorem of differential geometry: the Cartan structural equation.

I am using the following code

 cnf(axio1,axiom,
   (w(h(X))= zero)).

cnf(axio2,axiom,
   (w(v(X))= v(X))).
cnf(axio2A,axiom,
   (X= sum(h(X),v(X))  )).

cnf(axio3A,axiom,
   (dw(sum(X,Y),Z)= sum(dw(X,Z),dw(Y,Z))  )).
cnf(axio3,axiom,
   (dw(X,sum(Y,Z))= sum(dw(X,Y),dw(X,Z))  )).

cnf(axio4,axiom,
   (w(sum(X,Y))= sum(w(X),w(Y))  )).

cnf(axio5,axiom,
   (sum(zero,X)= X  )).

cnf(axio5A,axiom,
   (sum(X,sum(Y,Z))= sum(sum(X,Y),Z)  )).

cnf(axio6,axiom,
   (dw(X,Y)= divi(subst(subst(act(X,w(Y)),act(Y,w(X))),w(commu(X,Y))),two)  )).


cnf(axio6A,axiom,
   (subst(zero,zero) = zero      )).

cnf(axio6B,axiom,
   (subst(zero,X) = minus(X)      )).


cnf(axio7,axiom,
   (act(X,w(v(Y)))=zero                )).


cnf(axio7A,axiom,
   (act(X,zero)=zero                )).

cnf(axio8,axiom,
   (commu(h(X),v(Y))=h(z)                    )).

cnf(axio9,axiom,
    (minus(zero)=zero)).

cnf(axio10,axiom,
    (divi(zero,two) = zero      )).

cnf(axio11,axiom,
    (commu(X,Y)=minus(commu(Y,X))      )).

cnf(axio12,axiom,
    (w(minus(X))=minus(w(X))  )).

cnf(axio13,axiom,
   (sum(zero,X) = X        )).

cnf(axio14,axiom,
   (divi(minus(X),two) =minus(divi(X,two))  )).

cnf(axio14A,axiom,
   (sum(minus(X),X) = zero       )).

cnf(axio15,axiom,
    (w(commu(v(X),v(Y))) = commu(v(X),v(Y))      )).

cnf(axio15A,axiom,
   ( omega(X,Y)=dw(h(X),h(Y))              )).  

cnf(goal,negated_conjecture,
   (sum(dw(X,Y),divi(commu(w(X),w(Y)),two))!=  
omega(X,Y)   )).

The following ATPs were able to produce the proof: Bliksem, CiME, CVC4, E, EQP, Fiesta, Geo, Isabelle, Isabelle-HOT, LEO-II, Matita, Metis, Otter, Prover9, SNARK, SPASS, Vampire, Vampire-SAT.

My question is: how to reconstruct with Agda the proof generated by the mentioned ATPs?