Skipping 811 KB.. Full Log

Efficient-Mergesort: theory Efficient-Mergesort.Natural_Mergesort
03:20:47 Preparing Quaternions/document ...
03:20:47 HOL-Combinatorics: theory HOL-Combinatorics.Combinatorics
03:20:48 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.SequentialComposition
03:20:49 Preparing Kuratowski_Closure_Complement/document ...
03:20:50 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.Counterexamples
03:20:50 Preparing Fishburn_Impossibility/document ...
03:20:51 Finished Quaternions/document (0:00:03 elapsed time)
03:20:51 Preparing Quaternions/outline ...
03:20:54 Finished Kuratowski_Closure_Complement/document (0:00:04 elapsed time)
03:20:54 Preparing Kuratowski_Closure_Complement/outline ...
03:20:54 Finished Quaternions/outline (0:00:03 elapsed time)
03:20:54 Timing Quaternions (4 threads, 24.058s elapsed time, 31.143s cpu time, 1.070s GC time, factor 1.29)
03:20:54 Finished Quaternions (0:00:28 elapsed time, 0:00:34 cpu time, factor 1.24)
03:20:54 Building HOL-SPARK-Examples ...
03:20:54 Finished Fishburn_Impossibility/document (0:00:03 elapsed time)
03:20:54 Preparing Fishburn_Impossibility/outline ...
03:20:54 Preparing Abstract_Completeness/document ...
03:20:54 Preparing Knuth_Morris_Pratt/document ...
03:20:56 Preparing Efficient-Mergesort/document ...
03:20:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence
03:20:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD
03:20:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor
03:20:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt
03:20:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas
03:20:57 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
03:20:57 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
03:20:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification
03:20:57 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
03:20:57 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
03:20:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F
03:20:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash
03:20:58 Finished Fishburn_Impossibility/outline (0:00:03 elapsed time)
03:20:58 Finished Abstract_Completeness/document (0:00:03 elapsed time)
03:20:58 Preparing Abstract_Completeness/outline ...
03:20:58 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L
03:20:58 Timing Fishburn_Impossibility (4 threads, 23.562s elapsed time, 87.019s cpu time, 2.696s GC time, factor 3.69)
03:20:58 Finished Fishburn_Impossibility (0:00:26 elapsed time, 0:01:29 cpu time, factor 3.42)
03:20:58 Running TESL_Language ...
03:20:58 Finished Kuratowski_Closure_Complement/outline (0:00:04 elapsed time)
03:20:58 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
03:20:58 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
03:20:58 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
03:20:58 Timing Kuratowski_Closure_Complement (4 threads, 23.150s elapsed time, 66.991s cpu time, 1.576s GC time, factor 2.89)
03:20:58 Finished Kuratowski_Closure_Complement (0:00:27 elapsed time, 0:01:10 cpu time, factor 2.61)
03:20:58 Running Program-Conflict-Analysis ...
03:20:58 Finished Knuth_Morris_Pratt/document (0:00:03 elapsed time)
03:20:58 Preparing Knuth_Morris_Pratt/outline ...
03:20:59 Preparing Weight_Balanced_Trees/document ...
03:20:59 Finished Efficient-Mergesort/document (0:00:03 elapsed time)
03:20:59 Preparing Efficient-Mergesort/outline ...
03:21:00 TESL_Language: theory TESL_Language.TESL
03:21:00 TESL_Language: theory TESL_Language.Introduction
03:21:00 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R
03:21:00 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round
03:21:01 Finished Abstract_Completeness/outline (0:00:03 elapsed time)
03:21:01 Timing Abstract_Completeness (4 threads, 10.351s elapsed time, 22.432s cpu time, 0.581s GC time, factor 2.17)
03:21:01 Finished Abstract_Completeness (0:00:34 elapsed time, 0:00:59 cpu time, factor 1.74)
03:21:01 Running FOL_Harrison ...
03:21:02 Program-Conflict-Analysis: theory Program-Conflict-Analysis.Misc
03:21:02 Finished Knuth_Morris_Pratt/outline (0:00:03 elapsed time)
03:21:02 Finished Efficient-Mergesort/outline (0:00:03 elapsed time)
03:21:02 Timing Efficient-Mergesort (4 threads, 19.880s elapsed time, 59.160s cpu time, 2.308s GC time, factor 2.98)
03:21:02 Finished Efficient-Mergesort (0:00:22 elapsed time, 0:01:01 cpu time, factor 2.73)
03:21:02 Timing Knuth_Morris_Pratt (4 threads, 21.770s elapsed time, 74.732s cpu time, 1.449s GC time, factor 3.43)
03:21:02 Finished Knuth_Morris_Pratt (0:00:26 elapsed time, 0:01:19 cpu time, factor 2.95)
03:21:02 Running Sliding_Window_Algorithm ...
03:21:02 Running Formal_Puiseux_Series ...
03:21:02 Finished Weight_Balanced_Trees/document (0:00:03 elapsed time)
03:21:02 Preparing Weight_Balanced_Trees/outline ...
03:21:02 Program-Conflict-Analysis: theory Program-Conflict-Analysis.Interleave
03:21:03 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L
03:21:03 FOL_Harrison: theory FOL_Harrison.FOL_Harrison
03:21:04 TESL_Language: theory TESL_Language.Run
03:21:04 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R
03:21:04 TESL_Language: theory TESL_Language.Denotational
03:21:04 TESL_Language: theory TESL_Language.SymbolicPrimitive
03:21:04 Sliding_Window_Algorithm: theory Sliding_Window_Algorithm.SWA
03:21:04 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L
03:21:05 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
03:21:05 TESL_Language: theory TESL_Language.StutteringDefs
03:21:05 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R
03:21:06 Finished Weight_Balanced_Trees/outline (0:00:03 elapsed time)
03:21:06 Timing Weight_Balanced_Trees (4 threads, 17.950s elapsed time, 46.302s cpu time, 1.957s GC time, factor 2.58)
03:21:06 Finished Weight_Balanced_Trees (0:00:20 elapsed time, 0:00:48 cpu time, factor 2.36)
03:21:06 Running IMAP-CRDT ...
03:21:06 TESL_Language: theory TESL_Language.StutteringLemmas
03:21:06 Program-Conflict-Analysis: theory Program-Conflict-Analysis.LTS
03:21:06 Program-Conflict-Analysis: theory Program-Conflict-Analysis.Flowgraph
03:21:06 Program-Conflict-Analysis: theory Program-Conflict-Analysis.ConsInterleave
03:21:06 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Unsorted
03:21:06 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Laurent_Library
03:21:06 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom
03:21:06 Program-Conflict-Analysis: theory Program-Conflict-Analysis.ThreadTracking
03:21:07 Preparing Noninterference_Sequential_Composition/document ...
03:21:07 TESL_Language: theory TESL_Language.Stuttering
03:21:07 Program-Conflict-Analysis: theory Program-Conflict-Analysis.AcquisitionHistory
03:21:07 Preparing HOL-Combinatorics/document ...
03:21:08 IMAP-CRDT: theory IMAP-CRDT.IMAP-def
03:21:08 Program-Conflict-Analysis: theory Program-Conflict-Analysis.Semantics
03:21:09 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Polynomial
03:21:09 TESL_Language: theory TESL_Language.Operational
03:21:10 TESL_Language: theory TESL_Language.Corecursive_Prop
03:21:11 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-commute
03:21:11 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-helpers
03:21:11 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
03:21:12 TESL_Language: theory TESL_Language.Hygge_Theory
03:21:12 TESL_Language: theory TESL_Language.Config_Morphisms
03:21:12 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom_Poly
03:21:12 Program-Conflict-Analysis: theory Program-Conflict-Analysis.Normalization
03:21:13 Finished HOL-Combinatorics/document (0:00:06 elapsed time)
03:21:13 Preparing HOL-Combinatorics/outline ...
03:21:14 Program-Conflict-Analysis: theory Program-Conflict-Analysis.ConstraintSystems
03:21:15 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-independent
03:21:15 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Polynomial_Library
03:21:17 Program-Conflict-Analysis: theory Program-Conflict-Analysis.MainResult
03:21:17 Formal_Puiseux_Series: theory Formal_Puiseux_Series.FPS_Hensel
03:21:17 Finished HOL-Combinatorics/outline (0:00:03 elapsed time)
03:21:17 Timing HOL-Combinatorics (4 threads, 19.744s elapsed time, 71.058s cpu time, 2.384s GC time, factor 3.60)
03:21:17 Finished HOL-Combinatorics (0:00:35 elapsed time, 0:01:36 cpu time, factor 2.70)
03:21:17 Running AVL-Trees ...
03:21:18 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof
03:21:18 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Formal_Puiseux_Series
03:21:18 Finished Noninterference_Sequential_Composition/document (0:00:11 elapsed time)
03:21:18 Preparing Noninterference_Sequential_Composition/outline ...
03:21:19 Preparing Cubic_Quartic_Equations/document ...
03:21:20 AVL-Trees: theory AVL-Trees.AVL2
03:21:20 AVL-Trees: theory AVL-Trees.AVL
03:21:23 Finished Noninterference_Sequential_Composition/outline (0:00:04 elapsed time)
03:21:23 Preparing TESL_Language/document ...
03:21:23 Timing Noninterference_Sequential_Composition (4 threads, 13.952s elapsed time, 48.828s cpu time, 2.123s GC time, factor 3.50)
03:21:23 Finished Noninterference_Sequential_Composition (0:00:34 elapsed time, 0:01:13 cpu time, factor 2.13)
03:21:23 Running Polynomial_Interpolation ...
03:21:23 Preparing Program-Conflict-Analysis/document ...
03:21:24 Preparing Sliding_Window_Algorithm/document ...
03:21:24 Preparing FOL_Harrison/document ...
03:21:25 Preparing Formal_Puiseux_Series/document ...
03:21:26 Finished Cubic_Quartic_Equations/document (0:00:06 elapsed time)
03:21:26 Preparing Cubic_Quartic_Equations/outline ...
03:21:27 Finished FOL_Harrison/document (0:00:02 elapsed time)
03:21:27 Preparing FOL_Harrison/outline ...
03:21:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Improved_Code_Equations
03:21:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Unsorted
03:21:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
03:21:27 Polynomial_Interpolation: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
03:21:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Divmod_Int
03:21:27 Preparing IMAP-CRDT/document ...
03:21:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom
03:21:28 Finished Sliding_Window_Algorithm/document (0:00:03 elapsed time)
03:21:28 Preparing Sliding_Window_Algorithm/outline ...
03:21:28 Polynomial_Interpolation: theory Polynomial_Interpolation.Is_Rat_To_Rat
03:21:29 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Polynomial
03:21:29 Finished FOL_Harrison/outline (0:00:02 elapsed time)
03:21:29 Timing FOL_Harrison (4 threads, 19.558s elapsed time, 44.951s cpu time, 0.685s GC time, factor 2.30)
03:21:29 Finished FOL_Harrison (0:00:22 elapsed time, 0:00:47 cpu time, factor 2.12)
03:21:29 Running Complete_Non_Orders ...
03:21:30 Finished Cubic_Quartic_Equations/outline (0:00:04 elapsed time)
03:21:30 Polynomial_Interpolation: theory Polynomial_Interpolation.Lagrange_Interpolation
03:21:31 Timing HOL-SPARK-Examples (4 threads, 20.716s elapsed time, 39.240s cpu time, 0.935s GC time, factor 1.89)
03:21:31 Finished HOL-SPARK-Examples (0:00:35 elapsed time, 0:01:02 cpu time, factor 1.76)
03:21:31 Timing Cubic_Quartic_Equations (4 threads, 20.951s elapsed time, 50.463s cpu time, 2.050s GC time, factor 2.41)
03:21:31 Finished Cubic_Quartic_Equations (0:00:32 elapsed time, 0:01:01 cpu time, factor 1.89)
03:21:31 Building Random_BSTs ...
03:21:31 Running FLP ...
03:21:31 Complete_Non_Orders: theory Complete_Non_Orders.Binary_Relations
03:21:31 Finished TESL_Language/document (0:00:07 elapsed time)
03:21:31 Preparing TESL_Language/outline ...
03:21:31 Finished Sliding_Window_Algorithm/outline (0:00:03 elapsed time)
03:21:31 Timing Sliding_Window_Algorithm (4 threads, 18.689s elapsed time, 57.603s cpu time, 0.895s GC time, factor 3.08)
03:21:31 Finished Sliding_Window_Algorithm (0:00:21 elapsed time, 0:00:59 cpu time, factor 2.81)
03:21:31 Running OpSets ...
03:21:31 Finished IMAP-CRDT/document (0:00:04 elapsed time)
03:21:31 Preparing IMAP-CRDT/outline ...
03:21:32 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom_Poly
03:21:32 Finished Formal_Puiseux_Series/document (0:00:07 elapsed time)
03:21:32 Preparing Formal_Puiseux_Series/outline ...
03:21:32 FLP: theory FLP.Multiset
03:21:32 FLP: theory FLP.ListUtilities
03:21:32 FLP: theory FLP.AsynchronousSystem
03:21:33 Finished Program-Conflict-Analysis/document (0:00:09 elapsed time)
03:21:33 Preparing Program-Conflict-Analysis/outline ...
03:21:33 OpSets: theory OpSets.OpSet
03:21:34 OpSets: theory OpSets.Insert_Spec
03:21:34 Polynomial_Interpolation: theory Polynomial_Interpolation.Newton_Interpolation
03:21:35 OpSets: theory OpSets.Interleaving
03:21:35 OpSets: theory OpSets.List_Spec
03:21:35 OpSets: theory OpSets.RGA
03:21:35 Random_BSTs: theory HOL-Data_Structures.Less_False
03:21:35 Random_BSTs: theory HOL-Data_Structures.Cmp
03:21:35 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
03:21:35 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
03:21:35 Finished IMAP-CRDT/outline (0:00:03 elapsed time)
03:21:35 Random_BSTs: theory HOL-Data_Structures.Set_Specs
03:21:36 Random_BSTs: theory HOL-Data_Structures.Tree_Set
03:21:36 Timing IMAP-CRDT (4 threads, 18.486s elapsed time, 49.218s cpu time, 2.045s GC time, factor 2.66)
03:21:36 Finished IMAP-CRDT (0:00:21 elapsed time, 0:00:51 cpu time, factor 2.43)
03:21:36 Running Finger-Trees ...
03:21:36 FLP: theory FLP.Execution
03:21:36 FLP: theory FLP.FLPSystem
03:21:36 Finished TESL_Language/outline (0:00:05 elapsed time)
03:21:36 Timing TESL_Language (4 threads, 22.319s elapsed time, 72.968s cpu time, 2.454s GC time, factor 3.27)
03:21:36 Finished TESL_Language (0:00:24 elapsed time, 0:01:15 cpu time, factor 3.04)
03:21:36 Running Optics ...
03:21:37 FLP: theory FLP.FLPTheorem
03:21:37 Random_BSTs: theory Random_BSTs.Random_BSTs
03:21:37 Preparing AVL-Trees/document ...
03:21:37 Finished Formal_Puiseux_Series/outline (0:00:05 elapsed time)
03:21:38 Timing Formal_Puiseux_Series (4 threads, 17.702s elapsed time, 58.514s cpu time, 1.576s GC time, factor 3.31)
03:21:38 Finished Formal_Puiseux_Series (0:00:22 elapsed time, 0:01:02 cpu time, factor 2.81)
03:21:38 Running Finitely_Generated_Abelian_Groups ...
03:21:38 Polynomial_Interpolation: theory Polynomial_Interpolation.Polynomial_Interpolation
03:21:38 Optics: theory Optics.Two
03:21:38 Optics: theory Optics.Interp
03:21:38 Optics: theory Optics.Lens_Laws
03:21:38 FLP: theory FLP.FLPExistingSystem
03:21:39 Finished Program-Conflict-Analysis/outline (0:00:05 elapsed time)
03:21:39 Finger-Trees: theory Finger-Trees.FingerTree
03:21:39 Timing Program-Conflict-Analysis (4 threads, 20.114s elapsed time, 74.422s cpu time, 2.635s GC time, factor 3.70)
03:21:39 Finished Program-Conflict-Analysis (0:00:24 elapsed time, 0:01:18 cpu time, factor 3.23)
03:21:39 Running SenSocialChoice ...
03:21:39 Optics: theory Optics.Lens_Algebra
03:21:40 Finished AVL-Trees/document (0:00:02 elapsed time)
03:21:40 Preparing AVL-Trees/outline ...
03:21:40 Optics: theory Optics.Lens_Order
03:21:41 Optics: theory Optics.Lens_Symmetric
03:21:41 Optics: theory Optics.Lens_Instances
03:21:41 SenSocialChoice: theory SenSocialChoice.FSext
03:21:42 SenSocialChoice: theory SenSocialChoice.RPRs
03:21:42 Finished AVL-Trees/outline (0:00:02 elapsed time)
03:21:42 SenSocialChoice: theory SenSocialChoice.SCFs
03:21:42 Timing AVL-Trees (4 threads, 16.970s elapsed time, 67.180s cpu time, 1.489s GC time, factor 3.96)
03:21:42 Finished AVL-Trees (0:00:19 elapsed time, 0:01:09 cpu time, factor 3.53)
03:21:42 Running Finite_Automata_HF ...
03:21:42 Optics: theory Optics.Scenes
03:21:42 SenSocialChoice: theory SenSocialChoice.Arrow
03:21:43 SenSocialChoice: theory SenSocialChoice.May
03:21:43 Optics: theory Optics.Lenses
03:21:43 Optics: theory Optics.Prisms
03:21:43 SenSocialChoice: theory SenSocialChoice.Sen
03:21:43 Complete_Non_Orders: theory Complete_Non_Orders.Complete_Relations
03:21:43 Preparing Polynomial_Interpolation/document ...
03:21:43 Optics: theory Optics.Channel_Type
03:21:43 Optics: theory Optics.Dataspace
03:21:44 Optics: theory Optics.Optics
03:21:44 Complete_Non_Orders: theory Complete_Non_Orders.Fixed_Points
03:21:44 Finite_Automata_HF: theory Regular-Sets.Regular_Set
03:21:44 Finite_Automata_HF: theory HOL-Library.Nat_Bijection
03:21:44 Complete_Non_Orders: theory Complete_Non_Orders.Kleene_Fixed_Point
03:21:45 Finite_Automata_HF: theory HereditarilyFinite.HF
03:21:45 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
03:21:45 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
03:21:46 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom
03:21:46 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
03:21:47 Finite_Automata_HF: theory HereditarilyFinite.Ordinal
03:21:47 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
03:21:48 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
03:21:48 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds
03:21:49 Finite_Automata_HF: theory Regular-Sets.Regular_Exp
03:21:50 Preparing Complete_Non_Orders/document ...
03:21:50 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
03:21:50 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds
03:21:50 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations
03:21:51 Optics: theory Optics.Lens_Record_Example
03:21:51 Preparing OpSets/document ...
03:21:52 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
03:21:52 Preparing FLP/document ...
03:21:53 Finished Polynomial_Interpolation/document (0:00:09 elapsed time)
03:21:53 Preparing Polynomial_Interpolation/outline ...
03:21:53 Finite_Automata_HF: theory Finite_Automata_HF.Finite_Automata_HF
03:21:55 Finger-Trees: theory Finger-Trees.Test
03:21:55 Optics: theory HOL-Library.Adhoc_Overloading
03:21:55 Optics: theory HOL-Library.Monad_Syntax
03:21:55 Optics: theory HOL-Library.State_Monad
03:21:56 Optics: theory Optics.Lens_State
03:21:57 Preparing Optics/document ...
03:21:58 Finished FLP/document (0:00:05 elapsed time)
03:21:58 Preparing FLP/outline ...
03:21:58 Finished Polynomial_Interpolation/outline (0:00:05 elapsed time)
03:21:58 Preparing Finger-Trees/document ...
03:21:58 Finished Complete_Non_Orders/document (0:00:08 elapsed time)
03:21:58 Preparing Complete_Non_Orders/outline ...
03:21:58 Timing Polynomial_Interpolation (4 threads, 15.550s elapsed time, 57.659s cpu time, 1.944s GC time, factor 3.71)
03:21:58 Finished Polynomial_Interpolation (0:00:19 elapsed time, 0:01:01 cpu time, factor 3.10)
03:21:58 Running IMP2_Binary_Heap ...
03:21:59 Finished OpSets/document (0:00:07 elapsed time)
03:21:59 Preparing OpSets/outline ...
03:22:00 Preparing SenSocialChoice/document ...
03:22:00 IMP2_Binary_Heap: theory IMP2_Binary_Heap.IMP2_Binary_Heap
03:22:00 Preparing Finite_Automata_HF/document ...
03:22:01 Finished FLP/outline (0:00:03 elapsed time)
03:22:02 Timing FLP (4 threads, 18.016s elapsed time, 51.685s cpu time, 1.808s GC time, factor 2.87)
03:22:02 Finished FLP (0:00:20 elapsed time, 0:00:53 cpu time, factor 2.63)
03:22:02 Running Binomial-Heaps ...
03:22:03 Finished Finite_Automata_HF/document (0:00:02 elapsed time)
03:22:03 Preparing Finite_Automata_HF/outline ...
03:22:03 Finished Finger-Trees/document (0:00:05 elapsed time)
03:22:03 Preparing Finger-Trees/outline ...
03:22:03 Preparing Finitely_Generated_Abelian_Groups/document ...
03:22:03 Finished OpSets/outline (0:00:04 elapsed time)
03:22:04 Timing OpSets (4 threads, 17.266s elapsed time, 56.329s cpu time, 1.303s GC time, factor 3.26)
03:22:04 Finished OpSets (0:00:19 elapsed time, 0:00:58 cpu time, factor 2.96)
03:22:04 Running BNF_CC ...
03:22:04 Finished Complete_Non_Orders/outline (0:00:05 elapsed time)
03:22:04 Timing Complete_Non_Orders (4 threads, 17.759s elapsed time, 35.792s cpu time, 1.043s GC time, factor 2.02)
03:22:04 Finished Complete_Non_Orders (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.88)
03:22:04 Running CCS ...
03:22:04 Finished Optics/document (0:00:06 elapsed time)
03:22:04 Preparing Optics/outline ...
03:22:05 Finished Finite_Automata_HF/outline (0:00:02 elapsed time)
03:22:05 Finished SenSocialChoice/document (0:00:05 elapsed time)
03:22:05 Preparing SenSocialChoice/outline ...
03:22:05 Binomial-Heaps: theory Binomial-Heaps.BinomialHeap
03:22:05 Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap
03:22:05 Preparing Random_BSTs/document ...
03:22:05 Timing Finite_Automata_HF (4 threads, 15.101s elapsed time, 45.593s cpu time, 1.297s GC time, factor 3.02)
03:22:05 Finished Finite_Automata_HF (0:00:17 elapsed time, 0:00:47 cpu time, factor 2.70)
03:22:05 Running Sturm_Tarski ...
03:22:06 BNF_CC: theory BNF_CC.Preliminaries
03:22:06 BNF_CC: theory HOL-Library.Nat_Bijection
03:22:06 BNF_CC: theory HOL-Library.BNF_Axiomatization
03:22:06 BNF_CC: theory HOL-Library.Old_Datatype
03:22:06 BNF_CC: theory HOL-Library.Phantom_Type
03:22:06 BNF_CC: theory HOL-Library.Rewrite
03:22:06 CCS: theory CCS.Agent
03:22:07 BNF_CC: theory BNF_CC.Axiomatised_BNF_CC
03:22:07 BNF_CC: theory HOL-Library.Countable
03:22:07 BNF_CC: theory HOL-Library.Cardinality
03:22:07 Finished Finger-Trees/outline (0:00:04 elapsed time)
03:22:07 Timing Finger-Trees (4 threads, 17.747s elapsed time, 36.010s cpu time, 1.935s GC time, factor 2.03)
03:22:07 Finished Finger-Trees (0:00:21 elapsed time, 0:00:39 cpu time, factor 1.82)
03:22:07 Running Octonions ...
03:22:08 BNF_CC: theory BNF_CC.Concrete_Examples
03:22:08 BNF_CC: theory HOL-Library.FSet
03:22:08 BNF_CC: theory BNF_CC.Composition
03:22:08 BNF_CC: theory BNF_CC.Fixpoints
03:22:09 BNF_CC: theory BNF_CC.Quotient_Preservation
03:22:09 BNF_CC: theory BNF_CC.Subtypes
03:22:09 Finished SenSocialChoice/outline (0:00:03 elapsed time)
03:22:09 Finished Random_BSTs/document (0:00:03 elapsed time)
03:22:09 Preparing Random_BSTs/outline ...
03:22:09 Sturm_Tarski: theory Sturm_Tarski.PolyMisc
03:22:09 Timing SenSocialChoice (4 threads, 17.352s elapsed time, 50.025s cpu time, 0.864s GC time, factor 2.88)
03:22:09 Finished SenSocialChoice (0:00:20 elapsed time, 0:00:52 cpu time, factor 2.61)
03:22:09 Running InformationFlowSlicing_Inter ...
03:22:10 Sturm_Tarski: theory Sturm_Tarski.Sturm_Tarski
03:22:11 Finished Optics/outline (0:00:06 elapsed time)
03:22:11 CCS: theory CCS.Strong_Sim
03:22:11 CCS: theory CCS.Struct_Cong
03:22:11 Octonions: theory Octonions.Cross_Product_7
03:22:11 CCS: theory CCS.Tau_Chain
03:22:11 Timing Optics (4 threads, 18.525s elapsed time, 49.665s cpu time, 0.858s GC time, factor 2.68)
03:22:11 Finished Optics (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.48)
03:22:11 Running Floyd_Warshall ...
03:22:11 CCS: theory CCS.Strong_Bisim
03:22:11 CCS: theory CCS.Strong_Sim_Pres
03:22:11 CCS: theory CCS.Strong_Sim_SC
03:22:11 CCS: theory CCS.Weak_Cong_Semantics
03:22:11 CCS: theory CCS.Strong_Bisim_Pres
03:22:12 CCS: theory CCS.Weak_Semantics
03:22:12 CCS: theory CCS.Weak_Sim
03:22:12 CCS: theory CCS.Strong_Bisim_SC
03:22:12 CCS: theory CCS.Weak_Cong_Sim
03:22:12 CCS: theory CCS.Weak_Sim_Pres
03:22:12 CCS: theory CCS.Weak_Cong_Sim_Pres
03:22:12 CCS: theory CCS.Weak_Bisim
03:22:13 Finished Random_BSTs/outline (0:00:03 elapsed time)
03:22:13 CCS: theory CCS.Weak_Cong
03:22:13 CCS: theory CCS.Weak_Bisim_Pres
03:22:13 CCS: theory CCS.Weak_Cong_Pres
03:22:13 Timing Random_BSTs (4 threads, 7.720s elapsed time, 15.716s cpu time, 0.303s GC time, factor 2.04)
03:22:13 Finished Random_BSTs (0:00:34 elapsed time, 0:00:57 cpu time, factor 1.67)
03:22:13 Running Boolean_Expression_Checkers ...
03:22:14 Octonions: theory Octonions.Octonions
03:22:14 BNF_CC: theory BNF_CC.Operation_Examples
03:22:14 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
03:22:15 BNF_CC: theory BNF_CC.DDS
03:22:15 Finished Finitely_Generated_Abelian_Groups/document (0:00:11 elapsed time)
03:22:15 Preparing Finitely_Generated_Abelian_Groups/outline ...
03:22:16 Preparing IMP2_Binary_Heap/document ...
03:22:16 Floyd_Warshall: theory Floyd_Warshall.Floyd_Warshall
03:22:16 Floyd_Warshall: theory Floyd_Warshall.Recursion_Combinators
03:22:17 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
03:22:19 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
03:22:20 Binomial-Heaps: theory Binomial-Heaps.Test
03:22:21 Finished IMP2_Binary_Heap/document (0:00:04 elapsed time)
03:22:21 Preparing IMP2_Binary_Heap/outline ...
03:22:21 Finished Finitely_Generated_Abelian_Groups/outline (0:00:06 elapsed time)
03:22:21 Timing Finitely_Generated_Abelian_Groups (4 threads, 16.426s elapsed time, 51.176s cpu time, 2.933s GC time, factor 3.12)
03:22:21 Finished Finitely_Generated_Abelian_Groups (0:00:24 elapsed time, 0:00:59 cpu time, factor 2.39)
03:22:21 Running CISC-Kernel ...
03:22:22 Preparing CCS/document ...
03:22:22 Preparing BNF_CC/document ...
03:22:22 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
03:22:23 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Example
03:22:23 CISC-Kernel: theory CISC-Kernel.Option_Binders
03:22:23 CISC-Kernel: theory CISC-Kernel.List_Theorems
03:22:23 CISC-Kernel: theory CISC-Kernel.Step_configuration
03:22:23 Preparing Binomial-Heaps/document ...
03:22:23 CISC-Kernel: theory CISC-Kernel.K
03:22:23 Floyd_Warshall: theory Floyd_Warshall.FW_Code
03:22:24 CISC-Kernel: theory CISC-Kernel.SK
03:22:24 Finished IMP2_Binary_Heap/outline (0:00:03 elapsed time)
03:22:24 CISC-Kernel: theory CISC-Kernel.Step_policies
03:22:24 Timing IMP2_Binary_Heap (4 threads, 15.270s elapsed time, 40.986s cpu time, 0.627s GC time, factor 2.68)
03:22:24 Finished IMP2_Binary_Heap (0:00:17 elapsed time, 0:00:43 cpu time, factor 2.43)
03:22:24 Running Transitive-Closure-II ...
03:22:24 CISC-Kernel: theory CISC-Kernel.Step
03:22:25 CISC-Kernel: theory CISC-Kernel.ISK
03:22:26 CISC-Kernel: theory CISC-Kernel.CISK
03:22:26 Transitive-Closure-II: theory HOL-Library.While_Combinator
03:22:26 Transitive-Closure-II: theory Regular-Sets.Regular_Set
03:22:27 Preparing Sturm_Tarski/document ...
03:22:28 Preparing Octonions/document ...
03:22:28 CISC-Kernel: theory CISC-Kernel.Step_invariants
03:22:28 Finished CCS/document (0:00:06 elapsed time)
03:22:28 Preparing CCS/outline ...
03:22:28 CISC-Kernel: theory CISC-Kernel.Step_vpeq
03:22:28 CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects
03:22:29 CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent
03:22:29 CISC-Kernel: theory CISC-Kernel.Separation_kernel_model
03:22:30 Finished Binomial-Heaps/document (0:00:06 elapsed time)
03:22:30 Preparing Binomial-Heaps/outline ...
03:22:30 CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK
03:22:31 Transitive-Closure-II: theory Regular-Sets.Regular_Exp
03:22:32 Preparing InformationFlowSlicing_Inter/document ...
03:22:32 Finished BNF_CC/document (0:00:09 elapsed time)
03:22:32 Preparing BNF_CC/outline ...
03:22:32 Preparing Floyd_Warshall/document ...
03:22:33 Finished Sturm_Tarski/document (0:00:05 elapsed time)
03:22:33 Preparing Sturm_Tarski/outline ...
03:22:33 Finished CCS/outline (0:00:04 elapsed time)
03:22:33 Finished Octonions/document (0:00:05 elapsed time)
03:22:33 Preparing Octonions/outline ...
03:22:33 Preparing Boolean_Expression_Checkers/document ...
03:22:33 Timing CCS (4 threads, 14.868s elapsed time, 47.855s cpu time, 0.951s GC time, factor 3.22)
03:22:33 Finished CCS (0:00:17 elapsed time, 0:00:50 cpu time, factor 2.89)
03:22:33 Running Ribbon_Proofs ...
03:22:34 Finished Binomial-Heaps/outline (0:00:04 elapsed time)
03:22:34 Timing Binomial-Heaps (4 threads, 16.723s elapsed time, 48.134s cpu time, 2.547s GC time, factor 2.88)
03:22:34 Finished Binomial-Heaps (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.50)
03:22:34 Running Decreasing-Diagrams-II ...
03:22:34 Transitive-Closure-II: theory Regular-Sets.NDerivative
03:22:34 Transitive-Closure-II: theory Regular-Sets.Relation_Interpretation
03:22:35 Finished Boolean_Expression_Checkers/document (0:00:02 elapsed time)
03:22:35 Preparing Boolean_Expression_Checkers/outline ...
03:22:36 Finished Sturm_Tarski/outline (0:00:03 elapsed time)
03:22:36 Timing Sturm_Tarski (4 threads, 16.673s elapsed time, 42.037s cpu time, 0.676s GC time, factor 2.52)
03:22:36 Finished Sturm_Tarski (0:00:21 elapsed time, 0:00:46 cpu time, factor 2.18)
03:22:36 Running Real_Power ...
03:22:36 Ribbon_Proofs: theory Ribbon_Proofs.More_Finite_Map
03:22:36 Ribbon_Proofs: theory Ribbon_Proofs.JHelper
03:22:36 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Basic
03:22:37 Ribbon_Proofs: theory Ribbon_Proofs.Proofchain
03:22:37 Finished Boolean_Expression_Checkers/outline (0:00:01 elapsed time)
03:22:37 Finished Octonions/outline (0:00:04 elapsed time)
03:22:37 Timing Octonions (4 threads, 15.565s elapsed time, 54.870s cpu time, 1.422s GC time, factor 3.53)
03:22:37 Finished Octonions (0:00:19 elapsed time, 0:00:58 cpu time, factor 2.98)
03:22:37 Timing Boolean_Expression_Checkers (4 threads, 15.388s elapsed time, 29.101s cpu time, 1.574s GC time, factor 1.89)
03:22:37 Finished Boolean_Expression_Checkers (0:00:19 elapsed time, 0:00:33 cpu time, factor 1.68)
03:22:37 Running GraphMarkingIBP ...
03:22:37 Running Functional-Automata ...
03:22:37 Finished Floyd_Warshall/document (0:00:05 elapsed time)
03:22:37 Preparing Floyd_Warshall/outline ...
03:22:38 Preparing CISC-Kernel/document ...
03:22:38 Decreasing-Diagrams-II: theory Open_Induction.Restricted_Predicates
03:22:38 Decreasing-Diagrams-II: theory HOL-Cardinals.Order_Union
03:22:38 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Infinite_Sequences
03:22:38 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Least_Enum
03:22:38 Decreasing-Diagrams-II: theory HOL-Cardinals.Wellorder_Extension
03:22:38 Real_Power: theory Real_Power.RatPower
03:22:38 Transitive-Closure-II: theory Regular-Sets.Equivalence_Checking
03:22:38 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Multiset_Extension
03:22:38 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Elements
03:22:38 Real_Power: theory Real_Power.RealPower
03:22:38 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full
03:22:39 Transitive-Closure-II: theory Regular-Sets.Regexp_Method
03:22:39 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Interfaces
03:22:39 Finished BNF_CC/outline (0:00:06 elapsed time)
03:22:39 GraphMarkingIBP: theory GraphMarkingIBP.Graph
03:22:39 GraphMarkingIBP: theory LatticeProperties.WellFoundedTransitive
03:22:39 GraphMarkingIBP: theory LatticeProperties.Conj_Disj
03:22:39 Finished InformationFlowSlicing_Inter/document (0:00:07 elapsed time)
03:22:39 Preparing InformationFlowSlicing_Inter/outline ...
03:22:39 Timing BNF_CC (4 threads, 15.433s elapsed time, 48.249s cpu time, 2.571s GC time, factor 3.13)
03:22:39 Finished BNF_CC (0:00:17 elapsed time, 0:00:50 cpu time, factor 2.84)
03:22:39 Running Minsky_Machines ...
03:22:40 Real_Power: theory Real_Power.Log
03:22:40 Transitive-Closure-II: theory Transitive-Closure-II.RTrancl
03:22:40 GraphMarkingIBP: theory LatticeProperties.Complete_Lattice_Prop
03:22:40 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Bad_Sequences
03:22:40 GraphMarkingIBP: theory DataRefinementIBP.Preliminaries
03:22:40 GraphMarkingIBP: theory DataRefinementIBP.Statements
03:22:40 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full_Relations
03:22:40 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical
03:22:40 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Stratified
03:22:41 GraphMarkingIBP: theory DataRefinementIBP.Hoare
03:22:41 Functional-Automata: theory Functional-Automata.AutoProj
03:22:41 GraphMarkingIBP: theory DataRefinementIBP.Diagram
03:22:41 Functional-Automata: theory Functional-Automata.MaxPrefix
03:22:41 Functional-Automata: theory Regular-Sets.Regular_Set
03:22:41 Functional-Automata: theory Functional-Automata.DA
03:22:41 Functional-Automata: theory Functional-Automata.NA
03:22:41 Functional-Automata: theory Functional-Automata.NAe
03:22:41 Functional-Automata: theory Functional-Automata.MaxChop
03:22:41 GraphMarkingIBP: theory DataRefinementIBP.DataRefinement
03:22:41 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Well_Quasi_Orders
03:22:41 Functional-Automata: theory Functional-Automata.Automata
03:22:41 Functional-Automata: theory Functional-Automata.AutoMaxChop
03:22:42 Preparing Transitive-Closure-II/document ...
03:22:42 GraphMarkingIBP: theory GraphMarkingIBP.SetMark
03:22:42 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux
03:22:42 Finished Floyd_Warshall/outline (0:00:04 elapsed time)
03:22:42 Timing Floyd_Warshall (4 threads, 14.880s elapsed time, 50.756s cpu time, 1.060s GC time, factor 3.41)
03:22:42 Finished Floyd_Warshall (0:00:21 elapsed time, 0:00:56 cpu time, factor 2.69)
03:22:42 Running Name_Carrying_Type_Inference ...
03:22:42 GraphMarkingIBP: theory GraphMarkingIBP.StackMark
03:22:43 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II
03:22:43 GraphMarkingIBP: theory GraphMarkingIBP.LinkMark
03:22:43 Minsky_Machines: theory Pure-ex.Guess
03:22:43 Minsky_Machines: theory Recursion-Theory-I.CPair
03:22:44 Minsky_Machines: theory Recursion-Theory-I.PRecFun
03:22:44 GraphMarkingIBP: theory GraphMarkingIBP.DSWMark
03:22:44 Finished InformationFlowSlicing_Inter/outline (0:00:04 elapsed time)
03:22:44 Timing InformationFlowSlicing_Inter (4 threads, 16.465s elapsed time, 51.925s cpu time, 2.527s GC time, factor 3.15)
03:22:44 Finished InformationFlowSlicing_Inter (0:00:21 elapsed time, 0:00:57 cpu time, factor 2.61)
03:22:44 Running Median_Of_Medians_Selection ...
03:22:44 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical_Soundness
03:22:45 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.Permutation
03:22:45 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.Fresh
03:22:45 Finished Transitive-Closure-II/document (0:00:03 elapsed time)
03:22:45 Preparing Transitive-Closure-II/outline ...
03:22:45 Functional-Automata: theory Functional-Automata.RegSet_of_nat_DA
03:22:45 Functional-Automata: theory Regular-Sets.Regular_Exp
03:22:46 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.PreSimplyTyped
03:22:46 Median_Of_Medians_Selection: theory HOL-Library.Cancellation
03:22:47 Minsky_Machines: theory Recursion-Theory-I.PRecFinSet
03:22:47 Minsky_Machines: theory Recursion-Theory-I.PRecFun2
03:22:47 Minsky_Machines: theory Recursion-Theory-I.PRecList
03:22:47 Median_Of_Medians_Selection: theory HOL-Library.Multiset
03:22:49 Finished Transitive-Closure-II/outline (0:00:03 elapsed time)
03:22:49 Finished CISC-Kernel/document (0:00:11 elapsed time)
03:22:49 Preparing CISC-Kernel/outline ...
03:22:49 Timing Transitive-Closure-II (4 threads, 14.474s elapsed time, 27.314s cpu time, 1.052s GC time, factor 1.89)
03:22:49 Finished Transitive-Closure-II (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.73)
03:22:49 Running Posix-Lexing ...
03:22:49 Functional-Automata: theory Functional-Automata.RegExp2NA
03:22:49 Functional-Automata: theory Functional-Automata.RegExp2NAe
03:22:50 Minsky_Machines: theory Recursion-Theory-I.PRecUnGr
03:22:51 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.SimplyTyped
03:22:53 Posix-Lexing: theory Posix-Lexing.Lexer
03:22:53 Functional-Automata: theory Functional-Automata.AutoRegExp
03:22:53 Functional-Automata: theory Functional-Automata.Execute
03:22:53 Functional-Automata: theory Functional-Automata.Functional_Automata
03:22:53 Minsky_Machines: theory Recursion-Theory-I.RecEnSet
03:22:54 Preparing Decreasing-Diagrams-II/document ...
03:22:54 Preparing Ribbon_Proofs/document ...
03:22:54 Preparing Real_Power/document ...
03:22:55 Minsky_Machines: theory Minsky_Machines.Recursive_Inseparability
03:22:55 Minsky_Machines: theory Minsky_Machines.Minsky
03:22:56 Finished CISC-Kernel/outline (0:00:07 elapsed time)
03:22:56 Timing CISC-Kernel (4 threads, 13.707s elapsed time, 47.892s cpu time, 2.059s GC time, factor 3.49)
03:22:56 Finished CISC-Kernel (0:00:16 elapsed time, 0:00:49 cpu time, factor 3.10)
03:22:56 Running Decreasing-Diagrams ...
03:22:56 Median_Of_Medians_Selection: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
03:22:56 Preparing GraphMarkingIBP/document ...
03:22:58 Preparing Functional-Automata/document ...
03:22:58 Finished Decreasing-Diagrams-II/document (0:00:04 elapsed time)
03:22:58 Preparing Decreasing-Diagrams-II/outline ...
03:22:59 Finished Real_Power/document (0:00:04 elapsed time)
03:22:59 Preparing Real_Power/outline ...
03:22:59 Finished Ribbon_Proofs/document (0:00:05 elapsed time)
03:22:59 Preparing Ribbon_Proofs/outline ...
03:22:59 Decreasing-Diagrams: theory Decreasing-Diagrams.Decreasing_Diagrams
03:23:00 Preparing Minsky_Machines/document ...
03:23:00 Posix-Lexing: theory Posix-Lexing.Simplifying
03:23:01 Finished GraphMarkingIBP/document (0:00:04 elapsed time)
03:23:01 Preparing GraphMarkingIBP/outline ...
03:23:01 Preparing Name_Carrying_Type_Inference/document ...
03:23:01 Finished Functional-Automata/document (0:00:03 elapsed time)
03:23:01 Preparing Functional-Automata/outline ...
03:23:02 Finished Real_Power/outline (0:00:02 elapsed time)
03:23:02 Finished Decreasing-Diagrams-II/outline (0:00:03 elapsed time)
03:23:02 Timing Real_Power (4 threads, 15.439s elapsed time, 33.164s cpu time, 0.573s GC time, factor 2.15)
03:23:02 Finished Real_Power (0:00:17 elapsed time, 0:00:35 cpu time, factor 1.97)
03:23:02 Timing Decreasing-Diagrams-II (4 threads, 14.893s elapsed time, 55.341s cpu time, 1.347s GC time, factor 3.72)
03:23:02 Finished Decreasing-Diagrams-II (0:00:19 elapsed time, 0:00:59 cpu time, factor 3.11)
03:23:02 Running Nash_Williams ...
03:23:02 Running List_Inversions ...
03:23:02 Preparing Median_Of_Medians_Selection/document ...
03:23:03 Finished Ribbon_Proofs/outline (0:00:03 elapsed time)
03:23:03 Timing Ribbon_Proofs (4 threads, 16.627s elapsed time, 36.357s cpu time, 1.624s GC time, factor 2.19)
03:23:03 Finished Ribbon_Proofs (0:00:20 elapsed time, 0:00:40 cpu time, factor 1.94)
03:23:03 Running FunWithTilings ...
03:23:04 List_Inversions: theory HOL-Combinatorics.Transposition
03:23:04 List_Inversions: theory HOL-Library.FuncSet
03:23:04 List_Inversions: theory HOL-Library.Cancellation
03:23:04 Nash_Williams: theory HOL-Library.Infinite_Set
03:23:04 Nash_Williams: theory HOL-Library.FuncSet
03:23:04 Nash_Williams: theory HOL-Library.Old_Datatype
03:23:04 Nash_Williams: theory HOL-Library.Nat_Bijection
03:23:04 Finished Minsky_Machines/document (0:00:03 elapsed time)
03:23:04 Preparing Minsky_Machines/outline ...
03:23:04 Finished GraphMarkingIBP/outline (0:00:03 elapsed time)
03:23:04 List_Inversions: theory HOL-Library.Multiset
03:23:04 Timing GraphMarkingIBP (4 threads, 16.512s elapsed time, 52.285s cpu time, 0.737s GC time, factor 3.17)
03:23:04 Finished GraphMarkingIBP (0:00:19 elapsed time, 0:00:54 cpu time, factor 2.86)
03:23:04 Running POPLmark-deBruijn ...
03:23:04 List_Inversions: theory HOL-Library.Disjoint_Sets
03:23:05 Finished Functional-Automata/outline (0:00:03 elapsed time)
03:23:05 Timing Functional-Automata (4 threads, 15.875s elapsed time, 34.436s cpu time, 0.880s GC time, factor 2.17)
03:23:05 Finished Functional-Automata (0:00:19 elapsed time, 0:00:38 cpu time, factor 1.92)
03:23:05 Running Derangements ...
03:23:05 Nash_Williams: theory HOL-Library.Ramsey
03:23:05 Nash_Williams: theory HOL-Library.Countable
03:23:05 FunWithTilings: theory FunWithTilings.Tilings
03:23:06 Finished Median_Of_Medians_Selection/document (0:00:03 elapsed time)
03:23:06 Preparing Median_Of_Medians_Selection/outline ...
03:23:06 Nash_Williams: theory HOL-Library.Countable_Set
03:23:06 Finished Name_Carrying_Type_Inference/document (0:00:05 elapsed time)
03:23:06 Preparing Name_Carrying_Type_Inference/outline ...
03:23:07 Nash_Williams: theory Nash_Williams.Nash_Extras
03:23:07 Derangements: theory HOL-Combinatorics.Transposition
03:23:07 Derangements: theory HOL-Library.Cancellation
03:23:07 Derangements: theory HOL-Library.FuncSet
03:23:08 Nash_Williams: theory Nash_Williams.Nash_Williams
03:23:08 Finished Minsky_Machines/outline (0:00:03 elapsed time)
03:23:08 POPLmark-deBruijn: theory POPLmark-deBruijn.Basis
03:23:08 Timing Minsky_Machines (4 threads, 15.544s elapsed time, 53.280s cpu time, 2.408s GC time, factor 3.43)
03:23:08 Finished Minsky_Machines (0:00:19 elapsed time, 0:00:57 cpu time, factor 2.89)
03:23:08 Running Stream_Fusion_Code ...
03:23:08 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmarkRecord
03:23:08 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmark
03:23:09 Derangements: theory HOL-Library.Multiset
03:23:09 Derangements: theory HOL-Library.Disjoint_Sets
03:23:09 Preparing Posix-Lexing/document ...
03:23:09 Finished Median_Of_Medians_Selection/outline (0:00:03 elapsed time)
03:23:09 Timing Median_Of_Medians_Selection (4 threads, 14.672s elapsed time, 39.536s cpu time, 1.266s GC time, factor 2.69)
03:23:09 Finished Median_Of_Medians_Selection (0:00:17 elapsed time, 0:00:41 cpu time, factor 2.44)
03:23:09 Running AxiomaticCategoryTheory ...
03:23:10 Finished Name_Carrying_Type_Inference/outline (0:00:03 elapsed time)
03:23:10 Timing Name_Carrying_Type_Inference (4 threads, 15.587s elapsed time, 52.536s cpu time, 1.657s GC time, factor 3.37)
03:23:10 Finished Name_Carrying_Type_Inference (0:00:18 elapsed time, 0:00:55 cpu time, factor 3.01)
03:23:10 Running Jordan_Hoelder ...
03:23:11 List_Inversions: theory HOL-Combinatorics.Permutations
03:23:11 AxiomaticCategoryTheory: theory AxiomaticCategoryTheory.AxiomaticCategoryTheory
03:23:13 List_Inversions: theory List_Inversions.List_Inversions
03:23:13 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion
03:23:13 Finished Posix-Lexing/document (0:00:04 elapsed time)
03:23:13 Preparing Posix-Lexing/outline ...
03:23:13 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List
03:23:15 Derangements: theory HOL-Combinatorics.Permutations
03:23:15 Preparing Decreasing-Diagrams/document ...
03:23:17 Finished Posix-Lexing/outline (0:00:04 elapsed time)
03:23:18 Timing Posix-Lexing (4 threads, 15.176s elapsed time, 33.003s cpu time, 1.093s GC time, factor 2.17)
03:23:18 Finished Posix-Lexing (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.87)
03:23:18 Running Lambda_Free_RPOs ...
03:23:18 Derangements: theory Derangements.Derangements
03:23:18 POPLmark-deBruijn: theory POPLmark-deBruijn.Execute
03:23:18 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmarkRecordCtxt
03:23:19 Jordan_Hoelder: theory Secondary_Sylow.GroupAction
03:23:19 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
03:23:20 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
03:23:20 Jordan_Hoelder: theory Secondary_Sylow.SndSylow
03:23:20 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp
03:23:20 Preparing Nash_Williams/document ...
03:23:21 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups
03:23:21 Preparing List_Inversions/document ...
03:23:22 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups
03:23:22 Lambda_Free_RPOs: theory Nested_Multisets_Ordinals.Multiset_More
03:23:22 Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
03:23:22 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
03:23:22 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
03:23:22 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
03:23:22 Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
03:23:22 Preparing FunWithTilings/document ...
03:23:23 Finished Decreasing-Diagrams/document (0:00:07 elapsed time)
03:23:23 Preparing Decreasing-Diagrams/outline ...
03:23:23 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList
03:23:23 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
03:23:24 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
03:23:24 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
03:23:24 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
03:23:25 Finished Nash_Williams/document (0:00:04 elapsed time)
03:23:25 Preparing Nash_Williams/outline ...
03:23:25 Preparing Derangements/document ...
03:23:25 Finished List_Inversions/document (0:00:04 elapsed time)
03:23:25 Preparing List_Inversions/outline ...
03:23:26 Finished FunWithTilings/document (0:00:03 elapsed time)
03:23:26 Preparing FunWithTilings/outline ...
03:23:26 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples
03:23:27 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
03:23:27 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
03:23:27 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
03:23:28 Preparing POPLmark-deBruijn/document ...
03:23:28 Finished Decreasing-Diagrams/outline (0:00:04 elapsed time)
03:23:28 Timing Decreasing-Diagrams (4 threads, 14.406s elapsed time, 46.809s cpu time, 1.040s GC time, factor 3.25)
03:23:28 Finished Decreasing-Diagrams (0:00:18 elapsed time, 0:00:50 cpu time, factor 2.72)
03:23:28 Running Cayley_Hamilton ...
03:23:28 Finished Nash_Williams/outline (0:00:03 elapsed time)
03:23:29 Timing Nash_Williams (4 threads, 15.422s elapsed time, 56.023s cpu time, 1.146s GC time, factor 3.63)
03:23:29 Finished Nash_Williams (0:00:17 elapsed time, 0:00:58 cpu time, factor 3.26)
03:23:29 Running Coinductive_Languages ...
03:23:29 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
03:23:29 Preparing AxiomaticCategoryTheory/document ...
03:23:29 Finished List_Inversions/outline (0:00:03 elapsed time)
03:23:29 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
03:23:29 Finished Derangements/document (0:00:03 elapsed time)
03:23:29 Preparing Derangements/outline ...
03:23:29 Timing List_Inversions (4 threads, 16.082s elapsed time, 59.284s cpu time, 2.105s GC time, factor 3.69)
03:23:29 Finished List_Inversions (0:00:18 elapsed time, 0:01:01 cpu time, factor 3.31)
03:23:29 Running Pell ...
03:23:29 Finished FunWithTilings/outline (0:00:03 elapsed time)
03:23:30 Timing FunWithTilings (4 threads, 16.104s elapsed time, 52.061s cpu time, 0.341s GC time, factor 3.23)
03:23:30 Finished FunWithTilings (0:00:18 elapsed time, 0:00:54 cpu time, factor 2.92)
03:23:30 Building Combinatorics_Words ...
03:23:30 Coinductive_Languages: theory Coinductive_Languages.Coinductive_Language
03:23:30 Coinductive_Languages: theory HOL-Library.Old_Datatype
03:23:30 Coinductive_Languages: theory HOL-Library.Nat_Bijection
03:23:30 Coinductive_Languages: theory Regular-Sets.Regular_Set
03:23:31 Preparing Stream_Fusion_Code/document ...
03:23:31 Coinductive_Languages: theory HOL-Library.Countable
03:23:31 Cayley_Hamilton: theory HOL-Library.More_List
03:23:31 Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
03:23:31 Finished AxiomaticCategoryTheory/document (0:00:02 elapsed time)
03:23:32 Preparing AxiomaticCategoryTheory/outline ...
03:23:32 Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
03:23:32 Finished Derangements/outline (0:00:03 elapsed time)
03:23:32 Timing Derangements (4 threads, 16.730s elapsed time, 61.549s cpu time, 1.757s GC time, factor 3.68)
03:23:32 Finished Derangements (0:00:19 elapsed time, 0:01:04 cpu time, factor 3.28)
03:23:32 Running TLA ...
03:23:33 Coinductive_Languages: theory HOL-Library.FSet
03:23:33 Pell: theory Pell.Efficient_Discrete_Sqrt
03:23:33 Pell: theory Pell.Pell
03:23:33 Combinatorics_Words: theory Combinatorics_Words.Arithmetical_Hints
03:23:33 Combinatorics_Words: theory Combinatorics_Words.Reverse_Symmetry
03:23:33 Preparing Jordan_Hoelder/document ...
03:23:34 Combinatorics_Words: theory Combinatorics_Words.CoWBasic
03:23:34 TLA: theory TLA.Intensional
03:23:34 TLA: theory TLA.Sequence
03:23:35 Finished AxiomaticCategoryTheory/outline (0:00:03 elapsed time)
03:23:35 Timing AxiomaticCategoryTheory (4 threads, 16.436s elapsed time, 43.984s cpu time, 1.246s GC time, factor 2.68)
03:23:35 Finished AxiomaticCategoryTheory (0:00:19 elapsed time, 0:00:46 cpu time, factor 2.43)
03:23:35 Building Epistemic_Logic ...
03:23:35 Coinductive_Languages: theory Coinductive_Languages.Coinductive_Regular_Set
03:23:36 Pell: theory Pell.Pell_Algorithm
03:23:36 Finished POPLmark-deBruijn/document (0:00:08 elapsed time)
03:23:36 Preparing POPLmark-deBruijn/outline ...
03:23:37 TLA: theory TLA.Semantics
03:23:37 Pell: theory Pell.Pell_Algorithm_Test
03:23:38 TLA: theory TLA.PreFormulas
03:23:38 Preparing Lambda_Free_RPOs/document ...
03:23:38 TLA: theory TLA.Rules
03:23:39 Coinductive_Languages: theory Coinductive_Languages.Context_Free_Grammar
03:23:39 Finished Stream_Fusion_Code/document (0:00:08 elapsed time)
03:23:39 Preparing Stream_Fusion_Code/outline ...
03:23:39 TLA: theory TLA.Liveness
03:23:39 Epistemic_Logic: theory Epistemic_Logic.Epistemic_Logic
03:23:39 TLA: theory TLA.State
03:23:40 TLA: theory TLA.Buffer
03:23:40 TLA: theory TLA.Even
03:23:40 TLA: theory TLA.Inc
03:23:41 Finished Jordan_Hoelder/document (0:00:07 elapsed time)
03:23:41 Preparing Jordan_Hoelder/outline ...
03:23:42 Combinatorics_Words: theory Combinatorics_Words.Lyndon_Schutzenberger
03:23:42 Combinatorics_Words: theory Combinatorics_Words.Periodicity_Lemma
03:23:42 Combinatorics_Words: theory Combinatorics_Words.Submonoids
03:23:42 Finished POPLmark-deBruijn/outline (0:00:06 elapsed time)
03:23:43 Timing POPLmark-deBruijn (4 threads, 18.391s elapsed time, 63.439s cpu time, 2.530s GC time, factor 3.45)
03:23:43 Finished POPLmark-deBruijn (0:00:22 elapsed time, 0:01:07 cpu time, factor 2.99)
03:23:43 Running KD_Tree ...
03:23:43 Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
03:23:44 Finished Lambda_Free_RPOs/document (0:00:05 elapsed time)
03:23:44 Preparing Lambda_Free_RPOs/outline ...
03:23:45 Combinatorics_Words: theory Combinatorics_Words.CoWAll
03:23:45 Finished Jordan_Hoelder/outline (0:00:03 elapsed time)
03:23:45 Timing Jordan_Hoelder (4 threads, 13.267s elapsed time, 47.222s cpu time, 1.748s GC time, factor 3.56)
03:23:45 Finished Jordan_Hoelder (0:00:22 elapsed time, 0:00:56 cpu time, factor 2.47)
03:23:45 Running Types_Tableaus_and_Goedels_God ...
03:23:45 Preparing Coinductive_Languages/document ...
03:23:46 Finished Stream_Fusion_Code/outline (0:00:06 elapsed time)
03:23:46 Timing Stream_Fusion_Code (4 threads, 16.470s elapsed time, 56.027s cpu time, 1.635s GC time, factor 3.40)
03:23:46 Finished Stream_Fusion_Code (0:00:22 elapsed time, 0:01:01 cpu time, factor 2.76)
03:23:46 Running Euler_Partition ...
03:23:46 KD_Tree: theory KD_Tree.KD_Tree
03:23:46 KD_Tree: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
03:23:47 Finished Lambda_Free_RPOs/outline (0:00:03 elapsed time)
03:23:47 Timing Lambda_Free_RPOs (4 threads, 14.973s elapsed time, 56.801s cpu time, 1.892s GC time, factor 3.79)
03:23:47 Finished Lambda_Free_RPOs (0:00:19 elapsed time, 0:01:01 cpu time, factor 3.10)
03:23:47 Running Inductive_Confidentiality ...
03:23:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
03:23:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
03:23:47 Preparing Cayley_Hamilton/document ...
03:23:48 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
03:23:48 Finished Coinductive_Languages/document (0:00:02 elapsed time)
03:23:48 Preparing Coinductive_Languages/outline ...
03:23:48 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
03:23:48 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
03:23:48 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
03:23:48 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
03:23:48 Preparing TLA/document ...
03:23:48 Euler_Partition: theory HOL-Library.Cancellation
03:23:48 KD_Tree: theory KD_Tree.Nearest_Neighbors
03:23:48 KD_Tree: theory KD_Tree.Range_Search
03:23:48 KD_Tree: theory KD_Tree.Build
03:23:49 Preparing Pell/document ...
03:23:49 Inductive_Confidentiality: theory Inductive_Confidentiality.Message
03:23:49 Inductive_Confidentiality: theory Inductive_Confidentiality.MessageGA
03:23:49 Euler_Partition: theory HOL-Library.Multiset
03:23:50 Finished Coinductive_Languages/outline (0:00:02 elapsed time)
03:23:50 Timing Coinductive_Languages (4 threads, 14.086s elapsed time, 49.129s cpu time, 1.606s GC time, factor 3.49)
03:23:50 Finished Coinductive_Languages (0:00:16 elapsed time, 0:00:51 cpu time, factor 3.12)
03:23:50 Running Completeness ...
03:23:52 Finished Cayley_Hamilton/document (0:00:04 elapsed time)
03:23:52 Preparing Cayley_Hamilton/outline ...
03:23:52 Inductive_Confidentiality: theory Inductive_Confidentiality.EventGA
03:23:52 Inductive_Confidentiality: theory Inductive_Confidentiality.Event
03:23:52 Completeness: theory Completeness.Tree
03:23:52 Completeness: theory HOL-Library.Cancellation
03:23:53 Inductive_Confidentiality: theory Inductive_Confidentiality.PublicGA
03:23:54 Inductive_Confidentiality: theory Inductive_Confidentiality.Public
03:23:54 Completeness: theory HOL-Library.Multiset
03:23:54 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad_GA
03:23:54 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad
03:23:54 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityGA
03:23:54 Inductive_Confidentiality: theory Inductive_Confidentiality.Knowledge
03:23:54 Finished Pell/document (0:00:05 elapsed time)
03:23:54 Preparing Pell/outline ...
03:23:55 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityDY
03:23:56 Finished Cayley_Hamilton/outline (0:00:04 elapsed time)
03:23:56 Euler_Partition: theory Card_Number_Partitions.Additions_to_Main
03:23:56 Euler_Partition: theory Card_Number_Partitions.Number_Partition
03:23:56 Timing Cayley_Hamilton (4 threads, 14.531s elapsed time, 49.595s cpu time, 1.529s GC time, factor 3.41)
03:23:56 Finished Cayley_Hamilton (0:00:18 elapsed time, 0:00:53 cpu time, factor 2.86)
03:23:56 Running Constructor_Funs ...
03:23:56 Euler_Partition: theory Euler_Partition.Euler_Partition
03:23:58 Constructor_Funs: theory Constructor_Funs.Constructor_Funs
03:23:59 Finished TLA/document (0:00:10 elapsed time)
03:23:59 Preparing TLA/outline ...
03:23:59 Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
03:23:59 Finished Pell/outline (0:00:04 elapsed time)
03:23:59 Timing Pell (4 threads, 14.424s elapsed time, 48.624s cpu time, 0.588s GC time, factor 3.37)
03:23:59 Finished Pell (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.77)
03:23:59 Running Euler_MacLaurin ...
03:24:00 Completeness: theory Completeness.PermutationLemmas
03:24:00 Completeness: theory Completeness.Base
03:24:00 Completeness: theory Completeness.Formula
03:24:00 Preparing KD_Tree/document ...
03:24:01 Preparing Types_Tableaus_and_Goedels_God/document ...
03:24:02 Preparing Euler_Partition/document ...
03:24:02 Preparing Inductive_Confidentiality/document ...
03:24:02 Completeness: theory Completeness.Sequents
03:24:03 Completeness: theory Completeness.Completeness
03:24:04 Completeness: theory Completeness.Soundness
03:24:04 Preparing Combinatorics_Words/document ...
03:24:04 Euler_MacLaurin: theory HOL-Library.Function_Algebras
03:24:04 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
03:24:04 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
03:24:04 Finished TLA/outline (0:00:05 elapsed time)
03:24:04 Timing TLA (4 threads, 12.687s elapsed time, 43.898s cpu time, 1.270s GC time, factor 3.46)
03:24:04 Finished TLA (0:00:15 elapsed time, 0:00:46 cpu time, factor 2.98)
03:24:04 Running Optimal_BST ...
03:24:05 Finished KD_Tree/document (0:00:04 elapsed time)
03:24:05 Preparing KD_Tree/outline ...
03:24:05 Finished Euler_Partition/document (0:00:03 elapsed time)
03:24:05 Preparing Euler_Partition/outline ...
03:24:06 Preparing Completeness/document ...
03:24:06 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
03:24:06 Preparing Epistemic_Logic/document ...
03:24:06 Finished Types_Tableaus_and_Goedels_God/document (0:00:05 elapsed time)
03:24:06 Preparing Types_Tableaus_and_Goedels_God/outline ...
03:24:07 Optimal_BST: theory Optimal_BST.Weighted_Path_Length
03:24:07 Optimal_BST: theory Optimal_BST.Optimal_BST_Examples
03:24:07 Optimal_BST: theory Optimal_BST.Quadrilateral_Inequality
03:24:08 Optimal_BST: theory Optimal_BST.Optimal_BST
03:24:08 Finished Euler_Partition/outline (0:00:02 elapsed time)
03:24:08 Timing Euler_Partition (4 threads, 12.495s elapsed time, 37.167s cpu time, 1.100s GC time, factor 2.97)
03:24:08 Finished Euler_Partition (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.63)
03:24:08 Running Old_Datatype_Show ...
03:24:08 Finished KD_Tree/outline (0:00:03 elapsed time)
03:24:08 Timing KD_Tree (4 threads, 13.084s elapsed time, 46.846s cpu time, 1.280s GC time, factor 3.58)
03:24:08 Finished KD_Tree (0:00:17 elapsed time, 0:00:50 cpu time, factor 2.93)
03:24:08 Building Bell_Numbers_Spivey ...
03:24:09 Optimal_BST: theory Optimal_BST.Optimal_BST_Memo
03:24:09 Finished Completeness/document (0:00:03 elapsed time)
03:24:09 Preparing Completeness/outline ...
03:24:09 Optimal_BST: theory Optimal_BST.Optimal_BST2
03:24:09 Finished Inductive_Confidentiality/document (0:00:07 elapsed time)
03:24:09 Preparing Inductive_Confidentiality/outline ...
03:24:10 Preparing Constructor_Funs/document ...
03:24:10 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
03:24:11 Optimal_BST: theory Optimal_BST.Optimal_BST_Code
03:24:11 Finished Types_Tableaus_and_Goedels_God/outline (0:00:04 elapsed time)
03:24:11 Timing Types_Tableaus_and_Goedels_God (4 threads, 13.034s elapsed time, 25.470s cpu time, 0.388s GC time, factor 1.95)
03:24:11 Finished Types_Tableaus_and_Goedels_God (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.77)
03:24:11 Running PropResPI ...
03:24:11 Euler_MacLaurin: theory Landau_Symbols.Landau_More
03:24:11 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
03:24:11 Finished Constructor_Funs/document (0:00:01 elapsed time)
03:24:11 Preparing Constructor_Funs/outline ...
03:24:12 Bell_Numbers_Spivey: theory HOL-Eisbach.Eisbach
03:24:12 Bell_Numbers_Spivey: theory HOL-Combinatorics.Stirling
03:24:12 Bell_Numbers_Spivey: theory Card_Partitions.Set_Partition
03:24:12 Finished Completeness/outline (0:00:02 elapsed time)
03:24:12 Timing Completeness (4 threads, 12.146s elapsed time, 38.718s cpu time, 1.252s GC time, factor 3.19)
03:24:12 Finished Completeness (0:00:14 elapsed time, 0:00:41 cpu time, factor 2.75)
03:24:12 Running Abstract_Soundness ...
03:24:12 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
03:24:13 Finished Epistemic_Logic/document (0:00:06 elapsed time)
03:24:13 Preparing Epistemic_Logic/outline ...
03:24:13 PropResPI: theory PropResPI.Propositional_Resolution
03:24:13 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
03:24:13 Bell_Numbers_Spivey: theory Card_Partitions.Injectivity_Solver
03:24:13 Finished Constructor_Funs/outline (0:00:01 elapsed time)
03:24:13 Bell_Numbers_Spivey: theory Card_Partitions.Card_Partitions
03:24:13 Timing Constructor_Funs (4 threads, 10.790s elapsed time, 7.459s cpu time, 0.376s GC time, factor 0.69)
03:24:13 Finished Constructor_Funs (0:00:13 elapsed time, 0:00:09 cpu time, factor 0.72)
03:24:13 Running Category2 ...
03:24:14 Bell_Numbers_Spivey: theory Bell_Numbers_Spivey.Bell_Numbers
03:24:14 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
03:24:15 Finished Inductive_Confidentiality/outline (0:00:05 elapsed time)
03:24:15 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
03:24:15 Timing Inductive_Confidentiality (4 threads, 12.712s elapsed time, 40.024s cpu time, 1.488s GC time, factor 3.15)
03:24:15 Finished Inductive_Confidentiality (0:00:15 elapsed time, 0:00:42 cpu time, factor 2.78)
03:24:15 Running Catalan_Numbers ...
03:24:15 Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
03:24:16 Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
03:24:17 Preparing Euler_MacLaurin/document ...
03:24:17 Category2: theory HOL-ZF.LProd
03:24:17 Category2: theory Category2.Category
03:24:17 Category2: theory HOL-ZF.HOLZF
03:24:17 PropResPI: theory PropResPI.Prime_Implicates
03:24:17 Finished Epistemic_Logic/outline (0:00:04 elapsed time)
03:24:18 Category2: theory HOL-ZF.Zet
03:24:18 Category2: theory HOL-ZF.MainZF
03:24:18 Category2: theory Category2.Functors
03:24:18 Timing Epistemic_Logic (4 threads, 7.666s elapsed time, 17.189s cpu time, 0.661s GC time, factor 2.24)
03:24:18 Finished Epistemic_Logic (0:00:30 elapsed time, 0:00:51 cpu time, factor 1.70)
03:24:18 Running Neumann_Morgenstern_Utility ...
03:24:18 Category2: theory Category2.Universe
03:24:18 Category2: theory Category2.MonadicEquationalTheory
03:24:18 Catalan_Numbers: theory HOL-Library.Function_Algebras
03:24:18 Catalan_Numbers: theory HOL-Library.Landau_Symbols
03:24:18 Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
03:24:18 Catalan_Numbers: theory Landau_Symbols.Group_Sort
03:24:19 Preparing Optimal_BST/document ...
03:24:19 Category2: theory Category2.NatTrans
03:24:19 Category2: theory Category2.SetCat
03:24:21 Category2: theory Category2.Yoneda
03:24:22 Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
03:24:22 Finished Combinatorics_Words/document (0:00:18 elapsed time)
03:24:22 Preparing Combinatorics_Words/manual ...
03:24:22 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
03:24:22 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
03:24:22 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
03:24:23 Finished Euler_MacLaurin/document (0:00:05 elapsed time)
03:24:23 Preparing Euler_MacLaurin/outline ...
03:24:23 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
03:24:24 Finished Optimal_BST/document (0:00:04 elapsed time)
03:24:24 Preparing Optimal_BST/outline ...
03:24:24 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
03:24:24 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
03:24:25 Timing Old_Datatype_Show (4 threads, 11.300s elapsed time, 13.799s cpu time, 0.577s GC time, factor 1.22)
03:24:25 Finished Old_Datatype_Show (0:00:16 elapsed time, 0:00:18 cpu time, factor 1.12)
03:24:25 Running MonoBoolTranAlgebra ...
03:24:26 Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
03:24:26 Preparing PropResPI/document ...
03:24:27 Finished Euler_MacLaurin/outline (0:00:03 elapsed time)
03:24:27 MonoBoolTranAlgebra: theory LatticeProperties.WellFoundedTransitive
03:24:27 Timing Euler_MacLaurin (4 threads, 11.176s elapsed time, 41.682s cpu time, 1.236s GC time, factor 3.73)
03:24:27 Finished Euler_MacLaurin (0:00:16 elapsed time, 0:00:46 cpu time, factor 2.80)
03:24:27 MonoBoolTranAlgebra: theory LatticeProperties.Conj_Disj
03:24:27 Running BNF_Operations ...
03:24:27 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
03:24:27 Catalan_Numbers: theory Landau_Symbols.Landau_More
03:24:27 Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
03:24:27 MonoBoolTranAlgebra: theory LatticeProperties.Complete_Lattice_Prop
03:24:28 Finished Optimal_BST/outline (0:00:03 elapsed time)
03:24:28 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran
03:24:28 Timing Optimal_BST (4 threads, 11.065s elapsed time, 42.182s cpu time, 0.915s GC time, factor 3.81)
03:24:28 Finished Optimal_BST (0:00:14 elapsed time, 0:00:45 cpu time, factor 3.12)
03:24:28 Running Fermat3_4 ...
03:24:29 BNF_Operations: theory HOL-Library.BNF_Axiomatization
03:24:29 Preparing Abstract_Soundness/document ...
03:24:29 BNF_Operations: theory BNF_Operations.GFP
03:24:29 BNF_Operations: theory BNF_Operations.Kill
03:24:29 BNF_Operations: theory BNF_Operations.Compose
03:24:29 BNF_Operations: theory BNF_Operations.LFP
03:24:29 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
03:24:29 BNF_Operations: theory BNF_Operations.Lift
03:24:30 Preparing Category2/document ...
03:24:30 BNF_Operations: theory BNF_Operations.N2M
03:24:30 BNF_Operations: theory BNF_Operations.Permute
03:24:31 Finished PropResPI/document (0:00:04 elapsed time)
03:24:31 Preparing PropResPI/outline ...
03:24:31 Preparing Catalan_Numbers/document ...
03:24:32 Finished Abstract_Soundness/document (0:00:03 elapsed time)
03:24:32 Preparing Abstract_Soundness/outline ...
03:24:33 Finished Combinatorics_Words/manual (0:00:10 elapsed time)
03:24:33 Fermat3_4: theory Fermat3_4.Quad_Form
03:24:33 Fermat3_4: theory Fermat3_4.Fermat4
03:24:33 Finished PropResPI/outline (0:00:02 elapsed time)
03:24:34 Timing Combinatorics_Words (4 threads, 8.701s elapsed time, 27.377s cpu time, 1.135s GC time, factor 3.15)
03:24:34 Finished Combinatorics_Words (0:00:33 elapsed time, 0:01:01 cpu time, factor 1.83)
03:24:34 Timing PropResPI (4 threads, 12.543s elapsed time, 30.476s cpu time, 0.869s GC time, factor 2.43)
03:24:34 Finished PropResPI (0:00:15 elapsed time, 0:00:32 cpu time, factor 2.18)
03:24:34 Running Lower_Semicontinuous ...
03:24:34 Running Lam-ml-Normalization ...
03:24:34 Fermat3_4: theory Fermat3_4.Fermat3
03:24:35 Preparing Neumann_Morgenstern_Utility/document ...
03:24:35 Finished Catalan_Numbers/document (0:00:03 elapsed time)
03:24:35 Preparing Catalan_Numbers/outline ...
03:24:35 Finished Abstract_Soundness/outline (0:00:03 elapsed time)
03:24:36 Lam-ml-Normalization: theory HOL-Library.LaTeXsugar
03:24:36 Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
03:24:36 Timing Abstract_Soundness (4 threads, 12.468s elapsed time, 28.648s cpu time, 1.327s GC time, factor 2.30)
03:24:36 Finished Abstract_Soundness (0:00:16 elapsed time, 0:00:32 cpu time, factor 1.95)
03:24:36 Running Recursion-Theory-I ...
03:24:36 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Assertion_Algebra
03:24:36 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Statements
03:24:37 Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
03:24:38 Recursion-Theory-I: theory Recursion-Theory-I.CPair
03:24:38 Preparing MonoBoolTranAlgebra/document ...
03:24:38 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun
03:24:38 Finished Catalan_Numbers/outline (0:00:03 elapsed time)
03:24:39 Timing Catalan_Numbers (4 threads, 11.681s elapsed time, 43.274s cpu time, 1.694s GC time, factor 3.70)
03:24:39 Finished Catalan_Numbers (0:00:15 elapsed time, 0:00:47 cpu time, factor 2.98)
03:24:39 Running MiniML ...
03:24:39 Preparing Bell_Numbers_Spivey/document ...
03:24:40 Finished Category2/document (0:00:10 elapsed time)
03:24:40 Preparing Category2/outline ...
03:24:40 Preparing BNF_Operations/document ...
03:24:40 Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet
03:24:40 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2
03:24:40 Recursion-Theory-I: theory Recursion-Theory-I.PRecList
03:24:40 Finished Neumann_Morgenstern_Utility/document (0:00:05 elapsed time)
03:24:40 Preparing Neumann_Morgenstern_Utility/outline ...
03:24:41 MiniML: theory MiniML.Maybe
03:24:41 MiniML: theory MiniML.Type
03:24:43 Finished Bell_Numbers_Spivey/document (0:00:03 elapsed time)
03:24:43 Preparing Bell_Numbers_Spivey/outline ...
03:24:43 Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr
03:24:43 Finished MonoBoolTranAlgebra/document (0:00:05 elapsed time)
03:24:43 Preparing MonoBoolTranAlgebra/outline ...
03:24:44 MiniML: theory MiniML.Instance
03:24:44 Finished Neumann_Morgenstern_Utility/outline (0:00:03 elapsed time)
03:24:44 MiniML: theory MiniML.Generalize
03:24:44 MiniML: theory MiniML.MiniML
03:24:44 Preparing Fermat3_4/document ...
03:24:45 Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet
03:24:45 Timing Neumann_Morgenstern_Utility (4 threads, 11.544s elapsed time, 40.129s cpu time, 0.824s GC time, factor 3.48)
03:24:45 Finished Neumann_Morgenstern_Utility (0:00:16 elapsed time, 0:00:44 cpu time, factor 2.73)
03:24:45 Running FeatherweightJava ...
03:24:45 Finished Category2/outline (0:00:05 elapsed time)
03:24:45 MiniML: theory MiniML.W
03:24:45 Timing Category2 (4 threads, 11.498s elapsed time, 42.893s cpu time, 2.436s GC time, factor 3.73)
03:24:45 Finished Category2 (0:00:15 elapsed time, 0:00:46 cpu time, factor 3.00)
03:24:45 Running JiveDataStoreModel ...
03:24:46 Finished Bell_Numbers_Spivey/outline (0:00:02 elapsed time)
03:24:46 Timing Bell_Numbers_Spivey (4 threads, 10.118s elapsed time, 34.031s cpu time, 0.657s GC time, factor 3.36)
03:24:46 Finished Bell_Numbers_Spivey (0:00:30 elapsed time, 0:01:04 cpu time, factor 2.13)
03:24:46 Running IMO2019 ...
03:24:46 Preparing Lam-ml-Normalization/document ...
03:24:47 FeatherweightJava: theory FeatherweightJava.FJDefs
03:24:47 Finished MonoBoolTranAlgebra/outline (0:00:03 elapsed time)
03:24:47 JiveDataStoreModel: theory JiveDataStoreModel.TypeIds
03:24:47 Timing MonoBoolTranAlgebra (4 threads, 10.339s elapsed time, 19.003s cpu time, 0.594s GC time, factor 1.84)
03:24:47 Finished MonoBoolTranAlgebra (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.65)
03:24:47 Running Orbit_Stabiliser ...
03:24:48 Finished BNF_Operations/document (0:00:07 elapsed time)
03:24:48 Preparing BNF_Operations/outline ...
03:24:49 Preparing Lower_Semicontinuous/document ...
03:24:49 Preparing Recursion-Theory-I/document ...
03:24:49 JiveDataStoreModel: theory JiveDataStoreModel.JavaType
03:24:51 Finished Fermat3_4/document (0:00:06 elapsed time)
03:24:51 Preparing Fermat3_4/outline ...
03:24:51 FeatherweightJava: theory FeatherweightJava.FJAux
03:24:51 Preparing MiniML/document ...
03:24:51 FeatherweightJava: theory FeatherweightJava.FJSound
03:24:51 JiveDataStoreModel: theory JiveDataStoreModel.DirectSubtypes
03:24:51 JiveDataStoreModel: theory JiveDataStoreModel.Subtype
03:24:51 Finished Lam-ml-Normalization/document (0:00:04 elapsed time)
03:24:51 Preparing Lam-ml-Normalization/outline ...
03:24:51 Finished BNF_Operations/outline (0:00:03 elapsed time)
03:24:51 IMO2019: theory IMO2019.IMO2019_Q5
03:24:51 Timing BNF_Operations (4 threads, 9.721s elapsed time, 36.677s cpu time, 3.282s GC time, factor 3.77)
03:24:51 Finished BNF_Operations (0:00:12 elapsed time, 0:00:38 cpu time, factor 3.15)
03:24:51 Running Error_Function ...
03:24:51 IMO2019: theory IMO2019.IMO2019_Q1
03:24:51 IMO2019: theory IMO2019.IMO2019_Q4
03:24:51 FeatherweightJava: theory FeatherweightJava.Execute
03:24:51 JiveDataStoreModel: theory JiveDataStoreModel.Attributes
03:24:51 JiveDataStoreModel: theory JiveDataStoreModel.Value
03:24:52 Finished Lower_Semicontinuous/document (0:00:03 elapsed time)
03:24:52 Preparing Lower_Semicontinuous/outline ...
03:24:53 JiveDataStoreModel: theory JiveDataStoreModel.AttributesIndep
03:24:53 JiveDataStoreModel: theory JiveDataStoreModel.Location
03:24:54 JiveDataStoreModel: theory JiveDataStoreModel.Store
03:24:54 Finished Fermat3_4/outline (0:00:03 elapsed time)
03:24:54 Finished Lower_Semicontinuous/outline (0:00:02 elapsed time)
03:24:54 Timing Fermat3_4 (4 threads, 10.025s elapsed time, 38.546s cpu time, 0.761s GC time, factor 3.84)
03:24:54 Finished Fermat3_4 (0:00:15 elapsed time, 0:00:44 cpu time, factor 2.76)
03:24:54 Timing Lower_Semicontinuous (4 threads, 10.330s elapsed time, 23.652s cpu time, 0.333s GC time, factor 2.29)
03:24:54 Finished Lower_Semicontinuous (0:00:14 elapsed time, 0:00:27 cpu time, factor 1.89)
03:24:54 Running CryptoBasedCompositionalProperties ...
03:24:54 Running Pratt_Certificate ...
03:24:54 FeatherweightJava: theory FeatherweightJava.Featherweight_Java
03:24:54 Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset
03:24:55 Error_Function: theory HOL-Library.Function_Algebras
03:24:55 Error_Function: theory Error_Function.Error_Function
03:24:55 Error_Function: theory Landau_Symbols.Group_Sort
03:24:55 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
03:24:55 Finished MiniML/document (0:00:03 elapsed time)
03:24:55 Preparing MiniML/outline ...
03:24:55 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
03:24:55 Finished Lam-ml-Normalization/outline (0:00:04 elapsed time)
03:24:55 Timing Lam-ml-Normalization (4 threads, 9.961s elapsed time, 20.956s cpu time, 0.740s GC time, factor 2.10)
03:24:55 Finished Lam-ml-Normalization (0:00:12 elapsed time, 0:00:23 cpu time, factor 1.86)
03:24:55 Running Robbins-Conjecture ...
03:24:55 JiveDataStoreModel: theory JiveDataStoreModel.StoreProperties
03:24:56 JiveDataStoreModel: theory JiveDataStoreModel.JML
03:24:56 JiveDataStoreModel: theory JiveDataStoreModel.UnivSpec
03:24:56 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.ListExtras
03:24:56 Preparing FeatherweightJava/document ...
03:24:57 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy_types
03:24:57 Error_Function: theory Landau_Symbols.Landau_Real_Products
03:24:57 Robbins-Conjecture: theory Robbins-Conjecture.Robbins_Conjecture
03:24:58 Preparing JiveDataStoreModel/document ...
03:24:58 Finished MiniML/outline (0:00:03 elapsed time)
03:24:58 Timing MiniML (4 threads, 9.644s elapsed time, 21.442s cpu time, 0.604s GC time, factor 2.22)
03:24:58 Finished MiniML (0:00:12 elapsed time, 0:00:23 cpu time, factor 1.95)
03:24:58 Running Skip_Lists ...
03:24:59 Pratt_Certificate: theory Lehmer.Lehmer
03:25:00 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
03:25:01 Error_Function: theory Landau_Symbols.Landau_Simprocs
03:25:01 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.inout
03:25:01 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy
03:25:01 Finished Recursion-Theory-I/document (0:00:12 elapsed time)
03:25:01 Preparing Recursion-Theory-I/outline ...
03:25:02 Finished FeatherweightJava/document (0:00:05 elapsed time)
03:25:02 Preparing FeatherweightJava/outline ...
03:25:02 Error_Function: theory Landau_Symbols.Landau_More
03:25:02 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.CompLocalSecrets
03:25:02 Error_Function: theory Error_Function.Error_Function_Asymptotics
03:25:02 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
03:25:02 Skip_Lists: theory Skip_Lists.Pi_pmf
03:25:02 Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
03:25:02 Skip_Lists: theory Skip_Lists.Misc
03:25:03 Preparing IMO2019/document ...
03:25:04 Skip_Lists: theory Skip_Lists.Geometric_PMF
03:25:04 Finished JiveDataStoreModel/document (0:00:05 elapsed time)
03:25:04 Preparing JiveDataStoreModel/outline ...
03:25:04 Skip_Lists: theory Skip_Lists.Skip_List
03:25:04 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
03:25:05 Preparing Orbit_Stabiliser/document ...
03:25:05 Preparing Error_Function/document ...
03:25:06 Finished FeatherweightJava/outline (0:00:04 elapsed time)
03:25:06 Timing FeatherweightJava (4 threads, 8.979s elapsed time, 25.765s cpu time, 0.739s GC time, factor 2.87)
03:25:06 Finished FeatherweightJava (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.46)
03:25:06 Running Rank_Nullity_Theorem ...
03:25:07 Finished IMO2019/document (0:00:03 elapsed time)
03:25:07 Preparing IMO2019/outline ...
03:25:07 Preparing CryptoBasedCompositionalProperties/document ...
03:25:07 Preparing Robbins-Conjecture/document ...
03:25:07 Finished Recursion-Theory-I/outline (0:00:05 elapsed time)
03:25:07 Timing Recursion-Theory-I (4 threads, 9.597s elapsed time, 34.438s cpu time, 1.390s GC time, factor 3.59)
03:25:07 Finished Recursion-Theory-I (0:00:12 elapsed time, 0:00:36 cpu time, factor 3.01)
03:25:07 Running HyperCTL ...
03:25:08 Finished Error_Function/document (0:00:02 elapsed time)
03:25:08 Preparing Error_Function/outline ...
03:25:08 Finished JiveDataStoreModel/outline (0:00:04 elapsed time)
03:25:08 Timing JiveDataStoreModel (4 threads, 9.710s elapsed time, 26.125s cpu time, 1.069s GC time, factor 2.69)
03:25:08 Finished JiveDataStoreModel (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.31)
03:25:08 Running Stream-Fusion ...
03:25:09 Finished Orbit_Stabiliser/document (0:00:04 elapsed time)
03:25:09 Preparing Orbit_Stabiliser/outline ...
03:25:09 Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
03:25:09 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
03:25:09 Finished Robbins-Conjecture/document (0:00:02 elapsed time)
03:25:09 Preparing Robbins-Conjecture/outline ...
03:25:10 Finished IMO2019/outline (0:00:03 elapsed time)
03:25:10 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
03:25:10 Timing IMO2019 (4 threads, 10.476s elapsed time, 16.216s cpu time, 0.209s GC time, factor 1.55)
03:25:10 Finished IMO2019 (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.32)
03:25:10 Running Strong_Security ...
03:25:10 Finished Error_Function/outline (0:00:02 elapsed time)
03:25:10 Preparing Pratt_Certificate/document ...
03:25:10 Stream-Fusion: theory HOLCF-Library.Int_Discrete
03:25:10 Timing Error_Function (4 threads, 9.290s elapsed time, 31.800s cpu time, 0.957s GC time, factor 3.42)
03:25:10 Finished Error_Function (0:00:13 elapsed time, 0:00:35 cpu time, factor 2.66)
03:25:10 Running Transformer_Semantics ...
03:25:10 Stream-Fusion: theory Stream-Fusion.LazyList
03:25:11 Finished CryptoBasedCompositionalProperties/document (0:00:03 elapsed time)
03:25:11 Preparing CryptoBasedCompositionalProperties/outline ...
03:25:11 HyperCTL: theory HyperCTL.Prelim
03:25:11 HyperCTL: theory HyperCTL.Shallow
03:25:11 Finished Robbins-Conjecture/outline (0:00:01 elapsed time)
03:25:11 Timing Robbins-Conjecture (4 threads, 9.047s elapsed time, 22.994s cpu time, 0.453s GC time, factor 2.54)
03:25:11 Finished Robbins-Conjecture (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.18)
03:25:11 Running RefinementReactive ...
03:25:11 HyperCTL: theory HyperCTL.Deep
03:25:11 HyperCTL: theory HyperCTL.Noninterference
03:25:12 Stream-Fusion: theory Stream-Fusion.Stream
03:25:12 Strong_Security: theory Strong_Security.Types
03:25:12 Strong_Security: theory Strong_Security.Expr
03:25:12 Strong_Security: theory Strong_Security.Strong_Security
03:25:12 Strong_Security: theory Strong_Security.MWLf
03:25:12 Strong_Security: theory Strong_Security.Up_To_Technique
03:25:12 Finished Orbit_Stabiliser/outline (0:00:03 elapsed time)
03:25:12 Strong_Security: theory Strong_Security.Parallel_Composition
03:25:12 Preparing Skip_Lists/document ...
03:25:12 Timing Orbit_Stabiliser (4 threads, 9.142s elapsed time, 20.369s cpu time, 0.495s GC time, factor 2.23)
03:25:12 Finished Orbit_Stabiliser (0:00:17 elapsed time, 0:00:28 cpu time, factor 1.62)
03:25:12 Running Randomised_BSTs ...
03:25:13 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
03:25:13 Strong_Security: theory Strong_Security.Domain_example
03:25:13 RefinementReactive: theory RefinementReactive.Temporal
03:25:13 RefinementReactive: theory RefinementReactive.Refinement
03:25:14 Stream-Fusion: theory Stream-Fusion.StreamFusion
03:25:14 Finished CryptoBasedCompositionalProperties/outline (0:00:03 elapsed time)
03:25:14 Finished Pratt_Certificate/document (0:00:03 elapsed time)
03:25:14 Preparing Pratt_Certificate/outline ...
03:25:14 Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
03:25:14 Timing CryptoBasedCompositionalProperties (4 threads, 9.758s elapsed time, 24.893s cpu time, 0.665s GC time, factor 2.55)
03:25:14 Finished CryptoBasedCompositionalProperties (0:00:12 elapsed time, 0:00:26 cpu time, factor 2.22)
03:25:14 Running Integration ...
03:25:15 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
03:25:15 Strong_Security: theory Strong_Security.Language_Composition
03:25:15 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
03:25:15 Strong_Security: theory Strong_Security.Type_System
03:25:15 Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
03:25:15 Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
03:25:15 HyperCTL: theory HyperCTL.Finite_Noninterference
03:25:15 RefinementReactive: theory RefinementReactive.Reactive
03:25:16 Strong_Security: theory Strong_Security.Type_System_example
03:25:16 HyperCTL: theory HyperCTL.HyperCTL
03:25:16 Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
03:25:17 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
03:25:18 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
03:25:18 Finished Pratt_Certificate/outline (0:00:03 elapsed time)
03:25:18 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
03:25:18 Integration: theory Integration.MonConv
03:25:18 Integration: theory Integration.Sigma_Algebra
03:25:18 Timing Pratt_Certificate (4 threads, 9.864s elapsed time, 32.865s cpu time, 0.573s GC time, factor 3.33)
03:25:18 Finished Pratt_Certificate (0:00:15 elapsed time, 0:00:38 cpu time, factor 2.44)
03:25:18 Running Landau_Symbols ...
03:25:18 Preparing Rank_Nullity_Theorem/document ...
03:25:18 Integration: theory Integration.Measure
03:25:19 Finished Skip_Lists/document (0:00:06 elapsed time)
03:25:19 Preparing Skip_Lists/outline ...
03:25:19 Integration: theory Integration.RealRandVar
03:25:19 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
03:25:20 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
03:25:20 Integration: theory Integration.Failure
03:25:20 Integration: theory Integration.Integral
03:25:21 Preparing Stream-Fusion/document ...
03:25:21 Preparing HyperCTL/document ...
03:25:22 Landau_Symbols: theory Landau_Symbols.Group_Sort
03:25:23 Preparing Strong_Security/document ...
03:25:23 Finished Skip_Lists/outline (0:00:04 elapsed time)
03:25:23 Preparing RefinementReactive/document ...
03:25:23 Timing Skip_Lists (4 threads, 9.006s elapsed time, 32.583s cpu time, 0.553s GC time, factor 3.62)
03:25:23 Finished Skip_Lists (0:00:13 elapsed time, 0:00:36 cpu time, factor 2.72)
03:25:23 Running GPU_Kernel_PL ...
03:25:23 Finished Rank_Nullity_Theorem/document (0:00:05 elapsed time)
03:25:23 Preparing Rank_Nullity_Theorem/outline ...
03:25:24 Landau_Symbols: theory Landau_Symbols.Landau_Real_Products
03:25:25 Finished Stream-Fusion/document (0:00:03 elapsed time)
03:25:25 Preparing Stream-Fusion/outline ...
03:25:25 Finished HyperCTL/document (0:00:03 elapsed time)
03:25:25 Preparing HyperCTL/outline ...
03:25:25 GPU_Kernel_PL: theory GPU_Kernel_PL.Misc
03:25:25 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax
03:25:26 Preparing Transformer_Semantics/document ...
03:25:27 Finished Rank_Nullity_Theorem/outline (0:00:03 elapsed time)
03:25:27 Timing Rank_Nullity_Theorem (4 threads, 8.181s elapsed time, 17.594s cpu time, 0.599s GC time, factor 2.15)
03:25:27 Finished Rank_Nullity_Theorem (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.75)
03:25:27 Finished HyperCTL/outline (0:00:02 elapsed time)
03:25:27 Running Card_Multisets ...
03:25:27 Preparing Randomised_BSTs/document ...
03:25:27 Finished Strong_Security/document (0:00:04 elapsed time)
03:25:27 Preparing Strong_Security/outline ...
03:25:28 Timing HyperCTL (4 threads, 9.700s elapsed time, 33.743s cpu time, 1.381s GC time, factor 3.48)
03:25:28 Finished HyperCTL (0:00:13 elapsed time, 0:00:37 cpu time, factor 2.73)
03:25:28 Running Lowe_Ontological_Argument ...
03:25:28 Preparing Integration/document ...
03:25:28 Finished Stream-Fusion/outline (0:00:03 elapsed time)
03:25:28 Finished RefinementReactive/document (0:00:04 elapsed time)
03:25:28 Preparing RefinementReactive/outline ...
03:25:28 Timing Stream-Fusion (4 threads, 9.739s elapsed time, 14.775s cpu time, 0.348s GC time, factor 1.52)
03:25:28 Finished Stream-Fusion (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.40)
03:25:28 Running WorkerWrapper ...
03:25:28 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state
03:25:28 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness
03:25:28 Landau_Symbols: theory Landau_Symbols.Landau_Simprocs
03:25:29 Landau_Symbols: theory Landau_Symbols.Landau_More
03:25:29 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread
03:25:29 Card_Multisets: theory HOL-Library.Cancellation
03:25:29 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.Relations
03:25:29 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.QML
03:25:30 Card_Multisets: theory HOL-Library.Multiset
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
03:25:30 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
03:25:30 WorkerWrapper: theory WorkerWrapper.Nats
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
03:25:30 WorkerWrapper: theory WorkerWrapper.Maybe
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
03:25:30 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
03:25:30 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel
03:25:31 Finished Strong_Security/outline (0:00:03 elapsed time)
03:25:31 Finished Transformer_Semantics/document (0:00:05 elapsed time)
03:25:31 Preparing Transformer_Semantics/outline ...
03:25:31 Preparing Landau_Symbols/document ...
03:25:31 Timing Strong_Security (4 threads, 10.171s elapsed time, 34.330s cpu time, 0.952s GC time, factor 3.38)
03:25:31 Finished Strong_Security (0:00:12 elapsed time, 0:00:36 cpu time, factor 2.87)
03:25:31 Running Nullstellensatz ...
03:25:31 WorkerWrapper: theory WorkerWrapper.LList
03:25:32 Finished Randomised_BSTs/document (0:00:04 elapsed time)
03:25:32 Preparing Randomised_BSTs/outline ...
03:25:32 Finished RefinementReactive/outline (0:00:03 elapsed time)
03:25:32 Timing RefinementReactive (4 threads, 8.652s elapsed time, 24.085s cpu time, 0.541s GC time, factor 2.78)
03:25:32 Finished RefinementReactive (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.35)
03:25:32 Running Separata ...
03:25:33 GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language
03:25:34 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
03:25:34 Finished Integration/document (0:00:06 elapsed time)
03:25:34 Preparing Integration/outline ...
03:25:34 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
03:25:34 WorkerWrapper: theory WorkerWrapper.CounterExample
03:25:34 WorkerWrapper: theory WorkerWrapper.Streams
03:25:34 WorkerWrapper: theory WorkerWrapper.Last
03:25:34 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
03:25:34 WorkerWrapper: theory WorkerWrapper.Accumulator
03:25:34 Preparing GPU_Kernel_PL/document ...
03:25:35 WorkerWrapper: theory WorkerWrapper.Backtracking
03:25:35 WorkerWrapper: theory WorkerWrapper.Continuations
03:25:35 WorkerWrapper: theory WorkerWrapper.Nub
03:25:35 WorkerWrapper: theory WorkerWrapper.UnboxedNats
03:25:36 Finished Landau_Symbols/document (0:00:04 elapsed time)
03:25:36 Preparing Landau_Symbols/outline ...
03:25:36 Finished Randomised_BSTs/outline (0:00:03 elapsed time)
03:25:36 Finished Transformer_Semantics/outline (0:00:05 elapsed time)
03:25:36 Timing Randomised_BSTs (4 threads, 9.493s elapsed time, 32.829s cpu time, 0.749s GC time, factor 3.46)
03:25:36 Finished Randomised_BSTs (0:00:14 elapsed time, 0:00:37 cpu time, factor 2.60)
03:25:36 Timing Transformer_Semantics (4 threads, 9.566s elapsed time, 34.369s cpu time, 1.125s GC time, factor 3.59)
03:25:36 Finished Transformer_Semantics (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.64)
03:25:36 Running Attack_Trees ...
03:25:36 Separata: theory HOL-Eisbach.Eisbach
03:25:36 Running Belief_Revision ...
03:25:36 Separata: theory Separation_Algebra.Separation_Algebra
03:25:36 Card_Multisets: theory Card_Multisets.Card_Multisets
03:25:38 Separata: theory HOL-Eisbach.Eisbach_Tools
03:25:38 Separata: theory Separata.Separata
03:25:38 Finished GPU_Kernel_PL/document (0:00:03 elapsed time)
03:25:38 Preparing GPU_Kernel_PL/outline ...
03:25:38 Belief_Revision: theory Belief_Revision.AGM_Logic
03:25:38 Attack_Trees: theory Attack_Trees.MC
03:25:39 Finished Landau_Symbols/outline (0:00:03 elapsed time)
03:25:39 Belief_Revision: theory Belief_Revision.AGM_Remainder
03:25:39 Finished Integration/outline (0:00:05 elapsed time)
03:25:39 Belief_Revision: theory Belief_Revision.AGM_Contraction
03:25:39 Timing Integration (4 threads, 8.533s elapsed time, 19.586s cpu time, 0.525s GC time, factor 2.30)
03:25:39 Finished Integration (0:00:12 elapsed time, 0:00:23 cpu time, factor 1.84)
03:25:39 Timing Landau_Symbols (4 threads, 8.043s elapsed time, 23.234s cpu time, 0.862s GC time, factor 2.89)
03:25:39 Finished Landau_Symbols (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.17)
03:25:39 Running Noninterference_Concurrent_Composition ...
03:25:39 Running Tycon ...
03:25:39 Preparing Lowe_Ontological_Argument/document ...
03:25:40 Attack_Trees: theory Attack_Trees.AT
03:25:40 Belief_Revision: theory Belief_Revision.AGM_Revision
03:25:40 Preparing WorkerWrapper/document ...
03:25:40 Preparing Card_Multisets/document ...
03:25:41 Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
03:25:41 Tycon: theory Tycon.Coerce
03:25:41 Tycon: theory Tycon.TypeApp
03:25:41 Tycon: theory Tycon.Functor
03:25:42 Finished GPU_Kernel_PL/outline (0:00:03 elapsed time)
03:25:42 Timing GPU_Kernel_PL (4 threads, 8.724s elapsed time, 16.308s cpu time, 0.864s GC time, factor 1.87)
03:25:42 Finished GPU_Kernel_PL (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.64)
03:25:42 Running Huffman ...
03:25:42 Attack_Trees: theory Attack_Trees.Infrastructure
03:25:43 Finished Lowe_Ontological_Argument/document (0:00:03 elapsed time)
03:25:43 Preparing Lowe_Ontological_Argument/outline ...
03:25:43 Huffman: theory Huffman.Huffman
03:25:44 Finished Card_Multisets/document (0:00:03 elapsed time)
03:25:44 Preparing Card_Multisets/outline ...
03:25:44 Tycon: theory Tycon.Monad
03:25:44 Tycon: theory Tycon.Binary_Tree_Monad
03:25:44 Tycon: theory Tycon.Lift_Monad
03:25:44 Tycon: theory Tycon.Monad_Plus
03:25:44 Tycon: theory Tycon.Monad_Zero
03:25:44 Tycon: theory Tycon.Writer_Monad
03:25:44 Attack_Trees: theory Attack_Trees.GDPRhealthcare
03:25:45 Tycon: theory Tycon.Error_Monad
03:25:45 Tycon: theory Tycon.Resumption_Transformer
03:25:45 Tycon: theory Tycon.Monad_Zero_Plus
03:25:45 Tycon: theory Tycon.Writer_Transformer
03:25:45 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
03:25:45 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
03:25:45 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
03:25:45 Nullstellensatz: theory Nullstellensatz.Univariate_PM
03:25:45 Tycon: theory Tycon.Error_Transformer
03:25:45 Tycon: theory Tycon.Lazy_List_Monad
03:25:46 Finished WorkerWrapper/document (0:00:05 elapsed time)
03:25:46 Preparing WorkerWrapper/outline ...
03:25:46 Tycon: theory Tycon.Maybe_Monad
03:25:46 Tycon: theory Tycon.State_Transformer
03:25:46 Preparing Separata/document ...
03:25:47 Finished Card_Multisets/outline (0:00:03 elapsed time)
03:25:47 Timing Card_Multisets (4 threads, 10.370s elapsed time, 28.504s cpu time, 0.930s GC time, factor 2.75)
03:25:47 Finished Card_Multisets (0:00:12 elapsed time, 0:00:30 cpu time, factor 2.39)
03:25:47 Running Laplace_Transform ...
03:25:47 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
03:25:48 Tycon: theory Tycon.Monad_Transformer
03:25:48 Finished Lowe_Ontological_Argument/outline (0:00:04 elapsed time)
03:25:48 Timing Lowe_Ontological_Argument (4 threads, 9.247s elapsed time, 15.362s cpu time, 0.218s GC time, factor 1.66)
03:25:48 Finished Lowe_Ontological_Argument (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.49)
03:25:48 Running First_Welfare_Theorem ...
03:25:48 Preparing Attack_Trees/document ...
03:25:49 Finished Separata/document (0:00:02 elapsed time)
03:25:49 Preparing Separata/outline ...
03:25:49 Preparing Belief_Revision/document ...
03:25:50 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
03:25:50 Finished WorkerWrapper/outline (0:00:04 elapsed time)
03:25:50 Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
03:25:50 Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
03:25:50 Timing WorkerWrapper (4 threads, 9.481s elapsed time, 27.596s cpu time, 1.125s GC time, factor 2.91)
03:25:50 Finished WorkerWrapper (0:00:12 elapsed time, 0:00:29 cpu time, factor 2.48)
03:25:50 Running Selection_Heap_Sort ...
03:25:50 Preparing Tycon/document ...
03:25:50 Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
03:25:50 Preparing Noninterference_Concurrent_Composition/document ...
03:25:51 Laplace_Transform: theory Laplace_Transform.Existence
03:25:51 Finished Separata/outline (0:00:02 elapsed time)
03:25:51 Laplace_Transform: theory Laplace_Transform.Uniqueness
03:25:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
03:25:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
03:25:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
03:25:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
03:25:52 Timing Separata (4 threads, 9.499s elapsed time, 32.634s cpu time, 0.674s GC time, factor 3.44)
03:25:52 Finished Separata (0:00:14 elapsed time, 0:00:36 cpu time, factor 2.63)
03:25:52 Running VolpanoSmith ...
03:25:52 Laplace_Transform: theory Laplace_Transform.Laplace_Transform
03:25:53 Preparing Huffman/document ...
03:25:53 First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
03:25:53 First_Welfare_Theorem: theory First_Welfare_Theorem.Common
03:25:54 First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
03:25:54 Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
03:25:54 Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
03:25:54 VolpanoSmith: theory VolpanoSmith.Semantics
03:25:54 First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
03:25:54 First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
03:25:54 Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
03:25:54 Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
03:25:54 Finished Attack_Trees/document (0:00:05 elapsed time)
03:25:54 Preparing Attack_Trees/outline ...
03:25:55 Preparing Nullstellensatz/document ...
03:25:55 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
03:25:55 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
03:25:56 Finished Tycon/document (0:00:05 elapsed time)
03:25:56 Preparing Tycon/outline ...
03:25:57 Finished Belief_Revision/document (0:00:07 elapsed time)
03:25:57 Preparing Belief_Revision/outline ...
03:25:57 Finished Noninterference_Concurrent_Composition/document (0:00:06 elapsed time)
03:25:57 Preparing Noninterference_Concurrent_Composition/outline ...
03:25:57 Finished Huffman/document (0:00:03 elapsed time)
03:25:57 Preparing Huffman/outline ...
03:25:58 VolpanoSmith: theory VolpanoSmith.secTypes
03:25:59 Finished Attack_Trees/outline (0:00:04 elapsed time)
03:25:59 Timing Attack_Trees (4 threads, 9.159s elapsed time, 25.161s cpu time, 0.870s GC time, factor 2.75)
03:25:59 Finished Attack_Trees (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.31)
03:25:59 Running Hello_World ...
03:25:59 VolpanoSmith: theory VolpanoSmith.Execute
03:25:59 Preparing Laplace_Transform/document ...
03:26:00 Preparing First_Welfare_Theorem/document ...
03:26:00 Finished Huffman/outline (0:00:03 elapsed time)
03:26:01 Finished Noninterference_Concurrent_Composition/outline (0:00:03 elapsed time)
03:26:01 Timing Huffman (4 threads, 8.615s elapsed time, 25.283s cpu time, 0.563s GC time, factor 2.93)
03:26:01 Finished Huffman (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.48)
03:26:01 Timing Noninterference_Concurrent_Composition (4 threads, 8.117s elapsed time, 29.374s cpu time, 0.411s GC time, factor 3.62)
03:26:01 Finished Noninterference_Concurrent_Composition (0:00:10 elapsed time, 0:00:31 cpu time, factor 2.98)
03:26:01 Running Szemeredi_Regularity ...
03:26:01 Running LambdaMu ...
03:26:01 Hello_World: theory HOL-Library.Adhoc_Overloading
03:26:01 Finished Tycon/outline (0:00:04 elapsed time)
03:26:01 Hello_World: theory HOL-Library.Monad_Syntax
03:26:01 Hello_World: theory Hello_World.IO
03:26:01 Hello_World: theory Hello_World.HelloWorld
03:26:01 Timing Tycon (4 threads, 8.220s elapsed time, 23.278s cpu time, 0.845s GC time, factor 2.83)
03:26:01 Finished Tycon (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.36)
03:26:01 Running Impossible_Geometry ...
03:26:02 Preparing Selection_Heap_Sort/document ...
03:26:02 Finished Belief_Revision/outline (0:00:05 elapsed time)
03:26:02 Preparing VolpanoSmith/document ...
03:26:02 Finished Nullstellensatz/document (0:00:06 elapsed time)
03:26:02 Preparing Nullstellensatz/outline ...
03:26:02 Timing Belief_Revision (4 threads, 10.084s elapsed time, 33.190s cpu time, 0.647s GC time, factor 3.29)
03:26:02 Finished Belief_Revision (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.76)
03:26:02 Running Card_Partitions ...
03:26:03 LambdaMu: theory LambdaMu.Syntax
03:26:03 Impossible_Geometry: theory Impossible_Geometry.Impossible_Geometry
03:26:04 Szemeredi_Regularity: theory Girth_Chromatic.Girth_Chromatic_Misc
03:26:04 Card_Partitions: theory HOL-Eisbach.Eisbach
03:26:04 Card_Partitions: theory HOL-Combinatorics.Stirling
03:26:04 Card_Partitions: theory HOL-Library.Adhoc_Overloading
03:26:04 Card_Partitions: theory HOL-Library.FuncSet
03:26:04 Finished Laplace_Transform/document (0:00:05 elapsed time)
03:26:04 Preparing Laplace_Transform/outline ...
03:26:04 Szemeredi_Regularity: theory Girth_Chromatic.Ugraphs
03:26:04 Card_Partitions: theory HOL-Library.Monad_Syntax
03:26:05 Finished Selection_Heap_Sort/document (0:00:02 elapsed time)
03:26:05 Preparing Selection_Heap_Sort/outline ...
03:26:05 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
03:26:05 Card_Partitions: theory HOL-Library.Disjoint_Sets
03:26:05 LambdaMu: theory LambdaMu.DeBruijn
03:26:05 LambdaMu: theory LambdaMu.Types
03:26:06 Finished First_Welfare_Theorem/document (0:00:05 elapsed time)
03:26:06 Preparing First_Welfare_Theorem/outline ...
03:26:06 Hello_World: theory Hello_World.HelloWorld_Proof
03:26:06 LambdaMu: theory LambdaMu.Substitution
03:26:06 LambdaMu: theory LambdaMu.Peirce
03:26:06 Finished Nullstellensatz/outline (0:00:03 elapsed time)
03:26:06 LambdaMu: theory LambdaMu.Reduction
03:26:06 Card_Partitions: theory Card_Partitions.Injectivity_Solver
03:26:06 Card_Partitions: theory Card_Partitions.Set_Partition
03:26:06 LambdaMu: theory LambdaMu.ContextFacts
03:26:06 Finished VolpanoSmith/document (0:00:04 elapsed time)
03:26:06 Preparing VolpanoSmith/outline ...
03:26:06 Timing Nullstellensatz (4 threads, 8.620s elapsed time, 21.159s cpu time, 0.855s GC time, factor 2.45)
03:26:06 Finished Nullstellensatz (0:00:23 elapsed time, 0:00:35 cpu time, factor 1.52)
03:26:06 Running Random_Graph_Subgraph_Threshold ...
03:26:06 Card_Partitions: theory Card_Partitions.Card_Partitions
03:26:07 Hello_World: theory Hello_World.RunningCodeFromIsabelle
03:26:07 LambdaMu: theory LambdaMu.TypePreservation
03:26:07 LambdaMu: theory LambdaMu.Progress
03:26:07 Finished Selection_Heap_Sort/outline (0:00:02 elapsed time)
03:26:07 Timing Selection_Heap_Sort (4 threads, 7.358s elapsed time, 23.274s cpu time, 0.760s GC time, factor 3.16)
03:26:07 Finished Selection_Heap_Sort (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.37)
03:26:07 Running Verified-Prover ...
03:26:08 Finished Laplace_Transform/outline (0:00:03 elapsed time)
03:26:08 Timing Laplace_Transform (4 threads, 7.914s elapsed time, 30.030s cpu time, 0.505s GC time, factor 3.79)
03:26:08 Finished Laplace_Transform (0:00:11 elapsed time, 0:00:33 cpu time, factor 2.84)
03:26:08 Running Abstract-Hoare-Logics ...
03:26:09 Preparing Hello_World/document ...
03:26:09 Verified-Prover: theory Verified-Prover.Prover
03:26:10 Finished VolpanoSmith/outline (0:00:03 elapsed time)
03:26:10 Finished First_Welfare_Theorem/outline (0:00:04 elapsed time)
03:26:10 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Lang
03:26:10 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PLang
03:26:10 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsLang
03:26:10 Timing First_Welfare_Theorem (4 threads, 7.574s elapsed time, 25.916s cpu time, 0.636s GC time, factor 3.42)
03:26:10 Finished First_Welfare_Theorem (0:00:11 elapsed time, 0:00:29 cpu time, factor 2.56)
03:26:10 Timing VolpanoSmith (4 threads, 7.444s elapsed time, 17.876s cpu time, 0.603s GC time, factor 2.40)
03:26:10 Finished VolpanoSmith (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.01)
03:26:10 Running Minimal_SSA ...
03:26:10 Running Case_Labeling ...
03:26:11 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
03:26:11 Finished Hello_World/document (0:00:02 elapsed time)
03:26:11 Preparing Hello_World/outline ...
03:26:11 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Hoare
03:26:11 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Termi
03:26:11 Preparing LambdaMu/document ...
03:26:11 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.HoareTotal
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoare
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PTermi
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoare
03:26:12 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsTermi
03:26:12 Preparing Impossible_Geometry/document ...
03:26:12 Case_Labeling: theory HOL-Eisbach.Eisbach
03:26:12 Case_Labeling: theory Case_Labeling.Case_Labeling
03:26:12 Case_Labeling: theory HOL-Hoare.Arith2
03:26:12 Case_Labeling: theory HOL-Hoare.Hoare_Syntax
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoareTotal
03:26:12 Case_Labeling: theory HOL-Hoare.Hoare_Tac
03:26:12 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoareTotal
03:26:12 Preparing Card_Partitions/document ...
03:26:13 Finished Hello_World/outline (0:00:02 elapsed time)
03:26:13 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
03:26:13 Timing Hello_World (4 threads, 7.624s elapsed time, 2.431s cpu time, 0.000s GC time, factor 0.32)
03:26:13 Finished Hello_World (0:00:10 elapsed time, 0:00:04 cpu time, factor 0.43)
03:26:13 Running FileRefinement ...
03:26:14 Preparing Szemeredi_Regularity/document ...
03:26:14 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
03:26:14 Case_Labeling: theory Case_Labeling.Conditionals
03:26:14 Case_Labeling: theory Case_Labeling.Monadic_Language
03:26:14 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
03:26:15 Case_Labeling: theory HOL-Hoare.Hoare_Logic
03:26:15 FileRefinement: theory FileRefinement.ResizableArrays
03:26:15 Finished LambdaMu/document (0:00:04 elapsed time)
03:26:15 Preparing LambdaMu/outline ...
03:26:15 FileRefinement: theory FileRefinement.CArrays
03:26:15 FileRefinement: theory FileRefinement.FileRefinement
03:26:16 Minimal_SSA: theory Minimal_SSA.Irreducible
03:26:16 Case_Labeling: theory Case_Labeling.Labeled_Hoare
03:26:17 Finished Impossible_Geometry/document (0:00:04 elapsed time)
03:26:17 Preparing Impossible_Geometry/outline ...
03:26:17 Finished Card_Partitions/document (0:00:04 elapsed time)
03:26:17 Preparing Card_Partitions/outline ...
03:26:17 Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
03:26:17 Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
03:26:18 Preparing Verified-Prover/document ...
03:26:18 Finished Szemeredi_Regularity/document (0:00:04 elapsed time)
03:26:18 Preparing Szemeredi_Regularity/outline ...
03:26:18 Preparing Abstract-Hoare-Logics/document ...
03:26:19 Finished LambdaMu/outline (0:00:03 elapsed time)
03:26:19 Timing LambdaMu (4 threads, 8.059s elapsed time, 17.640s cpu time, 0.431s GC time, factor 2.19)
03:26:19 Finished LambdaMu (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.90)
03:26:19 Running GoedelGod ...
03:26:19 Preparing Random_Graph_Subgraph_Threshold/document ...
03:26:20 Finished Card_Partitions/outline (0:00:03 elapsed time)
03:26:20 Timing Card_Partitions (4 threads, 7.229s elapsed time, 27.099s cpu time, 0.463s GC time, factor 3.75)
03:26:20 Finished Card_Partitions (0:00:09 elapsed time, 0:00:29 cpu time, factor 3.01)
03:26:20 Running FinFun ...
03:26:20 Finished Impossible_Geometry/outline (0:00:03 elapsed time)
03:26:20 Timing Impossible_Geometry (4 threads, 8.176s elapsed time, 19.633s cpu time, 0.555s GC time, factor 2.40)
03:26:20 Finished Impossible_Geometry (0:00:10 elapsed time, 0:00:21 cpu time, factor 2.05)
03:26:20 Running PAL ...
03:26:21 Preparing Case_Labeling/document ...
03:26:21 GoedelGod: theory GoedelGod.GoedelGod
03:26:22 FinFun: theory HOL-Library.Phantom_Type
03:26:22 Finished Szemeredi_Regularity/outline (0:00:03 elapsed time)
03:26:22 Finished Verified-Prover/document (0:00:04 elapsed time)
03:26:22 Preparing Verified-Prover/outline ...
03:26:22 Timing Szemeredi_Regularity (4 threads, 8.446s elapsed time, 24.080s cpu time, 0.522s GC time, factor 2.85)
03:26:22 Finished Szemeredi_Regularity (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.22)
03:26:22 Running SumSquares ...
03:26:22 PAL: theory PAL.PAL
03:26:23 FinFun: theory HOL-Library.Cardinality
03:26:23 Preparing Minimal_SSA/document ...
03:26:23 Preparing FileRefinement/document ...
03:26:24 FinFun: theory FinFun.FinFun
03:26:24 Finished Abstract-Hoare-Logics/document (0:00:05 elapsed time)
03:26:24 Finished Case_Labeling/document (0:00:03 elapsed time)
03:26:24 Preparing Abstract-Hoare-Logics/outline ...
03:26:24 Preparing Case_Labeling/outline ...
03:26:25 Finished Random_Graph_Subgraph_Threshold/document (0:00:05 elapsed time)
03:26:25 Preparing Random_Graph_Subgraph_Threshold/outline ...
03:26:25 Finished Verified-Prover/outline (0:00:03 elapsed time)
03:26:26 Timing Verified-Prover (4 threads, 7.121s elapsed time, 17.916s cpu time, 0.418s GC time, factor 2.52)
03:26:26 Finished Verified-Prover (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.07)
03:26:26 Running Pop_Refinement ...
03:26:26 Finished FileRefinement/document (0:00:03 elapsed time)
03:26:26 Preparing FileRefinement/outline ...
03:26:27 FinFun: theory FinFun.FinFunPred
03:26:27 SumSquares: theory SumSquares.FourSquares
03:26:27 SumSquares: theory SumSquares.TwoSquares
03:26:27 Finished Case_Labeling/outline (0:00:03 elapsed time)
03:26:27 Pop_Refinement: theory Pop_Refinement.Definition
03:26:27 Pop_Refinement: theory Pop_Refinement.First_Example
03:26:27 Pop_Refinement: theory Pop_Refinement.Future_Work
03:26:27 Pop_Refinement: theory Pop_Refinement.General_Remarks
03:26:27 Pop_Refinement: theory Pop_Refinement.Related_Work
03:26:27 Pop_Refinement: theory Pop_Refinement.Second_Example
03:26:27 Finished Minimal_SSA/document (0:00:04 elapsed time)
03:26:27 Preparing Minimal_SSA/outline ...
03:26:28 Timing Case_Labeling (4 threads, 7.557s elapsed time, 22.721s cpu time, 0.593s GC time, factor 3.01)
03:26:28 Finished Case_Labeling (0:00:09 elapsed time, 0:00:24 cpu time, factor 2.51)
03:26:28 Running Menger ...
03:26:28 Finished Abstract-Hoare-Logics/outline (0:00:04 elapsed time)
03:26:28 Finished Random_Graph_Subgraph_Threshold/outline (0:00:03 elapsed time)
03:26:29 Timing Abstract-Hoare-Logics (4 threads, 7.417s elapsed time, 26.919s cpu time, 1.207s GC time, factor 3.63)
03:26:29 Finished Abstract-Hoare-Logics (0:00:09 elapsed time, 0:00:28 cpu time, factor 2.98)
03:26:29 Timing Random_Graph_Subgraph_Threshold (4 threads, 7.888s elapsed time, 23.656s cpu time, 0.533s GC time, factor 3.00)
03:26:29 Finished Random_Graph_Subgraph_Threshold (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.21)
03:26:29 Running InformationFlowSlicing ...
03:26:29 Running Noninterference_Inductive_Unwinding ...
03:26:29 Preparing GoedelGod/document ...
03:26:29 Preparing PAL/document ...
03:26:29 Preparing FinFun/document ...
03:26:29 Menger: theory Menger.Helpers
03:26:29 Menger: theory Menger.Graph
03:26:29 Finished FileRefinement/outline (0:00:03 elapsed time)
03:26:30 Timing FileRefinement (4 threads, 7.165s elapsed time, 17.686s cpu time, 0.147s GC time, factor 2.47)
03:26:30 Finished FileRefinement (0:00:09 elapsed time, 0:00:19 cpu time, factor 2.05)
03:26:30 Running Tree_Decomposition ...
03:26:30 Noninterference_Inductive_Unwinding: theory List_Interleaving.ListInterleaving
03:26:30 Noninterference_Inductive_Unwinding: theory Noninterference_CSP.CSPNoninterference
03:26:31 Menger: theory Menger.Separations
03:26:31 Finished GoedelGod/document (0:00:02 elapsed time)
03:26:31 Preparing GoedelGod/outline ...
03:26:31 Finished Minimal_SSA/outline (0:00:03 elapsed time)
03:26:31 Menger: theory Menger.DisjointPaths
03:26:31 Timing Minimal_SSA (4 threads, 6.827s elapsed time, 21.055s cpu time, 0.434s GC time, factor 3.08)
03:26:31 Finished Minimal_SSA (0:00:12 elapsed time, 0:00:26 cpu time, factor 2.12)
03:26:31 Running MuchAdoAboutTwo ...
03:26:31 Menger: theory Menger.MengerInduction
03:26:31 Tree_Decomposition: theory Tree_Decomposition.Graph
03:26:32 Tree_Decomposition: theory Tree_Decomposition.Tree
03:26:32 Menger: theory Menger.Y_eq_new_last
03:26:33 Finished FinFun/document (0:00:03 elapsed time)
03:26:33 Preparing FinFun/outline ...
03:26:33 Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
03:26:33 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
03:26:33 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
03:26:33 Finished PAL/document (0:00:03 elapsed time)
03:26:33 Preparing PAL/outline ...
03:26:33 Menger: theory Menger.Y_neq_new_last
03:26:33 Finished GoedelGod/outline (0:00:02 elapsed time)
03:26:33 Timing GoedelGod (4 threads, 6.839s elapsed time, 7.630s cpu time, 0.086s GC time, factor 1.12)
03:26:33 Finished GoedelGod (0:00:09 elapsed time, 0:00:09 cpu time, factor 1.05)
03:26:33 Running Concurrent_Ref_Alg ...
03:26:33 Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
03:26:33 Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
03:26:33 Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
03:26:33 Menger: theory Menger.Menger
03:26:34 InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
03:26:34 Preparing SumSquares/document ...
03:26:34 Preparing Pop_Refinement/document ...
03:26:34 MuchAdoAboutTwo: theory HOL-Combinatorics.Transposition
03:26:35 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
03:26:35 MuchAdoAboutTwo: theory HOL-Combinatorics.Permutations
03:26:35 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Refinement_Lattice
03:26:35 Noninterference_Inductive_Unwinding: theory Noninterference_Inductive_Unwinding.InductiveUnwinding
03:26:35 Finished FinFun/outline (0:00:02 elapsed time)
03:26:36 Timing FinFun (4 threads, 6.515s elapsed time, 13.630s cpu time, 0.322s GC time, factor 2.09)
03:26:36 Finished FinFun (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.76)
03:26:36 Running Ramsey-Infinite ...
03:26:36 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Galois_Connections
03:26:36 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Parallel
03:26:36 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunction
03:26:36 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Infimum_Nat
03:26:36 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
03:26:36 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Sequential
03:26:37 Finished PAL/outline (0:00:03 elapsed time)
03:26:37 Timing PAL (4 threads, 6.066s elapsed time, 20.513s cpu time, 0.449s GC time, factor 3.38)
03:26:37 Finished PAL (0:00:08 elapsed time, 0:00:22 cpu time, factor 2.66)
03:26:37 Running Banach_Steinhaus ...
03:26:37 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.CRA
03:26:37 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Sequential
03:26:37 Preparing Menger/document ...
03:26:37 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Iteration
03:26:38 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Iteration
03:26:38 Ramsey-Infinite: theory HOL-Library.Infinite_Set
03:26:38 MuchAdoAboutTwo: theory MuchAdoAboutTwo.MuchAdoAboutTwo
03:26:38 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Rely_Quotient
03:26:38 Preparing Tree_Decomposition/document ...
03:26:39 Ramsey-Infinite: theory Ramsey-Infinite.Ramsey
03:26:39 Finished SumSquares/document (0:00:04 elapsed time)
03:26:39 Preparing SumSquares/outline ...
03:26:39 Finished Pop_Refinement/document (0:00:04 elapsed time)
03:26:39 Preparing Pop_Refinement/outline ...
03:26:40 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
03:26:41 Preparing Noninterference_Inductive_Unwinding/document ...
03:26:42 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
03:26:42 Preparing InformationFlowSlicing/document ...
03:26:42 Finished SumSquares/outline (0:00:03 elapsed time)
03:26:42 Preparing MuchAdoAboutTwo/document ...
03:26:42 Timing SumSquares (4 threads, 6.322s elapsed time, 20.012s cpu time, 0.358s GC time, factor 3.17)
03:26:42 Finished SumSquares (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.12)
03:26:42 Running Binomial-Queues ...
03:26:42 Preparing Concurrent_Ref_Alg/document ...
03:26:43 Finished Pop_Refinement/outline (0:00:03 elapsed time)
03:26:43 Timing Pop_Refinement (4 threads, 6.132s elapsed time, 18.493s cpu time, 0.744s GC time, factor 3.02)
03:26:43 Finished Pop_Refinement (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.39)
03:26:43 Running Partial_Function_MR ...
03:26:44 Finished Menger/document (0:00:06 elapsed time)
03:26:44 Preparing Menger/outline ...
03:26:44 Finished Tree_Decomposition/document (0:00:05 elapsed time)
03:26:44 Preparing Tree_Decomposition/outline ...
03:26:44 Binomial-Queues: theory Binomial-Queues.PQ
03:26:44 Finished Noninterference_Inductive_Unwinding/document (0:00:03 elapsed time)
03:26:44 Preparing Noninterference_Inductive_Unwinding/outline ...
03:26:44 Binomial-Queues: theory Binomial-Queues.Binomial_Queue
03:26:44 Preparing Ramsey-Infinite/document ...
03:26:45 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
03:26:45 Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
03:26:45 Partial_Function_MR: theory HOL-Library.Monad_Syntax
03:26:45 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
03:26:46 Finished MuchAdoAboutTwo/document (0:00:04 elapsed time)
03:26:46 Preparing MuchAdoAboutTwo/outline ...
03:26:46 Finished Ramsey-Infinite/document (0:00:01 elapsed time)
03:26:46 Preparing Ramsey-Infinite/outline ...
03:26:47 Binomial-Queues: theory Binomial-Queues.PQ_Implementation
03:26:47 Finished Concurrent_Ref_Alg/document (0:00:04 elapsed time)
03:26:47 Preparing Concurrent_Ref_Alg/outline ...
03:26:47 Preparing Banach_Steinhaus/document ...
03:26:47 Finished Noninterference_Inductive_Unwinding/outline (0:00:03 elapsed time)
03:26:48 Finished InformationFlowSlicing/document (0:00:05 elapsed time)
03:26:48 Preparing InformationFlowSlicing/outline ...
03:26:48 Timing Noninterference_Inductive_Unwinding (4 threads, 6.374s elapsed time, 22.320s cpu time, 0.740s GC time, factor 3.50)
03:26:48 Finished Noninterference_Inductive_Unwinding (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.13)
03:26:48 Running Latin_Square ...
03:26:48 Finished Ramsey-Infinite/outline (0:00:01 elapsed time)
03:26:48 Timing Ramsey-Infinite (4 threads, 6.114s elapsed time, 11.546s cpu time, 0.140s GC time, factor 1.89)
03:26:48 Finished Ramsey-Infinite (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.58)
03:26:48 Running FOL_Axiomatic ...
03:26:48 Finished Tree_Decomposition/outline (0:00:04 elapsed time)
03:26:49 Finished Menger/outline (0:00:05 elapsed time)
03:26:49 Timing Tree_Decomposition (4 threads, 6.022s elapsed time, 18.352s cpu time, 0.435s GC time, factor 3.05)
03:26:49 Finished Tree_Decomposition (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.40)
03:26:49 Timing Menger (4 threads, 6.750s elapsed time, 23.830s cpu time, 0.651s GC time, factor 3.53)
03:26:49 Finished Menger (0:00:09 elapsed time, 0:00:25 cpu time, factor 2.81)
03:26:49 Running FOL_Seq_Calc1 ...
03:26:49 Running Comparison_Sort_Lower_Bound ...
03:26:49 Finished MuchAdoAboutTwo/outline (0:00:03 elapsed time)
03:26:49 Latin_Square: theory Marriage.Marriage
03:26:50 Latin_Square: theory Latin_Square.Latin_Square
03:26:50 Timing MuchAdoAboutTwo (4 threads, 6.367s elapsed time, 20.746s cpu time, 0.685s GC time, factor 3.26)
03:26:50 Finished MuchAdoAboutTwo (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.36)
03:26:50 Running Van_der_Waerden ...
03:26:50 FOL_Axiomatic: theory HOL-Library.Nat_Bijection
03:26:50 FOL_Axiomatic: theory HOL-Library.Old_Datatype
03:26:51 Finished Concurrent_Ref_Alg/outline (0:00:03 elapsed time)
03:26:51 Timing Concurrent_Ref_Alg (4 threads, 6.604s elapsed time, 19.646s cpu time, 0.412s GC time, factor 2.97)
03:26:51 Finished Concurrent_Ref_Alg (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.37)
03:26:51 Running ShortestPath ...
03:26:51 FOL_Axiomatic: theory HOL-Library.Countable
03:26:51 Preparing Partial_Function_MR/document ...
03:26:51 Preparing Binomial-Queues/document ...
03:26:51 Finished InformationFlowSlicing/outline (0:00:03 elapsed time)
03:26:52 Van_der_Waerden: theory Van_der_Waerden.Digits
03:26:52 Van_der_Waerden: theory HOL-Library.FuncSet
03:26:52 Timing InformationFlowSlicing (4 threads, 7.248s elapsed time, 22.989s cpu time, 0.816s GC time, factor 3.17)
03:26:52 Finished InformationFlowSlicing (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.16)
03:26:52 Running Tail_Recursive_Functions ...
03:26:52 Finished Banach_Steinhaus/document (0:00:04 elapsed time)
03:26:52 Preparing Banach_Steinhaus/outline ...
03:26:52 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
03:26:52 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
03:26:52 Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
03:26:53 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
03:26:53 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
03:26:54 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
03:26:54 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
03:26:54 Finished Binomial-Queues/document (0:00:02 elapsed time)
03:26:54 Preparing Binomial-Queues/outline ...
03:26:54 ShortestPath: theory ShortestPath.ShortestPath
03:26:55 Finished Partial_Function_MR/document (0:00:03 elapsed time)
03:26:55 Preparing Partial_Function_MR/outline ...
03:26:55 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
03:26:55 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
03:26:55 Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
03:26:55 Finished Banach_Steinhaus/outline (0:00:03 elapsed time)
03:26:56 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
03:26:56 Preparing Latin_Square/document ...
03:26:56 Timing Banach_Steinhaus (4 threads, 5.648s elapsed time, 18.418s cpu time, 0.241s GC time, factor 3.26)
03:26:56 Finished Banach_Steinhaus (0:00:10 elapsed time, 0:00:22 cpu time, factor 2.22)
03:26:56 Running Relational-Incorrectness-Logic ...
03:26:56 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
03:26:57 Finished Binomial-Queues/outline (0:00:02 elapsed time)
03:26:57 Timing Binomial-Queues (4 threads, 6.397s elapsed time, 15.192s cpu time, 0.311s GC time, factor 2.37)
03:26:57 Finished Binomial-Queues (0:00:08 elapsed time, 0:00:17 cpu time, factor 1.97)
03:26:57 Running Dynamic_Tables ...
03:26:57 ShortestPath: theory ShortestPath.ShortestPathNeg
03:26:57 Preparing FOL_Axiomatic/document ...
03:26:58 Preparing Van_der_Waerden/document ...
03:26:59 Finished Partial_Function_MR/outline (0:00:03 elapsed time)
03:26:59 Timing Partial_Function_MR (4 threads, 5.555s elapsed time, 8.886s cpu time, 0.325s GC time, factor 1.60)
03:26:59 Finished Partial_Function_MR (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.38)
03:26:59 Running Buffons_Needle ...
03:26:59 Preparing FOL_Seq_Calc1/document ...
03:26:59 Finished Latin_Square/document (0:00:03 elapsed time)
03:26:59 Preparing Latin_Square/outline ...
03:26:59 Relational-Incorrectness-Logic: theory Relational-Incorrectness-Logic.RelationalIncorrectness
03:27:01 Dynamic_Tables: theory Dynamic_Tables.Tables_real
03:27:01 Preparing ShortestPath/document ...
03:27:01 Preparing Tail_Recursive_Functions/document ...
03:27:01 Preparing Comparison_Sort_Lower_Bound/document ...
03:27:01 Finished Van_der_Waerden/document (0:00:03 elapsed time)
03:27:01 Preparing Van_der_Waerden/outline ...
03:27:02 Dynamic_Tables: theory Dynamic_Tables.Tables_nat
03:27:02 Finished Latin_Square/outline (0:00:02 elapsed time)
03:27:02 Finished FOL_Axiomatic/document (0:00:04 elapsed time)
03:27:02 Preparing FOL_Axiomatic/outline ...
03:27:02 Timing Latin_Square (4 threads, 5.132s elapsed time, 19.053s cpu time, 0.301s GC time, factor 3.71)
03:27:02 Finished Latin_Square (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.78)
03:27:02 Running Matroids ...
03:27:03 Finished FOL_Seq_Calc1/document (0:00:03 elapsed time)
03:27:03 Preparing FOL_Seq_Calc1/outline ...
03:27:03 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
03:27:04 Finished ShortestPath/document (0:00:03 elapsed time)
03:27:04 Preparing ShortestPath/outline ...
03:27:04 Matroids: theory Matroids.Indep_System
03:27:04 Finished Van_der_Waerden/outline (0:00:03 elapsed time)
03:27:05 Finished Comparison_Sort_Lower_Bound/document (0:00:03 elapsed time)
03:27:05 Preparing Comparison_Sort_Lower_Bound/outline ...
03:27:05 Finished Tail_Recursive_Functions/document (0:00:04 elapsed time)
03:27:05 Preparing Tail_Recursive_Functions/outline ...
03:27:05 Timing Van_der_Waerden (4 threads, 5.341s elapsed time, 20.553s cpu time, 0.351s GC time, factor 3.85)
03:27:05 Finished Van_der_Waerden (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.95)
03:27:05 Running Stellar_Quorums ...
03:27:05 Matroids: theory Matroids.Matroid
03:27:06 Finished FOL_Seq_Calc1/outline (0:00:02 elapsed time)
03:27:06 Preparing Relational-Incorrectness-Logic/document ...
03:27:06 Timing FOL_Seq_Calc1 (4 threads, 5.897s elapsed time, 18.391s cpu time, 0.320s GC time, factor 3.12)
03:27:06 Finished FOL_Seq_Calc1 (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.22)
03:27:06 Running HotelKeyCards ...
03:27:06 Preparing Dynamic_Tables/document ...
03:27:06 Finished FOL_Axiomatic/outline (0:00:04 elapsed time)
03:27:06 Timing FOL_Axiomatic (4 threads, 6.188s elapsed time, 14.639s cpu time, 0.293s GC time, factor 2.37)
03:27:06 Finished FOL_Axiomatic (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.94)
03:27:06 Running Falling_Factorial_Sum ...
03:27:07 Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
03:27:07 Finished ShortestPath/outline (0:00:02 elapsed time)
03:27:07 Timing ShortestPath (4 threads, 5.549s elapsed time, 8.371s cpu time, 0.278s GC time, factor 1.51)
03:27:07 Finished ShortestPath (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.26)
03:27:07 Running Topology ...
03:27:08 Finished Comparison_Sort_Lower_Bound/outline (0:00:03 elapsed time)
03:27:08 HotelKeyCards: theory HOL-Library.LaTeXsugar
03:27:08 HotelKeyCards: theory HotelKeyCards.Notation
03:27:08 HotelKeyCards: theory HotelKeyCards.Basis
03:27:08 Timing Comparison_Sort_Lower_Bound (4 threads, 5.980s elapsed time, 19.361s cpu time, 0.558s GC time, factor 3.24)
03:27:08 Finished Comparison_Sort_Lower_Bound (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.10)
03:27:08 Running Combinatorics_Words_Lyndon ...
03:27:08 HotelKeyCards: theory HotelKeyCards.State
03:27:08 HotelKeyCards: theory HotelKeyCards.NewCard
03:27:08 HotelKeyCards: theory HotelKeyCards.Trace
03:27:08 Finished Tail_Recursive_Functions/outline (0:00:03 elapsed time)
03:27:08 Timing Tail_Recursive_Functions (4 threads, 4.690s elapsed time, 11.306s cpu time, 0.332s GC time, factor 2.41)
03:27:08 Finished Tail_Recursive_Functions (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.72)
03:27:08 Running Public_Announcement_Logic ...
03:27:09 Preparing Buffons_Needle/document ...
03:27:09 HotelKeyCards: theory HotelKeyCards.Equivalence
03:27:09 Finished Relational-Incorrectness-Logic/document (0:00:03 elapsed time)
03:27:09 Preparing Relational-Incorrectness-Logic/outline ...
03:27:10 Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
03:27:10 Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
03:27:10 Preparing Matroids/document ...
03:27:10 Finished Dynamic_Tables/document (0:00:03 elapsed time)
03:27:10 Preparing Dynamic_Tables/outline ...
03:27:10 Falling_Factorial_Sum: theory Discrete_Summation.Factorials
03:27:11 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
03:27:11 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
03:27:11 Topology: theory Topology.Topology
03:27:11 Topology: theory Lazy-Lists-II.LList2
03:27:11 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
03:27:11 Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
03:27:11 Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
03:27:12 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
03:27:12 Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
03:27:12 Preparing Stellar_Quorums/document ...
03:27:13 Finished Relational-Incorrectness-Logic/outline (0:00:03 elapsed time)
03:27:13 Timing Relational-Incorrectness-Logic (4 threads, 5.176s elapsed time, 14.152s cpu time, 0.281s GC time, factor 2.73)
03:27:13 Finished Relational-Incorrectness-Logic (0:00:09 elapsed time, 0:00:18 cpu time, factor 1.90)
03:27:13 Running Secondary_Sylow ...
03:27:13 Finished Dynamic_Tables/outline (0:00:03 elapsed time)
03:27:13 Preparing HotelKeyCards/document ...
03:27:13 Timing Dynamic_Tables (4 threads, 4.736s elapsed time, 16.827s cpu time, 0.515s GC time, factor 3.55)
03:27:13 Finished Dynamic_Tables (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.31)
03:27:13 Running TortoiseHare ...
03:27:14 Topology: theory Topology.LList_Topology
03:27:15 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
03:27:15 Finished Matroids/document (0:00:04 elapsed time)
03:27:15 Preparing Matroids/outline ...
03:27:16 Preparing Falling_Factorial_Sum/document ...
03:27:16 Finished Buffons_Needle/document (0:00:06 elapsed time)
03:27:16 Preparing Buffons_Needle/outline ...
03:27:16 Finished Stellar_Quorums/document (0:00:03 elapsed time)
03:27:16 Preparing Stellar_Quorums/outline ...
03:27:16 Preparing Combinatorics_Words_Lyndon/document ...
03:27:17 Finished HotelKeyCards/document (0:00:03 elapsed time)
03:27:17 Preparing HotelKeyCards/outline ...
03:27:17 TortoiseHare: theory TortoiseHare.Basis
03:27:17 Preparing Public_Announcement_Logic/document ...
03:27:17 Preparing Topology/document ...
03:27:17 TortoiseHare: theory TortoiseHare.Brent
03:27:17 TortoiseHare: theory TortoiseHare.TortoiseHare
03:27:18 Finished Matroids/outline (0:00:03 elapsed time)
03:27:18 Timing Matroids (4 threads, 4.842s elapsed time, 14.865s cpu time, 0.184s GC time, factor 3.07)
03:27:18 Finished Matroids (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.34)
03:27:18 Running Source_Coding_Theorem ...
03:27:19 Finished Falling_Factorial_Sum/document (0:00:03 elapsed time)
03:27:19 Preparing Falling_Factorial_Sum/outline ...
03:27:19 Finished Stellar_Quorums/outline (0:00:02 elapsed time)
03:27:19 Timing Stellar_Quorums (4 threads, 5.048s elapsed time, 17.686s cpu time, 0.349s GC time, factor 3.50)
03:27:19 Finished Stellar_Quorums (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.68)
03:27:19 Running Arith_Prog_Rel_Primes ...
03:27:20 Finished Public_Announcement_Logic/document (0:00:03 elapsed time)
03:27:20 Preparing Public_Announcement_Logic/outline ...
03:27:20 Finished HotelKeyCards/outline (0:00:03 elapsed time)
03:27:20 Secondary_Sylow: theory Secondary_Sylow.GroupAction
03:27:20 Timing HotelKeyCards (4 threads, 4.721s elapsed time, 14.433s cpu time, 0.370s GC time, factor 3.06)
03:27:20 Finished HotelKeyCards (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.30)
03:27:20 Running Lazy_Case ...
03:27:21 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
03:27:21 Secondary_Sylow: theory Secondary_Sylow.SndSylow
03:27:21 Preparing TortoiseHare/document ...
03:27:22 Finished Falling_Factorial_Sum/outline (0:00:02 elapsed time)
03:27:22 Finished Topology/document (0:00:04 elapsed time)
03:27:22 Preparing Topology/outline ...
03:27:22 Finished Buffons_Needle/outline (0:00:06 elapsed time)
03:27:22 Timing Buffons_Needle (4 threads, 5.060s elapsed time, 14.923s cpu time, 0.097s GC time, factor 2.95)
03:27:22 Finished Buffons_Needle (0:00:09 elapsed time, 0:00:19 cpu time, factor 1.97)
03:27:22 Timing Falling_Factorial_Sum (4 threads, 4.850s elapsed time, 15.237s cpu time, 0.290s GC time, factor 3.14)
03:27:22 Finished Falling_Factorial_Sum (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.15)
03:27:22 Running Imperative_Insertion_Sort ...
03:27:22 Running Certification_Monads ...
03:27:22 Lazy_Case: theory Lazy_Case.Lazy_Case
03:27:22 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
03:27:23 Lazy_Case: theory Lazy_Case.Test_Lazy_Case
03:27:23 Finished Combinatorics_Words_Lyndon/document (0:00:06 elapsed time)
03:27:23 Preparing Combinatorics_Words_Lyndon/outline ...
03:27:23 Finished Public_Announcement_Logic/outline (0:00:03 elapsed time)
03:27:24 Timing Public_Announcement_Logic (4 threads, 4.283s elapsed time, 8.918s cpu time, 0.348s GC time, factor 2.08)
03:27:24 Finished Public_Announcement_Logic (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.53)
03:27:24 Running ArrowImpossibilityGS ...
03:27:24 Certification_Monads: theory Certification_Monads.Misc
03:27:24 Certification_Monads: theory Deriving.Derive_Manager
03:27:24 Certification_Monads: theory Deriving.Generator_Aux
03:27:24 Certification_Monads: theory HOL-Library.Adhoc_Overloading
03:27:24 Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
03:27:24 Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
03:27:24 Certification_Monads: theory Certification_Monads.Error_Syntax
03:27:24 Certification_Monads: theory HOL-Library.Monad_Syntax
03:27:24 Certification_Monads: theory Certification_Monads.Error_Monad
03:27:24 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
03:27:24 Certification_Monads: theory Show.Show
03:27:25 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
03:27:25 Certification_Monads: theory Certification_Monads.Strict_Sum
03:27:25 Finished TortoiseHare/document (0:00:03 elapsed time)
03:27:25 Preparing TortoiseHare/outline ...
03:27:25 ArrowImpossibilityGS: theory HOL-Library.FuncSet
03:27:25 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Utility
03:27:25 Preparing Secondary_Sylow/document ...
03:27:26 Finished Topology/outline (0:00:04 elapsed time)
03:27:26 Timing Topology (4 threads, 4.887s elapsed time, 17.903s cpu time, 0.970s GC time, factor 3.66)
03:27:26 Finished Topology (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.29)
03:27:26 Running Chord_Segments ...
03:27:26 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Order
03:27:26 Certification_Monads: theory Certification_Monads.Check_Monad
03:27:26 Certification_Monads: theory Certification_Monads.Parser_Monad
03:27:27 ArrowImpossibilityGS: theory ArrowImpossibilityGS.GS
03:27:27 Preparing Lazy_Case/document ...
03:27:28 Preparing Source_Coding_Theorem/document ...
03:27:28 Finished Combinatorics_Words_Lyndon/outline (0:00:05 elapsed time)
03:27:28 Finished Lazy_Case/document (0:00:01 elapsed time)
03:27:28 Preparing Lazy_Case/outline ...
03:27:28 Finished Secondary_Sylow/document (0:00:03 elapsed time)
03:27:28 Preparing Secondary_Sylow/outline ...
03:27:29 Finished TortoiseHare/outline (0:00:03 elapsed time)
03:27:29 Timing Combinatorics_Words_Lyndon (4 threads, 4.226s elapsed time, 15.853s cpu time, 0.364s GC time, factor 3.75)
03:27:29 Finished Combinatorics_Words_Lyndon (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.38)
03:27:29 Timing TortoiseHare (4 threads, 3.641s elapsed time, 10.357s cpu time, 0.215s GC time, factor 2.84)
03:27:29 Finished TortoiseHare (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.84)
03:27:29 Running Triangle ...
03:27:29 Running Category ...
03:27:29 Preparing Arith_Prog_Rel_Primes/document ...
03:27:29 Preparing Certification_Monads/document ...
03:27:29 Preparing Imperative_Insertion_Sort/document ...
03:27:29 Chord_Segments: theory Triangle.Angles
03:27:30 Chord_Segments: theory Triangle.Triangle
03:27:30 Preparing ArrowImpossibilityGS/document ...
03:27:30 Chord_Segments: theory Chord_Segments.Chord_Segments
03:27:30 Finished Lazy_Case/outline (0:00:01 elapsed time)
03:27:30 Category: theory HOL-Library.FuncSet
03:27:31 Finished Secondary_Sylow/outline (0:00:02 elapsed time)
03:27:31 Timing Lazy_Case (4 threads, 3.826s elapsed time, 6.190s cpu time, 0.355s GC time, factor 1.62)
03:27:31 Finished Lazy_Case (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.34)
03:27:31 Timing Secondary_Sylow (4 threads, 4.246s elapsed time, 13.847s cpu time, 0.526s GC time, factor 3.26)
03:27:31 Finished Secondary_Sylow (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.76)
03:27:31 Running LatticeProperties ...
03:27:31 Running GaleStewart_Games ...
03:27:31 Category: theory Category.Cat
03:27:31 Finished Source_Coding_Theorem/document (0:00:03 elapsed time)
03:27:31 Preparing Source_Coding_Theorem/outline ...
03:27:32 Finished Certification_Monads/document (0:00:02 elapsed time)
03:27:32 Preparing Certification_Monads/outline ...
03:27:32 Finished Imperative_Insertion_Sort/document (0:00:02 elapsed time)
03:27:32 Preparing Imperative_Insertion_Sort/outline ...
03:27:32 Category: theory Category.Functors
03:27:32 Triangle: theory Triangle.Angles
03:27:32 Category: theory Category.SetCat
03:27:32 Triangle: theory Triangle.Triangle
03:27:32 Category: theory Category.NatTrans
03:27:32 Category: theory Category.HomFunctors
03:27:32 LatticeProperties: theory LatticeProperties.Lattice_Prop
03:27:32 LatticeProperties: theory LatticeProperties.Conj_Disj
03:27:32 LatticeProperties: theory LatticeProperties.WellFoundedTransitive
03:27:33 Finished Arith_Prog_Rel_Primes/document (0:00:03 elapsed time)
03:27:33 Preparing Arith_Prog_Rel_Primes/outline ...
03:27:33 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice
03:27:33 Category: theory Category.Yoneda
03:27:33 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop
03:27:33 GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
03:27:33 GaleStewart_Games: theory GaleStewart_Games.MoreENat
03:27:33 GaleStewart_Games: theory GaleStewart_Games.MorePrefix
03:27:34 Finished Imperative_Insertion_Sort/outline (0:00:01 elapsed time)
03:27:34 Timing Imperative_Insertion_Sort (4 threads, 4.190s elapsed time, 14.022s cpu time, 0.167s GC time, factor 3.35)
03:27:34 Finished Imperative_Insertion_Sort (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.29)
03:27:34 Running Stewart_Apollonius ...
03:27:34 Finished ArrowImpossibilityGS/document (0:00:03 elapsed time)
03:27:34 Preparing ArrowImpossibilityGS/outline ...
03:27:34 Finished Certification_Monads/outline (0:00:02 elapsed time)
03:27:34 Finished Source_Coding_Theorem/outline (0:00:02 elapsed time)
03:27:34 Timing Source_Coding_Theorem (4 threads, 4.414s elapsed time, 11.307s cpu time, 0.145s GC time, factor 2.56)
03:27:34 Finished Source_Coding_Theorem (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.73)
03:27:34 GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
03:27:34 Timing Certification_Monads (4 threads, 4.464s elapsed time, 13.458s cpu time, 0.328s GC time, factor 3.01)
03:27:34 Finished Certification_Monads (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.26)
03:27:34 Running Compiling-Exceptions-Correctly ...
03:27:34 Running Goodstein_Lambda ...
03:27:34 Preparing Chord_Segments/document ...
03:27:34 GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
03:27:35 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
03:27:35 Preparing Category/document ...
03:27:35 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group
03:27:35 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
03:27:35 Finished Arith_Prog_Rel_Primes/outline (0:00:02 elapsed time)
03:27:36 Timing Arith_Prog_Rel_Primes (4 threads, 3.831s elapsed time, 13.255s cpu time, 0.244s GC time, factor 3.46)
03:27:36 Finished Arith_Prog_Rel_Primes (0:00:09 elapsed time, 0:00:18 cpu time, factor 1.94)
03:27:36 Running VeriComp ...
03:27:36 Compiling-Exceptions-Correctly: theory Compiling-Exceptions-Correctly.Exceptions
03:27:36 Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
03:27:37 Preparing Triangle/document ...
03:27:37 Finished ArrowImpossibilityGS/outline (0:00:03 elapsed time)
03:27:37 Preparing LatticeProperties/document ...
03:27:37 Stewart_Apollonius: theory Triangle.Angles
03:27:37 Timing ArrowImpossibilityGS (4 threads, 3.907s elapsed time, 15.120s cpu time, 0.513s GC time, factor 3.87)
03:27:37 Finished ArrowImpossibilityGS (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.72)
03:27:37 Running Sunflowers ...
03:27:37 Stewart_Apollonius: theory Triangle.Triangle
03:27:37 VeriComp: theory VeriComp.Behaviour
03:27:37 VeriComp: theory VeriComp.Transfer_Extras
03:27:37 VeriComp: theory VeriComp.Well_founded
03:27:38 VeriComp: theory VeriComp.Inf
03:27:38 Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
03:27:38 Finished Chord_Segments/document (0:00:03 elapsed time)
03:27:38 Preparing Chord_Segments/outline ...
03:27:38 Preparing GaleStewart_Games/document ...
03:27:39 VeriComp: theory VeriComp.Semantics
03:27:39 Finished Triangle/document (0:00:02 elapsed time)
03:27:39 Preparing Triangle/outline ...
03:27:39 Sunflowers: theory HOL-Library.FuncSet
03:27:39 VeriComp: theory VeriComp.Language
03:27:39 VeriComp: theory VeriComp.Simulation
03:27:39 Finished Category/document (0:00:04 elapsed time)
03:27:39 Preparing Category/outline ...
03:27:40 Sunflowers: theory Sunflowers.Sunflower
03:27:40 VeriComp: theory VeriComp.Compiler
03:27:40 Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
03:27:40 VeriComp: theory VeriComp.Fixpoint
03:27:40 Preparing Goodstein_Lambda/document ...
03:27:40 Preparing Compiling-Exceptions-Correctly/document ...
03:27:41 Finished Triangle/outline (0:00:01 elapsed time)
03:27:41 Finished LatticeProperties/document (0:00:03 elapsed time)
03:27:41 Preparing LatticeProperties/outline ...
03:27:41 Finished Chord_Segments/outline (0:00:03 elapsed time)
03:27:41 Timing Chord_Segments (4 threads, 4.025s elapsed time, 8.828s cpu time, 0.156s GC time, factor 2.19)
03:27:41 Finished Chord_Segments (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.56)
03:27:41 Timing Triangle (4 threads, 4.121s elapsed time, 7.204s cpu time, 0.153s GC time, factor 1.75)
03:27:41 Finished Triangle (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.35)
03:27:41 Running DataRefinementIBP ...
03:27:41 Running CYK ...
03:27:42 Preparing VeriComp/document ...
03:27:42 Preparing Stewart_Apollonius/document ...
03:27:43 Finished Category/outline (0:00:03 elapsed time)
03:27:43 Finished GaleStewart_Games/document (0:00:04 elapsed time)
03:27:43 Preparing GaleStewart_Games/outline ...
03:27:43 Timing Category (4 threads, 3.901s elapsed time, 12.339s cpu time, 0.168s GC time, factor 3.16)
03:27:43 Finished Category (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.28)
03:27:43 Running Transitive-Closure ...
03:27:43 DataRefinementIBP: theory LatticeProperties.WellFoundedTransitive
03:27:43 CYK: theory CYK.CYK
03:27:43 DataRefinementIBP: theory LatticeProperties.Conj_Disj
03:27:43 Finished Compiling-Exceptions-Correctly/document (0:00:02 elapsed time)
03:27:43 Preparing Compiling-Exceptions-Correctly/outline ...
03:27:43 Preparing Sunflowers/document ...
03:27:44 DataRefinementIBP: theory LatticeProperties.Complete_Lattice_Prop
03:27:44 DataRefinementIBP: theory DataRefinementIBP.Preliminaries
03:27:44 Finished Goodstein_Lambda/document (0:00:03 elapsed time)
03:27:44 Preparing Goodstein_Lambda/outline ...
03:27:44 Finished LatticeProperties/outline (0:00:03 elapsed time)
03:27:44 DataRefinementIBP: theory DataRefinementIBP.Statements
03:27:44 Timing LatticeProperties (4 threads, 3.889s elapsed time, 8.392s cpu time, 0.217s GC time, factor 2.16)
03:27:44 Finished LatticeProperties (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.68)
03:27:44 Running C2KA_DistributedSystems ...
03:27:44 DataRefinementIBP: theory DataRefinementIBP.Hoare
03:27:44 Finished Stewart_Apollonius/document (0:00:02 elapsed time)
03:27:44 Preparing Stewart_Apollonius/outline ...
03:27:45 DataRefinementIBP: theory DataRefinementIBP.Diagram
03:27:45 DataRefinementIBP: theory DataRefinementIBP.DataRefinement
03:27:45 Finished VeriComp/document (0:00:03 elapsed time)
03:27:45 Preparing VeriComp/outline ...
03:27:46 Finished Compiling-Exceptions-Correctly/outline (0:00:02 elapsed time)
03:27:46 C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
03:27:46 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
03:27:46 Timing Compiling-Exceptions-Correctly (4 threads, 3.956s elapsed time, 6.935s cpu time, 0.308s GC time, factor 1.75)
03:27:46 Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.43)
03:27:46 Running DPT-SAT-Solver ...
03:27:47 Finished GaleStewart_Games/outline (0:00:03 elapsed time)
03:27:47 Transitive-Closure: theory Matrix.Utility
03:27:47 Timing GaleStewart_Games (4 threads, 3.805s elapsed time, 12.652s cpu time, 0.249s GC time, factor 3.33)
03:27:47 Finished GaleStewart_Games (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.22)
03:27:47 Running Stuttering_Equivalence ...
03:27:47 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
03:27:47 Preparing DataRefinementIBP/document ...
03:27:47 Finished Sunflowers/document (0:00:03 elapsed time)
03:27:47 Preparing Sunflowers/outline ...
03:27:47 Finished Stewart_Apollonius/outline (0:00:02 elapsed time)
03:27:47 Preparing CYK/document ...
03:27:47 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
03:27:47 Timing Stewart_Apollonius (4 threads, 4.133s elapsed time, 7.599s cpu time, 0.151s GC time, factor 1.84)
03:27:47 Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.40)
03:27:47 Running Mason_Stothers ...
03:27:47 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
03:27:47 Finished Goodstein_Lambda/outline (0:00:03 elapsed time)
03:27:47 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
03:27:48 Timing Goodstein_Lambda (4 threads, 3.807s elapsed time, 9.453s cpu time, 0.215s GC time, factor 2.48)
03:27:48 Finished Goodstein_Lambda (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.87)
03:27:48 Running Szpilrajn ...
03:27:48 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
03:27:48 C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
03:27:48 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Solver
03:27:49 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
03:27:49 Finished VeriComp/outline (0:00:03 elapsed time)
03:27:49 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
03:27:49 Timing VeriComp (4 threads, 3.588s elapsed time, 8.684s cpu time, 0.234s GC time, factor 2.42)
03:27:49 Finished VeriComp (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.81)
03:27:49 Running Fresh_Identifiers ...
03:27:50 Szpilrajn: theory Szpilrajn.Szpilrajn
03:27:50 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Tests
03:27:50 Finished Sunflowers/outline (0:00:02 elapsed time)
03:27:50 Timing Sunflowers (4 threads, 3.633s elapsed time, 11.308s cpu time, 0.138s GC time, factor 3.11)
03:27:50 Finished Sunflowers (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.26)
03:27:50 Running Fisher_Yates ...
03:27:50 Preparing C2KA_DistributedSystems/document ...
03:27:50 Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
03:27:51 Finished DataRefinementIBP/document (0:00:03 elapsed time)
03:27:51 Preparing DataRefinementIBP/outline ...
03:27:51 Fresh_Identifiers: theory Fresh_Identifiers.Fresh
03:27:51 Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
03:27:51 Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
03:27:51 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
03:27:51 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
03:27:51 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
03:27:51 Finished CYK/document (0:00:03 elapsed time)
03:27:51 Preparing CYK/outline ...
03:27:51 Preparing Transitive-Closure/document ...
03:27:51 Mason_Stothers: theory Mason_Stothers.Mason_Stothers
03:27:52 Preparing DPT-SAT-Solver/document ...
03:27:53 Preparing Szpilrajn/document ...
03:27:54 Finished C2KA_DistributedSystems/document (0:00:03 elapsed time)
03:27:54 Preparing C2KA_DistributedSystems/outline ...
03:27:54 Finished DPT-SAT-Solver/document (0:00:01 elapsed time)
03:27:54 Preparing DPT-SAT-Solver/outline ...
03:27:54 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
03:27:54 Preparing Stuttering_Equivalence/document ...
03:27:54 Finished DataRefinementIBP/outline (0:00:03 elapsed time)
03:27:54 Finished CYK/outline (0:00:03 elapsed time)
03:27:54 Preparing Fresh_Identifiers/document ...
03:27:54 Timing DataRefinementIBP (4 threads, 3.276s elapsed time, 7.420s cpu time, 0.193s GC time, factor 2.26)
03:27:54 Finished DataRefinementIBP (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.69)
03:27:54 Timing CYK (4 threads, 3.468s elapsed time, 10.063s cpu time, 0.274s GC time, factor 2.90)
03:27:54 Finished CYK (0:00:05 elapsed time, 0:00:12 cpu time, factor 2.12)
03:27:54 Running List_Interleaving ...
03:27:54 Running Lifting_Definition_Option ...
03:27:55 Finished Transitive-Closure/document (0:00:03 elapsed time)
03:27:55 Preparing Transitive-Closure/outline ...
03:27:55 Preparing Mason_Stothers/document ...
03:27:56 Finished DPT-SAT-Solver/outline (0:00:01 elapsed time)
03:27:56 Timing DPT-SAT-Solver (4 threads, 3.273s elapsed time, 6.682s cpu time, 0.062s GC time, factor 2.04)
03:27:56 Finished DPT-SAT-Solver (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.56)
03:27:56 Running GenClock ...
03:27:56 Finished Fresh_Identifiers/document (0:00:01 elapsed time)
03:27:56 Preparing Fresh_Identifiers/outline ...
03:27:56 List_Interleaving: theory List_Interleaving.ListInterleaving
03:27:56 Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
03:27:57 Finished Szpilrajn/document (0:00:03 elapsed time)
03:27:57 Preparing Szpilrajn/outline ...
03:27:57 Finished C2KA_DistributedSystems/outline (0:00:03 elapsed time)
03:27:57 Preparing Fisher_Yates/document ...
03:27:57 Timing C2KA_DistributedSystems (4 threads, 3.349s elapsed time, 5.352s cpu time, 0.196s GC time, factor 1.60)
03:27:57 Finished C2KA_DistributedSystems (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.32)
03:27:57 Running Mereology ...
03:27:58 GenClock: theory GenClock.GenClock
03:27:58 Finished Fresh_Identifiers/outline (0:00:01 elapsed time)
03:27:58 Timing Fresh_Identifiers (4 threads, 2.996s elapsed time, 7.121s cpu time, 0.147s GC time, factor 2.38)
03:27:58 Finished Fresh_Identifiers (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.73)
03:27:58 Running Card_Number_Partitions ...
03:27:58 Finished Stuttering_Equivalence/document (0:00:04 elapsed time)
03:27:58 Preparing Stuttering_Equivalence/outline ...
03:27:58 Finished Mason_Stothers/document (0:00:03 elapsed time)
03:27:58 Preparing Mason_Stothers/outline ...
03:27:58 Finished Transitive-Closure/outline (0:00:03 elapsed time)
03:27:58 Timing Transitive-Closure (4 threads, 3.522s elapsed time, 10.301s cpu time, 0.264s GC time, factor 2.92)
03:27:58 Finished Transitive-Closure (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.80)
03:27:58 Running Gauss-Jordan-Elim-Fun ...
03:27:59 Preparing List_Interleaving/document ...
03:27:59 Mereology: theory Mereology.PM
03:27:59 Preparing Lifting_Definition_Option/document ...
03:27:59 Mereology: theory Mereology.M
03:28:00 Mereology: theory Mereology.CM
03:28:00 Mereology: theory Mereology.MM
03:28:00 Finished Szpilrajn/outline (0:00:02 elapsed time)
03:28:00 Mereology: theory Mereology.EM
03:28:00 Timing Szpilrajn (4 threads, 2.990s elapsed time, 7.773s cpu time, 0.104s GC time, factor 2.60)
03:28:00 Finished Szpilrajn (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.84)
03:28:00 Running Pairing_Heap ...
03:28:00 Mereology: theory Mereology.GM
03:28:00 Mereology: theory Mereology.CEM
03:28:00 Mereology: theory Mereology.GMM
03:28:00 Gauss-Jordan-Elim-Fun: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
03:28:00 Finished Fisher_Yates/document (0:00:03 elapsed time)
03:28:00 Preparing Fisher_Yates/outline ...
03:28:01 Finished Mason_Stothers/outline (0:00:02 elapsed time)
03:28:01 Mereology: theory Mereology.GEM
03:28:01 Timing Mason_Stothers (4 threads, 3.096s elapsed time, 7.128s cpu time, 0.140s GC time, factor 2.30)
03:28:01 Finished Mason_Stothers (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.49)
03:28:01 Running Discrete_Summation ...
03:28:01 Preparing GenClock/document ...
03:28:01 Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
03:28:01 Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
03:28:01 Finished Stuttering_Equivalence/outline (0:00:03 elapsed time)
03:28:01 Timing Stuttering_Equivalence (4 threads, 2.886s elapsed time, 8.684s cpu time, 0.226s GC time, factor 3.01)
03:28:01 Finished Stuttering_Equivalence (0:00:06 elapsed time, 0:00:12 cpu time, factor 1.80)
03:28:01 Running BinarySearchTree ...
03:28:02 Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
03:28:02 Finished Lifting_Definition_Option/document (0:00:03 elapsed time)
03:28:02 Preparing Lifting_Definition_Option/outline ...
03:28:03 Discrete_Summation: theory Discrete_Summation.Discrete_Summation
03:28:03 Discrete_Summation: theory HOL-Combinatorics.Stirling
03:28:03 Discrete_Summation: theory Discrete_Summation.Factorials
03:28:03 Pairing_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
03:28:03 BinarySearchTree: theory BinarySearchTree.BinaryTree
03:28:03 BinarySearchTree: theory BinarySearchTree.BinaryTree_TacticStyle
03:28:03 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List2
03:28:03 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List1
03:28:03 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_Tree
03:28:03 Finished Fisher_Yates/outline (0:00:03 elapsed time)
03:28:03 Preparing Mereology/document ...
03:28:03 Timing Fisher_Yates (4 threads, 2.708s elapsed time, 7.838s cpu time, 0.145s GC time, factor 2.89)
03:28:03 Finished Fisher_Yates (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.66)
03:28:03 Running ClockSynchInst ...
03:28:03 Preparing Gauss-Jordan-Elim-Fun/document ...
03:28:04 Discrete_Summation: theory Discrete_Summation.Summation_Conversion
03:28:04 Finished List_Interleaving/document (0:00:04 elapsed time)
03:28:04 Preparing List_Interleaving/outline ...
03:28:04 Discrete_Summation: theory Discrete_Summation.Examples
03:28:05 Preparing Card_Number_Partitions/document ...
03:28:05 BinarySearchTree: theory BinarySearchTree.BinaryTree_Map
03:28:05 Finished GenClock/document (0:00:03 elapsed time)
03:28:05 Preparing GenClock/outline ...
03:28:05 ClockSynchInst: theory ClockSynchInst.ICAInstance
03:28:05 ClockSynchInst: theory ClockSynchInst.LynchInstance
03:28:05 Finished Gauss-Jordan-Elim-Fun/document (0:00:01 elapsed time)
03:28:05 Preparing Gauss-Jordan-Elim-Fun/outline ...
03:28:06 Finished Lifting_Definition_Option/outline (0:00:03 elapsed time)
03:28:06 Preparing Discrete_Summation/document ...
03:28:06 Timing Lifting_Definition_Option (4 threads, 2.766s elapsed time, 3.425s cpu time, 0.000s GC time, factor 1.24)
03:28:06 Finished Lifting_Definition_Option (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.06)
03:28:06 Running Surprise_Paradox ...
03:28:06 Preparing BinarySearchTree/document ...
03:28:06 Preparing Pairing_Heap/document ...
03:28:07 Finished List_Interleaving/outline (0:00:03 elapsed time)
03:28:07 Timing List_Interleaving (4 threads, 2.449s elapsed time, 6.799s cpu time, 0.236s GC time, factor 2.78)
03:28:07 Finished List_Interleaving (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.87)
03:28:07 Running Descartes_Sign_Rule ...
03:28:07 Finished Gauss-Jordan-Elim-Fun/outline (0:00:01 elapsed time)
03:28:08 Timing Gauss-Jordan-Elim-Fun (4 threads, 2.601s elapsed time, 7.026s cpu time, 0.093s GC time, factor 2.70)
03:28:08 Finished Gauss-Jordan-Elim-Fun (0:00:04 elapsed time, 0:00:09 cpu time, factor 1.82)
03:28:08 Running List-Index ...
03:28:08 Finished Discrete_Summation/document (0:00:02 elapsed time)
03:28:08 Preparing Discrete_Summation/outline ...
03:28:08 Finished GenClock/outline (0:00:03 elapsed time)
03:28:08 Preparing ClockSynchInst/document ...
03:28:08 Finished Card_Number_Partitions/document (0:00:03 elapsed time)
03:28:08 Preparing Card_Number_Partitions/outline ...
03:28:09 Timing GenClock (4 threads, 2.689s elapsed time, 9.294s cpu time, 0.143s GC time, factor 3.46)
03:28:09 Finished GenClock (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.25)
03:28:09 Running Skew_Heap ...
03:28:09 Finished BinarySearchTree/document (0:00:02 elapsed time)
03:28:09 Preparing BinarySearchTree/outline ...
03:28:09 List-Index: theory List-Index.List_Index
03:28:09 Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
03:28:09 Finished Pairing_Heap/document (0:00:03 elapsed time)
03:28:10 Preparing Pairing_Heap/outline ...
03:28:10 Finished Discrete_Summation/outline (0:00:01 elapsed time)
03:28:10 Timing Discrete_Summation (4 threads, 2.446s elapsed time, 9.272s cpu time, 0.145s GC time, factor 3.79)
03:28:10 Finished Discrete_Summation (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.35)
03:28:10 Running Lazy-Lists-II ...
03:28:10 Finished Mereology/document (0:00:06 elapsed time)
03:28:10 Preparing Mereology/outline ...
03:28:11 Finished BinarySearchTree/outline (0:00:01 elapsed time)
03:28:11 Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
03:28:11 Timing BinarySearchTree (4 threads, 2.388s elapsed time, 7.997s cpu time, 0.289s GC time, factor 3.35)
03:28:11 Finished BinarySearchTree (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.12)
03:28:11 Running Open_Induction ...
03:28:11 Finished Card_Number_Partitions/outline (0:00:02 elapsed time)
03:28:12 Timing Card_Number_Partitions (4 threads, 2.711s elapsed time, 9.367s cpu time, 0.133s GC time, factor 3.46)
03:28:12 Finished Card_Number_Partitions (0:00:06 elapsed time, 0:00:12 cpu time, factor 1.95)
03:28:12 Running Perfect-Number-Thm ...
03:28:12 Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
03:28:12 Skew_Heap: theory HOL-Data_Structures.Heaps
03:28:12 Preparing List-Index/document ...
03:28:12 Finished ClockSynchInst/document (0:00:04 elapsed time)
03:28:12 Preparing ClockSynchInst/outline ...
03:28:12 Preparing Surprise_Paradox/document ...
03:28:12 Finished Pairing_Heap/outline (0:00:02 elapsed time)
03:28:12 Skew_Heap: theory Skew_Heap.Skew_Heap
03:28:13 Timing Pairing_Heap (4 threads, 2.514s elapsed time, 8.777s cpu time, 0.428s GC time, factor 3.49)
03:28:13 Finished Pairing_Heap (0:00:06 elapsed time, 0:00:12 cpu time, factor 1.92)
03:28:13 Running Lucas_Theorem ...
03:28:13 Open_Induction: theory Open_Induction.Restricted_Predicates
03:28:13 Open_Induction: theory Open_Induction.Open_Induction
03:28:14 Preparing Descartes_Sign_Rule/document ...
03:28:14 Finished List-Index/document (0:00:02 elapsed time)
03:28:14 Preparing List-Index/outline ...
03:28:14 Preparing Skew_Heap/document ...
03:28:14 Finished Mereology/outline (0:00:03 elapsed time)
03:28:14 Lazy-Lists-II: theory Lazy-Lists-II.LList2
03:28:15 Timing Mereology (4 threads, 2.640s elapsed time, 8.235s cpu time, 0.400s GC time, factor 3.12)
03:28:15 Finished Mereology (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.82)
03:28:15 Running Marriage ...
03:28:15 Preparing Open_Induction/document ...
03:28:15 Finished ClockSynchInst/outline (0:00:03 elapsed time)
03:28:16 Timing ClockSynchInst (4 threads, 2.106s elapsed time, 7.943s cpu time, 0.130s GC time, factor 3.77)
03:28:16 Finished ClockSynchInst (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.27)
03:28:16 Running Lifting_the_Exponent ...
03:28:16 Finished Surprise_Paradox/document (0:00:03 elapsed time)
03:28:16 Preparing Surprise_Paradox/outline ...
03:28:16 Finished List-Index/outline (0:00:01 elapsed time)
03:28:16 Timing List-Index (4 threads, 1.974s elapsed time, 6.837s cpu time, 0.136s GC time, factor 3.46)
03:28:16 Finished List-Index (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.06)
03:28:16 Running Cartan_FP ...
03:28:16 Marriage: theory Marriage.Marriage
03:28:17 Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem
03:28:17 Finished Skew_Heap/document (0:00:02 elapsed time)
03:28:17 Preparing Skew_Heap/outline ...
03:28:17 Preparing Lazy-Lists-II/document ...
03:28:17 Finished Descartes_Sign_Rule/document (0:00:03 elapsed time)
03:28:17 Preparing Descartes_Sign_Rule/outline ...
03:28:18 Preparing Marriage/document ...
03:28:19 Finished Open_Induction/document (0:00:03 elapsed time)
03:28:19 Preparing Open_Induction/outline ...
03:28:19 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
03:28:19 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
03:28:19 Finished Surprise_Paradox/outline (0:00:03 elapsed time)
03:28:19 Preparing Lucas_Theorem/document ...
03:28:19 Timing Surprise_Paradox (4 threads, 2.261s elapsed time, 4.096s cpu time, 0.000s GC time, factor 1.81)
03:28:19 Finished Surprise_Paradox (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.24)
03:28:19 Running Max-Card-Matching ...
03:28:19 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
03:28:19 Finished Skew_Heap/outline (0:00:02 elapsed time)
03:28:20 Cartan_FP: theory Cartan_FP.Cartan
03:28:20 Timing Skew_Heap (4 threads, 1.902s elapsed time, 2.893s cpu time, 0.000s GC time, factor 1.52)
03:28:20 Finished Skew_Heap (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.14)
03:28:20 Running Liouville_Numbers ...
03:28:20 Finished Descartes_Sign_Rule/outline (0:00:02 elapsed time)
03:28:20 Timing Descartes_Sign_Rule (4 threads, 2.086s elapsed time, 7.180s cpu time, 0.114s GC time, factor 3.44)
03:28:20 Finished Descartes_Sign_Rule (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.77)
03:28:20 Running CofGroups ...
03:28:20 Finished Lazy-Lists-II/document (0:00:03 elapsed time)
03:28:20 Preparing Lazy-Lists-II/outline ...
03:28:21 Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
03:28:21 Max-Card-Matching: theory Max-Card-Matching.Matching
03:28:21 Preparing Perfect-Number-Thm/document ...
03:28:21 Finished Marriage/document (0:00:02 elapsed time)
03:28:21 Preparing Marriage/outline ...
03:28:22 Preparing Cartan_FP/document ...
03:28:22 Finished Open_Induction/outline (0:00:03 elapsed time)
03:28:22 CofGroups: theory HOL-Library.Nat_Bijection
03:28:22 Timing Open_Induction (4 threads, 1.659s elapsed time, 5.252s cpu time, 0.164s GC time, factor 3.17)
03:28:22 Finished Open_Induction (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.84)
03:28:22 Running Blue_Eyes ...
03:28:22 Finished Lucas_Theorem/document (0:00:03 elapsed time)
03:28:22 Preparing Lucas_Theorem/outline ...
03:28:23 CofGroups: theory CofGroups.CofGroups
03:28:23 Preparing Lifting_the_Exponent/document ...
03:28:23 Preparing Max-Card-Matching/document ...
03:28:23 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
03:28:24 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
03:28:24 Preparing CofGroups/document ...
03:28:24 Finished Lazy-Lists-II/outline (0:00:03 elapsed time)
03:28:24 Finished Perfect-Number-Thm/document (0:00:02 elapsed time)
03:28:24 Preparing Perfect-Number-Thm/outline ...
03:28:24 Finished Marriage/outline (0:00:02 elapsed time)
03:28:24 Blue_Eyes: theory Blue_Eyes.Blue_Eyes
03:28:24 Timing Marriage (4 threads, 1.587s elapsed time, 5.398s cpu time, 0.087s GC time, factor 3.40)
03:28:24 Finished Marriage (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.92)
03:28:24 Timing Lazy-Lists-II (4 threads, 1.786s elapsed time, 5.035s cpu time, 0.000s GC time, factor 2.82)
03:28:24 Finished Lazy-Lists-II (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.45)
03:28:24 Running RIPEMD-160-SPARK ...
03:28:24 Running Combinatorics_Words_Graph_Lemma ...
03:28:25 Finished Cartan_FP/document (0:00:03 elapsed time)
03:28:25 Preparing Cartan_FP/outline ...
03:28:25 Finished Lucas_Theorem/outline (0:00:02 elapsed time)
03:28:25 Timing Lucas_Theorem (4 threads, 1.623s elapsed time, 5.289s cpu time, 0.113s GC time, factor 3.26)
03:28:25 Finished Lucas_Theorem (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.54)
03:28:25 Running Lehmer ...
03:28:25 Preparing Liouville_Numbers/document ...
03:28:26 Preparing Blue_Eyes/document ...
03:28:26 Finished Max-Card-Matching/document (0:00:03 elapsed time)
03:28:26 Preparing Max-Card-Matching/outline ...
03:28:26 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
03:28:27 Finished Perfect-Number-Thm/outline (0:00:02 elapsed time)
03:28:27 Timing Perfect-Number-Thm (4 threads, 1.633s elapsed time, 4.760s cpu time, 0.000s GC time, factor 2.91)
03:28:27 Finished Perfect-Number-Thm (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.30)
03:28:27 Running AnselmGod ...
03:28:27 Finished Lifting_the_Exponent/document (0:00:04 elapsed time)
03:28:27 Preparing Lifting_the_Exponent/outline ...
03:28:27 Finished CofGroups/document (0:00:03 elapsed time)
03:28:27 Preparing CofGroups/outline ...
03:28:27 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
03:28:28 Finished Cartan_FP/outline (0:00:02 elapsed time)
03:28:28 Timing Cartan_FP (4 threads, 1.444s elapsed time, 5.085s cpu time, 0.129s GC time, factor 3.52)
03:28:28 Finished Cartan_FP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.65)
03:28:28 Running FunWithFunctions ...
03:28:28 Preparing RIPEMD-160-SPARK/document ...
03:28:28 Finished Liouville_Numbers/document (0:00:03 elapsed time)
03:28:28 Preparing Liouville_Numbers/outline ...
03:28:29 AnselmGod: theory AnselmGod.AnselmGod
03:28:29 Finished Max-Card-Matching/outline (0:00:02 elapsed time)
03:28:29 Finished Blue_Eyes/document (0:00:03 elapsed time)
03:28:29 Preparing Blue_Eyes/outline ...
03:28:29 Timing Max-Card-Matching (4 threads, 1.475s elapsed time, 4.123s cpu time, 0.000s GC time, factor 2.80)
03:28:29 Finished Max-Card-Matching (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.62)
03:28:29 Running Monad_Normalisation ...
03:28:29 Preparing Combinatorics_Words_Graph_Lemma/document ...
03:28:30 FunWithFunctions: theory FunWithFunctions.FunWithFunctions
03:28:30 Finished CofGroups/outline (0:00:03 elapsed time)
03:28:30 Finished Lifting_the_Exponent/outline (0:00:03 elapsed time)
03:28:30 Lehmer: theory Lehmer.Lehmer
03:28:30 Preparing AnselmGod/document ...
03:28:30 Timing CofGroups (4 threads, 1.197s elapsed time, 3.431s cpu time, 0.000s GC time, factor 2.87)
03:28:30 Finished CofGroups (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.57)
03:28:30 Timing Lifting_the_Exponent (4 threads, 1.511s elapsed time, 5.108s cpu time, 0.118s GC time, factor 3.38)
03:28:30 Finished Lifting_the_Exponent (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.47)
03:28:30 Running Minkowskis_Theorem ...
03:28:30 Running Ptolemys_Theorem ...
03:28:31 Finished RIPEMD-160-SPARK/document (0:00:02 elapsed time)
03:28:31 Preparing RIPEMD-160-SPARK/outline ...
03:28:31 Finished Liouville_Numbers/outline (0:00:02 elapsed time)
03:28:31 Preparing FunWithFunctions/document ...
03:28:31 Timing Liouville_Numbers (4 threads, 1.400s elapsed time, 3.891s cpu time, 0.000s GC time, factor 2.78)
03:28:31 Finished Liouville_Numbers (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.42)
03:28:31 Running Lorenz_C1 ...
03:28:32 Finished Blue_Eyes/outline (0:00:02 elapsed time)
03:28:32 Preparing Lehmer/document ...
03:28:32 Timing Blue_Eyes (4 threads, 1.303s elapsed time, 2.766s cpu time, 0.000s GC time, factor 2.12)
03:28:32 Finished Blue_Eyes (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.32)
03:28:32 Running Free-Boolean-Algebra ...
03:28:33 Finished RIPEMD-160-SPARK/outline (0:00:02 elapsed time)
03:28:33 Finished AnselmGod/document (0:00:02 elapsed time)
03:28:33 Preparing AnselmGod/outline ...
03:28:33 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
03:28:33 Timing RIPEMD-160-SPARK (4 threads, 1.313s elapsed time, 1.386s cpu time, 0.000s GC time, factor 1.06)
03:28:33 Finished RIPEMD-160-SPARK (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.92)
03:28:33 Running Depth-First-Search ...
03:28:34 Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
03:28:34 Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
03:28:34 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
03:28:34 Finished FunWithFunctions/document (0:00:02 elapsed time)
03:28:34 Preparing FunWithFunctions/outline ...
03:28:34 Free-Boolean-Algebra: theory Free-Boolean-Algebra.Free_Boolean_Algebra
03:28:35 Finished Combinatorics_Words_Graph_Lemma/document (0:00:05 elapsed time)
03:28:35 Preparing Combinatorics_Words_Graph_Lemma/outline ...
03:28:35 Preparing Monad_Normalisation/document ...
03:28:35 Finished Lehmer/document (0:00:02 elapsed time)
03:28:35 Preparing Lehmer/outline ...
03:28:35 Depth-First-Search: theory Depth-First-Search.DFS
03:28:35 Preparing Ptolemys_Theorem/document ...
03:28:36 Preparing Free-Boolean-Algebra/document ...
03:28:36 Preparing Minkowskis_Theorem/document ...
03:28:36 Finished AnselmGod/outline (0:00:03 elapsed time)
03:28:36 Timing AnselmGod (4 threads, 1.215s elapsed time, 3.480s cpu time, 0.000s GC time, factor 2.86)
03:28:36 Finished AnselmGod (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.56)
03:28:36 Running Laws_of_Large_Numbers ...
03:28:36 Preparing Depth-First-Search/document ...
03:28:37 Finished FunWithFunctions/outline (0:00:02 elapsed time)
03:28:37 Timing FunWithFunctions (4 threads, 1.165s elapsed time, 2.978s cpu time, 0.000s GC time, factor 2.56)
03:28:37 Finished FunWithFunctions (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.43)
03:28:37 Running FFT ...
03:28:38 Finished Free-Boolean-Algebra/document (0:00:01 elapsed time)
03:28:38 Preparing Free-Boolean-Algebra/outline ...
03:28:38 Finished Lehmer/outline (0:00:02 elapsed time)
03:28:38 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
03:28:38 Timing Lehmer (4 threads, 1.158s elapsed time, 3.017s cpu time, 0.000s GC time, factor 2.61)
03:28:38 Finished Lehmer (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.23)
03:28:38 Running Conditional_Simplification ...
03:28:38 Finished Depth-First-Search/document (0:00:01 elapsed time)
03:28:38 Preparing Depth-First-Search/outline ...
03:28:38 Finished Monad_Normalisation/document (0:00:03 elapsed time)
03:28:38 Preparing Monad_Normalisation/outline ...
03:28:38 Finished Ptolemys_Theorem/document (0:00:03 elapsed time)
03:28:38 Preparing Ptolemys_Theorem/outline ...
03:28:39 FFT: theory FFT.FFT
03:28:39 Finished Minkowskis_Theorem/document (0:00:03 elapsed time)
03:28:39 Preparing Minkowskis_Theorem/outline ...
03:28:40 Finished Combinatorics_Words_Graph_Lemma/outline (0:00:04 elapsed time)
03:28:40 Finished Free-Boolean-Algebra/outline (0:00:01 elapsed time)
03:28:40 Conditional_Simplification: theory Conditional_Simplification.CS_Tools
03:28:40 Conditional_Simplification: theory HOL-Library.LaTeXsugar
03:28:40 Conditional_Simplification: theory Conditional_Simplification.IHOL_CS
03:28:40 Conditional_Simplification: theory Conditional_Simplification.Reference_Prerequisites
03:28:40 Timing Free-Boolean-Algebra (4 threads, 1.050s elapsed time, 2.312s cpu time, 0.000s GC time, factor 2.20)
03:28:40 Finished Free-Boolean-Algebra (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.30)
03:28:40 Timing Combinatorics_Words_Graph_Lemma (4 threads, 1.242s elapsed time, 4.056s cpu time, 0.000s GC time, factor 3.27)
03:28:40 Finished Combinatorics_Words_Graph_Lemma (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.50)
03:28:40 Timing Lorenz_C1 (4 threads, 1.233s elapsed time, 1.876s cpu time, 0.000s GC time, factor 1.52)
03:28:40 Finished Lorenz_C1 (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.04)
03:28:40 Running Bondy ...
03:28:40 Running Intro_Dest_Elim ...
03:28:40 Running Card_Equiv_Relations ...
03:28:40 Finished Depth-First-Search/outline (0:00:01 elapsed time)
03:28:40 Preparing FFT/document ...
03:28:40 Conditional_Simplification: theory Conditional_Simplification.CS_Reference
03:28:40 Timing Depth-First-Search (4 threads, 0.899s elapsed time, 1.965s cpu time, 0.000s GC time, factor 2.19)
03:28:40 Finished Depth-First-Search (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.26)
03:28:40 Running General-Triangle ...
03:28:41 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
03:28:41 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
03:28:41 Preparing Conditional_Simplification/document ...
03:28:41 Finished Ptolemys_Theorem/outline (0:00:02 elapsed time)
03:28:41 Timing Ptolemys_Theorem (4 threads, 1.152s elapsed time, 3.167s cpu time, 0.000s GC time, factor 2.75)
03:28:41 Finished Ptolemys_Theorem (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.35)
03:28:41 Running Roy_Floyd_Warshall ...
03:28:42 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Tools
03:28:42 Intro_Dest_Elim: theory HOL-Library.LaTeXsugar
03:28:42 Bondy: theory Bondy.Bondy
03:28:42 Finished Monad_Normalisation/outline (0:00:03 elapsed time)
03:28:42 Intro_Dest_Elim: theory Intro_Dest_Elim.IHOL_IDE
03:28:42 Intro_Dest_Elim: theory Intro_Dest_Elim.Reference_Prerequisites
03:28:42 Timing Monad_Normalisation (4 threads, 1.153s elapsed time, 1.767s cpu time, 0.000s GC time, factor 1.53)
03:28:42 Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.06)
03:28:42 Running Aristotles_Assertoric_Syllogistic ...
03:28:42 Finished Minkowskis_Theorem/outline (0:00:02 elapsed time)
03:28:42 Preparing Laws_of_Large_Numbers/document ...
03:28:42 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Reference
03:28:42 General-Triangle: theory General-Triangle.GeneralTriangle
03:28:42 Finished FFT/document (0:00:02 elapsed time)
03:28:42 Preparing FFT/outline ...
03:28:42 Timing Minkowskis_Theorem (4 threads, 1.548s elapsed time, 4.384s cpu time, 0.000s GC time, factor 2.83)
03:28:42 Finished Minkowskis_Theorem (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.47)
03:28:42 Running Ordinals_and_Cardinals ...
03:28:43 Preparing Intro_Dest_Elim/document ...
03:28:43 Preparing Bondy/document ...
03:28:43 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Equiv_Relations
03:28:43 Preparing General-Triangle/document ...
03:28:43 Roy_Floyd_Warshall: theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
03:28:43 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
03:28:44 Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
03:28:44 Finished FFT/outline (0:00:01 elapsed time)
03:28:44 Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
03:28:44 Preparing Roy_Floyd_Warshall/document ...
03:28:44 Preparing Card_Equiv_Relations/document ...
03:28:44 Timing FFT (4 threads, 0.920s elapsed time, 3.123s cpu time, 0.000s GC time, factor 3.39)
03:28:44 Finished FFT (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.60)
03:28:44 Running Example-Submission ...
03:28:45 Preparing Aristotles_Assertoric_Syllogistic/document ...
03:28:45 Preparing Ordinals_and_Cardinals/document ...
03:28:45 Finished Laws_of_Large_Numbers/document (0:00:03 elapsed time)
03:28:45 Preparing Laws_of_Large_Numbers/outline ...
03:28:45 Finished Bondy/document (0:00:02 elapsed time)
03:28:45 Preparing Bondy/outline ...
03:28:46 Example-Submission: theory Example-Submission.Submission
03:28:46 Finished Ordinals_and_Cardinals/document (0:00:01 elapsed time)
03:28:46 Preparing Ordinals_and_Cardinals/outline ...
03:28:46 Finished Aristotles_Assertoric_Syllogistic/document (0:00:01 elapsed time)
03:28:46 Preparing Aristotles_Assertoric_Syllogistic/outline ...
03:28:46 Finished Conditional_Simplification/document (0:00:05 elapsed time)
03:28:46 Preparing Conditional_Simplification/outline ...
03:28:47 Preparing Example-Submission/document ...
03:28:47 Finished Roy_Floyd_Warshall/document (0:00:02 elapsed time)
03:28:47 Preparing Roy_Floyd_Warshall/outline ...
03:28:47 Finished Card_Equiv_Relations/document (0:00:02 elapsed time)
03:28:47 Preparing Card_Equiv_Relations/outline ...
03:28:47 Finished General-Triangle/document (0:00:04 elapsed time)
03:28:47 Preparing General-Triangle/outline ...
03:28:48 Finished Ordinals_and_Cardinals/outline (0:00:01 elapsed time)
03:28:48 Finished Bondy/outline (0:00:02 elapsed time)
03:28:48 Timing Bondy (4 threads, 0.728s elapsed time, 0.908s cpu time, 0.000s GC time, factor 1.25)
03:28:48 Finished Bondy (0:00:02 elapsed time)
03:28:48 Timing Ordinals_and_Cardinals (4 threads, 0.109s elapsed time, 0.157s cpu time, 0.000s GC time, factor 1.44)
03:28:48 Finished Ordinals_and_Cardinals (0:00:02 elapsed time)
03:28:48 Finished Aristotles_Assertoric_Syllogistic/outline (0:00:01 elapsed time)
03:28:48 Finished Laws_of_Large_Numbers/outline (0:00:02 elapsed time)
03:28:48 Finished Intro_Dest_Elim/document (0:00:05 elapsed time)
03:28:48 Preparing Intro_Dest_Elim/outline ...
03:28:48 Timing Aristotles_Assertoric_Syllogistic (4 threads, 0.405s elapsed time, 0.948s cpu time, 0.000s GC time, factor 2.34)
03:28:48 Finished Aristotles_Assertoric_Syllogistic (0:00:02 elapsed time)
03:28:49 Timing Laws_of_Large_Numbers (4 threads, 0.909s elapsed time, 2.681s cpu time, 0.000s GC time, factor 2.95)
03:28:49 Finished Laws_of_Large_Numbers (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.26)
03:28:49 Finished Example-Submission/document (0:00:02 elapsed time)
03:28:49 Preparing Example-Submission/outline ...
03:28:50 Finished Roy_Floyd_Warshall/outline (0:00:02 elapsed time)
03:28:50 Finished Card_Equiv_Relations/outline (0:00:02 elapsed time)
03:28:50 Timing Card_Equiv_Relations (4 threads, 0.587s elapsed time, 1.885s cpu time, 0.000s GC time, factor 3.21)
03:28:50 Finished Card_Equiv_Relations (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.23)
03:28:50 Timing Roy_Floyd_Warshall (4 threads, 0.576s elapsed time, 1.263s cpu time, 0.000s GC time, factor 2.19)
03:28:50 Finished Roy_Floyd_Warshall (0:00:02 elapsed time, 0:00:03 cpu time)
03:28:51 Finished General-Triangle/outline (0:00:03 elapsed time)
03:28:51 Finished Example-Submission/outline (0:00:02 elapsed time)
03:28:52 Timing Example-Submission (4 threads, 0.113s elapsed time, 0.190s cpu time, 0.000s GC time, factor 1.68)
03:28:52 Finished Example-Submission (0:00:02 elapsed time)
03:28:52 Timing General-Triangle (4 threads, 0.652s elapsed time, 1.458s cpu time, 0.000s GC time, factor 2.24)
03:28:52 Finished General-Triangle (0:00:02 elapsed time, 0:00:03 cpu time)
03:28:52 Finished Conditional_Simplification/outline (0:00:05 elapsed time)
03:28:52 Timing Conditional_Simplification (4 threads, 0.764s elapsed time, 1.221s cpu time, 0.000s GC time, factor 1.60)
03:28:52 Finished Conditional_Simplification (0:00:02 elapsed time)
03:28:53 Finished Intro_Dest_Elim/outline (0:00:04 elapsed time)
03:28:53 Timing Intro_Dest_Elim (4 threads, 0.647s elapsed time, 0.947s cpu time, 0.000s GC time, factor 1.46)
03:28:53 Finished Intro_Dest_Elim (0:00:02 elapsed time)
03:28:53 Unfinished session(s): CZH_Elementary_Categories, CZH_Foundations, CZH_Universal_Constructions, Types_To_Sets_Extension
03:28:53 
03:28:53 === TIMING ===
03:28:53 
03:28:53 Group AFP: 22:48:32 elapsed time, 64:28:52 cpu time, factor 2.83
03:28:53 Group main: 0:43:00 elapsed time, 2:11:36 cpu time, factor 3.06
03:28:53 Group timing: 0:45:06 elapsed time, 2:16:35 cpu time, factor 3.03
03:28:53 Group large: 1:10:29 elapsed time, 4:24:30 cpu time, factor 3.75
03:28:53 Overall: 2:50:47 elapsed time, 67:06:29 cpu time, factor 23.58
03:28:53 
03:28:53 === FAILED SESSIONS ===
03:28:53 
03:28:53 Session CZH_Elementary_Categories: CANCELLED
03:28:53 Session Types_To_Sets_Extension: FAILED 1
03:28:53 Session CZH_Universal_Constructions: CANCELLED
03:28:53 Session CZH_Foundations: FAILED 1
03:28:53 
03:28:53 === DEPENDENCIES ===
03:28:53 
03:28:53 Generating dependencies file ...
03:28:59 Writing dependencies file ...
03:28:59 
03:28:59 === COMPLETED ===
03:28:59 
03:28:59 Build step 'Execute shell' marked build as failure
03:28:59 Started calculate disk usage of build
03:28:59 Finished Calculation of disk usage of build in 0 seconds
03:28:59 Started calculate disk usage of workspace
03:29:00 Finished Calculation of disk usage of workspace in 0 seconds
03:29:00 Finished: FAILURE