The evaluation of PROVE-FILE on the file: #./mg/c-predefined4.events was completed successfully. Nqthm-1992 mods: (PC-NQTHM-1992) Here is the list of names of the nondefinitional axioms assumed: (MG-MAX-TEMP-STK-SIZE-NUMBERP MG-MAX-CTRL-STK-SIZE-SMALL-NATURALP) No actions involving undoing, i.e., uses of UBT, were encountered. Total Statistics: [ 38.4 13.1 3.5 ] Start of run: April 4, 2000 11:18:22 End of run: April 4, 2000 11:19:42