[Hol-builds] SUCCESS: -expk:18a4494:mosml2.01

[<Mic...@ni...>]

Running in /import/atp-linhome/home/1/michaeln/current-hols/expkhol on machine atp-login1
Uname info (srm): Linux 2.6.32-5-686 i686
Cpu: Intel(R) Xeon(R) CPU E5405 @ 2.00GHz  x 8
Memory: 3037 MB
ML Implementation: mosml2.01
Started: Fri, 23 Dec 2011 02:00:04 +1100
Extra commandline arguments: -selftest 2
Revision: 18a4494 Start on properties of register machine 'copy program'.
Already up-to-date.
-- Configuration Description Ends --

Building directory tools/mlyacc/mlyacclib                      [23 Dec, 02:00:58]
Building directory src/portableML/mosml                        [23 Dec, 02:00:59]
Building directory src/portableML                              [23 Dec, 02:01:00]
Building directory src/prekernel                               [23 Dec, 02:01:05]
Building directory src/experimental-kernel                     [23 Dec, 02:01:09]
Building directory src/postkernel                              [23 Dec, 02:01:11]
Building directory src/parse                                   [23 Dec, 02:01:14]
Building directory src/bool                                    [23 Dec, 02:01:33]
Building directory src/1                                       [23 Dec, 02:01:40]
Building directory src/proofman                                [23 Dec, 02:02:02]
Building directory src/compute/src                             [23 Dec, 02:02:04]
Building directory src/HolSat/sat_solvers/minisat              [23 Dec, 02:02:06]
Building directory src/HolSat/sat_solvers/zc2hs                [23 Dec, 02:02:06]
Building directory src/HolSat                                  [23 Dec, 02:02:06]
Building directory src/taut                                    [23 Dec, 02:02:10]
Building directory src/marker                                  [23 Dec, 02:02:11]
Building directory src/q                                       [23 Dec, 02:02:14]
Building directory src/combin                                  [23 Dec, 02:02:16]
Building directory src/lite                                    [23 Dec, 02:02:20]
Building directory src/refute                                  [23 Dec, 02:02:20]
Building directory src/simp/src                                [23 Dec, 02:02:22]
Building directory src/metis                                   [23 Dec, 02:02:30]
Building directory src/meson/src                               [23 Dec, 02:02:50]
Building directory src/IndDef                                  [23 Dec, 02:02:52]
Building directory src/basicProof                              [23 Dec, 02:02:56]
Building directory src/relation                                [23 Dec, 02:02:56]
Building directory src/one                                     [23 Dec, 02:03:23]
Building directory src/pair/src                                [23 Dec, 02:03:27]
Building directory src/sum                                     [23 Dec, 02:04:00]
Building directory src/tfl/src                                 [23 Dec, 02:04:05]
Building directory src/option                                  [23 Dec, 02:04:09]
Building directory src/num/theories                            [23 Dec, 02:04:22]
Building directory src/num/reduce/src                          [23 Dec, 02:05:51]
Building directory src/num/arith/src                           [23 Dec, 02:05:52]
Building directory src/num                                     [23 Dec, 02:06:09]
Building directory src/num/termination                         [23 Dec, 02:06:09]
Building directory src/num/extra_theories                      [23 Dec, 02:06:10]
Building directory src/pred_set/src                            [23 Dec, 02:07:19]
Building directory src/datatype/equiv                          [23 Dec, 02:12:34]
Building directory src/datatype/record                         [23 Dec, 02:12:35]
Building directory src/datatype                                [23 Dec, 02:12:35]
Building directory src/list/src                                [23 Dec, 02:13:20]
Building directory src/quantHeuristics                         [23 Dec, 02:14:50]
Building directory src/unwind                                  [23 Dec, 02:15:20]
Building directory src/boss                                    [23 Dec, 02:15:21]
Building directory src/tfl/src/test                            [23 Dec, 02:15:22]
Building directory src/TeX                                     [23 Dec, 02:16:07]
Building directory examples/RSA                                [23 Dec, 02:16:21]
Building directory src/sort                                    [23 Dec, 02:17:22]
Building directory src/string                                  [23 Dec, 02:18:06]
Building directory src/string/theorytesting                    [23 Dec, 02:19:08]
Building directory examples/STE                                [23 Dec, 02:19:27]
Building directory src/res_quan/src                            [23 Dec, 02:20:08]
Building directory src/quotient/src                            [23 Dec, 02:20:19]
Building directory src/quotient/examples                       [23 Dec, 02:21:56]
Building directory src/finite_map                              [23 Dec, 02:23:08]
Building directory examples/ind_def                            [23 Dec, 02:24:27]
Building directory examples/decidable_separationLogic/src/     [23 Dec, 02:25:43]
Building directory src/bag                                     [23 Dec, 02:34:19]
Building directory examples/unification/triangular/first-order [23 Dec, 02:35:44]
Building directory src/n-bit                                   [23 Dec, 02:39:29]
Building directory examples/ARM/arm6-verification              [23 Dec, 02:49:39]
Building directory examples/ARM/arm6-verification/correctness  [23 Dec, 02:56:10]
Building directory src/ring/src                                [23 Dec, 03:38:04]
Building directory src/integer                                 [23 Dec, 03:39:43]
Building directory examples/rings                              [23 Dec, 03:44:16]
Building directory src/llist                                   [23 Dec, 03:45:14]
Building directory src/path                                    [23 Dec, 03:47:16]
Building directory src/integer/testing                         [23 Dec, 03:48:03]
Building directory src/patricia                                [23 Dec, 03:49:50]
Building directory src/update                                  [23 Dec, 03:52:23]
Building directory src/emit                                    [23 Dec, 03:52:35]
Building directory examples/ARM/v4                             [23 Dec, 04:00:54]
Building directory examples/ARM/v7                             [23 Dec, 04:27:02]
Building directory src/hol88                                   [23 Dec, 05:44:04]
Building directory src/quotient/examples/lambda                [23 Dec, 05:44:04]
Building directory src/quotient/examples/sigma                 [23 Dec, 05:46:59]
Building directory src/rational                                [23 Dec, 05:50:18]
Building directory src/real                                    [23 Dec, 05:52:51]
Building directory src/complex                                 [23 Dec, 05:57:22]
Building directory examples/separationLogic/src/               [23 Dec, 05:58:02]
Building directory src/HolQbf                                  [23 Dec, 06:11:45]
Building directory src/HolSmt                                  [23 Dec, 06:11:55]
Building directory src/opentheory                              [23 Dec, 06:17:19]
Building directory examples/misc                               [23 Dec, 06:17:45]
Building directory examples/muddy/muddyC                       [23 Dec, 06:18:52]
Building directory examples/muddy                              [23 Dec, 06:18:52]
Building directory examples/HolBdd                             [23 Dec, 06:18:53]
Building directory examples/HolCheck                           [23 Dec, 06:19:22]
Building directory src/datatype/inftree                        [23 Dec, 06:32:14]
Building directory examples/lambda/basics                      [23 Dec, 06:32:26]
Building directory examples/unification/triangular/nominal     [23 Dec, 06:35:51]
Building directory examples/lambda/barendregt                  [23 Dec, 06:46:52]
Building directory examples/computability                      [23 Dec, 06:56:11]
Building directory examples/lambda/other-models                [23 Dec, 06:57:32]
Building directory examples/lambda/typing                      [23 Dec, 07:03:07]
Building directory examples/computability/lambda               [23 Dec, 07:05:08]
Building directory examples/computability/register             [23 Dec, 07:23:05]
Building directory src/Boolify/src                             [23 Dec, 07:23:40]
Building directory src/float                                   [23 Dec, 07:25:14]
Building directory src/prob                                    [23 Dec, 07:27:11]
Building directory src/temporal/src                            [23 Dec, 07:30:15]
Building directory examples/parity                             [23 Dec, 07:31:23]
Building directory examples/MLsyntax                           [23 Dec, 07:31:45]
Building directory examples/zfset                              [23 Dec, 07:32:04]
Building directory examples/category                           [23 Dec, 07:33:45]
Building directory examples/miller/ho_prover                   [23 Dec, 07:41:23]
Building directory examples/miller/miller                      [23 Dec, 07:41:37]
Building directory examples/ordinal                            [23 Dec, 08:17:14]
Building directory examples/Crypto/AES                         [23 Dec, 08:18:28]
Building directory examples/Crypto/IDEA                        [23 Dec, 08:47:51]
Building directory examples/Crypto/MARS                        [23 Dec, 08:50:07]
Building directory examples/Crypto/RC6                         [23 Dec, 08:52:25]
Building directory examples/Crypto/Serpent/Reference           [23 Dec, 08:53:14]
Building directory examples/Crypto/Serpent/Bitslice            [23 Dec, 09:26:20]
Building directory examples/Crypto/SHA-1                       [23 Dec, 09:57:53]
Building directory examples/Crypto/TEA                         [23 Dec, 09:58:44]
Building directory examples/Crypto/TWOFISH                     [23 Dec, 09:59:36]