Safe_Distance: theory Sturm_Sequences.Sturm_Method
10:32:21Timing Secondary_Sylow (4 threads, 3.897s elapsed time, 12.089s cpu time, 0.654s GC time, factor 3.10)
10:32:21Finished Secondary_Sylow (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.31)
10:32:21Timing Relational_Paths (8 threads, 19.190s elapsed time, 99.752s cpu time, 9.262s GC time, factor 5.20)
10:32:21Finished Relational_Paths (0:00:20 elapsed time, 0:01:41 cpu time, factor 4.96)
10:32:22Safe_Distance: theory Sturm_Sequences.Sturm
10:32:22Separation_Algebra: theory HOL-Hoare.Hoare_Syntax
10:32:22Separation_Algebra: theory HOL-Hoare.Hoare_Tac
10:32:22Separation_Algebra: theory HOL-Library.Phantom_Type
10:32:22Separation_Algebra: theory Separation_Algebra.Map_Extra
10:32:22Safe_Distance: theory HOL-Decision_Procs.Approximation
10:32:22Separata: theory HOL-Eisbach.Eisbach_Tools
10:32:23Separata: theory Separata.Separata
10:32:23Separation_Algebra: theory Separation_Algebra.Separation_Algebra
10:32:23Separation_Algebra: theory HOL-Library.Cardinality
10:32:23S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Montecarlo
10:32:23S_Finite_Measure_Monad: theory S_Finite_Measure_Monad.Query
10:32:23Separation_Algebra: theory Separation_Algebra.Separation_Algebra_Alt
10:32:24Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting
10:32:24Separation_Algebra: theory HOL-Library.Numeral_Type
10:32:24Separation_Algebra: theory Separation_Algebra.Sep_Heap_Instance
10:32:24Separation_Algebra: theory Separation_Algebra.Sep_Tactics
10:32:24Separation_Algebra: theory Separation_Algebra.Sep_Eq
10:32:24Separation_Algebra: theory Separation_Algebra.Sep_Tactics_Test
10:32:25Separation_Algebra: theory HOL-Hoare.Hoare_Logic_Abort
10:32:25Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Replace_Constant
10:32:25Separation_Algebra: theory Separation_Algebra.VM_Example
10:32:25Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_Properties
10:32:25Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_GTRS
10:32:25Separation_Algebra: theory HOL-Library.Type_Length
10:32:25Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_LLRG_LV_Mondaic
10:32:26Separation_Algebra: theory HOL-Library.Word
10:32:27Timing SATSolverVerification (8 threads, 20.578s elapsed time, 120.960s cpu time, 12.195s GC time, factor 5.88)
10:32:27Finished SATSolverVerification (0:00:21 elapsed time, 0:02:02 cpu time, factor 5.65)
10:32:27Separation_Algebra: theory Separation_Algebra.Simple_Separation_Example
10:32:28Timing Robinson_Arithmetic (4 threads, 44.253s elapsed time, 145.678s cpu time, 16.513s GC time, factor 3.29)
10:32:28Finished Robinson_Arithmetic (0:00:46 elapsed time, 0:02:28 cpu time, factor 3.22)
10:32:30Timing Separata (4 threads, 8.760s elapsed time, 26.849s cpu time, 1.347s GC time, factor 3.06)
10:32:30Finished Separata (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.67)
10:32:34Timing Relational_Cardinality (8 threads, 64.549s elapsed time, 121.971s cpu time, 9.276s GC time, factor 1.89)
10:32:34Finished Relational_Cardinality (0:01:05 elapsed time, 0:02:03 cpu time, factor 1.89)
10:32:35Timing Relational_Forests (4 threads, 61.516s elapsed time, 113.123s cpu time, 10.473s GC time, factor 1.84)
10:32:35Finished Relational_Forests (0:01:03 elapsed time, 0:01:55 cpu time, factor 1.82)
10:32:35Roth_Arithmetic_Progressions: theory Girth_Chromatic.Girth_Chromatic
10:32:36Safe_Range_RC: theory Safe_Range_RC.Restrict_Bounds
10:32:36Separation_Algebra: theory Separation_Algebra.Types_D
10:32:36Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
10:32:37Timing SenSocialChoice (4 threads, 17.763s elapsed time, 46.574s cpu time, 3.932s GC time, factor 2.62)
10:32:37Finished SenSocialChoice (0:00:19 elapsed time, 0:00:48 cpu time, factor 2.50)
10:32:37Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
10:32:37Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
10:32:37Roth_Arithmetic_Progressions: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
10:32:37Roth_Arithmetic_Progressions: theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
10:32:39Running Relational_Minimum_Spanning_Trees (on of1-proof) ...
10:32:39Running SequentInvertibility (on of1-proof) ...
10:32:39SequentInvertibility: theory HOL-Library.Cancellation
10:32:39Safe_Range_RC: theory Safe_Range_RC.Restrict_Bounds_Impl
10:32:39Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Kruskal
10:32:39Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Prim
10:32:40Safe_Range_RC: theory Safe_Range_RC.Restrict_Frees
10:32:40SequentInvertibility: theory HOL-Library.Multiset
10:32:41Root_Balanced_Tree: theory Root_Balanced_Tree.Root_Balanced_Tree_Tab
10:32:41Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Boruvka
10:32:42Safe_Distance: theory Safe_Distance.Safe_Distance
10:32:42Separation_Algebra: theory Separation_Algebra.Abstract_Separation_D
10:32:42Running Shivers-CFA (on of2.proof.cit.tum.de) ...
10:32:42Running Show (on of2.proof.cit.tum.de) ...
10:32:42SequentInvertibility: theory SequentInvertibility.ModalSequents
10:32:42SequentInvertibility: theory SequentInvertibility.MultiSequents
10:32:42SequentInvertibility: theory SequentInvertibility.SRCTransforms
10:32:42SequentInvertibility: theory SequentInvertibility.SingleSuccedent
10:32:42SequentInvertibility: theory SequentInvertibility.NominalSequents
10:32:43Shivers-CFA: theory HOL-Library.Adhoc_Overloading
10:32:43Shivers-CFA: theory Shivers-CFA.FixTransform
10:32:43Shivers-CFA: theory Shivers-CFA.CPSScheme
10:32:43Shivers-CFA: theory Shivers-CFA.HOLCFUtils
10:32:43Shivers-CFA: theory Shivers-CFA.SetMap
10:32:43Shivers-CFA: theory Shivers-CFA.Utils
10:32:43Safe_Distance: theory Safe_Distance.Evaluation
10:32:43Safe_Distance: theory Safe_Distance.Safe_Distance_Reaction
10:32:43Shivers-CFA: theory Shivers-CFA.Computability
10:32:43Shivers-CFA: theory Shivers-CFA.MapSets
10:32:43Show: theory HOL-Computational_Algebra.Factorial_Ring
10:32:43Show: theory Show.Show
10:32:44Show: theory Show.Show_Instances
10:32:44Show: theory Show.Show_Real
10:32:44Show: theory Show.Show_Complex
10:32:44Separation_Algebra: theory Separation_Algebra.Separation_D
10:32:44Safe_Range_RC: theory Safe_Range_RC.Restrict_Frees_Impl
10:32:44Show: theory Show.Show_Real_Impl
10:32:45Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_GTRS
10:32:45Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_LLRG
10:32:45Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_LV
10:32:45Running Sigma_Commit_Crypto (on of4.proof.cit.tum.de) ...
10:32:45Running Skew_Heap (on of4.proof.cit.tum.de) ...
10:32:46Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
10:32:46Safe_Range_RC: theory Safe_Range_RC.Examples
10:32:46Skew_Heap: theory HOL-Data_Structures.Heaps
10:32:46Skew_Heap: theory Skew_Heap.Skew_Heap
10:32:46Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
10:32:46Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
10:32:46Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
10:32:46Shivers-CFA: theory Shivers-CFA.CPSUtils
10:32:46Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
10:32:46Shivers-CFA: theory Shivers-CFA.Eval
10:32:46Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
10:32:46Shivers-CFA: theory Shivers-CFA.AbsCF
10:32:46Shivers-CFA: theory Shivers-CFA.ExCF
10:32:46Sigma_Commit_Crypto: theory HOL-Algebra.Ring
10:32:47Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
10:32:47Timing Skew_Heap (8 threads, 0.795s elapsed time, 1.240s cpu time, 0.086s GC time, factor 1.56)
10:32:47Finished Skew_Heap (0:00:01 elapsed time)
10:32:47Sigma_Commit_Crypto: theory HOL-Algebra.Elementary_Groups
10:32:47Shivers-CFA: theory Shivers-CFA.ExCFSV
10:32:47Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
10:32:47Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
10:32:47Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
10:32:47Safe_Range_RC: theory Safe_Range_RC.Results
10:32:47Show: theory HOL-Computational_Algebra.Polynomial
10:32:48Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
10:32:48Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
10:32:48Shivers-CFA: theory Shivers-CFA.AbsCFComp
10:32:48SequentInvertibility: theory SequentInvertibility.SequentInvertibility
10:32:49Timing S_Finite_Measure_Monad (8 threads, 35.995s elapsed time, 190.289s cpu time, 11.246s GC time, factor 5.29)
10:32:49Finished S_Finite_Measure_Monad (0:00:37 elapsed time, 0:03:12 cpu time, factor 5.13)
10:32:49Timing Root_Balanced_Tree (4 threads, 61.772s elapsed time, 199.436s cpu time, 18.320s GC time, factor 3.23)
10:32:49Finished Root_Balanced_Tree (0:01:04 elapsed time, 0:03:23 cpu time, factor 3.16)
10:32:49Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
10:32:49Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
10:32:49Running Splay_Tree (on of3.proof.cit.tum.de) ...
10:32:50Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
10:32:50Sigma_Commit_Crypto: theory HOL-Algebra.Module
10:32:50Splay_Tree: theory HOL-Data_Structures.Cmp
10:32:50Splay_Tree: theory HOL-Data_Structures.Less_False
10:32:50Splay_Tree: theory Splay_Tree.Splay_Heap
10:32:50Splay_Tree: theory HOL-Data_Structures.Sorted_Less
10:32:50Splay_Tree: theory HOL-Data_Structures.AList_Upd_Del
10:32:50Splay_Tree: theory HOL-Data_Structures.List_Ins_Del
10:32:50Splay_Tree: theory HOL-Data_Structures.Set_Specs
10:32:50Splay_Tree: theory Splay_Tree.Splay_Tree
10:32:50Building Sqrt_Babylonian (on 10.195.8.29) ...
10:32:50Splay_Tree: theory HOL-Data_Structures.Map_Specs
10:32:51Splay_Tree: theory Splay_Tree.Splay_Map
10:32:51Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
10:32:52Running Stable_Matching (on 10.195.6.179) ...
10:32:52Timing Shivers-CFA (8 threads, 7.673s elapsed time, 29.258s cpu time, 2.350s GC time, factor 3.81)
10:32:52Finished Shivers-CFA (0:00:08 elapsed time, 0:00:30 cpu time, factor 3.55)
10:32:52Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
10:32:52Timing SIFUM_Type_Systems (4 threads, 40.131s elapsed time, 138.056s cpu time, 13.387s GC time, factor 3.44)
10:32:52Finished SIFUM_Type_Systems (0:00:42 elapsed time, 0:02:20 cpu time, factor 3.35)
10:32:52Show: theory Show.Show_Poly
10:32:52Timing Separation_Algebra (4 threads, 29.130s elapsed time, 97.545s cpu time, 11.004s GC time, factor 3.35)
10:32:52Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
10:32:52Finished Separation_Algebra (0:00:30 elapsed time, 0:01:39 cpu time, factor 3.25)
10:32:53Sqrt_Babylonian: theory Sqrt_Babylonian.Log_Impl
10:32:53Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
10:32:53Sqrt_Babylonian: theory Sqrt_Babylonian.NthRoot_Impl
10:32:53Stable_Matching: theory Stable_Matching.Basis
10:32:53Stable_Matching: theory Stable_Matching.Sotomayor
10:32:54Timing Show (8 threads, 9.231s elapsed time, 28.621s cpu time, 3.287s GC time, factor 3.10)
10:32:54Finished Show (0:00:10 elapsed time, 0:00:29 cpu time, factor 2.89)
10:32:54Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian
10:32:54Stable_Matching: theory Stable_Matching.Choice_Functions
10:32:54Timing Rewrite_Properties_Reduction (4 threads, 74.752s elapsed time, 231.542s cpu time, 15.646s GC time, factor 3.10)
10:32:54Finished Rewrite_Properties_Reduction (0:01:17 elapsed time, 0:03:55 cpu time, factor 3.05)
10:32:55Running Standard_Borel_Spaces (on 10.195.8.46) ...
10:32:55Stable_Matching: theory Stable_Matching.Contracts
10:32:56Running Statecharts (on 10.195.8.30) ...
10:32:56Timing Relational_Minimum_Spanning_Trees (8 threads, 16.150s elapsed time, 65.629s cpu time, 5.659s GC time, factor 4.06)
10:32:56Finished Relational_Minimum_Spanning_Trees (0:00:17 elapsed time, 0:01:06 cpu time, factor 3.87)
10:32:56Running Stellar_Quorums (on 10.195.8.40) ...
10:32:56Standard_Borel_Spaces: theory Standard_Borel_Spaces.Lemmas_StandardBorel
10:32:56Timing SequentInvertibility (8 threads, 16.055s elapsed time, 74.519s cpu time, 9.282s GC time, factor 4.64)
10:32:56Finished SequentInvertibility (0:00:17 elapsed time, 0:01:16 cpu time, factor 4.44)
10:32:57Statecharts: theory Statecharts.Kripke
10:32:57Statecharts: theory Statecharts.Contrib
10:32:57Statecharts: theory Statecharts.DataSpace
10:32:57Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
10:32:57Statecharts: theory Statecharts.Data
10:32:58Running Stern_Brocot (on 10.195.8.40) ...
10:32:58Timing Roth_Arithmetic_Progressions (8 threads, 47.754s elapsed time, 185.956s cpu time, 20.700s GC time, factor 3.89)
10:32:58Finished Roth_Arithmetic_Progressions (0:00:53 elapsed time, 0:03:22 cpu time, factor 3.81)
10:32:58Statecharts: theory Statecharts.Update
10:32:58Statecharts: theory Statecharts.Expr
10:32:59Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
10:32:59Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Space
10:32:59Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
10:32:59Running Stewart_Apollonius (on 10.195.8.11) ...
10:32:59Building Stirling_Formula (on 10.195.8.11) ...
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
10:33:00Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
10:33:00Stern_Brocot: theory Stern_Brocot.Cotree
10:33:00Timing Splay_Tree (8 threads, 10.699s elapsed time, 24.912s cpu time, 1.467s GC time, factor 2.33)
10:33:00Finished Splay_Tree (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.24)
10:33:01Stewart_Apollonius: theory Triangle.Angles
10:33:01Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Product
10:33:02Safe_OCL: theory Safe_OCL.OCL_Syntax
10:33:02Stable_Matching: theory Stable_Matching.COP
10:33:02Stirling_Formula: theory HOL-Library.Function_Algebras
10:33:02Stirling_Formula: theory Landau_Symbols.Group_Sort
10:33:02Statecharts: theory Statecharts.SA
10:33:02Stewart_Apollonius: theory Triangle.Triangle
10:33:02Statecharts: theory Statecharts.HA
10:33:02Standard_Borel_Spaces: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
10:33:03Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
10:33:03Timing Safe_Distance (8 threads, 50.775s elapsed time, 223.248s cpu time, 46.966s GC time, factor 4.40)
10:33:03Finished Safe_Distance (0:00:52 elapsed time, 0:03:46 cpu time, factor 4.33)
10:33:03Standard_Borel_Spaces: theory Standard_Borel_Spaces.StandardBorel
10:33:03Statecharts: theory Statecharts.HAOps
10:33:03Statecharts: theory Statecharts.HASem
10:33:04Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
10:33:05Statecharts: theory Statecharts.HAKripke
10:33:05Statecharts: theory Statecharts.CarAudioSystem
10:33:05Timing Stellar_Quorums (4 threads, 5.920s elapsed time, 16.572s cpu time, 0.789s GC time, factor 2.80)
10:33:05Finished Stellar_Quorums (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.41)
10:33:05Stable_Matching: theory Stable_Matching.Bossiness
10:33:06Timing Stewart_Apollonius (4 threads, 4.213s elapsed time, 7.259s cpu time, 0.295s GC time, factor 1.72)
10:33:06Finished Stewart_Apollonius (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.44)
10:33:07Stable_Matching: theory Stable_Matching.Strategic
10:33:08Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
10:33:08Timing Sigma_Commit_Crypto (8 threads, 21.545s elapsed time, 107.467s cpu time, 10.139s GC time, factor 4.99)
10:33:08Finished Sigma_Commit_Crypto (0:00:23 elapsed time, 0:01:50 cpu time, factor 4.75)
10:33:09Timing Sqrt_Babylonian (4 threads, 10.606s elapsed time, 27.497s cpu time, 2.205s GC time, factor 2.59)
10:33:09Finished Sqrt_Babylonian (0:00:18 elapsed time, 0:00:39 cpu time, factor 2.10)
10:33:09Stirling_Formula: theory Landau_Symbols.Landau_More
10:33:09Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
10:33:10Stirling_Formula: theory Stirling_Formula.Stirling_Formula
10:33:12Stirling_Formula: theory Stirling_Formula.Gamma_Asymptotics
10:33:13Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
10:33:18Running Store_Buffer_Reduction (on of1-proof) ...
10:33:18Running Stream-Fusion (on of1-proof) ...
10:33:18Timing Schutz_Spacetime (4 threads, 61.619s elapsed time, 211.272s cpu time, 16.150s GC time, factor 3.43)
10:33:18Finished Schutz_Spacetime (0:01:03 elapsed time, 0:03:34 cpu time, factor 3.36)
10:33:18Stream-Fusion: theory HOLCF-Library.Int_Discrete
10:33:18Store_Buffer_Reduction: theory Store_Buffer_Reduction.ReduceStoreBuffer
10:33:18Store_Buffer_Reduction: theory Store_Buffer_Reduction.SyntaxTweaks
10:33:18Stream-Fusion: theory Stream-Fusion.LazyList
10:33:19Stream-Fusion: theory Stream-Fusion.Stream
10:33:19Stream-Fusion: theory Stream-Fusion.StreamFusion
10:33:22Timing Stream-Fusion (8 threads, 3.151s elapsed time, 5.012s cpu time, 0.310s GC time, factor 1.59)
10:33:22Finished Stream-Fusion (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.46)
10:33:23Running StrictOmegaCategories (on of2.proof.cit.tum.de) ...
10:33:23Running Strong_Security (on of2.proof.cit.tum.de) ...
10:33:23Building Sturm_Sequences (on of2.proof.cit.tum.de) ...
10:33:23StrictOmegaCategories: theory HOL-Library.FuncSet
10:33:23Strong_Security: theory Strong_Security.Types
10:33:24Strong_Security: theory Strong_Security.Expr
10:33:24Strong_Security: theory Strong_Security.MWLf
10:33:24Strong_Security: theory Strong_Security.Strong_Security
10:33:24Strong_Security: theory Strong_Security.Up_To_Technique
10:33:24Strong_Security: theory Strong_Security.Parallel_Composition
10:33:24Sturm_Sequences: theory Pure-ex.Guess
10:33:24Sturm_Sequences: theory Sturm_Sequences.Sturm_Library_Document
10:33:24Sturm_Sequences: theory Sturm_Sequences.Misc_Polynomial
10:33:24StrictOmegaCategories: theory StrictOmegaCategories.Globular_Set
10:33:24Strong_Security: theory Strong_Security.Domain_example
10:33:25Running Sturm_Tarski (on of4.proof.cit.tum.de) ...
10:33:25Running Stuttering_Equivalence (on of4.proof.cit.tum.de) ...
10:33:25Running Subset_Boolean_Algebras (on of4.proof.cit.tum.de) ...
10:33:25StrictOmegaCategories: theory StrictOmegaCategories.Strict_Omega_Category
10:33:25StrictOmegaCategories: theory StrictOmegaCategories.Pasting_Diagram
10:33:25Subset_Boolean_Algebras: theory Subset_Boolean_Algebras.Subset_Boolean_Algebras
10:33:25Sturm_Sequences: theory Sturm_Sequences.Sturm_Library
10:33:25Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
10:33:25Sturm_Sequences: theory Sturm_Sequences.Sturm_Theorem
10:33:25Strong_Security: theory Strong_Security.Language_Composition
10:33:25Sturm_Tarski: theory Polynomial_Interpolation.Missing_Unsorted
10:33:25Sturm_Tarski: theory Sturm_Tarski.PolyMisc
10:33:25Sturm_Tarski: theory Polynomial_Interpolation.Ring_Hom
10:33:25Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
10:33:25Strong_Security: theory Strong_Security.Type_System
10:33:26Sturm_Tarski: theory Sturm_Tarski.Sturm_Tarski
10:33:26Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
10:33:26Strong_Security: theory Strong_Security.Type_System_example
10:33:26Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
10:33:26Sturm_Sequences: theory Sturm_Sequences.Sturm_Method
10:33:26Store_Buffer_Reduction: theory Store_Buffer_Reduction.ReduceStoreBufferSimulation
10:33:27Sturm_Tarski: theory Polynomial_Interpolation.Missing_Polynomial
10:33:27Sturm_Sequences: theory Sturm_Sequences.Sturm
10:33:27Sturm_Sequences: theory Sturm_Sequences.Sturm_Ex
10:33:27Running SumSquares (on of3.proof.cit.tum.de) ...
10:33:27Running Sunflowers (on of3.proof.cit.tum.de) ...
10:33:27Running SuperCalc (on of3.proof.cit.tum.de) ...
10:33:27Timing Stuttering_Equivalence (8 threads, 1.937s elapsed time, 4.435s cpu time, 0.159s GC time, factor 2.29)
10:33:27Finished Stuttering_Equivalence (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.79)
10:33:27Sunflowers: theory HOL-Library.FuncSet
10:33:27Timing StrictOmegaCategories (8 threads, 4.130s elapsed time, 12.859s cpu time, 0.846s GC time, factor 3.11)
10:33:27Finished StrictOmegaCategories (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.74)
10:33:27Sturm_Tarski: theory Polynomial_Interpolation.Ring_Hom_Poly
10:33:27SuperCalc: theory SuperCalc.well_founded_continued
10:33:27SuperCalc: theory SuperCalc.multisets_continued
10:33:27SuperCalc: theory HOL-ex.Unification
10:33:27SumSquares: theory SumSquares.TwoSquares
10:33:27SumSquares: theory SumSquares.FourSquares
10:33:27Store_Buffer_Reduction: theory Store_Buffer_Reduction.PIMP
10:33:28Sunflowers: theory Sunflowers.Sunflower
10:33:28Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
10:33:28Building Suppes_Theorem (on 10.195.8.42) ...
10:33:28Building Symmetric_Polynomials (on 10.195.8.42) ...
10:33:28Sturm_Tarski: theory Sturm_Tarski.Pseudo_Remainder_Sequence
10:33:29Timing Strong_Security (8 threads, 5.510s elapsed time, 16.731s cpu time, 1.856s GC time, factor 3.04)
10:33:29Finished Strong_Security (0:00:06 elapsed time, 0:00:17 cpu time, factor 2.76)
10:33:29SuperCalc: theory SuperCalc.terms
10:33:29Suppes_Theorem: theory HOL-Combinatorics.Transposition
10:33:29Suppes_Theorem: theory HOL-Library.FuncSet
10:33:29Suppes_Theorem: theory HOL-Library.Cancellation
10:33:29Suppes_Theorem: theory HOL-Library.Nat_Bijection
10:33:29Store_Buffer_Reduction: theory Store_Buffer_Reduction.Abbrevs
10:33:29Sturm_Tarski: theory Sturm_Tarski.Tarski_Query_Impl
10:33:29Timing Sunflowers (8 threads, 1.439s elapsed time, 6.099s cpu time, 0.167s GC time, factor 4.24)
10:33:29Finished Sunflowers (0:00:02 elapsed time, 0:00:06 cpu time)
10:33:29Running Szemeredi_Regularity (on 10.195.8.29) ...
10:33:29Store_Buffer_Reduction: theory Store_Buffer_Reduction.Preliminaries
10:33:29Store_Buffer_Reduction: theory Store_Buffer_Reduction.Variants
10:33:30Suppes_Theorem: theory HOL-Library.Old_Datatype
10:33:30Suppes_Theorem: theory Propositional_Logic_Class.Implication_Logic
10:33:30Store_Buffer_Reduction: theory Store_Buffer_Reduction.Text
10:33:31Symmetric_Polynomials: theory HOL-Combinatorics.Transposition
10:33:31Symmetric_Polynomials: theory Polynomials.MPoly_Type
10:33:31Symmetric_Polynomials: theory Polynomials.More_Modules
10:33:31Symmetric_Polynomials: theory Abstract-Rewriting.Seq
10:33:31Suppes_Theorem: theory HOL-Library.Multiset
10:33:31SuperCalc: theory SuperCalc.equational_clausal_logic
10:33:31Suppes_Theorem: theory HOL-Library.Disjoint_Sets
10:33:31Symmetric_Polynomials: theory HOL-Combinatorics.Permutations
10:33:31Suppes_Theorem: theory HOL-Library.Countable
10:33:31Symmetric_Polynomials: theory Symmetric_Polynomials.Vieta
10:33:31Timing SumSquares (8 threads, 2.557s elapsed time, 8.496s cpu time, 0.242s GC time, factor 3.32)
10:33:31Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic
10:33:31Finished SumSquares (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.54)
10:33:32Timing Sturm_Tarski (8 threads, 5.469s elapsed time, 34.061s cpu time, 1.328s GC time, factor 6.23)
10:33:32Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic_Completeness
10:33:32Finished Sturm_Tarski (0:00:06 elapsed time, 0:00:35 cpu time, factor 5.35)
10:33:32Symmetric_Polynomials: theory Open_Induction.Restricted_Predicates
10:33:32Symmetric_Polynomials: theory Polynomials.More_MPoly_Type
10:33:32Symmetric_Polynomials: theory Regular-Sets.Regular_Set
10:33:32Running Szpilrajn (on 10.195.7.194) ...
10:33:32Running TLA (on 10.195.7.194) ...
10:33:32Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
10:33:33SuperCalc: theory SuperCalc.superposition
10:33:33Symmetric_Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
10:33:33Symmetric_Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
10:33:33Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Elements
10:33:33Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials
10:33:33Symmetric_Polynomials: theory Well_Quasi_Orders.Least_Enum
10:33:34Szpilrajn: theory Szpilrajn.Szpilrajn
10:33:34TLA: theory TLA.Intensional
10:33:34TLA: theory TLA.Sequence
10:33:34TLA: theory TLA.Semantics
10:33:35Timing Safe_Range_RC (4 threads, 78.098s elapsed time, 274.777s cpu time, 14.352s GC time, factor 3.52)
10:33:35Finished Safe_Range_RC (0:01:20 elapsed time, 0:04:38 cpu time, factor 3.44)
10:33:35TLA: theory TLA.PreFormulas
10:33:35TLA: theory TLA.Rules
10:33:35Running Tarskis_Geometry (on 10.195.8.40) ...
10:33:36TLA: theory TLA.Liveness
10:33:36TLA: theory TLA.State
10:33:36TLA: theory TLA.Buffer
10:33:36TLA: theory TLA.Even
10:33:36TLA: theory TLA.Inc
10:33:37Running Three_Circles (on 10.195.8.11) ...
10:33:37Symmetric_Polynomials: theory Regular-Sets.Regular_Exp
10:33:37Suppes_Theorem: theory HOL-Combinatorics.Permutations
10:33:38Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant
10:33:38Tarskis_Geometry: theory Tarskis_Geometry.Metric
10:33:38Tarskis_Geometry: theory HOL-Algebra.Congruence
10:33:38Timing Szpilrajn (4 threads, 3.653s elapsed time, 7.324s cpu time, 0.229s GC time, factor 2.00)
10:33:38Finished Szpilrajn (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.70)
10:33:38Tarskis_Geometry: theory Tarskis_Geometry.Miscellany
10:33:38Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2
10:33:38Tarskis_Geometry: theory Tarskis_Geometry.Tarski
10:33:39Suppes_Theorem: theory HOL-Combinatorics.List_Permutation
10:33:39Running Timed_Automata (on 10.195.8.49) ...
10:33:39Running Topological_Semantics (on 10.195.8.49) ...
10:33:39Suppes_Theorem: theory Propositional_Logic_Class.List_Utilities
10:33:39Tarskis_Geometry: theory HOL-Algebra.Order
10:33:39Three_Circles: theory Polynomial_Interpolation.Missing_Unsorted
10:33:39Timing Szemeredi_Regularity (4 threads, 5.949s elapsed time, 13.813s cpu time, 0.565s GC time, factor 2.32)
10:33:39Three_Circles: theory Sturm_Tarski.PolyMisc
10:33:39Finished Szemeredi_Regularity (0:00:08 elapsed time, 0:00:16 cpu time, factor 1.89)
10:33:39Three_Circles: theory Polynomial_Interpolation.Ring_Hom
10:33:39Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski
10:33:39Stern_Brocot: theory Stern_Brocot.Bird_Tree
10:33:39Three_Circles: theory Sturm_Tarski.Sturm_Tarski
10:33:39Suppes_Theorem: theory Propositional_Logic_Class.Classical_Connectives
10:33:40Timing Sturm_Sequences (8 threads, 9.742s elapsed time, 39.034s cpu time, 2.552s GC time, factor 4.01)
10:33:40Finished Sturm_Sequences (0:00:16 elapsed time, 0:00:51 cpu time, factor 3.13)
10:33:40Timed_Automata: theory Timed_Automata.Misc
10:33:40Timed_Automata: theory Timed_Automata.Floyd_Warshall
10:33:40Timed_Automata: theory Timed_Automata.Timed_Automata
10:33:40Topological_Semantics: theory Topological_Semantics.boolean_algebra
10:33:40Timing SuperCalc (8 threads, 10.924s elapsed time, 44.952s cpu time, 3.399s GC time, factor 4.11)
10:33:40Finished SuperCalc (0:00:12 elapsed time, 0:00:47 cpu time, factor 3.86)
10:33:40Symmetric_Polynomials: theory Regular-Sets.NDerivative
10:33:40Symmetric_Polynomials: theory Regular-Sets.Relation_Interpretation
10:33:40Timing Stirling_Formula (4 threads, 19.055s elapsed time, 55.014s cpu time, 4.021s GC time, factor 2.89)
10:33:40Finished Stirling_Formula (0:00:39 elapsed time, 0:01:28 cpu time, factor 2.25)
10:33:41Topological_Semantics: theory Topological_Semantics.boolean_algebra_operators
10:33:41Tarskis_Geometry: theory HOL-Algebra.Lattice
10:33:41Topological_Semantics: theory Topological_Semantics.logics_consequence
10:33:41Three_Circles: theory Budan_Fourier.BF_Misc
10:33:41Three_Circles: theory Polynomial_Interpolation.Missing_Polynomial
10:33:41Suppes_Theorem: theory Suppes_Theorem.Probability_Logic
10:33:41Timing Stern_Brocot (4 threads, 39.395s elapsed time, 79.299s cpu time, 6.991s GC time, factor 2.01)
10:33:41Finished Stern_Brocot (0:00:42 elapsed time, 0:01:23 cpu time, factor 1.96)
10:33:42Topological_Semantics: theory Topological_Semantics.boolean_algebra_infinitary
10:33:42Topological_Semantics: theory Topological_Semantics.conditions_positive
10:33:42Safe_OCL: theory Safe_OCL.OCL_Object_Model
10:33:42Topological_Semantics: theory Topological_Semantics.logics_quantifiers
10:33:42Topological_Semantics: theory Topological_Semantics.conditions_negative
10:33:42Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice
10:33:42Safe_OCL: theory Safe_OCL.OCL_Typing
10:33:42Topological_Semantics: theory Topological_Semantics.conditions_positive_infinitary
10:33:42Topological_Semantics: theory Topological_Semantics.conditions_relativized
10:33:42Topological_Semantics: theory Topological_Semantics.logics_operators
10:33:42Three_Circles: theory Budan_Fourier.Budan_Fourier
10:33:42Suppes_Theorem: theory Suppes_Theorem.Suppes_Theorem
10:33:43Topological_Semantics: theory Topological_Semantics.conditions_negative_infinitary
10:33:43Tarskis_Geometry: theory HOL-Algebra.Group
10:33:43Topological_Semantics: theory Topological_Semantics.logics_quantifiers_example
10:33:43Topological_Semantics: theory Topological_Semantics.conditions_relativized_infinitary
10:33:43Topological_Semantics: theory Topological_Semantics.logics_negation
10:33:44Topological_Semantics: theory Topological_Semantics.logics_LFI
10:33:44Topological_Semantics: theory Topological_Semantics.logics_LFU
10:33:44Three_Circles: theory Polynomial_Interpolation.Ring_Hom_Poly
10:33:45Timed_Automata: theory Timed_Automata.DBM
10:33:45Timed_Automata: theory Timed_Automata.Paths_Cycles
10:33:45Symmetric_Polynomials: theory Regular-Sets.Equivalence_Checking
10:33:46Symmetric_Polynomials: theory Regular-Sets.Regexp_Method
10:33:46Timed_Automata: theory Timed_Automata.Regions
10:33:46Tarskis_Geometry: theory Tarskis_Geometry.Action
10:33:46Tarskis_Geometry: theory Tarskis_Geometry.Projective
10:33:46Timing Statecharts (4 threads, 48.092s elapsed time, 151.915s cpu time, 5.983s GC time, factor 3.16)
10:33:46Finished Statecharts (0:00:49 elapsed time, 0:02:34 cpu time, factor 3.10)
10:33:47Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full
10:33:47Timing Standard_Borel_Spaces (4 threads, 48.942s elapsed time, 133.418s cpu time, 6.787s GC time, factor 2.73)
10:33:47Finished Standard_Borel_Spaces (0:00:51 elapsed time, 0:02:16 cpu time, factor 2.64)
10:33:47Three_Circles: theory Three_Circles.RRI_Misc
10:33:47Timing TLA (4 threads, 13.395s elapsed time, 37.775s cpu time, 2.245s GC time, factor 2.82)
10:33:47Finished TLA (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.66)
10:33:48Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
10:33:48Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
10:33:48Three_Circles: theory Three_Circles.Bernstein_01
10:33:49Three_Circles: theory Three_Circles.Normal_Poly
10:33:49Timing Subset_Boolean_Algebras (8 threads, 23.244s elapsed time, 49.352s cpu time, 3.051s GC time, factor 2.12)
10:33:49Finished Subset_Boolean_Algebras (0:00:24 elapsed time, 0:00:50 cpu time, factor 2.09)
10:33:49Symmetric_Polynomials: theory Polynomials.Utils
10:33:49Symmetric_Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
10:33:49Timed_Automata: theory Timed_Automata.DBM_Basics
10:33:49Three_Circles: theory Three_Circles.Bernstein
10:33:49Timed_Automata: theory Timed_Automata.Closure
10:33:49Three_Circles: theory Three_Circles.Three_Circles
10:33:50Symmetric_Polynomials: theory Polynomials.Power_Products
10:33:50Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski
10:33:50Timed_Automata: theory Timed_Automata.DBM_Normalization
10:33:50Timed_Automata: theory Timed_Automata.DBM_Operations
10:33:52Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
10:33:52Timed_Automata: theory Timed_Automata.Regions_Beta
10:33:54Running Special_Function_Bounds (on of1-proof) ...
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
10:33:55Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
10:33:56Timing Store_Buffer_Reduction (8 threads, 36.025s elapsed time, 168.626s cpu time, 18.095s GC time, factor 4.68)
10:33:56Finished Store_Buffer_Reduction (0:00:37 elapsed time, 0:02:53 cpu time, factor 4.61)
10:33:57Timed_Automata: theory Timed_Automata.Approx_Beta
10:33:59Timed_Automata: theory Timed_Automata.Normalized_Zone_Semantics
10:33:59Running Topology (on of2.proof.cit.tum.de) ...
10:33:59Running TortoiseHare (on of2.proof.cit.tum.de) ...
10:34:00Running Transformer_Semantics (on of2.proof.cit.tum.de) ...
10:34:00Topology: theory Topology.Topology
10:34:00Topology: theory Lazy-Lists-II.LList2
10:34:01TortoiseHare: theory TortoiseHare.Basis
10:34:01Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
10:34:01Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
10:34:01TortoiseHare: theory TortoiseHare.TortoiseHare
10:34:01TortoiseHare: theory TortoiseHare.Brent
10:34:01Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
10:34:01Timing Special_Function_Bounds (8 threads, 5.865s elapsed time, 23.513s cpu time, 0.881s GC time, factor 4.01)
10:34:01Finished Special_Function_Bounds (0:00:07 elapsed time, 0:00:25 cpu time, factor 3.50)
10:34:02Running Clique_and_Monotone_Circuits (on of4.proof.cit.tum.de) ...
10:34:02Running Irrationals_From_THEBOOK (on of4.proof.cit.tum.de) ...
10:34:02Running Transitive-Closure (on of4.proof.cit.tum.de) ...
10:34:02Topology: theory Topology.LList_Topology
10:34:02Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
10:34:03Transitive-Closure: theory Matrix.Utility
10:34:03Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
10:34:03Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
10:34:03Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Monotone_Formula
10:34:03Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Preliminaries
10:34:03Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
10:34:03Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
10:34:03Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
10:34:03Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
10:34:03Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
10:34:03Timing TortoiseHare (8 threads, 2.201s elapsed time, 5.491s cpu time, 0.184s GC time, factor 2.49)
10:34:03Finished TortoiseHare (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.95)
10:34:03Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
10:34:04Running Transitive-Closure-II (on of3.proof.cit.tum.de) ...
10:34:04Running Transport (on of3.proof.cit.tum.de) ...
10:34:04Running Treaps (on of3.proof.cit.tum.de) ...
10:34:04Timing Topology (8 threads, 2.633s elapsed time, 9.067s cpu time, 1.281s GC time, factor 3.44)
10:34:04Finished Topology (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.62)
10:34:04Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
10:34:04Clique_and_Monotone_Circuits: theory Sunflowers.Sunflower
10:34:04Clique_and_Monotone_Circuits: theory Sunflowers.Erdos_Rado_Sunflower
10:34:04Transitive-Closure-II: theory HOL-Library.While_Combinator
10:34:04Transitive-Closure-II: theory Regular-Sets.Regular_Set
10:34:04Clique_and_Monotone_Circuits: theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
10:34:04Timing Transformer_Semantics (8 threads, 3.053s elapsed time, 15.896s cpu time, 1.254s GC time, factor 5.21)
10:34:04Finished Transformer_Semantics (0:00:04 elapsed time, 0:00:17 cpu time, factor 4.02)
10:34:04Timing Irrationals_From_THEBOOK (8 threads, 1.223s elapsed time, 3.282s cpu time, 0.087s GC time, factor 2.68)
10:34:04Finished Irrationals_From_THEBOOK (0:00:02 elapsed time, 0:00:04 cpu time)
10:34:05Transport: theory ML_Unification.ML_Attribute_Utils
10:34:05Transport: theory ML_Unification.ML_Code_Utils
10:34:05Transport: theory ML_Unification.ML_Conversion_Utils
10:34:05Transport: theory ML_Unification.ML_General_Utils
10:34:05Transport: theory ML_Unification.ML_Normalisations
10:34:05Transport: theory ML_Unification.ML_Generic_Data_Utils
10:34:05Transport: theory ML_Unification.ML_Method_Utils
10:34:05Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class
10:34:05Transport: theory ML_Unification.ML_Theorem_Utils
10:34:05Transport: theory ML_Unification.Setup_Result_Commands
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Functions
10:34:05Transport: theory Transport.HOL_Mem_Of
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Lattices
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Relations
10:34:05Transport: theory Transport.Functions_Surjective
10:34:05Transport: theory Transport.Predicates_Lattice
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Groups
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Orders
10:34:05Timing Transitive-Closure (8 threads, 1.485s elapsed time, 4.590s cpu time, 0.216s GC time, factor 3.09)
10:34:05Treaps: theory HOL-Data_Structures.Less_False
10:34:05Treaps: theory HOL-Data_Structures.Cmp
10:34:05Treaps: theory HOL-Library.Function_Algebras
10:34:05Treaps: theory Landau_Symbols.Group_Sort
10:34:05Treaps: theory List-Index.List_Index
10:34:05Transport: theory Transport.Predicates_Order
10:34:05Transport: theory Transport.HOL_Basics_Base
10:34:05Transport: theory Transport.Binary_Relation_Functions
10:34:05Transport: theory Transport.Functions_Base
10:34:05Transport: theory Transport.HOL_Syntax_Bundles_Base
10:34:05Finished Transitive-Closure (0:00:02 elapsed time, 0:00:05 cpu time)
10:34:05Transport: theory Transport.HOL_Syntax_Bundles
10:34:05Treaps: theory HOL-Data_Structures.Sorted_Less
10:34:05Transport: theory ML_Unification.ML_Attributes
10:34:05Transport: theory ML_Unification.ML_Binders
10:34:05Transport: theory ML_Unification.ML_Term_Index
10:34:05Transport: theory ML_Unification.ML_Term_Utils
10:34:05Transport: theory Transport.Functions_Injective
10:34:05Treaps: theory HOL-Data_Structures.List_Ins_Del
10:34:05Transport: theory Transport.Predicates
10:34:05Transport: theory ML_Unification.ML_Logger
10:34:05Transport: theory ML_Unification.ML_Parsing_Utils
10:34:05Transport: theory Transport.Functions_Inverse
10:34:05Transport: theory ML_Unification.ML_Unification_Base
10:34:05Transport: theory ML_Unification.ML_Tactic_Utils
10:34:05Transport: theory Transport.Binary_Relations_Antisymmetric
10:34:05Transport: theory Transport.Binary_Relations_Irreflexive
10:34:05Transport: theory Transport.Binary_Relations_Left_Total
10:34:05Transport: theory Transport.Binary_Relations_Order_Base
10:34:05Transport: theory Transport.Function_Relators
10:34:05Transport: theory Transport.Binary_Relations_Lattice
10:34:05Transport: theory Transport.Binary_Relations_Surjective
10:34:05Treaps: theory HOL-Data_Structures.Set_Specs
10:34:05Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
10:34:05Transport: theory ML_Unification.Simps_To
10:34:05Treaps: theory HOL-Data_Structures.Tree_Set
10:34:05Transport: theory ML_Unification.ML_Functor_Instances
10:34:05Transport: theory ML_Unification.ML_Unification_Parsers
10:34:05Transport: theory ML_Unification.ML_Priorities
10:34:05Transport: theory Transport.Functions_Monotone
10:34:06Transport: theory ML_Unification.ML_Unifiers
10:34:06Treaps: theory Landau_Symbols.Landau_Real_Products
10:34:06Transport: theory Transport.Binary_Relations_Symmetric
10:34:06Transport: theory Transport.Binary_Relations_Reflexive
10:34:06Transport: theory Transport.Binary_Relations_Transitive
10:34:06Transport: theory Transport.Functions_Bijection
10:34:06Transport: theory Transport.Binary_Relations_Order
10:34:06Transport: theory Transport.Preorders
10:34:06Transport: theory Transport.Function_Properties
10:34:06Transport: theory Transport.LFunctions
10:34:06Transport: theory Transport.Partial_Orders
10:34:06Transport: theory Transport.Partial_Equivalence_Relations
10:34:06Transport: theory Transport.Equivalence_Relations
10:34:06Transport: theory Transport.Restricted_Equality
10:34:06Transport: theory Transport.Order_Functions_Base
10:34:06Transport: theory ML_Unification.Unify_Assumption_Tactic
10:34:06Transport: theory ML_Unification.ML_Unification_Hints
10:34:07Transitive-Closure-II: theory Regular-Sets.Regular_Exp
10:34:07Transport: theory ML_Unification.Unify_Resolve_Tactics
10:34:07Running Tree_Decomposition (on 10.195.8.29) ...
10:34:07Transport: theory Transport.Closure_Operators
10:34:07Transport: theory Transport.Order_Functors_Base
10:34:07Transport: theory Transport.Order_Functions
10:34:07Transport: theory Transport.Galois_Base
10:34:07Transport: theory Transport.Order_Equivalences
10:34:07Transport: theory Transport.Galois_Relator_Base
10:34:07Transport: theory Transport.Half_Galois_Property
10:34:07Transport: theory Transport.Order_Functors
10:34:07Transport: theory Transport.Orders
10:34:07Transport: theory ML_Unification.ML_Unification_HOL_Setup
10:34:08Transport: theory Transport.Binary_Relations_Injective
10:34:08Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
10:34:08Transport: theory Transport.Binary_Relations_Right_Unique
10:34:08Timing Tarskis_Geometry (4 threads, 28.607s elapsed time, 103.490s cpu time, 8.723s GC time, factor 3.62)
10:34:08Finished Tarskis_Geometry (0:00:31 elapsed time, 0:01:47 cpu time, factor 3.40)
10:34:08Transport: theory Transport.Binary_Relation_Properties
10:34:08Transport: theory Transport.LBinary_Relations
10:34:08Transport: theory Transport.HOL_Alignment_Binary_Relations
10:34:08Transport: theory Transport.Galois_Property
10:34:08Transport: theory Transport.Galois_Connections
10:34:08Transport: theory Transport.Galois_Relator
10:34:08Transport: theory Transport.Galois_Equivalences
10:34:08Transport: theory Transport.HOL_Alignment_Functions
10:34:08Transport: theory Transport.HOL_Alignment_Orders
10:34:08Transport: theory Transport.Galois
10:34:08Transport: theory Transport.Transport_Base
10:34:08Transport: theory Transport.Reflexive_Relator
10:34:08Transport: theory Transport.HOL_Basics
10:34:08Transport: theory Transport.HOL_Algebra_Alignment_Orders
10:34:08Transport: theory Transport.HOL_Alignments
10:34:08Transport: theory Transport.Monotone_Function_Relator
10:34:08Transport: theory Transport.HOL_Algebra_Alignment_Galois
10:34:08Tree_Decomposition: theory Tree_Decomposition.Graph
10:34:08Transport: theory Transport.Transport_Bijections
10:34:08Transport: theory Transport.Transport_Compositions_Agree_Base
10:34:08Transport: theory Transport.Transport_Functions_Base
10:34:08Transport: theory Transport.Transport_Compositions_Generic_Base
10:34:08Transport: theory Transport.Transport_Natural_Functors_Base
10:34:08Treaps: theory Landau_Symbols.Landau_Simprocs
10:34:08Running Triangle (on 10.195.6.179) ...
10:34:08Transport: theory Transport.Transport_Identity
10:34:08Transitive-Closure-II: theory Regular-Sets.NDerivative
10:34:08Transitive-Closure-II: theory Regular-Sets.Relation_Interpretation
10:34:09Treaps: theory Landau_Symbols.Landau_More
10:34:09Transport: theory Transport.Transport_Typedef_Base
10:34:09Transport: theory Transport.HOL_Algebra_Alignments
10:34:09Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
10:34:09Tree_Decomposition: theory Tree_Decomposition.Tree
10:34:09Transport: theory Transport.Transport_Compositions_Agree_Galois_Property
10:34:09Transport: theory Transport.Transport_Compositions_Agree_Galois_Relator
10:34:09Transport: theory Transport.Transport_Compositions_Agree_Monotone
10:34:09Running Trie (on 10.195.7.194) ...
10:34:10Transport: theory Transport.Transport_Compositions_Agree_Galois_Connection
10:34:10Transport: theory Transport.Transport_Compositions_Agree_Order_Equivalence
10:34:10Running Two_Generated_Word_Monoids_Intersection (on 10.195.7.194) ...
10:34:10Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
10:34:10Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
10:34:10Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
10:34:10Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
10:34:10Transitive-Closure-II: theory Regular-Sets.Equivalence_Checking
10:34:10Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
10:34:10Triangle: theory Triangle.Angles
10:34:11Transitive-Closure-II: theory Regular-Sets.Regexp_Method
10:34:11Running Tycon (on 10.195.8.46) ...
10:34:11Transport: theory Transport.Transport_Compositions_Agree_Galois_Equivalence
10:34:11Two_Generated_Word_Monoids_Intersection: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
10:34:11Treaps: theory Random_BSTs.Random_BSTs
10:34:11Transitive-Closure-II: theory Transitive-Closure-II.RTrancl
10:34:11Triangle: theory Triangle.Triangle
10:34:11Trie: theory Trie.Trie
10:34:12Transport: theory Transport.Transport_Compositions_Agree
10:34:12Tycon: theory Tycon.Coerce
10:34:12Tycon: theory Tycon.TypeApp
10:34:12Two_Generated_Word_Monoids_Intersection: theory Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection
10:34:12Timing Transitive-Closure-II (8 threads, 7.796s elapsed time, 14.424s cpu time, 1.726s GC time, factor 1.85)
10:34:12Finished Transitive-Closure-II (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.77)
10:34:13Tycon: theory Tycon.Functor
10:34:13Timing Crypto_Standards (4 threads, 1958.823s elapsed time, 7147.532s cpu time, 1100.432s GC time, factor 3.65)
10:34:13Finished Crypto_Standards (0:32:45 elapsed time, 1:59:24 cpu time, factor 3.65)
10:34:13Running UTP (on 10.195.8.30) ...
10:34:13Treaps: theory Treaps.Treap
10:34:13Treaps: theory Treaps.Probability_Misc
10:34:14Treaps: theory Treaps.Random_List_Permutation
10:34:14Timing Tree_Decomposition (4 threads, 5.283s elapsed time, 15.212s cpu time, 0.896s GC time, factor 2.88)
10:34:14Finished Tree_Decomposition (0:00:06 elapsed time, 0:00:16 cpu time, factor 2.46)
10:34:14Transport: theory Transport.Transport_Compositions_Generic_Galois_Property
10:34:14Transport: theory Transport.Transport_Compositions_Generic_Galois_Relator
10:34:14Transport: theory Transport.Transport_Compositions_Generic_Monotone
10:34:14Transport: theory Transport.Transport_Compositions_Generic_Order_Base
10:34:14Treaps: theory Treaps.Treap_Sort_and_BSTs
10:34:14Trie: theory Trie.Tries
10:34:14Transport: theory Transport.Transport_Compositions_Generic_Order_Equivalence
10:34:14Tycon: theory Tycon.Monad
10:34:14Tycon: theory Tycon.Binary_Tree_Monad
10:34:14Tycon: theory Tycon.Lift_Monad
10:34:15Tycon: theory Tycon.Monad_Zero
10:34:15Tycon: theory Tycon.Monad_Plus
10:34:15Running Undirected_Graph_Theory (on 10.195.8.40) ...
10:34:15Tycon: theory Tycon.Writer_Monad
10:34:15Transport: theory Transport.Transport_Compositions_Generic_Galois_Connection
10:34:15Timing Clique_and_Monotone_Circuits (8 threads, 11.960s elapsed time, 31.115s cpu time, 1.447s GC time, factor 2.60)
10:34:15Finished Clique_and_Monotone_Circuits (0:00:13 elapsed time, 0:00:32 cpu time, factor 2.46)
10:34:15Tycon: theory Tycon.Error_Monad
10:34:15Tycon: theory Tycon.Resumption_Transformer
10:34:15Tycon: theory Tycon.Monad_Zero_Plus
10:34:15Timing Triangle (4 threads, 4.398s elapsed time, 7.480s cpu time, 0.298s GC time, factor 1.70)
10:34:15Finished Triangle (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.45)
10:34:15Tycon: theory Tycon.Writer_Transformer
10:34:16Treaps: theory Treaps.Random_Treap
10:34:16UTP: theory UTP.utp_parser_utils
10:34:16Tycon: theory Tycon.Error_Transformer
10:34:16Tycon: theory Tycon.Lazy_List_Monad
10:34:16Transport: theory Transport.Transport_Natural_Functors_Galois
10:34:16Transport: theory Transport.Transport_Natural_Functors_Galois_Relator
10:34:16Transport: theory Transport.Transport_Natural_Functors_Order_Equivalence
10:34:16Transport: theory Transport.Transport_Natural_Functors_Order_Base
10:34:16UTP: theory UTP.utp_var
10:34:16Transport: theory Transport.Transport_Compositions_Generic_Galois_Equivalence
10:34:16Tycon: theory Tycon.Maybe_Monad
10:34:17Tycon: theory Tycon.State_Transformer
10:34:17Undirected_Graph_Theory: theory HOL-Combinatorics.Transposition
10:34:17Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Multiset_More
10:34:17Undirected_Graph_Theory: theory Girth_Chromatic.Girth_Chromatic_Misc
10:34:17Undirected_Graph_Theory: theory Card_Partitions.Set_Partition
10:34:17Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Basics
10:34:17UTP: theory UTP.utp_expr
10:34:17Transport: theory Transport.Transport_Compositions_Generic
10:34:17Transport: theory Transport.Transport_Functions_Monotone
10:34:17Transport: theory Transport.Transport_Functions_Order_Base
10:34:17Tycon: theory Tycon.Monad_Transformer
10:34:17Running Universal_Hash_Families (on 10.195.8.11) ...
10:34:17Undirected_Graph_Theory: theory HOL-Combinatorics.Permutations
10:34:18Transport: theory Transport.Transport_Compositions
10:34:18Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
10:34:18Undirected_Graph_Theory: theory Design_Theory.Multisets_Extras
10:34:19Timing Three_Circles (4 threads, 39.298s elapsed time, 135.162s cpu time, 11.471s GC time, factor 3.44)
10:34:19Finished Three_Circles (0:00:41 elapsed time, 0:02:17 cpu time, factor 3.31)
10:34:19Undirected_Graph_Theory: theory HOL-Combinatorics.Multiset_Permutations
10:34:19UTP: theory UTP.utp_expr_insts
10:34:19Timing Suppes_Theorem (4 threads, 37.108s elapsed time, 107.636s cpu time, 10.987s GC time, factor 2.90)
10:34:19Finished Suppes_Theorem (0:00:50 elapsed time, 0:02:07 cpu time, factor 2.53)
10:34:20Undirected_Graph_Theory: theory Design_Theory.Design_Basics
10:34:20UTP: theory UTP.utp_expr_funcs
10:34:20UTP: theory UTP.utp_unrest
10:34:20Universal_Hash_Families: theory HOL-Algebra.Congruence
10:34:20Universal_Hash_Families: theory HOL-Combinatorics.List_Permutation
10:34:20Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families
10:34:20Timing Tycon (4 threads, 7.379s elapsed time, 20.524s cpu time, 1.091s GC time, factor 2.78)
10:34:20Finished Tycon (0:00:08 elapsed time, 0:00:22 cpu time, factor 2.47)
10:34:20Transport: theory Transport.Transport_Functions_Galois_Property
10:34:21UTP: theory UTP.utp_usedby
10:34:21Transport: theory Transport.Transport_Natural_Functors
10:34:21UTP: theory UTP.utp_subst
10:34:21Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
10:34:21UTP: theory UTP.utp_tactics
10:34:21Universal_Hash_Families: theory HOL-Algebra.Order
10:34:22Timing Treaps (8 threads, 16.742s elapsed time, 57.744s cpu time, 3.967s GC time, factor 3.45)
10:34:22Finished Treaps (0:00:18 elapsed time, 0:00:59 cpu time, factor 3.27)
10:34:23Universal_Hash_Families: theory HOL-Algebra.Lattice
10:34:24Undirected_Graph_Theory: theory Design_Theory.Design_Operations
10:34:24Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Triangles
10:34:24Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Walks
10:34:24Universal_Hash_Families: theory HOL-Algebra.Complete_Lattice
10:34:24Transport: theory Transport.Transport_Functions_Galois_Connection
10:34:25Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_FMap
10:34:25Undirected_Graph_Theory: theory Undirected_Graph_Theory.Bipartite_Graphs
10:34:25Undirected_Graph_Theory: theory Undirected_Graph_Theory.Connectivity
10:34:25Undirected_Graph_Theory: theory Design_Theory.Block_Designs
10:34:25Universal_Hash_Families: theory HOL-Algebra.Group
10:34:26UTP: theory UTP.utp_meta_subst
10:34:26Undirected_Graph_Theory: theory Undirected_Graph_Theory.Girth_Independence
10:34:26UTP: theory UTP.utp_pred
10:34:27Transport: theory Transport.Transport_Functions_Galois_Equivalence
10:34:28Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials_Code
10:34:28Undirected_Graph_Theory: theory Design_Theory.BIBD
10:34:28Universal_Hash_Families: theory HOL-Algebra.Coset
10:34:29Universal_Hash_Families: theory HOL-Algebra.FiniteProduct
10:34:30Timing Trie (4 threads, 17.865s elapsed time, 21.564s cpu time, 0.962s GC time, factor 1.21)
10:34:30Finished Trie (0:00:19 elapsed time, 0:00:23 cpu time, factor 1.18)
10:34:30Undirected_Graph_Theory: theory Design_Theory.Resolvable_Designs
10:34:30Universal_Hash_Families: theory HOL-Algebra.Ring
10:34:31Timing Topological_Semantics (4 threads, 50.390s elapsed time, 82.532s cpu time, 6.406s GC time, factor 1.64)
10:34:31Finished Topological_Semantics (0:00:51 elapsed time, 0:01:24 cpu time, factor 1.62)
10:34:31Undirected_Graph_Theory: theory Design_Theory.Group_Divisible_Designs
10:34:31Transport: theory Transport.Transport_Functions_Order_Equivalence
10:34:31Transport: theory Transport.Transport_Functions_Relation_Simplifications
10:34:32Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
10:34:32Transport: theory Transport.Transport_Functions_Galois_Relator
10:34:32UTP: theory UTP.utp_alphabet
10:34:32UTP: theory UTP.utp_pred_laws
10:34:32Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Theory_Relations
10:34:33Universal_Hash_Families: theory HOL-Algebra.Divisibility
10:34:33Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
10:34:34UTP: theory UTP.utp_lift
10:34:34Timing Two_Generated_Word_Monoids_Intersection (4 threads, 22.634s elapsed time, 33.086s cpu time, 4.798s GC time, factor 1.46)
10:34:34Finished Two_Generated_Word_Monoids_Intersection (0:00:24 elapsed time, 0:00:34 cpu time, factor 1.44)
10:34:34Running Probability_Inequality_Completeness (on of1-proof) ...
10:34:34Running UpDown_Scheme (on of1-proof) ...
10:34:35UTP: theory UTP.utp_healthy
10:34:35UTP: theory UTP.utp_sequent
10:34:35Probability_Inequality_Completeness: theory Probability_Inequality_Completeness.Probability_Inequality_Completeness
10:34:35UpDown_Scheme: theory HOL-Eisbach.Eisbach
10:34:35UpDown_Scheme: theory HOL-ex.Quicksort
10:34:35UpDown_Scheme: theory HOL-Library.Adhoc_Overloading
10:34:35UpDown_Scheme: theory HOL-Library.Option_ord
10:34:35UpDown_Scheme: theory HOL-Imperative_HOL.Heap
10:34:35UpDown_Scheme: theory UpDown_Scheme.Grid_Point
10:34:35UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match
10:34:36UTP: theory UTP.utp_rel
10:34:36UpDown_Scheme: theory HOL-Library.Monad_Syntax
10:34:36Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graphs_Root
10:34:36UpDown_Scheme: theory Automatic_Refinement.Misc
10:34:36UpDown_Scheme: theory UpDown_Scheme.Grid
10:34:37Universal_Hash_Families: theory HOL-Algebra.AbelCoset
10:34:37Universal_Hash_Families: theory HOL-Algebra.Module
10:34:37UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad
10:34:37Timing Stable_Matching (4 threads, 103.386s elapsed time, 318.137s cpu time, 13.377s GC time, factor 3.08)
10:34:37Finished Stable_Matching (0:01:45 elapsed time, 0:05:21 cpu time, factor 3.04)
10:34:37UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
10:34:37UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
10:34:38Safe_OCL: theory Safe_OCL.OCL_Normalization
10:34:38Transport: theory Transport.Transport_Functions
10:34:38UpDown_Scheme: theory UpDown_Scheme.Down
10:34:38UpDown_Scheme: theory UpDown_Scheme.Up
10:34:38UpDown_Scheme: theory HOL-Imperative_HOL.Array
10:34:38UpDown_Scheme: theory UpDown_Scheme.Up_Down
10:34:39UpDown_Scheme: theory HOL-Imperative_HOL.Ref
10:34:39UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL
10:34:39UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
10:34:39UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run
10:34:40UTP: theory UTP.utp_recursion
10:34:40UTP: theory UTP.utp_state_parser
10:34:40UTP: theory UTP.utp_rel_laws
10:34:40UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions
10:34:41Running VYDRA_MDL (on of2.proof.cit.tum.de) ...
10:34:41Universal_Hash_Families: theory HOL-Algebra.Ideal
10:34:41Running Valuation (on of2.proof.cit.tum.de) ...
10:34:41Running Van_der_Waerden (on of2.proof.cit.tum.de) ...
10:34:41Van_der_Waerden: theory HOL-Library.FuncSet
10:34:41Van_der_Waerden: theory Van_der_Waerden.Digits
10:34:41Valuation: theory Valuation.Valuation1
10:34:41Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
10:34:41VYDRA_MDL: theory VYDRA_MDL.NFA
10:34:41VYDRA_MDL: theory VYDRA_MDL.Timestamp
10:34:41UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple
10:34:42UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation
10:34:43Running VectorSpace (on of4.proof.cit.tum.de) ...
10:34:43Running VeriComp (on of4.proof.cit.tum.de) ...
10:34:43Running Verified-Prover (on of4.proof.cit.tum.de) ...
10:34:43Verified-Prover: theory Verified-Prover.Prover
10:34:43VeriComp: theory VeriComp.Behaviour
10:34:43VeriComp: theory VeriComp.Transfer_Extras
10:34:43VeriComp: theory VeriComp.Well_founded
10:34:43UTP: theory UTP.utp_theory
10:34:43UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main
10:34:43UpDown_Scheme: theory UpDown_Scheme.Imperative
10:34:44VeriComp: theory VeriComp.Inf
10:34:44VeriComp: theory VeriComp.Lifting_Simulation_To_Bisimulation
10:34:44Running VerifyThis2019 (on of3.proof.cit.tum.de) ...
10:34:44Running VolpanoSmith (on of3.proof.cit.tum.de) ...
10:34:44VYDRA_MDL: theory VYDRA_MDL.Interval
10:34:44VectorSpace: theory VectorSpace.RingModuleFacts
10:34:44VYDRA_MDL: theory VYDRA_MDL.Timestamp_Lex
10:34:44VectorSpace: theory VectorSpace.FunctionLemmas
10:34:44VeriComp: theory VeriComp.Semantics
10:34:44Valuation: theory Valuation.Valuation2
10:34:44VeriComp: theory VeriComp.Language
10:34:44VeriComp: theory VeriComp.Simulation
10:34:44VYDRA_MDL: theory VYDRA_MDL.Timestamp_Prod
10:34:44VolpanoSmith: theory VolpanoSmith.Semantics
10:34:44Universal_Hash_Families: theory HOL-Algebra.RingHom
10:34:44VYDRA_MDL: theory VYDRA_MDL.Trace
10:34:44VYDRA_MDL: theory VYDRA_MDL.Window
10:34:44VYDRA_MDL: theory VYDRA_MDL.Metric_Point_Structure
10:34:44VeriComp: theory VeriComp.Compiler
10:34:44VectorSpace: theory VectorSpace.MonoidSums
10:34:45VerifyThis2019: theory VerifyThis2019.Exc_Nres_Monad
10:34:45VYDRA_MDL: theory VYDRA_MDL.MDL
10:34:45Transport: theory Transport.Transport
10:34:45Transport: theory Transport.Transport_Partial_Quotient_Types
10:34:45Transport: theory Transport.Transport_Rel_If
10:34:45VeriComp: theory VeriComp.Fixpoint
10:34:45Transport: theory Transport.Transport_Syntax
10:34:45VectorSpace: theory VectorSpace.LinearCombinations
10:34:45Transport: theory Transport.Transport_Prototype
10:34:45Universal_Hash_Families: theory HOL-Algebra.QuotRing
10:34:45VerifyThis2019: theory VerifyThis2019.VTcomp
10:34:45Universal_Hash_Families: theory HOL-Algebra.UnivPoly
10:34:45Timing VeriComp (8 threads, 1.841s elapsed time, 6.395s cpu time, 0.769s GC time, factor 3.47)
10:34:45Finished VeriComp (0:00:02 elapsed time, 0:00:07 cpu time)
10:34:45VolpanoSmith: theory VolpanoSmith.secTypes
10:34:45Valuation: theory Valuation.Valuation3
10:34:45VerifyThis2019: theory VerifyThis2019.Parallel_Multiset_Fold
10:34:45VerifyThis2019: theory VerifyThis2019.Challenge1A
10:34:45VerifyThis2019: theory VerifyThis2019.Challenge2A
10:34:45Timing Van_der_Waerden (8 threads, 3.775s elapsed time, 9.907s cpu time, 0.283s GC time, factor 2.62)
10:34:45Finished Van_der_Waerden (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.28)
10:34:45Transport: theory Transport.Transport_Dep_Fun_Rel_Examples
10:34:45Transport: theory Transport.Transport_Lists_Sets_Examples
10:34:45Transport: theory Transport.Transport_Typedef
10:34:45Timing UpDown_Scheme (8 threads, 9.304s elapsed time, 61.860s cpu time, 5.311s GC time, factor 6.65)
10:34:45Finished UpDown_Scheme (0:00:10 elapsed time, 0:01:03 cpu time, factor 5.99)
10:34:46VolpanoSmith: theory VolpanoSmith.Execute
10:34:46Timing Verified-Prover (8 threads, 2.727s elapsed time, 7.394s cpu time, 0.304s GC time, factor 2.71)
10:34:46Finished Verified-Prover (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.34)
10:34:46VerifyThis2019: theory VerifyThis2019.Challenge3
10:34:46Running WHATandWHERE_Security (on 10.195.8.42) ...
10:34:46VectorSpace: theory VectorSpace.SumSpaces
10:34:46VerifyThis2019: theory VerifyThis2019.Challenge1B
10:34:46VectorSpace: theory VectorSpace.VectorSpace
10:34:46Timing Probability_Inequality_Completeness (8 threads, 10.680s elapsed time, 49.517s cpu time, 3.470s GC time, factor 4.64)
10:34:46Finished Probability_Inequality_Completeness (0:00:11 elapsed time, 0:00:51 cpu time, factor 4.39)
10:34:47Transport: theory Transport.Transport_Via_Partial_Galois_Connections_Equivalences_Paper
10:34:47UTP: theory UTP.utp_hoare
10:34:47Running WOOT_Strong_Eventual_Consistency (on 10.195.8.29) ...
10:34:47Timing VolpanoSmith (8 threads, 3.248s elapsed time, 8.519s cpu time, 0.815s GC time, factor 2.62)
10:34:47Finished VolpanoSmith (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.30)
10:34:47WHATandWHERE_Security: theory Strong_Security.Types
10:34:47WHATandWHERE_Security: theory WHATandWHERE_Security.WHATWHERE_Security
10:34:47WHATandWHERE_Security: theory WHATandWHERE_Security.MWLs
10:34:47WHATandWHERE_Security: theory Strong_Security.Expr
10:34:48WHATandWHERE_Security: theory WHATandWHERE_Security.Up_To_Technique
10:34:48Universal_Hash_Families: theory HOL-Algebra.IntRing
10:34:48WOOT_Strong_Eventual_Consistency: theory HOL-Library.Adhoc_Overloading
10:34:48WOOT_Strong_Eventual_Consistency: theory Deriving.Derive_Manager
10:34:48WOOT_Strong_Eventual_Consistency: theory HOL-Library.List_Lexorder
10:34:48WOOT_Strong_Eventual_Consistency: theory HOL-Eisbach.Eisbach
10:34:48WOOT_Strong_Eventual_Consistency: theory Datatype_Order_Generator.Derive_Aux
10:34:48Running WebAssembly (on 10.195.6.179) ...
10:34:48WOOT_Strong_Eventual_Consistency: theory Certification_Monads.Error_Syntax
10:34:48UTP: theory UTP.utp_concurrency
10:34:48WOOT_Strong_Eventual_Consistency: theory HOL-Library.Monad_Syntax
10:34:48UTP: theory UTP.utp_rel_opsem
10:34:48WOOT_Strong_Eventual_Consistency: theory HOL-Library.Product_Lexorder
10:34:49UTP: theory UTP.utp_wp
10:34:49WOOT_Strong_Eventual_Consistency: theory Certification_Monads.Error_Monad
10:34:49WOOT_Strong_Eventual_Consistency: theory Datatype_Order_Generator.Order_Generator
10:34:49WHATandWHERE_Security: theory Strong_Security.Domain_example
10:34:49Timing Transport (8 threads, 43.356s elapsed time, 143.347s cpu time, 11.994s GC time, factor 3.31)
10:34:49WOOT_Strong_Eventual_Consistency: theory HOL-Library.Sublist
10:34:49Finished Transport (0:00:44 elapsed time, 0:02:25 cpu time, factor 3.24)
10:34:49UTP: theory UTP.utp_sym_eval
10:34:49UTP: theory UTP.utp_dynlog
10:34:49UTP: theory UTP.utp_sp
10:34:49WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.Data
10:34:49Running Weight_Balanced_Trees (on 10.195.7.194) ...
10:34:50Running Weighted_Arithmetic_Geometric_Mean (on 10.195.7.194) ...
10:34:50WebAssembly: theory Word_Lib.Legacy_Aliases
10:34:50WebAssembly: theory Word_Lib.Bit_Comprehension
10:34:50WebAssembly: theory Word_Lib.More_Divides
10:34:50WebAssembly: theory Word_Lib.Signed_Division_Word
10:34:50WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.ErrorMonad
10:34:51WebAssembly: theory Native_Word.Code_Int_Integer_Conversion
10:34:51WebAssembly: theory WebAssembly.Wasm_Type_Abs
10:34:51WebAssembly: theory Word_Lib.Even_More_List
10:34:51Weighted_Arithmetic_Geometric_Mean: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
10:34:51Weight_Balanced_Trees: theory HOL-Data_Structures.Cmp
10:34:51Building Weighted_Path_Order (on 10.195.8.46) ...
10:34:51Weight_Balanced_Trees: theory HOL-Data_Structures.Less_False
10:34:51Weight_Balanced_Trees: theory HOL-Library.Tree
10:34:51WebAssembly: theory Word_Lib.More_Arithmetic
10:34:51VerifyThis2019: theory VerifyThis2019.Challenge2B
10:34:51VYDRA_MDL: theory VYDRA_MDL.Preliminaries
10:34:51VYDRA_MDL: theory VYDRA_MDL.Temporal
10:34:51Weight_Balanced_Trees: theory HOL-Data_Structures.Sorted_Less
10:34:51WebAssembly: theory Word_Lib.More_Bit_Ring
10:34:51Weight_Balanced_Trees: theory HOL-Data_Structures.List_Ins_Del
10:34:51WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.Sorting
10:34:52Weight_Balanced_Trees: theory HOL-Data_Structures.Set_Specs
10:34:52UTP: theory UTP.utp
10:34:52Running Well_Quasi_Orders (on 10.195.8.30) ...
10:34:52WebAssembly: theory Word_Lib.More_Word
10:34:52Timing VerifyThis2019 (8 threads, 7.771s elapsed time, 17.288s cpu time, 1.269s GC time, factor 2.22)
10:34:52Finished VerifyThis2019 (0:00:09 elapsed time, 0:00:18 cpu time, factor 2.04)
10:34:53Timing Weighted_Arithmetic_Geometric_Mean (4 threads, 1.393s elapsed time, 2.957s cpu time, 0.076s GC time, factor 2.12)
10:34:53Finished Weighted_Arithmetic_Geometric_Mean (0:00:02 elapsed time, 0:00:04 cpu time)
10:34:53WHATandWHERE_Security: theory WHATandWHERE_Security.Parallel_Composition
10:34:53Weighted_Path_Order: theory Weighted_Path_Order.Status
10:34:53Weighted_Path_Order: theory Weighted_Path_Order.List_Order
10:34:53UTP: theory UTP.utp_expr_ovld
10:34:53Weighted_Path_Order: theory Weighted_Path_Order.Relations
10:34:53UTP: theory UTP.utp_simple_time
10:34:53WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.BasicAlgorithms
10:34:53Weighted_Path_Order: theory Weighted_Path_Order.Precedence
10:34:53WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.SortKeys
10:34:53VYDRA_MDL: theory VYDRA_MDL.Monitor
10:34:53WHATandWHERE_Security: theory WHATandWHERE_Security.WHATWHERE_Secure_Skip_Assign
10:34:53WHATandWHERE_Security: theory WHATandWHERE_Security.Language_Composition
10:34:54Running Winding_Number_Eval (on 10.195.8.40) ...
10:34:54UTP: theory UTP.utp_full
10:34:54WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.CreateAlgorithms
10:34:54WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.IntegrateAlgorithm
10:34:54UTP: theory UTP.utp_easy_parser
10:34:54WHATandWHERE_Security: theory WHATandWHERE_Security.Type_System
10:34:54Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair
10:34:54Timing VectorSpace (8 threads, 10.335s elapsed time, 28.957s cpu time, 2.281s GC time, factor 2.80)
10:34:54Finished VectorSpace (0:00:11 elapsed time, 0:00:30 cpu time, factor 2.61)
10:34:54Well_Quasi_Orders: theory Abstract-Rewriting.Seq
10:34:54Well_Quasi_Orders: theory Open_Induction.Restricted_Predicates
10:34:54Well_Quasi_Orders: theory Regular-Sets.Regular_Set
10:34:54Well_Quasi_Orders: theory Well_Quasi_Orders.Infinite_Sequences
10:34:54WebAssembly: theory Native_Word.Code_Target_Word_Base
10:34:54Weight_Balanced_Trees: theory HOL-Data_Structures.Tree2
10:34:54UTP: theory UTP.sum_list
10:34:54WebAssembly: theory Word_Lib.Bit_Shifts_Infix_Syntax
10:34:54Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees_log
10:34:54WebAssembly: theory Word_Lib.Least_significant_bit
10:34:55WHATandWHERE_Security: theory WHATandWHERE_Security.Type_System_example
10:34:55Well_Quasi_Orders: theory Well_Quasi_Orders.Least_Enum
10:34:55Timing Valuation (8 threads, 12.862s elapsed time, 63.441s cpu time, 6.578s GC time, factor 4.93)
10:34:55Finished Valuation (0:00:14 elapsed time, 0:01:04 cpu time, factor 4.62)
10:34:55Weight_Balanced_Trees: theory HOL-Data_Structures.Isin2
10:34:55Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2
10:34:55Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair_Impl
10:34:55WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.DistributedExecution
10:34:55WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.Psi
10:34:55Well_Quasi_Orders: theory Open_Induction.Open_Induction
10:34:55Well_Quasi_Orders: theory Well_Quasi_Orders.Multiset_Extension
10:34:55Running WorkerWrapper (on 10.195.8.11) ...
10:34:55Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Elements
10:34:56Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees
10:34:56Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field
10:34:56Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring
10:34:56Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
10:34:56Winding_Number_Eval: theory HOL-Eisbach.Eisbach
10:34:56WebAssembly: theory Word_Lib.Aligned
10:34:56WebAssembly: theory Word_Lib.Singleton_Bit_Shifts
10:34:56WebAssembly: theory Word_Lib.Most_significant_bit
10:34:57WorkerWrapper: theory WorkerWrapper.Maybe
10:34:57Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
10:34:57WorkerWrapper: theory WorkerWrapper.Nats
10:34:57WebAssembly: theory Word_Lib.Generic_set_bit
10:34:57Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
10:34:57Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
10:34:58Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
10:34:58Running XML (on 10.195.8.49) ...
10:34:58WebAssembly: theory Native_Word.Code_Target_Integer_Bit
10:34:58WebAssembly: theory Native_Word.Word_Type_Copies
10:34:58VYDRA_MDL: theory VYDRA_MDL.Monitor_Code
10:34:58WebAssembly: theory Word_Lib.Bits_Int
10:34:58Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2_Impl
10:34:58WorkerWrapper: theory WorkerWrapper.LList
10:34:58Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
10:34:58WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.Consistency
10:34:59Well_Quasi_Orders: theory Regular-Sets.Regular_Exp
10:34:59WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.CreateConsistent
10:34:59Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
10:34:59WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.IntegrateInsertCommute
10:34:59XML: theory Deriving.Generator_Aux
10:34:59XML: theory Certification_Monads.Error_Syntax
10:34:59XML: theory Deriving.Derive_Manager
10:34:59XML: theory Partial_Function_MR.Partial_Function_MR
10:35:00XML: theory Certification_Monads.Error_Monad
10:35:00XML: theory Certification_Monads.Strict_Sum
10:35:00XML: theory Show.Show
10:35:00WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
10:35:00WorkerWrapper: theory WorkerWrapper.WorkerWrapper
10:35:00WorkerWrapper: theory WorkerWrapper.CounterExample
10:35:00WorkerWrapper: theory WorkerWrapper.Last
10:35:00WorkerWrapper: theory WorkerWrapper.Streams
10:35:02Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
10:35:02WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
10:35:02WorkerWrapper: theory WorkerWrapper.Accumulator
10:35:02WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.StrongConvergence
10:35:02WorkerWrapper: theory WorkerWrapper.Backtracking
10:35:02Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
10:35:02WorkerWrapper: theory WorkerWrapper.Continuations
10:35:02WorkerWrapper: theory WorkerWrapper.Nub
10:35:02XML: theory Certification_Monads.Parser_Monad
10:35:03WorkerWrapper: theory WorkerWrapper.UnboxedNats
10:35:03WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.SEC
10:35:03WOOT_Strong_Eventual_Consistency: theory WOOT_Strong_Eventual_Consistency.Example
10:35:03WebAssembly: theory Word_Lib.Typedef_Morphisms
10:35:03Winding_Number_Eval: theory Budan_Fourier.BF_Misc
10:35:04WebAssembly: theory Word_Lib.Reversed_Bit_Lists
10:35:04Timing Symmetric_Polynomials (4 threads, 68.286s elapsed time, 189.398s cpu time, 16.750s GC time, factor 2.77)
10:35:04Finished Symmetric_Polynomials (0:01:33 elapsed time, 0:03:48 cpu time, factor 2.44)
10:35:04XML: theory XML.Xml
10:35:05Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
10:35:05Well_Quasi_Orders: theory Regular-Sets.NDerivative
10:35:05Well_Quasi_Orders: theory Regular-Sets.Relation_Interpretation
10:35:05Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
10:35:05Universal_Hash_Families: theory HOL-Algebra.Subrings
10:35:06Weighted_Path_Order: theory Weighted_Path_Order.WPO
10:35:06Timing UTP (4 threads, 48.133s elapsed time, 152.707s cpu time, 11.110s GC time, factor 3.17)
10:35:06Finished UTP (0:00:51 elapsed time, 0:02:36 cpu time, factor 3.06)
10:35:06Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
10:35:06Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
10:35:07Timing WorkerWrapper (4 threads, 8.997s elapsed time, 23.156s cpu time, 1.116s GC time, factor 2.57)
10:35:07Finished WorkerWrapper (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.36)
10:35:09XML: theory XML.Xmlt
10:35:09Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
10:35:10Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
10:35:10Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
10:35:10Weighted_Path_Order: theory Weighted_Path_Order.KBO_Transformation
10:35:10Weighted_Path_Order: theory Weighted_Path_Order.LPO
10:35:10Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
10:35:11Weighted_Path_Order: theory Weighted_Path_Order.KBO_as_WPO
10:35:11Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
10:35:11WebAssembly: theory Native_Word.Uint8
10:35:11Safe_OCL: theory Safe_OCL.OCL_Examples
10:35:11Weighted_Path_Order: theory Weighted_Path_Order.RPO
10:35:12Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
10:35:13WebAssembly: theory WebAssembly.Wasm_Ast
10:35:13Weighted_Path_Order: theory Weighted_Path_Order.Executable_Orders
10:35:13Timing Undirected_Graph_Theory (4 threads, 54.440s elapsed time, 182.323s cpu time, 16.810s GC time, factor 3.35)
10:35:13Finished Undirected_Graph_Theory (0:00:56 elapsed time, 0:03:05 cpu time, factor 3.27)
10:35:13Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
10:35:13Timing Weight_Balanced_Trees (4 threads, 21.046s elapsed time, 49.197s cpu time, 6.752s GC time, factor 2.34)
10:35:13Finished Weight_Balanced_Trees (0:00:22 elapsed time, 0:00:51 cpu time, factor 2.27)
10:35:13Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
10:35:13Running Power_Sum_Polynomials (on of1-proof) ...
10:35:13Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
10:35:13Running Zeta_3_Irrational (on of1-proof) ...
10:35:14Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
10:35:14Timing VYDRA_MDL (8 threads, 31.706s elapsed time, 148.420s cpu time, 11.072s GC time, factor 4.68)
10:35:14Finished VYDRA_MDL (0:00:33 elapsed time, 0:02:31 cpu time, factor 4.54)
10:35:14Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
10:35:14Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
10:35:14Power_Sum_Polynomials: theory Matrix.Utility
10:35:14Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Unsorted
10:35:14Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom
10:35:14Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
10:35:15Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
10:35:15Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
10:35:15Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
10:35:15Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
10:35:15Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
10:35:15Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_List
10:35:15Timing WHATandWHERE_Security (4 threads, 27.229s elapsed time, 93.314s cpu time, 9.691s GC time, factor 3.43)
10:35:15Finished WHATandWHERE_Security (0:00:28 elapsed time, 0:01:35 cpu time, factor 3.30)
10:35:15Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Polynomial
10:35:15Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
10:35:15Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
10:35:15Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
10:35:16Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
10:35:16Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
10:35:16Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
10:35:16Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Polynomial_Factorial
10:35:16Power_Sum_Polynomials: theory Polynomial_Factorization.Order_Polynomial
10:35:16Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Multiset
10:35:16Power_Sum_Polynomials: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
10:35:17Power_Sum_Polynomials: theory Polynomial_Factorization.Prime_Factorization
10:35:17Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
10:35:17Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
10:35:17Skipping theories "Test/Test_Datatypes" (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
10:35:17Timing CakeML_Codegen (4 threads, 2347.677s elapsed time, 3356.373s cpu time, 301.565s GC time, factor 1.43)
10:35:17Finished CakeML_Codegen (0:39:12 elapsed time, 0:56:06 cpu time, factor 1.43)
10:35:17Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials
10:35:17Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom_Poly
10:35:18Universal_Hash_Families: theory HOL-Algebra.Polynomials
10:35:18Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
10:35:19Building Abstract_Completeness (on of2.proof.cit.tum.de) ...
10:35:19Running Ackermanns_not_PR (on of2.proof.cit.tum.de) ...
10:35:19Power_Sum_Polynomials: theory Polynomial_Factorization.Gauss_Lemma
10:35:20Ackermanns_not_PR: theory Ackermanns_not_PR.Primrec
10:35:20Power_Sum_Polynomials: theory Polynomial_Factorization.Rational_Root_Test
10:35:20Abstract_Completeness: theory Collections.ICF_Tools
10:35:20Abstract_Completeness: theory Collections.Ord_Code_Preproc
10:35:20Abstract_Completeness: theory Collections.Locale_Code
10:35:20Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Puzzle
10:35:21Abstract_Completeness: theory Abstract_Completeness.Abstract_Completeness
10:35:21Timing Ackermanns_not_PR (8 threads, 0.610s elapsed time, 1.471s cpu time, 0.043s GC time, factor 2.41)
10:35:21Finished Ackermanns_not_PR (0:00:01 elapsed time)
10:35:21Running AnselmGod (on of4.proof.cit.tum.de) ...
10:35:21Running Aristotles_Assertoric_Syllogistic (on of4.proof.cit.tum.de) ...
10:35:21Running Arith_Prog_Rel_Primes (on of4.proof.cit.tum.de) ...
10:35:21Abstract_Completeness: theory Abstract_Completeness.Propositional_Logic
10:35:22AnselmGod: theory AnselmGod.AnselmGod
10:35:22Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
10:35:22Running Attack_Trees (on of3.proof.cit.tum.de) ...
10:35:22Running Banach_Steinhaus (on of3.proof.cit.tum.de) ...
10:35:22Running Birkhoff_Finite_Distributive_Lattices (on of3.proof.cit.tum.de) ...
10:35:22Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
10:35:22Timing Well_Quasi_Orders (4 threads, 26.725s elapsed time, 81.699s cpu time, 8.521s GC time, factor 3.06)
10:35:22Finished Well_Quasi_Orders (0:00:29 elapsed time, 0:01:25 cpu time, factor 2.89)
10:35:22Timing Aristotles_Assertoric_Syllogistic (8 threads, 0.204s elapsed time, 0.565s cpu time, 0.021s GC time, factor 2.77)
10:35:22Finished Aristotles_Assertoric_Syllogistic (0:00:01 elapsed time)
10:35:22Timing XML (4 threads, 21.568s elapsed time, 44.472s cpu time, 5.855s GC time, factor 2.06)
10:35:22Finished XML (0:00:23 elapsed time, 0:00:47 cpu time, factor 1.99)
10:35:22Attack_Trees: theory Attack_Trees.MC
10:35:22Timing AnselmGod (8 threads, 0.538s elapsed time, 1.294s cpu time, 0.070s GC time, factor 2.41)
10:35:22Finished AnselmGod (0:00:01 elapsed time)
10:35:22Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Plus
10:35:23Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Order
10:35:23Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Finite_Lattice
10:35:23Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
10:35:23Attack_Trees: theory Attack_Trees.AT
10:35:23Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
10:35:23Timing Zeta_3_Irrational (8 threads, 8.240s elapsed time, 55.230s cpu time, 1.920s GC time, factor 6.70)
10:35:23Finished Zeta_3_Irrational (0:00:09 elapsed time, 0:00:56 cpu time, factor 5.85)
10:35:24Timing WOOT_Strong_Eventual_Consistency (4 threads, 34.756s elapsed time, 116.954s cpu time, 7.639s GC time, factor 3.37)
10:35:24Finished WOOT_Strong_Eventual_Consistency (0:00:36 elapsed time, 0:01:59 cpu time, factor 3.27)
10:35:24Attack_Trees: theory Attack_Trees.Infrastructure
10:35:25Birkhoff_Finite_Distributive_Lattices: theory Birkhoff_Finite_Distributive_Lattices.Birkhoff_Finite_Distributive_Lattices
10:35:25Timing Banach_Steinhaus (8 threads, 1.818s elapsed time, 9.266s cpu time, 0.335s GC time, factor 5.10)
10:35:25Finished Banach_Steinhaus (0:00:03 elapsed time, 0:00:10 cpu time, factor 3.41)
10:35:25Timing Arith_Prog_Rel_Primes (8 threads, 2.542s elapsed time, 4.365s cpu time, 0.167s GC time, factor 1.72)
10:35:25Finished Arith_Prog_Rel_Primes (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.45)
10:35:25Running Blue_Eyes (on 10.195.8.42) ...
10:35:25Attack_Trees: theory Attack_Trees.GDPRhealthcare
10:35:26Timing Attack_Trees (8 threads, 3.579s elapsed time, 10.259s cpu time, 1.055s GC time, factor 2.87)
10:35:26Finished Attack_Trees (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.48)
10:35:27Blue_Eyes: theory Blue_Eyes.Blue_Eyes
10:35:27Running Boolos_Curious_Inference (on 10.195.6.179) ...
10:35:28Timing Birkhoff_Finite_Distributive_Lattices (8 threads, 5.047s elapsed time, 9.017s cpu time, 0.838s GC time, factor 1.79)
10:35:28Finished Birkhoff_Finite_Distributive_Lattices (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.65)
10:35:29Running Buffons_Needle (on 10.195.7.194) ...
10:35:29Running C2KA_DistributedSystems (on 10.195.7.194) ...
10:35:29Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo1
10:35:29Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo2
10:35:29Timing Blue_Eyes (4 threads, 1.936s elapsed time, 3.569s cpu time, 0.195s GC time, factor 1.84)
10:35:29Finished Blue_Eyes (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.41)
10:35:30Timing Boolos_Curious_Inference (4 threads, 0.656s elapsed time, 1.472s cpu time, 0.069s GC time, factor 2.24)
10:35:30Finished Boolos_Curious_Inference (0:00:02 elapsed time)
10:35:30C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
10:35:30Timing Power_Sum_Polynomials (8 threads, 14.705s elapsed time, 62.057s cpu time, 4.456s GC time, factor 4.22)
10:35:30Finished Power_Sum_Polynomials (0:00:16 elapsed time, 0:01:04 cpu time, factor 3.99)
10:35:31C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
10:35:31Timing Abstract_Completeness (8 threads, 3.399s elapsed time, 8.189s cpu time, 0.676s GC time, factor 2.41)
10:35:31Finished Abstract_Completeness (0:00:10 elapsed time, 0:00:22 cpu time, factor 2.11)
10:35:31Running CYK (on 10.195.8.30) ...
10:35:32Buffons_Needle: theory Buffons_Needle.Buffons_Needle
10:35:33Running Card_Multisets (on 10.195.8.40) ...
10:35:33CYK: theory CYK.CYK
10:35:33C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
10:35:33C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
10:35:34C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
10:35:34Card_Multisets: theory HOL-Library.Cancellation
10:35:34WebAssembly: theory WebAssembly.Wasm_Base_Defs
10:35:34Running Cartan_FP (on 10.195.8.11) ...
10:35:35Timing C2KA_DistributedSystems (4 threads, 3.933s elapsed time, 5.495s cpu time, 0.232s GC time, factor 1.40)
10:35:35Finished C2KA_DistributedSystems (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.25)
10:35:35Card_Multisets: theory HOL-Library.Multiset
10:35:36Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
10:35:36WebAssembly: theory WebAssembly.Wasm
10:35:37Cartan_FP: theory Cartan_FP.Cartan
10:35:37Running Case_Labeling (on 10.195.8.49) ...
10:35:37Timing Buffons_Needle (4 threads, 4.749s elapsed time, 13.313s cpu time, 0.300s GC time, factor 2.80)
10:35:37Finished Buffons_Needle (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.15)
10:35:38Case_Labeling: theory HOL-Hoare.Arith2
10:35:38Case_Labeling: theory Case_Labeling.Case_Labeling
10:35:38Case_Labeling: theory HOL-Hoare.Hoare_Syntax
10:35:38Case_Labeling: theory HOL-Eisbach.Eisbach
10:35:38Case_Labeling: theory HOL-Hoare.Hoare_Tac
10:35:38Timing CYK (4 threads, 4.964s elapsed time, 13.977s cpu time, 1.571s GC time, factor 2.82)
10:35:38Finished CYK (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.41)
10:35:38WebAssembly: theory WebAssembly.Wasm_Axioms
10:35:38WebAssembly: theory WebAssembly.Wasm_Checker_Types
10:35:38WebAssembly: theory WebAssembly.Wasm_Properties_Aux
10:35:39WebAssembly: theory WebAssembly.Wasm_Interpreter
10:35:39WebAssembly: theory WebAssembly.Wasm_Properties
10:35:39Case_Labeling: theory Case_Labeling.Conditionals
10:35:39Case_Labeling: theory Case_Labeling.Monadic_Language
10:35:39Timing Cartan_FP (4 threads, 2.371s elapsed time, 4.933s cpu time, 0.141s GC time, factor 2.08)
10:35:39Finished Cartan_FP (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.51)
10:35:41Case_Labeling: theory HOL-Hoare.Hoare_Logic
10:35:41Card_Multisets: theory Card_Multisets.Card_Multisets
10:35:41WebAssembly: theory WebAssembly.Wasm_Soundness
10:35:42Case_Labeling: theory Case_Labeling.Labeled_Hoare
10:35:43WebAssembly: theory WebAssembly.Wasm_Checker
10:35:43Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
10:35:43Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
10:35:45Timing Card_Multisets (4 threads, 9.923s elapsed time, 27.635s cpu time, 1.341s GC time, factor 2.78)
10:35:45Finished Card_Multisets (0:00:11 elapsed time, 0:00:29 cpu time, factor 2.54)
10:35:47Timing Weighted_Path_Order (4 threads, 39.526s elapsed time, 100.512s cpu time, 6.221s GC time, factor 2.54)
10:35:47Finished Weighted_Path_Order (0:00:54 elapsed time, 0:02:06 cpu time, factor 2.30)
10:35:47Timing Case_Labeling (4 threads, 8.487s elapsed time, 22.243s cpu time, 1.587s GC time, factor 2.62)
10:35:47Finished Case_Labeling (0:00:10 elapsed time, 0:00:23 cpu time, factor 2.37)
10:35:48Timing Safe_OCL (4 threads, 213.978s elapsed time, 414.343s cpu time, 91.662s GC time, factor 1.94)
10:35:48Finished Safe_OCL (0:03:36 elapsed time, 0:06:58 cpu time, factor 1.93)
10:35:49WebAssembly: theory WebAssembly.Wasm_Interpreter_Properties
10:35:49WebAssembly: theory WebAssembly.Wasm_Checker_Properties
10:35:49Timing Winding_Number_Eval (4 threads, 51.303s elapsed time, 177.299s cpu time, 11.901s GC time, factor 3.46)
10:35:49Finished Winding_Number_Eval (0:00:54 elapsed time, 0:03:00 cpu time, factor 3.34)
10:35:50Running Abstract_Soundness (on of1-proof) ...
10:35:50Running Ceva (on of1-proof) ...
10:35:51Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
10:35:51Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
10:35:51Ceva: theory Triangle.Angles
10:35:51Ceva: theory Triangle.Triangle
10:35:51Ceva: theory Ceva.Ceva
10:35:54Timing Ceva (8 threads, 2.471s elapsed time, 7.401s cpu time, 0.340s GC time, factor 3.00)
10:35:54Finished Ceva (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.26)
10:35:56Timing Abstract_Soundness (8 threads, 4.575s elapsed time, 11.486s cpu time, 0.900s GC time, factor 2.51)
10:35:56Finished Abstract_Soundness (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.31)
10:35:57Running Efficient_Weighted_Path_Order (on of2.proof.cit.tum.de) ...
10:35:57Running Multiset_Ordering_NPC (on of2.proof.cit.tum.de) ...
10:35:57Running Chord_Segments (on of2.proof.cit.tum.de) ...
10:35:58Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.Indexed_Term
10:35:58Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Propositional_Formula
10:35:58Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_More
10:35:58Chord_Segments: theory Triangle.Angles
10:35:59Chord_Segments: theory Triangle.Triangle
10:35:59Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.List_Memo_Functions
10:35:59Chord_Segments: theory Chord_Segments.Chord_Segments
10:35:59Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_in_NP
10:35:59Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_NP_Hard
10:35:59Running Clean (on of4.proof.cit.tum.de) ...
10:35:59Running Coinductive_Languages (on of4.proof.cit.tum.de) ...
10:35:59Running Combinatorics_Words_Graph_Lemma (on of4.proof.cit.tum.de) ...
10:36:00Coinductive_Languages: theory Coinductive_Languages.Coinductive_Language
10:36:00Coinductive_Languages: theory HOL-Library.Nat_Bijection
10:36:00Coinductive_Languages: theory HOL-Library.Old_Datatype
10:36:00Coinductive_Languages: theory Regular-Sets.Regular_Set
10:36:00Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
10:36:00Clean: theory HOL-Eisbach.Eisbach
10:36:00Clean: theory Clean.Lens_Laws
10:36:00Clean: theory Clean.MonadSE
10:36:00Clean: theory HOL-Library.Cancellation
10:36:00Running Combinatorics_Words_Lyndon (on of3.proof.cit.tum.de) ...
10:36:00Coinductive_Languages: theory HOL-Library.Countable
10:36:00Timing Chord_Segments (8 threads, 1.459s elapsed time, 3.668s cpu time, 0.137s GC time, factor 2.51)
10:36:00Finished Chord_Segments (0:00:02 elapsed time, 0:00:04 cpu time)
10:36:00Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
10:36:01Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Approx
10:36:01Running Comparison_Sort_Lower_Bound (on of3.proof.cit.tum.de) ...
10:36:01Clean: theory HOL-Library.Multiset
10:36:01Running Complete_Non_Orders (on of3.proof.cit.tum.de) ...
10:36:01Clean: theory Clean.Seq_MonadSE
10:36:01Clean: theory Clean.Optics
10:36:01Coinductive_Languages: theory HOL-Library.FSet
10:36:01Timing Combinatorics_Words_Graph_Lemma (8 threads, 0.809s elapsed time, 1.673s cpu time, 0.061s GC time, factor 2.07)
10:36:01Finished Combinatorics_Words_Graph_Lemma (0:00:01 elapsed time)
10:36:01Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Mem_Impl
10:36:01Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
10:36:01Complete_Non_Orders: theory Complete_Non_Orders.Binary_Relations
10:36:01Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
10:36:01Clean: theory Clean.Symbex_MonadSE
10:36:02Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
10:36:02Clean: theory Clean.Clean
10:36:02Comparison_Sort_Lower_Bound: theory List-Index.List_Index
10:36:02Clean: theory Clean.Hoare_MonadSE
10:36:02Coinductive_Languages: theory Coinductive_Languages.Coinductive_Regular_Set
10:36:03Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
10:36:03Clean: theory Clean.Clean_Symbex
10:36:03Clean: theory Clean.Hoare_Clean
10:36:03Clean: theory Clean.LinearSearch
10:36:03Clean: theory Clean.Test_Clean
10:36:03Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
10:36:03Clean: theory Clean.Quicksort
10:36:03Clean: theory Clean.Quicksort_concept
10:36:03Clean: theory Clean.SquareRoot_concept
10:36:03Clean: theory Clean.Clean_Main
10:36:03Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
10:36:04Coinductive_Languages: theory Coinductive_Languages.Context_Free_Grammar
10:36:04Timing Combinatorics_Words_Lyndon (8 threads, 1.805s elapsed time, 7.266s cpu time, 0.295s GC time, factor 4.03)
10:36:04Finished Combinatorics_Words_Lyndon (0:00:02 elapsed time, 0:00:07 cpu time)
10:36:04Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Unbounded
10:36:04Running ConcurrentIMP (on 10.195.8.42) ...
10:36:04Running Constructor_Funs (on 10.195.8.42) ...
10:36:04Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.RPO_NP_Hard
10:36:04Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Mem_Impl
10:36:05Clean: theory HOL-Computational_Algebra.Factorial_Ring
10:36:05Constructor_Funs: theory Constructor_Funs.Constructor_Funs
10:36:05Timing Efficient_Weighted_Path_Order (8 threads, 6.536s elapsed time, 13.631s cpu time, 2.372s GC time, factor 2.09)
10:36:05Finished Efficient_Weighted_Path_Order (0:00:07 elapsed time, 0:00:14 cpu time, factor 1.94)
10:36:05Timing Comparison_Sort_Lower_Bound (8 threads, 2.768s elapsed time, 8.618s cpu time, 0.800s GC time, factor 3.11)
10:36:05Finished Comparison_Sort_Lower_Bound (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.37)
10:36:05Running Dedekind_Real (on 10.195.8.29) ...
10:36:05Running Dict_Construction (on 10.195.8.29) ...
10:36:05Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
10:36:06ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
10:36:06Timing Coinductive_Languages (8 threads, 5.817s elapsed time, 23.682s cpu time, 1.694s GC time, factor 4.07)
10:36:06Finished Coinductive_Languages (0:00:06 elapsed time, 0:00:24 cpu time, factor 3.73)
10:36:06ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
10:36:06Running Digit_Expansions (on 10.195.6.179) ...
10:36:06Dedekind_Real: theory Dedekind_Real.Dedekind_Real
10:36:07Dict_Construction: theory Deriving.Derive_Manager
10:36:07ConcurrentIMP: theory ConcurrentIMP.LTL
10:36:07Complete_Non_Orders: theory Complete_Non_Orders.Well_Relations
10:36:07Dict_Construction: theory Dict_Construction.Impossibility
10:36:07Dict_Construction: theory Deriving.Generator_Aux
10:36:07Dict_Construction: theory Automatic_Refinement.Refine_Util_Bootstrap1
10:36:07Dict_Construction: theory Dict_Construction.Introduction
10:36:07Dict_Construction: theory Automatic_Refinement.Mk_Term_Antiquot
10:36:07Dict_Construction: theory Automatic_Refinement.Mpat_Antiquot
10:36:07Dict_Construction: theory HOL-Library.ListVector
10:36:07Dict_Construction: theory Lazy_Case.Lazy_Case
10:36:07Dict_Construction: theory Automatic_Refinement.Refine_Util
10:36:07ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
10:36:07Dict_Construction: theory Show.Show
10:36:08Digit_Expansions: theory Digit_Expansions.Bits_Digits
10:36:08Dict_Construction: theory Dict_Construction.Dict_Construction
10:36:08Running DigitsInBase (on 10.195.7.194) ...
10:36:08Running Directed_Sets (on 10.195.7.194) ...
10:36:08Digit_Expansions: theory Digit_Expansions.Carries
10:36:08Digit_Expansions: theory Digit_Expansions.Binary_Operations
10:36:08Complete_Non_Orders: theory Complete_Non_Orders.Directedness
10:36:09Clean: theory HOL-Computational_Algebra.Euclidean_Algorithm
10:36:09Complete_Non_Orders: theory Complete_Non_Orders.Complete_Relations
10:36:09Dict_Construction: theory Show.Show_Instances
10:36:09Running Dominance_CHK (on 10.195.8.46) ...
10:36:09Complete_Non_Orders: theory Complete_Non_Orders.Continuity
10:36:09Complete_Non_Orders: theory Complete_Non_Orders.Fixed_Points
10:36:09Building Epistemic_Logic (on 10.195.8.46) ...
10:36:09Directed_Sets: theory Complete_Non_Orders.Binary_Relations
10:36:09Directed_Sets: theory HOL-Cardinals.Fun_More
10:36:09Directed_Sets: theory HOL-Cardinals.Order_Relation_More
10:36:09Directed_Sets: theory HOL-Cardinals.Order_Union
10:36:10Complete_Non_Orders: theory Complete_Non_Orders.Kleene_Fixed_Point
10:36:10Directed_Sets: theory HOL-Library.FuncSet
10:36:10Timing Timed_Automata (4 threads, 148.256s elapsed time, 387.676s cpu time, 30.344s GC time, factor 2.61)
10:36:10Finished Timed_Automata (0:02:30 elapsed time, 0:06:31 cpu time, factor 2.60)
10:36:10Directed_Sets: theory HOL-Cardinals.Wellorder_Extension
10:36:10Dict_Construction: theory Dict_Construction.Termination
10:36:10Dict_Construction: theory Dict_Construction.Test_Side_Conditions
10:36:10Dict_Construction: theory Dict_Construction.Test_Dict_Construction
10:36:10DigitsInBase: theory DigitsInBase.DigitsInBase
10:36:10Directed_Sets: theory HOL-Cardinals.Wellfounded_More
10:36:10Directed_Sets: theory HOL-Cardinals.Wellorder_Relation
10:36:10Running Error_Function (on 10.195.8.30) ...
10:36:11Directed_Sets: theory HOL-Cardinals.Wellorder_Embedding
10:36:11Running Euler_Polyhedron_Formula (on 10.195.8.30) ...
10:36:11Epistemic_Logic: theory Epistemic_Logic.Maximal_Consistent_Sets
10:36:11Dominance_CHK: theory Dominance_CHK.Cfg
10:36:11Dominance_CHK: theory HOL-Data_Structures.Less_False
10:36:11Dominance_CHK: theory HOL-Data_Structures.Cmp
10:36:11Dominance_CHK: theory HOL-Library.NList
10:36:11Directed_Sets: theory HOL-Cardinals.Wellorder_Constructions
10:36:11Dominance_CHK: theory HOL-Data_Structures.Sorted_Less
10:36:11Dict_Construction: theory Dict_Construction.Test_Lazy_Case
10:36:11Dominance_CHK: theory HOL-Library.While_Combinator
10:36:11Epistemic_Logic: theory Epistemic_Logic.Epistemic_Logic
10:36:11Dominance_CHK: theory Dominance_CHK.Sorted_Less2
10:36:11Dominance_CHK: theory Dominance_CHK.Sorted_List_Operations2
10:36:11Directed_Sets: theory HOL-Cardinals.Cardinal_Order_Relation
10:36:12Directed_Sets: theory HOL-Cardinals.Ordinal_Arithmetic
10:36:12Dominance_CHK: theory Jinja.Semilat
10:36:12Running FOL_Axiomatic (on 10.195.8.40) ...
10:36:12Timing Complete_Non_Orders (8 threads, 9.977s elapsed time, 21.330s cpu time, 2.187s GC time, factor 2.14)
10:36:12Finished Complete_Non_Orders (0:00:10 elapsed time, 0:00:22 cpu time, factor 2.10)
10:36:12Running FOL_Seq_Calc1 (on 10.195.8.40) ...
10:36:12Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
10:36:12Dominance_CHK: theory Dominance_CHK.Dom_Semi_List
10:36:12Dominance_CHK: theory Jinja.Err
10:36:13Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
10:36:13Directed_Sets: theory HOL-Cardinals.Cardinal_Arithmetic
10:36:13Clean: theory HOL-Computational_Algebra.Primes
10:36:13Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
10:36:13Error_Function: theory HOL-Library.Function_Algebras
10:36:13Clean: theory Clean.IsPrime
10:36:13FOL_Axiomatic: theory HOL-Library.Nat_Bijection
10:36:13Error_Function: theory Error_Function.Error_Function
10:36:13Dominance_CHK: theory Jinja.Listn
10:36:13FOL_Axiomatic: theory HOL-Library.Old_Datatype
10:36:13Euler_Polyhedron_Formula: theory Euler_Polyhedron_Formula.Euler_Formula
10:36:13Dominance_CHK: theory Jinja.Opt
10:36:13Error_Function: theory Landau_Symbols.Group_Sort
10:36:13Dominance_CHK: theory Jinja.Product
10:36:13Timing Multiset_Ordering_NPC (8 threads, 14.399s elapsed time, 28.301s cpu time, 2.188s GC time, factor 1.97)
10:36:13Finished Multiset_Ordering_NPC (0:00:15 elapsed time, 0:00:30 cpu time, factor 1.93)
10:36:13Directed_Sets: theory HOL-Cardinals.Cardinals
10:36:14Running FOL_Seq_Calc2 (on 10.195.8.11) ...
10:36:14FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
10:36:14FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
10:36:14Dominance_CHK: theory Jinja.Semilattices
10:36:14Dominance_CHK: theory Jinja.Typing_Framework_1
10:36:14FOL_Axiomatic: theory HOL-Library.Countable
10:36:14Dominance_CHK: theory Jinja.SemilatAlg
10:36:15FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
10:36:15Timing DigitsInBase (4 threads, 3.904s elapsed time, 7.949s cpu time, 0.279s GC time, factor 2.04)
10:36:15Finished DigitsInBase (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.65)
10:36:15Dominance_CHK: theory Dominance_CHK.Dom_Kildall
10:36:15Dominance_CHK: theory Jinja.Kildall_1
10:36:15Dominance_CHK: theory Dominance_CHK.Dom_Kildall_Property
10:36:15FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent2
10:36:15Error_Function: theory Landau_Symbols.Landau_Real_Products
10:36:15FOL_Seq_Calc2: theory FOL_Seq_Calc2.SeCaV
10:36:15FOL_Seq_Calc2: theory Collections.ICF_Tools
10:36:15FOL_Seq_Calc2: theory FOL-Fitting.FOL_Fitting
10:36:15Timing Clean (8 threads, 15.017s elapsed time, 49.957s cpu time, 5.829s GC time, factor 3.33)
10:36:15Finished Clean (0:00:16 elapsed time, 0:00:51 cpu time, factor 3.20)
10:36:16Timing Dedekind_Real (4 threads, 8.524s elapsed time, 17.697s cpu time, 0.414s GC time, factor 2.08)
10:36:16Finished Dedekind_Real (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.92)
10:36:16FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
10:36:16FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic_Variant
10:36:16FOL_Seq_Calc2: theory Collections.Ord_Code_Preproc
10:36:16FOL_Seq_Calc2: theory Collections.Locale_Code
10:36:16Running FOL_Seq_Calc3 (on 10.195.8.49) ...
10:36:16Dominance_CHK: theory Dominance_CHK.Dom_Kildall_Correct
10:36:16FOL_Seq_Calc2: theory Abstract_Completeness.Abstract_Completeness
10:36:16ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
10:36:17Timing Constructor_Funs (4 threads, 11.480s elapsed time, 8.221s cpu time, 0.543s GC time, factor 0.72)
10:36:17Finished Constructor_Funs (0:00:12 elapsed time, 0:00:09 cpu time, factor 0.74)
10:36:17Timing Digit_Expansions (4 threads, 8.965s elapsed time, 28.709s cpu time, 0.770s GC time, factor 3.20)
10:36:17Finished Digit_Expansions (0:00:10 elapsed time, 0:00:30 cpu time, factor 2.91)
10:36:18FOL_Seq_Calc3: theory Collections.ICF_Tools
10:36:18FOL_Seq_Calc3: theory FOL_Seq_Calc3.List_Syntax
10:36:18FOL_Seq_Calc3: theory FOL_Seq_Calc3.Fair_Stream
10:36:18FOL_Seq_Calc3: theory FOL_Seq_Calc3.Syntax
10:36:18FOL_Seq_Calc3: theory Collections.Ord_Code_Preproc
10:36:18FOL_Seq_Calc3: theory Collections.Locale_Code
10:36:18FOL_Seq_Calc3: theory Abstract_Completeness.Abstract_Completeness
10:36:19FOL_Seq_Calc2: theory FOL_Seq_Calc2.Usemantics
10:36:19FOL_Seq_Calc2: theory Abstract_Soundness.Finite_Proof_Soundness
10:36:19FOL_Seq_Calc2: theory FOL_Seq_Calc2.Prover
10:36:20Error_Function: theory Landau_Symbols.Landau_Simprocs
10:36:20FOL_Seq_Calc3: theory FOL_Seq_Calc3.Semantics
10:36:20FOL_Seq_Calc3: theory FOL_Seq_Calc3.Encoding
10:36:21Error_Function: theory Landau_Symbols.Landau_More
10:36:21Error_Function: theory Error_Function.Error_Function_Asymptotics
10:36:21Timing FOL_Seq_Calc1 (4 threads, 6.801s elapsed time, 16.493s cpu time, 0.533s GC time, factor 2.43)
10:36:21Finished FOL_Seq_Calc1 (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.09)
10:36:22FOL_Seq_Calc3: theory Abstract_Soundness.Finite_Proof_Soundness
10:36:22FOL_Seq_Calc3: theory FOL_Seq_Calc3.Prover
10:36:23FOL_Seq_Calc3: theory FOL_Seq_Calc3.Completeness
10:36:23Timing FOL_Axiomatic (4 threads, 9.162s elapsed time, 27.038s cpu time, 2.912s GC time, factor 2.95)
10:36:23Finished FOL_Axiomatic (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.71)
10:36:23FOL_Seq_Calc3: theory FOL_Seq_Calc3.Export
10:36:23FOL_Seq_Calc3: theory FOL_Seq_Calc3.Soundness
10:36:23ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
10:36:23FOL_Seq_Calc2: theory FOL_Seq_Calc2.Export
10:36:23FOL_Seq_Calc2: theory FOL_Seq_Calc2.Hintikka
10:36:23FOL_Seq_Calc2: theory FOL_Seq_Calc2.ProverLemmas
10:36:23ConcurrentIMP: theory ConcurrentIMP.CIMP
10:36:23FOL_Seq_Calc3: theory FOL_Seq_Calc3.Result
10:36:24ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
10:36:24ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
10:36:24ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
10:36:24FOL_Seq_Calc2: theory FOL_Seq_Calc2.Countermodel
10:36:24FOL_Seq_Calc2: theory FOL_Seq_Calc2.EPathHintikka
10:36:24FOL_Seq_Calc2: theory FOL_Seq_Calc2.Soundness
10:36:24Timing Error_Function (4 threads, 10.685s elapsed time, 33.643s cpu time, 2.419s GC time, factor 3.15)
10:36:24Finished Error_Function (0:00:13 elapsed time, 0:00:36 cpu time, factor 2.70)
10:36:25Timing Epistemic_Logic (4 threads, 6.595s elapsed time, 15.694s cpu time, 1.233s GC time, factor 2.38)
10:36:25Finished Epistemic_Logic (0:00:14 elapsed time, 0:00:28 cpu time, factor 1.92)
10:36:25FOL_Seq_Calc2: theory FOL_Seq_Calc2.Completeness
10:36:26Directed_Sets: theory Complete_Non_Orders.Well_Relations
10:36:28FOL_Seq_Calc2: theory FOL_Seq_Calc1.Common
10:36:28FOL_Seq_Calc2: theory FOL_Seq_Calc1.Tableau
10:36:28Timing FOL_Seq_Calc3 (4 threads, 9.809s elapsed time, 31.547s cpu time, 2.415s GC time, factor 3.22)
10:36:28Finished FOL_Seq_Calc3 (0:00:11 elapsed time, 0:00:33 cpu time, factor 2.83)
10:36:28FOL_Seq_Calc2: theory FOL_Seq_Calc1.Sequent
10:36:29FOL_Seq_Calc2: theory FOL_Seq_Calc2.Sequent1
10:36:29FOL_Seq_Calc2: theory FOL_Seq_Calc2.Sequent_Calculus_Verifier
10:36:29FOL_Seq_Calc2: theory FOL_Seq_Calc2.Results
10:36:30Running Falling_Factorial_Sum (on of1-proof) ...
10:36:30Running Fishburn_Impossibility (on of1-proof) ...
10:36:30Fishburn_Impossibility: theory HOL-Combinatorics.Transposition
10:36:30Fishburn_Impossibility: theory HOL-Library.FuncSet
10:36:30Fishburn_Impossibility: theory HOL-Library.Cancellation
10:36:30Fishburn_Impossibility: theory List-Index.List_Index
10:36:31Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
10:36:31Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
10:36:31Fishburn_Impossibility: theory HOL-Library.Disjoint_Sets
10:36:31Fishburn_Impossibility: theory HOL-Library.Multiset
10:36:31Falling_Factorial_Sum: theory Discrete_Summation.Factorials
10:36:31Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
10:36:31Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
10:36:31Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
10:36:32Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
10:36:33Directed_Sets: theory Complete_Non_Orders.Directedness
10:36:33Directed_Sets: theory Directed_Sets.Well_Order_Connection
10:36:33Timing ConcurrentIMP (4 threads, 26.245s elapsed time, 74.821s cpu time, 7.613s GC time, factor 2.85)
10:36:33Finished ConcurrentIMP (0:00:28 elapsed time, 0:01:18 cpu time, factor 2.73)
10:36:33Timing Falling_Factorial_Sum (8 threads, 1.697s elapsed time, 7.195s cpu time, 0.273s GC time, factor 4.24)
10:36:33Finished Falling_Factorial_Sum (0:00:02 elapsed time, 0:00:08 cpu time)
10:36:34Fishburn_Impossibility: theory HOL-Combinatorics.Permutations
10:36:34Directed_Sets: theory Complete_Non_Orders.Complete_Relations
10:36:34Fishburn_Impossibility: theory Randomised_Social_Choice.Order_Predicates
10:36:35Fishburn_Impossibility: theory Randomised_Social_Choice.Preference_Profiles
10:36:35Fishburn_Impossibility: theory Randomised_Social_Choice.Elections
10:36:35Fishburn_Impossibility: theory Randomised_Social_Choice.Preference_Profile_Cmd
10:36:36Fishburn_Impossibility: theory Fishburn_Impossibility.Social_Choice_Functions
10:36:36Directed_Sets: theory Complete_Non_Orders.Continuity
10:36:36Fishburn_Impossibility: theory Fishburn_Impossibility.Fishburn_Impossibility
10:36:37Running Fisher_Yates (on of2.proof.cit.tum.de) ...
10:36:37Running FocusStreamsCaseStudies (on of2.proof.cit.tum.de) ...
10:36:37Running Formula_Derivatives-Examples (on of2.proof.cit.tum.de) ...
10:36:37Directed_Sets: theory Directed_Sets.Directed_Completeness
10:36:37FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ListExtras
10:36:37FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ArithExtras
10:36:37FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.arith_hints
10:36:38FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.stream
10:36:38Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.Presburger_Examples
10:36:38Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Alt_Examples
10:36:38Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Examples
10:36:38Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Presburger_Examples
10:36:38Formula_Derivatives-Examples: theory Show.Show
10:36:38Fisher_Yates: theory Fisher_Yates.Fisher_Yates
10:36:38Running Fresh_Identifiers (on of4.proof.cit.tum.de) ...
10:36:39Formula_Derivatives-Examples: theory Show.Show_Instances
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.BitBoolTS
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_types
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_types
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.JoinSplitTime
10:36:39Running GaleStewart_Games (on of4.proof.cit.tum.de) ...
10:36:39Running GewirthPGCProof (on of4.proof.cit.tum.de) ...
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler
10:36:39FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler_proof
10:36:39Timing Fishburn_Impossibility (8 threads, 7.507s elapsed time, 39.307s cpu time, 4.035s GC time, factor 5.24)
10:36:39Finished Fishburn_Impossibility (0:00:08 elapsed time, 0:00:40 cpu time, factor 4.77)
10:36:40FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR
10:36:40Fresh_Identifiers: theory Fresh_Identifiers.Fresh
10:36:40GewirthPGCProof: theory GewirthPGCProof.CJDDLplus
10:36:40GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
10:36:40Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
10:36:40Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
10:36:40Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
10:36:40Running Goodstein_Lambda (on of3.proof.cit.tum.de) ...
10:36:40GaleStewart_Games: theory GaleStewart_Games.MoreENat
10:36:40GaleStewart_Games: theory GaleStewart_Games.MorePrefix
10:36:40Formula_Derivatives-Examples: theory Formula_Derivatives-Examples.WS1S_Nameful_Examples
10:36:40FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_proof
10:36:40Timing Fisher_Yates (8 threads, 1.415s elapsed time, 4.048s cpu time, 0.150s GC time, factor 2.86)
10:36:40Finished Fisher_Yates (0:00:02 elapsed time, 0:00:05 cpu time)
10:36:40GewirthPGCProof: theory GewirthPGCProof.ExtendedDDL
10:36:40GewirthPGCProof: theory GewirthPGCProof.GewirthArgument
10:36:40Running Hidden_Markov_Models (on of3.proof.cit.tum.de) ...
10:36:40Running Hood_Melville_Queue (on of3.proof.cit.tum.de) ...
10:36:41GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
10:36:41GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
10:36:41Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
10:36:41FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway
10:36:41Hood_Melville_Queue: theory HOL-Data_Structures.Queue_Spec
10:36:41Hood_Melville_Queue: theory Hood_Melville_Queue.Hood_Melville_Queue
10:36:41FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof_aux
10:36:42GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
10:36:42Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
10:36:42FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof
10:36:42GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
10:36:42Timing Euler_Polyhedron_Formula (4 threads, 27.432s elapsed time, 51.993s cpu time, 4.173s GC time, factor 1.90)
10:36:42Finished Euler_Polyhedron_Formula (0:00:30 elapsed time, 0:00:54 cpu time, factor 1.81)
10:36:42Timing Dominance_CHK (4 threads, 29.806s elapsed time, 101.649s cpu time, 3.682s GC time, factor 3.41)
10:36:42Finished Dominance_CHK (0:00:31 elapsed time, 0:01:43 cpu time, factor 3.29)
10:36:42Timing Fresh_Identifiers (8 threads, 1.887s elapsed time, 3.954s cpu time, 0.108s GC time, factor 2.10)
10:36:42Finished Fresh_Identifiers (0:00:02 elapsed time, 0:00:04 cpu time)
10:36:42Hidden_Markov_Models: theory HOL-Library.State_Monad
10:36:42Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
10:36:42Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
10:36:42Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
10:36:42Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
10:36:43WebAssembly: theory Native_Word.Code_Target_Int_Bit
10:36:43WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing
10:36:43WebAssembly: theory WebAssembly.Wasm_Type_Abs_Printing
10:36:43WebAssembly: theory WebAssembly.Wasm_Checker_Printing
10:36:43WebAssembly: theory WebAssembly.Wasm_Printing
10:36:43Timing Goodstein_Lambda (8 threads, 1.338s elapsed time, 3.861s cpu time, 0.154s GC time, factor 2.89)
10:36:43WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing_Pure
10:36:43Finished Goodstein_Lambda (0:00:02 elapsed time, 0:00:04 cpu time)
10:36:43Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
10:36:43Timing GaleStewart_Games (8 threads, 2.826s elapsed time, 6.939s cpu time, 0.182s GC time, factor 2.46)
10:36:43Finished GaleStewart_Games (0:00:03 elapsed time, 0:00:07 cpu time, factor 2.09)
10:36:43Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
10:36:43Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
10:36:44Hidden_Markov_Models: theory Monad_Memo_DP.Memory
10:36:44Running IMAP-CRDT (on 10.195.8.42) ...
10:36:44Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
10:36:45Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
10:36:45Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
10:36:45Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
10:36:45Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
10:36:45IMAP-CRDT: theory IMAP-CRDT.IMAP-def
10:36:45Timing FocusStreamsCaseStudies (8 threads, 7.209s elapsed time, 30.137s cpu time, 1.985s GC time, factor 4.18)
10:36:45Finished FocusStreamsCaseStudies (0:00:08 elapsed time, 0:00:31 cpu time, factor 3.84)
10:36:45Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
10:36:46Running IMP2_Binary_Heap (on 10.195.8.29) ...
10:36:46Timing Directed_Sets (4 threads, 34.130s elapsed time, 121.433s cpu time, 12.869s GC time, factor 3.56)
10:36:46Finished Directed_Sets (0:00:36 elapsed time, 0:02:04 cpu time, factor 3.44)
10:36:46Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
10:36:46Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
10:36:47Timing Dict_Construction (4 threads, 38.359s elapsed time, 84.298s cpu time, 9.589s GC time, factor 2.20)
10:36:47Finished Dict_Construction (0:00:40 elapsed time, 0:01:27 cpu time, factor 2.17)
10:36:47Running IMP_Compiler (on 10.195.6.179) ...
10:36:47Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
10:36:47IMP2_Binary_Heap: theory IMP2_Binary_Heap.IMP2_Binary_Heap
10:36:48IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-commute
10:36:48IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-helpers
10:36:48Running IMP_Compiler_Reuse (on 10.195.7.194) ...
10:36:48IMP_Compiler: theory HOL-IMP.AExp
10:36:48IMP_Compiler: theory HOL-IMP.Star
10:36:49Timing Formula_Derivatives-Examples (8 threads, 10.499s elapsed time, 49.569s cpu time, 16.757s GC time, factor 4.72)
10:36:49Finished Formula_Derivatives-Examples (0:00:11 elapsed time, 0:00:51 cpu time, factor 4.37)
10:36:49Running IO_Language_Conformance (on 10.195.8.46) ...
10:36:49IMP_Compiler_Reuse: theory HOL-IMP.AExp
10:36:49IMP_Compiler_Reuse: theory HOL-IMP.Star
10:36:49Timing WebAssembly (4 threads, 116.288s elapsed time, 392.067s cpu time, 28.821s GC time, factor 3.37)
10:36:49Finished WebAssembly (0:01:59 elapsed time, 0:06:37 cpu time, factor 3.33)
10:36:50IMP_Compiler: theory HOL-IMP.BExp
10:36:50Running Imperative_Insertion_Sort (on 10.195.8.30) ...
10:36:51IO_Language_Conformance: theory IO_Language_Conformance.Input_Output_Language_Conformance
10:36:51Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
10:36:51IMP_Compiler_Reuse: theory HOL-IMP.BExp
10:36:51IMP_Compiler: theory IMP_Compiler.Compiler
10:36:51Running Interpolation_Polynomials_HOL_Algebra (on 10.195.8.40) ...
10:36:51Running Involutions2Squares (on 10.195.8.40) ...
10:36:52Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
10:36:52Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
10:36:53Involutions2Squares: theory Involutions2Squares.Involutions2Squares
10:36:53IMP_Compiler_Reuse: theory HOL-IMP.Com
10:36:53Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
10:36:53IMAP-CRDT: theory IMAP-CRDT.IMAP-proof-independent
10:36:53Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
10:36:54Timing Hood_Melville_Queue (8 threads, 12.317s elapsed time, 37.593s cpu time, 1.397s GC time, factor 3.05)
10:36:54Finished Hood_Melville_Queue (0:00:13 elapsed time, 0:00:38 cpu time, factor 2.95)
10:36:54IMP_Compiler_Reuse: theory HOL-IMP.Big_Step
10:36:55IMP_Compiler_Reuse: theory IMP_Compiler_Reuse.Compiler
10:36:55Timing Hidden_Markov_Models (8 threads, 12.919s elapsed time, 37.844s cpu time, 4.854s GC time, factor 2.93)
10:36:55Finished Hidden_Markov_Models (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.73)
10:36:55IMP_Compiler: theory IMP_Compiler.Compiler2
10:36:56Timing Involutions2Squares (4 threads, 3.379s elapsed time, 5.582s cpu time, 0.181s GC time, factor 1.65)
10:36:56Finished Involutions2Squares (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.44)
10:36:56Running Irrational_Series_Erdos_Straus (on 10.195.8.49) ...
10:36:57Running Jacobson_Basic_Algebra (on 10.195.8.49) ...
10:36:57IMAP-CRDT: theory IMAP-CRDT.IMAP-proof
10:36:57Timing Imperative_Insertion_Sort (4 threads, 5.130s elapsed time, 13.271s cpu time, 0.433s GC time, factor 2.59)
10:36:57Finished Imperative_Insertion_Sort (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.15)
10:36:58Jacobson_Basic_Algebra: theory HOL-Library.FuncSet
10:36:59Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
10:36:59Jacobson_Basic_Algebra: theory Jacobson_Basic_Algebra.Set_Theory
10:36:59Irrational_Series_Erdos_Straus: theory Prime_Number_Theorem.Prime_Number_Theorem
10:36:59Jacobson_Basic_Algebra: theory Jacobson_Basic_Algebra.Group_Theory
10:37:00Irrational_Series_Erdos_Straus: theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
10:37:00Interpolation_Polynomials_HOL_Algebra: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
10:37:01Timing FOL_Seq_Calc2 (4 threads, 43.927s elapsed time, 130.276s cpu time, 9.044s GC time, factor 2.97)
10:37:01Finished FOL_Seq_Calc2 (0:00:46 elapsed time, 0:02:13 cpu time, factor 2.88)
10:37:02Timing IMP2_Binary_Heap (4 threads, 15.281s elapsed time, 35.877s cpu time, 1.905s GC time, factor 2.35)
10:37:02Finished IMP2_Binary_Heap (0:00:16 elapsed time, 0:00:37 cpu time, factor 2.23)
10:37:02IMP_Compiler_Reuse: theory IMP_Compiler_Reuse.Compiler2
10:37:03Timing IO_Language_Conformance (4 threads, 12.094s elapsed time, 40.880s cpu time, 3.005s GC time, factor 3.38)
10:37:03Finished IO_Language_Conformance (0:00:14 elapsed time, 0:00:43 cpu time, factor 3.06)
10:37:04Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
10:37:05Timing IMAP-CRDT (4 threads, 19.861s elapsed time, 50.700s cpu time, 5.178s GC time, factor 2.55)
10:37:05Finished IMAP-CRDT (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.43)
10:37:06Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
10:37:06Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
10:37:07Timing GewirthPGCProof (8 threads, 27.089s elapsed time, 12.551s cpu time, 0.903s GC time, factor 0.46)
10:37:07Finished GewirthPGCProof (0:00:27 elapsed time, 0:00:13 cpu time, factor 0.48)
10:37:07Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
10:37:10Running Knights_Tour (on of1-proof) ...
10:37:10Running Kuratowski_Closure_Complement (on of1-proof) ...
10:37:11Knights_Tour: theory Knights_Tour.KnightsTour
10:37:11Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem
10:37:15Jacobson_Basic_Algebra: theory Jacobson_Basic_Algebra.Ring_Theory
10:37:15Timing Interpolation_Polynomials_HOL_Algebra (4 threads, 21.334s elapsed time, 48.027s cpu time, 5.565s GC time, factor 2.25)
10:37:15Finished Interpolation_Polynomials_HOL_Algebra (0:00:23 elapsed time, 0:00:50 cpu time, factor 2.12)
10:37:17Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
10:37:17Running LLL_Factorization (on of2.proof.cit.tum.de) ...
10:37:17Running Laplace_Transform (on of2.proof.cit.tum.de) ...
10:37:17Running Lazy_Case (on of2.proof.cit.tum.de) ...
10:37:18Lazy_Case: theory Lazy_Case.Lazy_Case
10:37:18Lazy_Case: theory Lazy_Case.Test_Lazy_Case
10:37:18Running Lifting_Definition_Option (on of4.proof.cit.tum.de) ...
10:37:18Running Lifting_the_Exponent (on of4.proof.cit.tum.de) ...
10:37:18Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
10:37:18Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
10:37:18Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
10:37:19Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
10:37:19Laplace_Transform: theory Laplace_Transform.Existence
10:37:19Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
10:37:19Laplace_Transform: theory Laplace_Transform.Uniqueness
10:37:19LLL_Factorization: theory Perron_Frobenius.Cancel_Card_Constraint
10:37:19Laplace_Transform: theory Laplace_Transform.Laplace_Transform
10:37:19LLL_Factorization: theory LLL_Factorization.Sub_Sums
10:37:19LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
10:37:19Timing Kuratowski_Closure_Complement (8 threads, 7.349s elapsed time, 30.535s cpu time, 3.079s GC time, factor 4.15)
10:37:19Finished Kuratowski_Closure_Complement (0:00:08 elapsed time, 0:00:32 cpu time, factor 3.72)
10:37:20LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
10:37:20Running List_Inversions (on of3.proof.cit.tum.de) ...
10:37:20Running Localization_Ring (on of3.proof.cit.tum.de) ...
10:37:20Timing Lazy_Case (8 threads, 1.495s elapsed time, 2.484s cpu time, 0.197s GC time, factor 1.66)
10:37:20Finished Lazy_Case (0:00:02 elapsed time, 0:00:03 cpu time)
10:37:20Timing Irrational_Series_Erdos_Straus (4 threads, 20.768s elapsed time, 51.581s cpu time, 1.431s GC time, factor 2.48)
10:37:20Finished Irrational_Series_Erdos_Straus (0:00:23 elapsed time, 0:00:54 cpu time, factor 2.34)
10:37:20Timing Lifting_the_Exponent (8 threads, 0.535s elapsed time, 1.912s cpu time, 0.073s GC time, factor 3.57)
10:37:20Finished Lifting_the_Exponent (0:00:01 elapsed time)
10:37:20Timing Lifting_Definition_Option (8 threads, 1.014s elapsed time, 1.291s cpu time, 0.055s GC time, factor 1.27)
10:37:20Finished Lifting_Definition_Option (0:00:01 elapsed time)
10:37:20LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
10:37:21List_Inversions: theory HOL-Combinatorics.Transposition
10:37:21List_Inversions: theory HOL-Library.Cancellation
10:37:21List_Inversions: theory HOL-Library.FuncSet
10:37:21List_Inversions: theory HOL-Library.Multiset
10:37:21List_Inversions: theory HOL-Library.Disjoint_Sets
10:37:22LLL_Factorization: theory LLL_Factorization.LLL_Factorization
10:37:22Timing Laplace_Transform (8 threads, 3.078s elapsed time, 13.722s cpu time, 0.393s GC time, factor 4.46)
10:37:22Finished Laplace_Transform (0:00:04 elapsed time, 0:00:14 cpu time, factor 3.45)
10:37:22Running Lorenz_C1 (on of3.proof.cit.tum.de) ...
10:37:22Timing Knights_Tour (8 threads, 10.509s elapsed time, 61.208s cpu time, 5.196s GC time, factor 5.82)
10:37:22Finished Knights_Tour (0:00:11 elapsed time, 0:01:02 cpu time, factor 5.45)
10:37:23Localization_Ring: theory Localization_Ring.Localization
10:37:24List_Inversions: theory HOL-Combinatorics.Permutations
10:37:24Lorenz_C1: theory Lorenz_C1.Lorenz_C1
10:37:25List_Inversions: theory List_Inversions.List_Inversions
10:37:25LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
10:37:25Timing Lorenz_C1 (8 threads, 0.900s elapsed time, 1.237s cpu time, 0.023s GC time, factor 1.37)
10:37:25Finished Lorenz_C1 (0:00:02 elapsed time)
10:37:25Running Lowe_Ontological_Argument (on 10.195.8.42) ...
10:37:25Running ML_Unification (on 10.195.8.42) ...
10:37:27Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.Relations
10:37:27ML_Unification: theory ML_Unification.ML_Attribute_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Code_Utils
10:37:27ML_Unification: theory ML_Unification.ML_General_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Conversion_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Generic_Data_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Method_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Normalisations
10:37:27ML_Unification: theory ML_Unification.ML_Theorem_Utils
10:37:27ML_Unification: theory ML_Unification.Setup_Result_Commands
10:37:27Timing List_Inversions (8 threads, 5.644s elapsed time, 25.507s cpu time, 1.798s GC time, factor 4.52)
10:37:27Finished List_Inversions (0:00:06 elapsed time, 0:00:26 cpu time, factor 4.00)
10:37:27Running Mason_Stothers (on 10.195.8.29) ...
10:37:27ML_Unification: theory ML_Unification.ML_Attributes
10:37:27Running Matroids (on 10.195.8.29) ...
10:37:27ML_Unification: theory ML_Unification.ML_Binders
10:37:27ML_Unification: theory ML_Unification.ML_Term_Index
10:37:27Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.QML
10:37:27ML_Unification: theory ML_Unification.ML_Term_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Logger
10:37:27ML_Unification: theory ML_Unification.ML_Parsing_Utils
10:37:27Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
10:37:27ML_Unification: theory ML_Unification.ML_Tactic_Utils
10:37:27ML_Unification: theory ML_Unification.ML_Logger_Examples
10:37:27Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
10:37:27ML_Unification: theory ML_Unification.ML_Unification_Base
10:37:27LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
10:37:27Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
10:37:28Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
10:37:28Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
10:37:28Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
10:37:28Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
10:37:28ML_Unification: theory ML_Unification.Simps_To
10:37:28ML_Unification: theory ML_Unification.ML_Functor_Instances
10:37:28ML_Unification: theory ML_Unification.ML_Priorities
10:37:28ML_Unification: theory ML_Unification.ML_Unification_Parsers
10:37:28Running Maximum_Segment_Sum (on 10.195.6.179) ...
10:37:28Matroids: theory Matroids.Indep_System
10:37:28ML_Unification: theory ML_Unification.ML_Utils
10:37:28ML_Unification: theory ML_Unification.ML_Unifiers
10:37:29Mason_Stothers: theory Mason_Stothers.Mason_Stothers
10:37:29Matroids: theory Matroids.Matroid
10:37:29Running Median_Method (on 10.195.7.194) ...
10:37:29ML_Unification: theory ML_Unification.ML_Unification_Hints
10:37:29ML_Unification: theory ML_Unification.Unify_Assumption_Tactic
10:37:29Maximum_Segment_Sum: theory Maximum_Segment_Sum.Maximum_Segment_Sum
10:37:29ML_Unification: theory ML_Unification.Unify_Resolve_Tactics
10:37:30Running Median_Of_Medians_Selection (on 10.195.8.46) ...
10:37:30Running Mereology (on 10.195.8.46) ...
10:37:30Timing Localization_Ring (8 threads, 6.469s elapsed time, 25.896s cpu time, 1.774s GC time, factor 4.00)
10:37:30Finished Localization_Ring (0:00:07 elapsed time, 0:00:27 cpu time, factor 3.47)
10:37:31ML_Unification: theory ML_Unification.Unification_Attributes
10:37:31ML_Unification: theory ML_Unification.Unify_Fact_Tactic
10:37:31ML_Unification: theory ML_Unification.ML_Unification_HOL_Setup
10:37:31Median_Of_Medians_Selection: theory HOL-Library.Cancellation
10:37:32Running Monad_Normalisation (on 10.195.8.30) ...
10:37:32ML_Unification: theory ML_Unification.Unification_Tactics
10:37:32ML_Unification: theory ML_Unification.E_Unification_Examples
10:37:32ML_Unification: theory ML_Unification.Unification_Hints_Reification_Examples
10:37:32Running Monomorphic_Monad (on 10.195.8.30) ...
10:37:32Mereology: theory Mereology.PM
10:37:32Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
10:37:32Timing Mason_Stothers (4 threads, 2.702s elapsed time, 6.101s cpu time, 0.169s GC time, factor 2.26)
10:37:32Finished Mason_Stothers (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.72)
10:37:32Mereology: theory Mereology.M
10:37:32Mereology: theory Mereology.CM
10:37:32Mereology: theory Mereology.MM
10:37:32Mereology: theory Mereology.EM
10:37:32Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
10:37:32Mereology: theory Mereology.GM
10:37:33Mereology: theory Mereology.CEM
10:37:33Mereology: theory Mereology.GMM
10:37:33Median_Of_Medians_Selection: theory HOL-Library.Multiset
10:37:33Running Multitape_To_Singletape_TM (on 10.195.8.40) ...
10:37:33Building Noninterference_CSP (on 10.195.8.40) ...
10:37:33Mereology: theory Mereology.GEM
10:37:34Timing Matroids (4 threads, 4.898s elapsed time, 12.851s cpu time, 0.432s GC time, factor 2.62)
10:37:34Finished Matroids (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.24)
10:37:34Noninterference_CSP: theory Noninterference_CSP.CSPNoninterference
10:37:34Multitape_To_Singletape_TM: theory HOL-Library.FuncSet
10:37:34Median_Method: theory Median_Method.Median
10:37:34Timing IMP_Compiler_Reuse (4 threads, 44.080s elapsed time, 124.496s cpu time, 6.754s GC time, factor 2.82)
10:37:34Finished IMP_Compiler_Reuse (0:00:45 elapsed time, 0:02:06 cpu time, factor 2.76)
10:37:34Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
10:37:34Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
10:37:35Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
10:37:35Noninterference_CSP: theory Noninterference_CSP.ClassicalNoninterference
10:37:35Multitape_To_Singletape_TM: theory Multitape_To_Singletape_TM.TM_Common
10:37:35Running Noninterference_Concurrent_Composition (on 10.195.8.11) ...
10:37:35Timing LLL_Factorization (8 threads, 15.879s elapsed time, 48.215s cpu time, 2.998s GC time, factor 3.04)
10:37:35Finished LLL_Factorization (0:00:17 elapsed time, 0:00:50 cpu time, factor 2.86)
10:37:36Multitape_To_Singletape_TM: theory Multitape_To_Singletape_TM.Multitape_TM
10:37:36Multitape_To_Singletape_TM: theory Multitape_To_Singletape_TM.Singletape_TM
10:37:36Noninterference_CSP: theory Noninterference_CSP.GeneralizedNoninterference
10:37:36Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
10:37:37Timing Monad_Normalisation (4 threads, 1.858s elapsed time, 2.951s cpu time, 0.105s GC time, factor 1.59)
10:37:37Finished Monad_Normalisation (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.19)
10:37:37Timing Maximum_Segment_Sum (4 threads, 6.962s elapsed time, 8.321s cpu time, 0.343s GC time, factor 1.20)
10:37:37Finished Maximum_Segment_Sum (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.13)
10:37:37Timing IMP_Compiler (4 threads, 48.219s elapsed time, 80.501s cpu time, 3.543s GC time, factor 1.67)
10:37:37Finished IMP_Compiler (0:00:49 elapsed time, 0:01:22 cpu time, factor 1.65)
10:37:37Running PAL (on 10.195.8.49) ...
10:37:37Timing Mereology (4 threads, 4.982s elapsed time, 8.847s cpu time, 0.488s GC time, factor 1.78)
10:37:37Finished Mereology (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.58)
10:37:38Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
10:37:38PAL: theory PAL.PAL
10:37:39ML_Unification: theory SpecCheck.SpecCheck_Base
10:37:39ML_Unification: theory SpecCheck.SpecCheck_Show
10:37:39ML_Unification: theory SpecCheck.SpecCheck_Generators
10:37:39ML_Unification: theory SpecCheck.SpecCheck_Output_Style
10:37:40ML_Unification: theory SpecCheck.SpecCheck_Shrink
10:37:40ML_Unification: theory SpecCheck.SpecCheck
10:37:40Timing Median_Method (4 threads, 7.712s elapsed time, 17.718s cpu time, 1.272s GC time, factor 2.30)
10:37:40Finished Median_Method (0:00:10 elapsed time, 0:00:20 cpu time, factor 1.97)
10:37:40ML_Unification: theory ML_Unification.ML_Unification_Tests_Base
10:37:40Multitape_To_Singletape_TM: theory Multitape_To_Singletape_TM.STM_Renaming
10:37:40Timing Lowe_Ontological_Argument (4 threads, 13.441s elapsed time, 13.064s cpu time, 0.606s GC time, factor 0.97)
10:37:40Finished Lowe_Ontological_Argument (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.96)
10:37:41ML_Unification: theory ML_Unification.First_Order_ML_Unification_Tests
10:37:41ML_Unification: theory ML_Unification.Higher_Order_Pattern_ML_Unification_Tests
10:37:41ML_Unification: theory ML_Unification.Higher_Order_ML_Unification_Tests
10:37:41ML_Unification: theory ML_Unification.ML_Unification_Tests
10:37:41Multitape_To_Singletape_TM: theory Multitape_To_Singletape_TM.Multi_Single_TM_Translation
10:37:43Median_Of_Medians_Selection: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
10:37:44Timing Noninterference_Concurrent_Composition (4 threads, 7.227s elapsed time, 22.723s cpu time, 0.645s GC time, factor 3.14)
10:37:44Finished Noninterference_Concurrent_Composition (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.76)
10:37:46Timing PAL (4 threads, 7.222s elapsed time, 21.187s cpu time, 1.538s GC time, factor 2.93)
10:37:46Finished PAL (0:00:08 elapsed time, 0:00:22 cpu time, factor 2.63)
10:37:49Timing Noninterference_CSP (4 threads, 4.917s elapsed time, 13.985s cpu time, 1.183s GC time, factor 2.84)
10:37:49Finished Noninterference_CSP (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.75)
10:37:49Timing Median_Of_Medians_Selection (4 threads, 17.157s elapsed time, 46.608s cpu time, 4.519s GC time, factor 2.72)
10:37:49Finished Median_Of_Medians_Selection (0:00:18 elapsed time, 0:00:48 cpu time, factor 2.57)
10:37:49Timing Universal_Hash_Families (4 threads, 206.396s elapsed time, 725.826s cpu time, 265.386s GC time, factor 3.52)
10:37:49Finished Universal_Hash_Families (0:03:30 elapsed time, 0:12:11 cpu time, factor 3.48)
10:37:51Building Package_logic (on of1-proof) ...
10:37:51Running Partial_Function_MR (on of1-proof) ...
10:37:51Timing Jacobson_Basic_Algebra (4 threads, 52.769s elapsed time, 97.384s cpu time, 9.443s GC time, factor 1.85)
10:37:51Finished Jacobson_Basic_Algebra (0:00:54 elapsed time, 0:01:39 cpu time, factor 1.82)
10:37:51Package_logic: theory Package_logic.SepAlgebra
10:37:51Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
10:37:51Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
10:37:51Partial_Function_MR: theory HOL-Library.Monad_Syntax
10:37:51Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
10:37:52Package_logic: theory Package_logic.PackageLogic
10:37:53Timing ML_Unification (4 threads, 25.556s elapsed time, 52.226s cpu time, 3.472s GC time, factor 2.04)
10:37:53Finished ML_Unification (0:00:27 elapsed time, 0:00:53 cpu time, factor 1.99)
10:37:54Timing Partial_Function_MR (8 threads, 2.554s elapsed time, 4.666s cpu time, 0.704s GC time, factor 1.83)
10:37:54Finished Partial_Function_MR (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.61)
10:37:57Building Noninterference_Ipurge_Unwinding (on of2.proof.cit.tum.de) ...
10:37:58Running Password_Authentication_Protocol (on of2.proof.cit.tum.de) ...
10:37:58Running Prefix_Free_Code_Combinators (on of2.proof.cit.tum.de) ...
10:37:58Noninterference_Ipurge_Unwinding: theory List_Interleaving.ListInterleaving
10:37:58Building Priority_Search_Trees (on of4.proof.cit.tum.de) ...
10:37:58Running PropResPI (on of4.proof.cit.tum.de) ...
10:37:58Running Propositional_Logic_Class (on of4.proof.cit.tum.de) ...
10:37:58Password_Authentication_Protocol: theory Password_Authentication_Protocol.Propaedeutics
10:37:58Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
10:37:59Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
10:37:59PropResPI: theory PropResPI.Propositional_Resolution
10:37:59Propositional_Logic_Class: theory HOL-Library.Cancellation
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.Cmp
10:37:59Propositional_Logic_Class: theory HOL-Library.FuncSet
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.Less_False
10:37:59Propositional_Logic_Class: theory HOL-Combinatorics.Transposition
10:37:59Propositional_Logic_Class: theory Propositional_Logic_Class.Implication_Logic
10:37:59Priority_Search_Trees: theory HOL-Library.Tree
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.Sorted_Less
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.AList_Upd_Del
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.List_Ins_Del
10:37:59Priority_Search_Trees: theory HOL-Data_Structures.Set_Specs
10:37:59Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Logic
10:37:59Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Examples
10:37:59Propositional_Logic_Class: theory HOL-Library.Multiset
10:38:00Priority_Search_Trees: theory HOL-Data_Structures.Map_Specs
10:38:00Priority_Search_Trees: theory Priority_Search_Trees.Prio_Map_Specs
10:38:00Propositional_Logic_Class: theory HOL-Library.Disjoint_Sets
10:38:00Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Logic_Completeness
10:38:00Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
10:38:00Running Public_Announcement_Logic (on of3.proof.cit.tum.de) ...
10:38:00Running Quaternions (on of3.proof.cit.tum.de) ...
10:38:00Building Quick_Sort_Cost (on of3.proof.cit.tum.de) ...
10:38:00Timing Prefix_Free_Code_Combinators (8 threads, 1.790s elapsed time, 4.116s cpu time, 0.133s GC time, factor 2.30)
10:38:00Finished Prefix_Free_Code_Combinators (0:00:02 elapsed time, 0:00:04 cpu time)
10:38:01Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
10:38:01Password_Authentication_Protocol: theory Password_Authentication_Protocol.Protocol
10:38:01Quaternions: theory Quaternions.Quaternions
10:38:01Quick_Sort_Cost: theory HOL-Library.Function_Algebras
10:38:01Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
10:38:01Quick_Sort_Cost: theory List-Index.List_Index
10:38:01Priority_Search_Trees: theory HOL-Data_Structures.Tree2
10:38:02Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
10:38:02PropResPI: theory PropResPI.Prime_Implicates
10:38:02Priority_Search_Trees: theory HOL-Data_Structures.Lookup2
10:38:02Priority_Search_Trees: theory Priority_Search_Trees.PST_General
10:38:02Priority_Search_Trees: theory HOL-Data_Structures.Isin2
10:38:02Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
10:38:02Priority_Search_Trees: theory Priority_Search_Trees.PST_RBT
10:38:03Building Randomised_Social_Choice (on 10.195.8.42) ...
10:38:03Propositional_Logic_Class: theory HOL-Combinatorics.Permutations
10:38:03Timing Noninterference_Ipurge_Unwinding (8 threads, 2.237s elapsed time, 7.053s cpu time, 0.761s GC time, factor 3.15)
10:38:03Finished Noninterference_Ipurge_Unwinding (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.11)
10:38:03Timing Public_Announcement_Logic (8 threads, 2.570s elapsed time, 7.383s cpu time, 0.765s GC time, factor 2.87)
10:38:03Finished Public_Announcement_Logic (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.38)
10:38:03Timing Package_logic (8 threads, 7.201s elapsed time, 25.316s cpu time, 2.201s GC time, factor 3.52)
10:38:03Finished Package_logic (0:00:12 elapsed time, 0:00:37 cpu time, factor 2.97)
10:38:04Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
10:38:04Propositional_Logic_Class: theory HOL-Combinatorics.List_Permutation
10:38:04Propositional_Logic_Class: theory Propositional_Logic_Class.List_Utilities
10:38:04Quick_Sort_Cost: theory Landau_Symbols.Landau_More
10:38:04Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
10:38:04Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Connectives
10:38:04Running Real_Impl (on 10.195.8.29) ...
10:38:04Running Real_Power (on 10.195.8.29) ...
10:38:05Timing PropResPI (8 threads, 6.092s elapsed time, 15.512s cpu time, 1.573s GC time, factor 2.55)
10:38:05Finished PropResPI (0:00:07 elapsed time, 0:00:16 cpu time, factor 2.35)
10:38:05Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
10:38:05Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
10:38:05Running Real_Time_Deque (on 10.195.6.179) ...
10:38:05Running Resolution_FOL (on 10.195.6.179) ...
10:38:05Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
10:38:05Randomised_Social_Choice: theory List-Index.List_Index
10:38:05Real_Power: theory Real_Power.RatPower
10:38:06Real_Impl: theory Deriving.Derive_Manager
10:38:06Real_Impl: theory HOL-Library.Cancellation
10:38:06Real_Impl: theory Deriving.Generator_Aux
10:38:06Real_Impl: theory Real_Impl.Real_Impl
10:38:06Real_Power: theory Real_Power.RealPower
10:38:06Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
10:38:07Real_Impl: theory Show.Show
10:38:07Real_Time_Deque: theory Real_Time_Deque.Deque
10:38:07Real_Time_Deque: theory Real_Time_Deque.RTD_Util
10:38:07Real_Time_Deque: theory Real_Time_Deque.Type_Classes
10:38:07Running Risk_Free_Lending (on 10.195.7.194) ...
10:38:07Running SCC_Bloemen_Sequential (on 10.195.7.194) ...
10:38:07Real_Impl: theory HOL-Library.Multiset
10:38:07Real_Power: theory Real_Power.Log
10:38:07Real_Time_Deque: theory Real_Time_Deque.Stack
10:38:07Timing Propositional_Logic_Class (8 threads, 8.031s elapsed time, 44.962s cpu time, 4.304s GC time, factor 5.60)
10:38:07Finished Propositional_Logic_Class (0:00:09 elapsed time, 0:00:46 cpu time, factor 5.14)
10:38:08Timing Quaternions (8 threads, 6.552s elapsed time, 9.310s cpu time, 0.480s GC time, factor 1.42)
10:38:08Finished Quaternions (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.34)
10:38:08Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
10:38:08Risk_Free_Lending: theory Risk_Free_Lending.Risk_Free_Lending
10:38:08Real_Impl: theory Show.Show_Instances
10:38:08Real_Impl: theory Show.Show_Real
10:38:08Building Saturation_Framework (on 10.195.8.46) ...
10:38:08Running Selection_Heap_Sort (on 10.195.8.46) ...
10:38:08Real_Time_Deque: theory Real_Time_Deque.Current
10:38:08Real_Time_Deque: theory Real_Time_Deque.Idle
10:38:08Real_Time_Deque: theory Real_Time_Deque.Stack_Aux
10:38:08Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
10:38:09Real_Time_Deque: theory Real_Time_Deque.Stack_Proof
10:38:09Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
10:38:09Resolution_FOL: theory Fresh_Identifiers.Fresh
10:38:09Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
10:38:09Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
10:38:09Resolution_FOL: theory HOL-Library.Adhoc_Overloading
10:38:09Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
10:38:09Resolution_FOL: theory HOL-Library.Cancellation
10:38:09Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
10:38:09Resolution_FOL: theory HOL-Library.Infinite_Set
10:38:09Resolution_FOL: theory HOL-Library.Monad_Syntax
10:38:09Resolution_FOL: theory First_Order_Terms.Option_Monad
10:38:09Real_Time_Deque: theory Real_Time_Deque.Idle_Aux
10:38:09Resolution_FOL: theory First_Order_Terms.Renaming2
10:38:09Resolution_FOL: theory Abstract-Rewriting.Seq
10:38:09Running Separation_Logic_Unbounded (on 10.195.8.30) ...
10:38:10Real_Time_Deque: theory Real_Time_Deque.Common
10:38:10Real_Time_Deque: theory Real_Time_Deque.Current_Aux
10:38:10Resolution_FOL: theory HOL-Library.Nat_Bijection
10:38:10Real_Time_Deque: theory Real_Time_Deque.Idle_Proof
10:38:10Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
10:38:10Resolution_FOL: theory HOL-Library.Old_Datatype
10:38:10Resolution_FOL: theory HOL-Library.Multiset
10:38:10Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
10:38:10Saturation_Framework: theory Lambda_Free_RPOs.Lambda_Free_Util
10:38:10Saturation_Framework: theory Saturation_Framework.Calculus
10:38:10Saturation_Framework: theory Open_Induction.Restricted_Predicates
10:38:10Saturation_Framework: theory Well_Quasi_Orders.Infinite_Sequences
10:38:10Real_Time_Deque: theory Real_Time_Deque.Current_Proof
10:38:10Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
10:38:10SCC_Bloemen_Sequential: theory SCC_Bloemen_Sequential.SCC_Bloemen_Sequential
10:38:10Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
10:38:11Resolution_FOL: theory HOL-Library.While_Combinator
10:38:11Running Skip_Lists (on 10.195.8.40) ...
10:38:11Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
10:38:11Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
10:38:11Resolution_FOL: theory Regular-Sets.Regular_Set
10:38:11Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
10:38:11Saturation_Framework: theory Well_Quasi_Orders.Minimal_Elements
10:38:11Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.UnboundedLogic
10:38:11Resolution_FOL: theory HOL-Library.Countable
10:38:11Real_Time_Deque: theory Real_Time_Deque.Big
10:38:11Real_Time_Deque: theory Real_Time_Deque.Small
10:38:11Real_Time_Deque: theory Real_Time_Deque.Common_Aux
10:38:11Resolution_FOL: theory Resolution_FOL.Tree
10:38:12Timing Password_Authentication_Protocol (8 threads, 13.272s elapsed time, 56.497s cpu time, 3.413s GC time, factor 4.26)
10:38:12Finished Password_Authentication_Protocol (0:00:14 elapsed time, 0:00:58 cpu time, factor 4.02)
10:38:12Saturation_Framework: theory Saturation_Framework.Calculus_Variations
10:38:12Saturation_Framework: theory Saturation_Framework.Intersection_Calculus
10:38:12Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
10:38:12Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
10:38:12Timing Priority_Search_Trees (8 threads, 8.096s elapsed time, 19.583s cpu time, 3.667s GC time, factor 2.42)
10:38:12Finished Priority_Search_Trees (0:00:13 elapsed time, 0:00:31 cpu time, factor 2.24)
10:38:12Saturation_Framework: theory Saturation_Framework.Lifting_to_Non_Ground_Calculi
10:38:13Resolution_FOL: theory HOL-Library.Countable_Set
10:38:13Real_Time_Deque: theory Real_Time_Deque.Common_Proof
10:38:13Running Sliding_Window_Algorithm (on 10.195.8.11) ...
10:38:13Skip_Lists: theory Skip_Lists.Pi_pmf
10:38:13Running Source_Coding_Theorem (on 10.195.8.11) ...
10:38:13Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
10:38:13Skip_Lists: theory Skip_Lists.Misc
10:38:13Resolution_FOL: theory Resolution_FOL.TermsAndLiterals
10:38:13Real_Time_Deque: theory Real_Time_Deque.Big_Aux
10:38:14Real_Impl: theory HOL-Computational_Algebra.Factorial_Ring
10:38:14Timing Real_Power (4 threads, 7.920s elapsed time, 20.649s cpu time, 0.627s GC time, factor 2.61)
10:38:14Finished Real_Power (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.33)
10:38:14Skip_Lists: theory Skip_Lists.Geometric_PMF
10:38:14Real_Time_Deque: theory Real_Time_Deque.States
10:38:14Saturation_Framework: theory Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi
10:38:14Sliding_Window_Algorithm: theory Sliding_Window_Algorithm.SWA
10:38:14Real_Time_Deque: theory Real_Time_Deque.Small_Aux
10:38:15Skip_Lists: theory Skip_Lists.Skip_List
10:38:15Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
10:38:15Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
10:38:15Real_Time_Deque: theory Real_Time_Deque.Big_Proof
10:38:15Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
10:38:15Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
10:38:15Running Stalnaker_Logic (on 10.195.8.49) ...
10:38:15Resolution_FOL: theory Regular-Sets.Regular_Exp
10:38:15Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
10:38:17Saturation_Framework: theory Saturation_Framework.Given_Clause_Architectures
10:38:17Real_Time_Deque: theory Real_Time_Deque.Small_Proof
10:38:17Running Surprise_Paradox (on 10.195.8.49) ...
10:38:17Timing Quick_Sort_Cost (8 threads, 5.174s elapsed time, 19.969s cpu time, 1.892s GC time, factor 3.86)
10:38:17Finished Quick_Sort_Cost (0:00:14 elapsed time, 0:00:38 cpu time, factor 2.59)
10:38:17Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
10:38:17Timing Risk_Free_Lending (4 threads, 7.594s elapsed time, 19.537s cpu time, 0.749s GC time, factor 2.57)
10:38:17Finished Risk_Free_Lending (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.27)
10:38:17Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque
10:38:18Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
10:38:18Resolution_FOL: theory Resolution_FOL.Resolution
10:38:18Real_Time_Deque: theory Real_Time_Deque.States_Aux
10:38:19Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
10:38:19Resolution_FOL: theory First_Order_Terms.Term
10:38:20Real_Time_Deque: theory Real_Time_Deque.States_Proof
10:38:20Resolution_FOL: theory Resolution_FOL.Completeness
10:38:20Resolution_FOL: theory Resolution_FOL.Examples
10:38:20Resolution_FOL: theory Regular-Sets.NDerivative
10:38:21Resolution_FOL: theory Regular-Sets.Relation_Interpretation
10:38:21Timing Stalnaker_Logic (4 threads, 2.862s elapsed time, 6.646s cpu time, 0.221s GC time, factor 2.32)
10:38:21Finished Stalnaker_Logic (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.83)
10:38:21Resolution_FOL: theory First_Order_Terms.Unifiers
10:38:22Timing Source_Coding_Theorem (4 threads, 4.894s elapsed time, 9.890s cpu time, 0.349s GC time, factor 2.02)
10:38:22Resolution_FOL: theory First_Order_Terms.Term_Pair_Multiset
10:38:22Finished Source_Coding_Theorem (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.68)
10:38:22Timing Selection_Heap_Sort (4 threads, 10.070s elapsed time, 25.126s cpu time, 2.064s GC time, factor 2.50)
10:38:22Finished Selection_Heap_Sort (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.24)
10:38:22Timing Surprise_Paradox (4 threads, 2.714s elapsed time, 4.587s cpu time, 0.246s GC time, factor 1.69)
10:38:22Finished Surprise_Paradox (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.35)
10:38:22Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Aux
10:38:22Timing Monomorphic_Monad (4 threads, 46.358s elapsed time, 95.354s cpu time, 9.695s GC time, factor 2.06)
10:38:22Finished Monomorphic_Monad (0:00:49 elapsed time, 0:01:39 cpu time, factor 2.00)
10:38:23Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.Combinability
10:38:23Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Dequeue_Proof
10:38:23Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.Distributivity
10:38:23Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Enqueue_Proof
10:38:24Real_Time_Deque: theory Real_Time_Deque.RealTimeDeque_Proof
10:38:24Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.FixedPoint
10:38:24Resolution_FOL: theory Regular-Sets.Equivalence_Checking
10:38:24Timing Skip_Lists (4 threads, 9.883s elapsed time, 32.587s cpu time, 1.157s GC time, factor 3.30)
10:38:24Finished Skip_Lists (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.81)
10:38:25Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.WandProperties
10:38:25Resolution_FOL: theory Regular-Sets.Regexp_Method
10:38:25Real_Impl: theory HOL-Computational_Algebra.Euclidean_Algorithm
10:38:26Resolution_FOL: theory Abstract-Rewriting.Abstract_Rewriting
10:38:27Separation_Logic_Unbounded: theory Separation_Logic_Unbounded.AutomaticVerifiers
10:38:28Resolution_FOL: theory First_Order_Terms.Abstract_Unification
10:38:29Resolution_FOL: theory First_Order_Terms.Unification
10:38:30Timing SCC_Bloemen_Sequential (4 threads, 20.241s elapsed time, 50.922s cpu time, 2.358s GC time, factor 2.52)
10:38:30Finished SCC_Bloemen_Sequential (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.41)
10:38:30Resolution_FOL: theory Resolution_FOL.Unification_Theorem
10:38:30Resolution_FOL: theory Resolution_FOL.Completeness_Instance
10:38:30Running Noninterference_Generic_Unwinding (on of1-proof) ...
10:38:30Running Combinable_Wands (on of1-proof) ...
10:38:31Timing Sliding_Window_Algorithm (4 threads, 15.927s elapsed time, 45.311s cpu time, 1.740s GC time, factor 2.84)
10:38:31Finished Sliding_Window_Algorithm (0:00:17 elapsed time, 0:00:46 cpu time, factor 2.68)
10:38:31Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding
10:38:31Combinable_Wands: theory Combinable_Wands.PosRat
10:38:31Combinable_Wands: theory Combinable_Wands.Mask
10:38:32Combinable_Wands: theory Combinable_Wands.PartialHeapSA
10:38:33Combinable_Wands: theory Combinable_Wands.CombinableWands
10:38:35Timing Combinable_Wands (8 threads, 3.800s elapsed time, 16.771s cpu time, 1.139s GC time, factor 4.41)
10:38:35Finished Combinable_Wands (0:00:04 elapsed time, 0:00:17 cpu time, factor 3.74)
10:38:36Timing Multitape_To_Singletape_TM (4 threads, 61.507s elapsed time, 123.424s cpu time, 12.634s GC time, factor 2.01)
10:38:36Finished Multitape_To_Singletape_TM (0:01:03 elapsed time, 0:02:06 cpu time, factor 1.99)
10:38:37Real_Impl: theory HOL-Computational_Algebra.Primes
10:38:37Real_Impl: theory Real_Impl.Real_Impl_Auxiliary
10:38:37Real_Impl: theory Real_Impl.Prime_Product
10:38:38Running Prim_Dijkstra_Simple (on of2.proof.cit.tum.de) ...
10:38:38Building Random_BSTs (on of2.proof.cit.tum.de) ...
10:38:38Running Synthetic_Completeness (on of2.proof.cit.tum.de) ...
10:38:38Real_Impl: theory Real_Impl.Real_Unique_Impl
10:38:38Timing Noninterference_Generic_Unwinding (8 threads, 6.440s elapsed time, 7.957s cpu time, 0.169s GC time, factor 1.24)
10:38:38Prim_Dijkstra_Simple: theory HOL-Eisbach.Eisbach
10:38:38Finished Noninterference_Generic_Unwinding (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.19)
10:38:39Prim_Dijkstra_Simple: theory HOL-Library.Infinite_Set
10:38:39Prim_Dijkstra_Simple: theory HOL-Library.Old_Datatype
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Fun_More
10:38:39Prim_Dijkstra_Simple: theory HOL-Library.Nat_Bijection
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Order_Relation_More
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Order_Union
10:38:39Running Twelvefold_Way (on of4.proof.cit.tum.de) ...
10:38:39Running Types_Tableaus_and_Goedels_God (on of4.proof.cit.tum.de) ...
10:38:39Building UPF (on of4.proof.cit.tum.de) ...
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Wellfounded_More
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Relation
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Embedding
10:38:39Random_BSTs: theory HOL-Data_Structures.Cmp
10:38:39Random_BSTs: theory HOL-Data_Structures.Less_False
10:38:39Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
10:38:39Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Constructions
10:38:39Random_BSTs: theory HOL-Data_Structures.Sorted_Less
10:38:39Prim_Dijkstra_Simple: theory HOL-Library.Countable
10:38:39Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
10:38:39Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
10:38:39UPF: theory UPF.Monads
10:38:39Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
10:38:40Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
10:38:40Twelvefold_Way: theory HOL-Eisbach.Eisbach
10:38:40Twelvefold_Way: theory HOL-Combinatorics.Stirling
10:38:40Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
10:38:40Twelvefold_Way: theory HOL-Combinatorics.Transposition
10:38:40Twelvefold_Way: theory Card_Multisets.Card_Multisets
10:38:40Twelvefold_Way: theory Card_Number_Partitions.Additions_to_Main
10:38:40Random_BSTs: theory HOL-Data_Structures.Set_Specs
10:38:40Twelvefold_Way: theory Card_Partitions.Set_Partition
10:38:40Twelvefold_Way: theory HOL-ex.Birthday_Paradox
10:38:40Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
10:38:40Random_BSTs: theory HOL-Data_Structures.Tree_Set
10:38:40Synthetic_Completeness: theory HOL-Cardinals.Cardinal_Order_Relation
10:38:40Twelvefold_Way: theory Card_Number_Partitions.Number_Partition
10:38:40Prim_Dijkstra_Simple: theory HOL-Library.Countable_Set
10:38:40Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
10:38:40Prim_Dijkstra_Simple: theory HOL-Library.Countable_Complete_Lattices
10:38:40UPF: theory UPF.UPFCore
10:38:40Running Wetzels_Problem (on of3.proof.cit.tum.de) ...
10:38:40Random_BSTs: theory Random_BSTs.Random_BSTs
10:38:40Twelvefold_Way: theory Card_Number_Partitions.Card_Number_Partitions
10:38:40Running Youngs_Inequality (on of3.proof.cit.tum.de) ...
10:38:40Running Zeckendorf (on of3.proof.cit.tum.de) ...
10:38:41Twelvefold_Way: theory HOL-Combinatorics.Permutations
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Maximal_Consistent_Sets
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Derivations
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Refutations
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_Tableau
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Example_First_Order_Logic
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Example_Hybrid_Logic
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Example_Modal_Logic
10:38:41Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_SC
10:38:41Twelvefold_Way: theory Card_Partitions.Injectivity_Solver
10:38:41Zeckendorf: theory Zeckendorf.Zeckendorf
10:38:41Youngs_Inequality: theory Youngs_Inequality.Youngs
10:38:41Wetzels_Problem: theory HOL-Cardinals.Fun_More
10:38:41Wetzels_Problem: theory HOL-Cardinals.Order_Relation_More
10:38:42Wetzels_Problem: theory HOL-Cardinals.Order_Union
10:38:42UPF: theory UPF.ElementaryPolicies
10:38:42Wetzels_Problem: theory HOL-Cardinals.Wellorder_Extension
10:38:42Prim_Dijkstra_Simple: theory HOL-Library.Order_Continuity
10:38:42UPF: theory UPF.SeqComposition
10:38:42UPF: theory UPF.ParallelComposition
10:38:42Wetzels_Problem: theory HOL-Cardinals.Wellfounded_More
10:38:42Wetzels_Problem: theory HOL-Cardinals.Wellorder_Relation
10:38:42Twelvefold_Way: theory Card_Partitions.Card_Partitions
10:38:42Prim_Dijkstra_Simple: theory HOL-Library.Extended_Nat
10:38:42Wetzels_Problem: theory HOL-Cardinals.Wellorder_Embedding
10:38:42Wetzels_Problem: theory HOL-Cardinals.Wellorder_Constructions
10:38:43Timing Separation_Logic_Unbounded (4 threads, 30.403s elapsed time, 92.347s cpu time, 8.648s GC time, factor 3.04)
10:38:43Finished Separation_Logic_Unbounded (0:00:32 elapsed time, 0:01:35 cpu time, factor 2.94)
10:38:43Twelvefold_Way: theory Bell_Numbers_Spivey.Bell_Numbers
10:38:43Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Common
10:38:43Wetzels_Problem: theory HOL-Cardinals.Cardinal_Order_Relation
10:38:43Wetzels_Problem: theory HOL-Cardinals.Ordinal_Arithmetic
10:38:43Running pGCL (on 10.195.8.42) ...
10:38:43UPF: theory UPF.Analysis
10:38:43UPF: theory UPF.Normalisation
10:38:43Twelvefold_Way: theory Twelvefold_Way.Preliminaries
10:38:44Prim_Dijkstra_Simple: theory HOL-Data_Structures.RBT
10:38:44Prim_Dijkstra_Simple: theory HOL-Library.While_Combinator
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Chapter_Dijkstra
10:38:44Wetzels_Problem: theory HOL-Cardinals.Cardinal_Arithmetic
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Chapter_Prim
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Directed_Graph
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Undirected_Graph
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Dijkstra_Abstract
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Directed_Graph_Specs
10:38:44Wetzels_Problem: theory HOL-Cardinals.Cardinals
10:38:44Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Directed_Graph_Impl
10:38:44Timing Zeckendorf (8 threads, 2.452s elapsed time, 8.276s cpu time, 0.168s GC time, factor 3.38)
10:38:44Finished Zeckendorf (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.61)
10:38:44Wetzels_Problem: theory ZFC_in_HOL.ZFC_Library
10:38:44Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Core
10:38:44Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry1
10:38:44Wetzels_Problem: theory ZFC_in_HOL.ZFC_in_HOL
10:38:45Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Undirected_Graph_Specs
10:38:45Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Prim_Abstract
10:38:45Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry2
10:38:45Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Undirected_Graph_Impl
10:38:45Wetzels_Problem: theory ZFC_in_HOL.ZFC_Cardinals
10:38:45Twelvefold_Way: theory Twelvefold_Way.Equiv_Relations_on_Functions
10:38:45Twelvefold_Way: theory Twelvefold_Way.Card_Bijections_Direct
10:38:45Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry10
10:38:45Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry4
10:38:45Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry5
10:38:45Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry7
10:38:45UPF: theory UPF.NormalisationTestSpecification
10:38:45pGCL: theory pGCL.Misc
10:38:46Wetzels_Problem: theory ZFC_in_HOL.ZFC_Typeclasses
10:38:46Timing Synthetic_Completeness (8 threads, 6.502s elapsed time, 37.674s cpu time, 4.177s GC time, factor 5.79)
10:38:46Finished Synthetic_Completeness (0:00:07 elapsed time, 0:00:39 cpu time, factor 5.26)
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry6
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry8
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry9
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry11
10:38:46Prim_Dijkstra_Simple: theory HOL-Data_Structures.RBT_Set
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry12
10:38:46Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way_Entry3
10:38:46Twelvefold_Way: theory Twelvefold_Way.Card_Bijections
10:38:46pGCL: theory pGCL.Expectations
10:38:46Wetzels_Problem: theory ZFC_in_HOL.General_Cardinals
10:38:46Wetzels_Problem: theory Wetzels_Problem.Wetzels_Problem
10:38:47Twelvefold_Way: theory Twelvefold_Way.Twelvefold_Way
10:38:47UPF: theory UPF.UPF
10:38:47UPF: theory UPF.Service
10:38:47Prim_Dijkstra_Simple: theory HOL-Data_Structures.RBT_Map
10:38:47pGCL: theory pGCL.Transformers
10:38:47Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Dijkstra_Impl
10:38:47Prim_Dijkstra_Simple: theory Prim_Dijkstra_Simple.Prim_Impl
10:38:48Timing Types_Tableaus_and_Goedels_God (8 threads, 8.010s elapsed time, 11.490s cpu time, 0.446s GC time, factor 1.43)
10:38:48Timing Youngs_Inequality (8 threads, 5.945s elapsed time, 10.703s cpu time, 0.691s GC time, factor 1.80)
10:38:48Finished Types_Tableaus_and_Goedels_God (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.39)
10:38:48Finished Youngs_Inequality (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.65)
10:38:48pGCL: theory pGCL.Induction
10:38:49pGCL: theory pGCL.Embedding
10:38:49pGCL: theory pGCL.Healthiness
10:38:50pGCL: theory pGCL.Continuity
10:38:50pGCL: theory pGCL.LoopInduction
10:38:50Timing Randomised_Social_Choice (4 threads, 16.860s elapsed time, 56.570s cpu time, 5.470s GC time, factor 3.36)
10:38:50Finished Randomised_Social_Choice (0:00:46 elapsed time, 0:01:37 cpu time, factor 2.10)
10:38:51pGCL: theory pGCL.Sublinearity
10:38:51pGCL: theory pGCL.WellDefined
10:38:51Timing Random_BSTs (8 threads, 3.858s elapsed time, 7.812s cpu time, 0.847s GC time, factor 2.02)
10:38:51Finished Random_BSTs (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.62)
10:38:51pGCL: theory pGCL.Algebra
10:38:52pGCL: theory pGCL.Determinism
10:38:52pGCL: theory pGCL.Loops
10:38:52Timing Wetzels_Problem (8 threads, 10.076s elapsed time, 55.135s cpu time, 2.921s GC time, factor 5.47)
10:38:52Finished Wetzels_Problem (0:00:11 elapsed time, 0:00:57 cpu time, factor 5.02)
10:38:52pGCL: theory pGCL.StructuredReasoning
10:38:53pGCL: theory pGCL.Automation
10:38:53pGCL: theory pGCL.Termination
10:38:54UPF: theory UPF.ServiceExample
10:38:54pGCL: theory pGCL.pGCL
10:38:55pGCL: theory pGCL.LoopExamples
10:38:55pGCL: theory pGCL.Monty
10:38:55pGCL: theory pGCL.Primitives
10:38:56Timing Prim_Dijkstra_Simple (8 threads, 16.966s elapsed time, 70.355s cpu time, 4.565s GC time, factor 4.15)
10:38:56Finished Prim_Dijkstra_Simple (0:00:18 elapsed time, 0:01:11 cpu time, factor 3.99)
10:38:57Timing Saturation_Framework (4 threads, 24.978s elapsed time, 62.105s cpu time, 4.949s GC time, factor 2.49)
10:38:57Finished Saturation_Framework (0:00:47 elapsed time, 0:01:33 cpu time, factor 1.96)
10:38:59Timing UPF (8 threads, 15.152s elapsed time, 41.350s cpu time, 5.156s GC time, factor 2.73)
10:38:59Finished UPF (0:00:20 elapsed time, 0:00:50 cpu time, factor 2.50)
10:39:05Running UPF_Firewall (on of1-proof) ...
10:39:05Running Randomised_BSTs (on of1-proof) ...
10:39:06Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
10:39:06Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
10:39:07UPF_Firewall: theory UPF_Firewall.NetworkCore
10:39:07UPF_Firewall: theory UPF_Firewall.LTL_alike
10:39:07UPF_Firewall: theory UPF_Firewall.Ports
10:39:07UPF_Firewall: theory UPF_Firewall.DatatypeAddress
10:39:07UPF_Firewall: theory UPF_Firewall.IPv4
10:39:07UPF_Firewall: theory UPF_Firewall.DatatypePort
10:39:07UPF_Firewall: theory UPF_Firewall.IntegerAddress
10:39:07UPF_Firewall: theory UPF_Firewall.IntegerPort
10:39:07UPF_Firewall: theory UPF_Firewall.IntegerPort_TCPUDP
10:39:07UPF_Firewall: theory UPF_Firewall.PolicyCore
10:39:07UPF_Firewall: theory UPF_Firewall.IPv4_TCPUDP
10:39:08UPF_Firewall: theory UPF_Firewall.PolicyCombinators
10:39:08UPF_Firewall: theory UPF_Firewall.PortCombinators
10:39:08UPF_Firewall: theory UPF_Firewall.ProtocolPortCombinators
10:39:08UPF_Firewall: theory UPF_Firewall.NetworkModels
10:39:08Timing Real_Impl (4 threads, 61.272s elapsed time, 151.270s cpu time, 10.880s GC time, factor 2.47)
10:39:08Finished Real_Impl (0:01:03 elapsed time, 0:02:33 cpu time, factor 2.43)
10:39:08UPF_Firewall: theory UPF_Firewall.PacketFilter
10:39:08UPF_Firewall: theory UPF_Firewall.FWNormalisationCore
10:39:08UPF_Firewall: theory UPF_Firewall.NAT
10:39:08UPF_Firewall: theory UPF_Firewall.StatefulCore
10:39:08UPF_Firewall: theory UPF_Firewall.FTP
10:39:08UPF_Firewall: theory UPF_Firewall.VOIP
10:39:10Timing pGCL (4 threads, 23.160s elapsed time, 83.829s cpu time, 3.639s GC time, factor 3.62)
10:39:10Finished pGCL (0:00:25 elapsed time, 0:01:26 cpu time, factor 3.35)
10:39:10UPF_Firewall: theory UPF_Firewall.FTP_WithPolicy
10:39:10Timing Randomised_BSTs (8 threads, 3.703s elapsed time, 11.852s cpu time, 0.476s GC time, factor 3.20)
10:39:10Finished Randomised_BSTs (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.60)
10:39:10UPF_Firewall: theory UPF_Firewall.FTPVOIP
10:39:13Running Saturation_Framework_Extensions (on of2.proof.cit.tum.de) ...
10:39:13Running Given_Clause_Loops (on of2.proof.cit.tum.de) ...
10:39:13Running SDS_Impossibility (on of2.proof.cit.tum.de) ...
10:39:13Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Soundness
10:39:13Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited
10:39:13Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
10:39:13UPF_Firewall: theory UPF_Firewall.ElementaryRules
10:39:13UPF_Firewall: theory UPF_Firewall.NormalisationGenericProofs
10:39:13SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
10:39:13Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Clausal_Calculus
10:39:13UPF_Firewall: theory UPF_Firewall.NormalisationIntegerPortProof
10:39:14UPF_Firewall: theory UPF_Firewall.StatefulFW
10:39:14Given_Clause_Loops: theory Abstract-Rewriting.Seq
10:39:14Given_Clause_Loops: theory Regular-Sets.Regular_Set
10:39:14Given_Clause_Loops: theory Given_Clause_Loops.More_Given_Clause_Architectures
10:39:14Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited
10:39:14UPF_Firewall: theory UPF_Firewall.NormalisationIPPProofs
10:39:15UPF_Firewall: theory UPF_Firewall.FWNormalisation
10:39:15UPF_Firewall: theory UPF_Firewall.UPF-Firewall
10:39:15UPF_Firewall: theory UPF_Firewall.DMZDatatype
10:39:15UPF_Firewall: theory UPF_Firewall.DMZInteger
10:39:15UPF_Firewall: theory UPF_Firewall.DMZ
10:39:15UPF_Firewall: theory UPF_Firewall.NAT-FW
10:39:16Given_Clause_Loops: theory Regular-Sets.Regular_Exp
10:39:16UPF_Firewall: theory UPF_Firewall.PersonalFirewallDatatype
10:39:16UPF_Firewall: theory UPF_Firewall.PersonalFirewallInt
10:39:16UPF_Firewall: theory UPF_Firewall.PersonalFirewallIpv4
10:39:16UPF_Firewall: theory UPF_Firewall.Transformation01
10:39:16UPF_Firewall: theory UPF_Firewall.PersonalFirewall
10:39:16UPF_Firewall: theory UPF_Firewall.Transformation02
10:39:16UPF_Firewall: theory UPF_Firewall.Voice_over_IP
10:39:16UPF_Firewall: theory UPF_Firewall.Transformation
10:39:16UPF_Firewall: theory UPF_Firewall.Examples
10:39:17Timing Twelvefold_Way (8 threads, 36.598s elapsed time, 102.766s cpu time, 5.030s GC time, factor 2.81)
10:39:17Finished Twelvefold_Way (0:00:37 elapsed time, 0:01:44 cpu time, factor 2.76)
10:39:17Given_Clause_Loops: theory Regular-Sets.NDerivative
10:39:17Given_Clause_Loops: theory Regular-Sets.Relation_Interpretation
10:39:19Given_Clause_Loops: theory Regular-Sets.Equivalence_Checking
10:39:19Given_Clause_Loops: theory Regular-Sets.Regexp_Method
10:39:19Given_Clause_Loops: theory Abstract-Rewriting.Abstract_Rewriting
10:39:20Timing Saturation_Framework_Extensions (8 threads, 6.248s elapsed time, 19.405s cpu time, 1.384s GC time, factor 3.11)
10:39:20Finished Saturation_Framework_Extensions (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.76)
10:39:21Given_Clause_Loops: theory Weighted_Path_Order.Relations
10:39:21Given_Clause_Loops: theory Weighted_Path_Order.Multiset_Extension_Pair
10:39:22Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops_Util
10:39:22Given_Clause_Loops: theory Given_Clause_Loops.Prover_Queue
10:39:22Given_Clause_Loops: theory Given_Clause_Loops.DISCOUNT_Loop
10:39:22Given_Clause_Loops: theory Given_Clause_Loops.Otter_Loop
10:39:22Given_Clause_Loops: theory Given_Clause_Loops.Prover_Lazy_List_Queue
10:39:24Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Def
10:39:24Given_Clause_Loops: theory Given_Clause_Loops.Fair_DISCOUNT_Loop
10:39:24Given_Clause_Loops: theory Given_Clause_Loops.Zipperposition_Loop
10:39:24Given_Clause_Loops: theory Given_Clause_Loops.iProver_Loop
10:39:25Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop
10:39:25Given_Clause_Loops: theory Given_Clause_Loops.Fair_iProver_Loop
10:39:26Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Complete
10:39:27Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts
10:39:27Timing SDS_Impossibility (8 threads, 13.404s elapsed time, 49.069s cpu time, 3.988s GC time, factor 3.66)
10:39:27Finished SDS_Impossibility (0:00:14 elapsed time, 0:00:50 cpu time, factor 3.43)
10:39:29Timing UPF_Firewall (8 threads, 22.091s elapsed time, 85.506s cpu time, 9.064s GC time, factor 3.87)
10:39:29Finished UPF_Firewall (0:00:23 elapsed time, 0:01:28 cpu time, factor 3.79)
10:39:30Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops
10:39:31Timing Given_Clause_Loops (8 threads, 16.875s elapsed time, 74.894s cpu time, 5.377s GC time, factor 4.44)
10:39:31Finished Given_Clause_Loops (0:00:18 elapsed time, 0:01:17 cpu time, factor 4.23)
10:39:51Timing Real_Time_Deque (4 threads, 102.486s elapsed time, 270.766s cpu time, 9.444s GC time, factor 2.64)
10:39:51Finished Real_Time_Deque (0:01:44 elapsed time, 0:04:33 cpu time, factor 2.62)
10:39:51Timing Resolution_FOL (4 threads, 102.099s elapsed time, 212.271s cpu time, 11.369s GC time, factor 2.08)
10:39:51Finished Resolution_FOL (0:01:44 elapsed time, 0:03:35 cpu time, factor 2.07)
10:43:00Timing Modular_arithmetic_LLL_and_HNF_algorithms (4 threads, 1077.009s elapsed time, 3622.021s cpu time, 480.287s GC time, factor 3.36)
10:43:00Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:18:06 elapsed time, 1:00:46 cpu time, factor 3.36)
10:49:16Timing CZH_Universal_Constructions (4 threads, 1831.124s elapsed time, 4443.096s cpu time, 295.133s GC time, factor 2.43)
10:49:16Finished CZH_Universal_Constructions (0:30:36 elapsed time, 1:14:13 cpu time, factor 2.43)
10:49:2810:49:28Finished at Mon Dec 11 10:49:28 GMT+1 2023
10:49:281:01:08 elapsed time, 51:14:48 cpu time, factor 50.28
10:49:29Started calculate disk usage of build
10:49:30Finished Calculation of disk usage of build in 0 seconds
10:49:31Started calculate disk usage of workspace
10:49:34Finished Calculation of disk usage of workspace in 2 second
10:49:35Finished: SUCCESS
![[Jenkins]](/jenkins/static/21caf10b/images/svgs/logo.svg){kind=logo}
