# Format of the E protocol files for FV-Indexing experiments.

Columns numbers start at 0.
All numbers refer to the final proof state after termination.

00 Problem name
01 Status         ([T]heorem, [N]on-theorem, [F]ailure)
02 CPU Time 
03 Reason for termination
04 Prover version number
05 Number of processed clauses
06 Unification attempts
07 Unification successes
08 Number of generated clauses
09 Number of paramodulations
10 Size of the processed clause set
11 Size of the unprocessed clause set
12 Clause-clause subsumption calls
13 Clause-clause subsumption calls going into recursive matching
14 Unit Clause-clause subsumption calls
15 Forward-subsumed clauses
16 Backward-subsumed clauses
17 PC(MguTimer)
18 PC(SatTimer)       
19 PC(ParamodTimer)   
20 PC(PMIndexTimer)   
21 PC(BWRWTimer)      
22 PC(BWRWIndexTimer) 
23 PC(FreqVecTimer)   
24 PC(FVIndexTimer)   
25 PC(SubsumeTimer)   
26 PC(SetSubsumeTimer)