Probabilistic_Prime_Tests: theory HOL-Library.More_List
23:20:32Applicative_Lifting: theory Applicative_Lifting.Applicative
23:20:32Applicative_Lifting: theory Applicative_Lifting.Joinable
23:20:32Executable_Randomized_Algorithms: theory HOL-Library.While_Combinator
23:20:32Frequency_Moments: theory HOL-Algebra.Elementary_Groups
23:20:32Deep_Learning: theory VectorSpace.FunctionLemmas
23:20:32Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
23:20:33Deep_Learning: theory VectorSpace.RingModuleFacts
23:20:33Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
23:20:33Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping
23:20:33Applicative_Lifting: theory HOL-Library.State_Monad
23:20:33Schwartz_Zippel: theory Open_Induction.Restricted_Predicates
23:20:33Markov_Models: theory Markov_Models.MDP_RP_Certification
23:20:33S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Product
23:20:33Fourier: theory Fourier.Confine
23:20:33Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
23:20:33Fourier: theory HOL-Library.Function_Algebras
23:20:33Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
23:20:33Actuarial_Mathematics: theory Actuarial_Mathematics.Preliminaries
23:20:33Density_Compiler: theory Density_Compiler.PDF_Semantics
23:20:33Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
23:20:33Executable_Randomized_Algorithms: theory HOL-Library.Bourbaki_Witt_Fixpoint
23:20:33Fourier: theory Fourier.Fourier_Aux2
23:20:33Schwartz_Zippel: theory HOL-Algebra.Lattice
23:20:33Fourier: theory Fourier.Periodic
23:20:33Randomised_Social_Choice: theory List-Index.List_Index
23:20:33S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
23:20:33Executable_Randomized_Algorithms: theory HOL-Algebra.AbelCoset
23:20:33Executable_Randomized_Algorithms: theory HOL-Algebra.Module
23:20:33Projective_Measurements: theory Abstract-Rewriting.Seq
23:20:33Fourier: theory Ergodic_Theory.SG_Library_Complement
23:20:33Deep_Learning: theory VectorSpace.MonoidSums
23:20:33Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom
23:20:34Frequency_Moments: theory HOL-Algebra.RingHom
23:20:34Projective_Measurements: theory HOL-Algebra.Lattice
23:20:34Frequency_Moments: theory HOL-Library.Interval
23:20:34S_Finite_Measure_Monad: theory Standard_Borel_Spaces.StandardBorel
23:20:34Ergodic_Theory: theory Ergodic_Theory.Invariants
23:20:34Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
23:20:34Projective_Measurements: theory HOL-Library.More_List
23:20:34Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
23:20:34Deep_Learning: theory VectorSpace.LinearCombinations
23:20:34Schwartz_Zippel: theory Polynomials.MPoly_Type
23:20:34Schwartz_Zippel: theory Regular-Sets.Regular_Set
23:20:34Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
23:20:34List_Update: theory Regular-Sets.Regular_Exp
23:20:34Projective_Measurements: theory HOL-Library.While_Combinator
23:20:34Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
23:20:35S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Lemmas_S_Finite_Measure_Monad
23:20:35Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice
23:20:35S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Kernels
23:20:35S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Measure_QuasiBorel_Adjunction
23:20:35Projective_Measurements: theory HOL-Algebra.Complete_Lattice
23:20:35Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
23:20:35Schwartz_Zippel: theory Polynomials.More_MPoly_Type
23:20:35Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
23:20:35Frequency_Moments: theory HOL-Algebra.QuotRing
23:20:35Ergodic_Theory: theory Ergodic_Theory.Ergodicity
23:20:35Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
23:20:35Executable_Randomized_Algorithms: theory MFMC_Countable.MFMC_Finite
23:20:35Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
23:20:36Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
23:20:36Fourier: theory Lp.Functional_Spaces
23:20:36Running Quasi_Borel_Spaces (on 10.195.8.32) ...
23:20:36Running Universal_Hash_Families (on 10.195.8.32) ...
23:20:36Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_List
23:20:36Running Probabilistic_System_Zoo (on 10.195.8.32) ...
23:20:36Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
23:20:36Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
23:20:36Executable_Randomized_Algorithms: theory HOL-Number_Theory.Eratosthenes
23:20:36Running Roth_Arithmetic_Progressions (on 10.195.8.32) ...
23:20:36Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State
23:20:36Running Probabilistic_Noninterference (on 10.195.8.32) ...
23:20:36Ergodic_Theory: theory Ergodic_Theory.Kingman
23:20:36Ergodic_Theory: theory Ergodic_Theory.Shift_Operator
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
23:20:36Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
23:20:36Applicative_Lifting: theory Applicative_Lifting.Applicative_State
23:20:36Applicative_Lifting: theory HOL-Library.Confluence
23:20:36Executable_Randomized_Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
23:20:36Applicative_Lifting: theory HOL-Library.Confluent_Quotient
23:20:36Schwartz_Zippel: theory HOL-Algebra.Group
23:20:36Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
23:20:36Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
23:20:36Applicative_Lifting: theory HOL-Library.Dlist
23:20:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
23:20:37Applicative_Lifting: theory HOL-Library.Function_Algebras
23:20:37Deep_Learning: theory Jordan_Normal_Form.Matrix
23:20:37Executable_Randomized_Algorithms: theory HOL-Algebra.Ideal
23:20:37Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial
23:20:37Applicative_Lifting: theory HOL-Library.Function_Division
23:20:37Actuarial_Mathematics: theory Actuarial_Mathematics.Interest
23:20:37Balog_Szemeredi_Gowers: theory HOL-Library.Interval
23:20:37Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
23:20:37Projective_Measurements: theory HOL-Algebra.Group
23:20:37Actuarial_Mathematics: theory Actuarial_Mathematics.Survival_Model
23:20:37Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
23:20:37Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
23:20:37Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
23:20:37Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
23:20:37Frequency_Moments: theory HOL-Algebra.UnivPoly
23:20:37Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
23:20:37Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
23:20:37Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
23:20:37Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
23:20:38Probabilistic_Prime_Tests: theory HOL-Algebra.Group
23:20:38Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef
23:20:38S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Monad_QuasiBorel
23:20:38Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
23:20:38Schwartz_Zippel: theory HOL-Algebra.FiniteProduct
23:20:38Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
23:20:38Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
23:20:38Frequency_Moments: theory HOL-Algebra.IntRing
23:20:38Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.StandardBorel
23:20:38Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
23:20:38Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More
23:20:38Fourier: theory Lp.Lp
23:20:38Schwartz_Zippel: theory HOL-Algebra.Ring
23:20:38Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Dense_Linear_Order
23:20:38Roth_Arithmetic_Progressions: theory HOL-Library.Code_Abstract_Nat
23:20:38Probabilistic_Noninterference: theory HOL-Library.Case_Converter
23:20:38Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More
23:20:39Probabilistic_Noninterference: theory HOL-Library.Prefix_Order
23:20:39Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
23:20:39Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
23:20:39Universal_Hash_Families: theory HOL-Algebra.Congruence
23:20:39Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat
23:20:39Universal_Hash_Families: theory HOL-Combinatorics.List_Permutation
23:20:39Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Nat
23:20:39Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:20:39Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Int
23:20:39Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families
23:20:39List_Update: theory Regular-Sets.NDerivative
23:20:39Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
23:20:39Executable_Randomized_Algorithms: theory HOL-Algebra.RingHom
23:20:39Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
23:20:39Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation
23:20:39Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS
23:20:39Markov_Models: theory Markov_Models.PGCL
23:20:40Frequency_Moments: theory HOL-Library.Log_Nat
23:20:40Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
23:20:40Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda
23:20:40Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter
23:20:40Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate
23:20:40Frequency_Moments: theory HOL-Library.Float
23:20:40Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union
23:20:40List_Update: theory List_Update.MTF2_Effects
23:20:40Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial
23:20:40Deep_Learning: theory VectorSpace.SumSpaces
23:20:40Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv
23:20:40Schwartz_Zippel: theory Regular-Sets.Regular_Exp
23:20:40Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral
23:20:40Fourier: theory Fourier.Lspace
23:20:40Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
23:20:40Fourier: theory Fourier.Square_Integrable
23:20:40Roth_Arithmetic_Progressions: theory HOL-Library.Ramsey
23:20:40Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
23:20:40Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
23:20:40Projective_Measurements: theory HOL-Algebra.Coset
23:20:40Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:20:40List_Update: theory List_Update.BIT
23:20:40Fourier: theory Fourier.Fourier
23:20:41Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
23:20:41Deep_Learning: theory VectorSpace.VectorSpace
23:20:41Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed
23:20:41Universal_Hash_Families: theory HOL-Algebra.Order
23:20:41Probabilistic_Noninterference: theory Coinductive.Coinductive_List
23:20:41Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.QuasiBorel
23:20:41Executable_Randomized_Algorithms: theory HOL-Algebra.UnivPoly
23:20:41Applicative_Lifting: theory HOL-Proofs-Lambda.Eta
23:20:41Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial
23:20:41Schwartz_Zippel: theory HOL-Algebra.Module
23:20:41Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
23:20:41Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
23:20:41Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
23:20:41Building Quick_Sort_Cost (on 10.195.8.46) ...
23:20:41Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension
23:20:41Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
23:20:41Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
23:20:41Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
23:20:41Roth_Arithmetic_Progressions: theory HOL-Library.Lattice_Algebras
23:20:41Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring
23:20:42Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
23:20:42Balog_Szemeredi_Gowers: theory HOL-Library.Log_Nat
23:20:42Applicative_Lifting: theory Applicative_Lifting.Combinators
23:20:42Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
23:20:42Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction
23:20:42Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
23:20:42Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
23:20:42Building Girth_Chromatic (on 10.195.8.46) ...
23:20:42Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
23:20:42Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
23:20:42Running MFMC_Countable (on 10.195.8.46) ...
23:20:42Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
23:20:42Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
23:20:42Frequency_Moments: theory HOL-Library.Interval_Float
23:20:42Running Monomorphic_Monad (on 10.195.8.46) ...
23:20:42Deep_Learning: theory Deep_Learning.DL_Network
23:20:42Running Turans_Graph_Theorem (on 10.195.8.46) ...
23:20:42Balog_Szemeredi_Gowers: theory HOL-Library.Float
23:20:42Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
23:20:43Universal_Hash_Families: theory HOL-Algebra.Lattice
23:20:43Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
23:20:43Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel
23:20:43Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
23:20:43Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
23:20:43Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial
23:20:43Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
23:20:43Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
23:20:43Markov_Models: theory Markov_Models.Zeroconf_Analysis
23:20:43Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:20:43Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
23:20:43Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
23:20:43Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
23:20:43Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel
23:20:43Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
23:20:43Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
23:20:44Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
23:20:44Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
23:20:44Roth_Arithmetic_Progressions: theory HOL-Library.Log_Nat
23:20:44Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Product_QuasiBorel
23:20:44Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic_Misc
23:20:44Schwartz_Zippel: theory Regular-Sets.NDerivative
23:20:44Roth_Arithmetic_Progressions: theory Girth_Chromatic.Ugraphs
23:20:44Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
23:20:44Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.CoProduct_QuasiBorel
23:20:44Projective_Measurements: theory HOL-Algebra.FiniteProduct
23:20:44Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
23:20:44Turans_Graph_Theorem: theory HOL-Decision_Procs.Dense_Linear_Order
23:20:44Turans_Graph_Theorem: theory HOL-Library.Code_Abstract_Nat
23:20:44Roth_Arithmetic_Progressions: theory Szemeredi_Regularity.Szemeredi
23:20:44Quick_Sort_Cost: theory HOL-Library.Function_Algebras
23:20:44Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
23:20:44MFMC_Countable: theory Flow_Networks.Graph
23:20:45Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
23:20:45MFMC_Countable: theory HOL-Library.Case_Converter
23:20:45Turans_Graph_Theorem: theory HOL-Library.Code_Target_Nat
23:20:45Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
23:20:45Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
23:20:45Turans_Graph_Theorem: theory HOL-Library.Code_Target_Int
23:20:45Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:20:45Quick_Sort_Cost: theory List-Index.List_Index
23:20:45S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Montecarlo
23:20:45Girth_Chromatic: theory HOL-Library.Code_Target_Nat
23:20:45Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
23:20:45S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Query
23:20:45Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral
23:20:45Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Exponent_QuasiBorel
23:20:45Girth_Chromatic: theory HOL-Library.Code_Target_Int
23:20:45Markov_Models: theory Markov_Models.Markov_Models
23:20:45Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
23:20:45Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial_FPS
23:20:45Turans_Graph_Theorem: theory HOL-Library.Lattice_Algebras
23:20:46MFMC_Countable: theory HOL-Library.Simps_Case_Conv
23:20:46Girth_Chromatic: theory HOL-Library.Code_Target_Numeral
23:20:46MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
23:20:46Running Hahn_Jordan_Decomposition (on of3.proof.cit.tum.de) ...
23:20:46Running DiscretePricing (on of3.proof.cit.tum.de) ...
23:20:46Running Neumann_Morgenstern_Utility (on of3.proof.cit.tum.de) ...
23:20:46Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
23:20:46Running Standard_Borel_Spaces (on of3.proof.cit.tum.de) ...
23:20:46Universal_Hash_Families: theory HOL-Algebra.Complete_Lattice
23:20:46Girth_Chromatic: theory HOL-Library.Lattice_Algebras
23:20:46Projective_Measurements: theory HOL-Algebra.Ring
23:20:46Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra
23:20:46Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
23:20:46Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel
23:20:46Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:20:46MFMC_Countable: theory HOL-Library.While_Combinator
23:20:46List_Update: theory List_Update.Partial_Cost_Model
23:20:46Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
23:20:46Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set
23:20:46Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bool_Bounded_Set
23:20:47Roth_Arithmetic_Progressions: theory Ergodic_Theory.SG_Library_Complement
23:20:47Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
23:20:47Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl
23:20:47Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample
23:20:47DiscretePricing: theory DiscretePricing.Filtration
23:20:47Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
23:20:47Standard_Borel_Spaces: theory Standard_Borel_Spaces.Lemmas_StandardBorel
23:20:47Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
23:20:47DiscretePricing: theory DiscretePricing.Generated_Subalgebra
23:20:47Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
23:20:47MFMC_Countable: theory Flow_Networks.Network
23:20:47Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
23:20:47Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
23:20:47Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims
23:20:47Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
23:20:47Probabilistic_Prime_Tests: theory HOL-Algebra.Left_Coset
23:20:47Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
23:20:47Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Numeral_Float
23:20:47DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
23:20:47Probabilistic_Prime_Tests: theory HOL-Algebra.SimpleGroups
23:20:47Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
23:20:47Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
23:20:47Balog_Szemeredi_Gowers: theory HOL-Library.Interval_Float
23:20:48MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
23:20:48Probabilistic_Prime_Tests: theory HOL-Algebra.SndIsomorphismGrp
23:20:48Deep_Learning: theory Deep_Learning.DL_Shallow_Model
23:20:48Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
23:20:48Universal_Hash_Families: theory HOL-Algebra.Group
23:20:48Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
23:20:48Roth_Arithmetic_Progressions: theory Ergodic_Theory.Asymptotic_Density
23:20:48MFMC_Countable: theory MFMC_Countable.MFMC_Misc
23:20:48Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
23:20:48MFMC_Countable: theory Flow_Networks.Residual_Graph
23:20:48Schwartz_Zippel: theory Symmetric_Polynomials.Vieta
23:20:48Turans_Graph_Theorem: theory HOL-Library.Log_Nat
23:20:48Deep_Learning: theory Deep_Learning.Tensor_Matricization
23:20:48Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
23:20:48Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
23:20:48Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
23:20:48List_Update: theory Regular-Sets.Equivalence_Checking
23:20:48List_Update: theory List_Update.List_Factoring
23:20:48Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
23:20:48Girth_Chromatic: theory HOL-Library.Log_Nat
23:20:48Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
23:20:48Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
23:20:48List_Update: theory List_Update.RExp_Var
23:20:48Estimated completion: 25-Nov-2023 01:45:38 +0100 (took 2.900s)
23:20:49DiscretePricing: theory DiscretePricing.Martingale
23:20:49DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
23:20:49MFMC_Countable: theory MFMC_Countable.MFMC_Network
23:20:49Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Space
23:20:49Actuarial_Mathematics: theory Actuarial_Mathematics.Life_Table
23:20:49Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
23:20:49Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
23:20:49Running Lovasz_Local (on of1-proof+8-15) ...
23:20:49Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials
23:20:49Running Lp (on of1-proof+0-7) ...
23:20:50Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Ring_Theory
23:20:50Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
23:20:50Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
23:20:50Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
23:20:50Girth_Chromatic: theory Girth_Chromatic.Ugraphs
23:20:50Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
23:20:50Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
23:20:50Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
23:20:50Schwartz_Zippel: theory Regular-Sets.Regexp_Method
23:20:50Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
23:20:50Density_Compiler: theory Density_Compiler.PDF_Compiler
23:20:50Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:20:50Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
23:20:50Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
23:20:50Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation_Bounds
23:20:50Lp: theory HOL-Library.Function_Algebras
23:20:50Lp: theory Ergodic_Theory.SG_Library_Complement
23:20:50Lovasz_Local: theory HOL-Eisbach.Eisbach
23:20:50Lovasz_Local: theory Graph_Theory.Rtrancl_On
23:20:50Lovasz_Local: theory HOL-Combinatorics.Stirling
23:20:50Lovasz_Local: theory HOL-Library.Multiset_Order
23:20:50Lovasz_Local: theory Card_Partitions.Set_Partition
23:20:50Lovasz_Local: theory Graph_Theory.Stuff
23:20:50Roth_Arithmetic_Progressions: theory HOL-Library.Interval
23:20:50Roth_Arithmetic_Progressions: theory HOL-Library.Float
23:20:50Probabilistic_Prime_Tests: theory HOL-Algebra.Module
23:20:50MFMC_Countable: theory Flow_Networks.Augmenting_Flow
23:20:50Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Computational_Algebra
23:20:50MFMC_Countable: theory Flow_Networks.Augmenting_Path
23:20:50Lovasz_Local: theory Graph_Theory.Digraph
23:20:51Projective_Measurements: theory HOL-Algebra.Module
23:20:51Lovasz_Local: theory Nested_Multisets_Ordinals.Multiset_More
23:20:51List_Update: theory List_Update.OPT2
23:20:51MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
23:20:51Lp: theory Lp.Functional_Spaces
23:20:51List_Update: theory List_Update.BIT_pairwise
23:20:51Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Product
23:20:51Running Treaps (on 10.195.8.42) ...
23:20:51Lovasz_Local: theory Card_Partitions.Injectivity_Solver
23:20:51Universal_Hash_Families: theory HOL-Algebra.Coset
23:20:51Running Median_Method (on 10.195.8.42) ...
23:20:51Universal_Hash_Families: theory HOL-Algebra.FiniteProduct
23:20:51Lovasz_Local: theory Card_Partitions.Card_Partitions
23:20:51Deep_Learning: theory Jordan_Normal_Form.Column_Operations
23:20:51Lovasz_Local: theory Lovasz_Local.PiE_Rel_Extras
23:20:51Standard_Borel_Spaces: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
23:20:51Lovasz_Local: theory Lovasz_Local.Prob_Events_Extras
23:20:51Lovasz_Local: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
23:20:52Actuarial_Mathematics: theory Actuarial_Mathematics.Examples
23:20:52Frequency_Moments: theory HOL-Number_Theory.Fib
23:20:52Lovasz_Local: theory Graph_Theory.Arc_Walk
23:20:52Turans_Graph_Theorem: theory HOL-Library.Interval
23:20:52Lovasz_Local: theory Graph_Theory.Bidirected_Digraph
23:20:52Turans_Graph_Theorem: theory HOL-Library.Float
23:20:52Lovasz_Local: theory Design_Theory.Multisets_Extras
23:20:52Standard_Borel_Spaces: theory Standard_Borel_Spaces.StandardBorel
23:20:52Executable_Randomized_Algorithms: theory HOL-Library.Going_To_Filter
23:20:52Deep_Learning: theory Jordan_Normal_Form.Determinant
23:20:52Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
23:20:52Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tau_Additivity
23:20:52Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
23:20:52Executable_Randomized_Algorithms: theory HOL-Number_Theory.Fib
23:20:52Running Buffons_Needle (on of4.proof.cit.tum.de) ...
23:20:52Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Monad_QuasiBorel
23:20:52Running Skip_Lists (on of4.proof.cit.tum.de) ...
23:20:52Running Source_Coding_Theorem (on of4.proof.cit.tum.de) ...
23:20:52Running Monad_Normalisation (on of4.proof.cit.tum.de) ...
23:20:52Lovasz_Local: theory Lovasz_Local.Cond_Prob_Extensions
23:20:53Girth_Chromatic: theory HOL-Library.Interval
23:20:53Lp: theory Lp.Lp
23:20:53Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
23:20:53Girth_Chromatic: theory HOL-Library.Float
23:20:53MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
23:20:53Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:20:53Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
23:20:53Executable_Randomized_Algorithms: theory HOL-Number_Theory.Prime_Powers
23:20:53Lovasz_Local: theory Graph_Theory.Pair_Digraph
23:20:53Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
23:20:53Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
23:20:53Frequency_Moments: theory HOL-Number_Theory.Totient
23:20:53List_Update: theory List_Update.Phase_Partitioning
23:20:53Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
23:20:53Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
23:20:53Universal_Hash_Families: theory HOL-Algebra.Ring
23:20:53Skip_Lists: theory Skip_Lists.Pi_pmf
23:20:53Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
23:20:53Skip_Lists: theory Skip_Lists.Misc
23:20:53Lovasz_Local: theory Lovasz_Local.Indep_Events
23:20:54Buffons_Needle: theory Buffons_Needle.Buffons_Needle
23:20:54Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
23:20:54Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
23:20:54Treaps: theory HOL-Data_Structures.Cmp
23:20:54Treaps: theory HOL-Data_Structures.Less_False
23:20:54Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
23:20:54Quick_Sort_Cost: theory Landau_Symbols.Landau_More
23:20:54Executable_Randomized_Algorithms: theory HOL-Algebra.Multiplicative_Group
23:20:54List_Update: theory List_Update.BIT_2comp_on2
23:20:54Treaps: theory HOL-Data_Structures.Sorted_Less
23:20:54Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
23:20:54List_Update: theory List_Update.TS
23:20:54Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
23:20:54Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
23:20:54Skip_Lists: theory Skip_Lists.Geometric_PMF
23:20:54Treaps: theory HOL-Data_Structures.List_Ins_Del
23:20:54Frequency_Moments: theory HOL-Algebra.Subrings
23:20:54Executable_Randomized_Algorithms: theory HOL-Number_Theory.Totient
23:20:54Deep_Learning: theory Deep_Learning.DL_Deep_Model
23:20:54Deep_Learning: theory Jordan_Normal_Form.VS_Connect
23:20:54MFMC_Countable: theory MFMC_Countable.MFMC_Flow_Attainability
23:20:54Lovasz_Local: theory Lovasz_Local.Basic_Method
23:20:55Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
23:20:55Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
23:20:55Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
23:20:55MFMC_Countable: theory MFMC_Countable.MFMC_Finite
23:20:55Treaps: theory HOL-Library.Function_Algebras
23:20:55Skip_Lists: theory Skip_Lists.Skip_List
23:20:55Running Fisher_Yates (on 10.195.8.40) ...
23:20:55Treaps: theory Landau_Symbols.Group_Sort
23:20:55Treaps: theory HOL-Data_Structures.Set_Specs
23:20:55Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
23:20:55Three_Squares: theory Dirichlet_Series.Multiplicative_Function
23:20:55Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
23:20:55Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Contour_Integration
23:20:55Treaps: theory HOL-Data_Structures.Tree_Set
23:20:55Timing Monad_Normalisation (6 threads, 0.886s elapsed time, 1.240s cpu time, 0.036s GC time, factor 1.40)
23:20:55Finished Monad_Normalisation (0:00:02 elapsed time)
23:20:55DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
23:20:55Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
23:20:55MFMC_Countable: theory MFMC_Countable.MFMC_Web
23:20:55Three_Squares: theory Dirichlet_L.Dirichlet_Characters
23:20:56Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation
23:20:56Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
23:20:56Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral_Float
23:20:56Roth_Arithmetic_Progressions: theory HOL-Library.Interval_Float
23:20:56Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure
23:20:56Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
23:20:56Timing Neumann_Morgenstern_Utility (6 threads, 8.564s elapsed time, 26.910s cpu time, 2.024s GC time, factor 3.14)
23:20:56Finished Neumann_Morgenstern_Utility (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.82)
23:20:56Timing MDP-Rewards (2 threads, 39.212s elapsed time, 57.002s cpu time, 3.100s GC time, factor 1.45)
23:20:56Finished MDP-Rewards (0:00:59 elapsed time, 0:01:20 cpu time, factor 1.35)
23:20:56Timing Buffons_Needle (6 threads, 1.985s elapsed time, 7.274s cpu time, 0.148s GC time, factor 3.66)
23:20:56DiscretePricing: theory DiscretePricing.Fair_Price
23:20:56Finished Buffons_Needle (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.47)
23:20:56Median_Method: theory Median_Method.Median
23:20:56Timing QR_Decomposition (2 threads, 300.006s elapsed time, 518.170s cpu time, 41.967s GC time, factor 1.73)
23:20:56Finished QR_Decomposition (0:05:03 elapsed time, 0:08:42 cpu time, factor 1.72)
23:20:56Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
23:20:56Timing Source_Coding_Theorem (6 threads, 2.132s elapsed time, 5.177s cpu time, 0.171s GC time, factor 2.43)
23:20:56Finished Source_Coding_Theorem (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.79)
23:20:56Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
23:20:56Turans_Graph_Theorem: theory HOL-Library.Interval_Float
23:20:57Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
23:20:57Treaps: theory Landau_Symbols.Landau_Real_Products
23:20:57Treaps: theory List-Index.List_Index
23:20:57Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
23:20:57Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
23:20:57Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:20:57Girth_Chromatic: theory HOL-Library.Code_Target_Numeral_Float
23:20:57Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure
23:20:57Three_Squares: theory Dirichlet_Series.Dirichlet_Product
23:20:57Girth_Chromatic: theory HOL-Library.Interval_Float
23:20:57Projective_Measurements: theory Jordan_Normal_Form.Conjugate
23:20:57Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
23:20:57Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation_Bounds
23:20:57List_Update: theory List_Update.Comb
23:20:58Three_Squares: theory Dirichlet_Series.Dirichlet_Series
23:20:58Fisher_Yates: theory Fisher_Yates.Fisher_Yates
23:20:58Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
23:20:58Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
23:20:58Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Winding_Numbers
23:20:58Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
23:20:58Timing Skip_Lists (6 threads, 3.533s elapsed time, 14.935s cpu time, 0.437s GC time, factor 4.23)
23:20:58Finished Skip_Lists (0:00:04 elapsed time, 0:00:16 cpu time, factor 3.30)
23:20:58Lovasz_Local: theory Lovasz_Local.Digraph_Extensions
23:20:58Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
23:20:58Three_Squares: theory Dirichlet_Series.Euler_Products
23:20:58Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
23:20:58Projective_Measurements: theory Matrix.Utility
23:20:58Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Lemma
23:20:59Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residues
23:20:59Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
23:20:59Timing Hahn_Jordan_Decomposition (6 threads, 11.354s elapsed time, 27.093s cpu time, 0.858s GC time, factor 2.39)
23:20:59Finished Hahn_Jordan_Decomposition (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.22)
23:20:59Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
23:20:59Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
23:20:59Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
23:20:59Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
23:20:59Three_Squares: theory Bernoulli.Bernoulli_Zeta
23:20:59Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
23:20:59Universal_Hash_Families: theory HOL-Algebra.Divisibility
23:20:59Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Conformal_Mappings
23:20:59Timing Lp (8 threads, 8.449s elapsed time, 43.761s cpu time, 2.199s GC time, factor 5.18)
23:20:59Finished Lp (0:00:09 elapsed time, 0:00:45 cpu time, factor 4.58)
23:21:00Schwartz_Zippel: theory Polynomials.Utils
23:21:00Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
23:21:00DiscretePricing: theory DiscretePricing.CRR_Model
23:21:00Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Bayesian_Linear_Regression
23:21:00Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
23:21:00Schwartz_Zippel: theory Polynomials.Power_Products
23:21:00Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
23:21:00MFMC_Countable: theory MFMC_Countable.MFMC_Reduction
23:21:00Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:21:00Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Singularities
23:21:00Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Root
23:21:01Executable_Randomized_Algorithms: theory HOL-Number_Theory.Euler_Criterion
23:21:01Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin
23:21:01Executable_Randomized_Algorithms: theory HOL-Number_Theory.Gauss
23:21:01Executable_Randomized_Algorithms: theory HOL-Number_Theory.Quadratic_Reciprocity
23:21:01Projective_Measurements: theory Regular-Sets.Regular_Set
23:21:01Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
23:21:01Executable_Randomized_Algorithms: theory HOL-Number_Theory.Pocklington
23:21:01Frequency_Moments: theory HOL-Number_Theory.Residues
23:21:02Universal_Hash_Families: theory HOL-Algebra.AbelCoset
23:21:02MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
23:21:02Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
23:21:02Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Residues
23:21:02Three_Squares: theory Dirichlet_Series.Moebius_Mu
23:21:02Frequency_Moments: theory HOL-Algebra.Polynomials
23:21:02Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residue_Primitive_Roots
23:21:02Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Residue_Theorem
23:21:02Three_Squares: theory Dirichlet_Series.More_Totient
23:21:02Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
23:21:02Three_Squares: theory Dirichlet_Series.Divisor_Count
23:21:02Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
23:21:03Three_Squares: theory Dirichlet_Series.Liouville_Lambda
23:21:03Executable_Randomized_Algorithms: theory HOL-Number_Theory.Number_Theory
23:21:03Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
23:21:03Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Laurent_Convergence
23:21:03Treaps: theory Landau_Symbols.Landau_Simprocs
23:21:03Three_Squares: theory Winding_Number_Eval.Missing_Algebraic
23:21:03Timing Fisher_Yates (2 threads, 4.689s elapsed time, 8.568s cpu time, 0.368s GC time, factor 1.83)
23:21:03Finished Fisher_Yates (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.47)
23:21:03Three_Squares: theory Dirichlet_Series.Partial_Summation
23:21:03Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Misc
23:21:04Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation
23:21:04Executable_Randomized_Algorithms: theory Dirichlet_Series.Multiplicative_Function
23:21:04DiscretePricing: theory DiscretePricing.Option_Price_Examples
23:21:04Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Product
23:21:04Universal_Hash_Families: theory HOL-Algebra.Module
23:21:04MFMC_Countable: theory MFMC_Countable.MFMC_Bounded
23:21:04Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
23:21:04MFMC_Countable: theory MFMC_Countable.MFMC_Unbounded
23:21:04Timing Linear_Recurrences (6 threads, 35.114s elapsed time, 94.801s cpu time, 8.003s GC time, factor 2.70)
23:21:04Finished Linear_Recurrences (0:00:36 elapsed time, 0:01:36 cpu time, factor 2.64)
23:21:04Treaps: theory Landau_Symbols.Landau_More
23:21:04Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
23:21:04Frequency_Moments: theory HOL-Number_Theory.Gauss
23:21:04Projective_Measurements: theory Jordan_Normal_Form.Matrix
23:21:04Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series
23:21:04Three_Squares: theory Winding_Number_Eval.Missing_Transcendental
23:21:04Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
23:21:05Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
23:21:05Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
23:21:05Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
23:21:05Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem
23:21:05Deep_Learning: theory Jordan_Normal_Form.DL_Rank
23:21:05Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
23:21:05Frequency_Moments: theory HOL-Number_Theory.Pocklington
23:21:05Timing Median_Method (2 threads, 10.861s elapsed time, 15.549s cpu time, 0.559s GC time, factor 1.43)
23:21:05Finished Median_Method (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.32)
23:21:05Executable_Randomized_Algorithms: theory Dirichlet_Series.Euler_Products
23:21:05Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
23:21:05MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
23:21:06Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
23:21:06Frequency_Moments: theory HOL-Number_Theory.Number_Theory
23:21:06Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Great_Picard
23:21:06Girth_Chromatic: theory HOL-Decision_Procs.Approximation
23:21:06Timing Lovasz_Local (8 threads, 15.254s elapsed time, 96.790s cpu time, 8.313s GC time, factor 6.35)
23:21:06Finished Lovasz_Local (0:00:16 elapsed time, 0:01:38 cpu time, factor 5.88)
23:21:07Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Riemann_Mapping
23:21:07Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Meromorphic
23:21:07Timing Standard_Borel_Spaces (6 threads, 19.794s elapsed time, 73.421s cpu time, 3.716s GC time, factor 3.71)
23:21:07Finished Standard_Borel_Spaces (0:00:21 elapsed time, 0:01:14 cpu time, factor 3.54)
23:21:07Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
23:21:08Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval
23:21:08Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
23:21:08Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
23:21:08Projective_Measurements: theory Regular-Sets.Regular_Exp
23:21:08Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
23:21:08MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
23:21:08MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation_MFMC
23:21:08Universal_Hash_Families: theory HOL-Algebra.Ideal
23:21:08Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
23:21:09Executable_Randomized_Algorithms: theory Dirichlet_Series.Moebius_Mu
23:21:09Treaps: theory Random_BSTs.Random_BSTs
23:21:09Three_Squares: theory Three_Squares.Quadratic_Forms
23:21:09Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
23:21:09Executable_Randomized_Algorithms: theory Dirichlet_Series.More_Totient
23:21:09Executable_Randomized_Algorithms: theory Dirichlet_Series.Divisor_Count
23:21:09Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
23:21:10Executable_Randomized_Algorithms: theory Dirichlet_Series.Liouville_Lambda
23:21:10Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Analysis
23:21:10Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Coin_Space
23:21:10Executable_Randomized_Algorithms: theory Dirichlet_Series.Arithmetic_Summatory
23:21:10Three_Squares: theory Landau_Symbols.Group_Sort
23:21:10Executable_Randomized_Algorithms: theory Dirichlet_Series.Partial_Summation
23:21:10Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
23:21:10Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:21:10Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
23:21:11Timing DiscretePricing (6 threads, 22.655s elapsed time, 103.535s cpu time, 9.505s GC time, factor 4.57)
23:21:11Finished DiscretePricing (0:00:24 elapsed time, 0:01:45 cpu time, factor 4.36)
23:21:11Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
23:21:11Frequency_Moments: theory Median_Method.Median
23:21:11Projective_Measurements: theory Regular-Sets.NDerivative
23:21:11Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
23:21:11Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series_Analysis
23:21:11Three_Squares: theory Landau_Symbols.Landau_Real_Products
23:21:12Probabilistic_Prime_Tests: theory HOL-Algebra.Elementary_Groups
23:21:12Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
23:21:12Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Permuted_Congruential_Generator
23:21:12Timing Ordinary_Differential_Equations (2 threads, 297.964s elapsed time, 462.390s cpu time, 24.120s GC time, factor 1.55)
23:21:12Finished Ordinary_Differential_Equations (0:05:38 elapsed time, 0:08:34 cpu time, factor 1.52)
23:21:12Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
23:21:12Universal_Hash_Families: theory HOL-Algebra.RingHom
23:21:12Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
23:21:13Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
23:21:13Projective_Measurements: theory Jordan_Normal_Form.Determinant
23:21:13Frequency_Moments: theory Lp.Functional_Spaces
23:21:13Three_Squares: theory Zeta_Function.Zeta_Library
23:21:13Probabilistic_Prime_Tests: theory HOL-Algebra.Product_Groups
23:21:13Three_Squares: theory Zeta_Function.Zeta_Function
23:21:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
23:21:13Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
23:21:14Universal_Hash_Families: theory HOL-Algebra.QuotRing
23:21:14Universal_Hash_Families: theory HOL-Algebra.UnivPoly
23:21:14Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups
23:21:14Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
23:21:14Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
23:21:14Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
23:21:15Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
23:21:15Timing Ergodic_Theory (6 threads, 36.707s elapsed time, 136.824s cpu time, 8.672s GC time, factor 3.73)
23:21:15Finished Ergodic_Theory (0:00:47 elapsed time, 0:02:34 cpu time, factor 3.28)
23:21:15Executable_Randomized_Algorithms: theory MFMC_Countable.MFMC_Misc
23:21:15Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
23:21:16Three_Squares: theory Landau_Symbols.Landau_Simprocs
23:21:16Projective_Measurements: theory Regular-Sets.Equivalence_Checking
23:21:16Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample
23:21:16Executable_Randomized_Algorithms: theory MFMC_Countable.Matrix_For_Marginals
23:21:16Projective_Measurements: theory Regular-Sets.Relation_Interpretation
23:21:16Projective_Measurements: theory Regular-Sets.Regexp_Method
23:21:17Frequency_Moments: theory Lp.Lp
23:21:17Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
23:21:17Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
23:21:17Executable_Randomized_Algorithms: theory MFMC_Countable.Rel_PMF_Characterisation
23:21:17Three_Squares: theory Landau_Symbols.Landau_More
23:21:17Projective_Measurements: theory VectorSpace.FunctionLemmas
23:21:17Executable_Randomized_Algorithms: theory Probabilistic_While.While_SPMF
23:21:17Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
23:21:17Projective_Measurements: theory VectorSpace.RingModuleFacts
23:21:17Three_Squares: theory Lehmer.Lehmer
23:21:17Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
23:21:17Universal_Hash_Families: theory HOL-Algebra.IntRing
23:21:17Timing Probabilistic_While (2 threads, 56.458s elapsed time, 85.347s cpu time, 2.828s GC time, factor 1.51)
23:21:17Finished Probabilistic_While (0:01:19 elapsed time, 0:01:54 cpu time, factor 1.43)
23:21:17Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
23:21:17Three_Squares: theory Pratt_Certificate.Pratt_Certificate
23:21:18Frequency_Moments: theory Lehmer.Lehmer
23:21:18Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
23:21:18Executable_Randomized_Algorithms: theory Probabilistic_While.Bernoulli
23:21:18Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
23:21:18Executable_Randomized_Algorithms: theory Probabilistic_While.Geometric
23:21:19Projective_Measurements: theory VectorSpace.MonoidSums
23:21:19Running MDP-Algorithms (on of2.proof.cit.tum.de) ...
23:21:19Executable_Randomized_Algorithms: theory Zeta_Function.Zeta_Library
23:21:19Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions
23:21:19Projective_Measurements: theory VectorSpace.LinearCombinations
23:21:19Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
23:21:19Projective_Measurements: theory Abstract-Rewriting.SN_Orders
23:21:20MDP-Algorithms: theory HOL-Eisbach.Eisbach
23:21:20MDP-Algorithms: theory Containers.Equal
23:21:20MDP-Algorithms: theory Containers.Extend_Partial_Order
23:21:20MDP-Algorithms: theory Containers.List_Fusion
23:21:20MDP-Algorithms: theory Deriving.Comparator
23:21:20MDP-Algorithms: theory Deriving.Derive_Manager
23:21:20MDP-Algorithms: theory Deriving.Generator_Aux
23:21:20MDP-Algorithms: theory Containers.Closure_Set
23:21:20MDP-Algorithms: theory HOL-Computational_Algebra.Fraction_Field
23:21:20MDP-Algorithms: theory HOL-Data_Structures.Array_Specs
23:21:20MDP-Algorithms: theory Deriving.Equality_Generator
23:21:20MDP-Algorithms: theory HOL-Data_Structures.Cmp
23:21:21Three_Squares: theory Bertrands_Postulate.Bertrand
23:21:21MDP-Algorithms: theory HOL-Data_Structures.Less_False
23:21:21MDP-Algorithms: theory HOL-Data_Structures.Sorted_Less
23:21:21MDP-Algorithms: theory Deriving.Equality_Instances
23:21:21MDP-Algorithms: theory HOL-Data_Structures.AList_Upd_Del
23:21:21MDP-Algorithms: theory HOL-Data_Structures.List_Ins_Del
23:21:21MDP-Algorithms: theory Containers.Containers_Auxiliary
23:21:21MDP-Algorithms: theory Deriving.Compare
23:21:21MDP-Algorithms: theory Deriving.Comparator_Generator
23:21:21MDP-Algorithms: theory HOL-Data_Structures.Set_Specs
23:21:21MDP-Algorithms: theory HOL-Data_Structures.Map_Specs
23:21:21MDP-Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
23:21:21MDP-Algorithms: theory HOL-Library.Char_ord
23:21:21MDP-Algorithms: theory HOL-Library.Code_Abstract_Nat
23:21:21MDP-Algorithms: theory HOL-Library.Code_Target_Int
23:21:21MDP-Algorithms: theory HOL-Library.Code_Target_Nat
23:21:21MDP-Algorithms: theory Containers.Lexicographic_Order
23:21:21MDP-Algorithms: theory HOL-Algebra.Congruence
23:21:21MDP-Algorithms: theory HOL-Library.Code_Target_Numeral
23:21:21MDP-Algorithms: theory Jordan_Normal_Form.Missing_Misc
23:21:21Frequency_Moments: theory Bertrands_Postulate.Bertrand
23:21:21MDP-Algorithms: theory HOL-Library.IArray
23:21:22MDP-Algorithms: theory HOL-Library.More_List
23:21:22MDP-Algorithms: theory Deriving.Compare_Generator
23:21:22Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm
23:21:22MDP-Algorithms: theory Containers.Containers_Generator
23:21:22MDP-Algorithms: theory Containers.Set_Linorder
23:21:22MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
23:21:22MDP-Algorithms: theory HOL-Library.RBT_Impl
23:21:22MDP-Algorithms: theory Deriving.Compare_Instances
23:21:22MDP-Algorithms: theory Containers.Collection_Enum
23:21:22MDP-Algorithms: theory HOL-Algebra.Order
23:21:22MDP-Algorithms: theory Containers.Collection_Eq
23:21:22Projective_Measurements: theory Matrix.Ordered_Semiring
23:21:22Treaps: theory Treaps.Treap
23:21:22Treaps: theory Treaps.Probability_Misc
23:21:22MDP-Algorithms: theory HOL-Data_Structures.Tree2
23:21:22MDP-Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
23:21:22MDP-Algorithms: theory Containers.DList_Set
23:21:23Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility
23:21:23Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings
23:21:23MDP-Algorithms: theory HOL-Data_Structures.Isin2
23:21:23Treaps: theory Treaps.Random_List_Permutation
23:21:23Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Basic_Randomized_Algorithms
23:21:23Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm
23:21:23MDP-Algorithms: theory HOL-Data_Structures.Lookup2
23:21:23MDP-Algorithms: theory HOL-Algebra.Lattice
23:21:23Projective_Measurements: theory Matrix.Matrix_Legacy
23:21:23MDP-Algorithms: theory HOL-Data_Structures.RBT
23:21:23MDP-Algorithms: theory Perron_Frobenius.Cancel_Card_Constraint
23:21:23MDP-Algorithms: theory Polynomial_Interpolation.Missing_Unsorted
23:21:23MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial
23:21:23Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_SPMF
23:21:24Treaps: theory Treaps.Treap_Sort_and_BSTs
23:21:24Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Dice_Roll
23:21:24MDP-Algorithms: theory HOL-Algebra.Complete_Lattice
23:21:24Projective_Measurements: theory VectorSpace.SumSpaces
23:21:25Projective_Measurements: theory VectorSpace.VectorSpace
23:21:25Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
23:21:25MDP-Algorithms: theory HOL-Algebra.Group
23:21:25MDP-Algorithms: theory HOL-Library.Code_Real_Approx_By_Float
23:21:25MDP-Algorithms: theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
23:21:25MDP-Algorithms: theory Jordan_Normal_Form.Conjugate
23:21:25Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
23:21:26Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
23:21:26MDP-Algorithms: theory HOL-Data_Structures.RBT_Set
23:21:26MDP-Algorithms: theory HOL-Algebra.Coset
23:21:27Treaps: theory Treaps.Random_Treap
23:21:27Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic_Misc
23:21:27MDP-Algorithms: theory HOL-Algebra.FiniteProduct
23:21:27Balog_Szemeredi_Gowers: theory Girth_Chromatic.Ugraphs
23:21:27Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
23:21:28MDP-Algorithms: theory HOL-Algebra.Ring
23:21:28Timing Randomised_Social_Choice (2 threads, 31.340s elapsed time, 53.422s cpu time, 4.353s GC time, factor 1.70)
23:21:28Finished Randomised_Social_Choice (0:00:56 elapsed time, 0:01:23 cpu time, factor 1.47)
23:21:28MDP-Algorithms: theory HOL-Data_Structures.RBT_Map
23:21:28MDP-Algorithms: theory HOL-Library.Tree_Real
23:21:28Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
23:21:28Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
23:21:28MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
23:21:28Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
23:21:28MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
23:21:28MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
23:21:29Balog_Szemeredi_Gowers: theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
23:21:29MDP-Algorithms: theory Containers.Collection_Order
23:21:29MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:21:30MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
23:21:30Timing Monomorphic_Monad (2 threads, 44.045s elapsed time, 71.959s cpu time, 7.828s GC time, factor 1.63)
23:21:30Finished Monomorphic_Monad (0:00:47 elapsed time, 0:01:15 cpu time, factor 1.59)
23:21:30MDP-Algorithms: theory MDP-Algorithms.MDP_fin
23:21:30MDP-Algorithms: theory HOL-Algebra.Module
23:21:30Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
23:21:30Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
23:21:30MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
23:21:30MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
23:21:31Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
23:21:31MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
23:21:31Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Combinatorics_Preliminaries
23:21:31Timing Quick_Sort_Cost (2 threads, 25.352s elapsed time, 38.929s cpu time, 2.323s GC time, factor 1.54)
23:21:31Finished Quick_Sort_Cost (0:00:48 elapsed time, 0:01:05 cpu time, factor 1.35)
23:21:31Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
23:21:31Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Energy_Lower_Bounds
23:21:32Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Sumset_Triangle_Inequality
23:21:32Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Basics
23:21:32MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
23:21:32MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
23:21:32Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues
23:21:32MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
23:21:32MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:21:33MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
23:21:33MDP-Algorithms: theory Show.Show
23:21:33Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
23:21:33MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
23:21:33Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
23:21:34Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
23:21:35Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Walks
23:21:35Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
23:21:35Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion
23:21:35Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
23:21:37Universal_Hash_Families: theory HOL-Algebra.Subrings
23:21:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss
23:21:37Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Bipartite_Graphs
23:21:37Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
23:21:38Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
23:21:38Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Connectivity
23:21:38Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
23:21:38Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
23:21:38Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
23:21:39Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
23:21:39Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Graph_Theory_Preliminaries
23:21:39Timing Echelon_Form (2 threads, 369.813s elapsed time, 634.184s cpu time, 46.989s GC time, factor 1.71)
23:21:39Finished Echelon_Form (0:06:41 elapsed time, 0:11:11 cpu time, factor 1.67)
23:21:40Timing Schwartz_Zippel (6 threads, 68.768s elapsed time, 302.164s cpu time, 69.285s GC time, factor 4.39)
23:21:40Finished Schwartz_Zippel (0:01:10 elapsed time, 0:05:05 cpu time, factor 4.33)
23:21:40Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
23:21:41Three_Squares: theory Dirichlet_L.Dirichlet_Theorem
23:21:41Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
23:21:42Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
23:21:43Three_Squares: theory Three_Squares.Three_Squares
23:21:44Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
23:21:44MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
23:21:44Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
23:21:45MDP-Algorithms: theory Show.Show_Instances
23:21:45MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
23:21:45Universal_Hash_Families: theory HOL-Algebra.Polynomials
23:21:45Timing Density_Compiler (6 threads, 75.812s elapsed time, 154.213s cpu time, 11.672s GC time, factor 2.03)
23:21:45Finished Density_Compiler (0:01:17 elapsed time, 0:02:36 cpu time, factor 2.02)
23:21:45MDP-Algorithms: theory VectorSpace.FunctionLemmas
23:21:45MDP-Algorithms: theory VectorSpace.RingModuleFacts
23:21:46MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
23:21:46MDP-Algorithms: theory VectorSpace.MonoidSums
23:21:46MDP-Algorithms: theory Jordan_Normal_Form.Matrix
23:21:46MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
23:21:46MDP-Algorithms: theory VectorSpace.LinearCombinations
23:21:47Building HOL-ODE-Numerics (on of2.proof.cit.tum.de) ...
23:21:47Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
23:21:48MDP-Algorithms: theory MDP-Algorithms.Code_Setup
23:21:48Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
23:21:48HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
23:21:48HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
23:21:48HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
23:21:48HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
23:21:48HOL-ODE-Numerics: theory Deriving.Comparator
23:21:48HOL-ODE-Numerics: theory Deriving.Derive_Manager
23:21:48HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
23:21:48HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
23:21:48HOL-ODE-Numerics: theory Deriving.Generator_Aux
23:21:48HOL-ODE-Numerics: theory HOL-Library.AList
23:21:49HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
23:21:49HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
23:21:49HOL-ODE-Numerics: theory Deriving.Equality_Generator
23:21:49HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
23:21:49HOL-ODE-Numerics: theory HOL-ex.Quicksort
23:21:49MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:21:49MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
23:21:49Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
23:21:49HOL-ODE-Numerics: theory HOL-Library.Char_ord
23:21:50HOL-ODE-Numerics: theory Deriving.Equality_Instances
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
23:21:50HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
23:21:50HOL-ODE-Numerics: theory Deriving.Compare
23:21:50HOL-ODE-Numerics: theory Deriving.Comparator_Generator
23:21:50HOL-ODE-Numerics: theory HOL-Library.Option_ord
23:21:50HOL-ODE-Numerics: theory HOL-Library.Parallel
23:21:50HOL-ODE-Numerics: theory HOL-Library.Type_Length
23:21:50HOL-ODE-Numerics: theory Automatic_Refinement.Misc
23:21:50HOL-ODE-Numerics: theory HOL-Library.Mapping
23:21:50HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
23:21:50HOL-ODE-Numerics: theory HOL-Library.Signed_Division
23:21:50HOL-ODE-Numerics: theory Deriving.Compare_Generator
23:21:50HOL-ODE-Numerics: theory HOL-Library.Word
23:21:50Building CryptHOL (on 10.195.8.29) ...
23:21:51HOL-ODE-Numerics: theory Deriving.Compare_Instances
23:21:51HOL-ODE-Numerics: theory HOL-Library.While_Combinator
23:21:51Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic
23:21:51MDP-Algorithms: theory VectorSpace.SumSpaces
23:21:51Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
23:21:51HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
23:21:51HOL-ODE-Numerics: theory Deriving.Countable_Generator
23:21:51Running Differential_Dynamic_Logic (on 10.195.8.29) ...
23:21:51HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
23:21:51HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
23:21:51HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
23:21:51MDP-Algorithms: theory VectorSpace.VectorSpace
23:21:52Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
23:21:52MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
23:21:52MDP-Algorithms: theory Jordan_Normal_Form.Determinant
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
23:21:52Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
23:21:52HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
23:21:53Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
23:21:53Timing Treaps (2 threads, 56.920s elapsed time, 102.660s cpu time, 5.671s GC time, factor 1.80)
23:21:53Finished Treaps (0:01:00 elapsed time, 0:01:46 cpu time, factor 1.76)
23:21:53MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
23:21:53HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
23:21:53MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
23:21:53HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
23:21:54Running SDS_Impossibility (on 10.195.8.46) ...
23:21:54HOL-ODE-Numerics: theory Collections.SetIterator
23:21:54HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
23:21:54Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
23:21:54Building Random_BSTs (on 10.195.8.46) ...
23:21:54CryptHOL: theory HOL-Eisbach.Eisbach
23:21:54Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
23:21:54CryptHOL: theory Applicative_Lifting.Applicative
23:21:54Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
23:21:54Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
23:21:54Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:21:54Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility
23:21:54HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
23:21:54MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
23:21:55HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
23:21:55MDP-Algorithms: theory MDP-Algorithms.Fin_Code
23:21:55MDP-Algorithms: theory MDP-Algorithms.GS_Code
23:21:55HOL-ODE-Numerics: theory Automatic_Refinement.Relators
23:21:55Timing Applicative_Lifting (2 threads, 47.179s elapsed time, 76.840s cpu time, 7.423s GC time, factor 1.63)
23:21:55Finished Applicative_Lifting (0:01:23 elapsed time, 0:02:00 cpu time, factor 1.45)
23:21:55MDP-Algorithms: theory MDP-Algorithms.MPI_Code
23:21:55MDP-Algorithms: theory MDP-Algorithms.VI_Code
23:21:55MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
23:21:55Running Laws_of_Large_Numbers (on of3.proof.cit.tum.de) ...
23:21:55HOL-ODE-Numerics: theory Collections.SetIteratorOperations
23:21:55CryptHOL: theory CryptHOL.Partial_Function_Set
23:21:55Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Prob_Space_Lemmas
23:21:55CryptHOL: theory HOL-Library.Case_Converter
23:21:55HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
23:21:55Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof
23:21:56Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
23:21:56HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
23:21:56Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
23:21:56SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
23:21:56Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
23:21:56HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
23:21:56CryptHOL: theory HOL-Library.Simps_Case_Conv
23:21:56CryptHOL: theory Applicative_Lifting.Applicative_Environment
23:21:56CryptHOL: theory Applicative_Lifting.Applicative_Set
23:21:56Random_BSTs: theory HOL-Data_Structures.Cmp
23:21:56CryptHOL: theory CryptHOL.Environment_Functor
23:21:56CryptHOL: theory CryptHOL.Set_Applicative
23:21:56Random_BSTs: theory HOL-Data_Structures.Less_False
23:21:56CryptHOL: theory HOL-Algebra.Congruence
23:21:56CryptHOL: theory HOL-Library.Function_Algebras
23:21:56Estimated completion: 25-Nov-2023 01:51:47 +0100 (took 1.269s)
23:21:57CryptHOL: theory HOL-Library.Type_Length
23:21:57Random_BSTs: theory HOL-Data_Structures.Sorted_Less
23:21:57Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
23:21:57HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
23:21:57HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
23:21:57MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
23:21:57HOL-ODE-Numerics: theory Collections.Assoc_List
23:21:57Timing Laws_of_Large_Numbers (6 threads, 0.456s elapsed time, 1.177s cpu time, 0.048s GC time, factor 2.58)
23:21:57Finished Laws_of_Large_Numbers (0:00:01 elapsed time)
23:21:57Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
23:21:57Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
23:21:57Random_BSTs: theory HOL-Data_Structures.Set_Specs
23:21:57CryptHOL: theory HOL-Algebra.Order
23:21:57CryptHOL: theory HOL-Library.Countable_Set_Type
23:21:57MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
23:21:57HOL-ODE-Numerics: theory Collections.Proper_Iterator
23:21:57Random_BSTs: theory HOL-Data_Structures.Tree_Set
23:21:57HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
23:21:57Timing Probabilistic_System_Zoo (2 threads, 76.765s elapsed time, 120.800s cpu time, 8.907s GC time, factor 1.57)
23:21:57HOL-ODE-Numerics: theory Collections.Diff_Array
23:21:58Finished Probabilistic_System_Zoo (0:01:20 elapsed time, 0:02:05 cpu time, factor 1.55)
23:21:58HOL-ODE-Numerics: theory Collections.SetIteratorGA
23:21:58Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
23:21:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
23:21:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
23:21:58HOL-ODE-Numerics: theory Collections.It_to_It
23:21:58HOL-ODE-Numerics: theory Word_Lib.More_Divides
23:21:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
23:21:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
23:21:58HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
23:21:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
23:21:58HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
23:21:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
23:21:58Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
23:21:58HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
23:21:58HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
23:21:58HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
23:21:59HOL-ODE-Numerics: theory Show.Show
23:21:59Frequency_Moments: theory Finite_Fields.Ring_Characteristic
23:21:59MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
23:21:59MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
23:21:59Random_BSTs: theory Random_BSTs.Random_BSTs
23:21:59Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary
23:21:59CryptHOL: theory HOL-Algebra.Lattice
23:21:59Timing Quasi_Borel_Spaces (2 threads, 79.300s elapsed time, 113.854s cpu time, 6.769s GC time, factor 1.44)
23:21:59Finished Quasi_Borel_Spaces (0:01:22 elapsed time, 0:01:57 cpu time, factor 1.42)
23:22:00HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
23:22:00Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
23:22:00HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
23:22:00Projective_Measurements: theory QHLProver.Complex_Matrix
23:22:00Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
23:22:00HOL-ODE-Numerics: theory Show.Show_Instances
23:22:00Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
23:22:00MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
23:22:00HOL-ODE-Numerics: theory Word_Lib.More_Word
23:22:00CryptHOL: theory HOL-Algebra.Complete_Lattice
23:22:01CryptHOL: theory Coinductive.Coinductive_Nat
23:22:01HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
23:22:01HOL-ODE-Numerics: theory Collections.Intf_Comp
23:22:01HOL-ODE-Numerics: theory Collections.Idx_Iterator
23:22:01HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
23:22:02CryptHOL: theory HOL-Algebra.Group
23:22:02MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
23:22:02MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
23:22:02MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
23:22:02Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
23:22:02CryptHOL: theory Coinductive.Coinductive_List
23:22:02MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
23:22:04Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
23:22:04Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
23:22:04Projective_Measurements: theory QHLProver.Gates
23:22:04Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
23:22:05Timing Fourier (2 threads, 90.591s elapsed time, 156.894s cpu time, 8.964s GC time, factor 1.73)
23:22:05Finished Fourier (0:01:33 elapsed time, 0:02:40 cpu time, factor 1.71)
23:22:05Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
23:22:05CryptHOL: theory HOL-Algebra.Coset
23:22:05Frequency_Moments: theory Frequency_Moments.K_Smallest
23:22:06MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
23:22:06Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
23:22:06Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
23:22:06Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
23:22:06Frequency_Moments: theory Frequency_Moments.Probability_Ext
23:22:07MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
23:22:08Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
23:22:09CryptHOL: theory CryptHOL.Cyclic_Group
23:22:09Timing Actuarial_Mathematics (2 threads, 94.794s elapsed time, 164.226s cpu time, 6.776s GC time, factor 1.73)
23:22:09Finished Actuarial_Mathematics (0:01:37 elapsed time, 0:02:47 cpu time, factor 1.71)
23:22:09Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
23:22:09CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
23:22:10Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
23:22:10Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
23:22:10MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:22:10Frequency_Moments: theory Frequency_Moments.Frequency_Moments
23:22:10HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
23:22:10Projective_Measurements: theory Projective_Measurements.Projective_Measurements
23:22:10HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
23:22:10HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
23:22:10HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
23:22:11HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
23:22:11HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
23:22:11HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
23:22:11HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
23:22:11HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
23:22:11Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
23:22:12HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
23:22:12HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
23:22:12HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
23:22:12HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
23:22:12CryptHOL: theory Coinductive.TLList
23:22:12Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
23:22:12Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
23:22:12CryptHOL: theory Applicative_Lifting.Applicative_PMF
23:22:12HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
23:22:13HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
23:22:13MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
23:22:13MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
23:22:13MDP-Algorithms: theory Containers.RBT_ext
23:22:13MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
23:22:14HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
23:22:14HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
23:22:14HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
23:22:14HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
23:22:14HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
23:22:15HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
23:22:15CryptHOL: theory Monad_Normalisation.Monad_Normalisation
23:22:15HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
23:22:15HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
23:22:15HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
23:22:16CryptHOL: theory CryptHOL.SPMF_Applicative
23:22:16CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
23:22:16CryptHOL: theory Landau_Symbols.Group_Sort
23:22:17Building Hermite (on 10.195.8.11) ...
23:22:17HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
23:22:18Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
23:22:18HOL-ODE-Numerics: theory Collections.Gen_Iterator
23:22:18HOL-ODE-Numerics: theory Collections.Intf_Map
23:22:18HOL-ODE-Numerics: theory Collections.Intf_Set
23:22:18CryptHOL: theory Landau_Symbols.Landau_Real_Products
23:22:18HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
23:22:18HOL-ODE-Numerics: theory Collections.Iterator
23:22:19HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
23:22:19HOL-ODE-Numerics: theory Native_Word.Uint32
23:22:19HOL-ODE-Numerics: theory Native_Word.Uint
23:22:19HOL-ODE-Numerics: theory Collections.Array_Iterator
23:22:19Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
23:22:19HOL-ODE-Numerics: theory Collections.Gen_Map
23:22:19HOL-ODE-Numerics: theory Collections.Gen_Map2Set
23:22:20Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
23:22:20Hermite: theory Hermite.Hermite
23:22:20HOL-ODE-Numerics: theory Collections.Impl_Array_Map
23:22:20HOL-ODE-Numerics: theory Collections.Impl_List_Map
23:22:21HOL-ODE-Numerics: theory Collections.Gen_Set
23:22:21HOL-ODE-Numerics: theory Collections.Impl_List_Set
23:22:21HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
23:22:21HOL-ODE-Numerics: theory Collections.Code_Target_ICF
23:22:21HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
23:22:22HOL-ODE-Numerics: theory Collections.HashCode
23:22:22HOL-ODE-Numerics: theory Collections.Intf_Hash
23:22:22HOL-ODE-Numerics: theory Deriving.Hash_Generator
23:22:22HOL-ODE-Numerics: theory Collections.Gen_Hash
23:22:22HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
23:22:22HOL-ODE-Numerics: theory Deriving.Hash_Instances
23:22:22HOL-ODE-Numerics: theory Deriving.Derive
23:22:23CryptHOL: theory Landau_Symbols.Landau_Simprocs
23:22:23Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
23:22:24Timing Random_BSTs (2 threads, 8.506s elapsed time, 12.056s cpu time, 0.576s GC time, factor 1.42)
23:22:24Finished Random_BSTs (0:00:29 elapsed time, 0:00:35 cpu time, factor 1.21)
23:22:24CryptHOL: theory Landau_Symbols.Landau_More
23:22:24Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
23:22:25Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
23:22:25CryptHOL: theory CryptHOL.Negligible
23:22:25Hermite: theory Hermite.Hermite_IArrays
23:22:26Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
23:22:27Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
23:22:28Running Stern_Brocot (on of2.proof.cit.tum.de) ...
23:22:30Stern_Brocot: theory Stern_Brocot.Cotree
23:22:30Markov_Models: theory Markov_Models.MDP_RP
23:22:34Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
23:22:35Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
23:22:37HOL-ODE-Numerics: theory HOL-Library.RBT
23:22:37HOL-ODE-Numerics: theory Collections.RBT_add
23:22:38HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
23:22:38HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
23:22:38HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
23:22:40Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
23:22:41CryptHOL: theory CryptHOL.Misc_CryptHOL
23:22:43Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
23:22:44MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
23:22:44HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
23:22:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
23:22:46MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
23:22:46MDP-Algorithms: theory Containers.RBT_Mapping2
23:22:47Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
23:22:47MDP-Algorithms: theory Containers.RBT_Set2
23:22:47Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
23:22:47Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
23:22:48Timing E_Transcendental (2 threads, 206.703s elapsed time, 312.521s cpu time, 77.965s GC time, factor 1.51)
23:22:48Finished E_Transcendental (0:03:53 elapsed time, 0:05:42 cpu time, factor 1.47)
23:22:49Stern_Brocot: theory Stern_Brocot.Bird_Tree
23:22:49MDP-Algorithms: theory Containers.Set_Impl
23:22:49Running Randomised_BSTs (on of2.proof.cit.tum.de) ...
23:22:50HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
23:22:50HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
23:22:50Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
23:22:50Timing Stern_Brocot (6 threads, 19.804s elapsed time, 34.706s cpu time, 4.185s GC time, factor 1.75)
23:22:50Finished Stern_Brocot (0:00:21 elapsed time, 0:00:37 cpu time, factor 1.71)
23:22:51Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
23:22:51Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
23:22:52HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
23:22:54HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
23:22:54HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
23:22:54HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
23:22:54Timing Turans_Graph_Theorem (2 threads, 127.703s elapsed time, 221.279s cpu time, 15.253s GC time, factor 1.73)
23:22:54Finished Turans_Graph_Theorem (0:02:11 elapsed time, 0:03:45 cpu time, factor 1.72)
23:22:54Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
23:22:56CryptHOL: theory CryptHOL.Generat
23:22:56Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
23:22:56Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
23:22:56CryptHOL: theory CryptHOL.List_Bits
23:22:56CryptHOL: theory CryptHOL.Resumption
23:22:57Timing Randomised_BSTs (6 threads, 4.448s elapsed time, 15.224s cpu time, 0.542s GC time, factor 3.42)
23:22:57Finished Randomised_BSTs (0:00:06 elapsed time, 0:00:16 cpu time, factor 2.75)
23:22:57Timing MFMC_Countable (2 threads, 128.741s elapsed time, 207.925s cpu time, 10.279s GC time, factor 1.62)
23:22:57Finished MFMC_Countable (0:02:12 elapsed time, 0:03:32 cpu time, factor 1.60)
23:22:59Timing SDS_Impossibility (2 threads, 61.315s elapsed time, 80.461s cpu time, 3.942s GC time, factor 1.31)
23:22:59Finished SDS_Impossibility (0:01:04 elapsed time, 0:01:23 cpu time, factor 1.30)
23:22:59Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
23:23:00CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
23:23:02MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
23:23:03MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
23:23:04MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
23:23:05MDP-Algorithms: theory MDP-Algorithms.PI_Code
23:23:06Timing List_Update (2 threads, 158.139s elapsed time, 243.783s cpu time, 16.927s GC time, factor 1.54)
23:23:06Finished List_Update (0:02:41 elapsed time, 0:04:08 cpu time, factor 1.53)
23:23:11Timing Girth_Chromatic (2 threads, 105.722s elapsed time, 184.859s cpu time, 16.262s GC time, factor 1.75)
23:23:11Finished Girth_Chromatic (0:02:26 elapsed time, 0:03:55 cpu time, factor 1.60)
23:23:14MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
23:23:14MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
23:23:15Building Pi_Transcendental (on 10.195.6.179) ...
23:23:17Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
23:23:17Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
23:23:18Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
23:23:19Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
23:23:19Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
23:23:19Pi_Transcendental: theory HOL-Library.Fun_Lexorder
23:23:19Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
23:23:19Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:23:19Pi_Transcendental: theory HOL-Library.Poly_Mapping
23:23:20Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
23:23:21Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
23:23:21HOL-ODE-Numerics: theory Affine_Arithmetic.Print
23:23:22Pi_Transcendental: theory Polynomials.MPoly_Type
23:23:22Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
23:23:22Pi_Transcendental: theory Polynomials.More_MPoly_Type
23:23:22HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
23:23:23HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
23:23:23HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
23:23:23HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
23:23:23Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
23:23:23Pi_Transcendental: theory Symmetric_Polynomials.Vieta
23:23:24Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
23:23:26Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
23:23:26Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
23:23:27HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
23:23:27Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
23:23:27HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
23:23:27HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
23:23:27HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
23:23:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
23:23:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
23:23:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
23:23:31HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
23:23:31HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
23:23:31HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
23:23:32HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
23:23:32Timing Bernoulli (2 threads, 248.402s elapsed time, 389.217s cpu time, 100.108s GC time, factor 1.57)
23:23:32Finished Bernoulli (0:04:36 elapsed time, 0:07:03 cpu time, factor 1.53)
23:23:37Timing Markov_Models (2 threads, 164.638s elapsed time, 290.356s cpu time, 27.295s GC time, factor 1.76)
23:23:37Finished Markov_Models (0:03:36 elapsed time, 0:05:56 cpu time, factor 1.65)
23:23:37Timing Hermite (2 threads, 60.236s elapsed time, 93.083s cpu time, 5.633s GC time, factor 1.55)
23:23:37Finished Hermite (0:01:19 elapsed time, 0:01:55 cpu time, factor 1.45)
23:23:39Running Random_Graph_Subgraph_Threshold (on 10.195.8.49) ...
23:23:41CryptHOL: theory CryptHOL.Computational_Model
23:23:41CryptHOL: theory CryptHOL.GPV_Applicative
23:23:41HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
23:23:42Running Szemeredi_Regularity (on of2.proof.cit.tum.de) ...
23:23:42Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
23:23:43Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
23:23:43Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
23:23:44CryptHOL: theory CryptHOL.GPV_Expectation
23:23:44Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
23:23:45Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
23:23:45Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
23:23:46CryptHOL: theory CryptHOL.GPV_Bisim
23:23:46Timing Szemeredi_Regularity (6 threads, 2.601s elapsed time, 8.599s cpu time, 0.273s GC time, factor 3.31)
23:23:46Finished Szemeredi_Regularity (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.39)
23:23:47Running Stochastic_Matrices (on of3.proof.cit.tum.de) ...
23:23:47Running Probabilistic_Timed_Automata (on of3.proof.cit.tum.de) ...
23:23:47Running Hidden_Markov_Models (on of3.proof.cit.tum.de) ...
23:23:47CryptHOL: theory CryptHOL.CryptHOL
23:23:48Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
23:23:48Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
23:23:48Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
23:23:48Probabilistic_Timed_Automata: theory Timed_Automata.Misc
23:23:48Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
23:23:48Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
23:23:48Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
23:23:48Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
23:23:48Stochastic_Matrices: theory HOL-Eisbach.Eisbach
23:23:48Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
23:23:48Stochastic_Matrices: theory HOL-Algebra.Congruence
23:23:48Stochastic_Matrices: theory HOL-Library.Function_Algebras
23:23:48Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
23:23:48Stochastic_Matrices: theory HOL-Library.More_List
23:23:48Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
23:23:48Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
23:23:49Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
23:23:49Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
23:23:49Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
23:23:49Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
23:23:49Hidden_Markov_Models: theory HOL-Library.State_Monad
23:23:49Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
23:23:49Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
23:23:49Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
23:23:49Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
23:23:49Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
23:23:49Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
23:23:49Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
23:23:49Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
23:23:49Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
23:23:49Stochastic_Matrices: theory HOL-Algebra.Order
23:23:49Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
23:23:49Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
23:23:51Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
23:23:51Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
23:23:51Timing S_Finite_Measure_Monad (2 threads, 202.401s elapsed time, 314.784s cpu time, 16.032s GC time, factor 1.56)
23:23:51Finished S_Finite_Measure_Monad (0:03:26 elapsed time, 0:05:19 cpu time, factor 1.55)
23:23:51Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
23:23:51Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
23:23:51Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
23:23:51Stochastic_Matrices: theory VectorSpace.FunctionLemmas
23:23:51Stochastic_Matrices: theory HOL-Algebra.Lattice
23:23:51Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
23:23:52Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
23:23:52Hidden_Markov_Models: theory Monad_Memo_DP.Memory
23:23:52Probabilistic_Timed_Automata: theory Timed_Automata.DBM
23:23:52Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
23:23:52Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
23:23:52Probabilistic_Timed_Automata: theory Timed_Automata.Regions
23:23:53HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
23:23:53HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
23:23:53Stochastic_Matrices: theory HOL-Algebra.Group
23:23:53Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
23:23:53Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
23:23:54Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
23:23:54Timing Random_Graph_Subgraph_Threshold (2 threads, 11.136s elapsed time, 19.029s cpu time, 0.569s GC time, factor 1.71)
23:23:54Finished Random_Graph_Subgraph_Threshold (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.54)
23:23:54Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
23:23:54Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
23:23:54Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
23:23:55Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
23:23:55Probabilistic_Timed_Automata: theory Timed_Automata.Closure
23:23:55Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
23:23:55Stochastic_Matrices: theory HOL-Algebra.Coset
23:23:55Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
23:23:56Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
23:23:56Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
23:23:56Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
23:23:56Stochastic_Matrices: theory HOL-Algebra.Ring
23:23:56Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:23:56Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
23:23:56Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
23:23:57Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
23:23:57Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
23:23:57Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
23:23:57Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
23:23:58Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
23:23:59Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
23:23:59Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
23:23:59Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:23:59Stochastic_Matrices: theory HOL-Algebra.Module
23:23:59Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
23:24:00Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
23:24:01Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
23:24:01Stochastic_Matrices: theory VectorSpace.RingModuleFacts
23:24:01HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
23:24:01HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
23:24:01HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
23:24:01HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
23:24:02Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
23:24:02Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
23:24:05Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
23:24:06Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
23:24:08Stochastic_Matrices: theory VectorSpace.MonoidSums
23:24:08Stochastic_Matrices: theory VectorSpace.LinearCombinations
23:24:09Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
23:24:09Timing Hidden_Markov_Models (6 threads, 19.765s elapsed time, 48.787s cpu time, 6.954s GC time, factor 2.47)
23:24:09Finished Hidden_Markov_Models (0:00:21 elapsed time, 0:00:50 cpu time, factor 2.38)
23:24:09HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
23:24:10Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
23:24:10HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
23:24:11Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
23:24:12Stochastic_Matrices: theory VectorSpace.SumSpaces
23:24:12Stochastic_Matrices: theory VectorSpace.VectorSpace
23:24:12Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
23:24:12Building Smith_Normal_Form (on 10.195.8.11) ...
23:24:13Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:24:13Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
23:24:13Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
23:24:13Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
23:24:14Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
23:24:14Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
23:24:14Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
23:24:14Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
23:24:15Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
23:24:15HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
23:24:15Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
23:24:15Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
23:24:15Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
23:24:16Timing Roth_Arithmetic_Progressions (2 threads, 199.907s elapsed time, 349.612s cpu time, 33.051s GC time, factor 1.75)
23:24:16Finished Roth_Arithmetic_Progressions (0:03:38 elapsed time, 0:06:20 cpu time, factor 1.75)
23:24:16Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
23:24:16Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
23:24:16Timing Probabilistic_Noninterference (2 threads, 215.229s elapsed time, 343.254s cpu time, 23.652s GC time, factor 1.59)
23:24:16Smith_Normal_Form: theory HOL-Eisbach.Eisbach
23:24:16Finished Probabilistic_Noninterference (0:03:38 elapsed time, 0:05:47 cpu time, factor 1.59)
23:24:16Smith_Normal_Form: theory Deriving.Derive_Manager
23:24:16Smith_Normal_Form: theory Deriving.Generator_Aux
23:24:17Smith_Normal_Form: theory HOL-Number_Theory.Cong
23:24:17Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
23:24:17Smith_Normal_Form: theory HOL-Algebra.Congruence
23:24:18Building Stirling_Formula (on 10.195.8.49) ...
23:24:18Running Euler_MacLaurin (on 10.195.8.49) ...
23:24:19Smith_Normal_Form: theory HOL-Algebra.Order
23:24:19Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
23:24:19Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
23:24:19Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
23:24:20Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
23:24:20Running Lambert_W (on 10.195.6.179) ...
23:24:20Stirling_Formula: theory HOL-Library.Function_Algebras
23:24:20Stirling_Formula: theory Landau_Symbols.Group_Sort
23:24:21Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
23:24:21Smith_Normal_Form: theory HOL-Algebra.Lattice
23:24:21Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
23:24:21Euler_MacLaurin: theory HOL-Library.Function_Algebras
23:24:21Euler_MacLaurin: theory Landau_Symbols.Group_Sort
23:24:22Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
23:24:22HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
23:24:22Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
23:24:22Lambert_W: theory HOL-Library.Function_Algebras
23:24:22Lambert_W: theory Lambert_W.Lambert_W
23:24:22Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:24:23Timing Pi_Transcendental (2 threads, 44.392s elapsed time, 76.483s cpu time, 3.418s GC time, factor 1.72)
23:24:23Finished Pi_Transcendental (0:01:06 elapsed time, 0:01:41 cpu time, factor 1.52)
23:24:23Lambert_W: theory Landau_Symbols.Group_Sort
23:24:23Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
23:24:23Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
23:24:23Smith_Normal_Form: theory HOL-Algebra.Group
23:24:24Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
23:24:24Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
23:24:24Lambert_W: theory Landau_Symbols.Landau_Real_Products
23:24:25Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
23:24:25Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
23:24:25Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:24:26Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
23:24:26Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
23:24:26Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
23:24:26Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:24:27Smith_Normal_Form: theory HOL-Algebra.Coset
23:24:27Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
23:24:28Stirling_Formula: theory Landau_Symbols.Landau_More
23:24:28Stirling_Formula: theory Stirling_Formula.Stirling_Formula
23:24:28Lambert_W: theory Landau_Symbols.Landau_Simprocs
23:24:28Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
23:24:28Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
23:24:29Euler_MacLaurin: theory Landau_Symbols.Landau_More
23:24:29Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
23:24:29Lambert_W: theory Landau_Symbols.Landau_More
23:24:29Lambert_W: theory Stirling_Formula.Stirling_Formula
23:24:29Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
23:24:30Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
23:24:30Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series
23:24:30Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
23:24:30Smith_Normal_Form: theory HOL-Algebra.Ring
23:24:31Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
23:24:31Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
23:24:31Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
23:24:32Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
23:24:34Smith_Normal_Form: theory HOL-Number_Theory.Totient
23:24:35Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
23:24:35Smith_Normal_Form: theory HOL-Algebra.AbelCoset
23:24:36Smith_Normal_Form: theory HOL-Algebra.Module
23:24:38Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
23:24:39Smith_Normal_Form: theory HOL-Algebra.Ideal
23:24:42HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
23:24:43Running Hermite_Lindemann (on 10.195.6.179) ...
23:24:44Smith_Normal_Form: theory HOL-Algebra.RingHom
23:24:44Timing Euler_MacLaurin (2 threads, 22.229s elapsed time, 35.159s cpu time, 1.927s GC time, factor 1.58)
23:24:44Finished Euler_MacLaurin (0:00:25 elapsed time, 0:00:37 cpu time, factor 1.50)
23:24:45Timing Lambert_W (2 threads, 20.938s elapsed time, 37.724s cpu time, 1.561s GC time, factor 1.80)
23:24:45Finished Lambert_W (0:00:23 elapsed time, 0:00:40 cpu time, factor 1.70)
23:24:46Smith_Normal_Form: theory HOL-Algebra.UnivPoly
23:24:46Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
23:24:46Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
23:24:46Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
23:24:46Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
23:24:46Hermite_Lindemann: theory HOL-Library.Monad_Syntax
23:24:46Hermite_Lindemann: theory HOL-Algebra.Divisibility
23:24:46Hermite_Lindemann: theory Containers.Containers_Auxiliary
23:24:47Smith_Normal_Form: theory List-Index.List_Index
23:24:47Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
23:24:47Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
23:24:47Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
23:24:50Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
23:24:51Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
23:24:52Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
23:24:52Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
23:24:53Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
23:24:54Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
23:24:54Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
23:24:54Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:24:54Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
23:24:54Timing Balog_Szemeredi_Gowers (2 threads, 266.140s elapsed time, 441.389s cpu time, 40.102s GC time, factor 1.66)
23:24:54Finished Balog_Szemeredi_Gowers (0:04:30 elapsed time, 0:07:26 cpu time, factor 1.65)
23:24:55Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
23:24:55Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
23:24:55Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
23:24:56Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
23:24:57Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
23:24:58Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
23:24:58Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
23:24:58Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
23:24:58Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
23:24:58Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:24:58Hermite_Lindemann: theory Matrix.Utility
23:24:59Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
23:24:59Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
23:24:59Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
23:25:00Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
23:25:00Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
23:25:02Smith_Normal_Form: theory HOL-Number_Theory.Residues
23:25:02Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
23:25:02Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
23:25:03Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
23:25:04Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
23:25:04Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
23:25:04Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
23:25:05Timing Stirling_Formula (2 threads, 25.929s elapsed time, 44.039s cpu time, 2.133s GC time, factor 1.70)
23:25:05Finished Stirling_Formula (0:00:46 elapsed time, 0:01:08 cpu time, factor 1.49)
23:25:07Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
23:25:07Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
23:25:07Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
23:25:07Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
23:25:08Timing Dirichlet_Series (2 threads, 338.340s elapsed time, 544.744s cpu time, 129.856s GC time, factor 1.61)
23:25:08Finished Dirichlet_Series (0:06:12 elapsed time, 0:09:48 cpu time, factor 1.58)
23:25:08Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
23:25:09Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:25:09Smith_Normal_Form: theory Show.Show
23:25:10Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
23:25:11Smith_Normal_Form: theory Show.Show_Instances
23:25:11Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
23:25:12Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
23:25:12Smith_Normal_Form: theory Show.Show_Poly
23:25:12Building Zeta_Function (on 10.195.7.194) ...
23:25:12Running Gauss_Sums (on 10.195.7.194) ...
23:25:12Timing Probabilistic_Timed_Automata (6 threads, 82.564s elapsed time, 306.603s cpu time, 53.101s GC time, factor 3.71)
23:25:12Finished Probabilistic_Timed_Automata (0:01:24 elapsed time, 0:05:09 cpu time, factor 3.67)
23:25:13Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
23:25:13Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
23:25:14Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
23:25:15Zeta_Function: theory Bernoulli.Bernoulli_Zeta
23:25:15Gauss_Sums: theory HOL-Algebra.QuotRing
23:25:15Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
23:25:15Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
23:25:16Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
23:25:17Smith_Normal_Form: theory VectorSpace.FunctionLemmas
23:25:17Smith_Normal_Form: theory VectorSpace.RingModuleFacts
23:25:17Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
23:25:17Smith_Normal_Form: theory VectorSpace.MonoidSums
23:25:18Hermite_Lindemann: theory Subresultants.More_Homomorphisms
23:25:18Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
23:25:18Timing MDP-Algorithms (6 threads, 234.117s elapsed time, 1054.581s cpu time, 327.531s GC time, factor 4.50)
23:25:18Finished MDP-Algorithms (0:03:57 elapsed time, 0:17:44 cpu time, factor 4.49)
23:25:18Smith_Normal_Form: theory VectorSpace.LinearCombinations
23:25:18Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
23:25:18Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
23:25:19Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
23:25:20Gauss_Sums: theory HOL-Algebra.IntRing
23:25:20Hermite_Lindemann: theory Subresultants.Resultant_Prelim
23:25:20Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
23:25:20Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
23:25:21Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
23:25:21Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
23:25:22Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
23:25:22Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
23:25:23Zeta_Function: theory HOL-Eisbach.Eisbach
23:25:23Zeta_Function: theory Pure-ex.Guess
23:25:23Hermite_Lindemann: theory Algebraic_Numbers.Resultant
23:25:23Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
23:25:23Smith_Normal_Form: theory VectorSpace.SumSpaces
23:25:23Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
23:25:23Smith_Normal_Form: theory VectorSpace.VectorSpace
23:25:23Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
23:25:23Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
23:25:23Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
23:25:24Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
23:25:24Zeta_Function: theory Sturm_Tarski.PolyMisc
23:25:24Zeta_Function: theory Winding_Number_Eval.Missing_Topology
23:25:24Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
23:25:24Zeta_Function: theory Zeta_Function.Zeta_Library
23:25:24Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
23:25:24Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
23:25:24Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
23:25:25Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
23:25:25Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
23:25:25Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
23:25:25Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
23:25:26Zeta_Function: theory Budan_Fourier.BF_Misc
23:25:26Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
23:25:27Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
23:25:27Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
23:25:27Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
23:25:27Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
23:25:27Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
23:25:27Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
23:25:27Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
23:25:27Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
23:25:27Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
23:25:28Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
23:25:28Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
23:25:28Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
23:25:28Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
23:25:29Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
23:25:29Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
23:25:29Timing Stochastic_Matrices (6 threads, 98.815s elapsed time, 383.741s cpu time, 70.193s GC time, factor 3.88)
23:25:29Finished Stochastic_Matrices (0:01:40 elapsed time, 0:06:28 cpu time, factor 3.85)
23:25:31Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
23:25:31Timing Deep_Learning (2 threads, 324.503s elapsed time, 571.908s cpu time, 77.245s GC time, factor 1.76)
23:25:31Finished Deep_Learning (0:05:29 elapsed time, 0:09:38 cpu time, factor 1.76)
23:25:31Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
23:25:32Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
23:25:32Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
23:25:34Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
23:25:35Zeta_Function: theory Zeta_Function.Zeta_Function
23:25:35Running Clique_and_Monotone_Circuits (on 10.195.8.49) ...
23:25:35Running Irrationals_From_THEBOOK (on 10.195.8.49) ...
23:25:35Running Comparison_Sort_Lower_Bound (on 10.195.8.49) ...
23:25:36Gauss_Sums: theory Gauss_Sums.Gauss_Sums
23:25:37Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
23:25:37Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
23:25:37Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
23:25:37Comparison_Sort_Lower_Bound: theory List-Index.List_Index
23:25:37Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
23:25:39Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
23:25:39Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
23:25:40Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
23:25:40Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
23:25:40Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
23:25:41Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
23:25:41Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
23:25:41Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
23:25:41Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
23:25:41Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
23:25:42Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
23:25:42Timing Irrationals_From_THEBOOK (2 threads, 4.281s elapsed time, 5.943s cpu time, 0.110s GC time, factor 1.39)
23:25:42Finished Irrationals_From_THEBOOK (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.19)
23:25:43Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
23:25:47Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:25:48Timing Comparison_Sort_Lower_Bound (2 threads, 9.507s elapsed time, 16.986s cpu time, 1.271s GC time, factor 1.79)
23:25:48Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.58)
23:25:48Timing Transcendence_Series_Hancl_Rucki (2 threads, 393.460s elapsed time, 659.575s cpu time, 142.339s GC time, factor 1.68)
23:25:48Finished Transcendence_Series_Hancl_Rucki (0:06:52 elapsed time, 0:11:32 cpu time, factor 1.68)
23:25:48Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
23:25:53Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
23:25:53Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
23:25:56Timing DOM_Components (2 threads, 470.504s elapsed time, 913.940s cpu time, 109.083s GC time, factor 1.94)
23:25:56Finished DOM_Components (0:07:54 elapsed time, 0:15:18 cpu time, factor 1.94)
23:25:58Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
23:25:59Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
23:26:02Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
23:26:03Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
23:26:03Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
23:26:04Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
23:26:04Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
23:26:07Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
23:26:09Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
23:26:09Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
23:26:09Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
23:26:10Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
23:26:14Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
23:26:14Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
23:26:16Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
23:26:16Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
23:26:23Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
23:26:28Timing Virtual_Substitution (2 threads, 643.577s elapsed time, 1047.226s cpu time, 189.310s GC time, factor 1.63)
23:26:28Finished Virtual_Substitution (0:10:51 elapsed time, 0:17:39 cpu time, factor 1.63)
23:26:39Timing Gauss_Sums (2 threads, 81.916s elapsed time, 151.632s cpu time, 13.769s GC time, factor 1.85)
23:26:39Finished Gauss_Sums (0:01:25 elapsed time, 0:02:36 cpu time, factor 1.82)
23:26:41Timing Clique_and_Monotone_Circuits (2 threads, 62.533s elapsed time, 78.874s cpu time, 2.287s GC time, factor 1.26)
23:26:41Finished Clique_and_Monotone_Circuits (0:01:05 elapsed time, 0:01:21 cpu time, factor 1.25)
23:27:04Timing Universal_Hash_Families (2 threads, 382.365s elapsed time, 701.083s cpu time, 246.215s GC time, factor 1.83)
23:27:04Finished Universal_Hash_Families (0:06:26 elapsed time, 0:11:47 cpu time, factor 1.83)
23:27:16Timing CryptHOL (2 threads, 271.429s elapsed time, 508.699s cpu time, 123.358s GC time, factor 1.87)
23:27:16Finished CryptHOL (0:05:20 elapsed time, 0:09:33 cpu time, factor 1.79)
23:27:17Estimated completion: 25-Nov-2023 00:59:33 +0100 (took 0.478s)
23:27:21Building Constructive_Cryptography (on 10.195.8.30) ...
23:27:22Building Game_Based_Crypto (on 10.195.8.30) ...
23:27:22Running Sigma_Commit_Crypto (on 10.195.8.30) ...
23:27:22Running ABY3_Protocols (on 10.195.8.30) ...
23:27:25Constructive_Cryptography: theory Constructive_Cryptography.Resource
23:27:25ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
23:27:25ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
23:27:25Game_Based_Crypto: theory HOL-Library.LaTeXsugar
23:27:25Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
23:27:26Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
23:27:26Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
23:27:26Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
23:27:26ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
23:27:27Sigma_Commit_Crypto: theory HOL-Algebra.Ring
23:27:27Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
23:27:27Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
23:27:27Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
23:27:28Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
23:27:28Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
23:27:28Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
23:27:29Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
23:27:29Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
23:27:29ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
23:27:29Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
23:27:30ABY3_Protocols: theory ABY3_Protocols.Multiplication
23:27:30Constructive_Cryptography: theory Constructive_Cryptography.Converter
23:27:30ABY3_Protocols: theory ABY3_Protocols.Shuffle
23:27:30Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
23:27:30Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
23:27:30ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
23:27:32Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
23:27:33Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
23:27:33Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
23:27:33Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
23:27:36Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
23:27:36Timing Hermite_Lindemann (2 threads, 167.953s elapsed time, 311.393s cpu time, 24.900s GC time, factor 1.85)
23:27:36Finished Hermite_Lindemann (0:02:51 elapsed time, 0:05:15 cpu time, factor 1.84)
23:27:36Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
23:27:37Timing Zeta_Function (2 threads, 103.030s elapsed time, 192.978s cpu time, 13.339s GC time, factor 1.87)
23:27:37Finished Zeta_Function (0:02:22 elapsed time, 0:04:01 cpu time, factor 1.69)
23:27:37Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
23:27:38Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
23:27:39Sigma_Commit_Crypto: theory HOL-Algebra.Module
23:27:39Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
23:27:39Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
23:27:40Constructive_Cryptography: theory Constructive_Cryptography.Random_System
23:27:40Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
23:27:41Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
23:27:41Constructive_Cryptography: theory Constructive_Cryptography.Wiring
23:27:41Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
23:27:41Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
23:27:43Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
23:27:43Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
23:27:44Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
23:27:44Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
23:27:44Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
23:27:44Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
23:27:44Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
23:27:45Timing ABY3_Protocols (2 threads, 18.859s elapsed time, 30.586s cpu time, 1.205s GC time, factor 1.62)
23:27:45Finished ABY3_Protocols (0:00:22 elapsed time, 0:00:33 cpu time, factor 1.51)
23:27:45Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
23:27:45Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
23:27:46HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
23:27:47Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
23:27:50Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
23:27:50Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
23:27:52Running Dirichlet_L (on 10.195.8.29) ...
23:27:52Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
23:27:52Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
23:27:52Building Prime_Distribution_Elementary (on 10.195.8.29) ...
23:27:52Building Prime_Number_Theorem (on 10.195.8.29) ...
23:27:54Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
23:27:55Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
23:27:55Dirichlet_L: theory HOL-Library.Lattice_Algebras
23:27:55Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
23:27:55Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
23:27:55Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
23:27:55Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
23:27:55Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
23:27:57Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
23:27:57Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
23:27:57Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
23:27:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
23:27:58Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
23:27:58Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
23:27:58Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
23:27:58Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
23:27:59Dirichlet_L: theory HOL-Library.Log_Nat
23:27:59Dirichlet_L: theory Lehmer.Lehmer
23:27:59Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
23:27:59Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
23:27:59Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
23:28:00Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
23:28:00Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
23:28:00Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
23:28:00Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
23:28:01Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
23:28:01Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
23:28:01Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
23:28:01Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
23:28:01Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
23:28:02Dirichlet_L: theory HOL-Library.Interval
23:28:02Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
23:28:02Dirichlet_L: theory HOL-Library.Float
23:28:03Constructive_Cryptography: theory Constructive_Cryptography.Examples
23:28:03Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
23:28:03Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
23:28:04Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
23:28:04Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
23:28:06Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
23:28:06Dirichlet_L: theory HOL-Library.Interval_Float
23:28:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
23:28:08Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
23:28:08Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
23:28:14Dirichlet_L: theory Bertrands_Postulate.Bertrand
23:28:25HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
23:28:50Timing Differential_Dynamic_Logic (2 threads, 411.306s elapsed time, 657.463s cpu time, 131.223s GC time, factor 1.60)
23:28:50Finished Differential_Dynamic_Logic (0:06:55 elapsed time, 0:11:04 cpu time, factor 1.60)
23:28:53Timing Game_Based_Crypto (2 threads, 60.359s elapsed time, 105.407s cpu time, 8.674s GC time, factor 1.75)
23:28:53Finished Game_Based_Crypto (0:01:30 elapsed time, 0:02:22 cpu time, factor 1.58)
23:29:06Running Multi_Party_Computation (on 10.195.8.46) ...
23:29:09Timing Prime_Number_Theorem (2 threads, 46.537s elapsed time, 77.926s cpu time, 4.568s GC time, factor 1.67)
23:29:09Finished Prime_Number_Theorem (0:01:15 elapsed time, 0:01:54 cpu time, factor 1.51)
23:29:10Multi_Party_Computation: theory HOL-Number_Theory.Cong
23:29:10Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
23:29:11Multi_Party_Computation: theory HOL-Algebra.Ring
23:29:11Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
23:29:13Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
23:29:15Multi_Party_Computation: theory HOL-Number_Theory.Totient
23:29:15Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
23:29:16Multi_Party_Computation: theory HOL-Algebra.AbelCoset
23:29:18Multi_Party_Computation: theory HOL-Algebra.Module
23:29:19Running Zeta_3_Irrational (on 10.195.8.29) ...
23:29:21Multi_Party_Computation: theory HOL-Algebra.Ideal
23:29:21Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
23:29:21Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
23:29:21Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
23:29:22Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
23:29:22Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
23:29:23Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
23:29:24Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
23:29:24Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
23:29:24Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
23:29:24Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
23:29:25Multi_Party_Computation: theory Multi_Party_Computation.ETP
23:29:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
23:29:25Multi_Party_Computation: theory HOL-Algebra.RingHom
23:29:25Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
23:29:25Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
23:29:26Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
23:29:26Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
23:29:27Multi_Party_Computation: theory HOL-Algebra.UnivPoly
23:29:27Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
23:29:27Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
23:29:30Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
23:29:34Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
23:29:37Timing HOL-ODE-Numerics (6 threads, 425.973s elapsed time, 2018.341s cpu time, 406.831s GC time, factor 4.74)
23:29:37Finished HOL-ODE-Numerics (0:07:46 elapsed time, 0:35:01 cpu time, factor 4.51)
23:29:37Timing Prime_Distribution_Elementary (2 threads, 68.395s elapsed time, 124.844s cpu time, 6.599s GC time, factor 1.83)
23:29:37Finished Prime_Distribution_Elementary (0:01:43 elapsed time, 0:02:45 cpu time, factor 1.60)
23:29:38Building Lorenz_Approximation (on of2.proof.cit.tum.de) ...
23:29:38Running HOL-ODE-ARCH-COMP (on of2.proof.cit.tum.de) ...
23:29:38Running HOL-ODE-Examples (on of2.proof.cit.tum.de) ...
23:29:38Running Poincare_Bendixson (on of2.proof.cit.tum.de) ...
23:29:39Multi_Party_Computation: theory Multi_Party_Computation.OT14
23:29:39Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
23:29:39HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
23:29:39HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
23:29:39HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
23:29:39HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
23:29:39Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
23:29:39Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
23:29:40Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
23:29:42Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
23:29:42Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
23:29:42Multi_Party_Computation: theory Multi_Party_Computation.GMW
23:29:43Poincare_Bendixson: theory Poincare_Bendixson.Invariance
23:29:44Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
23:29:44Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
23:29:46Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
23:29:46Multi_Party_Computation: theory HOL-Number_Theory.Residues
23:29:47Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
23:29:49Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
23:29:49Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
23:29:50Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
23:29:50Poincare_Bendixson: theory Poincare_Bendixson.Examples
23:29:53Timing Sigma_Commit_Crypto (2 threads, 146.041s elapsed time, 247.791s cpu time, 20.377s GC time, factor 1.70)
23:29:53Finished Sigma_Commit_Crypto (0:02:30 elapsed time, 0:04:13 cpu time, factor 1.68)
23:29:54Timing Executable_Randomized_Algorithms (2 threads, 582.265s elapsed time, 1000.632s cpu time, 223.534s GC time, factor 1.72)
23:29:54Finished Executable_Randomized_Algorithms (0:09:48 elapsed time, 0:16:49 cpu time, factor 1.72)
23:29:56Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
23:30:00Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
23:30:00Dirichlet_L: theory HOL-Algebra.QuotRing
23:30:01Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
23:30:01Timing Probabilistic_Prime_Tests (2 threads, 549.271s elapsed time, 993.438s cpu time, 283.557s GC time, factor 1.81)
23:30:01Finished Probabilistic_Prime_Tests (0:09:34 elapsed time, 0:17:18 cpu time, factor 1.81)
23:30:03Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
23:30:03Running Irrational_Series_Erdos_Straus (on 10.195.8.32) ...
23:30:03Running IMO2019 (on 10.195.8.32) ...
23:30:03Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
23:30:06IMO2019: theory IMO2019.IMO2019_Q5
23:30:06Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
23:30:06IMO2019: theory IMO2019.IMO2019_Q1
23:30:06IMO2019: theory IMO2019.IMO2019_Q4
23:30:06Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
23:30:06Dirichlet_L: theory HOL-Algebra.IntRing
23:30:06Estimated completion: 25-Nov-2023 00:43:50 +0100 (took 0.353s)
23:30:07Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
23:30:08Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
23:30:09Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
23:30:09Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
23:30:10Timing Affine_Arithmetic (2 threads, 771.903s elapsed time, 1308.860s cpu time, 225.770s GC time, factor 1.70)
23:30:10Finished Affine_Arithmetic (0:14:32 elapsed time, 0:24:25 cpu time, factor 1.68)
23:30:11Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
23:30:12Timing Complex_Bounded_Operators_Dependencies (2 threads, 815.467s elapsed time, 1353.126s cpu time, 205.373s GC time, factor 1.66)
23:30:12Finished Complex_Bounded_Operators_Dependencies (0:15:05 elapsed time, 0:24:36 cpu time, factor 1.63)
23:30:14Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
23:30:15Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
23:30:15Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
23:30:16Timing IMO2019 (2 threads, 10.457s elapsed time, 13.530s cpu time, 0.482s GC time, factor 1.29)
23:30:16Finished IMO2019 (0:00:13 elapsed time, 0:00:16 cpu time, factor 1.21)
23:30:16Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
23:30:18Timing Zeta_3_Irrational (2 threads, 55.121s elapsed time, 105.620s cpu time, 4.063s GC time, factor 1.92)
23:30:18Finished Zeta_3_Irrational (0:00:58 elapsed time, 0:01:48 cpu time, factor 1.87)
23:30:18Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
23:30:19Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
23:30:22Building Complex_Bounded_Operators (on 10.195.8.32) ...
23:30:24Running Taylor_Models (on 10.195.8.32) ...
23:30:26Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
23:30:27Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
23:30:27Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
23:30:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
23:30:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
23:30:31Timing Poincare_Bendixson (6 threads, 50.927s elapsed time, 131.393s cpu time, 8.732s GC time, factor 2.58)
23:30:31Finished Poincare_Bendixson (0:00:52 elapsed time, 0:02:13 cpu time, factor 2.53)
23:30:35Timing Irrational_Series_Erdos_Straus (2 threads, 29.580s elapsed time, 54.081s cpu time, 2.806s GC time, factor 1.83)
23:30:35Finished Irrational_Series_Erdos_Straus (0:00:32 elapsed time, 0:00:57 cpu time, factor 1.75)
23:30:42Taylor_Models: theory Taylor_Models.Polynomial_Expression
23:30:43HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
23:30:44Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
23:30:47Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
23:30:47Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
23:30:49Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
23:30:49Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
23:30:50Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
23:30:54Timing Constructive_Cryptography (2 threads, 171.876s elapsed time, 277.035s cpu time, 9.988s GC time, factor 1.61)
23:30:54Finished Constructive_Cryptography (0:03:30 elapsed time, 0:05:28 cpu time, factor 1.56)
23:30:56Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
23:30:58Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
23:30:59Running Constructive_Cryptography_CM (on 10.195.8.40) ...
23:31:02Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
23:31:02Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
23:31:02Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
23:31:02Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
23:31:04Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
23:31:05Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
23:31:06Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
23:31:07Timing Dirichlet_L (2 threads, 188.574s elapsed time, 342.819s cpu time, 27.536s GC time, factor 1.82)
23:31:07Finished Dirichlet_L (0:03:12 elapsed time, 0:05:48 cpu time, factor 1.81)
23:31:10Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
23:31:12Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
23:31:13Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
23:31:13Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
23:31:14Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
23:31:14Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
23:31:15Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
23:31:18Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
23:31:20Taylor_Models: theory HOL-Library.Function_Algebras
23:31:20Taylor_Models: theory Taylor_Models.Horner_Eval
23:31:20Taylor_Models: theory Taylor_Models.Float_Topology
23:31:20Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
23:31:21Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
23:31:24Taylor_Models: theory Taylor_Models.Taylor_Models
23:31:26Timing HOL-ODE-Examples (6 threads, 106.047s elapsed time, 415.746s cpu time, 15.207s GC time, factor 3.92)
23:31:26Finished HOL-ODE-Examples (0:01:47 elapsed time, 0:06:57 cpu time, factor 3.87)
23:31:40Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
23:31:40Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
23:31:50Timing Projective_Measurements (2 threads, 624.495s elapsed time, 1043.906s cpu time, 193.533s GC time, factor 1.67)
23:31:50Finished Projective_Measurements (0:11:22 elapsed time, 0:18:46 cpu time, factor 1.65)
23:31:51Timing Lorenz_Approximation (6 threads, 116.822s elapsed time, 292.071s cpu time, 37.391s GC time, factor 2.50)
23:31:51Finished Lorenz_Approximation (0:02:12 elapsed time, 0:05:20 cpu time, factor 2.42)
23:31:52Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
23:31:53Building Commuting_Hermitian (on 10.195.8.32) ...
23:31:54Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
23:31:55Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
23:31:56Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
23:31:56Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
23:31:56Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
23:31:57Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
23:31:59Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
23:32:00Taylor_Models: theory Taylor_Models.Experiments
23:32:09Timing HOL-ODE-ARCH-COMP (6 threads, 148.764s elapsed time, 425.416s cpu time, 32.379s GC time, factor 2.86)
23:32:09Finished HOL-ODE-ARCH-COMP (0:02:30 elapsed time, 0:07:07 cpu time, factor 2.84)
23:32:15Running Lorenz_C0 (on 10.195.8.29) ...
23:32:15Running Lorenz_C1 (on 10.195.8.29) ...
23:32:19Lorenz_C1: theory Lorenz_C1.Lorenz_C1
23:32:19Lorenz_C0: theory Lorenz_C0.Lorenz_C0
23:32:21Timing Lorenz_C1 (2 threads, 1.933s elapsed time, 2.610s cpu time, 0.057s GC time, factor 1.35)
23:32:21Finished Lorenz_C1 (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.09)
23:32:42Timing Taylor_Models (2 threads, 133.607s elapsed time, 233.662s cpu time, 23.150s GC time, factor 1.75)
23:32:42Finished Taylor_Models (0:02:17 elapsed time, 0:03:58 cpu time, factor 1.73)
23:32:55Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
23:33:07Timing Commuting_Hermitian (2 threads, 48.189s elapsed time, 88.737s cpu time, 6.578s GC time, factor 1.84)
23:33:07Finished Commuting_Hermitian (0:01:13 elapsed time, 0:02:01 cpu time, factor 1.67)
23:33:07Running TsirelsonBound (on 10.195.8.32) ...
23:33:10TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
23:33:12TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
23:33:13TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
23:33:13TsirelsonBound: theory TsirelsonBound.Tsirelson
23:33:47Timing Three_Squares (2 threads, 834.441s elapsed time, 1405.508s cpu time, 386.638s GC time, factor 1.68)
23:33:47Finished Three_Squares (0:14:48 elapsed time, 0:24:43 cpu time, factor 1.67)
23:33:52Running Polygonal_Number_Theorem (on 10.195.8.11) ...
23:33:55Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
23:33:56Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
23:33:56Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
23:33:56Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
23:34:20Timing Multi_Party_Computation (2 threads, 307.949s elapsed time, 569.688s cpu time, 40.800s GC time, factor 1.85)
23:34:20Finished Multi_Party_Computation (0:05:12 elapsed time, 0:09:35 cpu time, factor 1.84)
23:34:27Timing TsirelsonBound (2 threads, 75.763s elapsed time, 124.642s cpu time, 6.531s GC time, factor 1.65)
23:34:27Finished TsirelsonBound (0:01:19 elapsed time, 0:02:07 cpu time, factor 1.62)
23:34:57Timing Complex_Bounded_Operators (2 threads, 239.594s elapsed time, 453.545s cpu time, 36.764s GC time, factor 1.89)
23:34:57Finished Complex_Bounded_Operators (0:04:31 elapsed time, 0:08:17 cpu time, factor 1.83)
23:35:02Running Registers (on 10.195.8.30) ...
23:35:05Registers: theory HOL-Eisbach.Eisbach
23:35:05Registers: theory HOL-Library.Type_Length
23:35:08Registers: theory HOL-Library.Z2
23:35:08Registers: theory HOL-Library.Word
23:35:08Registers: theory Registers.Axioms
23:35:09Registers: theory Registers.Laws
23:35:10Registers: theory Registers.Axioms_Complement
23:35:10Registers: theory Registers.Laws_Complement
23:35:10Registers: theory Registers.Axioms_Classical
23:35:11Registers: theory Registers.Laws_Classical
23:35:13Registers: theory Registers.Misc
23:35:14Registers: theory Registers.Classical_Extra
23:35:17Timing Polygonal_Number_Theorem (2 threads, 80.159s elapsed time, 145.434s cpu time, 7.545s GC time, factor 1.81)
23:35:17Finished Polygonal_Number_Theorem (0:01:23 elapsed time, 0:02:29 cpu time, factor 1.78)
23:35:21Registers: theory Registers.Finite_Tensor_Product
23:35:22Registers: theory Registers.Axioms_Quantum
23:35:22Registers: theory Registers.Finite_Tensor_Product_Matrices
23:35:22Registers: theory Registers.Quantum
23:35:25Registers: theory Registers.Laws_Quantum
23:35:26Timing Frequency_Moments (2 threads, 861.965s elapsed time, 1598.091s cpu time, 546.379s GC time, factor 1.85)
23:35:26Finished Frequency_Moments (0:15:22 elapsed time, 0:27:57 cpu time, factor 1.82)
23:35:30Registers: theory Registers.Quantum_Extra
23:35:31Registers: theory Registers.Axioms_Complement_Quantum
23:35:32Registers: theory Registers.Laws_Complement_Quantum
23:35:32Registers: theory Registers.QHoare
23:35:32Registers: theory Registers.Teleport
23:35:33Registers: theory Registers.Check_Autogenerated_Files
23:35:36Registers: theory Registers.Quantum_Extra2
23:35:36Registers: theory Registers.Pure_States
23:35:42Building Expander_Graphs (on 10.195.6.179) ...
23:35:49Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
23:35:49Expander_Graphs: theory Graph_Theory.Rtrancl_On
23:35:49Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
23:35:50Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
23:35:50Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
23:35:51Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
23:35:51Expander_Graphs: theory Abstract-Rewriting.Seq
23:35:52Expander_Graphs: theory HOL-Library.More_List
23:35:52Expander_Graphs: theory Perron_Frobenius.Bij_Nat
23:35:52Expander_Graphs: theory HOL-Library.While_Combinator
23:35:53Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
23:35:54Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
23:35:54Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
23:35:55Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
23:35:56Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
23:35:56Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
23:35:58Expander_Graphs: theory Jordan_Normal_Form.Conjugate
23:36:05Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
23:36:05Expander_Graphs: theory HOL-Decision_Procs.Approximation
23:36:07Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:36:09Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
23:36:11Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
23:36:12Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
23:36:12Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:36:13Expander_Graphs: theory Graph_Theory.Stuff
23:36:13Expander_Graphs: theory Graph_Theory.Digraph
23:36:15Expander_Graphs: theory Graph_Theory.Arc_Walk
23:36:18Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
23:36:19Expander_Graphs: theory Graph_Theory.Pair_Digraph
23:36:25Expander_Graphs: theory Graph_Theory.Digraph_Component
23:36:29Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
23:36:31Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
23:36:31Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
23:36:32Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
23:36:35Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
23:36:37Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
23:36:40Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
23:36:41Expander_Graphs: theory Matrix.Utility
23:36:41Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
23:36:46Expander_Graphs: theory Jordan_Normal_Form.Matrix
23:36:55Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
23:36:55Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:36:57Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
23:36:57Expander_Graphs: theory Jordan_Normal_Form.Determinant
23:36:58Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
23:37:01Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
23:37:04Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
23:37:05Expander_Graphs: theory Regular-Sets.Regular_Set
23:37:05Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
23:37:06Expander_Graphs: theory VectorSpace.FunctionLemmas
23:37:06Expander_Graphs: theory VectorSpace.RingModuleFacts
23:37:07Expander_Graphs: theory VectorSpace.MonoidSums
23:37:07Expander_Graphs: theory VectorSpace.LinearCombinations
23:37:08Expander_Graphs: theory Regular-Sets.Regular_Exp
23:37:15Expander_Graphs: theory Regular-Sets.NDerivative
23:37:18Expander_Graphs: theory Regular-Sets.Relation_Interpretation
23:37:18Expander_Graphs: theory VectorSpace.SumSpaces
23:37:19Expander_Graphs: theory VectorSpace.VectorSpace
23:37:22Expander_Graphs: theory Regular-Sets.Equivalence_Checking
23:37:23Expander_Graphs: theory Regular-Sets.Regexp_Method
23:37:24Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
23:37:25Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
23:37:26Expander_Graphs: theory Abstract-Rewriting.SN_Orders
23:37:28Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
23:37:29Expander_Graphs: theory Matrix.Ordered_Semiring
23:37:30Expander_Graphs: theory Matrix.Matrix_Legacy
23:37:32Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
23:37:34Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
23:37:34Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
23:37:35Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
23:37:37Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
23:37:37Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
23:37:38Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
23:37:40Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
23:37:42Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
23:37:46Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:37:51Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
23:37:51Expander_Graphs: theory QHLProver.Complex_Matrix
23:37:51Expander_Graphs: theory Perron_Frobenius.HMA_Connect
23:37:56Expander_Graphs: theory QHLProver.Gates
23:37:56Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
23:38:02Expander_Graphs: theory Projective_Measurements.Projective_Measurements
23:38:04Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
23:38:05Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
23:38:09Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
23:38:15Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
23:38:16Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
23:38:18Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
23:38:21Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
23:38:58Timing Registers (2 threads, 230.144s elapsed time, 417.702s cpu time, 41.075s GC time, factor 1.81)
23:38:58Finished Registers (0:03:54 elapsed time, 0:07:03 cpu time, factor 1.80)
23:40:17Timing Smith_Normal_Form (2 threads, 874.426s elapsed time, 1508.755s cpu time, 293.362s GC time, factor 1.73)
23:40:17Finished Smith_Normal_Form (0:15:56 elapsed time, 0:27:03 cpu time, factor 1.70)
23:40:19Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.8.11) ...
23:40:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
23:40:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
23:40:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
23:40:29Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
23:40:29Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
23:40:29Estimated completion: 25-Nov-2023 00:23:39 +0100 (took 0.058s)
23:40:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
23:40:31Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
23:40:31Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
23:40:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
23:40:33Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
23:40:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
23:40:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
23:40:34Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
23:40:34Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
23:40:34Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
23:40:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
23:40:36Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
23:40:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
23:40:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
23:40:39Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
23:40:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
23:40:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
23:40:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
23:40:43Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
23:40:44Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
23:40:53Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
23:40:54Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
23:40:55Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
23:40:55Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
23:40:55Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
23:40:57Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
23:40:57Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
23:40:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
23:40:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
23:40:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
23:41:00Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
23:41:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
23:41:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
23:41:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
23:41:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
23:41:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
23:41:11Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
23:41:12Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
23:41:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
23:41:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
23:41:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
23:41:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
23:41:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
23:41:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
23:41:18Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
23:41:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
23:41:19Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
23:41:21Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
23:41:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
23:41:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
23:41:31Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
23:41:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
23:41:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
23:41:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
23:41:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
23:41:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
23:41:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
23:41:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
23:41:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
23:41:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
23:41:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
23:41:55Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
23:41:55Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
23:41:56Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
23:41:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
23:42:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
23:42:02Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
23:42:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
23:42:05Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
23:42:05Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
23:42:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
23:42:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
23:42:09Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
23:42:11Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
23:42:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
23:42:21Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
23:42:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
23:42:23Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
23:42:25Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
23:42:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
23:42:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
23:42:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
23:42:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
23:42:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
23:42:40Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
23:42:40Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
23:42:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
23:42:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
23:42:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
23:42:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
23:42:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
23:42:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
23:42:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
23:42:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
23:42:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
23:43:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
23:44:00Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
23:44:00Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
23:44:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
23:44:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
23:44:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
23:44:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
23:44:04Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
23:44:05Timing Constructive_Cryptography_CM (2 threads, 740.010s elapsed time, 1397.639s cpu time, 197.544s GC time, factor 1.89)
23:44:05Finished Constructive_Cryptography_CM (0:13:04 elapsed time, 0:24:38 cpu time, factor 1.88)
23:44:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
23:44:06Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
23:44:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
23:44:09Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
23:44:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
23:44:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
23:44:11Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
23:44:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
23:44:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
23:44:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
23:44:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
23:44:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
23:44:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
23:44:24Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
23:44:29Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
23:44:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
23:44:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
23:44:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
23:44:39Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
23:44:54Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
23:45:24Timing Cook_Levin (2 threads, 1818.661s elapsed time, 2993.913s cpu time, 206.002s GC time, factor 1.65)
23:45:24Finished Cook_Levin (0:30:25 elapsed time, 0:50:05 cpu time, factor 1.65)
23:45:47Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
23:45:47Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
23:46:41Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
23:46:41Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
23:47:28Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
23:47:29Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
23:48:04Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
23:48:27Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
23:48:27Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
23:48:35Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
23:48:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
23:50:35Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
23:50:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
23:51:32Timing Expander_Graphs (2 threads, 887.355s elapsed time, 1609.096s cpu time, 478.025s GC time, factor 1.81)
23:51:32Finished Expander_Graphs (0:15:43 elapsed time, 0:28:09 cpu time, factor 1.79)
23:51:33Running Distributed_Distinct_Elements (on 10.195.6.179) ...
23:51:38Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
23:51:38Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
23:51:38Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
23:51:39Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
23:51:39Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
23:51:39Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
23:51:40Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
23:51:40Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:51:45Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
23:51:47Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
23:51:47Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
23:51:47Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
23:51:48Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
23:51:48Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
23:51:54Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
23:51:54Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
23:51:54Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
23:51:55Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
23:52:01Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
23:52:01Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
23:52:03Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
23:52:04Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
23:52:08Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
23:52:08Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
23:52:17Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
23:52:18Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
23:52:26Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
23:52:29Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
23:52:30Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
23:52:33Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
23:53:49Timing Distributed_Distinct_Elements (2 threads, 129.617s elapsed time, 245.857s cpu time, 15.917s GC time, factor 1.90)
23:53:49Finished Distributed_Distinct_Elements (0:02:14 elapsed time, 0:04:11 cpu time, factor 1.87)
23:57:39Timing Lorenz_C0 (2 threads, 1519.622s elapsed time, 2984.397s cpu time, 72.748s GC time, factor 1.96)
23:57:39Finished Lorenz_C0 (0:25:23 elapsed time, 0:49:48 cpu time, factor 1.96)
00:23:39Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2580.165s elapsed time, 4739.116s cpu time, 1111.568s GC time, factor 1.84)
00:23:39Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:43:10 elapsed time, 1:19:18 cpu time, factor 1.84)
00:23:50*** Host "10.195.8.32": failed to work
00:23:50*** Error
00:23:50*** Host "10.195.8.49": failed to work
00:23:50*** Error
00:23:50*** Host "10.195.6.179": failed to work
00:23:50*** Error
00:23:50*** Host "of3.proof.cit.tum.de": failed to work
00:23:50*** Error
00:23:50*** Host "of2.proof.cit.tum.de": failed to work
00:23:50*** Error
00:23:50*** Host "10.195.8.29": failed to work
00:23:50*** Error
00:23:50*** Host "of4.proof.cit.tum.de": failed to work
00:23:50*** Error
00:23:50*** Host "10.195.8.30": failed to work
00:23:50*** Error
00:23:50*** Host "10.195.8.46": failed to work
00:23:50*** Error
00:23:51*** Host "10.195.8.42": failed to work
00:23:51*** ### Ignored report message: int
00:23:51*** ### Ignored report message: array\ int
00:23:51*** ### Ignored report message: int
00:23:51*** Host "10.195.7.194": failed to work
00:23:51*** Error
00:23:51*** Host "10.195.8.40": failed to work
00:23:51*** Error
00:23:51*** Host "10.195.8.11": failed to work
00:23:51*** Error
00:23:51Unfinished session(s): MiniSail
00:23:5100:23:51Finished at Sat Nov 25 00:23:51 GMT+1 2023
00:23:511:50:12 elapsed time, 54:24:15 cpu time, factor 29.62
00:23:51Build step 'Execute shell' marked build as failure
00:23:52Started calculate disk usage of build
00:23:52Finished Calculation of disk usage of build in 0 seconds
00:24:09Started calculate disk usage of workspace
00:24:10Finished Calculation of disk usage of workspace in 0 seconds
00:24:10Finished: FAILURE
![[Jenkins]](/jenkins/static/334b159c/images/svgs/logo.svg){kind=logo}
