Skipping 32 KB.. Full Log

Session AFP/Gaussian_Integers (AFP)
00:17:16 Session AFP/Jordan_Normal_Form (AFP)
00:17:16 Session AFP/Farkas (AFP)
00:17:16 Session AFP/Isabelle_Marries_Dirac (AFP)
00:17:16 Session AFP/Knuth_Bendix_Order (AFP)
00:17:16 Session AFP/Functional_Ordered_Resolution_Prover (AFP)
00:17:16 Session AFP/Simple_Clause_Learning (AFP)
00:17:17 Session AFP/Regular_Tree_Relations (AFP)
00:17:17 Session AFP/FO_Theory_Rewriting (AFP)
00:17:17 Session AFP/Rewrite_Properties_Reduction (AFP)
00:17:17 Session AFP/Weighted_Path_Order (AFP)
00:17:17 Session AFP/Efficient_Weighted_Path_Order (AFP)
00:17:17 Session AFP/Given_Clause_Loops (AFP)
00:17:18 Session AFP/Multiset_Ordering_NPC (AFP)
00:17:18 Session AFP/Linear_Recurrences (AFP)
00:17:18 Session AFP/Polylog (AFP)
00:17:18 Session AFP/Lambert_Series (AFP)
00:17:18 Session AFP/Perron_Frobenius (AFP)
00:17:18 Session AFP/MDP-Algorithms (AFP)
00:17:19 Session AFP/Stochastic_Matrices (AFP)
00:17:19 Session AFP/Subresultants (AFP)
00:17:19 Session AFP/Berlekamp_Zassenhaus (AFP)
00:17:20 Session AFP/Algebraic_Numbers (AFP)
00:17:20 Session AFP/BenOr_Kozen_Reif (AFP)
00:17:20 Session AFP/LLL_Basis_Reduction (AFP)
00:17:20 Session AFP/CVP_Hardness (AFP)
00:17:20 Session AFP/LLL_Factorization (AFP)
00:17:20 Session AFP/Linear_Inequalities (AFP)
00:17:20 Session AFP/LP_Duality (AFP)
00:17:20 Session AFP/Linear_Programming (AFP)
00:17:20 Session AFP/Number_Theoretic_Transform (AFP)
00:17:20 Session AFP/CRYSTALS-Kyber (AFP)
00:17:20 Session AFP/Perfect_Fields (AFP)
00:17:20 Session AFP/Elimination_Of_Repeated_Factors (AFP)
00:17:20 Session AFP/Smith_Normal_Form (AFP)
00:17:21 Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
00:17:21 Session AFP/Polynomials (AFP)
00:17:22 Session AFP/Deep_Learning (AFP)
00:17:22 Session AFP/QHLProver (AFP)
00:17:22 Session AFP/Projective_Measurements (AFP)
00:17:23 Session AFP/Commuting_Hermitian (AFP)
00:17:23 Session AFP/TsirelsonBound (AFP)
00:17:23 Session AFP/Uncertainty_Principle (AFP)
00:17:23 Session AFP/Groebner_Bases (AFP)
00:17:23 Session AFP/Fishers_Inequality (AFP)
00:17:23 Session AFP/Hypergraph_Basics (AFP)
00:17:23 Session AFP/Hypergraph_Colourings (AFP)
00:17:23 Session AFP/Groebner_Macaulay (AFP)
00:17:24 Session AFP/Nullstellensatz (AFP)
00:17:24 Session AFP/Signature_Groebner (AFP)
00:17:24 Session AFP/Lambda_Free_KBOs (AFP)
00:17:24 Session AFP/Sumcheck_Protocol (AFP)
00:17:24 Session AFP/Symmetric_Polynomials (AFP)
00:17:24 Session AFP/Pi_Transcendental (AFP)
00:17:24 Session AFP/Power_Sum_Polynomials (AFP)
00:17:24 Session AFP/Hermite_Lindemann (AFP)
00:17:24 Session AFP/Factor_Algebraic_Polynomial (AFP)
00:17:24 Session AFP/Cubic_Quartic_Equations (AFP)
00:17:24 Session AFP/Linear_Recurrences_Solver (AFP)
00:17:25 Session AFP/Orient_Rewrite_Rule_Undecidable (AFP)
00:17:25 Session AFP/Schwartz_Zippel (AFP)
00:17:25 Session AFP/Virtual_Substitution (AFP)
00:17:26 Session AFP/Real_Impl (AFP)
00:17:26 Session AFP/Complex_Bounded_Operators_Dependencies (AFP)
00:17:26 Session AFP/Complex_Bounded_Operators (AFP)
00:17:26 Session AFP/Registers (AFP)
00:17:27 Session AFP/QR_Decomposition (AFP)
00:17:27 Session AFP/XML (AFP)
00:17:27 Session AFP/Van_Emde_Boas_Trees (AFP)
00:17:27 Session AFP/Dijkstra_Shortest_Path (AFP)
00:17:27 Session AFP/Koenigsberg_Friendship (AFP)
00:17:27 Session AFP/FOL_Seq_Calc2 (AFP)
00:17:27 Session AFP/Formal_SSA (AFP)
00:17:28 Session AFP/Minimal_SSA (AFP)
00:17:28 Session AFP/Gale_Shapley (AFP)
00:17:28 Session AFP/HOL-ODE-Numerics (AFP)
00:17:28 Session AFP/HOL-ODE-ARCH-COMP (AFP)
00:17:28 Session AFP/HOL-ODE-Examples (AFP large)
00:17:28 Session AFP/Lorenz_Approximation (AFP)
00:17:29 Session AFP/Lorenz_C0 (AFP large)
00:17:29 Session AFP/Lorenz_C1 (AFP large)
00:17:29 Session AFP/Poincare_Bendixson (AFP)
00:17:29 Session AFP/Picks_Theorem (AFP)
00:17:29 Session AFP/KnuthMorrisPratt (AFP)
00:17:29 Session AFP/Safe_Range_RC (AFP)
00:17:29 Session AFP/Transition_Systems_and_Automata (AFP)
00:17:29 Session AFP/Adaptive_State_Counting (AFP)
00:17:29 Session AFP/Buchi_Complementation (AFP)
00:17:29 Session AFP/LTL_Master_Theorem (AFP)
00:17:29 Session AFP/LTL_Normal_Form (AFP)
00:17:29 Session AFP/Partial_Order_Reduction (AFP)
00:17:30 Session AFP/SM_Base (AFP)
00:17:30 Session AFP/SM (AFP)
00:17:30 Session AFP/CAVA_Setup (AFP)
00:17:30 Session AFP/CAVA_LTL_Modelchecker (AFP)
00:17:30 Session AFP/Transitive-Closure (AFP)
00:17:30 Session AFP/KBPs (AFP)
00:17:30 Session AFP/LTL_to_DRA (AFP)
00:17:30 Session AFP/Network_Security_Policy_Verification (AFP)
00:17:31 Session AFP/Planarity_Certificates (AFP)
00:17:31 Session AFP/Tree-Automata (AFP)
00:17:31 Session AFP/Datatype_Order_Generator (AFP)
00:17:31 Session AFP/Higher_Order_Terms (AFP)
00:17:31 Session AFP/CakeML_Codegen (AFP)
00:17:31 Session AFP/Old_Datatype_Show (AFP)
00:17:31 Session AFP/Quantifier_Elimination_Hybrid (AFP)
00:17:32 Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
00:17:32 Session AFP/FSM_Tests (AFP)
00:17:32 Session AFP/Iptables_Semantics (AFP)
00:17:33 Session AFP/Iptables_Semantics_Examples (AFP)
00:17:33 Session AFP/LOFT (AFP)
00:17:33 Session AFP/Mersenne_Primes (AFP)
00:17:33 Session AFP/MiniSail (AFP)
00:17:33 Session AFP/Separation_Logic_Imperative_HOL (AFP)
00:17:33 Session AFP/Sepref_Prereq (AFP)
00:17:33 Session AFP/ROBDD (AFP)
00:17:33 Session AFP/Refine_Imperative_HOL (AFP)
00:17:33 Session AFP/BTree (AFP)
00:17:34 Session AFP/Floyd_Warshall (AFP)
00:17:34 Session AFP/Sepref_Basic (AFP)
00:17:34 Session AFP/Sepref_IICF (AFP)
00:17:34 Session AFP/Flow_Networks (AFP)
00:17:34 Session AFP/EdmondsKarp_Maxflow (AFP)
00:17:34 Session AFP/MFMC_Countable (AFP)
00:17:34 Session AFP/Probabilistic_While (AFP)
00:17:34 Session AFP/CryptHOL (AFP)
00:17:34 Session AFP/ABY3_Protocols (AFP)
00:17:34 Session AFP/Constructive_Cryptography (AFP)
00:17:34 Session AFP/Game_Based_Crypto (AFP)
00:17:34 Session AFP/CRYSTALS-Kyber_Security (AFP)
00:17:35 Session AFP/Multi_Party_Computation (AFP)
00:17:35 Session AFP/Sigma_Commit_Crypto (AFP)
00:17:35 Session AFP/Constructive_Cryptography_CM (AFP)
00:17:35 Session AFP/Executable_Randomized_Algorithms (AFP)
00:17:36 Session AFP/Finite_Fields (AFP)
00:17:37 Session AFP/Universal_Hash_Families (AFP)
00:17:38 Session AFP/Expander_Graphs (AFP)
00:17:38 Session AFP/Karatsuba (AFP)
00:17:39 Session AFP/Median_Method (AFP)
00:17:39 Session AFP/Frequency_Moments (AFP)
00:17:40 Session AFP/Approximate_Model_Counting (AFP)
00:17:40 Session AFP/Distributed_Distinct_Elements (AFP)
00:17:40 Session AFP/Derandomization_Conditional_Expectations (AFP)
00:17:40 Session AFP/Prpu_Maxflow (AFP)
00:17:40 Session AFP/Knuth_Morris_Pratt (AFP)
00:17:40 Session AFP/Kruskal (AFP)
00:17:41 Session AFP/PAC_Checker (AFP)
00:17:41 Session AFP/VerifyThis2018 (AFP)
00:17:41 Session AFP/VerifyThis2019 (AFP)
00:17:41 Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
00:17:41 Session AFP/UpDown_Scheme (AFP)
00:17:41 Session AFP/WebAssembly (AFP)
00:17:41 Session AFP/SPARCv8 (AFP)
00:17:42 Session AFP/Schoenhage_Strassen (AFP)
00:17:42 Session AFP/X86_Semantics (AFP)
00:17:42 Session AFP/ZFC_in_HOL (AFP)
00:17:43 Session AFP/CZH_Foundations (AFP)
00:17:43 Session AFP/CZH_Elementary_Categories (AFP)
00:17:43 Session AFP/CZH_Universal_Constructions (AFP)
00:17:43 Session AFP/Category3 (AFP)
00:17:44 Session AFP/MonoidalCategory (AFP)
00:17:44 Session AFP/Ordinal_Partitions (AFP)
00:17:44 Session AFP/Q0_Metatheory (AFP)
00:17:44 Session AFP/Q0_Soundness (AFP)
00:17:44 Session AFP/Wetzels_Problem (AFP)
00:17:44 Session FOL/ZF (main timing)
00:17:44 Session Doc/Logics_ZF (doc)
00:17:44 Session AFP/Recursion-Addition (AFP)
00:17:44 Session FOL/ZF-AC
00:17:44 Session FOL/ZF-Coind
00:17:44 Session FOL/ZF-Constructible
00:17:45 Session AFP/Delta_System_Lemma (AFP)
00:17:45 Session AFP/Transitive_Models (AFP)
00:17:45 Session AFP/Independence_CH (AFP)
00:17:45 Session AFP/Forcing (AFP)
00:17:45 Session FOL/ZF-IMP
00:17:45 Session FOL/ZF-Induct
00:17:45 Session FOL/ZF-UNITY (timing)
00:17:45 Session FOL/ZF-Resid
00:17:45 Session FOL/ZF-ex
00:18:09 Building Pure (on hpcisabelle/1) ...
00:18:38 Pure: theory Pure
00:18:39 Pure: theory ML_Bootstrap
00:18:39 Pure: theory Pure.Sessions
00:18:42 Timing Pure (1 threads, 1.165s elapsed time, 1.215s cpu time, 0.000s GC time, factor 1.04)
00:18:42 Finished Pure (0:00:32 elapsed time, 0:00:31 cpu time, factor 0.99)
00:18:42 Building HOL (on hpcisabelle/2) ...
00:18:45 HOL: theory Tools.Code_Generator
00:18:50 HOL: theory HOL.HOL
00:18:56 HOL: theory HOL.Argo
00:18:56 HOL: theory HOL.Orderings
00:18:56 HOL: theory HOL.Ctr_Sugar
00:19:00 HOL: theory HOL.Groups
00:19:02 HOL: theory HOL.SAT
00:19:03 HOL: theory HOL.Lattices
00:19:05 HOL: theory HOL.Boolean_Algebras
00:19:06 HOL: theory HOL.Set
00:19:07 HOL: theory HOL.Fun
00:19:07 HOL: theory HOL.Typedef
00:19:09 HOL: theory HOL.Complete_Lattices
00:19:09 HOL: theory HOL.Rings
00:19:12 HOL: theory HOL.Inductive
00:19:16 HOL: theory HOL.Product_Type
00:19:16 HOL: theory HOL.Sum_Type
00:19:18 HOL: theory HOL.Complete_Partial_Order
00:19:27 HOL: theory HOL.Nat
00:19:30 HOL: theory HOL.Meson
00:19:30 HOL: theory HOL.Fields
00:19:37 HOL: theory HOL.Relation
00:19:39 HOL: theory HOL.Finite_Set
00:19:41 HOL: theory HOL.Transitive_Closure
00:19:43 HOL: theory HOL.Wellfounded
00:19:44 HOL: theory HOL.Fun_Def_Base
00:19:44 HOL: theory HOL.Hilbert_Choice
00:19:44 HOL: theory HOL.Wfrec
00:19:44 HOL: theory HOL.Order_Relation
00:19:45 HOL: theory HOL.BNF_Wellorder_Relation
00:19:46 HOL: theory HOL.BNF_Wellorder_Embedding
00:19:46 HOL: theory HOL.Zorn
00:19:46 HOL: theory HOL.ATP
00:19:47 HOL: theory HOL.BNF_Wellorder_Constructions
00:19:48 HOL: theory HOL.BNF_Cardinal_Order_Relation
00:19:50 HOL: theory HOL.BNF_Cardinal_Arithmetic
00:19:51 HOL: theory HOL.BNF_Def
00:19:55 HOL: theory HOL.Metis
00:19:58 HOL: theory HOL.BNF_Composition
00:19:58 HOL: theory HOL.Basic_BNFs
00:20:00 HOL: theory HOL.BNF_Fixpoint_Base
00:20:06 HOL: theory HOL.BNF_Least_Fixpoint
00:20:10 HOL: theory HOL.Basic_BNF_LFPs
00:20:10 HOL: theory HOL.Equiv_Relations
00:20:10 HOL: theory HOL.Transfer
00:20:12 HOL: theory HOL.Num
00:20:12 HOL: theory HOL.Lifting
00:20:14 HOL: theory HOL.Option
00:20:14 HOL: theory HOL.Quotient
00:20:15 HOL: theory HOL.Extraction
00:20:15 HOL: theory HOL.Partial_Function
00:20:16 HOL: theory HOL.Power
00:20:16 HOL: theory HOL.Fun_Def
00:20:21 HOL: theory HOL.Groups_Big
00:20:25 HOL: theory HOL.Lattices_Big
00:20:25 HOL: theory HOL.Int
00:20:25 HOL: theory HOL.Lifting_Set
00:20:30 HOL: theory HOL.Euclidean_Rings
00:20:40 HOL: theory HOL.Parity
00:20:52 HOL: theory HOL.Divides
00:20:52 HOL: theory HOL.Numeral_Simprocs
00:20:52 HOL: theory HOL.Set_Interval
00:20:53 HOL: theory HOL.SMT
00:20:53 HOL: theory HOL.Semiring_Normalization
00:20:57 HOL: theory HOL.Groebner_Basis
00:21:00 HOL: theory HOL.Conditionally_Complete_Lattices
00:21:00 HOL: theory HOL.Filter
00:21:00 HOL: theory HOL.Presburger
00:21:05 HOL: theory HOL.Sledgehammer
00:21:10 HOL: theory HOL.List
00:21:22 HOL: theory HOL.Groups_List
00:21:22 HOL: theory HOL.Map
00:21:27 HOL: theory HOL.Bit_Operations
00:21:27 HOL: theory HOL.Enum
00:21:27 HOL: theory HOL.Factorial
00:21:28 HOL: theory HOL.Binomial
00:21:57 HOL: theory HOL.Code_Numeral
00:21:59 HOL: theory HOL.GCD
00:21:59 HOL: theory HOL.Random
00:21:59 HOL: theory HOL.String
00:22:04 HOL: theory HOL.BNF_Greatest_Fixpoint
00:22:04 HOL: theory HOL.Predicate
00:22:04 HOL: theory HOL.Typerep
00:22:05 HOL: theory HOL.Lazy_Sequence
00:22:06 HOL: theory HOL.Limited_Sequence
00:22:07 HOL: theory HOL.Code_Evaluation
00:22:08 HOL: theory HOL.Quickcheck_Random
00:22:11 HOL: theory HOL.Quickcheck_Narrowing
00:22:11 HOL: theory HOL.Quickcheck_Exhaustive
00:22:11 HOL: theory HOL.Random_Pred
00:22:11 HOL: theory HOL.Random_Sequence
00:22:17 HOL: theory HOL.Record
00:22:17 HOL: theory HOL.Predicate_Compile
00:22:19 HOL: theory HOL.Nitpick
00:22:20 HOL: theory HOL.Mirabelle
00:22:27 HOL: theory HOL.Nunchaku
00:22:29 HOL: theory Main
00:22:30 HOL: theory HOL.Archimedean_Field
00:22:30 HOL: theory HOL.Hull
00:22:30 HOL: theory HOL.Topological_Spaces
00:22:30 HOL: theory HOL.Modules
00:22:32 HOL: theory HOL.Vector_Spaces
00:22:42 HOL: theory HOL.Rat
00:22:45 HOL: theory HOL.Real
00:22:47 HOL: theory HOL.Binomial_Plus
00:22:47 HOL: theory HOL.Real_Vector_Spaces
00:23:10 HOL: theory HOL.Inequalities
00:23:10 HOL: theory HOL.Limits
00:23:20 HOL: theory HOL.Deriv
00:23:20 HOL: theory HOL.Series
00:23:23 HOL: theory HOL.NthRoot
00:23:23 HOL: theory HOL.Transcendental
00:23:30 HOL: theory HOL.Complex
00:23:31 HOL: theory HOL.MacLaurin
00:23:32 HOL: theory Complex_Main
00:24:30 Preparing HOL/document ...
00:26:25 Finished HOL/document (0:01:55 elapsed time)
00:26:25 Preparing HOL/outline ...
00:27:30 Finished HOL/outline (0:01:04 elapsed time)
00:27:31 Timing HOL (8 threads, 303.211s elapsed time, 1184.130s cpu time, 46.916s GC time, factor 3.91)
00:27:31 Finished HOL (0:05:31 elapsed time, 0:20:53 cpu time, factor 3.78)
00:27:31 Building HOL-Analysis (on hpcisabelle/3) ...
00:27:35 HOL-Analysis: theory HOL-Library.Cancellation
00:27:35 HOL-Analysis: theory HOL-Library.BNF_Corec
00:27:35 HOL-Analysis: theory HOL-Combinatorics.Transposition
00:27:35 HOL-Analysis: theory HOL-Library.FuncSet
00:27:35 HOL-Analysis: theory HOL-Library.Infinite_Set
00:27:35 HOL-Analysis: theory HOL-Library.Nat_Bijection
00:27:35 HOL-Analysis: theory HOL-Library.Old_Datatype
00:27:35 HOL-Analysis: theory HOL-Library.Phantom_Type
00:27:35 HOL-Analysis: theory HOL-Library.Product_Plus
00:27:36 HOL-Analysis: theory HOL-Library.Product_Order
00:27:36 HOL-Analysis: theory HOL-Library.Set_Algebras
00:27:36 HOL-Analysis: theory HOL-Real_Asymp.Inst_Existentials
00:27:36 HOL-Analysis: theory HOL-Analysis.Metric_Arith
00:27:36 HOL-Analysis: theory HOL-Library.Countable
00:27:36 HOL-Analysis: theory HOL-Library.Disjoint_Sets
00:27:36 HOL-Analysis: theory HOL-Analysis.Inner_Product
00:27:37 HOL-Analysis: theory HOL-Analysis.L2_Norm
00:27:37 HOL-Analysis: theory HOL-Library.Cardinality
00:27:37 HOL-Analysis: theory HOL-Library.Multiset
00:27:37 HOL-Analysis: theory HOL-Analysis.Operator_Norm
00:27:37 HOL-Analysis: theory HOL-Analysis.Poly_Roots
00:27:37 HOL-Analysis: theory HOL-Analysis.Product_Vector
00:27:37 HOL-Analysis: theory HOL-Library.Complex_Order
00:27:37 HOL-Analysis: theory HOL-Library.Discrete
00:27:38 HOL-Analysis: theory HOL-Library.Indicator_Function
00:27:38 HOL-Analysis: theory HOL-Library.Numeral_Type
00:27:38 HOL-Analysis: theory HOL-Library.Landau_Symbols
00:27:38 HOL-Analysis: theory HOL-Library.Liminf_Limsup
00:27:38 HOL-Analysis: theory HOL-Library.Nonpos_Ints
00:27:39 HOL-Analysis: theory HOL-Library.Countable_Set
00:27:39 HOL-Analysis: theory HOL-Library.Periodic_Fun
00:27:39 HOL-Analysis: theory HOL-Library.Sum_of_Squares
00:27:39 HOL-Analysis: theory HOL-Real_Asymp.Eventuallize
00:27:39 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
00:27:40 HOL-Analysis: theory HOL-Library.Equipollence
00:27:40 HOL-Analysis: theory HOL-Library.Set_Idioms
00:27:40 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
00:27:40 HOL-Analysis: theory HOL-Analysis.Abstract_Topology
00:27:41 HOL-Analysis: theory HOL-Analysis.Elementary_Topology
00:27:41 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
00:27:43 HOL-Analysis: theory HOL-Real_Asymp.Lazy_Eval
00:27:46 HOL-Analysis: theory HOL-Library.Order_Continuity
00:27:47 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
00:27:47 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
00:27:48 HOL-Analysis: theory HOL-Library.Extended_Nat
00:27:48 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
00:27:48 HOL-Analysis: theory HOL-Combinatorics.Permutations
00:27:48 HOL-Analysis: theory HOL-Analysis.Norm_Arith
00:27:49 HOL-Analysis: theory HOL-Analysis.Abstract_Limits
00:27:50 HOL-Analysis: theory HOL-Analysis.FSigma
00:27:50 HOL-Analysis: theory HOL-Analysis.Sum_Topology
00:27:50 HOL-Analysis: theory HOL-Analysis.Affine
00:27:50 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
00:27:52 HOL-Analysis: theory HOL-Library.Extended_Real
00:27:52 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion
00:27:53 HOL-Analysis: theory HOL-Analysis.Cartesian_Space
00:27:53 HOL-Analysis: theory HOL-Analysis.Convex
00:27:56 HOL-Analysis: theory HOL-Analysis.Connected
00:27:57 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
00:27:57 HOL-Analysis: theory HOL-Analysis.Determinants
00:27:57 HOL-Analysis: theory HOL-Analysis.Function_Topology
00:27:59 HOL-Analysis: theory HOL-Analysis.Product_Topology
00:28:00 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
00:28:00 HOL-Analysis: theory HOL-Analysis.T1_Spaces
00:28:00 HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
00:28:01 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
00:28:01 HOL-Analysis: theory HOL-Analysis.Function_Metric
00:28:01 HOL-Analysis: theory HOL-Analysis.Isolated
00:28:02 HOL-Analysis: theory HOL-Analysis.Infinite_Sum
00:28:02 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
00:28:02 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
00:28:04 HOL-Analysis: theory HOL-Analysis.Measurable
00:28:05 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
00:28:05 HOL-Analysis: theory HOL-Analysis.Line_Segment
00:28:05 HOL-Analysis: theory HOL-Analysis.Measure_Space
00:28:05 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
00:28:05 HOL-Analysis: theory HOL-Analysis.Tagged_Division
00:28:06 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
00:28:07 HOL-Analysis: theory HOL-Analysis.Summation_Tests
00:28:08 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
00:28:08 HOL-Analysis: theory HOL-Analysis.Starlike
00:28:09 HOL-Analysis: theory HOL-Analysis.Caratheodory
00:28:10 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
00:28:10 HOL-Analysis: theory HOL-Analysis.Path_Connected
00:28:12 HOL-Analysis: theory HOL-Analysis.Locally
00:28:12 HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
00:28:12 HOL-Analysis: theory HOL-Analysis.Homotopy
00:28:14 HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
00:28:14 HOL-Analysis: theory HOL-Analysis.Homeomorphism
00:28:14 HOL-Analysis: theory HOL-Analysis.Sparse_In
00:28:15 HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
00:28:18 HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
00:28:18 HOL-Analysis: theory HOL-Computational_Algebra.Primes
00:28:22 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
00:28:22 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
00:28:22 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
00:28:24 HOL-Analysis: theory HOL-Analysis.Derivative
00:28:26 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
00:28:27 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
00:28:27 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
00:28:27 HOL-Analysis: theory HOL-Analysis.Borel_Space
00:28:27 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
00:28:28 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
00:28:28 HOL-Analysis: theory HOL-Analysis.Cross3
00:28:28 HOL-Analysis: theory HOL-Analysis.Polytope
00:28:29 HOL-Analysis: theory HOL-Analysis.Lipschitz
00:28:29 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
00:28:30 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
00:28:31 HOL-Analysis: theory HOL-Analysis.Urysohn
00:28:32 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
00:28:32 HOL-Analysis: theory HOL-Real_Asymp.Real_Asymp
00:28:32 HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
00:28:32 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
00:28:33 HOL-Analysis: theory HOL-Analysis.Regularity
00:28:33 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
00:28:33 HOL-Analysis: theory HOL-Analysis.Retracts
00:28:37 HOL-Analysis: theory HOL-Analysis.Smooth_Paths
00:28:38 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
00:28:38 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
00:28:38 HOL-Analysis: theory HOL-Analysis.Infinite_Products
00:28:38 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
00:28:38 HOL-Analysis: theory HOL-Analysis.FPS_Convergence
00:28:40 HOL-Analysis: theory HOL-Analysis.Embed_Measure
00:28:40 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
00:28:41 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
00:28:42 HOL-Analysis: theory HOL-Analysis.Complete_Measure
00:28:42 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
00:28:43 HOL-Analysis: theory HOL-Analysis.Set_Integral
00:28:43 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
00:28:44 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
00:28:45 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
00:28:47 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
00:28:47 HOL-Analysis: theory HOL-Analysis.Integral_Test
00:28:47 HOL-Analysis: theory HOL-Analysis.Kronecker_Approximation_Theorem
00:28:49 HOL-Analysis: theory HOL-Analysis.Further_Topology
00:28:49 HOL-Analysis: theory HOL-Analysis.Gamma_Function
00:28:49 HOL-Analysis: theory HOL-Analysis.Improper_Integral
00:28:49 HOL-Analysis: theory HOL-Analysis.Interval_Integral
00:28:49 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
00:28:53 HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
00:28:53 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
00:28:54 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
00:28:55 HOL-Analysis: theory HOL-Analysis.Simplex_Content
00:28:56 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
00:28:57 HOL-Analysis: theory HOL-Analysis.Ball_Volume
00:28:57 HOL-Analysis: theory HOL-Analysis.Analysis
00:38:39 Preparing HOL-Analysis/document ...
00:41:43 Finished HOL-Analysis/document (0:03:03 elapsed time)
00:41:43 Preparing HOL-Analysis/manual ...
00:42:07 Finished HOL-Analysis/manual (0:00:24 elapsed time)
00:42:08 Timing HOL-Analysis (8 threads, 573.750s elapsed time, 3929.569s cpu time, 398.287s GC time, factor 6.85)
00:42:08 Finished HOL-Analysis (0:10:51 elapsed time, 1:08:50 cpu time, factor 6.34)
00:42:08 Building Ordinary_Differential_Equations (on hpcisabelle/4) ...
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
00:42:11 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Code_Cardinality
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
00:42:11 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
00:42:11 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
00:42:12 Ordinary_Differential_Equations: theory Triangle.Angles
00:42:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
00:42:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
00:42:12 Ordinary_Differential_Equations: theory List-Index.List_Index
00:42:12 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
00:42:12 Ordinary_Differential_Equations: theory Triangle.Triangle
00:42:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
00:42:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
00:42:18 Ordinary_Differential_Equations: theory HOL-Library.Interval
00:42:19 Ordinary_Differential_Equations: theory HOL-Library.Float
00:42:21 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
00:42:21 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral_Float
00:42:22 Ordinary_Differential_Equations: theory HOL-Library.Interval_Float
00:42:23 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
00:42:26 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
00:42:27 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
00:42:28 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
00:42:28 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
00:42:29 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
00:42:31 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
00:42:32 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
00:42:37 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
00:42:37 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
00:42:37 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
00:42:40 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
00:42:42 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs
00:43:19 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
00:43:21 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
00:44:55 Preparing Ordinary_Differential_Equations/document ...
00:45:11 Finished Ordinary_Differential_Equations/document (0:00:16 elapsed time)
00:45:11 Preparing Ordinary_Differential_Equations/outline ...
00:45:18 Finished Ordinary_Differential_Equations/outline (0:00:06 elapsed time)
00:45:18 Timing Ordinary_Differential_Equations (8 threads, 141.455s elapsed time, 713.815s cpu time, 11.359s GC time, factor 5.05)
00:45:18 Finished Ordinary_Differential_Equations (0:02:44 elapsed time, 0:12:40 cpu time, factor 4.63)
00:45:18 Building HOL-ODE-Numerics (on hpcisabelle/5) ...
00:45:21 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
00:45:21 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
00:45:21 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
00:45:21 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
00:45:21 HOL-ODE-Numerics: theory Deriving.Generator_Aux
00:45:21 HOL-ODE-Numerics: theory Deriving.Comparator
00:45:21 HOL-ODE-Numerics: theory Deriving.Derive_Manager
00:45:21 HOL-ODE-Numerics: theory HOL-Library.AList
00:45:21 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
00:45:21 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
00:45:21 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
00:45:22 HOL-ODE-Numerics: theory HOL-ex.Quicksort
00:45:22 HOL-ODE-Numerics: theory HOL-Library.Char_ord
00:45:22 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
00:45:22 HOL-ODE-Numerics: theory Deriving.Equality_Generator
00:45:22 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
00:45:22 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
00:45:22 HOL-ODE-Numerics: theory HOL-Library.Option_ord
00:45:22 HOL-ODE-Numerics: theory HOL-Library.Parallel
00:45:22 HOL-ODE-Numerics: theory HOL-Library.Type_Length
00:45:23 HOL-ODE-Numerics: theory Deriving.Equality_Instances
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
00:45:23 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
00:45:23 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
00:45:23 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
00:45:23 HOL-ODE-Numerics: theory Deriving.Compare
00:45:24 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
00:45:24 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
00:45:24 HOL-ODE-Numerics: theory HOL-Library.Mapping
00:45:24 HOL-ODE-Numerics: theory HOL-Library.Word
00:45:24 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
00:45:24 HOL-ODE-Numerics: theory Deriving.Countable_Generator
00:45:25 HOL-ODE-Numerics: theory Deriving.Compare_Generator
00:45:25 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
00:45:25 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
00:45:25 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
00:45:25 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
00:45:25 HOL-ODE-Numerics: theory Deriving.Compare_Instances
00:45:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
00:45:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
00:45:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
00:45:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
00:45:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
00:45:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
00:45:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
00:45:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
00:45:27 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
00:45:27 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
00:45:28 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
00:45:28 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
00:45:28 HOL-ODE-Numerics: theory Show.Show
00:45:28 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
00:45:28 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
00:45:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
00:45:30 HOL-ODE-Numerics: theory Show.Show_Instances
00:45:30 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
00:45:30 HOL-ODE-Numerics: theory Collections.SetIterator
00:45:31 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
00:45:31 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
00:45:31 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
00:45:31 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
00:45:32 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
00:45:33 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
00:45:33 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
00:45:35 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
00:45:35 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
00:45:35 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
00:45:36 HOL-ODE-Numerics: theory Word_Lib.More_Divides
00:45:36 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
00:45:36 HOL-ODE-Numerics: theory Collections.Assoc_List
00:45:36 HOL-ODE-Numerics: theory Collections.Proper_Iterator
00:45:36 HOL-ODE-Numerics: theory Collections.SetIteratorGA
00:45:36 HOL-ODE-Numerics: theory Word_Lib.More_Word
00:45:36 HOL-ODE-Numerics: theory Collections.Diff_Array
00:45:36 HOL-ODE-Numerics: theory Collections.It_to_It
00:45:36 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
00:45:37 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
00:45:37 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
00:45:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
00:45:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
00:45:38 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
00:45:38 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
00:45:38 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
00:45:38 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
00:45:39 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
00:45:40 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
00:45:41 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
00:45:41 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
00:45:42 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
00:45:42 HOL-ODE-Numerics: theory Collections.Intf_Comp
00:45:42 HOL-ODE-Numerics: theory Collections.Idx_Iterator
00:45:42 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
00:45:43 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
00:45:44 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
00:45:44 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
00:45:44 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
00:45:45 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
00:45:45 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
00:45:45 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
00:45:49 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
00:45:49 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
00:45:50 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
00:45:50 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
00:45:50 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
00:45:50 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
00:45:52 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
00:45:53 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
00:45:53 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
00:45:53 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
00:45:57 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
00:45:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
00:45:57 HOL-ODE-Numerics: theory Native_Word.Uint
00:45:57 HOL-ODE-Numerics: theory Native_Word.Uint32
00:45:57 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
00:45:58 HOL-ODE-Numerics: theory Collections.Gen_Iterator
00:45:58 HOL-ODE-Numerics: theory Collections.Intf_Map
00:45:58 HOL-ODE-Numerics: theory Collections.Intf_Set
00:45:59 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
00:45:59 HOL-ODE-Numerics: theory Collections.Iterator
00:45:59 HOL-ODE-Numerics: theory Collections.HashCode
00:45:59 HOL-ODE-Numerics: theory Collections.Array_Iterator
00:46:00 HOL-ODE-Numerics: theory Collections.Gen_Map
00:46:00 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
00:46:00 HOL-ODE-Numerics: theory Collections.Gen_Set
00:46:00 HOL-ODE-Numerics: theory Collections.Impl_List_Set
00:46:00 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
00:46:00 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
00:46:01 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
00:46:01 HOL-ODE-Numerics: theory Collections.Impl_List_Map
00:46:01 HOL-ODE-Numerics: theory Collections.Intf_Hash
00:46:02 HOL-ODE-Numerics: theory Deriving.Hash_Generator
00:46:02 HOL-ODE-Numerics: theory Collections.Gen_Hash
00:46:02 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
00:46:03 HOL-ODE-Numerics: theory Deriving.Hash_Instances
00:46:03 HOL-ODE-Numerics: theory Deriving.Derive
00:46:38 HOL-ODE-Numerics: theory HOL-Library.RBT
00:46:38 HOL-ODE-Numerics: theory Collections.RBT_add
00:46:39 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
00:46:39 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
00:46:40 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
00:46:50 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
00:46:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
00:46:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
00:46:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
00:46:59 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
00:47:02 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
00:47:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
00:47:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
00:47:05 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
00:47:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
00:47:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
00:47:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
00:47:06 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
00:47:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
00:47:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
00:47:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
00:47:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
00:47:22 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
00:47:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
00:47:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
00:47:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
00:47:28 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
00:47:29 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
00:47:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
00:47:47 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
00:48:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
00:48:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
00:48:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
00:48:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
00:48:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
00:48:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
00:48:41 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
00:48:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
00:48:54 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
00:49:19 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
00:50:11 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
00:58:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
00:58:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
01:00:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
01:01:52 Timing HOL-ODE-Numerics (8 threads, 908.338s elapsed time, 4998.211s cpu time, 255.125s GC time, factor 5.50)
01:01:52 Finished HOL-ODE-Numerics (0:16:25 elapsed time, 1:26:31 cpu time, factor 5.27)
01:01:52 Building ZFC_in_HOL (on hpcisabelle/6) ...
01:01:53 ZFC_in_HOL: theory HOL-Library.Infinite_Set
01:01:53 ZFC_in_HOL: theory HOL-Cardinals.Fun_More
01:01:53 ZFC_in_HOL: theory HOL-Cardinals.Order_Union
01:01:53 ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More
01:01:53 ZFC_in_HOL: theory HOL-Library.Old_Datatype
01:01:53 ZFC_in_HOL: theory HOL-Library.Nat_Bijection
01:01:53 ZFC_in_HOL: theory HOL-Library.FuncSet
01:01:54 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension
01:01:54 ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More
01:01:54 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation
01:01:55 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding
01:01:55 ZFC_in_HOL: theory HOL-Library.Countable
01:01:55 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions
01:01:56 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation
01:01:56 ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic
01:01:56 ZFC_in_HOL: theory HOL-Library.Countable_Set
01:01:57 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic
01:01:57 ZFC_in_HOL: theory HOL-Cardinals.Cardinals
01:01:57 ZFC_in_HOL: theory HOL-Library.Equipollence
01:01:57 ZFC_in_HOL: theory HOL-Analysis.Continuum_Not_Denumerable
01:01:58 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library
01:01:58 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL
01:01:59 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals
01:02:02 ZFC_in_HOL: theory ZFC_in_HOL.Kirby
01:02:02 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses
01:02:02 ZFC_in_HOL: theory ZFC_in_HOL.Ordinal_Exp
01:02:03 ZFC_in_HOL: theory ZFC_in_HOL.Cantor_NF
01:02:03 ZFC_in_HOL: theory ZFC_in_HOL.General_Cardinals
01:02:43 Preparing ZFC_in_HOL/document ...
01:02:53 Finished ZFC_in_HOL/document (0:00:10 elapsed time)
01:02:53 Preparing ZFC_in_HOL/outline ...
01:02:58 Finished ZFC_in_HOL/outline (0:00:05 elapsed time)
01:02:58 Timing ZFC_in_HOL (8 threads, 39.097s elapsed time, 256.542s cpu time, 4.634s GC time, factor 6.56)
01:02:58 Finished ZFC_in_HOL (0:00:49 elapsed time, 0:04:36 cpu time, factor 5.57)
01:02:58 Building CZH_Foundations (on hpcisabelle/7) ...
01:03:00 CZH_Foundations: theory CZH_Foundations.CZH_Sets_MIF
01:03:00 CZH_Foundations: theory CZH_Foundations.CZH_Utilities
01:03:00 CZH_Foundations: theory HOL-Eisbach.Eisbach
01:03:00 CZH_Foundations: theory Conditional_Simplification.CS_Tools
01:03:00 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum_Library
01:03:00 CZH_Foundations: theory CZH_Foundations.CZH_Introduction
01:03:00 CZH_Foundations: theory Intro_Dest_Elim.IHOL_IDE
01:03:00 CZH_Foundations: theory HOL-Library.Rewrite
01:03:00 CZH_Foundations: theory Conditional_Simplification.IHOL_CS
01:03:01 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum
01:03:02 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Introduction
01:03:03 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Sets
01:03:04 CZH_Foundations: theory CZH_Foundations.CZH_Sets_BRelations
01:03:04 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Nat
01:03:07 CZH_Foundations: theory CZH_Foundations.CZH_Sets_IF
01:03:08 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Equipollence
01:03:08 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Ordinals
01:03:08 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Cardinality
01:03:09 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FSequences
01:03:11 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FBRelations
01:03:12 CZH_Foundations: theory CZH_Foundations.CZH_Sets_NOP
01:03:12 CZH_Foundations: theory CZH_Foundations.CZH_Sets_VNHS
01:03:14 CZH_Foundations: theory CZH_Foundations.CZH_DG_Introduction
01:03:14 CZH_Foundations: theory CZH_Foundations.CZH_Sets_ZQR
01:03:20 CZH_Foundations: theory CZH_Foundations.CZH_EX_Replacement
01:03:20 CZH_Foundations: theory CZH_Foundations.CZH_DG_Digraph
01:03:20 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Introduction
01:03:20 CZH_Foundations: theory CZH_Foundations.CZH_EX_TS
01:03:22 CZH_Foundations: theory CZH_Foundations.CZH_EX_Algebra
01:03:22 CZH_Foundations: theory CZH_Foundations.CZH_DG_DGHM
01:03:23 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_Digraph
01:03:23 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semicategory
01:03:24 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Conclusions
01:03:27 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semicategory
01:03:40 CZH_Foundations: theory CZH_Foundations.CZH_DG_TDGHM
01:03:45 CZH_Foundations: theory CZH_Foundations.CZH_DG_GRPH
01:03:45 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_DGHM
01:03:45 CZH_Foundations: theory CZH_Foundations.CZH_DG_Subdigraph
01:03:45 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semifunctor
01:03:48 CZH_Foundations: theory CZH_Foundations.CZH_DG_Simple
01:03:48 CZH_Foundations: theory CZH_Foundations.CZH_DG_PDigraph
01:03:48 CZH_Foundations: theory CZH_Foundations.CZH_SMC_GRPH
01:03:51 CZH_Foundations: theory CZH_Foundations.CZH_DG_Rel
01:03:52 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_TDGHM
01:03:53 CZH_Foundations: theory CZH_Foundations.CZH_DG_Par
01:03:55 CZH_Foundations: theory CZH_Foundations.CZH_DG_Set
01:03:58 CZH_Foundations: theory CZH_Foundations.CZH_DG_Conclusions
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_DG_SemiCAT
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_NTSMCF
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Subsemicategory
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_PSemicategory
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Rel
01:04:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semifunctor
01:04:18 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Simple
01:04:18 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_NTSMCF
01:04:18 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Par
01:04:19 CZH_Foundations: theory CZH_Foundations.CZH_SMC_SemiCAT
01:04:20 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Set
01:04:29 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Conclusions
01:05:13 Preparing CZH_Foundations/document ...
01:06:35 Finished CZH_Foundations/document (0:01:22 elapsed time)
01:06:35 Preparing CZH_Foundations/outline ...
01:07:22 Finished CZH_Foundations/outline (0:00:46 elapsed time)
01:07:22 Timing CZH_Foundations (8 threads, 121.726s elapsed time, 776.802s cpu time, 67.340s GC time, factor 6.38)
01:07:22 Finished CZH_Foundations (0:02:12 elapsed time, 0:13:18 cpu time, factor 6.01)
01:07:23 Building CZH_Elementary_Categories (on hpcisabelle/0) ...
01:07:24 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Introduction
01:07:26 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Category
01:07:34 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Functor
01:07:34 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
01:07:37 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_GRPH
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_NTCF
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Order
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_CAT
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Rel
01:07:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
01:08:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Parallel
01:08:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SS
01:08:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
01:08:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
01:08:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
01:08:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Par
01:08:24 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_PCategory
01:08:24 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Simple
01:08:24 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
01:08:26 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Comma
01:08:27 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Discrete
01:08:33 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
01:08:37 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_CAT
01:08:38 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CAT
01:08:43 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_FUNCT
01:08:46 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Set
01:08:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Hom
01:08:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
01:09:00 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_FUNCT
01:09:04 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
01:09:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Cone
01:09:19 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
01:09:37 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Cone
01:09:56 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
01:17:00 Preparing CZH_Elementary_Categories/document ...
01:19:01 Finished CZH_Elementary_Categories/document (0:02:01 elapsed time)
01:19:01 Preparing CZH_Elementary_Categories/outline ...
01:19:58 Finished CZH_Elementary_Categories/outline (0:00:56 elapsed time)
01:19:58 Timing CZH_Elementary_Categories (8 threads, 562.524s elapsed time, 2529.566s cpu time, 229.464s GC time, factor 4.50)
01:19:58 Finished CZH_Elementary_Categories (0:09:34 elapsed time, 0:42:34 cpu time, factor 4.44)
01:19:59 Building Lorenz_Approximation (on hpcisabelle/1) ...
01:20:02 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
01:20:07 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
01:20:28 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
01:24:35 Timing Lorenz_Approximation (8 threads, 250.317s elapsed time, 626.326s cpu time, 37.699s GC time, factor 2.50)
01:24:35 Finished Lorenz_Approximation (0:04:35 elapsed time, 0:11:15 cpu time, factor 2.45)
01:24:35 Running Lorenz_C0 (on hpcisabelle/2) ...
01:24:39 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
01:49:00 Timing Lorenz_C0 (8 threads, 1459.970s elapsed time, 11516.565s cpu time, 25.543s GC time, factor 7.89)
01:49:00 Finished Lorenz_C0 (0:24:24 elapsed time, 3:12:02 cpu time, factor 7.87)
01:49:00 Building HOL-Library (on hpcisabelle/3) ...
01:49:01 HOL-Library: theory HOL-Library.README
01:49:01 HOL-Library: theory HOL-Library.AList
01:49:01 HOL-Library: theory HOL-Library.Adhoc_Overloading
01:49:01 HOL-Library: theory HOL-Library.BNF_Corec
01:49:01 HOL-Library: theory HOL-Library.BNF_Axiomatization
01:49:01 HOL-Library: theory HOL-Library.Case_Converter
01:49:01 HOL-Library: theory HOL-Library.Cancellation
01:49:01 HOL-Library: theory HOL-Library.Centered_Division
01:49:01 HOL-Library: theory HOL-Library.Char_ord
01:49:02 HOL-Library: theory HOL-Library.Code_Abstract_Char
01:49:02 HOL-Library: theory HOL-Library.Code_Abstract_Nat
01:49:02 HOL-Library: theory HOL-Library.Code_Prolog
01:49:02 HOL-Library: theory HOL-Library.Monad_Syntax
01:49:02 HOL-Library: theory HOL-Library.Code_Binary_Nat
01:49:02 HOL-Library: theory HOL-Library.State_Monad
01:49:02 HOL-Library: theory HOL-Library.Code_Lazy
01:49:02 HOL-Library: theory HOL-Library.Simps_Case_Conv
01:49:02 HOL-Library: theory HOL-Library.Extended
01:49:03 HOL-Library: theory HOL-Library.Multiset
01:49:03 HOL-Library: theory HOL-Library.Code_Target_Nat
01:49:04 HOL-Library: theory HOL-Library.Code_Target_Int
01:49:04 HOL-Library: theory HOL-Library.Code_Test
01:49:04 HOL-Library: theory HOL-Library.Code_Target_Numeral
01:49:04 HOL-Library: theory HOL-Library.Combine_PER
01:49:04 HOL-Library: theory HOL-Library.Comparator
01:49:04 HOL-Library: theory HOL-Library.DAList
01:49:04 HOL-Library: theory HOL-Library.Complete_Partial_Order2
01:49:05 HOL-Library: theory HOL-Library.Conditional_Parametricity
01:49:05 HOL-Library: theory HOL-Library.Confluence
01:49:05 HOL-Library: theory HOL-Library.Datatype_Records
01:49:05 HOL-Library: theory HOL-Library.Confluent_Quotient
01:49:05 HOL-Library: theory HOL-Library.Debug
01:49:06 HOL-Library: theory HOL-Library.Dlist
01:49:06 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
01:49:06 HOL-Library: theory HOL-Library.Fun_Lexorder
01:49:06 HOL-Library: theory HOL-Library.FuncSet
01:49:06 HOL-Library: theory HOL-Library.Function_Algebras
01:49:06 HOL-Library: theory HOL-Library.Function_Division
01:49:06 HOL-Library: theory HOL-Library.Groups_Big_Fun
01:49:06 HOL-Library: theory HOL-Library.IArray
01:49:07 HOL-Library: theory HOL-Library.Infinite_Set
01:49:07 HOL-Library: theory HOL-Library.Disjoint_Sets
01:49:07 HOL-Library: theory HOL-Library.LaTeXsugar
01:49:09 HOL-Library: theory HOL-Library.Lattice_Constructions
01:49:09 HOL-Library: theory HOL-Library.Omega_Words_Fun
01:49:09 HOL-Library: theory HOL-Library.ListVector
01:49:09 HOL-Library: theory HOL-Library.List_Lenlexorder
01:49:09 HOL-Library: theory HOL-Library.List_Lexorder
01:49:09 HOL-Library: theory HOL-Library.Mapping
01:49:09 HOL-Library: theory HOL-Library.More_List
01:49:09 HOL-Library: theory HOL-Library.NList
01:49:09 HOL-Library: theory HOL-Library.Nat_Bijection
01:49:09 HOL-Library: theory HOL-Library.Poly_Mapping
01:49:10 HOL-Library: theory HOL-Library.Stream
01:49:12 HOL-Library: theory HOL-Library.Old_Datatype
01:49:13 HOL-Library: theory HOL-Library.AList_Mapping
01:49:13 HOL-Library: theory HOL-Library.Old_Recdef
01:49:13 HOL-Library: theory HOL-Library.Open_State_Syntax
01:49:14 HOL-Library: theory HOL-Library.Option_ord
01:49:14 HOL-Library: theory HOL-Library.Parallel
01:49:14 HOL-Library: theory HOL-Library.Pattern_Aliases
01:49:14 HOL-Library: theory HOL-Library.Phantom_Type
01:49:14 HOL-Library: theory HOL-Library.Power_By_Squaring
01:49:14 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
01:49:15 HOL-Library: theory HOL-Library.DAList_Multiset
01:49:15 HOL-Library: theory HOL-Library.Multiset_Order
01:49:15 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
01:49:15 HOL-Library: theory HOL-Library.Preorder
01:49:15 HOL-Library: theory HOL-Library.Cardinality
01:49:16 HOL-Library: theory HOL-Library.Product_Lexorder
01:49:16 HOL-Library: theory HOL-Library.Product_Plus
01:49:16 HOL-Library: theory HOL-Library.Quotient_Syntax
01:49:16 HOL-Library: theory HOL-Library.Quotient_Option
01:49:16 HOL-Library: theory HOL-Library.Quotient_Product
01:49:16 HOL-Library: theory HOL-Library.Quotient_Set
01:49:16 HOL-Library: theory HOL-Library.Product_Order
01:49:16 HOL-Library: theory HOL-Library.Quotient_Sum
01:49:16 HOL-Library: theory HOL-Library.Quotient_Type
01:49:17 HOL-Library: theory HOL-Library.RBT_Impl
01:49:17 HOL-Library: theory HOL-Library.Quotient_List
01:49:17 HOL-Library: theory HOL-Library.Realizers
01:49:18 HOL-Library: theory HOL-Library.Reflection
01:49:18 HOL-Library: theory HOL-Library.Finite_Lattice
01:49:18 HOL-Library: theory HOL-Library.Refute
01:49:18 HOL-Library: theory HOL-Library.Rewrite
01:49:18 HOL-Library: theory HOL-Library.Set_Algebras
01:49:19 HOL-Library: theory HOL-Library.Code_Cardinality
01:49:19 HOL-Library: theory HOL-Library.Numeral_Type
01:49:19 HOL-Library: theory HOL-Library.Signed_Division
01:49:19 HOL-Library: theory HOL-Library.Sorting_Algorithms
01:49:20 HOL-Library: theory HOL-Library.Sublist
01:49:21 HOL-Library: theory HOL-Library.Transitive_Closure_Table
01:49:21 HOL-Library: theory HOL-Library.Tree
01:49:21 HOL-Library: theory HOL-Library.Type_Length
01:49:21 HOL-Library: theory HOL-Library.Uprod
01:49:21 HOL-Library: theory HOL-Library.While_Combinator
01:49:22 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
01:49:22 HOL-Library: theory HOL-Library.Z2
01:49:22 HOL-Library: theory HOL-Library.Saturated
01:49:22 HOL-Library: theory HOL-Library.Word
01:49:22 HOL-Library: theory HOL-Library.Countable
01:49:22 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
01:49:22 HOL-Library: theory HOL-Library.Prefix_Order
01:49:22 HOL-Library: theory HOL-Library.Subseq_Order
01:49:23 HOL-Library: theory HOL-Library.Complex_Order
01:49:23 HOL-Library: theory HOL-Library.Diagonal_Subsequence
01:49:23 HOL-Library: theory HOL-Library.Discrete
01:49:23 HOL-Library: theory HOL-Library.Going_To_Filter
01:49:23 HOL-Library: theory HOL-Library.Indicator_Function
01:49:23 HOL-Library: theory HOL-Library.Infinite_Typeclass
01:49:23 HOL-Library: theory HOL-Library.Landau_Symbols
01:49:23 HOL-Library: theory HOL-Library.Lattice_Algebras
01:49:23 HOL-Library: theory HOL-Library.Liminf_Limsup
01:49:23 HOL-Library: theory HOL-Library.Countable_Set
01:49:23 HOL-Library: theory HOL-Library.Tree_Multiset
01:49:24 HOL-Library: theory HOL-Library.FSet
01:49:24 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
01:49:24 HOL-Library: theory HOL-Library.Countable_Set_Type
01:49:26 HOL-Library: theory HOL-Library.Equipollence
01:49:26 HOL-Library: theory HOL-Library.Set_Idioms
01:49:26 HOL-Library: theory HOL-Library.Log_Nat
01:49:27 HOL-Library: theory HOL-Library.Lub_Glb
01:49:27 HOL-Library: theory HOL-Library.Ramsey
01:49:27 HOL-Library: theory HOL-Library.Nonpos_Ints
01:49:27 HOL-Library: theory HOL-Library.OptionalSugar
01:49:27 HOL-Library: theory HOL-Library.Order_Continuity
01:49:27 HOL-Library: theory HOL-Library.Periodic_Fun
01:49:27 HOL-Library: theory HOL-Library.Quadratic_Discriminant
01:49:28 HOL-Library: theory HOL-Library.Real_Mod
01:49:28 HOL-Library: theory HOL-Library.Sum_of_Squares
01:49:28 HOL-Library: theory HOL-Library.Finite_Map
01:49:28 HOL-Library: theory HOL-Library.Extended_Nat
01:49:28 HOL-Library: theory HOL-Library.Tree_Real
01:49:29 HOL-Library: theory HOL-Library.Extended_Real
01:49:29 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
01:49:29 HOL-Library: theory HOL-Library.Interval
01:49:31 HOL-Library: theory HOL-Library.Float
01:49:34 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
01:49:34 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
01:49:34 HOL-Library: theory HOL-Library.Interval_Float
01:49:44 HOL-Library: theory HOL-Library.Disjoint_FSets
01:49:44 HOL-Library: theory HOL-Library.Library
01:50:26 HOL-Library: theory HOL-Library.RBT
01:50:27 HOL-Library: theory HOL-Library.RBT_Mapping
01:50:27 HOL-Library: theory HOL-Library.RBT_Set
01:52:41 Preparing HOL-Library/document ...
01:53:46 Finished HOL-Library/document (0:01:04 elapsed time)
01:53:46 Preparing HOL-Library/outline ...
01:54:23 Finished HOL-Library/outline (0:00:37 elapsed time)
01:54:24 Timing HOL-Library (8 threads, 181.097s elapsed time, 1213.219s cpu time, 57.200s GC time, factor 6.70)
01:54:24 Finished HOL-Library (0:03:36 elapsed time, 0:21:38 cpu time, factor 6.00)
01:54:24 Running CZH_Universal_Constructions (on hpcisabelle/4) ...
01:54:26 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
01:54:26 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
01:54:26 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
01:54:40 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
01:55:21 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
01:55:21 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
01:55:22 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
01:55:22 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
01:55:22 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
01:55:22 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
01:55:45 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
01:56:11 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
01:56:14 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
01:56:17 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
01:56:55 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
01:57:31 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
01:57:41 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
02:16:25 Preparing CZH_Universal_Constructions/document ...
02:17:31 Finished CZH_Universal_Constructions/document (0:01:06 elapsed time)
02:17:31 Preparing CZH_Universal_Constructions/outline ...
02:17:56 Finished CZH_Universal_Constructions/outline (0:00:25 elapsed time)
02:17:57 Timing CZH_Universal_Constructions (8 threads, 1316.351s elapsed time, 5095.974s cpu time, 304.147s GC time, factor 3.87)
02:17:57 Finished CZH_Universal_Constructions (0:22:00 elapsed time, 1:25:06 cpu time, factor 3.87)
02:17:57 Building HOL-Computational_Algebra (on hpcisabelle/5) ...
02:17:59 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
02:17:59 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
02:17:59 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
02:18:10 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
02:18:24 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
02:18:24 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
02:18:24 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
02:18:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
02:18:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
02:18:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
02:18:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
02:18:46 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
02:18:46 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
02:18:46 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
02:18:47 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
02:18:51 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
02:19:21 Preparing HOL-Computational_Algebra/document ...
02:19:46 Finished HOL-Computational_Algebra/document (0:00:25 elapsed time)
02:19:46 Preparing HOL-Computational_Algebra/outline ...
02:19:59 Finished HOL-Computational_Algebra/outline (0:00:12 elapsed time)
02:19:59 Timing HOL-Computational_Algebra (8 threads, 66.273s elapsed time, 268.015s cpu time, 5.872s GC time, factor 4.04)
02:19:59 Finished HOL-Computational_Algebra (0:01:22 elapsed time, 0:04:59 cpu time, factor 3.64)
02:19:59 Building HOL-Algebra (on hpcisabelle/6) ...
02:20:02 HOL-Algebra: theory HOL-Algebra.README
02:20:02 HOL-Algebra: theory HOL-Cardinals.Fun_More
02:20:02 HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
02:20:02 HOL-Algebra: theory HOL-Algebra.Congruence
02:20:02 HOL-Algebra: theory HOL-Algebra.Exponent
02:20:02 HOL-Algebra: theory HOL-Cardinals.Order_Union
02:20:02 HOL-Algebra: theory HOL-Combinatorics.Transposition
02:20:02 HOL-Algebra: theory HOL-Combinatorics.Permutations
02:20:02 HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
02:20:03 HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
02:20:03 HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
02:20:03 HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
02:20:03 HOL-Algebra: theory HOL-Algebra.Order
02:20:04 HOL-Algebra: theory HOL-Combinatorics.Cycles
02:20:04 HOL-Algebra: theory HOL-Combinatorics.List_Permutation
02:20:04 HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
02:20:05 HOL-Algebra: theory HOL-Algebra.Lattice
02:20:05 HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
02:20:06 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
02:20:08 HOL-Algebra: theory HOL-Algebra.Galois_Connection
02:20:08 HOL-Algebra: theory HOL-Algebra.Group
02:20:11 HOL-Algebra: theory HOL-Algebra.Bij
02:20:11 HOL-Algebra: theory HOL-Algebra.Coset
02:20:11 HOL-Algebra: theory HOL-Algebra.FiniteProduct
02:20:11 HOL-Algebra: theory HOL-Algebra.Ring
02:20:13 HOL-Algebra: theory HOL-Algebra.Group_Action
02:20:13 HOL-Algebra: theory HOL-Algebra.Left_Coset
02:20:13 HOL-Algebra: theory HOL-Algebra.SimpleGroups
02:20:13 HOL-Algebra: theory HOL-Algebra.SndIsomorphismGrp
02:20:13 HOL-Algebra: theory HOL-Algebra.Sylow
02:20:13 HOL-Algebra: theory HOL-Algebra.Generated_Groups
02:20:14 HOL-Algebra: theory HOL-Algebra.Divisibility
02:20:14 HOL-Algebra: theory HOL-Algebra.Zassenhaus
02:20:15 HOL-Algebra: theory HOL-Algebra.Solvable_Groups
02:20:15 HOL-Algebra: theory HOL-Algebra.Elementary_Groups
02:20:15 HOL-Algebra: theory HOL-Algebra.Sym_Groups
02:20:17 HOL-Algebra: theory HOL-Algebra.Exact_Sequence
02:20:17 HOL-Algebra: theory HOL-Algebra.Product_Groups
02:20:18 HOL-Algebra: theory HOL-Algebra.AbelCoset
02:20:18 HOL-Algebra: theory HOL-Algebra.Module
02:20:18 HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
02:20:23 HOL-Algebra: theory HOL-Algebra.Ideal
02:20:26 HOL-Algebra: theory HOL-Algebra.Ideal_Product
02:20:26 HOL-Algebra: theory HOL-Algebra.RingHom
02:20:28 HOL-Algebra: theory HOL-Algebra.QuotRing
02:20:28 HOL-Algebra: theory HOL-Algebra.UnivPoly
02:20:32 HOL-Algebra: theory HOL-Algebra.IntRing
02:20:32 HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
02:20:34 HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
02:20:44 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
02:20:49 HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
02:20:49 HOL-Algebra: theory HOL-Algebra.Subrings
02:20:52 HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
02:20:53 HOL-Algebra: theory HOL-Algebra.Generated_Rings
02:20:55 HOL-Algebra: theory HOL-Algebra.Generated_Fields
02:20:58 HOL-Algebra: theory HOL-Algebra.Polynomials
02:21:19 HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
02:22:00 HOL-Algebra: theory HOL-Algebra.Finite_Extensions
02:22:00 HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
02:22:14 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
02:22:24 HOL-Algebra: theory HOL-Algebra.Algebra
02:22:24 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure_Type
02:23:07 Preparing HOL-Algebra/document ...
02:23:36 Finished HOL-Algebra/document (0:00:28 elapsed time)
02:23:36 Preparing HOL-Algebra/outline ...
02:23:49 Finished HOL-Algebra/outline (0:00:13 elapsed time)
02:23:50 Timing HOL-Algebra (8 threads, 157.180s elapsed time, 786.672s cpu time, 79.620s GC time, factor 5.00)
02:23:50 Finished HOL-Algebra (0:03:04 elapsed time, 0:14:07 cpu time, factor 4.59)
02:23:50 Building Automatic_Refinement (on hpcisabelle/7) ...
02:23:51 Automatic_Refinement: theory Automatic_Refinement.Prio_List
02:23:51 Automatic_Refinement: theory HOL-Eisbach.Eisbach
02:23:51 Automatic_Refinement: theory Automatic_Refinement.Foldi
02:23:51 Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
02:23:51 Automatic_Refinement: theory HOL-Library.Cancellation
02:23:51 Automatic_Refinement: theory HOL-Library.Option_ord
02:23:51 Automatic_Refinement: theory HOL-Library.Infinite_Set
02:23:51 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
02:23:51 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
02:23:52 Automatic_Refinement: theory Automatic_Refinement.Refine_Util
02:23:53 Automatic_Refinement: theory HOL-Library.Multiset
02:23:53 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
02:23:53 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
02:23:53 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
02:23:54 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
02:23:54 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
02:23:54 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
02:23:54 Automatic_Refinement: theory Automatic_Refinement.Select_Solve
02:23:59 Automatic_Refinement: theory HOL-ex.Quicksort
02:24:00 Automatic_Refinement: theory Automatic_Refinement.Misc
02:24:06 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
02:24:08 Automatic_Refinement: theory Automatic_Refinement.Relators
02:24:08 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
02:24:10 Automatic_Refinement: theory Automatic_Refinement.Param_Tool
02:24:10 Automatic_Refinement: theory Automatic_Refinement.Param_HOL
02:24:11 Automatic_Refinement: theory Automatic_Refinement.Parametricity
02:24:11 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
02:24:11 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
02:24:11 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
02:24:12 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
02:24:13 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
02:24:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
02:24:19 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
02:24:29 Preparing Automatic_Refinement/document ...
02:24:32 Finished Automatic_Refinement/document (0:00:03 elapsed time)
02:24:32 Preparing Automatic_Refinement/outline ...
02:24:35 Finished Automatic_Refinement/outline (0:00:02 elapsed time)
02:24:35 Timing Automatic_Refinement (8 threads, 27.762s elapsed time, 119.549s cpu time, 3.911s GC time, factor 4.31)
02:24:35 Finished Automatic_Refinement (0:00:38 elapsed time, 0:02:19 cpu time, factor 3.65)
02:24:35 Building Refine_Monadic (on hpcisabelle/0) ...
02:24:36 Refine_Monadic: theory HOL-Library.Adhoc_Overloading
02:24:36 Refine_Monadic: theory Refine_Monadic.Refine_Chapter
02:24:36 Refine_Monadic: theory Refine_Monadic.Example_Chapter
02:24:36 Refine_Monadic: theory HOL-Library.Phantom_Type
02:24:36 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
02:24:36 Refine_Monadic: theory HOL-Library.While_Combinator
02:24:37 Refine_Monadic: theory HOL-Library.Monad_Syntax
02:24:37 Refine_Monadic: theory Refine_Monadic.Refine_Misc
02:24:38 Refine_Monadic: theory HOL-Library.Cardinality
02:24:38 Refine_Monadic: theory Refine_Monadic.RefineG_Domain
02:24:38 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
02:24:38 Refine_Monadic: theory Refine_Monadic.RefineG_Assert
02:24:39 Refine_Monadic: theory HOL-Library.Numeral_Type
02:24:39 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
02:24:40 Refine_Monadic: theory Refine_Monadic.RefineG_While
02:24:40 Refine_Monadic: theory Refine_Monadic.Refine_Basic
02:24:40 Refine_Monadic: theory HOL-Library.Type_Length
02:24:41 Refine_Monadic: theory Refine_Monadic.Refine_Det
02:24:41 Refine_Monadic: theory HOL-Library.Word
02:24:44 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
02:24:44 Refine_Monadic: theory Refine_Monadic.Refine_Leof
02:24:45 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
02:24:45 Refine_Monadic: theory Refine_Monadic.Refine_Pfun
02:24:45 Refine_Monadic: theory Refine_Monadic.Refine_While
02:24:47 Refine_Monadic: theory Refine_Monadic.Refine_Transfer
02:24:48 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
02:24:48 Refine_Monadic: theory Refine_Monadic.Refine_Automation
02:24:48 Refine_Monadic: theory Refine_Monadic.Refine_Foreach
02:24:52 Refine_Monadic: theory Refine_Monadic.Refine_Monadic
02:24:52 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
02:24:53 Refine_Monadic: theory Refine_Monadic.WordRefine
02:24:53 Refine_Monadic: theory Refine_Monadic.Examples
02:25:28 Preparing Refine_Monadic/document ...
02:25:39 Finished Refine_Monadic/document (0:00:10 elapsed time)
02:25:39 Preparing Refine_Monadic/outline ...
02:25:46 Finished Refine_Monadic/outline (0:00:07 elapsed time)
02:25:46 Timing Refine_Monadic (8 threads, 39.771s elapsed time, 177.396s cpu time, 4.470s GC time, factor 4.46)
02:25:46 Finished Refine_Monadic (0:00:51 elapsed time, 0:03:20 cpu time, factor 3.88)
02:25:47 Building Collections (on hpcisabelle/1) ...
02:25:48 Collections: theory Collections.ICF_Tools
02:25:48 Collections: theory Collections.Partial_Equivalence_Relation
02:25:48 Collections: theory Finger-Trees.FingerTree
02:25:48 Collections: theory Binomial-Heaps.SkewBinomialHeap
02:25:48 Collections: theory Binomial-Heaps.BinomialHeap
02:25:48 Collections: theory HOL-Library.Code_Abstract_Nat
02:25:48 Collections: theory HOL-Library.Code_Target_Int
02:25:48 Collections: theory HOL-Library.AList
02:25:49 Collections: theory HOL-Library.Code_Target_Nat
02:25:49 Collections: theory HOL-Library.Confluence
02:25:49 Collections: theory Collections.Ord_Code_Preproc
02:25:49 Collections: theory Collections.Locale_Code
02:25:49 Collections: theory Collections.Record_Intf
02:25:49 Collections: theory HOL-Library.Confluent_Quotient
02:25:49 Collections: theory HOL-Library.Code_Target_Numeral
02:25:49 Collections: theory Collections.SetIterator
02:25:49 Collections: theory Collections.Sorted_List_Operations
02:25:49 Collections: theory HOL-Library.Dlist
02:25:49 Collections: theory Word_Lib.Bit_Comprehension
02:25:50 Collections: theory Word_Lib.More_Divides
02:25:50 Collections: theory HOL-Library.RBT_Impl
02:25:50 Collections: theory HOL-Library.Signed_Division
02:25:51 Collections: theory Collections.DatRef
02:25:51 Collections: theory Collections.Idx_Iterator
02:25:52 Collections: theory Collections.SetAbstractionIterator
02:25:52 Collections: theory Collections.SetIteratorOperations
02:25:52 Collections: theory Word_Lib.Signed_Division_Word
02:25:52 Collections: theory Native_Word.Code_Int_Integer_Conversion
02:25:52 Collections: theory Word_Lib.More_Arithmetic
02:25:52 Collections: theory Word_Lib.More_Bit_Ring
02:25:53 Collections: theory Word_Lib.More_Word
02:25:57 Collections: theory Collections.Assoc_List
02:25:57 Collections: theory Collections.Dlist_add
02:25:57 Collections: theory Collections.Proper_Iterator
02:25:57 Collections: theory Collections.SetIteratorGA
02:25:57 Collections: theory Native_Word.Code_Target_Word_Base
02:25:57 Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
02:25:57 Collections: theory Collections.Diff_Array
02:25:58 Collections: theory Collections.It_to_It
02:25:58 Collections: theory Collections.Gen_Iterator
02:25:58 Collections: theory Word_Lib.Least_significant_bit
02:25:59 Collections: theory Collections.Iterator
02:26:00 Collections: theory Word_Lib.Most_significant_bit
02:26:00 Collections: theory Collections.ICF_Spec_Base
02:26:00 Collections: theory Word_Lib.Generic_set_bit
02:26:00 Collections: theory Collections.MapSpec
02:26:01 Collections: theory Native_Word.Code_Target_Integer_Bit
02:26:01 Collections: theory Native_Word.Word_Type_Copies
02:26:04 Collections: theory Collections.Robdd
02:26:17 Collections: theory Native_Word.Code_Target_Int_Bit
02:26:17 Collections: theory Native_Word.Uint32
02:26:17 Collections: theory Collections.Code_Target_ICF
02:26:18 Collections: theory Collections.Locale_Code_Ex
02:26:19 Collections: theory Collections.HashCode
02:27:03 Collections: theory Collections.RBT_add
02:27:40 Collections: theory Collections.GenCF_Gen_Chapter
02:27:40 Collections: theory Collections.GenCF_Chapter
02:27:40 Collections: theory Collections.GenCF_Impl_Chapter
02:27:40 Collections: theory Collections.GenCF_Intf_Chapter
02:27:40 Collections: theory Collections.Intf_Comp
02:27:40 Collections: theory Collections.Impl_Array_Stack
02:27:40 Collections: theory HOL-Library.Product_Lexorder
02:27:40 Collections: theory Collections.Array_Iterator
02:27:40 Collections: theory Collections.Intf_Map
02:27:40 Collections: theory Collections.Intf_Set
02:27:40 Collections: theory Collections.Intf_Hash
02:27:41 Collections: theory Collections.Gen_Map
02:27:41 Collections: theory Collections.Gen_Set
02:27:41 Collections: theory Collections.Impl_Cfun_Set
02:27:41 Collections: theory Collections.Impl_List_Set
02:27:43 Collections: theory Collections.Gen_Comp
02:27:43 Collections: theory Collections.Impl_Array_Map
02:27:43 Collections: theory Collections.Impl_List_Map
02:27:43 Collections: theory Collections.Impl_RBT_Map
02:27:43 Collections: theory Collections.Gen_Map2Set
02:27:44 Collections: theory Collections.Impl_Array_Hash_Map
02:27:55 Collections: theory Native_Word.Uint
02:27:55 Collections: theory Collections.Impl_Bit_Set
02:27:55 Collections: theory Collections.Gen_Hash
02:27:57 Collections: theory Collections.Impl_Uv_Set
02:28:12 Collections: theory Collections.GenCF
02:28:16 Collections: theory Collections.ICF_Gen_Algo_Chapter
02:28:16 Collections: theory Collections.ICF_Impl_Chapter
02:28:16 Collections: theory Collections.ICF_Spec_Chapter
02:28:16 Collections: theory Collections.ICF_Chapter
02:28:16 Collections: theory Trie.Trie
02:28:16 Collections: theory HOL-Library.RBT
02:28:16 Collections: theory Collections.ListSpec
02:28:16 Collections: theory Collections.AnnotatedListSpec
02:28:16 Collections: theory Collections.PrioSpec
02:28:16 Collections: theory Collections.SetSpec
02:28:16 Collections: theory Collections.PrioUniqueSpec
02:28:17 Collections: theory Collections.BinoPrioImpl
02:28:17 Collections: theory Collections.SkewPrioImpl
02:28:18 Collections: theory Collections.ListGA
02:28:18 Collections: theory Collections.Trie_Impl
02:28:18 Collections: theory Collections.FTAnnotatedListImpl
02:28:18 Collections: theory Collections.PrioByAnnotatedList
02:28:19 Collections: theory Collections.Fifo
02:28:19 Collections: theory Collections.PrioUniqueByAnnotatedList
02:28:19 Collections: theory Collections.Trie2
02:28:20 Collections: theory Collections.Algos
02:28:20 Collections: theory Collections.SetIndex
02:28:21 Collections: theory Collections.SetIteratorCollectionsGA
02:28:22 Collections: theory Collections.MapGA
02:28:22 Collections: theory Collections.SetGA
02:28:23 Collections: theory Collections.FTPrioImpl
02:28:23 Collections: theory Collections.FTPrioUniqueImpl
02:28:24 Collections: theory Collections.ArrayMapImpl
02:28:24 Collections: theory Collections.ListMapImpl
02:28:25 Collections: theory Collections.ListMapImpl_Invar
02:28:25 Collections: theory Collections.TrieMapImpl
02:28:27 Collections: theory Collections.ListSetImpl
02:28:28 Collections: theory Collections.ListSetImpl_Invar
02:28:28 Collections: theory Collections.ListSetImpl_NotDist
02:28:28 Collections: theory Collections.ListSetImpl_Sorted
02:28:29 Collections: theory Collections.SetByMap
02:28:30 Collections: theory Collections.RBTMapImpl
02:28:31 Collections: theory Collections.ArrayHashMap_Impl
02:28:32 Collections: theory Collections.ArraySetImpl
02:28:32 Collections: theory Collections.TrieSetImpl
02:28:34 Collections: theory Collections.ArrayHashMap
02:28:37 Collections: theory Collections.RBTSetImpl
02:28:37 Collections: theory Collections.HashMap_Impl
02:28:39 Collections: theory Collections.HashMap
02:28:41 Collections: theory Collections.ArrayHashSet
02:28:45 Collections: theory Collections.MapStdImpl
02:28:45 Collections: theory Collections.HashSet
02:28:55 Collections: theory Collections.SetStdImpl
02:29:01 Collections: theory Collections.ICF_Impl
02:29:05 Collections: theory Collections.ICF_Refine_Monadic
02:29:05 Collections: theory Collections.ICF_Autoref
02:29:09 Collections: theory Collections.Userguides_Chapter
02:29:09 Collections: theory Collections.Collections_Entrypoints_Chapter
02:29:09 Collections: theory Collections.ICF_Entrypoints_Chapter
02:29:09 Collections: theory Collections.Collections
02:29:09 Collections: theory Collections.Refine_Dflt
02:29:10 Collections: theory Collections.CollectionsV1
02:29:10 Collections: theory Collections.ICF_Userguide
02:29:10 Collections: theory Collections.Refine_Dflt_ICF
02:29:10 Collections: theory Collections.Refine_Dflt_Only_ICF
02:29:10 Collections: theory Collections.Refine_Monadic_Userguide
02:30:39 Preparing Collections/document ...
02:30:59 Finished Collections/document (0:00:19 elapsed time)
02:30:59 Preparing Collections/outline ...
02:31:11 Finished Collections/outline (0:00:12 elapsed time)
02:31:11 Preparing Collections/userguide ...
02:31:14 Finished Collections/userguide (0:00:03 elapsed time)
02:31:15 Timing Collections (8 threads, 226.955s elapsed time, 1023.377s cpu time, 76.131s GC time, factor 4.51)
02:31:15 Finished Collections (0:04:48 elapsed time, 0:19:39 cpu time, factor 4.09)
02:31:15 Building Core_SC_DOM (on hpcisabelle/2) ...
02:31:30 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
02:31:30 Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
02:31:30 Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
02:31:31 Core_SC_DOM: theory Core_SC_DOM.Ref
02:31:31 Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
02:31:31 Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
02:31:31 Core_SC_DOM: theory Core_SC_DOM.BaseClass
02:31:32 Core_SC_DOM: theory Core_SC_DOM.NodePointer
02:31:32 Core_SC_DOM: theory Core_SC_DOM.ObjectClass
02:31:33 Core_SC_DOM: theory Core_SC_DOM.ElementPointer
02:31:34 Core_SC_DOM: theory Core_SC_DOM.NodeClass
02:31:34 Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
02:31:35 Core_SC_DOM: theory Core_SC_DOM.BaseMonad
02:31:35 Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
02:31:36 Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
02:31:37 Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
02:31:37 Core_SC_DOM: theory Core_SC_DOM.ElementClass
02:31:37 Core_SC_DOM: theory Core_SC_DOM.NodeMonad
02:31:39 Core_SC_DOM: theory Core_SC_DOM.ElementMonad
02:31:39 Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
02:31:40 Core_SC_DOM: theory Core_SC_DOM.DocumentClass
02:31:41 Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
02:31:42 Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
02:31:44 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
02:32:05 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
02:32:25 Core_SC_DOM: theory Core_SC_DOM.Core_DOM
02:32:25 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
02:32:33 Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
02:32:33 Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
02:32:33 Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
02:32:33 Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
02:32:35 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
02:34:55 Preparing Core_SC_DOM/document ...
02:35:11 Finished Core_SC_DOM/document (0:00:16 elapsed time)
02:35:11 Preparing Core_SC_DOM/outline ...
02:35:22 Finished Core_SC_DOM/outline (0:00:11 elapsed time)
02:35:23 Timing Core_SC_DOM (8 threads, 159.890s elapsed time, 866.949s cpu time, 54.814s GC time, factor 5.42)
02:35:23 Finished Core_SC_DOM (0:03:38 elapsed time, 0:16:53 cpu time, factor 4.63)
02:35:23 Building Jordan_Normal_Form (on hpcisabelle/3) ...
02:35:25 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
02:35:25 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
02:35:33 Jordan_Normal_Form: theory Containers.Equal
02:35:33 Jordan_Normal_Form: theory Containers.Extend_Partial_Order
02:35:33 Jordan_Normal_Form: theory Containers.List_Fusion
02:35:33 Jordan_Normal_Form: theory Deriving.Comparator
02:35:33 Jordan_Normal_Form: theory Deriving.Derive_Manager
02:35:33 Jordan_Normal_Form: theory Deriving.Generator_Aux
02:35:33 Jordan_Normal_Form: theory Containers.Containers_Auxiliary
02:35:33 Jordan_Normal_Form: theory Abstract-Rewriting.Seq
02:35:33 Jordan_Normal_Form: theory Containers.Closure_Set
02:35:33 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
02:35:33 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
02:35:33 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
02:35:33 Jordan_Normal_Form: theory Deriving.Equality_Generator
02:35:34 Jordan_Normal_Form: theory Containers.Containers_Generator
02:35:34 Jordan_Normal_Form: theory Regular-Sets.Regular_Set
02:35:34 Jordan_Normal_Form: theory Deriving.Equality_Instances
02:35:34 Jordan_Normal_Form: theory Show.Show
02:35:34 Jordan_Normal_Form: theory Containers.Collection_Enum
02:35:34 Jordan_Normal_Form: theory Deriving.Compare
02:35:35 Jordan_Normal_Form: theory Deriving.Comparator_Generator
02:35:35 Jordan_Normal_Form: theory Containers.Lexicographic_Order
02:35:35 Jordan_Normal_Form: theory Containers.Collection_Eq
02:35:36 Jordan_Normal_Form: theory Containers.RBT_ext
02:35:36 Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl
02:35:36 Jordan_Normal_Form: theory Containers.Set_Linorder
02:35:36 Jordan_Normal_Form: theory Deriving.Compare_Generator
02:35:36 Jordan_Normal_Form: theory Containers.DList_Set
02:35:36 Jordan_Normal_Form: theory Deriving.Compare_Instances
02:35:37 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
02:35:37 Jordan_Normal_Form: theory Show.Show_Instances
02:35:37 Jordan_Normal_Form: theory Regular-Sets.Regular_Exp
02:35:38 Jordan_Normal_Form: theory VectorSpace.FunctionLemmas
02:35:38 Jordan_Normal_Form: theory Show.Shows_Literal
02:35:38 Jordan_Normal_Form: theory VectorSpace.RingModuleFacts
02:35:39 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
02:35:39 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
02:35:39 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
02:35:39 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
02:35:39 Jordan_Normal_Form: theory VectorSpace.MonoidSums
02:35:40 Jordan_Normal_Form: theory VectorSpace.LinearCombinations
02:35:41 Jordan_Normal_Form: theory Regular-Sets.NDerivative
02:35:41 Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation
02:35:45 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
02:35:45 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
02:35:45 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
02:35:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
02:35:46 Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking
02:35:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Shows_Literal_Matrix
02:35:47 Jordan_Normal_Form: theory Regular-Sets.Regexp_Method
02:35:47 Jordan_Normal_Form: theory VectorSpace.SumSpaces
02:35:47 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
02:35:48 Jordan_Normal_Form: theory VectorSpace.VectorSpace
02:35:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
02:35:48 Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting
02:35:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
02:35:49 Jordan_Normal_Form: theory Containers.Collection_Order
02:35:51 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders
02:35:51 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
02:35:51 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
02:35:51 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
02:35:52 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
02:35:52 Jordan_Normal_Form: theory Containers.RBT_Mapping2
02:35:54 Jordan_Normal_Form: theory Containers.RBT_Set2
02:35:54 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier
02:35:54 Jordan_Normal_Form: theory Matrix.Ordered_Semiring
02:35:54 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
02:35:55 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
02:35:56 Jordan_Normal_Form: theory Containers.Set_Impl
02:35:58 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
02:35:59 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
02:35:59 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
02:36:03 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
02:36:11 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
02:36:11 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
02:36:13 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
02:36:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
02:36:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
02:36:19 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
02:36:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
02:36:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
02:36:24 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
02:39:54 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
02:39:54 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
02:39:57 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
02:39:58 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
02:40:05 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
02:40:50 Preparing Jordan_Normal_Form/document ...
02:41:17 Finished Jordan_Normal_Form/document (0:00:26 elapsed time)
02:41:17 Preparing Jordan_Normal_Form/outline ...
02:41:28 Finished Jordan_Normal_Form/outline (0:00:10 elapsed time)
02:41:28 Timing Jordan_Normal_Form (8 threads, 282.117s elapsed time, 1740.385s cpu time, 61.388s GC time, factor 6.17)
02:41:28 Finished Jordan_Normal_Form (0:05:23 elapsed time, 0:30:37 cpu time, factor 5.68)
02:41:28 Building HOL-Probability (on hpcisabelle/4) ...
02:41:31 HOL-Probability: theory HOL-Library.AList
02:41:31 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
02:41:31 HOL-Probability: theory HOL-Library.Adhoc_Overloading
02:41:31 HOL-Probability: theory HOL-Library.Conditional_Parametricity
02:41:31 HOL-Probability: theory HOL-Library.Rewrite
02:41:31 HOL-Probability: theory HOL-Library.Stream
02:41:31 HOL-Probability: theory HOL-Library.Sublist
02:41:31 HOL-Probability: theory HOL-Library.Tree
02:41:31 HOL-Probability: theory HOL-Library.Monad_Syntax
02:41:31 HOL-Probability: theory HOL-Library.FSet
02:41:32 HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
02:41:32 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
02:41:32 HOL-Probability: theory HOL-Probability.Discrete_Topology
02:41:33 HOL-Probability: theory HOL-Probability.Essential_Supremum
02:41:33 HOL-Probability: theory HOL-Probability.Probability_Measure
02:41:33 HOL-Probability: theory HOL-Probability.Stopping_Time
02:41:34 HOL-Probability: theory HOL-Library.Mapping
02:41:35 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
02:41:36 HOL-Probability: theory HOL-Probability.Tree_Space
02:41:37 HOL-Probability: theory HOL-Library.AList_Mapping
02:41:37 HOL-Probability: theory HOL-Probability.Conditional_Expectation
02:41:37 HOL-Probability: theory HOL-Probability.Distribution_Functions
02:41:37 HOL-Probability: theory HOL-Probability.Giry_Monad
02:41:37 HOL-Probability: theory HOL-Probability.Weak_Convergence
02:41:38 HOL-Probability: theory HOL-Probability.Helly_Selection
02:41:38 HOL-Probability: theory HOL-Library.Finite_Map
02:41:39 HOL-Probability: theory HOL-Probability.Projective_Family
02:41:39 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
02:41:40 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
02:41:41 HOL-Probability: theory HOL-Probability.Independent_Family
02:41:41 HOL-Probability: theory HOL-Probability.Stream_Space
02:41:42 HOL-Probability: theory HOL-Probability.PMF_Impl
02:41:42 HOL-Probability: theory HOL-Probability.Random_Permutations
02:41:42 HOL-Probability: theory HOL-Probability.SPMF
02:41:42 HOL-Probability: theory HOL-Probability.Convolution
02:41:42 HOL-Probability: theory HOL-Probability.Information
02:41:42 HOL-Probability: theory HOL-Probability.Product_PMF
02:41:43 HOL-Probability: theory HOL-Probability.Hoeffding
02:41:44 HOL-Probability: theory HOL-Probability.Distributions
02:41:46 HOL-Probability: theory HOL-Probability.Characteristic_Functions
02:41:46 HOL-Probability: theory HOL-Probability.Sinc_Integral
02:41:47 HOL-Probability: theory HOL-Probability.Levy
02:41:48 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
02:41:52 HOL-Probability: theory HOL-Probability.Fin_Map
02:41:54 HOL-Probability: theory HOL-Probability.Projective_Limit
02:41:57 HOL-Probability: theory HOL-Probability.Probability
02:43:09 Preparing HOL-Probability/document ...
02:43:31 Finished HOL-Probability/document (0:00:21 elapsed time)
02:43:31 Preparing HOL-Probability/outline ...
02:43:39 Finished HOL-Probability/outline (0:00:08 elapsed time)
02:43:39 Timing HOL-Probability (8 threads, 73.621s elapsed time, 498.317s cpu time, 13.357s GC time, factor 6.77)
02:43:39 Finished HOL-Probability (0:01:38 elapsed time, 0:09:10 cpu time, factor 5.59)
02:43:39 Building HOL-Number_Theory (on hpcisabelle/5) ...
02:43:42 HOL-Number_Theory: theory HOL-Number_Theory.Cong
02:43:42 HOL-Number_Theory: theory HOL-Algebra.Congruence
02:43:42 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
02:43:42 HOL-Number_Theory: theory HOL-Number_Theory.Fib
02:43:42 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
02:43:43 HOL-Number_Theory: theory HOL-Algebra.Order
02:43:44 HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
02:43:44 HOL-Number_Theory: theory HOL-Number_Theory.Totient
02:43:45 HOL-Number_Theory: theory HOL-Algebra.Lattice
02:43:46 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
02:43:47 HOL-Number_Theory: theory HOL-Algebra.Group
02:43:50 HOL-Number_Theory: theory HOL-Algebra.Coset
02:43:50 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
02:43:51 HOL-Number_Theory: theory HOL-Algebra.Ring
02:43:53 HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
02:43:54 HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
02:43:56 HOL-Number_Theory: theory HOL-Algebra.AbelCoset
02:43:56 HOL-Number_Theory: theory HOL-Algebra.Module
02:44:01 HOL-Number_Theory: theory HOL-Algebra.Ideal
02:44:04 HOL-Number_Theory: theory HOL-Algebra.RingHom
02:44:05 HOL-Number_Theory: theory HOL-Algebra.UnivPoly
02:44:19 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
02:44:23 HOL-Number_Theory: theory HOL-Number_Theory.Residues
02:44:27 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
02:44:27 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
02:44:27 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
02:44:27 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
02:44:27 HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
02:44:28 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
02:44:58 Preparing HOL-Number_Theory/document ...
02:45:04 Finished HOL-Number_Theory/document (0:00:05 elapsed time)
02:45:04 Preparing HOL-Number_Theory/outline ...
02:45:07 Finished HOL-Number_Theory/outline (0:00:02 elapsed time)
02:45:07 Timing HOL-Number_Theory (8 threads, 59.522s elapsed time, 336.341s cpu time, 10.318s GC time, factor 5.65)
02:45:07 Finished HOL-Number_Theory (0:01:17 elapsed time, 0:06:11 cpu time, factor 4.81)
02:45:07 Running Crypto_Standards (on hpcisabelle/6) ...
02:45:10 Crypto_Standards: theory Crypto_Standards.More_Bit_Operations_Nat
02:45:10 Crypto_Standards: theory HOL-Decision_Procs.Conversions
02:45:10 Crypto_Standards: theory HOL-Decision_Procs.Algebra_Aux
02:45:10 Crypto_Standards: theory Crypto_Standards.Words
02:45:11 Crypto_Standards: theory Crypto_Standards.More_Residues
02:45:11 Crypto_Standards: theory HOL-Decision_Procs.Commutative_Ring
02:45:13 Crypto_Standards: theory Crypto_Standards.FIPS180_4
02:45:13 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2
02:45:20 Crypto_Standards: theory Crypto_Standards.FIPS180_4_Test_Vectors
02:45:23 Crypto_Standards: theory HOL-Decision_Procs.Reflective_Field
02:45:23 Crypto_Standards: theory Crypto_Standards.Efficient_Mod_Exp
02:45:23 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Interpretations
02:45:26 Crypto_Standards: theory Crypto_Standards.FIPS198_1
02:45:27 Crypto_Standards: theory Crypto_Standards.FIPS198_1_Test_Vectors
02:45:29 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Test_Vectors
02:45:35 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Locale
02:45:40 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Test
02:45:46 Crypto_Standards: theory Crypto_Standards.EC_Common
02:45:56 Crypto_Standards: theory Crypto_Standards.SEC1v2_0
02:46:13 Crypto_Standards: theory Crypto_Standards.Crypto_Standards
02:46:13 Crypto_Standards: theory Crypto_Standards.Efficient_SEC1
02:46:21 Crypto_Standards: theory Crypto_Standards.FIPS186_4_Curves
02:46:54 Crypto_Standards: theory Crypto_Standards.SEC1v2_0_Test_Vectors
02:52:23 Crypto_Standards: theory Crypto_Standards.Test_Vectors
02:59:27 Preparing Crypto_Standards/document ...
02:59:32 Finished Crypto_Standards/document (0:00:04 elapsed time)
02:59:32 Preparing Crypto_Standards/outline ...
02:59:34 Finished Crypto_Standards/outline (0:00:01 elapsed time)
02:59:34 Timing Crypto_Standards (8 threads, 853.542s elapsed time, 6393.554s cpu time, 541.529s GC time, factor 7.49)
02:59:34 Finished Crypto_Standards (0:14:17 elapsed time, 1:46:43 cpu time, factor 7.47)
02:59:34 Building Bounded_Deducibility_Security (on hpcisabelle/7) ...
02:59:35 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Abstract_BD_Security
02:59:35 Bounded_Deducibility_Security: theory HOL-Library.Sublist
02:59:38 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Trivia
02:59:39 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Filtermap
02:59:39 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Transition_System
02:59:40 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_TS
02:59:40 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.IO_Automaton
02:59:41 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Triggers
02:59:42 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_IO
02:59:42 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Unwinding
02:59:43 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Compositional_Reasoning
02:59:44 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Bounded_Deducibility_Security
02:59:53 Preparing Bounded_Deducibility_Security/document ...
02:59:57 Finished Bounded_Deducibility_Security/document (0:00:03 elapsed time)
02:59:57 Preparing Bounded_Deducibility_Security/outline ...
03:00:00 Finished Bounded_Deducibility_Security/outline (0:00:03 elapsed time)
03:00:00 Timing Bounded_Deducibility_Security (8 threads, 9.763s elapsed time, 44.615s cpu time, 1.178s GC time, factor 4.57)
03:00:00 Finished Bounded_Deducibility_Security (0:00:18 elapsed time, 0:01:00 cpu time, factor 3.25)
03:00:00 Building BD_Security_Compositional (on hpcisabelle/0) ...
03:00:01 BD_Security_Compositional: theory BD_Security_Compositional.Trivial_Security
03:00:01 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security
03:00:01 BD_Security_Compositional: theory BD_Security_Compositional.Transporting_Security
03:00:01 BD_Security_Compositional: theory BD_Security_Compositional.Independent_Secrets
03:00:11 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security_Network
03:01:11 Preparing BD_Security_Compositional/document ...
03:01:17 Finished BD_Security_Compositional/document (0:00:05 elapsed time)
03:01:17 Preparing BD_Security_Compositional/outline ...
03:01:20 Finished BD_Security_Compositional/outline (0:00:03 elapsed time)
03:01:20 Timing BD_Security_Compositional (8 threads, 56.383s elapsed time, 200.749s cpu time, 5.817s GC time, factor 3.56)
03:01:20 Finished BD_Security_Compositional (0:01:10 elapsed time, 0:03:51 cpu time, factor 3.27)
03:01:20 Building Expander_Graphs (on hpcisabelle/1) ...
03:01:26 Expander_Graphs: theory HOL-Eisbach.Eisbach
03:01:26 Expander_Graphs: theory Digit_Expansions.Bits_Digits
03:01:26 Expander_Graphs: theory Graph_Theory.Rtrancl_On
03:01:26 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
03:01:26 Expander_Graphs: theory HOL-Decision_Procs.Dense_Linear_Order
03:01:26 Expander_Graphs: theory HOL-Library.Code_Abstract_Nat
03:01:26 Expander_Graphs: theory HOL-Library.Code_Target_Int
03:01:26 Expander_Graphs: theory HOL-Algebra.Congruence
03:01:26 Expander_Graphs: theory HOL-Library.Code_Target_Nat
03:01:26 Expander_Graphs: theory Finite_Fields.Finite_Fields_More_Bijections
03:01:26 Expander_Graphs: theory HOL-Combinatorics.List_Permutation
03:01:26 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
03:01:26 Expander_Graphs: theory HOL-Library.Code_Target_Numeral
03:01:27 Expander_Graphs: theory HOL-Library.Function_Algebras
03:01:27 Expander_Graphs: theory Abstract-Rewriting.Seq
03:01:27 Expander_Graphs: theory HOL-Library.More_List
03:01:27 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
03:01:27 Expander_Graphs: theory HOL-Library.While_Combinator
03:01:27 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
03:01:28 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
03:01:28 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
03:01:28 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
03:01:28 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
03:01:28 Expander_Graphs: theory HOL-Algebra.Order
03:01:29 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
03:01:29 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
03:01:29 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
03:01:29 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
03:01:29 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
03:01:30 Expander_Graphs: theory HOL-Library.Lattice_Algebras
03:01:30 Expander_Graphs: theory HOL-Library.Log_Nat
03:01:30 Expander_Graphs: theory HOL-Algebra.Lattice
03:01:30 Expander_Graphs: theory Graph_Theory.Stuff
03:01:30 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families
03:01:30 Expander_Graphs: theory Graph_Theory.Digraph
03:01:30 Expander_Graphs: theory Ergodic_Theory.SG_Library_Complement
03:01:30 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
03:01:31 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
03:01:31 Expander_Graphs: theory HOL-Algebra.Complete_Lattice
03:01:31 Expander_Graphs: theory Matrix.Utility
03:01:32 Expander_Graphs: theory Lp.Functional_Spaces
03:01:32 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
03:01:32 Expander_Graphs: theory Graph_Theory.Arc_Walk
03:01:32 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
03:01:32 Expander_Graphs: theory HOL-Algebra.Group
03:01:33 Expander_Graphs: theory Regular-Sets.Regular_Set
03:01:35 Expander_Graphs: theory Graph_Theory.Pair_Digraph
03:01:35 Expander_Graphs: theory VectorSpace.FunctionLemmas
03:01:36 Expander_Graphs: theory HOL-Algebra.Coset
03:01:36 Expander_Graphs: theory HOL-Algebra.FiniteProduct
03:01:36 Expander_Graphs: theory Lp.Lp
03:01:36 Expander_Graphs: theory HOL-Algebra.Ring
03:01:37 Expander_Graphs: theory Regular-Sets.Regular_Exp
03:01:37 Expander_Graphs: theory HOL-Library.Interval
03:01:37 Expander_Graphs: theory HOL-Library.Float
03:01:38 Expander_Graphs: theory HOL-Algebra.Generated_Groups
03:01:38 Expander_Graphs: theory HOL-Algebra.Divisibility
03:01:39 Expander_Graphs: theory HOL-Algebra.Elementary_Groups
03:01:41 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
03:01:41 Expander_Graphs: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
03:01:41 Expander_Graphs: theory HOL-Library.Interval_Float
03:01:41 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
03:01:43 Expander_Graphs: theory Regular-Sets.NDerivative
03:01:43 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
03:01:43 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
03:01:43 Expander_Graphs: theory HOL-Algebra.AbelCoset
03:01:44 Expander_Graphs: theory HOL-Algebra.Module
03:01:44 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
03:01:44 Expander_Graphs: theory Graph_Theory.Digraph_Component
03:01:44 Expander_Graphs: theory Universal_Hash_Families.Pseudorandom_Objects
03:01:44 Expander_Graphs: theory HOL-Decision_Procs.Approximation_Bounds
03:01:45 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
03:01:46 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
03:01:46 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
03:01:46 Expander_Graphs: theory VectorSpace.RingModuleFacts
03:01:47 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
03:01:47 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
03:01:47 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
03:01:47 Expander_Graphs: theory VectorSpace.MonoidSums
03:01:48 Expander_Graphs: theory VectorSpace.LinearCombinations
03:01:48 Expander_Graphs: theory HOL-Algebra.Ideal
03:01:51 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
03:01:51 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
03:01:52 Expander_Graphs: theory Regular-Sets.Regexp_Method
03:01:52 Expander_Graphs: theory Jordan_Normal_Form.Matrix
03:01:53 Expander_Graphs: theory HOL-Decision_Procs.Approximation
03:01:53 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
03:01:54 Expander_Graphs: theory HOL-Algebra.RingHom
03:01:55 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
03:01:56 Expander_Graphs: theory HOL-Algebra.QuotRing
03:01:56 Expander_Graphs: theory HOL-Algebra.UnivPoly
03:01:57 Expander_Graphs: theory VectorSpace.SumSpaces
03:01:58 Expander_Graphs: theory VectorSpace.VectorSpace
03:01:59 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
03:01:59 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
03:01:59 Expander_Graphs: theory Matrix.Ordered_Semiring
03:02:01 Expander_Graphs: theory Matrix.Matrix_Legacy
03:02:01 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
03:02:01 Expander_Graphs: theory Jordan_Normal_Form.Determinant
03:02:03 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
03:02:05 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
03:02:05 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
03:02:05 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
03:02:06 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
03:02:06 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
03:02:06 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
03:02:09 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
03:02:09 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
03:02:10 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
03:02:11 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
03:02:13 Expander_Graphs: theory HOL-Algebra.Multiplicative_Group
03:02:18 Expander_Graphs: theory HOL-Algebra.Ring_Divisibility
03:02:18 Expander_Graphs: theory HOL-Algebra.Subrings
03:02:21 Expander_Graphs: theory HOL-Algebra.Embedded_Algebras
03:02:24 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
03:02:26 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
03:02:28 Expander_Graphs: theory HOL-Algebra.Polynomials
03:02:30 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
03:02:36 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
03:02:36 Expander_Graphs: theory QHLProver.Complex_Matrix
03:02:36 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
03:02:41 Expander_Graphs: theory QHLProver.Gates
03:02:42 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
03:02:47 Expander_Graphs: theory HOL-Algebra.Polynomial_Divisibility
03:02:49 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
03:02:51 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
03:02:53 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
03:03:19 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
03:03:19 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
03:03:23 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
03:03:27 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
03:03:30 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
03:03:30 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
03:03:32 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
03:03:35 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
03:03:42 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
03:03:42 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
03:03:45 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
03:03:49 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
03:03:56 Expander_Graphs: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
03:11:57 Preparing Expander_Graphs/document ...
03:12:09 Finished Expander_Graphs/document (0:00:12 elapsed time)
03:12:09 Preparing Expander_Graphs/outline ...
03:12:14 Finished Expander_Graphs/outline (0:00:04 elapsed time)
03:12:15 Timing Expander_Graphs (8 threads, 566.482s elapsed time, 2629.760s cpu time, 142.209s GC time, factor 4.64)
03:12:15 Finished Expander_Graphs (0:10:27 elapsed time, 0:46:19 cpu time, factor 4.43)
03:12:15 Running Cook_Levin (on hpcisabelle/2) ...
03:12:18 Cook_Levin: theory HOL-Eisbach.Eisbach
03:12:18 Cook_Levin: theory Cook_Levin.Basics
03:12:21 Cook_Levin: theory Cook_Levin.Combinations
03:12:22 Cook_Levin: theory Cook_Levin.Elementary
03:12:24 Cook_Levin: theory Cook_Levin.Composing
03:12:24 Cook_Levin: theory Cook_Levin.Memorizing
03:12:25 Cook_Levin: theory Cook_Levin.Arithmetic
03:12:25 Cook_Levin: theory Cook_Levin.Oblivious
03:12:26 Cook_Levin: theory Cook_Levin.Oblivious_Polynomial
03:12:29 Cook_Levin: theory Cook_Levin.Lists_Lists
03:12:32 Cook_Levin: theory Cook_Levin.Two_Four_Symbols
03:12:33 Cook_Levin: theory Cook_Levin.Symbol_Ops
03:12:34 Cook_Levin: theory Cook_Levin.Wellformed
03:12:34 Cook_Levin: theory Cook_Levin.NP
03:12:35 Cook_Levin: theory Cook_Levin.Oblivious_2_Tape
03:12:36 Cook_Levin: theory Cook_Levin.Satisfiability
03:12:40 Cook_Levin: theory Cook_Levin.Reducing
03:12:42 Cook_Levin: theory Cook_Levin.Aux_TM_Reducing
03:12:47 Cook_Levin: theory Cook_Levin.Sat_TM_CNF
03:12:52 Cook_Levin: theory Cook_Levin.Reduction_TM
03:25:01 Preparing Cook_Levin/document ...
03:26:23 Finished Cook_Levin/document (0:01:21 elapsed time)
03:26:23 Preparing Cook_Levin/outline ...
03:26:57 Finished Cook_Levin/outline (0:00:34 elapsed time)
03:26:58 Timing Cook_Levin (8 threads, 758.793s elapsed time, 3895.309s cpu time, 31.028s GC time, factor 5.13)
03:26:58 Finished Cook_Levin (0:12:42 elapsed time, 1:05:03 cpu time, factor 5.12)
03:26:58 Building Abstract-Rewriting (on hpcisabelle/3) ...
03:27:02 Abstract-Rewriting: theory Abstract-Rewriting.Seq
03:27:02 Abstract-Rewriting: theory Regular-Sets.Regular_Set
03:27:06 Abstract-Rewriting: theory Regular-Sets.Regular_Exp
03:27:09 Abstract-Rewriting: theory Regular-Sets.NDerivative
03:27:09 Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
03:27:13 Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
03:27:13 Abstract-Rewriting: theory Regular-Sets.Regexp_Method
03:27:14 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
03:27:16 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
03:27:16 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
03:27:20 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
03:27:38 Preparing Abstract-Rewriting/document ...
03:27:46 Finished Abstract-Rewriting/document (0:00:08 elapsed time)
03:27:46 Preparing Abstract-Rewriting/outline ...
03:27:51 Finished Abstract-Rewriting/outline (0:00:04 elapsed time)
03:27:51 Timing Abstract-Rewriting (8 threads, 25.119s elapsed time, 88.305s cpu time, 2.634s GC time, factor 3.52)
03:27:51 Finished Abstract-Rewriting (0:00:39 elapsed time, 0:01:54 cpu time, factor 2.93)
03:27:51 Running X86_Semantics (on hpcisabelle/4) ...
03:27:52 X86_Semantics: theory HOL-Eisbach.Eisbach
03:27:52 X86_Semantics: theory Word_Lib.Even_More_List
03:27:52 X86_Semantics: theory Word_Lib.More_Bit_Ring
03:27:52 X86_Semantics: theory HOL-Library.Phantom_Type
03:27:52 X86_Semantics: theory HOL-Library.Sublist
03:27:54 X86_Semantics: theory HOL-Library.Cardinality
03:27:54 X86_Semantics: theory HOL-Library.Numeral_Type
03:27:56 X86_Semantics: theory HOL-Library.Type_Length
03:27:56 X86_Semantics: theory Word_Lib.More_Arithmetic
03:27:56 X86_Semantics: theory HOL-Library.Word
03:28:06 X86_Semantics: theory Word_Lib.Bit_Comprehension
03:28:06 X86_Semantics: theory Word_Lib.Legacy_Aliases
03:28:06 X86_Semantics: theory Word_Lib.More_Divides
03:28:06 X86_Semantics: theory Word_Lib.Syntax_Bundles
03:28:07 X86_Semantics: theory Word_Lib.More_Word
03:28:09 X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
03:28:09 X86_Semantics: theory Word_Lib.Least_significant_bit
03:28:11 X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
03:28:11 X86_Semantics: theory Word_Lib.Aligned
03:28:11 X86_Semantics: theory Word_Lib.Most_significant_bit
03:28:11 X86_Semantics: theory Word_Lib.Generic_set_bit
03:28:12 X86_Semantics: theory Word_Lib.Bits_Int
03:28:17 X86_Semantics: theory Word_Lib.Typedef_Morphisms
03:28:17 X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
03:28:20 X86_Semantics: theory Word_Lib.Bitwise
03:28:21 X86_Semantics: theory X86_Semantics.BitByte
03:28:21 X86_Semantics: theory X86_Semantics.Memory
03:28:22 X86_Semantics: theory X86_Semantics.State
03:28:30 X86_Semantics: theory X86_Semantics.StateCleanUp
03:28:30 X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
03:28:42 X86_Semantics: theory X86_Semantics.SymbolicExecution
03:28:42 X86_Semantics: theory X86_Semantics.X86_Parse
03:28:44 X86_Semantics: theory X86_Semantics.Examples
03:28:44 X86_Semantics: theory X86_Semantics.Example_WC
03:41:33 Preparing X86_Semantics/document ...
03:41:41 Finished X86_Semantics/document (0:00:07 elapsed time)
03:41:41 Preparing X86_Semantics/outline ...
03:41:48 Finished X86_Semantics/outline (0:00:06 elapsed time)
03:41:48 Timing X86_Semantics (8 threads, 819.034s elapsed time, 1029.266s cpu time, 12.700s GC time, factor 1.26)
03:41:48 Finished X86_Semantics (0:13:41 elapsed time, 0:17:13 cpu time, factor 1.26)
03:41:48 Building First_Order_Terms (on hpcisabelle/5) ...
03:41:50 First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
03:41:50 First_Order_Terms: theory Fresh_Identifiers.Fresh
03:41:50 First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
03:41:50 First_Order_Terms: theory First_Order_Terms.Renaming2
03:41:51 First_Order_Terms: theory First_Order_Terms.Renaming2_String
03:41:51 First_Order_Terms: theory First_Order_Terms.Fun_More
03:41:51 First_Order_Terms: theory First_Order_Terms.Seq_More
03:41:51 First_Order_Terms: theory First_Order_Terms.Option_Monad
03:41:52 First_Order_Terms: theory First_Order_Terms.Term
03:41:54 First_Order_Terms: theory First_Order_Terms.Unifiers
03:41:54 First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
03:41:54 First_Order_Terms: theory First_Order_Terms.Subsumption
03:41:54 First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
03:41:55 First_Order_Terms: theory First_Order_Terms.Abstract_Matching
03:41:55 First_Order_Terms: theory First_Order_Terms.Abstract_Unification
03:41:56 First_Order_Terms: theory First_Order_Terms.Unification
03:41:58 First_Order_Terms: theory First_Order_Terms.Matching
03:41:58 First_Order_Terms: theory First_Order_Terms.Unification_String
03:42:00 First_Order_Terms: theory Deriving.Generator_Aux
03:42:00 First_Order_Terms: theory Deriving.Derive_Manager
03:42:00 First_Order_Terms: theory Matrix.Utility
03:42:00 First_Order_Terms: theory Show.Show
03:42:01 First_Order_Terms: theory Polynomial_Factorization.Missing_List
03:42:02 First_Order_Terms: theory Show.Show_Instances
03:42:03 First_Order_Terms: theory Show.Shows_Literal
03:42:04 First_Order_Terms: theory First_Order_Terms.Position
03:42:06 First_Order_Terms: theory First_Order_Terms.Term_More
03:42:33 Preparing First_Order_Terms/document ...
03:42:43 Finished First_Order_Terms/document (0:00:10 elapsed time)
03:42:43 Preparing First_Order_Terms/outline ...
03:42:49 Finished First_Order_Terms/outline (0:00:05 elapsed time)
03:42:49 Timing First_Order_Terms (8 threads, 26.541s elapsed time, 116.105s cpu time, 3.798s GC time, factor 4.37)
03:42:49 Finished First_Order_Terms (0:00:43 elapsed time, 0:02:30 cpu time, factor 3.44)
03:42:49 Running CoSMeDis (on hpcisabelle/6) ...
03:42:50 CoSMeDis: theory Fresh_Identifiers.Fresh
03:42:51 CoSMeDis: theory Fresh_Identifiers.Fresh_String
03:42:51 CoSMeDis: theory CoSMeDis.Prelim
03:42:58 CoSMeDis: theory CoSMeDis.System_Specification
03:43:19 CoSMeDis: theory CoSMeDis.API_Network
03:43:19 CoSMeDis: theory CoSMeDis.Automation_Setup
03:43:19 CoSMeDis: theory CoSMeDis.Safety_Properties
03:43:19 CoSMeDis: theory CoSMeDis.Friend_Intro
03:43:19 CoSMeDis: theory CoSMeDis.Friend_Observation_Setup
03:43:19 CoSMeDis: theory CoSMeDis.Friend_State_Indistinguishability
03:43:20 CoSMeDis: theory CoSMeDis.Friend_Openness
03:43:20 CoSMeDis: theory CoSMeDis.Outer_Friend_Intro
03:43:20 CoSMeDis: theory CoSMeDis.Outer_Friend
03:43:20 CoSMeDis: theory CoSMeDis.Friend_Value_Setup
03:43:20 CoSMeDis: theory CoSMeDis.Friend_Request_Intro
03:43:21 CoSMeDis: theory CoSMeDis.Friend_Request_Value_Setup
03:43:21 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Observation_Setup
03:43:22 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Observation_Setup
03:43:22 CoSMeDis: theory CoSMeDis.Post_Intro
03:43:22 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_State_Indistinguishability
03:43:22 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_ISSUER
03:43:22 CoSMeDis: theory CoSMeDis.Friend
03:43:23 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_State_Indistinguishability
03:43:23 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_RECEIVER
03:43:23 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Value_Setup
03:43:23 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Openness
03:43:23 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Value_Setup
03:43:24 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_RECEIVER
03:43:24 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_RECEIVER
03:43:24 CoSMeDis: theory CoSMeDis.Friend_Request
03:43:24 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_ISSUER
03:43:25 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_ISSUER
03:43:25 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER
03:43:25 CoSMeDis: theory CoSMeDis.Independent_Post_Value_Setup_RECEIVER
03:43:26 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver
03:43:26 CoSMeDis: theory CoSMeDis.Post_Value_Setup_ISSUER
03:43:27 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer
03:43:27 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER
03:43:27 CoSMeDis: theory CoSMeDis.Friend_Network
03:43:27 CoSMeDis: theory CoSMeDis.Friend_Request_Network
03:43:27 CoSMeDis: theory CoSMeDis.Post_Value_Setup_RECEIVER
03:43:28 CoSMeDis: theory CoSMeDis.Outer_Friend_Network
03:43:29 CoSMeDis: theory CoSMeDis.Independent_Post_RECEIVER
03:43:31 CoSMeDis: theory CoSMeDis.Post_RECEIVER
03:43:31 CoSMeDis: theory CoSMeDis.Friend_All
03:43:32 CoSMeDis: theory CoSMeDis.Friend_Request_All
03:43:32 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_ISSUER
03:43:33 CoSMeDis: theory CoSMeDis.Post_ISSUER
03:43:33 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_ISSUER
03:43:34 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_COMPOSE2
03:43:34 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Network
03:43:34 CoSMeDis: theory CoSMeDis.Outer_Friend_All
03:43:35 CoSMeDis: theory CoSMeDis.Post_COMPOSE2
03:43:35 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Network
03:43:37 CoSMeDis: theory CoSMeDis.Post_Network
03:43:42 CoSMeDis: theory CoSMeDis.Independent_Posts_Network
03:45:54 CoSMeDis: theory CoSMeDis.Post_All
03:56:01 Preparing CoSMeDis/document ...
03:56:18 Finished CoSMeDis/document (0:00:17 elapsed time)
03:56:18 Preparing CoSMeDis/outline ...
03:56:27 Finished CoSMeDis/outline (0:00:08 elapsed time)
03:56:27 Timing CoSMeDis (8 threads, 787.466s elapsed time, 4464.014s cpu time, 98.714s GC time, factor 5.67)
03:56:27 Finished CoSMeDis (0:13:10 elapsed time, 1:14:32 cpu time, factor 5.66)
03:56:27 Building Shadow_SC_DOM (on hpcisabelle/7) ...
03:57:07 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
03:57:09 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
03:57:12 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
03:58:33 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
03:58:45 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
03:58:45 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
03:58:48 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
03:58:48 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
03:58:48 Shadow_SC_DOM: theory Shadow_SC_DOM.slots
03:58:48 Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
03:58:58 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
04:05:18 Preparing Shadow_SC_DOM/document ...
04:05:34 Finished Shadow_SC_DOM/document (0:00:16 elapsed time)
04:05:34 Preparing Shadow_SC_DOM/outline ...
04:05:45 Finished Shadow_SC_DOM/outline (0:00:10 elapsed time)
04:05:45 Timing Shadow_SC_DOM (8 threads, 437.452s elapsed time, 2657.880s cpu time, 162.213s GC time, factor 6.08)
04:05:45 Finished Shadow_SC_DOM (0:08:49 elapsed time, 0:48:16 cpu time, factor 5.47)
04:05:45 Building Stateful_Protocol_Composition_and_Typing (on hpcisabelle/0) ...
04:05:50 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
04:05:51 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
04:05:53 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
04:05:57 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
04:05:58 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
04:06:08 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
04:06:09 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
04:06:09 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
04:06:10 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
04:06:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
04:06:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
04:06:24 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
04:06:29 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
04:06:30 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
04:06:49 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
04:07:17 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
04:07:33 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
04:10:40 Preparing Stateful_Protocol_Composition_and_Typing/document ...
04:11:17 Finished Stateful_Protocol_Composition_and_Typing/document (0:00:37 elapsed time)
04:11:17 Preparing Stateful_Protocol_Composition_and_Typing/outline ...
04:11:34 Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:16 elapsed time)
04:11:34 Timing Stateful_Protocol_Composition_and_Typing (8 threads, 248.003s elapsed time, 1454.246s cpu time, 84.267s GC time, factor 5.86)
04:11:34 Finished Stateful_Protocol_Composition_and_Typing (0:04:51 elapsed time, 0:25:57 cpu time, factor 5.34)
04:11:34 Building Padic_Ints (on hpcisabelle/1) ...
04:11:36 Padic_Ints: theory Padic_Ints.Function_Ring
04:11:36 Padic_Ints: theory HOL-Number_Theory.Cong
04:11:36 Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
04:11:36 Padic_Ints: theory Padic_Ints.Extended_Int
04:11:39 Padic_Ints: theory HOL-Number_Theory.Totient
04:11:40 Padic_Ints: theory HOL-Number_Theory.Residues
04:11:43 Padic_Ints: theory Padic_Ints.Padic_Construction
04:11:44 Padic_Ints: theory Padic_Ints.Padic_Integers
04:11:47 Padic_Ints: theory Padic_Ints.Cring_Poly
04:12:47 Padic_Ints: theory Padic_Ints.Padic_Int_Topology
04:12:51 Padic_Ints: theory Padic_Ints.Zp_Compact
04:13:29 Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
04:13:33 Padic_Ints: theory Padic_Ints.Hensels_Lemma
04:14:11 Preparing Padic_Ints/document ...
04:14:41 Finished Padic_Ints/document (0:00:29 elapsed time)
04:14:41 Preparing Padic_Ints/outline ...
04:14:53 Finished Padic_Ints/outline (0:00:11 elapsed time)
04:14:53 Timing Padic_Ints (8 threads, 132.649s elapsed time, 551.213s cpu time, 64.000s GC time, factor 4.16)
04:14:53 Finished Padic_Ints (0:02:36 elapsed time, 0:10:01 cpu time, factor 3.86)
04:14:53 Building Frequency_Moments (on hpcisabelle/2) ...
04:14:58 Frequency_Moments: theory HOL-Eisbach.Eisbach
04:14:58 Frequency_Moments: theory Digit_Expansions.Bits_Digits
04:14:58 Frequency_Moments: theory Flow_Networks.Graph
04:14:58 Frequency_Moments: theory Graph_Theory.Rtrancl_On
04:14:58 Frequency_Moments: theory HOL-Combinatorics.Stirling
04:14:58 Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order
04:14:58 Frequency_Moments: theory HOL-Computational_Algebra.Group_Closure
04:14:58 Frequency_Moments: theory HOL-Computational_Algebra.Fraction_Field
04:14:59 Frequency_Moments: theory HOL-Computational_Algebra.Nth_Powers
04:14:59 Frequency_Moments: theory HOL-Computational_Algebra.Squarefree
04:14:59 Frequency_Moments: theory HOL-Number_Theory.Cong
04:15:00 Frequency_Moments: theory HOL-Library.Case_Converter
04:15:00 Frequency_Moments: theory HOL-Library.Code_Abstract_Nat
04:15:00 Frequency_Moments: theory HOL-Library.Code_Target_Nat
04:15:01 Frequency_Moments: theory HOL-Library.Code_Lazy
04:15:01 Frequency_Moments: theory HOL-Library.Code_Target_Int
04:15:01 Frequency_Moments: theory Expander_Graphs.Extra_Congruence_Method
04:15:01 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_Bijections
04:15:01 Frequency_Moments: theory HOL-Library.Code_Target_Numeral
04:15:01 Frequency_Moments: theory HOL-Algebra.Congruence
04:15:01 Frequency_Moments: theory Card_Partitions.Injectivity_Solver
04:15:01 Frequency_Moments: theory HOL-Computational_Algebra.Normalized_Fraction
04:15:01 Frequency_Moments: theory Card_Partitions.Set_Partition
04:15:02 Frequency_Moments: theory HOL-Combinatorics.List_Permutation
04:15:02 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
04:15:02 Frequency_Moments: theory Flow_Networks.Network
04:15:02 Frequency_Moments: theory Jordan_Normal_Form.Missing_Misc
04:15:02 Frequency_Moments: theory Card_Partitions.Card_Partitions
04:15:02 Frequency_Moments: theory HOL-Library.Function_Algebras
04:15:02 Frequency_Moments: theory Abstract-Rewriting.Seq
04:15:02 Frequency_Moments: theory HOL-Library.List_Lexorder
04:15:03 Frequency_Moments: theory HOL-Library.More_List
04:15:03 Frequency_Moments: theory Perron_Frobenius.Bij_Nat
04:15:03 Frequency_Moments: theory HOL-Library.Power_By_Squaring
04:15:03 Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers
04:15:03 Frequency_Moments: theory HOL-Library.Transitive_Closure_Table
04:15:03 Frequency_Moments: theory HOL-Algebra.Order
04:15:03 Frequency_Moments: theory HOL-Library.While_Combinator
04:15:03 Frequency_Moments: theory HOL-Number_Theory.Mod_Exp
04:15:03 Frequency_Moments: theory HOL-Number_Theory.Eratosthenes
04:15:04 Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations
04:15:04 Frequency_Moments: theory HOL-Types_To_Sets.Prerequisites
04:15:04 Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
04:15:04 Frequency_Moments: theory HOL-Types_To_Sets.Types_To_Sets
04:15:04 Frequency_Moments: theory Polynomial_Interpolation.Missing_Unsorted
04:15:04 Frequency_Moments: theory HOL-Library.Bourbaki_Witt_Fixpoint
04:15:04 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial
04:15:04 Frequency_Moments: theory HOL-Types_To_Sets.Group_On_With
04:15:05 Frequency_Moments: theory Perron_Frobenius.Cancel_Card_Constraint
04:15:05 Frequency_Moments: theory Jordan_Normal_Form.Conjugate
04:15:05 Frequency_Moments: theory Flow_Networks.Residual_Graph
04:15:05 Frequency_Moments: theory HOL-Algebra.Lattice
04:15:05 Frequency_Moments: theory HOL-Library.Going_To_Filter
04:15:05 Frequency_Moments: theory Frequency_Moments.Landau_Ext
04:15:05 Frequency_Moments: theory HOL-Library.Lattice_Algebras
04:15:06 Frequency_Moments: theory HOL-Library.Log_Nat
04:15:06 Frequency_Moments: theory Graph_Theory.Stuff
04:15:06 Frequency_Moments: theory Executable_Randomized_Algorithms.Tau_Additivity
04:15:06 Frequency_Moments: theory Graph_Theory.Digraph
04:15:06 Frequency_Moments: theory HOL-Algebra.Complete_Lattice
04:15:06 Frequency_Moments: theory HOL-Number_Theory.Fib
04:15:06 Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
04:15:06 Frequency_Moments: theory HOL-Number_Theory.Totient
04:15:07 Frequency_Moments: theory HOL-Algebra.Group
04:15:07 Frequency_Moments: theory Flow_Networks.Augmenting_Flow
04:15:07 Frequency_Moments: theory Flow_Networks.Augmenting_Path
04:15:07 Frequency_Moments: theory HOL-Complex_Analysis.Contour_Integration
04:15:07 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_PMF
04:15:07 Frequency_Moments: theory Flow_Networks.Ford_Fulkerson
04:15:07 Frequency_Moments: theory Graph_Theory.Arc_Walk
04:15:08 Frequency_Moments: theory Graph_Theory.Bidirected_Digraph
04:15:08 Frequency_Moments: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
04:15:09 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
04:15:09 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
04:15:09 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
04:15:10 Frequency_Moments: theory MFMC_Countable.MFMC_Finite
04:15:10 Frequency_Moments: theory HOL-Algebra.Coset
04:15:10 Frequency_Moments: theory HOL-Algebra.FiniteProduct
04:15:10 Frequency_Moments: theory Graph_Theory.Pair_Digraph
04:15:10 Frequency_Moments: theory HOL-Complex_Analysis.Winding_Numbers
04:15:11 Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
04:15:11 Frequency_Moments: theory Executable_Randomized_Algorithms.Coin_Space
04:15:11 Frequency_Moments: theory HOL-Algebra.Ring
04:15:12 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
04:15:12 Frequency_Moments: theory MFMC_Countable.MFMC_Misc
04:15:15 Frequency_Moments: theory HOL-Library.Interval
04:15:15 Frequency_Moments: theory HOL-Library.Float
04:15:15 Frequency_Moments: theory HOL-Complex_Analysis.Conformal_Mappings
04:15:15 Frequency_Moments: theory HOL-Algebra.Generated_Groups
04:15:16 Frequency_Moments: theory HOL-Algebra.Divisibility
04:15:16 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Singularities
04:15:17 Frequency_Moments: theory HOL-Algebra.Elementary_Groups
04:15:18 Frequency_Moments: theory HOL-Complex_Analysis.Great_Picard
04:15:19 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Residues
04:15:19 Frequency_Moments: theory HOL-Complex_Analysis.Riemann_Mapping
04:15:19 Frequency_Moments: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
04:15:19 Frequency_Moments: theory HOL-Algebra.AbelCoset
04:15:20 Frequency_Moments: theory HOL-Algebra.Module
04:15:20 Frequency_Moments: theory Jordan_Normal_Form.Missing_Ring
04:15:20 Frequency_Moments: theory HOL-Library.Code_Target_Numeral_Float
04:15:20 Frequency_Moments: theory HOL-Library.Interval_Float
04:15:20 Frequency_Moments: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
04:15:21 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_FPS
04:15:21 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_Factorial
04:15:21 Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
04:15:21 Frequency_Moments: theory Graph_Theory.Digraph_Component
04:15:21 Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
04:15:22 Frequency_Moments: theory HOL-Computational_Algebra.Formal_Laurent_Series
04:15:22 Frequency_Moments: theory HOL-Complex_Analysis.Residue_Theorem
04:15:22 Frequency_Moments: theory MFMC_Countable.Matrix_For_Marginals
04:15:22 Frequency_Moments: theory Polynomial_Interpolation.Missing_Polynomial
04:15:23 Frequency_Moments: theory Median_Method.Median
04:15:23 Frequency_Moments: theory HOL-Algebra.Ideal
04:15:24 Frequency_Moments: theory Polynomial_Factorization.Order_Polynomial
04:15:24 Frequency_Moments: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
04:15:25 Frequency_Moments: theory Lp.Functional_Spaces
04:15:25 Frequency_Moments: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
04:15:25 Frequency_Moments: theory Matrix.Utility
04:15:25 Frequency_Moments: theory HOL-Computational_Algebra.Computational_Algebra
04:15:26 Frequency_Moments: theory HOL-Complex_Analysis.Laurent_Convergence
04:15:26 Frequency_Moments: theory Graph_Theory.Digraph_Isomorphism
04:15:26 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom
04:15:26 Frequency_Moments: theory Regular-Sets.Regular_Set
04:15:26 Frequency_Moments: theory HOL-Algebra.RingHom
04:15:27 Frequency_Moments: theory HOL-Decision_Procs.Approximation
04:15:27 Frequency_Moments: theory VectorSpace.FunctionLemmas
04:15:27 Frequency_Moments: theory VectorSpace.RingModuleFacts
04:15:27 Frequency_Moments: theory Lp.Lp
04:15:27 Frequency_Moments: theory HOL-Algebra.QuotRing
04:15:28 Frequency_Moments: theory HOL-Algebra.UnivPoly
04:15:28 Frequency_Moments: theory HOL-Complex_Analysis.Meromorphic
04:15:28 Frequency_Moments: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
04:15:29 Frequency_Moments: theory Concentration_Inequalities.Bienaymes_Identity
04:15:29 Frequency_Moments: theory MFMC_Countable.Rel_PMF_Characterisation
04:15:29 Frequency_Moments: theory Probabilistic_While.While_SPMF
04:15:29 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
04:15:29 Frequency_Moments: theory HOL-Complex_Analysis.Weierstrass_Factorization
04:15:30 Frequency_Moments: theory VectorSpace.MonoidSums
04:15:30 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Analysis
04:15:30 Frequency_Moments: theory Jordan_Normal_Form.Matrix
04:15:30 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom_Poly
04:15:30 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects
04:15:30 Frequency_Moments: theory Expander_Graphs.Constructive_Chernoff_Bound
04:15:30 Frequency_Moments: theory HOL-Algebra.IntRing
04:15:30 Frequency_Moments: theory VectorSpace.LinearCombinations
04:15:31 Frequency_Moments: theory Regular-Sets.Regular_Exp
04:15:34 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian_Misc
04:15:34 Frequency_Moments: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
04:15:35 Frequency_Moments: theory Regular-Sets.NDerivative
04:15:35 Frequency_Moments: theory Regular-Sets.Relation_Interpretation
04:15:36 Frequency_Moments: theory Jordan_Normal_Form.Column_Operations
04:15:37 Frequency_Moments: theory VectorSpace.SumSpaces
04:15:37 Frequency_Moments: theory Jordan_Normal_Form.Determinant
04:15:37 Frequency_Moments: theory VectorSpace.VectorSpace
04:15:40 Frequency_Moments: theory Jordan_Normal_Form.Char_Poly
04:15:40 Frequency_Moments: theory Regular-Sets.Equivalence_Checking
04:15:40 Frequency_Moments: theory Regular-Sets.Regexp_Method
04:15:41 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form
04:15:41 Frequency_Moments: theory Abstract-Rewriting.Abstract_Rewriting
04:15:42 Frequency_Moments: theory Isabelle_Marries_Dirac.Basics
04:15:42 Frequency_Moments: theory Isabelle_Marries_Dirac.Binary_Nat
04:15:42 Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
04:15:42 Frequency_Moments: theory Isabelle_Marries_Dirac.Quantum
04:15:44 Frequency_Moments: theory Abstract-Rewriting.SN_Orders
04:15:45 Frequency_Moments: theory Jordan_Normal_Form.Missing_VectorSpace
04:15:45 Frequency_Moments: theory Isabelle_Marries_Dirac.Complex_Vectors
04:15:47 Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
04:15:47 Frequency_Moments: theory HOL-Algebra.Subrings
04:15:47 Frequency_Moments: theory HOL-Number_Theory.Residues
04:15:47 Frequency_Moments: theory Matrix.Ordered_Semiring
04:15:49 Frequency_Moments: theory Jordan_Normal_Form.VS_Connect
04:15:49 Frequency_Moments: theory Matrix.Matrix_Legacy
04:15:50 Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
04:15:50 Frequency_Moments: theory HOL-Number_Theory.Pocklington
04:15:50 Frequency_Moments: theory Lehmer.Lehmer
04:15:51 Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
04:15:51 Frequency_Moments: theory HOL-Number_Theory.Gauss
04:15:51 Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
04:15:51 Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
04:15:51 Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
04:15:51 Frequency_Moments: theory Matrix_Tensor.Matrix_Tensor
04:15:52 Frequency_Moments: theory HOL-Number_Theory.Number_Theory
04:15:54 Frequency_Moments: theory Isabelle_Marries_Dirac.Tensor
04:15:54 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Misc
04:15:54 Frequency_Moments: theory Dirichlet_Series.Multiplicative_Function
04:15:55 Frequency_Moments: theory Isabelle_Marries_Dirac.More_Tensor
04:15:55 Frequency_Moments: theory Bertrands_Postulate.Bertrand
04:15:55 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Product
04:15:55 Frequency_Moments: theory Dirichlet_Series.Euler_Products
04:15:55 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series
04:16:01 Frequency_Moments: theory HOL-Algebra.Polynomials
04:16:04 Frequency_Moments: theory Dirichlet_Series.Moebius_Mu
04:16:04 Frequency_Moments: theory Dirichlet_Series.More_Totient
04:16:04 Frequency_Moments: theory Dirichlet_Series.Liouville_Lambda
04:16:05 Frequency_Moments: theory Dirichlet_Series.Divisor_Count
04:16:05 Frequency_Moments: theory Dirichlet_Series.Arithmetic_Summatory
04:16:05 Frequency_Moments: theory Dirichlet_Series.Partial_Summation
04:16:07 Frequency_Moments: theory Jordan_Normal_Form.Gram_Schmidt
04:16:07 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series_Analysis
04:16:09 Frequency_Moments: theory Jordan_Normal_Form.Schur_Decomposition
04:16:14 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
04:16:17 Frequency_Moments: theory Zeta_Function.Zeta_Library
04:16:18 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
04:16:24 Frequency_Moments: theory Jordan_Normal_Form.Spectral_Radius
04:16:24 Frequency_Moments: theory QHLProver.Complex_Matrix
04:16:24 Frequency_Moments: theory Perron_Frobenius.HMA_Connect
04:16:24 Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
04:16:25 Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
04:16:25 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm
04:16:29 Frequency_Moments: theory QHLProver.Gates
04:16:30 Frequency_Moments: theory Projective_Measurements.Linear_Algebra_Complements
04:16:37 Frequency_Moments: theory Projective_Measurements.Projective_Measurements
04:16:39 Frequency_Moments: theory Commuting_Hermitian.Spectral_Theory_Complements
04:16:40 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian
04:16:57 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
04:16:58 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
04:16:58 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
04:17:10 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
04:17:13 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
04:17:13 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
04:17:13 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Definition
04:17:13 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
04:17:14 Frequency_Moments: theory Frequency_Moments.K_Smallest
04:17:17 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_TTS
04:17:17 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_MGG
04:17:18 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Algebra
04:17:19 Frequency_Moments: theory Frequency_Moments.Probability_Ext
04:17:21 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Eigenvalues
04:17:24 Frequency_Moments: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
04:17:24 Frequency_Moments: theory Finite_Fields.Formal_Polynomial_Derivatives
04:17:25 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
04:17:25 Frequency_Moments: theory Finite_Fields.Monic_Polynomial_Factorization
04:17:26 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
04:17:26 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
04:17:26 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
04:17:28 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Walks
04:17:31 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
04:17:31 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Power_Construction
04:17:35 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
04:17:38 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
04:17:38 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test
04:17:39 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials
04:17:42 Frequency_Moments: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
04:17:45 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test_Code
04:17:49 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
04:17:57 Frequency_Moments: theory Finite_Fields.Find_Irreducible_Poly
04:18:04 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
04:18:09 Frequency_Moments: theory Frequency_Moments.Tutorial_Pseudorandom_Objects
04:28:31 Preparing Frequency_Moments/document ...
04:28:39 Finished Frequency_Moments/document (0:00:08 elapsed time)
04:28:39 Preparing Frequency_Moments/outline ...
04:28:43 Finished Frequency_Moments/outline (0:00:03 elapsed time)
04:28:44 Timing Frequency_Moments (8 threads, 722.027s elapsed time, 4268.958s cpu time, 372.974s GC time, factor 5.91)
04:28:44 Finished Frequency_Moments (0:13:23 elapsed time, 1:14:28 cpu time, factor 5.56)
04:28:44 Running HOL-ODE-ARCH-COMP (on hpcisabelle/3) ...
04:28:48 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
04:41:04 Timing HOL-ODE-ARCH-COMP (8 threads, 735.409s elapsed time, 1668.258s cpu time, 17.974s GC time, factor 2.27)
04:41:04 Finished HOL-ODE-ARCH-COMP (0:12:19 elapsed time, 0:27:54 cpu time, factor 2.26)
04:41:04 Building Sepref_Prereq (on hpcisabelle/4) ...
04:41:07 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
04:41:07 Sepref_Prereq: theory HOL-Library.Nat_Bijection
04:41:07 Sepref_Prereq: theory HOL-Library.Old_Datatype
04:41:08 Sepref_Prereq: theory HOL-Library.Countable
04:41:10 Sepref_Prereq: theory HOL-Imperative_HOL.Heap
04:41:11 Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
04:41:14 Sepref_Prereq: theory HOL-Imperative_HOL.Array
04:41:15 Sepref_Prereq: theory HOL-Imperative_HOL.Ref
04:41:15 Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
04:41:15 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
04:41:15 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
04:41:16 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
04:41:18 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
04:41:18 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
04:41:20 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
04:41:21 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
04:41:21 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
04:41:24 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
04:41:25 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
04:41:30 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
04:41:35 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
04:41:35 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
04:41:36 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
04:41:36 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
04:41:37 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
04:41:39 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
04:41:58 Timing Sepref_Prereq (8 threads, 34.770s elapsed time, 102.365s cpu time, 3.141s GC time, factor 2.94)
04:41:58 Finished Sepref_Prereq (0:00:52 elapsed time, 0:02:16 cpu time, factor 2.59)
04:41:58 Running MiniSail (on hpcisabelle/5) ...
04:42:01 MiniSail: theory HOL-Eisbach.Eisbach
04:42:01 MiniSail: theory FinFun.FinFun
04:42:02 MiniSail: theory HOL-Eisbach.Eisbach_Tools
04:42:02 MiniSail: theory Nominal2.Nominal2_Base
04:42:08 MiniSail: theory Nominal2.Nominal2_Abs
04:42:11 MiniSail: theory Nominal2.Nominal2_FCB
04:42:11 MiniSail: theory Nominal2.Nominal2
04:42:16 MiniSail FAILED (see also "isabelle build_log -H Error MiniSail")
04:42:16 *** Failed to load theory "MiniSail.Nominal-Utils" (unresolved "Nominal2.Nominal2")
04:42:16 *** Failed to load theory "MiniSail.Syntax" (unresolved "MiniSail.Nominal-Utils", "Nominal2.Nominal2")
04:42:16 *** Failed to load theory "MiniSail.BTVSubst" (unresolved "MiniSail.Syntax")
04:42:16 *** Failed to load theory "MiniSail.IVSubst" (unresolved "MiniSail.Syntax")
04:42:16 *** Failed to load theory "MiniSail.Wellformed" (unresolved "MiniSail.BTVSubst", "MiniSail.IVSubst")
04:42:16 *** Failed to load theory "MiniSail.SyntaxL" (unresolved "MiniSail.IVSubst", "MiniSail.Syntax")
04:42:16 *** Failed to load theory "MiniSail.RCLogic" (unresolved "MiniSail.Wellformed")
04:42:16 *** Failed to load theory "MiniSail.WellformedL" (unresolved "MiniSail.SyntaxL", "MiniSail.Wellformed")
04:42:16 *** Failed to load theory "MiniSail.SubstMethods" (unresolved "MiniSail.IVSubst", "MiniSail.WellformedL")
04:42:16 *** Failed to load theory "MiniSail.RCLogicL" (unresolved "MiniSail.RCLogic", "MiniSail.WellformedL")
04:42:16 *** Failed to load theory "MiniSail.Typing" (unresolved "MiniSail.RCLogic", "MiniSail.WellformedL")
04:42:16 *** Failed to load theory "MiniSail.Operational" (unresolved "MiniSail.Typing")
04:42:16 *** Failed to load theory "MiniSail.TypingL" (unresolved "MiniSail.RCLogicL", "MiniSail.Typing")
04:42:16 *** Failed to load theory "MiniSail.ContextSubtypingL" (unresolved "MiniSail.SubstMethods", "MiniSail.TypingL")
04:42:16 *** Failed to load theory "MiniSail.BTVSubstTypingL" (unresolved "MiniSail.ContextSubtypingL", "MiniSail.SubstMethods")
04:42:16 *** Failed to load theory "MiniSail.IVSubstTypingL" (unresolved "MiniSail.ContextSubtypingL", "MiniSail.SubstMethods")
04:42:16 *** Failed to load theory "MiniSail.Safety" (unresolved "MiniSail.BTVSubstTypingL", "MiniSail.IVSubstTypingL", "MiniSail.Operational")
04:42:16 *** Failed to load theory "MiniSail.MiniSail" (unresolved "MiniSail.Safety")
04:42:16 *** Undefined fact: "Wellfounded.wfP_induct_rule" (line 880 of "$AFP/Nominal2/nominal_function_core.ML")
04:42:16 *** At command "ML_file" (line 38 of "$AFP/Nominal2/Nominal2.thy")
04:42:16 Running Finite_Fields (on hpcisabelle/6) ...
04:42:21 Finite_Fields: theory Digit_Expansions.Bits_Digits
04:42:21 Finite_Fields: theory Flow_Networks.Graph
04:42:21 Finite_Fields: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
04:42:21 Finite_Fields: theory HOL-Number_Theory.Cong
04:42:21 Finite_Fields: theory HOL-Real_Asymp.Inst_Existentials
04:42:21 Finite_Fields: theory HOL-Types_To_Sets.Types_To_Sets
04:42:21 Finite_Fields: theory HOL-Number_Theory.Eratosthenes
04:42:21 Finite_Fields: theory HOL-Analysis.Metric_Arith
04:42:21 Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results
04:42:22 Finite_Fields: theory Finite_Fields.Finite_Fields_More_Bijections
04:42:22 Finite_Fields: theory HOL-Analysis.Abstract_Topology
04:42:22 Finite_Fields: theory HOL-Analysis.Continuum_Not_Denumerable
04:42:22 Finite_Fields: theory HOL-Analysis.Inner_Product
04:42:22 Finite_Fields: theory HOL-Analysis.L2_Norm
04:42:23 Finite_Fields: theory HOL-Analysis.Operator_Norm
04:42:23 Finite_Fields: theory HOL-Analysis.Poly_Roots
04:42:23 Finite_Fields: theory HOL-Analysis.Product_Vector
04:42:23 Finite_Fields: theory HOL-Combinatorics.Multiset_Permutations
04:42:23 Finite_Fields: theory HOL-Number_Theory.Mod_Exp
04:42:24 Finite_Fields: theory HOL-Analysis.Sigma_Algebra
04:42:24 Finite_Fields: theory Flow_Networks.Network
04:42:24 Finite_Fields: theory HOL-Analysis.Norm_Arith
04:42:25 Finite_Fields: theory HOL-Number_Theory.Fib
04:42:25 Finite_Fields: theory HOL-Number_Theory.Prime_Powers
04:42:25 Finite_Fields: theory HOL-Number_Theory.Totient
04:42:25 Finite_Fields: theory HOL-Real_Asymp.Eventuallize
04:42:26 Finite_Fields: theory HOL-Real_Asymp.Lazy_Eval
04:42:26 Finite_Fields: theory HOL-Number_Theory.Residues
04:42:26 Finite_Fields: theory HOL-Analysis.Elementary_Topology
04:42:26 Finite_Fields: theory HOL-Analysis.Euclidean_Space
04:42:27 Finite_Fields: theory Flow_Networks.Residual_Graph
04:42:27 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion
04:42:27 Finite_Fields: theory HOL-Analysis.Measurable
04:42:28 Finite_Fields: theory HOL-Analysis.Abstract_Limits
04:42:29 Finite_Fields: theory HOL-Analysis.FSigma
04:42:29 Finite_Fields: theory HOL-Analysis.Sum_Topology
04:42:29 Finite_Fields: theory HOL-Analysis.Measure_Space
04:42:31 Finite_Fields: theory Flow_Networks.Augmenting_Flow
04:42:31 Finite_Fields: theory Flow_Networks.Augmenting_Path
04:42:31 Finite_Fields: theory HOL-Analysis.Finite_Cartesian_Product
04:42:31 Finite_Fields: theory HOL-Analysis.Linear_Algebra
04:42:31 Finite_Fields: theory HOL-Analysis.Abstract_Topology_2
04:42:31 Finite_Fields: theory Flow_Networks.Ford_Fulkerson
04:42:31 Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
04:42:32 Finite_Fields: theory Finite_Fields.Ring_Characteristic
04:42:32 Finite_Fields: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
04:42:34 Finite_Fields: theory HOL-Analysis.Affine
04:42:34 Finite_Fields: theory HOL-Analysis.Infinite_Sum
04:42:35 Finite_Fields: theory MFMC_Countable.MFMC_Finite
04:42:35 Finite_Fields: theory HOL-Analysis.Cartesian_Space
04:42:35 Finite_Fields: theory HOL-Analysis.Convex
04:42:35 Finite_Fields: theory HOL-Analysis.Caratheodory
04:42:35 Finite_Fields: theory HOL-Analysis.Connected
04:42:35 Finite_Fields: theory HOL-Analysis.Elementary_Metric_Spaces
04:42:35 Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
04:42:36 Finite_Fields: theory HOL-Analysis.Function_Topology
04:42:36 Finite_Fields: theory HOL-Number_Theory.Gauss
04:42:37 Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
04:42:38 Finite_Fields: theory HOL-Analysis.Product_Topology
04:42:38 Finite_Fields: theory HOL-Number_Theory.Pocklington
04:42:38 Finite_Fields: theory HOL-Analysis.T1_Spaces
04:42:39 Finite_Fields: theory HOL-Analysis.Determinants
04:42:39 Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
04:42:39 Finite_Fields: theory HOL-Analysis.Lindelof_Spaces
04:42:39 Finite_Fields: theory HOL-Number_Theory.Number_Theory
04:42:40 Finite_Fields: theory HOL-Analysis.Elementary_Normed_Spaces
04:42:40 Finite_Fields: theory HOL-Analysis.Function_Metric
04:42:40 Finite_Fields: theory HOL-Analysis.Isolated
04:42:41 Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
04:42:41 Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
04:42:41 Finite_Fields: theory HOL-Analysis.Topology_Euclidean_Space
04:42:41 Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
04:42:41 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
04:42:43 Finite_Fields: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
04:42:43 Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
04:42:43 Finite_Fields: theory HOL-Analysis.Extended_Real_Limits
04:42:44 Finite_Fields: theory HOL-Analysis.Line_Segment
04:42:44 Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
04:42:44 Finite_Fields: theory HOL-Analysis.Tagged_Division
04:42:45 Finite_Fields: theory HOL-Analysis.Summation_Tests
04:42:45 Finite_Fields: theory HOL-Analysis.Convex_Euclidean_Space
04:42:46 Finite_Fields: theory Dirichlet_Series.Moebius_Mu
04:42:46 Finite_Fields: theory Dirichlet_Series.More_Totient
04:42:46 Finite_Fields: theory Dirichlet_Series.Divisor_Count
04:42:47 Finite_Fields: theory HOL-Analysis.Uniform_Limit
04:42:47 Finite_Fields: theory Dirichlet_Series.Liouville_Lambda
04:42:47 Finite_Fields: theory HOL-Analysis.Ordered_Euclidean_Space
04:42:47 Finite_Fields: theory HOL-Analysis.Starlike
04:42:47 Finite_Fields: theory Dirichlet_Series.Arithmetic_Summatory
04:42:49 Finite_Fields: theory HOL-Analysis.Bounded_Continuous_Function
04:42:49 Finite_Fields: theory HOL-Analysis.Bounded_Linear_Function
04:42:50 Finite_Fields: theory HOL-Analysis.Continuous_Extension
04:42:50 Finite_Fields: theory HOL-Analysis.Path_Connected
04:42:50 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
04:42:51 Finite_Fields: theory HOL-Analysis.Derivative
04:42:52 Finite_Fields: theory HOL-Analysis.Locally
04:42:52 Finite_Fields: theory HOL-Analysis.Uncountable_Sets
04:42:52 Finite_Fields: theory HOL-Analysis.Arcwise_Connected
04:42:53 Finite_Fields: theory HOL-Analysis.Homotopy
04:42:54 Finite_Fields: theory HOL-Analysis.Borel_Space
04:42:54 Finite_Fields: theory HOL-Analysis.Cartesian_Euclidean_Space
04:42:54 Finite_Fields: theory HOL-Analysis.Complex_Analysis_Basics
04:42:55 Finite_Fields: theory HOL-Analysis.Weierstrass_Theorems
04:42:55 Finite_Fields: theory HOL-Analysis.Cross3
04:42:56 Finite_Fields: theory HOL-Analysis.Polytope
04:42:57 Finite_Fields: theory HOL-Analysis.Abstract_Euclidean_Space
04:42:57 Finite_Fields: theory HOL-Analysis.Homeomorphism
04:42:58 Finite_Fields: theory HOL-Analysis.Sparse_In
04:42:59 Finite_Fields: theory HOL-Analysis.Abstract_Topological_Spaces
04:42:59 Finite_Fields: theory HOL-Analysis.Complex_Transcendental
04:43:00 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
04:43:00 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test
04:43:00 Finite_Fields: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
04:43:00 Finite_Fields: theory HOL-Analysis.Regularity
04:43:01 Finite_Fields: theory HOL-Analysis.Brouwer_Fixpoint
04:43:02 Finite_Fields: theory Executable_Randomized_Algorithms.Tau_Additivity
04:43:02 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
04:43:05 Finite_Fields: theory HOL-Analysis.Generalised_Binomial_Theorem
04:43:05 Finite_Fields: theory HOL-Analysis.FPS_Convergence
04:43:05 Finite_Fields: theory HOL-Analysis.Harmonic_Numbers
04:43:06 Finite_Fields: theory HOL-Analysis.Binary_Product_Measure
04:43:06 Finite_Fields: theory HOL-Analysis.Infinite_Products
04:43:06 Finite_Fields: theory HOL-Analysis.Abstract_Metric_Spaces
04:43:07 Finite_Fields: theory HOL-Analysis.Embed_Measure
04:43:07 Finite_Fields: theory HOL-Analysis.Finite_Product_Measure
04:43:07 Finite_Fields: theory HOL-Analysis.Fashoda_Theorem
04:43:07 Finite_Fields: theory HOL-Analysis.Retracts
04:43:08 Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
04:43:09 Finite_Fields: theory HOL-Analysis.Bochner_Integration
04:43:09 Finite_Fields: theory HOL-Probability.Fin_Map
04:43:10 Finite_Fields: theory HOL-Analysis.Smooth_Paths
04:43:10 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test_Code
04:43:13 Finite_Fields: theory HOL-Analysis.Lipschitz
04:43:13 Finite_Fields: theory HOL-Analysis.Complete_Measure
04:43:13 Finite_Fields: theory HOL-Analysis.Radon_Nikodym
04:43:13 Finite_Fields: theory HOL-Analysis.Urysohn
04:43:14 Finite_Fields: theory HOL-Analysis.Set_Integral
04:43:14 Finite_Fields: theory HOL-Analysis.Lebesgue_Measure
04:43:15 Finite_Fields: theory HOL-Analysis.Multivariate_Analysis
04:43:16 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
04:43:16 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
04:43:16 Finite_Fields: theory HOL-Analysis.Infinite_Set_Sum
04:43:19 Finite_Fields: theory HOL-Analysis.Henstock_Kurzweil_Integration
04:43:21 Finite_Fields: theory HOL-Real_Asymp.Real_Asymp
04:43:24 Finite_Fields: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
04:43:24 Finite_Fields: theory HOL-Analysis.Integral_Test
04:43:24 Finite_Fields: theory HOL-Analysis.Kronecker_Approximation_Theorem
04:43:26 Finite_Fields: theory HOL-Analysis.Further_Topology
04:43:26 Finite_Fields: theory HOL-Analysis.Gamma_Function
04:43:26 Finite_Fields: theory HOL-Analysis.Improper_Integral
04:43:26 Finite_Fields: theory HOL-Analysis.Interval_Integral
04:43:26 Finite_Fields: theory HOL-Analysis.Vitali_Covering_Theorem
04:43:27 Finite_Fields: theory HOL-Analysis.Equivalence_Measurable_On_Borel
04:43:27 Finite_Fields: theory HOL-Analysis.Lebesgue_Integral_Substitution
04:43:28 Finite_Fields: theory HOL-Analysis.Change_Of_Vars
04:43:30 Finite_Fields: theory HOL-Analysis.Simplex_Content
04:43:31 Finite_Fields: theory HOL-Analysis.Jordan_Curve
04:43:32 Finite_Fields: theory HOL-Analysis.Ball_Volume
04:43:32 Finite_Fields: theory HOL-Analysis.Analysis
04:43:33 Finite_Fields: theory Dirichlet_Series.Euler_Products
04:43:33 Finite_Fields: theory Dirichlet_Series.Partial_Summation
04:43:33 Finite_Fields: theory HOL-Complex_Analysis.Contour_Integration
04:43:33 Finite_Fields: theory HOL-Probability.Discrete_Topology
04:43:33 Finite_Fields: theory HOL-Probability.Essential_Supremum
04:43:33 Finite_Fields: theory HOL-Probability.Probability_Measure
04:43:33 Finite_Fields: theory HOL-Probability.Stopping_Time
04:43:33 Finite_Fields: theory HOL-Probability.Tree_Space
04:43:35 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
04:43:39 Finite_Fields: theory HOL-Complex_Analysis.Winding_Numbers
04:43:39 Finite_Fields: theory HOL-Probability.Conditional_Expectation
04:43:39 Finite_Fields: theory HOL-Probability.Distribution_Functions
04:43:39 Finite_Fields: theory HOL-Probability.Giry_Monad
04:43:39 Finite_Fields: theory HOL-Probability.Weak_Convergence
04:43:40 Finite_Fields: theory HOL-Probability.Helly_Selection
04:43:40 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
04:43:42 Finite_Fields: theory HOL-Probability.Probability_Mass_Function
04:43:42 Finite_Fields: theory HOL-Probability.Projective_Family
04:43:42 Finite_Fields: theory HOL-Complex_Analysis.Conformal_Mappings
04:43:43 Finite_Fields: theory HOL-Complex_Analysis.Complex_Singularities
04:43:43 Finite_Fields: theory HOL-Complex_Analysis.Great_Picard
04:43:43 Finite_Fields: theory HOL-Probability.Infinite_Product_Measure
04:43:43 Finite_Fields: theory HOL-Complex_Analysis.Riemann_Mapping
04:43:45 Finite_Fields: theory HOL-Probability.Independent_Family
04:43:45 Finite_Fields: theory HOL-Probability.Projective_Limit
04:43:45 Finite_Fields: theory HOL-Probability.Stream_Space
04:43:45 Finite_Fields: theory HOL-Complex_Analysis.Complex_Residues
04:43:46 Finite_Fields: theory HOL-Complex_Analysis.Residue_Theorem
04:43:46 Finite_Fields: theory Finite_Fields.Finite_Fields_More_PMF
04:43:46 Finite_Fields: theory HOL-Probability.PMF_Impl
04:43:46 Finite_Fields: theory HOL-Probability.Random_Permutations
04:43:46 Finite_Fields: theory HOL-Probability.SPMF
04:43:46 Finite_Fields: theory HOL-Complex_Analysis.Laurent_Convergence
04:43:46 Finite_Fields: theory HOL-Probability.Convolution
04:43:47 Finite_Fields: theory HOL-Probability.Information
04:43:47 Finite_Fields: theory HOL-Probability.Product_PMF
04:43:48 Finite_Fields: theory HOL-Probability.Hoeffding
04:43:49 Finite_Fields: theory HOL-Probability.Distributions
04:43:51 Finite_Fields: theory HOL-Complex_Analysis.Meromorphic
04:43:51 Finite_Fields: theory HOL-Probability.Characteristic_Functions
04:43:51 Finite_Fields: theory HOL-Probability.Sinc_Integral
04:43:51 Finite_Fields: theory HOL-Complex_Analysis.Weierstrass_Factorization
04:43:52 Finite_Fields: theory HOL-Complex_Analysis.Complex_Analysis
04:43:52 Finite_Fields: theory HOL-Probability.Levy
04:43:52 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series_Analysis
04:43:52 Finite_Fields: theory HOL-Probability.Central_Limit_Theorem
04:43:52 Finite_Fields: theory HOL-Probability.Probability
04:43:59 Finite_Fields: theory Executable_Randomized_Algorithms.Coin_Space
04:43:59 Finite_Fields: theory MFMC_Countable.MFMC_Misc
04:44:00 Finite_Fields: theory MFMC_Countable.Matrix_For_Marginals
04:44:01 Finite_Fields: theory MFMC_Countable.Rel_PMF_Characterisation
04:44:01 Finite_Fields: theory Probabilistic_While.While_SPMF
04:44:02 Finite_Fields: theory Zeta_Function.Zeta_Library
04:44:03 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
04:44:05 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm
04:44:07 Finite_Fields: theory Finite_Fields.Find_Irreducible_Poly
04:54:49 Preparing Finite_Fields/document ...
04:55:00 Finished Finite_Fields/document (0:00:11 elapsed time)
04:55:00 Preparing Finite_Fields/outline ...
04:55:05 Finished Finite_Fields/outline (0:00:04 elapsed time)
04:55:05 Timing Finite_Fields (8 threads, 724.233s elapsed time, 5006.082s cpu time, 515.027s GC time, factor 6.91)
04:55:05 Finished Finite_Fields (0:12:11 elapsed time, 1:23:56 cpu time, factor 6.89)
04:55:05 Building Refine_Imperative_HOL (on hpcisabelle/7) ...
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.User_Smashing
04:55:08 Refine_Imperative_HOL: theory Isar_Ref.Base
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.PO_Normalizer
04:55:08 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Misc
04:55:08 Refine_Imperative_HOL: theory List-Index.List_Index
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Concl_Pres_Clarification
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Add
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Named_Theorems_Rev
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Structured_Apply
04:55:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Mono_Prover
04:55:08 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Refine_Aux
04:55:09 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Misc
04:55:10 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Term_Synth
04:55:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_IICF
04:55:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Setup
04:55:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Userguides
04:55:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Tool
04:55:11 Refine_Imperative_HOL: theory HOL-Library.Rewrite
04:55:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Id_Op
04:55:11 Refine_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
04:55:12 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Basic
04:55:14 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Constraints
04:55:14 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Monadify
04:55:15 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Frame
04:55:15 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Rules
04:55:19 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
04:55:19 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Definition
04:55:20 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Translate
04:55:23 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Intf_Util
04:55:25 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Tool
04:55:25 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
04:55:29 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Foreach
04:55:30 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Improper
04:55:30 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref
04:55:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Map
04:55:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List
04:55:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Matrix
04:55:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Set
04:55:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Multiset
04:55:32 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Map
04:55:32 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_SetO
04:55:32 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_Mset
04:55:32 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_MsetO
04:55:32 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Bag
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_List
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_HOL_List
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_MS_Array_List
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heap
04:55:33 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Sepl_Binding
04:55:34 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
04:55:34 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
04:55:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heap
04:55:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_Matrix
04:55:37 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
04:55:53 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF
04:55:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_General_Util
04:55:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
04:55:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Reference
04:56:42 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc
04:56:42 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph
04:56:42 Refine_Imperative_HOL: theory HOL-Library.Omega_Words_Fun
04:56:42 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight
04:56:42 Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph
04:56:42 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
04:56:42 Refine_Imperative_HOL: theory CAVA_Automata.Digraph_Basic
04:56:43 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec
04:56:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph
04:56:46 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra
04:56:48 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA
04:56:48 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap
04:56:51 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl
04:56:51 Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS
04:56:54 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
04:57:37 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator
04:57:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype
04:57:47 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
04:57:49 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS
04:57:49 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS
04:57:49 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests
04:58:05 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark
04:58:18 Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark
04:58:18 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples
04:59:18 Preparing Refine_Imperative_HOL/document ...
04:59:32 Finished Refine_Imperative_HOL/document (0:00:13 elapsed time)
04:59:32 Preparing Refine_Imperative_HOL/outline ...
04:59:41 Finished Refine_Imperative_HOL/outline (0:00:08 elapsed time)
04:59:41 Timing Refine_Imperative_HOL (8 threads, 221.742s elapsed time, 581.099s cpu time, 23.968s GC time, factor 2.62)
04:59:41 Finished Refine_Imperative_HOL (0:04:10 elapsed time, 0:10:43 cpu time, factor 2.57)
04:59:41 Building Word_Lib (on hpcisabelle/0) ...
04:59:42 Word_Lib: theory Word_Lib.Even_More_List
04:59:42 Word_Lib: theory Word_Lib.Enumeration
04:59:42 Word_Lib: theory HOL-Library.Phantom_Type
04:59:42 Word_Lib: theory HOL-Library.Sublist
04:59:43 Word_Lib: theory Word_Lib.More_Bit_Ring
04:59:43 Word_Lib: theory Word_Lib.More_Misc
04:59:44 Word_Lib: theory HOL-Library.Cardinality
04:59:45 Word_Lib: theory HOL-Library.Numeral_Type
04:59:46 Word_Lib: theory Word_Lib.More_Sublist
04:59:46 Word_Lib: theory HOL-Library.Type_Length
04:59:47 Word_Lib: theory Word_Lib.More_Arithmetic
04:59:47 Word_Lib: theory HOL-Library.Word
04:59:57 Word_Lib: theory Word_Lib.Legacy_Aliases
04:59:57 Word_Lib: theory Word_Lib.More_Divides
04:59:57 Word_Lib: theory Word_Lib.More_Word
04:59:59 Word_Lib: theory Word_Lib.Strict_part_mono
05:00:04 Word_Lib: theory Word_Lib.Bit_Comprehension
05:00:04 Word_Lib: theory HOL-Library.Signed_Division
05:00:04 Word_Lib: theory Word_Lib.Least_significant_bit
05:00:04 Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
05:00:05 Word_Lib: theory Word_Lib.Signed_Division_Word
05:00:06 Word_Lib: theory Word_Lib.Aligned
05:00:06 Word_Lib: theory Word_Lib.Most_significant_bit
05:00:06 Word_Lib: theory Word_Lib.Generic_set_bit
05:00:07 Word_Lib: theory Word_Lib.Next_and_Prev
05:00:07 Word_Lib: theory Word_Lib.Bits_Int
05:00:13 Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
05:00:13 Word_Lib: theory Word_Lib.Many_More
05:00:13 Word_Lib: theory Word_Lib.Typedef_Morphisms
05:00:15 Word_Lib: theory HOL-Eisbach.Eisbach
05:00:15 Word_Lib: theory Word_Lib.Bit_Comprehension_Int
05:00:15 Word_Lib: theory Word_Lib.Hex_Words
05:00:15 Word_Lib: theory Word_Lib.Signed_Words
05:00:15 Word_Lib: theory Word_Lib.Syntax_Bundles
05:00:15 Word_Lib: theory Word_Lib.Word_Syntax
05:00:15 Word_Lib: theory Word_Lib.Type_Syntax
05:00:15 Word_Lib: theory Word_Lib.Enumeration_Word
05:00:15 Word_Lib: theory Word_Lib.Sgn_Abs
05:00:15 Word_Lib: theory Word_Lib.Rsplit
05:00:15 Word_Lib: theory Word_Lib.Reversed_Bit_Lists
05:00:15 Word_Lib: theory Word_Lib.Norm_Words
05:00:15 Word_Lib: theory Word_Lib.Word_Names
05:00:15 Word_Lib: theory Word_Lib.Word_16
05:00:16 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
05:00:16 Word_Lib: theory Word_Lib.Word_EqI
05:00:18 Word_Lib: theory Word_Lib.Bitwise
05:00:18 Word_Lib: theory Word_Lib.Bitwise_Signed
05:00:19 Word_Lib: theory Word_Lib.Boolean_Inequalities
05:00:22 Word_Lib: theory Word_Lib.Word_Lemmas
05:00:25 Word_Lib: theory Word_Lib.Word_8
05:00:25 Word_Lib: theory Word_Lib.More_Word_Operations
05:00:26 Word_Lib: theory Word_Lib.Word_32
05:00:26 Word_Lib: theory Word_Lib.Word_64
05:00:27 Word_Lib: theory Word_Lib.Machine_Word_64_Basics
05:00:27 Word_Lib: theory Word_Lib.Machine_Word_64
05:00:28 Word_Lib: theory Word_Lib.Machine_Word_32_Basics
05:00:28 Word_Lib: theory Word_Lib.Word_Lib_Sumo
05:00:28 Word_Lib: theory Word_Lib.Machine_Word_32
05:00:31 Word_Lib: theory Word_Lib.Guide
05:00:33 Word_Lib: theory Word_Lib.Examples
05:00:48 Preparing Word_Lib/document ...
05:00:56 Finished Word_Lib/document (0:00:08 elapsed time)
05:00:56 Preparing Word_Lib/outline ...
05:01:03 Finished Word_Lib/outline (0:00:06 elapsed time)
05:01:03 Timing Word_Lib (8 threads, 52.650s elapsed time, 287.742s cpu time, 7.086s GC time, factor 5.47)
05:01:03 Finished Word_Lib (0:01:05 elapsed time, 0:05:12 cpu time, factor 4.80)
05:01:03 Building HOL-Proofs (on hpcisabelle/1) ...
05:01:05 HOL-Proofs: theory Tools.Code_Generator
05:01:11 HOL-Proofs: theory HOL.HOL
05:01:18 HOL-Proofs: theory HOL.Argo
05:01:18 HOL-Proofs: theory HOL.Ctr_Sugar
05:01:18 HOL-Proofs: theory HOL.Orderings
05:01:22 HOL-Proofs: theory HOL.Groups
05:01:23 HOL-Proofs: theory HOL.SAT
05:01:25 HOL-Proofs: theory HOL.Lattices
05:01:29 HOL-Proofs: theory HOL.Boolean_Algebras
05:01:30 HOL-Proofs: theory HOL.Set
05:01:35 HOL-Proofs: theory HOL.Fun
05:01:35 HOL-Proofs: theory HOL.Typedef
05:01:39 HOL-Proofs: theory HOL.Complete_Lattices
05:01:39 HOL-Proofs: theory HOL.Rings
05:01:46 HOL-Proofs: theory HOL.Inductive
05:01:51 HOL-Proofs: theory HOL.Product_Type
05:01:51 HOL-Proofs: theory HOL.Sum_Type
05:01:53 HOL-Proofs: theory HOL.Complete_Partial_Order
05:02:04 HOL-Proofs: theory HOL.Nat
05:02:10 HOL-Proofs: theory HOL.Fields
05:02:10 HOL-Proofs: theory HOL.Meson
05:02:19 HOL-Proofs: theory HOL.Relation
05:02:24 HOL-Proofs: theory HOL.Finite_Set
05:02:49 HOL-Proofs: theory HOL.Transitive_Closure
05:02:57 HOL-Proofs: theory HOL.Wellfounded
05:03:00 HOL-Proofs: theory HOL.Fun_Def_Base
05:03:00 HOL-Proofs: theory HOL.Wfrec
05:03:00 HOL-Proofs: theory HOL.Hilbert_Choice
05:03:01 HOL-Proofs: theory HOL.Order_Relation
05:03:02 HOL-Proofs: theory HOL.BNF_Wellorder_Relation
05:03:05 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
05:03:05 HOL-Proofs: theory HOL.Zorn
05:03:05 HOL-Proofs: theory HOL.ATP
05:03:11 HOL-Proofs: theory HOL.Metis
05:03:12 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
05:03:18 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
05:03:24 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
05:03:26 HOL-Proofs: theory HOL.BNF_Def
05:03:31 HOL-Proofs: theory HOL.BNF_Composition
05:03:31 HOL-Proofs: theory HOL.Basic_BNFs
05:03:32 HOL-Proofs: theory HOL.BNF_Fixpoint_Base
05:03:39 HOL-Proofs: theory HOL.BNF_Least_Fixpoint
05:03:46 HOL-Proofs: theory HOL.Basic_BNF_LFPs
05:03:46 HOL-Proofs: theory HOL.Equiv_Relations
05:03:46 HOL-Proofs: theory HOL.Transfer
05:03:48 HOL-Proofs: theory HOL.Num
05:03:50 HOL-Proofs: theory HOL.Lifting
05:03:54 HOL-Proofs: theory HOL.Power
05:03:55 HOL-Proofs: theory HOL.Option
05:03:55 HOL-Proofs: theory HOL.Quotient
05:03:56 HOL-Proofs: theory HOL.Extraction
05:03:56 HOL-Proofs: theory HOL.Partial_Function
05:03:59 HOL-Proofs: theory HOL.Fun_Def
05:04:01 HOL-Proofs: theory HOL.Groups_Big
05:04:16 HOL-Proofs: theory HOL.Int
05:04:16 HOL-Proofs: theory HOL.Lattices_Big
05:04:16 HOL-Proofs: theory HOL.Lifting_Set
05:04:27 HOL-Proofs: theory HOL.Euclidean_Rings
05:04:59 HOL-Proofs: theory HOL.Parity
05:05:18 HOL-Proofs: theory HOL.Divides
05:05:18 HOL-Proofs: theory HOL.Numeral_Simprocs
05:05:18 HOL-Proofs: theory HOL.Set_Interval
05:05:19 HOL-Proofs: theory HOL.SMT
05:05:19 HOL-Proofs: theory HOL.Semiring_Normalization
05:05:24 HOL-Proofs: theory HOL.Groebner_Basis
05:05:48 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
05:05:48 HOL-Proofs: theory HOL.Filter
05:05:48 HOL-Proofs: theory HOL.Presburger
05:06:03 HOL-Proofs: theory HOL.Sledgehammer
05:06:08 HOL-Proofs: theory HOL.List
05:07:43 HOL-Proofs: theory HOL.Groups_List
05:07:43 HOL-Proofs: theory HOL.Map
05:07:49 HOL-Proofs: theory HOL.Bit_Operations
05:07:49 HOL-Proofs: theory HOL.Enum
05:07:49 HOL-Proofs: theory HOL.Factorial
05:07:53 HOL-Proofs: theory HOL.Binomial
05:08:44 HOL-Proofs: theory HOL.Code_Numeral
05:08:58 HOL-Proofs: theory HOL.GCD
05:08:58 HOL-Proofs: theory HOL.String
05:08:58 HOL-Proofs: theory HOL.Random
05:09:20 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
05:09:20 HOL-Proofs: theory HOL.Predicate
05:09:20 HOL-Proofs: theory HOL.Typerep
05:09:23 HOL-Proofs: theory HOL.Lazy_Sequence
05:09:25 HOL-Proofs: theory HOL.Limited_Sequence
05:09:25 HOL-Proofs: theory HOL.Code_Evaluation
05:09:27 HOL-Proofs: theory HOL.Quickcheck_Random
05:09:31 HOL-Proofs: theory HOL.Random_Pred
05:09:31 HOL-Proofs: theory HOL.Quickcheck_Narrowing
05:09:31 HOL-Proofs: theory HOL.Quickcheck_Exhaustive
05:09:31 HOL-Proofs: theory HOL.Random_Sequence
05:09:36 HOL-Proofs: theory HOL.Record
05:09:36 HOL-Proofs: theory HOL.Predicate_Compile
05:09:40 HOL-Proofs: theory HOL.Nitpick
05:09:41 HOL-Proofs: theory HOL.Mirabelle
05:09:49 HOL-Proofs: theory HOL.Nunchaku
05:09:50 HOL-Proofs: theory Main
05:09:52 HOL-Proofs: theory HOL-Library.Realizers
05:12:00 Timing HOL-Proofs (8 threads, 533.095s elapsed time, 925.157s cpu time, 116.285s GC time, factor 1.74)
05:12:01 Finished HOL-Proofs (0:10:42 elapsed time, 0:20:26 cpu time, factor 1.91)
05:12:01 Building Subresultants (on hpcisabelle/2) ...
05:12:04 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
05:12:04 Subresultants: theory Subresultants.Coeff_Int
05:12:04 Subresultants: theory Subresultants.Dichotomous_Lazard
05:12:04 Subresultants: theory Subresultants.More_Homomorphisms
05:12:04 Subresultants: theory Subresultants.Binary_Exponentiation
05:12:04 Subresultants: theory Subresultants.Resultant_Prelim
05:12:05 Subresultants: theory Subresultants.Subresultant
05:12:10 Subresultants: theory Subresultants.Subresultant_Gcd
05:13:17 Preparing Subresultants/document ...
05:13:24 Finished Subresultants/document (0:00:06 elapsed time)
05:13:24 Preparing Subresultants/outline ...
05:13:27 Finished Subresultants/outline (0:00:03 elapsed time)
05:13:27 Timing Subresultants (8 threads, 55.841s elapsed time, 273.557s cpu time, 2.446s GC time, factor 4.90)
05:13:27 Finished Subresultants (0:01:16 elapsed time, 0:05:12 cpu time, factor 4.10)
05:13:28 Building Syntax_Independent_Logic (on hpcisabelle/3) ...
05:13:29 Syntax_Independent_Logic: theory HOL-Eisbach.Eisbach
05:13:30 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Prelim
05:13:34 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax
05:13:38 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction
05:13:39 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax_Arith
05:13:42 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Natural_Deduction
05:13:42 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Standard_Model
05:14:13 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Pseudo_Term
05:14:13 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction_Q
05:14:39 Build timed out (after 300 minutes). Marking the build as failed.
05:14:39 Build was aborted
05:19:01 Started calculate disk usage of build
05:19:01 Finished Calculation of disk usage of build in 0 seconds
05:19:02 Started calculate disk usage of workspace
05:19:03 Finished Calculation of disk usage of workspace in  1 second
05:19:04 No emails were triggered.
05:19:04 Finished: FAILURE