Console Output

20:54:51 Started by an SCM change
20:54:51 Running as SYSTEM
20:54:51 [EnvInject] - Loading node environment variables.
20:54:51 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all
20:54:51 [isabelle-all] $ hg showconfig paths.default
20:54:51 [isabelle-all] $ hg pull --rev default
20:54:52 pulling from http://isabelle.in.tum.de/repos/isabelle/
20:54:52 no changes found
20:54:52 [isabelle-all] $ hg update --clean --rev default
20:54:52 7 files updated, 0 files merged, 1 files removed, 0 files unresolved
20:54:52 [isabelle-all] $ hg log --rev . --template {node}
20:54:52 [isabelle-all] $ hg log --rev . --template {rev}
20:54:52 [isabelle-all] $ hg log --rev 43a43b182a81f06f274c59b1157ffaeef20722e4 --template exists\n
20:54:52 exists
20:54:52 [isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(43a43b182a81f06f274c59b1157ffaeef20722e4)" --encoding UTF-8 --encodingmode replace
20:54:52 [afp] $ hg showconfig paths.default
20:54:52 [afp] $ hg pull --rev default
20:54:56 pulling from https://foss.heptapod.net/isa-afp/afp-devel/
20:54:56 no changes found
20:54:56 [afp] $ hg update --clean --rev default
20:54:56 556 files updated, 0 files merged, 0 files removed, 0 files unresolved
20:54:56 [afp] $ hg --config extensions.purge= clean --all
20:54:57 [afp] $ hg log --rev . --template {node}
20:54:57 [afp] $ hg log --rev . --template {rev}
20:54:57 [afp] $ hg log --rev cac1c67360f3f2b4c7796180290a98fbd7699dee --template exists\n
20:54:57 exists
20:54:57 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(cac1c67360f3f2b4c7796180290a98fbd7699dee)" --encoding UTF-8 --encodingmode replace
20:54:57 No emails were triggered.
20:54:57 
[isabelle-all] $ /bin/sh -xe /tmp/jenkins6940002665651543264.sh

20:54:57 + Admin/jenkins/run_build all
20:54:57 + set -e
20:54:57 + PROFILE=all
20:54:57 + shift
20:54:57 + bin/isabelle components -a
20:54:57 + bin/isabelle jedit -bf
20:54:57 ### Building Isabelle/Scala ...
20:55:26 ### Building Isabelle/jEdit ...
20:55:43 + bin/isabelle ocaml_setup
20:55:43 # Run eval $(opam env) to update the current shell environment
20:55:43 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
20:55:43        opam update
20:55:43 
20:55:43 [NOTE] Package zarith is already installed (current version is 1.7).
20:55:44 + bin/isabelle ghc_setup
20:55:45 stack will use a sandboxed GHC it installed
20:55:45 For more information on paths, see 'stack path' and 'stack exec env'
20:55:45 To use this GHC and packages outside of a project, consider using:
20:55:45 stack ghc, stack ghci, stack runghc, or stack exec
20:55:45 The Glorious Glasgow Haskell Compilation System, version 8.6.4
20:55:45 + bin/isabelle ci_build_all
20:55:51 
20:55:51 === CONFIGURATION ===
20:55:51 
20:55:51 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
20:55:51 ISABELLE_BUILD_OPTIONS=""
20:55:51 
20:55:51 ML_PLATFORM="x86_64_32-linux"
20:55:51 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8.1/x86_64_32-linux"
20:55:51 ML_SYSTEM="polyml-5.8.1"
20:55:51 ML_OPTIONS="-H 4000 --maxheap 8G"
20:55:52 jobs = 10, threads = 4, numa = false
20:55:52 
20:55:52 === BUILD ===
20:55:52 
20:55:52 Build started at Wed, 5 Aug 2020 18:55:51 GMT
20:55:52 Isabelle id a36db1c8238e
20:55:52 AFP id 3e79743d7844
20:55:52 
20:55:52 === LOG ===
20:55:52 
20:55:53 Session Pure/Pure
20:55:53 Session CTT/CTT
20:55:53 Session Cube/Cube
20:55:53 Session FOL/FOL
20:55:53 Session CCL/CCL
20:55:53 Session FOL/FOL-ex
20:55:53 Session FOLP/FOLP
20:55:53 Session FOLP/FOLP-ex
20:55:53 Session Tools/Haskell
20:55:53 Session Doc/Intro (doc)
20:55:54 Session LCF/LCF
20:55:54 Session Doc/Logics (doc)
20:55:54 Session Doc/Nitpick (doc)
20:55:54 Session Pure/Pure-Examples
20:55:54 Session Tools/SML
20:55:54 Session Sequents/Sequents
20:55:54 Session Doc/Sledgehammer (doc)
20:55:54 Session Tools/Spec_Check
20:55:54 Session Tools/Tools
20:55:54 Session HOL/HOL (main)
20:55:55 Session AFP/AVL-Trees (AFP)
20:55:55 Session AFP/AWN (AFP)
20:55:55 Session AFP/Abortable_Linearizable_Modules (AFP)
20:55:55 Session AFP/Abstract-Hoare-Logics (AFP)
20:55:55 Session AFP/AnselmGod (AFP)
20:55:55 Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
20:55:55 Session AFP/Attack_Trees (AFP)
20:55:55 Session AFP/AxiomaticCategoryTheory (AFP)
20:55:55 Session AFP/BinarySearchTree (AFP)
20:55:55 Session AFP/Binomial-Queues (AFP)
20:55:55 Session AFP/Bondy (AFP)
20:55:55 Session AFP/Bounded_Deducibility_Security (AFP)
20:55:55 Session AFP/BytecodeLogicJmlTypes (AFP)
20:55:55 Session AFP/C2KA_DistributedSystems (AFP)
20:55:55 Session AFP/CISC-Kernel (AFP)
20:55:55 Session AFP/CYK (AFP)
20:55:55 Session AFP/Cauchy (AFP)
20:55:55 Session AFP/Sqrt_Babylonian (AFP)
20:55:55 Session Doc/Classes (doc)
20:55:55 Session AFP/ClockSynchInst (AFP)
20:55:55 Session AFP/Compiling-Exceptions-Correctly (AFP)
20:55:55 Session AFP/Complete_Non_Orders (AFP)
20:55:55 Session AFP/ComponentDependencies (AFP)
20:55:55 Session AFP/Concurrent_Revisions (AFP)
20:55:55 Session AFP/Constructor_Funs (AFP)
20:55:55 Session AFP/CryptoBasedCompositionalProperties (AFP)
20:55:55 Session AFP/DPT-SAT-Solver (AFP)
20:55:55 Session AFP/Depth-First-Search (AFP)
20:55:55 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
20:55:55 Session AFP/DiskPaxos (AFP)
20:55:55 Session AFP/Example-Submission (AFP)
20:55:55 Session AFP/FFT (AFP)
20:55:55 Session AFP/FLP (AFP)
20:55:55 Session AFP/FeatherweightJava (AFP)
20:55:55 Session AFP/Featherweight_OCL (AFP)
20:55:56 Session AFP/FileRefinement (AFP)
20:55:56 Session AFP/FocusStreamsCaseStudies (AFP)
20:55:56 Session AFP/Free-Boolean-Algebra (AFP)
20:55:56 Session AFP/FunWithFunctions (AFP)
20:55:56 Session AFP/FunWithTilings (AFP)
20:55:56 Session Doc/Functions (doc)
20:55:56 Session AFP/GPU_Kernel_PL (AFP)
20:55:56 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
20:55:56 Session AFP/GenClock (AFP)
20:55:56 Session AFP/General-Triangle (AFP)
20:55:56 Session AFP/Generic_Deriving (AFP)
20:55:56 Session AFP/GewirthPGCProof (AFP)
20:55:56 Session AFP/GoedelGod (AFP)
20:55:56 Session AFP/Goodstein_Lambda (AFP)
20:55:56 Session HOL/HOL-Cardinals (timing)
20:55:56 Session AFP/Binding_Syntax_Theory (AFP)
20:55:56 Session AFP/Ordinals_and_Cardinals (AFP)
20:55:56 Session HOL/HOL-Hoare
20:55:56 Session HOL/HOL-Hoare_Parallel (timing)
20:55:56 Session HOL/HOL-IMPP
20:55:56 Session HOL/HOL-IOA
20:55:56 Session HOL/HOL-Import
20:55:56 Session HOL/HOL-Lattice
20:55:56 Session HOL/HOL-Library (main timing)
20:55:56 Session AFP/ADS_Functor (AFP)
20:55:56 Session AFP/Approximation_Algorithms (AFP)
20:55:57 Session AFP/ArrowImpossibilityGS (AFP)
20:55:57 Session AFP/Auto2_HOL (AFP)
20:55:57 Session AFP/BNF_CC (AFP)
20:55:57 Session AFP/BNF_Operations (AFP)
20:55:57 Session AFP/Binomial-Heaps (AFP)
20:55:57 Session AFP/Boolean_Expression_Checkers (AFP)
20:55:57 Session AFP/Buildings (AFP)
20:55:57 Session AFP/CRDT (AFP)
20:55:57 Session AFP/IMAP-CRDT (AFP)
20:55:57 Session AFP/Card_Multisets (AFP)
20:55:57 Session AFP/Card_Number_Partitions (AFP)
20:55:57 Session AFP/Category (AFP)
20:55:57 Session Doc/Codegen (doc)
20:55:57 Session AFP/CofGroups (AFP)
20:55:57 Session AFP/Completeness (AFP)
20:55:58 Session AFP/ConcurrentIMP (AFP)
20:55:58 Session AFP/Concurrent_Ref_Alg (AFP)
20:55:58 Session AFP/CoreC++ (AFP)
20:55:58 Session AFP/Core_DOM (AFP)
20:55:58 Session Doc/Datatypes (doc)
20:55:58 Session Doc/Corec (doc)
20:55:58 Session AFP/Decl_Sem_Fun_PL (AFP)
20:55:58 Session AFP/Derangements (AFP)
20:55:58 Session AFP/Discrete_Summation (AFP)
20:55:58 Session AFP/Efficient-Mergesort (AFP)
20:55:58 Session AFP/Encodability_Process_Calculi (AFP)
20:55:58 Session AFP/Epistemic_Logic (AFP)
20:55:58 Session AFP/Euler_Partition (AFP)
20:55:59 Session AFP/FOL-Fitting (AFP)
20:55:59 Session AFP/FOL_Seq_Calc1 (AFP)
20:55:59 Session AFP/FOL_Harrison (AFP)
20:55:59 Session AFP/Factored_Transition_System_Bounding (AFP)
20:55:59 Session AFP/FinFun (AFP)
20:55:59 Session AFP/Finger-Trees (AFP)
20:55:59 Session AFP/Generalized_Counting_Sort (AFP)
20:55:59 Session AFP/Graph_Saturation (AFP)
20:55:59 Session AFP/Graph_Theory (AFP)
20:55:59 Session AFP/ShortestPath (AFP)
20:55:59 Session AFP/Group-Ring-Module (AFP)
20:55:59 Session AFP/Valuation (AFP)
20:55:59 Session HOL/HOL-Auth (timing)
20:55:59 Session HOL/HOL-UNITY (timing)
20:56:00 Session HOL/HOL-Bali (timing)
20:56:00 Session HOL/HOL-Computational_Algebra (main timing)
20:56:00 Session AFP/Descartes_Sign_Rule (AFP)
20:56:00 Session HOL/HOL-Algebra (main timing)
20:56:00 Session HOL/HOL-Decision_Procs (timing)
20:56:00 Session HOL/HOL-Quotient_Examples (timing)
20:56:00 Session AFP/Localization_Ring (AFP)
20:56:00 Session AFP/Orbit_Stabiliser (AFP)
20:56:00 Session AFP/Perfect-Number-Thm (AFP)
20:56:00 Session AFP/Secondary_Sylow (AFP)
20:56:00 Session AFP/Jordan_Hoelder (AFP)
20:56:00 Session AFP/VectorSpace (AFP)
20:56:01 Session HOL/HOL-Analysis (main timing)
20:56:01 Session AFP/Cayley_Hamilton (AFP)
20:56:01 Session AFP/Coinductive (AFP)
20:56:01 Session AFP/DynamicArchitectures (AFP)
20:56:01 Session AFP/Architectural_Design_Patterns (AFP)
20:56:01 Session AFP/Lazy-Lists-II (AFP)
20:56:01 Session AFP/Stream_Fusion_Code (AFP)
20:56:01 Session AFP/Topology (AFP)
20:56:01 Session AFP/Complex_Geometry (AFP)
20:56:02 Session AFP/Poincare_Disc (AFP)
20:56:02 Session AFP/Differential_Game_Logic (AFP)
20:56:02 Session AFP/First_Welfare_Theorem (AFP)
20:56:02 Session AFP/Green (AFP)
20:56:02 Session HOL/HOL-Analysis-ex
20:56:02 Session HOL/HOL-Complex_Analysis (main timing)
20:56:02 Session AFP/Cartan_FP (AFP)
20:56:02 Session HOL/HOL-Eisbach
20:56:02 Session AFP/Allen_Calculus (AFP)
20:56:02 Session AFP/Card_Partitions (AFP)
20:56:02 Session AFP/Bell_Numbers_Spivey (AFP)
20:56:02 Session AFP/Card_Equiv_Relations (AFP)
20:56:02 Session AFP/Falling_Factorial_Sum (AFP)
20:56:02 Session AFP/Case_Labeling (AFP)
20:56:02 Session AFP/Clean (AFP)
20:56:02 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
20:56:02 Session AFP/Dependent_SIFUM_Refinement (AFP)
20:56:02 Session Doc/Eisbach (doc)
20:56:02 Session HOL/HOL-Hahn_Banach
20:56:02 Session HOL/HOL-Homology (timing)
20:56:03 Session HOL/HOL-Probability (main timing)
20:56:03 Session AFP/Buffons_Needle (AFP)
20:56:03 Session AFP/Density_Compiler (AFP)
20:56:03 Session AFP/DiscretePricing (AFP)
20:56:03 Session AFP/Ergodic_Theory (AFP)
20:56:03 Session AFP/Gromov_Hyperbolicity (AFP)
20:56:03 Session AFP/Fisher_Yates (AFP)
20:56:03 Session AFP/Girth_Chromatic (AFP)
20:56:03 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
20:56:03 Session HOL/HOL-Probability-ex (timing)
20:56:03 Session AFP/Lp (AFP)
20:56:03 Session AFP/Markov_Models (AFP)
20:56:03 Session AFP/Monad_Normalisation (AFP)
20:56:03 Session AFP/Monomorphic_Monad (AFP)
20:56:04 Session AFP/Neumann_Morgenstern_Utility (AFP)
20:56:04 Session AFP/Probabilistic_Noninterference (AFP)
20:56:04 Session AFP/Probabilistic_System_Zoo (AFP)
20:56:04 Session AFP/Skip_Lists (AFP)
20:56:04 Session AFP/Source_Coding_Theorem (AFP)
20:56:04 Session AFP/Irrationality_J_Hancl (AFP)
20:56:04 Session AFP/Kuratowski_Closure_Complement (AFP)
20:56:04 Session AFP/Laplace_Transform (AFP)
20:56:04 Session AFP/Lower_Semicontinuous (AFP)
20:56:04 Session AFP/Minkowskis_Theorem (AFP)
20:56:04 Session AFP/Octonions (AFP)
20:56:04 Session AFP/Ptolemys_Theorem (AFP)
20:56:04 Session AFP/Quaternions (AFP)
20:56:04 Session AFP/Rank_Nullity_Theorem (AFP)
20:56:04 Session AFP/Gauss_Jordan (AFP)
20:56:04 Session AFP/Echelon_Form (AFP)
20:56:04 Session AFP/Hermite (AFP)
20:56:04 Session AFP/Tarskis_Geometry (AFP)
20:56:04 Session AFP/Triangle (AFP)
20:56:04 Session AFP/Chord_Segments (AFP)
20:56:04 Session AFP/Stewart_Apollonius (AFP)
20:56:04 Session AFP/pGCL (AFP)
20:56:04 Session HOL/HOL-Isar_Examples
20:56:04 Session HOL/HOL-Nonstandard_Analysis (timing)
20:56:05 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
20:56:05 Session HOL/HOL-Number_Theory (main timing)
20:56:05 Session AFP/Arith_Prog_Rel_Primes (AFP)
20:56:05 Session AFP/Bernoulli (AFP)
20:56:05 Session AFP/E_Transcendental (AFP)
20:56:05 Session AFP/Elliptic_Curves_Group_Law (AFP)
20:56:05 Session AFP/Fermat3_4 (AFP)
20:56:05 Session HOL/HOL-Data_Structures (timing)
20:56:05 Session HOL/HOL-ex (timing)
20:56:06 Session AFP/Automatic_Refinement (AFP)
20:56:06 Session AFP/Lehmer (AFP)
20:56:06 Session AFP/Pratt_Certificate (AFP)
20:56:06 Session AFP/Bertrands_Postulate (AFP)
20:56:06 Session AFP/Prime_Harmonic_Series (AFP)
20:56:06 Session AFP/RSAPSS (AFP)
20:56:06 Session AFP/SumSquares (AFP)
20:56:06 Session AFP/Liouville_Numbers (AFP)
20:56:06 Session AFP/Lucas_Theorem (AFP)
20:56:06 Session AFP/Mason_Stothers (AFP)
20:56:06 Session AFP/Polynomial_Interpolation (AFP)
20:56:06 Session AFP/Probabilistic_Prime_Tests (AFP)
20:56:07 Session AFP/Rep_Fin_Groups (AFP)
20:56:07 Session AFP/Sturm_Sequences (AFP)
20:56:07 Session AFP/Safe_Distance (AFP)
20:56:07 Session AFP/Special_Function_Bounds (AFP)
20:56:07 Session AFP/Sturm_Tarski (AFP)
20:56:07 Session AFP/Budan_Fourier (AFP)
20:56:07 Session AFP/Winding_Number_Eval (AFP)
20:56:07 Session AFP/Count_Complex_Roots (AFP)
20:56:07 Session HOL/HOL-Corec_Examples (timing)
20:56:07 Session HOL/HOL-Datatype_Examples (timing)
20:56:07 Session HOL/HOL-Examples
20:56:07 Session HOL/HOL-IMP (timing)
20:56:07 Session AFP/Abs_Int_ITP2012 (AFP)
20:56:07 Session AFP/Relational-Incorrectness-Logic (AFP)
20:56:07 Session HOL/HOL-Imperative_HOL (timing)
20:56:08 Session AFP/Auto2_Imperative_HOL (AFP)
20:56:08 Session AFP/Imperative_Insertion_Sort (AFP)
20:56:08 Session HOL/HOL-Induct
20:56:08 Session HOL/HOL-Metis_Examples (timing)
20:56:08 Session HOL/HOL-Nitpick_Examples
20:56:08 Session HOL/HOL-Proofs (timing)
20:56:08 Session HOL/HOL-Proofs-Extraction (timing)
20:56:09 Session HOL/HOL-Proofs-ex
20:56:09 Session HOL/HOL-Proofs-Lambda (timing)
20:56:09 Session AFP/Applicative_Lifting (AFP)
20:56:09 Session AFP/Free-Groups (AFP)
20:56:09 Session AFP/Stern_Brocot (AFP)
20:56:09 Session AFP/HereditarilyFinite (AFP)
20:56:09 Session AFP/Category3 (AFP)
20:56:09 Session AFP/MonoidalCategory (AFP)
20:56:09 Session AFP/HyperCTL (AFP)
20:56:09 Session AFP/Integration (AFP)
20:56:09 Session AFP/Isabelle_Meta_Model (AFP)
20:56:09 Session AFP/LTL (AFP)
20:56:09 Session AFP/Stuttering_Equivalence (AFP)
20:56:09 Session AFP/Landau_Symbols (AFP)
20:56:09 Session AFP/Akra_Bazzi (AFP)
20:56:10 Session AFP/Catalan_Numbers (AFP)
20:56:10 Session AFP/Error_Function (AFP)
20:56:10 Session AFP/Euler_MacLaurin (AFP)
20:56:10 Session AFP/LightweightJava (AFP)
20:56:10 Session AFP/LinearQuantifierElim (AFP)
20:56:10 Session AFP/List-Infinite (AFP)
20:56:10 Session AFP/Nat-Interval-Logic (AFP)
20:56:10 Session AFP/AutoFocus-Stream (AFP)
20:56:10 Session AFP/MuchAdoAboutTwo (AFP)
20:56:10 Session AFP/Optics (AFP)
20:56:10 Session AFP/UTP-Toolkit (AFP)
20:56:10 Session AFP/UTP (AFP)
20:56:10 Session AFP/Order_Lattice_Props (AFP)
20:56:10 Session AFP/POPLmark-deBruijn (AFP)
20:56:10 Session AFP/Pairing_Heap (AFP)
20:56:10 Session AFP/Password_Authentication_Protocol (AFP)
20:56:10 Session AFP/Pell (AFP)
20:56:10 Session AFP/Presburger-Automata (AFP)
20:56:10 Session AFP/Priority_Queue_Braun (AFP)
20:56:10 Session AFP/Program-Conflict-Analysis (AFP)
20:56:10 Session AFP/Regular-Sets (AFP)
20:56:10 Session AFP/Abstract-Rewriting (AFP)
20:56:10 Session AFP/Decreasing-Diagrams (AFP)
20:56:10 Session AFP/First_Order_Terms (AFP)
20:56:10 Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
20:56:11 Session AFP/Automated_Stateful_Protocol_Verification (AFP)
20:56:11 Session AFP/Matrix (AFP)
20:56:11 Session AFP/Matrix_Tensor (AFP)
20:56:11 Session AFP/Knot_Theory (AFP)
20:56:11 Session AFP/Coinductive_Languages (AFP)
20:56:11 Session AFP/Finite_Automata_HF (AFP)
20:56:11 Session AFP/Functional-Automata (AFP)
20:56:11 Session AFP/Posix-Lexing (AFP)
20:56:11 Session AFP/Ribbon_Proofs (AFP)
20:56:11 Session AFP/SATSolverVerification (AFP)
20:56:11 Session AFP/Safe_OCL (AFP)
20:56:11 Session AFP/Selection_Heap_Sort (AFP)
20:56:11 Session AFP/Simplex (AFP)
20:56:11 Session AFP/Skew_Heap (AFP)
20:56:11 Session AFP/Sort_Encodings (AFP)
20:56:11 Session AFP/Splay_Tree (AFP)
20:56:11 Session AFP/Amortized_Complexity (AFP)
20:56:11 Session AFP/Dynamic_Tables (AFP)
20:56:11 Session AFP/Root_Balanced_Tree (AFP)
20:56:12 Session AFP/Closest_Pair_Points (AFP)
20:56:12 Session AFP/Stable_Matching (AFP)
20:56:12 Session AFP/SuperCalc (AFP)
20:56:12 Session Doc/System (doc)
20:56:12 Session AFP/Tail_Recursive_Functions (AFP)
20:56:12 Session AFP/TortoiseHare (AFP)
20:56:12 Session AFP/Trie (AFP)
20:56:12 Session AFP/Flyspeck-Tame (AFP)
20:56:12 Session AFP/Twelvefold_Way (AFP)
20:56:12 Session AFP/Vickrey_Clarke_Groves (AFP)
20:56:12 Session HOL/HOL-Matrix_LP
20:56:12 Session HOL/HOL-MicroJava (timing)
20:56:12 Session HOL/HOL-Mirabelle
20:56:12 Session HOL/HOL-Mirabelle-ex
20:56:12 Session HOL/HOL-Mutabelle
20:56:12 Session HOL/HOL-NanoJava
20:56:12 Session HOL/HOL-Nominal
20:56:12 Session AFP/CCS (AFP)
20:56:12 Session HOL/HOL-Nominal-Examples (timing)
20:56:13 Session AFP/Lam-ml-Normalization (AFP)
20:56:13 Session AFP/Pi_Calculus (AFP)
20:56:13 Session AFP/Psi_Calculi (AFP)
20:56:13 Session AFP/SequentInvertibility (AFP)
20:56:13 Session HOL/HOL-Predicate_Compile_Examples (timing)
20:56:13 Session HOL/HOL-Prolog
20:56:13 Session HOL/HOL-Quickcheck_Examples (timing)
20:56:13 Session HOL/HOL-Real_Asymp
20:56:14 Session AFP/Fourier (AFP)
20:56:14 Session AFP/Furstenberg_Topology (AFP)
20:56:14 Session HOL/HOL-Real_Asymp-Manual
20:56:15 Session AFP/Stirling_Formula (AFP)
20:56:15 Session AFP/Lambert_W (AFP)
20:56:15 Session HOL/HOL-SET_Protocol (timing)
20:56:15 Session HOL/HOL-Statespace
20:56:15 Session HOL/HOL-TLA
20:56:15 Session HOL/HOL-TLA-Buffer
20:56:15 Session HOL/HOL-TLA-Inc
20:56:15 Session HOL/HOL-TLA-Memory
20:56:15 Session HOL/HOL-TPTP
20:56:15 Session HOL/HOL-Types_To_Sets
20:56:15 Session AFP/Banach_Steinhaus (AFP)
20:56:15 Session AFP/Smooth_Manifolds (AFP)
20:56:16 Session HOL/HOL-Unix
20:56:16 Session HOL/HOL-Word (main timing)
20:56:16 Session HOL/HOL-Codegenerator_Test
20:56:16 Session HOL/HOL-SPARK
20:56:16 Session HOL/HOL-SPARK-Examples
20:56:16 Session AFP/RIPEMD-160-SPARK (AFP)
20:56:16 Session HOL/HOL-SPARK-Manual
20:56:16 Session HOL/HOL-Word-SMT_Examples (timing)
20:56:16 Session AFP/Kleene_Algebra (AFP)
20:56:16 Session AFP/KAT_and_DRA (AFP)
20:56:16 Session AFP/Multirelations (AFP)
20:56:16 Session AFP/Quantales (AFP)
20:56:16 Session AFP/Transformer_Semantics (AFP)
20:56:16 Session AFP/Regular_Algebras (AFP)
20:56:16 Session AFP/Relation_Algebra (AFP)
20:56:16 Session AFP/Residuated_Lattices (AFP)
20:56:16 Session AFP/LEM (AFP)
20:56:17 Session AFP/Native_Word (AFP)
20:56:17 Session AFP/Mersenne_Primes (AFP)
20:56:17 Session AFP/WebAssembly (AFP)
20:56:17 Session AFP/Refine_Monadic (AFP)
20:56:18 Session AFP/Collections (AFP)
20:56:18 Session AFP/Abstract_Completeness (AFP)
20:56:18 Session AFP/Abstract_Soundness (AFP)
20:56:18 Session AFP/Incredible_Proof_Machine (AFP)
20:56:18 Session AFP/Deriving (AFP)
20:56:18 Session AFP/CAVA_Base (AFP)
20:56:18 Session AFP/CAVA_Automata (AFP)
20:56:18 Session AFP/DFS_Framework (AFP)
20:56:18 Session AFP/Gabow_SCC (AFP)
20:56:18 Session AFP/LTL_to_GBA (AFP)
20:56:18 Session AFP/Promela (AFP)
20:56:18 Session AFP/Containers (AFP)
20:56:19 Session AFP/Collections_Examples (AFP)
20:56:19 Session AFP/Containers-Benchmarks (AFP)
20:56:19 Session AFP/MFOTL_Monitor (AFP)
20:56:19 Session AFP/Generic_Join (AFP)
20:56:19 Session AFP/Datatype_Order_Generator (AFP)
20:56:19 Session AFP/Old_Datatype_Show (AFP)
20:56:19 Session AFP/Show (AFP)
20:56:19 Session AFP/JNF-AFP-Lib (AFP)
20:56:20 Session AFP/Real_Impl (AFP)
20:56:20 Session AFP/QR_Decomposition (AFP)
20:56:20 Session AFP/Dijkstra_Shortest_Path (AFP)
20:56:20 Session AFP/Koenigsberg_Friendship (AFP)
20:56:20 Session AFP/Transition_Systems_and_Automata (AFP)
20:56:20 Session AFP/Adaptive_State_Counting (AFP)
20:56:20 Session AFP/Buchi_Complementation (AFP)
20:56:20 Session AFP/LTL_Master_Theorem (AFP)
20:56:20 Session AFP/LTL_Normal_Form (AFP)
20:56:20 Session AFP/Partial_Order_Reduction (AFP)
20:56:21 Session AFP/SM_Base (AFP)
20:56:21 Session AFP/SM (AFP)
20:56:21 Session AFP/CAVA_Setup (AFP)
20:56:21 Session AFP/CAVA_LTL_Modelchecker (AFP)
20:56:21 Session AFP/Transitive-Closure (AFP)
20:56:21 Session AFP/KBPs (AFP)
20:56:21 Session AFP/Tree-Automata (AFP)
20:56:21 Session AFP/SPARCv8 (AFP)
20:56:21 Session AFP/Separation_Algebra (AFP)
20:56:21 Session AFP/Separata (AFP)
20:56:21 Session AFP/Separation_Logic_Imperative_HOL (AFP)
20:56:22 Session AFP/Sepref_Prereq (AFP)
20:56:22 Session AFP/ROBDD (AFP)
20:56:22 Session AFP/UpDown_Scheme (AFP)
20:56:22 Session AFP/Word_Lib (AFP)
20:56:22 Session AFP/Complx (AFP)
20:56:22 Session AFP/IEEE_Floating_Point (AFP)
20:56:22 Session AFP/CakeML (AFP)
20:56:22 Session AFP/MFODL_Monitor_Optimized (AFP)
20:56:22 Session AFP/IP_Addresses (AFP)
20:56:23 Session AFP/Simple_Firewall (AFP)
20:56:23 Session AFP/Routing (AFP)
20:56:23 Session AFP/Iptables_Semantics (AFP)
20:56:23 Session AFP/Iptables_Semantics_Examples (AFP)
20:56:23 Session AFP/LOFT (AFP)
20:56:23 Session AFP/Interval_Arithmetic_Word32 (AFP)
20:56:23 Session HOL/HOL-ZF
20:56:23 Session AFP/Category2 (AFP)
20:56:23 Session HOL/HOLCF (main timing)
20:56:23 Session AFP/Circus (AFP)
20:56:23 Session AFP/HOL-CSP (AFP)
20:56:23 Session HOL/HOLCF-IMP
20:56:23 Session HOL/HOLCF-Library
20:56:23 Session HOL/HOLCF-FOCUS
20:56:23 Session HOL/HOLCF-ex
20:56:24 Session AFP/PCF (AFP)
20:56:24 Session AFP/HOLCF-Prelude (AFP)
20:56:24 Session HOL/HOLCF-Tutorial
20:56:24 Session HOL/IOA (timing)
20:56:24 Session HOL/IOA-ABP
20:56:24 Session HOL/IOA-NTP
20:56:24 Session HOL/IOA-Storage
20:56:24 Session HOL/IOA-ex
20:56:24 Session AFP/Shivers-CFA (AFP)
20:56:24 Session AFP/Stream-Fusion (AFP)
20:56:24 Session AFP/Tycon (AFP)
20:56:24 Session AFP/WorkerWrapper (AFP)
20:56:24 Session AFP/Heard_Of (AFP)
20:56:24 Session AFP/Consensus_Refined (AFP)
20:56:24 Session AFP/Hello_World (AFP)
20:56:24 Session AFP/Hoare_Time (AFP)
20:56:24 Session AFP/HotelKeyCards (AFP)
20:56:24 Session Doc/How_to_Prove_it (no_doc)
20:56:24 Session AFP/Huffman (AFP)
20:56:24 Session AFP/Hybrid_Logic (AFP)
20:56:24 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
20:56:24 Session AFP/IMP2 (AFP)
20:56:25 Session AFP/IMP2_Binary_Heap (AFP)
20:56:25 Session Doc/Implementation (doc)
20:56:25 Session AFP/Impossible_Geometry (AFP)
20:56:25 Session AFP/Inductive_Confidentiality (AFP)
20:56:25 Session AFP/InfPathElimination (AFP)
20:56:25 Session Doc/Isar_Ref (doc)
20:56:25 Session AFP/Isabelle_C (AFP)
20:56:25 Session Doc/JEdit (doc)
20:56:25 Session AFP/Jacobson_Basic_Algebra (AFP)
20:56:25 Session AFP/JiveDataStoreModel (AFP)
20:56:25 Session AFP/KAD (AFP)
20:56:25 Session AFP/Algebraic_VCs (AFP)
20:56:25 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
20:56:25 Session AFP/LambdaMu (AFP)
20:56:25 Session AFP/LatticeProperties (AFP)
20:56:25 Session AFP/DataRefinementIBP (AFP)
20:56:25 Session AFP/GraphMarkingIBP (AFP)
20:56:25 Session AFP/Lazy_Case (AFP)
20:56:25 Session AFP/Dict_Construction (AFP)
20:56:25 Session AFP/Lifting_Definition_Option (AFP)
20:56:25 Session AFP/List-Index (AFP)
20:56:25 Session AFP/Affine_Arithmetic (AFP)
20:56:26 Session AFP/Taylor_Models (AFP)
20:56:26 Session AFP/Comparison_Sort_Lower_Bound (AFP)
20:56:26 Session AFP/Formula_Derivatives (AFP)
20:56:26 Session AFP/Formula_Derivatives-Examples (AFP)
20:56:26 Session AFP/Jinja (AFP)
20:56:26 Session AFP/HRB-Slicing (AFP)
20:56:26 Session AFP/InformationFlowSlicing_Inter (AFP)
20:56:26 Session AFP/Slicing (AFP)
20:56:26 Session AFP/Formal_SSA (AFP)
20:56:26 Session AFP/Minimal_SSA (AFP)
20:56:26 Session AFP/InformationFlowSlicing (AFP)
20:56:26 Session AFP/LTL_to_DRA (AFP)
20:56:26 Session AFP/List_Update (AFP)
20:56:26 Session AFP/Ordinary_Differential_Equations (AFP)
20:56:27 Session AFP/Differential_Dynamic_Logic (AFP)
20:56:27 Session AFP/HOL-ODE-Numerics (AFP)
20:56:27 Session AFP/HOL-ODE-ARCH-COMP (AFP)
20:56:27 Session AFP/HOL-ODE-Examples (AFP large)
20:56:27 Session AFP/Lorenz_Approximation (AFP)
20:56:27 Session AFP/Lorenz_C0 (AFP large)
20:56:27 Session AFP/Lorenz_C1 (AFP large)
20:56:27 Session AFP/Poincare_Bendixson (AFP)
20:56:27 Session AFP/Hybrid_Systems_VCs (AFP)
20:56:27 Session AFP/Matrices_for_ODEs (AFP)
20:56:27 Session AFP/Quick_Sort_Cost (AFP)
20:56:27 Session AFP/Random_BSTs (AFP)
20:56:27 Session AFP/Randomised_BSTs (AFP)
20:56:27 Session AFP/Treaps (AFP)
20:56:27 Session AFP/Randomised_Social_Choice (AFP)
20:56:28 Session AFP/Fishburn_Impossibility (AFP)
20:56:28 Session AFP/SDS_Impossibility (AFP)
20:56:28 Session AFP/Refine_Imperative_HOL (AFP)
20:56:28 Session AFP/Floyd_Warshall (AFP)
20:56:28 Session AFP/Sepref_Basic (AFP)
20:56:28 Session AFP/Sepref_IICF (AFP)
20:56:28 Session AFP/Flow_Networks (AFP)
20:56:28 Session AFP/EdmondsKarp_Maxflow (AFP)
20:56:28 Session AFP/MFMC_Countable (AFP)
20:56:28 Session AFP/Prpu_Maxflow (AFP)
20:56:28 Session AFP/Knuth_Morris_Pratt (AFP)
20:56:28 Session AFP/VerifyThis2018 (AFP)
20:56:28 Session AFP/VerifyThis2019 (AFP)
20:56:28 Session AFP/List_Interleaving (AFP)
20:56:28 Session AFP/List_Inversions (AFP)
20:56:29 Session AFP/LocalLexing (AFP)
20:56:29 Session Doc/Locales (doc)
20:56:29 Session AFP/Locally-Nameless-Sigma (AFP)
20:56:29 Session AFP/Lowe_Ontological_Argument (AFP)
20:56:29 Session AFP/MSO_Regex_Equivalence (AFP)
20:56:29 Session Doc/Main (doc)
20:56:29 Session AFP/Marriage (AFP)
20:56:29 Session AFP/Latin_Square (AFP)
20:56:29 Session AFP/Matroids (AFP)
20:56:29 Session AFP/Kruskal (AFP)
20:56:29 Session AFP/Max-Card-Matching (AFP)
20:56:29 Session AFP/Median_Of_Medians_Selection (AFP)
20:56:29 Session AFP/KD_Tree (AFP)
20:56:29 Session AFP/Menger (AFP)
20:56:29 Session AFP/MiniML (AFP)
20:56:29 Session AFP/Modular_Assembly_Kit_Security (AFP)
20:56:29 Session AFP/Monad_Memo_DP (AFP)
20:56:29 Session AFP/Hidden_Markov_Models (AFP)
20:56:30 Session AFP/Optimal_BST (AFP)
20:56:30 Session AFP/MonoBoolTranAlgebra (AFP)
20:56:30 Session AFP/Name_Carrying_Type_Inference (AFP)
20:56:30 Session AFP/Nash_Williams (AFP)
20:56:30 Session AFP/Network_Security_Policy_Verification (AFP)
20:56:30 Session AFP/No_FTL_observers (AFP)
20:56:30 Session AFP/Nominal2 (AFP)
20:56:30 Session AFP/Incompleteness (AFP)
20:56:30 Session AFP/Surprise_Paradox (AFP)
20:56:30 Session AFP/LambdaAuth (AFP)
20:56:31 Session AFP/Launchbury (AFP)
20:56:31 Session AFP/Call_Arity (AFP)
20:56:31 Session AFP/Modal_Logics_for_NTS (AFP)
20:56:31 Session AFP/Rewriting_Z (AFP)
20:56:31 Session AFP/Noninterference_CSP (AFP)
20:56:31 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
20:56:31 Session AFP/Noninterference_Generic_Unwinding (AFP)
20:56:31 Session AFP/Noninterference_Inductive_Unwinding (AFP)
20:56:31 Session AFP/Noninterference_Sequential_Composition (AFP)
20:56:31 Session AFP/Noninterference_Concurrent_Composition (AFP)
20:56:31 Session AFP/NormByEval (AFP)
20:56:31 Session AFP/OpSets (AFP)
20:56:31 Session AFP/Open_Induction (AFP)
20:56:31 Session AFP/Well_Quasi_Orders (AFP)
20:56:31 Session AFP/Decreasing-Diagrams-II (AFP)
20:56:31 Session AFP/Myhill-Nerode (AFP)
20:56:31 Session AFP/Polynomials (AFP)
20:56:31 Session AFP/Symmetric_Polynomials (AFP)
20:56:32 Session AFP/Pi_Transcendental (AFP)
20:56:32 Session AFP/Ordinal (AFP)
20:56:32 Session AFP/Nested_Multisets_Ordinals (AFP)
20:56:32 Session AFP/Lambda_Free_RPOs (AFP)
20:56:32 Session AFP/Higher_Order_Terms (AFP)
20:56:32 Session AFP/CakeML_Codegen (AFP)
20:56:33 Session AFP/Lambda_Free_EPO (AFP)
20:56:33 Session AFP/Lambda_Free_KBOs (AFP)
20:56:33 Session AFP/Ordered_Resolution_Prover (AFP)
20:56:33 Session AFP/Saturation_Framework (AFP)
20:56:33 Session AFP/PLM (AFP)
20:56:33 Session AFP/PSemigroupsConvolution (AFP)
20:56:33 Session AFP/Paraconsistency (AFP)
20:56:33 Session AFP/Parity_Game (AFP)
20:56:33 Session AFP/Partial_Function_MR (AFP)
20:56:33 Session AFP/Certification_Monads (AFP)
20:56:33 Session AFP/XML (AFP)
20:56:33 Session AFP/Polynomial_Factorization (AFP)
20:56:33 Session AFP/Dirichlet_Series (AFP)
20:56:34 Session AFP/Zeta_Function (AFP)
20:56:34 Session AFP/Dirichlet_L (AFP)
20:56:34 Session AFP/Gauss_Sums (AFP)
20:56:34 Session AFP/Prime_Number_Theorem (AFP)
20:56:34 Session AFP/Prime_Distribution_Elementary (AFP)
20:56:34 Session AFP/IMO2019 (AFP)
20:56:34 Session AFP/Irrational_Series_Erdos_Straus (AFP)
20:56:35 Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
20:56:35 Session AFP/Zeta_3_Irrational (AFP)
20:56:35 Session AFP/Gaussian_Integers (AFP)
20:56:35 Session AFP/Jordan_Normal_Form (AFP)
20:56:36 Session AFP/Deep_Learning (AFP)
20:56:36 Session AFP/Farkas (AFP)
20:56:36 Session AFP/Groebner_Bases (AFP)
20:56:36 Session AFP/Groebner_Macaulay (AFP)
20:56:36 Session AFP/Nullstellensatz (AFP)
20:56:36 Session AFP/Signature_Groebner (AFP)
20:56:36 Session AFP/QHLProver (AFP)
20:56:37 Session AFP/Knuth_Bendix_Order (AFP)
20:56:37 Session AFP/Functional_Ordered_Resolution_Prover (AFP)
20:56:37 Session AFP/Linear_Recurrences (AFP)
20:56:37 Session AFP/Perron_Frobenius (AFP)
20:56:38 Session AFP/Stochastic_Matrices (AFP)
20:56:38 Session AFP/Power_Sum_Polynomials (AFP)
20:56:38 Session AFP/Subresultants (AFP)
20:56:38 Session AFP/Pre_BZ (AFP)
20:56:38 Session AFP/Berlekamp_Zassenhaus (AFP)
20:56:39 Session AFP/Algebraic_Numbers (AFP)
20:56:39 Session AFP/LLL_Basis_Reduction (AFP)
20:56:39 Session AFP/LLL_Factorization (AFP)
20:56:39 Session AFP/Linear_Inequalities (AFP)
20:56:39 Session AFP/Linear_Programming (AFP)
20:56:39 Session AFP/Linear_Recurrences_Solver (AFP)
20:56:39 Session AFP/Smith_Normal_Form (AFP)
20:56:39 Session AFP/Probabilistic_While (AFP)
20:56:39 Session AFP/CryptHOL (AFP)
20:56:39 Session AFP/Constructive_Cryptography (AFP)
20:56:39 Session AFP/Game_Based_Crypto (AFP)
20:56:40 Session AFP/Multi_Party_Computation (AFP)
20:56:40 Session AFP/Sigma_Commit_Crypto (AFP)
20:56:40 Session AFP/Pop_Refinement (AFP)
20:56:40 Session AFP/Possibilistic_Noninterference (AFP)
20:56:40 Session AFP/Priority_Search_Trees (AFP)
20:56:40 Session AFP/Prim_Dijkstra_Simple (AFP)
20:56:40 Session Doc/Prog_Prove (doc)
20:56:40 Session AFP/Projective_Geometry (AFP)
20:56:40 Session AFP/Proof_Strategy_Language (AFP)
20:56:40 Session AFP/PropResPI (AFP)
20:56:40 Session AFP/Propositional_Proof_Systems (AFP)
20:56:40 Session AFP/PseudoHoops (AFP)
20:56:40 Session AFP/Ramsey-Infinite (AFP)
20:56:40 Session AFP/Recursion-Theory-I (AFP)
20:56:40 Session AFP/Minsky_Machines (AFP)
20:56:41 Session AFP/RefinementReactive (AFP)
20:56:41 Session AFP/Regex_Equivalence (AFP)
20:56:41 Session AFP/Resolution_FOL (AFP)
20:56:41 Session AFP/Robbins-Conjecture (AFP)
20:56:41 Session AFP/Roy_Floyd_Warshall (AFP)
20:56:41 Session AFP/SIFPL (AFP)
20:56:41 Session AFP/SIFUM_Type_Systems (AFP)
20:56:41 Session AFP/Security_Protocol_Refinement (AFP)
20:56:41 Session AFP/SenSocialChoice (AFP)
20:56:41 Session AFP/Simpl (AFP)
20:56:42 Session AFP/BDD (AFP)
20:56:42 Session AFP/Planarity_Certificates (AFP)
20:56:42 Session AFP/Sliding_Window_Algorithm (AFP)
20:56:42 Session AFP/Statecharts (AFP)
20:56:42 Session AFP/Stellar_Quorums (AFP)
20:56:42 Session AFP/Stone_Algebras (AFP)
20:56:42 Session AFP/Stone_Relation_Algebras (AFP)
20:56:42 Session AFP/Stone_Kleene_Relation_Algebras (AFP)
20:56:42 Session AFP/Aggregation_Algebras (AFP)
20:56:42 Session AFP/Subset_Boolean_Algebras (AFP)
20:56:42 Session AFP/Store_Buffer_Reduction (AFP)
20:56:42 Session AFP/Strong_Security (AFP)
20:56:42 Session Doc/Sugar (doc)
20:56:42 Session AFP/Szpilrajn (AFP)
20:56:42 Session AFP/TESL_Language (AFP)
20:56:42 Session AFP/TLA (AFP)
20:56:42 Session AFP/Timed_Automata (AFP)
20:56:42 Session AFP/Probabilistic_Timed_Automata (AFP)
20:56:42 Session AFP/Transitive-Closure-II (AFP)
20:56:42 Session AFP/Tree_Decomposition (AFP)
20:56:42 Session Doc/Tutorial (doc)
20:56:43 Session Doc/Typeclass_Hierarchy (doc)
20:56:43 Session AFP/Types_Tableaus_and_Goedels_God (AFP)
20:56:43 Session AFP/UPF (AFP)
20:56:43 Session AFP/UPF_Firewall (AFP)
20:56:43 Session AFP/Universal_Turing_Machine (AFP)
20:56:43 Session AFP/VeriComp (AFP)
20:56:43 Session AFP/Verified-Prover (AFP)
20:56:43 Session AFP/VolpanoSmith (AFP)
20:56:43 Session AFP/WHATandWHERE_Security (AFP)
20:56:43 Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
20:56:43 Session AFP/Weight_Balanced_Trees (AFP)
20:56:43 Session AFP/ZFC_in_HOL (AFP)
20:56:43 Session ZF/ZF (main timing)
20:56:43 Session Doc/Logics_ZF (doc)
20:56:43 Session AFP/Recursion-Addition (AFP)
20:56:43 Session ZF/ZF-AC
20:56:43 Session ZF/ZF-Coind
20:56:43 Session ZF/ZF-Constructible
20:56:44 Session AFP/Forcing (AFP)
20:56:44 Session ZF/ZF-IMP
20:56:44 Session ZF/ZF-Induct
20:56:44 Session ZF/ZF-UNITY (timing)
20:56:44 Session ZF/ZF-Resid
20:56:44 Session ZF/ZF-ex
20:57:48 Building HOL-ODE-Numerics ...
20:57:48 Building Refine_Monadic ...
20:57:48 Building HOL-Word ...
20:57:48 Building Deriving ...
20:57:48 Building Pre_BZ ...
20:57:48 Running HOL-Codegenerator_Test ...
20:57:48 Building Affine_Arithmetic ...
20:57:49 Building Datatype_Order_Generator ...
20:57:49 Running Functional_Ordered_Resolution_Prover ...
20:57:49 Running WebAssembly ...
20:57:49 HOL-Word: theory HOL-Word.Misc_Auxiliary
20:57:49 HOL-Word: theory HOL-Library.Phantom_Type
20:57:49 HOL-Word: theory HOL-Library.Boolean_Algebra
20:57:49 HOL-Word: theory HOL-Word.Misc_Typedef
20:57:49 HOL-Word: theory HOL-Word.Traditional_Syntax
20:57:50 Refine_Monadic: theory HOL-Library.Boolean_Algebra
20:57:50 Refine_Monadic: theory HOL-Library.Adhoc_Overloading
20:57:50 Refine_Monadic: theory HOL-Library.Phantom_Type
20:57:50 Refine_Monadic: theory HOL-Library.While_Combinator
20:57:50 HOL-Word: theory HOL-Library.Bit_Operations
20:57:50 Refine_Monadic: theory HOL-Library.Monad_Syntax
20:57:50 Refine_Monadic: theory HOL-Word.Misc_Typedef
20:57:50 Refine_Monadic: theory HOL-Library.Bit_Operations
20:57:50 Deriving: theory Deriving.Comparator
20:57:50 Deriving: theory Deriving.Derive_Manager
20:57:50 Deriving: theory Deriving.Generator_Aux
20:57:50 Deriving: theory HOL-Word.Misc_Typedef
20:57:50 Refine_Monadic: theory HOL-Word.Traditional_Syntax
20:57:50 Deriving: theory HOL-Word.Traditional_Syntax
20:57:50 Datatype_Order_Generator: theory Deriving.Derive_Manager
20:57:50 Datatype_Order_Generator: theory HOL-Word.Misc_Typedef
20:57:50 Datatype_Order_Generator: theory HOL-Word.Traditional_Syntax
20:57:50 Datatype_Order_Generator: theory Deriving.Countable_Generator
20:57:50 Datatype_Order_Generator: theory Datatype_Order_Generator.Derive_Aux
20:57:50 Deriving: theory Deriving.Countable_Generator
20:57:50 Refine_Monadic: theory Refine_Monadic.Example_Chapter
20:57:50 Deriving: theory Deriving.Equality_Generator
20:57:50 Refine_Monadic: theory Refine_Monadic.Refine_Chapter
20:57:50 HOL-Word: theory HOL-Library.Cardinality
20:57:50 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False
20:57:50 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp
20:57:50 HOL-Codegenerator_Test: theory HOL-Examples.Records
20:57:50 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Lazy_Test
20:57:50 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
20:57:50 Refine_Monadic: theory HOL-Library.Cardinality
20:57:51 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less
20:57:51 Affine_Arithmetic: theory Deriving.Comparator
20:57:51 Affine_Arithmetic: theory Deriving.Derive_Manager
20:57:51 Affine_Arithmetic: theory Deriving.Generator_Aux
20:57:51 Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order
20:57:51 WebAssembly: theory HOL-Word.Misc_Typedef
20:57:51 WebAssembly: theory HOL-Word.Traditional_Syntax
20:57:51 WebAssembly: theory WebAssembly.Wasm_Type_Abs
20:57:51 Datatype_Order_Generator: theory Datatype_Order_Generator.Order_Generator
20:57:51 Refine_Monadic: theory Refine_Monadic.Refine_Misc
20:57:51 Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
20:57:51 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del
20:57:51 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
20:57:51 Affine_Arithmetic: theory HOL-Library.Monad_Syntax
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
20:57:51 Affine_Arithmetic: theory Deriving.Equality_Generator
20:57:51 Affine_Arithmetic: theory HOL-Library.Boolean_Algebra
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
20:57:51 Deriving: theory Deriving.Equality_Instances
20:57:51 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del
20:57:51 HOL-ODE-Numerics: theory Deriving.Comparator
20:57:51 HOL-ODE-Numerics: theory Deriving.Derive_Manager
20:57:51 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
20:57:51 Deriving: theory Deriving.Compare
20:57:51 Deriving: theory Deriving.Comparator_Generator
20:57:51 HOL-ODE-Numerics: theory Deriving.Generator_Aux
20:57:51 Datatype_Order_Generator: theory HOL-Word.Bits_Int
20:57:51 Deriving: theory Deriving.RBT_Comparator_Impl
20:57:51 Affine_Arithmetic: theory HOL-Library.Bit_Operations
20:57:51 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_Specs
20:57:51 Deriving: theory HOL-Word.Bits_Int
20:57:52 WebAssembly: theory HOL-Word.Bits_Int
20:57:52 Refine_Monadic: theory Refine_Monadic.RefineG_Domain
20:57:52 HOL-Codegenerator_Test: theory HOL-Word.Misc_Typedef
20:57:52 HOL-ODE-Numerics: theory Deriving.Equality_Generator
20:57:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_Specs
20:57:52 Affine_Arithmetic: theory Deriving.Equality_Instances
20:57:52 HOL-Codegenerator_Test: theory HOL-Word.Traditional_Syntax
20:57:52 HOL-Word: theory HOL-Library.Numeral_Type
20:57:52 Refine_Monadic: theory HOL-Library.Numeral_Type
20:57:52 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
20:57:52 HOL-ODE-Numerics: theory HOL-Library.AList
20:57:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set
20:57:52 Affine_Arithmetic: theory HOL-Library.Permutation
20:57:52 Deriving: theory Deriving.RBT_Compare_Order_Impl
20:57:52 Affine_Arithmetic: theory Deriving.Compare
20:57:52 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
20:57:52 Affine_Arithmetic: theory Deriving.Comparator_Generator
20:57:52 Pre_BZ: theory Efficient-Mergesort.Efficient_Sort
20:57:52 Pre_BZ: theory HOL-Number_Theory.Cong
20:57:52 Pre_BZ: theory Polynomial_Factorization.Precomputation
20:57:52 Pre_BZ: theory HOL-Types_To_Sets.Types_To_Sets
20:57:52 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
20:57:52 Deriving: theory Deriving.Compare_Generator
20:57:52 Refine_Monadic: theory Refine_Monadic.RefineG_Assert
20:57:52 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
20:57:52 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
20:57:53 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
20:57:53 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
20:57:53 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
20:57:53 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
20:57:53 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
20:57:53 HOL-ODE-Numerics: theory Deriving.Compare
20:57:53 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
20:57:53 HOL-ODE-Numerics: theory Deriving.Equality_Instances
20:57:53 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
20:57:53 Pre_BZ: theory HOL-Word.Misc_Typedef
20:57:53 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
20:57:53 Pre_BZ: theory HOL-Word.Traditional_Syntax
20:57:53 HOL-ODE-Numerics: theory HOL-Library.Boolean_Algebra
20:57:53 Deriving: theory Deriving.Compare_Instances
20:57:53 Affine_Arithmetic: theory HOL-Library.Char_ord
20:57:53 Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
20:57:53 Pre_BZ: theory Cauchy.CauchysMeanTheorem
20:57:53 HOL-Codegenerator_Test: theory HOL-Word.Bits_Int
20:57:53 Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
20:57:53 Deriving: theory Deriving.Compare_Rat
20:57:53 HOL-ODE-Numerics: theory HOL-Library.Bit_Operations
20:57:53 Refine_Monadic: theory Refine_Monadic.RefineG_While
20:57:53 Refine_Monadic: theory Refine_Monadic.Refine_Basic
20:57:54 Affine_Arithmetic: theory Deriving.Compare_Generator
20:57:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map
20:57:54 HOL-Word: theory HOL-Library.Type_Length
20:57:54 HOL-ODE-Numerics: theory HOL-Library.Permutation
20:57:54 Affine_Arithmetic: theory HOL-Library.Code_Target_Int
20:57:54 Deriving: theory Deriving.Compare_Real
20:57:54 Pre_BZ: theory Polynomial_Interpolation.Improved_Code_Equations
20:57:54 HOL-ODE-Numerics: theory HOL-ex.Quicksort
20:57:54 HOL-ODE-Numerics: theory Deriving.Compare_Generator
20:57:54 Refine_Monadic: theory HOL-Library.Type_Length
20:57:54 Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
20:57:54 Deriving: theory Deriving.Compare_Order_Instances
20:57:54 Affine_Arithmetic: theory Deriving.Compare_Instances
20:57:54 HOL-ODE-Numerics: theory HOL-Library.Char_ord
20:57:54 Pre_BZ: theory HOL-Word.Bits_Int
20:57:54 Pre_BZ: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
20:57:54 Affine_Arithmetic: theory HOL-Library.Mapping
20:57:54 HOL-ODE-Numerics: theory HOL-Library.Mapping
20:57:55 Datatype_Order_Generator: theory HOL-Word.Bit_Comprehension
20:57:55 Refine_Monadic: theory Refine_Monadic.Refine_Det
20:57:55 Pre_BZ: theory Polynomial_Factorization.Polynomial_Divisibility
20:57:55 HOL-ODE-Numerics: theory Deriving.Compare_Instances
20:57:55 Pre_BZ: theory Polynomial_Interpolation.Lagrange_Interpolation
20:57:55 Functional_Ordered_Resolution_Prover: theory Deriving.Comparator
20:57:55 Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager
20:57:55 Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux
20:57:55 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More
20:57:55 Pre_BZ: theory HOL-Number_Theory.Totient
20:57:55 HOL-ODE-Numerics: theory HOL-Library.Option_ord
20:57:55 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term
20:57:55 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More
20:57:55 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
20:57:55 Deriving: theory HOL-Word.Bit_Comprehension
20:57:55 Affine_Arithmetic: theory HOL-Library.Type_Length
20:57:55 Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union
20:57:55 Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator
20:57:55 Affine_Arithmetic: theory HOL-Library.RBT_Impl
20:57:56 Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension
20:57:56 Pre_BZ: theory Polynomial_Factorization.Missing_List
20:57:56 HOL-Word: theory HOL-Word.Bits_Int
20:57:56 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad
20:57:56 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
20:57:56 HOL-ODE-Numerics: theory HOL-Library.Parallel
20:57:56 Datatype_Order_Generator: theory HOL-Word.Word
20:57:56 Affine_Arithmetic: theory HOL-Word.Misc_Typedef
20:57:56 Pre_BZ: theory HOL-Number_Theory.Residues
20:57:56 Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances
20:57:56 Datatype_Order_Generator: theory Native_Word.More_Bits_Int
20:57:56 WebAssembly: theory HOL-Word.Bit_Comprehension
20:57:56 HOL-ODE-Numerics: theory HOL-Library.Type_Length
20:57:56 Deriving: theory HOL-Word.Word
20:57:56 Pre_BZ: theory Polynomial_Interpolation.Is_Rat_To_Rat
20:57:56 Refine_Monadic: theory HOL-Word.Bits_Int
20:57:56 Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq
20:57:56 Affine_Arithmetic: theory HOL-Word.Traditional_Syntax
20:57:56 Affine_Arithmetic: theory Deriving.Countable_Generator
20:57:56 Deriving: theory Native_Word.More_Bits_Int
20:57:56 Functional_Ordered_Resolution_Prover: theory Deriving.Compare
20:57:57 Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator
20:57:57 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
20:57:57 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
20:57:57 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More
20:57:57 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers
20:57:57 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset
20:57:57 HOL-Codegenerator_Test: theory HOL-Word.Bit_Comprehension
20:57:57 Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
20:57:57 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption
20:57:57 Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Typedef
20:57:58 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
20:57:58 Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator
20:57:58 Functional_Ordered_Resolution_Prover: theory HOL-Word.Traditional_Syntax
20:57:58 Affine_Arithmetic: theory HOL-Library.Log_Nat
20:57:58 WebAssembly: theory HOL-Word.Word
20:57:58 Affine_Arithmetic: theory HOL-Word.Bits_Int
20:57:58 Pre_BZ: theory HOL-Word.Bit_Comprehension
20:57:58 WebAssembly: theory Native_Word.More_Bits_Int
20:57:58 Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator
20:57:58 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
20:57:58 Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances
20:57:58 Functional_Ordered_Resolution_Prover: theory Lambda_Free_RPOs.Lambda_Free_Util
20:57:58 HOL-Codegenerator_Test: theory HOL-Word.Word
20:57:58 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
20:57:59 Pre_BZ: theory Sqrt_Babylonian.Log_Impl
20:57:59 Functional_Ordered_Resolution_Prover: theory Matrix.Utility
20:57:59 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
20:57:59 Refine_Monadic: theory Refine_Monadic.Refine_Leof
20:57:59 Refine_Monadic: theory Refine_Monadic.Refine_Pfun
20:57:59 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
20:57:59 Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Int
20:57:59 Pre_BZ: theory HOL-Word.Word
20:57:59 HOL-Word: theory HOL-Word.Bit_Comprehension
20:57:59 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
20:57:59 Refine_Monadic: theory Refine_Monadic.Refine_While
20:57:59 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
20:57:59 HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef
20:57:59 Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates
20:57:59 Pre_BZ: theory Native_Word.More_Bits_Int
20:57:59 Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List
20:58:00 Pre_BZ: theory Sqrt_Babylonian.NthRoot_Impl
20:58:00 HOL-ODE-Numerics: theory HOL-Word.Traditional_Syntax
20:58:00 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
20:58:00 Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
20:58:00 Pre_BZ: theory Polynomial_Factorization.Missing_Multiset
20:58:00 HOL-ODE-Numerics: theory Deriving.Countable_Generator
20:58:00 Pre_BZ: theory Polynomial_Factorization.Prime_Factorization
20:58:00 Refine_Monadic: theory HOL-Word.Bit_Comprehension
20:58:00 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set
20:58:00 HOL-Word: theory HOL-Word.Misc_Arithmetic
20:58:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
20:58:01 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
20:58:01 HOL-Word: theory HOL-Word.Word
20:58:01 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian
20:58:01 HOL-ODE-Numerics: theory HOL-Word.Bits_Int
20:58:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
20:58:01 Refine_Monadic: theory Refine_Monadic.Refine_Transfer
20:58:01 Pre_BZ: theory Polynomial_Interpolation.Divmod_Int
20:58:01 Pre_BZ: theory Polynomial_Factorization.Dvd_Int_Poly
20:58:01 Pre_BZ: theory Polynomial_Factorization.Explicit_Roots
20:58:01 Refine_Monadic: theory HOL-Word.Word
20:58:01 Affine_Arithmetic: theory HOL-Word.Bit_Comprehension
20:58:01 Pre_BZ: theory Polynomial_Factorization.Gauss_Lemma
20:58:02 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
20:58:02 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
20:58:02 Affine_Arithmetic: theory Affine_Arithmetic.Polygon
20:58:02 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
20:58:02 Refine_Monadic: theory Refine_Monadic.Refine_Automation
20:58:02 Refine_Monadic: theory Refine_Monadic.Refine_Foreach
20:58:02 Pre_BZ: theory Polynomial_Factorization.Square_Free_Factorization
20:58:03 Affine_Arithmetic: theory HOL-Word.Word
20:58:03 Affine_Arithmetic: theory Native_Word.More_Bits_Int
20:58:03 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
20:58:03 Pre_BZ: theory Polynomial_Interpolation.Newton_Interpolation
20:58:03 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
20:58:03 Functional_Ordered_Resolution_Prover: theory HOL-Word.Bit_Comprehension
20:58:03 Pre_BZ: theory Polynomial_Factorization.Gcd_Rat_Poly
20:58:03 Datatype_Order_Generator: theory HOL-Word.Reversed_Bit_Lists
20:58:04 Functional_Ordered_Resolution_Prover: theory Show.Show
20:58:04 Deriving: theory HOL-Word.Reversed_Bit_Lists
20:58:04 Pre_BZ: theory Polynomial_Factorization.Rational_Root_Test
20:58:04 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
20:58:04 Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
20:58:04 Functional_Ordered_Resolution_Prover: theory HOL-Word.Word
20:58:04 Functional_Ordered_Resolution_Prover: theory Native_Word.More_Bits_Int
20:58:05 HOL-ODE-Numerics: theory Collections.SetIterator
20:58:05 HOL-ODE-Numerics: theory HOL-Word.Bit_Comprehension
20:58:05 Affine_Arithmetic: theory List-Index.List_Index
20:58:05 Pre_BZ: theory Show.Show_Poly
20:58:05 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML
20:58:05 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala
20:58:05 WebAssembly: theory HOL-Word.Reversed_Bit_Lists
20:58:05 Datatype_Order_Generator: theory HOL-Word.Misc_lsb
20:58:06 Affine_Arithmetic: theory Show.Show
20:58:06 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp
20:58:06 Affine_Arithmetic: theory HOL-Library.Interval
20:58:06 Refine_Monadic: theory Refine_Monadic.Refine_Monadic
20:58:06 HOL-ODE-Numerics: theory HOL-Word.Word
20:58:06 Datatype_Order_Generator: theory HOL-Word.Misc_msb
20:58:06 Deriving: theory HOL-Word.Misc_lsb
20:58:06 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates
20:58:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
20:58:06 Datatype_Order_Generator: theory HOL-Word.Misc_set_bit
20:58:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
20:58:07 Functional_Ordered_Resolution_Prover: theory Show.Show_Instances
20:58:07 Deriving: theory HOL-Word.Misc_msb
20:58:07 Pre_BZ: theory HOL-Word.Reversed_Bit_Lists
20:58:07 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
20:58:07 Deriving: theory HOL-Word.Misc_set_bit
20:58:07 Affine_Arithmetic: theory HOL-Library.Float
20:58:08 WebAssembly: theory HOL-Word.Misc_lsb
20:58:08 Pre_BZ: theory Polynomial_Interpolation.Polynomial_Interpolation
20:58:08 WebAssembly: theory HOL-Word.Misc_msb
20:58:08 WebAssembly: theory HOL-Word.Misc_set_bit
20:58:08 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
20:58:08 HOL-Word: theory HOL-Word.Reversed_Bit_Lists
20:58:09 Datatype_Order_Generator: theory Native_Word.Code_Symbolic_Bits_Int
20:58:09 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
20:58:09 Pre_BZ: theory HOL-Word.Misc_lsb
20:58:09 Refine_Monadic: theory Refine_Monadic.WordRefine
20:58:09 Pre_BZ: theory HOL-Word.Misc_msb
20:58:10 Datatype_Order_Generator: theory Native_Word.Bits_Integer
20:58:10 Affine_Arithmetic: theory Show.Show_Instances
20:58:10 Pre_BZ: theory HOL-Word.Misc_set_bit
20:58:10 Deriving: theory Native_Word.Code_Symbolic_Bits_Int
20:58:10 Refine_Monadic: theory Refine_Monadic.Examples
20:58:11 Affine_Arithmetic: theory HOL-Word.Reversed_Bit_Lists
20:58:11 Deriving: theory Native_Word.Bits_Integer
20:58:11 HOL-Word: theory HOL-Word.Misc_lsb
20:58:11 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
20:58:11 WebAssembly: theory Native_Word.Code_Symbolic_Bits_Int
20:58:11 HOL-Word: theory HOL-Word.Misc_msb
20:58:11 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
20:58:11 HOL-Word: theory HOL-Word.Misc_set_bit
20:58:11 Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative
20:58:11 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation
20:58:12 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
20:58:12 Pre_BZ: theory Polynomial_Factorization.Kronecker_Factorization
20:58:12 HOL-Word: theory HOL-Word.Ancient_Numeral
20:58:12 WebAssembly: theory Native_Word.Bits_Integer
20:58:12 Affine_Arithmetic: theory HOL-Library.Interval_Float
20:58:12 Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
20:58:12 Pre_BZ: theory Native_Word.Code_Symbolic_Bits_Int
20:58:12 Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
20:58:12 Functional_Ordered_Resolution_Prover: theory HOL-Word.Reversed_Bit_Lists
20:58:12 Affine_Arithmetic: theory HOL-Word.Misc_lsb
20:58:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate
20:58:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat
20:58:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures
20:58:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat
20:58:13 Pre_BZ: theory Native_Word.Bits_Integer
20:58:13 HOL-Word: theory HOL-Word.More_Word
20:58:13 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
20:58:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
20:58:14 Affine_Arithmetic: theory HOL-Word.Misc_msb
20:58:14 HOL-ODE-Numerics: theory Collections.Assoc_List
20:58:14 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
20:58:14 Affine_Arithmetic: theory HOL-Word.Misc_set_bit
20:58:14 HOL-Word: theory HOL-Word.Word_Examples
20:58:14 HOL-ODE-Numerics: theory Collections.Diff_Array
20:58:15 Pre_BZ: theory Polynomial_Factorization.Rational_Factorization
20:58:15 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
20:58:16 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
20:58:16 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
20:58:16 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
20:58:16 Affine_Arithmetic: theory Native_Word.Code_Symbolic_Bits_Int
20:58:16 HOL-ODE-Numerics: theory Collections.Proper_Iterator
20:58:16 Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_lsb
20:58:16 Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_msb
20:58:16 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
20:58:17 Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_set_bit
20:58:17 Affine_Arithmetic: theory Native_Word.Bits_Integer
20:58:17 HOL-ODE-Numerics: theory Collections.It_to_It
20:58:17 HOL-ODE-Numerics: theory Collections.SetIteratorGA
20:58:18 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
20:58:19 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
20:58:19 HOL-ODE-Numerics: theory HOL-Word.Reversed_Bit_Lists
20:58:20 Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Symbolic_Bits_Int
20:58:20 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking
20:58:21 Functional_Ordered_Resolution_Prover: theory Native_Word.Bits_Integer
20:58:21 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method
20:58:22 HOL-ODE-Numerics: theory HOL-Word.Misc_lsb
20:58:22 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
20:58:23 HOL-ODE-Numerics: theory HOL-Word.Misc_msb
20:58:24 Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting
20:58:24 HOL-ODE-Numerics: theory HOL-Word.Misc_set_bit
20:58:24 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
20:58:24 HOL-ODE-Numerics: theory Collections.Intf_Comp
20:58:27 Affine_Arithmetic: theory Affine_Arithmetic.Intersection
20:58:27 HOL-ODE-Numerics: theory Collections.Idx_Iterator
20:58:28 HOL-ODE-Numerics: theory Native_Word.More_Bits_Int
20:58:28 Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Relative_Rewriting
20:58:28 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching
20:58:28 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification
20:58:28 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
20:58:30 Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Subterm_and_Context
20:58:30 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification
20:58:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
20:58:31 HOL-ODE-Numerics: theory Native_Word.Code_Symbolic_Bits_Int
20:58:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
20:58:32 Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Order_Pair
20:58:32 Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching
20:58:32 HOL-ODE-Numerics: theory Native_Word.Bits_Integer
20:58:32 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
20:58:33 Datatype_Order_Generator: theory Native_Word.Code_Target_Word_Base
20:58:33 Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Lexicographic_Extension
20:58:34 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
20:58:34 Datatype_Order_Generator: theory Native_Word.Uint32
20:58:34 Deriving: theory Native_Word.Code_Target_Word_Base
20:58:35 Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Term_Aux
20:58:35 WebAssembly: theory Native_Word.Code_Target_Word_Base
20:58:35 Deriving: theory Native_Word.Uint32
20:58:36 Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.KBO
20:58:36 WebAssembly: theory Native_Word.Uint8
20:58:37 Pre_BZ: theory Native_Word.Code_Target_Bits_Int
20:58:37 Pre_BZ: theory Native_Word.Code_Target_Word_Base
20:58:37 Datatype_Order_Generator: theory Collections.HashCode
20:58:38 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
20:58:38 Pre_BZ: theory Native_Word.Uint32
20:58:38 Datatype_Order_Generator: theory Datatype_Order_Generator.Hash_Generator
20:58:38 Pre_BZ: theory Native_Word.Uint64
20:58:39 Datatype_Order_Generator: theory Datatype_Order_Generator.Derive
20:58:39 Deriving: theory Collections.HashCode
20:58:39 WebAssembly: theory WebAssembly.Wasm_Ast
20:58:39 Deriving: theory Deriving.Hash_Generator
20:58:40 Datatype_Order_Generator: theory Datatype_Order_Generator.Derive_Examples
20:58:41 Deriving: theory Deriving.Hash_Instances
20:58:41 Deriving: theory Deriving.Derive
20:58:42 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
20:58:42 Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base
20:58:43 Deriving: theory Deriving.Derive_Examples
20:58:43 Affine_Arithmetic: theory Native_Word.Uint32
20:58:46 Affine_Arithmetic: theory Collections.HashCode
20:58:47 Affine_Arithmetic: theory Deriving.Hash_Generator
20:58:47 Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Target_Word_Base
20:58:48 Affine_Arithmetic: theory Deriving.Hash_Instances
20:58:48 Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32
20:58:48 Affine_Arithmetic: theory Deriving.Derive
20:58:49 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
20:58:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
20:58:51 Functional_Ordered_Resolution_Prover: theory Collections.HashCode
20:58:51 HOL-ODE-Numerics: theory Native_Word.Code_Target_Bits_Int
20:58:51 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
20:58:51 Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator
20:58:52 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
20:58:53 Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances
20:58:53 HOL-ODE-Numerics: theory Native_Word.Uint
20:58:53 Functional_Ordered_Resolution_Prover: theory Deriving.Derive
20:58:54 Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
20:58:54 HOL-ODE-Numerics: theory Native_Word.Uint32
20:58:55 Affine_Arithmetic: theory HOL-Library.RBT
20:58:56 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
20:58:56 Affine_Arithmetic: theory HOL-Library.RBT_Mapping
20:58:57 HOL-ODE-Numerics: theory Collections.HashCode
20:58:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
20:58:57 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
20:58:57 HOL-ODE-Numerics: theory Collections.Intf_Hash
20:58:57 HOL-ODE-Numerics: theory Deriving.Hash_Generator
20:58:58 HOL-ODE-Numerics: theory Collections.Gen_Hash
20:58:58 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
20:58:58 HOL-ODE-Numerics: theory HOL-Library.RBT
20:58:58 HOL-ODE-Numerics: theory Deriving.Hash_Instances
20:58:59 HOL-ODE-Numerics: theory Deriving.Derive
20:58:59 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
20:58:59 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
20:58:59 Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
20:59:00 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
20:59:00 HOL-ODE-Numerics: theory Show.Show
20:59:00 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
20:59:00 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
20:59:01 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
20:59:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
20:59:01 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
20:59:01 HOL-ODE-Numerics: theory Show.Show_Instances
20:59:01 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
20:59:02 Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover
20:59:03 WebAssembly: theory WebAssembly.Wasm_Base_Defs
20:59:04 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
20:59:04 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
20:59:05 WebAssembly: theory WebAssembly.Wasm
20:59:05 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
20:59:05 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
20:59:05 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
20:59:06 WebAssembly: theory WebAssembly.Wasm_Axioms
20:59:06 WebAssembly: theory WebAssembly.Wasm_Checker_Types
20:59:06 WebAssembly: theory WebAssembly.Wasm_Interpreter
20:59:06 WebAssembly: theory WebAssembly.Wasm_Properties_Aux
20:59:07 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
20:59:07 WebAssembly: theory WebAssembly.Wasm_Properties
20:59:07 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
20:59:07 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
20:59:07 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
20:59:08 WebAssembly: theory WebAssembly.Wasm_Soundness
20:59:08 Timing HOL-Word (4 threads, 49.607s elapsed time, 153.380s cpu time, 4.104s GC time, factor 3.09)
20:59:08 Finished HOL-Word (0:01:18 elapsed time, 0:03:23 cpu time, factor 2.60)
20:59:08 Running Native_Word ...
20:59:10 Native_Word: theory HOL-Library.Adhoc_Overloading
20:59:10 Native_Word: theory HOL-Library.Code_Target_Int
20:59:10 Native_Word: theory HOL-Library.Nat_Bijection
20:59:10 Native_Word: theory HOL-Library.Code_Test
20:59:10 Native_Word: theory HOL-Library.Monad_Syntax
20:59:10 Native_Word: theory HOL-Library.Old_Datatype
20:59:10 Native_Word: theory Native_Word.More_Bits_Int
20:59:10 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
20:59:11 WebAssembly: theory WebAssembly.Wasm_Checker
20:59:11 Native_Word: theory HOL-Library.Countable
20:59:12 HOL-ODE-Numerics: theory Collections.Gen_Iterator
20:59:12 Native_Word: theory Native_Word.Code_Symbolic_Bits_Int
20:59:13 HOL-ODE-Numerics: theory Collections.Iterator
20:59:13 Native_Word: theory Native_Word.Bits_Integer
20:59:13 Native_Word: theory HOL-Imperative_HOL.Heap
20:59:14 HOL-ODE-Numerics: theory Collections.Array_Iterator
20:59:14 HOL-ODE-Numerics: theory Collections.RBT_add
20:59:16 Native_Word: theory HOL-Imperative_HOL.Heap_Monad
20:59:16 HOL-ODE-Numerics: theory Collections.Intf_Map
20:59:16 WebAssembly: theory WebAssembly.Wasm_Interpreter_Properties
20:59:17 HOL-ODE-Numerics: theory Collections.Gen_Map
20:59:18 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
20:59:18 WebAssembly: theory WebAssembly.Wasm_Checker_Properties
20:59:18 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
20:59:19 HOL-ODE-Numerics: theory Collections.Impl_List_Map
20:59:20 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
20:59:21 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
20:59:22 HOL-ODE-Numerics: theory Collections.Intf_Set
20:59:22 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
20:59:23 HOL-ODE-Numerics: theory Collections.Gen_Set
20:59:25 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
20:59:26 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
20:59:26 HOL-ODE-Numerics: theory Collections.Impl_List_Set
20:59:26 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
20:59:27 Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
20:59:28 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
20:59:29 Native_Word: theory Native_Word.Code_Target_Bits_Int
20:59:29 Native_Word: theory Native_Word.Code_Target_Word_Base
20:59:30 Native_Word: theory Native_Word.Uint
20:59:31 Native_Word: theory Native_Word.Uint16
20:59:32 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
20:59:32 Native_Word: theory Native_Word.Uint32
20:59:33 Native_Word: theory Native_Word.Uint64
20:59:33 Native_Word: theory Native_Word.Uint8
20:59:34 Native_Word: theory Native_Word.Native_Word_Imperative_HOL
20:59:36 Native_Word: theory Native_Word.Native_Cast
20:59:36 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
20:59:36 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
20:59:36 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
20:59:37 Native_Word: theory Native_Word.Native_Cast_Uint
20:59:38 Native_Word: theory Native_Word.Native_Word_Test
20:59:44 Timing Deriving (4 threads, 69.833s elapsed time, 196.540s cpu time, 6.676s GC time, factor 2.81)
20:59:44 Finished Deriving (0:01:53 elapsed time, 0:05:28 cpu time, factor 2.89)
20:59:44 Timing Refine_Monadic (4 threads, 77.027s elapsed time, 212.724s cpu time, 7.324s GC time, factor 2.76)
20:59:44 Finished Refine_Monadic (0:01:54 elapsed time, 0:04:35 cpu time, factor 2.41)
20:59:44 Building Collections ...
20:59:45 Building LEM ...
20:59:47 LEM: theory HOL-Library.While_Combinator
20:59:47 LEM: theory HOL-Library.Cancellation
20:59:47 LEM: theory LEM.Lem_bool
20:59:47 LEM: theory LEM.Lem_basic_classes
20:59:48 Collections: theory Collections.ICF_Tools
20:59:48 Collections: theory Collections.Partial_Equivalence_Relation
20:59:48 Collections: theory HOL-Library.AList
20:59:48 Collections: theory Finger-Trees.FingerTree
20:59:48 Collections: theory Binomial-Heaps.BinomialHeap
20:59:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
20:59:48 Collections: theory Collections.Ord_Code_Preproc
20:59:48 Collections: theory Collections.Locale_Code
20:59:48 Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
20:59:49 LEM: theory HOL-Library.Multiset
20:59:49 Collections: theory Collections.Record_Intf
20:59:49 Collections: theory Binomial-Heaps.SkewBinomialHeap
20:59:51 Collections: theory HOL-Library.Code_Abstract_Nat
20:59:51 Collections: theory HOL-Library.Code_Target_Nat
20:59:51 Collections: theory HOL-Library.Code_Target_Int
20:59:51 Collections: theory HOL-Library.Code_Target_Numeral
20:59:52 Collections: theory HOL-Library.Confluence
20:59:52 Collections: theory HOL-Library.Confluent_Quotient
20:59:52 Collections: theory HOL-Library.Dlist
20:59:54 Collections: theory Collections.SetIterator
20:59:54 Collections: theory Collections.Sorted_List_Operations
20:59:56 Collections: theory HOL-Library.RBT_Impl
20:59:56 LEM: theory LEM.Lem_function
20:59:56 LEM: theory LEM.Lem_num
20:59:56 LEM: theory LEM.Lem_tuple
20:59:56 LEM: theory LEM.Lem_maybe
20:59:56 Collections: theory Collections.Idx_Iterator
20:59:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
20:59:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
20:59:57 LEM: theory HOL-Library.Permutation
20:59:57 LEM: theory LEM.LemExtraDefs
20:59:57 Collections: theory Collections.SetAbstractionIterator
20:59:58 Collections: theory Collections.SetIteratorOperations
21:00:00 LEM: theory LEM.Lem
21:00:01 LEM: theory LEM.Lem_assert_extra
21:00:01 LEM: theory LEM.Lem_maybe_extra
21:00:02 Collections: theory Collections.Assoc_List
21:00:03 Collections: theory Collections.Diff_Array
21:00:06 LEM: theory LEM.Lem_list
21:00:06 LEM: theory LEM.Lem_set_helpers
21:00:06 LEM: theory LEM.Lem_function_extra
21:00:06 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
21:00:06 Collections: theory Collections.Dlist_add
21:00:07 Collections: theory Collections.Proper_Iterator
21:00:07 Collections: theory Collections.SetIteratorGA
21:00:07 Collections: theory Collections.It_to_It
21:00:08 Collections: theory Collections.DatRef
21:00:09 Collections: theory HOL-Word.Reversed_Bit_Lists
21:00:09 Collections: theory Native_Word.More_Bits_Int
21:00:11 Collections: theory HOL-Word.Misc_lsb
21:00:11 LEM: theory LEM.Lem_sorting
21:00:11 LEM: theory LEM.Lem_string
21:00:11 LEM: theory LEM.Lem_set
21:00:11 LEM: theory LEM.Lem_either
21:00:11 WebAssembly: theory WebAssembly.Wasm_Checker_Printing
21:00:11 WebAssembly: theory WebAssembly.Wasm_Type_Abs_Printing
21:00:11 WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing
21:00:11 Collections: theory HOL-Word.Misc_msb
21:00:11 WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing_Pure
21:00:11 WebAssembly: theory WebAssembly.Wasm_Printing
21:00:11 LEM: theory LEM.Lem_num_extra
21:00:11 Collections: theory HOL-Word.Misc_set_bit
21:00:11 LEM: theory LEM.Lem_show
21:00:11 LEM: theory LEM.Lem_list_extra
21:00:11 LEM: theory LEM.Lem_word
21:00:12 LEM: theory LEM.Lem_set_extra
21:00:12 LEM: theory LEM.Lem_map
21:00:12 LEM: theory LEM.Lem_map_extra
21:00:12 Collections: theory Collections.Gen_Iterator
21:00:12 LEM: theory LEM.Lem_machine_word
21:00:13 LEM: theory LEM.Lem_relation
21:00:13 Collections: theory Collections.Iterator
21:00:13 LEM: theory LEM.Lem_string_extra
21:00:14 Collections: theory Native_Word.Code_Symbolic_Bits_Int
21:00:14 Collections: theory Collections.ICF_Spec_Base
21:00:14 LEM: theory LEM.Lem_show_extra
21:00:14 Collections: theory Native_Word.Bits_Integer
21:00:14 Collections: theory Collections.MapSpec
21:00:15 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
21:00:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
21:00:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
21:00:19 Affine_Arithmetic: theory Affine_Arithmetic.Print
21:00:19 Collections: theory Collections.Robdd
21:00:19 LEM: theory LEM.Lem_pervasives
21:00:21 LEM: theory LEM.Lem_pervasives_extra
21:00:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
21:00:22 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
21:00:22 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
21:00:22 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
21:00:23 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
21:00:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
21:00:24 Timing WebAssembly (4 threads, 145.179s elapsed time, 450.512s cpu time, 12.400s GC time, factor 3.10)
21:00:24 Finished WebAssembly (0:02:34 elapsed time, 0:08:44 cpu time, factor 3.40)
21:00:24 Building Word_Lib ...
21:00:25 Word_Lib: theory HOL-Eisbach.Eisbach
21:00:25 Word_Lib: theory HOL-Library.Sublist
21:00:25 Word_Lib: theory Word_Lib.Hex_Words
21:00:25 Word_Lib: theory Word_Lib.Bitwise
21:00:25 Word_Lib: theory Word_Lib.Signed_Words
21:00:26 Word_Lib: theory Word_Lib.Norm_Words
21:00:26 Word_Lib: theory Word_Lib.Word_Type_Syntax
21:00:26 Word_Lib: theory Word_Lib.Enumeration
21:00:27 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
21:00:27 Word_Lib: theory Word_Lib.Examples
21:00:27 Word_Lib: theory Word_Lib.Bitwise_Signed
21:00:27 Word_Lib: theory Word_Lib.HOL_Lemmas
21:00:27 Word_Lib: theory Word_Lib.More_Divides
21:00:27 Word_Lib: theory Word_Lib.Word_Syntax
21:00:28 Word_Lib: theory Word_Lib.Word_Lib
21:00:30 Word_Lib: theory Word_Lib.Word_Enum
21:00:30 Word_Lib: theory Word_Lib.Aligned
21:00:31 Word_Lib: theory Word_Lib.Word_Setup_32
21:00:31 Word_Lib: theory Word_Lib.Word_Setup_64
21:00:31 Word_Lib: theory Word_Lib.Word_Next
21:00:31 Word_Lib: theory Word_Lib.Word_EqI
21:00:31 Collections: theory Native_Word.Code_Target_Bits_Int
21:00:31 Collections: theory Native_Word.Code_Target_Word_Base
21:00:32 Collections: theory Collections.Code_Target_ICF
21:00:32 Collections: theory Collections.Locale_Code_Ex
21:00:32 Collections: theory Native_Word.Uint32
21:00:34 Word_Lib: theory Word_Lib.Word_Lemmas
21:00:34 Collections: theory Collections.HashCode
21:00:39 Word_Lib: theory Word_Lib.Word_Lemmas_32
21:00:40 Word_Lib: theory Word_Lib.Word_Lemmas_64
21:00:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
21:00:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
21:00:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
21:00:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
21:00:46 Collections: theory Collections.RBT_add
21:00:52 Timing LEM (4 threads, 35.804s elapsed time, 97.060s cpu time, 5.496s GC time, factor 2.71)
21:00:52 Finished LEM (0:01:05 elapsed time, 0:02:25 cpu time, factor 2.21)
21:00:52 Building CakeML ...
21:00:54 CakeML: theory HOL-Eisbach.Eisbach
21:00:54 CakeML: theory Deriving.Derive_Manager
21:00:54 CakeML: theory CakeML.Doc_Generated
21:00:54 CakeML: theory CakeML.Doc_Proofs
21:00:54 CakeML: theory Deriving.Generator_Aux
21:00:54 CakeML: theory HOL-Library.Case_Converter
21:00:54 CakeML: theory HOL-Library.Datatype_Records
21:00:55 CakeML: theory HOL-Library.Infinite_Set
21:00:55 CakeML: theory HOL-Library.Simps_Case_Conv
21:00:55 CakeML: theory HOL-Library.Lattice_Syntax
21:00:55 CakeML: theory HOL-Library.Nat_Bijection
21:00:55 CakeML: theory HOL-Library.Complete_Partial_Order2
21:00:55 CakeML: theory HOL-Library.Old_Datatype
21:00:56 CakeML: theory HOL-Eisbach.Eisbach_Tools
21:00:56 CakeML: theory HOL-Library.Sublist
21:00:56 CakeML: theory Word_Lib.Bitwise
21:00:56 CakeML: theory Word_Lib.Hex_Words
21:00:56 CakeML: theory Word_Lib.Signed_Words
21:00:57 CakeML: theory Word_Lib.Norm_Words
21:00:57 CakeML: theory Word_Lib.Word_Type_Syntax
21:00:57 CakeML: theory HOL-Library.Countable
21:00:57 CakeML: theory Word_Lib.Bitwise_Signed
21:00:57 CakeML: theory Word_Lib.Word_Syntax
21:00:58 CakeML: theory HOL-Library.Lattice_Algebras
21:00:58 CakeML: theory Word_Lib.Word_Lib
21:00:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
21:00:59 CakeML: theory HOL-Library.Countable_Set
21:01:00 CakeML: theory HOL-Library.Log_Nat
21:01:00 CakeML: theory CakeML.Namespace
21:01:00 CakeML: theory CakeML.Tokens
21:01:00 CakeML: theory HOL-Library.Countable_Complete_Lattices
21:01:01 Timing Pre_BZ (4 threads, 128.369s elapsed time, 384.564s cpu time, 12.192s GC time, factor 3.00)
21:01:01 Finished Pre_BZ (0:03:10 elapsed time, 0:09:03 cpu time, factor 2.86)
21:01:01 Building Containers ...
21:01:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
21:01:03 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
21:01:03 Containers: theory Containers.Equal
21:01:03 Containers: theory Containers.Extend_Partial_Order
21:01:03 Containers: theory Containers.List_Fusion
21:01:03 Containers: theory Containers.AssocList
21:01:03 Containers: theory Containers.Closure_Set
21:01:03 Containers: theory Containers.Containers_Auxiliary
21:01:04 Containers: theory Containers.Card_Datatype
21:01:04 Containers: theory Regular-Sets.Regular_Set
21:01:04 Containers: theory Containers.Containers_Generator
21:01:04 CakeML: theory HOL-Library.Order_Continuity
21:01:05 Containers: theory Containers.Collection_Enum
21:01:05 Containers: theory Containers.Collection_Eq
21:01:05 CakeML: theory HOL-Library.Extended_Nat
21:01:06 Containers: theory Containers.Lexicographic_Order
21:01:06 Containers: theory Containers.DList_Set
21:01:06 Containers: theory Containers.RBT_ext
21:01:06 CakeML: theory HOL-Library.Float
21:01:06 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
21:01:06 Containers: theory Containers.Set_Linorder
21:01:07 CakeML: theory Coinductive.Coinductive_Nat
21:01:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
21:01:08 CakeML: theory Coinductive.Coinductive_List
21:01:08 Containers: theory Regular-Sets.Regular_Exp
21:01:08 CakeML: theory CakeML.NamespaceAuxiliary
21:01:08 CakeML: theory Show.Show
21:01:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
21:01:10 CakeML: theory Word_Lib.Enumeration
21:01:10 CakeML: theory Show.Show_Instances
21:01:10 CakeML: theory Word_Lib.Word_Enum
21:01:11 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
21:01:13 CakeML: theory Word_Lib.Word_Setup_64
21:01:13 CakeML: theory Word_Lib.HOL_Lemmas
21:01:13 Containers: theory Regular-Sets.NDerivative
21:01:13 Containers: theory Regular-Sets.Relation_Interpretation
21:01:13 CakeML: theory Word_Lib.More_Divides
21:01:13 CakeML: theory Word_Lib.Aligned
21:01:14 CakeML: theory Word_Lib.Word_Next
21:01:14 CakeML: theory Word_Lib.Word_EqI
21:01:18 CakeML: theory Word_Lib.Word_Lemmas
21:01:18 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
21:01:18 Containers: theory Regular-Sets.Equivalence_Checking
21:01:18 Containers: theory Regular-Sets.Regexp_Method
21:01:19 CakeML: theory CakeML.Lib
21:01:20 Containers: theory Containers.Collection_Order
21:01:23 Timing Word_Lib (4 threads, 30.697s elapsed time, 114.776s cpu time, 3.560s GC time, factor 3.74)
21:01:23 Finished Word_Lib (0:00:57 elapsed time, 0:02:40 cpu time, factor 2.78)
21:01:23 Building IP_Addresses ...
21:01:23 Containers: theory Containers.List_Proper_Interval
21:01:23 CakeML: theory IEEE_Floating_Point.IEEE
21:01:23 CakeML: theory Word_Lib.Word_Lemmas_64
21:01:24 Containers: theory Containers.RBT_Mapping2
21:01:24 CakeML: theory CakeML.LibAuxiliary
21:01:24 CakeML: theory CakeML.Ffi
21:01:25 IP_Addresses: theory HOL-Library.Option_ord
21:01:25 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
21:01:25 IP_Addresses: theory HOL-Library.Infinite_Set
21:01:25 IP_Addresses: theory HOL-Library.Cancellation
21:01:25 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
21:01:26 IP_Addresses: theory HOL-Library.Multiset
21:01:26 Containers: theory Containers.RBT_Set2
21:01:28 Containers: theory Containers.Set_Impl
21:01:28 CakeML: theory IEEE_Floating_Point.FP64
21:01:29 CakeML: theory CakeML.FpSem
21:01:33 IP_Addresses: theory HOL-ex.Quicksort
21:01:34 IP_Addresses: theory Automatic_Refinement.Misc
21:01:34 CakeML: theory CakeML.Ast
21:01:35 CakeML: theory CakeML.SimpleIO
21:01:44 IP_Addresses: theory HOL-Library.Product_Lexorder
21:01:44 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
21:01:44 IP_Addresses: theory IP_Addresses.Hs_Compat
21:01:44 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
21:01:44 IP_Addresses: theory IP_Addresses.WordInterval
21:01:44 IP_Addresses: theory HOL-Library.Code_Target_Nat
21:01:44 IP_Addresses: theory IP_Addresses.Lib_List_toString
21:01:44 IP_Addresses: theory IP_Addresses.Lib_Word_toString
21:01:47 Collections: theory Collections.GenCF_Chapter
21:01:47 Collections: theory Collections.GenCF_Gen_Chapter
21:01:47 Collections: theory Collections.GenCF_Impl_Chapter
21:01:47 Collections: theory Collections.GenCF_Intf_Chapter
21:01:47 Collections: theory Collections.Intf_Comp
21:01:47 Collections: theory Collections.Impl_Array_Stack
21:01:47 Collections: theory HOL-Library.Product_Lexorder
21:01:47 Collections: theory Collections.Intf_Hash
21:01:47 Collections: theory Collections.Array_Iterator
21:01:47 Collections: theory Collections.Intf_Map
21:01:47 Collections: theory Collections.Intf_Set
21:01:47 Containers: theory Containers.Mapping_Impl
21:01:48 Collections: theory Collections.Gen_Map
21:01:48 Collections: theory Collections.Gen_Set
21:01:48 Collections: theory Collections.Impl_Cfun_Set
21:01:48 Collections: theory Collections.Impl_List_Set
21:01:49 Collections: theory Collections.Gen_Comp
21:01:49 Collections: theory Collections.Impl_Array_Map
21:01:49 IP_Addresses: theory IP_Addresses.IP_Address
21:01:49 Collections: theory Collections.Impl_List_Map
21:01:49 Collections: theory Collections.Impl_RBT_Map
21:01:50 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
21:01:50 Collections: theory Collections.Gen_Map2Set
21:01:50 Collections: theory Collections.Impl_Array_Hash_Map
21:01:51 Containers: theory Containers.Map_To_Mapping
21:01:51 Containers: theory Containers.Containers
21:01:51 Containers: theory Containers.Containers_Userguide
21:01:51 Containers: theory Containers.Compatibility_Containers_Regular_Sets
21:01:56 IP_Addresses: theory IP_Addresses.IPv4
21:01:56 IP_Addresses: theory IP_Addresses.IPv6
21:01:56 IP_Addresses: theory IP_Addresses.Prefix_Match
21:01:57 IP_Addresses: theory IP_Addresses.CIDR_Split
21:02:10 CakeML: theory CakeML.CakeML_Compiler
21:02:10 CakeML: theory CakeML.AstAuxiliary
21:02:10 CakeML: theory CakeML.SemanticPrimitives
21:02:11 Collections: theory Collections.Gen_Hash
21:02:11 Collections: theory Collections.Impl_Bit_Set
21:02:11 Collections: theory Native_Word.Uint
21:02:13 Collections: theory Collections.Impl_Uv_Set
21:02:24 Containers: theory Containers.Card_Datatype_Ex
21:02:24 Containers: theory Containers.TwoSat_Ex
21:02:24 Containers: theory Containers.Containers_DFS_Ex
21:02:24 Containers: theory Containers.Map_To_Mapping_Ex
21:02:27 Containers: theory Containers.Containers_TwoSat_Ex
21:02:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
21:02:30 Collections: theory Collections.GenCF
21:02:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
21:02:33 Timing Functional_Ordered_Resolution_Prover (4 threads, 273.772s elapsed time, 617.060s cpu time, 39.948s GC time, factor 2.25)
21:02:33 Finished Functional_Ordered_Resolution_Prover (0:04:42 elapsed time, 0:11:36 cpu time, factor 2.47)
21:02:33 Building Berlekamp_Zassenhaus ...
21:02:36 Collections: theory Collections.ICF_Chapter
21:02:36 Collections: theory Collections.ICF_Gen_Algo_Chapter
21:02:36 Collections: theory Collections.ICF_Impl_Chapter
21:02:36 Collections: theory Collections.ICF_Spec_Chapter
21:02:36 Collections: theory Trie.Trie
21:02:36 Collections: theory HOL-Library.RBT
21:02:36 Collections: theory Collections.ListSpec
21:02:36 Collections: theory Collections.AnnotatedListSpec
21:02:37 Collections: theory Collections.PrioSpec
21:02:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Missing_Multiset2
21:02:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
21:02:37 Berlekamp_Zassenhaus: theory HOL-Word.Misc_Arithmetic
21:02:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
21:02:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
21:02:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
21:02:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
21:02:39 Collections: theory Collections.BinoPrioImpl
21:02:39 Collections: theory Collections.ListGA
21:02:39 Collections: theory Collections.Trie_Impl
21:02:39 Collections: theory Collections.FTAnnotatedListImpl
21:02:40 Collections: theory Collections.Trie2
21:02:40 Collections: theory Collections.Fifo
21:02:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
21:02:40 Collections: theory Collections.PrioByAnnotatedList
21:02:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
21:02:42 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
21:02:43 Collections: theory Collections.SkewPrioImpl
21:02:43 Collections: theory Collections.PrioUniqueSpec
21:02:44 Collections: theory Collections.SetSpec
21:02:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
21:02:45 Collections: theory Collections.PrioUniqueByAnnotatedList
21:02:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
21:02:46 Collections: theory Collections.FTPrioImpl
21:02:48 Collections: theory Collections.FTPrioUniqueImpl
21:02:49 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
21:02:50 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
21:02:50 Collections: theory Collections.Algos
21:02:50 Collections: theory Collections.SetIndex
21:02:51 Collections: theory Collections.SetIteratorCollectionsGA
21:02:51 Collections: theory Collections.MapGA
21:02:51 Collections: theory Collections.SetGA
21:02:54 Collections: theory Collections.ArrayMapImpl
21:02:54 Collections: theory Collections.ListMapImpl
21:02:54 Collections: theory Collections.ListMapImpl_Invar
21:02:57 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
21:02:57 Collections: theory Collections.TrieMapImpl
21:02:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
21:02:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
21:02:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
21:02:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
21:02:59 Collections: theory Collections.ArrayHashMap_Impl
21:03:00 CakeML: theory CakeML.CakeML_Quickcheck
21:03:00 CakeML: theory CakeML.Evaluate
21:03:00 CakeML: theory CakeML.SmallStep
21:03:00 CakeML: theory CakeML.TypeSystem
21:03:00 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
21:03:00 Collections: theory Collections.ListSetImpl
21:03:00 Collections: theory Collections.ListSetImpl_Invar
21:03:02 Collections: theory Collections.ListSetImpl_NotDist
21:03:04 Collections: theory Collections.ArrayHashMap
21:03:04 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
21:03:06 Collections: theory Collections.ListSetImpl_Sorted
21:03:07 Collections: theory Collections.SetByMap
21:03:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
21:03:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
21:03:08 CakeML: theory CakeML.BigStep
21:03:08 Collections: theory Collections.RBTMapImpl
21:03:09 Collections: theory Collections.ArraySetImpl
21:03:10 CakeML: theory CakeML.PrimTypes
21:03:11 Collections: theory Collections.ArrayHashSet
21:03:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
21:03:13 CakeML: theory CakeML.BigSmallInvariants
21:03:13 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
21:03:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
21:03:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
21:03:13 CakeML: theory CakeML.SemanticPrimitivesAuxiliary
21:03:14 Collections: theory Collections.TrieSetImpl
21:03:14 CakeML: theory CakeML.Semantic_Extras
21:03:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
21:03:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
21:03:17 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
21:03:17 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
21:03:17 Collections: theory Collections.HashMap_Impl
21:03:17 Collections: theory Collections.RBTSetImpl
21:03:18 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
21:03:20 Collections: theory Collections.HashMap
21:03:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
21:03:21 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
21:03:24 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
21:03:24 IP_Addresses: theory IP_Addresses.IP_Address_Parser
21:03:25 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
21:03:26 Collections: theory Collections.HashSet
21:03:26 Collections: theory Collections.MapStdImpl
21:03:27 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
21:03:30 Timing Datatype_Order_Generator (4 threads, 224.381s elapsed time, 583.160s cpu time, 80.128s GC time, factor 2.60)
21:03:30 Finished Datatype_Order_Generator (0:05:40 elapsed time, 0:14:13 cpu time, factor 2.51)
21:03:30 Running Complx ...
21:03:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
21:03:32 Complx: theory Complx.Cache_Tactics
21:03:32 Complx: theory Complx.Language
21:03:32 Collections: theory Collections.SetStdImpl
21:03:33 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
21:03:34 CakeML: theory CakeML.TypeSystemAuxiliary
21:03:35 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
21:03:35 CakeML: theory CakeML.Big_Step_Determ
21:03:35 CakeML: theory CakeML.Big_Step_Total
21:03:36 CakeML: theory CakeML.Big_Step_Clocked
21:03:37 Complx: theory Complx.SmallStep
21:03:37 CakeML: theory CakeML.Big_Step_Unclocked
21:03:37 Collections: theory Collections.ICF_Impl
21:03:37 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
21:03:38 CakeML: theory CakeML.Evaluate_Termination
21:03:39 CakeML: theory CakeML.Matching
21:03:39 CakeML: theory CakeML.Evaluate_Clock
21:03:39 CakeML: theory CakeML.Big_Step_Fun_Equiv
21:03:39 IP_Addresses: theory IP_Addresses.IP_Address_toString
21:03:40 CakeML: theory CakeML.Evaluate_Single
21:03:41 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
21:03:42 Collections: theory Collections.ICF_Refine_Monadic
21:03:43 Collections: theory Collections.ICF_Autoref
21:03:43 CakeML: theory CakeML.Big_Step_Unclocked_Single
21:03:46 Complx: theory Complx.OG_Annotations
21:03:46 Complx: theory Complx.SeqCatch_decomp
21:03:47 Collections: theory Collections.Collections_Entrypoints_Chapter
21:03:47 Collections: theory Collections.ICF_Entrypoints_Chapter
21:03:47 Collections: theory Collections.Userguides_Chapter
21:03:47 Collections: theory Collections.Collections
21:03:48 Collections: theory Collections.Refine_Dflt
21:03:48 Collections: theory Collections.CollectionsV1
21:03:48 Collections: theory Collections.ICF_Userguide
21:03:48 Collections: theory Collections.Refine_Dflt_ICF
21:03:49 Collections: theory Collections.Refine_Dflt_Only_ICF
21:03:49 Collections: theory Collections.Refine_Monadic_Userguide
21:03:50 Complx: theory Complx.OG_Hoare
21:03:50 CakeML: theory CakeML.CakeML_Code
21:03:53 Complx: theory Complx.OG_Soundness
21:03:54 Complx: theory Complx.OG_Tactics
21:03:56 Complx: theory Complx.OG_Syntax
21:03:57 Complx: theory Complx.Examples
21:03:57 Complx: theory Complx.SumArr
21:04:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
21:04:28 Timing Containers (4 threads, 140.330s elapsed time, 316.724s cpu time, 19.904s GC time, factor 2.26)
21:04:28 Finished Containers (0:03:25 elapsed time, 0:10:00 cpu time, factor 2.92)
21:04:28 Running MFODL_Monitor_Optimized ...
21:04:31 MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach
21:04:31 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Trace
21:04:31 MFODL_Monitor_Optimized: theory Word_Lib.Hex_Words
21:04:31 MFODL_Monitor_Optimized: theory HOL-Word.Misc_Arithmetic
21:04:31 MFODL_Monitor_Optimized: theory Word_Lib.Signed_Words
21:04:31 MFODL_Monitor_Optimized: theory Word_Lib.Norm_Words
21:04:31 MFODL_Monitor_Optimized: theory Word_Lib.Word_Type_Syntax
21:04:31 MFODL_Monitor_Optimized: theory Word_Lib.Bitwise
21:04:31 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Interval
21:04:32 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Regex
21:04:32 MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach_Tools
21:04:32 MFODL_Monitor_Optimized: theory MFOTL_Monitor.Table
21:04:33 MFODL_Monitor_Optimized: theory Word_Lib.Enumeration
21:04:33 MFODL_Monitor_Optimized: theory Word_Lib.Bitwise_Signed
21:04:33 MFODL_Monitor_Optimized: theory Word_Lib.Word_Syntax
21:04:33 MFODL_Monitor_Optimized: theory Word_Lib.HOL_Lemmas
21:04:33 MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join
21:04:34 MFODL_Monitor_Optimized: theory Word_Lib.More_Divides
21:04:34 MFODL_Monitor_Optimized: theory Word_Lib.Word_Lib
21:04:35 MFODL_Monitor_Optimized: theory Word_Lib.Word_Enum
21:04:36 MFODL_Monitor_Optimized: theory Word_Lib.Aligned
21:04:37 MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join_Correctness
21:04:37 MFODL_Monitor_Optimized: theory Word_Lib.Word_Next
21:04:37 MFODL_Monitor_Optimized: theory Word_Lib.Word_EqI
21:04:38 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_Join
21:04:40 MFODL_Monitor_Optimized: theory Word_Lib.Word_Lemmas
21:04:45 MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE
21:04:49 MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE_Properties
21:04:49 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Code_Double
21:04:52 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Event_Data
21:04:56 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Formula
21:05:44 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Abstract_Monitor
21:05:45 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor
21:05:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
21:06:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC
21:06:15 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton
21:06:19 Timing Berlekamp_Zassenhaus (4 threads, 121.484s elapsed time, 425.288s cpu time, 16.896s GC time, factor 3.50)
21:06:19 Finished Berlekamp_Zassenhaus (0:03:44 elapsed time, 0:09:55 cpu time, factor 2.65)
21:06:21 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml
21:06:22 Timing Affine_Arithmetic (4 threads, 390.316s elapsed time, 1301.732s cpu time, 103.756s GC time, factor 3.34)
21:06:22 Finished Affine_Arithmetic (0:08:30 elapsed time, 0:26:17 cpu time, factor 3.09)
21:06:22 Running Algebraic_Numbers ...
21:06:22 Running Linear_Recurrences_Solver ...
21:06:22 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ
21:06:24 Timing HOL-Codegenerator_Test (4 threads, 512.662s elapsed time, 839.496s cpu time, 41.860s GC time, factor 1.64)
21:06:24 Finished HOL-Codegenerator_Test (0:08:35 elapsed time, 0:50:33 cpu time, factor 5.89)
21:06:24 Building Kleene_Algebra ...
21:06:26 Kleene_Algebra: theory Kleene_Algebra.Signatures
21:06:26 Kleene_Algebra: theory Kleene_Algebra.Dioid
21:06:32 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_MTL
21:06:34 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
21:06:34 Linear_Recurrences_Solver: theory Deriving.Compare_Real
21:06:34 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
21:06:34 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
21:06:34 Algebraic_Numbers: theory Deriving.Compare_Rat
21:06:34 Algebraic_Numbers: theory Deriving.Compare_Real
21:06:34 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
21:06:34 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
21:06:34 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
21:06:34 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
21:06:34 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
21:06:34 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
21:06:34 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
21:06:34 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
21:06:34 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
21:06:34 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
21:06:34 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
21:06:35 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
21:06:35 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
21:06:35 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
21:06:35 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
21:06:35 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
21:06:36 Algebraic_Numbers: theory Show.Show_Real
21:06:36 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
21:06:36 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
21:06:36 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
21:06:36 Algebraic_Numbers: theory Show.Show_Complex
21:06:37 Linear_Recurrences_Solver: theory Show.Show_Real
21:06:37 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
21:06:37 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
21:06:37 Linear_Recurrences_Solver: theory Show.Show_Complex
21:06:37 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
21:06:38 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
21:06:38 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
21:06:38 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
21:06:39 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
21:06:39 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
21:06:39 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
21:06:39 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
21:06:40 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
21:06:41 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
21:06:41 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
21:06:41 Kleene_Algebra: theory Kleene_Algebra.Conway
21:06:41 Kleene_Algebra: theory Kleene_Algebra.Dioid_Models
21:06:41 Kleene_Algebra: theory Kleene_Algebra.Finite_Suprema
21:06:41 Kleene_Algebra: theory Kleene_Algebra.Matrix
21:06:41 Kleene_Algebra: theory Kleene_Algebra.Inf_Matrix
21:06:43 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
21:06:46 Timing Collections (4 threads, 271.917s elapsed time, 707.348s cpu time, 57.520s GC time, factor 2.60)
21:06:46 Finished Collections (0:06:56 elapsed time, 0:24:14 cpu time, factor 3.49)
21:06:46 Building CAVA_Base ...
21:06:47 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
21:06:48 CAVA_Base: theory CAVA_Base.Lexord_List
21:06:48 CAVA_Base: theory CAVA_Base.Statistics
21:06:48 CAVA_Base: theory Deriving.Comparator
21:06:48 CAVA_Base: theory Deriving.Derive_Manager
21:06:49 CAVA_Base: theory Deriving.Generator_Aux
21:06:49 CAVA_Base: theory HOL-Library.Char_ord
21:06:49 CAVA_Base: theory HOL-Library.Nat_Bijection
21:06:49 CAVA_Base: theory HOL-Library.Old_Datatype
21:06:49 CAVA_Base: theory Deriving.Equality_Generator
21:06:50 CAVA_Base: theory Deriving.Hash_Generator
21:06:50 CAVA_Base: theory Deriving.Equality_Instances
21:06:50 CAVA_Base: theory HOL-Library.Countable
21:06:50 CAVA_Base: theory Deriving.Compare
21:06:50 CAVA_Base: theory Deriving.Comparator_Generator
21:06:51 CAVA_Base: theory Deriving.Hash_Instances
21:06:51 CAVA_Base: theory CAVA_Base.Code_String
21:06:51 CAVA_Base: theory CAVA_Base.CAVA_Code_Target
21:06:51 CAVA_Base: theory Deriving.Compare_Generator
21:06:51 CAVA_Base: theory CAVA_Base.CAVA_Base
21:06:52 CAVA_Base: theory Deriving.Compare_Instances
21:06:52 CAVA_Base: theory Deriving.Countable_Generator
21:06:52 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Impl
21:06:52 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra
21:06:53 CAVA_Base: theory Deriving.Derive
21:06:53 CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base
21:06:58 Timing IP_Addresses (4 threads, 274.340s elapsed time, 849.092s cpu time, 43.628s GC time, factor 3.10)
21:06:58 Finished IP_Addresses (0:05:34 elapsed time, 0:16:04 cpu time, factor 2.88)
21:06:58 Building Simple_Firewall ...
21:07:00 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
21:07:00 Simple_Firewall: theory Simple_Firewall.GroupF
21:07:00 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
21:07:00 Simple_Firewall: theory HOL-Library.Char_ord
21:07:00 Simple_Firewall: theory Simple_Firewall.Iface
21:07:01 Kleene_Algebra: theory Kleene_Algebra.DRA
21:07:01 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra
21:07:01 Kleene_Algebra: theory Kleene_Algebra.PHL_KA
21:07:01 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra_Models
21:07:02 Kleene_Algebra: theory Kleene_Algebra.Formal_Power_Series
21:07:02 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
21:07:02 Kleene_Algebra: theory Kleene_Algebra.PHL_DRA
21:07:03 Simple_Firewall: theory Simple_Firewall.L4_Protocol
21:07:03 Simple_Firewall: theory Simple_Firewall.List_Product_More
21:07:03 Simple_Firewall: theory Simple_Firewall.Option_Helpers
21:07:03 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
21:07:06 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
21:07:07 Simple_Firewall: theory Simple_Firewall.Simple_Packet
21:07:07 Simple_Firewall: theory Simple_Firewall.Primitives_toString
21:07:07 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
21:07:07 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra_Models
21:07:08 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
21:07:08 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
21:07:08 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
21:07:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
21:07:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
21:07:10 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
21:07:10 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
21:07:11 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
21:07:13 Algebraic_Numbers: theory Algebraic_Numbers.Real_Factorization
21:07:13 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
21:07:14 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
21:07:14 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
21:07:16 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
21:07:16 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
21:07:17 Simple_Firewall: theory Simple_Firewall.Shadowed
21:07:17 Simple_Firewall: theory Simple_Firewall.Service_Matrix
21:07:22 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
21:07:23 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
21:07:31 Timing CAVA_Base (4 threads, 16.359s elapsed time, 46.080s cpu time, 1.284s GC time, factor 2.82)
21:07:31 Finished CAVA_Base (0:00:44 elapsed time, 0:01:28 cpu time, factor 1.98)
21:07:31 Building CAVA_Automata ...
21:07:33 CAVA_Automata: theory CAVA_Automata.Step_Conv
21:07:33 CAVA_Automata: theory HOL-Library.Omega_Words_Fun
21:07:34 CakeML: theory CakeML.Compiler_Test
21:07:34 CAVA_Automata: theory CAVA_Automata.Digraph_Basic
21:07:35 CAVA_Automata: theory CAVA_Automata.Digraph
21:07:38 CAVA_Automata: theory CAVA_Automata.Automata
21:07:38 CAVA_Automata: theory CAVA_Automata.Digraph_Impl
21:07:41 Timing Kleene_Algebra (4 threads, 46.248s elapsed time, 109.120s cpu time, 4.364s GC time, factor 2.36)
21:07:41 Finished Kleene_Algebra (0:01:15 elapsed time, 0:02:40 cpu time, factor 2.11)
21:07:41 Building Sepref_Prereq ...
21:07:44 Sepref_Prereq: theory HOL-Library.Old_Datatype
21:07:44 Sepref_Prereq: theory HOL-Library.Nat_Bijection
21:07:44 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
21:07:45 CakeML: theory CakeML.Code_Test_Haskell
21:07:45 Sepref_Prereq: theory HOL-Library.Countable
21:07:46 CAVA_Automata: theory CAVA_Automata.Lasso
21:07:46 CAVA_Automata: theory CAVA_Automata.Simulation
21:07:47 CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
21:07:48 Sepref_Prereq: theory HOL-Imperative_HOL.Heap
21:07:50 Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
21:07:52 Sepref_Prereq: theory HOL-Imperative_HOL.Array
21:07:53 Sepref_Prereq: theory HOL-Imperative_HOL.Ref
21:07:54 Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
21:07:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
21:07:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
21:07:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
21:07:57 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
21:07:57 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
21:07:59 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
21:08:00 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
21:08:01 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
21:08:02 Timing Simple_Firewall (4 threads, 28.883s elapsed time, 107.944s cpu time, 4.180s GC time, factor 3.74)
21:08:02 Finished Simple_Firewall (0:01:02 elapsed time, 0:02:54 cpu time, factor 2.78)
21:08:02 Building Routing ...
21:08:04 Routing: theory HOL-Library.Adhoc_Overloading
21:08:04 Routing: theory Routing.Linorder_Helper
21:08:04 Routing: theory HOL-Library.Monad_Syntax
21:08:04 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
21:08:05 Routing: theory Routing.Routing_Table
21:08:05 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
21:08:06 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
21:08:07 CAVA_Automata: theory CAVA_Automata.Automata_Impl
21:08:10 Routing: theory Routing.IpRoute_Parser
21:08:10 Routing: theory Routing.Linux_Router
21:08:11 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
21:08:17 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
21:08:17 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
21:08:18 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
21:08:18 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
21:08:18 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
21:08:21 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
21:08:33 Native_Word: theory Native_Word.Native_Word_Test_Emu
21:08:33 Native_Word: theory Native_Word.Native_Word_Test_PolyML
21:08:33 Native_Word: theory Native_Word.Native_Word_Test_PolyML64
21:08:33 Native_Word: theory Native_Word.Native_Word_Test_Scala
21:08:39 Timing Routing (4 threads, 16.353s elapsed time, 39.552s cpu time, 0.940s GC time, factor 2.42)
21:08:39 Finished Routing (0:00:37 elapsed time, 0:01:15 cpu time, factor 2.03)
21:08:39 Building Iptables_Semantics ...
21:08:42 Iptables_Semantics: theory Iptables_Semantics.List_Misc
21:08:42 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
21:08:44 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
21:08:45 Iptables_Semantics: theory HOL-Library.Code_Target_Int
21:08:45 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
21:08:45 Iptables_Semantics: theory HOL-Library.LaTeXsugar
21:08:45 Iptables_Semantics: theory Native_Word.More_Bits_Int
21:08:45 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
21:08:45 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
21:08:45 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
21:08:45 Iptables_Semantics: theory Iptables_Semantics.Ternary
21:08:46 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
21:08:46 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
21:08:47 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int
21:08:48 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
21:08:48 Iptables_Semantics: theory Native_Word.Bits_Integer
21:08:49 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
21:08:49 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
21:08:50 Iptables_Semantics: theory Iptables_Semantics.Ports
21:08:52 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
21:08:52 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
21:08:58 Native_Word: theory Native_Word.Native_Word_Test_PolyML2
21:08:59 Timing Complx (4 threads, 321.577s elapsed time, 913.096s cpu time, 10.956s GC time, factor 2.84)
21:08:59 Finished Complx (0:05:27 elapsed time, 0:15:25 cpu time, factor 2.82)
21:08:59 Building Formal_SSA ...
21:09:02 CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
21:09:02 Timing Sepref_Prereq (4 threads, 43.283s elapsed time, 99.880s cpu time, 4.500s GC time, factor 2.31)
21:09:02 Finished Sepref_Prereq (0:01:19 elapsed time, 0:04:58 cpu time, factor 3.74)
21:09:02 Building Sepref_Basic ...
21:09:02 Formal_SSA: theory Formal_SSA.Serial_Rel
21:09:02 Formal_SSA: theory Dijkstra_Shortest_Path.Graph
21:09:02 Formal_SSA: theory HOL-Library.Char_ord
21:09:02 Formal_SSA: theory HOL-Library.Omega_Words_Fun
21:09:02 Formal_SSA: theory HOL-Library.List_Lexorder
21:09:03 Formal_SSA: theory HOL-Library.Mapping
21:09:03 Formal_SSA: theory HOL-Library.RBT_Set
21:09:03 Formal_SSA: theory CAVA_Automata.Digraph_Basic
21:09:03 Native_Word: theory Native_Word.Native_Word_Test_GHC
21:09:04 Formal_SSA: theory HOL-Library.Sublist
21:09:04 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
21:09:04 Iptables_Semantics: theory Iptables_Semantics.Semantics
21:09:04 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
21:09:04 Formal_SSA: theory Formal_SSA.While_Combinator_Exts
21:09:04 Formal_SSA: theory Dijkstra_Shortest_Path.GraphSpec
21:09:04 Formal_SSA: theory Slicing.AuxLemmas
21:09:04 Formal_SSA: theory HOL-Library.RBT_Mapping
21:09:04 Formal_SSA: theory Slicing.BasicDefs
21:09:04 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
21:09:05 Formal_SSA: theory Slicing.Com
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.User_Smashing
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.PO_Normalizer
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.Pf_Add
21:09:05 Sepref_Basic: theory HOL-Library.Rewrite
21:09:05 Sepref_Basic: theory List-Index.List_Index
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.Concl_Pres_Clarification
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.Named_Theorems_Rev
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Id_Op
21:09:05 Sepref_Basic: theory Refine_Imperative_HOL.Structured_Apply
21:09:06 Sepref_Basic: theory Separation_Logic_Imperative_HOL.Default_Insts
21:09:06 Sepref_Basic: theory Refine_Imperative_HOL.Pf_Mono_Prover
21:09:06 Formal_SSA: theory Formal_SSA.FormalSSA_Misc
21:09:06 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
21:09:06 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Misc
21:09:06 Formal_SSA: theory Slicing.CFG
21:09:06 Formal_SSA: theory Formal_SSA.Mapping_Exts
21:09:06 Formal_SSA: theory Slicing.CFGExit
21:09:07 Formal_SSA: theory Slicing.Postdomination
21:09:07 Formal_SSA: theory Formal_SSA.RBT_Mapping_Exts
21:09:07 Iptables_Semantics: theory Iptables_Semantics.Matching
21:09:07 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
21:09:07 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
21:09:07 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
21:09:08 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Basic
21:09:08 Sepref_Basic: theory Refine_Imperative_HOL.Term_Synth
21:09:08 Formal_SSA: theory Slicing.DynStandardControlDependence
21:09:08 Formal_SSA: theory Slicing.DynWeakControlDependence
21:09:08 Formal_SSA: theory Slicing.StandardControlDependence
21:09:08 Formal_SSA: theory Slicing.CFG_wf
21:09:08 Formal_SSA: theory Slicing.WeakControlDependence
21:09:08 Formal_SSA: theory Slicing.CFGExit_wf
21:09:08 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
21:09:08 Formal_SSA: theory Slicing.DynDataDependence
21:09:08 Formal_SSA: theory Slicing.DataDependence
21:09:08 Formal_SSA: theory Slicing.Distance
21:09:08 Formal_SSA: theory Slicing.PDG
21:09:08 Formal_SSA: theory Slicing.Observable
21:09:09 Formal_SSA: theory Slicing.SemanticsCFG
21:09:09 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
21:09:09 Formal_SSA: theory Slicing.Slice
21:09:09 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
21:09:09 Formal_SSA: theory Slicing.WeakOrderDependence
21:09:09 Formal_SSA: theory Slicing.Labels
21:09:09 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
21:09:10 Formal_SSA: theory Slicing.WCFG
21:09:10 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Monadify
21:09:10 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Constraints
21:09:11 Formal_SSA: theory Slicing.Interpretation
21:09:11 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Frame
21:09:11 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Rules
21:09:11 Formal_SSA: theory Slicing.CDepInstantiations
21:09:12 Formal_SSA: theory Formal_SSA.Graph_path
21:09:12 Formal_SSA: theory Slicing.WellFormed
21:09:12 Iptables_Semantics: theory Iptables_Semantics.Optimizing
21:09:12 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
21:09:13 Formal_SSA: theory Slicing.AdditionalLemmas
21:09:13 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
21:09:13 Formal_SSA: theory Formal_SSA.Disjoin_Transform
21:09:14 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
21:09:14 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
21:09:16 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
21:09:16 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Definition
21:09:17 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Translate
21:09:18 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
21:09:18 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
21:09:19 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Intf_Util
21:09:19 Formal_SSA: theory Formal_SSA.SSA_CFG
21:09:19 Native_Word: theory Native_Word.Native_Word_Test_MLton
21:09:19 Native_Word: theory Native_Word.Native_Word_Test_MLton2
21:09:19 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
21:09:22 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
21:09:22 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Tool
21:09:23 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
21:09:23 Formal_SSA: theory Formal_SSA.Construct_SSA
21:09:23 Formal_SSA: theory Formal_SSA.Minimality
21:09:23 Formal_SSA: theory Formal_SSA.SSA_CFG_code
21:09:24 Formal_SSA: theory Formal_SSA.Construct_SSA_notriv
21:09:27 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Foreach
21:09:27 Formal_SSA: theory Formal_SSA.SSA_Semantics
21:09:27 Formal_SSA: theory Formal_SSA.Construct_SSA_code
21:09:27 Formal_SSA: theory Formal_SSA.Construct_SSA_notriv_code
21:09:29 Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Improper
21:09:29 Sepref_Basic: theory Refine_Imperative_HOL.Sepref
21:09:30 Formal_SSA: theory Formal_SSA.SSA_Transfer_Rules
21:09:35 Native_Word: theory Native_Word.Native_Word_Test_OCaml2
21:09:35 Native_Word: theory Native_Word.Native_Word_Test_OCaml
21:09:37 Formal_SSA: theory Formal_SSA.Generic_Interpretation
21:09:41 Timing CAVA_Automata (4 threads, 89.949s elapsed time, 143.512s cpu time, 5.972s GC time, factor 1.60)
21:09:41 Finished CAVA_Automata (0:02:09 elapsed time, 0:03:36 cpu time, factor 1.68)
21:09:41 Building CAVA_Setup ...
21:09:44 CAVA_Setup: theory HOL-Library.Case_Converter
21:09:44 CAVA_Setup: theory HOL-Library.IArray
21:09:44 CAVA_Setup: theory Partial_Order_Reduction.Basic_Extensions
21:09:44 CAVA_Setup: theory Partial_Order_Reduction.Set_Extensions
21:09:45 CAVA_Setup: theory Partial_Order_Reduction.Functions
21:09:45 CAVA_Setup: theory HOL-Library.Simps_Case_Conv
21:09:45 CAVA_Setup: theory HOL-Library.Lattice_Syntax
21:09:45 CAVA_Setup: theory HOL-Library.Complete_Partial_Order2
21:09:45 CAVA_Setup: theory Partial_Order_Reduction.Relation_Extensions
21:09:45 CAVA_Setup: theory HOL-Library.Mapping
21:09:45 CAVA_Setup: theory HOL-Library.Stream
21:09:46 CAVA_Setup: theory DFS_Framework.DFS_Framework_Misc
21:09:46 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ
21:09:46 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2
21:09:46 CAVA_Setup: theory HOL-Library.Sublist
21:09:47 CAVA_Setup: theory HOL-Library.RBT_Mapping
21:09:47 CAVA_Setup: theory HOL-Library.Countable_Set
21:09:47 CAVA_Setup: theory LTL.LTL
21:09:48 CAVA_Setup: theory HOL-Library.Countable_Complete_Lattices
21:09:48 CAVA_Setup: theory HOL-Library.Prefix_Order
21:09:48 CAVA_Setup: theory Partial_Order_Reduction.List_Prefixes
21:09:48 CAVA_Setup: theory Partial_Order_Reduction.List_Extensions
21:09:48 CAVA_Setup: theory Promela.PromelaAST
21:09:50 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton
21:09:52 CAVA_Setup: theory HOL-Library.Order_Continuity
21:09:53 CAVA_Setup: theory HOL-Library.Extended_Nat
21:09:54 CAVA_Setup: theory Coinductive.Coinductive_Nat
21:09:55 Formal_SSA: theory Formal_SSA.Generic_Extract
21:09:55 Formal_SSA: theory Formal_SSA.WhileGraphSSA
21:09:55 CAVA_Setup: theory Coinductive.Coinductive_List
21:09:56 CAVA_Setup: theory Partial_Order_Reduction.ENat_Extensions
21:09:56 CAVA_Setup: theory Partial_Order_Reduction.CCPO_Extensions
21:09:56 Native_Word: theory Native_Word.Uint_Userguide
21:09:57 CAVA_Setup: theory Partial_Order_Reduction.ESet_Extensions
21:10:00 CAVA_Setup: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:10:01 Timing CakeML (4 threads, 434.195s elapsed time, 1319.276s cpu time, 228.448s GC time, factor 3.04)
21:10:01 Finished CakeML (0:09:05 elapsed time, 0:26:23 cpu time, factor 2.90)
21:10:01 Timing Sepref_Basic (4 threads, 24.821s elapsed time, 54.540s cpu time, 1.868s GC time, factor 2.20)
21:10:01 Finished Sepref_Basic (0:00:57 elapsed time, 0:01:43 cpu time, factor 1.80)
21:10:01 Running CakeML_Codegen ...
21:10:01 Building Transition_Systems_and_Automata ...
21:10:03 CAVA_Setup: theory Gabow_SCC.Gabow_SCC
21:10:04 CakeML_Codegen: theory Automatic_Refinement.Refine_Util_Bootstrap1
21:10:04 CakeML_Codegen: theory HOL-Data_Structures.Cmp
21:10:04 CakeML_Codegen: theory HOL-Library.AList
21:10:04 CakeML_Codegen: theory HOL-Data_Structures.Less_False
21:10:04 CakeML_Codegen: theory HOL-Data_Structures.Sorted_Less
21:10:04 CakeML_Codegen: theory Automatic_Refinement.Mk_Term_Antiquot
21:10:04 Transition_Systems_and_Automata: theory CAVA_Base.Statistics
21:10:04 Transition_Systems_and_Automata: theory HOL-Library.Omega_Words_Fun
21:10:04 Transition_Systems_and_Automata: theory HOL-Library.Nat_Bijection
21:10:04 Transition_Systems_and_Automata: theory HOL-Library.Old_Datatype
21:10:04 CakeML_Codegen: theory Automatic_Refinement.Mpat_Antiquot
21:10:04 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Misc
21:10:04 CakeML_Codegen: theory HOL-Data_Structures.List_Ins_Del
21:10:04 Transition_Systems_and_Automata: theory HOL-Library.Sublist
21:10:05 CakeML_Codegen: theory Automatic_Refinement.Refine_Util
21:10:05 CAVA_Setup: theory SM.LTS
21:10:05 CakeML_Codegen: theory HOL-Library.Adhoc_Overloading
21:10:05 CakeML_Codegen: theory HOL-Data_Structures.Set_Specs
21:10:05 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Basic
21:10:05 CakeML_Codegen: theory HOL-Library.Monad_Syntax
21:10:05 CAVA_Setup: theory Promela.PromelaStatistics
21:10:05 CAVA_Setup: theory Gabow_SCC.Find_Path
21:10:05 CakeML_Codegen: theory HOL-Data_Structures.Priority_Queue_Specs
21:10:05 Transition_Systems_and_Automata: theory HOL-Library.Stream
21:10:05 CAVA_Setup: theory Gabow_SCC.Find_Path_Impl
21:10:05 CakeML_Codegen: theory HOL-Library.Conditional_Parametricity
21:10:05 CakeML_Codegen: theory HOL-Library.Pattern_Aliases
21:10:06 Transition_Systems_and_Automata: theory HOL-Library.Countable
21:10:06 CakeML_Codegen: theory Dict_Construction.Dict_Construction
21:10:06 CakeML_Codegen: theory HOL-Library.Tree
21:10:06 CakeML_Codegen: theory HOL-Library.FSet
21:10:07 CakeML_Codegen: theory Amortized_Complexity.Amortized_Framework0
21:10:07 Transition_Systems_and_Automata: theory CAVA_Base.Code_String
21:10:07 Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Code_Target
21:10:07 Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Base
21:10:07 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Refine_Aux
21:10:07 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Basic
21:10:07 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence
21:10:07 CakeML_Codegen: theory Huffman.Huffman
21:10:07 CAVA_Setup: theory Coinductive.Coinductive_List_Prefix
21:10:08 CAVA_Setup: theory Coinductive.Coinductive_Stream
21:10:08 Transition_Systems_and_Automata: theory HOL-Library.Countable_Set
21:10:08 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA
21:10:09 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph
21:10:09 Transition_Systems_and_Automata: theory HOL-Library.Countable_Complete_Lattices
21:10:09 Transition_Systems_and_Automata: theory DFS_Framework.Impl_Rev_Array_Stack
21:10:10 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System
21:10:10 CAVA_Setup: theory Partial_Order_Reduction.Coinductive_List_Extensions
21:10:10 CakeML_Codegen: theory HOL-Data_Structures.Tree2
21:10:11 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
21:10:11 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
21:10:11 CakeML_Codegen: theory HOL-Data_Structures.Tree_Set
21:10:11 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
21:10:11 Transition_Systems_and_Automata: theory CAVA_Automata.Automata
21:10:11 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Impl
21:10:11 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton
21:10:11 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
21:10:12 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
21:10:12 CAVA_Setup: theory Gabow_SCC.Gabow_GBG
21:10:12 CakeML_Codegen: theory HOL-Library.Tree_Multiset
21:10:12 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
21:10:13 CakeML_Codegen: theory CakeML_Codegen.ML_Utils
21:10:13 Transition_Systems_and_Automata: theory HOL-Library.Order_Continuity
21:10:13 CakeML_Codegen: theory Pairing_Heap.Pairing_Heap_Tree
21:10:13 CakeML_Codegen: theory HOL-Library.Finite_Map
21:10:13 CakeML_Codegen: theory CakeML_Codegen.Code_Utils
21:10:13 CakeML_Codegen: theory HOL-Data_Structures.Leftist_Heap
21:10:13 Timing Native_Word (4 threads, 654.758s elapsed time, 673.244s cpu time, 6.344s GC time, factor 1.03)
21:10:13 Finished Native_Word (0:11:03 elapsed time, 0:23:09 cpu time, factor 2.09)
21:10:13 Building Sepref_IICF ...
21:10:13 CakeML_Codegen: theory HOL-Library.Tree_Real
21:10:14 CakeML_Codegen: theory HOL-Data_Structures.Balance
21:10:14 Transition_Systems_and_Automata: theory HOL-Library.Extended_Nat
21:10:15 CakeML_Codegen: theory Root_Balanced_Tree.Time_Monad
21:10:15 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
21:10:16 Transition_Systems_and_Automata: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:10:16 CakeML_Codegen: theory Root_Balanced_Tree.Root_Balanced_Tree
21:10:16 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton_Code
21:10:17 Sepref_IICF: theory Refine_Imperative_HOL.IICF_List
21:10:17 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Map
21:10:17 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Matrix
21:10:17 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Multiset
21:10:18 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
21:10:18 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
21:10:18 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Map
21:10:18 Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path
21:10:18 Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_Mset
21:10:18 Transition_Systems_and_Automata: theory DFS_Framework.Param_DFS
21:10:18 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_LTL
21:10:19 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
21:10:19 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array
21:10:20 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance
21:10:20 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_List
21:10:20 Sepref_IICF: theory Refine_Imperative_HOL.IICF_HOL_List
21:10:20 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_Zip
21:10:20 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization
21:10:21 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Maps
21:10:21 Sepref_IICF: theory Refine_Imperative_HOL.IICF_MS_Array_List
21:10:21 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Refine
21:10:22 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA_impl
21:10:22 Transition_Systems_and_Automata: theory CAVA_Automata.Lasso
21:10:22 Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_MsetO
21:10:22 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_Matrix
21:10:23 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Bag
21:10:23 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Set
21:10:23 CAVA_Setup: theory Promela.PromelaDatastructures
21:10:23 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
21:10:23 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
21:10:23 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heap
21:10:24 Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_SetO
21:10:24 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance_Refine
21:10:24 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Sepl_Binding
21:10:24 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG
21:10:25 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
21:10:25 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization_Refine
21:10:26 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Implement
21:10:26 CAVA_Setup: theory DFS_Framework.DFS_Framework_Refine_Aux
21:10:26 Iptables_Semantics: theory Iptables_Semantics.Transform
21:10:26 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heap
21:10:27 CAVA_Setup: theory DFS_Framework.Impl_Rev_Array_Stack
21:10:27 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Invars_Basic
21:10:28 Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
21:10:28 CAVA_Setup: theory DFS_Framework.Param_DFS
21:10:29 Transition_Systems_and_Automata: theory DFS_Framework.General_DFS_Structure
21:10:30 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Construction
21:10:31 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Extra
21:10:31 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
21:10:32 CakeML_Codegen: theory CakeML_Codegen.Test_Utils
21:10:32 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Deterministic
21:10:32 CakeML_Codegen: theory CakeML_Codegen.Compiler_Utils
21:10:32 CakeML_Codegen: theory CakeML_Codegen.CakeML_Utils
21:10:33 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
21:10:36 CAVA_Setup: theory DFS_Framework.DFS_Invars_Basic
21:10:38 Transition_Systems_and_Automata: theory DFS_Framework.Rec_Impl
21:10:38 Transition_Systems_and_Automata: theory DFS_Framework.Tailrec_Impl
21:10:39 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Nondeterministic
21:10:39 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
21:10:39 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
21:10:40 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
21:10:41 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
21:10:41 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
21:10:43 CAVA_Setup: theory DFS_Framework.General_DFS_Structure
21:10:47 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA
21:10:47 Sepref_IICF: theory Refine_Imperative_HOL.IICF
21:10:48 Transition_Systems_and_Automata: theory CAVA_Automata.Automata_Impl
21:10:48 Iptables_Semantics: theory Iptables_Semantics.Parser
21:10:48 Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path_Impl
21:10:48 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton_Code
21:10:48 Iptables_Semantics: theory Iptables_Semantics.Parser6
21:10:49 Iptables_Semantics: theory Iptables_Semantics.Documentation
21:10:49 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
21:10:53 CAVA_Setup: theory DFS_Framework.Rec_Impl
21:10:56 Transition_Systems_and_Automata: theory DFS_Framework.Simple_Impl
21:11:03 CAVA_Setup: theory DFS_Framework.Tailrec_Impl
21:11:04 CAVA_Setup: theory DFS_Framework.Simple_Impl
21:11:04 Transition_Systems_and_Automata: theory DFS_Framework.Restr_Impl
21:11:04 CAVA_Setup: theory Gabow_SCC.Gabow_GBG_Code
21:11:05 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA
21:11:07 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA
21:11:07 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework
21:11:08 Transition_Systems_and_Automata: theory DFS_Framework.Reachable_Nodes
21:11:08 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DFA
21:11:10 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBA
21:11:12 CAVA_Setup: theory Gabow_SCC.Gabow_SCC_Code
21:11:12 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA_Combine
21:11:13 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBTA
21:11:15 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA_Combine
21:11:16 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGCA
21:11:17 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA_Combine
21:11:19 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA
21:11:20 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Combine
21:11:21 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_Backend
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_Compiler
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_CupCake
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_Preproc
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_Rewriting
21:11:22 CakeML_Codegen: theory CakeML_Codegen.Doc_Terms
21:11:22 CakeML_Codegen: theory Constructor_Funs.Constructor_Funs
21:11:22 CakeML_Codegen: theory Datatype_Order_Generator.Derive_Aux
21:11:22 CakeML_Codegen: theory HOL-Library.State_Monad
21:11:22 CakeML_Codegen: theory Higher_Order_Terms.Disjoint_Sets
21:11:22 CakeML_Codegen: theory Higher_Order_Terms.Name
21:11:22 CakeML_Codegen: theory List-Index.List_Index
21:11:22 CakeML_Codegen: theory Datatype_Order_Generator.Order_Generator
21:11:22 CakeML_Codegen: theory CakeML_Codegen.CakeML_Byte
21:11:22 CakeML_Codegen: theory CakeML_Codegen.CupCake_Env
21:11:23 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA
21:11:23 CakeML_Codegen: theory Higher_Order_Terms.Find_First
21:11:23 CakeML_Codegen: theory Higher_Order_Terms.Term_Utils
21:11:24 CakeML_Codegen: theory Higher_Order_Terms.Fresh_Monad
21:11:24 CakeML_Codegen: theory Higher_Order_Terms.Term_Class
21:11:24 CakeML_Codegen: theory Higher_Order_Terms.Fresh_Class
21:11:24 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NFA
21:11:25 CakeML_Codegen: theory CakeML_Codegen.CupCake_Semantics
21:11:26 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA
21:11:27 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Combine
21:11:28 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBTA
21:11:28 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Refine
21:11:29 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Refine
21:11:30 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA_Combine
21:11:31 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Implement
21:11:31 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Refine
21:11:32 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Implement
21:11:32 CakeML_Codegen: theory Higher_Order_Terms.Nterm
21:11:32 CakeML_Codegen: theory Higher_Order_Terms.Term
21:11:33 CakeML_Codegen: theory Higher_Order_Terms.Pats
21:11:34 CakeML_Codegen: theory CakeML_Codegen.Terms_Extras
21:11:35 CakeML_Codegen: theory Higher_Order_Terms.Term_to_Nterm
21:11:35 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Refine
21:11:35 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Implement
21:11:36 CakeML_Codegen: theory CakeML_Codegen.General_Rewriting
21:11:36 CakeML_Codegen: theory CakeML_Codegen.HOL_Datatype
21:11:39 CakeML_Codegen: theory CakeML_Codegen.Constructors
21:11:40 CAVA_Setup: theory LTL_to_GBA.All_Of_LTL_to_GBA
21:11:40 CAVA_Setup: theory DFS_Framework.Restr_Impl
21:11:43 CAVA_Setup: theory DFS_Framework.DFS_Framework
21:11:44 CAVA_Setup: theory DFS_Framework.Reachable_Nodes
21:11:48 MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Code
21:11:50 CakeML_Codegen: theory CakeML_Codegen.Consts
21:11:50 CakeML_Codegen: theory CakeML_Codegen.Strong_Term
21:11:50 CAVA_Setup: theory SM.SM_Syntax
21:11:50 CakeML_Codegen: theory CakeML_Codegen.CakeML_Setup
21:11:52 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Term
21:11:52 CakeML_Codegen: theory CakeML_Codegen.Sterm
21:11:52 CakeML_Codegen: theory CakeML_Codegen.Eval_Class
21:11:52 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Nterm
21:11:53 Timing Linear_Recurrences_Solver (4 threads, 325.624s elapsed time, 923.692s cpu time, 72.444s GC time, factor 2.84)
21:11:53 Finished Linear_Recurrences_Solver (0:05:30 elapsed time, 0:15:28 cpu time, factor 2.81)
21:11:53 Building SM_Base ...
21:11:54 CakeML_Codegen: theory CakeML_Codegen.Embed
21:11:55 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG_Code
21:11:55 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Graphs
21:11:55 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Graphs
21:11:55 CAVA_Setup: theory SM.SM_State
21:11:56 CakeML_Codegen: theory CakeML_Codegen.Pterm
21:11:57 SM_Base: theory HOL-Library.Case_Converter
21:11:57 SM_Base: theory Partial_Order_Reduction.Basic_Extensions
21:11:57 SM_Base: theory Partial_Order_Reduction.Set_Extensions
21:11:57 SM_Base: theory HOL-Library.Lattice_Syntax
21:11:57 SM_Base: theory HOL-Library.Complete_Partial_Order2
21:11:58 SM_Base: theory Partial_Order_Reduction.Functions
21:11:58 SM_Base: theory HOL-Library.Simps_Case_Conv
21:11:58 CAVA_Setup: theory SM.SOS_Misc_Add
21:11:58 CAVA_Setup: theory SM.Gen_Scheduler
21:11:58 SM_Base: theory HOL-Library.Stream
21:11:58 SM_Base: theory Partial_Order_Reduction.Relation_Extensions
21:11:58 SM_Base: theory DFS_Framework.DFS_Framework_Misc
21:11:58 SM_Base: theory HOL-Library.Sublist
21:11:58 CakeML_Codegen: theory CakeML_Codegen.Term_as_Value
21:11:59 SM_Base: theory HOL-Library.Countable_Set
21:11:59 CakeML_Codegen: theory CakeML_Codegen.Eval_Instances
21:11:59 CakeML_Codegen: theory CakeML_Codegen.Value
21:12:00 SM_Base: theory HOL-Library.Countable_Complete_Lattices
21:12:01 SM_Base: theory LTL.LTL
21:12:01 SM_Base: theory HOL-Library.Prefix_Order
21:12:01 SM_Base: theory Partial_Order_Reduction.List_Prefixes
21:12:01 SM_Base: theory Partial_Order_Reduction.List_Extensions
21:12:01 SM_Base: theory DFS_Framework.DFS_Framework_Refine_Aux
21:12:02 SM_Base: theory DFS_Framework.Impl_Rev_Array_Stack
21:12:03 CAVA_Setup: theory SM.Gen_Scheduler_Refine
21:12:04 SM_Base: theory DFS_Framework.Param_DFS
21:12:04 CAVA_Setup: theory SM.Gen_Cfg_Bisim
21:12:04 SM_Base: theory Stuttering_Equivalence.Samplers
21:12:04 SM_Base: theory Stuttering_Equivalence.StutterEquivalence
21:12:04 SM_Base: theory HOL-Library.Order_Continuity
21:12:05 CAVA_Setup: theory SM.SM_Cfg
21:12:05 SM_Base: theory Transition_Systems_and_Automata.Basic
21:12:05 SM_Base: theory Transition_Systems_and_Automata.Sequence
21:12:06 SM_Base: theory HOL-Library.Extended_Nat
21:12:07 SM_Base: theory Partial_Order_Reduction.Word_Prefixes
21:12:08 SM_Base: theory Coinductive.Coinductive_Nat
21:12:08 SM_Base: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:12:08 Timing Sepref_IICF (4 threads, 70.316s elapsed time, 217.004s cpu time, 4.304s GC time, factor 3.09)
21:12:08 Finished Sepref_IICF (0:01:53 elapsed time, 0:05:11 cpu time, factor 2.73)
21:12:08 Building Flow_Networks ...
21:12:10 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm_Elim
21:12:10 SM_Base: theory Coinductive.Coinductive_List
21:12:11 SM_Base: theory Partial_Order_Reduction.ENat_Extensions
21:12:11 SM_Base: theory Partial_Order_Reduction.CCPO_Extensions
21:12:12 Flow_Networks: theory CAVA_Base.Statistics
21:12:12 Flow_Networks: theory Flow_Networks.Graph
21:12:12 Flow_Networks: theory HOL-Library.Omega_Words_Fun
21:12:12 Flow_Networks: theory DFS_Framework.DFS_Framework_Misc
21:12:12 Flow_Networks: theory Program-Conflict-Analysis.LTS
21:12:12 Flow_Networks: theory CAVA_Base.Code_String
21:12:12 Flow_Networks: theory CAVA_Base.CAVA_Code_Target
21:12:13 Flow_Networks: theory CAVA_Base.CAVA_Base
21:12:13 Flow_Networks: theory DFS_Framework.DFS_Framework_Refine_Aux
21:12:13 SM_Base: theory DFS_Framework.DFS_Invars_Basic
21:12:14 SM_Base: theory Partial_Order_Reduction.ESet_Extensions
21:12:14 Flow_Networks: theory CAVA_Automata.Digraph_Basic
21:12:14 Flow_Networks: theory Flow_Networks.Fofu_Abs_Base
21:12:15 CAVA_Setup: theory SM.SM_Semantics
21:12:15 SM_Base: theory DFS_Framework.General_DFS_Structure
21:12:15 Flow_Networks: theory DFS_Framework.Impl_Rev_Array_Stack
21:12:15 Flow_Networks: theory CAVA_Automata.Digraph
21:12:16 Flow_Networks: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
21:12:17 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Nodes
21:12:18 Flow_Networks: theory CAVA_Automata.Digraph_Impl
21:12:18 Flow_Networks: theory DFS_Framework.Param_DFS
21:12:19 SM_Base: theory Partial_Order_Reduction.Traces
21:12:20 Flow_Networks: theory Flow_Networks.Fofu_Impl_Base
21:12:20 SM_Base: theory Transition_Systems_and_Automata.Sequence_LTL
21:12:22 SM_Base: theory Transition_Systems_and_Automata.Transition_System
21:12:22 SM_Base: theory Transition_Systems_and_Automata.Transition_System_Construction
21:12:23 SM_Base: theory Transition_Systems_and_Automata.Transition_System_Extra
21:12:23 CAVA_Setup: theory SM.Decide_Locality
21:12:24 SM_Base: theory Partial_Order_Reduction.Transition_System_Extensions
21:12:24 SM_Base: theory Coinductive.Coinductive_List_Prefix
21:12:24 SM_Base: theory Coinductive.Coinductive_Stream
21:12:25 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Explicit
21:12:25 CAVA_Setup: theory SM.SM_LTL
21:12:25 Flow_Networks: theory DFS_Framework.DFS_Invars_Basic
21:12:25 SM_Base: theory Stuttering_Equivalence.PLTL
21:12:26 Flow_Networks: theory DFS_Framework.General_DFS_Structure
21:12:26 SM_Base: theory Partial_Order_Reduction.Coinductive_List_Extensions
21:12:26 Flow_Networks: theory Flow_Networks.Refine_Add_Fofu
21:12:26 SM_Base: theory Partial_Order_Reduction.Transition_System_Traces
21:12:27 CAVA_Setup: theory Promela.PromelaInvariants
21:12:27 SM_Base: theory DFS_Framework.Rec_Impl
21:12:27 SM_Base: theory DFS_Framework.Tailrec_Impl
21:12:28 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm
21:12:28 SM_Base: theory Partial_Order_Reduction.LList_Prefixes
21:12:29 SM_Base: theory Partial_Order_Reduction.Stuttering
21:12:29 CAVA_Setup: theory Promela.Promela
21:12:30 SM_Base: theory Partial_Order_Reduction.Formula
21:12:30 SM_Base: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
21:12:31 SM_Base: theory Partial_Order_Reduction.Ample_Abstract
21:12:31 CAVA_Setup: theory SM.Type_System
21:12:32 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Translate
21:12:32 SM_Base: theory Partial_Order_Reduction.Ample_Analysis
21:12:33 SM_Base: theory Partial_Order_Reduction.Ample_Correctness
21:12:34 Flow_Networks: theory DFS_Framework.Rec_Impl
21:12:35 Flow_Networks: theory DFS_Framework.Tailrec_Impl
21:12:36 SM_Base: theory DFS_Framework.Simple_Impl
21:12:36 CAVA_Setup: theory SM.SM_Finite_Reachable
21:12:36 CakeML_Codegen: theory CakeML_Codegen.Rewriting_Sterm
21:12:37 CAVA_Setup: theory SM.Rename_Cfg
21:12:42 Flow_Networks: theory DFS_Framework.Simple_Impl
21:12:44 SM_Base: theory DFS_Framework.Restr_Impl
21:12:47 CAVA_Setup: theory SM.SM_Visible
21:12:47 SM_Base: theory DFS_Framework.DFS_Framework
21:12:48 SM_Base: theory DFS_Framework.Reachable_Nodes
21:12:49 CAVA_Setup: theory DFS_Framework.Feedback_Arcs
21:12:49 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Sterm
21:12:49 CakeML_Codegen: theory CakeML_Codegen.CakeML_Backend
21:12:49 CAVA_Setup: theory Stuttering_Equivalence.Samplers
21:12:50 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value
21:12:50 CAVA_Setup: theory Stuttering_Equivalence.StutterEquivalence
21:12:50 Flow_Networks: theory DFS_Framework.Restr_Impl
21:12:50 CAVA_Setup: theory Stuttering_Equivalence.PLTL
21:12:51 CAVA_Setup: theory Transition_Systems_and_Automata.Basic
21:12:51 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence
21:12:51 CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value_ML
21:12:52 CAVA_Setup: theory Partial_Order_Reduction.Word_Prefixes
21:12:53 Flow_Networks: theory DFS_Framework.DFS_Framework
21:12:53 CAVA_Setup: theory Gabow_SCC.All_Of_Gabow_SCC
21:12:53 CAVA_Setup: theory Partial_Order_Reduction.LList_Prefixes
21:12:53 Flow_Networks: theory DFS_Framework.Reachable_Nodes
21:12:54 CAVA_Setup: theory Partial_Order_Reduction.Stuttering
21:12:54 CAVA_Setup: theory Partial_Order_Reduction.Traces
21:12:55 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence_LTL
21:12:55 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System
21:12:56 Timing MFODL_Monitor_Optimized (4 threads, 492.513s elapsed time, 1313.828s cpu time, 96.204s GC time, factor 2.67)
21:12:56 Finished MFODL_Monitor_Optimized (0:08:26 elapsed time, 0:22:20 cpu time, factor 2.64)
21:12:56 Building LLL_Basis_Reduction ...
21:13:03 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Construction
21:13:03 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Extra
21:13:03 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
21:13:03 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
21:13:03 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
21:13:03 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
21:13:04 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Extensions
21:13:05 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
21:13:06 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Traces
21:13:06 CAVA_Setup: theory SM.Pid_Scheduler
21:13:07 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
21:13:08 CAVA_Setup: theory Partial_Order_Reduction.Ample_Abstract
21:13:09 CAVA_Setup: theory Partial_Order_Reduction.Ample_Analysis
21:13:09 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
21:13:11 CAVA_Setup: theory SM.SM_Pid
21:13:12 Timing Iptables_Semantics (4 threads, 182.302s elapsed time, 676.736s cpu time, 50.132s GC time, factor 3.71)
21:13:12 Finished Iptables_Semantics (0:04:30 elapsed time, 0:14:59 cpu time, factor 3.33)
21:13:12 Running Iptables_Semantics_Examples ...
21:13:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
21:13:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
21:13:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
21:13:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
21:13:16 CAVA_Setup: theory SM.SM_Variables
21:13:18 CAVA_Setup: theory SM.SM_Indep
21:13:20 CakeML_Codegen: theory CakeML_Codegen.CakeML_Correctness
21:13:21 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
21:13:21 CakeML_Codegen: theory CakeML_Codegen.Composition
21:13:22 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
21:13:27 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
21:13:27 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
21:13:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
21:13:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
21:13:31 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
21:13:32 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
21:13:32 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
21:13:33 Timing Algebraic_Numbers (4 threads, 416.194s elapsed time, 1348.232s cpu time, 94.008s GC time, factor 3.24)
21:13:33 Finished Algebraic_Numbers (0:07:09 elapsed time, 0:22:49 cpu time, factor 3.19)
21:13:33 Building Refine_Imperative_HOL ...
21:13:35 CakeML_Codegen: theory CakeML_Codegen.Compiler
21:13:36 Refine_Imperative_HOL: theory Isar_Ref.Base
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.User_Smashing
21:13:36 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Misc
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.PO_Normalizer
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Add
21:13:36 Refine_Imperative_HOL: theory List-Index.List_Index
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Concl_Pres_Clarification
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Named_Theorems_Rev
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Structured_Apply
21:13:36 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Refine_Aux
21:13:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Mono_Prover
21:13:37 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Misc
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Term_Synth
21:13:39 Refine_Imperative_HOL: theory HOL-Library.Rewrite
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_IICF
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Setup
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Tool
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Userguides
21:13:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Id_Op
21:13:39 Refine_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
21:13:40 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Algorithms
21:13:40 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Basic
21:13:42 CAVA_Setup: theory SM.SM_Datastructures
21:13:42 CAVA_Setup: theory SM.SM_Sticky
21:13:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Monadify
21:13:43 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Constraints
21:13:44 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Frame
21:13:44 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Rules
21:13:46 SM_Base: theory DFS_Framework.Feedback_Arcs
21:13:48 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
21:13:48 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Definition
21:13:49 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Translate
21:13:49 CAVA_Setup: theory Promela.PromelaLTL
21:13:49 CAVA_Setup: theory Promela.PromelaLTLConv
21:13:51 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Intf_Util
21:13:54 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Tool
21:13:55 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Explicit
21:13:55 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Algorithms
21:13:55 CAVA_Setup: theory SM.SM_POR
21:13:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
21:13:57 Flow_Networks: theory Flow_Networks.Network
21:13:59 Flow_Networks: theory Flow_Networks.Residual_Graph
21:14:00 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Foreach
21:14:01 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
21:14:01 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
21:14:01 Flow_Networks: theory Flow_Networks.Augmenting_Flow
21:14:01 Flow_Networks: theory Flow_Networks.Augmenting_Path
21:14:02 Flow_Networks: theory Flow_Networks.Ford_Fulkerson
21:14:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Improper
21:14:03 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref
21:14:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Map
21:14:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Matrix
21:14:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Multiset
21:14:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List
21:14:04 Flow_Networks: theory Flow_Networks.Graph_Impl
21:14:04 Flow_Networks: theory Flow_Networks.Network_Impl
21:14:04 CAVA_Setup: theory Promela.All_Of_Promela
21:14:04 CakeML_Codegen: theory Lazy_Case.Lazy_Case
21:14:05 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Map
21:14:05 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
21:14:05 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
21:14:05 CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
21:14:05 CakeML_Codegen: theory CakeML_Codegen.Test_Composition
21:14:05 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_Mset
21:14:05 Flow_Networks: theory Flow_Networks.NetCheck
21:14:05 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Translate
21:14:06 CAVA_Setup: theory SM.SM_Ample_Impl
21:14:06 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array
21:14:06 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_List
21:14:06 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_HOL_List
21:14:07 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_MS_Array_List
21:14:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_MsetO
21:14:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_Matrix
21:14:08 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Bag
21:14:09 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
21:14:09 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Set
21:14:09 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heap
21:14:09 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_SetO
21:14:10 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Sepl_Binding
21:14:10 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
21:14:12 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heap
21:14:13 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
21:14:16 CakeML_Codegen: theory CakeML_Codegen.Test_Print
21:14:31 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF
21:14:34 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_General_Util
21:14:34 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
21:14:37 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Reference
21:14:57 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
21:14:57 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
21:15:23 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc
21:15:23 Refine_Imperative_HOL: theory HOL-Library.Omega_Words_Fun
21:15:23 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight
21:15:23 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph
21:15:23 Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph
21:15:24 Refine_Imperative_HOL: theory CAVA_Automata.Digraph_Basic
21:15:24 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec
21:15:25 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
21:15:27 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra
21:15:28 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph
21:15:31 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA
21:15:32 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap
21:15:33 Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS
21:15:35 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
21:15:35 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl
21:15:38 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
21:15:40 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
21:15:55 Timing SM_Base (4 threads, 164.455s elapsed time, 568.980s cpu time, 28.380s GC time, factor 3.46)
21:15:55 Finished SM_Base (0:03:59 elapsed time, 0:12:28 cpu time, factor 3.13)
21:15:56 Timing Flow_Networks (4 threads, 162.251s elapsed time, 441.336s cpu time, 12.964s GC time, factor 2.72)
21:15:56 Finished Flow_Networks (0:03:44 elapsed time, 0:10:08 cpu time, factor 2.71)
21:15:56 Building KAT_and_DRA ...
21:15:56 Running SPARCv8 ...
21:15:58 SPARCv8: theory SPARCv8.WordDecl
21:15:58 KAT_and_DRA: theory KAT_and_DRA.Test_Dioid
21:15:58 KAT_and_DRA: theory KAT_and_DRA.KAT2
21:15:58 KAT_and_DRA: theory KAT_and_DRA.DRAT2
21:15:59 SPARCv8: theory HOL-Eisbach.Eisbach
21:15:59 SPARCv8: theory SPARCv8.Lib
21:15:59 SPARCv8: theory SPARCv8.RegistersOps
21:15:59 SPARCv8: theory SPARCv8.Sparc_Types
21:15:59 SPARCv8: theory SPARCv8.DetMonad
21:16:00 SPARCv8: theory HOL-Eisbach.Eisbach_Tools
21:16:00 SPARCv8: theory SPARCv8.DetMonadLemmas
21:16:02 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
21:16:02 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
21:16:07 KAT_and_DRA: theory KAT_and_DRA.Conway_Tests
21:16:08 CAVA_Setup: theory SM.SM_Wrapup
21:16:10 KAT_and_DRA: theory KAT_and_DRA.KAT
21:16:15 KAT_and_DRA: theory KAT_and_DRA.DRAT
21:16:16 KAT_and_DRA: theory KAT_and_DRA.PHL_KAT
21:16:16 KAT_and_DRA: theory KAT_and_DRA.KAT_Models
21:16:17 KAT_and_DRA: theory KAT_and_DRA.DRA_Models
21:16:17 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
21:16:17 KAT_and_DRA: theory KAT_and_DRA.FolkTheorem
21:16:22 KAT_and_DRA: theory KAT_and_DRA.PHL_DRAT
21:16:28 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test
21:16:31 SPARCv8: theory SPARCv8.MMU
21:16:33 SPARCv8: theory SPARCv8.Sparc_State
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra
21:16:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator
21:16:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype
21:16:37 SPARCv8: theory SPARCv8.Sparc_Instruction
21:16:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS
21:16:42 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS
21:16:42 SPARCv8: theory SPARCv8.Sparc_Execution
21:16:43 SPARCv8: theory SPARCv8.Sparc_Properties
21:16:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests
21:16:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
21:16:51 Timing KAT_and_DRA (4 threads, 30.613s elapsed time, 96.228s cpu time, 3.064s GC time, factor 3.14)
21:16:51 Finished KAT_and_DRA (0:00:54 elapsed time, 0:02:30 cpu time, factor 2.78)
21:16:51 Running Algebraic_VCs ...
21:16:53 Algebraic_VCs: theory HOL-Eisbach.Eisbach
21:16:53 Algebraic_VCs: theory Algebraic_VCs.P2S2R
21:16:53 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_scratch
21:16:53 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_scratch
21:16:53 Algebraic_VCs: theory HOL-Hoare.Heap
21:16:54 Algebraic_VCs: theory KAD.Domain_Semiring
21:16:55 Algebraic_VCs: theory Algebraic_VCs.VC_KAT
21:16:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark
21:16:59 Algebraic_VCs: theory Algebraic_VCs.RKAT
21:17:00 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples
21:17:00 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples2
21:17:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
21:17:01 Algebraic_VCs: theory Algebraic_VCs.RKAT_Models
21:17:01 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT
21:17:01 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT_Examples
21:17:11 Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark
21:17:13 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples
21:17:17 Timing Transition_Systems_and_Automata (4 threads, 328.316s elapsed time, 1200.964s cpu time, 96.000s GC time, factor 3.66)
21:17:17 Finished Transition_Systems_and_Automata (0:07:12 elapsed time, 0:24:16 cpu time, factor 3.36)
21:17:17 Running Promela ...
21:17:18 Algebraic_VCs: theory KAD.Antidomain_Semiring
21:17:19 Promela: theory Promela.PromelaStatistics
21:17:20 Promela: theory HOL-Library.IArray
21:17:20 Promela: theory LTL.LTL
21:17:20 Promela: theory Promela.PromelaAST
21:17:34 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
21:17:39 Timing Formal_SSA (4 threads, 446.867s elapsed time, 870.800s cpu time, 15.784s GC time, factor 1.95)
21:17:39 Finished Formal_SSA (0:08:38 elapsed time, 0:16:37 cpu time, factor 1.93)
21:17:39 Running SM ...
21:17:42 SM: theory SM.LTS
21:17:42 SM: theory SM.SOS_Misc_Add
21:17:43 SM: theory HOL-Library.IArray
21:17:43 SM: theory HOL-Library.Mapping
21:17:43 SM: theory SM.SM_Syntax
21:17:43 SM: theory SM.Gen_Scheduler
21:17:43 Promela: theory Promela.PromelaDatastructures
21:17:44 SM: theory SM.SM_Datastructures
21:17:44 SM: theory HOL-Library.RBT_Mapping
21:17:45 Timing LLL_Basis_Reduction (4 threads, 205.638s elapsed time, 515.084s cpu time, 18.268s GC time, factor 2.50)
21:17:45 Finished LLL_Basis_Reduction (0:04:47 elapsed time, 0:10:55 cpu time, factor 2.28)
21:17:45 Running LTL_to_GBA ...
21:17:46 SM: theory SM.Gen_Scheduler_Refine
21:17:47 CakeML_Codegen: theory CakeML_Codegen.Test_Datatypes
21:17:47 LTL_to_GBA: theory LTL.LTL
21:17:48 SM: theory SM.Gen_Cfg_Bisim
21:17:48 SM: theory SM.Pid_Scheduler
21:17:49 SM: theory SM.SM_State
21:17:51 SM: theory SM.SM_Cfg
21:17:57 SM: theory SM.SM_Semantics
21:18:03 LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA
21:18:03 SM: theory SM.Decide_Locality
21:18:04 SM: theory SM.SM_LTL
21:18:04 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Applications
21:18:04 Algebraic_VCs: theory KAD.Range_Semiring
21:18:05 SM: theory SM.Type_System
21:18:09 SM: theory SM.SM_Finite_Reachable
21:18:10 SM: theory SM.Rename_Cfg
21:18:15 LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA_impl
21:18:19 SM: theory SM.SM_Visible
21:18:21 SM: theory SM.SM_Pid
21:18:25 SM: theory SM.SM_Variables
21:18:27 SM: theory SM.SM_Indep
21:18:27 Timing CakeML_Codegen (4 threads, 492.356s elapsed time, 1432.428s cpu time, 78.232s GC time, factor 2.91)
21:18:27 Finished CakeML_Codegen (0:08:23 elapsed time, 0:39:32 cpu time, factor 4.71)
21:18:27 Running DFS_Framework ...
21:18:30 DFS_Framework: theory DFS_Framework.DFS_Framework_Misc
21:18:30 DFS_Framework: theory DFS_Framework.On_Stack
21:18:30 DFS_Framework: theory DFS_Framework.DFS_Framework_Refine_Aux
21:18:30 DFS_Framework: theory DFS_Framework.Impl_Rev_Array_Stack
21:18:32 DFS_Framework: theory DFS_Framework.DFS_Chapter_Examples
21:18:32 DFS_Framework: theory DFS_Framework.DFS_Chapter_Framework
21:18:32 DFS_Framework: theory DFS_Framework.Param_DFS
21:18:36 SM: theory SM.SM_Sticky
21:18:39 DFS_Framework: theory DFS_Framework.DFS_Invars_Basic
21:18:40 DFS_Framework: theory DFS_Framework.General_DFS_Structure
21:18:41 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra
21:18:43 DFS_Framework: theory DFS_Framework.DFS_Invars_SCC
21:18:46 SM: theory SM.SM_POR
21:18:48 DFS_Framework: theory DFS_Framework.Rec_Impl
21:18:50 DFS_Framework: theory DFS_Framework.Tailrec_Impl
21:18:54 SM: theory SM.SM_Ample_Impl
21:18:54 Timing Refine_Imperative_HOL (4 threads, 248.669s elapsed time, 595.492s cpu time, 25.992s GC time, factor 2.39)
21:18:54 Finished Refine_Imperative_HOL (0:05:19 elapsed time, 0:17:42 cpu time, factor 3.33)
21:18:54 Running Containers-Benchmarks ...
21:18:55 DFS_Framework: theory DFS_Framework.Simple_Impl
21:18:58 Containers-Benchmarks: theory HOL-Eisbach.Eisbach
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Foldi
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Prio_List
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Refine_Util_Bootstrap1
21:18:58 Containers-Benchmarks: theory Collections.ICF_Tools
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Mk_Term_Antiquot
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Mpat_Antiquot
21:18:58 Containers-Benchmarks: theory Collections.Ord_Code_Preproc
21:18:58 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Comparison
21:18:58 Containers-Benchmarks: theory Collections.Locale_Code
21:18:58 Containers-Benchmarks: theory Automatic_Refinement.Refine_Util
21:18:58 Containers-Benchmarks: theory Collections.Record_Intf
21:18:58 Containers-Benchmarks: theory Finger-Trees.FingerTree
21:18:59 Containers-Benchmarks: theory Trie.Trie
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Anti_Unification
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Attr_Comb
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Named_Sorted_Thms
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Data
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Indep_Vars
21:18:59 Containers-Benchmarks: theory Automatic_Refinement.Mk_Record_Simp
21:19:00 Containers-Benchmarks: theory Automatic_Refinement.Tagged_Solver
21:19:00 Containers-Benchmarks: theory Automatic_Refinement.Select_Solve
21:19:00 Containers-Benchmarks: theory Binomial-Heaps.BinomialHeap
21:19:00 Containers-Benchmarks: theory Binomial-Heaps.SkewBinomialHeap
21:19:01 Containers-Benchmarks: theory HOL-ex.Quicksort
21:19:02 DFS_Framework: theory DFS_Framework.Restr_Impl
21:19:03 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Default
21:19:03 Containers-Benchmarks: theory Automatic_Refinement.Misc
21:19:04 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_RBT
21:19:04 DFS_Framework: theory DFS_Framework.DFS_Framework
21:19:05 DFS_Framework: theory DFS_Framework.Cyc_Check
21:19:05 DFS_Framework: theory DFS_Framework.DFS_Find_Path
21:19:05 DFS_Framework: theory DFS_Framework.Reachable_Nodes
21:19:07 Containers-Benchmarks: theory Collections.DatRef
21:19:08 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set
21:19:10 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_Default
21:19:11 Containers-Benchmarks: theory Automatic_Refinement.Refine_Lib
21:19:13 Promela: theory Promela.PromelaInvariants
21:19:14 Algebraic_VCs: theory Algebraic_VCs.Domain_Quantale
21:19:14 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Models
21:19:14 Containers-Benchmarks: theory Collections.SetIterator
21:19:15 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Phases
21:19:15 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tagging
21:19:15 Containers-Benchmarks: theory Automatic_Refinement.Relators
21:19:15 Promela: theory Promela.Promela
21:19:16 Containers-Benchmarks: theory Collections.Sorted_List_Operations
21:19:16 Containers-Benchmarks: theory Collections.SetIteratorOperations
21:19:17 Containers-Benchmarks: theory Native_Word.Code_Target_Bits_Int
21:19:17 Containers-Benchmarks: theory Automatic_Refinement.Param_Tool
21:19:17 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Bool
21:19:17 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_LC
21:19:17 Containers-Benchmarks: theory Automatic_Refinement.Param_HOL
21:19:17 Containers-Benchmarks: theory Collections.Code_Target_ICF
21:19:18 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
21:19:18 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_LC
21:19:19 Containers-Benchmarks: theory Automatic_Refinement.Parametricity
21:19:19 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Id_Ops
21:19:20 DFS_Framework: theory DFS_Framework.Tarjan_LowLink
21:19:20 Containers-Benchmarks: theory Collections.Assoc_List
21:19:21 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Fix_Rel
21:19:21 Containers-Benchmarks: theory Collections.Diff_Array
21:19:21 DFS_Framework: theory DFS_Framework.Tarjan
21:19:22 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Translate
21:19:22 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Gen_Algo
21:19:22 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Relator_Interface
21:19:22 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tool
21:19:23 Containers-Benchmarks: theory Collections.Trie_Impl
21:19:23 Containers-Benchmarks: theory Collections.Trie2
21:19:24 Containers-Benchmarks: theory Collections.Dlist_add
21:19:24 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Bindings_HOL
21:19:24 Containers-Benchmarks: theory Collections.Proper_Iterator
21:19:25 Containers-Benchmarks: theory Collections.It_to_It
21:19:25 Containers-Benchmarks: theory Collections.SetIteratorGA
21:19:27 Containers-Benchmarks: theory Containers-Benchmarks.Clauses
21:19:27 Containers-Benchmarks: theory Refine_Monadic.Refine_Chapter
21:19:27 Containers-Benchmarks: theory Refine_Monadic.Refine_Mono_Prover
21:19:28 Containers-Benchmarks: theory Automatic_Refinement.Automatic_Refinement
21:19:28 Containers-Benchmarks: theory Collections.Idx_Iterator
21:19:28 Containers-Benchmarks: theory Refine_Monadic.Refine_Misc
21:19:30 Containers-Benchmarks: theory Refine_Monadic.RefineG_Domain
21:19:30 Containers-Benchmarks: theory Refine_Monadic.RefineG_Transfer
21:19:30 Containers-Benchmarks: theory Refine_Monadic.RefineG_Assert
21:19:30 Containers-Benchmarks: theory Refine_Monadic.RefineG_Recursion
21:19:31 Containers-Benchmarks: theory Refine_Monadic.RefineG_While
21:19:31 Containers-Benchmarks: theory Refine_Monadic.Refine_Basic
21:19:31 Algebraic_VCs: theory Algebraic_VCs.VC_KAD
21:19:32 Containers-Benchmarks: theory Refine_Monadic.Refine_Det
21:19:36 Containers-Benchmarks: theory Refine_Monadic.Refine_Heuristics
21:19:36 Containers-Benchmarks: theory Refine_Monadic.Refine_Leof
21:19:36 Containers-Benchmarks: theory Refine_Monadic.Refine_Pfun
21:19:36 Containers-Benchmarks: theory Refine_Monadic.Refine_While
21:19:36 Containers-Benchmarks: theory Refine_Monadic.Refine_More_Comb
21:19:38 Containers-Benchmarks: theory Refine_Monadic.Refine_Transfer
21:19:38 Containers-Benchmarks: theory Refine_Monadic.Autoref_Monadic
21:19:38 Containers-Benchmarks: theory Refine_Monadic.Refine_Automation
21:19:38 Containers-Benchmarks: theory Refine_Monadic.Refine_Foreach
21:19:41 Containers-Benchmarks: theory Refine_Monadic.Refine_Monadic
21:19:43 Containers-Benchmarks: theory Collections.Gen_Iterator
21:19:43 Containers-Benchmarks: theory Collections.Intf_Map
21:19:43 Containers-Benchmarks: theory Collections.Intf_Set
21:19:44 Containers-Benchmarks: theory Collections.Iterator
21:19:44 Containers-Benchmarks: theory Collections.Array_Iterator
21:19:44 Containers-Benchmarks: theory Collections.ICF_Spec_Base
21:19:44 Containers-Benchmarks: theory Collections.RBT_add
21:19:45 Containers-Benchmarks: theory Collections.AnnotatedListSpec
21:19:45 Containers-Benchmarks: theory Collections.ListSpec
21:19:45 Containers-Benchmarks: theory Collections.MapSpec
21:19:46 Containers-Benchmarks: theory Collections.PrioSpec
21:19:47 Containers-Benchmarks: theory Collections.ListGA
21:19:48 Containers-Benchmarks: theory Collections.BinoPrioImpl
21:19:48 Containers-Benchmarks: theory Collections.FTAnnotatedListImpl
21:19:48 Containers-Benchmarks: theory Collections.Fifo
21:19:52 SPARCv8: theory SPARCv8.Sparc_Init_State
21:19:52 SPARCv8: theory SPARCv8.Sparc_Code_Gen
21:19:53 Algebraic_VCs: theory Algebraic_VCs.Path_Model_Example
21:19:53 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples
21:19:53 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples2
21:19:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual
21:19:54 Algebraic_VCs: theory Algebraic_VCs.Pointer_Examples
21:19:54 Containers-Benchmarks: theory Collections.SkewPrioImpl
21:19:54 Containers-Benchmarks: theory Collections.PrioByAnnotatedList
21:19:54 Containers-Benchmarks: theory Collections.PrioUniqueSpec
21:19:54 Containers-Benchmarks: theory Collections.SetSpec
21:19:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf
21:19:56 Containers-Benchmarks: theory Collections.PrioUniqueByAnnotatedList
21:19:57 Containers-Benchmarks: theory Collections.FTPrioImpl
21:19:59 Containers-Benchmarks: theory Collections.FTPrioUniqueImpl
21:20:01 Containers-Benchmarks: theory Collections.Algos
21:20:01 Containers-Benchmarks: theory Collections.SetIndex
21:20:02 Containers-Benchmarks: theory Collections.SetIteratorCollectionsGA
21:20:02 Algebraic_VCs: theory Algebraic_VCs.KAD_is_KAT
21:20:02 Containers-Benchmarks: theory Collections.MapGA
21:20:02 Containers-Benchmarks: theory Collections.SetGA
21:20:05 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf_Examples
21:20:05 Timing Iptables_Semantics_Examples (4 threads, 403.856s elapsed time, 1544.596s cpu time, 112.644s GC time, factor 3.82)
21:20:05 Finished Iptables_Semantics_Examples (0:06:51 elapsed time, 0:25:58 cpu time, factor 3.79)
21:20:05 Running Prpu_Maxflow ...
21:20:06 Containers-Benchmarks: theory Collections.ArrayMapImpl
21:20:06 Containers-Benchmarks: theory Collections.ListMapImpl
21:20:07 Containers-Benchmarks: theory Collections.ListMapImpl_Invar
21:20:08 DFS_Framework: theory DFS_Framework.Feedback_Arcs
21:20:09 Prpu_Maxflow: theory Prpu_Maxflow.Generic_Push_Relabel
21:20:09 Prpu_Maxflow: theory Prpu_Maxflow.Graph_Topological_Ordering
21:20:09 Containers-Benchmarks: theory Collections.TrieMapImpl
21:20:11 Containers-Benchmarks: theory Collections.ArrayHashMap_Impl
21:20:13 Containers-Benchmarks: theory Collections.ListSetImpl
21:20:13 Containers-Benchmarks: theory Collections.ListSetImpl_Invar
21:20:13 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual_Examples
21:20:14 Containers-Benchmarks: theory Collections.ListSetImpl_NotDist
21:20:16 Containers-Benchmarks: theory Collections.ArrayHashMap
21:20:17 Containers-Benchmarks: theory Collections.ListSetImpl_Sorted
21:20:18 Timing SPARCv8 (4 threads, 243.489s elapsed time, 667.188s cpu time, 19.248s GC time, factor 2.74)
21:20:18 Finished SPARCv8 (0:04:21 elapsed time, 0:11:34 cpu time, factor 2.66)
21:20:18 Running Interval_Arithmetic_Word32 ...
21:20:18 Containers-Benchmarks: theory Collections.SetByMap
21:20:19 Interval_Arithmetic_Word32: theory HOL-Library.Code_Target_Int
21:20:19 Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Interval_Word32
21:20:20 Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Finite_String
21:20:20 Containers-Benchmarks: theory Collections.RBTMapImpl
21:20:20 Containers-Benchmarks: theory Collections.ArraySetImpl
21:20:21 Promela: theory Promela.PromelaLTL
21:20:21 Promela: theory Promela.PromelaLTLConv
21:20:21 Containers-Benchmarks: theory Collections.ArrayHashSet
21:20:22 DFS_Framework: theory DFS_Framework.Nested_DFS
21:20:24 Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel
21:20:24 Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Inst
21:20:25 Containers-Benchmarks: theory Collections.TrieSetImpl
21:20:26 Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Impl
21:20:26 Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front
21:20:27 Containers-Benchmarks: theory Collections.HashMap_Impl
21:20:27 Containers-Benchmarks: theory Collections.RBTSetImpl
21:20:29 Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Interpreter
21:20:29 Containers-Benchmarks: theory Collections.HashMap
21:20:34 SM: theory SM.SM_Wrapup
21:20:35 Containers-Benchmarks: theory Collections.HashSet
21:20:35 Containers-Benchmarks: theory Collections.MapStdImpl
21:20:35 Promela: theory Promela.All_Of_Promela
21:20:41 LTL_to_GBA: theory LTL_to_GBA.All_Of_LTL_to_GBA
21:20:41 Containers-Benchmarks: theory Collections.SetStdImpl
21:20:42 Timing Promela (4 threads, 196.910s elapsed time, 389.380s cpu time, 30.400s GC time, factor 1.98)
21:20:42 Finished Promela (0:03:25 elapsed time, 0:07:03 cpu time, factor 2.06)
21:20:42 Running Collections_Examples ...
21:20:44 Timing SM (4 threads, 180.196s elapsed time, 311.468s cpu time, 9.428s GC time, factor 1.73)
21:20:44 Finished SM (0:03:03 elapsed time, 0:06:19 cpu time, factor 2.07)
21:20:44 Running LOFT ...
21:20:45 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples_Chapter
21:20:45 Collections_Examples: theory Collections_Examples.Examples_Chapter
21:20:45 Collections_Examples: theory Collections_Examples.ICF_Examples_Chapter
21:20:45 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples_Chapter
21:20:45 Containers-Benchmarks: theory Collections.ICF_Impl
21:20:45 Collections_Examples: theory Containers.Equal
21:20:45 Collections_Examples: theory Containers.Extend_Partial_Order
21:20:45 Collections_Examples: theory Containers.List_Fusion
21:20:45 Collections_Examples: theory Deriving.Comparator
21:20:45 Collections_Examples: theory Containers.Closure_Set
21:20:45 Collections_Examples: theory Deriving.Derive_Manager
21:20:45 Collections_Examples: theory Deriving.Generator_Aux
21:20:46 Collections_Examples: theory HOL-Library.DAList
21:20:46 Collections_Examples: theory Deriving.Equality_Generator
21:20:46 LOFT: theory LOFT.OpenFlow_Helpers
21:20:46 LOFT: theory LOFT.Sort_Descending
21:20:47 Collections_Examples: theory Deriving.Equality_Instances
21:20:47 Collections_Examples: theory Deriving.Compare
21:20:47 Collections_Examples: theory Deriving.Comparator_Generator
21:20:47 LOFT: theory LOFT.List_Group
21:20:47 Timing LTL_to_GBA (4 threads, 173.421s elapsed time, 575.540s cpu time, 23.012s GC time, factor 3.32)
21:20:47 Finished LTL_to_GBA (0:03:02 elapsed time, 0:09:59 cpu time, factor 3.29)
21:20:47 Running Gabow_SCC ...
21:20:47 Collections_Examples: theory Containers.Containers_Auxiliary
21:20:48 Collections_Examples: theory Containers.AssocList
21:20:48 Collections_Examples: theory HOL-Library.Char_ord
21:20:48 Collections_Examples: theory HOL-Library.Omega_Words_Fun
21:20:48 Collections_Examples: theory Containers.Lexicographic_Order
21:20:48 Collections_Examples: theory Deriving.Compare_Generator
21:20:48 LOFT: theory HOL-Library.List_Lexorder
21:20:48 LOFT: theory LOFT.Semantics_OpenFlow
21:20:48 Collections_Examples: theory HOL-Library.Mapping
21:20:48 LOFT: theory LOFT.OpenFlow_Matches
21:20:48 Collections_Examples: theory Containers.Containers_Generator
21:20:48 Collections_Examples: theory Deriving.Compare_Instances
21:20:48 Collections_Examples: theory CAVA_Automata.Digraph_Basic
21:20:49 Collections_Examples: theory Containers.Collection_Enum
21:20:49 Collections_Examples: theory Containers.Collection_Eq
21:20:50 Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton
21:20:50 Gabow_SCC: theory Gabow_SCC.Find_Path
21:20:50 Collections_Examples: theory Containers.Set_Linorder
21:20:50 Collections_Examples: theory Containers.RBT_ext
21:20:50 Gabow_SCC: theory Gabow_SCC.Find_Path_Impl
21:20:51 Collections_Examples: theory Deriving.RBT_Comparator_Impl
21:20:51 Collections_Examples: theory Containers.DList_Set
21:20:51 Containers-Benchmarks: theory Collections.ICF_Refine_Monadic
21:20:51 Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
21:20:51 Containers-Benchmarks: theory Collections.ICF_Autoref
21:20:52 Collections_Examples: theory HOL-Library.Uprod
21:20:52 Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front_Impl
21:20:53 LOFT: theory LOFT.Featherweight_OpenFlow_Comparison
21:20:53 Collections_Examples: theory Collections_Examples.Exploration
21:20:53 Collections_Examples: theory Containers.TwoSat_Ex
21:20:54 Collections_Examples: theory Collections_Examples.Exploration_DFS
21:20:54 Collections_Examples: theory Collections_Examples.PerformanceTest
21:20:55 Containers-Benchmarks: theory Collections.Collections
21:20:55 Containers-Benchmarks: theory Collections.CollectionsV1
21:20:56 LOFT: theory LOFT.OpenFlow_Action
21:20:57 Gabow_SCC: theory Gabow_SCC.Gabow_SCC
21:20:57 Gabow_SCC: theory Gabow_SCC.Gabow_GBG
21:20:57 Collections_Examples: theory Collections_Examples.itp_2010
21:20:58 Collections_Examples: theory Collections_Examples.Simple_DFS
21:20:58 Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton_Code
21:20:58 LOFT: theory LOFT.OpenFlow_Serialize
21:21:04 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_ICF
21:21:04 Collections_Examples: theory Collections_Examples.Succ_Graph
21:21:05 Collections_Examples: theory Containers.Collection_Order
21:21:07 LOFT: theory LOFT.LinuxRouter_OpenFlow_Translation
21:21:08 Collections_Examples: theory Containers.RBT_Mapping2
21:21:10 Collections_Examples: theory Containers.RBT_Set2
21:21:11 Collections_Examples: theory Collections_Examples.ICF_Examples
21:21:11 LOFT: theory LOFT.OpenFlow_Documentation
21:21:11 LOFT: theory LOFT.OF_conv_test
21:21:12 Collections_Examples: theory Collections_Examples.ICF_Test
21:21:12 LOFT: theory LOFT.RFC2544
21:21:13 Collections_Examples: theory Containers.Set_Impl
21:21:13 Collections_Examples: theory Collections_Examples.Coll_Test
21:21:16 DFS_Framework: theory DFS_Framework.DFS_All_Examples
21:21:34 Collections_Examples: theory Containers.Mapping_Impl
21:21:35 Timing DFS_Framework (4 threads, 176.341s elapsed time, 591.668s cpu time, 33.072s GC time, factor 3.36)
21:21:35 Finished DFS_Framework (0:03:07 elapsed time, 0:12:09 cpu time, factor 3.90)
21:21:35 Running Mersenne_Primes ...
21:21:36 Timing Algebraic_VCs (4 threads, 276.525s elapsed time, 561.208s cpu time, 52.968s GC time, factor 2.03)
21:21:36 Finished Algebraic_VCs (0:04:43 elapsed time, 0:09:35 cpu time, factor 2.03)
21:21:36 Running Regular_Algebras ...
21:21:36 Gabow_SCC: theory Gabow_SCC.Gabow_GBG_Code
21:21:37 Gabow_SCC: theory Gabow_SCC.Gabow_SCC_Code
21:21:37 Regular_Algebras: theory Regular_Algebras.Dioid_Power_Sum
21:21:38 Collections_Examples: theory Collections_Examples.Nested_DFS
21:21:39 Regular_Algebras: theory Regular_Algebras.Regular_Algebras
21:21:39 Mersenne_Primes: theory HOL-Number_Theory.Cong
21:21:39 Mersenne_Primes: theory HOL-Number_Theory.Eratosthenes
21:21:39 Mersenne_Primes: theory HOL-Word.Traditional_Syntax
21:21:39 Mersenne_Primes: theory HOL-Word.Misc_Typedef
21:21:39 Mersenne_Primes: theory HOL-Number_Theory.Fib
21:21:39 Mersenne_Primes: theory HOL-Number_Theory.Prime_Powers
21:21:40 Mersenne_Primes: theory Pell.Pell
21:21:41 Mersenne_Primes: theory HOL-Word.Bits_Int
21:21:41 Collections_Examples: theory Collections_Examples.Combined_TwoSat
21:21:41 Mersenne_Primes: theory HOL-Number_Theory.Mod_Exp
21:21:41 Mersenne_Primes: theory HOL-Number_Theory.Totient
21:21:42 Timing Containers-Benchmarks (4 threads, 161.171s elapsed time, 518.172s cpu time, 55.008s GC time, factor 3.22)
21:21:42 Finished Containers-Benchmarks (0:02:45 elapsed time, 0:12:36 cpu time, factor 4.58)
21:21:42 Running Taylor_Models ...
21:21:42 Mersenne_Primes: theory HOL-Number_Theory.Residues
21:21:44 Mersenne_Primes: theory HOL-Word.Bit_Comprehension
21:21:45 Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
21:21:45 Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
21:21:46 Mersenne_Primes: theory HOL-Word.Word
21:21:46 Mersenne_Primes: theory Native_Word.More_Bits_Int
21:21:47 Mersenne_Primes: theory HOL-Number_Theory.Euler_Criterion
21:21:47 Mersenne_Primes: theory HOL-Number_Theory.Gauss
21:21:48 Mersenne_Primes: theory HOL-Number_Theory.Quadratic_Reciprocity
21:21:48 Mersenne_Primes: theory HOL-Number_Theory.Pocklington
21:21:49 Mersenne_Primes: theory HOL-Number_Theory.Residue_Primitive_Roots
21:21:49 Mersenne_Primes: theory HOL-Number_Theory.Number_Theory
21:21:51 Mersenne_Primes: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
21:21:51 Mersenne_Primes: theory Probabilistic_Prime_Tests.Legendre_Symbol
21:21:52 Mersenne_Primes: theory HOL-Word.Reversed_Bit_Lists
21:21:53 Mersenne_Primes: theory Probabilistic_Prime_Tests.Jacobi_Symbol
21:21:54 Mersenne_Primes: theory HOL-Word.Misc_lsb
21:21:54 Mersenne_Primes: theory HOL-Word.Misc_msb
21:21:54 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Auxiliary
21:21:54 Mersenne_Primes: theory HOL-Word.Misc_set_bit
21:21:56 Mersenne_Primes: theory Native_Word.Code_Symbolic_Bits_Int
21:21:57 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer
21:21:57 Mersenne_Primes: theory Native_Word.Bits_Integer
21:21:58 Collections_Examples: theory Collections_Examples.Foreach_Refine
21:22:06 Taylor_Models: theory Taylor_Models.Polynomial_Expression
21:22:09 Collections_Examples: theory Collections_Examples.ICF_Only_Test
21:22:10 Collections_Examples: theory Collections_Examples.Refine_Fold
21:22:10 Collections_Examples: theory Collections_Examples.Bfs_Impl
21:22:12 Mersenne_Primes: theory Native_Word.Code_Target_Bits_Int
21:22:13 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Code
21:22:27 Prpu_Maxflow: theory Prpu_Maxflow.Generated_Code_Test
21:22:33 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples
21:22:35 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples
21:22:37 Taylor_Models: theory HOL-Library.Function_Algebras
21:22:37 Taylor_Models: theory Taylor_Models.Horner_Eval
21:22:37 Taylor_Models: theory Taylor_Models.Float_Topology
21:22:37 Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
21:22:38 Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
21:22:41 Taylor_Models: theory Taylor_Models.Taylor_Models
21:22:52 Regular_Algebras: theory Regular_Algebras.Pratts_Counterexamples
21:22:52 Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Models
21:22:55 Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Variants
21:22:57 Timing Prpu_Maxflow (4 threads, 161.815s elapsed time, 311.720s cpu time, 8.036s GC time, factor 1.93)
21:22:57 Finished Prpu_Maxflow (0:02:51 elapsed time, 0:06:36 cpu time, factor 2.32)
21:22:57 Running MFOTL_Monitor ...
21:23:00 MFOTL_Monitor: theory MFOTL_Monitor.Trace
21:23:00 MFOTL_Monitor: theory MFOTL_Monitor.Interval
21:23:00 MFOTL_Monitor: theory MFOTL_Monitor.Table
21:23:01 MFOTL_Monitor: theory MFOTL_Monitor.MFOTL
21:23:02 Timing Interval_Arithmetic_Word32 (4 threads, 155.826s elapsed time, 506.936s cpu time, 12.940s GC time, factor 3.25)
21:23:02 Finished Interval_Arithmetic_Word32 (0:02:43 elapsed time, 0:08:40 cpu time, factor 3.19)
21:23:02 Running LTL_Master_Theorem ...
21:23:04 Gabow_SCC: theory Gabow_SCC.All_Of_Gabow_SCC
21:23:05 LTL_Master_Theorem: theory Deriving.Comparator
21:23:05 LTL_Master_Theorem: theory Deriving.Derive_Manager
21:23:05 LTL_Master_Theorem: theory HOL-Library.Char_ord
21:23:05 LTL_Master_Theorem: theory Deriving.Generator_Aux
21:23:06 LTL_Master_Theorem: theory HOL-Library.Mapping
21:23:06 LTL_Master_Theorem: theory LTL_Master_Theorem.Omega_Words_Fun_Stream
21:23:06 LTL_Master_Theorem: theory Deriving.Equality_Generator
21:23:06 LTL_Master_Theorem: theory Deriving.Hash_Generator
21:23:07 LTL_Master_Theorem: theory Deriving.Equality_Instances
21:23:07 LTL_Master_Theorem: theory Deriving.Countable_Generator
21:23:07 LTL_Master_Theorem: theory Deriving.Compare
21:23:07 LTL_Master_Theorem: theory Deriving.Comparator_Generator
21:23:07 LTL_Master_Theorem: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
21:23:08 LTL_Master_Theorem: theory HOL-Library.AList_Mapping
21:23:08 LTL_Master_Theorem: theory Deriving.Hash_Instances
21:23:08 LTL_Master_Theorem: theory HOL-Library.FSet
21:23:08 LTL_Master_Theorem: theory HOL-Library.Log_Nat
21:23:08 LTL_Master_Theorem: theory Deriving.Compare_Generator
21:23:08 LTL_Master_Theorem: theory LTL.LTL
21:23:09 LTL_Master_Theorem: theory Deriving.Compare_Instances
21:23:09 Collections_Examples: theory Collections_Examples.Collection_Examples
21:23:10 LTL_Master_Theorem: theory Deriving.Derive
21:23:10 Taylor_Models: theory Taylor_Models.Experiments
21:23:10 MFOTL_Monitor: theory MFOTL_Monitor.Abstract_Monitor
21:23:11 MFOTL_Monitor: theory MFOTL_Monitor.Monitor
21:23:11 LTL_Master_Theorem: theory LTL_Master_Theorem.Quotient_Type
21:23:12 Timing Gabow_SCC (4 threads, 135.205s elapsed time, 347.280s cpu time, 8.588s GC time, factor 2.57)
21:23:12 Finished Gabow_SCC (0:02:24 elapsed time, 0:06:39 cpu time, factor 2.77)
21:23:12 Running Separation_Logic_Imperative_HOL ...
21:23:13 LTL_Master_Theorem: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
21:23:14 Separation_Logic_Imperative_HOL: theory HOL-Eisbach.Eisbach
21:23:14 Separation_Logic_Imperative_HOL: theory HOL-ex.Quicksort
21:23:14 Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_Typedef
21:23:14 Separation_Logic_Imperative_HOL: theory HOL-Word.Traditional_Syntax
21:23:14 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap
21:23:15 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Syntax_Match
21:23:15 Separation_Logic_Imperative_HOL: theory Automatic_Refinement.Misc
21:23:15 Separation_Logic_Imperative_HOL: theory HOL-Word.Bits_Int
21:23:16 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
21:23:17 Timing Collections_Examples (4 threads, 146.089s elapsed time, 468.092s cpu time, 17.672s GC time, factor 3.20)
21:23:17 Finished Collections_Examples (0:02:33 elapsed time, 0:14:55 cpu time, factor 5.82)
21:23:17 Running Multirelations ...
21:23:18 Separation_Logic_Imperative_HOL: theory HOL-Word.Bit_Comprehension
21:23:18 Multirelations: theory Multirelations.C_Algebras
21:23:19 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Array
21:23:19 Separation_Logic_Imperative_HOL: theory HOL-Word.Word
21:23:19 Separation_Logic_Imperative_HOL: theory Native_Word.More_Bits_Int
21:23:20 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Ref
21:23:20 Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
21:23:20 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
21:23:21 Timing LOFT (4 threads, 146.831s elapsed time, 514.676s cpu time, 17.816s GC time, factor 3.51)
21:23:21 Finished LOFT (0:02:37 elapsed time, 0:09:03 cpu time, factor 3.46)
21:23:21 Running EdmondsKarp_Maxflow ...
21:23:24 Timing Regular_Algebras (4 threads, 100.825s elapsed time, 166.200s cpu time, 4.136s GC time, factor 1.65)
21:23:24 Finished Regular_Algebras (0:01:47 elapsed time, 0:03:12 cpu time, factor 1.79)
21:23:24 Running HOL-Word-SMT_Examples ...
21:23:24 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
21:23:24 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.FordFulkerson_Algo
21:23:24 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
21:23:25 LTL_Master_Theorem: theory LTL.Equivalence_Relations
21:23:25 LTL_Master_Theorem: theory LTL.Rewriting
21:23:25 LTL_Master_Theorem: theory LTL_Master_Theorem.Syntactic_Fragments_and_Stability
21:23:25 Timing Mersenne_Primes (4 threads, 99.997s elapsed time, 338.308s cpu time, 9.748s GC time, factor 3.38)
21:23:25 Finished Mersenne_Primes (0:01:48 elapsed time, 0:06:40 cpu time, factor 3.67)
21:23:25 Running Dijkstra_Shortest_Path ...
21:23:25 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie
21:23:25 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples
21:23:25 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests
21:23:25 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples
21:23:26 Separation_Logic_Imperative_HOL: theory HOL-Word.Reversed_Bit_Lists
21:23:29 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Graph
21:23:29 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Misc
21:23:29 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Introduction
21:23:29 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Weight
21:23:29 Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_lsb
21:23:29 Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_msb
21:23:29 Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_set_bit
21:23:30 LTL_Master_Theorem: theory LTL.Code_Equations
21:23:30 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphSpec
21:23:31 LTL_Master_Theorem: theory LTL.Disjunctive_Normal_Form
21:23:32 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Symbolic_Bits_Int
21:23:33 Separation_Logic_Imperative_HOL: theory Native_Word.Bits_Integer
21:23:34 LTL_Master_Theorem: theory LTL_Master_Theorem.After
21:23:34 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra
21:23:36 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Algo
21:23:38 LTL_Master_Theorem: theory LTL_Master_Theorem.Advice
21:23:39 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphGA
21:23:40 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphByMap
21:23:40 LTL_Master_Theorem: theory LTL_Master_Theorem.Asymmetric_Master_Theorem
21:23:40 LTL_Master_Theorem: theory LTL_Master_Theorem.Extra_Equivalence_Relations
21:23:41 LTL_Master_Theorem: theory LTL_Master_Theorem.Master_Theorem
21:23:41 LTL_Master_Theorem: theory LTL_Master_Theorem.Transition_Functions
21:23:41 LTL_Master_Theorem: theory LTL_Master_Theorem.Restricted_Master_Theorem
21:23:41 Multirelations: theory Multirelations.Multirelations
21:23:42 LTL_Master_Theorem: theory LTL_Master_Theorem.DRA_Construction
21:23:43 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.HashGraphImpl
21:23:46 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
21:23:47 Timing Taylor_Models (4 threads, 116.907s elapsed time, 308.180s cpu time, 10.584s GC time, factor 2.64)
21:23:47 Finished Taylor_Models (0:02:05 elapsed time, 0:05:22 cpu time, factor 2.57)
21:23:47 Running Buchi_Complementation ...
21:23:48 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Impl
21:23:48 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
21:23:48 LTL_Master_Theorem: theory LTL_Master_Theorem.DRA_Implementation
21:23:50 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Bits_Int
21:23:51 Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Word_Base
21:23:51 Buchi_Complementation: theory Buchi_Complementation.Alternate
21:23:51 Buchi_Complementation: theory Buchi_Complementation.Formula
21:23:51 Buchi_Complementation: theory HOL-Library.Permutation
21:23:51 Buchi_Complementation: theory HOL-Library.Lattice_Syntax
21:23:51 Buchi_Complementation: theory Buchi_Complementation.Graph
21:23:51 Separation_Logic_Imperative_HOL: theory Collections.Code_Target_ICF
21:23:51 Separation_Logic_Imperative_HOL: theory Native_Word.Uint32
21:23:51 Buchi_Complementation: theory Buchi_Complementation.Ranking
21:23:53 Buchi_Complementation: theory Buchi_Complementation.Complementation
21:23:53 Separation_Logic_Imperative_HOL: theory Collections.HashCode
21:23:54 Buchi_Complementation: theory Buchi_Complementation.Complementation_Implement
21:23:58 LTL_Master_Theorem: theory LTL_Master_Theorem.DRA_Instantiation
21:23:58 Timing CAVA_Setup (4 threads, 659.959s elapsed time, 2370.796s cpu time, 322.580s GC time, factor 3.59)
21:23:58 Finished CAVA_Setup (0:14:12 elapsed time, 0:48:20 cpu time, factor 3.40)
21:23:58 Running CAVA_LTL_Modelchecker ...
21:24:03 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
21:24:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
21:24:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
21:24:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
21:24:10 Buchi_Complementation: theory Buchi_Complementation.Complementation_Final
21:24:12 Separation_Logic_Imperative_HOL: theory Collections.Partial_Equivalence_Relation
21:24:12 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Run
21:24:12 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Assertions
21:24:13 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Checked_Impl
21:24:13 LTL_Master_Theorem: theory LTL_Master_Theorem.Code_Export
21:24:14 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hoare_Triple
21:24:15 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Automation
21:24:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Main
21:24:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Table
21:24:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
21:24:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
21:24:16 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
21:24:17 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.List_Seg
21:24:17 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Union_Find
21:24:18 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Circ_List
21:24:18 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Open_List
21:24:21 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map
21:24:23 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
21:24:28 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
21:24:28 MFOTL_Monitor: theory MFOTL_Monitor.Monitor_Code
21:24:34 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Idioms
21:24:35 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.To_List_GA
21:24:38 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Blit
21:24:38 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
21:24:39 MFOTL_Monitor: theory MFOTL_Monitor.Examples
21:24:40 Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Test
21:24:40 Buchi_Complementation: theory Buchi_Complementation.Complementation_Build
21:24:43 EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Benchmark_Export
21:24:48 Timing Multirelations (4 threads, 85.294s elapsed time, 215.828s cpu time, 6.660s GC time, factor 2.53)
21:24:48 Finished Multirelations (0:01:30 elapsed time, 0:13:03 cpu time, factor 8.62)
21:24:48 Running LLL_Factorization ...
21:24:51 Timing Dijkstra_Shortest_Path (4 threads, 77.787s elapsed time, 130.720s cpu time, 4.268s GC time, factor 1.68)
21:24:51 Finished Dijkstra_Shortest_Path (0:01:25 elapsed time, 0:05:30 cpu time, factor 3.86)
21:24:51 Running VerifyThis2018 ...
21:24:52 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
21:24:52 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
21:24:53 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.From_List_GA
21:24:54 VerifyThis2018: theory VerifyThis2018.Synth_Definition
21:24:54 VerifyThis2018: theory VerifyThis2018.Dynamic_Array
21:24:54 VerifyThis2018: theory VerifyThis2018.DRAT_Misc
21:24:54 VerifyThis2018: theory VerifyThis2018.DF_System
21:24:54 Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Examples
21:24:54 VerifyThis2018: theory VerifyThis2018.Exc_Nres_Monad
21:24:54 LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
21:24:54 LLL_Factorization: theory LLL_Factorization.Sub_Sums
21:24:54 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
21:24:54 Timing LTL_Master_Theorem (4 threads, 102.050s elapsed time, 370.064s cpu time, 23.356s GC time, factor 3.63)
21:24:54 Finished LTL_Master_Theorem (0:01:51 elapsed time, 0:06:25 cpu time, factor 3.47)
21:24:54 Running Adaptive_State_Counting ...
21:24:54 VerifyThis2018: theory VerifyThis2018.Array_Map_Default
21:24:54 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
21:24:56 VerifyThis2018: theory VerifyThis2018.VTcomp
21:24:56 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
21:24:57 Adaptive_State_Counting: theory HOL-Hoare.Hoare_Logic
21:24:57 Adaptive_State_Counting: theory Adaptive_State_Counting.FSM
21:24:57 Timing HOL-Word-SMT_Examples (4 threads, 90.952s elapsed time, 129.452s cpu time, 1.588s GC time, factor 1.42)
21:24:57 Finished HOL-Word-SMT_Examples (0:01:32 elapsed time, 0:02:15 cpu time, factor 1.46)
21:24:57 Running Tree-Automata ...
21:24:59 VerifyThis2018: theory VerifyThis2018.Snippets
21:24:59 Tree-Automata: theory Tree-Automata.Tree
21:24:59 Tree-Automata: theory Collections_Examples.Exploration
21:25:00 Timing Buchi_Complementation (4 threads, 64.132s elapsed time, 128.532s cpu time, 2.812s GC time, factor 2.00)
21:25:00 Finished Buchi_Complementation (0:01:12 elapsed time, 0:02:36 cpu time, factor 2.17)
21:25:00 Building Relation_Algebra ...
21:25:00 Timing EdmondsKarp_Maxflow (4 threads, 90.829s elapsed time, 133.772s cpu time, 3.480s GC time, factor 1.47)
21:25:00 Finished EdmondsKarp_Maxflow (0:01:38 elapsed time, 0:03:00 cpu time, factor 1.84)
21:25:00 Running Linear_Inequalities ...
21:25:00 Timing Separation_Logic_Imperative_HOL (4 threads, 101.273s elapsed time, 249.024s cpu time, 8.620s GC time, factor 2.46)
21:25:00 Finished Separation_Logic_Imperative_HOL (0:01:47 elapsed time, 0:07:23 cpu time, factor 4.12)
21:25:00 Running Partial_Order_Reduction ...
21:25:00 Tree-Automata: theory Tree-Automata.Ta
21:25:01 Relation_Algebra: theory Relation_Algebra.More_Boolean_Algebra
21:25:01 LLL_Factorization: theory LLL_Factorization.LLL_Factorization
21:25:02 Adaptive_State_Counting: theory Adaptive_State_Counting.ATC
21:25:02 Adaptive_State_Counting: theory Adaptive_State_Counting.FSM_Product
21:25:02 Relation_Algebra: theory Relation_Algebra.Relation_Algebra
21:25:03 Partial_Order_Reduction: theory HOL-Library.Case_Converter
21:25:03 Partial_Order_Reduction: theory Partial_Order_Reduction.Basic_Extensions
21:25:03 Partial_Order_Reduction: theory Partial_Order_Reduction.Set_Extensions
21:25:03 Partial_Order_Reduction: theory HOL-Library.Lattice_Syntax
21:25:03 Partial_Order_Reduction: theory HOL-Library.Complete_Partial_Order2
21:25:04 Partial_Order_Reduction: theory Partial_Order_Reduction.Functions
21:25:04 Partial_Order_Reduction: theory HOL-Library.Simps_Case_Conv
21:25:04 Partial_Order_Reduction: theory HOL-Library.Prefix_Order
21:25:04 Partial_Order_Reduction: theory Partial_Order_Reduction.Relation_Extensions
21:25:04 Partial_Order_Reduction: theory Partial_Order_Reduction.List_Extensions
21:25:04 Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
21:25:04 Partial_Order_Reduction: theory Partial_Order_Reduction.List_Prefixes
21:25:04 Partial_Order_Reduction: theory LTL.LTL
21:25:04 Partial_Order_Reduction: theory Stuttering_Equivalence.Samplers
21:25:04 Partial_Order_Reduction: theory Partial_Order_Reduction.Word_Prefixes
21:25:05 Partial_Order_Reduction: theory Stuttering_Equivalence.StutterEquivalence
21:25:05 Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
21:25:05 Partial_Order_Reduction: theory Partial_Order_Reduction.Traces
21:25:05 Partial_Order_Reduction: theory Partial_Order_Reduction.Transition_System_Extensions
21:25:05 Tree-Automata: theory Tree-Automata.AbsAlgo
21:25:05 Adaptive_State_Counting: theory Adaptive_State_Counting.ASC_LB
21:25:06 Timing HOL-ODE-Numerics (4 threads, 1427.180s elapsed time, 4925.228s cpu time, 480.200s GC time, factor 3.45)
21:25:06 Finished HOL-ODE-Numerics (0:27:12 elapsed time, 1:30:55 cpu time, factor 3.34)
21:25:06 Timing MFOTL_Monitor (4 threads, 117.136s elapsed time, 260.664s cpu time, 5.980s GC time, factor 2.23)
21:25:06 Finished MFOTL_Monitor (0:02:04 elapsed time, 0:04:34 cpu time, factor 2.20)
21:25:06 Building Lorenz_Approximation ...
21:25:06 Running HOL-ODE-ARCH-COMP ...
21:25:07 Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
21:25:07 Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
21:25:07 Partial_Order_Reduction: theory Partial_Order_Reduction.Transition_System_Traces
21:25:07 Partial_Order_Reduction: theory Coinductive.Coinductive_Nat
21:25:07 Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
21:25:09 Partial_Order_Reduction: theory Coinductive.Coinductive_List
21:25:09 Partial_Order_Reduction: theory Partial_Order_Reduction.ENat_Extensions
21:25:09 Partial_Order_Reduction: theory Partial_Order_Reduction.CCPO_Extensions
21:25:09 Adaptive_State_Counting: theory Adaptive_State_Counting.ASC_Suite
21:25:09 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Models
21:25:09 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_RTC
21:25:09 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Tests
21:25:09 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Vectors
21:25:09 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
21:25:09 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
21:25:10 Partial_Order_Reduction: theory Partial_Order_Reduction.ESet_Extensions
21:25:10 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Functions
21:25:11 VerifyThis2018: theory VerifyThis2018.Challenge1_short
21:25:11 VerifyThis2018: theory VerifyThis2018.Challenge1
21:25:11 VerifyThis2018: theory VerifyThis2018.Challenge2
21:25:11 VerifyThis2018: theory VerifyThis2018.Challenge3
21:25:11 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
21:25:14 Tree-Automata: theory Tree-Automata.Ta_impl
21:25:14 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
21:25:14 Linear_Inequalities: theory Linear_Inequalities.Cone
21:25:16 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
21:25:16 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Direct_Products
21:25:17 Partial_Order_Reduction: theory Coinductive.Coinductive_List_Prefix
21:25:17 Partial_Order_Reduction: theory Coinductive.Coinductive_Stream
21:25:18 Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
21:25:19 Partial_Order_Reduction: theory Partial_Order_Reduction.Coinductive_List_Extensions
21:25:21 Partial_Order_Reduction: theory Stuttering_Equivalence.PLTL
21:25:21 Partial_Order_Reduction: theory Partial_Order_Reduction.LList_Prefixes
21:25:22 Partial_Order_Reduction: theory Partial_Order_Reduction.Stuttering
21:25:23 Partial_Order_Reduction: theory Partial_Order_Reduction.Formula
21:25:23 Partial_Order_Reduction: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
21:25:23 Adaptive_State_Counting: theory Adaptive_State_Counting.ASC_Sufficiency
21:25:23 Adaptive_State_Counting: theory Adaptive_State_Counting.ASC_Hoare
21:25:24 Partial_Order_Reduction: theory Partial_Order_Reduction.Ample_Abstract
21:25:25 Partial_Order_Reduction: theory Partial_Order_Reduction.Ample_Analysis
21:25:25 Partial_Order_Reduction: theory Partial_Order_Reduction.Ample_Correctness
21:25:25 Adaptive_State_Counting: theory Adaptive_State_Counting.ASC_Example
21:25:26 Linear_Inequalities: theory Linear_Inequalities.Dim_Span
21:25:26 Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
21:25:29 Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
21:25:33 Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
21:25:33 Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
21:25:35 Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
21:25:38 Tree-Automata: theory Tree-Automata.Ta_impl_codegen
21:25:40 Timing Relation_Algebra (4 threads, 18.072s elapsed time, 56.696s cpu time, 2.164s GC time, factor 3.14)
21:25:40 Finished Relation_Algebra (0:00:39 elapsed time, 0:01:34 cpu time, factor 2.37)
21:25:40 Running HOL-ODE-Examples ...
21:25:42 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
21:25:42 Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
21:25:43 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
21:25:43 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
21:25:43 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
21:25:45 Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
21:25:51 Timing VerifyThis2018 (4 threads, 52.460s elapsed time, 148.904s cpu time, 2.912s GC time, factor 2.84)
21:25:51 Finished VerifyThis2018 (0:00:59 elapsed time, 0:03:04 cpu time, factor 3.11)
21:25:51 Running Poincare_Bendixson ...
21:25:52 Timing Partial_Order_Reduction (4 threads, 41.826s elapsed time, 152.680s cpu time, 7.588s GC time, factor 3.65)
21:25:52 Finished Partial_Order_Reduction (0:00:50 elapsed time, 0:02:53 cpu time, factor 3.44)
21:25:52 Running Residuated_Lattices ...
21:25:53 Residuated_Lattices: theory Residuated_Lattices.Residuated_Lattices
21:25:54 Timing LLL_Factorization (4 threads, 55.191s elapsed time, 147.392s cpu time, 3.892s GC time, factor 2.67)
21:25:54 Finished LLL_Factorization (0:01:04 elapsed time, 0:02:42 cpu time, factor 2.52)
21:25:54 Timing Adaptive_State_Counting (4 threads, 48.556s elapsed time, 172.740s cpu time, 6.212s GC time, factor 3.56)
21:25:54 Finished Adaptive_State_Counting (0:00:59 elapsed time, 0:03:09 cpu time, factor 3.20)
21:25:54 Running Kruskal ...
21:25:54 Running ROBDD ...
21:25:54 Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
21:25:54 Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
21:25:56 Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
21:25:56 Timing Tree-Automata (4 threads, 50.894s elapsed time, 91.316s cpu time, 2.856s GC time, factor 1.79)
21:25:56 Finished Tree-Automata (0:00:58 elapsed time, 0:01:45 cpu time, factor 1.80)
21:25:56 Running IEEE_Floating_Point ...
21:25:57 ROBDD: theory ROBDD.Option_Helpers
21:25:57 ROBDD: theory ROBDD.Bool_Func
21:25:57 ROBDD: theory ROBDD.Array_List
21:25:57 ROBDD: theory ROBDD.Pointer_Map
21:25:57 Kruskal: theory Kruskal.SeprefUF
21:25:57 Kruskal: theory Kruskal.Kruskal_Misc
21:25:57 ROBDD: theory ROBDD.BDT
21:25:57 ROBDD: theory ROBDD.Pointer_Map_Impl
21:25:58 IEEE_Floating_Point: theory HOL-Library.Adhoc_Overloading
21:25:58 IEEE_Floating_Point: theory HOL-Library.Code_Target_Int
21:25:58 IEEE_Floating_Point: theory HOL-Library.Code_Abstract_Nat
21:25:58 IEEE_Floating_Point: theory HOL-Library.Lattice_Algebras
21:25:58 IEEE_Floating_Point: theory HOL-Library.Code_Target_Nat
21:25:58 IEEE_Floating_Point: theory HOL-Library.Monad_Syntax
21:25:58 IEEE_Floating_Point: theory HOL-Library.Log_Nat
21:25:58 IEEE_Floating_Point: theory HOL-Library.Code_Target_Numeral
21:26:00 Timing Linear_Inequalities (4 threads, 49.613s elapsed time, 143.880s cpu time, 4.724s GC time, factor 2.90)
21:26:00 Finished Linear_Inequalities (0:00:59 elapsed time, 0:02:40 cpu time, factor 2.68)
21:26:00 Running Show ...
21:26:00 Kruskal: theory Dijkstra_Shortest_Path.Graph
21:26:00 Kruskal: theory HOL-Library.Uprod
21:26:00 Kruskal: theory Dijkstra_Shortest_Path.Weight
21:26:00 Kruskal: theory Matroids.Indep_System
21:26:01 Poincare_Bendixson: theory Poincare_Bendixson.Invariance
21:26:01 Kruskal: theory Matroids.Matroid
21:26:02 ROBDD: theory ROBDD.Abstract_Impl
21:26:02 Kruskal: theory Kruskal.UGraph
21:26:02 Show: theory HOL-Computational_Algebra.Factorial_Ring
21:26:02 Show: theory Show.Show
21:26:02 Kruskal: theory Kruskal.MinWeightBasis
21:26:03 Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
21:26:03 Kruskal: theory Kruskal.Kruskal
21:26:03 Kruskal: theory Kruskal.Kruskal_Refine
21:26:04 Show: theory Show.Show_Instances
21:26:04 Show: theory Show.Show_Real
21:26:04 Kruskal: theory Kruskal.Kruskal_Impl
21:26:04 IEEE_Floating_Point: theory HOL-Library.Float
21:26:04 Kruskal: theory Kruskal.Graph_Definition
21:26:04 Show: theory Show.Show_Complex
21:26:05 Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
21:26:05 ROBDD: theory ROBDD.Middle_Impl
21:26:06 Show: theory Show.Show_Real_Impl
21:26:06 Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
21:26:06 Residuated_Lattices: theory Residuated_Lattices.Action_Algebra
21:26:06 Residuated_Lattices: theory Residuated_Lattices.Involutive_Residuated
21:26:06 Residuated_Lattices: theory Residuated_Lattices.Residuated_Boolean_Algebras
21:26:07 Kruskal: theory Kruskal.Graph_Definition_Aux
21:26:08 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE
21:26:08 Kruskal: theory Kruskal.UGraph_Impl
21:26:08 ROBDD: theory ROBDD.Conc_Impl
21:26:08 Kruskal: theory Kruskal.Graph_Definition_Impl
21:26:12 ROBDD: theory ROBDD.Level_Collapse
21:26:12 ROBDD: theory ROBDD.BDD_Examples
21:26:12 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
21:26:12 CAVA_LTL_Modelchecker: theory LTL.Rewriting
21:26:12 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
21:26:12 IEEE_Floating_Point: theory IEEE_Floating_Point.FP64
21:26:12 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Properties
21:26:13 Poincare_Bendixson: theory Poincare_Bendixson.Examples
21:26:13 Residuated_Lattices: theory Residuated_Lattices.Residuated_Relation_Algebra
21:26:13 Residuated_Lattices: theory Residuated_Lattices.Action_Algebra_Models
21:26:13 IEEE_Floating_Point: theory IEEE_Floating_Point.Conversion_IEEE_Float
21:26:14 IEEE_Floating_Point: theory IEEE_Floating_Point.Double
21:26:15 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
21:26:15 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
21:26:15 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
21:26:16 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
21:26:16 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
21:26:17 Show: theory HOL-Computational_Algebra.Polynomial
21:26:17 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
21:26:23 ROBDD: theory ROBDD.BDD_Code
21:26:24 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
21:26:28 Show: theory Show.Show_Poly
21:26:32 Timing IEEE_Floating_Point (4 threads, 29.937s elapsed time, 89.468s cpu time, 2.164s GC time, factor 2.99)
21:26:32 Finished IEEE_Floating_Point (0:00:35 elapsed time, 0:01:40 cpu time, factor 2.83)
21:26:32 Timing ROBDD (4 threads, 30.737s elapsed time, 87.396s cpu time, 2.152s GC time, factor 2.84)
21:26:32 Finished ROBDD (0:00:38 elapsed time, 0:01:41 cpu time, factor 2.68)
21:26:32 Running VerifyThis2019 ...
21:26:32 Running Knuth_Morris_Pratt ...
21:26:34 Timing Show (4 threads, 27.672s elapsed time, 63.532s cpu time, 2.612s GC time, factor 2.30)
21:26:34 Finished Show (0:00:33 elapsed time, 0:01:14 cpu time, factor 2.23)
21:26:34 Timing Residuated_Lattices (4 threads, 36.909s elapsed time, 68.792s cpu time, 2.084s GC time, factor 1.86)
21:26:34 Finished Residuated_Lattices (0:00:42 elapsed time, 0:01:20 cpu time, factor 1.88)
21:26:34 Building HOL-SPARK ...
21:26:34 Running Floyd_Warshall ...
21:26:35 Knuth_Morris_Pratt: theory HOL-Library.Sublist
21:26:35 VerifyThis2019: theory VerifyThis2019.Exc_Nres_Monad
21:26:35 Timing Kruskal (4 threads, 33.567s elapsed time, 113.208s cpu time, 3.536s GC time, factor 3.37)
21:26:35 Finished Kruskal (0:00:40 elapsed time, 0:02:34 cpu time, factor 3.78)
21:26:35 Running Separation_Algebra ...
21:26:36 HOL-SPARK: theory HOL-SPARK.SPARK_Setup
21:26:37 Separation_Algebra: theory HOL-Hoare.Hoare_Logic_Abort
21:26:37 Separation_Algebra: theory Separation_Algebra.Types_D
21:26:37 Separation_Algebra: theory Separation_Algebra.Map_Extra
21:26:37 Separation_Algebra: theory Separation_Algebra.Separation_Algebra
21:26:37 Knuth_Morris_Pratt: theory Knuth_Morris_Pratt.KMP
21:26:38 Separation_Algebra: theory Separation_Algebra.Separation_Algebra_Alt
21:26:38 Floyd_Warshall: theory Floyd_Warshall.Floyd_Warshall
21:26:38 Floyd_Warshall: theory Floyd_Warshall.Recursion_Combinators
21:26:38 VerifyThis2019: theory VerifyThis2019.VTcomp
21:26:39 Separation_Algebra: theory Separation_Algebra.Sep_Heap_Instance
21:26:39 Separation_Algebra: theory Separation_Algebra.Sep_Tactics
21:26:39 HOL-SPARK: theory HOL-SPARK.SPARK
21:26:39 Separation_Algebra: theory Separation_Algebra.Sep_Eq
21:26:39 Separation_Algebra: theory Separation_Algebra.Sep_Tactics_Test
21:26:39 Separation_Algebra: theory Separation_Algebra.Simple_Separation_Example
21:26:40 Separation_Algebra: theory Separation_Algebra.VM_Example
21:26:40 VerifyThis2019: theory VerifyThis2019.Parallel_Multiset_Fold
21:26:40 VerifyThis2019: theory VerifyThis2019.Challenge1A
21:26:40 VerifyThis2019: theory VerifyThis2019.Challenge2A
21:26:40 VerifyThis2019: theory VerifyThis2019.Challenge3
21:26:42 VerifyThis2019: theory VerifyThis2019.Challenge1B
21:26:44 Separation_Algebra: theory Separation_Algebra.Abstract_Separation_D
21:26:46 Floyd_Warshall: theory Floyd_Warshall.FW_Code
21:26:47 Separation_Algebra: theory Separation_Algebra.Separation_D
21:26:51 Timing HOL-SPARK (4 threads, 3.502s elapsed time, 4.528s cpu time, 0.000s GC time, factor 1.29)
21:26:51 Finished HOL-SPARK (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.35)
21:26:51 Building HOL-SPARK-Examples ...
21:26:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas
21:26:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor
21:26:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence
21:26:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD
21:26:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt
21:26:54 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification
21:26:55 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F
21:26:55 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash
21:26:55 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L
21:26:55 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R
21:26:55 VerifyThis2019: theory VerifyThis2019.Challenge2B
21:26:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L
21:26:56 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R
21:26:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round
21:26:58 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L
21:26:58 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R
21:26:59 Timing Separation_Algebra (4 threads, 17.403s elapsed time, 46.304s cpu time, 2.124s GC time, factor 2.66)
21:26:59 Finished Separation_Algebra (0:00:23 elapsed time, 0:00:58 cpu time, factor 2.48)
21:26:59 Timing Floyd_Warshall (4 threads, 16.331s elapsed time, 55.788s cpu time, 1.304s GC time, factor 3.42)
21:26:59 Finished Floyd_Warshall (0:00:23 elapsed time, 0:01:17 cpu time, factor 3.25)
21:26:59 Running Old_Datatype_Show ...
21:26:59 Running Minimal_SSA ...
21:27:01 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
21:27:01 Timing VerifyThis2019 (4 threads, 21.635s elapsed time, 43.268s cpu time, 1.276s GC time, factor 2.00)
21:27:01 Finished VerifyThis2019 (0:00:28 elapsed time, 0:02:25 cpu time, factor 5.16)
21:27:01 Timing Knuth_Morris_Pratt (4 threads, 21.701s elapsed time, 67.500s cpu time, 1.328s GC time, factor 3.11)
21:27:01 Finished Knuth_Morris_Pratt (0:00:28 elapsed time, 0:01:19 cpu time, factor 2.79)
21:27:01 Running Transitive-Closure ...
21:27:01 Running HOL-SPARK-Manual ...
21:27:02 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
21:27:02 Minimal_SSA: theory Minimal_SSA.Irreducible
21:27:02 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Complex_Types
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Examples.Greatest_Common_Divisor
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc1
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles
21:27:03 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification
21:27:03 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
21:27:03 Transitive-Closure: theory Matrix.Utility
21:27:03 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
21:27:04 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
21:27:04 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
21:27:04 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
21:27:04 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
21:27:10 Timing Transitive-Closure (4 threads, 3.150s elapsed time, 10.340s cpu time, 0.360s GC time, factor 3.28)
21:27:10 Finished Transitive-Closure (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.43)
21:27:11 Timing HOL-SPARK-Manual (4 threads, 3.820s elapsed time, 9.664s cpu time, 0.300s GC time, factor 2.53)
21:27:11 Finished HOL-SPARK-Manual (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.24)
21:27:12 Timing Old_Datatype_Show (4 threads, 9.600s elapsed time, 11.684s cpu time, 0.356s GC time, factor 1.22)
21:27:12 Finished Old_Datatype_Show (0:00:11 elapsed time, 0:00:13 cpu time, factor 1.15)
21:27:13 Timing Minimal_SSA (4 threads, 7.051s elapsed time, 19.016s cpu time, 0.508s GC time, factor 2.70)
21:27:13 Finished Minimal_SSA (0:00:13 elapsed time, 0:00:30 cpu time, factor 2.28)
21:27:19 Timing HOL-SPARK-Examples (4 threads, 13.778s elapsed time, 39.788s cpu time, 1.120s GC time, factor 2.89)
21:27:19 Finished HOL-SPARK-Examples (0:00:27 elapsed time, 0:01:01 cpu time, factor 2.24)
21:27:19 Running RIPEMD-160-SPARK ...
21:27:20 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
21:27:20 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
21:27:25 Timing RIPEMD-160-SPARK (4 threads, 1.347s elapsed time, 1.420s cpu time, 0.000s GC time, factor 1.05)
21:27:25 Finished RIPEMD-160-SPARK (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.87)
21:28:16 Timing Poincare_Bendixson (4 threads, 135.449s elapsed time, 262.600s cpu time, 5.836s GC time, factor 1.94)
21:28:16 Finished Poincare_Bendixson (0:02:24 elapsed time, 0:04:43 cpu time, factor 1.96)
21:30:07 Timing Lorenz_Approximation (4 threads, 251.832s elapsed time, 590.068s cpu time, 43.432s GC time, factor 2.34)
21:30:07 Finished Lorenz_Approximation (0:05:00 elapsed time, 0:11:12 cpu time, factor 2.24)
21:30:07 Running Lorenz_C0 ...
21:30:07 Running Lorenz_C1 ...
21:30:10 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
21:30:10 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
21:30:12 Timing Lorenz_C1 (4 threads, 1.020s elapsed time, 1.704s cpu time, 0.000s GC time, factor 1.67)
21:30:12 Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.11)
21:30:22 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
21:31:09 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
21:31:09 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
21:31:23 Timing CAVA_LTL_Modelchecker (4 threads, 435.359s elapsed time, 565.184s cpu time, 20.484s GC time, factor 1.30)
21:31:23 Finished CAVA_LTL_Modelchecker (0:07:24 elapsed time, 0:11:20 cpu time, factor 1.53)
21:33:59 Timing HOL-ODE-Examples (4 threads, 495.116s elapsed time, 1429.160s cpu time, 10.348s GC time, factor 2.89)
21:33:59 Finished HOL-ODE-Examples (0:08:18 elapsed time, 0:23:52 cpu time, factor 2.87)
21:35:27 Timing HOL-ODE-ARCH-COMP (4 threads, 616.358s elapsed time, 1390.876s cpu time, 17.612s GC time, factor 2.26)
21:35:27 Finished HOL-ODE-ARCH-COMP (0:10:20 elapsed time, 0:23:14 cpu time, factor 2.25)
22:02:21 Timing Lorenz_C0 (4 threads, 1929.438s elapsed time, 7620.140s cpu time, 42.320s GC time, factor 3.95)
22:02:21 Finished Lorenz_C0 (0:32:13 elapsed time, 2:07:03 cpu time, factor 3.94)
22:02:21 
22:02:21 === TIMING ===
22:02:21 
22:02:21 Group AFP: 5:35:22 elapsed time, 16:57:24 cpu time, factor 3.03
22:02:21 Group main: 0:01:18 elapsed time, 0:03:23 cpu time, factor 2.60
22:02:21 Group doc: 0:00:00 elapsed time
22:02:21 Group timing: 0:02:51 elapsed time, 0:05:38 cpu time, factor 1.98
22:02:21 Group large: 0:40:36 elapsed time, 2:31:01 cpu time, factor 3.72
22:02:21 Group no_doc: 0:00:00 elapsed time
22:02:21 Overall: 1:06:29 elapsed time, 17:55:22 cpu time, factor 16.17
22:02:21 
22:02:21 === DEPENDENCIES ===
22:02:21 
22:02:21 Generating dependencies file ...
22:02:27 Writing dependencies file ...
22:02:27 
22:02:27 === REPORT ===
22:02:27 
22:02:27 Writing report file ...
22:02:27 
22:02:27 === SITEGEN ===
22:02:27 
22:02:27 Writing status file ...
22:02:27 Running sitegen ...
22:02:30 Success: Generated topics.html
22:02:30 Success: Generated index.html
22:02:30 Success: Generated html files for 546 entries
22:02:30 Success: Generated statistics.html
22:02:30 Success: Generated download.html
22:02:30 Success: Generated about.html
22:02:30 Success: Generated citing.html
22:02:30 Success: Generated updating.html
22:02:30 Success: Generated search.html
22:02:30 Success: Generated submitting.html
22:02:30 Success: Generated using.html
22:02:30 Success: Generated rss.xml
22:02:30 Success: Generated status.html
22:02:30 Checked directory thys. Found 0 warnings.
22:02:30 Packing tars ...
22:02:44 
22:02:44 === COMPLETED ===
22:02:44 
22:02:44 Archiving artifacts
22:06:32 Started calculate disk usage of build
22:06:32 Finished Calculation of disk usage of build in 0 seconds
22:06:39 Started calculate disk usage of workspace
22:06:40 Finished Calculation of disk usage of workspace in 0 seconds
22:06:40 No emails were triggered.
22:06:40 Finished: SUCCESS