Console Output

19:08:03 Started by an SCM change
19:08:03 Running as SYSTEM
19:08:03 [EnvInject] - Loading node environment variables.
19:08:03 Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
19:08:03 [isabelle-all] $ hg showconfig paths.default
19:08:03 [isabelle-all] $ hg pull --rev default
19:08:04 pulling from https://isabelle.in.tum.de/repos/isabelle/
19:08:04 no changes found
19:08:04 [isabelle-all] $ hg update --clean --rev default
19:08:04 0 files updated, 0 files merged, 0 files removed, 0 files unresolved
19:08:04 [isabelle-all] $ hg log --rev . --template {node}
19:08:04 [isabelle-all] $ hg log --rev . --template {rev}
19:08:04 [isabelle-all] $ hg log --rev b8ce1269e1900d1d51c12f950b3566d8662d77bb --template exists\n
19:08:04 exists
19:08:04 [isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(b8ce1269e1900d1d51c12f950b3566d8662d77bb)" --encoding UTF-8 --encodingmode replace
19:08:04 [afp] $ hg showconfig paths.default
19:08:04 [afp] $ hg pull --rev default
19:08:05 pulling from https://foss.heptapod.net/isa-afp/afp-devel/
19:08:05 no changes found
19:08:05 [afp] $ hg update --clean --rev default
19:08:05 5 files updated, 0 files merged, 0 files removed, 0 files unresolved
19:08:05 [afp] $ hg --config extensions.purge= clean --all
19:08:06 [afp] $ hg log --rev . --template {node}
19:08:06 [afp] $ hg log --rev . --template {rev}
19:08:06 WARN: Revision data for previous build unavailable; unable to determine change log
19:08:06 No emails were triggered.
19:08:06 
[isabelle-all] $ /bin/sh -xe /tmp/jenkins3395857095276705004.sh

19:08:06 + Admin/jenkins/run_build all
19:08:06 + set -e
19:08:06 + PROFILE=all
19:08:06 + shift
19:08:06 + bin/isabelle components -a
19:08:06 + bin/isabelle jedit -bf
19:08:07 ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
19:09:19 ### Building Demo (/media/data/jenkins/workspace/isabelle-all/src/Tools/Demo/lib/demo.jar) ...
19:09:20 ### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
19:09:21 Hinweis: Einige Eingabedateien verwenden nicht geprüfte oder unsichere Vorgänge.
19:09:21 Hinweis: Wiederholen Sie die Kompilierung mit -Xlint:unchecked, um Details zu erhalten.
19:09:21 ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
19:09:21 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
19:09:25 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
19:09:29 + bin/isabelle ocaml_setup
19:09:29 # Run eval $(opam env) to update the current shell environment
19:09:30 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
19:09:30        opam update
19:09:30 
19:09:31 [NOTE] Package zarith is already installed (current version is 1.12).
19:09:31 + bin/isabelle ghc_setup
19:09:32 Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
19:09:32 consider using: stack ghc, stack ghci, stack runghc, or stack exec.
19:09:33 The Glorious Glasgow Haskell Compilation System, version 9.6.4
19:09:33 + bin/isabelle go_setup
19:09:35 Component directory "/media/data/jenkins/.isabelle/contrib/go-1.22.1"
19:09:35 ### Platform x86_64-linux already installed
19:09:35 + bin/isabelle ci_build all
19:09:38 
19:09:38 === CONFIGURATION ===
19:09:38 
19:09:38 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
19:09:38 ISABELLE_BUILD_OPTIONS=""
19:09:38 
19:09:38 ML_PLATFORM="x86_64_32-linux"
19:09:38 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64_32-linux"
19:09:38 ML_SYSTEM="polyml-5.9.1"
19:09:38 ML_OPTIONS="-H 4000 --maxheap 16G"
19:09:38 Cluster(cluster.default,true)
19:09:38 
19:09:38 === BUILD ===
19:09:38 
19:09:38 Build started at Mon, 10 Jun 2024 19:09:38 +0200
19:09:38 Isabelle id b8ce1269e190
19:09:38 AFP id 5944e7c4985b
19:09:39 
19:09:39 === LOG ===
19:09:39 
19:09:41 Session Pure/Pure
19:09:42 Session Misc/CTT
19:09:42 Session Misc/Cube
19:09:42 Session FOL/FOL
19:09:42 Session FOL/CCL
19:09:42 Session FOL/FOL-ex
19:09:42 Session FOL/FOLP
19:09:42 Session FOL/FOLP-ex
19:09:42 Session Doc/Intro (doc)
19:09:42 Session FOL/LCF
19:09:42 Session Doc/Logics (doc)
19:09:42 Session Doc/Nitpick (doc)
19:09:42 Session Pure/Pure-Examples
19:09:42 Session Pure/Pure-ex
19:09:42 Session Misc/SML
19:09:42 Session Misc/Sequents
19:09:42 Session Doc/Sledgehammer (doc)
19:09:43 Session AFP/SpecCheck (AFP)
19:09:43 Session Misc/Tools
19:09:43 Session HOL/HOL (main)
19:09:44 Session AFP/AVL-Trees (AFP)
19:09:44 Session AFP/AWN (AFP)
19:09:44 Session AFP/Abortable_Linearizable_Modules (AFP)
19:09:44 Session AFP/Abstract-Hoare-Logics (AFP)
19:09:44 Session AFP/Ackermanns_not_PR (AFP)
19:09:44 Session AFP/AnselmGod (AFP)
19:09:44 Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
19:09:44 Session AFP/Attack_Trees (AFP)
19:09:45 Session AFP/AxiomaticCategoryTheory (AFP)
19:09:45 Session AFP/Belief_Revision (AFP)
19:09:45 Session AFP/BinarySearchTree (AFP)
19:09:45 Session AFP/Binomial-Queues (AFP)
19:09:45 Session AFP/Bondy (AFP)
19:09:45 Session AFP/Boolos_Curious_Inference (AFP)
19:09:45 Session AFP/Boolos_Curious_Inference_Automated (AFP)
19:09:45 Session AFP/BytecodeLogicJmlTypes (AFP)
19:09:45 Session AFP/C2KA_DistributedSystems (AFP)
19:09:45 Session AFP/CISC-Kernel (AFP)
19:09:46 Session AFP/CYK (AFP)
19:09:46 Session AFP/Cauchy (AFP)
19:09:46 Session AFP/Sqrt_Babylonian (AFP)
19:09:46 Session Doc/Classes (doc)
19:09:46 Session AFP/ClockSynchInst (AFP)
19:09:46 Session AFP/Compiling-Exceptions-Correctly (AFP)
19:09:46 Session AFP/ComponentDependencies (AFP)
19:09:46 Session AFP/Concurrent_Revisions (AFP)
19:09:46 Session AFP/CondNormReasHOL (AFP)
19:09:46 Session AFP/Constructor_Funs (AFP)
19:09:46 Session AFP/CryptoBasedCompositionalProperties (AFP)
19:09:47 Session AFP/DCR-ExecutionEquivalence (AFP)
19:09:47 Session AFP/DPT-SAT-Solver (AFP)
19:09:47 Session AFP/Dedekind_Real (AFP)
19:09:47 Session Doc/Demo_EPTCS (doc)
19:09:47 Session Doc/Demo_Easychair (doc)
19:09:47 Session Doc/Demo_FoilTeX (doc)
19:09:47 Session Doc/Demo_LIPIcs (doc)
19:09:47 Session Doc/Demo_LLNCS (doc)
19:09:47 Session AFP/Depth-First-Search (AFP)
19:09:47 Session AFP/Digit_Expansions (AFP)
19:09:47 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
19:09:47 Session AFP/DiskPaxos (AFP)
19:09:47 Session AFP/Eudoxus_Reals (AFP)
19:09:47 Session AFP/Example-Submission (AFP)
19:09:47 Session AFP/FFT (AFP)
19:09:47 Session AFP/FLP (AFP)
19:09:47 Session AFP/FeatherweightJava (AFP)
19:09:47 Session AFP/Featherweight_OCL (AFP)
19:09:47 Session AFP/FileRefinement (AFP)
19:09:47 Session AFP/FocusStreamsCaseStudies (AFP)
19:09:47 Session AFP/Foundation_of_geometry (AFP)
19:09:47 Session AFP/Free-Boolean-Algebra (AFP)
19:09:47 Session AFP/Fresh_Identifiers (AFP)
19:09:47 Session AFP/FunWithFunctions (AFP)
19:09:47 Session AFP/FunWithTilings (AFP)
19:09:47 Session Doc/Functions (doc)
19:09:47 Session AFP/GPU_Kernel_PL (AFP)
19:09:47 Session AFP/GenClock (AFP)
19:09:47 Session AFP/General-Triangle (AFP)
19:09:47 Session AFP/Generic_Deriving (AFP)
19:09:47 Session AFP/GewirthPGCProof (AFP)
19:09:48 Session AFP/Go (AFP)
19:09:48 Session AFP/GoedelGod (AFP)
19:09:48 Session AFP/Goodstein_Lambda (AFP)
19:09:48 Session AFP/Gray_Codes (AFP)
19:09:48 Session HOL/HOL-Cardinals (timing)
19:09:48 Session AFP/Binding_Syntax_Theory (AFP)
19:09:48 Session AFP/Epistemic_Logic (AFP)
19:09:48 Session AFP/Public_Announcement_Logic (AFP)
19:09:48 Session AFP/Stalnaker_Logic (AFP)
19:09:48 Session AFP/Ordinals_and_Cardinals (AFP)
19:09:48 Session AFP/Risk_Free_Lending (AFP)
19:09:48 Session HOL/HOL-Hoare
19:09:48 Session HOL/HOL-Hoare_Parallel (timing)
19:09:48 Session HOL/HOL-IMPP
19:09:48 Session HOL/HOL-IOA
19:09:48 Session HOL/HOL-Import
19:09:48 Session HOL/HOL-Lattice
19:09:48 Session HOL/HOL-Library (main timing)
19:09:49 Session AFP/ADS_Functor (AFP)
19:09:49 Session AFP/Approximation_Algorithms (AFP)
19:09:49 Session AFP/ArrowImpossibilityGS (AFP)
19:09:49 Session AFP/Auto2_HOL (AFP)
19:09:49 Session AFP/BNF_CC (AFP)
19:09:49 Session AFP/BNF_Operations (AFP)
19:09:49 Session AFP/Binomial-Heaps (AFP)
19:09:49 Session AFP/Birkhoff_Finite_Distributive_Lattices (AFP)
19:09:49 Session AFP/Boolean_Expression_Checkers (AFP)
19:09:49 Session AFP/Bounded_Deducibility_Security (AFP)
19:09:50 Session AFP/BD_Security_Compositional (AFP)
19:09:50 Session AFP/CoSMeDis (AFP)
19:09:50 Session AFP/CoCon (AFP)
19:09:50 Session AFP/CoSMed (AFP)
19:09:50 Session AFP/Buildings (AFP)
19:09:50 Session AFP/CRDT (AFP)
19:09:50 Session AFP/IMAP-CRDT (AFP)
19:09:50 Session AFP/Card_Multisets (AFP)
19:09:50 Session AFP/Card_Number_Partitions (AFP)
19:09:50 Session AFP/Category (AFP)
19:09:50 Session Doc/Codegen (doc)
19:09:51 Session AFP/CofGroups (AFP)
19:09:51 Session AFP/CommCSL (AFP)
19:09:51 Session AFP/Complete_Non_Orders (AFP)
19:09:51 Session AFP/Completeness (AFP)
19:09:51 Session AFP/ConcurrentIMP (AFP)
19:09:51 Session AFP/Concurrent_Ref_Alg (AFP)
19:09:51 Session AFP/Conditional_Simplification (AFP)
19:09:51 Session AFP/Conditional_Transfer_Rule (AFP)
19:09:51 Session AFP/CoreC++ (AFP)
19:09:51 Session AFP/Core_DOM (AFP)
19:09:51 Session AFP/Shadow_DOM (AFP)
19:09:52 Session AFP/DOM_Components (AFP)
19:09:52 Session AFP/Core_SC_DOM (AFP)
19:09:52 Session AFP/Shadow_SC_DOM (AFP)
19:09:52 Session AFP/SC_DOM_Components (AFP)
19:09:52 Session AFP/Coupledsim_Contrasim (AFP)
19:09:52 Session Doc/Datatypes (doc)
19:09:53 Session Doc/Corec (doc)
19:09:53 Session AFP/Decl_Sem_Fun_PL (AFP)
19:09:53 Session AFP/Directed_Sets (AFP)
19:09:53 Session AFP/Earley_Parser (AFP)
19:09:53 Session AFP/Encodability_Process_Calculi (AFP)
19:09:53 Session AFP/Euler_Partition (AFP)
19:09:53 Session AFP/FOL-Fitting (AFP)
19:09:53 Session AFP/FOL_Seq_Calc1 (AFP)
19:09:53 Session AFP/FOL_Axiomatic (AFP)
19:09:53 Session AFP/FOL_Harrison (AFP)
19:09:53 Session AFP/Factored_Transition_System_Bounding (AFP)
19:09:53 Session AFP/FinFun (AFP)
19:09:54 Session AFP/Extended_Finite_State_Machines (AFP)
19:09:54 Session AFP/Extended_Finite_State_Machine_Inference (AFP)
19:09:54 Session AFP/Finger-Trees (AFP)
19:09:54 Session AFP/Finite-Map-Extras (AFP)
19:09:54 Session AFP/Fixed_Length_Vector (AFP)
19:09:54 Session AFP/Generalized_Counting_Sort (AFP)
19:09:54 Session AFP/Graph_Saturation (AFP)
19:09:54 Session AFP/Group-Ring-Module (AFP)
19:09:54 Session AFP/Valuation (AFP)
19:09:54 Session HOL/HOL-Auth (timing)
19:09:54 Session HOL/HOL-UNITY (timing)
19:09:55 Session HOL/HOL-Bali (timing)
19:09:55 Session HOL/HOL-Combinatorics (main timing)
19:09:55 Session AFP/Blue_Eyes (AFP)
19:09:55 Session AFP/Derangements (AFP)
19:09:55 Session AFP/Discrete_Summation (AFP)
19:09:55 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
19:09:55 Session AFP/Graph_Theory (AFP)
19:09:56 Session AFP/ShortestPath (AFP)
19:09:56 Session HOL/HOL-Computational_Algebra (main timing)
19:09:56 Session AFP/Descartes_Sign_Rule (AFP)
19:09:56 Session HOL/HOL-Algebra (main timing)
19:09:56 Session AFP/Edwards_Elliptic_Curves_Group (AFP)
19:09:56 Session AFP/Finitely_Generated_Abelian_Groups (AFP)
19:09:56 Session HOL/HOL-Decision_Procs (timing)
19:09:57 Session HOL/HOL-Quotient_Examples (timing)
19:09:57 Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
19:09:57 Session AFP/Localization_Ring (AFP)
19:09:57 Session AFP/Orbit_Stabiliser (AFP)
19:09:57 Session AFP/Perfect-Number-Thm (AFP)
19:09:57 Session AFP/Secondary_Sylow (AFP)
19:09:57 Session AFP/Jordan_Hoelder (AFP)
19:09:57 Session AFP/VectorSpace (AFP)
19:09:57 Session HOL/HOL-Examples
19:09:57 Session HOL/HOL-Isar_Examples
19:09:57 Session HOL/HOL-Nonstandard_Analysis (timing)
19:09:58 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
19:09:58 Session HOL/HOL-Number_Theory (main timing)
19:09:58 Session AFP/Arith_Prog_Rel_Primes (AFP)
19:09:58 Session AFP/DigitsInBase (AFP)
19:09:58 Session AFP/Elliptic_Curves_Group_Law (AFP)
19:09:58 Session AFP/Crypto_Standards (AFP)
19:09:58 Session AFP/Fermat3_4 (AFP)
19:09:58 Session HOL/HOL-Data_Structures (timing)
19:09:59 Session AFP/Efficient-Mergesort (AFP)
19:09:59 Session AFP/Go_Test_Quick (AFP)
19:09:59 Session AFP/Go_Test_Slow (AFP)
19:09:59 Session HOL/HOL-Codegenerator_Test
19:09:59 Session AFP/Query_Optimization (AFP)
19:09:59 Session HOL/HOL-ex (timing)
19:10:00 Session AFP/Lehmer (AFP)
19:10:00 Session AFP/Lifting_the_Exponent (AFP)
19:10:00 Session AFP/Padic_Ints (AFP)
19:10:00 Session AFP/Padic_Field (AFP)
19:10:00 Session AFP/Pratt_Certificate (AFP)
19:10:00 Session AFP/Bertrands_Postulate (AFP)
19:10:00 Session AFP/RSAPSS (AFP)
19:10:00 Session AFP/SumSquares (AFP)
19:10:00 Session AFP/Liouville_Numbers (AFP)
19:10:00 Session AFP/Lucas_Theorem (AFP)
19:10:00 Session AFP/DPRM_Theorem (AFP)
19:10:01 Session AFP/Mason_Stothers (AFP)
19:10:01 Session AFP/Polynomial_Interpolation (AFP)
19:10:01 Session AFP/Formal_Puiseux_Series (AFP)
19:10:01 Session AFP/Rep_Fin_Groups (AFP)
19:10:01 Session AFP/Sturm_Sequences (AFP)
19:10:01 Session AFP/Special_Function_Bounds (AFP)
19:10:01 Session AFP/Sturm_Tarski (AFP)
19:10:01 Session AFP/Budan_Fourier (AFP)
19:10:01 Session AFP/Three_Circles (AFP)
19:10:01 Session HOL/HOL-Corec_Examples (timing)
19:10:01 Session HOL/HOL-Datatype_Examples (timing)
19:10:01 Session HOL/HOL-IMP (timing)
19:10:01 Session AFP/Abs_Int_ITP2012 (AFP)
19:10:02 Session AFP/Relational-Incorrectness-Logic (AFP)
19:10:02 Session HOL/HOL-Imperative_HOL (timing)
19:10:02 Session AFP/Auto2_Imperative_HOL (AFP)
19:10:02 Session AFP/Imperative_Insertion_Sort (AFP)
19:10:02 Session HOL/HOL-Induct
19:10:02 Session HOL/HOL-Metis_Examples (timing)
19:10:02 Session HOL/HOL-Proofs (timing)
19:10:03 Session HOL/HOL-Proofs-Extraction (timing)
19:10:03 Session HOL/HOL-Proofs-ex
19:10:03 Session HOL/HOL-Proofs-Lambda (timing)
19:10:03 Session AFP/HereditarilyFinite (AFP)
19:10:03 Session AFP/HyperCTL (AFP)
19:10:03 Session AFP/IO_Language_Conformance (AFP)
19:10:03 Session AFP/Integration (AFP)
19:10:03 Session AFP/Isabelle_Meta_Model (AFP)
19:10:03 Session AFP/Isabelle_hoops (AFP)
19:10:03 Session AFP/LTL (AFP)
19:10:03 Session AFP/Stuttering_Equivalence (AFP)
19:10:04 Session AFP/Landau_Symbols (AFP)
19:10:04 Session AFP/LightweightJava (AFP)
19:10:04 Session AFP/LinearQuantifierElim (AFP)
19:10:04 Session AFP/List-Infinite (AFP)
19:10:04 Session AFP/Nat-Interval-Logic (AFP)
19:10:04 Session AFP/AutoFocus-Stream (AFP)
19:10:04 Session AFP/MuchAdoAboutTwo (AFP)
19:10:04 Session AFP/Order_Lattice_Props (AFP)
19:10:04 Session AFP/POPLmark-deBruijn (AFP)
19:10:04 Session AFP/Pairing_Heap (AFP)
19:10:04 Session AFP/Password_Authentication_Protocol (AFP)
19:10:04 Session AFP/Pell (AFP)
19:10:04 Session AFP/Prefix_Free_Code_Combinators (AFP)
19:10:04 Session AFP/Presburger-Automata (AFP)
19:10:04 Session AFP/Priority_Queue_Braun (AFP)
19:10:04 Session AFP/Program-Conflict-Analysis (AFP)
19:10:04 Session AFP/QBF_Solver_Verification (AFP)
19:10:04 Session AFP/Regular-Sets (AFP)
19:10:04 Session AFP/Abstract-Rewriting (AFP)
19:10:04 Session AFP/Decreasing-Diagrams (AFP)
19:10:04 Session AFP/Matrix (AFP)
19:10:05 Session AFP/Matrix_Tensor (AFP)
19:10:05 Session AFP/Knot_Theory (AFP)
19:10:05 Session AFP/Coinductive_Languages (AFP)
19:10:05 Session AFP/Finite_Automata_HF (AFP)
19:10:05 Session AFP/Functional-Automata (AFP)
19:10:05 Session AFP/Isabelle_DOF (AFP)
19:10:05 Session AFP/Posix-Lexing (AFP)
19:10:05 Session AFP/ResiduatedTransitionSystem (AFP)
19:10:05 Session AFP/Ribbon_Proofs (AFP)
19:10:05 Session AFP/SATSolverVerification (AFP)
19:10:05 Session AFP/Safe_OCL (AFP)
19:10:05 Session AFP/Schutz_Spacetime (AFP)
19:10:06 Session AFP/Selection_Heap_Sort (AFP)
19:10:06 Session AFP/Simplex (AFP)
19:10:06 Session AFP/Skew_Heap (AFP)
19:10:06 Session AFP/Sort_Encodings (AFP)
19:10:06 Session AFP/Splay_Tree (AFP)
19:10:06 Session AFP/Amortized_Complexity (AFP)
19:10:06 Session AFP/Dynamic_Tables (AFP)
19:10:06 Session AFP/Root_Balanced_Tree (AFP)
19:10:06 Session AFP/Stable_Matching (AFP)
19:10:06 Session AFP/SuperCalc (AFP)
19:10:06 Session Doc/System (doc)
19:10:07 Session AFP/Tail_Recursive_Functions (AFP)
19:10:07 Session AFP/TortoiseHare (AFP)
19:10:07 Session AFP/Trie (AFP)
19:10:07 Session AFP/Flyspeck-Tame (AFP)
19:10:07 Session AFP/Vickrey_Clarke_Groves (AFP)
19:10:07 Session AFP/Zeckendorf (AFP)
19:10:07 Session HOL/HOL-Matrix_LP
19:10:07 Session HOL/HOL-Mutabelle
19:10:07 Session HOL/HOL-NanoJava
19:10:07 Session HOL/HOL-Nitpick_Examples
19:10:07 Session HOL/HOL-Nominal
19:10:08 Session AFP/CCS (AFP)
19:10:08 Session HOL/HOL-Nominal-Examples (timing)
19:10:08 Session AFP/Lam-ml-Normalization (AFP)
19:10:08 Session AFP/Pi_Calculus (AFP)
19:10:08 Session AFP/Psi_Calculi (AFP)
19:10:09 Session AFP/Broadcast_Psi (AFP)
19:10:09 Session AFP/SequentInvertibility (AFP)
19:10:09 Session HOL/HOL-Predicate_Compile_Examples (timing)
19:10:09 Session HOL/HOL-Prolog
19:10:09 Session HOL/HOL-Quickcheck_Examples (timing)
19:10:10 Session HOL/HOL-Real_Asymp
19:10:10 Session HOL/HOL-Analysis (main timing)
19:10:11 Session AFP/Akra_Bazzi (AFP)
19:10:12 Session AFP/Closest_Pair_Points (AFP)
19:10:12 Session AFP/Cardinality_Continuum (AFP)
19:10:12 Session AFP/Catalan_Numbers (AFP)
19:10:12 Session AFP/Cayley_Hamilton (AFP)
19:10:12 Session AFP/Chebyshev_Polynomials (AFP)
19:10:12 Session AFP/Coinductive (AFP)
19:10:12 Session AFP/DynamicArchitectures (AFP)
19:10:12 Session AFP/Architectural_Design_Patterns (AFP)
19:10:12 Session AFP/Lazy-Lists-II (AFP)
19:10:12 Session AFP/Stream_Fusion_Code (AFP)
19:10:12 Session AFP/Topology (AFP)
19:10:12 Session AFP/Complex_Geometry (AFP)
19:10:12 Session AFP/Poincare_Disc (AFP)
19:10:13 Session AFP/Differential_Game_Logic (AFP)
19:10:13 Session AFP/Euler_Polyhedron_Formula (AFP)
19:10:13 Session AFP/First_Welfare_Theorem (AFP)
19:10:13 Session AFP/Furstenberg_Topology (AFP)
19:10:13 Session AFP/Green (AFP)
19:10:13 Session HOL/HOL-Analysis-ex
19:10:13 Session HOL/HOL-Complex_Analysis (main timing)
19:10:13 Session AFP/Bernoulli (AFP)
19:10:13 Session AFP/Cartan_FP (AFP)
19:10:13 Session AFP/Cotangent_PFD_Formula (AFP)
19:10:13 Session AFP/E_Transcendental (AFP)
19:10:14 Session AFP/Error_Function (AFP)
19:10:14 Session AFP/Euler_MacLaurin (AFP)
19:10:14 Session HOL/HOL-Eisbach
19:10:14 Session AFP/AOT (AFP)
19:10:14 Session AFP/Allen_Calculus (AFP)
19:10:14 Session AFP/Automatic_Refinement (AFP)
19:10:14 Session AFP/Refine_Monadic (AFP)
19:10:15 Session AFP/Card_Partitions (AFP)
19:10:15 Session AFP/Bell_Numbers_Spivey (AFP)
19:10:15 Session AFP/Card_Equiv_Relations (AFP)
19:10:15 Session AFP/Equivalence_Relation_Enumeration (AFP)
19:10:15 Session AFP/Falling_Factorial_Sum (AFP)
19:10:15 Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
19:10:15 Session AFP/Case_Labeling (AFP)
19:10:15 Session AFP/Clean (AFP)
19:10:15 Session AFP/Combinatorics_Words (AFP)
19:10:15 Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
19:10:15 Session AFP/Binary_Code_Imprimitive (AFP)
19:10:15 Session AFP/Two_Generated_Word_Monoids_Intersection (AFP)
19:10:15 Session AFP/Cook_Levin (AFP)
19:10:16 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
19:10:16 Session AFP/Dependent_SIFUM_Refinement (AFP)
19:10:16 Session Doc/Eisbach (doc)
19:10:16 Session HOL/HOL-MicroJava (timing)
19:10:16 Session AFP/Optics (AFP)
19:10:16 Session AFP/ConcurrentHOL (AFP)
19:10:16 Session AFP/UTP-Toolkit (AFP)
19:10:16 Session AFP/UTP (AFP)
19:10:16 Session AFP/Solidity (AFP)
19:10:17 Session AFP/Twelvefold_Way (AFP)
19:10:17 Session HOL/HOL-Hahn_Banach
19:10:17 Session HOL/HOL-Homology (timing)
19:10:17 Session HOL/HOL-Mirabelle-ex
19:10:17 Session HOL/HOL-Probability (main timing)
19:10:17 Session AFP/Actuarial_Mathematics (AFP)
19:10:17 Session AFP/Applicative_Lifting (AFP)
19:10:18 Session AFP/Free-Groups (AFP)
19:10:18 Session AFP/Stern_Brocot (AFP)
19:10:18 Session AFP/Buffons_Needle (AFP)
19:10:18 Session AFP/Density_Compiler (AFP)
19:10:18 Session AFP/DiscretePricing (AFP)
19:10:18 Session AFP/Ergodic_Theory (AFP)
19:10:18 Session AFP/Gromov_Hyperbolicity (AFP)
19:10:19 Session AFP/Laws_of_Large_Numbers (AFP)
19:10:19 Session AFP/Fisher_Yates (AFP)
19:10:19 Session AFP/Girth_Chromatic (AFP)
19:10:19 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
19:10:19 Session AFP/Szemeredi_Regularity (AFP)
19:10:19 Session HOL/HOL-Probability-ex (timing)
19:10:19 Session AFP/Hahn_Jordan_Decomposition (AFP)
19:10:19 Session AFP/Lp (AFP)
19:10:19 Session AFP/Concentration_Inequalities (AFP)
19:10:19 Session AFP/Fourier (AFP)
19:10:19 Session AFP/MDP-Rewards (AFP)
19:10:19 Session AFP/Markov_Models (AFP)
19:10:19 Session AFP/Martingales (AFP)
19:10:19 Session AFP/Doob_Convergence (AFP)
19:10:20 Session AFP/Monad_Normalisation (AFP)
19:10:20 Session AFP/Monomorphic_Monad (AFP)
19:10:20 Session AFP/Neumann_Morgenstern_Utility (AFP)
19:10:20 Session AFP/Probabilistic_Noninterference (AFP)
19:10:20 Session AFP/Probabilistic_Prime_Tests (AFP)
19:10:20 Session AFP/Probabilistic_System_Zoo (AFP)
19:10:20 Session AFP/Quasi_Borel_Spaces (AFP)
19:10:20 Session AFP/Roth_Arithmetic_Progressions (AFP)
19:10:20 Session AFP/Skip_Lists (AFP)
19:10:20 Session AFP/Source_Coding_Theorem (AFP)
19:10:20 Session AFP/Standard_Borel_Spaces (AFP)
19:10:21 Session AFP/S_Finite_Measure_Monad (AFP)
19:10:21 Session AFP/Disintegration (AFP)
19:10:21 Session AFP/Turans_Graph_Theorem (AFP)
19:10:21 Session AFP/Hyperdual (AFP)
19:10:21 Session AFP/Interval_Analysis (AFP)
19:10:21 Session AFP/Irrationality_J_Hancl (AFP)
19:10:21 Session AFP/Kuratowski_Closure_Complement (AFP)
19:10:21 Session AFP/Laplace_Transform (AFP)
19:10:21 Session AFP/Lower_Semicontinuous (AFP)
19:10:22 Session AFP/Minkowskis_Theorem (AFP)
19:10:22 Session AFP/Octonions (AFP)
19:10:22 Session AFP/Polynomial_Crit_Geometry (AFP)
19:10:22 Session AFP/Prime_Harmonic_Series (AFP)
19:10:22 Session AFP/Ptolemys_Theorem (AFP)
19:10:22 Session AFP/Quaternions (AFP)
19:10:22 Session AFP/Rank_Nullity_Theorem (AFP)
19:10:22 Session AFP/Gauss_Jordan (AFP)
19:10:22 Session AFP/Echelon_Form (AFP)
19:10:22 Session AFP/Hermite (AFP)
19:10:22 Session AFP/Safe_Distance (AFP)
19:10:22 Session AFP/Tarskis_Geometry (AFP)
19:10:22 Session AFP/Triangle (AFP)
19:10:22 Session AFP/Ceva (AFP)
19:10:23 Session AFP/Chord_Segments (AFP)
19:10:23 Session AFP/Stewart_Apollonius (AFP)
19:10:23 Session AFP/Winding_Number_Eval (AFP)
19:10:23 Session AFP/Count_Complex_Roots (AFP)
19:10:23 Session AFP/Youngs_Inequality (AFP)
19:10:23 Session AFP/pGCL (AFP)
19:10:23 Session HOL/HOL-Real_Asymp-Manual
19:10:23 Session AFP/Sophomores_Dream (AFP)
19:10:23 Session AFP/Stirling_Formula (AFP)
19:10:23 Session AFP/Irrationals_From_THEBOOK (AFP)
19:10:23 Session AFP/Lambert_W (AFP)
19:10:23 Session HOL/HOL-SET_Protocol (timing)
19:10:23 Session HOL/HOL-SMT_Examples (timing)
19:10:23 Session HOL/HOL-SPARK
19:10:24 Session HOL/HOL-SPARK-Examples
19:10:24 Session AFP/RIPEMD-160-SPARK (AFP)
19:10:24 Session HOL/HOL-SPARK-Manual
19:10:24 Session HOL/HOL-Statespace
19:10:24 Session HOL/HOL-TLA
19:10:24 Session HOL/HOL-TLA-Buffer
19:10:24 Session HOL/HOL-TLA-Inc
19:10:24 Session HOL/HOL-TLA-Memory
19:10:24 Session HOL/HOL-TPTP
19:10:24 Session HOL/HOL-Types_To_Sets
19:10:24 Session AFP/Banach_Steinhaus (AFP)
19:10:24 Session AFP/Smooth_Manifolds (AFP)
19:10:24 Session AFP/Types_To_Sets_Extension (AFP)
19:10:24 Session HOL/HOL-Unix
19:10:24 Session HOL/HOL-ZF
19:10:24 Session AFP/Category2 (AFP)
19:10:24 Session HOL/HOLCF (main timing)
19:10:25 Session AFP/Circus (AFP)
19:10:25 Session AFP/HOL-CSP (AFP)
19:10:25 Session AFP/HOL-CSPM (AFP)
19:10:25 Session AFP/HOL-CSP_OpSem (AFP)
19:10:25 Session HOL/HOLCF-IMP
19:10:25 Session HOL/HOLCF-Library
19:10:25 Session AFP/CSP_RefTK (AFP)
19:10:25 Session HOL/HOLCF-FOCUS
19:10:25 Session HOL/HOLCF-ex
19:10:25 Session AFP/PCF (AFP)
19:10:25 Session AFP/HOLCF-Prelude (AFP)
19:10:26 Session AFP/BirdKMP (AFP)
19:10:26 Session HOL/HOLCF-Tutorial
19:10:26 Session HOL/IOA (timing)
19:10:26 Session HOL/IOA-ABP
19:10:26 Session HOL/IOA-NTP
19:10:26 Session HOL/IOA-Storage
19:10:26 Session HOL/IOA-ex
19:10:26 Session AFP/Shivers-CFA (AFP)
19:10:26 Session AFP/Stream-Fusion (AFP)
19:10:26 Session AFP/Tycon (AFP)
19:10:26 Session AFP/WorkerWrapper (AFP)
19:10:26 Session AFP/Hales_Jewett (AFP)
19:10:26 Session Misc/Haskell
19:10:26 Session AFP/Heard_Of (AFP)
19:10:26 Session AFP/Consensus_Refined (AFP)
19:10:26 Session AFP/Hello_World (AFP)
19:10:26 Session AFP/HoareForDivergence (AFP)
19:10:26 Session AFP/Hood_Melville_Queue (AFP)
19:10:26 Session AFP/HotelKeyCards (AFP)
19:10:26 Session Doc/How_to_Prove_it (no_doc)
19:10:26 Session AFP/Huffman (AFP)
19:10:26 Session AFP/Hybrid_Logic (AFP)
19:10:27 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
19:10:27 Session AFP/HyperHoareLogic (AFP)
19:10:27 Session AFP/IFC_Tracking (AFP)
19:10:27 Session AFP/IMP2 (AFP)
19:10:27 Session AFP/IMP2_Binary_Heap (AFP)
19:10:27 Session AFP/IMP_Compiler (AFP)
19:10:27 Session AFP/IMP_Compiler_Reuse (AFP)
19:10:27 Session AFP/IMP_Noninterference (AFP)
19:10:27 Session Doc/Implementation (doc)
19:10:27 Session AFP/Implicational_Logic (AFP)
19:10:27 Session AFP/Impossible_Geometry (AFP)
19:10:27 Session AFP/Inductive_Confidentiality (AFP)
19:10:27 Session AFP/Inductive_Inference (AFP)
19:10:27 Session AFP/InfPathElimination (AFP)
19:10:27 Session AFP/Intro_Dest_Elim (AFP)
19:10:27 Session AFP/Involutions2Squares (AFP)
19:10:27 Session AFP/IsaGeoCoq (AFP)
19:10:28 Session AFP/IsaNet (AFP)
19:10:28 Session Doc/Isar_Ref (doc)
19:10:28 Session AFP/Isabelle_C (AFP)
19:10:28 Session Doc/JEdit (doc)
19:10:28 Session AFP/Jacobson_Basic_Algebra (AFP)
19:10:28 Session AFP/Grothendieck_Schemes (AFP)
19:10:28 Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
19:10:28 Session AFP/Khovanskii_Theorem (AFP)
19:10:28 Session AFP/Kneser_Cauchy_Davenport (AFP)
19:10:28 Session AFP/JiveDataStoreModel (AFP)
19:10:28 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
19:10:29 Session AFP/Kleene_Algebra (AFP)
19:10:29 Session AFP/KAD (AFP)
19:10:29 Session AFP/KAT_and_DRA (AFP)
19:10:29 Session AFP/Algebraic_VCs (AFP)
19:10:29 Session AFP/Multirelations (AFP)
19:10:29 Session AFP/Quantales (AFP)
19:10:29 Session AFP/Transformer_Semantics (AFP)
19:10:29 Session AFP/Regular_Algebras (AFP)
19:10:29 Session AFP/Relation_Algebra (AFP)
19:10:29 Session AFP/Relational_Paths (AFP)
19:10:29 Session AFP/Residuated_Lattices (AFP)
19:10:29 Session AFP/Knights_Tour (AFP)
19:10:29 Session AFP/LambdaMu (AFP)
19:10:29 Session AFP/LatticeProperties (AFP)
19:10:29 Session AFP/DataRefinementIBP (AFP)
19:10:29 Session AFP/GraphMarkingIBP (AFP)
19:10:29 Session AFP/Lazy_Case (AFP)
19:10:29 Session AFP/Lifting_Definition_Option (AFP)
19:10:29 Session AFP/List-Index (AFP)
19:10:29 Session AFP/Comparison_Sort_Lower_Bound (AFP)
19:10:29 Session AFP/Jinja (AFP)
19:10:30 Session AFP/Dominance_CHK (AFP)
19:10:30 Session AFP/HRB-Slicing (AFP)
19:10:30 Session AFP/InformationFlowSlicing_Inter (AFP)
19:10:30 Session AFP/Slicing (AFP)
19:10:30 Session AFP/InformationFlowSlicing (AFP)
19:10:30 Session AFP/JinjaDCI (AFP)
19:10:30 Session AFP/Regression_Test_Selection (AFP)
19:10:31 Session AFP/List_Update (AFP)
19:10:31 Session AFP/Quick_Sort_Cost (AFP)
19:10:31 Session AFP/Random_BSTs (AFP)
19:10:31 Session AFP/Randomised_BSTs (AFP)
19:10:31 Session AFP/Treaps (AFP)
19:10:31 Session AFP/Randomised_Social_Choice (AFP)
19:10:31 Session AFP/Fishburn_Impossibility (AFP)
19:10:31 Session AFP/PAPP_Impossibility (AFP)
19:10:31 Session AFP/SDS_Impossibility (AFP)
19:10:31 Session AFP/List_Interleaving (AFP)
19:10:31 Session AFP/List_Inversions (AFP)
19:10:32 Session AFP/LocalLexing (AFP)
19:10:32 Session Doc/Locales (doc)
19:10:32 Session AFP/Locally-Nameless-Sigma (AFP)
19:10:32 Session AFP/Logging_Independent_Anonymity (AFP)
19:10:32 Session AFP/Lowe_Ontological_Argument (AFP)
19:10:32 Session AFP/MHComputation (AFP)
19:10:32 Session AFP/MLSS_Decision_Proc (AFP)
19:10:32 Session AFP/ML_Unification (AFP)
19:10:32 Session Doc/Main (doc)
19:10:32 Session AFP/Marriage (AFP)
19:10:32 Session AFP/Latin_Square (AFP)
19:10:32 Session AFP/Matroids (AFP)
19:10:32 Session AFP/Max-Card-Matching (AFP)
19:10:32 Session AFP/Maximum_Segment_Sum (AFP)
19:10:32 Session AFP/Median_Of_Medians_Selection (AFP)
19:10:33 Session AFP/KD_Tree (AFP)
19:10:33 Session AFP/Menger (AFP)
19:10:33 Session AFP/Mereology (AFP)
19:10:33 Session AFP/Metalogic_ProofChecker (AFP)
19:10:33 Session AFP/MiniML (AFP)
19:10:33 Session AFP/Modular_Assembly_Kit_Security (AFP)
19:10:33 Session AFP/MonoBoolTranAlgebra (AFP)
19:10:33 Session AFP/Multirelations_Heterogeneous (AFP)
19:10:33 Session AFP/Multitape_To_Singletape_TM (AFP)
19:10:33 Session AFP/Name_Carrying_Type_Inference (AFP)
19:10:33 Session AFP/Nano_JSON (AFP)
19:10:33 Session AFP/Nash_Williams (AFP)
19:10:33 Session AFP/No_FTL_observers (AFP)
19:10:33 Session AFP/No_FTL_observers_Gen_Rel (AFP)
19:10:33 Session AFP/Nominal2 (AFP)
19:10:34 Session AFP/Incompleteness (AFP)
19:10:34 Session AFP/Surprise_Paradox (AFP)
19:10:34 Session AFP/LambdaAuth (AFP)
19:10:34 Session AFP/Launchbury (AFP)
19:10:34 Session AFP/Call_Arity (AFP)
19:10:34 Session AFP/Modal_Logics_for_NTS (AFP)
19:10:34 Session AFP/Rewriting_Z (AFP)
19:10:34 Session AFP/Nominal_Myhill_Nerode (AFP)
19:10:35 Session AFP/Noninterference_CSP (AFP)
19:10:35 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
19:10:35 Session AFP/Noninterference_Generic_Unwinding (AFP)
19:10:35 Session AFP/Noninterference_Inductive_Unwinding (AFP)
19:10:35 Session AFP/Noninterference_Sequential_Composition (AFP)
19:10:35 Session AFP/Noninterference_Concurrent_Composition (AFP)
19:10:35 Session AFP/NormByEval (AFP)
19:10:35 Session AFP/OpSets (AFP)
19:10:35 Session AFP/Open_Induction (AFP)
19:10:35 Session AFP/Well_Quasi_Orders (AFP)
19:10:35 Session AFP/Decreasing-Diagrams-II (AFP)
19:10:35 Session AFP/Myhill-Nerode (AFP)
19:10:35 Session AFP/Ordinal (AFP)
19:10:35 Session AFP/Nested_Multisets_Ordinals (AFP)
19:10:35 Session AFP/Design_Theory (AFP)
19:10:35 Session AFP/Lovasz_Local (AFP)
19:10:36 Session AFP/Undirected_Graph_Theory (AFP)
19:10:36 Session AFP/Balog_Szemeredi_Gowers (AFP)
19:10:36 Session AFP/Lambda_Free_RPOs (AFP)
19:10:36 Session AFP/Lambda_Free_EPO (AFP)
19:10:36 Session AFP/Substitutions_Lambda_Free (AFP)
19:10:36 Session AFP/Ordered_Resolution_Prover (AFP)
19:10:36 Session AFP/Chandy_Lamport (AFP)
19:10:36 Session AFP/Saturation_Framework (AFP)
19:10:36 Session AFP/Progress_Tracking (AFP)
19:10:36 Session AFP/PAL (AFP)
19:10:36 Session AFP/PLM (AFP)
19:10:36 Session AFP/PSemigroupsConvolution (AFP)
19:10:36 Session AFP/Package_logic (AFP)
19:10:37 Session AFP/Combinable_Wands (AFP)
19:10:37 Session AFP/Paraconsistency (AFP)
19:10:37 Session AFP/Parity_Game (AFP)
19:10:37 Session AFP/GaleStewart_Games (AFP)
19:10:37 Session AFP/Partial_Function_MR (AFP)
19:10:37 Session AFP/Physical_Quantities (AFP)
19:10:37 Session AFP/Pop_Refinement (AFP)
19:10:37 Session AFP/Possibilistic_Noninterference (AFP)
19:10:37 Session AFP/Priority_Search_Trees (AFP)
19:10:37 Session AFP/Prim_Dijkstra_Simple (AFP)
19:10:37 Session Doc/Prog_Prove (doc)
19:10:37 Session AFP/Projective_Geometry (AFP)
19:10:37 Session AFP/Proof_Strategy_Language (AFP)
19:10:38 Session AFP/PropResPI (AFP)
19:10:38 Session AFP/Propositional_Logic_Class (AFP)
19:10:38 Session AFP/Propositional_Proof_Systems (AFP)
19:10:38 Session AFP/PseudoHoops (AFP)
19:10:38 Session AFP/Quantales_Converse (AFP)
19:10:38 Session AFP/Catoids (AFP)
19:10:38 Session AFP/CubicalCategories (AFP)
19:10:38 Session AFP/OmegaCatoidsQuantales (AFP)
19:10:38 Session AFP/Ramsey-Infinite (AFP)
19:10:38 Session AFP/Real_Power (AFP)
19:10:38 Session AFP/Real_Time_Deque (AFP)
19:10:38 Session AFP/Recursion-Theory-I (AFP)
19:10:39 Session AFP/Minsky_Machines (AFP)
19:10:39 Session AFP/RefinementReactive (AFP)
19:10:39 Session AFP/Regex_Equivalence (AFP)
19:10:39 Session AFP/Region_Quadtrees (AFP)
19:10:39 Session AFP/Relational_Method (AFP)
19:10:39 Session AFP/Rensets (AFP)
19:10:39 Session AFP/Robbins-Conjecture (AFP)
19:10:39 Session AFP/Roy_Floyd_Warshall (AFP)
19:10:39 Session AFP/SCC_Bloemen_Sequential (AFP)
19:10:39 Session AFP/SIFPL (AFP)
19:10:39 Session AFP/SIFUM_Type_Systems (AFP)
19:10:39 Session AFP/Sauer_Shelah_Lemma (AFP)
19:10:39 Session AFP/Security_Protocol_Refinement (AFP)
19:10:39 Session AFP/SenSocialChoice (AFP)
19:10:39 Session AFP/Separation_Algebra (AFP)
19:10:40 Session AFP/Hoare_Time (AFP)
19:10:40 Session AFP/Separata (AFP)
19:10:40 Session AFP/Separation_Logic_Unbounded (AFP)
19:10:40 Session AFP/Simpl (AFP)
19:10:40 Session AFP/BDD (AFP)
19:10:40 Session AFP/SimplifiedOntologicalArgument (AFP)
19:10:40 Session AFP/Sliding_Window_Algorithm (AFP)
19:10:40 Session AFP/Statecharts (AFP)
19:10:40 Session AFP/Stellar_Quorums (AFP)
19:10:40 Session AFP/Stone_Algebras (AFP)
19:10:40 Session AFP/Stone_Relation_Algebras (AFP)
19:10:40 Session AFP/Relational_Cardinality (AFP)
19:10:41 Session AFP/Stone_Kleene_Relation_Algebras (AFP)
19:10:41 Session AFP/Aggregation_Algebras (AFP)
19:10:41 Session AFP/Relational_Disjoint_Set_Forests (AFP)
19:10:41 Session AFP/Relational_Minimum_Spanning_Trees (AFP)
19:10:41 Session AFP/Relational_Forests (AFP)
19:10:41 Session AFP/Subset_Boolean_Algebras (AFP)
19:10:41 Session AFP/Correctness_Algebras (AFP)
19:10:41 Session AFP/Store_Buffer_Reduction (AFP)
19:10:41 Session AFP/StrictOmegaCategories (AFP)
19:10:41 Session AFP/Strong_Security (AFP)
19:10:41 Session Doc/Sugar (doc)
19:10:41 Session AFP/Sunflowers (AFP)
19:10:41 Session AFP/Clique_and_Monotone_Circuits (AFP)
19:10:41 Session AFP/Suppes_Theorem (AFP)
19:10:42 Session AFP/Probability_Inequality_Completeness (AFP)
19:10:42 Session AFP/Syntax_Independent_Logic (AFP)
19:10:42 Session AFP/Goedel_Incompleteness (AFP)
19:10:42 Session AFP/Goedel_HFSet_Semantic (AFP)
19:10:42 Session AFP/Goedel_HFSet_Semanticless (AFP)
19:10:43 Session AFP/Robinson_Arithmetic (AFP)
19:10:43 Session AFP/Synthetic_Completeness (AFP)
19:10:43 Session AFP/Szpilrajn (AFP)
19:10:43 Session AFP/Combinatorics_Words_Lyndon (AFP)
19:10:43 Session AFP/TESL_Language (AFP)
19:10:43 Session AFP/TLA (AFP)
19:10:43 Session AFP/Timed_Automata (AFP)
19:10:43 Session AFP/Probabilistic_Timed_Automata (AFP)
19:10:43 Session AFP/Top_Down_Solver (AFP)
19:10:43 Session AFP/Topological_Semantics (AFP)
19:10:43 Session AFP/Transitive-Closure-II (AFP)
19:10:43 Session AFP/Transport (AFP)
19:10:44 Session AFP/Tree_Decomposition (AFP)
19:10:44 Session AFP/Tree_Enumeration (AFP)
19:10:44 Session Doc/Tutorial (doc)
19:10:44 Session Doc/Typeclass_Hierarchy (doc)
19:10:44 Session AFP/Types_Tableaus_and_Goedels_God (AFP)
19:10:45 Session AFP/UPF (AFP)
19:10:45 Session AFP/UPF_Firewall (AFP)
19:10:45 Session AFP/Universal_Turing_Machine (AFP)
19:10:45 Session AFP/Van_der_Waerden (AFP)
19:10:45 Session AFP/VeriComp (AFP)
19:10:45 Session AFP/Interpreter_Optimizations (AFP)
19:10:45 Session AFP/Verified-Prover (AFP)
19:10:45 Session AFP/VolpanoSmith (AFP)
19:10:45 Session AFP/WHATandWHERE_Security (AFP)
19:10:45 Session AFP/Weight_Balanced_Trees (AFP)
19:10:45 Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
19:10:45 Session AFP/Word_Lib (AFP)
19:10:45 Session AFP/AutoCorres2 (AFP)
19:10:46 Session AFP/AutoCorres2_Main (AFP)
19:10:47 Session AFP/AutoCorres2_Test (AFP)
19:10:47 Session AFP/Complx (AFP)
19:10:47 Session AFP/IEEE_Floating_Point (AFP)
19:10:47 Session AFP/IP_Addresses (AFP)
19:10:48 Session AFP/Simple_Firewall (AFP)
19:10:48 Session AFP/Routing (AFP)
19:10:48 Session AFP/Interval_Arithmetic_Word32 (AFP)
19:10:48 Session AFP/LEM (AFP)
19:10:48 Session AFP/Native_Word (AFP)
19:10:49 Session AFP/Collections (AFP)
19:10:49 Session AFP/Abstract_Completeness (AFP)
19:10:49 Session AFP/Abstract_Soundness (AFP)
19:10:49 Session AFP/FOL_Seq_Calc3 (AFP)
19:10:49 Session AFP/Incredible_Proof_Machine (AFP)
19:10:49 Session AFP/Deriving (AFP)
19:10:49 Session AFP/CAVA_Base (AFP)
19:10:49 Session AFP/CAVA_Automata (AFP)
19:10:49 Session AFP/DFS_Framework (AFP)
19:10:49 Session AFP/Gabow_SCC (AFP)
19:10:49 Session AFP/LTL_to_GBA (AFP)
19:10:49 Session AFP/Promela (AFP)
19:10:50 Session AFP/Containers (AFP)
19:10:50 Session AFP/CHERI-C_Memory_Model (AFP)
19:10:50 Session AFP/Collections_Examples (AFP)
19:10:50 Session AFP/Containers-Benchmarks (AFP)
19:10:50 Session AFP/Eval_FO (AFP)
19:10:50 Session AFP/MFOTL_Monitor (AFP)
19:10:50 Session AFP/Generic_Join (AFP)
19:10:51 Session AFP/MFODL_Monitor_Optimized (AFP)
19:10:51 Session AFP/MFOTL_Checker (AFP)
19:10:51 Session AFP/VYDRA_MDL (AFP)
19:10:51 Session AFP/Formula_Derivatives (AFP)
19:10:51 Session AFP/Labeled_Transition_Systems (AFP)
19:10:51 Session AFP/Pushdown_Systems (AFP)
19:10:51 Session AFP/MSO_Regex_Equivalence (AFP)
19:10:51 Session AFP/Show (AFP)
19:10:52 Session AFP/Affine_Arithmetic (AFP)
19:10:52 Session AFP/Ordinary_Differential_Equations (AFP)
19:10:52 Session AFP/Differential_Dynamic_Logic (AFP)
19:10:52 Session AFP/Hybrid_Systems_VCs (AFP)
19:10:52 Session AFP/Matrices_for_ODEs (AFP)
19:10:53 Session AFP/Taylor_Models (AFP)
19:10:53 Session AFP/CakeML (AFP)
19:10:53 Session AFP/Certification_Monads (AFP)
19:10:53 Session AFP/AI_Planning_Languages_Semantics (AFP)
19:10:53 Session AFP/Verified_SAT_Based_AI_Planning (AFP)
19:10:53 Session AFP/Dict_Construction (AFP)
19:10:53 Session AFP/Formula_Derivatives-Examples (AFP)
19:10:53 Session AFP/LL1_Parser (AFP)
19:10:54 Session AFP/Monad_Memo_DP (AFP)
19:10:54 Session AFP/Hidden_Markov_Models (AFP)
19:10:54 Session AFP/Optimal_BST (AFP)
19:10:54 Session AFP/Polynomial_Factorization (AFP)
19:10:54 Session AFP/Amicable_Numbers (AFP)
19:10:54 Session AFP/Continued_Fractions (AFP)
19:10:54 Session AFP/Dirichlet_Series (AFP)
19:10:55 Session AFP/Zeta_Function (AFP)
19:10:55 Session AFP/Dirichlet_L (AFP)
19:10:55 Session AFP/Gauss_Sums (AFP)
19:10:55 Session AFP/Three_Squares (AFP)
19:10:56 Session AFP/Polygonal_Number_Theorem (AFP)
19:10:56 Session AFP/Wieferich_Kempner (AFP)
19:10:56 Session AFP/Kummer_Congruence (AFP)
19:10:56 Session AFP/Prime_Number_Theorem (AFP)
19:10:56 Session AFP/PNT_with_Remainder (AFP)
19:10:56 Session AFP/Prime_Distribution_Elementary (AFP)
19:10:56 Session AFP/IMO2019 (AFP)
19:10:56 Session AFP/Irrational_Series_Erdos_Straus (AFP)
19:10:56 Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
19:10:56 Session AFP/Zeta_3_Irrational (AFP)
19:10:56 Session AFP/First_Order_Terms (AFP)
19:10:57 Session AFP/Resolution_FOL (AFP)
19:10:57 Session AFP/Saturation_Framework_Extensions (AFP)
19:10:57 Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
19:10:57 Session AFP/Automated_Stateful_Protocol_Verification (AFP)
19:10:57 Session AFP/Gaussian_Integers (AFP)
19:10:57 Session AFP/Jordan_Normal_Form (AFP)
19:10:58 Session AFP/Farkas (AFP)
19:10:58 Session AFP/Isabelle_Marries_Dirac (AFP)
19:10:58 Session AFP/Knuth_Bendix_Order (AFP)
19:10:58 Session AFP/Functional_Ordered_Resolution_Prover (AFP)
19:10:58 Session AFP/Simple_Clause_Learning (AFP)
19:10:58 Session AFP/Regular_Tree_Relations (AFP)
19:10:59 Session AFP/FO_Theory_Rewriting (AFP)
19:10:59 Session AFP/Rewrite_Properties_Reduction (AFP)
19:10:59 Session AFP/Weighted_Path_Order (AFP)
19:10:59 Session AFP/Efficient_Weighted_Path_Order (AFP)
19:10:59 Session AFP/Given_Clause_Loops (AFP)
19:10:59 Session AFP/Multiset_Ordering_NPC (AFP)
19:10:59 Session AFP/Linear_Recurrences (AFP)
19:10:59 Session AFP/Polylog (AFP)
19:10:59 Session AFP/Lambert_Series (AFP)
19:10:59 Session AFP/Perron_Frobenius (AFP)
19:11:00 Session AFP/MDP-Algorithms (AFP)
19:11:01 Session AFP/Stochastic_Matrices (AFP)
19:11:01 Session AFP/Subresultants (AFP)
19:11:01 Session AFP/Berlekamp_Zassenhaus (AFP)
19:11:01 Session AFP/Algebraic_Numbers (AFP)
19:11:01 Session AFP/BenOr_Kozen_Reif (AFP)
19:11:01 Session AFP/LLL_Basis_Reduction (AFP)
19:11:01 Session AFP/CVP_Hardness (AFP)
19:11:02 Session AFP/LLL_Factorization (AFP)
19:11:02 Session AFP/Linear_Inequalities (AFP)
19:11:02 Session AFP/LP_Duality (AFP)
19:11:02 Session AFP/Linear_Programming (AFP)
19:11:02 Session AFP/Number_Theoretic_Transform (AFP)
19:11:02 Session AFP/CRYSTALS-Kyber (AFP)
19:11:02 Session AFP/Perfect_Fields (AFP)
19:11:02 Session AFP/Elimination_Of_Repeated_Factors (AFP)
19:11:02 Session AFP/Smith_Normal_Form (AFP)
19:11:02 Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
19:11:03 Session AFP/Polynomials (AFP)
19:11:03 Session AFP/Deep_Learning (AFP)
19:11:04 Session AFP/QHLProver (AFP)
19:11:04 Session AFP/Projective_Measurements (AFP)
19:11:04 Session AFP/Commuting_Hermitian (AFP)
19:11:04 Session AFP/TsirelsonBound (AFP)
19:11:04 Session AFP/Uncertainty_Principle (AFP)
19:11:04 Session AFP/Groebner_Bases (AFP)
19:11:05 Session AFP/Fishers_Inequality (AFP)
19:11:05 Session AFP/Hypergraph_Basics (AFP)
19:11:05 Session AFP/Hypergraph_Colourings (AFP)
19:11:05 Session AFP/Groebner_Macaulay (AFP)
19:11:05 Session AFP/Nullstellensatz (AFP)
19:11:05 Session AFP/Signature_Groebner (AFP)
19:11:05 Session AFP/Lambda_Free_KBOs (AFP)
19:11:06 Session AFP/Sumcheck_Protocol (AFP)
19:11:06 Session AFP/Symmetric_Polynomials (AFP)
19:11:06 Session AFP/Pi_Transcendental (AFP)
19:11:06 Session AFP/Power_Sum_Polynomials (AFP)
19:11:06 Session AFP/Hermite_Lindemann (AFP)
19:11:06 Session AFP/Factor_Algebraic_Polynomial (AFP)
19:11:06 Session AFP/Cubic_Quartic_Equations (AFP)
19:11:06 Session AFP/Linear_Recurrences_Solver (AFP)
19:11:07 Session AFP/Orient_Rewrite_Rule_Undecidable (AFP)
19:11:07 Session AFP/Schwartz_Zippel (AFP)
19:11:07 Session AFP/Virtual_Substitution (AFP)
19:11:07 Session AFP/Real_Impl (AFP)
19:11:08 Session AFP/Complex_Bounded_Operators_Dependencies (AFP)
19:11:08 Session AFP/Complex_Bounded_Operators (AFP)
19:11:08 Session AFP/Registers (AFP)
19:11:08 Session AFP/QR_Decomposition (AFP)
19:11:09 Session AFP/XML (AFP)
19:11:09 Session AFP/Van_Emde_Boas_Trees (AFP)
19:11:09 Session AFP/Dijkstra_Shortest_Path (AFP)
19:11:09 Session AFP/Koenigsberg_Friendship (AFP)
19:11:09 Session AFP/FOL_Seq_Calc2 (AFP)
19:11:09 Session AFP/Formal_SSA (AFP)
19:11:09 Session AFP/Minimal_SSA (AFP)
19:11:10 Session AFP/Gale_Shapley (AFP)
19:11:10 Session AFP/HOL-ODE-Numerics (AFP)
19:11:10 Session AFP/HOL-ODE-ARCH-COMP (AFP)
19:11:10 Session AFP/HOL-ODE-Examples (AFP large)
19:11:10 Session AFP/Lorenz_Approximation (AFP)
19:11:11 Session AFP/Lorenz_C0 (AFP large)
19:11:11 Session AFP/Lorenz_C1 (AFP large)
19:11:11 Session AFP/Poincare_Bendixson (AFP)
19:11:11 Session AFP/Picks_Theorem (AFP)
19:11:11 Session AFP/KnuthMorrisPratt (AFP)
19:11:11 Session AFP/Safe_Range_RC (AFP)
19:11:11 Session AFP/Transition_Systems_and_Automata (AFP)
19:11:11 Session AFP/Adaptive_State_Counting (AFP)
19:11:11 Session AFP/Buchi_Complementation (AFP)
19:11:11 Session AFP/LTL_Master_Theorem (AFP)
19:11:11 Session AFP/LTL_Normal_Form (AFP)
19:11:12 Session AFP/Partial_Order_Reduction (AFP)
19:11:12 Session AFP/SM_Base (AFP)
19:11:12 Session AFP/SM (AFP)
19:11:12 Session AFP/CAVA_Setup (AFP)
19:11:12 Session AFP/CAVA_LTL_Modelchecker (AFP)
19:11:12 Session AFP/Transitive-Closure (AFP)
19:11:12 Session AFP/KBPs (AFP)
19:11:12 Session AFP/LTL_to_DRA (AFP)
19:11:12 Session AFP/Network_Security_Policy_Verification (AFP)
19:11:13 Session AFP/Planarity_Certificates (AFP)
19:11:13 Session AFP/Tree-Automata (AFP)
19:11:13 Session AFP/Datatype_Order_Generator (AFP)
19:11:13 Session AFP/Higher_Order_Terms (AFP)
19:11:13 Session AFP/CakeML_Codegen (AFP)
19:11:14 Session AFP/Old_Datatype_Show (AFP)
19:11:14 Session AFP/Quantifier_Elimination_Hybrid (AFP)
19:11:14 Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
19:11:14 Session AFP/FSM_Tests (AFP)
19:11:15 Session AFP/Iptables_Semantics (AFP)
19:11:15 Session AFP/Iptables_Semantics_Examples (AFP)
19:11:15 Session AFP/LOFT (AFP)
19:11:15 Session AFP/Mersenne_Primes (AFP)
19:11:15 Session AFP/MiniSail (AFP)
19:11:15 Session AFP/Separation_Logic_Imperative_HOL (AFP)
19:11:16 Session AFP/Sepref_Prereq (AFP)
19:11:16 Session AFP/ROBDD (AFP)
19:11:16 Session AFP/Refine_Imperative_HOL (AFP)
19:11:16 Session AFP/BTree (AFP)
19:11:16 Session AFP/Floyd_Warshall (AFP)
19:11:16 Session AFP/Sepref_Basic (AFP)
19:11:16 Session AFP/Sepref_IICF (AFP)
19:11:16 Session AFP/Flow_Networks (AFP)
19:11:16 Session AFP/EdmondsKarp_Maxflow (AFP)
19:11:16 Session AFP/MFMC_Countable (AFP)
19:11:17 Session AFP/Probabilistic_While (AFP)
19:11:17 Session AFP/CryptHOL (AFP)
19:11:17 Session AFP/ABY3_Protocols (AFP)
19:11:17 Session AFP/Constructive_Cryptography (AFP)
19:11:17 Session AFP/Game_Based_Crypto (AFP)
19:11:17 Session AFP/CRYSTALS-Kyber_Security (AFP)
19:11:17 Session AFP/Multi_Party_Computation (AFP)
19:11:18 Session AFP/Sigma_Commit_Crypto (AFP)
19:11:18 Session AFP/Constructive_Cryptography_CM (AFP)
19:11:18 Session AFP/Executable_Randomized_Algorithms (AFP)
19:11:18 Session AFP/Finite_Fields (AFP)
19:11:20 Session AFP/Universal_Hash_Families (AFP)
19:11:21 Session AFP/Expander_Graphs (AFP)
19:11:21 Session AFP/Karatsuba (AFP)
19:11:22 Session AFP/Median_Method (AFP)
19:11:22 Session AFP/Frequency_Moments (AFP)
19:11:23 Session AFP/Approximate_Model_Counting (AFP)
19:11:23 Session AFP/Distributed_Distinct_Elements (AFP)
19:11:23 Session AFP/Derandomization_Conditional_Expectations (AFP)
19:11:23 Session AFP/Prpu_Maxflow (AFP)
19:11:23 Session AFP/Knuth_Morris_Pratt (AFP)
19:11:23 Session AFP/Kruskal (AFP)
19:11:24 Session AFP/PAC_Checker (AFP)
19:11:24 Session AFP/VerifyThis2018 (AFP)
19:11:24 Session AFP/VerifyThis2019 (AFP)
19:11:24 Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
19:11:24 Session AFP/UpDown_Scheme (AFP)
19:11:24 Session AFP/WebAssembly (AFP)
19:11:24 Session AFP/SPARCv8 (AFP)
19:11:25 Session AFP/Schoenhage_Strassen (AFP)
19:11:25 Session AFP/X86_Semantics (AFP)
19:11:25 Session AFP/ZFC_in_HOL (AFP)
19:11:26 Session AFP/CZH_Foundations (AFP)
19:11:26 Session AFP/CZH_Elementary_Categories (AFP)
19:11:26 Session AFP/CZH_Universal_Constructions (AFP)
19:11:26 Session AFP/Category3 (AFP)
19:11:26 Session AFP/MonoidalCategory (AFP)
19:11:27 Session AFP/Ordinal_Partitions (AFP)
19:11:27 Session AFP/Q0_Metatheory (AFP)
19:11:27 Session AFP/Q0_Soundness (AFP)
19:11:27 Session AFP/Wetzels_Problem (AFP)
19:11:27 Session FOL/ZF (main timing)
19:11:27 Session Doc/Logics_ZF (doc)
19:11:27 Session AFP/Recursion-Addition (AFP)
19:11:27 Session FOL/ZF-AC
19:11:27 Session FOL/ZF-Coind
19:11:27 Session FOL/ZF-Constructible
19:11:27 Session AFP/Delta_System_Lemma (AFP)
19:11:27 Session AFP/Transitive_Models (AFP)
19:11:28 Session AFP/Independence_CH (AFP)
19:11:28 Session AFP/Forcing (AFP)
19:11:28 Session FOL/ZF-IMP
19:11:28 Session FOL/ZF-Induct
19:11:28 Session FOL/ZF-UNITY (timing)
19:11:28 Session FOL/ZF-Resid
19:11:28 Session FOL/ZF-ex
19:11:54 Building HOL (on hpcisabelle/1) ...
19:11:57 HOL: theory Tools.Code_Generator
19:12:02 HOL: theory HOL.HOL
19:12:08 HOL: theory HOL.Argo
19:12:08 HOL: theory HOL.Ctr_Sugar
19:12:08 HOL: theory HOL.Orderings
19:12:13 HOL: theory HOL.Groups
19:12:14 HOL: theory HOL.SAT
19:12:15 HOL: theory HOL.Lattices
19:12:17 HOL: theory HOL.Boolean_Algebras
19:12:18 HOL: theory HOL.Set
19:12:19 HOL: theory HOL.Fun
19:12:19 HOL: theory HOL.Typedef
19:12:21 HOL: theory HOL.Rings
19:12:21 HOL: theory HOL.Complete_Lattices
19:12:24 HOL: theory HOL.Inductive
19:12:28 HOL: theory HOL.Product_Type
19:12:28 HOL: theory HOL.Sum_Type
19:12:30 HOL: theory HOL.Complete_Partial_Order
19:12:39 HOL: theory HOL.Nat
19:12:42 HOL: theory HOL.Fields
19:12:42 HOL: theory HOL.Meson
19:12:49 HOL: theory HOL.Relation
19:12:51 HOL: theory HOL.Finite_Set
19:12:53 HOL: theory HOL.Transitive_Closure
19:12:55 HOL: theory HOL.Wellfounded
19:12:56 HOL: theory HOL.Fun_Def_Base
19:12:56 HOL: theory HOL.Hilbert_Choice
19:12:56 HOL: theory HOL.Wfrec
19:12:56 HOL: theory HOL.Order_Relation
19:12:57 HOL: theory HOL.BNF_Wellorder_Relation
19:12:58 HOL: theory HOL.BNF_Wellorder_Embedding
19:12:58 HOL: theory HOL.Zorn
19:12:58 HOL: theory HOL.ATP
19:12:59 HOL: theory HOL.BNF_Wellorder_Constructions
19:13:01 HOL: theory HOL.BNF_Cardinal_Order_Relation
19:13:03 HOL: theory HOL.BNF_Cardinal_Arithmetic
19:13:04 HOL: theory HOL.BNF_Def
19:13:07 HOL: theory HOL.Metis
19:13:11 HOL: theory HOL.BNF_Composition
19:13:11 HOL: theory HOL.Basic_BNFs
19:13:12 HOL: theory HOL.BNF_Fixpoint_Base
19:13:18 HOL: theory HOL.BNF_Least_Fixpoint
19:13:22 HOL: theory HOL.Basic_BNF_LFPs
19:13:22 HOL: theory HOL.Equiv_Relations
19:13:22 HOL: theory HOL.Transfer
19:13:23 HOL: theory HOL.Num
19:13:23 HOL: theory HOL.Lifting
19:13:26 HOL: theory HOL.Option
19:13:26 HOL: theory HOL.Quotient
19:13:27 HOL: theory HOL.Extraction
19:13:27 HOL: theory HOL.Partial_Function
19:13:28 HOL: theory HOL.Fun_Def
19:13:28 HOL: theory HOL.Power
19:13:33 HOL: theory HOL.Groups_Big
19:13:36 HOL: theory HOL.Int
19:13:36 HOL: theory HOL.Lifting_Set
19:13:36 HOL: theory HOL.Lattices_Big
19:13:42 HOL: theory HOL.Euclidean_Rings
19:13:51 HOL: theory HOL.Parity
19:14:03 HOL: theory HOL.Divides
19:14:03 HOL: theory HOL.Set_Interval
19:14:03 HOL: theory HOL.Numeral_Simprocs
19:14:05 HOL: theory HOL.SMT
19:14:05 HOL: theory HOL.Semiring_Normalization
19:14:09 HOL: theory HOL.Groebner_Basis
19:14:11 HOL: theory HOL.Presburger
19:14:11 HOL: theory HOL.Filter
19:14:11 HOL: theory HOL.Conditionally_Complete_Lattices
19:14:17 HOL: theory HOL.Sledgehammer
19:14:21 HOL: theory HOL.List
19:14:33 HOL: theory HOL.Groups_List
19:14:33 HOL: theory HOL.Map
19:14:38 HOL: theory HOL.Bit_Operations
19:14:38 HOL: theory HOL.Enum
19:14:38 HOL: theory HOL.Factorial
19:14:40 HOL: theory HOL.Binomial
19:15:08 HOL: theory HOL.Code_Numeral
19:15:10 HOL: theory HOL.GCD
19:15:10 HOL: theory HOL.String
19:15:10 HOL: theory HOL.Random
19:15:15 HOL: theory HOL.BNF_Greatest_Fixpoint
19:15:15 HOL: theory HOL.Typerep
19:15:15 HOL: theory HOL.Predicate
19:15:17 HOL: theory HOL.Lazy_Sequence
19:15:18 HOL: theory HOL.Limited_Sequence
19:15:18 HOL: theory HOL.Code_Evaluation
19:15:20 HOL: theory HOL.Quickcheck_Random
19:15:22 HOL: theory HOL.Quickcheck_Narrowing
19:15:22 HOL: theory HOL.Random_Pred
19:15:22 HOL: theory HOL.Quickcheck_Exhaustive
19:15:23 HOL: theory HOL.Random_Sequence
19:15:29 HOL: theory HOL.Predicate_Compile
19:15:29 HOL: theory HOL.Record
19:15:31 HOL: theory HOL.Nitpick
19:15:32 HOL: theory HOL.Mirabelle
19:15:38 HOL: theory HOL.Nunchaku
19:15:40 HOL: theory Main
19:15:41 HOL: theory HOL.Archimedean_Field
19:15:41 HOL: theory HOL.Hull
19:15:41 HOL: theory HOL.Topological_Spaces
19:15:42 HOL: theory HOL.Modules
19:15:43 HOL: theory HOL.Vector_Spaces
19:15:53 HOL: theory HOL.Rat
19:15:56 HOL: theory HOL.Real
19:15:58 HOL: theory HOL.Binomial_Plus
19:15:58 HOL: theory HOL.Real_Vector_Spaces
19:16:21 HOL: theory HOL.Limits
19:16:21 HOL: theory HOL.Inequalities
19:16:31 HOL: theory HOL.Deriv
19:16:31 HOL: theory HOL.Series
19:16:33 HOL: theory HOL.NthRoot
19:16:34 HOL: theory HOL.Transcendental
19:16:41 HOL: theory HOL.Complex
19:16:42 HOL: theory HOL.MacLaurin
19:16:43 HOL: theory Complex_Main
19:17:45 Preparing HOL/document ...
19:19:42 Finished HOL/document (0:01:57 elapsed time)
19:19:42 Preparing HOL/outline ...
19:20:47 Finished HOL/outline (0:01:05 elapsed time)
19:20:48 Timing HOL (8 threads, 305.383s elapsed time, 1204.816s cpu time, 67.669s GC time, factor 3.95)
19:20:48 Finished HOL (0:05:34 elapsed time, 0:21:15 cpu time, factor 3.81)
19:20:48 Building HOL-Analysis (on hpcisabelle/2) ...
19:20:52 HOL-Analysis: theory HOL-Combinatorics.Transposition
19:20:52 HOL-Analysis: theory HOL-Library.BNF_Corec
19:20:52 HOL-Analysis: theory HOL-Library.Cancellation
19:20:52 HOL-Analysis: theory HOL-Library.FuncSet
19:20:52 HOL-Analysis: theory HOL-Library.Nat_Bijection
19:20:52 HOL-Analysis: theory HOL-Library.Old_Datatype
19:20:52 HOL-Analysis: theory HOL-Library.Infinite_Set
19:20:52 HOL-Analysis: theory HOL-Library.Phantom_Type
19:20:53 HOL-Analysis: theory HOL-Library.Product_Plus
19:20:53 HOL-Analysis: theory HOL-Library.Product_Order
19:20:53 HOL-Analysis: theory HOL-Library.Set_Algebras
19:20:54 HOL-Analysis: theory HOL-Real_Asymp.Inst_Existentials
19:20:54 HOL-Analysis: theory HOL-Analysis.Metric_Arith
19:20:54 HOL-Analysis: theory HOL-Library.Countable
19:20:54 HOL-Analysis: theory HOL-Analysis.Inner_Product
19:20:54 HOL-Analysis: theory HOL-Library.Disjoint_Sets
19:20:54 HOL-Analysis: theory HOL-Analysis.L2_Norm
19:20:54 HOL-Analysis: theory HOL-Library.Cardinality
19:20:54 HOL-Analysis: theory HOL-Library.Multiset
19:20:54 HOL-Analysis: theory HOL-Analysis.Operator_Norm
19:20:55 HOL-Analysis: theory HOL-Analysis.Poly_Roots
19:20:55 HOL-Analysis: theory HOL-Analysis.Product_Vector
19:20:55 HOL-Analysis: theory HOL-Library.Complex_Order
19:20:55 HOL-Analysis: theory HOL-Library.Discrete
19:20:55 HOL-Analysis: theory HOL-Library.Indicator_Function
19:20:56 HOL-Analysis: theory HOL-Library.Landau_Symbols
19:20:56 HOL-Analysis: theory HOL-Library.Numeral_Type
19:20:56 HOL-Analysis: theory HOL-Library.Liminf_Limsup
19:20:56 HOL-Analysis: theory HOL-Library.Nonpos_Ints
19:20:56 HOL-Analysis: theory HOL-Library.Countable_Set
19:20:56 HOL-Analysis: theory HOL-Library.Periodic_Fun
19:20:56 HOL-Analysis: theory HOL-Library.Sum_of_Squares
19:20:57 HOL-Analysis: theory HOL-Real_Asymp.Eventuallize
19:20:57 HOL-Analysis: theory HOL-Real_Asymp.Lazy_Eval
19:20:57 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
19:20:57 HOL-Analysis: theory HOL-Library.Equipollence
19:20:58 HOL-Analysis: theory HOL-Library.Set_Idioms
19:20:58 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
19:20:58 HOL-Analysis: theory HOL-Analysis.Abstract_Topology
19:20:58 HOL-Analysis: theory HOL-Analysis.Elementary_Topology
19:20:58 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
19:21:04 HOL-Analysis: theory HOL-Library.Order_Continuity
19:21:04 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
19:21:04 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
19:21:05 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
19:21:05 HOL-Analysis: theory HOL-Combinatorics.Permutations
19:21:05 HOL-Analysis: theory HOL-Analysis.Norm_Arith
19:21:05 HOL-Analysis: theory HOL-Library.Extended_Nat
19:21:08 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion
19:21:08 HOL-Analysis: theory HOL-Analysis.Abstract_Limits
19:21:08 HOL-Analysis: theory HOL-Analysis.FSigma
19:21:08 HOL-Analysis: theory HOL-Analysis.Sum_Topology
19:21:08 HOL-Analysis: theory HOL-Analysis.Affine
19:21:08 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
19:21:09 HOL-Analysis: theory HOL-Library.Extended_Real
19:21:09 HOL-Analysis: theory HOL-Analysis.Convex
19:21:09 HOL-Analysis: theory HOL-Analysis.Cartesian_Space
19:21:12 HOL-Analysis: theory HOL-Analysis.Connected
19:21:12 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
19:21:12 HOL-Analysis: theory HOL-Analysis.Function_Topology
19:21:13 HOL-Analysis: theory HOL-Analysis.Determinants
19:21:14 HOL-Analysis: theory HOL-Analysis.Product_Topology
19:21:16 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
19:21:16 HOL-Analysis: theory HOL-Analysis.T1_Spaces
19:21:17 HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
19:21:17 HOL-Analysis: theory HOL-Analysis.Function_Metric
19:21:17 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
19:21:17 HOL-Analysis: theory HOL-Analysis.Isolated
19:21:19 HOL-Analysis: theory HOL-Analysis.Infinite_Sum
19:21:19 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
19:21:19 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
19:21:21 HOL-Analysis: theory HOL-Analysis.Measurable
19:21:21 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
19:21:21 HOL-Analysis: theory HOL-Analysis.Line_Segment
19:21:21 HOL-Analysis: theory HOL-Analysis.Measure_Space
19:21:21 HOL-Analysis: theory HOL-Analysis.Tagged_Division
19:21:21 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
19:21:23 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
19:21:23 HOL-Analysis: theory HOL-Analysis.Summation_Tests
19:21:24 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
19:21:24 HOL-Analysis: theory HOL-Analysis.Starlike
19:21:25 HOL-Analysis: theory HOL-Analysis.Caratheodory
19:21:27 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
19:21:27 HOL-Analysis: theory HOL-Analysis.Path_Connected
19:21:29 HOL-Analysis: theory HOL-Analysis.Locally
19:21:29 HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
19:21:29 HOL-Analysis: theory HOL-Analysis.Homotopy
19:21:32 HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
19:21:32 HOL-Analysis: theory HOL-Analysis.Homeomorphism
19:21:32 HOL-Analysis: theory HOL-Analysis.Sparse_In
19:21:32 HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
19:21:36 HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
19:21:37 HOL-Analysis: theory HOL-Computational_Algebra.Primes
19:21:38 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
19:21:40 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
19:21:40 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
19:21:42 HOL-Analysis: theory HOL-Analysis.Derivative
19:21:43 HOL-Analysis: theory HOL-Analysis.Borel_Space
19:21:43 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
19:21:44 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
19:21:44 HOL-Analysis: theory HOL-Analysis.Lipschitz
19:21:44 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
19:21:44 HOL-Analysis: theory HOL-Analysis.Cross3
19:21:44 HOL-Analysis: theory HOL-Analysis.Polytope
19:21:46 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
19:21:46 HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
19:21:46 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
19:21:47 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
19:21:47 HOL-Analysis: theory HOL-Analysis.Retracts
19:21:47 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
19:21:48 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
19:21:48 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
19:21:48 HOL-Analysis: theory HOL-Analysis.Regularity
19:21:49 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
19:21:50 HOL-Analysis: theory HOL-Analysis.Smooth_Paths
19:21:53 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
19:21:53 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
19:21:53 HOL-Analysis: theory HOL-Analysis.Infinite_Products
19:21:53 HOL-Analysis: theory HOL-Analysis.Urysohn
19:21:54 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
19:21:55 HOL-Analysis: theory HOL-Real_Asymp.Real_Asymp
19:21:56 HOL-Analysis: theory HOL-Analysis.Embed_Measure
19:21:56 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
19:21:58 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
19:21:59 HOL-Analysis: theory HOL-Analysis.FPS_Convergence
19:22:01 HOL-Analysis: theory HOL-Analysis.Complete_Measure
19:22:01 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
19:22:02 HOL-Analysis: theory HOL-Analysis.Set_Integral
19:22:05 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
19:22:06 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
19:22:07 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
19:22:09 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
19:22:09 HOL-Analysis: theory HOL-Analysis.Integral_Test
19:22:09 HOL-Analysis: theory HOL-Analysis.Kronecker_Approximation_Theorem
19:22:12 HOL-Analysis: theory HOL-Analysis.Further_Topology
19:22:12 HOL-Analysis: theory HOL-Analysis.Gamma_Function
19:22:12 HOL-Analysis: theory HOL-Analysis.Improper_Integral
19:22:12 HOL-Analysis: theory HOL-Analysis.Interval_Integral
19:22:12 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
19:22:12 HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
19:22:13 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
19:22:14 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
19:22:16 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
19:22:16 HOL-Analysis: theory HOL-Analysis.Simplex_Content
19:22:17 HOL-Analysis: theory HOL-Analysis.Ball_Volume
19:22:17 HOL-Analysis: theory HOL-Analysis.Analysis
19:31:59 Preparing HOL-Analysis/document ...
19:35:01 Finished HOL-Analysis/document (0:03:02 elapsed time)
19:35:01 Preparing HOL-Analysis/manual ...
19:35:26 Finished HOL-Analysis/manual (0:00:24 elapsed time)
19:35:27 Timing HOL-Analysis (8 threads, 573.020s elapsed time, 3931.443s cpu time, 377.416s GC time, factor 6.86)
19:35:27 Finished HOL-Analysis (0:10:52 elapsed time, 1:08:51 cpu time, factor 6.33)
19:35:27 Building Ordinary_Differential_Equations (on hpcisabelle/3) ...
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
19:35:29 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Code_Cardinality
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
19:35:29 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
19:35:29 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
19:35:30 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
19:35:30 Ordinary_Differential_Equations: theory Triangle.Angles
19:35:30 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
19:35:30 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
19:35:30 Ordinary_Differential_Equations: theory List-Index.List_Index
19:35:30 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
19:35:30 Ordinary_Differential_Equations: theory Triangle.Triangle
19:35:30 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
19:35:30 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
19:35:37 Ordinary_Differential_Equations: theory HOL-Library.Interval
19:35:37 Ordinary_Differential_Equations: theory HOL-Library.Float
19:35:40 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral_Float
19:35:40 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
19:35:40 Ordinary_Differential_Equations: theory HOL-Library.Interval_Float
19:35:41 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
19:35:44 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
19:35:45 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
19:35:46 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
19:35:47 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
19:35:48 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
19:35:50 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
19:35:51 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
19:35:56 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
19:35:56 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
19:35:56 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
19:35:58 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
19:36:01 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs
19:36:39 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
19:36:42 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
19:38:22 Preparing Ordinary_Differential_Equations/document ...
19:38:38 Finished Ordinary_Differential_Equations/document (0:00:16 elapsed time)
19:38:38 Preparing Ordinary_Differential_Equations/outline ...
19:38:45 Finished Ordinary_Differential_Equations/outline (0:00:06 elapsed time)
19:38:45 Timing Ordinary_Differential_Equations (8 threads, 150.397s elapsed time, 747.005s cpu time, 11.656s GC time, factor 4.97)
19:38:45 Finished Ordinary_Differential_Equations (0:02:53 elapsed time, 0:13:12 cpu time, factor 4.58)
19:38:45 Building HOL-ODE-Numerics (on hpcisabelle/4) ...
19:38:48 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
19:38:48 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
19:38:48 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
19:38:48 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
19:38:48 HOL-ODE-Numerics: theory Deriving.Comparator
19:38:48 HOL-ODE-Numerics: theory Deriving.Derive_Manager
19:38:48 HOL-ODE-Numerics: theory Deriving.Generator_Aux
19:38:48 HOL-ODE-Numerics: theory HOL-Library.AList
19:38:49 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
19:38:49 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
19:38:49 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
19:38:49 HOL-ODE-Numerics: theory HOL-ex.Quicksort
19:38:49 HOL-ODE-Numerics: theory HOL-Library.Char_ord
19:38:49 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
19:38:49 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
19:38:49 HOL-ODE-Numerics: theory Deriving.Equality_Generator
19:38:49 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
19:38:49 HOL-ODE-Numerics: theory HOL-Library.Option_ord
19:38:50 HOL-ODE-Numerics: theory HOL-Library.Parallel
19:38:50 HOL-ODE-Numerics: theory HOL-Library.Type_Length
19:38:50 HOL-ODE-Numerics: theory Deriving.Equality_Instances
19:38:50 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
19:38:51 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
19:38:51 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
19:38:51 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
19:38:51 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
19:38:51 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
19:38:51 HOL-ODE-Numerics: theory Deriving.Compare
19:38:51 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
19:38:51 HOL-ODE-Numerics: theory HOL-Library.Mapping
19:38:51 HOL-ODE-Numerics: theory HOL-Library.Word
19:38:51 HOL-ODE-Numerics: theory Deriving.Countable_Generator
19:38:52 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
19:38:52 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
19:38:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
19:38:53 HOL-ODE-Numerics: theory Deriving.Compare_Generator
19:38:53 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
19:38:53 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
19:38:53 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
19:38:54 HOL-ODE-Numerics: theory Deriving.Compare_Instances
19:38:54 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
19:38:54 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
19:38:54 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
19:38:54 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
19:38:54 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
19:38:55 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
19:38:55 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
19:38:56 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
19:38:56 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
19:38:56 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
19:38:56 HOL-ODE-Numerics: theory Show.Show
19:38:56 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
19:38:56 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
19:38:57 HOL-ODE-Numerics: theory Show.Show_Instances
19:38:58 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
19:38:58 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
19:38:58 HOL-ODE-Numerics: theory Collections.SetIterator
19:38:58 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
19:38:58 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
19:38:59 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
19:38:59 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
19:38:59 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
19:39:00 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
19:39:01 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
19:39:02 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
19:39:02 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
19:39:02 HOL-ODE-Numerics: theory Collections.Assoc_List
19:39:03 HOL-ODE-Numerics: theory Collections.Proper_Iterator
19:39:03 HOL-ODE-Numerics: theory Collections.SetIteratorGA
19:39:03 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
19:39:03 HOL-ODE-Numerics: theory Word_Lib.More_Divides
19:39:03 HOL-ODE-Numerics: theory Collections.Diff_Array
19:39:03 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
19:39:03 HOL-ODE-Numerics: theory Collections.It_to_It
19:39:03 HOL-ODE-Numerics: theory Word_Lib.More_Word
19:39:04 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
19:39:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
19:39:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
19:39:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
19:39:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
19:39:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
19:39:06 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
19:39:06 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
19:39:06 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
19:39:07 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
19:39:07 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
19:39:08 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
19:39:08 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
19:39:09 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
19:39:09 HOL-ODE-Numerics: theory Collections.Intf_Comp
19:39:09 HOL-ODE-Numerics: theory Collections.Idx_Iterator
19:39:09 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
19:39:10 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
19:39:11 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
19:39:11 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
19:39:12 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
19:39:12 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
19:39:12 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
19:39:13 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
19:39:15 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
19:39:17 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
19:39:17 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
19:39:17 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
19:39:17 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
19:39:17 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
19:39:19 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
19:39:20 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
19:39:20 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
19:39:21 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
19:39:24 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
19:39:24 HOL-ODE-Numerics: theory Native_Word.Uint
19:39:24 HOL-ODE-Numerics: theory Native_Word.Uint32
19:39:24 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
19:39:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
19:39:26 HOL-ODE-Numerics: theory Collections.Gen_Iterator
19:39:26 HOL-ODE-Numerics: theory Collections.Intf_Map
19:39:26 HOL-ODE-Numerics: theory Collections.Intf_Set
19:39:26 HOL-ODE-Numerics: theory Collections.HashCode
19:39:27 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
19:39:27 HOL-ODE-Numerics: theory Collections.Iterator
19:39:27 HOL-ODE-Numerics: theory Collections.Intf_Hash
19:39:27 HOL-ODE-Numerics: theory Deriving.Hash_Generator
19:39:27 HOL-ODE-Numerics: theory Collections.Array_Iterator
19:39:27 HOL-ODE-Numerics: theory Collections.Gen_Map
19:39:28 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
19:39:28 HOL-ODE-Numerics: theory Collections.Gen_Set
19:39:28 HOL-ODE-Numerics: theory Collections.Impl_List_Set
19:39:28 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
19:39:29 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
19:39:29 HOL-ODE-Numerics: theory Collections.Gen_Hash
19:39:29 HOL-ODE-Numerics: theory Deriving.Hash_Instances
19:39:29 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
19:39:29 HOL-ODE-Numerics: theory Collections.Impl_List_Map
19:39:29 HOL-ODE-Numerics: theory Deriving.Derive
19:39:30 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
19:40:03 HOL-ODE-Numerics: theory HOL-Library.RBT
19:40:03 HOL-ODE-Numerics: theory Collections.RBT_add
19:40:04 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
19:40:04 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
19:40:05 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
19:40:15 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
19:40:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
19:40:22 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
19:40:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
19:40:24 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
19:40:27 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
19:40:29 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
19:40:29 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
19:40:29 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
19:40:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
19:40:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
19:40:31 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
19:40:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
19:40:40 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
19:40:40 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
19:40:40 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
19:40:40 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
19:40:46 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
19:40:46 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
19:40:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
19:40:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
19:40:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
19:40:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
19:40:55 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
19:41:16 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
19:41:37 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
19:41:38 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
19:41:53 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
19:41:53 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
19:41:53 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
19:41:54 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
19:42:11 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
19:42:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
19:42:25 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
19:42:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
19:43:41 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
19:51:53 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
19:52:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
19:53:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
19:55:28 Timing HOL-ODE-Numerics (8 threads, 916.353s elapsed time, 5079.857s cpu time, 344.513s GC time, factor 5.54)
19:55:28 Finished HOL-ODE-Numerics (0:16:33 elapsed time, 1:27:51 cpu time, factor 5.30)
19:55:28 Building ZFC_in_HOL (on hpcisabelle/5) ...
19:55:29 ZFC_in_HOL: theory HOL-Cardinals.Fun_More
19:55:29 ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More
19:55:29 ZFC_in_HOL: theory HOL-Cardinals.Order_Union
19:55:29 ZFC_in_HOL: theory HOL-Library.Infinite_Set
19:55:29 ZFC_in_HOL: theory HOL-Library.FuncSet
19:55:29 ZFC_in_HOL: theory HOL-Library.Old_Datatype
19:55:29 ZFC_in_HOL: theory HOL-Library.Nat_Bijection
19:55:29 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension
19:55:30 ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More
19:55:30 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation
19:55:30 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding
19:55:30 ZFC_in_HOL: theory HOL-Library.Countable
19:55:30 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions
19:55:31 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation
19:55:31 ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic
19:55:32 ZFC_in_HOL: theory HOL-Library.Countable_Set
19:55:32 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic
19:55:33 ZFC_in_HOL: theory HOL-Library.Equipollence
19:55:33 ZFC_in_HOL: theory HOL-Analysis.Continuum_Not_Denumerable
19:55:33 ZFC_in_HOL: theory HOL-Cardinals.Cardinals
19:55:34 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library
19:55:34 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL
19:55:35 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals
19:55:37 ZFC_in_HOL: theory ZFC_in_HOL.Kirby
19:55:37 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses
19:55:38 ZFC_in_HOL: theory ZFC_in_HOL.Ordinal_Exp
19:55:38 ZFC_in_HOL: theory ZFC_in_HOL.Cantor_NF
19:55:39 ZFC_in_HOL: theory ZFC_in_HOL.General_Cardinals
19:56:19 Preparing ZFC_in_HOL/document ...
19:56:29 Finished ZFC_in_HOL/document (0:00:10 elapsed time)
19:56:29 Preparing ZFC_in_HOL/outline ...
19:56:34 Finished ZFC_in_HOL/outline (0:00:05 elapsed time)
19:56:34 Timing ZFC_in_HOL (8 threads, 39.224s elapsed time, 253.553s cpu time, 4.569s GC time, factor 6.46)
19:56:34 Finished ZFC_in_HOL (0:00:49 elapsed time, 0:04:33 cpu time, factor 5.48)
19:56:34 Building CZH_Foundations (on hpcisabelle/6) ...
19:56:36 CZH_Foundations: theory CZH_Foundations.CZH_Sets_MIF
19:56:36 CZH_Foundations: theory CZH_Foundations.CZH_Utilities
19:56:36 CZH_Foundations: theory Conditional_Simplification.CS_Tools
19:56:36 CZH_Foundations: theory HOL-Eisbach.Eisbach
19:56:36 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum_Library
19:56:36 CZH_Foundations: theory HOL-Library.Rewrite
19:56:36 CZH_Foundations: theory CZH_Foundations.CZH_Introduction
19:56:36 CZH_Foundations: theory Intro_Dest_Elim.IHOL_IDE
19:56:36 CZH_Foundations: theory Conditional_Simplification.IHOL_CS
19:56:37 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum
19:56:38 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Introduction
19:56:39 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Sets
19:56:40 CZH_Foundations: theory CZH_Foundations.CZH_Sets_BRelations
19:56:40 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Nat
19:56:43 CZH_Foundations: theory CZH_Foundations.CZH_Sets_IF
19:56:44 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Equipollence
19:56:44 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Cardinality
19:56:45 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Ordinals
19:56:45 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FSequences
19:56:47 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FBRelations
19:56:49 CZH_Foundations: theory CZH_Foundations.CZH_Sets_NOP
19:56:49 CZH_Foundations: theory CZH_Foundations.CZH_Sets_VNHS
19:56:50 CZH_Foundations: theory CZH_Foundations.CZH_DG_Introduction
19:56:50 CZH_Foundations: theory CZH_Foundations.CZH_Sets_ZQR
19:56:56 CZH_Foundations: theory CZH_Foundations.CZH_EX_Replacement
19:56:57 CZH_Foundations: theory CZH_Foundations.CZH_EX_TS
19:56:57 CZH_Foundations: theory CZH_Foundations.CZH_DG_Digraph
19:56:57 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Introduction
19:56:58 CZH_Foundations: theory CZH_Foundations.CZH_EX_Algebra
19:56:59 CZH_Foundations: theory CZH_Foundations.CZH_DG_DGHM
19:56:59 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_Digraph
19:56:59 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semicategory
19:57:00 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Conclusions
19:57:03 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semicategory
19:57:16 CZH_Foundations: theory CZH_Foundations.CZH_DG_TDGHM
19:57:16 CZH_Foundations: theory CZH_Foundations.CZH_DG_GRPH
19:57:17 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_DGHM
19:57:23 CZH_Foundations: theory CZH_Foundations.CZH_DG_Rel
19:57:23 CZH_Foundations: theory CZH_Foundations.CZH_DG_Subdigraph
19:57:23 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semifunctor
19:57:24 CZH_Foundations: theory CZH_Foundations.CZH_DG_Simple
19:57:24 CZH_Foundations: theory CZH_Foundations.CZH_DG_PDigraph
19:57:24 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_TDGHM
19:57:25 CZH_Foundations: theory CZH_Foundations.CZH_SMC_GRPH
19:57:29 CZH_Foundations: theory CZH_Foundations.CZH_DG_Par
19:57:31 CZH_Foundations: theory CZH_Foundations.CZH_DG_Set
19:57:32 CZH_Foundations: theory CZH_Foundations.CZH_DG_Conclusions
19:57:42 CZH_Foundations: theory CZH_Foundations.CZH_DG_SemiCAT
19:57:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_NTSMCF
19:57:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Subsemicategory
19:57:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_PSemicategory
19:57:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Rel
19:57:43 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semifunctor
19:57:51 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Simple
19:57:51 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_NTSMCF
19:57:52 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Par
19:57:52 CZH_Foundations: theory CZH_Foundations.CZH_SMC_SemiCAT
19:57:53 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Set
19:58:02 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Conclusions
19:58:45 Preparing CZH_Foundations/document ...
20:00:07 Finished CZH_Foundations/document (0:01:22 elapsed time)
20:00:07 Preparing CZH_Foundations/outline ...
20:00:54 Finished CZH_Foundations/outline (0:00:47 elapsed time)
20:00:55 Timing CZH_Foundations (8 threads, 117.452s elapsed time, 753.220s cpu time, 51.830s GC time, factor 6.41)
20:00:55 Finished CZH_Foundations (0:02:08 elapsed time, 0:12:54 cpu time, factor 6.04)
20:00:55 Building CZH_Elementary_Categories (on hpcisabelle/7) ...
20:00:56 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Introduction
20:00:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Category
20:01:06 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Functor
20:01:06 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
20:01:09 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_GRPH
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Order
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_NTCF
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_CAT
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Rel
20:01:32 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
20:01:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Parallel
20:01:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SS
20:01:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
20:01:46 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
20:01:47 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
20:01:47 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Par
20:01:57 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_PCategory
20:01:57 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Simple
20:01:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
20:01:59 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Comma
20:02:00 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Discrete
20:02:06 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
20:02:10 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_CAT
20:02:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CAT
20:02:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_FUNCT
20:02:19 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Set
20:02:24 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Hom
20:02:26 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
20:02:34 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_FUNCT
20:02:38 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
20:02:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Cone
20:02:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
20:03:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Cone
20:03:29 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
20:10:25 Preparing CZH_Elementary_Categories/document ...
20:12:28 Finished CZH_Elementary_Categories/document (0:02:02 elapsed time)
20:12:28 Preparing CZH_Elementary_Categories/outline ...
20:13:25 Finished CZH_Elementary_Categories/outline (0:00:57 elapsed time)
20:13:26 Timing CZH_Elementary_Categories (8 threads, 555.929s elapsed time, 2499.527s cpu time, 212.581s GC time, factor 4.50)
20:13:26 Finished CZH_Elementary_Categories (0:09:28 elapsed time, 0:42:06 cpu time, factor 4.45)
20:13:26 Building Lorenz_Approximation (on hpcisabelle/0) ...
20:13:30 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
20:13:34 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
20:13:55 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
20:18:02 Timing Lorenz_Approximation (8 threads, 249.675s elapsed time, 625.752s cpu time, 34.339s GC time, factor 2.51)
20:18:02 Finished Lorenz_Approximation (0:04:35 elapsed time, 0:11:15 cpu time, factor 2.45)
20:18:02 Running Lorenz_C0 (on hpcisabelle/1) ...
20:18:06 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
20:42:54 Timing Lorenz_C0 (8 threads, 1487.583s elapsed time, 11728.361s cpu time, 24.509s GC time, factor 7.88)
20:42:54 Finished Lorenz_C0 (0:24:52 elapsed time, 3:15:34 cpu time, factor 7.86)
20:42:54 Building HOL-Library (on hpcisabelle/2) ...
20:42:56 HOL-Library: theory HOL-Library.README
20:42:56 HOL-Library: theory HOL-Library.AList
20:42:56 HOL-Library: theory HOL-Library.Adhoc_Overloading
20:42:56 HOL-Library: theory HOL-Library.Cancellation
20:42:56 HOL-Library: theory HOL-Library.Centered_Division
20:42:56 HOL-Library: theory HOL-Library.BNF_Axiomatization
20:42:56 HOL-Library: theory HOL-Library.BNF_Corec
20:42:56 HOL-Library: theory HOL-Library.Char_ord
20:42:56 HOL-Library: theory HOL-Library.Case_Converter
20:42:56 HOL-Library: theory HOL-Library.Code_Abstract_Char
20:42:56 HOL-Library: theory HOL-Library.Code_Abstract_Nat
20:42:56 HOL-Library: theory HOL-Library.Code_Prolog
20:42:57 HOL-Library: theory HOL-Library.Monad_Syntax
20:42:57 HOL-Library: theory HOL-Library.Code_Binary_Nat
20:42:57 HOL-Library: theory HOL-Library.State_Monad
20:42:57 HOL-Library: theory HOL-Library.Code_Target_Nat
20:42:57 HOL-Library: theory HOL-Library.Code_Lazy
20:42:57 HOL-Library: theory HOL-Library.Simps_Case_Conv
20:42:57 HOL-Library: theory HOL-Library.Extended
20:42:58 HOL-Library: theory HOL-Library.Multiset
20:42:58 HOL-Library: theory HOL-Library.Code_Target_Int
20:42:59 HOL-Library: theory HOL-Library.Code_Test
20:42:59 HOL-Library: theory HOL-Library.Code_Target_Numeral
20:42:59 HOL-Library: theory HOL-Library.Combine_PER
20:42:59 HOL-Library: theory HOL-Library.Comparator
20:42:59 HOL-Library: theory HOL-Library.Complete_Partial_Order2
20:42:59 HOL-Library: theory HOL-Library.DAList
20:43:00 HOL-Library: theory HOL-Library.Conditional_Parametricity
20:43:00 HOL-Library: theory HOL-Library.Confluence
20:43:00 HOL-Library: theory HOL-Library.Confluent_Quotient
20:43:00 HOL-Library: theory HOL-Library.Dlist
20:43:00 HOL-Library: theory HOL-Library.Datatype_Records
20:43:00 HOL-Library: theory HOL-Library.Debug
20:43:00 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
20:43:00 HOL-Library: theory HOL-Library.Fun_Lexorder
20:43:00 HOL-Library: theory HOL-Library.FuncSet
20:43:01 HOL-Library: theory HOL-Library.Function_Algebras
20:43:01 HOL-Library: theory HOL-Library.Groups_Big_Fun
20:43:01 HOL-Library: theory HOL-Library.IArray
20:43:01 HOL-Library: theory HOL-Library.Function_Division
20:43:02 HOL-Library: theory HOL-Library.Infinite_Set
20:43:02 HOL-Library: theory HOL-Library.Disjoint_Sets
20:43:02 HOL-Library: theory HOL-Library.LaTeXsugar
20:43:02 HOL-Library: theory HOL-Library.Lattice_Constructions
20:43:02 HOL-Library: theory HOL-Library.Omega_Words_Fun
20:43:02 HOL-Library: theory HOL-Library.ListVector
20:43:03 HOL-Library: theory HOL-Library.List_Lenlexorder
20:43:03 HOL-Library: theory HOL-Library.List_Lexorder
20:43:03 HOL-Library: theory HOL-Library.Mapping
20:43:03 HOL-Library: theory HOL-Library.More_List
20:43:04 HOL-Library: theory HOL-Library.NList
20:43:04 HOL-Library: theory HOL-Library.Nat_Bijection
20:43:04 HOL-Library: theory HOL-Library.Poly_Mapping
20:43:04 HOL-Library: theory HOL-Library.Stream
20:43:07 HOL-Library: theory HOL-Library.Old_Datatype
20:43:08 HOL-Library: theory HOL-Library.AList_Mapping
20:43:09 HOL-Library: theory HOL-Library.Old_Recdef
20:43:09 HOL-Library: theory HOL-Library.Open_State_Syntax
20:43:09 HOL-Library: theory HOL-Library.Option_ord
20:43:09 HOL-Library: theory HOL-Library.Parallel
20:43:09 HOL-Library: theory HOL-Library.Pattern_Aliases
20:43:10 HOL-Library: theory HOL-Library.Phantom_Type
20:43:10 HOL-Library: theory HOL-Library.Power_By_Squaring
20:43:10 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
20:43:10 HOL-Library: theory HOL-Library.DAList_Multiset
20:43:10 HOL-Library: theory HOL-Library.Multiset_Order
20:43:10 HOL-Library: theory HOL-Library.Preorder
20:43:10 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
20:43:11 HOL-Library: theory HOL-Library.Product_Lexorder
20:43:11 HOL-Library: theory HOL-Library.Cardinality
20:43:11 HOL-Library: theory HOL-Library.Product_Plus
20:43:11 HOL-Library: theory HOL-Library.Quotient_Syntax
20:43:11 HOL-Library: theory HOL-Library.Quotient_Type
20:43:11 HOL-Library: theory HOL-Library.RBT_Impl
20:43:12 HOL-Library: theory HOL-Library.Quotient_Option
20:43:12 HOL-Library: theory HOL-Library.Quotient_Product
20:43:12 HOL-Library: theory HOL-Library.Product_Order
20:43:12 HOL-Library: theory HOL-Library.Quotient_Set
20:43:13 HOL-Library: theory HOL-Library.Quotient_Sum
20:43:13 HOL-Library: theory HOL-Library.Quotient_List
20:43:13 HOL-Library: theory HOL-Library.Realizers
20:43:13 HOL-Library: theory HOL-Library.Reflection
20:43:13 HOL-Library: theory HOL-Library.Refute
20:43:13 HOL-Library: theory HOL-Library.Finite_Lattice
20:43:13 HOL-Library: theory HOL-Library.Rewrite
20:43:14 HOL-Library: theory HOL-Library.Set_Algebras
20:43:14 HOL-Library: theory HOL-Library.Signed_Division
20:43:14 HOL-Library: theory HOL-Library.Code_Cardinality
20:43:14 HOL-Library: theory HOL-Library.Numeral_Type
20:43:14 HOL-Library: theory HOL-Library.Sorting_Algorithms
20:43:14 HOL-Library: theory HOL-Library.Sublist
20:43:15 HOL-Library: theory HOL-Library.Transitive_Closure_Table
20:43:16 HOL-Library: theory HOL-Library.Tree
20:43:16 HOL-Library: theory HOL-Library.Uprod
20:43:16 HOL-Library: theory HOL-Library.Type_Length
20:43:16 HOL-Library: theory HOL-Library.While_Combinator
20:43:16 HOL-Library: theory HOL-Library.Z2
20:43:16 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
20:43:16 HOL-Library: theory HOL-Library.Saturated
20:43:17 HOL-Library: theory HOL-Library.Word
20:43:17 HOL-Library: theory HOL-Library.Countable
20:43:17 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
20:43:17 HOL-Library: theory HOL-Library.Prefix_Order
20:43:17 HOL-Library: theory HOL-Library.Subseq_Order
20:43:17 HOL-Library: theory HOL-Library.Complex_Order
20:43:17 HOL-Library: theory HOL-Library.Diagonal_Subsequence
20:43:17 HOL-Library: theory HOL-Library.Discrete
20:43:17 HOL-Library: theory HOL-Library.Going_To_Filter
20:43:17 HOL-Library: theory HOL-Library.Indicator_Function
20:43:17 HOL-Library: theory HOL-Library.Infinite_Typeclass
20:43:17 HOL-Library: theory HOL-Library.Landau_Symbols
20:43:18 HOL-Library: theory HOL-Library.Lattice_Algebras
20:43:18 HOL-Library: theory HOL-Library.Liminf_Limsup
20:43:18 HOL-Library: theory HOL-Library.Countable_Set
20:43:18 HOL-Library: theory HOL-Library.Tree_Multiset
20:43:19 HOL-Library: theory HOL-Library.FSet
20:43:19 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
20:43:19 HOL-Library: theory HOL-Library.Countable_Set_Type
20:43:21 HOL-Library: theory HOL-Library.Equipollence
20:43:21 HOL-Library: theory HOL-Library.Set_Idioms
20:43:21 HOL-Library: theory HOL-Library.Log_Nat
20:43:22 HOL-Library: theory HOL-Library.Lub_Glb
20:43:22 HOL-Library: theory HOL-Library.Ramsey
20:43:22 HOL-Library: theory HOL-Library.Nonpos_Ints
20:43:22 HOL-Library: theory HOL-Library.OptionalSugar
20:43:22 HOL-Library: theory HOL-Library.Order_Continuity
20:43:22 HOL-Library: theory HOL-Library.Periodic_Fun
20:43:22 HOL-Library: theory HOL-Library.Quadratic_Discriminant
20:43:22 HOL-Library: theory HOL-Library.Real_Mod
20:43:22 HOL-Library: theory HOL-Library.Sum_of_Squares
20:43:23 HOL-Library: theory HOL-Library.Finite_Map
20:43:23 HOL-Library: theory HOL-Library.Extended_Nat
20:43:23 HOL-Library: theory HOL-Library.Tree_Real
20:43:24 HOL-Library: theory HOL-Library.Extended_Real
20:43:24 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
20:43:24 HOL-Library: theory HOL-Library.Interval
20:43:26 HOL-Library: theory HOL-Library.Float
20:43:29 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
20:43:29 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
20:43:29 HOL-Library: theory HOL-Library.Interval_Float
20:43:38 HOL-Library: theory HOL-Library.Disjoint_FSets
20:43:38 HOL-Library: theory HOL-Library.Library
20:44:20 HOL-Library: theory HOL-Library.RBT
20:44:21 HOL-Library: theory HOL-Library.RBT_Mapping
20:44:21 HOL-Library: theory HOL-Library.RBT_Set
20:46:50 Preparing HOL-Library/document ...
20:47:56 Finished HOL-Library/document (0:01:05 elapsed time)
20:47:56 Preparing HOL-Library/outline ...
20:48:33 Finished HOL-Library/outline (0:00:37 elapsed time)
20:48:34 Timing HOL-Library (8 threads, 194.296s elapsed time, 1293.818s cpu time, 72.142s GC time, factor 6.66)
20:48:34 Finished HOL-Library (0:03:49 elapsed time, 0:22:57 cpu time, factor 5.99)
20:48:34 Running CZH_Universal_Constructions (on hpcisabelle/3) ...
20:48:36 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
20:48:36 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
20:48:36 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
20:48:50 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
20:49:32 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
20:49:55 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
20:50:21 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
20:50:24 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
20:50:28 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
20:51:05 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
20:51:41 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
20:51:50 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
21:10:59 Preparing CZH_Universal_Constructions/document ...
21:12:06 Finished CZH_Universal_Constructions/document (0:01:06 elapsed time)
21:12:06 Preparing CZH_Universal_Constructions/outline ...
21:12:31 Finished CZH_Universal_Constructions/outline (0:00:25 elapsed time)
21:12:31 Timing CZH_Universal_Constructions (8 threads, 1339.973s elapsed time, 5158.274s cpu time, 377.435s GC time, factor 3.85)
21:12:31 Finished CZH_Universal_Constructions (0:22:23 elapsed time, 1:26:06 cpu time, factor 3.85)
21:12:31 Building HOL-Computational_Algebra (on hpcisabelle/4) ...
21:12:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
21:12:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
21:12:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
21:12:44 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
21:12:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
21:12:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
21:12:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
21:13:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
21:13:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
21:13:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
21:13:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
21:13:20 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:13:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
21:13:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
21:13:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
21:13:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
21:13:55 Preparing HOL-Computational_Algebra/document ...
21:14:21 Finished HOL-Computational_Algebra/document (0:00:25 elapsed time)
21:14:21 Preparing HOL-Computational_Algebra/outline ...
21:14:33 Finished HOL-Computational_Algebra/outline (0:00:12 elapsed time)
21:14:33 Timing HOL-Computational_Algebra (8 threads, 66.669s elapsed time, 269.940s cpu time, 5.502s GC time, factor 4.05)
21:14:33 Finished HOL-Computational_Algebra (0:01:22 elapsed time, 0:05:01 cpu time, factor 3.65)
21:14:33 Building HOL-Algebra (on hpcisabelle/5) ...
21:14:36 HOL-Algebra: theory HOL-Algebra.README
21:14:36 HOL-Algebra: theory HOL-Cardinals.Order_Union
21:14:36 HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
21:14:36 HOL-Algebra: theory HOL-Cardinals.Fun_More
21:14:36 HOL-Algebra: theory HOL-Combinatorics.Transposition
21:14:36 HOL-Algebra: theory HOL-Algebra.Exponent
21:14:36 HOL-Algebra: theory HOL-Algebra.Congruence
21:14:36 HOL-Algebra: theory HOL-Combinatorics.Permutations
21:14:37 HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
21:14:37 HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
21:14:37 HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
21:14:37 HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
21:14:38 HOL-Algebra: theory HOL-Algebra.Order
21:14:38 HOL-Algebra: theory HOL-Combinatorics.Cycles
21:14:38 HOL-Algebra: theory HOL-Combinatorics.List_Permutation
21:14:38 HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
21:14:39 HOL-Algebra: theory HOL-Algebra.Lattice
21:14:39 HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
21:14:40 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
21:14:42 HOL-Algebra: theory HOL-Algebra.Galois_Connection
21:14:42 HOL-Algebra: theory HOL-Algebra.Group
21:14:45 HOL-Algebra: theory HOL-Algebra.Bij
21:14:45 HOL-Algebra: theory HOL-Algebra.Coset
21:14:45 HOL-Algebra: theory HOL-Algebra.FiniteProduct
21:14:46 HOL-Algebra: theory HOL-Algebra.Ring
21:14:47 HOL-Algebra: theory HOL-Algebra.Group_Action
21:14:47 HOL-Algebra: theory HOL-Algebra.Left_Coset
21:14:47 HOL-Algebra: theory HOL-Algebra.SimpleGroups
21:14:47 HOL-Algebra: theory HOL-Algebra.SndIsomorphismGrp
21:14:48 HOL-Algebra: theory HOL-Algebra.Sylow
21:14:48 HOL-Algebra: theory HOL-Algebra.Generated_Groups
21:14:48 HOL-Algebra: theory HOL-Algebra.Divisibility
21:14:48 HOL-Algebra: theory HOL-Algebra.Zassenhaus
21:14:49 HOL-Algebra: theory HOL-Algebra.Solvable_Groups
21:14:49 HOL-Algebra: theory HOL-Algebra.Elementary_Groups
21:14:50 HOL-Algebra: theory HOL-Algebra.Sym_Groups
21:14:51 HOL-Algebra: theory HOL-Algebra.Exact_Sequence
21:14:51 HOL-Algebra: theory HOL-Algebra.Product_Groups
21:14:52 HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
21:14:52 HOL-Algebra: theory HOL-Algebra.AbelCoset
21:14:52 HOL-Algebra: theory HOL-Algebra.Module
21:14:57 HOL-Algebra: theory HOL-Algebra.Ideal
21:15:00 HOL-Algebra: theory HOL-Algebra.Ideal_Product
21:15:01 HOL-Algebra: theory HOL-Algebra.RingHom
21:15:02 HOL-Algebra: theory HOL-Algebra.QuotRing
21:15:02 HOL-Algebra: theory HOL-Algebra.UnivPoly
21:15:06 HOL-Algebra: theory HOL-Algebra.IntRing
21:15:06 HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
21:15:08 HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
21:15:18 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
21:15:23 HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
21:15:23 HOL-Algebra: theory HOL-Algebra.Subrings
21:15:26 HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
21:15:28 HOL-Algebra: theory HOL-Algebra.Generated_Rings
21:15:29 HOL-Algebra: theory HOL-Algebra.Generated_Fields
21:15:32 HOL-Algebra: theory HOL-Algebra.Polynomials
21:15:53 HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
21:16:37 HOL-Algebra: theory HOL-Algebra.Finite_Extensions
21:16:37 HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
21:16:51 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
21:17:00 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure_Type
21:17:00 HOL-Algebra: theory HOL-Algebra.Algebra
21:17:45 Preparing HOL-Algebra/document ...
21:18:13 Finished HOL-Algebra/document (0:00:28 elapsed time)
21:18:13 Preparing HOL-Algebra/outline ...
21:18:26 Finished HOL-Algebra/outline (0:00:13 elapsed time)
21:18:27 Timing HOL-Algebra (8 threads, 159.804s elapsed time, 805.162s cpu time, 92.757s GC time, factor 5.04)
21:18:27 Finished HOL-Algebra (0:03:07 elapsed time, 0:14:28 cpu time, factor 4.62)
21:18:27 Building Automatic_Refinement (on hpcisabelle/6) ...
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Foldi
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Prio_List
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
21:18:29 Automatic_Refinement: theory HOL-Eisbach.Eisbach
21:18:29 Automatic_Refinement: theory HOL-Library.Cancellation
21:18:29 Automatic_Refinement: theory HOL-Library.Infinite_Set
21:18:29 Automatic_Refinement: theory HOL-Library.Option_ord
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
21:18:29 Automatic_Refinement: theory Automatic_Refinement.Refine_Util
21:18:30 Automatic_Refinement: theory HOL-Library.Multiset
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Select_Solve
21:18:30 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
21:18:36 Automatic_Refinement: theory HOL-ex.Quicksort
21:18:37 Automatic_Refinement: theory Automatic_Refinement.Misc
21:18:44 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
21:18:46 Automatic_Refinement: theory Automatic_Refinement.Relators
21:18:46 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
21:18:47 Automatic_Refinement: theory Automatic_Refinement.Param_Tool
21:18:48 Automatic_Refinement: theory Automatic_Refinement.Param_HOL
21:18:48 Automatic_Refinement: theory Automatic_Refinement.Parametricity
21:18:49 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
21:18:49 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
21:18:49 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
21:18:49 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
21:18:50 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
21:18:51 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
21:18:51 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
21:18:51 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
21:18:51 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
21:18:51 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
21:18:52 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
21:18:56 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
21:19:06 Preparing Automatic_Refinement/document ...
21:19:10 Finished Automatic_Refinement/document (0:00:03 elapsed time)
21:19:10 Preparing Automatic_Refinement/outline ...
21:19:12 Finished Automatic_Refinement/outline (0:00:02 elapsed time)
21:19:12 Timing Automatic_Refinement (8 threads, 27.586s elapsed time, 119.623s cpu time, 3.610s GC time, factor 4.34)
21:19:12 Finished Automatic_Refinement (0:00:38 elapsed time, 0:02:19 cpu time, factor 3.65)
21:19:12 Building Refine_Monadic (on hpcisabelle/7) ...
21:19:14 Refine_Monadic: theory Refine_Monadic.Example_Chapter
21:19:14 Refine_Monadic: theory Refine_Monadic.Refine_Chapter
21:19:14 Refine_Monadic: theory HOL-Library.Adhoc_Overloading
21:19:14 Refine_Monadic: theory HOL-Library.Phantom_Type
21:19:14 Refine_Monadic: theory HOL-Library.While_Combinator
21:19:14 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
21:19:15 Refine_Monadic: theory HOL-Library.Monad_Syntax
21:19:15 Refine_Monadic: theory Refine_Monadic.Refine_Misc
21:19:15 Refine_Monadic: theory HOL-Library.Cardinality
21:19:15 Refine_Monadic: theory Refine_Monadic.RefineG_Domain
21:19:15 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
21:19:16 Refine_Monadic: theory Refine_Monadic.RefineG_Assert
21:19:16 Refine_Monadic: theory HOL-Library.Numeral_Type
21:19:17 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
21:19:17 Refine_Monadic: theory Refine_Monadic.RefineG_While
21:19:17 Refine_Monadic: theory Refine_Monadic.Refine_Basic
21:19:17 Refine_Monadic: theory HOL-Library.Type_Length
21:19:18 Refine_Monadic: theory Refine_Monadic.Refine_Det
21:19:18 Refine_Monadic: theory HOL-Library.Word
21:19:22 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
21:19:22 Refine_Monadic: theory Refine_Monadic.Refine_Leof
21:19:22 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
21:19:22 Refine_Monadic: theory Refine_Monadic.Refine_Pfun
21:19:23 Refine_Monadic: theory Refine_Monadic.Refine_While
21:19:25 Refine_Monadic: theory Refine_Monadic.Refine_Transfer
21:19:25 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
21:19:25 Refine_Monadic: theory Refine_Monadic.Refine_Automation
21:19:25 Refine_Monadic: theory Refine_Monadic.Refine_Foreach
21:19:29 Refine_Monadic: theory Refine_Monadic.Refine_Monadic
21:19:30 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
21:19:30 Refine_Monadic: theory Refine_Monadic.WordRefine
21:19:31 Refine_Monadic: theory Refine_Monadic.Examples
21:20:04 Preparing Refine_Monadic/document ...
21:20:15 Finished Refine_Monadic/document (0:00:10 elapsed time)
21:20:15 Preparing Refine_Monadic/outline ...
21:20:23 Finished Refine_Monadic/outline (0:00:07 elapsed time)
21:20:23 Timing Refine_Monadic (8 threads, 39.263s elapsed time, 174.773s cpu time, 4.510s GC time, factor 4.45)
21:20:23 Finished Refine_Monadic (0:00:50 elapsed time, 0:03:18 cpu time, factor 3.89)
21:20:23 Building Collections (on hpcisabelle/0) ...
21:20:25 Collections: theory Collections.ICF_Tools
21:20:25 Collections: theory Collections.Partial_Equivalence_Relation
21:20:25 Collections: theory Finger-Trees.FingerTree
21:20:25 Collections: theory Binomial-Heaps.BinomialHeap
21:20:25 Collections: theory Binomial-Heaps.SkewBinomialHeap
21:20:25 Collections: theory HOL-Library.AList
21:20:25 Collections: theory HOL-Library.Code_Abstract_Nat
21:20:25 Collections: theory HOL-Library.Code_Target_Int
21:20:25 Collections: theory HOL-Library.Code_Target_Nat
21:20:25 Collections: theory Collections.Ord_Code_Preproc
21:20:25 Collections: theory HOL-Library.Confluence
21:20:25 Collections: theory Collections.Locale_Code
21:20:25 Collections: theory Collections.Record_Intf
21:20:25 Collections: theory HOL-Library.Confluent_Quotient
21:20:25 Collections: theory HOL-Library.Code_Target_Numeral
21:20:26 Collections: theory Collections.SetIterator
21:20:26 Collections: theory Collections.Sorted_List_Operations
21:20:26 Collections: theory HOL-Library.Dlist
21:20:26 Collections: theory Word_Lib.Bit_Comprehension
21:20:27 Collections: theory Word_Lib.More_Divides
21:20:27 Collections: theory HOL-Library.RBT_Impl
21:20:27 Collections: theory HOL-Library.Signed_Division
21:20:27 Collections: theory Collections.DatRef
21:20:28 Collections: theory Collections.Idx_Iterator
21:20:28 Collections: theory Collections.SetAbstractionIterator
21:20:28 Collections: theory Collections.SetIteratorOperations
21:20:29 Collections: theory Word_Lib.Signed_Division_Word
21:20:29 Collections: theory Native_Word.Code_Int_Integer_Conversion
21:20:29 Collections: theory Word_Lib.More_Arithmetic
21:20:29 Collections: theory Word_Lib.More_Bit_Ring
21:20:30 Collections: theory Word_Lib.More_Word
21:20:32 Collections: theory Collections.Assoc_List
21:20:32 Collections: theory Collections.Dlist_add
21:20:32 Collections: theory Collections.Proper_Iterator
21:20:32 Collections: theory Collections.SetIteratorGA
21:20:34 Collections: theory Collections.Diff_Array
21:20:34 Collections: theory Native_Word.Code_Target_Word_Base
21:20:34 Collections: theory Collections.It_to_It
21:20:34 Collections: theory Collections.Gen_Iterator
21:20:34 Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
21:20:34 Collections: theory Word_Lib.Least_significant_bit
21:20:35 Collections: theory Collections.Iterator
21:20:36 Collections: theory Collections.ICF_Spec_Base
21:20:36 Collections: theory Collections.MapSpec
21:20:36 Collections: theory Word_Lib.Most_significant_bit
21:20:37 Collections: theory Word_Lib.Generic_set_bit
21:20:38 Collections: theory Native_Word.Code_Target_Integer_Bit
21:20:38 Collections: theory Native_Word.Word_Type_Copies
21:20:41 Collections: theory Collections.Robdd
21:20:53 Collections: theory Native_Word.Code_Target_Int_Bit
21:20:53 Collections: theory Native_Word.Uint32
21:20:53 Collections: theory Collections.Code_Target_ICF
21:20:54 Collections: theory Collections.Locale_Code_Ex
21:20:55 Collections: theory Collections.HashCode
21:21:39 Collections: theory Collections.RBT_add
21:22:17 Collections: theory Collections.GenCF_Impl_Chapter
21:22:17 Collections: theory Collections.GenCF_Gen_Chapter
21:22:17 Collections: theory Collections.GenCF_Chapter
21:22:17 Collections: theory Collections.GenCF_Intf_Chapter
21:22:17 Collections: theory Collections.Impl_Array_Stack
21:22:17 Collections: theory Collections.Intf_Comp
21:22:17 Collections: theory Collections.Array_Iterator
21:22:17 Collections: theory HOL-Library.Product_Lexorder
21:22:17 Collections: theory Collections.Intf_Map
21:22:17 Collections: theory Collections.Intf_Set
21:22:17 Collections: theory Collections.Intf_Hash
21:22:18 Collections: theory Collections.Gen_Map
21:22:18 Collections: theory Collections.Gen_Set
21:22:18 Collections: theory Collections.Impl_Cfun_Set
21:22:18 Collections: theory Collections.Impl_List_Set
21:22:20 Collections: theory Collections.Gen_Comp
21:22:20 Collections: theory Collections.Impl_Array_Map
21:22:20 Collections: theory Collections.Impl_List_Map
21:22:20 Collections: theory Collections.Impl_RBT_Map
21:22:20 Collections: theory Collections.Gen_Map2Set
21:22:21 Collections: theory Collections.Impl_Array_Hash_Map
21:22:32 Collections: theory Collections.Impl_Bit_Set
21:22:32 Collections: theory Native_Word.Uint
21:22:32 Collections: theory Collections.Gen_Hash
21:22:37 Collections: theory Collections.Impl_Uv_Set
21:22:52 Collections: theory Collections.GenCF
21:22:56 Collections: theory Collections.ICF_Chapter
21:22:56 Collections: theory Collections.ICF_Gen_Algo_Chapter
21:22:56 Collections: theory Collections.ICF_Impl_Chapter
21:22:56 Collections: theory Collections.ICF_Spec_Chapter
21:22:56 Collections: theory Trie.Trie
21:22:56 Collections: theory Collections.ListSpec
21:22:56 Collections: theory HOL-Library.RBT
21:22:56 Collections: theory Collections.AnnotatedListSpec
21:22:56 Collections: theory Collections.PrioSpec
21:22:56 Collections: theory Collections.PrioUniqueSpec
21:22:56 Collections: theory Collections.SetSpec
21:23:00 Collections: theory Collections.BinoPrioImpl
21:23:00 Collections: theory Collections.SkewPrioImpl
21:23:01 Collections: theory Collections.ListGA
21:23:01 Collections: theory Collections.Trie_Impl
21:23:01 Collections: theory Collections.FTAnnotatedListImpl
21:23:02 Collections: theory Collections.PrioByAnnotatedList
21:23:02 Collections: theory Collections.PrioUniqueByAnnotatedList
21:23:02 Collections: theory Collections.Fifo
21:23:02 Collections: theory Collections.Trie2
21:23:03 Collections: theory Collections.Algos
21:23:03 Collections: theory Collections.SetIndex
21:23:04 Collections: theory Collections.SetIteratorCollectionsGA
21:23:05 Collections: theory Collections.MapGA
21:23:05 Collections: theory Collections.SetGA
21:23:07 Collections: theory Collections.FTPrioImpl
21:23:07 Collections: theory Collections.FTPrioUniqueImpl
21:23:07 Collections: theory Collections.ArrayMapImpl
21:23:07 Collections: theory Collections.ListMapImpl
21:23:07 Collections: theory Collections.ListMapImpl_Invar
21:23:08 Collections: theory Collections.TrieMapImpl
21:23:10 Collections: theory Collections.ListSetImpl
21:23:11 Collections: theory Collections.ListSetImpl_Invar
21:23:11 Collections: theory Collections.ListSetImpl_NotDist
21:23:11 Collections: theory Collections.ListSetImpl_Sorted
21:23:12 Collections: theory Collections.SetByMap
21:23:13 Collections: theory Collections.RBTMapImpl
21:23:13 Collections: theory Collections.ArrayHashMap_Impl
21:23:15 Collections: theory Collections.ArraySetImpl
21:23:16 Collections: theory Collections.TrieSetImpl
21:23:17 Collections: theory Collections.ArrayHashMap
21:23:20 Collections: theory Collections.RBTSetImpl
21:23:20 Collections: theory Collections.HashMap_Impl
21:23:22 Collections: theory Collections.HashMap
21:23:24 Collections: theory Collections.ArrayHashSet
21:23:28 Collections: theory Collections.HashSet
21:23:28 Collections: theory Collections.MapStdImpl
21:23:34 Collections: theory Collections.SetStdImpl
21:23:39 Collections: theory Collections.ICF_Impl
21:23:43 Collections: theory Collections.ICF_Refine_Monadic
21:23:44 Collections: theory Collections.ICF_Autoref
21:23:48 Collections: theory Collections.Userguides_Chapter
21:23:48 Collections: theory Collections.Collections_Entrypoints_Chapter
21:23:48 Collections: theory Collections.ICF_Entrypoints_Chapter
21:23:48 Collections: theory Collections.Collections
21:23:48 Collections: theory Collections.Refine_Dflt
21:23:49 Collections: theory Collections.CollectionsV1
21:23:49 Collections: theory Collections.ICF_Userguide
21:23:49 Collections: theory Collections.Refine_Dflt_ICF
21:23:49 Collections: theory Collections.Refine_Dflt_Only_ICF
21:23:49 Collections: theory Collections.Refine_Monadic_Userguide
21:25:14 Preparing Collections/document ...
21:25:34 Finished Collections/document (0:00:19 elapsed time)
21:25:34 Preparing Collections/outline ...
21:25:46 Finished Collections/outline (0:00:12 elapsed time)
21:25:46 Preparing Collections/userguide ...
21:25:49 Finished Collections/userguide (0:00:03 elapsed time)
21:25:50 Timing Collections (8 threads, 228.711s elapsed time, 1036.472s cpu time, 76.521s GC time, factor 4.53)
21:25:50 Finished Collections (0:04:47 elapsed time, 0:19:43 cpu time, factor 4.11)
21:25:50 Building Jordan_Normal_Form (on hpcisabelle/1) ...
21:25:52 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
21:25:53 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
21:26:00 Jordan_Normal_Form: theory Containers.Equal
21:26:00 Jordan_Normal_Form: theory Containers.Extend_Partial_Order
21:26:00 Jordan_Normal_Form: theory Containers.List_Fusion
21:26:00 Jordan_Normal_Form: theory Deriving.Derive_Manager
21:26:00 Jordan_Normal_Form: theory Deriving.Comparator
21:26:00 Jordan_Normal_Form: theory Deriving.Generator_Aux
21:26:00 Jordan_Normal_Form: theory Containers.Containers_Auxiliary
21:26:00 Jordan_Normal_Form: theory Abstract-Rewriting.Seq
21:26:01 Jordan_Normal_Form: theory Containers.Closure_Set
21:26:01 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
21:26:01 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
21:26:01 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
21:26:01 Jordan_Normal_Form: theory Deriving.Equality_Generator
21:26:01 Jordan_Normal_Form: theory Containers.Containers_Generator
21:26:01 Jordan_Normal_Form: theory Regular-Sets.Regular_Set
21:26:02 Jordan_Normal_Form: theory Deriving.Equality_Instances
21:26:02 Jordan_Normal_Form: theory Show.Show
21:26:02 Jordan_Normal_Form: theory Containers.Collection_Enum
21:26:02 Jordan_Normal_Form: theory Deriving.Compare
21:26:02 Jordan_Normal_Form: theory Deriving.Comparator_Generator
21:26:03 Jordan_Normal_Form: theory Containers.Lexicographic_Order
21:26:03 Jordan_Normal_Form: theory Containers.Collection_Eq
21:26:03 Jordan_Normal_Form: theory Containers.RBT_ext
21:26:03 Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl
21:26:04 Jordan_Normal_Form: theory Deriving.Compare_Generator
21:26:04 Jordan_Normal_Form: theory Containers.Set_Linorder
21:26:04 Jordan_Normal_Form: theory Containers.DList_Set
21:26:04 Jordan_Normal_Form: theory Deriving.Compare_Instances
21:26:04 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
21:26:04 Jordan_Normal_Form: theory Show.Show_Instances
21:26:05 Jordan_Normal_Form: theory Regular-Sets.Regular_Exp
21:26:06 Jordan_Normal_Form: theory VectorSpace.FunctionLemmas
21:26:06 Jordan_Normal_Form: theory Show.Shows_Literal
21:26:06 Jordan_Normal_Form: theory VectorSpace.RingModuleFacts
21:26:06 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
21:26:06 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
21:26:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
21:26:07 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
21:26:07 Jordan_Normal_Form: theory VectorSpace.MonoidSums
21:26:07 Jordan_Normal_Form: theory VectorSpace.LinearCombinations
21:26:09 Jordan_Normal_Form: theory Regular-Sets.NDerivative
21:26:09 Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation
21:26:14 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
21:26:14 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
21:26:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
21:26:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
21:26:16 Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking
21:26:16 Jordan_Normal_Form: theory Jordan_Normal_Form.Shows_Literal_Matrix
21:26:16 Jordan_Normal_Form: theory VectorSpace.SumSpaces
21:26:16 Jordan_Normal_Form: theory Regular-Sets.Regexp_Method
21:26:16 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
21:26:17 Jordan_Normal_Form: theory VectorSpace.VectorSpace
21:26:17 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
21:26:17 Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting
21:26:17 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
21:26:18 Jordan_Normal_Form: theory Containers.Collection_Order
21:26:20 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders
21:26:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
21:26:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
21:26:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
21:26:21 Jordan_Normal_Form: theory Containers.RBT_Mapping2
21:26:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
21:26:22 Jordan_Normal_Form: theory Containers.RBT_Set2
21:26:23 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier
21:26:23 Jordan_Normal_Form: theory Matrix.Ordered_Semiring
21:26:24 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
21:26:24 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
21:26:25 Jordan_Normal_Form: theory Containers.Set_Impl
21:26:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
21:26:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
21:26:28 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
21:26:32 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
21:26:41 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
21:26:41 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
21:26:43 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
21:26:45 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
21:26:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
21:26:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
21:26:51 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
21:26:53 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
21:26:53 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
21:30:15 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
21:30:15 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
21:30:15 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
21:30:18 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
21:30:28 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
21:31:14 Preparing Jordan_Normal_Form/document ...
21:31:40 Finished Jordan_Normal_Form/document (0:00:26 elapsed time)
21:31:40 Preparing Jordan_Normal_Form/outline ...
21:31:51 Finished Jordan_Normal_Form/outline (0:00:10 elapsed time)
21:31:51 Timing Jordan_Normal_Form (8 threads, 277.705s elapsed time, 1747.736s cpu time, 80.014s GC time, factor 6.29)
21:31:51 Finished Jordan_Normal_Form (0:05:19 elapsed time, 0:30:46 cpu time, factor 5.77)
21:31:52 Building Core_SC_DOM (on hpcisabelle/2) ...
21:32:07 Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
21:32:07 Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
21:32:07 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
21:32:08 Core_SC_DOM: theory Core_SC_DOM.Ref
21:32:08 Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
21:32:08 Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
21:32:08 Core_SC_DOM: theory Core_SC_DOM.BaseClass
21:32:09 Core_SC_DOM: theory Core_SC_DOM.NodePointer
21:32:09 Core_SC_DOM: theory Core_SC_DOM.ObjectClass
21:32:09 Core_SC_DOM: theory Core_SC_DOM.ElementPointer
21:32:10 Core_SC_DOM: theory Core_SC_DOM.NodeClass
21:32:10 Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
21:32:11 Core_SC_DOM: theory Core_SC_DOM.BaseMonad
21:32:12 Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
21:32:13 Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
21:32:13 Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
21:32:14 Core_SC_DOM: theory Core_SC_DOM.ElementClass
21:32:14 Core_SC_DOM: theory Core_SC_DOM.NodeMonad
21:32:16 Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
21:32:16 Core_SC_DOM: theory Core_SC_DOM.ElementMonad
21:32:17 Core_SC_DOM: theory Core_SC_DOM.DocumentClass
21:32:17 Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
21:32:19 Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
21:32:20 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
21:32:41 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
21:33:01 Core_SC_DOM: theory Core_SC_DOM.Core_DOM
21:33:01 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
21:33:09 Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
21:33:09 Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
21:33:09 Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
21:33:09 Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
21:33:12 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
21:35:31 Preparing Core_SC_DOM/document ...
21:35:47 Finished Core_SC_DOM/document (0:00:16 elapsed time)
21:35:47 Preparing Core_SC_DOM/outline ...
21:35:58 Finished Core_SC_DOM/outline (0:00:11 elapsed time)
21:35:58 Timing Core_SC_DOM (8 threads, 159.041s elapsed time, 857.966s cpu time, 55.861s GC time, factor 5.39)
21:35:58 Finished Core_SC_DOM (0:03:37 elapsed time, 0:16:44 cpu time, factor 4.61)
21:35:58 Building HOL-Probability (on hpcisabelle/3) ...
21:36:01 HOL-Probability: theory HOL-Library.Adhoc_Overloading
21:36:01 HOL-Probability: theory HOL-Library.AList
21:36:01 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
21:36:01 HOL-Probability: theory HOL-Library.Stream
21:36:01 HOL-Probability: theory HOL-Library.Conditional_Parametricity
21:36:01 HOL-Probability: theory HOL-Library.Sublist
21:36:01 HOL-Probability: theory HOL-Library.Tree
21:36:01 HOL-Probability: theory HOL-Library.Rewrite
21:36:01 HOL-Probability: theory HOL-Library.Monad_Syntax
21:36:02 HOL-Probability: theory HOL-Library.FSet
21:36:02 HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
21:36:02 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
21:36:03 HOL-Probability: theory HOL-Probability.Discrete_Topology
21:36:03 HOL-Probability: theory HOL-Probability.Essential_Supremum
21:36:03 HOL-Probability: theory HOL-Probability.Probability_Measure
21:36:03 HOL-Probability: theory HOL-Probability.Stopping_Time
21:36:03 HOL-Probability: theory HOL-Library.Mapping
21:36:05 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:36:06 HOL-Probability: theory HOL-Probability.Tree_Space
21:36:06 HOL-Probability: theory HOL-Library.AList_Mapping
21:36:06 HOL-Probability: theory HOL-Probability.Conditional_Expectation
21:36:06 HOL-Probability: theory HOL-Probability.Distribution_Functions
21:36:06 HOL-Probability: theory HOL-Probability.Giry_Monad
21:36:06 HOL-Probability: theory HOL-Probability.Weak_Convergence
21:36:07 HOL-Probability: theory HOL-Probability.Helly_Selection
21:36:08 HOL-Probability: theory HOL-Library.Finite_Map
21:36:08 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
21:36:08 HOL-Probability: theory HOL-Probability.Projective_Family
21:36:09 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
21:36:10 HOL-Probability: theory HOL-Probability.Independent_Family
21:36:10 HOL-Probability: theory HOL-Probability.Stream_Space
21:36:11 HOL-Probability: theory HOL-Probability.PMF_Impl
21:36:11 HOL-Probability: theory HOL-Probability.Random_Permutations
21:36:11 HOL-Probability: theory HOL-Probability.SPMF
21:36:11 HOL-Probability: theory HOL-Probability.Convolution
21:36:11 HOL-Probability: theory HOL-Probability.Information
21:36:11 HOL-Probability: theory HOL-Probability.Product_PMF
21:36:13 HOL-Probability: theory HOL-Probability.Hoeffding
21:36:14 HOL-Probability: theory HOL-Probability.Distributions
21:36:16 HOL-Probability: theory HOL-Probability.Characteristic_Functions
21:36:16 HOL-Probability: theory HOL-Probability.Sinc_Integral
21:36:17 HOL-Probability: theory HOL-Probability.Levy
21:36:18 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
21:36:22 HOL-Probability: theory HOL-Probability.Fin_Map
21:36:24 HOL-Probability: theory HOL-Probability.Projective_Limit
21:36:26 HOL-Probability: theory HOL-Probability.Probability
21:37:39 Preparing HOL-Probability/document ...
21:38:00 Finished HOL-Probability/document (0:00:21 elapsed time)
21:38:00 Preparing HOL-Probability/outline ...
21:38:08 Finished HOL-Probability/outline (0:00:07 elapsed time)
21:38:08 Timing HOL-Probability (8 threads, 73.127s elapsed time, 500.104s cpu time, 13.289s GC time, factor 6.84)
21:38:08 Finished HOL-Probability (0:01:37 elapsed time, 0:09:10 cpu time, factor 5.65)
21:38:08 Building HOL-Number_Theory (on hpcisabelle/4) ...
21:38:11 HOL-Number_Theory: theory HOL-Number_Theory.Cong
21:38:11 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
21:38:11 HOL-Number_Theory: theory HOL-Algebra.Congruence
21:38:11 HOL-Number_Theory: theory HOL-Number_Theory.Fib
21:38:11 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
21:38:12 HOL-Number_Theory: theory HOL-Algebra.Order
21:38:13 HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
21:38:13 HOL-Number_Theory: theory HOL-Number_Theory.Totient
21:38:14 HOL-Number_Theory: theory HOL-Algebra.Lattice
21:38:15 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
21:38:16 HOL-Number_Theory: theory HOL-Algebra.Group
21:38:19 HOL-Number_Theory: theory HOL-Algebra.Coset
21:38:19 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
21:38:20 HOL-Number_Theory: theory HOL-Algebra.Ring
21:38:22 HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
21:38:23 HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
21:38:25 HOL-Number_Theory: theory HOL-Algebra.AbelCoset
21:38:25 HOL-Number_Theory: theory HOL-Algebra.Module
21:38:29 HOL-Number_Theory: theory HOL-Algebra.Ideal
21:38:33 HOL-Number_Theory: theory HOL-Algebra.RingHom
21:38:34 HOL-Number_Theory: theory HOL-Algebra.UnivPoly
21:38:48 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
21:38:52 HOL-Number_Theory: theory HOL-Number_Theory.Residues
21:38:55 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
21:38:55 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
21:38:56 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
21:38:56 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
21:38:56 HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
21:38:57 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
21:39:27 Preparing HOL-Number_Theory/document ...
21:39:33 Finished HOL-Number_Theory/document (0:00:05 elapsed time)
21:39:33 Preparing HOL-Number_Theory/outline ...
21:39:36 Finished HOL-Number_Theory/outline (0:00:02 elapsed time)
21:39:36 Timing HOL-Number_Theory (8 threads, 58.802s elapsed time, 334.847s cpu time, 10.435s GC time, factor 5.69)
21:39:36 Finished HOL-Number_Theory (0:01:16 elapsed time, 0:06:10 cpu time, factor 4.82)
21:39:36 Building Bounded_Deducibility_Security (on hpcisabelle/5) ...
21:39:37 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Abstract_BD_Security
21:39:37 Bounded_Deducibility_Security: theory HOL-Library.Sublist
21:39:40 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Trivia
21:39:41 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Filtermap
21:39:41 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Transition_System
21:39:42 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_TS
21:39:42 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.IO_Automaton
21:39:43 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Triggers
21:39:44 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_IO
21:39:45 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Unwinding
21:39:45 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Compositional_Reasoning
21:39:46 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Bounded_Deducibility_Security
21:39:55 Preparing Bounded_Deducibility_Security/document ...
21:39:59 Finished Bounded_Deducibility_Security/document (0:00:03 elapsed time)
21:39:59 Preparing Bounded_Deducibility_Security/outline ...
21:40:02 Finished Bounded_Deducibility_Security/outline (0:00:03 elapsed time)
21:40:02 Timing Bounded_Deducibility_Security (8 threads, 9.734s elapsed time, 44.636s cpu time, 1.242s GC time, factor 4.59)
21:40:02 Finished Bounded_Deducibility_Security (0:00:18 elapsed time, 0:01:00 cpu time, factor 3.28)
21:40:02 Building BD_Security_Compositional (on hpcisabelle/6) ...
21:40:03 BD_Security_Compositional: theory BD_Security_Compositional.Transporting_Security
21:40:03 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security
21:40:03 BD_Security_Compositional: theory BD_Security_Compositional.Trivial_Security
21:40:03 BD_Security_Compositional: theory BD_Security_Compositional.Independent_Secrets
21:40:13 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security_Network
21:41:13 Preparing BD_Security_Compositional/document ...
21:41:18 Finished BD_Security_Compositional/document (0:00:05 elapsed time)
21:41:18 Preparing BD_Security_Compositional/outline ...
21:41:22 Finished BD_Security_Compositional/outline (0:00:03 elapsed time)
21:41:22 Timing BD_Security_Compositional (8 threads, 55.957s elapsed time, 197.783s cpu time, 5.345s GC time, factor 3.53)
21:41:22 Finished BD_Security_Compositional (0:01:10 elapsed time, 0:03:49 cpu time, factor 3.24)
21:41:22 Building Expander_Graphs (on hpcisabelle/7) ...
21:41:27 Expander_Graphs: theory Graph_Theory.Rtrancl_On
21:41:27 Expander_Graphs: theory HOL-Eisbach.Eisbach
21:41:27 Expander_Graphs: theory Digit_Expansions.Bits_Digits
21:41:27 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
21:41:27 Expander_Graphs: theory HOL-Decision_Procs.Dense_Linear_Order
21:41:27 Expander_Graphs: theory HOL-Library.Code_Abstract_Nat
21:41:27 Expander_Graphs: theory HOL-Library.Code_Target_Int
21:41:27 Expander_Graphs: theory HOL-Algebra.Congruence
21:41:28 Expander_Graphs: theory HOL-Library.Code_Target_Nat
21:41:28 Expander_Graphs: theory Finite_Fields.Finite_Fields_More_Bijections
21:41:28 Expander_Graphs: theory HOL-Combinatorics.List_Permutation
21:41:28 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
21:41:28 Expander_Graphs: theory HOL-Library.Code_Target_Numeral
21:41:28 Expander_Graphs: theory HOL-Library.Function_Algebras
21:41:28 Expander_Graphs: theory Abstract-Rewriting.Seq
21:41:28 Expander_Graphs: theory HOL-Library.More_List
21:41:28 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
21:41:29 Expander_Graphs: theory HOL-Library.While_Combinator
21:41:29 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
21:41:29 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
21:41:29 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
21:41:29 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
21:41:30 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
21:41:30 Expander_Graphs: theory HOL-Algebra.Order
21:41:30 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
21:41:30 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
21:41:30 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
21:41:30 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
21:41:30 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
21:41:31 Expander_Graphs: theory HOL-Library.Lattice_Algebras
21:41:31 Expander_Graphs: theory HOL-Library.Log_Nat
21:41:31 Expander_Graphs: theory HOL-Algebra.Lattice
21:41:31 Expander_Graphs: theory Graph_Theory.Stuff
21:41:31 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families
21:41:31 Expander_Graphs: theory Graph_Theory.Digraph
21:41:32 Expander_Graphs: theory Ergodic_Theory.SG_Library_Complement
21:41:32 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
21:41:32 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
21:41:32 Expander_Graphs: theory HOL-Algebra.Complete_Lattice
21:41:33 Expander_Graphs: theory Matrix.Utility
21:41:33 Expander_Graphs: theory Lp.Functional_Spaces
21:41:33 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
21:41:34 Expander_Graphs: theory Graph_Theory.Arc_Walk
21:41:34 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
21:41:34 Expander_Graphs: theory HOL-Algebra.Group
21:41:34 Expander_Graphs: theory Regular-Sets.Regular_Set
21:41:36 Expander_Graphs: theory Graph_Theory.Pair_Digraph
21:41:36 Expander_Graphs: theory VectorSpace.FunctionLemmas
21:41:36 Expander_Graphs: theory HOL-Algebra.Coset
21:41:36 Expander_Graphs: theory HOL-Algebra.FiniteProduct
21:41:36 Expander_Graphs: theory Lp.Lp
21:41:37 Expander_Graphs: theory HOL-Algebra.Ring
21:41:38 Expander_Graphs: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
21:41:38 Expander_Graphs: theory HOL-Library.Interval
21:41:38 Expander_Graphs: theory HOL-Library.Float
21:41:38 Expander_Graphs: theory HOL-Algebra.Generated_Groups
21:41:38 Expander_Graphs: theory HOL-Algebra.Divisibility
21:41:41 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
21:41:41 Expander_Graphs: theory HOL-Algebra.Elementary_Groups
21:41:43 Expander_Graphs: theory Regular-Sets.Regular_Exp
21:41:43 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
21:41:43 Expander_Graphs: theory HOL-Library.Interval_Float
21:41:43 Expander_Graphs: theory Universal_Hash_Families.Pseudorandom_Objects
21:41:43 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
21:41:44 Expander_Graphs: theory HOL-Algebra.AbelCoset
21:41:44 Expander_Graphs: theory HOL-Algebra.Module
21:41:44 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
21:41:44 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:41:44 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
21:41:44 Expander_Graphs: theory HOL-Decision_Procs.Approximation_Bounds
21:41:45 Expander_Graphs: theory Graph_Theory.Digraph_Component
21:41:46 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
21:41:46 Expander_Graphs: theory VectorSpace.RingModuleFacts
21:41:46 Expander_Graphs: theory Regular-Sets.NDerivative
21:41:46 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
21:41:47 Expander_Graphs: theory VectorSpace.MonoidSums
21:41:47 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
21:41:47 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
21:41:47 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
21:41:47 Expander_Graphs: theory VectorSpace.LinearCombinations
21:41:48 Expander_Graphs: theory HOL-Algebra.Ideal
21:41:50 Expander_Graphs: theory Jordan_Normal_Form.Matrix
21:41:50 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
21:41:50 Expander_Graphs: theory HOL-Decision_Procs.Approximation
21:41:51 Expander_Graphs: theory HOL-Algebra.RingHom
21:41:52 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
21:41:52 Expander_Graphs: theory Regular-Sets.Regexp_Method
21:41:53 Expander_Graphs: theory HOL-Algebra.QuotRing
21:41:53 Expander_Graphs: theory HOL-Algebra.UnivPoly
21:41:53 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
21:41:55 Expander_Graphs: theory VectorSpace.SumSpaces
21:41:56 Expander_Graphs: theory VectorSpace.VectorSpace
21:41:56 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
21:41:56 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
21:41:56 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
21:41:58 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
21:41:58 Expander_Graphs: theory Jordan_Normal_Form.Determinant
21:41:59 Expander_Graphs: theory Matrix.Ordered_Semiring
21:42:01 Expander_Graphs: theory Matrix.Matrix_Legacy
21:42:01 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
21:42:02 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
21:42:02 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
21:42:03 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
21:42:03 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
21:42:03 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
21:42:03 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
21:42:06 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
21:42:06 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
21:42:07 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
21:42:08 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
21:42:10 Expander_Graphs: theory HOL-Algebra.Multiplicative_Group
21:42:15 Expander_Graphs: theory HOL-Algebra.Ring_Divisibility
21:42:15 Expander_Graphs: theory HOL-Algebra.Subrings
21:42:19 Expander_Graphs: theory HOL-Algebra.Embedded_Algebras
21:42:21 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
21:42:23 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
21:42:25 Expander_Graphs: theory HOL-Algebra.Polynomials
21:42:28 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
21:42:34 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
21:42:34 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
21:42:34 Expander_Graphs: theory QHLProver.Complex_Matrix
21:42:40 Expander_Graphs: theory QHLProver.Gates
21:42:40 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
21:42:49 Expander_Graphs: theory HOL-Algebra.Polynomial_Divisibility
21:42:51 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
21:42:53 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
21:42:54 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
21:43:22 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
21:43:22 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
21:43:33 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
21:43:36 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
21:43:40 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
21:43:40 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
21:43:41 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
21:43:44 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
21:43:50 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
21:43:50 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
21:43:54 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
21:43:57 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
21:44:04 Expander_Graphs: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
21:52:24 Preparing Expander_Graphs/document ...
21:52:36 Finished Expander_Graphs/document (0:00:12 elapsed time)
21:52:36 Preparing Expander_Graphs/outline ...
21:52:41 Finished Expander_Graphs/outline (0:00:04 elapsed time)
21:52:41 Timing Expander_Graphs (8 threads, 590.580s elapsed time, 2813.849s cpu time, 217.139s GC time, factor 4.76)
21:52:41 Finished Expander_Graphs (0:10:52 elapsed time, 0:49:23 cpu time, factor 4.54)
21:52:41 Running Crypto_Standards (on hpcisabelle/0) ...
21:52:44 Crypto_Standards: theory Crypto_Standards.More_Bit_Operations_Nat
21:52:44 Crypto_Standards: theory HOL-Decision_Procs.Conversions
21:52:44 Crypto_Standards: theory HOL-Decision_Procs.Algebra_Aux
21:52:44 Crypto_Standards: theory Crypto_Standards.Words
21:52:46 Crypto_Standards: theory Crypto_Standards.More_Residues
21:52:46 Crypto_Standards: theory HOL-Decision_Procs.Commutative_Ring
21:52:47 Crypto_Standards: theory Crypto_Standards.FIPS180_4
21:52:47 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2
21:52:54 Crypto_Standards: theory Crypto_Standards.FIPS180_4_Test_Vectors
21:52:57 Crypto_Standards: theory Crypto_Standards.Efficient_Mod_Exp
21:52:57 Crypto_Standards: theory HOL-Decision_Procs.Reflective_Field
21:52:57 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Interpretations
21:53:00 Crypto_Standards: theory Crypto_Standards.FIPS198_1
21:53:01 Crypto_Standards: theory Crypto_Standards.FIPS198_1_Test_Vectors
21:53:03 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Test_Vectors
21:53:09 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Locale
21:53:14 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Test
21:53:20 Crypto_Standards: theory Crypto_Standards.EC_Common
21:53:30 Crypto_Standards: theory Crypto_Standards.SEC1v2_0
21:53:47 Crypto_Standards: theory Crypto_Standards.Crypto_Standards
21:53:47 Crypto_Standards: theory Crypto_Standards.Efficient_SEC1
21:53:55 Crypto_Standards: theory Crypto_Standards.FIPS186_4_Curves
21:54:28 Crypto_Standards: theory Crypto_Standards.SEC1v2_0_Test_Vectors
22:00:09 Crypto_Standards: theory Crypto_Standards.Test_Vectors
22:07:14 Preparing Crypto_Standards/document ...
22:07:18 Finished Crypto_Standards/document (0:00:03 elapsed time)
22:07:18 Preparing Crypto_Standards/outline ...
22:07:20 Finished Crypto_Standards/outline (0:00:01 elapsed time)
22:07:20 Timing Crypto_Standards (8 threads, 865.976s elapsed time, 6464.870s cpu time, 557.957s GC time, factor 7.47)
22:07:20 Finished Crypto_Standards (0:14:29 elapsed time, 1:47:53 cpu time, factor 7.44)
22:07:20 Building Abstract-Rewriting (on hpcisabelle/1) ...
22:07:24 Abstract-Rewriting: theory Regular-Sets.Regular_Set
22:07:24 Abstract-Rewriting: theory Abstract-Rewriting.Seq
22:07:28 Abstract-Rewriting: theory Regular-Sets.Regular_Exp
22:07:31 Abstract-Rewriting: theory Regular-Sets.NDerivative
22:07:31 Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
22:07:35 Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
22:07:36 Abstract-Rewriting: theory Regular-Sets.Regexp_Method
22:07:36 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
22:07:38 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
22:07:38 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
22:07:42 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
22:08:00 Preparing Abstract-Rewriting/document ...
22:08:09 Finished Abstract-Rewriting/document (0:00:08 elapsed time)
22:08:09 Preparing Abstract-Rewriting/outline ...
22:08:13 Finished Abstract-Rewriting/outline (0:00:04 elapsed time)
22:08:13 Timing Abstract-Rewriting (8 threads, 24.980s elapsed time, 87.000s cpu time, 2.518s GC time, factor 3.48)
22:08:13 Finished Abstract-Rewriting (0:00:39 elapsed time, 0:01:53 cpu time, factor 2.89)
22:08:13 Running X86_Semantics (on hpcisabelle/2) ...
22:08:14 X86_Semantics: theory HOL-Eisbach.Eisbach
22:08:14 X86_Semantics: theory HOL-Library.Phantom_Type
22:08:14 X86_Semantics: theory Word_Lib.Even_More_List
22:08:14 X86_Semantics: theory Word_Lib.More_Bit_Ring
22:08:14 X86_Semantics: theory HOL-Library.Sublist
22:08:16 X86_Semantics: theory HOL-Library.Cardinality
22:08:17 X86_Semantics: theory HOL-Library.Numeral_Type
22:08:18 X86_Semantics: theory HOL-Library.Type_Length
22:08:19 X86_Semantics: theory Word_Lib.More_Arithmetic
22:08:19 X86_Semantics: theory HOL-Library.Word
22:08:28 X86_Semantics: theory Word_Lib.Bit_Comprehension
22:08:28 X86_Semantics: theory Word_Lib.Legacy_Aliases
22:08:28 X86_Semantics: theory Word_Lib.More_Divides
22:08:28 X86_Semantics: theory Word_Lib.Syntax_Bundles
22:08:29 X86_Semantics: theory Word_Lib.More_Word
22:08:31 X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:08:31 X86_Semantics: theory Word_Lib.Least_significant_bit
22:08:33 X86_Semantics: theory Word_Lib.Aligned
22:08:33 X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
22:08:33 X86_Semantics: theory Word_Lib.Most_significant_bit
22:08:33 X86_Semantics: theory Word_Lib.Generic_set_bit
22:08:34 X86_Semantics: theory Word_Lib.Bits_Int
22:08:39 X86_Semantics: theory Word_Lib.Typedef_Morphisms
22:08:39 X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
22:08:42 X86_Semantics: theory Word_Lib.Bitwise
22:08:43 X86_Semantics: theory X86_Semantics.BitByte
22:08:43 X86_Semantics: theory X86_Semantics.Memory
22:08:44 X86_Semantics: theory X86_Semantics.State
22:08:51 X86_Semantics: theory X86_Semantics.StateCleanUp
22:08:51 X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
22:09:04 X86_Semantics: theory X86_Semantics.SymbolicExecution
22:09:04 X86_Semantics: theory X86_Semantics.X86_Parse
22:09:06 X86_Semantics: theory X86_Semantics.Examples
22:09:06 X86_Semantics: theory X86_Semantics.Example_WC
22:21:57 Preparing X86_Semantics/document ...
22:22:05 Finished X86_Semantics/document (0:00:07 elapsed time)
22:22:05 Preparing X86_Semantics/outline ...
22:22:11 Finished X86_Semantics/outline (0:00:06 elapsed time)
22:22:11 Timing X86_Semantics (8 threads, 820.622s elapsed time, 1027.529s cpu time, 11.444s GC time, factor 1.25)
22:22:11 Finished X86_Semantics (0:13:42 elapsed time, 0:17:12 cpu time, factor 1.25)
22:22:12 Running CoSMeDis (on hpcisabelle/3) ...
22:22:13 CoSMeDis: theory Fresh_Identifiers.Fresh
22:22:14 CoSMeDis: theory Fresh_Identifiers.Fresh_String
22:22:14 CoSMeDis: theory CoSMeDis.Prelim
22:22:20 CoSMeDis: theory CoSMeDis.System_Specification
22:22:41 CoSMeDis: theory CoSMeDis.Automation_Setup
22:22:41 CoSMeDis: theory CoSMeDis.API_Network
22:22:41 CoSMeDis: theory CoSMeDis.Safety_Properties
22:22:42 CoSMeDis: theory CoSMeDis.Friend_Intro
22:22:42 CoSMeDis: theory CoSMeDis.Friend_Observation_Setup
22:22:42 CoSMeDis: theory CoSMeDis.Friend_State_Indistinguishability
22:22:43 CoSMeDis: theory CoSMeDis.Outer_Friend_Intro
22:22:43 CoSMeDis: theory CoSMeDis.Outer_Friend
22:22:43 CoSMeDis: theory CoSMeDis.Friend_Openness
22:22:43 CoSMeDis: theory CoSMeDis.Post_Intro
22:22:43 CoSMeDis: theory CoSMeDis.Friend_Value_Setup
22:22:43 CoSMeDis: theory CoSMeDis.Friend_Request_Intro
22:22:43 CoSMeDis: theory CoSMeDis.Friend_Request_Value_Setup
22:22:43 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Observation_Setup
22:22:44 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Observation_Setup
22:22:45 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_ISSUER
22:22:45 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_State_Indistinguishability
22:22:45 CoSMeDis: theory CoSMeDis.Friend
22:22:46 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_State_Indistinguishability
22:22:46 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_RECEIVER
22:22:46 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Openness
22:22:46 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Value_Setup
22:22:46 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Value_Setup
22:22:47 CoSMeDis: theory CoSMeDis.Friend_Request
22:22:47 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_ISSUER
22:22:47 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_ISSUER
22:22:47 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_RECEIVER
22:22:47 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER
22:22:48 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_RECEIVER
22:22:48 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER
22:22:49 CoSMeDis: theory CoSMeDis.Independent_Post_Value_Setup_RECEIVER
22:22:49 CoSMeDis: theory CoSMeDis.Post_Value_Setup_ISSUER
22:22:49 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver
22:22:49 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer
22:22:49 CoSMeDis: theory CoSMeDis.Friend_Network
22:22:50 CoSMeDis: theory CoSMeDis.Friend_Request_Network
22:22:50 CoSMeDis: theory CoSMeDis.Post_Value_Setup_RECEIVER
22:22:51 CoSMeDis: theory CoSMeDis.Outer_Friend_Network
22:22:52 CoSMeDis: theory CoSMeDis.Independent_Post_RECEIVER
22:22:53 CoSMeDis: theory CoSMeDis.Post_RECEIVER
22:22:54 CoSMeDis: theory CoSMeDis.Friend_All
22:22:55 CoSMeDis: theory CoSMeDis.Friend_Request_All
22:22:55 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_ISSUER
22:22:55 CoSMeDis: theory CoSMeDis.Post_ISSUER
22:22:56 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_ISSUER
22:22:57 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_COMPOSE2
22:22:57 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Network
22:22:57 CoSMeDis: theory CoSMeDis.Outer_Friend_All
22:22:57 CoSMeDis: theory CoSMeDis.Post_COMPOSE2
22:22:57 CoSMeDis: theory CoSMeDis.Post_Network
22:22:58 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Network
22:23:05 CoSMeDis: theory CoSMeDis.Independent_Posts_Network
22:24:53 CoSMeDis: theory CoSMeDis.Post_All
22:35:35 Preparing CoSMeDis/document ...
22:35:52 Finished CoSMeDis/document (0:00:17 elapsed time)
22:35:52 Preparing CoSMeDis/outline ...
22:36:01 Finished CoSMeDis/outline (0:00:08 elapsed time)
22:36:01 Timing CoSMeDis (8 threads, 799.255s elapsed time, 4490.920s cpu time, 136.733s GC time, factor 5.62)
22:36:01 Finished CoSMeDis (0:13:21 elapsed time, 1:14:57 cpu time, factor 5.61)
22:36:01 Building First_Order_Terms (on hpcisabelle/4) ...
22:36:03 First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
22:36:03 First_Order_Terms: theory Fresh_Identifiers.Fresh
22:36:03 First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
22:36:03 First_Order_Terms: theory First_Order_Terms.Renaming2
22:36:04 First_Order_Terms: theory First_Order_Terms.Renaming2_String
22:36:04 First_Order_Terms: theory First_Order_Terms.Fun_More
22:36:04 First_Order_Terms: theory First_Order_Terms.Option_Monad
22:36:04 First_Order_Terms: theory First_Order_Terms.Seq_More
22:36:05 First_Order_Terms: theory First_Order_Terms.Term
22:36:07 First_Order_Terms: theory First_Order_Terms.Unifiers
22:36:07 First_Order_Terms: theory First_Order_Terms.Subsumption
22:36:07 First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
22:36:07 First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
22:36:08 First_Order_Terms: theory First_Order_Terms.Abstract_Matching
22:36:08 First_Order_Terms: theory First_Order_Terms.Abstract_Unification
22:36:09 First_Order_Terms: theory First_Order_Terms.Unification
22:36:11 First_Order_Terms: theory First_Order_Terms.Matching
22:36:11 First_Order_Terms: theory First_Order_Terms.Unification_String
22:36:13 First_Order_Terms: theory Deriving.Derive_Manager
22:36:13 First_Order_Terms: theory Matrix.Utility
22:36:13 First_Order_Terms: theory Deriving.Generator_Aux
22:36:13 First_Order_Terms: theory Show.Show
22:36:14 First_Order_Terms: theory Polynomial_Factorization.Missing_List
22:36:15 First_Order_Terms: theory Show.Show_Instances
22:36:16 First_Order_Terms: theory Show.Shows_Literal
22:36:17 First_Order_Terms: theory First_Order_Terms.Position
22:36:19 First_Order_Terms: theory First_Order_Terms.Term_More
22:36:46 Preparing First_Order_Terms/document ...
22:36:56 Finished First_Order_Terms/document (0:00:10 elapsed time)
22:36:56 Preparing First_Order_Terms/outline ...
22:37:02 Finished First_Order_Terms/outline (0:00:05 elapsed time)
22:37:02 Timing First_Order_Terms (8 threads, 26.391s elapsed time, 115.593s cpu time, 3.897s GC time, factor 4.38)
22:37:02 Finished First_Order_Terms (0:00:43 elapsed time, 0:02:30 cpu time, factor 3.43)
22:37:02 Building CAVA_Base (on hpcisabelle/5) ...
22:37:04 CAVA_Base: theory CAVA_Base.Lexord_List
22:37:04 CAVA_Base: theory Deriving.Comparator
22:37:04 CAVA_Base: theory CAVA_Base.Statistics
22:37:04 CAVA_Base: theory Deriving.Generator_Aux
22:37:04 CAVA_Base: theory Deriving.Derive_Manager
22:37:04 CAVA_Base: theory HOL-Library.Char_ord
22:37:04 CAVA_Base: theory HOL-Library.Nat_Bijection
22:37:04 CAVA_Base: theory HOL-Library.Old_Datatype
22:37:04 CAVA_Base: theory CAVA_Base.Code_String
22:37:05 CAVA_Base: theory CAVA_Base.CAVA_Code_Target
22:37:05 CAVA_Base: theory CAVA_Base.CAVA_Base
22:37:05 CAVA_Base: theory Deriving.Equality_Generator
22:37:05 CAVA_Base: theory Deriving.Hash_Generator
22:37:05 CAVA_Base: theory HOL-Library.Countable
22:37:06 CAVA_Base: theory Deriving.Equality_Instances
22:37:06 CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base
22:37:06 CAVA_Base: theory Deriving.Compare
22:37:06 CAVA_Base: theory Deriving.Comparator_Generator
22:37:06 CAVA_Base: theory Deriving.Hash_Instances
22:37:07 CAVA_Base: theory Deriving.Countable_Generator
22:37:07 CAVA_Base: theory Deriving.Compare_Generator
22:37:08 CAVA_Base: theory Deriving.Compare_Instances
22:37:09 CAVA_Base: theory Deriving.Derive
22:37:23 Timing CAVA_Base (8 threads, 5.971s elapsed time, 24.382s cpu time, 0.571s GC time, factor 4.08)
22:37:23 Finished CAVA_Base (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.47)
22:37:23 Building CAVA_Automata (on hpcisabelle/6) ...
22:37:26 CAVA_Automata: theory CAVA_Automata.Step_Conv
22:37:26 CAVA_Automata: theory HOL-Library.Omega_Words_Fun
22:37:26 CAVA_Automata: theory CAVA_Automata.Digraph_Basic
22:37:27 CAVA_Automata: theory CAVA_Automata.Digraph
22:37:29 CAVA_Automata: theory CAVA_Automata.Automata
22:37:29 CAVA_Automata: theory CAVA_Automata.Digraph_Impl
22:37:36 CAVA_Automata: theory CAVA_Automata.Lasso
22:37:36 CAVA_Automata: theory CAVA_Automata.Simulation
22:37:36 CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
22:37:51 CAVA_Automata: theory CAVA_Automata.Automata_Impl
22:38:33 CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
22:38:49 Preparing CAVA_Automata/document ...
22:38:53 Finished CAVA_Automata/document (0:00:04 elapsed time)
22:38:53 Preparing CAVA_Automata/outline ...
22:38:56 Finished CAVA_Automata/outline (0:00:03 elapsed time)
22:38:56 Timing CAVA_Automata (8 threads, 68.483s elapsed time, 122.441s cpu time, 4.382s GC time, factor 1.79)
22:38:56 Finished CAVA_Automata (0:01:25 elapsed time, 0:02:34 cpu time, factor 1.82)
22:38:56 Building Shadow_SC_DOM (on hpcisabelle/7) ...
22:39:36 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
22:39:39 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
22:39:41 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
22:41:02 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
22:41:14 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
22:41:15 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
22:41:18 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
22:41:18 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
22:41:19 Shadow_SC_DOM: theory Shadow_SC_DOM.slots
22:41:19 Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
22:41:29 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
22:47:49 Preparing Shadow_SC_DOM/document ...
22:48:05 Finished Shadow_SC_DOM/document (0:00:16 elapsed time)
22:48:05 Preparing Shadow_SC_DOM/outline ...
22:48:15 Finished Shadow_SC_DOM/outline (0:00:10 elapsed time)
22:48:15 Timing Shadow_SC_DOM (8 threads, 441.340s elapsed time, 2682.202s cpu time, 171.559s GC time, factor 6.08)
22:48:15 Finished Shadow_SC_DOM (0:08:51 elapsed time, 0:48:39 cpu time, factor 5.49)
22:48:16 Building Stateful_Protocol_Composition_and_Typing (on hpcisabelle/0) ...
22:48:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
22:48:22 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
22:48:24 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
22:48:28 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
22:48:29 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
22:48:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
22:48:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
22:48:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
22:48:41 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
22:48:49 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
22:48:49 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
22:48:54 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
22:48:59 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
22:48:59 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
22:49:18 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
22:49:44 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
22:50:00 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
22:53:16 Preparing Stateful_Protocol_Composition_and_Typing/document ...
22:53:54 Finished Stateful_Protocol_Composition_and_Typing/document (0:00:37 elapsed time)
22:53:54 Preparing Stateful_Protocol_Composition_and_Typing/outline ...
22:54:10 Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:16 elapsed time)
22:54:10 Timing Stateful_Protocol_Composition_and_Typing (8 threads, 253.262s elapsed time, 1484.682s cpu time, 47.601s GC time, factor 5.86)
22:54:10 Finished Stateful_Protocol_Composition_and_Typing (0:04:57 elapsed time, 0:26:28 cpu time, factor 5.34)
22:54:11 Running Cook_Levin (on hpcisabelle/1) ...
22:54:14 Cook_Levin: theory HOL-Eisbach.Eisbach
22:54:14 Cook_Levin: theory Cook_Levin.Basics
22:54:16 Cook_Levin: theory Cook_Levin.Combinations
22:54:18 Cook_Levin: theory Cook_Levin.Elementary
22:54:20 Cook_Levin: theory Cook_Levin.Composing
22:54:20 Cook_Levin: theory Cook_Levin.Memorizing
22:54:21 Cook_Levin: theory Cook_Levin.Arithmetic
22:54:21 Cook_Levin: theory Cook_Levin.Oblivious
22:54:22 Cook_Levin: theory Cook_Levin.Oblivious_Polynomial
22:54:25 Cook_Levin: theory Cook_Levin.Lists_Lists
22:54:28 Cook_Levin: theory Cook_Levin.Two_Four_Symbols
22:54:29 Cook_Levin: theory Cook_Levin.Symbol_Ops
22:54:30 Cook_Levin: theory Cook_Levin.Wellformed
22:54:30 Cook_Levin: theory Cook_Levin.NP
22:54:31 Cook_Levin: theory Cook_Levin.Oblivious_2_Tape
22:54:32 Cook_Levin: theory Cook_Levin.Satisfiability
22:54:37 Cook_Levin: theory Cook_Levin.Reducing
22:54:38 Cook_Levin: theory Cook_Levin.Aux_TM_Reducing
22:54:43 Cook_Levin: theory Cook_Levin.Sat_TM_CNF
22:54:50 Cook_Levin: theory Cook_Levin.Reduction_TM
23:08:29 Preparing Cook_Levin/document ...
23:09:50 Finished Cook_Levin/document (0:01:21 elapsed time)
23:09:50 Preparing Cook_Levin/outline ...
23:10:24 Finished Cook_Levin/outline (0:00:33 elapsed time)
23:10:24 Timing Cook_Levin (8 threads, 850.205s elapsed time, 4296.976s cpu time, 225.530s GC time, factor 5.05)
23:10:24 Finished Cook_Levin (0:14:13 elapsed time, 1:11:44 cpu time, factor 5.04)
23:10:24 Building Frequency_Moments (on hpcisabelle/2) ...
23:10:30 Frequency_Moments: theory Digit_Expansions.Bits_Digits
23:10:30 Frequency_Moments: theory Flow_Networks.Graph
23:10:30 Frequency_Moments: theory HOL-Eisbach.Eisbach
23:10:30 Frequency_Moments: theory Graph_Theory.Rtrancl_On
23:10:30 Frequency_Moments: theory HOL-Combinatorics.Stirling
23:10:30 Frequency_Moments: theory HOL-Computational_Algebra.Group_Closure
23:10:30 Frequency_Moments: theory HOL-Computational_Algebra.Fraction_Field
23:10:30 Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order
23:10:31 Frequency_Moments: theory HOL-Computational_Algebra.Nth_Powers
23:10:31 Frequency_Moments: theory HOL-Computational_Algebra.Squarefree
23:10:31 Frequency_Moments: theory HOL-Number_Theory.Cong
23:10:31 Frequency_Moments: theory HOL-Library.Case_Converter
23:10:31 Frequency_Moments: theory HOL-Library.Code_Abstract_Nat
23:10:31 Frequency_Moments: theory HOL-Library.Code_Target_Nat
23:10:32 Frequency_Moments: theory Expander_Graphs.Extra_Congruence_Method
23:10:32 Frequency_Moments: theory HOL-Library.Code_Target_Int
23:10:32 Frequency_Moments: theory HOL-Library.Code_Lazy
23:10:32 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_Bijections
23:10:32 Frequency_Moments: theory HOL-Library.Code_Target_Numeral
23:10:32 Frequency_Moments: theory HOL-Algebra.Congruence
23:10:32 Frequency_Moments: theory Card_Partitions.Injectivity_Solver
23:10:32 Frequency_Moments: theory HOL-Computational_Algebra.Normalized_Fraction
23:10:33 Frequency_Moments: theory Card_Partitions.Set_Partition
23:10:33 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
23:10:33 Frequency_Moments: theory HOL-Combinatorics.List_Permutation
23:10:34 Frequency_Moments: theory Card_Partitions.Card_Partitions
23:10:34 Frequency_Moments: theory Jordan_Normal_Form.Missing_Misc
23:10:34 Frequency_Moments: theory Flow_Networks.Network
23:10:34 Frequency_Moments: theory HOL-Library.Function_Algebras
23:10:34 Frequency_Moments: theory Abstract-Rewriting.Seq
23:10:34 Frequency_Moments: theory HOL-Library.List_Lexorder
23:10:34 Frequency_Moments: theory HOL-Library.More_List
23:10:34 Frequency_Moments: theory Perron_Frobenius.Bij_Nat
23:10:34 Frequency_Moments: theory HOL-Library.Power_By_Squaring
23:10:34 Frequency_Moments: theory HOL-Algebra.Order
23:10:34 Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers
23:10:34 Frequency_Moments: theory HOL-Library.Transitive_Closure_Table
23:10:34 Frequency_Moments: theory HOL-Library.While_Combinator
23:10:34 Frequency_Moments: theory HOL-Number_Theory.Mod_Exp
23:10:34 Frequency_Moments: theory HOL-Number_Theory.Eratosthenes
23:10:35 Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations
23:10:35 Frequency_Moments: theory HOL-Types_To_Sets.Prerequisites
23:10:35 Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
23:10:35 Frequency_Moments: theory HOL-Types_To_Sets.Types_To_Sets
23:10:35 Frequency_Moments: theory Polynomial_Interpolation.Missing_Unsorted
23:10:36 Frequency_Moments: theory HOL-Library.Bourbaki_Witt_Fixpoint
23:10:36 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial
23:10:36 Frequency_Moments: theory HOL-Types_To_Sets.Group_On_With
23:10:36 Frequency_Moments: theory Perron_Frobenius.Cancel_Card_Constraint
23:10:36 Frequency_Moments: theory Flow_Networks.Residual_Graph
23:10:36 Frequency_Moments: theory Jordan_Normal_Form.Conjugate
23:10:36 Frequency_Moments: theory HOL-Algebra.Lattice
23:10:36 Frequency_Moments: theory HOL-Library.Going_To_Filter
23:10:37 Frequency_Moments: theory Frequency_Moments.Landau_Ext
23:10:37 Frequency_Moments: theory HOL-Library.Lattice_Algebras
23:10:37 Frequency_Moments: theory HOL-Library.Log_Nat
23:10:37 Frequency_Moments: theory Graph_Theory.Stuff
23:10:37 Frequency_Moments: theory HOL-Algebra.Complete_Lattice
23:10:37 Frequency_Moments: theory Executable_Randomized_Algorithms.Tau_Additivity
23:10:37 Frequency_Moments: theory Graph_Theory.Digraph
23:10:37 Frequency_Moments: theory HOL-Number_Theory.Fib
23:10:37 Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
23:10:37 Frequency_Moments: theory HOL-Number_Theory.Totient
23:10:38 Frequency_Moments: theory HOL-Algebra.Group
23:10:38 Frequency_Moments: theory Flow_Networks.Augmenting_Flow
23:10:38 Frequency_Moments: theory Flow_Networks.Augmenting_Path
23:10:38 Frequency_Moments: theory HOL-Complex_Analysis.Contour_Integration
23:10:39 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_PMF
23:10:39 Frequency_Moments: theory Flow_Networks.Ford_Fulkerson
23:10:39 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
23:10:39 Frequency_Moments: theory Graph_Theory.Arc_Walk
23:10:39 Frequency_Moments: theory Graph_Theory.Bidirected_Digraph
23:10:40 Frequency_Moments: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
23:10:40 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
23:10:41 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
23:10:41 Frequency_Moments: theory MFMC_Countable.MFMC_Finite
23:10:41 Frequency_Moments: theory HOL-Algebra.Coset
23:10:43 Frequency_Moments: theory HOL-Algebra.FiniteProduct
23:10:43 Frequency_Moments: theory HOL-Complex_Analysis.Winding_Numbers
23:10:43 Frequency_Moments: theory Graph_Theory.Pair_Digraph
23:10:43 Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
23:10:44 Frequency_Moments: theory Executable_Randomized_Algorithms.Coin_Space
23:10:44 Frequency_Moments: theory HOL-Algebra.Ring
23:10:45 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
23:10:45 Frequency_Moments: theory MFMC_Countable.MFMC_Misc
23:10:46 Frequency_Moments: theory HOL-Algebra.Generated_Groups
23:10:46 Frequency_Moments: theory HOL-Algebra.Divisibility
23:10:46 Frequency_Moments: theory HOL-Library.Interval
23:10:47 Frequency_Moments: theory HOL-Library.Float
23:10:47 Frequency_Moments: theory HOL-Algebra.Elementary_Groups
23:10:47 Frequency_Moments: theory HOL-Complex_Analysis.Conformal_Mappings
23:10:49 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Singularities
23:10:49 Frequency_Moments: theory HOL-Complex_Analysis.Great_Picard
23:10:50 Frequency_Moments: theory HOL-Complex_Analysis.Riemann_Mapping
23:10:51 Frequency_Moments: theory MFMC_Countable.Matrix_For_Marginals
23:10:51 Frequency_Moments: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
23:10:51 Frequency_Moments: theory HOL-Algebra.AbelCoset
23:10:52 Frequency_Moments: theory HOL-Algebra.Module
23:10:52 Frequency_Moments: theory Jordan_Normal_Form.Missing_Ring
23:10:52 Frequency_Moments: theory HOL-Library.Code_Target_Numeral_Float
23:10:52 Frequency_Moments: theory HOL-Library.Interval_Float
23:10:52 Frequency_Moments: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:10:52 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_FPS
23:10:52 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_Factorial
23:10:52 Frequency_Moments: theory Graph_Theory.Digraph_Component
23:10:53 Frequency_Moments: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:10:53 Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
23:10:53 Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
23:10:53 Frequency_Moments: theory Polynomial_Interpolation.Missing_Polynomial
23:10:55 Frequency_Moments: theory HOL-Algebra.Ideal
23:10:55 Frequency_Moments: theory Polynomial_Factorization.Order_Polynomial
23:10:55 Frequency_Moments: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:10:56 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Residues
23:10:56 Frequency_Moments: theory Median_Method.Median
23:10:56 Frequency_Moments: theory HOL-Complex_Analysis.Residue_Theorem
23:10:56 Frequency_Moments: theory HOL-Computational_Algebra.Computational_Algebra
23:10:57 Frequency_Moments: theory Graph_Theory.Digraph_Isomorphism
23:10:57 Frequency_Moments: theory Lp.Functional_Spaces
23:10:57 Frequency_Moments: theory HOL-Complex_Analysis.Laurent_Convergence
23:10:57 Frequency_Moments: theory MFMC_Countable.Rel_PMF_Characterisation
23:10:57 Frequency_Moments: theory Probabilistic_While.While_SPMF
23:10:57 Frequency_Moments: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
23:10:57 Frequency_Moments: theory Matrix.Utility
23:10:58 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom
23:10:58 Frequency_Moments: theory Regular-Sets.Regular_Set
23:10:58 Frequency_Moments: theory VectorSpace.FunctionLemmas
23:10:58 Frequency_Moments: theory VectorSpace.RingModuleFacts
23:10:58 Frequency_Moments: theory HOL-Algebra.RingHom
23:10:58 Frequency_Moments: theory HOL-Decision_Procs.Approximation
23:10:59 Frequency_Moments: theory VectorSpace.MonoidSums
23:10:59 Frequency_Moments: theory HOL-Algebra.QuotRing
23:10:59 Frequency_Moments: theory HOL-Algebra.UnivPoly
23:10:59 Frequency_Moments: theory VectorSpace.LinearCombinations
23:11:00 Frequency_Moments: theory Lp.Lp
23:11:00 Frequency_Moments: theory HOL-Complex_Analysis.Meromorphic
23:11:01 Frequency_Moments: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
23:11:01 Frequency_Moments: theory HOL-Complex_Analysis.Weierstrass_Factorization
23:11:01 Frequency_Moments: theory Concentration_Inequalities.Bienaymes_Identity
23:11:01 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
23:11:02 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Analysis
23:11:02 Frequency_Moments: theory HOL-Algebra.IntRing
23:11:02 Frequency_Moments: theory Jordan_Normal_Form.Matrix
23:11:02 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom_Poly
23:11:02 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects
23:11:02 Frequency_Moments: theory Expander_Graphs.Constructive_Chernoff_Bound
23:11:03 Frequency_Moments: theory Regular-Sets.Regular_Exp
23:11:05 Frequency_Moments: theory VectorSpace.SumSpaces
23:11:05 Frequency_Moments: theory VectorSpace.VectorSpace
23:11:07 Frequency_Moments: theory Regular-Sets.NDerivative
23:11:07 Frequency_Moments: theory Regular-Sets.Relation_Interpretation
23:11:07 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian_Misc
23:11:07 Frequency_Moments: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:11:10 Frequency_Moments: theory Jordan_Normal_Form.Column_Operations
23:11:10 Frequency_Moments: theory Jordan_Normal_Form.Determinant
23:11:12 Frequency_Moments: theory Regular-Sets.Equivalence_Checking
23:11:12 Frequency_Moments: theory Regular-Sets.Regexp_Method
23:11:13 Frequency_Moments: theory Jordan_Normal_Form.Missing_VectorSpace
23:11:13 Frequency_Moments: theory Jordan_Normal_Form.Char_Poly
23:11:13 Frequency_Moments: theory Abstract-Rewriting.Abstract_Rewriting
23:11:14 Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
23:11:15 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form
23:11:15 Frequency_Moments: theory Isabelle_Marries_Dirac.Basics
23:11:16 Frequency_Moments: theory Isabelle_Marries_Dirac.Binary_Nat
23:11:16 Frequency_Moments: theory Isabelle_Marries_Dirac.Quantum
23:11:16 Frequency_Moments: theory Abstract-Rewriting.SN_Orders
23:11:17 Frequency_Moments: theory Jordan_Normal_Form.VS_Connect
23:11:18 Frequency_Moments: theory Isabelle_Marries_Dirac.Complex_Vectors
23:11:19 Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
23:11:19 Frequency_Moments: theory HOL-Algebra.Subrings
23:11:19 Frequency_Moments: theory HOL-Number_Theory.Residues
23:11:19 Frequency_Moments: theory Matrix.Ordered_Semiring
23:11:21 Frequency_Moments: theory Matrix.Matrix_Legacy
23:11:23 Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
23:11:23 Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
23:11:23 Frequency_Moments: theory HOL-Number_Theory.Pocklington
23:11:23 Frequency_Moments: theory Lehmer.Lehmer
23:11:23 Frequency_Moments: theory HOL-Number_Theory.Gauss
23:11:23 Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
23:11:24 Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
23:11:24 Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
23:11:24 Frequency_Moments: theory Matrix_Tensor.Matrix_Tensor
23:11:24 Frequency_Moments: theory HOL-Number_Theory.Number_Theory
23:11:29 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Misc
23:11:29 Frequency_Moments: theory Dirichlet_Series.Multiplicative_Function
23:11:30 Frequency_Moments: theory Isabelle_Marries_Dirac.Tensor
23:11:30 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Product
23:11:30 Frequency_Moments: theory Dirichlet_Series.Euler_Products
23:11:30 Frequency_Moments: theory Bertrands_Postulate.Bertrand
23:11:30 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series
23:11:31 Frequency_Moments: theory Isabelle_Marries_Dirac.More_Tensor
23:11:36 Frequency_Moments: theory HOL-Algebra.Polynomials
23:11:38 Frequency_Moments: theory Jordan_Normal_Form.Gram_Schmidt
23:11:39 Frequency_Moments: theory Dirichlet_Series.Moebius_Mu
23:11:40 Frequency_Moments: theory Dirichlet_Series.More_Totient
23:11:40 Frequency_Moments: theory Dirichlet_Series.Liouville_Lambda
23:11:40 Frequency_Moments: theory Dirichlet_Series.Divisor_Count
23:11:40 Frequency_Moments: theory Dirichlet_Series.Arithmetic_Summatory
23:11:40 Frequency_Moments: theory Jordan_Normal_Form.Schur_Decomposition
23:11:41 Frequency_Moments: theory Dirichlet_Series.Partial_Summation
23:11:42 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series_Analysis
23:11:46 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:11:51 Frequency_Moments: theory Jordan_Normal_Form.Spectral_Radius
23:11:51 Frequency_Moments: theory QHLProver.Complex_Matrix
23:11:51 Frequency_Moments: theory Perron_Frobenius.HMA_Connect
23:11:53 Frequency_Moments: theory Zeta_Function.Zeta_Library
23:11:53 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
23:11:56 Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
23:11:56 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm
23:11:57 Frequency_Moments: theory QHLProver.Gates
23:11:57 Frequency_Moments: theory Projective_Measurements.Linear_Algebra_Complements
23:11:58 Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
23:12:04 Frequency_Moments: theory Projective_Measurements.Projective_Measurements
23:12:06 Frequency_Moments: theory Commuting_Hermitian.Spectral_Theory_Complements
23:12:08 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian
23:12:28 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
23:12:28 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
23:12:28 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
23:12:33 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
23:12:35 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
23:12:36 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
23:12:36 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Definition
23:12:36 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
23:12:36 Frequency_Moments: theory Frequency_Moments.K_Smallest
23:12:39 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_TTS
23:12:39 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_MGG
23:12:40 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Algebra
23:12:41 Frequency_Moments: theory Frequency_Moments.Probability_Ext
23:12:43 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Eigenvalues
23:12:46 Frequency_Moments: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
23:12:46 Frequency_Moments: theory Finite_Fields.Formal_Polynomial_Derivatives
23:12:47 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
23:12:47 Frequency_Moments: theory Finite_Fields.Monic_Polynomial_Factorization
23:12:48 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
23:12:48 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
23:12:49 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
23:12:50 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Walks
23:12:53 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Power_Construction
23:12:54 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
23:12:57 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
23:13:00 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
23:13:00 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test
23:13:01 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials
23:13:04 Frequency_Moments: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
23:13:07 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test_Code
23:13:11 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
23:13:20 Frequency_Moments: theory Finite_Fields.Find_Irreducible_Poly
23:13:27 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
23:13:32 Frequency_Moments: theory Frequency_Moments.Tutorial_Pseudorandom_Objects
23:23:57 Preparing Frequency_Moments/document ...
23:24:06 Finished Frequency_Moments/document (0:00:08 elapsed time)
23:24:06 Preparing Frequency_Moments/outline ...
23:24:10 Finished Frequency_Moments/outline (0:00:03 elapsed time)
23:24:10 Timing Frequency_Moments (8 threads, 715.969s elapsed time, 4073.447s cpu time, 219.454s GC time, factor 5.69)
23:24:10 Finished Frequency_Moments (0:13:17 elapsed time, 1:11:11 cpu time, factor 5.36)
23:24:11 Building Padic_Ints (on hpcisabelle/3) ...
23:24:13 Padic_Ints: theory Padic_Ints.Function_Ring
23:24:13 Padic_Ints: theory HOL-Number_Theory.Cong
23:24:13 Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
23:24:13 Padic_Ints: theory Padic_Ints.Extended_Int
23:24:15 Padic_Ints: theory HOL-Number_Theory.Totient
23:24:16 Padic_Ints: theory HOL-Number_Theory.Residues
23:24:20 Padic_Ints: theory Padic_Ints.Padic_Construction
23:24:21 Padic_Ints: theory Padic_Ints.Padic_Integers
23:24:23 Padic_Ints: theory Padic_Ints.Cring_Poly
23:25:24 Padic_Ints: theory Padic_Ints.Padic_Int_Topology
23:25:28 Padic_Ints: theory Padic_Ints.Zp_Compact
23:26:06 Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
23:26:09 Padic_Ints: theory Padic_Ints.Hensels_Lemma
23:26:48 Preparing Padic_Ints/document ...
23:27:18 Finished Padic_Ints/document (0:00:29 elapsed time)
23:27:18 Preparing Padic_Ints/outline ...
23:27:29 Finished Padic_Ints/outline (0:00:11 elapsed time)
23:27:29 Timing Padic_Ints (8 threads, 132.366s elapsed time, 547.617s cpu time, 61.928s GC time, factor 4.14)
23:27:29 Finished Padic_Ints (0:02:35 elapsed time, 0:09:56 cpu time, factor 3.83)
23:27:30 Running Finite_Fields (on hpcisabelle/4) ...
23:27:35 Finite_Fields: theory Digit_Expansions.Bits_Digits
23:27:35 Finite_Fields: theory Flow_Networks.Graph
23:27:35 Finite_Fields: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
23:27:35 Finite_Fields: theory HOL-Number_Theory.Cong
23:27:35 Finite_Fields: theory HOL-Real_Asymp.Inst_Existentials
23:27:35 Finite_Fields: theory HOL-Number_Theory.Eratosthenes
23:27:35 Finite_Fields: theory HOL-Types_To_Sets.Types_To_Sets
23:27:35 Finite_Fields: theory HOL-Analysis.Metric_Arith
23:27:35 Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results
23:27:35 Finite_Fields: theory Finite_Fields.Finite_Fields_More_Bijections
23:27:35 Finite_Fields: theory HOL-Analysis.Abstract_Topology
23:27:36 Finite_Fields: theory HOL-Analysis.Continuum_Not_Denumerable
23:27:36 Finite_Fields: theory HOL-Analysis.Inner_Product
23:27:36 Finite_Fields: theory HOL-Analysis.L2_Norm
23:27:36 Finite_Fields: theory HOL-Analysis.Operator_Norm
23:27:36 Finite_Fields: theory HOL-Analysis.Poly_Roots
23:27:36 Finite_Fields: theory HOL-Analysis.Product_Vector
23:27:36 Finite_Fields: theory HOL-Combinatorics.Multiset_Permutations
23:27:37 Finite_Fields: theory HOL-Number_Theory.Mod_Exp
23:27:37 Finite_Fields: theory HOL-Analysis.Sigma_Algebra
23:27:37 Finite_Fields: theory Flow_Networks.Network
23:27:38 Finite_Fields: theory HOL-Analysis.Norm_Arith
23:27:38 Finite_Fields: theory HOL-Number_Theory.Fib
23:27:38 Finite_Fields: theory HOL-Number_Theory.Prime_Powers
23:27:38 Finite_Fields: theory HOL-Number_Theory.Totient
23:27:39 Finite_Fields: theory HOL-Real_Asymp.Eventuallize
23:27:39 Finite_Fields: theory HOL-Real_Asymp.Lazy_Eval
23:27:39 Finite_Fields: theory HOL-Number_Theory.Residues
23:27:40 Finite_Fields: theory HOL-Analysis.Elementary_Topology
23:27:40 Finite_Fields: theory Flow_Networks.Residual_Graph
23:27:41 Finite_Fields: theory HOL-Analysis.Euclidean_Space
23:27:41 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion
23:27:41 Finite_Fields: theory HOL-Analysis.Measurable
23:27:42 Finite_Fields: theory HOL-Analysis.Abstract_Limits
23:27:42 Finite_Fields: theory HOL-Analysis.FSigma
23:27:42 Finite_Fields: theory HOL-Analysis.Sum_Topology
23:27:43 Finite_Fields: theory HOL-Analysis.Measure_Space
23:27:44 Finite_Fields: theory Flow_Networks.Augmenting_Flow
23:27:44 Finite_Fields: theory Flow_Networks.Augmenting_Path
23:27:44 Finite_Fields: theory HOL-Analysis.Finite_Cartesian_Product
23:27:44 Finite_Fields: theory HOL-Analysis.Linear_Algebra
23:27:44 Finite_Fields: theory HOL-Analysis.Abstract_Topology_2
23:27:44 Finite_Fields: theory Flow_Networks.Ford_Fulkerson
23:27:44 Finite_Fields: theory HOL-Analysis.Infinite_Sum
23:27:44 Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
23:27:45 Finite_Fields: theory Finite_Fields.Ring_Characteristic
23:27:45 Finite_Fields: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
23:27:46 Finite_Fields: theory HOL-Analysis.Affine
23:27:47 Finite_Fields: theory HOL-Analysis.Caratheodory
23:27:47 Finite_Fields: theory HOL-Analysis.Convex
23:27:48 Finite_Fields: theory MFMC_Countable.MFMC_Finite
23:27:48 Finite_Fields: theory HOL-Analysis.Cartesian_Space
23:27:48 Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
23:27:48 Finite_Fields: theory HOL-Number_Theory.Gauss
23:27:48 Finite_Fields: theory HOL-Analysis.Connected
23:27:48 Finite_Fields: theory HOL-Analysis.Elementary_Metric_Spaces
23:27:49 Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
23:27:49 Finite_Fields: theory HOL-Analysis.Function_Topology
23:27:50 Finite_Fields: theory HOL-Number_Theory.Pocklington
23:27:51 Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
23:27:52 Finite_Fields: theory HOL-Analysis.Product_Topology
23:27:52 Finite_Fields: theory HOL-Number_Theory.Number_Theory
23:27:52 Finite_Fields: theory HOL-Analysis.T1_Spaces
23:27:53 Finite_Fields: theory HOL-Analysis.Determinants
23:27:53 Finite_Fields: theory HOL-Analysis.Lindelof_Spaces
23:27:54 Finite_Fields: theory HOL-Analysis.Elementary_Normed_Spaces
23:27:54 Finite_Fields: theory HOL-Analysis.Function_Metric
23:27:54 Finite_Fields: theory HOL-Analysis.Isolated
23:27:54 Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
23:27:54 Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
23:27:55 Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
23:27:55 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
23:27:55 Finite_Fields: theory HOL-Analysis.Topology_Euclidean_Space
23:27:57 Finite_Fields: theory HOL-Analysis.Extended_Real_Limits
23:27:57 Finite_Fields: theory HOL-Analysis.Line_Segment
23:27:57 Finite_Fields: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
23:27:57 Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
23:27:58 Finite_Fields: theory HOL-Analysis.Convex_Euclidean_Space
23:27:58 Finite_Fields: theory HOL-Analysis.Tagged_Division
23:27:58 Finite_Fields: theory HOL-Analysis.Summation_Tests
23:27:59 Finite_Fields: theory Dirichlet_Series.Moebius_Mu
23:27:59 Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
23:27:59 Finite_Fields: theory Dirichlet_Series.More_Totient
23:28:00 Finite_Fields: theory HOL-Analysis.Ordered_Euclidean_Space
23:28:00 Finite_Fields: theory HOL-Analysis.Starlike
23:28:00 Finite_Fields: theory HOL-Analysis.Uniform_Limit
23:28:00 Finite_Fields: theory Dirichlet_Series.Divisor_Count
23:28:01 Finite_Fields: theory Dirichlet_Series.Liouville_Lambda
23:28:01 Finite_Fields: theory Dirichlet_Series.Arithmetic_Summatory
23:28:02 Finite_Fields: theory HOL-Analysis.Bounded_Continuous_Function
23:28:02 Finite_Fields: theory HOL-Analysis.Bounded_Linear_Function
23:28:02 Finite_Fields: theory HOL-Analysis.Continuous_Extension
23:28:02 Finite_Fields: theory HOL-Analysis.Path_Connected
23:28:04 Finite_Fields: theory HOL-Analysis.Derivative
23:28:04 Finite_Fields: theory HOL-Analysis.Locally
23:28:04 Finite_Fields: theory HOL-Analysis.Uncountable_Sets
23:28:04 Finite_Fields: theory HOL-Analysis.Homotopy
23:28:04 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
23:28:05 Finite_Fields: theory HOL-Analysis.Arcwise_Connected
23:28:07 Finite_Fields: theory HOL-Analysis.Borel_Space
23:28:07 Finite_Fields: theory HOL-Analysis.Cartesian_Euclidean_Space
23:28:07 Finite_Fields: theory HOL-Analysis.Complex_Analysis_Basics
23:28:07 Finite_Fields: theory HOL-Analysis.Weierstrass_Theorems
23:28:08 Finite_Fields: theory HOL-Analysis.Cross3
23:28:08 Finite_Fields: theory HOL-Analysis.Polytope
23:28:08 Finite_Fields: theory HOL-Analysis.Abstract_Euclidean_Space
23:28:09 Finite_Fields: theory HOL-Analysis.Abstract_Topological_Spaces
23:28:09 Finite_Fields: theory HOL-Analysis.Homeomorphism
23:28:10 Finite_Fields: theory HOL-Analysis.Sparse_In
23:28:11 Finite_Fields: theory HOL-Analysis.Complex_Transcendental
23:28:11 Finite_Fields: theory HOL-Analysis.Brouwer_Fixpoint
23:28:12 Finite_Fields: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
23:28:12 Finite_Fields: theory HOL-Analysis.Regularity
23:28:13 Finite_Fields: theory Executable_Randomized_Algorithms.Tau_Additivity
23:28:14 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
23:28:14 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test
23:28:14 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
23:28:15 Finite_Fields: theory HOL-Analysis.Fashoda_Theorem
23:28:16 Finite_Fields: theory HOL-Analysis.Retracts
23:28:17 Finite_Fields: theory HOL-Analysis.Abstract_Metric_Spaces
23:28:17 Finite_Fields: theory HOL-Analysis.Generalised_Binomial_Theorem
23:28:17 Finite_Fields: theory HOL-Analysis.FPS_Convergence
23:28:17 Finite_Fields: theory HOL-Analysis.Binary_Product_Measure
23:28:19 Finite_Fields: theory HOL-Analysis.Embed_Measure
23:28:19 Finite_Fields: theory HOL-Analysis.Finite_Product_Measure
23:28:19 Finite_Fields: theory HOL-Analysis.Harmonic_Numbers
23:28:19 Finite_Fields: theory HOL-Analysis.Infinite_Products
23:28:20 Finite_Fields: theory HOL-Analysis.Smooth_Paths
23:28:21 Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
23:28:22 Finite_Fields: theory HOL-Analysis.Bochner_Integration
23:28:22 Finite_Fields: theory HOL-Probability.Fin_Map
23:28:24 Finite_Fields: theory HOL-Analysis.Lipschitz
23:28:24 Finite_Fields: theory HOL-Analysis.Urysohn
23:28:25 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test_Code
23:28:25 Finite_Fields: theory HOL-Analysis.Complete_Measure
23:28:25 Finite_Fields: theory HOL-Analysis.Radon_Nikodym
23:28:26 Finite_Fields: theory HOL-Analysis.Set_Integral
23:28:26 Finite_Fields: theory HOL-Analysis.Multivariate_Analysis
23:28:26 Finite_Fields: theory HOL-Analysis.Lebesgue_Measure
23:28:28 Finite_Fields: theory HOL-Analysis.Infinite_Set_Sum
23:28:30 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
23:28:31 Finite_Fields: theory HOL-Analysis.Henstock_Kurzweil_Integration
23:28:31 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
23:28:33 Finite_Fields: theory HOL-Real_Asymp.Real_Asymp
23:28:36 Finite_Fields: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
23:28:36 Finite_Fields: theory HOL-Analysis.Integral_Test
23:28:36 Finite_Fields: theory HOL-Analysis.Kronecker_Approximation_Theorem
23:28:38 Finite_Fields: theory HOL-Analysis.Further_Topology
23:28:38 Finite_Fields: theory HOL-Analysis.Gamma_Function
23:28:38 Finite_Fields: theory HOL-Analysis.Improper_Integral
23:28:38 Finite_Fields: theory HOL-Analysis.Interval_Integral
23:28:38 Finite_Fields: theory HOL-Analysis.Vitali_Covering_Theorem
23:28:40 Finite_Fields: theory HOL-Analysis.Equivalence_Measurable_On_Borel
23:28:40 Finite_Fields: theory HOL-Analysis.Lebesgue_Integral_Substitution
23:28:40 Finite_Fields: theory HOL-Analysis.Change_Of_Vars
23:28:43 Finite_Fields: theory HOL-Analysis.Simplex_Content
23:28:47 Finite_Fields: theory HOL-Analysis.Jordan_Curve
23:28:48 Finite_Fields: theory HOL-Analysis.Ball_Volume
23:28:48 Finite_Fields: theory HOL-Analysis.Analysis
23:28:50 Finite_Fields: theory Dirichlet_Series.Euler_Products
23:28:50 Finite_Fields: theory Dirichlet_Series.Partial_Summation
23:28:50 Finite_Fields: theory HOL-Complex_Analysis.Contour_Integration
23:28:50 Finite_Fields: theory HOL-Probability.Discrete_Topology
23:28:50 Finite_Fields: theory HOL-Probability.Essential_Supremum
23:28:50 Finite_Fields: theory HOL-Probability.Probability_Measure
23:28:50 Finite_Fields: theory HOL-Probability.Stopping_Time
23:28:50 Finite_Fields: theory HOL-Probability.Tree_Space
23:28:51 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
23:28:52 Finite_Fields: theory HOL-Probability.Conditional_Expectation
23:28:52 Finite_Fields: theory HOL-Complex_Analysis.Winding_Numbers
23:28:52 Finite_Fields: theory HOL-Probability.Distribution_Functions
23:28:52 Finite_Fields: theory HOL-Probability.Giry_Monad
23:28:52 Finite_Fields: theory HOL-Probability.Weak_Convergence
23:28:53 Finite_Fields: theory HOL-Probability.Helly_Selection
23:28:53 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
23:28:55 Finite_Fields: theory HOL-Probability.Probability_Mass_Function
23:28:55 Finite_Fields: theory HOL-Probability.Projective_Family
23:28:55 Finite_Fields: theory HOL-Complex_Analysis.Conformal_Mappings
23:28:56 Finite_Fields: theory HOL-Complex_Analysis.Complex_Singularities
23:28:56 Finite_Fields: theory HOL-Complex_Analysis.Great_Picard
23:28:56 Finite_Fields: theory HOL-Probability.Infinite_Product_Measure
23:28:57 Finite_Fields: theory HOL-Complex_Analysis.Riemann_Mapping
23:28:58 Finite_Fields: theory HOL-Probability.Independent_Family
23:28:58 Finite_Fields: theory HOL-Probability.Projective_Limit
23:28:58 Finite_Fields: theory HOL-Probability.Stream_Space
23:28:59 Finite_Fields: theory HOL-Complex_Analysis.Complex_Residues
23:28:59 Finite_Fields: theory HOL-Complex_Analysis.Residue_Theorem
23:28:59 Finite_Fields: theory Finite_Fields.Finite_Fields_More_PMF
23:28:59 Finite_Fields: theory HOL-Probability.PMF_Impl
23:29:00 Finite_Fields: theory HOL-Probability.Random_Permutations
23:29:00 Finite_Fields: theory HOL-Probability.SPMF
23:29:00 Finite_Fields: theory HOL-Complex_Analysis.Laurent_Convergence
23:29:00 Finite_Fields: theory HOL-Probability.Convolution
23:29:00 Finite_Fields: theory HOL-Probability.Information
23:29:00 Finite_Fields: theory HOL-Probability.Product_PMF
23:29:02 Finite_Fields: theory HOL-Probability.Hoeffding
23:29:03 Finite_Fields: theory HOL-Probability.Distributions
23:29:04 Finite_Fields: theory HOL-Complex_Analysis.Meromorphic
23:29:05 Finite_Fields: theory HOL-Probability.Characteristic_Functions
23:29:05 Finite_Fields: theory HOL-Probability.Sinc_Integral
23:29:05 Finite_Fields: theory HOL-Complex_Analysis.Weierstrass_Factorization
23:29:06 Finite_Fields: theory HOL-Complex_Analysis.Complex_Analysis
23:29:06 Finite_Fields: theory HOL-Probability.Levy
23:29:06 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series_Analysis
23:29:06 Finite_Fields: theory HOL-Probability.Central_Limit_Theorem
23:29:06 Finite_Fields: theory HOL-Probability.Probability
23:29:11 Finite_Fields: theory Executable_Randomized_Algorithms.Coin_Space
23:29:11 Finite_Fields: theory MFMC_Countable.MFMC_Misc
23:29:13 Finite_Fields: theory MFMC_Countable.Matrix_For_Marginals
23:29:14 Finite_Fields: theory MFMC_Countable.Rel_PMF_Characterisation
23:29:14 Finite_Fields: theory Probabilistic_While.While_SPMF
23:29:14 Finite_Fields: theory Zeta_Function.Zeta_Library
23:29:15 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
23:29:18 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm
23:29:20 Finite_Fields: theory Finite_Fields.Find_Irreducible_Poly
23:39:46 Preparing Finite_Fields/document ...
23:39:58 Finished Finite_Fields/document (0:00:11 elapsed time)
23:39:58 Preparing Finite_Fields/outline ...
23:40:02 Finished Finite_Fields/outline (0:00:04 elapsed time)
23:40:03 Timing Finite_Fields (8 threads, 706.848s elapsed time, 4989.146s cpu time, 472.566s GC time, factor 7.06)
23:40:03 Finished Finite_Fields (0:11:54 elapsed time, 1:23:42 cpu time, factor 7.03)
23:40:03 Running HOL-ODE-ARCH-COMP (on hpcisabelle/5) ...
23:40:07 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
23:52:28 Timing HOL-ODE-ARCH-COMP (8 threads, 740.215s elapsed time, 1676.664s cpu time, 16.914s GC time, factor 2.27)
23:52:28 Finished HOL-ODE-ARCH-COMP (0:12:24 elapsed time, 0:28:03 cpu time, factor 2.26)
23:52:28 Building Sepref_Prereq (on hpcisabelle/6) ...
23:52:30 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
23:52:30 Sepref_Prereq: theory HOL-Library.Nat_Bijection
23:52:30 Sepref_Prereq: theory HOL-Library.Old_Datatype
23:52:31 Sepref_Prereq: theory HOL-Library.Countable
23:52:33 Sepref_Prereq: theory HOL-Imperative_HOL.Heap
23:52:35 Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
23:52:38 Sepref_Prereq: theory HOL-Imperative_HOL.Array
23:52:38 Sepref_Prereq: theory HOL-Imperative_HOL.Ref
23:52:39 Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
23:52:39 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
23:52:39 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
23:52:39 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
23:52:41 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
23:52:42 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
23:52:43 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
23:52:45 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
23:52:45 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
23:52:47 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
23:52:48 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
23:52:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
23:52:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
23:52:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
23:53:00 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
23:53:00 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
23:53:01 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
23:53:03 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
23:53:22 Timing Sepref_Prereq (8 threads, 35.001s elapsed time, 101.208s cpu time, 2.999s GC time, factor 2.89)
23:53:22 Finished Sepref_Prereq (0:00:52 elapsed time, 0:02:14 cpu time, factor 2.56)
23:53:22 Running MiniSail (on hpcisabelle/7) ...
23:53:24 MiniSail: theory HOL-Eisbach.Eisbach
23:53:24 MiniSail: theory FinFun.FinFun
23:53:26 MiniSail: theory HOL-Eisbach.Eisbach_Tools
23:53:26 MiniSail: theory Nominal2.Nominal2_Base
23:53:32 MiniSail: theory Nominal2.Nominal2_Abs
23:53:34 MiniSail: theory Nominal2.Nominal2_FCB
23:53:35 MiniSail: theory Nominal2.Nominal2
23:53:39 MiniSail: theory MiniSail.Nominal-Utils
23:53:40 MiniSail: theory MiniSail.Syntax
23:54:36 MiniSail: theory MiniSail.BTVSubst
23:54:36 MiniSail: theory MiniSail.IVSubst
23:54:42 MiniSail: theory MiniSail.Wellformed
23:54:42 MiniSail: theory MiniSail.SyntaxL
23:56:24 MiniSail: theory MiniSail.RCLogic
23:56:24 MiniSail: theory MiniSail.WellformedL
23:56:47 MiniSail: theory MiniSail.SubstMethods
23:56:52 MiniSail: theory MiniSail.RCLogicL
23:56:56 MiniSail: theory MiniSail.Typing
23:59:15 MiniSail: theory MiniSail.Operational
23:59:17 MiniSail: theory MiniSail.TypingL
23:59:29 MiniSail: theory MiniSail.ContextSubtypingL
23:59:33 MiniSail: theory MiniSail.BTVSubstTypingL
23:59:33 MiniSail: theory MiniSail.IVSubstTypingL
23:59:34 MiniSail: theory MiniSail.Safety
23:59:40 MiniSail: theory MiniSail.MiniSail
00:05:32 Preparing MiniSail/document ...
00:06:05 Finished MiniSail/document (0:00:33 elapsed time)
00:06:06 Preparing MiniSail/outline ...
00:06:19 Finished MiniSail/outline (0:00:13 elapsed time)
00:06:19 Timing MiniSail (8 threads, 722.123s elapsed time, 3660.410s cpu time, 215.252s GC time, factor 5.07)
00:06:19 Finished MiniSail (0:12:06 elapsed time, 1:01:10 cpu time, factor 5.06)
00:06:19 Building CAVA_Setup (on hpcisabelle/0) ...
00:06:22 CAVA_Setup: theory Partial_Order_Reduction.Basic_Extensions
00:06:22 CAVA_Setup: theory HOL-Library.Complete_Partial_Order2
00:06:22 CAVA_Setup: theory HOL-Library.Case_Converter
00:06:22 CAVA_Setup: theory HOL-Library.IArray
00:06:22 CAVA_Setup: theory Partial_Order_Reduction.Set_Extensions
00:06:22 CAVA_Setup: theory HOL-Library.Mapping
00:06:22 CAVA_Setup: theory HOL-Library.Stream
00:06:22 CAVA_Setup: theory DFS_Framework.DFS_Framework_Misc
00:06:22 CAVA_Setup: theory HOL-Library.Sublist
00:06:22 CAVA_Setup: theory Partial_Order_Reduction.Functions
00:06:23 CAVA_Setup: theory HOL-Library.Simps_Case_Conv
00:06:23 CAVA_Setup: theory HOL-Library.Countable_Set
00:06:23 CAVA_Setup: theory LTL.LTL
00:06:23 CAVA_Setup: theory Partial_Order_Reduction.Relation_Extensions
00:06:23 CAVA_Setup: theory Promela.PromelaAST
00:06:24 CAVA_Setup: theory DFS_Framework.DFS_Framework_Refine_Aux
00:06:24 CAVA_Setup: theory HOL-Library.Countable_Complete_Lattices
00:06:24 CAVA_Setup: theory SM.SM_Syntax
00:06:24 CAVA_Setup: theory SM.SOS_Misc_Add
00:06:24 CAVA_Setup: theory Stuttering_Equivalence.Samplers
00:06:25 CAVA_Setup: theory HOL-Library.RBT_Mapping
00:06:25 CAVA_Setup: theory Stuttering_Equivalence.StutterEquivalence
00:06:25 CAVA_Setup: theory Transition_Systems_and_Automata.Basic
00:06:25 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence
00:06:25 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton
00:06:26 CAVA_Setup: theory HOL-Library.Prefix_Order
00:06:26 CAVA_Setup: theory Partial_Order_Reduction.List_Prefixes
00:06:26 CAVA_Setup: theory Partial_Order_Reduction.List_Extensions
00:06:26 CAVA_Setup: theory SM.LTS
00:06:26 CAVA_Setup: theory SM.Gen_Scheduler
00:06:26 CAVA_Setup: theory Partial_Order_Reduction.Word_Prefixes
00:06:27 CAVA_Setup: theory Partial_Order_Reduction.Traces
00:06:28 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System
00:06:28 CAVA_Setup: theory DFS_Framework.Impl_Rev_Array_Stack
00:06:28 CAVA_Setup: theory DFS_Framework.Param_DFS
00:06:28 CAVA_Setup: theory HOL-Library.Order_Continuity
00:06:29 CAVA_Setup: theory HOL-Library.Extended_Nat
00:06:29 CAVA_Setup: theory SM.Gen_Scheduler_Refine
00:06:30 CAVA_Setup: theory Promela.PromelaStatistics
00:06:30 CAVA_Setup: theory Gabow_SCC.Find_Path
00:06:30 CAVA_Setup: theory SM.SM_Cfg
00:06:30 CAVA_Setup: theory Gabow_SCC.Find_Path_Impl
00:06:30 CAVA_Setup: theory Gabow_SCC.Gabow_SCC
00:06:30 CAVA_Setup: theory Coinductive.Coinductive_Nat
00:06:30 CAVA_Setup: theory HOL-Library.Linear_Temporal_Logic_on_Streams
00:06:31 CAVA_Setup: theory SM.Gen_Cfg_Bisim
00:06:31 CAVA_Setup: theory Coinductive.Coinductive_List
00:06:32 CAVA_Setup: theory Partial_Order_Reduction.ENat_Extensions
00:06:32 CAVA_Setup: theory Partial_Order_Reduction.CCPO_Extensions
00:06:33 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence_LTL
00:06:34 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Construction
00:06:34 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Extra
00:06:34 CAVA_Setup: theory Partial_Order_Reduction.ESet_Extensions
00:06:34 CAVA_Setup: theory DFS_Framework.DFS_Invars_Basic
00:06:34 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Extensions
00:06:35 CAVA_Setup: theory DFS_Framework.General_DFS_Structure
00:06:36 CAVA_Setup: theory Gabow_SCC.Gabow_GBG
00:06:36 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Traces
00:06:37 CAVA_Setup: theory SM.Pid_Scheduler
00:06:37 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton_Code
00:06:40 CAVA_Setup: theory Coinductive.Coinductive_List_Prefix
00:06:41 CAVA_Setup: theory Coinductive.Coinductive_Stream
00:06:41 CAVA_Setup: theory Word_Lib.Bits_Int
00:06:42 CAVA_Setup: theory Partial_Order_Reduction.Coinductive_List_Extensions
00:06:42 CAVA_Setup: theory Stuttering_Equivalence.PLTL
00:06:43 CAVA_Setup: theory DFS_Framework.Rec_Impl
00:06:43 CAVA_Setup: theory DFS_Framework.Tailrec_Impl
00:06:43 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA
00:06:44 CAVA_Setup: theory Partial_Order_Reduction.LList_Prefixes
00:06:44 CAVA_Setup: theory Partial_Order_Reduction.Stuttering
00:06:46 CAVA_Setup: theory Word_Lib.Typedef_Morphisms
00:06:46 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
00:06:46 CAVA_Setup: theory SM.SM_State
00:06:47 CAVA_Setup: theory Partial_Order_Reduction.Ample_Abstract
00:06:48 CAVA_Setup: theory Partial_Order_Reduction.Ample_Analysis
00:06:48 CAVA_Setup: theory SM.SM_Semantics
00:06:51 CAVA_Setup: theory Promela.PromelaDatastructures
00:06:52 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA_impl
00:06:52 CAVA_Setup: theory DFS_Framework.Simple_Impl
00:06:54 CAVA_Setup: theory SM.Decide_Locality
00:06:54 CAVA_Setup: theory SM.SM_LTL
00:06:55 CAVA_Setup: theory SM.Type_System
00:06:59 CAVA_Setup: theory DFS_Framework.Restr_Impl
00:06:59 CAVA_Setup: theory SM.SM_Finite_Reachable
00:07:00 CAVA_Setup: theory SM.Rename_Cfg
00:07:01 CAVA_Setup: theory DFS_Framework.DFS_Framework
00:07:02 CAVA_Setup: theory DFS_Framework.Reachable_Nodes
00:07:09 CAVA_Setup: theory SM.SM_Visible
00:07:09 CAVA_Setup: theory Gabow_SCC.Gabow_GBG_Code
00:07:09 CAVA_Setup: theory Gabow_SCC.Gabow_SCC_Code
00:07:11 CAVA_Setup: theory SM.SM_Pid
00:07:16 CAVA_Setup: theory SM.SM_Variables
00:07:17 CAVA_Setup: theory SM.SM_Indep
00:07:48 CAVA_Setup: theory LTL_to_GBA.All_Of_LTL_to_GBA
00:07:57 CAVA_Setup: theory DFS_Framework.Feedback_Arcs
00:08:06 Build timed out (after 300 minutes). Marking the build as failed.
00:08:06 Build was aborted
00:12:26 Started calculate disk usage of build
00:12:27 Finished Calculation of disk usage of build in 0 seconds
00:12:27 Started calculate disk usage of workspace
00:12:28 Finished Calculation of disk usage of workspace in  1 second
00:12:29 No emails were triggered.
00:12:29 Finished: FAILURE