Skipping 792 KB.. Full Log

Finished Noninterference_Sequential_Composition/outline (0:00:04 elapsed time)
21:45:07 Timing Noninterference_Sequential_Composition (4 threads, 12.498s elapsed time, 42.928s cpu time, 1.644s GC time, factor 3.43)
21:45:07 Finished Noninterference_Sequential_Composition (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.40)
21:45:07 VerifyThis2019 CANCELLED
21:45:07 Running ConcurrentIMP ...
21:45:07 Finished TESL_Language/outline (0:00:05 elapsed time)
21:45:07 Timing TESL_Language (4 threads, 20.236s elapsed time, 65.741s cpu time, 2.155s GC time, factor 3.25)
21:45:07 Finished TESL_Language (0:00:23 elapsed time, 0:01:08 cpu time, factor 2.95)
21:45:07 Running Shivers-CFA ...
21:45:08 Preparing PSemigroupsConvolution/document ...
21:45:08 Finished Quaternions/outline (0:00:03 elapsed time)
21:45:09 Finished Abstract_Completeness/outline (0:00:03 elapsed time)
21:45:09 Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
21:45:09 Timing Quaternions (4 threads, 21.837s elapsed time, 28.377s cpu time, 0.967s GC time, factor 1.30)
21:45:09 Finished Quaternions (0:00:25 elapsed time, 0:00:32 cpu time, factor 1.24)
21:45:09 Timing Abstract_Completeness (4 threads, 10.435s elapsed time, 22.026s cpu time, 0.645s GC time, factor 2.11)
21:45:09 Finished Abstract_Completeness (0:00:32 elapsed time, 0:00:56 cpu time, factor 1.72)
21:45:09 Running Formal_Puiseux_Series ...
21:45:09 Running NormByEval ...
21:45:09 Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
21:45:09 Finished Optics/document (0:00:07 elapsed time)
21:45:09 Preparing Optics/outline ...
21:45:09 Shivers-CFA: theory HOL-Library.Adhoc_Overloading
21:45:09 Shivers-CFA: theory Shivers-CFA.FixTransform
21:45:09 Shivers-CFA: theory Shivers-CFA.HOLCFUtils
21:45:09 Shivers-CFA: theory Shivers-CFA.CPSScheme
21:45:10 Shivers-CFA: theory Shivers-CFA.SetMap
21:45:10 Shivers-CFA: theory Shivers-CFA.Computability
21:45:10 Shivers-CFA: theory Shivers-CFA.Utils
21:45:10 Shivers-CFA: theory Shivers-CFA.MapSets
21:45:10 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
21:45:10 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
21:45:10 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
21:45:11 ConcurrentIMP: theory ConcurrentIMP.LTL
21:45:11 NormByEval: theory NormByEval.NBE
21:45:11 Finished PLM/outline (0:00:19 elapsed time)
21:45:11 Timing PLM (4 threads, 24.278s elapsed time, 73.034s cpu time, 1.928s GC time, factor 3.01)
21:45:11 Finished PLM (0:00:26 elapsed time, 0:01:15 cpu time, factor 2.80)
21:45:11 Knuth_Morris_Pratt CANCELLED
21:45:11 Running FocusStreamsCaseStudies ...
21:45:11 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
21:45:11 Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
21:45:11 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
21:45:12 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
21:45:13 Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
21:45:13 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom
21:45:13 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Unsorted
21:45:13 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Laurent_Library
21:45:13 Finished PSemigroupsConvolution/document (0:00:05 elapsed time)
21:45:13 Preparing PSemigroupsConvolution/outline ...
21:45:13 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
21:45:13 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
21:45:13 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
21:45:13 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
21:45:13 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ArithExtras
21:45:14 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ListExtras
21:45:14 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.arith_hints
21:45:14 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.stream
21:45:15 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Polynomial
21:45:16 Preparing Fishburn_Impossibility/document ...
21:45:16 Finished Optics/outline (0:00:06 elapsed time)
21:45:16 Timing Optics (4 threads, 17.533s elapsed time, 45.948s cpu time, 0.824s GC time, factor 2.62)
21:45:16 Finished Optics (0:00:20 elapsed time, 0:00:48 cpu time, factor 2.42)
21:45:16 Running Cubic_Quartic_Equations ...
21:45:17 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.BitBoolTS
21:45:17 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_types
21:45:17 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_types
21:45:17 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.JoinSplitTime
21:45:18 Finished PSemigroupsConvolution/outline (0:00:04 elapsed time)
21:45:18 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler
21:45:18 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler_proof
21:45:18 Timing PSemigroupsConvolution (4 threads, 24.316s elapsed time, 59.323s cpu time, 1.896s GC time, factor 2.44)
21:45:18 Finished PSemigroupsConvolution (0:00:26 elapsed time, 0:01:01 cpu time, factor 2.31)
21:45:18 Running Finitely_Generated_Abelian_Groups ...
21:45:18 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR
21:45:18 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_proof
21:45:19 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
21:45:19 Shivers-CFA: theory Shivers-CFA.CPSUtils
21:45:19 Shivers-CFA: theory Shivers-CFA.Eval
21:45:19 Shivers-CFA: theory Shivers-CFA.AbsCF
21:45:19 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom_Poly
21:45:20 Timing HOL-SPARK-Examples (4 threads, 18.933s elapsed time, 36.362s cpu time, 0.795s GC time, factor 1.92)
21:45:20 Finished HOL-SPARK-Examples (0:00:34 elapsed time, 0:01:01 cpu time, factor 1.76)
21:45:20 Running Sliding_Window_Algorithm ...
21:45:20 Finished Fishburn_Impossibility/document (0:00:04 elapsed time)
21:45:20 Preparing Fishburn_Impossibility/outline ...
21:45:20 Shivers-CFA: theory Shivers-CFA.ExCF
21:45:20 Preparing Well_Quasi_Orders/document ...
21:45:21 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway
21:45:21 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof_aux
21:45:21 Sliding_Window_Algorithm: theory Sliding_Window_Algorithm.SWA
21:45:21 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Polynomial_Library
21:45:22 Shivers-CFA: theory Shivers-CFA.AbsCFComp
21:45:22 Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
21:45:23 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof
21:45:23 Shivers-CFA: theory Shivers-CFA.ExCFSV
21:45:23 Finished Fishburn_Impossibility/outline (0:00:03 elapsed time)
21:45:24 Timing Fishburn_Impossibility (4 threads, 21.397s elapsed time, 80.022s cpu time, 2.623s GC time, factor 3.74)
21:45:24 Finished Fishburn_Impossibility (0:00:23 elapsed time, 0:01:22 cpu time, factor 3.44)
21:45:24 Running AVL-Trees ...
21:45:24 Formal_Puiseux_Series: theory Formal_Puiseux_Series.FPS_Hensel
21:45:25 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Formal_Puiseux_Series
21:45:25 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
21:45:26 ConcurrentIMP: theory ConcurrentIMP.CIMP
21:45:26 AVL-Trees: theory AVL-Trees.AVL
21:45:26 AVL-Trees: theory AVL-Trees.AVL2
21:45:26 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
21:45:26 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
21:45:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
21:45:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
21:45:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
21:45:26 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom
21:45:26 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
21:45:27 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
21:45:28 Finished Well_Quasi_Orders/document (0:00:07 elapsed time)
21:45:28 Preparing Well_Quasi_Orders/outline ...
21:45:28 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
21:45:28 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds
21:45:28 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
21:45:28 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
21:45:28 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
21:45:29 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
21:45:30 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
21:45:30 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
21:45:30 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
21:45:30 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
21:45:31 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds
21:45:31 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations
21:45:33 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
21:45:33 Finished Well_Quasi_Orders/outline (0:00:05 elapsed time)
21:45:33 Timing Well_Quasi_Orders (4 threads, 21.881s elapsed time, 63.547s cpu time, 2.252s GC time, factor 2.90)
21:45:33 Finished Well_Quasi_Orders (0:00:26 elapsed time, 0:01:07 cpu time, factor 2.58)
21:45:33 Running GraphMarkingIBP ...
21:45:34 Preparing Formal_Puiseux_Series/document ...
21:45:35 GraphMarkingIBP: theory GraphMarkingIBP.Graph
21:45:35 GraphMarkingIBP: theory LatticeProperties.Conj_Disj
21:45:35 GraphMarkingIBP: theory LatticeProperties.WellFoundedTransitive
21:45:36 Preparing Shivers-CFA/document ...
21:45:36 GraphMarkingIBP: theory LatticeProperties.Complete_Lattice_Prop
21:45:36 Preparing ConcurrentIMP/document ...
21:45:36 GraphMarkingIBP: theory DataRefinementIBP.Preliminaries
21:45:37 GraphMarkingIBP: theory DataRefinementIBP.Statements
21:45:37 Preparing FocusStreamsCaseStudies/document ...
21:45:37 GraphMarkingIBP: theory DataRefinementIBP.Hoare
21:45:37 GraphMarkingIBP: theory DataRefinementIBP.Diagram
21:45:37 Preparing NormByEval/document ...
21:45:37 GraphMarkingIBP: theory DataRefinementIBP.DataRefinement
21:45:38 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
21:45:38 GraphMarkingIBP: theory GraphMarkingIBP.SetMark
21:45:39 GraphMarkingIBP: theory GraphMarkingIBP.StackMark
21:45:39 GraphMarkingIBP: theory GraphMarkingIBP.LinkMark
21:45:40 GraphMarkingIBP: theory GraphMarkingIBP.DSWMark
21:45:41 Finished Formal_Puiseux_Series/document (0:00:07 elapsed time)
21:45:41 Preparing Formal_Puiseux_Series/outline ...
21:45:42 Preparing Sliding_Window_Algorithm/document ...
21:45:42 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
21:45:42 Finished ConcurrentIMP/document (0:00:06 elapsed time)
21:45:42 Preparing ConcurrentIMP/outline ...
21:45:43 Finished NormByEval/document (0:00:05 elapsed time)
21:45:43 Preparing NormByEval/outline ...
21:45:43 Finished Shivers-CFA/document (0:00:07 elapsed time)
21:45:43 Preparing Shivers-CFA/outline ...
21:45:44 Preparing AVL-Trees/document ...
21:45:45 Preparing Finitely_Generated_Abelian_Groups/document ...
21:45:45 Finished Sliding_Window_Algorithm/document (0:00:03 elapsed time)
21:45:45 Preparing Sliding_Window_Algorithm/outline ...
21:45:46 Finished FocusStreamsCaseStudies/document (0:00:09 elapsed time)
21:45:46 Preparing FocusStreamsCaseStudies/outline ...
21:45:46 Finished Formal_Puiseux_Series/outline (0:00:04 elapsed time)
21:45:47 Finished AVL-Trees/document (0:00:02 elapsed time)
21:45:47 Finished NormByEval/outline (0:00:03 elapsed time)
21:45:47 Preparing AVL-Trees/outline ...
21:45:47 Timing NormByEval (4 threads, 25.227s elapsed time, 65.202s cpu time, 1.323s GC time, factor 2.58)
21:45:47 Finished NormByEval (0:00:27 elapsed time, 0:01:07 cpu time, factor 2.43)
21:45:47 Timing Formal_Puiseux_Series (4 threads, 19.312s elapsed time, 60.173s cpu time, 1.561s GC time, factor 3.12)
21:45:47 Finished Formal_Puiseux_Series (0:00:24 elapsed time, 0:01:04 cpu time, factor 2.68)
21:45:47 Running XML ...
21:45:47 Running Efficient-Mergesort ...
21:45:48 Finished ConcurrentIMP/outline (0:00:05 elapsed time)
21:45:48 Timing ConcurrentIMP (4 threads, 25.048s elapsed time, 79.096s cpu time, 3.486s GC time, factor 3.16)
21:45:48 Finished ConcurrentIMP (0:00:29 elapsed time, 0:01:22 cpu time, factor 2.85)
21:45:48 Running Decreasing-Diagrams-II ...
21:45:48 Efficient-Mergesort: theory HOL-Library.Cancellation
21:45:48 Finished AVL-Trees/outline (0:00:01 elapsed time)
21:45:49 Finished Sliding_Window_Algorithm/outline (0:00:03 elapsed time)
21:45:49 Timing Sliding_Window_Algorithm (4 threads, 19.335s elapsed time, 58.793s cpu time, 0.860s GC time, factor 3.04)
21:45:49 Finished Sliding_Window_Algorithm (0:00:21 elapsed time, 0:01:00 cpu time, factor 2.78)
21:45:49 Timing AVL-Trees (4 threads, 18.135s elapsed time, 71.326s cpu time, 1.544s GC time, factor 3.93)
21:45:49 Finished AVL-Trees (0:00:20 elapsed time, 0:01:13 cpu time, factor 3.55)
21:45:49 Running Polynomial_Interpolation ...
21:45:49 Running Finite_Automata_HF ...
21:45:49 Efficient-Mergesort: theory HOL-Library.Multiset
21:45:49 Finished Shivers-CFA/outline (0:00:05 elapsed time)
21:45:49 Timing Shivers-CFA (4 threads, 25.123s elapsed time, 78.762s cpu time, 3.284s GC time, factor 3.14)
21:45:49 Finished Shivers-CFA (0:00:27 elapsed time, 0:01:21 cpu time, factor 2.92)
21:45:49 Running CCS ...
21:45:49 Preparing Cubic_Quartic_Equations/document ...
21:45:50 XML: theory Deriving.Generator_Aux
21:45:50 XML: theory Certification_Monads.Error_Syntax
21:45:50 XML: theory Deriving.Derive_Manager
21:45:50 XML: theory Partial_Function_MR.Partial_Function_MR
21:45:50 XML: theory Certification_Monads.Error_Monad
21:45:50 XML: theory Certification_Monads.Strict_Sum
21:45:50 XML: theory Show.Show
21:45:50 Finite_Automata_HF: theory Regular-Sets.Regular_Set
21:45:51 Finite_Automata_HF: theory HOL-Library.Nat_Bijection
21:45:51 CCS: theory CCS.Agent
21:45:51 Finite_Automata_HF: theory HereditarilyFinite.HF
21:45:51 Decreasing-Diagrams-II: theory HOL-Cardinals.Order_Union
21:45:51 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Infinite_Sequences
21:45:51 Decreasing-Diagrams-II: theory Open_Induction.Restricted_Predicates
21:45:51 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Least_Enum
21:45:52 Preparing GraphMarkingIBP/document ...
21:45:52 Decreasing-Diagrams-II: theory HOL-Cardinals.Wellorder_Extension
21:45:53 Finished FocusStreamsCaseStudies/outline (0:00:06 elapsed time)
21:45:53 Finite_Automata_HF: theory HereditarilyFinite.Ordinal
21:45:53 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Unsorted
21:45:53 Polynomial_Interpolation: theory Polynomial_Interpolation.Improved_Code_Equations
21:45:53 Polynomial_Interpolation: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
21:45:53 Polynomial_Interpolation: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
21:45:53 Timing FocusStreamsCaseStudies (4 threads, 22.297s elapsed time, 63.394s cpu time, 1.813s GC time, factor 2.84)
21:45:53 Finished FocusStreamsCaseStudies (0:00:24 elapsed time, 0:01:05 cpu time, factor 2.64)
21:45:53 Running SenSocialChoice ...
21:45:53 XML: theory Certification_Monads.Parser_Monad
21:45:54 Polynomial_Interpolation: theory Polynomial_Interpolation.Divmod_Int
21:45:54 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom
21:45:54 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Multiset_Extension
21:45:54 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Elements
21:45:54 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full
21:45:54 Polynomial_Interpolation: theory Polynomial_Interpolation.Is_Rat_To_Rat
21:45:54 XML: theory XML.Xml
21:45:55 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Bad_Sequences
21:45:55 SenSocialChoice: theory SenSocialChoice.FSext
21:45:55 Finite_Automata_HF: theory Regular-Sets.Regular_Exp
21:45:56 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full_Relations
21:45:56 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Polynomial
21:45:56 SenSocialChoice: theory SenSocialChoice.RPRs
21:45:56 Efficient-Mergesort: theory Efficient-Mergesort.Efficient_Sort
21:45:57 Efficient-Mergesort: theory HOL-Data_Structures.Sorting
21:45:57 Finished GraphMarkingIBP/document (0:00:04 elapsed time)
21:45:57 Preparing GraphMarkingIBP/outline ...
21:45:57 SenSocialChoice: theory SenSocialChoice.SCFs
21:45:57 Decreasing-Diagrams-II: theory Well_Quasi_Orders.Well_Quasi_Orders
21:45:57 Finished Finitely_Generated_Abelian_Groups/document (0:00:12 elapsed time)
21:45:57 Preparing Finitely_Generated_Abelian_Groups/outline ...
21:45:57 CCS: theory CCS.Strong_Sim
21:45:57 CCS: theory CCS.Struct_Cong
21:45:57 CCS: theory CCS.Tau_Chain
21:45:57 Finished Cubic_Quartic_Equations/document (0:00:07 elapsed time)
21:45:57 Preparing Cubic_Quartic_Equations/outline ...
21:45:57 CCS: theory CCS.Strong_Bisim
21:45:57 CCS: theory CCS.Strong_Sim_Pres
21:45:58 SenSocialChoice: theory SenSocialChoice.Arrow
21:45:58 SenSocialChoice: theory SenSocialChoice.May
21:45:58 SenSocialChoice: theory SenSocialChoice.Sen
21:45:58 CCS: theory CCS.Strong_Sim_SC
21:45:58 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux
21:45:58 CCS: theory CCS.Weak_Cong_Semantics
21:45:58 CCS: theory CCS.Weak_Semantics
21:45:58 CCS: theory CCS.Strong_Bisim_Pres
21:45:59 XML: theory XML.Xmlt
21:45:59 CCS: theory CCS.Weak_Sim
21:45:59 CCS: theory CCS.Strong_Bisim_SC
21:45:59 Efficient-Mergesort: theory Efficient-Mergesort.Mergesort_Complexity
21:45:59 CCS: theory CCS.Weak_Cong_Sim
21:45:59 CCS: theory CCS.Weak_Cong_Sim_Pres
21:45:59 CCS: theory CCS.Weak_Sim_Pres
21:45:59 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II
21:46:00 Efficient-Mergesort: theory Efficient-Mergesort.Natural_Mergesort
21:46:00 Polynomial_Interpolation: theory Polynomial_Interpolation.Lagrange_Interpolation
21:46:00 Finite_Automata_HF: theory Finite_Automata_HF.Finite_Automata_HF
21:46:00 CCS: theory CCS.Weak_Bisim
21:46:01 CCS: theory CCS.Weak_Cong
21:46:01 CCS: theory CCS.Weak_Bisim_Pres
21:46:01 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom_Poly
21:46:01 CCS: theory CCS.Weak_Cong_Pres
21:46:01 Finished GraphMarkingIBP/outline (0:00:04 elapsed time)
21:46:02 Timing GraphMarkingIBP (4 threads, 15.488s elapsed time, 47.190s cpu time, 0.700s GC time, factor 3.05)
21:46:02 Finished GraphMarkingIBP (0:00:18 elapsed time, 0:00:49 cpu time, factor 2.71)
21:46:02 Running Fermat3_4 ...
21:46:03 Finished Cubic_Quartic_Equations/outline (0:00:05 elapsed time)
21:46:03 Polynomial_Interpolation: theory Polynomial_Interpolation.Newton_Interpolation
21:46:03 Finished Finitely_Generated_Abelian_Groups/outline (0:00:06 elapsed time)
21:46:03 Timing Cubic_Quartic_Equations (4 threads, 20.383s elapsed time, 51.690s cpu time, 1.967s GC time, factor 2.54)
21:46:03 Finished Cubic_Quartic_Equations (0:00:33 elapsed time, 0:01:04 cpu time, factor 1.93)
21:46:03 Timing Finitely_Generated_Abelian_Groups (4 threads, 17.530s elapsed time, 55.485s cpu time, 2.912s GC time, factor 3.17)
21:46:03 Finished Finitely_Generated_Abelian_Groups (0:00:26 elapsed time, 0:01:03 cpu time, factor 2.44)
21:46:03 Running Derangements ...
21:46:03 Running Name_Carrying_Type_Inference ...
21:46:05 Derangements: theory HOL-Combinatorics.Transposition
21:46:05 Derangements: theory HOL-Library.FuncSet
21:46:05 Derangements: theory HOL-Library.Cancellation
21:46:05 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.Fresh
21:46:05 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.Permutation
21:46:07 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.PreSimplyTyped
21:46:07 Derangements: theory HOL-Library.Multiset
21:46:07 Derangements: theory HOL-Library.Disjoint_Sets
21:46:07 Polynomial_Interpolation: theory Polynomial_Interpolation.Polynomial_Interpolation
21:46:07 Fermat3_4: theory Fermat3_4.Quad_Form
21:46:07 Fermat3_4: theory Fermat3_4.Fermat4
21:46:08 Preparing Decreasing-Diagrams-II/document ...
21:46:09 Preparing CCS/document ...
21:46:09 Fermat3_4: theory Fermat3_4.Fermat3
21:46:09 Preparing Finite_Automata_HF/document ...
21:46:11 Preparing Efficient-Mergesort/document ...
21:46:11 Name_Carrying_Type_Inference: theory Name_Carrying_Type_Inference.SimplyTyped
21:46:11 Finished Finite_Automata_HF/document (0:00:02 elapsed time)
21:46:11 Preparing Finite_Automata_HF/outline ...
21:46:12 Preparing Polynomial_Interpolation/document ...
21:46:13 Derangements: theory HOL-Combinatorics.Permutations
21:46:13 Finished Decreasing-Diagrams-II/document (0:00:04 elapsed time)
21:46:13 Preparing Decreasing-Diagrams-II/outline ...
21:46:14 Preparing XML/document ...
21:46:14 Preparing SenSocialChoice/document ...
21:46:14 Finished Finite_Automata_HF/outline (0:00:02 elapsed time)
21:46:14 Timing Finite_Automata_HF (4 threads, 17.363s elapsed time, 50.789s cpu time, 1.438s GC time, factor 2.93)
21:46:14 Finished Finite_Automata_HF (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.67)
21:46:14 Running FLP ...
21:46:14 Finished Efficient-Mergesort/document (0:00:03 elapsed time)
21:46:14 Preparing Efficient-Mergesort/outline ...
21:46:14 Derangements: theory Derangements.Derangements
21:46:15 Finished CCS/document (0:00:06 elapsed time)
21:46:15 Preparing CCS/outline ...
21:46:16 FLP: theory FLP.Multiset
21:46:16 FLP: theory FLP.ListUtilities
21:46:16 FLP: theory FLP.AsynchronousSystem
21:46:16 Finished XML/document (0:00:02 elapsed time)
21:46:16 Preparing XML/outline ...
21:46:16 Finished Decreasing-Diagrams-II/outline (0:00:03 elapsed time)
21:46:17 Timing Decreasing-Diagrams-II (4 threads, 15.601s elapsed time, 58.585s cpu time, 1.524s GC time, factor 3.76)
21:46:17 Finished Decreasing-Diagrams-II (0:00:19 elapsed time, 0:01:02 cpu time, factor 3.17)
21:46:17 Running List_Inversions ...
21:46:17 Finished Efficient-Mergesort/outline (0:00:03 elapsed time)
21:46:17 Timing Efficient-Mergesort (4 threads, 20.811s elapsed time, 62.528s cpu time, 2.161s GC time, factor 3.00)
21:46:17 Finished Efficient-Mergesort (0:00:23 elapsed time, 0:01:04 cpu time, factor 2.78)
21:46:17 Running Jordan_Hoelder ...
21:46:19 Finished XML/outline (0:00:02 elapsed time)
21:46:19 List_Inversions: theory HOL-Combinatorics.Transposition
21:46:19 List_Inversions: theory HOL-Library.Cancellation
21:46:19 List_Inversions: theory HOL-Library.FuncSet
21:46:19 Preparing Fermat3_4/document ...
21:46:19 Timing XML (4 threads, 22.607s elapsed time, 43.958s cpu time, 2.486s GC time, factor 1.94)
21:46:19 Finished XML (0:00:26 elapsed time, 0:00:47 cpu time, factor 1.79)
21:46:19 Running CISC-Kernel ...
21:46:19 FLP: theory FLP.Execution
21:46:19 FLP: theory FLP.FLPSystem
21:46:19 Finished CCS/outline (0:00:04 elapsed time)
21:46:20 Finished SenSocialChoice/document (0:00:06 elapsed time)
21:46:20 Preparing SenSocialChoice/outline ...
21:46:20 List_Inversions: theory HOL-Library.Multiset
21:46:20 Timing CCS (4 threads, 16.680s elapsed time, 53.022s cpu time, 1.037s GC time, factor 3.18)
21:46:20 Finished CCS (0:00:19 elapsed time, 0:00:55 cpu time, factor 2.88)
21:46:20 Running FOL_Harrison ...
21:46:20 List_Inversions: theory HOL-Library.Disjoint_Sets
21:46:20 FLP: theory FLP.FLPTheorem
21:46:20 Finished Polynomial_Interpolation/document (0:00:08 elapsed time)
21:46:20 Preparing Polynomial_Interpolation/outline ...
21:46:21 CISC-Kernel: theory CISC-Kernel.List_Theorems
21:46:21 CISC-Kernel: theory CISC-Kernel.Option_Binders
21:46:21 CISC-Kernel: theory CISC-Kernel.Step_configuration
21:46:21 CISC-Kernel: theory CISC-Kernel.K
21:46:21 Preparing Derangements/document ...
21:46:22 FLP: theory FLP.FLPExistingSystem
21:46:22 CISC-Kernel: theory CISC-Kernel.SK
21:46:22 CISC-Kernel: theory CISC-Kernel.Step_policies
21:46:22 Preparing Name_Carrying_Type_Inference/document ...
21:46:22 FOL_Harrison: theory FOL_Harrison.FOL_Harrison
21:46:22 CISC-Kernel: theory CISC-Kernel.Step
21:46:23 CISC-Kernel: theory CISC-Kernel.ISK
21:46:24 CISC-Kernel: theory CISC-Kernel.CISK
21:46:24 Finished SenSocialChoice/outline (0:00:04 elapsed time)
21:46:25 Timing SenSocialChoice (4 threads, 17.494s elapsed time, 53.643s cpu time, 0.564s GC time, factor 3.07)
21:46:25 Finished SenSocialChoice (0:00:20 elapsed time, 0:00:56 cpu time, factor 2.77)
21:46:25 Running Octonions ...
21:46:25 Finished Derangements/document (0:00:03 elapsed time)
21:46:25 Preparing Derangements/outline ...
21:46:26 Jordan_Hoelder: theory Secondary_Sylow.GroupAction
21:46:26 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
21:46:26 List_Inversions: theory HOL-Combinatorics.Permutations
21:46:26 CISC-Kernel: theory CISC-Kernel.Step_invariants
21:46:26 Finished Fermat3_4/document (0:00:06 elapsed time)
21:46:26 Preparing Fermat3_4/outline ...
21:46:26 CISC-Kernel: theory CISC-Kernel.Step_vpeq
21:46:26 CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects
21:46:26 CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent
21:46:26 Finished Polynomial_Interpolation/outline (0:00:05 elapsed time)
21:46:26 Timing Polynomial_Interpolation (4 threads, 17.997s elapsed time, 65.990s cpu time, 2.120s GC time, factor 3.67)
21:46:26 Finished Polynomial_Interpolation (0:00:22 elapsed time, 0:01:10 cpu time, factor 3.09)
21:46:26 Running Sturm_Tarski ...
21:46:26 CISC-Kernel: theory CISC-Kernel.Separation_kernel_model
21:46:27 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
21:46:27 List_Inversions: theory List_Inversions.List_Inversions
21:46:27 Jordan_Hoelder: theory Secondary_Sylow.SndSylow
21:46:27 Finished Name_Carrying_Type_Inference/document (0:00:05 elapsed time)
21:46:27 Preparing Name_Carrying_Type_Inference/outline ...
21:46:27 CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK
21:46:27 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp
21:46:28 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups
21:46:28 Finished Derangements/outline (0:00:03 elapsed time)
21:46:28 Timing Derangements (4 threads, 14.295s elapsed time, 54.334s cpu time, 1.540s GC time, factor 3.80)
21:46:28 Finished Derangements (0:00:16 elapsed time, 0:00:56 cpu time, factor 3.34)
21:46:28 Running TLA ...
21:46:29 Octonions: theory Octonions.Cross_Product_7
21:46:29 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups
21:46:29 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
21:46:29 Finished Fermat3_4/outline (0:00:03 elapsed time)
21:46:30 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
21:46:30 Timing Fermat3_4 (4 threads, 10.518s elapsed time, 40.910s cpu time, 0.870s GC time, factor 3.89)
21:46:30 Finished Fermat3_4 (0:00:16 elapsed time, 0:00:46 cpu time, factor 2.80)
21:46:30 Running Complete_Non_Orders ...
21:46:30 Sturm_Tarski: theory Sturm_Tarski.PolyMisc
21:46:30 TLA: theory TLA.Intensional
21:46:30 TLA: theory TLA.Sequence
21:46:30 Finished Name_Carrying_Type_Inference/outline (0:00:03 elapsed time)
21:46:30 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
21:46:30 Sturm_Tarski: theory Sturm_Tarski.Sturm_Tarski
21:46:31 Timing Name_Carrying_Type_Inference (4 threads, 15.311s elapsed time, 52.211s cpu time, 1.815s GC time, factor 3.41)
21:46:31 Finished Name_Carrying_Type_Inference (0:00:17 elapsed time, 0:00:54 cpu time, factor 3.05)
21:46:31 Running Transitive-Closure-II ...
21:46:32 Complete_Non_Orders: theory Complete_Non_Orders.Binary_Relations
21:46:33 Octonions: theory Octonions.Octonions
21:46:33 Transitive-Closure-II: theory Regular-Sets.Regular_Set
21:46:33 Transitive-Closure-II: theory HOL-Library.While_Combinator
21:46:34 TLA: theory TLA.Semantics
21:46:35 Preparing FLP/document ...
21:46:35 Preparing List_Inversions/document ...
21:46:35 TLA: theory TLA.PreFormulas
21:46:36 TLA: theory TLA.Rules
21:46:37 TLA: theory TLA.Liveness
21:46:38 Preparing CISC-Kernel/document ...
21:46:38 TLA: theory TLA.State
21:46:38 TLA: theory TLA.Buffer
21:46:38 TLA: theory TLA.Even
21:46:38 TLA: theory TLA.Inc
21:46:39 Transitive-Closure-II: theory Regular-Sets.Regular_Exp
21:46:39 Finished List_Inversions/document (0:00:03 elapsed time)
21:46:39 Preparing List_Inversions/outline ...
21:46:41 Preparing Jordan_Hoelder/document ...
21:46:41 Finished FLP/document (0:00:06 elapsed time)
21:46:41 Preparing FLP/outline ...
21:46:42 Finished List_Inversions/outline (0:00:02 elapsed time)
21:46:42 Timing List_Inversions (4 threads, 14.789s elapsed time, 55.239s cpu time, 1.897s GC time, factor 3.74)
21:46:42 Finished List_Inversions (0:00:17 elapsed time, 0:00:57 cpu time, factor 3.31)
21:46:42 Running Neumann_Morgenstern_Utility ...
21:46:42 Transitive-Closure-II: theory Regular-Sets.NDerivative
21:46:42 Transitive-Closure-II: theory Regular-Sets.Relation_Interpretation
21:46:43 Preparing FOL_Harrison/document ...
21:46:44 Preparing TLA/document ...
21:46:45 Finished FLP/outline (0:00:03 elapsed time)
21:46:45 Timing FLP (4 threads, 17.678s elapsed time, 49.626s cpu time, 1.733s GC time, factor 2.81)
21:46:45 Finished FLP (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.57)
21:46:45 Running IMAP-CRDT ...
21:46:45 Complete_Non_Orders: theory Complete_Non_Orders.Complete_Relations
21:46:45 Finished FOL_Harrison/document (0:00:02 elapsed time)
21:46:45 Preparing FOL_Harrison/outline ...
21:46:46 Preparing Octonions/document ...
21:46:46 Complete_Non_Orders: theory Complete_Non_Orders.Fixed_Points
21:46:46 Complete_Non_Orders: theory Complete_Non_Orders.Kleene_Fixed_Point
21:46:46 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
21:46:46 Transitive-Closure-II: theory Regular-Sets.Equivalence_Checking
21:46:46 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
21:46:46 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
21:46:47 Transitive-Closure-II: theory Regular-Sets.Regexp_Method
21:46:47 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
21:46:47 IMAP-CRDT: theory IMAP-CRDT.IMAP-def
21:46:47 Finished Jordan_Hoelder/document (0:00:06 elapsed time)
21:46:47 Preparing Jordan_Hoelder/outline ...
21:46:48 Finished FOL_Harrison/outline (0:00:02 elapsed time)
21:46:48 Transitive-Closure-II: theory Transitive-Closure-II.RTrancl
21:46:48 Timing FOL_Harrison (4 threads, 19.573s elapsed time, 47.044s cpu time, 0.731s GC time, factor 2.40)
21:46:48 Finished FOL_Harrison (0:00:22 elapsed time, 0:00:49 cpu time, factor 2.22)
21:46:48 Finished CISC-Kernel/document (0:00:09 elapsed time)
21:46:48 Running InformationFlowSlicing_Inter ...
21:46:48 Preparing CISC-Kernel/outline ...
21:46:48 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
21:46:48 Preparing Sturm_Tarski/document ...
21:46:48 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
21:46:49 Preparing Transitive-Closure-II/document ...
21:46:50 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-commute
21:46:50 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-helpers
21:46:50 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
21:46:50 Finished Octonions/document (0:00:04 elapsed time)
21:46:50 Preparing Octonions/outline ...
21:46:51 Preparing Complete_Non_Orders/document ...
21:46:51 Finished Jordan_Hoelder/outline (0:00:03 elapsed time)
21:46:51 Timing Jordan_Hoelder (4 threads, 14.200s elapsed time, 49.490s cpu time, 1.698s GC time, factor 3.49)
21:46:51 Finished Jordan_Hoelder (0:00:23 elapsed time, 0:00:58 cpu time, factor 2.52)
21:46:51 Running OpSets ...
21:46:52 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
21:46:52 Finished Transitive-Closure-II/document (0:00:03 elapsed time)
21:46:52 Preparing Transitive-Closure-II/outline ...
21:46:53 Finished TLA/document (0:00:08 elapsed time)
21:46:53 Preparing TLA/outline ...
21:46:53 Finished Sturm_Tarski/document (0:00:04 elapsed time)
21:46:53 Preparing Sturm_Tarski/outline ...
21:46:53 OpSets: theory OpSets.OpSet
21:46:53 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-independent
21:46:54 OpSets: theory OpSets.Insert_Spec
21:46:54 Finished CISC-Kernel/outline (0:00:06 elapsed time)
21:46:54 Timing CISC-Kernel (4 threads, 15.735s elapsed time, 51.463s cpu time, 1.958s GC time, factor 3.27)
21:46:54 Finished CISC-Kernel (0:00:18 elapsed time, 0:00:53 cpu time, factor 2.93)
21:46:54 Building Random_BSTs ...
21:46:55 Finished Octonions/outline (0:00:04 elapsed time)
21:46:55 OpSets: theory OpSets.Interleaving
21:46:55 OpSets: theory OpSets.List_Spec
21:46:55 OpSets: theory OpSets.RGA
21:46:55 Timing Octonions (4 threads, 16.062s elapsed time, 56.884s cpu time, 1.448s GC time, factor 3.54)
21:46:55 Finished Octonions (0:00:20 elapsed time, 0:01:00 cpu time, factor 2.94)
21:46:55 Running BNF_CC ...
21:46:56 Finished Transitive-Closure-II/outline (0:00:03 elapsed time)
21:46:56 Timing Transitive-Closure-II (4 threads, 15.709s elapsed time, 28.698s cpu time, 0.950s GC time, factor 1.83)
21:46:56 Finished Transitive-Closure-II (0:00:18 elapsed time, 0:00:31 cpu time, factor 1.69)
21:46:56 Running Cayley_Hamilton ...
21:46:56 IMAP-CRDT: theory IMAP-CRDT.IMAP-proof
21:46:56 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
21:46:56 Finished Sturm_Tarski/outline (0:00:03 elapsed time)
21:46:57 Timing Sturm_Tarski (4 threads, 16.588s elapsed time, 42.373s cpu time, 0.678s GC time, factor 2.55)
21:46:57 Finished Sturm_Tarski (0:00:21 elapsed time, 0:00:46 cpu time, factor 2.19)
21:46:57 Running IMP2_Binary_Heap ...
21:46:57 BNF_CC: theory BNF_CC.Preliminaries
21:46:57 BNF_CC: theory HOL-Library.Old_Datatype
21:46:57 BNF_CC: theory HOL-Library.Nat_Bijection
21:46:57 BNF_CC: theory HOL-Library.BNF_Axiomatization
21:46:57 BNF_CC: theory HOL-Library.Phantom_Type
21:46:58 BNF_CC: theory HOL-Library.Rewrite
21:46:58 Preparing Neumann_Morgenstern_Utility/document ...
21:46:58 BNF_CC: theory BNF_CC.Axiomatised_BNF_CC
21:46:59 BNF_CC: theory HOL-Library.Countable
21:46:59 Random_BSTs: theory HOL-Data_Structures.Cmp
21:46:59 Random_BSTs: theory HOL-Data_Structures.Less_False
21:46:59 Finished Complete_Non_Orders/document (0:00:08 elapsed time)
21:46:59 Preparing Complete_Non_Orders/outline ...
21:46:59 BNF_CC: theory HOL-Library.Cardinality
21:46:59 IMP2_Binary_Heap: theory IMP2_Binary_Heap.IMP2_Binary_Heap
21:46:59 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
21:46:59 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
21:46:59 Finished TLA/outline (0:00:06 elapsed time)
21:46:59 Timing TLA (4 threads, 13.178s elapsed time, 45.890s cpu time, 1.387s GC time, factor 3.48)
21:46:59 Finished TLA (0:00:15 elapsed time, 0:00:48 cpu time, factor 3.04)
21:46:59 Running Pell ...
21:46:59 Cayley_Hamilton: theory HOL-Library.More_List
21:46:59 Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
21:47:00 Random_BSTs: theory HOL-Data_Structures.Set_Specs
21:47:00 Random_BSTs: theory HOL-Data_Structures.Tree_Set
21:47:00 Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
21:47:01 BNF_CC: theory BNF_CC.Concrete_Examples
21:47:01 BNF_CC: theory HOL-Library.FSet
21:47:02 Random_BSTs: theory Random_BSTs.Random_BSTs
21:47:03 BNF_CC: theory BNF_CC.Composition
21:47:03 BNF_CC: theory BNF_CC.Fixpoints
21:47:04 Pell: theory Pell.Efficient_Discrete_Sqrt
21:47:04 Pell: theory Pell.Pell
21:47:04 BNF_CC: theory BNF_CC.Quotient_Preservation
21:47:04 BNF_CC: theory BNF_CC.Subtypes
21:47:05 Finished Neumann_Morgenstern_Utility/document (0:00:06 elapsed time)
21:47:05 Preparing Neumann_Morgenstern_Utility/outline ...
21:47:06 Finished Complete_Non_Orders/outline (0:00:07 elapsed time)
21:47:06 Timing Complete_Non_Orders (4 threads, 17.929s elapsed time, 34.150s cpu time, 1.020s GC time, factor 1.90)
21:47:06 Finished Complete_Non_Orders (0:00:20 elapsed time, 0:00:36 cpu time, factor 1.77)
21:47:06 Running POPLmark-deBruijn ...
21:47:07 Preparing IMAP-CRDT/document ...
21:47:07 Pell: theory Pell.Pell_Algorithm
21:47:09 Pell: theory Pell.Pell_Algorithm_Test
21:47:09 Preparing InformationFlowSlicing_Inter/document ...
21:47:10 BNF_CC: theory BNF_CC.Operation_Examples
21:47:10 Finished Neumann_Morgenstern_Utility/outline (0:00:04 elapsed time)
21:47:10 Timing Neumann_Morgenstern_Utility (4 threads, 11.217s elapsed time, 38.479s cpu time, 0.825s GC time, factor 3.43)
21:47:10 Finished Neumann_Morgenstern_Utility (0:00:15 elapsed time, 0:00:42 cpu time, factor 2.70)
21:47:10 Running Posix-Lexing ...
21:47:10 POPLmark-deBruijn: theory POPLmark-deBruijn.Basis
21:47:10 BNF_CC: theory BNF_CC.DDS
21:47:10 Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
21:47:10 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmark
21:47:10 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmarkRecord
21:47:11 Finished IMAP-CRDT/document (0:00:04 elapsed time)
21:47:11 Preparing IMAP-CRDT/outline ...
21:47:12 Preparing OpSets/document ...
21:47:13 Posix-Lexing: theory Posix-Lexing.Lexer
21:47:15 Finished IMAP-CRDT/outline (0:00:03 elapsed time)
21:47:15 Preparing Cayley_Hamilton/document ...
21:47:15 Timing IMAP-CRDT (4 threads, 18.814s elapsed time, 48.302s cpu time, 2.081s GC time, factor 2.57)
21:47:15 Finished IMAP-CRDT (0:00:21 elapsed time, 0:00:50 cpu time, factor 2.37)
21:47:15 Running Stream_Fusion_Code ...
21:47:15 Preparing BNF_CC/document ...
21:47:17 Preparing IMP2_Binary_Heap/document ...
21:47:17 Finished InformationFlowSlicing_Inter/document (0:00:07 elapsed time)
21:47:17 Preparing InformationFlowSlicing_Inter/outline ...
21:47:18 POPLmark-deBruijn: theory POPLmark-deBruijn.Execute
21:47:18 POPLmark-deBruijn: theory POPLmark-deBruijn.POPLmarkRecordCtxt
21:47:19 Finished Cayley_Hamilton/document (0:00:03 elapsed time)
21:47:19 Preparing Cayley_Hamilton/outline ...
21:47:19 Preparing Pell/document ...
21:47:19 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion
21:47:19 Finished OpSets/document (0:00:07 elapsed time)
21:47:19 Preparing OpSets/outline ...
21:47:19 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List
21:47:20 Finished IMP2_Binary_Heap/document (0:00:03 elapsed time)
21:47:20 Preparing IMP2_Binary_Heap/outline ...
21:47:21 Finished InformationFlowSlicing_Inter/outline (0:00:03 elapsed time)
21:47:21 Posix-Lexing: theory Posix-Lexing.Simplifying
21:47:21 Timing InformationFlowSlicing_Inter (4 threads, 15.971s elapsed time, 52.784s cpu time, 2.607s GC time, factor 3.30)
21:47:21 Finished InformationFlowSlicing_Inter (0:00:20 elapsed time, 0:00:57 cpu time, factor 2.75)
21:47:21 Running Minsky_Machines ...
21:47:22 Finished Cayley_Hamilton/outline (0:00:03 elapsed time)
21:47:22 Timing Cayley_Hamilton (4 threads, 14.041s elapsed time, 49.254s cpu time, 1.602s GC time, factor 3.51)
21:47:22 Finished Cayley_Hamilton (0:00:18 elapsed time, 0:00:53 cpu time, factor 2.91)
21:47:22 Running Binomial-Heaps ...
21:47:23 Finished Pell/document (0:00:04 elapsed time)
21:47:23 Preparing Pell/outline ...
21:47:24 Finished IMP2_Binary_Heap/outline (0:00:03 elapsed time)
21:47:24 Finished OpSets/outline (0:00:04 elapsed time)
21:47:24 Finished BNF_CC/document (0:00:08 elapsed time)
21:47:24 Preparing BNF_CC/outline ...
21:47:24 Timing IMP2_Binary_Heap (4 threads, 17.073s elapsed time, 46.455s cpu time, 0.643s GC time, factor 2.72)
21:47:24 Finished IMP2_Binary_Heap (0:00:19 elapsed time, 0:00:48 cpu time, factor 2.48)
21:47:24 Timing OpSets (4 threads, 17.674s elapsed time, 59.240s cpu time, 1.294s GC time, factor 3.35)
21:47:24 Finished OpSets (0:00:20 elapsed time, 0:01:01 cpu time, factor 3.05)
21:47:24 Running Finger-Trees ...
21:47:24 Running Functional-Automata ...
21:47:24 Minsky_Machines: theory Pure-ex.Guess
21:47:24 Minsky_Machines: theory Recursion-Theory-I.CPair
21:47:25 Minsky_Machines: theory Recursion-Theory-I.PRecFun
21:47:25 Preparing POPLmark-deBruijn/document ...
21:47:25 Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap
21:47:25 Binomial-Heaps: theory Binomial-Heaps.BinomialHeap
21:47:27 Minsky_Machines: theory Recursion-Theory-I.PRecFinSet
21:47:27 Minsky_Machines: theory Recursion-Theory-I.PRecFun2
21:47:27 Minsky_Machines: theory Recursion-Theory-I.PRecList
21:47:27 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList
21:47:27 Finished Pell/outline (0:00:03 elapsed time)
21:47:27 Finger-Trees: theory Finger-Trees.FingerTree
21:47:27 Functional-Automata: theory Functional-Automata.AutoProj
21:47:27 Functional-Automata: theory Functional-Automata.MaxPrefix
21:47:27 Functional-Automata: theory Regular-Sets.Regular_Set
21:47:27 Functional-Automata: theory Functional-Automata.DA
21:47:27 Functional-Automata: theory Functional-Automata.NA
21:47:27 Timing Pell (4 threads, 13.877s elapsed time, 48.370s cpu time, 0.627s GC time, factor 3.49)
21:47:27 Finished Pell (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.80)
21:47:27 Floyd_Warshall CANCELLED
21:47:27 Running Median_Of_Medians_Selection ...
21:47:28 Functional-Automata: theory Functional-Automata.NAe
21:47:28 Functional-Automata: theory Functional-Automata.Automata
21:47:28 Functional-Automata: theory Functional-Automata.MaxChop
21:47:28 Functional-Automata: theory Functional-Automata.AutoMaxChop
21:47:29 Preparing Posix-Lexing/document ...
21:47:29 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples
21:47:30 Preparing Random_BSTs/document ...
21:47:30 Median_Of_Medians_Selection: theory HOL-Library.Cancellation
21:47:30 Minsky_Machines: theory Recursion-Theory-I.PRecUnGr
21:47:31 Median_Of_Medians_Selection: theory HOL-Library.Multiset
21:47:32 Finished BNF_CC/outline (0:00:08 elapsed time)
21:47:32 Timing BNF_CC (4 threads, 16.757s elapsed time, 53.586s cpu time, 3.167s GC time, factor 3.20)
21:47:32 Finished BNF_CC (0:00:19 elapsed time, 0:00:55 cpu time, factor 2.90)
21:47:32 Running KD_Tree ...
21:47:32 Functional-Automata: theory Functional-Automata.RegSet_of_nat_DA
21:47:32 Functional-Automata: theory Regular-Sets.Regular_Exp
21:47:33 Minsky_Machines: theory Recursion-Theory-I.RecEnSet
21:47:34 Finished Posix-Lexing/document (0:00:04 elapsed time)
21:47:34 Preparing Posix-Lexing/outline ...
21:47:34 Finished POPLmark-deBruijn/document (0:00:08 elapsed time)
21:47:34 Preparing POPLmark-deBruijn/outline ...
21:47:34 Finished Random_BSTs/document (0:00:04 elapsed time)
21:47:34 Preparing Random_BSTs/outline ...
21:47:35 Minsky_Machines: theory Minsky_Machines.Recursive_Inseparability
21:47:35 Minsky_Machines: theory Minsky_Machines.Minsky
21:47:35 Preparing Stream_Fusion_Code/document ...
21:47:36 KD_Tree: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
21:47:36 KD_Tree: theory KD_Tree.KD_Tree
21:47:36 Functional-Automata: theory Functional-Automata.RegExp2NA
21:47:36 Functional-Automata: theory Functional-Automata.RegExp2NAe
21:47:37 Finished Posix-Lexing/outline (0:00:03 elapsed time)
21:47:38 Timing Posix-Lexing (4 threads, 15.074s elapsed time, 32.826s cpu time, 1.186s GC time, factor 2.18)
21:47:38 Finished Posix-Lexing (0:00:19 elapsed time, 0:00:36 cpu time, factor 1.90)
21:47:38 Running Ribbon_Proofs ...
21:47:38 Finished Random_BSTs/outline (0:00:03 elapsed time)
21:47:38 Timing Random_BSTs (4 threads, 8.309s elapsed time, 16.785s cpu time, 0.323s GC time, factor 2.02)
21:47:38 Finished Random_BSTs (0:00:35 elapsed time, 0:00:57 cpu time, factor 1.65)
21:47:38 Running AxiomaticCategoryTheory ...
21:47:38 KD_Tree: theory KD_Tree.Nearest_Neighbors
21:47:38 KD_Tree: theory KD_Tree.Range_Search
21:47:38 KD_Tree: theory KD_Tree.Build
21:47:39 Functional-Automata: theory Functional-Automata.AutoRegExp
21:47:40 Functional-Automata: theory Functional-Automata.Execute
21:47:40 Functional-Automata: theory Functional-Automata.Functional_Automata
21:47:40 Finished POPLmark-deBruijn/outline (0:00:05 elapsed time)
21:47:40 Median_Of_Medians_Selection: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
21:47:40 Binomial-Heaps: theory Binomial-Heaps.Test
21:47:40 Timing POPLmark-deBruijn (4 threads, 14.351s elapsed time, 50.354s cpu time, 2.071s GC time, factor 3.51)
21:47:40 Finished POPLmark-deBruijn (0:00:18 elapsed time, 0:00:54 cpu time, factor 2.92)
21:47:40 Running Lambda_Free_RPOs ...
21:47:40 AxiomaticCategoryTheory: theory AxiomaticCategoryTheory.AxiomaticCategoryTheory
21:47:41 Ribbon_Proofs: theory Ribbon_Proofs.JHelper
21:47:41 Ribbon_Proofs: theory Ribbon_Proofs.More_Finite_Map
21:47:41 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Basic
21:47:41 Ribbon_Proofs: theory Ribbon_Proofs.Proofchain
21:47:42 Preparing Minsky_Machines/document ...
21:47:42 Finger-Trees: theory Finger-Trees.Test
21:47:43 Finished Stream_Fusion_Code/document (0:00:08 elapsed time)
21:47:43 Preparing Stream_Fusion_Code/outline ...
21:47:44 Preparing Binomial-Heaps/document ...
21:47:44 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Interfaces
21:47:44 Preparing Functional-Automata/document ...
21:47:44 Lambda_Free_RPOs: theory Nested_Multisets_Ordinals.Multiset_More
21:47:44 Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
21:47:44 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
21:47:44 Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
21:47:45 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
21:47:45 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
21:47:45 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
21:47:45 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical
21:47:45 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Stratified
21:47:46 Finished Minsky_Machines/document (0:00:04 elapsed time)
21:47:46 Preparing Minsky_Machines/outline ...
21:47:46 Preparing Finger-Trees/document ...
21:47:47 Preparing Median_Of_Medians_Selection/document ...
21:47:48 Finished Functional-Automata/document (0:00:04 elapsed time)
21:47:48 Preparing Functional-Automata/outline ...
21:47:49 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
21:47:49 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
21:47:49 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
21:47:49 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical_Soundness
21:47:50 Finished Stream_Fusion_Code/outline (0:00:06 elapsed time)
21:47:50 Preparing KD_Tree/document ...
21:47:50 Timing Stream_Fusion_Code (4 threads, 14.287s elapsed time, 49.434s cpu time, 1.401s GC time, factor 3.46)
21:47:50 Finished Stream_Fusion_Code (0:00:19 elapsed time, 0:00:54 cpu time, factor 2.79)
21:47:50 Running Real_Power ...
21:47:50 Finished Minsky_Machines/outline (0:00:03 elapsed time)
21:47:50 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
21:47:50 Timing Minsky_Machines (4 threads, 15.382s elapsed time, 52.557s cpu time, 2.168s GC time, factor 3.42)
21:47:50 Finished Minsky_Machines (0:00:19 elapsed time, 0:00:56 cpu time, factor 2.87)
21:47:50 Building Bell_Numbers_Spivey ...
21:47:51 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
21:47:51 Finished Binomial-Heaps/document (0:00:06 elapsed time)
21:47:51 Preparing Binomial-Heaps/outline ...
21:47:51 Finished Median_Of_Medians_Selection/document (0:00:04 elapsed time)
21:47:51 Preparing Median_Of_Medians_Selection/outline ...
21:47:52 Real_Power: theory Real_Power.RatPower
21:47:52 Finished Functional-Automata/outline (0:00:03 elapsed time)
21:47:52 Real_Power: theory Real_Power.RealPower
21:47:52 Timing Functional-Automata (4 threads, 15.387s elapsed time, 33.351s cpu time, 0.921s GC time, factor 2.17)
21:47:52 Finished Functional-Automata (0:00:19 elapsed time, 0:00:37 cpu time, factor 1.90)
21:47:52 Running Decreasing-Diagrams ...
21:47:52 Finished Finger-Trees/document (0:00:05 elapsed time)
21:47:52 Preparing Finger-Trees/outline ...
21:47:53 Real_Power: theory Real_Power.Log
21:47:54 Bell_Numbers_Spivey: theory HOL-Eisbach.Eisbach
21:47:54 Bell_Numbers_Spivey: theory HOL-Combinatorics.Stirling
21:47:54 Bell_Numbers_Spivey: theory Card_Partitions.Set_Partition
21:47:54 Finished Median_Of_Medians_Selection/outline (0:00:03 elapsed time)
21:47:54 Timing Median_Of_Medians_Selection (4 threads, 15.147s elapsed time, 41.518s cpu time, 1.155s GC time, factor 2.74)
21:47:54 Finished Median_Of_Medians_Selection (0:00:18 elapsed time, 0:00:44 cpu time, factor 2.43)
21:47:54 Running Boolean_Expression_Checkers ...
21:47:54 Finished KD_Tree/document (0:00:04 elapsed time)
21:47:54 Preparing KD_Tree/outline ...
21:47:55 Finished Binomial-Heaps/outline (0:00:04 elapsed time)
21:47:55 Preparing AxiomaticCategoryTheory/document ...
21:47:55 Timing Binomial-Heaps (4 threads, 16.818s elapsed time, 48.592s cpu time, 2.620s GC time, factor 2.89)
21:47:55 Finished Binomial-Heaps (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.48)
21:47:55 Running Coinductive_Languages ...
21:47:55 Bell_Numbers_Spivey: theory Card_Partitions.Injectivity_Solver
21:47:56 Bell_Numbers_Spivey: theory Card_Partitions.Card_Partitions
21:47:56 Decreasing-Diagrams: theory Decreasing-Diagrams.Decreasing_Diagrams
21:47:56 Bell_Numbers_Spivey: theory Bell_Numbers_Spivey.Bell_Numbers
21:47:57 Finished Finger-Trees/outline (0:00:04 elapsed time)
21:47:57 Timing Finger-Trees (4 threads, 17.656s elapsed time, 34.922s cpu time, 2.079s GC time, factor 1.98)
21:47:57 Finished Finger-Trees (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.78)
21:47:57 Running Nash_Williams ...
21:47:57 Coinductive_Languages: theory Coinductive_Languages.Coinductive_Language
21:47:57 Coinductive_Languages: theory HOL-Library.Nat_Bijection
21:47:57 Coinductive_Languages: theory Regular-Sets.Regular_Set
21:47:57 Coinductive_Languages: theory HOL-Library.Old_Datatype
21:47:58 Preparing Ribbon_Proofs/document ...
21:47:58 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
21:47:58 Finished KD_Tree/outline (0:00:03 elapsed time)
21:47:58 Coinductive_Languages: theory HOL-Library.Countable
21:47:58 Finished AxiomaticCategoryTheory/document (0:00:03 elapsed time)
21:47:58 Preparing AxiomaticCategoryTheory/outline ...
21:47:58 Timing KD_Tree (4 threads, 12.789s elapsed time, 45.816s cpu time, 1.064s GC time, factor 3.58)
21:47:58 Finished KD_Tree (0:00:17 elapsed time, 0:00:49 cpu time, factor 2.90)
21:47:58 Building Combinatorics_Words ...
21:47:59 Nash_Williams: theory HOL-Library.Infinite_Set
21:47:59 Nash_Williams: theory HOL-Library.Nat_Bijection
21:47:59 Nash_Williams: theory HOL-Library.FuncSet
21:47:59 Nash_Williams: theory HOL-Library.Old_Datatype
21:48:00 Preparing Lambda_Free_RPOs/document ...
21:48:00 Coinductive_Languages: theory HOL-Library.FSet
21:48:01 Nash_Williams: theory HOL-Library.Ramsey
21:48:01 Nash_Williams: theory HOL-Library.Countable
21:48:02 Finished AxiomaticCategoryTheory/outline (0:00:03 elapsed time)
21:48:02 Nash_Williams: theory HOL-Library.Countable_Set
21:48:02 Timing AxiomaticCategoryTheory (4 threads, 14.208s elapsed time, 37.995s cpu time, 1.223s GC time, factor 2.67)
21:48:02 Finished AxiomaticCategoryTheory (0:00:16 elapsed time, 0:00:40 cpu time, factor 2.38)
21:48:02 Running Category2 ...
21:48:02 Combinatorics_Words: theory Combinatorics_Words.Arithmetical_Hints
21:48:02 Combinatorics_Words: theory Combinatorics_Words.Reverse_Symmetry
21:48:02 Coinductive_Languages: theory Coinductive_Languages.Coinductive_Regular_Set
21:48:03 Nash_Williams: theory Nash_Williams.Nash_Extras
21:48:03 Combinatorics_Words: theory Combinatorics_Words.CoWBasic
21:48:03 Nash_Williams: theory Nash_Williams.Nash_Williams
21:48:03 Finished Ribbon_Proofs/document (0:00:05 elapsed time)
21:48:03 Preparing Ribbon_Proofs/outline ...
21:48:04 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
21:48:04 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Example
21:48:04 Coinductive_Languages: theory Coinductive_Languages.Context_Free_Grammar
21:48:05 Finished Lambda_Free_RPOs/document (0:00:05 elapsed time)
21:48:05 Preparing Lambda_Free_RPOs/outline ...
21:48:06 Category2: theory HOL-ZF.LProd
21:48:06 Category2: theory Category2.Category
21:48:06 Category2: theory HOL-ZF.HOLZF
21:48:07 Category2: theory HOL-ZF.Zet
21:48:08 Category2: theory HOL-ZF.MainZF
21:48:08 Category2: theory Category2.Functors
21:48:08 Category2: theory Category2.Universe
21:48:08 Finished Ribbon_Proofs/outline (0:00:04 elapsed time)
21:48:08 Preparing Real_Power/document ...
21:48:08 Combinatorics_Words: theory Combinatorics_Words.Lyndon_Schutzenberger
21:48:08 Combinatorics_Words: theory Combinatorics_Words.Periodicity_Lemma
21:48:08 Combinatorics_Words: theory Combinatorics_Words.Submonoids
21:48:08 Category2: theory Category2.MonadicEquationalTheory
21:48:08 Timing Ribbon_Proofs (4 threads, 15.634s elapsed time, 36.104s cpu time, 1.646s GC time, factor 2.31)
21:48:08 Finished Ribbon_Proofs (0:00:19 elapsed time, 0:00:40 cpu time, factor 2.02)
21:48:08 Running JiveDataStoreModel ...
21:48:09 Finished Lambda_Free_RPOs/outline (0:00:03 elapsed time)
21:48:09 Category2: theory Category2.NatTrans
21:48:09 Category2: theory Category2.SetCat
21:48:09 Timing Lambda_Free_RPOs (4 threads, 14.126s elapsed time, 53.439s cpu time, 1.993s GC time, factor 3.78)
21:48:09 Finished Lambda_Free_RPOs (0:00:18 elapsed time, 0:00:57 cpu time, factor 3.09)
21:48:09 Running Random_Graph_Subgraph_Threshold ...
21:48:10 Category2: theory Category2.Yoneda
21:48:10 JiveDataStoreModel: theory JiveDataStoreModel.TypeIds
21:48:11 Combinatorics_Words: theory Combinatorics_Words.CoWAll
21:48:12 Preparing Decreasing-Diagrams/document ...
21:48:12 JiveDataStoreModel: theory JiveDataStoreModel.JavaType
21:48:12 Preparing Coinductive_Languages/document ...
21:48:12 Finished Real_Power/document (0:00:04 elapsed time)
21:48:12 Preparing Real_Power/outline ...
21:48:14 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
21:48:15 Preparing Boolean_Expression_Checkers/document ...
21:48:15 Finished Coinductive_Languages/document (0:00:02 elapsed time)
21:48:15 Preparing Coinductive_Languages/outline ...
21:48:15 JiveDataStoreModel: theory JiveDataStoreModel.DirectSubtypes
21:48:15 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
21:48:15 JiveDataStoreModel: theory JiveDataStoreModel.Subtype
21:48:15 Preparing Nash_Williams/document ...
21:48:15 JiveDataStoreModel: theory JiveDataStoreModel.Attributes
21:48:15 JiveDataStoreModel: theory JiveDataStoreModel.Value
21:48:15 Finished Real_Power/outline (0:00:02 elapsed time)
21:48:15 Timing Real_Power (4 threads, 15.503s elapsed time, 32.437s cpu time, 0.581s GC time, factor 2.09)
21:48:15 Finished Real_Power (0:00:18 elapsed time, 0:00:34 cpu time, factor 1.93)
21:48:15 Running IMO2019 ...
21:48:16 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
21:48:16 JiveDataStoreModel: theory JiveDataStoreModel.AttributesIndep
21:48:17 JiveDataStoreModel: theory JiveDataStoreModel.Location
21:48:17 Finished Boolean_Expression_Checkers/document (0:00:02 elapsed time)
21:48:17 Preparing Boolean_Expression_Checkers/outline ...
21:48:17 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
21:48:17 Finished Coinductive_Languages/outline (0:00:02 elapsed time)
21:48:17 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
21:48:17 Timing Coinductive_Languages (4 threads, 14.008s elapsed time, 49.173s cpu time, 1.530s GC time, factor 3.51)
21:48:17 Finished Coinductive_Languages (0:00:16 elapsed time, 0:00:51 cpu time, factor 3.10)
21:48:17 Running Catalan_Numbers ...
21:48:18 JiveDataStoreModel: theory JiveDataStoreModel.Store
21:48:18 Finished Decreasing-Diagrams/document (0:00:06 elapsed time)
21:48:18 Preparing Decreasing-Diagrams/outline ...
21:48:18 Preparing Category2/document ...
21:48:18 Finished Nash_Williams/document (0:00:03 elapsed time)
21:48:18 Preparing Nash_Williams/outline ...
21:48:19 Finished Boolean_Expression_Checkers/outline (0:00:02 elapsed time)
21:48:19 Timing Boolean_Expression_Checkers (4 threads, 15.834s elapsed time, 29.934s cpu time, 1.717s GC time, factor 1.89)
21:48:19 Finished Boolean_Expression_Checkers (0:00:20 elapsed time, 0:00:33 cpu time, factor 1.68)
21:48:19 Running Strong_Security ...
21:48:19 JiveDataStoreModel: theory JiveDataStoreModel.StoreProperties
21:48:19 JiveDataStoreModel: theory JiveDataStoreModel.JML
21:48:19 JiveDataStoreModel: theory JiveDataStoreModel.UnivSpec
21:48:21 Strong_Security: theory Strong_Security.Types
21:48:21 Strong_Security: theory Strong_Security.Expr
21:48:21 Strong_Security: theory Strong_Security.MWLf
21:48:21 Strong_Security: theory Strong_Security.Strong_Security
21:48:21 Catalan_Numbers: theory HOL-Library.Function_Algebras
21:48:21 Catalan_Numbers: theory HOL-Library.Landau_Symbols
21:48:21 Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
21:48:21 Catalan_Numbers: theory Landau_Symbols.Group_Sort
21:48:21 Strong_Security: theory Strong_Security.Up_To_Technique
21:48:21 IMO2019: theory IMO2019.IMO2019_Q5
21:48:21 IMO2019: theory IMO2019.IMO2019_Q1
21:48:21 IMO2019: theory IMO2019.IMO2019_Q4
21:48:21 Strong_Security: theory Strong_Security.Parallel_Composition
21:48:21 Preparing JiveDataStoreModel/document ...
21:48:22 Finished Nash_Williams/outline (0:00:03 elapsed time)
21:48:22 Timing Nash_Williams (4 threads, 14.960s elapsed time, 54.331s cpu time, 1.316s GC time, factor 3.63)
21:48:22 Finished Nash_Williams (0:00:17 elapsed time, 0:00:56 cpu time, factor 3.24)
21:48:22 Running PropResPI ...
21:48:22 Finished Decreasing-Diagrams/outline (0:00:03 elapsed time)
21:48:22 Strong_Security: theory Strong_Security.Domain_example
21:48:22 Preparing Random_Graph_Subgraph_Threshold/document ...
21:48:22 Timing Decreasing-Diagrams (4 threads, 14.996s elapsed time, 48.828s cpu time, 1.068s GC time, factor 3.26)
21:48:22 Finished Decreasing-Diagrams (0:00:19 elapsed time, 0:00:52 cpu time, factor 2.74)
21:48:22 Running Abstract_Soundness ...
21:48:23 Preparing Bell_Numbers_Spivey/document ...
21:48:23 Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
21:48:24 Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
21:48:24 PropResPI: theory PropResPI.Propositional_Resolution
21:48:24 Strong_Security: theory Strong_Security.Language_Composition
21:48:24 Strong_Security: theory Strong_Security.Type_System
21:48:25 Strong_Security: theory Strong_Security.Type_System_example
21:48:26 Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
21:48:26 Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
21:48:26 Finished Bell_Numbers_Spivey/document (0:00:03 elapsed time)
21:48:26 Preparing Bell_Numbers_Spivey/outline ...
21:48:27 Finished JiveDataStoreModel/document (0:00:05 elapsed time)
21:48:27 Preparing JiveDataStoreModel/outline ...
21:48:28 Finished Random_Graph_Subgraph_Threshold/document (0:00:05 elapsed time)
21:48:28 Preparing Random_Graph_Subgraph_Threshold/outline ...
21:48:28 PropResPI: theory PropResPI.Prime_Implicates
21:48:28 Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
21:48:28 Finished Category2/document (0:00:09 elapsed time)
21:48:28 Preparing Category2/outline ...
21:48:29 Catalan_Numbers: theory Landau_Symbols.Landau_More
21:48:29 Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
21:48:29 Preparing Combinatorics_Words/document ...
21:48:29 Finished Bell_Numbers_Spivey/outline (0:00:03 elapsed time)
21:48:30 Timing Bell_Numbers_Spivey (4 threads, 11.147s elapsed time, 37.730s cpu time, 0.618s GC time, factor 3.38)
21:48:30 Finished Bell_Numbers_Spivey (0:00:32 elapsed time, 0:01:08 cpu time, factor 2.15)
21:48:30 Running Szemeredi_Regularity ...
21:48:31 Preparing Strong_Security/document ...
21:48:31 Finished Random_Graph_Subgraph_Threshold/outline (0:00:03 elapsed time)
21:48:32 Timing Random_Graph_Subgraph_Threshold (4 threads, 7.589s elapsed time, 22.680s cpu time, 0.505s GC time, factor 2.99)
21:48:32 Finished Random_Graph_Subgraph_Threshold (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.15)
21:48:32 Running Euler_MacLaurin ...
21:48:32 Finished JiveDataStoreModel/outline (0:00:04 elapsed time)
21:48:32 Preparing IMO2019/document ...
21:48:33 Timing JiveDataStoreModel (4 threads, 10.255s elapsed time, 26.412s cpu time, 1.119s GC time, factor 2.58)
21:48:33 Finished JiveDataStoreModel (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.23)
21:48:33 Running MonoBoolTranAlgebra ...
21:48:33 Szemeredi_Regularity: theory Girth_Chromatic.Girth_Chromatic_Misc
21:48:33 Szemeredi_Regularity: theory Girth_Chromatic.Ugraphs
21:48:33 Finished Category2/outline (0:00:05 elapsed time)
21:48:33 Preparing Catalan_Numbers/document ...
21:48:33 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
21:48:34 Timing Category2 (4 threads, 11.243s elapsed time, 42.855s cpu time, 2.314s GC time, factor 3.81)
21:48:34 Finished Category2 (0:00:15 elapsed time, 0:00:47 cpu time, factor 2.98)
21:48:34 Running Completeness ...
21:48:34 MonoBoolTranAlgebra: theory LatticeProperties.Conj_Disj
21:48:34 MonoBoolTranAlgebra: theory LatticeProperties.WellFoundedTransitive
21:48:35 MonoBoolTranAlgebra: theory LatticeProperties.Complete_Lattice_Prop
21:48:35 Completeness: theory Completeness.Tree
21:48:35 Completeness: theory HOL-Library.Cancellation
21:48:36 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran
21:48:36 Finished Strong_Security/document (0:00:04 elapsed time)
21:48:36 Preparing Strong_Security/outline ...
21:48:36 Finished IMO2019/document (0:00:03 elapsed time)
21:48:36 Preparing IMO2019/outline ...
21:48:36 Completeness: theory HOL-Library.Multiset
21:48:36 Euler_MacLaurin: theory HOL-Library.Function_Algebras
21:48:36 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
21:48:36 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
21:48:37 Preparing PropResPI/document ...
21:48:37 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
21:48:37 Finished Catalan_Numbers/document (0:00:03 elapsed time)
21:48:37 Preparing Catalan_Numbers/outline ...
21:48:38 Preparing Abstract_Soundness/document ...
21:48:38 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
21:48:39 Finished Strong_Security/outline (0:00:03 elapsed time)
21:48:39 Finished IMO2019/outline (0:00:03 elapsed time)
21:48:40 Timing IMO2019 (4 threads, 10.200s elapsed time, 16.313s cpu time, 0.201s GC time, factor 1.60)
21:48:40 Finished IMO2019 (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.35)
21:48:40 Timing Strong_Security (4 threads, 9.636s elapsed time, 33.079s cpu time, 1.103s GC time, factor 3.43)
21:48:40 Finished Strong_Security (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.91)
21:48:40 Building Epistemic_Logic ...
21:48:40 Running Types_Tableaus_and_Goedels_God ...
21:48:40 Finished Catalan_Numbers/outline (0:00:03 elapsed time)
21:48:41 Timing Catalan_Numbers (4 threads, 11.234s elapsed time, 40.805s cpu time, 1.604s GC time, factor 3.63)
21:48:41 Finished Catalan_Numbers (0:00:15 elapsed time, 0:00:44 cpu time, factor 2.91)
21:48:41 Running BNF_Operations ...
21:48:41 Finished PropResPI/document (0:00:04 elapsed time)
21:48:41 Preparing PropResPI/outline ...
21:48:41 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
21:48:41 Finished Abstract_Soundness/document (0:00:03 elapsed time)
21:48:41 Preparing Abstract_Soundness/outline ...
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
21:48:42 Completeness: theory Completeness.PermutationLemmas
21:48:42 Completeness: theory Completeness.Base
21:48:42 Preparing Szemeredi_Regularity/document ...
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
21:48:42 Completeness: theory Completeness.Formula
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
21:48:42 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
21:48:42 BNF_Operations: theory HOL-Library.BNF_Axiomatization
21:48:43 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
21:48:43 Epistemic_Logic: theory Epistemic_Logic.Epistemic_Logic
21:48:43 BNF_Operations: theory BNF_Operations.Compose
21:48:43 BNF_Operations: theory BNF_Operations.GFP
21:48:43 BNF_Operations: theory BNF_Operations.Kill
21:48:43 BNF_Operations: theory BNF_Operations.LFP
21:48:44 BNF_Operations: theory BNF_Operations.Lift
21:48:44 Finished PropResPI/outline (0:00:02 elapsed time)
21:48:44 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Assertion_Algebra
21:48:44 Euler_MacLaurin: theory Landau_Symbols.Landau_More
21:48:44 Timing PropResPI (4 threads, 11.823s elapsed time, 28.833s cpu time, 0.863s GC time, factor 2.44)
21:48:44 Finished PropResPI (0:00:14 elapsed time, 0:00:31 cpu time, factor 2.17)
21:48:44 Running Constructor_Funs ...
21:48:44 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
21:48:44 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Statements
21:48:45 Completeness: theory Completeness.Sequents
21:48:45 Finished Abstract_Soundness/outline (0:00:03 elapsed time)
21:48:45 Timing Abstract_Soundness (4 threads, 11.334s elapsed time, 26.331s cpu time, 1.108s GC time, factor 2.32)
21:48:45 Finished Abstract_Soundness (0:00:15 elapsed time, 0:00:30 cpu time, factor 1.95)
21:48:45 Running Old_Datatype_Show ...
21:48:45 BNF_Operations: theory BNF_Operations.N2M
21:48:45 Completeness: theory Completeness.Completeness
21:48:46 BNF_Operations: theory BNF_Operations.Permute
21:48:46 Preparing MonoBoolTranAlgebra/document ...
21:48:46 Constructor_Funs: theory Constructor_Funs.Constructor_Funs
21:48:47 Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
21:48:47 Finished Szemeredi_Regularity/document (0:00:05 elapsed time)
21:48:47 Preparing Szemeredi_Regularity/outline ...
21:48:48 Completeness: theory Completeness.Soundness
21:48:48 Finished Combinatorics_Words/document (0:00:19 elapsed time)
21:48:48 Preparing Combinatorics_Words/manual ...
21:48:49 Preparing Completeness/document ...
21:48:50 Preparing Euler_MacLaurin/document ...
21:48:50 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
21:48:51 Finished Szemeredi_Regularity/outline (0:00:03 elapsed time)
21:48:51 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
21:48:51 Timing Szemeredi_Regularity (4 threads, 8.041s elapsed time, 23.363s cpu time, 0.494s GC time, factor 2.91)
21:48:51 Finished Szemeredi_Regularity (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.25)
21:48:51 Running Lowe_Ontological_Argument ...
21:48:52 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
21:48:52 Finished MonoBoolTranAlgebra/document (0:00:05 elapsed time)
21:48:52 Preparing MonoBoolTranAlgebra/outline ...
21:48:53 Finished Completeness/document (0:00:03 elapsed time)
21:48:53 Preparing Completeness/outline ...
21:48:53 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
21:48:53 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.Relations
21:48:53 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.QML
21:48:53 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
21:48:53 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
21:48:54 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
21:48:54 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
21:48:54 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
21:48:54 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
21:48:54 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
21:48:55 Preparing Types_Tableaus_and_Goedels_God/document ...
21:48:55 Preparing BNF_Operations/document ...
21:48:56 Finished Completeness/outline (0:00:03 elapsed time)
21:48:56 Finished Euler_MacLaurin/document (0:00:05 elapsed time)
21:48:56 Preparing Euler_MacLaurin/outline ...
21:48:56 Finished MonoBoolTranAlgebra/outline (0:00:03 elapsed time)
21:48:56 Timing Completeness (4 threads, 12.492s elapsed time, 38.530s cpu time, 1.351s GC time, factor 3.08)
21:48:56 Finished Completeness (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.72)
21:48:56 Timing MonoBoolTranAlgebra (4 threads, 10.955s elapsed time, 19.680s cpu time, 0.604s GC time, factor 1.80)
21:48:56 Finished MonoBoolTranAlgebra (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.63)
21:48:56 Running Optimal_BST ...
21:48:56 Running Orbit_Stabiliser ...
21:48:59 Preparing Constructor_Funs/document ...
21:48:59 Optimal_BST: theory Optimal_BST.Weighted_Path_Length
21:48:59 Optimal_BST: theory Optimal_BST.Optimal_BST_Examples
21:48:59 Optimal_BST: theory Optimal_BST.Quadrilateral_Inequality
21:49:00 Finished Combinatorics_Words/manual (0:00:11 elapsed time)
21:49:00 Timing Combinatorics_Words (4 threads, 8.742s elapsed time, 28.042s cpu time, 1.097s GC time, factor 3.21)
21:49:00 Finished Combinatorics_Words (0:00:30 elapsed time, 0:00:59 cpu time, factor 1.99)
21:49:00 Running Recursion-Theory-I ...
21:49:00 Optimal_BST: theory Optimal_BST.Optimal_BST
21:49:00 Finished Euler_MacLaurin/outline (0:00:04 elapsed time)
21:49:01 Timing Euler_MacLaurin (4 threads, 12.230s elapsed time, 44.502s cpu time, 1.365s GC time, factor 3.64)
21:49:01 Finished Euler_MacLaurin (0:00:17 elapsed time, 0:00:49 cpu time, factor 2.79)
21:49:01 Running Inductive_Confidentiality ...
21:49:01 Finished Types_Tableaus_and_Goedels_God/document (0:00:05 elapsed time)
21:49:01 Preparing Types_Tableaus_and_Goedels_God/outline ...
21:49:01 Finished Constructor_Funs/document (0:00:02 elapsed time)
21:49:01 Preparing Constructor_Funs/outline ...
21:49:02 Optimal_BST: theory Optimal_BST.Optimal_BST_Memo
21:49:02 Optimal_BST: theory Optimal_BST.Optimal_BST2
21:49:02 Recursion-Theory-I: theory Recursion-Theory-I.CPair
21:49:02 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun
21:49:03 Preparing Lowe_Ontological_Argument/document ...
21:49:03 Inductive_Confidentiality: theory Inductive_Confidentiality.Message
21:49:03 Inductive_Confidentiality: theory Inductive_Confidentiality.MessageGA
21:49:03 Finished Constructor_Funs/outline (0:00:01 elapsed time)
21:49:03 Timing Old_Datatype_Show (4 threads, 12.071s elapsed time, 14.684s cpu time, 0.536s GC time, factor 1.22)
21:49:03 Finished Old_Datatype_Show (0:00:17 elapsed time, 0:00:19 cpu time, factor 1.12)
21:49:03 Timing Constructor_Funs (4 threads, 12.243s elapsed time, 7.892s cpu time, 0.378s GC time, factor 0.64)
21:49:03 Finished Constructor_Funs (0:00:14 elapsed time, 0:00:10 cpu time, factor 0.69)
21:49:03 Running Euler_Partition ...
21:49:03 Running Error_Function ...
21:49:03 Optimal_BST: theory Optimal_BST.Optimal_BST_Code
21:49:04 Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset
21:49:04 Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet
21:49:04 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2
21:49:04 Recursion-Theory-I: theory Recursion-Theory-I.PRecList
21:49:04 Finished BNF_Operations/document (0:00:09 elapsed time)
21:49:04 Preparing BNF_Operations/outline ...
21:49:04 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
21:49:05 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
21:49:05 Euler_Partition: theory HOL-Library.Cancellation
21:49:06 Finished Types_Tableaus_and_Goedels_God/outline (0:00:04 elapsed time)
21:49:06 Euler_Partition: theory HOL-Library.Multiset
21:49:06 Timing Types_Tableaus_and_Goedels_God (4 threads, 12.765s elapsed time, 25.136s cpu time, 0.335s GC time, factor 1.97)
21:49:06 Finished Types_Tableaus_and_Goedels_God (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.78)
21:49:06 Running MiniML ...
21:49:07 Inductive_Confidentiality: theory Inductive_Confidentiality.EventGA
21:49:07 Inductive_Confidentiality: theory Inductive_Confidentiality.Event
21:49:07 Finished Lowe_Ontological_Argument/document (0:00:04 elapsed time)
21:49:07 Preparing Lowe_Ontological_Argument/outline ...
21:49:07 Error_Function: theory HOL-Library.Function_Algebras
21:49:07 Error_Function: theory Error_Function.Error_Function
21:49:07 Error_Function: theory Landau_Symbols.Group_Sort
21:49:07 Inductive_Confidentiality: theory Inductive_Confidentiality.PublicGA
21:49:07 Inductive_Confidentiality: theory Inductive_Confidentiality.Public
21:49:08 Finished BNF_Operations/outline (0:00:04 elapsed time)
21:49:08 Timing BNF_Operations (4 threads, 10.855s elapsed time, 40.827s cpu time, 3.879s GC time, factor 3.76)
21:49:08 Finished BNF_Operations (0:00:13 elapsed time, 0:00:43 cpu time, factor 3.14)
21:49:08 Running Laplace_Transform ...
21:49:08 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad
21:49:08 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad_GA
21:49:09 MiniML: theory MiniML.Maybe
21:49:09 MiniML: theory MiniML.Type
21:49:09 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityGA
21:49:09 Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr
21:49:09 Error_Function: theory Landau_Symbols.Landau_Real_Products
21:49:09 Inductive_Confidentiality: theory Inductive_Confidentiality.Knowledge
21:49:09 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityDY
21:49:11 Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet
21:49:11 Preparing Epistemic_Logic/document ...
21:49:11 Finished Lowe_Ontological_Argument/outline (0:00:04 elapsed time)
21:49:11 Timing Lowe_Ontological_Argument (4 threads, 8.918s elapsed time, 14.955s cpu time, 0.175s GC time, factor 1.68)
21:49:11 Finished Lowe_Ontological_Argument (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.50)
21:49:11 Running Pratt_Certificate ...
21:49:12 Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
21:49:12 Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
21:49:12 Preparing Optimal_BST/document ...
21:49:13 MiniML: theory MiniML.Instance
21:49:13 Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
21:49:13 MiniML: theory MiniML.Generalize
21:49:14 MiniML: theory MiniML.MiniML
21:49:14 MiniML: theory MiniML.W
21:49:15 Laplace_Transform: theory Laplace_Transform.Existence
21:49:15 Error_Function: theory Landau_Symbols.Landau_Simprocs
21:49:15 Euler_Partition: theory Card_Number_Partitions.Additions_to_Main
21:49:15 Euler_Partition: theory Card_Number_Partitions.Number_Partition
21:49:16 Laplace_Transform: theory Laplace_Transform.Uniqueness
21:49:16 Preparing Orbit_Stabiliser/document ...
21:49:16 Euler_Partition: theory Euler_Partition.Euler_Partition
21:49:16 Laplace_Transform: theory Laplace_Transform.Laplace_Transform
21:49:16 Error_Function: theory Landau_Symbols.Landau_More
21:49:16 Error_Function: theory Error_Function.Error_Function_Asymptotics
21:49:16 Preparing Inductive_Confidentiality/document ...
21:49:17 Pratt_Certificate: theory Lehmer.Lehmer
21:49:17 Finished Optimal_BST/document (0:00:04 elapsed time)
21:49:17 Preparing Optimal_BST/outline ...
21:49:17 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
21:49:18 Finished Epistemic_Logic/document (0:00:07 elapsed time)
21:49:18 Preparing Epistemic_Logic/outline ...
21:49:19 Preparing Error_Function/document ...
21:49:19 Preparing Euler_Partition/document ...
21:49:19 Preparing Recursion-Theory-I/document ...
21:49:20 Preparing MiniML/document ...
21:49:20 Finished Orbit_Stabiliser/document (0:00:04 elapsed time)
21:49:20 Preparing Orbit_Stabiliser/outline ...
21:49:21 Finished Optimal_BST/outline (0:00:03 elapsed time)
21:49:21 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
21:49:21 Timing Optimal_BST (4 threads, 12.180s elapsed time, 47.983s cpu time, 0.931s GC time, factor 3.94)
21:49:21 Finished Optimal_BST (0:00:15 elapsed time, 0:00:51 cpu time, factor 3.23)
21:49:21 Running Skip_Lists ...
21:49:21 Finished Error_Function/document (0:00:02 elapsed time)
21:49:21 Preparing Error_Function/outline ...
21:49:21 Preparing Laplace_Transform/document ...
21:49:22 Finished Euler_Partition/document (0:00:03 elapsed time)
21:49:22 Preparing Euler_Partition/outline ...
21:49:23 Finished Epistemic_Logic/outline (0:00:04 elapsed time)
21:49:23 Timing Epistemic_Logic (4 threads, 8.540s elapsed time, 18.709s cpu time, 0.627s GC time, factor 2.19)
21:49:23 Finished Epistemic_Logic (0:00:31 elapsed time, 0:00:52 cpu time, factor 1.68)
21:49:23 Running Stream-Fusion ...
21:49:23 Finished Orbit_Stabiliser/outline (0:00:03 elapsed time)
21:49:23 Finished Error_Function/outline (0:00:02 elapsed time)
21:49:23 Finished Inductive_Confidentiality/document (0:00:06 elapsed time)
21:49:23 Preparing Inductive_Confidentiality/outline ...
21:49:23 Finished MiniML/document (0:00:03 elapsed time)
21:49:23 Preparing MiniML/outline ...
21:49:23 Timing Error_Function (4 threads, 10.134s elapsed time, 35.303s cpu time, 1.036s GC time, factor 3.48)
21:49:23 Finished Error_Function (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.64)
21:49:23 Timing Orbit_Stabiliser (4 threads, 10.147s elapsed time, 20.843s cpu time, 0.474s GC time, factor 2.05)
21:49:23 Finished Orbit_Stabiliser (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.53)
21:49:23 Running Transformer_Semantics ...
21:49:23 Running CryptoBasedCompositionalProperties ...
21:49:25 Stream-Fusion: theory HOLCF-Library.Int_Discrete
21:49:25 Skip_Lists: theory Skip_Lists.Pi_pmf
21:49:25 Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
21:49:25 Skip_Lists: theory Skip_Lists.Misc
21:49:25 Stream-Fusion: theory Stream-Fusion.LazyList
21:49:25 Finished Euler_Partition/outline (0:00:02 elapsed time)
21:49:25 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.ListExtras
21:49:25 Skip_Lists: theory Skip_Lists.Geometric_PMF
21:49:25 Timing Euler_Partition (4 threads, 12.660s elapsed time, 37.640s cpu time, 0.998s GC time, factor 2.97)
21:49:25 Finished Euler_Partition (0:00:15 elapsed time, 0:00:39 cpu time, factor 2.60)
21:49:25 Running Minimal_SSA ...
21:49:26 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy_types
21:49:26 Skip_Lists: theory Skip_Lists.Skip_List
21:49:26 Stream-Fusion: theory Stream-Fusion.Stream
21:49:26 Finished MiniML/outline (0:00:03 elapsed time)
21:49:26 Timing MiniML (4 threads, 10.421s elapsed time, 22.901s cpu time, 0.601s GC time, factor 2.20)
21:49:26 Finished MiniML (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.91)
21:49:26 Running HyperCTL ...
21:49:27 Finished Laplace_Transform/document (0:00:05 elapsed time)
21:49:27 Preparing Laplace_Transform/outline ...
21:49:28 Preparing Pratt_Certificate/document ...
21:49:28 Stream-Fusion: theory Stream-Fusion.StreamFusion
21:49:28 Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
21:49:28 Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
21:49:29 Finished Inductive_Confidentiality/outline (0:00:05 elapsed time)
21:49:29 Timing Inductive_Confidentiality (4 threads, 12.650s elapsed time, 38.948s cpu time, 1.337s GC time, factor 3.08)
21:49:29 Finished Inductive_Confidentiality (0:00:15 elapsed time, 0:00:41 cpu time, factor 2.69)
21:49:29 Running WorkerWrapper ...
21:49:29 Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
21:49:30 HyperCTL: theory HyperCTL.Prelim
21:49:30 HyperCTL: theory HyperCTL.Shallow
21:49:30 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.inout
21:49:30 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy
21:49:30 Finished Laplace_Transform/outline (0:00:03 elapsed time)
21:49:30 Minimal_SSA: theory Minimal_SSA.Irreducible
21:49:30 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
21:49:31 Timing Laplace_Transform (4 threads, 8.314s elapsed time, 31.592s cpu time, 0.551s GC time, factor 3.80)
21:49:31 Finished Laplace_Transform (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.81)
21:49:31 Running Nullstellensatz ...
21:49:31 HyperCTL: theory HyperCTL.Deep
21:49:31 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.CompLocalSecrets
21:49:31 HyperCTL: theory HyperCTL.Noninterference
21:49:31 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
21:49:31 WorkerWrapper: theory WorkerWrapper.Maybe
21:49:31 WorkerWrapper: theory WorkerWrapper.Nats
21:49:32 Finished Recursion-Theory-I/document (0:00:12 elapsed time)
21:49:32 Preparing Recursion-Theory-I/outline ...
21:49:32 Finished Pratt_Certificate/document (0:00:04 elapsed time)
21:49:32 Preparing Pratt_Certificate/outline ...
21:49:33 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
21:49:33 WorkerWrapper: theory WorkerWrapper.LList
21:49:33 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
21:49:35 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
21:49:35 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
21:49:35 Preparing Stream-Fusion/document ...
21:49:35 WorkerWrapper: theory WorkerWrapper.CounterExample
21:49:35 WorkerWrapper: theory WorkerWrapper.Streams
21:49:35 WorkerWrapper: theory WorkerWrapper.Last
21:49:35 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
21:49:36 WorkerWrapper: theory WorkerWrapper.Accumulator
21:49:36 HyperCTL: theory HyperCTL.Finite_Noninterference
21:49:36 Preparing Skip_Lists/document ...
21:49:36 Finished Pratt_Certificate/outline (0:00:03 elapsed time)
21:49:36 WorkerWrapper: theory WorkerWrapper.Backtracking
21:49:36 Preparing CryptoBasedCompositionalProperties/document ...
21:49:36 Timing Pratt_Certificate (4 threads, 9.866s elapsed time, 31.913s cpu time, 0.527s GC time, factor 3.23)
21:49:36 Finished Pratt_Certificate (0:00:16 elapsed time, 0:00:37 cpu time, factor 2.35)
21:49:36 Running Card_Multisets ...
21:49:36 WorkerWrapper: theory WorkerWrapper.Continuations
21:49:36 HyperCTL: theory HyperCTL.HyperCTL
21:49:36 WorkerWrapper: theory WorkerWrapper.Nub
21:49:37 WorkerWrapper: theory WorkerWrapper.UnboxedNats
21:49:38 Finished Recursion-Theory-I/outline (0:00:05 elapsed time)
21:49:38 Timing Recursion-Theory-I (4 threads, 10.472s elapsed time, 36.936s cpu time, 1.491s GC time, factor 3.53)
21:49:38 Finished Recursion-Theory-I (0:00:18 elapsed time, 0:00:39 cpu time, factor 2.12)
21:49:38 Running Huffman ...
21:49:38 Card_Multisets: theory HOL-Library.Cancellation
21:49:38 Preparing Minimal_SSA/document ...
21:49:39 Preparing Transformer_Semantics/document ...
21:49:39 Card_Multisets: theory HOL-Library.Multiset
21:49:39 Finished Stream-Fusion/document (0:00:03 elapsed time)
21:49:39 Preparing Stream-Fusion/outline ...
21:49:39 Huffman: theory Huffman.Huffman
21:49:40 Finished CryptoBasedCompositionalProperties/document (0:00:04 elapsed time)
21:49:40 Preparing CryptoBasedCompositionalProperties/outline ...
21:49:41 Preparing HyperCTL/document ...
21:49:41 Preparing WorkerWrapper/document ...
21:49:42 Finished Skip_Lists/document (0:00:06 elapsed time)
21:49:42 Preparing Skip_Lists/outline ...
21:49:42 Finished Stream-Fusion/outline (0:00:03 elapsed time)
21:49:43 Timing Stream-Fusion (4 threads, 9.709s elapsed time, 14.869s cpu time, 0.284s GC time, factor 1.53)
21:49:43 Finished Stream-Fusion (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.39)
21:49:43 Running Randomised_BSTs ...
21:49:43 Finished Minimal_SSA/document (0:00:04 elapsed time)
21:49:43 Preparing Minimal_SSA/outline ...
21:49:44 Finished CryptoBasedCompositionalProperties/outline (0:00:03 elapsed time)
21:49:44 Finished Transformer_Semantics/document (0:00:05 elapsed time)
21:49:44 Preparing Transformer_Semantics/outline ...
21:49:44 Timing CryptoBasedCompositionalProperties (4 threads, 9.869s elapsed time, 25.991s cpu time, 0.798s GC time, factor 2.63)
21:49:44 Finished CryptoBasedCompositionalProperties (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.31)
21:49:44 Running Lower_Semicontinuous ...
21:49:44 Finished HyperCTL/document (0:00:03 elapsed time)
21:49:44 Preparing HyperCTL/outline ...
21:49:44 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
21:49:44 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
21:49:44 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
21:49:44 Nullstellensatz: theory Nullstellensatz.Univariate_PM
21:49:45 Card_Multisets: theory Card_Multisets.Card_Multisets
21:49:45 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
21:49:45 Finished Skip_Lists/outline (0:00:03 elapsed time)
21:49:46 Timing Skip_Lists (4 threads, 9.805s elapsed time, 34.695s cpu time, 0.557s GC time, factor 3.54)
21:49:46 Finished Skip_Lists (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.72)
21:49:46 Running Lam-ml-Normalization ...
21:49:46 Finished WorkerWrapper/document (0:00:04 elapsed time)
21:49:46 Preparing WorkerWrapper/outline ...
21:49:46 Finished Minimal_SSA/outline (0:00:03 elapsed time)
21:49:46 Timing Minimal_SSA (4 threads, 7.361s elapsed time, 23.151s cpu time, 0.433s GC time, factor 3.15)
21:49:46 Finished Minimal_SSA (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.22)
21:49:46 Running Integration ...
21:49:46 Finished HyperCTL/outline (0:00:02 elapsed time)
21:49:47 Timing HyperCTL (4 threads, 9.800s elapsed time, 34.624s cpu time, 1.630s GC time, factor 3.53)
21:49:47 Finished HyperCTL (0:00:13 elapsed time, 0:00:38 cpu time, factor 2.75)
21:49:47 Running Landau_Symbols ...
21:49:47 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
21:49:47 Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
21:49:47 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
21:49:47 Lam-ml-Normalization: theory HOL-Library.LaTeXsugar
21:49:48 Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
21:49:48 Finished Transformer_Semantics/outline (0:00:04 elapsed time)
21:49:48 Preparing Card_Multisets/document ...
21:49:48 Timing Transformer_Semantics (4 threads, 9.503s elapsed time, 34.050s cpu time, 1.023s GC time, factor 3.58)
21:49:48 Finished Transformer_Semantics (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.62)
21:49:48 Running Card_Partitions ...
21:49:48 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
21:49:49 Preparing Huffman/document ...
21:49:49 Integration: theory Integration.Sigma_Algebra
21:49:49 Integration: theory Integration.MonConv
21:49:50 Integration: theory Integration.Measure
21:49:50 Landau_Symbols: theory Landau_Symbols.Group_Sort
21:49:50 Finished WorkerWrapper/outline (0:00:04 elapsed time)
21:49:50 Timing WorkerWrapper (4 threads, 8.816s elapsed time, 24.718s cpu time, 0.691s GC time, factor 2.80)
21:49:50 Finished WorkerWrapper (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.34)
21:49:50 Running VolpanoSmith ...
21:49:50 Card_Partitions: theory HOL-Eisbach.Eisbach
21:49:50 Card_Partitions: theory HOL-Combinatorics.Stirling
21:49:50 Card_Partitions: theory HOL-Library.Adhoc_Overloading
21:49:50 Card_Partitions: theory HOL-Library.FuncSet
21:49:51 Integration: theory Integration.RealRandVar
21:49:51 Card_Partitions: theory HOL-Library.Monad_Syntax
21:49:51 Finished Card_Multisets/document (0:00:03 elapsed time)
21:49:51 Preparing Card_Multisets/outline ...
21:49:52 Landau_Symbols: theory Landau_Symbols.Landau_Real_Products
21:49:52 VolpanoSmith: theory VolpanoSmith.Semantics
21:49:52 Integration: theory Integration.Failure
21:49:52 Integration: theory Integration.Integral
21:49:53 Card_Partitions: theory HOL-Library.Disjoint_Sets
21:49:53 Finished Huffman/document (0:00:04 elapsed time)
21:49:53 Preparing Huffman/outline ...
21:49:54 Finished Card_Multisets/outline (0:00:03 elapsed time)
21:49:54 Preparing Nullstellensatz/document ...
21:49:55 Timing Card_Multisets (4 threads, 8.991s elapsed time, 25.193s cpu time, 0.816s GC time, factor 2.80)
21:49:55 Finished Card_Multisets (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.39)
21:49:55 Running Separata ...
21:49:55 Card_Partitions: theory Card_Partitions.Injectivity_Solver
21:49:55 Card_Partitions: theory Card_Partitions.Set_Partition
21:49:56 Card_Partitions: theory Card_Partitions.Card_Partitions
21:49:57 Landau_Symbols: theory Landau_Symbols.Landau_Simprocs
21:49:57 VolpanoSmith: theory VolpanoSmith.secTypes
21:49:57 Finished Huffman/outline (0:00:03 elapsed time)
21:49:57 Timing Huffman (4 threads, 8.358s elapsed time, 24.071s cpu time, 0.533s GC time, factor 2.88)
21:49:57 Finished Huffman (0:00:10 elapsed time, 0:00:26 cpu time, factor 2.42)
21:49:57 Running Belief_Revision ...
21:49:58 Preparing Randomised_BSTs/document ...
21:49:58 Landau_Symbols: theory Landau_Symbols.Landau_More
21:49:58 Separata: theory HOL-Eisbach.Eisbach
21:49:58 Separata: theory Separation_Algebra.Separation_Algebra
21:49:59 VolpanoSmith: theory VolpanoSmith.Execute
21:49:59 Preparing Lower_Semicontinuous/document ...
21:49:59 Preparing Card_Partitions/document ...
21:49:59 Preparing Lam-ml-Normalization/document ...
21:49:59 Belief_Revision: theory Belief_Revision.AGM_Logic
21:50:00 Belief_Revision: theory Belief_Revision.AGM_Remainder
21:50:00 Preparing Integration/document ...
21:50:00 Belief_Revision: theory Belief_Revision.AGM_Contraction
21:50:00 Preparing Landau_Symbols/document ...
21:50:00 Separata: theory HOL-Eisbach.Eisbach_Tools
21:50:00 Separata: theory Separata.Separata
21:50:01 Belief_Revision: theory Belief_Revision.AGM_Revision
21:50:01 Preparing VolpanoSmith/document ...
21:50:01 Finished Nullstellensatz/document (0:00:07 elapsed time)
21:50:01 Preparing Nullstellensatz/outline ...
21:50:02 Finished Lower_Semicontinuous/document (0:00:03 elapsed time)
21:50:02 Preparing Lower_Semicontinuous/outline ...
21:50:02 Finished Randomised_BSTs/document (0:00:04 elapsed time)
21:50:02 Preparing Randomised_BSTs/outline ...
21:50:03 Finished Card_Partitions/document (0:00:03 elapsed time)
21:50:03 Preparing Card_Partitions/outline ...
21:50:04 Finished Landau_Symbols/document (0:00:03 elapsed time)
21:50:04 Preparing Landau_Symbols/outline ...
21:50:04 Finished Lam-ml-Normalization/document (0:00:04 elapsed time)
21:50:04 Preparing Lam-ml-Normalization/outline ...
21:50:04 Finished Lower_Semicontinuous/outline (0:00:02 elapsed time)
21:50:05 Timing Lower_Semicontinuous (4 threads, 10.513s elapsed time, 23.847s cpu time, 0.382s GC time, factor 2.27)
21:50:05 Finished Lower_Semicontinuous (0:00:14 elapsed time, 0:00:27 cpu time, factor 1.89)
21:50:05 Running GPU_Kernel_PL ...
21:50:05 Finished Nullstellensatz/outline (0:00:03 elapsed time)
21:50:05 Timing Nullstellensatz (4 threads, 8.796s elapsed time, 21.550s cpu time, 0.870s GC time, factor 2.45)
21:50:05 Finished Nullstellensatz (0:00:23 elapsed time, 0:00:35 cpu time, factor 1.54)
21:50:05 Running RefinementReactive ...
21:50:06 Finished Randomised_BSTs/outline (0:00:03 elapsed time)
21:50:06 Finished Integration/document (0:00:05 elapsed time)
21:50:06 Preparing Integration/outline ...
21:50:06 Finished VolpanoSmith/document (0:00:04 elapsed time)
21:50:06 Preparing VolpanoSmith/outline ...
21:50:06 Timing Randomised_BSTs (4 threads, 9.464s elapsed time, 32.696s cpu time, 0.722s GC time, factor 3.45)
21:50:06 Finished Randomised_BSTs (0:00:14 elapsed time, 0:00:37 cpu time, factor 2.58)
21:50:06 Running Tycon ...
21:50:06 Finished Card_Partitions/outline (0:00:03 elapsed time)
21:50:06 Finished Landau_Symbols/outline (0:00:02 elapsed time)
21:50:06 Timing Card_Partitions (4 threads, 7.604s elapsed time, 28.779s cpu time, 0.494s GC time, factor 3.78)
21:50:06 Finished Card_Partitions (0:00:10 elapsed time, 0:00:31 cpu time, factor 3.02)
21:50:06 Timing Landau_Symbols (4 threads, 9.105s elapsed time, 25.818s cpu time, 0.876s GC time, factor 2.84)
21:50:06 Finished Landau_Symbols (0:00:13 elapsed time, 0:00:29 cpu time, factor 2.26)
21:50:06 Running Van_der_Waerden ...
21:50:06 Running FeatherweightJava ...
21:50:07 GPU_Kernel_PL: theory GPU_Kernel_PL.Misc
21:50:07 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax
21:50:07 RefinementReactive: theory RefinementReactive.Refinement
21:50:07 RefinementReactive: theory RefinementReactive.Temporal
21:50:08 Tycon: theory Tycon.Coerce
21:50:08 Tycon: theory Tycon.TypeApp
21:50:08 Finished Lam-ml-Normalization/outline (0:00:04 elapsed time)
21:50:08 Tycon: theory Tycon.Functor
21:50:08 Preparing Separata/document ...
21:50:08 FeatherweightJava: theory FeatherweightJava.FJDefs
21:50:08 Van_der_Waerden: theory HOL-Library.FuncSet
21:50:08 Van_der_Waerden: theory Van_der_Waerden.Digits
21:50:08 Timing Lam-ml-Normalization (4 threads, 10.475s elapsed time, 22.039s cpu time, 0.784s GC time, factor 2.10)
21:50:08 Finished Lam-ml-Normalization (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.84)
21:50:08 Running Latin_Square ...
21:50:09 Preparing Belief_Revision/document ...
21:50:09 Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
21:50:09 Finished VolpanoSmith/outline (0:00:03 elapsed time)
21:50:09 RefinementReactive: theory RefinementReactive.Reactive
21:50:09 Timing VolpanoSmith (4 threads, 8.201s elapsed time, 19.169s cpu time, 0.638s GC time, factor 2.34)
21:50:09 Finished VolpanoSmith (0:00:10 elapsed time, 0:00:21 cpu time, factor 1.98)
21:50:09 Running Robbins-Conjecture ...
21:50:10 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state
21:50:10 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness
21:50:10 Finished Integration/outline (0:00:04 elapsed time)
21:50:10 Timing Integration (4 threads, 9.225s elapsed time, 20.018s cpu time, 0.577s GC time, factor 2.17)
21:50:10 Finished Integration (0:00:13 elapsed time, 0:00:23 cpu time, factor 1.81)
21:50:10 Running Noninterference_Concurrent_Composition ...
21:50:10 Tycon: theory Tycon.Monad
21:50:10 Latin_Square: theory Marriage.Marriage
21:50:10 Tycon: theory Tycon.Binary_Tree_Monad
21:50:10 Tycon: theory Tycon.Monad_Zero
21:50:10 Tycon: theory Tycon.Lift_Monad
21:50:10 Tycon: theory Tycon.Monad_Plus
21:50:10 Latin_Square: theory Latin_Square.Latin_Square
21:50:11 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread
21:50:11 Tycon: theory Tycon.Writer_Monad
21:50:11 Finished Separata/document (0:00:02 elapsed time)
21:50:11 Preparing Separata/outline ...
21:50:11 Tycon: theory Tycon.Error_Monad
21:50:11 Tycon: theory Tycon.Resumption_Transformer
21:50:11 Tycon: theory Tycon.Monad_Zero_Plus
21:50:11 Robbins-Conjecture: theory Robbins-Conjecture.Robbins_Conjecture
21:50:12 Tycon: theory Tycon.Writer_Transformer
21:50:12 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group
21:50:12 Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
21:50:12 Tycon: theory Tycon.Error_Transformer
21:50:12 Tycon: theory Tycon.Lazy_List_Monad
21:50:12 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel
21:50:13 Tycon: theory Tycon.Maybe_Monad
21:50:13 FeatherweightJava: theory FeatherweightJava.FJAux
21:50:13 Tycon: theory Tycon.State_Transformer
21:50:13 Finished Separata/outline (0:00:02 elapsed time)
21:50:13 Timing Separata (4 threads, 8.748s elapsed time, 29.733s cpu time, 0.646s GC time, factor 3.40)
21:50:13 Finished Separata (0:00:13 elapsed time, 0:00:33 cpu time, factor 2.58)
21:50:13 Running Impossible_Geometry ...
21:50:14 FeatherweightJava: theory FeatherweightJava.FJSound
21:50:15 FeatherweightJava: theory FeatherweightJava.Execute
21:50:15 GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language
21:50:15 Tycon: theory Tycon.Monad_Transformer
21:50:15 Preparing Van_der_Waerden/document ...
21:50:16 Impossible_Geometry: theory Impossible_Geometry.Impossible_Geometry
21:50:16 Preparing GPU_Kernel_PL/document ...
21:50:17 Preparing Latin_Square/document ...
21:50:17 Finished Belief_Revision/document (0:00:08 elapsed time)
21:50:17 Preparing Belief_Revision/outline ...
21:50:17 Preparing Tycon/document ...
21:50:17 FeatherweightJava: theory FeatherweightJava.Featherweight_Java
21:50:17 Preparing RefinementReactive/document ...
21:50:19 Finished Van_der_Waerden/document (0:00:03 elapsed time)
21:50:19 Preparing Van_der_Waerden/outline ...
21:50:19 Preparing FeatherweightJava/document ...
21:50:20 Finished GPU_Kernel_PL/document (0:00:03 elapsed time)
21:50:20 Preparing GPU_Kernel_PL/outline ...
21:50:20 Finished Latin_Square/document (0:00:03 elapsed time)
21:50:20 Preparing Latin_Square/outline ...
21:50:22 Preparing Noninterference_Concurrent_Composition/document ...
21:50:22 Preparing Robbins-Conjecture/document ...
21:50:22 Finished Van_der_Waerden/outline (0:00:03 elapsed time)
21:50:22 Finished Belief_Revision/outline (0:00:05 elapsed time)
21:50:22 Timing Van_der_Waerden (4 threads, 5.750s elapsed time, 22.365s cpu time, 0.322s GC time, factor 3.89)
21:50:22 Finished Van_der_Waerden (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.96)
21:50:22 Timing Belief_Revision (4 threads, 8.644s elapsed time, 29.663s cpu time, 0.663s GC time, factor 3.43)
21:50:22 Finished Belief_Revision (0:00:11 elapsed time, 0:00:31 cpu time, factor 2.85)
21:50:22 Running Attack_Trees ...
21:50:22 Running Selection_Heap_Sort ...
21:50:22 Finished RefinementReactive/document (0:00:04 elapsed time)
21:50:22 Preparing RefinementReactive/outline ...
21:50:23 Finished Tycon/document (0:00:05 elapsed time)
21:50:23 Preparing Tycon/outline ...
21:50:23 Finished GPU_Kernel_PL/outline (0:00:03 elapsed time)
21:50:23 Timing GPU_Kernel_PL (4 threads, 8.997s elapsed time, 16.855s cpu time, 0.911s GC time, factor 1.87)
21:50:23 Finished GPU_Kernel_PL (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.66)
21:50:23 Running Menger ...
21:50:23 Finished Latin_Square/outline (0:00:02 elapsed time)
21:50:23 Timing Latin_Square (4 threads, 6.024s elapsed time, 22.767s cpu time, 0.294s GC time, factor 3.78)
21:50:23 Finished Latin_Square (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.97)
21:50:23 Running Rank_Nullity_Theorem ...
21:50:24 Finished Robbins-Conjecture/document (0:00:02 elapsed time)
21:50:24 Preparing Robbins-Conjecture/outline ...
21:50:24 Attack_Trees: theory Attack_Trees.MC
21:50:24 Preparing Impossible_Geometry/document ...
21:50:24 Finished FeatherweightJava/document (0:00:05 elapsed time)
21:50:24 Preparing FeatherweightJava/outline ...
21:50:25 Menger: theory Menger.Graph
21:50:25 Menger: theory Menger.Helpers
21:50:25 Attack_Trees: theory Attack_Trees.AT
21:50:26 Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
21:50:26 Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
21:50:26 Menger: theory Menger.Separations
21:50:26 Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
21:50:26 Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
21:50:26 Finished RefinementReactive/outline (0:00:03 elapsed time)
21:50:26 Finished Robbins-Conjecture/outline (0:00:01 elapsed time)
21:50:26 Menger: theory Menger.DisjointPaths
21:50:26 Timing RefinementReactive (4 threads, 9.490s elapsed time, 25.189s cpu time, 0.488s GC time, factor 2.65)
21:50:26 Finished RefinementReactive (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.29)
21:50:26 Timing Robbins-Conjecture (4 threads, 9.816s elapsed time, 25.544s cpu time, 0.428s GC time, factor 2.60)
21:50:26 Finished Robbins-Conjecture (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.25)
21:50:26 Running First_Welfare_Theorem ...
21:50:26 Running Arith_Prog_Rel_Primes ...
21:50:26 Menger: theory Menger.MengerInduction
21:50:27 Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
21:50:27 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
21:50:27 Attack_Trees: theory Attack_Trees.Infrastructure
21:50:27 Finished Tycon/outline (0:00:04 elapsed time)
21:50:27 Timing Tycon (4 threads, 8.373s elapsed time, 24.452s cpu time, 0.854s GC time, factor 2.92)
21:50:27 Finished Tycon (0:00:10 elapsed time, 0:00:26 cpu time, factor 2.44)
21:50:27 Running Pop_Refinement ...
21:50:27 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
21:50:28 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
21:50:28 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
21:50:28 Menger: theory Menger.Y_eq_new_last
21:50:28 Finished Noninterference_Concurrent_Composition/document (0:00:06 elapsed time)
21:50:28 Preparing Noninterference_Concurrent_Composition/outline ...
21:50:28 Menger: theory Menger.Y_neq_new_last
21:50:28 Menger: theory Menger.Menger
21:50:28 Finished FeatherweightJava/outline (0:00:03 elapsed time)
21:50:28 Timing FeatherweightJava (4 threads, 10.394s elapsed time, 29.439s cpu time, 0.913s GC time, factor 2.83)
21:50:28 Finished FeatherweightJava (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.48)
21:50:29 Running Hello_World ...
21:50:29 Finished Impossible_Geometry/document (0:00:04 elapsed time)
21:50:29 Preparing Impossible_Geometry/outline ...
21:50:29 Pop_Refinement: theory Pop_Refinement.Definition
21:50:29 Pop_Refinement: theory Pop_Refinement.First_Example
21:50:29 Pop_Refinement: theory Pop_Refinement.Future_Work
21:50:29 Pop_Refinement: theory Pop_Refinement.General_Remarks
21:50:29 Pop_Refinement: theory Pop_Refinement.Related_Work
21:50:29 Pop_Refinement: theory Pop_Refinement.Second_Example
21:50:30 Attack_Trees: theory Attack_Trees.GDPRhealthcare
21:50:30 First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
21:50:30 First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
21:50:30 First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
21:50:30 First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
21:50:30 Hello_World: theory HOL-Library.Adhoc_Overloading
21:50:31 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
21:50:31 Hello_World: theory HOL-Library.Monad_Syntax
21:50:31 Hello_World: theory Hello_World.IO
21:50:31 Hello_World: theory Hello_World.HelloWorld
21:50:31 First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
21:50:32 Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
21:50:32 First_Welfare_Theorem: theory First_Welfare_Theorem.Common
21:50:32 Finished Noninterference_Concurrent_Composition/outline (0:00:04 elapsed time)
21:50:32 Timing Noninterference_Concurrent_Composition (4 threads, 8.478s elapsed time, 29.252s cpu time, 0.694s GC time, factor 3.45)
21:50:32 Finished Noninterference_Concurrent_Composition (0:00:11 elapsed time, 0:00:31 cpu time, factor 2.87)
21:50:32 Running Abstract-Hoare-Logics ...
21:50:32 Finished Impossible_Geometry/outline (0:00:03 elapsed time)
21:50:32 Preparing Menger/document ...
21:50:32 First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
21:50:32 First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
21:50:32 First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
21:50:33 Timing Impossible_Geometry (4 threads, 7.611s elapsed time, 18.424s cpu time, 0.436s GC time, factor 2.42)
21:50:33 Finished Impossible_Geometry (0:00:10 elapsed time, 0:00:21 cpu time, factor 1.99)
21:50:33 Running FileRefinement ...
21:50:33 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
21:50:33 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
21:50:34 Preparing Attack_Trees/document ...
21:50:34 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Lang
21:50:34 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsLang
21:50:34 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PLang
21:50:35 FileRefinement: theory FileRefinement.CArrays
21:50:35 FileRefinement: theory FileRefinement.ResizableArrays
21:50:35 FileRefinement: theory FileRefinement.FileRefinement
21:50:35 Preparing Selection_Heap_Sort/document ...
21:50:35 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Hoare
21:50:35 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Termi
21:50:36 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.HoareTotal
21:50:36 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoare
21:50:36 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PTermi
21:50:36 Hello_World: theory Hello_World.HelloWorld_Proof
21:50:36 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoare
21:50:36 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsTermi
21:50:37 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoareTotal
21:50:37 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoareTotal
21:50:37 Preparing Arith_Prog_Rel_Primes/document ...
21:50:37 Preparing Pop_Refinement/document ...
21:50:37 Hello_World: theory Hello_World.RunningCodeFromIsabelle
21:50:37 Preparing Rank_Nullity_Theorem/document ...
21:50:38 Finished Selection_Heap_Sort/document (0:00:03 elapsed time)
21:50:38 Preparing Selection_Heap_Sort/outline ...
21:50:39 Preparing First_Welfare_Theorem/document ...
21:50:39 Preparing Hello_World/document ...
21:50:39 Finished Menger/document (0:00:07 elapsed time)
21:50:39 Preparing Menger/outline ...
21:50:40 Finished Selection_Heap_Sort/outline (0:00:02 elapsed time)
21:50:40 Finished Attack_Trees/document (0:00:06 elapsed time)
21:50:40 Preparing Attack_Trees/outline ...
21:50:40 Finished Arith_Prog_Rel_Primes/document (0:00:03 elapsed time)
21:50:40 Preparing Arith_Prog_Rel_Primes/outline ...
21:50:41 Timing Selection_Heap_Sort (4 threads, 8.208s elapsed time, 24.774s cpu time, 0.813s GC time, factor 3.02)
21:50:41 Finished Selection_Heap_Sort (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.32)
21:50:41 Running Case_Labeling ...
21:50:41 Finished Hello_World/document (0:00:01 elapsed time)
21:50:41 Preparing Hello_World/outline ...
21:50:41 Finished Pop_Refinement/document (0:00:04 elapsed time)
21:50:41 Preparing Pop_Refinement/outline ...
21:50:42 Finished Rank_Nullity_Theorem/document (0:00:04 elapsed time)
21:50:42 Preparing Rank_Nullity_Theorem/outline ...
21:50:42 Case_Labeling: theory HOL-Eisbach.Eisbach
21:50:42 Case_Labeling: theory Case_Labeling.Case_Labeling
21:50:42 Case_Labeling: theory HOL-Hoare.Arith2
21:50:42 Case_Labeling: theory HOL-Hoare.Hoare_Syntax
21:50:42 Preparing Abstract-Hoare-Logics/document ...
21:50:42 Case_Labeling: theory HOL-Hoare.Hoare_Tac
21:50:43 Preparing FileRefinement/document ...
21:50:43 Finished Hello_World/outline (0:00:01 elapsed time)
21:50:43 Timing Hello_World (4 threads, 8.149s elapsed time, 2.601s cpu time, 0.000s GC time, factor 0.32)
21:50:43 Finished Hello_World (0:00:10 elapsed time, 0:00:04 cpu time, factor 0.44)
21:50:43 Running LambdaMu ...
21:50:43 Finished Arith_Prog_Rel_Primes/outline (0:00:02 elapsed time)
21:50:44 Timing Arith_Prog_Rel_Primes (4 threads, 4.151s elapsed time, 13.962s cpu time, 0.277s GC time, factor 3.36)
21:50:44 Finished Arith_Prog_Rel_Primes (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.93)
21:50:44 Running Verified-Prover ...
21:50:44 Case_Labeling: theory Case_Labeling.Conditionals
21:50:44 Case_Labeling: theory Case_Labeling.Monadic_Language
21:50:44 Finished Menger/outline (0:00:05 elapsed time)
21:50:44 Finished Attack_Trees/outline (0:00:04 elapsed time)
21:50:44 Finished First_Welfare_Theorem/document (0:00:05 elapsed time)
21:50:44 Preparing First_Welfare_Theorem/outline ...
21:50:45 Case_Labeling: theory HOL-Hoare.Hoare_Logic
21:50:45 Timing Menger (4 threads, 6.561s elapsed time, 23.015s cpu time, 0.602s GC time, factor 3.51)
21:50:45 Finished Menger (0:00:09 elapsed time, 0:00:25 cpu time, factor 2.78)
21:50:45 Timing Attack_Trees (4 threads, 8.702s elapsed time, 24.266s cpu time, 0.823s GC time, factor 2.79)
21:50:45 Finished Attack_Trees (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.36)
21:50:45 Running InformationFlowSlicing ...
21:50:45 Running GoedelGod ...
21:50:45 LambdaMu: theory LambdaMu.Syntax
21:50:45 Finished Pop_Refinement/outline (0:00:03 elapsed time)
21:50:45 Verified-Prover: theory Verified-Prover.Prover
21:50:45 Finished Rank_Nullity_Theorem/outline (0:00:03 elapsed time)
21:50:46 Finished FileRefinement/document (0:00:03 elapsed time)
21:50:46 Preparing FileRefinement/outline ...
21:50:46 Timing Rank_Nullity_Theorem (4 threads, 9.803s elapsed time, 18.390s cpu time, 0.631s GC time, factor 1.88)
21:50:46 Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.61)
21:50:46 Timing Pop_Refinement (4 threads, 6.645s elapsed time, 19.362s cpu time, 0.712s GC time, factor 2.91)
21:50:46 Finished Pop_Refinement (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.33)
21:50:46 Running FinFun ...
21:50:46 Running Matroids ...
21:50:46 Case_Labeling: theory Case_Labeling.Labeled_Hoare
21:50:46 GoedelGod: theory GoedelGod.GoedelGod
21:50:46 Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
21:50:47 Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
21:50:47 FinFun: theory HOL-Library.Phantom_Type
21:50:47 Matroids: theory Matroids.Indep_System
21:50:48 LambdaMu: theory LambdaMu.DeBruijn
21:50:48 LambdaMu: theory LambdaMu.Types
21:50:48 Finished Abstract-Hoare-Logics/document (0:00:05 elapsed time)
21:50:48 Preparing Abstract-Hoare-Logics/outline ...
21:50:48 LambdaMu: theory LambdaMu.Substitution
21:50:48 LambdaMu: theory LambdaMu.Peirce
21:50:48 LambdaMu: theory LambdaMu.Reduction
21:50:48 Matroids: theory Matroids.Matroid
21:50:48 FinFun: theory HOL-Library.Cardinality
21:50:48 LambdaMu: theory LambdaMu.ContextFacts
21:50:49 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
21:50:49 Finished First_Welfare_Theorem/outline (0:00:04 elapsed time)
21:50:49 Timing First_Welfare_Theorem (4 threads, 8.220s elapsed time, 28.492s cpu time, 0.733s GC time, factor 3.47)
21:50:49 Finished First_Welfare_Theorem (0:00:12 elapsed time, 0:00:32 cpu time, factor 2.61)
21:50:49 Running FOL_Seq_Calc1 ...
21:50:49 Finished FileRefinement/outline (0:00:03 elapsed time)
21:50:49 LambdaMu: theory LambdaMu.TypePreservation
21:50:49 LambdaMu: theory LambdaMu.Progress
21:50:49 Timing FileRefinement (4 threads, 7.277s elapsed time, 17.647s cpu time, 0.162s GC time, factor 2.43)
21:50:49 Finished FileRefinement (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.01)
21:50:49 Running Comparison_Sort_Lower_Bound ...
21:50:50 FinFun: theory FinFun.FinFun
21:50:50 InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
21:50:51 Preparing Case_Labeling/document ...
21:50:52 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
21:50:52 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
21:50:52 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
21:50:52 Finished Abstract-Hoare-Logics/outline (0:00:04 elapsed time)
21:50:53 Timing Abstract-Hoare-Logics (4 threads, 7.394s elapsed time, 27.284s cpu time, 1.203s GC time, factor 3.69)
21:50:53 Finished Abstract-Hoare-Logics (0:00:10 elapsed time, 0:00:29 cpu time, factor 2.96)
21:50:53 Running Concurrent_Ref_Alg ...
21:50:53 FinFun: theory FinFun.FinFunPred
21:50:53 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
21:50:53 Preparing Matroids/document ...
21:50:54 Preparing LambdaMu/document ...
21:50:54 Preparing Verified-Prover/document ...
21:50:54 Finished Case_Labeling/document (0:00:03 elapsed time)
21:50:54 Preparing Case_Labeling/outline ...
21:50:54 Preparing GoedelGod/document ...
21:50:55 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Refinement_Lattice
21:50:55 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
21:50:55 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
21:50:55 Preparing FinFun/document ...
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunction
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Galois_Connections
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Parallel
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Infimum_Nat
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Sequential
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.CRA
21:50:56 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Sequential
21:50:56 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
21:50:56 Finished GoedelGod/document (0:00:01 elapsed time)
21:50:56 Preparing GoedelGod/outline ...
21:50:56 Preparing InformationFlowSlicing/document ...
21:50:57 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Iteration
21:50:57 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
21:50:57 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Iteration
21:50:57 Finished Case_Labeling/outline (0:00:03 elapsed time)
21:50:57 Finished LambdaMu/document (0:00:03 elapsed time)
21:50:57 Preparing LambdaMu/outline ...
21:50:58 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Rely_Quotient
21:50:58 Timing Case_Labeling (4 threads, 7.325s elapsed time, 21.301s cpu time, 0.645s GC time, factor 2.91)
21:50:58 Finished Case_Labeling (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.40)
21:50:58 Running SumSquares ...
21:50:58 Finished Matroids/document (0:00:04 elapsed time)
21:50:58 Preparing Matroids/outline ...
21:50:58 Finished GoedelGod/outline (0:00:01 elapsed time)
21:50:58 Finished Verified-Prover/document (0:00:04 elapsed time)
21:50:58 Preparing Verified-Prover/outline ...
21:50:59 Finished FinFun/document (0:00:03 elapsed time)
21:50:59 Preparing FinFun/outline ...
21:50:59 Timing GoedelGod (4 threads, 7.269s elapsed time, 8.083s cpu time, 0.089s GC time, factor 1.11)
21:50:59 Finished GoedelGod (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.05)
21:50:59 Running PAL ...
21:50:59 Preparing FOL_Seq_Calc1/document ...
21:51:00 PAL: theory PAL.PAL
21:51:01 Finished LambdaMu/outline (0:00:03 elapsed time)
21:51:01 Finished FinFun/outline (0:00:02 elapsed time)
21:51:01 Timing FinFun (4 threads, 6.890s elapsed time, 14.139s cpu time, 0.283s GC time, factor 2.05)
21:51:01 Finished FinFun (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.74)
21:51:01 Timing LambdaMu (4 threads, 8.014s elapsed time, 17.809s cpu time, 0.450s GC time, factor 2.22)
21:51:01 Finished LambdaMu (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.90)
21:51:01 Running MuchAdoAboutTwo ...
21:51:01 Running Noninterference_Inductive_Unwinding ...
21:51:01 Preparing Comparison_Sort_Lower_Bound/document ...
21:51:02 Finished Matroids/outline (0:00:03 elapsed time)
21:51:02 Finished Verified-Prover/outline (0:00:03 elapsed time)
21:51:02 Preparing Concurrent_Ref_Alg/document ...
21:51:02 Timing Matroids (4 threads, 5.056s elapsed time, 15.829s cpu time, 0.203s GC time, factor 3.13)
21:51:02 Finished Matroids (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.39)
21:51:02 Timing Verified-Prover (4 threads, 7.420s elapsed time, 18.136s cpu time, 0.394s GC time, factor 2.44)
21:51:02 Finished Verified-Prover (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.05)
21:51:02 Running Banach_Steinhaus ...
21:51:02 Running Tree_Decomposition ...
21:51:02 Finished InformationFlowSlicing/document (0:00:05 elapsed time)
21:51:02 Preparing InformationFlowSlicing/outline ...
21:51:03 SumSquares: theory SumSquares.FourSquares
21:51:03 SumSquares: theory SumSquares.TwoSquares
21:51:03 Finished FOL_Seq_Calc1/document (0:00:03 elapsed time)
21:51:03 Preparing FOL_Seq_Calc1/outline ...
21:51:03 Noninterference_Inductive_Unwinding: theory Noninterference_CSP.CSPNoninterference
21:51:03 Noninterference_Inductive_Unwinding: theory List_Interleaving.ListInterleaving
21:51:04 Tree_Decomposition: theory Tree_Decomposition.Graph
21:51:04 Tree_Decomposition: theory Tree_Decomposition.Tree
21:51:05 MuchAdoAboutTwo: theory HOL-Combinatorics.Transposition
21:51:05 Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
21:51:05 MuchAdoAboutTwo: theory HOL-Combinatorics.Permutations
21:51:05 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
21:51:05 Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
21:51:05 Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
21:51:05 Finished Comparison_Sort_Lower_Bound/document (0:00:03 elapsed time)
21:51:05 Preparing Comparison_Sort_Lower_Bound/outline ...
21:51:05 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
21:51:06 Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
21:51:06 Finished FOL_Seq_Calc1/outline (0:00:03 elapsed time)
21:51:06 Finished InformationFlowSlicing/outline (0:00:04 elapsed time)
21:51:06 Timing InformationFlowSlicing (4 threads, 6.525s elapsed time, 21.467s cpu time, 0.762s GC time, factor 3.29)
21:51:06 Finished InformationFlowSlicing (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.31)
21:51:06 Timing FOL_Seq_Calc1 (4 threads, 5.964s elapsed time, 18.103s cpu time, 0.310s GC time, factor 3.04)
21:51:06 Finished FOL_Seq_Calc1 (0:00:10 elapsed time, 0:00:22 cpu time, factor 2.18)
21:51:06 Running Ramsey-Infinite ...
21:51:06 Running Relational-Incorrectness-Logic ...
21:51:07 Finished Concurrent_Ref_Alg/document (0:00:04 elapsed time)
21:51:07 Preparing Concurrent_Ref_Alg/outline ...
21:51:07 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
21:51:07 MuchAdoAboutTwo: theory MuchAdoAboutTwo.MuchAdoAboutTwo
21:51:08 Preparing PAL/document ...
21:51:08 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
21:51:08 Ramsey-Infinite: theory HOL-Library.Infinite_Set
21:51:09 Noninterference_Inductive_Unwinding: theory Noninterference_Inductive_Unwinding.InductiveUnwinding
21:51:09 Finished Comparison_Sort_Lower_Bound/outline (0:00:03 elapsed time)
21:51:09 Ramsey-Infinite: theory Ramsey-Infinite.Ramsey
21:51:09 Timing Comparison_Sort_Lower_Bound (4 threads, 5.767s elapsed time, 18.140s cpu time, 0.532s GC time, factor 3.15)
21:51:09 Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:24 cpu time, factor 2.00)
21:51:09 Running Imperative_Insertion_Sort ...
21:51:10 Preparing SumSquares/document ...
21:51:11 Preparing Tree_Decomposition/document ...
21:51:11 Finished Concurrent_Ref_Alg/outline (0:00:04 elapsed time)
21:51:11 Timing Concurrent_Ref_Alg (4 threads, 6.244s elapsed time, 18.647s cpu time, 0.439s GC time, factor 2.99)
21:51:11 Finished Concurrent_Ref_Alg (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.36)
21:51:11 Running Binomial-Queues ...
21:51:11 Relational-Incorrectness-Logic: theory Relational-Incorrectness-Logic.RelationalIncorrectness
21:51:12 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
21:51:12 Finished PAL/document (0:00:03 elapsed time)
21:51:12 Preparing PAL/outline ...
21:51:12 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
21:51:12 Preparing MuchAdoAboutTwo/document ...
21:51:12 Preparing Banach_Steinhaus/document ...
21:51:13 Preparing Noninterference_Inductive_Unwinding/document ...
21:51:13 Binomial-Queues: theory Binomial-Queues.PQ
21:51:13 Binomial-Queues: theory Binomial-Queues.Binomial_Queue
21:51:14 Finished SumSquares/document (0:00:04 elapsed time)
21:51:14 Preparing SumSquares/outline ...
21:51:15 Preparing Ramsey-Infinite/document ...
21:51:15 Finished PAL/outline (0:00:03 elapsed time)
21:51:15 Binomial-Queues: theory Binomial-Queues.PQ_Implementation
21:51:16 Timing PAL (4 threads, 6.650s elapsed time, 22.046s cpu time, 0.401s GC time, factor 3.32)
21:51:16 Finished PAL (0:00:09 elapsed time, 0:00:24 cpu time, factor 2.66)
21:51:16 Running Stellar_Quorums ...
21:51:16 Finished Noninterference_Inductive_Unwinding/document (0:00:03 elapsed time)
21:51:16 Preparing Noninterference_Inductive_Unwinding/outline ...
21:51:16 Finished Tree_Decomposition/document (0:00:05 elapsed time)
21:51:16 Preparing Tree_Decomposition/outline ...
21:51:16 Finished MuchAdoAboutTwo/document (0:00:04 elapsed time)
21:51:16 Preparing MuchAdoAboutTwo/outline ...
21:51:17 Preparing Imperative_Insertion_Sort/document ...
21:51:17 Preparing Relational-Incorrectness-Logic/document ...
21:51:17 Finished Ramsey-Infinite/document (0:00:01 elapsed time)
21:51:17 Preparing Ramsey-Infinite/outline ...
21:51:17 Finished SumSquares/outline (0:00:02 elapsed time)
21:51:17 Finished Banach_Steinhaus/document (0:00:04 elapsed time)
21:51:17 Preparing Banach_Steinhaus/outline ...
21:51:17 Timing SumSquares (4 threads, 6.648s elapsed time, 20.413s cpu time, 0.357s GC time, factor 3.07)
21:51:17 Finished SumSquares (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.09)
21:51:17 Running FOL_Axiomatic ...
21:51:18 Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
21:51:19 Finished Ramsey-Infinite/outline (0:00:01 elapsed time)
21:51:19 Finished Imperative_Insertion_Sort/document (0:00:02 elapsed time)
21:51:19 Preparing Imperative_Insertion_Sort/outline ...
21:51:19 Timing Ramsey-Infinite (4 threads, 6.226s elapsed time, 11.601s cpu time, 0.131s GC time, factor 1.86)
21:51:19 Finished Ramsey-Infinite (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.58)
21:51:19 Running Tail_Recursive_Functions ...
21:51:19 FOL_Axiomatic: theory HOL-Library.Nat_Bijection
21:51:19 FOL_Axiomatic: theory HOL-Library.Old_Datatype
21:51:19 Finished Noninterference_Inductive_Unwinding/outline (0:00:03 elapsed time)
21:51:19 Timing Noninterference_Inductive_Unwinding (4 threads, 6.509s elapsed time, 23.170s cpu time, 0.782s GC time, factor 3.56)
21:51:19 Finished Noninterference_Inductive_Unwinding (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.38)
21:51:19 Running Dynamic_Tables ...
21:51:20 Finished MuchAdoAboutTwo/outline (0:00:03 elapsed time)
21:51:20 Preparing Binomial-Queues/document ...
21:51:20 FOL_Axiomatic: theory HOL-Library.Countable
21:51:20 Timing MuchAdoAboutTwo (4 threads, 6.333s elapsed time, 21.428s cpu time, 0.618s GC time, factor 3.38)
21:51:20 Finished MuchAdoAboutTwo (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.41)
21:51:20 Running Partial_Function_MR ...
21:51:20 Finished Banach_Steinhaus/outline (0:00:03 elapsed time)
21:51:20 Timing Banach_Steinhaus (4 threads, 6.211s elapsed time, 20.882s cpu time, 0.268s GC time, factor 3.36)
21:51:20 Finished Banach_Steinhaus (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.38)
21:51:20 Running ShortestPath ...
21:51:20 Finished Relational-Incorrectness-Logic/document (0:00:03 elapsed time)
21:51:20 Preparing Relational-Incorrectness-Logic/outline ...
21:51:21 Finished Imperative_Insertion_Sort/outline (0:00:01 elapsed time)
21:51:21 Finished Tree_Decomposition/outline (0:00:04 elapsed time)
21:51:21 Timing Imperative_Insertion_Sort (4 threads, 4.123s elapsed time, 13.320s cpu time, 0.164s GC time, factor 3.23)
21:51:21 Finished Imperative_Insertion_Sort (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.23)
21:51:21 Timing Tree_Decomposition (4 threads, 6.360s elapsed time, 19.699s cpu time, 0.408s GC time, factor 3.10)
21:51:21 Finished Tree_Decomposition (0:00:08 elapsed time, 0:00:21 cpu time, factor 2.48)
21:51:21 Running ArrowImpossibilityGS ...
21:51:21 Running Buffons_Needle ...
21:51:22 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
21:51:22 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
21:51:22 Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
21:51:22 Partial_Function_MR: theory HOL-Library.Monad_Syntax
21:51:22 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
21:51:22 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
21:51:22 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
21:51:22 Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
21:51:23 Finished Binomial-Queues/document (0:00:02 elapsed time)
21:51:23 Preparing Binomial-Queues/outline ...
21:51:23 ArrowImpossibilityGS: theory HOL-Library.FuncSet
21:51:23 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Utility
21:51:23 Dynamic_Tables: theory Dynamic_Tables.Tables_real
21:51:23 Preparing Stellar_Quorums/document ...
21:51:24 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Order
21:51:24 Finished Relational-Incorrectness-Logic/outline (0:00:03 elapsed time)
21:51:24 Timing Relational-Incorrectness-Logic (4 threads, 5.084s elapsed time, 14.138s cpu time, 0.279s GC time, factor 2.78)
21:51:24 Finished Relational-Incorrectness-Logic (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.85)
21:51:24 Running Topology ...
21:51:24 ShortestPath: theory ShortestPath.ShortestPath
21:51:24 ArrowImpossibilityGS: theory ArrowImpossibilityGS.GS
21:51:25 Dynamic_Tables: theory Dynamic_Tables.Tables_nat
21:51:25 Finished Binomial-Queues/outline (0:00:02 elapsed time)
21:51:25 Timing Binomial-Queues (4 threads, 6.206s elapsed time, 14.847s cpu time, 0.276s GC time, factor 2.39)
21:51:25 Finished Binomial-Queues (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.97)
21:51:25 Running HotelKeyCards ...
21:51:25 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
21:51:26 Preparing FOL_Axiomatic/document ...
21:51:26 ShortestPath: theory ShortestPath.ShortestPathNeg
21:51:27 HotelKeyCards: theory HOL-Library.LaTeXsugar
21:51:27 HotelKeyCards: theory HotelKeyCards.Notation
21:51:27 HotelKeyCards: theory HotelKeyCards.Basis
21:51:27 Finished Stellar_Quorums/document (0:00:03 elapsed time)
21:51:27 Preparing Stellar_Quorums/outline ...
21:51:27 HotelKeyCards: theory HotelKeyCards.Trace
21:51:27 HotelKeyCards: theory HotelKeyCards.State
21:51:27 HotelKeyCards: theory HotelKeyCards.NewCard
21:51:28 Preparing ArrowImpossibilityGS/document ...
21:51:28 HotelKeyCards: theory HotelKeyCards.Equivalence
21:51:28 Topology: theory Lazy-Lists-II.LList2
21:51:28 Topology: theory Topology.Topology
21:51:28 Preparing Tail_Recursive_Functions/document ...
21:51:29 Preparing Partial_Function_MR/document ...
21:51:29 Preparing Dynamic_Tables/document ...
21:51:30 Finished Stellar_Quorums/outline (0:00:03 elapsed time)
21:51:30 Preparing ShortestPath/document ...
21:51:31 Timing Stellar_Quorums (4 threads, 4.955s elapsed time, 17.343s cpu time, 0.338s GC time, factor 3.50)
21:51:31 Finished Stellar_Quorums (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.62)
21:51:31 Running Stewart_Apollonius ...
21:51:31 Topology: theory Topology.LList_Topology
21:51:31 Preparing Buffons_Needle/document ...
21:51:31 Finished FOL_Axiomatic/document (0:00:05 elapsed time)
21:51:31 Preparing FOL_Axiomatic/outline ...
21:51:31 Finished ArrowImpossibilityGS/document (0:00:03 elapsed time)
21:51:31 Preparing ArrowImpossibilityGS/outline ...
21:51:32 Finished Partial_Function_MR/document (0:00:03 elapsed time)
21:51:32 Preparing Partial_Function_MR/outline ...
21:51:33 Preparing HotelKeyCards/document ...
21:51:33 Finished Tail_Recursive_Functions/document (0:00:04 elapsed time)
21:51:33 Preparing Tail_Recursive_Functions/outline ...
21:51:33 Finished Dynamic_Tables/document (0:00:03 elapsed time)
21:51:33 Preparing Dynamic_Tables/outline ...
21:51:34 Finished ShortestPath/document (0:00:03 elapsed time)
21:51:34 Preparing ShortestPath/outline ...
21:51:34 Stewart_Apollonius: theory Triangle.Angles
21:51:34 Preparing Topology/document ...
21:51:34 Stewart_Apollonius: theory Triangle.Triangle
21:51:34 Finished ArrowImpossibilityGS/outline (0:00:02 elapsed time)
21:51:35 Timing ArrowImpossibilityGS (4 threads, 4.064s elapsed time, 15.618s cpu time, 0.480s GC time, factor 3.84)
21:51:35 Finished ArrowImpossibilityGS (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.76)
21:51:35 Running Falling_Factorial_Sum ...
21:51:35 Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
21:51:35 Finished FOL_Axiomatic/outline (0:00:04 elapsed time)
21:51:36 Timing FOL_Axiomatic (4 threads, 6.024s elapsed time, 14.374s cpu time, 0.344s GC time, factor 2.39)
21:51:36 Finished FOL_Axiomatic (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.96)
21:51:36 Running Source_Coding_Theorem ...
21:51:36 Finished Partial_Function_MR/outline (0:00:03 elapsed time)
21:51:36 Finished Dynamic_Tables/outline (0:00:02 elapsed time)
21:51:36 Finished Tail_Recursive_Functions/outline (0:00:03 elapsed time)
21:51:36 Timing Dynamic_Tables (4 threads, 5.070s elapsed time, 17.820s cpu time, 0.497s GC time, factor 3.51)
21:51:36 Finished Dynamic_Tables (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.30)
21:51:36 Timing Tail_Recursive_Functions (4 threads, 5.187s elapsed time, 12.120s cpu time, 0.373s GC time, factor 2.34)
21:51:36 Finished Tail_Recursive_Functions (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.70)
21:51:36 Timing Partial_Function_MR (4 threads, 6.139s elapsed time, 9.661s cpu time, 0.282s GC time, factor 1.57)
21:51:36 Finished Partial_Function_MR (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.38)
21:51:36 Running Combinatorics_Words_Lyndon ...
21:51:36 Running TortoiseHare ...
21:51:36 Running Lazy_Case ...
21:51:36 Finished HotelKeyCards/document (0:00:03 elapsed time)
21:51:36 Preparing HotelKeyCards/outline ...
21:51:36 Finished ShortestPath/outline (0:00:02 elapsed time)
21:51:37 Timing ShortestPath (4 threads, 5.562s elapsed time, 8.525s cpu time, 0.284s GC time, factor 1.53)
21:51:37 Finished ShortestPath (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.27)
21:51:37 Running DataRefinementIBP ...
21:51:38 Lazy_Case: theory Lazy_Case.Lazy_Case
21:51:38 Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
21:51:38 Finished Buffons_Needle/document (0:00:06 elapsed time)
21:51:38 Preparing Buffons_Needle/outline ...
21:51:38 Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
21:51:38 Lazy_Case: theory Lazy_Case.Test_Lazy_Case
21:51:38 DataRefinementIBP: theory LatticeProperties.WellFoundedTransitive
21:51:38 Falling_Factorial_Sum: theory Discrete_Summation.Factorials
21:51:38 Preparing Stewart_Apollonius/document ...
21:51:38 DataRefinementIBP: theory LatticeProperties.Conj_Disj
21:51:39 Finished Topology/document (0:00:04 elapsed time)
21:51:39 Preparing Topology/outline ...
21:51:39 DataRefinementIBP: theory LatticeProperties.Complete_Lattice_Prop
21:51:39 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
21:51:39 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
21:51:39 Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
21:51:39 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
21:51:39 Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
21:51:39 TortoiseHare: theory TortoiseHare.Basis
21:51:39 DataRefinementIBP: theory DataRefinementIBP.Preliminaries
21:51:39 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
21:51:40 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
21:51:40 Finished HotelKeyCards/outline (0:00:03 elapsed time)
21:51:40 Timing HotelKeyCards (4 threads, 4.951s elapsed time, 15.030s cpu time, 0.337s GC time, factor 3.04)
21:51:40 Finished HotelKeyCards (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.30)
21:51:40 Running Secondary_Sylow ...
21:51:40 DataRefinementIBP: theory DataRefinementIBP.Statements
21:51:40 DataRefinementIBP: theory DataRefinementIBP.Hoare
21:51:40 TortoiseHare: theory TortoiseHare.Brent
21:51:40 TortoiseHare: theory TortoiseHare.TortoiseHare
21:51:40 DataRefinementIBP: theory DataRefinementIBP.Diagram
21:51:41 DataRefinementIBP: theory DataRefinementIBP.DataRefinement
21:51:41 Finished Stewart_Apollonius/document (0:00:02 elapsed time)
21:51:41 Preparing Stewart_Apollonius/outline ...
21:51:43 Preparing Lazy_Case/document ...
21:51:43 Preparing DataRefinementIBP/document ...
21:51:43 Finished Topology/outline (0:00:04 elapsed time)
21:51:43 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
21:51:43 Timing Topology (4 threads, 4.643s elapsed time, 17.431s cpu time, 0.933s GC time, factor 3.75)
21:51:43 Finished Topology (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.27)
21:51:43 Running Goodstein_Lambda ...
21:51:44 Preparing Falling_Factorial_Sum/document ...
21:51:44 Finished Stewart_Apollonius/outline (0:00:02 elapsed time)
21:51:44 Timing Stewart_Apollonius (4 threads, 3.945s elapsed time, 7.346s cpu time, 0.146s GC time, factor 1.86)
21:51:44 Finished Stewart_Apollonius (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.40)
21:51:44 Running Certification_Monads ...
21:51:44 Finished Lazy_Case/document (0:00:01 elapsed time)
21:51:44 Preparing Lazy_Case/outline ...
21:51:44 Finished Buffons_Needle/outline (0:00:06 elapsed time)
21:51:45 Preparing TortoiseHare/document ...
21:51:45 Preparing Source_Coding_Theorem/document ...
21:51:45 Timing Buffons_Needle (4 threads, 5.060s elapsed time, 15.463s cpu time, 0.105s GC time, factor 3.06)
21:51:45 Finished Buffons_Needle (0:00:10 elapsed time, 0:00:20 cpu time, factor 2.01)
21:51:45 Running Chord_Segments ...
21:51:45 Preparing Combinatorics_Words_Lyndon/document ...
21:51:45 Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
21:51:46 Certification_Monads: theory Certification_Monads.Misc
21:51:46 Certification_Monads: theory Deriving.Generator_Aux
21:51:46 Certification_Monads: theory Deriving.Derive_Manager
21:51:46 Certification_Monads: theory HOL-Library.Adhoc_Overloading
21:51:46 Finished Lazy_Case/outline (0:00:01 elapsed time)
21:51:46 Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
21:51:46 Finished DataRefinementIBP/document (0:00:03 elapsed time)
21:51:46 Preparing DataRefinementIBP/outline ...
21:51:46 Certification_Monads: theory Certification_Monads.Error_Syntax
21:51:46 Certification_Monads: theory HOL-Library.Monad_Syntax
21:51:46 Certification_Monads: theory Certification_Monads.Error_Monad
21:51:46 Timing Lazy_Case (4 threads, 4.138s elapsed time, 6.545s cpu time, 0.365s GC time, factor 1.58)
21:51:46 Finished Lazy_Case (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.32)
21:51:46 Running Triangle ...
21:51:46 Certification_Monads: theory Show.Show
21:51:47 Certification_Monads: theory Certification_Monads.Strict_Sum
21:51:47 Finished Falling_Factorial_Sum/document (0:00:03 elapsed time)
21:51:47 Preparing Falling_Factorial_Sum/outline ...
21:51:47 Secondary_Sylow: theory Secondary_Sylow.GroupAction
21:51:48 Chord_Segments: theory Triangle.Angles
21:51:48 Finished Source_Coding_Theorem/document (0:00:03 elapsed time)
21:51:48 Preparing Source_Coding_Theorem/outline ...
21:51:48 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
21:51:48 Finished TortoiseHare/document (0:00:03 elapsed time)
21:51:48 Preparing TortoiseHare/outline ...
21:51:48 Certification_Monads: theory Certification_Monads.Check_Monad
21:51:48 Certification_Monads: theory Certification_Monads.Parser_Monad
21:51:48 Chord_Segments: theory Triangle.Triangle
21:51:49 Secondary_Sylow: theory Secondary_Sylow.SndSylow
21:51:49 Chord_Segments: theory Chord_Segments.Chord_Segments
21:51:49 Preparing Goodstein_Lambda/document ...
21:51:50 Finished DataRefinementIBP/outline (0:00:03 elapsed time)
21:51:50 Timing DataRefinementIBP (4 threads, 3.613s elapsed time, 8.027s cpu time, 0.182s GC time, factor 2.22)
21:51:50 Finished DataRefinementIBP (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.70)
21:51:50 Running Stuttering_Equivalence ...
21:51:50 Triangle: theory Triangle.Angles
21:51:50 Finished Falling_Factorial_Sum/outline (0:00:03 elapsed time)
21:51:50 Triangle: theory Triangle.Triangle
21:51:50 Timing Falling_Factorial_Sum (4 threads, 4.828s elapsed time, 15.450s cpu time, 0.291s GC time, factor 3.20)
21:51:50 Finished Falling_Factorial_Sum (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.17)
21:51:50 Running LatticeProperties ...
21:51:51 Preparing Certification_Monads/document ...
21:51:51 Finished Source_Coding_Theorem/outline (0:00:03 elapsed time)
21:51:52 Finished Combinatorics_Words_Lyndon/document (0:00:06 elapsed time)
21:51:52 Preparing Combinatorics_Words_Lyndon/outline ...
21:51:52 Finished TortoiseHare/outline (0:00:03 elapsed time)
21:51:52 Timing Source_Coding_Theorem (4 threads, 4.250s elapsed time, 11.431s cpu time, 0.151s GC time, factor 2.69)
21:51:52 Finished Source_Coding_Theorem (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.77)
21:51:52 Timing TortoiseHare (4 threads, 4.365s elapsed time, 11.879s cpu time, 0.223s GC time, factor 2.72)
21:51:52 Finished TortoiseHare (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.86)
21:51:52 Running GaleStewart_Games ...
21:51:52 Running VeriComp ...
21:51:52 LatticeProperties: theory LatticeProperties.Conj_Disj
21:51:52 LatticeProperties: theory LatticeProperties.WellFoundedTransitive
21:51:52 LatticeProperties: theory LatticeProperties.Lattice_Prop
21:51:52 Preparing Secondary_Sylow/document ...
21:51:52 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice
21:51:53 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop
21:51:53 Preparing Chord_Segments/document ...
21:51:53 Finished Goodstein_Lambda/document (0:00:03 elapsed time)
21:51:53 Preparing Goodstein_Lambda/outline ...
21:51:53 Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
21:51:53 Finished Certification_Monads/document (0:00:02 elapsed time)
21:51:53 Preparing Certification_Monads/outline ...
21:51:53 VeriComp: theory VeriComp.Behaviour
21:51:53 VeriComp: theory VeriComp.Transfer_Extras
21:51:53 VeriComp: theory VeriComp.Well_founded
21:51:54 VeriComp: theory VeriComp.Inf
21:51:54 Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
21:51:54 Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
21:51:54 GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
21:51:54 Preparing Triangle/document ...
21:51:54 GaleStewart_Games: theory GaleStewart_Games.MoreENat
21:51:54 GaleStewart_Games: theory GaleStewart_Games.MorePrefix
21:51:54 VeriComp: theory VeriComp.Semantics
21:51:55 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group
21:51:55 VeriComp: theory VeriComp.Language
21:51:55 VeriComp: theory VeriComp.Simulation
21:51:55 GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
21:51:55 Finished Secondary_Sylow/document (0:00:03 elapsed time)
21:51:55 Preparing Secondary_Sylow/outline ...
21:51:56 GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
21:51:56 Finished Certification_Monads/outline (0:00:02 elapsed time)
21:51:56 VeriComp: theory VeriComp.Compiler
21:51:56 Timing Certification_Monads (4 threads, 4.121s elapsed time, 12.893s cpu time, 0.431s GC time, factor 3.13)
21:51:56 Finished Certification_Monads (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.29)
21:51:56 Running Public_Announcement_Logic ...
21:51:56 VeriComp: theory VeriComp.Fixpoint
21:51:56 Finished Chord_Segments/document (0:00:03 elapsed time)
21:51:56 Preparing Chord_Segments/outline ...
21:51:56 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
21:51:56 Finished Triangle/document (0:00:02 elapsed time)
21:51:56 Preparing Triangle/outline ...
21:51:56 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
21:51:57 Preparing LatticeProperties/document ...
21:51:57 Finished Goodstein_Lambda/outline (0:00:03 elapsed time)
21:51:57 Timing Goodstein_Lambda (4 threads, 3.820s elapsed time, 9.522s cpu time, 0.208s GC time, factor 2.49)
21:51:57 Finished Goodstein_Lambda (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.88)
21:51:57 Running Category ...
21:51:57 Finished Combinatorics_Words_Lyndon/outline (0:00:05 elapsed time)
21:51:57 Preparing Stuttering_Equivalence/document ...
21:51:57 Timing Combinatorics_Words_Lyndon (4 threads, 4.480s elapsed time, 16.902s cpu time, 0.403s GC time, factor 3.77)
21:51:57 Finished Combinatorics_Words_Lyndon (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.43)
21:51:57 Running Sunflowers ...
21:51:58 Finished Secondary_Sylow/outline (0:00:02 elapsed time)
21:51:58 Preparing VeriComp/document ...
21:51:58 Timing Secondary_Sylow (4 threads, 4.375s elapsed time, 14.301s cpu time, 0.505s GC time, factor 3.27)
21:51:58 Finished Secondary_Sylow (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.77)
21:51:58 Running Compiling-Exceptions-Correctly ...
21:51:58 Finished Triangle/outline (0:00:01 elapsed time)
21:51:59 Category: theory HOL-Library.FuncSet
21:51:59 Timing Triangle (4 threads, 4.031s elapsed time, 7.074s cpu time, 0.184s GC time, factor 1.75)
21:51:59 Finished Triangle (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.34)
21:51:59 Running Transitive-Closure ...
21:51:59 Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
21:51:59 Preparing GaleStewart_Games/document ...
21:51:59 Sunflowers: theory HOL-Library.FuncSet
21:51:59 Category: theory Category.Cat
21:52:00 Finished Chord_Segments/outline (0:00:03 elapsed time)
21:52:00 Compiling-Exceptions-Correctly: theory Compiling-Exceptions-Correctly.Exceptions
21:52:00 Timing Chord_Segments (4 threads, 4.038s elapsed time, 9.062s cpu time, 0.156s GC time, factor 2.24)
21:52:00 Finished Chord_Segments (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.61)
21:52:00 Running GenClock ...
21:52:00 Sunflowers: theory Sunflowers.Sunflower
21:52:00 Category: theory Category.Functors
21:52:00 Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
21:52:00 Category: theory Category.SetCat
21:52:01 Finished LatticeProperties/document (0:00:03 elapsed time)
21:52:01 Preparing LatticeProperties/outline ...
21:52:01 Category: theory Category.NatTrans
21:52:01 Category: theory Category.HomFunctors
21:52:01 Category: theory Category.Yoneda
21:52:01 Finished Stuttering_Equivalence/document (0:00:04 elapsed time)
21:52:01 Preparing Stuttering_Equivalence/outline ...
21:52:02 Finished VeriComp/document (0:00:03 elapsed time)
21:52:02 Preparing VeriComp/outline ...
21:52:02 GenClock: theory GenClock.GenClock
21:52:03 Transitive-Closure: theory Matrix.Utility
21:52:03 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
21:52:03 Preparing Category/document ...
21:52:04 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
21:52:04 Preparing Sunflowers/document ...
21:52:04 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
21:52:04 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
21:52:04 Finished LatticeProperties/outline (0:00:03 elapsed time)
21:52:04 Preparing Compiling-Exceptions-Correctly/document ...
21:52:04 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
21:52:04 Preparing Public_Announcement_Logic/document ...
21:52:04 Finished GaleStewart_Games/document (0:00:05 elapsed time)
21:52:04 Preparing GaleStewart_Games/outline ...
21:52:04 Timing LatticeProperties (4 threads, 3.974s elapsed time, 8.419s cpu time, 0.182s GC time, factor 2.12)
21:52:04 Finished LatticeProperties (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.65)
21:52:04 Running CYK ...
21:52:05 Finished Stuttering_Equivalence/outline (0:00:03 elapsed time)
21:52:05 Finished VeriComp/outline (0:00:03 elapsed time)
21:52:05 Timing VeriComp (4 threads, 3.658s elapsed time, 8.591s cpu time, 0.247s GC time, factor 2.35)
21:52:05 Finished VeriComp (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.79)
21:52:05 Timing Stuttering_Equivalence (4 threads, 3.024s elapsed time, 8.866s cpu time, 0.204s GC time, factor 2.93)
21:52:05 Finished Stuttering_Equivalence (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.75)
21:52:05 Running C2KA_DistributedSystems ...
21:52:05 Running Szpilrajn ...
21:52:05 Preparing GenClock/document ...
21:52:06 CYK: theory CYK.CYK
21:52:07 Szpilrajn: theory Szpilrajn.Szpilrajn
21:52:07 C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
21:52:07 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
21:52:07 Finished Compiling-Exceptions-Correctly/document (0:00:02 elapsed time)
21:52:07 Preparing Compiling-Exceptions-Correctly/outline ...
21:52:07 Finished Sunflowers/document (0:00:03 elapsed time)
21:52:07 Preparing Sunflowers/outline ...
21:52:07 Preparing Transitive-Closure/document ...
21:52:07 Finished Public_Announcement_Logic/document (0:00:03 elapsed time)
21:52:07 Preparing Public_Announcement_Logic/outline ...
21:52:08 Finished Category/document (0:00:04 elapsed time)
21:52:08 Preparing Category/outline ...
21:52:08 Finished GaleStewart_Games/outline (0:00:03 elapsed time)
21:52:08 Timing GaleStewart_Games (4 threads, 3.951s elapsed time, 12.769s cpu time, 0.224s GC time, factor 3.23)
21:52:08 Finished GaleStewart_Games (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.17)
21:52:08 Running DPT-SAT-Solver ...
21:52:09 C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
21:52:09 Finished GenClock/document (0:00:03 elapsed time)
21:52:09 Preparing GenClock/outline ...
21:52:09 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
21:52:09 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
21:52:09 Finished Compiling-Exceptions-Correctly/outline (0:00:02 elapsed time)
21:52:10 Timing Compiling-Exceptions-Correctly (4 threads, 3.934s elapsed time, 6.951s cpu time, 0.356s GC time, factor 1.77)
21:52:10 Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.43)
21:52:10 Running Discrete_Summation ...
21:52:10 Finished Sunflowers/outline (0:00:03 elapsed time)
21:52:10 Preparing Szpilrajn/document ...
21:52:10 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Solver
21:52:10 Preparing C2KA_DistributedSystems/document ...
21:52:10 Timing Sunflowers (4 threads, 3.653s elapsed time, 11.431s cpu time, 0.158s GC time, factor 3.13)
21:52:10 Finished Sunflowers (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.22)
21:52:10 Running Mason_Stothers ...
21:52:10 Preparing CYK/document ...
21:52:11 Finished Public_Announcement_Logic/outline (0:00:03 elapsed time)
21:52:11 Finished Transitive-Closure/document (0:00:03 elapsed time)
21:52:11 Preparing Transitive-Closure/outline ...
21:52:11 Finished Category/outline (0:00:03 elapsed time)
21:52:11 Timing Public_Announcement_Logic (4 threads, 4.420s elapsed time, 8.842s cpu time, 0.416s GC time, factor 2.00)
21:52:11 Finished Public_Announcement_Logic (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.49)
21:52:11 Timing Category (4 threads, 4.022s elapsed time, 12.542s cpu time, 0.195s GC time, factor 3.12)
21:52:11 Finished Category (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.27)
21:52:11 Running Lifting_Definition_Option ...
21:52:11 Running Marriage ...
21:52:12 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Tests
21:52:12 Discrete_Summation: theory Discrete_Summation.Discrete_Summation
21:52:12 Discrete_Summation: theory HOL-Combinatorics.Stirling
21:52:12 Finished GenClock/outline (0:00:03 elapsed time)
21:52:12 Timing GenClock (4 threads, 2.715s elapsed time, 9.346s cpu time, 0.156s GC time, factor 3.44)
21:52:12 Finished GenClock (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.30)
21:52:12 Running Gauss-Jordan-Elim-Fun ...
21:52:12 Discrete_Summation: theory Discrete_Summation.Factorials
21:52:13 Discrete_Summation: theory Discrete_Summation.Summation_Conversion
21:52:13 Marriage: theory Marriage.Marriage
21:52:13 Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
21:52:13 Discrete_Summation: theory Discrete_Summation.Examples
21:52:14 Finished Szpilrajn/document (0:00:03 elapsed time)
21:52:14 Preparing Szpilrajn/outline ...
21:52:14 Gauss-Jordan-Elim-Fun: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
21:52:14 Preparing DPT-SAT-Solver/document ...
21:52:14 Finished Transitive-Closure/outline (0:00:03 elapsed time)
21:52:14 Mason_Stothers: theory Mason_Stothers.Mason_Stothers
21:52:14 Finished CYK/document (0:00:03 elapsed time)
21:52:14 Preparing CYK/outline ...
21:52:14 Finished C2KA_DistributedSystems/document (0:00:03 elapsed time)
21:52:14 Preparing C2KA_DistributedSystems/outline ...
21:52:14 Timing Transitive-Closure (4 threads, 3.427s elapsed time, 10.396s cpu time, 0.251s GC time, factor 3.03)
21:52:14 Finished Transitive-Closure (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.83)
21:52:14 Running Fresh_Identifiers ...
21:52:15 Preparing Discrete_Summation/document ...
21:52:15 Preparing Marriage/document ...
21:52:16 Finished DPT-SAT-Solver/document (0:00:01 elapsed time)
21:52:16 Preparing DPT-SAT-Solver/outline ...
21:52:16 Preparing Lifting_Definition_Option/document ...
21:52:16 Fresh_Identifiers: theory Fresh_Identifiers.Fresh
21:52:17 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
21:52:17 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
21:52:17 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
21:52:17 Finished Szpilrajn/outline (0:00:02 elapsed time)
21:52:17 Finished Discrete_Summation/document (0:00:02 elapsed time)
21:52:17 Preparing Discrete_Summation/outline ...
21:52:17 Preparing Gauss-Jordan-Elim-Fun/document ...
21:52:17 Timing Szpilrajn (4 threads, 2.910s elapsed time, 7.671s cpu time, 0.118s GC time, factor 2.64)
21:52:17 Finished Szpilrajn (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.88)
21:52:17 Running List_Interleaving ...
21:52:17 Finished CYK/outline (0:00:03 elapsed time)
21:52:17 Timing CYK (4 threads, 3.584s elapsed time, 10.399s cpu time, 0.261s GC time, factor 2.90)
21:52:17 Finished CYK (0:00:05 elapsed time, 0:00:12 cpu time, factor 2.09)
21:52:17 Running Mereology ...
21:52:18 Finished DPT-SAT-Solver/outline (0:00:01 elapsed time)
21:52:18 Finished C2KA_DistributedSystems/outline (0:00:03 elapsed time)
21:52:18 Finished Marriage/document (0:00:02 elapsed time)
21:52:18 Preparing Marriage/outline ...
21:52:18 Preparing Mason_Stothers/document ...
21:52:18 Timing C2KA_DistributedSystems (4 threads, 3.299s elapsed time, 5.239s cpu time, 0.175s GC time, factor 1.59)
21:52:18 Finished C2KA_DistributedSystems (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.32)
21:52:18 Timing DPT-SAT-Solver (4 threads, 3.198s elapsed time, 6.536s cpu time, 0.056s GC time, factor 2.04)
21:52:18 Finished DPT-SAT-Solver (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.55)
21:52:18 Running Fisher_Yates ...
21:52:18 Running BinarySearchTree ...
21:52:19 Finished Discrete_Summation/outline (0:00:01 elapsed time)
21:52:19 Finished Gauss-Jordan-Elim-Fun/document (0:00:01 elapsed time)
21:52:19 Preparing Gauss-Jordan-Elim-Fun/outline ...
21:52:19 List_Interleaving: theory List_Interleaving.ListInterleaving
21:52:19 Finished Lifting_Definition_Option/document (0:00:02 elapsed time)
21:52:19 Preparing Lifting_Definition_Option/outline ...
21:52:19 Timing Discrete_Summation (4 threads, 2.461s elapsed time, 9.178s cpu time, 0.141s GC time, factor 3.73)
21:52:19 Finished Discrete_Summation (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.41)
21:52:19 Running Card_Number_Partitions ...
21:52:19 Mereology: theory Mereology.PM
21:52:19 Mereology: theory Mereology.M
21:52:20 Mereology: theory Mereology.CM
21:52:20 Mereology: theory Mereology.MM
21:52:20 Preparing Fresh_Identifiers/document ...
21:52:20 BinarySearchTree: theory BinarySearchTree.BinaryTree_TacticStyle
21:52:20 BinarySearchTree: theory BinarySearchTree.BinaryTree
21:52:20 Mereology: theory Mereology.EM
21:52:20 Mereology: theory Mereology.GM
21:52:20 Mereology: theory Mereology.CEM
21:52:20 Mereology: theory Mereology.GMM
21:52:20 Finished Marriage/outline (0:00:02 elapsed time)
21:52:20 Finished Gauss-Jordan-Elim-Fun/outline (0:00:01 elapsed time)
21:52:21 Timing Gauss-Jordan-Elim-Fun (4 threads, 2.558s elapsed time, 6.745s cpu time, 0.108s GC time, factor 2.64)
21:52:21 Finished Gauss-Jordan-Elim-Fun (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.80)
21:52:21 Timing Marriage (4 threads, 1.626s elapsed time, 5.382s cpu time, 0.092s GC time, factor 3.31)
21:52:21 Finished Marriage (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.89)
21:52:21 Running List-Index ...
21:52:21 Running Descartes_Sign_Rule ...
21:52:21 Finished Mason_Stothers/document (0:00:03 elapsed time)
21:52:21 Preparing Mason_Stothers/outline ...
21:52:21 Mereology: theory Mereology.GEM
21:52:21 BinarySearchTree: theory BinarySearchTree.BinaryTree_Map
21:52:22 Finished Fresh_Identifiers/document (0:00:02 elapsed time)
21:52:22 Preparing Fresh_Identifiers/outline ...
21:52:22 Finished Lifting_Definition_Option/outline (0:00:03 elapsed time)
21:52:22 Timing Lifting_Definition_Option (4 threads, 2.731s elapsed time, 3.383s cpu time, 0.000s GC time, factor 1.24)
21:52:22 Finished Lifting_Definition_Option (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.07)
21:52:22 Running Pairing_Heap ...
21:52:22 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
21:52:22 Preparing List_Interleaving/document ...
21:52:22 List-Index: theory List-Index.List_Index
21:52:23 Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
21:52:23 Preparing BinarySearchTree/document ...
21:52:23 Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
21:52:23 Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
21:52:24 Finished Fresh_Identifiers/outline (0:00:02 elapsed time)
21:52:24 Preparing Mereology/document ...
21:52:24 Finished Mason_Stothers/outline (0:00:02 elapsed time)
21:52:24 Timing Fresh_Identifiers (4 threads, 2.901s elapsed time, 6.909s cpu time, 0.134s GC time, factor 2.38)
21:52:24 Finished Fresh_Identifiers (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.72)
21:52:24 Timing Mason_Stothers (4 threads, 3.020s elapsed time, 7.144s cpu time, 0.140s GC time, factor 2.37)
21:52:24 Finished Mason_Stothers (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.53)
21:52:24 Running Surprise_Paradox ...
21:52:24 Running Lucas_Theorem ...
21:52:24 Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
21:52:25 Preparing List-Index/document ...
21:52:25 Finished BinarySearchTree/document (0:00:02 elapsed time)
21:52:25 Preparing BinarySearchTree/outline ...
21:52:25 Pairing_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
21:52:26 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List1
21:52:26 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List2
21:52:26 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_Tree
21:52:26 Preparing Fisher_Yates/document ...
21:52:26 Preparing Card_Number_Partitions/document ...
21:52:27 Finished List_Interleaving/document (0:00:04 elapsed time)
21:52:27 Preparing List_Interleaving/outline ...
21:52:27 Preparing Descartes_Sign_Rule/document ...
21:52:27 Finished List-Index/document (0:00:02 elapsed time)
21:52:27 Preparing List-Index/outline ...
21:52:27 Finished BinarySearchTree/outline (0:00:01 elapsed time)
21:52:28 Timing BinarySearchTree (4 threads, 2.425s elapsed time, 8.188s cpu time, 0.254s GC time, factor 3.38)
21:52:28 Finished BinarySearchTree (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.17)
21:52:28 Running Cartan_FP ...
21:52:28 Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
21:52:28 Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem
21:52:28 Preparing Pairing_Heap/document ...
21:52:29 Finished Fisher_Yates/document (0:00:03 elapsed time)
21:52:29 Preparing Fisher_Yates/outline ...
21:52:29 Finished List-Index/outline (0:00:01 elapsed time)
21:52:30 Timing List-Index (4 threads, 2.064s elapsed time, 7.144s cpu time, 0.118s GC time, factor 3.46)
21:52:30 Finished List-Index (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.07)
21:52:30 Running ClockSynchInst ...
21:52:30 Finished List_Interleaving/outline (0:00:03 elapsed time)
21:52:30 Finished Card_Number_Partitions/document (0:00:03 elapsed time)
21:52:30 Preparing Card_Number_Partitions/outline ...
21:52:30 Preparing Lucas_Theorem/document ...
21:52:30 Timing List_Interleaving (4 threads, 2.767s elapsed time, 7.570s cpu time, 0.276s GC time, factor 2.74)
21:52:30 Finished List_Interleaving (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.89)
21:52:30 Running Max-Card-Matching ...
21:52:31 Preparing Surprise_Paradox/document ...
21:52:31 Finished Mereology/document (0:00:06 elapsed time)
21:52:31 Preparing Mereology/outline ...
21:52:31 Finished Descartes_Sign_Rule/document (0:00:03 elapsed time)
21:52:31 Preparing Descartes_Sign_Rule/outline ...
21:52:31 Cartan_FP: theory Cartan_FP.Cartan
21:52:31 ClockSynchInst: theory ClockSynchInst.ICAInstance
21:52:31 ClockSynchInst: theory ClockSynchInst.LynchInstance
21:52:32 Finished Fisher_Yates/outline (0:00:02 elapsed time)
21:52:32 Finished Pairing_Heap/document (0:00:03 elapsed time)
21:52:32 Preparing Pairing_Heap/outline ...
21:52:32 Timing Fisher_Yates (4 threads, 2.875s elapsed time, 8.441s cpu time, 0.150s GC time, factor 2.94)
21:52:32 Finished Fisher_Yates (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.70)
21:52:32 Running Perfect-Number-Thm ...
21:52:32 Max-Card-Matching: theory Max-Card-Matching.Matching
21:52:33 Finished Card_Number_Partitions/outline (0:00:02 elapsed time)
21:52:33 Timing Card_Number_Partitions (4 threads, 2.579s elapsed time, 9.176s cpu time, 0.119s GC time, factor 3.56)
21:52:33 Finished Card_Number_Partitions (0:00:06 elapsed time, 0:00:13 cpu time, factor 1.91)
21:52:33 Running Lazy-Lists-II ...
21:52:33 Preparing Cartan_FP/document ...
21:52:33 Finished Lucas_Theorem/document (0:00:03 elapsed time)
21:52:33 Preparing Lucas_Theorem/outline ...
21:52:34 Finished Descartes_Sign_Rule/outline (0:00:03 elapsed time)
21:52:34 Finished Surprise_Paradox/document (0:00:03 elapsed time)
21:52:34 Preparing Surprise_Paradox/outline ...
21:52:34 Preparing Max-Card-Matching/document ...
21:52:34 Timing Descartes_Sign_Rule (4 threads, 2.082s elapsed time, 7.301s cpu time, 0.117s GC time, factor 3.51)
21:52:34 Finished Descartes_Sign_Rule (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.76)
21:52:34 Running Skew_Heap ...
21:52:34 Preparing ClockSynchInst/document ...
21:52:34 Finished Mereology/outline (0:00:03 elapsed time)
21:52:35 Finished Pairing_Heap/outline (0:00:03 elapsed time)
21:52:35 Timing Mereology (4 threads, 2.668s elapsed time, 8.284s cpu time, 0.431s GC time, factor 3.10)
21:52:35 Finished Mereology (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.77)
21:52:35 Timing Pairing_Heap (4 threads, 2.462s elapsed time, 8.441s cpu time, 0.396s GC time, factor 3.43)
21:52:35 Finished Pairing_Heap (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.89)
21:52:35 Running Open_Induction ...
21:52:35 Running Combinatorics_Words_Graph_Lemma ...
21:52:36 Finished Lucas_Theorem/outline (0:00:02 elapsed time)
21:52:36 Timing Lucas_Theorem (4 threads, 1.629s elapsed time, 5.398s cpu time, 0.110s GC time, factor 3.31)
21:52:36 Finished Lucas_Theorem (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.60)
21:52:36 Running Lifting_the_Exponent ...
21:52:36 Finished Cartan_FP/document (0:00:03 elapsed time)
21:52:36 Preparing Cartan_FP/outline ...
21:52:36 Open_Induction: theory Open_Induction.Restricted_Predicates
21:52:37 Finished Max-Card-Matching/document (0:00:03 elapsed time)
21:52:37 Preparing Max-Card-Matching/outline ...
21:52:37 Finished Surprise_Paradox/outline (0:00:03 elapsed time)
21:52:37 Open_Induction: theory Open_Induction.Open_Induction
21:52:37 Timing Surprise_Paradox (4 threads, 2.266s elapsed time, 3.991s cpu time, 0.000s GC time, factor 1.76)
21:52:37 Finished Surprise_Paradox (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.22)
21:52:37 Running Blue_Eyes ...
21:52:37 Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
21:52:37 Skew_Heap: theory HOL-Data_Structures.Heaps
21:52:37 Lazy-Lists-II: theory Lazy-Lists-II.LList2
21:52:38 Skew_Heap: theory Skew_Heap.Skew_Heap
21:52:38 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
21:52:38 Finished ClockSynchInst/document (0:00:04 elapsed time)
21:52:38 Preparing ClockSynchInst/outline ...
21:52:39 Preparing Open_Induction/document ...
21:52:39 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
21:52:39 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
21:52:39 Blue_Eyes: theory Blue_Eyes.Blue_Eyes
21:52:39 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
21:52:39 Finished Cartan_FP/outline (0:00:02 elapsed time)
21:52:40 Timing Cartan_FP (4 threads, 1.515s elapsed time, 5.195s cpu time, 0.135s GC time, factor 3.43)
21:52:40 Finished Cartan_FP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.62)
21:52:40 Running AnselmGod ...
21:52:40 Preparing Skew_Heap/document ...
21:52:40 Finished Max-Card-Matching/outline (0:00:03 elapsed time)
21:52:40 Preparing Combinatorics_Words_Graph_Lemma/document ...
21:52:40 Preparing Lazy-Lists-II/document ...
21:52:40 Timing Max-Card-Matching (4 threads, 1.453s elapsed time, 3.987s cpu time, 0.000s GC time, factor 2.74)
21:52:40 Finished Max-Card-Matching (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.63)
21:52:40 Running RIPEMD-160-SPARK ...
21:52:41 Preparing Blue_Eyes/document ...
21:52:41 Preparing Perfect-Number-Thm/document ...
21:52:41 Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
21:52:42 Finished ClockSynchInst/outline (0:00:03 elapsed time)
21:52:42 AnselmGod: theory AnselmGod.AnselmGod
21:52:42 Timing ClockSynchInst (4 threads, 2.308s elapsed time, 8.176s cpu time, 0.149s GC time, factor 3.54)
21:52:42 Finished ClockSynchInst (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.28)
21:52:42 Running Liouville_Numbers ...
21:52:42 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
21:52:42 Finished Open_Induction/document (0:00:03 elapsed time)
21:52:42 Preparing Open_Induction/outline ...
21:52:43 Finished Skew_Heap/document (0:00:02 elapsed time)
21:52:43 Preparing Skew_Heap/outline ...
21:52:43 Preparing AnselmGod/document ...
21:52:43 Preparing Lifting_the_Exponent/document ...
21:52:44 Finished Lazy-Lists-II/document (0:00:03 elapsed time)
21:52:44 Preparing Lazy-Lists-II/outline ...
21:52:44 Finished Perfect-Number-Thm/document (0:00:02 elapsed time)
21:52:44 Preparing Perfect-Number-Thm/outline ...
21:52:44 Preparing RIPEMD-160-SPARK/document ...
21:52:44 Finished Blue_Eyes/document (0:00:03 elapsed time)
21:52:44 Preparing Blue_Eyes/outline ...
21:52:45 Finished Skew_Heap/outline (0:00:02 elapsed time)
21:52:45 Timing Skew_Heap (4 threads, 1.883s elapsed time, 2.847s cpu time, 0.000s GC time, factor 1.51)
21:52:45 Finished Skew_Heap (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.12)
21:52:45 Running Minkowskis_Theorem ...
21:52:45 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
21:52:45 Finished Combinatorics_Words_Graph_Lemma/document (0:00:05 elapsed time)
21:52:45 Preparing Combinatorics_Words_Graph_Lemma/outline ...
21:52:46 Finished Open_Induction/outline (0:00:03 elapsed time)
21:52:46 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
21:52:46 Timing Open_Induction (4 threads, 1.663s elapsed time, 5.315s cpu time, 0.169s GC time, factor 3.20)
21:52:46 Finished Open_Induction (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.83)
21:52:46 Running FunWithFunctions ...
21:52:46 Finished AnselmGod/document (0:00:02 elapsed time)
21:52:46 Preparing AnselmGod/outline ...
21:52:46 Finished RIPEMD-160-SPARK/document (0:00:02 elapsed time)
21:52:46 Preparing RIPEMD-160-SPARK/outline ...
21:52:47 Finished Perfect-Number-Thm/outline (0:00:02 elapsed time)
21:52:47 Timing Perfect-Number-Thm (4 threads, 1.646s elapsed time, 4.825s cpu time, 0.000s GC time, factor 2.93)
21:52:47 Finished Perfect-Number-Thm (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.32)
21:52:47 Running Lehmer ...
21:52:47 Finished Lazy-Lists-II/outline (0:00:03 elapsed time)
21:52:47 Finished Blue_Eyes/outline (0:00:02 elapsed time)
21:52:47 Timing Lazy-Lists-II (4 threads, 1.802s elapsed time, 5.141s cpu time, 0.000s GC time, factor 2.85)
21:52:47 Finished Lazy-Lists-II (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.46)
21:52:47 Timing Blue_Eyes (4 threads, 1.321s elapsed time, 2.863s cpu time, 0.000s GC time, factor 2.17)
21:52:47 Finished Blue_Eyes (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.32)
21:52:47 Running Ptolemys_Theorem ...
21:52:47 Running Free-Boolean-Algebra ...
21:52:47 Finished Lifting_the_Exponent/document (0:00:03 elapsed time)
21:52:47 Preparing Lifting_the_Exponent/outline ...
21:52:48 FunWithFunctions: theory FunWithFunctions.FunWithFunctions
21:52:48 Preparing Liouville_Numbers/document ...
21:52:49 Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
21:52:49 Finished RIPEMD-160-SPARK/outline (0:00:02 elapsed time)
21:52:49 Free-Boolean-Algebra: theory Free-Boolean-Algebra.Free_Boolean_Algebra
21:52:49 Finished AnselmGod/outline (0:00:02 elapsed time)
21:52:49 Preparing FunWithFunctions/document ...
21:52:49 Timing AnselmGod (4 threads, 1.196s elapsed time, 3.484s cpu time, 0.000s GC time, factor 2.91)
21:52:49 Finished AnselmGod (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.56)
21:52:49 Timing RIPEMD-160-SPARK (4 threads, 1.307s elapsed time, 1.396s cpu time, 0.000s GC time, factor 1.07)
21:52:49 Finished RIPEMD-160-SPARK (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.93)
21:52:49 Running Depth-First-Search ...
21:52:49 Running CofGroups ...
21:52:50 Finished Combinatorics_Words_Graph_Lemma/outline (0:00:04 elapsed time)
21:52:50 Timing Combinatorics_Words_Graph_Lemma (4 threads, 1.238s elapsed time, 4.036s cpu time, 0.000s GC time, factor 3.26)
21:52:50 Finished Combinatorics_Words_Graph_Lemma (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.48)
21:52:50 Running Lorenz_C1 ...
21:52:50 Preparing Minkowskis_Theorem/document ...
21:52:51 Preparing Free-Boolean-Algebra/document ...
21:52:51 Finished Liouville_Numbers/document (0:00:03 elapsed time)
21:52:51 Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
21:52:51 Preparing Liouville_Numbers/outline ...
21:52:51 Finished Lifting_the_Exponent/outline (0:00:03 elapsed time)
21:52:51 Timing Lifting_the_Exponent (4 threads, 1.529s elapsed time, 5.095s cpu time, 0.114s GC time, factor 3.33)
21:52:51 Finished Lifting_the_Exponent (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.46)
21:52:51 Running Monad_Normalisation ...
21:52:51 CofGroups: theory HOL-Library.Nat_Bijection
21:52:51 Depth-First-Search: theory Depth-First-Search.DFS
21:52:52 CofGroups: theory CofGroups.CofGroups
21:52:52 Lehmer: theory Lehmer.Lehmer
21:52:52 Finished FunWithFunctions/document (0:00:02 elapsed time)
21:52:52 Preparing FunWithFunctions/outline ...
21:52:52 Preparing Ptolemys_Theorem/document ...
21:52:53 Preparing Depth-First-Search/document ...
21:52:53 Finished Free-Boolean-Algebra/document (0:00:02 elapsed time)
21:52:53 Preparing Free-Boolean-Algebra/outline ...
21:52:53 Preparing CofGroups/document ...
21:52:53 Finished Liouville_Numbers/outline (0:00:02 elapsed time)
21:52:54 Preparing Lehmer/document ...
21:52:54 Finished Minkowskis_Theorem/document (0:00:03 elapsed time)
21:52:54 Preparing Minkowskis_Theorem/outline ...
21:52:54 Timing Liouville_Numbers (4 threads, 1.375s elapsed time, 3.813s cpu time, 0.000s GC time, factor 2.77)
21:52:54 Finished Liouville_Numbers (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.38)
21:52:54 Running Laws_of_Large_Numbers ...
21:52:54 Finished Depth-First-Search/document (0:00:01 elapsed time)
21:52:54 Preparing Depth-First-Search/outline ...
21:52:55 Finished Free-Boolean-Algebra/outline (0:00:01 elapsed time)
21:52:55 Finished FunWithFunctions/outline (0:00:02 elapsed time)
21:52:55 Timing Free-Boolean-Algebra (4 threads, 1.050s elapsed time, 2.325s cpu time, 0.000s GC time, factor 2.21)
21:52:55 Finished Free-Boolean-Algebra (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.30)
21:52:55 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
21:52:55 Timing FunWithFunctions (4 threads, 1.178s elapsed time, 2.951s cpu time, 0.000s GC time, factor 2.51)
21:52:55 Finished FunWithFunctions (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.43)
21:52:55 Running FFT ...
21:52:55 Running General-Triangle ...
21:52:55 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
21:52:56 Finished Ptolemys_Theorem/document (0:00:03 elapsed time)
21:52:56 Preparing Ptolemys_Theorem/outline ...
21:52:56 Finished Depth-First-Search/outline (0:00:01 elapsed time)
21:52:56 Finished CofGroups/document (0:00:03 elapsed time)
21:52:56 Timing Depth-First-Search (4 threads, 0.974s elapsed time, 2.089s cpu time, 0.000s GC time, factor 2.14)
21:52:56 Finished Depth-First-Search (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.27)
21:52:56 Preparing CofGroups/outline ...
21:52:56 Running Intro_Dest_Elim ...
21:52:57 Finished Lehmer/document (0:00:02 elapsed time)
21:52:57 Preparing Lehmer/outline ...
21:52:57 Finished Minkowskis_Theorem/outline (0:00:02 elapsed time)
21:52:57 FFT: theory FFT.FFT
21:52:57 General-Triangle: theory General-Triangle.GeneralTriangle
21:52:57 Preparing Monad_Normalisation/document ...
21:52:57 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
21:52:57 Timing Minkowskis_Theorem (4 threads, 1.176s elapsed time, 4.152s cpu time, 0.000s GC time, factor 3.53)
21:52:57 Finished Minkowskis_Theorem (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.54)
21:52:57 Running Conditional_Simplification ...
21:52:58 Preparing General-Triangle/document ...
21:52:58 Preparing FFT/document ...
21:52:58 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
21:52:58 Intro_Dest_Elim: theory HOL-Library.LaTeXsugar
21:52:58 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Tools
21:52:58 Intro_Dest_Elim: theory Intro_Dest_Elim.IHOL_IDE
21:52:58 Intro_Dest_Elim: theory Intro_Dest_Elim.Reference_Prerequisites
21:52:58 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
21:52:58 Finished Ptolemys_Theorem/outline (0:00:02 elapsed time)
21:52:58 Timing Ptolemys_Theorem (4 threads, 1.157s elapsed time, 3.209s cpu time, 0.000s GC time, factor 2.77)
21:52:58 Finished Ptolemys_Theorem (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.34)
21:52:58 Running Card_Equiv_Relations ...
21:52:59 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Reference
21:52:59 Conditional_Simplification: theory Conditional_Simplification.CS_Tools
21:52:59 Conditional_Simplification: theory HOL-Library.LaTeXsugar
21:52:59 Conditional_Simplification: theory Conditional_Simplification.IHOL_CS
21:52:59 Conditional_Simplification: theory Conditional_Simplification.Reference_Prerequisites
21:52:59 Timing Lorenz_C1 (4 threads, 1.108s elapsed time, 1.766s cpu time, 0.000s GC time, factor 1.59)
21:52:59 Finished Lorenz_C1 (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.04)
21:52:59 Running Bondy ...
21:52:59 Preparing Intro_Dest_Elim/document ...
21:52:59 Finished Lehmer/outline (0:00:02 elapsed time)
21:52:59 Conditional_Simplification: theory Conditional_Simplification.CS_Reference
21:52:59 Timing Lehmer (4 threads, 1.226s elapsed time, 3.170s cpu time, 0.000s GC time, factor 2.59)
21:52:59 Finished Lehmer (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.25)
21:52:59 Running Roy_Floyd_Warshall ...
21:53:00 Finished CofGroups/outline (0:00:03 elapsed time)
21:53:00 Preparing Laws_of_Large_Numbers/document ...
21:53:00 Preparing Conditional_Simplification/document ...
21:53:00 Timing CofGroups (4 threads, 1.327s elapsed time, 3.716s cpu time, 0.000s GC time, factor 2.80)
21:53:00 Finished CofGroups (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.58)
21:53:00 Running Aristotles_Assertoric_Syllogistic ...
21:53:00 Finished Monad_Normalisation/document (0:00:03 elapsed time)
21:53:00 Preparing Monad_Normalisation/outline ...
21:53:00 Finished FFT/document (0:00:02 elapsed time)
21:53:00 Preparing FFT/outline ...
21:53:01 Bondy: theory Bondy.Bondy
21:53:01 Roy_Floyd_Warshall: theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
21:53:02 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Equiv_Relations
21:53:02 Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
21:53:02 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
21:53:02 Finished General-Triangle/document (0:00:04 elapsed time)
21:53:02 Preparing General-Triangle/outline ...
21:53:02 Preparing Bondy/document ...
21:53:02 Finished FFT/outline (0:00:01 elapsed time)
21:53:02 Preparing Roy_Floyd_Warshall/document ...
21:53:03 Timing FFT (4 threads, 0.890s elapsed time, 3.115s cpu time, 0.000s GC time, factor 3.50)
21:53:03 Finished FFT (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.63)
21:53:03 Running Ordinals_and_Cardinals ...
21:53:03 Preparing Aristotles_Assertoric_Syllogistic/document ...
21:53:03 Finished Laws_of_Large_Numbers/document (0:00:03 elapsed time)
21:53:03 Preparing Laws_of_Large_Numbers/outline ...
21:53:03 Preparing Card_Equiv_Relations/document ...
21:53:03 Finished Monad_Normalisation/outline (0:00:03 elapsed time)
21:53:04 Timing Monad_Normalisation (4 threads, 1.177s elapsed time, 1.868s cpu time, 0.000s GC time, factor 1.59)
21:53:04 Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.07)
21:53:04 Running Example-Submission ...
21:53:04 Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
21:53:04 Finished Aristotles_Assertoric_Syllogistic/document (0:00:01 elapsed time)
21:53:04 Preparing Aristotles_Assertoric_Syllogistic/outline ...
21:53:04 Finished Bondy/document (0:00:02 elapsed time)
21:53:04 Preparing Bondy/outline ...
21:53:05 Preparing Ordinals_and_Cardinals/document ...
21:53:05 Finished Intro_Dest_Elim/document (0:00:05 elapsed time)
21:53:05 Preparing Intro_Dest_Elim/outline ...
21:53:05 Finished Roy_Floyd_Warshall/document (0:00:02 elapsed time)
21:53:05 Preparing Roy_Floyd_Warshall/outline ...
21:53:05 Example-Submission: theory Example-Submission.Submission
21:53:06 Finished Conditional_Simplification/document (0:00:05 elapsed time)
21:53:06 Preparing Conditional_Simplification/outline ...
21:53:06 Preparing Example-Submission/document ...
21:53:06 Finished Laws_of_Large_Numbers/outline (0:00:02 elapsed time)
21:53:06 Finished Card_Equiv_Relations/document (0:00:02 elapsed time)
21:53:06 Preparing Card_Equiv_Relations/outline ...
21:53:06 Finished General-Triangle/outline (0:00:03 elapsed time)
21:53:06 Timing Laws_of_Large_Numbers (4 threads, 0.931s elapsed time, 2.735s cpu time, 0.000s GC time, factor 2.94)
21:53:06 Finished Laws_of_Large_Numbers (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.26)
21:53:06 Timing General-Triangle (4 threads, 0.682s elapsed time, 1.506s cpu time, 0.000s GC time, factor 2.21)
21:53:06 Finished General-Triangle (0:00:02 elapsed time, 0:00:03 cpu time)
21:53:06 Finished Aristotles_Assertoric_Syllogistic/outline (0:00:01 elapsed time)
21:53:06 Finished Ordinals_and_Cardinals/document (0:00:01 elapsed time)
21:53:06 Preparing Ordinals_and_Cardinals/outline ...
21:53:07 Timing Aristotles_Assertoric_Syllogistic (4 threads, 0.387s elapsed time, 0.947s cpu time, 0.000s GC time, factor 2.45)
21:53:07 Finished Aristotles_Assertoric_Syllogistic (0:00:02 elapsed time)
21:53:07 Finished Bondy/outline (0:00:02 elapsed time)
21:53:07 Timing Bondy (4 threads, 0.752s elapsed time, 0.925s cpu time, 0.000s GC time, factor 1.23)
21:53:07 Finished Bondy (0:00:02 elapsed time)
21:53:08 Finished Roy_Floyd_Warshall/outline (0:00:02 elapsed time)
21:53:08 Finished Ordinals_and_Cardinals/outline (0:00:01 elapsed time)
21:53:08 Timing Ordinals_and_Cardinals (4 threads, 0.112s elapsed time, 0.170s cpu time, 0.000s GC time, factor 1.52)
21:53:08 Finished Ordinals_and_Cardinals (0:00:02 elapsed time)
21:53:08 Timing Roy_Floyd_Warshall (4 threads, 0.582s elapsed time, 1.268s cpu time, 0.000s GC time, factor 2.18)
21:53:08 Finished Roy_Floyd_Warshall (0:00:02 elapsed time, 0:00:03 cpu time)
21:53:08 Finished Example-Submission/document (0:00:02 elapsed time)
21:53:08 Preparing Example-Submission/outline ...
21:53:08 Finished Card_Equiv_Relations/outline (0:00:02 elapsed time)
21:53:09 Timing Card_Equiv_Relations (4 threads, 0.682s elapsed time, 1.926s cpu time, 0.000s GC time, factor 2.82)
21:53:09 Finished Card_Equiv_Relations (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.21)
21:53:10 Finished Intro_Dest_Elim/outline (0:00:05 elapsed time)
21:53:10 Timing Intro_Dest_Elim (4 threads, 0.693s elapsed time, 1.015s cpu time, 0.000s GC time, factor 1.46)
21:53:10 Finished Intro_Dest_Elim (0:00:02 elapsed time)
21:53:10 Finished Example-Submission/outline (0:00:02 elapsed time)
21:53:10 Finished Conditional_Simplification/outline (0:00:04 elapsed time)
21:53:11 Timing Example-Submission (4 threads, 0.089s elapsed time, 0.157s cpu time, 0.000s GC time, factor 1.76)
21:53:11 Finished Example-Submission (0:00:02 elapsed time)
21:53:11 Timing Conditional_Simplification (4 threads, 0.786s elapsed time, 1.252s cpu time, 0.000s GC time, factor 1.59)
21:53:11 Finished Conditional_Simplification (0:00:02 elapsed time, 0:00:03 cpu time)
21:53:11 Unfinished session(s): BTree, EdmondsKarp_Maxflow, Flow_Networks, Floyd_Warshall, Knuth_Morris_Pratt, Kruskal, PAC_Checker, Prpu_Maxflow, Refine_Imperative_HOL, Sepref_Basic, Sepref_IICF, VerifyThis2018, VerifyThis2019
21:53:11 
21:53:11 === TIMING ===
21:53:11 
21:53:11 Group AFP: 23:10:14 elapsed time, 65:34:33 cpu time, factor 2.83
21:53:11 Group main: 0:41:51 elapsed time, 2:07:59 cpu time, factor 3.06
21:53:11 Group timing: 0:44:02 elapsed time, 2:13:34 cpu time, factor 3.03
21:53:11 Group large: 1:08:50 elapsed time, 4:17:05 cpu time, factor 3.73
21:53:11 Overall: 2:52:48 elapsed time, 68:07:28 cpu time, factor 23.65
21:53:11 
21:53:11 === FAILED SESSIONS ===
21:53:11 
21:53:11 Session EdmondsKarp_Maxflow: CANCELLED
21:53:11 Session BTree: CANCELLED
21:53:11 Session Sepref_IICF: CANCELLED
21:53:11 Session VerifyThis2019: CANCELLED
21:53:11 Session Floyd_Warshall: CANCELLED
21:53:11 Session Prpu_Maxflow: CANCELLED
21:53:11 Session Sepref_Basic: FAILED 1
21:53:11 Session Kruskal: CANCELLED
21:53:11 Session VerifyThis2018: CANCELLED
21:53:11 Session PAC_Checker: CANCELLED
21:53:11 Session Knuth_Morris_Pratt: CANCELLED
21:53:11 Session Refine_Imperative_HOL: FAILED 1
21:53:11 Session Flow_Networks: CANCELLED
21:53:11 
21:53:11 === DEPENDENCIES ===
21:53:11 
21:53:11 Generating dependencies file ...
21:53:17 Writing dependencies file ...
21:53:17 
21:53:17 === COMPLETED ===
21:53:17 
21:53:17 Build step 'Execute shell' marked build as failure
21:53:17 Started calculate disk usage of build
21:53:17 Finished Calculation of disk usage of build in 0 seconds
21:53:17 Started calculate disk usage of workspace
21:53:18 Finished Calculation of disk usage of workspace in 0 seconds
21:53:18 Finished: FAILURE