Skipping 871 KB.. Full Log

Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_SPMF
13:45:43 Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Dice_Roll
13:45:44 Frequency_Moments: theory Lp.Lp
13:45:45 Executable_Randomized_Algorithms: theory MFMC_Countable.Rel_PMF_Characterisation
13:45:45 Executable_Randomized_Algorithms: theory Probabilistic_While.While_SPMF
13:45:45 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
13:45:45 Frequency_Moments: theory Lehmer.Lehmer
13:45:46 Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
13:45:46 Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
13:45:46 Schwartz_Zippel: theory Regular-Sets.Regular_Exp
13:45:47 Projective_Measurements: theory Regular-Sets.Regular_Exp
13:45:48 Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof
13:45:48 Executable_Randomized_Algorithms: theory Probabilistic_While.Geometric
13:45:48 Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Basic_Randomized_Algorithms
13:45:49 Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary
13:45:49 Frequency_Moments: theory Bertrands_Postulate.Bertrand
13:45:50 Schwartz_Zippel: theory Regular-Sets.NDerivative
13:45:50 Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
13:45:51 Projective_Measurements: theory Regular-Sets.NDerivative
13:45:52 Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
13:45:52 Projective_Measurements: theory Regular-Sets.Relation_Interpretation
13:45:52 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
13:45:54 Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
13:45:55 Schwartz_Zippel: theory Regular-Sets.Regexp_Method
13:45:55 Projective_Measurements: theory Regular-Sets.Equivalence_Checking
13:45:55 Projective_Measurements: theory Regular-Sets.Regexp_Method
13:45:56 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
13:45:56 Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
13:45:57 Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
13:45:58 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
13:45:58 Projective_Measurements: theory Abstract-Rewriting.SN_Orders
13:45:59 Schwartz_Zippel: theory Polynomials.Utils
13:45:59 Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
13:45:59 Schwartz_Zippel: theory Polynomials.Power_Products
13:46:05 Timing Balog_Szemeredi_Gowers (6 threads, 135.752s elapsed time, 268.718s cpu time, 28.424s GC time, factor 1.98)
13:46:05 Finished Balog_Szemeredi_Gowers (0:02:17 elapsed time, 0:04:32 cpu time, factor 1.98)
13:46:05 Timing MDP-Rewards (2 threads, 40.088s elapsed time, 60.134s cpu time, 1.983s GC time, factor 1.50)
13:46:05 Finished MDP-Rewards (0:02:23 elapsed time, 0:01:35 cpu time, factor 0.66)
13:46:05 Projective_Measurements: theory Matrix.Ordered_Semiring
13:46:05 Projective_Measurements: theory Matrix.Matrix_Legacy
13:46:06 Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
13:46:07 Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
13:46:08 Timing Probabilistic_While (6 threads, 121.621s elapsed time, 53.287s cpu time, 1.913s GC time, factor 0.44)
13:46:08 Finished Probabilistic_While (0:02:20 elapsed time, 0:01:18 cpu time, factor 0.56)
13:46:09 Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
13:46:09 Timing Universal_Hash_Families (6 threads, 134.759s elapsed time, 277.806s cpu time, 57.255s GC time, factor 2.06)
13:46:09 Finished Universal_Hash_Families (0:02:22 elapsed time, 0:04:58 cpu time, factor 2.10)
13:46:09 Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
13:46:15 Projective_Measurements: theory Projective_Measurements.Projective_Measurements
13:46:16 Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
13:46:16 Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
13:46:17 Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
13:46:17 Timing Echelon_Form (2 threads, 398.886s elapsed time, 692.521s cpu time, 43.161s GC time, factor 1.74)
13:46:17 Finished Echelon_Form (0:08:00 elapsed time, 0:12:24 cpu time, factor 1.55)
13:46:22 Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
13:46:22 Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
13:46:23 Timing Ordinary_Differential_Equations (2 threads, 382.276s elapsed time, 590.566s cpu time, 74.348s GC time, factor 1.54)
13:46:23 Finished Ordinary_Differential_Equations (0:08:04 elapsed time, 0:10:48 cpu time, factor 1.34)
13:46:24 Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
13:46:54 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
13:46:54 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
13:46:55 Timing Executable_Randomized_Algorithms (6 threads, 184.927s elapsed time, 515.037s cpu time, 138.117s GC time, factor 2.79)
13:46:55 Finished Executable_Randomized_Algorithms (0:03:07 elapsed time, 0:08:39 cpu time, factor 2.78)
13:46:58 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
13:47:00 Timing Hybrid_Systems_VCs (2 threads, 479.984s elapsed time, 736.713s cpu time, 54.200s GC time, factor 1.53)
13:47:00 Finished Hybrid_Systems_VCs (0:08:05 elapsed time, 0:12:24 cpu time, factor 1.53)
13:47:02 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
13:47:02 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
13:47:03 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
13:47:04 Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
13:47:06 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
13:47:06 Timing Count_Complex_Roots (2 threads, 214.225s elapsed time, 363.885s cpu time, 24.884s GC time, factor 1.70)
13:47:06 Finished Count_Complex_Roots (0:04:18 elapsed time, 0:06:59 cpu time, factor 1.62)
13:47:07 Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
13:47:14 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
13:47:15 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
13:47:16 Frequency_Moments: theory Frequency_Moments.K_Smallest
13:47:16 Frequency_Moments: theory Frequency_Moments.Probability_Ext
13:47:20 Timing Complex_Bounded_Operators (2 threads, 259.356s elapsed time, 448.305s cpu time, 43.849s GC time, factor 1.73)
13:47:20 Finished Complex_Bounded_Operators (0:05:04 elapsed time, 0:08:24 cpu time, factor 1.66)
13:47:23 Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
13:47:24 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
13:47:29 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
13:47:37 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
13:47:43 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
13:47:43 Timing Bernoulli (2 threads, 249.191s elapsed time, 353.220s cpu time, 26.766s GC time, factor 1.42)
13:47:43 Finished Bernoulli (0:04:55 elapsed time, 0:06:52 cpu time, factor 1.39)
13:47:44 Timing E_Transcendental (2 threads, 241.738s elapsed time, 334.312s cpu time, 36.542s GC time, factor 1.38)
13:47:44 Finished E_Transcendental (0:04:53 elapsed time, 0:06:37 cpu time, factor 1.36)
13:47:55 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
13:47:59 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
13:48:01 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
13:48:03 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
13:48:04 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
13:48:04 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
13:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
13:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
13:48:06 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
13:48:07 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
13:48:07 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
13:48:10 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
13:49:05 Timing MonoidalCategory (2 threads, 487.426s elapsed time, 867.659s cpu time, 170.400s GC time, factor 1.78)
13:49:05 Finished MonoidalCategory (0:08:11 elapsed time, 0:14:33 cpu time, factor 1.78)
13:49:14 Timing Schwartz_Zippel (2 threads, 319.209s elapsed time, 500.447s cpu time, 44.883s GC time, factor 1.57)
13:49:14 Finished Schwartz_Zippel (0:05:24 elapsed time, 0:08:28 cpu time, factor 1.57)
13:49:40 Timing Dirichlet_Series (2 threads, 372.583s elapsed time, 582.066s cpu time, 130.434s GC time, factor 1.56)
13:49:40 Finished Dirichlet_Series (0:06:54 elapsed time, 0:10:37 cpu time, factor 1.54)
13:50:04 Timing Transcendence_Series_Hancl_Rucki (2 threads, 435.024s elapsed time, 700.716s cpu time, 141.347s GC time, factor 1.61)
13:50:04 Finished Transcendence_Series_Hancl_Rucki (0:07:19 elapsed time, 0:11:47 cpu time, factor 1.61)
13:50:22 Timing Deep_Learning (2 threads, 387.259s elapsed time, 686.692s cpu time, 151.782s GC time, factor 1.77)
13:50:22 Finished Deep_Learning (0:06:32 elapsed time, 0:11:33 cpu time, factor 1.77)
13:52:06 Timing Virtual_Substitution (2 threads, 786.195s elapsed time, 1330.676s cpu time, 370.391s GC time, factor 1.69)
13:52:06 Finished Virtual_Substitution (0:13:13 elapsed time, 0:22:23 cpu time, factor 1.69)
13:56:09 Timing Probabilistic_Prime_Tests (2 threads, 714.002s elapsed time, 1340.293s cpu time, 514.512s GC time, factor 1.88)
13:56:09 Finished Probabilistic_Prime_Tests (0:12:24 elapsed time, 0:23:13 cpu time, factor 1.87)
13:58:09 Timing Three_Squares (2 threads, 865.209s elapsed time, 1502.498s cpu time, 422.825s GC time, factor 1.74)
13:58:09 Finished Three_Squares (0:15:20 elapsed time, 0:26:19 cpu time, factor 1.72)
13:58:28 Timing Projective_Measurements (2 threads, 810.137s elapsed time, 1345.456s cpu time, 372.438s GC time, factor 1.66)
13:58:28 Finished Projective_Measurements (0:14:38 elapsed time, 0:23:54 cpu time, factor 1.63)
13:59:54 Timing Frequency_Moments (2 threads, 887.875s elapsed time, 1630.436s cpu time, 547.591s GC time, factor 1.84)
13:59:54 Finished Frequency_Moments (0:16:07 elapsed time, 0:29:05 cpu time, factor 1.80)
14:01:40 Estimated 0:17:01 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.442s)
14:01:41 Running Linear_Recurrences_Solver (on of1-proof+8-15) ...
14:01:42 Running Differential_Dynamic_Logic (on of1-proof+0-7) ...
14:01:43 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
14:01:43 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
14:01:43 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
14:01:44 Building Hermite (on 10.195.8.30) ...
14:01:46 Linear_Recurrences_Solver: theory Pure-ex.Guess
14:01:46 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
14:01:46 Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
14:01:46 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
14:01:46 Linear_Recurrences_Solver: theory Deriving.Compare_Real
14:01:46 Linear_Recurrences_Solver: theory Polynomials.More_Modules
14:01:46 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
14:01:46 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
14:01:46 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
14:01:46 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
14:01:46 Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
14:01:46 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
14:01:46 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
14:01:46 Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
14:01:46 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
14:01:47 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
14:01:47 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
14:01:47 Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
14:01:47 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
14:01:47 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
14:01:47 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
14:01:47 Linear_Recurrences_Solver: theory Show.Show_Real
14:01:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
14:01:47 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
14:01:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
14:01:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
14:01:47 Linear_Recurrences_Solver: theory Show.Show_Complex
14:01:47 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
14:01:48 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
14:01:48 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
14:01:48 Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
14:01:48 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
14:01:48 Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
14:01:48 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
14:01:48 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
14:01:48 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
14:01:48 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
14:01:49 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
14:01:49 Building HOL-ODE-Numerics (on 10.195.8.30) ...
14:01:49 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
14:01:49 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
14:01:49 Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
14:01:50 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
14:01:50 Linear_Recurrences_Solver: theory Polynomials.Utils
14:01:50 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
14:01:50 Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
14:01:50 Linear_Recurrences_Solver: theory Polynomials.Power_Products
14:01:50 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
14:01:51 Running MDP-Algorithms (on 10.195.8.30) ...
14:01:51 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
14:01:52 Hermite: theory Hermite.Hermite
14:01:52 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
14:01:52 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
14:01:52 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
14:01:52 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
14:01:53 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
14:01:53 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
14:01:54 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
14:01:54 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
14:01:54 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
14:01:54 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
14:01:54 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
14:01:54 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
14:01:55 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
14:01:55 HOL-ODE-Numerics: theory Deriving.Comparator
14:01:55 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
14:01:55 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
14:01:55 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
14:01:55 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
14:01:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
14:01:55 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
14:01:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
14:01:56 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
14:01:56 HOL-ODE-Numerics: theory Deriving.Compare
14:01:56 HOL-ODE-Numerics: theory Deriving.Derive_Manager
14:01:56 HOL-ODE-Numerics: theory Deriving.Generator_Aux
14:01:56 Building Expander_Graphs (on 10.195.8.30) ...
14:01:57 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
14:01:57 HOL-ODE-Numerics: theory Deriving.Equality_Generator
14:01:58 Hermite: theory Hermite.Hermite_IArrays
14:01:58 HOL-ODE-Numerics: theory Deriving.Compare_Generator
14:01:58 Building CryptHOL (on 10.195.8.30) ...
14:01:58 HOL-ODE-Numerics: theory Deriving.Equality_Instances
14:01:58 HOL-ODE-Numerics: theory HOL-Library.AList
14:01:59 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
14:01:59 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
14:01:59 HOL-ODE-Numerics: theory HOL-ex.Quicksort
14:02:00 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
14:02:01 MDP-Algorithms: theory HOL-Eisbach.Eisbach
14:02:01 MDP-Algorithms: theory Containers.Equal
14:02:01 HOL-ODE-Numerics: theory HOL-Library.Char_ord
14:02:01 MDP-Algorithms: theory Containers.Closure_Set
14:02:01 HOL-ODE-Numerics: theory Deriving.Compare_Instances
14:02:01 MDP-Algorithms: theory Containers.Extend_Partial_Order
14:02:01 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
14:02:01 HOL-ODE-Numerics: theory HOL-Library.Mapping
14:02:01 MDP-Algorithms: theory Containers.List_Fusion
14:02:01 HOL-ODE-Numerics: theory HOL-Library.Option_ord
14:02:01 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
14:02:02 MDP-Algorithms: theory Deriving.Comparator
14:02:02 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
14:02:02 CryptHOL: theory HOL-Eisbach.Eisbach
14:02:02 CryptHOL: theory Applicative_Lifting.Applicative
14:02:03 MDP-Algorithms: theory Deriving.Derive_Manager
14:02:03 HOL-ODE-Numerics: theory HOL-Library.Parallel
14:02:03 MDP-Algorithms: theory Deriving.Generator_Aux
14:02:03 MDP-Algorithms: theory Deriving.Equality_Generator
14:02:03 MDP-Algorithms: theory Deriving.Compare
14:02:03 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
14:02:03 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
14:02:03 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
14:02:03 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
14:02:04 MDP-Algorithms: theory Deriving.Comparator_Generator
14:02:04 Building LLL_Basis_Reduction (on 10.195.8.49) ...
14:02:04 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
14:02:04 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
14:02:04 HOL-ODE-Numerics: theory HOL-Library.Type_Length
14:02:04 MDP-Algorithms: theory Deriving.Equality_Instances
14:02:04 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
14:02:04 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
14:02:05 Building Algebraic_Numbers (on 10.195.8.49) ...
14:02:05 CryptHOL: theory CryptHOL.Partial_Function_Set
14:02:05 Running CVP_Hardness (on 10.195.8.49) ...
14:02:05 Expander_Graphs: theory Graph_Theory.Rtrancl_On
14:02:05 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
14:02:05 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
14:02:06 Building Zeta_Function (on 10.195.8.49) ...
14:02:06 Running Fishers_Inequality (on 10.195.8.49) ...
14:02:06 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
14:02:06 MDP-Algorithms: theory Deriving.Compare_Generator
14:02:06 MDP-Algorithms: theory HOL-Computational_Algebra.Fraction_Field
14:02:06 HOL-ODE-Numerics: theory HOL-Library.Word
14:02:06 MDP-Algorithms: theory HOL-Data_Structures.Array_Specs
14:02:06 MDP-Algorithms: theory HOL-Data_Structures.Cmp
14:02:06 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
14:02:06 MDP-Algorithms: theory HOL-Data_Structures.Less_False
14:02:07 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
14:02:07 MDP-Algorithms: theory HOL-Data_Structures.Sorted_Less
14:02:07 MDP-Algorithms: theory HOL-Data_Structures.AList_Upd_Del
14:02:07 CryptHOL: theory HOL-Library.Case_Converter
14:02:07 CryptHOL: theory Applicative_Lifting.Applicative_Environment
14:02:07 CryptHOL: theory CryptHOL.Environment_Functor
14:02:07 MDP-Algorithms: theory HOL-Data_Structures.Map_Specs
14:02:08 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
14:02:08 MDP-Algorithms: theory HOL-Data_Structures.List_Ins_Del
14:02:08 MDP-Algorithms: theory Containers.Containers_Auxiliary
14:02:08 CryptHOL: theory Applicative_Lifting.Applicative_Set
14:02:08 CryptHOL: theory HOL-Library.Simps_Case_Conv
14:02:08 CryptHOL: theory HOL-Algebra.Congruence
14:02:08 CryptHOL: theory CryptHOL.Set_Applicative
14:02:08 CryptHOL: theory HOL-Library.Function_Algebras
14:02:08 MDP-Algorithms: theory HOL-Data_Structures.Set_Specs
14:02:08 CryptHOL: theory HOL-Library.Type_Length
14:02:08 MDP-Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
14:02:08 MDP-Algorithms: theory HOL-Library.Char_ord
14:02:09 MDP-Algorithms: theory Containers.Lexicographic_Order
14:02:09 CryptHOL: theory HOL-Algebra.Order
14:02:09 Zeta_Function: theory Bernoulli.Bernoulli_Zeta
14:02:09 CryptHOL: theory HOL-Library.Countable_Set_Type
14:02:09 Expander_Graphs: theory Abstract-Rewriting.Seq
14:02:09 CVP_Hardness: theory CVP_Hardness.Digits_int
14:02:09 CVP_Hardness: theory CVP_Hardness.Reduction
14:02:09 CVP_Hardness: theory CVP_Hardness.Partition
14:02:09 Fishers_Inequality: theory Card_Partitions.Set_Partition
14:02:09 Fishers_Inequality: theory Polynomials.MPoly_Type
14:02:09 CVP_Hardness: theory CVP_Hardness.Subset_Sum
14:02:09 MDP-Algorithms: theory Deriving.Compare_Instances
14:02:10 MDP-Algorithms: theory HOL-Library.Code_Abstract_Nat
14:02:10 Expander_Graphs: theory HOL-Library.More_List
14:02:10 MDP-Algorithms: theory HOL-Library.Code_Target_Nat
14:02:10 CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
14:02:10 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
14:02:10 MDP-Algorithms: theory HOL-Library.Code_Target_Int
14:02:10 MDP-Algorithms: theory HOL-Algebra.Congruence
14:02:10 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
14:02:10 CryptHOL: theory HOL-Algebra.Lattice
14:02:10 Expander_Graphs: theory HOL-Library.While_Combinator
14:02:10 MDP-Algorithms: theory HOL-Library.Code_Target_Numeral
14:02:10 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Misc
14:02:11 MDP-Algorithms: theory HOL-Library.IArray
14:02:11 Fishers_Inequality: theory Polynomials.More_MPoly_Type
14:02:11 CryptHOL: theory HOL-Algebra.Complete_Lattice
14:02:11 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
14:02:11 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
14:02:11 CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
14:02:11 Running CRYSTALS-Kyber (on 10.195.8.29) ...
14:02:11 Fishers_Inequality: theory Polynomials.More_Modules
14:02:11 CryptHOL: theory Coinductive.Coinductive_Nat
14:02:11 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
14:02:11 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
14:02:11 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
14:02:12 Fishers_Inequality: theory Design_Theory.Multisets_Extras
14:02:12 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
14:02:12 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
14:02:12 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
14:02:12 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
14:02:12 MDP-Algorithms: theory HOL-Algebra.Order
14:02:12 CryptHOL: theory HOL-Algebra.Group
14:02:13 Running MFMC_Countable (on 10.195.8.29) ...
14:02:13 Fishers_Inequality: theory List-Index.List_Index
14:02:13 Fishers_Inequality: theory Design_Theory.Design_Basics
14:02:13 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
14:02:14 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
14:02:14 MDP-Algorithms: theory HOL-Library.More_List
14:02:14 CryptHOL: theory Coinductive.Coinductive_List
14:02:14 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
14:02:14 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
14:02:14 CVP_Hardness: theory Algebraic_Numbers.Resultant
14:02:14 MDP-Algorithms: theory Containers.Containers_Generator
14:02:14 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
14:02:14 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
14:02:14 MDP-Algorithms: theory HOL-Algebra.Lattice
14:02:14 Building Markov_Models (on 10.195.8.29) ...
14:02:14 Running Turans_Graph_Theorem (on 10.195.8.29) ...
14:02:14 MDP-Algorithms: theory Containers.Collection_Enum
14:02:14 Running DiscretePricing (on 10.195.8.29) ...
14:02:14 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
14:02:14 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
14:02:14 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
14:02:14 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
14:02:14 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
14:02:15 Fishers_Inequality: theory Design_Theory.Design_Operations
14:02:15 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
14:02:15 MDP-Algorithms: theory HOL-Algebra.Complete_Lattice
14:02:15 MDP-Algorithms: theory Containers.Collection_Eq
14:02:15 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
14:02:16 Zeta_Function: theory HOL-Eisbach.Eisbach
14:02:16 Zeta_Function: theory Pure-ex.Guess
14:02:16 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
14:02:16 CVP_Hardness: theory CVP_Hardness.Lattice_int
14:02:16 Algebraic_Numbers: theory Pure-ex.Guess
14:02:16 Algebraic_Numbers: theory Deriving.Compare_Rat
14:02:16 Running Actuarial_Mathematics (on 10.195.7.194) ...
14:02:16 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
14:02:17 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
14:02:17 Fishers_Inequality: theory Design_Theory.Block_Designs
14:02:17 CryptHOL: theory HOL-Algebra.Coset
14:02:17 Algebraic_Numbers: theory Deriving.Compare_Real
14:02:17 CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes
14:02:17 Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
14:02:17 CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp
14:02:17 CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
14:02:17 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
14:02:17 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
14:02:17 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
14:02:17 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
14:02:18 MDP-Algorithms: theory Containers.DList_Set
14:02:18 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
14:02:18 DiscretePricing: theory DiscretePricing.Filtration
14:02:18 MFMC_Countable: theory Flow_Networks.Graph
14:02:18 DiscretePricing: theory DiscretePricing.Generated_Subalgebra
14:02:18 Turans_Graph_Theorem: theory HOL-Decision_Procs.Dense_Linear_Order
14:02:18 MFMC_Countable: theory HOL-Library.Case_Converter
14:02:18 Turans_Graph_Theorem: theory HOL-Library.Code_Abstract_Nat
14:02:18 Markov_Models: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
14:02:18 Markov_Models: theory HOL-Computational_Algebra.Group_Closure
14:02:18 CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product
14:02:18 CVP_Hardness: theory CVP_Hardness.CVP_p
14:02:18 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Nat
14:02:18 MDP-Algorithms: theory HOL-Algebra.Group
14:02:18 CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm
14:02:19 Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
14:02:19 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Int
14:02:19 Zeta_Function: theory Sturm_Tarski.PolyMisc
14:02:19 Markov_Models: theory HOL-Library.Case_Converter
14:02:19 CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector
14:02:19 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
14:02:19 Zeta_Function: theory Winding_Number_Eval.Missing_Topology
14:02:19 Running Gauss_Sums (on 10.195.7.194) ...
14:02:19 Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
14:02:19 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
14:02:19 Zeta_Function: theory Zeta_Function.Zeta_Library
14:02:19 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
14:02:19 Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
14:02:19 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
14:02:19 MDP-Algorithms: theory Containers.Set_Linorder
14:02:19 MFMC_Countable: theory HOL-Library.Simps_Case_Conv
14:02:19 MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
14:02:19 DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
14:02:19 MFMC_Countable: theory HOL-Library.While_Combinator
14:02:20 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral
14:02:20 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
14:02:20 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
14:02:20 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
14:02:20 Turans_Graph_Theorem: theory HOL-Library.Lattice_Algebras
14:02:20 CRYSTALS-Kyber: theory HOL-Number_Theory.Fib
14:02:20 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
14:02:20 Fishers_Inequality: theory Design_Theory.BIBD
14:02:20 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
14:02:21 HOL-ODE-Numerics: theory Collections.SetIterator
14:02:21 MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
14:02:21 Markov_Models: theory HOL-Library.Simps_Case_Conv
14:02:21 Building Commuting_Hermitian (on 10.195.7.194) ...
14:02:21 Markov_Models: theory HOL-Library.Code_Abstract_Nat
14:02:21 Running Treaps (on 10.195.7.194) ...
14:02:21 Running Density_Compiler (on 10.195.7.194) ...
14:02:21 Zeta_Function: theory Budan_Fourier.BF_Misc
14:02:21 Markov_Models: theory HOL-Library.Code_Target_Int
14:02:21 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
14:02:21 Fishers_Inequality: theory Design_Theory.Sub_Designs
14:02:21 CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers
14:02:21 Markov_Models: theory HOL-Library.Code_Target_Nat
14:02:22 MDP-Algorithms: theory HOL-Algebra.Coset
14:02:22 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
14:02:22 Markov_Models: theory HOL-Library.IArray
14:02:22 Markov_Models: theory HOL-Library.Code_Target_Numeral
14:02:22 Markov_Models: theory HOL-Library.While_Combinator
14:02:22 CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space
14:02:22 Actuarial_Mathematics: theory Actuarial_Mathematics.Preliminaries
14:02:22 Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
14:02:22 DiscretePricing: theory DiscretePricing.Martingale
14:02:22 DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
14:02:22 MFMC_Countable: theory MFMC_Countable.MFMC_Misc
14:02:22 MFMC_Countable: theory Flow_Networks.Network
14:02:22 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
14:02:22 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
14:02:23 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
14:02:23 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
14:02:23 Markov_Models: theory Coinductive.Coinductive_Nat
14:02:23 CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion
14:02:23 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
14:02:23 CryptHOL: theory CryptHOL.Cyclic_Group
14:02:23 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
14:02:23 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
14:02:23 CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss
14:02:23 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
14:02:23 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
14:02:23 Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
14:02:24 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
14:02:24 CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
14:02:24 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
14:02:24 Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
14:02:24 CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity
14:02:24 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
14:02:24 MFMC_Countable: theory MFMC_Countable.MFMC_Network
14:02:24 Building Applicative_Lifting (on 10.195.8.40) ...
14:02:24 Turans_Graph_Theorem: theory HOL-Library.Log_Nat
14:02:24 MFMC_Countable: theory Flow_Networks.Residual_Graph
14:02:24 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
14:02:25 Treaps: theory HOL-Data_Structures.Cmp
14:02:25 Treaps: theory HOL-Data_Structures.Less_False
14:02:25 Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
14:02:25 Density_Compiler: theory Density_Compiler.Density_Predicates
14:02:25 Gauss_Sums: theory HOL-Algebra.QuotRing
14:02:25 Treaps: theory HOL-Data_Structures.Sorted_Less
14:02:25 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
14:02:25 Treaps: theory HOL-Data_Structures.List_Ins_Del
14:02:25 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
14:02:25 Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
14:02:25 Markov_Models: theory Coinductive.Coinductive_List
14:02:25 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
14:02:25 Actuarial_Mathematics: theory Actuarial_Mathematics.Interest
14:02:25 HOL-ODE-Numerics: theory Collections.Assoc_List
14:02:25 Treaps: theory HOL-Library.Function_Algebras
14:02:25 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
14:02:25 CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington
14:02:25 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
14:02:25 Treaps: theory Landau_Symbols.Group_Sort
14:02:25 Treaps: theory HOL-Data_Structures.Set_Specs
14:02:25 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
14:02:25 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
14:02:26 Treaps: theory HOL-Data_Structures.Tree_Set
14:02:26 CryptHOL: theory Applicative_Lifting.Applicative_PMF
14:02:26 CryptHOL: theory Coinductive.TLList
14:02:26 Expander_Graphs: theory HOL-Decision_Procs.Approximation
14:02:26 Density_Compiler: theory Density_Compiler.PDF_Transformations
14:02:26 Actuarial_Mathematics: theory Actuarial_Mathematics.Survival_Model
14:02:26 Density_Compiler: theory Density_Compiler.PDF_Values
14:02:26 HOL-ODE-Numerics: theory Collections.Diff_Array
14:02:26 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
14:02:26 CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots
14:02:26 CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product
14:02:26 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
14:02:27 MDP-Algorithms: theory HOL-Algebra.FiniteProduct
14:02:27 Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
14:02:27 CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory
14:02:27 Treaps: theory List-Index.List_Index
14:02:28 Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
14:02:28 Running Registers (on 10.195.8.40) ...
14:02:28 Running Roth_Arithmetic_Progressions (on 10.195.8.40) ...
14:02:28 Treaps: theory Landau_Symbols.Landau_Real_Products
14:02:28 Running S_Finite_Measure_Monad (on 10.195.8.40) ...
14:02:28 Running Probabilistic_Noninterference (on 10.195.8.40) ...
14:02:28 Algebraic_Numbers: theory Show.Show_Real
14:02:28 MDP-Algorithms: theory HOL-Algebra.Ring
14:02:28 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
14:02:28 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
14:02:28 Algebraic_Numbers: theory Show.Show_Complex
14:02:28 Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
14:02:28 HOL-ODE-Numerics: theory Collections.Intf_Comp
14:02:29 CryptHOL: theory Monad_Normalisation.Monad_Normalisation
14:02:29 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
14:02:29 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
14:02:29 MFMC_Countable: theory Flow_Networks.Augmenting_Flow
14:02:29 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
14:02:29 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
14:02:29 CryptHOL: theory CryptHOL.SPMF_Applicative
14:02:29 CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
14:02:29 Turans_Graph_Theorem: theory HOL-Library.Interval
14:02:29 Turans_Graph_Theorem: theory HOL-Library.Float
14:02:29 Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
14:02:29 MFMC_Countable: theory Flow_Networks.Augmenting_Path
14:02:29 Fishers_Inequality: theory Polynomials.Utils
14:02:30 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec
14:02:30 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
14:02:30 CryptHOL: theory Landau_Symbols.Group_Sort
14:02:30 MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
14:02:30 Fishers_Inequality: theory Groebner_Bases.General
14:02:30 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
14:02:30 Gauss_Sums: theory HOL-Algebra.IntRing
14:02:30 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral
14:02:30 Running Lp (on 10.195.8.46) ...
14:02:30 MFMC_Countable: theory MFMC_Countable.MFMC_Flow_Attainability
14:02:30 Running List_Update (on 10.195.8.46) ...
14:02:30 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:02:31 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
14:02:31 Density_Compiler: theory Density_Compiler.PDF_Semantics
14:02:31 HOL-ODE-Numerics: theory Collections.Idx_Iterator
14:02:31 Building Girth_Chromatic (on 10.195.8.46) ...
14:02:31 Applicative_Lifting: theory Applicative_Lifting.Applicative
14:02:31 CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas
14:02:31 Applicative_Lifting: theory Applicative_Lifting.Joinable
14:02:31 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Dense_Linear_Order
14:02:31 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Abstract_Nat
14:02:31 MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
14:02:31 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
14:02:31 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QuasiBorel
14:02:31 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Lemmas_StandardBorel
14:02:31 Probabilistic_Noninterference: theory HOL-Library.Case_Converter
14:02:31 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
14:02:31 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
14:02:31 Probabilistic_Noninterference: theory HOL-Library.Prefix_Order
14:02:31 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
14:02:31 Applicative_Lifting: theory HOL-Library.State_Monad
14:02:31 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Nat
14:02:31 Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat
14:02:32 Fishers_Inequality: theory Polynomials.Power_Products
14:02:32 HOL-ODE-Numerics: theory Collections.Proper_Iterator
14:02:32 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Int
14:02:32 Registers: theory HOL-Eisbach.Eisbach
14:02:32 Zeta_Function: theory Zeta_Function.Zeta_Function
14:02:32 Registers: theory HOL-Library.Type_Length
14:02:32 Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
14:02:32 Actuarial_Mathematics: theory Actuarial_Mathematics.Life_Table
14:02:32 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral
14:02:32 CryptHOL: theory Landau_Symbols.Landau_Real_Products
14:02:32 CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT
14:02:32 Roth_Arithmetic_Progressions: theory HOL-Library.Ramsey
14:02:32 Building Pi_Transcendental (on 10.195.8.46) ...
14:02:32 Running Monomorphic_Monad (on 10.195.8.46) ...
14:02:32 CVP_Hardness: theory LLL_Basis_Reduction.Norms
14:02:33 HOL-ODE-Numerics: theory Collections.It_to_It
14:02:33 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
14:02:33 HOL-ODE-Numerics: theory Collections.SetIteratorGA
14:02:33 Treaps: theory Landau_Symbols.Landau_Simprocs
14:02:33 Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv
14:02:33 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
14:02:33 Lp: theory HOL-Library.Function_Algebras
14:02:33 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
14:02:33 Lp: theory Ergodic_Theory.SG_Library_Complement
14:02:34 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
14:02:34 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
14:02:34 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus
14:02:34 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr
14:02:34 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
14:02:34 Applicative_Lifting: theory HOL-Library.Confluence
14:02:34 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
14:02:34 MDP-Algorithms: theory HOL-Algebra.Module
14:02:34 List_Update: theory List_Update.Prob_Theory
14:02:34 List_Update: theory HOL-Library.While_Combinator
14:02:34 MFMC_Countable: theory MFMC_Countable.MFMC_Finite
14:02:34 Actuarial_Mathematics: theory Actuarial_Mathematics.Examples
14:02:34 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress
14:02:34 Treaps: theory Landau_Symbols.Landau_More
14:02:35 Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
14:02:35 Probabilistic_Noninterference: theory Coinductive.Coinductive_List
14:02:35 Building Quick_Sort_Cost (on 10.195.6.179) ...
14:02:35 Lp: theory Lp.Functional_Spaces
14:02:35 MFMC_Countable: theory MFMC_Countable.MFMC_Web
14:02:35 Building Ergodic_Theory (on 10.195.6.179) ...
14:02:35 Roth_Arithmetic_Progressions: theory HOL-Library.Lattice_Algebras
14:02:35 Running Hahn_Jordan_Decomposition (on 10.195.6.179) ...
14:02:35 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
14:02:35 Running Neumann_Morgenstern_Utility (on 10.195.6.179) ...
14:02:35 List_Update: theory List_Update.Bit_Strings
14:02:35 Building Randomised_Social_Choice (on 10.195.6.179) ...
14:02:35 Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
14:02:35 Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
14:02:35 HOL-ODE-Numerics: theory Word_Lib.More_Divides
14:02:35 Turans_Graph_Theorem: theory HOL-Library.Interval_Float
14:02:36 Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
14:02:36 Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
14:02:36 List_Update: theory List_Update.On_Off
14:02:36 Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
14:02:36 List_Update: theory List-Index.List_Index
14:02:36 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
14:02:36 Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
14:02:36 Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
14:02:36 DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
14:02:36 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Space
14:02:36 Girth_Chromatic: theory HOL-Library.Code_Target_Nat
14:02:36 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
14:02:36 Girth_Chromatic: theory HOL-Library.Code_Target_Int
14:02:37 List_Update: theory List_Update.Inversion
14:02:37 Registers: theory HOL-Library.Word
14:02:37 Registers: theory HOL-Library.Z2
14:02:37 List_Update: theory List_Update.Swaps
14:02:37 Roth_Arithmetic_Progressions: theory HOL-Library.Log_Nat
14:02:37 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme
14:02:37 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic_Misc
14:02:37 Markov_Models: theory Coinductive.Coinductive_Stream
14:02:37 Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
14:02:37 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
14:02:37 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values
14:02:37 Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
14:02:37 Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
14:02:37 MDP-Algorithms: theory Containers.Collection_Order
14:02:37 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Ugraphs
14:02:37 Registers: theory Registers.Axioms
14:02:37 List_Update: theory Regular-Sets.Regular_Set
14:02:37 Registers: theory Registers.Laws
14:02:37 DiscretePricing: theory DiscretePricing.Fair_Price
14:02:37 Ergodic_Theory: theory Ergodic_Theory.ME_Library_Complement
14:02:37 List_Update: theory List_Update.Competitive_Analysis
14:02:37 Girth_Chromatic: theory HOL-Library.Code_Target_Numeral
14:02:37 Ergodic_Theory: theory Ergodic_Theory.Fekete
14:02:38 Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
14:02:38 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844
14:02:38 Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
14:02:38 Girth_Chromatic: theory HOL-Library.Lattice_Algebras
14:02:38 Running Polygonal_Number_Theorem (on of4.proof.cit.tum.de) ...
14:02:38 Quick_Sort_Cost: theory HOL-Library.Function_Algebras
14:02:38 Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
14:02:38 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
14:02:38 Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
14:02:38 Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
14:02:38 Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl
14:02:38 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
14:02:38 Roth_Arithmetic_Progressions: theory Szemeredi_Regularity.Szemeredi
14:02:38 Applicative_Lifting: theory HOL-Library.Confluent_Quotient
14:02:38 Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
14:02:38 Treaps: theory Random_BSTs.Random_BSTs
14:02:38 CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_List
14:02:38 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:02:38 Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State
14:02:38 Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
14:02:38 Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
14:02:38 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
14:02:38 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
14:02:38 Quick_Sort_Cost: theory List-Index.List_Index
14:02:38 Randomised_Social_Choice: theory List-Index.List_Index
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
14:02:38 Pi_Transcendental: theory HOL-Library.Fun_Lexorder
14:02:38 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
14:02:38 Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
14:02:38 Expander_Graphs: theory Graph_Theory.Stuff
14:02:38 Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims
14:02:38 Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
14:02:38 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
14:02:38 Applicative_Lifting: theory Applicative_Lifting.Applicative_State
14:02:38 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
14:02:39 Running Lovasz_Local (on of4.proof.cit.tum.de) ...
14:02:39 Running Standard_Borel_Spaces (on of4.proof.cit.tum.de) ...
14:02:39 Applicative_Lifting: theory HOL-Library.Dlist
14:02:39 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
14:02:39 Running Probabilistic_System_Zoo (on of4.proof.cit.tum.de) ...
14:02:39 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QBS_Morphism
14:02:39 Expander_Graphs: theory Graph_Theory.Digraph
14:02:39 CryptHOL: theory Landau_Symbols.Landau_Simprocs
14:02:39 Applicative_Lifting: theory HOL-Library.Function_Algebras
14:02:39 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
14:02:39 Pi_Transcendental: theory HOL-Library.Poly_Mapping
14:02:39 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
14:02:39 Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
14:02:39 Applicative_Lifting: theory HOL-Library.Function_Division
14:02:39 Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density
14:02:39 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
14:02:39 Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
14:02:39 Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
14:02:40 Registers: theory Registers.Axioms_Complement
14:02:40 CryptHOL: theory Landau_Symbols.Landau_More
14:02:40 Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
14:02:40 Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
14:02:40 Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:02:40 Registers: theory Registers.Laws_Complement
14:02:40 Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef
14:02:40 CryptHOL: theory CryptHOL.Negligible
14:02:40 Lovasz_Local: theory HOL-Eisbach.Eisbach
14:02:40 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Lemmas_StandardBorel
14:02:40 Lovasz_Local: theory Graph_Theory.Rtrancl_On
14:02:40 Lovasz_Local: theory HOL-Combinatorics.Stirling
14:02:40 Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
14:02:40 Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
14:02:40 Registers: theory Registers.Axioms_Classical
14:02:40 Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
14:02:40 Lovasz_Local: theory HOL-Library.Multiset_Order
14:02:40 Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More
14:02:40 Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More
14:02:40 Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union
14:02:40 Lovasz_Local: theory Card_Partitions.Set_Partition
14:02:40 Lovasz_Local: theory Graph_Theory.Stuff
14:02:40 Roth_Arithmetic_Progressions: theory Ergodic_Theory.SG_Library_Complement
14:02:40 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
14:02:40 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
14:02:40 Lovasz_Local: theory Graph_Theory.Digraph
14:02:40 Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension
14:02:40 Registers: theory Registers.Laws_Classical
14:02:40 Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
14:02:40 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
14:02:40 List_Update: theory List_Update.Move_to_Front
14:02:41 Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
14:02:41 Lovasz_Local: theory Nested_Multisets_Ordinals.Multiset_More
14:02:41 Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
14:02:41 Expander_Graphs: theory Graph_Theory.Arc_Walk
14:02:41 Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
14:02:41 Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
14:02:41 MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
14:02:41 MFMC_Countable: theory MFMC_Countable.MFMC_Reduction
14:02:41 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT
14:02:41 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Product
14:02:41 MDP-Algorithms: theory HOL-Library.RBT_Impl
14:02:41 Lovasz_Local: theory Card_Partitions.Injectivity_Solver
14:02:41 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
14:02:41 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values
14:02:42 Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
14:02:42 Registers: theory Registers.Misc
14:02:42 Lovasz_Local: theory Card_Partitions.Card_Partitions
14:02:42 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
14:02:42 Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
14:02:42 Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
14:02:42 Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
14:02:42 Registers: theory Registers.Classical_Extra
14:02:42 Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation
14:02:42 Roth_Arithmetic_Progressions: theory Ergodic_Theory.Asymptotic_Density
14:02:42 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
14:02:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
14:02:42 Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
14:02:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
14:02:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
14:02:42 Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda
14:02:42 Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter
14:02:42 Lp: theory Lp.Lp
14:02:42 Ergodic_Theory: theory Ergodic_Theory.Recurrence
14:02:42 Girth_Chromatic: theory HOL-Library.Log_Nat
14:02:42 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
14:02:42 Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
14:02:42 Lovasz_Local: theory Lovasz_Local.PiE_Rel_Extras
14:02:42 Running Fourier (on of2.proof.cit.tum.de) ...
14:02:42 Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
14:02:42 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
14:02:42 Running Quasi_Borel_Spaces (on of2.proof.cit.tum.de) ...
14:02:42 Lovasz_Local: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
14:02:42 Running Buffons_Needle (on of2.proof.cit.tum.de) ...
14:02:43 Running Source_Coding_Theorem (on of2.proof.cit.tum.de) ...
14:02:43 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Space
14:02:43 Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
14:02:43 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
14:02:43 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
14:02:43 Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed
14:02:43 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
14:02:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
14:02:43 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
14:02:43 Roth_Arithmetic_Progressions: theory HOL-Library.Interval
14:02:43 Lovasz_Local: theory Lovasz_Local.Prob_Events_Extras
14:02:43 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
14:02:43 Applicative_Lifting: theory HOL-Proofs-Lambda.Eta
14:02:43 Girth_Chromatic: theory Girth_Chromatic.Ugraphs
14:02:43 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
14:02:43 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
14:02:43 Lovasz_Local: theory Design_Theory.Multisets_Extras
14:02:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
14:02:43 List_Update: theory Regular-Sets.Regular_Exp
14:02:43 MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
14:02:43 Lovasz_Local: theory Graph_Theory.Arc_Walk
14:02:43 MFMC_Countable: theory MFMC_Countable.MFMC_Unbounded
14:02:43 Lovasz_Local: theory Graph_Theory.Bidirected_Digraph
14:02:43 Roth_Arithmetic_Progressions: theory HOL-Library.Float
14:02:43 Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
14:02:43 Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
14:02:43 Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
14:02:43 MDP-Algorithms: theory HOL-Data_Structures.Tree2
14:02:43 Applicative_Lifting: theory Applicative_Lifting.Combinators
14:02:43 Expander_Graphs: theory Graph_Theory.Pair_Digraph
14:02:43 Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
14:02:43 Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
14:02:43 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.StandardBorel
14:02:44 Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
14:02:44 Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
14:02:44 Running Skip_Lists (on 10.195.8.42) ...
14:02:44 Running Median_Method (on 10.195.8.42) ...
14:02:44 Running Fisher_Yates (on 10.195.8.42) ...
14:02:44 Running Monad_Normalisation (on 10.195.8.42) ...
14:02:44 Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
14:02:44 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
14:02:44 MDP-Algorithms: theory HOL-Data_Structures.Isin2
14:02:44 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
14:02:44 Fourier: theory HOL-Library.Function_Algebras
14:02:44 Pi_Transcendental: theory Polynomials.MPoly_Type
14:02:44 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.StandardBorel
14:02:44 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
14:02:44 Fourier: theory Fourier.Confine
14:02:44 Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
14:02:44 Fourier: theory Fourier.Periodic
14:02:44 Lovasz_Local: theory Lovasz_Local.Cond_Prob_Extensions
14:02:44 Fourier: theory Fourier.Fourier_Aux2
14:02:44 Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
14:02:44 Fourier: theory Ergodic_Theory.SG_Library_Complement
14:02:44 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
14:02:44 Ergodic_Theory: theory Ergodic_Theory.Invariants
14:02:44 Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
14:02:45 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Lemmas_S_Finite_Measure_Monad
14:02:45 Pi_Transcendental: theory Polynomials.More_MPoly_Type
14:02:45 Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
14:02:45 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Product
14:02:45 Fourier: theory Lp.Functional_Spaces
14:02:45 Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
14:02:45 MFMC_Countable: theory MFMC_Countable.MFMC_Bounded
14:02:45 Lovasz_Local: theory Graph_Theory.Pair_Digraph
14:02:45 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Kernels
14:02:45 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Measure_QuasiBorel_Adjunction
14:02:45 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
14:02:45 Lovasz_Local: theory Lovasz_Local.Indep_Events
14:02:45 MDP-Algorithms: theory HOL-Data_Structures.Lookup2
14:02:45 HOL-ODE-Numerics: theory Deriving.Countable_Generator
14:02:45 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
14:02:46 Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
14:02:46 MDP-Algorithms: theory HOL-Data_Structures.RBT
14:02:46 Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set
14:02:46 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bool_Bounded_Set
14:02:46 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample
14:02:46 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
14:02:46 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
14:02:46 Pi_Transcendental: theory Symmetric_Polynomials.Vieta
14:02:46 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.QuasiBorel
14:02:46 Ergodic_Theory: theory Ergodic_Theory.Ergodicity
14:02:46 Standard_Borel_Spaces: theory Standard_Borel_Spaces.StandardBorel
14:02:46 Lovasz_Local: theory Lovasz_Local.Basic_Method
14:02:46 Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
14:02:46 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
14:02:46 Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
14:02:46 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
14:02:46 Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
14:02:46 Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
14:02:46 Markov_Models: theory Markov_Models.Crowds_Protocol
14:02:46 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
14:02:46 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
14:02:46 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
14:02:46 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction
14:02:47 Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
14:02:47 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
14:02:47 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
14:02:47 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
14:02:47 Skip_Lists: theory Skip_Lists.Pi_pmf
14:02:47 Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
14:02:47 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
14:02:47 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
14:02:47 Girth_Chromatic: theory HOL-Library.Interval
14:02:47 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel
14:02:47 Girth_Chromatic: theory HOL-Library.Float
14:02:47 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel
14:02:47 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
14:02:47 Fourier: theory Lp.Lp
14:02:47 Timing Buffons_Needle (6 threads, 2.483s elapsed time, 8.085s cpu time, 0.147s GC time, factor 3.26)
14:02:47 Finished Buffons_Needle (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.27)
14:02:47 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Product_QuasiBorel
14:02:47 Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
14:02:47 Timing Source_Coding_Theorem (6 threads, 2.635s elapsed time, 5.699s cpu time, 0.180s GC time, factor 2.16)
14:02:47 Finished Source_Coding_Theorem (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.65)
14:02:47 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.CoProduct_QuasiBorel
14:02:47 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
14:02:47 DiscretePricing: theory DiscretePricing.CRR_Model
14:02:47 Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
14:02:47 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
14:02:47 Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
14:02:47 Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
14:02:48 Fourier: theory Fourier.Lspace
14:02:48 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Exponent_QuasiBorel
14:02:48 Fourier: theory Fourier.Square_Integrable
14:02:48 Skip_Lists: theory Skip_Lists.Misc
14:02:48 Skip_Lists: theory Skip_Lists.Geometric_PMF
14:02:48 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral_Float
14:02:48 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel
14:02:48 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
14:02:48 Fourier: theory Fourier.Fourier
14:02:48 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
14:02:48 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
14:02:48 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
14:02:48 Roth_Arithmetic_Progressions: theory HOL-Library.Interval_Float
14:02:48 Quick_Sort_Cost: theory Landau_Symbols.Landau_More
14:02:48 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
14:02:48 Skip_Lists: theory Skip_Lists.Skip_List
14:02:49 MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
14:02:49 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Monad_QuasiBorel
14:02:49 Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
14:02:49 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation_MFMC
14:02:49 Ergodic_Theory: theory Ergodic_Theory.Kingman
14:02:49 Median_Method: theory Median_Method.Median
14:02:49 Timing Monad_Normalisation (2 threads, 1.735s elapsed time, 2.607s cpu time, 0.106s GC time, factor 1.50)
14:02:49 Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.09)
14:02:49 Gauss_Sums: theory Gauss_Sums.Gauss_Sums
14:02:49 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
14:02:50 MDP-Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
14:02:50 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
14:02:50 List_Update: theory Regular-Sets.NDerivative
14:02:50 Registers: theory Registers.Finite_Tensor_Product
14:02:50 MDP-Algorithms: theory Perron_Frobenius.Cancel_Card_Constraint
14:02:50 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation_Bounds
14:02:50 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
14:02:50 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
14:02:50 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Monad_QuasiBorel
14:02:50 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
14:02:50 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Unsorted
14:02:50 Ergodic_Theory: theory Ergodic_Theory.Shift_Operator
14:02:50 Expander_Graphs: theory Graph_Theory.Digraph_Component
14:02:50 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
14:02:51 Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
14:02:51 List_Update: theory List_Update.MTF2_Effects
14:02:51 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure
14:02:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
14:02:51 Registers: theory Registers.Axioms_Quantum
14:02:51 Girth_Chromatic: theory HOL-Library.Code_Target_Numeral_Float
14:02:51 Girth_Chromatic: theory HOL-Library.Interval_Float
14:02:51 Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
14:02:51 List_Update: theory List_Update.BIT
14:02:51 Lovasz_Local: theory Lovasz_Local.Digraph_Extensions
14:02:51 Timing Fisher_Yates (2 threads, 4.307s elapsed time, 7.441s cpu time, 0.212s GC time, factor 1.73)
14:02:51 Finished Fisher_Yates (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.38)
14:02:52 Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
14:02:52 Registers: theory Registers.Finite_Tensor_Product_Matrices
14:02:52 Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
14:02:52 Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
14:02:52 Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
14:02:52 Registers: theory Registers.Quantum
14:02:52 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure
14:02:52 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
14:02:52 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
14:02:52 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial
14:02:53 Density_Compiler: theory Density_Compiler.PDF_Compiler
14:02:53 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
14:02:53 Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Bayesian_Linear_Regression
14:02:53 Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Lemma
14:02:53 Treaps: theory Treaps.Treap
14:02:53 Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
14:02:53 Treaps: theory Treaps.Probability_Misc
14:02:53 Treaps: theory Treaps.Random_List_Permutation
14:02:53 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
14:02:53 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
14:02:53 Markov_Models: theory Markov_Models.Gossip_Broadcast
14:02:54 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Montecarlo
14:02:54 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Query
14:02:54 Treaps: theory Treaps.Treap_Sort_and_BSTs
14:02:54 Registers: theory Registers.Laws_Quantum
14:02:54 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
14:02:54 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
14:02:55 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
14:02:55 Markov_Models: theory Markov_Models.Example_A
14:02:55 Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Root
14:02:55 Markov_Models: theory Markov_Models.Example_B
14:02:56 List_Update: theory List_Update.Partial_Cost_Model
14:02:56 List_Update: theory Regular-Sets.Equivalence_Checking
14:02:56 Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
14:02:56 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
14:02:56 List_Update: theory List_Update.RExp_Var
14:02:56 Markov_Models: theory Markov_Models.Markov_Decision_Process
14:02:56 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
14:02:57 Treaps: theory Treaps.Random_Treap
14:02:57 CryptHOL: theory CryptHOL.Misc_CryptHOL
14:02:57 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation
14:02:57 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
14:02:57 Registers: theory Registers.Quantum_Extra
14:02:57 Timing Median_Method (2 threads, 9.912s elapsed time, 15.566s cpu time, 0.701s GC time, factor 1.57)
14:02:57 Finished Median_Method (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.43)
14:02:57 List_Update: theory List_Update.List_Factoring
14:02:57 Estimated 0:52:10 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.457s)
14:02:58 Registers: theory Registers.Axioms_Complement_Quantum
14:02:58 List_Update: theory List_Update.OPT2
14:02:58 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
14:02:59 Markov_Models: theory Markov_Models.PCTL
14:02:59 Registers: theory Registers.Laws_Complement_Quantum
14:02:59 Registers: theory Registers.QHoare
14:02:59 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
14:02:59 Timing Quasi_Borel_Spaces (6 threads, 14.571s elapsed time, 58.304s cpu time, 5.425s GC time, factor 4.00)
14:02:59 Finished Quasi_Borel_Spaces (0:00:16 elapsed time, 0:01:00 cpu time, factor 3.70)
14:02:59 Registers: theory Registers.Teleport
14:02:59 Registers: theory Registers.Check_Autogenerated_Files
14:02:59 Timing Fourier (6 threads, 14.811s elapsed time, 70.407s cpu time, 3.054s GC time, factor 4.75)
14:02:59 Finished Fourier (0:00:16 elapsed time, 0:01:12 cpu time, factor 4.35)
14:03:00 List_Update: theory List_Update.BIT_pairwise
14:03:00 List_Update: theory List_Update.Phase_Partitioning
14:03:01 Girth_Chromatic: theory HOL-Decision_Procs.Approximation
14:03:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
14:03:01 List_Update: theory List_Update.BIT_2comp_on2
14:03:01 List_Update: theory List_Update.TS
14:03:02 Markov_Models: theory Markov_Models.MDP_Reachability_Problem
14:03:02 DiscretePricing: theory DiscretePricing.Option_Price_Examples
14:03:02 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
14:03:03 Registers: theory Registers.Quantum_Extra2
14:03:03 MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:03:03 Registers: theory Registers.Pure_States
14:03:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
14:03:04 Timing Neumann_Morgenstern_Utility (2 threads, 24.851s elapsed time, 38.873s cpu time, 1.331s GC time, factor 1.56)
14:03:04 Finished Neumann_Morgenstern_Utility (0:00:28 elapsed time, 0:00:42 cpu time, factor 1.49)
14:03:04 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
14:03:04 List_Update: theory List_Update.Comb
14:03:04 Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
14:03:04 Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
14:03:04 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample
14:03:05 Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
14:03:05 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
14:03:05 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
14:03:05 Timing Skip_Lists (2 threads, 17.675s elapsed time, 31.893s cpu time, 1.271s GC time, factor 1.80)
14:03:05 Finished Skip_Lists (0:00:20 elapsed time, 0:00:35 cpu time, factor 1.67)
14:03:05 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
14:03:06 Markov_Models: theory Markov_Models.MDP_RP_Certification
14:03:06 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
14:03:06 Timing Lovasz_Local (6 threads, 25.432s elapsed time, 98.748s cpu time, 7.137s GC time, factor 3.88)
14:03:06 Finished Lovasz_Local (0:00:27 elapsed time, 0:01:40 cpu time, factor 3.72)
14:03:06 Timing Standard_Borel_Spaces (6 threads, 25.659s elapsed time, 84.083s cpu time, 4.215s GC time, factor 3.28)
14:03:06 Finished Standard_Borel_Spaces (0:00:27 elapsed time, 0:01:25 cpu time, factor 3.14)
14:03:06 Timing Polygonal_Number_Theorem (6 threads, 25.455s elapsed time, 87.635s cpu time, 4.191s GC time, factor 3.44)
14:03:06 Finished Polygonal_Number_Theorem (0:00:27 elapsed time, 0:01:29 cpu time, factor 3.27)
14:03:07 MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
14:03:07 MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:03:07 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
14:03:08 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
14:03:08 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
14:03:08 MDP-Algorithms: theory HOL-Data_Structures.RBT_Set
14:03:08 CVP_Hardness: theory CVP_Hardness.infnorm
14:03:08 Timing Probabilistic_System_Zoo (6 threads, 27.210s elapsed time, 75.380s cpu time, 7.714s GC time, factor 2.77)
14:03:08 Finished Probabilistic_System_Zoo (0:00:29 elapsed time, 0:01:18 cpu time, factor 2.68)
14:03:08 CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
14:03:08 CVP_Hardness: theory CVP_Hardness.CVP_vec
14:03:08 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
14:03:08 CryptHOL: theory CryptHOL.Generat
14:03:08 CryptHOL: theory CryptHOL.List_Bits
14:03:09 CryptHOL: theory CryptHOL.Resumption
14:03:09 Expander_Graphs: theory Matrix.Utility
14:03:09 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
14:03:09 CVP_Hardness: theory CVP_Hardness.BHLE
14:03:10 MDP-Algorithms: theory HOL-Data_Structures.RBT_Map
14:03:10 CVP_Hardness: theory CVP_Hardness.SVP_vec
14:03:11 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
14:03:11 Timing Hahn_Jordan_Decomposition (2 threads, 32.961s elapsed time, 45.838s cpu time, 1.658s GC time, factor 1.39)
14:03:11 Finished Hahn_Jordan_Decomposition (0:00:36 elapsed time, 0:00:48 cpu time, factor 1.35)
14:03:12 MDP-Algorithms: theory HOL-Library.Code_Real_Approx_By_Float
14:03:12 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
14:03:12 CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
14:03:12 Markov_Models: theory Markov_Models.PGCL
14:03:12 MDP-Algorithms: theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
14:03:12 MDP-Algorithms: theory Jordan_Normal_Form.Conjugate
14:03:13 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
14:03:13 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
14:03:13 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
14:03:14 Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
14:03:14 Expander_Graphs: theory Jordan_Normal_Form.Matrix
14:03:15 Markov_Models: theory Markov_Models.Zeroconf_Analysis
14:03:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
14:03:16 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
14:03:17 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
14:03:17 Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
14:03:18 MDP-Algorithms: theory HOL-Library.Tree_Real
14:03:18 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
14:03:18 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
14:03:18 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
14:03:18 MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
14:03:18 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
14:03:18 Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
14:03:18 MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
14:03:19 Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
14:03:20 Timing Treaps (2 threads, 54.497s elapsed time, 89.487s cpu time, 4.438s GC time, factor 1.64)
14:03:20 Finished Treaps (0:00:58 elapsed time, 0:01:33 cpu time, factor 1.60)
14:03:20 Markov_Models: theory Markov_Models.Markov_Models
14:03:20 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
14:03:21 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
14:03:22 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
14:03:23 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
14:03:23 Timing Monomorphic_Monad (2 threads, 46.031s elapsed time, 75.519s cpu time, 6.852s GC time, factor 1.64)
14:03:23 Finished Monomorphic_Monad (0:00:50 elapsed time, 0:01:19 cpu time, factor 1.59)
14:03:24 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
14:03:24 Timing Lp (2 threads, 49.712s elapsed time, 74.398s cpu time, 2.862s GC time, factor 1.50)
14:03:24 Finished Lp (0:00:53 elapsed time, 0:01:17 cpu time, factor 1.46)
14:03:24 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
14:03:24 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
14:03:24 MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
14:03:24 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:03:24 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
14:03:24 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
14:03:24 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
14:03:24 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
14:03:25 Timing Differential_Dynamic_Logic (8 threads, 100.405s elapsed time, 277.954s cpu time, 24.981s GC time, factor 2.77)
14:03:25 Finished Differential_Dynamic_Logic (0:01:42 elapsed time, 0:04:43 cpu time, factor 2.76)
14:03:26 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
14:03:26 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
14:03:26 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
14:03:26 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
14:03:27 Timing Linear_Recurrences_Solver (8 threads, 101.495s elapsed time, 487.319s cpu time, 57.897s GC time, factor 4.80)
14:03:27 Finished Linear_Recurrences_Solver (0:01:44 elapsed time, 0:08:12 cpu time, factor 4.74)
14:03:28 Expander_Graphs: theory Jordan_Normal_Form.Determinant
14:03:28 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
14:03:29 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
14:03:30 MDP-Algorithms: theory MDP-Algorithms.MDP_fin
14:03:31 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
14:03:31 Expander_Graphs: theory Regular-Sets.Regular_Set
14:03:31 Timing Randomised_Social_Choice (2 threads, 27.899s elapsed time, 44.512s cpu time, 2.458s GC time, factor 1.60)
14:03:31 Finished Randomised_Social_Choice (0:00:54 elapsed time, 0:01:18 cpu time, factor 1.42)
14:03:31 Timing Quick_Sort_Cost (2 threads, 26.306s elapsed time, 40.201s cpu time, 2.303s GC time, factor 1.53)
14:03:31 Finished Quick_Sort_Cost (0:00:55 elapsed time, 0:01:16 cpu time, factor 1.38)
14:03:31 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
14:03:33 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
14:03:33 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
14:03:33 CryptHOL: theory CryptHOL.Computational_Model
14:03:33 CryptHOL: theory CryptHOL.GPV_Applicative
14:03:33 Building Random_BSTs (on of2.proof.cit.tum.de) ...
14:03:33 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
14:03:33 MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
14:03:33 Running SDS_Impossibility (on of2.proof.cit.tum.de) ...
14:03:33 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
14:03:33 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
14:03:34 Timing Hermite (2 threads, 74.769s elapsed time, 103.078s cpu time, 5.789s GC time, factor 1.38)
14:03:34 Finished Hermite (0:01:43 elapsed time, 0:02:12 cpu time, factor 1.28)
14:03:34 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
14:03:34 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
14:03:34 MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
14:03:34 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
14:03:34 Random_BSTs: theory HOL-Data_Structures.Cmp
14:03:34 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
14:03:34 Random_BSTs: theory HOL-Data_Structures.Less_False
14:03:35 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
14:03:35 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
14:03:35 Expander_Graphs: theory VectorSpace.FunctionLemmas
14:03:35 Expander_Graphs: theory VectorSpace.RingModuleFacts
14:03:35 Random_BSTs: theory HOL-Data_Structures.Set_Specs
14:03:35 Random_BSTs: theory HOL-Data_Structures.Tree_Set
14:03:35 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
14:03:35 Random_BSTs: theory Random_BSTs.Random_BSTs
14:03:36 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
14:03:36 CryptHOL: theory CryptHOL.GPV_Expectation
14:03:37 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
14:03:37 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
14:03:37 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
14:03:38 CryptHOL: theory CryptHOL.GPV_Bisim
14:03:38 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
14:03:38 Expander_Graphs: theory VectorSpace.MonoidSums
14:03:38 Expander_Graphs: theory Regular-Sets.Regular_Exp
14:03:38 Expander_Graphs: theory VectorSpace.LinearCombinations
14:03:39 CryptHOL: theory CryptHOL.CryptHOL
14:03:39 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
14:03:42 MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
14:03:44 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
14:03:44 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
14:03:45 HOL-ODE-Numerics: theory Collections.Gen_Iterator
14:03:45 HOL-ODE-Numerics: theory HOL-Library.RBT
14:03:46 Timing Commuting_Hermitian (2 threads, 47.697s elapsed time, 74.202s cpu time, 3.448s GC time, factor 1.56)
14:03:46 Finished Commuting_Hermitian (0:01:24 elapsed time, 0:01:57 cpu time, factor 1.39)
14:03:46 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
14:03:46 HOL-ODE-Numerics: theory Collections.Iterator
14:03:46 Timing SDS_Impossibility (6 threads, 11.680s elapsed time, 36.076s cpu time, 2.657s GC time, factor 3.09)
14:03:46 Finished SDS_Impossibility (0:00:13 elapsed time, 0:00:37 cpu time, factor 2.83)
14:03:46 Timing Random_BSTs (6 threads, 2.648s elapsed time, 5.538s cpu time, 0.567s GC time, factor 2.09)
14:03:46 Finished Random_BSTs (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.57)
14:03:47 HOL-ODE-Numerics: theory Collections.Intf_Map
14:03:47 Timing Actuarial_Mathematics (2 threads, 83.477s elapsed time, 135.167s cpu time, 7.572s GC time, factor 1.62)
14:03:47 Finished Actuarial_Mathematics (0:01:27 elapsed time, 0:02:19 cpu time, factor 1.59)
14:03:47 HOL-ODE-Numerics: theory Collections.Array_Iterator
14:03:47 HOL-ODE-Numerics: theory Collections.RBT_add
14:03:48 HOL-ODE-Numerics: theory Collections.Gen_Map
14:03:48 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
14:03:49 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
14:03:50 HOL-ODE-Numerics: theory Collections.Impl_List_Map
14:03:50 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
14:03:51 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
14:03:51 Timing Gauss_Sums (2 threads, 84.577s elapsed time, 139.889s cpu time, 12.783s GC time, factor 1.65)
14:03:51 Finished Gauss_Sums (0:01:29 elapsed time, 0:02:24 cpu time, factor 1.63)
14:03:51 Building Smith_Normal_Form (on of4.proof.cit.tum.de) ...
14:03:52 HOL-ODE-Numerics: theory Collections.Intf_Set
14:03:52 MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
14:03:52 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
14:03:52 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
14:03:52 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
14:03:53 Running TsirelsonBound (on of4.proof.cit.tum.de) ...
14:03:53 HOL-ODE-Numerics: theory Collections.Gen_Set
14:03:53 Timing Applicative_Lifting (2 threads, 49.715s elapsed time, 71.910s cpu time, 8.398s GC time, factor 1.45)
14:03:53 Finished Applicative_Lifting (0:01:23 elapsed time, 0:01:52 cpu time, factor 1.34)
14:03:54 MDP-Algorithms: theory Containers.RBT_ext
14:03:54 Smith_Normal_Form: theory HOL-Eisbach.Eisbach
14:03:54 Smith_Normal_Form: theory Deriving.Derive_Manager
14:03:54 Smith_Normal_Form: theory Deriving.Generator_Aux
14:03:54 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
14:03:54 Smith_Normal_Form: theory HOL-Algebra.Congruence
14:03:54 Smith_Normal_Form: theory HOL-Number_Theory.Cong
14:03:54 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
14:03:54 Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
14:03:55 Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
14:03:55 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
14:03:55 Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:03:55 Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
14:03:55 Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
14:03:55 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
14:03:55 HOL-ODE-Numerics: theory Collections.Impl_List_Set
14:03:55 Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
14:03:55 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
14:03:55 Smith_Normal_Form: theory HOL-Algebra.Order
14:03:55 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
14:03:56 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
14:03:56 Smith_Normal_Form: theory HOL-Number_Theory.Totient
14:03:56 Smith_Normal_Form: theory List-Index.List_Index
14:03:56 Running Stern_Brocot (on of2.proof.cit.tum.de) ...
14:03:56 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
14:03:56 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
14:03:56 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
14:03:56 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
14:03:56 Smith_Normal_Form: theory HOL-Algebra.Lattice
14:03:56 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
14:03:56 Smith_Normal_Form: theory Show.Show
14:03:56 MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
14:03:56 HOL-ODE-Numerics: theory Show.Show
14:03:56 TsirelsonBound: theory TsirelsonBound.Tsirelson
14:03:56 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
14:03:56 MDP-Algorithms: theory MDP-Algorithms.Code_Setup
14:03:57 Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
14:03:57 Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
14:03:57 Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:03:57 Smith_Normal_Form: theory Show.Show_Instances
14:03:57 Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
14:03:57 Smith_Normal_Form: theory VectorSpace.FunctionLemmas
14:03:57 Smith_Normal_Form: theory HOL-Algebra.Group
14:03:57 Stern_Brocot: theory Stern_Brocot.Cotree
14:03:58 Smith_Normal_Form: theory Show.Show_Poly
14:03:59 Smith_Normal_Form: theory HOL-Algebra.Coset
14:03:59 Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
14:03:59 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
14:03:59 Smith_Normal_Form: theory HOL-Algebra.Ring
14:04:00 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
14:04:01 Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
14:04:01 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
14:04:01 HOL-ODE-Numerics: theory Show.Show_Instances
14:04:01 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
14:04:01 Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
14:04:01 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
14:04:02 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
14:04:02 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
14:04:02 Smith_Normal_Form: theory HOL-Algebra.AbelCoset
14:04:02 Smith_Normal_Form: theory HOL-Algebra.Module
14:04:02 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
14:04:03 HOL-ODE-Numerics: theory Word_Lib.More_Word
14:04:03 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
14:04:03 Smith_Normal_Form: theory VectorSpace.RingModuleFacts
14:04:04 Smith_Normal_Form: theory VectorSpace.MonoidSums
14:04:04 Smith_Normal_Form: theory VectorSpace.LinearCombinations
14:04:04 Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
14:04:04 Smith_Normal_Form: theory HOL-Algebra.Ideal
14:04:05 Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
14:04:05 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
14:04:05 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
14:04:05 MDP-Algorithms: theory Containers.RBT_Mapping2
14:04:05 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
14:04:06 Smith_Normal_Form: theory HOL-Algebra.RingHom
14:04:06 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
14:04:06 Smith_Normal_Form: theory HOL-Algebra.UnivPoly
14:04:07 MDP-Algorithms: theory MDP-Algorithms.Fin_Code
14:04:07 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
14:04:07 MDP-Algorithms: theory Containers.RBT_Set2
14:04:07 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
14:04:07 Smith_Normal_Form: theory VectorSpace.SumSpaces
14:04:07 Smith_Normal_Form: theory VectorSpace.VectorSpace
14:04:08 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
14:04:08 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
14:04:08 Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:04:08 Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
14:04:08 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
14:04:08 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
14:04:08 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
14:04:09 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
14:04:09 Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
14:04:09 Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
14:04:09 Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
14:04:09 Timing TsirelsonBound (6 threads, 14.284s elapsed time, 64.303s cpu time, 3.239s GC time, factor 4.50)
14:04:09 Finished TsirelsonBound (0:00:16 elapsed time, 0:01:06 cpu time, factor 4.09)
14:04:09 Stern_Brocot: theory Stern_Brocot.Bird_Tree
14:04:10 Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
14:04:10 Expander_Graphs: theory Regular-Sets.NDerivative
14:04:10 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
14:04:10 Timing Stern_Brocot (6 threads, 12.834s elapsed time, 23.519s cpu time, 2.249s GC time, factor 1.83)
14:04:10 Finished Stern_Brocot (0:00:14 elapsed time, 0:00:25 cpu time, factor 1.75)
14:04:11 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
14:04:11 Running Randomised_BSTs (on 10.195.6.179) ...
14:04:12 Timing Pi_Transcendental (2 threads, 61.732s elapsed time, 95.177s cpu time, 5.711s GC time, factor 1.54)
14:04:12 Finished Pi_Transcendental (0:01:38 elapsed time, 0:02:18 cpu time, factor 1.41)
14:04:13 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
14:04:13 Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
14:04:13 Expander_Graphs: theory VectorSpace.SumSpaces
14:04:14 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
14:04:14 Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
14:04:14 Expander_Graphs: theory VectorSpace.VectorSpace
14:04:14 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
14:04:15 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
14:04:15 Expander_Graphs: theory Regular-Sets.Regexp_Method
14:04:15 Smith_Normal_Form: theory HOL-Number_Theory.Residues
14:04:16 Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
14:04:18 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
14:04:18 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
14:04:18 Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
14:04:18 Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
14:04:19 Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
14:04:20 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
14:04:20 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:04:21 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
14:04:22 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
14:04:22 Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
14:04:22 Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
14:04:22 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
14:04:23 Expander_Graphs: theory Matrix.Ordered_Semiring
14:04:23 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
14:04:24 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
14:04:24 Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
14:04:24 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
14:04:24 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
14:04:24 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
14:04:24 HOL-ODE-Numerics: theory Native_Word.Uint
14:04:25 Expander_Graphs: theory Matrix.Matrix_Legacy
14:04:25 HOL-ODE-Numerics: theory Native_Word.Uint32
14:04:26 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
14:04:26 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
14:04:26 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
14:04:26 Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
14:04:26 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
14:04:26 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
14:04:26 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
14:04:27 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
14:04:27 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
14:04:27 Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
14:04:27 HOL-ODE-Numerics: theory Collections.HashCode
14:04:27 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
14:04:27 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
14:04:27 HOL-ODE-Numerics: theory Collections.Intf_Hash
14:04:28 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
14:04:28 HOL-ODE-Numerics: theory Collections.Gen_Hash
14:04:28 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
14:04:29 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
14:04:29 Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
14:04:29 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
14:04:29 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
14:04:30 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
14:04:30 Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
14:04:30 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
14:04:30 Timing Randomised_BSTs (2 threads, 15.096s elapsed time, 28.045s cpu time, 1.921s GC time, factor 1.86)
14:04:30 Finished Randomised_BSTs (0:00:18 elapsed time, 0:00:31 cpu time, factor 1.71)
14:04:31 Running Hermite_Lindemann (on 10.195.8.40) ...
14:04:31 HOL-ODE-Numerics: theory Deriving.Hash_Generator
14:04:32 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
14:04:32 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
14:04:32 HOL-ODE-Numerics: theory Deriving.Hash_Instances
14:04:32 HOL-ODE-Numerics: theory Deriving.Derive
14:04:33 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
14:04:33 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
14:04:33 Timing Zeta_Function (2 threads, 112.784s elapsed time, 187.722s cpu time, 8.906s GC time, factor 1.66)
14:04:33 Finished Zeta_Function (0:02:25 elapsed time, 0:03:46 cpu time, factor 1.56)
14:04:33 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
14:04:34 Timing Density_Compiler (2 threads, 127.044s elapsed time, 233.098s cpu time, 14.245s GC time, factor 1.83)
14:04:34 Finished Density_Compiler (0:02:11 elapsed time, 0:03:58 cpu time, factor 1.81)
14:04:36 Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
14:04:36 Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
14:04:36 Hermite_Lindemann: theory HOL-Library.Monad_Syntax
14:04:36 Hermite_Lindemann: theory HOL-Algebra.Divisibility
14:04:36 Hermite_Lindemann: theory Containers.Containers_Auxiliary
14:04:36 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
14:04:36 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
14:04:37 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
14:04:39 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
14:04:40 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
14:04:41 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
14:04:42 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
14:04:43 Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
14:04:43 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:04:43 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
14:04:43 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
14:04:44 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
14:04:45 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
14:04:45 Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
14:04:45 Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
14:04:45 Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:04:45 Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
14:04:45 Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
14:04:46 Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
14:04:47 Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
14:04:49 Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
14:04:49 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
14:04:49 Expander_Graphs: theory QHLProver.Complex_Matrix
14:04:49 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
14:04:50 Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
14:04:50 Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
14:04:50 Building Prime_Number_Theorem (on of4.proof.cit.tum.de) ...
14:04:50 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
14:04:50 Hermite_Lindemann: theory Matrix.Utility
14:04:50 Building Prime_Distribution_Elementary (on of4.proof.cit.tum.de) ...
14:04:51 Running Dirichlet_L (on of4.proof.cit.tum.de) ...
14:04:51 Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
14:04:51 Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
14:04:51 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
14:04:52 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
14:04:52 Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
14:04:52 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
14:04:52 Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
14:04:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
14:04:52 Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
14:04:52 Dirichlet_L: theory HOL-Library.Log_Nat
14:04:52 Dirichlet_L: theory Lehmer.Lehmer
14:04:52 Dirichlet_L: theory HOL-Library.Lattice_Algebras
14:04:53 Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
14:04:53 Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
14:04:53 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
14:04:53 Expander_Graphs: theory QHLProver.Gates
14:04:54 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
14:04:54 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
14:04:54 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
14:04:55 Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
14:04:55 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
14:04:55 Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
14:04:55 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
14:04:55 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
14:04:55 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
14:04:56 Timing DiscretePricing (2 threads, 155.700s elapsed time, 246.678s cpu time, 20.146s GC time, factor 1.58)
14:04:56 Finished DiscretePricing (0:02:40 elapsed time, 0:04:11 cpu time, factor 1.57)
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
14:04:57 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
14:04:58 Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
14:04:58 Dirichlet_L: theory HOL-Library.Interval
14:04:58 Dirichlet_L: theory HOL-Library.Float
14:04:58 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
14:04:59 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
14:05:00 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
14:05:01 Dirichlet_L: theory HOL-Library.Interval_Float
14:05:01 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
14:05:02 Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
14:05:02 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
14:05:03 Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:05:05 Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
14:05:06 Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
14:05:06 Dirichlet_L: theory Bertrands_Postulate.Bertrand
14:05:07 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
14:05:07 Timing Ergodic_Theory (2 threads, 120.977s elapsed time, 221.807s cpu time, 10.163s GC time, factor 1.83)
14:05:07 Finished Ergodic_Theory (0:02:30 elapsed time, 0:04:20 cpu time, factor 1.73)
14:05:08 Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
14:05:09 MDP-Algorithms: theory Containers.Set_Impl
14:05:10 Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
14:05:11 Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
14:05:11 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
14:05:12 Hermite_Lindemann: theory Subresultants.More_Homomorphisms
14:05:13 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
14:05:14 Hermite_Lindemann: theory Subresultants.Resultant_Prelim
14:05:14 Timing MFMC_Countable (2 threads, 174.079s elapsed time, 271.765s cpu time, 12.944s GC time, factor 1.56)
14:05:14 Finished MFMC_Countable (0:02:58 elapsed time, 0:04:37 cpu time, factor 1.55)
14:05:15 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
14:05:15 Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
14:05:15 Timing Turans_Graph_Theorem (2 threads, 175.205s elapsed time, 289.841s cpu time, 21.992s GC time, factor 1.65)
14:05:15 Finished Turans_Graph_Theorem (0:03:00 elapsed time, 0:04:56 cpu time, factor 1.64)
14:05:17 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
14:05:17 Hermite_Lindemann: theory Algebraic_Numbers.Resultant
14:05:17 Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
14:05:19 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
14:05:19 Dirichlet_L: theory HOL-Algebra.QuotRing
14:05:19 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
14:05:20 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
14:05:20 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
14:05:20 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
14:05:20 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
14:05:20 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
14:05:21 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
14:05:22 Dirichlet_L: theory HOL-Algebra.IntRing
14:05:22 MDP-Algorithms: theory MDP-Algorithms.GS_Code
14:05:22 Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
14:05:22 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
14:05:22 Timing Prime_Number_Theorem (6 threads, 16.357s elapsed time, 50.121s cpu time, 2.692s GC time, factor 3.06)
14:05:22 Finished Prime_Number_Theorem (0:00:31 elapsed time, 0:01:11 cpu time, factor 2.28)
14:05:22 Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
14:05:23 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
14:05:23 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
14:05:23 Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
14:05:23 Timing CVP_Hardness (2 threads, 191.034s elapsed time, 323.462s cpu time, 13.390s GC time, factor 1.69)
14:05:23 Finished CVP_Hardness (0:03:16 elapsed time, 0:05:29 cpu time, factor 1.68)
14:05:23 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
14:05:23 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
14:05:24 Running Laws_of_Large_Numbers (on 10.195.7.194) ...
14:05:24 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
14:05:24 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
14:05:24 Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
14:05:24 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
14:05:24 Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
14:05:24 Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
14:05:25 Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
14:05:26 Timing Prime_Distribution_Elementary (6 threads, 19.209s elapsed time, 80.580s cpu time, 4.668s GC time, factor 4.19)
14:05:26 Finished Prime_Distribution_Elementary (0:00:33 elapsed time, 0:01:41 cpu time, factor 3.00)
14:05:26 Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
14:05:26 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
14:05:27 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
14:05:28 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
14:05:28 MDP-Algorithms: theory MDP-Algorithms.MPI_Code
14:05:28 Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
14:05:29 Markov_Models: theory Markov_Models.MDP_RP
14:05:30 Timing Laws_of_Large_Numbers (2 threads, 2.400s elapsed time, 4.000s cpu time, 0.198s GC time, factor 1.67)
14:05:30 Finished Laws_of_Large_Numbers (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.23)
14:05:31 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
14:05:32 Timing Girth_Chromatic (2 threads, 123.702s elapsed time, 213.561s cpu time, 23.312s GC time, factor 1.73)
14:05:32 Finished Girth_Chromatic (0:02:57 elapsed time, 0:04:39 cpu time, factor 1.58)
14:05:33 Timing Dirichlet_L (6 threads, 38.834s elapsed time, 172.757s cpu time, 16.798s GC time, factor 4.45)
14:05:33 Finished Dirichlet_L (0:00:41 elapsed time, 0:02:55 cpu time, factor 4.27)
14:05:33 Timing CRYSTALS-Kyber (2 threads, 193.592s elapsed time, 281.017s cpu time, 24.460s GC time, factor 1.45)
14:05:33 Finished CRYSTALS-Kyber (0:03:18 elapsed time, 0:04:46 cpu time, factor 1.44)
14:05:33 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
14:05:34 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
14:05:35 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
14:05:36 MDP-Algorithms: theory MDP-Algorithms.VI_Code
14:05:37 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
14:05:40 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
14:05:42 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
14:05:42 MDP-Algorithms: theory Jordan_Normal_Form.Matrix
14:05:44 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
14:05:45 Running Zeta_3_Irrational (on 10.195.7.194) ...
14:05:46 Running Irrational_Series_Erdos_Straus (on 10.195.7.194) ...
14:05:46 Running IMO2019 (on 10.195.7.194) ...
14:05:47 Running Szemeredi_Regularity (on 10.195.7.194) ...
14:05:47 Running Random_Graph_Subgraph_Threshold (on 10.195.7.194) ...
14:05:47 MDP-Algorithms: theory Show.Show
14:05:48 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:05:48 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
14:05:49 Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
14:05:49 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
14:05:49 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
14:05:50 MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
14:05:50 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
14:05:50 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
14:05:50 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
14:05:50 Timing Fishers_Inequality (2 threads, 216.932s elapsed time, 370.921s cpu time, 31.013s GC time, factor 1.71)
14:05:50 Finished Fishers_Inequality (0:03:42 elapsed time, 0:06:17 cpu time, factor 1.70)
14:05:50 IMO2019: theory IMO2019.IMO2019_Q5
14:05:50 IMO2019: theory IMO2019.IMO2019_Q1
14:05:50 MDP-Algorithms: theory Jordan_Normal_Form.Determinant
14:05:50 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
14:05:50 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
14:05:50 IMO2019: theory IMO2019.IMO2019_Q4
14:05:52 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
14:05:52 Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
14:05:52 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
14:05:52 Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
14:05:52 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
14:05:52 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
14:05:53 MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
14:05:53 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
14:05:53 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
14:05:54 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
14:05:54 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
14:05:54 MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
14:05:54 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
14:05:54 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
14:05:55 MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
14:05:55 Timing Probabilistic_Noninterference (2 threads, 200.645s elapsed time, 316.740s cpu time, 22.945s GC time, factor 1.58)
14:05:55 Finished Probabilistic_Noninterference (0:03:25 elapsed time, 0:05:22 cpu time, factor 1.57)
14:05:55 Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
14:05:55 Timing S_Finite_Measure_Monad (2 threads, 201.064s elapsed time, 309.135s cpu time, 16.667s GC time, factor 1.54)
14:05:56 MDP-Algorithms: theory Show.Show_Instances
14:05:56 Finished S_Finite_Measure_Monad (0:03:25 elapsed time, 0:05:14 cpu time, factor 1.53)
14:05:56 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
14:05:56 MDP-Algorithms: theory VectorSpace.FunctionLemmas
14:05:56 MDP-Algorithms: theory VectorSpace.RingModuleFacts
14:05:58 MDP-Algorithms: theory VectorSpace.MonoidSums
14:05:58 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
14:05:58 Timing Registers (2 threads, 203.931s elapsed time, 330.339s cpu time, 26.237s GC time, factor 1.62)
14:05:58 Finished Registers (0:03:29 elapsed time, 0:05:36 cpu time, factor 1.61)
14:06:00 Timing Szemeredi_Regularity (2 threads, 9.229s elapsed time, 13.114s cpu time, 0.466s GC time, factor 1.42)
14:06:00 Finished Szemeredi_Regularity (0:00:13 elapsed time, 0:00:16 cpu time, factor 1.28)
14:06:00 Timing List_Update (2 threads, 188.771s elapsed time, 315.999s cpu time, 40.507s GC time, factor 1.67)
14:06:00 Finished List_Update (0:03:27 elapsed time, 0:05:48 cpu time, factor 1.68)
14:06:01 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
14:06:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
14:06:02 Timing IMO2019 (2 threads, 11.150s elapsed time, 13.186s cpu time, 0.865s GC time, factor 1.18)
14:06:02 Finished IMO2019 (0:00:15 elapsed time, 0:00:16 cpu time, factor 1.11)
14:06:03 MDP-Algorithms: theory VectorSpace.LinearCombinations
14:06:03 Timing Random_Graph_Subgraph_Threshold (2 threads, 12.930s elapsed time, 20.184s cpu time, 0.661s GC time, factor 1.56)
14:06:04 Finished Random_Graph_Subgraph_Threshold (0:00:16 elapsed time, 0:00:23 cpu time, factor 1.42)
14:06:04 Timing Roth_Arithmetic_Progressions (2 threads, 209.816s elapsed time, 353.413s cpu time, 64.469s GC time, factor 1.68)
14:06:04 Finished Roth_Arithmetic_Progressions (0:03:34 elapsed time, 0:06:00 cpu time, factor 1.68)
14:06:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
14:06:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
14:06:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
14:06:10 MDP-Algorithms: theory VectorSpace.SumSpaces
14:06:10 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
14:06:11 MDP-Algorithms: theory VectorSpace.VectorSpace
14:06:14 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
14:06:18 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
14:06:18 MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
14:06:19 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
14:06:20 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
14:06:20 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
14:06:20 Timing Irrational_Series_Erdos_Straus (2 threads, 30.230s elapsed time, 51.028s cpu time, 2.752s GC time, factor 1.69)
14:06:20 Finished Irrational_Series_Erdos_Straus (0:00:34 elapsed time, 0:00:55 cpu time, factor 1.60)
14:06:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
14:06:27 MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
14:06:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
14:06:37 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
14:06:38 MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
14:06:40 MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
14:06:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
14:06:43 Timing Markov_Models (2 threads, 206.622s elapsed time, 339.848s cpu time, 21.843s GC time, factor 1.64)
14:06:43 Finished Markov_Models (0:04:25 elapsed time, 0:06:54 cpu time, factor 1.56)
14:06:43 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:06:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
14:06:47 Running Stochastic_Matrices (on 10.195.8.49) ...
14:06:47 Running Probabilistic_Timed_Automata (on 10.195.8.49) ...
14:06:47 Running Hidden_Markov_Models (on 10.195.8.49) ...
14:06:48 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
14:06:48 MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
14:06:48 MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
14:06:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
14:06:49 Timing Zeta_3_Irrational (2 threads, 58.397s elapsed time, 108.086s cpu time, 5.542s GC time, factor 1.85)
14:06:49 Finished Zeta_3_Irrational (0:01:02 elapsed time, 0:01:52 cpu time, factor 1.80)
14:06:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
14:06:50 Stochastic_Matrices: theory HOL-Eisbach.Eisbach
14:06:50 Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
14:06:51 Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
14:06:51 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
14:06:51 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
14:06:51 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
14:06:51 Probabilistic_Timed_Automata: theory Timed_Automata.Misc
14:06:52 Stochastic_Matrices: theory HOL-Algebra.Congruence
14:06:52 Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
14:06:52 MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
14:06:52 Stochastic_Matrices: theory HOL-Algebra.Order
14:06:52 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
14:06:52 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
14:06:53 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
14:06:53 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
14:06:53 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
14:06:53 Hidden_Markov_Models: theory HOL-Library.State_Monad
14:06:53 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
14:06:53 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
14:06:53 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
14:06:53 Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
14:06:53 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
14:06:53 Stochastic_Matrices: theory HOL-Library.Function_Algebras
14:06:54 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
14:06:54 Stochastic_Matrices: theory HOL-Library.More_List
14:06:54 Stochastic_Matrices: theory HOL-Algebra.Lattice
14:06:54 Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
14:06:54 Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
14:06:55 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
14:06:55 Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
14:06:55 Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
14:06:55 Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
14:06:55 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
14:06:55 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
14:06:56 Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
14:06:56 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
14:06:57 Stochastic_Matrices: theory HOL-Algebra.Group
14:06:57 Timing LLL_Basis_Reduction (2 threads, 245.740s elapsed time, 403.399s cpu time, 31.457s GC time, factor 1.64)
14:06:57 Finished LLL_Basis_Reduction (0:04:49 elapsed time, 0:07:40 cpu time, factor 1.59)
14:06:58 Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
14:06:58 MDP-Algorithms: theory MDP-Algorithms.PI_Code
14:06:58 Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
14:06:59 Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
14:06:59 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
14:06:59 Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
14:06:59 Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
14:06:59 Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
14:06:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
14:06:59 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
14:07:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
14:07:00 Stochastic_Matrices: theory HOL-Algebra.Coset
14:07:01 Hidden_Markov_Models: theory Monad_Memo_DP.Memory
14:07:02 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
14:07:02 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
14:07:03 Probabilistic_Timed_Automata: theory Timed_Automata.DBM
14:07:03 Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
14:07:03 Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
14:07:03 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
14:07:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
14:07:04 Stochastic_Matrices: theory HOL-Algebra.Ring
14:07:05 Probabilistic_Timed_Automata: theory Timed_Automata.Regions
14:07:05 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
14:07:05 Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
14:07:06 Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
14:07:07 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
14:07:07 Stochastic_Matrices: theory HOL-Algebra.Module
14:07:08 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
14:07:08 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
14:07:09 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
14:07:09 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
14:07:09 Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:07:09 Probabilistic_Timed_Automata: theory Timed_Automata.Closure
14:07:10 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
14:07:11 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
14:07:12 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
14:07:12 Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
14:07:12 Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:07:12 Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
14:07:12 Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
14:07:14 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
14:07:15 Building Linear_Inequalities (on 10.195.7.194) ...
14:07:15 Running LLL_Factorization (on 10.195.7.194) ...
14:07:16 Timing Smith_Normal_Form (6 threads, 172.700s elapsed time, 692.011s cpu time, 163.950s GC time, factor 4.01)
14:07:16 Finished Smith_Normal_Form (0:03:19 elapsed time, 0:12:23 cpu time, factor 3.73)
14:07:17 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
14:07:17 Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
14:07:17 Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
14:07:17 Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
14:07:18 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
14:07:18 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
14:07:19 Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
14:07:20 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
14:07:20 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
14:07:20 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
14:07:20 Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
14:07:21 LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
14:07:21 LLL_Factorization: theory LLL_Factorization.Sub_Sums
14:07:22 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
14:07:22 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
14:07:22 Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
14:07:23 Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
14:07:23 Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:07:23 Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
14:07:23 Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
14:07:23 Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
14:07:23 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
14:07:24 Stochastic_Matrices: theory VectorSpace.FunctionLemmas
14:07:24 Stochastic_Matrices: theory VectorSpace.RingModuleFacts
14:07:24 Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
14:07:25 Stochastic_Matrices: theory VectorSpace.MonoidSums
14:07:25 Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
14:07:25 Stochastic_Matrices: theory VectorSpace.LinearCombinations
14:07:27 Timing CryptHOL (2 threads, 269.922s elapsed time, 461.479s cpu time, 108.096s GC time, factor 1.71)
14:07:27 Finished CryptHOL (0:05:22 elapsed time, 0:08:44 cpu time, factor 1.62)
14:07:27 Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
14:07:28 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
14:07:29 LLL_Factorization: theory LLL_Factorization.LLL_Factorization
14:07:30 Stochastic_Matrices: theory VectorSpace.SumSpaces
14:07:30 Stochastic_Matrices: theory VectorSpace.VectorSpace
14:07:31 Linear_Inequalities: theory Linear_Inequalities.Cone
14:07:33 Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.8.30) ...
14:07:34 Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
14:07:37 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
14:07:39 Timing Hidden_Markov_Models (2 threads, 47.324s elapsed time, 85.397s cpu time, 7.892s GC time, factor 1.80)
14:07:39 Finished Hidden_Markov_Models (0:00:51 elapsed time, 0:01:29 cpu time, factor 1.74)
14:07:40 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
14:07:40 Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
14:07:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
14:07:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
14:07:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
14:07:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
14:07:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
14:07:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
14:07:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
14:07:46 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
14:07:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
14:07:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
14:07:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
14:07:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
14:07:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
14:07:47 Timing Hermite_Lindemann (2 threads, 188.541s elapsed time, 342.271s cpu time, 19.817s GC time, factor 1.82)
14:07:47 Finished Hermite_Lindemann (0:03:13 elapsed time, 0:05:49 cpu time, factor 1.80)
14:07:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
14:07:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
14:07:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
14:07:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
14:07:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
14:07:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
14:07:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
14:07:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
14:07:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
14:07:51 Linear_Inequalities: theory Linear_Inequalities.Dim_Span
14:07:51 Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
14:07:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
14:07:51 Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
14:07:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
14:07:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
14:07:52 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
14:07:52 Building Constructive_Cryptography (on 10.195.8.29) ...
14:07:53 Building Game_Based_Crypto (on 10.195.8.29) ...
14:07:53 Running Sigma_Commit_Crypto (on 10.195.8.29) ...
14:07:53 Running ABY3_Protocols (on 10.195.8.29) ...
14:07:53 Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
14:07:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
14:07:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
14:07:54 Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
14:07:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
14:07:55 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
14:07:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
14:07:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
14:07:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
14:07:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
14:07:57 Constructive_Cryptography: theory Constructive_Cryptography.Resource
14:07:57 ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
14:07:57 ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
14:07:57 Game_Based_Crypto: theory HOL-Library.LaTeXsugar
14:07:57 Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
14:07:57 Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
14:07:57 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:07:57 Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
14:07:57 Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
14:07:58 ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
14:07:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
14:07:58 Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
14:07:58 Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
14:07:58 Sigma_Commit_Crypto: theory HOL-Algebra.Ring
14:07:59 Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
14:07:59 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
14:07:59 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
14:07:59 Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
14:07:59 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
14:08:00 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
14:08:00 Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
14:08:00 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
14:08:01 Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
14:08:01 ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
14:08:01 Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
14:08:01 ABY3_Protocols: theory ABY3_Protocols.Multiplication
14:08:01 Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
14:08:02 Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
14:08:02 Constructive_Cryptography: theory Constructive_Cryptography.Converter
14:08:02 Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
14:08:02 ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
14:08:02 ABY3_Protocols: theory ABY3_Protocols.Shuffle
14:08:02 Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
14:08:03 Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
14:08:04 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
14:08:05 Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
14:08:05 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
14:08:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
14:08:07 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
14:08:07 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
14:08:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
14:08:07 Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
14:08:08 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
14:08:08 Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
14:08:08 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
14:08:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
14:08:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
14:08:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
14:08:09 Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
14:08:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
14:08:09 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
14:08:10 Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
14:08:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
14:08:10 Sigma_Commit_Crypto: theory HOL-Algebra.Module
14:08:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
14:08:11 Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
14:08:11 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
14:08:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
14:08:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
14:08:13 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
14:08:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
14:08:14 Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
14:08:15 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
14:08:17 Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
14:08:17 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
14:08:17 Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
14:08:17 Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
14:08:18 Constructive_Cryptography: theory Constructive_Cryptography.Random_System
14:08:18 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
14:08:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
14:08:18 Timing ABY3_Protocols (2 threads, 19.772s elapsed time, 34.867s cpu time, 1.633s GC time, factor 1.76)
14:08:18 Finished ABY3_Protocols (0:00:24 elapsed time, 0:00:39 cpu time, factor 1.62)
14:08:19 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
14:08:19 Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
14:08:19 Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
14:08:19 Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
14:08:19 Constructive_Cryptography: theory Constructive_Cryptography.Wiring
14:08:20 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
14:08:23 Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
14:08:23 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
14:08:23 Timing LLL_Factorization (2 threads, 62.516s elapsed time, 119.078s cpu time, 7.378s GC time, factor 1.90)
14:08:23 Finished LLL_Factorization (0:01:07 elapsed time, 0:02:04 cpu time, factor 1.84)
14:08:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
14:08:24 Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
14:08:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
14:08:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
14:08:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
14:08:25 Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
14:08:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
14:08:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
14:08:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
14:08:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
14:08:28 Timing Algebraic_Numbers (2 threads, 332.579s elapsed time, 582.660s cpu time, 33.480s GC time, factor 1.75)
14:08:28 Finished Algebraic_Numbers (0:06:20 elapsed time, 0:10:43 cpu time, factor 1.69)
14:08:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
14:08:29 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
14:08:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
14:08:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
14:08:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
14:08:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
14:08:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
14:08:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
14:08:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
14:08:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
14:08:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
14:08:34 Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
14:08:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
14:08:34 Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
14:08:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
14:08:35 Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
14:08:38 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
14:08:39 Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
14:08:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
14:08:42 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
14:08:43 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
14:08:43 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
14:08:43 Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
14:08:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
14:08:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
14:08:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
14:08:45 Constructive_Cryptography: theory Constructive_Cryptography.Examples
14:08:46 Running Quantifier_Elimination_Hybrid (on 10.195.7.194) ...
14:08:46 Running BenOr_Kozen_Reif (on 10.195.7.194) ...
14:08:46 Running Factor_Algebraic_Polynomial (on 10.195.7.194) ...
14:08:46 Running Cubic_Quartic_Equations (on 10.195.7.194) ...
14:08:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
14:08:46 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
14:08:46 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
14:08:50 BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc
14:08:50 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix
14:08:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
14:08:50 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
14:08:50 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
14:08:50 Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
14:08:50 BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski
14:08:50 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
14:08:50 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
14:08:51 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
14:08:51 Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
14:08:51 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux
14:08:51 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type
14:08:51 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
14:08:51 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
14:08:52 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator
14:08:52 Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
14:08:52 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
14:08:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
14:08:52 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
14:08:52 Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules
14:08:52 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
14:08:52 Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type
14:08:52 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
14:08:53 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
14:08:53 Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
14:08:53 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
14:08:53 Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots
14:08:53 Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map
14:08:53 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate
14:08:53 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
14:08:53 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta
14:08:54 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc
14:08:54 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm
14:08:54 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski
14:08:54 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
14:08:54 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
14:08:55 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials
14:08:55 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
14:08:56 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
14:08:56 Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates
14:08:56 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence
14:08:56 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
14:08:57 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs
14:08:57 Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
14:08:58 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
14:08:58 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
14:08:58 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm
14:08:59 Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
14:08:59 Factor_Algebraic_Polynomial: theory Polynomials.Utils
14:08:59 Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials
14:08:59 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
14:08:59 Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
14:08:59 Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
14:08:59 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
14:09:00 Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
14:09:00 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision
14:09:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
14:09:00 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix
14:09:00 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs
14:09:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
14:09:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
14:09:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
14:09:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
14:09:03 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
14:09:04 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm
14:09:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
14:09:08 Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials
14:09:08 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
14:09:08 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm
14:09:08 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs
14:09:09 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision
14:09:10 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences
14:09:10 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs
14:09:10 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements
14:09:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
14:09:10 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum
14:09:10 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full
14:09:11 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision
14:09:12 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences
14:09:12 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations
14:09:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
14:09:12 Quantifier_Elimination_Hybrid: theory Polynomials.Utils
14:09:13 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders
14:09:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
14:09:13 Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products
14:09:14 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
14:09:14 Timing Cubic_Quartic_Equations (2 threads, 22.204s elapsed time, 35.495s cpu time, 2.528s GC time, factor 1.60)
14:09:14 Finished Cubic_Quartic_Equations (0:00:26 elapsed time, 0:00:40 cpu time, factor 1.49)
14:09:14 Timing Linear_Inequalities (2 threads, 79.430s elapsed time, 147.267s cpu time, 14.211s GC time, factor 1.85)
14:09:14 Finished Linear_Inequalities (0:01:57 elapsed time, 0:03:08 cpu time, factor 1.60)
14:09:14 Running LP_Duality (on 10.195.7.194) ...
14:09:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
14:09:16 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
14:09:16 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
14:09:16 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision
14:09:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
14:09:17 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
14:09:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
14:09:17 LP_Duality: theory LP_Duality.Minimum_Maximum
14:09:18 LP_Duality: theory LP_Duality.LP_Duality
14:09:18 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
14:09:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
14:09:19 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified
14:09:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
14:09:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
14:09:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
14:09:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
14:09:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
14:09:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
14:09:25 Timing LP_Duality (2 threads, 7.221s elapsed time, 8.830s cpu time, 0.230s GC time, factor 1.22)
14:09:25 Finished LP_Duality (0:00:11 elapsed time, 0:00:12 cpu time, factor 1.09)
14:09:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
14:09:26 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class
14:09:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
14:09:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
14:09:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
14:09:29 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
14:09:29 Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection
14:09:29 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered
14:09:31 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
14:09:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
14:09:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
14:09:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
14:09:34 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
14:09:35 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
14:09:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
14:09:37 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
14:09:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
14:09:41 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
14:09:41 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap
14:09:41 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
14:09:43 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension
14:09:43 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE
14:09:44 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
14:09:44 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
14:09:44 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps
14:09:46 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms
14:09:55 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn
14:09:55 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting
14:09:56 Timing Game_Based_Crypto (2 threads, 67.440s elapsed time, 121.742s cpu time, 8.138s GC time, factor 1.81)
14:09:56 Finished Game_Based_Crypto (0:02:01 elapsed time, 0:03:04 cpu time, factor 1.52)
14:09:59 Running Multi_Party_Computation (on 10.195.8.49) ...
14:10:00 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations
14:10:00 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex
14:10:02 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms
14:10:03 Multi_Party_Computation: theory HOL-Number_Theory.Cong
14:10:03 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
14:10:04 Multi_Party_Computation: theory HOL-Algebra.Ring
14:10:04 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
14:10:06 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
14:10:07 Multi_Party_Computation: theory HOL-Number_Theory.Totient
14:10:08 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs
14:10:08 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos
14:10:08 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
14:10:08 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
14:10:11 Multi_Party_Computation: theory HOL-Algebra.Module
14:10:12 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
14:10:13 Multi_Party_Computation: theory HOL-Algebra.Ideal
14:10:17 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
14:10:17 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
14:10:18 Multi_Party_Computation: theory Multi_Party_Computation.ETP
14:10:18 Multi_Party_Computation: theory HOL-Algebra.RingHom
14:10:19 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
14:10:20 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
14:10:20 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF
14:10:20 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
14:10:20 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic
14:10:20 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
14:10:21 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
14:10:26 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase
14:10:26 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity
14:10:27 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase
14:10:27 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni
14:10:28 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
14:10:28 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable
14:10:28 Timing Factor_Algebraic_Polynomial (2 threads, 95.462s elapsed time, 172.487s cpu time, 14.194s GC time, factor 1.81)
14:10:28 Finished Factor_Algebraic_Polynomial (0:01:40 elapsed time, 0:02:59 cpu time, factor 1.77)
14:10:29 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind
14:10:29 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS
14:10:29 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals
14:10:29 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports
14:10:30 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni
14:10:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni
14:10:32 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs
14:10:33 Multi_Party_Computation: theory Multi_Party_Computation.OT14
14:10:34 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad
14:10:35 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props
14:10:36 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
14:10:36 Multi_Party_Computation: theory Multi_Party_Computation.GMW
14:10:37 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs
14:10:37 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments
14:10:37 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
14:10:37 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs
14:10:38 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence
14:10:39 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
14:10:40 Multi_Party_Computation: theory HOL-Number_Theory.Residues
14:10:44 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
14:10:44 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
14:10:45 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
14:10:45 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
14:10:45 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
14:10:45 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
14:10:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
14:10:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
14:10:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
14:10:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
14:10:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
14:10:51 Timing Sigma_Commit_Crypto (2 threads, 171.135s elapsed time, 299.337s cpu time, 25.487s GC time, factor 1.75)
14:10:51 Finished Sigma_Commit_Crypto (0:02:56 elapsed time, 0:05:05 cpu time, factor 1.73)
14:10:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
14:10:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
14:10:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
14:10:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
14:11:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
14:11:00 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
14:11:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
14:11:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
14:11:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
14:11:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
14:11:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
14:11:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
14:11:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
14:11:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
14:11:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
14:11:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
14:11:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
14:11:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
14:11:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
14:11:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
14:11:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
14:11:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
14:11:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
14:11:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
14:11:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
14:11:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
14:11:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
14:11:22 Timing Cook_Levin (2 threads, 1977.796s elapsed time, 3316.546s cpu time, 258.614s GC time, factor 1.68)
14:11:22 Finished Cook_Levin (0:33:03 elapsed time, 0:55:25 cpu time, factor 1.68)
14:11:25 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
14:11:31 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
14:11:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
14:11:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
14:11:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
14:11:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
14:11:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
14:11:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
14:11:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
14:11:49 Timing BenOr_Kozen_Reif (2 threads, 176.851s elapsed time, 288.564s cpu time, 23.389s GC time, factor 1.63)
14:11:49 Finished BenOr_Kozen_Reif (0:03:01 elapsed time, 0:04:54 cpu time, factor 1.62)
14:11:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
14:11:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
14:12:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
14:12:32 Timing Constructive_Cryptography (2 threads, 217.159s elapsed time, 353.195s cpu time, 15.547s GC time, factor 1.63)
14:12:32 Finished Constructive_Cryptography (0:04:37 elapsed time, 0:07:06 cpu time, factor 1.54)
14:12:33 Running Constructive_Cryptography_CM (on 10.195.8.29) ...
14:12:37 *** Host "10.195.8.49": failed to work
14:12:37 *** ### Ignored report message: int
14:12:37 *** ### Ignored report message: array\ int
14:12:37 *** ### Ignored report message: int
14:12:37 Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
14:12:37 Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
14:12:40 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
14:12:49 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
14:12:51 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
14:12:51 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
14:12:52 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
14:13:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
14:13:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
14:13:25 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
14:13:27 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
14:13:40 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
14:13:41 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
14:13:57 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
14:13:57 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
14:13:57 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
14:14:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
14:14:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
14:14:47 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
14:16:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
14:16:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
14:16:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
14:16:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
14:16:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
14:16:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
14:17:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
14:17:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
14:17:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
14:18:35 Timing Expander_Graphs (2 threads, 919.677s elapsed time, 1578.158s cpu time, 478.766s GC time, factor 1.72)
14:18:35 Finished Expander_Graphs (0:16:31 elapsed time, 0:27:52 cpu time, factor 1.69)
14:18:36 Running Distributed_Distinct_Elements (on 10.195.8.30) ...
14:18:41 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
14:18:41 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
14:18:41 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
14:18:41 Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
14:18:42 Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
14:18:42 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
14:18:43 Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
14:18:43 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
14:18:50 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
14:18:51 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
14:18:51 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
14:18:52 Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
14:18:52 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
14:18:53 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
14:18:57 Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
14:18:58 Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
14:18:58 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
14:18:59 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
14:19:04 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
14:19:06 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
14:19:06 Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
14:19:08 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
14:19:11 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
14:19:11 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
14:19:20 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
14:19:21 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
14:19:28 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
14:19:30 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
14:19:31 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
14:19:33 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
14:20:38 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
14:20:52 Timing Distributed_Distinct_Elements (2 threads, 128.192s elapsed time, 238.781s cpu time, 15.035s GC time, factor 1.86)
14:20:52 Finished Distributed_Distinct_Elements (0:02:13 elapsed time, 0:04:05 cpu time, factor 1.83)
14:21:17 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
14:22:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
14:23:03 Timing MDP-Algorithms (2 threads, 1251.629s elapsed time, 2182.211s cpu time, 777.300s GC time, factor 1.74)
14:23:03 Finished MDP-Algorithms (0:21:01 elapsed time, 0:36:38 cpu time, factor 1.74)
14:25:53 Timing Quantifier_Elimination_Hybrid (2 threads, 1012.630s elapsed time, 1730.340s cpu time, 274.768s GC time, factor 1.71)
14:25:53 Finished Quantifier_Elimination_Hybrid (0:17:01 elapsed time, 0:29:04 cpu time, factor 1.71)
14:26:02 Timing Constructive_Cryptography_CM (2 threads, 799.876s elapsed time, 1496.752s cpu time, 245.775s GC time, factor 1.87)
14:26:02 Finished Constructive_Cryptography_CM (0:13:26 elapsed time, 0:25:07 cpu time, factor 1.87)
14:47:52 Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2397.733s elapsed time, 4367.301s cpu time, 1051.706s GC time, factor 1.82)
14:47:52 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:40:11 elapsed time, 1:13:10 cpu time, factor 1.82)
14:48:01 Estimated 0:08:11 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.131s)
14:52:09 Timing HOL-ODE-Numerics (2 threads, 2893.297s elapsed time, 5327.341s cpu time, 1185.665s GC time, factor 1.84)
14:52:09 Finished HOL-ODE-Numerics (0:50:07 elapsed time, 1:31:20 cpu time, factor 1.82)
14:52:10 Building Lorenz_Approximation (on 10.195.8.30) ...
14:52:10 Running HOL-ODE-ARCH-COMP (on 10.195.8.30) ...
14:52:10 Running HOL-ODE-Examples (on 10.195.8.30) ...
14:52:10 Running Poincare_Bendixson (on 10.195.8.30) ...
14:52:15 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
14:52:15 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
14:52:15 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
14:52:15 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
14:52:15 Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
14:52:15 Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
14:52:16 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
14:52:17 Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
14:52:19 Estimated 0:11:55 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.131s)
14:52:20 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
14:52:21 Poincare_Bendixson: theory Poincare_Bendixson.Invariance
14:52:24 Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
14:52:27 Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
14:52:29 Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
14:52:36 Poincare_Bendixson: theory Poincare_Bendixson.Examples
14:52:43 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
14:53:58 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
14:54:38 Timing Poincare_Bendixson (2 threads, 141.629s elapsed time, 215.341s cpu time, 10.221s GC time, factor 1.52)
14:54:38 Finished Poincare_Bendixson (0:02:26 elapsed time, 0:03:41 cpu time, factor 1.50)
14:58:52 Timing Lorenz_Approximation (2 threads, 343.601s elapsed time, 643.437s cpu time, 88.027s GC time, factor 1.87)
14:58:52 Finished Lorenz_Approximation (0:06:40 elapsed time, 0:11:59 cpu time, factor 1.80)
14:58:54 Running Lorenz_C0 (on 10.195.8.30) ...
14:58:54 Running Lorenz_C1 (on 10.195.8.30) ...
14:58:58 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
14:58:58 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
14:59:01 Timing Lorenz_C1 (2 threads, 1.981s elapsed time, 2.597s cpu time, 0.057s GC time, factor 1.31)
14:59:01 Finished Lorenz_C1 (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.07)
14:59:10 Estimated 0:25:03 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.064s)
14:59:16 Timing HOL-ODE-Examples (2 threads, 420.011s elapsed time, 726.347s cpu time, 36.107s GC time, factor 1.73)
14:59:16 Finished HOL-ODE-Examples (0:07:05 elapsed time, 0:12:11 cpu time, factor 1.72)
14:59:32 Timing HOL-ODE-ARCH-COMP (2 threads, 435.668s elapsed time, 838.637s cpu time, 70.338s GC time, factor 1.92)
14:59:32 Finished HOL-ODE-ARCH-COMP (0:07:21 elapsed time, 0:14:04 cpu time, factor 1.91)
15:26:18 Timing Lorenz_C0 (2 threads, 1639.426s elapsed time, 3208.161s cpu time, 85.026s GC time, factor 1.96)
15:26:18 Finished Lorenz_C0 (0:27:23 elapsed time, 0:53:32 cpu time, factor 1.95)
15:26:27 Estimated 0:00:33 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1)) (took 0.175s)
16:17:08 Build timed out (after 200 minutes). Marking the build as failed.
16:17:08 Build was aborted
16:17:08 Started calculate disk usage of build
16:17:09 Finished Calculation of disk usage of build in 0 seconds
16:17:26 Started calculate disk usage of workspace
16:17:26 Finished Calculation of disk usage of workspace in 0 seconds
16:17:27 Finished: FAILURE