Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon



On 08/02/2021 22:42, Makarius wrote:

> Presumably the last release candidate is
> https://isabelle.sketis.net/website-Isabelle2021-RC5

The announcement now says:

  * Support for macOS Big Sur on Intel and Apple Silicon (ARM).

For RC5 the main change is "Improved support for Apple Silicon (ARM): external
processes are managed by Isabelle/Scala instead of Apple's Rosetta (which does
not support multithreaded process fork)."

Thus sledgehammer works properly, and as far as I can see everything else as well.


I also managed to run complete Isabelle + AFP twice: it takes approx. 12h for
one run. Detailed timings are included for the following setup:

* Hardware: Macmini9,1, Apple M1 CPU with 4 cores * 2 (hyperthreading), 16GB RAM

* macOS Big Sur 11.2

* Isabelle/da0ee7fbc068 (approx. Isabelle2021-RC5)

* AFP/07ea995a6665 from afp-2021 repository

* etc/settings:

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

  ML_PLATFORM="x86_64_32-darwin"
  ML_OPTIONS="--minheap 1500 --maxheap=10g"

* isabelle build -o threads=4 -d '$AFP' -a -X very_slow


For comparison, here are timings for Isabelle on the last generation of Intel
Mac Mini (Macmini8,1, 6-Core Intel Core i7, 64 GB RAM):
https://isabelle.sketis.net/devel/build_status/macOS_11.1_Big_Sur_4_threads/index.html


Overall the Apple Silicon machine is pretty impressive: slightly faster than
the Intel one. Note that 16 GB is presently the upper bound for that new
generation of Mac Minis, while the older generation supported 64 GB.


	Makarius
Building Pure ...
Finished Pure (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
Building HOL ...
Finished HOL (0:03:19 elapsed time, 0:08:09 cpu time, factor 2.45)
Building AWN ...
Finished AWN (0:00:39 elapsed time, 0:01:45 cpu time, factor 2.65)
Running AODV ...
Finished AODV (0:58:32 elapsed time, 3:16:34 cpu time, factor 3.36)
Building HOL-Analysis ...
Finished HOL-Analysis (0:05:06 elapsed time, 0:16:51 cpu time, factor 3.30)
Building HOL-Library ...
Finished HOL-Library (0:01:54 elapsed time, 0:05:54 cpu time, factor 3.09)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:25 elapsed time, 0:04:04 cpu time, factor 2.87)
Building HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:10:27 elapsed time, 0:32:44 cpu time, factor 3.13)
Building Category3 ...
Finished Category3 (0:03:33 elapsed time, 0:10:27 cpu time, factor 2.94)
Running JinjaThreads ...
Finished JinjaThreads (0:41:35 elapsed time, 2:13:24 cpu time, factor 3.21)
Building MonoidalCategory ...
Finished MonoidalCategory (0:03:10 elapsed time, 0:06:51 cpu time, factor 2.17)
Running Bicategory ...
Finished Bicategory (0:33:27 elapsed time, 1:34:00 cpu time, factor 2.81)
Building Lorenz_Approximation ...
Finished Lorenz_Approximation (0:02:39 elapsed time, 0:05:30 cpu time, factor 2.07)
Running Lorenz_C0 ...
Finished Lorenz_C0 (0:23:18 elapsed time, 1:30:50 cpu time, factor 3.90)
Building ConcurrentIMP ...
Finished ConcurrentIMP (0:00:22 elapsed time, 0:00:49 cpu time, factor 2.22)
Running ConcurrentGC ...
Finished ConcurrentGC (0:12:31 elapsed time, 0:46:47 cpu time, factor 3.74)
Building Core_SC_DOM ...
Finished Core_SC_DOM (0:02:19 elapsed time, 0:06:37 cpu time, factor 2.84)
Building Shadow_SC_DOM ...
Finished Shadow_SC_DOM (0:06:04 elapsed time, 0:18:02 cpu time, factor 2.97)
Building Automatic_Refinement ...
Finished Automatic_Refinement (0:00:19 elapsed time, 0:00:49 cpu time, factor 2.49)
Building Refine_Monadic ...
Finished Refine_Monadic (0:00:33 elapsed time, 0:01:31 cpu time, factor 2.73)
Building Collections ...
Finished Collections (0:02:54 elapsed time, 0:06:39 cpu time, factor 2.29)
Building Core_DOM ...
Finished Core_DOM (0:02:34 elapsed time, 0:07:39 cpu time, factor 2.98)
Building HOL-Computational_Algebra ...
Finished HOL-Computational_Algebra (0:00:39 elapsed time, 0:01:44 cpu time, factor 2.64)
Building HOL-Algebra ...
Finished HOL-Algebra (0:01:41 elapsed time, 0:05:25 cpu time, factor 3.22)
Building CAVA_Base ...
Finished CAVA_Base (0:00:17 elapsed time, 0:00:36 cpu time, factor 2.05)
Building CAVA_Automata ...
Finished CAVA_Automata (0:00:45 elapsed time, 0:01:14 cpu time, factor 1.64)
Building Word_Lib ...
Finished Word_Lib (0:00:41 elapsed time, 0:02:06 cpu time, factor 3.06)
Building CAVA_Setup ...
Finished CAVA_Setup (0:05:34 elapsed time, 0:17:04 cpu time, factor 3.06)
Building IP_Addresses ...
Finished IP_Addresses (0:02:39 elapsed time, 0:06:42 cpu time, factor 2.52)
Running HOL-ODE-ARCH-COMP ...
Finished HOL-ODE-ARCH-COMP (0:06:35 elapsed time, 0:13:34 cpu time, factor 2.06)
Building JNF-AFP-Lib ...
Finished JNF-AFP-Lib (0:01:03 elapsed time, 0:03:06 cpu time, factor 2.92)
Building Shadow_DOM ...
Finished Shadow_DOM (0:04:06 elapsed time, 0:12:55 cpu time, factor 3.14)
Building LEM ...
Finished LEM (0:00:48 elapsed time, 0:02:23 cpu time, factor 2.98)
Building Jordan_Normal_Form ...
Finished Jordan_Normal_Form (0:02:29 elapsed time, 0:06:39 cpu time, factor 2.68)
Running MSO_Regex_Equivalence ...
Finished MSO_Regex_Equivalence (0:03:26 elapsed time, 0:10:22 cpu time, factor 3.02)
Building CakeML ...
Skipping theories "Tests/Compiler_Test" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
Finished CakeML (0:03:11 elapsed time, 0:09:12 cpu time, factor 2.89)
Building Syntax_Independent_Logic ...
Finished Syntax_Independent_Logic (0:01:30 elapsed time, 0:05:00 cpu time, factor 3.33)
Running SC_DOM_Components ...
Finished SC_DOM_Components (0:05:17 elapsed time, 0:16:15 cpu time, factor 3.07)
Building Echelon_Form ...
Finished Echelon_Form (0:02:01 elapsed time, 0:06:30 cpu time, factor 3.22)
Running HOL-ODE-Examples ...
Finished HOL-ODE-Examples (0:05:02 elapsed time, 0:14:10 cpu time, factor 2.81)
Building HOL-Proofs ...
Finished HOL-Proofs (0:05:01 elapsed time, 0:08:42 cpu time, factor 1.73)
Building Jinja ...
Finished Jinja (0:01:59 elapsed time, 0:06:26 cpu time, factor 3.24)
Building HOL-Number_Theory ...
Finished HOL-Number_Theory (0:00:48 elapsed time, 0:02:26 cpu time, factor 3.04)
Building Deriving ...
Finished Deriving (0:00:38 elapsed time, 0:01:17 cpu time, factor 2.03)
Building Abstract-Rewriting ...
Finished Abstract-Rewriting (0:00:23 elapsed time, 0:00:49 cpu time, factor 2.06)
Building Simple_Firewall ...
Finished Simple_Firewall (0:00:23 elapsed time, 0:01:03 cpu time, factor 2.72)
Building First_Order_Terms ...
Finished First_Order_Terms (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.92)
Running JinjaDCI ...
Preparing JinjaDCI/document ...
Finished JinjaDCI/document (0:00:14 elapsed time)
Finished JinjaDCI (0:03:37 elapsed time, 0:12:15 cpu time, factor 3.39)
Building Stateful_Protocol_Composition_and_Typing ...
Finished Stateful_Protocol_Composition_and_Typing (0:02:27 elapsed time, 0:07:41 cpu time, factor 3.14)
Running HOL-ex ...
Finished HOL-ex (0:04:28 elapsed time, 0:11:47 cpu time, factor 2.63)
Building Routing ...
Finished Routing (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.90)
Building Containers ...
Finished Containers (0:01:14 elapsed time, 0:02:36 cpu time, factor 2.10)
Building Iptables_Semantics ...
Finished Iptables_Semantics (0:01:36 elapsed time, 0:04:55 cpu time, factor 3.06)
Building Goedel_Incompleteness ...
Finished Goedel_Incompleteness (0:00:15 elapsed time, 0:00:40 cpu time, factor 2.66)
Running Native_Word ...
Skipping theories "Native_Word_Test_MLton", "Native_Word_Test_MLton2" (undefined ISABELLE_MLTON)
Skipping theories "Native_Word_Test_OCaml", "Native_Word_Test_OCaml2" (undefined ISABELLE_OCAMLFIND)
Skipping theories "Native_Word_Test_SMLNJ", "Native_Word_Test_SMLNJ2" (undefined ISABELLE_SMLNJ)
Finished Native_Word (0:03:59 elapsed time, 0:04:03 cpu time, factor 1.02)
Building Subresultants ...
Finished Subresultants (0:00:44 elapsed time, 0:01:33 cpu time, factor 2.12)
Running Goedel_HFSet_Semanticless ...
Finished Goedel_HFSet_Semanticless (0:03:57 elapsed time, 0:10:30 cpu time, factor 2.65)
Building Pre_BZ ...
Finished Pre_BZ (0:01:04 elapsed time, 0:02:41 cpu time, factor 2.48)
Building HRB-Slicing ...
Finished HRB-Slicing (0:03:43 elapsed time, 0:09:40 cpu time, factor 2.59)
Building Hermite ...
Finished Hermite (0:00:30 elapsed time, 0:01:06 cpu time, factor 2.18)
Running Goedel_HFSet_Semantic ...
Finished Goedel_HFSet_Semantic (0:03:30 elapsed time, 0:08:54 cpu time, factor 2.54)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.80)
Building HereditarilyFinite ...
Finished HereditarilyFinite (0:00:12 elapsed time, 0:00:24 cpu time, factor 1.95)
Building Incompleteness ...
Finished Incompleteness (0:03:39 elapsed time, 0:08:40 cpu time, factor 2.37)
Running HOL-Nominal-Examples ...
Finished HOL-Nominal-Examples (0:02:42 elapsed time, 0:09:27 cpu time, factor 3.48)
Building HOL-Probability ...
Finished HOL-Probability (0:01:02 elapsed time, 0:03:07 cpu time, factor 2.99)
Building Slicing ...
Finished Slicing (0:03:16 elapsed time, 0:10:02 cpu time, factor 3.07)
Building MFOTL_Monitor ...
Finished MFOTL_Monitor (0:00:57 elapsed time, 0:02:08 cpu time, factor 2.24)
Running CakeML_Codegen ...
Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
Finished CakeML_Codegen (0:03:15 elapsed time, 0:09:25 cpu time, factor 2.89)
Building Affine_Arithmetic ...
Finished Affine_Arithmetic (0:03:08 elapsed time, 0:09:40 cpu time, factor 3.09)
Running Smith_Normal_Form ...
Finished Smith_Normal_Form (0:03:01 elapsed time, 0:09:25 cpu time, factor 3.11)
Building Groebner_Bases ...
Finished Groebner_Bases (0:03:28 elapsed time, 0:10:25 cpu time, factor 3.00)
Building Sepref_Prereq ...
Finished Sepref_Prereq (0:00:36 elapsed time, 0:01:04 cpu time, factor 1.75)
Running CAVA_LTL_Modelchecker ...
Finished CAVA_LTL_Modelchecker (0:02:57 elapsed time, 0:03:38 cpu time, factor 1.23)
Building Stone_Algebras ...
Finished Stone_Algebras (0:00:31 elapsed time, 0:00:58 cpu time, factor 1.88)
Running HOL-Data_Structures ...
Finished HOL-Data_Structures (0:02:51 elapsed time, 0:10:24 cpu time, factor 3.65)
Running DOM_Components ...
Finished DOM_Components (0:03:04 elapsed time, 0:07:48 cpu time, factor 2.53)
Building HOL-Complex_Analysis ...
Finished HOL-Complex_Analysis (0:00:37 elapsed time, 0:01:44 cpu time, factor 2.79)
Running Iptables_Semantics_Examples ...
Finished Iptables_Semantics_Examples (0:03:00 elapsed time, 0:11:26 cpu time, factor 3.80)
Running HOL-Decision_Procs ...
Finished HOL-Decision_Procs (0:02:46 elapsed time, 0:09:26 cpu time, factor 3.40)
Building Berlekamp_Zassenhaus ...
Finished Berlekamp_Zassenhaus (0:01:11 elapsed time, 0:03:23 cpu time, factor 2.84)
Building Sepref_Basic ...
Finished Sepref_Basic (0:00:21 elapsed time, 0:00:40 cpu time, factor 1.84)
Running Irrational_Series_Erdos_Straus ...
Finished Irrational_Series_Erdos_Straus (0:02:39 elapsed time, 0:09:07 cpu time, factor 3.42)
Running HOL-Codegenerator_Test ...
Skipping theories "Code_Test_MLton" (undefined ISABELLE_MLTON)
Skipping theories "Code_Test_OCaml" (undefined ISABELLE_OCAMLFIND)
Skipping theories "Code_Test_SMLNJ" (undefined ISABELLE_SMLNJ)
Finished HOL-Codegenerator_Test (0:02:41 elapsed time, 0:05:59 cpu time, factor 2.23)
Running MFODL_Monitor_Optimized ...
Finished MFODL_Monitor_Optimized (0:02:34 elapsed time, 0:06:55 cpu time, factor 2.70)
Building Stone_Relation_Algebras ...
Finished Stone_Relation_Algebras (0:00:38 elapsed time, 0:01:11 cpu time, factor 1.88)
Building Transition_Systems_and_Automata ...
Finished Transition_Systems_and_Automata (0:02:40 elapsed time, 0:08:22 cpu time, factor 3.13)
Building Markov_Models ...
Finished Markov_Models (0:00:53 elapsed time, 0:02:30 cpu time, factor 2.84)
Building Auto2_HOL ...
Finished Auto2_HOL (0:00:15 elapsed time, 0:00:34 cpu time, factor 2.18)
Building Sepref_IICF ...
Finished Sepref_IICF (0:00:38 elapsed time, 0:01:35 cpu time, factor 2.45)
Building Dirichlet_Series ...
Finished Dirichlet_Series (0:01:54 elapsed time, 0:05:45 cpu time, factor 3.01)
Building Kleene_Algebra ...
Finished Kleene_Algebra (0:00:34 elapsed time, 0:01:41 cpu time, factor 2.95)
Building Formal_SSA ...
Finished Formal_SSA (0:02:41 elapsed time, 0:05:36 cpu time, factor 2.08)
Running Automated_Stateful_Protocol_Verification ...
Finished Automated_Stateful_Protocol_Verification (0:02:35 elapsed time, 0:08:25 cpu time, factor 3.26)
Building SM_Base ...
Finished SM_Base (0:01:38 elapsed time, 0:04:26 cpu time, factor 2.72)
Running Proof_Strategy_Language ...
Finished Proof_Strategy_Language (0:02:18 elapsed time, 0:00:40 cpu time, factor 0.29)
Building Probabilistic_While ...
Finished Probabilistic_While (0:00:25 elapsed time, 0:00:57 cpu time, factor 2.25)
Running Psi_Calculi ...
Finished Psi_Calculi (0:02:28 elapsed time, 0:07:56 cpu time, factor 3.20)
Running Auto2_Imperative_HOL ...
Finished Auto2_Imperative_HOL (0:02:17 elapsed time, 0:08:21 cpu time, factor 3.65)
Building Formula_Derivatives ...
Finished Formula_Derivatives (0:02:47 elapsed time, 0:05:55 cpu time, factor 2.13)
Running Network_Security_Policy_Verification ...
Finished Network_Security_Policy_Verification (0:02:11 elapsed time, 0:07:33 cpu time, factor 3.44)
Running Security_Protocol_Refinement ...
Finished Security_Protocol_Refinement (0:02:04 elapsed time, 0:07:33 cpu time, factor 3.63)
Running Algebraic_Numbers ...
Finished Algebraic_Numbers (0:02:14 elapsed time, 0:07:15 cpu time, factor 3.24)
Building Flow_Networks ...
Finished Flow_Networks (0:01:23 elapsed time, 0:03:15 cpu time, factor 2.33)
Building CryptHOL ...
Finished CryptHOL (0:01:12 elapsed time, 0:03:30 cpu time, factor 2.89)
Building Stone_Kleene_Relation_Algebras ...
Finished Stone_Kleene_Relation_Algebras (0:00:45 elapsed time, 0:01:59 cpu time, factor 2.62)
Building KAT_and_DRA ...
Finished KAT_and_DRA (0:00:19 elapsed time, 0:00:48 cpu time, factor 2.51)
Building Refine_Imperative_HOL ...
Finished Refine_Imperative_HOL (0:02:18 elapsed time, 0:04:47 cpu time, factor 2.08)
Building HOLCF ...
Finished HOLCF (0:00:14 elapsed time, 0:00:30 cpu time, factor 2.18)
Running Stochastic_Matrices ...
Finished Stochastic_Matrices (0:01:54 elapsed time, 0:05:19 cpu time, factor 2.80)
Running Perron_Frobenius ...
Finished Perron_Frobenius (0:01:52 elapsed time, 0:06:08 cpu time, factor 3.28)
Running PAC_Checker ...
Skipping theories "PAC_Checker_MLton" (undefined ISABELLE_MLTON)
Finished PAC_Checker (0:01:51 elapsed time, 0:06:49 cpu time, factor 3.66)
Running Algebraic_VCs ...
Finished Algebraic_VCs (0:01:52 elapsed time, 0:03:39 cpu time, factor 1.95)
Running CSP_RefTK ...
Finished CSP_RefTK (0:01:48 elapsed time, 0:06:07 cpu time, factor 3.39)
Running SPARCv8 ...
Finished SPARCv8 (0:01:46 elapsed time, 0:05:07 cpu time, factor 2.88)
Running Linear_Recurrences_Solver ...
Finished Linear_Recurrences_Solver (0:01:49 elapsed time, 0:05:00 cpu time, factor 2.75)
Running Probabilistic_Prime_Tests ...
Finished Probabilistic_Prime_Tests (0:01:45 elapsed time, 0:06:21 cpu time, factor 3.61)
Running Complx ...
Finished Complx (0:01:43 elapsed time, 0:05:04 cpu time, factor 2.94)
Running Hybrid_Systems_VCs ...
Finished Hybrid_Systems_VCs (0:01:42 elapsed time, 0:05:38 cpu time, factor 3.30)
Running Universal_Turing_Machine ...
Finished Universal_Turing_Machine (0:01:39 elapsed time, 0:04:54 cpu time, factor 2.95)
Building LLL_Basis_Reduction ...
Finished LLL_Basis_Reduction (0:01:42 elapsed time, 0:03:55 cpu time, factor 2.28)
Running Transcendence_Series_Hancl_Rucki ...
Finished Transcendence_Series_Hancl_Rucki (0:01:39 elapsed time, 0:05:43 cpu time, factor 3.44)
Running HOL-Corec_Examples ...
Finished HOL-Corec_Examples (0:01:34 elapsed time, 0:04:16 cpu time, factor 2.73)
Running Differential_Dynamic_Logic ...
Finished Differential_Dynamic_Logic (0:01:36 elapsed time, 0:03:33 cpu time, factor 2.21)
Running HOL-CSP ...
Finished HOL-CSP (0:01:42 elapsed time, 0:05:22 cpu time, factor 3.15)
Building Ordered_Resolution_Prover ...
Finished Ordered_Resolution_Prover (0:00:33 elapsed time, 0:01:27 cpu time, factor 2.62)
Running No_FTL_observers ...
Finished No_FTL_observers (0:01:31 elapsed time, 0:01:44 cpu time, factor 1.14)
Building Group-Ring-Module ...
Finished Group-Ring-Module (0:01:28 elapsed time, 0:04:10 cpu time, factor 2.83)
Building Dependent_SIFUM_Type_Systems ...
Finished Dependent_SIFUM_Type_Systems (0:00:57 elapsed time, 0:02:26 cpu time, factor 2.54)
Running Key_Agreement_Strong_Adversaries ...
Finished Key_Agreement_Strong_Adversaries (0:01:30 elapsed time, 0:05:01 cpu time, factor 3.33)
Building Simpl ...
Finished Simpl (0:00:58 elapsed time, 0:02:45 cpu time, factor 2.84)
Running CoreC++ ...
Finished CoreC++ (0:01:31 elapsed time, 0:04:21 cpu time, factor 2.84)
Running HOL-Quickcheck_Examples ...
Finished HOL-Quickcheck_Examples (0:01:27 elapsed time, 0:01:46 cpu time, factor 1.21)
Running HOL-Datatype_Examples ...
Finished HOL-Datatype_Examples (0:00:57 elapsed time, 0:03:30 cpu time, factor 3.67)
Building Count_Complex_Roots ...
Finished Count_Complex_Roots (0:00:56 elapsed time, 0:02:37 cpu time, factor 2.79)
Running DFS_Framework ...
Finished DFS_Framework (0:01:26 elapsed time, 0:04:13 cpu time, factor 2.94)
Building Datatype_Order_Generator ...
Finished Datatype_Order_Generator (0:01:57 elapsed time, 0:04:47 cpu time, factor 2.44)
Building Aggregation_Algebras ...
Finished Aggregation_Algebras (0:00:50 elapsed time, 0:01:18 cpu time, factor 1.57)
Building Bernoulli ...
Finished Bernoulli (0:01:11 elapsed time, 0:03:34 cpu time, factor 2.99)
Running Probabilistic_Timed_Automata ...
Finished Probabilistic_Timed_Automata (0:01:20 elapsed time, 0:03:55 cpu time, factor 2.93)
Running KAD ...
Finished KAD (0:01:20 elapsed time, 0:02:12 cpu time, factor 1.65)
Running QR_Decomposition ...
Finished QR_Decomposition (0:01:17 elapsed time, 0:04:33 cpu time, factor 3.54)
Running Containers-Benchmarks ...
Finished Containers-Benchmarks (0:01:18 elapsed time, 0:03:34 cpu time, factor 2.73)
Building Nominal2 ...
Finished Nominal2 (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.78)
Running Promela ...
Finished Promela (0:01:18 elapsed time, 0:02:33 cpu time, factor 1.97)
Running HOL-Proofs-Extraction ...
Finished HOL-Proofs-Extraction (0:01:11 elapsed time, 0:01:57 cpu time, factor 1.65)
Building Game_Based_Crypto ...
Finished Game_Based_Crypto (0:00:27 elapsed time, 0:01:08 cpu time, factor 2.51)
Running HOL-Proofs-Lambda ...
Finished HOL-Proofs-Lambda (0:01:13 elapsed time, 0:01:22 cpu time, factor 1.12)
Running Functional_Ordered_Resolution_Prover ...
Finished Functional_Ordered_Resolution_Prover (0:01:14 elapsed time, 0:03:09 cpu time, factor 2.52)
Running SM ...
Finished SM (0:01:13 elapsed time, 0:02:01 cpu time, factor 1.65)
Running Safe_OCL ...
Finished Safe_OCL (0:01:15 elapsed time, 0:02:26 cpu time, factor 1.95)
Running Topological_Semantics ...
Finished Topological_Semantics (0:01:13 elapsed time, 0:01:40 cpu time, factor 1.37)
Running Collections_Examples ...
Finished Collections_Examples (0:01:10 elapsed time, 0:03:20 cpu time, factor 2.86)
Running Deep_Learning ...
Finished Deep_Learning (0:01:09 elapsed time, 0:04:05 cpu time, factor 3.55)
Building E_Transcendental ...
Finished E_Transcendental (0:00:55 elapsed time, 0:02:47 cpu time, factor 3.04)
Running Modal_Logics_for_NTS ...
Finished Modal_Logics_for_NTS (0:01:06 elapsed time, 0:03:35 cpu time, factor 3.24)
Running Store_Buffer_Reduction ...
Finished Store_Buffer_Reduction (0:01:07 elapsed time, 0:03:05 cpu time, factor 2.75)
Building HOLCF-Prelude ...
Finished HOLCF-Prelude (0:00:25 elapsed time, 0:01:00 cpu time, factor 2.39)
Running LTL_to_GBA ...
Finished LTL_to_GBA (0:01:03 elapsed time, 0:03:24 cpu time, factor 3.19)
Building HOL-Auth ...
Finished HOL-Auth (0:00:54 elapsed time, 0:02:47 cpu time, factor 3.06)
Running Isabelle_Meta_Model ...
Finished Isabelle_Meta_Model (0:01:04 elapsed time, 0:01:49 cpu time, factor 1.69)
Building IMP2 ...
Finished IMP2 (0:00:59 elapsed time, 0:02:23 cpu time, factor 2.43)
Running Isabelle_Marries_Dirac ...
Finished Isabelle_Marries_Dirac (0:01:03 elapsed time, 0:03:24 cpu time, factor 3.21)
Running Featherweight_OCL ...
Finished Featherweight_OCL (0:01:01 elapsed time, 0:02:39 cpu time, factor 2.57)
Running Prpu_Maxflow ...
Finished Prpu_Maxflow (0:01:02 elapsed time, 0:01:54 cpu time, factor 1.84)
Building LTL ...
Finished LTL (0:00:34 elapsed time, 0:01:28 cpu time, factor 2.55)
Building Simplex ...
Finished Simplex (0:00:47 elapsed time, 0:01:58 cpu time, factor 2.51)
Running LOFT ...
Finished LOFT (0:01:00 elapsed time, 0:03:24 cpu time, factor 3.37)
Building Coinductive ...
Finished Coinductive (0:00:59 elapsed time, 0:02:47 cpu time, factor 2.80)
Running Linear_Programming ...
Finished Linear_Programming (0:01:00 elapsed time, 0:02:48 cpu time, factor 2.77)
Building Zeta_Function ...
Finished Zeta_Function (0:00:41 elapsed time, 0:01:52 cpu time, factor 2.69)
Running Poincare_Bendixson ...
Finished Poincare_Bendixson (0:01:01 elapsed time, 0:01:48 cpu time, factor 1.75)
Running Multi_Party_Computation ...
Finished Multi_Party_Computation (0:01:01 elapsed time, 0:03:36 cpu time, factor 3.50)
Building Order_Lattice_Props ...
Finished Order_Lattice_Props (0:00:25 elapsed time, 0:00:59 cpu time, factor 2.31)
Building Akra_Bazzi ...
Finished Akra_Bazzi (0:00:52 elapsed time, 0:02:24 cpu time, factor 2.76)
Running Constructive_Cryptography ...
Finished Constructive_Cryptography (0:00:45 elapsed time, 0:02:16 cpu time, factor 3.01)
Running Polynomials ...
Finished Polynomials (0:00:59 elapsed time, 0:03:04 cpu time, factor 3.08)
Running Allen_Calculus ...
Finished Allen_Calculus (0:01:00 elapsed time, 0:02:34 cpu time, factor 2.55)
Running Timed_Automata ...
Finished Timed_Automata (0:00:55 elapsed time, 0:02:41 cpu time, factor 2.88)
Running Gromov_Hyperbolicity ...
Finished Gromov_Hyperbolicity (0:00:57 elapsed time, 0:03:07 cpu time, factor 3.24)
Running WebAssembly ...
Finished WebAssembly (0:00:56 elapsed time, 0:02:49 cpu time, factor 3.02)
Building Ordinal ...
Finished Ordinal (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.54)
Running AI_Planning_Languages_Semantics ...
Finished AI_Planning_Languages_Semantics (0:00:56 elapsed time, 0:03:22 cpu time, factor 3.59)
Running Gabow_SCC ...
Finished Gabow_SCC (0:00:58 elapsed time, 0:02:14 cpu time, factor 2.31)
Running Relational_Method ...
Finished Relational_Method (0:00:54 elapsed time, 0:02:31 cpu time, factor 2.81)
Building Nested_Multisets_Ordinals ...
Finished Nested_Multisets_Ordinals (0:00:30 elapsed time, 0:01:28 cpu time, factor 2.91)
Building Monad_Memo_DP ...
Finished Monad_Memo_DP (0:01:09 elapsed time, 0:03:34 cpu time, factor 3.09)
Running Dependent_SIFUM_Refinement ...
Finished Dependent_SIFUM_Refinement (0:00:53 elapsed time, 0:02:35 cpu time, factor 2.88)
Building Symmetric_Polynomials ...
Finished Symmetric_Polynomials (0:00:46 elapsed time, 0:01:49 cpu time, factor 2.38)
Building Relation_Algebra ...
Finished Relation_Algebra (0:00:16 elapsed time, 0:00:38 cpu time, factor 2.29)
Running HOL-Homology ...
Finished HOL-Homology (0:00:51 elapsed time, 0:02:52 cpu time, factor 3.35)
Building Datatypes ...
Finished Datatypes (0:00:39 elapsed time, 0:01:10 cpu time, factor 1.78)
Running HOL-Hoare_Parallel ...
Finished HOL-Hoare_Parallel (0:00:46 elapsed time, 0:02:42 cpu time, factor 3.48)
Running Density_Compiler ...
Finished Density_Compiler (0:00:54 elapsed time, 0:01:51 cpu time, factor 2.04)
Running Safe_Distance ...
Finished Safe_Distance (0:00:48 elapsed time, 0:02:33 cpu time, factor 3.16)
Running Planarity_Certificates ...
Finished Planarity_Certificates (0:00:50 elapsed time, 0:02:47 cpu time, factor 3.31)
Building Complex_Geometry ...
Finished Complex_Geometry (0:00:34 elapsed time, 0:01:32 cpu time, factor 2.66)
Running Interval_Arithmetic_Word32 ...
Finished Interval_Arithmetic_Word32 (0:00:53 elapsed time, 0:02:47 cpu time, factor 3.16)
Running BirdKMP ...
Finished BirdKMP (0:00:49 elapsed time, 0:01:26 cpu time, factor 1.77)
Building HOL-Imperative_HOL ...
Finished HOL-Imperative_HOL (0:00:59 elapsed time, 0:02:11 cpu time, factor 2.20)
Running KBPs ...
Finished KBPs (0:00:48 elapsed time, 0:02:17 cpu time, factor 2.85)
Running Stable_Matching ...
Finished Stable_Matching (0:00:48 elapsed time, 0:02:24 cpu time, factor 2.97)
Building HOL-IMP ...
Finished HOL-IMP (0:01:01 elapsed time, 0:03:00 cpu time, factor 2.94)
Running Amicable_Numbers ...
Finished Amicable_Numbers (0:00:46 elapsed time, 0:01:34 cpu time, factor 2.04)
Running Verified_SAT_Based_AI_Planning ...
Finished Verified_SAT_Based_AI_Planning (0:00:45 elapsed time, 0:02:14 cpu time, factor 2.92)
Building HOL-Real_Asymp ...
Finished HOL-Real_Asymp (0:00:59 elapsed time, 0:03:14 cpu time, factor 3.25)
Running Groebner_Macaulay ...
Finished Groebner_Macaulay (0:00:48 elapsed time, 0:01:24 cpu time, factor 1.74)
Running HOL-Predicate_Compile_Examples ...
Skipping theories "Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example_Prolog", "Lambda_Example", "List_Examples" (undefined ISABELLE_SWIPL)
Skipping theories "Reg_Exp_Example" (undefined ISABELLE_SWIPL)
Finished HOL-Predicate_Compile_Examples (0:00:46 elapsed time, 0:02:07 cpu time, factor 2.74)
Running Furstenberg_Topology ...
Finished Furstenberg_Topology (0:00:47 elapsed time, 0:02:50 cpu time, factor 3.61)
Running HOL-SMT_Examples ...
Finished HOL-SMT_Examples (0:00:45 elapsed time, 0:01:46 cpu time, factor 2.35)
Running Flyspeck-Tame ...
Finished Flyspeck-Tame (0:00:45 elapsed time, 0:02:33 cpu time, factor 3.36)
Running PseudoHoops ...
Finished PseudoHoops (0:00:43 elapsed time, 0:01:01 cpu time, factor 1.41)
Building Extended_Finite_State_Machines ...
Finished Extended_Finite_State_Machines (0:00:28 elapsed time, 0:01:21 cpu time, factor 2.82)
Running Ordinal_Partitions ...
Finished Ordinal_Partitions (0:00:42 elapsed time, 0:02:30 cpu time, factor 3.52)
Building Launchbury ...
Finished Launchbury (0:00:35 elapsed time, 0:01:45 cpu time, factor 3.02)
Building HOL-Cardinals ...
Finished HOL-Cardinals (0:00:11 elapsed time, 0:00:30 cpu time, factor 2.65)
Running Relational_Minimum_Spanning_Trees ...
Finished Relational_Minimum_Spanning_Trees (0:00:44 elapsed time, 0:01:52 cpu time, factor 2.54)
Running Inductive_Inference ...
Finished Inductive_Inference (0:00:44 elapsed time, 0:01:58 cpu time, factor 2.67)
Building Matrix ...
Finished Matrix (0:00:19 elapsed time, 0:00:48 cpu time, factor 2.44)
Running InfPathElimination ...
Finished InfPathElimination (0:00:45 elapsed time, 0:02:19 cpu time, factor 3.05)
Running Paraconsistency ...
Finished Paraconsistency (0:00:44 elapsed time, 0:02:42 cpu time, factor 3.67)
Building Quantales ...
Finished Quantales (0:00:52 elapsed time, 0:01:33 cpu time, factor 1.77)
Running Chandy_Lamport ...
Finished Chandy_Lamport (0:00:40 elapsed time, 0:02:22 cpu time, factor 3.53)
Running Separation_Logic_Imperative_HOL ...
Finished Separation_Logic_Imperative_HOL (0:00:44 elapsed time, 0:01:27 cpu time, factor 1.94)
Running Relational_Paths ...
Finished Relational_Paths (0:00:44 elapsed time, 0:01:59 cpu time, factor 2.69)
Running HOL-MicroJava ...
Finished HOL-MicroJava (0:00:44 elapsed time, 0:02:35 cpu time, factor 3.54)
Running Taylor_Models ...
Finished Taylor_Models (0:00:43 elapsed time, 0:01:57 cpu time, factor 2.71)
Running Linear_Recurrences ...
Finished Linear_Recurrences (0:00:43 elapsed time, 0:02:20 cpu time, factor 3.22)
Building UPF ...
Finished UPF (0:00:18 elapsed time, 0:00:44 cpu time, factor 2.42)
Running Hoare_Time ...
Finished Hoare_Time (0:00:43 elapsed time, 0:02:37 cpu time, factor 3.65)
Running Vickrey_Clarke_Groves ...
Finished Vickrey_Clarke_Groves (0:00:41 elapsed time, 0:01:50 cpu time, factor 2.67)
Running LTL_to_DRA ...
Finished LTL_to_DRA (0:00:41 elapsed time, 0:02:25 cpu time, factor 3.48)
Running Resolution_FOL ...
Finished Resolution_FOL (0:00:41 elapsed time, 0:01:28 cpu time, factor 2.13)
Running IsaGeoCoq ...
Finished IsaGeoCoq (0:00:39 elapsed time, 0:01:56 cpu time, factor 2.92)
Running Isabelle_C ...
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: int
### Ignored report message: array\ int
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: int\isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: int
### Ignored report message: array\ int
### Ignored report message: \isacommand{}
### Ignored report message: \isacommand{}
### Ignored report message: int\isacommand{}
### Ignored report message: \isacommand{}
Finished Isabelle_C (0:00:40 elapsed time, 0:00:49 cpu time, factor 1.22)
Running Multirelations ...
Finished Multirelations (0:00:41 elapsed time, 0:01:21 cpu time, factor 1.98)
Running List_Update ...
Finished List_Update (0:00:39 elapsed time, 0:02:00 cpu time, factor 3.03)
Running Mersenne_Primes ...
Finished Mersenne_Primes (0:00:42 elapsed time, 0:02:06 cpu time, factor 2.98)
Running Gauss_Jordan ...
Finished Gauss_Jordan (0:00:40 elapsed time, 0:02:21 cpu time, factor 3.49)
Running LTL_Master_Theorem ...
Finished LTL_Master_Theorem (0:00:41 elapsed time, 0:02:27 cpu time, factor 3.57)
Running Binding_Syntax_Theory ...
Finished Binding_Syntax_Theory (0:00:40 elapsed time, 0:02:02 cpu time, factor 3.07)
Running Regular_Algebras ...
Finished Regular_Algebras (0:00:39 elapsed time, 0:01:02 cpu time, factor 1.57)
Running HOL-Bali ...
Finished HOL-Bali (0:00:37 elapsed time, 0:01:53 cpu time, factor 3.00)
Running Rep_Fin_Groups ...
Finished Rep_Fin_Groups (0:00:40 elapsed time, 0:01:23 cpu time, factor 2.07)
Building Girth_Chromatic ...
Finished Girth_Chromatic (0:00:47 elapsed time, 0:01:44 cpu time, factor 2.19)
Running Abortable_Linearizable_Modules ...
Finished Abortable_Linearizable_Modules (0:00:36 elapsed time, 0:01:07 cpu time, factor 1.86)
Building Matrix_Tensor ...
Finished Matrix_Tensor (0:00:23 elapsed time, 0:00:41 cpu time, factor 1.79)
Running Probabilistic_Noninterference ...
Finished Probabilistic_Noninterference (0:00:34 elapsed time, 0:01:42 cpu time, factor 2.97)
Building List-Infinite ...
Finished List-Infinite (0:00:14 elapsed time, 0:00:35 cpu time, factor 2.41)
Running Lambda_Free_KBOs ...
Finished Lambda_Free_KBOs (0:00:30 elapsed time, 0:01:20 cpu time, factor 2.64)
Running Dirichlet_L ...
Finished Dirichlet_L (0:00:36 elapsed time, 0:01:48 cpu time, factor 2.99)
Running Signature_Groebner ...
Finished Signature_Groebner (0:00:36 elapsed time, 0:01:13 cpu time, factor 2.01)
Running Sigma_Commit_Crypto ...
Finished Sigma_Commit_Crypto (0:00:34 elapsed time, 0:01:57 cpu time, factor 3.39)
Running Prime_Harmonic_Series ...
Finished Prime_Harmonic_Series (0:00:34 elapsed time, 0:02:02 cpu time, factor 3.57)
Running BytecodeLogicJmlTypes ...
Finished BytecodeLogicJmlTypes (0:00:33 elapsed time, 0:01:22 cpu time, factor 2.45)
Running Fourier ...
Finished Fourier (0:00:33 elapsed time, 0:01:53 cpu time, factor 3.37)
Running UPF_Firewall ...
Finished UPF_Firewall (0:00:33 elapsed time, 0:01:30 cpu time, factor 2.73)
Running Physical_Quantities ...
Finished Physical_Quantities (0:00:33 elapsed time, 0:01:29 cpu time, factor 2.67)
Building VeriComp ...
Finished VeriComp (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.61)
Running Root_Balanced_Tree ...
Finished Root_Balanced_Tree (0:00:32 elapsed time, 0:01:30 cpu time, factor 2.81)
Running Pi_Transcendental ...
Finished Pi_Transcendental (0:00:33 elapsed time, 0:01:43 cpu time, factor 3.09)
Running Irrationality_J_Hancl ...
Finished Irrationality_J_Hancl (0:00:33 elapsed time, 0:01:20 cpu time, factor 2.40)
Running EdmondsKarp_Maxflow ...
Finished EdmondsKarp_Maxflow (0:00:33 elapsed time, 0:00:44 cpu time, factor 1.33)
Building Priority_Search_Trees ...
Finished Priority_Search_Trees (0:00:14 elapsed time, 0:00:28 cpu time, factor 1.93)
Running Propositional_Proof_Systems ...
Finished Propositional_Proof_Systems (0:00:30 elapsed time, 0:01:49 cpu time, factor 3.54)
Running Parity_Game ...
Finished Parity_Game (0:00:31 elapsed time, 0:01:46 cpu time, factor 3.35)
Building Stirling_Formula ...
Finished Stirling_Formula (0:00:42 elapsed time, 0:01:33 cpu time, factor 2.18)
Building Cauchy ...
Finished Cauchy (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.66)
Running Factored_Transition_System_Bounding ...
Finished Factored_Transition_System_Bounding (0:00:31 elapsed time, 0:01:02 cpu time, factor 2.00)
Running BDD ...
Finished BDD (0:00:20 elapsed time, 0:01:06 cpu time, factor 3.23)
Running Interpreter_Optimizations ...
Finished Interpreter_Optimizations (0:00:30 elapsed time, 0:01:26 cpu time, factor 2.80)
Running Buildings ...
Finished Buildings (0:00:30 elapsed time, 0:01:31 cpu time, factor 2.98)
Running Relational_Disjoint_Set_Forests ...
Finished Relational_Disjoint_Set_Forests (0:00:30 elapsed time, 0:00:51 cpu time, factor 1.69)
Running Green ...
Finished Green (0:00:29 elapsed time, 0:01:28 cpu time, factor 3.03)
Running Winding_Number_Eval ...
Finished Winding_Number_Eval (0:00:30 elapsed time, 0:01:29 cpu time, factor 2.91)
Running Regex_Equivalence ...
Finished Regex_Equivalence (0:00:31 elapsed time, 0:01:31 cpu time, factor 2.92)
Building Sqrt_Babylonian ...
Finished Sqrt_Babylonian (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.92)
Building Applicative_Lifting ...
Finished Applicative_Lifting (0:00:24 elapsed time, 0:00:53 cpu time, factor 2.24)
Building Nat-Interval-Logic ...
Finished Nat-Interval-Logic (0:00:18 elapsed time, 0:00:40 cpu time, factor 2.21)
Running Hidden_Markov_Models ...
Finished Hidden_Markov_Models (0:00:30 elapsed time, 0:00:53 cpu time, factor 1.77)
Running Ergodic_Theory ...
Finished Ergodic_Theory (0:00:28 elapsed time, 0:01:35 cpu time, factor 3.33)
Building Regular-Sets ...
Finished Regular-Sets (0:00:32 elapsed time, 0:01:02 cpu time, factor 1.92)
Running Dijkstra_Shortest_Path ...
Finished Dijkstra_Shortest_Path (0:00:31 elapsed time, 0:00:47 cpu time, factor 1.52)
Running Free-Groups ...
Finished Free-Groups (0:00:29 elapsed time, 0:01:44 cpu time, factor 3.58)
Running Extended_Finite_State_Machine_Inference ...
Finished Extended_Finite_State_Machine_Inference (0:00:30 elapsed time, 0:01:18 cpu time, factor 2.57)
Running Abs_Int_ITP2012 ...
Finished Abs_Int_ITP2012 (0:00:30 elapsed time, 0:01:25 cpu time, factor 2.84)
Running Corec ...
Finished Corec (0:00:28 elapsed time, 0:00:42 cpu time, factor 1.49)
Running HOL-Nitpick_Examples ...
Finished HOL-Nitpick_Examples (0:00:28 elapsed time, 0:01:09 cpu time, factor 2.43)
Running Differential_Game_Logic ...
Finished Differential_Game_Logic (0:00:29 elapsed time, 0:00:50 cpu time, factor 1.74)
Running MFMC_Countable ...
Finished MFMC_Countable (0:00:30 elapsed time, 0:01:31 cpu time, factor 2.96)
Building ZF ...
Finished ZF (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.45)
Running Matrices_for_ODEs ...
Finished Matrices_for_ODEs (0:00:28 elapsed time, 0:01:21 cpu time, factor 2.89)
Running LambdaAuth ...
Finished LambdaAuth (0:00:25 elapsed time, 0:01:03 cpu time, factor 2.47)
Running DiscretePricing ...
Finished DiscretePricing (0:00:28 elapsed time, 0:01:33 cpu time, factor 3.25)
Running Farkas ...
Finished Farkas (0:00:27 elapsed time, 0:01:23 cpu time, factor 3.04)
Running Password_Authentication_Protocol ...
Finished Password_Authentication_Protocol (0:00:27 elapsed time, 0:01:06 cpu time, factor 2.45)
Running Lambert_W ...
Finished Lambert_W (0:00:27 elapsed time, 0:01:06 cpu time, factor 2.42)
Running Higher_Order_Terms ...
Finished Higher_Order_Terms (0:00:26 elapsed time, 0:01:10 cpu time, factor 2.64)
Running Elliptic_Curves_Group_Law ...
Finished Elliptic_Curves_Group_Law (0:00:26 elapsed time, 0:01:10 cpu time, factor 2.62)
Running SATSolverVerification ...
Finished SATSolverVerification (0:00:25 elapsed time, 0:01:32 cpu time, factor 3.59)
Building Amortized_Complexity ...
Finished Amortized_Complexity (0:00:41 elapsed time, 0:01:47 cpu time, factor 2.58)
Running GewirthPGCProof ...
Finished GewirthPGCProof (0:00:25 elapsed time, 0:00:11 cpu time, factor 0.46)
Running Codegen ...
Finished Codegen (0:00:25 elapsed time, 0:01:01 cpu time, factor 2.47)
Running QHLProver ...
Finished QHLProver (0:00:26 elapsed time, 0:01:25 cpu time, factor 3.19)
Building UTP-Toolkit ...
Finished UTP-Toolkit (0:00:22 elapsed time, 0:00:54 cpu time, factor 2.41)
Building Sturm_Sequences ...
Finished Sturm_Sequences (0:00:21 elapsed time, 0:00:53 cpu time, factor 2.43)
Running LLL_Factorization ...
Finished LLL_Factorization (0:00:27 elapsed time, 0:01:07 cpu time, factor 2.41)
Running Polynomial_Factorization ...
Finished Polynomial_Factorization (0:00:26 elapsed time, 0:01:13 cpu time, factor 2.74)
Building Prime_Number_Theorem ...
Finished Prime_Number_Theorem (0:00:25 elapsed time, 0:01:00 cpu time, factor 2.36)
Running Prim_Dijkstra_Simple ...
Finished Prim_Dijkstra_Simple (0:00:25 elapsed time, 0:01:02 cpu time, factor 2.49)
Running LocalLexing ...
Finished LocalLexing (0:00:24 elapsed time, 0:01:10 cpu time, factor 2.88)
Running Closest_Pair_Points ...
Finished Closest_Pair_Points (0:00:25 elapsed time, 0:01:23 cpu time, factor 3.32)
Running Real_Impl ...
Finished Real_Impl (0:00:24 elapsed time, 0:01:02 cpu time, factor 2.53)
Running VerifyThis2018 ...
Finished VerifyThis2018 (0:00:24 elapsed time, 0:00:56 cpu time, factor 2.36)
Running Sort_Encodings ...
Finished Sort_Encodings (0:00:24 elapsed time, 0:00:59 cpu time, factor 2.44)
Running Pi_Calculus ...
Finished Pi_Calculus (0:00:24 elapsed time, 0:01:19 cpu time, factor 3.29)
Running Encodability_Process_Calculi ...
Finished Encodability_Process_Calculi (0:00:23 elapsed time, 0:01:05 cpu time, factor 2.77)
Running Poincare_Disc ...
Finished Poincare_Disc (0:00:21 elapsed time, 0:01:11 cpu time, factor 3.26)
Running Call_Arity ...
Finished Call_Arity (0:00:22 elapsed time, 0:01:13 cpu time, factor 3.32)
Running Power_Sum_Polynomials ...
Finished Power_Sum_Polynomials (0:00:22 elapsed time, 0:00:51 cpu time, factor 2.34)
Running Subset_Boolean_Algebras ...
Finished Subset_Boolean_Algebras (0:00:21 elapsed time, 0:00:48 cpu time, factor 2.20)
Building Saturation_Framework ...
Finished Saturation_Framework (0:00:16 elapsed time, 0:00:38 cpu time, factor 2.27)
Running ComponentDependencies ...
Finished ComponentDependencies (0:00:22 elapsed time, 0:01:10 cpu time, factor 3.09)
Running Generic_Deriving ...
Finished Generic_Deriving (0:00:23 elapsed time, 0:01:06 cpu time, factor 2.86)
Running Partial_Order_Reduction ...
Finished Partial_Order_Reduction (0:00:23 elapsed time, 0:01:12 cpu time, factor 3.13)
Building Prime_Distribution_Elementary ...
Finished Prime_Distribution_Elementary (0:00:30 elapsed time, 0:01:23 cpu time, factor 2.75)
Running LinearQuantifierElim ...
Finished LinearQuantifierElim (0:00:22 elapsed time, 0:01:07 cpu time, factor 2.96)
Running Hybrid_Multi_Lane_Spatial_Logic ...
Finished Hybrid_Multi_Lane_Spatial_Logic (0:00:17 elapsed time, 0:01:01 cpu time, factor 3.61)
Running Knot_Theory ...
Finished Knot_Theory (0:00:23 elapsed time, 0:01:17 cpu time, factor 3.35)
Running Adaptive_State_Counting ...
Finished Adaptive_State_Counting (0:00:22 elapsed time, 0:01:12 cpu time, factor 3.20)
Running ZFC_in_HOL ...
Finished ZFC_in_HOL (0:00:22 elapsed time, 0:01:16 cpu time, factor 3.35)
Building Randomised_Social_Choice ...
Finished Randomised_Social_Choice (0:00:17 elapsed time, 0:00:38 cpu time, factor 2.26)
Running Linear_Inequalities ...
Finished Linear_Inequalities (0:00:23 elapsed time, 0:00:59 cpu time, factor 2.56)
Running Twelvefold_Way ...
Finished Twelvefold_Way (0:00:21 elapsed time, 0:01:02 cpu time, factor 2.92)
Running Hood_Melville_Queue ...
Finished Hood_Melville_Queue (0:00:16 elapsed time, 0:00:44 cpu time, factor 2.76)
Building HOLCF-Library ...
Finished HOLCF-Library (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.29)
Running Bertrands_Postulate ...
Finished Bertrands_Postulate (0:00:21 elapsed time, 0:01:02 cpu time, factor 2.94)
Running Jacobson_Basic_Algebra ...
Finished Jacobson_Basic_Algebra (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.87)
Running SequentInvertibility ...
Finished SequentInvertibility (0:00:21 elapsed time, 0:01:06 cpu time, factor 3.13)
Running LightweightJava ...
Finished LightweightJava (0:00:20 elapsed time, 0:00:41 cpu time, factor 2.02)
Running Robinson_Arithmetic ...
Finished Robinson_Arithmetic (0:00:20 elapsed time, 0:00:59 cpu time, factor 2.93)
Running AutoFocus-Stream ...
Finished AutoFocus-Stream (0:00:20 elapsed time, 0:00:53 cpu time, factor 2.64)
Building HOL-SPARK ...
Finished HOL-SPARK (0:00:20 elapsed time, 0:00:49 cpu time, factor 2.44)
Running Stern_Brocot ...
Finished Stern_Brocot (0:00:20 elapsed time, 0:00:32 cpu time, factor 1.59)
Running Tree-Automata ...
Finished Tree-Automata (0:00:20 elapsed time, 0:00:35 cpu time, factor 1.77)
Running Gaussian_Integers ...
Finished Gaussian_Integers (0:00:19 elapsed time, 0:00:43 cpu time, factor 2.22)
Running HOL-SET_Protocol ...
Finished HOL-SET_Protocol (0:00:18 elapsed time, 0:00:52 cpu time, factor 2.91)
Running Dict_Construction ...
Finished Dict_Construction (0:00:19 elapsed time, 0:00:38 cpu time, factor 2.00)
Building ZF-Constructible ...
Finished ZF-Constructible (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.66)
Building Graph_Theory ...
Finished Graph_Theory (0:00:25 elapsed time, 0:01:05 cpu time, factor 2.60)
Running Koenigsberg_Friendship ...
Finished Koenigsberg_Friendship (0:00:18 elapsed time, 0:00:55 cpu time, factor 3.06)
Running Generalized_Counting_Sort ...
Finished Generalized_Counting_Sort (0:00:20 elapsed time, 0:00:54 cpu time, factor 2.67)
Running HOL-Metis_Examples ...
Finished HOL-Metis_Examples (0:00:17 elapsed time, 0:00:35 cpu time, factor 2.06)
Running HOL-UNITY ...
Finished HOL-UNITY (0:00:17 elapsed time, 0:00:57 cpu time, factor 3.24)
Running Statecharts ...
Finished Statecharts (0:00:17 elapsed time, 0:00:53 cpu time, factor 3.08)
Running HOL-Quotient_Examples ...
Finished HOL-Quotient_Examples (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.25)
Running Treaps ...
Finished Treaps (0:00:17 elapsed time, 0:00:54 cpu time, factor 3.10)
Running Buchi_Complementation ...
Skipping theories "Complementation_Build" (undefined ISABELLE_MLTON)
Finished Buchi_Complementation (0:00:18 elapsed time, 0:00:44 cpu time, factor 2.46)
Running Smooth_Manifolds ...
Finished Smooth_Manifolds (0:00:17 elapsed time, 0:00:48 cpu time, factor 2.75)
Running SIFUM_Type_Systems ...
Finished SIFUM_Type_Systems (0:00:17 elapsed time, 0:00:52 cpu time, factor 2.94)
Running Formula_Derivatives-Examples ...
Finished Formula_Derivatives-Examples (0:00:17 elapsed time, 0:00:48 cpu time, factor 2.83)
Running Separation_Algebra ...
Finished Separation_Algebra (0:00:16 elapsed time, 0:00:53 cpu time, factor 3.18)
Running UTP ...
Finished UTP (0:00:17 elapsed time, 0:00:51 cpu time, factor 2.96)
Running Concurrent_Revisions ...
Finished Concurrent_Revisions (0:00:16 elapsed time, 0:00:46 cpu time, factor 2.84)
Building DynamicArchitectures ...
Finished DynamicArchitectures (0:00:14 elapsed time, 0:00:28 cpu time, factor 2.05)
Running SuperCalc ...
Finished SuperCalc (0:00:15 elapsed time, 0:00:44 cpu time, factor 2.81)
Running PCF ...
Finished PCF (0:00:15 elapsed time, 0:00:38 cpu time, factor 2.42)
Running SDS_Impossibility ...
Finished SDS_Impossibility (0:00:16 elapsed time, 0:00:35 cpu time, factor 2.20)
Running SIFPL ...
Finished SIFPL (0:00:15 elapsed time, 0:00:43 cpu time, factor 2.81)
Running Valuation ...
Finished Valuation (0:00:15 elapsed time, 0:00:48 cpu time, factor 3.07)
Running Incredible_Proof_Machine ...
Finished Incredible_Proof_Machine (0:00:15 elapsed time, 0:00:50 cpu time, factor 3.16)
Running Circus ...
Finished Circus (0:00:15 elapsed time, 0:00:52 cpu time, factor 3.32)
Running Kruskal ...
Finished Kruskal (0:00:15 elapsed time, 0:00:43 cpu time, factor 2.80)
Running WOOT_Strong_Eventual_Consistency ...
Finished WOOT_Strong_Eventual_Consistency (0:00:14 elapsed time, 0:00:50 cpu time, factor 3.48)
Building Quick_Sort_Cost ...
Finished Quick_Sort_Cost (0:00:18 elapsed time, 0:00:42 cpu time, factor 2.33)
Building CRDT ...
Finished CRDT (0:00:13 elapsed time, 0:00:34 cpu time, factor 2.57)
Running Probabilistic_System_Zoo ...
Finished Probabilistic_System_Zoo (0:00:15 elapsed time, 0:00:49 cpu time, factor 3.13)
Running FunWithTilings ...
Finished FunWithTilings (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.58)
Running LTL_Normal_Form ...
Finished LTL_Normal_Form (0:00:13 elapsed time, 0:00:37 cpu time, factor 2.78)
Running Myhill-Nerode ...
Finished Myhill-Nerode (0:00:14 elapsed time, 0:00:33 cpu time, factor 2.34)
Running UpDown_Scheme ...
Finished UpDown_Scheme (0:00:14 elapsed time, 0:00:50 cpu time, factor 3.45)
Building Noninterference_CSP ...
Finished Noninterference_CSP (0:00:07 elapsed time, 0:00:14 cpu time, factor 1.81)
Running Monomorphic_Monad ...
Finished Monomorphic_Monad (0:00:14 elapsed time, 0:00:25 cpu time, factor 1.72)
Running Forcing ...
Finished Forcing (0:00:13 elapsed time, 0:00:40 cpu time, factor 3.10)
Running VectorSpace ...
Finished VectorSpace (0:00:13 elapsed time, 0:00:32 cpu time, factor 2.42)
Running Saturation_Framework_Extensions ...
Finished Saturation_Framework_Extensions (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.71)
Running Localization_Ring ...
Finished Localization_Ring (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04)
Running Zeta_3_Irrational ...
Finished Zeta_3_Irrational (0:00:14 elapsed time, 0:00:48 cpu time, factor 3.34)
Running Gauss_Sums ...
Finished Gauss_Sums (0:00:12 elapsed time, 0:00:41 cpu time, factor 3.20)
Running Residuated_Lattices ...
Finished Residuated_Lattices (0:00:14 elapsed time, 0:00:27 cpu time, factor 1.86)
Running Splay_Tree ...
Finished Splay_Tree (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.77)
Running Possibilistic_Noninterference ...
Finished Possibilistic_Noninterference (0:00:12 elapsed time, 0:00:34 cpu time, factor 2.64)
Running Tarskis_Geometry ...
Finished Tarskis_Geometry (0:00:13 elapsed time, 0:00:43 cpu time, factor 3.31)
Running Finite-Map-Extras ...
Finished Finite-Map-Extras (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.47)
Running Decl_Sem_Fun_PL ...
Finished Decl_Sem_Fun_PL (0:00:12 elapsed time, 0:00:40 cpu time, factor 3.25)
Running ROBDD ...
Finished ROBDD (0:00:13 elapsed time, 0:00:31 cpu time, factor 2.29)
Running Special_Function_Bounds ...
Finished Special_Function_Bounds (0:00:13 elapsed time, 0:00:30 cpu time, factor 2.36)
Running Architectural_Design_Patterns ...
Finished Architectural_Design_Patterns (0:00:13 elapsed time, 0:00:32 cpu time, factor 2.30)
Building FOL-Fitting ...
Finished FOL-Fitting (0:00:17 elapsed time, 0:00:35 cpu time, factor 2.05)
Running Rewriting_Z ...
Finished Rewriting_Z (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.17)
Running Consensus_Refined ...
Finished Consensus_Refined (0:00:12 elapsed time, 0:00:41 cpu time, factor 3.43)
Running Diophantine_Eqns_Lin_Hom ...
Finished Diophantine_Eqns_Lin_Hom (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.13)
Running Graph_Saturation ...
Finished Graph_Saturation (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.53)
Running AxiomaticCategoryTheory ...
Finished AxiomaticCategoryTheory (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.67)
Building Noninterference_Ipurge_Unwinding ...
Finished Noninterference_Ipurge_Unwinding (0:00:07 elapsed time, 0:00:14 cpu time, factor 1.87)
Running Heard_Of ...
Finished Heard_Of (0:00:11 elapsed time, 0:00:34 cpu time, factor 3.09)
Running Locally-Nameless-Sigma ...
Finished Locally-Nameless-Sigma (0:00:11 elapsed time, 0:00:36 cpu time, factor 3.23)
Running Well_Quasi_Orders ...
Finished Well_Quasi_Orders (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.29)
Running HOL-Hoare ...
Finished HOL-Hoare (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.24)
Running Shivers-CFA ...
Finished Shivers-CFA (0:00:11 elapsed time, 0:00:32 cpu time, factor 2.80)
Running VerifyThis2019 ...
Finished VerifyThis2019 (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.33)
Building HOL-Eisbach ...
Finished HOL-Eisbach (0:00:08 elapsed time, 0:00:17 cpu time, factor 2.18)
Running IEEE_Floating_Point ...
Finished IEEE_Floating_Point (0:00:11 elapsed time, 0:00:31 cpu time, factor 2.68)
Running Modular_Assembly_Kit_Security ...
Finished Modular_Assembly_Kit_Security (0:00:12 elapsed time, 0:00:38 cpu time, factor 3.17)
Running Projective_Geometry ...
Finished Projective_Geometry (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.77)
Running PLM ...
Finished PLM (0:00:11 elapsed time, 0:00:28 cpu time, factor 2.55)
Running Presburger-Automata ...
Finished Presburger-Automata (0:00:11 elapsed time, 0:00:30 cpu time, factor 2.71)
Running Lambda_Free_EPO ...
Finished Lambda_Free_EPO (0:00:11 elapsed time, 0:00:35 cpu time, factor 3.18)
Running WHATandWHERE_Security ...
Finished WHATandWHERE_Security (0:00:10 elapsed time, 0:00:34 cpu time, factor 3.22)
Building Noninterference_Sequential_Composition ...
Finished Noninterference_Sequential_Composition (0:00:12 elapsed time, 0:00:29 cpu time, factor 2.35)
Running DiskPaxos ...
Finished DiskPaxos (0:00:10 elapsed time, 0:00:34 cpu time, factor 3.19)
Running TESL_Language ...
Finished TESL_Language (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.69)
Running Tutorial ...
Finished Tutorial (0:00:10 elapsed time, 0:00:31 cpu time, factor 2.96)
Running ADS_Functor ...
Finished ADS_Functor (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.23)
Running Show ...
Finished Show (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.37)
Running Generic_Join ...
Finished Generic_Join (0:00:09 elapsed time, 0:00:30 cpu time, factor 3.11)
Running Hybrid_Logic ...
Finished Hybrid_Logic (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.47)
Running NormByEval ...
Finished NormByEval (0:00:10 elapsed time, 0:00:22 cpu time, factor 2.22)
Running Fishburn_Impossibility ...
Finished Fishburn_Impossibility (0:00:10 elapsed time, 0:00:32 cpu time, factor 3.13)
Running Quaternions ...
Finished Quaternions (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.23)
Running Lp ...
Finished Lp (0:00:11 elapsed time, 0:00:31 cpu time, factor 2.81)
Running HOL-Analysis-ex ...
Finished HOL-Analysis-ex (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.43)
Building HOL-Mirabelle ...
Finished HOL-Mirabelle (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.34)
Running Isar_Ref ...
Finished Isar_Ref (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.18)
Running FocusStreamsCaseStudies ...
Finished FocusStreamsCaseStudies (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.55)
Building Abstract_Completeness ...
Finished Abstract_Completeness (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.66)
Running PSemigroupsConvolution ...
Finished PSemigroupsConvolution (0:00:10 elapsed time, 0:00:21 cpu time, factor 2.15)
Running XML ...
Finished XML (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.85)
Running pGCL ...
Finished pGCL (0:00:10 elapsed time, 0:00:34 cpu time, factor 3.28)
Running Boolean_Expression_Checkers ...
Finished Boolean_Expression_Checkers (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.61)
Running HOL-Mirabelle-ex ...
Finished HOL-Mirabelle-ex (0:00:09 elapsed time)
Running InformationFlowSlicing_Inter ...
Finished InformationFlowSlicing_Inter (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.55)
Building IOA ...
Finished IOA (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.29)
Running Noninterference_Generic_Unwinding ...
Finished Noninterference_Generic_Unwinding (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.16)
Running Weight_Balanced_Trees ...
Finished Weight_Balanced_Trees (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.25)
Running Knuth_Morris_Pratt ...
Finished Knuth_Morris_Pratt (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.47)
Running Program-Conflict-Analysis ...
Finished Program-Conflict-Analysis (0:00:09 elapsed time, 0:00:27 cpu time, factor 2.92)
Running FLP ...
Finished FLP (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.47)
Running HOL-Statespace ...
Finished HOL-Statespace (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.14)
Building Haskell ...
Finished Haskell (0:00:08 elapsed time)
Building Random_BSTs ...
Finished Random_BSTs (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.64)
Running Kuratowski_Closure_Complement ...
Finished Kuratowski_Closure_Complement (0:00:09 elapsed time, 0:00:24 cpu time, factor 2.66)
Running Finite_Automata_HF ...
Finished Finite_Automata_HF (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.17)
Running Types_Tableaus_and_Goedels_God ...
Finished Types_Tableaus_and_Goedels_God (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.22)
Running Budan_Fourier ...
Finished Budan_Fourier (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.57)
Running Approximation_Algorithms ...
Finished Approximation_Algorithms (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.95)
Running IMP2_Binary_Heap ...
Finished IMP2_Binary_Heap (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.30)
Running Trie ...
Finished Trie (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.14)
Running Finger-Trees ...
Finished Finger-Trees (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.75)
Running Efficient-Mergesort ...
Finished Efficient-Mergesort (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.53)
Running BNF_CC ...
Finished BNF_CC (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.93)
Running Ribbon_Proofs ...
Finished Ribbon_Proofs (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.90)
Running Posix-Lexing ...
Finished Posix-Lexing (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.73)
Running System ...
Finished System (0:00:08 elapsed time)
Running FOL_Harrison ...
Finished FOL_Harrison (0:00:07 elapsed time, 0:00:14 cpu time, factor 1.83)
Running Sliding_Window_Algorithm ...
Finished Sliding_Window_Algorithm (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.48)
Running IMAP-CRDT ...
Finished IMAP-CRDT (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.31)
Running Optics ...
Finished Optics (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.24)
Running RSAPSS ...
Finished RSAPSS (0:00:08 elapsed time, 0:00:23 cpu time, factor 2.61)
Running Lowe_Ontological_Argument ...
Finished Lowe_Ontological_Argument (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.98)
Running POPLmark-deBruijn ...
Finished POPLmark-deBruijn (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.86)
Running Binomial-Heaps ...
Finished Binomial-Heaps (0:00:08 elapsed time, 0:00:20 cpu time, factor 2.43)
Running Decreasing-Diagrams-II ...
Finished Decreasing-Diagrams-II (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.83)
Running Transitive-Closure-II ...
Finished Transitive-Closure-II (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.58)
Running HOL-Matrix_LP ...
Finished HOL-Matrix_LP (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.54)
Running Pell ...
Finished Pell (0:00:08 elapsed time, 0:00:23 cpu time, factor 2.74)
Running Priority_Queue_Braun ...
Finished Priority_Queue_Braun (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.34)
Running Coinductive_Languages ...
Finished Coinductive_Languages (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.75)
Running Minsky_Machines ...
Finished Minsky_Machines (0:00:08 elapsed time, 0:00:23 cpu time, factor 2.80)
Running Floyd_Warshall ...
Finished Floyd_Warshall (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.27)
Running Octonions ...
Finished Octonions (0:00:08 elapsed time, 0:00:23 cpu time, factor 2.81)
Running Complete_Non_Orders ...
Finished Complete_Non_Orders (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.68)
Running CISC-Kernel ...
Finished CISC-Kernel (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.95)
Running Functional-Automata ...
Finished Functional-Automata (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.73)
Running OpSets ...
Finished OpSets (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.87)
Running HOL-Examples ...
Finished HOL-Examples (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.19)
Running Name_Carrying_Type_Inference ...
Finished Name_Carrying_Type_Inference (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.70)
Running Derangements ...
Finished Derangements (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.66)
Running Polynomial_Interpolation ...
Finished Polynomial_Interpolation (0:00:08 elapsed time, 0:00:24 cpu time, factor 3.09)
Running Completeness ...
Finished Completeness (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.46)
Running GraphMarkingIBP ...
Finished GraphMarkingIBP (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.51)
Running SenSocialChoice ...
Finished SenSocialChoice (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.55)
Building HOL-Nonstandard_Analysis ...
Finished HOL-Nonstandard_Analysis (0:00:14 elapsed time, 0:00:29 cpu time, factor 2.08)
Running Jordan_Hoelder ...
Finished Jordan_Hoelder (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.59)
Running HOL-Induct ...
Finished HOL-Induct (0:00:06 elapsed time, 0:00:19 cpu time, factor 2.77)
Running BNF_Operations ...
Finished BNF_Operations (0:00:07 elapsed time, 0:00:21 cpu time, factor 3.10)
Running TLA ...
Finished TLA (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.83)
Running List_Inversions ...
Finished List_Inversions (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.74)
Running HOL-Types_To_Sets ...
Finished HOL-Types_To_Sets (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.72)
Building ZF-Induct ...
Finished ZF-Induct (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.20)
Running Stream_Fusion_Code ...
Finished Stream_Fusion_Code (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.57)
Running Cayley_Hamilton ...
Finished Cayley_Hamilton (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.81)
Running Fermat3_4 ...
Finished Fermat3_4 (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.67)
Running Lambda_Free_RPOs ...
Finished Lambda_Free_RPOs (0:00:07 elapsed time, 0:00:22 cpu time, factor 3.10)
Building HOL-SPARK-Examples ...
Finished HOL-SPARK-Examples (0:00:11 elapsed time, 0:00:23 cpu time, factor 2.14)
Running CCS ...
Finished CCS (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.53)
Running Median_Of_Medians_Selection ...
Finished Median_Of_Medians_Selection (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.21)
Running Nash_Williams ...
Finished Nash_Williams (0:00:06 elapsed time, 0:00:21 cpu time, factor 3.12)
Running Category2 ...
Finished Category2 (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.89)
Running Constructor_Funs ...
Finished Constructor_Funs (0:00:06 elapsed time, 0:00:04 cpu time, factor 0.65)
Running Hello_World ...
Finished Hello_World (0:00:06 elapsed time)
Running Decreasing-Diagrams ...
Finished Decreasing-Diagrams (0:00:06 elapsed time, 0:00:18 cpu time, factor 2.68)
Running Catalan_Numbers ...
Finished Catalan_Numbers (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.68)
Running Knuth_Bendix_Order ...
Finished Knuth_Bendix_Order (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.98)
Running HOL-TPTP ...
Finished HOL-TPTP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.11)
Running Strong_Security ...
Finished Strong_Security (0:00:05 elapsed time, 0:00:15 cpu time, factor 2.67)
Running Sturm_Tarski ...
Finished Sturm_Tarski (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.12)
Running AVL-Trees ...
Finished AVL-Trees (0:00:06 elapsed time, 0:00:18 cpu time, factor 2.92)
Running JiveDataStoreModel ...
Finished JiveDataStoreModel (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.88)
Running PropResPI ...
Finished PropResPI (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.08)
Building HOL-TLA ...
Finished HOL-TLA (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.46)
Running Abstract_Soundness ...
Finished Abstract_Soundness (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.75)
Building FOL ...
Finished FOL (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.05)
Running Euler_MacLaurin ...
Finished Euler_MacLaurin (0:00:06 elapsed time, 0:00:19 cpu time, factor 2.87)
Running KD_Tree ...
Finished KD_Tree (0:00:06 elapsed time, 0:00:18 cpu time, factor 2.74)
Running HOLCF-Tutorial ...
Finished HOLCF-Tutorial (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.28)
Running Inductive_Confidentiality ...
Finished Inductive_Confidentiality (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.51)
Running Random_Graph_Subgraph_Threshold ...
Finished Random_Graph_Subgraph_Threshold (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.73)
Running Euler_Partition ...
Finished Euler_Partition (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.36)
Running HyperCTL ...
Finished HyperCTL (0:00:06 elapsed time, 0:00:16 cpu time, factor 2.63)
Running Pratt_Certificate ...
Finished Pratt_Certificate (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.33)
Running Optimal_BST ...
Finished Optimal_BST (0:00:06 elapsed time, 0:00:18 cpu time, factor 2.95)
Building Bell_Numbers_Spivey ...
Finished Bell_Numbers_Spivey (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.10)
Running Recursion-Theory-I ...
Finished Recursion-Theory-I (0:00:05 elapsed time, 0:00:17 cpu time, factor 2.89)
Running Old_Datatype_Show ...
Finished Old_Datatype_Show (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.11)
Running Orbit_Stabiliser ...
Finished Orbit_Stabiliser (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.42)
Running Randomised_BSTs ...
Finished Randomised_BSTs (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.35)
Running HOL-ZF ...
Finished HOL-ZF (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.59)
Running FeatherweightJava ...
Finished FeatherweightJava (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.13)
Running Lam-ml-Normalization ...
Finished Lam-ml-Normalization (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.66)
Running Neumann_Morgenstern_Utility ...
Finished Neumann_Morgenstern_Utility (0:00:06 elapsed time, 0:00:16 cpu time, factor 2.67)
Running Error_Function ...
Finished Error_Function (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.45)
Running Nullstellensatz ...
Finished Nullstellensatz (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.70)
Running MiniML ...
Finished MiniML (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.75)
Running CryptoBasedCompositionalProperties ...
Finished CryptoBasedCompositionalProperties (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.81)
Running IMO2019 ...
Finished IMO2019 (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.39)
Running MonoBoolTranAlgebra ...
Finished MonoBoolTranAlgebra (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.53)
Running HOL-TLA-Memory ...
Finished HOL-TLA-Memory (0:00:05 elapsed time, 0:00:12 cpu time, factor 2.31)
Running Robbins-Conjecture ...
Finished Robbins-Conjecture (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.86)
Running Typeclass_Hierarchy ...
Finished Typeclass_Hierarchy (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.07)
Running Stream-Fusion ...
Finished Stream-Fusion (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.24)
Running Separata ...
Finished Separata (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.50)
Running Card_Multisets ...
Finished Card_Multisets (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.13)
Running Clean ...
Finished Clean (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.91)
Running Laplace_Transform ...
Finished Laplace_Transform (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.56)
Running HOL-Probability-ex ...
Finished HOL-Probability-ex (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.13)
Running Landau_Symbols ...
Finished Landau_Symbols (0:00:05 elapsed time, 0:00:11 cpu time, factor 1.99)
Running ZF-UNITY ...
Finished ZF-UNITY (0:00:04 elapsed time, 0:00:13 cpu time, factor 3.10)
Running Attack_Trees ...
Finished Attack_Trees (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.04)
Running Skip_Lists ...
Finished Skip_Lists (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.55)
Running Transformer_Semantics ...
Finished Transformer_Semantics (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.34)
Running Huffman ...
Finished Huffman (0:00:05 elapsed time, 0:00:10 cpu time, factor 2.05)
Running Selection_Heap_Sort ...
Finished Selection_Heap_Sort (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.07)
Running Impossible_Geometry ...
Finished Impossible_Geometry (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.77)
Running CCL ...
Finished CCL (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.26)
Running Delta_System_Lemma ...
Finished Delta_System_Lemma (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.56)
Running VolpanoSmith ...
Finished VolpanoSmith (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.75)
Running GPU_Kernel_PL ...
Finished GPU_Kernel_PL (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.49)
Running Latin_Square ...
Finished Latin_Square (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.47)
Running WorkerWrapper ...
Finished WorkerWrapper (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.33)
Running HOL-Hahn_Banach ...
Finished HOL-Hahn_Banach (0:00:04 elapsed time, 0:00:12 cpu time, factor 2.55)
Running InformationFlowSlicing ...
Finished InformationFlowSlicing (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.03)
Running Arith_Prog_Rel_Primes ...
Finished Arith_Prog_Rel_Primes (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.81)
Running Rank_Nullity_Theorem ...
Finished Rank_Nullity_Theorem (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.51)
Running RefinementReactive ...
Finished RefinementReactive (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.09)
Running Tycon ...
Finished Tycon (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.26)
Running FinFun ...
Finished FinFun (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.56)
Running Minimal_SSA ...
Finished Minimal_SSA (0:00:04 elapsed time, 0:00:09 cpu time, factor 1.90)
Running Abstract-Hoare-Logics ...
Finished Abstract-Hoare-Logics (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.71)
Running HOL-Unix ...
Finished HOL-Unix (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.30)
Running First_Welfare_Theorem ...
Finished First_Welfare_Theorem (0:00:04 elapsed time, 0:00:12 cpu time, factor 2.43)
Running Pop_Refinement ...
Finished Pop_Refinement (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.10)
Running Noninterference_Concurrent_Composition ...
Finished Noninterference_Concurrent_Composition (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.52)
Running LambdaMu ...
Finished LambdaMu (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.70)
Running IOA-NTP ...
Finished IOA-NTP (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.78)
Running ZF-ex ...
Finished ZF-ex (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.10)
Running Verified-Prover ...
Finished Verified-Prover (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.82)
Running Tools ...
Finished Tools (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.93)
Running Menger ...
Finished Menger (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.42)
Running Comparison_Sort_Lower_Bound ...
Finished Comparison_Sort_Lower_Bound (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.94)
Running HOLCF-IMP ...
Finished HOLCF-IMP (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.58)
Running Card_Partitions ...
Finished Card_Partitions (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.66)
Running Noninterference_Inductive_Unwinding ...
Finished Noninterference_Inductive_Unwinding (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.46)
Running Binomial-Queues ...
Finished Binomial-Queues (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.69)
Running Partial_Function_MR ...
Finished Partial_Function_MR (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.27)
Running Epistemic_Logic ...
Finished Epistemic_Logic (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.62)
Running FOL_Seq_Calc1 ...
Finished FOL_Seq_Calc1 (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.99)
Running Integration ...
Finished Integration (0:00:04 elapsed time, 0:00:09 cpu time, factor 1.88)
Running HOL-NanoJava ...
Finished HOL-NanoJava (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.59)
Running FileRefinement ...
Finished FileRefinement (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.78)
Running Case_Labeling ...
Finished Case_Labeling (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.06)
Running GoedelGod ...
Finished GoedelGod (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.01)
Running IOA-ABP ...
Finished IOA-ABP (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.60)
Building FOLP ...
Finished FOLP (0:00:01 elapsed time)
Running Concurrent_Ref_Alg ...
Finished Concurrent_Ref_Alg (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.23)
Running SumSquares ...
Finished SumSquares (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.06)
Running Dynamic_Tables ...
Finished Dynamic_Tables (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.04)
Running Stellar_Quorums ...
Finished Stellar_Quorums (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.24)
Running FOL-ex ...
Finished FOL-ex (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.56)
Running Banach_Steinhaus ...
Finished Banach_Steinhaus (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.01)
Running ShortestPath ...
Finished ShortestPath (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.18)
Running Tail_Recursive_Functions ...
Finished Tail_Recursive_Functions (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.57)
Running HOL-Isar_Examples ...
Finished HOL-Isar_Examples (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.85)
Running LCF ...
Finished LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.01)
Running Bounded_Deducibility_Security ...
Finished Bounded_Deducibility_Security (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.77)
Running Ramsey-Infinite ...
Finished Ramsey-Infinite (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.56)
Running Tree_Decomposition ...
Finished Tree_Decomposition (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.07)
Running Implementation ...
Finished Implementation (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.01)
Running Relational-Incorrectness-Logic ...
Finished Relational-Incorrectness-Logic (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.73)
Running MuchAdoAboutTwo ...
Finished MuchAdoAboutTwo (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.62)
Running Topology ...
Finished Topology (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.14)
Running DPT-SAT-Solver ...
Finished DPT-SAT-Solver (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.57)
Running HOL-IMPP ...
Finished HOL-IMPP (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.45)
Running HotelKeyCards ...
Finished HotelKeyCards (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.10)
Running Certification_Monads ...
Finished Certification_Monads (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.26)
Running Compiling-Exceptions-Correctly ...
Finished Compiling-Exceptions-Correctly (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.23)
Running Prog_Prove ...
Finished Prog_Prove (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.31)
Running Goodstein_Lambda ...
Finished Goodstein_Lambda (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.56)
Running Lower_Semicontinuous ...
Finished Lower_Semicontinuous (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.03)
Running Imperative_Insertion_Sort ...
Finished Imperative_Insertion_Sort (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.97)
Running CYK ...
Finished CYK (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.79)
Running Triangle ...
Finished Triangle (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.27)
Running Lazy_Case ...
Finished Lazy_Case (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.12)
Running Matroids ...
Finished Matroids (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.98)
Running Stewart_Apollonius ...
Finished Stewart_Apollonius (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.34)
Running ArrowImpossibilityGS ...
Finished ArrowImpossibilityGS (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.22)
Running Category ...
Finished Category (0:00:03 elapsed time, 0:00:06 cpu time, factor 2.03)
Running Falling_Factorial_Sum ...
Finished Falling_Factorial_Sum (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.01)
Running Chord_Segments ...
Finished Chord_Segments (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.51)
Running Stuttering_Equivalence ...
Finished Stuttering_Equivalence (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.61)
Running Source_Coding_Theorem ...
Finished Source_Coding_Theorem (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.64)
Running TortoiseHare ...
Finished TortoiseHare (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.76)
Running Secondary_Sylow ...
Finished Secondary_Sylow (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.82)
Running LatticeProperties ...
Finished LatticeProperties (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.56)
Running Buffons_Needle ...
Finished Buffons_Needle (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.83)
Running HOL-SPARK-Manual ...
Finished HOL-SPARK-Manual (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.63)
Running FOLP-ex ...
Finished FOLP-ex (0:00:02 elapsed time, 0:00:04 cpu time)
Running Transitive-Closure ...
Finished Transitive-Closure (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.81)
Running Functions ...
Finished Functions (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.04)
Running DataRefinementIBP ...
Finished DataRefinementIBP (0:00:02 elapsed time, 0:00:04 cpu time)
Running ZF-AC ...
Finished ZF-AC (0:00:02 elapsed time, 0:00:05 cpu time)
Running HOLCF-FOCUS ...
Finished HOLCF-FOCUS (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.93)
Running HOLCF-ex ...
Finished HOLCF-ex (0:00:03 elapsed time, 0:00:06 cpu time, factor 2.21)
Running BinarySearchTree ...
Finished BinarySearchTree (0:00:02 elapsed time, 0:00:05 cpu time)
Running List_Interleaving ...
Finished List_Interleaving (0:00:02 elapsed time, 0:00:04 cpu time)
Running Discrete_Summation ...
Finished Discrete_Summation (0:00:02 elapsed time, 0:00:05 cpu time)
Running Pairing_Heap ...
Finished Pairing_Heap (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.86)
Running Fisher_Yates ...
Finished Fisher_Yates (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.59)
Running HOL-Lattice ...
Finished HOL-Lattice (0:00:02 elapsed time, 0:00:03 cpu time)
Running Lifting_Definition_Option ...
Finished Lifting_Definition_Option (0:00:02 elapsed time)
Running C2KA_DistributedSystems ...
Finished C2KA_DistributedSystems (0:00:02 elapsed time, 0:00:03 cpu time)
Running GenClock ...
Finished GenClock (0:00:02 elapsed time, 0:00:04 cpu time)
Running Gauss-Jordan-Elim-Fun ...
Finished Gauss-Jordan-Elim-Fun (0:00:02 elapsed time, 0:00:04 cpu time)
Running Eisbach ...
Finished Eisbach (0:00:02 elapsed time)
Running Surprise_Paradox ...
Finished Surprise_Paradox (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.09)
Running Mason_Stothers ...
Finished Mason_Stothers (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.42)
Running Marriage ...
Finished Marriage (0:00:02 elapsed time, 0:00:03 cpu time)
Running Card_Number_Partitions ...
Finished Card_Number_Partitions (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.88)
Running ClockSynchInst ...
Finished ClockSynchInst (0:00:02 elapsed time, 0:00:04 cpu time)
Running List-Index ...
Finished List-Index (0:00:02 elapsed time, 0:00:04 cpu time)
Running Classes ...
Finished Classes (0:00:02 elapsed time)
Running Sequents ...
Finished Sequents (0:00:01 elapsed time, 0:00:04 cpu time)
Running Lucas_Theorem ...
Finished Lucas_Theorem (0:00:02 elapsed time, 0:00:03 cpu time)
Running HOL-Mutabelle ...
Finished HOL-Mutabelle (0:00:02 elapsed time)
Running Descartes_Sign_Rule ...
Finished Descartes_Sign_Rule (0:00:02 elapsed time, 0:00:04 cpu time)
Running HOL-IOA ...
Finished HOL-IOA (0:00:02 elapsed time)
Running Cartan_FP ...
Finished Cartan_FP (0:00:02 elapsed time, 0:00:03 cpu time)
Running Skew_Heap ...
Finished Skew_Heap (0:00:02 elapsed time)
Running HOL-TLA-Inc ...
Finished HOL-TLA-Inc (0:00:02 elapsed time, 0:00:03 cpu time)
Running Lazy-Lists-II ...
Finished Lazy-Lists-II (0:00:02 elapsed time, 0:00:03 cpu time)
Running JEdit ...
Finished JEdit (0:00:02 elapsed time)
Running Open_Induction ...
Finished Open_Induction (0:00:02 elapsed time, 0:00:03 cpu time)
Running IOA-Storage ...
Finished IOA-Storage (0:00:02 elapsed time)
Running HOL-Nonstandard_Analysis-Examples ...
Finished HOL-Nonstandard_Analysis-Examples (0:00:02 elapsed time, 0:00:03 cpu time)
Running Perfect-Number-Thm ...
Finished Perfect-Number-Thm (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.28)
Running Blue_Eyes ...
Finished Blue_Eyes (0:00:02 elapsed time)
Running Max-Card-Matching ...
Finished Max-Card-Matching (0:00:02 elapsed time)
Running AnselmGod ...
Finished AnselmGod (0:00:02 elapsed time)
Running CofGroups ...
Finished CofGroups (0:00:02 elapsed time)
Running Liouville_Numbers ...
Finished Liouville_Numbers (0:00:02 elapsed time, 0:00:03 cpu time)
Building Naproche ...
Finished Naproche (0:00:00 elapsed time)
Running Minkowskis_Theorem ...
Finished Minkowskis_Theorem (0:00:02 elapsed time, 0:00:03 cpu time)
Running Lehmer ...
Finished Lehmer (0:00:02 elapsed time, 0:00:03 cpu time)
Running Ptolemys_Theorem ...
Finished Ptolemys_Theorem (0:00:02 elapsed time)
Running Locales ...
Finished Locales (0:00:02 elapsed time)
Running HOL-Import ...
Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)
Finished HOL-Import (0:00:02 elapsed time)
Running FunWithFunctions ...
Finished FunWithFunctions (0:00:01 elapsed time)
Running Free-Boolean-Algebra ...
Finished Free-Boolean-Algebra (0:00:01 elapsed time)
Running Monad_Normalisation ...
Finished Monad_Normalisation (0:00:02 elapsed time)
Running ZF-Resid ...
Finished ZF-Resid (0:00:01 elapsed time)
Running Spec_Check ...
Finished Spec_Check (0:00:01 elapsed time)
Running Sugar ...
Finished Sugar (0:00:02 elapsed time)
Running FFT ...
Finished FFT (0:00:01 elapsed time)
Running CTT ...
Finished CTT (0:00:01 elapsed time)
Running RIPEMD-160-SPARK ...
Finished RIPEMD-160-SPARK (0:00:01 elapsed time)
Running IOA-ex ...
Finished IOA-ex (0:00:02 elapsed time)
Running Depth-First-Search ...
Finished Depth-First-Search (0:00:01 elapsed time)
Running HOL-Proofs-ex ...
Finished HOL-Proofs-ex (0:00:02 elapsed time)
Running Main ...
Finished Main (0:00:01 elapsed time)
Running Lorenz_C1 ...
Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
Running Naproche-Test ...
Finished Naproche-Test (0:00:01 elapsed time)
Running ZF-IMP ...
Finished ZF-IMP (0:00:01 elapsed time)
Running General-Triangle ...
Finished General-Triangle (0:00:01 elapsed time)
Running Bondy ...
Finished Bondy (0:00:01 elapsed time)
Running Card_Equiv_Relations ...
Finished Card_Equiv_Relations (0:00:02 elapsed time)
Running Roy_Floyd_Warshall ...
Finished Roy_Floyd_Warshall (0:00:01 elapsed time)
Running Recursion-Addition ...
Finished Recursion-Addition (0:00:01 elapsed time)
Running HOL-Real_Asymp-Manual ...
Finished HOL-Real_Asymp-Manual (0:00:01 elapsed time)
Running ZF-Coind ...
Finished ZF-Coind (0:00:01 elapsed time)
Running Logics_ZF ...
Finished Logics_ZF (0:00:01 elapsed time)
Running Szpilrajn ...
Finished Szpilrajn (0:00:01 elapsed time)
Running HOL-TLA-Buffer ...
Finished HOL-TLA-Buffer (0:00:01 elapsed time)
Running HOL-Prolog ...
Finished HOL-Prolog (0:00:01 elapsed time)
Running Cube ...
Finished Cube (0:00:00 elapsed time)
Running How_to_Prove_it ...
Finished How_to_Prove_it (0:00:01 elapsed time)
Running Pure-Examples ...
Finished Pure-Examples (0:00:00 elapsed time)
Running Aristotles_Assertoric_Syllogistic ...
Finished Aristotles_Assertoric_Syllogistic (0:00:01 elapsed time)
Running Naproche-Build ...
Finished Naproche-Build (0:00:00 elapsed time)
Running Example-Submission ...
Finished Example-Submission (0:00:01 elapsed time)
Running Ordinals_and_Cardinals ...
Finished Ordinals_and_Cardinals (0:00:01 elapsed time)
Running Intro ...
Finished Intro (0:00:00 elapsed time)
Running Logics ...
Finished Logics (0:00:00 elapsed time)
Running Nitpick ...
Finished Nitpick (0:00:00 elapsed time)
Running SML ...
Finished SML (0:00:00 elapsed time)
Running Sledgehammer ...
Finished Sledgehammer (0:00:00 elapsed time)
10:26:25 elapsed time, 29:14:24 cpu time, factor 2.80


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.