Skipping 33 KB.. Full Log

Session AFP/Linear_Inequalities (AFP)
13:39:27 Session AFP/LP_Duality (AFP)
13:39:27 Session AFP/Linear_Programming (AFP)
13:39:27 Session AFP/Number_Theoretic_Transform (AFP)
13:39:27 Session AFP/CRYSTALS-Kyber (AFP)
13:39:27 Session AFP/Perfect_Fields (AFP)
13:39:27 Session AFP/Elimination_Of_Repeated_Factors (AFP)
13:39:27 Session AFP/Smith_Normal_Form (AFP)
13:39:27 Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
13:39:28 Session AFP/Polynomials (AFP)
13:39:28 Session AFP/Deep_Learning (AFP)
13:39:29 Session AFP/QHLProver (AFP)
13:39:29 Session AFP/Projective_Measurements (AFP)
13:39:29 Session AFP/Commuting_Hermitian (AFP)
13:39:29 Session AFP/TsirelsonBound (AFP)
13:39:29 Session AFP/Uncertainty_Principle (AFP)
13:39:29 Session AFP/Groebner_Bases (AFP)
13:39:30 Session AFP/Fishers_Inequality (AFP)
13:39:30 Session AFP/Hypergraph_Basics (AFP)
13:39:30 Session AFP/Hypergraph_Colourings (AFP)
13:39:30 Session AFP/Groebner_Macaulay (AFP)
13:39:30 Session AFP/Nullstellensatz (AFP)
13:39:30 Session AFP/Signature_Groebner (AFP)
13:39:31 Session AFP/Lambda_Free_KBOs (AFP)
13:39:31 Session AFP/Sumcheck_Protocol (AFP)
13:39:31 Session AFP/Symmetric_Polynomials (AFP)
13:39:31 Session AFP/Pi_Transcendental (AFP)
13:39:31 Session AFP/Power_Sum_Polynomials (AFP)
13:39:31 Session AFP/Hermite_Lindemann (AFP)
13:39:31 Session AFP/Factor_Algebraic_Polynomial (AFP)
13:39:31 Session AFP/Cubic_Quartic_Equations (AFP)
13:39:31 Session AFP/Linear_Recurrences_Solver (AFP)
13:39:32 Session AFP/Orient_Rewrite_Rule_Undecidable (AFP)
13:39:32 Session AFP/Schwartz_Zippel (AFP)
13:39:32 Session AFP/Virtual_Substitution (AFP)
13:39:33 Session AFP/Real_Impl (AFP)
13:39:33 Session AFP/Complex_Bounded_Operators_Dependencies (AFP)
13:39:33 Session AFP/Complex_Bounded_Operators (AFP)
13:39:33 Session AFP/Registers (AFP)
13:39:34 Session AFP/QR_Decomposition (AFP)
13:39:34 Session AFP/XML (AFP)
13:39:34 Session AFP/Van_Emde_Boas_Trees (AFP)
13:39:34 Session AFP/Dijkstra_Shortest_Path (AFP)
13:39:34 Session AFP/Koenigsberg_Friendship (AFP)
13:39:34 Session AFP/FOL_Seq_Calc2 (AFP)
13:39:34 Session AFP/Formal_SSA (AFP)
13:39:35 Session AFP/Minimal_SSA (AFP)
13:39:35 Session AFP/Gale_Shapley (AFP)
13:39:35 Session AFP/HOL-ODE-Numerics (AFP)
13:39:36 Session AFP/HOL-ODE-ARCH-COMP (AFP)
13:39:36 Session AFP/HOL-ODE-Examples (AFP large)
13:39:36 Session AFP/Lorenz_Approximation (AFP)
13:39:36 Session AFP/Lorenz_C0 (AFP large)
13:39:36 Session AFP/Lorenz_C1 (AFP large)
13:39:36 Session AFP/Poincare_Bendixson (AFP)
13:39:36 Session AFP/Picks_Theorem (AFP)
13:39:36 Session AFP/KnuthMorrisPratt (AFP)
13:39:36 Session AFP/Safe_Range_RC (AFP)
13:39:36 Session AFP/Transition_Systems_and_Automata (AFP)
13:39:36 Session AFP/Adaptive_State_Counting (AFP)
13:39:36 Session AFP/Buchi_Complementation (AFP)
13:39:36 Session AFP/LTL_Master_Theorem (AFP)
13:39:37 Session AFP/LTL_Normal_Form (AFP)
13:39:37 Session AFP/Partial_Order_Reduction (AFP)
13:39:37 Session AFP/SM_Base (AFP)
13:39:37 Session AFP/SM (AFP)
13:39:37 Session AFP/CAVA_Setup (AFP)
13:39:37 Session AFP/CAVA_LTL_Modelchecker (AFP)
13:39:37 Session AFP/Transitive-Closure (AFP)
13:39:37 Session AFP/KBPs (AFP)
13:39:37 Session AFP/LTL_to_DRA (AFP)
13:39:38 Session AFP/Network_Security_Policy_Verification (AFP)
13:39:38 Session AFP/Planarity_Certificates (AFP)
13:39:38 Session AFP/Tree-Automata (AFP)
13:39:38 Session AFP/Datatype_Order_Generator (AFP)
13:39:38 Session AFP/Higher_Order_Terms (AFP)
13:39:38 Session AFP/CakeML_Codegen (AFP)
13:39:39 Session AFP/Old_Datatype_Show (AFP)
13:39:39 Session AFP/Quantifier_Elimination_Hybrid (AFP)
13:39:39 Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
13:39:39 Session AFP/FSM_Tests (AFP)
13:39:40 Session AFP/Iptables_Semantics (AFP)
13:39:40 Session AFP/Iptables_Semantics_Examples (AFP)
13:39:40 Session AFP/LOFT (AFP)
13:39:40 Session AFP/Mersenne_Primes (AFP)
13:39:40 Session AFP/MiniSail (AFP)
13:39:40 Session AFP/Separation_Logic_Imperative_HOL (AFP)
13:39:40 Session AFP/Sepref_Prereq (AFP)
13:39:41 Session AFP/ROBDD (AFP)
13:39:41 Session AFP/Refine_Imperative_HOL (AFP)
13:39:41 Session AFP/BTree (AFP)
13:39:41 Session AFP/Floyd_Warshall (AFP)
13:39:41 Session AFP/Sepref_Basic (AFP)
13:39:41 Session AFP/Sepref_IICF (AFP)
13:39:41 Session AFP/Flow_Networks (AFP)
13:39:41 Session AFP/EdmondsKarp_Maxflow (AFP)
13:39:41 Session AFP/MFMC_Countable (AFP)
13:39:41 Session AFP/Probabilistic_While (AFP)
13:39:41 Session AFP/CryptHOL (AFP)
13:39:42 Session AFP/ABY3_Protocols (AFP)
13:39:42 Session AFP/Constructive_Cryptography (AFP)
13:39:42 Session AFP/Game_Based_Crypto (AFP)
13:39:42 Session AFP/CRYSTALS-Kyber_Security (AFP)
13:39:42 Session AFP/Multi_Party_Computation (AFP)
13:39:42 Session AFP/Sigma_Commit_Crypto (AFP)
13:39:42 Session AFP/Constructive_Cryptography_CM (AFP)
13:39:42 Session AFP/Executable_Randomized_Algorithms (AFP)
13:39:43 Session AFP/Finite_Fields (AFP)
13:39:45 Session AFP/Universal_Hash_Families (AFP)
13:39:45 Session AFP/Expander_Graphs (AFP)
13:39:46 Session AFP/Karatsuba (AFP)
13:39:46 Session AFP/Median_Method (AFP)
13:39:46 Session AFP/Frequency_Moments (AFP)
13:39:47 Session AFP/Approximate_Model_Counting (AFP)
13:39:47 Session AFP/Distributed_Distinct_Elements (AFP)
13:39:48 Session AFP/Derandomization_Conditional_Expectations (AFP)
13:39:48 Session AFP/Prpu_Maxflow (AFP)
13:39:48 Session AFP/Knuth_Morris_Pratt (AFP)
13:39:48 Session AFP/Kruskal (AFP)
13:39:48 Session AFP/PAC_Checker (AFP)
13:39:48 Session AFP/VerifyThis2018 (AFP)
13:39:48 Session AFP/VerifyThis2019 (AFP)
13:39:48 Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
13:39:49 Session AFP/UpDown_Scheme (AFP)
13:39:49 Session AFP/WebAssembly (AFP)
13:39:49 Session AFP/SPARCv8 (AFP)
13:39:49 Session AFP/Schoenhage_Strassen (AFP)
13:39:50 Session AFP/X86_Semantics (AFP)
13:39:50 Session AFP/ZFC_in_HOL (AFP)
13:39:50 Session AFP/CZH_Foundations (AFP)
13:39:50 Session AFP/CZH_Elementary_Categories (AFP)
13:39:51 Session AFP/CZH_Universal_Constructions (AFP)
13:39:51 Session AFP/Category3 (AFP)
13:39:51 Session AFP/MonoidalCategory (AFP)
13:39:51 Session AFP/Ordinal_Partitions (AFP)
13:39:51 Session AFP/Q0_Metatheory (AFP)
13:39:51 Session AFP/Q0_Soundness (AFP)
13:39:51 Session AFP/Wetzels_Problem (AFP)
13:39:52 Session FOL/ZF (main timing)
13:39:52 Session Doc/Logics_ZF (doc)
13:39:52 Session AFP/Recursion-Addition (AFP)
13:39:52 Session FOL/ZF-AC
13:39:52 Session FOL/ZF-Coind
13:39:52 Session FOL/ZF-Constructible
13:39:52 Session AFP/Delta_System_Lemma (AFP)
13:39:52 Session AFP/Transitive_Models (AFP)
13:39:52 Session AFP/Independence_CH (AFP)
13:39:52 Session AFP/Forcing (AFP)
13:39:52 Session FOL/ZF-IMP
13:39:52 Session FOL/ZF-Induct
13:39:52 Session FOL/ZF-UNITY (timing)
13:39:52 Session FOL/ZF-Resid
13:39:52 Session FOL/ZF-ex
13:40:27 Building LEM (on hpcisabelle/0) ...
13:40:29 LEM: theory HOL-Library.Cancellation
13:40:29 LEM: theory HOL-Combinatorics.Transposition
13:40:29 LEM: theory HOL-Library.FuncSet
13:40:29 LEM: theory HOL-Library.Phantom_Type
13:40:29 LEM: theory LEM.Lem_bool
13:40:29 LEM: theory HOL-Library.Sublist
13:40:29 LEM: theory HOL-Library.While_Combinator
13:40:29 LEM: theory Word_Lib.Even_More_List
13:40:29 LEM: theory LEM.Lem_basic_classes
13:40:29 LEM: theory Word_Lib.More_Bit_Ring
13:40:30 LEM: theory HOL-Library.Disjoint_Sets
13:40:30 LEM: theory HOL-Library.Cardinality
13:40:30 LEM: theory HOL-Library.Multiset
13:40:31 LEM: theory HOL-Library.Numeral_Type
13:40:32 LEM: theory HOL-Library.Type_Length
13:40:33 LEM: theory HOL-Library.Word
13:40:33 LEM: theory Word_Lib.More_Arithmetic
13:40:35 LEM: theory LEM.Lem_function
13:40:35 LEM: theory LEM.Lem_tuple
13:40:35 LEM: theory LEM.Lem_maybe
13:40:37 LEM: theory HOL-Combinatorics.Permutations
13:40:39 LEM: theory HOL-Combinatorics.List_Permutation
13:40:39 LEM: theory LEM.LemExtraDefs
13:40:44 LEM: theory Word_Lib.Bit_Comprehension
13:40:44 LEM: theory Word_Lib.Legacy_Aliases
13:40:44 LEM: theory Word_Lib.More_Divides
13:40:44 LEM: theory LEM.Lem_num
13:40:44 LEM: theory Word_Lib.More_Word
13:40:46 LEM: theory Word_Lib.Bit_Shifts_Infix_Syntax
13:40:46 LEM: theory Word_Lib.Least_significant_bit
13:40:48 LEM: theory Word_Lib.Aligned
13:40:48 LEM: theory Word_Lib.Singleton_Bit_Shifts
13:40:49 LEM: theory Word_Lib.Most_significant_bit
13:40:49 LEM: theory Word_Lib.Generic_set_bit
13:40:50 LEM: theory Word_Lib.Bits_Int
13:40:52 LEM: theory LEM.Lem_set_helpers
13:40:54 LEM: theory Word_Lib.Typedef_Morphisms
13:40:55 LEM: theory Word_Lib.Reversed_Bit_Lists
13:40:58 LEM: theory LEM.Lem
13:40:59 LEM: theory LEM.Lem_assert_extra
13:40:59 LEM: theory LEM.Lem_function_extra
13:40:59 LEM: theory LEM.Lem_list
13:40:59 LEM: theory LEM.Lem_maybe_extra
13:41:04 LEM: theory LEM.Lem_set
13:41:04 LEM: theory LEM.Lem_string
13:41:04 LEM: theory LEM.Lem_word
13:41:04 LEM: theory LEM.Lem_sorting
13:41:04 LEM: theory LEM.Lem_either
13:41:04 LEM: theory LEM.Lem_list_extra
13:41:04 LEM: theory LEM.Lem_num_extra
13:41:04 LEM: theory LEM.Lem_show
13:41:05 LEM: theory LEM.Lem_relation
13:41:05 LEM: theory LEM.Lem_map
13:41:05 LEM: theory LEM.Lem_set_extra
13:41:05 LEM: theory LEM.Lem_map_extra
13:41:05 LEM: theory LEM.Lem_machine_word
13:41:06 LEM: theory LEM.Lem_string_extra
13:41:06 LEM: theory LEM.Lem_show_extra
13:41:10 LEM: theory LEM.Lem_pervasives
13:41:12 LEM: theory LEM.Lem_pervasives_extra
13:41:36 Timing LEM (8 threads, 48.256s elapsed time, 302.042s cpu time, 9.207s GC time, factor 6.26)
13:41:36 Finished LEM (0:01:07 elapsed time, 0:05:43 cpu time, factor 5.11)
13:41:36 Running Finite_Fields (on hpcisabelle/1) ...
13:41:41 Finite_Fields: theory Digit_Expansions.Bits_Digits
13:41:41 Finite_Fields: theory Flow_Networks.Graph
13:41:41 Finite_Fields: theory HOL-Number_Theory.Cong
13:41:41 Finite_Fields: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
13:41:41 Finite_Fields: theory HOL-Number_Theory.Eratosthenes
13:41:41 Finite_Fields: theory HOL-Real_Asymp.Inst_Existentials
13:41:41 Finite_Fields: theory HOL-Types_To_Sets.Types_To_Sets
13:41:41 Finite_Fields: theory HOL-Analysis.Metric_Arith
13:41:41 Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results
13:41:42 Finite_Fields: theory Finite_Fields.Finite_Fields_More_Bijections
13:41:42 Finite_Fields: theory HOL-Analysis.Abstract_Topology
13:41:42 Finite_Fields: theory HOL-Analysis.Continuum_Not_Denumerable
13:41:42 Finite_Fields: theory HOL-Analysis.Inner_Product
13:41:43 Finite_Fields: theory HOL-Analysis.L2_Norm
13:41:43 Finite_Fields: theory HOL-Analysis.Operator_Norm
13:41:43 Finite_Fields: theory HOL-Analysis.Poly_Roots
13:41:43 Finite_Fields: theory HOL-Analysis.Product_Vector
13:41:43 Finite_Fields: theory HOL-Combinatorics.Multiset_Permutations
13:41:44 Finite_Fields: theory HOL-Analysis.Sigma_Algebra
13:41:44 Finite_Fields: theory HOL-Number_Theory.Mod_Exp
13:41:44 Finite_Fields: theory Flow_Networks.Network
13:41:45 Finite_Fields: theory HOL-Analysis.Norm_Arith
13:41:46 Finite_Fields: theory HOL-Number_Theory.Fib
13:41:46 Finite_Fields: theory HOL-Number_Theory.Prime_Powers
13:41:46 Finite_Fields: theory HOL-Number_Theory.Totient
13:41:46 Finite_Fields: theory HOL-Real_Asymp.Eventuallize
13:41:46 Finite_Fields: theory HOL-Real_Asymp.Lazy_Eval
13:41:47 Finite_Fields: theory HOL-Analysis.Elementary_Topology
13:41:47 Finite_Fields: theory HOL-Analysis.Euclidean_Space
13:41:47 Finite_Fields: theory Flow_Networks.Residual_Graph
13:41:48 Finite_Fields: theory HOL-Number_Theory.Residues
13:41:48 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion
13:41:48 Finite_Fields: theory HOL-Analysis.Measurable
13:41:49 Finite_Fields: theory HOL-Analysis.Abstract_Limits
13:41:50 Finite_Fields: theory HOL-Analysis.FSigma
13:41:50 Finite_Fields: theory HOL-Analysis.Sum_Topology
13:41:50 Finite_Fields: theory HOL-Analysis.Measure_Space
13:41:52 Finite_Fields: theory Flow_Networks.Augmenting_Flow
13:41:52 Finite_Fields: theory Flow_Networks.Augmenting_Path
13:41:52 Finite_Fields: theory HOL-Analysis.Finite_Cartesian_Product
13:41:52 Finite_Fields: theory HOL-Analysis.Linear_Algebra
13:41:52 Finite_Fields: theory Flow_Networks.Ford_Fulkerson
13:41:53 Finite_Fields: theory HOL-Analysis.Abstract_Topology_2
13:41:53 Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
13:41:53 Finite_Fields: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
13:41:54 Finite_Fields: theory Finite_Fields.Ring_Characteristic
13:41:54 Finite_Fields: theory HOL-Analysis.Affine
13:41:55 Finite_Fields: theory HOL-Analysis.Infinite_Sum
13:41:55 Finite_Fields: theory MFMC_Countable.MFMC_Finite
13:41:56 Finite_Fields: theory HOL-Analysis.Convex
13:41:56 Finite_Fields: theory HOL-Analysis.Cartesian_Space
13:41:56 Finite_Fields: theory HOL-Analysis.Caratheodory
13:41:56 Finite_Fields: theory HOL-Analysis.Connected
13:41:57 Finite_Fields: theory HOL-Analysis.Elementary_Metric_Spaces
13:41:57 Finite_Fields: theory HOL-Analysis.Function_Topology
13:41:57 Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
13:41:58 Finite_Fields: theory HOL-Number_Theory.Gauss
13:41:59 Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
13:41:59 Finite_Fields: theory HOL-Number_Theory.Pocklington
13:41:59 Finite_Fields: theory HOL-Analysis.Product_Topology
13:42:01 Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
13:42:01 Finite_Fields: theory HOL-Analysis.T1_Spaces
13:42:01 Finite_Fields: theory HOL-Analysis.Determinants
13:42:01 Finite_Fields: theory HOL-Number_Theory.Number_Theory
13:42:01 Finite_Fields: theory HOL-Analysis.Lindelof_Spaces
13:42:02 Finite_Fields: theory HOL-Analysis.Elementary_Normed_Spaces
13:42:02 Finite_Fields: theory HOL-Analysis.Function_Metric
13:42:02 Finite_Fields: theory HOL-Analysis.Isolated
13:42:03 Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
13:42:03 Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
13:42:03 Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
13:42:03 Finite_Fields: theory HOL-Analysis.Topology_Euclidean_Space
13:42:04 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
13:42:05 Finite_Fields: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
13:42:05 Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
13:42:06 Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
13:42:06 Finite_Fields: theory HOL-Analysis.Extended_Real_Limits
13:42:07 Finite_Fields: theory HOL-Analysis.Line_Segment
13:42:07 Finite_Fields: theory HOL-Analysis.Tagged_Division
13:42:07 Finite_Fields: theory HOL-Analysis.Summation_Tests
13:42:08 Finite_Fields: theory Dirichlet_Series.Moebius_Mu
13:42:08 Finite_Fields: theory Dirichlet_Series.More_Totient
13:42:08 Finite_Fields: theory Dirichlet_Series.Divisor_Count
13:42:08 Finite_Fields: theory HOL-Analysis.Convex_Euclidean_Space
13:42:09 Finite_Fields: theory Dirichlet_Series.Liouville_Lambda
13:42:09 Finite_Fields: theory HOL-Analysis.Uniform_Limit
13:42:09 Finite_Fields: theory Dirichlet_Series.Arithmetic_Summatory
13:42:09 Finite_Fields: theory HOL-Analysis.Ordered_Euclidean_Space
13:42:09 Finite_Fields: theory HOL-Analysis.Starlike
13:42:11 Finite_Fields: theory HOL-Analysis.Bounded_Continuous_Function
13:42:11 Finite_Fields: theory HOL-Analysis.Bounded_Linear_Function
13:42:12 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
13:42:12 Finite_Fields: theory HOL-Analysis.Continuous_Extension
13:42:12 Finite_Fields: theory HOL-Analysis.Path_Connected
13:42:14 Finite_Fields: theory HOL-Analysis.Derivative
13:42:15 Finite_Fields: theory HOL-Analysis.Locally
13:42:15 Finite_Fields: theory HOL-Analysis.Uncountable_Sets
13:42:15 Finite_Fields: theory HOL-Analysis.Arcwise_Connected
13:42:15 Finite_Fields: theory HOL-Analysis.Homotopy
13:42:17 Finite_Fields: theory HOL-Analysis.Borel_Space
13:42:17 Finite_Fields: theory HOL-Analysis.Cartesian_Euclidean_Space
13:42:18 Finite_Fields: theory HOL-Analysis.Complex_Analysis_Basics
13:42:18 Finite_Fields: theory HOL-Analysis.Cross3
13:42:18 Finite_Fields: theory HOL-Analysis.Polytope
13:42:19 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
13:42:20 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test
13:42:21 Finite_Fields: theory HOL-Analysis.Abstract_Euclidean_Space
13:42:21 Finite_Fields: theory HOL-Analysis.Homeomorphism
13:42:23 Finite_Fields: theory HOL-Analysis.Complex_Transcendental
13:42:24 Finite_Fields: theory HOL-Analysis.Abstract_Topological_Spaces
13:42:24 Finite_Fields: theory HOL-Analysis.Sparse_In
13:42:24 Finite_Fields: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
13:42:24 Finite_Fields: theory HOL-Analysis.Regularity
13:42:24 Finite_Fields: theory HOL-Analysis.Brouwer_Fixpoint
13:42:25 Finite_Fields: theory Executable_Randomized_Algorithms.Tau_Additivity
13:42:26 Finite_Fields: theory HOL-Analysis.Weierstrass_Theorems
13:42:28 Finite_Fields: theory HOL-Analysis.Fashoda_Theorem
13:42:30 Finite_Fields: theory HOL-Analysis.Retracts
13:42:30 Finite_Fields: theory HOL-Analysis.Generalised_Binomial_Theorem
13:42:30 Finite_Fields: theory HOL-Analysis.Binary_Product_Measure
13:42:31 Finite_Fields: theory HOL-Analysis.Harmonic_Numbers
13:42:31 Finite_Fields: theory HOL-Analysis.FPS_Convergence
13:42:31 Finite_Fields: theory HOL-Analysis.Infinite_Products
13:42:32 Finite_Fields: theory HOL-Analysis.Abstract_Metric_Spaces
13:42:33 Finite_Fields: theory HOL-Analysis.Embed_Measure
13:42:33 Finite_Fields: theory HOL-Analysis.Finite_Product_Measure
13:42:34 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
13:42:34 Finite_Fields: theory HOL-Analysis.Smooth_Paths
13:42:35 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test_Code
13:42:36 Finite_Fields: theory HOL-Analysis.Bochner_Integration
13:42:36 Finite_Fields: theory HOL-Probability.Fin_Map
13:42:38 Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
13:42:40 Finite_Fields: theory HOL-Analysis.Complete_Measure
13:42:40 Finite_Fields: theory HOL-Analysis.Radon_Nikodym
13:42:41 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
13:42:41 Finite_Fields: theory HOL-Analysis.Lipschitz
13:42:41 Finite_Fields: theory HOL-Analysis.Urysohn
13:42:41 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
13:42:41 Finite_Fields: theory HOL-Analysis.Set_Integral
13:42:42 Finite_Fields: theory HOL-Analysis.Lebesgue_Measure
13:42:43 Finite_Fields: theory HOL-Analysis.Multivariate_Analysis
13:42:43 Finite_Fields: theory HOL-Analysis.Infinite_Set_Sum
13:42:46 Finite_Fields: theory HOL-Real_Asymp.Real_Asymp
13:42:46 Finite_Fields: theory HOL-Analysis.Henstock_Kurzweil_Integration
13:42:51 Finite_Fields: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
13:42:51 Finite_Fields: theory HOL-Analysis.Integral_Test
13:42:51 Finite_Fields: theory HOL-Analysis.Kronecker_Approximation_Theorem
13:42:53 Finite_Fields: theory HOL-Analysis.Further_Topology
13:42:53 Finite_Fields: theory HOL-Analysis.Gamma_Function
13:42:53 Finite_Fields: theory HOL-Analysis.Improper_Integral
13:42:53 Finite_Fields: theory HOL-Analysis.Interval_Integral
13:42:53 Finite_Fields: theory HOL-Analysis.Vitali_Covering_Theorem
13:42:57 Finite_Fields: theory HOL-Analysis.Equivalence_Measurable_On_Borel
13:42:58 Finite_Fields: theory HOL-Analysis.Lebesgue_Integral_Substitution
13:42:59 Finite_Fields: theory HOL-Analysis.Change_Of_Vars
13:43:01 Finite_Fields: theory HOL-Analysis.Simplex_Content
13:43:02 Finite_Fields: theory HOL-Analysis.Jordan_Curve
13:43:03 Finite_Fields: theory HOL-Analysis.Ball_Volume
13:43:03 Finite_Fields: theory HOL-Analysis.Analysis
13:43:05 Finite_Fields: theory Dirichlet_Series.Euler_Products
13:43:05 Finite_Fields: theory Dirichlet_Series.Partial_Summation
13:43:05 Finite_Fields: theory HOL-Complex_Analysis.Contour_Integration
13:43:05 Finite_Fields: theory HOL-Probability.Discrete_Topology
13:43:05 Finite_Fields: theory HOL-Probability.Essential_Supremum
13:43:05 Finite_Fields: theory HOL-Probability.Probability_Measure
13:43:05 Finite_Fields: theory HOL-Probability.Stopping_Time
13:43:05 Finite_Fields: theory HOL-Probability.Tree_Space
13:43:06 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
13:43:07 Finite_Fields: theory HOL-Complex_Analysis.Winding_Numbers
13:43:08 Finite_Fields: theory HOL-Probability.Conditional_Expectation
13:43:08 Finite_Fields: theory HOL-Probability.Distribution_Functions
13:43:08 Finite_Fields: theory HOL-Probability.Giry_Monad
13:43:08 Finite_Fields: theory HOL-Probability.Weak_Convergence
13:43:08 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
13:43:09 Finite_Fields: theory HOL-Probability.Helly_Selection
13:43:10 Finite_Fields: theory HOL-Complex_Analysis.Conformal_Mappings
13:43:11 Finite_Fields: theory HOL-Probability.Probability_Mass_Function
13:43:11 Finite_Fields: theory HOL-Probability.Projective_Family
13:43:11 Finite_Fields: theory HOL-Complex_Analysis.Complex_Singularities
13:43:11 Finite_Fields: theory HOL-Complex_Analysis.Great_Picard
13:43:12 Finite_Fields: theory HOL-Probability.Infinite_Product_Measure
13:43:12 Finite_Fields: theory HOL-Complex_Analysis.Riemann_Mapping
13:43:15 Finite_Fields: theory HOL-Probability.Independent_Family
13:43:15 Finite_Fields: theory HOL-Probability.Projective_Limit
13:43:15 Finite_Fields: theory HOL-Probability.Stream_Space
13:43:15 Finite_Fields: theory HOL-Complex_Analysis.Complex_Residues
13:43:15 Finite_Fields: theory HOL-Complex_Analysis.Residue_Theorem
13:43:16 Finite_Fields: theory Finite_Fields.Finite_Fields_More_PMF
13:43:16 Finite_Fields: theory HOL-Complex_Analysis.Laurent_Convergence
13:43:16 Finite_Fields: theory HOL-Probability.PMF_Impl
13:43:16 Finite_Fields: theory HOL-Probability.Random_Permutations
13:43:16 Finite_Fields: theory HOL-Probability.SPMF
13:43:16 Finite_Fields: theory HOL-Probability.Convolution
13:43:17 Finite_Fields: theory HOL-Probability.Information
13:43:17 Finite_Fields: theory HOL-Probability.Product_PMF
13:43:18 Finite_Fields: theory HOL-Probability.Hoeffding
13:43:19 Finite_Fields: theory HOL-Probability.Distributions
13:43:20 Finite_Fields: theory HOL-Complex_Analysis.Meromorphic
13:43:21 Finite_Fields: theory HOL-Complex_Analysis.Weierstrass_Factorization
13:43:21 Finite_Fields: theory HOL-Probability.Characteristic_Functions
13:43:21 Finite_Fields: theory HOL-Probability.Sinc_Integral
13:43:22 Finite_Fields: theory HOL-Complex_Analysis.Complex_Analysis
13:43:22 Finite_Fields: theory HOL-Probability.Levy
13:43:22 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series_Analysis
13:43:22 Finite_Fields: theory HOL-Probability.Central_Limit_Theorem
13:43:22 Finite_Fields: theory HOL-Probability.Probability
13:43:26 Finite_Fields: theory Executable_Randomized_Algorithms.Coin_Space
13:43:26 Finite_Fields: theory MFMC_Countable.MFMC_Misc
13:43:27 Finite_Fields: theory MFMC_Countable.Matrix_For_Marginals
13:43:28 Finite_Fields: theory Zeta_Function.Zeta_Library
13:43:28 Finite_Fields: theory MFMC_Countable.Rel_PMF_Characterisation
13:43:28 Finite_Fields: theory Probabilistic_While.While_SPMF
13:43:29 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
13:43:33 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm
13:43:34 Finite_Fields: theory Finite_Fields.Find_Irreducible_Poly
13:54:23 Preparing Finite_Fields/document ...
13:54:35 Finished Finite_Fields/document (0:00:12 elapsed time)
13:54:35 Preparing Finite_Fields/outline ...
13:54:40 Finished Finite_Fields/outline (0:00:04 elapsed time)
13:54:41 Timing Finite_Fields (8 threads, 738.569s elapsed time, 5093.044s cpu time, 488.381s GC time, factor 6.90)
13:54:41 Finished Finite_Fields (0:12:26 elapsed time, 1:25:25 cpu time, factor 6.87)
13:54:41 Building Subresultants (on hpcisabelle/2) ...
13:54:44 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
13:54:44 Subresultants: theory Subresultants.Coeff_Int
13:54:44 Subresultants: theory Subresultants.Dichotomous_Lazard
13:54:44 Subresultants: theory Subresultants.More_Homomorphisms
13:54:44 Subresultants: theory Subresultants.Resultant_Prelim
13:54:44 Subresultants: theory Subresultants.Binary_Exponentiation
13:54:45 Subresultants: theory Subresultants.Subresultant
13:54:51 Subresultants: theory Subresultants.Subresultant_Gcd
13:55:57 Preparing Subresultants/document ...
13:56:04 Finished Subresultants/document (0:00:06 elapsed time)
13:56:04 Preparing Subresultants/outline ...
13:56:08 Finished Subresultants/outline (0:00:03 elapsed time)
13:56:08 Timing Subresultants (8 threads, 55.489s elapsed time, 273.890s cpu time, 2.463s GC time, factor 4.94)
13:56:08 Finished Subresultants (0:01:15 elapsed time, 0:05:12 cpu time, factor 4.11)
13:56:08 Building HOL-Proofs (on hpcisabelle/3) ...
13:56:10 HOL-Proofs: theory Tools.Code_Generator
13:56:16 HOL-Proofs: theory HOL.HOL
13:56:22 HOL-Proofs: theory HOL.Ctr_Sugar
13:56:22 HOL-Proofs: theory HOL.Argo
13:56:22 HOL-Proofs: theory HOL.Orderings
13:56:27 HOL-Proofs: theory HOL.Groups
13:56:28 HOL-Proofs: theory HOL.SAT
13:56:30 HOL-Proofs: theory HOL.Lattices
13:56:34 HOL-Proofs: theory HOL.Boolean_Algebras
13:56:35 HOL-Proofs: theory HOL.Set
13:56:40 HOL-Proofs: theory HOL.Typedef
13:56:40 HOL-Proofs: theory HOL.Fun
13:56:44 HOL-Proofs: theory HOL.Rings
13:56:44 HOL-Proofs: theory HOL.Complete_Lattices
13:56:51 HOL-Proofs: theory HOL.Inductive
13:56:55 HOL-Proofs: theory HOL.Product_Type
13:56:55 HOL-Proofs: theory HOL.Sum_Type
13:56:58 HOL-Proofs: theory HOL.Complete_Partial_Order
13:57:09 HOL-Proofs: theory HOL.Nat
13:57:14 HOL-Proofs: theory HOL.Meson
13:57:14 HOL-Proofs: theory HOL.Fields
13:57:24 HOL-Proofs: theory HOL.Relation
13:57:28 HOL-Proofs: theory HOL.Finite_Set
13:57:54 HOL-Proofs: theory HOL.Transitive_Closure
13:58:01 HOL-Proofs: theory HOL.Wellfounded
13:58:05 HOL-Proofs: theory HOL.Fun_Def_Base
13:58:05 HOL-Proofs: theory HOL.Wfrec
13:58:05 HOL-Proofs: theory HOL.Hilbert_Choice
13:58:05 HOL-Proofs: theory HOL.Order_Relation
13:58:07 HOL-Proofs: theory HOL.BNF_Wellorder_Relation
13:58:10 HOL-Proofs: theory HOL.Zorn
13:58:10 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
13:58:10 HOL-Proofs: theory HOL.ATP
13:58:15 HOL-Proofs: theory HOL.Metis
13:58:17 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
13:58:22 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
13:58:28 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
13:58:31 HOL-Proofs: theory HOL.BNF_Def
13:58:36 HOL-Proofs: theory HOL.BNF_Composition
13:58:36 HOL-Proofs: theory HOL.Basic_BNFs
13:58:37 HOL-Proofs: theory HOL.BNF_Fixpoint_Base
13:58:43 HOL-Proofs: theory HOL.BNF_Least_Fixpoint
13:58:50 HOL-Proofs: theory HOL.Basic_BNF_LFPs
13:58:50 HOL-Proofs: theory HOL.Equiv_Relations
13:58:50 HOL-Proofs: theory HOL.Transfer
13:58:53 HOL-Proofs: theory HOL.Num
13:58:54 HOL-Proofs: theory HOL.Lifting
13:58:59 HOL-Proofs: theory HOL.Power
13:58:59 HOL-Proofs: theory HOL.Option
13:58:59 HOL-Proofs: theory HOL.Quotient
13:59:01 HOL-Proofs: theory HOL.Extraction
13:59:01 HOL-Proofs: theory HOL.Partial_Function
13:59:03 HOL-Proofs: theory HOL.Fun_Def
13:59:06 HOL-Proofs: theory HOL.Groups_Big
13:59:17 HOL-Proofs: theory HOL.Int
13:59:17 HOL-Proofs: theory HOL.Lifting_Set
13:59:17 HOL-Proofs: theory HOL.Lattices_Big
13:59:31 HOL-Proofs: theory HOL.Euclidean_Rings
14:00:00 HOL-Proofs: theory HOL.Parity
14:00:18 HOL-Proofs: theory HOL.Divides
14:00:18 HOL-Proofs: theory HOL.Numeral_Simprocs
14:00:18 HOL-Proofs: theory HOL.Set_Interval
14:00:19 HOL-Proofs: theory HOL.SMT
14:00:19 HOL-Proofs: theory HOL.Semiring_Normalization
14:00:24 HOL-Proofs: theory HOL.Groebner_Basis
14:00:47 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
14:00:47 HOL-Proofs: theory HOL.Presburger
14:00:47 HOL-Proofs: theory HOL.Filter
14:01:06 HOL-Proofs: theory HOL.Sledgehammer
14:01:11 HOL-Proofs: theory HOL.List
14:02:50 HOL-Proofs: theory HOL.Groups_List
14:02:50 HOL-Proofs: theory HOL.Map
14:02:57 HOL-Proofs: theory HOL.Bit_Operations
14:02:57 HOL-Proofs: theory HOL.Enum
14:02:57 HOL-Proofs: theory HOL.Factorial
14:03:00 HOL-Proofs: theory HOL.Binomial
14:03:58 HOL-Proofs: theory HOL.Code_Numeral
14:04:13 HOL-Proofs: theory HOL.String
14:04:13 HOL-Proofs: theory HOL.GCD
14:04:13 HOL-Proofs: theory HOL.Random
14:04:29 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
14:04:29 HOL-Proofs: theory HOL.Typerep
14:04:29 HOL-Proofs: theory HOL.Predicate
14:04:32 HOL-Proofs: theory HOL.Lazy_Sequence
14:04:33 HOL-Proofs: theory HOL.Limited_Sequence
14:04:34 HOL-Proofs: theory HOL.Code_Evaluation
14:04:36 HOL-Proofs: theory HOL.Quickcheck_Random
14:04:39 HOL-Proofs: theory HOL.Quickcheck_Narrowing
14:04:39 HOL-Proofs: theory HOL.Quickcheck_Exhaustive
14:04:39 HOL-Proofs: theory HOL.Random_Pred
14:04:40 HOL-Proofs: theory HOL.Random_Sequence
14:04:44 HOL-Proofs: theory HOL.Record
14:04:44 HOL-Proofs: theory HOL.Predicate_Compile
14:04:48 HOL-Proofs: theory HOL.Nitpick
14:04:50 HOL-Proofs: theory HOL.Mirabelle
14:04:57 HOL-Proofs: theory HOL.Nunchaku
14:04:59 HOL-Proofs: theory Main
14:05:00 HOL-Proofs: theory HOL-Library.Realizers
14:07:12 Timing HOL-Proofs (8 threads, 536.876s elapsed time, 947.653s cpu time, 136.710s GC time, factor 1.77)
14:07:12 Finished HOL-Proofs (0:10:50 elapsed time, 0:20:58 cpu time, factor 1.93)
14:07:12 Building Syntax_Independent_Logic (on hpcisabelle/4) ...
14:07:14 Syntax_Independent_Logic: theory HOL-Eisbach.Eisbach
14:07:15 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Prelim
14:07:19 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax
14:07:23 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction
14:07:23 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax_Arith
14:07:27 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Natural_Deduction
14:07:27 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Standard_Model
14:07:58 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Pseudo_Term
14:07:58 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction_Q
14:10:20 Preparing Syntax_Independent_Logic/document ...
14:10:31 Finished Syntax_Independent_Logic/document (0:00:11 elapsed time)
14:10:31 Preparing Syntax_Independent_Logic/outline ...
14:10:38 Finished Syntax_Independent_Logic/outline (0:00:06 elapsed time)
14:10:38 Timing Syntax_Independent_Logic (8 threads, 173.821s elapsed time, 963.661s cpu time, 7.597s GC time, factor 5.54)
14:10:38 Finished Syntax_Independent_Logic (0:03:07 elapsed time, 0:16:31 cpu time, factor 5.30)
14:10:38 Building IP_Addresses (on hpcisabelle/5) ...
14:10:39 IP_Addresses: theory HOL-Library.Infinite_Set
14:10:39 IP_Addresses: theory HOL-Library.Cancellation
14:10:39 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
14:10:39 IP_Addresses: theory HOL-Library.Option_ord
14:10:39 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
14:10:41 IP_Addresses: theory HOL-Library.Multiset
14:10:47 IP_Addresses: theory HOL-ex.Quicksort
14:10:48 IP_Addresses: theory Automatic_Refinement.Misc
14:10:56 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
14:10:56 IP_Addresses: theory IP_Addresses.Hs_Compat
14:10:56 IP_Addresses: theory HOL-Library.Product_Lexorder
14:10:56 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
14:10:56 IP_Addresses: theory IP_Addresses.WordInterval
14:10:56 IP_Addresses: theory HOL-Library.Code_Target_Nat
14:10:56 IP_Addresses: theory IP_Addresses.Lib_List_toString
14:10:56 IP_Addresses: theory IP_Addresses.Lib_Word_toString
14:11:01 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
14:11:01 IP_Addresses: theory IP_Addresses.IP_Address
14:11:06 IP_Addresses: theory IP_Addresses.IPv4
14:11:07 IP_Addresses: theory IP_Addresses.Prefix_Match
14:11:08 IP_Addresses: theory IP_Addresses.IPv6
14:11:08 IP_Addresses: theory IP_Addresses.CIDR_Split
14:12:04 IP_Addresses: theory IP_Addresses.IP_Address_Parser
14:12:04 IP_Addresses: theory IP_Addresses.IP_Address_toString
14:12:05 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
14:15:19 Preparing IP_Addresses/document ...
14:15:23 Finished IP_Addresses/document (0:00:03 elapsed time)
14:15:23 Preparing IP_Addresses/outline ...
14:15:26 Finished IP_Addresses/outline (0:00:02 elapsed time)
14:15:26 Timing IP_Addresses (8 threads, 264.777s elapsed time, 875.290s cpu time, 32.378s GC time, factor 3.31)
14:15:26 Finished IP_Addresses (0:04:40 elapsed time, 0:15:07 cpu time, factor 3.24)
14:15:26 Running Padic_Field (on hpcisabelle/6) ...
14:15:29 Padic_Field: theory Padic_Field.Cring_Multivariable_Poly
14:15:29 Padic_Field: theory Localization_Ring.Localization
14:15:29 Padic_Field: theory Padic_Field.Generated_Boolean_Algebra
14:15:29 Padic_Field: theory Padic_Field.Indices
14:15:31 Padic_Field: theory Padic_Field.Fraction_Field
14:15:41 Padic_Field: theory Padic_Field.Padic_Fields
14:16:10 Padic_Field: theory Padic_Field.Ring_Powers
14:16:33 Padic_Field: theory Padic_Field.Padic_Field_Polynomials
14:16:33 Padic_Field: theory Padic_Field.Padic_Field_Topology
14:18:58 Padic_Field: theory Padic_Field.Padic_Field_Powers
14:21:12 Padic_Field: theory Padic_Field.Padic_Semialgebraic_Function_Ring
14:25:55 Preparing Padic_Field/document ...
14:27:08 Finished Padic_Field/document (0:01:13 elapsed time)
14:27:08 Preparing Padic_Field/outline ...
14:27:30 Finished Padic_Field/outline (0:00:22 elapsed time)
14:27:31 Timing Padic_Field (8 threads, 619.183s elapsed time, 1537.743s cpu time, 146.617s GC time, factor 2.48)
14:27:31 Finished Padic_Field (0:10:24 elapsed time, 0:25:52 cpu time, factor 2.49)
14:27:31 Building Berlekamp_Zassenhaus (on hpcisabelle/7) ...
14:27:34 Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
14:27:34 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
14:27:34 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
14:27:34 Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
14:27:34 Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
14:27:34 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
14:27:34 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
14:27:34 Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
14:27:35 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
14:27:35 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
14:27:35 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
14:27:35 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
14:27:35 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
14:27:35 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
14:27:35 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
14:27:35 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
14:27:36 Berlekamp_Zassenhaus: theory Matrix.Utility
14:27:36 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
14:27:36 Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
14:27:36 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
14:27:36 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
14:27:37 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
14:27:37 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
14:27:37 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
14:27:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
14:27:37 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
14:27:37 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
14:27:38 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
14:27:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
14:27:38 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
14:27:38 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
14:27:38 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
14:27:38 Berlekamp_Zassenhaus: theory Show.Show_Poly
14:27:38 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
14:27:39 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
14:27:39 Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
14:27:39 Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
14:27:39 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
14:27:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
14:27:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
14:27:40 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
14:27:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
14:27:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
14:27:40 Berlekamp_Zassenhaus: theory Word_Lib.More_Word
14:27:41 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
14:27:41 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
14:27:41 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
14:27:43 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
14:27:43 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
14:27:43 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
14:27:43 Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
14:27:44 Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
14:27:45 Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
14:27:45 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
14:27:46 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
14:27:46 Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
14:27:48 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
14:27:51 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
14:27:54 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
14:27:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
14:27:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
14:28:00 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
14:28:00 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
14:28:00 Berlekamp_Zassenhaus: theory Native_Word.Uint32
14:28:01 Berlekamp_Zassenhaus: theory Native_Word.Uint64
14:28:04 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
14:28:09 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
14:28:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
14:28:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
14:28:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
14:28:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
14:28:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
14:28:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
14:28:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
14:28:15 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
14:28:17 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
14:28:19 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
14:28:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
14:28:21 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
14:28:26 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
14:28:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
14:28:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
14:28:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorization_External_Interface
14:30:31 Preparing Berlekamp_Zassenhaus/document ...
14:30:56 Finished Berlekamp_Zassenhaus/document (0:00:25 elapsed time)
14:30:56 Preparing Berlekamp_Zassenhaus/outline ...
14:31:07 Finished Berlekamp_Zassenhaus/outline (0:00:10 elapsed time)
14:31:07 Timing Berlekamp_Zassenhaus (8 threads, 142.837s elapsed time, 849.361s cpu time, 51.950s GC time, factor 5.95)
14:31:07 Finished Berlekamp_Zassenhaus (0:02:57 elapsed time, 0:15:23 cpu time, factor 5.21)
14:31:07 Building CakeML (on hpcisabelle/0) ...
14:31:09 CakeML: theory CakeML.Doc_Generated
14:31:09 CakeML: theory HOL-Eisbach.Eisbach
14:31:09 CakeML: theory CakeML.Doc_Proofs
14:31:09 CakeML: theory Deriving.Derive_Manager
14:31:09 CakeML: theory Deriving.Generator_Aux
14:31:09 CakeML: theory HOL-Library.Case_Converter
14:31:09 CakeML: theory HOL-Library.Complete_Partial_Order2
14:31:09 CakeML: theory HOL-Library.Datatype_Records
14:31:09 CakeML: theory HOL-Library.Infinite_Set
14:31:09 CakeML: theory HOL-Library.Nat_Bijection
14:31:09 CakeML: theory HOL-Library.Old_Datatype
14:31:10 CakeML: theory Word_Lib.Signed_Words
14:31:10 CakeML: theory HOL-Library.Simps_Case_Conv
14:31:10 CakeML: theory Word_Lib.Type_Syntax
14:31:11 CakeML: theory Word_Lib.Word_Names
14:31:11 CakeML: theory Word_Lib.Word_Syntax
14:31:11 CakeML: theory HOL-Library.Signed_Division
14:31:11 CakeML: theory HOL-Library.Lattice_Algebras
14:31:11 CakeML: theory HOL-Library.Log_Nat
14:31:11 CakeML: theory Show.Show
14:31:11 CakeML: theory HOL-Library.Countable
14:31:11 CakeML: theory Word_Lib.Enumeration
14:31:11 CakeML: theory HOL-Eisbach.Eisbach_Tools
14:31:11 CakeML: theory Word_Lib.Many_More
14:31:12 CakeML: theory Word_Lib.Rsplit
14:31:12 CakeML: theory Word_Lib.Word_EqI
14:31:12 CakeML: theory Word_Lib.Enumeration_Word
14:31:12 CakeML: theory Word_Lib.More_Misc
14:31:12 CakeML: theory Word_Lib.Signed_Division_Word
14:31:12 CakeML: theory CakeML.Namespace
14:31:13 CakeML: theory Show.Show_Instances
14:31:13 CakeML: theory CakeML.Tokens
14:31:13 CakeML: theory HOL-Library.Countable_Set
14:31:13 CakeML: theory HOL-Library.Countable_Complete_Lattices
14:31:14 CakeML: theory Word_Lib.Boolean_Inequalities
14:31:16 CakeML: theory HOL-Library.Order_Continuity
14:31:17 CakeML: theory HOL-Library.Float
14:31:17 CakeML: theory Word_Lib.Word_Lemmas
14:31:17 CakeML: theory HOL-Library.Extended_Nat
14:31:17 CakeML: theory CakeML.NamespaceAuxiliary
14:31:19 CakeML: theory Coinductive.Coinductive_Nat
14:31:20 CakeML: theory Coinductive.Coinductive_List
14:31:20 CakeML: theory IEEE_Floating_Point.IEEE
14:31:20 CakeML: theory Word_Lib.More_Word_Operations
14:31:22 CakeML: theory Word_Lib.Word_64
14:31:24 CakeML: theory IEEE_Floating_Point.FP64
14:31:28 CakeML: theory CakeML.Lib
14:31:32 CakeML: theory CakeML.LibAuxiliary
14:31:32 CakeML: theory CakeML.Ffi
14:31:32 CakeML: theory CakeML.FpSem
14:31:36 CakeML: theory CakeML.Ast
14:31:41 CakeML: theory CakeML.SimpleIO
14:32:08 CakeML: theory CakeML.CakeML_Compiler
14:32:08 CakeML: theory CakeML.AstAuxiliary
14:32:08 CakeML: theory CakeML.SemanticPrimitives
14:32:42 CakeML: theory CakeML.Evaluate
14:32:42 CakeML: theory CakeML.CakeML_Quickcheck
14:32:42 CakeML: theory CakeML.SmallStep
14:32:42 CakeML: theory CakeML.TypeSystem
14:32:42 CakeML: theory CakeML.SemanticPrimitivesAuxiliary
14:32:48 CakeML: theory CakeML.BigStep
14:32:49 CakeML: theory CakeML.PrimTypes
14:32:54 CakeML: theory CakeML.BigSmallInvariants
14:32:54 CakeML: theory CakeML.Semantic_Extras
14:33:05 CakeML: theory CakeML.TypeSystemAuxiliary
14:33:09 CakeML: theory CakeML.Big_Step_Determ
14:33:09 CakeML: theory CakeML.Big_Step_Total
14:33:09 CakeML: theory CakeML.Big_Step_Clocked
14:33:09 CakeML: theory CakeML.Big_Step_Unclocked
14:33:10 CakeML: theory CakeML.Evaluate_Termination
14:33:10 CakeML: theory CakeML.Matching
14:33:10 CakeML: theory CakeML.Evaluate_Clock
14:33:11 CakeML: theory CakeML.Big_Step_Fun_Equiv
14:33:11 CakeML: theory CakeML.Evaluate_Single
14:33:13 CakeML: theory CakeML.Big_Step_Unclocked_Single
14:33:21 CakeML: theory CakeML.CakeML_Code
14:34:31 CakeML: theory CakeML.Compiler_Test
14:34:39 CakeML: theory CakeML.Code_Test_Haskell
14:35:35 Preparing CakeML/document ...
14:35:41 Finished CakeML/document (0:00:06 elapsed time)
14:35:41 Preparing CakeML/outline ...
14:35:46 Finished CakeML/outline (0:00:04 elapsed time)
14:35:46 Timing CakeML (8 threads, 230.834s elapsed time, 1165.801s cpu time, 97.628s GC time, factor 5.05)
14:35:46 Finished CakeML (0:04:25 elapsed time, 0:20:46 cpu time, factor 4.70)
14:35:47 Building Simpl (on hpcisabelle/1) ...
14:35:48 Simpl: theory HOL-Library.Cancellation
14:35:48 Simpl: theory HOL-Library.Old_Recdef
14:35:48 Simpl: theory HOL-Library.LaTeXsugar
14:35:48 Simpl: theory Simpl.Simpl_Heap
14:35:48 Simpl: theory HOL-Statespace.DistinctTreeProver
14:35:48 Simpl: theory Simpl.HeapList
14:35:49 Simpl: theory HOL-Library.Multiset
14:35:50 Simpl: theory Simpl.Generalise
14:35:50 Simpl: theory HOL-Statespace.StateFun
14:35:51 Simpl: theory Simpl.Language
14:35:51 Simpl: theory HOL-Statespace.StateSpaceLocale
14:35:52 Simpl: theory HOL-Statespace.StateSpaceSyntax
14:35:59 Simpl: theory Simpl.Semantic
14:36:04 Simpl: theory Simpl.HoarePartialDef
14:36:04 Simpl: theory Simpl.Termination
14:36:05 Simpl: theory Simpl.HoarePartialProps
14:36:06 Simpl: theory Simpl.HoareTotalDef
14:36:06 Simpl: theory Simpl.SmallStep
14:36:07 Simpl: theory Simpl.HoarePartial
14:36:08 Simpl: theory Simpl.AlternativeSmallStep
14:36:09 Simpl: theory Simpl.HoareTotalProps
14:36:11 Simpl: theory Simpl.Compose
14:36:11 Simpl: theory Simpl.HoareTotal
14:36:14 Simpl: theory Simpl.Hoare
14:36:15 Simpl: theory Simpl.Closure
14:36:15 Simpl: theory Simpl.StateSpace
14:36:15 Simpl: theory Simpl.Vcg
14:36:24 Simpl: theory Simpl.ProcParEx
14:36:24 Simpl: theory Simpl.ProcParExSP
14:36:24 Simpl: theory Simpl.XVcg
14:36:24 Simpl: theory Simpl.ClosureEx
14:36:24 Simpl: theory Simpl.ComposeEx
14:36:24 Simpl: theory Simpl.XVcgEx
14:36:24 Simpl: theory Simpl.Quicksort
14:36:24 Simpl: theory Simpl.SyntaxTest
14:36:24 Simpl: theory Simpl.UserGuide
14:36:24 Simpl: theory Simpl.VcgEx
14:36:24 Simpl: theory Simpl.VcgExSP
14:36:24 Simpl: theory Simpl.VcgExTotal
14:36:29 Simpl: theory Simpl.Simpl
14:37:06 Preparing Simpl/document ...
14:37:42 Finished Simpl/document (0:00:35 elapsed time)
14:37:42 Preparing Simpl/outline ...
14:37:59 Finished Simpl/outline (0:00:17 elapsed time)
14:37:59 Timing Simpl (8 threads, 55.653s elapsed time, 354.190s cpu time, 20.610s GC time, factor 6.36)
14:37:59 Finished Simpl (0:01:15 elapsed time, 0:06:38 cpu time, factor 5.27)
14:37:59 Running Native_Word (on hpcisabelle/2) ...
14:38:01 Native_Word: theory HOL-Library.Adhoc_Overloading
14:38:01 Native_Word: theory HOL-Library.Nat_Bijection
14:38:01 Native_Word: theory HOL-Library.Old_Datatype
14:38:01 Native_Word: theory HOL-Library.Code_Target_Int
14:38:01 Native_Word: theory Native_Word.Code_Target_Word_Base
14:38:01 Native_Word: theory Native_Word.Code_Int_Integer_Conversion
14:38:01 Native_Word: theory HOL-Library.Code_Test
14:38:01 Native_Word: theory Native_Word.Code_Target_Integer_Bit
14:38:01 Native_Word: theory HOL-Library.Monad_Syntax
14:38:01 Native_Word: theory Native_Word.Word_Type_Copies
14:38:02 Native_Word: theory HOL-Library.Countable
14:38:03 Native_Word: theory HOL-Imperative_HOL.Heap
14:38:05 Native_Word: theory HOL-Imperative_HOL.Heap_Monad
14:38:07 Native_Word: theory Native_Word.Native_Word_Imperative_HOL
14:38:15 Native_Word: theory Native_Word.Code_Target_Int_Bit
14:38:15 Native_Word: theory Native_Word.Uint16
14:38:15 Native_Word: theory Native_Word.Uint
14:38:15 Native_Word: theory Native_Word.Uint32
14:38:15 Native_Word: theory Native_Word.Uint64
14:38:15 Native_Word: theory Native_Word.Uint8
14:38:18 Native_Word: theory Native_Word.Native_Cast
14:38:19 Native_Word: theory Native_Word.Native_Cast_Uint
14:38:19 Native_Word: theory Native_Word.Native_Word_Test
14:46:14 Native_Word: theory Native_Word.Native_Word_Test_Emu
14:46:14 Native_Word: theory Native_Word.Native_Word_Test_PolyML
14:46:14 Native_Word: theory Native_Word.Native_Word_Test_PolyML64
14:46:14 Native_Word: theory Native_Word.Native_Word_Test_Scala
14:46:36 Native_Word: theory Native_Word.Native_Word_Test_PolyML2
14:46:41 Native_Word: theory Native_Word.Native_Word_Test_GHC
14:46:49 Native_Word: theory Native_Word.Native_Word_Test_MLton2
14:46:49 Native_Word: theory Native_Word.Native_Word_Test_MLton
14:47:00 Native_Word: theory Native_Word.Native_Word_Test_OCaml2
14:47:00 Native_Word: theory Native_Word.Native_Word_Test_OCaml
14:47:08 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2
14:47:08 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ
14:47:17 Native_Word: theory Native_Word.Uint_Userguide
14:47:26 Preparing Native_Word/document ...
14:47:34 Finished Native_Word/document (0:00:08 elapsed time)
14:47:34 Preparing Native_Word/outline ...
14:47:41 Finished Native_Word/outline (0:00:07 elapsed time)
14:47:42 Timing Native_Word (8 threads, 563.253s elapsed time, 626.729s cpu time, 26.835s GC time, factor 1.11)
14:47:42 Finished Native_Word (0:09:26 elapsed time, 0:10:34 cpu time, factor 1.12)
14:47:42 Building Category3 (on hpcisabelle/3) ...
14:47:44 Category3: theory HOL-Cardinals.Fun_More
14:47:44 Category3: theory HOL-Cardinals.Order_Relation_More
14:47:44 Category3: theory Category3.Category
14:47:44 Category3: theory HOL-Cardinals.Order_Union
14:47:44 Category3: theory HereditarilyFinite.HF
14:47:44 Category3: theory HOL-Cardinals.Wellorder_Extension
14:47:45 Category3: theory HOL-Cardinals.Wellfounded_More
14:47:45 Category3: theory HOL-Cardinals.Wellorder_Relation
14:47:45 Category3: theory Category3.ConcreteCategory
14:47:45 Category3: theory Category3.DiscreteCategory
14:47:45 Category3: theory Category3.EpiMonoIso
14:47:45 Category3: theory HOL-Cardinals.Wellorder_Embedding
14:47:45 Category3: theory Category3.DualCategory
14:47:45 Category3: theory Category3.InitialTerminal
14:47:45 Category3: theory HOL-Cardinals.Wellorder_Constructions
14:47:45 Category3: theory Category3.ProductCategory
14:47:46 Category3: theory HOL-Cardinals.Cardinal_Order_Relation
14:47:46 Category3: theory HOL-Cardinals.Ordinal_Arithmetic
14:47:47 Category3: theory Category3.FreeCategory
14:47:47 Category3: theory Category3.Functor
14:47:47 Category3: theory HOL-Cardinals.Cardinal_Arithmetic
14:47:48 Category3: theory HOL-Cardinals.Cardinals
14:47:48 Category3: theory ZFC_in_HOL.ZFC_Library
14:47:49 Category3: theory ZFC_in_HOL.ZFC_in_HOL
14:47:50 Category3: theory ZFC_in_HOL.ZFC_Cardinals
14:47:53 Category3: theory Category3.NaturalTransformation
14:47:54 Category3: theory Category3.Subcategory
14:47:56 Category3: theory Category3.SetCategory
14:47:57 Category3: theory Category3.BinaryFunctor
14:48:00 Category3: theory Category3.SetCat
14:48:04 Category3: theory Category3.FunctorCategory
14:48:18 Category3: theory Category3.Yoneda
14:48:45 Category3: theory Category3.Adjunction
14:49:40 Category3: theory Category3.EquivalenceOfCategories
14:49:40 Category3: theory Category3.Limit
14:51:26 Category3: theory Category3.CategoryWithPullbacks
14:51:28 Category3: theory Category3.ZFC_SetCat
14:51:42 Category3: theory Category3.CartesianCategory
14:51:42 Category3: theory Category3.ZFC_SetCat_Interp
14:52:03 Category3: theory Category3.CartesianClosedCategory
14:52:04 Category3: theory Category3.CategoryWithFiniteLimits
14:52:05 Category3: theory Category3.HF_SetCat
14:52:09 Category3: theory Category3.HF_SetCat_Interp
14:54:01 Preparing Category3/document ...
14:54:32 Finished Category3/document (0:00:30 elapsed time)
14:54:32 Preparing Category3/outline ...
14:54:43 Finished Category3/outline (0:00:11 elapsed time)
14:54:43 Timing Category3 (8 threads, 341.279s elapsed time, 1937.100s cpu time, 145.202s GC time, factor 5.68)
14:54:43 Finished Category3 (0:06:16 elapsed time, 0:33:40 cpu time, factor 5.37)
14:54:43 Running Automated_Stateful_Protocol_Verification (on hpcisabelle/4) ...
14:54:46 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
14:54:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
14:54:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
14:54:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
14:54:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
14:54:47 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
14:54:48 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
14:54:49 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
14:54:49 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
14:54:50 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
14:54:59 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
14:55:04 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
14:55:34 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
14:56:14 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
15:00:04 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
15:00:05 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
15:00:05 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
15:00:05 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
15:00:05 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
15:00:05 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
15:00:06 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
15:00:06 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
15:00:06 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
15:02:39 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
15:03:38 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
15:04:00 Preparing Automated_Stateful_Protocol_Verification/document ...
15:04:40 Finished Automated_Stateful_Protocol_Verification/document (0:00:39 elapsed time)
15:04:40 Preparing Automated_Stateful_Protocol_Verification/outline ...
15:04:58 Finished Automated_Stateful_Protocol_Verification/outline (0:00:18 elapsed time)
15:04:58 Timing Automated_Stateful_Protocol_Verification (8 threads, 540.711s elapsed time, 2188.608s cpu time, 295.991s GC time, factor 4.05)
15:04:58 Finished Automated_Stateful_Protocol_Verification (0:09:10 elapsed time, 0:37:10 cpu time, factor 4.05)
15:04:58 Building Complex_Bounded_Operators_Dependencies (on hpcisabelle/5) ...
15:05:01 Complex_Bounded_Operators_Dependencies: theory Containers.Extend_Partial_Order
15:05:01 Complex_Bounded_Operators_Dependencies: theory Containers.Equal
15:05:01 Complex_Bounded_Operators_Dependencies: theory Containers.List_Fusion
15:05:01 Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator
15:05:01 Complex_Bounded_Operators_Dependencies: theory Deriving.Derive_Manager
15:05:01 Complex_Bounded_Operators_Dependencies: theory Deriving.Generator_Aux
15:05:01 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Fun_More
15:05:01 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Relation_More
15:05:01 Complex_Bounded_Operators_Dependencies: theory Containers.Closure_Set
15:05:01 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Union
15:05:01 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fraction_Field
15:05:01 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Adhoc_Overloading
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Char_ord
15:05:02 Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Generator
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Extension
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Monad_Syntax
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellfounded_More
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Abstract_Nat
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Relation
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Int
15:05:02 Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Auxiliary
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Nat
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Embedding
15:05:02 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Complemented_Lattices
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Numeral
15:05:03 Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Instances
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Constructions
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Congruence
15:05:03 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Misc
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Function_Algebras
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Library.IArray
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Library.More_List
15:05:03 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare
15:05:03 Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator_Generator
15:05:03 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Normalized_Fraction
15:05:03 Complex_Bounded_Operators_Dependencies: theory Containers.Lexicographic_Order
15:05:04 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Order_Relation
15:05:04 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Ordinal_Arithmetic
15:05:04 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Order
15:05:04 Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Generator
15:05:04 Complex_Bounded_Operators_Dependencies: theory Containers.Set_Linorder
15:05:05 Complex_Bounded_Operators_Dependencies: theory HOL-Library.RBT_Impl
15:05:05 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Generator
15:05:05 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Arithmetic
15:05:05 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Enum
15:05:06 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Eq
15:05:06 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Instances
15:05:06 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinals
15:05:06 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Lattice
15:05:06 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Rewrite
15:05:06 Complex_Bounded_Operators_Dependencies: theory Containers.DList_Set
15:05:06 Complex_Bounded_Operators_Dependencies: theory HOL-Types_To_Sets.Types_To_Sets
15:05:06 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Unsorted
15:05:07 Complex_Bounded_Operators_Dependencies: theory Cauchy.CauchysMeanTheorem
15:05:07 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial
15:05:09 Complex_Bounded_Operators_Dependencies: theory HOL-Examples.Sqrt
15:05:09 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Conjugate
15:05:09 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Complete_Lattice
15:05:09 Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus_Missing
15:05:10 Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus
15:05:10 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
15:05:10 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Group
15:05:10 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom
15:05:10 Complex_Bounded_Operators_Dependencies: theory Show.Show
15:05:10 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Log_Impl
15:05:11 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.NthRoot_Impl
15:05:12 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian
15:05:12 Complex_Bounded_Operators_Dependencies: theory Show.Show_Instances
15:05:13 Complex_Bounded_Operators_Dependencies: theory Real_Impl.Real_Impl
15:05:13 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Coset
15:05:13 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.FiniteProduct
15:05:14 Complex_Bounded_Operators_Dependencies: theory Show.Shows_Literal
15:05:14 Complex_Bounded_Operators_Dependencies: theory VectorSpace.FunctionLemmas
15:05:14 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Ring
15:05:18 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Module
15:05:18 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Ring
15:05:19 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Order
15:05:20 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
15:05:20 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial_Factorial
15:05:21 Complex_Bounded_Operators_Dependencies: theory VectorSpace.RingModuleFacts
15:05:22 Complex_Bounded_Operators_Dependencies: theory VectorSpace.MonoidSums
15:05:22 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Polynomial
15:05:23 Complex_Bounded_Operators_Dependencies: theory VectorSpace.LinearCombinations
15:05:24 Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Order_Polynomial
15:05:24 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom_Poly
15:05:24 Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
15:05:25 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix
15:05:29 Complex_Bounded_Operators_Dependencies: theory VectorSpace.SumSpaces
15:05:30 Complex_Bounded_Operators_Dependencies: theory VectorSpace.VectorSpace
15:05:31 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
15:05:31 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Show_Matrix
15:05:31 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Shows_Literal_Matrix
15:05:33 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Column_Operations
15:05:33 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant
15:05:36 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant_Impl
15:05:36 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Char_Poly
15:05:37 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_VectorSpace
15:05:38 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form
15:05:41 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.VS_Connect
15:05:56 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gram_Schmidt
15:05:56 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Kernel
15:05:58 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Schur_Decomposition
15:06:03 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
15:06:18 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_ext
15:06:18 Complex_Bounded_Operators_Dependencies: theory Deriving.RBT_Comparator_Impl
15:06:28 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Mapping2
15:06:30 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Set2
15:06:32 Complex_Bounded_Operators_Dependencies: theory Containers.Set_Impl
15:06:57 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_IArray_Impl
15:07:00 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
15:07:03 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Impl
15:11:11 Timing Complex_Bounded_Operators_Dependencies (8 threads, 312.026s elapsed time, 2048.517s cpu time, 161.279s GC time, factor 6.57)
15:11:11 Finished Complex_Bounded_Operators_Dependencies (0:06:06 elapsed time, 0:36:20 cpu time, factor 5.94)
15:11:11 Building Projective_Measurements (on hpcisabelle/6) ...
15:11:16 Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
15:11:16 Projective_Measurements: theory Abstract-Rewriting.Seq
15:11:16 Projective_Measurements: theory HOL-Computational_Algebra.Fraction_Field
15:11:16 Projective_Measurements: theory HOL-Algebra.Congruence
15:11:16 Projective_Measurements: theory HOL-Library.More_List
15:11:16 Projective_Measurements: theory HOL-Library.While_Combinator
15:11:16 Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
15:11:16 Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
15:11:16 Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
15:11:16 Projective_Measurements: theory Jordan_Normal_Form.Conjugate
15:11:17 Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
15:11:17 Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
15:11:17 Projective_Measurements: theory Matrix.Utility
15:11:17 Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
15:11:17 Projective_Measurements: theory Regular-Sets.Regular_Set
15:11:17 Projective_Measurements: theory HOL-Algebra.Order
15:11:18 Projective_Measurements: theory HOL-Computational_Algebra.Normalized_Fraction
15:11:18 Projective_Measurements: theory VectorSpace.FunctionLemmas
15:11:19 Projective_Measurements: theory HOL-Algebra.Lattice
15:11:20 Projective_Measurements: theory HOL-Algebra.Complete_Lattice
15:11:21 Projective_Measurements: theory HOL-Algebra.Group
15:11:22 Projective_Measurements: theory Regular-Sets.Regular_Exp
15:11:24 Projective_Measurements: theory HOL-Algebra.Coset
15:11:24 Projective_Measurements: theory HOL-Algebra.FiniteProduct
15:11:25 Projective_Measurements: theory HOL-Algebra.Ring
15:11:26 Projective_Measurements: theory Regular-Sets.NDerivative
15:11:26 Projective_Measurements: theory Regular-Sets.Relation_Interpretation
15:11:29 Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
15:11:29 Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
15:11:30 Projective_Measurements: theory HOL-Algebra.Module
15:11:30 Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
15:11:30 Projective_Measurements: theory Regular-Sets.Equivalence_Checking
15:11:31 Projective_Measurements: theory Regular-Sets.Regexp_Method
15:11:31 Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
15:11:32 Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
15:11:32 Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
15:11:32 Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
15:11:32 Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
15:11:32 Projective_Measurements: theory VectorSpace.RingModuleFacts
15:11:34 Projective_Measurements: theory VectorSpace.MonoidSums
15:11:34 Projective_Measurements: theory Abstract-Rewriting.SN_Orders
15:11:34 Projective_Measurements: theory VectorSpace.LinearCombinations
15:11:36 Projective_Measurements: theory Jordan_Normal_Form.Matrix
15:11:38 Projective_Measurements: theory Matrix.Ordered_Semiring
15:11:39 Projective_Measurements: theory Matrix.Matrix_Legacy
15:11:41 Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
15:11:41 Projective_Measurements: theory VectorSpace.SumSpaces
15:11:42 Projective_Measurements: theory VectorSpace.VectorSpace
15:11:43 Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
15:11:44 Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
15:11:45 Projective_Measurements: theory Jordan_Normal_Form.Determinant
15:11:47 Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
15:11:49 Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
15:11:49 Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
15:11:49 Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
15:11:50 Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
15:11:50 Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
15:11:52 Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
15:11:53 Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
15:11:53 Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
15:11:55 Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
15:12:07 Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
15:12:09 Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
15:12:14 Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
15:12:19 Projective_Measurements: theory QHLProver.Complex_Matrix
15:12:30 Projective_Measurements: theory QHLProver.Gates
15:12:30 Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
15:12:37 Projective_Measurements: theory Projective_Measurements.Projective_Measurements
15:12:38 Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
15:19:52 Preparing Projective_Measurements/document ...
15:19:57 Finished Projective_Measurements/document (0:00:05 elapsed time)
15:19:57 Preparing Projective_Measurements/outline ...
15:20:00 Finished Projective_Measurements/outline (0:00:02 elapsed time)
15:20:00 Timing Projective_Measurements (8 threads, 474.717s elapsed time, 1514.675s cpu time, 57.986s GC time, factor 3.19)
15:20:00 Finished Projective_Measurements (0:08:35 elapsed time, 0:26:47 cpu time, factor 3.12)
15:20:01 Running AutoCorres2 (on hpcisabelle/7) ...
15:20:02 AutoCorres2: theory AutoCorres2.ML_Fun_Cache
15:20:02 AutoCorres2: theory AutoCorres2.MkTermAntiquote
15:20:02 AutoCorres2: theory AutoCorres2.TermPatternAntiquote
15:20:02 AutoCorres2: theory AutoCorres2.Apply_Trace
15:20:02 AutoCorres2: theory HOL-Eisbach.Eisbach
15:20:02 AutoCorres2: theory AutoCorres2.Introduction_AutoCorres2
15:20:02 AutoCorres2: theory AutoCorres2.ML_Infer_Instantiate
15:20:02 AutoCorres2: theory AutoCorres2.ML_Record_Antiquotation
15:20:03 AutoCorres2: theory AutoCorres2.MapExtra
15:20:03 AutoCorres2: theory AutoCorres2.Misc_Antiquotation
15:20:03 AutoCorres2: theory AutoCorres2.MkTermAntiquote_Tests
15:20:03 AutoCorres2: theory AutoCorres2.Named_Rules
15:20:03 AutoCorres2: theory AutoCorres2.Padding
15:20:03 AutoCorres2: theory AutoCorres2.Option_Scanner
15:20:03 AutoCorres2: theory AutoCorres2.Print_Annotated
15:20:03 AutoCorres2: theory AutoCorres2.Apply_Trace_Cmd
15:20:03 AutoCorres2: theory AutoCorres2.StaticFun
15:20:03 AutoCorres2: theory AutoCorres2.AutoCorres_Utils
15:20:03 AutoCorres2: theory AutoCorres2.Subgoal_Methods
15:20:04 AutoCorres2: theory AutoCorres2.Subgoals
15:20:04 AutoCorres2: theory AutoCorres2.Target_Architecture
15:20:04 AutoCorres2: theory AutoCorres2.TermPatternAntiquote_Tests
15:20:04 AutoCorres2: theory AutoCorres2.MapExtraTrans
15:20:04 AutoCorres2: theory AutoCorres2.Tuple_Tools
15:20:04 AutoCorres2: theory HOL-Library.Adhoc_Overloading
15:20:04 AutoCorres2: theory HOL-Library.Code_Abstract_Nat
15:20:04 AutoCorres2: theory HOL-Library.Code_Binary_Nat
15:20:04 AutoCorres2: theory HOL-Library.Monad_Syntax
15:20:04 AutoCorres2: theory HOL-Library.Complete_Partial_Order2
15:20:04 AutoCorres2: theory AutoCorres2.Less_Monad_Syntax
15:20:04 AutoCorres2: theory HOL-Library.Phantom_Type
15:20:05 AutoCorres2: theory HOL-Eisbach.Eisbach_Tools
15:20:05 AutoCorres2: theory AutoCorres2.Tagging
15:20:05 AutoCorres2: theory HOL-Library.Signed_Division
15:20:05 AutoCorres2: theory AutoCorres2.Cong_Tactic
15:20:05 AutoCorres2: theory AutoCorres2.Rule_By_Method
15:20:05 AutoCorres2: theory AutoCorres2.Match_Cterm
15:20:05 AutoCorres2: theory AutoCorres2.Simp_Trace
15:20:05 AutoCorres2: theory AutoCorres2.Basic_Runs_To_VCG
15:20:06 AutoCorres2: theory HOL-Library.Sublist
15:20:06 AutoCorres2: theory HOL-Library.Cardinality
15:20:06 AutoCorres2: theory AutoCorres2.PrettyProgs
15:20:06 AutoCorres2: theory AutoCorres2.Eisbach_Methods
15:20:06 AutoCorres2: theory AutoCorres2.IndirectCalls
15:20:07 AutoCorres2: theory Word_Lib.Enumeration
15:20:07 AutoCorres2: theory Word_Lib.Even_More_List
15:20:07 AutoCorres2: theory Word_Lib.More_Bit_Ring
15:20:07 AutoCorres2: theory Word_Lib.More_Misc
15:20:07 AutoCorres2: theory HOL-Library.Numeral_Type
15:20:08 AutoCorres2: theory AutoCorres2.Runs_To_VCG
15:20:08 AutoCorres2: theory AutoCorres2.Arrays
15:20:08 AutoCorres2: theory HOL-Library.Type_Length
15:20:09 AutoCorres2: theory HOL-Library.Prefix_Order
15:20:09 AutoCorres2: theory Word_Lib.More_Sublist
15:20:09 AutoCorres2: theory Word_Lib.More_Arithmetic
15:20:09 AutoCorres2: theory HOL-Library.Word
15:20:09 AutoCorres2: theory AutoCorres2.Mutual_CCPO_Recursion
15:20:10 AutoCorres2: theory AutoCorres2.Spec_Monad
15:20:16 AutoCorres2: theory AutoCorres2.Synthesize
15:20:21 AutoCorres2: theory Word_Lib.Bit_Comprehension
15:20:21 AutoCorres2: theory Word_Lib.Hex_Words
15:20:21 AutoCorres2: theory Word_Lib.Legacy_Aliases
15:20:21 AutoCorres2: theory Word_Lib.More_Divides
15:20:21 AutoCorres2: theory Word_Lib.Signed_Words
15:20:21 AutoCorres2: theory Word_Lib.Syntax_Bundles
15:20:21 AutoCorres2: theory Word_Lib.Type_Syntax
15:20:21 AutoCorres2: theory Word_Lib.Word_Syntax
15:20:21 AutoCorres2: theory Word_Lib.Signed_Division_Word
15:20:21 AutoCorres2: theory Word_Lib.Norm_Words
15:20:21 AutoCorres2: theory Word_Lib.Word_Names
15:20:22 AutoCorres2: theory Word_Lib.More_Word
15:20:22 AutoCorres2: theory AutoCorres2.Reaches
15:20:23 AutoCorres2: theory Word_Lib.Bit_Comprehension_Int
15:20:24 AutoCorres2: theory Word_Lib.Bit_Shifts_Infix_Syntax
15:20:24 AutoCorres2: theory Word_Lib.Enumeration_Word
15:20:24 AutoCorres2: theory Word_Lib.Least_significant_bit
15:20:24 AutoCorres2: theory Word_Lib.Many_More
15:20:24 AutoCorres2: theory Word_Lib.Strict_part_mono
15:20:24 AutoCorres2: theory Word_Lib.Word_16
15:20:24 AutoCorres2: theory AutoCorres2.Distinct_Prop
15:20:25 AutoCorres2: theory AutoCorres2.Lens
15:20:25 AutoCorres2: theory Word_Lib.Aligned
15:20:25 AutoCorres2: theory Word_Lib.Singleton_Bit_Shifts
15:20:25 AutoCorres2: theory Word_Lib.Most_significant_bit
15:20:25 AutoCorres2: theory Word_Lib.Generic_set_bit
15:20:25 AutoCorres2: theory Word_Lib.Sgn_Abs
15:20:25 AutoCorres2: theory Word_Lib.Next_and_Prev
15:20:25 AutoCorres2: theory Word_Lib.Word_EqI
15:20:26 AutoCorres2: theory Word_Lib.Bits_Int
15:20:29 AutoCorres2: theory Word_Lib.Boolean_Inequalities
15:20:31 AutoCorres2: theory Word_Lib.Rsplit
15:20:31 AutoCorres2: theory Word_Lib.Typedef_Morphisms
15:20:31 AutoCorres2: theory Word_Lib.Reversed_Bit_Lists
15:20:32 AutoCorres2: theory Word_Lib.Word_Lemmas
15:20:35 AutoCorres2: theory Word_Lib.Bitwise
15:20:36 AutoCorres2: theory Word_Lib.Word_8
15:20:36 AutoCorres2: theory Word_Lib.More_Word_Operations
15:20:36 AutoCorres2: theory Word_Lib.Bitwise_Signed
15:20:37 AutoCorres2: theory AutoCorres2.Word_Lemmas_Internal
15:20:37 AutoCorres2: theory Word_Lib.Word_32
15:20:37 AutoCorres2: theory Word_Lib.Word_64
15:20:38 AutoCorres2: theory Word_Lib.Machine_Word_64_Basics
15:20:38 AutoCorres2: theory Word_Lib.Machine_Word_64
15:20:38 AutoCorres2: theory Word_Lib.Machine_Word_32_Basics
15:20:38 AutoCorres2: theory Word_Lib.Word_Lib_Sumo
15:20:38 AutoCorres2: theory Word_Lib.Machine_Word_32
15:20:41 AutoCorres2: theory AutoCorres2.More_Lib
15:20:41 AutoCorres2: theory AutoCorres2.Word_Lemmas_32_Internal
15:20:41 AutoCorres2: theory AutoCorres2.Word_Lemmas_64_Internal
15:20:42 AutoCorres2: theory AutoCorres2.WordSetup
15:20:43 AutoCorres2: theory AutoCorres2.Addr_Type_ARM64
15:20:43 AutoCorres2: theory AutoCorres2.Addr_Type_ARM
15:20:43 AutoCorres2: theory AutoCorres2.Addr_Type_ARM_HYP
15:20:43 AutoCorres2: theory AutoCorres2.Addr_Type_RISCV64
15:20:43 AutoCorres2: theory AutoCorres2.Addr_Type_X64
15:20:44 AutoCorres2: theory AutoCorres2.Addr_Type
15:20:44 AutoCorres2: theory AutoCorres2.NatBitwise
15:20:44 AutoCorres2: theory AutoCorres2.Reader_Monad
15:20:45 AutoCorres2: theory AutoCorres2.CTypesBase
15:20:45 AutoCorres2: theory AutoCorres2.Option_MonadND
15:20:47 AutoCorres2: theory AutoCorres2.CTypesDefs
15:21:02 AutoCorres2: theory AutoCorres2.CTypes
15:21:06 AutoCorres2: theory AutoCorres2.HeapRawState
15:21:06 AutoCorres2: theory AutoCorres2.Vanilla32_Preliminaries
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM64
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_RISCV64
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_X64
15:21:07 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding
15:21:07 AutoCorres2: theory AutoCorres2.Vanilla32
15:21:08 AutoCorres2: theory AutoCorres2.CompoundCTypes
15:21:14 AutoCorres2: theory AutoCorres2.ArraysMemInstance
15:21:16 AutoCorres2: theory AutoCorres2.ArchArraysMemInstance
15:21:18 AutoCorres2: theory AutoCorres2.TypHeap
15:21:26 AutoCorres2: theory AutoCorres2.Separation_UMM
15:21:27 AutoCorres2: theory AutoCorres2.SepCode
15:21:29 AutoCorres2: theory AutoCorres2.SepInv
15:21:31 AutoCorres2: theory AutoCorres2.SepTactic
15:21:31 AutoCorres2: theory AutoCorres2.SepFrame
15:21:33 AutoCorres2: theory AutoCorres2.StructSupport
15:21:34 AutoCorres2: theory AutoCorres2.ArrayAssertion
15:21:35 AutoCorres2: theory AutoCorres2.CProof
15:21:44 AutoCorres2: theory AutoCorres2.CLanguage
15:21:44 AutoCorres2: theory AutoCorres2.Padding_Equivalence
15:21:44 AutoCorres2: theory AutoCorres2.PackedTypes
15:21:51 AutoCorres2: theory AutoCorres2.ModifiesProofs
15:21:54 AutoCorres2: theory AutoCorres2.UMM
15:22:03 AutoCorres2: theory AutoCorres2.CLocals
15:22:06 AutoCorres2: theory AutoCorres2.CTranslationSetup
15:22:35 AutoCorres2: theory AutoCorres2.Array_Selectors
15:22:35 AutoCorres2: theory AutoCorres2.CTranslation
15:22:36 AutoCorres2: theory AutoCorres2.CTranslationInfrastructure
15:22:36 AutoCorres2: theory AutoCorres2.TypHeapLib
15:22:37 AutoCorres2: theory AutoCorres2.AbstractArrays
15:22:37 AutoCorres2: theory AutoCorres2.LemmaBucket_C
15:22:37 AutoCorres2: theory AutoCorres2.AutoCorres_Base
15:22:42 AutoCorres2: theory AutoCorres2.SimplBucket
15:22:42 AutoCorres2: theory AutoCorres2.TypHeapSimple
15:22:42 AutoCorres2: theory AutoCorres2.AutoCorresSimpset
15:22:42 AutoCorres2: theory AutoCorres2.CCorresE
15:22:43 AutoCorres2: theory AutoCorres2.CorresXF
15:22:43 AutoCorres2: theory AutoCorres2.L1Defs
15:22:46 AutoCorres2: theory AutoCorres2.L1Peephole
15:22:46 AutoCorres2: theory AutoCorres2.L1Valid
15:22:46 AutoCorres2: theory AutoCorres2.ExceptionRewrite
15:22:46 AutoCorres2: theory AutoCorres2.SimplConv
15:22:47 AutoCorres2: theory AutoCorres2.L2Defs
15:22:51 AutoCorres2: theory AutoCorres2.Split_Heap
15:22:54 AutoCorres2: theory AutoCorres2.L2ExceptionRewrite
15:22:55 AutoCorres2: theory AutoCorres2.L2Peephole
15:22:55 AutoCorres2: theory AutoCorres2.LocalVarExtract
15:22:55 AutoCorres2: theory AutoCorres2.Stack_Typing
15:22:56 AutoCorres2: theory AutoCorres2.WordAbstract
15:22:57 AutoCorres2: theory AutoCorres2.Refines_Spec
15:22:58 AutoCorres2: theory AutoCorres2.In_Out_Parameters
15:23:00 AutoCorres2: theory AutoCorres2.WordPolish
15:23:16 AutoCorres2: theory AutoCorres2.TypeStrengthen
15:23:16 AutoCorres2: theory AutoCorres2.HeapLift
15:23:40 AutoCorres2: theory AutoCorres2.Polish
15:23:40 AutoCorres2: theory AutoCorres2.Runs_To_VCG_StackPointer
15:23:50 AutoCorres2: theory AutoCorres2.AutoCorres
15:24:17 AutoCorres2: theory AutoCorres2.AutoCorresInfrastructure
15:24:17 AutoCorres2: theory AutoCorres2.Chapter1_MinMax
15:24:17 AutoCorres2: theory AutoCorres2.Chapter3_HoareHeap
15:24:17 AutoCorres2: theory AutoCorres2.Chapter2_HoareHeap
15:24:17 AutoCorres2: theory AutoCorres2.In_Out_Parameters_Ex
15:24:17 AutoCorres2: theory AutoCorres2.fnptr
15:24:17 AutoCorres2: theory AutoCorres2.open_struct
15:24:17 AutoCorres2: theory AutoCorres2.pointers_to_locals
15:24:26 AutoCorres2: theory AutoCorres2.union_ac
15:28:07 AutoCorres2: theory AutoCorres2.AutoCorres_Documentation
15:28:52 Preparing AutoCorres2/document ...
15:30:29 Finished AutoCorres2/document (0:01:37 elapsed time)
15:30:29 Preparing AutoCorres2/outline ...
15:31:25 Finished AutoCorres2/outline (0:00:56 elapsed time)
15:31:26 Timing AutoCorres2 (8 threads, 510.423s elapsed time, 3389.747s cpu time, 99.500s GC time, factor 6.64)
15:31:26 Finished AutoCorres2 (0:08:37 elapsed time, 0:57:02 cpu time, factor 6.62)
15:31:26 Building HOL-Complex_Analysis (on hpcisabelle/0) ...
15:31:29 HOL-Complex_Analysis: theory HOL-Library.More_List
15:31:29 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Contour_Integration
15:31:29 HOL-Complex_Analysis: theory HOL-Computational_Algebra.Polynomial
15:31:31 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
15:31:32 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Winding_Numbers
15:31:33 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
15:31:36 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Conformal_Mappings
15:31:37 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Singularities
15:31:37 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Great_Picard
15:31:37 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Riemann_Mapping
15:31:39 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Residues
15:31:39 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Residue_Theorem
15:31:42 HOL-Complex_Analysis: theory HOL-Computational_Algebra.Polynomial_FPS
15:31:43 HOL-Complex_Analysis: theory HOL-Computational_Algebra.Formal_Laurent_Series
15:31:46 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Laurent_Convergence
15:31:50 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Meromorphic
15:31:51 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Weierstrass_Factorization
15:31:52 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Analysis
15:32:54 Preparing HOL-Complex_Analysis/document ...
15:33:22 Finished HOL-Complex_Analysis/document (0:00:27 elapsed time)
15:33:22 Preparing HOL-Complex_Analysis/manual ...
15:33:27 Finished HOL-Complex_Analysis/manual (0:00:05 elapsed time)
15:33:27 Timing HOL-Complex_Analysis (8 threads, 65.347s elapsed time, 435.708s cpu time, 7.184s GC time, factor 6.67)
15:33:27 Finished HOL-Complex_Analysis (0:01:24 elapsed time, 0:07:54 cpu time, factor 5.59)
15:33:27 Building Echelon_Form (on hpcisabelle/1) ...
15:33:30 Echelon_Form: theory HOL-Library.Code_Abstract_Nat
15:33:30 Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field
15:33:30 Echelon_Form: theory HOL-Library.Code_Target_Int
15:33:30 Echelon_Form: theory HOL-Library.Function_Algebras
15:33:30 Echelon_Form: theory HOL-Library.IArray
15:33:30 Echelon_Form: theory HOL-Library.Z2
15:33:30 Echelon_Form: theory HOL-Library.Code_Cardinality
15:33:30 Echelon_Form: theory HOL-Library.More_List
15:33:30 Echelon_Form: theory HOL-Library.Code_Target_Nat
15:33:30 Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
15:33:30 Echelon_Form: theory HOL-Computational_Algebra.Polynomial
15:33:30 Echelon_Form: theory Cayley_Hamilton.Square_Matrix
15:33:30 Echelon_Form: theory HOL-Library.Code_Target_Numeral
15:33:30 Echelon_Form: theory Gauss_Jordan.Code_Set
15:33:30 Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
15:33:30 Echelon_Form: theory Gauss_Jordan.Code_Z2
15:33:31 Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
15:33:31 Echelon_Form: theory Gauss_Jordan.IArray_Addenda
15:33:32 Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
15:33:35 Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
15:33:37 Echelon_Form: theory Gauss_Jordan.Code_Matrix
15:33:37 Echelon_Form: theory Gauss_Jordan.Rref
15:33:37 Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
15:33:38 Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
15:33:38 Echelon_Form: theory Gauss_Jordan.Rank
15:33:38 Echelon_Form: theory Gauss_Jordan.Elementary_Operations
15:33:39 Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
15:33:39 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
15:33:41 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
15:33:41 Echelon_Form: theory Gauss_Jordan.Linear_Maps
15:33:42 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
15:33:43 Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
15:33:43 Echelon_Form: theory Gauss_Jordan.Determinants2
15:33:43 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
15:33:43 Echelon_Form: theory Gauss_Jordan.Inverse
15:33:43 Echelon_Form: theory Gauss_Jordan.System_Of_Equations
15:33:44 Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
15:33:44 Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
15:33:44 Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
15:33:44 Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
15:33:46 Echelon_Form: theory Echelon_Form.Rings2
15:34:22 Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
15:34:23 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
15:34:23 Echelon_Form: theory Echelon_Form.Echelon_Form
15:34:26 Echelon_Form: theory Echelon_Form.Echelon_Form_Det
15:34:26 Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
15:34:26 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
15:34:27 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
15:34:27 Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
15:34:28 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
15:34:29 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
15:34:30 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
15:36:15 Preparing Echelon_Form/document ...
15:36:21 Finished Echelon_Form/document (0:00:05 elapsed time)
15:36:21 Preparing Echelon_Form/outline ...
15:36:24 Finished Echelon_Form/outline (0:00:02 elapsed time)
15:36:24 Timing Echelon_Form (8 threads, 141.823s elapsed time, 876.796s cpu time, 36.970s GC time, factor 6.18)
15:36:24 Finished Echelon_Form (0:02:45 elapsed time, 0:15:26 cpu time, factor 5.61)
15:36:24 Building Core_DOM (on hpcisabelle/2) ...
15:36:42 Core_DOM: theory Core_DOM.Core_DOM_Basic_Datatypes
15:36:42 Core_DOM: theory Core_DOM.Testing_Utils
15:36:42 Core_DOM: theory Core_DOM.Hiding_Type_Variables
15:36:43 Core_DOM: theory Core_DOM.Ref
15:36:43 Core_DOM: theory Core_DOM.Heap_Error_Monad
15:36:43 Core_DOM: theory Core_DOM.BaseClass
15:36:43 Core_DOM: theory Core_DOM.ObjectPointer
15:36:44 Core_DOM: theory Core_DOM.NodePointer
15:36:44 Core_DOM: theory Core_DOM.ObjectClass
15:36:45 Core_DOM: theory Core_DOM.ElementPointer
15:36:46 Core_DOM: theory Core_DOM.NodeClass
15:36:46 Core_DOM: theory Core_DOM.CharacterDataPointer
15:36:47 Core_DOM: theory Core_DOM.BaseMonad
15:36:47 Core_DOM: theory Core_DOM.DocumentPointer
15:36:48 Core_DOM: theory Core_DOM.ShadowRootPointer
15:36:49 Core_DOM: theory Core_DOM.ObjectMonad
15:36:49 Core_DOM: theory Core_DOM.ElementClass
15:36:50 Core_DOM: theory Core_DOM.NodeMonad
15:36:51 Core_DOM: theory Core_DOM.CharacterDataClass
15:36:51 Core_DOM: theory Core_DOM.ElementMonad
15:36:52 Core_DOM: theory Core_DOM.DocumentClass
15:36:53 Core_DOM: theory Core_DOM.CharacterDataMonad
15:36:54 Core_DOM: theory Core_DOM.DocumentMonad
15:36:56 Core_DOM: theory Core_DOM.Core_DOM_Functions
15:37:16 Core_DOM: theory Core_DOM.Core_DOM_Heap_WF
15:37:38 Core_DOM: theory Core_DOM.Core_DOM
15:37:38 Core_DOM: theory Core_DOM.Core_DOM_BaseTest
15:37:47 Core_DOM: theory Core_DOM.Document_adoptNode
15:37:48 Core_DOM: theory Core_DOM.Document_getElementById
15:37:48 Core_DOM: theory Core_DOM.Node_insertBefore
15:37:48 Core_DOM: theory Core_DOM.Node_removeChild
15:37:50 Core_DOM: theory Core_DOM.Core_DOM_Tests
15:40:17 Preparing Core_DOM/document ...
15:40:34 Finished Core_DOM/document (0:00:16 elapsed time)
15:40:34 Preparing Core_DOM/outline ...
15:40:45 Finished Core_DOM/outline (0:00:11 elapsed time)
15:40:45 Timing Core_DOM (8 threads, 178.040s elapsed time, 1024.604s cpu time, 75.821s GC time, factor 5.75)
15:40:45 Finished Core_DOM (0:03:51 elapsed time, 0:19:18 cpu time, factor 4.99)
15:40:45 Building Shadow_DOM (on hpcisabelle/3) ...
15:41:10 Shadow_DOM: theory Shadow_DOM.ShadowRootClass
15:41:12 Shadow_DOM: theory Shadow_DOM.ShadowRootMonad
15:41:15 Shadow_DOM: theory Shadow_DOM.Shadow_DOM
15:42:25 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_BaseTest
15:42:37 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_Document_adoptNode
15:42:37 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_Document_getElementById
15:42:38 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_Node_insertBefore
15:42:38 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_Node_removeChild
15:42:39 Shadow_DOM: theory Shadow_DOM.slots
15:42:43 Shadow_DOM: theory Shadow_DOM.slots_fallback
15:42:50 Shadow_DOM: theory Shadow_DOM.Shadow_DOM_Tests
15:46:27 Preparing Shadow_DOM/document ...
15:46:41 Finished Shadow_DOM/document (0:00:13 elapsed time)
15:46:41 Preparing Shadow_DOM/outline ...
15:46:50 Finished Shadow_DOM/outline (0:00:09 elapsed time)
15:46:50 Timing Shadow_DOM (8 threads, 271.391s elapsed time, 1668.028s cpu time, 121.666s GC time, factor 6.15)
15:46:50 Finished Shadow_DOM (0:05:41 elapsed time, 0:30:46 cpu time, factor 5.42)
15:46:50 Running CoCon (on hpcisabelle/4) ...
15:46:51 CoCon: theory Fresh_Identifiers.Fresh
15:46:52 CoCon: theory Fresh_Identifiers.Fresh_String
15:46:52 CoCon: theory CoCon.Prelim
15:47:01 CoCon: theory CoCon.System_Specification
15:47:22 CoCon: theory CoCon.Automation_Setup
15:47:22 CoCon: theory CoCon.Safety_Properties
15:47:24 CoCon: theory CoCon.Decision_Intro
15:47:24 CoCon: theory CoCon.Discussion_Intro
15:47:24 CoCon: theory CoCon.Decision_Value_Setup
15:47:24 CoCon: theory CoCon.Discussion_Value_Setup
15:47:24 CoCon: theory CoCon.Observation_Setup
15:47:24 CoCon: theory CoCon.Paper_Intro
15:47:24 CoCon: theory CoCon.Review_Intro
15:47:24 CoCon: theory CoCon.Paper_Value_Setup
15:47:24 CoCon: theory CoCon.Review_Value_Setup
15:47:25 CoCon: theory CoCon.Reviewer_Assignment_Intro
15:47:25 CoCon: theory CoCon.Reviewer_Assignment_Value_Setup
15:47:25 CoCon: theory CoCon.Traceback_Properties
15:47:26 CoCon: theory CoCon.Discussion_NCPC
15:47:26 CoCon: theory CoCon.Decision_NCPC
15:47:26 CoCon: theory CoCon.Decision_NCPC_Aut
15:47:26 CoCon: theory CoCon.Paper_Aut
15:47:26 CoCon: theory CoCon.Paper_Aut_PC
15:47:27 CoCon: theory CoCon.Discussion_All
15:47:27 CoCon: theory CoCon.Review_RAut
15:47:27 CoCon: theory CoCon.Review_RAut_NCPC
15:47:27 CoCon: theory CoCon.Review_RAut_NCPC_PAut
15:47:28 CoCon: theory CoCon.Paper_All
15:47:28 CoCon: theory CoCon.Reviewer_Assignment_NCPC
15:47:28 CoCon: theory CoCon.Decision_All
15:47:28 CoCon: theory CoCon.Reviewer_Assignment_NCPC_Aut
15:47:30 CoCon: theory CoCon.Reviewer_Assignment_All
15:47:30 CoCon: theory CoCon.Review_All
15:47:57 CoCon: theory CoCon.All_BD_Security_Instances_for_CoCon
15:55:05 Preparing CoCon/document ...
15:55:18 Finished CoCon/document (0:00:12 elapsed time)
15:55:18 Preparing CoCon/outline ...
15:55:24 Finished CoCon/outline (0:00:06 elapsed time)
15:55:25 Timing CoCon (8 threads, 491.512s elapsed time, 3572.151s cpu time, 29.994s GC time, factor 7.27)
15:55:25 Finished CoCon (0:08:13 elapsed time, 0:59:38 cpu time, factor 7.24)
15:55:25 Building Stone_Algebras (on hpcisabelle/5) ...
15:55:27 Stone_Algebras: theory Stone_Algebras.Lattice_Basics
15:55:45 Stone_Algebras: theory Stone_Algebras.P_Algebras
15:55:45 Stone_Algebras: theory Stone_Algebras.Filters
15:56:17 Stone_Algebras: theory Stone_Algebras.Stone_Construction
15:56:35 Preparing Stone_Algebras/document ...
15:56:42 Finished Stone_Algebras/document (0:00:06 elapsed time)
15:56:42 Preparing Stone_Algebras/outline ...
15:56:46 Finished Stone_Algebras/outline (0:00:04 elapsed time)
15:56:46 Timing Stone_Algebras (8 threads, 60.877s elapsed time, 130.097s cpu time, 3.597s GC time, factor 2.14)
15:56:46 Finished Stone_Algebras (0:01:09 elapsed time, 0:02:26 cpu time, factor 2.10)
15:56:46 Running HOL-ODE-Examples (on hpcisabelle/6) ...
15:56:50 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
15:56:50 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
15:56:50 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
15:58:49 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
16:04:56 Timing HOL-ODE-Examples (8 threads, 484.990s elapsed time, 1732.595s cpu time, 9.067s GC time, factor 3.57)
16:04:56 Finished HOL-ODE-Examples (0:08:09 elapsed time, 0:28:58 cpu time, factor 3.55)
16:04:56 Running BTree (on hpcisabelle/7) ...
16:04:59 BTree: theory HOL-Data_Structures.Cmp
16:04:59 BTree: theory HOL-Data_Structures.Less_False
16:04:59 BTree: theory HOL-Library.Sublist
16:04:59 BTree: theory HOL-Data_Structures.Sorted_Less
16:04:59 BTree: theory HOL-Data_Structures.List_Ins_Del
16:05:00 BTree: theory BTree.BTree
16:05:00 BTree: theory BTree.BPlusTree
16:05:00 BTree: theory HOL-Data_Structures.Set_Specs
16:05:02 BTree: theory BTree.BTree_Height
16:05:02 BTree: theory BTree.BTree_Set
16:05:04 BTree: theory BTree.BPlusTree_Split
16:05:05 BTree: theory BTree.BPlusTree_Set
16:05:05 BTree: theory BTree.BPlusTree_Range
16:05:08 BTree: theory BTree.BTree_Split
16:05:13 BTree: theory BTree.BPlusTree_SplitCE
16:09:57 BTree: theory BTree.Subst_Mod_Mult_AC
16:09:57 BTree: theory HOL-Real_Asymp.Inst_Existentials
16:09:57 BTree: theory BTree.Inst_Ex_Assn
16:09:57 BTree: theory BTree.Array_SBlit
16:09:57 BTree: theory BTree.Basic_Assn
16:09:57 BTree: theory BTree.Imperative_Loops
16:09:57 BTree: theory BTree.Flatten_Iter
16:09:57 BTree: theory BTree.Flatten_Iter_Spec
16:10:05 BTree: theory BTree.Partially_Filled_Array
16:10:06 BTree: theory BTree.BPlusTree_Imp
16:10:06 BTree: theory BTree.BTree_Imp
16:10:06 BTree: theory BTree.Partially_Filled_Array_Iter
16:10:09 BTree: theory BTree.BTree_ImpSet
16:10:11 BTree: theory BTree.BPlusTree_Iter_OneWay
16:10:11 BTree: theory BTree.BPlusTree_Iter
16:10:11 BTree: theory BTree.BPlusTree_ImpSplit
16:10:12 BTree: theory BTree.BPlusTree_ImpSet
16:10:13 BTree: theory BTree.BTree_ImpSplit
16:10:18 BTree: theory BTree.BPlusTree_ImpRange
16:10:20 BTree: theory BTree.BPlusTree_ImpSplitCE
16:12:57 Preparing BTree/document ...
16:13:14 Finished BTree/document (0:00:17 elapsed time)
16:13:14 Preparing BTree/outline ...
16:13:22 Finished BTree/outline (0:00:08 elapsed time)
16:13:22 Timing BTree (8 threads, 474.930s elapsed time, 1751.527s cpu time, 24.167s GC time, factor 3.69)
16:13:22 Finished BTree (0:07:59 elapsed time, 0:29:23 cpu time, factor 3.68)
16:13:23 Building Deriving (on hpcisabelle/0) ...
16:13:25 Deriving: theory Deriving.Generator_Aux
16:13:25 Deriving: theory Deriving.Comparator
16:13:25 Deriving: theory Deriving.Derive_Manager
16:13:25 Deriving: theory Word_Lib.Bit_Comprehension
16:13:25 Deriving: theory Word_Lib.More_Divides
16:13:25 Deriving: theory Native_Word.Code_Int_Integer_Conversion
16:13:25 Deriving: theory Word_Lib.Signed_Division_Word
16:13:25 Deriving: theory Word_Lib.More_Arithmetic
16:13:25 Deriving: theory Word_Lib.More_Bit_Ring
16:13:25 Deriving: theory Deriving.Countable_Generator
16:13:25 Deriving: theory Deriving.Equality_Generator
16:13:26 Deriving: theory Deriving.Equality_Instances
16:13:26 Deriving: theory Deriving.Compare
16:13:26 Deriving: theory Deriving.Comparator_Generator
16:13:26 Deriving: theory Deriving.RBT_Comparator_Impl
16:13:27 Deriving: theory Word_Lib.More_Word
16:13:28 Deriving: theory Deriving.Compare_Generator
16:13:28 Deriving: theory Deriving.RBT_Compare_Order_Impl
16:13:28 Deriving: theory Deriving.Compare_Instances
16:13:28 Deriving: theory Deriving.Compare_Rat
16:13:28 Deriving: theory Deriving.Compare_Real
16:13:29 Deriving: theory Native_Word.Code_Target_Word_Base
16:13:29 Deriving: theory Word_Lib.Bit_Shifts_Infix_Syntax
16:13:29 Deriving: theory Word_Lib.Least_significant_bit
16:13:29 Deriving: theory Deriving.Compare_Order_Instances
16:13:31 Deriving: theory Word_Lib.Most_significant_bit
16:13:31 Deriving: theory Word_Lib.Generic_set_bit
16:13:32 Deriving: theory Native_Word.Code_Target_Integer_Bit
16:13:33 Deriving: theory Native_Word.Word_Type_Copies
16:13:46 Deriving: theory Native_Word.Uint32
16:13:48 Deriving: theory Collections.HashCode
16:13:49 Deriving: theory Deriving.Hash_Generator
16:13:50 Deriving: theory Deriving.Hash_Instances
16:13:50 Deriving: theory Deriving.Derive
16:13:51 Deriving: theory Deriving.Derive_Examples
16:14:23 Preparing Deriving/document ...
16:14:27 Finished Deriving/document (0:00:03 elapsed time)
16:14:27 Preparing Deriving/outline ...
16:14:30 Finished Deriving/outline (0:00:03 elapsed time)
16:14:30 Timing Deriving (8 threads, 40.505s elapsed time, 152.890s cpu time, 4.539s GC time, factor 3.77)
16:14:30 Finished Deriving (0:00:59 elapsed time, 0:03:12 cpu time, factor 3.22)
16:14:30 Building Algebraic_Numbers (on hpcisabelle/1) ...
16:14:38 Algebraic_Numbers: theory Pure-ex.Guess
16:14:38 Algebraic_Numbers: theory Deriving.Compare_Rat
16:14:38 Algebraic_Numbers: theory Deriving.Compare_Real
16:14:38 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
16:14:38 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
16:14:38 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
16:14:38 Algebraic_Numbers: theory Show.Show_Real
16:14:38 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
16:14:38 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
16:14:38 Algebraic_Numbers: theory Show.Show_Complex
16:14:39 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
16:14:39 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
16:14:41 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
16:14:41 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
16:14:41 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
16:14:41 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
16:14:41 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
16:14:44 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
16:14:47 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
16:14:53 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
16:14:54 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
16:15:07 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
16:15:07 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
16:15:08 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
16:15:08 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
16:15:09 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
16:15:12 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
16:15:18 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
16:17:11 Preparing Algebraic_Numbers/document ...
16:17:25 Finished Algebraic_Numbers/document (0:00:14 elapsed time)
16:17:25 Preparing Algebraic_Numbers/outline ...
16:17:32 Finished Algebraic_Numbers/outline (0:00:06 elapsed time)
16:17:32 Timing Algebraic_Numbers (8 threads, 133.229s elapsed time, 717.147s cpu time, 12.203s GC time, factor 5.38)
16:17:32 Finished Algebraic_Numbers (0:02:39 elapsed time, 0:12:49 cpu time, factor 4.82)
16:17:32 Running Isabelle_Marries_Dirac (on hpcisabelle/2) ...
16:17:36 Isabelle_Marries_Dirac: theory Matrix.Utility
16:17:36 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Basics
16:17:36 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Binary_Nat
16:17:37 Isabelle_Marries_Dirac: theory Matrix.Matrix_Legacy
16:17:37 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum
16:17:39 Isabelle_Marries_Dirac: theory Matrix_Tensor.Matrix_Tensor
16:17:39 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Complex_Vectors
16:17:39 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Measurement
16:17:41 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Tensor
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.More_Tensor
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.No_Cloning
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Entanglement
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma
16:17:42 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Quantum_Teleportation
16:17:44 Isabelle_Marries_Dirac: theory Isabelle_Marries_Dirac.Deutsch_Jozsa
16:24:11 Preparing Isabelle_Marries_Dirac/document ...
16:24:24 Finished Isabelle_Marries_Dirac/document (0:00:13 elapsed time)
16:24:24 Preparing Isabelle_Marries_Dirac/outline ...
16:24:30 Finished Isabelle_Marries_Dirac/outline (0:00:05 elapsed time)
16:24:30 Timing Isabelle_Marries_Dirac (8 threads, 393.557s elapsed time, 608.857s cpu time, 13.280s GC time, factor 1.55)
16:24:30 Finished Isabelle_Marries_Dirac (0:06:37 elapsed time, 0:10:13 cpu time, factor 1.55)
16:24:30 Building Probabilistic_While (on hpcisabelle/3) ...
16:24:33 Probabilistic_While: theory Flow_Networks.Graph
16:24:33 Probabilistic_While: theory HOL-Types_To_Sets.Types_To_Sets
16:24:33 Probabilistic_While: theory HOL-Library.Transitive_Closure_Table
16:24:33 Probabilistic_While: theory HOL-Library.While_Combinator
16:24:33 Probabilistic_While: theory Probabilistic_While.Bernoulli
16:24:34 Probabilistic_While: theory HOL-Library.Bourbaki_Witt_Fixpoint
16:24:35 Probabilistic_While: theory MFMC_Countable.MFMC_Misc
16:24:36 Probabilistic_While: theory Flow_Networks.Network
16:24:37 Probabilistic_While: theory Flow_Networks.Residual_Graph
16:24:39 Probabilistic_While: theory Flow_Networks.Augmenting_Flow
16:24:39 Probabilistic_While: theory Flow_Networks.Augmenting_Path
16:24:40 Probabilistic_While: theory Flow_Networks.Ford_Fulkerson
16:24:41 Probabilistic_While: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
16:24:42 Probabilistic_While: theory MFMC_Countable.MFMC_Finite
16:24:42 Probabilistic_While: theory MFMC_Countable.Matrix_For_Marginals
16:24:43 Probabilistic_While: theory MFMC_Countable.Rel_PMF_Characterisation
16:24:43 Probabilistic_While: theory Probabilistic_While.While_SPMF
16:24:44 Probabilistic_While: theory Probabilistic_While.Resampling
16:24:44 Probabilistic_While: theory Probabilistic_While.Fast_Dice_Roll
16:24:44 Probabilistic_While: theory Probabilistic_While.Geometric
16:25:20 Preparing Probabilistic_While/document ...
16:25:24 Finished Probabilistic_While/document (0:00:03 elapsed time)
16:25:24 Preparing Probabilistic_While/outline ...
16:25:27 Finished Probabilistic_While/outline (0:00:02 elapsed time)
16:25:27 Timing Probabilistic_While (8 threads, 31.718s elapsed time, 134.237s cpu time, 1.836s GC time, factor 4.23)
16:25:27 Finished Probabilistic_While (0:00:48 elapsed time, 0:02:44 cpu time, factor 3.37)
16:25:27 Building Goedel_Incompleteness (on hpcisabelle/4) ...
16:25:28 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_Jeroslow_Encoding
16:25:28 Goedel_Incompleteness: theory Goedel_Incompleteness.Deduction2
16:25:29 Goedel_Incompleteness: theory Goedel_Incompleteness.Jeroslow_Simplified
16:25:29 Goedel_Incompleteness: theory Goedel_Incompleteness.Jeroslow_Original
16:25:32 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_Encoding
16:25:32 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_Representability
16:25:34 Goedel_Incompleteness: theory Goedel_Incompleteness.Derivability_Conditions
16:25:34 Goedel_Incompleteness: theory Goedel_Incompleteness.Diagonalization
16:25:36 Goedel_Incompleteness: theory Goedel_Incompleteness.Goedel_Formula
16:25:36 Goedel_Incompleteness: theory Goedel_Incompleteness.Loeb_Formula
16:25:36 Goedel_Incompleteness: theory Goedel_Incompleteness.Standard_Model_More
16:25:36 Goedel_Incompleteness: theory Goedel_Incompleteness.Loeb
16:25:37 Goedel_Incompleteness: theory Goedel_Incompleteness.Rosser_Formula
16:25:40 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_First_Goedel
16:25:40 Goedel_Incompleteness: theory Goedel_Incompleteness.Tarski
16:25:40 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_First_Goedel_Rosser
16:25:45 Goedel_Incompleteness: theory Goedel_Incompleteness.Abstract_Second_Goedel
16:25:45 Goedel_Incompleteness: theory Goedel_Incompleteness.All_Abstract
16:25:54 Preparing Goedel_Incompleteness/document ...
16:25:59 Finished Goedel_Incompleteness/document (0:00:05 elapsed time)
16:25:59 Preparing Goedel_Incompleteness/outline ...
16:26:04 Finished Goedel_Incompleteness/outline (0:00:04 elapsed time)
16:26:04 Timing Goedel_Incompleteness (8 threads, 18.105s elapsed time, 88.852s cpu time, 1.718s GC time, factor 4.91)
16:26:04 Finished Goedel_Incompleteness (0:00:26 elapsed time, 0:01:45 cpu time, factor 3.93)
16:26:04 Building Groebner_Bases (on hpcisabelle/5) ...
16:26:08 Groebner_Bases: theory Containers.List_Fusion
16:26:08 Groebner_Bases: theory Containers.Extend_Partial_Order
16:26:08 Groebner_Bases: theory Deriving.Comparator
16:26:08 Groebner_Bases: theory Containers.Equal
16:26:08 Groebner_Bases: theory Deriving.Derive_Manager
16:26:08 Groebner_Bases: theory Deriving.Generator_Aux
16:26:08 Groebner_Bases: theory Containers.Containers_Auxiliary
16:26:08 Groebner_Bases: theory Jordan_Normal_Form.Missing_Misc
16:26:08 Groebner_Bases: theory Containers.Closure_Set
16:26:08 Groebner_Bases: theory Abstract-Rewriting.Seq
16:26:08 Groebner_Bases: theory Polynomials.MPoly_Type
16:26:09 Groebner_Bases: theory Polynomials.More_Modules
16:26:09 Groebner_Bases: theory Jordan_Normal_Form.Missing_Ring
16:26:09 Groebner_Bases: theory Deriving.Equality_Generator
16:26:09 Groebner_Bases: theory Polynomial_Interpolation.Missing_Unsorted
16:26:09 Groebner_Bases: theory Containers.Containers_Generator
16:26:09 Groebner_Bases: theory Groebner_Bases.Code_Target_Rat
16:26:09 Groebner_Bases: theory Deriving.Equality_Instances
16:26:09 Groebner_Bases: theory Polynomials.More_MPoly_Type
16:26:09 Groebner_Bases: theory Jordan_Normal_Form.Conjugate
16:26:09 Groebner_Bases: theory Open_Induction.Restricted_Predicates
16:26:10 Groebner_Bases: theory Containers.Collection_Enum
16:26:10 Groebner_Bases: theory Deriving.Compare
16:26:10 Groebner_Bases: theory Polynomials.OAlist
16:26:10 Groebner_Bases: theory Deriving.Comparator_Generator
16:26:10 Groebner_Bases: theory Containers.Lexicographic_Order
16:26:11 Groebner_Bases: theory Containers.Collection_Eq
16:26:11 Groebner_Bases: theory Containers.Set_Linorder
16:26:11 Groebner_Bases: theory Containers.RBT_ext
16:26:11 Groebner_Bases: theory Deriving.Compare_Generator
16:26:11 Groebner_Bases: theory Deriving.RBT_Comparator_Impl
16:26:11 Groebner_Bases: theory Containers.DList_Set
16:26:12 Groebner_Bases: theory Deriving.Compare_Instances
16:26:12 Groebner_Bases: theory Polynomial_Interpolation.Ring_Hom
16:26:12 Groebner_Bases: theory Regular-Sets.Regular_Set
16:26:14 Groebner_Bases: theory Well_Quasi_Orders.Infinite_Sequences
16:26:14 Groebner_Bases: theory Well_Quasi_Orders.Minimal_Elements
16:26:14 Groebner_Bases: theory Well_Quasi_Orders.Least_Enum
16:26:16 Groebner_Bases: theory Regular-Sets.Regular_Exp
16:26:18 Groebner_Bases: theory Jordan_Normal_Form.Matrix
16:26:20 Groebner_Bases: theory Regular-Sets.NDerivative
16:26:20 Groebner_Bases: theory Regular-Sets.Relation_Interpretation
16:26:23 Groebner_Bases: theory Containers.Collection_Order
16:26:24 Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
16:26:25 Groebner_Bases: theory Regular-Sets.Equivalence_Checking
16:26:26 Groebner_Bases: theory Regular-Sets.Regexp_Method
16:26:26 Groebner_Bases: theory Containers.RBT_Mapping2
16:26:27 Groebner_Bases: theory Abstract-Rewriting.Abstract_Rewriting
16:26:27 Groebner_Bases: theory Well_Quasi_Orders.Almost_Full
16:26:28 Groebner_Bases: theory Containers.RBT_Set2
16:26:29 Groebner_Bases: theory Groebner_Bases.Confluence
16:26:30 Groebner_Bases: theory Well_Quasi_Orders.Minimal_Bad_Sequences
16:26:30 Groebner_Bases: theory Well_Quasi_Orders.Almost_Full_Relations
16:26:30 Groebner_Bases: theory Containers.Set_Impl
16:26:31 Groebner_Bases: theory Polynomials.Utils
16:26:31 Groebner_Bases: theory Well_Quasi_Orders.Well_Quasi_Orders
16:26:31 Groebner_Bases: theory Groebner_Bases.General
16:26:31 Groebner_Bases: theory Polynomials.Power_Products
16:26:49 Groebner_Bases: theory Polynomials.MPoly_Type_Class
16:26:49 Groebner_Bases: theory Polynomials.PP_Type
16:26:55 Groebner_Bases: theory Polynomials.MPoly_Type_Class_Ordered
16:26:56 Groebner_Bases: theory Jordan_Normal_Form.Matrix_IArray_Impl
16:26:59 Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
16:27:14 Groebner_Bases: theory Groebner_Bases.More_MPoly_Type_Class
16:27:14 Groebner_Bases: theory Groebner_Bases.Reduction
16:27:14 Groebner_Bases: theory Polynomials.Quasi_PM_Power_Products
16:27:14 Groebner_Bases: theory Polynomials.OAlist_Poly_Mapping
16:27:17 Groebner_Bases: theory Groebner_Bases.Macaulay_Matrix
16:27:21 Groebner_Bases: theory Polynomials.MPoly_PM
16:27:26 Groebner_Bases: theory Polynomials.Term_Order
16:27:28 Groebner_Bases: theory Groebner_Bases.Auto_Reduction
16:27:28 Groebner_Bases: theory Groebner_Bases.Groebner_Bases
16:27:36 Groebner_Bases: theory Polynomials.MPoly_Type_Class_OAlist
16:27:48 Groebner_Bases: theory Groebner_Bases.Algorithm_Schema
16:27:48 Groebner_Bases: theory Groebner_Bases.Reduced_GB
16:27:48 Groebner_Bases: theory Groebner_Bases.Syzygy
16:27:55 Groebner_Bases: theory Groebner_Bases.Benchmarks
16:27:58 Groebner_Bases: theory Groebner_Bases.Groebner_PM
16:28:34 Groebner_Bases: theory Groebner_Bases.Buchberger
16:28:34 Groebner_Bases: theory Groebner_Bases.Algorithm_Schema_Impl
16:28:34 Groebner_Bases: theory Groebner_Bases.F4
16:28:43 Groebner_Bases: theory Groebner_Bases.Buchberger_Examples
16:28:43 Groebner_Bases: theory Groebner_Bases.Syzygy_Examples
16:28:43 Groebner_Bases: theory Groebner_Bases.Reduced_GB_Examples
16:28:54 Groebner_Bases: theory Groebner_Bases.F4_Examples
16:31:17 Preparing Groebner_Bases/document ...
16:31:41 Finished Groebner_Bases/document (0:00:24 elapsed time)
16:31:41 Preparing Groebner_Bases/outline ...
16:31:51 Finished Groebner_Bases/outline (0:00:09 elapsed time)
16:31:51 Timing Groebner_Bases (8 threads, 235.922s elapsed time, 1351.323s cpu time, 126.462s GC time, factor 5.73)
16:31:51 Finished Groebner_Bases (0:05:06 elapsed time, 0:25:33 cpu time, factor 5.01)
16:31:51 Running HOL-Codegenerator_Test (on hpcisabelle/6) ...
16:31:54 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fraction_Field
16:31:54 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Group_Closure
16:31:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False
16:31:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp
16:31:54 HOL-Codegenerator_Test: theory HOL-Examples.Records
16:31:54 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Factorial_Ring
16:31:54 HOL-Codegenerator_Test: theory HOL-Examples.Gauss_Numbers
16:31:54 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Lazy_Test
16:31:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less
16:31:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del
16:31:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del
16:31:55 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_Specs
16:31:55 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_Specs
16:31:55 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set
16:31:57 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map
16:32:05 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm
16:32:06 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML
16:32:06 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala
16:32:21 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Primes
16:32:21 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Normalized_Fraction
16:32:30 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Nth_Powers
16:32:30 HOL-Codegenerator_Test: theory HOL-Number_Theory.Eratosthenes
16:32:30 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Squarefree
16:32:30 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Power_Series
16:32:30 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial
16:32:43 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
16:32:43 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_FPS
16:32:43 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_Factorial
16:32:44 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Laurent_Series
16:32:48 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Computational_Algebra
16:32:50 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates
16:32:54 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate
16:32:55 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Abstract_Char
16:32:55 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat
16:32:55 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures
16:32:55 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat
16:38:50 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC
16:38:52 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton
16:38:56 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml
16:38:57 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ
16:39:01 Timing HOL-Codegenerator_Test (8 threads, 424.143s elapsed time, 1171.133s cpu time, 78.325s GC time, factor 2.76)
16:39:01 Finished HOL-Codegenerator_Test (0:07:07 elapsed time, 0:19:43 cpu time, factor 2.76)
16:39:01 Running Goedel_HFSet_Semanticless (on hpcisabelle/7) ...
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Infinite_Set
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Cancellation
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Nat_Bijection
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Old_Datatype
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Syntax
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Phantom_Type
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Product
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Option
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Set
16:39:03 Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_List
16:39:04 Goedel_HFSet_Semanticless: theory HereditarilyFinite.HF
16:39:04 Goedel_HFSet_Semanticless: theory HOL-Library.Countable
16:39:04 Goedel_HFSet_Semanticless: theory HOL-Library.Multiset
16:39:04 Goedel_HFSet_Semanticless: theory HOL-Library.Cardinality
16:39:05 Goedel_HFSet_Semanticless: theory HereditarilyFinite.Ordinal
16:39:05 Goedel_HFSet_Semanticless: theory FinFun.FinFun
16:39:06 Goedel_HFSet_Semanticless: theory HereditarilyFinite.Rank
16:39:06 Goedel_HFSet_Semanticless: theory HOL-Library.FSet
16:39:06 Goedel_HFSet_Semanticless: theory HereditarilyFinite.OrdArith
16:39:11 Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_Base
16:39:18 Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_Abs
16:39:20 Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_FCB
16:39:21 Goedel_HFSet_Semanticless: theory Nominal2.Nominal2
16:39:25 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.SyntaxN
16:39:32 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Coding
16:39:33 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Predicates
16:39:35 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Sigma
16:39:40 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Coding_Predicates
16:39:45 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Functions
16:39:45 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Pf_Predicates
16:39:47 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.II_Prelims
16:39:49 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Goedel_I
16:39:49 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Pseudo_Coding
16:39:50 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Quote
16:39:51 Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Instance
16:46:31 Preparing Goedel_HFSet_Semanticless/document ...
16:46:40 Finished Goedel_HFSet_Semanticless/document (0:00:09 elapsed time)
16:46:40 Preparing Goedel_HFSet_Semanticless/outline ...
16:46:45 Finished Goedel_HFSet_Semanticless/outline (0:00:04 elapsed time)
16:46:45 Timing Goedel_HFSet_Semanticless (8 threads, 444.829s elapsed time, 1872.186s cpu time, 20.974s GC time, factor 4.21)
16:46:45 Finished Goedel_HFSet_Semanticless (0:07:27 elapsed time, 0:31:17 cpu time, factor 4.20)
16:46:46 Building Stone_Relation_Algebras (on hpcisabelle/0) ...
16:46:48 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Fixpoints
16:46:51 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Semirings
16:47:03 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Relation_Algebras
16:47:54 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Choose_Component
16:47:54 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Relation_Subalgebras
16:47:54 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Matrix_Relation_Algebras
16:48:02 Stone_Relation_Algebras: theory Stone_Relation_Algebras.Linear_Order_Matrices
16:48:24 Preparing Stone_Relation_Algebras/document ...
16:48:31 Finished Stone_Relation_Algebras/document (0:00:06 elapsed time)
16:48:31 Preparing Stone_Relation_Algebras/outline ...
16:48:36 Finished Stone_Relation_Algebras/outline (0:00:04 elapsed time)
16:48:36 Timing Stone_Relation_Algebras (8 threads, 86.688s elapsed time, 180.889s cpu time, 4.291s GC time, factor 2.09)
16:48:36 Finished Stone_Relation_Algebras (0:01:37 elapsed time, 0:03:22 cpu time, factor 2.07)
16:48:36 Building HOL-Nominal (on hpcisabelle/1) ...
16:48:37 HOL-Nominal: theory HOL-Library.Infinite_Set
16:48:37 HOL-Nominal: theory HOL-Library.Old_Datatype
16:48:38 HOL-Nominal: theory HOL-Nominal.Nominal
16:48:54 Timing HOL-Nominal (8 threads, 9.608s elapsed time, 38.940s cpu time, 0.999s GC time, factor 4.05)
16:48:54 Finished HOL-Nominal (0:00:17 elapsed time, 0:00:53 cpu time, factor 3.07)
16:48:54 Building CryptHOL (on hpcisabelle/2) ...
16:48:57 CryptHOL: theory HOL-Eisbach.Eisbach
16:48:57 CryptHOL: theory Applicative_Lifting.Applicative
16:48:57 CryptHOL: theory CryptHOL.Partial_Function_Set
16:48:57 CryptHOL: theory HOL-Library.Case_Converter
16:48:57 CryptHOL: theory HOL-Algebra.Congruence
16:48:57 CryptHOL: theory HOL-Library.Function_Algebras
16:48:57 CryptHOL: theory HOL-Library.Countable_Set_Type
16:48:57 CryptHOL: theory HOL-Library.Type_Length
16:48:57 CryptHOL: theory Coinductive.Coinductive_Nat
16:48:58 CryptHOL: theory HOL-Library.Simps_Case_Conv
16:48:58 CryptHOL: theory Monad_Normalisation.Monad_Normalisation
16:48:58 CryptHOL: theory Landau_Symbols.Group_Sort
16:48:59 CryptHOL: theory HOL-Algebra.Order
16:49:00 CryptHOL: theory Coinductive.Coinductive_List
16:49:00 CryptHOL: theory Applicative_Lifting.Applicative_Environment
16:49:00 CryptHOL: theory Applicative_Lifting.Applicative_Set
16:49:00 CryptHOL: theory Applicative_Lifting.Applicative_PMF
16:49:00 CryptHOL: theory CryptHOL.Environment_Functor
16:49:00 CryptHOL: theory CryptHOL.Set_Applicative
16:49:01 CryptHOL: theory Landau_Symbols.Landau_Real_Products
16:49:01 CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
16:49:01 CryptHOL: theory HOL-Algebra.Lattice
16:49:01 CryptHOL: theory HOL-Algebra.Complete_Lattice
16:49:02 CryptHOL: theory CryptHOL.SPMF_Applicative
16:49:03 CryptHOL: theory HOL-Algebra.Group
16:49:05 CryptHOL: theory Landau_Symbols.Landau_Simprocs
16:49:05 CryptHOL: theory HOL-Algebra.Coset
16:49:05 CryptHOL: theory Landau_Symbols.Landau_More
16:49:06 CryptHOL: theory CryptHOL.Negligible
16:49:07 CryptHOL: theory Coinductive.TLList
16:49:08 CryptHOL: theory CryptHOL.Cyclic_Group
16:49:08 CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
16:49:25 CryptHOL: theory CryptHOL.Misc_CryptHOL
16:49:36 CryptHOL: theory CryptHOL.Generat
16:49:36 CryptHOL: theory CryptHOL.List_Bits
16:49:36 CryptHOL: theory CryptHOL.Resumption
16:49:39 CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
16:49:56 CryptHOL: theory CryptHOL.Computational_Model
16:49:57 CryptHOL: theory CryptHOL.GPV_Applicative
16:49:59 CryptHOL: theory CryptHOL.GPV_Expectation
16:50:00 CryptHOL: theory CryptHOL.GPV_Bisim
16:50:01 CryptHOL: theory CryptHOL.CryptHOL
16:50:47 Preparing CryptHOL/document ...
16:51:06 Finished CryptHOL/document (0:00:18 elapsed time)
16:51:06 Preparing CryptHOL/outline ...
16:51:17 Finished CryptHOL/outline (0:00:10 elapsed time)
16:51:17 Timing CryptHOL (8 threads, 77.125s elapsed time, 469.113s cpu time, 14.474s GC time, factor 6.08)
16:51:17 Finished CryptHOL (0:01:49 elapsed time, 0:09:00 cpu time, factor 4.93)
16:51:17 Running Solidity (on hpcisabelle/3) ...
16:51:19 Solidity: theory HOL-Eisbach.Eisbach
16:51:19 Solidity: theory Finite-Map-Extras.Finite_Map_Extras
16:51:21 Solidity: theory HOL-Eisbach.Eisbach_Tools
16:51:21 Solidity: theory Solidity.Utils
16:51:21 Solidity: theory Solidity.Solidity_Symbex
16:51:21 Solidity: theory Solidity.ReadShow
16:51:21 Solidity: theory Solidity.StateMonad
16:51:21 Solidity: theory Solidity.Valuetypes
16:51:25 Solidity: theory Solidity.Accounts
16:51:26 Solidity: theory Solidity.Storage
16:51:29 Solidity: theory Solidity.Environment
16:52:05 Solidity: theory Solidity.Contracts
16:52:12 Solidity: theory Solidity.Expressions
16:52:41 Solidity: theory Solidity.Statements
16:53:25 Solidity: theory Solidity.Solidity_Main
16:53:25 Solidity: theory Solidity.Constant_Folding
16:53:28 Solidity: theory Solidity.Solidity_Evaluator
16:53:44 Solidity: theory Solidity.Weakest_Precondition
16:56:17 Solidity: theory Solidity.Reentrancy
16:58:16 Solidity: theory Solidity.Compile_Evaluator
16:58:30 Preparing Solidity/document ...
16:58:47 Finished Solidity/document (0:00:16 elapsed time)
16:58:47 Preparing Solidity/outline ...
16:58:55 Finished Solidity/outline (0:00:08 elapsed time)
16:58:56 Timing Solidity (8 threads, 428.285s elapsed time, 2497.603s cpu time, 35.375s GC time, factor 5.83)
16:58:56 Finished Solidity (0:07:11 elapsed time, 0:41:46 cpu time, factor 5.81)
16:58:56 Building Containers (on hpcisabelle/4) ...
16:58:58 Containers: theory Containers.List_Fusion
16:58:58 Containers: theory Containers.Equal
16:58:58 Containers: theory Containers.Extend_Partial_Order
16:58:58 Containers: theory Containers.AssocList
16:58:58 Containers: theory Containers.Containers_Auxiliary
16:58:58 Containers: theory Containers.Card_Datatype
16:58:58 Containers: theory Regular-Sets.Regular_Set
16:58:58 Containers: theory Containers.Closure_Set
16:58:59 Containers: theory Containers.Containers_Generator
16:58:59 Containers: theory Containers.Collection_Enum
16:58:59 Containers: theory Containers.Collection_Eq
16:59:00 Containers: theory Containers.Lexicographic_Order
16:59:00 Containers: theory Containers.RBT_ext
16:59:00 Containers: theory Containers.DList_Set
16:59:00 Containers: theory Containers.Set_Linorder
16:59:02 Containers: theory Regular-Sets.Regular_Exp
16:59:05 Containers: theory Regular-Sets.NDerivative
16:59:05 Containers: theory Regular-Sets.Relation_Interpretation
16:59:09 Containers: theory Regular-Sets.Equivalence_Checking
16:59:09 Containers: theory Regular-Sets.Regexp_Method
16:59:13 Containers: theory Containers.Collection_Order
16:59:15 Containers: theory Containers.List_Proper_Interval
16:59:15 Containers: theory Containers.RBT_Mapping2
16:59:17 Containers: theory Containers.RBT_Set2
16:59:19 Containers: theory Containers.Set_Impl
16:59:39 Containers: theory Containers.Mapping_Impl
16:59:41 Containers: theory Containers.Map_To_Mapping
16:59:41 Containers: theory Containers.Containers
16:59:41 Containers: theory Containers.Containers_Userguide
16:59:41 Containers: theory Containers.Compatibility_Containers_Regular_Sets
16:59:53 Containers: theory Containers.Card_Datatype_Ex
16:59:53 Containers: theory Containers.Containers_DFS_Ex
16:59:53 Containers: theory Containers.Map_To_Mapping_Ex
16:59:53 Containers: theory Containers.TwoSat_Ex
16:59:56 Containers: theory Containers.Containers_TwoSat_Ex
17:01:02 Preparing Containers/document ...
17:01:15 Finished Containers/document (0:00:13 elapsed time)
17:01:15 Preparing Containers/outline ...
17:01:24 Finished Containers/outline (0:00:08 elapsed time)
17:01:24 Timing Containers (8 threads, 102.417s elapsed time, 281.323s cpu time, 9.185s GC time, factor 2.75)
17:01:24 Finished Containers (0:02:05 elapsed time, 0:05:28 cpu time, factor 2.63)
17:01:24 Building Quantales_Converse (on hpcisabelle/5) ...
17:01:25 Quantales_Converse: theory Kleene_Algebra.Signatures
17:01:25 Quantales_Converse: theory Order_Lattice_Props.Sup_Lattice
17:01:26 Quantales_Converse: theory Kleene_Algebra.Dioid
17:01:34 Quantales_Converse: theory Order_Lattice_Props.Order_Duality
17:01:43 Quantales_Converse: theory Kleene_Algebra.Conway
17:01:44 Quantales_Converse: theory Order_Lattice_Props.Order_Lattice_Props
17:01:54 Quantales_Converse: theory Kleene_Algebra.Kleene_Algebra
17:01:58 Quantales_Converse: theory Order_Lattice_Props.Galois_Connections
17:01:58 Quantales_Converse: theory Order_Lattice_Props.Closure_Operators
17:02:00 Quantales_Converse: theory Quantales.Quantales
17:02:04 Quantales_Converse: theory KAD.Domain_Semiring
17:02:04 Quantales_Converse: theory Quantales_Converse.Kleene_Algebra_Converse
17:02:18 Quantales_Converse: theory KAD.Antidomain_Semiring
17:02:38 Quantales_Converse: theory KAD.Range_Semiring
17:03:00 Quantales_Converse: theory KAD.Modal_Kleene_Algebra
17:03:00 Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Var
17:03:06 Quantales_Converse: theory Quantales.Quantale_Star
17:03:09 Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Converse
17:03:27 Quantales_Converse: theory Quantales_Converse.Modal_Quantale
17:05:24 Quantales_Converse: theory Quantales_Converse.Quantale_Converse
17:08:28 Preparing Quantales_Converse/document ...
17:08:32 Finished Quantales_Converse/document (0:00:04 elapsed time)
17:08:32 Preparing Quantales_Converse/outline ...
17:08:36 Finished Quantales_Converse/outline (0:00:03 elapsed time)
17:08:36 Timing Quantales_Converse (8 threads, 406.201s elapsed time, 682.908s cpu time, 17.777s GC time, factor 1.68)
17:08:36 Finished Quantales_Converse (0:07:03 elapsed time, 0:12:01 cpu time, factor 1.70)
17:08:36 Building Formal_SSA (on hpcisabelle/6) ...
17:08:39 Formal_SSA: theory Dijkstra_Shortest_Path.Graph
17:08:39 Formal_SSA: theory Formal_SSA.Serial_Rel
17:08:39 Formal_SSA: theory HOL-Library.List_Lexorder
17:08:39 Formal_SSA: theory HOL-Library.Omega_Words_Fun
17:08:39 Formal_SSA: theory HOL-Library.Char_ord
17:08:39 Formal_SSA: theory HOL-Library.Mapping
17:08:39 Formal_SSA: theory HOL-Library.RBT_Set
17:08:39 Formal_SSA: theory HOL-Library.Sublist
17:08:39 Formal_SSA: theory Formal_SSA.While_Combinator_Exts
17:08:39 Formal_SSA: theory Slicing.AuxLemmas
17:08:39 Formal_SSA: theory Slicing.Com
17:08:39 Formal_SSA: theory Slicing.BasicDefs
17:08:39 Formal_SSA: theory CAVA_Automata.Digraph_Basic
17:08:40 Formal_SSA: theory Dijkstra_Shortest_Path.GraphSpec
17:08:40 Formal_SSA: theory Slicing.CFG
17:08:41 Formal_SSA: theory Slicing.CFGExit
17:08:41 Formal_SSA: theory Slicing.CFG_wf
17:08:41 Formal_SSA: theory HOL-Library.RBT_Mapping
17:08:41 Formal_SSA: theory Slicing.Postdomination
17:08:41 Formal_SSA: theory Slicing.CFGExit_wf
17:08:41 Formal_SSA: theory Slicing.DynDataDependence
17:08:41 Formal_SSA: theory Slicing.Distance
17:08:41 Formal_SSA: theory Slicing.DataDependence
17:08:41 Formal_SSA: theory Slicing.Observable
17:08:41 Formal_SSA: theory Slicing.SemanticsCFG
17:08:41 Formal_SSA: theory Slicing.WeakOrderDependence
17:08:42 Formal_SSA: theory Slicing.DynStandardControlDependence
17:08:42 Formal_SSA: theory Slicing.DynWeakControlDependence
17:08:42 Formal_SSA: theory Slicing.Slice
17:08:42 Formal_SSA: theory Slicing.WeakControlDependence
17:08:42 Formal_SSA: theory Slicing.StandardControlDependence
17:08:42 Formal_SSA: theory Slicing.PDG
17:08:42 Formal_SSA: theory Formal_SSA.FormalSSA_Misc
17:08:42 Formal_SSA: theory Formal_SSA.Mapping_Exts
17:08:43 Formal_SSA: theory Formal_SSA.RBT_Mapping_Exts
17:08:43 Formal_SSA: theory Slicing.Labels
17:08:43 Formal_SSA: theory Slicing.WCFG
17:08:44 Formal_SSA: theory Slicing.CDepInstantiations
17:08:45 Formal_SSA: theory Slicing.Interpretation
17:08:45 Formal_SSA: theory Slicing.WellFormed
17:08:45 Formal_SSA: theory Formal_SSA.Graph_path
17:08:46 Formal_SSA: theory Slicing.AdditionalLemmas
17:08:46 Formal_SSA: theory Formal_SSA.Disjoin_Transform
17:08:52 Formal_SSA: theory Formal_SSA.SSA_CFG
17:08:55 Formal_SSA: theory Formal_SSA.Construct_SSA
17:08:55 Formal_SSA: theory Formal_SSA.Minimality
17:08:55 Formal_SSA: theory Formal_SSA.SSA_CFG_code
17:08:57 Formal_SSA: theory Formal_SSA.Construct_SSA_notriv
17:09:00 Formal_SSA: theory Formal_SSA.SSA_Semantics
17:09:00 Formal_SSA: theory Formal_SSA.Construct_SSA_code
17:09:00 Formal_SSA: theory Formal_SSA.Construct_SSA_notriv_code
17:09:02 Formal_SSA: theory Formal_SSA.SSA_Transfer_Rules
17:09:10 Formal_SSA: theory Formal_SSA.Generic_Interpretation
17:09:32 Formal_SSA: theory Formal_SSA.Generic_Extract
17:09:34 Formal_SSA: theory Formal_SSA.WhileGraphSSA
17:16:16 Preparing Formal_SSA/document ...
17:16:29 Finished Formal_SSA/document (0:00:13 elapsed time)
17:16:29 Preparing Formal_SSA/outline ...
17:16:36 Finished Formal_SSA/outline (0:00:06 elapsed time)
17:16:36 Timing Formal_SSA (8 threads, 429.169s elapsed time, 995.406s cpu time, 14.428s GC time, factor 2.32)
17:16:36 Finished Formal_SSA (0:07:37 elapsed time, 0:17:39 cpu time, factor 2.31)
17:16:36 Running Broadcast_Psi (on hpcisabelle/7) ...
17:16:38 Broadcast_Psi: theory Psi_Calculi.Chain
17:16:38 Broadcast_Psi: theory HOL-Library.Cancellation
17:16:39 Broadcast_Psi: theory HOL-Library.Multiset
17:16:40 Broadcast_Psi: theory Broadcast_Psi.Broadcast_Chain
17:16:40 Broadcast_Psi: theory Psi_Calculi.Subst_Term
17:16:40 Broadcast_Psi: theory Psi_Calculi.Agent
17:16:57 Broadcast_Psi: theory Psi_Calculi.Close_Subst
17:16:57 Broadcast_Psi: theory Psi_Calculi.Frame
17:16:57 Broadcast_Psi: theory Psi_Calculi.Structural_Congruence
17:17:00 Broadcast_Psi: theory Broadcast_Psi.Broadcast_Frame
17:17:01 Broadcast_Psi: theory Broadcast_Psi.Semantics
17:17:24 Broadcast_Psi: theory Broadcast_Psi.Simulation
17:17:25 Broadcast_Psi: theory Broadcast_Psi.Bisimulation
17:17:25 Broadcast_Psi: theory Broadcast_Psi.Sim_Pres
17:17:26 Broadcast_Psi: theory Broadcast_Psi.Sim_Struct_Cong
17:17:27 Broadcast_Psi: theory Broadcast_Psi.Bisim_Pres
17:17:29 Broadcast_Psi: theory Broadcast_Psi.Bisim_Struct_Cong
17:17:30 Broadcast_Psi: theory Broadcast_Psi.Bisim_Subst
17:17:32 Broadcast_Psi: theory Broadcast_Psi.Broadcast_Thms
17:24:20 Preparing Broadcast_Psi/document ...
17:25:12 Finished Broadcast_Psi/document (0:00:51 elapsed time)
17:25:12 Preparing Broadcast_Psi/outline ...
17:25:25 Finished Broadcast_Psi/outline (0:00:13 elapsed time)
17:25:25 Timing Broadcast_Psi (8 threads, 455.781s elapsed time, 2139.387s cpu time, 76.339s GC time, factor 4.69)
17:25:25 Finished Broadcast_Psi (0:07:38 elapsed time, 0:35:49 cpu time, factor 4.68)
17:25:26 Running Goedel_HFSet_Semantic (on hpcisabelle/0) ...
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Cancellation
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Syntax
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Infinite_Set
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Nat_Bijection
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Old_Datatype
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Phantom_Type
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Product
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Option
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Set
17:25:27 Goedel_HFSet_Semantic: theory HOL-Library.Quotient_List
17:25:28 Goedel_HFSet_Semantic: theory HereditarilyFinite.HF
17:25:28 Goedel_HFSet_Semantic: theory HOL-Library.Countable
17:25:29 Goedel_HFSet_Semantic: theory HOL-Library.Cardinality
17:25:29 Goedel_HFSet_Semantic: theory HOL-Library.Multiset
17:25:30 Goedel_HFSet_Semantic: theory FinFun.FinFun
17:25:30 Goedel_HFSet_Semantic: theory HereditarilyFinite.Ordinal
17:25:30 Goedel_HFSet_Semantic: theory HOL-Library.FSet
17:25:30 Goedel_HFSet_Semantic: theory HereditarilyFinite.Rank
17:25:30 Goedel_HFSet_Semantic: theory HereditarilyFinite.OrdArith
17:25:36 Goedel_HFSet_Semantic: theory Nominal2.Nominal2_Base
17:25:42 Goedel_HFSet_Semantic: theory Nominal2.Nominal2_Abs
17:25:45 Goedel_HFSet_Semantic: theory Nominal2.Nominal2_FCB
17:25:45 Goedel_HFSet_Semantic: theory Nominal2.Nominal2
17:25:49 Goedel_HFSet_Semantic: theory Incompleteness.SyntaxN
17:25:57 Goedel_HFSet_Semantic: theory Incompleteness.Coding
17:25:57 Goedel_HFSet_Semantic: theory Incompleteness.Predicates
17:25:59 Goedel_HFSet_Semantic: theory Incompleteness.Sigma
17:26:05 Goedel_HFSet_Semantic: theory Incompleteness.Coding_Predicates
17:26:11 Goedel_HFSet_Semantic: theory Incompleteness.Functions
17:26:11 Goedel_HFSet_Semantic: theory Incompleteness.Pf_Predicates
17:26:13 Goedel_HFSet_Semantic: theory Incompleteness.Goedel_I
17:26:13 Goedel_HFSet_Semantic: theory Incompleteness.II_Prelims
17:26:15 Goedel_HFSet_Semantic: theory Incompleteness.Pseudo_Coding
17:26:16 Goedel_HFSet_Semantic: theory Incompleteness.Quote
17:26:17 Goedel_HFSet_Semantic: theory Goedel_HFSet_Semantic.Instance
17:32:37 Preparing Goedel_HFSet_Semantic/document ...
17:32:39 Finished Goedel_HFSet_Semantic/document (0:00:01 elapsed time)
17:32:39 Preparing Goedel_HFSet_Semantic/outline ...
17:32:41 Finished Goedel_HFSet_Semantic/outline (0:00:01 elapsed time)
17:32:41 Timing Goedel_HFSet_Semantic (8 threads, 427.052s elapsed time, 1597.622s cpu time, 18.657s GC time, factor 3.74)
17:32:41 Finished Goedel_HFSet_Semantic (0:07:09 elapsed time, 0:26:43 cpu time, factor 3.73)
17:32:41 Building HereditarilyFinite (on hpcisabelle/1) ...
17:32:43 HereditarilyFinite: theory HereditarilyFinite.HF
17:32:44 HereditarilyFinite: theory HereditarilyFinite.Ordinal
17:32:45 HereditarilyFinite: theory HereditarilyFinite.Finitary
17:32:45 HereditarilyFinite: theory HereditarilyFinite.Finite_Automata
17:32:45 HereditarilyFinite: theory HereditarilyFinite.Rank
17:32:45 HereditarilyFinite: theory HereditarilyFinite.OrdArith
17:33:01 Preparing HereditarilyFinite/document ...
17:33:06 Finished HereditarilyFinite/document (0:00:04 elapsed time)
17:33:06 Preparing HereditarilyFinite/outline ...
17:33:10 Finished HereditarilyFinite/outline (0:00:04 elapsed time)
17:33:10 Timing HereditarilyFinite (8 threads, 7.898s elapsed time, 49.367s cpu time, 0.697s GC time, factor 6.25)
17:33:10 Finished HereditarilyFinite (0:00:19 elapsed time, 0:01:10 cpu time, factor 3.63)
17:33:10 Building Three_Squares (on hpcisabelle/2) ...
17:33:13 Three_Squares: theory HOL-Computational_Algebra.Group_Closure
17:33:13 Three_Squares: theory Pure-ex.Guess
17:33:13 Three_Squares: theory HOL-Eisbach.Eisbach
17:33:13 Three_Squares: theory HOL-Computational_Algebra.Fraction_Field
17:33:13 Three_Squares: theory HOL-Combinatorics.Stirling
17:33:13 Three_Squares: theory HOL-Decision_Procs.Dense_Linear_Order
17:33:13 Three_Squares: theory HOL-Computational_Algebra.Nth_Powers
17:33:13 Three_Squares: theory HOL-Library.Adhoc_Overloading
17:33:13 Three_Squares: theory HOL-Computational_Algebra.Squarefree
17:33:13 Three_Squares: theory Three_Squares.Low_Dimensional_Linear_Algebra
17:33:14 Three_Squares: theory HOL-Number_Theory.Cong
17:33:14 Three_Squares: theory HOL-Library.Code_Abstract_Nat
17:33:14 Three_Squares: theory HOL-Library.Code_Target_Int
17:33:14 Three_Squares: theory HOL-Library.Code_Target_Nat
17:33:14 Three_Squares: theory HOL-Algebra.Congruence
17:33:14 Three_Squares: theory HOL-Library.Code_Target_Numeral
17:33:14 Three_Squares: theory HOL-Eisbach.Eisbach_Tools
17:33:14 Three_Squares: theory HOL-Library.Function_Algebras
17:33:14 Three_Squares: theory HOL-Library.Power_By_Squaring
17:33:14 Three_Squares: theory HOL-Number_Theory.Eratosthenes
17:33:15 Three_Squares: theory Bernoulli.Bernoulli
17:33:15 Three_Squares: theory HOL-Computational_Algebra.Field_as_Ring
17:33:15 Three_Squares: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
17:33:15 Three_Squares: theory HOL-Computational_Algebra.Normalized_Fraction
17:33:15 Three_Squares: theory HOL-Library.Going_To_Filter
17:33:15 Three_Squares: theory HOL-Library.Lattice_Algebras
17:33:16 Three_Squares: theory HOL-Algebra.Order
17:33:16 Three_Squares: theory HOL-Library.Log_Nat
17:33:16 Three_Squares: theory HOL-Number_Theory.Mod_Exp
17:33:16 Three_Squares: theory Bernoulli.Periodic_Bernpoly
17:33:16 Three_Squares: theory HOL-Computational_Algebra.Polynomial_Factorial
17:33:16 Three_Squares: theory Winding_Number_Eval.Missing_Topology
17:33:17 Three_Squares: theory HOL-Number_Theory.Fib
17:33:17 Three_Squares: theory HOL-Number_Theory.Prime_Powers
17:33:17 Three_Squares: theory HOL-Number_Theory.Totient
17:33:17 Three_Squares: theory HOL-Algebra.Lattice
17:33:17 Three_Squares: theory Winding_Number_Eval.Missing_Analysis
17:33:17 Three_Squares: theory Three_Squares.Quadratic_Forms
17:33:17 Three_Squares: theory Landau_Symbols.Group_Sort
17:33:18 Three_Squares: theory HOL-Computational_Algebra.Computational_Algebra
17:33:18 Three_Squares: theory Sturm_Tarski.PolyMisc
17:33:18 Three_Squares: theory Sturm_Tarski.Sturm_Tarski
17:33:18 Three_Squares: theory HOL-Algebra.Complete_Lattice
17:33:19 Three_Squares: theory Landau_Symbols.Landau_Real_Products
17:33:19 Three_Squares: theory HOL-Algebra.Group
17:33:19 Three_Squares: theory Budan_Fourier.BF_Misc
17:33:20 Three_Squares: theory Winding_Number_Eval.Missing_Algebraic
17:33:22 Three_Squares: theory Winding_Number_Eval.Missing_Transcendental
17:33:22 Three_Squares: theory HOL-Algebra.Coset
17:33:22 Three_Squares: theory HOL-Algebra.FiniteProduct
17:33:22 Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem
17:33:22 Three_Squares: theory HOL-Library.Interval
17:33:23 Three_Squares: theory HOL-Library.Float
17:33:23 Three_Squares: theory HOL-Algebra.Ring
17:33:24 Three_Squares: theory Landau_Symbols.Landau_Simprocs
17:33:25 Three_Squares: theory HOL-Algebra.Generated_Groups
17:33:25 Three_Squares: theory Landau_Symbols.Landau_More
17:33:26 Three_Squares: theory HOL-Library.Interval_Float
17:33:27 Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval
17:33:27 Three_Squares: theory HOL-Algebra.Elementary_Groups
17:33:28 Three_Squares: theory HOL-Decision_Procs.Approximation_Bounds
17:33:28 Three_Squares: theory HOL-Algebra.AbelCoset
17:33:28 Three_Squares: theory HOL-Algebra.Module
17:33:32 Three_Squares: theory HOL-Algebra.Ideal
17:33:36 Three_Squares: theory HOL-Algebra.RingHom
17:33:37 Three_Squares: theory HOL-Algebra.QuotRing
17:33:37 Three_Squares: theory HOL-Algebra.UnivPoly
17:33:41 Three_Squares: theory HOL-Algebra.IntRing
17:33:43 Three_Squares: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
17:33:54 Three_Squares: theory HOL-Algebra.Multiplicative_Group
17:33:59 Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
17:33:59 Three_Squares: theory HOL-Number_Theory.Residues
17:33:59 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom
17:33:59 Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
17:34:00 Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
17:34:00 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
17:34:00 Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds
17:34:02 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
17:34:02 Three_Squares: theory HOL-Number_Theory.Euler_Criterion
17:34:02 Three_Squares: theory HOL-Number_Theory.Pocklington
17:34:02 Three_Squares: theory Lehmer.Lehmer
17:34:03 Three_Squares: theory Pratt_Certificate.Pratt_Certificate
17:34:03 Three_Squares: theory HOL-Number_Theory.Gauss
17:34:03 Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity
17:34:03 Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots
17:34:03 Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds
17:34:03 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations
17:34:04 Three_Squares: theory Three_Squares.Residues_Properties
17:34:04 Three_Squares: theory HOL-Number_Theory.Number_Theory
17:34:05 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
17:34:05 Three_Squares: theory Dirichlet_L.Multiplicative_Characters
17:34:06 Three_Squares: theory Bernoulli.Bernoulli_FPS
17:34:06 Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
17:34:06 Three_Squares: theory Dirichlet_Series.Multiplicative_Function
17:34:06 Three_Squares: theory Bertrands_Postulate.Bertrand
17:34:06 Three_Squares: theory Dirichlet_Series.Dirichlet_Product
17:34:06 Three_Squares: theory Dirichlet_Series.Euler_Products
17:34:07 Three_Squares: theory Dirichlet_L.Dirichlet_Characters
17:34:07 Three_Squares: theory Dirichlet_Series.Dirichlet_Series
17:34:10 Three_Squares: theory Bernoulli.Bernoulli_Zeta
17:34:10 Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin
17:34:12 Three_Squares: theory Dirichlet_Series.Moebius_Mu
17:34:12 Three_Squares: theory Dirichlet_Series.More_Totient
17:34:12 Three_Squares: theory Dirichlet_Series.Liouville_Lambda
17:34:12 Three_Squares: theory Dirichlet_Series.Divisor_Count
17:34:13 Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
17:34:13 Three_Squares: theory Dirichlet_Series.Partial_Summation
17:34:15 Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
17:34:25 Three_Squares: theory Zeta_Function.Zeta_Library
17:34:25 Three_Squares: theory Zeta_Function.Zeta_Function
17:34:31 Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions
17:34:39 Three_Squares: theory Dirichlet_L.Dirichlet_Theorem
17:34:42 Three_Squares: theory Three_Squares.Three_Squares
17:38:21 Preparing Three_Squares/document ...
17:38:27 Finished Three_Squares/document (0:00:05 elapsed time)
17:38:27 Preparing Three_Squares/outline ...
17:38:30 Finished Three_Squares/outline (0:00:03 elapsed time)
17:38:30 Timing Three_Squares (8 threads, 267.549s elapsed time, 1652.343s cpu time, 92.735s GC time, factor 6.18)
17:38:30 Finished Three_Squares (0:05:05 elapsed time, 0:28:56 cpu time, factor 5.69)
17:38:30 Building Incompleteness (on hpcisabelle/3) ...
17:38:32 Incompleteness: theory FinFun.FinFun
17:38:34 Incompleteness: theory Nominal2.Nominal2_Base
17:38:40 Incompleteness: theory Nominal2.Nominal2_Abs
17:38:43 Incompleteness: theory Nominal2.Nominal2_FCB
17:38:43 Incompleteness: theory Nominal2.Nominal2
17:38:47 Incompleteness: theory Incompleteness.SyntaxN
17:38:54 Incompleteness: theory Incompleteness.Coding
17:38:55 Incompleteness: theory Incompleteness.Predicates
17:38:57 Incompleteness: theory Incompleteness.Sigma
17:39:03 Incompleteness: theory Incompleteness.Coding_Predicates
17:39:08 Incompleteness: theory Incompleteness.Functions
17:39:08 Incompleteness: theory Incompleteness.Pf_Predicates
17:39:11 Incompleteness: theory Incompleteness.Goedel_I
17:39:11 Incompleteness: theory Incompleteness.II_Prelims
17:39:13 Incompleteness: theory Incompleteness.Pseudo_Coding
17:39:14 Incompleteness: theory Incompleteness.Quote
17:39:15 Incompleteness: theory Incompleteness.Goedel_II
17:45:49 Preparing Incompleteness/document ...
17:46:10 Finished Incompleteness/document (0:00:21 elapsed time)
17:46:10 Preparing Incompleteness/outline ...
17:46:21 Finished Incompleteness/outline (0:00:10 elapsed time)
17:46:21 Timing Incompleteness (8 threads, 420.926s elapsed time, 1473.265s cpu time, 12.654s GC time, factor 3.50)
17:46:21 Finished Incompleteness (0:07:16 elapsed time, 0:25:04 cpu time, factor 3.44)
17:46:21 Running OmegaCatoidsQuantales (on hpcisabelle/4) ...
17:46:22 OmegaCatoidsQuantales: theory Catoids.Catoid
17:46:22 OmegaCatoidsQuantales: theory Kleene_Algebra.Signatures
17:46:22 OmegaCatoidsQuantales: theory Order_Lattice_Props.Sup_Lattice
17:46:23 OmegaCatoidsQuantales: theory Kleene_Algebra.Dioid
17:46:27 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid
17:46:31 OmegaCatoidsQuantales: theory Order_Lattice_Props.Order_Duality
17:46:40 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Catoid
17:46:40 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid_Collapse
17:46:41 OmegaCatoidsQuantales: theory Kleene_Algebra.Conway
17:46:42 OmegaCatoidsQuantales: theory Order_Lattice_Props.Order_Lattice_Props
17:46:53 OmegaCatoidsQuantales: theory Kleene_Algebra.Kleene_Algebra
17:46:57 OmegaCatoidsQuantales: theory Order_Lattice_Props.Galois_Connections
17:46:57 OmegaCatoidsQuantales: theory Order_Lattice_Props.Closure_Operators
17:46:59 OmegaCatoidsQuantales: theory Quantales.Quantales
17:47:03 OmegaCatoidsQuantales: theory KAD.Domain_Semiring
17:47:17 OmegaCatoidsQuantales: theory KAD.Antidomain_Semiring
17:47:37 OmegaCatoidsQuantales: theory KAD.Range_Semiring
17:48:00 OmegaCatoidsQuantales: theory KAD.Modal_Kleene_Algebra
17:48:00 OmegaCatoidsQuantales: theory Quantales_Converse.Modal_Kleene_Algebra_Var
17:48:06 OmegaCatoidsQuantales: theory Quantales.Quantale_Star
17:48:10 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Kleene_Algebra
17:48:10 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Kleene_Algebra
17:48:27 OmegaCatoidsQuantales: theory Quantales_Converse.Modal_Quantale
17:50:29 OmegaCatoidsQuantales: theory Catoids.Catoid_Lifting
17:50:29 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Quantale
17:50:29 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Quantale
17:52:09 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Catoid_Lifting
17:53:04 OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid_Lifting
17:53:13 Preparing OmegaCatoidsQuantales/document ...
17:53:19 Finished OmegaCatoidsQuantales/document (0:00:06 elapsed time)
17:53:19 Preparing OmegaCatoidsQuantales/outline ...
17:53:24 Finished OmegaCatoidsQuantales/outline (0:00:04 elapsed time)
17:53:24 Timing OmegaCatoidsQuantales (8 threads, 408.463s elapsed time, 999.983s cpu time, 34.818s GC time, factor 2.45)
17:53:24 Finished OmegaCatoidsQuantales (0:06:51 elapsed time, 0:16:48 cpu time, factor 2.45)
17:53:24 Building MDP-Rewards (on hpcisabelle/5) ...
17:53:27 MDP-Rewards: theory HOL-Library.Omega_Words_Fun
17:53:27 MDP-Rewards: theory MDP-Rewards.MDP_cont
17:53:27 MDP-Rewards: theory MDP-Rewards.Bounded_Functions
17:53:28 MDP-Rewards: theory MDP-Rewards.MDP_disc
17:53:30 MDP-Rewards: theory MDP-Rewards.Blinfun_Util
17:53:31 MDP-Rewards: theory MDP-Rewards.MDP_reward_Util
17:53:31 MDP-Rewards: theory MDP-Rewards.MDP_reward
17:53:53 Preparing MDP-Rewards/document ...
17:54:04 Finished MDP-Rewards/document (0:00:11 elapsed time)
17:54:04 Preparing MDP-Rewards/outline ...
17:54:11 Finished MDP-Rewards/outline (0:00:06 elapsed time)
17:54:11 Timing MDP-Rewards (8 threads, 10.919s elapsed time, 71.702s cpu time, 1.294s GC time, factor 6.57)
17:54:11 Finished MDP-Rewards (0:00:28 elapsed time, 0:01:43 cpu time, factor 3.68)
17:54:11 Building Jinja (on hpcisabelle/6) ...
17:54:13 Jinja: theory Jinja.Auxiliary
17:54:13 Jinja: theory Jinja.Semilat
17:54:13 Jinja: theory List-Index.List_Index
17:54:13 Jinja: theory Jinja.Type
17:54:14 Jinja: theory Jinja.Err
17:54:14 Jinja: theory Jinja.Hidden
17:54:14 Jinja: theory Jinja.Decl
17:54:14 Jinja: theory Jinja.TypeRel
17:54:15 Jinja: theory Jinja.Listn
17:54:15 Jinja: theory Jinja.Opt
17:54:15 Jinja: theory Jinja.Product
17:54:16 Jinja: theory Jinja.Semilattices
17:54:16 Jinja: theory Jinja.Typing_Framework_1
17:54:16 Jinja: theory Jinja.SemilatAlg
17:54:16 Jinja: theory Jinja.Typing_Framework_2
17:54:16 Jinja: theory Jinja.Value
17:54:16 Jinja: theory Jinja.Kildall_1
17:54:17 Jinja: theory Jinja.Kildall_2
17:54:17 Jinja: theory Jinja.LBVSpec
17:54:17 Jinja: theory Jinja.Typing_Framework_err
17:54:17 Jinja: theory Jinja.Objects
17:54:17 Jinja: theory Jinja.Exceptions
17:54:17 Jinja: theory Jinja.JVMState
17:54:17 Jinja: theory Jinja.JVMInstructions
17:54:17 Jinja: theory Jinja.Conform
17:54:17 Jinja: theory Jinja.Expr
17:54:18 Jinja: theory Jinja.State
17:54:18 Jinja: theory Jinja.SystemClasses
17:54:18 Jinja: theory Jinja.LBVComplete
17:54:18 Jinja: theory Jinja.LBVCorrect
17:54:18 Jinja: theory Jinja.WellForm
17:54:18 Jinja: theory Jinja.Abstract_BV
17:54:18 Jinja: theory Jinja.PCompiler
17:54:18 Jinja: theory Jinja.SemiType
17:54:19 Jinja: theory Jinja.JVM_SemiType
17:54:20 Jinja: theory Jinja.JVMExceptions
17:54:20 Jinja: theory Jinja.JVMExecInstr
17:54:20 Jinja: theory Jinja.Effect
17:54:20 Jinja: theory Jinja.JVMExec
17:54:21 Jinja: theory Jinja.JVMDefensive
17:54:22 Jinja: theory Jinja.JVMListExample
17:54:25 Jinja: theory Jinja.Examples
17:54:25 Jinja: theory Jinja.BigStep
17:54:26 Jinja: theory Jinja.SmallStep
17:54:26 Jinja: theory Jinja.WellType
17:54:26 Jinja: theory Jinja.WWellForm
17:54:27 Jinja: theory Jinja.Annotate
17:54:27 Jinja: theory Jinja.WellTypeRT
17:54:27 Jinja: theory Jinja.execute_WellType
17:54:30 Jinja: theory Jinja.DefAss
17:54:30 Jinja: theory Jinja.J1
17:54:30 Jinja: theory Jinja.execute_Bigstep
17:54:30 Jinja: theory Jinja.JWellForm
17:54:31 Jinja: theory Jinja.BVSpec
17:54:31 Jinja: theory Jinja.EffectMono
17:54:32 Jinja: theory Jinja.BVConform
17:54:32 Jinja: theory Jinja.TF_JVM
17:54:32 Jinja: theory Jinja.Equivalence
17:54:32 Jinja: theory Jinja.Compiler2
17:54:32 Jinja: theory Jinja.J1WellForm
17:54:32 Jinja: theory Jinja.LBVJVM
17:54:33 Jinja: theory Jinja.BVSpecTypeSafe
17:54:33 Jinja: theory Jinja.BVExec
17:54:34 Jinja: theory Jinja.Compiler1
17:54:34 Jinja: theory Jinja.Correctness2
17:54:35 Jinja: theory Jinja.Progress
17:54:35 Jinja: theory Jinja.BVNoTypeError
17:54:35 Jinja: theory Jinja.BVExample
17:54:36 Jinja: theory Jinja.Correctness1
17:54:37 Jinja: theory Jinja.TypeSafe
17:54:37 Jinja: theory Jinja.Compiler
17:54:38 Jinja: theory Jinja.TypeComp
17:55:08 Jinja: theory Jinja.Jinja
17:57:01 Preparing Jinja/document ...
17:57:12 Finished Jinja/document (0:00:10 elapsed time)
17:57:12 Preparing Jinja/outline ...
17:57:22 Finished Jinja/outline (0:00:10 elapsed time)
17:57:22 Timing Jinja (8 threads, 146.521s elapsed time, 1024.700s cpu time, 15.183s GC time, factor 6.99)
17:57:22 Finished Jinja (0:02:47 elapsed time, 0:17:48 cpu time, factor 6.40)
17:57:22 Running CAVA_LTL_Modelchecker (on hpcisabelle/7) ...
17:57:26 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
17:57:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
17:57:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
17:57:29 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
17:59:23 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
17:59:23 CAVA_LTL_Modelchecker: theory LTL.Rewriting
17:59:23 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
17:59:25 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
17:59:25 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
17:59:25 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
17:59:26 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
17:59:26 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
17:59:26 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
17:59:32 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
18:02:52 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
18:03:36 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
18:03:36 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
18:03:46 Preparing CAVA_LTL_Modelchecker/document ...
18:03:50 Finished CAVA_LTL_Modelchecker/document (0:00:04 elapsed time)
18:03:50 Preparing CAVA_LTL_Modelchecker/outline ...
18:03:53 Finished CAVA_LTL_Modelchecker/outline (0:00:03 elapsed time)
18:03:53 Timing CAVA_LTL_Modelchecker (8 threads, 378.837s elapsed time, 526.540s cpu time, 23.189s GC time, factor 1.39)
18:03:53 Finished CAVA_LTL_Modelchecker (0:06:23 elapsed time, 0:08:53 cpu time, factor 1.39)
18:03:53 Running Correctness_Algebras (on hpcisabelle/0) ...
18:03:56 Correctness_Algebras: theory LatticeProperties.Conj_Disj
18:03:56 Correctness_Algebras: theory LatticeProperties.WellFoundedTransitive
18:03:56 Correctness_Algebras: theory Stone_Algebras.Lattice_Basics
18:03:57 Correctness_Algebras: theory LatticeProperties.Complete_Lattice_Prop
18:03:57 Correctness_Algebras: theory MonoBoolTranAlgebra.Mono_Bool_Tran
18:03:58 Correctness_Algebras: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
18:04:05 Correctness_Algebras: theory MonoBoolTranAlgebra.Assertion_Algebra
18:04:14 Correctness_Algebras: theory Stone_Algebras.P_Algebras
18:04:14 Correctness_Algebras: theory Stone_Relation_Algebras.Fixpoints
18:04:16 Correctness_Algebras: theory Stone_Relation_Algebras.Semirings
18:04:28 Correctness_Algebras: theory Correctness_Algebras.Base
18:04:28 Correctness_Algebras: theory Correctness_Algebras.Lattice_Ordered_Semirings
18:04:28 Correctness_Algebras: theory Stone_Kleene_Relation_Algebras.Iterings
18:04:30 Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings
18:04:31 Correctness_Algebras: theory Correctness_Algebras.Monotonic_Boolean_Transformers
18:04:44 Correctness_Algebras: theory Correctness_Algebras.Approximation
18:04:44 Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings_Strict
18:04:44 Correctness_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Algebras
18:04:49 Correctness_Algebras: theory Stone_Relation_Algebras.Relation_Algebras
18:04:49 Correctness_Algebras: theory Subset_Boolean_Algebras.Subset_Boolean_Algebras
18:05:00 Correctness_Algebras: theory Correctness_Algebras.Omega_Algebras
18:05:05 Correctness_Algebras: theory Correctness_Algebras.Boolean_Semirings
18:05:05 Correctness_Algebras: theory Correctness_Algebras.N_Algebras
18:05:16 Correctness_Algebras: theory Correctness_Algebras.Recursion
18:05:19 Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings_Nonstrict
18:05:19 Correctness_Algebras: theory Correctness_Algebras.Capped_Omega_Algebras
18:05:19 Correctness_Algebras: theory Correctness_Algebras.General_Refinement_Algebras
18:05:28 Correctness_Algebras: theory Correctness_Algebras.Tests
18:05:29 Correctness_Algebras: theory Correctness_Algebras.N_Omega_Algebras
18:05:31 Correctness_Algebras: theory Correctness_Algebras.Complete_Tests
18:05:31 Correctness_Algebras: theory Correctness_Algebras.Preconditions
18:05:31 Correctness_Algebras: theory Correctness_Algebras.Relative_Domain
18:05:32 Correctness_Algebras: theory Correctness_Algebras.Domain
18:05:32 Correctness_Algebras: theory Correctness_Algebras.Test_Iterings
18:05:37 Correctness_Algebras: theory Correctness_Algebras.N_Semirings
18:05:38 Correctness_Algebras: theory Correctness_Algebras.Hoare
18:05:38 Correctness_Algebras: theory Correctness_Algebras.Pre_Post
18:05:40 Correctness_Algebras: theory Correctness_Algebras.Domain_Iterings
18:05:45 Correctness_Algebras: theory Correctness_Algebras.Complete_Domain
18:05:47 Correctness_Algebras: theory Correctness_Algebras.Relative_Modal
18:05:48 Correctness_Algebras: theory Correctness_Algebras.Extended_Designs
18:05:52 Correctness_Algebras: theory Correctness_Algebras.N_Semirings_Boolean
18:05:52 Correctness_Algebras: theory Correctness_Algebras.Recursion_Strict
18:05:55 Correctness_Algebras: theory Correctness_Algebras.N_Omega_Binary_Iterings
18:05:55 Correctness_Algebras: theory Correctness_Algebras.N_Relation_Algebras
18:05:59 Correctness_Algebras: theory Correctness_Algebras.Domain_Recursion
18:06:03 Correctness_Algebras: theory Correctness_Algebras.Hoare_Modal
18:06:10 Correctness_Algebras: theory Correctness_Algebras.N_Semirings_Modal
18:07:02 Correctness_Algebras: theory Correctness_Algebras.Pre_Post_Modal
18:07:20 Correctness_Algebras: theory Correctness_Algebras.Monotonic_Boolean_Transformers_Instances
18:10:26 Preparing Correctness_Algebras/document ...
18:10:45 Finished Correctness_Algebras/document (0:00:19 elapsed time)
18:10:45 Preparing Correctness_Algebras/outline ...
18:10:56 Finished Correctness_Algebras/outline (0:00:11 elapsed time)
18:10:57 Timing Correctness_Algebras (8 threads, 387.859s elapsed time, 1565.088s cpu time, 117.225s GC time, factor 4.04)
18:10:57 Finished Correctness_Algebras (0:06:31 elapsed time, 0:26:15 cpu time, factor 4.03)
18:10:57 Running MDP-Algorithms (on hpcisabelle/1) ...
18:11:00 MDP-Algorithms: theory Containers.Equal
18:11:00 MDP-Algorithms: theory Deriving.Comparator
18:11:00 MDP-Algorithms: theory Containers.Extend_Partial_Order
18:11:00 MDP-Algorithms: theory Containers.List_Fusion
18:11:00 MDP-Algorithms: theory HOL-Eisbach.Eisbach
18:11:00 MDP-Algorithms: theory Deriving.Derive_Manager
18:11:00 MDP-Algorithms: theory Deriving.Generator_Aux
18:11:00 MDP-Algorithms: theory HOL-Computational_Algebra.Fraction_Field
18:11:00 MDP-Algorithms: theory Containers.Closure_Set
18:11:00 MDP-Algorithms: theory HOL-Data_Structures.Array_Specs
18:11:00 MDP-Algorithms: theory HOL-Data_Structures.Cmp
18:11:00 MDP-Algorithms: theory HOL-Data_Structures.Define_Time_Function
18:11:00 MDP-Algorithms: theory HOL-Data_Structures.Less_False
18:11:00 MDP-Algorithms: theory Deriving.Equality_Generator
18:11:00 MDP-Algorithms: theory HOL-Data_Structures.Sorted_Less
18:11:01 MDP-Algorithms: theory HOL-Data_Structures.AList_Upd_Del
18:11:01 MDP-Algorithms: theory HOL-Data_Structures.List_Ins_Del
18:11:01 MDP-Algorithms: theory HOL-Data_Structures.Time_Funs
18:11:02 MDP-Algorithms: theory Deriving.Equality_Instances
18:11:02 MDP-Algorithms: theory Containers.Containers_Auxiliary
18:11:02 MDP-Algorithms: theory HOL-Data_Structures.Map_Specs
18:11:02 MDP-Algorithms: theory HOL-Data_Structures.Set_Specs
18:11:02 MDP-Algorithms: theory HOL-Library.Char_ord
18:11:02 MDP-Algorithms: theory HOL-Library.Code_Abstract_Nat
18:11:02 MDP-Algorithms: theory HOL-Library.Code_Target_Int
18:11:02 MDP-Algorithms: theory HOL-Algebra.Congruence
18:11:02 MDP-Algorithms: theory Deriving.Compare
18:11:02 MDP-Algorithms: theory Deriving.Comparator_Generator
18:11:03 MDP-Algorithms: theory HOL-Library.Code_Target_Nat
18:11:03 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Misc
18:11:03 MDP-Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
18:11:03 MDP-Algorithms: theory Containers.Lexicographic_Order
18:11:03 MDP-Algorithms: theory HOL-Library.Code_Target_Numeral
18:11:03 MDP-Algorithms: theory HOL-Library.IArray
18:11:03 MDP-Algorithms: theory HOL-Library.More_List
18:11:03 MDP-Algorithms: theory Containers.Containers_Generator
18:11:03 MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
18:11:04 MDP-Algorithms: theory Containers.Set_Linorder
18:11:04 MDP-Algorithms: theory HOL-Library.RBT_Impl
18:11:04 MDP-Algorithms: theory HOL-Data_Structures.Tree2
18:11:04 MDP-Algorithms: theory Deriving.Compare_Generator
18:11:04 MDP-Algorithms: theory HOL-Algebra.Order
18:11:04 MDP-Algorithms: theory Containers.Collection_Enum
18:11:04 MDP-Algorithms: theory Containers.Collection_Eq
18:11:04 MDP-Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
18:11:05 MDP-Algorithms: theory HOL-Data_Structures.Isin2
18:11:05 MDP-Algorithms: theory Deriving.Compare_Instances
18:11:05 MDP-Algorithms: theory HOL-Data_Structures.Lookup2
18:11:05 MDP-Algorithms: theory Containers.DList_Set
18:11:05 MDP-Algorithms: theory HOL-Data_Structures.RBT
18:11:05 MDP-Algorithms: theory Perron_Frobenius.Cancel_Card_Constraint
18:11:05 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Unsorted
18:11:05 MDP-Algorithms: theory HOL-Algebra.Lattice
18:11:05 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial
18:11:05 MDP-Algorithms: theory HOL-Library.Code_Real_Approx_By_Float
18:11:06 MDP-Algorithms: theory Jordan_Normal_Form.Conjugate
18:11:06 MDP-Algorithms: theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
18:11:06 MDP-Algorithms: theory HOL-Library.Tree_Real
18:11:06 MDP-Algorithms: theory HOL-Algebra.Complete_Lattice
18:11:07 MDP-Algorithms: theory HOL-Data_Structures.Braun_Tree
18:11:07 MDP-Algorithms: theory MDP-Algorithms.Backward_Induction
18:11:07 MDP-Algorithms: theory HOL-Data_Structures.Array_Braun
18:11:07 MDP-Algorithms: theory HOL-Algebra.Group
18:11:09 MDP-Algorithms: theory MDP-Algorithms.MDP_fin
18:11:09 MDP-Algorithms: theory HOL-Data_Structures.RBT_Set
18:11:10 MDP-Algorithms: theory HOL-Algebra.Coset
18:11:10 MDP-Algorithms: theory HOL-Algebra.FiniteProduct
18:11:11 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration
18:11:11 MDP-Algorithms: theory HOL-Algebra.Ring
18:11:12 MDP-Algorithms: theory HOL-Data_Structures.RBT_Map
18:11:14 MDP-Algorithms: theory MDP-Algorithms.Value_Iteration
18:11:14 MDP-Algorithms: theory MDP-Algorithms.DiffArray_Base
18:11:14 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom
18:11:15 MDP-Algorithms: theory Show.Show
18:11:16 MDP-Algorithms: theory MDP-Algorithms.Modified_Policy_Iteration
18:11:16 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods
18:11:18 MDP-Algorithms: theory HOL-Algebra.Module
18:11:18 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
18:11:18 MDP-Algorithms: theory Containers.Collection_Order
18:11:19 MDP-Algorithms: theory MDP-Algorithms.Splitting_Methods_Fin
18:11:19 MDP-Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
18:11:20 MDP-Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
18:11:20 MDP-Algorithms: theory Show.Show_Instances
18:11:21 MDP-Algorithms: theory VectorSpace.FunctionLemmas
18:11:21 MDP-Algorithms: theory VectorSpace.RingModuleFacts
18:11:22 MDP-Algorithms: theory Polynomial_Interpolation.Missing_Polynomial
18:11:22 MDP-Algorithms: theory Show.Shows_Literal
18:11:22 MDP-Algorithms: theory VectorSpace.MonoidSums
18:11:23 MDP-Algorithms: theory VectorSpace.LinearCombinations
18:11:23 MDP-Algorithms: theory Polynomial_Factorization.Order_Polynomial
18:11:23 MDP-Algorithms: theory Polynomial_Interpolation.Ring_Hom_Poly
18:11:23 MDP-Algorithms: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
18:11:24 MDP-Algorithms: theory Jordan_Normal_Form.Matrix
18:11:26 MDP-Algorithms: theory MDP-Algorithms.DiffArray_ST
18:11:30 MDP-Algorithms: theory VectorSpace.SumSpaces
18:11:30 MDP-Algorithms: theory VectorSpace.VectorSpace
18:11:30 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
18:11:30 MDP-Algorithms: theory Jordan_Normal_Form.Show_Matrix
18:11:30 MDP-Algorithms: theory Jordan_Normal_Form.Shows_Literal_Matrix
18:11:32 MDP-Algorithms: theory MDP-Algorithms.Code_Setup
18:11:33 MDP-Algorithms: theory Jordan_Normal_Form.Column_Operations
18:11:33 MDP-Algorithms: theory Jordan_Normal_Form.Determinant
18:11:36 MDP-Algorithms: theory Jordan_Normal_Form.Determinant_Impl
18:11:36 MDP-Algorithms: theory Jordan_Normal_Form.Char_Poly
18:11:38 MDP-Algorithms: theory Jordan_Normal_Form.Missing_VectorSpace
18:11:38 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form
18:11:42 MDP-Algorithms: theory Jordan_Normal_Form.VS_Connect
18:11:43 MDP-Algorithms: theory MDP-Algorithms.Fin_Code
18:11:43 MDP-Algorithms: theory MDP-Algorithms.GS_Code
18:11:43 MDP-Algorithms: theory MDP-Algorithms.MPI_Code
18:11:44 MDP-Algorithms: theory MDP-Algorithms.VI_Code
18:11:48 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Float
18:11:48 MDP-Algorithms: theory MDP-Algorithms.VI_Code_Export_Rat
18:11:51 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Float
18:11:51 MDP-Algorithms: theory MDP-Algorithms.Fin_Code_Export_Rat
18:11:52 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Float
18:11:52 MDP-Algorithms: theory MDP-Algorithms.MPI_Code_Export_Rat
18:11:53 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Float
18:11:53 MDP-Algorithms: theory MDP-Algorithms.GS_Code_Export_Rat
18:11:56 MDP-Algorithms: theory Jordan_Normal_Form.Gram_Schmidt
18:11:58 MDP-Algorithms: theory Jordan_Normal_Form.Schur_Decomposition
18:12:06 MDP-Algorithms: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
18:12:12 MDP-Algorithms: theory Jordan_Normal_Form.Spectral_Radius
18:12:12 MDP-Algorithms: theory Perron_Frobenius.HMA_Connect
18:12:17 MDP-Algorithms: theory MDP-Algorithms.Blinfun_To_Matrix
18:12:21 MDP-Algorithms: theory MDP-Algorithms.Policy_Iteration_Fin
18:12:24 MDP-Algorithms: theory Containers.RBT_ext
18:12:24 MDP-Algorithms: theory Deriving.RBT_Comparator_Impl
18:12:34 MDP-Algorithms: theory Containers.RBT_Mapping2
18:12:36 MDP-Algorithms: theory Containers.RBT_Set2
18:12:38 MDP-Algorithms: theory Containers.Set_Impl
18:13:04 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
18:13:07 MDP-Algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
18:13:09 MDP-Algorithms: theory Jordan_Normal_Form.Matrix_Impl
18:13:12 MDP-Algorithms: theory MDP-Algorithms.PI_Code
18:13:22 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Float
18:13:22 MDP-Algorithms: theory MDP-Algorithms.PI_Code_Export_Rat
18:17:42 Preparing MDP-Algorithms/document ...
18:18:00 Finished MDP-Algorithms/document (0:00:18 elapsed time)
18:18:00 Preparing MDP-Algorithms/outline ...
18:18:10 Finished MDP-Algorithms/outline (0:00:09 elapsed time)
18:18:10 Timing MDP-Algorithms (8 threads, 394.121s elapsed time, 2378.496s cpu time, 206.173s GC time, factor 6.03)
18:18:10 Finished MDP-Algorithms (0:06:39 elapsed time, 0:39:57 cpu time, factor 6.00)
18:18:10 Running SC_DOM_Components (on hpcisabelle/2) ...
18:18:18 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
18:18:31 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
18:18:39 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
18:19:00 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
18:24:09 Preparing SC_DOM_Components/document ...
18:24:19 Finished SC_DOM_Components/document (0:00:10 elapsed time)
18:24:19 Preparing SC_DOM_Components/outline ...
18:24:25 Finished SC_DOM_Components/outline (0:00:06 elapsed time)
18:24:25 Timing SC_DOM_Components (8 threads, 352.708s elapsed time, 2114.839s cpu time, 103.169s GC time, factor 6.00)
18:24:25 Finished SC_DOM_Components (0:05:57 elapsed time, 0:35:30 cpu time, factor 5.96)
18:24:25 Building Hermite (on hpcisabelle/3) ...
18:24:28 Hermite: theory Hermite.Hermite
18:24:33 Hermite: theory Hermite.Hermite_IArrays
18:25:12 Preparing Hermite/document ...
18:25:15 Finished Hermite/document (0:00:03 elapsed time)
18:25:15 Preparing Hermite/outline ...
18:25:17 Finished Hermite/outline (0:00:02 elapsed time)
18:25:17 Timing Hermite (8 threads, 29.657s elapsed time, 113.919s cpu time, 1.418s GC time, factor 3.84)
18:25:17 Finished Hermite (0:00:46 elapsed time, 0:02:22 cpu time, factor 3.09)
18:25:17 Building Regular-Sets (on hpcisabelle/4) ...
18:25:19 Regular-Sets: theory Regular-Sets.Regular_Set
18:25:23 Regular-Sets: theory Regular-Sets.Regular_Exp
18:25:23 Regular-Sets: theory Regular-Sets.Regular_Exp2
18:25:26 Regular-Sets: theory Regular-Sets.Equivalence_Checking2
18:25:27 Regular-Sets: theory Regular-Sets.Derivatives
18:25:27 Regular-Sets: theory Regular-Sets.NDerivative
18:25:27 Regular-Sets: theory Regular-Sets.Regexp_Constructions
18:25:27 Regular-Sets: theory Regular-Sets.Relation_Interpretation
18:25:31 Regular-Sets: theory Regular-Sets.Equivalence_Checking
18:25:31 Regular-Sets: theory Regular-Sets.pEquivalence_Checking
18:25:31 Regular-Sets: theory Regular-Sets.Regexp_Method
18:26:16 Preparing Regular-Sets/document ...
18:26:20 Finished Regular-Sets/document (0:00:04 elapsed time)
18:26:20 Preparing Regular-Sets/outline ...
18:26:24 Finished Regular-Sets/outline (0:00:03 elapsed time)
18:26:24 Timing Regular-Sets (8 threads, 44.203s elapsed time, 118.243s cpu time, 2.347s GC time, factor 2.67)
18:26:24 Finished Regular-Sets (0:00:58 elapsed time, 0:02:25 cpu time, factor 2.48)
18:26:24 Building Simple_Firewall (on hpcisabelle/5) ...
18:26:26 Simple_Firewall: theory Simple_Firewall.GroupF
18:26:26 Simple_Firewall: theory HOL-Library.Char_ord
18:26:26 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
18:26:26 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
18:26:26 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
18:26:26 Simple_Firewall: theory Simple_Firewall.List_Product_More
18:26:26 Simple_Firewall: theory Simple_Firewall.Option_Helpers
18:26:26 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
18:26:26 Simple_Firewall: theory Simple_Firewall.Iface
18:26:26 Simple_Firewall: theory Simple_Firewall.L4_Protocol
18:26:29 Simple_Firewall: theory Simple_Firewall.Simple_Packet
18:26:29 Simple_Firewall: theory Simple_Firewall.Primitives_toString
18:26:32 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
18:26:35 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
18:26:35 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
18:26:37 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
18:26:37 Simple_Firewall: theory Simple_Firewall.Shadowed
18:26:37 Simple_Firewall: theory Simple_Firewall.Service_Matrix
18:26:56 Preparing Simple_Firewall/document ...
18:27:04 Finished Simple_Firewall/document (0:00:08 elapsed time)
18:27:04 Preparing Simple_Firewall/outline ...
18:27:10 Finished Simple_Firewall/outline (0:00:06 elapsed time)
18:27:10 Timing Simple_Firewall (8 threads, 18.809s elapsed time, 88.728s cpu time, 2.298s GC time, factor 4.72)
18:27:10 Finished Simple_Firewall (0:00:30 elapsed time, 0:01:51 cpu time, factor 3.61)
18:27:10 Building Constructive_Cryptography (on hpcisabelle/6) ...
18:27:14 Constructive_Cryptography: theory Constructive_Cryptography.Resource
18:27:17 Constructive_Cryptography: theory Constructive_Cryptography.Converter
18:27:26 Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
18:27:27 Constructive_Cryptography: theory Constructive_Cryptography.Random_System
18:27:29 Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
18:27:29 Constructive_Cryptography: theory Constructive_Cryptography.Wiring
18:27:31 Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
18:27:32 Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
18:27:39 Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
18:27:39 Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
18:27:45 Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
18:27:47 Constructive_Cryptography: theory Constructive_Cryptography.Examples
18:29:19 Preparing Constructive_Cryptography/document ...
18:29:29 Finished Constructive_Cryptography/document (0:00:10 elapsed time)
18:29:29 Preparing Constructive_Cryptography/outline ...
18:29:35 Finished Constructive_Cryptography/outline (0:00:05 elapsed time)
18:29:35 Timing Constructive_Cryptography (8 threads, 104.731s elapsed time, 371.608s cpu time, 3.212s GC time, factor 3.55)
18:29:35 Finished Constructive_Cryptography (0:02:07 elapsed time, 0:06:53 cpu time, factor 3.25)
18:29:35 Building Stone_Kleene_Relation_Algebras (on hpcisabelle/7) ...
18:29:37 Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Iterings
18:29:51 Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Algebras
18:30:05 Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras
18:31:14 Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Matrix_Kleene_Algebras
18:31:14 Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Subalgebras
18:31:38 Preparing Stone_Kleene_Relation_Algebras/document ...
18:31:48 Finished Stone_Kleene_Relation_Algebras/document (0:00:09 elapsed time)
18:31:48 Preparing Stone_Kleene_Relation_Algebras/outline ...
18:31:52 Finished Stone_Kleene_Relation_Algebras/outline (0:00:04 elapsed time)
18:31:52 Timing Stone_Kleene_Relation_Algebras (8 threads, 109.471s elapsed time, 299.172s cpu time, 13.783s GC time, factor 2.73)
18:31:52 Finished Stone_Kleene_Relation_Algebras (0:02:02 elapsed time, 0:05:24 cpu time, factor 2.65)
18:31:53 Running CakeML_Codegen (on hpcisabelle/0) ...
18:31:55 CakeML_Codegen: theory Automatic_Refinement.Refine_Util_Bootstrap1
18:31:55 CakeML_Codegen: theory HOL-Data_Structures.Define_Time_Function
18:31:55 CakeML_Codegen: theory HOL-Data_Structures.Less_False
18:31:55 CakeML_Codegen: theory HOL-Data_Structures.Cmp
18:31:55 CakeML_Codegen: theory HOL-Library.AList
18:31:55 CakeML_Codegen: theory HOL-Library.Adhoc_Overloading
18:31:55 CakeML_Codegen: theory HOL-Data_Structures.Priority_Queue_Specs
18:31:55 CakeML_Codegen: theory HOL-Library.Conditional_Parametricity
18:31:55 CakeML_Codegen: theory Automatic_Refinement.Mk_Term_Antiquot
18:31:55 CakeML_Codegen: theory Automatic_Refinement.Mpat_Antiquot
18:31:55 CakeML_Codegen: theory HOL-Data_Structures.Sorted_Less
18:31:56 CakeML_Codegen: theory HOL-Data_Structures.List_Ins_Del
18:31:56 CakeML_Codegen: theory HOL-Library.Monad_Syntax
18:31:56 CakeML_Codegen: theory HOL-Library.Pattern_Aliases
18:31:56 CakeML_Codegen: theory Automatic_Refinement.Refine_Util
18:31:56 CakeML_Codegen: theory HOL-Library.Tree
18:31:56 CakeML_Codegen: theory HOL-Library.FSet
18:31:56 CakeML_Codegen: theory Amortized_Complexity.Amortized_Framework0
18:31:56 CakeML_Codegen: theory Huffman.Huffman
18:31:56 CakeML_Codegen: theory Root_Balanced_Tree.Time_Monad
18:31:56 CakeML_Codegen: theory HOL-Data_Structures.Set_Specs
18:31:57 CakeML_Codegen: theory Dict_Construction.Dict_Construction
18:32:00 CakeML_Codegen: theory HOL-Data_Structures.Tree2
18:32:00 CakeML_Codegen: theory HOL-Data_Structures.Tree_Set
18:32:00 CakeML_Codegen: theory HOL-Library.Tree_Multiset
18:32:00 CakeML_Codegen: theory HOL-Library.Tree_Real
18:32:00 CakeML_Codegen: theory HOL-Data_Structures.Leftist_Heap
18:32:00 CakeML_Codegen: theory HOL-Data_Structures.Balance
18:32:01 CakeML_Codegen: theory Pairing_Heap.Pairing_Heap_Tree
18:32:01 CakeML_Codegen: theory CakeML_Codegen.ML_Utils
18:32:01 CakeML_Codegen: theory HOL-Library.Finite_Map
18:32:01 CakeML_Codegen: theory CakeML_Codegen.Code_Utils
18:32:02 CakeML_Codegen: theory Root_Balanced_Tree.Root_Balanced_Tree
18:32:15 CakeML_Codegen: theory CakeML_Codegen.Compiler_Utils
18:32:15 CakeML_Codegen: theory CakeML_Codegen.CakeML_Utils
18:32:16 CakeML_Codegen: theory CakeML_Codegen.Test_Utils
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_Compiler
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_Preproc
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_Backend
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_CupCake
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_Rewriting
18:32:53 CakeML_Codegen: theory CakeML_Codegen.Doc_Terms
18:32:53 CakeML_Codegen: theory Constructor_Funs.Constructor_Funs
18:32:53 CakeML_Codegen: theory Datatype_Order_Generator.Derive_Aux
18:32:53 CakeML_Codegen: theory HOL-Library.State_Monad
18:32:53 CakeML_Codegen: theory HOL-Library.Disjoint_FSets
18:32:53 CakeML_Codegen: theory Higher_Order_Terms.Name
18:32:53 CakeML_Codegen: theory List-Index.List_Index
18:32:53 CakeML_Codegen: theory CakeML_Codegen.CakeML_Byte
18:32:53 CakeML_Codegen: theory CakeML_Codegen.CupCake_Env
18:32:53 CakeML_Codegen: theory Datatype_Order_Generator.Order_Generator
18:32:54 CakeML_Codegen: theory Higher_Order_Terms.Find_First
18:32:54 CakeML_Codegen: theory Higher_Order_Terms.Term_Utils
18:32:55 CakeML_Codegen: theory Higher_Order_Terms.Fresh_Monad
18:32:55 CakeML_Codegen: theory Higher_Order_Terms.Term_Class
18:32:55 CakeML_Codegen: theory Higher_Order_Terms.Fresh_Class
18:32:55 CakeML_Codegen: theory CakeML_Codegen.CupCake_Semantics
18:33:02 CakeML_Codegen: theory Higher_Order_Terms.Nterm
18:33:04 CakeML_Codegen: theory Higher_Order_Terms.Term
18:33:05 CakeML_Codegen: theory Higher_Order_Terms.Pats
18:33:05 CakeML_Codegen: theory CakeML_Codegen.Terms_Extras
18:33:05 CakeML_Codegen: theory Higher_Order_Terms.Term_to_Nterm
18:33:08 CakeML_Codegen: theory CakeML_Codegen.General_Rewriting
18:33:08 CakeML_Codegen: theory CakeML_Codegen.HOL_Datatype
18:33:10 CakeML_Codegen: theory CakeML_Codegen.Constructors
18:33:19 CakeML_Codegen: theory CakeML_Codegen.Consts
18:33:19 CakeML_Codegen: theory CakeML_Codegen.Strong_Term
18:33:19 CakeML_Codegen: theory CakeML_Codegen.CakeML_Setup
18:33:21 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Term
18:33:21 CakeML_Codegen: theory CakeML_Codegen.Sterm
18:33:21 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Nterm
18:33:21 CakeML_Codegen: theory CakeML_Codegen.Eval_Class
18:33:23 CakeML_Codegen: theory CakeML_Codegen.Embed
18:33:25 CakeML_Codegen: theory CakeML_Codegen.Pterm
18:33:25 CakeML_Codegen: theory CakeML_Codegen.Term_as_Value
18:33:26 CakeML_Codegen: theory CakeML_Codegen.Value
18:33:27 CakeML_Codegen: theory CakeML_Codegen.Eval_Instances
18:33:33 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm_Elim
18:33:46 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm
18:33:53 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Sterm
18:34:02 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Sterm
18:34:02 CakeML_Codegen: theory CakeML_Codegen.CakeML_Backend
18:34:03 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value
18:34:04 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value_ML
18:34:29 CakeML_Codegen: theory CakeML_Codegen.CakeML_Correctness
18:34:31 CakeML_Codegen: theory CakeML_Codegen.Composition
18:34:44 CakeML_Codegen: theory CakeML_Codegen.Compiler
18:35:07 CakeML_Codegen: theory Lazy_Case.Lazy_Case
18:35:08 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
18:35:08 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
18:35:08 CakeML_Codegen: theory CakeML_Codegen.Test_Composition
18:35:08 CakeML_Codegen: theory CakeML_Codegen.Test_Print
18:35:08 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
18:36:39 Build timed out (after 300 minutes). Marking the build as failed.
18:36:39 Build was aborted
18:41:00 Started calculate disk usage of build
18:41:00 Finished Calculation of disk usage of build in 0 seconds
18:41:01 Started calculate disk usage of workspace
18:41:02 Finished Calculation of disk usage of workspace in  1 second
18:41:03 No emails were triggered.
18:41:03 Finished: FAILURE