Markov_Models: theory Markov_Models.MDP_RP
01:39:07MDP-Algorithms: theory HOL-Algebra.Coset
01:39:07MDP-Algorithms: theory HOL-Algebra.FiniteProduct
01:39:07Schwartz_Zippel: theory Regular-Sets.Regular_Set
01:39:07Treaps: theory Treaps.Treap_Sort_and_BSTs
01:39:08Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
01:39:08MDP-Algorithms: theory HOL-Library.Tree_Real
01:39:08Frequency_Moments: theory Lehmer.Lehmer
01:39:08Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin
01:39:08Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Moebius_Mu
01:39:08MDP-Algorithms: theory HOL-Algebra.Ring
01:39:08Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.More_Totient
01:39:08Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
01:39:08Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Misc
01:39:08HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
01:39:08Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
01:39:08Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count
01:39:08MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
01:39:08Executable_Randomized_Algorithms: theory Dirichlet_Series.Multiplicative_Function
01:39:08Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
01:39:08Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
01:39:08Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic_Misc
01:39:09Balog_Szemeredi_Gowers: theory Girth_Chromatic.Ugraphs
01:39:09Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Product
01:39:09Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Liouville_Lambda
01:39:09Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
01:39:09Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory
01:39:09MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
01:39:09Applicative_Lifting: theory Applicative_Lifting.Applicative
01:39:09HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
01:39:09Applicative_Lifting: theory Applicative_Lifting.Joinable
01:39:09Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
01:39:09Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation
01:39:09MDP-Algorithms: theory Containers.Collection_Order
01:39:09Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series
01:39:09Executable_Randomized_Algorithms: theory Dirichlet_Series.Euler_Products
01:39:09Applicative_Lifting: theory HOL-Library.State_Monad
01:39:09Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
01:39:09Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
01:39:09Universal_Hash_Families: theory HOL-Algebra.RingHom
01:39:09Deep_Learning: theory VectorSpace.SumSpaces
01:39:09Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
01:39:10HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
01:39:10HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
01:39:10Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
01:39:10HOL-ODE-Numerics: theory Collections.SetIterator
01:39:10Skip_Lists: theory Skip_Lists.Pi_pmf
01:39:10Bernoulli: theory HOL-Number_Theory.Residues
01:39:10Balog_Szemeredi_Gowers: theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
01:39:10Deep_Learning: theory VectorSpace.VectorSpace
01:39:11HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
01:39:11Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
01:39:11Timing Hermite (2 threads, 68.982s elapsed time, 102.318s cpu time, 4.582s GC time, factor 1.48)
01:39:11Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis
01:39:11Finished Hermite (0:01:35 elapsed time, 0:02:13 cpu time, factor 1.40)
01:39:11Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
01:39:11Universal_Hash_Families: theory HOL-Algebra.QuotRing
01:39:11Skip_Lists: theory Skip_Lists.Misc
01:39:11MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:39:11HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
01:39:11Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
01:39:11Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
01:39:11Treaps: theory Treaps.Random_Treap
01:39:11Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
01:39:11Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
01:39:11MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
01:39:11Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
01:39:11Skip_Lists: theory Skip_Lists.Geometric_PMF
01:39:11Universal_Hash_Families: theory HOL-Algebra.UnivPoly
01:39:11HOL-ODE-Numerics: theory Automatic_Refinement.Relators
01:39:11Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
01:39:12Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_List
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State
01:39:12Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
01:39:12Skip_Lists: theory Skip_Lists.Skip_List
01:39:12MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
01:39:12Frequency_Moments: theory Bertrands_Postulate.Bertrand
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
01:39:12Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Combinatorics_Preliminaries
01:39:12MDP-Algorithms: theory MDP-Algorithms.MDP_fin
01:39:12Quick_Sort_Cost: theory Landau_Symbols.Landau_More
01:39:12Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
01:39:12Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
01:39:12HOL-ODE-Numerics: theory Collections.SetIteratorOperations
01:39:12Executable_Randomized_Algorithms: theory Dirichlet_Series.Moebius_Mu
01:39:13Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
01:39:13MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
01:39:13Bernoulli: theory HOL-Number_Theory.Euler_Criterion
01:39:13Executable_Randomized_Algorithms: theory Dirichlet_Series.More_Totient
01:39:13Applicative_Lifting: theory Applicative_Lifting.Applicative_State
01:39:13Bernoulli: theory HOL-Number_Theory.Pocklington
01:39:13Executable_Randomized_Algorithms: theory Dirichlet_Series.Liouville_Lambda
01:39:13Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Energy_Lower_Bounds
01:39:13Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
01:39:13Executable_Randomized_Algorithms: theory Dirichlet_Series.Divisor_Count
01:39:13Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:39:13Applicative_Lifting: theory HOL-Library.Confluence
01:39:13Applicative_Lifting: theory HOL-Library.Function_Algebras
01:39:13Bernoulli: theory HOL-Number_Theory.Gauss
01:39:13HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
01:39:13Executable_Randomized_Algorithms: theory Dirichlet_Series.Arithmetic_Summatory
01:39:13MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
01:39:13Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Sumset_Triangle_Inequality
01:39:13Applicative_Lifting: theory HOL-Library.Confluent_Quotient
01:39:13Executable_Randomized_Algorithms: theory Dirichlet_Series.Partial_Summation
01:39:13MDP-Algorithms: theory HOL-Algebra.Module
01:39:13Bernoulli: theory HOL-Number_Theory.Residue_Primitive_Roots
01:39:13Bernoulli: theory HOL-Number_Theory.Quadratic_Reciprocity
01:39:13Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Basics
01:39:13Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
01:39:13Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
01:39:14Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
01:39:14HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
01:39:14Applicative_Lifting: theory HOL-Library.Function_Division
01:39:14Applicative_Lifting: theory HOL-Library.Dlist
01:39:14Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
01:39:14Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
01:39:14Deep_Learning: theory Deep_Learning.DL_Network
01:39:14Bernoulli: theory HOL-Number_Theory.Number_Theory
01:39:14Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
01:39:14Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef
01:39:14MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
01:39:14HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
01:39:14Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
01:39:14Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
01:39:15Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
01:39:15Universal_Hash_Families: theory HOL-Algebra.IntRing
01:39:15Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
01:39:15Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series_Analysis
01:39:15Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:39:16Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
01:39:16MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
01:39:16MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
01:39:16Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
01:39:16MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:39:16HOL-ODE-Numerics: theory Word_Lib.More_Divides
01:39:16Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
01:39:16Bernoulli: theory Bernoulli.Bernoulli_FPS
01:39:16Schwartz_Zippel: theory Regular-Sets.Regular_Exp
01:39:16HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
01:39:16MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
01:39:16HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
01:39:16Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
01:39:16HOL-ODE-Numerics: theory Collections.Assoc_List
01:39:16HOL-ODE-Numerics: theory Collections.Proper_Iterator
01:39:16Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation
01:39:16MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
01:39:17Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Walks
01:39:17Projective_Measurements: theory QHLProver.Complex_Matrix
01:39:17HOL-ODE-Numerics: theory Collections.SetIteratorGA
01:39:17MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
01:39:17Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
01:39:17Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda
01:39:17MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
01:39:17HOL-ODE-Numerics: theory Collections.Diff_Array
01:39:17Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter
01:39:17HOL-ODE-Numerics: theory Collections.It_to_It
01:39:17Deep_Learning: theory Deep_Learning.Tensor_Matricization
01:39:17Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Bipartite_Graphs
01:39:17Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed
01:39:18HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
01:39:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
01:39:18HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
01:39:18Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
01:39:18Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
01:39:18Applicative_Lifting: theory HOL-Proofs-Lambda.Eta
01:39:18Deep_Learning: theory Deep_Learning.DL_Shallow_Model
01:39:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
01:39:18Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Connectivity
01:39:18HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
01:39:18HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
01:39:18Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
01:39:18Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
01:39:18HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
01:39:18Applicative_Lifting: theory Applicative_Lifting.Combinators
01:39:18HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
01:39:19Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
01:39:19HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
01:39:19Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
01:39:19MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
01:39:19HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
01:39:19HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
01:39:19HOL-ODE-Numerics: theory Show.Show
01:39:19Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:39:19Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
01:39:19HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
01:39:19Timing Matrices_for_ODEs (2 threads, 190.649s elapsed time, 257.393s cpu time, 15.147s GC time, factor 1.35)
01:39:19Finished Matrices_for_ODEs (0:03:14 elapsed time, 0:04:20 cpu time, factor 1.34)
01:39:19Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Graph_Theory_Preliminaries
01:39:20HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
01:39:20Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
01:39:20Bernoulli: theory Bernoulli.Bernoulli_Zeta
01:39:20Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Library
01:39:20Projective_Measurements: theory QHLProver.Gates
01:39:20HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
01:39:20Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function
01:39:20Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
01:39:21Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
01:39:21HOL-ODE-Numerics: theory Show.Show_Instances
01:39:21MDP-Algorithms: theory Show.Show
01:39:21HOL-ODE-Numerics: theory Word_Lib.More_Word
01:39:21Deep_Learning: theory Jordan_Normal_Form.Column_Operations
01:39:22Executable_Randomized_Algorithms: theory Zeta_Function.Zeta_Library
01:39:22Deep_Learning: theory Jordan_Normal_Form.Determinant
01:39:22Schwartz_Zippel: theory Regular-Sets.NDerivative
01:39:22Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
01:39:23Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
01:39:23Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
01:39:23Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
01:39:23Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
01:39:23HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
01:39:23HOL-ODE-Numerics: theory Collections.Intf_Comp
01:39:23HOL-ODE-Numerics: theory Collections.Idx_Iterator
01:39:24Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
01:39:24HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
01:39:24HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
01:39:24HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
01:39:24Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
01:39:24Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
01:39:24Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
01:39:24HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
01:39:24Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
01:39:25Timing Randomised_Social_Choice (2 threads, 32.359s elapsed time, 49.187s cpu time, 3.351s GC time, factor 1.52)
01:39:25Finished Randomised_Social_Choice (0:01:04 elapsed time, 0:01:23 cpu time, factor 1.30)
01:39:25HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
01:39:25Deep_Learning: theory Deep_Learning.DL_Deep_Model
01:39:25Deep_Learning: theory Jordan_Normal_Form.VS_Connect
01:39:25Projective_Measurements: theory Projective_Measurements.Projective_Measurements
01:39:25Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm
01:39:25HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
01:39:25HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
01:39:26HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
01:39:26HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
01:39:26Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
01:39:26Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
01:39:26Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Basic_Randomized_Algorithms
01:39:26Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm
01:39:26Building Smith_Normal_Form (on 10.195.8.42) ...
01:39:27Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
01:39:27Schwartz_Zippel: theory Regular-Sets.Regexp_Method
01:39:27Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
01:39:27Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_SPMF
01:39:27Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
01:39:27Timing Monomorphic_Monad (2 threads, 52.993s elapsed time, 81.703s cpu time, 8.917s GC time, factor 1.54)
01:39:27HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
01:39:27Finished Monomorphic_Monad (0:00:56 elapsed time, 0:01:25 cpu time, factor 1.51)
01:39:28Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Dice_Roll
01:39:28Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
01:39:28Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
01:39:28HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
01:39:28HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
01:39:28Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
01:39:28Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
01:39:29HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
01:39:29HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
01:39:29HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
01:39:29Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:39:29Timing Skip_Lists (2 threads, 19.170s elapsed time, 31.491s cpu time, 0.898s GC time, factor 1.64)
01:39:29Finished Skip_Lists (0:00:22 elapsed time, 0:00:34 cpu time, factor 1.53)
01:39:30Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
01:39:30Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
01:39:30Schwartz_Zippel: theory Polynomials.Utils
01:39:30Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
01:39:31Timing Probabilistic_While (2 threads, 56.976s elapsed time, 98.889s cpu time, 5.386s GC time, factor 1.74)
01:39:31Finished Probabilistic_While (0:01:28 elapsed time, 0:02:16 cpu time, factor 1.55)
01:39:31Smith_Normal_Form: theory HOL-Eisbach.Eisbach
01:39:31Smith_Normal_Form: theory Deriving.Derive_Manager
01:39:31Smith_Normal_Form: theory Deriving.Generator_Aux
01:39:31HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
01:39:31Schwartz_Zippel: theory Polynomials.Power_Products
01:39:31Smith_Normal_Form: theory HOL-Number_Theory.Cong
01:39:31Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
01:39:32Universal_Hash_Families: theory HOL-Algebra.Subrings
01:39:32Smith_Normal_Form: theory HOL-Algebra.Congruence
01:39:32Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic
01:39:33Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
01:39:33Smith_Normal_Form: theory HOL-Algebra.Order
01:39:33Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
01:39:33HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
01:39:33Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
01:39:33HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
01:39:33HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
01:39:33Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
01:39:34HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
01:39:34HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
01:39:34Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
01:39:34Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
01:39:35Smith_Normal_Form: theory HOL-Algebra.Lattice
01:39:35Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
01:39:36Timing Neumann_Morgenstern_Utility (2 threads, 26.998s elapsed time, 43.743s cpu time, 2.723s GC time, factor 1.62)
01:39:36Finished Neumann_Morgenstern_Utility (0:00:30 elapsed time, 0:00:47 cpu time, factor 1.54)
01:39:36Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:39:36Timing Hahn_Jordan_Decomposition (2 threads, 31.594s elapsed time, 48.985s cpu time, 2.119s GC time, factor 1.55)
01:39:36Finished Hahn_Jordan_Decomposition (0:00:34 elapsed time, 0:00:52 cpu time, factor 1.49)
01:39:36Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
01:39:36Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
01:39:36Deep_Learning: theory Jordan_Normal_Form.DL_Rank
01:39:36HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
01:39:37Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:39:37Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
01:39:37Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
01:39:37HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
01:39:37HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
01:39:37HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
01:39:37Smith_Normal_Form: theory HOL-Algebra.Group
01:39:37Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Prob_Space_Lemmas
01:39:39Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof
01:39:40Timing Treaps (2 threads, 67.760s elapsed time, 112.437s cpu time, 6.517s GC time, factor 1.66)
01:39:40Finished Treaps (0:01:11 elapsed time, 0:01:56 cpu time, factor 1.62)
01:39:40Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
01:39:40Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:39:40Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
01:39:41MDP-Algorithms: theory VectorSpace.FunctionLemmas
01:39:41Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary
01:39:42Universal_Hash_Families: theory HOL-Algebra.Polynomials
01:39:42MDP-Algorithms: theory VectorSpace.RingModuleFacts
01:39:42Smith_Normal_Form: theory HOL-Algebra.Coset
01:39:42Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:39:42HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
01:39:43Timing Wetzels_Problem (2 threads, 77.170s elapsed time, 122.441s cpu time, 8.652s GC time, factor 1.59)
01:39:43Finished Wetzels_Problem (0:01:20 elapsed time, 0:02:06 cpu time, factor 1.56)
01:39:43Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
01:39:43MDP-Algorithms: theory VectorSpace.MonoidSums
01:39:43MDP-Algorithms: theory Show.Show_Instances
01:39:43MDP-Algorithms: theory VectorSpace.LinearCombinations
01:39:43HOL-ODE-Numerics: theory Collections.Gen_Iterator
01:39:43HOL-ODE-Numerics: theory Collections.Intf_Map
01:39:44HOL-ODE-Numerics: theory Collections.Intf_Set
01:39:44Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
01:39:44Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
01:39:44MDP-Algorithms: theory Jordan_Normal_Form.Matrix
01:39:44MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
01:39:44HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
01:39:44Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
01:39:45Timing Markov_Models (6 threads, 75.563s elapsed time, 233.085s cpu time, 62.143s GC time, factor 3.08)
01:39:45Finished Markov_Models (0:01:44 elapsed time, 0:04:33 cpu time, factor 2.61)
01:39:45Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
01:39:45HOL-ODE-Numerics: theory Collections.Iterator
01:39:45Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
01:39:45Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
01:39:45HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
01:39:45HOL-ODE-Numerics: theory Native_Word.Uint
01:39:45HOL-ODE-Numerics: theory Collections.Array_Iterator
01:39:46HOL-ODE-Numerics: theory Collections.Gen_Map
01:39:46HOL-ODE-Numerics: theory Collections.Gen_Map2Set
01:39:46HOL-ODE-Numerics: theory Collections.Gen_Set
01:39:46Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
01:39:46Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
01:39:46Smith_Normal_Form: theory HOL-Algebra.Ring
01:39:46HOL-ODE-Numerics: theory Collections.Impl_List_Set
01:39:46Timing Quasi_Borel_Spaces (2 threads, 74.018s elapsed time, 113.217s cpu time, 7.012s GC time, factor 1.53)
01:39:46Finished Quasi_Borel_Spaces (0:01:18 elapsed time, 0:01:57 cpu time, factor 1.50)
01:39:46MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
01:39:46Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
01:39:47Building CryptHOL (on 10.195.8.32) ...
01:39:47HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
01:39:47Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:39:47Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
01:39:47Running SDS_Impossibility (on 10.195.8.32) ...
01:39:47HOL-ODE-Numerics: theory Collections.Impl_Array_Map
01:39:47HOL-ODE-Numerics: theory Collections.Impl_List_Map
01:39:48Smith_Normal_Form: theory HOL-Number_Theory.Totient
01:39:48HOL-ODE-Numerics: theory Collections.Code_Target_ICF
01:39:48Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
01:39:48Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
01:39:48Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
01:39:49Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
01:39:49Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
01:39:49Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
01:39:49Running Probabilistic_System_Zoo (on 10.195.7.194) ...
01:39:49Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
01:39:50HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
01:39:50Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
01:39:50Smith_Normal_Form: theory HOL-Algebra.AbelCoset
01:39:50HOL-ODE-Numerics: theory Native_Word.Uint32
01:39:50SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
01:39:50MDP-Algorithms: theory VectorSpace.SumSpaces
01:39:50CryptHOL: theory HOL-Eisbach.Eisbach
01:39:50CryptHOL: theory Applicative_Lifting.Applicative
01:39:50Running Fourier (on 10.195.6.179) ...
01:39:50Smith_Normal_Form: theory HOL-Algebra.Module
01:39:51MDP-Algorithms: theory VectorSpace.VectorSpace
01:39:51Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
01:39:52MDP-Algorithms: theory MDP-Algorithms.Code_Setup
01:39:52CryptHOL: theory CryptHOL.Partial_Function_Set
01:39:52Timing Dirichlet_Series (6 threads, 92.424s elapsed time, 380.336s cpu time, 98.422s GC time, factor 4.12)
01:39:52Finished Dirichlet_Series (0:02:00 elapsed time, 0:07:04 cpu time, factor 3.53)
01:39:52CryptHOL: theory HOL-Library.Case_Converter
01:39:52Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More
01:39:52Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
01:39:52Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
01:39:53Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More
01:39:53Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
01:39:53MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:39:53MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
01:39:53Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
01:39:53CryptHOL: theory HOL-Library.Simps_Case_Conv
01:39:53CryptHOL: theory Applicative_Lifting.Applicative_Environment
01:39:53HOL-ODE-Numerics: theory Collections.HashCode
01:39:53CryptHOL: theory Applicative_Lifting.Applicative_Set
01:39:53CryptHOL: theory CryptHOL.Environment_Functor
01:39:53Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union
01:39:53CryptHOL: theory CryptHOL.Set_Applicative
01:39:53Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
01:39:53CryptHOL: theory HOL-Algebra.Congruence
01:39:53Smith_Normal_Form: theory HOL-Algebra.Ideal
01:39:53CryptHOL: theory HOL-Library.Function_Algebras
01:39:53CryptHOL: theory HOL-Library.Type_Length
01:39:53Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
01:39:53Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
01:39:53HOL-ODE-Numerics: theory Collections.Intf_Hash
01:39:54Fourier: theory Fourier.Confine
01:39:54Fourier: theory HOL-Library.Function_Algebras
01:39:54HOL-ODE-Numerics: theory Deriving.Hash_Generator
01:39:54Fourier: theory Fourier.Fourier_Aux2
01:39:54Running Lp (on 10.195.8.46) ...
01:39:54Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension
01:39:54HOL-ODE-Numerics: theory Collections.Gen_Hash
01:39:54Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
01:39:54HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
01:39:54Fourier: theory Fourier.Periodic
01:39:54Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
01:39:54Fourier: theory Ergodic_Theory.SG_Library_Complement
01:39:54CryptHOL: theory HOL-Library.Countable_Set_Type
01:39:54CryptHOL: theory HOL-Algebra.Order
01:39:54Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
01:39:55HOL-ODE-Numerics: theory Deriving.Hash_Instances
01:39:55Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
01:39:55Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
01:39:55HOL-ODE-Numerics: theory Deriving.Derive
01:39:55Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
01:39:56Fourier: theory Lp.Functional_Spaces
01:39:56Smith_Normal_Form: theory HOL-Algebra.RingHom
01:39:56CryptHOL: theory HOL-Algebra.Lattice
01:39:56MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
01:39:56Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
01:39:57Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
01:39:57CryptHOL: theory Coinductive.Coinductive_Nat
01:39:57Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
01:39:57Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
01:39:57Lp: theory HOL-Library.Function_Algebras
01:39:57Lp: theory Ergodic_Theory.SG_Library_Complement
01:39:57Smith_Normal_Form: theory HOL-Algebra.UnivPoly
01:39:57CryptHOL: theory HOL-Algebra.Complete_Lattice
01:39:57MDP-Algorithms: theory Jordan_Normal_Form.Determinant
01:39:58Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set
01:39:58Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bool_Bounded_Set
01:39:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
01:39:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
01:39:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
01:39:58Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
01:39:58Running Median_Method (on 10.195.8.30) ...
01:39:58Timing Quick_Sort_Cost (2 threads, 23.307s elapsed time, 43.566s cpu time, 2.992s GC time, factor 1.87)
01:39:58Finished Quick_Sort_Cost (0:00:55 elapsed time, 0:01:23 cpu time, factor 1.50)
01:39:58Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample
01:39:58Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
01:39:58Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
01:39:58Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
01:39:58Timing Standard_Borel_Spaces (2 threads, 93.268s elapsed time, 130.865s cpu time, 5.992s GC time, factor 1.40)
01:39:58Finished Standard_Borel_Spaces (0:01:36 elapsed time, 0:02:14 cpu time, factor 1.39)
01:39:58Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
01:39:59Lp: theory Lp.Functional_Spaces
01:39:59Smith_Normal_Form: theory List-Index.List_Index
01:39:59Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
01:39:59CryptHOL: theory Coinductive.Coinductive_List
01:39:59CryptHOL: theory HOL-Algebra.Group
01:39:59Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
01:40:00Fourier: theory Lp.Lp
01:40:00Running Source_Coding_Theorem (on 10.195.8.40) ...
01:40:00Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
01:40:00Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
01:40:01Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
01:40:01Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
01:40:01Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
01:40:01Fourier: theory Fourier.Lspace
01:40:01Fourier: theory Fourier.Square_Integrable
01:40:01Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
01:40:02CryptHOL: theory HOL-Algebra.Coset
01:40:02Timing Winding_Number_Eval (2 threads, 96.083s elapsed time, 168.936s cpu time, 10.617s GC time, factor 1.76)
01:40:02Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
01:40:02Finished Winding_Number_Eval (0:01:39 elapsed time, 0:02:52 cpu time, factor 1.73)
01:40:02Fourier: theory Fourier.Fourier
01:40:02Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
01:40:03MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
01:40:03MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
01:40:03MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
01:40:03Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
01:40:03Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
01:40:03Lp: theory Lp.Lp
01:40:03Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
01:40:03Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
01:40:03Median_Method: theory Median_Method.Median
01:40:03Timing Actuarial_Mathematics (2 threads, 101.257s elapsed time, 151.851s cpu time, 5.367s GC time, factor 1.50)
01:40:03Finished Actuarial_Mathematics (0:01:45 elapsed time, 0:02:35 cpu time, factor 1.48)
01:40:04MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
01:40:04Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
01:40:05CryptHOL: theory CryptHOL.Cyclic_Group
01:40:06CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
01:40:08CryptHOL: theory Coinductive.TLList
01:40:08CryptHOL: theory Applicative_Lifting.Applicative_PMF
01:40:09MDP-Algorithms: theory MDP-Algorithms.Fin_Code
01:40:09MDP-Algorithms: theory MDP-Algorithms.GS_Code
01:40:09MDP-Algorithms: theory MDP-Algorithms.MPI_Code
01:40:09MDP-Algorithms: theory MDP-Algorithms.VI_Code
01:40:09MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
01:40:09Timing Lovasz_Local (2 threads, 107.157s elapsed time, 170.595s cpu time, 15.368s GC time, factor 1.59)
01:40:09Finished Lovasz_Local (0:01:50 elapsed time, 0:02:54 cpu time, factor 1.57)
01:40:11Timing Source_Coding_Theorem (2 threads, 6.855s elapsed time, 10.140s cpu time, 0.289s GC time, factor 1.48)
01:40:11Finished Source_Coding_Theorem (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.29)
01:40:11CryptHOL: theory Monad_Normalisation.Monad_Normalisation
01:40:11Timing Median_Method (2 threads, 9.834s elapsed time, 15.674s cpu time, 0.605s GC time, factor 1.59)
01:40:11CryptHOL: theory CryptHOL.SPMF_Applicative
01:40:11Finished Median_Method (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.43)
01:40:12CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
01:40:12CryptHOL: theory Landau_Symbols.Group_Sort
01:40:13Timing Probabilistic_Prime_Tests (6 threads, 140.908s elapsed time, 679.343s cpu time, 233.432s GC time, factor 4.82)
01:40:13Finished Probabilistic_Prime_Tests (0:02:23 elapsed time, 0:11:25 cpu time, factor 4.78)
01:40:13MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
01:40:14CryptHOL: theory Landau_Symbols.Landau_Real_Products
01:40:14Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
01:40:15Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
01:40:15Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:40:16MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
01:40:16Timing Closest_Pair_Points (2 threads, 114.600s elapsed time, 192.094s cpu time, 7.144s GC time, factor 1.68)
01:40:16Finished Closest_Pair_Points (0:01:58 elapsed time, 0:03:16 cpu time, factor 1.66)
01:40:17Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
01:40:18Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
01:40:18Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
01:40:18CryptHOL: theory Landau_Symbols.Landau_Simprocs
01:40:19MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
01:40:19MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
01:40:19Smith_Normal_Form: theory HOL-Number_Theory.Residues
01:40:19CryptHOL: theory Landau_Symbols.Landau_More
01:40:19CryptHOL: theory CryptHOL.Negligible
01:40:19MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
01:40:20Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
01:40:20Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
01:40:21MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
01:40:21MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
01:40:21MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
01:40:21Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
01:40:22Running Stochastic_Matrices (on of4.proof.cit.tum.de) ...
01:40:23Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
01:40:23Stochastic_Matrices: theory HOL-Eisbach.Eisbach
01:40:23Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
01:40:23Stochastic_Matrices: theory HOL-Algebra.Congruence
01:40:23Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
01:40:23Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
01:40:23Stochastic_Matrices: theory HOL-Library.Function_Algebras
01:40:23Stochastic_Matrices: theory HOL-Library.More_List
01:40:23Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample
01:40:24Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
01:40:24Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
01:40:24Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
01:40:24Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
01:40:24Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
01:40:25Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
01:40:25Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
01:40:25Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
01:40:25Stochastic_Matrices: theory HOL-Algebra.Order
01:40:25Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
01:40:25Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
01:40:25Stochastic_Matrices: theory VectorSpace.FunctionLemmas
01:40:26Stochastic_Matrices: theory HOL-Algebra.Lattice
01:40:26Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
01:40:26MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
01:40:26Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
01:40:26Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
01:40:27Smith_Normal_Form: theory Show.Show
01:40:27Building Zeta_Function (on of2.proof.cit.tum.de) ...
01:40:27Stochastic_Matrices: theory HOL-Algebra.Group
01:40:28MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
01:40:28Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
01:40:29Timing DiscretePricing (2 threads, 128.662s elapsed time, 206.369s cpu time, 13.688s GC time, factor 1.60)
01:40:29Finished DiscretePricing (0:02:12 elapsed time, 0:03:31 cpu time, factor 1.59)
01:40:29Zeta_Function: theory Bernoulli.Bernoulli_Zeta
01:40:30Running Probabilistic_Timed_Automata (on 10.195.8.32) ...
01:40:30Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
01:40:30Stochastic_Matrices: theory HOL-Algebra.Coset
01:40:30Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
01:40:30Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
01:40:30Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
01:40:30Stochastic_Matrices: theory HOL-Algebra.Ring
01:40:31Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:40:31Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
01:40:31Running Gauss_Sums (on 10.195.8.32) ...
01:40:31MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:40:31Zeta_Function: theory HOL-Eisbach.Eisbach
01:40:31Zeta_Function: theory Pure-ex.Guess
01:40:31Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
01:40:31Zeta_Function: theory Sturm_Tarski.PolyMisc
01:40:31Zeta_Function: theory Winding_Number_Eval.Missing_Topology
01:40:31Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
01:40:32Smith_Normal_Form: theory Show.Show_Instances
01:40:32Zeta_Function: theory Zeta_Function.Zeta_Library
01:40:32Timing QR_Decomposition (2 threads, 279.601s elapsed time, 476.871s cpu time, 44.546s GC time, factor 1.71)
01:40:32Finished QR_Decomposition (0:04:43 elapsed time, 0:08:01 cpu time, factor 1.70)
01:40:32Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
01:40:32Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
01:40:33Timing Berlekamp_Zassenhaus (6 threads, 127.266s elapsed time, 448.954s cpu time, 101.345s GC time, factor 3.53)
01:40:33Finished Berlekamp_Zassenhaus (0:02:32 elapsed time, 0:08:13 cpu time, factor 3.24)
01:40:33Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
01:40:33Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
01:40:33Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
01:40:33Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
01:40:33Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:40:33Smith_Normal_Form: theory Show.Show_Poly
01:40:34Timing Applicative_Lifting (2 threads, 45.641s elapsed time, 72.379s cpu time, 6.043s GC time, factor 1.59)
01:40:34Finished Applicative_Lifting (0:01:26 elapsed time, 0:02:00 cpu time, factor 1.39)
01:40:34Zeta_Function: theory Budan_Fourier.BF_Misc
01:40:34Stochastic_Matrices: theory HOL-Algebra.Module
01:40:34Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
01:40:34MDP-Algorithms: theory Containers.RBT_ext
01:40:34MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
01:40:34Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
01:40:34Running Hidden_Markov_Models (on 10.195.7.194) ...
01:40:35Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
01:40:35Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
01:40:35Gauss_Sums: theory HOL-Algebra.QuotRing
01:40:35Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
01:40:35CryptHOL: theory CryptHOL.Misc_CryptHOL
01:40:35Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
01:40:35Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
01:40:35Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
01:40:35Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
01:40:35Probabilistic_Timed_Automata: theory Timed_Automata.Misc
01:40:36Stochastic_Matrices: theory VectorSpace.RingModuleFacts
01:40:36Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
01:40:36Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
01:40:36Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
01:40:36Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
01:40:36Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
01:40:37Stochastic_Matrices: theory VectorSpace.MonoidSums
01:40:37Timing Groebner_Macaulay (2 threads, 214.958s elapsed time, 293.164s cpu time, 46.727s GC time, factor 1.36)
01:40:37Finished Groebner_Macaulay (0:03:42 elapsed time, 0:05:02 cpu time, factor 1.36)
01:40:37Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
01:40:37Stochastic_Matrices: theory VectorSpace.LinearCombinations
01:40:37Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
01:40:37Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
01:40:37Smith_Normal_Form: theory VectorSpace.FunctionLemmas
01:40:37Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
01:40:37Smith_Normal_Form: theory VectorSpace.RingModuleFacts
01:40:37Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
01:40:38Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
01:40:38Zeta_Function: theory Zeta_Function.Zeta_Function
01:40:38Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
01:40:38Building Random_BSTs (on 10.195.8.29) ...
01:40:38Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
01:40:38Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
01:40:38MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
01:40:38Smith_Normal_Form: theory VectorSpace.MonoidSums
01:40:39Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
01:40:39MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
01:40:39Running Error_Function (on 10.195.8.29) ...
01:40:39Running Fisher_Yates (on 10.195.8.29) ...
01:40:39Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
01:40:39Smith_Normal_Form: theory VectorSpace.LinearCombinations
01:40:39Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
01:40:40Hidden_Markov_Models: theory HOL-Library.State_Monad
01:40:40Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
01:40:40Running Cartan_FP (on 10.195.8.46) ...
01:40:40Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
01:40:40Running Monad_Normalisation (on 10.195.8.46) ...
01:40:40Gauss_Sums: theory HOL-Algebra.IntRing
01:40:40Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
01:40:40Running Buffons_Needle (on 10.195.8.46) ...
01:40:40Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
01:40:40Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
01:40:41HOL-ODE-Numerics: theory HOL-Library.RBT
01:40:41HOL-ODE-Numerics: theory Collections.RBT_add
01:40:41Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
01:40:41Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
01:40:41Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
01:40:41Error_Function: theory HOL-Library.Function_Algebras
01:40:41Error_Function: theory Error_Function.Error_Function
01:40:41Stochastic_Matrices: theory VectorSpace.SumSpaces
01:40:41Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
01:40:41HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
01:40:41Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
01:40:42Random_BSTs: theory HOL-Data_Structures.Cmp
01:40:42Random_BSTs: theory HOL-Data_Structures.Less_False
01:40:42Error_Function: theory Landau_Symbols.Group_Sort
01:40:42Stochastic_Matrices: theory VectorSpace.VectorSpace
01:40:42Fisher_Yates: theory Fisher_Yates.Fisher_Yates
01:40:42Random_BSTs: theory HOL-Data_Structures.Sorted_Less
01:40:42HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
01:40:42Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
01:40:42Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
01:40:42Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:40:42Random_BSTs: theory HOL-Data_Structures.Set_Specs
01:40:42HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
01:40:43Random_BSTs: theory HOL-Data_Structures.Tree_Set
01:40:43Cartan_FP: theory Cartan_FP.Cartan
01:40:43Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
01:40:43Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
01:40:43Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
01:40:43Buffons_Needle: theory Buffons_Needle.Buffons_Needle
01:40:43Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
01:40:43Timing Lp (2 threads, 45.541s elapsed time, 79.473s cpu time, 5.258s GC time, factor 1.75)
01:40:43Finished Lp (0:00:49 elapsed time, 0:01:22 cpu time, factor 1.69)
01:40:43Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
01:40:43Running Cotangent_PFD_Formula (on 10.195.8.30) ...
01:40:44Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
01:40:44Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
01:40:44Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
01:40:44Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
01:40:44Error_Function: theory Landau_Symbols.Landau_Real_Products
01:40:44Timing MFMC_Countable (2 threads, 145.761s elapsed time, 228.200s cpu time, 10.332s GC time, factor 1.57)
01:40:44Finished MFMC_Countable (0:02:29 elapsed time, 0:03:53 cpu time, factor 1.56)
01:40:44Random_BSTs: theory Random_BSTs.Random_BSTs
01:40:45Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
01:40:45Frequency_Moments: theory Finite_Fields.Ring_Characteristic
01:40:45Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
01:40:45Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
01:40:45Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
01:40:45Timing Monad_Normalisation (2 threads, 1.848s elapsed time, 2.819s cpu time, 0.127s GC time, factor 1.53)
01:40:45Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.12)
01:40:45Timing Density_Compiler (2 threads, 133.855s elapsed time, 246.948s cpu time, 9.466s GC time, factor 1.84)
01:40:45Finished Density_Compiler (0:02:18 elapsed time, 0:04:11 cpu time, factor 1.82)
01:40:46Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
01:40:46Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
01:40:46Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
01:40:46Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
01:40:46Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
01:40:46Cotangent_PFD_Formula: theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
01:40:46Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
01:40:46Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
01:40:47Timing Cartan_FP (2 threads, 3.373s elapsed time, 5.501s cpu time, 0.199s GC time, factor 1.63)
01:40:47Finished Cartan_FP (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.31)
01:40:47Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
01:40:47CryptHOL: theory CryptHOL.Generat
01:40:47Timing Fisher_Yates (2 threads, 4.705s elapsed time, 7.205s cpu time, 0.224s GC time, factor 1.53)
01:40:47Finished Fisher_Yates (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.26)
01:40:47Timing Executable_Randomized_Algorithms (6 threads, 163.842s elapsed time, 642.799s cpu time, 158.270s GC time, factor 3.92)
01:40:47CryptHOL: theory CryptHOL.List_Bits
01:40:47Finished Executable_Randomized_Algorithms (0:02:46 elapsed time, 0:10:49 cpu time, factor 3.89)
01:40:47Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
01:40:47CryptHOL: theory CryptHOL.Resumption
01:40:47Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
01:40:47Hidden_Markov_Models: theory Monad_Memo_DP.Memory
01:40:48Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
01:40:48Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
01:40:48Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
01:40:48Error_Function: theory Landau_Symbols.Landau_Simprocs
01:40:48Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
01:40:48Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
01:40:49Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
01:40:49HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
01:40:49Timing Turans_Graph_Theorem (2 threads, 149.696s elapsed time, 250.363s cpu time, 23.434s GC time, factor 1.67)
01:40:49Finished Turans_Graph_Theorem (0:02:34 elapsed time, 0:04:15 cpu time, factor 1.66)
01:40:49Error_Function: theory Landau_Symbols.Landau_More
01:40:50Probabilistic_Timed_Automata: theory Timed_Automata.DBM
01:40:50Error_Function: theory Error_Function.Error_Function_Asymptotics
01:40:50Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
01:40:50Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
01:40:50Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
01:40:50Timing Cotangent_PFD_Formula (2 threads, 3.668s elapsed time, 5.915s cpu time, 0.240s GC time, factor 1.61)
01:40:50Finished Cotangent_PFD_Formula (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.30)
01:40:51Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
01:40:52Timing Buffons_Needle (2 threads, 8.330s elapsed time, 14.086s cpu time, 0.313s GC time, factor 1.69)
01:40:52Finished Buffons_Needle (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.48)
01:40:52Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
01:40:52HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
01:40:52CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
01:40:52Probabilistic_Timed_Automata: theory Timed_Automata.Regions
01:40:54Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
01:40:54Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
01:40:54Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
01:40:54Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
01:40:55Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
01:40:55Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
01:40:55Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
01:40:56Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
01:40:56Frequency_Moments: theory Frequency_Moments.K_Smallest
01:40:56Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
01:40:57Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:40:57HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
01:40:57HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
01:40:57Frequency_Moments: theory Frequency_Moments.Probability_Ext
01:40:58Timing Girth_Chromatic (2 threads, 121.857s elapsed time, 199.666s cpu time, 14.500s GC time, factor 1.64)
01:40:58Finished Girth_Chromatic (0:02:42 elapsed time, 0:04:11 cpu time, factor 1.55)
01:40:58Timing Error_Function (2 threads, 15.863s elapsed time, 28.496s cpu time, 1.837s GC time, factor 1.80)
01:40:58Finished Error_Function (0:00:18 elapsed time, 0:00:31 cpu time, factor 1.67)
01:40:58Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
01:40:58Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
01:40:58Frequency_Moments: theory Frequency_Moments.Frequency_Moments
01:40:58Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
01:40:59Probabilistic_Timed_Automata: theory Timed_Automata.Closure
01:41:00Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
01:41:00Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
01:41:00HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
01:41:00Timing SDS_Impossibility (2 threads, 69.454s elapsed time, 87.499s cpu time, 4.515s GC time, factor 1.26)
01:41:00Finished SDS_Impossibility (0:01:13 elapsed time, 0:01:31 cpu time, factor 1.24)
01:41:00Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
01:41:00Gauss_Sums: theory Gauss_Sums.Gauss_Sums
01:41:01Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
01:41:01Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
01:41:01Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
01:41:01Timing List_Update (2 threads, 167.559s elapsed time, 278.939s cpu time, 21.541s GC time, factor 1.66)
01:41:01Finished List_Update (0:02:52 elapsed time, 0:04:44 cpu time, factor 1.65)
01:41:02Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
01:41:02Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
01:41:03Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
01:41:03Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
01:41:03Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
01:41:03HOL-ODE-Numerics: theory Affine_Arithmetic.Print
01:41:03HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
01:41:03HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
01:41:03HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
01:41:05Timing Probabilistic_System_Zoo (2 threads, 70.701s elapsed time, 128.209s cpu time, 16.716s GC time, factor 1.81)
01:41:05Finished Probabilistic_System_Zoo (0:01:14 elapsed time, 0:02:13 cpu time, factor 1.77)
01:41:06Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
01:41:07Timing Zeta_Function (6 threads, 24.476s elapsed time, 101.945s cpu time, 8.820s GC time, factor 4.17)
01:41:07Finished Zeta_Function (0:00:38 elapsed time, 0:02:03 cpu time, factor 3.25)
01:41:07Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
01:41:09Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
01:41:10HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
01:41:10HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
01:41:10HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
01:41:11HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
01:41:12Building Algebraic_Numbers (on of4.proof.cit.tum.de) ...
01:41:14CryptHOL: theory CryptHOL.Computational_Model
01:41:14CryptHOL: theory CryptHOL.GPV_Applicative
01:41:16Algebraic_Numbers: theory Pure-ex.Guess
01:41:16Algebraic_Numbers: theory Deriving.Compare_Rat
01:41:16Algebraic_Numbers: theory Deriving.Compare_Real
01:41:16Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
01:41:16Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:41:16Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
01:41:16Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
01:41:17Algebraic_Numbers: theory Show.Show_Real
01:41:17Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
01:41:17Algebraic_Numbers: theory Show.Show_Complex
01:41:17Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
01:41:17Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
01:41:17CryptHOL: theory CryptHOL.GPV_Expectation
01:41:18Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
01:41:18Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
01:41:18Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
01:41:18Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
01:41:18Algebraic_Numbers: theory Algebraic_Numbers.Resultant
01:41:18Building LLL_Basis_Reduction (on 10.195.8.49) ...
01:41:18CryptHOL: theory CryptHOL.GPV_Bisim
01:41:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
01:41:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
01:41:18Timing Random_BSTs (2 threads, 10.292s elapsed time, 14.541s cpu time, 1.181s GC time, factor 1.41)
01:41:18HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
01:41:18Finished Random_BSTs (0:00:36 elapsed time, 0:00:45 cpu time, factor 1.25)
01:41:19Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
01:41:19HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
01:41:19CryptHOL: theory CryptHOL.CryptHOL
01:41:20Timing Complex_Bounded_Operators_Dependencies (6 threads, 298.943s elapsed time, 1110.608s cpu time, 396.719s GC time, factor 3.72)
01:41:20Finished Complex_Bounded_Operators_Dependencies (0:05:31 elapsed time, 0:19:29 cpu time, factor 3.53)
01:41:21Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
01:41:21Running Fishers_Inequality (on of2.proof.cit.tum.de) ...
01:41:21Running CVP_Hardness (on of2.proof.cit.tum.de) ...
01:41:21Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
01:41:22Fishers_Inequality: theory Card_Partitions.Set_Partition
01:41:23CVP_Hardness: theory CVP_Hardness.Reduction
01:41:23Fishers_Inequality: theory Polynomials.MPoly_Type
01:41:23CVP_Hardness: theory CVP_Hardness.Digits_int
01:41:23CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
01:41:23Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
01:41:23Fishers_Inequality: theory Polynomials.More_Modules
01:41:23CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
01:41:23Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
01:41:23CVP_Hardness: theory CVP_Hardness.Partition
01:41:23Fishers_Inequality: theory List-Index.List_Index
01:41:23HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
01:41:23CVP_Hardness: theory CVP_Hardness.Subset_Sum
01:41:23Fishers_Inequality: theory Open_Induction.Restricted_Predicates
01:41:23HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
01:41:23Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
01:41:23Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
01:41:23Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
01:41:23Fishers_Inequality: theory Polynomials.More_MPoly_Type
01:41:24Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
01:41:24Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
01:41:24Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
01:41:24Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
01:41:24Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
01:41:24Fishers_Inequality: theory Design_Theory.Multisets_Extras
01:41:24HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
01:41:24CVP_Hardness: theory Algebraic_Numbers.Resultant
01:41:24Fishers_Inequality: theory Design_Theory.Design_Basics
01:41:24Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
01:41:24Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:41:24Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
01:41:25LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
01:41:25LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
01:41:25CVP_Hardness: theory CVP_Hardness.Lattice_int
01:41:25LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
01:41:25LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
01:41:25Fishers_Inequality: theory Polynomials.Utils
01:41:25Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
01:41:25Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
01:41:25Fishers_Inequality: theory Design_Theory.Design_Operations
01:41:25Fishers_Inequality: theory Groebner_Bases.General
01:41:25Fishers_Inequality: theory Polynomials.Power_Products
01:41:25Timing Hidden_Markov_Models (2 threads, 45.698s elapsed time, 86.377s cpu time, 8.035s GC time, factor 1.89)
01:41:25Finished Hidden_Markov_Models (0:00:49 elapsed time, 0:01:30 cpu time, factor 1.82)
01:41:25CVP_Hardness: theory CVP_Hardness.CVP_p
01:41:25CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
01:41:26Smith_Normal_Form: theory VectorSpace.SumSpaces
01:41:26Fishers_Inequality: theory Design_Theory.Block_Designs
01:41:26Fishers_Inequality: theory Design_Theory.Sub_Designs
01:41:26Smith_Normal_Form: theory VectorSpace.VectorSpace
01:41:27Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
01:41:27Timing Fourier (2 threads, 91.762s elapsed time, 145.818s cpu time, 6.328s GC time, factor 1.59)
01:41:27Finished Fourier (0:01:35 elapsed time, 0:02:29 cpu time, factor 1.56)
01:41:27LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
01:41:28HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
01:41:28HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
01:41:28HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
01:41:28Running CRYSTALS-Kyber (on 10.195.7.194) ...
01:41:28Fishers_Inequality: theory Design_Theory.BIBD
01:41:29Timing Differential_Dynamic_Logic (6 threads, 149.191s elapsed time, 371.432s cpu time, 94.998s GC time, factor 2.49)
01:41:29Finished Differential_Dynamic_Logic (0:02:31 elapsed time, 0:06:16 cpu time, factor 2.48)
01:41:29Fishers_Inequality: theory Fishers_Inequality.Design_Extras
01:41:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
01:41:30Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
01:41:30Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
01:41:30MDP-Algorithms: theory Containers.RBT_Mapping2
01:41:30Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
01:41:30Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
01:41:30LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
01:41:30Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
01:41:31MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
01:41:31MDP-Algorithms: theory Containers.RBT_Set2
01:41:32MDP-Algorithms: theory Containers.Set_Impl
01:41:32Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
01:41:32MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
01:41:33CVP_Hardness: theory LLL_Basis_Reduction.Norms
01:41:33CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes
01:41:33CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp
01:41:34CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product
01:41:34Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
01:41:34CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm
01:41:34CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector
01:41:34Running Linear_Recurrences_Solver (on 10.195.6.179) ...
01:41:35Timing Ergodic_Theory (2 threads, 142.743s elapsed time, 240.566s cpu time, 8.879s GC time, factor 1.69)
01:41:35Finished Ergodic_Theory (0:02:57 elapsed time, 0:04:43 cpu time, factor 1.60)
01:41:35Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
01:41:35CRYSTALS-Kyber: theory HOL-Number_Theory.Fib
01:41:36Fishers_Inequality: theory Polynomials.MPoly_Type_Class
01:41:36Timing Projective_Measurements (6 threads, 183.226s elapsed time, 652.990s cpu time, 113.235s GC time, factor 3.56)
01:41:36Finished Projective_Measurements (0:03:32 elapsed time, 0:11:44 cpu time, factor 3.31)
01:41:36CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers
01:41:36CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space
01:41:36Running Stern_Brocot (on 10.195.8.11) ...
01:41:37Running Random_Graph_Subgraph_Threshold (on 10.195.8.11) ...
01:41:37Running Szemeredi_Regularity (on 10.195.8.11) ...
01:41:37CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion
01:41:37CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss
01:41:38Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
01:41:38CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity
01:41:38Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
01:41:39CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington
01:41:39Stern_Brocot: theory Stern_Brocot.Cotree
01:41:40CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots
01:41:40Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
01:41:40Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
01:41:40CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product
01:41:40CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory
01:41:41Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:41:41HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
01:41:42CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec
01:41:42Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
01:41:42CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral
01:41:43Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
01:41:43Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
01:41:43LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
01:41:43CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas
01:41:44Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
01:41:44Linear_Recurrences_Solver: theory Pure-ex.Guess
01:41:44Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
01:41:44Timing Roth_Arithmetic_Progressions (2 threads, 191.231s elapsed time, 339.120s cpu time, 26.416s GC time, factor 1.77)
01:41:44Finished Roth_Arithmetic_Progressions (0:03:16 elapsed time, 0:05:45 cpu time, factor 1.76)
01:41:44Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
01:41:44CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT
01:41:44CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus
01:41:45Linear_Recurrences_Solver: theory Deriving.Compare_Rat
01:41:45CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr
01:41:45CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress
01:41:45Linear_Recurrences_Solver: theory Deriving.Compare_Real
01:41:45Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
01:41:45Linear_Recurrences_Solver: theory Polynomials.More_Modules
01:41:46Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
01:41:46Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
01:41:46Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
01:41:46Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
01:41:47CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme
01:41:47Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
01:41:47MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
01:41:47CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values
01:41:47Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
01:41:47Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
01:41:48CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme
01:41:48CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844
01:41:48Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
01:41:48Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
01:41:48Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
01:41:49Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
01:41:49Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
01:41:49CVP_Hardness: theory CVP_Hardness.infnorm
01:41:49CVP_Hardness: theory CVP_Hardness.CVP_vec
01:41:49CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
01:41:49MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
01:41:49Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
01:41:49Timing Szemeredi_Regularity (2 threads, 9.150s elapsed time, 13.750s cpu time, 0.460s GC time, factor 1.50)
01:41:49Finished Szemeredi_Regularity (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.36)
01:41:50CVP_Hardness: theory CVP_Hardness.BHLE
01:41:50CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT
01:41:50CVP_Hardness: theory CVP_Hardness.SVP_vec
01:41:50CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values
01:41:50Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
01:41:51MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
01:41:52Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
01:41:52Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
01:41:52Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
01:41:52Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
01:41:52Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
01:41:53MDP-Algorithms: theory MDP-Algorithms.PI_Code
01:41:53Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
01:41:53Timing Random_Graph_Subgraph_Threshold (2 threads, 12.645s elapsed time, 21.434s cpu time, 0.721s GC time, factor 1.70)
01:41:53Finished Random_Graph_Subgraph_Threshold (0:00:15 elapsed time, 0:00:24 cpu time, factor 1.55)
01:41:53Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:41:53Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
01:41:53Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
01:41:54Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
01:41:54Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:41:54Building Complex_Bounded_Operators (on 10.195.8.42) ...
01:41:54Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
01:41:54Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
01:41:55Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
01:41:55Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
01:41:55Timing E_Transcendental (2 threads, 176.467s elapsed time, 301.032s cpu time, 42.707s GC time, factor 1.71)
01:41:55Finished E_Transcendental (0:03:45 elapsed time, 0:06:04 cpu time, factor 1.62)
01:41:55Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
01:41:55Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
01:41:56Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
01:41:56Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
01:41:57Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
01:41:57Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
01:41:57Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
01:41:58Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
01:41:58Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
01:41:58Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
01:41:59Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:41:59Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
01:41:59Timing Padic_Field (2 threads, 1176.994s elapsed time, 2293.797s cpu time, 1012.869s GC time, factor 1.95)
01:41:59Finished Padic_Field (0:19:45 elapsed time, 0:38:28 cpu time, factor 1.95)
01:42:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
01:42:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
01:42:00Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
01:42:01Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
01:42:01Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
01:42:01Timing Fishers_Inequality (6 threads, 37.931s elapsed time, 195.067s cpu time, 20.156s GC time, factor 5.14)
01:42:01Finished Fishers_Inequality (0:00:40 elapsed time, 0:03:18 cpu time, factor 4.94)
01:42:02Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
01:42:02Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
01:42:03Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
01:42:03Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
01:42:03Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
01:42:03Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
01:42:03Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
01:42:04Building Pi_Transcendental (on of4.proof.cit.tum.de) ...
01:42:04Running Dirichlet_L (on of4.proof.cit.tum.de) ...
01:42:05Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
01:42:05Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
01:42:05Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
01:42:05Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:42:05Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
01:42:05Pi_Transcendental: theory HOL-Library.Fun_Lexorder
01:42:05Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
01:42:05Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:42:06Pi_Transcendental: theory HOL-Library.Poly_Mapping
01:42:06Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
01:42:06Dirichlet_L: theory HOL-Library.Lattice_Algebras
01:42:06Dirichlet_L: theory HOL-Library.Log_Nat
01:42:06Dirichlet_L: theory Lehmer.Lehmer
01:42:06Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
01:42:06Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
01:42:06Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
01:42:06Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
01:42:06Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
01:42:07Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
01:42:07Linear_Recurrences_Solver: theory Show.Show_Real
01:42:07Pi_Transcendental: theory Polynomials.MPoly_Type
01:42:07Timing CVP_Hardness (6 threads, 44.060s elapsed time, 180.556s cpu time, 11.668s GC time, factor 4.10)
01:42:07Finished CVP_Hardness (0:00:46 elapsed time, 0:03:03 cpu time, factor 3.97)
01:42:07Linear_Recurrences_Solver: theory Show.Show_Complex
01:42:07Pi_Transcendental: theory Polynomials.More_MPoly_Type
01:42:08Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
01:42:08Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
01:42:08Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
01:42:08Building Prime_Number_Theorem (on of2.proof.cit.tum.de) ...
01:42:08Building Prime_Distribution_Elementary (on of2.proof.cit.tum.de) ...
01:42:08Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
01:42:08Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
01:42:08Pi_Transcendental: theory Symmetric_Polynomials.Vieta
01:42:08Timing Gauss_Sums (2 threads, 91.862s elapsed time, 155.880s cpu time, 12.826s GC time, factor 1.70)
01:42:08Finished Gauss_Sums (0:01:36 elapsed time, 0:02:40 cpu time, factor 1.67)
01:42:09Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
01:42:09Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
01:42:09Dirichlet_L: theory HOL-Library.Interval
01:42:09Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
01:42:09Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:42:09Dirichlet_L: theory HOL-Library.Float
01:42:09Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
01:42:09Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
01:42:10Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
01:42:10Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
01:42:10Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
01:42:10Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
01:42:10MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
01:42:10MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
01:42:10Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
01:42:10Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
01:42:11Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
01:42:11Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
01:42:11Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
01:42:11Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
01:42:11Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
01:42:11Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
01:42:11Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
01:42:11Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
01:42:11Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
01:42:12Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
01:42:12Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
01:42:12Dirichlet_L: theory HOL-Library.Interval_Float
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
01:42:12Building Commuting_Hermitian (on 10.195.8.32) ...
01:42:12Linear_Recurrences_Solver: theory Polynomials.Utils
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
01:42:12Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
01:42:13Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
01:42:13Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
01:42:13Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
01:42:13Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
01:42:13Linear_Recurrences_Solver: theory Polynomials.Power_Products
01:42:14Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
01:42:14LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
01:42:14LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
01:42:14Running Randomised_BSTs (on 10.195.7.194) ...
01:42:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
01:42:16Running Laws_of_Large_Numbers (on 10.195.7.194) ...
01:42:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
01:42:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
01:42:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
01:42:17Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
01:42:17Dirichlet_L: theory Bertrands_Postulate.Bertrand
01:42:18Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
01:42:19Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
01:42:19Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
01:42:19Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
01:42:19Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
01:42:20Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
01:42:20Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
01:42:20Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
01:42:20Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
01:42:20Stern_Brocot: theory Stern_Brocot.Bird_Tree
01:42:21Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
01:42:22Timing Laws_of_Large_Numbers (2 threads, 2.447s elapsed time, 3.729s cpu time, 0.177s GC time, factor 1.52)
01:42:22Finished Laws_of_Large_Numbers (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.15)
01:42:22Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
01:42:22Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
01:42:23Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
01:42:23Timing Stern_Brocot (2 threads, 41.669s elapsed time, 68.953s cpu time, 8.372s GC time, factor 1.65)
01:42:23Finished Stern_Brocot (0:00:45 elapsed time, 0:01:13 cpu time, factor 1.61)
01:42:24Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
01:42:25Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
01:42:25Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
01:42:25Timing S_Finite_Measure_Monad (2 threads, 228.503s elapsed time, 367.588s cpu time, 18.861s GC time, factor 1.61)
01:42:25Finished S_Finite_Measure_Monad (0:03:52 elapsed time, 0:06:12 cpu time, factor 1.60)
01:42:25Timing Count_Complex_Roots (2 threads, 217.245s elapsed time, 376.043s cpu time, 59.828s GC time, factor 1.73)
01:42:26Finished Count_Complex_Roots (0:04:13 elapsed time, 0:07:00 cpu time, factor 1.66)
01:42:26Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
01:42:26Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
01:42:26Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
01:42:27Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
01:42:28Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
01:42:28Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
01:42:28Timing Bernoulli (2 threads, 210.650s elapsed time, 349.063s cpu time, 34.427s GC time, factor 1.66)
01:42:28Finished Bernoulli (0:04:11 elapsed time, 0:06:43 cpu time, factor 1.60)
01:42:28HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
01:42:29Timing Prime_Number_Theorem (6 threads, 8.845s elapsed time, 40.173s cpu time, 2.373s GC time, factor 4.54)
01:42:29Finished Prime_Number_Theorem (0:00:19 elapsed time, 0:00:55 cpu time, factor 2.84)
01:42:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
01:42:29Timing Probabilistic_Noninterference (2 threads, 233.363s elapsed time, 372.362s cpu time, 32.278s GC time, factor 1.60)
01:42:29Finished Probabilistic_Noninterference (0:03:57 elapsed time, 0:06:17 cpu time, factor 1.59)
01:42:30Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
01:42:31Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
01:42:31Dirichlet_L: theory HOL-Algebra.QuotRing
01:42:31Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
01:42:31Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
01:42:31Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
01:42:32Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
01:42:32Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
01:42:33Dirichlet_L: theory HOL-Algebra.IntRing
01:42:33Timing Pi_Transcendental (6 threads, 12.170s elapsed time, 54.746s cpu time, 4.487s GC time, factor 4.50)
01:42:33Finished Pi_Transcendental (0:00:27 elapsed time, 0:01:17 cpu time, factor 2.76)
01:42:33Timing Stochastic_Matrices (6 threads, 127.181s elapsed time, 486.085s cpu time, 129.863s GC time, factor 3.82)
01:42:33Finished Stochastic_Matrices (0:02:09 elapsed time, 0:08:12 cpu time, factor 3.79)
01:42:33Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
01:42:33Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
01:42:34HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
01:42:34Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
01:42:34Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
01:42:34Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
01:42:34Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
01:42:34Timing Prime_Distribution_Elementary (6 threads, 11.725s elapsed time, 59.423s cpu time, 3.559s GC time, factor 5.07)
01:42:34Finished Prime_Distribution_Elementary (0:00:25 elapsed time, 0:01:19 cpu time, factor 3.19)
01:42:34Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
01:42:35Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
01:42:35Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
01:42:35Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
01:42:35Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
01:42:35Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
01:42:35Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
01:42:35Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
01:42:36Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
01:42:36Timing Randomised_BSTs (2 threads, 16.770s elapsed time, 30.869s cpu time, 1.933s GC time, factor 1.84)
01:42:36Finished Randomised_BSTs (0:00:20 elapsed time, 0:00:34 cpu time, factor 1.69)
01:42:36Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
01:42:36Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
01:42:36Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
01:42:36Timing Algebraic_Numbers (6 threads, 59.714s elapsed time, 262.065s cpu time, 22.870s GC time, factor 4.39)
01:42:36Finished Algebraic_Numbers (0:01:23 elapsed time, 0:05:00 cpu time, factor 3.58)
01:42:37Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
01:42:37Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
01:42:38Running Linear_Recurrences (on of2.proof.cit.tum.de) ...
01:42:39Building Stirling_Formula (on of2.proof.cit.tum.de) ...
01:42:39Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
01:42:39Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
01:42:40Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
01:42:40Stirling_Formula: theory HOL-Library.Function_Algebras
01:42:40Linear_Recurrences: theory HOL-Combinatorics.Stirling
01:42:40Stirling_Formula: theory Landau_Symbols.Group_Sort
01:42:40Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers
01:42:40Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree
01:42:40Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure
01:42:40Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat
01:42:40Linear_Recurrences: theory HOL-Library.Code_Target_Int
01:42:40Linear_Recurrences: theory HOL-Library.Code_Target_Nat
01:42:40Linear_Recurrences: theory HOL-Library.Sublist
01:42:40Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial
01:42:40Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Irreducibility
01:42:40Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
01:42:40Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials
01:42:41Linear_Recurrences: theory Matrix.Utility
01:42:41Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:42:41Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
01:42:41Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
01:42:41Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
01:42:41Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
01:42:41Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
01:42:41Running Lambert_W (on 10.195.8.32) ...
01:42:41Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
01:42:41Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
01:42:41Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
01:42:42Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
01:42:42Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
01:42:42Linear_Recurrences: theory Linear_Recurrences.RatFPS
01:42:42Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
01:42:42Linear_Recurrences: theory Linear_Recurrences.Factorizations
01:42:42Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
01:42:43Timing Three_Squares (6 threads, 240.889s elapsed time, 856.204s cpu time, 193.311s GC time, factor 3.55)
01:42:43Finished Three_Squares (0:04:49 elapsed time, 0:15:38 cpu time, factor 3.25)
01:42:43Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
01:42:43Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
01:42:43Stirling_Formula: theory Landau_Symbols.Landau_More
01:42:43Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
01:42:43Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
01:42:44Stirling_Formula: theory Stirling_Formula.Stirling_Formula
01:42:44Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
01:42:44Timing Dirichlet_L (6 threads, 36.685s elapsed time, 170.452s cpu time, 19.642s GC time, factor 4.65)
01:42:44Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
01:42:44Finished Dirichlet_L (0:00:38 elapsed time, 0:02:53 cpu time, factor 4.48)
01:42:44Lambert_W: theory HOL-Library.Function_Algebras
01:42:44Lambert_W: theory Lambert_W.Lambert_W
01:42:44Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
01:42:45Lambert_W: theory Landau_Symbols.Group_Sort
01:42:45Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
01:42:45Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
01:42:45HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
01:42:45Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
01:42:45Running Euler_MacLaurin (on 10.195.7.194) ...
01:42:46Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
01:42:46Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
01:42:47Lambert_W: theory Landau_Symbols.Landau_Real_Products
01:42:49Euler_MacLaurin: theory HOL-Library.Function_Algebras
01:42:49Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
01:42:49Euler_MacLaurin: theory Landau_Symbols.Group_Sort
01:42:51Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
01:42:51Lambert_W: theory Landau_Symbols.Landau_Simprocs
01:42:53Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
01:42:53Lambert_W: theory Landau_Symbols.Landau_More
01:42:53Lambert_W: theory Stirling_Formula.Stirling_Formula
01:42:54Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
01:42:55Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series
01:42:55LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
01:42:55Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
01:42:55Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
01:42:55Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
01:42:55LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
01:42:56Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
01:42:57Timing Stirling_Formula (6 threads, 7.290s elapsed time, 25.041s cpu time, 1.571s GC time, factor 3.43)
01:42:57Finished Stirling_Formula (0:00:17 elapsed time, 0:00:39 cpu time, factor 2.27)
01:42:58Euler_MacLaurin: theory Landau_Symbols.Landau_More
01:42:58Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
01:42:58Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
01:42:59Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
01:43:01Timing Linear_Recurrences (6 threads, 20.894s elapsed time, 65.383s cpu time, 3.888s GC time, factor 3.13)
01:43:01Finished Linear_Recurrences (0:00:22 elapsed time, 0:01:07 cpu time, factor 2.99)
01:43:02Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
01:43:02Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
01:43:03Timing Balog_Szemeredi_Gowers (2 threads, 288.248s elapsed time, 507.460s cpu time, 46.400s GC time, factor 1.76)
01:43:03Finished Balog_Szemeredi_Gowers (0:04:53 elapsed time, 0:08:34 cpu time, factor 1.75)
01:43:05Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
01:43:05Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
01:43:06Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
01:43:07Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
01:43:07Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
01:43:10Running Quantifier_Elimination_Hybrid (on of3.proof.cit.tum.de) ...
01:43:11Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
01:43:11Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
01:43:12Timing Lambert_W (2 threads, 26.707s elapsed time, 45.275s cpu time, 2.700s GC time, factor 1.70)
01:43:12Finished Lambert_W (0:00:30 elapsed time, 0:00:48 cpu time, factor 1.60)
01:43:12Timing Cook_Levin (6 threads, 451.644s elapsed time, 1683.328s cpu time, 62.011s GC time, factor 3.73)
01:43:12Finished Cook_Levin (0:07:34 elapsed time, 0:28:11 cpu time, factor 3.72)
01:43:13Running Hermite_Lindemann (on of4.proof.cit.tum.de) ...
01:43:13Running BenOr_Kozen_Reif (on of4.proof.cit.tum.de) ...
01:43:13Running Factor_Algebraic_Polynomial (on of4.proof.cit.tum.de) ...
01:43:13HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
01:43:14Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux
01:43:14Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type
01:43:14Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules
01:43:14Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots
01:43:14Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta
01:43:14Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc
01:43:14Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
01:43:14Timing Euler_MacLaurin (2 threads, 24.661s elapsed time, 45.734s cpu time, 2.802s GC time, factor 1.85)
01:43:14Finished Euler_MacLaurin (0:00:28 elapsed time, 0:00:49 cpu time, factor 1.74)
01:43:14Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates
01:43:14Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator
01:43:14Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski
01:43:14Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials
01:43:14Running Polygonal_Number_Theorem (on of4.proof.cit.tum.de) ...
01:43:14Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix
01:43:15Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
01:43:15Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences
01:43:15Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
01:43:15Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type
01:43:15Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum
01:43:15Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
01:43:15Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
01:43:15Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements
01:43:15Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
01:43:15BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc
01:43:15Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
01:43:15Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
01:43:15BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix
01:43:15Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
01:43:15Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
01:43:15Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
01:43:15Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
01:43:15Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:43:15Hermite_Lindemann: theory HOL-Library.Monad_Syntax
01:43:15Hermite_Lindemann: theory HOL-Algebra.Divisibility
01:43:15Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
01:43:15Hermite_Lindemann: theory Containers.Containers_Auxiliary
01:43:15Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
01:43:15BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski
01:43:15Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full
01:43:15Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map
01:43:15Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate
01:43:15Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
01:43:15Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
01:43:15Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
01:43:15Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
01:43:15Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
01:43:16Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials
01:43:16Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence
01:43:16Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
01:43:16Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
01:43:16Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
01:43:16Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
01:43:16Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:43:16Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
01:43:16Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
01:43:16Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
01:43:16Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
01:43:17Running Clique_and_Monotone_Circuits (on of2.proof.cit.tum.de) ...
01:43:17Running Zeta_3_Irrational (on of2.proof.cit.tum.de) ...
01:43:17Running Irrational_Series_Erdos_Straus (on of2.proof.cit.tum.de) ...
01:43:17Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations
01:43:17Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
01:43:17Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:43:17Hermite_Lindemann: theory Matrix.Utility
01:43:17Quantifier_Elimination_Hybrid: theory Polynomials.Utils
01:43:18Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
01:43:18BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm
01:43:18Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders
01:43:18Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
01:43:18Factor_Algebraic_Polynomial: theory Polynomials.Utils
01:43:18Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
01:43:18Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products
01:43:18Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm
01:43:18Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
01:43:18Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
01:43:18Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
01:43:18Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
01:43:18Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
01:43:18Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
01:43:18Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
01:43:18Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
01:43:18Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
01:43:18Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
01:43:18Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:43:19Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
01:43:19Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
01:43:19Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
01:43:19Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:43:19Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
01:43:19Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
01:43:19Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
01:43:19Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
01:43:19Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
01:43:19Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm
01:43:19BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
01:43:19Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
01:43:19Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
01:43:19Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
01:43:19Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
01:43:20Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
01:43:20Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
01:43:20Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:43:20BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm
01:43:20Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
01:43:20Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
01:43:20Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs
01:43:20Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
01:43:20Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials
01:43:20Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
01:43:20Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:43:20Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:43:20BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs
01:43:20Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
01:43:20LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
01:43:21Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:43:21Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs
01:43:21Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
01:43:21Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision
01:43:21Running Cubic_Quartic_Equations (on 10.195.7.194) ...
01:43:21Running Comparison_Sort_Lower_Bound (on 10.195.7.194) ...
01:43:22BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs
01:43:22BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision
01:43:22LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
01:43:22Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:43:22Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
01:43:23Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
01:43:23Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
01:43:24Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
01:43:24Running IMO2019 (on 10.195.6.179) ...
01:43:24Comparison_Sort_Lower_Bound: theory List-Index.List_Index
01:43:25Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
01:43:25Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:43:25Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision
01:43:25Running Irrationals_From_THEBOOK (on 10.195.6.179) ...
01:43:27Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
01:43:27Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
01:43:27Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
01:43:27Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
01:43:27Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
01:43:28Timing Irrational_Series_Erdos_Straus (6 threads, 7.912s elapsed time, 31.844s cpu time, 0.842s GC time, factor 4.02)
01:43:28Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
01:43:28Finished Irrational_Series_Erdos_Straus (0:00:09 elapsed time, 0:00:33 cpu time, factor 3.46)
01:43:28Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
01:43:28Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
01:43:28BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision
01:43:28Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
01:43:28Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified
01:43:29Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
01:43:29Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
01:43:29Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
01:43:29Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
01:43:30Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
01:43:30Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class
01:43:30Timing Hybrid_Systems_VCs (2 threads, 455.817s elapsed time, 717.783s cpu time, 51.023s GC time, factor 1.57)
01:43:30Finished Hybrid_Systems_VCs (0:07:41 elapsed time, 0:12:04 cpu time, factor 1.57)
01:43:30IMO2019: theory IMO2019.IMO2019_Q5
01:43:30IMO2019: theory IMO2019.IMO2019_Q1
01:43:30Timing Zeta_3_Irrational (6 threads, 10.497s elapsed time, 53.074s cpu time, 2.600s GC time, factor 5.06)
01:43:30Finished Zeta_3_Irrational (0:00:12 elapsed time, 0:00:54 cpu time, factor 4.48)
01:43:30IMO2019: theory IMO2019.IMO2019_Q4
01:43:31Timing Shadow_SC_DOM (2 threads, 1558.325s elapsed time, 2667.977s cpu time, 374.245s GC time, factor 1.71)
01:43:31Finished Shadow_SC_DOM (0:28:20 elapsed time, 0:47:30 cpu time, factor 1.68)
01:43:32Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:43:32Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection
01:43:33Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered
01:43:33Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
01:43:34Timing Clique_and_Monotone_Circuits (6 threads, 14.265s elapsed time, 37.635s cpu time, 1.256s GC time, factor 2.64)
01:43:34Finished Clique_and_Monotone_Circuits (0:00:16 elapsed time, 0:00:39 cpu time, factor 2.46)
01:43:34Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
01:43:34Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
01:43:35Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
01:43:35Timing Irrationals_From_THEBOOK (2 threads, 4.542s elapsed time, 6.532s cpu time, 0.175s GC time, factor 1.44)
01:43:35Finished Irrationals_From_THEBOOK (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.22)
01:43:35Timing Comparison_Sort_Lower_Bound (2 threads, 9.057s elapsed time, 17.268s cpu time, 1.421s GC time, factor 1.91)
01:43:35Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.67)
01:43:36Hermite_Lindemann: theory Subresultants.More_Homomorphisms
01:43:36Hermite_Lindemann: theory Subresultants.Resultant_Prelim
01:43:37Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
01:43:37Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
01:43:37Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
01:43:38Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
01:43:39Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
01:43:40Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:43:40Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
01:43:40Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
01:43:41Timing IMO2019 (2 threads, 10.932s elapsed time, 13.818s cpu time, 0.680s GC time, factor 1.26)
01:43:41Finished IMO2019 (0:00:14 elapsed time, 0:00:17 cpu time, factor 1.17)
01:43:42Hermite_Lindemann: theory Algebraic_Numbers.Resultant
01:43:42Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
01:43:42Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap
01:43:43LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
01:43:43Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension
01:43:43Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
01:43:43Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps
01:43:44Running SC_DOM_Components (on 10.195.8.40) ...
01:43:44Timing Commuting_Hermitian (2 threads, 53.008s elapsed time, 91.543s cpu time, 6.812s GC time, factor 1.73)
01:43:44Finished Commuting_Hermitian (0:01:28 elapsed time, 0:02:15 cpu time, factor 1.53)
01:43:44Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms
01:43:44Timing Polygonal_Number_Theorem (6 threads, 26.440s elapsed time, 88.595s cpu time, 4.227s GC time, factor 3.35)
01:43:44Finished Polygonal_Number_Theorem (0:00:28 elapsed time, 0:01:31 cpu time, factor 3.15)
01:43:45Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
01:43:45Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
01:43:45Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
01:43:45LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
01:43:45Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
01:43:46Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
01:43:46Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn
01:43:47Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations
01:43:48Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
01:43:50Timing Cubic_Quartic_Equations (2 threads, 23.436s elapsed time, 44.009s cpu time, 3.605s GC time, factor 1.88)
01:43:50Finished Cubic_Quartic_Equations (0:00:27 elapsed time, 0:00:48 cpu time, factor 1.75)
01:43:50Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs
01:43:50Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
01:43:50Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex
01:43:50Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms
01:43:51Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
01:43:52Running TsirelsonBound (on 10.195.8.42) ...
01:43:53Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
01:43:53Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos
01:43:54SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
01:43:54LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
01:43:55Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
01:43:55Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
01:43:56TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
01:43:57Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
01:43:57Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
01:43:57Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF
01:43:57Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE
01:43:58Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable
01:43:59Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals
01:43:59Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind
01:43:59Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS
01:43:59TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
01:44:00TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
01:44:01Timing Factor_Algebraic_Polynomial (6 threads, 44.476s elapsed time, 127.309s cpu time, 11.292s GC time, factor 2.86)
01:44:01Finished Factor_Algebraic_Polynomial (0:00:46 elapsed time, 0:02:10 cpu time, factor 2.79)
01:44:01TsirelsonBound: theory TsirelsonBound.Tsirelson
01:44:01Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports
01:44:02Timing Schwartz_Zippel (2 threads, 336.816s elapsed time, 593.677s cpu time, 136.361s GC time, factor 1.76)
01:44:02Finished Schwartz_Zippel (0:05:41 elapsed time, 0:10:00 cpu time, factor 1.76)
01:44:03Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni
01:44:03Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni
01:44:04Timing CRYSTALS-Kyber (2 threads, 149.918s elapsed time, 241.519s cpu time, 15.348s GC time, factor 1.61)
01:44:04Finished CRYSTALS-Kyber (0:02:34 elapsed time, 0:04:06 cpu time, factor 1.59)
01:44:04Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni
01:44:05Timing BenOr_Kozen_Reif (6 threads, 48.941s elapsed time, 175.500s cpu time, 10.076s GC time, factor 3.59)
01:44:05Finished BenOr_Kozen_Reif (0:00:51 elapsed time, 0:02:58 cpu time, factor 3.49)
01:44:05Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs
01:44:06Timing Hermite_Lindemann (6 threads, 50.480s elapsed time, 211.878s cpu time, 20.213s GC time, factor 4.20)
01:44:06Finished Hermite_Lindemann (0:00:52 elapsed time, 0:03:35 cpu time, factor 4.11)
01:44:06Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad
01:44:07Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props
01:44:07Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs
01:44:08Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs
01:44:10Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments
01:44:10Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence
01:44:11Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
01:44:13SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
01:44:15Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
01:44:15Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
01:44:28SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
01:44:30Timing CryptHOL (2 threads, 224.936s elapsed time, 409.695s cpu time, 40.529s GC time, factor 1.82)
01:44:31Finished CryptHOL (0:04:39 elapsed time, 0:08:02 cpu time, factor 1.73)
01:44:44Building Game_Based_Crypto (on of4.proof.cit.tum.de) ...
01:44:45Building Constructive_Cryptography (on of4.proof.cit.tum.de) ...
01:44:45Running Sigma_Commit_Crypto (on of4.proof.cit.tum.de) ...
01:44:45Running ABY3_Protocols (on of4.proof.cit.tum.de) ...
01:44:46Constructive_Cryptography: theory Constructive_Cryptography.Resource
01:44:46ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
01:44:46ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
01:44:46Game_Based_Crypto: theory HOL-Library.LaTeXsugar
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
01:44:46Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
01:44:46Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
01:44:46Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
01:44:46Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
01:44:46Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
01:44:46Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
01:44:47ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
01:44:47Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
01:44:47Sigma_Commit_Crypto: theory HOL-Algebra.Ring
01:44:47Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
01:44:48Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
01:44:48Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
01:44:48Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
01:44:48Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
01:44:48Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
01:44:48Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
01:44:48Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
01:44:48Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
01:44:48Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
01:44:49ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
01:44:49Constructive_Cryptography: theory Constructive_Cryptography.Converter
01:44:49Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
01:44:49ABY3_Protocols: theory ABY3_Protocols.Multiplication
01:44:49ABY3_Protocols: theory ABY3_Protocols.Shuffle
01:44:49Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
01:44:49Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
01:44:50Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
01:44:50Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
01:44:50ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
01:44:51Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
01:44:51Sigma_Commit_Crypto: theory HOL-Algebra.Module
01:44:51Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
01:44:53Timing MDP-Algorithms (6 threads, 354.651s elapsed time, 1303.022s cpu time, 424.194s GC time, factor 3.67)
01:44:53Finished MDP-Algorithms (0:05:58 elapsed time, 0:21:55 cpu time, factor 3.66)
01:44:53SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
01:44:54Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
01:44:55Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
01:44:56Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
01:44:56Timing ABY3_Protocols (6 threads, 8.907s elapsed time, 18.075s cpu time, 0.719s GC time, factor 2.03)
01:44:56Finished ABY3_Protocols (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.86)
01:44:56Timing Deep_Learning (2 threads, 391.188s elapsed time, 690.436s cpu time, 149.618s GC time, factor 1.76)
01:44:56Finished Deep_Learning (0:06:36 elapsed time, 0:11:37 cpu time, factor 1.76)
01:44:56Constructive_Cryptography: theory Constructive_Cryptography.Random_System
01:44:57Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
01:44:57Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
01:44:57Constructive_Cryptography: theory Constructive_Cryptography.Wiring
01:44:58Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
01:44:58Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
01:44:59Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
01:45:02Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
01:45:03Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
01:45:03Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
01:45:03Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
01:45:05Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
01:45:05Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
01:45:06Constructive_Cryptography: theory Constructive_Cryptography.Examples
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
01:45:07Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
01:45:07Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
01:45:12Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
01:45:14Timing Transcendence_Series_Hancl_Rucki (2 threads, 419.266s elapsed time, 761.576s cpu time, 151.959s GC time, factor 1.82)
01:45:14Finished Transcendence_Series_Hancl_Rucki (0:07:04 elapsed time, 0:12:49 cpu time, factor 1.81)
01:45:15Timing Universal_Hash_Families (2 threads, 398.587s elapsed time, 739.534s cpu time, 253.691s GC time, factor 1.86)
01:45:15Finished Universal_Hash_Families (0:06:43 elapsed time, 0:12:26 cpu time, factor 1.85)
01:45:17Timing Game_Based_Crypto (6 threads, 13.978s elapsed time, 57.114s cpu time, 2.152s GC time, factor 4.09)
01:45:17Finished Game_Based_Crypto (0:00:32 elapsed time, 0:01:24 cpu time, factor 2.60)
01:45:18Timing Sigma_Commit_Crypto (6 threads, 30.765s elapsed time, 138.868s cpu time, 10.830s GC time, factor 4.51)
01:45:18Finished Sigma_Commit_Crypto (0:00:32 elapsed time, 0:02:21 cpu time, factor 4.32)
01:45:34Timing TsirelsonBound (2 threads, 95.870s elapsed time, 143.351s cpu time, 5.423s GC time, factor 1.50)
01:45:34Finished TsirelsonBound (0:01:40 elapsed time, 0:02:27 cpu time, factor 1.47)
01:45:35Running Multi_Party_Computation (on 10.195.6.179) ...
01:45:38Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
01:45:38Multi_Party_Computation: theory HOL-Number_Theory.Cong
01:45:39Multi_Party_Computation: theory HOL-Algebra.Ring
01:45:40Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
01:45:41Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
01:45:43Multi_Party_Computation: theory HOL-Number_Theory.Totient
01:45:44Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
01:45:45Multi_Party_Computation: theory HOL-Algebra.AbelCoset
01:45:47Multi_Party_Computation: theory HOL-Algebra.Module
01:45:49Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
01:45:50Multi_Party_Computation: theory HOL-Algebra.Ideal
01:45:51Timing Constructive_Cryptography (6 threads, 49.408s elapsed time, 151.827s cpu time, 11.091s GC time, factor 3.07)
01:45:51Finished Constructive_Cryptography (0:01:05 elapsed time, 0:02:59 cpu time, factor 2.75)
01:45:51Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
01:45:53Timing CAVA_Setup (2 threads, 1351.971s elapsed time, 2379.151s cpu time, 589.960s GC time, factor 1.76)
01:45:53Multi_Party_Computation: theory Multi_Party_Computation.ETP
01:45:53Finished CAVA_Setup (0:25:17 elapsed time, 0:44:04 cpu time, factor 1.74)
01:45:54Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
01:45:54Multi_Party_Computation: theory HOL-Algebra.RingHom
01:45:54Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
01:45:54Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
01:45:56Multi_Party_Computation: theory HOL-Algebra.UnivPoly
01:45:57Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
01:46:03Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
01:46:04Running CAVA_LTL_Modelchecker (on 10.195.8.32) ...
01:46:06Timing Probabilistic_Timed_Automata (2 threads, 327.708s elapsed time, 576.223s cpu time, 34.709s GC time, factor 1.76)
01:46:06Finished Probabilistic_Timed_Automata (0:05:33 elapsed time, 0:09:43 cpu time, factor 1.75)
01:46:07Multi_Party_Computation: theory Multi_Party_Computation.OT14
01:46:08CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
01:46:10Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
01:46:10Multi_Party_Computation: theory Multi_Party_Computation.GMW
01:46:12Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
01:46:13CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
01:46:13CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
01:46:15CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
01:46:15Multi_Party_Computation: theory HOL-Number_Theory.Residues
01:46:17Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
01:46:17Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
01:46:17Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
01:46:18Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
01:46:18Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials
01:46:18Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
01:46:18Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize
01:46:18Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval
01:46:19Perron_Frobenius: theory Perron_Frobenius.Roots_Unity
01:46:19Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion
01:46:20Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
01:46:23Running Constructive_Cryptography_CM (on of4.proof.cit.tum.de) ...
01:46:24Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
01:46:25Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
01:46:25Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
01:46:25Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
01:46:25Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
01:46:27Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible
01:46:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
01:46:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
01:46:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
01:46:28Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
01:46:29Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General
01:46:30Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
01:46:32Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan
01:46:34Timing LLL_Basis_Reduction (2 threads, 270.133s elapsed time, 466.058s cpu time, 98.694s GC time, factor 1.73)
01:46:34Finished LLL_Basis_Reduction (0:05:14 elapsed time, 0:08:40 cpu time, factor 1.66)
01:46:36Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
01:46:37Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
01:46:37Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
01:46:37Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
01:46:38Building Linear_Inequalities (on of4.proof.cit.tum.de) ...
01:46:38Running LLL_Factorization (on of4.proof.cit.tum.de) ...
01:46:38Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
01:46:39Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
01:46:40Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
01:46:40LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
01:46:40LLL_Factorization: theory LLL_Factorization.Sub_Sums
01:46:40LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
01:46:40LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
01:46:41Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
01:46:41Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
01:46:41Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
01:46:41LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
01:46:42LLL_Factorization: theory LLL_Factorization.LLL_Factorization
01:46:43Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
01:46:43Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
01:46:43Linear_Inequalities: theory Linear_Inequalities.Cone
01:46:44Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
01:46:46Linear_Inequalities: theory Linear_Inequalities.Dim_Span
01:46:46Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
01:46:47LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
01:46:48Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
01:46:50Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
01:46:50LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
01:46:50Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
01:46:51Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
01:46:54Quantifier_Elimination_Hybrid FAILED (see also "isabelle build_log -H Error Quantifier_Elimination_Hybrid")
01:46:54*** Failed to apply initial proof method (line 1248 of "~~/AFP/thys/BenOr_Kozen_Reif/BKR_Decision.thy"):
01:46:54*** using this:
01:46:54*** ∀n. n < length (sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0}) - 1 ∧
01:46:54*** sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} ! n ≤ x1 ⟶
01:46:54*** sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} ! (n + 1) ≤ x1 ⟹
01:46:54*** False
01:46:54*** sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} ! 0 ≤ x1 ∧
01:46:54*** x1 ≤ sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} !
01:46:54*** (length (sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0}) - 1)
01:46:54*** goal (1 subgoal):
01:46:54*** 1. ∃n<length (sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0}) - 1.
01:46:54*** sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} ! n < x1 ∧
01:46:54*** x1 < sorted_list_of_set {x. ∃q∈set qs. rpoly q x = 0} ! (n + 1)
01:46:54*** At command "by" (line 1248 of "~~/AFP/thys/BenOr_Kozen_Reif/BKR_Decision.thy")
01:46:55Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
01:46:56Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
01:46:56Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
01:47:00Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp
01:47:00Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block
01:47:02Timing LLL_Factorization (6 threads, 22.341s elapsed time, 64.288s cpu time, 5.627s GC time, factor 2.88)
01:47:02Finished LLL_Factorization (0:00:24 elapsed time, 0:01:06 cpu time, factor 2.72)
01:47:04Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2
01:47:05Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth
01:47:12Timing Linear_Inequalities (6 threads, 20.238s elapsed time, 77.004s cpu time, 7.287s GC time, factor 3.80)
01:47:12Finished Linear_Inequalities (0:00:33 elapsed time, 0:01:37 cpu time, factor 2.87)
01:47:19Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
01:47:20Running LP_Duality (on of2.proof.cit.tum.de) ...
01:47:22LP_Duality: theory LP_Duality.Minimum_Maximum
01:47:22LP_Duality: theory LP_Duality.LP_Duality
01:47:25Timing LP_Duality (6 threads, 1.898s elapsed time, 4.392s cpu time, 0.112s GC time, factor 2.31)
01:47:25Finished LP_Duality (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.60)
01:47:54Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
01:47:56HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
01:47:57Timing Perron_Frobenius (2 threads, 765.410s elapsed time, 1255.491s cpu time, 200.365s GC time, factor 1.64)
01:47:57Finished Perron_Frobenius (0:12:53 elapsed time, 0:21:07 cpu time, factor 1.64)
01:47:57Timing Complex_Bounded_Operators (2 threads, 295.414s elapsed time, 526.152s cpu time, 57.195s GC time, factor 1.78)
01:47:57Finished Complex_Bounded_Operators (0:05:59 elapsed time, 0:10:02 cpu time, factor 1.67)
01:48:05Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
01:48:05Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
01:48:08HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
01:48:12Running Registers (on 10.195.8.32) ...
01:48:13CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
01:48:13CAVA_LTL_Modelchecker: theory LTL.Rewriting
01:48:13CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
01:48:15CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
01:48:16Registers: theory HOL-Eisbach.Eisbach
01:48:16Registers: theory HOL-Library.Type_Length
01:48:17Registers: theory HOL-Library.Z2
01:48:17Registers: theory HOL-Library.Word
01:48:17Registers: theory Registers.Axioms
01:48:17Registers: theory Registers.Laws
01:48:19Registers: theory Registers.Axioms_Complement
01:48:19Registers: theory Registers.Laws_Complement
01:48:19Registers: theory Registers.Axioms_Classical
01:48:19Registers: theory Registers.Laws_Classical
01:48:20CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
01:48:21Registers: theory Registers.Misc
01:48:22Registers: theory Registers.Classical_Extra
01:48:25CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
01:48:26Timing Virtual_Substitution (2 threads, 749.445s elapsed time, 1227.267s cpu time, 358.765s GC time, factor 1.64)
01:48:26Finished Virtual_Substitution (0:12:35 elapsed time, 0:20:36 cpu time, factor 1.64)
01:48:26CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
01:48:27CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
01:48:29Timing Constructive_Cryptography_CM (6 threads, 121.854s elapsed time, 523.172s cpu time, 92.004s GC time, factor 4.29)
01:48:29Finished Constructive_Cryptography_CM (0:02:04 elapsed time, 0:08:47 cpu time, factor 4.25)
01:48:29Registers: theory Registers.Finite_Tensor_Product
01:48:30CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
01:48:30Registers: theory Registers.Axioms_Quantum
01:48:30Registers: theory Registers.Finite_Tensor_Product_Matrices
01:48:30Registers: theory Registers.Quantum
01:48:31CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
01:48:33Registers: theory Registers.Laws_Quantum
01:48:35HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
01:48:36Registers: theory Registers.Quantum_Extra
01:48:37Registers: theory Registers.Axioms_Complement_Quantum
01:48:38Registers: theory Registers.Laws_Complement_Quantum
01:48:38Registers: theory Registers.QHoare
01:48:38Registers: theory Registers.Teleport
01:48:38Registers: theory Registers.Check_Autogenerated_Files
01:48:41Registers: theory Registers.Quantum_Extra2
01:48:42Registers: theory Registers.Pure_States
01:49:04Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
01:49:57Timing Affine_Arithmetic (2 threads, 779.761s elapsed time, 1314.929s cpu time, 250.079s GC time, factor 1.69)
01:49:57Finished Affine_Arithmetic (0:14:04 elapsed time, 0:23:27 cpu time, factor 1.67)
01:49:57Running Taylor_Models (on 10.195.8.49) ...
01:50:00Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
01:50:00Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
01:50:03Timing HOL-ODE-Numerics (6 threads, 620.567s elapsed time, 2626.012s cpu time, 694.415s GC time, factor 4.23)
01:50:03Finished HOL-ODE-Numerics (0:11:03 elapsed time, 0:45:10 cpu time, factor 4.09)
01:50:12Timing Linear_Recurrences_Solver (2 threads, 508.078s elapsed time, 931.132s cpu time, 60.260s GC time, factor 1.83)
01:50:12Finished Linear_Recurrences_Solver (0:08:34 elapsed time, 0:15:39 cpu time, factor 1.83)
01:50:16Building Lorenz_Approximation (on 10.195.8.32) ...
01:50:16Running HOL-ODE-Examples (on 10.195.8.32) ...
01:50:17Taylor_Models: theory Taylor_Models.Polynomial_Expression
01:50:19Timing Multi_Party_Computation (2 threads, 278.466s elapsed time, 508.268s cpu time, 34.875s GC time, factor 1.83)
01:50:19Finished Multi_Party_Computation (0:04:43 elapsed time, 0:08:35 cpu time, factor 1.82)
01:50:20Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
01:50:20HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
01:50:20HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
01:50:21HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
01:50:21Running Poincare_Bendixson (on 10.195.7.194) ...
01:50:22Running HOL-ODE-ARCH-COMP (on 10.195.7.194) ...
01:50:25Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
01:50:26HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
01:50:26Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
01:50:26Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
01:50:27Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
01:50:32Poincare_Bendixson: theory Poincare_Bendixson.Invariance
01:50:35Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
01:50:39Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
01:50:40Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
01:50:47Poincare_Bendixson: theory Poincare_Bendixson.Examples
01:50:50Taylor_Models: theory Taylor_Models.Horner_Eval
01:50:50Taylor_Models: theory HOL-Library.Function_Algebras
01:50:50Taylor_Models: theory Taylor_Models.Float_Topology
01:50:50Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
01:50:50Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
01:50:51Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
01:50:53Taylor_Models: theory Taylor_Models.Taylor_Models
01:51:29Taylor_Models: theory Taylor_Models.Experiments
01:51:42Timing Registers (2 threads, 203.694s elapsed time, 367.661s cpu time, 26.500s GC time, factor 1.80)
01:51:42Finished Registers (0:03:28 elapsed time, 0:06:13 cpu time, factor 1.79)
01:51:59Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
01:52:08Timing Taylor_Models (2 threads, 125.346s elapsed time, 224.198s cpu time, 22.892s GC time, factor 1.79)
01:52:08Finished Taylor_Models (0:02:10 elapsed time, 0:03:50 cpu time, factor 1.77)
01:52:09HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
01:52:47CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
01:53:11Timing Poincare_Bendixson (2 threads, 163.088s elapsed time, 251.602s cpu time, 20.615s GC time, factor 1.54)
01:53:11Finished Poincare_Bendixson (0:02:48 elapsed time, 0:04:17 cpu time, factor 1.53)
01:53:48CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
01:53:48CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
01:53:59Timing CAVA_LTL_Modelchecker (2 threads, 468.237s elapsed time, 566.854s cpu time, 39.498s GC time, factor 1.21)
01:53:59Finished CAVA_LTL_Modelchecker (0:07:54 elapsed time, 0:09:33 cpu time, factor 1.21)
01:55:42Timing Frequency_Moments (2 threads, 988.472s elapsed time, 1794.651s cpu time, 630.518s GC time, factor 1.82)
01:55:42Finished Frequency_Moments (0:18:01 elapsed time, 0:32:05 cpu time, factor 1.78)
01:55:46Building Expander_Graphs (on 10.195.8.42) ...
01:55:54Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
01:55:54Expander_Graphs: theory Graph_Theory.Rtrancl_On
01:55:54Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
01:55:54Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
01:55:55Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
01:55:55Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
01:55:56Expander_Graphs: theory Abstract-Rewriting.Seq
01:55:57Expander_Graphs: theory HOL-Library.More_List
01:55:57Expander_Graphs: theory Perron_Frobenius.Bij_Nat
01:55:57Expander_Graphs: theory HOL-Library.While_Combinator
01:55:58Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
01:55:58Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
01:55:58Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
01:56:00Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
01:56:00Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
01:56:00Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
01:56:03Expander_Graphs: theory Jordan_Normal_Form.Conjugate
01:56:08Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
01:56:09Expander_Graphs: theory HOL-Decision_Procs.Approximation
01:56:11Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:56:13Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
01:56:14Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
01:56:16Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
01:56:16Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:56:17Expander_Graphs: theory Graph_Theory.Stuff
01:56:17Expander_Graphs: theory Graph_Theory.Digraph
01:56:19Expander_Graphs: theory Graph_Theory.Arc_Walk
01:56:23Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
01:56:23Expander_Graphs: theory Graph_Theory.Pair_Digraph
01:56:30Expander_Graphs: theory Graph_Theory.Digraph_Component
01:56:34Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
01:56:37Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
01:56:37Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
01:56:38Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
01:56:42Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
01:56:44Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
01:56:47Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
01:56:48Expander_Graphs: theory Matrix.Utility
01:56:48Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
01:56:54Expander_Graphs: theory Jordan_Normal_Form.Matrix
01:56:55CakeML_Codegen: theory Lazy_Case.Lazy_Case
01:56:55CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
01:56:55CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
01:57:01Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
01:57:01Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:57:02CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
01:57:04CakeML_Codegen: theory CakeML_Codegen.Test_Composition
01:57:06Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
01:57:07Expander_Graphs: theory Jordan_Normal_Form.Determinant
01:57:09Timing Lorenz_Approximation (2 threads, 353.386s elapsed time, 654.008s cpu time, 77.623s GC time, factor 1.85)
01:57:09Finished Lorenz_Approximation (0:06:51 elapsed time, 0:12:11 cpu time, factor 1.78)
01:57:09Running Lorenz_C0 (on 10.195.8.32) ...
01:57:09Running Lorenz_C1 (on 10.195.8.32) ...
01:57:10Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
01:57:10Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
01:57:13CakeML_Codegen: theory CakeML_Codegen.Test_Print
01:57:13Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
01:57:15Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
01:57:15Expander_Graphs: theory Regular-Sets.Regular_Set
01:57:16Expander_Graphs: theory VectorSpace.FunctionLemmas
01:57:16Expander_Graphs: theory VectorSpace.RingModuleFacts
01:57:17Expander_Graphs: theory VectorSpace.MonoidSums
01:57:17Expander_Graphs: theory VectorSpace.LinearCombinations
01:57:19Timing HOL-ODE-Examples (2 threads, 418.188s elapsed time, 720.538s cpu time, 33.651s GC time, factor 1.72)
01:57:19Finished HOL-ODE-Examples (0:07:02 elapsed time, 0:12:05 cpu time, factor 1.72)
01:57:22Expander_Graphs: theory Regular-Sets.Regular_Exp
01:57:26Expander_Graphs: theory Regular-Sets.NDerivative
01:57:28Expander_Graphs: theory Regular-Sets.Relation_Interpretation
01:57:28Expander_Graphs: theory VectorSpace.SumSpaces
01:57:29Expander_Graphs: theory VectorSpace.VectorSpace
01:57:32Expander_Graphs: theory Regular-Sets.Equivalence_Checking
01:57:33Expander_Graphs: theory Regular-Sets.Regexp_Method
01:57:34Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
01:57:41Expander_Graphs: theory Abstract-Rewriting.SN_Orders
01:57:41Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
01:57:44Expander_Graphs: theory Matrix.Ordered_Semiring
01:57:44Timing HOL-ODE-ARCH-COMP (2 threads, 436.647s elapsed time, 842.647s cpu time, 51.251s GC time, factor 1.93)
01:57:44Finished HOL-ODE-ARCH-COMP (0:07:21 elapsed time, 0:14:08 cpu time, factor 1.92)
01:57:45Expander_Graphs: theory Matrix.Matrix_Legacy
01:57:45Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
01:57:46Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
01:57:48Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
01:57:49Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
01:57:49Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
01:57:49Lorenz_C1: theory Lorenz_C1.Lorenz_C1
01:57:49Lorenz_C0: theory Lorenz_C0.Lorenz_C0
01:57:51Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
01:57:52Timing Lorenz_C1 (2 threads, 1.929s elapsed time, 2.584s cpu time, 0.053s GC time, factor 1.34)
01:57:52Finished Lorenz_C1 (0:00:42 elapsed time, 0:00:07 cpu time, factor 0.19)
01:57:52Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
01:57:54Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
01:58:01Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
01:58:03Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
01:58:55Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:59:01Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
01:59:01Expander_Graphs: theory Perron_Frobenius.HMA_Connect
01:59:03Expander_Graphs: theory QHLProver.Complex_Matrix
01:59:08Expander_Graphs: theory QHLProver.Gates
01:59:08Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
01:59:16Expander_Graphs: theory Projective_Measurements.Projective_Measurements
01:59:18Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
01:59:20Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
01:59:25Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
01:59:31Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
01:59:31Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
01:59:35Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
01:59:38Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
02:01:30Timing Smith_Normal_Form (2 threads, 1223.440s elapsed time, 2075.347s cpu time, 633.999s GC time, factor 1.70)
02:01:30Finished Smith_Normal_Form (0:21:54 elapsed time, 0:36:35 cpu time, factor 1.67)
02:01:35Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.8.42) ...
02:01:35Estimated 0:43:36 build time with path time heuristic (critical: absolute time (0:20:00), parallel: time based threads) (took 0.003s)
02:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
02:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
02:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
02:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
02:01:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
02:01:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
02:01:49Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
02:01:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
02:01:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
02:01:51Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
02:01:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
02:01:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
02:01:53Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
02:01:54Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
02:01:54Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
02:01:54Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
02:01:55Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
02:01:56Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
02:01:56Timing CakeML_Codegen (2 threads, 2539.664s elapsed time, 3034.879s cpu time, 286.395s GC time, factor 1.19)
02:01:56Finished CakeML_Codegen (0:42:25 elapsed time, 0:50:44 cpu time, factor 1.20)
02:01:57Timing Automated_Stateful_Protocol_Verification (2 threads, 1901.676s elapsed time, 3612.757s cpu time, 1900.580s GC time, factor 1.90)
02:01:57Finished Automated_Stateful_Protocol_Verification (0:31:55 elapsed time, 1:00:38 cpu time, factor 1.90)
02:01:57Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
02:02:00Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
02:02:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
02:02:02Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
02:02:02Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
02:02:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
02:02:04Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
02:02:05Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
02:02:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
02:02:15Timing SC_DOM_Components (2 threads, 1105.853s elapsed time, 2065.390s cpu time, 243.622s GC time, factor 1.87)
02:02:15Finished SC_DOM_Components (0:18:31 elapsed time, 0:34:33 cpu time, factor 1.87)
02:02:16Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
02:02:18Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
02:02:18Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
02:02:19Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
02:02:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
02:02:21Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
02:02:21Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
02:02:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
02:02:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
02:02:24Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
02:02:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
02:02:35Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
02:02:35Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
02:02:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
02:02:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
02:02:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
02:02:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
02:02:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
02:02:39Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
02:02:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
02:02:41Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
02:02:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
02:02:43Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
02:02:43Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
02:02:44Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
02:02:44Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
02:02:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
02:02:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
02:02:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
02:02:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
02:03:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
02:03:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
02:03:01Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
02:03:04Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
02:03:19Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
02:03:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
02:03:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
02:03:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
02:03:23Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
02:03:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
02:03:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
02:03:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
02:03:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
02:03:33Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
02:03:34Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
02:03:35Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
02:03:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
02:03:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
02:03:44Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
02:03:46Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
02:03:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
02:03:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
02:03:48Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
02:03:49Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
02:03:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
02:03:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
02:03:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
02:04:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
02:04:59Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
02:05:03Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
02:05:08Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
02:05:13Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
02:05:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
02:05:14Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
02:05:15Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
02:05:17Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
02:05:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
02:05:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
02:05:24Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
02:05:24Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
02:05:25Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
02:05:26Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
02:05:27Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
02:05:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
02:05:30Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
02:05:32Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
02:05:33Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
02:05:34Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
02:05:36Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
02:05:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
02:05:37Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
02:05:38Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
02:05:40Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
02:05:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
02:05:47Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
02:05:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
02:05:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
02:05:51Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
02:05:52Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
02:05:55Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
02:05:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
02:05:58Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
02:06:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
02:06:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
02:06:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
02:06:10Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
02:06:16Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
02:06:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
02:06:20Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
02:06:28Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
02:06:29Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
02:06:55Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
02:08:00Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
02:08:00Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
02:10:25Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
02:10:25Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
02:10:58Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
02:10:58Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
02:11:32Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
02:11:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
02:11:42Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
02:11:50Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
02:11:55Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
02:12:07Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
02:12:45Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
02:14:53Timing Expander_Graphs (2 threads, 1038.683s elapsed time, 1884.077s cpu time, 603.249s GC time, factor 1.81)
02:14:53Finished Expander_Graphs (0:18:57 elapsed time, 0:33:33 cpu time, factor 1.77)
02:14:53Running Distributed_Distinct_Elements (on 10.195.8.42) ...
02:14:59Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
02:14:59Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
02:15:00Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
02:15:00Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
02:15:00Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
02:15:00Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
02:15:01Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
02:15:02Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
02:15:08Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
02:15:10Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
02:15:10Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
02:15:10Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
02:15:11Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
02:15:13Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
02:15:17Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
02:15:18Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
02:15:18Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
02:15:19Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
02:15:26Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
02:15:27Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
02:15:27Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
02:15:29Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
02:15:32Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
02:15:32Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
02:15:42Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
02:15:43Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
02:15:52Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
02:15:55Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
02:15:56Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
02:15:58Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
02:17:34Timing Distributed_Distinct_Elements (2 threads, 152.254s elapsed time, 289.648s cpu time, 18.958s GC time, factor 1.90)
02:17:34Finished Distributed_Distinct_Elements (0:02:38 elapsed time, 0:04:57 cpu time, factor 1.87)
02:26:37Timing Lorenz_C0 (2 threads, 1727.622s elapsed time, 3383.444s cpu time, 82.885s GC time, factor 1.96)
02:26:37Finished Lorenz_C0 (0:29:28 elapsed time, 0:56:28 cpu time, factor 1.92)
02:35:33Timing CZH_Universal_Constructions (2 threads, 4711.913s elapsed time, 7378.491s cpu time, 2654.914s GC time, factor 1.57)
02:35:33Finished CZH_Universal_Constructions (1:18:36 elapsed time, 2:03:05 cpu time, factor 1.57)
02:50:34Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2918.041s elapsed time, 5330.276s cpu time, 1537.509s GC time, factor 1.83)
02:50:34Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:48:50 elapsed time, 1:29:11 cpu time, factor 1.83)
02:50:44*** Host "10.195.7.194": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.29": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.11": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.32": failed to work
02:50:44*** Error
02:50:44*** Host "of4.proof.cit.tum.de": failed to work
02:50:44*** Error
02:50:44*** Host "of2.proof.cit.tum.de": failed to work
02:50:44*** Error
02:50:44*** Host "of3.proof.cit.tum.de": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.46": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.40": failed to work
02:50:44*** Error
02:50:44*** Host "10.195.8.30": failed to work
02:50:44*** ### Ignored report message: int
02:50:44*** ### Ignored report message: array\ int
02:50:44*** ### Ignored report message: int
02:50:44*** Host "10.195.8.49": failed to work
02:50:44*** Error
02:50:45*** Host "10.195.6.179": failed to work
02:50:45*** Error
02:50:45*** Host "10.195.8.42": failed to work
02:50:45*** Error
02:50:45Unfinished session(s): Quantifier_Elimination_Hybrid
02:50:4502:50:45Finished at Thu Dec 7 02:50:45 GMT+1 2023
02:50:452:00:31 elapsed time, 59:15:25 cpu time, factor 29.50
02:50:45Build step 'Execute shell' marked build as failure
02:50:46Started calculate disk usage of build
02:50:46Finished Calculation of disk usage of build in 0 seconds
02:51:06Started calculate disk usage of workspace
02:51:07Finished Calculation of disk usage of workspace in 0 seconds
02:51:07Finished: FAILURE