Skipping 886 KB.. Full Log

UTP-Toolkit: theory UTP-Toolkit.Partial_Fun
19:17:52 Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
19:17:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
19:17:52 Probabilistic_Timed_Automata: theory Timed_Automata.Regions
19:17:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
19:17:52 Timing Stuttering_Equivalence (6 threads, 2.195s elapsed time, 4.494s cpu time, 0.161s GC time, factor 2.05)
19:17:52 Finished Stuttering_Equivalence (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.70)
19:17:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
19:17:52 Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
19:17:52 Constructive_Cryptography: theory Constructive_Cryptography.Wiring
19:17:52 Timing Stern_Brocot (2 threads, 38.921s elapsed time, 63.597s cpu time, 8.047s GC time, factor 1.63)
19:17:52 Finished Stern_Brocot (0:00:42 elapsed time, 0:01:07 cpu time, factor 1.60)
19:17:52 SuperCalc: theory SuperCalc.equational_clausal_logic
19:17:52 UTP-Toolkit: theory UTP-Toolkit.Finite_Fun
19:17:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
19:17:52 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
19:17:52 UTP-Toolkit: theory UTP-Toolkit.Sequence
19:17:53 MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
19:17:53 Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
19:17:53 UTP-Toolkit: theory UTP-Toolkit.Countable_Set_Extra
19:17:54 Timing SumSquares (6 threads, 3.237s elapsed time, 9.049s cpu time, 0.237s GC time, factor 2.80)
19:17:54 Finished SumSquares (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.30)
19:17:54 Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
19:17:54 Sigma_Commit_Crypto: theory HOL-Algebra.Module
19:17:54 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
19:17:54 Timing CoSMeDis (2 threads, 1819.391s elapsed time, 2883.727s cpu time, 102.798s GC time, factor 1.58)
19:17:54 Finished CoSMeDis (0:30:24 elapsed time, 0:48:10 cpu time, factor 1.58)
19:17:54 UTP-Toolkit: theory UTP-Toolkit.utp_toolkit
19:17:55 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
19:17:55 SuperCalc: theory SuperCalc.superposition
19:17:55 SM: theory SM.SM_Datastructures
19:17:55 Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
19:17:55 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
19:17:56 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
19:17:56 Quantales: theory Quantales.Quantale_Modules
19:17:56 Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
19:17:56 Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
19:17:56 Safe_OCL: theory Safe_OCL.OCL_Object_Model
19:17:56 Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
19:17:56 SM: theory Word_Lib.Bits_Int
19:17:56 Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
19:17:56 Safe_OCL: theory Safe_OCL.OCL_Typing
19:17:57 Probabilistic_Timed_Automata: theory Timed_Automata.Closure
19:17:57 Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
19:17:58 Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
19:17:58 Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
19:17:58 Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
19:17:58 Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
19:17:58 Building Commuting_Hermitian (on 10.195.8.49) ...
19:17:58 Building Symmetric_Polynomials (on 10.195.8.49) ...
19:17:58 Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
19:17:58 Timing Sturm_Tarski (2 threads, 38.693s elapsed time, 67.227s cpu time, 2.909s GC time, factor 1.74)
19:17:58 Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
19:17:58 Finished Sturm_Tarski (0:00:41 elapsed time, 0:01:09 cpu time, factor 1.69)
19:17:59 Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
19:17:59 Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
19:18:00 Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
19:18:00 SM: theory Word_Lib.Typedef_Morphisms
19:18:00 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
19:18:00 Symmetric_Polynomials: theory HOL-Combinatorics.Transposition
19:18:00 Symmetric_Polynomials: theory Abstract-Rewriting.Seq
19:18:01 SM: theory SM.SM_State
19:18:01 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
19:18:01 Symmetric_Polynomials: theory HOL-Combinatorics.Permutations
19:18:01 Symmetric_Polynomials: theory Polynomials.MPoly_Type
19:18:01 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
19:18:02 Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
19:18:02 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Blit
19:18:02 Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
19:18:02 Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
19:18:02 Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
19:18:02 Symmetric_Polynomials: theory Polynomials.More_MPoly_Type
19:18:02 Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
19:18:02 Symmetric_Polynomials: theory Polynomials.More_Modules
19:18:03 Symmetric_Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
19:18:03 Symmetric_Polynomials: theory Symmetric_Polynomials.Vieta
19:18:03 SM: theory SM.SM_Semantics
19:18:03 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
19:18:03 Symmetric_Polynomials: theory Open_Induction.Restricted_Predicates
19:18:04 Promela: theory Promela.PromelaLTL
19:18:04 Symmetric_Polynomials: theory Regular-Sets.Regular_Set
19:18:04 Running Szemeredi_Regularity (on 10.195.8.29) ...
19:18:04 Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials
19:18:04 Running Three_Circles (on 10.195.8.29) ...
19:18:04 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
19:18:04 Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
19:18:04 Timing UTP-Toolkit (8 threads, 9.033s elapsed time, 60.594s cpu time, 3.889s GC time, factor 6.71)
19:18:04 Finished UTP-Toolkit (0:00:17 elapsed time, 0:01:16 cpu time, factor 4.43)
19:18:05 Timing SuperCalc (6 threads, 14.034s elapsed time, 50.865s cpu time, 3.905s GC time, factor 3.62)
19:18:05 Finished SuperCalc (0:00:15 elapsed time, 0:00:52 cpu time, factor 3.45)
19:18:05 Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
19:18:05 Timing ABY3_Protocols (2 threads, 18.810s elapsed time, 26.710s cpu time, 2.220s GC time, factor 1.42)
19:18:05 Finished ABY3_Protocols (0:00:22 elapsed time, 0:00:29 cpu time, factor 1.35)
19:18:05 Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
19:18:05 Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
19:18:06 MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
19:18:06 Three_Circles: theory Sturm_Tarski.PolyMisc
19:18:06 Three_Circles: theory Polynomial_Interpolation.Missing_Unsorted
19:18:06 Timing Stirling_Formula (2 threads, 26.405s elapsed time, 46.085s cpu time, 2.549s GC time, factor 1.75)
19:18:06 Finished Stirling_Formula (0:00:49 elapsed time, 0:01:14 cpu time, factor 1.52)
19:18:06 Three_Circles: theory Sturm_Tarski.Sturm_Tarski
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
19:18:06 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
19:18:06 Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
19:18:07 SM: theory SM.Decide_Locality
19:18:07 Promela: theory Promela.PromelaLTLConv
19:18:07 Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
19:18:07 Symmetric_Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
19:18:07 Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Elements
19:18:08 Symmetric_Polynomials: theory Regular-Sets.Regular_Exp
19:18:08 Running Topology (on 10.195.8.40) ...
19:18:08 MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
19:18:08 Running TortoiseHare (on 10.195.8.40) ...
19:18:08 Symmetric_Polynomials: theory Well_Quasi_Orders.Least_Enum
19:18:08 SM: theory SM.Type_System
19:18:08 Three_Circles: theory Polynomial_Interpolation.Missing_Polynomial
19:18:08 SM: theory SM.SM_LTL
19:18:08 Three_Circles: theory Budan_Fourier.BF_Misc
19:18:10 Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
19:18:10 Three_Circles: theory Budan_Fourier.Budan_Fourier
19:18:10 Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
19:18:10 Three_Circles: theory Polynomial_Interpolation.Ring_Hom
19:18:10 TortoiseHare: theory TortoiseHare.Basis
19:18:10 Topology: theory Topology.Topology
19:18:10 Topology: theory Lazy-Lists-II.LList2
19:18:10 SM: theory SM.SM_Finite_Reachable
19:18:11 TortoiseHare: theory TortoiseHare.Brent
19:18:11 TortoiseHare: theory TortoiseHare.TortoiseHare
19:18:11 Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
19:18:11 SM: theory SM.Rename_Cfg
19:18:11 Timing Saturation_Framework_Extensions (2 threads, 24.847s elapsed time, 36.227s cpu time, 1.564s GC time, factor 1.46)
19:18:11 Finished Saturation_Framework_Extensions (0:00:27 elapsed time, 0:00:38 cpu time, factor 1.41)
19:18:11 Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
19:18:12 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
19:18:12 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
19:18:12 Symmetric_Polynomials: theory Regular-Sets.NDerivative
19:18:12 Symmetric_Polynomials: theory Regular-Sets.Relation_Interpretation
19:18:13 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
19:18:13 Constructive_Cryptography: theory Constructive_Cryptography.Examples
19:18:13 Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
19:18:14 Topology: theory Topology.LList_Topology
19:18:14 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
19:18:15 Three_Circles: theory Polynomial_Interpolation.Ring_Hom_Poly
19:18:16 Timing Sigma_Commit_Crypto (6 threads, 24.624s elapsed time, 110.112s cpu time, 9.004s GC time, factor 4.47)
19:18:16 Finished Sigma_Commit_Crypto (0:00:26 elapsed time, 0:01:52 cpu time, factor 4.26)
19:18:16 Symmetric_Polynomials: theory Regular-Sets.Equivalence_Checking
19:18:16 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
19:18:17 Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
19:18:17 Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
19:18:17 Timing Szemeredi_Regularity (2 threads, 9.737s elapsed time, 13.591s cpu time, 0.399s GC time, factor 1.40)
19:18:17 Finished Szemeredi_Regularity (0:00:13 elapsed time, 0:00:16 cpu time, factor 1.25)
19:18:17 Symmetric_Polynomials: theory Regular-Sets.Regexp_Method
19:18:18 Timing Probabilistic_Noninterference (2 threads, 203.300s elapsed time, 338.418s cpu time, 26.419s GC time, factor 1.66)
19:18:18 Finished Probabilistic_Noninterference (0:03:27 elapsed time, 0:05:43 cpu time, factor 1.66)
19:18:18 Promela: theory Promela.All_Of_Promela
19:18:18 Three_Circles: theory Three_Circles.RRI_Misc
19:18:18 Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full
19:18:18 Timing TortoiseHare (2 threads, 7.771s elapsed time, 9.631s cpu time, 0.329s GC time, factor 1.24)
19:18:18 Finished TortoiseHare (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.13)
19:18:19 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
19:18:19 Three_Circles: theory Three_Circles.Bernstein_01
19:18:19 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
19:18:19 Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:18:20 Three_Circles: theory Three_Circles.Bernstein
19:18:20 Three_Circles: theory Three_Circles.Normal_Poly
19:18:20 Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
19:18:20 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
19:18:20 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
19:18:20 Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
19:18:20 Three_Circles: theory Three_Circles.Three_Circles
19:18:20 Symmetric_Polynomials: theory Polynomials.Utils
19:18:20 Symmetric_Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
19:18:20 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.From_List_GA
19:18:21 Symmetric_Polynomials: theory Polynomials.Power_Products
19:18:21 SM: theory SM.SM_Visible
19:18:21 Timing Topology (2 threads, 10.731s elapsed time, 17.619s cpu time, 1.715s GC time, factor 1.64)
19:18:21 Finished Topology (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.50)
19:18:22 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Examples
19:18:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
19:18:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
19:18:23 SM: theory SM.SM_Pid
19:18:23 Building Prime_Distribution_Elementary (on of3.proof.cit.tum.de) ...
19:18:23 Running CAVA_LTL_Modelchecker (on of3.proof.cit.tum.de) ...
19:18:23 Running Dirichlet_L (on of3.proof.cit.tum.de) ...
19:18:24 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
19:18:24 MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
19:18:24 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
19:18:24 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
19:18:24 MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
19:18:24 Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
19:18:24 Dirichlet_L: theory HOL-Library.Lattice_Algebras
19:18:25 Dirichlet_L: theory HOL-Library.Log_Nat
19:18:25 Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
19:18:25 Dirichlet_L: theory Lehmer.Lehmer
19:18:25 Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
19:18:25 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
19:18:26 SM: theory SM.SM_Variables
19:18:26 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
19:18:26 Running Registers (on of2.proof.cit.tum.de) ...
19:18:26 Timing Sturm_Sequences (2 threads, 45.115s elapsed time, 81.862s cpu time, 4.840s GC time, factor 1.81)
19:18:26 Finished Sturm_Sequences (0:01:09 elapsed time, 0:01:50 cpu time, factor 1.58)
19:18:27 SM: theory SM.SM_Indep
19:18:27 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
19:18:27 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
19:18:27 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
19:18:28 Timing Separation_Logic_Imperative_HOL (2 threads, 113.295s elapsed time, 149.073s cpu time, 8.731s GC time, factor 1.32)
19:18:28 Finished Separation_Logic_Imperative_HOL (0:01:56 elapsed time, 0:02:33 cpu time, factor 1.32)
19:18:28 Registers: theory HOL-Eisbach.Eisbach
19:18:28 Registers: theory HOL-Library.Type_Length
19:18:28 Registers: theory HOL-Library.Z2
19:18:28 Registers: theory Registers.Axioms
19:18:28 Registers: theory Registers.Axioms_Classical
19:18:28 Registers: theory Registers.Laws
19:18:28 Registers: theory Registers.Laws_Classical
19:18:28 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
19:18:28 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
19:18:28 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
19:18:28 Registers: theory Registers.Misc
19:18:28 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
19:18:28 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
19:18:29 Registers: theory HOL-Library.Word
19:18:29 Registers: theory Registers.Axioms_Complement
19:18:29 Registers: theory Registers.Laws_Complement
19:18:29 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
19:18:29 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
19:18:29 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
19:18:29 Building Prime_Number_Theorem (on 10.195.8.46) ...
19:18:29 Running Transitive-Closure (on 10.195.8.46) ...
19:18:29 Dirichlet_L: theory HOL-Library.Interval
19:18:29 Dirichlet_L: theory HOL-Library.Float
19:18:29 Registers: theory Registers.Classical_Extra
19:18:29 Registers: theory Registers.Finite_Tensor_Product
19:18:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
19:18:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
19:18:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
19:18:29 MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
19:18:30 Registers: theory Registers.Axioms_Quantum
19:18:30 Registers: theory Registers.Finite_Tensor_Product_Matrices
19:18:30 Registers: theory Registers.Quantum
19:18:30 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
19:18:30 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph
19:18:30 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc
19:18:31 Refine_Imperative_HOL: theory HOL-Library.Omega_Words_Fun
19:18:31 Refine_Imperative_HOL: theory CAVA_Automata.Digraph_Basic
19:18:31 Registers: theory Registers.Laws_Quantum
19:18:31 Transitive-Closure: theory Matrix.Utility
19:18:31 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight
19:18:31 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
19:18:32 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
19:18:32 Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
19:18:32 Timing Quantales (2 threads, 110.331s elapsed time, 170.146s cpu time, 11.255s GC time, factor 1.54)
19:18:32 Timing Schutz_Spacetime (2 threads, 124.634s elapsed time, 200.406s cpu time, 14.602s GC time, factor 1.61)
19:18:32 Finished Quantales (0:02:11 elapsed time, 0:03:17 cpu time, factor 1.50)
19:18:32 Finished Schutz_Spacetime (0:02:07 elapsed time, 0:03:23 cpu time, factor 1.60)
19:18:32 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
19:18:32 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
19:18:32 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec
19:18:32 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
19:18:32 SM: theory SM.SM_Sticky
19:18:33 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
19:18:33 Dirichlet_L: theory HOL-Library.Interval_Float
19:18:33 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
19:18:33 Registers: theory Registers.Quantum_Extra
19:18:33 Running Transport (on 10.195.7.194) ...
19:18:34 Registers: theory Registers.Axioms_Complement_Quantum
19:18:34 Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
19:18:34 Registers: theory Registers.QHoare
19:18:34 Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
19:18:34 Timing Standard_Borel_Spaces (2 threads, 83.577s elapsed time, 121.393s cpu time, 3.912s GC time, factor 1.45)
19:18:34 Finished Standard_Borel_Spaces (0:01:26 elapsed time, 0:02:04 cpu time, factor 1.43)
19:18:34 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
19:18:34 Running Treaps (on 10.195.8.42) ...
19:18:34 Registers: theory Registers.Laws_Complement_Quantum
19:18:35 Registers: theory Registers.Check_Autogenerated_Files
19:18:35 Registers: theory Registers.Quantum_Extra2
19:18:35 Registers: theory Registers.Teleport
19:18:35 Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class
19:18:35 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
19:18:35 Transport: theory ML_Unification.ML_Code_Utils
19:18:35 Transport: theory ML_Unification.ML_Attribute_Utils
19:18:35 Transport: theory ML_Unification.ML_Conversion_Utils
19:18:35 Registers: theory Registers.Pure_States
19:18:35 Transport: theory ML_Unification.ML_General_Utils
19:18:35 Transport: theory ML_Unification.ML_Generic_Data_Utils
19:18:35 MDP-Algorithms: theory MDP-Algorithms.PI_Code
19:18:35 Transport: theory ML_Unification.ML_Method_Utils
19:18:35 Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
19:18:35 Transport: theory ML_Unification.ML_Normalisations
19:18:36 Transport: theory ML_Unification.ML_Attributes
19:18:36 Transport: theory ML_Unification.ML_Binders
19:18:36 Transport: theory ML_Unification.ML_Term_Utils
19:18:36 Transport: theory ML_Unification.ML_Logger
19:18:36 Transport: theory ML_Unification.ML_Parsing_Utils
19:18:36 Transport: theory ML_Unification.ML_Tactic_Utils
19:18:36 Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph
19:18:36 Transport: theory ML_Unification.ML_Functor_Instances
19:18:36 Transport: theory ML_Unification.ML_Priorities
19:18:37 Transport: theory ML_Unification.ML_Unification_Parsers
19:18:37 Transport: theory ML_Unification.ML_Term_Index
19:18:37 Transport: theory ML_Unification.ML_Unification_Base
19:18:37 Treaps: theory HOL-Data_Structures.Cmp
19:18:37 Transport: theory ML_Unification.ML_Theorem_Utils
19:18:37 Treaps: theory HOL-Data_Structures.Less_False
19:18:37 Building Weighted_Path_Order (on of1-proof+8-15) ...
19:18:37 Transport: theory ML_Unification.Setup_Result_Commands
19:18:37 Building Randomised_Social_Choice (on of1-proof+0-7) ...
19:18:38 Treaps: theory HOL-Data_Structures.Sorted_Less
19:18:38 Transport: theory Transport.HOL_Syntax_Bundles_Functions
19:18:38 Transport: theory ML_Unification.Simps_To
19:18:38 Transport: theory Transport.HOL_Mem_Of
19:18:38 Transport: theory Transport.HOL_Syntax_Bundles_Lattices
19:18:38 Transport: theory Transport.Functions_Surjective
19:18:38 Treaps: theory HOL-Data_Structures.List_Ins_Del
19:18:38 Transport: theory Transport.Predicates_Lattice
19:18:38 Transport: theory Transport.HOL_Syntax_Bundles_Relations
19:18:38 Transport: theory ML_Unification.ML_Unifiers
19:18:38 Transport: theory Transport.HOL_Syntax_Bundles_Groups
19:18:38 Transport: theory Transport.HOL_Syntax_Bundles_Orders
19:18:38 Transport: theory Transport.Predicates_Order
19:18:38 Transport: theory Transport.HOL_Basics_Base
19:18:38 Transport: theory Transport.Binary_Relation_Functions
19:18:38 Timing Transitive-Closure (2 threads, 5.322s elapsed time, 8.988s cpu time, 0.385s GC time, factor 1.69)
19:18:38 Finished Transitive-Closure (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.41)
19:18:38 Transport: theory Transport.Binary_Relations_Antisymmetric
19:18:38 Treaps: theory HOL-Library.Function_Algebras
19:18:38 Transport: theory Transport.Binary_Relations_Irreflexive
19:18:38 Transport: theory Transport.Binary_Relations_Left_Total
19:18:38 Treaps: theory HOL-Data_Structures.Set_Specs
19:18:38 Treaps: theory Landau_Symbols.Group_Sort
19:18:38 Transport: theory Transport.Binary_Relations_Surjective
19:18:38 Running Trie (on of4.proof.cit.tum.de) ...
19:18:38 Transport: theory Transport.Binary_Relations_Order_Base
19:18:38 Running Turans_Graph_Theorem (on of4.proof.cit.tum.de) ...
19:18:38 Transport: theory Transport.Binary_Relations_Lattice
19:18:38 Transport: theory Transport.Functions_Base
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.List_Order
19:18:38 Transport: theory Transport.Function_Relators
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Relations
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Precedence
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Status
19:18:38 Treaps: theory HOL-Data_Structures.Tree_Set
19:18:38 Transport: theory Transport.Functions_Injective
19:18:38 Transport: theory ML_Unification.ML_Unification_Hints
19:18:38 Transport: theory ML_Unification.Unify_Assumption_Tactic
19:18:38 Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
19:18:38 Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
19:18:38 Randomised_Social_Choice: theory List-Index.List_Index
19:18:38 Transport: theory ML_Unification.Unify_Resolve_Tactics
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair
19:18:38 Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
19:18:38 Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
19:18:38 Trie: theory Trie.Trie
19:18:38 Running UTP (on of4.proof.cit.tum.de) ...
19:18:38 Running Undirected_Graph_Theory (on of4.proof.cit.tum.de) ...
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2
19:18:38 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair_Impl
19:18:39 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
19:18:39 Treaps: theory Landau_Symbols.Landau_Real_Products
19:18:39 Trie: theory Trie.Tries
19:18:39 Undirected_Graph_Theory: theory Card_Partitions.Set_Partition
19:18:39 Treaps: theory List-Index.List_Index
19:18:39 Undirected_Graph_Theory: theory HOL-Combinatorics.Transposition
19:18:39 Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Multiset_More
19:18:39 Undirected_Graph_Theory: theory Girth_Chromatic.Girth_Chromatic_Misc
19:18:39 Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
19:18:39 UTP: theory UTP.utp_parser_utils
19:18:39 Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
19:18:39 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Basics
19:18:39 Turans_Graph_Theorem: theory HOL-Library.Code_Abstract_Nat
19:18:39 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Int
19:18:39 Turans_Graph_Theorem: theory HOL-Library.Lattice_Algebras
19:18:39 UTP: theory UTP.utp_var
19:18:39 Turans_Graph_Theorem: theory HOL-Library.Log_Nat
19:18:39 Undirected_Graph_Theory: theory HOL-Combinatorics.Permutations
19:18:39 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
19:18:40 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
19:18:40 Turans_Graph_Theorem: theory HOL-Decision_Procs.Dense_Linear_Order
19:18:40 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Nat
19:18:40 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA
19:18:40 Transport: theory Transport.Functions_Inverse
19:18:40 Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
19:18:40 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
19:18:40 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral
19:18:40 Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
19:18:40 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap
19:18:40 Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
19:18:40 UTP: theory UTP.utp_expr
19:18:40 Transport: theory Transport.Predicates
19:18:40 Transport: theory Transport.Functions_Monotone
19:18:40 Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
19:18:40 Transport: theory ML_Unification.ML_Unification_HOL_Setup
19:18:40 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2_Impl
19:18:40 Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
19:18:40 Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
19:18:41 Transport: theory Transport.Binary_Relations_Reflexive
19:18:41 Transport: theory Transport.Binary_Relations_Symmetric
19:18:41 Transport: theory Transport.Binary_Relations_Injective
19:18:41 Transport: theory Transport.Binary_Relations_Transitive
19:18:41 Transport: theory Transport.Binary_Relations_Order
19:18:41 Transport: theory Transport.Binary_Relations_Right_Unique
19:18:41 Undirected_Graph_Theory: theory Design_Theory.Multisets_Extras
19:18:41 Transport: theory Transport.Preorders
19:18:41 Undirected_Graph_Theory: theory HOL-Combinatorics.Multiset_Permutations
19:18:41 Dirichlet_L: theory Bertrands_Postulate.Bertrand
19:18:41 Transport: theory Transport.Binary_Relation_Properties
19:18:41 Transport: theory Transport.Partial_Equivalence_Relations
19:18:41 Transport: theory Transport.Partial_Orders
19:18:41 Transport: theory Transport.Equivalence_Relations
19:18:41 Transport: theory Transport.Functions_Bijection
19:18:41 Transport: theory Transport.Restricted_Equality
19:18:41 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Walks
19:18:41 Undirected_Graph_Theory: theory Design_Theory.Design_Basics
19:18:41 Transport: theory Transport.LBinary_Relations
19:18:41 Transport: theory Transport.Function_Properties
19:18:41 Transport: theory Transport.LFunctions
19:18:41 Transport: theory Transport.Order_Functions_Base
19:18:41 Transport: theory Transport.HOL_Alignment_Binary_Relations
19:18:41 SM: theory SM.SM_POR
19:18:41 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Triangles
19:18:41 Transport: theory Transport.Closure_Operators
19:18:41 UTP: theory UTP.utp_expr_insts
19:18:41 Transport: theory Transport.Order_Functions
19:18:41 Transport: theory Transport.Order_Functors_Base
19:18:41 Weighted_Path_Order: theory Weighted_Path_Order.WPO
19:18:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
19:18:42 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
19:18:42 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
19:18:42 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Bipartite_Graphs
19:18:42 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Connectivity
19:18:42 UTP: theory UTP.utp_expr_funcs
19:18:42 UTP: theory UTP.utp_unrest
19:18:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
19:18:42 Transport: theory Transport.Galois_Base
19:18:42 Transport: theory Transport.Galois_Relator_Base
19:18:42 Transport: theory Transport.Order_Equivalences
19:18:42 UTP: theory UTP.utp_usedby
19:18:42 Transport: theory Transport.Half_Galois_Property
19:18:42 UTP: theory UTP.utp_subst
19:18:42 UTP: theory UTP.utp_tactics
19:18:42 Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
19:18:43 Transport: theory Transport.HOL_Alignment_Functions
19:18:43 Undirected_Graph_Theory: theory Design_Theory.Design_Operations
19:18:43 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl
19:18:43 Turans_Graph_Theorem: theory HOL-Library.Interval
19:18:43 Turans_Graph_Theorem: theory HOL-Library.Float
19:18:43 Transport: theory Transport.Order_Functors
19:18:43 Transport: theory Transport.Orders
19:18:43 Transport: theory Transport.HOL_Alignment_Orders
19:18:43 Transport: theory Transport.Galois_Property
19:18:43 Transport: theory Transport.Galois_Connections
19:18:43 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Girth_Independence
19:18:43 Weighted_Path_Order: theory Weighted_Path_Order.KBO_Transformation
19:18:43 Transport: theory Transport.Galois_Equivalences
19:18:43 Weighted_Path_Order: theory Weighted_Path_Order.KBO_as_WPO
19:18:44 Treaps: theory Landau_Symbols.Landau_Simprocs
19:18:44 Undirected_Graph_Theory: theory Design_Theory.Block_Designs
19:18:44 Transport: theory Transport.Galois_Relator
19:18:44 Transport: theory Transport.HOL_Algebra_Alignment_Orders
19:18:44 Timing Sepref_IICF (2 threads, 84.746s elapsed time, 137.919s cpu time, 9.572s GC time, factor 1.63)
19:18:44 Finished Sepref_IICF (0:01:49 elapsed time, 0:02:47 cpu time, factor 1.53)
19:18:44 Weighted_Path_Order: theory Weighted_Path_Order.LPO
19:18:44 UTP: theory UTP.utp_meta_subst
19:18:44 Transport: theory Transport.Galois
19:18:44 Transport: theory Transport.Reflexive_Relator
19:18:44 Weighted_Path_Order: theory Weighted_Path_Order.RPO
19:18:45 Transport: theory Transport.Transport_Base
19:18:45 UTP: theory UTP.utp_pred
19:18:45 Treaps: theory Landau_Symbols.Landau_More
19:18:45 Weighted_Path_Order: theory Weighted_Path_Order.Executable_Orders
19:18:46 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
19:18:46 Turans_Graph_Theorem: theory HOL-Library.Interval_Float
19:18:46 Transport: theory Transport.Monotone_Function_Relator
19:18:46 Transport: theory Transport.HOL_Algebra_Alignment_Galois
19:18:46 Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
19:18:46 Undirected_Graph_Theory: theory Design_Theory.BIBD
19:18:46 Safe_OCL: theory Safe_OCL.OCL_Normalization
19:18:46 Transport: theory Transport.Transport_Bijections
19:18:47 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
19:18:47 Transport: theory Transport.Transport_Compositions_Agree_Base
19:18:47 Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS
19:18:47 Transport: theory Transport.Transport_Identity
19:18:47 Transport: theory Transport.Transport_Typedef_Base
19:18:48 Transport: theory Transport.Transport_Compositions_Generic_Base
19:18:48 Undirected_Graph_Theory: theory Design_Theory.Resolvable_Designs
19:18:48 Timing Padic_Field (6 threads, 369.296s elapsed time, 1035.638s cpu time, 470.391s GC time, factor 2.80)
19:18:48 Finished Padic_Field (0:06:12 elapsed time, 0:17:24 cpu time, factor 2.80)
19:18:48 Running Clique_and_Monotone_Circuits (on 10.195.8.49) ...
19:18:48 Transport: theory Transport.Transport_Compositions_Agree_Galois_Property
19:18:48 Undirected_Graph_Theory: theory Design_Theory.Group_Divisible_Designs
19:18:48 UTP: theory UTP.utp_pred_laws
19:18:48 UTP: theory UTP.utp_alphabet
19:18:49 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra
19:18:49 Transport: theory Transport.Transport_Compositions_Agree_Galois_Relator
19:18:49 Timing Trie (6 threads, 9.302s elapsed time, 10.641s cpu time, 0.398s GC time, factor 1.14)
19:18:49 Finished Trie (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.09)
19:18:49 Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
19:18:49 Transport: theory Transport.Transport_Compositions_Agree_Monotone
19:18:49 UTP: theory UTP.utp_lift
19:18:49 SM: theory SM.SM_Ample_Impl
19:18:50 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Theory_Relations
19:18:50 Transport: theory Transport.Transport_Compositions_Agree_Galois_Connection
19:18:50 Treaps: theory Random_BSTs.Random_BSTs
19:18:50 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
19:18:50 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
19:18:50 UTP: theory UTP.utp_healthy
19:18:50 UTP: theory UTP.utp_sequent
19:18:50 Timing Randomised_Social_Choice (8 threads, 6.147s elapsed time, 26.245s cpu time, 2.997s GC time, factor 4.27)
19:18:50 Finished Randomised_Social_Choice (0:00:13 elapsed time, 0:00:38 cpu time, factor 2.94)
19:18:51 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
19:18:51 UTP: theory UTP.utp_rel
19:18:51 Transport: theory Transport.Transport_Compositions_Agree_Galois_Equivalence
19:18:52 Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_FMap
19:18:52 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graphs_Root
19:18:53 UTP: theory UTP.utp_recursion
19:18:53 Running Irrationals_From_THEBOOK (on 10.195.8.29) ...
19:18:53 UTP: theory UTP.utp_state_parser
19:18:53 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
19:18:53 Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
19:18:53 Running Special_Function_Bounds (on 10.195.8.29) ...
19:18:53 UTP: theory UTP.utp_rel_laws
19:18:53 Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
19:18:53 Transport: theory Transport.Transport_Compositions_Agree_Order_Equivalence
19:18:54 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
19:18:54 Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
19:18:55 Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
19:18:55 Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials_Code
19:18:55 Running Universal_Hash_Families (on 10.195.8.30) ...
19:18:55 Running VYDRA_MDL (on 10.195.8.30) ...
19:18:55 Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
19:18:55 Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
19:18:55 Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
19:18:55 UTP: theory UTP.utp_theory
19:18:55 Running Valuation (on 10.195.8.30) ...
19:18:55 Running VectorSpace (on 10.195.8.30) ...
19:18:56 Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
19:18:57 Running Vickrey_Clarke_Groves (on 10.195.8.40) ...
19:18:57 Running WebAssembly (on 10.195.8.40) ...
19:18:57 Timing Roth_Arithmetic_Progressions (2 threads, 187.706s elapsed time, 329.330s cpu time, 23.056s GC time, factor 1.75)
19:18:57 Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
19:18:57 Finished Roth_Arithmetic_Progressions (0:03:12 elapsed time, 0:05:35 cpu time, factor 1.74)
19:18:57 Running Well_Quasi_Orders (on 10.195.8.40) ...
19:18:57 Dirichlet_L: theory HOL-Algebra.QuotRing
19:18:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
19:18:57 Transport: theory Transport.Transport_Compositions_Agree
19:18:57 Transport: theory Transport.Transport_Functions_Base
19:18:57 Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
19:18:57 UTP: theory UTP.utp_hoare
19:18:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
19:18:57 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
19:18:58 Valuation: theory Valuation.Valuation1
19:18:58 VYDRA_MDL: theory VYDRA_MDL.NFA
19:18:58 VYDRA_MDL: theory VYDRA_MDL.Timestamp
19:18:58 VectorSpace: theory VectorSpace.FunctionLemmas
19:18:58 VectorSpace: theory VectorSpace.RingModuleFacts
19:18:58 Transport: theory Transport.Transport_Compositions_Generic_Galois_Property
19:18:58 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
19:18:58 Timing Weighted_Path_Order (8 threads, 12.779s elapsed time, 46.051s cpu time, 3.802s GC time, factor 3.60)
19:18:58 Finished Weighted_Path_Order (0:00:21 elapsed time, 0:01:02 cpu time, factor 2.96)
19:18:59 UTP: theory UTP.utp_concurrency
19:18:59 UTP: theory UTP.utp_rel_opsem
19:18:59 Timing Prime_Distribution_Elementary (6 threads, 20.721s elapsed time, 79.685s cpu time, 3.999s GC time, factor 3.85)
19:18:59 Finished Prime_Distribution_Elementary (0:00:34 elapsed time, 0:01:40 cpu time, factor 2.90)
19:18:59 Universal_Hash_Families: theory HOL-Algebra.Congruence
19:18:59 Universal_Hash_Families: theory HOL-Combinatorics.List_Permutation
19:18:59 UTP: theory UTP.utp_sym_eval
19:18:59 UTP: theory UTP.utp_wp
19:18:59 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.SetUtils
19:18:59 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Argmax
19:18:59 WebAssembly: theory Word_Lib.Bit_Comprehension
19:18:59 WebAssembly: theory Word_Lib.Legacy_Aliases
19:18:59 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families
19:18:59 UTP: theory UTP.utp_dynlog
19:18:59 UTP: theory UTP.utp_sp
19:18:59 Well_Quasi_Orders: theory Abstract-Rewriting.Seq
19:18:59 Well_Quasi_Orders: theory Open_Induction.Restricted_Predicates
19:18:59 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Partitions
19:18:59 VectorSpace: theory VectorSpace.MonoidSums
19:18:59 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationOperators
19:18:59 WebAssembly: theory Word_Lib.More_Divides
19:19:00 Dirichlet_L: theory HOL-Algebra.IntRing
19:19:00 Safe_OCL: theory Safe_OCL.OCL_Examples
19:19:00 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
19:19:00 VectorSpace: theory VectorSpace.LinearCombinations
19:19:00 WebAssembly: theory Word_Lib.Signed_Division_Word
19:19:00 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
19:19:00 Transport: theory Transport.Transport_Compositions_Generic_Galois_Relator
19:19:00 Universal_Hash_Families: theory HOL-Algebra.Order
19:19:00 Well_Quasi_Orders: theory Regular-Sets.Regular_Set
19:19:00 Well_Quasi_Orders: theory Open_Induction.Open_Induction
19:19:00 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
19:19:01 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
19:19:01 Timing Irrationals_From_THEBOOK (2 threads, 4.643s elapsed time, 6.181s cpu time, 0.123s GC time, factor 1.33)
19:19:01 Finished Irrationals_From_THEBOOK (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.18)
19:19:01 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationProperties
19:19:01 UTP: theory UTP.utp
19:19:01 Timing Undirected_Graph_Theory (6 threads, 20.252s elapsed time, 97.771s cpu time, 5.905s GC time, factor 4.83)
19:19:01 Finished Undirected_Graph_Theory (0:00:21 elapsed time, 0:01:39 cpu time, factor 4.65)
19:19:01 Timing Game_Based_Crypto (2 threads, 51.676s elapsed time, 90.718s cpu time, 5.590s GC time, factor 1.76)
19:19:01 Finished Game_Based_Crypto (0:01:16 elapsed time, 0:01:59 cpu time, factor 1.57)
19:19:01 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.MiscTools
19:19:01 WebAssembly: theory Native_Word.Code_Int_Integer_Conversion
19:19:01 UTP: theory UTP.utp_expr_ovld
19:19:01 UTP: theory UTP.utp_simple_time
19:19:01 WebAssembly: theory WebAssembly.Wasm_Type_Abs
19:19:01 Well_Quasi_Orders: theory Well_Quasi_Orders.Multiset_Extension
19:19:01 UTP: theory UTP.utp_full
19:19:01 UTP: theory UTP.utp_easy_parser
19:19:01 UTP: theory UTP.sum_list
19:19:01 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
19:19:01 WebAssembly: theory Word_Lib.Even_More_List
19:19:02 WebAssembly: theory Word_Lib.More_Arithmetic
19:19:02 WebAssembly: theory Word_Lib.More_Bit_Ring
19:19:02 VYDRA_MDL: theory VYDRA_MDL.Interval
19:19:02 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
19:19:02 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
19:19:02 Well_Quasi_Orders: theory Well_Quasi_Orders.Infinite_Sequences
19:19:02 VYDRA_MDL: theory VYDRA_MDL.Timestamp_Lex
19:19:02 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Elements
19:19:02 Universal_Hash_Families: theory HOL-Algebra.Lattice
19:19:02 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
19:19:02 VYDRA_MDL: theory VYDRA_MDL.Timestamp_Prod
19:19:03 WebAssembly: theory Word_Lib.More_Word
19:19:03 VYDRA_MDL: theory VYDRA_MDL.Trace
19:19:03 Well_Quasi_Orders: theory Well_Quasi_Orders.Least_Enum
19:19:03 Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
19:19:03 VYDRA_MDL: theory VYDRA_MDL.Metric_Point_Structure
19:19:03 Transport: theory Transport.Transport_Compositions_Generic_Monotone
19:19:03 Posix-Lexing: theory Posix-Lexing.LexicalVals3
19:19:03 Posix-Lexing: theory Posix-Lexing.Simplifying3
19:19:03 Timing UTP (6 threads, 23.026s elapsed time, 74.635s cpu time, 6.357s GC time, factor 3.24)
19:19:03 Finished UTP (0:00:24 elapsed time, 0:01:16 cpu time, factor 3.12)
19:19:03 Posix-Lexing: theory Posix-Lexing.Positions3
19:19:03 Transport: theory Transport.Transport_Compositions_Generic_Galois_Connection
19:19:04 Valuation: theory Valuation.Valuation2
19:19:04 VYDRA_MDL: theory VYDRA_MDL.MDL
19:19:04 Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
19:19:04 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.StrictCombinatorialAuction
19:19:05 Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
19:19:05 VYDRA_MDL: theory VYDRA_MDL.Window
19:19:05 Universal_Hash_Families: theory HOL-Algebra.Complete_Lattice
19:19:05 Well_Quasi_Orders: theory Regular-Sets.Regular_Exp
19:19:05 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Universes
19:19:05 WebAssembly: theory Native_Word.Code_Target_Word_Base
19:19:05 WebAssembly: theory Word_Lib.Bit_Shifts_Infix_Syntax
19:19:05 Timing Safe_Range_RC (2 threads, 157.078s elapsed time, 284.173s cpu time, 22.244s GC time, factor 1.81)
19:19:05 Finished Safe_Range_RC (0:02:40 elapsed time, 0:04:48 cpu time, factor 1.80)
19:19:05 Treaps: theory Treaps.Treap
19:19:05 Treaps: theory Treaps.Probability_Misc
19:19:05 Transport: theory Transport.Transport_Compositions_Generic_Galois_Equivalence
19:19:06 WebAssembly: theory Word_Lib.Least_significant_bit
19:19:06 Treaps: theory Treaps.Random_List_Permutation
19:19:06 Timing Registers (6 threads, 37.210s elapsed time, 173.217s cpu time, 17.225s GC time, factor 4.66)
19:19:06 Finished Registers (0:00:39 elapsed time, 0:02:56 cpu time, factor 4.50)
19:19:06 Universal_Hash_Families: theory HOL-Algebra.Group
19:19:06 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.UniformTieBreaking
19:19:07 Treaps: theory Treaps.Treap_Sort_and_BSTs
19:19:07 WebAssembly: theory Word_Lib.Aligned
19:19:07 Timing Promela (2 threads, 174.396s elapsed time, 307.690s cpu time, 34.429s GC time, factor 1.76)
19:19:07 Finished Promela (0:03:44 elapsed time, 0:06:36 cpu time, factor 1.77)
19:19:07 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuction
19:19:08 Transport: theory Transport.Transport_Compositions_Generic_Order_Equivalence
19:19:08 Valuation: theory Valuation.Valuation3
19:19:08 Timing Hermite_Lindemann (2 threads, 174.374s elapsed time, 297.775s cpu time, 22.404s GC time, factor 1.71)
19:19:08 Finished Hermite_Lindemann (0:02:58 elapsed time, 0:05:02 cpu time, factor 1.70)
19:19:08 VectorSpace: theory VectorSpace.SumSpaces
19:19:08 WebAssembly: theory Word_Lib.Singleton_Bit_Shifts
19:19:08 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction
19:19:08 Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
19:19:08 WebAssembly: theory Word_Lib.Most_significant_bit
19:19:09 WebAssembly: theory Word_Lib.Generic_set_bit
19:19:09 VectorSpace: theory VectorSpace.VectorSpace
19:19:09 Well_Quasi_Orders: theory Regular-Sets.NDerivative
19:19:09 Well_Quasi_Orders: theory Regular-Sets.Relation_Interpretation
19:19:10 WebAssembly: theory Native_Word.Code_Target_Integer_Bit
19:19:10 WebAssembly: theory Native_Word.Word_Type_Copies
19:19:10 Treaps: theory Treaps.Random_Treap
19:19:10 Universal_Hash_Families: theory HOL-Algebra.Coset
19:19:10 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
19:19:10 Universal_Hash_Families: theory HOL-Algebra.FiniteProduct
19:19:11 WebAssembly: theory Word_Lib.Bits_Int
19:19:11 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
19:19:11 Universal_Hash_Families: theory HOL-Algebra.Ring
19:19:11 Transport: theory Transport.Transport_Compositions_Generic_Order_Base
19:19:11 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
19:19:12 Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
19:19:12 Running PAC_Checker (on of2.proof.cit.tum.de) ...
19:19:12 Timing Simplex (2 threads, 110.815s elapsed time, 196.369s cpu time, 13.394s GC time, factor 1.77)
19:19:12 Finished Simplex (0:02:14 elapsed time, 0:03:46 cpu time, factor 1.69)
19:19:13 Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
19:19:13 Transport: theory Transport.Transport_Compositions_Generic
19:19:13 Timing Dirichlet_L (6 threads, 47.112s elapsed time, 196.813s cpu time, 21.713s GC time, factor 4.18)
19:19:13 Finished Dirichlet_L (0:00:48 elapsed time, 0:03:19 cpu time, factor 4.08)
19:19:13 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
19:19:14 PAC_Checker: theory Deriving.Derive_Manager
19:19:14 PAC_Checker: theory Deriving.Generator_Aux
19:19:14 PAC_Checker: theory HOL-Combinatorics.Transposition
19:19:14 PAC_Checker: theory HOL-Library.Multiset_Order
19:19:14 PAC_Checker: theory HOL-Library.Conditional_Parametricity
19:19:14 PAC_Checker: theory HOL-Library.Fun_Lexorder
19:19:14 PAC_Checker: theory HOL-Library.FuncSet
19:19:14 PAC_Checker: theory HOL-Library.Function_Algebras
19:19:14 PAC_Checker: theory HOL-Library.Groups_Big_Fun
19:19:14 PAC_Checker: theory Abstract-Rewriting.Seq
19:19:14 PAC_Checker: theory HOL-Library.More_List
19:19:14 PAC_Checker: theory HOL-Library.Sublist
19:19:14 PAC_Checker: theory HOL-Library.Countable_Set
19:19:14 PAC_Checker: theory HOL-Library.FSet
19:19:14 PAC_Checker: theory HOL-Library.Poly_Mapping
19:19:14 Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
19:19:14 PAC_Checker: theory HOL-Algebra.Congruence
19:19:14 PAC_Checker: theory HOL-Library.Disjoint_Sets
19:19:14 WebAssembly: theory Word_Lib.Typedef_Morphisms
19:19:14 PAC_Checker: theory HOL-Library.Ramsey
19:19:14 Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
19:19:14 PAC_Checker: theory HOL-Combinatorics.Permutations
19:19:14 Building Flow_Networks (on 10.195.8.46) ...
19:19:15 WebAssembly: theory Word_Lib.Reversed_Bit_Lists
19:19:15 PAC_Checker: theory Polynomials.More_Modules
19:19:15 PAC_Checker: theory HOL-Algebra.Order
19:19:15 Timing Commuting_Hermitian (2 threads, 49.175s elapsed time, 84.845s cpu time, 6.085s GC time, factor 1.73)
19:19:15 Finished Commuting_Hermitian (0:01:15 elapsed time, 0:01:55 cpu time, factor 1.53)
19:19:15 Universal_Hash_Families: theory HOL-Algebra.Divisibility
19:19:15 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph
19:19:15 Transport: theory Transport.Transport_Compositions
19:19:15 PAC_Checker: theory Open_Induction.Restricted_Predicates
19:19:15 Transport: theory Transport.Transport_Natural_Functors_Base
19:19:15 VYDRA_MDL: theory VYDRA_MDL.Preliminaries
19:19:15 VYDRA_MDL: theory VYDRA_MDL.Temporal
19:19:15 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
19:19:15 PAC_Checker: theory PAC_Checker.PAC_Misc
19:19:15 PAC_Checker: theory PAC_Checker.PAC_Version
19:19:15 PAC_Checker: theory PAC_Checker.More_Loops
19:19:15 PAC_Checker: theory Polynomials.MPoly_Type
19:19:16 Timing Turans_Graph_Theorem (6 threads, 34.847s elapsed time, 125.023s cpu time, 10.921s GC time, factor 3.59)
19:19:16 Finished Turans_Graph_Theorem (0:00:36 elapsed time, 0:02:07 cpu time, factor 3.50)
19:19:16 PAC_Checker: theory HOL-Combinatorics.List_Permutation
19:19:16 PAC_Checker: theory Nested_Multisets_Ordinals.Multiset_More
19:19:16 PAC_Checker: theory Regular-Sets.Regular_Set
19:19:16 PAC_Checker: theory Show.Show
19:19:16 PAC_Checker: theory HOL-Algebra.Lattice
19:19:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
19:19:16 PAC_Checker: theory Polynomials.More_MPoly_Type
19:19:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
19:19:16 Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
19:19:16 PAC_Checker: theory Well_Quasi_Orders.Infinite_Sequences
19:19:16 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:19:16 PAC_Checker: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
19:19:16 PAC_Checker: theory Well_Quasi_Orders.Minimal_Elements
19:19:17 PAC_Checker: theory Well_Quasi_Orders.Least_Enum
19:19:17 PAC_Checker: theory Show.Show_Instances
19:19:17 PAC_Checker: theory PAC_Checker.WB_Sort
19:19:17 PAC_Checker: theory Native_Word.Uint64
19:19:17 PAC_Checker: theory HOL-Algebra.Complete_Lattice
19:19:17 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
19:19:17 PAC_Checker: theory HOL-Library.Finite_Map
19:19:17 Flow_Networks: theory CAVA_Base.Statistics
19:19:17 Flow_Networks: theory Flow_Networks.Graph
19:19:17 Flow_Networks: theory HOL-Library.Omega_Words_Fun
19:19:17 Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
19:19:17 PAC_Checker: theory HOL-Algebra.Group
19:19:17 Universal_Hash_Families: theory HOL-Algebra.AbelCoset
19:19:18 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
19:19:18 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
19:19:18 Flow_Networks: theory CAVA_Automata.Digraph_Basic
19:19:18 PAC_Checker: theory Regular-Sets.Regular_Exp
19:19:18 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
19:19:18 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
19:19:18 PAC_Checker: theory HOL-Algebra.Coset
19:19:19 PAC_Checker: theory HOL-Algebra.FiniteProduct
19:19:19 Universal_Hash_Families: theory HOL-Algebra.Module
19:19:19 Flow_Networks: theory DFS_Framework.DFS_Framework_Misc
19:19:19 PAC_Checker: theory HOL-Algebra.Ring
19:19:19 Flow_Networks: theory Program-Conflict-Analysis.LTS
19:19:19 Timing Three_Circles (2 threads, 72.321s elapsed time, 131.007s cpu time, 9.199s GC time, factor 1.81)
19:19:19 Finished Three_Circles (0:01:15 elapsed time, 0:02:14 cpu time, factor 1.78)
19:19:19 VYDRA_MDL: theory VYDRA_MDL.Monitor
19:19:19 Flow_Networks: theory DFS_Framework.DFS_Framework_Refine_Aux
19:19:20 PAC_Checker: theory Regular-Sets.NDerivative
19:19:20 Transport: theory Transport.Transport_Functions_Monotone
19:19:20 PAC_Checker: theory Regular-Sets.Relation_Interpretation
19:19:20 PAC_Checker: theory HOL-Algebra.Generated_Groups
19:19:20 Flow_Networks: theory Flow_Networks.Fofu_Abs_Base
19:19:20 PAC_Checker: theory HOL-Algebra.Divisibility
19:19:20 Flow_Networks: theory CAVA_Base.Code_String
19:19:20 Flow_Networks: theory CAVA_Base.CAVA_Code_Target
19:19:20 Flow_Networks: theory CAVA_Base.CAVA_Base
19:19:20 PAC_Checker: theory HOL-Algebra.Elementary_Groups
19:19:21 Running TsirelsonBound (on 10.195.7.194) ...
19:19:21 Flow_Networks: theory CAVA_Automata.Digraph
19:19:21 Flow_Networks: theory DFS_Framework.Impl_Rev_Array_Stack
19:19:21 WebAssembly: theory Native_Word.Uint8
19:19:21 Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
19:19:22 Universal_Hash_Families: theory HOL-Algebra.Ideal
19:19:22 Running Multi_Party_Computation (on 10.195.8.42) ...
19:19:22 PAC_Checker: theory HOL-Algebra.AbelCoset
19:19:22 PAC_Checker: theory HOL-Algebra.Module
19:19:22 Flow_Networks: theory CAVA_Automata.Digraph_Impl
19:19:23 WebAssembly: theory WebAssembly.Wasm_Ast
19:19:23 Flow_Networks: theory DFS_Framework.Param_DFS
19:19:23 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
19:19:23 PAC_Checker: theory Regular-Sets.Equivalence_Checking
19:19:23 PAC_Checker: theory Regular-Sets.Regexp_Method
19:19:24 PAC_Checker: theory Well_Quasi_Orders.Almost_Full
19:19:24 Building Abstract_Completeness (on of1-proof+8-15) ...
19:19:24 Building Quick_Sort_Cost (on of1-proof+0-7) ...
19:19:24 PAC_Checker: theory PAC_Checker.Finite_Map_Multiset
19:19:24 PAC_Checker: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:19:24 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
19:19:24 PAC_Checker: theory PAC_Checker.PAC_Map_Rel
19:19:24 PAC_Checker: theory HOL-Algebra.Ideal
19:19:24 Abstract_Completeness: theory Collections.ICF_Tools
19:19:25 PAC_Checker: theory Well_Quasi_Orders.Almost_Full_Relations
19:19:25 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
19:19:25 Multi_Party_Computation: theory HOL-Number_Theory.Cong
19:19:25 Abstract_Completeness: theory Collections.Ord_Code_Preproc
19:19:25 Abstract_Completeness: theory Collections.Locale_Code
19:19:25 Abstract_Completeness: theory Abstract_Completeness.Abstract_Completeness
19:19:25 Quick_Sort_Cost: theory HOL-Library.Function_Algebras
19:19:25 Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
19:19:25 Quick_Sort_Cost: theory List-Index.List_Index
19:19:25 PAC_Checker: theory Polynomials.Utils
19:19:25 PAC_Checker: theory Well_Quasi_Orders.Well_Quasi_Orders
19:19:25 PAC_Checker: theory Polynomials.Power_Products
19:19:25 Running Efficient_Weighted_Path_Order (on of4.proof.cit.tum.de) ...
19:19:25 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
19:19:25 Universal_Hash_Families: theory HOL-Algebra.RingHom
19:19:25 Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
19:19:26 PAC_Checker: theory PAC_Checker.PAC_Assoc_Map_Rel
19:19:26 Running Knuth_Morris_Pratt (on of4.proof.cit.tum.de) ...
19:19:26 Multi_Party_Computation: theory HOL-Algebra.Ring
19:19:26 Running Kruskal (on of4.proof.cit.tum.de) ...
19:19:26 TsirelsonBound: theory TsirelsonBound.Tsirelson
19:19:26 Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
19:19:26 Abstract_Completeness: theory Abstract_Completeness.Propositional_Logic
19:19:27 PAC_Checker: theory HOL-Algebra.RingHom
19:19:27 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
19:19:27 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.Indexed_Term
19:19:27 Universal_Hash_Families: theory HOL-Algebra.QuotRing
19:19:27 Knuth_Morris_Pratt: theory HOL-Library.Sublist
19:19:27 Kruskal: theory Kruskal.Kruskal_Misc
19:19:27 Kruskal: theory Kruskal.SeprefUF
19:19:27 Universal_Hash_Families: theory HOL-Algebra.UnivPoly
19:19:27 PAC_Checker: theory HOL-Algebra.QuotRing
19:19:27 PAC_Checker: theory HOL-Algebra.UnivPoly
19:19:27 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.List_Memo_Functions
19:19:27 Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
19:19:28 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
19:19:28 Quick_Sort_Cost: theory Landau_Symbols.Landau_More
19:19:28 Knuth_Morris_Pratt: theory Knuth_Morris_Pratt.KMP
19:19:28 Transport: theory Transport.Transport_Functions_Galois_Property
19:19:28 Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
19:19:29 Flow_Networks: theory DFS_Framework.DFS_Invars_Basic
19:19:29 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Approx
19:19:29 Multi_Party_Computation: theory HOL-Number_Theory.Totient
19:19:29 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
19:19:29 CAVA_LTL_Modelchecker: theory LTL.Rewriting
19:19:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
19:19:29 Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
19:19:30 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Mem_Impl
19:19:30 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
19:19:30 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
19:19:30 Universal_Hash_Families: theory HOL-Algebra.IntRing
19:19:31 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
19:19:31 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
19:19:31 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
19:19:31 Timing Prime_Number_Theorem (2 threads, 39.830s elapsed time, 68.117s cpu time, 3.895s GC time, factor 1.71)
19:19:31 Finished Prime_Number_Theorem (0:01:01 elapsed time, 0:01:34 cpu time, factor 1.53)
19:19:32 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
19:19:32 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
19:19:32 Flow_Networks: theory DFS_Framework.General_DFS_Structure
19:19:32 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Unbounded
19:19:33 Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Mem_Impl
19:19:33 Multi_Party_Computation: theory HOL-Algebra.Module
19:19:33 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
19:19:33 Running Multiset_Ordering_NPC (on 10.195.6.179) ...
19:19:33 PAC_Checker: theory Polynomials.MPoly_Type_Class
19:19:34 Timing Abstract_Completeness (8 threads, 3.828s elapsed time, 9.996s cpu time, 0.787s GC time, factor 2.61)
19:19:34 Running Transformer_Semantics (on 10.195.6.179) ...
19:19:34 Finished Abstract_Completeness (0:00:08 elapsed time, 0:00:17 cpu time, factor 2.10)
19:19:35 Timing Three_Squares (2 threads, 860.321s elapsed time, 1427.710s cpu time, 391.584s GC time, factor 1.66)
19:19:35 Finished Three_Squares (0:15:19 elapsed time, 0:25:07 cpu time, factor 1.64)
19:19:35 Timing Efficient_Weighted_Path_Order (6 threads, 6.837s elapsed time, 14.516s cpu time, 2.648s GC time, factor 2.12)
19:19:35 Finished Efficient_Weighted_Path_Order (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.97)
19:19:35 Transport: theory Transport.Transport_Functions_Order_Base
19:19:35 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
19:19:35 Multi_Party_Computation: theory HOL-Algebra.Ideal
19:19:35 Timing Knuth_Morris_Pratt (6 threads, 7.246s elapsed time, 26.499s cpu time, 1.557s GC time, factor 3.66)
19:19:35 Finished Knuth_Morris_Pratt (0:00:08 elapsed time, 0:00:27 cpu time, factor 3.22)
19:19:35 PAC_Checker: theory HOL-Algebra.Multiplicative_Group
19:19:36 Timing Treaps (2 threads, 57.350s elapsed time, 103.355s cpu time, 5.023s GC time, factor 1.80)
19:19:36 Finished Treaps (0:01:00 elapsed time, 0:01:46 cpu time, factor 1.76)
19:19:36 Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Propositional_Formula
19:19:36 Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_More
19:19:36 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
19:19:36 Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
19:19:37 Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
19:19:37 VYDRA_MDL: theory VYDRA_MDL.Monitor_Code
19:19:37 Timing Special_Function_Bounds (2 threads, 41.152s elapsed time, 66.743s cpu time, 3.695s GC time, factor 1.62)
19:19:37 Finished Special_Function_Bounds (0:00:43 elapsed time, 0:01:08 cpu time, factor 1.59)
19:19:37 Kruskal: theory Dijkstra_Shortest_Path.Graph
19:19:37 Kruskal: theory HOL-Library.Uprod
19:19:37 Kruskal: theory Dijkstra_Shortest_Path.Weight
19:19:37 Kruskal: theory Matroids.Indep_System
19:19:37 Kruskal: theory Matroids.Matroid
19:19:38 Kruskal: theory Kruskal.UGraph
19:19:38 Kruskal: theory Kruskal.MinWeightBasis
19:19:38 Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
19:19:38 PAC_Checker: theory HOL-Algebra.Ring_Divisibility
19:19:38 PAC_Checker: theory HOL-Algebra.Subrings
19:19:38 Kruskal: theory Kruskal.Kruskal
19:19:38 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
19:19:38 Multi_Party_Computation: theory HOL-Algebra.RingHom
19:19:39 Kruskal: theory Kruskal.Graph_Definition
19:19:39 Kruskal: theory Kruskal.Kruskal_Refine
19:19:39 Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_in_NP
19:19:39 Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_NP_Hard
19:19:39 Kruskal: theory Kruskal.Kruskal_Impl
19:19:39 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
19:19:39 Kruskal: theory Kruskal.Graph_Definition_Aux
19:19:39 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
19:19:40 Multi_Party_Computation: theory Multi_Party_Computation.ETP
19:19:40 Transport: theory Transport.Transport_Functions_Galois_Connection
19:19:40 Kruskal: theory Kruskal.Graph_Definition_Impl
19:19:40 Kruskal: theory Kruskal.UGraph_Impl
19:19:40 Flow_Networks: theory DFS_Framework.Rec_Impl
19:19:40 WebAssembly: theory WebAssembly.Wasm_Base_Defs
19:19:40 Timing Well_Quasi_Orders (2 threads, 39.491s elapsed time, 64.094s cpu time, 6.187s GC time, factor 1.62)
19:19:40 Finished Well_Quasi_Orders (0:00:42 elapsed time, 0:01:07 cpu time, factor 1.59)
19:19:40 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
19:19:40 Running VerifyThis2018 (on 10.195.8.49) ...
19:19:40 Timing Quick_Sort_Cost (8 threads, 5.637s elapsed time, 22.340s cpu time, 2.045s GC time, factor 3.96)
19:19:40 Finished Quick_Sort_Cost (0:00:15 elapsed time, 0:00:40 cpu time, factor 2.65)
19:19:41 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
19:19:41 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
19:19:41 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
19:19:41 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
19:19:41 WebAssembly: theory WebAssembly.Wasm
19:19:41 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
19:19:43 VerifyThis2018: theory VerifyThis2018.Synth_Definition
19:19:43 VerifyThis2018: theory VerifyThis2018.Dynamic_Array
19:19:43 WebAssembly: theory WebAssembly.Wasm_Axioms
19:19:43 WebAssembly: theory WebAssembly.Wasm_Checker_Types
19:19:43 WebAssembly: theory WebAssembly.Wasm_Properties_Aux
19:19:44 VerifyThis2018: theory VerifyThis2018.DF_System
19:19:44 PAC_Checker: theory HOL-Algebra.Polynomials
19:19:44 VerifyThis2018: theory VerifyThis2018.DRAT_Misc
19:19:44 Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
19:19:44 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
19:19:44 WebAssembly: theory WebAssembly.Wasm_Properties
19:19:44 Timing VectorSpace (2 threads, 45.232s elapsed time, 68.536s cpu time, 4.742s GC time, factor 1.52)
19:19:44 Finished VectorSpace (0:00:48 elapsed time, 0:01:11 cpu time, factor 1.47)
19:19:44 VerifyThis2018: theory VerifyThis2018.Array_Map_Default
19:19:44 Transport: theory Transport.Transport_Natural_Functors_Galois
19:19:45 VerifyThis2018: theory VerifyThis2018.Exc_Nres_Monad
19:19:45 Timing Kruskal (6 threads, 17.013s elapsed time, 47.593s cpu time, 3.264s GC time, factor 2.80)
19:19:45 Finished Kruskal (0:00:18 elapsed time, 0:00:49 cpu time, factor 2.66)
19:19:45 WebAssembly: theory WebAssembly.Wasm_Soundness
19:19:45 WebAssembly: theory WebAssembly.Wasm_Interpreter
19:19:46 Running VerifyThis2019 (on 10.195.8.29) ...
19:19:46 Running XML (on 10.195.8.29) ...
19:19:46 Running Arith_Prog_Rel_Primes (on 10.195.8.29) ...
19:19:47 VerifyThis2018: theory VerifyThis2018.VTcomp
19:19:47 Flow_Networks: theory DFS_Framework.Tailrec_Impl
19:19:47 WebAssembly: theory WebAssembly.Wasm_Checker
19:19:48 Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
19:19:48 Flow_Networks: theory DFS_Framework.Simple_Impl
19:19:48 XML: theory Deriving.Derive_Manager
19:19:48 XML: theory Deriving.Generator_Aux
19:19:48 XML: theory Certification_Monads.Error_Syntax
19:19:48 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
19:19:48 Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
19:19:48 XML: theory Certification_Monads.Error_Monad
19:19:48 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test
19:19:48 Transport: theory Transport.Transport_Functions_Galois_Equivalence
19:19:48 VerifyThis2018: theory VerifyThis2018.Snippets
19:19:48 XML: theory Partial_Function_MR.Partial_Function_MR
19:19:48 Universal_Hash_Families: theory HOL-Algebra.Subrings
19:19:48 VerifyThis2019: theory VerifyThis2019.Exc_Nres_Monad
19:19:49 XML: theory Certification_Monads.Strict_Sum
19:19:49 Flow_Networks: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
19:19:49 Running Buffons_Needle (on 10.195.8.40) ...
19:19:49 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
19:19:50 XML: theory Show.Show
19:19:51 Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
19:19:51 VerifyThis2019: theory VerifyThis2019.VTcomp
19:19:51 Flow_Networks: theory Flow_Networks.Fofu_Impl_Base
19:19:52 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
19:19:52 XML: theory Certification_Monads.Parser_Monad
19:19:52 Multi_Party_Computation: theory Multi_Party_Computation.OT14
19:19:53 Multi_Party_Computation: theory HOL-Number_Theory.Residues
19:19:53 Timing Transformer_Semantics (2 threads, 16.282s elapsed time, 28.151s cpu time, 1.532s GC time, factor 1.73)
19:19:53 Finished Transformer_Semantics (0:00:18 elapsed time, 0:00:30 cpu time, factor 1.62)
19:19:53 XML: theory XML.Xml
19:19:54 Flow_Networks: theory DFS_Framework.Restr_Impl
19:19:54 VerifyThis2019: theory VerifyThis2019.Parallel_Multiset_Fold
19:19:54 VerifyThis2019: theory VerifyThis2019.Challenge1A
19:19:54 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
19:19:54 Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
19:19:55 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
19:19:55 Timing Safe_OCL (2 threads, 209.079s elapsed time, 336.056s cpu time, 33.600s GC time, factor 1.61)
19:19:55 Finished Safe_OCL (0:03:33 elapsed time, 0:05:41 cpu time, factor 1.60)
19:19:55 VerifyThis2019: theory VerifyThis2019.Challenge3
19:19:55 Multi_Party_Computation: theory Multi_Party_Computation.GMW
19:19:55 Timing Functional_Ordered_Resolution_Prover (2 threads, 274.080s elapsed time, 411.935s cpu time, 32.688s GC time, factor 1.50)
19:19:55 Finished Functional_Ordered_Resolution_Prover (0:04:38 elapsed time, 0:06:57 cpu time, factor 1.50)
19:19:55 Flow_Networks: theory Flow_Networks.Refine_Add_Fofu
19:19:55 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
19:19:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
19:19:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
19:19:56 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
19:19:56 VerifyThis2019: theory VerifyThis2019.Challenge1B
19:19:56 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
19:19:56 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
19:19:56 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
19:19:56 Universal_Hash_Families: theory HOL-Algebra.Polynomials
19:19:56 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
19:19:56 VerifyThis2019: theory VerifyThis2019.Challenge2A
19:19:56 Flow_Networks: theory DFS_Framework.DFS_Framework
19:19:56 Timing Simple_Clause_Learning (2 threads, 668.556s elapsed time, 1052.371s cpu time, 145.979s GC time, factor 1.57)
19:19:56 Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
19:19:56 Finished Simple_Clause_Learning (0:11:13 elapsed time, 0:17:38 cpu time, factor 1.57)
19:19:57 Timing Clique_and_Monotone_Circuits (2 threads, 65.984s elapsed time, 79.413s cpu time, 1.877s GC time, factor 1.20)
19:19:57 Finished Clique_and_Monotone_Circuits (0:01:08 elapsed time, 0:01:22 cpu time, factor 1.19)
19:19:57 Timing Arith_Prog_Rel_Primes (2 threads, 8.539s elapsed time, 11.596s cpu time, 0.463s GC time, factor 1.36)
19:19:57 Finished Arith_Prog_Rel_Primes (0:00:11 elapsed time, 0:00:13 cpu time, factor 1.26)
19:19:57 Flow_Networks: theory DFS_Framework.Reachable_Nodes
19:19:58 WebAssembly: theory WebAssembly.Wasm_Checker_Properties
19:19:58 XML: theory XML.Xmlt
19:19:58 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
19:19:58 Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.RPO_NP_Hard
19:19:58 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
19:19:59 WebAssembly: theory WebAssembly.Wasm_Interpreter_Properties
19:19:59 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
19:19:59 Shadow_SC_DOM: theory Shadow_SC_DOM.slots
19:20:00 Transport: theory Transport.Transport_Natural_Functors_Galois_Relator
19:20:00 Timing Stochastic_Matrices (6 threads, 145.045s elapsed time, 563.612s cpu time, 208.043s GC time, factor 3.89)
19:20:00 Finished Stochastic_Matrices (0:02:27 elapsed time, 0:09:28 cpu time, factor 3.86)
19:20:00 Transport: theory Transport.Transport_Natural_Functors_Order_Base
19:20:01 Timing Buffons_Needle (2 threads, 8.501s elapsed time, 14.416s cpu time, 0.324s GC time, factor 1.70)
19:20:01 Finished Buffons_Needle (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.49)
19:20:01 Timing Formal_SSA (2 threads, 594.262s elapsed time, 785.548s cpu time, 28.272s GC time, factor 1.32)
19:20:01 Finished Formal_SSA (0:10:37 elapsed time, 0:14:02 cpu time, factor 1.32)
19:20:01 Transport: theory Transport.Transport_Natural_Functors_Order_Equivalence
19:20:02 Timing Symmetric_Polynomials (2 threads, 94.204s elapsed time, 176.609s cpu time, 18.915s GC time, factor 1.87)
19:20:02 Finished Symmetric_Polynomials (0:02:02 elapsed time, 0:03:31 cpu time, factor 1.72)
19:20:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
19:20:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples
19:20:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption
19:20:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench
19:20:04 Running Farkas (on of3.proof.cit.tum.de) ...
19:20:04 Running IMO2019 (on of3.proof.cit.tum.de) ...
19:20:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph
19:20:04 Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
19:20:04 VerifyThis2018: theory VerifyThis2018.Challenge1_short
19:20:04 VerifyThis2018: theory VerifyThis2018.Challenge1
19:20:05 Farkas: theory HOL-Combinatorics.Transposition
19:20:05 Farkas: theory HOL-Algebra.Congruence
19:20:05 Farkas: theory HOL-Computational_Algebra.Factorial_Ring
19:20:05 Farkas: theory Jordan_Normal_Form.Conjugate
19:20:05 Farkas: theory Farkas.Farkas
19:20:05 Farkas: theory HOL-Combinatorics.Permutations
19:20:05 IMO2019: theory IMO2019.IMO2019_Q5
19:20:05 IMO2019: theory IMO2019.IMO2019_Q4
19:20:05 IMO2019: theory IMO2019.IMO2019_Q1
19:20:05 Timing Valuation (2 threads, 66.136s elapsed time, 101.405s cpu time, 8.079s GC time, factor 1.53)
19:20:05 Finished Valuation (0:01:08 elapsed time, 0:01:44 cpu time, factor 1.51)
19:20:06 Running Zeta_3_Irrational (on of2.proof.cit.tum.de) ...
19:20:06 Farkas: theory HOL-Algebra.Order
19:20:06 Transport: theory Transport.Transport_Functions_Order_Equivalence
19:20:07 Farkas: theory Jordan_Normal_Form.Missing_Misc
19:20:07 Running Abstract_Soundness (on 10.195.8.46) ...
19:20:07 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
19:20:07 Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
19:20:07 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
19:20:07 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
19:20:07 Farkas: theory HOL-Algebra.Lattice
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
19:20:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
19:20:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS
19:20:08 Transport: theory Transport.Transport_Functions_Relation_Simplifications
19:20:08 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
19:20:08 Farkas: theory HOL-Algebra.Complete_Lattice
19:20:08 Farkas: theory Farkas.Simplex_for_Reals
19:20:08 Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
19:20:09 Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
19:20:09 PAC_Checker: theory PAC_Checker.PAC_More_Poly
19:20:09 VerifyThis2019: theory VerifyThis2019.Challenge2B
19:20:09 Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
19:20:09 VerifyThis2018: theory VerifyThis2018.Challenge2
19:20:09 Farkas: theory HOL-Algebra.Group
19:20:10 PAC_Checker: theory PAC_Checker.PAC_Specification
19:20:10 PAC_Checker: theory PAC_Checker.PAC_Polynomials
19:20:10 PAC_Checker: theory PAC_Checker.PAC_Checker_Specification
19:20:10 Running Power_Sum_Polynomials (on 10.195.8.11) ...
19:20:10 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
19:20:11 VerifyThis2018: theory VerifyThis2018.Challenge3
19:20:11 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
19:20:11 Transport: theory Transport.Transport_Functions_Galois_Relator
19:20:11 PAC_Checker: theory PAC_Checker.PAC_Polynomials_Term
19:20:11 Farkas: theory HOL-Algebra.FiniteProduct
19:20:11 Timing IMO2019 (6 threads, 5.986s elapsed time, 8.577s cpu time, 0.658s GC time, factor 1.43)
19:20:11 Finished IMO2019 (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.30)
19:20:12 Farkas: theory HOL-Algebra.Ring
19:20:12 Farkas: theory Polynomial_Interpolation.Ring_Hom
19:20:12 Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Unsorted
19:20:12 Power_Sum_Polynomials: theory Matrix.Utility
19:20:12 Running Comparison_Sort_Lower_Bound (on 10.195.7.194) ...
19:20:12 Timing XML (2 threads, 23.849s elapsed time, 40.807s cpu time, 5.049s GC time, factor 1.71)
19:20:12 Finished XML (0:00:26 elapsed time, 0:00:44 cpu time, factor 1.66)
19:20:14 Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_List
19:20:14 Running ConcurrentIMP (on 10.195.8.42) ...
19:20:14 Running DigitsInBase (on 10.195.8.42) ...
19:20:15 Running FOL_Seq_Calc1 (on 10.195.8.42) ...
19:20:15 Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Polynomial
19:20:15 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS
19:20:15 Farkas: theory HOL-Algebra.Module
19:20:16 PAC_Checker: theory PAC_Checker.PAC_Polynomials_Operations
19:20:16 Farkas: theory Jordan_Normal_Form.Missing_Ring
19:20:16 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
19:20:16 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
19:20:16 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
19:20:16 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
19:20:16 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
19:20:16 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
19:20:16 DigitsInBase: theory DigitsInBase.DigitsInBase
19:20:16 Running Zeckendorf (on of1-proof+8-15) ...
19:20:16 Building Random_BSTs (on of1-proof+0-7) ...
19:20:16 Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Polynomial_Factorial
19:20:16 ConcurrentIMP: theory ConcurrentIMP.LTL
19:20:16 Power_Sum_Polynomials: theory Polynomial_Factorization.Order_Polynomial
19:20:16 Power_Sum_Polynomials: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
19:20:16 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
19:20:16 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
19:20:16 Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Multiset
19:20:16 Zeckendorf: theory Zeckendorf.Zeckendorf
19:20:17 Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
19:20:17 Power_Sum_Polynomials: theory Polynomial_Factorization.Prime_Factorization
19:20:17 Random_BSTs: theory HOL-Data_Structures.Less_False
19:20:17 Random_BSTs: theory HOL-Data_Structures.Cmp
19:20:17 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
19:20:17 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
19:20:17 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
19:20:17 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
19:20:17 Running Minimal_SSA (on of4.proof.cit.tum.de) ...
19:20:17 Random_BSTs: theory HOL-Data_Structures.Set_Specs
19:20:17 Running FOL_Seq_Calc2 (on of4.proof.cit.tum.de) ...
19:20:17 Running FOL_Seq_Calc3 (on of4.proof.cit.tum.de) ...
19:20:17 Running Falling_Factorial_Sum (on of4.proof.cit.tum.de) ...
19:20:17 Random_BSTs: theory HOL-Data_Structures.Tree_Set
19:20:18 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent2
19:20:18 Farkas: theory Jordan_Normal_Form.Matrix
19:20:18 Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials
19:20:18 Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom
19:20:18 Random_BSTs: theory Random_BSTs.Random_BSTs
19:20:19 Timing Zeta_3_Irrational (6 threads, 10.389s elapsed time, 54.009s cpu time, 1.620s GC time, factor 5.20)
19:20:19 Finished Zeta_3_Irrational (0:00:11 elapsed time, 0:00:55 cpu time, factor 4.68)
19:20:19 FOL_Seq_Calc2: theory FOL_Seq_Calc2.SeCaV
19:20:19 FOL_Seq_Calc3: theory FOL_Seq_Calc3.List_Syntax
19:20:19 FOL_Seq_Calc2: theory Collections.ICF_Tools
19:20:19 FOL_Seq_Calc2: theory FOL-Fitting.FOL_Fitting
19:20:19 Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
19:20:19 FOL_Seq_Calc3: theory Collections.ICF_Tools
19:20:19 Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
19:20:19 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Fair_Stream
19:20:19 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Syntax
19:20:19 FOL_Seq_Calc3: theory Collections.Ord_Code_Preproc
19:20:19 FOL_Seq_Calc2: theory Collections.Ord_Code_Preproc
19:20:19 FOL_Seq_Calc3: theory Collections.Locale_Code
19:20:19 FOL_Seq_Calc2: theory Collections.Locale_Code
19:20:19 FOL_Seq_Calc3: theory Abstract_Completeness.Abstract_Completeness
19:20:19 Falling_Factorial_Sum: theory Discrete_Summation.Factorials
19:20:19 FOL_Seq_Calc2: theory Abstract_Completeness.Abstract_Completeness
19:20:19 Minimal_SSA: theory Minimal_SSA.Irreducible
19:20:19 PAC_Checker: theory PAC_Checker.PAC_Checker
19:20:19 Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
19:20:19 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
19:20:19 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
19:20:19 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
19:20:19 Timing Zeckendorf (8 threads, 2.055s elapsed time, 6.985s cpu time, 0.147s GC time, factor 3.40)
19:20:19 Finished Zeckendorf (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.50)
19:20:20 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Encoding
19:20:20 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Semantics
19:20:20 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Usemantics
19:20:20 Timing VerifyThis2019 (2 threads, 30.903s elapsed time, 37.733s cpu time, 2.652s GC time, factor 1.22)
19:20:20 Finished VerifyThis2019 (0:00:34 elapsed time, 0:00:40 cpu time, factor 1.20)
19:20:21 FOL_Seq_Calc3: theory Abstract_Soundness.Finite_Proof_Soundness
19:20:21 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Prover
19:20:21 FOL_Seq_Calc2: theory Abstract_Soundness.Finite_Proof_Soundness
19:20:21 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Prover
19:20:21 Timing Falling_Factorial_Sum (6 threads, 2.113s elapsed time, 6.873s cpu time, 0.206s GC time, factor 3.25)
19:20:21 Finished Falling_Factorial_Sum (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.38)
19:20:21 Farkas: theory Farkas.Matrix_Farkas
19:20:21 Timing Multiset_Ordering_NPC (2 threads, 44.480s elapsed time, 65.634s cpu time, 3.742s GC time, factor 1.48)
19:20:21 Finished Multiset_Ordering_NPC (0:00:46 elapsed time, 0:01:07 cpu time, factor 1.45)
19:20:21 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
19:20:21 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Completeness
19:20:21 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
19:20:22 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Export
19:20:22 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Soundness
19:20:22 Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom_Poly
19:20:22 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Result
19:20:22 Timing DigitsInBase (2 threads, 5.748s elapsed time, 7.145s cpu time, 0.218s GC time, factor 1.24)
19:20:22 Finished DigitsInBase (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.16)
19:20:23 Transport: theory Transport.Transport_Natural_Functors
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Export
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Hintikka
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.ProverLemmas
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Countermodel
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.EPathHintikka
19:20:23 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Soundness
19:20:24 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Completeness
19:20:24 Timing FOL_Seq_Calc3 (6 threads, 5.006s elapsed time, 17.523s cpu time, 1.124s GC time, factor 3.50)
19:20:24 Finished FOL_Seq_Calc3 (0:00:06 elapsed time, 0:00:18 cpu time, factor 3.08)
19:20:24 Power_Sum_Polynomials: theory Polynomial_Factorization.Gauss_Lemma
19:20:24 Timing Minimal_SSA (6 threads, 5.055s elapsed time, 10.366s cpu time, 0.345s GC time, factor 2.05)
19:20:24 Finished Minimal_SSA (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.79)
19:20:24 SM: theory SM.SM_Wrapup
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc1.Common
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc1.Tableau
19:20:25 Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc1.Sequent
19:20:25 Timing Comparison_Sort_Lower_Bound (2 threads, 8.786s elapsed time, 15.091s cpu time, 1.342s GC time, factor 1.72)
19:20:25 Finished Comparison_Sort_Lower_Bound (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.50)
19:20:25 PAC_Checker: theory PAC_Checker.PAC_Checker_Relation
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Sequent1
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Sequent_Calculus_Verifier
19:20:25 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark
19:20:25 FOL_Seq_Calc2: theory FOL_Seq_Calc2.Results
19:20:26 PAC_Checker: theory PAC_Checker.PAC_Checker_Init
19:20:26 Running Polygonal_Number_Theorem (on 10.195.6.179) ...
19:20:26 Power_Sum_Polynomials: theory Polynomial_Factorization.Rational_Root_Test
19:20:26 Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Puzzle
19:20:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
19:20:27 Timing FOL_Seq_Calc1 (2 threads, 10.240s elapsed time, 15.360s cpu time, 0.409s GC time, factor 1.50)
19:20:27 Running Fisher_Yates (on 10.195.8.49) ...
19:20:27 Finished FOL_Seq_Calc1 (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.41)
19:20:27 Timing Abstract_Soundness (2 threads, 17.394s elapsed time, 27.477s cpu time, 2.440s GC time, factor 1.58)
19:20:27 Finished Abstract_Soundness (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.51)
19:20:28 Running Formula_Derivatives-Examples (on 10.195.8.49) ...
19:20:28 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas
19:20:29 Running Given_Clause_Loops (on 10.195.8.49) ...
19:20:29 Transport: theory Transport.HOL_Algebra_Alignments
19:20:29 Transport: theory Transport.Transport_Functions
19:20:29 Transport: theory Transport.HOL_Alignments
19:20:29 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss
19:20:29 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests
19:20:29 Transport: theory Transport.HOL_Basics
19:20:29 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy
19:20:29 Transport: theory Transport.HOL_Syntax_Bundles_Base
19:20:29 Transport: theory Transport.HOL_Syntax_Bundles
19:20:29 Timing Random_BSTs (8 threads, 2.901s elapsed time, 6.523s cpu time, 0.698s GC time, factor 2.25)
19:20:29 Finished Random_BSTs (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.00)
19:20:30 Polygonal_Number_Theorem: theory Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre
19:20:30 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
19:20:30 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples
19:20:30 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.FirstPrice
19:20:31 Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.Presburger_Examples
19:20:31 Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Alt_Examples
19:20:31 Timing Posix-Lexing (6 threads, 223.166s elapsed time, 539.060s cpu time, 282.263s GC time, factor 2.42)
19:20:31 Finished Posix-Lexing (0:03:44 elapsed time, 0:09:02 cpu time, factor 2.41)
19:20:31 Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Examples
19:20:32 Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Presburger_Examples
19:20:32 Formula_Derivatives-Examples: theory Show.Show
19:20:32 Timing TsirelsonBound (2 threads, 67.630s elapsed time, 103.097s cpu time, 4.772s GC time, factor 1.52)
19:20:32 Finished TsirelsonBound (0:01:10 elapsed time, 0:01:45 cpu time, factor 1.50)
19:20:32 Timing FOL_Seq_Calc2 (6 threads, 13.075s elapsed time, 58.123s cpu time, 5.593s GC time, factor 4.45)
19:20:32 Finished FOL_Seq_Calc2 (0:00:14 elapsed time, 0:00:59 cpu time, factor 4.22)
19:20:33 Given_Clause_Loops: theory Abstract-Rewriting.Seq
19:20:33 Given_Clause_Loops: theory Regular-Sets.Regular_Set
19:20:33 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
19:20:33 ConcurrentIMP: theory ConcurrentIMP.CIMP
19:20:34 Running Hidden_Markov_Models (on 10.195.8.29) ...
19:20:34 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
19:20:34 Running IO_Language_Conformance (on 10.195.8.29) ...
19:20:34 Formula_Derivatives-Examples: theory Show.Show_Instances
19:20:34 Running Interpolation_Polynomials_HOL_Algebra (on 10.195.8.29) ...
19:20:34 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
19:20:34 Given_Clause_Loops: theory Given_Clause_Loops.More_Given_Clause_Architectures
19:20:34 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
19:20:35 PAC_Checker: theory PAC_Checker.PAC_Checker_Synthesis
19:20:35 Timing Fisher_Yates (2 threads, 4.293s elapsed time, 7.547s cpu time, 0.235s GC time, factor 1.76)
19:20:35 Finished Fisher_Yates (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.45)
19:20:36 Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Nameful_Examples
19:20:36 Running Irrational_Series_Erdos_Straus (on 10.195.8.29) ...
19:20:36 IO_Language_Conformance: theory IO_Language_Conformance.Input_Output_Language_Conformance
19:20:37 Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
19:20:37 Timing Farkas (6 threads, 31.152s elapsed time, 115.070s cpu time, 10.268s GC time, factor 3.69)
19:20:38 Finished Farkas (0:00:32 elapsed time, 0:01:57 cpu time, factor 3.59)
19:20:38 Given_Clause_Loops: theory Regular-Sets.Regular_Exp
19:20:38 Running Lifting_the_Exponent (on 10.195.8.30) ...
19:20:38 Running Localization_Ring (on 10.195.8.30) ...
19:20:38 Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
19:20:38 Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
19:20:38 Timing SM (2 threads, 173.097s elapsed time, 290.730s cpu time, 23.482s GC time, factor 1.68)
19:20:38 Finished SM (0:02:57 elapsed time, 0:04:56 cpu time, factor 1.67)
19:20:39 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
19:20:39 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
19:20:39 Hidden_Markov_Models: theory HOL-Library.State_Monad
19:20:39 Running Mason_Stothers (on 10.195.8.40) ...
19:20:39 Running Median_Method (on 10.195.8.40) ...
19:20:39 Running Monad_Normalisation (on 10.195.8.40) ...
19:20:39 Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
19:20:40 Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
19:20:40 Localization_Ring: theory Localization_Ring.Localization
19:20:40 Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
19:20:41 Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
19:20:41 Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark
19:20:41 Mason_Stothers: theory Mason_Stothers.Mason_Stothers
19:20:41 Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
19:20:41 Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
19:20:41 Given_Clause_Loops: theory Regular-Sets.NDerivative
19:20:41 Given_Clause_Loops: theory Regular-Sets.Relation_Interpretation
19:20:41 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
19:20:41 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
19:20:42 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
19:20:42 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
19:20:43 Timing Lifting_the_Exponent (2 threads, 2.452s elapsed time, 4.210s cpu time, 0.124s GC time, factor 1.72)
19:20:43 Finished Lifting_the_Exponent (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.29)
19:20:44 Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
19:20:44 Timing Monad_Normalisation (2 threads, 1.770s elapsed time, 2.428s cpu time, 0.091s GC time, factor 1.37)
19:20:44 Finished Monad_Normalisation (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.07)
19:20:44 Median_Method: theory Median_Method.Median
19:20:45 Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
19:20:45 Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
19:20:45 Timing Mason_Stothers (2 threads, 3.932s elapsed time, 5.924s cpu time, 0.157s GC time, factor 1.51)
19:20:45 Finished Mason_Stothers (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.27)
19:20:46 Timing Stable_Matching (2 threads, 216.275s elapsed time, 294.271s cpu time, 18.568s GC time, factor 1.36)
19:20:46 Finished Stable_Matching (0:03:38 elapsed time, 0:04:56 cpu time, factor 1.36)
19:20:46 Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
19:20:46 Transport: theory Transport.Transport
19:20:46 Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
19:20:46 Transport: theory Transport.Transport_Partial_Quotient_Types
19:20:46 Given_Clause_Loops: theory Regular-Sets.Equivalence_Checking
19:20:46 Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
19:20:47 Timing Constructive_Cryptography (2 threads, 160.067s elapsed time, 260.386s cpu time, 10.246s GC time, factor 1.63)
19:20:47 Finished Constructive_Cryptography (0:03:09 elapsed time, 0:04:58 cpu time, factor 1.57)
19:20:47 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
19:20:47 Transport: theory Transport.Transport_Rel_If
19:20:47 Given_Clause_Loops: theory Regular-Sets.Regexp_Method
19:20:48 Hidden_Markov_Models: theory Monad_Memo_DP.Memory
19:20:48 Given_Clause_Loops: theory Abstract-Rewriting.Abstract_Rewriting
19:20:48 Transport: theory Transport.Transport_Prototype
19:20:49 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
19:20:49 Transport: theory Transport.Transport_Syntax
19:20:49 Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
19:20:50 Transport: theory Transport.Transport_Dep_Fun_Rel_Examples
19:20:50 Transport: theory Transport.Transport_Lists_Sets_Examples
19:20:50 Given_Clause_Loops: theory Weighted_Path_Order.Relations
19:20:50 Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
19:20:50 Given_Clause_Loops: theory Weighted_Path_Order.Multiset_Extension_Pair
19:20:51 Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops_Util
19:20:52 Timing Median_Method (2 threads, 10.026s elapsed time, 15.854s cpu time, 0.585s GC time, factor 1.58)
19:20:52 Finished Median_Method (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.44)
19:20:52 Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
19:20:52 Transport: theory Transport.Transport_Typedef
19:20:52 Given_Clause_Loops: theory Given_Clause_Loops.Prover_Queue
19:20:52 Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
19:20:53 Running Monomorphic_Monad (on 10.195.8.32) ...
19:20:53 Given_Clause_Loops: theory Given_Clause_Loops.Prover_Lazy_List_Queue
19:20:53 Given_Clause_Loops: theory Given_Clause_Loops.DISCOUNT_Loop
19:20:53 Transport: theory Transport.Transport_Via_Partial_Galois_Connections_Equivalences_Paper
19:20:53 Running Password_Authentication_Protocol (on of3.proof.cit.tum.de) ...
19:20:53 Running Prefix_Free_Code_Combinators (on of3.proof.cit.tum.de) ...
19:20:53 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator
19:20:54 Given_Clause_Loops: theory Given_Clause_Loops.Otter_Loop
19:20:54 Timing ConcurrentIMP (2 threads, 37.297s elapsed time, 63.271s cpu time, 6.143s GC time, factor 1.70)
19:20:54 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype
19:20:54 Finished ConcurrentIMP (0:00:39 elapsed time, 0:01:06 cpu time, factor 1.66)
19:20:54 Running Randomised_BSTs (on of2.proof.cit.tum.de) ...
19:20:54 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
19:20:54 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
19:20:54 Running SDS_Impossibility (on of2.proof.cit.tum.de) ...
19:20:54 Password_Authentication_Protocol: theory Password_Authentication_Protocol.Propaedeutics
19:20:54 Running Selection_Heap_Sort (on of2.proof.cit.tum.de) ...
19:20:55 Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
19:20:55 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
19:20:55 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
19:20:55 Running Skip_Lists (on 10.195.8.46) ...
19:20:55 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Examples
19:20:56 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
19:20:56 Given_Clause_Loops: theory Given_Clause_Loops.Fair_DISCOUNT_Loop
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
19:20:56 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
19:20:57 Timing Prefix_Free_Code_Combinators (6 threads, 1.994s elapsed time, 4.285s cpu time, 0.134s GC time, factor 2.15)
19:20:57 Finished Prefix_Free_Code_Combinators (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.64)
19:20:57 Password_Authentication_Protocol: theory Password_Authentication_Protocol.Protocol
19:20:58 Given_Clause_Loops: theory Given_Clause_Loops.Zipperposition_Loop
19:20:58 Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
19:20:58 Skip_Lists: theory Skip_Lists.Pi_pmf
19:20:58 Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
19:20:59 Running Source_Coding_Theorem (on 10.195.8.11) ...
19:20:59 Skip_Lists: theory Skip_Lists.Misc
19:20:59 Skip_Lists: theory Skip_Lists.Geometric_PMF
19:20:59 Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop
19:20:59 Timing Selection_Heap_Sort (6 threads, 3.412s elapsed time, 12.112s cpu time, 0.595s GC time, factor 3.55)
19:20:59 Finished Selection_Heap_Sort (0:00:04 elapsed time, 0:00:13 cpu time, factor 2.88)
19:20:59 Skip_Lists: theory Skip_Lists.Skip_List
19:21:00 Timing IO_Language_Conformance (2 threads, 23.428s elapsed time, 42.047s cpu time, 2.364s GC time, factor 1.79)
19:21:00 Finished IO_Language_Conformance (0:00:26 elapsed time, 0:00:44 cpu time, factor 1.71)
19:21:00 Timing Randomised_BSTs (6 threads, 4.840s elapsed time, 14.021s cpu time, 0.466s GC time, factor 2.90)
19:21:00 Finished Randomised_BSTs (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.47)
19:21:01 Running Surprise_Paradox (on 10.195.7.194) ...
19:21:01 Running Twelvefold_Way (on 10.195.7.194) ...
19:21:01 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
19:21:01 PAC_Checker: theory PAC_Checker.PAC_Checker_MLton
19:21:03 Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Def
19:21:03 Twelvefold_Way: theory HOL-Eisbach.Eisbach
19:21:03 Twelvefold_Way: theory HOL-Combinatorics.Stirling
19:21:03 Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
19:21:03 Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts
19:21:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
19:21:03 Estimated completion: 29-Nov-2023 20:58:55 +0100 (took 0.440s)
19:21:04 Timing Vickrey_Clarke_Groves (2 threads, 123.798s elapsed time, 203.067s cpu time, 10.505s GC time, factor 1.64)
19:21:04 Finished Vickrey_Clarke_Groves (0:02:06 elapsed time, 0:03:25 cpu time, factor 1.63)
19:21:04 Twelvefold_Way: theory HOL-Combinatorics.Transposition
19:21:04 Twelvefold_Way: theory Card_Multisets.Card_Multisets
19:21:04 Twelvefold_Way: theory Card_Number_Partitions.Additions_to_Main
19:21:04 Twelvefold_Way: theory Card_Partitions.Injectivity_Solver
19:21:04 Twelvefold_Way: theory Card_Number_Partitions.Number_Partition
19:21:04 Twelvefold_Way: theory Card_Number_Partitions.Card_Number_Partitions
19:21:04 Twelvefold_Way: theory Card_Partitions.Set_Partition
19:21:04 Twelvefold_Way: theory HOL-Combinatorics.Permutations
19:21:05 Twelvefold_Way: theory Card_Partitions.Card_Partitions
19:21:05 Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
19:21:05 Twelvefold_Way: theory Bell_Numbers_Spivey.Bell_Numbers
19:21:06 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples
19:21:06 Twelvefold_Way: theory HOL-ex.Birthday_Paradox
19:21:06 Twelvefold_Way: theory Twelvefold_Way.Preliminaries
19:21:06 Timing Surprise_Paradox (2 threads, 3.263s elapsed time, 3.760s cpu time, 0.162s GC time, factor 1.15)
19:21:06 Finished Surprise_Paradox (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.04)
19:21:07 Timing Formula_Derivatives-Examples (2 threads, 35.297s elapsed time, 66.423s cpu time, 16.176s GC time, factor 1.88)
19:21:07 Finished Formula_Derivatives-Examples (0:00:37 elapsed time, 0:01:08 cpu time, factor 1.83)
19:21:07 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
19:21:07 Timing Interpolation_Polynomials_HOL_Algebra (2 threads, 28.175s elapsed time, 48.413s cpu time, 5.825s GC time, factor 1.72)
19:21:07 Finished Interpolation_Polynomials_HOL_Algebra (0:00:31 elapsed time, 0:00:51 cpu time, factor 1.65)
19:21:07 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Core
19:21:07 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry1
19:21:07 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry2
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Equiv_Relations_on_Functions
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Card_Bijections_Direct
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry10
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry11
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry4
19:21:08 Timing Source_Coding_Theorem (2 threads, 6.052s elapsed time, 9.316s cpu time, 0.253s GC time, factor 1.54)
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry5
19:21:08 Finished Source_Coding_Theorem (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.34)
19:21:08 Given_Clause_Loops: theory Given_Clause_Loops.iProver_Loop
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry6
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry7
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry8
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry9
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry12
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry3
19:21:08 Twelvefold_Way: theory Twelvefold_Way.Card_Bijections
19:21:09 Timing SDS_Impossibility (6 threads, 12.721s elapsed time, 36.481s cpu time, 2.564s GC time, factor 2.87)
19:21:09 Finished SDS_Impossibility (0:00:14 elapsed time, 0:00:37 cpu time, factor 2.69)
19:21:09 Given_Clause_Loops: theory Given_Clause_Loops.Fair_iProver_Loop
19:21:09 Timing PAC_Checker (6 threads, 112.710s elapsed time, 548.339s cpu time, 140.193s GC time, factor 4.87)
19:21:09 Finished PAC_Checker (0:01:54 elapsed time, 0:09:13 cpu time, factor 4.82)
19:21:09 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way
19:21:10 Timing VerifyThis2018 (2 threads, 86.447s elapsed time, 132.429s cpu time, 4.735s GC time, factor 1.53)
19:21:10 Finished VerifyThis2018 (0:01:29 elapsed time, 0:02:15 cpu time, factor 1.51)
19:21:11 Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Complete
19:21:13 Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops
19:21:14 Timing Irrational_Series_Erdos_Straus (2 threads, 34.542s elapsed time, 55.310s cpu time, 1.567s GC time, factor 1.60)
19:21:14 Finished Irrational_Series_Erdos_Straus (0:00:37 elapsed time, 0:00:58 cpu time, factor 1.54)
19:21:15 Timing Password_Authentication_Protocol (6 threads, 20.053s elapsed time, 70.530s cpu time, 3.423s GC time, factor 3.52)
19:21:15 Finished Password_Authentication_Protocol (0:00:21 elapsed time, 0:01:11 cpu time, factor 3.36)
19:21:15 Timing Skip_Lists (2 threads, 16.526s elapsed time, 29.659s cpu time, 0.971s GC time, factor 1.79)
19:21:15 Finished Skip_Lists (0:00:19 elapsed time, 0:00:32 cpu time, factor 1.66)
19:21:18 Timing Power_Sum_Polynomials (2 threads, 64.149s elapsed time, 104.103s cpu time, 7.525s GC time, factor 1.62)
19:21:18 Finished Power_Sum_Polynomials (0:01:06 elapsed time, 0:01:46 cpu time, factor 1.60)
19:21:18 Timing Stateful_Protocol_Composition_and_Typing (2 threads, 698.923s elapsed time, 1172.055s cpu time, 158.779s GC time, factor 1.68)
19:21:18 Finished Stateful_Protocol_Composition_and_Typing (0:12:33 elapsed time, 0:20:46 cpu time, factor 1.65)
19:21:18 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
19:21:20 Timing Crypto_Standards (6 threads, 641.297s elapsed time, 3134.884s cpu time, 747.187s GC time, factor 4.89)
19:21:20 Finished Crypto_Standards (0:10:44 elapsed time, 0:52:23 cpu time, factor 4.88)
19:21:22 Timing Localization_Ring (2 threads, 41.240s elapsed time, 54.311s cpu time, 3.668s GC time, factor 1.32)
19:21:22 Finished Localization_Ring (0:00:43 elapsed time, 0:00:56 cpu time, factor 1.29)
19:21:22 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
19:21:22 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
19:21:22 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
19:21:23 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
19:21:23 Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
19:21:23 Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
19:21:23 Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
19:21:24 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
19:21:24 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
19:21:27 Running Constructive_Cryptography_CM (on of3.proof.cit.tum.de) ...
19:21:28 Timing CAVA_LTL_Modelchecker (6 threads, 181.395s elapsed time, 270.388s cpu time, 66.562s GC time, factor 1.49)
19:21:28 Finished CAVA_LTL_Modelchecker (0:03:03 elapsed time, 0:04:33 cpu time, factor 1.49)
19:21:28 Timing Hidden_Markov_Models (2 threads, 49.973s elapsed time, 93.389s cpu time, 10.728s GC time, factor 1.87)
19:21:28 Finished Hidden_Markov_Models (0:00:54 elapsed time, 0:01:38 cpu time, factor 1.81)
19:21:28 Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
19:21:28 Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
19:21:28 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
19:21:30 Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
19:21:31 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
19:21:31 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
19:21:31 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
19:21:31 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
19:21:32 Timing Transport (2 threads, 174.820s elapsed time, 323.822s cpu time, 30.035s GC time, factor 1.85)
19:21:32 Finished Transport (0:02:57 elapsed time, 0:05:26 cpu time, factor 1.84)
19:21:33 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
19:21:35 Timing Monomorphic_Monad (2 threads, 39.273s elapsed time, 71.688s cpu time, 6.370s GC time, factor 1.83)
19:21:35 Finished Monomorphic_Monad (0:00:42 elapsed time, 0:01:15 cpu time, factor 1.77)
19:21:40 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
19:21:40 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
19:21:40 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
19:21:41 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
19:21:41 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
19:21:45 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
19:21:45 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
19:21:46 Timing VYDRA_MDL (2 threads, 164.813s elapsed time, 303.299s cpu time, 20.020s GC time, factor 1.84)
19:21:46 Finished VYDRA_MDL (0:02:49 elapsed time, 0:05:09 cpu time, factor 1.83)
19:21:51 Timing Polygonal_Number_Theorem (2 threads, 82.559s elapsed time, 133.563s cpu time, 6.039s GC time, factor 1.62)
19:21:51 Finished Polygonal_Number_Theorem (0:01:25 elapsed time, 0:02:16 cpu time, factor 1.60)
19:21:53 Running Automated_Stateful_Protocol_Verification (on 10.195.8.30) ...
19:21:54 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
19:21:55 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
19:21:55 Timing Given_Clause_Loops (2 threads, 83.254s elapsed time, 145.920s cpu time, 12.080s GC time, factor 1.75)
19:21:55 Finished Given_Clause_Loops (0:01:26 elapsed time, 0:02:29 cpu time, factor 1.74)
19:21:56 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
19:21:56 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
19:21:56 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
19:21:57 Flow_Networks: theory Flow_Networks.Network
19:21:57 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
19:21:58 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
19:21:58 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
19:21:58 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
19:21:58 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
19:21:59 Flow_Networks: theory Flow_Networks.Residual_Graph
19:21:59 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
19:22:00 Timing Refine_Imperative_HOL (2 threads, 307.295s elapsed time, 459.564s cpu time, 48.175s GC time, factor 1.50)
19:22:00 Finished Refine_Imperative_HOL (0:05:49 elapsed time, 0:08:37 cpu time, factor 1.48)
19:22:00 Flow_Networks: theory Flow_Networks.Augmenting_Flow
19:22:00 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
19:22:00 Flow_Networks: theory Flow_Networks.Augmenting_Path
19:22:01 Flow_Networks: theory Flow_Networks.Ford_Fulkerson
19:22:02 Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
19:22:02 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
19:22:03 Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
19:22:05 Flow_Networks: theory Flow_Networks.Network_Impl
19:22:05 Flow_Networks: theory Flow_Networks.Graph_Impl
19:22:05 Flow_Networks: theory Flow_Networks.NetCheck
19:22:06 Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
19:22:08 Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
19:22:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
19:22:15 Timing FSM_Tests (2 threads, 1008.627s elapsed time, 1774.706s cpu time, 459.780s GC time, factor 1.76)
19:22:15 Finished FSM_Tests (0:16:55 elapsed time, 0:29:47 cpu time, factor 1.76)
19:22:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
19:22:16 Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
19:22:20 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
19:22:21 Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
19:22:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
19:22:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
19:22:26 Timing Probabilistic_Timed_Automata (2 threads, 283.804s elapsed time, 487.774s cpu time, 28.603s GC time, factor 1.72)
19:22:26 Finished Probabilistic_Timed_Automata (0:04:48 elapsed time, 0:08:13 cpu time, factor 1.71)
19:22:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
19:22:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
19:22:36 Timing FO_Theory_Rewriting (2 threads, 1033.760s elapsed time, 1768.118s cpu time, 575.956s GC time, factor 1.71)
19:22:36 Finished FO_Theory_Rewriting (0:17:19 elapsed time, 0:29:37 cpu time, factor 1.71)
19:22:38 Running BTree (on 10.195.8.32) ...
19:22:38 Running Floyd_Warshall (on 10.195.8.32) ...
19:22:41 Floyd_Warshall: theory Floyd_Warshall.Floyd_Warshall
19:22:41 Floyd_Warshall: theory Floyd_Warshall.Recursion_Combinators
19:22:41 BTree: theory HOL-Data_Structures.Cmp
19:22:41 BTree: theory HOL-Data_Structures.Less_False
19:22:41 BTree: theory HOL-Data_Structures.Sorted_Less
19:22:41 BTree: theory HOL-Data_Structures.List_Ins_Del
19:22:42 BTree: theory BTree.BTree
19:22:42 BTree: theory HOL-Data_Structures.Set_Specs
19:22:42 BTree: theory BTree.BPlusTree
19:22:43 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
19:22:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
19:22:44 BTree: theory BTree.BTree_Height
19:22:45 Timing Jordan_Normal_Form (2 threads, 712.901s elapsed time, 1201.697s cpu time, 216.763s GC time, factor 1.69)
19:22:45 Finished Jordan_Normal_Form (0:12:52 elapsed time, 0:21:22 cpu time, factor 1.66)
19:22:45 BTree: theory BTree.BTree_Set
19:22:47 Floyd_Warshall: theory Floyd_Warshall.FW_Code
19:22:48 BTree: theory BTree.BPlusTree_Split
19:22:48 Estimated completion: 29-Nov-2023 21:56:22 +0100 (took 0.162s)
19:22:49 BTree: theory BTree.BPlusTree_Set
19:22:53 BTree: theory BTree.BTree_Split
19:22:57 WebAssembly: theory Native_Word.Code_Target_Int_Bit
19:22:57 WebAssembly: theory WebAssembly.Wasm_Checker_Printing
19:22:57 WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing
19:22:57 WebAssembly: theory WebAssembly.Wasm_Type_Abs_Printing
19:22:57 WebAssembly: theory WebAssembly.Wasm_Printing
19:22:57 WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing_Pure
19:22:58 BTree: theory HOL-Library.Sublist
19:23:01 BTree: theory BTree.BPlusTree_Range
19:23:02 Running Perron_Frobenius (on 10.195.8.40) ...
19:23:02 Running Linear_Programming (on 10.195.8.40) ...
19:23:02 Running Isabelle_Marries_Dirac (on 10.195.8.40) ...
19:23:02 Running QHLProver (on 10.195.8.40) ...
19:23:03 BTree: theory BTree.BPlusTree_SplitCE
19:23:05 Linear_Programming: theory Simplex.Simplex_Auxiliary
19:23:05 QHLProver: theory Deep_Learning.Tensor
19:23:05 QHLProver: theory QHLProver.Complex_Matrix
19:23:05 Linear_Programming: theory Simplex.Simplex_Algebra
19:23:05 Linear_Programming: theory Simplex.Rel_Chain
19:23:05 Linear_Programming: theory Linear_Programming.More_Jordan_Normal_Forms
19:23:06 QHLProver: theory Deep_Learning.Tensor_Subtensor
19:23:06 Timing WebAssembly (2 threads, 243.655s elapsed time, 440.837s cpu time, 83.134s GC time, factor 1.81)
19:23:06 Isabelle_Marries_Dirac: theory Matrix.Utility
19:23:06 Finished WebAssembly (0:04:07 elapsed time, 0:07:26 cpu time, factor 1.80)
19:23:06 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Basics
19:23:06 QHLProver: theory Deep_Learning.Tensor_Plus
19:23:07 QHLProver: theory Deep_Learning.Tensor_Matricization
19:23:07 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Binary_Nat
19:23:07 Isabelle_Marries_Dirac: theory Matrix.Matrix_Legacy
19:23:07 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum
19:23:08 Building Subresultants (on of3.proof.cit.tum.de) ...
19:23:09 Subresultants: theory Subresultants.Dichotomous_Lazard
19:23:09 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
19:23:09 Subresultants: theory Subresultants.More_Homomorphisms
19:23:09 Subresultants: theory Subresultants.Coeff_Int
19:23:09 Subresultants: theory Subresultants.Resultant_Prelim
19:23:09 Subresultants: theory Subresultants.Binary_Exponentiation
19:23:09 Perron_Frobenius: theory HOL-Eisbach.Eisbach
19:23:09 Perron_Frobenius: theory Pure-ex.Guess
19:23:09 Subresultants: theory Subresultants.Subresultant
19:23:09 Linear_Programming: theory Simplex.Abstract_Linear_Poly
19:23:09 Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets
19:23:09 Isabelle_Marries_Dirac: theory Matrix_Tensor.Matrix_Tensor
19:23:09 Timing Floyd_Warshall (2 threads, 28.337s elapsed time, 46.305s cpu time, 1.519s GC time, factor 1.63)
19:23:10 Finished Floyd_Warshall (0:00:31 elapsed time, 0:00:49 cpu time, factor 1.56)
19:23:10 Perron_Frobenius: theory HOL-Analysis.Metric_Arith
19:23:10 Linear_Programming: theory Simplex.Linear_Poly_Maps
19:23:11 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology
19:23:11 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Complex_Vectors
19:23:11 Linear_Programming: theory Simplex.QDelta
19:23:11 QHLProver: theory QHLProver.Gates
19:23:11 QHLProver: theory QHLProver.Matrix_Limit
19:23:11 Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable
19:23:11 Perron_Frobenius: theory HOL-Analysis.Inner_Product
19:23:11 Subresultants: theory Subresultants.Subresultant_Gcd
19:23:12 Linear_Programming: theory Simplex.Simplex
19:23:12 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Measurement
19:23:13 QHLProver: theory QHLProver.Quantum_Program
19:23:14 Perron_Frobenius: theory HOL-Analysis.L2_Norm
19:23:14 Perron_Frobenius: theory HOL-Analysis.Operator_Norm
19:23:14 Perron_Frobenius: theory HOL-Analysis.Product_Vector
19:23:14 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Tensor
19:23:14 Perron_Frobenius: theory HOL-Analysis.Abstract_Limits
19:23:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
19:23:15 Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Irreducibility
19:23:15 Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial
19:23:15 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.More_Tensor
19:23:15 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.No_Cloning
19:23:16 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch
19:23:16 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Entanglement
19:23:16 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma
19:23:16 QHLProver: theory QHLProver.Partial_State
19:23:16 QHLProver: theory QHLProver.Quantum_Hoare
19:23:16 Perron_Frobenius: theory Sturm_Sequences.Sturm_Library
19:23:16 Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem
19:23:16 Perron_Frobenius: theory HOL-Analysis.Elementary_Topology
19:23:17 Perron_Frobenius: theory HOL-Analysis.Euclidean_Space
19:23:17 Estimated completion: 29-Nov-2023 20:58:55 +0100 (took 0.157s)
19:23:18 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch_Jozsa
19:23:19 QHLProver: theory QHLProver.Grover
19:23:20 Perron_Frobenius: theory Sturm_Sequences.Sturm_Method
19:23:20 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Teleportation
19:23:20 Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2
19:23:21 Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product
19:23:22 Timing Flow_Networks (2 threads, 207.871s elapsed time, 344.848s cpu time, 28.449s GC time, factor 1.66)
19:23:22 Finished Flow_Networks (0:04:05 elapsed time, 0:06:33 cpu time, factor 1.60)
19:23:22 Timing Twelvefold_Way (2 threads, 138.290s elapsed time, 186.747s cpu time, 10.061s GC time, factor 1.35)
19:23:22 Finished Twelvefold_Way (0:02:20 elapsed time, 0:03:09 cpu time, factor 1.35)
19:23:22 Perron_Frobenius: theory HOL-Analysis.Linear_Algebra
19:23:24 Perron_Frobenius: theory HOL-Analysis.Connected
19:23:25 Perron_Frobenius: theory HOL-Analysis.Function_Topology
19:23:25 Perron_Frobenius: theory HOL-Analysis.Affine
19:23:26 Perron_Frobenius: theory HOL-Analysis.Convex
19:23:26 Perron_Frobenius: theory HOL-Analysis.Cartesian_Space
19:23:28 Perron_Frobenius: theory HOL-Analysis.Product_Topology
19:23:28 Perron_Frobenius: theory HOL-Analysis.Determinants
19:23:29 Perron_Frobenius: theory HOL-Analysis.T1_Spaces
19:23:29 Running EdmondsKarp_Maxflow (on 10.195.8.30) ...
19:23:29 Running Prpu_Maxflow (on 10.195.8.30) ...
19:23:29 Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces
19:23:30 Perron_Frobenius: theory HOL-Analysis.Infinite_Sum
19:23:32 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
19:23:32 Prpu_Maxflow: theory Prpu_Maxflow.Generic_Push_Relabel
19:23:32 Prpu_Maxflow: theory Prpu_Maxflow.Graph_Topological_Ordering
19:23:32 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.FordFulkerson_Algo
19:23:34 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
19:23:34 Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces
19:23:34 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
19:23:35 Perron_Frobenius: theory HOL-Analysis.Norm_Arith
19:23:35 Perron_Frobenius: theory Matrix.Utility
19:23:36 Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization
19:23:36 Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space
19:23:36 Timing Subresultants (6 threads, 17.296s elapsed time, 61.675s cpu time, 4.134s GC time, factor 3.57)
19:23:36 Finished Subresultants (0:00:27 elapsed time, 0:01:18 cpu time, factor 2.90)
19:23:37 Linear_Programming: theory Farkas.Farkas
19:23:37 Linear_Programming: theory Simplex.Simplex_Incremental
19:23:38 Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order
19:23:39 Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space
19:23:39 Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits
19:23:39 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Algo
19:23:41 Perron_Frobenius: theory HOL-Analysis.Line_Segment
19:23:41 Perron_Frobenius: theory HOL-Analysis.Summation_Tests
19:23:41 Linear_Programming: theory Farkas.Matrix_Farkas
19:23:42 Perron_Frobenius: theory HOL-Analysis.Starlike
19:23:42 Perron_Frobenius: theory HOL-Analysis.Uniform_Limit
19:23:42 Timing Constructive_Cryptography_CM (6 threads, 131.695s elapsed time, 486.241s cpu time, 78.738s GC time, factor 3.69)
19:23:42 Finished Constructive_Cryptography_CM (0:02:13 elapsed time, 0:08:10 cpu time, factor 3.66)
19:23:43 Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function
19:23:44 Perron_Frobenius: theory HOL-Analysis.Path_Connected
19:23:45 Perron_Frobenius: theory HOL-Analysis.Derivative
19:23:46 Linear_Programming: theory Farkas.Simplex_for_Reals
19:23:46 Perron_Frobenius: theory HOL-Analysis.Uncountable_Sets
19:23:46 Perron_Frobenius: theory HOL-Analysis.Homotopy
19:23:46 Linear_Programming: theory Linear_Programming.Matrix_LinPoly
19:23:47 Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel
19:23:47 Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Inst
19:23:48 Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space
19:23:48 Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type
19:23:48 Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Impl
19:23:49 Perron_Frobenius: theory HOL-Analysis.Homeomorphism
19:23:49 Building Berlekamp_Zassenhaus (on 10.195.8.49) ...
19:23:49 Linear_Programming: theory Linear_Programming.LP_Preliminaries
19:23:49 Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint
19:23:50 Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front
19:23:50 Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous
19:23:52 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
19:23:52 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
19:23:52 Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
19:23:54 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
19:23:54 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
19:23:55 Linear_Programming: theory Linear_Programming.Linear_Programming
19:23:55 Timing Multi_Party_Computation (2 threads, 267.705s elapsed time, 490.200s cpu time, 40.543s GC time, factor 1.83)
19:23:55 Finished Multi_Party_Computation (0:04:31 elapsed time, 0:08:15 cpu time, factor 1.82)
19:23:57 Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
19:23:57 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
19:23:57 Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
19:23:58 Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
19:23:58 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
19:23:58 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
19:23:59 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
19:23:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
19:23:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
19:23:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
19:24:00 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
19:24:00 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
19:24:00 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
19:24:01 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
19:24:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
19:24:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
19:24:05 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
19:24:06 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
19:24:07 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
19:24:07 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
19:24:08 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
19:24:08 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
19:24:09 Berlekamp_Zassenhaus: theory Matrix.Utility
19:24:10 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
19:24:10 Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
19:24:10 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Checked_Impl
19:24:10 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
19:24:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
19:24:12 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
19:24:12 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
19:24:13 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
19:24:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
19:24:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
19:24:14 Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
19:24:14 Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front_Impl
19:24:15 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
19:24:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
19:24:21 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
19:24:21 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
19:24:22 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
19:24:25 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
19:24:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
19:24:29 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
19:24:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
19:24:32 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
19:24:34 Berlekamp_Zassenhaus: theory Show.Show_Poly
19:24:34 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
19:24:35 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
19:24:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
19:24:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
19:24:39 Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
19:24:39 Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
19:24:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
19:24:40 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Benchmark_Export
19:24:40 Berlekamp_Zassenhaus: theory Word_Lib.More_Word
19:24:42 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
19:24:42 Timing QHLProver (2 threads, 94.809s elapsed time, 163.536s cpu time, 6.104s GC time, factor 1.72)
19:24:42 Finished QHLProver (0:01:38 elapsed time, 0:02:47 cpu time, factor 1.70)
19:24:42 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
19:24:44 Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
19:24:45 Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
19:24:45 Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
19:24:45 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
19:24:46 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
19:24:48 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
19:24:48 Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
19:24:52 Timing EdmondsKarp_Maxflow (2 threads, 78.619s elapsed time, 98.207s cpu time, 8.558s GC time, factor 1.25)
19:24:52 Finished EdmondsKarp_Maxflow (0:01:22 elapsed time, 0:01:41 cpu time, factor 1.23)
19:24:56 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
19:24:57 Berlekamp_Zassenhaus: theory Native_Word.Uint32
19:24:59 Berlekamp_Zassenhaus: theory Native_Word.Uint64
19:25:01 Timing JinjaDCI (2 threads, 1179.734s elapsed time, 1844.684s cpu time, 272.142s GC time, factor 1.56)
19:25:01 Finished JinjaDCI (0:19:45 elapsed time, 0:30:54 cpu time, factor 1.56)
19:25:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
19:25:05 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
19:25:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
19:25:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
19:25:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
19:25:14 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
19:25:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
19:25:15 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
19:25:18 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
19:25:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
19:25:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
19:25:21 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
19:25:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
19:25:22 Timing Universal_Hash_Families (2 threads, 379.583s elapsed time, 695.479s cpu time, 241.103s GC time, factor 1.83)
19:25:22 Finished Universal_Hash_Families (0:06:24 elapsed time, 0:11:42 cpu time, factor 1.83)
19:25:24 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
19:25:25 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
19:25:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
19:25:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
19:25:51 Prpu_Maxflow: theory Prpu_Maxflow.Generated_Code_Test
19:26:11 Timing Prpu_Maxflow (2 threads, 157.778s elapsed time, 246.769s cpu time, 12.238s GC time, factor 1.56)
19:26:11 Finished Prpu_Maxflow (0:02:41 elapsed time, 0:04:10 cpu time, factor 1.55)
19:26:59 Timing Linear_Programming (2 threads, 231.677s elapsed time, 383.898s cpu time, 26.504s GC time, factor 1.66)
19:26:59 Finished Linear_Programming (0:03:56 elapsed time, 0:06:29 cpu time, factor 1.65)
19:27:07 Timing HRB-Slicing (2 threads, 627.801s elapsed time, 1094.859s cpu time, 159.778s GC time, factor 1.74)
19:27:07 Finished HRB-Slicing (0:11:47 elapsed time, 0:20:02 cpu time, factor 1.70)
19:27:14 Running InformationFlowSlicing_Inter (on of3.proof.cit.tum.de) ...
19:27:15 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
19:27:17 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
19:27:21 Timing InformationFlowSlicing_Inter (6 threads, 5.382s elapsed time, 18.739s cpu time, 2.450s GC time, factor 3.48)
19:27:21 Finished InformationFlowSlicing_Inter (0:00:06 elapsed time, 0:00:20 cpu time, factor 2.92)
19:27:22 Timing Isabelle_Marries_Dirac (2 threads, 254.524s elapsed time, 428.494s cpu time, 21.211s GC time, factor 1.68)
19:27:22 Finished Isabelle_Marries_Dirac (0:04:19 elapsed time, 0:07:13 cpu time, factor 1.67)
19:27:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
19:28:01 Timing Slicing (2 threads, 704.669s elapsed time, 1251.862s cpu time, 133.341s GC time, factor 1.78)
19:28:01 Finished Slicing (0:12:43 elapsed time, 0:22:13 cpu time, factor 1.75)
19:28:01 Running InformationFlowSlicing (on 10.195.8.11) ...
19:28:04 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
19:28:05 InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
19:28:06 Timing CZH_Elementary_Categories (2 threads, 1726.445s elapsed time, 2987.857s cpu time, 1244.670s GC time, factor 1.73)
19:28:06 Finished CZH_Elementary_Categories (0:29:10 elapsed time, 0:50:16 cpu time, factor 1.72)
19:28:07 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
19:28:17 Timing Cook_Levin (2 threads, 1730.909s elapsed time, 2748.232s cpu time, 199.978s GC time, factor 1.59)
19:28:17 Finished Cook_Levin (0:28:57 elapsed time, 0:45:59 cpu time, factor 1.59)
19:28:18 Timing InformationFlowSlicing (2 threads, 12.612s elapsed time, 23.843s cpu time, 2.111s GC time, factor 1.89)
19:28:18 Finished InformationFlowSlicing (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.72)
19:28:23 Running CZH_Universal_Constructions (on 10.195.7.194) ...
19:28:25 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
19:28:25 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
19:28:25 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
19:28:25 Estimated completion: 29-Nov-2023 20:36:15 +0100 (took 0.109s)
19:28:42 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
19:29:08 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
19:29:09 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
19:29:39 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
19:29:40 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
19:29:40 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
19:29:59 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
19:30:02 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
19:30:13 Skipping theories "Array_SBlit", "Partially_Filled_Array", "BTree_Imp", "BTree_ImpSet", "BTree_ImpSplit", "Flatten_Iter_Spec", "Flatten_Iter", "BPlusTree_Imp", "BPlusTree_ImpSplit", "BPlusTree_ImpSet", "BPlusTree_Iter_OneWay", "BPlusTree_Iter", "BPlusTree_ImpRange", "BPlusTree_ImpSplitCE" (undefined ISABELLE_OCAMLFIND)
19:30:13 Timing BTree (2 threads, 450.438s elapsed time, 590.378s cpu time, 14.495s GC time, factor 1.31)
19:30:13 Finished BTree (0:07:34 elapsed time, 0:09:55 cpu time, factor 1.31)
19:31:07 Timing Berlekamp_Zassenhaus (2 threads, 391.636s elapsed time, 706.217s cpu time, 152.132s GC time, factor 1.80)
19:31:07 Finished Berlekamp_Zassenhaus (0:07:14 elapsed time, 0:12:46 cpu time, factor 1.76)
19:31:08 Building Algebraic_Numbers (on 10.195.8.49) ...
19:31:08 Building LLL_Basis_Reduction (on 10.195.8.49) ...
19:31:08 Running Linear_Recurrences_Solver (on 10.195.8.49) ...
19:31:08 Running CRYSTALS-Kyber (on 10.195.8.49) ...
19:31:08 Running CVP_Hardness (on 10.195.8.49) ...
19:31:11 CVP_Hardness: theory CVP_Hardness.Reduction
19:31:11 CVP_Hardness: theory CVP_Hardness.Digits_int
19:31:11 CVP_Hardness: theory CVP_Hardness.Partition
19:31:11 CRYSTALS-Kyber: theory HOL-Number_Theory.Eratosthenes
19:31:11 CVP_Hardness: theory CVP_Hardness.Subset_Sum
19:31:11 CRYSTALS-Kyber: theory HOL-Number_Theory.Mod_Exp
19:31:12 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
19:31:12 CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
19:31:12 CRYSTALS-Kyber: theory HOL-Analysis.Inner_Product
19:31:12 CRYSTALS-Kyber: theory HOL-Analysis.L2_Norm
19:31:12 CRYSTALS-Kyber: theory HOL-Analysis.Product_Vector
19:31:12 CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
19:31:13 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
19:31:14 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
19:31:14 CRYSTALS-Kyber: theory HOL-Number_Theory.Fib
19:31:14 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
19:31:14 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
19:31:14 CRYSTALS-Kyber: theory HOL-Number_Theory.Prime_Powers
19:31:14 CVP_Hardness: theory Algebraic_Numbers.Resultant
19:31:14 CRYSTALS-Kyber: theory HOL-Analysis.Euclidean_Space
19:31:15 CRYSTALS-Kyber: theory HOL-Number_Theory.Euler_Criterion
19:31:15 CRYSTALS-Kyber: theory HOL-Number_Theory.Gauss
19:31:16 CRYSTALS-Kyber: theory HOL-Number_Theory.Quadratic_Reciprocity
19:31:16 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
19:31:16 CVP_Hardness: theory CVP_Hardness.Lattice_int
19:31:17 CRYSTALS-Kyber: theory HOL-Number_Theory.Pocklington
19:31:17 CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
19:31:18 CVP_Hardness: theory CVP_Hardness.CVP_p
19:31:18 CRYSTALS-Kyber: theory HOL-Number_Theory.Residue_Primitive_Roots
19:31:18 CRYSTALS-Kyber: theory HOL-Analysis.Finite_Cartesian_Product
19:31:18 CRYSTALS-Kyber: theory HOL-Number_Theory.Number_Theory
19:31:18 Algebraic_Numbers: theory Pure-ex.Guess
19:31:18 Algebraic_Numbers: theory Deriving.Compare_Rat
19:31:19 Linear_Recurrences_Solver: theory Pure-ex.Guess
19:31:19 Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
19:31:19 Algebraic_Numbers: theory Deriving.Compare_Real
19:31:19 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
19:31:19 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
19:31:19 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
19:31:19 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
19:31:19 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
19:31:19 Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
19:31:20 Linear_Recurrences_Solver: theory Deriving.Compare_Real
19:31:20 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
19:31:20 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
19:31:20 Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
19:31:20 Linear_Recurrences_Solver: theory Polynomials.More_Modules
19:31:20 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_spec
19:31:21 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
19:31:21 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Ring_Numeral
19:31:21 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
19:31:21 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
19:31:22 CRYSTALS-Kyber: theory Number_Theoretic_Transform.Preliminary_Lemmas
19:31:22 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
19:31:22 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
19:31:22 CRYSTALS-Kyber: theory Number_Theoretic_Transform.NTT
19:31:22 Running Fishers_Inequality (on 10.195.8.29) ...
19:31:23 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
19:31:23 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Mod_Plus_Minus
19:31:23 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Abs_Qr
19:31:23 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
19:31:24 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Compress
19:31:24 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
19:31:24 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
19:31:24 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
19:31:25 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
19:31:25 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
19:31:27 Fishers_Inequality: theory Card_Partitions.Set_Partition
19:31:27 Fishers_Inequality: theory Polynomials.MPoly_Type
19:31:27 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme
19:31:27 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
19:31:28 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_Values
19:31:28 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
19:31:28 Fishers_Inequality: theory Polynomials.More_MPoly_Type
19:31:28 Fishers_Inequality: theory Polynomials.More_Modules
19:31:28 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Powers3844
19:31:29 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
19:31:29 Fishers_Inequality: theory Design_Theory.Multisets_Extras
19:31:29 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
19:31:29 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
19:31:29 CRYSTALS-Kyber: theory CRYSTALS-Kyber.NTT_Scheme
19:31:29 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
19:31:29 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
19:31:29 Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
19:31:29 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
19:31:29 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
19:31:30 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
19:31:30 Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
19:31:30 Fishers_Inequality: theory Design_Theory.Design_Basics
19:31:30 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
19:31:30 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
19:31:30 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
19:31:30 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
19:31:31 Algebraic_Numbers: theory Show.Show_Real
19:31:31 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Crypto_Scheme_NTT
19:31:31 Algebraic_Numbers: theory Show.Show_Complex
19:31:31 CRYSTALS-Kyber: theory CRYSTALS-Kyber.Kyber_NTT_Values
19:31:32 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
19:31:32 Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
19:31:32 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
19:31:32 Fishers_Inequality: theory Design_Theory.Design_Operations
19:31:32 Fishers_Inequality: theory List-Index.List_Index
19:31:33 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
19:31:33 CVP_Hardness: theory LLL_Basis_Reduction.Norms
19:31:33 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
19:31:33 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
19:31:33 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
19:31:33 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
19:31:33 Fishers_Inequality: theory Design_Theory.Block_Designs
19:31:35 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
19:31:35 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
19:31:36 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
19:31:36 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
19:31:37 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
19:31:37 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
19:31:38 Fishers_Inequality: theory Design_Theory.Sub_Designs
19:31:39 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
19:31:39 Fishers_Inequality: theory Design_Theory.BIBD
19:31:39 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
19:31:39 Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
19:31:39 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
19:31:40 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
19:31:40 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
19:31:40 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
19:31:40 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
19:31:41 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
19:31:41 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
19:31:42 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
19:31:42 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
19:31:42 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
19:31:42 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:31:42 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
19:31:43 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
19:31:43 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
19:31:43 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
19:31:43 Fishers_Inequality: theory Polynomials.Utils
19:31:43 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
19:31:44 Fishers_Inequality: theory Groebner_Bases.General
19:31:44 Fishers_Inequality: theory Polynomials.Power_Products
19:31:44 Linear_Recurrences_Solver: theory Show.Show_Real
19:31:45 Linear_Recurrences_Solver: theory Show.Show_Complex
19:31:45 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
19:31:45 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
19:31:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
19:31:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
19:31:47 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
19:31:48 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
19:31:49 Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
19:31:49 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:31:50 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
19:31:50 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
19:31:50 Linear_Recurrences_Solver: theory Polynomials.Utils
19:31:51 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
19:31:51 Linear_Recurrences_Solver: theory Polynomials.Power_Products
19:31:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
19:31:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
19:31:57 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
19:31:57 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
19:31:58 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
19:31:58 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
19:31:58 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
19:32:01 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
19:32:02 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
19:32:06 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
19:32:06 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
19:32:07 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
19:32:08 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
19:32:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
19:32:10 CVP_Hardness: theory CVP_Hardness.infnorm
19:32:10 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
19:32:10 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
19:32:10 CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
19:32:10 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
19:32:11 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
19:32:11 CVP_Hardness: theory CVP_Hardness.CVP_vec
19:32:12 CVP_Hardness: theory CVP_Hardness.BHLE
19:32:13 CVP_Hardness: theory CVP_Hardness.SVP_vec
19:32:13 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
19:32:13 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
19:32:13 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
19:32:14 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
19:32:16 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
19:32:24 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
19:32:27 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
19:32:28 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
19:32:28 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
19:32:31 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
19:32:32 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
19:32:33 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
19:32:34 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
19:32:35 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
19:32:37 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
19:32:37 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
19:32:38 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
19:32:39 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
19:32:41 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
19:32:41 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
19:32:42 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
19:32:42 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
19:32:44 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
19:32:46 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
19:32:46 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
19:32:48 Timing MDP-Algorithms (2 threads, 1151.660s elapsed time, 1960.135s cpu time, 535.483s GC time, factor 1.70)
19:32:48 Finished MDP-Algorithms (0:19:19 elapsed time, 0:32:53 cpu time, factor 1.70)
19:32:51 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
19:32:53 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
19:32:54 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
19:33:04 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
19:33:22 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
19:33:22 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
19:33:26 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
19:33:26 Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials
19:33:26 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
19:33:26 Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize
19:33:27 Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval
19:33:27 Perron_Frobenius: theory Perron_Frobenius.Roots_Unity
19:33:28 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion
19:33:28 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
19:33:29 Timing CRYSTALS-Kyber (2 threads, 136.221s elapsed time, 211.863s cpu time, 11.316s GC time, factor 1.56)
19:33:29 Finished CRYSTALS-Kyber (0:02:20 elapsed time, 0:03:36 cpu time, factor 1.54)
19:33:33 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
19:33:34 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
19:33:35 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible
19:33:37 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General
19:33:37 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
19:33:41 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
19:33:42 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
19:33:44 Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan
19:33:49 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
19:33:53 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
19:34:15 Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
19:34:18 Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp
19:34:18 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block
19:34:22 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2
19:34:23 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth
19:34:43 Timing CVP_Hardness (2 threads, 209.798s elapsed time, 332.741s cpu time, 16.630s GC time, factor 1.59)
19:34:43 Finished CVP_Hardness (0:03:33 elapsed time, 0:05:37 cpu time, factor 1.58)
19:35:01 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
19:35:01 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
19:35:04 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
19:35:09 Timing Perron_Frobenius (2 threads, 715.050s elapsed time, 1235.757s cpu time, 192.630s GC time, factor 1.73)
19:35:09 Finished Perron_Frobenius (0:12:01 elapsed time, 0:20:46 cpu time, factor 1.73)
19:35:11 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
19:35:13 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
19:35:22 Timing Fishers_Inequality (2 threads, 232.446s elapsed time, 430.353s cpu time, 44.344s GC time, factor 1.85)
19:35:22 Finished Fishers_Inequality (0:03:57 elapsed time, 0:07:16 cpu time, factor 1.84)
19:35:54 Timing LLL_Basis_Reduction (2 threads, 244.826s elapsed time, 404.271s cpu time, 26.193s GC time, factor 1.65)
19:35:54 Finished LLL_Basis_Reduction (0:04:44 elapsed time, 0:07:37 cpu time, factor 1.61)
19:35:55 Building Linear_Inequalities (on 10.195.8.49) ...
19:35:55 Running LLL_Factorization (on 10.195.8.49) ...
19:35:59 Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
19:36:00 Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
19:36:00 LLL_Factorization: theory LLL_Factorization.Sub_Sums
19:36:00 LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
19:36:01 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
19:36:01 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
19:36:03 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
19:36:03 Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
19:36:03 Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
19:36:04 Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
19:36:07 LLL_Factorization: theory LLL_Factorization.LLL_Factorization
19:36:11 Linear_Inequalities: theory Linear_Inequalities.Cone
19:36:14 Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
19:36:17 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
19:36:22 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
19:36:31 Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
19:36:31 Linear_Inequalities: theory Linear_Inequalities.Dim_Span
19:36:34 Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
19:36:37 Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
19:36:38 Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
19:36:40 Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
19:36:47 Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
19:36:50 Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
19:37:16 Timing LLL_Factorization (2 threads, 75.647s elapsed time, 143.726s cpu time, 9.467s GC time, factor 1.90)
19:37:16 Finished LLL_Factorization (0:01:19 elapsed time, 0:02:27 cpu time, factor 1.86)
19:37:48 Timing Linear_Inequalities (2 threads, 79.443s elapsed time, 145.544s cpu time, 10.091s GC time, factor 1.83)
19:37:48 Finished Linear_Inequalities (0:01:51 elapsed time, 0:03:06 cpu time, factor 1.67)
19:37:48 Running LP_Duality (on 10.195.8.49) ...
19:37:51 LP_Duality: theory LP_Duality.Minimum_Maximum
19:37:51 LP_Duality: theory LP_Duality.LP_Duality
19:37:53 Timing Algebraic_Numbers (2 threads, 362.817s elapsed time, 639.515s cpu time, 36.305s GC time, factor 1.76)
19:37:53 Finished Algebraic_Numbers (0:06:42 elapsed time, 0:11:33 cpu time, factor 1.72)
19:37:59 Timing LP_Duality (2 threads, 8.075s elapsed time, 10.573s cpu time, 0.295s GC time, factor 1.31)
19:37:59 Finished LP_Duality (0:00:11 elapsed time, 0:00:13 cpu time, factor 1.19)
19:38:03 Running Quantifier_Elimination_Hybrid (on 10.195.8.40) ...
19:38:03 Running BenOr_Kozen_Reif (on 10.195.8.40) ...
19:38:03 Running Cubic_Quartic_Equations (on 10.195.8.40) ...
19:38:03 Running Factor_Algebraic_Polynomial (on 10.195.8.40) ...
19:38:06 BenOr_Kozen_Reif: theory Sturm_Tarski.PolyMisc
19:38:06 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.More_Matrix
19:38:06 Cubic_Quartic_Equations: theory Complex_Geometry.More_Transcendental
19:38:06 Cubic_Quartic_Equations: theory Factor_Algebraic_Polynomial.Roots_via_IA
19:38:06 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
19:38:06 Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
19:38:07 BenOr_Kozen_Reif: theory Sturm_Tarski.Sturm_Tarski
19:38:07 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
19:38:07 Cubic_Quartic_Equations: theory Complex_Geometry.Canonical_Angle
19:38:07 Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
19:38:08 Cubic_Quartic_Equations: theory Complex_Geometry.More_Complex
19:38:08 Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
19:38:08 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux
19:38:08 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type
19:38:08 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cardanos_Formula
19:38:08 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Ferraris_Formula
19:38:08 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
19:38:09 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
19:38:09 Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator
19:38:09 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
19:38:09 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Complex_Roots
19:38:09 Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
19:38:09 Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules
19:38:10 Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type
19:38:10 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Algorithm
19:38:10 Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map
19:38:10 Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots
19:38:10 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
19:38:10 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate
19:38:11 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta
19:38:11 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc
19:38:11 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski
19:38:11 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
19:38:12 Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials
19:38:12 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
19:38:12 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Algorithm
19:38:12 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Proofs
19:38:12 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
19:38:12 Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
19:38:13 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
19:38:13 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
19:38:13 Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
19:38:15 Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates
19:38:15 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.BKR_Decision
19:38:15 Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence
19:38:15 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Proofs
19:38:15 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:38:16 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
19:38:16 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Cubic_Polynomials
19:38:17 Factor_Algebraic_Polynomial: theory Polynomials.Utils
19:38:17 Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
19:38:17 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
19:38:17 Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials
19:38:17 Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
19:38:18 Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
19:38:18 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix
19:38:20 Cubic_Quartic_Equations: theory Cubic_Quartic_Equations.Quartic_Polynomials
19:38:22 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm
19:38:22 BenOr_Kozen_Reif: theory BenOr_Kozen_Reif.Renegar_Decision
19:38:23 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction
19:38:24 Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials
19:38:24 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs
19:38:24 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm
19:38:25 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences
19:38:25 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements
19:38:25 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum
19:38:25 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full
19:38:25 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs
19:38:27 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences
19:38:27 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision
19:38:27 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations
19:38:27 Quantifier_Elimination_Hybrid: theory Polynomials.Utils
19:38:28 Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders
19:38:28 Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products
19:38:30 Timing Cubic_Quartic_Equations (2 threads, 22.246s elapsed time, 39.310s cpu time, 2.872s GC time, factor 1.77)
19:38:30 Finished Cubic_Quartic_Equations (0:00:26 elapsed time, 0:00:43 cpu time, factor 1.64)
19:38:30 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
19:38:32 Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision
19:38:33 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
19:38:33 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
19:38:34 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
19:38:35 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified
19:38:36 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
19:38:44 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class
19:38:47 Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection
19:38:48 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered
19:38:49 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
19:38:52 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
19:38:52 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
19:38:55 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
19:38:57 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
19:38:57 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
19:39:00 Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap
19:39:02 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
19:39:02 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
19:39:03 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension
19:39:03 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE
19:39:04 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps
19:39:05 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms
19:39:14 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn
19:39:14 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting
19:39:18 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations
19:39:19 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex
19:39:21 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms
19:39:26 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs
19:39:27 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos
19:39:35 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF
19:39:35 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic
19:39:36 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase
19:39:36 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity
19:39:37 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase
19:39:37 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable
19:39:38 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind
19:39:38 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS
19:39:38 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals
19:39:39 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni
19:39:40 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni
19:39:41 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni
19:39:42 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs
19:39:43 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports
19:39:43 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad
19:39:44 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props
19:39:46 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments
19:39:47 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence
19:39:48 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
19:39:50 Timing Factor_Algebraic_Polynomial (2 threads, 100.313s elapsed time, 188.310s cpu time, 21.518s GC time, factor 1.88)
19:39:50 Finished Factor_Algebraic_Polynomial (0:01:45 elapsed time, 0:03:13 cpu time, factor 1.84)
19:39:50 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs
19:39:51 Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs
19:39:54 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
19:39:57 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
19:40:21 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
19:40:21 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
19:40:47 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
19:41:01 Timing Linear_Recurrences_Solver (2 threads, 584.960s elapsed time, 1049.882s cpu time, 141.202s GC time, factor 1.79)
19:41:01 Finished Linear_Recurrences_Solver (0:09:50 elapsed time, 0:17:36 cpu time, factor 1.79)
19:41:01 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
19:41:09 Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
19:41:28 Timing BenOr_Kozen_Reif (2 threads, 199.673s elapsed time, 314.190s cpu time, 25.491s GC time, factor 1.57)
19:41:28 Finished BenOr_Kozen_Reif (0:03:24 elapsed time, 0:05:20 cpu time, factor 1.56)
19:42:45 CakeML_Codegen: theory Lazy_Case.Lazy_Case
19:42:45 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
19:42:45 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
19:42:54 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
19:42:57 CakeML_Codegen: theory CakeML_Codegen.Test_Composition
19:43:04 CakeML_Codegen: theory CakeML_Codegen.Test_Print
19:43:05 Timing Shadow_SC_DOM (2 threads, 1478.362s elapsed time, 2530.294s cpu time, 324.926s GC time, factor 1.71)
19:43:05 Finished Shadow_SC_DOM (0:26:10 elapsed time, 0:44:17 cpu time, factor 1.69)
19:43:07 Running SC_DOM_Components (on 10.195.7.194) ...
19:43:18 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
19:43:35 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
19:43:48 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
19:43:50 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
19:44:05 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
19:46:48 Timing Automated_Stateful_Protocol_Verification (2 threads, 1474.436s elapsed time, 2842.384s cpu time, 1243.181s GC time, factor 1.93)
19:46:48 Finished Automated_Stateful_Protocol_Verification (0:24:49 elapsed time, 0:47:50 cpu time, factor 1.93)
19:47:50 Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
19:47:50 Timing CakeML_Codegen (2 threads, 2638.678s elapsed time, 3194.978s cpu time, 307.188s GC time, factor 1.21)
19:47:50 Finished CakeML_Codegen (0:44:05 elapsed time, 0:53:26 cpu time, factor 1.21)
19:50:14 Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2249.570s elapsed time, 3971.681s cpu time, 794.771s GC time, factor 1.77)
19:50:14 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:37:39 elapsed time, 1:06:29 cpu time, factor 1.77)
19:53:44 Timing HOL-ODE-Numerics (2 threads, 2706.970s elapsed time, 4606.977s cpu time, 564.552s GC time, factor 1.70)
19:53:44 Finished HOL-ODE-Numerics (0:46:40 elapsed time, 1:19:04 cpu time, factor 1.69)
19:53:50 Running HOL-ODE-ARCH-COMP (on of4.proof.cit.tum.de) ...
19:53:50 Running HOL-ODE-Examples (on of4.proof.cit.tum.de) ...
19:53:50 Building Lorenz_Approximation (on of4.proof.cit.tum.de) ...
19:53:50 Running Poincare_Bendixson (on of4.proof.cit.tum.de) ...
19:53:51 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
19:53:51 Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
19:53:51 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
19:53:51 Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
19:53:51 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
19:53:51 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
19:53:51 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
19:53:52 Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
19:53:54 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
19:53:55 Poincare_Bendixson: theory Poincare_Bendixson.Invariance
19:53:57 Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
19:53:58 Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
19:53:59 Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
19:54:00 Estimated completion: 29-Nov-2023 20:29:33 +0100 (took 0.028s)
19:54:03 Poincare_Bendixson: theory Poincare_Bendixson.Examples
19:54:09 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
19:54:40 Timing Quantifier_Elimination_Hybrid (2 threads, 981.910s elapsed time, 1659.149s cpu time, 210.017s GC time, factor 1.69)
19:54:40 Finished Quantifier_Elimination_Hybrid (0:16:30 elapsed time, 0:27:53 cpu time, factor 1.69)
19:54:41 Timing Poincare_Bendixson (6 threads, 48.859s elapsed time, 127.167s cpu time, 6.677s GC time, factor 2.60)
19:54:41 Finished Poincare_Bendixson (0:00:50 elapsed time, 0:02:09 cpu time, factor 2.54)
19:54:55 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
19:55:38 Timing HOL-ODE-Examples (6 threads, 106.865s elapsed time, 418.302s cpu time, 17.132s GC time, factor 3.91)
19:55:38 Finished HOL-ODE-Examples (0:01:48 elapsed time, 0:07:00 cpu time, factor 3.87)
19:56:01 Timing Lorenz_Approximation (6 threads, 115.553s elapsed time, 287.139s cpu time, 36.155s GC time, factor 2.48)
19:56:01 Finished Lorenz_Approximation (0:02:10 elapsed time, 0:05:14 cpu time, factor 2.41)
19:56:02 Running Lorenz_C0 (on of4.proof.cit.tum.de) ...
19:56:02 Running Lorenz_C1 (on of4.proof.cit.tum.de) ...
19:56:04 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
19:56:04 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
19:56:05 Timing Lorenz_C1 (6 threads, 0.637s elapsed time, 0.920s cpu time, 0.020s GC time, factor 1.44)
19:56:05 Finished Lorenz_C1 (0:00:02 elapsed time)
19:56:23 Timing HOL-ODE-ARCH-COMP (6 threads, 151.145s elapsed time, 429.033s cpu time, 29.979s GC time, factor 2.84)
19:56:23 Finished HOL-ODE-ARCH-COMP (0:02:33 elapsed time, 0:07:10 cpu time, factor 2.82)
19:58:20 Timing SC_DOM_Components (2 threads, 907.192s elapsed time, 1663.762s cpu time, 225.308s GC time, factor 1.83)
19:58:20 Finished SC_DOM_Components (0:15:12 elapsed time, 0:27:52 cpu time, factor 1.83)
20:00:21 Timing Lorenz_C0 (6 threads, 256.835s elapsed time, 1463.803s cpu time, 18.388s GC time, factor 5.70)
20:00:21 Finished Lorenz_C0 (0:04:18 elapsed time, 0:24:25 cpu time, factor 5.67)
20:38:23 Timing CZH_Universal_Constructions (2 threads, 4192.662s elapsed time, 7017.462s cpu time, 2522.213s GC time, factor 1.67)
20:38:23 Finished CZH_Universal_Constructions (1:09:57 elapsed time, 1:57:04 cpu time, factor 1.67)
20:38:34 
20:38:34 Finished at Wed Nov 29 20:38:34 GMT+1 2023
20:38:34 2:01:56 elapsed time, 54:59:11 cpu time, factor 27.05
20:38:35 Started calculate disk usage of build
20:38:35 Finished Calculation of disk usage of build in 0 seconds
20:38:55 Started calculate disk usage of workspace
20:38:56 Finished Calculation of disk usage of workspace in 0 seconds
20:38:57 Finished: SUCCESS