Console Output

11:38:02 Started by user nipkow
11:38:02 Running as SYSTEM
11:38:02 [EnvInject] - Loading node environment variables.
11:38:02 Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
11:38:02 [isabelle-all] $ hg showconfig paths.default
11:38:02 [isabelle-all] $ hg pull --rev default
11:38:02 pulling from https://isabelle.in.tum.de/repos/isabelle/
11:38:02 no changes found
11:38:02 [isabelle-all] $ hg update --clean --rev default
11:38:02 0 files updated, 0 files merged, 0 files removed, 0 files unresolved
11:38:02 [isabelle-all] $ hg log --rev . --template {node}
11:38:03 [isabelle-all] $ hg log --rev . --template {rev}
11:38:03 [isabelle-all] $ hg log --rev 613ac8c77a84212408cba7d5bc65238ea3ab2f34 --template exists\n
11:38:03 exists
11:38:03 [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(613ac8c77a84212408cba7d5bc65238ea3ab2f34)" --encoding UTF-8 --encodingmode replace
11:38:03 [afp] $ hg showconfig paths.default
11:38:03 [afp] $ hg pull --rev default
11:38:04 pulling from https://foss.heptapod.net/isa-afp/afp-devel/
11:38:04 no changes found
11:38:04 [afp] $ hg update --clean --rev default
11:38:04 0 files updated, 0 files merged, 0 files removed, 0 files unresolved
11:38:04 [afp] $ hg --config extensions.purge= clean --all
11:38:04 [afp] $ hg log --rev . --template {node}
11:38:04 [afp] $ hg log --rev . --template {rev}
11:38:04 [afp] $ hg log --rev 153470351ff5859eed0de7504dc84827fd779a22 --template exists\n
11:38:04 exists
11:38:04 [afp] $ 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(153470351ff5859eed0de7504dc84827fd779a22)" --encoding UTF-8 --encodingmode replace
11:38:05 No emails were triggered.
11:38:05 
[isabelle-all] $ /bin/sh -xe /tmp/jenkins4869908564295098969.sh

11:38:05 + Admin/jenkins/run_build all
11:38:05 + set -e
11:38:05 + PROFILE=all
11:38:05 + shift
11:38:05 + bin/isabelle components -a
11:38:05 + bin/isabelle jedit -bf
11:38:05 ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
11:39:17 ### Building Demo (/media/data/jenkins/workspace/isabelle-all/src/Tools/Demo/lib/demo.jar) ...
11:39:18 ### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
11:39:19 Hinweis: Einige Eingabedateien verwenden nicht geprüfte oder unsichere Vorgänge.
11:39:19 Hinweis: Wiederholen Sie die Kompilierung mit -Xlint:unchecked, um Details zu erhalten.
11:39:19 ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
11:39:19 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
11:39:22 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
11:39:26 + bin/isabelle ocaml_setup
11:39:26 # Run eval $(opam env) to update the current shell environment
11:39:27 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
11:39:27        opam update
11:39:27 
11:39:28 [NOTE] Package zarith is already installed (current version is 1.12).
11:39:28 + bin/isabelle ghc_setup
11:39:29 Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
11:39:29 consider using: stack ghc, stack ghci, stack runghc, or stack exec.
11:39:30 The Glorious Glasgow Haskell Compilation System, version 9.6.4
11:39:30 + bin/isabelle go_setup
11:39:32 Component directory "/media/data/jenkins/.isabelle/contrib/go-1.22.1"
11:39:32 ### Platform x86_64-linux already installed
11:39:32 + bin/isabelle ci_build all
11:39:35 
11:39:35 === CONFIGURATION ===
11:39:35 
11:39:35 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
11:39:35 ISABELLE_BUILD_OPTIONS=""
11:39:35 
11:39:35 ML_PLATFORM="x86_64_32-linux"
11:39:35 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64_32-linux"
11:39:35 ML_SYSTEM="polyml-5.9.1"
11:39:35 ML_OPTIONS="-H 4000 --maxheap 16G"
11:39:35 Cluster(cluster.default,true)
11:39:35 
11:39:35 === BUILD ===
11:39:35 
11:39:35 Build started at Wed, 12 Jun 2024 11:39:35 +0200
11:39:35 Isabelle id 613ac8c77a84
11:39:35 AFP id 153470351ff5
11:39:36 
11:39:36 === LOG ===
11:39:36 
11:39:38 Session Pure/Pure
11:39:38 Session Misc/CTT
11:39:39 Session Misc/Cube
11:39:39 Session FOL/FOL
11:39:39 Session FOL/CCL
11:39:39 Session FOL/FOL-ex
11:39:39 Session FOL/FOLP
11:39:39 Session FOL/FOLP-ex
11:39:39 Session Doc/Intro (doc)
11:39:39 Session FOL/LCF
11:39:39 Session Doc/Logics (doc)
11:39:39 Session Doc/Nitpick (doc)
11:39:39 Session Pure/Pure-Examples
11:39:39 Session Pure/Pure-ex
11:39:39 Session Misc/SML
11:39:39 Session Misc/Sequents
11:39:39 Session Doc/Sledgehammer (doc)
11:39:39 Session AFP/SpecCheck (AFP)
11:39:39 Session Misc/Tools
11:39:39 Session HOL/HOL (main)
11:39:40 Session AFP/AVL-Trees (AFP)
11:39:40 Session AFP/AWN (AFP)
11:39:41 Session AFP/Abortable_Linearizable_Modules (AFP)
11:39:41 Session AFP/Abstract-Hoare-Logics (AFP)
11:39:41 Session AFP/Ackermanns_not_PR (AFP)
11:39:41 Session AFP/AnselmGod (AFP)
11:39:41 Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
11:39:41 Session AFP/Attack_Trees (AFP)
11:39:41 Session AFP/AxiomaticCategoryTheory (AFP)
11:39:41 Session AFP/Belief_Revision (AFP)
11:39:41 Session AFP/BinarySearchTree (AFP)
11:39:41 Session AFP/Binomial-Queues (AFP)
11:39:41 Session AFP/Bondy (AFP)
11:39:41 Session AFP/Boolos_Curious_Inference (AFP)
11:39:41 Session AFP/Boolos_Curious_Inference_Automated (AFP)
11:39:41 Session AFP/BytecodeLogicJmlTypes (AFP)
11:39:41 Session AFP/C2KA_DistributedSystems (AFP)
11:39:41 Session AFP/CISC-Kernel (AFP)
11:39:41 Session AFP/CYK (AFP)
11:39:41 Session AFP/Cauchy (AFP)
11:39:41 Session AFP/Sqrt_Babylonian (AFP)
11:39:41 Session Doc/Classes (doc)
11:39:41 Session AFP/ClockSynchInst (AFP)
11:39:41 Session AFP/Compiling-Exceptions-Correctly (AFP)
11:39:41 Session AFP/ComponentDependencies (AFP)
11:39:41 Session AFP/Concurrent_Revisions (AFP)
11:39:41 Session AFP/CondNormReasHOL (AFP)
11:39:41 Session AFP/Constructor_Funs (AFP)
11:39:41 Session AFP/CryptoBasedCompositionalProperties (AFP)
11:39:41 Session AFP/DCR-ExecutionEquivalence (AFP)
11:39:41 Session AFP/DPT-SAT-Solver (AFP)
11:39:41 Session AFP/Dedekind_Real (AFP)
11:39:41 Session Doc/Demo_EPTCS (doc)
11:39:41 Session Doc/Demo_Easychair (doc)
11:39:41 Session Doc/Demo_FoilTeX (doc)
11:39:41 Session Doc/Demo_LIPIcs (doc)
11:39:41 Session Doc/Demo_LLNCS (doc)
11:39:41 Session AFP/Depth-First-Search (AFP)
11:39:42 Session AFP/Digit_Expansions (AFP)
11:39:42 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
11:39:42 Session AFP/DiskPaxos (AFP)
11:39:42 Session AFP/Eudoxus_Reals (AFP)
11:39:42 Session AFP/Example-Submission (AFP)
11:39:42 Session AFP/FFT (AFP)
11:39:42 Session AFP/FLP (AFP)
11:39:42 Session AFP/FeatherweightJava (AFP)
11:39:42 Session AFP/Featherweight_OCL (AFP)
11:39:42 Session AFP/FileRefinement (AFP)
11:39:42 Session AFP/FocusStreamsCaseStudies (AFP)
11:39:42 Session AFP/Foundation_of_geometry (AFP)
11:39:42 Session AFP/Free-Boolean-Algebra (AFP)
11:39:42 Session AFP/Fresh_Identifiers (AFP)
11:39:42 Session AFP/FunWithFunctions (AFP)
11:39:42 Session AFP/FunWithTilings (AFP)
11:39:42 Session Doc/Functions (doc)
11:39:42 Session AFP/GPU_Kernel_PL (AFP)
11:39:42 Session AFP/GenClock (AFP)
11:39:42 Session AFP/General-Triangle (AFP)
11:39:42 Session AFP/Generic_Deriving (AFP)
11:39:43 Session AFP/GewirthPGCProof (AFP)
11:39:43 Session AFP/Go (AFP)
11:39:43 Session AFP/GoedelGod (AFP)
11:39:43 Session AFP/Goodstein_Lambda (AFP)
11:39:43 Session AFP/Gray_Codes (AFP)
11:39:43 Session HOL/HOL-Cardinals (timing)
11:39:43 Session AFP/Binding_Syntax_Theory (AFP)
11:39:43 Session AFP/Epistemic_Logic (AFP)
11:39:43 Session AFP/Public_Announcement_Logic (AFP)
11:39:43 Session AFP/Stalnaker_Logic (AFP)
11:39:43 Session AFP/Ordinals_and_Cardinals (AFP)
11:39:43 Session AFP/Risk_Free_Lending (AFP)
11:39:43 Session HOL/HOL-Hoare
11:39:43 Session HOL/HOL-Hoare_Parallel (timing)
11:39:43 Session HOL/HOL-IMPP
11:39:43 Session HOL/HOL-IOA
11:39:43 Session HOL/HOL-Import
11:39:43 Session HOL/HOL-Lattice
11:39:43 Session HOL/HOL-Library (main timing)
11:39:44 Session AFP/ADS_Functor (AFP)
11:39:44 Session AFP/Approximation_Algorithms (AFP)
11:39:44 Session AFP/ArrowImpossibilityGS (AFP)
11:39:44 Session AFP/Auto2_HOL (AFP)
11:39:44 Session AFP/BNF_CC (AFP)
11:39:44 Session AFP/BNF_Operations (AFP)
11:39:44 Session AFP/Binomial-Heaps (AFP)
11:39:44 Session AFP/Birkhoff_Finite_Distributive_Lattices (AFP)
11:39:45 Session AFP/Boolean_Expression_Checkers (AFP)
11:39:45 Session AFP/Bounded_Deducibility_Security (AFP)
11:39:45 Session AFP/BD_Security_Compositional (AFP)
11:39:45 Session AFP/CoSMeDis (AFP)
11:39:45 Session AFP/CoCon (AFP)
11:39:45 Session AFP/CoSMed (AFP)
11:39:45 Session AFP/Buildings (AFP)
11:39:45 Session AFP/CRDT (AFP)
11:39:45 Session AFP/IMAP-CRDT (AFP)
11:39:45 Session AFP/Card_Multisets (AFP)
11:39:45 Session AFP/Card_Number_Partitions (AFP)
11:39:45 Session AFP/Category (AFP)
11:39:45 Session Doc/Codegen (doc)
11:39:46 Session AFP/CofGroups (AFP)
11:39:46 Session AFP/CommCSL (AFP)
11:39:46 Session AFP/Complete_Non_Orders (AFP)
11:39:46 Session AFP/Completeness (AFP)
11:39:46 Session AFP/ConcurrentIMP (AFP)
11:39:46 Session AFP/Concurrent_Ref_Alg (AFP)
11:39:46 Session AFP/Conditional_Simplification (AFP)
11:39:46 Session AFP/Conditional_Transfer_Rule (AFP)
11:39:46 Session AFP/CoreC++ (AFP)
11:39:46 Session AFP/Core_DOM (AFP)
11:39:46 Session AFP/Shadow_DOM (AFP)
11:39:47 Session AFP/DOM_Components (AFP)
11:39:47 Session AFP/Core_SC_DOM (AFP)
11:39:47 Session AFP/Shadow_SC_DOM (AFP)
11:39:47 Session AFP/SC_DOM_Components (AFP)
11:39:47 Session AFP/Coupledsim_Contrasim (AFP)
11:39:47 Session Doc/Datatypes (doc)
11:39:48 Session Doc/Corec (doc)
11:39:48 Session AFP/Decl_Sem_Fun_PL (AFP)
11:39:48 Session AFP/Directed_Sets (AFP)
11:39:48 Session AFP/Earley_Parser (AFP)
11:39:48 Session AFP/Encodability_Process_Calculi (AFP)
11:39:48 Session AFP/Euler_Partition (AFP)
11:39:48 Session AFP/FOL-Fitting (AFP)
11:39:48 Session AFP/FOL_Seq_Calc1 (AFP)
11:39:48 Session AFP/FOL_Axiomatic (AFP)
11:39:48 Session AFP/FOL_Harrison (AFP)
11:39:48 Session AFP/Factored_Transition_System_Bounding (AFP)
11:39:48 Session AFP/FinFun (AFP)
11:39:48 Session AFP/Extended_Finite_State_Machines (AFP)
11:39:49 Session AFP/Extended_Finite_State_Machine_Inference (AFP)
11:39:49 Session AFP/Finger-Trees (AFP)
11:39:49 Session AFP/Finite-Map-Extras (AFP)
11:39:49 Session AFP/Fixed_Length_Vector (AFP)
11:39:49 Session AFP/Generalized_Counting_Sort (AFP)
11:39:49 Session AFP/Graph_Saturation (AFP)
11:39:49 Session AFP/Group-Ring-Module (AFP)
11:39:49 Session AFP/Valuation (AFP)
11:39:49 Session HOL/HOL-Auth (timing)
11:39:49 Session HOL/HOL-UNITY (timing)
11:39:50 Session HOL/HOL-Bali (timing)
11:39:50 Session HOL/HOL-Combinatorics (main timing)
11:39:50 Session AFP/Blue_Eyes (AFP)
11:39:50 Session AFP/Derangements (AFP)
11:39:51 Session AFP/Discrete_Summation (AFP)
11:39:51 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
11:39:51 Session AFP/Graph_Theory (AFP)
11:39:51 Session AFP/ShortestPath (AFP)
11:39:51 Session HOL/HOL-Computational_Algebra (main timing)
11:39:51 Session AFP/Descartes_Sign_Rule (AFP)
11:39:51 Session HOL/HOL-Algebra (main timing)
11:39:51 Session AFP/Edwards_Elliptic_Curves_Group (AFP)
11:39:51 Session AFP/Finitely_Generated_Abelian_Groups (AFP)
11:39:51 Session HOL/HOL-Decision_Procs (timing)
11:39:52 Session HOL/HOL-Quotient_Examples (timing)
11:39:52 Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
11:39:52 Session AFP/Localization_Ring (AFP)
11:39:52 Session AFP/Orbit_Stabiliser (AFP)
11:39:52 Session AFP/Perfect-Number-Thm (AFP)
11:39:52 Session AFP/Secondary_Sylow (AFP)
11:39:52 Session AFP/Jordan_Hoelder (AFP)
11:39:52 Session AFP/VectorSpace (AFP)
11:39:52 Session HOL/HOL-Examples
11:39:52 Session HOL/HOL-Isar_Examples
11:39:52 Session HOL/HOL-Nonstandard_Analysis (timing)
11:39:53 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
11:39:53 Session HOL/HOL-Number_Theory (main timing)
11:39:53 Session AFP/Arith_Prog_Rel_Primes (AFP)
11:39:53 Session AFP/DigitsInBase (AFP)
11:39:53 Session AFP/Elliptic_Curves_Group_Law (AFP)
11:39:53 Session AFP/Crypto_Standards (AFP)
11:39:53 Session AFP/Fermat3_4 (AFP)
11:39:53 Session HOL/HOL-Data_Structures (timing)
11:39:54 Session AFP/Efficient-Mergesort (AFP)
11:39:54 Session AFP/Go_Test_Quick (AFP)
11:39:54 Session AFP/Go_Test_Slow (AFP)
11:39:54 Session HOL/HOL-Codegenerator_Test
11:39:54 Session AFP/Query_Optimization (AFP)
11:39:55 Session HOL/HOL-ex (timing)
11:39:55 Session AFP/Lehmer (AFP)
11:39:55 Session AFP/Lifting_the_Exponent (AFP)
11:39:55 Session AFP/Padic_Ints (AFP)
11:39:55 Session AFP/Padic_Field (AFP)
11:39:55 Session AFP/Pratt_Certificate (AFP)
11:39:55 Session AFP/Bertrands_Postulate (AFP)
11:39:55 Session AFP/RSAPSS (AFP)
11:39:55 Session AFP/SumSquares (AFP)
11:39:56 Session AFP/Liouville_Numbers (AFP)
11:39:56 Session AFP/Lucas_Theorem (AFP)
11:39:56 Session AFP/DPRM_Theorem (AFP)
11:39:56 Session AFP/Mason_Stothers (AFP)
11:39:56 Session AFP/Polynomial_Interpolation (AFP)
11:39:56 Session AFP/Formal_Puiseux_Series (AFP)
11:39:56 Session AFP/Rep_Fin_Groups (AFP)
11:39:56 Session AFP/Sturm_Sequences (AFP)
11:39:56 Session AFP/Special_Function_Bounds (AFP)
11:39:56 Session AFP/Sturm_Tarski (AFP)
11:39:56 Session AFP/Budan_Fourier (AFP)
11:39:56 Session AFP/Three_Circles (AFP)
11:39:56 Session HOL/HOL-Corec_Examples (timing)
11:39:56 Session HOL/HOL-Datatype_Examples (timing)
11:39:56 Session HOL/HOL-IMP (timing)
11:39:57 Session AFP/Abs_Int_ITP2012 (AFP)
11:39:57 Session AFP/Relational-Incorrectness-Logic (AFP)
11:39:57 Session HOL/HOL-Imperative_HOL (timing)
11:39:57 Session AFP/Auto2_Imperative_HOL (AFP)
11:39:57 Session AFP/Imperative_Insertion_Sort (AFP)
11:39:57 Session HOL/HOL-Induct
11:39:57 Session HOL/HOL-Metis_Examples (timing)
11:39:57 Session HOL/HOL-Proofs (timing)
11:39:58 Session HOL/HOL-Proofs-Extraction (timing)
11:39:58 Session HOL/HOL-Proofs-ex
11:39:58 Session HOL/HOL-Proofs-Lambda (timing)
11:39:58 Session AFP/HereditarilyFinite (AFP)
11:39:58 Session AFP/HyperCTL (AFP)
11:39:58 Session AFP/IO_Language_Conformance (AFP)
11:39:58 Session AFP/Integration (AFP)
11:39:58 Session AFP/Isabelle_Meta_Model (AFP)
11:39:58 Session AFP/Isabelle_hoops (AFP)
11:39:58 Session AFP/LTL (AFP)
11:39:58 Session AFP/Stuttering_Equivalence (AFP)
11:39:58 Session AFP/Landau_Symbols (AFP)
11:39:59 Session AFP/LightweightJava (AFP)
11:39:59 Session AFP/LinearQuantifierElim (AFP)
11:39:59 Session AFP/List-Infinite (AFP)
11:39:59 Session AFP/Nat-Interval-Logic (AFP)
11:39:59 Session AFP/AutoFocus-Stream (AFP)
11:39:59 Session AFP/MuchAdoAboutTwo (AFP)
11:39:59 Session AFP/Order_Lattice_Props (AFP)
11:39:59 Session AFP/POPLmark-deBruijn (AFP)
11:39:59 Session AFP/Pairing_Heap (AFP)
11:39:59 Session AFP/Password_Authentication_Protocol (AFP)
11:39:59 Session AFP/Pell (AFP)
11:39:59 Session AFP/Prefix_Free_Code_Combinators (AFP)
11:39:59 Session AFP/Presburger-Automata (AFP)
11:39:59 Session AFP/Priority_Queue_Braun (AFP)
11:39:59 Session AFP/Program-Conflict-Analysis (AFP)
11:39:59 Session AFP/QBF_Solver_Verification (AFP)
11:39:59 Session AFP/Regular-Sets (AFP)
11:39:59 Session AFP/Abstract-Rewriting (AFP)
11:39:59 Session AFP/Decreasing-Diagrams (AFP)
11:39:59 Session AFP/Matrix (AFP)
11:40:00 Session AFP/Matrix_Tensor (AFP)
11:40:00 Session AFP/Knot_Theory (AFP)
11:40:00 Session AFP/Coinductive_Languages (AFP)
11:40:00 Session AFP/Finite_Automata_HF (AFP)
11:40:00 Session AFP/Functional-Automata (AFP)
11:40:00 Session AFP/Isabelle_DOF (AFP)
11:40:00 Session AFP/Posix-Lexing (AFP)
11:40:00 Session AFP/ResiduatedTransitionSystem (AFP)
11:40:00 Session AFP/Ribbon_Proofs (AFP)
11:40:00 Session AFP/SATSolverVerification (AFP)
11:40:00 Session AFP/Safe_OCL (AFP)
11:40:00 Session AFP/Schutz_Spacetime (AFP)
11:40:01 Session AFP/Selection_Heap_Sort (AFP)
11:40:01 Session AFP/Simplex (AFP)
11:40:01 Session AFP/Skew_Heap (AFP)
11:40:01 Session AFP/Sort_Encodings (AFP)
11:40:01 Session AFP/Splay_Tree (AFP)
11:40:01 Session AFP/Amortized_Complexity (AFP)
11:40:01 Session AFP/Dynamic_Tables (AFP)
11:40:01 Session AFP/Root_Balanced_Tree (AFP)
11:40:01 Session AFP/Stable_Matching (AFP)
11:40:01 Session AFP/SuperCalc (AFP)
11:40:01 Session Doc/System (doc)
11:40:01 Session AFP/Tail_Recursive_Functions (AFP)
11:40:01 Session AFP/TortoiseHare (AFP)
11:40:01 Session AFP/Trie (AFP)
11:40:01 Session AFP/Flyspeck-Tame (AFP)
11:40:01 Session AFP/Vickrey_Clarke_Groves (AFP)
11:40:01 Session AFP/Zeckendorf (AFP)
11:40:02 Session HOL/HOL-Matrix_LP
11:40:02 Session HOL/HOL-Mutabelle
11:40:02 Session HOL/HOL-NanoJava
11:40:02 Session HOL/HOL-Nitpick_Examples
11:40:02 Session HOL/HOL-Nominal
11:40:02 Session AFP/CCS (AFP)
11:40:02 Session HOL/HOL-Nominal-Examples (timing)
11:40:02 Session AFP/Lam-ml-Normalization (AFP)
11:40:02 Session AFP/Pi_Calculus (AFP)
11:40:02 Session AFP/Psi_Calculi (AFP)
11:40:02 Session AFP/Broadcast_Psi (AFP)
11:40:03 Session AFP/SequentInvertibility (AFP)
11:40:03 Session HOL/HOL-Predicate_Compile_Examples (timing)
11:40:03 Session HOL/HOL-Prolog
11:40:03 Session HOL/HOL-Quickcheck_Examples (timing)
11:40:03 Session HOL/HOL-Real_Asymp
11:40:04 Session HOL/HOL-Analysis (main timing)
11:40:05 Session AFP/Akra_Bazzi (AFP)
11:40:05 Session AFP/Closest_Pair_Points (AFP)
11:40:05 Session AFP/Cardinality_Continuum (AFP)
11:40:05 Session AFP/Catalan_Numbers (AFP)
11:40:05 Session AFP/Cayley_Hamilton (AFP)
11:40:06 Session AFP/Chebyshev_Polynomials (AFP)
11:40:06 Session AFP/Coinductive (AFP)
11:40:06 Session AFP/DynamicArchitectures (AFP)
11:40:06 Session AFP/Architectural_Design_Patterns (AFP)
11:40:06 Session AFP/Lazy-Lists-II (AFP)
11:40:06 Session AFP/Stream_Fusion_Code (AFP)
11:40:06 Session AFP/Topology (AFP)
11:40:06 Session AFP/Complex_Geometry (AFP)
11:40:06 Session AFP/Poincare_Disc (AFP)
11:40:06 Session AFP/Differential_Game_Logic (AFP)
11:40:06 Session AFP/Euler_Polyhedron_Formula (AFP)
11:40:06 Session AFP/First_Welfare_Theorem (AFP)
11:40:06 Session AFP/Furstenberg_Topology (AFP)
11:40:07 Session AFP/Green (AFP)
11:40:07 Session HOL/HOL-Analysis-ex
11:40:07 Session HOL/HOL-Complex_Analysis (main timing)
11:40:07 Session AFP/Bernoulli (AFP)
11:40:07 Session AFP/Cartan_FP (AFP)
11:40:07 Session AFP/Cotangent_PFD_Formula (AFP)
11:40:07 Session AFP/E_Transcendental (AFP)
11:40:07 Session AFP/Error_Function (AFP)
11:40:07 Session AFP/Euler_MacLaurin (AFP)
11:40:07 Session HOL/HOL-Eisbach
11:40:07 Session AFP/AOT (AFP)
11:40:08 Session AFP/Allen_Calculus (AFP)
11:40:08 Session AFP/Automatic_Refinement (AFP)
11:40:08 Session AFP/Refine_Monadic (AFP)
11:40:08 Session AFP/Card_Partitions (AFP)
11:40:08 Session AFP/Bell_Numbers_Spivey (AFP)
11:40:08 Session AFP/Card_Equiv_Relations (AFP)
11:40:08 Session AFP/Equivalence_Relation_Enumeration (AFP)
11:40:08 Session AFP/Falling_Factorial_Sum (AFP)
11:40:08 Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
11:40:08 Session AFP/Case_Labeling (AFP)
11:40:08 Session AFP/Clean (AFP)
11:40:09 Session AFP/Combinatorics_Words (AFP)
11:40:09 Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
11:40:09 Session AFP/Binary_Code_Imprimitive (AFP)
11:40:09 Session AFP/Two_Generated_Word_Monoids_Intersection (AFP)
11:40:09 Session AFP/Cook_Levin (AFP)
11:40:09 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
11:40:09 Session AFP/Dependent_SIFUM_Refinement (AFP)
11:40:10 Session Doc/Eisbach (doc)
11:40:10 Session HOL/HOL-MicroJava (timing)
11:40:10 Session AFP/Optics (AFP)
11:40:10 Session AFP/ConcurrentHOL (AFP)
11:40:10 Session AFP/UTP-Toolkit (AFP)
11:40:10 Session AFP/UTP (AFP)
11:40:10 Session AFP/Solidity (AFP)
11:40:10 Session AFP/Twelvefold_Way (AFP)
11:40:10 Session HOL/HOL-Hahn_Banach
11:40:10 Session HOL/HOL-Homology (timing)
11:40:11 Session HOL/HOL-Mirabelle-ex
11:40:11 Session HOL/HOL-Probability (main timing)
11:40:11 Session AFP/Actuarial_Mathematics (AFP)
11:40:11 Session AFP/Applicative_Lifting (AFP)
11:40:11 Session AFP/Free-Groups (AFP)
11:40:12 Session AFP/Stern_Brocot (AFP)
11:40:12 Session AFP/Buffons_Needle (AFP)
11:40:12 Session AFP/Density_Compiler (AFP)
11:40:12 Session AFP/DiscretePricing (AFP)
11:40:12 Session AFP/Ergodic_Theory (AFP)
11:40:12 Session AFP/Gromov_Hyperbolicity (AFP)
11:40:12 Session AFP/Laws_of_Large_Numbers (AFP)
11:40:12 Session AFP/Fisher_Yates (AFP)
11:40:12 Session AFP/Girth_Chromatic (AFP)
11:40:12 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
11:40:12 Session AFP/Szemeredi_Regularity (AFP)
11:40:12 Session HOL/HOL-Probability-ex (timing)
11:40:12 Session AFP/Hahn_Jordan_Decomposition (AFP)
11:40:12 Session AFP/Lp (AFP)
11:40:12 Session AFP/Concentration_Inequalities (AFP)
11:40:13 Session AFP/Fourier (AFP)
11:40:13 Session AFP/MDP-Rewards (AFP)
11:40:13 Session AFP/Markov_Models (AFP)
11:40:13 Session AFP/Martingales (AFP)
11:40:13 Session AFP/Doob_Convergence (AFP)
11:40:13 Session AFP/Monad_Normalisation (AFP)
11:40:13 Session AFP/Monomorphic_Monad (AFP)
11:40:13 Session AFP/Neumann_Morgenstern_Utility (AFP)
11:40:13 Session AFP/Probabilistic_Noninterference (AFP)
11:40:13 Session AFP/Probabilistic_Prime_Tests (AFP)
11:40:14 Session AFP/Probabilistic_System_Zoo (AFP)
11:40:14 Session AFP/Quasi_Borel_Spaces (AFP)
11:40:14 Session AFP/Roth_Arithmetic_Progressions (AFP)
11:40:14 Session AFP/Skip_Lists (AFP)
11:40:14 Session AFP/Source_Coding_Theorem (AFP)
11:40:14 Session AFP/Standard_Borel_Spaces (AFP)
11:40:14 Session AFP/S_Finite_Measure_Monad (AFP)
11:40:14 Session AFP/Disintegration (AFP)
11:40:14 Session AFP/Turans_Graph_Theorem (AFP)
11:40:14 Session AFP/Hyperdual (AFP)
11:40:15 Session AFP/Interval_Analysis (AFP)
11:40:15 Session AFP/Irrationality_J_Hancl (AFP)
11:40:15 Session AFP/Kuratowski_Closure_Complement (AFP)
11:40:15 Session AFP/Laplace_Transform (AFP)
11:40:15 Session AFP/Lower_Semicontinuous (AFP)
11:40:15 Session AFP/Minkowskis_Theorem (AFP)
11:40:15 Session AFP/Octonions (AFP)
11:40:15 Session AFP/Polynomial_Crit_Geometry (AFP)
11:40:15 Session AFP/Prime_Harmonic_Series (AFP)
11:40:15 Session AFP/Ptolemys_Theorem (AFP)
11:40:15 Session AFP/Quaternions (AFP)
11:40:15 Session AFP/Rank_Nullity_Theorem (AFP)
11:40:15 Session AFP/Gauss_Jordan (AFP)
11:40:15 Session AFP/Echelon_Form (AFP)
11:40:15 Session AFP/Hermite (AFP)
11:40:15 Session AFP/Safe_Distance (AFP)
11:40:16 Session AFP/Tarskis_Geometry (AFP)
11:40:16 Session AFP/Triangle (AFP)
11:40:16 Session AFP/Ceva (AFP)
11:40:16 Session AFP/Chord_Segments (AFP)
11:40:16 Session AFP/Stewart_Apollonius (AFP)
11:40:16 Session AFP/Winding_Number_Eval (AFP)
11:40:16 Session AFP/Count_Complex_Roots (AFP)
11:40:16 Session AFP/Youngs_Inequality (AFP)
11:40:16 Session AFP/pGCL (AFP)
11:40:16 Session HOL/HOL-Real_Asymp-Manual
11:40:16 Session AFP/Sophomores_Dream (AFP)
11:40:16 Session AFP/Stirling_Formula (AFP)
11:40:16 Session AFP/Irrationals_From_THEBOOK (AFP)
11:40:16 Session AFP/Lambert_W (AFP)
11:40:16 Session HOL/HOL-SET_Protocol (timing)
11:40:16 Session HOL/HOL-SMT_Examples (timing)
11:40:17 Session HOL/HOL-SPARK
11:40:17 Session HOL/HOL-SPARK-Examples
11:40:17 Session AFP/RIPEMD-160-SPARK (AFP)
11:40:17 Session HOL/HOL-SPARK-Manual
11:40:17 Session HOL/HOL-Statespace
11:40:17 Session HOL/HOL-TLA
11:40:17 Session HOL/HOL-TLA-Buffer
11:40:17 Session HOL/HOL-TLA-Inc
11:40:17 Session HOL/HOL-TLA-Memory
11:40:17 Session HOL/HOL-TPTP
11:40:17 Session HOL/HOL-Types_To_Sets
11:40:17 Session AFP/Banach_Steinhaus (AFP)
11:40:17 Session AFP/Smooth_Manifolds (AFP)
11:40:17 Session AFP/Types_To_Sets_Extension (AFP)
11:40:17 Session HOL/HOL-Unix
11:40:17 Session HOL/HOL-ZF
11:40:18 Session AFP/Category2 (AFP)
11:40:18 Session HOL/HOLCF (main timing)
11:40:18 Session AFP/Circus (AFP)
11:40:18 Session AFP/HOL-CSP (AFP)
11:40:18 Session AFP/HOL-CSPM (AFP)
11:40:18 Session AFP/HOL-CSP_OpSem (AFP)
11:40:18 Session HOL/HOLCF-IMP
11:40:18 Session HOL/HOLCF-Library
11:40:18 Session AFP/CSP_RefTK (AFP)
11:40:19 Session HOL/HOLCF-FOCUS
11:40:19 Session HOL/HOLCF-ex
11:40:19 Session AFP/PCF (AFP)
11:40:19 Session AFP/HOLCF-Prelude (AFP)
11:40:19 Session AFP/BirdKMP (AFP)
11:40:19 Session HOL/HOLCF-Tutorial
11:40:19 Session HOL/IOA (timing)
11:40:19 Session HOL/IOA-ABP
11:40:19 Session HOL/IOA-NTP
11:40:19 Session HOL/IOA-Storage
11:40:19 Session HOL/IOA-ex
11:40:19 Session AFP/Shivers-CFA (AFP)
11:40:19 Session AFP/Stream-Fusion (AFP)
11:40:19 Session AFP/Tycon (AFP)
11:40:19 Session AFP/WorkerWrapper (AFP)
11:40:20 Session AFP/Hales_Jewett (AFP)
11:40:20 Session Misc/Haskell
11:40:20 Session AFP/Heard_Of (AFP)
11:40:20 Session AFP/Consensus_Refined (AFP)
11:40:20 Session AFP/Hello_World (AFP)
11:40:20 Session AFP/HoareForDivergence (AFP)
11:40:20 Session AFP/Hood_Melville_Queue (AFP)
11:40:20 Session AFP/HotelKeyCards (AFP)
11:40:20 Session Doc/How_to_Prove_it (no_doc)
11:40:20 Session AFP/Huffman (AFP)
11:40:20 Session AFP/Hybrid_Logic (AFP)
11:40:20 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
11:40:20 Session AFP/HyperHoareLogic (AFP)
11:40:20 Session AFP/IFC_Tracking (AFP)
11:40:20 Session AFP/IMP2 (AFP)
11:40:20 Session AFP/IMP2_Binary_Heap (AFP)
11:40:20 Session AFP/IMP_Compiler (AFP)
11:40:20 Session AFP/IMP_Compiler_Reuse (AFP)
11:40:21 Session AFP/IMP_Noninterference (AFP)
11:40:21 Session Doc/Implementation (doc)
11:40:21 Session AFP/Implicational_Logic (AFP)
11:40:21 Session AFP/Impossible_Geometry (AFP)
11:40:21 Session AFP/Inductive_Confidentiality (AFP)
11:40:21 Session AFP/Inductive_Inference (AFP)
11:40:21 Session AFP/InfPathElimination (AFP)
11:40:21 Session AFP/Intro_Dest_Elim (AFP)
11:40:21 Session AFP/Involutions2Squares (AFP)
11:40:21 Session AFP/IsaGeoCoq (AFP)
11:40:21 Session AFP/IsaNet (AFP)
11:40:21 Session Doc/Isar_Ref (doc)
11:40:21 Session AFP/Isabelle_C (AFP)
11:40:21 Session Doc/JEdit (doc)
11:40:22 Session AFP/Jacobson_Basic_Algebra (AFP)
11:40:22 Session AFP/Grothendieck_Schemes (AFP)
11:40:22 Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
11:40:22 Session AFP/Khovanskii_Theorem (AFP)
11:40:22 Session AFP/Kneser_Cauchy_Davenport (AFP)
11:40:22 Session AFP/JiveDataStoreModel (AFP)
11:40:22 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
11:40:22 Session AFP/Kleene_Algebra (AFP)
11:40:22 Session AFP/KAD (AFP)
11:40:22 Session AFP/KAT_and_DRA (AFP)
11:40:22 Session AFP/Algebraic_VCs (AFP)
11:40:22 Session AFP/Multirelations (AFP)
11:40:22 Session AFP/Quantales (AFP)
11:40:22 Session AFP/Transformer_Semantics (AFP)
11:40:22 Session AFP/Regular_Algebras (AFP)
11:40:22 Session AFP/Relation_Algebra (AFP)
11:40:22 Session AFP/Relational_Paths (AFP)
11:40:23 Session AFP/Residuated_Lattices (AFP)
11:40:23 Session AFP/Knights_Tour (AFP)
11:40:23 Session AFP/LambdaMu (AFP)
11:40:23 Session AFP/LatticeProperties (AFP)
11:40:23 Session AFP/DataRefinementIBP (AFP)
11:40:23 Session AFP/GraphMarkingIBP (AFP)
11:40:23 Session AFP/Lazy_Case (AFP)
11:40:23 Session AFP/Lifting_Definition_Option (AFP)
11:40:23 Session AFP/List-Index (AFP)
11:40:23 Session AFP/Comparison_Sort_Lower_Bound (AFP)
11:40:23 Session AFP/Jinja (AFP)
11:40:23 Session AFP/Dominance_CHK (AFP)
11:40:23 Session AFP/HRB-Slicing (AFP)
11:40:23 Session AFP/InformationFlowSlicing_Inter (AFP)
11:40:23 Session AFP/Slicing (AFP)
11:40:23 Session AFP/InformationFlowSlicing (AFP)
11:40:23 Session AFP/JinjaDCI (AFP)
11:40:24 Session AFP/Regression_Test_Selection (AFP)
11:40:24 Session AFP/List_Update (AFP)
11:40:24 Session AFP/Quick_Sort_Cost (AFP)
11:40:24 Session AFP/Random_BSTs (AFP)
11:40:24 Session AFP/Randomised_BSTs (AFP)
11:40:24 Session AFP/Treaps (AFP)
11:40:24 Session AFP/Randomised_Social_Choice (AFP)
11:40:24 Session AFP/Fishburn_Impossibility (AFP)
11:40:24 Session AFP/PAPP_Impossibility (AFP)
11:40:24 Session AFP/SDS_Impossibility (AFP)
11:40:24 Session AFP/List_Interleaving (AFP)
11:40:24 Session AFP/List_Inversions (AFP)
11:40:25 Session AFP/LocalLexing (AFP)
11:40:25 Session Doc/Locales (doc)
11:40:25 Session AFP/Locally-Nameless-Sigma (AFP)
11:40:25 Session AFP/Logging_Independent_Anonymity (AFP)
11:40:25 Session AFP/Lowe_Ontological_Argument (AFP)
11:40:25 Session AFP/MHComputation (AFP)
11:40:25 Session AFP/MLSS_Decision_Proc (AFP)
11:40:25 Session AFP/ML_Unification (AFP)
11:40:25 Session Doc/Main (doc)
11:40:25 Session AFP/Marriage (AFP)
11:40:25 Session AFP/Latin_Square (AFP)
11:40:25 Session AFP/Matroids (AFP)
11:40:25 Session AFP/Max-Card-Matching (AFP)
11:40:25 Session AFP/Maximum_Segment_Sum (AFP)
11:40:25 Session AFP/Median_Of_Medians_Selection (AFP)
11:40:26 Session AFP/KD_Tree (AFP)
11:40:26 Session AFP/Menger (AFP)
11:40:26 Session AFP/Mereology (AFP)
11:40:26 Session AFP/Metalogic_ProofChecker (AFP)
11:40:26 Session AFP/MiniML (AFP)
11:40:26 Session AFP/Modular_Assembly_Kit_Security (AFP)
11:40:26 Session AFP/MonoBoolTranAlgebra (AFP)
11:40:26 Session AFP/Multirelations_Heterogeneous (AFP)
11:40:26 Session AFP/Multitape_To_Singletape_TM (AFP)
11:40:26 Session AFP/Name_Carrying_Type_Inference (AFP)
11:40:26 Session AFP/Nano_JSON (AFP)
11:40:26 Session AFP/Nash_Williams (AFP)
11:40:26 Session AFP/No_FTL_observers (AFP)
11:40:26 Session AFP/No_FTL_observers_Gen_Rel (AFP)
11:40:26 Session AFP/Nominal2 (AFP)
11:40:27 Session AFP/Incompleteness (AFP)
11:40:27 Session AFP/Surprise_Paradox (AFP)
11:40:27 Session AFP/LambdaAuth (AFP)
11:40:27 Session AFP/Launchbury (AFP)
11:40:28 Session AFP/Call_Arity (AFP)
11:40:28 Session AFP/Modal_Logics_for_NTS (AFP)
11:40:28 Session AFP/Rewriting_Z (AFP)
11:40:28 Session AFP/Nominal_Myhill_Nerode (AFP)
11:40:28 Session AFP/Noninterference_CSP (AFP)
11:40:28 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
11:40:28 Session AFP/Noninterference_Generic_Unwinding (AFP)
11:40:28 Session AFP/Noninterference_Inductive_Unwinding (AFP)
11:40:28 Session AFP/Noninterference_Sequential_Composition (AFP)
11:40:28 Session AFP/Noninterference_Concurrent_Composition (AFP)
11:40:28 Session AFP/NormByEval (AFP)
11:40:28 Session AFP/OpSets (AFP)
11:40:29 Session AFP/Open_Induction (AFP)
11:40:29 Session AFP/Well_Quasi_Orders (AFP)
11:40:29 Session AFP/Decreasing-Diagrams-II (AFP)
11:40:29 Session AFP/Myhill-Nerode (AFP)
11:40:29 Session AFP/Ordinal (AFP)
11:40:29 Session AFP/Nested_Multisets_Ordinals (AFP)
11:40:29 Session AFP/Design_Theory (AFP)
11:40:29 Session AFP/Lovasz_Local (AFP)
11:40:29 Session AFP/Undirected_Graph_Theory (AFP)
11:40:29 Session AFP/Balog_Szemeredi_Gowers (AFP)
11:40:29 Session AFP/Lambda_Free_RPOs (AFP)
11:40:29 Session AFP/Lambda_Free_EPO (AFP)
11:40:30 Session AFP/Substitutions_Lambda_Free (AFP)
11:40:30 Session AFP/Ordered_Resolution_Prover (AFP)
11:40:30 Session AFP/Chandy_Lamport (AFP)
11:40:30 Session AFP/Saturation_Framework (AFP)
11:40:30 Session AFP/Progress_Tracking (AFP)
11:40:30 Session AFP/PAL (AFP)
11:40:30 Session AFP/PLM (AFP)
11:40:30 Session AFP/PSemigroupsConvolution (AFP)
11:40:30 Session AFP/Package_logic (AFP)
11:40:30 Session AFP/Combinable_Wands (AFP)
11:40:30 Session AFP/Paraconsistency (AFP)
11:40:30 Session AFP/Parity_Game (AFP)
11:40:30 Session AFP/GaleStewart_Games (AFP)
11:40:30 Session AFP/Partial_Function_MR (AFP)
11:40:30 Session AFP/Physical_Quantities (AFP)
11:40:31 Session AFP/Pop_Refinement (AFP)
11:40:31 Session AFP/Possibilistic_Noninterference (AFP)
11:40:31 Session AFP/Priority_Search_Trees (AFP)
11:40:31 Session AFP/Prim_Dijkstra_Simple (AFP)
11:40:31 Session Doc/Prog_Prove (doc)
11:40:31 Session AFP/Projective_Geometry (AFP)
11:40:31 Session AFP/Proof_Strategy_Language (AFP)
11:40:31 Session AFP/PropResPI (AFP)
11:40:31 Session AFP/Propositional_Logic_Class (AFP)
11:40:31 Session AFP/Propositional_Proof_Systems (AFP)
11:40:32 Session AFP/PseudoHoops (AFP)
11:40:32 Session AFP/Quantales_Converse (AFP)
11:40:32 Session AFP/Catoids (AFP)
11:40:32 Session AFP/CubicalCategories (AFP)
11:40:32 Session AFP/OmegaCatoidsQuantales (AFP)
11:40:32 Session AFP/Ramsey-Infinite (AFP)
11:40:32 Session AFP/Real_Power (AFP)
11:40:32 Session AFP/Real_Time_Deque (AFP)
11:40:32 Session AFP/Recursion-Theory-I (AFP)
11:40:32 Session AFP/Minsky_Machines (AFP)
11:40:32 Session AFP/RefinementReactive (AFP)
11:40:32 Session AFP/Regex_Equivalence (AFP)
11:40:32 Session AFP/Region_Quadtrees (AFP)
11:40:32 Session AFP/Relational_Method (AFP)
11:40:32 Session AFP/Rensets (AFP)
11:40:32 Session AFP/Robbins-Conjecture (AFP)
11:40:33 Session AFP/Roy_Floyd_Warshall (AFP)
11:40:33 Session AFP/SCC_Bloemen_Sequential (AFP)
11:40:33 Session AFP/SIFPL (AFP)
11:40:33 Session AFP/SIFUM_Type_Systems (AFP)
11:40:33 Session AFP/Sauer_Shelah_Lemma (AFP)
11:40:33 Session AFP/Security_Protocol_Refinement (AFP)
11:40:33 Session AFP/SenSocialChoice (AFP)
11:40:33 Session AFP/Separation_Algebra (AFP)
11:40:33 Session AFP/Hoare_Time (AFP)
11:40:33 Session AFP/Separata (AFP)
11:40:33 Session AFP/Separation_Logic_Unbounded (AFP)
11:40:33 Session AFP/Simpl (AFP)
11:40:34 Session AFP/BDD (AFP)
11:40:34 Session AFP/SimplifiedOntologicalArgument (AFP)
11:40:34 Session AFP/Sliding_Window_Algorithm (AFP)
11:40:34 Session AFP/Statecharts (AFP)
11:40:34 Session AFP/Stellar_Quorums (AFP)
11:40:34 Session AFP/Stone_Algebras (AFP)
11:40:34 Session AFP/Stone_Relation_Algebras (AFP)
11:40:34 Session AFP/Relational_Cardinality (AFP)
11:40:34 Session AFP/Stone_Kleene_Relation_Algebras (AFP)
11:40:34 Session AFP/Aggregation_Algebras (AFP)
11:40:34 Session AFP/Relational_Disjoint_Set_Forests (AFP)
11:40:34 Session AFP/Relational_Minimum_Spanning_Trees (AFP)
11:40:34 Session AFP/Relational_Forests (AFP)
11:40:34 Session AFP/Subset_Boolean_Algebras (AFP)
11:40:34 Session AFP/Correctness_Algebras (AFP)
11:40:35 Session AFP/Store_Buffer_Reduction (AFP)
11:40:35 Session AFP/StrictOmegaCategories (AFP)
11:40:35 Session AFP/Strong_Security (AFP)
11:40:35 Session Doc/Sugar (doc)
11:40:35 Session AFP/Sunflowers (AFP)
11:40:35 Session AFP/Clique_and_Monotone_Circuits (AFP)
11:40:35 Session AFP/Suppes_Theorem (AFP)
11:40:35 Session AFP/Probability_Inequality_Completeness (AFP)
11:40:35 Session AFP/Syntax_Independent_Logic (AFP)
11:40:35 Session AFP/Goedel_Incompleteness (AFP)
11:40:35 Session AFP/Goedel_HFSet_Semantic (AFP)
11:40:36 Session AFP/Goedel_HFSet_Semanticless (AFP)
11:40:36 Session AFP/Robinson_Arithmetic (AFP)
11:40:36 Session AFP/Synthetic_Completeness (AFP)
11:40:36 Session AFP/Szpilrajn (AFP)
11:40:36 Session AFP/Combinatorics_Words_Lyndon (AFP)
11:40:36 Session AFP/TESL_Language (AFP)
11:40:37 Session AFP/TLA (AFP)
11:40:37 Session AFP/Timed_Automata (AFP)
11:40:37 Session AFP/Probabilistic_Timed_Automata (AFP)
11:40:37 Session AFP/Top_Down_Solver (AFP)
11:40:37 Session AFP/Topological_Semantics (AFP)
11:40:37 Session AFP/Transitive-Closure-II (AFP)
11:40:37 Session AFP/Transport (AFP)
11:40:37 Session AFP/Tree_Decomposition (AFP)
11:40:37 Session AFP/Tree_Enumeration (AFP)
11:40:38 Session Doc/Tutorial (doc)
11:40:38 Session Doc/Typeclass_Hierarchy (doc)
11:40:38 Session AFP/Types_Tableaus_and_Goedels_God (AFP)
11:40:38 Session AFP/UPF (AFP)
11:40:38 Session AFP/UPF_Firewall (AFP)
11:40:38 Session AFP/Universal_Turing_Machine (AFP)
11:40:39 Session AFP/Van_der_Waerden (AFP)
11:40:39 Session AFP/VeriComp (AFP)
11:40:39 Session AFP/Interpreter_Optimizations (AFP)
11:40:39 Session AFP/Verified-Prover (AFP)
11:40:39 Session AFP/VolpanoSmith (AFP)
11:40:39 Session AFP/WHATandWHERE_Security (AFP)
11:40:39 Session AFP/Weight_Balanced_Trees (AFP)
11:40:39 Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
11:40:39 Session AFP/Word_Lib (AFP)
11:40:39 Session AFP/AutoCorres2 (AFP)
11:40:40 Session AFP/AutoCorres2_Main (AFP)
11:40:41 Session AFP/AutoCorres2_Test (AFP)
11:40:41 Session AFP/Complx (AFP)
11:40:41 Session AFP/IEEE_Floating_Point (AFP)
11:40:41 Session AFP/IP_Addresses (AFP)
11:40:41 Session AFP/Simple_Firewall (AFP)
11:40:41 Session AFP/Routing (AFP)
11:40:41 Session AFP/Interval_Arithmetic_Word32 (AFP)
11:40:41 Session AFP/LEM (AFP)
11:40:42 Session AFP/Native_Word (AFP)
11:40:42 Session AFP/Collections (AFP)
11:40:42 Session AFP/Abstract_Completeness (AFP)
11:40:42 Session AFP/Abstract_Soundness (AFP)
11:40:42 Session AFP/FOL_Seq_Calc3 (AFP)
11:40:42 Session AFP/Incredible_Proof_Machine (AFP)
11:40:42 Session AFP/Deriving (AFP)
11:40:42 Session AFP/CAVA_Base (AFP)
11:40:43 Session AFP/CAVA_Automata (AFP)
11:40:43 Session AFP/DFS_Framework (AFP)
11:40:43 Session AFP/Gabow_SCC (AFP)
11:40:43 Session AFP/LTL_to_GBA (AFP)
11:40:43 Session AFP/Promela (AFP)
11:40:43 Session AFP/Containers (AFP)
11:40:43 Session AFP/CHERI-C_Memory_Model (AFP)
11:40:43 Session AFP/Collections_Examples (AFP)
11:40:43 Session AFP/Containers-Benchmarks (AFP)
11:40:44 Session AFP/Eval_FO (AFP)
11:40:44 Session AFP/MFOTL_Monitor (AFP)
11:40:44 Session AFP/Generic_Join (AFP)
11:40:44 Session AFP/MFODL_Monitor_Optimized (AFP)
11:40:44 Session AFP/MFOTL_Checker (AFP)
11:40:44 Session AFP/VYDRA_MDL (AFP)
11:40:44 Session AFP/Formula_Derivatives (AFP)
11:40:44 Session AFP/Labeled_Transition_Systems (AFP)
11:40:44 Session AFP/Pushdown_Systems (AFP)
11:40:44 Session AFP/MSO_Regex_Equivalence (AFP)
11:40:44 Session AFP/Show (AFP)
11:40:45 Session AFP/Affine_Arithmetic (AFP)
11:40:45 Session AFP/Ordinary_Differential_Equations (AFP)
11:40:45 Session AFP/Differential_Dynamic_Logic (AFP)
11:40:45 Session AFP/Hybrid_Systems_VCs (AFP)
11:40:45 Session AFP/Matrices_for_ODEs (AFP)
11:40:46 Session AFP/Taylor_Models (AFP)
11:40:46 Session AFP/CakeML (AFP)
11:40:46 Session AFP/Certification_Monads (AFP)
11:40:46 Session AFP/AI_Planning_Languages_Semantics (AFP)
11:40:46 Session AFP/Verified_SAT_Based_AI_Planning (AFP)
11:40:46 Session AFP/Dict_Construction (AFP)
11:40:46 Session AFP/Formula_Derivatives-Examples (AFP)
11:40:46 Session AFP/LL1_Parser (AFP)
11:40:47 Session AFP/Monad_Memo_DP (AFP)
11:40:47 Session AFP/Hidden_Markov_Models (AFP)
11:40:47 Session AFP/Optimal_BST (AFP)
11:40:47 Session AFP/Polynomial_Factorization (AFP)
11:40:47 Session AFP/Amicable_Numbers (AFP)
11:40:47 Session AFP/Continued_Fractions (AFP)
11:40:47 Session AFP/Dirichlet_Series (AFP)
11:40:47 Session AFP/Zeta_Function (AFP)
11:40:48 Session AFP/Dirichlet_L (AFP)
11:40:48 Session AFP/Gauss_Sums (AFP)
11:40:48 Session AFP/Three_Squares (AFP)
11:40:48 Session AFP/Polygonal_Number_Theorem (AFP)
11:40:48 Session AFP/Wieferich_Kempner (AFP)
11:40:49 Session AFP/Kummer_Congruence (AFP)
11:40:49 Session AFP/Prime_Number_Theorem (AFP)
11:40:49 Session AFP/PNT_with_Remainder (AFP)
11:40:49 Session AFP/Prime_Distribution_Elementary (AFP)
11:40:49 Session AFP/IMO2019 (AFP)
11:40:49 Session AFP/Irrational_Series_Erdos_Straus (AFP)
11:40:49 Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
11:40:49 Session AFP/Zeta_3_Irrational (AFP)
11:40:49 Session AFP/First_Order_Terms (AFP)
11:40:49 Session AFP/Resolution_FOL (AFP)
11:40:50 Session AFP/Saturation_Framework_Extensions (AFP)
11:40:50 Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
11:40:50 Session AFP/Automated_Stateful_Protocol_Verification (AFP)
11:40:50 Session AFP/Gaussian_Integers (AFP)
11:40:50 Session AFP/Jordan_Normal_Form (AFP)
11:40:50 Session AFP/Farkas (AFP)
11:40:51 Session AFP/Isabelle_Marries_Dirac (AFP)
11:40:51 Session AFP/Knuth_Bendix_Order (AFP)
11:40:51 Session AFP/Functional_Ordered_Resolution_Prover (AFP)
11:40:51 Session AFP/Simple_Clause_Learning (AFP)
11:40:51 Session AFP/Regular_Tree_Relations (AFP)
11:40:51 Session AFP/FO_Theory_Rewriting (AFP)
11:40:52 Session AFP/Rewrite_Properties_Reduction (AFP)
11:40:52 Session AFP/Weighted_Path_Order (AFP)
11:40:52 Session AFP/Efficient_Weighted_Path_Order (AFP)
11:40:52 Session AFP/Given_Clause_Loops (AFP)
11:40:52 Session AFP/Multiset_Ordering_NPC (AFP)
11:40:52 Session AFP/Linear_Recurrences (AFP)
11:40:52 Session AFP/Polylog (AFP)
11:40:52 Session AFP/Lambert_Series (AFP)
11:40:52 Session AFP/Perron_Frobenius (AFP)
11:40:53 Session AFP/MDP-Algorithms (AFP)
11:40:53 Session AFP/Stochastic_Matrices (AFP)
11:40:53 Session AFP/Subresultants (AFP)
11:40:53 Session AFP/Berlekamp_Zassenhaus (AFP)
11:40:54 Session AFP/Algebraic_Numbers (AFP)
11:40:54 Session AFP/BenOr_Kozen_Reif (AFP)
11:40:54 Session AFP/LLL_Basis_Reduction (AFP)
11:40:54 Session AFP/CVP_Hardness (AFP)
11:40:54 Session AFP/LLL_Factorization (AFP)
11:40:54 Session AFP/Linear_Inequalities (AFP)
11:40:54 Session AFP/LP_Duality (AFP)
11:40:54 Session AFP/Linear_Programming (AFP)
11:40:54 Session AFP/Number_Theoretic_Transform (AFP)
11:40:54 Session AFP/CRYSTALS-Kyber (AFP)
11:40:55 Session AFP/Perfect_Fields (AFP)
11:40:55 Session AFP/Elimination_Of_Repeated_Factors (AFP)
11:40:55 Session AFP/Smith_Normal_Form (AFP)
11:40:55 Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
11:40:56 Session AFP/Polynomials (AFP)
11:40:56 Session AFP/Deep_Learning (AFP)
11:40:56 Session AFP/QHLProver (AFP)
11:40:56 Session AFP/Projective_Measurements (AFP)
11:40:57 Session AFP/Commuting_Hermitian (AFP)
11:40:57 Session AFP/TsirelsonBound (AFP)
11:40:57 Session AFP/Uncertainty_Principle (AFP)
11:40:57 Session AFP/Groebner_Bases (AFP)
11:40:57 Session AFP/Fishers_Inequality (AFP)
11:40:57 Session AFP/Hypergraph_Basics (AFP)
11:40:57 Session AFP/Hypergraph_Colourings (AFP)
11:40:58 Session AFP/Groebner_Macaulay (AFP)
11:40:58 Session AFP/Nullstellensatz (AFP)
11:40:58 Session AFP/Signature_Groebner (AFP)
11:40:58 Session AFP/Lambda_Free_KBOs (AFP)
11:40:58 Session AFP/Sumcheck_Protocol (AFP)
11:40:58 Session AFP/Symmetric_Polynomials (AFP)
11:40:58 Session AFP/Pi_Transcendental (AFP)
11:40:58 Session AFP/Power_Sum_Polynomials (AFP)
11:40:58 Session AFP/Hermite_Lindemann (AFP)
11:40:59 Session AFP/Factor_Algebraic_Polynomial (AFP)
11:40:59 Session AFP/Cubic_Quartic_Equations (AFP)
11:40:59 Session AFP/Linear_Recurrences_Solver (AFP)
11:40:59 Session AFP/Orient_Rewrite_Rule_Undecidable (AFP)
11:40:59 Session AFP/Schwartz_Zippel (AFP)
11:40:59 Session AFP/Virtual_Substitution (AFP)
11:41:00 Session AFP/Real_Impl (AFP)
11:41:00 Session AFP/Complex_Bounded_Operators_Dependencies (AFP)
11:41:01 Session AFP/Complex_Bounded_Operators (AFP)
11:41:01 Session AFP/Registers (AFP)
11:41:01 Session AFP/QR_Decomposition (AFP)
11:41:01 Session AFP/XML (AFP)
11:41:01 Session AFP/Van_Emde_Boas_Trees (AFP)
11:41:02 Session AFP/Dijkstra_Shortest_Path (AFP)
11:41:02 Session AFP/Koenigsberg_Friendship (AFP)
11:41:02 Session AFP/FOL_Seq_Calc2 (AFP)
11:41:02 Session AFP/Formal_SSA (AFP)
11:41:02 Session AFP/Minimal_SSA (AFP)
11:41:02 Session AFP/Gale_Shapley (AFP)
11:41:02 Session AFP/HOL-ODE-Numerics (AFP)
11:41:03 Session AFP/HOL-ODE-ARCH-COMP (AFP)
11:41:03 Session AFP/HOL-ODE-Examples (AFP large)
11:41:03 Session AFP/Lorenz_Approximation (AFP)
11:41:03 Session AFP/Lorenz_C0 (AFP large)
11:41:03 Session AFP/Lorenz_C1 (AFP large)
11:41:03 Session AFP/Poincare_Bendixson (AFP)
11:41:03 Session AFP/Picks_Theorem (AFP)
11:41:04 Session AFP/KnuthMorrisPratt (AFP)
11:41:04 Session AFP/Safe_Range_RC (AFP)
11:41:04 Session AFP/Transition_Systems_and_Automata (AFP)
11:41:04 Session AFP/Adaptive_State_Counting (AFP)
11:41:04 Session AFP/Buchi_Complementation (AFP)
11:41:04 Session AFP/LTL_Master_Theorem (AFP)
11:41:04 Session AFP/LTL_Normal_Form (AFP)
11:41:04 Session AFP/Partial_Order_Reduction (AFP)
11:41:04 Session AFP/SM_Base (AFP)
11:41:04 Session AFP/SM (AFP)
11:41:04 Session AFP/CAVA_Setup (AFP)
11:41:05 Session AFP/CAVA_LTL_Modelchecker (AFP)
11:41:05 Session AFP/Transitive-Closure (AFP)
11:41:05 Session AFP/KBPs (AFP)
11:41:05 Session AFP/LTL_to_DRA (AFP)
11:41:05 Session AFP/Network_Security_Policy_Verification (AFP)
11:41:05 Session AFP/Planarity_Certificates (AFP)
11:41:06 Session AFP/Tree-Automata (AFP)
11:41:06 Session AFP/Datatype_Order_Generator (AFP)
11:41:06 Session AFP/Higher_Order_Terms (AFP)
11:41:06 Session AFP/CakeML_Codegen (AFP)
11:41:06 Session AFP/Old_Datatype_Show (AFP)
11:41:06 Session AFP/Quantifier_Elimination_Hybrid (AFP)
11:41:07 Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
11:41:07 Session AFP/FSM_Tests (AFP)
11:41:07 Session AFP/Iptables_Semantics (AFP)
11:41:07 Session AFP/Iptables_Semantics_Examples (AFP)
11:41:07 Session AFP/LOFT (AFP)
11:41:07 Session AFP/Mersenne_Primes (AFP)
11:41:08 Session AFP/MiniSail (AFP)
11:41:08 Session AFP/Separation_Logic_Imperative_HOL (AFP)
11:41:08 Session AFP/Sepref_Prereq (AFP)
11:41:08 Session AFP/ROBDD (AFP)
11:41:08 Session AFP/Refine_Imperative_HOL (AFP)
11:41:08 Session AFP/BTree (AFP)
11:41:08 Session AFP/Floyd_Warshall (AFP)
11:41:08 Session AFP/Sepref_Basic (AFP)
11:41:08 Session AFP/Sepref_IICF (AFP)
11:41:09 Session AFP/Flow_Networks (AFP)
11:41:09 Session AFP/EdmondsKarp_Maxflow (AFP)
11:41:09 Session AFP/MFMC_Countable (AFP)
11:41:09 Session AFP/Probabilistic_While (AFP)
11:41:09 Session AFP/CryptHOL (AFP)
11:41:09 Session AFP/ABY3_Protocols (AFP)
11:41:09 Session AFP/Constructive_Cryptography (AFP)
11:41:09 Session AFP/Game_Based_Crypto (AFP)
11:41:09 Session AFP/CRYSTALS-Kyber_Security (AFP)
11:41:10 Session AFP/Multi_Party_Computation (AFP)
11:41:10 Session AFP/Sigma_Commit_Crypto (AFP)
11:41:10 Session AFP/Constructive_Cryptography_CM (AFP)
11:41:10 Session AFP/Executable_Randomized_Algorithms (AFP)
11:41:11 Session AFP/Finite_Fields (AFP)
11:41:12 Session AFP/Universal_Hash_Families (AFP)
11:41:13 Session AFP/Expander_Graphs (AFP)
11:41:13 Session AFP/Karatsuba (AFP)
11:41:14 Session AFP/Median_Method (AFP)
11:41:14 Session AFP/Frequency_Moments (AFP)
11:41:15 Session AFP/Approximate_Model_Counting (AFP)
11:41:15 Session AFP/Distributed_Distinct_Elements (AFP)
11:41:15 Session AFP/Derandomization_Conditional_Expectations (AFP)
11:41:16 Session AFP/Prpu_Maxflow (AFP)
11:41:16 Session AFP/Knuth_Morris_Pratt (AFP)
11:41:16 Session AFP/Kruskal (AFP)
11:41:16 Session AFP/PAC_Checker (AFP)
11:41:16 Session AFP/VerifyThis2018 (AFP)
11:41:16 Session AFP/VerifyThis2019 (AFP)
11:41:16 Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
11:41:16 Session AFP/UpDown_Scheme (AFP)
11:41:16 Session AFP/WebAssembly (AFP)
11:41:16 Session AFP/SPARCv8 (AFP)
11:41:17 Session AFP/Schoenhage_Strassen (AFP)
11:41:17 Session AFP/X86_Semantics (AFP)
11:41:18 Session AFP/ZFC_in_HOL (AFP)
11:41:18 Session AFP/CZH_Foundations (AFP)
11:41:18 Session AFP/CZH_Elementary_Categories (AFP)
11:41:18 Session AFP/CZH_Universal_Constructions (AFP)
11:41:18 Session AFP/Category3 (AFP)
11:41:19 Session AFP/MonoidalCategory (AFP)
11:41:19 Session AFP/Ordinal_Partitions (AFP)
11:41:19 Session AFP/Q0_Metatheory (AFP)
11:41:19 Session AFP/Q0_Soundness (AFP)
11:41:19 Session AFP/Wetzels_Problem (AFP)
11:41:19 Session FOL/ZF (main timing)
11:41:19 Session Doc/Logics_ZF (doc)
11:41:19 Session AFP/Recursion-Addition (AFP)
11:41:19 Session FOL/ZF-AC
11:41:19 Session FOL/ZF-Coind
11:41:19 Session FOL/ZF-Constructible
11:41:20 Session AFP/Delta_System_Lemma (AFP)
11:41:20 Session AFP/Transitive_Models (AFP)
11:41:20 Session AFP/Independence_CH (AFP)
11:41:20 Session AFP/Forcing (AFP)
11:41:20 Session FOL/ZF-IMP
11:41:20 Session FOL/ZF-Induct
11:41:20 Session FOL/ZF-UNITY (timing)
11:41:20 Session FOL/ZF-Resid
11:41:20 Session FOL/ZF-ex
11:42:36 Running HOL-Datatype_Examples (on hpcisabelle/7) ...
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Datatype_Simproc_Tests
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TLList
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Cyclic_List
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.FAE_Sequence
11:42:39 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Free_Idempotent_Monoid
11:42:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Regex_ACI
11:42:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Regex_ACIDZ
11:42:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig
11:42:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process
11:42:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor
11:42:42 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term
11:42:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype
11:42:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype
11:42:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim
11:42:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree
11:42:44 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI
11:42:44 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang
11:42:44 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition
11:43:55 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec
11:44:10 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec
11:44:19 Timing HOL-Datatype_Examples (8 threads, 97.010s elapsed time, 493.065s cpu time, 40.311s GC time, factor 5.08)
11:44:19 Finished HOL-Datatype_Examples (0:01:42 elapsed time, 0:08:32 cpu time, factor 5.02)
11:44:19 Building HOL-Eisbach (on hpcisabelle/0) ...
11:44:21 HOL-Eisbach: theory IFOL
11:44:21 HOL-Eisbach: theory HOL-Eisbach.Eisbach
11:44:21 HOL-Eisbach: theory HOL-Analysis.Metric_Arith
11:44:22 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax
11:44:22 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools
11:44:22 HOL-Eisbach: theory HOL-Eisbach.Tests
11:44:22 HOL-Eisbach: theory HOL-Eisbach.Examples
11:44:22 HOL-Eisbach: theory HOL-Eisbach.Example_Metric
11:44:23 HOL-Eisbach: theory FOL
11:44:25 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL
11:44:32 Timing HOL-Eisbach (8 threads, 5.020s elapsed time, 21.756s cpu time, 0.388s GC time, factor 4.33)
11:44:32 Finished HOL-Eisbach (0:00:12 elapsed time, 0:00:34 cpu time, factor 2.85)
11:44:32 Running Store_Buffer_Reduction (on hpcisabelle/1) ...
11:44:33 Store_Buffer_Reduction: theory Store_Buffer_Reduction.SyntaxTweaks
11:44:33 Store_Buffer_Reduction: theory Store_Buffer_Reduction.ReduceStoreBuffer
11:44:52 Store_Buffer_Reduction: theory Store_Buffer_Reduction.ReduceStoreBufferSimulation
11:44:56 Store_Buffer_Reduction: theory Store_Buffer_Reduction.PIMP
11:45:00 Store_Buffer_Reduction: theory Store_Buffer_Reduction.Abbrevs
11:45:01 Store_Buffer_Reduction: theory Store_Buffer_Reduction.Preliminaries
11:45:01 Store_Buffer_Reduction: theory Store_Buffer_Reduction.Variants
11:45:02 Store_Buffer_Reduction: theory Store_Buffer_Reduction.Text
11:45:57 Preparing Store_Buffer_Reduction/document ...
11:48:01 Finished Store_Buffer_Reduction/document (0:02:04 elapsed time)
11:48:01 Preparing Store_Buffer_Reduction/outline ...
11:48:34 Finished Store_Buffer_Reduction/outline (0:00:32 elapsed time)
11:48:34 Timing Store_Buffer_Reduction (8 threads, 78.601s elapsed time, 506.566s cpu time, 10.251s GC time, factor 6.44)
11:48:34 Finished Store_Buffer_Reduction (0:01:20 elapsed time, 0:08:31 cpu time, factor 6.34)
11:48:34 Running Multi_Party_Computation (on hpcisabelle/2) ...
11:48:38 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
11:48:38 Multi_Party_Computation: theory HOL-Number_Theory.Cong
11:48:38 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
11:48:38 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
11:48:38 Multi_Party_Computation: theory Multi_Party_Computation.ETP
11:48:38 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
11:48:38 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
11:48:39 Multi_Party_Computation: theory HOL-Algebra.Ring
11:48:39 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
11:48:40 Multi_Party_Computation: theory HOL-Number_Theory.Totient
11:48:40 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
11:48:40 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
11:48:40 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
11:48:41 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
11:48:43 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
11:48:43 Multi_Party_Computation: theory Multi_Party_Computation.OT14
11:48:43 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
11:48:44 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
11:48:44 Multi_Party_Computation: theory HOL-Algebra.Module
11:48:45 Multi_Party_Computation: theory Multi_Party_Computation.GMW
11:48:48 Multi_Party_Computation: theory HOL-Algebra.Ideal
11:48:51 Multi_Party_Computation: theory HOL-Algebra.RingHom
11:48:53 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
11:49:09 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
11:49:13 Multi_Party_Computation: theory HOL-Number_Theory.Residues
11:49:16 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
11:49:17 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
11:49:17 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
11:50:03 Preparing Multi_Party_Computation/document ...
11:50:14 Finished Multi_Party_Computation/document (0:00:10 elapsed time)
11:50:14 Preparing Multi_Party_Computation/outline ...
11:50:19 Finished Multi_Party_Computation/outline (0:00:05 elapsed time)
11:50:19 Timing Multi_Party_Computation (8 threads, 83.215s elapsed time, 581.374s cpu time, 12.297s GC time, factor 6.99)
11:50:19 Finished Multi_Party_Computation (0:01:27 elapsed time, 0:09:49 cpu time, factor 6.73)
11:50:19 Running Collections_Examples (on hpcisabelle/3) ...
11:50:22 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples_Chapter
11:50:22 Collections_Examples: theory Collections_Examples.Examples_Chapter
11:50:22 Collections_Examples: theory Collections_Examples.ICF_Examples_Chapter
11:50:22 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples_Chapter
11:50:22 Collections_Examples: theory Containers.Extend_Partial_Order
11:50:22 Collections_Examples: theory Deriving.Comparator
11:50:22 Collections_Examples: theory Containers.List_Fusion
11:50:22 Collections_Examples: theory Containers.Equal
11:50:22 Collections_Examples: theory Deriving.Derive_Manager
11:50:22 Collections_Examples: theory Deriving.Generator_Aux
11:50:22 Collections_Examples: theory Containers.Containers_Auxiliary
11:50:22 Collections_Examples: theory HOL-Library.DAList
11:50:22 Collections_Examples: theory Containers.Closure_Set
11:50:22 Collections_Examples: theory HOL-Library.Char_ord
11:50:22 Collections_Examples: theory HOL-Library.Omega_Words_Fun
11:50:22 Collections_Examples: theory HOL-Library.Mapping
11:50:22 Collections_Examples: theory HOL-Library.Uprod
11:50:23 Collections_Examples: theory Deriving.Equality_Generator
11:50:23 Collections_Examples: theory CAVA_Automata.Digraph_Basic
11:50:23 Collections_Examples: theory Containers.Containers_Generator
11:50:23 Collections_Examples: theory Deriving.Equality_Instances
11:50:23 Collections_Examples: theory Collections_Examples.Bfs_Impl
11:50:23 Collections_Examples: theory Collections_Examples.Foreach_Refine
11:50:24 Collections_Examples: theory Containers.Collection_Enum
11:50:24 Collections_Examples: theory Containers.AssocList
11:50:24 Collections_Examples: theory Deriving.Compare
11:50:24 Collections_Examples: theory Deriving.Comparator_Generator
11:50:24 Collections_Examples: theory Containers.Lexicographic_Order
11:50:24 Collections_Examples: theory Containers.Collection_Eq
11:50:25 Collections_Examples: theory Containers.RBT_ext
11:50:25 Collections_Examples: theory Containers.Set_Linorder
11:50:25 Collections_Examples: theory Deriving.RBT_Comparator_Impl
11:50:25 Collections_Examples: theory Collections_Examples.ICF_Only_Test
11:50:25 Collections_Examples: theory Deriving.Compare_Generator
11:50:25 Collections_Examples: theory Containers.DList_Set
11:50:26 Collections_Examples: theory Deriving.Compare_Instances
11:50:26 Collections_Examples: theory Collections_Examples.Refine_Fold
11:50:26 Collections_Examples: theory Collections_Examples.Exploration
11:50:26 Collections_Examples: theory Containers.TwoSat_Ex
11:50:27 Collections_Examples: theory Collections_Examples.Exploration_DFS
11:50:27 Collections_Examples: theory Collections_Examples.PerformanceTest
11:50:28 Collections_Examples: theory Collections_Examples.itp_2010
11:50:30 Collections_Examples: theory Collections_Examples.Simple_DFS
11:50:30 Collections_Examples: theory Collections_Examples.Succ_Graph
11:50:34 Collections_Examples: theory Collections_Examples.ICF_Test
11:50:39 Collections_Examples: theory Containers.Collection_Order
11:50:40 Collections_Examples: theory Collections_Examples.ICF_Examples
11:50:40 Collections_Examples: theory Collections_Examples.Coll_Test
11:50:41 Collections_Examples: theory Collections_Examples.Nested_DFS
11:50:42 Collections_Examples: theory Containers.RBT_Mapping2
11:50:44 Collections_Examples: theory Containers.RBT_Set2
11:50:46 Collections_Examples: theory Containers.Set_Impl
11:50:52 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples
11:51:08 Collections_Examples: theory Containers.Mapping_Impl
11:51:15 Collections_Examples: theory Collections_Examples.Combined_TwoSat
11:51:43 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples
11:51:50 Collections_Examples: theory Collections_Examples.Collection_Examples
11:51:54 Preparing Collections_Examples/document ...
11:52:00 Finished Collections_Examples/document (0:00:05 elapsed time)
11:52:00 Preparing Collections_Examples/outline ...
11:52:04 Finished Collections_Examples/outline (0:00:04 elapsed time)
11:52:04 Timing Collections_Examples (8 threads, 89.520s elapsed time, 472.649s cpu time, 24.041s GC time, factor 5.28)
11:52:04 Finished Collections_Examples (0:01:33 elapsed time, 0:08:00 cpu time, factor 5.16)
11:52:05 Running Relational_Method (on hpcisabelle/4) ...
11:52:06 Relational_Method: theory Relational_Method.Definitions
11:52:11 Relational_Method: theory Relational_Method.Authentication
11:52:12 Relational_Method: theory Relational_Method.Anonymity
11:52:13 Relational_Method: theory Relational_Method.Possibility
11:53:41 Preparing Relational_Method/document ...
11:53:48 Finished Relational_Method/document (0:00:06 elapsed time)
11:53:48 Preparing Relational_Method/outline ...
11:53:53 Finished Relational_Method/outline (0:00:04 elapsed time)
11:53:53 Timing Relational_Method (8 threads, 93.916s elapsed time, 423.862s cpu time, 12.229s GC time, factor 4.51)
11:53:53 Finished Relational_Method (0:01:35 elapsed time, 0:07:06 cpu time, factor 4.45)
11:53:53 Running Schwartz_Zippel (on hpcisabelle/5) ...
11:53:56 Schwartz_Zippel: theory HOL-Computational_Algebra.Group_Closure
11:53:56 Schwartz_Zippel: theory HOL-Computational_Algebra.Fraction_Field
11:53:56 Schwartz_Zippel: theory HOL-Computational_Algebra.Nth_Powers
11:53:56 Schwartz_Zippel: theory HOL-Computational_Algebra.Squarefree
11:53:56 Schwartz_Zippel: theory HOL-Algebra.Congruence
11:53:56 Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Misc
11:53:56 Schwartz_Zippel: theory HOL-Library.Fun_Lexorder
11:53:56 Schwartz_Zippel: theory HOL-Library.Function_Algebras
11:53:56 Schwartz_Zippel: theory HOL-Library.Groups_Big_Fun
11:53:56 Schwartz_Zippel: theory Abstract-Rewriting.Seq
11:53:56 Schwartz_Zippel: theory HOL-Library.More_List
11:53:56 Schwartz_Zippel: theory HOL-Library.While_Combinator
11:53:57 Schwartz_Zippel: theory HOL-Library.Ramsey
11:53:57 Schwartz_Zippel: theory Polynomials.More_Modules
11:53:57 Schwartz_Zippel: theory HOL-Library.Poly_Mapping
11:53:58 Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Unsorted
11:53:58 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial
11:53:58 Schwartz_Zippel: theory Jordan_Normal_Form.Conjugate
11:53:58 Schwartz_Zippel: theory Open_Induction.Restricted_Predicates
11:53:58 Schwartz_Zippel: theory HOL-Algebra.Order
11:53:59 Schwartz_Zippel: theory HOL-Computational_Algebra.Normalized_Fraction
11:53:59 Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom
11:53:59 Schwartz_Zippel: theory Regular-Sets.Regular_Set
11:54:00 Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
11:54:00 Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
11:54:00 Schwartz_Zippel: theory HOL-Algebra.Lattice
11:54:00 Schwartz_Zippel: theory Polynomials.MPoly_Type
11:54:00 Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
11:54:01 Schwartz_Zippel: theory Polynomials.More_MPoly_Type
11:54:02 Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice
11:54:03 Schwartz_Zippel: theory HOL-Algebra.Group
11:54:05 Schwartz_Zippel: theory HOL-Algebra.FiniteProduct
11:54:05 Schwartz_Zippel: theory Regular-Sets.Regular_Exp
11:54:05 Schwartz_Zippel: theory HOL-Algebra.Ring
11:54:08 Schwartz_Zippel: theory Regular-Sets.NDerivative
11:54:08 Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
11:54:09 Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:54:09 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS
11:54:09 Schwartz_Zippel: theory HOL-Algebra.Module
11:54:10 Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring
11:54:10 Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate
11:54:10 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial
11:54:10 Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series
11:54:12 Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial
11:54:13 Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial
11:54:13 Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
11:54:13 Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
11:54:13 Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
11:54:14 Schwartz_Zippel: theory Regular-Sets.Regexp_Method
11:54:14 Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra
11:54:15 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
11:54:16 Schwartz_Zippel: theory Symmetric_Polynomials.Vieta
11:54:16 Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
11:54:17 Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials
11:54:17 Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
11:54:17 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
11:54:18 Schwartz_Zippel: theory Polynomials.Utils
11:54:18 Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
11:54:19 Schwartz_Zippel: theory Polynomials.Power_Products
11:54:20 Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
11:54:21 Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
11:54:22 Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
11:54:24 Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
11:54:25 Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
11:54:37 Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
11:54:41 Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
11:54:44 Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
11:54:47 Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
11:55:30 Preparing Schwartz_Zippel/document ...
11:55:33 Finished Schwartz_Zippel/document (0:00:03 elapsed time)
11:55:33 Preparing Schwartz_Zippel/outline ...
11:55:36 Finished Schwartz_Zippel/outline (0:00:02 elapsed time)
11:55:36 Timing Schwartz_Zippel (8 threads, 89.322s elapsed time, 642.120s cpu time, 17.576s GC time, factor 7.19)
11:55:36 Finished Schwartz_Zippel (0:01:33 elapsed time, 0:10:52 cpu time, factor 6.97)
11:55:36 Running Roth_Arithmetic_Progressions (on hpcisabelle/6) ...
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Abstract_Nat
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Dense_Linear_Order
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Int
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Ramsey
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Lattice_Algebras
11:55:39 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic_Misc
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Log_Nat
11:55:39 Roth_Arithmetic_Progressions: theory Ergodic_Theory.SG_Library_Complement
11:55:39 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Nat
11:55:39 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Ugraphs
11:55:39 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
11:55:40 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral
11:55:40 Roth_Arithmetic_Progressions: theory Szemeredi_Regularity.Szemeredi
11:55:41 Roth_Arithmetic_Progressions: theory Ergodic_Theory.Asymptotic_Density
11:55:47 Roth_Arithmetic_Progressions: theory HOL-Library.Interval
11:55:47 Roth_Arithmetic_Progressions: theory HOL-Library.Float
11:55:49 Roth_Arithmetic_Progressions: theory HOL-Library.Code_Target_Numeral_Float
11:55:50 Roth_Arithmetic_Progressions: theory HOL-Library.Interval_Float
11:55:51 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation_Bounds
11:55:57 Roth_Arithmetic_Progressions: theory HOL-Decision_Procs.Approximation
11:56:43 Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
11:56:46 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
11:56:48 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
11:56:49 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
11:56:49 Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
11:56:49 Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
11:57:16 Preparing Roth_Arithmetic_Progressions/document ...
11:57:19 Finished Roth_Arithmetic_Progressions/document (0:00:02 elapsed time)
11:57:19 Preparing Roth_Arithmetic_Progressions/outline ...
11:57:20 Finished Roth_Arithmetic_Progressions/outline (0:00:01 elapsed time)
11:57:20 Timing Roth_Arithmetic_Progressions (8 threads, 94.224s elapsed time, 457.881s cpu time, 6.724s GC time, factor 4.86)
11:57:20 Finished Roth_Arithmetic_Progressions (0:01:37 elapsed time, 0:07:43 cpu time, factor 4.74)
11:57:21 Building Matrix_Tensor (on hpcisabelle/7) ...
11:57:23 Matrix_Tensor: theory Matrix_Tensor.Matrix_Tensor
11:58:01 Preparing Matrix_Tensor/document ...
11:58:04 Finished Matrix_Tensor/document (0:00:03 elapsed time)
11:58:04 Preparing Matrix_Tensor/outline ...
11:58:06 Finished Matrix_Tensor/outline (0:00:01 elapsed time)
11:58:06 Timing Matrix_Tensor (8 threads, 26.422s elapsed time, 66.743s cpu time, 1.664s GC time, factor 2.53)
11:58:06 Finished Matrix_Tensor (0:00:38 elapsed time, 0:01:27 cpu time, factor 2.27)
11:58:07 Running InfPathElimination (on hpcisabelle/0) ...
11:58:08 InfPathElimination: theory InfPathElimination.Aexp
11:58:08 InfPathElimination: theory InfPathElimination.Graph
11:58:08 InfPathElimination: theory InfPathElimination.Bexp
11:58:08 InfPathElimination: theory InfPathElimination.Labels
11:58:08 InfPathElimination: theory InfPathElimination.Store
11:58:09 InfPathElimination: theory InfPathElimination.Conf
11:58:09 InfPathElimination: theory InfPathElimination.SubRel
11:58:09 InfPathElimination: theory InfPathElimination.SymExec
11:58:10 InfPathElimination: theory InfPathElimination.ArcExt
11:58:10 InfPathElimination: theory InfPathElimination.SubExt
11:58:10 InfPathElimination: theory InfPathElimination.LTS
11:58:11 InfPathElimination: theory InfPathElimination.RB
11:59:43 Preparing InfPathElimination/document ...
11:59:50 Finished InfPathElimination/document (0:00:07 elapsed time)
11:59:50 Preparing InfPathElimination/outline ...
11:59:55 Finished InfPathElimination/outline (0:00:04 elapsed time)
11:59:55 Timing InfPathElimination (8 threads, 93.570s elapsed time, 412.036s cpu time, 2.780s GC time, factor 4.40)
11:59:55 Finished InfPathElimination (0:01:35 elapsed time, 0:06:56 cpu time, factor 4.35)
11:59:55 Running Signature_Groebner (on hpcisabelle/1) ...
11:59:58 Signature_Groebner: theory Signature_Groebner.Prelims
11:59:59 Signature_Groebner: theory Signature_Groebner.More_MPoly
12:00:02 Signature_Groebner: theory Signature_Groebner.Signature_Groebner
12:00:33 Signature_Groebner: theory Signature_Groebner.Signature_Examples
12:01:29 Preparing Signature_Groebner/document ...
12:01:44 Finished Signature_Groebner/document (0:00:15 elapsed time)
12:01:44 Preparing Signature_Groebner/outline ...
12:01:50 Finished Signature_Groebner/outline (0:00:05 elapsed time)
12:01:50 Timing Signature_Groebner (8 threads, 88.084s elapsed time, 187.696s cpu time, 20.514s GC time, factor 2.13)
12:01:50 Finished Signature_Groebner (0:01:32 elapsed time, 0:03:16 cpu time, factor 2.13)
12:01:50 Running Lambda_Free_KBOs (on hpcisabelle/2) ...
12:01:54 Lambda_Free_KBOs: theory Abstract-Rewriting.Seq
12:01:54 Lambda_Free_KBOs: theory HOL-Cardinals.Order_Union
12:01:54 Lambda_Free_KBOs: theory HOL-Library.While_Combinator
12:01:54 Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Util
12:01:54 Lambda_Free_KBOs: theory Matrix.Utility
12:01:54 Lambda_Free_KBOs: theory Regular-Sets.Regular_Set
12:01:55 Lambda_Free_KBOs: theory HOL-Cardinals.Wellorder_Extension
12:01:55 Lambda_Free_KBOs: theory Lambda_Free_RPOs.Infinite_Chain
12:01:55 Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Term
12:01:55 Lambda_Free_KBOs: theory Lambda_Free_RPOs.Extension_Orders
12:01:58 Lambda_Free_KBOs: theory Regular-Sets.Regular_Exp
12:01:59 Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Encoding
12:02:02 Lambda_Free_KBOs: theory Regular-Sets.NDerivative
12:02:02 Lambda_Free_KBOs: theory Regular-Sets.Relation_Interpretation
12:02:06 Lambda_Free_KBOs: theory Regular-Sets.Equivalence_Checking
12:02:06 Lambda_Free_KBOs: theory Regular-Sets.Regexp_Method
12:02:07 Lambda_Free_KBOs: theory Abstract-Rewriting.Abstract_Rewriting
12:02:09 Lambda_Free_KBOs: theory Abstract-Rewriting.SN_Orders
12:02:12 Lambda_Free_KBOs: theory Polynomials.Polynomials
12:02:19 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util
12:02:20 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App
12:02:20 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std
12:02:21 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic
12:02:22 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Encoding_KBO
12:02:22 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs
12:02:26 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs
12:03:09 Preparing Lambda_Free_KBOs/document ...
12:03:13 Finished Lambda_Free_KBOs/document (0:00:03 elapsed time)
12:03:13 Preparing Lambda_Free_KBOs/outline ...
12:03:15 Finished Lambda_Free_KBOs/outline (0:00:02 elapsed time)
12:03:15 Timing Lambda_Free_KBOs (8 threads, 75.297s elapsed time, 237.881s cpu time, 5.763s GC time, factor 3.16)
12:03:15 Finished Lambda_Free_KBOs (0:01:17 elapsed time, 0:04:03 cpu time, factor 3.13)
12:03:16 Building Suppes_Theorem (on hpcisabelle/3) ...
12:03:17 Suppes_Theorem: theory HOL-Library.Cancellation
12:03:17 Suppes_Theorem: theory HOL-Combinatorics.Transposition
12:03:17 Suppes_Theorem: theory HOL-Library.FuncSet
12:03:17 Suppes_Theorem: theory HOL-Library.Nat_Bijection
12:03:17 Suppes_Theorem: theory Propositional_Logic_Class.Implication_Logic
12:03:17 Suppes_Theorem: theory HOL-Library.Old_Datatype
12:03:18 Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic
12:03:18 Suppes_Theorem: theory HOL-Library.Disjoint_Sets
12:03:18 Suppes_Theorem: theory HOL-Library.Countable
12:03:18 Suppes_Theorem: theory HOL-Library.Multiset
12:03:18 Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic_Completeness
12:03:25 Suppes_Theorem: theory HOL-Combinatorics.Permutations
12:03:26 Suppes_Theorem: theory HOL-Combinatorics.List_Permutation
12:03:27 Suppes_Theorem: theory Propositional_Logic_Class.List_Utilities
12:03:27 Suppes_Theorem: theory Propositional_Logic_Class.Classical_Connectives
12:03:29 Suppes_Theorem: theory Suppes_Theorem.Probability_Logic
12:03:31 Suppes_Theorem: theory Suppes_Theorem.Suppes_Theorem
12:03:49 Preparing Suppes_Theorem/document ...
12:03:53 Finished Suppes_Theorem/document (0:00:04 elapsed time)
12:03:53 Preparing Suppes_Theorem/outline ...
12:03:56 Finished Suppes_Theorem/outline (0:00:03 elapsed time)
12:03:56 Timing Suppes_Theorem (8 threads, 22.138s elapsed time, 131.146s cpu time, 3.483s GC time, factor 5.92)
12:03:56 Finished Suppes_Theorem (0:00:32 elapsed time, 0:02:31 cpu time, factor 4.71)
12:03:57 Running Probabilistic_Noninterference (on hpcisabelle/4) ...
12:03:59 Probabilistic_Noninterference: theory HOL-Library.Prefix_Order
12:03:59 Probabilistic_Noninterference: theory HOL-Library.Case_Converter
12:03:59 Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat
12:04:00 Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv
12:04:01 Probabilistic_Noninterference: theory Coinductive.Coinductive_List
12:04:09 Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
12:04:10 Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
12:04:14 Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
12:04:16 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
12:04:19 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
12:04:25 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
12:04:35 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
12:04:35 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
12:04:46 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
12:04:50 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
12:05:11 Preparing Probabilistic_Noninterference/document ...
12:05:20 Finished Probabilistic_Noninterference/document (0:00:08 elapsed time)
12:05:20 Preparing Probabilistic_Noninterference/outline ...
12:05:25 Finished Probabilistic_Noninterference/outline (0:00:04 elapsed time)
12:05:25 Timing Probabilistic_Noninterference (8 threads, 69.607s elapsed time, 415.475s cpu time, 8.308s GC time, factor 5.97)
12:05:25 Finished Probabilistic_Noninterference (0:01:13 elapsed time, 0:07:03 cpu time, factor 5.77)
12:05:25 Running Stable_Matching (on hpcisabelle/5) ...
12:05:27 Stable_Matching: theory Stable_Matching.Basis
12:05:27 Stable_Matching: theory Stable_Matching.Sotomayor
12:05:28 Stable_Matching: theory Stable_Matching.Choice_Functions
12:05:30 Stable_Matching: theory Stable_Matching.Contracts
12:05:37 Stable_Matching: theory Stable_Matching.COP
12:05:40 Stable_Matching: theory Stable_Matching.Bossiness
12:05:40 Stable_Matching: theory Stable_Matching.Strategic
12:06:55 Preparing Stable_Matching/document ...
12:07:04 Finished Stable_Matching/document (0:00:08 elapsed time)
12:07:04 Preparing Stable_Matching/outline ...
12:07:10 Finished Stable_Matching/outline (0:00:06 elapsed time)
12:07:11 Timing Stable_Matching (8 threads, 86.467s elapsed time, 467.385s cpu time, 5.821s GC time, factor 5.41)
12:07:11 Finished Stable_Matching (0:01:29 elapsed time, 0:07:52 cpu time, factor 5.29)
12:07:11 Running Taylor_Models (on hpcisabelle/6) ...
12:07:14 Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
12:07:14 Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
12:07:29 Taylor_Models: theory Taylor_Models.Polynomial_Expression
12:07:54 Taylor_Models: theory HOL-Library.Function_Algebras
12:07:54 Taylor_Models: theory Taylor_Models.Horner_Eval
12:07:54 Taylor_Models: theory Taylor_Models.Float_Topology
12:07:54 Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
12:07:55 Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
12:07:58 Taylor_Models: theory Taylor_Models.Taylor_Models
12:08:25 Taylor_Models: theory Taylor_Models.Experiments
12:08:41 Preparing Taylor_Models/document ...
12:08:44 Finished Taylor_Models/document (0:00:03 elapsed time)
12:08:44 Preparing Taylor_Models/outline ...
12:08:46 Finished Taylor_Models/outline (0:00:02 elapsed time)
12:08:46 Timing Taylor_Models (8 threads, 85.330s elapsed time, 299.983s cpu time, 6.500s GC time, factor 3.52)
12:08:46 Finished Taylor_Models (0:01:29 elapsed time, 0:05:06 cpu time, factor 3.44)
12:08:46 Running Twelvefold_Way (on hpcisabelle/7) ...
12:08:48 Twelvefold_Way: theory Card_Number_Partitions.Additions_to_Main
12:08:48 Twelvefold_Way: theory Card_Multisets.Card_Multisets
12:08:48 Twelvefold_Way: theory HOL-Combinatorics.Transposition
12:08:48 Twelvefold_Way: theory HOL-Combinatorics.Stirling
12:08:48 Twelvefold_Way: theory HOL-Eisbach.Eisbach
12:08:48 Twelvefold_Way: theory Card_Partitions.Set_Partition
12:08:48 Twelvefold_Way: theory HOL-ex.Birthday_Paradox
12:08:49 Twelvefold_Way: theory Card_Number_Partitions.Number_Partition
12:08:49 Twelvefold_Way: theory HOL-Combinatorics.Permutations
12:08:49 Twelvefold_Way: theory Card_Number_Partitions.Card_Number_Partitions
12:08:50 Twelvefold_Way: theory Card_Partitions.Injectivity_Solver
12:08:51 Twelvefold_Way: theory Card_Partitions.Card_Partitions
12:08:51 Twelvefold_Way: theory Bell_Numbers_Spivey.Bell_Numbers
12:08:51 Twelvefold_Way: theory Twelvefold_Way.Preliminaries
12:08:52 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Core
12:08:52 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry1
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry2
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Equiv_Relations_on_Functions
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Card_Bijections_Direct
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry10
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry4
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry5
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry7
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry6
12:08:53 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry11
12:08:54 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry8
12:08:54 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry9
12:08:54 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry12
12:08:54 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry3
12:08:54 Twelvefold_Way: theory Twelvefold_Way.Card_Bijections
12:08:55 Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way
12:10:15 Preparing Twelvefold_Way/document ...
12:10:22 Finished Twelvefold_Way/document (0:00:07 elapsed time)
12:10:22 Preparing Twelvefold_Way/outline ...
12:10:26 Finished Twelvefold_Way/outline (0:00:03 elapsed time)
12:10:26 Timing Twelvefold_Way (8 threads, 84.722s elapsed time, 255.467s cpu time, 3.604s GC time, factor 3.02)
12:10:26 Finished Twelvefold_Way (0:01:27 elapsed time, 0:04:20 cpu time, factor 2.98)
12:10:26 Building UPF (on hpcisabelle/0) ...
12:10:28 UPF: theory UPF.Monads
12:10:29 UPF: theory UPF.UPFCore
12:10:30 UPF: theory UPF.ElementaryPolicies
12:10:30 UPF: theory UPF.ParallelComposition
12:10:30 UPF: theory UPF.SeqComposition
12:10:32 UPF: theory UPF.Analysis
12:10:32 UPF: theory UPF.Normalisation
12:10:33 UPF: theory UPF.NormalisationTestSpecification
12:10:34 UPF: theory UPF.UPF
12:10:34 UPF: theory UPF.Service
12:10:47 UPF: theory UPF.ServiceExample
12:10:56 Preparing UPF/document ...
12:11:03 Finished UPF/document (0:00:06 elapsed time)
12:11:03 Preparing UPF/outline ...
12:11:08 Finished UPF/outline (0:00:05 elapsed time)
12:11:08 Timing UPF (8 threads, 20.555s elapsed time, 84.440s cpu time, 1.694s GC time, factor 4.11)
12:11:08 Finished UPF (0:00:29 elapsed time, 0:01:41 cpu time, factor 3.42)
12:11:08 Running LOFT (on hpcisabelle/1) ...
12:11:11 LOFT: theory LOFT.OpenFlow_Helpers
12:11:11 LOFT: theory LOFT.Sort_Descending
12:11:11 LOFT: theory LOFT.List_Group
12:11:12 LOFT: theory LOFT.Semantics_OpenFlow
12:11:12 LOFT: theory HOL-Library.List_Lexorder
12:11:12 LOFT: theory LOFT.OpenFlow_Matches
12:11:16 LOFT: theory LOFT.Featherweight_OpenFlow_Comparison
12:11:19 LOFT: theory LOFT.OpenFlow_Action
12:11:20 LOFT: theory LOFT.OpenFlow_Serialize
12:11:26 LOFT: theory LOFT.LinuxRouter_OpenFlow_Translation
12:11:28 LOFT: theory LOFT.OF_conv_test
12:11:32 LOFT: theory LOFT.OpenFlow_Documentation
12:11:33 LOFT: theory LOFT.RFC2544
12:12:39 Preparing LOFT/document ...
12:12:48 Finished LOFT/document (0:00:08 elapsed time)
12:12:48 Preparing LOFT/outline ...
12:12:56 Finished LOFT/outline (0:00:07 elapsed time)
12:12:56 Timing LOFT (8 threads, 87.800s elapsed time, 411.743s cpu time, 8.626s GC time, factor 4.69)
12:12:56 Finished LOFT (0:01:30 elapsed time, 0:06:56 cpu time, factor 4.59)
12:12:56 Running Query_Optimization (on hpcisabelle/2) ...
12:12:58 Query_Optimization: theory Query_Optimization.Misc
12:12:58 Query_Optimization: theory Query_Optimization.Graph_Theory_Batteries
12:12:59 Query_Optimization: theory Query_Optimization.Graph_Definitions
12:13:01 Query_Optimization: theory Query_Optimization.Shortest_Path_Tree
12:13:03 Query_Optimization: theory Query_Optimization.Selectivities
12:13:03 Query_Optimization: theory Query_Optimization.Graph_Additions
12:13:04 Query_Optimization: theory Query_Optimization.Directed_Tree_Additions
12:13:05 Query_Optimization: theory Query_Optimization.JoinTree
12:13:09 Query_Optimization: theory Query_Optimization.CostFunctions
12:13:09 Query_Optimization: theory Query_Optimization.QueryGraph
12:13:09 Query_Optimization: theory Query_Optimization.Dtree
12:13:19 Query_Optimization: theory Query_Optimization.List_Dtree
12:13:21 Query_Optimization: theory Query_Optimization.IKKBZ
12:13:29 Query_Optimization: theory Query_Optimization.IKKBZ_Optimality
12:13:39 Query_Optimization: theory Query_Optimization.IKKBZ_Examples
12:14:26 Preparing Query_Optimization/document ...
12:15:04 Finished Query_Optimization/document (0:00:38 elapsed time)
12:15:04 Preparing Query_Optimization/outline ...
12:15:21 Finished Query_Optimization/outline (0:00:16 elapsed time)
12:15:21 Timing Query_Optimization (8 threads, 84.500s elapsed time, 508.865s cpu time, 11.146s GC time, factor 6.02)
12:15:21 Finished Query_Optimization (0:01:27 elapsed time, 0:08:37 cpu time, factor 5.89)
12:15:21 Running Higher_Order_Terms (on hpcisabelle/3) ...
12:15:22 Higher_Order_Terms: theory HOL-Library.AList
12:15:22 Higher_Order_Terms: theory HOL-Library.Nat_Bijection
12:15:22 Higher_Order_Terms: theory List-Index.List_Index
12:15:22 Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading
12:15:22 Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity
12:15:22 Higher_Order_Terms: theory HOL-Library.Old_Datatype
12:15:23 Higher_Order_Terms: theory HOL-Library.Monad_Syntax
12:15:23 Higher_Order_Terms: theory HOL-Library.State_Monad
12:15:24 Higher_Order_Terms: theory HOL-Library.Countable
12:15:25 Higher_Order_Terms: theory HOL-Library.FSet
12:15:29 Higher_Order_Terms: theory HOL-Library.Finite_Map
12:15:43 Higher_Order_Terms: theory Higher_Order_Terms.Term_Utils
12:15:43 Higher_Order_Terms: theory Higher_Order_Terms.Find_First
12:15:45 Higher_Order_Terms: theory Deriving.Derive_Manager
12:15:45 Higher_Order_Terms: theory HOL-Library.Cancellation
12:15:45 Higher_Order_Terms: theory HOL-Library.FuncSet
12:15:45 Higher_Order_Terms: theory HOL-ex.Unification
12:15:45 Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Monad
12:15:45 Higher_Order_Terms: theory HOL-Library.Infinite_Set
12:15:45 Higher_Order_Terms: theory Higher_Order_Terms.Name
12:15:45 Higher_Order_Terms: theory Datatype_Order_Generator.Derive_Aux
12:15:45 Higher_Order_Terms: theory Datatype_Order_Generator.Order_Generator
12:15:46 Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Class
12:15:46 Higher_Order_Terms: theory HOL-Library.Countable_Set
12:15:46 Higher_Order_Terms: theory HOL-Library.Disjoint_Sets
12:15:46 Higher_Order_Terms: theory HOL-Library.Multiset
12:15:46 Higher_Order_Terms: theory HOL-Library.Disjoint_FSets
12:15:47 Higher_Order_Terms: theory HOL-Library.Countable_Complete_Lattices
12:15:47 Higher_Order_Terms: theory Higher_Order_Terms.Term_Class
12:15:49 Higher_Order_Terms: theory HOL-Library.Order_Continuity
12:15:50 Higher_Order_Terms: theory HOL-Library.Extended_Nat
12:15:53 Higher_Order_Terms: theory HOL-Library.Multiset_Order
12:15:53 Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Util
12:15:54 Higher_Order_Terms: theory Higher_Order_Terms.Nterm
12:15:54 Higher_Order_Terms: theory Higher_Order_Terms.Term
12:15:54 Higher_Order_Terms: theory Higher_Order_Terms.Unification_Compat
12:15:54 Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Term
12:15:55 Higher_Order_Terms: theory Higher_Order_Terms.Pats
12:15:56 Higher_Order_Terms: theory Higher_Order_Terms.Term_to_Nterm
12:15:58 Higher_Order_Terms: theory Higher_Order_Terms.Lambda_Free_Compat
12:16:20 Preparing Higher_Order_Terms/document ...
12:16:26 Finished Higher_Order_Terms/document (0:00:05 elapsed time)
12:16:26 Preparing Higher_Order_Terms/outline ...
12:16:30 Finished Higher_Order_Terms/outline (0:00:03 elapsed time)
12:16:30 Timing Higher_Order_Terms (8 threads, 55.460s elapsed time, 241.025s cpu time, 6.605s GC time, factor 4.35)
12:16:30 Finished Higher_Order_Terms (0:00:57 elapsed time, 0:04:07 cpu time, factor 4.27)
12:16:30 Running HOL-MicroJava (on hpcisabelle/4) ...
12:16:31 HOL-MicroJava: theory HOL-Eisbach.Eisbach
12:16:31 HOL-MicroJava: theory HOL-Library.Transitive_Closure_Table
12:16:31 HOL-MicroJava: theory HOL-Library.While_Combinator
12:16:32 HOL-MicroJava: theory HOL-MicroJava.Semilat
12:16:33 HOL-MicroJava: theory HOL-MicroJava.JBasis
12:16:33 HOL-MicroJava: theory HOL-MicroJava.AuxLemmas
12:16:33 HOL-MicroJava: theory HOL-MicroJava.Type
12:16:33 HOL-MicroJava: theory HOL-MicroJava.Err
12:16:34 HOL-MicroJava: theory HOL-MicroJava.Listn
12:16:34 HOL-MicroJava: theory HOL-MicroJava.Opt
12:16:34 HOL-MicroJava: theory HOL-MicroJava.Product
12:16:34 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework
12:16:34 HOL-MicroJava: theory HOL-MicroJava.Semilattices
12:16:35 HOL-MicroJava: theory HOL-MicroJava.SemilatAlg
12:16:35 HOL-MicroJava: theory HOL-MicroJava.Kildall
12:16:35 HOL-MicroJava: theory HOL-MicroJava.LBVSpec
12:16:35 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err
12:16:36 HOL-MicroJava: theory HOL-MicroJava.Decl
12:16:36 HOL-MicroJava: theory HOL-MicroJava.Value
12:16:36 HOL-MicroJava: theory HOL-MicroJava.LBVComplete
12:16:36 HOL-MicroJava: theory HOL-MicroJava.SystemClasses
12:16:36 HOL-MicroJava: theory HOL-MicroJava.TypeRel
12:16:36 HOL-MicroJava: theory HOL-MicroJava.LBVCorrect
12:16:36 HOL-MicroJava: theory HOL-MicroJava.Abstract_BV
12:16:36 HOL-MicroJava: theory HOL-MicroJava.WellForm
12:16:37 HOL-MicroJava: theory HOL-MicroJava.State
12:16:37 HOL-MicroJava: theory HOL-MicroJava.Term
12:16:37 HOL-MicroJava: theory HOL-MicroJava.Exceptions
12:16:37 HOL-MicroJava: theory HOL-MicroJava.JType
12:16:38 HOL-MicroJava: theory HOL-MicroJava.JVMType
12:16:41 HOL-MicroJava: theory HOL-MicroJava.WellType
12:16:42 HOL-MicroJava: theory HOL-MicroJava.Conform
12:16:42 HOL-MicroJava: theory HOL-MicroJava.Eval
12:16:42 HOL-MicroJava: theory HOL-MicroJava.TypeInf
12:16:42 HOL-MicroJava: theory HOL-MicroJava.JVMState
12:16:42 HOL-MicroJava: theory HOL-MicroJava.JVMInstructions
12:16:44 HOL-MicroJava: theory HOL-MicroJava.JVMExceptions
12:16:44 HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr
12:16:44 HOL-MicroJava: theory HOL-MicroJava.Effect
12:16:44 HOL-MicroJava: theory HOL-MicroJava.JVMExec
12:16:45 HOL-MicroJava: theory HOL-MicroJava.DefsComp
12:16:45 HOL-MicroJava: theory HOL-MicroJava.JVMDefensive
12:16:45 HOL-MicroJava: theory HOL-MicroJava.JVMListExample
12:16:45 HOL-MicroJava: theory HOL-MicroJava.Index
12:16:46 HOL-MicroJava: theory HOL-MicroJava.TranslCompTp
12:16:47 HOL-MicroJava: theory HOL-MicroJava.TranslComp
12:16:47 HOL-MicroJava: theory HOL-MicroJava.LemmasComp
12:16:47 HOL-MicroJava: theory HOL-MicroJava.Example
12:16:47 HOL-MicroJava: theory HOL-MicroJava.JListExample
12:16:47 HOL-MicroJava: theory HOL-MicroJava.JTypeSafe
12:16:48 HOL-MicroJava: theory HOL-MicroJava.CorrComp
12:17:06 HOL-MicroJava: theory HOL-MicroJava.BVSpec
12:17:06 HOL-MicroJava: theory HOL-MicroJava.EffectMono
12:17:06 HOL-MicroJava: theory HOL-MicroJava.Altern
12:17:06 HOL-MicroJava: theory HOL-MicroJava.Correct
12:17:06 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM
12:17:07 HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe
12:17:07 HOL-MicroJava: theory HOL-MicroJava.JVM
12:17:07 HOL-MicroJava: theory HOL-MicroJava.LBVJVM
12:17:08 HOL-MicroJava: theory HOL-MicroJava.CorrCompTp
12:17:08 HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError
12:17:08 HOL-MicroJava: theory HOL-MicroJava.BVExample
12:17:10 HOL-MicroJava: theory HOL-MicroJava.MicroJava
12:17:56 Preparing HOL-MicroJava/document ...
12:18:07 Finished HOL-MicroJava/document (0:00:10 elapsed time)
12:18:07 Preparing HOL-MicroJava/outline ...
12:18:13 Finished HOL-MicroJava/outline (0:00:06 elapsed time)
12:18:13 Timing HOL-MicroJava (8 threads, 82.390s elapsed time, 432.210s cpu time, 6.651s GC time, factor 5.25)
12:18:13 Finished HOL-MicroJava (0:01:24 elapsed time, 0:07:16 cpu time, factor 5.16)
12:18:14 Running Metalogic_ProofChecker (on hpcisabelle/5) ...
12:18:15 Metalogic_ProofChecker: theory HOL-Eisbach.Eisbach
12:18:15 Metalogic_ProofChecker: theory HOL-Library.AList
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Case_Converter
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Char_ord
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Code_Abstract_Nat
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Code_Target_Int
12:18:15 Metalogic_ProofChecker: theory List-Index.List_Index
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Sublist
12:18:15 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Core
12:18:15 Metalogic_ProofChecker: theory HOL-Library.Code_Target_Nat
12:18:16 Metalogic_ProofChecker: theory HOL-Library.Simps_Case_Conv
12:18:18 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Preliminaries
12:18:21 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Term
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.BetaNorm
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Instances
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Name
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Sorts
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Term_Subst
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.SortConstants
12:18:35 Metalogic_ProofChecker: theory Metalogic_ProofChecker.SortsExe
12:18:36 Metalogic_ProofChecker: theory Metalogic_ProofChecker.EtaNorm
12:18:36 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Theory
12:18:37 Metalogic_ProofChecker: theory Metalogic_ProofChecker.BetaNormProof
12:18:37 Metalogic_ProofChecker: theory Metalogic_ProofChecker.EtaNormProof
12:18:37 Metalogic_ProofChecker: theory Metalogic_ProofChecker.Logic
12:18:39 Metalogic_ProofChecker: theory Metalogic_ProofChecker.EqualityProof
12:18:40 Metalogic_ProofChecker: theory Metalogic_ProofChecker.TheoryExe
12:18:41 Metalogic_ProofChecker: theory Metalogic_ProofChecker.ProofTerm
12:18:47 Metalogic_ProofChecker: theory Metalogic_ProofChecker.CheckerExe
12:18:50 Metalogic_ProofChecker: theory Metalogic_ProofChecker.CodeGen
12:19:37 Preparing Metalogic_ProofChecker/document ...
12:19:56 Finished Metalogic_ProofChecker/document (0:00:18 elapsed time)
12:19:56 Preparing Metalogic_ProofChecker/outline ...
12:20:05 Finished Metalogic_ProofChecker/outline (0:00:09 elapsed time)
12:20:05 Timing Metalogic_ProofChecker (8 threads, 79.706s elapsed time, 483.756s cpu time, 6.773s GC time, factor 6.07)
12:20:05 Finished Metalogic_ProofChecker (0:01:21 elapsed time, 0:08:08 cpu time, factor 5.96)
12:20:05 Running HOL-SMT_Examples (on hpcisabelle/6) ...
12:20:07 HOL-SMT_Examples: theory HOL-Library.Phantom_Type
12:20:07 HOL-SMT_Examples: theory HOL-SMT_Examples.Boogie
12:20:07 HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Examples_Verit
12:20:07 HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Examples
12:20:07 HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Tests_Verit
12:20:08 HOL-SMT_Examples: theory HOL-Library.Cardinality
12:20:09 HOL-SMT_Examples: theory HOL-Library.Numeral_Type
12:20:10 HOL-SMT_Examples: theory HOL-Library.Type_Length
12:20:11 HOL-SMT_Examples: theory HOL-Library.Word
12:20:22 HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Word_Examples
12:21:23 HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Tests
12:21:29 Timing HOL-SMT_Examples (8 threads, 81.061s elapsed time, 227.792s cpu time, 4.045s GC time, factor 2.81)
12:21:29 Finished HOL-SMT_Examples (0:01:23 elapsed time, 0:03:52 cpu time, factor 2.79)
12:21:29 Running Interval_Analysis (on hpcisabelle/7) ...
12:21:34 Interval_Analysis: theory HOL-Library.Lattice_Algebras
12:21:34 Interval_Analysis: theory Interval_Analysis.Affine_Functions
12:21:34 Interval_Analysis: theory HOL-Library.Log_Nat
12:21:40 Interval_Analysis: theory HOL-Library.Interval
12:21:40 Interval_Analysis: theory HOL-Library.Float
12:21:43 Interval_Analysis: theory HOL-Library.Interval_Float
12:21:45 Interval_Analysis: theory Interval_Analysis.Interval_Utilities
12:21:46 Interval_Analysis: theory Interval_Analysis.Interval_Division_Non_Zero
12:21:46 Interval_Analysis: theory Interval_Analysis.Extended_Interval_Division
12:21:46 Interval_Analysis: theory Interval_Analysis.Interval_Division_Real
12:21:47 Interval_Analysis: theory Interval_Analysis.Inclusion_Isotonicity
12:21:49 Interval_Analysis: theory Interval_Analysis.Lipschitz_Interval_Extension
12:21:50 Interval_Analysis: theory Interval_Analysis.Multi_Interval_Preliminaries
12:21:52 Interval_Analysis: theory Interval_Analysis.Lipschitz_Subdivisions_Refinements
12:21:52 Interval_Analysis: theory Interval_Analysis.Multi_Interval_Adjacent
12:21:54 Interval_Analysis: theory Interval_Analysis.Extended_Interval_Analysis
12:21:54 Interval_Analysis: theory Interval_Analysis.Interval_Analysis
12:21:54 Interval_Analysis: theory Interval_Analysis.Multi_Interval_Non_Overlapping
12:21:54 Interval_Analysis: theory Interval_Analysis.Multi_Interval_Overlapping
12:21:56 Interval_Analysis: theory Interval_Analysis.Multi_Interval
12:21:58 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Division_Core
12:21:58 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Division_Adjacent
12:21:58 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Division_Non_Overlapping
12:21:58 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Division_Overlapping
12:21:58 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Division
12:21:59 Interval_Analysis: theory Interval_Analysis.Extended_Multi_Interval_Analysis
12:22:56 Preparing Interval_Analysis/document ...
12:23:35 Finished Interval_Analysis/document (0:00:39 elapsed time)
12:23:35 Preparing Interval_Analysis/outline ...
12:24:01 Finished Interval_Analysis/outline (0:00:25 elapsed time)
12:24:01 Timing Interval_Analysis (8 threads, 82.318s elapsed time, 469.689s cpu time, 6.645s GC time, factor 5.71)
12:24:01 Finished Interval_Analysis (0:01:25 elapsed time, 0:07:56 cpu time, factor 5.56)
12:24:01 Building Pi_Transcendental (on hpcisabelle/0) ...
12:24:04 Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
12:24:04 Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
12:24:04 Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
12:24:04 Pi_Transcendental: theory HOL-Library.Fun_Lexorder
12:24:04 Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
12:24:04 Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
12:24:05 Pi_Transcendental: theory HOL-Library.Poly_Mapping
12:24:05 Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
12:24:07 Pi_Transcendental: theory Polynomials.MPoly_Type
12:24:07 Pi_Transcendental: theory Symmetric_Polynomials.Vieta
12:24:08 Pi_Transcendental: theory Polynomials.More_MPoly_Type
12:24:08 Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
12:24:12 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
12:24:37 Preparing Pi_Transcendental/document ...
12:24:41 Finished Pi_Transcendental/document (0:00:03 elapsed time)
12:24:41 Preparing Pi_Transcendental/outline ...
12:24:43 Finished Pi_Transcendental/outline (0:00:02 elapsed time)
12:24:43 Timing Pi_Transcendental (8 threads, 17.024s elapsed time, 105.810s cpu time, 1.943s GC time, factor 6.22)
12:24:43 Finished Pi_Transcendental (0:00:35 elapsed time, 0:02:19 cpu time, factor 3.93)
12:24:43 Running Eval_FO (on hpcisabelle/1) ...
12:24:45 Eval_FO: theory Eval_FO.FO
12:24:45 Eval_FO: theory Eval_FO.Mapping_Code
12:24:46 Eval_FO: theory Eval_FO.Cluster
12:24:51 Eval_FO: theory Eval_FO.Eval_FO
12:24:54 Eval_FO: theory Eval_FO.Ailamazyan
12:25:09 Eval_FO: theory Eval_FO.Ailamazyan_Code
12:26:11 Preparing Eval_FO/document ...
12:26:20 Finished Eval_FO/document (0:00:08 elapsed time)
12:26:20 Preparing Eval_FO/outline ...
12:26:24 Finished Eval_FO/outline (0:00:04 elapsed time)
12:26:24 Timing Eval_FO (8 threads, 83.783s elapsed time, 402.636s cpu time, 6.555s GC time, factor 4.81)
12:26:24 Finished Eval_FO (0:01:27 elapsed time, 0:06:48 cpu time, factor 4.69)
12:26:24 Running Flyspeck-Tame (on hpcisabelle/2) ...
12:26:26 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
12:26:26 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
12:26:26 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
12:26:26 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
12:26:26 Flyspeck-Tame: theory HOL-Library.AList
12:26:26 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
12:26:26 Flyspeck-Tame: theory HOL-Library.IArray
12:26:26 Flyspeck-Tame: theory HOL-Library.While_Combinator
12:26:26 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
12:26:26 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
12:26:27 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
12:26:27 Flyspeck-Tame: theory Flyspeck-Tame.Arch
12:26:27 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
12:26:27 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
12:26:27 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
12:26:27 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
12:26:28 Flyspeck-Tame: theory Flyspeck-Tame.Graph
12:26:28 Flyspeck-Tame: theory Flyspeck-Tame.Maps
12:26:28 Flyspeck-Tame: theory Trie.Trie
12:26:29 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
12:26:30 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
12:26:30 Flyspeck-Tame: theory Flyspeck-Tame.Tame
12:26:30 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
12:26:30 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
12:26:30 Flyspeck-Tame: theory Trie.Tries
12:26:31 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
12:26:31 Flyspeck-Tame: theory Flyspeck-Tame.Plane
12:26:33 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
12:26:33 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
12:26:33 Flyspeck-Tame: theory Flyspeck-Tame.Generator
12:26:33 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
12:26:36 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
12:26:36 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
12:26:38 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
12:26:38 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
12:26:38 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
12:26:39 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
12:26:39 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
12:26:39 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
12:26:39 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
12:26:40 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
12:27:53 Preparing Flyspeck-Tame/document ...
12:28:10 Finished Flyspeck-Tame/document (0:00:17 elapsed time)
12:28:10 Preparing Flyspeck-Tame/outline ...
12:28:18 Finished Flyspeck-Tame/outline (0:00:07 elapsed time)
12:28:18 Timing Flyspeck-Tame (8 threads, 84.466s elapsed time, 477.295s cpu time, 29.823s GC time, factor 5.65)
12:28:18 Finished Flyspeck-Tame (0:01:27 elapsed time, 0:08:05 cpu time, factor 5.55)
12:28:18 Running Orient_Rewrite_Rule_Undecidable (on hpcisabelle/3) ...
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Combinatorics.Transposition
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Fraction_Field
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Nth_Powers
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Group_Closure
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Squarefree
12:28:20 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Interpolation.Missing_Unsorted
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Formal_Power_Series
12:28:20 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
12:28:21 Orient_Rewrite_Rule_Undecidable: theory HOL-Combinatorics.Permutations
12:28:21 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Interpolation.Ring_Hom
12:28:21 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Preliminaries_on_Polynomials_1
12:28:23 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Normalized_Fraction
12:28:23 Orient_Rewrite_Rule_Undecidable: theory Jordan_Normal_Form.Missing_Misc
12:28:24 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Polynomial_Factorial
12:28:25 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Interpolation.Missing_Polynomial
12:28:27 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Factorization.Order_Polynomial
12:28:27 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Polynomial_FPS
12:28:27 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
12:28:27 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Interpolation.Ring_Hom_Poly
12:28:27 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Formal_Laurent_Series
12:28:31 Orient_Rewrite_Rule_Undecidable: theory HOL-Computational_Algebra.Computational_Algebra
12:28:32 Orient_Rewrite_Rule_Undecidable: theory Symmetric_Polynomials.Vieta
12:28:34 Orient_Rewrite_Rule_Undecidable: theory Symmetric_Polynomials.Symmetric_Polynomials
12:28:37 Orient_Rewrite_Rule_Undecidable: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
12:28:38 Orient_Rewrite_Rule_Undecidable: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
12:28:38 Orient_Rewrite_Rule_Undecidable: theory Factor_Algebraic_Polynomial.Poly_Connection
12:28:41 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Preliminaries_on_Polynomials_2
12:28:57 Orient_Rewrite_Rule_Undecidable: theory First_Order_Terms.Term
12:28:59 Orient_Rewrite_Rule_Undecidable: theory First_Order_Terms.Subterm_and_Context
12:29:03 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Polynomial_Interpretation
12:29:05 Orient_Rewrite_Rule_Undecidable: theory Polynomial_Factorization.Missing_List
12:29:05 Orient_Rewrite_Rule_Undecidable: theory Knuth_Bendix_Order.Order_Pair
12:29:05 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Hilbert10_to_Inequality
12:29:05 Orient_Rewrite_Rule_Undecidable: theory Knuth_Bendix_Order.Lexicographic_Extension
12:29:06 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Linear_Poly_Termination_Undecidable
12:29:08 Orient_Rewrite_Rule_Undecidable: theory Knuth_Bendix_Order.KBO
12:29:11 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.KBO_Subterm_Coefficients_Undecidable
12:29:11 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Poly_Termination_Undecidable
12:29:15 Orient_Rewrite_Rule_Undecidable: theory Orient_Rewrite_Rule_Undecidable.Delta_Poly_Termination_Undecidable
12:29:29 Preparing Orient_Rewrite_Rule_Undecidable/document ...
12:29:39 Finished Orient_Rewrite_Rule_Undecidable/document (0:00:10 elapsed time)
12:29:39 Preparing Orient_Rewrite_Rule_Undecidable/outline ...
12:29:44 Finished Orient_Rewrite_Rule_Undecidable/outline (0:00:04 elapsed time)
12:29:44 Timing Orient_Rewrite_Rule_Undecidable (8 threads, 64.882s elapsed time, 432.026s cpu time, 10.145s GC time, factor 6.66)
12:29:44 Finished Orient_Rewrite_Rule_Undecidable (0:01:08 elapsed time, 0:07:20 cpu time, factor 6.42)
12:29:44 Building Cauchy (on hpcisabelle/4) ...
12:29:45 Cauchy: theory Cauchy.CauchysMeanTheorem
12:29:45 Cauchy: theory Cauchy.CauchySchwarz
12:29:52 Preparing Cauchy/document ...
12:29:55 Finished Cauchy/document (0:00:02 elapsed time)
12:29:55 Preparing Cauchy/outline ...
12:29:56 Finished Cauchy/outline (0:00:01 elapsed time)
12:29:56 Timing Cauchy (8 threads, 1.936s elapsed time, 8.785s cpu time, 0.131s GC time, factor 4.54)
12:29:56 Finished Cauchy (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.28)
12:29:56 Running LTL_to_DRA (on hpcisabelle/5) ...
12:29:59 LTL_to_DRA: theory LTL_to_DRA.LTL_FGXU
12:29:59 LTL_to_DRA: theory KBPs.DFS
12:29:59 LTL_to_DRA: theory LTL_to_DRA.Map2
12:29:59 LTL_to_DRA: theory LTL_to_DRA.Preliminaries2
12:29:59 LTL_to_DRA: theory List-Index.List_Index
12:29:59 LTL_to_DRA: theory LTL_to_DRA.Mapping2
12:30:00 LTL_to_DRA: theory LTL_to_DRA.DTS
12:30:00 LTL_to_DRA: theory LTL_to_DRA.List2
12:30:02 LTL_to_DRA: theory LTL_to_DRA.Rabin
12:30:02 LTL_to_DRA: theory LTL_to_DRA.Semi_Mojmir
12:30:05 LTL_to_DRA: theory LTL_to_DRA.Mojmir
12:30:07 LTL_to_DRA: theory LTL_to_DRA.Mojmir_Rabin
12:30:07 LTL_to_DRA: theory LTL_to_DRA.LTL_Compat
12:30:07 LTL_to_DRA: theory LTL_to_DRA.LTL_Impl
12:30:07 LTL_to_DRA: theory LTL_to_DRA.af
12:30:08 LTL_to_DRA: theory LTL_to_DRA.Mojmir_Rabin_Impl
12:30:09 LTL_to_DRA: theory LTL_to_DRA.Logical_Characterization
12:30:10 LTL_to_DRA: theory LTL_to_DRA.af_Impl
12:30:11 LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin
12:30:18 LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin_Unfold_Opt
12:30:30 LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin_Impl
12:30:34 LTL_to_DRA: theory LTL_to_DRA.Export_Code
12:31:22 Preparing LTL_to_DRA/document ...
12:31:35 Finished LTL_to_DRA/document (0:00:13 elapsed time)
12:31:35 Preparing LTL_to_DRA/outline ...
12:31:42 Finished LTL_to_DRA/outline (0:00:06 elapsed time)
12:31:42 Timing LTL_to_DRA (8 threads, 80.083s elapsed time, 406.464s cpu time, 34.839s GC time, factor 5.08)
12:31:42 Finished LTL_to_DRA (0:01:23 elapsed time, 0:06:56 cpu time, factor 4.96)
12:31:43 Running Fishers_Inequality (on hpcisabelle/6) ...
12:31:46 Fishers_Inequality: theory Card_Partitions.Set_Partition
12:31:46 Fishers_Inequality: theory Polynomials.MPoly_Type
12:31:46 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
12:31:46 Fishers_Inequality: theory Polynomials.More_Modules
12:31:46 Fishers_Inequality: theory List-Index.List_Index
12:31:46 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
12:31:46 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
12:31:46 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
12:31:47 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
12:31:47 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
12:31:47 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
12:31:47 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
12:31:48 Fishers_Inequality: theory Polynomials.More_MPoly_Type
12:31:48 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
12:31:48 Fishers_Inequality: theory Design_Theory.Multisets_Extras
12:31:49 Fishers_Inequality: theory Design_Theory.Design_Basics
12:31:49 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
12:31:49 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
12:31:50 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
12:31:50 Fishers_Inequality: theory Design_Theory.Design_Operations
12:31:50 Fishers_Inequality: theory Polynomials.Utils
12:31:50 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
12:31:51 Fishers_Inequality: theory Groebner_Bases.General
12:31:51 Fishers_Inequality: theory Polynomials.Power_Products
12:31:52 Fishers_Inequality: theory Design_Theory.Block_Designs
12:31:52 Fishers_Inequality: theory Design_Theory.Sub_Designs
12:31:53 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
12:31:55 Fishers_Inequality: theory Design_Theory.BIBD
12:31:57 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
12:32:09 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
12:32:13 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
12:32:31 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
12:32:34 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
12:32:37 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
12:32:39 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
12:32:40 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
12:32:46 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
12:32:46 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
12:32:49 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
12:32:51 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
12:32:51 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
12:32:53 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
12:33:01 Preparing Fishers_Inequality/document ...
12:33:13 Finished Fishers_Inequality/document (0:00:12 elapsed time)
12:33:13 Preparing Fishers_Inequality/outline ...
12:33:20 Finished Fishers_Inequality/outline (0:00:06 elapsed time)
12:33:20 Timing Fishers_Inequality (8 threads, 71.588s elapsed time, 455.241s cpu time, 13.349s GC time, factor 6.36)
12:33:20 Finished Fishers_Inequality (0:01:16 elapsed time, 0:07:43 cpu time, factor 6.10)
12:33:20 Building HOL-Cardinals (on hpcisabelle/7) ...
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Fun_More
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Order_Union
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More
12:33:22 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation
12:33:23 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding
12:33:23 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions
12:33:24 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation
12:33:24 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic
12:33:25 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic
12:33:26 HOL-Cardinals: theory HOL-Cardinals.Cardinals
12:33:26 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set
12:33:40 Preparing HOL-Cardinals/document ...
12:33:48 Finished HOL-Cardinals/document (0:00:08 elapsed time)
12:33:48 Preparing HOL-Cardinals/outline ...
12:33:53 Finished HOL-Cardinals/outline (0:00:04 elapsed time)
12:33:53 Timing HOL-Cardinals (8 threads, 10.884s elapsed time, 75.394s cpu time, 1.460s GC time, factor 6.93)
12:33:53 Finished HOL-Cardinals (0:00:19 elapsed time, 0:01:30 cpu time, factor 4.70)
12:33:53 Running Tree_Enumeration (on hpcisabelle/0) ...
12:33:55 Tree_Enumeration: theory HOL-Combinatorics.Transposition
12:33:55 Tree_Enumeration: theory HOL-Library.Cancellation
12:33:55 Tree_Enumeration: theory HOL-Library.FuncSet
12:33:55 Tree_Enumeration: theory HOL-Library.Nat_Bijection
12:33:55 Tree_Enumeration: theory HOL-Library.Infinite_Set
12:33:55 Tree_Enumeration: theory HOL-Library.Old_Datatype
12:33:55 Tree_Enumeration: theory HOL-Library.Sublist
12:33:55 Tree_Enumeration: theory HOL-Library.Liminf_Limsup
12:33:56 Tree_Enumeration: theory HOL-Library.Disjoint_Sets
12:33:56 Tree_Enumeration: theory HOL-Library.Countable
12:33:57 Tree_Enumeration: theory HOL-Library.Multiset
12:33:57 Tree_Enumeration: theory Card_Partitions.Set_Partition
12:33:58 Tree_Enumeration: theory HOL-Library.Countable_Set
12:33:58 Tree_Enumeration: theory HOL-Library.FSet
12:33:59 Tree_Enumeration: theory HOL-Library.Countable_Complete_Lattices
12:34:02 Tree_Enumeration: theory HOL-Library.Order_Continuity
12:34:03 Tree_Enumeration: theory HOL-Library.Multiset_Order
12:34:03 Tree_Enumeration: theory HOL-Combinatorics.Permutations
12:34:04 Tree_Enumeration: theory HOL-Library.Extended_Nat
12:34:04 Tree_Enumeration: theory Nested_Multisets_Ordinals.Multiset_More
12:34:05 Tree_Enumeration: theory HOL-Library.Extended_Real
12:34:05 Tree_Enumeration: theory HOL-Combinatorics.Multiset_Permutations
12:34:06 Tree_Enumeration: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
12:34:06 Tree_Enumeration: theory Design_Theory.Multisets_Extras
12:34:07 Tree_Enumeration: theory Design_Theory.Design_Basics
12:34:08 Tree_Enumeration: theory Design_Theory.Design_Operations
12:34:09 Tree_Enumeration: theory Girth_Chromatic.Girth_Chromatic_Misc
12:34:09 Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Basics
12:34:10 Tree_Enumeration: theory Design_Theory.Block_Designs
12:34:12 Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Triangles
12:34:13 Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Walks
12:34:13 Tree_Enumeration: theory Design_Theory.BIBD
12:34:14 Tree_Enumeration: theory Undirected_Graph_Theory.Bipartite_Graphs
12:34:14 Tree_Enumeration: theory Undirected_Graph_Theory.Connectivity
12:34:15 Tree_Enumeration: theory Design_Theory.Resolvable_Designs
12:34:16 Tree_Enumeration: theory Undirected_Graph_Theory.Girth_Independence
12:34:16 Tree_Enumeration: theory Design_Theory.Group_Divisible_Designs
12:34:18 Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Theory_Relations
12:34:21 Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graphs_Root
12:34:22 Tree_Enumeration: theory Tree_Enumeration.Tree_Graph
12:34:29 Tree_Enumeration: theory Tree_Enumeration.Labeled_Tree_Enumeration
12:34:29 Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree
12:34:40 Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree_Enumeration
12:35:09 Preparing Tree_Enumeration/document ...
12:35:15 Finished Tree_Enumeration/document (0:00:06 elapsed time)
12:35:15 Preparing Tree_Enumeration/outline ...
12:35:19 Finished Tree_Enumeration/outline (0:00:03 elapsed time)
12:35:19 Timing Tree_Enumeration (8 threads, 71.041s elapsed time, 518.195s cpu time, 16.055s GC time, factor 7.29)
12:35:19 Finished Tree_Enumeration (0:01:13 elapsed time, 0:08:44 cpu time, factor 7.14)
12:35:19 Running S_Finite_Measure_Monad (on hpcisabelle/1) ...
12:35:22 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QuasiBorel
12:35:22 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Lemmas_StandardBorel
12:35:24 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Space
12:35:24 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.QBS_Morphism
12:35:26 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Set_Based_Metric_Product
12:35:27 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
12:35:27 S_Finite_Measure_Monad: theory Standard_Borel_Spaces.StandardBorel
12:35:28 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Lemmas_S_Finite_Measure_Monad
12:35:28 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Kernels
12:35:29 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Measure_QuasiBorel_Adjunction
12:35:31 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Monad_QuasiBorel
12:35:38 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Montecarlo
12:35:38 S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Query
12:36:44 Preparing S_Finite_Measure_Monad/document ...
12:37:03 Finished S_Finite_Measure_Monad/document (0:00:19 elapsed time)
12:37:03 Preparing S_Finite_Measure_Monad/outline ...
12:37:11 Finished S_Finite_Measure_Monad/outline (0:00:08 elapsed time)
12:37:11 Timing S_Finite_Measure_Monad (8 threads, 79.665s elapsed time, 484.004s cpu time, 6.997s GC time, factor 6.08)
12:37:11 Finished S_Finite_Measure_Monad (0:01:23 elapsed time, 0:08:09 cpu time, factor 5.89)
12:37:11 Building Sqrt_Babylonian (on hpcisabelle/2) ...
12:37:13 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
12:37:14 Sqrt_Babylonian: theory Sqrt_Babylonian.Log_Impl
12:37:14 Sqrt_Babylonian: theory Sqrt_Babylonian.NthRoot_Impl
12:37:15 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian
12:37:28 Preparing Sqrt_Babylonian/document ...
12:37:32 Finished Sqrt_Babylonian/document (0:00:03 elapsed time)
12:37:32 Preparing Sqrt_Babylonian/outline ...
12:37:35 Finished Sqrt_Babylonian/outline (0:00:02 elapsed time)
12:37:35 Timing Sqrt_Babylonian (8 threads, 9.153s elapsed time, 31.401s cpu time, 0.482s GC time, factor 3.43)
12:37:35 Finished Sqrt_Babylonian (0:00:16 elapsed time, 0:00:43 cpu time, factor 2.71)
12:37:35 Running Turans_Graph_Theorem (on hpcisabelle/3) ...
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Code_Abstract_Nat
12:37:38 Turans_Graph_Theorem: theory HOL-Decision_Procs.Dense_Linear_Order
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Int
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Lattice_Algebras
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Log_Nat
12:37:38 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Nat
12:37:38 Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
12:37:38 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
12:37:38 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral
12:37:44 Turans_Graph_Theorem: theory HOL-Library.Interval
12:37:44 Turans_Graph_Theorem: theory HOL-Library.Float
12:37:47 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
12:37:48 Turans_Graph_Theorem: theory HOL-Library.Interval_Float
12:37:49 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
12:37:55 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
12:38:40 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
12:38:43 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
12:38:45 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
12:38:46 Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
12:38:55 Preparing Turans_Graph_Theorem/document ...
12:38:58 Finished Turans_Graph_Theorem/document (0:00:03 elapsed time)
12:38:58 Preparing Turans_Graph_Theorem/outline ...
12:39:00 Finished Turans_Graph_Theorem/outline (0:00:02 elapsed time)
12:39:00 Timing Turans_Graph_Theorem (8 threads, 75.119s elapsed time, 304.575s cpu time, 5.307s GC time, factor 4.05)
12:39:00 Finished Turans_Graph_Theorem (0:01:18 elapsed time, 0:05:10 cpu time, factor 3.95)
12:39:00 Building Complex_Geometry (on hpcisabelle/4) ...
12:39:01 Complex_Geometry: theory Complex_Geometry.More_Set
12:39:01 Complex_Geometry: theory Complex_Geometry.Linear_Systems
12:39:01 Complex_Geometry: theory HOL-Analysis.Inner_Product
12:39:01 Complex_Geometry: theory HOL-Library.Product_Plus
12:39:01 Complex_Geometry: theory HOL-Analysis.L2_Norm
12:39:01 Complex_Geometry: theory HOL-Library.Periodic_Fun
12:39:01 Complex_Geometry: theory HOL-Library.Quadratic_Discriminant
12:39:02 Complex_Geometry: theory HOL-Analysis.Product_Vector
12:39:02 Complex_Geometry: theory Complex_Geometry.More_Transcendental
12:39:02 Complex_Geometry: theory Complex_Geometry.Canonical_Angle
12:39:02 Complex_Geometry: theory Complex_Geometry.More_Complex
12:39:03 Complex_Geometry: theory Complex_Geometry.Angles
12:39:03 Complex_Geometry: theory Complex_Geometry.Quadratic
12:39:03 Complex_Geometry: theory Complex_Geometry.Elementary_Complex_Geometry
12:39:04 Complex_Geometry: theory Complex_Geometry.Matrices
12:39:04 Complex_Geometry: theory HOL-Analysis.Euclidean_Space
12:39:06 Complex_Geometry: theory Complex_Geometry.Homogeneous_Coordinates
12:39:06 Complex_Geometry: theory Complex_Geometry.Unitary11_Matrices
12:39:06 Complex_Geometry: theory Complex_Geometry.Unitary_Matrices
12:39:06 Complex_Geometry: theory Complex_Geometry.Hermitean_Matrices
12:39:08 Complex_Geometry: theory Complex_Geometry.Moebius
12:39:09 Complex_Geometry: theory Complex_Geometry.Circlines
12:39:12 Complex_Geometry: theory Complex_Geometry.Oriented_Circlines
12:39:12 Complex_Geometry: theory Complex_Geometry.Riemann_Sphere
12:39:13 Complex_Geometry: theory Complex_Geometry.Circlines_Angle
12:39:13 Complex_Geometry: theory Complex_Geometry.Unit_Circle_Preserving_Moebius
12:39:14 Complex_Geometry: theory Complex_Geometry.Chordal_Metric
12:39:53 Preparing Complex_Geometry/document ...
12:40:08 Finished Complex_Geometry/document (0:00:15 elapsed time)
12:40:08 Preparing Complex_Geometry/outline ...
12:40:16 Finished Complex_Geometry/outline (0:00:07 elapsed time)
12:40:16 Timing Complex_Geometry (8 threads, 42.315s elapsed time, 231.157s cpu time, 3.880s GC time, factor 5.46)
12:40:16 Finished Complex_Geometry (0:00:51 elapsed time, 0:04:07 cpu time, factor 4.81)
12:40:16 Running PAPP_Impossibility (on hpcisabelle/5) ...
12:40:18 PAPP_Impossibility: theory PAPP_Impossibility.SAT_Replay
12:40:19 PAPP_Impossibility: theory PAPP_Impossibility.PAPP_Multiset_Extras
12:40:19 PAPP_Impossibility: theory List-Index.List_Index
12:40:19 PAPP_Impossibility: theory HOL-Combinatorics.Transposition
12:40:19 PAPP_Impossibility: theory HOL-Combinatorics.Permutations
12:40:21 PAPP_Impossibility: theory Randomised_Social_Choice.Order_Predicates
12:40:22 PAPP_Impossibility: theory PAPP_Impossibility.Anonymous_PAPP
12:40:26 PAPP_Impossibility: theory PAPP_Impossibility.Anonymous_PAPP_Lowering
12:40:26 PAPP_Impossibility: theory PAPP_Impossibility.PAPP_Impossibility_Base_Case
12:40:28 PAPP_Impossibility: theory PAPP_Impossibility.PAPP_Impossibility
12:41:36 Preparing PAPP_Impossibility/document ...
12:41:43 Finished PAPP_Impossibility/document (0:00:06 elapsed time)
12:41:43 Preparing PAPP_Impossibility/outline ...
12:41:48 Finished PAPP_Impossibility/outline (0:00:05 elapsed time)
12:41:48 Timing PAPP_Impossibility (8 threads, 77.196s elapsed time, 250.706s cpu time, 9.205s GC time, factor 3.25)
12:41:48 Finished PAPP_Impossibility (0:01:19 elapsed time, 0:04:14 cpu time, factor 3.19)
12:41:49 Running Vickrey_Clarke_Groves (on hpcisabelle/6) ...
12:41:51 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Argmax
12:41:51 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.SetUtils
12:41:51 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Partitions
12:41:51 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationOperators
12:41:52 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationProperties
12:41:52 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.MiscTools
12:41:55 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.StrictCombinatorialAuction
12:41:56 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Universes
12:41:57 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.UniformTieBreaking
12:41:59 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuction
12:42:00 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction
12:42:28 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples
12:42:28 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.FirstPrice
12:43:05 Preparing Vickrey_Clarke_Groves/document ...
12:43:12 Finished Vickrey_Clarke_Groves/document (0:00:07 elapsed time)
12:43:12 Preparing Vickrey_Clarke_Groves/outline ...
12:43:17 Finished Vickrey_Clarke_Groves/outline (0:00:05 elapsed time)
12:43:17 Timing Vickrey_Clarke_Groves (8 threads, 73.142s elapsed time, 283.258s cpu time, 4.439s GC time, factor 3.87)
12:43:17 Finished Vickrey_Clarke_Groves (0:01:15 elapsed time, 0:04:47 cpu time, factor 3.79)
12:43:17 Building Applicative_Lifting (on hpcisabelle/7) ...
12:43:20 Applicative_Lifting: theory Applicative_Lifting.Applicative
12:43:20 Applicative_Lifting: theory Applicative_Lifting.Joinable
12:43:20 Applicative_Lifting: theory HOL-Library.State_Monad
12:43:20 Applicative_Lifting: theory HOL-Library.Function_Algebras
12:43:20 Applicative_Lifting: theory HOL-Library.Confluence
12:43:20 Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
12:43:20 Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation
12:43:20 Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda
12:43:21 Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef
12:43:21 Applicative_Lifting: theory HOL-Library.Confluent_Quotient
12:43:21 Applicative_Lifting: theory HOL-Library.Function_Division
12:43:21 Applicative_Lifting: theory HOL-Library.Dlist
12:43:22 Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed
12:43:22 Applicative_Lifting: theory HOL-Proofs-Lambda.Eta
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_List
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_State
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Combinators
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
12:43:23 Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
12:43:26 Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
12:43:29 Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
12:43:35 Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
12:43:39 Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
12:43:40 Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
12:44:00 Preparing Applicative_Lifting/document ...
12:44:05 Finished Applicative_Lifting/document (0:00:05 elapsed time)
12:44:05 Preparing Applicative_Lifting/outline ...
12:44:09 Finished Applicative_Lifting/outline (0:00:03 elapsed time)
12:44:09 Timing Applicative_Lifting (8 threads, 20.511s elapsed time, 88.748s cpu time, 2.706s GC time, factor 4.33)
12:44:09 Finished Applicative_Lifting (0:00:41 elapsed time, 0:02:09 cpu time, factor 3.13)
12:44:09 Building Girth_Chromatic (on hpcisabelle/0) ...
12:44:12 Girth_Chromatic: theory HOL-Library.Code_Target_Int
12:44:12 Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
12:44:12 Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
12:44:12 Girth_Chromatic: theory HOL-Library.Lattice_Algebras
12:44:12 Girth_Chromatic: theory HOL-Library.Log_Nat
12:44:12 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
12:44:12 Girth_Chromatic: theory HOL-Library.Code_Target_Nat
12:44:12 Girth_Chromatic: theory Girth_Chromatic.Ugraphs
12:44:12 Girth_Chromatic: theory HOL-Library.Code_Target_Numeral
12:44:19 Girth_Chromatic: theory HOL-Library.Interval
12:44:19 Girth_Chromatic: theory HOL-Library.Float
12:44:22 Girth_Chromatic: theory HOL-Library.Code_Target_Numeral_Float
12:44:22 Girth_Chromatic: theory HOL-Library.Interval_Float
12:44:23 Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
12:44:29 Girth_Chromatic: theory HOL-Decision_Procs.Approximation
12:45:14 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
12:45:38 Preparing Girth_Chromatic/document ...
12:45:41 Finished Girth_Chromatic/document (0:00:03 elapsed time)
12:45:41 Preparing Girth_Chromatic/outline ...
12:45:44 Finished Girth_Chromatic/outline (0:00:02 elapsed time)
12:45:44 Timing Girth_Chromatic (8 threads, 67.989s elapsed time, 254.576s cpu time, 4.169s GC time, factor 3.74)
12:45:44 Finished Girth_Chromatic (0:01:27 elapsed time, 0:04:52 cpu time, factor 3.33)
12:45:44 Running Separation_Logic_Imperative_HOL (on hpcisabelle/1) ...
12:45:46 Separation_Logic_Imperative_HOL: theory Word_Lib.Bit_Comprehension
12:45:46 Separation_Logic_Imperative_HOL: theory HOL-Eisbach.Eisbach
12:45:46 Separation_Logic_Imperative_HOL: theory Word_Lib.More_Divides
12:45:46 Separation_Logic_Imperative_HOL: theory Word_Lib.Signed_Division_Word
12:45:46 Separation_Logic_Imperative_HOL: theory HOL-ex.Quicksort
12:45:46 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Int_Integer_Conversion
12:45:46 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Syntax_Match
12:45:46 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap
12:45:46 Separation_Logic_Imperative_HOL: theory Word_Lib.More_Arithmetic
12:45:46 Separation_Logic_Imperative_HOL: theory Word_Lib.More_Bit_Ring
12:45:48 Separation_Logic_Imperative_HOL: theory Automatic_Refinement.Misc
12:45:48 Separation_Logic_Imperative_HOL: theory Word_Lib.More_Word
12:45:48 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
12:45:50 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Word_Base
12:45:50 Separation_Logic_Imperative_HOL: theory Word_Lib.Bit_Shifts_Infix_Syntax
12:45:50 Separation_Logic_Imperative_HOL: theory Word_Lib.Least_significant_bit
12:45:51 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Array
12:45:52 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Ref
12:45:52 Separation_Logic_Imperative_HOL: theory Word_Lib.Most_significant_bit
12:45:52 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
12:45:52 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
12:45:52 Separation_Logic_Imperative_HOL: theory Word_Lib.Generic_set_bit
12:45:54 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Integer_Bit
12:45:54 Separation_Logic_Imperative_HOL: theory Native_Word.Word_Type_Copies
12:46:08 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Int_Bit
12:46:08 Separation_Logic_Imperative_HOL: theory Native_Word.Uint32
12:46:08 Separation_Logic_Imperative_HOL: theory Collections.Code_Target_ICF
12:46:10 Separation_Logic_Imperative_HOL: theory Collections.HashCode
12:46:12 Separation_Logic_Imperative_HOL: theory Collections.Partial_Equivalence_Relation
12:46:12 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Run
12:46:12 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Assertions
12:46:14 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hoare_Triple
12:46:15 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Automation
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Main
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.List_Seg
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Union_Find
12:46:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Table
12:46:17 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Circ_List
12:46:18 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Open_List
12:46:20 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map
12:46:21 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
12:46:26 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
12:46:32 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Idioms
12:46:32 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.To_List_GA
12:46:36 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
12:46:36 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Blit
12:46:53 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
12:46:53 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
12:46:53 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.From_List_GA
12:46:54 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Examples
12:46:58 Preparing Separation_Logic_Imperative_HOL/document ...
12:47:04 Finished Separation_Logic_Imperative_HOL/document (0:00:05 elapsed time)
12:47:04 Preparing Separation_Logic_Imperative_HOL/outline ...
12:47:08 Finished Separation_Logic_Imperative_HOL/outline (0:00:04 elapsed time)
12:47:08 Timing Separation_Logic_Imperative_HOL (8 threads, 69.566s elapsed time, 199.105s cpu time, 6.152s GC time, factor 2.86)
12:47:08 Finished Separation_Logic_Imperative_HOL (0:01:12 elapsed time, 0:03:24 cpu time, factor 2.83)
12:47:08 Running VYDRA_MDL (on hpcisabelle/2) ...
12:47:11 VYDRA_MDL: theory VYDRA_MDL.NFA
12:47:11 VYDRA_MDL: theory VYDRA_MDL.Timestamp
12:47:15 VYDRA_MDL: theory VYDRA_MDL.Interval
12:47:15 VYDRA_MDL: theory VYDRA_MDL.Timestamp_Lex
12:47:15 VYDRA_MDL: theory VYDRA_MDL.Timestamp_Prod
12:47:15 VYDRA_MDL: theory VYDRA_MDL.Trace
12:47:15 VYDRA_MDL: theory VYDRA_MDL.Window
12:47:16 VYDRA_MDL: theory VYDRA_MDL.Metric_Point_Structure
12:47:16 VYDRA_MDL: theory VYDRA_MDL.MDL
12:47:26 VYDRA_MDL: theory VYDRA_MDL.Preliminaries
12:47:26 VYDRA_MDL: theory VYDRA_MDL.Temporal
12:47:31 VYDRA_MDL: theory VYDRA_MDL.Monitor
12:47:44 VYDRA_MDL: theory VYDRA_MDL.Monitor_Code
12:48:17 Preparing VYDRA_MDL/document ...
12:48:27 Finished VYDRA_MDL/document (0:00:10 elapsed time)
12:48:27 Preparing VYDRA_MDL/outline ...
12:48:32 Finished VYDRA_MDL/outline (0:00:05 elapsed time)
12:48:32 Timing VYDRA_MDL (8 threads, 63.366s elapsed time, 384.165s cpu time, 9.714s GC time, factor 6.06)
12:48:32 Finished VYDRA_MDL (0:01:07 elapsed time, 0:06:33 cpu time, factor 5.85)
12:48:33 Running Edwards_Elliptic_Curves_Group (on hpcisabelle/3) ...
12:48:34 Edwards_Elliptic_Curves_Group: theory HOL-Library.FuncSet
12:48:34 Edwards_Elliptic_Curves_Group: theory HOL-Library.Rewrite
12:48:35 Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Congruence
12:48:36 Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Order
12:48:37 Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Lattice
12:48:39 Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Complete_Lattice
12:48:40 Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Group
12:48:42 Edwards_Elliptic_Curves_Group: theory Edwards_Elliptic_Curves_Group.Edwards_Elliptic_Curves_Group
12:49:52 Preparing Edwards_Elliptic_Curves_Group/document ...
12:50:03 Finished Edwards_Elliptic_Curves_Group/document (0:00:11 elapsed time)
12:50:03 Preparing Edwards_Elliptic_Curves_Group/outline ...
12:50:07 Finished Edwards_Elliptic_Curves_Group/outline (0:00:03 elapsed time)
12:50:07 Timing Edwards_Elliptic_Curves_Group (8 threads, 75.540s elapsed time, 313.276s cpu time, 5.528s GC time, factor 4.15)
12:50:07 Finished Edwards_Elliptic_Curves_Group (0:01:17 elapsed time, 0:05:17 cpu time, factor 4.09)
12:50:07 Running Furstenberg_Topology (on hpcisabelle/4) ...
12:50:10 Furstenberg_Topology: theory HOL-Number_Theory.Cong
12:50:10 Furstenberg_Topology: theory HOL-Algebra.Congruence
12:50:10 Furstenberg_Topology: theory HOL-Library.Power_By_Squaring
12:50:10 Furstenberg_Topology: theory HOL-Number_Theory.Eratosthenes
12:50:10 Furstenberg_Topology: theory HOL-Number_Theory.Prime_Powers
12:50:10 Furstenberg_Topology: theory HOL-Number_Theory.Fib
12:50:11 Furstenberg_Topology: theory HOL-Algebra.Order
12:50:12 Furstenberg_Topology: theory HOL-Number_Theory.Mod_Exp
12:50:12 Furstenberg_Topology: theory HOL-Number_Theory.Totient
12:50:13 Furstenberg_Topology: theory HOL-Algebra.Lattice
12:50:14 Furstenberg_Topology: theory HOL-Algebra.Complete_Lattice
12:50:15 Furstenberg_Topology: theory HOL-Algebra.Group
12:50:18 Furstenberg_Topology: theory HOL-Algebra.Coset
12:50:19 Furstenberg_Topology: theory HOL-Algebra.FiniteProduct
12:50:20 Furstenberg_Topology: theory HOL-Algebra.Ring
12:50:21 Furstenberg_Topology: theory HOL-Algebra.Generated_Groups
12:50:22 Furstenberg_Topology: theory HOL-Algebra.Elementary_Groups
12:50:24 Furstenberg_Topology: theory HOL-Algebra.AbelCoset
12:50:24 Furstenberg_Topology: theory HOL-Algebra.Module
12:50:29 Furstenberg_Topology: theory HOL-Algebra.Ideal
12:50:32 Furstenberg_Topology: theory HOL-Algebra.RingHom
12:50:34 Furstenberg_Topology: theory HOL-Algebra.UnivPoly
12:50:48 Furstenberg_Topology: theory HOL-Algebra.Multiplicative_Group
12:50:52 Furstenberg_Topology: theory HOL-Number_Theory.Residues
12:50:55 Furstenberg_Topology: theory HOL-Number_Theory.Euler_Criterion
12:50:55 Furstenberg_Topology: theory HOL-Number_Theory.Pocklington
12:50:55 Furstenberg_Topology: theory HOL-Number_Theory.Gauss
12:50:56 Furstenberg_Topology: theory HOL-Number_Theory.Quadratic_Reciprocity
12:50:56 Furstenberg_Topology: theory HOL-Number_Theory.Residue_Primitive_Roots
12:50:56 Furstenberg_Topology: theory HOL-Number_Theory.Number_Theory
12:50:58 Furstenberg_Topology: theory Furstenberg_Topology.Furstenberg_Topology
12:51:12 Preparing Furstenberg_Topology/document ...
12:51:15 Finished Furstenberg_Topology/document (0:00:02 elapsed time)
12:51:15 Preparing Furstenberg_Topology/outline ...
12:51:18 Finished Furstenberg_Topology/outline (0:00:02 elapsed time)
12:51:18 Timing Furstenberg_Topology (8 threads, 60.192s elapsed time, 343.497s cpu time, 10.519s GC time, factor 5.71)
12:51:18 Finished Furstenberg_Topology (0:01:03 elapsed time, 0:05:49 cpu time, factor 5.51)
12:51:18 Running Verified_SAT_Based_AI_Planning (on hpcisabelle/5) ...
12:51:19 Verified_SAT_Based_AI_Planning: theory HOL-Library.Nat_Bijection
12:51:19 Verified_SAT_Based_AI_Planning: theory HOL-Library.Case_Converter
12:51:19 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.List_Supplement
12:51:19 Verified_SAT_Based_AI_Planning: theory HOL-Library.Old_Datatype
12:51:19 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.Map_Supplement
12:51:20 Verified_SAT_Based_AI_Planning: theory HOL-Library.Simps_Case_Conv
12:51:20 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.CNF
12:51:20 Verified_SAT_Based_AI_Planning: theory HOL-Library.Countable
12:51:21 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.CNF_Sema
12:51:22 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.Formulas
12:51:25 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.CNF_Formulas
12:51:25 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.Sema
12:51:28 Verified_SAT_Based_AI_Planning: theory Propositional_Proof_Systems.CNF_Formulas_Sema
12:51:29 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.CNF_Supplement
12:51:29 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.CNF_Semantics_Supplement
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Less_False
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Cmp
12:51:32 Verified_SAT_Based_AI_Planning: theory AI_Planning_Languages_Semantics.SASP_Semantics
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Library.Code_Abstract_Nat
12:51:32 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.State_Variable_Representation
12:51:32 Verified_SAT_Based_AI_Planning: theory List-Index.List_Index
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Library.Tree
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Sorted_Less
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Library.Code_Target_Nat
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.AList_Upd_Del
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.List_Ins_Del
12:51:32 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAS_Plus_Representation
12:51:32 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.STRIPS_Representation
12:51:32 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Set_Specs
12:51:33 Verified_SAT_Based_AI_Planning: theory AI_Planning_Languages_Semantics.SASP_Checker
12:51:33 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Map_Specs
12:51:34 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.STRIPS_Semantics
12:51:34 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAS_Plus_Semantics
12:51:35 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.AST_SAS_Plus_Equivalence
12:51:36 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAS_Plus_STRIPS
12:51:36 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAT_Plan_Base
12:51:36 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Tree2
12:51:36 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Isin2
12:51:36 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Lookup2
12:51:36 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.RBT
12:51:37 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.Set2_Join
12:51:39 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions
12:51:39 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus
12:51:40 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.RBT_Set
12:51:42 Verified_SAT_Based_AI_Planning: theory HOL-Data_Structures.RBT_Map
12:51:42 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.Set2_Join_RBT
12:51:45 Verified_SAT_Based_AI_Planning: theory Verified_SAT_Based_AI_Planning.Solve_SASP
12:52:25 Preparing Verified_SAT_Based_AI_Planning/document ...
12:52:43 Finished Verified_SAT_Based_AI_Planning/document (0:00:17 elapsed time)
12:52:43 Preparing Verified_SAT_Based_AI_Planning/outline ...
12:52:50 Finished Verified_SAT_Based_AI_Planning/outline (0:00:07 elapsed time)
12:52:50 Timing Verified_SAT_Based_AI_Planning (8 threads, 64.025s elapsed time, 382.068s cpu time, 7.095s GC time, factor 5.97)
12:52:50 Finished Verified_SAT_Based_AI_Planning (0:01:06 elapsed time, 0:06:26 cpu time, factor 5.84)
12:52:50 Building Knuth_Bendix_Order (on hpcisabelle/6) ...
12:52:52 Knuth_Bendix_Order: theory Knuth_Bendix_Order.Order_Pair
12:52:53 Knuth_Bendix_Order: theory Knuth_Bendix_Order.Lexicographic_Extension
12:52:54 Knuth_Bendix_Order: theory Knuth_Bendix_Order.KBO
12:53:10 Preparing Knuth_Bendix_Order/document ...
12:53:14 Finished Knuth_Bendix_Order/document (0:00:04 elapsed time)
12:53:14 Preparing Knuth_Bendix_Order/outline ...
12:53:17 Finished Knuth_Bendix_Order/outline (0:00:03 elapsed time)
12:53:17 Timing Knuth_Bendix_Order (8 threads, 5.621s elapsed time, 35.186s cpu time, 0.579s GC time, factor 6.26)
12:53:17 Finished Knuth_Bendix_Order (0:00:19 elapsed time, 0:01:00 cpu time, factor 3.16)
12:53:17 Building HOL-Real_Asymp (on hpcisabelle/7) ...
12:53:19 HOL-Real_Asymp: theory HOL-Decision_Procs.Dense_Linear_Order
12:53:19 HOL-Real_Asymp: theory HOL-Library.BNF_Corec
12:53:19 HOL-Real_Asymp: theory HOL-Library.Code_Target_Int
12:53:19 HOL-Real_Asymp: theory HOL-Library.Code_Abstract_Nat
12:53:19 HOL-Real_Asymp: theory HOL-Real_Asymp.Inst_Existentials
12:53:19 HOL-Real_Asymp: theory HOL-Library.Set_Algebras
12:53:19 HOL-Real_Asymp: theory HOL-Library.Landau_Symbols
12:53:19 HOL-Real_Asymp: theory HOL-Library.Lattice_Algebras
12:53:19 HOL-Real_Asymp: theory HOL-Library.Log_Nat
12:53:19 HOL-Real_Asymp: theory HOL-Library.Code_Target_Nat
12:53:20 HOL-Real_Asymp: theory HOL-Real_Asymp.Eventuallize
12:53:20 HOL-Real_Asymp: theory HOL-Real_Asymp.Lazy_Eval
12:53:20 HOL-Real_Asymp: theory HOL-Library.Code_Target_Numeral
12:53:27 HOL-Real_Asymp: theory HOL-Library.Interval
12:53:27 HOL-Real_Asymp: theory HOL-Library.Float
12:53:28 HOL-Real_Asymp: theory HOL-Real_Asymp.Multiseries_Expansion
12:53:29 HOL-Real_Asymp: theory HOL-Library.Code_Target_Numeral_Float
12:53:29 HOL-Real_Asymp: theory HOL-Library.Interval_Float
12:53:31 HOL-Real_Asymp: theory HOL-Decision_Procs.Approximation_Bounds
12:53:36 HOL-Real_Asymp: theory HOL-Decision_Procs.Approximation
12:54:03 HOL-Real_Asymp: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
12:54:05 HOL-Real_Asymp: theory HOL-Real_Asymp.Real_Asymp
12:54:05 HOL-Real_Asymp: theory HOL-Real_Asymp.Real_Asymp_Examples
12:54:25 HOL-Real_Asymp: theory HOL-Real_Asymp.Real_Asymp_Approx
12:54:48 Timing HOL-Real_Asymp (8 threads, 72.326s elapsed time, 466.185s cpu time, 16.714s GC time, factor 6.45)
12:54:48 Finished HOL-Real_Asymp (0:01:28 elapsed time, 0:08:20 cpu time, factor 5.66)
12:54:49 Running Projective_Geometry (on hpcisabelle/0) ...
12:54:50 Projective_Geometry: theory Projective_Geometry.Higher_Projective_Space_Rank_Axioms
12:54:50 Projective_Geometry: theory Projective_Geometry.Higher_Projective_Space_Axioms
12:54:50 Projective_Geometry: theory Projective_Geometry.Projective_Plane_Axioms
12:54:50 Projective_Geometry: theory Projective_Geometry.Projective_Space_Axioms
12:54:50 Projective_Geometry: theory Projective_Geometry.Pappus_Property
12:54:50 Projective_Geometry: theory Projective_Geometry.Matroid_Rank_Properties
12:54:50 Projective_Geometry: theory Projective_Geometry.Desargues_2D
12:54:50 Projective_Geometry: theory Projective_Geometry.Desargues_3D
12:54:51 Projective_Geometry: theory Projective_Geometry.Pascal_Property
12:54:51 Projective_Geometry: theory Projective_Geometry.Desargues_Property
12:54:51 Projective_Geometry: theory Projective_Geometry.Pappus_Desargues
12:56:00 Preparing Projective_Geometry/document ...
12:56:06 Finished Projective_Geometry/document (0:00:05 elapsed time)
12:56:06 Preparing Projective_Geometry/outline ...
12:56:09 Finished Projective_Geometry/outline (0:00:03 elapsed time)
12:56:09 Timing Projective_Geometry (8 threads, 69.325s elapsed time, 211.378s cpu time, 3.856s GC time, factor 3.05)
12:56:09 Finished Projective_Geometry (0:01:11 elapsed time, 0:03:35 cpu time, factor 3.01)
12:56:10 Running Kneser_Cauchy_Davenport (on hpcisabelle/1) ...
12:56:12 Kneser_Cauchy_Davenport: theory Jacobson_Basic_Algebra.Set_Theory
12:56:13 Kneser_Cauchy_Davenport: theory Jacobson_Basic_Algebra.Group_Theory
12:56:30 Kneser_Cauchy_Davenport: theory Jacobson_Basic_Algebra.Ring_Theory
12:57:04 Kneser_Cauchy_Davenport: theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
12:57:05 Kneser_Cauchy_Davenport: theory Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_preliminaries
12:57:10 Kneser_Cauchy_Davenport: theory Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_main_proofs
12:57:26 Preparing Kneser_Cauchy_Davenport/document ...
12:57:31 Finished Kneser_Cauchy_Davenport/document (0:00:04 elapsed time)
12:57:31 Preparing Kneser_Cauchy_Davenport/outline ...
12:57:34 Finished Kneser_Cauchy_Davenport/outline (0:00:02 elapsed time)
12:57:34 Timing Kneser_Cauchy_Davenport (8 threads, 72.487s elapsed time, 233.548s cpu time, 5.853s GC time, factor 3.22)
12:57:34 Finished Kneser_Cauchy_Davenport (0:01:15 elapsed time, 0:04:00 cpu time, factor 3.17)
12:57:34 Running Hyperdual (on hpcisabelle/2) ...
12:57:37 Hyperdual: theory HOL-Library.Code_Abstract_Nat
12:57:37 Hyperdual: theory HOL-Decision_Procs.Dense_Linear_Order
12:57:37 Hyperdual: theory HOL-Library.Code_Target_Int
12:57:37 Hyperdual: theory HOL-Library.Lattice_Algebras
12:57:37 Hyperdual: theory HOL-Library.Log_Nat
12:57:37 Hyperdual: theory Hyperdual.Hyperdual
12:57:37 Hyperdual: theory Hyperdual.TwiceFieldDifferentiable
12:57:37 Hyperdual: theory HOL-Library.Code_Target_Nat
12:57:37 Hyperdual: theory HOL-Library.Code_Target_Numeral
12:57:40 Hyperdual: theory Hyperdual.HyperdualFunctionExtension
12:57:43 Hyperdual: theory Hyperdual.LogisticFunction
12:57:44 Hyperdual: theory HOL-Library.Interval
12:57:45 Hyperdual: theory HOL-Library.Float
12:57:48 Hyperdual: theory HOL-Library.Code_Target_Numeral_Float
12:57:48 Hyperdual: theory HOL-Library.Interval_Float
12:57:50 Hyperdual: theory HOL-Decision_Procs.Approximation_Bounds
12:57:56 Hyperdual: theory HOL-Decision_Procs.Approximation
12:58:40 Hyperdual: theory Hyperdual.AnalyticTestFunction
12:58:52 Preparing Hyperdual/document ...
12:59:00 Finished Hyperdual/document (0:00:07 elapsed time)
12:59:00 Preparing Hyperdual/outline ...
12:59:05 Finished Hyperdual/outline (0:00:05 elapsed time)
12:59:05 Timing Hyperdual (8 threads, 73.894s elapsed time, 308.947s cpu time, 9.774s GC time, factor 4.18)
12:59:05 Finished Hyperdual (0:01:17 elapsed time, 0:05:14 cpu time, factor 4.08)
12:59:06 Running HOL-Hoare_Parallel (on hpcisabelle/3) ...
12:59:07 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph
12:59:07 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com
12:59:07 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote
12:59:07 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com
12:59:08 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran
12:59:10 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran
12:59:11 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare
12:59:12 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare
12:59:12 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax
12:59:12 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples
12:59:13 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics
12:59:14 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax
12:59:14 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll
12:59:14 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll
12:59:14 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples
12:59:18 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel
13:00:19 Preparing HOL-Hoare_Parallel/document ...
13:00:28 Finished HOL-Hoare_Parallel/document (0:00:09 elapsed time)
13:00:28 Preparing HOL-Hoare_Parallel/outline ...
13:00:34 Finished HOL-Hoare_Parallel/outline (0:00:05 elapsed time)
13:00:34 Timing HOL-Hoare_Parallel (8 threads, 70.858s elapsed time, 478.936s cpu time, 5.421s GC time, factor 6.76)
13:00:34 Finished HOL-Hoare_Parallel (0:01:13 elapsed time, 0:08:03 cpu time, factor 6.62)
13:00:34 Running Corec (on hpcisabelle/4) ...
13:00:36 Corec: theory HOL-Library.BNF_Corec
13:00:45 Corec: theory Corec.Corec
13:01:45 Preparing Corec/corec ...
13:01:48 Finished Corec/corec (0:00:03 elapsed time)
13:01:48 Timing Corec (8 threads, 67.466s elapsed time, 117.510s cpu time, 4.477s GC time, factor 1.74)
13:01:48 Finished Corec (0:01:10 elapsed time, 0:02:05 cpu time, factor 1.77)
13:01:48 Running Ordinal_Partitions (on hpcisabelle/5) ...
13:01:50 Ordinal_Partitions: theory HOL-Cardinals.Order_Union
13:01:50 Ordinal_Partitions: theory HOL-Cardinals.Order_Relation_More
13:01:50 Ordinal_Partitions: theory HOL-Cardinals.Fun_More
13:01:50 Ordinal_Partitions: theory HOL-Library.Infinite_Set
13:01:50 Ordinal_Partitions: theory HOL-Library.Nat_Bijection
13:01:50 Ordinal_Partitions: theory HOL-Library.FuncSet
13:01:50 Ordinal_Partitions: theory HOL-Library.Old_Datatype
13:01:50 Ordinal_Partitions: theory HOL-Library.Product_Lexorder
13:01:51 Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Extension
13:01:51 Ordinal_Partitions: theory HOL-Cardinals.Wellfounded_More
13:01:51 Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Relation
13:01:52 Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Embedding
13:01:52 Ordinal_Partitions: theory HOL-Library.Countable
13:01:52 Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Constructions
13:01:53 Ordinal_Partitions: theory HOL-Cardinals.Cardinal_Order_Relation
13:01:53 Ordinal_Partitions: theory HOL-Cardinals.Ordinal_Arithmetic
13:01:54 Ordinal_Partitions: theory HOL-Library.Countable_Set
13:01:54 Ordinal_Partitions: theory HOL-Cardinals.Cardinal_Arithmetic
13:01:55 Ordinal_Partitions: theory HOL-Library.Equipollence
13:01:55 Ordinal_Partitions: theory HOL-Cardinals.Cardinals
13:01:55 Ordinal_Partitions: theory HOL-Library.Ramsey
13:01:55 Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Library
13:01:55 Ordinal_Partitions: theory ZFC_in_HOL.ZFC_in_HOL
13:01:56 Ordinal_Partitions: theory Nash_Williams.Nash_Extras
13:01:56 Ordinal_Partitions: theory Nash_Williams.Nash_Williams
13:01:56 Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Cardinals
13:01:58 Ordinal_Partitions: theory ZFC_in_HOL.Kirby
13:01:58 Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Typeclasses
13:01:59 Ordinal_Partitions: theory ZFC_in_HOL.Ordinal_Exp
13:01:59 Ordinal_Partitions: theory Ordinal_Partitions.Library_Additions
13:01:59 Ordinal_Partitions: theory ZFC_in_HOL.Cantor_NF
13:02:00 Ordinal_Partitions: theory Ordinal_Partitions.Partitions
13:02:01 Ordinal_Partitions: theory Ordinal_Partitions.Erdos_Milner
13:02:01 Ordinal_Partitions: theory Ordinal_Partitions.Omega_Omega
13:03:02 Preparing Ordinal_Partitions/document ...
13:03:12 Finished Ordinal_Partitions/document (0:00:09 elapsed time)
13:03:12 Preparing Ordinal_Partitions/outline ...
13:03:16 Finished Ordinal_Partitions/outline (0:00:03 elapsed time)
13:03:16 Timing Ordinal_Partitions (8 threads, 69.672s elapsed time, 503.470s cpu time, 7.580s GC time, factor 7.23)
13:03:16 Finished Ordinal_Partitions (0:01:12 elapsed time, 0:08:29 cpu time, factor 7.06)
13:03:16 Running EdmondsKarp_Maxflow (on hpcisabelle/6) ...
13:03:19 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
13:03:19 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.FordFulkerson_Algo
13:03:19 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
13:03:25 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Algo
13:03:36 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
13:03:54 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Checked_Impl
13:04:19 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Benchmark_Export
13:04:29 Preparing EdmondsKarp_Maxflow/document ...
13:04:34 Finished EdmondsKarp_Maxflow/document (0:00:04 elapsed time)
13:04:34 Preparing EdmondsKarp_Maxflow/outline ...
13:04:37 Finished EdmondsKarp_Maxflow/outline (0:00:03 elapsed time)
13:04:37 Timing EdmondsKarp_Maxflow (8 threads, 68.569s elapsed time, 108.007s cpu time, 2.195s GC time, factor 1.58)
13:04:37 Finished EdmondsKarp_Maxflow (0:01:12 elapsed time, 0:01:54 cpu time, factor 1.58)
13:04:38 Running Chebyshev_Polynomials (on hpcisabelle/7) ...
13:04:40 Chebyshev_Polynomials: theory HOL-Library.More_List
13:04:40 Chebyshev_Polynomials: theory Polynomial_Interpolation.Missing_Unsorted
13:04:40 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Fraction_Field
13:04:40 Chebyshev_Polynomials: theory Polynomial_Interpolation.Ring_Hom
13:04:41 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Polynomial
13:04:42 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Normalized_Fraction
13:04:53 Chebyshev_Polynomials: theory Chebyshev_Polynomials.Chebyshev_Polynomials_Library
13:04:53 Chebyshev_Polynomials: theory Chebyshev_Polynomials.Polynomial_Transfer
13:04:53 Chebyshev_Polynomials: theory Descartes_Sign_Rule.Descartes_Sign_Rule
13:04:53 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Polynomial_FPS
13:04:53 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Polynomial_Factorial
13:04:54 Chebyshev_Polynomials: theory HOL-Computational_Algebra.Formal_Laurent_Series
13:04:55 Chebyshev_Polynomials: theory Polynomial_Interpolation.Missing_Polynomial
13:04:57 Chebyshev_Polynomials: theory Polynomial_Interpolation.Ring_Hom_Poly
13:05:00 Chebyshev_Polynomials: theory Chebyshev_Polynomials.Chebyshev_Polynomials
13:05:11 Preparing Chebyshev_Polynomials/document ...
13:05:25 Finished Chebyshev_Polynomials/document (0:00:14 elapsed time)
13:05:25 Preparing Chebyshev_Polynomials/outline ...
13:05:37 Finished Chebyshev_Polynomials/outline (0:00:12 elapsed time)
13:05:37 Timing Chebyshev_Polynomials (8 threads, 28.885s elapsed time, 187.127s cpu time, 4.393s GC time, factor 6.48)
13:05:37 Finished Chebyshev_Polynomials (0:00:32 elapsed time, 0:03:11 cpu time, factor 5.99)
13:05:37 Building List-Infinite (on hpcisabelle/0) ...
13:05:39 List-Infinite: theory List-Infinite.Util_NatInf
13:05:39 List-Infinite: theory List-Infinite.Util_MinMax
13:05:39 List-Infinite: theory List-Infinite.Util_Nat
13:05:39 List-Infinite: theory List-Infinite.Util_Set
13:05:40 List-Infinite: theory List-Infinite.Util_Div
13:05:41 List-Infinite: theory List-Infinite.SetInterval2
13:05:43 List-Infinite: theory List-Infinite.InfiniteSet2
13:05:43 List-Infinite: theory List-Infinite.SetIntervalCut
13:05:44 List-Infinite: theory List-Infinite.List2
13:05:44 List-Infinite: theory List-Infinite.SetIntervalStep
13:05:46 List-Infinite: theory List-Infinite.ListInf
13:05:48 List-Infinite: theory List-Infinite.ListInf_Prefix
13:05:49 List-Infinite: theory List-Infinite.ListInfinite
13:06:01 Preparing List-Infinite/document ...
13:06:09 Finished List-Infinite/document (0:00:07 elapsed time)
13:06:09 Preparing List-Infinite/outline ...
13:06:14 Finished List-Infinite/outline (0:00:05 elapsed time)
13:06:14 Timing List-Infinite (8 threads, 10.768s elapsed time, 61.286s cpu time, 1.688s GC time, factor 5.69)
13:06:14 Finished List-Infinite (0:00:23 elapsed time, 0:01:24 cpu time, factor 3.61)
13:06:14 Running HOL-Bali (on hpcisabelle/1) ...
13:06:16 HOL-Bali: theory HOL-Bali.Basis
13:06:17 HOL-Bali: theory HOL-Bali.Name
13:06:17 HOL-Bali: theory HOL-Bali.Table
13:06:19 HOL-Bali: theory HOL-Bali.Type
13:06:21 HOL-Bali: theory HOL-Bali.Value
13:06:22 HOL-Bali: theory HOL-Bali.Term
13:06:42 HOL-Bali: theory HOL-Bali.Decl
13:06:46 HOL-Bali: theory HOL-Bali.TypeRel
13:06:46 HOL-Bali: theory HOL-Bali.DeclConcepts
13:06:49 HOL-Bali: theory HOL-Bali.State
13:06:49 HOL-Bali: theory HOL-Bali.WellType
13:06:51 HOL-Bali: theory HOL-Bali.Eval
13:06:51 HOL-Bali: theory HOL-Bali.Conform
13:06:53 HOL-Bali: theory HOL-Bali.DefiniteAssignment
13:06:58 HOL-Bali: theory HOL-Bali.WellForm
13:07:00 HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect
13:07:00 HOL-Bali: theory HOL-Bali.Example
13:07:01 HOL-Bali: theory HOL-Bali.TypeSafe
13:07:03 HOL-Bali: theory HOL-Bali.Evaln
13:07:07 HOL-Bali: theory HOL-Bali.AxSem
13:07:07 HOL-Bali: theory HOL-Bali.Trans
13:07:11 HOL-Bali: theory HOL-Bali.AxCompl
13:07:12 HOL-Bali: theory HOL-Bali.AxSound
13:07:12 HOL-Bali: theory HOL-Bali.AxExample
13:07:28 Preparing HOL-Bali/document ...
13:07:47 Finished HOL-Bali/document (0:00:19 elapsed time)
13:07:47 Preparing HOL-Bali/outline ...
13:07:55 Finished HOL-Bali/outline (0:00:08 elapsed time)
13:07:55 Timing HOL-Bali (8 threads, 69.066s elapsed time, 330.756s cpu time, 7.792s GC time, factor 4.79)
13:07:55 Finished HOL-Bali (0:01:11 elapsed time, 0:05:37 cpu time, factor 4.72)
13:07:56 Running Real_Impl (on hpcisabelle/2) ...
13:07:57 Real_Impl: theory Deriving.Derive_Manager
13:07:57 Real_Impl: theory Deriving.Generator_Aux
13:07:57 Real_Impl: theory HOL-Library.Cancellation
13:07:57 Real_Impl: theory Real_Impl.Real_Impl
13:07:58 Real_Impl: theory Show.Show
13:07:58 Real_Impl: theory HOL-Library.Multiset
13:07:59 Real_Impl: theory Show.Show_Instances
13:08:01 Real_Impl: theory Show.Shows_Literal
13:08:02 Real_Impl: theory Show.Show_Real
13:08:06 Real_Impl: theory HOL-Computational_Algebra.Factorial_Ring
13:08:16 Real_Impl: theory HOL-Computational_Algebra.Euclidean_Algorithm
13:08:30 Real_Impl: theory HOL-Computational_Algebra.Primes
13:08:39 Real_Impl: theory Real_Impl.Real_Impl_Auxiliary
13:08:39 Real_Impl: theory Real_Impl.Prime_Product
13:08:39 Real_Impl: theory Real_Impl.Real_Unique_Impl
13:09:07 Preparing Real_Impl/document ...
13:09:11 Finished Real_Impl/document (0:00:03 elapsed time)
13:09:11 Preparing Real_Impl/outline ...
13:09:13 Finished Real_Impl/outline (0:00:02 elapsed time)
13:09:13 Timing Real_Impl (8 threads, 68.741s elapsed time, 204.558s cpu time, 4.292s GC time, factor 2.98)
13:09:13 Finished Real_Impl (0:01:10 elapsed time, 0:03:27 cpu time, factor 2.94)
13:09:13 Running Root_Balanced_Tree (on hpcisabelle/3) ...
13:09:15 Root_Balanced_Tree: theory Amortized_Complexity.Amortized_Framework0
13:09:15 Root_Balanced_Tree: theory Root_Balanced_Tree.Time_Monad
13:09:15 Root_Balanced_Tree: theory HOL-Data_Structures.Cmp
13:09:15 Root_Balanced_Tree: theory HOL-Data_Structures.Balance
13:09:15 Root_Balanced_Tree: theory HOL-Data_Structures.Less_False
13:09:15 Root_Balanced_Tree: theory HOL-Decision_Procs.Dense_Linear_Order
13:09:16 Root_Balanced_Tree: theory HOL-Data_Structures.Sorted_Less
13:09:16 Root_Balanced_Tree: theory HOL-Data_Structures.List_Ins_Del
13:09:16 Root_Balanced_Tree: theory HOL-Data_Structures.Set_Specs
13:09:16 Root_Balanced_Tree: theory HOL-Data_Structures.Tree_Set
13:09:20 Root_Balanced_Tree: theory HOL-Decision_Procs.Approximation_Bounds
13:09:22 Root_Balanced_Tree: theory Root_Balanced_Tree.Root_Balanced_Tree
13:09:26 Root_Balanced_Tree: theory HOL-Decision_Procs.Approximation
13:10:13 Root_Balanced_Tree: theory Root_Balanced_Tree.Root_Balanced_Tree_Tab
13:10:23 Preparing Root_Balanced_Tree/document ...
13:10:27 Finished Root_Balanced_Tree/document (0:00:04 elapsed time)
13:10:27 Preparing Root_Balanced_Tree/outline ...
13:10:30 Finished Root_Balanced_Tree/outline (0:00:03 elapsed time)
13:10:31 Timing Root_Balanced_Tree (8 threads, 66.678s elapsed time, 267.401s cpu time, 10.747s GC time, factor 4.01)
13:10:31 Finished Root_Balanced_Tree (0:01:09 elapsed time, 0:04:31 cpu time, factor 3.92)
13:10:31 Running Registers (on hpcisabelle/4) ...
13:10:34 Registers: theory HOL-Eisbach.Eisbach
13:10:34 Registers: theory HOL-Library.Type_Length
13:10:34 Registers: theory HOL-Library.Z2
13:10:34 Registers: theory Registers.Axioms
13:10:34 Registers: theory Registers.Axioms_Classical
13:10:34 Registers: theory Registers.Laws
13:10:34 Registers: theory Registers.Laws_Classical
13:10:35 Registers: theory Registers.Misc
13:10:36 Registers: theory HOL-Library.Word
13:10:36 Registers: theory Registers.Axioms_Complement
13:10:36 Registers: theory Registers.Laws_Complement
13:10:37 Registers: theory Registers.Classical_Extra
13:10:37 Registers: theory Registers.Finite_Tensor_Product
13:10:38 Registers: theory Registers.Axioms_Quantum
13:10:40 Registers: theory Registers.Finite_Tensor_Product_Matrices
13:10:40 Registers: theory Registers.Quantum
13:10:41 Registers: theory Registers.Laws_Quantum
13:10:44 Registers: theory Registers.Quantum_Extra
13:10:45 Registers: theory Registers.Axioms_Complement_Quantum
13:10:45 Registers: theory Registers.QHoare
13:10:46 Registers: theory Registers.Laws_Complement_Quantum
13:10:46 Registers: theory Registers.Teleport
13:10:47 Registers: theory Registers.Check_Autogenerated_Files
13:10:47 Registers: theory Registers.Quantum_Extra2
13:10:47 Registers: theory Registers.Pure_States
13:11:43 Preparing Registers/document ...
13:11:59 Finished Registers/document (0:00:15 elapsed time)
13:11:59 Preparing Registers/outline ...
13:12:07 Finished Registers/outline (0:00:07 elapsed time)
13:12:07 Timing Registers (8 threads, 67.218s elapsed time, 404.888s cpu time, 18.895s GC time, factor 6.02)
13:12:07 Finished Registers (0:01:11 elapsed time, 0:06:53 cpu time, factor 5.78)
13:12:07 Running MFMC_Countable (on hpcisabelle/5) ...
13:12:10 MFMC_Countable: theory Flow_Networks.Graph
13:12:10 MFMC_Countable: theory HOL-Library.Case_Converter
13:12:10 MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
13:12:10 MFMC_Countable: theory HOL-Library.While_Combinator
13:12:10 MFMC_Countable: theory HOL-Library.Simps_Case_Conv
13:12:11 MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
13:12:11 MFMC_Countable: theory MFMC_Countable.MFMC_Misc
13:12:12 MFMC_Countable: theory Flow_Networks.Network
13:12:13 MFMC_Countable: theory MFMC_Countable.MFMC_Network
13:12:14 MFMC_Countable: theory Flow_Networks.Residual_Graph
13:12:16 MFMC_Countable: theory MFMC_Countable.MFMC_Flow_Attainability
13:12:16 MFMC_Countable: theory MFMC_Countable.MFMC_Web
13:12:16 MFMC_Countable: theory Flow_Networks.Augmenting_Flow
13:12:16 MFMC_Countable: theory Flow_Networks.Augmenting_Path
13:12:17 MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
13:12:17 MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
13:12:18 MFMC_Countable: theory MFMC_Countable.MFMC_Finite
13:12:19 MFMC_Countable: theory MFMC_Countable.MFMC_Reduction
13:12:19 MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
13:12:20 MFMC_Countable: theory MFMC_Countable.MFMC_Bounded
13:12:20 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
13:12:22 MFMC_Countable: theory MFMC_Countable.MFMC_Unbounded
13:12:26 MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
13:12:26 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation_MFMC
13:13:21 Preparing MFMC_Countable/document ...
13:13:40 Finished MFMC_Countable/document (0:00:18 elapsed time)
13:13:40 Preparing MFMC_Countable/outline ...
13:13:46 Finished MFMC_Countable/outline (0:00:05 elapsed time)
13:13:46 Timing MFMC_Countable (8 threads, 68.726s elapsed time, 303.167s cpu time, 5.985s GC time, factor 4.41)
13:13:46 Finished MFMC_Countable (0:01:12 elapsed time, 0:05:10 cpu time, factor 4.28)
13:13:46 Running Factor_Algebraic_Polynomial (on hpcisabelle/6) ...
13:13:50 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
13:13:50 Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
13:13:50 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
13:13:50 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
13:13:50 Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
13:13:50 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
13:13:50 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
13:13:50 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
13:13:51 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
13:13:51 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
13:13:51 Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
13:13:51 Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
13:13:51 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
13:13:51 Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
13:13:53 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
13:13:53 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
13:13:54 Factor_Algebraic_Polynomial: theory Polynomials.Utils
13:13:54 Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
13:13:55 Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
13:13:55 Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
13:13:56 Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
13:14:11 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
13:14:14 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
13:14:14 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
13:14:14 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
13:14:16 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
13:14:30 Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
13:14:34 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
13:14:35 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
13:14:38 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
13:14:42 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
13:14:42 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
13:14:46 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
13:14:46 Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
13:15:01 Preparing Factor_Algebraic_Polynomial/document ...
13:15:10 Finished Factor_Algebraic_Polynomial/document (0:00:08 elapsed time)
13:15:10 Preparing Factor_Algebraic_Polynomial/outline ...
13:15:14 Finished Factor_Algebraic_Polynomial/outline (0:00:04 elapsed time)
13:15:14 Timing Factor_Algebraic_Polynomial (8 threads, 69.125s elapsed time, 255.178s cpu time, 6.994s GC time, factor 3.69)
13:15:14 Finished Factor_Algebraic_Polynomial (0:01:13 elapsed time, 0:04:23 cpu time, factor 3.58)
13:15:15 Running Irrationality_J_Hancl (on hpcisabelle/7) ...
13:15:17 Irrationality_J_Hancl: theory HOL-Decision_Procs.Dense_Linear_Order
13:15:17 Irrationality_J_Hancl: theory HOL-Library.Code_Abstract_Nat
13:15:17 Irrationality_J_Hancl: theory HOL-Library.Code_Target_Int
13:15:17 Irrationality_J_Hancl: theory HOL-Library.Lattice_Algebras
13:15:17 Irrationality_J_Hancl: theory HOL-Library.Log_Nat
13:15:17 Irrationality_J_Hancl: theory HOL-Library.Code_Target_Nat
13:15:18 Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral
13:15:24 Irrationality_J_Hancl: theory HOL-Library.Interval
13:15:24 Irrationality_J_Hancl: theory HOL-Library.Float
13:15:27 Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral_Float
13:15:27 Irrationality_J_Hancl: theory HOL-Library.Interval_Float
13:15:28 Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds
13:15:34 Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation
13:16:19 Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl
13:16:25 Preparing Irrationality_J_Hancl/document ...
13:16:29 Finished Irrationality_J_Hancl/document (0:00:03 elapsed time)
13:16:29 Preparing Irrationality_J_Hancl/outline ...
13:16:31 Finished Irrationality_J_Hancl/outline (0:00:02 elapsed time)
13:16:31 Timing Irrationality_J_Hancl (8 threads, 66.556s elapsed time, 253.860s cpu time, 4.280s GC time, factor 3.81)
13:16:31 Finished Irrationality_J_Hancl (0:01:09 elapsed time, 0:04:19 cpu time, factor 3.71)
13:16:32 Running Binding_Syntax_Theory (on hpcisabelle/0) ...
13:16:33 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Preliminaries
13:16:35 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Pick
13:16:35 Binding_Syntax_Theory: theory Binding_Syntax_Theory.QuasiTerms_Swap_Fresh
13:16:35 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Equiv_Relation2
13:16:40 Binding_Syntax_Theory: theory Binding_Syntax_Theory.QuasiTerms_PickFresh_Alpha
13:16:43 Binding_Syntax_Theory: theory Binding_Syntax_Theory.QuasiTerms_Environments_Substitution
13:16:44 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Transition_QuasiTerms_Terms
13:16:50 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Terms
13:16:53 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Well_Sorted_Terms
13:17:01 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Iteration
13:17:14 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Recursion
13:17:14 Binding_Syntax_Theory: theory Binding_Syntax_Theory.Semantic_Domains
13:17:43 Preparing Binding_Syntax_Theory/document ...
13:17:55 Finished Binding_Syntax_Theory/document (0:00:11 elapsed time)
13:17:55 Preparing Binding_Syntax_Theory/outline ...
13:18:02 Finished Binding_Syntax_Theory/outline (0:00:07 elapsed time)
13:18:02 Timing Binding_Syntax_Theory (8 threads, 66.590s elapsed time, 357.448s cpu time, 10.225s GC time, factor 5.37)
13:18:02 Finished Binding_Syntax_Theory (0:01:09 elapsed time, 0:06:04 cpu time, factor 5.27)
13:18:02 Building Weighted_Path_Order (on hpcisabelle/1) ...
13:18:05 Weighted_Path_Order: theory Weighted_Path_Order.Status
13:18:05 Weighted_Path_Order: theory Weighted_Path_Order.List_Order
13:18:05 Weighted_Path_Order: theory Weighted_Path_Order.Precedence
13:18:05 Weighted_Path_Order: theory Weighted_Path_Order.Relations
13:18:06 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair
13:18:07 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2
13:18:07 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair_Impl
13:18:10 Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2_Impl
13:18:15 Weighted_Path_Order: theory Weighted_Path_Order.WPO
13:18:19 Weighted_Path_Order: theory Weighted_Path_Order.KBO_Transformation
13:18:19 Weighted_Path_Order: theory Weighted_Path_Order.LPO
13:18:19 Weighted_Path_Order: theory Weighted_Path_Order.KBO_as_WPO
13:18:20 Weighted_Path_Order: theory Weighted_Path_Order.RPO
13:18:21 Weighted_Path_Order: theory Weighted_Path_Order.Executable_Orders
13:18:55 Preparing Weighted_Path_Order/document ...
13:19:06 Finished Weighted_Path_Order/document (0:00:11 elapsed time)
13:19:06 Preparing Weighted_Path_Order/outline ...
13:19:12 Finished Weighted_Path_Order/outline (0:00:05 elapsed time)
13:19:12 Timing Weighted_Path_Order (8 threads, 36.246s elapsed time, 125.371s cpu time, 2.623s GC time, factor 3.46)
13:19:12 Finished Weighted_Path_Order (0:00:51 elapsed time, 0:02:35 cpu time, factor 3.00)
13:19:12 Building Relation_Algebra (on hpcisabelle/2) ...
13:19:14 Relation_Algebra: theory Relation_Algebra.More_Boolean_Algebra
13:19:15 Relation_Algebra: theory Relation_Algebra.Relation_Algebra
13:19:19 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Models
13:19:19 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_RTC
13:19:19 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Vectors
13:19:19 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Tests
13:19:20 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Functions
13:19:24 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Direct_Products
13:19:34 Preparing Relation_Algebra/document ...
13:19:38 Finished Relation_Algebra/document (0:00:03 elapsed time)
13:19:38 Preparing Relation_Algebra/outline ...
13:19:41 Finished Relation_Algebra/outline (0:00:03 elapsed time)
13:19:41 Timing Relation_Algebra (8 threads, 12.051s elapsed time, 57.408s cpu time, 1.615s GC time, factor 4.76)
13:19:41 Finished Relation_Algebra (0:00:21 elapsed time, 0:01:15 cpu time, factor 3.48)
13:19:41 Running Physical_Quantities (on hpcisabelle/3) ...
13:19:42 Physical_Quantities: theory HOL-Eisbach.Eisbach
13:19:42 Physical_Quantities: theory HOL-Decision_Procs.Dense_Linear_Order
13:19:42 Physical_Quantities: theory HOL-Library.Code_Abstract_Nat
13:19:42 Physical_Quantities: theory HOL-Library.Code_Target_Int
13:19:42 Physical_Quantities: theory HOL-Library.Phantom_Type
13:19:42 Physical_Quantities: theory Physical_Quantities.Power_int
13:19:42 Physical_Quantities: theory HOL-Library.Lattice_Algebras
13:19:42 Physical_Quantities: theory HOL-Library.Set_Algebras
13:19:43 Physical_Quantities: theory HOL-Library.Log_Nat
13:19:43 Physical_Quantities: theory HOL-Library.Code_Target_Nat
13:19:43 Physical_Quantities: theory Physical_Quantities.Groups_mult
13:19:43 Physical_Quantities: theory HOL-Library.Code_Target_Numeral
13:19:44 Physical_Quantities: theory HOL-Library.Cardinality
13:19:45 Physical_Quantities: theory HOL-Library.Code_Cardinality
13:19:45 Physical_Quantities: theory Physical_Quantities.Enum_extra
13:19:45 Physical_Quantities: theory Physical_Quantities.ISQ_Dimensions
13:19:49 Physical_Quantities: theory HOL-Library.Interval
13:19:49 Physical_Quantities: theory HOL-Library.Float
13:19:50 Physical_Quantities: theory Physical_Quantities.ISQ_Quantities
13:19:52 Physical_Quantities: theory HOL-Library.Code_Target_Numeral_Float
13:19:52 Physical_Quantities: theory HOL-Library.Interval_Float
13:19:53 Physical_Quantities: theory Physical_Quantities.ISQ_Proof
13:19:53 Physical_Quantities: theory Physical_Quantities.ISQ_Algebra
13:19:54 Physical_Quantities: theory Physical_Quantities.ISQ_Units
13:19:54 Physical_Quantities: theory Physical_Quantities.ISQ_Conversion
13:19:54 Physical_Quantities: theory HOL-Decision_Procs.Approximation_Bounds
13:19:55 Physical_Quantities: theory Physical_Quantities.ISQ
13:19:55 Physical_Quantities: theory Physical_Quantities.SI_Units
13:19:55 Physical_Quantities: theory Physical_Quantities.CGS
13:19:56 Physical_Quantities: theory Physical_Quantities.BIS
13:19:56 Physical_Quantities: theory Physical_Quantities.SI_Constants
13:19:56 Physical_Quantities: theory Physical_Quantities.SI_Prefix
13:19:56 Physical_Quantities: theory Physical_Quantities.SI_Derived
13:19:57 Physical_Quantities: theory Physical_Quantities.SI_Accepted
13:19:57 Physical_Quantities: theory Physical_Quantities.SI_Imperial
13:19:57 Physical_Quantities: theory Physical_Quantities.SI
13:19:57 Physical_Quantities: theory Physical_Quantities.SI_Pretty
13:19:59 Physical_Quantities: theory HOL-Decision_Procs.Approximation
13:20:44 Physical_Quantities: theory Physical_Quantities.SI_Astronomical
13:20:49 Preparing Physical_Quantities/document ...
13:20:54 Finished Physical_Quantities/document (0:00:04 elapsed time)
13:20:54 Preparing Physical_Quantities/outline ...
13:20:58 Finished Physical_Quantities/outline (0:00:04 elapsed time)
13:20:58 Timing Physical_Quantities (8 threads, 64.658s elapsed time, 271.752s cpu time, 4.903s GC time, factor 4.20)
13:20:58 Finished Physical_Quantities (0:01:06 elapsed time, 0:04:36 cpu time, factor 4.13)
13:20:59 Running SATSolverVerification (on hpcisabelle/4) ...
13:21:01 SATSolverVerification: theory SATSolverVerification.MoreList
13:21:01 SATSolverVerification: theory SATSolverVerification.CNF
13:21:01 SATSolverVerification: theory SATSolverVerification.Trail
13:21:03 SATSolverVerification: theory SATSolverVerification.SatSolverVerification
13:21:05 SATSolverVerification: theory SATSolverVerification.KrsticGoel
13:21:05 SATSolverVerification: theory SATSolverVerification.BasicDPLL
13:21:05 SATSolverVerification: theory SATSolverVerification.NieuwenhuisOliverasTinelli
13:21:05 SATSolverVerification: theory SATSolverVerification.SatSolverCode
13:21:08 SATSolverVerification: theory SATSolverVerification.AssertLiteral
13:21:09 SATSolverVerification: theory SATSolverVerification.ConflictAnalysis
13:21:09 SATSolverVerification: theory SATSolverVerification.Decide
13:21:10 SATSolverVerification: theory SATSolverVerification.UnitPropagate
13:21:11 SATSolverVerification: theory SATSolverVerification.Initialization
13:21:11 SATSolverVerification: theory SATSolverVerification.SolveLoop
13:21:12 SATSolverVerification: theory SATSolverVerification.FunctionalImplementation
13:21:40 Preparing SATSolverVerification/document ...
13:22:05 Finished SATSolverVerification/document (0:00:25 elapsed time)
13:22:05 Preparing SATSolverVerification/outline ...
13:22:13 Finished SATSolverVerification/outline (0:00:07 elapsed time)
13:22:13 Timing SATSolverVerification (8 threads, 37.039s elapsed time, 285.996s cpu time, 3.731s GC time, factor 7.72)
13:22:13 Finished SATSolverVerification (0:00:39 elapsed time, 0:04:50 cpu time, factor 7.30)
13:22:13 Running Multirelations_Heterogeneous (on hpcisabelle/5) ...
13:22:15 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Relational_Properties
13:22:16 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Power_Allegories_Properties
13:22:16 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Multirelations_Basics
13:22:19 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Power_Allegories_Multirelations
13:22:19 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Multirelations
13:23:21 Preparing Multirelations_Heterogeneous/document ...
13:23:32 Finished Multirelations_Heterogeneous/document (0:00:11 elapsed time)
13:23:32 Preparing Multirelations_Heterogeneous/outline ...
13:23:38 Finished Multirelations_Heterogeneous/outline (0:00:06 elapsed time)
13:23:38 Timing Multirelations_Heterogeneous (8 threads, 64.066s elapsed time, 308.178s cpu time, 6.208s GC time, factor 4.81)
13:23:38 Finished Multirelations_Heterogeneous (0:01:06 elapsed time, 0:05:14 cpu time, factor 4.73)
13:23:39 Running Prime_Harmonic_Series (on hpcisabelle/6) ...
13:23:41 Prime_Harmonic_Series: theory HOL-Algebra.Congruence
13:23:41 Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes
13:23:41 Prime_Harmonic_Series: theory HOL-Number_Theory.Cong
13:23:41 Prime_Harmonic_Series: theory HOL-Library.Power_By_Squaring
13:23:41 Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers
13:23:41 Prime_Harmonic_Series: theory HOL-Number_Theory.Fib
13:23:43 Prime_Harmonic_Series: theory HOL-Algebra.Order
13:23:43 Prime_Harmonic_Series: theory HOL-Number_Theory.Mod_Exp
13:23:43 Prime_Harmonic_Series: theory HOL-Number_Theory.Totient
13:23:44 Prime_Harmonic_Series: theory HOL-Algebra.Lattice
13:23:46 Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice
13:23:47 Prime_Harmonic_Series: theory HOL-Algebra.Group
13:23:50 Prime_Harmonic_Series: theory HOL-Algebra.Coset
13:23:50 Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct
13:23:51 Prime_Harmonic_Series: theory HOL-Algebra.Ring
13:23:52 Prime_Harmonic_Series: theory HOL-Algebra.Generated_Groups
13:23:54 Prime_Harmonic_Series: theory HOL-Algebra.Elementary_Groups
13:23:55 Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset
13:23:55 Prime_Harmonic_Series: theory HOL-Algebra.Module
13:24:00 Prime_Harmonic_Series: theory HOL-Algebra.Ideal
13:24:03 Prime_Harmonic_Series: theory HOL-Algebra.RingHom
13:24:04 Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly
13:24:18 Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group
13:24:23 Prime_Harmonic_Series: theory HOL-Number_Theory.Residues
13:24:26 Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion
13:24:26 Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington
13:24:26 Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss
13:24:26 Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
13:24:26 Prime_Harmonic_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
13:24:27 Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory
13:24:29 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc
13:24:29 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat
13:24:29 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic
13:24:43 Preparing Prime_Harmonic_Series/document ...
13:24:45 Finished Prime_Harmonic_Series/document (0:00:01 elapsed time)
13:24:45 Preparing Prime_Harmonic_Series/outline ...
13:24:46 Finished Prime_Harmonic_Series/outline (0:00:01 elapsed time)
13:24:46 Timing Prime_Harmonic_Series (8 threads, 59.313s elapsed time, 342.875s cpu time, 10.165s GC time, factor 5.78)
13:24:46 Finished Prime_Harmonic_Series (0:01:02 elapsed time, 0:05:49 cpu time, factor 5.57)
13:24:46 Running HOL-Examples (on hpcisabelle/7) ...
13:24:48 HOL-Examples: theory HOL-Examples.Commands
13:24:48 HOL-Examples: theory HOL-Examples.Cantor
13:24:48 HOL-Examples: theory HOL-Examples.Drinker
13:24:48 HOL-Examples: theory HOL-Examples.Coherent
13:24:48 HOL-Examples: theory HOL-Examples.Groebner_Examples
13:24:48 HOL-Examples: theory HOL-Examples.Iff_Oracle
13:24:48 HOL-Examples: theory HOL-Examples.Induction_Schema
13:24:48 HOL-Examples: theory HOL-Examples.Knaster_Tarski
13:24:48 HOL-Examples: theory HOL-Examples.ML
13:24:48 HOL-Examples: theory HOL-Examples.Peirce
13:24:48 HOL-Examples: theory HOL-Examples.Records
13:24:48 HOL-Examples: theory HOL-Examples.Seq
13:24:48 HOL-Examples: theory HOL-Library.Adhoc_Overloading
13:24:48 HOL-Examples: theory HOL-Library.Cancellation
13:24:48 HOL-Examples: theory HOL-Library.Centered_Division
13:24:48 HOL-Examples: theory HOL-Examples.Gauss_Numbers
13:24:48 HOL-Examples: theory HOL-Library.Monad_Syntax
13:24:48 HOL-Examples: theory HOL-Library.Infinite_Set
13:24:48 HOL-Examples: theory HOL-Examples.Functions
13:24:48 HOL-Examples: theory HOL-Library.Product_Lexorder
13:24:48 HOL-Examples: theory HOL-Library.Rewrite
13:24:49 HOL-Examples: theory HOL-Examples.Adhoc_Overloading_Examples
13:24:49 HOL-Examples: theory HOL-Examples.Rewrite_Examples
13:24:49 HOL-Examples: theory HOL-Library.Multiset
13:24:56 HOL-Examples: theory HOL-Computational_Algebra.Factorial_Ring
13:24:56 HOL-Examples: theory HOL-Library.Multiset_Order
13:24:56 HOL-Examples: theory HOL-Examples.Ackermann
13:25:07 HOL-Examples: theory HOL-Computational_Algebra.Euclidean_Algorithm
13:25:23 HOL-Examples: theory HOL-Computational_Algebra.Primes
13:25:32 HOL-Examples: theory HOL-Examples.Sqrt
13:25:37 Preparing HOL-Examples/document ...
13:25:41 Finished HOL-Examples/document (0:00:04 elapsed time)
13:25:41 Preparing HOL-Examples/outline ...
13:25:45 Finished HOL-Examples/outline (0:00:03 elapsed time)
13:25:45 Timing HOL-Examples (8 threads, 47.492s elapsed time, 287.409s cpu time, 9.070s GC time, factor 6.05)
13:25:45 Finished HOL-Examples (0:00:49 elapsed time, 0:04:54 cpu time, factor 5.89)
13:25:46 Running Real_Time_Deque (on hpcisabelle/0) ...
13:25:47 Real_Time_Deque: theory Real_Time_Deque.Deque
13:25:47 Real_Time_Deque: theory Real_Time_Deque.RTD_Util
13:25:47 Real_Time_Deque: theory Real_Time_Deque.Type_Classes
13:25:47 Real_Time_Deque: theory Real_Time_Deque.Stack
13:25:48 Real_Time_Deque: theory Real_Time_Deque.Idle
13:25:48 Real_Time_Deque: theory Real_Time_Deque.Stack_Aux
13:25:48 Real_Time_Deque: theory Real_Time_Deque.Current
13:25:49 Real_Time_Deque: theory Real_Time_Deque.Stack_Proof
13:25:49 Real_Time_Deque: theory Real_Time_Deque.Idle_Aux
13:25:50 Real_Time_Deque: theory Real_Time_Deque.Common
13:25:50 Real_Time_Deque: theory Real_Time_Deque.Current_Aux
13:25:50 Real_Time_Deque: theory Real_Time_Deque.Idle_Proof
13:25:50 Real_Time_Deque: theory Real_Time_Deque.Current_Proof
13:25:51 Real_Time_Deque: theory Real_Time_Deque.Big
13:25:51 Real_Time_Deque: theory Real_Time_Deque.Small
13:25:51 Real_Time_Deque: theory Real_Time_Deque.Common_Aux
13:25:53 Real_Time_Deque: theory Real_Time_Deque.Common_Proof
13:25:53 Real_Time_Deque: theory Real_Time_Deque.Big_Aux
13:25:53 Real_Time_Deque: theory Real_Time_Deque.States
13:25:53 Real_Time_Deque: theory Real_Time_Deque.Small_Aux
13:25:54 Real_Time_Deque: theory Real_Time_Deque.Big_Proof
13:25:54 Real_Time_Deque: theory Real_Time_Deque.Small_Proof
13:25:55 Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque
13:25:55 Real_Time_Deque: theory Real_Time_Deque.States_Aux
13:25:57 Real_Time_Deque: theory Real_Time_Deque.States_Proof
13:26:00 Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Aux
13:26:00 Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Dequeue_Proof
13:26:01 Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Enqueue_Proof
13:26:01 Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Proof
13:26:55 Preparing Real_Time_Deque/document ...
13:27:00 Finished Real_Time_Deque/document (0:00:05 elapsed time)
13:27:00 Preparing Real_Time_Deque/outline ...
13:27:04 Finished Real_Time_Deque/outline (0:00:03 elapsed time)
13:27:04 Timing Real_Time_Deque (8 threads, 67.219s elapsed time, 350.410s cpu time, 3.506s GC time, factor 5.21)
13:27:04 Finished Real_Time_Deque (0:01:09 elapsed time, 0:05:53 cpu time, factor 5.12)
13:27:04 Running Propositional_Proof_Systems (on hpcisabelle/1) ...
13:27:06 Propositional_Proof_Systems: theory HOL-Library.Case_Converter
13:27:06 Propositional_Proof_Systems: theory HOL-Library.Cancellation
13:27:06 Propositional_Proof_Systems: theory HOL-Library.List_Lexorder
13:27:06 Propositional_Proof_Systems: theory HOL-Library.Nat_Bijection
13:27:06 Propositional_Proof_Systems: theory HOL-Library.Old_Datatype
13:27:06 Propositional_Proof_Systems: theory HOL-Library.While_Combinator
13:27:07 Propositional_Proof_Systems: theory HOL-Library.Simps_Case_Conv
13:27:07 Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF
13:27:07 Propositional_Proof_Systems: theory HOL-Library.Countable
13:27:07 Propositional_Proof_Systems: theory HOL-Library.Multiset
13:27:08 Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Sema
13:27:08 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution
13:27:08 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl
13:27:09 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Formulas
13:27:12 Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Formulas
13:27:12 Propositional_Proof_Systems: theory Propositional_Proof_Systems.HC
13:27:12 Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniFormulas
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Sema
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Substitution
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_FiniteAssms
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Compactness
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Consistency
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniFormulas_Sema
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Sound
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Substitution_Sema
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.NDHC
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Sema_Craig
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_Truthtable
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_Truthtable_Compact
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Compactness_Consistency
13:27:13 Propositional_Proof_Systems: theory Propositional_Proof_Systems.HC_Compl_Consistency
13:27:14 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SCND
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Cut
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC_Craig
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC_HC
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_To_Formula
13:27:15 Propositional_Proof_Systems: theory Propositional_Proof_Systems.HCSC
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.LSC
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Depth
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.HCSCND
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Formulas_Sema
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Sema
13:27:16 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Tseytin
13:27:17 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Tseytin_Sema
13:27:17 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Sound
13:27:17 Propositional_Proof_Systems: theory Propositional_Proof_Systems.LSC_Resolution
13:27:18 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_Consistency
13:27:19 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Gentzen
13:27:19 Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_SC
13:27:19 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_SC_Full
13:27:19 Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_SC_Small
13:27:19 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Compl_Consistency
13:27:20 Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Depth_Limit
13:27:57 Preparing Propositional_Proof_Systems/document ...
13:28:11 Finished Propositional_Proof_Systems/document (0:00:13 elapsed time)
13:28:11 Preparing Propositional_Proof_Systems/outline ...
13:28:19 Finished Propositional_Proof_Systems/outline (0:00:08 elapsed time)
13:28:19 Timing Propositional_Proof_Systems (8 threads, 49.386s elapsed time, 315.095s cpu time, 14.112s GC time, factor 6.38)
13:28:19 Finished Propositional_Proof_Systems (0:00:51 elapsed time, 0:05:20 cpu time, factor 6.20)
13:28:19 Running Hypergraph_Colourings (on hpcisabelle/2) ...
13:28:22 Hypergraph_Colourings: theory Graph_Theory.Rtrancl_On
13:28:22 Hypergraph_Colourings: theory HOL-Eisbach.Eisbach
13:28:22 Hypergraph_Colourings: theory Card_Number_Partitions.Additions_to_Main
13:28:22 Hypergraph_Colourings: theory Card_Multisets.Card_Multisets
13:28:22 Hypergraph_Colourings: theory HOL-Combinatorics.Stirling
13:28:22 Hypergraph_Colourings: theory HOL-Library.Multiset_Order
13:28:22 Hypergraph_Colourings: theory Card_Partitions.Set_Partition
13:28:22 Hypergraph_Colourings: theory HOL-Library.Code_Abstract_Nat
13:28:22 Hypergraph_Colourings: theory Card_Number_Partitions.Number_Partition
13:28:22 Hypergraph_Colourings: theory HOL-Library.Code_Target_Nat
13:28:22 Hypergraph_Colourings: theory HOL-ex.Birthday_Paradox
13:28:23 Hypergraph_Colourings: theory Girth_Chromatic.Girth_Chromatic_Misc
13:28:23 Hypergraph_Colourings: theory Card_Number_Partitions.Card_Number_Partitions
13:28:23 Hypergraph_Colourings: theory Graph_Theory.Stuff
13:28:23 Hypergraph_Colourings: theory Undirected_Graph_Theory.Undirected_Graph_Basics
13:28:23 Hypergraph_Colourings: theory Graph_Theory.Digraph
13:28:23 Hypergraph_Colourings: theory Nested_Multisets_Ordinals.Multiset_More
13:28:24 Hypergraph_Colourings: theory Card_Partitions.Injectivity_Solver
13:28:24 Hypergraph_Colourings: theory Card_Partitions.Card_Partitions
13:28:24 Hypergraph_Colourings: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
13:28:25 Hypergraph_Colourings: theory Design_Theory.Multisets_Extras
13:28:25 Hypergraph_Colourings: theory Bell_Numbers_Spivey.Bell_Numbers
13:28:25 Hypergraph_Colourings: theory Lovasz_Local.PiE_Rel_Extras
13:28:25 Hypergraph_Colourings: theory Lovasz_Local.Prob_Events_Extras
13:28:25 Hypergraph_Colourings: theory Graph_Theory.Arc_Walk
13:28:25 Hypergraph_Colourings: theory Graph_Theory.Bidirected_Digraph
13:28:25 Hypergraph_Colourings: theory Twelvefold_Way.Preliminaries
13:28:26 Hypergraph_Colourings: theory Design_Theory.Design_Basics
13:28:26 Hypergraph_Colourings: theory Fishers_Inequality.Set_Multiset_Extras
13:28:26 Hypergraph_Colourings: theory Lovasz_Local.Cond_Prob_Extensions
13:28:26 Hypergraph_Colourings: theory Twelvefold_Way.Twelvefold_Way_Core
13:28:27 Hypergraph_Colourings: theory Design_Theory.Design_Operations
13:28:27 Hypergraph_Colourings: theory Graph_Theory.Pair_Digraph
13:28:27 Hypergraph_Colourings: theory Lovasz_Local.Indep_Events
13:28:28 Hypergraph_Colourings: theory Undirected_Graph_Theory.Undirected_Graph_Walks
13:28:28 Hypergraph_Colourings: theory Lovasz_Local.Basic_Method
13:28:28 Hypergraph_Colourings: theory Design_Theory.Block_Designs
13:28:29 Hypergraph_Colourings: theory Design_Theory.Sub_Designs
13:28:29 Hypergraph_Colourings: theory Undirected_Graph_Theory.Bipartite_Graphs
13:28:32 Hypergraph_Colourings: theory Design_Theory.BIBD
13:28:34 Hypergraph_Colourings: theory Fishers_Inequality.Design_Extras
13:28:34 Hypergraph_Colourings: theory Lovasz_Local.Digraph_Extensions
13:28:35 Hypergraph_Colourings: theory Lovasz_Local.Lovasz_Local_Lemma
13:28:35 Hypergraph_Colourings: theory Hypergraph_Basics.Hypergraph
13:28:37 Hypergraph_Colourings: theory Hypergraph_Basics.Hypergraph_Variations
13:28:41 Hypergraph_Colourings: theory Hypergraph_Colourings.Hypergraph_Colourings
13:28:43 Hypergraph_Colourings: theory Hypergraph_Colourings.Basic_Bounds_Application
13:28:52 Hypergraph_Colourings: theory Hypergraph_Colourings.LLL_Applications
13:28:54 Hypergraph_Colourings: theory Hypergraph_Colourings.Hypergraph_Colourings_Root
13:29:18 Preparing Hypergraph_Colourings/document ...
13:29:23 Finished Hypergraph_Colourings/document (0:00:04 elapsed time)
13:29:23 Preparing Hypergraph_Colourings/outline ...
13:29:26 Finished Hypergraph_Colourings/outline (0:00:03 elapsed time)
13:29:26 Timing Hypergraph_Colourings (8 threads, 53.492s elapsed time, 391.038s cpu time, 10.009s GC time, factor 7.31)
13:29:26 Finished Hypergraph_Colourings (0:00:57 elapsed time, 0:06:37 cpu time, factor 6.97)
13:29:26 Running Simplicial_complexes_and_boolean_functions (on hpcisabelle/3) ...
13:29:29 Simplicial_complexes_and_boolean_functions: theory HOL-Computational_Algebra.Factorial_Ring
13:29:29 Simplicial_complexes_and_boolean_functions: theory HOL-Combinatorics.Transposition
13:29:29 Simplicial_complexes_and_boolean_functions: theory HOL-Library.FuncSet
13:29:29 Simplicial_complexes_and_boolean_functions: theory HOL-Library.Complex_Order
13:29:29 Simplicial_complexes_and_boolean_functions: theory ROBDD.Bool_Func
13:29:29 Simplicial_complexes_and_boolean_functions: theory ROBDD.Pointer_Map
13:29:29 Simplicial_complexes_and_boolean_functions: theory ROBDD.Option_Helpers
13:29:29 Simplicial_complexes_and_boolean_functions: theory ROBDD.Array_List
13:29:29 Simplicial_complexes_and_boolean_functions: theory Jordan_Normal_Form.Conjugate
13:29:29 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.ListLexorder
13:29:29 Simplicial_complexes_and_boolean_functions: theory ROBDD.BDT
13:29:30 Simplicial_complexes_and_boolean_functions: theory ROBDD.Pointer_Map_Impl
13:29:30 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Congruence
13:29:30 Simplicial_complexes_and_boolean_functions: theory HOL-Library.Disjoint_Sets
13:29:31 Simplicial_complexes_and_boolean_functions: theory HOL-Combinatorics.Permutations
13:29:31 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Order
13:29:32 Simplicial_complexes_and_boolean_functions: theory Jordan_Normal_Form.Missing_Misc
13:29:33 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Lattice
13:29:33 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.MkIfex
13:29:33 Simplicial_complexes_and_boolean_functions: theory ROBDD.Abstract_Impl
13:29:34 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Complete_Lattice
13:29:35 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Group
13:29:37 Simplicial_complexes_and_boolean_functions: theory ROBDD.Middle_Impl
13:29:38 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.FiniteProduct
13:29:39 Simplicial_complexes_and_boolean_functions: theory ROBDD.Conc_Impl
13:29:39 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Ring
13:29:42 Simplicial_complexes_and_boolean_functions: theory ROBDD.Level_Collapse
13:29:42 Simplicial_complexes_and_boolean_functions: theory Polynomial_Interpolation.Ring_Hom
13:29:44 Simplicial_complexes_and_boolean_functions: theory HOL-Algebra.Module
13:29:44 Simplicial_complexes_and_boolean_functions: theory Jordan_Normal_Form.Missing_Ring
13:29:51 Simplicial_complexes_and_boolean_functions: theory Jordan_Normal_Form.Matrix
13:29:57 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.Boolean_functions
13:29:57 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.Simplicial_complex
13:29:58 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.Bij_betw_simplicial_complex_bool_func
13:29:58 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.Binary_operations
13:29:58 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.Evasive
13:29:59 Simplicial_complexes_and_boolean_functions: theory Simplicial_complexes_and_boolean_functions.BDD
13:30:19 Preparing Simplicial_complexes_and_boolean_functions/document ...
13:30:25 Finished Simplicial_complexes_and_boolean_functions/document (0:00:06 elapsed time)
13:30:25 Preparing Simplicial_complexes_and_boolean_functions/outline ...
13:30:30 Finished Simplicial_complexes_and_boolean_functions/outline (0:00:04 elapsed time)
13:30:30 Timing Simplicial_complexes_and_boolean_functions (8 threads, 47.833s elapsed time, 343.882s cpu time, 9.039s GC time, factor 7.19)
13:30:30 Finished Simplicial_complexes_and_boolean_functions (0:00:51 elapsed time, 0:05:50 cpu time, factor 6.82)
13:30:30 Building HOL-CSPM (on hpcisabelle/4) ...
13:30:32 HOL-CSPM: theory HOL-CSPM.Introduction
13:30:32 HOL-CSPM: theory HOL-Library.LaTeXsugar
13:30:32 HOL-CSPM: theory HOL-CSPM.Patch
13:30:32 HOL-CSPM: theory HOL-Library.Cancellation
13:30:32 HOL-CSPM: theory HOL-CSPM.MultiSeq
13:30:33 HOL-CSPM: theory HOL-Library.Multiset
13:30:40 HOL-CSPM: theory HOL-CSPM.PreliminaryWork
13:30:40 HOL-CSPM: theory HOL-CSPM.MultiDet
13:30:40 HOL-CSPM: theory HOL-CSPM.MultiNdet
13:30:40 HOL-CSPM: theory HOL-CSPM.MultiSync
13:30:41 HOL-CSPM: theory HOL-CSPM.GlobalNdet
13:30:41 HOL-CSPM: theory HOL-CSPM.CSPM
13:30:42 HOL-CSPM: theory HOL-CSPM.DeadlockResults
13:30:43 HOL-CSPM: theory HOL-CSPM.Conclusion
13:30:43 HOL-CSPM: theory HOL-CSPM.DiningPhilosophers
13:30:43 HOL-CSPM: theory HOL-CSPM.EventsProperties
13:30:43 HOL-CSPM: theory HOL-CSPM.POTS
13:30:51 Build was aborted
13:30:51 Aborted by Administrative User
13:35:15 Started calculate disk usage of build
13:35:15 Finished Calculation of disk usage of build in 0 seconds
13:35:15 Started calculate disk usage of workspace
13:35:17 Finished Calculation of disk usage of workspace in  1 second
13:35:17 No emails were triggered.
13:35:17 Finished: ABORTED