Skipping 885 KB.. Full Log

Count_Complex_Roots: theory Polynomial_Interpolation.Missing_Polynomial
11:10:42 Timing Density_Compiler (2 threads, 118.007s elapsed time, 225.901s cpu time, 13.030s GC time, factor 1.91)
11:10:42 Finished Density_Compiler (0:02:02 elapsed time, 0:03:50 cpu time, factor 1.89)
11:10:43 Bernoulli: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:10:43 Count_Complex_Roots: theory Sturm_Tarski.PolyMisc
11:10:43 Three_Squares: theory HOL-Computational_Algebra.Squarefree
11:10:43 Three_Squares: theory HOL-Eisbach.Eisbach_Tools
11:10:43 Three_Squares: theory HOL-Number_Theory.Cong
11:10:43 Three_Squares: theory HOL-Library.Code_Abstract_Nat
11:10:43 Dirichlet_Series: theory HOL-Algebra.Ideal
11:10:43 E_Transcendental: theory HOL-Algebra.Lattice
11:10:43 Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski
11:10:43 HOL-ODE-Numerics: theory Collections.Iterator
11:10:43 Three_Squares: theory HOL-Library.Code_Target_Nat
11:10:43 Three_Squares: theory HOL-Library.Code_Target_Int
11:10:43 Bernoulli: theory HOL-Number_Theory.Fib
11:10:43 Bernoulli: theory Bernoulli.Periodic_Bernpoly
11:10:43 Three_Squares: theory HOL-Computational_Algebra.Normalized_Fraction
11:10:43 Three_Squares: theory HOL-Algebra.Congruence
11:10:43 CryptHOL: theory HOL-Algebra.Coset
11:10:43 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
11:10:43 Three_Squares: theory HOL-Library.Code_Target_Numeral
11:10:43 Three_Squares: theory HOL-Library.Function_Algebras
11:10:43 Three_Squares: theory HOL-Library.Power_By_Squaring
11:10:43 HOL-ODE-Numerics: theory Collections.Array_Iterator
11:10:43 HOL-ODE-Numerics: theory Collections.RBT_add
11:10:44 Three_Squares: theory HOL-Number_Theory.Eratosthenes
11:10:44 HOL-ODE-Numerics: theory Collections.Intf_Map
11:10:44 Three_Squares: theory Bernoulli.Bernoulli
11:10:44 Bernoulli: theory HOL-Computational_Algebra.Normalized_Fraction
11:10:44 Bernoulli: theory HOL-Number_Theory.Prime_Powers
11:10:44 Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom
11:10:44 Bernoulli: theory HOL-Number_Theory.Mod_Exp
11:10:44 Bernoulli: theory HOL-Algebra.Order
11:10:44 HOL-ODE-Numerics: theory Collections.Gen_Map
11:10:44 Three_Squares: theory HOL-Number_Theory.Mod_Exp
11:10:44 Bernoulli: theory HOL-Number_Theory.Totient
11:10:44 Three_Squares: theory HOL-Algebra.Order
11:10:44 E_Transcendental: theory HOL-Algebra.Complete_Lattice
11:10:44 Three_Squares: theory HOL-Computational_Algebra.Field_as_Ring
11:10:44 Three_Squares: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:10:44 Bernoulli: theory HOL-Computational_Algebra.Polynomial_Factorial
11:10:46 Dirichlet_Series: theory HOL-Algebra.RingHom
11:10:46 Transcendence_Series_Hancl_Rucki: theory Pure-ex.Guess
11:10:46 Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach
11:10:46 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
11:10:46 Three_Squares: theory HOL-Computational_Algebra.Polynomial_Factorial
11:10:46 Count_Complex_Roots: theory Budan_Fourier.BF_Misc
11:10:46 Transcendence_Series_Hancl_Rucki: theory HOL-Combinatorics.Stirling
11:10:46 Three_Squares: theory HOL-Library.Going_To_Filter
11:10:46 Dirichlet_Series: theory HOL-Algebra.UnivPoly
11:10:46 Bernoulli: theory HOL-Algebra.Lattice
11:10:46 Three_Squares: theory HOL-Library.Lattice_Algebras
11:10:47 Three_Squares: theory HOL-Library.Log_Nat
11:10:47 Three_Squares: theory Bernoulli.Periodic_Bernpoly
11:10:47 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fraction_Field
11:10:47 MDP-Algorithms: theory Containers.RBT_Mapping2
11:10:47 HOL-ODE-Numerics: theory Collections.Impl_List_Map
11:10:47 E_Transcendental: theory HOL-Algebra.Group
11:10:47 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
11:10:47 Three_Squares: theory Winding_Number_Eval.Missing_Topology
11:10:47 Three_Squares: theory HOL-Number_Theory.Fib
11:10:47 Bernoulli: theory HOL-Computational_Algebra.Computational_Algebra
11:10:47 CryptHOL: theory CryptHOL.Cyclic_Group
11:10:47 Three_Squares: theory HOL-Algebra.Lattice
11:10:47 Count_Complex_Roots: theory Budan_Fourier.Sturm_Multiple_Roots
11:10:47 Three_Squares: theory HOL-Number_Theory.Prime_Powers
11:10:47 Three_Squares: theory HOL-Number_Theory.Totient
11:10:47 Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach_Tools
11:10:47 Bernoulli: theory HOL-Algebra.Complete_Lattice
11:10:47 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Group_Closure
11:10:48 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic
11:10:48 Three_Squares: theory Winding_Number_Eval.Missing_Analysis
11:10:48 CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
11:10:48 Three_Squares: theory HOL-Computational_Algebra.Computational_Algebra
11:10:48 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Nth_Powers
11:10:48 Three_Squares: theory Sturm_Tarski.PolyMisc
11:10:48 HOL-ODE-Numerics: theory Collections.Intf_Set
11:10:48 Three_Squares: theory Three_Squares.Quadratic_Forms
11:10:48 Running Winding_Number_Eval (on 10.195.6.179) ...
11:10:48 Three_Squares: theory Sturm_Tarski.Sturm_Tarski
11:10:48 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Normalized_Fraction
11:10:48 Three_Squares: theory Landau_Symbols.Group_Sort
11:10:48 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Squarefree
11:10:48 Three_Squares: theory HOL-Algebra.Complete_Lattice
11:10:48 MDP-Algorithms: theory Containers.RBT_Set2
11:10:48 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
11:10:48 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Cong
11:10:48 Running Wetzels_Problem (on of1-proof+8-15) ...
11:10:48 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental
11:10:48 Bernoulli: theory HOL-Algebra.Group
11:10:48 Running Stern_Brocot (on of1-proof+0-7) ...
11:10:49 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Congruence
11:10:49 Three_Squares: theory Budan_Fourier.BF_Misc
11:10:49 HOL-ODE-Numerics: theory Collections.Gen_Set
11:10:49 Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem
11:10:49 Three_Squares: theory HOL-Algebra.Group
11:10:49 Three_Squares: theory Landau_Symbols.Landau_Real_Products
11:10:49 Transcendence_Series_Hancl_Rucki: theory HOL-Library.Power_By_Squaring
11:10:49 CryptHOL: theory Coinductive.TLList
11:10:49 Wetzels_Problem: theory HOL-Cardinals.Order_Union
11:10:49 Wetzels_Problem: theory HOL-Cardinals.Order_Relation_More
11:10:49 Wetzels_Problem: theory HOL-Cardinals.Fun_More
11:10:50 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Mod_Exp
11:10:50 CryptHOL: theory Applicative_Lifting.Applicative_PMF
11:10:50 Three_Squares: theory Winding_Number_Eval.Missing_Algebraic
11:10:50 Stern_Brocot: theory Stern_Brocot.Cotree
11:10:50 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Extension
11:10:50 Winding_Number_Eval: theory HOL-Eisbach.Eisbach
11:10:50 Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field
11:10:50 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Order
11:10:50 Wetzels_Problem: theory HOL-Cardinals.Wellfounded_More
11:10:50 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Relation
11:10:50 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Embedding
11:10:50 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Constructions
11:10:51 Running Error_Function (on of3.proof.cit.tum.de) ...
11:10:51 Running Cotangent_PFD_Formula (on of3.proof.cit.tum.de) ...
11:10:51 Running Cartan_FP (on of3.proof.cit.tum.de) ...
11:10:51 Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom_Poly
11:10:51 MDP-Algorithms: theory Containers.Set_Impl
11:10:51 Three_Squares: theory Winding_Number_Eval.Missing_Transcendental
11:10:51 Wetzels_Problem: theory HOL-Cardinals.Cardinal_Order_Relation
11:10:51 Three_Squares: theory HOL-Library.Interval
11:10:51 Wetzels_Problem: theory HOL-Cardinals.Ordinal_Arithmetic
11:10:52 Three_Squares: theory HOL-Library.Float
11:10:52 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Eratosthenes
11:10:52 Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem
11:10:52 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
11:10:52 Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
11:10:52 HOL-ODE-Numerics: theory Collections.Impl_List_Set
11:10:52 Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring
11:10:52 E_Transcendental: theory HOL-Algebra.Coset
11:10:52 Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
11:10:52 E_Transcendental: theory HOL-Algebra.FiniteProduct
11:10:52 MDP-Algorithms: theory MDP-Algorithms.Fin_Code
11:10:52 Error_Function: theory HOL-Library.Function_Algebras
11:10:52 Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli
11:10:52 Error_Function: theory Error_Function.Error_Function
11:10:52 Cotangent_PFD_Formula: theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
11:10:52 Error_Function: theory Landau_Symbols.Group_Sort
11:10:52 Cartan_FP: theory Cartan_FP.Cartan
11:10:52 Wetzels_Problem: theory HOL-Cardinals.Cardinal_Arithmetic
11:10:52 Bernoulli: theory HOL-Algebra.Coset
11:10:52 Bernoulli: theory HOL-Algebra.FiniteProduct
11:10:52 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Lattice
11:10:52 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
11:10:52 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
11:10:52 Wetzels_Problem: theory HOL-Cardinals.Cardinals
11:10:52 Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval
11:10:52 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Field_as_Ring
11:10:52 Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:10:52 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Library
11:10:52 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
11:10:52 Wetzels_Problem: theory ZFC_in_HOL.ZFC_in_HOL
11:10:53 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
11:10:53 Error_Function: theory Landau_Symbols.Landau_Real_Products
11:10:53 E_Transcendental: theory HOL-Algebra.Ring
11:10:53 CryptHOL: theory Monad_Normalisation.Monad_Normalisation
11:10:53 Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
11:10:53 CryptHOL: theory CryptHOL.SPMF_Applicative
11:10:53 Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
11:10:53 Bernoulli: theory HOL-Algebra.Ring
11:10:53 Three_Squares: theory HOL-Algebra.Coset
11:10:53 Three_Squares: theory HOL-Algebra.FiniteProduct
11:10:53 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Cardinals
11:10:53 Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
11:10:53 Timing Cartan_FP (6 threads, 0.958s elapsed time, 2.732s cpu time, 0.096s GC time, factor 2.85)
11:10:53 Finished Cartan_FP (0:00:02 elapsed time, 0:00:04 cpu time)
11:10:53 CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
11:10:53 Timing Cotangent_PFD_Formula (6 threads, 1.020s elapsed time, 3.270s cpu time, 0.098s GC time, factor 3.21)
11:10:53 Finished Cotangent_PFD_Formula (0:00:02 elapsed time, 0:00:04 cpu time)
11:10:53 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Complete_Lattice
11:10:53 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
11:10:54 Timing Random_BSTs (2 threads, 9.504s elapsed time, 14.549s cpu time, 1.334s GC time, factor 1.53)
11:10:54 Finished Random_BSTs (0:00:39 elapsed time, 0:00:50 cpu time, factor 1.30)
11:10:54 Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group
11:10:54 CryptHOL: theory Landau_Symbols.Group_Sort
11:10:54 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:10:54 Error_Function: theory Landau_Symbols.Landau_Simprocs
11:10:54 Count_Complex_Roots: theory Count_Complex_Roots.CC_Polynomials_Extra
11:10:54 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
11:10:54 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Typeclasses
11:10:55 Error_Function: theory Landau_Symbols.Landau_More
11:10:55 Error_Function: theory Error_Function.Error_Function_Asymptotics
11:10:55 Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
11:10:55 Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
11:10:55 Three_Squares: theory HOL-Algebra.Ring
11:10:55 Dirichlet_Series: theory HOL-Number_Theory.Residues
11:10:55 E_Transcendental: theory HOL-Algebra.Generated_Groups
11:10:55 CryptHOL: theory Landau_Symbols.Landau_Real_Products
11:10:55 Wetzels_Problem: theory ZFC_in_HOL.General_Cardinals
11:10:55 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Group
11:10:55 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_Factorial
11:10:55 Wetzels_Problem: theory Wetzels_Problem.Wetzels_Problem
11:10:56 Timing Error_Function (6 threads, 3.728s elapsed time, 13.053s cpu time, 1.130s GC time, factor 3.50)
11:10:56 Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm
11:10:56 Finished Error_Function (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.74)
11:10:56 Bernoulli: theory HOL-Algebra.Generated_Groups
11:10:56 Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion
11:10:56 Dirichlet_Series: theory HOL-Number_Theory.Gauss
11:10:56 Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
11:10:56 E_Transcendental: theory HOL-Algebra.Elementary_Groups
11:10:56 Winding_Number_Eval: theory Budan_Fourier.BF_Misc
11:10:57 Dirichlet_Series: theory HOL-Number_Theory.Pocklington
11:10:57 Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
11:10:57 Dirichlet_Series: theory HOL-Number_Theory.Number_Theory
11:10:57 Three_Squares: theory Landau_Symbols.Landau_Simprocs
11:10:57 Three_Squares: theory HOL-Library.Interval_Float
11:10:58 E_Transcendental: theory HOL-Algebra.AbelCoset
11:10:58 E_Transcendental: theory HOL-Algebra.Module
11:10:58 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Coset
11:10:58 Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
11:10:58 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.FiniteProduct
11:10:58 Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval
11:10:58 Timing Turans_Graph_Theorem (2 threads, 130.193s elapsed time, 225.403s cpu time, 19.752s GC time, factor 1.73)
11:10:58 Finished Turans_Graph_Theorem (0:02:14 elapsed time, 0:03:50 cpu time, factor 1.71)
11:10:58 Three_Squares: theory HOL-Algebra.Generated_Groups
11:10:58 Dirichlet_Series: theory Bernoulli.Bernoulli_FPS
11:10:58 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc
11:10:58 Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function
11:10:58 Count_Complex_Roots: theory Count_Complex_Roots.Count_Line
11:10:58 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
11:10:58 Three_Squares: theory Landau_Symbols.Landau_More
11:10:58 Bernoulli: theory HOL-Algebra.Elementary_Groups
11:10:59 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product
11:10:59 Dirichlet_Series: theory Dirichlet_Series.Euler_Products
11:10:59 Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
11:10:59 Bernoulli: theory HOL-Algebra.AbelCoset
11:10:59 Bernoulli: theory HOL-Algebra.Module
11:10:59 Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
11:10:59 Three_Squares: theory HOL-Decision_Procs.Approximation_Bounds
11:10:59 Building Smith_Normal_Form (on 10.195.8.32) ...
11:10:59 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ring
11:10:59 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series
11:11:00 Count_Complex_Roots: theory Count_Complex_Roots.Count_Half_Plane
11:11:00 Three_Squares: theory HOL-Algebra.Elementary_Groups
11:11:00 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
11:11:00 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
11:11:00 Three_Squares: theory HOL-Algebra.AbelCoset
11:11:00 Three_Squares: theory HOL-Algebra.Module
11:11:00 Count_Complex_Roots: theory Count_Complex_Roots.Count_Rectangle
11:11:01 CryptHOL: theory Landau_Symbols.Landau_Simprocs
11:11:01 Count_Complex_Roots: theory Count_Complex_Roots.Count_Circle
11:11:01 Timing Projective_Measurements (6 threads, 138.926s elapsed time, 568.536s cpu time, 49.998s GC time, factor 4.09)
11:11:01 Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
11:11:01 Finished Projective_Measurements (0:02:55 elapsed time, 0:10:40 cpu time, factor 3.64)
11:11:01 Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots
11:11:01 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Generated_Groups
11:11:01 Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples
11:11:01 Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu
11:11:01 E_Transcendental: theory HOL-Algebra.Ideal
11:11:02 Dirichlet_Series: theory Dirichlet_Series.More_Totient
11:11:02 CryptHOL: theory Landau_Symbols.Landau_More
11:11:02 Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda
11:11:02 Dirichlet_Series: theory Dirichlet_Series.Divisor_Count
11:11:02 Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
11:11:02 Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory
11:11:02 Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
11:11:02 CryptHOL: theory CryptHOL.Negligible
11:11:02 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code
11:11:02 Dirichlet_Series: theory Dirichlet_Series.Partial_Summation
11:11:02 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Elementary_Groups
11:11:02 MDP-Algorithms: theory MDP-Algorithms.GS_Code
11:11:02 Timing Padic_Field (6 threads, 324.474s elapsed time, 830.752s cpu time, 316.856s GC time, factor 2.56)
11:11:02 Timing Wetzels_Problem (8 threads, 12.254s elapsed time, 68.157s cpu time, 5.499s GC time, factor 5.56)
11:11:02 Finished Wetzels_Problem (0:00:13 elapsed time, 0:01:09 cpu time, factor 5.11)
11:11:03 Finished Padic_Field (0:05:50 elapsed time, 0:15:13 cpu time, factor 2.61)
11:11:03 Smith_Normal_Form: theory HOL-Eisbach.Eisbach
11:11:03 Smith_Normal_Form: theory Deriving.Derive_Manager
11:11:03 Smith_Normal_Form: theory Deriving.Generator_Aux
11:11:04 Smith_Normal_Form: theory HOL-Number_Theory.Cong
11:11:04 Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Computational_Algebra
11:11:04 Stern_Brocot: theory Stern_Brocot.Bird_Tree
11:11:05 Smith_Normal_Form: theory HOL-Algebra.Congruence
11:11:05 Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
11:11:05 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.AbelCoset
11:11:05 Three_Squares: theory HOL-Algebra.Ideal
11:11:05 Timing Stern_Brocot (8 threads, 14.537s elapsed time, 29.852s cpu time, 3.955s GC time, factor 2.05)
11:11:05 Finished Stern_Brocot (0:00:16 elapsed time, 0:00:32 cpu time, factor 2.01)
11:11:06 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
11:11:06 Smith_Normal_Form: theory HOL-Algebra.Order
11:11:06 Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
11:11:06 Bernoulli: theory HOL-Algebra.Ideal
11:11:06 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Module
11:11:06 Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
11:11:06 E_Transcendental: theory HOL-Algebra.RingHom
11:11:07 Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
11:11:07 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
11:11:07 E_Transcendental: theory HOL-Algebra.UnivPoly
11:11:07 Smith_Normal_Form: theory HOL-Algebra.Lattice
11:11:08 Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.PolyMisc
11:11:08 Three_Squares: theory HOL-Algebra.RingHom
11:11:08 Transcendence_Series_Hancl_Rucki: theory HOL-Library.Going_To_Filter
11:11:08 Transcendence_Series_Hancl_Rucki: theory Bernoulli.Periodic_Bernpoly
11:11:09 Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
11:11:09 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ideal
11:11:09 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Topology
11:11:09 Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:11:09 Bernoulli: theory HOL-Algebra.RingHom
11:11:09 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Fib
11:11:09 Three_Squares: theory HOL-Algebra.QuotRing
11:11:09 Three_Squares: theory HOL-Algebra.UnivPoly
11:11:10 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Prime_Powers
11:11:10 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
11:11:10 Smith_Normal_Form: theory HOL-Algebra.Group
11:11:11 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Totient
11:11:12 Bernoulli: theory HOL-Algebra.UnivPoly
11:11:12 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Analysis
11:11:12 Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
11:11:12 Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:11:12 Markov_Models: theory Markov_Models.MDP_RP
11:11:12 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
11:11:12 Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.Sturm_Tarski
11:11:12 MDP-Algorithms: theory MDP-Algorithms.MPI_Code
11:11:12 Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
11:11:12 Three_Squares: theory HOL-Algebra.IntRing
11:11:12 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.RingHom
11:11:13 Building Commuting_Hermitian (on 10.195.7.194) ...
11:11:13 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
11:11:13 Smith_Normal_Form: theory HOL-Algebra.Coset
11:11:14 Transcendence_Series_Hancl_Rucki: theory Budan_Fourier.BF_Misc
11:11:14 Three_Squares: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
11:11:14 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.UnivPoly
11:11:15 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Algebraic
11:11:15 Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
11:11:16 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
11:11:16 Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
11:11:16 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
11:11:16 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Transcendental
11:11:17 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Cauchy_Index_Theorem
11:11:17 Smith_Normal_Form: theory HOL-Algebra.Ring
11:11:18 Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
11:11:18 Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
11:11:18 CryptHOL: theory CryptHOL.Misc_CryptHOL
11:11:19 Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
11:11:19 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
11:11:20 Smith_Normal_Form: theory HOL-Number_Theory.Totient
11:11:20 Timing List_Update (2 threads, 150.251s elapsed time, 256.687s cpu time, 20.112s GC time, factor 1.71)
11:11:20 E_Transcendental: theory HOL-Algebra.Multiplicative_Group
11:11:20 Finished List_Update (0:02:35 elapsed time, 0:04:23 cpu time, factor 1.70)
11:11:20 Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Winding_Number_Eval
11:11:20 Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
11:11:21 Smith_Normal_Form: theory HOL-Algebra.AbelCoset
11:11:22 MDP-Algorithms: theory MDP-Algorithms.VI_Code
11:11:22 Three_Squares: theory HOL-Algebra.Multiplicative_Group
11:11:22 Bernoulli: theory HOL-Algebra.Multiplicative_Group
11:11:22 Smith_Normal_Form: theory HOL-Algebra.Module
11:11:23 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
11:11:23 E_Transcendental: theory HOL-Number_Theory.Residues
11:11:24 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
11:11:25 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
11:11:25 Timing MFMC_Countable (2 threads, 136.636s elapsed time, 232.452s cpu time, 12.156s GC time, factor 1.70)
11:11:25 Bernoulli: theory HOL-Number_Theory.Residues
11:11:25 Finished MFMC_Countable (0:02:21 elapsed time, 0:03:58 cpu time, factor 1.68)
11:11:26 Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
11:11:26 E_Transcendental: theory HOL-Number_Theory.Euler_Criterion
11:11:26 Three_Squares: theory HOL-Number_Theory.Residues
11:11:26 Smith_Normal_Form: theory HOL-Algebra.Ideal
11:11:26 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom
11:11:26 E_Transcendental: theory HOL-Number_Theory.Gauss
11:11:26 E_Transcendental: theory HOL-Number_Theory.Pocklington
11:11:26 Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Multiplicative_Group
11:11:26 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
11:11:26 E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity
11:11:26 E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots
11:11:27 Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
11:11:27 Timing Gromov_Hyperbolicity (2 threads, 305.981s elapsed time, 495.619s cpu time, 39.429s GC time, factor 1.62)
11:11:27 Finished Gromov_Hyperbolicity (0:05:10 elapsed time, 0:08:21 cpu time, factor 1.62)
11:11:27 E_Transcendental: theory HOL-Number_Theory.Number_Theory
11:11:27 Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
11:11:28 E_Transcendental: theory E_Transcendental.E_Transcendental
11:11:28 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
11:11:28 Bernoulli: theory HOL-Number_Theory.Euler_Criterion
11:11:29 Bernoulli: theory HOL-Number_Theory.Gauss
11:11:29 Bernoulli: theory HOL-Number_Theory.Pocklington
11:11:29 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
11:11:29 Bernoulli: theory HOL-Number_Theory.Quadratic_Reciprocity
11:11:29 Smith_Normal_Form: theory HOL-Algebra.RingHom
11:11:29 Bernoulli: theory HOL-Number_Theory.Residue_Primitive_Roots
11:11:29 Running Randomised_BSTs (on of1-proof+0-7) ...
11:11:30 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residues
11:11:30 Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds
11:11:30 Bernoulli: theory HOL-Number_Theory.Number_Theory
11:11:30 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
11:11:30 CryptHOL: theory CryptHOL.Generat
11:11:30 CryptHOL: theory CryptHOL.List_Bits
11:11:30 MDP-Algorithms: theory Jordan_Normal_Form.Matrix
11:11:30 CryptHOL: theory CryptHOL.Resumption
11:11:30 Smith_Normal_Form: theory HOL-Algebra.UnivPoly
11:11:30 Three_Squares: theory HOL-Number_Theory.Euler_Criterion
11:11:30 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
11:11:31 Three_Squares: theory HOL-Number_Theory.Pocklington
11:11:31 Bernoulli: theory Bernoulli.Bernoulli_FPS
11:11:31 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
11:11:32 Three_Squares: theory HOL-Number_Theory.Gauss
11:11:32 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
11:11:32 Three_Squares: theory Lehmer.Lehmer
11:11:32 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
11:11:32 Three_Squares: theory Pratt_Certificate.Pratt_Certificate
11:11:32 Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots
11:11:32 Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity
11:11:32 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Euler_Criterion
11:11:32 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
11:11:32 Smith_Normal_Form: theory List-Index.List_Index
11:11:32 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Gauss
11:11:32 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
11:11:32 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Pocklington
11:11:33 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Quadratic_Reciprocity
11:11:33 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
11:11:33 Three_Squares: theory Three_Squares.Residues_Properties
11:11:33 Three_Squares: theory HOL-Number_Theory.Number_Theory
11:11:33 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
11:11:33 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
11:11:33 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residue_Primitive_Roots
11:11:33 Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Number_Theory
11:11:33 Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds
11:11:33 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations
11:11:34 Timing Ergodic_Theory (2 threads, 118.314s elapsed time, 193.587s cpu time, 7.664s GC time, factor 1.64)
11:11:34 Finished Ergodic_Theory (0:02:32 elapsed time, 0:03:54 cpu time, factor 1.54)
11:11:34 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
11:11:34 Three_Squares: theory Bernoulli.Bernoulli_FPS
11:11:35 Bernoulli: theory Bernoulli.Bernoulli_Zeta
11:11:35 Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
11:11:35 Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_FPS
11:11:35 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Misc
11:11:35 Timing QR_Decomposition (2 threads, 314.281s elapsed time, 535.744s cpu time, 46.668s GC time, factor 1.70)
11:11:35 Finished QR_Decomposition (0:05:18 elapsed time, 0:09:00 cpu time, factor 1.70)
11:11:35 MDP-Algorithms: theory Show.Show
11:11:35 Three_Squares: theory Dirichlet_Series.Multiplicative_Function
11:11:35 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Multiplicative_Function
11:11:35 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Product
11:11:35 CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
11:11:35 Three_Squares: theory Dirichlet_L.Multiplicative_Characters
11:11:35 Three_Squares: theory Dirichlet_Series.Dirichlet_Product
11:11:35 Three_Squares: theory Dirichlet_Series.Euler_Products
11:11:35 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
11:11:35 Timing Randomised_BSTs (8 threads, 3.739s elapsed time, 12.034s cpu time, 0.471s GC time, factor 3.22)
11:11:35 Finished Randomised_BSTs (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.59)
11:11:36 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series
11:11:36 Three_Squares: theory Bertrands_Postulate.Bertrand
11:11:36 MDP-Algorithms: theory Show.Show_Instances
11:11:36 Three_Squares: theory Dirichlet_Series.Dirichlet_Series
11:11:36 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:11:37 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
11:11:38 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Euler_Products
11:11:38 MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
11:11:38 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
11:11:38 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
11:11:39 Running Laws_of_Large_Numbers (on 10.195.8.32) ...
11:11:39 MDP-Algorithms: theory Jordan_Normal_Form.Determinant
11:11:39 Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_Zeta
11:11:39 Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
11:11:39 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Moebius_Mu
11:11:39 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
11:11:40 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.More_Totient
11:11:40 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
11:11:40 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count
11:11:40 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Liouville_Lambda
11:11:40 Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin
11:11:40 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory
11:11:40 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation
11:11:40 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
11:11:41 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
11:11:41 Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
11:11:41 MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
11:11:41 MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
11:11:42 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
11:11:42 Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis
11:11:42 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
11:11:42 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
11:11:42 Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
11:11:43 MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
11:11:43 MDP-Algorithms: theory VectorSpace.FunctionLemmas
11:11:43 MDP-Algorithms: theory VectorSpace.RingModuleFacts
11:11:44 MDP-Algorithms: theory VectorSpace.MonoidSums
11:11:44 Timing Laws_of_Large_Numbers (2 threads, 2.081s elapsed time, 3.395s cpu time, 0.165s GC time, factor 1.63)
11:11:44 Finished Laws_of_Large_Numbers (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20)
11:11:44 MDP-Algorithms: theory VectorSpace.LinearCombinations
11:11:46 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
11:11:46 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
11:11:46 HOL-ODE-Numerics: theory Show.Show
11:11:46 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
11:11:46 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
11:11:46 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
11:11:47 HOL-ODE-Numerics: theory Word_Lib.More_Word
11:11:48 HOL-ODE-Numerics: theory Show.Show_Instances
11:11:48 Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Library
11:11:48 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
11:11:49 Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function
11:11:49 Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:11:49 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
11:11:49 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:11:49 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
11:11:50 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
11:11:50 MDP-Algorithms: theory VectorSpace.SumSpaces
11:11:50 Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
11:11:51 Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
11:11:51 MDP-Algorithms: theory VectorSpace.VectorSpace
11:11:51 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
11:11:51 Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
11:11:52 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
11:11:52 Timing Dirichlet_Series (6 threads, 60.028s elapsed time, 274.512s cpu time, 69.653s GC time, factor 4.57)
11:11:52 Finished Dirichlet_Series (0:01:18 elapsed time, 0:05:07 cpu time, factor 3.94)
11:11:53 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
11:11:53 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
11:11:53 Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
11:11:53 CryptHOL: theory CryptHOL.Computational_Model
11:11:53 CryptHOL: theory CryptHOL.GPV_Applicative
11:11:54 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
11:11:54 Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
11:11:55 Smith_Normal_Form: theory HOL-Number_Theory.Residues
11:11:56 Three_Squares: theory Dirichlet_L.Dirichlet_Characters
11:11:56 Three_Squares: theory Bernoulli.Bernoulli_Zeta
11:11:56 Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin
11:11:56 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
11:11:56 CryptHOL: theory CryptHOL.GPV_Expectation
11:11:57 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
11:11:57 MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
11:11:57 Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
11:11:57 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
11:11:58 CryptHOL: theory CryptHOL.GPV_Bisim
11:11:58 Frequency_Moments: theory Frequency_Moments.K_Smallest
11:11:58 Three_Squares: theory Dirichlet_Series.Moebius_Mu
11:11:58 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
11:11:58 Frequency_Moments: theory Frequency_Moments.Probability_Ext
11:11:58 Three_Squares: theory Dirichlet_Series.More_Totient
11:11:58 Three_Squares: theory Dirichlet_Series.Liouville_Lambda
11:11:58 Three_Squares: theory Dirichlet_Series.Divisor_Count
11:11:59 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
11:11:59 Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
11:11:59 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
11:11:59 CryptHOL: theory CryptHOL.CryptHOL
11:11:59 Three_Squares: theory Dirichlet_Series.Partial_Summation
11:11:59 Smith_Normal_Form: theory Show.Show
11:12:00 Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
11:12:00 Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
11:12:01 Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
11:12:01 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
11:12:01 Timing E_Transcendental (6 threads, 57.733s elapsed time, 184.783s cpu time, 15.951s GC time, factor 3.20)
11:12:01 Finished E_Transcendental (0:01:20 elapsed time, 0:03:38 cpu time, factor 2.72)
11:12:02 Smith_Normal_Form: theory Show.Show_Instances
11:12:02 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
11:12:03 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
11:12:03 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
11:12:03 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
11:12:03 HOL-ODE-Numerics: theory Native_Word.Uint
11:12:04 Smith_Normal_Form: theory Show.Show_Poly
11:12:04 HOL-ODE-Numerics: theory Native_Word.Uint32
11:12:05 Three_Squares: theory Zeta_Function.Zeta_Library
11:12:05 Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
11:12:05 Three_Squares: theory Zeta_Function.Zeta_Function
11:12:05 Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
11:12:05 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
11:12:06 HOL-ODE-Numerics: theory Collections.HashCode
11:12:06 HOL-ODE-Numerics: theory Collections.Intf_Hash
11:12:07 HOL-ODE-Numerics: theory Collections.Gen_Hash
11:12:07 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
11:12:07 Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions
11:12:09 Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
11:12:09 Timing Bernoulli (6 threads, 62.735s elapsed time, 226.575s cpu time, 25.084s GC time, factor 3.61)
11:12:09 Finished Bernoulli (0:01:28 elapsed time, 0:04:26 cpu time, factor 3.03)
11:12:09 Smith_Normal_Form: theory VectorSpace.FunctionLemmas
11:12:10 Smith_Normal_Form: theory VectorSpace.RingModuleFacts
11:12:10 HOL-ODE-Numerics: theory Deriving.Hash_Generator
11:12:10 HOL-ODE-Numerics: theory Deriving.Hash_Instances
11:12:10 HOL-ODE-Numerics: theory Deriving.Derive
11:12:11 Smith_Normal_Form: theory VectorSpace.MonoidSums
11:12:11 Three_Squares: theory Dirichlet_L.Dirichlet_Theorem
11:12:11 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
11:12:11 Smith_Normal_Form: theory VectorSpace.LinearCombinations
11:12:12 Three_Squares: theory Three_Squares.Three_Squares
11:12:14 Timing Winding_Number_Eval (2 threads, 81.998s elapsed time, 151.520s cpu time, 8.965s GC time, factor 1.85)
11:12:14 Finished Winding_Number_Eval (0:01:25 elapsed time, 0:02:34 cpu time, factor 1.81)
11:12:19 Timing Jordan_Normal_Form (2 threads, 743.103s elapsed time, 1290.418s cpu time, 247.352s GC time, factor 1.74)
11:12:19 Finished Jordan_Normal_Form (0:13:28 elapsed time, 0:22:59 cpu time, factor 1.71)
11:12:19 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
11:12:19 Smith_Normal_Form: theory VectorSpace.SumSpaces
11:12:21 Smith_Normal_Form: theory VectorSpace.VectorSpace
11:12:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
11:12:21 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
11:12:22 Building Zeta_Function (on 10.195.7.194) ...
11:12:23 Timing Markov_Models (2 threads, 191.979s elapsed time, 303.687s cpu time, 26.655s GC time, factor 1.58)
11:12:23 Finished Markov_Models (0:04:10 elapsed time, 0:06:17 cpu time, factor 1.51)
11:12:25 Building Pi_Transcendental (on 10.195.8.30) ...
11:12:25 Zeta_Function: theory Bernoulli.Bernoulli_Zeta
11:12:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
11:12:26 Building Stirling_Formula (on 10.195.8.30) ...
11:12:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
11:12:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
11:12:27 Running Gauss_Sums (on 10.195.8.30) ...
11:12:27 Running Euler_MacLaurin (on 10.195.8.30) ...
11:12:28 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
11:12:30 Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
11:12:30 Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
11:12:30 Running Lambert_W (on of2.proof.cit.tum.de) ...
11:12:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
11:12:31 Euler_MacLaurin: theory HOL-Library.Function_Algebras
11:12:31 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
11:12:31 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
11:12:31 Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
11:12:31 Gauss_Sums: theory HOL-Algebra.QuotRing
11:12:31 Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
11:12:31 Stirling_Formula: theory HOL-Library.Function_Algebras
11:12:31 Stirling_Formula: theory Landau_Symbols.Group_Sort
11:12:31 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
11:12:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
11:12:31 Lambert_W: theory HOL-Library.Function_Algebras
11:12:31 Lambert_W: theory Lambert_W.Lambert_W
11:12:31 Lambert_W: theory Landau_Symbols.Group_Sort
11:12:31 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
11:12:32 Zeta_Function: theory HOL-Eisbach.Eisbach
11:12:32 Zeta_Function: theory Pure-ex.Guess
11:12:32 Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
11:12:32 Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
11:12:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
11:12:32 Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
11:12:32 Lambert_W: theory Landau_Symbols.Landau_Real_Products
11:12:32 Pi_Transcendental: theory HOL-Library.Fun_Lexorder
11:12:32 Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
11:12:32 Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
11:12:32 Zeta_Function: theory Sturm_Tarski.PolyMisc
11:12:33 Zeta_Function: theory Winding_Number_Eval.Missing_Topology
11:12:33 Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
11:12:33 Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:12:33 Pi_Transcendental: theory HOL-Library.Poly_Mapping
11:12:33 Zeta_Function: theory Zeta_Function.Zeta_Library
11:12:33 Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
11:12:33 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
11:12:33 Lambert_W: theory Landau_Symbols.Landau_Simprocs
11:12:34 Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
11:12:34 Timing Commuting_Hermitian (2 threads, 47.572s elapsed time, 82.241s cpu time, 6.314s GC time, factor 1.73)
11:12:34 Finished Commuting_Hermitian (0:01:20 elapsed time, 0:01:59 cpu time, factor 1.48)
11:12:34 Lambert_W: theory Landau_Symbols.Landau_More
11:12:34 Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
11:12:34 Lambert_W: theory Stirling_Formula.Stirling_Formula
11:12:34 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
11:12:34 Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series
11:12:35 Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
11:12:35 Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
11:12:36 Zeta_Function: theory Budan_Fourier.BF_Misc
11:12:36 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
11:12:37 Timing Lambert_W (6 threads, 4.896s elapsed time, 18.411s cpu time, 1.675s GC time, factor 3.76)
11:12:37 Finished Lambert_W (0:00:06 elapsed time, 0:00:20 cpu time, factor 3.08)
11:12:37 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
11:12:37 Pi_Transcendental: theory Polynomials.MPoly_Type
11:12:37 Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
11:12:37 Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
11:12:38 Pi_Transcendental: theory Polynomials.More_MPoly_Type
11:12:38 Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
11:12:38 Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
11:12:40 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
11:12:40 Gauss_Sums: theory HOL-Algebra.IntRing
11:12:41 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
11:12:41 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
11:12:41 Pi_Transcendental: theory Symmetric_Polynomials.Vieta
11:12:41 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
11:12:41 Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
11:12:41 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
11:12:42 Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
11:12:42 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
11:12:42 Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
11:12:43 Euler_MacLaurin: theory Landau_Symbols.Landau_More
11:12:43 Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
11:12:43 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
11:12:43 Stirling_Formula: theory Landau_Symbols.Landau_More
11:12:44 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
11:12:44 Stirling_Formula: theory Stirling_Formula.Stirling_Formula
11:12:44 Zeta_Function: theory Zeta_Function.Zeta_Function
11:12:45 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
11:12:45 Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
11:12:46 Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
11:12:46 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
11:12:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
11:12:47 Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
11:12:47 Running TsirelsonBound (on 10.195.8.32) ...
11:12:47 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
11:12:48 Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
11:12:48 Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
11:12:48 Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
11:12:49 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
11:12:49 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
11:12:50 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
11:12:51 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
11:12:52 Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
11:12:53 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
11:12:54 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
11:12:54 Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
11:12:55 TsirelsonBound: theory TsirelsonBound.Tsirelson
11:12:56 Building Subresultants (on 10.195.7.194) ...
11:12:56 Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
11:12:56 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
11:12:57 Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
11:12:58 Timing Euler_MacLaurin (2 threads, 25.192s elapsed time, 39.956s cpu time, 2.458s GC time, factor 1.59)
11:12:58 Finished Euler_MacLaurin (0:00:29 elapsed time, 0:00:43 cpu time, factor 1.50)
11:12:59 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
11:12:59 Subresultants: theory Subresultants.Coeff_Int
11:12:59 Subresultants: theory Subresultants.Dichotomous_Lazard
11:13:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
11:13:00 Subresultants: theory Subresultants.More_Homomorphisms
11:13:00 Subresultants: theory Subresultants.Resultant_Prelim
11:13:00 Gauss_Sums: theory Gauss_Sums.Gauss_Sums
11:13:01 Timing Probabilistic_Noninterference (2 threads, 252.091s elapsed time, 404.360s cpu time, 68.718s GC time, factor 1.60)
11:13:01 Finished Probabilistic_Noninterference (0:04:16 elapsed time, 0:06:49 cpu time, factor 1.60)
11:13:01 Subresultants: theory Subresultants.Binary_Exponentiation
11:13:01 Subresultants: theory Subresultants.Subresultant
11:13:02 Running Stochastic_Matrices (on of2.proof.cit.tum.de) ...
11:13:02 Running Probabilistic_Timed_Automata (on of2.proof.cit.tum.de) ...
11:13:02 Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
11:13:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
11:13:03 Running Perron_Frobenius (on of2.proof.cit.tum.de) ...
11:13:03 Running Linear_Programming (on of2.proof.cit.tum.de) ...
11:13:04 Stochastic_Matrices: theory HOL-Eisbach.Eisbach
11:13:04 Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
11:13:04 Stochastic_Matrices: theory HOL-Algebra.Congruence
11:13:04 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
11:13:04 Stochastic_Matrices: theory HOL-Library.Function_Algebras
11:13:04 Stochastic_Matrices: theory HOL-Library.More_List
11:13:04 Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
11:13:04 Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
11:13:04 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
11:13:04 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
11:13:04 Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
11:13:04 Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
11:13:04 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
11:13:04 Stochastic_Matrices: theory HOL-Algebra.Order
11:13:04 Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
11:13:05 Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
11:13:05 Stochastic_Matrices: theory VectorSpace.FunctionLemmas
11:13:05 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
11:13:05 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
11:13:05 Probabilistic_Timed_Automata: theory Timed_Automata.Misc
11:13:05 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
11:13:05 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
11:13:05 Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
11:13:05 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
11:13:05 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
11:13:05 Linear_Programming: theory Simplex.Simplex_Auxiliary
11:13:05 Linear_Programming: theory Simplex.Simplex_Algebra
11:13:05 Linear_Programming: theory Linear_Programming.More_Jordan_Normal_Forms
11:13:05 Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
11:13:05 Stochastic_Matrices: theory HOL-Algebra.Lattice
11:13:05 Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
11:13:05 Linear_Programming: theory Simplex.Rel_Chain
11:13:06 Subresultants: theory Subresultants.Subresultant_Gcd
11:13:07 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
11:13:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
11:13:07 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
11:13:07 Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
11:13:07 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
11:13:07 Perron_Frobenius: theory HOL-Eisbach.Eisbach
11:13:07 Perron_Frobenius: theory Pure-ex.Guess
11:13:07 Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets
11:13:07 Perron_Frobenius: theory HOL-Analysis.Metric_Arith
11:13:07 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology
11:13:07 Timing Cook_Levin (6 threads, 430.257s elapsed time, 1613.543s cpu time, 171.513s GC time, factor 3.75)
11:13:07 Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable
11:13:07 Finished Cook_Levin (0:07:12 elapsed time, 0:26:59 cpu time, factor 3.74)
11:13:07 Perron_Frobenius: theory HOL-Analysis.Inner_Product
11:13:08 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
11:13:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
11:13:08 Linear_Programming: theory Simplex.Abstract_Linear_Poly
11:13:08 Perron_Frobenius: theory HOL-Analysis.L2_Norm
11:13:08 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
11:13:08 Perron_Frobenius: theory HOL-Analysis.Operator_Norm
11:13:08 Perron_Frobenius: theory HOL-Analysis.Product_Vector
11:13:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
11:13:08 Stochastic_Matrices: theory HOL-Algebra.Group
11:13:09 Linear_Programming: theory Simplex.Linear_Poly_Maps
11:13:09 Linear_Programming: theory Simplex.QDelta
11:13:09 Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
11:13:09 Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Irreducibility
11:13:09 Running Isabelle_Marries_Dirac (on 10.195.8.29) ...
11:13:09 Probabilistic_Timed_Automata: theory Timed_Automata.DBM
11:13:09 Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
11:13:09 Linear_Programming: theory Simplex.Simplex
11:13:09 Probabilistic_Timed_Automata: theory Timed_Automata.Regions
11:13:09 Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial
11:13:10 Perron_Frobenius: theory HOL-Analysis.Norm_Arith
11:13:10 Perron_Frobenius: theory Matrix.Utility
11:13:10 Stochastic_Matrices: theory HOL-Algebra.Coset
11:13:10 Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
11:13:10 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
11:13:11 Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order
11:13:11 Perron_Frobenius: theory Sturm_Sequences.Sturm_Library
11:13:11 Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem
11:13:11 Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization
11:13:11 Stochastic_Matrices: theory HOL-Algebra.Ring
11:13:11 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
11:13:12 Perron_Frobenius: theory HOL-Analysis.Elementary_Topology
11:13:12 Perron_Frobenius: theory HOL-Analysis.Euclidean_Space
11:13:12 Probabilistic_Timed_Automata: theory Timed_Automata.Closure
11:13:13 Perron_Frobenius: theory Sturm_Sequences.Sturm_Method
11:13:13 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
11:13:13 Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:13:13 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
11:13:13 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
11:13:13 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
11:13:14 Isabelle_Marries_Dirac: theory Matrix.Utility
11:13:14 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Basics
11:13:15 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
11:13:15 Perron_Frobenius: theory HOL-Analysis.Abstract_Limits
11:13:15 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Binary_Nat
11:13:15 Isabelle_Marries_Dirac: theory Matrix.Matrix_Legacy
11:13:15 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum
11:13:16 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2
11:13:16 Perron_Frobenius: theory HOL-Analysis.Infinite_Sum
11:13:16 Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product
11:13:16 Perron_Frobenius: theory HOL-Analysis.Linear_Algebra
11:13:16 Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
11:13:16 Stochastic_Matrices: theory HOL-Algebra.Module
11:13:16 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
11:13:16 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
11:13:16 Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:13:16 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
11:13:16 Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
11:13:17 Running Hidden_Markov_Models (on 10.195.8.11) ...
11:13:17 Perron_Frobenius: theory HOL-Analysis.Affine
11:13:17 Stochastic_Matrices: theory VectorSpace.RingModuleFacts
11:13:18 Isabelle_Marries_Dirac: theory Matrix_Tensor.Matrix_Tensor
11:13:18 Perron_Frobenius: theory HOL-Analysis.Connected
11:13:18 Perron_Frobenius: theory HOL-Analysis.Convex
11:13:18 Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces
11:13:18 Perron_Frobenius: theory HOL-Analysis.Cartesian_Space
11:13:18 Stochastic_Matrices: theory VectorSpace.MonoidSums
11:13:18 Perron_Frobenius: theory HOL-Analysis.Function_Topology
11:13:18 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Complex_Vectors
11:13:18 Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
11:13:18 Stochastic_Matrices: theory VectorSpace.LinearCombinations
11:13:19 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
11:13:19 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
11:13:19 Running QHLProver (on of4.proof.cit.tum.de) ...
11:13:19 Perron_Frobenius: theory HOL-Analysis.Product_Topology
11:13:19 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Measurement
11:13:19 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
11:13:20 Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
11:13:20 Perron_Frobenius: theory HOL-Analysis.T1_Spaces
11:13:21 Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
11:13:21 QHLProver: theory Deep_Learning.Tensor
11:13:21 QHLProver: theory QHLProver.Complex_Matrix
11:13:21 QHLProver: theory Deep_Learning.Tensor_Subtensor
11:13:21 QHLProver: theory Deep_Learning.Tensor_Plus
11:13:21 Perron_Frobenius: theory HOL-Analysis.Determinants
11:13:21 QHLProver: theory Deep_Learning.Tensor_Matricization
11:13:21 Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces
11:13:22 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
11:13:22 Hidden_Markov_Models: theory HOL-Library.State_Monad
11:13:22 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
11:13:23 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
11:13:23 QHLProver: theory QHLProver.Gates
11:13:23 QHLProver: theory QHLProver.Matrix_Limit
11:13:23 QHLProver: theory QHLProver.Quantum_Program
11:13:23 Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
11:13:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
11:13:23 Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
11:13:23 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Tensor
11:13:23 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
11:13:23 Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space
11:13:24 QHLProver: theory QHLProver.Partial_State
11:13:24 QHLProver: theory QHLProver.Quantum_Hoare
11:13:24 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.More_Tensor
11:13:24 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.No_Cloning
11:13:25 Stochastic_Matrices: theory VectorSpace.SumSpaces
11:13:25 QHLProver: theory QHLProver.Grover
11:13:25 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch
11:13:25 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Entanglement
11:13:25 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma
11:13:25 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
11:13:26 Stochastic_Matrices: theory VectorSpace.VectorSpace
11:13:27 Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
11:13:27 Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space
11:13:27 Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits
11:13:27 Perron_Frobenius: theory HOL-Analysis.Line_Segment
11:13:27 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch_Jozsa
11:13:27 Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
11:13:28 Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
11:13:28 Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
11:13:28 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
11:13:28 Perron_Frobenius: theory HOL-Analysis.Starlike
11:13:28 Perron_Frobenius: theory HOL-Analysis.Summation_Tests
11:13:28 Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
11:13:28 Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
11:13:28 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
11:13:29 Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:13:29 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Teleportation
11:13:29 Hidden_Markov_Models: theory Monad_Memo_DP.Memory
11:13:29 Perron_Frobenius: theory HOL-Analysis.Uniform_Limit
11:13:30 Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
11:13:30 Linear_Programming: theory Farkas.Farkas
11:13:30 Linear_Programming: theory Simplex.Simplex_Incremental
11:13:30 Perron_Frobenius: theory HOL-Analysis.Path_Connected
11:13:31 Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function
11:13:31 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
11:13:31 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
11:13:32 Timing Stirling_Formula (2 threads, 29.025s elapsed time, 46.271s cpu time, 2.285s GC time, factor 1.59)
11:13:32 Finished Stirling_Formula (0:01:03 elapsed time, 0:01:26 cpu time, factor 1.36)
11:13:32 Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
11:13:32 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
11:13:32 MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
11:13:32 Perron_Frobenius: theory HOL-Analysis.Derivative
11:13:32 Perron_Frobenius: theory HOL-Analysis.Uncountable_Sets
11:13:33 Perron_Frobenius: theory HOL-Analysis.Homotopy
11:13:33 Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
11:13:33 Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
11:13:34 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
11:13:34 Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
11:13:35 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
11:13:35 Linear_Programming: theory Farkas.Matrix_Farkas
11:13:35 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
11:13:36 Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
11:13:36 Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space
11:13:36 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
11:13:36 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
11:13:36 Perron_Frobenius: theory HOL-Analysis.Homeomorphism
11:13:36 Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type
11:13:37 Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint
11:13:37 Timing QHLProver (6 threads, 16.206s elapsed time, 77.387s cpu time, 5.210s GC time, factor 4.78)
11:13:37 Finished QHLProver (0:00:18 elapsed time, 0:01:19 cpu time, factor 4.41)
11:13:37 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
11:13:38 Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
11:13:39 Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous
11:13:39 Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
11:13:39 Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
11:13:42 Running Clique_and_Monotone_Circuits (on 10.195.8.32) ...
11:13:42 Running Comparison_Sort_Lower_Bound (on 10.195.8.32) ...
11:13:42 Running Irrationals_From_THEBOOK (on 10.195.8.32) ...
11:13:43 Linear_Programming: theory Farkas.Simplex_for_Reals
11:13:44 Linear_Programming: theory Linear_Programming.Matrix_LinPoly
11:13:44 Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
11:13:45 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
11:13:45 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
11:13:45 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
11:13:45 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
11:13:45 Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
11:13:45 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
11:13:45 Linear_Programming: theory Linear_Programming.LP_Preliminaries
11:13:46 MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
11:13:46 Timing Schwartz_Zippel (2 threads, 320.943s elapsed time, 544.564s cpu time, 126.501s GC time, factor 1.70)
11:13:46 Finished Schwartz_Zippel (0:05:26 elapsed time, 0:09:11 cpu time, factor 1.69)
11:13:46 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
11:13:47 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
11:13:47 Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
11:13:47 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
11:13:47 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
11:13:47 MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
11:13:48 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
11:13:48 Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
11:13:49 Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
11:13:50 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
11:13:50 Timing Irrationals_From_THEBOOK (2 threads, 4.583s elapsed time, 6.442s cpu time, 0.122s GC time, factor 1.41)
11:13:50 Finished Irrationals_From_THEBOOK (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.17)
11:13:50 Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
11:13:50 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
11:13:51 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
11:13:51 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
11:13:51 Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
11:13:51 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
11:13:53 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
11:13:53 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
11:13:53 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
11:13:54 Linear_Programming: theory Linear_Programming.Linear_Programming
11:13:55 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
11:13:55 MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
11:13:55 MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
11:13:55 Timing Comparison_Sort_Lower_Bound (2 threads, 9.840s elapsed time, 17.151s cpu time, 0.853s GC time, factor 1.74)
11:13:55 Finished Comparison_Sort_Lower_Bound (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.53)
11:13:55 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
11:13:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
11:13:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
11:13:58 Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
11:13:58 Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
11:13:58 MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
11:13:59 Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
11:13:59 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
11:13:59 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
11:14:00 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
11:14:01 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
11:14:01 Timing Hidden_Markov_Models (2 threads, 39.133s elapsed time, 74.169s cpu time, 6.739s GC time, factor 1.90)
11:14:01 Finished Hidden_Markov_Models (0:00:43 elapsed time, 0:01:18 cpu time, factor 1.82)
11:14:01 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
11:14:02 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
11:14:03 MDP-Algorithms: theory MDP-Algorithms.PI_Code
11:14:04 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
11:14:04 Timing Three_Squares (6 threads, 175.885s elapsed time, 727.785s cpu time, 182.990s GC time, factor 4.14)
11:14:04 Finished Three_Squares (0:03:21 elapsed time, 0:12:57 cpu time, factor 3.85)
11:14:09 Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
11:14:09 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
11:14:10 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
11:14:11 Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
11:14:11 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
11:14:11 Timing TsirelsonBound (2 threads, 79.536s elapsed time, 129.299s cpu time, 7.892s GC time, factor 1.63)
11:14:11 Finished TsirelsonBound (0:01:23 elapsed time, 0:02:13 cpu time, factor 1.59)
11:14:11 Timing Gauss_Sums (2 threads, 97.585s elapsed time, 164.185s cpu time, 13.637s GC time, factor 1.68)
11:14:11 Finished Gauss_Sums (0:01:42 elapsed time, 0:02:49 cpu time, factor 1.66)
11:14:13 Timing Pi_Transcendental (2 threads, 59.956s elapsed time, 95.839s cpu time, 6.511s GC time, factor 1.60)
11:14:13 Finished Pi_Transcendental (0:01:44 elapsed time, 0:02:28 cpu time, factor 1.42)
11:14:15 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
11:14:15 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
11:14:17 Timing Deep_Learning (2 threads, 353.434s elapsed time, 607.048s cpu time, 128.721s GC time, factor 1.72)
11:14:17 Finished Deep_Learning (0:05:59 elapsed time, 0:10:14 cpu time, factor 1.71)
11:14:17 Running Polygonal_Number_Theorem (on 10.195.8.30) ...
11:14:21 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
11:14:21 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
11:14:23 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
11:14:23 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
11:14:23 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
11:14:24 Timing Differential_Dynamic_Logic (2 threads, 317.669s elapsed time, 447.245s cpu time, 27.170s GC time, factor 1.41)
11:14:24 Finished Differential_Dynamic_Logic (0:05:23 elapsed time, 0:07:35 cpu time, factor 1.41)
11:14:25 Timing CoSMeDis (2 threads, 2083.702s elapsed time, 3320.786s cpu time, 347.582s GC time, factor 1.59)
11:14:25 Finished CoSMeDis (0:34:49 elapsed time, 0:55:29 cpu time, factor 1.59)
11:14:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
11:14:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
11:14:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
11:14:36 Timing Count_Complex_Roots (2 threads, 196.034s elapsed time, 333.853s cpu time, 24.073s GC time, factor 1.70)
11:14:36 Finished Count_Complex_Roots (0:03:58 elapsed time, 0:06:24 cpu time, factor 1.62)
11:14:36 Timing Linear_Programming (6 threads, 90.132s elapsed time, 259.917s cpu time, 21.794s GC time, factor 2.88)
11:14:36 Finished Linear_Programming (0:01:32 elapsed time, 0:04:23 cpu time, factor 2.85)
11:14:37 Timing Zeta_Function (2 threads, 96.767s elapsed time, 168.567s cpu time, 9.058s GC time, factor 1.74)
11:14:37 Finished Zeta_Function (0:02:13 elapsed time, 0:03:31 cpu time, factor 1.59)
11:14:37 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
11:14:42 Running Dirichlet_L (on 10.195.8.49) ...
11:14:43 Running Hermite_Lindemann (on 10.195.8.49) ...
11:14:43 Building Prime_Number_Theorem (on 10.195.8.49) ...
11:14:44 Building Prime_Distribution_Elementary (on 10.195.8.49) ...
11:14:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
11:14:46 Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
11:14:46 Dirichlet_L: theory HOL-Library.Lattice_Algebras
11:14:46 Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
11:14:46 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
11:14:47 Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
11:14:47 Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
11:14:47 Running Linear_Recurrences (on 10.195.8.32) ...
11:14:47 Hermite_Lindemann: theory HOL-Library.Monad_Syntax
11:14:47 Hermite_Lindemann: theory HOL-Algebra.Divisibility
11:14:47 Hermite_Lindemann: theory Containers.Containers_Auxiliary
11:14:47 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
11:14:47 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
11:14:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
11:14:48 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
11:14:48 Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
11:14:48 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
11:14:49 Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
11:14:49 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
11:14:50 Timing Universal_Hash_Families (2 threads, 388.448s elapsed time, 652.856s cpu time, 188.579s GC time, factor 1.68)
11:14:50 Finished Universal_Hash_Families (0:06:34 elapsed time, 0:11:00 cpu time, factor 1.67)
11:14:50 Linear_Recurrences: theory HOL-Combinatorics.Stirling
11:14:50 Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure
11:14:50 Timing Subresultants (2 threads, 73.560s elapsed time, 111.227s cpu time, 7.808s GC time, factor 1.51)
11:14:50 Finished Subresultants (0:01:53 elapsed time, 0:02:41 cpu time, factor 1.42)
11:14:50 Dirichlet_L: theory HOL-Library.Log_Nat
11:14:51 Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers
11:14:51 Dirichlet_L: theory Lehmer.Lehmer
11:14:51 Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
11:14:51 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
11:14:51 Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree
11:14:51 Timing Clique_and_Monotone_Circuits (2 threads, 65.497s elapsed time, 84.630s cpu time, 3.637s GC time, factor 1.29)
11:14:51 Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat
11:14:51 Finished Clique_and_Monotone_Circuits (0:01:09 elapsed time, 0:01:28 cpu time, factor 1.28)
11:14:51 Linear_Recurrences: theory HOL-Library.Code_Target_Nat
11:14:51 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
11:14:51 Linear_Recurrences: theory HOL-Library.Code_Target_Int
11:14:51 Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
11:14:51 Linear_Recurrences: theory HOL-Library.Sublist
11:14:52 Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
11:14:52 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
11:14:52 Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
11:14:53 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
11:14:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
11:14:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
11:14:53 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
11:14:53 Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial
11:14:54 Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:14:54 Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Irreducibility
11:14:54 Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
11:14:54 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
11:14:54 Dirichlet_L: theory HOL-Library.Interval
11:14:54 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
11:14:54 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
11:14:54 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
11:14:55 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
11:14:55 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
11:14:55 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
11:14:55 Linear_Recurrences: theory Linear_Recurrences.Factorizations
11:14:55 Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
11:14:55 Dirichlet_L: theory HOL-Library.Float
11:14:55 Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials
11:14:55 Linear_Recurrences: theory Linear_Recurrences.RatFPS
11:14:56 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
11:14:56 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
11:14:56 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
11:14:56 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
11:14:56 Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
11:14:57 Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
11:14:57 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
11:14:58 Linear_Recurrences: theory Matrix.Utility
11:14:58 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
11:14:58 Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
11:14:58 Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
11:14:58 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
11:14:58 Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
11:14:58 Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:14:59 Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
11:14:59 Dirichlet_L: theory HOL-Library.Interval_Float
11:15:00 Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
11:15:00 Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
11:15:01 Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
11:15:01 Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
11:15:01 Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
11:15:02 Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
11:15:02 Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
11:15:02 Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
11:15:03 Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
11:15:04 Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
11:15:04 Hermite_Lindemann: theory Matrix.Utility
11:15:05 Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
11:15:05 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
11:15:05 Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
11:15:06 Dirichlet_L: theory Bertrands_Postulate.Bertrand
11:15:09 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
11:15:09 Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
11:15:10 Timing Probabilistic_Timed_Automata (6 threads, 123.922s elapsed time, 379.258s cpu time, 60.051s GC time, factor 3.06)
11:15:10 Finished Probabilistic_Timed_Automata (0:02:06 elapsed time, 0:06:23 cpu time, factor 3.03)
11:15:11 Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
11:15:11 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
11:15:14 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
11:15:14 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
11:15:14 Building Berlekamp_Zassenhaus (on 10.195.8.49) ...
11:15:18 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
11:15:18 Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:15:18 Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
11:15:18 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
11:15:19 Timing Hybrid_Systems_VCs (2 threads, 550.078s elapsed time, 846.929s cpu time, 137.858s GC time, factor 1.54)
11:15:19 Finished Hybrid_Systems_VCs (0:09:14 elapsed time, 0:14:13 cpu time, factor 1.54)
11:15:20 Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
11:15:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
11:15:21 Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
11:15:21 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
11:15:23 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
11:15:23 Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials
11:15:23 Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize
11:15:23 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
11:15:23 Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval
11:15:23 Perron_Frobenius: theory Perron_Frobenius.Roots_Unity
11:15:23 Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan
11:15:23 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
11:15:23 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion
11:15:24 Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
11:15:25 Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
11:15:25 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
11:15:25 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
11:15:25 Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
11:15:25 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
11:15:25 Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
11:15:25 Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
11:15:26 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible
11:15:26 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
11:15:26 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
11:15:26 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
11:15:26 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
11:15:27 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General
11:15:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
11:15:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
11:15:28 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
11:15:28 Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
11:15:28 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
11:15:28 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
11:15:28 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
11:15:28 Hermite_Lindemann: theory Subresultants.More_Homomorphisms
11:15:30 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
11:15:30 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
11:15:31 Hermite_Lindemann: theory Subresultants.Resultant_Prelim
11:15:32 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
11:15:32 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
11:15:33 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
11:15:33 Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
11:15:33 Timing CryptHOL (2 threads, 237.903s elapsed time, 437.449s cpu time, 48.088s GC time, factor 1.84)
11:15:33 Finished CryptHOL (0:05:00 elapsed time, 0:08:50 cpu time, factor 1.76)
11:15:34 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
11:15:34 Hermite_Lindemann: theory Algebraic_Numbers.Resultant
11:15:34 Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
11:15:35 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
11:15:36 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
11:15:36 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
11:15:37 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
11:15:37 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
11:15:37 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
11:15:37 Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
11:15:37 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
11:15:37 Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp
11:15:37 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block
11:15:38 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
11:15:38 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
11:15:38 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
11:15:38 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2
11:15:39 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth
11:15:39 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
11:15:39 Berlekamp_Zassenhaus: theory Matrix.Utility
11:15:39 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
11:15:39 Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
11:15:39 Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
11:15:40 Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
11:15:40 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
11:15:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
11:15:40 Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
11:15:41 Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
11:15:42 Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
11:15:42 Timing Stochastic_Matrices (6 threads, 157.158s elapsed time, 544.431s cpu time, 134.917s GC time, factor 3.46)
11:15:42 Finished Stochastic_Matrices (0:02:39 elapsed time, 0:09:09 cpu time, factor 3.44)
11:15:44 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
11:15:44 Building Constructive_Cryptography (on 10.195.8.32) ...
11:15:44 Running Sigma_Commit_Crypto (on 10.195.8.32) ...
11:15:44 Building Game_Based_Crypto (on 10.195.8.32) ...
11:15:44 Timing Perron_Frobenius (6 threads, 156.022s elapsed time, 628.159s cpu time, 100.276s GC time, factor 4.03)
11:15:45 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
11:15:45 Timing Polygonal_Number_Theorem (2 threads, 81.171s elapsed time, 147.485s cpu time, 8.043s GC time, factor 1.82)
11:15:45 Finished Perron_Frobenius (0:02:38 elapsed time, 0:10:34 cpu time, factor 4.00)
11:15:45 Finished Polygonal_Number_Theorem (0:01:25 elapsed time, 0:02:32 cpu time, factor 1.77)
11:15:45 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
11:15:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
11:15:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
11:15:46 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
11:15:47 Constructive_Cryptography: theory Constructive_Cryptography.Resource
11:15:48 Game_Based_Crypto: theory HOL-Library.LaTeXsugar
11:15:48 Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
11:15:48 Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
11:15:48 Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
11:15:48 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
11:15:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
11:15:48 Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
11:15:49 Sigma_Commit_Crypto: theory HOL-Algebra.Ring
11:15:49 Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
11:15:49 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
11:15:49 Running ABY3_Protocols (on 10.195.8.42) ...
11:15:50 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
11:15:50 Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
11:15:50 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
11:15:50 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
11:15:51 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
11:15:51 Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
11:15:51 Constructive_Cryptography: theory Constructive_Cryptography.Converter
11:15:52 Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
11:15:52 Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
11:15:52 Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
11:15:53 Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
11:15:53 ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
11:15:53 ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
11:15:54 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
11:15:54 ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
11:15:54 Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
11:15:55 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
11:15:55 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
11:15:55 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
11:15:56 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
11:15:56 ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
11:15:57 ABY3_Protocols: theory ABY3_Protocols.Multiplication
11:15:57 ABY3_Protocols: theory ABY3_Protocols.Shuffle
11:15:58 ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
11:15:58 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
11:15:59 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
11:15:59 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
11:15:59 Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
11:16:00 Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
11:16:00 Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
11:16:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
11:16:01 Sigma_Commit_Crypto: theory HOL-Algebra.Module
11:16:02 Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
11:16:02 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
11:16:03 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
11:16:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
11:16:03 Constructive_Cryptography: theory Constructive_Cryptography.Random_System
11:16:03 Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
11:16:04 Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
11:16:05 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
11:16:05 Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
11:16:06 Constructive_Cryptography: theory Constructive_Cryptography.Wiring
11:16:06 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
11:16:06 Berlekamp_Zassenhaus: theory Show.Show_Poly
11:16:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
11:16:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
11:16:07 Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
11:16:07 Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
11:16:07 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
11:16:08 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
11:16:08 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
11:16:08 Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
11:16:09 Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
11:16:10 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
11:16:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
11:16:10 Timing Prime_Number_Theorem (2 threads, 48.456s elapsed time, 75.505s cpu time, 3.514s GC time, factor 1.56)
11:16:10 Finished Prime_Number_Theorem (0:01:26 elapsed time, 0:01:55 cpu time, factor 1.33)
11:16:10 Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
11:16:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
11:16:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
11:16:13 Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
11:16:13 Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
11:16:13 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
11:16:13 Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
11:16:14 Berlekamp_Zassenhaus: theory Word_Lib.More_Word
11:16:15 Timing ABY3_Protocols (2 threads, 21.113s elapsed time, 38.262s cpu time, 3.591s GC time, factor 1.81)
11:16:15 Finished ABY3_Protocols (0:00:25 elapsed time, 0:00:42 cpu time, factor 1.68)
11:16:16 Running Zeta_3_Irrational (on of2.proof.cit.tum.de) ...
11:16:16 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
11:16:17 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
11:16:18 Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
11:16:18 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
11:16:18 Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
11:16:19 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
11:16:19 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
11:16:19 Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
11:16:19 Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
11:16:19 Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
11:16:19 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
11:16:20 Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
11:16:20 Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
11:16:20 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
11:16:21 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
11:16:21 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
11:16:22 Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
11:16:22 Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
11:16:26 Timing Zeta_3_Irrational (6 threads, 7.443s elapsed time, 38.552s cpu time, 1.352s GC time, factor 5.18)
11:16:26 Finished Zeta_3_Irrational (0:00:09 elapsed time, 0:00:40 cpu time, factor 4.38)
11:16:26 Timing Linear_Recurrences (2 threads, 94.854s elapsed time, 164.507s cpu time, 11.551s GC time, factor 1.73)
11:16:26 Finished Linear_Recurrences (0:01:38 elapsed time, 0:02:48 cpu time, factor 1.71)
11:16:27 Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
11:16:28 Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
11:16:29 Constructive_Cryptography: theory Constructive_Cryptography.Examples
11:16:30 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
11:16:30 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
11:16:30 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
11:16:33 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
11:16:33 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
11:16:36 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
11:16:38 Timing Prime_Distribution_Elementary (2 threads, 74.677s elapsed time, 124.933s cpu time, 6.306s GC time, factor 1.67)
11:16:38 Finished Prime_Distribution_Elementary (0:01:53 elapsed time, 0:02:47 cpu time, factor 1.48)
11:16:41 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
11:16:41 Berlekamp_Zassenhaus: theory Native_Word.Uint32
11:16:42 Berlekamp_Zassenhaus: theory Native_Word.Uint64
11:16:44 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
11:16:49 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
11:16:51 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
11:16:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
11:16:53 Running IMO2019 (on of2.proof.cit.tum.de) ...
11:16:53 Running Irrational_Series_Erdos_Straus (on of2.proof.cit.tum.de) ...
11:16:54 IMO2019: theory IMO2019.IMO2019_Q5
11:16:54 IMO2019: theory IMO2019.IMO2019_Q1
11:16:54 IMO2019: theory IMO2019.IMO2019_Q4
11:16:54 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
11:16:55 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
11:16:55 Dirichlet_L: theory HOL-Algebra.QuotRing
11:16:55 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
11:16:55 Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
11:16:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
11:16:56 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
11:16:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
11:16:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
11:16:58 Timing IMO2019 (6 threads, 3.513s elapsed time, 6.400s cpu time, 0.458s GC time, factor 1.82)
11:16:58 Finished IMO2019 (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.53)
11:16:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
11:16:59 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
11:17:01 Timing Irrational_Series_Erdos_Straus (6 threads, 5.667s elapsed time, 21.941s cpu time, 0.683s GC time, factor 3.87)
11:17:01 Finished Irrational_Series_Erdos_Straus (0:00:07 elapsed time, 0:00:23 cpu time, factor 3.16)
11:17:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
11:17:02 Dirichlet_L: theory HOL-Algebra.IntRing
11:17:02 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
11:17:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
11:17:03 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
11:17:04 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
11:17:04 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
11:17:04 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
11:17:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
11:17:06 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
11:17:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
11:17:09 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
11:17:09 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
11:17:10 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
11:17:10 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
11:17:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
11:17:11 Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
11:17:14 Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
11:17:16 Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
11:17:22 Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
11:17:24 Timing Game_Based_Crypto (2 threads, 61.945s elapsed time, 107.336s cpu time, 6.729s GC time, factor 1.73)
11:17:24 Finished Game_Based_Crypto (0:01:39 elapsed time, 0:02:32 cpu time, factor 1.54)
11:17:25 Running Multi_Party_Computation (on 10.195.8.32) ...
11:17:29 Multi_Party_Computation: theory HOL-Number_Theory.Cong
11:17:29 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
11:17:30 Timing Transcendence_Series_Hancl_Rucki (2 threads, 399.455s elapsed time, 704.725s cpu time, 154.437s GC time, factor 1.76)
11:17:30 Finished Transcendence_Series_Hancl_Rucki (0:06:44 elapsed time, 0:11:52 cpu time, factor 1.76)
11:17:30 Multi_Party_Computation: theory HOL-Algebra.Ring
11:17:31 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
11:17:32 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
11:17:33 Multi_Party_Computation: theory HOL-Number_Theory.Totient
11:17:34 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
11:17:35 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
11:17:37 Multi_Party_Computation: theory HOL-Algebra.Module
11:17:41 Multi_Party_Computation: theory HOL-Algebra.Ideal
11:17:42 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
11:17:44 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
11:17:45 Multi_Party_Computation: theory Multi_Party_Computation.ETP
11:17:45 Multi_Party_Computation: theory HOL-Algebra.RingHom
11:17:46 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
11:17:47 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
11:17:47 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
11:17:47 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
11:17:48 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
11:17:51 Timing Isabelle_Marries_Dirac (2 threads, 275.258s elapsed time, 477.641s cpu time, 20.221s GC time, factor 1.74)
11:17:51 Finished Isabelle_Marries_Dirac (0:04:40 elapsed time, 0:08:03 cpu time, factor 1.72)
11:17:54 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
11:17:57 Timing Dirichlet_L (2 threads, 188.727s elapsed time, 328.758s cpu time, 31.159s GC time, factor 1.74)
11:17:57 Finished Dirichlet_L (0:03:13 elapsed time, 0:05:34 cpu time, factor 1.73)
11:17:58 Multi_Party_Computation: theory Multi_Party_Computation.OT14
11:17:59 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
11:18:01 Multi_Party_Computation: theory Multi_Party_Computation.GMW
11:18:03 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
11:18:03 Multi_Party_Computation: theory HOL-Number_Theory.Residues
11:18:06 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
11:18:06 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
11:18:06 Timing Hermite_Lindemann (2 threads, 197.067s elapsed time, 343.409s cpu time, 27.789s GC time, factor 1.74)
11:18:06 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
11:18:06 Finished Hermite_Lindemann (0:03:21 elapsed time, 0:05:49 cpu time, factor 1.73)
11:18:30 Timing Sigma_Commit_Crypto (2 threads, 160.627s elapsed time, 266.898s cpu time, 24.851s GC time, factor 1.66)
11:18:30 Finished Sigma_Commit_Crypto (0:02:45 elapsed time, 0:04:32 cpu time, factor 1.65)
11:19:17 Timing Executable_Randomized_Algorithms (2 threads, 654.415s elapsed time, 1112.524s cpu time, 229.055s GC time, factor 1.70)
11:19:17 Finished Executable_Randomized_Algorithms (0:11:01 elapsed time, 0:18:42 cpu time, factor 1.70)
11:19:24 Timing Virtual_Substitution (2 threads, 791.143s elapsed time, 1266.617s cpu time, 359.532s GC time, factor 1.60)
11:19:24 Finished Virtual_Substitution (0:13:16 elapsed time, 0:21:15 cpu time, factor 1.60)
11:19:46 Timing Constructive_Cryptography (2 threads, 200.456s elapsed time, 315.173s cpu time, 17.320s GC time, factor 1.57)
11:19:46 Finished Constructive_Cryptography (0:04:01 elapsed time, 0:06:09 cpu time, factor 1.53)
11:19:48 Running Constructive_Cryptography_CM (on 10.195.8.42) ...
11:19:52 Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
11:19:52 Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
11:19:55 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
11:20:04 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
11:20:04 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
11:20:04 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
11:20:05 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
11:20:06 Timing CZH_Elementary_Categories (2 threads, 2044.025s elapsed time, 3821.737s cpu time, 1974.149s GC time, factor 1.87)
11:20:06 Finished CZH_Elementary_Categories (0:34:28 elapsed time, 1:04:13 cpu time, factor 1.86)
11:20:08 Running CZH_Universal_Constructions (on 10.195.8.11) ...
11:20:10 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
11:20:10 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
11:20:10 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
11:20:18 Estimated 1:02:06 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.208s)
11:20:26 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
11:20:27 Timing Affine_Arithmetic (2 threads, 786.640s elapsed time, 1323.580s cpu time, 222.651s GC time, factor 1.68)
11:20:27 Finished Affine_Arithmetic (0:14:18 elapsed time, 0:23:45 cpu time, factor 1.66)
11:20:27 Running Taylor_Models (on 10.195.6.179) ...
11:20:30 Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
11:20:30 Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
11:20:35 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
11:20:36 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
11:20:39 Timing CAVA_Setup (2 threads, 1296.639s elapsed time, 2273.188s cpu time, 624.854s GC time, factor 1.75)
11:20:39 Finished CAVA_Setup (0:23:05 elapsed time, 0:39:59 cpu time, factor 1.73)
11:20:46 Taylor_Models: theory Taylor_Models.Polynomial_Expression
11:20:46 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
11:20:47 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
11:20:48 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
11:20:48 CakeML_Codegen: theory Lazy_Case.Lazy_Case
11:20:49 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
11:20:49 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
11:20:49 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
11:20:50 Running CAVA_LTL_Modelchecker (on 10.195.8.29) ...
11:20:52 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
11:20:54 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
11:20:56 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
11:20:58 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
11:20:59 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
11:20:59 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
11:21:00 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
11:21:01 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
11:21:07 CakeML_Codegen: theory CakeML_Codegen.Test_Composition
11:21:12 CakeML_Codegen: theory CakeML_Codegen.Test_Print
11:21:21 Taylor_Models: theory HOL-Library.Function_Algebras
11:21:21 Taylor_Models: theory Taylor_Models.Horner_Eval
11:21:21 Taylor_Models: theory Taylor_Models.Float_Topology
11:21:22 Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
11:21:22 Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
11:21:25 Taylor_Models: theory Taylor_Models.Taylor_Models
11:21:27 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
11:21:35 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
11:21:39 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
11:21:39 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
11:21:58 Taylor_Models: theory Taylor_Models.Experiments
11:22:16 Timing Multi_Party_Computation (2 threads, 285.068s elapsed time, 519.435s cpu time, 46.032s GC time, factor 1.82)
11:22:16 Finished Multi_Party_Computation (0:04:50 elapsed time, 0:08:45 cpu time, factor 1.81)
11:22:21 Timing Berlekamp_Zassenhaus (2 threads, 367.715s elapsed time, 644.487s cpu time, 115.095s GC time, factor 1.75)
11:22:21 Finished Berlekamp_Zassenhaus (0:07:01 elapsed time, 0:11:59 cpu time, factor 1.71)
11:22:26 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
11:22:36 Timing Taylor_Models (2 threads, 124.066s elapsed time, 216.490s cpu time, 17.674s GC time, factor 1.74)
11:22:36 Finished Taylor_Models (0:02:08 elapsed time, 0:03:41 cpu time, factor 1.73)
11:22:38 Building Algebraic_Numbers (on 10.195.8.46) ...
11:22:38 Running Linear_Recurrences_Solver (on 10.195.8.46) ...
11:22:38 Building LLL_Basis_Reduction (on 10.195.8.46) ...
11:22:38 Running Fishers_Inequality (on 10.195.8.46) ...
11:22:39 Running CVP_Hardness (on 10.195.8.46) ...
11:22:42 Fishers_Inequality: theory Card_Partitions.Set_Partition
11:22:42 Fishers_Inequality: theory Polynomials.MPoly_Type
11:22:43 CVP_Hardness: theory CVP_Hardness.Reduction
11:22:43 CVP_Hardness: theory CVP_Hardness.Digits_int
11:22:43 CVP_Hardness: theory CVP_Hardness.Partition
11:22:43 CVP_Hardness: theory CVP_Hardness.Subset_Sum
11:22:43 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
11:22:43 CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
11:22:43 Fishers_Inequality: theory Polynomials.More_MPoly_Type
11:22:44 Fishers_Inequality: theory Polynomials.More_Modules
11:22:44 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
11:22:44 CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
11:22:44 Fishers_Inequality: theory Design_Theory.Multisets_Extras
11:22:44 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
11:22:45 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
11:22:45 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
11:22:45 Running CRYSTALS-Kyber (on 10.195.8.30) ...
11:22:45 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
11:22:45 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
11:22:46 Fishers_Inequality: theory Design_Theory.Design_Basics
11:22:46 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
11:22:47 CVP_Hardness: theory Algebraic_Numbers.Resultant
11:22:47 Fishers_Inequality: theory List-Index.List_Index
11:22:47 Linear_Recurrences_Solver: theory Pure-ex.Guess
11:22:47 Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
11:22:47 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
11:22:48 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
11:22:48 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
11:22:48 Algebraic_Numbers: theory Pure-ex.Guess
11:22:48 Algebraic_Numbers: theory Deriving.Compare_Rat
11:22:48 Fishers_Inequality: theory Design_Theory.Design_Operations
11:22:48 Linear_Recurrences_Solver: theory Deriving.Compare_Real
11:22:48 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
11:22:48 Algebraic_Numbers: theory Deriving.Compare_Real
11:22:48 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
11:22:48 Linear_Recurrences_Solver: theory Polynomials.More_Modules
11:22:49 Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
11:22:49 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
11:22:49 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
11:22:49 CVP_Hardness: theory CVP_Hardness.Lattice_int
11:22:49 CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp
11:22:49 CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes
11:22:49 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
11:22:49 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
11:22:49 Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
11:22:50 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
11:22:50 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
11:22:50 CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
11:22:50 CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product
11:22:50 Fishers_Inequality: theory Design_Theory.Block_Designs
11:22:50 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
11:22:50 CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm
11:22:50 CVP_Hardness: theory CVP_Hardness.CVP_p
11:22:50 CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector
11:22:51 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
11:22:51 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
11:22:51 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
11:22:51 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
11:22:51 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
11:22:52 CRYSTALS-Kyber: theory HOL-Number_Theory.Fib
11:22:52 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
11:22:52 CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers
11:22:52 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
11:22:52 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
11:22:53 CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space
11:22:53 Fishers_Inequality: theory Design_Theory.Sub_Designs
11:22:53 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
11:22:53 CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion
11:22:53 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
11:22:54 CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss
11:22:54 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
11:22:54 CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity
11:22:54 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
11:22:55 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
11:22:55 CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington
11:22:55 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
11:22:55 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
11:22:56 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
11:22:56 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
11:22:56 CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots
11:22:56 Fishers_Inequality: theory Design_Theory.BIBD
11:22:56 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
11:22:57 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
11:22:57 CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product
11:22:57 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
11:22:57 CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory
11:22:57 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
11:22:57 Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
11:22:57 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
11:22:58 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
11:22:58 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
11:22:58 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
11:22:58 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
11:22:58 CAVA_LTL_Modelchecker: theory LTL.Rewriting
11:22:58 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
11:22:58 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
11:22:58 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
11:22:59 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
11:22:59 Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
11:22:59 Fishers_Inequality: theory Polynomials.Utils
11:22:59 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec
11:22:59 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral
11:22:59 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
11:22:59 Fishers_Inequality: theory Groebner_Bases.General
11:22:59 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
11:23:00 Algebraic_Numbers: theory Show.Show_Real
11:23:00 Algebraic_Numbers: theory Show.Show_Complex
11:23:00 CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas
11:23:00 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
11:23:00 Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
11:23:01 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
11:23:01 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
11:23:01 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
11:23:01 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
11:23:01 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
11:23:02 Fishers_Inequality: theory Polynomials.Power_Products
11:23:02 CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT
11:23:03 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus
11:23:03 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr
11:23:03 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress
11:23:04 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
11:23:04 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
11:23:05 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
11:23:05 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
11:23:05 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme
11:23:05 CVP_Hardness: theory LLL_Basis_Reduction.Norms
11:23:06 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
11:23:06 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
11:23:06 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values
11:23:06 CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme
11:23:06 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
11:23:07 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844
11:23:07 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
11:23:08 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT
11:23:09 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values
11:23:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
11:23:09 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
11:23:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
11:23:11 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
11:23:11 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
11:23:11 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
11:23:11 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
11:23:12 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
11:23:12 Linear_Recurrences_Solver: theory Show.Show_Real
11:23:12 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
11:23:12 Linear_Recurrences_Solver: theory Show.Show_Complex
11:23:13 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
11:23:13 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
11:23:13 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
11:23:15 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
11:23:15 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
11:23:15 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
11:23:15 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
11:23:15 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
11:23:16 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
11:23:16 Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
11:23:17 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
11:23:17 Timing Frequency_Moments (2 threads, 827.367s elapsed time, 1458.363s cpu time, 365.177s GC time, factor 1.76)
11:23:17 Finished Frequency_Moments (0:14:58 elapsed time, 0:25:51 cpu time, factor 1.73)
11:23:17 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
11:23:17 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
11:23:17 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
11:23:17 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
11:23:17 Linear_Recurrences_Solver: theory Polynomials.Utils
11:23:18 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
11:23:18 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
11:23:18 Linear_Recurrences_Solver: theory Polynomials.Power_Products
11:23:20 Building Expander_Graphs (on 10.195.8.29) ...
11:23:21 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
11:23:22 Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
11:23:22 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
11:23:22 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
11:23:23 Timing Complex_Bounded_Operators_Dependencies (2 threads, 957.281s elapsed time, 1644.377s cpu time, 438.330s GC time, factor 1.72)
11:23:23 Finished Complex_Bounded_Operators_Dependencies (0:17:12 elapsed time, 0:29:11 cpu time, factor 1.70)
11:23:23 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
11:23:24 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
11:23:24 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
11:23:24 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
11:23:28 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
11:23:28 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
11:23:28 Expander_Graphs: theory Graph_Theory.Rtrancl_On
11:23:28 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
11:23:30 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
11:23:30 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
11:23:30 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
11:23:31 Expander_Graphs: theory Abstract-Rewriting.Seq
11:23:32 Expander_Graphs: theory HOL-Library.More_List
11:23:32 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
11:23:32 Expander_Graphs: theory HOL-Library.While_Combinator
11:23:32 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
11:23:33 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
11:23:33 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
11:23:34 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
11:23:34 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
11:23:34 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
11:23:35 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
11:23:35 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
11:23:36 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
11:23:36 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
11:23:36 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
11:23:36 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
11:23:37 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
11:23:37 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
11:23:38 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
11:23:38 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
11:23:39 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
11:23:40 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
11:23:41 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
11:23:41 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
11:23:42 Building Complex_Bounded_Operators (on of3.proof.cit.tum.de) ...
11:23:42 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
11:23:43 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
11:23:43 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
11:23:43 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
11:23:43 Expander_Graphs: theory HOL-Decision_Procs.Approximation
11:23:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
11:23:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
11:23:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
11:23:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
11:23:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
11:23:44 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
11:23:44 CVP_Hardness: theory CVP_Hardness.infnorm
11:23:44 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
11:23:45 CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
11:23:45 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
11:23:45 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
11:23:47 CVP_Hardness: theory CVP_Hardness.BHLE
11:23:48 CVP_Hardness: theory CVP_Hardness.SVP_vec
11:23:48 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
11:23:48 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:23:48 CVP_Hardness: theory CVP_Hardness.CVP_vec
11:23:48 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
11:23:50 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
11:23:50 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
11:23:50 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
11:23:51 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
11:23:52 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
11:23:53 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
11:23:53 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
11:23:53 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:23:53 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
11:23:53 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
11:23:54 Expander_Graphs: theory Graph_Theory.Stuff
11:23:54 Expander_Graphs: theory Graph_Theory.Digraph
11:23:55 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
11:23:55 Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
11:23:55 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
11:23:55 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
11:23:56 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
11:23:56 Expander_Graphs: theory Graph_Theory.Arc_Walk
11:23:56 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
11:23:56 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
11:23:57 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
11:23:57 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
11:23:58 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
11:23:58 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
11:23:58 Expander_Graphs: theory Graph_Theory.Pair_Digraph
11:23:59 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
11:24:00 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
11:24:00 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
11:24:01 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
11:24:03 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
11:24:03 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
11:24:05 Expander_Graphs: theory Graph_Theory.Digraph_Component
11:24:06 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
11:24:07 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
11:24:08 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
11:24:10 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
11:24:11 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
11:24:12 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
11:24:12 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
11:24:15 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
11:24:17 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
11:24:19 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
11:24:19 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
11:24:20 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
11:24:20 Expander_Graphs: theory Matrix.Utility
11:24:21 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
11:24:26 Expander_Graphs: theory Jordan_Normal_Form.Matrix
11:24:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
11:24:34 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
11:24:34 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
11:24:34 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:24:35 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
11:24:36 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
11:24:37 Expander_Graphs: theory Jordan_Normal_Form.Determinant
11:24:39 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
11:24:39 Expander_Graphs: theory Regular-Sets.Regular_Set
11:24:41 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
11:24:42 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
11:24:43 Expander_Graphs: theory Regular-Sets.Regular_Exp
11:24:43 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
11:24:44 Timing Complex_Bounded_Operators (6 threads, 41.841s elapsed time, 193.538s cpu time, 17.428s GC time, factor 4.63)
11:24:44 Finished Complex_Bounded_Operators (0:01:01 elapsed time, 0:03:49 cpu time, factor 3.74)
11:24:44 Expander_Graphs: theory VectorSpace.FunctionLemmas
11:24:44 Expander_Graphs: theory VectorSpace.RingModuleFacts
11:24:44 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
11:24:44 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
11:24:45 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
11:24:45 Running Registers (on of3.proof.cit.tum.de) ...
11:24:45 Expander_Graphs: theory VectorSpace.MonoidSums
11:24:46 Expander_Graphs: theory VectorSpace.LinearCombinations
11:24:47 Registers: theory HOL-Eisbach.Eisbach
11:24:47 Registers: theory HOL-Library.Type_Length
11:24:47 Registers: theory HOL-Library.Z2
11:24:47 Registers: theory Registers.Axioms
11:24:47 Registers: theory Registers.Axioms_Classical
11:24:47 Registers: theory Registers.Laws
11:24:47 Registers: theory Registers.Laws_Classical
11:24:47 Registers: theory Registers.Misc
11:24:47 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
11:24:47 Registers: theory HOL-Library.Word
11:24:48 Registers: theory Registers.Axioms_Complement
11:24:48 Registers: theory Registers.Laws_Complement
11:24:48 Registers: theory Registers.Classical_Extra
11:24:48 Registers: theory Registers.Finite_Tensor_Product
11:24:48 Registers: theory Registers.Axioms_Quantum
11:24:48 Registers: theory Registers.Finite_Tensor_Product_Matrices
11:24:48 Registers: theory Registers.Quantum
11:24:48 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
11:24:49 Registers: theory Registers.Laws_Quantum
11:24:50 Expander_Graphs: theory Regular-Sets.NDerivative
11:24:50 Registers: theory Registers.Quantum_Extra
11:24:51 Registers: theory Registers.Axioms_Complement_Quantum
11:24:51 Registers: theory Registers.QHoare
11:24:52 Registers: theory Registers.Laws_Complement_Quantum
11:24:52 Registers: theory Registers.Check_Autogenerated_Files
11:24:52 Registers: theory Registers.Quantum_Extra2
11:24:52 Registers: theory Registers.Teleport
11:24:52 Registers: theory Registers.Pure_States
11:24:56 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
11:24:56 Expander_Graphs: theory VectorSpace.SumSpaces
11:24:56 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
11:24:57 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
11:24:57 Expander_Graphs: theory VectorSpace.VectorSpace
11:24:57 Expander_Graphs: theory Regular-Sets.Regexp_Method
11:24:58 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
11:25:04 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
11:25:06 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
11:25:06 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
11:25:07 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
11:25:08 Expander_Graphs: theory Matrix.Ordered_Semiring
11:25:09 Expander_Graphs: theory Matrix.Matrix_Legacy
11:25:11 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
11:25:12 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
11:25:14 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
11:25:15 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
11:25:15 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
11:25:15 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
11:25:15 Timing Registers (6 threads, 26.929s elapsed time, 123.973s cpu time, 11.294s GC time, factor 4.60)
11:25:15 Finished Registers (0:00:29 elapsed time, 0:02:07 cpu time, factor 4.36)
11:25:17 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
11:25:18 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
11:25:19 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
11:25:22 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
11:25:23 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
11:25:27 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
11:25:31 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
11:25:31 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
11:25:31 Expander_Graphs: theory QHLProver.Complex_Matrix
11:25:36 Expander_Graphs: theory QHLProver.Gates
11:25:36 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
11:25:36 Timing CRYSTALS-Kyber (2 threads, 164.876s elapsed time, 272.772s cpu time, 20.210s GC time, factor 1.65)
11:25:36 Finished CRYSTALS-Kyber (0:02:50 elapsed time, 0:04:38 cpu time, factor 1.64)
11:25:42 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
11:25:42 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
11:25:44 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
11:25:45 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
11:25:49 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
11:25:54 Timing CVP_Hardness (2 threads, 189.854s elapsed time, 309.396s cpu time, 18.278s GC time, factor 1.63)
11:25:54 Finished CVP_Hardness (0:03:15 elapsed time, 0:05:15 cpu time, factor 1.62)
11:25:55 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
11:25:55 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
11:25:56 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
11:25:57 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
11:26:00 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
11:26:08 Timing Fishers_Inequality (2 threads, 202.405s elapsed time, 339.951s cpu time, 31.641s GC time, factor 1.68)
11:26:08 Finished Fishers_Inequality (0:03:27 elapsed time, 0:05:46 cpu time, factor 1.67)
11:26:56 Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
11:26:56 Timing CakeML_Codegen (2 threads, 2706.607s elapsed time, 3302.490s cpu time, 416.073s GC time, factor 1.22)
11:26:56 Finished CakeML_Codegen (0:45:13 elapsed time, 0:55:13 cpu time, factor 1.22)
11:27:11 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
11:27:17 Timing LLL_Basis_Reduction (2 threads, 233.492s elapsed time, 372.626s cpu time, 31.065s GC time, factor 1.60)
11:27:17 Finished LLL_Basis_Reduction (0:04:36 elapsed time, 0:07:09 cpu time, factor 1.55)
11:27:19 Building Linear_Inequalities (on 10.195.8.46) ...
11:27:19 Running LLL_Factorization (on 10.195.8.46) ...
11:27:23 Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
11:27:23 LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
11:27:23 LLL_Factorization: theory LLL_Factorization.Sub_Sums
11:27:23 Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
11:27:23 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
11:27:24 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
11:27:26 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
11:27:26 Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
11:27:26 Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
11:27:27 Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
11:27:31 LLL_Factorization: theory LLL_Factorization.LLL_Factorization
11:27:35 Linear_Inequalities: theory Linear_Inequalities.Cone
11:27:38 Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
11:27:40 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
11:27:45 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
11:27:54 Linear_Inequalities: theory Linear_Inequalities.Dim_Span
11:27:54 Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
11:27:57 Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
11:27:59 Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
11:27:59 Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
11:28:01 Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
11:28:06 Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
11:28:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
11:28:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
11:28:09 Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
11:28:18 Timing MDP-Algorithms (2 threads, 1146.844s elapsed time, 2004.346s cpu time, 625.772s GC time, factor 1.75)
11:28:18 Finished MDP-Algorithms (0:19:15 elapsed time, 0:33:38 cpu time, factor 1.75)
11:28:19 Timing CAVA_LTL_Modelchecker (2 threads, 442.404s elapsed time, 555.541s cpu time, 40.031s GC time, factor 1.26)
11:28:19 Finished CAVA_LTL_Modelchecker (0:07:28 elapsed time, 0:09:22 cpu time, factor 1.26)
11:28:31 Timing LLL_Factorization (2 threads, 67.731s elapsed time, 128.990s cpu time, 9.542s GC time, factor 1.90)
11:28:31 Finished LLL_Factorization (0:01:11 elapsed time, 0:02:13 cpu time, factor 1.85)
11:28:44 Timing Algebraic_Numbers (2 threads, 316.024s elapsed time, 543.103s cpu time, 37.914s GC time, factor 1.72)
11:28:44 Finished Algebraic_Numbers (0:06:03 elapsed time, 0:10:04 cpu time, factor 1.66)
11:28:55 Running Quantifier_Elimination_Hybrid (on 10.195.7.194) ...
11:28:55 Running BenOr_Kozen_Reif (on 10.195.7.194) ...
11:28:55 Running Factor_Algebraic_Polynomial (on 10.195.7.194) ...
11:28:55 Running Cubic_Quartic_Equations (on 10.195.7.194) ...
11:28:59 BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc
11:28:59 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix
11:28:59 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
11:28:59 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
11:28:59 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
11:28:59 Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
11:29:00 BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski
11:29:00 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
11:29:00 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
11:29:00 Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
11:29:01 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
11:29:01 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
11:29:01 Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
11:29:01 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux
11:29:01 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type
11:29:01 Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
11:29:02 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
11:29:02 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator
11:29:02 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
11:29:02 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
11:29:02 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
11:29:02 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
11:29:02 Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules
11:29:02 Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots
11:29:03 Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type
11:29:03 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
11:29:03 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
11:29:04 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
11:29:04 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta
11:29:04 Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map
11:29:04 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate
11:29:04 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
11:29:04 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm
11:29:04 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
11:29:05 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials
11:29:05 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc
11:29:06 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski
11:29:06 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
11:29:06 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
11:29:07 Timing Linear_Inequalities (2 threads, 73.037s elapsed time, 131.564s cpu time, 10.681s GC time, factor 1.80)
11:29:07 Finished Linear_Inequalities (0:01:48 elapsed time, 0:02:56 cpu time, factor 1.63)
11:29:07 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs
11:29:07 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
11:29:08 Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
11:29:08 Factor_Algebraic_Polynomial: theory Polynomials.Utils
11:29:09 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
11:29:09 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm
11:29:09 Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
11:29:09 Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates
11:29:09 Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
11:29:09 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs
11:29:09 Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
11:29:10 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence
11:29:10 Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
11:29:10 Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials
11:29:10 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision
11:29:11 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
11:29:11 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix
11:29:13 Running LP_Duality (on 10.195.8.42) ...
11:29:16 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm
11:29:17 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
11:29:17 Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials
11:29:18 LP_Duality: theory LP_Duality.Minimum_Maximum
11:29:18 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
11:29:18 LP_Duality: theory LP_Duality.LP_Duality
11:29:18 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm
11:29:19 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs
11:29:19 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision
11:29:20 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences
11:29:20 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements
11:29:20 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs
11:29:20 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum
11:29:21 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full
11:29:22 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences
11:29:22 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision
11:29:22 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations
11:29:23 Quantifier_Elimination_Hybrid: theory Polynomials.Utils
11:29:23 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders
11:29:24 Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products
11:29:26 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
11:29:27 Timing LP_Duality (2 threads, 8.822s elapsed time, 11.238s cpu time, 0.408s GC time, factor 1.27)
11:29:27 Finished LP_Duality (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.17)
11:29:28 Timing Cubic_Quartic_Equations (2 threads, 27.145s elapsed time, 40.265s cpu time, 3.475s GC time, factor 1.48)
11:29:28 Finished Cubic_Quartic_Equations (0:00:31 elapsed time, 0:00:44 cpu time, factor 1.41)
11:29:29 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision
11:29:29 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
11:29:29 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
11:29:30 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
11:29:31 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
11:29:32 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified
11:29:38 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class
11:29:42 Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection
11:29:42 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered
11:29:44 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
11:29:47 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
11:29:48 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
11:29:50 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
11:29:53 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
11:29:53 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
11:29:56 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
11:29:56 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
11:30:00 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap
11:30:03 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension
11:30:03 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE
11:30:04 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps
11:30:06 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms
11:30:06 Timing Smith_Normal_Form (2 threads, 1078.355s elapsed time, 1876.095s cpu time, 583.513s GC time, factor 1.74)
11:30:06 Finished Smith_Normal_Form (0:19:01 elapsed time, 0:32:42 cpu time, factor 1.72)
11:30:09 Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.8.32) ...
11:30:12 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn
11:30:13 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting
11:30:14 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations
11:30:15 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex
11:30:16 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms
11:30:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
11:30:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
11:30:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
11:30:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
11:30:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
11:30:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
11:30:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
11:30:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
11:30:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
11:30:22 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs
11:30:22 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
11:30:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
11:30:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
11:30:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
11:30:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
11:30:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
11:30:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
11:30:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
11:30:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
11:30:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
11:30:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
11:30:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
11:30:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
11:30:30 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF
11:30:30 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic
11:30:30 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase
11:30:30 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity
11:30:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
11:30:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
11:30:31 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase
11:30:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable
11:30:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
11:30:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind
11:30:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS
11:30:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals
11:30:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
11:30:33 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni
11:30:34 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni
11:30:35 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni
11:30:36 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs
11:30:37 Timing Factor_Algebraic_Polynomial (2 threads, 94.479s elapsed time, 168.189s cpu time, 13.833s GC time, factor 1.78)
11:30:37 Finished Factor_Algebraic_Polynomial (0:01:39 elapsed time, 0:02:54 cpu time, factor 1.75)
11:30:37 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports
11:30:38 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad
11:30:39 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props
11:30:41 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments
11:30:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
11:30:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
11:30:42 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence
11:30:43 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs
11:30:43 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
11:30:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
11:30:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
11:30:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
11:30:44 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs
11:30:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
11:30:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
11:30:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
11:30:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
11:30:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
11:30:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
11:30:49 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
11:30:49 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
11:30:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
11:31:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
11:31:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
11:31:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
11:31:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
11:31:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
11:31:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
11:31:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
11:31:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
11:31:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
11:31:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
11:31:05 Timing Linear_Recurrences_Solver (2 threads, 496.358s elapsed time, 869.104s cpu time, 68.023s GC time, factor 1.75)
11:31:05 Finished Linear_Recurrences_Solver (0:08:23 elapsed time, 0:14:39 cpu time, factor 1.75)
11:31:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
11:31:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
11:31:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
11:31:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
11:31:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
11:31:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
11:31:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
11:31:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
11:31:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
11:31:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
11:31:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
11:31:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
11:31:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
11:31:32 Timing Constructive_Cryptography_CM (2 threads, 694.779s elapsed time, 1254.847s cpu time, 175.824s GC time, factor 1.81)
11:31:32 Finished Constructive_Cryptography_CM (0:11:41 elapsed time, 0:21:05 cpu time, factor 1.80)
11:31:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
11:31:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
11:31:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
11:31:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
11:31:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
11:31:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
11:31:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
11:31:49 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
11:31:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
11:31:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
11:31:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
11:31:56 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
11:31:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
11:31:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
11:31:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
11:32:00 Timing BenOr_Kozen_Reif (2 threads, 177.890s elapsed time, 277.763s cpu time, 22.575s GC time, factor 1.56)
11:32:00 Finished BenOr_Kozen_Reif (0:03:03 elapsed time, 0:04:43 cpu time, factor 1.55)
11:32:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
11:32:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
11:32:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
11:32:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
11:32:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
11:32:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
11:32:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
11:32:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
11:32:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
11:32:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
11:32:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
11:32:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
11:33:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
11:33:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
11:33:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
11:33:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
11:33:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
11:33:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
11:33:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
11:33:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
11:33:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
11:33:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
11:33:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
11:33:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
11:33:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
11:33:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
11:33:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
11:33:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
11:33:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
11:33:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
11:33:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
11:33:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
11:33:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
11:33:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
11:33:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
11:33:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
11:33:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
11:33:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:33:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
11:33:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
11:33:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
11:33:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
11:33:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
11:34:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
11:34:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
11:34:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
11:34:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
11:34:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
11:34:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
11:34:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
11:34:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
11:34:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
11:34:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
11:34:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
11:34:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
11:35:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
11:35:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
11:36:40 Timing Automated_Stateful_Protocol_Verification (2 threads, 2174.033s elapsed time, 4115.722s cpu time, 2425.317s GC time, factor 1.89)
11:36:40 Finished Automated_Stateful_Protocol_Verification (0:36:27 elapsed time, 1:09:00 cpu time, factor 1.89)
11:37:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
11:37:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
11:38:11 Timing Expander_Graphs (2 threads, 793.274s elapsed time, 1436.881s cpu time, 257.266s GC time, factor 1.81)
11:38:11 Finished Expander_Graphs (0:14:42 elapsed time, 0:25:56 cpu time, factor 1.76)
11:38:11 Running Distributed_Distinct_Elements (on 10.195.8.29) ...
11:38:18 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
11:38:18 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
11:38:18 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
11:38:18 Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
11:38:19 Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
11:38:19 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
11:38:20 Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
11:38:20 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
11:38:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
11:38:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
11:38:25 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
11:38:27 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
11:38:27 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
11:38:27 Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
11:38:28 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
11:38:28 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
11:38:34 Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
11:38:34 Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
11:38:34 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
11:38:36 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
11:38:41 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
11:38:42 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
11:38:42 Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
11:38:43 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
11:38:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
11:38:47 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
11:38:48 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
11:38:59 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
11:39:00 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
11:39:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
11:39:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
11:39:10 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
11:39:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
11:39:13 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
11:39:16 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
11:39:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
11:39:21 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
11:39:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
11:40:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
11:41:19 Timing Distributed_Distinct_Elements (2 threads, 180.184s elapsed time, 342.657s cpu time, 72.070s GC time, factor 1.90)
11:41:19 Finished Distributed_Distinct_Elements (0:03:05 elapsed time, 0:05:49 cpu time, factor 1.88)
11:45:47 Timing Quantifier_Elimination_Hybrid (2 threads, 996.217s elapsed time, 1732.809s cpu time, 382.927s GC time, factor 1.74)
11:45:47 Finished Quantifier_Elimination_Hybrid (0:16:46 elapsed time, 0:29:08 cpu time, factor 1.74)
11:47:03 Timing HOL-ODE-Numerics (2 threads, 2120.258s elapsed time, 3899.947s cpu time, 484.947s GC time, factor 1.84)
11:47:03 Finished HOL-ODE-Numerics (0:37:53 elapsed time, 1:08:29 cpu time, factor 1.81)
11:47:03 Building Lorenz_Approximation (on 10.195.7.194) ...
11:47:03 Running HOL-ODE-ARCH-COMP (on 10.195.7.194) ...
11:47:03 Running HOL-ODE-Examples (on 10.195.7.194) ...
11:47:04 Running Poincare_Bendixson (on 10.195.7.194) ...
11:47:07 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
11:47:07 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
11:47:09 Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
11:47:09 Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
11:47:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
11:47:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
11:47:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
11:47:10 Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
11:47:14 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
11:47:15 Poincare_Bendixson: theory Poincare_Bendixson.Invariance
11:47:17 Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
11:47:20 Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
11:47:21 Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
11:47:26 Poincare_Bendixson: theory Poincare_Bendixson.Examples
11:47:36 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
11:48:34 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
11:49:28 Timing Poincare_Bendixson (2 threads, 137.989s elapsed time, 210.896s cpu time, 14.862s GC time, factor 1.53)
11:49:28 Finished Poincare_Bendixson (0:02:23 elapsed time, 0:03:36 cpu time, factor 1.51)
11:51:09 Timing Crypto_Standards (2 threads, 3529.890s elapsed time, 6712.951s cpu time, 1487.190s GC time, factor 1.90)
11:51:09 Finished Crypto_Standards (0:59:00 elapsed time, 1:52:12 cpu time, factor 1.90)
11:53:06 Timing HOL-ODE-Examples (2 threads, 356.390s elapsed time, 623.084s cpu time, 29.759s GC time, factor 1.75)
11:53:06 Finished HOL-ODE-Examples (0:06:01 elapsed time, 0:10:28 cpu time, factor 1.74)
11:53:07 Timing Lorenz_Approximation (2 threads, 304.740s elapsed time, 566.918s cpu time, 76.895s GC time, factor 1.86)
11:53:07 Finished Lorenz_Approximation (0:06:02 elapsed time, 0:10:44 cpu time, factor 1.78)
11:53:25 Running Lorenz_C0 (on 10.195.8.40) ...
11:53:25 Running Lorenz_C1 (on 10.195.8.40) ...
11:53:29 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
11:53:29 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
11:53:31 Timing Lorenz_C1 (2 threads, 1.929s elapsed time, 2.606s cpu time, 0.061s GC time, factor 1.35)
11:53:31 Finished Lorenz_C1 (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.08)
11:54:31 Timing HOL-ODE-ARCH-COMP (2 threads, 442.608s elapsed time, 849.476s cpu time, 77.426s GC time, factor 1.92)
11:54:31 Finished HOL-ODE-ARCH-COMP (0:07:27 elapsed time, 0:14:14 cpu time, factor 1.91)
12:14:32 Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2647.355s elapsed time, 4837.838s cpu time, 1516.568s GC time, factor 1.83)
12:14:32 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:44:16 elapsed time, 1:20:52 cpu time, factor 1.83)
12:19:24 Timing Lorenz_C0 (2 threads, 1554.108s elapsed time, 3046.798s cpu time, 80.378s GC time, factor 1.96)
12:19:24 Finished Lorenz_C0 (0:25:58 elapsed time, 0:50:51 cpu time, factor 1.96)
12:33:47 Timing CZH_Universal_Constructions (2 threads, 4411.921s elapsed time, 7234.685s cpu time, 2668.172s GC time, factor 1.64)
12:33:47 Finished CZH_Universal_Constructions (1:13:37 elapsed time, 2:00:42 cpu time, factor 1.64)
12:33:58 
12:33:58 Finished at Mon Dec 4 12:33:58 GMT+1 2023
12:33:58 2:12:20 elapsed time, 58:37:37 cpu time, factor 26.58
12:33:59 Started calculate disk usage of build
12:33:59 Finished Calculation of disk usage of build in 0 seconds
12:34:15 Started calculate disk usage of workspace
12:34:16 Finished Calculation of disk usage of workspace in 0 seconds
12:34:16 Finished: SUCCESS