Started by user nipkow
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-all] $ hg update --clean --rev default
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-all] $ hg log --rev . --template {node}
[isabelle-all] $ hg log --rev . --template {rev}
[isabelle-all] $ hg log --rev 613ac8c77a84212408cba7d5bc65238ea3ab2f34 --template exists\n
exists
[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
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 153470351ff5859eed0de7504dc84827fd779a22 --template exists\n
exists
[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
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins4869908564295098969.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building Demo (/media/data/jenkins/workspace/isabelle-all/src/Tools/Demo/lib/demo.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Hinweis: Einige Eingabedateien verwenden nicht geprüfte oder unsichere Vorgänge.
Hinweis: Wiederholen Sie die Kompilierung mit -Xlint:unchecked, um Details zu erhalten.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
+ bin/isabelle ghc_setup
Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
consider using: stack ghc, stack ghci, stack runghc, or stack exec.
The Glorious Glasgow Haskell Compilation System, version 9.6.4
+ bin/isabelle go_setup
Component directory "/media/data/jenkins/.isabelle/contrib/go-1.22.1"
### Platform x86_64-linux already installed
+ bin/isabelle ci_build all

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64_32-linux"
ML_SYSTEM="polyml-5.9.1"
ML_OPTIONS="-H 4000 --maxheap 16G"
Cluster(cluster.default,true)

=== BUILD ===

Build started at Wed, 12 Jun 2024 11:39:35 +0200
Isabelle id 613ac8c77a84
AFP id 153470351ff5

=== LOG ===

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