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