Skip to content
Success

Console Output

01:40:59 Started by an SCM change

01:40:59 [EnvInject] - Loading node environment variables.

01:40:59 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark

01:40:59 [isabelle-nightly-benchmark] $ hg showconfig paths.default

01:40:59 [isabelle-nightly-benchmark] $ hg pull --rev default

01:41:00 pulling from http://isabelle.in.tum.de/repos/isabelle/

01:41:00 searching for changes

01:41:00 no changes found

01:41:00 [isabelle-nightly-benchmark] $ hg update --clean --rev default

01:41:00 10 files updated, 0 files merged, 2 files removed, 0 files unresolved

01:41:00 [isabelle-nightly-benchmark] $ hg --config extensions.purge= clean --all

01:41:00 [isabelle-nightly-benchmark] $ hg log --rev . --template {node}

01:41:00 [isabelle-nightly-benchmark] $ hg log --rev . --template {rev}

01:41:00 [isabelle-nightly-benchmark] $ hg log --rev 805d0a9a4e3769f5a34750386bc34d65e72e8b6a --template exists\n

01:41:00 exists

01:41:00 [isabelle-nightly-benchmark] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(805d0a9a4e3769f5a34750386bc34d65e72e8b6a)" --encoding UTF-8 --encodingmode replace

01:41:01 No emails were triggered.

01:41:01 [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/hudson876320670550540156.sh

01:41:01 + Admin/jenkins/run_build benchmark

01:41:01 + set -e

01:41:01 + PROFILE=benchmark

01:41:01 + shift

01:41:01 + bin/isabelle components -a

01:41:01 + bin/isabelle jedit -bf

01:41:01 ### Building graph browser ...

01:41:01 warning: [options] bootstrap class path not set in conjunction with -source 1.4

01:41:01 warning: [options] source value 1.4 is obsolete and will be removed in a future release

01:41:01 warning: [options] target value 1.4 is obsolete and will be removed in a future release

01:41:01 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.

01:41:02 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.

01:41:02 Note: Recompile with -Xlint:deprecation for details.

01:41:02 4 warnings

01:41:03 ### Building Isabelle/Scala ...

01:43:17 ### Building Isabelle/jEdit ...

01:43:44 + bin/isabelle ci_build_benchmark

01:43:50

01:43:50 === CONFIGURATION ===

01:43:50

01:43:50 ISABELLE_BUILD_OPTIONS=""

01:43:50

01:43:50 ML_PLATFORM="x86_64-linux"

01:43:50 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

01:43:50 ML_SYSTEM="polyml-5.6"

01:43:50 ML_OPTIONS="-H 4000 --maxheap 8G"

01:43:51

01:43:51 === BUILD ===

01:43:51

01:43:51 Build started at Mon, 27 Feb 2017 00:43:50 GMT

01:43:51 Isabelle id 002b4c8c366e

01:43:51

01:43:51 === LOG ===

01:43:51

01:43:51 Session Pure/Pure

01:43:51 Session HOL/HOL (main)

01:43:52 Session HOL/HOL-Algebra (main timing)

01:43:53 Session HOL/HOL-Analysis (main timing)

01:43:53 Session HOL/HOL-Probability (timing)

01:43:53 Session HOL/HOL-Probability-ex (timing)

01:43:53 Session HOL/HOL-Auth (timing)

01:43:53 Session HOL/HOL-UNITY (timing)

01:43:53 Session HOL/HOL-Bali (timing)

01:43:53 Session HOL/HOL-Cardinals (timing)

01:43:53 Session HOL/HOL-Corec_Examples (timing)

01:43:53 Session HOL/HOL-Data_Structures (timing)

01:43:54 Session HOL/HOL-Datatype_Benchmark

01:43:54 Session HOL/HOL-Datatype_Examples (timing)

01:43:54 Session HOL/HOL-Decision_Procs (timing)

01:43:54 Session HOL/HOL-Hoare_Parallel (timing)

01:43:54 Session HOL/HOL-IMP (timing)

01:43:54 Session HOL/HOL-Library (main timing)

01:43:55 Session HOL/HOL-Metis_Examples (timing)

01:43:55 Session HOL/HOL-MicroJava (timing)

01:43:55 Session HOL/HOL-Nominal

01:43:55 Session HOL/HOL-Nominal-Examples (timing)

01:43:55 Session HOL/HOL-Nonstandard_Analysis (timing)

01:43:55 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

01:43:55 Session HOL/HOL-Number_Theory (timing)

01:43:56 Session HOL/HOL-Predicate_Compile_Examples (timing)

01:43:56 Session HOL/HOL-Quickcheck_Benchmark

01:43:56 Session HOL/HOL-Quickcheck_Examples (timing)

01:43:56 Session HOL/HOL-Quotient_Examples (timing)

01:43:56 Session HOL/HOL-Record_Benchmark

01:43:56 Session HOL/HOL-SET_Protocol (timing)

01:43:56 Session HOL/HOL-Word (main timing)

01:43:56 Session HOL/HOL-Word-SMT_Examples (timing)

01:43:56 Session HOL/HOLCF (main timing)

01:43:57 Session HOL/IOA (timing)

01:43:57 Session HOL/HOL-Proofs (timing)

01:43:57 Session HOL/HOL-Proofs-Extraction (timing)

01:43:57 Session HOL/HOL-Proofs-Lambda (timing)

01:43:57 Session ZF/ZF (main timing ZF)

01:43:57 Session ZF/ZF-UNITY (timing ZF)

01:43:57 Building Pure ...

01:44:12 Pure: theory Pure

01:44:12 Pure: theory ML_Bootstrap

01:44:16 Timing Pure (1 threads, 0.661s elapsed time, 0.660s cpu time, 0.000s GC time, factor 1.00)

01:44:16 Finished Pure (0:00:17 elapsed time, 0:00:17 cpu time, factor 1.00)

01:44:16 Building HOL ...

01:44:17 HOL: theory Code_Generator

01:44:20 HOL: theory HOL

01:44:24 HOL: theory Argo

01:44:24 HOL: theory Ctr_Sugar

01:44:24 HOL: theory Orderings

01:44:25 HOL: theory SAT

01:44:25 HOL: theory Groups

01:44:28 HOL: theory Lattices

01:44:30 HOL: theory Set

01:44:31 HOL: theory Fun

01:44:31 HOL: theory Typedef

01:44:31 HOL: theory Rings

01:44:32 HOL: theory Complete_Lattices

01:44:35 HOL: theory Inductive

01:44:37 HOL: theory Product_Type

01:44:37 HOL: theory Sum_Type

01:44:38 HOL: theory Complete_Partial_Order

01:44:43 HOL: theory Nat

01:44:45 HOL: theory Fields

01:44:45 HOL: theory Meson

01:44:46 HOL: theory ATP

01:44:48 HOL: theory Metis

01:44:50 HOL: theory Finite_Set

01:44:51 HOL: theory Relation

01:44:53 HOL: theory Transitive_Closure

01:44:54 HOL: theory Wellfounded

01:44:55 HOL: theory Fun_Def_Base

01:44:55 HOL: theory Hilbert_Choice

01:44:55 HOL: theory Wfrec

01:44:55 HOL: theory Order_Relation

01:44:56 HOL: theory BNF_Wellorder_Relation

01:44:56 HOL: theory Zorn

01:44:56 HOL: theory BNF_Wellorder_Embedding

01:44:56 HOL: theory BNF_Wellorder_Constructions

01:44:57 HOL: theory BNF_Cardinal_Order_Relation

01:44:58 HOL: theory BNF_Cardinal_Arithmetic

01:44:59 HOL: theory BNF_Def

01:45:01 HOL: theory BNF_Composition

01:45:01 HOL: theory Basic_BNFs

01:45:02 HOL: theory BNF_Fixpoint_Base

01:45:05 HOL: theory BNF_Least_Fixpoint

01:45:07 HOL: theory Basic_BNF_LFPs

01:45:07 HOL: theory Transfer

01:45:08 HOL: theory Num

01:45:12 HOL: theory Power

01:45:15 HOL: theory Groups_Big

01:45:17 HOL: theory Equiv_Relations

01:45:17 HOL: theory Lifting

01:45:19 HOL: theory Lifting_Set

01:45:19 HOL: theory Option

01:45:19 HOL: theory Quotient

01:45:19 HOL: theory Extraction

01:45:19 HOL: theory Lattices_Big

01:45:19 HOL: theory Partial_Function

01:45:20 HOL: theory Fun_Def

01:45:21 HOL: theory Int

01:45:24 HOL: theory Nat_Transfer

01:45:24 HOL: theory Euclidean_Division

01:45:29 HOL: theory Parity

01:45:31 HOL: theory Divides

01:45:39 HOL: theory Code_Numeral

01:45:39 HOL: theory Numeral_Simprocs

01:45:39 HOL: theory SMT

01:45:39 HOL: theory Set_Interval

01:45:40 HOL: theory Semiring_Normalization

01:45:42 HOL: theory Conditionally_Complete_Lattices

01:45:42 HOL: theory Filter

01:45:42 HOL: theory Groebner_Basis

01:45:43 HOL: theory Presburger

01:45:45 HOL: theory Sledgehammer

01:45:47 HOL: theory List

01:45:55 HOL: theory Groups_List

01:45:55 HOL: theory Map

01:45:56 HOL: theory Random

01:45:56 HOL: theory Enum

01:45:59 HOL: theory String

01:45:59 HOL: theory BNF_Greatest_Fixpoint

01:46:00 HOL: theory Predicate

01:46:00 HOL: theory Typerep

01:46:01 HOL: theory Lazy_Sequence

01:46:02 HOL: theory Limited_Sequence

01:46:02 HOL: theory Code_Evaluation

01:46:04 HOL: theory Quickcheck_Random

01:46:06 HOL: theory Quickcheck_Exhaustive

01:46:06 HOL: theory Quickcheck_Narrowing

01:46:06 HOL: theory Random_Pred

01:46:07 HOL: theory Random_Sequence

01:46:11 HOL: theory Record

01:46:11 HOL: theory Predicate_Compile

01:46:13 HOL: theory Nitpick

01:46:18 HOL: theory Main

01:46:20 HOL: theory Archimedean_Field

01:46:20 HOL: theory Binomial

01:46:20 HOL: theory GCD

01:46:20 HOL: theory Topological_Spaces

01:46:26 HOL: theory Rat

01:46:29 HOL: theory Real

01:46:31 HOL: theory Real_Vector_Spaces

01:46:43 HOL: theory Inequalities

01:46:43 HOL: theory Limits

01:46:47 HOL: theory Deriv

01:46:47 HOL: theory Series

01:46:48 HOL: theory NthRoot

01:46:49 HOL: theory Transcendental

01:46:54 HOL: theory Complex

01:46:54 HOL: theory MacLaurin

01:46:55 HOL: theory Complex_Main

01:47:55 Timing HOL (6 threads, 171.327s elapsed time, 521.564s cpu time, 34.220s GC time, factor 3.04)

01:47:55 Finished HOL (0:03:38 elapsed time, 0:10:41 cpu time, factor 2.94)

01:47:57 Building HOL-Proofs ...

01:47:57 HOL-Proofs: theory Proofs

01:47:58 HOL-Proofs: theory Code_Generator

01:48:00 HOL-Proofs: theory HOL

01:48:05 HOL-Proofs: theory Argo

01:48:05 HOL-Proofs: theory Ctr_Sugar

01:48:05 HOL-Proofs: theory Orderings

01:48:06 HOL-Proofs: theory SAT

01:48:07 HOL-Proofs: theory Groups

01:48:12 HOL-Proofs: theory Lattices

01:48:17 HOL-Proofs: theory Set

01:48:23 HOL-Proofs: theory Fun

01:48:23 HOL-Proofs: theory Typedef

01:48:23 HOL-Proofs: theory Rings

01:48:25 HOL-Proofs: theory Complete_Lattices

01:48:30 HOL-Proofs: theory Inductive

01:48:32 HOL-Proofs: theory Product_Type

01:48:32 HOL-Proofs: theory Sum_Type

01:48:35 HOL-Proofs: theory Complete_Partial_Order

01:48:39 HOL-Proofs: theory Nat

01:48:44 HOL-Proofs: theory Fields

01:48:44 HOL-Proofs: theory Meson

01:48:44 HOL-Proofs: theory ATP

01:48:47 HOL-Proofs: theory Metis

01:48:53 HOL-Proofs: theory Finite_Set

01:49:01 HOL-Proofs: theory Relation

01:49:04 HOL-Proofs: theory Transitive_Closure

01:49:08 HOL-Proofs: theory Wellfounded

01:49:11 HOL-Proofs: theory Fun_Def_Base

01:49:11 HOL-Proofs: theory Hilbert_Choice

01:49:11 HOL-Proofs: theory Wfrec

01:49:11 HOL-Proofs: theory Order_Relation

01:49:12 HOL-Proofs: theory BNF_Wellorder_Relation

01:49:13 HOL-Proofs: theory Zorn

01:49:13 HOL-Proofs: theory BNF_Wellorder_Embedding

01:49:15 HOL-Proofs: theory BNF_Wellorder_Constructions

01:49:21 HOL-Proofs: theory BNF_Cardinal_Order_Relation

01:49:27 HOL-Proofs: theory BNF_Cardinal_Arithmetic

01:49:28 HOL-Proofs: theory BNF_Def

01:49:33 HOL-Proofs: theory BNF_Composition

01:49:33 HOL-Proofs: theory Basic_BNFs

01:49:34 HOL-Proofs: theory BNF_Fixpoint_Base

01:49:37 HOL-Proofs: theory BNF_Least_Fixpoint

01:49:40 HOL-Proofs: theory Basic_BNF_LFPs

01:49:41 HOL-Proofs: theory Transfer

01:49:43 HOL-Proofs: theory Num

01:49:48 HOL-Proofs: theory Power

01:49:51 HOL-Proofs: theory Groups_Big

01:49:59 HOL-Proofs: theory Equiv_Relations

01:50:01 HOL-Proofs: theory Lifting

01:50:05 HOL-Proofs: theory Lifting_Set

01:50:05 HOL-Proofs: theory Option

01:50:05 HOL-Proofs: theory Quotient

01:50:07 HOL-Proofs: theory Extraction

01:50:07 HOL-Proofs: theory Partial_Function

01:50:07 HOL-Proofs: theory Lattices_Big

01:50:12 HOL-Proofs: theory Fun_Def

01:50:14 HOL-Proofs: theory Int

01:50:20 HOL-Proofs: theory Nat_Transfer

01:50:22 HOL-Proofs: theory Euclidean_Division

01:50:28 HOL-Proofs: theory Parity

01:50:31 HOL-Proofs: theory Divides

01:50:53 HOL-Proofs: theory Code_Numeral

01:50:53 HOL-Proofs: theory SMT

01:50:53 HOL-Proofs: theory Numeral_Simprocs

01:50:53 HOL-Proofs: theory Set_Interval

01:50:55 HOL-Proofs: theory Semiring_Normalization

01:50:58 HOL-Proofs: theory Groebner_Basis

01:51:08 HOL-Proofs: theory Conditionally_Complete_Lattices

01:51:08 HOL-Proofs: theory Filter

01:51:08 HOL-Proofs: theory Presburger

01:51:20 HOL-Proofs: theory Sledgehammer

01:51:22 HOL-Proofs: theory List

01:52:17 HOL-Proofs: theory Groups_List

01:52:17 HOL-Proofs: theory Map

01:52:19 HOL-Proofs: theory Random

01:52:21 HOL-Proofs: theory Enum

01:53:05 HOL-Proofs: theory String

01:53:08 HOL-Proofs: theory BNF_Greatest_Fixpoint

01:53:09 HOL-Proofs: theory Predicate

01:53:13 HOL-Proofs: theory Lazy_Sequence

01:53:14 HOL-Proofs: theory Limited_Sequence

01:53:15 HOL-Proofs: theory Typerep

01:53:16 HOL-Proofs: theory Code_Evaluation

01:53:18 HOL-Proofs: theory Quickcheck_Random

01:53:21 HOL-Proofs: theory Quickcheck_Exhaustive

01:53:21 HOL-Proofs: theory Quickcheck_Narrowing

01:53:21 HOL-Proofs: theory Random_Pred

01:53:22 HOL-Proofs: theory Random_Sequence

01:53:27 HOL-Proofs: theory Record

01:53:27 HOL-Proofs: theory Predicate_Compile

01:53:30 HOL-Proofs: theory Nitpick

01:53:37 HOL-Proofs: theory Main

01:53:39 HOL-Proofs: theory Old_Datatype

01:55:56 Timing HOL-Proofs (6 threads, 380.188s elapsed time, 1096.784s cpu time, 115.072s GC time, factor 2.88)

01:55:56 Finished HOL-Proofs (0:07:58 elapsed time, 0:22:31 cpu time, factor 2.83)

01:55:58 Building HOL-Analysis ...

01:56:01 HOL-Analysis: theory Cancellation

01:56:01 HOL-Analysis: theory Disjoint_Sets

01:56:01 HOL-Analysis: theory FuncSet

01:56:01 HOL-Analysis: theory Infinite_Set

01:56:01 HOL-Analysis: theory Nat_Bijection

01:56:01 HOL-Analysis: theory Old_Datatype

01:56:02 HOL-Analysis: theory Phantom_Type

01:56:02 HOL-Analysis: theory Product_Plus

01:56:02 HOL-Analysis: theory Set_Algebras

01:56:02 HOL-Analysis: theory Product_Order

01:56:02 HOL-Analysis: theory Multiset

01:56:02 HOL-Analysis: theory L2_Norm

01:56:02 HOL-Analysis: theory Discrete

01:56:02 HOL-Analysis: theory Indicator_Function

01:56:02 HOL-Analysis: theory Inner_Product

01:56:03 HOL-Analysis: theory Cardinality

01:56:03 HOL-Analysis: theory Liminf_Limsup

01:56:03 HOL-Analysis: theory Countable

01:56:03 HOL-Analysis: theory Nonpos_Ints

01:56:03 HOL-Analysis: theory Operator_Norm

01:56:03 HOL-Analysis: theory Periodic_Fun

01:56:03 HOL-Analysis: theory Poly_Roots

01:56:04 HOL-Analysis: theory Numeral_Type

01:56:04 HOL-Analysis: theory Product_Vector

01:56:04 HOL-Analysis: theory Sum_of_Squares

01:56:04 HOL-Analysis: theory Euclidean_Space

01:56:04 HOL-Analysis: theory Countable_Set

01:56:05 HOL-Analysis: theory Countable_Complete_Lattices

01:56:05 HOL-Analysis: theory Continuum_Not_Denumerable

01:56:06 HOL-Analysis: theory Finite_Cartesian_Product

01:56:06 HOL-Analysis: theory Linear_Algebra

01:56:07 HOL-Analysis: theory Permutations

01:56:07 HOL-Analysis: theory Factorial_Ring

01:56:07 HOL-Analysis: theory Norm_Arith

01:56:08 HOL-Analysis: theory Order_Continuity

01:56:09 HOL-Analysis: theory Extended_Nat

01:56:09 HOL-Analysis: theory Topology_Euclidean_Space

01:56:10 HOL-Analysis: theory Extended_Real

01:56:14 HOL-Analysis: theory Extended_Nonnegative_Real

01:56:14 HOL-Analysis: theory Summation_Tests

01:56:15 HOL-Analysis: theory Euclidean_Algorithm

01:56:17 HOL-Analysis: theory Sigma_Algebra

01:56:20 HOL-Analysis: theory Bounded_Linear_Function

01:56:20 HOL-Analysis: theory Convex_Euclidean_Space

01:56:20 HOL-Analysis: theory Extended_Real_Limits

01:56:21 HOL-Analysis: theory Measurable

01:56:21 HOL-Analysis: theory Tagged_Division

01:56:22 HOL-Analysis: theory Measure_Space

01:56:22 HOL-Analysis: theory Uniform_Limit

01:56:24 HOL-Analysis: theory Primes

01:56:25 HOL-Analysis: theory Caratheodory

01:56:27 HOL-Analysis: theory Continuous_Extension

01:56:27 HOL-Analysis: theory Path_Connected

01:56:32 HOL-Analysis: theory Homeomorphism

01:56:33 HOL-Analysis: theory Brouwer_Fixpoint

01:56:35 HOL-Analysis: theory Derivative

01:56:38 HOL-Analysis: theory Cartesian_Euclidean_Space

01:56:38 HOL-Analysis: theory Weierstrass_Theorems

01:56:41 HOL-Analysis: theory Determinants

01:56:41 HOL-Analysis: theory Fashoda_Theorem

01:56:41 HOL-Analysis: theory Ordered_Euclidean_Space

01:56:41 HOL-Analysis: theory Polytope

01:56:47 HOL-Analysis: theory Arcwise_Connected

01:56:47 HOL-Analysis: theory Borel_Space

01:56:50 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

01:56:50 HOL-Analysis: theory Regularity

01:56:52 HOL-Analysis: theory Binary_Product_Measure

01:56:53 HOL-Analysis: theory Embed_Measure

01:56:53 HOL-Analysis: theory Finite_Product_Measure

01:56:55 HOL-Analysis: theory Bochner_Integration

01:56:55 HOL-Analysis: theory Function_Topology

01:56:57 HOL-Analysis: theory Complete_Measure

01:56:57 HOL-Analysis: theory Radon_Nikodym

01:56:58 HOL-Analysis: theory Set_Integral

01:56:58 HOL-Analysis: theory Lebesgue_Measure

01:57:00 HOL-Analysis: theory Henstock_Kurzweil_Integration

01:57:03 HOL-Analysis: theory Bounded_Continuous_Function

01:57:03 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

01:57:03 HOL-Analysis: theory Integral_Test

01:57:05 HOL-Analysis: theory Complex_Analysis_Basics

01:57:05 HOL-Analysis: theory Interval_Integral

01:57:06 HOL-Analysis: theory Lebesgue_Integral_Substitution

01:57:06 HOL-Analysis: theory Complex_Transcendental

01:57:09 HOL-Analysis: theory Generalised_Binomial_Theorem

01:57:09 HOL-Analysis: theory Harmonic_Numbers

01:57:09 HOL-Analysis: theory Cauchy_Integral_Theorem

01:57:09 HOL-Analysis: theory Further_Topology

01:57:12 HOL-Analysis: theory Jordan_Curve

01:57:13 HOL-Analysis: theory Conformal_Mappings

01:57:13 HOL-Analysis: theory Gamma_Function

01:57:13 HOL-Analysis: theory Winding_Numbers

01:57:15 HOL-Analysis: theory Great_Picard

01:57:17 HOL-Analysis: theory Analysis

02:02:22 Timing HOL-Analysis (6 threads, 348.568s elapsed time, 1416.556s cpu time, 85.668s GC time, factor 4.06)

02:02:22 Finished HOL-Analysis (0:06:23 elapsed time, 0:25:02 cpu time, factor 3.91)

02:02:23 Building HOL-Auth ...

02:02:25 HOL-Auth: theory Message

02:02:25 HOL-Auth: theory Nat_Bijection

02:02:25 HOL-Auth: theory Simps_Case_Conv

02:02:29 HOL-Auth: theory All_Symmetric

02:02:29 HOL-Auth: theory Event

02:02:29 HOL-Auth: theory EventSC

02:02:30 HOL-Auth: theory Extensions

02:02:30 HOL-Auth: theory Public

02:02:30 HOL-Auth: theory Shared

02:02:31 HOL-Auth: theory Analz

02:02:31 HOL-Auth: theory List_Msg

02:02:31 HOL-Auth: theory CertifiedEmail

02:02:31 HOL-Auth: theory KerberosIV

02:02:31 HOL-Auth: theory KerberosIV_Gets

02:02:31 HOL-Auth: theory KerberosV

02:02:31 HOL-Auth: theory Guard

02:02:32 HOL-Auth: theory GuardK

02:02:32 HOL-Auth: theory Guard_Public

02:02:32 HOL-Auth: theory Guard_NS_Public

02:02:32 HOL-Auth: theory Proto

02:02:32 HOL-Auth: theory Kerberos_BAN

02:02:33 HOL-Auth: theory P2

02:02:33 HOL-Auth: theory Kerberos_BAN_Gets

02:02:33 HOL-Auth: theory NS_Public

02:02:33 HOL-Auth: theory NS_Public_Bad

02:02:33 HOL-Auth: theory NS_Shared

02:02:33 HOL-Auth: theory OtwayRees

02:02:33 HOL-Auth: theory OtwayReesBella

02:02:33 HOL-Auth: theory OtwayRees_AN

02:02:33 HOL-Auth: theory OtwayRees_Bad

02:02:34 HOL-Auth: theory P1

02:02:34 HOL-Auth: theory Recur

02:02:34 HOL-Auth: theory WooLam

02:02:34 HOL-Auth: theory Yahalom

02:02:34 HOL-Auth: theory Yahalom2

02:02:35 HOL-Auth: theory Yahalom_Bad

02:02:35 HOL-Auth: theory ZhouGollmann

02:02:35 HOL-Auth: theory Guard_Shared

02:02:35 HOL-Auth: theory TLS

02:02:35 HOL-Auth: theory Smartcard

02:02:35 HOL-Auth: theory Guard_OtwayRees

02:02:36 HOL-Auth: theory Guard_Yahalom

02:02:36 HOL-Auth: theory Auth_Shared

02:02:36 HOL-Auth: theory ShoupRubin

02:02:36 HOL-Auth: theory ShoupRubinBella

02:02:36 HOL-Auth: theory Auth_Guard_Shared

02:02:37 HOL-Auth: theory Auth_Public

02:02:38 HOL-Auth: theory Auth_Smartcard

02:02:39 HOL-Auth: theory Auth_Guard_Public

02:03:48 Timing HOL-Auth (6 threads, 63.612s elapsed time, 300.704s cpu time, 9.016s GC time, factor 4.73)

02:03:48 Finished HOL-Auth (0:01:24 elapsed time, 0:05:50 cpu time, factor 4.17)

02:03:48 Building HOL-Nominal ...

02:03:50 HOL-Nominal: theory Infinite_Set

02:03:50 HOL-Nominal: theory Old_Datatype

02:03:52 HOL-Nominal: theory Nominal

02:04:06 Timing HOL-Nominal (6 threads, 7.010s elapsed time, 17.540s cpu time, 0.724s GC time, factor 2.50)

02:04:06 Finished HOL-Nominal (0:00:17 elapsed time, 0:00:41 cpu time, factor 2.32)

02:04:06 Building HOL-Nonstandard_Analysis ...

02:04:08 HOL-Nonstandard_Analysis: theory Lub_Glb

02:04:08 HOL-Nonstandard_Analysis: theory Infinite_Set

02:04:09 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

02:04:09 HOL-Nonstandard_Analysis: theory StarDef

02:04:10 HOL-Nonstandard_Analysis: theory HyperNat

02:04:11 HOL-Nonstandard_Analysis: theory HyperDef

02:04:12 HOL-Nonstandard_Analysis: theory NSA

02:04:14 HOL-Nonstandard_Analysis: theory NSComplex

02:04:14 HOL-Nonstandard_Analysis: theory Star

02:04:15 HOL-Nonstandard_Analysis: theory HLim

02:04:15 HOL-Nonstandard_Analysis: theory NatStar

02:04:15 HOL-Nonstandard_Analysis: theory HDeriv

02:04:15 HOL-Nonstandard_Analysis: theory HSEQ

02:04:16 HOL-Nonstandard_Analysis: theory HSeries

02:04:17 HOL-Nonstandard_Analysis: theory HTranscendental

02:04:17 HOL-Nonstandard_Analysis: theory HLog

02:04:17 HOL-Nonstandard_Analysis: theory NSCA

02:04:18 HOL-Nonstandard_Analysis: theory Hyperreal

02:04:18 HOL-Nonstandard_Analysis: theory CStar

02:04:19 HOL-Nonstandard_Analysis: theory CLim

02:04:19 HOL-Nonstandard_Analysis: theory Hypercomplex

02:04:20 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

02:04:29 Timing HOL-Nonstandard_Analysis (6 threads, 12.081s elapsed time, 34.060s cpu time, 1.096s GC time, factor 2.82)

02:04:29 Finished HOL-Nonstandard_Analysis (0:00:22 elapsed time, 0:00:57 cpu time, factor 2.54)

02:04:29 Building HOL-Probability ...

02:04:34 HOL-Probability: theory Permutation

02:04:34 HOL-Probability: theory AList

02:04:34 HOL-Probability: theory FSet

02:04:34 HOL-Probability: theory Diagonal_Subsequence

02:04:37 HOL-Probability: theory Finite_Map

02:04:40 HOL-Probability: theory Lattice_Syntax

02:04:40 HOL-Probability: theory Adhoc_Overloading

02:04:40 HOL-Probability: theory Mapping

02:04:40 HOL-Probability: theory Stream

02:04:40 HOL-Probability: theory Rewrite

02:04:40 HOL-Probability: theory Sublist

02:04:40 HOL-Probability: theory Complete_Partial_Order2

02:04:40 HOL-Probability: theory Monad_Syntax

02:04:41 HOL-Probability: theory Multiset_Permutations

02:04:41 HOL-Probability: theory Fin_Map

02:04:41 HOL-Probability: theory Discrete_Topology

02:04:41 HOL-Probability: theory AList_Mapping

02:04:42 HOL-Probability: theory Essential_Supremum

02:04:42 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

02:04:42 HOL-Probability: theory Probability_Measure

02:04:42 HOL-Probability: theory Stopping_Time

02:04:44 HOL-Probability: theory Conditional_Expectation

02:04:44 HOL-Probability: theory Distribution_Functions

02:04:44 HOL-Probability: theory Giry_Monad

02:04:44 HOL-Probability: theory Weak_Convergence

02:04:45 HOL-Probability: theory Helly_Selection

02:04:46 HOL-Probability: theory Probability_Mass_Function

02:04:46 HOL-Probability: theory Projective_Family

02:04:47 HOL-Probability: theory Infinite_Product_Measure

02:04:48 HOL-Probability: theory Independent_Family

02:04:48 HOL-Probability: theory PMF_Impl

02:04:48 HOL-Probability: theory Random_Permutations

02:04:48 HOL-Probability: theory SPMF

02:04:48 HOL-Probability: theory Projective_Limit

02:04:49 HOL-Probability: theory Stream_Space

02:04:49 HOL-Probability: theory Convolution

02:04:49 HOL-Probability: theory Information

02:04:52 HOL-Probability: theory Distributions

02:04:53 HOL-Probability: theory Characteristic_Functions

02:04:53 HOL-Probability: theory Sinc_Integral

02:04:54 HOL-Probability: theory Levy

02:04:55 HOL-Probability: theory Central_Limit_Theorem

02:04:56 HOL-Probability: theory Probability

02:05:58 Timing HOL-Probability (6 threads, 63.295s elapsed time, 285.620s cpu time, 8.752s GC time, factor 4.51)

02:05:58 Finished HOL-Probability (0:01:28 elapsed time, 0:05:41 cpu time, factor 3.86)

02:05:58 Building HOL-Word ...

02:06:00 HOL-Word: theory Bit

02:06:00 HOL-Word: theory Misc_Numeric

02:06:00 HOL-Word: theory Boolean_Algebra

02:06:00 HOL-Word: theory Bits

02:06:00 HOL-Word: theory Misc_Typedef

02:06:00 HOL-Word: theory Phantom_Type

02:06:00 HOL-Word: theory Bit_Representation

02:06:01 HOL-Word: theory Bits_Bit

02:06:01 HOL-Word: theory Word_Miscellaneous

02:06:01 HOL-Word: theory Bits_Int

02:06:01 HOL-Word: theory Cardinality

02:06:02 HOL-Word: theory Numeral_Type

02:06:03 HOL-Word: theory Bool_List_Representation

02:06:03 HOL-Word: theory Type_Length

02:06:03 HOL-Word: theory Word

02:06:19 Timing HOL-Word (6 threads, 9.365s elapsed time, 39.920s cpu time, 1.260s GC time, factor 4.26)

02:06:19 Finished HOL-Word (0:00:20 elapsed time, 0:01:05 cpu time, factor 3.14)

02:06:19 Building HOLCF ...

02:06:21 HOLCF: theory Nat_Bijection

02:06:21 HOLCF: theory Old_Datatype

02:06:23 HOLCF: theory Countable

02:06:24 HOLCF: theory Porder

02:06:25 HOLCF: theory Pcpo

02:06:26 HOLCF: theory Cont

02:06:27 HOLCF: theory Adm

02:06:27 HOLCF: theory Discrete

02:06:27 HOLCF: theory Cpodef

02:06:27 HOLCF: theory Fun_Cpo

02:06:27 HOLCF: theory Product_Cpo

02:06:27 HOLCF: theory Cfun

02:06:28 HOLCF: theory Fix

02:06:28 HOLCF: theory Cprod

02:06:28 HOLCF: theory Sfun

02:06:28 HOLCF: theory Sprod

02:06:28 HOLCF: theory Up

02:06:29 HOLCF: theory Lift

02:06:29 HOLCF: theory One

02:06:29 HOLCF: theory Tr

02:06:30 HOLCF: theory Ssum

02:06:30 HOLCF: theory Plain_HOLCF

02:06:31 HOLCF: theory Completion

02:06:31 HOLCF: theory Deflation

02:06:31 HOLCF: theory Fixrec

02:06:31 HOLCF: theory Map_Functions

02:06:32 HOLCF: theory Bifinite

02:06:32 HOLCF: theory Domain_Aux

02:06:33 HOLCF: theory Universal

02:06:34 HOLCF: theory Algebraic

02:06:34 HOLCF: theory Compact_Basis

02:06:34 HOLCF: theory LowerPD

02:06:34 HOLCF: theory UpperPD

02:06:35 HOLCF: theory Representable

02:06:35 HOLCF: theory ConvexPD

02:06:37 HOLCF: theory Domain

02:06:39 HOLCF: theory Powerdomains

02:06:40 HOLCF: theory HOLCF

02:06:53 Timing HOLCF (6 threads, 18.436s elapsed time, 40.260s cpu time, 2.028s GC time, factor 2.18)

02:06:53 Finished HOLCF (0:00:32 elapsed time, 0:01:11 cpu time, factor 2.19)

02:06:53 Building ZF ...

02:06:53 ZF: theory IFOL

02:06:54 ZF: theory FOL

02:06:55 ZF: theory ZF

02:06:56 ZF: theory upair

02:06:56 ZF: theory pair

02:06:56 ZF: theory Bool

02:06:56 ZF: theory equalities

02:06:57 ZF: theory Fixedpt

02:06:57 ZF: theory Sum

02:06:57 ZF: theory func

02:06:57 ZF: theory Perm

02:06:57 ZF: theory QPair

02:06:58 ZF: theory Trancl

02:06:58 ZF: theory EquivClass

02:06:58 ZF: theory WF

02:06:58 ZF: theory Order

02:06:58 ZF: theory Ordinal

02:06:58 ZF: theory OrdQuant

02:06:58 ZF: theory OrderArith

02:06:59 ZF: theory Nat_ZF

02:06:59 ZF: theory Epsilon

02:06:59 ZF: theory OrderType

02:06:59 ZF: theory Inductive_ZF

02:06:59 ZF: theory Finite

02:06:59 ZF: theory Cardinal

02:07:00 ZF: theory Univ

02:07:00 ZF: theory QUniv

02:07:00 ZF: theory Arith

02:07:00 ZF: theory Datatype_ZF

02:07:00 ZF: theory ArithSimp

02:07:01 ZF: theory Int_ZF

02:07:01 ZF: theory List_ZF

02:07:01 ZF: theory CardinalArith

02:07:01 ZF: theory Bin

02:07:02 ZF: theory IntDiv_ZF

02:07:02 ZF: theory Main_ZF

02:07:03 ZF: theory AC

02:07:03 ZF: theory Main

02:07:03 ZF: theory Zorn

02:07:03 ZF: theory Cardinal_AC

02:07:03 ZF: theory InfDatatype

02:07:03 ZF: theory Main_ZFC

02:07:06 Timing ZF (6 threads, 10.390s elapsed time, 35.256s cpu time, 2.128s GC time, factor 3.39)

02:07:06 Finished ZF (0:00:13 elapsed time, 0:00:41 cpu time, factor 3.17)

02:07:06 Running HOL-Algebra ...

02:07:08 HOL-Algebra: theory Cancellation

02:07:08 HOL-Algebra: theory FuncSet

02:07:09 HOL-Algebra: theory Multiset

02:07:13 HOL-Algebra: theory Permutation

02:07:13 HOL-Algebra: theory Factorial_Ring

02:07:20 HOL-Algebra: theory Euclidean_Algorithm

02:07:26 HOL-Algebra: theory Primes

02:07:29 HOL-Algebra: theory Congruence

02:07:29 HOL-Algebra: theory Exponent

02:07:30 HOL-Algebra: theory Lattice

02:07:32 HOL-Algebra: theory Group

02:07:33 HOL-Algebra: theory Bij

02:07:33 HOL-Algebra: theory Coset

02:07:33 HOL-Algebra: theory FiniteProduct

02:07:33 HOL-Algebra: theory Ring

02:07:34 HOL-Algebra: theory Divisibility

02:07:34 HOL-Algebra: theory Sylow

02:07:37 HOL-Algebra: theory AbelCoset

02:07:37 HOL-Algebra: theory Module

02:07:43 HOL-Algebra: theory Ideal

02:07:46 HOL-Algebra: theory RingHom

02:07:48 HOL-Algebra: theory QuotRing

02:07:48 HOL-Algebra: theory UnivPoly

02:07:49 HOL-Algebra: theory IntRing

02:08:03 Timing HOL-Algebra (6 threads, 53.838s elapsed time, 153.624s cpu time, 8.668s GC time, factor 2.85)

02:08:03 Finished HOL-Algebra (0:00:55 elapsed time, 0:02:35 cpu time, factor 2.79)

02:08:03 Running HOL-Bali ...

02:08:04 HOL-Bali: theory Old_Recdef

02:08:05 HOL-Bali: theory Basis

02:08:07 HOL-Bali: theory Name

02:08:07 HOL-Bali: theory Table

02:08:09 HOL-Bali: theory Type

02:08:10 HOL-Bali: theory Value

02:08:11 HOL-Bali: theory Term

02:08:28 HOL-Bali: theory Decl

02:08:32 HOL-Bali: theory TypeRel

02:08:33 HOL-Bali: theory DeclConcepts

02:08:35 HOL-Bali: theory State

02:08:35 HOL-Bali: theory WellType

02:08:36 HOL-Bali: theory Conform

02:08:36 HOL-Bali: theory Eval

02:08:37 HOL-Bali: theory DefiniteAssignment

02:08:41 HOL-Bali: theory WellForm

02:08:42 HOL-Bali: theory DefiniteAssignmentCorrect

02:08:42 HOL-Bali: theory Example

02:08:43 HOL-Bali: theory TypeSafe

02:08:45 HOL-Bali: theory Evaln

02:08:47 HOL-Bali: theory AxSem

02:08:47 HOL-Bali: theory Trans

02:08:50 HOL-Bali: theory AxCompl

02:08:51 HOL-Bali: theory AxSound

02:08:51 HOL-Bali: theory AxExample

02:09:04 Timing HOL-Bali (6 threads, 59.435s elapsed time, 202.760s cpu time, 8.844s GC time, factor 3.41)

02:09:04 Finished HOL-Bali (0:01:01 elapsed time, 0:03:24 cpu time, factor 3.34)

02:09:04 Running HOL-Cardinals ...

02:09:06 HOL-Cardinals: theory Order_Union

02:09:06 HOL-Cardinals: theory Fun_More

02:09:06 HOL-Cardinals: theory Order_Relation_More

02:09:06 HOL-Cardinals: theory Cardinal_Notations

02:09:06 HOL-Cardinals: theory Wellorder_Extension

02:09:06 HOL-Cardinals: theory Wellfounded_More

02:09:06 HOL-Cardinals: theory Wellorder_Relation

02:09:06 HOL-Cardinals: theory Wellorder_Embedding

02:09:07 HOL-Cardinals: theory Wellorder_Constructions

02:09:08 HOL-Cardinals: theory Cardinal_Order_Relation

02:09:08 HOL-Cardinals: theory Ordinal_Arithmetic

02:09:09 HOL-Cardinals: theory Cardinal_Arithmetic

02:09:09 HOL-Cardinals: theory Cardinals

02:09:09 HOL-Cardinals: theory Bounded_Set

02:09:13 Timing HOL-Cardinals (6 threads, 6.599s elapsed time, 34.948s cpu time, 1.120s GC time, factor 5.30)

02:09:13 Finished HOL-Cardinals (0:00:08 elapsed time, 0:00:36 cpu time, factor 4.35)

02:09:13 Running HOL-Corec_Examples ...

02:09:14 HOL-Corec_Examples: theory BNF_Axiomatization

02:09:14 HOL-Corec_Examples: theory BNF_Corec

02:09:14 HOL-Corec_Examples: theory FSet

02:09:14 HOL-Corec_Examples: theory Nat_Bijection

02:09:15 HOL-Corec_Examples: theory Stream

02:09:19 HOL-Corec_Examples: theory Iterate_GPV

02:09:19 HOL-Corec_Examples: theory LFilter

02:09:19 HOL-Corec_Examples: theory Simple_Nesting

02:09:19 HOL-Corec_Examples: theory Stream_Processor

02:09:19 HOL-Corec_Examples: theory Paper_Examples

02:10:00 HOL-Corec_Examples: theory GPV_Bare_Bones

02:10:00 HOL-Corec_Examples: theory Merge_A

02:10:00 HOL-Corec_Examples: theory Misc_Mono

02:10:00 HOL-Corec_Examples: theory Merge_Poly

02:10:00 HOL-Corec_Examples: theory Misc_Poly

02:10:00 HOL-Corec_Examples: theory Small_Concrete

02:10:03 HOL-Corec_Examples: theory Merge_B

02:10:06 HOL-Corec_Examples: theory Merge_C

02:10:09 HOL-Corec_Examples: theory Stream_Friends

02:10:11 HOL-Corec_Examples: theory Merge_D

02:10:21 HOL-Corec_Examples: theory TLList_Friends

02:10:22 HOL-Corec_Examples: theory Type_Class

02:11:58 Timing HOL-Corec_Examples (6 threads, 162.653s elapsed time, 489.060s cpu time, 62.252s GC time, factor 3.01)

02:11:58 Finished HOL-Corec_Examples (0:02:44 elapsed time, 0:08:11 cpu time, factor 2.98)

02:11:58 Running HOL-Data_Structures ...

02:11:59 HOL-Data_Structures: theory Less_False

02:11:59 HOL-Data_Structures: theory Cancellation

02:11:59 HOL-Data_Structures: theory Fib

02:12:00 HOL-Data_Structures: theory Multiset

02:12:05 HOL-Data_Structures: theory Sorted_Less

02:12:05 HOL-Data_Structures: theory Cmp

02:12:05 HOL-Data_Structures: theory Tree

02:12:05 HOL-Data_Structures: theory Tree2

02:12:05 HOL-Data_Structures: theory Tree23

02:12:05 HOL-Data_Structures: theory Tree234

02:12:05 HOL-Data_Structures: theory AList_Upd_Del

02:12:05 HOL-Data_Structures: theory List_Ins_Del

02:12:05 HOL-Data_Structures: theory Map_by_Ordered

02:12:06 HOL-Data_Structures: theory Set_by_Ordered

02:12:06 HOL-Data_Structures: theory Brother12_Set

02:12:06 HOL-Data_Structures: theory Isin2

02:12:06 HOL-Data_Structures: theory Leftist_Heap

02:12:06 HOL-Data_Structures: theory Lookup2

02:12:06 HOL-Data_Structures: theory AA_Set

02:12:06 HOL-Data_Structures: theory AVL_Set

02:12:07 HOL-Data_Structures: theory RBT

02:12:08 HOL-Data_Structures: theory AA_Map

02:12:08 HOL-Data_Structures: theory Balance

02:12:08 HOL-Data_Structures: theory Splay_Set

02:12:08 HOL-Data_Structures: theory Tree_Set

02:12:08 HOL-Data_Structures: theory AVL_Map

02:12:09 HOL-Data_Structures: theory Tree23_Set

02:12:09 HOL-Data_Structures: theory Tree234_Set

02:12:09 HOL-Data_Structures: theory Tree_Map

02:12:09 HOL-Data_Structures: theory Splay_Map

02:12:10 HOL-Data_Structures: theory RBT_Set

02:12:13 HOL-Data_Structures: theory RBT_Map

02:12:15 HOL-Data_Structures: theory Tree23_Map

02:12:31 HOL-Data_Structures: theory Tree234_Map

02:13:14 HOL-Data_Structures: theory Brother12_Map

02:15:48 Timing HOL-Data_Structures (6 threads, 228.186s elapsed time, 915.512s cpu time, 56.760s GC time, factor 4.01)

02:15:48 Finished HOL-Data_Structures (0:03:50 elapsed time, 0:15:17 cpu time, factor 3.99)

02:15:48 Running HOL-Datatype_Benchmark ...

02:15:50 HOL-Datatype_Benchmark: theory BNF_Axiomatization

02:15:50 HOL-Datatype_Benchmark: theory Brackin

02:15:50 HOL-Datatype_Benchmark: theory IsaFoR

02:15:50 HOL-Datatype_Benchmark: theory Misc_N2M

02:22:47 Timing HOL-Datatype_Benchmark (6 threads, 416.324s elapsed time, 1580.156s cpu time, 411.184s GC time, factor 3.80)

02:22:47 Finished HOL-Datatype_Benchmark (0:06:58 elapsed time, 0:26:22 cpu time, factor 3.78)

02:22:47 Running HOL-Datatype_Examples ...

02:22:49 HOL-Datatype_Examples: theory BNF_Axiomatization

02:22:49 HOL-Datatype_Examples: theory Lift_BNF

02:22:49 HOL-Datatype_Examples: theory FSet

02:22:49 HOL-Datatype_Examples: theory Milner_Tofte

02:22:49 HOL-Datatype_Examples: theory Nat_Bijection

02:22:49 HOL-Datatype_Examples: theory Infinite_Set

02:22:49 HOL-Datatype_Examples: theory Old_Datatype

02:22:49 HOL-Datatype_Examples: theory TreeFI

02:22:49 HOL-Datatype_Examples: theory Stream

02:22:50 HOL-Datatype_Examples: theory Compat

02:22:50 HOL-Datatype_Examples: theory Countable

02:22:51 HOL-Datatype_Examples: theory Process

02:22:51 HOL-Datatype_Examples: theory Stream_Processor

02:22:51 HOL-Datatype_Examples: theory Koenig

02:22:52 HOL-Datatype_Examples: theory Lambda_Term

02:22:53 HOL-Datatype_Examples: theory Misc_Codatatype

02:22:53 HOL-Datatype_Examples: theory Prelim

02:22:53 HOL-Datatype_Examples: theory DTree

02:22:54 HOL-Datatype_Examples: theory TreeFsetI

02:22:54 HOL-Datatype_Examples: theory Parallel

02:22:54 HOL-Datatype_Examples: theory Gram_Lang

02:22:56 HOL-Datatype_Examples: theory Misc_Datatype

02:23:54 HOL-Datatype_Examples: theory Misc_Primcorec

02:24:11 HOL-Datatype_Examples: theory Misc_Primrec

02:24:14 Timing HOL-Datatype_Examples (6 threads, 84.801s elapsed time, 314.412s cpu time, 27.948s GC time, factor 3.71)

02:24:14 Finished HOL-Datatype_Examples (0:01:26 elapsed time, 0:05:32 cpu time, factor 3.83)

02:24:14 Running HOL-Decision_Procs ...

02:24:16 HOL-Decision_Procs: theory Code_Abstract_Nat

02:24:16 HOL-Decision_Procs: theory Congruence

02:24:16 HOL-Decision_Procs: theory Conversions

02:24:16 HOL-Decision_Procs: theory DP_Library

02:24:16 HOL-Decision_Procs: theory Dense_Linear_Order

02:24:16 HOL-Decision_Procs: theory FuncSet

02:24:16 HOL-Decision_Procs: theory Code_Target_Int

02:24:16 HOL-Decision_Procs: theory Code_Target_Nat

02:24:16 HOL-Decision_Procs: theory Old_Recdef

02:24:16 HOL-Decision_Procs: theory Code_Target_Numeral

02:24:16 HOL-Decision_Procs: theory Lattice_Algebras

02:24:16 HOL-Decision_Procs: theory Log_Nat

02:24:17 HOL-Decision_Procs: theory Polynomial_List

02:24:17 HOL-Decision_Procs: theory Rat_Pair

02:24:17 HOL-Decision_Procs: theory Lattice

02:24:17 HOL-Decision_Procs: theory Cooper

02:24:18 HOL-Decision_Procs: theory Dense_Linear_Order_Ex

02:24:18 HOL-Decision_Procs: theory Ferrack

02:24:18 HOL-Decision_Procs: theory MIR

02:24:19 HOL-Decision_Procs: theory Group

02:24:20 HOL-Decision_Procs: theory FiniteProduct

02:24:21 HOL-Decision_Procs: theory Ring

02:24:22 HOL-Decision_Procs: theory Float

02:24:24 HOL-Decision_Procs: theory Algebra_Aux

02:24:24 HOL-Decision_Procs: theory Approximation

02:24:25 HOL-Decision_Procs: theory Commutative_Ring

02:24:27 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial

02:24:34 HOL-Decision_Procs: theory Commutative_Ring_Complete

02:24:35 HOL-Decision_Procs: theory Reflective_Field

02:24:37 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff

02:24:47 HOL-Decision_Procs: theory Commutative_Ring_Ex

02:25:15 HOL-Decision_Procs: theory Approximation_Ex

02:25:15 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex

02:25:38 HOL-Decision_Procs: theory Decision_Procs

02:27:47 Timing HOL-Decision_Procs (6 threads, 210.747s elapsed time, 855.104s cpu time, 75.536s GC time, factor 4.06)

02:27:47 Finished HOL-Decision_Procs (0:03:32 elapsed time, 0:14:17 cpu time, factor 4.03)

02:27:47 Running HOL-Hoare_Parallel ...

02:27:49 HOL-Hoare_Parallel: theory Graph

02:27:49 HOL-Hoare_Parallel: theory OG_Com

02:27:49 HOL-Hoare_Parallel: theory Quote_Antiquote

02:27:49 HOL-Hoare_Parallel: theory RG_Com

02:27:50 HOL-Hoare_Parallel: theory RG_Tran

02:27:51 HOL-Hoare_Parallel: theory OG_Tran

02:27:52 HOL-Hoare_Parallel: theory RG_Hoare

02:27:52 HOL-Hoare_Parallel: theory OG_Hoare

02:27:53 HOL-Hoare_Parallel: theory RG_Syntax

02:27:53 HOL-Hoare_Parallel: theory RG_Examples

02:27:53 HOL-Hoare_Parallel: theory OG_Tactics

02:27:54 HOL-Hoare_Parallel: theory OG_Syntax

02:27:54 HOL-Hoare_Parallel: theory Gar_Coll

02:27:54 HOL-Hoare_Parallel: theory Mul_Gar_Coll

02:27:54 HOL-Hoare_Parallel: theory OG_Examples

02:27:58 HOL-Hoare_Parallel: theory Hoare_Parallel

02:28:52 Timing HOL-Hoare_Parallel (6 threads, 62.817s elapsed time, 318.948s cpu time, 3.800s GC time, factor 5.08)

02:28:52 Finished HOL-Hoare_Parallel (0:01:04 elapsed time, 0:05:20 cpu time, factor 4.96)

02:28:52 Running HOL-IMP ...

02:28:54 HOL-IMP: theory Char_ord

02:28:54 HOL-IMP: theory List_lexord

02:28:54 HOL-IMP: theory Quotient_Syntax

02:28:54 HOL-IMP: theory While_Combinator

02:28:54 HOL-IMP: theory Simps_Case_Conv

02:28:54 HOL-IMP: theory Quotient_Option

02:28:54 HOL-IMP: theory Quotient_Product

02:28:54 HOL-IMP: theory Quotient_Set

02:28:54 HOL-IMP: theory Extended

02:28:54 HOL-IMP: theory Quotient_List

02:28:57 HOL-IMP: theory AExp

02:28:57 HOL-IMP: theory C_like

02:28:57 HOL-IMP: theory Complete_Lattice

02:28:57 HOL-IMP: theory OO

02:28:57 HOL-IMP: theory Star

02:28:57 HOL-IMP: theory Types

02:28:58 HOL-IMP: theory ASM

02:28:58 HOL-IMP: theory BExp

02:29:00 HOL-IMP: theory Com

02:29:00 HOL-IMP: theory Procs

02:29:00 HOL-IMP: theory ACom

02:29:01 HOL-IMP: theory Abs_Int_Tests

02:29:01 HOL-IMP: theory Big_Step

02:29:01 HOL-IMP: theory Vars

02:29:01 HOL-IMP: theory Poly_Types

02:29:01 HOL-IMP: theory Denotational

02:29:01 HOL-IMP: theory Hoare

02:29:01 HOL-IMP: theory Sec_Type_Expr

02:29:01 HOL-IMP: theory Hoare_Examples

02:29:01 HOL-IMP: theory Hoare_Sound_Complete

02:29:01 HOL-IMP: theory Hoare_Total

02:29:02 HOL-IMP: theory Hoare_Total_EX

02:29:02 HOL-IMP: theory VCG

02:29:02 HOL-IMP: theory Sec_Typing

02:29:02 HOL-IMP: theory VCG_Total_EX

02:29:02 HOL-IMP: theory Sec_TypingT

02:29:02 HOL-IMP: theory Sem_Equiv

02:29:02 HOL-IMP: theory Def_Init

02:29:02 HOL-IMP: theory Def_Init_Exp

02:29:02 HOL-IMP: theory Fold

02:29:03 HOL-IMP: theory Def_Init_Big

02:29:03 HOL-IMP: theory Live

02:29:03 HOL-IMP: theory Procs_Dyn_Vars_Dyn

02:29:03 HOL-IMP: theory Procs_Stat_Vars_Dyn

02:29:03 HOL-IMP: theory Procs_Stat_Vars_Stat

02:29:03 HOL-IMP: theory Collecting

02:29:04 HOL-IMP: theory Compiler

02:29:04 HOL-IMP: theory Def_Init_Small

02:29:04 HOL-IMP: theory Small_Step

02:29:04 HOL-IMP: theory Collecting1

02:29:04 HOL-IMP: theory Collecting_Examples

02:29:04 HOL-IMP: theory Abs_Int_init

02:29:04 HOL-IMP: theory Live_True

02:29:05 HOL-IMP: theory Finite_Reachable

02:29:05 HOL-IMP: theory Abs_Int0

02:29:06 HOL-IMP: theory Abs_State

02:29:07 HOL-IMP: theory Compiler2

02:29:07 HOL-IMP: theory Abs_Int1

02:29:08 HOL-IMP: theory Abs_Int1_const

02:29:08 HOL-IMP: theory Abs_Int1_parity

02:29:08 HOL-IMP: theory Abs_Int2

02:29:09 HOL-IMP: theory Abs_Int2_ivl

02:29:11 HOL-IMP: theory Abs_Int3

02:30:05 Timing HOL-IMP (6 threads, 70.919s elapsed time, 292.924s cpu time, 18.204s GC time, factor 4.13)

02:30:05 Finished HOL-IMP (0:01:12 elapsed time, 0:04:55 cpu time, factor 4.06)

02:30:05 Running HOL-Library ...

02:30:08 HOL-Library: theory Lattice_Syntax

02:30:08 HOL-Library: theory Adhoc_Overloading

02:30:08 HOL-Library: theory AList

02:30:08 HOL-Library: theory BNF_Corec

02:30:08 HOL-Library: theory Stirling

02:30:08 HOL-Library: theory BNF_Axiomatization

02:30:08 HOL-Library: theory Bit

02:30:08 HOL-Library: theory Bits

02:30:08 HOL-Library: theory Boolean_Algebra

02:30:08 HOL-Library: theory Cancellation

02:30:08 HOL-Library: theory Cardinal_Notations

02:30:08 HOL-Library: theory Char_ord

02:30:08 HOL-Library: theory Bits_Bit

02:30:08 HOL-Library: theory Code_Abstract_Nat

02:30:08 HOL-Library: theory Code_Char

02:30:08 HOL-Library: theory Code_Binary_Nat

02:30:09 HOL-Library: theory Code_Target_Nat

02:30:09 HOL-Library: theory Multiset

02:30:09 HOL-Library: theory Code_Prolog

02:30:09 HOL-Library: theory Code_Test

02:30:09 HOL-Library: theory Combine_PER

02:30:09 HOL-Library: theory Complete_Partial_Order2

02:30:09 HOL-Library: theory Debug

02:30:09 HOL-Library: theory DAList

02:30:09 HOL-Library: theory Disjoint_Sets

02:30:10 HOL-Library: theory Dlist

02:30:10 HOL-Library: theory FSet

02:30:10 HOL-Library: theory Fraction_Field

02:30:11 HOL-Library: theory Fun_Lexorder

02:30:11 HOL-Library: theory FuncSet

02:30:11 HOL-Library: theory Function_Algebras

02:30:11 HOL-Library: theory Function_Division

02:30:11 HOL-Library: theory Code_Target_Int

02:30:12 HOL-Library: theory Groups_Big_Fun

02:30:12 HOL-Library: theory Code_Target_Numeral

02:30:12 HOL-Library: theory IArray

02:30:12 HOL-Library: theory Infinite_Set

02:30:12 HOL-Library: theory LaTeXsugar

02:30:12 HOL-Library: theory Lattice_Constructions

02:30:12 HOL-Library: theory Omega_Words_Fun

02:30:13 HOL-Library: theory Finite_Map

02:30:13 HOL-Library: theory ListVector

02:30:13 HOL-Library: theory List_lexord

02:30:13 HOL-Library: theory Mapping

02:30:13 HOL-Library: theory DAList_Multiset

02:30:13 HOL-Library: theory Multiset_Order

02:30:13 HOL-Library: theory Permutation

02:30:13 HOL-Library: theory Permutations

02:30:13 HOL-Library: theory Factorial_Ring

02:30:13 HOL-Library: theory Misc_Numeric

02:30:14 HOL-Library: theory Bit_Representation

02:30:14 HOL-Library: theory AList_Mapping

02:30:14 HOL-Library: theory Misc_Typedef

02:30:14 HOL-Library: theory Monad_Syntax

02:30:14 HOL-Library: theory Bits_Int

02:30:14 HOL-Library: theory More_List

02:30:14 HOL-Library: theory Nat_Bijection

02:30:14 HOL-Library: theory Old_Datatype

02:30:15 HOL-Library: theory Old_Recdef

02:30:15 HOL-Library: theory Option_ord

02:30:15 HOL-Library: theory Stream

02:30:15 HOL-Library: theory Parallel

02:30:15 HOL-Library: theory Perm

02:30:15 HOL-Library: theory Countable

02:30:15 HOL-Library: theory Bool_List_Representation

02:30:16 HOL-Library: theory Phantom_Type

02:30:16 HOL-Library: theory Predicate_Compile_Alternative_Defs

02:30:16 HOL-Library: theory Product_Lexorder

02:30:16 HOL-Library: theory Cardinality

02:30:16 HOL-Library: theory Predicate_Compile_Quickcheck

02:30:16 HOL-Library: theory Product_Plus

02:30:17 HOL-Library: theory Quotient_Syntax

02:30:17 HOL-Library: theory Product_Order

02:30:17 HOL-Library: theory Quotient_Type

02:30:17 HOL-Library: theory Quotient_Option

02:30:17 HOL-Library: theory Quotient_Product

02:30:17 HOL-Library: theory Quotient_Set

02:30:17 HOL-Library: theory Countable_Set

02:30:17 HOL-Library: theory Finite_Lattice

02:30:17 HOL-Library: theory Quotient_Sum

02:30:17 HOL-Library: theory Quotient_List

02:30:17 HOL-Library: theory RBT_Impl

02:30:17 HOL-Library: theory Numeral_Type

02:30:17 HOL-Library: theory Ramsey

02:30:17 HOL-Library: theory Countable_Complete_Lattices

02:30:18 HOL-Library: theory Countable_Set_Type

02:30:18 HOL-Library: theory Type_Length

02:30:18 HOL-Library: theory Saturated

02:30:19 HOL-Library: theory Reflection

02:30:19 HOL-Library: theory Refute

02:30:19 HOL-Library: theory Rewrite

02:30:20 HOL-Library: theory Set_Algebras

02:30:20 HOL-Library: theory Simps_Case_Conv

02:30:20 HOL-Library: theory Extended

02:30:20 HOL-Library: theory State_Monad

02:30:20 HOL-Library: theory Sublist

02:30:20 HOL-Library: theory Polynomial

02:30:20 HOL-Library: theory BigO

02:30:21 HOL-Library: theory Euclidean_Algorithm

02:30:21 HOL-Library: theory Prefix_Order

02:30:21 HOL-Library: theory Sublist_Order

02:30:21 HOL-Library: theory Code_Real_Approx_By_Float

02:30:21 HOL-Library: theory Diagonal_Subsequence

02:30:21 HOL-Library: theory Discrete

02:30:21 HOL-Library: theory Indicator_Function

02:30:21 HOL-Library: theory Lattice_Algebras

02:30:22 HOL-Library: theory Liminf_Limsup

02:30:22 HOL-Library: theory Log_Nat

02:30:22 HOL-Library: theory Lub_Glb

02:30:22 HOL-Library: theory Multiset_Permutations

02:30:23 HOL-Library: theory Nonpos_Ints

02:30:23 HOL-Library: theory OptionalSugar

02:30:23 HOL-Library: theory Order_Continuity

02:30:23 HOL-Library: theory Periodic_Fun

02:30:24 HOL-Library: theory Quadratic_Discriminant

02:30:24 HOL-Library: theory Sum_of_Squares

02:30:24 HOL-Library: theory Extended_Nat

02:30:25 HOL-Library: theory Extended_Real

02:30:26 HOL-Library: theory Fundamental_Theorem_Algebra

02:30:26 HOL-Library: theory Linear_Temporal_Logic_on_Streams

02:30:27 HOL-Library: theory Float

02:30:27 HOL-Library: theory Transitive_Closure_Table

02:30:27 HOL-Library: theory Tree

02:30:28 HOL-Library: theory Normalized_Fraction

02:30:28 HOL-Library: theory Field_as_Ring

02:30:28 HOL-Library: theory Formal_Power_Series

02:30:28 HOL-Library: theory Extended_Nonnegative_Real

02:30:29 HOL-Library: theory Polynomial_Factorial

02:30:29 HOL-Library: theory While_Combinator

02:30:30 HOL-Library: theory Bourbaki_Witt_Fixpoint

02:30:30 HOL-Library: theory Word_Miscellaneous

02:30:30 HOL-Library: theory Tree_Multiset

02:30:31 HOL-Library: theory Word

02:30:31 HOL-Library: theory Preorder

02:30:31 HOL-Library: theory Function_Growth

02:30:32 HOL-Library: theory Polynomial_FPS

02:30:32 HOL-Library: theory Library

02:30:35 HOL-Library: theory Old_SMT

02:30:48 HOL-Library: theory RBT

02:30:48 HOL-Library: theory RBT_Mapping

02:30:48 HOL-Library: theory RBT_Set

02:31:45 Timing HOL-Library (6 threads, 97.224s elapsed time, 470.156s cpu time, 45.740s GC time, factor 4.84)

02:31:45 Finished HOL-Library (0:01:39 elapsed time, 0:07:52 cpu time, factor 4.76)

02:31:45 Running HOL-Metis_Examples ...

02:31:47 HOL-Metis_Examples: theory Binary_Tree

02:31:47 HOL-Metis_Examples: theory Function_Algebras

02:31:47 HOL-Metis_Examples: theory Set_Algebras

02:31:47 HOL-Metis_Examples: theory FuncSet

02:31:47 HOL-Metis_Examples: theory Dense_Linear_Order

02:31:47 HOL-Metis_Examples: theory Message

02:31:47 HOL-Metis_Examples: theory Sets

02:31:47 HOL-Metis_Examples: theory Clausification

02:31:47 HOL-Metis_Examples: theory Trans_Closure

02:31:48 HOL-Metis_Examples: theory Abstraction

02:31:48 HOL-Metis_Examples: theory Tarski

02:31:48 HOL-Metis_Examples: theory Type_Encodings

02:31:48 HOL-Metis_Examples: theory Proxies

02:31:49 HOL-Metis_Examples: theory Big_O

02:32:00 Timing HOL-Metis_Examples (6 threads, 12.430s elapsed time, 56.156s cpu time, 2.936s GC time, factor 4.52)

02:32:00 Finished HOL-Metis_Examples (0:00:14 elapsed time, 0:01:09 cpu time, factor 4.90)

02:32:00 Running HOL-MicroJava ...

02:32:01 HOL-MicroJava: theory While_Combinator

02:32:03 HOL-MicroJava: theory Eisbach

02:32:03 HOL-MicroJava: theory Transitive_Closure_Table

02:32:03 HOL-MicroJava: theory Semilat

02:32:03 HOL-MicroJava: theory Err

02:32:03 HOL-MicroJava: theory JBasis

02:32:04 HOL-MicroJava: theory AuxLemmas

02:32:04 HOL-MicroJava: theory Type

02:32:04 HOL-MicroJava: theory Listn

02:32:04 HOL-MicroJava: theory Opt

02:32:05 HOL-MicroJava: theory Product

02:32:05 HOL-MicroJava: theory Typing_Framework

02:32:05 HOL-MicroJava: theory SemilatAlg

02:32:05 HOL-MicroJava: theory Kildall

02:32:05 HOL-MicroJava: theory LBVSpec

02:32:05 HOL-MicroJava: theory Typing_Framework_err

02:32:06 HOL-MicroJava: theory Semilattices

02:32:06 HOL-MicroJava: theory Decl

02:32:06 HOL-MicroJava: theory Value

02:32:06 HOL-MicroJava: theory LBVComplete

02:32:06 HOL-MicroJava: theory LBVCorrect

02:32:06 HOL-MicroJava: theory SystemClasses

02:32:06 HOL-MicroJava: theory TypeRel

02:32:06 HOL-MicroJava: theory Abstract_BV

02:32:06 HOL-MicroJava: theory Term

02:32:06 HOL-MicroJava: theory WellForm

02:32:06 HOL-MicroJava: theory State

02:32:07 HOL-MicroJava: theory Exceptions

02:32:07 HOL-MicroJava: theory JType

02:32:08 HOL-MicroJava: theory JVMType

02:32:09 HOL-MicroJava: theory WellType

02:32:10 HOL-MicroJava: theory Conform

02:32:10 HOL-MicroJava: theory Eval

02:32:10 HOL-MicroJava: theory TypeInf

02:32:11 HOL-MicroJava: theory JVMState

02:32:11 HOL-MicroJava: theory JVMInstructions

02:32:12 HOL-MicroJava: theory JVMExceptions

02:32:12 HOL-MicroJava: theory JVMExecInstr

02:32:12 HOL-MicroJava: theory Effect

02:32:12 HOL-MicroJava: theory JVMExec

02:32:13 HOL-MicroJava: theory DefsComp

02:32:13 HOL-MicroJava: theory JVMDefensive

02:32:13 HOL-MicroJava: theory JVMListExample

02:32:13 HOL-MicroJava: theory Index

02:32:13 HOL-MicroJava: theory TranslCompTp

02:32:14 HOL-MicroJava: theory Example

02:32:14 HOL-MicroJava: theory JListExample

02:32:14 HOL-MicroJava: theory JTypeSafe

02:32:14 HOL-MicroJava: theory TranslComp

02:32:14 HOL-MicroJava: theory LemmasComp

02:32:15 HOL-MicroJava: theory CorrComp

02:32:29 HOL-MicroJava: theory BVSpec

02:32:29 HOL-MicroJava: theory EffectMono

02:32:30 HOL-MicroJava: theory Altern

02:32:30 HOL-MicroJava: theory Correct

02:32:30 HOL-MicroJava: theory Typing_Framework_JVM

02:32:30 HOL-MicroJava: theory BVSpecTypeSafe

02:32:30 HOL-MicroJava: theory JVM

02:32:30 HOL-MicroJava: theory LBVJVM

02:32:30 HOL-MicroJava: theory CorrCompTp

02:32:31 HOL-MicroJava: theory BVNoTypeError

02:32:31 HOL-MicroJava: theory BVExample

02:32:32 HOL-MicroJava: theory MicroJava

02:33:04 Timing HOL-MicroJava (6 threads, 61.849s elapsed time, 276.296s cpu time, 7.636s GC time, factor 4.47)

02:33:04 Finished HOL-MicroJava (0:01:03 elapsed time, 0:04:38 cpu time, factor 4.36)

02:33:04 Running HOL-Nominal-Examples ...

02:33:06 HOL-Nominal-Examples: theory CK_Machine

02:33:06 HOL-Nominal-Examples: theory CR_Takahashi

02:33:06 HOL-Nominal-Examples: theory Class1

02:33:06 HOL-Nominal-Examples: theory Contexts

02:33:06 HOL-Nominal-Examples: theory Compile

02:33:06 HOL-Nominal-Examples: theory Crary

02:33:09 HOL-Nominal-Examples: theory Fsub

02:33:09 HOL-Nominal-Examples: theory Height

02:33:11 HOL-Nominal-Examples: theory Lam_Funs

02:33:12 HOL-Nominal-Examples: theory Lambda_mu

02:33:14 HOL-Nominal-Examples: theory CR

02:33:15 HOL-Nominal-Examples: theory SN

02:33:17 HOL-Nominal-Examples: theory LocalWeakening

02:33:17 HOL-Nominal-Examples: theory Pattern

02:33:18 HOL-Nominal-Examples: theory SOS

02:33:18 HOL-Nominal-Examples: theory Standardization

02:33:20 HOL-Nominal-Examples: theory Support

02:33:20 HOL-Nominal-Examples: theory Type_Preservation

02:33:21 HOL-Nominal-Examples: theory W

02:33:21 HOL-Nominal-Examples: theory Weakening

02:35:21 HOL-Nominal-Examples: theory Class2

02:35:23 HOL-Nominal-Examples: theory Class3

02:39:07 HOL-Nominal-Examples: theory VC_Condition

02:39:09 Timing HOL-Nominal-Examples (6 threads, 363.375s elapsed time, 1363.948s cpu time, 120.796s GC time, factor 3.75)

02:39:09 Finished HOL-Nominal-Examples (0:06:05 elapsed time, 0:22:46 cpu time, factor 3.74)

02:39:10 Running HOL-Nonstandard_Analysis-Examples ...

02:39:11 HOL-Nonstandard_Analysis-Examples: theory Cancellation

02:39:12 HOL-Nonstandard_Analysis-Examples: theory Multiset

02:39:16 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring

02:39:23 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm

02:39:29 HOL-Nonstandard_Analysis-Examples: theory Primes

02:39:29 HOL-Nonstandard_Analysis-Examples: theory NSPrimes

02:39:33 Timing HOL-Nonstandard_Analysis-Examples (6 threads, 20.559s elapsed time, 50.808s cpu time, 1.880s GC time, factor 2.47)

02:39:33 Finished HOL-Nonstandard_Analysis-Examples (0:00:22 elapsed time, 0:00:52 cpu time, factor 2.34)

02:39:33 Running HOL-Number_Theory ...

02:39:34 HOL-Number_Theory: theory Cancellation

02:39:34 HOL-Number_Theory: theory Congruence

02:39:34 HOL-Number_Theory: theory FuncSet

02:39:35 HOL-Number_Theory: theory Multiset

02:39:35 HOL-Number_Theory: theory Lattice

02:39:37 HOL-Number_Theory: theory Group

02:39:38 HOL-Number_Theory: theory FiniteProduct

02:39:39 HOL-Number_Theory: theory Ring

02:39:44 HOL-Number_Theory: theory MiscAlgebra

02:39:44 HOL-Number_Theory: theory Factorial_Ring

02:39:44 HOL-Number_Theory: theory Fib

02:39:51 HOL-Number_Theory: theory Euclidean_Algorithm

02:39:57 HOL-Number_Theory: theory Primes

02:39:58 HOL-Number_Theory: theory Cong

02:39:58 HOL-Number_Theory: theory Eratosthenes

02:39:58 HOL-Number_Theory: theory Residues

02:40:00 HOL-Number_Theory: theory Euler_Criterion

02:40:00 HOL-Number_Theory: theory Pocklington

02:40:00 HOL-Number_Theory: theory Gauss

02:40:01 HOL-Number_Theory: theory Quadratic_Reciprocity

02:40:01 HOL-Number_Theory: theory Number_Theory

02:40:13 Timing HOL-Number_Theory (6 threads, 38.386s elapsed time, 137.400s cpu time, 4.160s GC time, factor 3.58)

02:40:13 Finished HOL-Number_Theory (0:00:40 elapsed time, 0:02:19 cpu time, factor 3.46)

02:40:13 Running HOL-Predicate_Compile_Examples ...

02:40:15 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs

02:40:15 HOL-Predicate_Compile_Examples: theory Examples

02:40:15 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck

02:40:15 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests

02:40:15 HOL-Predicate_Compile_Examples: theory Specialisation_Examples

02:40:16 HOL-Predicate_Compile_Examples: theory IMP_1

02:40:16 HOL-Predicate_Compile_Examples: theory IMP_2

02:40:16 HOL-Predicate_Compile_Examples: theory IMP_3

02:40:16 HOL-Predicate_Compile_Examples: theory IMP_4

02:40:16 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples

02:40:57 HOL-Predicate_Compile_Examples: theory Code_Prolog

02:40:57 HOL-Predicate_Compile_Examples: theory Hotel_Example

02:40:57 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples

02:40:57 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example

02:40:57 HOL-Predicate_Compile_Examples: theory Lambda_Example

02:40:57 HOL-Predicate_Compile_Examples: theory List_Examples

02:40:59 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog

02:41:00 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example

02:41:06 Timing HOL-Predicate_Compile_Examples (6 threads, 50.227s elapsed time, 154.068s cpu time, 7.848s GC time, factor 3.07)

02:41:06 Finished HOL-Predicate_Compile_Examples (0:00:52 elapsed time, 0:04:26 cpu time, factor 5.11)

02:41:06 Running HOL-Probability-ex ...

02:41:11 HOL-Probability-ex: theory Dining_Cryptographers

02:41:11 HOL-Probability-ex: theory Koepf_Duermuth_Countermeasure

02:41:11 HOL-Probability-ex: theory Measure_Not_CCC

02:41:38 Timing HOL-Probability-ex (6 threads, 26.312s elapsed time, 45.428s cpu time, 1.144s GC time, factor 1.73)

02:41:38 Finished HOL-Probability-ex (0:00:31 elapsed time, 0:00:50 cpu time, factor 1.60)

02:41:38 Running HOL-Proofs-Extraction ...

02:41:40 HOL-Proofs-Extraction: theory Adhoc_Overloading

02:41:40 HOL-Proofs-Extraction: theory Binomial

02:41:40 HOL-Proofs-Extraction: theory Cancellation

02:41:40 HOL-Proofs-Extraction: theory Code_Abstract_Nat

02:41:40 HOL-Proofs-Extraction: theory GCD

02:41:40 HOL-Proofs-Extraction: theory Monad_Syntax

02:41:40 HOL-Proofs-Extraction: theory Code_Target_Nat

02:41:40 HOL-Proofs-Extraction: theory State_Monad

02:41:41 HOL-Proofs-Extraction: theory Multiset

02:41:54 HOL-Proofs-Extraction: theory Code_Target_Int

02:41:54 HOL-Proofs-Extraction: theory Code_Target_Numeral

02:41:59 HOL-Proofs-Extraction: theory Factorial_Ring

02:42:11 HOL-Proofs-Extraction: theory Euclidean_Algorithm

02:42:19 HOL-Proofs-Extraction: theory Primes

02:42:28 HOL-Proofs-Extraction: theory Warshall

02:42:28 HOL-Proofs-Extraction: theory Higman

02:42:28 HOL-Proofs-Extraction: theory Util

02:42:28 HOL-Proofs-Extraction: theory QuotRem

02:42:28 HOL-Proofs-Extraction: theory Euclid

02:42:28 HOL-Proofs-Extraction: theory Pigeonhole

02:42:29 HOL-Proofs-Extraction: theory Higman_Extraction

02:42:32 HOL-Proofs-Extraction: theory Greatest_Common_Divisor

02:43:09 Timing HOL-Proofs-Extraction (6 threads, 88.738s elapsed time, 219.948s cpu time, 10.108s GC time, factor 2.48)

02:43:09 Finished HOL-Proofs-Extraction (0:01:31 elapsed time, 0:03:42 cpu time, factor 2.44)

02:43:09 Running HOL-Proofs-Lambda ...

02:43:11 HOL-Proofs-Lambda: theory GCD

02:43:25 HOL-Proofs-Lambda: theory Code_Target_Int

02:43:25 HOL-Proofs-Lambda: theory Lambda

02:43:25 HOL-Proofs-Lambda: theory Commutation

02:43:25 HOL-Proofs-Lambda: theory ListOrder

02:43:28 HOL-Proofs-Lambda: theory ListApplication

02:43:28 HOL-Proofs-Lambda: theory ParRed

02:43:28 HOL-Proofs-Lambda: theory LambdaType

02:43:28 HOL-Proofs-Lambda: theory ListBeta

02:43:29 HOL-Proofs-Lambda: theory Eta

02:43:29 HOL-Proofs-Lambda: theory InductTermi

02:43:29 HOL-Proofs-Lambda: theory NormalForm

02:43:29 HOL-Proofs-Lambda: theory Standardization

02:43:30 HOL-Proofs-Lambda: theory StrongNorm

02:43:30 HOL-Proofs-Lambda: theory WeakNorm

02:45:25 Timing HOL-Proofs-Lambda (6 threads, 132.869s elapsed time, 165.912s cpu time, 7.112s GC time, factor 1.25)

02:45:25 Finished HOL-Proofs-Lambda (0:02:15 elapsed time, 0:02:48 cpu time, factor 1.24)

02:45:25 Running HOL-Quickcheck_Benchmark ...

02:45:26 HOL-Quickcheck_Benchmark: theory Predicate_Compile_Alternative_Defs

02:45:26 HOL-Quickcheck_Benchmark: theory Find_Unused_Assms_Examples

02:45:27 HOL-Quickcheck_Benchmark: theory Predicate_Compile_Quickcheck

02:45:27 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Base

02:45:30 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Guided_Attacker_Example

02:45:31 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_No_Attacker_Example

02:45:31 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Unguided_Attacker_Example

02:49:14 Timing HOL-Quickcheck_Benchmark (6 threads, 226.972s elapsed time, 1088.024s cpu time, 100.488s GC time, factor 4.79)

02:49:14 Finished HOL-Quickcheck_Benchmark (0:03:49 elapsed time, 0:18:38 cpu time, factor 4.88)

02:49:14 Running HOL-Quickcheck_Examples ...

02:49:16 HOL-Quickcheck_Examples: theory AList

02:49:16 HOL-Quickcheck_Examples: theory Completeness

02:49:16 HOL-Quickcheck_Examples: theory Cancellation

02:49:16 HOL-Quickcheck_Examples: theory Dlist

02:49:16 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces

02:49:16 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples

02:49:16 HOL-Quickcheck_Examples: theory Quickcheck_Nesting

02:49:17 HOL-Quickcheck_Examples: theory Multiset

02:49:17 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example

02:49:18 HOL-Quickcheck_Examples: theory DAList

02:49:21 HOL-Quickcheck_Examples: theory DAList_Multiset

02:49:21 HOL-Quickcheck_Examples: theory Quickcheck_Examples

02:49:42 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples

02:49:42 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs

02:49:42 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck

02:49:42 HOL-Quickcheck_Examples: theory Hotel_Example

02:50:26 Timing HOL-Quickcheck_Examples (6 threads, 69.944s elapsed time, 174.988s cpu time, 6.148s GC time, factor 2.50)

02:50:26 Finished HOL-Quickcheck_Examples (0:01:11 elapsed time, 0:04:07 cpu time, factor 3.45)

02:50:26 Running HOL-Quotient_Examples ...

02:50:28 HOL-Quotient_Examples: theory Cancellation

02:50:28 HOL-Quotient_Examples: theory Lift_DList

02:50:28 HOL-Quotient_Examples: theory FuncSet

02:50:28 HOL-Quotient_Examples: theory Lift_FSet

02:50:28 HOL-Quotient_Examples: theory Lift_Set

02:50:28 HOL-Quotient_Examples: theory Congruence

02:50:28 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test

02:50:29 HOL-Quotient_Examples: theory Quotient_Syntax

02:50:29 HOL-Quotient_Examples: theory Multiset

02:50:29 HOL-Quotient_Examples: theory Lift_Fun

02:50:29 HOL-Quotient_Examples: theory Quotient_Message

02:50:29 HOL-Quotient_Examples: theory Quotient_Option

02:50:29 HOL-Quotient_Examples: theory Quotient_Product

02:50:29 HOL-Quotient_Examples: theory Quotient_Rat

02:50:29 HOL-Quotient_Examples: theory Lattice

02:50:29 HOL-Quotient_Examples: theory Quotient_Set

02:50:29 HOL-Quotient_Examples: theory Quotient_List

02:50:30 HOL-Quotient_Examples: theory DList

02:50:30 HOL-Quotient_Examples: theory Quotient_Int

02:50:31 HOL-Quotient_Examples: theory Group

02:50:32 HOL-Quotient_Examples: theory Int_Pow

02:50:33 HOL-Quotient_Examples: theory Quotient_FSet

02:50:55 Timing HOL-Quotient_Examples (6 threads, 26.809s elapsed time, 70.620s cpu time, 3.360s GC time, factor 2.63)

02:50:55 Finished HOL-Quotient_Examples (0:00:28 elapsed time, 0:01:57 cpu time, factor 4.10)

02:50:55 Running HOL-Record_Benchmark ...

02:50:57 HOL-Record_Benchmark: theory Record_Benchmark

02:52:42 Timing HOL-Record_Benchmark (6 threads, 104.848s elapsed time, 176.700s cpu time, 8.952s GC time, factor 1.69)

02:52:42 Finished HOL-Record_Benchmark (0:01:46 elapsed time, 0:02:58 cpu time, factor 1.67)

02:52:42 Running HOL-SET_Protocol ...

02:52:44 HOL-SET_Protocol: theory Nat_Bijection

02:52:45 HOL-SET_Protocol: theory Message_SET

02:52:48 HOL-SET_Protocol: theory Event_SET

02:52:49 HOL-SET_Protocol: theory Public_SET

02:52:50 HOL-SET_Protocol: theory Cardholder_Registration

02:52:50 HOL-SET_Protocol: theory Merchant_Registration

02:52:50 HOL-SET_Protocol: theory Purchase

02:52:52 HOL-SET_Protocol: theory SET_Protocol

02:53:07 Timing HOL-SET_Protocol (6 threads, 22.290s elapsed time, 90.636s cpu time, 1.860s GC time, factor 4.07)

02:53:07 Finished HOL-SET_Protocol (0:00:24 elapsed time, 0:01:32 cpu time, factor 3.83)

02:53:07 Running HOL-UNITY ...

02:53:09 HOL-UNITY: theory Cancellation

02:53:09 HOL-UNITY: theory UNITY

02:53:09 HOL-UNITY: theory ListOrder

02:53:10 HOL-UNITY: theory Constrains

02:53:10 HOL-UNITY: theory Deadlock

02:53:10 HOL-UNITY: theory FP

02:53:10 HOL-UNITY: theory Multiset

02:53:10 HOL-UNITY: theory Network

02:53:10 HOL-UNITY: theory WFair

02:53:11 HOL-UNITY: theory SubstAx

02:53:11 HOL-UNITY: theory Token

02:53:11 HOL-UNITY: theory Detects

02:53:11 HOL-UNITY: theory Union

02:53:12 HOL-UNITY: theory Comp

02:53:12 HOL-UNITY: theory Guar

02:53:12 HOL-UNITY: theory Transformers

02:53:12 HOL-UNITY: theory Extend

02:53:12 HOL-UNITY: theory ProgressSets

02:53:13 HOL-UNITY: theory Project

02:53:13 HOL-UNITY: theory Rename

02:53:13 HOL-UNITY: theory Lift_prog

02:53:14 HOL-UNITY: theory ELT

02:53:14 HOL-UNITY: theory PPROD

02:53:14 HOL-UNITY: theory Multiset_Order

02:53:14 HOL-UNITY: theory Follows

02:53:15 HOL-UNITY: theory UNITY_Main

02:53:15 HOL-UNITY: theory AllocBase

02:53:15 HOL-UNITY: theory Channel

02:53:15 HOL-UNITY: theory Common

02:53:15 HOL-UNITY: theory Counter

02:53:15 HOL-UNITY: theory Alloc

02:53:16 HOL-UNITY: theory AllocImpl

02:53:16 HOL-UNITY: theory Client

02:53:17 HOL-UNITY: theory Counterc

02:53:17 HOL-UNITY: theory Handshake

02:53:17 HOL-UNITY: theory Lift

02:53:17 HOL-UNITY: theory Mutex

02:53:17 HOL-UNITY: theory NSP_Bad

02:53:18 HOL-UNITY: theory PriorityAux

02:53:18 HOL-UNITY: theory Progress

02:53:18 HOL-UNITY: theory Priority

02:53:18 HOL-UNITY: theory Reach

02:53:18 HOL-UNITY: theory TimerArray

02:53:18 HOL-UNITY: theory Reachability

02:53:31 Timing HOL-UNITY (6 threads, 21.057s elapsed time, 104.204s cpu time, 3.988s GC time, factor 4.95)

02:53:31 Finished HOL-UNITY (0:00:23 elapsed time, 0:01:46 cpu time, factor 4.51)

02:53:31 Running HOL-Word-SMT_Examples ...

02:53:33 HOL-Word-SMT_Examples: theory Boogie

02:53:33 HOL-Word-SMT_Examples: theory SMT_Examples

02:53:33 HOL-Word-SMT_Examples: theory SMT_Tests

02:53:33 HOL-Word-SMT_Examples: theory SMT_Word_Examples

02:54:29 Timing HOL-Word-SMT_Examples (6 threads, 55.643s elapsed time, 74.996s cpu time, 0.884s GC time, factor 1.35)

02:54:29 Finished HOL-Word-SMT_Examples (0:00:57 elapsed time, 0:01:18 cpu time, factor 1.36)

02:54:29 Running IOA ...

02:54:31 IOA: theory Asig

02:54:31 IOA: theory Seq

02:54:31 IOA: theory Pred

02:54:31 IOA: theory Automata

02:54:32 IOA: theory Sequence

02:54:33 IOA: theory Traces

02:54:33 IOA: theory TL

02:54:34 IOA: theory CompoExecs

02:54:34 IOA: theory RefMappings

02:54:34 IOA: theory ShortExecutions

02:54:34 IOA: theory RefCorrectness

02:54:35 IOA: theory CompoScheds

02:54:35 IOA: theory Simulations

02:54:35 IOA: theory SimCorrectness

02:54:35 IOA: theory Deadlock

02:54:35 IOA: theory CompoTraces

02:54:36 IOA: theory Compositionality

02:54:36 IOA: theory IOA

02:54:37 IOA: theory TLS

02:54:37 IOA: theory LiveIOA

02:54:37 IOA: theory Abstraction

02:54:39 Timing IOA (6 threads, 7.537s elapsed time, 30.440s cpu time, 0.940s GC time, factor 4.04)

02:54:39 Finished IOA (0:00:09 elapsed time, 0:00:32 cpu time, factor 3.31)

02:54:39 Running ZF-UNITY ...

02:54:39 ZF-UNITY: theory FoldSet

02:54:39 ZF-UNITY: theory GenPrefix

02:54:39 ZF-UNITY: theory Acc

02:54:39 ZF-UNITY: theory State

02:54:39 ZF-UNITY: theory UNITY

02:54:40 ZF-UNITY: theory Multiset

02:54:40 ZF-UNITY: theory Constrains

02:54:40 ZF-UNITY: theory FP

02:54:40 ZF-UNITY: theory WFair

02:54:40 ZF-UNITY: theory SubstAx

02:54:40 ZF-UNITY: theory MultisetSum

02:54:40 ZF-UNITY: theory Monotonicity

02:54:40 ZF-UNITY: theory Mutex

02:54:40 ZF-UNITY: theory Union

02:54:41 ZF-UNITY: theory Increasing

02:54:41 ZF-UNITY: theory Follows

02:54:41 ZF-UNITY: theory Comp

02:54:41 ZF-UNITY: theory Guar

02:54:41 ZF-UNITY: theory AllocBase

02:54:42 ZF-UNITY: theory ClientImpl

02:54:42 ZF-UNITY: theory Distributor

02:54:42 ZF-UNITY: theory Merge

02:54:42 ZF-UNITY: theory AllocImpl

02:54:46 Timing ZF-UNITY (6 threads, 6.170s elapsed time, 30.748s cpu time, 1.100s GC time, factor 4.98)

02:54:46 Finished ZF-UNITY (0:00:06 elapsed time, 0:00:31 cpu time, factor 4.66)

02:54:46

02:54:46 === TIMING ===

02:54:46

02:54:46 Group main: 0:13:43 elapsed time, 0:49:09 cpu time, factor 3.58

02:54:46 Group timing: 0:53:39 elapsed time, 3:06:24 cpu time, factor 3.47

02:54:46 Group ZF: 0:00:19 elapsed time, 0:01:12 cpu time, factor 3.67

02:54:46 Overall: 1:10:55 elapsed time, 4:06:04 cpu time, factor 3.47

02:54:46 Archiving artifacts

02:54:46 Started calculate disk usage of build

02:54:46 Finished Calculation of disk usage of build in 0 seconds

02:54:49 Started calculate disk usage of workspace

02:54:49 Finished Calculation of disk usage of workspace in 0 seconds

02:54:49 No emails were triggered.

02:54:49 Finished: SUCCESS