The evaluation of PROVE-FILE on the file: #./flatau/app-f.events was completed successfully. Here is the list of names of the nondefinitional axioms assumed: (P-PRESERVES-PROPER-P-STATEP ONCE-ERRORP-ALWAYS-ERRORP ONCE-ERRORP-ALWAYS-ERRORP-STEP P-STEP-PRESERVES-PROPER-P-STATEP) No actions involving undoing, i.e., uses of UBT, were encountered. Total Statistics: [ 11.1 556.7 42.0 ] Start of run: April 2, 2000 22:08:05 End of run: April 2, 2000 22:18:50