Frequency_Moments: theory HOL-Algebra.RingHom
00:40:28Universal_Hash_Families: theory HOL-Algebra.Ring
00:40:28Treaps: theory HOL-Data_Structures.List_Ins_Del
00:40:28Treaps: theory HOL-Data_Structures.Set_Specs
00:40:28Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
00:40:28Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.StandardBorel
00:40:28Treaps: theory HOL-Data_Structures.Tree_Set
00:40:28Three_Squares: theory Winding_Number_Eval.Missing_Analysis
00:40:28Applicative_Lifting: theory Applicative_Lifting.Joinable
00:40:28Lovasz_Local: theory Lovasz_Local.Basic_Method
00:40:28MFMC_Countable: theory MFMC_Countable.MFMC_Misc
00:40:28Three_Squares: theory Sturm_Tarski.Sturm_Tarski
00:40:28Applicative_Lifting: theory Applicative_Lifting.Applicative
00:40:28Applicative_Lifting: theory HOL-Library.State_Monad
00:40:28Applicative_Lifting: theory HOL-Library.Confluence
00:40:28Applicative_Lifting: theory HOL-Library.Function_Algebras
00:40:28Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
00:40:28Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Order_Relation
00:40:28Dirichlet_Series: theory Dirichlet_Series.Euler_Products
00:40:28Applicative_Lifting: theory HOL-Library.Confluent_Quotient
00:40:28Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
00:40:28Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef
00:40:28Projective_Measurements: theory HOL-Algebra.Lattice
00:40:28Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation
00:40:28Applicative_Lifting: theory HOL-Library.Function_Division
00:40:28Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda
00:40:28Applicative_Lifting: theory HOL-Library.Dlist
00:40:28Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
00:40:28Turans_Graph_Theorem: theory HOL-Library.Log_Nat
00:40:28Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residues
00:40:29Treaps: theory Landau_Symbols.Landau_Real_Products
00:40:29Projective_Measurements: theory Abstract-Rewriting.Seq
00:40:29Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice
00:40:29Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom
00:40:29Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
00:40:29MFMC_Countable: theory Flow_Networks.Residual_Graph
00:40:29List_Update: theory Regular-Sets.Regular_Exp
00:40:29Running S_Finite_Measure_Monad (on 10.195.8.32) ...
00:40:29Running Probabilistic_System_Zoo (on 10.195.8.32) ...
00:40:29Running Roth_Arithmetic_Progressions (on 10.195.8.32) ...
00:40:29Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
00:40:29MFMC_Countable: theory MFMC_Countable.MFMC_Network
00:40:29Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
00:40:29Fourier: theory Lp.Lp
00:40:29Frequency_Moments: theory HOL-Algebra.QuotRing
00:40:29Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
00:40:29Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
00:40:29Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
00:40:29Frequency_Moments: theory HOL-Algebra.UnivPoly
00:40:29Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.QuasiBorel
00:40:29Probabilistic_Prime_Tests: theory HOL-Library.Fun_Lexorder
00:40:29Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed
00:40:29Building Girth_Chromatic (on 10.195.8.32) ...
00:40:30Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence
00:40:30Projective_Measurements: theory HOL-Library.More_List
00:40:30Three_Squares: theory HOL-Number_Theory.Residues
00:40:30Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
00:40:30Fourier: theory Fourier.Lspace
00:40:30Projective_Measurements: theory HOL-Library.While_Combinator
00:40:30Fourier: theory Fourier.Square_Integrable
00:40:30Executable_Randomized_Algorithms: theory HOL-Number_Theory.Euler_Criterion
00:40:30Executable_Randomized_Algorithms: theory HOL-Number_Theory.Gauss
00:40:30Executable_Randomized_Algorithms: theory HOL-Number_Theory.Pocklington
00:40:30Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu
00:40:30Projective_Measurements: theory HOL-Algebra.Complete_Lattice
00:40:30Ergodic_Theory: theory Ergodic_Theory.Recurrence
00:40:30Actuarial_Mathematics: theory Actuarial_Mathematics.Life_Table
00:40:30Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
00:40:30Executable_Randomized_Algorithms: theory HOL-Number_Theory.Quadratic_Reciprocity
00:40:30Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
00:40:30Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
00:40:30Applicative_Lifting: theory Applicative_Lifting.Applicative_List
00:40:30Dirichlet_Series: theory Dirichlet_Series.More_Totient
00:40:30Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
00:40:30Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
00:40:30Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Arithmetic
00:40:30Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residue_Primitive_Roots
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State
00:40:31Schwartz_Zippel: theory HOL-Algebra.Group
00:40:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction
00:40:31Dirichlet_Series: theory Dirichlet_Series.Divisor_Count
00:40:31Fourier: theory Fourier.Fourier
00:40:31Schwartz_Zippel: theory Polynomials.MPoly_Type
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
00:40:31Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
00:40:31Executable_Randomized_Algorithms: theory HOL-Number_Theory.Number_Theory
00:40:31Probabilistic_Prime_Tests: theory HOL-Combinatorics.Cycles
00:40:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
00:40:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_State
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
00:40:31Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda
00:40:31Applicative_Lifting: theory HOL-Proofs-Lambda.Eta
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
00:40:31Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
00:40:31Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
00:40:31Probabilistic_Prime_Tests: theory HOL-Algebra.Order
00:40:31Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
00:40:31Applicative_Lifting: theory Applicative_Lifting.Combinators
00:40:31Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
00:40:31MFMC_Countable: theory Flow_Networks.Augmenting_Flow
00:40:31Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
00:40:31Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory
00:40:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Product_QuasiBorel
00:40:31Deep_Learning: theory HOL-Algebra.FiniteProduct
00:40:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.CoProduct_QuasiBorel
00:40:31Probabilistic_Prime_Tests: theory HOL-Combinatorics.List_Permutation
00:40:31Probabilistic_Prime_Tests: theory HOL-Library.Groups_Big_Fun
00:40:31Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
00:40:31Dirichlet_Series: theory Dirichlet_Series.Partial_Summation
00:40:31Projective_Measurements: theory HOL-Algebra.Group
00:40:31MFMC_Countable: theory Flow_Networks.Augmenting_Path
00:40:31Treaps: theory Landau_Symbols.Landau_Simprocs
00:40:31Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Misc
00:40:32MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
00:40:32Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
00:40:32Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
00:40:32Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More
00:40:32Turans_Graph_Theorem: theory HOL-Library.Interval
00:40:32Roth_Arithmetic_Progressions: theory HOL-Library.Code_Abstract_Nat
00:40:32Turans_Graph_Theorem: theory HOL-Library.Float
00:40:32Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Dense_Linear_Order
00:40:32Deep_Learning: theory HOL-Algebra.Ring
00:40:32S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QuasiBorel
00:40:32Schwartz_Zippel: theory Polynomials.More_MPoly_Type
00:40:32S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Lemmas_StandardBorel
00:40:32Executable_Randomized_Algorithms: theory Dirichlet_Series.Multiplicative_Function
00:40:32Lovasz_Local: theory Lovasz_Local.Digraph_Extensions
00:40:32Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Exponent_QuasiBorel
00:40:32Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
00:40:32Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More
00:40:32Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
00:40:32Probabilistic_Prime_Tests: theory HOL-Library.More_List
00:40:32Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Nat
00:40:32Actuarial_Mathematics: theory Actuarial_Mathematics.Examples
00:40:32Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Product
00:40:32Executable_Randomized_Algorithms: theory Dirichlet_Series.Euler_Products
00:40:32Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Lemma
00:40:32Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
00:40:32Treaps: theory Landau_Symbols.Landau_More
00:40:32Universal_Hash_Families: theory HOL-Algebra.Divisibility
00:40:32Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping
00:40:32Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
00:40:32Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
00:40:32Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Int
00:40:32Closest_Pair_Points: theory Closest_Pair_Points.Closest_Pair
00:40:32Universal_Hash_Families: theory HOL-Algebra.AbelCoset
00:40:32Closest_Pair_Points: theory Closest_Pair_Points.Closest_Pair_Alternative
00:40:32Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel
00:40:32Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
00:40:32Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
00:40:32Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series
00:40:33Schwartz_Zippel: theory HOL-Library.While_Combinator
00:40:33Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code
00:40:33Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union
00:40:33Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
00:40:33Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral
00:40:33Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
00:40:33Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
00:40:33Roth_Arithmetic_Progressions: theory HOL-Library.Ramsey
00:40:33Ergodic_Theory: theory Ergodic_Theory.Invariants
00:40:33Girth_Chromatic: theory HOL-Library.Code_Target_Nat
00:40:33Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
00:40:33Schwartz_Zippel: theory Polynomials.More_Modules
00:40:33MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
00:40:33Running Monomorphic_Monad (on 10.195.6.179) ...
00:40:33Running Lp (on 10.195.6.179) ...
00:40:33MFMC_Countable: theory MFMC_Countable.MFMC_Flow_Attainability
00:40:33Running Balog_Szemeredi_Gowers (on 10.195.6.179) ...
00:40:34Girth_Chromatic: theory HOL-Library.Code_Target_Int
00:40:34Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Root
00:40:34Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
00:40:34Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
00:40:34Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
00:40:34Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Unsorted
00:40:34Girth_Chromatic: theory HOL-Library.Code_Target_Numeral
00:40:34Schwartz_Zippel: theory HOL-Algebra.FiniteProduct
00:40:34Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
00:40:34Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
00:40:34Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds
00:40:34Girth_Chromatic: theory HOL-Library.Lattice_Algebras
00:40:34Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension
00:40:34Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
00:40:35Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
00:40:35Roth_Arithmetic_Progressions: theory HOL-Library.Lattice_Algebras
00:40:35Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
00:40:35Frequency_Moments: theory HOL-Algebra.IntRing
00:40:35Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
00:40:35Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
00:40:35Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Monad_QuasiBorel
00:40:35MFMC_Countable: theory MFMC_Countable.MFMC_Finite
00:40:35Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
00:40:35List_Update: theory Regular-Sets.NDerivative
00:40:35Executable_Randomized_Algorithms: theory Dirichlet_Series.Moebius_Mu
00:40:35Treaps: theory Random_BSTs.Random_BSTs
00:40:35Executable_Randomized_Algorithms: theory Dirichlet_Series.More_Totient
00:40:35Executable_Randomized_Algorithms: theory Dirichlet_Series.Liouville_Lambda
00:40:35Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
00:40:35Ergodic_Theory: theory Ergodic_Theory.Ergodicity
00:40:35Executable_Randomized_Algorithms: theory Dirichlet_Series.Divisor_Count
00:40:35MFMC_Countable: theory MFMC_Countable.MFMC_Web
00:40:35Deep_Learning: theory HOL-Algebra.Module
00:40:35Projective_Measurements: theory HOL-Algebra.Coset
00:40:35Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
00:40:35Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure
00:40:35Roth_Arithmetic_Progressions: theory HOL-Library.Log_Nat
00:40:35Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
00:40:35Executable_Randomized_Algorithms: theory Dirichlet_Series.Arithmetic_Summatory
00:40:36Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
00:40:36Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
00:40:36Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic_Misc
00:40:36List_Update: theory List_Update.MTF2_Effects
00:40:36Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
00:40:36Three_Squares: theory HOL-Number_Theory.Euler_Criterion
00:40:36Roth_Arithmetic_Progressions: theory Girth_Chromatic.Ugraphs
00:40:36Executable_Randomized_Algorithms: theory Dirichlet_Series.Partial_Summation
00:40:36Probabilistic_Prime_Tests: theory HOL-Algebra.Group
00:40:36Schwartz_Zippel: theory HOL-Algebra.Ring
00:40:36S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Space
00:40:36Lp: theory HOL-Library.Function_Algebras
00:40:36Lp: theory Ergodic_Theory.SG_Library_Complement
00:40:36Three_Squares: theory HOL-Number_Theory.Gauss
00:40:36List_Update: theory List_Update.BIT
00:40:36Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
00:40:36Frequency_Moments: theory HOL-Library.Interval
00:40:36Turans_Graph_Theorem: theory HOL-Library.Interval_Float
00:40:36Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure
00:40:36Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds
00:40:36Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations
00:40:36Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Dense_Linear_Order
00:40:36Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series_Analysis
00:40:37Balog_Szemeredi_Gowers: theory HOL-Library.Code_Abstract_Nat
00:40:37Roth_Arithmetic_Progressions: theory Szemeredi_Regularity.Szemeredi
00:40:37S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QBS_Morphism
00:40:37Girth_Chromatic: theory HOL-Library.Log_Nat
00:40:37Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
00:40:37Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Nat
00:40:37Ergodic_Theory: theory Ergodic_Theory.Kingman
00:40:37Ergodic_Theory: theory Ergodic_Theory.Shift_Operator
00:40:37Girth_Chromatic: theory Girth_Chromatic.Ugraphs
00:40:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
00:40:37Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Bayesian_Linear_Regression
00:40:37Projective_Measurements: theory HOL-Algebra.FiniteProduct
00:40:37Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial
00:40:37Treaps: theory Treaps.Treap
00:40:37Treaps: theory Treaps.Probability_Misc
00:40:37Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Int
00:40:37Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
00:40:37Deep_Learning: theory Jordan_Normal_Form.Missing_Ring
00:40:37Treaps: theory Treaps.Random_List_Permutation
00:40:39Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity
00:40:39Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
00:40:39Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
00:40:39Universal_Hash_Families: theory HOL-Algebra.Module
00:40:39Lp: theory Lp.Functional_Spaces
00:40:39Treaps: theory Treaps.Treap_Sort_and_BSTs
00:40:39Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Numeral
00:40:39Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
00:40:39Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Set_Theory
00:40:39Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set
00:40:39Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bool_Bounded_Set
00:40:39Projective_Measurements: theory HOL-Algebra.Ring
00:40:39Universal_Hash_Families: theory HOL-Algebra.Ideal
00:40:39Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
00:40:39Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample
00:40:40Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
00:40:40Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
00:40:40Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
00:40:40Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Group_Theory
00:40:40Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
00:40:40S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Product
00:40:40Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
00:40:40Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
00:40:40MFMC_Countable: theory MFMC_Countable.MFMC_Reduction
00:40:40Frequency_Moments: theory HOL-Library.Log_Nat
00:40:40Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
00:40:40Roth_Arithmetic_Progressions: theory Ergodic_Theory.SG_Library_Complement
00:40:40Deep_Learning: theory Polynomials.MPoly_Type_Univariate
00:40:40Frequency_Moments: theory HOL-Library.Float
00:40:40Treaps: theory Treaps.Random_Treap
00:40:40Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
00:40:40Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
00:40:40S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
00:40:41Density_Compiler: theory Density_Compiler.PDF_Compiler
00:40:41Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
00:40:41Roth_Arithmetic_Progressions: theory Ergodic_Theory.Asymptotic_Density
00:40:41S_Finite_Measure_Monad: theory Standard_Borel_Spaces.StandardBorel
00:40:41Three_Squares: theory Three_Squares.Residues_Properties
00:40:41Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial
00:40:41Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
00:40:41MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
00:40:41Three_Squares: theory HOL-Number_Theory.Pocklington
00:40:41Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Miscellaneous_Lemmas
00:40:41Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
00:40:41S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Lemmas_S_Finite_Measure_Monad
00:40:41S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Kernels
00:40:41Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
00:40:41Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
00:40:41S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Measure_QuasiBorel_Adjunction
00:40:41Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
00:40:41Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
00:40:41Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
00:40:41Balog_Szemeredi_Gowers: theory HOL-Library.Lattice_Algebras
00:40:41Universal_Hash_Families: theory HOL-Algebra.RingHom
00:40:41Roth_Arithmetic_Progressions: theory HOL-Library.Interval
00:40:41Schwartz_Zippel: theory HOL-Algebra.Module
00:40:41Roth_Arithmetic_Progressions: theory HOL-Library.Float
00:40:41Three_Squares: theory Dirichlet_L.Multiplicative_Characters
00:40:41Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots
00:40:41Deep_Learning: theory Jordan_Normal_Form.Conjugate
00:40:41Executable_Randomized_Algorithms: theory Zeta_Function.Zeta_Library
00:40:42List_Update: theory List_Update.Partial_Cost_Model
00:40:42Deep_Learning: theory Deep_Learning.Lebesgue_Functional
00:40:42Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
00:40:43Three_Squares: theory HOL-Number_Theory.Number_Theory
00:40:43MFMC_Countable: theory MFMC_Countable.MFMC_Bounded
00:40:43Lp: theory Lp.Lp
00:40:43Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
00:40:43Girth_Chromatic: theory HOL-Library.Interval
00:40:43Girth_Chromatic: theory HOL-Library.Float
00:40:43Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
00:40:43Universal_Hash_Families: theory HOL-Algebra.QuotRing
00:40:43Projective_Measurements: theory HOL-Algebra.Module
00:40:43Universal_Hash_Families: theory HOL-Algebra.UnivPoly
00:40:43MFMC_Countable: theory MFMC_Countable.MFMC_Unbounded
00:40:43Three_Squares: theory Budan_Fourier.BF_Misc
00:40:44Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
00:40:44Three_Squares: theory Bernoulli.Bernoulli_FPS
00:40:44Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List
00:40:44Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist
00:40:44List_Update: theory Regular-Sets.Equivalence_Checking
00:40:44MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
00:40:44List_Update: theory List_Update.List_Factoring
00:40:44Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring
00:40:44List_Update: theory List_Update.RExp_Var
00:40:44Deep_Learning: theory Polynomial_Interpolation.Ring_Hom
00:40:44Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm
00:40:44Frequency_Moments: theory HOL-Library.Interval_Float
00:40:44Timing Quasi_Borel_Spaces (6 threads, 15.168s elapsed time, 61.697s cpu time, 6.998s GC time, factor 4.07)
00:40:44Finished Quasi_Borel_Spaces (0:00:16 elapsed time, 0:01:03 cpu time, factor 3.76)
00:40:44Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
00:40:44Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
00:40:44Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
00:40:44Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Basic_Randomized_Algorithms
00:40:45Three_Squares: theory Dirichlet_Series.Multiplicative_Function
00:40:45Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm
00:40:45S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Monad_QuasiBorel
00:40:45List_Update: theory List_Update.OPT2
00:40:45Timing Standard_Borel_Spaces (6 threads, 21.100s elapsed time, 83.590s cpu time, 5.287s GC time, factor 3.96)
00:40:45Finished Standard_Borel_Spaces (0:00:22 elapsed time, 0:01:25 cpu time, factor 3.75)
00:40:45Three_Squares: theory Dirichlet_L.Dirichlet_Characters
00:40:45Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
00:40:45Deep_Learning: theory VectorSpace.FunctionLemmas
00:40:45Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_SPMF
00:40:45Timing Lovasz_Local (6 threads, 21.369s elapsed time, 99.806s cpu time, 8.507s GC time, factor 4.67)
00:40:45Finished Lovasz_Local (0:00:23 elapsed time, 0:01:41 cpu time, factor 4.41)
00:40:45Deep_Learning: theory VectorSpace.RingModuleFacts
00:40:45Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
00:40:45Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Dice_Roll
00:40:46Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral_Float
00:40:46Roth_Arithmetic_Progressions: theory HOL-Library.Interval_Float
00:40:46Three_Squares: theory Dirichlet_Series.Dirichlet_Product
00:40:46Deep_Learning: theory VectorSpace.MonoidSums
00:40:46Universal_Hash_Families: theory HOL-Algebra.IntRing
00:40:46Timing Treaps (6 threads, 17.943s elapsed time, 56.447s cpu time, 3.676s GC time, factor 3.15)
00:40:46Finished Treaps (0:00:19 elapsed time, 0:00:58 cpu time, factor 2.98)
00:40:46Probabilistic_Prime_Tests: theory HOL-Algebra.Left_Coset
00:40:46Girth_Chromatic: theory HOL-Library.Code_Target_Numeral_Float
00:40:46Probabilistic_Prime_Tests: theory HOL-Algebra.SimpleGroups
00:40:46Deep_Learning: theory VectorSpace.LinearCombinations
00:40:46Timing Fourier (6 threads, 19.606s elapsed time, 86.727s cpu time, 3.908s GC time, factor 4.42)
00:40:46Finished Fourier (0:00:21 elapsed time, 0:01:28 cpu time, factor 4.17)
00:40:46Girth_Chromatic: theory HOL-Library.Interval_Float
00:40:47Three_Squares: theory Dirichlet_Series.Dirichlet_Series
00:40:47Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:40:47MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
00:40:47MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation_MFMC
00:40:47List_Update: theory List_Update.BIT_pairwise
00:40:47Three_Squares: theory Dirichlet_Series.Euler_Products
00:40:47Probabilistic_Prime_Tests: theory HOL-Algebra.SndIsomorphismGrp
00:40:47Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
00:40:47Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS
00:40:47Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
00:40:47Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation_Bounds
00:40:48Balog_Szemeredi_Gowers: theory HOL-Library.Interval
00:40:48Timing Actuarial_Mathematics (6 threads, 21.598s elapsed time, 92.196s cpu time, 6.351s GC time, factor 4.27)
00:40:48Finished Actuarial_Mathematics (0:00:23 elapsed time, 0:01:34 cpu time, factor 4.03)
00:40:48Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:40:48Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
00:40:48Three_Squares: theory Bernoulli.Bernoulli_Zeta
00:40:48Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
00:40:49Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
00:40:49Deep_Learning: theory Jordan_Normal_Form.Matrix
00:40:49Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate
00:40:49Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series
00:40:49Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
00:40:49List_Update: theory List_Update.Phase_Partitioning
00:40:49Timing Markov_Models (8 threads, 32.799s elapsed time, 183.563s cpu time, 16.805s GC time, factor 5.60)
00:40:49Finished Markov_Models (0:00:50 elapsed time, 0:03:37 cpu time, factor 4.28)
00:40:50Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
00:40:50List_Update: theory List_Update.BIT_2comp_on2
00:40:50Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial
00:40:50List_Update: theory List_Update.TS
00:40:50Probabilistic_Prime_Tests: theory HOL-Algebra.Module
00:40:50Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
00:40:50Projective_Measurements: theory Jordan_Normal_Form.Conjugate
00:40:50Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin
00:40:51Three_Squares: theory Dirichlet_Series.Moebius_Mu
00:40:51Three_Squares: theory Dirichlet_Series.More_Totient
00:40:51Three_Squares: theory Dirichlet_Series.Divisor_Count
00:40:51Three_Squares: theory Dirichlet_Series.Liouville_Lambda
00:40:52Timing Closest_Pair_Points (6 threads, 24.417s elapsed time, 106.086s cpu time, 5.948s GC time, factor 4.34)
00:40:52Finished Closest_Pair_Points (0:00:26 elapsed time, 0:01:48 cpu time, factor 4.17)
00:40:52Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
00:40:52S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Montecarlo
00:40:52S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Query
00:40:52Deep_Learning: theory VectorSpace.SumSpaces
00:40:52Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial
00:40:52Three_Squares: theory Dirichlet_Series.Partial_Summation
00:40:52Balog_Szemeredi_Gowers: theory HOL-Library.Log_Nat
00:40:53Balog_Szemeredi_Gowers: theory HOL-Library.Float
00:40:53Deep_Learning: theory VectorSpace.VectorSpace
00:40:53Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
00:40:53Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:40:53Projective_Measurements: theory Matrix.Utility
00:40:53Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation
00:40:53Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
00:40:53Three_Squares: theory Winding_Number_Eval.Missing_Algebraic
00:40:53Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
00:40:53Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
00:40:53List_Update: theory List_Update.Comb
00:40:53Estimated 0:25:18 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.596s)
00:40:54Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
00:40:54Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial
00:40:54Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:40:54Three_Squares: theory Winding_Number_Eval.Missing_Transcendental
00:40:54Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
00:40:54Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra
00:40:54Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
00:40:54Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
00:40:54Schwartz_Zippel: theory Jordan_Normal_Form.Conjugate
00:40:54Timing Applicative_Lifting (6 threads, 11.301s elapsed time, 38.574s cpu time, 4.490s GC time, factor 3.41)
00:40:54Finished Applicative_Lifting (0:00:27 elapsed time, 0:01:05 cpu time, factor 2.41)
00:40:54Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem
00:40:54Deep_Learning: theory Deep_Learning.DL_Network
00:40:54Girth_Chromatic: theory HOL-Decision_Procs.Approximation
00:40:55Schwartz_Zippel: theory Symmetric_Polynomials.Vieta
00:40:55Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
00:40:56Projective_Measurements: theory Regular-Sets.Regular_Set
00:40:56Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials
00:40:58Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
00:40:58Deep_Learning: theory Deep_Learning.Tensor_Matricization
00:40:58Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Numeral_Float
00:40:58Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval
00:40:59Schwartz_Zippel: theory Open_Induction.Restricted_Predicates
00:40:59Balog_Szemeredi_Gowers: theory HOL-Library.Interval_Float
00:40:59Probabilistic_Prime_Tests: theory HOL-Algebra.Elementary_Groups
00:40:59Three_Squares: theory Three_Squares.Quadratic_Forms
00:41:00Projective_Measurements: theory Jordan_Normal_Form.Matrix
00:41:00Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Ring_Theory
00:41:00Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom
00:41:00Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
00:41:00Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
00:41:01Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
00:41:01Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
00:41:01Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation_Bounds
00:41:01Three_Squares: theory Landau_Symbols.Group_Sort
00:41:01Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
00:41:01Three_Squares: theory Zeta_Function.Zeta_Library
00:41:01Building Randomised_Social_Choice (on 10.195.7.194) ...
00:41:01Three_Squares: theory Zeta_Function.Zeta_Function
00:41:01Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
00:41:01Building Quick_Sort_Cost (on 10.195.7.194) ...
00:41:01Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
00:41:02Probabilistic_Prime_Tests: theory HOL-Algebra.Product_Groups
00:41:02Schwartz_Zippel: theory Regular-Sets.Regular_Set
00:41:02Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
00:41:02Universal_Hash_Families: theory HOL-Algebra.Subrings
00:41:02Three_Squares: theory Landau_Symbols.Landau_Real_Products
00:41:02Timing Ordinary_Differential_Equations (2 threads, 299.786s elapsed time, 495.236s cpu time, 36.414s GC time, factor 1.65)
00:41:02Finished Ordinary_Differential_Equations (0:05:42 elapsed time, 0:09:12 cpu time, factor 1.61)
00:41:02Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:41:02Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups
00:41:02Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
00:41:03Deep_Learning: theory Deep_Learning.DL_Shallow_Model
00:41:03Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
00:41:03Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
00:41:04Projective_Measurements: theory Regular-Sets.Regular_Exp
00:41:04Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
00:41:04Deep_Learning: theory Jordan_Normal_Form.Column_Operations
00:41:04Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
00:41:04Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
00:41:04Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
00:41:05Quick_Sort_Cost: theory HOL-Library.Function_Algebras
00:41:05Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
00:41:05Randomised_Social_Choice: theory List-Index.List_Index
00:41:05Deep_Learning: theory Jordan_Normal_Form.Determinant
00:41:05Quick_Sort_Cost: theory List-Index.List_Index
00:41:05Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:41:05Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
00:41:05Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions
00:41:05Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
00:41:06Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
00:41:06Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
00:41:06Three_Squares: theory Landau_Symbols.Landau_Simprocs
00:41:06Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
00:41:06Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
00:41:07Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
00:41:07Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
00:41:07Three_Squares: theory Landau_Symbols.Landau_More
00:41:07Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
00:41:07Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
00:41:07Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
00:41:07Three_Squares: theory Lehmer.Lehmer
00:41:07Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
00:41:07Three_Squares: theory Pratt_Certificate.Pratt_Certificate
00:41:07Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation
00:41:07Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample
00:41:08Deep_Learning: theory Deep_Learning.DL_Deep_Model
00:41:08Deep_Learning: theory Jordan_Normal_Form.VS_Connect
00:41:08Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
00:41:08Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
00:41:08Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
00:41:08Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
00:41:09Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
00:41:09Schwartz_Zippel: theory Regular-Sets.Regular_Exp
00:41:09Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
00:41:09Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
00:41:10Three_Squares: theory Bertrands_Postulate.Bertrand
00:41:10Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
00:41:10Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
00:41:10Running DiscretePricing (on of2.proof.cit.tum.de) ...
00:41:10Running Hahn_Jordan_Decomposition (on of2.proof.cit.tum.de) ...
00:41:10Projective_Measurements: theory Regular-Sets.NDerivative
00:41:10Projective_Measurements: theory Jordan_Normal_Form.Determinant
00:41:10Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
00:41:11DiscretePricing: theory DiscretePricing.Filtration
00:41:11DiscretePricing: theory DiscretePricing.Generated_Subalgebra
00:41:11Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl
00:41:11Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:41:11Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims
00:41:11DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
00:41:11Universal_Hash_Families: theory HOL-Algebra.Polynomials
00:41:12Running Stern_Brocot (on of3.proof.cit.tum.de) ...
00:41:12Running Neumann_Morgenstern_Utility (on of3.proof.cit.tum.de) ...
00:41:12Running Source_Coding_Theorem (on of3.proof.cit.tum.de) ...
00:41:12Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
00:41:12Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
00:41:12DiscretePricing: theory DiscretePricing.Martingale
00:41:12DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
00:41:12Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
00:41:12Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
00:41:13Running Skip_Lists (on of4.proof.cit.tum.de) ...
00:41:13Running Median_Method (on of4.proof.cit.tum.de) ...
00:41:13Running Buffons_Needle (on of4.proof.cit.tum.de) ...
00:41:13Quick_Sort_Cost: theory Landau_Symbols.Landau_More
00:41:13Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
00:41:13Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
00:41:13Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
00:41:13Stern_Brocot: theory Stern_Brocot.Cotree
00:41:13Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
00:41:13Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
00:41:13Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
00:41:13Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
00:41:13Schwartz_Zippel: theory Regular-Sets.NDerivative
00:41:13Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
00:41:14Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
00:41:14Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
00:41:14Timing Echelon_Form (2 threads, 319.332s elapsed time, 590.111s cpu time, 37.626s GC time, factor 1.85)
00:41:14Finished Echelon_Form (0:05:55 elapsed time, 0:10:38 cpu time, factor 1.79)
00:41:14Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
00:41:14Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
00:41:14Buffons_Needle: theory Buffons_Needle.Buffons_Needle
00:41:14Skip_Lists: theory Skip_Lists.Misc
00:41:14Skip_Lists: theory Skip_Lists.Pi_pmf
00:41:14Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
00:41:14Skip_Lists: theory Skip_Lists.Geometric_PMF
00:41:14Projective_Measurements: theory Regular-Sets.Relation_Interpretation
00:41:14Projective_Measurements: theory VectorSpace.FunctionLemmas
00:41:14Projective_Measurements: theory VectorSpace.RingModuleFacts
00:41:14Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
00:41:14Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
00:41:15Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
00:41:15Skip_Lists: theory Skip_Lists.Skip_List
00:41:15Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
00:41:15Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
00:41:15Projective_Measurements: theory Regular-Sets.Equivalence_Checking
00:41:15Frequency_Moments: theory HOL-Algebra.Subrings
00:41:15Median_Method: theory Median_Method.Median
00:41:15Projective_Measurements: theory VectorSpace.MonoidSums
00:41:15Timing Source_Coding_Theorem (6 threads, 1.594s elapsed time, 4.956s cpu time, 0.164s GC time, factor 3.11)
00:41:15Finished Source_Coding_Theorem (0:00:03 elapsed time, 0:00:06 cpu time, factor 2.01)
00:41:15Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
00:41:16Projective_Measurements: theory Regular-Sets.Regexp_Method
00:41:16Projective_Measurements: theory VectorSpace.LinearCombinations
00:41:16Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
00:41:16Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
00:41:16Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
00:41:16Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
00:41:16Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
00:41:16Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
00:41:16Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
00:41:16Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
00:41:16DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
00:41:16Timing Buffons_Needle (6 threads, 1.990s elapsed time, 7.002s cpu time, 0.135s GC time, factor 3.52)
00:41:16Finished Buffons_Needle (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.41)
00:41:17Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
00:41:17DiscretePricing: theory DiscretePricing.Fair_Price
00:41:17Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
00:41:17Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
00:41:17Timing MDP-Rewards (2 threads, 31.875s elapsed time, 58.696s cpu time, 2.946s GC time, factor 1.84)
00:41:17Finished MDP-Rewards (0:01:05 elapsed time, 0:01:37 cpu time, factor 1.49)
00:41:17Timing Median_Method (6 threads, 2.916s elapsed time, 7.978s cpu time, 0.312s GC time, factor 2.74)
00:41:17Finished Median_Method (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.06)
00:41:18Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
00:41:18Schwartz_Zippel: theory Regular-Sets.Regexp_Method
00:41:18Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
00:41:18Timing Skip_Lists (6 threads, 3.349s elapsed time, 15.503s cpu time, 0.456s GC time, factor 4.63)
00:41:18Finished Skip_Lists (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.34)
00:41:18Timing Neumann_Morgenstern_Utility (6 threads, 4.262s elapsed time, 18.867s cpu time, 1.462s GC time, factor 4.43)
00:41:18Finished Neumann_Morgenstern_Utility (0:00:05 elapsed time, 0:00:20 cpu time, factor 3.43)
00:41:19Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
00:41:19Deep_Learning: theory Jordan_Normal_Form.DL_Rank
00:41:19Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
00:41:19Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility
00:41:19Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings
00:41:20Frequency_Moments: theory HOL-Algebra.Polynomials
00:41:20Timing Hahn_Jordan_Decomposition (6 threads, 8.293s elapsed time, 24.366s cpu time, 0.860s GC time, factor 2.94)
00:41:20Finished Hahn_Jordan_Decomposition (0:00:09 elapsed time, 0:00:25 cpu time, factor 2.59)
00:41:20Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
00:41:20Timing Lp (2 threads, 42.171s elapsed time, 74.596s cpu time, 3.265s GC time, factor 1.77)
00:41:20Finished Lp (0:00:45 elapsed time, 0:01:17 cpu time, factor 1.71)
00:41:20DiscretePricing: theory DiscretePricing.CRR_Model
00:41:20Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
00:41:21Schwartz_Zippel: theory Polynomials.Utils
00:41:21Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
00:41:21Timing Monomorphic_Monad (2 threads, 42.683s elapsed time, 78.368s cpu time, 8.477s GC time, factor 1.84)
00:41:21Finished Monomorphic_Monad (0:00:46 elapsed time, 0:01:22 cpu time, factor 1.78)
00:41:21Projective_Measurements: theory Abstract-Rewriting.SN_Orders
00:41:21Schwartz_Zippel: theory Polynomials.Power_Products
00:41:23Projective_Measurements: theory VectorSpace.SumSpaces
00:41:24Projective_Measurements: theory VectorSpace.VectorSpace
00:41:24DiscretePricing: theory DiscretePricing.Option_Price_Examples
00:41:24Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
00:41:24Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
00:41:24Timing Executable_Randomized_Algorithms (8 threads, 82.729s elapsed time, 540.626s cpu time, 43.082s GC time, factor 6.53)
00:41:24Finished Executable_Randomized_Algorithms (0:01:25 elapsed time, 0:09:07 cpu time, factor 6.42)
00:41:25Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
00:41:25Projective_Measurements: theory Matrix.Ordered_Semiring
00:41:25Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
00:41:25Timing Density_Compiler (6 threads, 60.820s elapsed time, 143.177s cpu time, 8.711s GC time, factor 2.35)
00:41:25Finished Density_Compiler (0:01:02 elapsed time, 0:02:25 cpu time, factor 2.32)
00:41:25Three_Squares: theory Dirichlet_L.Dirichlet_Theorem
00:41:25Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
00:41:26Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
00:41:26Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
00:41:26Stern_Brocot: theory Stern_Brocot.Bird_Tree
00:41:27Timing Stern_Brocot (6 threads, 13.601s elapsed time, 24.633s cpu time, 2.449s GC time, factor 1.81)
00:41:27Finished Stern_Brocot (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.75)
00:41:28Projective_Measurements: theory Matrix.Matrix_Legacy
00:41:28Three_Squares: theory Three_Squares.Three_Squares
00:41:29Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
00:41:30Frequency_Moments: theory HOL-Number_Theory.Fib
00:41:30Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
00:41:30Timing DiscretePricing (6 threads, 18.618s elapsed time, 91.935s cpu time, 6.896s GC time, factor 4.94)
00:41:30Finished DiscretePricing (0:00:20 elapsed time, 0:01:34 cpu time, factor 4.63)
00:41:30Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
00:41:30Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
00:41:30Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
00:41:31Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
00:41:31Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues
00:41:31Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
00:41:32Frequency_Moments: theory HOL-Number_Theory.Totient
00:41:32Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
00:41:32Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
00:41:32Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
00:41:32Frequency_Moments: theory HOL-Number_Theory.Residues
00:41:32Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic_Misc
00:41:33Balog_Szemeredi_Gowers: theory Girth_Chromatic.Ugraphs
00:41:33Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
00:41:33Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
00:41:34Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
00:41:34Balog_Szemeredi_Gowers: theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
00:41:34Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
00:41:35Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
00:41:35Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
00:41:35Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
00:41:35Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
00:41:35Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
00:41:36Frequency_Moments: theory HOL-Number_Theory.Gauss
00:41:36Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Combinatorics_Preliminaries
00:41:36Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
00:41:36Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
00:41:36Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Energy_Lower_Bounds
00:41:36Frequency_Moments: theory HOL-Number_Theory.Pocklington
00:41:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion
00:41:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss
00:41:37Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Sumset_Triangle_Inequality
00:41:37Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Basics
00:41:37Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
00:41:37Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
00:41:37Frequency_Moments: theory HOL-Number_Theory.Number_Theory
00:41:37Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
00:41:38Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
00:41:39Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
00:41:39Building HOL-ODE-Numerics (on 10.195.8.46) ...
00:41:39Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
00:41:39Building Hermite (on 10.195.8.46) ...
00:41:39Timing Probabilistic_While (2 threads, 54.915s elapsed time, 91.419s cpu time, 3.531s GC time, factor 1.66)
00:41:39Finished Probabilistic_While (0:01:26 elapsed time, 0:02:09 cpu time, factor 1.49)
00:41:39Estimated 0:47:24 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.368s)
00:41:40Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Walks
00:41:40Running MDP-Algorithms (on of1-proof+8-15) ...
00:41:41Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
00:41:41Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
00:41:41Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Bipartite_Graphs
00:41:41Frequency_Moments: theory Median_Method.Median
00:41:41Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Connectivity
00:41:41MDP-Algorithms: theory HOL-Eisbach.Eisbach
00:41:41MDP-Algorithms: theory Containers.Extend_Partial_Order
00:41:41MDP-Algorithms: theory Containers.List_Fusion
00:41:41MDP-Algorithms: theory Containers.Equal
00:41:41MDP-Algorithms: theory Deriving.Comparator
00:41:41MDP-Algorithms: theory Deriving.Derive_Manager
00:41:41MDP-Algorithms: theory Deriving.Generator_Aux
00:41:41MDP-Algorithms: theory HOL-Computational_Algebra.Fraction_Field
00:41:41MDP-Algorithms: theory HOL-Data_Structures.Array_Specs
00:41:41MDP-Algorithms: theory Containers.Closure_Set
00:41:41MDP-Algorithms: theory HOL-Data_Structures.Cmp
00:41:41MDP-Algorithms: theory HOL-Data_Structures.Less_False
00:41:41MDP-Algorithms: theory Containers.Containers_Auxiliary
00:41:41MDP-Algorithms: theory HOL-Data_Structures.Sorted_Less
00:41:41MDP-Algorithms: theory Deriving.Equality_Generator
00:41:41MDP-Algorithms: theory HOL-Data_Structures.AList_Upd_Del
00:41:42MDP-Algorithms: theory HOL-Data_Structures.List_Ins_Del
00:41:42Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
00:41:42Hermite: theory Hermite.Hermite
00:41:42MDP-Algorithms: theory Deriving.Equality_Instances
00:41:42MDP-Algorithms: theory HOL-Library.Char_ord
00:41:42MDP-Algorithms: theory HOL-Library.Code_Abstract_Nat
00:41:42MDP-Algorithms: theory HOL-Library.Code_Target_Int
00:41:42MDP-Algorithms: theory HOL-Algebra.Congruence
00:41:42MDP-Algorithms: theory HOL-Library.Code_Target_Nat
00:41:42MDP-Algorithms: theory Deriving.Compare
00:41:42MDP-Algorithms: theory Deriving.Comparator_Generator
00:41:42MDP-Algorithms: theory HOL-Data_Structures.Map_Specs
00:41:42MDP-Algorithms: theory HOL-Data_Structures.Set_Specs
00:41:42MDP-Algorithms: theory HOL-Library.Code_Target_Numeral
00:41:42MDP-Algorithms: theory Jordan_Normal_Form.Missing_Misc
00:41:42MDP-Algorithms: theory HOL-Library.IArray
00:41:42MDP-Algorithms: theory HOL-Library.More_List
00:41:42MDP-Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
00:41:42Frequency_Moments: theory Lp.Functional_Spaces
00:41:42Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Graph_Theory_Preliminaries
00:41:42MDP-Algorithms: theory Containers.Containers_Generator
00:41:42HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
00:41:42HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
00:41:42MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
00:41:42MDP-Algorithms: theory Containers.Lexicographic_Order
00:41:42MDP-Algorithms: theory HOL-Library.RBT_Impl
00:41:43MDP-Algorithms: theory HOL-Data_Structures.Tree2
00:41:43MDP-Algorithms: theory Deriving.Compare_Generator
00:41:43MDP-Algorithms: theory HOL-Algebra.Order
00:41:43MDP-Algorithms: theory Containers.Collection_Enum
00:41:43MDP-Algorithms: theory Containers.Collection_Eq
00:41:43MDP-Algorithms: theory Containers.Set_Linorder
00:41:43MDP-Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
00:41:43MDP-Algorithms: theory HOL-Data_Structures.Isin2
00:41:43MDP-Algorithms: theory Deriving.Compare_Instances
00:41:43MDP-Algorithms: theory HOL-Data_Structures.Lookup2
00:41:43HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
00:41:43MDP-Algorithms: theory Containers.DList_Set
00:41:43MDP-Algorithms: theory HOL-Data_Structures.RBT
00:41:43MDP-Algorithms: theory Perron_Frobenius.Cancel_Card_Constraint
00:41:43HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
00:41:43Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
00:41:43HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
00:41:43HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
00:41:43MDP-Algorithms: theory Polynomial_Interpolation.Missing_Unsorted
00:41:43MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial
00:41:43MDP-Algorithms: theory HOL-Algebra.Lattice
00:41:43MDP-Algorithms: theory HOL-Library.Code_Real_Approx_By_Float
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
00:41:44Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
00:41:44HOL-ODE-Numerics: theory Deriving.Comparator
00:41:44MDP-Algorithms: theory Jordan_Normal_Form.Conjugate
00:41:44MDP-Algorithms: theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
00:41:44MDP-Algorithms: theory HOL-Library.Tree_Real
00:41:44Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
00:41:44HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
00:41:44MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
00:41:45HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
00:41:45Timing Probabilistic_System_Zoo (2 threads, 70.850s elapsed time, 125.387s cpu time, 10.973s GC time, factor 1.77)
00:41:45Finished Probabilistic_System_Zoo (0:01:15 elapsed time, 0:02:10 cpu time, factor 1.74)
00:41:45MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
00:41:45HOL-ODE-Numerics: theory Deriving.Derive_Manager
00:41:45HOL-ODE-Numerics: theory Deriving.Compare
00:41:45MDP-Algorithms: theory HOL-Algebra.Complete_Lattice
00:41:45HOL-ODE-Numerics: theory Deriving.Generator_Aux
00:41:45MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
00:41:45Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
00:41:45HOL-ODE-Numerics: theory Deriving.Comparator_Generator
00:41:45MDP-Algorithms: theory HOL-Algebra.Group
00:41:46MDP-Algorithms: theory HOL-Data_Structures.RBT_Set
00:41:46HOL-ODE-Numerics: theory Deriving.Equality_Generator
00:41:46HOL-ODE-Numerics: theory Deriving.Compare_Generator
00:41:46MDP-Algorithms: theory MDP-Algorithms.MDP_fin
00:41:47Frequency_Moments: theory Lp.Lp
00:41:47Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
00:41:47HOL-ODE-Numerics: theory Deriving.Equality_Instances
00:41:47MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
00:41:47MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
00:41:47HOL-ODE-Numerics: theory HOL-Library.AList
00:41:47HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
00:41:47Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
00:41:47MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
00:41:47MDP-Algorithms: theory HOL-Data_Structures.RBT_Map
00:41:47HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
00:41:47Hermite: theory Hermite.Hermite_IArrays
00:41:47MDP-Algorithms: theory HOL-Algebra.Coset
00:41:47HOL-ODE-Numerics: theory HOL-ex.Quicksort
00:41:47MDP-Algorithms: theory HOL-Algebra.FiniteProduct
00:41:48HOL-ODE-Numerics: theory HOL-Library.Char_ord
00:41:48HOL-ODE-Numerics: theory Deriving.Compare_Instances
00:41:48Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
00:41:48MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
00:41:48Frequency_Moments: theory Lehmer.Lehmer
00:41:48Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
00:41:48MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
00:41:48MDP-Algorithms: theory HOL-Algebra.Ring
00:41:49HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
00:41:49HOL-ODE-Numerics: theory HOL-Library.Mapping
00:41:49Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
00:41:49Running Differential_Dynamic_Logic (on 10.195.8.49) ...
00:41:49HOL-ODE-Numerics: theory HOL-Library.Option_ord
00:41:49HOL-ODE-Numerics: theory Automatic_Refinement.Misc
00:41:50Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
00:41:50Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
00:41:50Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
00:41:50MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
00:41:50MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
00:41:51HOL-ODE-Numerics: theory HOL-Library.Parallel
00:41:51MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:41:51MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
00:41:51MDP-Algorithms: theory Show.Show
00:41:51MDP-Algorithms: theory Containers.Collection_Order
00:41:51Frequency_Moments: theory Bertrands_Postulate.Bertrand
00:41:51MDP-Algorithms: theory VectorSpace.FunctionLemmas
00:41:51MDP-Algorithms: theory HOL-Algebra.Module
00:41:51MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
00:41:51MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
00:41:52Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
00:41:52Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
00:41:52HOL-ODE-Numerics: theory HOL-Library.Type_Length
00:41:52MDP-Algorithms: theory Show.Show_Instances
00:41:52Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
00:41:52MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
00:41:52MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
00:41:52MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:41:53HOL-ODE-Numerics: theory HOL-Library.Word
00:41:53MDP-Algorithms: theory VectorSpace.RingModuleFacts
00:41:53MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
00:41:53Projective_Measurements: theory QHLProver.Complex_Matrix
00:41:53MDP-Algorithms: theory VectorSpace.MonoidSums
00:41:54Running Stochastic_Matrices (on of2.proof.cit.tum.de) ...
00:41:54Running Probabilistic_Timed_Automata (on of2.proof.cit.tum.de) ...
00:41:54Running Hidden_Markov_Models (on of2.proof.cit.tum.de) ...
00:41:54MDP-Algorithms: theory VectorSpace.LinearCombinations
00:41:54MDP-Algorithms: theory MDP-Algorithms.Code_Setup
00:41:55MDP-Algorithms: theory Jordan_Normal_Form.Matrix
00:41:56Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
00:41:56Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
00:41:56Probabilistic_Timed_Automata: theory Timed_Automata.Misc
00:41:56Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
00:41:56Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
00:41:56Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
00:41:56Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
00:41:56Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
00:41:56Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
00:41:56Stochastic_Matrices: theory HOL-Eisbach.Eisbach
00:41:56Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
00:41:56Stochastic_Matrices: theory HOL-Algebra.Congruence
00:41:56Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
00:41:56Stochastic_Matrices: theory HOL-Library.More_List
00:41:56Stochastic_Matrices: theory HOL-Library.Function_Algebras
00:41:56Running Fisher_Yates (on of3.proof.cit.tum.de) ...
00:41:56Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
00:41:56Running Monad_Normalisation (on of3.proof.cit.tum.de) ...
00:41:57Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
00:41:57Timing Quick_Sort_Cost (2 threads, 22.634s elapsed time, 41.388s cpu time, 2.820s GC time, factor 1.83)
00:41:57Finished Quick_Sort_Cost (0:00:54 elapsed time, 0:01:19 cpu time, factor 1.47)
00:41:57Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
00:41:57Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
00:41:57Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
00:41:57Hidden_Markov_Models: theory HOL-Library.State_Monad
00:41:57Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
00:41:57Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
00:41:57Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
00:41:57Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
00:41:57Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic
00:41:57Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
00:41:57Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
00:41:57Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
00:41:57Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
00:41:57Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
00:41:57Projective_Measurements: theory QHLProver.Gates
00:41:57Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
00:41:57Stochastic_Matrices: theory HOL-Algebra.Order
00:41:57Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
00:41:57Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
00:41:57Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
00:41:57Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
00:41:57Fisher_Yates: theory Fisher_Yates.Fisher_Yates
00:41:57Timing Randomised_Social_Choice (2 threads, 24.438s elapsed time, 44.315s cpu time, 3.574s GC time, factor 1.81)
00:41:57Finished Randomised_Social_Choice (0:00:55 elapsed time, 0:01:21 cpu time, factor 1.48)
00:41:57Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
00:41:57Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
00:41:57MDP-Algorithms: theory VectorSpace.SumSpaces
00:41:57Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
00:41:57Stochastic_Matrices: theory VectorSpace.FunctionLemmas
00:41:57HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
00:41:57Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
00:41:57Stochastic_Matrices: theory HOL-Algebra.Lattice
00:41:57Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
00:41:57Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
00:41:57MDP-Algorithms: theory VectorSpace.VectorSpace
00:41:58Timing Monad_Normalisation (6 threads, 0.541s elapsed time, 0.888s cpu time, 0.041s GC time, factor 1.64)
00:41:58Finished Monad_Normalisation (0:00:02 elapsed time)
00:41:58Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
00:41:58Hidden_Markov_Models: theory Monad_Memo_DP.Memory
00:41:58Timing Fisher_Yates (6 threads, 0.964s elapsed time, 2.837s cpu time, 0.115s GC time, factor 2.94)
00:41:58Finished Fisher_Yates (0:00:02 elapsed time, 0:00:04 cpu time)
00:41:58Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
00:41:58MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:41:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
00:41:58MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
00:41:59Probabilistic_Timed_Automata: theory Timed_Automata.Regions
00:41:59HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
00:41:59Probabilistic_Timed_Automata: theory Timed_Automata.DBM
00:41:59HOL-ODE-Numerics: theory Automatic_Refinement.Relators
00:41:59Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
00:41:59Stochastic_Matrices: theory HOL-Algebra.Group
00:42:00Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
00:42:00Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
00:42:00Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
00:42:00Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
00:42:00MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
00:42:01HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
00:42:01Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
00:42:01Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
00:42:01Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
00:42:01HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
00:42:01MDP-Algorithms: theory Jordan_Normal_Form.Determinant
00:42:02Probabilistic_Timed_Automata: theory Timed_Automata.Closure
00:42:02Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Prob_Space_Lemmas
00:42:02HOL-ODE-Numerics: theory Collections.SetIterator
00:42:02Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof
00:42:02Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
00:42:02Stochastic_Matrices: theory HOL-Algebra.Coset
00:42:02Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
00:42:02Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
00:42:02HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
00:42:02HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
00:42:02Projective_Measurements: theory Projective_Measurements.Projective_Measurements
00:42:03Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
00:42:03Stochastic_Matrices: theory HOL-Algebra.Ring
00:42:03Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
00:42:03Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:42:03Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
00:42:03Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
00:42:03HOL-ODE-Numerics: theory Collections.SetIteratorOperations
00:42:03Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
00:42:03HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
00:42:03MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
00:42:03MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
00:42:03MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
00:42:03Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
00:42:03Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
00:42:03MDP-Algorithms: theory MDP-Algorithms.Fin_Code
00:42:04HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
00:42:04HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
00:42:04HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
00:42:04MDP-Algorithms: theory MDP-Algorithms.GS_Code
00:42:04Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
00:42:04HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
00:42:04Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
00:42:04MDP-Algorithms: theory MDP-Algorithms.MPI_Code
00:42:04MDP-Algorithms: theory MDP-Algorithms.VI_Code
00:42:04Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
00:42:04MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
00:42:05Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary
00:42:05HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
00:42:05Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
00:42:05Timing CoSMeDis (2 threads, 2487.287s elapsed time, 3831.129s cpu time, 464.029s GC time, factor 1.54)
00:42:05Finished CoSMeDis (0:41:32 elapsed time, 1:04:00 cpu time, factor 1.54)
00:42:05Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
00:42:05Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
00:42:05MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
00:42:06Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:42:06Stochastic_Matrices: theory HOL-Algebra.Module
00:42:06Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
00:42:06Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
00:42:06HOL-ODE-Numerics: theory Collections.Assoc_List
00:42:06Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
00:42:06Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
00:42:06HOL-ODE-Numerics: theory Collections.Diff_Array
00:42:06MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
00:42:07Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
00:42:07Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
00:42:07MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
00:42:08Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
00:42:08Stochastic_Matrices: theory VectorSpace.RingModuleFacts
00:42:08Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
00:42:08MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
00:42:08MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
00:42:08Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
00:42:08Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
00:42:08Stochastic_Matrices: theory VectorSpace.MonoidSums
00:42:08Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
00:42:08HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
00:42:08HOL-ODE-Numerics: theory Collections.Intf_Comp
00:42:08Stochastic_Matrices: theory VectorSpace.LinearCombinations
00:42:08MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
00:42:09MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
00:42:09MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
00:42:09MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
00:42:10Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
00:42:10Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
00:42:10HOL-ODE-Numerics: theory Collections.Idx_Iterator
00:42:11Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
00:42:11HOL-ODE-Numerics: theory Collections.Proper_Iterator
00:42:11Frequency_Moments: theory Finite_Fields.Ring_Characteristic
00:42:11HOL-ODE-Numerics: theory Collections.It_to_It
00:42:11HOL-ODE-Numerics: theory Collections.SetIteratorGA
00:42:12Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
00:42:12Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
00:42:12Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
00:42:12MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
00:42:13HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
00:42:13Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
00:42:13MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
00:42:14HOL-ODE-Numerics: theory Word_Lib.More_Divides
00:42:14Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
00:42:14HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
00:42:15Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
00:42:15Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
00:42:15Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
00:42:15MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
00:42:16Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
00:42:16Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
00:42:16Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
00:42:16Timing Hidden_Markov_Models (6 threads, 19.952s elapsed time, 48.531s cpu time, 5.612s GC time, factor 2.43)
00:42:16Finished Hidden_Markov_Models (0:00:21 elapsed time, 0:00:50 cpu time, factor 2.32)
00:42:17Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
00:42:17Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
00:42:17HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
00:42:18Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
00:42:18MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
00:42:18MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
00:42:19Stochastic_Matrices: theory VectorSpace.SumSpaces
00:42:19Stochastic_Matrices: theory VectorSpace.VectorSpace
00:42:19HOL-ODE-Numerics: theory HOL-Library.Signed_Division
00:42:19Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:42:20Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
00:42:20HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
00:42:20Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
00:42:20MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
00:42:21HOL-ODE-Numerics: theory HOL-Library.While_Combinator
00:42:21MDP-Algorithms: theory Containers.RBT_ext
00:42:21MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
00:42:21Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
00:42:21Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
00:42:21Building CryptHOL (on of1-proof+0-7) ...
00:42:21Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
00:42:21HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
00:42:21Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
00:42:21MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
00:42:22HOL-ODE-Numerics: theory Deriving.Countable_Generator
00:42:22Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
00:42:22Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
00:42:22Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
00:42:22Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
00:42:22HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
00:42:22Frequency_Moments: theory Frequency_Moments.Frequency_Moments
00:42:22HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
00:42:22CryptHOL: theory HOL-Eisbach.Eisbach
00:42:22CryptHOL: theory Applicative_Lifting.Applicative
00:42:22CryptHOL: theory CryptHOL.Partial_Function_Set
00:42:22CryptHOL: theory HOL-Library.Case_Converter
00:42:22CryptHOL: theory HOL-Algebra.Congruence
00:42:22CryptHOL: theory HOL-Library.Function_Algebras
00:42:22CryptHOL: theory HOL-Library.Countable_Set_Type
00:42:22CryptHOL: theory HOL-Library.Type_Length
00:42:23CryptHOL: theory Coinductive.Coinductive_Nat
00:42:23Frequency_Moments: theory Frequency_Moments.K_Smallest
00:42:23HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
00:42:23CryptHOL: theory HOL-Library.Simps_Case_Conv
00:42:23CryptHOL: theory Monad_Normalisation.Monad_Normalisation
00:42:23CryptHOL: theory Landau_Symbols.Group_Sort
00:42:23HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
00:42:23Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
00:42:23Frequency_Moments: theory Frequency_Moments.Probability_Ext
00:42:23CryptHOL: theory HOL-Algebra.Order
00:42:24HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
00:42:24HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
00:42:24CryptHOL: theory Coinductive.Coinductive_List
00:42:24CryptHOL: theory Applicative_Lifting.Applicative_Environment
00:42:24CryptHOL: theory Applicative_Lifting.Applicative_Set
00:42:24CryptHOL: theory Applicative_Lifting.Applicative_PMF
00:42:24CryptHOL: theory CryptHOL.Environment_Functor
00:42:24CryptHOL: theory CryptHOL.Set_Applicative
00:42:24CryptHOL: theory Landau_Symbols.Landau_Real_Products
00:42:24CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
00:42:25Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
00:42:25CryptHOL: theory HOL-Algebra.Lattice
00:42:26Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
00:42:26Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
00:42:26HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
00:42:26Building Random_BSTs (on 10.195.7.194) ...
00:42:26Running SDS_Impossibility (on 10.195.7.194) ...
00:42:26Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
00:42:26Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
00:42:26CryptHOL: theory CryptHOL.SPMF_Applicative
00:42:26HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
00:42:26CryptHOL: theory HOL-Algebra.Complete_Lattice
00:42:26MDP-Algorithms: theory Containers.RBT_Mapping2
00:42:27HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
00:42:27CryptHOL: theory HOL-Algebra.Group
00:42:27CryptHOL: theory Landau_Symbols.Landau_Simprocs
00:42:27MDP-Algorithms: theory Containers.RBT_Set2
00:42:28Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility
00:42:28HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
00:42:28CryptHOL: theory Landau_Symbols.Landau_More
00:42:28CryptHOL: theory CryptHOL.Negligible
00:42:28SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
00:42:28CryptHOL: theory HOL-Algebra.Coset
00:42:29Random_BSTs: theory HOL-Data_Structures.Less_False
00:42:29Random_BSTs: theory HOL-Data_Structures.Cmp
00:42:29MDP-Algorithms: theory Containers.Set_Impl
00:42:30Random_BSTs: theory HOL-Data_Structures.Sorted_Less
00:42:30Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
00:42:30Random_BSTs: theory HOL-Data_Structures.Set_Specs
00:42:30Random_BSTs: theory HOL-Data_Structures.Tree_Set
00:42:30CryptHOL: theory Coinductive.TLList
00:42:30CryptHOL: theory CryptHOL.Cyclic_Group
00:42:31Random_BSTs: theory Random_BSTs.Random_BSTs
00:42:31CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
00:42:32Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
00:42:32HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
00:42:32Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
00:42:33Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
00:42:33Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
00:42:34Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
00:42:35Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
00:42:35Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
00:42:36Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
00:42:37Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
00:42:37Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
00:42:37Timing Turans_Graph_Theorem (2 threads, 130.770s elapsed time, 233.252s cpu time, 22.341s GC time, factor 1.78)
00:42:37Finished Turans_Graph_Theorem (0:02:15 elapsed time, 0:03:59 cpu time, factor 1.76)
00:42:37Timing MFMC_Countable (2 threads, 130.817s elapsed time, 219.367s cpu time, 10.589s GC time, factor 1.68)
00:42:37Finished MFMC_Countable (0:02:15 elapsed time, 0:03:44 cpu time, factor 1.66)
00:42:37HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
00:42:38Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
00:42:38Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
00:42:39Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
00:42:41Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
00:42:42CryptHOL: theory CryptHOL.Misc_CryptHOL
00:42:43MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
00:42:45Timing E_Transcendental (2 threads, 164.548s elapsed time, 286.296s cpu time, 21.018s GC time, factor 1.74)
00:42:45Finished E_Transcendental (0:03:18 elapsed time, 0:05:31 cpu time, factor 1.67)
00:42:45MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
00:42:46MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
00:42:46CryptHOL: theory CryptHOL.Generat
00:42:46CryptHOL: theory CryptHOL.List_Bits
00:42:46CryptHOL: theory CryptHOL.Resumption
00:42:47MDP-Algorithms: theory MDP-Algorithms.PI_Code
00:42:48HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
00:42:49HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
00:42:49CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
00:42:52HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
00:42:53HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
00:42:54HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
00:42:54HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
00:42:54HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
00:42:55HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
00:42:55HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
00:42:56HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
00:42:56HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
00:42:56HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
00:42:56HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
00:42:56MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
00:42:57CryptHOL: theory CryptHOL.Computational_Model
00:42:57CryptHOL: theory CryptHOL.GPV_Applicative
00:42:58Timing List_Update (2 threads, 153.026s elapsed time, 252.996s cpu time, 18.016s GC time, factor 1.65)
00:42:58Finished List_Update (0:02:38 elapsed time, 0:04:19 cpu time, factor 1.64)
00:42:58Timing Count_Complex_Roots (2 threads, 169.732s elapsed time, 324.824s cpu time, 18.489s GC time, factor 1.91)
00:42:58Finished Count_Complex_Roots (0:03:28 elapsed time, 0:06:14 cpu time, factor 1.79)
00:42:58MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
00:42:58HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
00:42:58Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
00:42:58CryptHOL: theory CryptHOL.GPV_Expectation
00:42:59Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
00:42:59CryptHOL: theory CryptHOL.GPV_Bisim
00:43:00CryptHOL: theory CryptHOL.CryptHOL
00:43:02Building Pi_Transcendental (on 10.195.8.29) ...
00:43:04Timing Ergodic_Theory (2 threads, 122.644s elapsed time, 216.293s cpu time, 8.609s GC time, factor 1.76)
00:43:04Finished Ergodic_Theory (0:02:41 elapsed time, 0:04:24 cpu time, factor 1.64)
00:43:05Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
00:43:05Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
00:43:05HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
00:43:05Timing Random_BSTs (2 threads, 8.628s elapsed time, 13.565s cpu time, 1.319s GC time, factor 1.57)
00:43:05HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
00:43:05Finished Random_BSTs (0:00:38 elapsed time, 0:00:49 cpu time, factor 1.30)
00:43:05HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
00:43:05Timing Hermite (2 threads, 59.032s elapsed time, 93.766s cpu time, 4.828s GC time, factor 1.59)
00:43:05Finished Hermite (0:01:25 elapsed time, 0:02:05 cpu time, factor 1.48)
00:43:06HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
00:43:06Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
00:43:06HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
00:43:06Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
00:43:06Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
00:43:07Pi_Transcendental: theory HOL-Library.Fun_Lexorder
00:43:07Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
00:43:07Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:43:07Pi_Transcendental: theory HOL-Library.Poly_Mapping
00:43:07Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
00:43:08HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
00:43:09HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
00:43:09HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
00:43:09Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
00:43:09Timing Girth_Chromatic (2 threads, 114.527s elapsed time, 207.179s cpu time, 17.086s GC time, factor 1.81)
00:43:09Finished Girth_Chromatic (0:02:37 elapsed time, 0:04:20 cpu time, factor 1.66)
00:43:10Pi_Transcendental: theory Polynomials.MPoly_Type
00:43:10Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
00:43:10Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
00:43:10Pi_Transcendental: theory Polynomials.More_MPoly_Type
00:43:11Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
00:43:11Pi_Transcendental: theory Symmetric_Polynomials.Vieta
00:43:12HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
00:43:12Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
00:43:14Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
00:43:14HOL-ODE-Numerics: theory HOL-Library.RBT
00:43:15Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
00:43:17HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
00:43:17HOL-ODE-Numerics: theory Show.Show
00:43:17HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
00:43:18Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
00:43:18HOL-ODE-Numerics: theory Collections.Gen_Iterator
00:43:19HOL-ODE-Numerics: theory Collections.Intf_Map
00:43:19HOL-ODE-Numerics: theory Collections.Iterator
00:43:19HOL-ODE-Numerics: theory Collections.Intf_Set
00:43:20HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
00:43:20HOL-ODE-Numerics: theory Collections.Array_Iterator
00:43:20HOL-ODE-Numerics: theory Collections.RBT_add
00:43:20HOL-ODE-Numerics: theory Collections.Gen_Map
00:43:21HOL-ODE-Numerics: theory Collections.Impl_Array_Map
00:43:21HOL-ODE-Numerics: theory Collections.Impl_List_Map
00:43:22HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
00:43:22HOL-ODE-Numerics: theory Collections.Gen_Map2Set
00:43:23HOL-ODE-Numerics: theory Collections.Gen_Set
00:43:23Timing Probabilistic_Timed_Automata (6 threads, 86.139s elapsed time, 320.029s cpu time, 60.676s GC time, factor 3.72)
00:43:23Finished Probabilistic_Timed_Automata (0:01:28 elapsed time, 0:05:23 cpu time, factor 3.66)
00:43:25HOL-ODE-Numerics: theory Collections.Impl_List_Set
00:43:25HOL-ODE-Numerics: theory Show.Show_Instances
00:43:26Building Smith_Normal_Form (on 10.195.8.46) ...
00:43:27HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
00:43:27HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
00:43:27Timing CryptHOL (8 threads, 44.224s elapsed time, 235.831s cpu time, 21.989s GC time, factor 5.33)
00:43:27Finished CryptHOL (0:01:04 elapsed time, 0:04:37 cpu time, factor 4.30)
00:43:28HOL-ODE-Numerics: theory Word_Lib.More_Word
00:43:29Timing Bernoulli (2 threads, 189.718s elapsed time, 322.808s cpu time, 26.346s GC time, factor 1.70)
00:43:29Finished Bernoulli (0:03:55 elapsed time, 0:06:18 cpu time, factor 1.61)
00:43:30HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
00:43:30HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
00:43:30Smith_Normal_Form: theory HOL-Eisbach.Eisbach
00:43:30Smith_Normal_Form: theory Deriving.Derive_Manager
00:43:30Smith_Normal_Form: theory Deriving.Generator_Aux
00:43:30HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
00:43:31Smith_Normal_Form: theory HOL-Number_Theory.Cong
00:43:31Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
00:43:31Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
00:43:31HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
00:43:31Timing SDS_Impossibility (2 threads, 61.285s elapsed time, 83.724s cpu time, 6.657s GC time, factor 1.37)
00:43:31Finished SDS_Impossibility (0:01:04 elapsed time, 0:01:27 cpu time, factor 1.35)
00:43:31Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
00:43:31HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
00:43:31Smith_Normal_Form: theory HOL-Algebra.Congruence
00:43:32Smith_Normal_Form: theory HOL-Algebra.Order
00:43:32Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
00:43:32HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
00:43:32HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
00:43:32Running Linear_Recurrences (on 10.195.7.194) ...
00:43:33Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
00:43:33Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
00:43:33Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
00:43:33Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
00:43:33Smith_Normal_Form: theory HOL-Algebra.Lattice
00:43:33Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
00:43:34Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
00:43:35Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
00:43:35Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
00:43:35Running Randomised_BSTs (on 10.195.8.29) ...
00:43:36Smith_Normal_Form: theory HOL-Algebra.Group
00:43:36Timing Stochastic_Matrices (6 threads, 98.421s elapsed time, 384.240s cpu time, 64.079s GC time, factor 3.90)
00:43:36Finished Stochastic_Matrices (0:01:40 elapsed time, 0:06:29 cpu time, factor 3.86)
00:43:36Linear_Recurrences: theory HOL-Combinatorics.Stirling
00:43:36Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure
00:43:37Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers
00:43:37Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:43:37Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree
00:43:37Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat
00:43:38Linear_Recurrences: theory HOL-Library.Code_Target_Nat
00:43:38Running Random_Graph_Subgraph_Threshold (on 10.195.8.49) ...
00:43:38Linear_Recurrences: theory HOL-Library.Code_Target_Int
00:43:38Running Szemeredi_Regularity (on 10.195.8.49) ...
00:43:38Linear_Recurrences: theory HOL-Library.Sublist
00:43:38Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
00:43:38Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
00:43:38Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
00:43:38Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
00:43:39Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
00:43:39Smith_Normal_Form: theory HOL-Algebra.Coset
00:43:39Running Laws_of_Large_Numbers (on 10.195.8.30) ...
00:43:40Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
00:43:40Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial
00:43:40Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Irreducibility
00:43:40Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:43:40Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
00:43:40Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
00:43:41Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
00:43:41Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
00:43:41Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
00:43:41Linear_Recurrences: theory Linear_Recurrences.Factorizations
00:43:41Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
00:43:41Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials
00:43:41Linear_Recurrences: theory Linear_Recurrences.RatFPS
00:43:42Smith_Normal_Form: theory HOL-Algebra.Ring
00:43:42Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
00:43:42Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
00:43:43Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
00:43:43Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
00:43:43Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
00:43:44Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
00:43:44HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
00:43:44Linear_Recurrences: theory Matrix.Utility
00:43:44Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
00:43:44Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
00:43:44Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
00:43:44Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
00:43:44Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
00:43:45Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
00:43:45Timing Roth_Arithmetic_Progressions (2 threads, 189.404s elapsed time, 350.183s cpu time, 29.066s GC time, factor 1.85)
00:43:45Finished Roth_Arithmetic_Progressions (0:03:14 elapsed time, 0:05:56 cpu time, factor 1.84)
00:43:45Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
00:43:46HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
00:43:46Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
00:43:46Timing Probabilistic_Noninterference (2 threads, 201.487s elapsed time, 328.122s cpu time, 21.046s GC time, factor 1.63)
00:43:46Finished Probabilistic_Noninterference (0:03:26 elapsed time, 0:05:34 cpu time, factor 1.62)
00:43:46HOL-ODE-Numerics: theory Collections.Code_Target_ICF
00:43:46Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:43:46Timing Laws_of_Large_Numbers (2 threads, 2.643s elapsed time, 4.204s cpu time, 0.182s GC time, factor 1.59)
00:43:46Finished Laws_of_Large_Numbers (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.19)
00:43:46HOL-ODE-Numerics: theory Native_Word.Uint
00:43:46HOL-ODE-Numerics: theory Native_Word.Uint32
00:43:46Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
00:43:47Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
00:43:47Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
00:43:47HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
00:43:47Smith_Normal_Form: theory HOL-Algebra.AbelCoset
00:43:48Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
00:43:48HOL-ODE-Numerics: theory Collections.HashCode
00:43:49HOL-ODE-Numerics: theory Collections.Intf_Hash
00:43:50HOL-ODE-Numerics: theory Collections.Gen_Hash
00:43:50HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
00:43:50Timing Szemeredi_Regularity (2 threads, 8.727s elapsed time, 14.097s cpu time, 0.413s GC time, factor 1.62)
00:43:50Finished Szemeredi_Regularity (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.42)
00:43:51Smith_Normal_Form: theory HOL-Algebra.Ideal
00:43:51Smith_Normal_Form: theory HOL-Algebra.Module
00:43:52Timing Randomised_BSTs (2 threads, 13.813s elapsed time, 24.558s cpu time, 0.893s GC time, factor 1.78)
00:43:52Finished Randomised_BSTs (0:00:17 elapsed time, 0:00:27 cpu time, factor 1.61)
00:43:53Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
00:43:54Timing Random_Graph_Subgraph_Threshold (2 threads, 12.251s elapsed time, 21.892s cpu time, 0.768s GC time, factor 1.79)
00:43:54Finished Random_Graph_Subgraph_Threshold (0:00:15 elapsed time, 0:00:24 cpu time, factor 1.61)
00:43:54Smith_Normal_Form: theory HOL-Algebra.RingHom
00:43:54HOL-ODE-Numerics: theory Deriving.Hash_Generator
00:43:55HOL-ODE-Numerics: theory Deriving.Hash_Instances
00:43:55HOL-ODE-Numerics: theory Deriving.Derive
00:43:55Smith_Normal_Form: theory HOL-Algebra.UnivPoly
00:43:56HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
00:43:57Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
00:43:57Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
00:43:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
00:43:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
00:43:58Smith_Normal_Form: theory HOL-Number_Theory.Totient
00:43:59Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
00:43:59Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
00:43:59Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
00:43:59Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
00:44:00Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
00:44:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
00:44:01Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
00:44:02Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
00:44:02Smith_Normal_Form: theory List-Index.List_Index
00:44:02Building Constructive_Cryptography (on of1-proof+0-7) ...
00:44:03Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
00:44:03HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
00:44:04Constructive_Cryptography: theory Constructive_Cryptography.Resource
00:44:05Constructive_Cryptography: theory Constructive_Cryptography.Converter
00:44:07HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
00:44:07Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
00:44:07Building Game_Based_Crypto (on 10.195.7.194) ...
00:44:07HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
00:44:08Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
00:44:08CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
00:44:10Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
00:44:10HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
00:44:10Running Sigma_Commit_Crypto (on 10.195.8.29) ...
00:44:10Constructive_Cryptography: theory Constructive_Cryptography.Random_System
00:44:11Game_Based_Crypto: theory HOL-Library.LaTeXsugar
00:44:11Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
00:44:11Smith_Normal_Form: theory HOL-Number_Theory.Residues
00:44:11Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
00:44:11Constructive_Cryptography: theory Constructive_Cryptography.Wiring
00:44:12Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
00:44:12Building Stirling_Formula (on 10.195.8.40) ...
00:44:12HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
00:44:12Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
00:44:12Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
00:44:12Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
00:44:12Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
00:44:12HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
00:44:12Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
00:44:13Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:44:13Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
00:44:13Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
00:44:13Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
00:44:13Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
00:44:14Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
00:44:14Running Euler_MacLaurin (on 10.195.8.49) ...
00:44:14Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
00:44:14HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
00:44:14Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
00:44:14Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
00:44:14Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
00:44:14Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
00:44:15Stirling_Formula: theory HOL-Library.Function_Algebras
00:44:15Stirling_Formula: theory Landau_Symbols.Group_Sort
00:44:15Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
00:44:15Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
00:44:15Running ABY3_Protocols (on 10.195.8.49) ...
00:44:15Sigma_Commit_Crypto: theory HOL-Algebra.Ring
00:44:15Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
00:44:15Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
00:44:16Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
00:44:16Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
00:44:16Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
00:44:16Timing S_Finite_Measure_Monad (2 threads, 221.632s elapsed time, 372.137s cpu time, 32.421s GC time, factor 1.68)
00:44:16Finished S_Finite_Measure_Monad (0:03:45 elapsed time, 0:06:17 cpu time, factor 1.67)
00:44:17Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
00:44:17HOL-ODE-Numerics: theory Affine_Arithmetic.Print
00:44:17Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
00:44:17Running Lambert_W (on 10.195.8.30) ...
00:44:17Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
00:44:18Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
00:44:18Euler_MacLaurin: theory HOL-Library.Function_Algebras
00:44:18Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
00:44:18Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
00:44:18Euler_MacLaurin: theory Landau_Symbols.Group_Sort
00:44:18ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
00:44:18ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
00:44:18Smith_Normal_Form: theory Show.Show
00:44:18Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
00:44:19Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
00:44:19ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
00:44:19HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
00:44:19Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
00:44:19Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
00:44:19Constructive_Cryptography: theory Constructive_Cryptography.Examples
00:44:21Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
00:44:21Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
00:44:21HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
00:44:21Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
00:44:21Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
00:44:21Lambert_W: theory HOL-Library.Function_Algebras
00:44:22Lambert_W: theory Lambert_W.Lambert_W
00:44:22Smith_Normal_Form: theory Show.Show_Instances
00:44:22Lambert_W: theory Landau_Symbols.Group_Sort
00:44:22HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
00:44:22Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
00:44:22Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
00:44:22ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
00:44:23Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
00:44:23ABY3_Protocols: theory ABY3_Protocols.Multiplication
00:44:23Smith_Normal_Form: theory Show.Show_Poly
00:44:23ABY3_Protocols: theory ABY3_Protocols.Shuffle
00:44:23Timing Pi_Transcendental (2 threads, 51.733s elapsed time, 92.330s cpu time, 5.974s GC time, factor 1.78)
00:44:23Finished Pi_Transcendental (0:01:20 elapsed time, 0:02:09 cpu time, factor 1.60)
00:44:23HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
00:44:23ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
00:44:23Stirling_Formula: theory Landau_Symbols.Landau_More
00:44:23Lambert_W: theory Landau_Symbols.Landau_Real_Products
00:44:23Timing MDP-Algorithms (8 threads, 158.695s elapsed time, 919.953s cpu time, 93.263s GC time, factor 5.80)
00:44:23Finished MDP-Algorithms (0:02:42 elapsed time, 0:15:33 cpu time, factor 5.76)
00:44:24Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
00:44:24Stirling_Formula: theory Stirling_Formula.Stirling_Formula
00:44:24Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
00:44:24Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
00:44:24Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
00:44:25Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
00:44:25Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
00:44:26Sigma_Commit_Crypto: theory HOL-Algebra.Module
00:44:26Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
00:44:26Smith_Normal_Form: theory VectorSpace.FunctionLemmas
00:44:26Smith_Normal_Form: theory VectorSpace.RingModuleFacts
00:44:27Euler_MacLaurin: theory Landau_Symbols.Landau_More
00:44:27Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
00:44:27Smith_Normal_Form: theory VectorSpace.MonoidSums
00:44:27Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
00:44:27Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
00:44:27Smith_Normal_Form: theory VectorSpace.LinearCombinations
00:44:28Lambert_W: theory Landau_Symbols.Landau_Simprocs
00:44:28Timing Hybrid_Systems_VCs (2 threads, 523.356s elapsed time, 854.233s cpu time, 175.021s GC time, factor 1.63)
00:44:28Finished Hybrid_Systems_VCs (0:08:48 elapsed time, 0:14:21 cpu time, factor 1.63)
00:44:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
00:44:29Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
00:44:29Lambert_W: theory Landau_Symbols.Landau_More
00:44:29Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
00:44:29Lambert_W: theory Stirling_Formula.Stirling_Formula
00:44:30Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
00:44:30Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
00:44:31Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series
00:44:31Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
00:44:31Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
00:44:32Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
00:44:32Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
00:44:33HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
00:44:33Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
00:44:33Smith_Normal_Form: theory VectorSpace.SumSpaces
00:44:34Smith_Normal_Form: theory VectorSpace.VectorSpace
00:44:35HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
00:44:36Timing ABY3_Protocols (2 threads, 16.459s elapsed time, 31.061s cpu time, 1.075s GC time, factor 1.89)
00:44:36Finished ABY3_Protocols (0:00:19 elapsed time, 0:00:34 cpu time, factor 1.72)
00:44:36Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
00:44:39Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
00:44:40HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
00:44:41Running Hermite_Lindemann (on of1-proof+8-15) ...
00:44:42Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
00:44:42Timing Euler_MacLaurin (2 threads, 22.094s elapsed time, 42.411s cpu time, 2.422s GC time, factor 1.92)
00:44:42Finished Euler_MacLaurin (0:00:25 elapsed time, 0:00:45 cpu time, factor 1.80)
00:44:42HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
00:44:42Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
00:44:42Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
00:44:42Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
00:44:42Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
00:44:42Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
00:44:42Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
00:44:42Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
00:44:42Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
00:44:42Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
00:44:42Hermite_Lindemann: theory HOL-Library.Monad_Syntax
00:44:42Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
00:44:42Hermite_Lindemann: theory HOL-Algebra.Divisibility
00:44:42Hermite_Lindemann: theory Containers.Containers_Auxiliary
00:44:43Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
00:44:43Hermite_Lindemann: theory Matrix.Utility
00:44:43Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
00:44:43Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
00:44:43Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
00:44:44Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
00:44:44Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
00:44:45HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
00:44:45Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
00:44:45Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
00:44:45Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
00:44:45Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:44:45Timing Lambert_W (2 threads, 23.321s elapsed time, 43.364s cpu time, 2.887s GC time, factor 1.86)
00:44:45Finished Lambert_W (0:00:27 elapsed time, 0:00:47 cpu time, factor 1.73)
00:44:45Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
00:44:46Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
00:44:46Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
00:44:46Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
00:44:47Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
00:44:47Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
00:44:47Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
00:44:48HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
00:44:48HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
00:44:49Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
00:44:49Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
00:44:49Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
00:44:49Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
00:44:50Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:44:51Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
00:44:51Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
00:44:52Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
00:44:53Timing Balog_Szemeredi_Gowers (2 threads, 252.898s elapsed time, 464.701s cpu time, 37.219s GC time, factor 1.84)
00:44:53Finished Balog_Szemeredi_Gowers (0:04:17 elapsed time, 0:07:51 cpu time, factor 1.83)
00:44:53Hermite_Lindemann: theory Subresultants.More_Homomorphisms
00:44:53Hermite_Lindemann: theory Subresultants.Resultant_Prelim
00:44:54Timing Transcendence_Series_Hancl_Rucki (2 threads, 328.646s elapsed time, 588.986s cpu time, 47.617s GC time, factor 1.79)
00:44:54Finished Transcendence_Series_Hancl_Rucki (0:05:33 elapsed time, 0:09:56 cpu time, factor 1.79)
00:44:55Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
00:44:55Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
00:44:55Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
00:44:55Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
00:44:56Timing Linear_Recurrences (2 threads, 78.389s elapsed time, 142.344s cpu time, 10.638s GC time, factor 1.82)
00:44:56Finished Linear_Recurrences (0:01:22 elapsed time, 0:02:27 cpu time, factor 1.78)
00:44:57Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
00:44:57Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
00:44:57CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
00:44:57CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
00:44:57HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
00:44:57Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
00:44:57Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
00:44:57HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
00:44:57Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
00:44:58Hermite_Lindemann: theory Algebraic_Numbers.Resultant
00:44:58Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
00:44:59Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
00:44:59Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
00:45:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
00:45:01Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
00:45:01Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
00:45:01Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
00:45:01Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
00:45:02Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
00:45:02Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
00:45:03HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
00:45:04Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
00:45:06Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
00:45:09Timing CAVA_LTL_Modelchecker (2 threads, 436.017s elapsed time, 526.095s cpu time, 69.313s GC time, factor 1.21)
00:45:09Finished CAVA_LTL_Modelchecker (0:07:21 elapsed time, 0:08:52 cpu time, factor 1.21)
00:45:09HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
00:45:10Timing Stirling_Formula (2 threads, 25.667s elapsed time, 48.818s cpu time, 3.018s GC time, factor 1.90)
00:45:10Finished Stirling_Formula (0:00:56 elapsed time, 0:01:25 cpu time, factor 1.51)
00:45:11Timing Constructive_Cryptography (8 threads, 52.520s elapsed time, 143.135s cpu time, 6.079s GC time, factor 2.73)
00:45:11Finished Constructive_Cryptography (0:01:08 elapsed time, 0:02:50 cpu time, factor 2.50)
00:45:14Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
00:45:14Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
00:45:15Timing Hermite_Lindemann (8 threads, 31.409s elapsed time, 200.436s cpu time, 17.615s GC time, factor 6.38)
00:45:15Finished Hermite_Lindemann (0:00:33 elapsed time, 0:03:24 cpu time, factor 6.12)
00:45:18Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
00:45:19Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
00:45:22Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
00:45:22Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
00:45:23Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
00:45:23Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
00:45:23Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
00:45:26Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
00:45:27Running Constructive_Cryptography_CM (on 10.195.8.46) ...
00:45:28Timing Schwartz_Zippel (2 threads, 299.604s elapsed time, 537.845s cpu time, 65.379s GC time, factor 1.80)
00:45:28Finished Schwartz_Zippel (0:05:06 elapsed time, 0:09:08 cpu time, factor 1.79)
00:45:28Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
00:45:29Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
00:45:29Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
00:45:29Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
00:45:31Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
00:45:31Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
00:45:32Running Clique_and_Monotone_Circuits (on 10.195.8.42) ...
00:45:32Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
00:45:32Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
00:45:32Running Irrationals_From_THEBOOK (on of1-proof+8-15) ...
00:45:32Running Comparison_Sort_Lower_Bound (on of1-proof+0-7) ...
00:45:33Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
00:45:33Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
00:45:33Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
00:45:33Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
00:45:33Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
00:45:33Comparison_Sort_Lower_Bound: theory List-Index.List_Index
00:45:34Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
00:45:34Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
00:45:35Timing Irrationals_From_THEBOOK (8 threads, 1.130s elapsed time, 3.168s cpu time, 0.080s GC time, factor 2.80)
00:45:35Finished Irrationals_From_THEBOOK (0:00:02 elapsed time, 0:00:04 cpu time)
00:45:37Timing Comparison_Sort_Lower_Bound (8 threads, 2.904s elapsed time, 8.830s cpu time, 0.824s GC time, factor 3.04)
00:45:37Finished Comparison_Sort_Lower_Bound (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.32)
00:45:40Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
00:45:41Timing Game_Based_Crypto (2 threads, 53.339s elapsed time, 98.393s cpu time, 5.373s GC time, factor 1.84)
00:45:41Finished Game_Based_Crypto (0:01:32 elapsed time, 0:02:27 cpu time, factor 1.59)
00:45:41Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
00:45:41Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
00:45:42Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
00:45:43Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
00:45:48HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
00:45:48HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
00:45:49Timing SC_DOM_Components (2 threads, 990.481s elapsed time, 1903.563s cpu time, 264.923s GC time, factor 1.92)
00:45:49Finished SC_DOM_Components (0:16:35 elapsed time, 0:31:50 cpu time, factor 1.92)
00:45:51Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
00:45:51Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
00:45:54Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
00:45:54Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
00:45:54Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
00:45:54CakeML_Codegen: theory Lazy_Case.Lazy_Case
00:45:55CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
00:45:55CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
00:45:55Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
00:45:56Running Multi_Party_Computation (on of1-proof+0-7) ...
00:45:58Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
00:45:58Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
00:45:58Multi_Party_Computation: theory HOL-Number_Theory.Cong
00:45:58Multi_Party_Computation: theory Multi_Party_Computation.ETP
00:45:58Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
00:45:58Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
00:45:58Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
00:45:58Multi_Party_Computation: theory HOL-Algebra.Ring
00:45:59Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
00:45:59Multi_Party_Computation: theory HOL-Number_Theory.Totient
00:45:59Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
00:45:59Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
00:45:59Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
00:45:59Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
00:46:00Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
00:46:00Multi_Party_Computation: theory Multi_Party_Computation.OT14
00:46:00Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
00:46:01Multi_Party_Computation: theory HOL-Algebra.AbelCoset
00:46:01Multi_Party_Computation: theory HOL-Algebra.Module
00:46:02HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
00:46:02Multi_Party_Computation: theory Multi_Party_Computation.GMW
00:46:03CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
00:46:04Multi_Party_Computation: theory HOL-Algebra.Ideal
00:46:06CakeML_Codegen: theory CakeML_Codegen.Test_Composition
00:46:06Multi_Party_Computation: theory HOL-Algebra.RingHom
00:46:06Multi_Party_Computation: theory HOL-Algebra.UnivPoly
00:46:09Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
00:46:10Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
00:46:13CakeML_Codegen: theory CakeML_Codegen.Test_Print
00:46:15Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
00:46:17Multi_Party_Computation: theory HOL-Number_Theory.Residues
00:46:19Timing Deep_Learning (2 threads, 358.729s elapsed time, 649.873s cpu time, 138.002s GC time, factor 1.81)
00:46:19Finished Deep_Learning (0:06:03 elapsed time, 0:10:57 cpu time, factor 1.81)
00:46:20Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
00:46:20Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
00:46:20Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
00:46:21Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
00:46:21Timing DOM_Components (2 threads, 412.408s elapsed time, 805.702s cpu time, 39.331s GC time, factor 1.95)
00:46:21Finished DOM_Components (0:06:57 elapsed time, 0:13:32 cpu time, factor 1.95)
00:46:22Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
00:46:23Timing Universal_Hash_Families (2 threads, 363.140s elapsed time, 665.928s cpu time, 233.103s GC time, factor 1.83)
00:46:23Finished Universal_Hash_Families (0:06:08 elapsed time, 0:11:13 cpu time, factor 1.83)
00:46:24Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
00:46:24Timing Dirichlet_Series (2 threads, 360.298s elapsed time, 638.195s cpu time, 152.901s GC time, factor 1.77)
00:46:24Finished Dirichlet_Series (0:06:55 elapsed time, 0:11:46 cpu time, factor 1.70)
00:46:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
00:46:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
00:46:33Timing Virtual_Substitution (2 threads, 652.039s elapsed time, 1067.332s cpu time, 224.192s GC time, factor 1.64)
00:46:33Finished Virtual_Substitution (0:10:59 elapsed time, 0:17:57 cpu time, factor 1.64)
00:46:43Building Zeta_Function (on 10.195.7.194) ...
00:46:43Running Gauss_Sums (on 10.195.7.194) ...
00:46:44Timing Multi_Party_Computation (8 threads, 44.950s elapsed time, 268.730s cpu time, 22.164s GC time, factor 5.98)
00:46:44Finished Multi_Party_Computation (0:00:47 elapsed time, 0:04:32 cpu time, factor 5.78)
00:46:46Timing Clique_and_Monotone_Circuits (2 threads, 54.403s elapsed time, 72.610s cpu time, 2.764s GC time, factor 1.33)
00:46:46Finished Clique_and_Monotone_Circuits (0:01:13 elapsed time, 0:01:16 cpu time, factor 1.04)
00:46:47Zeta_Function: theory Bernoulli.Bernoulli_Zeta
00:46:47Gauss_Sums: theory HOL-Algebra.QuotRing
00:46:47Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
00:46:50Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
00:46:50Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
00:46:51Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
00:46:52Gauss_Sums: theory HOL-Algebra.IntRing
00:46:52Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
00:46:53Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
00:46:53Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
00:46:54Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
00:46:54Zeta_Function: theory HOL-Eisbach.Eisbach
00:46:54Zeta_Function: theory Pure-ex.Guess
00:46:54Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
00:46:54Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
00:46:55Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
00:46:55Zeta_Function: theory Sturm_Tarski.PolyMisc
00:46:55Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
00:46:55Zeta_Function: theory Winding_Number_Eval.Missing_Topology
00:46:55Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
00:46:55Zeta_Function: theory Zeta_Function.Zeta_Library
00:46:55Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
00:46:57Zeta_Function: theory Budan_Fourier.BF_Misc
00:46:57Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
00:46:57Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
00:46:58Timing Sigma_Commit_Crypto (2 threads, 160.826s elapsed time, 278.574s cpu time, 23.700s GC time, factor 1.73)
00:46:58Finished Sigma_Commit_Crypto (0:02:45 elapsed time, 0:04:44 cpu time, factor 1.72)
00:46:58Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
00:46:58Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
00:46:58Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
00:46:58Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
00:46:58Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
00:46:59Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
00:47:00Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
00:47:00Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
00:47:00Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
00:47:02Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
00:47:03Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
00:47:04Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
00:47:04Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
00:47:06Zeta_Function: theory Zeta_Function.Zeta_Function
00:47:06Gauss_Sums: theory Gauss_Sums.Gauss_Sums
00:47:08Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
00:47:10Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
00:47:11Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
00:47:15Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
00:47:30Timing Affine_Arithmetic (2 threads, 641.462s elapsed time, 1114.302s cpu time, 79.959s GC time, factor 1.74)
00:47:30Finished Affine_Arithmetic (0:11:55 elapsed time, 0:20:20 cpu time, factor 1.71)
00:47:40Running Taylor_Models (on 10.195.7.194) ...
00:47:44Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
00:47:44Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
00:47:56HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
00:47:56HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
00:48:00Taylor_Models: theory Taylor_Models.Polynomial_Expression
00:48:03HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
00:48:12Timing Gauss_Sums (2 threads, 82.551s elapsed time, 148.471s cpu time, 13.453s GC time, factor 1.80)
00:48:12Finished Gauss_Sums (0:01:27 elapsed time, 0:02:33 cpu time, factor 1.76)
00:48:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
00:48:17HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
00:48:20Timing Differential_Dynamic_Logic (2 threads, 383.635s elapsed time, 629.959s cpu time, 136.815s GC time, factor 1.64)
00:48:20Finished Differential_Dynamic_Logic (0:06:28 elapsed time, 0:10:36 cpu time, factor 1.64)
00:48:32Taylor_Models: theory HOL-Library.Function_Algebras
00:48:32Taylor_Models: theory Taylor_Models.Horner_Eval
00:48:32Taylor_Models: theory Taylor_Models.Float_Topology
00:48:32Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
00:48:33Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
00:48:36Taylor_Models: theory Taylor_Models.Taylor_Models
00:48:49HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
00:48:54HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
00:49:01Timing Complex_Bounded_Operators_Dependencies (2 threads, 721.536s elapsed time, 1219.465s cpu time, 82.021s GC time, factor 1.69)
00:49:01Finished Complex_Bounded_Operators_Dependencies (0:13:25 elapsed time, 0:22:20 cpu time, factor 1.66)
00:49:06Taylor_Models: theory Taylor_Models.Experiments
00:49:08Timing Zeta_Function (2 threads, 100.429s elapsed time, 184.000s cpu time, 8.381s GC time, factor 1.83)
00:49:08Finished Zeta_Function (0:02:23 elapsed time, 0:03:55 cpu time, factor 1.65)
00:49:13Building Complex_Bounded_Operators (on 10.195.7.194) ...
00:49:17Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
00:49:17Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
00:49:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
00:49:33Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
00:49:33Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
00:49:35Running Dirichlet_L (on 10.195.7.194) ...
00:49:36Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
00:49:36Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
00:49:37Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
00:49:37Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
00:49:38Building Prime_Distribution_Elementary (on 10.195.8.29) ...
00:49:38Building Prime_Number_Theorem (on 10.195.8.29) ...
00:49:39Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
00:49:39Dirichlet_L: theory HOL-Library.Lattice_Algebras
00:49:41Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
00:49:41Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
00:49:41Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
00:49:41Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
00:49:42Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
00:49:42Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
00:49:43Dirichlet_L: theory HOL-Library.Log_Nat
00:49:43Dirichlet_L: theory Lehmer.Lehmer
00:49:43Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
00:49:43Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
00:49:43Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
00:49:43Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
00:49:44Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
00:49:44Dirichlet_L: theory HOL-Library.Interval
00:49:44Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
00:49:44Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
00:49:45Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
00:49:45Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
00:49:45Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
00:49:45Timing Taylor_Models (2 threads, 118.508s elapsed time, 207.243s cpu time, 15.201s GC time, factor 1.75)
00:49:45Finished Taylor_Models (0:02:03 elapsed time, 0:03:32 cpu time, factor 1.73)
00:49:46Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
00:49:46Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
00:49:47Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
00:49:47Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
00:49:47Dirichlet_L: theory HOL-Library.Float
00:49:48Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
00:49:48Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
00:49:48Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
00:49:48Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
00:49:49Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
00:49:49Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
00:49:50Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
00:49:50Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
00:49:50Dirichlet_L: theory HOL-Library.Interval_Float
00:49:51Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
00:49:52Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
00:49:55Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
00:49:56Dirichlet_L: theory Bertrands_Postulate.Bertrand
00:49:57Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
00:50:00Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
00:50:02Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
00:51:07Timing Prime_Number_Theorem (2 threads, 47.618s elapsed time, 85.211s cpu time, 5.823s GC time, factor 1.79)
00:51:07Finished Prime_Number_Theorem (0:01:28 elapsed time, 0:02:13 cpu time, factor 1.51)
00:51:18Running Zeta_3_Irrational (on 10.195.8.29) ...
00:51:22Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
00:51:22Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
00:51:22Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
00:51:23Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
00:51:23Dirichlet_L: theory HOL-Algebra.QuotRing
00:51:23Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
00:51:24Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
00:51:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
00:51:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
00:51:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
00:51:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
00:51:26Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
00:51:26Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
00:51:26Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
00:51:27Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
00:51:28Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
00:51:29Dirichlet_L: theory HOL-Algebra.IntRing
00:51:30Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
00:51:31Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
00:51:31Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
00:51:31Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
00:51:33Timing Prime_Distribution_Elementary (2 threads, 73.182s elapsed time, 141.142s cpu time, 9.417s GC time, factor 1.93)
00:51:33Finished Prime_Distribution_Elementary (0:01:54 elapsed time, 0:03:10 cpu time, factor 1.67)
00:51:33Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
00:51:35Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
00:51:35Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
00:51:36Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
00:51:37Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
00:51:38Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
00:51:39Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
00:51:44Running Irrational_Series_Erdos_Straus (on 10.195.8.29) ...
00:51:44Running IMO2019 (on 10.195.8.29) ...
00:51:44Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
00:51:48Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
00:51:48IMO2019: theory IMO2019.IMO2019_Q1
00:51:48IMO2019: theory IMO2019.IMO2019_Q5
00:51:48IMO2019: theory IMO2019.IMO2019_Q4
00:51:49Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
00:51:50Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
00:52:00Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
00:52:00Timing CakeML_Codegen (2 threads, 2847.154s elapsed time, 3391.946s cpu time, 386.769s GC time, factor 1.19)
00:52:00Finished CakeML_Codegen (0:47:33 elapsed time, 0:56:42 cpu time, factor 1.19)
00:52:00Timing IMO2019 (2 threads, 11.662s elapsed time, 15.051s cpu time, 0.536s GC time, factor 1.29)
00:52:00Finished IMO2019 (0:00:15 elapsed time, 0:00:18 cpu time, factor 1.21)
00:52:09Timing Frequency_Moments (2 threads, 660.987s elapsed time, 1203.058s cpu time, 270.697s GC time, factor 1.82)
00:52:09Finished Frequency_Moments (0:12:02 elapsed time, 0:21:26 cpu time, factor 1.78)
00:52:21Timing Irrational_Series_Erdos_Straus (2 threads, 32.835s elapsed time, 60.005s cpu time, 2.441s GC time, factor 1.83)
00:52:21Finished Irrational_Series_Erdos_Straus (0:00:36 elapsed time, 0:01:03 cpu time, factor 1.74)
00:52:23Timing Zeta_3_Irrational (2 threads, 59.802s elapsed time, 112.158s cpu time, 4.945s GC time, factor 1.88)
00:52:23Finished Zeta_3_Irrational (0:01:03 elapsed time, 0:01:56 cpu time, factor 1.82)
00:52:25Timing Dirichlet_L (2 threads, 163.478s elapsed time, 294.798s cpu time, 29.182s GC time, factor 1.80)
00:52:25Finished Dirichlet_L (0:02:48 elapsed time, 0:05:00 cpu time, factor 1.79)
00:52:28Building Expander_Graphs (on 10.195.8.46) ...
00:52:35Expander_Graphs: theory Graph_Theory.Rtrancl_On
00:52:35Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
00:52:36Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
00:52:36Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
00:52:36Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
00:52:37Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
00:52:38Expander_Graphs: theory Abstract-Rewriting.Seq
00:52:38Expander_Graphs: theory HOL-Library.More_List
00:52:39Expander_Graphs: theory Perron_Frobenius.Bij_Nat
00:52:39Expander_Graphs: theory HOL-Library.While_Combinator
00:52:41Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
00:52:41Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
00:52:41Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
00:52:43Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
00:52:43Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
00:52:44Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
00:52:45Expander_Graphs: theory Jordan_Normal_Form.Conjugate
00:52:49Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
00:52:50Expander_Graphs: theory HOL-Decision_Procs.Approximation
00:52:55Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
00:52:55Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
00:52:58Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
00:52:59Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
00:53:00Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
00:53:00Expander_Graphs: theory Graph_Theory.Stuff
00:53:00Expander_Graphs: theory Graph_Theory.Digraph
00:53:02Expander_Graphs: theory Graph_Theory.Arc_Walk
00:53:04Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
00:53:05Expander_Graphs: theory Graph_Theory.Pair_Digraph
00:53:10Expander_Graphs: theory Graph_Theory.Digraph_Component
00:53:13Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
00:53:14Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
00:53:15Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
00:53:15Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
00:53:18Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
00:53:20Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
00:53:23Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
00:53:23Timing Projective_Measurements (2 threads, 690.883s elapsed time, 1198.399s cpu time, 199.488s GC time, factor 1.73)
00:53:23Finished Projective_Measurements (0:12:58 elapsed time, 0:21:54 cpu time, factor 1.69)
00:53:24Expander_Graphs: theory Matrix.Utility
00:53:24Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
00:53:29Expander_Graphs: theory Jordan_Normal_Form.Matrix
00:53:34Building Commuting_Hermitian (on 10.195.8.29) ...
00:53:34Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
00:53:37Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
00:53:37Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
00:53:37Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
00:53:38Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
00:53:39Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
00:53:39Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
00:53:39Expander_Graphs: theory Jordan_Normal_Form.Determinant
00:53:40Expander_Graphs: theory Regular-Sets.Regular_Set
00:53:41Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
00:53:42Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
00:53:43Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
00:53:43Expander_Graphs: theory VectorSpace.FunctionLemmas
00:53:43Expander_Graphs: theory VectorSpace.RingModuleFacts
00:53:44Expander_Graphs: theory Regular-Sets.Regular_Exp
00:53:44Expander_Graphs: theory VectorSpace.MonoidSums
00:53:45Expander_Graphs: theory VectorSpace.LinearCombinations
00:53:50Timing Complex_Bounded_Operators (2 threads, 223.254s elapsed time, 417.564s cpu time, 41.754s GC time, factor 1.87)
00:53:50Finished Complex_Bounded_Operators (0:04:33 elapsed time, 0:08:00 cpu time, factor 1.76)
00:53:50Expander_Graphs: theory Regular-Sets.NDerivative
00:53:53Expander_Graphs: theory Regular-Sets.Relation_Interpretation
00:53:53Expander_Graphs: theory VectorSpace.SumSpaces
00:53:53Expander_Graphs: theory VectorSpace.VectorSpace
00:53:54Expander_Graphs: theory Regular-Sets.Equivalence_Checking
00:53:55Expander_Graphs: theory Regular-Sets.Regexp_Method
00:53:55Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
00:53:57Expander_Graphs: theory Abstract-Rewriting.SN_Orders
00:53:58Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
00:54:00Expander_Graphs: theory Matrix.Ordered_Semiring
00:54:01Expander_Graphs: theory Matrix.Matrix_Legacy
00:54:02Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
00:54:02Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
00:54:04Running Registers (on 10.195.8.29) ...
00:54:04Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
00:54:04Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
00:54:05Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
00:54:06Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
00:54:07Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
00:54:08Registers: theory HOL-Library.Type_Length
00:54:08Registers: theory HOL-Eisbach.Eisbach
00:54:08Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
00:54:09Registers: theory HOL-Library.Z2
00:54:09Registers: theory HOL-Library.Word
00:54:10Registers: theory Registers.Axioms
00:54:10Registers: theory Registers.Laws
00:54:11Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
00:54:11Registers: theory Registers.Axioms_Complement
00:54:11Registers: theory Registers.Laws_Complement
00:54:11Registers: theory Registers.Axioms_Classical
00:54:12Registers: theory Registers.Laws_Classical
00:54:12Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
00:54:13Registers: theory Registers.Misc
00:54:15Registers: theory Registers.Classical_Extra
00:54:15Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
00:54:19Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
00:54:19Expander_Graphs: theory QHLProver.Complex_Matrix
00:54:19Expander_Graphs: theory Perron_Frobenius.HMA_Connect
00:54:20Registers: theory Registers.Finite_Tensor_Product
00:54:22Registers: theory Registers.Axioms_Quantum
00:54:22Registers: theory Registers.Finite_Tensor_Product_Matrices
00:54:22Registers: theory Registers.Quantum
00:54:22Expander_Graphs: theory QHLProver.Gates
00:54:23Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
00:54:25Registers: theory Registers.Laws_Quantum
00:54:27Timing Probabilistic_Prime_Tests (2 threads, 835.493s elapsed time, 1591.536s cpu time, 741.741s GC time, factor 1.90)
00:54:27Finished Probabilistic_Prime_Tests (0:14:03 elapsed time, 0:26:43 cpu time, factor 1.90)
00:54:27Expander_Graphs: theory Projective_Measurements.Projective_Measurements
00:54:28Registers: theory Registers.Quantum_Extra
00:54:29Registers: theory Registers.Axioms_Complement_Quantum
00:54:29Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
00:54:29Registers: theory Registers.QHoare
00:54:29Registers: theory Registers.Laws_Complement_Quantum
00:54:30Registers: theory Registers.Teleport
00:54:30Registers: theory Registers.Check_Autogenerated_Files
00:54:30Timing Three_Squares (2 threads, 808.188s elapsed time, 1425.365s cpu time, 292.446s GC time, factor 1.76)
00:54:30Finished Three_Squares (0:14:50 elapsed time, 0:25:35 cpu time, factor 1.72)
00:54:30Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
00:54:33Registers: theory Registers.Quantum_Extra2
00:54:33Registers: theory Registers.Pure_States
00:54:33Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
00:54:36Running Polygonal_Number_Theorem (on 10.195.8.29) ...
00:54:37Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
00:54:37Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
00:54:39Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
00:54:41Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
00:54:41Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
00:54:41Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
00:54:42Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
00:54:44Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
00:55:09Timing Commuting_Hermitian (2 threads, 51.137s elapsed time, 96.019s cpu time, 7.060s GC time, factor 1.88)
00:55:09Finished Commuting_Hermitian (0:01:33 elapsed time, 0:02:26 cpu time, factor 1.56)
00:55:23Running TsirelsonBound (on 10.195.7.194) ...
00:55:27TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
00:55:29TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
00:55:30TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
00:55:31TsirelsonBound: theory TsirelsonBound.Tsirelson
00:55:37Timing Constructive_Cryptography_CM (2 threads, 602.003s elapsed time, 1123.781s cpu time, 181.226s GC time, factor 1.87)
00:55:37Finished Constructive_Cryptography_CM (0:10:08 elapsed time, 0:18:53 cpu time, factor 1.86)
00:56:12Timing Polygonal_Number_Theorem (2 threads, 90.816s elapsed time, 164.600s cpu time, 8.557s GC time, factor 1.81)
00:56:12Finished Polygonal_Number_Theorem (0:01:34 elapsed time, 0:02:49 cpu time, factor 1.78)
00:56:41Timing TsirelsonBound (2 threads, 73.088s elapsed time, 123.198s cpu time, 6.782s GC time, factor 1.69)
00:56:41Finished TsirelsonBound (0:01:17 elapsed time, 0:02:07 cpu time, factor 1.65)
00:56:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
00:57:36HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
00:57:47Timing Registers (2 threads, 217.114s elapsed time, 394.930s cpu time, 38.064s GC time, factor 1.82)
00:57:47Finished Registers (0:03:42 elapsed time, 0:06:41 cpu time, factor 1.80)
00:58:17Timing Smith_Normal_Form (2 threads, 806.435s elapsed time, 1363.159s cpu time, 223.458s GC time, factor 1.69)
00:58:17Finished Smith_Normal_Form (0:14:44 elapsed time, 0:24:32 cpu time, factor 1.66)
00:58:30Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.7.194) ...
00:58:42Estimated 0:44:04 build time with path time heuristic (critical: absolute time (0:20:00), parallel: fixed threads (1)) (took 0.171s)
00:58:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
00:58:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
00:58:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
00:58:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
00:58:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
00:58:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
00:58:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
00:58:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
00:58:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
00:58:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
00:58:47Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
00:58:47Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
00:58:47Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
00:58:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
00:58:48Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
00:58:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
00:58:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
00:58:48Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
00:58:49Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
00:58:50Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
00:58:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
00:58:51Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
00:58:53Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
00:58:55Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
00:58:55Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
00:58:56Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
00:58:56Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
00:58:57Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
00:58:57Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
00:58:58Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
00:59:05Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
00:59:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
00:59:06Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
00:59:08Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
00:59:10HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
00:59:10Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
00:59:11Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
00:59:12Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
00:59:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
00:59:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
00:59:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
00:59:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
00:59:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
00:59:24Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
00:59:25Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
00:59:25Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
00:59:25Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
00:59:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
00:59:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
00:59:27Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
00:59:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
00:59:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
00:59:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
00:59:31Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
00:59:31Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
00:59:32Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
00:59:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
00:59:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
00:59:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
00:59:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
00:59:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
00:59:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
00:59:49Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
00:59:49Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
00:59:49Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
00:59:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
01:00:09Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
01:00:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
01:00:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
01:00:12Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
01:00:12Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
01:00:13Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
01:00:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
01:00:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
01:00:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
01:00:16Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
01:00:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
01:00:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
01:00:21Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
01:00:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
01:00:23Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
01:00:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
01:00:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
01:00:27Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
01:00:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
01:00:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
01:00:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
01:00:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
01:00:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
01:00:39Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
01:00:39Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
01:00:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
01:00:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
01:00:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
01:00:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
01:00:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
01:00:54Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
01:00:56Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
01:00:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
01:01:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
01:01:02Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
01:01:02Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
01:01:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
01:01:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
01:01:05Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
01:01:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
01:01:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
01:01:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
01:01:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
01:01:09Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
01:01:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
01:01:11Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
01:01:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
01:01:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
01:01:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
01:01:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
01:01:16Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
01:01:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
01:01:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
01:01:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
01:01:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
01:01:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
01:01:19Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
01:01:19Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
01:01:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
01:01:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
01:01:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
01:01:39Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
01:01:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
01:01:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
01:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
01:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
01:01:52Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
01:02:05Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
01:02:39Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
01:02:39Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
01:03:21Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
01:03:23Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
01:03:51Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
01:03:52Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
01:04:15Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
01:04:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
01:04:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
01:04:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
01:04:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
01:04:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
01:05:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
01:06:11Timing Cook_Levin (2 threads, 1820.596s elapsed time, 3093.857s cpu time, 235.548s GC time, factor 1.70)
01:06:11Finished Cook_Levin (0:30:27 elapsed time, 0:51:44 cpu time, factor 1.70)
01:08:20Timing Expander_Graphs (2 threads, 868.979s elapsed time, 1549.308s cpu time, 423.468s GC time, factor 1.78)
01:08:20Finished Expander_Graphs (0:15:43 elapsed time, 0:27:30 cpu time, factor 1.75)
01:08:32Running Distributed_Distinct_Elements (on 10.195.6.179) ...
01:08:37Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
01:08:37Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
01:08:37Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
01:08:38Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
01:08:38Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
01:08:38Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
01:08:39Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
01:08:39Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
01:08:44Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
01:08:45Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
01:08:46Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
01:08:46Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
01:08:46Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
01:08:48Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
01:08:51Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
01:08:52Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
01:08:52Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
01:08:52Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
01:08:58Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
01:08:59Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
01:08:59Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
01:09:00Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
01:09:03Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
01:09:04Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
01:09:14Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
01:09:15Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
01:09:24Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
01:09:26Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
01:09:27Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
01:09:30Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
01:10:45Timing Distributed_Distinct_Elements (2 threads, 126.686s elapsed time, 241.889s cpu time, 14.973s GC time, factor 1.91)
01:10:45Finished Distributed_Distinct_Elements (0:02:12 elapsed time, 0:04:08 cpu time, factor 1.88)
01:26:26Timing HOL-ODE-Numerics (2 threads, 2573.251s elapsed time, 4796.523s cpu time, 915.587s GC time, factor 1.86)
01:26:26Finished HOL-ODE-Numerics (0:44:38 elapsed time, 1:22:20 cpu time, factor 1.84)
01:26:34Building Lorenz_Approximation (on 10.195.8.49) ...
01:26:34Running HOL-ODE-ARCH-COMP (on 10.195.8.49) ...
01:26:34Running HOL-ODE-Examples (on 10.195.8.49) ...
01:26:34Running Poincare_Bendixson (on 10.195.8.49) ...
01:26:37Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
01:26:38HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
01:26:38HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
01:26:38HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
01:26:38Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
01:26:38Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
01:26:39HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
01:26:40Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
01:26:42Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
01:26:44Poincare_Bendixson: theory Poincare_Bendixson.Invariance
01:26:44Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.059s)
01:26:46Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
01:26:48Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
01:26:49Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
01:26:56Poincare_Bendixson: theory Poincare_Bendixson.Examples
01:27:06Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
01:28:27HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
01:29:00Timing Poincare_Bendixson (2 threads, 139.362s elapsed time, 210.764s cpu time, 14.036s GC time, factor 1.51)
01:29:00Finished Poincare_Bendixson (0:02:24 elapsed time, 0:03:35 cpu time, factor 1.50)
01:29:12Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.157s)
01:32:59Timing HOL-ODE-Examples (2 threads, 379.498s elapsed time, 650.473s cpu time, 25.308s GC time, factor 1.71)
01:32:59Finished HOL-ODE-Examples (0:06:24 elapsed time, 0:10:55 cpu time, factor 1.71)
01:33:03Timing Lorenz_Approximation (2 threads, 329.934s elapsed time, 615.086s cpu time, 70.520s GC time, factor 1.86)
01:33:03Finished Lorenz_Approximation (0:06:27 elapsed time, 0:11:31 cpu time, factor 1.78)
01:33:11Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.057s)
01:33:25Running Lorenz_C0 (on 10.195.8.29) ...
01:33:25Running Lorenz_C1 (on 10.195.8.29) ...
01:33:30Lorenz_C0: theory Lorenz_C0.Lorenz_C0
01:33:30Lorenz_C1: theory Lorenz_C1.Lorenz_C1
01:33:33Timing Lorenz_C1 (2 threads, 1.921s elapsed time, 2.551s cpu time, 0.057s GC time, factor 1.33)
01:33:33Finished Lorenz_C1 (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.07)
01:33:41Estimated 0:25:07 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.001s)
01:33:50Timing HOL-ODE-ARCH-COMP (2 threads, 431.076s elapsed time, 795.707s cpu time, 82.574s GC time, factor 1.85)
01:33:50Finished HOL-ODE-ARCH-COMP (0:07:15 elapsed time, 0:13:19 cpu time, factor 1.84)
01:36:07Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2237.388s elapsed time, 4108.048s cpu time, 934.651s GC time, factor 1.84)
01:36:07Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:37:29 elapsed time, 1:08:47 cpu time, factor 1.84)
02:01:22Timing Lorenz_C0 (2 threads, 1671.227s elapsed time, 3268.775s cpu time, 87.561s GC time, factor 1.96)
02:01:22Finished Lorenz_C0 (0:27:55 elapsed time, 0:54:33 cpu time, factor 1.95)
02:01:33Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.003s)
03:05:18Build timed out (after 200 minutes). Marking the build as failed.
03:05:18Build was aborted
03:05:18Started calculate disk usage of build
03:05:19Finished Calculation of disk usage of build in 0 seconds
03:05:32Started calculate disk usage of workspace
03:05:33Finished Calculation of disk usage of workspace in 0 seconds
03:05:33Finished: FAILURE
![[Jenkins]](/jenkins/static/0ab21b84/images/svgs/logo.svg){kind=logo}
