Console Output

16:59:32 Started by an SCM change
16:59:32 [EnvInject] - Loading node environment variables.
16:59:32 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark
16:59:32 [isabelle-nightly-benchmark] $ hg showconfig paths.default
16:59:32 [isabelle-nightly-benchmark] $ hg pull --rev default
16:59:32 pulling from http://isabelle.in.tum.de/repos/isabelle/
16:59:32 searching for changes
16:59:32 no changes found
16:59:32 [isabelle-nightly-benchmark] $ hg update --clean --rev default
16:59:32 39 files updated, 0 files merged, 0 files removed, 0 files unresolved
16:59:32 [isabelle-nightly-benchmark] $ hg --config extensions.purge= clean --all
16:59:32 [isabelle-nightly-benchmark] $ hg log --rev . --template {node}
16:59:33 [isabelle-nightly-benchmark] $ hg log --rev . --template {rev}
16:59:33 No emails were triggered.
16:59:33 [EnvInject] - Executing scripts and injecting environment variables after the SCM step.
16:59:33 [EnvInject] - Injecting as environment variables the properties content 
16:59:33 ISABELLE_CI_PLATFORM=32
16:59:33 
16:59:33 [EnvInject] - Variables injected successfully.
16:59:33 [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/hudson7893162493998290561.sh
16:59:33 + Admin/jenkins/run_build benchmark
16:59:33 + set -e
16:59:33 + PROFILE=benchmark
16:59:33 + shift
16:59:33 + bin/isabelle components -a
16:59:33 + bin/isabelle jedit -bf
16:59:33 ### Building graph browser ...
16:59:33 warning: [options] bootstrap class path not set in conjunction with -source 1.4
16:59:33 warning: [options] source value 1.4 is obsolete and will be removed in a future release
16:59:33 warning: [options] target value 1.4 is obsolete and will be removed in a future release
16:59:33 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
16:59:35 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
16:59:35 Note: Recompile with -Xlint:deprecation for details.
16:59:35 4 warnings
16:59:35 ### Building Isabelle/Scala ...
17:00:18 ### Building Isabelle/jEdit ...
17:00:45 + bin/isabelle ci_build_benchmark
17:00:50 
17:00:50 === CONFIGURATION ===
17:00:50 
17:00:50 ML_PLATFORM="x86-linux"
17:00:50 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux"
17:00:50 ML_SYSTEM="polyml-5.6"
17:00:50 ML_OPTIONS="-H 1000 --gcthreads 2"
17:00:51 
17:00:51 === BUILD ===
17:00:51 
17:00:51 Build started at Thu, 22 Sep 2016 15:00:50 GMT
17:00:51 Isabelle id d4b89572ae71
17:00:51 
17:00:51 === LOG ===
17:00:51 
17:00:51 Session Pure/Pure
17:00:51 Session HOL/HOL (main)
17:00:52 Session HOL/HOL-Algebra (main timing)
17:00:52 Session HOL/HOL-Analysis (main timing)
17:00:53 Session HOL/HOL-Probability (timing)
17:00:53 Session HOL/HOL-Probability-ex (timing)
17:00:53 Session HOL/HOL-Auth (timing)
17:00:53 Session HOL/HOL-UNITY (timing)
17:00:53 Session HOL/HOL-Bali (timing)
17:00:53 Session HOL/HOL-Cardinals (timing)
17:00:53 Session HOL/HOL-Corec_Examples (timing)
17:00:53 Session HOL/HOL-Data_Structures (timing)
17:00:53 Session HOL/HOL-Datatype_Benchmark
17:00:53 Session HOL/HOL-Datatype_Examples (timing)
17:00:53 Session HOL/HOL-Decision_Procs (timing)
17:00:54 Session HOL/HOL-Hoare_Parallel (timing)
17:00:54 Session HOL/HOL-IMP (timing)
17:00:54 Session HOL/HOL-Library (main timing)
17:00:54 Session HOL/HOL-Metis_Examples (timing)
17:00:54 Session HOL/HOL-MicroJava (timing)
17:00:54 Session HOL/HOL-Nominal
17:00:54 Session HOL/HOL-Nominal-Examples (timing)
17:00:55 Session HOL/HOL-Nonstandard_Analysis (timing)
17:00:55 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
17:00:55 Session HOL/HOL-Number_Theory (timing)
17:00:55 Session HOL/HOL-Predicate_Compile_Examples (timing)
17:00:55 Session HOL/HOL-Quickcheck_Benchmark
17:00:55 Session HOL/HOL-Quickcheck_Examples (timing)
17:00:55 Session HOL/HOL-Quotient_Examples (timing)
17:00:55 Session HOL/HOL-Record_Benchmark
17:00:55 Session HOL/HOL-SET_Protocol (timing)
17:00:55 Session HOL/HOL-Word (main timing)
17:00:55 Session HOL/HOL-Word-SMT_Examples (timing)
17:00:56 Session HOL/HOLCF (main timing)
17:00:56 Session HOL/IOA (timing)
17:00:56 Session HOL/HOL-Proofs (timing)
17:00:56 Session HOL/HOL-Proofs-Extraction (timing)
17:00:56 Session HOL/HOL-Proofs-Lambda (timing)
17:00:56 Session ZF/ZF (main timing ZF)
17:00:56 Session ZF/ZF-UNITY (timing ZF)
17:00:56 Building Pure ...
17:01:07 Pure: theory Pure
17:01:08 Pure: theory ML_Bootstrap
17:01:10 Timing Pure (6 threads, 0.662s elapsed time, 0.744s cpu time, 0.040s GC time, factor 1.12)
17:01:10 Finished Pure (0:00:12 elapsed time, 0:00:14 cpu time, factor 1.09)
17:01:10 Building HOL ...
17:01:10 HOL: theory Code_Generator
17:01:13 HOL: theory HOL
17:01:16 HOL: theory Ctr_Sugar
17:01:16 HOL: theory Orderings
17:01:16 HOL: theory SAT
17:01:18 HOL: theory Groups
17:01:20 HOL: theory Lattices
17:01:23 HOL: theory Set
17:01:24 HOL: theory Fun
17:01:24 HOL: theory Rings
17:01:24 HOL: theory Typedef
17:01:25 HOL: theory Complete_Lattices
17:01:28 HOL: theory Inductive
17:01:30 HOL: theory Product_Type
17:01:30 HOL: theory Sum_Type
17:01:31 HOL: theory Complete_Partial_Order
17:01:34 HOL: theory Nat
17:01:36 HOL: theory Fields
17:01:36 HOL: theory Meson
17:01:36 HOL: theory ATP
17:01:39 HOL: theory Metis
17:01:41 HOL: theory Finite_Set
17:01:42 HOL: theory Relation
17:01:44 HOL: theory Transitive_Closure
17:01:45 HOL: theory Wellfounded
17:01:46 HOL: theory Fun_Def_Base
17:01:46 HOL: theory Hilbert_Choice
17:01:46 HOL: theory Wfrec
17:01:46 HOL: theory Order_Relation
17:01:46 HOL: theory BNF_Wellorder_Relation
17:01:46 HOL: theory Zorn
17:01:47 HOL: theory BNF_Wellorder_Embedding
17:01:47 HOL: theory BNF_Wellorder_Constructions
17:01:48 HOL: theory BNF_Cardinal_Order_Relation
17:01:49 HOL: theory BNF_Cardinal_Arithmetic
17:01:49 HOL: theory BNF_Def
17:01:51 HOL: theory BNF_Composition
17:01:51 HOL: theory Basic_BNFs
17:01:52 HOL: theory BNF_Fixpoint_Base
17:01:56 HOL: theory BNF_Least_Fixpoint
17:01:58 HOL: theory Basic_BNF_LFPs
17:01:58 HOL: theory Num
17:01:58 HOL: theory Transfer
17:02:01 HOL: theory Power
17:02:03 HOL: theory Groups_Big
17:02:05 HOL: theory Equiv_Relations
17:02:06 HOL: theory Lifting
17:02:08 HOL: theory Lifting_Set
17:02:08 HOL: theory Option
17:02:08 HOL: theory Quotient
17:02:08 HOL: theory Extraction
17:02:08 HOL: theory Lattices_Big
17:02:08 HOL: theory Partial_Function
17:02:09 HOL: theory Fun_Def
17:02:11 HOL: theory Int
17:02:14 HOL: theory Nat_Transfer
17:02:15 HOL: theory Parity
17:02:20 HOL: theory Divides
17:02:25 HOL: theory Code_Numeral
17:02:25 HOL: theory Numeral_Simprocs
17:02:25 HOL: theory SMT
17:02:25 HOL: theory Set_Interval
17:02:26 HOL: theory Semiring_Normalization
17:02:28 HOL: theory Conditionally_Complete_Lattices
17:02:28 HOL: theory Filter
17:02:28 HOL: theory Groebner_Basis
17:02:29 HOL: theory Presburger
17:02:32 HOL: theory Sledgehammer
17:02:34 HOL: theory List
17:02:42 HOL: theory Groups_List
17:02:42 HOL: theory Map
17:02:43 HOL: theory Enum
17:02:43 HOL: theory Random
17:02:45 HOL: theory String
17:02:46 HOL: theory BNF_Greatest_Fixpoint
17:02:46 HOL: theory Predicate
17:02:46 HOL: theory Typerep
17:02:48 HOL: theory Lazy_Sequence
17:02:49 HOL: theory Limited_Sequence
17:02:49 HOL: theory Code_Evaluation
17:02:51 HOL: theory Quickcheck_Random
17:02:54 HOL: theory Quickcheck_Exhaustive
17:02:54 HOL: theory Quickcheck_Narrowing
17:02:54 HOL: theory Random_Pred
17:02:54 HOL: theory Random_Sequence
17:03:00 HOL: theory Record
17:03:00 HOL: theory Predicate_Compile
17:03:06 HOL: theory Nitpick
17:03:14 HOL: theory Main
17:03:16 HOL: theory Archimedean_Field
17:03:16 HOL: theory Binomial
17:03:16 HOL: theory GCD
17:03:16 HOL: theory Topological_Spaces
17:03:21 HOL: theory Rat
17:03:24 HOL: theory Real
17:03:25 HOL: theory Real_Vector_Spaces
17:03:36 HOL: theory Inequalities
17:03:36 HOL: theory Limits
17:03:40 HOL: theory Deriv
17:03:40 HOL: theory Series
17:03:41 HOL: theory NthRoot
17:03:42 HOL: theory Transcendental
17:03:46 HOL: theory Complex
17:03:46 HOL: theory MacLaurin
17:03:48 HOL: theory Complex_Main
17:05:06 Timing HOL (6 threads, 166.833s elapsed time, 579.580s cpu time, 48.060s GC time, factor 3.47)
17:05:06 Finished HOL (0:03:56 elapsed time, 0:11:32 cpu time, factor 2.93)
17:05:07 Building HOL-Proofs ...
17:05:07 HOL-Proofs: theory Proofs
17:05:08 HOL-Proofs: theory Code_Generator
17:05:10 HOL-Proofs: theory HOL
17:05:13 HOL-Proofs: theory Ctr_Sugar
17:05:13 HOL-Proofs: theory Orderings
17:05:13 HOL-Proofs: theory SAT
17:05:16 HOL-Proofs: theory Groups
17:05:20 HOL-Proofs: theory Lattices
17:05:23 HOL-Proofs: theory Set
17:05:25 HOL-Proofs: theory Fun
17:05:25 HOL-Proofs: theory Typedef
17:05:25 HOL-Proofs: theory Rings
17:05:26 HOL-Proofs: theory Complete_Lattices
17:05:29 HOL-Proofs: theory Inductive
17:05:30 HOL-Proofs: theory Product_Type
17:05:30 HOL-Proofs: theory Sum_Type
17:05:32 HOL-Proofs: theory Complete_Partial_Order
17:05:36 HOL-Proofs: theory Nat
17:05:39 HOL-Proofs: theory Fields
17:05:39 HOL-Proofs: theory Meson
17:05:40 HOL-Proofs: theory ATP
17:05:42 HOL-Proofs: theory Metis
17:05:45 HOL-Proofs: theory Finite_Set
17:05:47 HOL-Proofs: theory Relation
17:05:48 HOL-Proofs: theory Transitive_Closure
17:05:53 HOL-Proofs: theory Wellfounded
17:05:53 HOL-Proofs: theory Fun_Def_Base
17:05:53 HOL-Proofs: theory Hilbert_Choice
17:05:53 HOL-Proofs: theory Wfrec
17:05:54 HOL-Proofs: theory Order_Relation
17:05:54 HOL-Proofs: theory BNF_Wellorder_Relation
17:05:54 HOL-Proofs: theory Zorn
17:05:54 HOL-Proofs: theory BNF_Wellorder_Embedding
17:05:55 HOL-Proofs: theory BNF_Wellorder_Constructions
17:05:58 HOL-Proofs: theory BNF_Cardinal_Order_Relation
17:05:59 HOL-Proofs: theory BNF_Cardinal_Arithmetic
17:06:00 HOL-Proofs: theory BNF_Def
17:06:02 HOL-Proofs: theory BNF_Composition
17:06:02 HOL-Proofs: theory Basic_BNFs
17:06:04 HOL-Proofs: theory BNF_Fixpoint_Base
17:06:07 HOL-Proofs: theory BNF_Least_Fixpoint
17:06:09 HOL-Proofs: theory Basic_BNF_LFPs
17:06:09 HOL-Proofs: theory Num
17:06:10 HOL-Proofs: theory Transfer
17:06:14 HOL-Proofs: theory Power
17:06:17 HOL-Proofs: theory Groups_Big
17:06:20 HOL-Proofs: theory Equiv_Relations
17:06:20 HOL-Proofs: theory Lifting
17:06:23 HOL-Proofs: theory Lifting_Set
17:06:23 HOL-Proofs: theory Quotient
17:06:23 HOL-Proofs: theory Option
17:06:24 HOL-Proofs: theory Lattices_Big
17:06:24 HOL-Proofs: theory Partial_Function
17:06:25 HOL-Proofs: theory Fun_Def
17:06:27 HOL-Proofs: theory Int
17:06:34 HOL-Proofs: theory Nat_Transfer
17:06:35 HOL-Proofs: theory Parity
17:06:37 HOL-Proofs: theory Divides
17:06:42 HOL-Proofs: theory Code_Numeral
17:06:43 HOL-Proofs: theory Numeral_Simprocs
17:06:43 HOL-Proofs: theory SMT
17:06:43 HOL-Proofs: theory Set_Interval
17:06:44 HOL-Proofs: theory Semiring_Normalization
17:06:47 HOL-Proofs: theory Groebner_Basis
17:06:47 HOL-Proofs: theory Presburger
17:06:50 HOL-Proofs: theory Sledgehammer
17:06:52 HOL-Proofs: theory List
17:12:57 HOL-Proofs: theory Extraction
17:12:57 HOL-Proofs: theory Conditionally_Complete_Lattices
17:12:57 HOL-Proofs: theory Filter
17:12:57 HOL-Proofs: theory Groups_List
17:12:57 HOL-Proofs: theory Map
17:12:58 HOL-Proofs: theory Enum
17:12:58 HOL-Proofs: theory Random
17:13:01 HOL-Proofs: theory String
17:13:02 HOL-Proofs: theory BNF_Greatest_Fixpoint
17:13:02 HOL-Proofs: theory Typerep
17:13:02 HOL-Proofs: theory Predicate
17:13:04 HOL-Proofs: theory Lazy_Sequence
17:13:06 HOL-Proofs: theory Limited_Sequence
17:13:06 HOL-Proofs: theory Code_Evaluation
17:13:09 HOL-Proofs: theory Quickcheck_Random
17:13:12 HOL-Proofs: theory Quickcheck_Exhaustive
17:13:12 HOL-Proofs: theory Quickcheck_Narrowing
17:13:14 HOL-Proofs: theory Random_Pred
17:13:15 HOL-Proofs: theory Random_Sequence
17:13:19 HOL-Proofs: theory Record
17:13:19 HOL-Proofs: theory Predicate_Compile
17:13:22 HOL-Proofs: theory Nitpick
17:13:40 HOL-Proofs: theory Main
17:13:42 HOL-Proofs: theory Old_Datatype
17:15:57 Timing HOL-Proofs (6 threads, 593.859s elapsed time, 2093.092s cpu time, 144.092s GC time, factor 3.52)
17:15:57 Finished HOL-Proofs (0:10:49 elapsed time, 0:36:23 cpu time, factor 3.36)
17:15:59 Building HOL-Analysis ...
17:16:01 HOL-Analysis: theory Disjoint_Sets
17:16:01 HOL-Analysis: theory FuncSet
17:16:01 HOL-Analysis: theory Nat_Bijection
17:16:01 HOL-Analysis: theory Infinite_Set
17:16:01 HOL-Analysis: theory Multiset
17:16:01 HOL-Analysis: theory Old_Datatype
17:16:02 HOL-Analysis: theory Phantom_Type
17:16:02 HOL-Analysis: theory Product_plus
17:16:02 HOL-Analysis: theory Set_Algebras
17:16:02 HOL-Analysis: theory Product_Order
17:16:02 HOL-Analysis: theory L2_Norm
17:16:02 HOL-Analysis: theory Indicator_Function
17:16:02 HOL-Analysis: theory Inner_Product
17:16:02 HOL-Analysis: theory Cardinality
17:16:03 HOL-Analysis: theory Liminf_Limsup
17:16:03 HOL-Analysis: theory Countable
17:16:03 HOL-Analysis: theory Nonpos_Ints
17:16:03 HOL-Analysis: theory Operator_Norm
17:16:03 HOL-Analysis: theory Periodic_Fun
17:16:03 HOL-Analysis: theory Poly_Roots
17:16:04 HOL-Analysis: theory Numeral_Type
17:16:04 HOL-Analysis: theory Sum_of_Squares
17:16:04 HOL-Analysis: theory Product_Vector
17:16:04 HOL-Analysis: theory Convex
17:16:05 HOL-Analysis: theory Countable_Set
17:16:05 HOL-Analysis: theory Euclidean_Space
17:16:05 HOL-Analysis: theory Countable_Complete_Lattices
17:16:06 HOL-Analysis: theory Permutations
17:16:07 HOL-Analysis: theory Finite_Cartesian_Product
17:16:07 HOL-Analysis: theory Linear_Algebra
17:16:07 HOL-Analysis: theory Norm_Arith
17:16:08 HOL-Analysis: theory Order_Continuity
17:16:09 HOL-Analysis: theory Extended_Nat
17:16:10 HOL-Analysis: theory Topology_Euclidean_Space
17:16:10 HOL-Analysis: theory Extended_Real
17:16:14 HOL-Analysis: theory Extended_Nonnegative_Real
17:16:14 HOL-Analysis: theory Summation_Tests
17:16:17 HOL-Analysis: theory Sigma_Algebra
17:16:19 HOL-Analysis: theory Bounded_Linear_Function
17:16:19 HOL-Analysis: theory Convex_Euclidean_Space
17:16:19 HOL-Analysis: theory Extended_Real_Limits
17:16:19 HOL-Analysis: theory Uniform_Limit
17:16:20 HOL-Analysis: theory Measurable
17:16:21 HOL-Analysis: theory Measure_Space
17:16:24 HOL-Analysis: theory Caratheodory
17:16:25 HOL-Analysis: theory Continuous_Extension
17:16:26 HOL-Analysis: theory Path_Connected
17:16:29 HOL-Analysis: theory Homeomorphism
17:16:30 HOL-Analysis: theory Brouwer_Fixpoint
17:16:32 HOL-Analysis: theory Derivative
17:16:34 HOL-Analysis: theory Cartesian_Euclidean_Space
17:16:34 HOL-Analysis: theory Weierstrass_Theorems
17:16:37 HOL-Analysis: theory Determinants
17:16:37 HOL-Analysis: theory Fashoda_Theorem
17:16:37 HOL-Analysis: theory Ordered_Euclidean_Space
17:16:37 HOL-Analysis: theory Polytope
17:16:46 HOL-Analysis: theory Borel_Space
17:16:49 HOL-Analysis: theory Nonnegative_Lebesgue_Integration
17:16:49 HOL-Analysis: theory Regularity
17:16:51 HOL-Analysis: theory Binary_Product_Measure
17:16:52 HOL-Analysis: theory Embed_Measure
17:16:52 HOL-Analysis: theory Finite_Product_Measure
17:16:53 HOL-Analysis: theory Bochner_Integration
17:16:56 HOL-Analysis: theory Complete_Measure
17:16:56 HOL-Analysis: theory Radon_Nikodym
17:16:56 HOL-Analysis: theory Lebesgue_Measure
17:16:56 HOL-Analysis: theory Henstock_Kurzweil_Integration
17:17:02 HOL-Analysis: theory Bounded_Continuous_Function
17:17:02 HOL-Analysis: theory Complex_Analysis_Basics
17:17:02 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration
17:17:02 HOL-Analysis: theory Integral_Test
17:17:02 HOL-Analysis: theory Set_Integral
17:17:03 HOL-Analysis: theory Interval_Integral
17:17:03 HOL-Analysis: theory Complex_Transcendental
17:17:04 HOL-Analysis: theory Lebesgue_Integral_Substitution
17:17:06 HOL-Analysis: theory Generalised_Binomial_Theorem
17:17:06 HOL-Analysis: theory Harmonic_Numbers
17:17:06 HOL-Analysis: theory Cauchy_Integral_Theorem
17:17:09 HOL-Analysis: theory Gamma_Function
17:17:13 HOL-Analysis: theory Conformal_Mappings
17:17:15 HOL-Analysis: theory Analysis
17:22:17 Timing HOL-Analysis (6 threads, 308.384s elapsed time, 1486.116s cpu time, 153.480s GC time, factor 4.82)
17:22:17 Finished HOL-Analysis (0:06:18 elapsed time, 0:26:39 cpu time, factor 4.23)
17:22:18 Building HOL-Auth ...
17:22:20 HOL-Auth: theory Message
17:22:20 HOL-Auth: theory Nat_Bijection
17:22:20 HOL-Auth: theory Simps_Case_Conv
17:22:23 HOL-Auth: theory All_Symmetric
17:22:23 HOL-Auth: theory Event
17:22:23 HOL-Auth: theory EventSC
17:22:24 HOL-Auth: theory Extensions
17:22:24 HOL-Auth: theory Public
17:22:24 HOL-Auth: theory Shared
17:22:24 HOL-Auth: theory Analz
17:22:24 HOL-Auth: theory List_Msg
17:22:24 HOL-Auth: theory CertifiedEmail
17:22:24 HOL-Auth: theory KerberosIV
17:22:25 HOL-Auth: theory KerberosIV_Gets
17:22:25 HOL-Auth: theory KerberosV
17:22:25 HOL-Auth: theory Guard
17:22:25 HOL-Auth: theory GuardK
17:22:26 HOL-Auth: theory Guard_Public
17:22:26 HOL-Auth: theory Kerberos_BAN
17:22:26 HOL-Auth: theory Guard_NS_Public
17:22:26 HOL-Auth: theory P2
17:22:26 HOL-Auth: theory Proto
17:22:27 HOL-Auth: theory Kerberos_BAN_Gets
17:22:27 HOL-Auth: theory NS_Public
17:22:27 HOL-Auth: theory NS_Public_Bad
17:22:27 HOL-Auth: theory NS_Shared
17:22:27 HOL-Auth: theory OtwayRees
17:22:28 HOL-Auth: theory OtwayReesBella
17:22:28 HOL-Auth: theory OtwayRees_AN
17:22:28 HOL-Auth: theory OtwayRees_Bad
17:22:28 HOL-Auth: theory P1
17:22:28 HOL-Auth: theory Recur
17:22:28 HOL-Auth: theory WooLam
17:22:28 HOL-Auth: theory Yahalom
17:22:29 HOL-Auth: theory Yahalom2
17:22:29 HOL-Auth: theory Yahalom_Bad
17:22:29 HOL-Auth: theory ZhouGollmann
17:22:29 HOL-Auth: theory Guard_Shared
17:22:30 HOL-Auth: theory TLS
17:22:30 HOL-Auth: theory Smartcard
17:22:30 HOL-Auth: theory Guard_OtwayRees
17:22:30 HOL-Auth: theory Auth_Shared
17:22:30 HOL-Auth: theory Guard_Yahalom
17:22:30 HOL-Auth: theory ShoupRubin
17:22:30 HOL-Auth: theory ShoupRubinBella
17:22:31 HOL-Auth: theory Auth_Guard_Shared
17:22:32 HOL-Auth: theory Auth_Public
17:22:32 HOL-Auth: theory Auth_Smartcard
17:22:33 HOL-Auth: theory Auth_Guard_Public
17:23:48 Timing HOL-Auth (6 threads, 59.696s elapsed time, 290.620s cpu time, 16.248s GC time, factor 4.87)
17:23:48 Finished HOL-Auth (0:01:29 elapsed time, 0:05:37 cpu time, factor 3.77)
17:23:48 Building HOL-Nominal ...
17:23:50 HOL-Nominal: theory Old_Datatype
17:23:50 HOL-Nominal: theory Infinite_Set
17:23:51 HOL-Nominal: theory Nominal
17:24:12 Timing HOL-Nominal (6 threads, 7.413s elapsed time, 22.284s cpu time, 0.784s GC time, factor 3.01)
17:24:12 Finished HOL-Nominal (0:00:23 elapsed time, 0:00:46 cpu time, factor 1.97)
17:24:12 Building HOL-Nonstandard_Analysis ...
17:24:14 HOL-Nonstandard_Analysis: theory Infinite_Set
17:24:14 HOL-Nonstandard_Analysis: theory Lub_Glb
17:24:14 HOL-Nonstandard_Analysis: theory Free_Ultrafilter
17:24:15 HOL-Nonstandard_Analysis: theory StarDef
17:24:16 HOL-Nonstandard_Analysis: theory HyperNat
17:24:16 HOL-Nonstandard_Analysis: theory HyperDef
17:24:17 HOL-Nonstandard_Analysis: theory NSA
17:24:19 HOL-Nonstandard_Analysis: theory NSComplex
17:24:19 HOL-Nonstandard_Analysis: theory Star
17:24:20 HOL-Nonstandard_Analysis: theory HLim
17:24:20 HOL-Nonstandard_Analysis: theory NatStar
17:24:20 HOL-Nonstandard_Analysis: theory HSEQ
17:24:21 HOL-Nonstandard_Analysis: theory HDeriv
17:24:21 HOL-Nonstandard_Analysis: theory HSeries
17:24:22 HOL-Nonstandard_Analysis: theory HTranscendental
17:24:23 HOL-Nonstandard_Analysis: theory HLog
17:24:23 HOL-Nonstandard_Analysis: theory NSCA
17:24:23 HOL-Nonstandard_Analysis: theory Hyperreal
17:24:24 HOL-Nonstandard_Analysis: theory CStar
17:24:24 HOL-Nonstandard_Analysis: theory CLim
17:24:25 HOL-Nonstandard_Analysis: theory Hypercomplex
17:24:25 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis
17:24:40 Timing HOL-Nonstandard_Analysis (6 threads, 11.704s elapsed time, 35.708s cpu time, 0.900s GC time, factor 3.05)
17:24:40 Finished HOL-Nonstandard_Analysis (0:00:27 elapsed time, 0:00:59 cpu time, factor 2.15)
17:24:40 Building HOL-Probability ...
17:24:44 HOL-Probability: theory Diagonal_Subsequence
17:24:44 HOL-Probability: theory FSet
17:24:44 HOL-Probability: theory Permutation
17:24:44 HOL-Probability: theory AList
17:24:47 HOL-Probability: theory Finite_Map
17:24:50 HOL-Probability: theory Lattice_Syntax
17:24:50 HOL-Probability: theory Adhoc_Overloading
17:24:50 HOL-Probability: theory Mapping
17:24:50 HOL-Probability: theory Stream
17:24:50 HOL-Probability: theory Rewrite
17:24:50 HOL-Probability: theory Sublist
17:24:50 HOL-Probability: theory Complete_Partial_Order2
17:24:50 HOL-Probability: theory Monad_Syntax
17:24:50 HOL-Probability: theory Continuum_Not_Denumerable
17:24:50 HOL-Probability: theory Set_Permutations
17:24:51 HOL-Probability: theory Fin_Map
17:24:51 HOL-Probability: theory Discrete_Topology
17:24:51 HOL-Probability: theory Probability_Measure
17:24:51 HOL-Probability: theory AList_Mapping
17:24:51 HOL-Probability: theory Linear_Temporal_Logic_on_Streams
17:24:53 HOL-Probability: theory Distribution_Functions
17:24:53 HOL-Probability: theory Giry_Monad
17:24:54 HOL-Probability: theory Weak_Convergence
17:24:54 HOL-Probability: theory Helly_Selection
17:24:55 HOL-Probability: theory Probability_Mass_Function
17:24:55 HOL-Probability: theory Projective_Family
17:24:56 HOL-Probability: theory Infinite_Product_Measure
17:24:57 HOL-Probability: theory Independent_Family
17:24:57 HOL-Probability: theory Projective_Limit
17:24:57 HOL-Probability: theory Stream_Space
17:24:57 HOL-Probability: theory PMF_Impl
17:24:57 HOL-Probability: theory Random_Permutations
17:24:57 HOL-Probability: theory SPMF
17:24:59 HOL-Probability: theory Convolution
17:24:59 HOL-Probability: theory Information
17:25:02 HOL-Probability: theory Distributions
17:25:03 HOL-Probability: theory Characteristic_Functions
17:25:03 HOL-Probability: theory Sinc_Integral
17:25:04 HOL-Probability: theory Levy
17:25:05 HOL-Probability: theory Central_Limit_Theorem
17:25:06 HOL-Probability: theory Probability
17:26:32 Timing HOL-Probability (6 threads, 69.981s elapsed time, 355.992s cpu time, 10.816s GC time, factor 5.09)
17:26:32 Finished HOL-Probability (0:01:50 elapsed time, 0:06:58 cpu time, factor 3.78)
17:26:32 Building HOL-Word ...
17:26:33 HOL-Word: theory Bit
17:26:33 HOL-Word: theory Bits
17:26:33 HOL-Word: theory Boolean_Algebra
17:26:33 HOL-Word: theory Misc_Numeric
17:26:33 HOL-Word: theory Misc_Typedef
17:26:33 HOL-Word: theory Phantom_Type
17:26:34 HOL-Word: theory Bit_Representation
17:26:34 HOL-Word: theory Bits_Bit
17:26:34 HOL-Word: theory Word_Miscellaneous
17:26:34 HOL-Word: theory Cardinality
17:26:34 HOL-Word: theory Bits_Int
17:26:35 HOL-Word: theory Numeral_Type
17:26:36 HOL-Word: theory Bool_List_Representation
17:26:36 HOL-Word: theory Type_Length
17:26:37 HOL-Word: theory Word
17:27:01 Timing HOL-Word (6 threads, 10.547s elapsed time, 42.364s cpu time, 1.240s GC time, factor 4.02)
17:27:01 Finished HOL-Word (0:00:28 elapsed time, 0:01:09 cpu time, factor 2.43)
17:27:01 Building HOLCF ...
17:27:03 HOLCF: theory Nat_Bijection
17:27:03 HOLCF: theory Old_Datatype
17:27:04 HOLCF: theory Countable
17:27:05 HOLCF: theory Porder
17:27:06 HOLCF: theory Pcpo
17:27:07 HOLCF: theory Cont
17:27:07 HOLCF: theory Adm
17:27:07 HOLCF: theory Discrete
17:27:08 HOLCF: theory Cpodef
17:27:08 HOLCF: theory Fun_Cpo
17:27:08 HOLCF: theory Product_Cpo
17:27:08 HOLCF: theory Cfun
17:27:09 HOLCF: theory Cprod
17:27:09 HOLCF: theory Fix
17:27:09 HOLCF: theory Sfun
17:27:09 HOLCF: theory Up
17:27:09 HOLCF: theory Sprod
17:27:09 HOLCF: theory Lift
17:27:10 HOLCF: theory One
17:27:10 HOLCF: theory Tr
17:27:10 HOLCF: theory Ssum
17:27:11 HOLCF: theory Plain_HOLCF
17:27:11 HOLCF: theory Completion
17:27:11 HOLCF: theory Deflation
17:27:11 HOLCF: theory Fixrec
17:27:11 HOLCF: theory Map_Functions
17:27:12 HOLCF: theory Bifinite
17:27:12 HOLCF: theory Domain_Aux
17:27:13 HOLCF: theory Universal
17:27:14 HOLCF: theory Algebraic
17:27:14 HOLCF: theory Compact_Basis
17:27:14 HOLCF: theory LowerPD
17:27:14 HOLCF: theory UpperPD
17:27:15 HOLCF: theory Representable
17:27:15 HOLCF: theory ConvexPD
17:27:17 HOLCF: theory Domain
17:27:18 HOLCF: theory Powerdomains
17:27:19 HOLCF: theory HOLCF
17:27:38 Timing HOLCF (6 threads, 17.082s elapsed time, 44.672s cpu time, 1.720s GC time, factor 2.62)
17:27:38 Finished HOLCF (0:00:36 elapsed time, 0:01:14 cpu time, factor 2.02)
17:27:38 Building ZF ...
17:27:38 ZF: theory IFOL
17:27:39 ZF: theory FOL
17:27:40 ZF: theory ZF
17:27:41 ZF: theory upair
17:27:41 ZF: theory pair
17:27:41 ZF: theory Bool
17:27:41 ZF: theory equalities
17:27:42 ZF: theory Fixedpt
17:27:42 ZF: theory Sum
17:27:42 ZF: theory func
17:27:42 ZF: theory Perm
17:27:42 ZF: theory QPair
17:27:43 ZF: theory Trancl
17:27:43 ZF: theory EquivClass
17:27:43 ZF: theory WF
17:27:43 ZF: theory Order
17:27:43 ZF: theory Ordinal
17:27:44 ZF: theory OrdQuant
17:27:44 ZF: theory OrderArith
17:27:44 ZF: theory Nat_ZF
17:27:44 ZF: theory Epsilon
17:27:44 ZF: theory OrderType
17:27:44 ZF: theory Inductive_ZF
17:27:45 ZF: theory Finite
17:27:45 ZF: theory Cardinal
17:27:45 ZF: theory Univ
17:27:46 ZF: theory Arith
17:27:46 ZF: theory QUniv
17:27:46 ZF: theory Datatype_ZF
17:27:46 ZF: theory ArithSimp
17:27:46 ZF: theory Int_ZF
17:27:46 ZF: theory List_ZF
17:27:46 ZF: theory CardinalArith
17:27:47 ZF: theory Bin
17:27:48 ZF: theory IntDiv_ZF
17:27:49 ZF: theory Main_ZF
17:27:49 ZF: theory AC
17:27:49 ZF: theory Main
17:27:49 ZF: theory Zorn
17:27:49 ZF: theory Cardinal_AC
17:27:49 ZF: theory InfDatatype
17:27:49 ZF: theory Main_ZFC
17:27:54 Timing ZF (6 threads, 11.267s elapsed time, 36.732s cpu time, 1.816s GC time, factor 3.26)
17:27:54 Finished ZF (0:00:15 elapsed time, 0:00:43 cpu time, factor 2.78)
17:27:54 Running HOL-Algebra ...
17:27:56 HOL-Algebra: theory FuncSet
17:27:56 HOL-Algebra: theory Multiset
17:28:00 HOL-Algebra: theory Factorial_Ring
17:28:00 HOL-Algebra: theory Permutation
17:28:07 HOL-Algebra: theory Euclidean_Algorithm
17:28:15 HOL-Algebra: theory Primes
17:28:18 HOL-Algebra: theory Congruence
17:28:18 HOL-Algebra: theory Exponent
17:28:19 HOL-Algebra: theory Lattice
17:28:21 HOL-Algebra: theory Group
17:28:23 HOL-Algebra: theory Bij
17:28:23 HOL-Algebra: theory Coset
17:28:23 HOL-Algebra: theory FiniteProduct
17:28:24 HOL-Algebra: theory Ring
17:28:24 HOL-Algebra: theory Sylow
17:28:24 HOL-Algebra: theory Divisibility
17:28:28 HOL-Algebra: theory AbelCoset
17:28:28 HOL-Algebra: theory Module
17:28:34 HOL-Algebra: theory Ideal
17:28:39 HOL-Algebra: theory RingHom
17:28:40 HOL-Algebra: theory QuotRing
17:28:40 HOL-Algebra: theory UnivPoly
17:28:41 HOL-Algebra: theory IntRing
17:28:58 Timing HOL-Algebra (6 threads, 61.388s elapsed time, 201.420s cpu time, 8.044s GC time, factor 3.28)
17:28:58 Finished HOL-Algebra (0:01:03 elapsed time, 0:03:22 cpu time, factor 3.22)
17:28:58 Running HOL-Bali ...
17:29:00 HOL-Bali: theory Old_Recdef
17:29:00 HOL-Bali: theory Basis
17:29:02 HOL-Bali: theory Name
17:29:02 HOL-Bali: theory Table
17:29:04 HOL-Bali: theory Type
17:29:06 HOL-Bali: theory Value
17:29:07 HOL-Bali: theory Term
17:29:27 HOL-Bali: theory Decl
17:29:32 HOL-Bali: theory TypeRel
17:29:33 HOL-Bali: theory DeclConcepts
17:29:35 HOL-Bali: theory State
17:29:35 HOL-Bali: theory WellType
17:29:37 HOL-Bali: theory Conform
17:29:37 HOL-Bali: theory Eval
17:29:38 HOL-Bali: theory DefiniteAssignment
17:29:41 HOL-Bali: theory WellForm
17:29:43 HOL-Bali: theory DefiniteAssignmentCorrect
17:29:43 HOL-Bali: theory Example
17:29:44 HOL-Bali: theory TypeSafe
17:29:46 HOL-Bali: theory Evaln
17:29:49 HOL-Bali: theory AxSem
17:29:49 HOL-Bali: theory Trans
17:29:53 HOL-Bali: theory AxCompl
17:29:53 HOL-Bali: theory AxSound
17:29:53 HOL-Bali: theory AxExample
17:30:17 Timing HOL-Bali (6 threads, 76.956s elapsed time, 293.244s cpu time, 18.032s GC time, factor 3.81)
17:30:17 Finished HOL-Bali (0:01:18 elapsed time, 0:04:54 cpu time, factor 3.75)
17:30:17 Running HOL-Cardinals ...
17:30:19 HOL-Cardinals: theory Order_Union
17:30:19 HOL-Cardinals: theory Cardinal_Notations
17:30:19 HOL-Cardinals: theory Fun_More
17:30:19 HOL-Cardinals: theory Order_Relation_More
17:30:19 HOL-Cardinals: theory Wellorder_Extension
17:30:19 HOL-Cardinals: theory Wellfounded_More
17:30:19 HOL-Cardinals: theory Wellorder_Relation
17:30:19 HOL-Cardinals: theory Wellorder_Embedding
17:30:19 HOL-Cardinals: theory Wellorder_Constructions
17:30:21 HOL-Cardinals: theory Cardinal_Order_Relation
17:30:21 HOL-Cardinals: theory Ordinal_Arithmetic
17:30:22 HOL-Cardinals: theory Cardinal_Arithmetic
17:30:22 HOL-Cardinals: theory Cardinals
17:30:22 HOL-Cardinals: theory Bounded_Set
17:36:48 Timing HOL-Cardinals (6 threads, 388.538s elapsed time, 438.496s cpu time, 12.596s GC time, factor 1.13)
17:36:48 Finished HOL-Cardinals (0:06:30 elapsed time, 0:07:20 cpu time, factor 1.13)
17:36:48 Running HOL-Corec_Examples ...
17:36:49 HOL-Corec_Examples: theory BNF_Corec
17:36:49 HOL-Corec_Examples: theory Nat_Bijection
17:36:49 HOL-Corec_Examples: theory FSet
17:36:50 HOL-Corec_Examples: theory Stream
17:36:55 HOL-Corec_Examples: theory LFilter
17:36:55 HOL-Corec_Examples: theory Simple_Nesting
17:36:55 HOL-Corec_Examples: theory Stream_Processor
17:36:55 HOL-Corec_Examples: theory Paper_Examples
17:37:45 HOL-Corec_Examples: theory GPV_Bare_Bones
17:37:45 HOL-Corec_Examples: theory Merge_A
17:37:45 HOL-Corec_Examples: theory Merge_Poly
17:37:45 HOL-Corec_Examples: theory Misc_Mono
17:37:45 HOL-Corec_Examples: theory Misc_Poly
17:37:45 HOL-Corec_Examples: theory Small_Concrete
17:37:54 HOL-Corec_Examples: theory Merge_B
17:37:58 HOL-Corec_Examples: theory Merge_C
17:38:05 HOL-Corec_Examples: theory Stream_Friends
17:38:08 HOL-Corec_Examples: theory Merge_D
17:38:15 HOL-Corec_Examples: theory TLList_Friends
17:38:17 HOL-Corec_Examples: theory Type_Class
17:40:41 Timing HOL-Corec_Examples (6 threads, 231.622s elapsed time, 596.868s cpu time, 94.028s GC time, factor 2.58)
17:40:41 Finished HOL-Corec_Examples (0:03:53 elapsed time, 0:09:58 cpu time, factor 2.56)
17:40:41 Running HOL-Data_Structures ...
17:40:43 HOL-Data_Structures: theory Multiset
17:40:43 HOL-Data_Structures: theory Less_False
17:40:43 HOL-Data_Structures: theory Lattice_Algebras
17:40:43 HOL-Data_Structures: theory Log_Nat
17:40:49 HOL-Data_Structures: theory Float
17:40:53 HOL-Data_Structures: theory Cmp
17:40:53 HOL-Data_Structures: theory Fib
17:40:53 HOL-Data_Structures: theory Sorted_Less
17:40:53 HOL-Data_Structures: theory Tree
17:40:53 HOL-Data_Structures: theory Tree2
17:40:53 HOL-Data_Structures: theory Tree23
17:40:53 HOL-Data_Structures: theory AList_Upd_Del
17:40:54 HOL-Data_Structures: theory List_Ins_Del
17:40:54 HOL-Data_Structures: theory Tree234
17:40:54 HOL-Data_Structures: theory Map_by_Ordered
17:40:54 HOL-Data_Structures: theory Set_by_Ordered
17:40:54 HOL-Data_Structures: theory Brother12_Set
17:40:55 HOL-Data_Structures: theory Isin2
17:40:55 HOL-Data_Structures: theory Leftist_Heap
17:40:55 HOL-Data_Structures: theory Lookup2
17:40:55 HOL-Data_Structures: theory AA_Set
17:40:56 HOL-Data_Structures: theory AVL_Set
17:40:57 HOL-Data_Structures: theory RBT
17:40:57 HOL-Data_Structures: theory Tree23_Set
17:40:57 HOL-Data_Structures: theory Balance
17:40:57 HOL-Data_Structures: theory Splay_Set
17:40:57 HOL-Data_Structures: theory Tree_Set
17:40:58 HOL-Data_Structures: theory AA_Map
17:40:59 HOL-Data_Structures: theory Tree_Map
17:40:59 HOL-Data_Structures: theory AVL_Map
17:40:59 HOL-Data_Structures: theory Splay_Map
17:41:00 HOL-Data_Structures: theory Tree234_Set
17:41:05 HOL-Data_Structures: theory Tree23_Map
17:41:07 HOL-Data_Structures: theory RBT_Set
17:41:15 HOL-Data_Structures: theory RBT_Map
17:41:27 HOL-Data_Structures: theory Tree234_Map
17:42:13 HOL-Data_Structures: theory Brother12_Map
17:44:01 Timing HOL-Data_Structures (6 threads, 197.640s elapsed time, 1005.780s cpu time, 64.376s GC time, factor 5.09)
17:44:01 Finished HOL-Data_Structures (0:03:19 elapsed time, 0:16:47 cpu time, factor 5.05)
17:44:01 Running HOL-Datatype_Benchmark ...
17:44:02 HOL-Datatype_Benchmark: theory BNF_Axiomatization
17:44:02 HOL-Datatype_Benchmark: theory Brackin
17:44:02 HOL-Datatype_Benchmark: theory IsaFoR
17:44:02 HOL-Datatype_Benchmark: theory Misc_N2M
17:54:10 Timing HOL-Datatype_Benchmark (6 threads, 607.229s elapsed time, 1791.420s cpu time, 519.428s GC time, factor 2.95)
17:54:10 Finished HOL-Datatype_Benchmark (0:10:09 elapsed time, 0:29:53 cpu time, factor 2.94)
17:54:10 Running HOL-Datatype_Examples ...
17:54:11 HOL-Datatype_Examples: theory BNF_Axiomatization
17:54:11 HOL-Datatype_Examples: theory FSet
17:54:11 HOL-Datatype_Examples: theory Infinite_Set
17:54:11 HOL-Datatype_Examples: theory Lift_BNF
17:54:11 HOL-Datatype_Examples: theory Milner_Tofte
17:54:11 HOL-Datatype_Examples: theory Nat_Bijection
17:54:12 HOL-Datatype_Examples: theory Old_Datatype
17:54:12 HOL-Datatype_Examples: theory TreeFI
17:54:12 HOL-Datatype_Examples: theory Stream
17:54:13 HOL-Datatype_Examples: theory Compat
17:54:13 HOL-Datatype_Examples: theory Countable
17:54:14 HOL-Datatype_Examples: theory Process
17:54:14 HOL-Datatype_Examples: theory Stream_Processor
17:54:15 HOL-Datatype_Examples: theory Koenig
17:54:15 HOL-Datatype_Examples: theory Lambda_Term
17:54:15 HOL-Datatype_Examples: theory Misc_Codatatype
17:54:15 HOL-Datatype_Examples: theory Prelim
17:54:15 HOL-Datatype_Examples: theory DTree
17:54:16 HOL-Datatype_Examples: theory Parallel
17:54:16 HOL-Datatype_Examples: theory TreeFsetI
17:54:16 HOL-Datatype_Examples: theory Gram_Lang
17:54:17 HOL-Datatype_Examples: theory Misc_Datatype
17:55:36 HOL-Datatype_Examples: theory Misc_Primcorec
17:55:54 HOL-Datatype_Examples: theory Misc_Primrec
17:55:57 Timing HOL-Datatype_Examples (6 threads, 105.090s elapsed time, 343.144s cpu time, 45.216s GC time, factor 3.27)
17:55:57 Finished HOL-Datatype_Examples (0:01:46 elapsed time, 0:06:02 cpu time, factor 3.39)
17:55:57 Running HOL-Decision_Procs ...
17:55:59 HOL-Decision_Procs: theory Code_Abstract_Nat
17:55:59 HOL-Decision_Procs: theory Commutative_Ring
17:55:59 HOL-Decision_Procs: theory DP_Library
17:55:59 HOL-Decision_Procs: theory Code_Target_Int
17:55:59 HOL-Decision_Procs: theory Dense_Linear_Order
17:55:59 HOL-Decision_Procs: theory Old_Recdef
17:55:59 HOL-Decision_Procs: theory Lattice_Algebras
17:55:59 HOL-Decision_Procs: theory Code_Target_Nat
17:55:59 HOL-Decision_Procs: theory Log_Nat
17:55:59 HOL-Decision_Procs: theory Code_Target_Numeral
17:55:59 HOL-Decision_Procs: theory Polynomial_List
17:55:59 HOL-Decision_Procs: theory Rat_Pair
17:56:00 HOL-Decision_Procs: theory Cooper
17:56:01 HOL-Decision_Procs: theory Dense_Linear_Order_Ex
17:56:01 HOL-Decision_Procs: theory Ferrack
17:56:01 HOL-Decision_Procs: theory MIR
17:56:03 HOL-Decision_Procs: theory Commutative_Ring_Complete
17:56:04 HOL-Decision_Procs: theory Commutative_Ring_Ex
17:56:05 HOL-Decision_Procs: theory Float
17:56:08 HOL-Decision_Procs: theory Approximation
17:56:12 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
17:56:25 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
17:57:04 HOL-Decision_Procs: theory Approximation_Ex
17:57:04 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex
17:57:04 HOL-Decision_Procs: theory Decision_Procs
17:58:44 Timing HOL-Decision_Procs (6 threads, 164.763s elapsed time, 774.684s cpu time, 77.104s GC time, factor 4.70)
17:58:44 Finished HOL-Decision_Procs (0:02:46 elapsed time, 0:12:56 cpu time, factor 4.67)
17:58:44 Running HOL-Hoare_Parallel ...
17:58:45 HOL-Hoare_Parallel: theory Graph
17:58:45 HOL-Hoare_Parallel: theory OG_Com
17:58:45 HOL-Hoare_Parallel: theory Quote_Antiquote
17:58:45 HOL-Hoare_Parallel: theory RG_Com
17:58:46 HOL-Hoare_Parallel: theory RG_Tran
17:58:47 HOL-Hoare_Parallel: theory OG_Tran
17:58:48 HOL-Hoare_Parallel: theory RG_Hoare
17:58:49 HOL-Hoare_Parallel: theory OG_Hoare
17:58:49 HOL-Hoare_Parallel: theory RG_Syntax
17:58:49 HOL-Hoare_Parallel: theory RG_Examples
17:58:49 HOL-Hoare_Parallel: theory OG_Tactics
17:58:50 HOL-Hoare_Parallel: theory OG_Syntax
17:58:50 HOL-Hoare_Parallel: theory Gar_Coll
17:58:51 HOL-Hoare_Parallel: theory Mul_Gar_Coll
17:58:51 HOL-Hoare_Parallel: theory OG_Examples
17:58:55 HOL-Hoare_Parallel: theory Hoare_Parallel
17:59:49 Timing HOL-Hoare_Parallel (6 threads, 63.543s elapsed time, 316.136s cpu time, 4.032s GC time, factor 4.98)
17:59:49 Finished HOL-Hoare_Parallel (0:01:05 elapsed time, 0:05:17 cpu time, factor 4.88)
17:59:49 Running HOL-IMP ...
17:59:50 HOL-IMP: theory Char_ord
17:59:50 HOL-IMP: theory Quotient_Syntax
17:59:50 HOL-IMP: theory List_lexord
17:59:50 HOL-IMP: theory Simps_Case_Conv
17:59:50 HOL-IMP: theory While_Combinator
17:59:50 HOL-IMP: theory Quotient_Option
17:59:50 HOL-IMP: theory Quotient_Product
17:59:50 HOL-IMP: theory Quotient_Set
17:59:50 HOL-IMP: theory Extended
17:59:51 HOL-IMP: theory Quotient_List
17:59:53 HOL-IMP: theory AExp
17:59:53 HOL-IMP: theory Complete_Lattice_ix
17:59:53 HOL-IMP: theory OO
17:59:53 HOL-IMP: theory C_like
17:59:53 HOL-IMP: theory Complete_Lattice
17:59:53 HOL-IMP: theory Star
17:59:53 HOL-IMP: theory Types
17:59:54 HOL-IMP: theory ASM
17:59:54 HOL-IMP: theory BExp
17:59:56 HOL-IMP: theory Com
17:59:56 HOL-IMP: theory Procs
17:59:57 HOL-IMP: theory ACom
17:59:57 HOL-IMP: theory ACom_ITP
17:59:58 HOL-IMP: theory Abs_Int_Tests
17:59:58 HOL-IMP: theory Big_Step
17:59:58 HOL-IMP: theory Vars
17:59:58 HOL-IMP: theory Procs_Dyn_Vars_Dyn
17:59:59 HOL-IMP: theory Denotational
17:59:59 HOL-IMP: theory Hoare
17:59:59 HOL-IMP: theory Sec_Type_Expr
17:59:59 HOL-IMP: theory Hoare_Examples
17:59:59 HOL-IMP: theory Hoare_Sound_Complete
17:59:59 HOL-IMP: theory Hoare_Total_EX
17:59:59 HOL-IMP: theory Hoare_Total
17:59:59 HOL-IMP: theory VCG
18:00:00 HOL-IMP: theory Sec_Typing
18:00:00 HOL-IMP: theory VCG_Total_EX
18:00:00 HOL-IMP: theory Sec_TypingT
18:00:01 HOL-IMP: theory Sem_Equiv
18:00:01 HOL-IMP: theory Def_Init
18:00:01 HOL-IMP: theory Def_Init_Exp
18:00:01 HOL-IMP: theory Fold
18:00:01 HOL-IMP: theory Live
18:00:01 HOL-IMP: theory Procs_Stat_Vars_Dyn
18:00:01 HOL-IMP: theory Def_Init_Big
18:00:01 HOL-IMP: theory Procs_Stat_Vars_Stat
18:00:02 HOL-IMP: theory Collecting
18:00:02 HOL-IMP: theory Collecting_ITP
18:00:02 HOL-IMP: theory Compiler
18:00:02 HOL-IMP: theory Def_Init_Small
18:00:03 HOL-IMP: theory Collecting1
18:00:03 HOL-IMP: theory Collecting_Examples
18:00:03 HOL-IMP: theory Small_Step
18:00:03 HOL-IMP: theory Poly_Types
18:00:04 HOL-IMP: theory Finite_Reachable
18:00:04 HOL-IMP: theory Abs_Int_init
18:00:05 HOL-IMP: theory Live_True
18:00:05 HOL-IMP: theory Abs_Int0
18:00:07 HOL-IMP: theory Abs_State
18:00:07 HOL-IMP: theory Abs_Int0_ITP
18:00:07 HOL-IMP: theory Compiler2
18:00:08 HOL-IMP: theory Abs_Int1
18:00:08 HOL-IMP: theory Abs_Int1_parity
18:00:08 HOL-IMP: theory Abs_Int1_const
18:00:08 HOL-IMP: theory Abs_Int2
18:00:10 HOL-IMP: theory Abs_Int2_ivl
18:00:12 HOL-IMP: theory Abs_State_ITP
18:00:12 HOL-IMP: theory Abs_Int3
18:00:14 HOL-IMP: theory Abs_Int1_ITP
18:00:15 HOL-IMP: theory Abs_Int1_const_ITP
18:00:15 HOL-IMP: theory Abs_Int1_parity_ITP
18:00:15 HOL-IMP: theory Abs_Int2_ITP
18:00:20 HOL-IMP: theory Abs_Int2_ivl_ITP
18:00:22 HOL-IMP: theory Abs_Int3_ITP
18:01:44 Timing HOL-IMP (6 threads, 113.539s elapsed time, 545.844s cpu time, 52.968s GC time, factor 4.81)
18:01:44 Finished HOL-IMP (0:01:55 elapsed time, 0:09:08 cpu time, factor 4.76)
18:01:44 Running HOL-Library ...
18:01:47 HOL-Library: theory Adhoc_Overloading
18:01:47 HOL-Library: theory Preorder
18:01:47 HOL-Library: theory AList
18:01:47 HOL-Library: theory Lattice_Syntax
18:01:47 HOL-Library: theory BNF_Axiomatization
18:01:47 HOL-Library: theory BNF_Corec
18:01:47 HOL-Library: theory Stirling
18:01:47 HOL-Library: theory Bit
18:01:47 HOL-Library: theory Bits
18:01:47 HOL-Library: theory Boolean_Algebra
18:01:47 HOL-Library: theory Cardinal_Notations
18:01:47 HOL-Library: theory Char_ord
18:01:47 HOL-Library: theory Code_Abstract_Nat
18:01:47 HOL-Library: theory Code_Prolog
18:01:47 HOL-Library: theory Bits_Bit
18:01:47 HOL-Library: theory Code_Char
18:01:47 HOL-Library: theory Code_Binary_Nat
18:01:47 HOL-Library: theory Code_Target_Nat
18:01:48 HOL-Library: theory Code_Test
18:01:48 HOL-Library: theory Combine_PER
18:01:48 HOL-Library: theory Complete_Partial_Order2
18:01:48 HOL-Library: theory Debug
18:01:48 HOL-Library: theory Discrete
18:01:48 HOL-Library: theory Disjoint_Sets
18:01:48 HOL-Library: theory Dlist
18:01:48 HOL-Library: theory FSet
18:01:49 HOL-Library: theory Fraction_Field
18:01:49 HOL-Library: theory DAList
18:01:49 HOL-Library: theory Fun_Lexorder
18:01:49 HOL-Library: theory FuncSet
18:01:50 HOL-Library: theory Function_Algebras
18:01:50 HOL-Library: theory Function_Growth
18:01:50 HOL-Library: theory Function_Division
18:01:50 HOL-Library: theory Code_Target_Int
18:01:50 HOL-Library: theory Groups_Big_Fun
18:01:50 HOL-Library: theory Code_Target_Numeral
18:01:51 HOL-Library: theory IArray
18:01:51 HOL-Library: theory Infinite_Set
18:01:51 HOL-Library: theory LaTeXsugar
18:01:51 HOL-Library: theory Lattice_Constructions
18:01:52 HOL-Library: theory Omega_Words_Fun
18:01:52 HOL-Library: theory ListVector
18:01:52 HOL-Library: theory List_lexord
18:01:52 HOL-Library: theory Mapping
18:01:52 HOL-Library: theory Misc_Numeric
18:01:52 HOL-Library: theory Finite_Map
18:01:52 HOL-Library: theory Misc_Typedef
18:01:52 HOL-Library: theory Bit_Representation
18:01:52 HOL-Library: theory Monad_Syntax
18:01:53 HOL-Library: theory More_List
18:01:53 HOL-Library: theory Multiset
18:01:53 HOL-Library: theory Bits_Int
18:01:53 HOL-Library: theory AList_Mapping
18:01:54 HOL-Library: theory Nat_Bijection
18:01:54 HOL-Library: theory Old_Datatype
18:01:54 HOL-Library: theory Old_Recdef
18:01:55 HOL-Library: theory Stream
18:01:55 HOL-Library: theory Option_ord
18:01:55 HOL-Library: theory Parallel
18:01:55 HOL-Library: theory Perm
18:01:56 HOL-Library: theory Phantom_Type
18:01:56 HOL-Library: theory Predicate_Compile_Alternative_Defs
18:01:56 HOL-Library: theory Product_Lexorder
18:01:56 HOL-Library: theory Product_plus
18:01:56 HOL-Library: theory Countable
18:01:57 HOL-Library: theory Predicate_Compile_Quickcheck
18:01:57 HOL-Library: theory Product_Order
18:01:57 HOL-Library: theory Cardinality
18:01:57 HOL-Library: theory Quotient_Syntax
18:01:57 HOL-Library: theory Quotient_Option
18:01:57 HOL-Library: theory Quotient_Product
18:01:57 HOL-Library: theory Finite_Lattice
18:01:57 HOL-Library: theory Quotient_Set
18:01:57 HOL-Library: theory Quotient_Sum
18:01:57 HOL-Library: theory Quotient_List
18:01:57 HOL-Library: theory Quotient_Type
18:01:58 HOL-Library: theory RBT_Impl
18:01:58 HOL-Library: theory FinFun
18:01:58 HOL-Library: theory Numeral_Type
18:01:58 HOL-Library: theory Countable_Set
18:01:59 HOL-Library: theory Countable_Complete_Lattices
18:01:59 HOL-Library: theory Countable_Set_Type
18:01:59 HOL-Library: theory DAList_Multiset
18:02:00 HOL-Library: theory Factorial_Ring
18:02:01 HOL-Library: theory Multiset_Order
18:02:01 HOL-Library: theory Permutation
18:02:01 HOL-Library: theory Permutations
18:02:01 HOL-Library: theory Type_Length
18:02:01 HOL-Library: theory Ramsey
18:02:02 HOL-Library: theory Saturated
18:02:02 HOL-Library: theory Reflection
18:02:02 HOL-Library: theory Refute
18:02:02 HOL-Library: theory Rewrite
18:02:02 HOL-Library: theory Set_Algebras
18:02:02 HOL-Library: theory Simps_Case_Conv
18:02:03 HOL-Library: theory Extended
18:02:03 HOL-Library: theory State_Monad
18:02:03 HOL-Library: theory Sublist
18:02:03 HOL-Library: theory Polynomial
18:02:03 HOL-Library: theory BigO
18:02:04 HOL-Library: theory Prefix_Order
18:02:04 HOL-Library: theory Sublist_Order
18:02:04 HOL-Library: theory Bool_List_Representation
18:02:04 HOL-Library: theory Code_Real_Approx_By_Float
18:02:05 HOL-Library: theory Continuum_Not_Denumerable
18:02:05 HOL-Library: theory Diagonal_Subsequence
18:02:05 HOL-Library: theory Indicator_Function
18:02:05 HOL-Library: theory Inner_Product
18:02:05 HOL-Library: theory Lattice_Algebras
18:02:06 HOL-Library: theory Liminf_Limsup
18:02:07 HOL-Library: theory Product_Vector
18:02:07 HOL-Library: theory Log_Nat
18:02:07 HOL-Library: theory Lub_Glb
18:02:08 HOL-Library: theory Convex
18:02:08 HOL-Library: theory Nonpos_Ints
18:02:08 HOL-Library: theory OptionalSugar
18:02:08 HOL-Library: theory Order_Continuity
18:02:09 HOL-Library: theory Periodic_Fun
18:02:09 HOL-Library: theory Fundamental_Theorem_Algebra
18:02:09 HOL-Library: theory Euclidean_Algorithm
18:02:09 HOL-Library: theory Quadratic_Discriminant
18:02:10 HOL-Library: theory Extended_Nat
18:02:10 HOL-Library: theory Set_Permutations
18:02:13 HOL-Library: theory Sum_of_Squares
18:02:14 HOL-Library: theory Transitive_Closure_Table
18:02:14 HOL-Library: theory Extended_Real
18:02:14 HOL-Library: theory Linear_Temporal_Logic_on_Streams
18:02:15 HOL-Library: theory Float
18:02:16 HOL-Library: theory Tree
18:02:16 HOL-Library: theory While_Combinator
18:02:17 HOL-Library: theory Bourbaki_Witt_Fixpoint
18:02:17 HOL-Library: theory Word_Miscellaneous
18:02:18 HOL-Library: theory Word
18:02:19 HOL-Library: theory Extended_Nonnegative_Real
18:02:20 HOL-Library: theory Tree_Multiset
18:02:23 HOL-Library: theory Normalized_Fraction
18:02:23 HOL-Library: theory Formal_Power_Series
18:02:24 HOL-Library: theory Polynomial_Factorial
18:02:24 HOL-Library: theory Old_SMT
18:02:28 HOL-Library: theory Polynomial_FPS
18:02:29 HOL-Library: theory Library
18:02:43 HOL-Library: theory RBT
18:02:44 HOL-Library: theory RBT_Mapping
18:02:44 HOL-Library: theory RBT_Set
18:03:54 Timing HOL-Library (6 threads, 127.353s elapsed time, 623.824s cpu time, 56.836s GC time, factor 4.90)
18:03:54 Finished HOL-Library (0:02:09 elapsed time, 0:10:25 cpu time, factor 4.84)
18:03:54 Running HOL-Metis_Examples ...
18:03:56 HOL-Metis_Examples: theory Binary_Tree
18:03:56 HOL-Metis_Examples: theory Dense_Linear_Order
18:03:56 HOL-Metis_Examples: theory FuncSet
18:03:56 HOL-Metis_Examples: theory Message
18:03:56 HOL-Metis_Examples: theory Function_Algebras
18:03:56 HOL-Metis_Examples: theory Set_Algebras
18:03:56 HOL-Metis_Examples: theory Sets
18:03:56 HOL-Metis_Examples: theory Clausification
18:03:56 HOL-Metis_Examples: theory Trans_Closure
18:03:57 HOL-Metis_Examples: theory Type_Encodings
18:03:57 HOL-Metis_Examples: theory Abstraction
18:03:57 HOL-Metis_Examples: theory Tarski
18:03:57 HOL-Metis_Examples: theory Proxies
18:03:58 HOL-Metis_Examples: theory Big_O
18:04:12 Timing HOL-Metis_Examples (6 threads, 16.063s elapsed time, 68.188s cpu time, 4.904s GC time, factor 4.25)
18:04:12 Finished HOL-Metis_Examples (0:00:17 elapsed time, 0:01:23 cpu time, factor 4.69)
18:04:12 Running HOL-MicroJava ...
18:04:14 HOL-MicroJava: theory While_Combinator
18:04:15 HOL-MicroJava: theory Eisbach
18:04:15 HOL-MicroJava: theory Transitive_Closure_Table
18:04:15 HOL-MicroJava: theory Semilat
18:04:16 HOL-MicroJava: theory Err
18:04:16 HOL-MicroJava: theory JBasis
18:04:16 HOL-MicroJava: theory AuxLemmas
18:04:16 HOL-MicroJava: theory Type
18:04:17 HOL-MicroJava: theory Listn
18:04:17 HOL-MicroJava: theory Opt
18:04:17 HOL-MicroJava: theory Product
18:04:17 HOL-MicroJava: theory Typing_Framework
18:04:17 HOL-MicroJava: theory Semilattices
18:04:17 HOL-MicroJava: theory SemilatAlg
18:04:18 HOL-MicroJava: theory Kildall
18:04:18 HOL-MicroJava: theory LBVSpec
18:04:18 HOL-MicroJava: theory Typing_Framework_err
18:04:18 HOL-MicroJava: theory Decl
18:04:18 HOL-MicroJava: theory Value
18:04:18 HOL-MicroJava: theory LBVComplete
18:04:18 HOL-MicroJava: theory LBVCorrect
18:04:18 HOL-MicroJava: theory SystemClasses
18:04:19 HOL-MicroJava: theory TypeRel
18:04:19 HOL-MicroJava: theory Abstract_BV
18:04:19 HOL-MicroJava: theory WellForm
18:04:19 HOL-MicroJava: theory State
18:04:19 HOL-MicroJava: theory Term
18:04:20 HOL-MicroJava: theory Exceptions
18:04:20 HOL-MicroJava: theory JType
18:04:20 HOL-MicroJava: theory JVMType
18:04:23 HOL-MicroJava: theory WellType
18:04:24 HOL-MicroJava: theory Conform
18:04:24 HOL-MicroJava: theory Eval
18:04:24 HOL-MicroJava: theory TypeInf
18:04:24 HOL-MicroJava: theory JVMState
18:04:24 HOL-MicroJava: theory JVMInstructions
18:04:25 HOL-MicroJava: theory JVMExceptions
18:04:25 HOL-MicroJava: theory JVMExecInstr
18:04:26 HOL-MicroJava: theory Effect
18:04:26 HOL-MicroJava: theory JVMExec
18:04:27 HOL-MicroJava: theory DefsComp
18:04:27 HOL-MicroJava: theory JVMDefensive
18:04:27 HOL-MicroJava: theory JVMListExample
18:04:27 HOL-MicroJava: theory Index
18:04:27 HOL-MicroJava: theory TranslCompTp
18:04:28 HOL-MicroJava: theory Example
18:04:28 HOL-MicroJava: theory JListExample
18:04:28 HOL-MicroJava: theory JTypeSafe
18:04:28 HOL-MicroJava: theory TranslComp
18:04:29 HOL-MicroJava: theory LemmasComp
18:04:29 HOL-MicroJava: theory CorrComp
18:04:46 HOL-MicroJava: theory BVSpec
18:04:46 HOL-MicroJava: theory EffectMono
18:04:47 HOL-MicroJava: theory Altern
18:04:47 HOL-MicroJava: theory Correct
18:04:47 HOL-MicroJava: theory Typing_Framework_JVM
18:04:47 HOL-MicroJava: theory BVSpecTypeSafe
18:04:47 HOL-MicroJava: theory JVM
18:04:47 HOL-MicroJava: theory LBVJVM
18:04:48 HOL-MicroJava: theory CorrCompTp
18:04:48 HOL-MicroJava: theory BVNoTypeError
18:04:48 HOL-MicroJava: theory BVExample
18:04:50 HOL-MicroJava: theory MicroJava
18:05:25 Timing HOL-MicroJava (6 threads, 71.092s elapsed time, 320.160s cpu time, 17.340s GC time, factor 4.50)
18:05:25 Finished HOL-MicroJava (0:01:12 elapsed time, 0:05:21 cpu time, factor 4.42)
18:05:25 Running HOL-Nominal-Examples ...
18:05:27 HOL-Nominal-Examples: theory CK_Machine
18:05:27 HOL-Nominal-Examples: theory CR_Takahashi
18:05:27 HOL-Nominal-Examples: theory Class1
18:05:27 HOL-Nominal-Examples: theory Compile
18:05:27 HOL-Nominal-Examples: theory Crary
18:05:27 HOL-Nominal-Examples: theory Contexts
18:05:32 HOL-Nominal-Examples: theory Fsub
18:05:32 HOL-Nominal-Examples: theory Height
18:05:35 HOL-Nominal-Examples: theory Lam_Funs
18:05:36 HOL-Nominal-Examples: theory Lambda_mu
18:05:39 HOL-Nominal-Examples: theory CR
18:05:40 HOL-Nominal-Examples: theory SN
18:05:41 HOL-Nominal-Examples: theory LocalWeakening
18:05:41 HOL-Nominal-Examples: theory Pattern
18:05:42 HOL-Nominal-Examples: theory SOS
18:05:43 HOL-Nominal-Examples: theory Standardization
18:05:45 HOL-Nominal-Examples: theory Support
18:05:46 HOL-Nominal-Examples: theory Type_Preservation
18:05:46 HOL-Nominal-Examples: theory W
18:05:47 HOL-Nominal-Examples: theory Weakening
18:08:30 HOL-Nominal-Examples: theory Class2
18:08:33 HOL-Nominal-Examples: theory Class3
18:12:03 HOL-Nominal-Examples: theory VC_Condition
18:12:07 Timing HOL-Nominal-Examples (6 threads, 398.839s elapsed time, 1467.488s cpu time, 139.008s GC time, factor 3.68)
18:12:07 Finished HOL-Nominal-Examples (0:06:40 elapsed time, 0:24:29 cpu time, factor 3.67)
18:12:07 Running HOL-Nonstandard_Analysis-Examples ...
18:12:08 HOL-Nonstandard_Analysis-Examples: theory Multiset
18:12:13 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring
18:12:20 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm
18:12:28 HOL-Nonstandard_Analysis-Examples: theory Primes
18:12:29 HOL-Nonstandard_Analysis-Examples: theory NSPrimes
18:12:32 Timing HOL-Nonstandard_Analysis-Examples (6 threads, 22.994s elapsed time, 65.992s cpu time, 1.704s GC time, factor 2.87)
18:12:32 Finished HOL-Nonstandard_Analysis-Examples (0:00:24 elapsed time, 0:01:07 cpu time, factor 2.73)
18:12:32 Running HOL-Number_Theory ...
18:12:33 HOL-Number_Theory: theory Congruence
18:12:33 HOL-Number_Theory: theory Multiset
18:12:33 HOL-Number_Theory: theory FuncSet
18:12:34 HOL-Number_Theory: theory Lattice
18:12:36 HOL-Number_Theory: theory Group
18:12:38 HOL-Number_Theory: theory FiniteProduct
18:12:38 HOL-Number_Theory: theory Ring
18:12:44 HOL-Number_Theory: theory MiscAlgebra
18:12:44 HOL-Number_Theory: theory Fib
18:12:44 HOL-Number_Theory: theory Factorial_Ring
18:12:51 HOL-Number_Theory: theory Euclidean_Algorithm
18:12:59 HOL-Number_Theory: theory Primes
18:12:59 HOL-Number_Theory: theory Cong
18:12:59 HOL-Number_Theory: theory Eratosthenes
18:13:00 HOL-Number_Theory: theory Residues
18:13:02 HOL-Number_Theory: theory Gauss
18:13:02 HOL-Number_Theory: theory Pocklington
18:13:02 HOL-Number_Theory: theory Number_Theory
18:13:09 Timing HOL-Number_Theory (6 threads, 35.787s elapsed time, 142.752s cpu time, 3.352s GC time, factor 3.99)
18:13:09 Finished HOL-Number_Theory (0:00:37 elapsed time, 0:02:24 cpu time, factor 3.85)
18:13:09 Running HOL-Predicate_Compile_Examples ...
18:13:11 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs
18:13:11 HOL-Predicate_Compile_Examples: theory Examples
18:13:11 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck
18:13:11 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests
18:13:11 HOL-Predicate_Compile_Examples: theory Specialisation_Examples
18:13:12 HOL-Predicate_Compile_Examples: theory IMP_1
18:13:12 HOL-Predicate_Compile_Examples: theory IMP_2
18:13:12 HOL-Predicate_Compile_Examples: theory IMP_3
18:13:13 HOL-Predicate_Compile_Examples: theory IMP_4
18:13:13 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples
18:13:58 HOL-Predicate_Compile_Examples: theory Code_Prolog
18:13:58 HOL-Predicate_Compile_Examples: theory Hotel_Example
18:13:59 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples
18:13:59 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example
18:13:59 HOL-Predicate_Compile_Examples: theory Lambda_Example
18:13:59 HOL-Predicate_Compile_Examples: theory List_Examples
18:14:01 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog
18:14:02 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example
18:14:08 Timing HOL-Predicate_Compile_Examples (6 threads, 57.246s elapsed time, 172.248s cpu time, 17.816s GC time, factor 3.01)
18:14:08 Finished HOL-Predicate_Compile_Examples (0:00:58 elapsed time, 0:04:44 cpu time, factor 4.83)
18:14:08 Running HOL-Probability-ex ...
18:14:13 HOL-Probability-ex: theory Dining_Cryptographers
18:14:13 HOL-Probability-ex: theory Measure_Not_CCC
18:14:13 HOL-Probability-ex: theory Koepf_Duermuth_Countermeasure
18:14:42 Timing HOL-Probability-ex (6 threads, 28.624s elapsed time, 59.208s cpu time, 0.904s GC time, factor 2.07)
18:14:42 Finished HOL-Probability-ex (0:00:33 elapsed time, 0:01:03 cpu time, factor 1.92)
18:14:42 Running HOL-Proofs-Extraction ...
18:14:44 HOL-Proofs-Extraction: theory Adhoc_Overloading
18:14:44 HOL-Proofs-Extraction: theory Binomial
18:14:44 HOL-Proofs-Extraction: theory Code_Abstract_Nat
18:14:44 HOL-Proofs-Extraction: theory GCD
18:14:44 HOL-Proofs-Extraction: theory Multiset
18:14:44 HOL-Proofs-Extraction: theory Monad_Syntax
18:14:44 HOL-Proofs-Extraction: theory Code_Target_Nat
18:14:44 HOL-Proofs-Extraction: theory State_Monad
18:15:04 HOL-Proofs-Extraction: theory Code_Target_Int
18:15:04 HOL-Proofs-Extraction: theory Code_Target_Numeral
18:15:40 HOL-Proofs-Extraction: theory Factorial_Ring
18:16:11 HOL-Proofs-Extraction: theory Euclidean_Algorithm
18:16:29 HOL-Proofs-Extraction: theory Primes
18:19:59 HOL-Proofs-Extraction: theory Util
18:19:59 HOL-Proofs-Extraction: theory Warshall
18:19:59 HOL-Proofs-Extraction: theory Higman
18:20:01 HOL-Proofs-Extraction: theory Euclid
18:20:01 HOL-Proofs-Extraction: theory Pigeonhole
18:20:01 HOL-Proofs-Extraction: theory QuotRem
18:20:03 HOL-Proofs-Extraction: theory Higman_Extraction
18:20:06 HOL-Proofs-Extraction: theory Greatest_Common_Divisor
18:20:47 Timing HOL-Proofs-Extraction (6 threads, 362.840s elapsed time, 918.836s cpu time, 60.600s GC time, factor 2.53)
18:20:47 Finished HOL-Proofs-Extraction (0:06:04 elapsed time, 0:15:20 cpu time, factor 2.52)
18:20:47 Running HOL-Proofs-Lambda ...
18:20:49 HOL-Proofs-Lambda: theory GCD
18:21:08 HOL-Proofs-Lambda: theory Code_Target_Int
18:21:41 HOL-Proofs-Lambda: theory Commutation
18:21:41 HOL-Proofs-Lambda: theory Lambda
18:21:41 HOL-Proofs-Lambda: theory ListOrder
18:21:44 HOL-Proofs-Lambda: theory ListApplication
18:21:44 HOL-Proofs-Lambda: theory ParRed
18:21:44 HOL-Proofs-Lambda: theory LambdaType
18:21:44 HOL-Proofs-Lambda: theory ListBeta
18:21:45 HOL-Proofs-Lambda: theory Eta
18:21:45 HOL-Proofs-Lambda: theory InductTermi
18:21:46 HOL-Proofs-Lambda: theory NormalForm
18:21:46 HOL-Proofs-Lambda: theory StrongNorm
18:21:47 HOL-Proofs-Lambda: theory Standardization
18:21:47 HOL-Proofs-Lambda: theory WeakNorm
18:23:59 Timing HOL-Proofs-Lambda (6 threads, 190.433s elapsed time, 331.704s cpu time, 10.468s GC time, factor 1.74)
18:23:59 Finished HOL-Proofs-Lambda (0:03:12 elapsed time, 0:05:33 cpu time, factor 1.73)
18:24:00 Running HOL-Quickcheck_Benchmark ...
18:24:01 HOL-Quickcheck_Benchmark: theory Predicate_Compile_Alternative_Defs
18:24:01 HOL-Quickcheck_Benchmark: theory Find_Unused_Assms_Examples
18:24:02 HOL-Quickcheck_Benchmark: theory Predicate_Compile_Quickcheck
18:24:02 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Base
18:24:06 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Guided_Attacker_Example
18:24:06 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_No_Attacker_Example
18:24:07 HOL-Quickcheck_Benchmark: theory Needham_Schroeder_Unguided_Attacker_Example
18:28:18 Timing HOL-Quickcheck_Benchmark (6 threads, 255.762s elapsed time, 1099.616s cpu time, 111.776s GC time, factor 4.30)
18:28:18 Finished HOL-Quickcheck_Benchmark (0:04:17 elapsed time, 0:18:49 cpu time, factor 4.38)
18:28:18 Running HOL-Quickcheck_Examples ...
18:28:19 HOL-Quickcheck_Examples: theory AList
18:28:19 HOL-Quickcheck_Examples: theory Completeness
18:28:19 HOL-Quickcheck_Examples: theory Multiset
18:28:19 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces
18:28:19 HOL-Quickcheck_Examples: theory Dlist
18:28:19 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples
18:28:19 HOL-Quickcheck_Examples: theory Quickcheck_Nesting
18:28:20 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example
18:28:21 HOL-Quickcheck_Examples: theory DAList
18:28:24 HOL-Quickcheck_Examples: theory DAList_Multiset
18:28:25 HOL-Quickcheck_Examples: theory Quickcheck_Examples
18:28:54 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs
18:28:54 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples
18:28:55 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck
18:28:55 HOL-Quickcheck_Examples: theory Hotel_Example
18:29:50 Timing HOL-Quickcheck_Examples (6 threads, 89.950s elapsed time, 204.900s cpu time, 14.252s GC time, factor 2.28)
18:29:50 Finished HOL-Quickcheck_Examples (0:01:31 elapsed time, 0:04:55 cpu time, factor 3.23)
18:29:50 Running HOL-Quotient_Examples ...
18:29:51 HOL-Quotient_Examples: theory Lift_Set
18:29:51 HOL-Quotient_Examples: theory Congruence
18:29:51 HOL-Quotient_Examples: theory FuncSet
18:29:51 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test
18:29:51 HOL-Quotient_Examples: theory Lift_FSet
18:29:51 HOL-Quotient_Examples: theory Lift_DList
18:29:52 HOL-Quotient_Examples: theory Multiset
18:29:52 HOL-Quotient_Examples: theory Quotient_Syntax
18:29:52 HOL-Quotient_Examples: theory Lift_Fun
18:29:52 HOL-Quotient_Examples: theory Quotient_Message
18:29:52 HOL-Quotient_Examples: theory Quotient_Option
18:29:52 HOL-Quotient_Examples: theory Quotient_Product
18:29:52 HOL-Quotient_Examples: theory Lattice
18:29:53 HOL-Quotient_Examples: theory Quotient_Int
18:29:53 HOL-Quotient_Examples: theory Quotient_Rat
18:29:53 HOL-Quotient_Examples: theory Quotient_Set
18:29:54 HOL-Quotient_Examples: theory Quotient_List
18:29:54 HOL-Quotient_Examples: theory DList
18:29:55 HOL-Quotient_Examples: theory Group
18:29:56 HOL-Quotient_Examples: theory Int_Pow
18:29:57 HOL-Quotient_Examples: theory Quotient_FSet
18:30:23 Timing HOL-Quotient_Examples (6 threads, 31.711s elapsed time, 87.748s cpu time, 3.548s GC time, factor 2.77)
18:30:23 Finished HOL-Quotient_Examples (0:00:33 elapsed time, 0:02:26 cpu time, factor 4.38)
18:30:23 Running HOL-Record_Benchmark ...
18:30:25 HOL-Record_Benchmark: theory Record_Benchmark
18:32:33 Timing HOL-Record_Benchmark (6 threads, 127.694s elapsed time, 209.872s cpu time, 17.752s GC time, factor 1.64)
18:32:33 Finished HOL-Record_Benchmark (0:02:09 elapsed time, 0:03:31 cpu time, factor 1.63)
18:32:33 Running HOL-SET_Protocol ...
18:32:34 HOL-SET_Protocol: theory Nat_Bijection
18:32:35 HOL-SET_Protocol: theory Message_SET
18:32:39 HOL-SET_Protocol: theory Event_SET
18:32:40 HOL-SET_Protocol: theory Public_SET
18:32:40 HOL-SET_Protocol: theory Cardholder_Registration
18:32:40 HOL-SET_Protocol: theory Merchant_Registration
18:32:40 HOL-SET_Protocol: theory Purchase
18:32:42 HOL-SET_Protocol: theory SET_Protocol
18:32:56 Timing HOL-SET_Protocol (6 threads, 21.114s elapsed time, 90.724s cpu time, 1.720s GC time, factor 4.30)
18:32:56 Finished HOL-SET_Protocol (0:00:22 elapsed time, 0:01:32 cpu time, factor 4.06)
18:32:56 Running HOL-UNITY ...
18:32:58 HOL-UNITY: theory ListOrder
18:32:58 HOL-UNITY: theory Multiset
18:32:58 HOL-UNITY: theory UNITY
18:32:59 HOL-UNITY: theory Constrains
18:32:59 HOL-UNITY: theory Deadlock
18:32:59 HOL-UNITY: theory FP
18:32:59 HOL-UNITY: theory Network
18:32:59 HOL-UNITY: theory WFair
18:32:59 HOL-UNITY: theory SubstAx
18:32:59 HOL-UNITY: theory Token
18:33:00 HOL-UNITY: theory Detects
18:33:00 HOL-UNITY: theory Union
18:33:01 HOL-UNITY: theory Comp
18:33:01 HOL-UNITY: theory Guar
18:33:01 HOL-UNITY: theory Transformers
18:33:01 HOL-UNITY: theory Extend
18:33:02 HOL-UNITY: theory ProgressSets
18:33:02 HOL-UNITY: theory Project
18:33:02 HOL-UNITY: theory Rename
18:33:03 HOL-UNITY: theory Lift_prog
18:33:03 HOL-UNITY: theory ELT
18:33:03 HOL-UNITY: theory Multiset_Order
18:33:03 HOL-UNITY: theory Follows
18:33:03 HOL-UNITY: theory PPROD
18:33:04 HOL-UNITY: theory UNITY_Main
18:33:04 HOL-UNITY: theory AllocBase
18:33:04 HOL-UNITY: theory Channel
18:33:04 HOL-UNITY: theory Alloc
18:33:05 HOL-UNITY: theory AllocImpl
18:33:05 HOL-UNITY: theory Client
18:33:06 HOL-UNITY: theory Common
18:33:06 HOL-UNITY: theory Counter
18:33:06 HOL-UNITY: theory Counterc
18:33:07 HOL-UNITY: theory Handshake
18:33:07 HOL-UNITY: theory Lift
18:33:07 HOL-UNITY: theory Mutex
18:33:07 HOL-UNITY: theory NSP_Bad
18:33:07 HOL-UNITY: theory PriorityAux
18:33:08 HOL-UNITY: theory Progress
18:33:08 HOL-UNITY: theory Priority
18:33:08 HOL-UNITY: theory Reach
18:33:08 HOL-UNITY: theory TimerArray
18:33:08 HOL-UNITY: theory Reachability
18:33:20 Timing HOL-UNITY (6 threads, 22.162s elapsed time, 113.560s cpu time, 3.812s GC time, factor 5.12)
18:33:20 Finished HOL-UNITY (0:00:24 elapsed time, 0:01:55 cpu time, factor 4.74)
18:33:20 Running HOL-Word-SMT_Examples ...
18:33:22 HOL-Word-SMT_Examples: theory SMT_Word_Examples
18:33:22 HOL-Word-SMT_Examples: theory Boogie
18:33:22 HOL-Word-SMT_Examples: theory SMT_Tests
18:33:22 HOL-Word-SMT_Examples: theory SMT_Examples
18:34:25 Timing HOL-Word-SMT_Examples (6 threads, 62.321s elapsed time, 80.848s cpu time, 0.768s GC time, factor 1.30)
18:34:25 Finished HOL-Word-SMT_Examples (0:01:04 elapsed time, 0:01:25 cpu time, factor 1.33)
18:34:25 Running IOA ...
18:34:27 IOA: theory Asig
18:34:27 IOA: theory Seq
18:34:27 IOA: theory Pred
18:34:27 IOA: theory Automata
18:34:28 IOA: theory Sequence
18:34:29 IOA: theory Traces
18:34:29 IOA: theory TL
18:34:30 IOA: theory CompoExecs
18:34:30 IOA: theory RefMappings
18:34:30 IOA: theory ShortExecutions
18:34:30 IOA: theory RefCorrectness
18:34:30 IOA: theory CompoScheds
18:34:31 IOA: theory Simulations
18:34:31 IOA: theory SimCorrectness
18:34:31 IOA: theory Deadlock
18:34:31 IOA: theory CompoTraces
18:34:32 IOA: theory Compositionality
18:34:33 IOA: theory IOA
18:34:33 IOA: theory TLS
18:34:34 IOA: theory LiveIOA
18:34:34 IOA: theory Abstraction
18:34:35 Timing IOA (6 threads, 8.286s elapsed time, 34.196s cpu time, 0.924s GC time, factor 4.13)
18:34:35 Finished IOA (0:00:10 elapsed time, 0:00:36 cpu time, factor 3.50)
18:34:35 Running ZF-UNITY ...
18:34:36 ZF-UNITY: theory Acc
18:34:36 ZF-UNITY: theory FoldSet
18:34:36 ZF-UNITY: theory GenPrefix
18:34:36 ZF-UNITY: theory State
18:34:36 ZF-UNITY: theory UNITY
18:34:36 ZF-UNITY: theory Multiset
18:34:36 ZF-UNITY: theory Constrains
18:34:36 ZF-UNITY: theory FP
18:34:36 ZF-UNITY: theory WFair
18:34:37 ZF-UNITY: theory SubstAx
18:34:37 ZF-UNITY: theory MultisetSum
18:34:37 ZF-UNITY: theory Mutex
18:34:37 ZF-UNITY: theory Union
18:34:37 ZF-UNITY: theory Monotonicity
18:34:37 ZF-UNITY: theory Increasing
18:34:37 ZF-UNITY: theory Follows
18:34:37 ZF-UNITY: theory Comp
18:34:38 ZF-UNITY: theory Guar
18:34:38 ZF-UNITY: theory AllocBase
18:34:38 ZF-UNITY: theory ClientImpl
18:34:38 ZF-UNITY: theory Distributor
18:34:38 ZF-UNITY: theory Merge
18:34:38 ZF-UNITY: theory AllocImpl
18:34:42 Timing ZF-UNITY (6 threads, 5.928s elapsed time, 29.560s cpu time, 0.940s GC time, factor 4.99)
18:34:42 Finished ZF-UNITY (0:00:06 elapsed time, 0:00:29 cpu time, factor 4.75)
18:34:42 
18:34:42 === TIMING ===
18:34:42 
18:34:42 Group main: 0:14:47 elapsed time, 0:55:07 cpu time, factor 3.73
18:34:42 Group timing: 1:12:20 elapsed time, 4:00:48 cpu time, factor 3.33
18:34:42 Group ZF: 0:00:21 elapsed time, 0:01:13 cpu time, factor 3.35
18:34:42 Overall: 1:33:51 elapsed time, 5:05:36 cpu time, factor 3.26
18:34:42 Archiving artifacts
18:34:42 No emails were triggered.
18:34:42 Finished: SUCCESS