program invited: 
../atp/ArgoCLP/./ArgoCLP -n axioms/th_7_04.txt axioms/ax_for_th_7_04.txt 

----------------------------------------------------
The complete proof:
----------------------------------------------------
The Isar proof is in: 
proofs/nonoptimized_isar_proof_th_7_04.thy

The proof in the natural language form is in: 
proofs/nonoptimized_nl_proof_th_7_04.tex

The proof in xml format is in: 
proofs/nonoptimized_theorem_th_7_04.xml

The number of axioms used: 6
The list of used axioms:
ax_branch_inc_po_l NONE ax_I2 ax_g1 ax_D6 ax_D1a 

----------------------------------------------------
The clean proof: 
----------------------------------------------------
The Isar proof is in: 
proofs/isar_proof_th_7_04.thy

The proof in the natural language form is in: 
proofs/nl_proof_th_7_04.tex

The proof in xml format is in: 
proofs/theorem_th_7_04.xml

The list of all axioms considered (given and derived) is in: all_axioms.txt.

Basic time: 0.175242 seconds. 
Cleaning time: 0.022053 seconds. 
Total time: 0.197295 seconds. 

