Skipping 886 KB.. Full Log

Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
01:40:10 Timing Transcendence_Series_Hancl_Rucki (6 threads, 117.583s elapsed time, 453.766s cpu time, 109.999s GC time, factor 3.86)
01:40:10 Finished Transcendence_Series_Hancl_Rucki (0:01:59 elapsed time, 0:07:38 cpu time, factor 3.83)
01:40:11 Timing Source_Coding_Theorem (2 threads, 6.232s elapsed time, 9.508s cpu time, 0.261s GC time, factor 1.53)
01:40:11 Finished Source_Coding_Theorem (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.33)
01:40:11 Universal_Hash_Families: theory HOL-Algebra.Polynomials
01:40:11 Timing Median_Method (2 threads, 10.268s elapsed time, 15.771s cpu time, 0.514s GC time, factor 1.54)
01:40:11 Finished Median_Method (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.38)
01:40:11 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
01:40:12 MDP-Algorithms: theory HOL-Algebra.Module
01:40:13 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
01:40:14 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
01:40:14 Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
01:40:14 Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
01:40:14 Timing Randomised_Social_Choice (2 threads, 31.578s elapsed time, 47.846s cpu time, 3.125s GC time, factor 1.52)
01:40:14 Finished Randomised_Social_Choice (0:01:02 elapsed time, 0:01:23 cpu time, factor 1.33)
01:40:14 MDP-Algorithms: theory Containers.Collection_Order
01:40:15 Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
01:40:15 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:40:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
01:40:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
01:40:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
01:40:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
01:40:16 DOM_Components: theory DOM_Components.Shadow_DOM_Components
01:40:16 Deep_Learning: theory Jordan_Normal_Form.DL_Rank
01:40:16 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
01:40:17 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
01:40:17 MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
01:40:17 Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
01:40:18 MDP-Algorithms: theory HOL-Library.RBT_Impl
01:40:18 Timing Skip_Lists (2 threads, 19.189s elapsed time, 32.666s cpu time, 0.866s GC time, factor 1.70)
01:40:18 Finished Skip_Lists (0:00:22 elapsed time, 0:00:35 cpu time, factor 1.58)
01:40:18 Timing Hahn_Jordan_Decomposition (2 threads, 41.845s elapsed time, 57.636s cpu time, 2.848s GC time, factor 1.38)
01:40:18 Finished Hahn_Jordan_Decomposition (0:00:45 elapsed time, 0:01:01 cpu time, factor 1.34)
01:40:18 Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
01:40:19 Frequency_Moments: theory HOL-Algebra.Polynomials
01:40:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
01:40:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
01:40:19 Frequency_Moments: theory HOL-Number_Theory.Totient
01:40:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
01:40:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
01:40:20 Timing Ordinary_Differential_Equations (2 threads, 376.466s elapsed time, 629.416s cpu time, 104.737s GC time, factor 1.67)
01:40:20 Finished Ordinary_Differential_Equations (0:06:58 elapsed time, 0:11:23 cpu time, factor 1.63)
01:40:20 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
01:40:20 MDP-Algorithms: theory HOL-Data_Structures.Tree2
01:40:20 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
01:40:20 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
01:40:21 MDP-Algorithms: theory HOL-Data_Structures.Isin2
01:40:21 Frequency_Moments: theory HOL-Number_Theory.Residues
01:40:22 MDP-Algorithms: theory HOL-Data_Structures.Lookup2
01:40:22 MDP-Algorithms: theory HOL-Data_Structures.RBT
01:40:23 Building Hermite (on of3.proof.cit.tum.de) ...
01:40:24 Running Perron_Frobenius (on of3.proof.cit.tum.de) ...
01:40:24 Hermite: theory Hermite.Hermite
01:40:24 Building Subresultants (on of3.proof.cit.tum.de) ...
01:40:25 Timing Executable_Randomized_Algorithms (8 threads, 88.549s elapsed time, 570.383s cpu time, 55.235s GC time, factor 6.44)
01:40:25 Finished Executable_Randomized_Algorithms (0:01:30 elapsed time, 0:09:36 cpu time, factor 6.35)
01:40:26 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
01:40:26 Subresultants: theory Subresultants.Coeff_Int
01:40:26 Subresultants: theory Subresultants.Dichotomous_Lazard
01:40:26 Subresultants: theory Subresultants.Resultant_Prelim
01:40:26 Subresultants: theory Subresultants.Binary_Exponentiation
01:40:26 Subresultants: theory Subresultants.More_Homomorphisms
01:40:26 Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
01:40:26 Timing Treaps (2 threads, 67.539s elapsed time, 114.543s cpu time, 5.893s GC time, factor 1.70)
01:40:26 Finished Treaps (0:01:11 elapsed time, 0:01:58 cpu time, factor 1.66)
01:40:26 Hermite: theory Hermite.Hermite_IArrays
01:40:27 Frequency_Moments: theory HOL-Number_Theory.Gauss
01:40:27 Timing Probabilistic_System_Zoo (2 threads, 67.601s elapsed time, 120.055s cpu time, 10.249s GC time, factor 1.78)
01:40:27 Finished Probabilistic_System_Zoo (0:01:11 elapsed time, 0:02:05 cpu time, factor 1.74)
01:40:27 MDP-Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
01:40:27 Subresultants: theory Subresultants.Subresultant
01:40:27 Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
01:40:28 MDP-Algorithms: theory Perron_Frobenius.Cancel_Card_Constraint
01:40:28 Perron_Frobenius: theory Pure-ex.Guess
01:40:28 Perron_Frobenius: theory HOL-Eisbach.Eisbach
01:40:28 Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets
01:40:28 Perron_Frobenius: theory HOL-Analysis.Metric_Arith
01:40:28 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology
01:40:28 Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable
01:40:28 Running QHLProver (on of2.proof.cit.tum.de) ...
01:40:28 Perron_Frobenius: theory HOL-Analysis.Inner_Product
01:40:28 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Unsorted
01:40:28 Timing Probabilistic_Prime_Tests (8 threads, 91.487s elapsed time, 528.429s cpu time, 74.235s GC time, factor 5.78)
01:40:28 Finished Probabilistic_Prime_Tests (0:01:34 elapsed time, 0:08:56 cpu time, factor 5.68)
01:40:29 Running Linear_Programming (on of2.proof.cit.tum.de) ...
01:40:29 Perron_Frobenius: theory HOL-Analysis.L2_Norm
01:40:29 Frequency_Moments: theory HOL-Number_Theory.Pocklington
01:40:29 Timing Groebner_Bases (2 threads, 883.996s elapsed time, 1658.963s cpu time, 631.050s GC time, factor 1.88)
01:40:29 Finished Groebner_Bases (0:16:09 elapsed time, 0:29:36 cpu time, factor 1.83)
01:40:29 Perron_Frobenius: theory HOL-Analysis.Operator_Norm
01:40:29 Timing Monomorphic_Monad (2 threads, 52.395s elapsed time, 89.382s cpu time, 9.757s GC time, factor 1.71)
01:40:29 Perron_Frobenius: theory HOL-Analysis.Product_Vector
01:40:29 Finished Monomorphic_Monad (0:00:56 elapsed time, 0:01:34 cpu time, factor 1.66)
01:40:29 Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Irreducibility
01:40:30 Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial
01:40:30 Building Pi_Transcendental (on of2.proof.cit.tum.de) ...
01:40:30 Running Isabelle_Marries_Dirac (on of2.proof.cit.tum.de) ...
01:40:30 Perron_Frobenius: theory HOL-Analysis.Norm_Arith
01:40:30 Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
01:40:30 Perron_Frobenius: theory Matrix.Utility
01:40:30 Timing Lp (2 threads, 53.214s elapsed time, 84.483s cpu time, 2.885s GC time, factor 1.59)
01:40:30 Finished Lp (0:00:57 elapsed time, 0:01:28 cpu time, factor 1.55)
01:40:30 QHLProver: theory Deep_Learning.Tensor
01:40:30 QHLProver: theory QHLProver.Complex_Matrix
01:40:30 Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
01:40:30 Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order
01:40:30 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial
01:40:30 Running Linear_Recurrences (on of4.proof.cit.tum.de) ...
01:40:30 QHLProver: theory Deep_Learning.Tensor_Subtensor
01:40:30 QHLProver: theory Deep_Learning.Tensor_Plus
01:40:31 QHLProver: theory Deep_Learning.Tensor_Matricization
01:40:31 Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization
01:40:31 Perron_Frobenius: theory Sturm_Sequences.Sturm_Library
01:40:31 Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem
01:40:31 Linear_Programming: theory Simplex.Simplex_Auxiliary
01:40:31 Linear_Programming: theory Simplex.Simplex_Algebra
01:40:31 Linear_Programming: theory Linear_Programming.More_Jordan_Normal_Forms
01:40:31 Running Fisher_Yates (on of4.proof.cit.tum.de) ...
01:40:31 Running Monad_Normalisation (on of4.proof.cit.tum.de) ...
01:40:31 Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
01:40:31 Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
01:40:31 Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
01:40:31 Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
01:40:31 Pi_Transcendental: theory HOL-Library.Fun_Lexorder
01:40:31 Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
01:40:31 Linear_Programming: theory Simplex.Rel_Chain
01:40:31 Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:40:32 Isabelle_Marries_Dirac: theory Matrix.Utility
01:40:32 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Basics
01:40:32 Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers
01:40:32 Linear_Recurrences: theory HOL-Combinatorics.Stirling
01:40:32 Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure
01:40:32 Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat
01:40:32 Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree
01:40:32 Linear_Recurrences: theory HOL-Library.Code_Target_Int
01:40:32 Subresultants: theory Subresultants.Subresultant_Gcd
01:40:32 Pi_Transcendental: theory HOL-Library.Poly_Mapping
01:40:32 Linear_Recurrences: theory HOL-Library.Code_Target_Nat
01:40:32 Linear_Recurrences: theory HOL-Library.Sublist
01:40:32 Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial
01:40:32 Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Irreducibility
01:40:32 Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
01:40:32 Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials
01:40:32 Perron_Frobenius: theory HOL-Analysis.Elementary_Topology
01:40:32 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Binary_Nat
01:40:32 Linear_Recurrences: theory Matrix.Utility
01:40:32 Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:40:32 Isabelle_Marries_Dirac: theory Matrix.Matrix_Legacy
01:40:32 Perron_Frobenius: theory HOL-Analysis.Euclidean_Space
01:40:32 Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
01:40:32 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum
01:40:32 Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
01:40:33 Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
01:40:33 Perron_Frobenius: theory Sturm_Sequences.Sturm_Method
01:40:33 Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
01:40:33 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
01:40:33 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
01:40:33 Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
01:40:33 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
01:40:33 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
01:40:33 Linear_Recurrences: theory Linear_Recurrences.RatFPS
01:40:33 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
01:40:34 QHLProver: theory QHLProver.Gates
01:40:34 Linear_Recurrences: theory Linear_Recurrences.Factorizations
01:40:34 QHLProver: theory QHLProver.Matrix_Limit
01:40:34 Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
01:40:34 Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
01:40:34 Linear_Programming: theory Simplex.Abstract_Linear_Poly
01:40:34 Pi_Transcendental: theory Polynomials.MPoly_Type
01:40:34 Isabelle_Marries_Dirac: theory Matrix_Tensor.Matrix_Tensor
01:40:34 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Complex_Vectors
01:40:34 Timing Monad_Normalisation (6 threads, 1.008s elapsed time, 1.319s cpu time, 0.063s GC time, factor 1.31)
01:40:34 Finished Monad_Normalisation (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.01)
01:40:35 Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
01:40:35 Timing Fisher_Yates (6 threads, 1.657s elapsed time, 4.298s cpu time, 0.161s GC time, factor 2.59)
01:40:35 Finished Fisher_Yates (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.66)
01:40:35 Timing Quasi_Borel_Spaces (2 threads, 75.580s elapsed time, 120.010s cpu time, 10.281s GC time, factor 1.59)
01:40:35 Finished Quasi_Borel_Spaces (0:01:19 elapsed time, 0:02:04 cpu time, factor 1.56)
01:40:35 Perron_Frobenius: theory HOL-Analysis.Abstract_Limits
01:40:35 Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product
01:40:35 Perron_Frobenius: theory HOL-Analysis.Linear_Algebra
01:40:35 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Measurement
01:40:35 Linear_Programming: theory Simplex.QDelta
01:40:35 Linear_Programming: theory Simplex.Linear_Poly_Maps
01:40:35 Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
01:40:35 QHLProver: theory QHLProver.Quantum_Program
01:40:35 Pi_Transcendental: theory Polynomials.More_MPoly_Type
01:40:35 Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
01:40:36 Linear_Programming: theory Simplex.Simplex
01:40:36 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2
01:40:36 Perron_Frobenius: theory HOL-Analysis.Infinite_Sum
01:40:36 Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
01:40:36 Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
01:40:36 Running SDS_Impossibility (on 10.195.8.49) ...
01:40:36 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
01:40:36 Pi_Transcendental: theory Symmetric_Polynomials.Vieta
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Tensor
01:40:37 QHLProver: theory QHLProver.Partial_State
01:40:37 QHLProver: theory QHLProver.Quantum_Hoare
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.More_Tensor
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.No_Cloning
01:40:37 Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch
01:40:37 Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Entanglement
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma
01:40:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Teleportation
01:40:37 Perron_Frobenius: theory HOL-Analysis.Affine
01:40:38 Perron_Frobenius: theory HOL-Analysis.Cartesian_Space
01:40:38 Perron_Frobenius: theory HOL-Analysis.Convex
01:40:38 Perron_Frobenius: theory HOL-Analysis.Connected
01:40:39 Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces
01:40:39 Perron_Frobenius: theory HOL-Analysis.Function_Topology
01:40:39 QHLProver: theory QHLProver.Grover
01:40:39 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
01:40:39 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch_Jozsa
01:40:40 Perron_Frobenius: theory HOL-Analysis.Product_Topology
01:40:40 Perron_Frobenius: theory HOL-Analysis.T1_Spaces
01:40:40 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
01:40:40 Perron_Frobenius: theory HOL-Analysis.Determinants
01:40:40 Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces
01:40:41 MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:40:41 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
01:40:41 Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space
01:40:43 Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space
01:40:43 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
01:40:43 Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits
01:40:43 Perron_Frobenius: theory HOL-Analysis.Line_Segment
01:40:44 Timing Lovasz_Local (2 threads, 91.340s elapsed time, 169.626s cpu time, 12.139s GC time, factor 1.86)
01:40:44 Finished Lovasz_Local (0:01:35 elapsed time, 0:02:53 cpu time, factor 1.83)
01:40:44 MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
01:40:45 Perron_Frobenius: theory HOL-Analysis.Starlike
01:40:45 Perron_Frobenius: theory HOL-Analysis.Summation_Tests
01:40:45 MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:40:45 Timing Fourier (2 threads, 89.481s elapsed time, 150.248s cpu time, 7.884s GC time, factor 1.68)
01:40:45 Finished Fourier (0:01:33 elapsed time, 0:02:34 cpu time, factor 1.65)
01:40:45 MDP-Algorithms: theory HOL-Data_Structures.RBT_Set
01:40:45 Perron_Frobenius: theory HOL-Analysis.Uniform_Limit
01:40:45 Timing Applicative_Lifting (2 threads, 51.177s elapsed time, 74.444s cpu time, 6.813s GC time, factor 1.45)
01:40:45 Finished Applicative_Lifting (0:01:32 elapsed time, 0:02:04 cpu time, factor 1.34)
01:40:46 Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function
01:40:46 Perron_Frobenius: theory HOL-Analysis.Path_Connected
01:40:47 Timing Probabilistic_While (2 threads, 78.948s elapsed time, 109.361s cpu time, 4.474s GC time, factor 1.39)
01:40:47 Finished Probabilistic_While (0:02:06 elapsed time, 0:02:39 cpu time, factor 1.26)
01:40:47 Perron_Frobenius: theory HOL-Analysis.Uncountable_Sets
01:40:47 Perron_Frobenius: theory HOL-Analysis.Derivative
01:40:48 Perron_Frobenius: theory HOL-Analysis.Homotopy
01:40:48 MDP-Algorithms: theory HOL-Data_Structures.RBT_Map
01:40:49 MDP-Algorithms: theory HOL-Library.Code_Real_Approx_By_Float
01:40:49 Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space
01:40:49 Perron_Frobenius: theory HOL-Analysis.Homeomorphism
01:40:49 MDP-Algorithms: theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
01:40:50 MDP-Algorithms: theory Jordan_Normal_Form.Conjugate
01:40:50 Timing Standard_Borel_Spaces (2 threads, 95.326s elapsed time, 134.022s cpu time, 5.995s GC time, factor 1.41)
01:40:50 Finished Standard_Borel_Spaces (0:01:38 elapsed time, 0:02:17 cpu time, factor 1.39)
01:40:50 Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type
01:40:50 Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint
01:40:51 Timing Quick_Sort_Cost (2 threads, 31.674s elapsed time, 49.224s cpu time, 2.981s GC time, factor 1.55)
01:40:51 Finished Quick_Sort_Cost (0:01:17 elapsed time, 0:01:40 cpu time, factor 1.29)
01:40:52 Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous
01:40:54 MDP-Algorithms: theory HOL-Library.Tree_Real
01:40:54 Linear_Programming: theory Farkas.Farkas
01:40:54 Linear_Programming: theory Simplex.Simplex_Incremental
01:40:55 MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
01:40:55 MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
01:40:57 Timing Linear_Recurrences (6 threads, 24.365s elapsed time, 76.124s cpu time, 6.526s GC time, factor 3.12)
01:40:57 Finished Linear_Recurrences (0:00:26 elapsed time, 0:01:18 cpu time, factor 2.98)
01:40:57 Timing Hermite (6 threads, 20.431s elapsed time, 61.472s cpu time, 5.486s GC time, factor 3.01)
01:40:57 Finished Hermite (0:00:33 elapsed time, 0:01:19 cpu time, factor 2.34)
01:40:57 Timing Actuarial_Mathematics (2 threads, 102.132s elapsed time, 172.718s cpu time, 7.877s GC time, factor 1.69)
01:40:57 Finished Actuarial_Mathematics (0:01:46 elapsed time, 0:02:56 cpu time, factor 1.67)
01:40:58 Linear_Programming: theory Farkas.Matrix_Farkas
01:40:59 MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
01:40:59 Building CryptHOL (on 10.195.8.46) ...
01:41:01 Linear_Programming: theory Farkas.Simplex_for_Reals
01:41:02 Timing QHLProver (6 threads, 30.663s elapsed time, 120.028s cpu time, 7.924s GC time, factor 3.91)
01:41:02 Finished QHLProver (0:00:32 elapsed time, 0:02:02 cpu time, factor 3.75)
01:41:02 MDP-Algorithms: theory MDP-Algorithms.MDP_fin
01:41:02 Linear_Programming: theory Linear_Programming.Matrix_LinPoly
01:41:03 CryptHOL: theory HOL-Eisbach.Eisbach
01:41:03 CryptHOL: theory Applicative_Lifting.Applicative
01:41:03 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
01:41:03 Linear_Programming: theory Linear_Programming.LP_Preliminaries
01:41:04 CryptHOL: theory CryptHOL.Partial_Function_Set
01:41:04 CryptHOL: theory HOL-Library.Case_Converter
01:41:04 MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
01:41:05 CryptHOL: theory Applicative_Lifting.Applicative_Environment
01:41:05 CryptHOL: theory Applicative_Lifting.Applicative_Set
01:41:05 CryptHOL: theory CryptHOL.Environment_Functor
01:41:05 CryptHOL: theory CryptHOL.Set_Applicative
01:41:05 CryptHOL: theory HOL-Library.Simps_Case_Conv
01:41:05 CryptHOL: theory HOL-Algebra.Congruence
01:41:05 CryptHOL: theory HOL-Library.Function_Algebras
01:41:05 CryptHOL: theory HOL-Library.Type_Length
01:41:05 MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
01:41:06 CryptHOL: theory HOL-Library.Countable_Set_Type
01:41:06 CryptHOL: theory HOL-Algebra.Order
01:41:08 CryptHOL: theory HOL-Algebra.Lattice
01:41:08 Linear_Programming: theory Linear_Programming.Linear_Programming
01:41:09 CryptHOL: theory Coinductive.Coinductive_Nat
01:41:09 CryptHOL: theory HOL-Algebra.Complete_Lattice
01:41:10 Building HOL-ODE-Numerics (on 10.195.8.42) ...
01:41:10 CryptHOL: theory Coinductive.Coinductive_List
01:41:11 Timing Pi_Transcendental (6 threads, 18.178s elapsed time, 61.707s cpu time, 5.090s GC time, factor 3.39)
01:41:11 Finished Pi_Transcendental (0:00:37 elapsed time, 0:01:27 cpu time, factor 2.33)
01:41:11 CryptHOL: theory HOL-Algebra.Group
01:41:12 Timing Subresultants (6 threads, 29.778s elapsed time, 83.481s cpu time, 5.469s GC time, factor 2.80)
01:41:12 Finished Subresultants (0:00:47 elapsed time, 0:01:51 cpu time, factor 2.35)
01:41:13 Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
01:41:13 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
01:41:13 Frequency_Moments: theory HOL-Number_Theory.Number_Theory
01:41:13 Timing DiscretePricing (2 threads, 120.208s elapsed time, 216.302s cpu time, 23.772s GC time, factor 1.80)
01:41:13 Finished DiscretePricing (0:02:04 elapsed time, 0:03:40 cpu time, factor 1.78)
01:41:14 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
01:41:14 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
01:41:14 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
01:41:14 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
01:41:14 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
01:41:14 CryptHOL: theory HOL-Algebra.Coset
01:41:14 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
01:41:15 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
01:41:15 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
01:41:15 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
01:41:15 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
01:41:15 HOL-ODE-Numerics: theory Deriving.Comparator
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
01:41:16 Running Groebner_Macaulay (on of4.proof.cit.tum.de) ...
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
01:41:16 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
01:41:16 HOL-ODE-Numerics: theory Deriving.Derive_Manager
01:41:16 HOL-ODE-Numerics: theory Deriving.Compare
01:41:16 HOL-ODE-Numerics: theory Deriving.Generator_Aux
01:41:17 Running Differential_Dynamic_Logic (on of4.proof.cit.tum.de) ...
01:41:17 Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
01:41:17 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
01:41:17 MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
01:41:17 HOL-ODE-Numerics: theory Deriving.Equality_Generator
01:41:17 CryptHOL: theory CryptHOL.Cyclic_Group
01:41:18 HOL-ODE-Numerics: theory Deriving.Compare_Generator
01:41:18 Frequency_Moments: theory Median_Method.Median
01:41:18 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
01:41:18 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
01:41:18 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
01:41:18 HOL-ODE-Numerics: theory Deriving.Equality_Instances
01:41:18 HOL-ODE-Numerics: theory HOL-Library.AList
01:41:18 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
01:41:18 Groebner_Macaulay: theory Groebner_Macaulay.Binomial_Int
01:41:18 Groebner_Macaulay: theory Groebner_Macaulay.Dube_Prelims
01:41:18 Groebner_Macaulay: theory Groebner_Macaulay.Monomial_Module
01:41:18 Groebner_Macaulay: theory Groebner_Macaulay.Degree_Bound_Utils
01:41:18 Groebner_Macaulay: theory Groebner_Macaulay.Degree_Section
01:41:18 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
01:41:18 Estimated 0:53:56 build time with path time heuristic (critical: relative time (0.5), parallel: time based threads) (took 0.466s)
01:41:19 HOL-ODE-Numerics: theory HOL-ex.Quicksort
01:41:19 Groebner_Macaulay: theory Groebner_Macaulay.Hilbert_Function
01:41:19 Groebner_Macaulay: theory Groebner_Macaulay.Poly_Fun
01:41:19 CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
01:41:19 HOL-ODE-Numerics: theory HOL-Library.Char_ord
01:41:19 HOL-ODE-Numerics: theory Deriving.Compare_Instances
01:41:19 Running Nullstellensatz (on of1-proof+8-15) ...
01:41:19 Running Signature_Groebner (on of1-proof+0-7) ...
01:41:20 Frequency_Moments: theory Lp.Functional_Spaces
01:41:20 CryptHOL: theory Coinductive.TLList
01:41:20 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
01:41:20 HOL-ODE-Numerics: theory HOL-Library.Mapping
01:41:20 HOL-ODE-Numerics: theory HOL-Library.Option_ord
01:41:21 Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay
01:41:21 Groebner_Macaulay: theory Groebner_Macaulay.Cone_Decomposition
01:41:21 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
01:41:21 Signature_Groebner: theory Signature_Groebner.Prelims
01:41:21 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
01:41:21 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
01:41:21 Nullstellensatz: theory Nullstellensatz.Univariate_PM
01:41:21 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
01:41:21 Signature_Groebner: theory Signature_Groebner.More_MPoly
01:41:21 CryptHOL: theory Applicative_Lifting.Applicative_PMF
01:41:21 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
01:41:22 Timing Turans_Graph_Theorem (2 threads, 141.016s elapsed time, 256.610s cpu time, 25.991s GC time, factor 1.82)
01:41:22 Finished Turans_Graph_Theorem (0:02:25 elapsed time, 0:04:21 cpu time, factor 1.80)
01:41:22 Signature_Groebner: theory Signature_Groebner.Signature_Groebner
01:41:22 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
01:41:23 HOL-ODE-Numerics: theory HOL-Library.Parallel
01:41:23 CryptHOL: theory Monad_Normalisation.Monad_Normalisation
01:41:23 Frequency_Moments: theory Lp.Lp
01:41:23 CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
01:41:24 CryptHOL: theory CryptHOL.SPMF_Applicative
01:41:24 Timing MFMC_Countable (2 threads, 139.087s elapsed time, 220.794s cpu time, 10.219s GC time, factor 1.59)
01:41:24 Finished MFMC_Countable (0:02:23 elapsed time, 0:03:45 cpu time, factor 1.57)
01:41:24 Running Stern_Brocot (on 10.195.8.29) ...
01:41:24 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
01:41:24 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
01:41:24 Timing Nullstellensatz (8 threads, 2.983s elapsed time, 8.951s cpu time, 0.883s GC time, factor 3.00)
01:41:24 Finished Nullstellensatz (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.24)
01:41:25 Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
01:41:25 HOL-ODE-Numerics: theory HOL-Library.Type_Length
01:41:25 CryptHOL: theory Landau_Symbols.Group_Sort
01:41:25 MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
01:41:25 Frequency_Moments: theory Lehmer.Lehmer
01:41:25 Timing Isabelle_Marries_Dirac (6 threads, 53.292s elapsed time, 241.575s cpu time, 12.103s GC time, factor 4.53)
01:41:25 Finished Isabelle_Marries_Dirac (0:00:55 elapsed time, 0:04:04 cpu time, factor 4.42)
01:41:25 Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
01:41:26 HOL-ODE-Numerics: theory HOL-Library.Word
01:41:26 Groebner_Macaulay: theory Groebner_Macaulay.Dube_Bound
01:41:27 MDP-Algorithms: theory Containers.RBT_ext
01:41:27 CryptHOL: theory Landau_Symbols.Landau_Real_Products
01:41:27 Stern_Brocot: theory Stern_Brocot.Cotree
01:41:27 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
01:41:27 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
01:41:28 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
01:41:28 Timing Density_Compiler (2 threads, 138.885s elapsed time, 269.500s cpu time, 9.646s GC time, factor 1.94)
01:41:28 Finished Density_Compiler (0:02:23 elapsed time, 0:04:34 cpu time, factor 1.92)
01:41:29 MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
01:41:29 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
01:41:29 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
01:41:29 MDP-Algorithms: theory MDP-Algorithms.Code_Setup
01:41:30 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
01:41:30 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
01:41:30 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
01:41:30 Frequency_Moments: theory Bertrands_Postulate.Bertrand
01:41:30 Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay_Examples
01:41:31 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
01:41:31 CryptHOL: theory Landau_Symbols.Landau_Simprocs
01:41:32 CryptHOL: theory Landau_Symbols.Landau_More
01:41:32 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
01:41:32 CryptHOL: theory CryptHOL.Negligible
01:41:32 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
01:41:32 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
01:41:33 Timing Linear_Programming (6 threads, 61.477s elapsed time, 208.465s cpu time, 13.844s GC time, factor 3.39)
01:41:33 Finished Linear_Programming (0:01:03 elapsed time, 0:03:31 cpu time, factor 3.33)
01:41:34 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
01:41:34 Signature_Groebner: theory Signature_Groebner.Signature_Examples
01:41:35 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
01:41:35 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
01:41:36 Building Random_BSTs (on 10.195.7.194) ...
01:41:36 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
01:41:36 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
01:41:37 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
01:41:37 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
01:41:37 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
01:41:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
01:41:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
01:41:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
01:41:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
01:41:39 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
01:41:39 Timing SDS_Impossibility (2 threads, 58.912s elapsed time, 77.998s cpu time, 3.928s GC time, factor 1.32)
01:41:39 Finished SDS_Impossibility (0:01:02 elapsed time, 0:01:22 cpu time, factor 1.31)
01:41:39 Random_BSTs: theory HOL-Data_Structures.Cmp
01:41:39 Random_BSTs: theory HOL-Data_Structures.Less_False
01:41:39 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
01:41:39 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
01:41:40 Random_BSTs: theory HOL-Data_Structures.Set_Specs
01:41:40 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
01:41:40 HOL-ODE-Numerics: theory Collections.SetIterator
01:41:40 Random_BSTs: theory HOL-Data_Structures.Tree_Set
01:41:42 Random_BSTs: theory Random_BSTs.Random_BSTs
01:41:42 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
01:41:43 Timing Girth_Chromatic (2 threads, 121.583s elapsed time, 205.372s cpu time, 19.333s GC time, factor 1.69)
01:41:43 Finished Girth_Chromatic (0:02:41 elapsed time, 0:04:16 cpu time, factor 1.59)
01:41:45 Timing Three_Squares (6 threads, 181.624s elapsed time, 740.876s cpu time, 183.228s GC time, factor 4.08)
01:41:45 Finished Three_Squares (0:03:32 elapsed time, 0:13:21 cpu time, factor 3.76)
01:41:45 HOL-ODE-Numerics: theory Collections.Assoc_List
01:41:45 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
01:41:45 HOL-ODE-Numerics: theory Collections.Intf_Comp
01:41:46 HOL-ODE-Numerics: theory Collections.Idx_Iterator
01:41:46 HOL-ODE-Numerics: theory Collections.Diff_Array
01:41:47 CryptHOL: theory CryptHOL.Misc_CryptHOL
01:41:48 HOL-ODE-Numerics: theory Collections.Proper_Iterator
01:41:48 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
01:41:49 HOL-ODE-Numerics: theory Collections.It_to_It
01:41:49 HOL-ODE-Numerics: theory Collections.SetIteratorGA
01:41:49 Building Smith_Normal_Form (on 10.195.8.46) ...
01:41:50 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
01:41:50 Markov_Models: theory Markov_Models.MDP_RP
01:41:52 HOL-ODE-Numerics: theory Word_Lib.More_Divides
01:41:52 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
01:41:53 Building Berlekamp_Zassenhaus (on 10.195.8.46) ...
01:41:54 Timing Signature_Groebner (8 threads, 32.198s elapsed time, 72.879s cpu time, 13.116s GC time, factor 2.26)
01:41:54 Finished Signature_Groebner (0:00:34 elapsed time, 0:01:16 cpu time, factor 2.23)
01:41:55 Running Hermite_Lindemann (on 10.195.8.46) ...
01:41:55 Timing Ergodic_Theory (2 threads, 137.057s elapsed time, 231.660s cpu time, 8.380s GC time, factor 1.69)
01:41:55 Finished Ergodic_Theory (0:02:51 elapsed time, 0:04:35 cpu time, factor 1.60)
01:41:57 Smith_Normal_Form: theory HOL-Eisbach.Eisbach
01:41:57 Smith_Normal_Form: theory Deriving.Derive_Manager
01:41:58 Smith_Normal_Form: theory Deriving.Generator_Aux
01:41:58 CryptHOL: theory CryptHOL.Generat
01:41:58 CryptHOL: theory CryptHOL.List_Bits
01:41:58 CryptHOL: theory CryptHOL.Resumption
01:41:58 Smith_Normal_Form: theory HOL-Number_Theory.Cong
01:41:58 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
01:41:58 Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
01:41:58 Smith_Normal_Form: theory HOL-Algebra.Congruence
01:41:58 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
01:41:58 Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials
01:41:58 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
01:41:59 Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize
01:41:59 Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval
01:41:59 Perron_Frobenius: theory Perron_Frobenius.Roots_Unity
01:41:59 Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan
01:41:59 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
01:41:59 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion
01:41:59 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
01:41:59 Smith_Normal_Form: theory HOL-Algebra.Order
01:41:59 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
01:42:00 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
01:42:00 Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
01:42:00 Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
01:42:00 Hermite_Lindemann: theory HOL-Library.Adhoc_Overloading
01:42:00 Hermite_Lindemann: theory HOL-Combinatorics.List_Permutation
01:42:00 Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
01:42:00 Hermite_Lindemann: theory HOL-Library.Monad_Syntax
01:42:00 Hermite_Lindemann: theory HOL-Algebra.Divisibility
01:42:00 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
01:42:00 Hermite_Lindemann: theory Containers.Containers_Auxiliary
01:42:00 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
01:42:01 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
01:42:01 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
01:42:01 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Misc
01:42:01 Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
01:42:01 Hermite_Lindemann: theory Jordan_Normal_Form.Missing_Ring
01:42:01 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible
01:42:01 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
01:42:02 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
01:42:02 Smith_Normal_Form: theory HOL-Algebra.Lattice
01:42:02 CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
01:42:02 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General
01:42:02 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
01:42:02 Running Random_Graph_Subgraph_Threshold (on of3.proof.cit.tum.de) ...
01:42:02 Running Szemeredi_Regularity (on of3.proof.cit.tum.de) ...
01:42:03 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
01:42:03 Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
01:42:03 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
01:42:04 Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
01:42:04 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
01:42:04 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
01:42:04 Running Laws_of_Large_Numbers (on of2.proof.cit.tum.de) ...
01:42:04 HOL-ODE-Numerics: theory Deriving.Countable_Generator
01:42:04 Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:42:04 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
01:42:04 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
01:42:04 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
01:42:05 Timing Projective_Measurements (6 threads, 167.933s elapsed time, 616.238s cpu time, 126.199s GC time, factor 3.67)
01:42:05 Finished Projective_Measurements (0:03:16 elapsed time, 0:11:11 cpu time, factor 3.42)
01:42:05 Smith_Normal_Form: theory HOL-Algebra.Group
01:42:05 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
01:42:05 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
01:42:05 Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
01:42:05 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
01:42:05 Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
01:42:05 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
01:42:05 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Unsorted
01:42:05 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
01:42:05 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
01:42:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
01:42:06 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
01:42:06 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
01:42:06 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
01:42:06 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
01:42:06 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
01:42:06 Timing Szemeredi_Regularity (6 threads, 1.869s elapsed time, 6.654s cpu time, 0.238s GC time, factor 3.56)
01:42:06 Finished Szemeredi_Regularity (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.22)
01:42:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
01:42:07 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
01:42:07 Timing Laws_of_Large_Numbers (6 threads, 0.452s elapsed time, 1.211s cpu time, 0.051s GC time, factor 2.68)
01:42:07 Finished Laws_of_Large_Numbers (0:00:02 elapsed time)
01:42:07 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
01:42:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
01:42:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
01:42:07 Stern_Brocot: theory Stern_Brocot.Bird_Tree
01:42:07 Hermite_Lindemann: theory HOL-Computational_Algebra.Field_as_Ring
01:42:07 Timing Random_Graph_Subgraph_Threshold (6 threads, 3.099s elapsed time, 9.439s cpu time, 0.355s GC time, factor 3.05)
01:42:08 Finished Random_Graph_Subgraph_Threshold (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.22)
01:42:08 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
01:42:08 Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
01:42:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
01:42:08 Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:42:08 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
01:42:08 Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
01:42:08 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
01:42:08 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
01:42:08 Hermite_Lindemann: theory Polynomial_Interpolation.Missing_Polynomial
01:42:08 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
01:42:09 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
01:42:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
01:42:09 Smith_Normal_Form: theory HOL-Algebra.Coset
01:42:10 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
01:42:10 Hermite_Lindemann: theory Jordan_Normal_Form.Conjugate
01:42:10 Timing Stern_Brocot (2 threads, 41.088s elapsed time, 69.396s cpu time, 9.198s GC time, factor 1.69)
01:42:10 Finished Stern_Brocot (0:00:45 elapsed time, 0:01:14 cpu time, factor 1.64)
01:42:10 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Polynomial_Factorial
01:42:10 Hermite_Lindemann: theory Polynomial_Factorization.Order_Polynomial
01:42:10 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
01:42:10 Hermite_Lindemann: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:42:11 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
01:42:11 Hermite_Lindemann: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:42:12 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
01:42:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
01:42:12 Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
01:42:12 Hermite_Lindemann: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:42:12 Hermite_Lindemann: theory Polynomial_Factorization.Polynomial_Irreducibility
01:42:13 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
01:42:13 Hermite_Lindemann: theory Hermite_Lindemann.Complex_Lexorder
01:42:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
01:42:13 Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
01:42:13 Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp
01:42:13 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block
01:42:14 Hermite_Lindemann: theory Hermite_Lindemann.Misc_HLW
01:42:14 Smith_Normal_Form: theory HOL-Algebra.Ring
01:42:14 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
01:42:15 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2
01:42:15 Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
01:42:15 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth
01:42:15 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
01:42:15 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
01:42:15 Hermite_Lindemann: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
01:42:16 Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
01:42:16 Hermite_Lindemann: theory Polynomial_Interpolation.Is_Rat_To_Rat
01:42:17 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
01:42:17 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
01:42:17 Hermite_Lindemann: theory Matrix.Utility
01:42:17 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
01:42:17 Hermite_Lindemann: theory Polynomial_Factorization.Missing_List
01:42:18 Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
01:42:19 Smith_Normal_Form: theory HOL-Number_Theory.Totient
01:42:19 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
01:42:19 Timing Random_BSTs (2 threads, 10.364s elapsed time, 16.448s cpu time, 1.528s GC time, factor 1.59)
01:42:19 Finished Random_BSTs (0:00:42 elapsed time, 0:00:55 cpu time, factor 1.29)
01:42:19 Hermite_Lindemann: theory Polynomial_Interpolation.Divmod_Int
01:42:19 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom
01:42:19 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
01:42:19 Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
01:42:20 Timing Perron_Frobenius (6 threads, 111.165s elapsed time, 500.957s cpu time, 56.369s GC time, factor 4.51)
01:42:20 Finished Perron_Frobenius (0:01:53 elapsed time, 0:08:26 cpu time, factor 4.45)
01:42:20 Berlekamp_Zassenhaus: theory Matrix.Utility
01:42:21 Smith_Normal_Form: theory HOL-Algebra.AbelCoset
01:42:21 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
01:42:22 Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
01:42:22 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
01:42:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
01:42:22 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
01:42:23 Hermite_Lindemann: theory Polynomial_Factorization.Missing_Multiset
01:42:23 Smith_Normal_Form: theory HOL-Algebra.Module
01:42:23 Hermite_Lindemann: theory Berlekamp_Zassenhaus.More_Missing_Multiset
01:42:24 CryptHOL: theory CryptHOL.Computational_Model
01:42:24 CryptHOL: theory CryptHOL.GPV_Applicative
01:42:24 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
01:42:24 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
01:42:24 Building Commuting_Hermitian (on of3.proof.cit.tum.de) ...
01:42:25 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
01:42:25 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
01:42:26 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
01:42:26 Hermite_Lindemann: theory Jordan_Normal_Form.Matrix
01:42:26 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
01:42:26 Running Polygonal_Number_Theorem (on of3.proof.cit.tum.de) ...
01:42:27 CryptHOL: theory CryptHOL.GPV_Expectation
01:42:27 Hermite_Lindemann: theory Polynomial_Interpolation.Ring_Hom_Poly
01:42:27 Smith_Normal_Form: theory HOL-Algebra.Ideal
01:42:27 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
01:42:28 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
01:42:28 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
01:42:28 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
01:42:28 CryptHOL: theory CryptHOL.GPV_Bisim
01:42:28 Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
01:42:28 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
01:42:28 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
01:42:28 Timing Bernoulli (2 threads, 205.283s elapsed time, 356.093s cpu time, 58.934s GC time, factor 1.73)
01:42:28 Finished Bernoulli (0:04:13 elapsed time, 0:06:45 cpu time, factor 1.60)
01:42:28 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
01:42:29 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
01:42:29 CryptHOL: theory CryptHOL.CryptHOL
01:42:30 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
01:42:30 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization
01:42:30 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
01:42:30 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
01:42:31 Smith_Normal_Form: theory HOL-Algebra.RingHom
01:42:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
01:42:33 Hermite_Lindemann: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:42:33 Smith_Normal_Form: theory HOL-Algebra.UnivPoly
01:42:33 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
01:42:34 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
01:42:34 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
01:42:34 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
01:42:34 Timing Hybrid_Systems_VCs (2 threads, 526.504s elapsed time, 817.807s cpu time, 47.383s GC time, factor 1.55)
01:42:34 Finished Hybrid_Systems_VCs (0:08:51 elapsed time, 0:13:45 cpu time, factor 1.55)
01:42:36 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
01:42:36 Smith_Normal_Form: theory List-Index.List_Index
01:42:36 Hermite_Lindemann: theory Jordan_Normal_Form.Column_Operations
01:42:36 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
01:42:37 Hermite_Lindemann: theory Jordan_Normal_Form.Determinant
01:42:37 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
01:42:37 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
01:42:37 MDP-Algorithms: theory Containers.RBT_Mapping2
01:42:39 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
01:42:40 MDP-Algorithms: theory Containers.RBT_Set2
01:42:40 MDP-Algorithms: theory MDP-Algorithms.Fin_Code
01:42:40 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
01:42:40 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
01:42:40 Hermite_Lindemann: theory Polynomial_Factorization.Gauss_Lemma
01:42:40 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
01:42:41 Hermite_Lindemann: theory Polynomial_Factorization.Square_Free_Factorization
01:42:42 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
01:42:42 MDP-Algorithms: theory Containers.Set_Impl
01:42:42 Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
01:42:43 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
01:42:44 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
01:42:44 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
01:42:44 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
01:42:44 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
01:42:44 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
01:42:44 Hermite_Lindemann: theory Polynomial_Interpolation.Newton_Interpolation
01:42:44 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
01:42:44 Timing Polygonal_Number_Theorem (6 threads, 15.215s elapsed time, 69.908s cpu time, 3.622s GC time, factor 4.59)
01:42:44 Finished Polygonal_Number_Theorem (0:00:17 elapsed time, 0:01:11 cpu time, factor 4.21)
01:42:45 Hermite_Lindemann: theory Subresultants.More_Homomorphisms
01:42:45 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
01:42:46 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
01:42:47 Hermite_Lindemann: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
01:42:47 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
01:42:47 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
01:42:47 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
01:42:47 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
01:42:48 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
01:42:48 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
01:42:49 Hermite_Lindemann: theory Subresultants.Resultant_Prelim
01:42:49 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
01:42:49 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
01:42:49 Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:42:50 Berlekamp_Zassenhaus: theory Show.Show_Poly
01:42:50 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:42:50 Hermite_Lindemann: theory Algebraic_Numbers.Bivariate_Polynomials
01:42:50 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
01:42:50 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
01:42:50 Running Randomised_BSTs (on 10.195.8.40) ...
01:42:51 Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
01:42:51 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
01:42:52 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
01:42:52 Timing Commuting_Hermitian (6 threads, 9.039s elapsed time, 44.059s cpu time, 2.596s GC time, factor 4.87)
01:42:52 Finished Commuting_Hermitian (0:00:24 elapsed time, 0:01:09 cpu time, factor 2.85)
01:42:52 Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
01:42:52 MDP-Algorithms: theory MDP-Algorithms.GS_Code
01:42:52 Hermite_Lindemann: theory Algebraic_Numbers.Resultant
01:42:53 Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
01:42:53 Hermite_Lindemann: theory Algebraic_Numbers.Min_Int_Poly
01:42:53 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
01:42:54 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
01:42:54 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
01:42:55 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
01:42:55 Hermite_Lindemann: theory Algebraic_Numbers.Algebraic_Numbers
01:42:56 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
01:42:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
01:42:56 Smith_Normal_Form: theory HOL-Number_Theory.Residues
01:42:56 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
01:42:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
01:42:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
01:42:57 Timing Markov_Models (2 threads, 201.571s elapsed time, 321.011s cpu time, 22.931s GC time, factor 1.59)
01:42:57 Finished Markov_Models (0:04:13 elapsed time, 0:06:19 cpu time, factor 1.50)
01:42:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
01:42:58 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
01:42:58 Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
01:42:58 Frequency_Moments: theory Frequency_Moments.K_Smallest
01:42:58 Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
01:42:58 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
01:42:58 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
01:42:58 Hermite_Lindemann: theory Hermite_Lindemann.Algebraic_Integer_Divisibility
01:42:59 Hermite_Lindemann: theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
01:42:59 Frequency_Moments: theory Frequency_Moments.Probability_Ext
01:42:59 Hermite_Lindemann: theory Hermite_Lindemann.More_Polynomial_HLW
01:42:59 Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
01:42:59 Berlekamp_Zassenhaus: theory Word_Lib.More_Word
01:42:59 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
01:43:00 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
01:43:00 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
01:43:01 Hermite_Lindemann: theory Hermite_Lindemann.More_Min_Int_Poly
01:43:01 Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
01:43:01 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
01:43:01 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
01:43:01 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
01:43:02 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
01:43:02 Hermite_Lindemann: theory Hermite_Lindemann.Hermite_Lindemann
01:43:02 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
01:43:02 Smith_Normal_Form: theory Show.Show
01:43:02 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
01:43:02 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
01:43:02 Running Lambert_W (on of3.proof.cit.tum.de) ...
01:43:02 Running Euler_MacLaurin (on of3.proof.cit.tum.de) ...
01:43:02 Building Stirling_Formula (on of3.proof.cit.tum.de) ...
01:43:03 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
01:43:04 Lambert_W: theory HOL-Library.Function_Algebras
01:43:04 Lambert_W: theory Landau_Symbols.Group_Sort
01:43:04 Lambert_W: theory Lambert_W.Lambert_W
01:43:04 Euler_MacLaurin: theory HOL-Library.Function_Algebras
01:43:04 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
01:43:04 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
01:43:04 Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
01:43:04 Stirling_Formula: theory HOL-Library.Function_Algebras
01:43:04 Stirling_Formula: theory Landau_Symbols.Group_Sort
01:43:05 Lambert_W: theory Landau_Symbols.Landau_Real_Products
01:43:05 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
01:43:05 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
01:43:05 Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
01:43:05 Smith_Normal_Form: theory Show.Show_Instances
01:43:05 Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
01:43:06 Timing Groebner_Macaulay (6 threads, 106.023s elapsed time, 221.751s cpu time, 117.171s GC time, factor 2.09)
01:43:06 Finished Groebner_Macaulay (0:01:48 elapsed time, 0:03:45 cpu time, factor 2.08)
01:43:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
01:43:07 Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
01:43:07 Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
01:43:07 Smith_Normal_Form: theory Show.Show_Poly
01:43:07 Lambert_W: theory Landau_Symbols.Landau_Simprocs
01:43:07 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
01:43:07 Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
01:43:08 Lambert_W: theory Landau_Symbols.Landau_More
01:43:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
01:43:08 Euler_MacLaurin: theory Landau_Symbols.Landau_More
01:43:08 Lambert_W: theory Stirling_Formula.Stirling_Formula
01:43:08 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
01:43:08 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
01:43:08 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
01:43:08 Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
01:43:08 Stirling_Formula: theory Landau_Symbols.Landau_More
01:43:08 Stirling_Formula: theory Stirling_Formula.Stirling_Formula
01:43:08 Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
01:43:08 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
01:43:08 Lambert_W: theory Lambert_W.Lambert_W_MacLaurin_Series
01:43:09 HOL-ODE-Numerics: theory HOL-Library.RBT
01:43:09 Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
01:43:09 Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
01:43:09 HOL-ODE-Numerics: theory Collections.Gen_Iterator
01:43:09 Timing Euler_MacLaurin (6 threads, 5.119s elapsed time, 22.221s cpu time, 1.500s GC time, factor 4.34)
01:43:09 Finished Euler_MacLaurin (0:00:06 elapsed time, 0:00:23 cpu time, factor 3.60)
01:43:10 Timing Differential_Dynamic_Logic (6 threads, 110.019s elapsed time, 278.401s cpu time, 69.112s GC time, factor 2.53)
01:43:10 Finished Differential_Dynamic_Logic (0:01:51 elapsed time, 0:04:41 cpu time, factor 2.52)
01:43:10 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
01:43:10 Timing Randomised_BSTs (2 threads, 15.722s elapsed time, 29.576s cpu time, 1.909s GC time, factor 1.88)
01:43:10 Finished Randomised_BSTs (0:00:19 elapsed time, 0:00:32 cpu time, factor 1.71)
01:43:10 HOL-ODE-Numerics: theory Collections.Intf_Map
01:43:10 MDP-Algorithms: theory MDP-Algorithms.MPI_Code
01:43:11 HOL-ODE-Numerics: theory Collections.Iterator
01:43:11 HOL-ODE-Numerics: theory Collections.Intf_Set
01:43:11 Timing Lambert_W (6 threads, 6.723s elapsed time, 25.073s cpu time, 2.216s GC time, factor 3.73)
01:43:11 Finished Lambert_W (0:00:08 elapsed time, 0:00:26 cpu time, factor 3.17)
01:43:11 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
01:43:11 HOL-ODE-Numerics: theory Collections.Array_Iterator
01:43:11 MDP-Algorithms: theory MDP-Algorithms.VI_Code
01:43:12 HOL-ODE-Numerics: theory Collections.RBT_add
01:43:12 HOL-ODE-Numerics: theory Collections.Gen_Map
01:43:13 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
01:43:13 Smith_Normal_Form: theory VectorSpace.FunctionLemmas
01:43:13 Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
01:43:13 Smith_Normal_Form: theory VectorSpace.RingModuleFacts
01:43:14 HOL-ODE-Numerics: theory Collections.Impl_List_Map
01:43:14 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
01:43:14 Smith_Normal_Form: theory VectorSpace.MonoidSums
01:43:15 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
01:43:15 Smith_Normal_Form: theory VectorSpace.LinearCombinations
01:43:16 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
01:43:17 HOL-ODE-Numerics: theory Collections.Gen_Set
01:43:20 HOL-ODE-Numerics: theory Collections.Impl_List_Set
01:43:25 Timing Stirling_Formula (6 threads, 8.137s elapsed time, 25.119s cpu time, 1.549s GC time, factor 3.09)
01:43:25 Finished Stirling_Formula (0:00:22 elapsed time, 0:00:50 cpu time, factor 2.23)
01:43:27 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
01:43:27 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
01:43:27 Running Probabilistic_Timed_Automata (on 10.195.8.40) ...
01:43:27 Running Stochastic_Matrices (on 10.195.8.40) ...
01:43:27 Berlekamp_Zassenhaus: theory Native_Word.Uint32
01:43:29 Smith_Normal_Form: theory VectorSpace.SumSpaces
01:43:29 Running TsirelsonBound (on 10.195.8.40) ...
01:43:30 Smith_Normal_Form: theory VectorSpace.VectorSpace
01:43:30 Berlekamp_Zassenhaus: theory Native_Word.Uint64
01:43:30 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
01:43:30 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach
01:43:30 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
01:43:31 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
01:43:31 Probabilistic_Timed_Automata: theory Timed_Automata.Misc
01:43:32 Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
01:43:32 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
01:43:32 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
01:43:32 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
01:43:32 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
01:43:32 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
01:43:33 Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
01:43:33 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
01:43:33 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
01:43:33 Running Hidden_Markov_Models (on 10.195.8.11) ...
01:43:33 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
01:43:33 Stochastic_Matrices: theory HOL-Eisbach.Eisbach
01:43:33 Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
01:43:33 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
01:43:34 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
01:43:34 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
01:43:34 Stochastic_Matrices: theory HOL-Algebra.Congruence
01:43:35 Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
01:43:35 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
01:43:35 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
01:43:35 Stochastic_Matrices: theory HOL-Algebra.Order
01:43:35 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
01:43:36 Stochastic_Matrices: theory HOL-Library.Function_Algebras
01:43:36 Stochastic_Matrices: theory HOL-Library.More_List
01:43:36 Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
01:43:36 Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
01:43:36 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
01:43:38 TsirelsonBound: theory TsirelsonBound.Tsirelson
01:43:38 MDP-Algorithms: theory Show.Show
01:43:38 Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
01:43:38 Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
01:43:39 Hidden_Markov_Models: theory HOL-Library.State_Monad
01:43:39 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
01:43:39 Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
01:43:39 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
01:43:39 Stochastic_Matrices: theory HOL-Algebra.Lattice
01:43:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
01:43:39 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
01:43:40 MDP-Algorithms: theory Show.Show_Instances
01:43:40 Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
01:43:40 Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
01:43:40 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
01:43:41 Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
01:43:41 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
01:43:42 MDP-Algorithms: theory VectorSpace.FunctionLemmas
01:43:42 MDP-Algorithms: theory VectorSpace.RingModuleFacts
01:43:42 MDP-Algorithms: theory Jordan_Normal_Form.Matrix
01:43:42 Stochastic_Matrices: theory HOL-Algebra.Group
01:43:43 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
01:43:43 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
01:43:43 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
01:43:44 Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
01:43:44 Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
01:43:44 Probabilistic_Timed_Automata: theory Timed_Automata.DBM
01:43:44 Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
01:43:45 Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
01:43:45 Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
01:43:45 Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
01:43:45 Stochastic_Matrices: theory HOL-Algebra.Coset
01:43:46 Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
01:43:46 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
01:43:47 MDP-Algorithms: theory VectorSpace.MonoidSums
01:43:47 Timing CAVA_Setup (2 threads, 1266.455s elapsed time, 2211.896s cpu time, 601.038s GC time, factor 1.75)
01:43:47 Finished CAVA_Setup (0:22:41 elapsed time, 0:39:09 cpu time, factor 1.73)
01:43:47 Hidden_Markov_Models: theory Monad_Memo_DP.Memory
01:43:47 MDP-Algorithms: theory VectorSpace.LinearCombinations
01:43:47 Probabilistic_Timed_Automata: theory Timed_Automata.Regions
01:43:48 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
01:43:48 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
01:43:49 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
01:43:49 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
01:43:49 Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
01:43:49 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
01:43:49 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:43:50 Stochastic_Matrices: theory HOL-Algebra.Ring
01:43:50 Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
01:43:50 Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
01:43:51 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
01:43:51 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
01:43:51 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
01:43:51 Probabilistic_Timed_Automata: theory Timed_Automata.Closure
01:43:52 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
01:43:52 Running Clique_and_Monotone_Circuits (on 10.195.8.11) ...
01:43:52 Running Comparison_Sort_Lower_Bound (on 10.195.8.11) ...
01:43:52 Running Irrationals_From_THEBOOK (on 10.195.8.11) ...
01:43:52 MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
01:43:53 MDP-Algorithms: theory Jordan_Normal_Form.Determinant
01:43:54 Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:43:54 Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
01:43:55 Stochastic_Matrices: theory HOL-Algebra.Module
01:43:55 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
01:43:55 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
01:43:55 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
01:43:55 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
01:43:55 Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
01:43:55 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
01:43:55 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
01:43:55 Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
01:43:55 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
01:43:56 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
01:43:56 MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
01:43:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
01:43:57 Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
01:43:57 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
01:43:57 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
01:43:58 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
01:43:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
01:43:58 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
01:43:58 Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
01:43:59 Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
01:43:59 Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
01:43:59 Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:44:00 Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
01:44:00 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
01:44:00 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
01:44:00 Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
01:44:00 Timing Irrationals_From_THEBOOK (2 threads, 4.206s elapsed time, 6.452s cpu time, 0.164s GC time, factor 1.53)
01:44:00 Finished Irrationals_From_THEBOOK (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.27)
01:44:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
01:44:02 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
01:44:02 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
01:44:02 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
01:44:03 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
01:44:04 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
01:44:04 MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
01:44:04 Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
01:44:04 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
01:44:05 Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
01:44:05 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
01:44:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
01:44:06 MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
01:44:06 Timing Comparison_Sort_Lower_Bound (2 threads, 9.973s elapsed time, 18.907s cpu time, 1.578s GC time, factor 1.90)
01:44:06 Finished Comparison_Sort_Lower_Bound (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.65)
01:44:06 MDP-Algorithms: theory VectorSpace.SumSpaces
01:44:07 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
01:44:07 MDP-Algorithms: theory VectorSpace.VectorSpace
01:44:08 Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
01:44:11 Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
01:44:12 Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
01:44:13 Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:44:14 Stochastic_Matrices: theory VectorSpace.FunctionLemmas
01:44:14 Stochastic_Matrices: theory VectorSpace.RingModuleFacts
01:44:15 Running CAVA_LTL_Modelchecker (on 10.195.8.49) ...
01:44:15 Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
01:44:15 MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
01:44:15 Stochastic_Matrices: theory VectorSpace.MonoidSums
01:44:16 Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
01:44:16 Stochastic_Matrices: theory VectorSpace.LinearCombinations
01:44:18 Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
01:44:19 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
01:44:20 Timing Hidden_Markov_Models (2 threads, 43.114s elapsed time, 82.508s cpu time, 8.013s GC time, factor 1.91)
01:44:20 Finished Hidden_Markov_Models (0:00:47 elapsed time, 0:01:26 cpu time, factor 1.84)
01:44:24 Stochastic_Matrices: theory VectorSpace.SumSpaces
01:44:24 HOL-ODE-Numerics: theory Show.Show
01:44:24 Stochastic_Matrices: theory VectorSpace.VectorSpace
01:44:25 MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
01:44:26 HOL-ODE-Numerics: theory Show.Show_Instances
01:44:28 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
01:44:28 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
01:44:29 HOL-ODE-Numerics: theory Word_Lib.More_Word
01:44:31 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
01:44:31 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
01:44:32 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
01:44:32 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
01:44:32 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
01:44:33 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
01:44:33 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
01:44:34 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
01:44:34 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
01:44:35 Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
01:44:37 MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
01:44:38 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
01:44:38 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
01:44:38 MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
01:44:40 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
01:44:40 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
01:44:40 Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
01:44:42 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:44:42 Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
01:44:46 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:44:46 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
01:44:47 Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
01:44:47 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
01:44:48 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
01:44:49 Timing Dirichlet_Series (2 threads, 341.189s elapsed time, 607.463s cpu time, 142.209s GC time, factor 1.78)
01:44:49 Finished Dirichlet_Series (0:06:26 elapsed time, 0:11:07 cpu time, factor 1.73)
01:44:49 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
01:44:49 MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
01:44:49 MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
01:44:49 Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
01:44:50 Running Gauss_Sums (on of1-proof+8-15) ...
01:44:50 Building Zeta_Function (on of1-proof+0-7) ...
01:44:51 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
01:44:51 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
01:44:51 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
01:44:51 HOL-ODE-Numerics: theory Native_Word.Uint
01:44:51 HOL-ODE-Numerics: theory Native_Word.Uint32
01:44:51 Zeta_Function: theory Bernoulli.Bernoulli_Zeta
01:44:51 Gauss_Sums: theory Polynomial_Interpolation.Missing_Unsorted
01:44:51 Gauss_Sums: theory HOL-Algebra.QuotRing
01:44:51 Gauss_Sums: theory Gauss_Sums.Periodic_Arithmetic
01:44:51 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
01:44:52 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Hom
01:44:52 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
01:44:52 Gauss_Sums: theory Gauss_Sums.Complex_Roots_Of_Unity
01:44:52 Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
01:44:52 Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
01:44:52 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
01:44:53 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
01:44:53 Gauss_Sums: theory Polynomial_Interpolation.Missing_Polynomial
01:44:53 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:44:53 HOL-ODE-Numerics: theory Collections.HashCode
01:44:53 Zeta_Function: theory Pure-ex.Guess
01:44:53 Zeta_Function: theory HOL-Eisbach.Eisbach
01:44:53 Zeta_Function: theory Sturm_Tarski.PolyMisc
01:44:53 Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring
01:44:53 Zeta_Function: theory Winding_Number_Eval.Missing_Topology
01:44:53 Zeta_Function: theory Zeta_Function.Zeta_Library
01:44:53 Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
01:44:54 Gauss_Sums: theory HOL-Algebra.IntRing
01:44:54 HOL-ODE-Numerics: theory Collections.Intf_Hash
01:44:54 Gauss_Sums: theory Polynomial_Interpolation.Lagrange_Interpolation
01:44:54 MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
01:44:54 Gauss_Sums: theory Gauss_Sums.Finite_Fourier_Series
01:44:54 Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
01:44:55 Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
01:44:55 HOL-ODE-Numerics: theory Collections.Gen_Hash
01:44:55 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
01:44:55 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
01:44:56 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
01:44:56 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.IDirProds
01:44:56 Zeta_Function: theory Budan_Fourier.BF_Misc
01:44:57 Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
01:44:57 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
01:44:57 Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
01:44:58 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
01:44:58 Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
01:44:58 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.DirProds
01:44:58 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Group_Relations
01:44:59 Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
01:44:59 HOL-ODE-Numerics: theory Deriving.Hash_Generator
01:44:59 Gauss_Sums: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
01:44:59 Gauss_Sums: theory Dirichlet_L.Multiplicative_Characters
01:45:00 HOL-ODE-Numerics: theory Deriving.Hash_Instances
01:45:00 HOL-ODE-Numerics: theory Deriving.Derive
01:45:00 Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
01:45:01 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
01:45:01 Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
01:45:01 MDP-Algorithms: theory MDP-Algorithms.PI_Code
01:45:01 Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
01:45:01 Gauss_Sums: theory Dirichlet_L.Dirichlet_Characters
01:45:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
01:45:01 Zeta_Function: theory Zeta_Function.Zeta_Function
01:45:02 Timing Clique_and_Monotone_Circuits (2 threads, 65.688s elapsed time, 86.378s cpu time, 4.200s GC time, factor 1.31)
01:45:02 Finished Clique_and_Monotone_Circuits (0:01:09 elapsed time, 0:01:29 cpu time, factor 1.30)
01:45:02 Gauss_Sums: theory Gauss_Sums.Gauss_Sums_Auxiliary
01:45:02 Gauss_Sums: theory Gauss_Sums.Ramanujan_Sums
01:45:03 Timing TsirelsonBound (2 threads, 88.964s elapsed time, 132.564s cpu time, 5.728s GC time, factor 1.49)
01:45:03 Finished TsirelsonBound (0:01:33 elapsed time, 0:02:16 cpu time, factor 1.47)
01:45:04 Gauss_Sums: theory Gauss_Sums.Gauss_Sums
01:45:04 Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
01:45:04 Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
01:45:05 Gauss_Sums: theory Gauss_Sums.Polya_Vinogradov
01:45:08 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
01:45:08 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
01:45:09 Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
01:45:09 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
01:45:10 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
01:45:10 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
01:45:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
01:45:10 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
01:45:10 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
01:45:10 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
01:45:11 Timing Gauss_Sums (8 threads, 18.322s elapsed time, 99.607s cpu time, 13.254s GC time, factor 5.44)
01:45:11 Finished Gauss_Sums (0:00:20 elapsed time, 0:01:42 cpu time, factor 5.05)
01:45:12 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
01:45:14 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
01:45:17 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
01:45:17 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
01:45:17 Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
01:45:17 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
01:45:18 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
01:45:18 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
01:45:19 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
01:45:19 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
01:45:20 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
01:45:21 Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
01:45:21 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
01:45:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
01:45:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
01:45:24 Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
01:45:24 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
01:45:24 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
01:45:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
01:45:26 Timing Zeta_Function (8 threads, 20.422s elapsed time, 119.420s cpu time, 5.277s GC time, factor 5.85)
01:45:26 Finished Zeta_Function (0:00:35 elapsed time, 0:02:27 cpu time, factor 4.16)
01:45:28 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
01:45:33 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
01:45:36 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
01:45:37 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
01:45:40 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
01:45:41 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
01:45:42 Running Dirichlet_L (on 10.195.7.194) ...
01:45:42 Building Prime_Distribution_Elementary (on 10.195.7.194) ...
01:45:42 Building Prime_Number_Theorem (on 10.195.7.194) ...
01:45:46 Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
01:45:46 Dirichlet_L: theory HOL-Library.Lattice_Algebras
01:45:46 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
01:45:46 Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
01:45:46 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
01:45:46 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
01:45:47 Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
01:45:47 Timing Shadow_SC_DOM (2 threads, 1501.894s elapsed time, 2606.724s cpu time, 566.827s GC time, factor 1.74)
01:45:47 Finished Shadow_SC_DOM (0:26:02 elapsed time, 0:44:51 cpu time, factor 1.72)
01:45:48 Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
01:45:48 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
01:45:48 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
01:45:49 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
01:45:49 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
01:45:49 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
01:45:49 Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
01:45:49 Dirichlet_L: theory HOL-Library.Log_Nat
01:45:50 Dirichlet_L: theory Lehmer.Lehmer
01:45:50 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
01:45:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
01:45:50 Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
01:45:51 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
01:45:51 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
01:45:51 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
01:45:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
01:45:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
01:45:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
01:45:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
01:45:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
01:45:53 Dirichlet_L: theory HOL-Library.Interval
01:45:54 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
01:45:54 Dirichlet_L: theory HOL-Library.Float
01:45:55 Timing Hermite_Lindemann (2 threads, 232.517s elapsed time, 366.846s cpu time, 28.483s GC time, factor 1.58)
01:45:55 Finished Hermite_Lindemann (0:03:57 elapsed time, 0:06:13 cpu time, factor 1.57)
01:45:58 Dirichlet_L: theory HOL-Library.Interval_Float
01:45:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
01:45:59 Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
01:46:02 Timing Universal_Hash_Families (2 threads, 432.151s elapsed time, 739.276s cpu time, 242.245s GC time, factor 1.71)
01:46:02 Finished Universal_Hash_Families (0:07:18 elapsed time, 0:12:27 cpu time, factor 1.71)
01:46:04 Running SC_DOM_Components (on of3.proof.cit.tum.de) ...
01:46:06 Dirichlet_L: theory Bertrands_Postulate.Bertrand
01:46:07 Timing Deep_Learning (2 threads, 435.913s elapsed time, 733.303s cpu time, 152.407s GC time, factor 1.68)
01:46:07 Finished Deep_Learning (0:07:22 elapsed time, 0:12:22 cpu time, factor 1.68)
01:46:08 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
01:46:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
01:46:12 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
01:46:13 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
01:46:13 Timing CryptHOL (2 threads, 242.083s elapsed time, 404.378s cpu time, 35.786s GC time, factor 1.67)
01:46:13 Finished CryptHOL (0:05:08 elapsed time, 0:08:04 cpu time, factor 1.57)
01:46:17 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
01:46:18 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
01:46:19 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
01:46:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
01:46:24 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
01:46:24 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
01:46:25 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
01:46:27 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
01:46:28 Building Game_Based_Crypto (on 10.195.8.46) ...
01:46:28 Building Constructive_Cryptography (on 10.195.8.46) ...
01:46:30 Running Sigma_Commit_Crypto (on of3.proof.cit.tum.de) ...
01:46:30 Running ABY3_Protocols (on of3.proof.cit.tum.de) ...
01:46:32 Timing CoSMeDis (2 threads, 2460.200s elapsed time, 3786.143s cpu time, 481.922s GC time, factor 1.54)
01:46:32 Finished CoSMeDis (0:41:05 elapsed time, 1:03:14 cpu time, factor 1.54)
01:46:32 Constructive_Cryptography: theory Constructive_Cryptography.Resource
01:46:32 ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
01:46:32 ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
01:46:32 Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
01:46:32 Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
01:46:32 Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
01:46:32 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
01:46:32 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
01:46:32 Game_Based_Crypto: theory HOL-Library.LaTeXsugar
01:46:32 Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
01:46:32 ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
01:46:33 Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
01:46:33 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
01:46:33 Sigma_Commit_Crypto: theory HOL-Algebra.Ring
01:46:33 Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
01:46:33 Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
01:46:34 Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
01:46:34 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
01:46:34 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
01:46:34 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
01:46:34 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
01:46:34 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
01:46:34 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
01:46:35 ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
01:46:35 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
01:46:35 ABY3_Protocols: theory ABY3_Protocols.Multiplication
01:46:35 ABY3_Protocols: theory ABY3_Protocols.Shuffle
01:46:35 Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
01:46:35 Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
01:46:35 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
01:46:35 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
01:46:35 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
01:46:35 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
01:46:35 CAVA_LTL_Modelchecker: theory LTL.Rewriting
01:46:35 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
01:46:35 ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
01:46:35 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
01:46:36 Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
01:46:36 Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
01:46:36 Sigma_Commit_Crypto: theory HOL-Algebra.Module
01:46:36 Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
01:46:36 Constructive_Cryptography: theory Constructive_Cryptography.Converter
01:46:38 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
01:46:39 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
01:46:39 Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
01:46:40 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
01:46:40 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
01:46:41 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
01:46:41 Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
01:46:41 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
01:46:41 Timing ABY3_Protocols (6 threads, 8.786s elapsed time, 18.487s cpu time, 0.756s GC time, factor 2.10)
01:46:41 Finished ABY3_Protocols (0:00:10 elapsed time, 0:00:20 cpu time, factor 1.92)
01:46:42 Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
01:46:43 Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
01:46:43 Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
01:46:44 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
01:46:44 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
01:46:45 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
01:46:46 Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
01:46:47 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
01:46:47 Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
01:46:48 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
01:46:48 Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
01:46:48 Constructive_Cryptography: theory Constructive_Cryptography.Random_System
01:46:49 Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
01:46:49 Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
01:46:49 Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
01:46:50 Constructive_Cryptography: theory Constructive_Cryptography.Wiring
01:46:50 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
01:46:51 Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
01:46:52 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
01:46:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
01:46:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
01:46:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
01:46:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
01:46:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
01:46:53 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
01:46:54 Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
01:46:54 Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
01:46:55 Timing Virtual_Substitution (2 threads, 780.876s elapsed time, 1235.092s cpu time, 253.359s GC time, factor 1.58)
01:46:55 Finished Virtual_Substitution (0:13:09 elapsed time, 0:20:48 cpu time, factor 1.58)
01:46:55 Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
01:46:58 Timing DOM_Components (2 threads, 421.788s elapsed time, 830.925s cpu time, 38.586s GC time, factor 1.97)
01:46:58 Finished DOM_Components (0:07:06 elapsed time, 0:13:57 cpu time, factor 1.96)
01:47:03 Timing Sigma_Commit_Crypto (6 threads, 30.400s elapsed time, 144.026s cpu time, 13.527s GC time, factor 4.74)
01:47:03 Finished Sigma_Commit_Crypto (0:00:32 elapsed time, 0:02:27 cpu time, factor 4.52)
01:47:04 Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
01:47:04 Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
01:47:07 Timing Prime_Number_Theorem (2 threads, 45.212s elapsed time, 78.905s cpu time, 5.038s GC time, factor 1.75)
01:47:07 Finished Prime_Number_Theorem (0:01:24 elapsed time, 0:02:05 cpu time, factor 1.49)
01:47:14 Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
01:47:16 Constructive_Cryptography: theory Constructive_Cryptography.Examples
01:47:19 Running Zeta_3_Irrational (on 10.195.8.40) ...
01:47:23 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
01:47:23 Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
01:47:23 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
01:47:24 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
01:47:25 Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
01:47:26 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
01:47:26 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
01:47:26 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
01:47:27 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
01:47:27 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
01:47:29 Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
01:47:32 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
01:47:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
01:47:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
01:47:34 Timing Prime_Distribution_Elementary (2 threads, 68.124s elapsed time, 128.581s cpu time, 6.566s GC time, factor 1.89)
01:47:34 Finished Prime_Distribution_Elementary (0:01:50 elapsed time, 0:02:58 cpu time, factor 1.62)
01:47:37 Running IMO2019 (on 10.195.8.40) ...
01:47:39 IMO2019: theory IMO2019.IMO2019_Q5
01:47:39 IMO2019: theory IMO2019.IMO2019_Q1
01:47:39 Running Irrational_Series_Erdos_Straus (on 10.195.8.11) ...
01:47:40 IMO2019: theory IMO2019.IMO2019_Q4
01:47:43 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
01:47:44 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
01:47:45 Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
01:47:48 Dirichlet_L: theory HOL-Algebra.QuotRing
01:47:48 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
01:47:49 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
01:47:50 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
01:47:50 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
01:47:51 Timing IMO2019 (2 threads, 11.391s elapsed time, 13.802s cpu time, 0.402s GC time, factor 1.21)
01:47:51 Finished IMO2019 (0:00:14 elapsed time, 0:00:16 cpu time, factor 1.15)
01:47:52 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
01:47:54 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
01:47:54 Dirichlet_L: theory HOL-Algebra.IntRing
01:47:56 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
01:47:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
01:47:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
01:47:59 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
01:48:01 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
01:48:02 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
01:48:02 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
01:48:04 Timing Game_Based_Crypto (2 threads, 53.965s elapsed time, 92.561s cpu time, 2.935s GC time, factor 1.72)
01:48:04 Finished Game_Based_Crypto (0:01:33 elapsed time, 0:02:16 cpu time, factor 1.46)
01:48:04 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
01:48:05 Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
01:48:07 Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
01:48:08 Timing Affine_Arithmetic (2 threads, 806.455s elapsed time, 1402.987s cpu time, 233.930s GC time, factor 1.74)
01:48:08 Finished Affine_Arithmetic (0:14:35 elapsed time, 0:24:58 cpu time, factor 1.71)
01:48:10 Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
01:48:10 Running Taylor_Models (on of1-proof+8-15) ...
01:48:10 Running Multi_Party_Computation (on of1-proof+0-7) ...
01:48:12 Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
01:48:12 Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
01:48:12 Multi_Party_Computation: theory HOL-Number_Theory.Cong
01:48:12 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
01:48:12 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
01:48:12 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
01:48:12 Multi_Party_Computation: theory Multi_Party_Computation.ETP
01:48:12 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
01:48:12 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
01:48:13 Timing Irrational_Series_Erdos_Straus (2 threads, 29.476s elapsed time, 54.497s cpu time, 2.407s GC time, factor 1.85)
01:48:13 Finished Irrational_Series_Erdos_Straus (0:00:33 elapsed time, 0:00:58 cpu time, factor 1.76)
01:48:13 Multi_Party_Computation: theory HOL-Algebra.Ring
01:48:13 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
01:48:13 Multi_Party_Computation: theory HOL-Number_Theory.Totient
01:48:13 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
01:48:13 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
01:48:13 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
01:48:14 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
01:48:14 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
01:48:14 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
01:48:14 Multi_Party_Computation: theory Multi_Party_Computation.OT14
01:48:14 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
01:48:15 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
01:48:15 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
01:48:15 Multi_Party_Computation: theory HOL-Algebra.Module
01:48:16 Multi_Party_Computation: theory Multi_Party_Computation.GMW
01:48:18 Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
01:48:18 Multi_Party_Computation: theory HOL-Algebra.Ideal
01:48:18 Taylor_Models: theory Taylor_Models.Polynomial_Expression
01:48:20 Timing Zeta_3_Irrational (2 threads, 56.183s elapsed time, 102.074s cpu time, 3.134s GC time, factor 1.82)
01:48:20 Finished Zeta_3_Irrational (0:01:00 elapsed time, 0:01:45 cpu time, factor 1.76)
01:48:20 Multi_Party_Computation: theory HOL-Algebra.RingHom
01:48:21 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
01:48:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
01:48:24 Timing SC_DOM_Components (6 threads, 138.252s elapsed time, 713.854s cpu time, 42.716s GC time, factor 5.16)
01:48:24 Finished SC_DOM_Components (0:02:20 elapsed time, 0:11:59 cpu time, factor 5.12)
01:48:27 Taylor_Models: theory HOL-Library.Function_Algebras
01:48:27 Taylor_Models: theory Taylor_Models.Horner_Eval
01:48:27 Taylor_Models: theory Taylor_Models.Float_Topology
01:48:27 Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
01:48:27 Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
01:48:29 Taylor_Models: theory Taylor_Models.Taylor_Models
01:48:31 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
01:48:35 Multi_Party_Computation: theory HOL-Number_Theory.Residues
01:48:37 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
01:48:37 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
01:48:37 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
01:48:39 Taylor_Models: theory Taylor_Models.Experiments
01:48:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
01:48:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
01:48:46 Timing Taylor_Models (8 threads, 33.127s elapsed time, 107.376s cpu time, 10.426s GC time, factor 3.24)
01:48:46 Finished Taylor_Models (0:00:35 elapsed time, 0:01:50 cpu time, factor 3.16)
01:48:56 Timing Dirichlet_L (2 threads, 186.973s elapsed time, 348.832s cpu time, 29.221s GC time, factor 1.87)
01:48:56 Finished Dirichlet_L (0:03:12 elapsed time, 0:05:55 cpu time, factor 1.85)
01:48:59 Timing Multi_Party_Computation (8 threads, 46.321s elapsed time, 278.070s cpu time, 22.713s GC time, factor 6.00)
01:48:59 Finished Multi_Party_Computation (0:00:48 elapsed time, 0:04:41 cpu time, factor 5.81)
01:49:08 Timing Probabilistic_Timed_Automata (2 threads, 333.657s elapsed time, 588.745s cpu time, 34.768s GC time, factor 1.76)
01:49:08 Finished Probabilistic_Timed_Automata (0:05:38 elapsed time, 0:09:55 cpu time, factor 1.76)
01:49:17 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
01:49:22 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
01:50:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
01:50:19 Timing Berlekamp_Zassenhaus (2 threads, 440.754s elapsed time, 701.621s cpu time, 131.674s GC time, factor 1.59)
01:50:19 Finished Berlekamp_Zassenhaus (0:08:20 elapsed time, 0:12:57 cpu time, factor 1.55)
01:50:20 Running Linear_Recurrences_Solver (on 10.195.8.46) ...
01:50:21 Building LLL_Basis_Reduction (on 10.195.8.46) ...
01:50:24 CakeML_Codegen: theory Lazy_Case.Lazy_Case
01:50:25 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
01:50:25 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
01:50:29 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
01:50:29 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
01:50:29 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
01:50:29 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
01:50:30 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
01:50:31 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
01:50:32 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
01:50:34 CakeML_Codegen: theory CakeML_Codegen.Test_Composition
01:50:34 Linear_Recurrences_Solver: theory Pure-ex.Guess
01:50:34 Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
01:50:34 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
01:50:35 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
01:50:35 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
01:50:35 Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
01:50:35 Linear_Recurrences_Solver: theory Deriving.Compare_Real
01:50:36 Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
01:50:36 Linear_Recurrences_Solver: theory Polynomials.More_Modules
01:50:37 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
01:50:37 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
01:50:38 Building Algebraic_Numbers (on 10.195.8.42) ...
01:50:38 Running CRYSTALS-Kyber (on 10.195.8.42) ...
01:50:38 Running CVP_Hardness (on 10.195.8.42) ...
01:50:38 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
01:50:39 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
01:50:40 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
01:50:40 CakeML_Codegen: theory CakeML_Codegen.Test_Print
01:50:40 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
01:50:40 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
01:50:40 Running Fishers_Inequality (on of2.proof.cit.tum.de) ...
01:50:42 Fishers_Inequality: theory Card_Partitions.Set_Partition
01:50:42 Fishers_Inequality: theory Polynomials.MPoly_Type
01:50:42 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
01:50:42 Fishers_Inequality: theory Polynomials.More_Modules
01:50:42 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
01:50:42 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
01:50:42 Fishers_Inequality: theory List-Index.List_Index
01:50:42 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
01:50:42 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
01:50:42 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
01:50:42 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
01:50:42 Fishers_Inequality: theory Polynomials.More_MPoly_Type
01:50:42 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
01:50:42 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
01:50:42 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
01:50:43 Fishers_Inequality: theory Design_Theory.Multisets_Extras
01:50:43 CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp
01:50:43 CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes
01:50:43 CVP_Hardness: theory CVP_Hardness.Digits_int
01:50:43 CVP_Hardness: theory CVP_Hardness.Reduction
01:50:43 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:50:43 Fishers_Inequality: theory Design_Theory.Design_Basics
01:50:43 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
01:50:43 CVP_Hardness: theory CVP_Hardness.Partition
01:50:43 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
01:50:43 CVP_Hardness: theory CVP_Hardness.Subset_Sum
01:50:43 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
01:50:43 Fishers_Inequality: theory Polynomials.Utils
01:50:43 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
01:50:43 Fishers_Inequality: theory Design_Theory.Design_Operations
01:50:43 CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product
01:50:43 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
01:50:44 Fishers_Inequality: theory Groebner_Bases.General
01:50:44 Fishers_Inequality: theory Polynomials.Power_Products
01:50:44 CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
01:50:44 Fishers_Inequality: theory Design_Theory.Block_Designs
01:50:44 Fishers_Inequality: theory Design_Theory.Sub_Designs
01:50:44 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
01:50:44 CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm
01:50:44 CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector
01:50:44 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
01:50:44 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
01:50:45 CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
01:50:45 Fishers_Inequality: theory Design_Theory.BIBD
01:50:45 Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:50:45 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
01:50:45 CRYSTALS-Kyber: theory HOL-Number_Theory.Fib
01:50:45 Timing Padic_Field (2 threads, 1057.483s elapsed time, 2078.886s cpu time, 811.897s GC time, factor 1.97)
01:50:45 Finished Padic_Field (0:18:37 elapsed time, 0:36:27 cpu time, factor 1.96)
01:50:46 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
01:50:46 CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers
01:50:46 Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:50:47 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
01:50:47 CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space
01:50:47 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
01:50:47 CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion
01:50:48 CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss
01:50:48 CVP_Hardness: theory Algebraic_Numbers.Resultant
01:50:48 Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
01:50:48 CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity
01:50:49 CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington
01:50:49 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
01:50:49 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
01:50:50 CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots
01:50:50 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
01:50:50 CVP_Hardness: theory CVP_Hardness.Lattice_int
01:50:51 CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product
01:50:51 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:50:51 CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory
01:50:52 CVP_Hardness: theory CVP_Hardness.CVP_p
01:50:52 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
01:50:52 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
01:50:52 CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
01:50:52 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
01:50:53 Algebraic_Numbers: theory Pure-ex.Guess
01:50:53 Algebraic_Numbers: theory Deriving.Compare_Rat
01:50:53 Algebraic_Numbers: theory Deriving.Compare_Real
01:50:53 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
01:50:53 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
01:50:54 Timing Constructive_Cryptography (2 threads, 210.283s elapsed time, 322.198s cpu time, 18.504s GC time, factor 1.53)
01:50:54 Finished Constructive_Cryptography (0:04:23 elapsed time, 0:06:25 cpu time, factor 1.46)
01:50:54 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
01:50:54 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec
01:50:54 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
01:50:54 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
01:50:55 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral
01:50:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
01:50:55 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
01:50:56 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
01:50:56 Timing Complex_Bounded_Operators_Dependencies (2 threads, 962.396s elapsed time, 1702.937s cpu time, 435.817s GC time, factor 1.77)
01:50:56 Finished Complex_Bounded_Operators_Dependencies (0:17:13 elapsed time, 0:30:04 cpu time, factor 1.75)
01:50:56 CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas
01:50:58 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
01:50:58 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
01:50:58 CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT
01:50:58 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus
01:50:58 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr
01:50:59 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
01:50:59 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress
01:51:00 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
01:51:00 Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
01:51:00 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
01:51:01 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme
01:51:01 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
01:51:01 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values
01:51:01 CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme
01:51:02 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:51:02 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
01:51:02 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
01:51:02 Running Constructive_Cryptography_CM (on of2.proof.cit.tum.de) ...
01:51:02 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
01:51:02 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844
01:51:03 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
01:51:03 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
01:51:03 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
01:51:03 Linear_Recurrences_Solver: theory Show.Show_Real
01:51:04 Linear_Recurrences_Solver: theory Show.Show_Complex
01:51:04 Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
01:51:04 Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
01:51:04 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
01:51:04 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT
01:51:04 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
01:51:05 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values
01:51:05 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
01:51:05 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
01:51:05 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
01:51:06 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
01:51:06 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
01:51:06 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
01:51:06 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
01:51:07 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
01:51:07 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
01:51:07 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
01:51:07 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
01:51:07 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
01:51:07 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
01:51:08 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
01:51:08 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
01:51:08 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
01:51:08 Algebraic_Numbers: theory Show.Show_Real
01:51:08 Algebraic_Numbers: theory Show.Show_Complex
01:51:08 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:51:09 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
01:51:09 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
01:51:09 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
01:51:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
01:51:10 Linear_Recurrences_Solver: theory Polynomials.Utils
01:51:10 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
01:51:10 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
01:51:10 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
01:51:11 Linear_Recurrences_Solver: theory Polynomials.Power_Products
01:51:11 CVP_Hardness: theory LLL_Basis_Reduction.Norms
01:51:13 Timing Fishers_Inequality (6 threads, 29.899s elapsed time, 159.294s cpu time, 18.375s GC time, factor 5.33)
01:51:13 Finished Fishers_Inequality (0:00:32 elapsed time, 0:02:42 cpu time, factor 5.07)
01:51:15 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
01:51:16 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
01:51:16 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
01:51:17 Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
01:51:17 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
01:51:18 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
01:51:18 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
01:51:18 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
01:51:18 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
01:51:19 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
01:51:22 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
01:51:22 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
01:51:23 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
01:51:23 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
01:51:26 Timing CAVA_LTL_Modelchecker (2 threads, 413.220s elapsed time, 520.884s cpu time, 52.271s GC time, factor 1.26)
01:51:26 Finished CAVA_LTL_Modelchecker (0:07:10 elapsed time, 0:08:48 cpu time, factor 1.23)
01:51:27 Building Complex_Bounded_Operators (on of2.proof.cit.tum.de) ...
01:51:28 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
01:51:29 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
01:51:29 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
01:51:29 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
01:51:29 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
01:51:29 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
01:51:30 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
01:51:31 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
01:51:31 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
01:51:32 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
01:51:33 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
01:51:33 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
01:51:35 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
01:51:36 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
01:51:36 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
01:51:36 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
01:51:36 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
01:51:37 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
01:51:37 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
01:51:38 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
01:51:38 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
01:51:39 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
01:51:39 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
01:51:40 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
01:51:41 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
01:51:43 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
01:51:43 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
01:51:43 Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
01:51:43 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
01:51:43 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
01:51:44 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
01:51:45 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
01:51:47 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
01:51:48 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
01:51:49 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
01:51:51 Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
01:51:53 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
01:51:55 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
01:52:00 CVP_Hardness: theory CVP_Hardness.infnorm
01:52:01 CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
01:52:01 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
01:52:02 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
01:52:03 CVP_Hardness: theory CVP_Hardness.BHLE
01:52:04 CVP_Hardness: theory CVP_Hardness.SVP_vec
01:52:04 CVP_Hardness: theory CVP_Hardness.CVP_vec
01:52:05 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
01:52:06 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
01:52:06 Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
01:52:07 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
01:52:09 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
01:52:09 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
01:52:09 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
01:52:12 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
01:52:14 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
01:52:14 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
01:52:21 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
01:52:21 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
01:52:23 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
01:52:23 Timing Stochastic_Matrices (2 threads, 524.097s elapsed time, 881.661s cpu time, 185.533s GC time, factor 1.68)
01:52:23 Finished Stochastic_Matrices (0:08:51 elapsed time, 0:14:51 cpu time, factor 1.68)
01:52:38 Timing Complex_Bounded_Operators (6 threads, 54.536s elapsed time, 265.828s cpu time, 26.929s GC time, factor 4.87)
01:52:38 Finished Complex_Bounded_Operators (0:01:10 elapsed time, 0:04:52 cpu time, factor 4.14)
01:52:41 Running Registers (on of2.proof.cit.tum.de) ...
01:52:42 Registers: theory HOL-Eisbach.Eisbach
01:52:42 Registers: theory HOL-Library.Type_Length
01:52:42 Registers: theory HOL-Library.Z2
01:52:42 Registers: theory Registers.Axioms
01:52:42 Registers: theory Registers.Axioms_Classical
01:52:42 Registers: theory Registers.Laws
01:52:42 Registers: theory Registers.Laws_Classical
01:52:43 Registers: theory Registers.Misc
01:52:43 Registers: theory HOL-Library.Word
01:52:43 Registers: theory Registers.Axioms_Complement
01:52:43 Registers: theory Registers.Laws_Complement
01:52:43 Registers: theory Registers.Classical_Extra
01:52:43 Registers: theory Registers.Finite_Tensor_Product
01:52:44 Registers: theory Registers.Axioms_Quantum
01:52:44 Registers: theory Registers.Finite_Tensor_Product_Matrices
01:52:44 Registers: theory Registers.Quantum
01:52:46 Registers: theory Registers.Laws_Quantum
01:52:47 Registers: theory Registers.Quantum_Extra
01:52:48 Registers: theory Registers.Axioms_Complement_Quantum
01:52:48 Registers: theory Registers.QHoare
01:52:48 Registers: theory Registers.Laws_Complement_Quantum
01:52:49 Registers: theory Registers.Check_Autogenerated_Files
01:52:49 Registers: theory Registers.Quantum_Extra2
01:52:49 Registers: theory Registers.Pure_States
01:52:49 Registers: theory Registers.Teleport
01:52:54 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
01:52:55 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
01:53:15 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
01:53:15 Timing Registers (6 threads, 31.146s elapsed time, 145.383s cpu time, 13.711s GC time, factor 4.67)
01:53:15 Finished Registers (0:00:33 elapsed time, 0:02:28 cpu time, factor 4.46)
01:53:21 Timing Constructive_Cryptography_CM (6 threads, 136.167s elapsed time, 605.838s cpu time, 123.361s GC time, factor 4.45)
01:53:21 Finished Constructive_Cryptography_CM (0:02:18 elapsed time, 0:10:10 cpu time, factor 4.40)
01:53:21 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
01:53:26 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
01:53:29 Timing CRYSTALS-Kyber (2 threads, 164.691s elapsed time, 247.682s cpu time, 13.367s GC time, factor 1.50)
01:53:29 Finished CRYSTALS-Kyber (0:02:50 elapsed time, 0:04:13 cpu time, factor 1.49)
01:54:18 Timing CVP_Hardness (2 threads, 212.766s elapsed time, 376.531s cpu time, 21.574s GC time, factor 1.77)
01:54:18 Finished CVP_Hardness (0:03:38 elapsed time, 0:06:22 cpu time, factor 1.75)
01:55:23 Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
01:55:23 Timing CakeML_Codegen (2 threads, 2322.774s elapsed time, 2765.277s cpu time, 120.503s GC time, factor 1.19)
01:55:23 Finished CakeML_Codegen (0:38:50 elapsed time, 0:46:16 cpu time, factor 1.19)
01:55:42 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
01:55:59 Timing LLL_Basis_Reduction (2 threads, 276.623s elapsed time, 464.258s cpu time, 42.144s GC time, factor 1.68)
01:55:59 Finished LLL_Basis_Reduction (0:05:36 elapsed time, 0:08:56 cpu time, factor 1.59)
01:56:02 Running LLL_Factorization (on of2.proof.cit.tum.de) ...
01:56:02 Building Linear_Inequalities (on of2.proof.cit.tum.de) ...
01:56:05 Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
01:56:05 Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
01:56:05 LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
01:56:05 LLL_Factorization: theory LLL_Factorization.Sub_Sums
01:56:05 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
01:56:06 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
01:56:06 Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
01:56:06 Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
01:56:06 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
01:56:06 Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
01:56:08 LLL_Factorization: theory LLL_Factorization.LLL_Factorization
01:56:08 Linear_Inequalities: theory Linear_Inequalities.Cone
01:56:10 Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
01:56:11 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
01:56:12 Linear_Inequalities: theory Linear_Inequalities.Dim_Span
01:56:12 Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
01:56:13 Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
01:56:14 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
01:56:14 Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
01:56:14 Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
01:56:15 Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
01:56:18 Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
01:56:18 Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
01:56:23 Timing LLL_Factorization (6 threads, 17.827s elapsed time, 53.440s cpu time, 5.026s GC time, factor 3.00)
01:56:23 Finished LLL_Factorization (0:00:19 elapsed time, 0:00:55 cpu time, factor 2.78)
01:56:36 Timing Linear_Inequalities (6 threads, 15.971s elapsed time, 60.137s cpu time, 4.652s GC time, factor 3.77)
01:56:36 Finished Linear_Inequalities (0:00:32 elapsed time, 0:01:29 cpu time, factor 2.72)
01:56:45 Running LP_Duality (on 10.195.8.30) ...
01:56:50 LP_Duality: theory LP_Duality.Minimum_Maximum
01:56:50 LP_Duality: theory LP_Duality.LP_Duality
01:57:01 Timing LP_Duality (2 threads, 10.123s elapsed time, 13.409s cpu time, 0.459s GC time, factor 1.32)
01:57:01 Finished LP_Duality (0:00:15 elapsed time, 0:00:18 cpu time, factor 1.20)
01:57:08 Timing Frequency_Moments (2 threads, 1047.841s elapsed time, 1867.689s cpu time, 732.453s GC time, factor 1.78)
01:57:08 Finished Frequency_Moments (0:18:22 elapsed time, 0:32:19 cpu time, factor 1.76)
01:57:24 Building Expander_Graphs (on 10.195.8.46) ...
01:57:32 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
01:57:32 Expander_Graphs: theory Graph_Theory.Rtrancl_On
01:57:32 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
01:57:33 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
01:57:33 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
01:57:34 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
01:57:34 Expander_Graphs: theory Abstract-Rewriting.Seq
01:57:35 Expander_Graphs: theory HOL-Library.More_List
01:57:35 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
01:57:36 Expander_Graphs: theory HOL-Library.While_Combinator
01:57:36 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
01:57:36 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
01:57:37 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
01:57:39 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
01:57:39 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
01:57:40 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
01:57:41 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
01:57:47 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
01:57:48 Expander_Graphs: theory HOL-Decision_Procs.Approximation
01:57:51 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
01:57:51 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
01:57:53 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
01:57:55 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
01:57:56 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
01:57:56 Expander_Graphs: theory Graph_Theory.Stuff
01:57:56 Expander_Graphs: theory Graph_Theory.Digraph
01:57:58 Expander_Graphs: theory Graph_Theory.Arc_Walk
01:58:01 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
01:58:02 Expander_Graphs: theory Graph_Theory.Pair_Digraph
01:58:05 Timing Algebraic_Numbers (2 threads, 388.029s elapsed time, 688.545s cpu time, 43.283s GC time, factor 1.77)
01:58:05 Finished Algebraic_Numbers (0:07:24 elapsed time, 0:12:42 cpu time, factor 1.72)
01:58:07 Running Quantifier_Elimination_Hybrid (on 10.195.8.42) ...
01:58:07 Running BenOr_Kozen_Reif (on 10.195.8.42) ...
01:58:07 Running Factor_Algebraic_Polynomial (on 10.195.8.42) ...
01:58:07 Running Cubic_Quartic_Equations (on 10.195.8.42) ...
01:58:08 Expander_Graphs: theory Graph_Theory.Digraph_Component
01:58:11 BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc
01:58:11 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix
01:58:11 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
01:58:11 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:58:11 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
01:58:11 Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
01:58:11 BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski
01:58:12 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
01:58:12 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
01:58:12 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
01:58:12 Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
01:58:12 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
01:58:13 Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
01:58:13 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux
01:58:13 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type
01:58:13 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
01:58:13 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
01:58:14 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
01:58:14 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
01:58:14 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator
01:58:14 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
01:58:14 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
01:58:14 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
01:58:15 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
01:58:15 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
01:58:15 Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules
01:58:15 Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
01:58:15 Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type
01:58:15 Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots
01:58:15 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta
01:58:15 Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map
01:58:16 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm
01:58:16 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate
01:58:16 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
01:58:16 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials
01:58:17 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc
01:58:17 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski
01:58:18 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
01:58:18 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
01:58:18 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
01:58:18 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
01:58:19 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs
01:58:19 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
01:58:19 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
01:58:20 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
01:58:20 Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:58:21 Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:58:21 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm
01:58:21 Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates
01:58:22 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:58:22 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence
01:58:22 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs
01:58:22 Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
01:58:22 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
01:58:22 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
01:58:22 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
01:58:23 Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
01:58:23 Factor_Algebraic_Polynomial: theory Polynomials.Utils
01:58:23 Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials
01:58:23 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix
01:58:23 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision
01:58:23 Expander_Graphs: theory Matrix.Utility
01:58:24 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
01:58:24 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
01:58:25 Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
01:58:28 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
01:58:28 Expander_Graphs: theory Jordan_Normal_Form.Matrix
01:58:28 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm
01:58:31 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
01:58:31 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs
01:58:33 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision
01:58:33 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm
01:58:33 Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials
01:58:34 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences
01:58:34 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements
01:58:34 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs
01:58:34 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum
01:58:35 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full
01:58:35 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
01:58:36 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
01:58:36 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
01:58:36 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision
01:58:38 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences
01:58:38 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations
01:58:39 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
01:58:39 Quantifier_Elimination_Hybrid: theory Polynomials.Utils
01:58:39 Expander_Graphs: theory Jordan_Normal_Form.Determinant
01:58:39 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders
01:58:40 Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products
01:58:40 Timing Cubic_Quartic_Equations (2 threads, 27.424s elapsed time, 43.539s cpu time, 2.930s GC time, factor 1.59)
01:58:40 Finished Cubic_Quartic_Equations (0:00:32 elapsed time, 0:00:48 cpu time, factor 1.50)
01:58:42 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
01:58:42 Expander_Graphs: theory Regular-Sets.Regular_Set
01:58:43 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
01:58:44 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
01:58:45 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision
01:58:45 Expander_Graphs: theory Regular-Sets.Regular_Exp
01:58:45 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
01:58:46 Expander_Graphs: theory VectorSpace.FunctionLemmas
01:58:46 Expander_Graphs: theory VectorSpace.RingModuleFacts
01:58:47 Expander_Graphs: theory VectorSpace.MonoidSums
01:58:48 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
01:58:48 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
01:58:48 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified
01:58:49 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
01:58:50 Expander_Graphs: theory VectorSpace.LinearCombinations
01:58:51 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
01:58:51 Expander_Graphs: theory Regular-Sets.NDerivative
01:58:56 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
01:58:56 Expander_Graphs: theory VectorSpace.SumSpaces
01:58:56 Expander_Graphs: theory VectorSpace.VectorSpace
01:58:56 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
01:58:57 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class
01:58:57 Expander_Graphs: theory Regular-Sets.Regexp_Method
01:58:58 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
01:59:00 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
01:59:00 Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection
01:59:00 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered
01:59:01 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
01:59:03 Expander_Graphs: theory Matrix.Ordered_Semiring
01:59:04 Expander_Graphs: theory Matrix.Matrix_Legacy
01:59:05 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
01:59:06 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
01:59:08 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
01:59:08 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
01:59:08 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
01:59:08 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
01:59:10 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
01:59:11 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
01:59:12 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
01:59:12 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
01:59:13 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
01:59:15 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
01:59:15 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
01:59:16 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap
01:59:17 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
01:59:18 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
01:59:18 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
01:59:19 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension
01:59:19 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE
01:59:20 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
01:59:21 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps
01:59:22 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms
01:59:23 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
01:59:23 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
01:59:25 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
01:59:25 Expander_Graphs: theory QHLProver.Complex_Matrix
01:59:25 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
01:59:30 Expander_Graphs: theory QHLProver.Gates
01:59:30 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
01:59:31 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn
01:59:34 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting
01:59:35 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations
01:59:37 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
01:59:39 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
01:59:40 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex
01:59:41 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
01:59:42 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms
01:59:44 Timing Automated_Stateful_Protocol_Verification (2 threads, 2062.898s elapsed time, 3933.257s cpu time, 2222.727s GC time, factor 1.91)
01:59:44 Finished Automated_Stateful_Protocol_Verification (0:34:40 elapsed time, 1:06:07 cpu time, factor 1.91)
01:59:44 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
01:59:45 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs
01:59:46 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos
01:59:50 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
01:59:50 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
01:59:53 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
01:59:55 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
01:59:57 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF
01:59:58 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic
01:59:58 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase
01:59:58 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity
01:59:59 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase
02:00:00 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable
02:00:01 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind
02:00:01 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS
02:00:01 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals
02:00:02 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni
02:00:04 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni
02:00:05 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports
02:00:05 Timing Factor_Algebraic_Polynomial (2 threads, 111.300s elapsed time, 199.803s cpu time, 14.884s GC time, factor 1.80)
02:00:05 Finished Factor_Algebraic_Polynomial (0:01:56 elapsed time, 0:03:26 cpu time, factor 1.77)
02:00:05 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni
02:00:06 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs
02:00:08 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad
02:00:10 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props
02:00:13 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs
02:00:14 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments
02:00:14 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs
02:00:15 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence
02:00:17 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
02:00:25 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
02:00:26 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
02:00:49 Timing Linear_Recurrences_Solver (2 threads, 618.545s elapsed time, 1119.533s cpu time, 166.711s GC time, factor 1.81)
02:00:50 Finished Linear_Recurrences_Solver (0:10:25 elapsed time, 0:18:47 cpu time, factor 1.80)
02:01:28 Timing BenOr_Kozen_Reif (2 threads, 194.239s elapsed time, 305.980s cpu time, 22.129s GC time, factor 1.58)
02:01:28 Finished BenOr_Kozen_Reif (0:03:19 elapsed time, 0:05:11 cpu time, factor 1.56)
02:01:30 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
02:01:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
02:01:37 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
02:02:05 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
02:02:18 Timing Smith_Normal_Form (2 threads, 1146.226s elapsed time, 1914.273s cpu time, 570.849s GC time, factor 1.67)
02:02:18 Finished Smith_Normal_Form (0:20:17 elapsed time, 0:33:29 cpu time, factor 1.65)
02:02:18 Running Modular_arithmetic_LLL_and_HNF_algorithms (on 10.195.8.46) ...
02:02:21 Timing MDP-Algorithms (2 threads, 1357.069s elapsed time, 2303.606s cpu time, 753.569s GC time, factor 1.70)
02:02:21 Finished MDP-Algorithms (0:22:45 elapsed time, 0:38:36 cpu time, factor 1.70)
02:02:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
02:02:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
02:02:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
02:02:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
02:02:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
02:02:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
02:02:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
02:02:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
02:02:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
02:02:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
02:02:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
02:02:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
02:02:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
02:02:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
02:02:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
02:02:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
02:02:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
02:02:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
02:02:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
02:02:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
02:02:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
02:02:40 Estimated 0:42:54 build time with path time heuristic (critical: relative time (0.5), parallel: fixed threads (1)) (took 0.124s)
02:02:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
02:02:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
02:02:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
02:02:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
02:02:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
02:02:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
02:02:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
02:02:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
02:02:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
02:02:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
02:02:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
02:02:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
02:02:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
02:02:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
02:02:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
02:03:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
02:03:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
02:03:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
02:03:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
02:03:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
02:03:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
02:03:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
02:03:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
02:03:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
02:03:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
02:03:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
02:03:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
02:03:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
02:03:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
02:03:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
02:03:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
02:03:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
02:03:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
02:03:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
02:03:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
02:03:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
02:03:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
02:03:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
02:03:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
02:03:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
02:03:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
02:03:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
02:03:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
02:03:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
02:03:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
02:03:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
02:04:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
02:04:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
02:04:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
02:04:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
02:04:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
02:04:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
02:04:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
02:04:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
02:04:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
02:04:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
02:04:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
02:04:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
02:04:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
02:04:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
02:04:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
02:04:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
02:04:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
02:04:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
02:04:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
02:04:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
02:05:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
02:05:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
02:05:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
02:05:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
02:05:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
02:05:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
02:05:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
02:05:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
02:05:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
02:05:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
02:05:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
02:05:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
02:05:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
02:05:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
02:05:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
02:06:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
02:06:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
02:06:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
02:06:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
02:06:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
02:06:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
02:06:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
02:06:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
02:06:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
02:06:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
02:06:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
02:06:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
02:06:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
02:06:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
02:06:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
02:06:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
02:06:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
02:06:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
02:06:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
02:06:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
02:06:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
02:06:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
02:06:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
02:06:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
02:06:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
02:07:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
02:07:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
02:08:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
02:08:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
02:08:53 Timing Cook_Levin (2 threads, 2100.699s elapsed time, 3485.776s cpu time, 250.761s GC time, factor 1.66)
02:08:53 Finished Cook_Levin (0:35:07 elapsed time, 0:58:16 cpu time, factor 1.66)
02:10:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
02:10:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
02:11:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
02:11:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
02:11:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
02:11:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
02:12:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
02:12:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
02:12:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
02:12:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
02:12:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
02:14:06 Timing Expander_Graphs (2 threads, 906.664s elapsed time, 1619.590s cpu time, 441.203s GC time, factor 1.79)
02:14:06 Finished Expander_Graphs (0:16:32 elapsed time, 0:28:52 cpu time, factor 1.74)
02:14:12 Running Distributed_Distinct_Elements (on 10.195.8.40) ...
02:14:17 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
02:14:17 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
02:14:18 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
02:14:18 Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
02:14:18 Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
02:14:19 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
02:14:19 Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
02:14:20 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
02:14:25 Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
02:14:27 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
02:14:27 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
02:14:27 Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
02:14:27 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
02:14:28 Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
02:14:33 Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
02:14:34 Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
02:14:35 Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
02:14:36 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
02:14:41 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
02:14:43 Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
02:14:43 Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
02:14:44 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
02:14:48 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
02:14:48 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
02:15:00 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
02:15:01 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
02:15:10 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
02:15:12 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
02:15:14 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
02:15:16 Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
02:16:38 Timing Distributed_Distinct_Elements (2 threads, 139.152s elapsed time, 265.559s cpu time, 16.832s GC time, factor 1.91)
02:16:38 Finished Distributed_Distinct_Elements (0:02:25 elapsed time, 0:04:32 cpu time, factor 1.88)
02:17:07 Timing Quantifier_Elimination_Hybrid (2 threads, 1124.002s elapsed time, 1915.038s cpu time, 420.166s GC time, factor 1.70)
02:17:07 Finished Quantifier_Elimination_Hybrid (0:18:53 elapsed time, 0:32:09 cpu time, factor 1.70)
02:24:16 Timing Crypto_Standards (2 threads, 4020.354s elapsed time, 7669.356s cpu time, 1662.015s GC time, factor 1.91)
02:24:16 Finished Crypto_Standards (1:07:10 elapsed time, 2:08:07 cpu time, factor 1.91)
02:32:59 Timing HOL-ODE-Numerics (2 threads, 2982.728s elapsed time, 5509.750s cpu time, 1083.279s GC time, factor 1.85)
02:32:59 Finished HOL-ODE-Numerics (0:51:35 elapsed time, 1:34:23 cpu time, factor 1.83)
02:33:05 Building Lorenz_Approximation (on 10.195.8.32) ...
02:33:05 Running HOL-ODE-ARCH-COMP (on 10.195.8.32) ...
02:33:05 Running HOL-ODE-Examples (on 10.195.8.32) ...
02:33:05 Running Poincare_Bendixson (on 10.195.8.32) ...
02:33:09 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
02:33:09 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
02:33:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
02:33:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
02:33:09 Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
02:33:09 Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
02:33:09 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
02:33:10 Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
02:33:14 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
02:33:15 Poincare_Bendixson: theory Poincare_Bendixson.Invariance
02:33:17 Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
02:33:19 Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
02:33:21 Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
02:33:27 Poincare_Bendixson: theory Poincare_Bendixson.Examples
02:33:39 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
02:34:53 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
02:35:51 Timing Poincare_Bendixson (2 threads, 160.633s elapsed time, 242.696s cpu time, 19.815s GC time, factor 1.51)
02:35:51 Finished Poincare_Bendixson (0:02:45 elapsed time, 0:04:07 cpu time, factor 1.50)
02:39:52 Timing Lorenz_Approximation (2 threads, 347.266s elapsed time, 647.131s cpu time, 74.315s GC time, factor 1.86)
02:39:52 Finished Lorenz_Approximation (0:06:45 elapsed time, 0:12:04 cpu time, factor 1.79)
02:39:54 Running Lorenz_C0 (on 10.195.8.42) ...
02:39:54 Running Lorenz_C1 (on 10.195.8.42) ...
02:39:59 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
02:39:59 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
02:40:02 Timing Lorenz_C1 (2 threads, 2.241s elapsed time, 2.964s cpu time, 0.064s GC time, factor 1.32)
02:40:02 Finished Lorenz_C1 (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.08)
02:40:08 Estimated 0:23:12 build time with path time heuristic (critical: absolute time (0:10:00), parallel: fixed threads (1)) (took 0.001s)
02:40:19 Timing HOL-ODE-Examples (2 threads, 428.041s elapsed time, 742.041s cpu time, 30.766s GC time, factor 1.73)
02:40:19 Finished HOL-ODE-Examples (0:07:12 elapsed time, 0:12:26 cpu time, factor 1.73)
02:40:41 Timing HOL-ODE-ARCH-COMP (2 threads, 450.459s elapsed time, 868.217s cpu time, 67.392s GC time, factor 1.93)
02:40:41 Finished HOL-ODE-ARCH-COMP (0:07:35 elapsed time, 0:14:33 cpu time, factor 1.92)
02:50:18 Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2860.194s elapsed time, 5228.015s cpu time, 1543.902s GC time, factor 1.83)
02:50:18 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:47:51 elapsed time, 1:27:27 cpu time, factor 1.83)
03:09:11 Timing Lorenz_C0 (2 threads, 1752.293s elapsed time, 3436.583s cpu time, 87.655s GC time, factor 1.96)
03:09:11 Finished Lorenz_C0 (0:29:17 elapsed time, 0:57:21 cpu time, factor 1.96)
03:09:23 *** Host "10.195.8.11": failed to work
03:09:23 *** Error
03:09:23 *** Host "of3.proof.cit.tum.de": failed to work
03:09:23 *** Error
03:09:23 *** Host "10.195.6.179": failed to work
03:09:23 *** ### Ignored report message: int
03:09:23 *** ### Ignored report message: array\ int
03:09:23 *** ### Ignored report message: int
03:09:23 *** Host "10.195.7.194": failed to work
03:09:23 *** Error
03:09:23 *** Host "10.195.8.40": failed to work
03:09:23 *** Error
03:09:23 *** Host "of2.proof.cit.tum.de": failed to work
03:09:23 *** Error
03:09:23 *** Host "of4.proof.cit.tum.de": failed to work
03:09:23 *** Error
03:09:24 *** Host "10.195.8.30": failed to work
03:09:24 *** Error
03:09:24 *** Host "10.195.8.29": failed to work
03:09:24 *** Error
03:09:24 *** Host "10.195.8.46": failed to work
03:09:24 *** Error
03:09:24 *** Host "10.195.8.32": failed to work
03:09:24 *** Error
03:09:24 *** Host "10.195.8.49": failed to work
03:09:24 *** Error
03:09:24 *** Host "10.195.8.42": failed to work
03:09:24 *** Error
03:09:24 Unfinished session(s): CZH_Elementary_Categories, CZH_Universal_Constructions
03:09:24 
03:09:24 Finished at Fri Dec 8 03:09:24 GMT+1 2023
03:09:24 2:19:09 elapsed time, 64:10:30 cpu time, factor 27.67
03:09:24 Build step 'Execute shell' marked build as failure
03:09:25 Started calculate disk usage of build
03:09:25 Finished Calculation of disk usage of build in 0 seconds
03:09:47 Started calculate disk usage of workspace
03:09:47 Finished Calculation of disk usage of workspace in 0 seconds
03:09:48 Finished: FAILURE