Skipping 889 KB.. Full Log

Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
20:11:54 Running Lam-ml-Normalization (on 10.195.8.29+2) ...
20:11:54 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
20:11:56 Nash_Williams: theory HOL-Library.Countable_Set
20:11:56 Lam-ml-Normalization: theory HOL-Library.LaTeXsugar
20:11:56 Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
20:11:57 Nash_Williams: theory Nash_Williams.Nash_Extras
20:11:58 Running OpSets (on 10.195.8.42+3) ...
20:11:59 Nash_Williams: theory Nash_Williams.Nash_Williams
20:11:59 Running Standard_Borel_Spaces (on 10.195.6.179+2) ...
20:11:59 OpSets: theory OpSets.OpSet
20:11:59 Timing Boolean_Expression_Checkers (2 threads, 24.166s elapsed time, 24.136s cpu time, 4.126s GC time, factor 1.00)
20:11:59 Finished Boolean_Expression_Checkers (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.99)
20:11:59 Timing Zeta_3_Irrational (8 threads, 8.608s elapsed time, 55.211s cpu time, 2.443s GC time, factor 6.41)
20:11:59 Finished Zeta_3_Irrational (0:00:10 elapsed time, 0:00:57 cpu time, factor 5.51)
20:12:00 OpSets: theory OpSets.Insert_Spec
20:12:01 Running Separata (on of2.proof.cit.tum.de+3) ...
20:12:01 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Lemmas_StandardBorel
20:12:02 Separata: theory HOL-Eisbach.Eisbach
20:12:02 Separata: theory Separation_Algebra.Separation_Algebra
20:12:02 OpSets: theory OpSets.Interleaving
20:12:03 OpSets: theory OpSets.List_Spec
20:12:03 Separata: theory HOL-Eisbach.Eisbach_Tools
20:12:04 OpSets: theory OpSets.RGA
20:12:04 Separata: theory Separata.Separata
20:12:06 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Space
20:12:09 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Set_Based_Metric_Product
20:12:10 Standard_Borel_Spaces: theory Standard_Borel_Spaces.Abstract_Metrizable_Topology
20:12:11 Timing Sliding_Window_Algorithm (2 threads, 39.574s elapsed time, 39.547s cpu time, 0.911s GC time, factor 1.00)
20:12:11 Finished Sliding_Window_Algorithm (0:00:41 elapsed time, 0:00:41 cpu time, factor 0.99)
20:12:11 Standard_Borel_Spaces: theory Standard_Borel_Spaces.StandardBorel
20:12:13 Timing Separata (6 threads, 9.909s elapsed time, 9.908s cpu time, 0.371s GC time, factor 1.00)
20:12:13 Finished Separata (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.97)
20:12:14 Timing Lam-ml-Normalization (2 threads, 17.292s elapsed time, 17.291s cpu time, 0.807s GC time, factor 1.00)
20:12:14 Finished Lam-ml-Normalization (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
20:12:18 Timing Generic_Join (2 threads, 58.495s elapsed time, 58.439s cpu time, 3.477s GC time, factor 1.00)
20:12:18 Finished Generic_Join (0:01:00 elapsed time, 0:01:00 cpu time, factor 0.99)
20:12:22 Running PLM (on of1-proof+0-7) ...
20:12:23 PLM: theory HOL-Eisbach.Eisbach
20:12:23 PLM: theory HOL-Library.LaTeXsugar
20:12:23 PLM: theory PLM.TAO_1_Embedding
20:12:23 PLM: theory HOL-Library.OptionalSugar
20:12:23 Running Combinatorial_Enumeration_Algorithms (on 10.195.8.32+1) ...
20:12:23 PLM: theory HOL-Eisbach.Eisbach_Tools
20:12:24 PLM: theory PLM.TAO_2_Semantics
20:12:24 PLM: theory PLM.TAO_3_Quantifiable
20:12:24 PLM: theory PLM.TAO_4_BasicDefinitions
20:12:24 PLM: theory PLM.TAO_5_MetaSolver
20:12:25 PLM: theory PLM.TAO_6_Identifiable
20:12:25 PLM: theory PLM.TAO_7_Axioms
20:12:25 PLM: theory PLM.TAO_8_Definitions
20:12:25 Running Rewriting_Z (on 10.195.8.11+2) ...
20:12:25 PLM: theory PLM.TAO_98_ArtificialTheorems
20:12:25 PLM: theory PLM.TAO_99_SanityTests
20:12:26 Combinatorial_Enumeration_Algorithms: theory HOL-Eisbach.Eisbach
20:12:26 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Filter_Bool_List
20:12:26 PLM: theory PLM.TAO_9_PLM
20:12:27 Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Stirling
20:12:28 Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Transposition
20:12:28 Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Additions_to_Main
20:12:28 PLM: theory PLM.TAO_10_PossibleWorlds
20:12:28 Combinatorial_Enumeration_Algorithms: theory Card_Partitions.Injectivity_Solver
20:12:28 PLM: theory PLM.TAO_99_Paradox
20:12:29 Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Number_Partition
20:12:29 PLM: theory PLM.Thesis
20:12:30 Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Card_Number_Partitions
20:12:30 Running Consensus_Refined (on 10.195.8.29+1) ...
20:12:30 Rewriting_Z: theory HOL-Eisbach.Eisbach
20:12:30 Rewriting_Z: theory Abstract-Rewriting.Seq
20:12:30 Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Permutations
20:12:30 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Common_Lemmas
20:12:31 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Integer_Compositions
20:12:31 Consensus_Refined: theory Consensus_Refined.Consensus_Misc
20:12:31 Consensus_Refined: theory Consensus_Refined.Consensus_Types
20:12:31 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Integer_Partitions
20:12:31 Rewriting_Z: theory HOL-Library.While_Combinator
20:12:31 Consensus_Refined: theory Consensus_Refined.Quorums
20:12:31 Rewriting_Z: theory Regular-Sets.Regular_Set
20:12:31 Timing PLM (8 threads, 7.664s elapsed time, 32.822s cpu time, 3.174s GC time, factor 4.28)
20:12:31 Finished PLM (0:00:08 elapsed time, 0:00:34 cpu time, factor 3.87)
20:12:32 Consensus_Refined: theory Consensus_Refined.Infra
20:12:32 Consensus_Refined: theory Consensus_Refined.Refinement
20:12:32 Consensus_Refined: theory Consensus_Refined.Three_Steps
20:12:32 Consensus_Refined: theory Consensus_Refined.Two_Steps
20:12:32 Consensus_Refined: theory HOL-Library.Infinite_Set
20:12:33 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Sequences
20:12:33 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Trees
20:12:33 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Powerset
20:12:33 Combinatorial_Enumeration_Algorithms: theory Discrete_Summation.Factorials
20:12:34 Consensus_Refined: theory HOL-Library.Omega_Words_Fun
20:12:34 Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Multiset_Permutations
20:12:34 Combinatorial_Enumeration_Algorithms: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
20:12:35 Timing Commuting_Hermitian (6 threads, 35.118s elapsed time, 35.109s cpu time, 2.056s GC time, factor 1.00)
20:12:35 Finished Commuting_Hermitian (0:00:49 elapsed time, 0:00:48 cpu time, factor 0.99)
20:12:35 Timing Nash_Williams (2 threads, 47.923s elapsed time, 47.875s cpu time, 1.393s GC time, factor 1.00)
20:12:35 Consensus_Refined: theory Heard_Of.HOModel
20:12:35 Finished Nash_Williams (0:00:50 elapsed time, 0:00:49 cpu time, factor 0.99)
20:12:35 Rewriting_Z: theory Regular-Sets.Regular_Exp
20:12:36 Consensus_Refined: theory Consensus_Refined.Voting
20:12:36 Running Ceva (on of2.proof.cit.tum.de+3) ...
20:12:36 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Derangements_Enum
20:12:37 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Weak_Integer_Compositions
20:12:37 Consensus_Refined: theory Consensus_Refined.Same_Vote
20:12:38 Ceva: theory Triangle.Angles
20:12:38 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Permutations
20:12:38 Consensus_Refined: theory Consensus_Refined.MRU_Vote
20:12:38 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Subsets
20:12:38 Consensus_Refined: theory Consensus_Refined.MRU_Vote_Opt
20:12:38 Ceva: theory Triangle.Triangle
20:12:38 Running VerifyThis2019 (on 10.195.8.40+1) ...
20:12:39 Consensus_Refined: theory Consensus_Refined.Observing_Quorums
20:12:40 Ceva: theory Ceva.Ceva
20:12:40 Consensus_Refined: theory Consensus_Refined.Three_Step_MRU
20:12:40 Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Combinatorial_Enumeration_Algorithms
20:12:40 Consensus_Refined: theory Consensus_Refined.Observing_Quorums_Opt
20:12:41 VerifyThis2019: theory VerifyThis2019.Exc_Nres_Monad
20:12:41 Consensus_Refined: theory Consensus_Refined.Voting_Opt
20:12:41 Consensus_Refined: theory Consensus_Refined.Two_Step_Observing
20:12:42 Running Finger-Trees (on 10.195.7.194+3) ...
20:12:42 Consensus_Refined: theory Consensus_Refined.Ate_Defs
20:12:43 Rewriting_Z: theory Regular-Sets.NDerivative
20:12:43 Consensus_Refined: theory Consensus_Refined.BenOr_Defs
20:12:43 Rewriting_Z: theory Regular-Sets.Relation_Interpretation
20:12:44 Consensus_Refined: theory Consensus_Refined.CT_Defs
20:12:44 Finger-Trees: theory Finger-Trees.FingerTree
20:12:45 Timing Ceva (6 threads, 6.438s elapsed time, 6.428s cpu time, 0.219s GC time, factor 1.00)
20:12:45 Finished Ceva (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.96)
20:12:45 Timing OpSets (2 threads, 44.926s elapsed time, 44.867s cpu time, 1.156s GC time, factor 1.00)
20:12:45 Finished OpSets (0:00:47 elapsed time, 0:00:46 cpu time, factor 0.99)
20:12:46 VerifyThis2019: theory VerifyThis2019.VTcomp
20:12:46 Consensus_Refined: theory Consensus_Refined.HO_Transition_System
20:12:48 Consensus_Refined: theory Consensus_Refined.New_Algorithm_Defs
20:12:49 Consensus_Refined: theory Consensus_Refined.OneThirdRule_Defs
20:12:50 Consensus_Refined: theory Consensus_Refined.Paxos_Defs
20:12:50 Consensus_Refined: theory Consensus_Refined.Uv_Defs
20:12:51 Rewriting_Z: theory Regular-Sets.Equivalence_Checking
20:12:52 Rewriting_Z: theory Regular-Sets.Regexp_Method
20:12:52 VerifyThis2019: theory VerifyThis2019.Parallel_Multiset_Fold
20:12:52 VerifyThis2019: theory VerifyThis2019.Challenge1A
20:12:53 VerifyThis2019: theory VerifyThis2019.Challenge3
20:12:54 Consensus_Refined: theory Heard_Of.Majorities
20:12:54 Consensus_Refined: theory Stuttering_Equivalence.Samplers
20:12:54 Consensus_Refined: theory Consensus_Refined.Ate_Proofs
20:12:54 Rewriting_Z: theory Abstract-Rewriting.Abstract_Rewriting
20:12:54 Running Finite_Automata_HF (on 10.195.8.30+0) ...
20:12:55 VerifyThis2019: theory VerifyThis2019.Challenge1B
20:12:56 Finite_Automata_HF: theory HOL-Library.Nat_Bijection
20:12:56 Finite_Automata_HF: theory Regular-Sets.Regular_Set
20:12:56 Consensus_Refined: theory Consensus_Refined.CT_Proofs
20:12:56 VerifyThis2019: theory VerifyThis2019.Challenge2A
20:12:57 Consensus_Refined: theory Consensus_Refined.New_Algorithm_Proofs
20:12:57 Finite_Automata_HF: theory HereditarilyFinite.HF
20:12:58 Consensus_Refined: theory Consensus_Refined.OneThirdRule_Proofs
20:12:59 Consensus_Refined: theory Consensus_Refined.Paxos_Proofs
20:13:00 Rewriting_Z: theory Rewriting_Z.Z
20:13:00 Consensus_Refined: theory Stuttering_Equivalence.StutterEquivalence
20:13:00 Finite_Automata_HF: theory HereditarilyFinite.Ordinal
20:13:00 Rewriting_Z: theory Rewriting_Z.CL_Z
20:13:00 Consensus_Refined: theory Heard_Of.Reduction
20:13:00 Finite_Automata_HF: theory Regular-Sets.Regular_Exp
20:13:01 Rewriting_Z: theory Rewriting_Z.Lambda_Z
20:13:03 Consensus_Refined: theory Consensus_Refined.BenOr_Proofs
20:13:03 Consensus_Refined: theory Consensus_Refined.Uv_Proofs
20:13:03 Estimated 0:11:46 build time with path time heuristic (critical: absolute time (0:05:00), parallel: time based threads, fast hosts: per critical node) (took 6.702s)
20:13:03 Running Schutz_Spacetime (on of1-proof+8-15) ...
20:13:04 Schutz_Spacetime: theory Schutz_Spacetime.Util
20:13:04 Schutz_Spacetime: theory Schutz_Spacetime.TernaryOrdering
20:13:04 Schutz_Spacetime: theory Schutz_Spacetime.Minkowski
20:13:06 Schutz_Spacetime: theory Schutz_Spacetime.TemporalOrderOnPath
20:13:07 VerifyThis2019: theory VerifyThis2019.Challenge2B
20:13:08 Running Old_Datatype_Show (on 10.195.8.11+3) ...
20:13:10 Finger-Trees: theory Finger-Trees.Test
20:13:11 Finite_Automata_HF: theory Finite_Automata_HF.Finite_Automata_HF
20:13:11 Running Fermat3_4 (on 10.195.8.46+4) ...
20:13:11 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
20:13:12 Timing Monad_Memo_DP (6 threads, 319.056s elapsed time, 318.980s cpu time, 80.076s GC time, factor 1.00)
20:13:12 Finished Monad_Memo_DP (0:05:38 elapsed time, 0:05:37 cpu time, factor 1.00)
20:13:13 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
20:13:13 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
20:13:13 Timing Finger-Trees (2 threads, 27.759s elapsed time, 27.736s cpu time, 2.571s GC time, factor 1.00)
20:13:13 Finished Finger-Trees (0:00:31 elapsed time, 0:00:30 cpu time, factor 0.99)
20:13:14 Fermat3_4: theory Fermat3_4.Fermat4
20:13:14 Fermat3_4: theory Fermat3_4.Quad_Form
20:13:15 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
20:13:16 Fermat3_4: theory Fermat3_4.Fermat3
20:13:16 Running SenSocialChoice (on 10.195.8.42+3) ...
20:13:16 Timing Combinatorial_Enumeration_Algorithms (2 threads, 49.192s elapsed time, 49.160s cpu time, 1.701s GC time, factor 1.00)
20:13:16 Finished Combinatorial_Enumeration_Algorithms (0:00:52 elapsed time, 0:00:52 cpu time, factor 0.99)
20:13:18 SenSocialChoice: theory SenSocialChoice.FSext
20:13:18 SenSocialChoice: theory SenSocialChoice.RPRs
20:13:18 Running FOL_Seq_Calc3 (on of2.proof.cit.tum.de+3) ...
20:13:19 SenSocialChoice: theory SenSocialChoice.SCFs
20:13:20 FOL_Seq_Calc3: theory Collections.ICF_Tools
20:13:20 FOL_Seq_Calc3: theory FOL_Seq_Calc3.List_Syntax
20:13:20 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Fair_Stream
20:13:20 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Syntax
20:13:20 FOL_Seq_Calc3: theory Collections.Ord_Code_Preproc
20:13:20 SenSocialChoice: theory SenSocialChoice.Arrow
20:13:20 FOL_Seq_Calc3: theory Collections.Locale_Code
20:13:21 FOL_Seq_Calc3: theory Abstract_Completeness.Abstract_Completeness
20:13:21 SenSocialChoice: theory SenSocialChoice.May
20:13:21 Timing Schutz_Spacetime (8 threads, 16.155s elapsed time, 105.847s cpu time, 7.325s GC time, factor 6.55)
20:13:21 Finished Schutz_Spacetime (0:00:17 elapsed time, 0:01:48 cpu time, factor 6.10)
20:13:22 SenSocialChoice: theory SenSocialChoice.Sen
20:13:23 Timing VerifyThis2019 (2 threads, 40.124s elapsed time, 34.382s cpu time, 1.008s GC time, factor 0.86)
20:13:23 Finished VerifyThis2019 (0:00:43 elapsed time, 0:00:37 cpu time, factor 0.86)
20:13:23 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Semantics
20:13:23 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Encoding
20:13:24 Timing Old_Datatype_Show (2 threads, 12.363s elapsed time, 12.264s cpu time, 1.373s GC time, factor 0.99)
20:13:24 Finished Old_Datatype_Show (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.96)
20:13:24 Running IO_Language_Conformance (on 10.195.7.194+4) ...
20:13:26 FOL_Seq_Calc3: theory Abstract_Soundness.Finite_Proof_Soundness
20:13:26 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Prover
20:13:27 IO_Language_Conformance: theory IO_Language_Conformance.Input_Output_Language_Conformance
20:13:28 Timing Rewriting_Z (2 threads, 58.445s elapsed time, 58.417s cpu time, 4.064s GC time, factor 1.00)
20:13:28 Finished Rewriting_Z (0:01:01 elapsed time, 0:01:00 cpu time, factor 0.99)
20:13:28 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Completeness
20:13:28 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Export
20:13:28 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Soundness
20:13:29 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Result
20:13:33 Timing FOL_Seq_Calc3 (6 threads, 11.906s elapsed time, 11.898s cpu time, 0.452s GC time, factor 1.00)
20:13:33 Finished FOL_Seq_Calc3 (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
20:13:39 Building Incompleteness (on of4.proof.cit.tum.de+9-12) ...
20:13:39 Incompleteness: theory FinFun.FinFun
20:13:39 Running Hybrid_Multi_Lane_Spatial_Logic (on of1-proof+0-7) ...
20:13:40 Running Optimal_BST (on of3.proof.cit.tum.de+6) ...
20:13:40 Incompleteness: theory Nominal2.Nominal2_Base
20:13:40 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Cars
20:13:40 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.NatInt
20:13:40 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.RealInt
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Traffic
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Views
20:13:41 Optimal_BST: theory Optimal_BST.Optimal_BST_Examples
20:13:41 Optimal_BST: theory Optimal_BST.Weighted_Path_Length
20:13:41 Optimal_BST: theory Optimal_BST.Quadrilateral_Inequality
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Move
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Restriction
20:13:41 Timing Finite_Automata_HF (2 threads, 44.348s elapsed time, 44.169s cpu time, 2.371s GC time, factor 1.00)
20:13:41 Finished Finite_Automata_HF (0:00:46 elapsed time, 0:00:46 cpu time, factor 0.99)
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Sensors
20:13:41 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Length
20:13:42 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL
20:13:42 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Perfect_Sensors
20:13:42 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Regular_Sensors
20:13:43 Incompleteness: theory Nominal2.Nominal2_Abs
20:13:43 Running PAL (on 10.195.8.32+0) ...
20:13:43 Optimal_BST: theory Optimal_BST.Optimal_BST
20:13:43 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Perfect
20:13:43 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Regular
20:13:43 Incompleteness: theory Nominal2.Nominal2_FCB
20:13:43 Incompleteness: theory Nominal2.Nominal2
20:13:43 Running JiveDataStoreModel (on 10.195.8.11+1) ...
20:13:43 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Perfect
20:13:44 Hybrid_Multi_Lane_Spatial_Logic: theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Regular
20:13:45 PAL: theory PAL.PAL
20:13:46 JiveDataStoreModel: theory JiveDataStoreModel.TypeIds
20:13:46 Incompleteness: theory Incompleteness.SyntaxN
20:13:47 Optimal_BST: theory Optimal_BST.Optimal_BST_Memo
20:13:47 Timing Fermat3_4 (2 threads, 31.583s elapsed time, 31.533s cpu time, 0.740s GC time, factor 1.00)
20:13:47 Finished Fermat3_4 (0:00:34 elapsed time, 0:00:34 cpu time, factor 0.99)
20:13:47 Optimal_BST: theory Optimal_BST.Optimal_BST2
20:13:49 JiveDataStoreModel: theory JiveDataStoreModel.JavaType
20:13:49 Incompleteness: theory Incompleteness.Coding
20:13:49 Incompleteness: theory Incompleteness.Predicates
20:13:50 Optimal_BST: theory Optimal_BST.Optimal_BST_Code
20:13:51 Incompleteness: theory Incompleteness.Sigma
20:13:52 JiveDataStoreModel: theory JiveDataStoreModel.DirectSubtypes
20:13:52 JiveDataStoreModel: theory JiveDataStoreModel.Subtype
20:13:52 JiveDataStoreModel: theory JiveDataStoreModel.Attributes
20:13:52 JiveDataStoreModel: theory JiveDataStoreModel.Value
20:13:54 Running Binomial-Heaps (on of2.proof.cit.tum.de+3) ...
20:13:54 Incompleteness: theory Incompleteness.Coding_Predicates
20:13:55 Binomial-Heaps: theory Binomial-Heaps.BinomialHeap
20:13:55 Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap
20:13:56 JiveDataStoreModel: theory JiveDataStoreModel.AttributesIndep
20:13:56 JiveDataStoreModel: theory JiveDataStoreModel.Location
20:13:56 Timing Standard_Borel_Spaces (2 threads, 112.535s elapsed time, 112.512s cpu time, 2.745s GC time, factor 1.00)
20:13:56 Finished Standard_Borel_Spaces (0:01:56 elapsed time, 0:01:55 cpu time, factor 1.00)
20:13:56 Timing SenSocialChoice (2 threads, 37.418s elapsed time, 37.341s cpu time, 1.281s GC time, factor 1.00)
20:13:56 Finished SenSocialChoice (0:00:39 elapsed time, 0:00:39 cpu time, factor 0.99)
20:13:57 Running Finitely_Generated_Abelian_Groups (on 10.195.8.40+1) ...
20:13:58 Incompleteness: theory Incompleteness.Functions
20:13:58 Incompleteness: theory Incompleteness.Pf_Predicates
20:13:58 JiveDataStoreModel: theory JiveDataStoreModel.Store
20:13:58 Timing Hybrid_Multi_Lane_Spatial_Logic (8 threads, 17.016s elapsed time, 73.615s cpu time, 4.870s GC time, factor 4.33)
20:13:58 Finished Hybrid_Multi_Lane_Spatial_Logic (0:00:18 elapsed time, 0:01:15 cpu time, factor 4.11)
20:13:59 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
20:13:59 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
20:14:00 Timing Consensus_Refined (2 threads, 86.645s elapsed time, 86.612s cpu time, 5.347s GC time, factor 1.00)
20:14:00 Finished Consensus_Refined (0:01:29 elapsed time, 0:01:29 cpu time, factor 1.00)
20:14:00 Incompleteness: theory Incompleteness.Goedel_I
20:14:00 Incompleteness: theory Incompleteness.II_Prelims
20:14:00 JiveDataStoreModel: theory JiveDataStoreModel.StoreProperties
20:14:01 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom
20:14:01 Timing Optimal_BST (6 threads, 18.334s elapsed time, 18.334s cpu time, 0.443s GC time, factor 1.00)
20:14:01 Finished Optimal_BST (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
20:14:01 JiveDataStoreModel: theory JiveDataStoreModel.JML
20:14:02 Timing IO_Language_Conformance (2 threads, 33.539s elapsed time, 33.514s cpu time, 1.080s GC time, factor 1.00)
20:14:02 Finished IO_Language_Conformance (0:00:36 elapsed time, 0:00:36 cpu time, factor 0.99)
20:14:02 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
20:14:02 JiveDataStoreModel: theory JiveDataStoreModel.UnivSpec
20:14:02 Incompleteness: theory Incompleteness.Pseudo_Coding
20:14:02 Incompleteness: theory Incompleteness.Quote
20:14:02 Incompleteness: theory Incompleteness.Goedel_II
20:14:03 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
20:14:04 Timing PAL (2 threads, 18.476s elapsed time, 18.194s cpu time, 0.595s GC time, factor 0.98)
20:14:04 Finished PAL (0:00:20 elapsed time, 0:00:19 cpu time, factor 0.97)
20:14:04 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
20:14:07 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds
20:14:11 Timing JiveDataStoreModel (2 threads, 23.940s elapsed time, 23.842s cpu time, 1.457s GC time, factor 1.00)
20:14:11 Finished JiveDataStoreModel (0:00:26 elapsed time, 0:00:25 cpu time, factor 0.98)
20:14:12 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
20:14:13 Binomial-Heaps: theory Binomial-Heaps.Test
20:14:13 Running AxiomaticCategoryTheory (on 10.195.8.30+3) ...
20:14:13 Running IMO2019 (on of1-proof+8-15) ...
20:14:14 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds
20:14:14 Running Birkhoff_Finite_Distributive_Lattices (on of3.proof.cit.tum.de+6) ...
20:14:14 Timing Binomial-Heaps (6 threads, 18.847s elapsed time, 18.837s cpu time, 1.777s GC time, factor 1.00)
20:14:14 Finished Binomial-Heaps (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
20:14:14 AxiomaticCategoryTheory: theory AxiomaticCategoryTheory.AxiomaticCategoryTheory
20:14:14 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Plus
20:14:14 IMO2019: theory IMO2019.IMO2019_Q5
20:14:14 IMO2019: theory IMO2019.IMO2019_Q1
20:14:14 IMO2019: theory IMO2019.IMO2019_Q4
20:14:15 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations
20:14:15 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Order
20:14:15 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Finite_Lattice
20:14:16 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
20:14:17 Birkhoff_Finite_Distributive_Lattices: theory Birkhoff_Finite_Distributive_Lattices.Birkhoff_Finite_Distributive_Lattices
20:14:17 Running Attack_Trees (on 10.195.8.32+2) ...
20:14:19 Timing IMO2019 (8 threads, 3.752s elapsed time, 6.512s cpu time, 0.435s GC time, factor 1.74)
20:14:19 Finished IMO2019 (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.47)
20:14:20 Attack_Trees: theory Attack_Trees.MC
20:14:21 Running GPU_Kernel_PL (on 10.195.8.46+4) ...
20:14:22 GPU_Kernel_PL: theory GPU_Kernel_PL.Misc
20:14:23 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax
20:14:23 Attack_Trees: theory Attack_Trees.AT
20:14:24 Timing Birkhoff_Finite_Distributive_Lattices (6 threads, 7.587s elapsed time, 7.587s cpu time, 0.300s GC time, factor 1.00)
20:14:24 Finished Birkhoff_Finite_Distributive_Lattices (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.96)
20:14:24 Running Tycon (on 10.195.8.29+1) ...
20:14:26 Tycon: theory Tycon.Coerce
20:14:26 Tycon: theory Tycon.TypeApp
20:14:26 Attack_Trees: theory Attack_Trees.Infrastructure
20:14:27 Tycon: theory Tycon.Functor
20:14:27 Running Formal_Puiseux_Series (on 10.195.8.42+1) ...
20:14:28 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state
20:14:28 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness
20:14:29 Tycon: theory Tycon.Monad
20:14:29 Running TsirelsonBound (on of2.proof.cit.tum.de+2) ...
20:14:30 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Unsorted
20:14:30 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom
20:14:30 Tycon: theory Tycon.Binary_Tree_Monad
20:14:30 Tycon: theory Tycon.Lift_Monad
20:14:30 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread
20:14:30 Running Gaussian_Integers (on 10.195.6.179+0) ...
20:14:30 Tycon: theory Tycon.Monad_Plus
20:14:31 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
20:14:31 Tycon: theory Tycon.Monad_Zero
20:14:32 Tycon: theory Tycon.Error_Monad
20:14:32 Tycon: theory Tycon.Resumption_Transformer
20:14:32 Attack_Trees: theory Attack_Trees.GDPRhealthcare
20:14:33 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group
20:14:33 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers
20:14:33 Gaussian_Integers: theory Matrix.Utility
20:14:33 Tycon: theory Tycon.Error_Transformer
20:14:33 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel
20:14:34 Gaussian_Integers: theory Polynomial_Factorization.Missing_List
20:14:34 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Polynomial
20:14:34 Tycon: theory Tycon.Monad_Zero_Plus
20:14:34 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
20:14:35 Tycon: theory Tycon.Writer_Monad
20:14:35 GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language
20:14:36 Tycon: theory Tycon.Lazy_List_Monad
20:14:36 Running CCS (on 10.195.7.194+2) ...
20:14:36 Tycon: theory Tycon.Maybe_Monad
20:14:37 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
20:14:37 Tycon: theory Tycon.State_Transformer
20:14:37 Timing GPU_Kernel_PL (2 threads, 13.921s elapsed time, 13.919s cpu time, 1.172s GC time, factor 1.00)
20:14:37 Finished GPU_Kernel_PL (0:00:16 elapsed time, 0:00:15 cpu time, factor 0.97)
20:14:37 CCS: theory CCS.Agent
20:14:37 Tycon: theory Tycon.Writer_Transformer
20:14:38 TsirelsonBound: theory TsirelsonBound.Tsirelson
20:14:39 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples
20:14:39 Tycon: theory Tycon.Monad_Transformer
20:14:39 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares
20:14:40 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom_Poly
20:14:40 Gaussian_Integers: theory Polynomial_Factorization.Missing_Multiset
20:14:41 Gaussian_Integers: theory Polynomial_Factorization.Prime_Factorization
20:14:43 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Test
20:14:43 Timing Attack_Trees (2 threads, 22.175s elapsed time, 22.100s cpu time, 1.849s GC time, factor 1.00)
20:14:43 Finished Attack_Trees (0:00:24 elapsed time, 0:00:24 cpu time, factor 0.98)
20:14:44 CCS: theory CCS.Strong_Sim
20:14:44 CCS: theory CCS.Struct_Cong
20:14:44 CCS: theory CCS.Strong_Bisim
20:14:44 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Everything
20:14:44 CCS: theory CCS.Strong_Sim_Pres
20:14:44 CCS: theory CCS.Strong_Bisim_Pres
20:14:45 CCS: theory CCS.Strong_Sim_SC
20:14:45 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Polynomial_Library
20:14:45 CCS: theory CCS.Tau_Chain
20:14:45 CCS: theory CCS.Strong_Bisim_SC
20:14:45 CCS: theory CCS.Weak_Cong_Semantics
20:14:45 CCS: theory CCS.Weak_Semantics
20:14:45 CCS: theory CCS.Weak_Sim
20:14:46 CCS: theory CCS.Weak_Bisim
20:14:46 CCS: theory CCS.Weak_Cong_Sim
20:14:46 CCS: theory CCS.Weak_Cong_Sim_Pres
20:14:46 CCS: theory CCS.Weak_Sim_Pres
20:14:47 CCS: theory CCS.Weak_Cong
20:14:47 CCS: theory CCS.Weak_Bisim_Pres
20:14:47 Timing Tycon (2 threads, 20.391s elapsed time, 20.369s cpu time, 0.768s GC time, factor 1.00)
20:14:47 Finished Tycon (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
20:14:47 CCS: theory CCS.Weak_Cong_Pres
20:14:48 Formal_Puiseux_Series: theory Formal_Puiseux_Series.FPS_Hensel
20:14:49 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Formal_Puiseux_Series
20:14:49 Running Landau_Symbols (on of1-proof+0-7) ...
20:14:50 Timing Finitely_Generated_Abelian_Groups (2 threads, 49.606s elapsed time, 49.571s cpu time, 4.157s GC time, factor 1.00)
20:14:50 Finished Finitely_Generated_Abelian_Groups (0:00:53 elapsed time, 0:00:52 cpu time, factor 0.99)
20:14:50 Running Cayley_Hamilton (on of3.proof.cit.tum.de+6) ...
20:14:50 Landau_Symbols: theory Landau_Symbols.Group_Sort
20:14:51 Landau_Symbols: theory Landau_Symbols.Landau_Real_Products
20:14:52 Cayley_Hamilton: theory HOL-Library.More_List
20:14:52 Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
20:14:52 Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
20:14:52 Landau_Symbols: theory Landau_Symbols.Landau_Simprocs
20:14:53 Landau_Symbols: theory Landau_Symbols.Landau_More
20:14:54 Timing Landau_Symbols (8 threads, 3.334s elapsed time, 10.215s cpu time, 0.878s GC time, factor 3.06)
20:14:54 Finished Landau_Symbols (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.50)
20:14:55 Running Inductive_Confidentiality (on 10.195.8.11+0) ...
20:14:56 Inductive_Confidentiality: theory Inductive_Confidentiality.Message
20:14:56 Inductive_Confidentiality: theory Inductive_Confidentiality.MessageGA
20:14:57 Running Derangements (on 10.195.8.46+1) ...
20:14:58 Derangements: theory HOL-Combinatorics.Transposition
20:14:58 Derangements: theory HOL-Library.Cancellation
20:14:59 Derangements: theory HOL-Library.FuncSet
20:15:00 Running Integration (on 10.195.8.29+1) ...
20:15:01 Derangements: theory HOL-Library.Multiset
20:15:01 Derangements: theory HOL-Library.Disjoint_Sets
20:15:02 Integration: theory Integration.MonConv
20:15:02 Integration: theory Integration.Sigma_Algebra
20:15:03 Integration: theory Integration.Measure
20:15:03 Inductive_Confidentiality: theory Inductive_Confidentiality.EventGA
20:15:03 Inductive_Confidentiality: theory Inductive_Confidentiality.Event
20:15:04 Integration: theory Integration.RealRandVar
20:15:05 Inductive_Confidentiality: theory Inductive_Confidentiality.PublicGA
20:15:05 Inductive_Confidentiality: theory Inductive_Confidentiality.Public
20:15:06 Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
20:15:06 Integration: theory Integration.Failure
20:15:06 Integration: theory Integration.Integral
20:15:07 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad_GA
20:15:07 Running Euler_MacLaurin (on 10.195.8.40+2) ...
20:15:08 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad
20:15:08 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityGA
20:15:08 Timing Cayley_Hamilton (6 threads, 16.058s elapsed time, 16.053s cpu time, 0.629s GC time, factor 1.00)
20:15:08 Finished Cayley_Hamilton (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.98)
20:15:08 Inductive_Confidentiality: theory Inductive_Confidentiality.Knowledge
20:15:09 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityDY
20:15:10 Euler_MacLaurin: theory HOL-Library.Function_Algebras
20:15:10 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
20:15:11 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
20:15:11 Timing CCS (2 threads, 33.808s elapsed time, 33.806s cpu time, 0.858s GC time, factor 1.00)
20:15:11 Finished CCS (0:00:35 elapsed time, 0:00:35 cpu time, factor 0.99)
20:15:13 Derangements: theory HOL-Combinatorics.Permutations
20:15:14 Timing AxiomaticCategoryTheory (2 threads, 58.380s elapsed time, 48.740s cpu time, 4.687s GC time, factor 0.83)
20:15:14 Finished AxiomaticCategoryTheory (0:01:00 elapsed time, 0:00:50 cpu time, factor 0.83)
20:15:15 Timing Formal_Puiseux_Series (2 threads, 45.265s elapsed time, 45.169s cpu time, 1.450s GC time, factor 1.00)
20:15:15 Finished Formal_Puiseux_Series (0:00:48 elapsed time, 0:00:47 cpu time, factor 0.99)
20:15:15 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
20:15:16 Derangements: theory Derangements.Derangements
20:15:18 Timing Integration (2 threads, 15.242s elapsed time, 15.161s cpu time, 0.402s GC time, factor 0.99)
20:15:18 Finished Integration (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.97)
20:15:23 Running Special_Function_Bounds (on of1-proof+8-15) ...
20:15:24 Running Transitive-Closure-II (on of3.proof.cit.tum.de+6) ...
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
20:15:24 Timing TsirelsonBound (6 threads, 53.129s elapsed time, 53.126s cpu time, 1.993s GC time, factor 1.00)
20:15:24 Finished TsirelsonBound (0:00:55 elapsed time, 0:00:54 cpu time, factor 0.99)
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
20:15:24 Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
20:15:25 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
20:15:25 Transitive-Closure-II: theory HOL-Library.While_Combinator
20:15:25 Transitive-Closure-II: theory Regular-Sets.Regular_Set
20:15:27 Transitive-Closure-II: theory Regular-Sets.Regular_Exp
20:15:27 Euler_MacLaurin: theory Landau_Symbols.Landau_More
20:15:27 Running Boolos_Curious_Inference_Automated (on 10.195.8.32+1) ...
20:15:28 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
20:15:28 Timing Inductive_Confidentiality (2 threads, 30.973s elapsed time, 30.932s cpu time, 1.896s GC time, factor 1.00)
20:15:28 Finished Inductive_Confidentiality (0:00:33 elapsed time, 0:00:32 cpu time, factor 0.99)
20:15:29 Boolos_Curious_Inference_Automated: theory Boolos_Curious_Inference_Automated.Boolos_Curious_Inference_Automated
20:15:30 Transitive-Closure-II: theory Regular-Sets.NDerivative
20:15:30 Transitive-Closure-II: theory Regular-Sets.Relation_Interpretation
20:15:32 Timing Special_Function_Bounds (8 threads, 6.911s elapsed time, 28.989s cpu time, 1.969s GC time, factor 4.19)
20:15:32 Finished Special_Function_Bounds (0:00:08 elapsed time, 0:00:30 cpu time, factor 3.59)
20:15:33 Transitive-Closure-II: theory Regular-Sets.Equivalence_Checking
20:15:33 Transitive-Closure-II: theory Regular-Sets.Regexp_Method
20:15:34 Running Free-Boolean-Algebra (on 10.195.8.29+1) ...
20:15:35 Free-Boolean-Algebra: theory Free-Boolean-Algebra.Free_Boolean_Algebra
20:15:35 Transitive-Closure-II: theory Transitive-Closure-II.RTrancl
20:15:37 Timing Transitive-Closure-II (6 threads, 10.656s elapsed time, 10.656s cpu time, 0.916s GC time, factor 1.00)
20:15:37 Finished Transitive-Closure-II (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
20:15:37 Running Jordan_Hoelder (on 10.195.8.42+2) ...
20:15:38 Timing Free-Boolean-Algebra (2 threads, 2.589s elapsed time, 2.589s cpu time, 0.040s GC time, factor 1.00)
20:15:38 Finished Free-Boolean-Algebra (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.92)
20:15:39 Running Huffman (on of2.proof.cit.tum.de+3) ...
20:15:39 Huffman: theory Huffman.Huffman
20:15:40 Jordan_Hoelder: theory Secondary_Sylow.GroupAction
20:15:40 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
20:15:41 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
20:15:42 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
20:15:43 Jordan_Hoelder: theory Secondary_Sylow.SndSylow
20:15:44 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
20:15:46 Timing Gaussian_Integers (2 threads, 71.674s elapsed time, 71.650s cpu time, 1.942s GC time, factor 1.00)
20:15:46 Finished Gaussian_Integers (0:01:14 elapsed time, 0:01:14 cpu time, factor 0.99)
20:15:46 Running FunWithTilings (on 10.195.7.194+0) ...
20:15:47 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
20:15:47 Timing Boolos_Curious_Inference_Automated (2 threads, 17.037s elapsed time, 17.033s cpu time, 2.552s GC time, factor 1.00)
20:15:47 Finished Boolos_Curious_Inference_Automated (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
20:15:47 Timing Derangements (2 threads, 47.412s elapsed time, 47.390s cpu time, 1.563s GC time, factor 1.00)
20:15:47 Finished Derangements (0:00:49 elapsed time, 0:00:49 cpu time, factor 0.99)
20:15:48 FunWithTilings: theory FunWithTilings.Tilings
20:15:49 Timing Huffman (6 threads, 8.902s elapsed time, 8.902s cpu time, 0.224s GC time, factor 1.00)
20:15:49 Finished Huffman (0:00:10 elapsed time, 0:00:09 cpu time, factor 0.97)
20:15:53 Timing Euler_MacLaurin (2 threads, 40.826s elapsed time, 40.781s cpu time, 1.921s GC time, factor 1.00)
20:15:53 Finished Euler_MacLaurin (0:00:44 elapsed time, 0:00:44 cpu time, factor 0.99)
20:16:02 Estimated 0:11:46 build time with path time heuristic (critical: absolute time (0:05:00), parallel: time based threads, fast hosts: per critical node) (took 4.470s)
20:16:02 Running Design_Theory (on of1-proof+8-15) ...
20:16:03 Design_Theory: theory Graph_Theory.Rtrancl_On
20:16:03 Design_Theory: theory Card_Partitions.Set_Partition
20:16:03 Design_Theory: theory Nested_Multisets_Ordinals.Multiset_More
20:16:03 Design_Theory: theory HOL-Combinatorics.Transposition
20:16:03 Design_Theory: theory Graph_Theory.Stuff
20:16:03 Design_Theory: theory Graph_Theory.Digraph
20:16:03 Design_Theory: theory HOL-Combinatorics.Permutations
20:16:03 Design_Theory: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
20:16:03 Design_Theory: theory Design_Theory.Multisets_Extras
20:16:04 Running Multi_Party_Computation (on of3.proof.cit.tum.de+6) ...
20:16:04 Design_Theory: theory Graph_Theory.Arc_Walk
20:16:04 Design_Theory: theory Graph_Theory.Bidirected_Digraph
20:16:04 Design_Theory: theory Design_Theory.Design_Basics
20:16:06 Design_Theory: theory Graph_Theory.Pair_Digraph
20:16:06 Multi_Party_Computation: theory HOL-Number_Theory.Cong
20:16:06 Multi_Party_Computation: theory HOL-Algebra.FiniteProduct
20:16:06 Multi_Party_Computation: theory HOL-Algebra.Generated_Groups
20:16:06 Multi_Party_Computation: theory Multi_Party_Computation.ETP
20:16:06 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
20:16:06 Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities
20:16:06 Design_Theory: theory Design_Theory.Design_Operations
20:16:07 Running Constructor_Funs (on 10.195.8.30+0) ...
20:16:07 Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def
20:16:07 Design_Theory: theory Design_Theory.Block_Designs
20:16:07 Design_Theory: theory Design_Theory.Sub_Designs
20:16:08 Multi_Party_Computation: theory HOL-Algebra.Ring
20:16:08 Design_Theory: theory Design_Theory.Design_Isomorphisms
20:16:09 Running Robbins-Conjecture (on 10.195.8.32+1) ...
20:16:09 Constructor_Funs: theory Constructor_Funs.Constructor_Funs
20:16:09 Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
20:16:09 Design_Theory: theory Design_Theory.BIBD
20:16:10 Multi_Party_Computation: theory HOL-Algebra.Elementary_Groups
20:16:10 Robbins-Conjecture: theory Robbins-Conjecture.Robbins_Conjecture
20:16:10 Multi_Party_Computation: theory HOL-Number_Theory.Totient
20:16:10 Running Risk_Free_Lending (on 10.195.8.11+2) ...
20:16:10 Design_Theory: theory Graph_Theory.Digraph_Component
20:16:10 Design_Theory: theory Design_Theory.Resolvable_Designs
20:16:11 Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
20:16:11 Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
20:16:11 Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
20:16:11 Design_Theory: theory Design_Theory.Group_Divisible_Designs
20:16:12 Risk_Free_Lending: theory Risk_Free_Lending.Risk_Free_Lending
20:16:12 Design_Theory: theory Design_Theory.Designs_And_Graphs
20:16:13 Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
20:16:13 Timing Jordan_Hoelder (2 threads, 32.549s elapsed time, 32.527s cpu time, 1.852s GC time, factor 1.00)
20:16:13 Finished Jordan_Hoelder (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
20:16:13 Running Random_Graph_Subgraph_Threshold (on 10.195.8.46+2) ...
20:16:14 Running NormByEval (on 10.195.8.29+2) ...
20:16:14 Design_Theory: theory Design_Theory.Design_Theory_Root
20:16:16 NormByEval: theory NormByEval.NBE
20:16:16 Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
20:16:16 Multi_Party_Computation: theory Multi_Party_Computation.OT14
20:16:16 Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
20:16:17 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
20:16:17 Timing FunWithTilings (2 threads, 29.440s elapsed time, 29.438s cpu time, 0.324s GC time, factor 1.00)
20:16:17 Finished FunWithTilings (0:00:31 elapsed time, 0:00:31 cpu time, factor 0.99)
20:16:18 Multi_Party_Computation: theory HOL-Algebra.AbelCoset
20:16:18 Multi_Party_Computation: theory HOL-Algebra.Module
20:16:19 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
20:16:19 Running Digit_Expansions (on of2.proof.cit.tum.de+3) ...
20:16:19 Timing Design_Theory (8 threads, 15.713s elapsed time, 107.513s cpu time, 8.809s GC time, factor 6.84)
20:16:19 Finished Design_Theory (0:00:17 elapsed time, 0:01:50 cpu time, factor 6.34)
20:16:20 Digit_Expansions: theory Digit_Expansions.Bits_Digits
20:16:21 Digit_Expansions: theory Digit_Expansions.Carries
20:16:21 Digit_Expansions: theory Digit_Expansions.Binary_Operations
20:16:21 Running GraphMarkingIBP (on 10.195.6.179+0) ...
20:16:22 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
20:16:23 GraphMarkingIBP: theory GraphMarkingIBP.Graph
20:16:23 GraphMarkingIBP: theory LatticeProperties.Conj_Disj
20:16:23 Running LambdaMu (on 10.195.8.40+2) ...
20:16:23 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
20:16:23 GraphMarkingIBP: theory LatticeProperties.WellFoundedTransitive
20:16:24 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
20:16:24 Running Generalized_Counting_Sort (on 10.195.8.49+1) ...
20:16:24 Timing Constructor_Funs (2 threads, 15.513s elapsed time, 7.986s cpu time, 0.548s GC time, factor 0.51)
20:16:24 Finished Constructor_Funs (0:00:17 elapsed time, 0:00:09 cpu time, factor 0.55)
20:16:25 LambdaMu: theory LambdaMu.Syntax
20:16:25 GraphMarkingIBP: theory LatticeProperties.Complete_Lattice_Prop
20:16:25 Multi_Party_Computation: theory Multi_Party_Computation.GMW
20:16:26 GraphMarkingIBP: theory DataRefinementIBP.Preliminaries
20:16:26 GraphMarkingIBP: theory DataRefinementIBP.Statements
20:16:26 Generalized_Counting_Sort: theory Generalized_Counting_Sort.Algorithm
20:16:26 GraphMarkingIBP: theory DataRefinementIBP.Hoare
20:16:27 Running Dedekind_Real (on 10.195.7.194+3) ...
20:16:27 GraphMarkingIBP: theory DataRefinementIBP.Diagram
20:16:27 GraphMarkingIBP: theory DataRefinementIBP.DataRefinement
20:16:28 GraphMarkingIBP: theory GraphMarkingIBP.SetMark
20:16:28 Dedekind_Real: theory Dedekind_Real.Dedekind_Real
20:16:29 Timing Robbins-Conjecture (2 threads, 18.075s elapsed time, 18.049s cpu time, 0.541s GC time, factor 1.00)
20:16:29 Finished Robbins-Conjecture (0:00:20 elapsed time, 0:00:19 cpu time, factor 0.98)
20:16:29 Timing Risk_Free_Lending (2 threads, 16.748s elapsed time, 16.615s cpu time, 0.405s GC time, factor 0.99)
20:16:29 Finished Risk_Free_Lending (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.97)
20:16:29 Multi_Party_Computation: theory HOL-Algebra.Ideal
20:16:30 LambdaMu: theory LambdaMu.DeBruijn
20:16:30 LambdaMu: theory LambdaMu.Types
20:16:30 GraphMarkingIBP: theory GraphMarkingIBP.StackMark
20:16:30 Generalized_Counting_Sort: theory Generalized_Counting_Sort.Conservation
20:16:30 LambdaMu: theory LambdaMu.Substitution
20:16:31 LambdaMu: theory LambdaMu.Peirce
20:16:31 GraphMarkingIBP: theory GraphMarkingIBP.LinkMark
20:16:31 LambdaMu: theory LambdaMu.Reduction
20:16:32 GraphMarkingIBP: theory GraphMarkingIBP.DSWMark
20:16:32 LambdaMu: theory LambdaMu.ContextFacts
20:16:32 Timing Digit_Expansions (6 threads, 11.541s elapsed time, 11.540s cpu time, 0.251s GC time, factor 1.00)
20:16:32 Finished Digit_Expansions (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
20:16:32 Generalized_Counting_Sort: theory Generalized_Counting_Sort.Sorting
20:16:33 LambdaMu: theory LambdaMu.TypePreservation
20:16:33 LambdaMu: theory LambdaMu.Progress
20:16:33 Generalized_Counting_Sort: theory Generalized_Counting_Sort.Stability
20:16:38 Multi_Party_Computation: theory HOL-Algebra.RingHom
20:16:38 Timing Random_Graph_Subgraph_Threshold (2 threads, 19.865s elapsed time, 19.852s cpu time, 0.501s GC time, factor 1.00)
20:16:38 Finished Random_Graph_Subgraph_Threshold (0:00:23 elapsed time, 0:00:23 cpu time, factor 0.98)
20:16:39 Running Relational_Minimum_Spanning_Trees (on of1-proof+0-7) ...
20:16:40 Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Kruskal
20:16:40 Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Prim
20:16:41 Multi_Party_Computation: theory HOL-Algebra.UnivPoly
20:16:41 Timing LambdaMu (2 threads, 15.708s elapsed time, 15.655s cpu time, 0.549s GC time, factor 1.00)
20:16:41 Finished LambdaMu (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.98)
20:16:41 Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Boruvka
20:16:42 Running FOL_Axiomatic (on 10.195.8.30+1) ...
20:16:43 Timing Incompleteness (6 threads, 165.761s elapsed time, 486.665s cpu time, 29.133s GC time, factor 2.94)
20:16:43 Finished Incompleteness (0:03:03 elapsed time, 0:08:36 cpu time, factor 2.81)
20:16:44 Timing Dedekind_Real (2 threads, 14.873s elapsed time, 14.846s cpu time, 0.221s GC time, factor 1.00)
20:16:44 Finished Dedekind_Real (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
20:16:44 Running StrictOmegaCategories (on 10.195.8.32+2) ...
20:16:44 FOL_Axiomatic: theory HOL-Library.Nat_Bijection
20:16:44 FOL_Axiomatic: theory HOL-Library.Old_Datatype
20:16:46 StrictOmegaCategories: theory HOL-Library.FuncSet
20:16:47 FOL_Axiomatic: theory HOL-Library.Countable
20:16:47 Running Comparison_Sort_Lower_Bound (on 10.195.8.11+0) ...
20:16:48 StrictOmegaCategories: theory StrictOmegaCategories.Globular_Set
20:16:50 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
20:16:50 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
20:16:50 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
20:16:50 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic_Variant
20:16:51 StrictOmegaCategories: theory StrictOmegaCategories.Strict_Omega_Category
20:16:52 StrictOmegaCategories: theory StrictOmegaCategories.Pasting_Diagram
20:16:53 Running XML (on 10.195.8.42+4) ...
20:16:54 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
20:16:56 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
20:16:56 Timing Relational_Minimum_Spanning_Trees (8 threads, 14.827s elapsed time, 61.384s cpu time, 5.497s GC time, factor 4.14)
20:16:56 Finished Relational_Minimum_Spanning_Trees (0:00:16 elapsed time, 0:01:03 cpu time, factor 3.88)
20:16:57 XML: theory Deriving.Derive_Manager
20:16:57 XML: theory Deriving.Generator_Aux
20:16:57 XML: theory Certification_Monads.Error_Syntax
20:16:57 XML: theory Certification_Monads.Error_Monad
20:16:58 XML: theory Partial_Function_MR.Partial_Function_MR
20:16:59 XML: theory Certification_Monads.Strict_Sum
20:17:00 Timing GraphMarkingIBP (2 threads, 35.510s elapsed time, 35.485s cpu time, 0.593s GC time, factor 1.00)
20:17:00 Finished GraphMarkingIBP (0:00:37 elapsed time, 0:00:37 cpu time, factor 0.99)
20:17:00 Running Lower_Semicontinuous (on 10.195.8.40+2) ...
20:17:02 XML: theory Show.Show
20:17:03 Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
20:17:03 Running Abstract_Soundness (on 10.195.7.194+2) ...
20:17:06 Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
20:17:06 Timing NormByEval (2 threads, 48.469s elapsed time, 48.456s cpu time, 2.062s GC time, factor 1.00)
20:17:06 Finished NormByEval (0:00:50 elapsed time, 0:00:50 cpu time, factor 0.99)
20:17:06 XML: theory Certification_Monads.Parser_Monad
20:17:06 Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
20:17:07 Timing StrictOmegaCategories (2 threads, 19.975s elapsed time, 19.974s cpu time, 0.588s GC time, factor 1.00)
20:17:07 Finished StrictOmegaCategories (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98)
20:17:09 XML: theory XML.Xml
20:17:10 Timing Comparison_Sort_Lower_Bound (2 threads, 18.299s elapsed time, 18.278s cpu time, 0.655s GC time, factor 1.00)
20:17:10 Finished Comparison_Sort_Lower_Bound (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
20:17:13 Timing FOL_Axiomatic (2 threads, 26.971s elapsed time, 26.931s cpu time, 3.065s GC time, factor 1.00)
20:17:13 Finished FOL_Axiomatic (0:00:29 elapsed time, 0:00:29 cpu time, factor 0.99)
20:17:15 Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
20:17:15 Running Median_Method (on of1-proof+8-12) ...
20:17:16 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
20:17:17 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
20:17:17 Median_Method: theory Median_Method.Median
20:17:18 Building Padic_Ints (on of4.proof.cit.tum.de+0) ...
20:17:19 XML: theory XML.Xmlt
20:17:19 Padic_Ints: theory HOL-Number_Theory.Cong
20:17:19 Padic_Ints: theory Padic_Ints.Function_Ring
20:17:19 Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
20:17:19 Padic_Ints: theory Padic_Ints.Extended_Int
20:17:19 Timing Median_Method (8 threads, 2.518s elapsed time, 6.884s cpu time, 0.250s GC time, factor 2.73)
20:17:19 Finished Median_Method (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.01)
20:17:20 Running Belief_Revision (on 10.195.8.32+4) ...
20:17:21 Running Impossible_Geometry (on 10.195.8.11+4) ...
20:17:22 Belief_Revision: theory Belief_Revision.AGM_Logic
20:17:23 Impossible_Geometry: theory Impossible_Geometry.Impossible_Geometry
20:17:23 Belief_Revision: theory Belief_Revision.AGM_Remainder
20:17:23 Padic_Ints: theory HOL-Number_Theory.Totient
20:17:23 Multi_Party_Computation: theory HOL-Number_Theory.Residues
20:17:24 Running Combinable_Wands (on 10.195.8.46+4) ...
20:17:24 Belief_Revision: theory Belief_Revision.AGM_Contraction
20:17:25 Padic_Ints: theory HOL-Number_Theory.Residues
20:17:26 Timing Lower_Semicontinuous (2 threads, 22.563s elapsed time, 22.562s cpu time, 0.387s GC time, factor 1.00)
20:17:26 Finished Lower_Semicontinuous (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.98)
20:17:26 Combinable_Wands: theory Combinable_Wands.PosRat
20:17:26 Belief_Revision: theory Belief_Revision.AGM_Revision
20:17:27 Combinable_Wands: theory Combinable_Wands.Mask
20:17:27 Running SDS_Impossibility (on 10.195.8.29+1) ...
20:17:30 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
20:17:30 Combinable_Wands: theory Combinable_Wands.PartialHeapSA
20:17:31 Timing Abstract_Soundness (2 threads, 25.040s elapsed time, 25.009s cpu time, 1.543s GC time, factor 1.00)
20:17:31 Finished Abstract_Soundness (0:00:28 elapsed time, 0:00:27 cpu time, factor 0.99)
20:17:31 Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux
20:17:32 Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT
20:17:34 Padic_Ints: theory Padic_Ints.Padic_Construction
20:17:35 Running Well_Quasi_Orders (on 10.195.6.179+4) ...
20:17:35 Combinable_Wands: theory Combinable_Wands.CombinableWands
20:17:36 Padic_Ints: theory Padic_Ints.Padic_Integers
20:17:37 Well_Quasi_Orders: theory Abstract-Rewriting.Seq
20:17:37 Well_Quasi_Orders: theory Open_Induction.Restricted_Predicates
20:17:39 Well_Quasi_Orders: theory Open_Induction.Open_Induction
20:17:39 Well_Quasi_Orders: theory Well_Quasi_Orders.Multiset_Extension
20:17:40 Timing Impossible_Geometry (2 threads, 16.002s elapsed time, 15.945s cpu time, 0.979s GC time, factor 1.00)
20:17:40 Finished Impossible_Geometry (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.98)
20:17:41 Well_Quasi_Orders: theory Regular-Sets.Regular_Set
20:17:41 Well_Quasi_Orders: theory Well_Quasi_Orders.Infinite_Sequences
20:17:41 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Elements
20:17:41 Well_Quasi_Orders: theory Well_Quasi_Orders.Least_Enum
20:17:42 Timing XML (2 threads, 43.691s elapsed time, 43.648s cpu time, 5.450s GC time, factor 1.00)
20:17:42 Finished XML (0:00:47 elapsed time, 0:00:46 cpu time, factor 0.99)
20:17:43 Padic_Ints: theory Padic_Ints.Cring_Poly
20:17:44 Well_Quasi_Orders: theory Regular-Sets.Regular_Exp
20:17:46 Timing Belief_Revision (2 threads, 23.256s elapsed time, 23.232s cpu time, 0.683s GC time, factor 1.00)
20:17:46 Finished Belief_Revision (0:00:25 elapsed time, 0:00:24 cpu time, factor 0.98)
20:17:50 Running Szemeredi_Regularity (on of1-proof+0-7) ...
20:17:51 Well_Quasi_Orders: theory Regular-Sets.NDerivative
20:17:51 Well_Quasi_Orders: theory Regular-Sets.Relation_Interpretation
20:17:52 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
20:17:54 Timing Szemeredi_Regularity (8 threads, 1.939s elapsed time, 6.567s cpu time, 0.238s GC time, factor 3.39)
20:17:54 Finished Szemeredi_Regularity (0:00:03 elapsed time, 0:00:08 cpu time, factor 2.23)
20:17:55 Running Public_Announcement_Logic (on 10.195.8.30+0) ...
20:17:56 Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
20:17:57 Running Transformer_Semantics (on 10.195.8.11+3) ...
20:17:59 Timing Combinable_Wands (2 threads, 31.567s elapsed time, 31.535s cpu time, 1.551s GC time, factor 1.00)
20:17:59 Finished Combinable_Wands (0:00:33 elapsed time, 0:00:33 cpu time, factor 0.99)
20:18:00 Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
20:18:00 Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
20:18:00 Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
20:18:00 Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
20:18:02 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
20:18:03 Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
20:18:04 Timing Generalized_Counting_Sort (2 threads, 95.988s elapsed time, 95.835s cpu time, 1.428s GC time, factor 1.00)
20:18:04 Finished Generalized_Counting_Sort (0:01:38 elapsed time, 0:01:38 cpu time, factor 0.99)
20:18:05 Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
20:18:05 Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT
20:18:05 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
20:18:05 Running InformationFlowSlicing_Inter (on 10.195.8.42+3) ...
20:18:05 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
20:18:06 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
20:18:07 Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
20:18:08 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
20:18:08 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
20:18:08 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
20:18:08 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
20:18:08 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
20:18:09 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
20:18:09 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
20:18:11 Timing Public_Announcement_Logic (2 threads, 13.876s elapsed time, 13.834s cpu time, 0.991s GC time, factor 1.00)
20:18:11 Finished Public_Announcement_Logic (0:00:15 elapsed time, 0:00:15 cpu time, factor 0.98)
20:18:12 Running Lambda_Free_RPOs (on 10.195.8.40+0) ...
20:18:14 Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
20:18:14 Lambda_Free_RPOs: theory Nested_Multisets_Ordinals.Multiset_More
20:18:14 Running Ramsey-Infinite (on 10.195.7.194+4) ...
20:18:15 Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
20:18:15 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
20:18:15 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
20:18:16 Ramsey-Infinite: theory HOL-Library.FuncSet
20:18:16 Ramsey-Infinite: theory HOL-Library.Infinite_Set
20:18:18 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
20:18:19 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
20:18:19 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
20:18:19 Ramsey-Infinite: theory HOL-Library.Ramsey
20:18:21 Ramsey-Infinite: theory Ramsey-Infinite.Ramsey
20:18:27 Running BNF_Operations (on of1-proof+8-15) ...
20:18:28 Timing Transformer_Semantics (2 threads, 27.457s elapsed time, 27.354s cpu time, 0.852s GC time, factor 1.00)
20:18:28 Finished Transformer_Semantics (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.99)
20:18:28 BNF_Operations: theory HOL-Library.BNF_Axiomatization
20:18:28 BNF_Operations: theory BNF_Operations.GFP
20:18:28 BNF_Operations: theory BNF_Operations.Compose
20:18:28 BNF_Operations: theory BNF_Operations.Kill
20:18:28 BNF_Operations: theory BNF_Operations.LFP
20:18:28 BNF_Operations: theory BNF_Operations.Permute
20:18:28 BNF_Operations: theory BNF_Operations.N2M
20:18:28 BNF_Operations: theory BNF_Operations.Lift
20:18:29 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
20:18:29 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
20:18:29 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
20:18:31 Running Pell (on 10.195.8.30+3) ...
20:18:32 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
20:18:33 Running Card_Multisets (on 10.195.8.32+0) ...
20:18:33 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
20:18:33 Timing BNF_Operations (8 threads, 4.590s elapsed time, 21.726s cpu time, 5.013s GC time, factor 4.73)
20:18:33 Finished BNF_Operations (0:00:05 elapsed time, 0:00:24 cpu time, factor 4.09)
20:18:34 Card_Multisets: theory HOL-Library.Cancellation
20:18:34 Pell: theory Pell.Efficient_Discrete_Sqrt
20:18:34 Pell: theory Pell.Pell
20:18:35 Card_Multisets: theory HOL-Library.Multiset
20:18:36 Running Fixed_Length_Vector (on 10.195.8.46+2) ...
20:18:37 Fixed_Length_Vector: theory HOL-Library.Phantom_Type
20:18:39 Pell: theory Pell.Pell_Algorithm
20:18:39 Fixed_Length_Vector: theory HOL-Library.Cardinality
20:18:40 Timing Well_Quasi_Orders (2 threads, 61.996s elapsed time, 61.892s cpu time, 5.309s GC time, factor 1.00)
20:18:40 Finished Well_Quasi_Orders (0:01:05 elapsed time, 0:01:04 cpu time, factor 0.99)
20:18:41 Fixed_Length_Vector: theory HOL-Library.Numeral_Type
20:18:41 Fixed_Length_Vector: theory HOL-Library.Code_Cardinality
20:18:42 Pell: theory Pell.Pell_Algorithm_Test
20:18:44 Fixed_Length_Vector: theory Fixed_Length_Vector.Fixed_Length_Vector
20:18:44 Timing Ramsey-Infinite (2 threads, 26.890s elapsed time, 26.864s cpu time, 1.046s GC time, factor 1.00)
20:18:44 Finished Ramsey-Infinite (0:00:28 elapsed time, 0:00:28 cpu time, factor 0.99)
20:18:45 Timing SDS_Impossibility (2 threads, 73.399s elapsed time, 73.371s cpu time, 2.547s GC time, factor 1.00)
20:18:45 Finished SDS_Impossibility (0:01:17 elapsed time, 0:01:16 cpu time, factor 0.99)
20:18:47 Running Fourier (on 10.195.8.49+3) ...
20:18:49 Card_Multisets: theory Card_Multisets.Card_Multisets
20:18:50 Fourier: theory HOL-Library.Function_Algebras
20:18:50 Fourier: theory Fourier.Confine
20:18:50 Timing Fixed_Length_Vector (2 threads, 12.213s elapsed time, 11.127s cpu time, 0.373s GC time, factor 0.91)
20:18:50 Finished Fixed_Length_Vector (0:00:14 elapsed time, 0:00:12 cpu time, factor 0.90)
20:18:51 Fourier: theory Fourier.Fourier_Aux2
20:18:51 Fourier: theory Fourier.Periodic
20:18:53 Fourier: theory Ergodic_Theory.SG_Library_Complement
20:18:55 Fourier: theory Lp.Functional_Spaces
20:18:58 Timing InformationFlowSlicing_Inter (2 threads, 47.652s elapsed time, 47.629s cpu time, 4.301s GC time, factor 1.00)
20:18:58 Finished InformationFlowSlicing_Inter (0:00:51 elapsed time, 0:00:50 cpu time, factor 0.99)
20:19:01 Fourier: theory Lp.Lp
20:19:01 Timing Card_Multisets (2 threads, 25.700s elapsed time, 25.643s cpu time, 0.960s GC time, factor 1.00)
20:19:01 Finished Card_Multisets (0:00:27 elapsed time, 0:00:27 cpu time, factor 0.98)
20:19:02 Estimated 0:11:46 build time with path time heuristic (critical: absolute time (0:05:00), parallel: time based threads, fast hosts: per critical node) (took 2.932s)
20:19:02 Running Wetzels_Problem (on of1-proof+8-15) ...
20:19:03 Fourier: theory Fourier.Lspace
20:19:03 Fourier: theory Fourier.Square_Integrable
20:19:03 Wetzels_Problem: theory HOL-Cardinals.Fun_More
20:19:03 Wetzels_Problem: theory HOL-Cardinals.Order_Relation_More
20:19:03 Wetzels_Problem: theory HOL-Cardinals.Order_Union
20:19:03 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Extension
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Wellfounded_More
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Relation
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Embedding
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Wellorder_Constructions
20:19:04 Fourier: theory Fourier.Fourier
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Cardinal_Order_Relation
20:19:04 Wetzels_Problem: theory HOL-Cardinals.Ordinal_Arithmetic
20:19:05 Wetzels_Problem: theory HOL-Cardinals.Cardinal_Arithmetic
20:19:06 Wetzels_Problem: theory HOL-Cardinals.Cardinals
20:19:06 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Library
20:19:06 Wetzels_Problem: theory ZFC_in_HOL.ZFC_in_HOL
20:19:07 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Cardinals
20:19:08 Running Probabilistic_Prime_Tests (on of4.proof.cit.tum.de+9-12) ...
20:19:08 Wetzels_Problem: theory ZFC_in_HOL.ZFC_Typeclasses
20:19:09 Wetzels_Problem: theory ZFC_in_HOL.General_Cardinals
20:19:09 Probabilistic_Prime_Tests: theory HOL-Cardinals.Fun_More
20:19:09 Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Union
20:19:09 Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Relation_More
20:19:09 Probabilistic_Prime_Tests: theory HOL-Computational_Algebra.Squarefree
20:19:09 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Cong
20:19:09 Probabilistic_Prime_Tests: theory HOL-Algebra.Exponent
20:19:09 Wetzels_Problem: theory Wetzels_Problem.Wetzels_Problem
20:19:10 Timing Pell (2 threads, 34.611s elapsed time, 34.587s cpu time, 0.633s GC time, factor 1.00)
20:19:10 Finished Pell (0:00:37 elapsed time, 0:00:37 cpu time, factor 0.99)
20:19:10 Probabilistic_Prime_Tests: theory HOL-Library.Fun_Lexorder
20:19:10 Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence
20:19:10 Probabilistic_Prime_Tests: theory HOL-Combinatorics.Cycles
20:19:10 Probabilistic_Prime_Tests: theory HOL-Combinatorics.List_Permutation
20:19:10 Probabilistic_Prime_Tests: theory HOL-Library.Groups_Big_Fun
20:19:10 Probabilistic_Prime_Tests: theory HOL-Library.More_List
20:19:10 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellfounded_More
20:19:10 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Relation
20:19:10 Running GoedelGod (on 10.195.8.11+4) ...
20:19:10 Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
20:19:10 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Embedding
20:19:10 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
20:19:10 Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping
20:19:10 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
20:19:10 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Constructions
20:19:11 Probabilistic_Prime_Tests: theory HOL-Algebra.Order
20:19:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
20:19:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
20:19:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
20:19:11 Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Order_Relation
20:19:12 GoedelGod: theory GoedelGod.GoedelGod
20:19:12 Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
20:19:12 Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Arithmetic
20:19:12 Running LP_Duality (on 10.195.8.46+0) ...
20:19:13 Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
20:19:14 Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
20:19:14 Probabilistic_Prime_Tests: theory HOL-Algebra.Group
20:19:16 Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
20:19:16 Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
20:19:16 Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
20:19:16 Running Laplace_Transform (on 10.195.8.29+1) ...
20:19:17 Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
20:19:17 LP_Duality: theory LP_Duality.Minimum_Maximum
20:19:17 Timing Wetzels_Problem (8 threads, 12.471s elapsed time, 68.491s cpu time, 5.934s GC time, factor 5.49)
20:19:17 Finished Wetzels_Problem (0:00:14 elapsed time, 0:01:11 cpu time, factor 4.99)
20:19:18 LP_Duality: theory LP_Duality.LP_Duality
20:19:19 Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
20:19:19 Probabilistic_Prime_Tests: theory HOL-Algebra.Left_Coset
20:19:19 Probabilistic_Prime_Tests: theory HOL-Algebra.SimpleGroups
20:19:19 Running Banach_Steinhaus (on 10.195.8.42+2) ...
20:19:19 Probabilistic_Prime_Tests: theory HOL-Algebra.SndIsomorphismGrp
20:19:19 Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
20:19:20 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
20:19:20 Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
20:19:20 Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
20:19:20 Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
20:19:20 Timing GoedelGod (2 threads, 7.308s elapsed time, 6.590s cpu time, 0.149s GC time, factor 0.90)
20:19:20 Finished GoedelGod (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.88)
20:19:20 Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
20:19:20 Timing Lambda_Free_RPOs (2 threads, 64.005s elapsed time, 63.954s cpu time, 3.192s GC time, factor 1.00)
20:19:20 Finished Lambda_Free_RPOs (0:01:07 elapsed time, 0:01:06 cpu time, factor 0.99)
20:19:21 Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
20:19:21 Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
20:19:21 Probabilistic_Prime_Tests: theory HOL-Algebra.Elementary_Groups
20:19:21 Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
20:19:22 Probabilistic_Prime_Tests: theory HOL-Algebra.Module
20:19:22 Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
20:19:22 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
20:19:22 Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
20:19:22 Probabilistic_Prime_Tests: theory HOL-Algebra.Product_Groups
20:19:22 Laplace_Transform: theory Laplace_Transform.Existence
20:19:23 Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups
20:19:23 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
20:19:24 Laplace_Transform: theory Laplace_Transform.Uniqueness
20:19:24 Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
20:19:25 Laplace_Transform: theory Laplace_Transform.Laplace_Transform
20:19:26 Running VectorSpace (on 10.195.8.49+2) ...
20:19:26 Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
20:19:26 Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
20:19:27 Running Maximum_Segment_Sum (on 10.195.6.179+4) ...
20:19:27 Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
20:19:27 Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
20:19:28 Running Partial_Function_MR (on 10.195.7.194+4) ...
20:19:28 Maximum_Segment_Sum: theory Maximum_Segment_Sum.Maximum_Segment_Sum
20:19:28 Timing LP_Duality (2 threads, 10.317s elapsed time, 10.316s cpu time, 0.176s GC time, factor 1.00)
20:19:28 Finished LP_Duality (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.97)
20:19:28 VectorSpace: theory VectorSpace.FunctionLemmas
20:19:28 VectorSpace: theory VectorSpace.RingModuleFacts
20:19:29 Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
20:19:29 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
20:19:30 Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
20:19:30 Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
20:19:30 VectorSpace: theory VectorSpace.MonoidSums
20:19:30 Partial_Function_MR: theory HOL-Library.Monad_Syntax
20:19:30 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
20:19:31 Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
20:19:31 VectorSpace: theory VectorSpace.LinearCombinations
20:19:35 Timing Maximum_Segment_Sum (2 threads, 6.543s elapsed time, 6.387s cpu time, 0.133s GC time, factor 0.98)
20:19:35 Finished Maximum_Segment_Sum (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.94)
20:19:37 Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
20:19:38 Timing Partial_Function_MR (2 threads, 8.082s elapsed time, 8.081s cpu time, 0.497s GC time, factor 1.00)
20:19:38 Finished Partial_Function_MR (0:00:10 elapsed time, 0:00:09 cpu time, factor 0.97)
20:19:38 Running Hypergraph_Basics (on of1-proof+0-7) ...
20:19:39 Hypergraph_Basics: theory HOL-Combinatorics.Transposition
20:19:39 Hypergraph_Basics: theory Card_Partitions.Set_Partition
20:19:39 Hypergraph_Basics: theory Nested_Multisets_Ordinals.Multiset_More
20:19:39 Hypergraph_Basics: theory Girth_Chromatic.Girth_Chromatic_Misc
20:19:39 Hypergraph_Basics: theory Undirected_Graph_Theory.Undirected_Graph_Basics
20:19:39 Hypergraph_Basics: theory HOL-Combinatorics.Permutations
20:19:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility
20:19:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings
20:19:40 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues
20:19:40 Hypergraph_Basics: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
20:19:40 Hypergraph_Basics: theory Design_Theory.Multisets_Extras
20:19:40 Hypergraph_Basics: theory HOL-Combinatorics.Multiset_Permutations
20:19:40 Hypergraph_Basics: theory Design_Theory.Design_Basics
20:19:41 Timing Banach_Steinhaus (2 threads, 18.921s elapsed time, 18.764s cpu time, 0.469s GC time, factor 0.99)
20:19:41 VectorSpace: theory VectorSpace.SumSpaces
20:19:41 Finished Banach_Steinhaus (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98)
20:19:41 Hypergraph_Basics: theory Fishers_Inequality.Set_Multiset_Extras
20:19:41 Hypergraph_Basics: theory Undirected_Graph_Theory.Undirected_Graph_Walks
20:19:42 Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
20:19:42 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
20:19:42 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion
20:19:42 VectorSpace: theory VectorSpace.VectorSpace
20:19:42 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss
20:19:42 Hypergraph_Basics: theory Undirected_Graph_Theory.Bipartite_Graphs
20:19:42 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
20:19:42 Hypergraph_Basics: theory Design_Theory.Design_Operations
20:19:43 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
20:19:43 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
20:19:43 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
20:19:43 Hypergraph_Basics: theory Design_Theory.Block_Designs
20:19:43 Hypergraph_Basics: theory Design_Theory.Sub_Designs
20:19:44 Running FileRefinement (on 10.195.8.30+4) ...
20:19:45 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
20:19:45 Running Arith_Prog_Rel_Primes (on 10.195.8.11+0) ...
20:19:45 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
20:19:45 FileRefinement: theory FileRefinement.CArrays
20:19:45 FileRefinement: theory FileRefinement.ResizableArrays
20:19:45 Hypergraph_Basics: theory Design_Theory.BIBD
20:19:46 Running HotelKeyCards (on 10.195.8.32+0) ...
20:19:46 FileRefinement: theory FileRefinement.FileRefinement
20:19:46 Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
20:19:46 Running Binomial-Queues (on 10.195.8.46+2) ...
20:19:47 Hypergraph_Basics: theory Fishers_Inequality.Design_Extras
20:19:47 Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
20:19:47 HotelKeyCards: theory HOL-Library.LaTeXsugar
20:19:47 Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph
20:19:48 Timing Laplace_Transform (2 threads, 27.817s elapsed time, 27.813s cpu time, 0.520s GC time, factor 1.00)
20:19:48 Finished Laplace_Transform (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.99)
20:19:48 HotelKeyCards: theory HotelKeyCards.Notation
20:19:48 HotelKeyCards: theory HotelKeyCards.Basis
20:19:48 Binomial-Queues: theory Binomial-Queues.PQ
20:19:48 HotelKeyCards: theory HotelKeyCards.State
20:19:48 HotelKeyCards: theory HotelKeyCards.Trace
20:19:48 Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph_Variations
20:19:49 Timing Multi_Party_Computation (6 threads, 221.682s elapsed time, 221.663s cpu time, 42.320s GC time, factor 1.00)
20:19:49 Finished Multi_Party_Computation (0:03:44 elapsed time, 0:03:44 cpu time, factor 1.00)
20:19:50 Binomial-Queues: theory Binomial-Queues.Binomial_Queue
20:19:50 HotelKeyCards: theory HotelKeyCards.NewCard
20:19:50 HotelKeyCards: theory HotelKeyCards.Equivalence
20:19:50 Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph_Basics_Root
20:19:51 Timing Hypergraph_Basics (8 threads, 11.860s elapsed time, 78.681s cpu time, 6.152s GC time, factor 6.63)
20:19:51 Finished Hypergraph_Basics (0:00:13 elapsed time, 0:01:20 cpu time, factor 6.06)
20:19:53 Running Menger (on 10.195.8.42+4) ...
20:19:54 Binomial-Queues: theory Binomial-Queues.PQ_Implementation
20:19:54 Menger: theory Menger.Graph
20:19:54 Menger: theory Menger.Helpers
20:19:58 Menger: theory Menger.Separations
20:19:58 Menger: theory Menger.DisjointPaths
20:19:59 Timing Arith_Prog_Rel_Primes (2 threads, 10.722s elapsed time, 10.452s cpu time, 0.283s GC time, factor 0.97)
20:19:59 Finished Arith_Prog_Rel_Primes (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.96)
20:19:59 Running Rank_Nullity_Theorem (on 10.195.8.40+0) ...
20:19:59 Menger: theory Menger.MengerInduction
20:19:59 Timing HotelKeyCards (2 threads, 11.532s elapsed time, 11.531s cpu time, 0.326s GC time, factor 1.00)
20:19:59 Finished HotelKeyCards (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
20:20:00 Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility
20:20:00 Timing FileRefinement (2 threads, 14.485s elapsed time, 14.481s cpu time, 0.185s GC time, factor 1.00)
20:20:00 Finished FileRefinement (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
20:20:01 Running CryptoBasedCompositionalProperties (on 10.195.6.179+4) ...
20:20:01 Menger: theory Menger.Y_eq_new_last
20:20:01 Menger: theory Menger.Y_neq_new_last
20:20:03 Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
20:20:03 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
20:20:03 Timing Binomial-Queues (2 threads, 13.187s elapsed time, 13.186s cpu time, 0.492s GC time, factor 1.00)
20:20:03 Finished Binomial-Queues (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.98)
20:20:03 Menger: theory Menger.Menger
20:20:03 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.ListExtras
20:20:04 Padic_Ints: theory Padic_Ints.Padic_Int_Topology
20:20:04 Running Relational-Incorrectness-Logic (on 10.195.7.194+3) ...
20:20:04 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
20:20:04 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy_types
20:20:07 Relational-Incorrectness-Logic: theory Relational-Incorrectness-Logic.RelationalIncorrectness
20:20:09 Padic_Ints: theory Padic_Ints.Zp_Compact
20:20:09 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.inout
20:20:10 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy
20:20:10 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
20:20:11 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.CompLocalSecrets
20:20:11 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
20:20:13 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
20:20:14 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
20:20:14 Running Prefix_Free_Code_Combinators (on of1-proof+8-15) ...
20:20:15 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
20:20:16 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Examples
20:20:17 Timing Prefix_Free_Code_Combinators (8 threads, 1.588s elapsed time, 3.982s cpu time, 0.132s GC time, factor 2.51)
20:20:17 Finished Prefix_Free_Code_Combinators (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.75)
20:20:18 Timing Relational-Incorrectness-Logic (2 threads, 11.544s elapsed time, 11.528s cpu time, 0.319s GC time, factor 1.00)
20:20:18 Finished Relational-Incorrectness-Logic (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.97)
20:20:19 Building Parity_Game (on of3.proof.cit.tum.de+2) ...
20:20:19 Timing Rank_Nullity_Theorem (2 threads, 16.039s elapsed time, 16.031s cpu time, 0.584s GC time, factor 1.00)
20:20:19 Finished Rank_Nullity_Theorem (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.98)
20:20:19 Timing Menger (2 threads, 23.168s elapsed time, 23.164s cpu time, 0.871s GC time, factor 1.00)
20:20:19 Finished Menger (0:00:25 elapsed time, 0:00:24 cpu time, factor 0.99)
20:20:19 Parity_Game: theory Graph_Theory.Rtrancl_On
20:20:19 Parity_Game: theory HOL-Combinatorics.Transposition
20:20:19 Parity_Game: theory HOL-Library.Cancellation
20:20:19 Parity_Game: theory HOL-Library.Case_Converter
20:20:19 Parity_Game: theory HOL-Library.Complete_Partial_Order2
20:20:20 Parity_Game: theory HOL-Library.FuncSet
20:20:20 Running Randomised_BSTs (on 10.195.8.30+2) ...
20:20:20 Parity_Game: theory HOL-Library.Infinite_Set
20:20:20 Parity_Game: theory HOL-Library.Nat_Bijection
20:20:20 Parity_Game: theory HOL-Library.Simps_Case_Conv
20:20:21 Parity_Game: theory HOL-Library.Old_Datatype
20:20:21 Timing CryptoBasedCompositionalProperties (2 threads, 17.860s elapsed time, 17.797s cpu time, 0.565s GC time, factor 1.00)
20:20:21 Finished CryptoBasedCompositionalProperties (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
20:20:22 Parity_Game: theory HOL-Library.Disjoint_Sets
20:20:22 Parity_Game: theory HOL-Library.Sublist
20:20:22 Parity_Game: theory HOL-Library.Multiset
20:20:22 Running Secondary_Sylow (on 10.195.8.11+1) ...
20:20:22 Parity_Game: theory HOL-Library.Liminf_Limsup
20:20:23 Running RefinementReactive (on 10.195.8.32+1) ...
20:20:23 Parity_Game: theory HOL-Library.Countable
20:20:23 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
20:20:24 Running Youngs_Inequality (on 10.195.8.46+4) ...
20:20:24 RefinementReactive: theory RefinementReactive.Refinement
20:20:24 RefinementReactive: theory RefinementReactive.Temporal
20:20:25 Secondary_Sylow: theory Secondary_Sylow.GroupAction
20:20:25 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
20:20:26 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
20:20:26 Youngs_Inequality: theory Youngs_Inequality.Youngs
20:20:27 Parity_Game: theory HOL-Library.Countable_Set
20:20:27 Secondary_Sylow: theory Secondary_Sylow.SndSylow
20:20:27 Timing VectorSpace (2 threads, 58.707s elapsed time, 58.689s cpu time, 3.990s GC time, factor 1.00)
20:20:27 Finished VectorSpace (0:01:01 elapsed time, 0:01:01 cpu time, factor 0.99)
20:20:29 Parity_Game: theory HOL-Library.Countable_Complete_Lattices
20:20:29 RefinementReactive: theory RefinementReactive.Reactive
20:20:29 Running Van_der_Waerden (on 10.195.8.29+1) ...
20:20:31 Van_der_Waerden: theory HOL-Library.FuncSet
20:20:31 Van_der_Waerden: theory Van_der_Waerden.Digits
20:20:33 Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
20:20:37 Running Recursion-Theory-I (on 10.195.8.40+4) ...
20:20:38 Timing Secondary_Sylow (2 threads, 11.512s elapsed time, 11.480s cpu time, 0.414s GC time, factor 1.00)
20:20:38 Finished Secondary_Sylow (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.97)
20:20:38 Parity_Game: theory HOL-Library.Order_Continuity
20:20:38 Running Tail_Recursive_Functions (on 10.195.6.179+4) ...
20:20:39 Recursion-Theory-I: theory Recursion-Theory-I.CPair
20:20:39 Parity_Game: theory HOL-Combinatorics.Permutations
20:20:40 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun
20:20:40 Parity_Game: theory HOL-Library.Extended_Nat
20:20:40 Running Orbit_Stabiliser (on 10.195.7.194+0) ...
20:20:41 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
20:20:41 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
20:20:43 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
20:20:43 Parity_Game: theory Coinductive.Coinductive_Nat
20:20:43 Parity_Game: theory HOL-Library.Extended_Real
20:20:43 Timing RefinementReactive (2 threads, 17.000s elapsed time, 16.967s cpu time, 0.458s GC time, factor 1.00)
20:20:43 Finished RefinementReactive (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.98)
20:20:43 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
20:20:44 Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet
20:20:44 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2
20:20:44 Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
20:20:45 Recursion-Theory-I: theory Recursion-Theory-I.PRecList
20:20:46 Parity_Game: theory Coinductive.Coinductive_List
20:20:47 Timing Youngs_Inequality (2 threads, 19.459s elapsed time, 19.148s cpu time, 0.458s GC time, factor 0.98)
20:20:47 Finished Youngs_Inequality (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.97)
20:20:48 Timing Randomised_BSTs (2 threads, 23.292s elapsed time, 23.273s cpu time, 0.685s GC time, factor 1.00)
20:20:48 Finished Randomised_BSTs (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.98)
20:20:49 Running Minimal_SSA (on of1-proof+0-7) ...
20:20:50 Timing Van_der_Waerden (2 threads, 17.948s elapsed time, 17.947s cpu time, 0.361s GC time, factor 1.00)
20:20:50 Finished Van_der_Waerden (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
20:20:50 Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr
20:20:50 Timing Fourier (2 threads, 118.198s elapsed time, 118.175s cpu time, 3.974s GC time, factor 1.00)
20:20:50 Finished Fourier (0:02:01 elapsed time, 0:02:01 cpu time, factor 1.00)
20:20:50 Timing Tail_Recursive_Functions (2 threads, 9.772s elapsed time, 9.771s cpu time, 0.615s GC time, factor 1.00)
20:20:50 Finished Tail_Recursive_Functions (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
20:20:51 Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
20:20:51 Minimal_SSA: theory Minimal_SSA.Irreducible
20:20:52 Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
20:20:54 Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet
20:20:55 Timing Minimal_SSA (8 threads, 3.678s elapsed time, 7.761s cpu time, 0.313s GC time, factor 2.11)
20:20:55 Finished Minimal_SSA (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.76)
20:20:56 Parity_Game: theory Graph_Theory.Stuff
20:20:56 Parity_Game: theory Graph_Theory.Digraph
20:20:57 Timing Orbit_Stabiliser (2 threads, 13.501s elapsed time, 13.449s cpu time, 0.397s GC time, factor 1.00)
20:20:57 Finished Orbit_Stabiliser (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.97)
20:20:59 Running Dynamic_Tables (on 10.195.8.11+2) ...
20:21:01 Dynamic_Tables: theory Dynamic_Tables.Tables_real
20:21:01 Parity_Game: theory Graph_Theory.Arc_Walk
20:21:01 Parity_Game: theory Graph_Theory.Bidirected_Digraph
20:21:02 Running InformationFlowSlicing (on 10.195.8.32+3) ...
20:21:02 Running MonoBoolTranAlgebra (on 10.195.8.46+1) ...
20:21:04 MonoBoolTranAlgebra: theory LatticeProperties.Conj_Disj
20:21:04 MonoBoolTranAlgebra: theory LatticeProperties.WellFoundedTransitive
20:21:04 Dynamic_Tables: theory Dynamic_Tables.Tables_nat
20:21:05 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
20:21:05 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
20:21:06 MonoBoolTranAlgebra: theory LatticeProperties.Complete_Lattice_Prop
20:21:07 InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
20:21:07 Parity_Game: theory Graph_Theory.Pair_Digraph
20:21:07 Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
20:21:07 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran
20:21:08 Parity_Game: theory Parity_Game.MoreCoinductiveList
20:21:08 Running Bondy (on 10.195.8.29+1) ...
20:21:09 Parity_Game: theory Parity_Game.ParityGame
20:21:09 Bondy: theory Bondy.Bondy
20:21:10 Padic_Ints: theory Padic_Ints.Hensels_Lemma
20:21:10 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
20:21:11 Timing Bondy (2 threads, 1.051s elapsed time, 1.050s cpu time, 0.024s GC time, factor 1.00)
20:21:11 Finished Bondy (0:00:02 elapsed time)
20:21:11 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
20:21:12 Running Nullstellensatz (on 10.195.8.42+3) ...
20:21:12 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
20:21:14 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
20:21:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
20:21:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
20:21:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
20:21:15 Timing Recursion-Theory-I (2 threads, 35.253s elapsed time, 35.213s cpu time, 1.830s GC time, factor 1.00)
20:21:15 Finished Recursion-Theory-I (0:00:37 elapsed time, 0:00:37 cpu time, factor 0.99)
20:21:15 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
20:21:15 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
20:21:15 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
20:21:16 Parity_Game: theory Parity_Game.Strategy
20:21:16 Timing Dynamic_Tables (2 threads, 14.035s elapsed time, 14.017s cpu time, 0.441s GC time, factor 1.00)
20:21:16 Finished Dynamic_Tables (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
20:21:16 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
20:21:16 Nullstellensatz: theory Nullstellensatz.Univariate_PM
20:21:18 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
20:21:18 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
20:21:18 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Assertion_Algebra
20:21:18 Parity_Game: theory Parity_Game.AttractingStrategy
20:21:19 Running Weight_Balanced_Trees (on 10.195.6.179+3) ...
20:21:19 Parity_Game: theory Parity_Game.WellOrderedStrategy
20:21:19 Parity_Game: theory Parity_Game.WinningStrategy
20:21:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
20:21:19 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Statements
20:21:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
20:21:19 Parity_Game: theory Parity_Game.WinningRegion
20:21:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
20:21:19 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
20:21:19 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
20:21:20 Running Lambda_Free_EPO (on 10.195.8.49+4) ...
20:21:20 Weight_Balanced_Trees: theory HOL-Data_Structures.Cmp
20:21:20 Weight_Balanced_Trees: theory HOL-Data_Structures.Less_False
20:21:20 Weight_Balanced_Trees: theory HOL-Data_Structures.Sorted_Less
20:21:21 Weight_Balanced_Trees: theory HOL-Data_Structures.List_Ins_Del
20:21:21 Running Certification_Monads (on 10.195.7.194+2) ...
20:21:21 Weight_Balanced_Trees: theory HOL-Library.Tree
20:21:22 Weight_Balanced_Trees: theory HOL-Data_Structures.Set_Specs
20:21:22 Timing MonoBoolTranAlgebra (2 threads, 17.005s elapsed time, 16.979s cpu time, 0.577s GC time, factor 1.00)
20:21:22 Finished MonoBoolTranAlgebra (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.98)
20:21:22 Lambda_Free_EPO: theory HOL-Cardinals.Order_Union
20:21:22 Lambda_Free_EPO: theory Nested_Multisets_Ordinals.Multiset_More
20:21:22 Certification_Monads: theory Certification_Monads.Misc
20:21:22 Certification_Monads: theory Deriving.Derive_Manager
20:21:23 Certification_Monads: theory Deriving.Generator_Aux
20:21:23 Certification_Monads: theory HOL-Library.Adhoc_Overloading
20:21:23 Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension
20:21:23 Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util
20:21:23 Certification_Monads: theory Certification_Monads.Error_Syntax
20:21:23 Certification_Monads: theory HOL-Library.Monad_Syntax
20:21:23 Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
20:21:23 Certification_Monads: theory Certification_Monads.Error_Monad
20:21:24 Timing InformationFlowSlicing (2 threads, 18.476s elapsed time, 18.474s cpu time, 0.709s GC time, factor 1.00)
20:21:24 Finished InformationFlowSlicing (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
20:21:24 Certification_Monads: theory Certification_Monads.Strict_Sum
20:21:24 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
20:21:25 Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain
20:21:26 Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders
20:21:26 Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term
20:21:27 Weight_Balanced_Trees: theory HOL-Data_Structures.Tree2
20:21:27 Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees_log
20:21:27 Certification_Monads: theory Certification_Monads.Check_Monad
20:21:28 Certification_Monads: theory Show.Show
20:21:28 Weight_Balanced_Trees: theory HOL-Data_Structures.Isin2
20:21:30 Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees
20:21:30 Certification_Monads: theory Certification_Monads.Parser_Monad
20:21:30 Running DigitsInBase (on of1-proof+8-15) ...
20:21:32 DigitsInBase: theory DigitsInBase.DigitsInBase
20:21:33 Timing DigitsInBase (8 threads, 0.994s elapsed time, 4.133s cpu time, 0.152s GC time, factor 4.16)
20:21:33 Finished DigitsInBase (0:00:02 elapsed time, 0:00:06 cpu time)
20:21:34 Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings
20:21:35 Timing Certification_Monads (2 threads, 11.474s elapsed time, 11.456s cpu time, 0.630s GC time, factor 1.00)
20:21:35 Finished Certification_Monads (0:00:13 elapsed time, 0:00:12 cpu time, factor 0.97)
20:21:35 Timing Probabilistic_Prime_Tests (6 threads, 142.840s elapsed time, 523.623s cpu time, 162.130s GC time, factor 3.67)
20:21:35 Finished Probabilistic_Prime_Tests (0:02:25 elapsed time, 0:08:48 cpu time, factor 3.63)
20:21:35 Parity_Game: theory Parity_Game.Attractor
20:21:35 Parity_Game: theory Parity_Game.UniformStrategy
20:21:35 Parity_Game: theory Parity_Game.AttractorInductive
20:21:36 Parity_Game: theory Parity_Game.AttractorStrategy
20:21:37 Parity_Game: theory Parity_Game.PositionalDeterminacy
20:21:37 Running Category (on 10.195.8.30+3) ...
20:21:38 Lambda_Free_EPO: theory Lambda_Free_EPO.Chop
20:21:38 Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO
20:21:38 Running Concurrent_Ref_Alg (on 10.195.8.11+3) ...
20:21:39 Category: theory HOL-Library.FuncSet
20:21:39 Parity_Game: theory Graph_Theory.Digraph_Component
20:21:40 Timing Nullstellensatz (2 threads, 23.323s elapsed time, 23.080s cpu time, 1.358s GC time, factor 0.99)
20:21:40 Finished Nullstellensatz (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.98)
20:21:40 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Refinement_Lattice
20:21:40 Running Combinatorics_Words_Lyndon (on 10.195.8.32+4) ...
20:21:41 Running MiniML (on 10.195.8.46+0) ...
20:21:41 Category: theory Category.Cat
20:21:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunction
20:21:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Galois_Connections
20:21:42 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
20:21:42 Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
20:21:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Infimum_Nat
20:21:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Parallel
20:21:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Sequential
20:21:43 MiniML: theory MiniML.Maybe
20:21:43 MiniML: theory MiniML.Type
20:21:43 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.CRA
20:21:43 Category: theory Category.Functors
20:21:43 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Sequential
20:21:43 Category: theory Category.SetCat
20:21:44 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Iteration
20:21:45 Category: theory Category.NatTrans
20:21:45 Category: theory Category.HomFunctors
20:21:46 Category: theory Category.Yoneda
20:21:46 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Iteration
20:21:47 Running Lp (on 10.195.8.29+3) ...
20:21:48 MiniML: theory MiniML.Instance
20:21:48 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Rely_Quotient
20:21:48 MiniML: theory MiniML.Generalize
20:21:48 MiniML: theory MiniML.MiniML
20:21:49 Timing Padic_Ints (6 threads, 252.233s elapsed time, 252.169s cpu time, 97.365s GC time, factor 1.00)
20:21:49 Finished Padic_Ints (0:04:30 elapsed time, 0:04:29 cpu time, factor 1.00)
20:21:49 Lp: theory HOL-Library.Function_Algebras
20:21:49 Lp: theory Ergodic_Theory.SG_Library_Complement
20:21:50 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
20:21:50 MiniML: theory MiniML.W
20:21:50 Parity_Game: theory Graph_Theory.Digraph_Isomorphism
20:21:53 Lp: theory Lp.Functional_Spaces
20:21:54 Running CISC-Kernel (on 10.195.8.40+3) ...
20:21:55 Timing Weight_Balanced_Trees (2 threads, 33.695s elapsed time, 33.645s cpu time, 2.730s GC time, factor 1.00)
20:21:55 Finished Weight_Balanced_Trees (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
20:21:56 CISC-Kernel: theory CISC-Kernel.List_Theorems
20:21:56 Timing Category (2 threads, 16.629s elapsed time, 16.601s cpu time, 0.788s GC time, factor 1.00)
20:21:56 Finished Category (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
20:21:56 CISC-Kernel: theory CISC-Kernel.Option_Binders
20:21:56 Parity_Game: theory Parity_Game.Graph_TheoryCompatibility
20:21:56 CISC-Kernel: theory CISC-Kernel.Step_configuration
20:21:56 Running FinFun (on 10.195.7.194+3) ...
20:21:56 CISC-Kernel: theory CISC-Kernel.K
20:21:57 Timing Combinatorics_Words_Lyndon (2 threads, 15.064s elapsed time, 15.036s cpu time, 0.521s GC time, factor 1.00)
20:21:57 Finished Combinatorics_Words_Lyndon (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.98)
20:21:58 FinFun: theory HOL-Library.Phantom_Type
20:21:58 CISC-Kernel: theory CISC-Kernel.SK
20:21:58 Timing Concurrent_Ref_Alg (2 threads, 17.896s elapsed time, 17.832s cpu time, 0.557s GC time, factor 1.00)
20:21:58 Finished Concurrent_Ref_Alg (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
20:22:00 CISC-Kernel: theory CISC-Kernel.Step_policies
20:22:00 CISC-Kernel: theory CISC-Kernel.Step
20:22:01 FinFun: theory HOL-Library.Cardinality
20:22:01 Lp: theory Lp.Lp
20:22:01 Timing MiniML (2 threads, 16.945s elapsed time, 16.923s cpu time, 0.592s GC time, factor 1.00)
20:22:01 Finished MiniML (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.98)
20:22:01 CISC-Kernel: theory CISC-Kernel.ISK
20:22:03 FinFun: theory FinFun.FinFun
20:22:03 CISC-Kernel: theory CISC-Kernel.CISK
20:22:07 FinFun: theory FinFun.FinFunPred
20:22:07 Estimated 0:10:57 build time with default build heuristic (took 1.357s)
20:22:07 Running Automated_Stateful_Protocol_Verification (on of1-proof+8-15) ...
20:22:09 CISC-Kernel: theory CISC-Kernel.Step_invariants
20:22:09 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
20:22:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
20:22:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
20:22:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
20:22:09 CISC-Kernel: theory CISC-Kernel.Step_vpeq
20:22:09 CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects
20:22:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
20:22:09 CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent
20:22:09 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
20:22:09 CISC-Kernel: theory CISC-Kernel.Separation_kernel_model
20:22:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
20:22:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
20:22:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
20:22:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
20:22:11 Timing FinFun (2 threads, 11.792s elapsed time, 11.629s cpu time, 0.418s GC time, factor 0.99)
20:22:11 Finished FinFun (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.96)
20:22:11 Running Implicational_Logic (on of3.proof.cit.tum.de+0-1,3-6) ...
20:22:11 CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK
20:22:12 Implicational_Logic: theory Implicational_Logic.Implicational_Logic
20:22:12 Implicational_Logic: theory Implicational_Logic.Implicational_Logic_Appendix
20:22:13 Timing Implicational_Logic (6 threads, 0.754s elapsed time, 2.482s cpu time, 0.151s GC time, factor 3.29)
20:22:13 Finished Implicational_Logic (0:00:01 elapsed time, 0:00:03 cpu time)
20:22:13 Running Sophomores_Dream (on 10.195.8.30+8-9) ...
20:22:15 Running Laws_of_Large_Numbers (on 10.195.8.11+6-7) ...
20:22:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
20:22:16 Running Pratt_Certificate (on of4.proof.cit.tum.de+6-11) ...
20:22:17 Sophomores_Dream: theory Sophomores_Dream.Sophomores_Dream
20:22:17 Running Card_Equiv_Relations (on 10.195.8.32+2-3) ...
20:22:17 Pratt_Certificate: theory Lehmer.Lehmer
20:22:17 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
20:22:17 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
20:22:18 Running BinarySearchTree (on 10.195.8.46+6-7) ...
20:22:18 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
20:22:19 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
20:22:19 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
20:22:19 BinarySearchTree: theory BinarySearchTree.BinaryTree
20:22:19 BinarySearchTree: theory BinarySearchTree.BinaryTree_TacticStyle
20:22:19 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Equiv_Relations
20:22:20 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
20:22:20 Timing Sophomores_Dream (2 threads, 2.572s elapsed time, 4.292s cpu time, 0.120s GC time, factor 1.67)
20:22:20 Finished Sophomores_Dream (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.24)
20:22:21 Timing Laws_of_Large_Numbers (2 threads, 2.133s elapsed time, 3.349s cpu time, 0.129s GC time, factor 1.57)
20:22:21 Timing Pratt_Certificate (6 threads, 3.384s elapsed time, 14.329s cpu time, 0.354s GC time, factor 4.23)
20:22:21 Finished Laws_of_Large_Numbers (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.17)
20:22:21 Finished Pratt_Certificate (0:00:04 elapsed time, 0:00:15 cpu time, factor 3.21)
20:22:21 BinarySearchTree: theory BinarySearchTree.BinaryTree_Map
20:22:22 Timing Card_Equiv_Relations (2 threads, 1.776s elapsed time, 2.641s cpu time, 0.072s GC time, factor 1.49)
20:22:22 Finished Card_Equiv_Relations (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.13)
20:22:22 Running IEEE_Floating_Point (on of2.proof.cit.tum.de+6-11) ...
20:22:23 IEEE_Floating_Point: theory HOL-Library.Code_Abstract_Nat
20:22:23 IEEE_Floating_Point: theory HOL-Library.Code_Target_Int
20:22:23 IEEE_Floating_Point: theory HOL-Library.Adhoc_Overloading
20:22:23 IEEE_Floating_Point: theory HOL-Library.Log_Nat
20:22:23 IEEE_Floating_Point: theory HOL-Library.Lattice_Algebras
20:22:23 Running Intro_Dest_Elim (on 10.195.8.29+7-8) ...
20:22:23 IEEE_Floating_Point: theory HOL-Library.Monad_Syntax
20:22:23 IEEE_Floating_Point: theory HOL-Library.Code_Target_Nat
20:22:23 IEEE_Floating_Point: theory HOL-Library.Code_Target_Numeral
20:22:25 Intro_Dest_Elim: theory Intro_Dest_Elim.IHOL_IDE
20:22:25 Intro_Dest_Elim: theory HOL-Library.LaTeXsugar
20:22:25 Timing BinarySearchTree (2 threads, 4.957s elapsed time, 8.843s cpu time, 0.453s GC time, factor 1.78)
20:22:25 Finished BinarySearchTree (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.52)
20:22:25 Running Example-Submission (on 10.195.8.42+0-1) ...
20:22:25 Intro_Dest_Elim: theory Intro_Dest_Elim.Reference_Prerequisites
20:22:25 IEEE_Floating_Point: theory HOL-Library.Float
20:22:26 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Reference
20:22:26 Timing Intro_Dest_Elim (2 threads, 1.146s elapsed time, 1.237s cpu time, 0.044s GC time, factor 1.08)
20:22:26 Finished Intro_Dest_Elim (0:00:02 elapsed time)
20:22:27 Example-Submission: theory Example-Submission.Submission
20:22:27 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE
20:22:27 Timing Example-Submission (2 threads, 0.294s elapsed time, 0.373s cpu time, 0.000s GC time, factor 1.27)
20:22:27 Finished Example-Submission (0:00:02 elapsed time)
20:22:29 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Properties
20:22:29 IEEE_Floating_Point: theory IEEE_Floating_Point.FP64
20:22:29 IEEE_Floating_Point: theory IEEE_Floating_Point.Conversion_IEEE_Float
20:22:29 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN
20:22:29 IEEE_Floating_Point: theory IEEE_Floating_Point.Double
20:22:30 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN_SMTLIB
20:22:30 Running Conditional_Simplification (on 10.195.8.40+5-6) ...
20:22:31 Running Depth-First-Search (on 10.195.6.179+7-8) ...
20:22:31 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
20:22:32 Conditional_Simplification: theory Conditional_Simplification.CS_Tools
20:22:32 Conditional_Simplification: theory HOL-Library.LaTeXsugar
20:22:32 Conditional_Simplification: theory Conditional_Simplification.IHOL_CS
20:22:32 Conditional_Simplification: theory Conditional_Simplification.Reference_Prerequisites
20:22:33 Running Descartes_Sign_Rule (on 10.195.7.194+0-1) ...
20:22:33 Conditional_Simplification: theory Conditional_Simplification.CS_Reference
20:22:33 Depth-First-Search: theory Depth-First-Search.DFS
20:22:34 Running FunWithFunctions (on 10.195.8.49+2-3) ...
20:22:34 Timing Conditional_Simplification (2 threads, 1.244s elapsed time, 1.598s cpu time, 0.040s GC time, factor 1.28)
20:22:34 Finished Conditional_Simplification (0:00:02 elapsed time, 0:00:03 cpu time)
20:22:35 Timing IEEE_Floating_Point (6 threads, 10.503s elapsed time, 38.999s cpu time, 2.935s GC time, factor 3.71)
20:22:35 Finished IEEE_Floating_Point (0:00:11 elapsed time, 0:00:40 cpu time, factor 3.45)
20:22:35 FunWithFunctions: theory FunWithFunctions.FunWithFunctions
20:22:35 Timing Depth-First-Search (2 threads, 1.581s elapsed time, 2.304s cpu time, 0.060s GC time, factor 1.46)
20:22:35 Finished Depth-First-Search (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.17)
20:22:35 Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
20:22:37 Timing FunWithFunctions (2 threads, 1.814s elapsed time, 2.922s cpu time, 0.075s GC time, factor 1.61)
20:22:37 Finished FunWithFunctions (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.25)
20:22:40 Timing Descartes_Sign_Rule (2 threads, 4.032s elapsed time, 7.474s cpu time, 0.138s GC time, factor 1.85)
20:22:40 Finished Descartes_Sign_Rule (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.48)
20:22:40 Timing CISC-Kernel (2 threads, 42.620s elapsed time, 42.565s cpu time, 2.505s GC time, factor 1.00)
20:22:41 Finished CISC-Kernel (0:00:45 elapsed time, 0:00:44 cpu time, factor 0.99)
20:22:42 Timing Parity_Game (6 threads, 129.346s elapsed time, 129.329s cpu time, 27.578s GC time, factor 1.00)
20:22:42 Finished Parity_Game (0:02:21 elapsed time, 0:02:21 cpu time, factor 1.00)
20:22:42 Timing Lambda_Free_EPO (2 threads, 78.260s elapsed time, 78.209s cpu time, 5.165s GC time, factor 1.00)
20:22:42 Finished Lambda_Free_EPO (0:01:21 elapsed time, 0:01:20 cpu time, factor 0.99)
20:22:47 Running Lehmer (on of3.proof.cit.tum.de+7-12) ...
20:22:48 Lehmer: theory Lehmer.Lehmer
20:22:49 Timing Lehmer (6 threads, 0.607s elapsed time, 1.206s cpu time, 0.028s GC time, factor 1.99)
20:22:49 Finished Lehmer (0:00:02 elapsed time)
20:22:49 Running ShortestPath (on 10.195.8.30+0-1) ...
20:22:49 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
20:22:50 Running Stewart_Apollonius (on of4.proof.cit.tum.de+6-11) ...
20:22:51 Running ClockSynchInst (on 10.195.8.32+8-9) ...
20:22:51 ShortestPath: theory ShortestPath.ShortestPath
20:22:52 Stewart_Apollonius: theory Triangle.Angles
20:22:52 Stewart_Apollonius: theory Triangle.Triangle
20:22:52 Running ArrowImpossibilityGS (on 10.195.8.46+4-5) ...
20:22:52 Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
20:22:53 ClockSynchInst: theory ClockSynchInst.ICAInstance
20:22:53 ClockSynchInst: theory ClockSynchInst.LynchInstance
20:22:53 Timing Stewart_Apollonius (6 threads, 1.374s elapsed time, 2.952s cpu time, 0.111s GC time, factor 2.15)
20:22:53 Finished Stewart_Apollonius (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.43)
20:22:54 ArrowImpossibilityGS: theory HOL-Library.FuncSet
20:22:54 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Utility
20:22:54 ShortestPath: theory ShortestPath.ShortestPathNeg
20:22:55 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Order
20:22:56 ArrowImpossibilityGS: theory ArrowImpossibilityGS.GS
20:22:56 Timing Lp (2 threads, 65.966s elapsed time, 65.921s cpu time, 1.445s GC time, factor 1.00)
20:22:56 Finished Lp (0:01:09 elapsed time, 0:01:08 cpu time, factor 0.99)
20:22:57 Running Selection_Heap_Sort (on of2.proof.cit.tum.de+6-11) ...
20:22:59 Running General-Triangle (on 10.195.8.29+0-1) ...
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
20:22:59 Timing ShortestPath (2 threads, 5.906s elapsed time, 7.904s cpu time, 0.447s GC time, factor 1.34)
20:22:59 Finished ShortestPath (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.20)
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
20:22:59 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
20:23:00 Timing ClockSynchInst (2 threads, 5.158s elapsed time, 9.144s cpu time, 0.229s GC time, factor 1.77)
20:23:00 Finished ClockSynchInst (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.52)
20:23:00 General-Triangle: theory General-Triangle.GeneralTriangle
20:23:00 Running FFT (on 10.195.8.42+2,4) ...
20:23:01 Timing General-Triangle (2 threads, 0.938s elapsed time, 1.366s cpu time, 0.026s GC time, factor 1.46)
20:23:01 Finished General-Triangle (0:00:02 elapsed time)
20:23:02 FFT: theory FFT.FFT
20:23:02 Timing Selection_Heap_Sort (6 threads, 2.908s elapsed time, 11.467s cpu time, 0.809s GC time, factor 3.94)
20:23:02 Finished Selection_Heap_Sort (0:00:04 elapsed time, 0:00:12 cpu time, factor 3.05)
20:23:04 Timing ArrowImpossibilityGS (2 threads, 9.013s elapsed time, 17.107s cpu time, 1.295s GC time, factor 1.90)
20:23:04 Finished ArrowImpossibilityGS (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.73)
20:23:04 Timing FFT (2 threads, 1.973s elapsed time, 3.564s cpu time, 0.080s GC time, factor 1.81)
20:23:04 Finished FFT (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.37)
20:23:05 Running CofGroups (on 10.195.8.40+0-1) ...
20:23:06 Running DCR-ExecutionEquivalence (on 10.195.6.179+0-1) ...
20:23:07 CofGroups: theory HOL-Library.Nat_Bijection
20:23:07 Running Discrete_Summation (on 10.195.7.194+2,4) ...
20:23:08 CofGroups: theory CofGroups.CofGroups
20:23:08 DCR-ExecutionEquivalence: theory DCR-ExecutionEquivalence.DCRExecutionEquivalence
20:23:09 Running Gauss-Jordan-Elim-Fun (on 10.195.8.49+5-6) ...
20:23:09 Discrete_Summation: theory Discrete_Summation.Discrete_Summation
20:23:09 Discrete_Summation: theory HOL-Combinatorics.Stirling
20:23:10 Discrete_Summation: theory Discrete_Summation.Factorials
20:23:10 Timing CofGroups (2 threads, 2.307s elapsed time, 4.128s cpu time, 0.126s GC time, factor 1.79)
20:23:10 Finished CofGroups (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.40)
20:23:10 Gauss-Jordan-Elim-Fun: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
20:23:10 Discrete_Summation: theory Discrete_Summation.Summation_Conversion
20:23:11 Discrete_Summation: theory Discrete_Summation.Examples
20:23:12 Timing DCR-ExecutionEquivalence (2 threads, 2.890s elapsed time, 3.347s cpu time, 0.151s GC time, factor 1.16)
20:23:12 Finished DCR-ExecutionEquivalence (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.04)
20:23:14 Timing Discrete_Summation (2 threads, 4.822s elapsed time, 8.950s cpu time, 0.196s GC time, factor 1.86)
20:23:14 Finished Discrete_Summation (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.57)
20:23:15 Timing Gauss-Jordan-Elim-Fun (2 threads, 4.115s elapsed time, 5.755s cpu time, 0.134s GC time, factor 1.40)
20:23:15 Finished Gauss-Jordan-Elim-Fun (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.23)
20:23:22 Running Lucas_Theorem (on of3.proof.cit.tum.de+7-12) ...
20:23:24 Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem
20:23:24 Running Roy_Floyd_Warshall (on 10.195.8.30+8-9) ...
20:23:25 Timing Lucas_Theorem (6 threads, 0.713s elapsed time, 1.912s cpu time, 0.049s GC time, factor 2.68)
20:23:25 Finished Lucas_Theorem (0:00:02 elapsed time, 0:00:03 cpu time)
20:23:26 Running AnselmGod (on of4.proof.cit.tum.de+6-11) ...
20:23:26 Roy_Floyd_Warshall: theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
20:23:27 AnselmGod: theory AnselmGod.AnselmGod
20:23:27 Running Card_Number_Partitions (on 10.195.8.32+4-5) ...
20:23:27 Timing Roy_Floyd_Warshall (2 threads, 1.011s elapsed time, 1.585s cpu time, 0.046s GC time, factor 1.57)
20:23:27 Finished Roy_Floyd_Warshall (0:00:02 elapsed time, 0:00:03 cpu time)
20:23:28 Timing AnselmGod (6 threads, 0.602s elapsed time, 1.366s cpu time, 0.065s GC time, factor 2.27)
20:23:28 Finished AnselmGod (0:00:01 elapsed time)
20:23:28 Running Binary_Code_Imprimitive (on 10.195.8.46+8-9) ...
20:23:29 Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
20:23:30 Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
20:23:30 Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
20:23:30 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Square_Interpretation
20:23:30 Binary_Code_Imprimitive: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
20:23:32 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Code_Imprimitive
20:23:32 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Imprimitive_Decision
20:23:33 Running DOM_Components (on of2.proof.cit.tum.de+0-5) ...
20:23:34 Running Hello_World (on 10.195.8.29+5-6) ...
20:23:35 Timing Card_Number_Partitions (2 threads, 5.003s elapsed time, 9.271s cpu time, 0.197s GC time, factor 1.85)
20:23:35 Finished Card_Number_Partitions (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.51)
20:23:35 DOM_Components: theory DOM_Components.Core_DOM_Components
20:23:35 DOM_Components: theory DOM_Components.fancy_tabs
20:23:36 Hello_World: theory HOL-Library.Adhoc_Overloading
20:23:36 Running Liouville_Numbers (on 10.195.8.42+3,9) ...
20:23:36 Hello_World: theory HOL-Library.Monad_Syntax
20:23:36 Hello_World: theory Hello_World.IO
20:23:36 Hello_World: theory Hello_World.HelloWorld
20:23:38 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
20:23:39 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
20:23:39 Hello_World: theory Hello_World.HelloWorld_Proof
20:23:40 Hello_World: theory Hello_World.RunningCodeFromIsabelle
20:23:41 DOM_Components: theory DOM_Components.Shadow_DOM_Components
20:23:41 Timing Hello_World (2 threads, 5.038s elapsed time, 2.632s cpu time, 0.077s GC time, factor 0.52)
20:23:41 Running Compiling-Exceptions-Correctly (on 10.195.8.40+2,4) ...
20:23:41 Finished Hello_World (0:00:06 elapsed time, 0:00:04 cpu time, factor 0.59)
20:23:41 Timing Binary_Code_Imprimitive (2 threads, 10.481s elapsed time, 18.668s cpu time, 0.720s GC time, factor 1.78)
20:23:41 Finished Binary_Code_Imprimitive (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.62)
20:23:42 Timing Liouville_Numbers (2 threads, 2.741s elapsed time, 4.409s cpu time, 0.113s GC time, factor 1.61)
20:23:42 Finished Liouville_Numbers (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.23)
20:23:42 Running DPT-SAT-Solver (on 10.195.6.179+2,4) ...
20:23:43 Compiling-Exceptions-Correctly: theory Compiling-Exceptions-Correctly.Exceptions
20:23:43 Running Nano_JSON (on 10.195.7.194+3,9) ...
20:23:43 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Solver
20:23:44 Running GenClock (on 10.195.8.49+7-8) ...
20:23:45 Nano_JSON: theory Nano_JSON.Nano_JSON
20:23:45 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Tests
20:23:45 GenClock: theory GenClock.GenClock
20:23:47 Nano_JSON: theory Nano_JSON.Nano_JSON_Query
20:23:47 Timing Compiling-Exceptions-Correctly (2 threads, 4.165s elapsed time, 6.664s cpu time, 0.404s GC time, factor 1.60)
20:23:47 Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.38)
20:23:48 Nano_JSON: theory Nano_JSON.Nano_JSON_Main
20:23:48 Nano_JSON: theory Nano_JSON.Example
20:23:48 Nano_JSON: theory Nano_JSON.Example_Real
20:23:48 Nano_JSON: theory Nano_JSON.Nano_JSON_Manual
20:23:49 Timing DPT-SAT-Solver (2 threads, 4.724s elapsed time, 7.141s cpu time, 0.166s GC time, factor 1.51)
20:23:49 Finished DPT-SAT-Solver (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.35)
20:23:50 Timing Nano_JSON (2 threads, 4.501s elapsed time, 7.142s cpu time, 0.388s GC time, factor 1.59)
20:23:50 Finished Nano_JSON (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.37)
20:23:50 Timing GenClock (2 threads, 4.446s elapsed time, 8.002s cpu time, 0.181s GC time, factor 1.80)
20:23:50 Finished GenClock (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.55)
20:23:58 Running Open_Induction (on of3.proof.cit.tum.de+7-12) ...
20:23:58 Open_Induction: theory Open_Induction.Restricted_Predicates
20:23:59 Open_Induction: theory Open_Induction.Open_Induction
20:23:59 Running Verified-Prover (on 10.195.8.30+0-1) ...
20:24:00 Timing Open_Induction (6 threads, 0.941s elapsed time, 2.626s cpu time, 0.095s GC time, factor 2.79)
20:24:00 Finished Open_Induction (0:00:02 elapsed time, 0:00:03 cpu time)
20:24:01 Verified-Prover: theory Verified-Prover.Prover
20:24:01 Running Blue_Eyes (on of4.proof.cit.tum.de+6-11) ...
20:24:02 Blue_Eyes: theory Blue_Eyes.Blue_Eyes
20:24:03 Running Stream-Fusion (on 10.195.8.32+8-9) ...
20:24:03 Timing Blue_Eyes (6 threads, 0.590s elapsed time, 1.177s cpu time, 0.051s GC time, factor 1.99)
20:24:03 Finished Blue_Eyes (0:00:01 elapsed time)
20:24:03 Running Sunflowers (on 10.195.8.46+6-7) ...
20:24:05 Stream-Fusion: theory HOLCF-Library.Int_Discrete
20:24:05 Stream-Fusion: theory Stream-Fusion.LazyList
20:24:05 Sunflowers: theory HOL-Library.FuncSet
20:24:06 Sunflowers: theory Sunflowers.Sunflower
20:24:06 Stream-Fusion: theory Stream-Fusion.Stream
20:24:06 Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
20:24:08 Stream-Fusion: theory Stream-Fusion.StreamFusion
20:24:09 Running Ordinals_and_Cardinals (on 10.195.8.29+5-6) ...
20:24:11 Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
20:24:11 Running List_Interleaving (on 10.195.8.42+0-1) ...
20:24:11 Timing Ordinals_and_Cardinals (2 threads, 0.119s elapsed time, 0.185s cpu time, 0.000s GC time, factor 1.55)
20:24:11 Finished Ordinals_and_Cardinals (0:00:01 elapsed time)
20:24:12 List_Interleaving: theory List_Interleaving.ListInterleaving
20:24:13 Timing Sunflowers (2 threads, 7.305s elapsed time, 12.455s cpu time, 0.294s GC time, factor 1.70)
20:24:13 Finished Sunflowers (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.53)
20:24:15 Timing Stream-Fusion (2 threads, 9.670s elapsed time, 12.395s cpu time, 0.620s GC time, factor 1.28)
20:24:15 Finished Stream-Fusion (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.21)
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
20:24:15 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
20:24:16 Running Max-Card-Matching (on 10.195.8.40+5-6) ...
20:24:16 Timing Verified-Prover (2 threads, 14.644s elapsed time, 19.355s cpu time, 1.411s GC time, factor 1.32)
20:24:16 Finished Verified-Prover (0:00:16 elapsed time, 0:00:21 cpu time, factor 1.28)
20:24:17 Running DataRefinementIBP (on 10.195.6.179+5-6) ...
20:24:18 Timing List_Interleaving (2 threads, 4.351s elapsed time, 7.602s cpu time, 0.351s GC time, factor 1.75)
20:24:18 Max-Card-Matching: theory Max-Card-Matching.Matching
20:24:18 Finished List_Interleaving (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.47)
20:24:18 Running Boolos_Curious_Inference (on 10.195.7.194+3,9) ...
20:24:18 DataRefinementIBP: theory LatticeProperties.WellFoundedTransitive
20:24:18 DataRefinementIBP: theory LatticeProperties.Conj_Disj
20:24:19 DataRefinementIBP: theory LatticeProperties.Complete_Lattice_Prop
20:24:19 Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo1
20:24:20 Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo2
20:24:20 Running Stuttering_Equivalence (on 10.195.8.49+7-8) ...
20:24:20 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
20:24:20 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
20:24:21 DataRefinementIBP: theory DataRefinementIBP.Preliminaries
20:24:21 DataRefinementIBP: theory DataRefinementIBP.Statements
20:24:21 DataRefinementIBP: theory DataRefinementIBP.Hoare
20:24:21 DataRefinementIBP: theory DataRefinementIBP.Diagram
20:24:22 Timing Boolos_Curious_Inference (2 threads, 0.837s elapsed time, 1.317s cpu time, 0.045s GC time, factor 1.57)
20:24:22 Timing Max-Card-Matching (2 threads, 2.469s elapsed time, 3.863s cpu time, 0.074s GC time, factor 1.56)
20:24:22 Finished Max-Card-Matching (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.26)
20:24:22 Finished Boolos_Curious_Inference (0:00:02 elapsed time)
20:24:22 DataRefinementIBP: theory DataRefinementIBP.DataRefinement
20:24:23 Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
20:24:23 Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
20:24:23 Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
20:24:24 Timing DataRefinementIBP (2 threads, 4.431s elapsed time, 7.329s cpu time, 0.195s GC time, factor 1.65)
20:24:24 Finished DataRefinementIBP (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.44)
20:24:29 Timing Stuttering_Equivalence (2 threads, 5.555s elapsed time, 8.589s cpu time, 0.269s GC time, factor 1.55)
20:24:29 Finished Stuttering_Equivalence (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.35)
20:24:34 Running RIPEMD-160-SPARK (on of3.proof.cit.tum.de+7-12) ...
20:24:35 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
20:24:36 Timing RIPEMD-160-SPARK (6 threads, 0.576s elapsed time, 0.645s cpu time, 0.010s GC time, factor 1.12)
20:24:36 Finished RIPEMD-160-SPARK (0:00:01 elapsed time)
20:24:36 Running VolpanoSmith (on 10.195.8.30+8-9) ...
20:24:38 VolpanoSmith: theory VolpanoSmith.Semantics
20:24:38 Running Combinatorics_Words_Graph_Lemma (on of4.proof.cit.tum.de+6-11) ...
20:24:39 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
20:24:39 Running Card_Partitions (on 10.195.8.32+6-7) ...
20:24:39 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
20:24:40 Running Abstract-Hoare-Logics (on 10.195.8.46+0-1) ...
20:24:40 Timing Combinatorics_Words_Graph_Lemma (6 threads, 0.552s elapsed time, 1.348s cpu time, 0.056s GC time, factor 2.44)
20:24:40 Finished Combinatorics_Words_Graph_Lemma (0:00:01 elapsed time)
20:24:41 Card_Partitions: theory HOL-Combinatorics.Stirling
20:24:41 Card_Partitions: theory HOL-Eisbach.Eisbach
20:24:41 Card_Partitions: theory HOL-Library.Adhoc_Overloading
20:24:42 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Lang
20:24:42 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PLang
20:24:42 Card_Partitions: theory HOL-Library.Monad_Syntax
20:24:42 Card_Partitions: theory HOL-Library.FuncSet
20:24:43 VolpanoSmith: theory VolpanoSmith.secTypes
20:24:43 Card_Partitions: theory HOL-Library.Disjoint_Sets
20:24:43 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Hoare
20:24:43 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Termi
20:24:44 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.HoareTotal
20:24:44 Card_Partitions: theory Card_Partitions.Injectivity_Solver
20:24:44 Card_Partitions: theory Card_Partitions.Set_Partition
20:24:44 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoare
20:24:44 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PTermi
20:24:44 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsLang
20:24:44 Card_Partitions: theory Card_Partitions.Card_Partitions
20:24:44 VolpanoSmith: theory VolpanoSmith.Execute
20:24:45 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoareTotal
20:24:45 Running Marriage (on 10.195.8.29+0-1) ...
20:24:47 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoare
20:24:47 Marriage: theory Marriage.Marriage
20:24:47 Running Perfect-Number-Thm (on 10.195.8.42+3,9) ...
20:24:47 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsTermi
20:24:48 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoareTotal
20:24:49 Timing VolpanoSmith (2 threads, 10.999s elapsed time, 19.296s cpu time, 1.588s GC time, factor 1.75)
20:24:49 Finished VolpanoSmith (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.63)
20:24:50 Timing Marriage (2 threads, 2.624s elapsed time, 4.478s cpu time, 0.094s GC time, factor 1.71)
20:24:50 Finished Marriage (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.35)
20:24:50 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
20:24:50 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
20:24:51 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
20:24:52 Running Cotangent_PFD_Formula (on 10.195.8.40+7-8) ...
20:24:53 Running List-Index (on 10.195.6.179+3,9) ...
20:24:54 Timing Perfect-Number-Thm (2 threads, 3.341s elapsed time, 4.977s cpu time, 0.086s GC time, factor 1.49)
20:24:54 Finished Perfect-Number-Thm (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.20)
20:24:54 Running TortoiseHare (on 10.195.7.194+0-1) ...
20:24:55 List-Index: theory List-Index.List_Index
20:24:55 Running MuchAdoAboutTwo (on 10.195.8.49+2-3) ...
20:24:55 Cotangent_PFD_Formula: theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
20:24:55 Timing DOM_Components (6 threads, 80.075s elapsed time, 399.534s cpu time, 19.041s GC time, factor 4.99)
20:24:55 Finished DOM_Components (0:01:22 elapsed time, 0:06:43 cpu time, factor 4.91)
20:24:56 Timing Card_Partitions (2 threads, 14.306s elapsed time, 25.570s cpu time, 0.777s GC time, factor 1.79)
20:24:56 Finished Card_Partitions (0:00:16 elapsed time, 0:00:27 cpu time, factor 1.69)
20:24:56 TortoiseHare: theory TortoiseHare.Basis
20:24:57 TortoiseHare: theory TortoiseHare.Brent
20:24:57 MuchAdoAboutTwo: theory HOL-Combinatorics.Transposition
20:24:57 TortoiseHare: theory TortoiseHare.TortoiseHare
20:24:58 MuchAdoAboutTwo: theory HOL-Combinatorics.Permutations
20:24:59 Timing List-Index (2 threads, 3.622s elapsed time, 6.279s cpu time, 0.160s GC time, factor 1.73)
20:24:59 Finished List-Index (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.46)
20:24:59 MuchAdoAboutTwo: theory MuchAdoAboutTwo.MuchAdoAboutTwo
20:25:00 Timing Cotangent_PFD_Formula (2 threads, 4.483s elapsed time, 6.307s cpu time, 0.166s GC time, factor 1.41)
20:25:00 Finished Cotangent_PFD_Formula (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.20)
20:25:01 Timing Abstract-Hoare-Logics (2 threads, 18.426s elapsed time, 32.204s cpu time, 2.717s GC time, factor 1.75)
20:25:01 Finished Abstract-Hoare-Logics (0:00:20 elapsed time, 0:00:34 cpu time, factor 1.66)
20:25:03 Timing TortoiseHare (2 threads, 6.002s elapsed time, 9.829s cpu time, 0.306s GC time, factor 1.64)
20:25:03 Finished TortoiseHare (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.42)
20:25:07 Estimated 0:06:06 build time with default build heuristic (took 0.413s)
20:25:08 Timing MuchAdoAboutTwo (2 threads, 9.377s elapsed time, 16.530s cpu time, 0.691s GC time, factor 1.76)
20:25:08 Finished MuchAdoAboutTwo (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.60)
20:25:10 Running Smooth_Manifolds (on of3.proof.cit.tum.de+6-11) ...
20:25:11 Smooth_Manifolds: theory HOL-Library.Function_Algebras
20:25:11 Smooth_Manifolds: theory HOL-Library.Quotient_Syntax
20:25:11 Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites
20:25:11 Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets
20:25:11 Smooth_Manifolds: theory HOL-Library.Quotient_Set
20:25:11 Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With
20:25:12 Running Euler_Partition (on 10.195.8.30+4-5) ...
20:25:12 Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With
20:25:12 Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On
20:25:13 Running C2KA_DistributedSystems (on 10.195.8.11+2-3) ...
20:25:13 Euler_Partition: theory HOL-Library.Cancellation
20:25:14 Running Minkowskis_Theorem (on 10.195.8.32+6-7) ...
20:25:14 C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
20:25:14 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
20:25:15 Euler_Partition: theory HOL-Library.Multiset
20:25:15 Running LatticeProperties (on 10.195.8.46+8-9) ...
20:25:17 C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
20:25:17 LatticeProperties: theory LatticeProperties.Conj_Disj
20:25:17 LatticeProperties: theory LatticeProperties.Lattice_Prop
20:25:17 Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More
20:25:17 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
20:25:17 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
20:25:17 Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
20:25:18 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice
20:25:18 LatticeProperties: theory LatticeProperties.WellFoundedTransitive
20:25:18 Smooth_Manifolds: theory Smooth_Manifolds.Chart
20:25:18 Smooth_Manifolds: theory Smooth_Manifolds.Smooth
20:25:18 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop
20:25:19 Timing C2KA_DistributedSystems (2 threads, 3.997s elapsed time, 5.545s cpu time, 0.227s GC time, factor 1.39)
20:25:19 Finished C2KA_DistributedSystems (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.21)
20:25:19 Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold
20:25:19 Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function
20:25:19 Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold
20:25:20 Running Padic_Field (on of2.proof.cit.tum.de+6-11) ...
20:25:20 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group
20:25:20 Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity
20:25:20 Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold
20:25:20 Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space
20:25:20 Smooth_Manifolds: theory Smooth_Manifolds.Sphere
20:25:21 Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space
20:25:21 Euler_Partition: theory Card_Number_Partitions.Additions_to_Main
20:25:21 Running Aristotles_Assertoric_Syllogistic (on 10.195.8.29+8-9) ...
20:25:21 Euler_Partition: theory Card_Number_Partitions.Number_Partition
20:25:21 Timing Minkowskis_Theorem (2 threads, 2.974s elapsed time, 5.021s cpu time, 0.116s GC time, factor 1.69)
20:25:21 Finished Minkowskis_Theorem (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.27)
20:25:21 Padic_Field: theory Padic_Field.Cring_Multivariable_Poly
20:25:21 Padic_Field: theory Localization_Ring.Localization
20:25:21 Padic_Field: theory Padic_Field.Generated_Boolean_Algebra
20:25:21 Padic_Field: theory Padic_Field.Indices
20:25:21 Euler_Partition: theory Euler_Partition.Euler_Partition
20:25:22 Padic_Field: theory Padic_Field.Fraction_Field
20:25:22 Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
20:25:23 Running Triangle (on 10.195.8.42+7-8) ...
20:25:23 Timing LatticeProperties (2 threads, 5.274s elapsed time, 9.728s cpu time, 0.316s GC time, factor 1.84)
20:25:23 Finished LatticeProperties (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.57)
20:25:24 Timing Aristotles_Assertoric_Syllogistic (2 threads, 0.714s elapsed time, 1.151s cpu time, 0.035s GC time, factor 1.61)
20:25:24 Finished Aristotles_Assertoric_Syllogistic (0:00:02 elapsed time)
20:25:25 Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space
20:25:25 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
20:25:26 Triangle: theory Triangle.Angles
20:25:27 Triangle: theory Triangle.Triangle
20:25:28 Running Pairing_Heap (on 10.195.8.40+4-5) ...
20:25:28 Timing Smooth_Manifolds (6 threads, 16.391s elapsed time, 58.636s cpu time, 6.715s GC time, factor 3.58)
20:25:28 Finished Smooth_Manifolds (0:00:18 elapsed time, 0:01:00 cpu time, factor 3.36)
20:25:29 Running Sauer_Shelah_Lemma (on 10.195.6.179+5-6) ...
20:25:29 Padic_Field: theory Padic_Field.Padic_Fields
20:25:30 Running Szpilrajn (on 10.195.7.194+8-9) ...
20:25:30 Pairing_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
20:25:31 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Binomial_Lemmas
20:25:31 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Card_Lemmas
20:25:31 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List2
20:25:31 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List1
20:25:31 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Shattering
20:25:31 Running VeriComp (on 10.195.8.49+8-9) ...
20:25:31 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Sauer_Shelah_Lemma
20:25:32 Szpilrajn: theory Szpilrajn.Szpilrajn
20:25:32 Timing Triangle (2 threads, 5.562s elapsed time, 7.373s cpu time, 0.267s GC time, factor 1.33)
20:25:32 Finished Triangle (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.17)
20:25:33 VeriComp: theory VeriComp.Behaviour
20:25:33 VeriComp: theory VeriComp.Transfer_Extras
20:25:33 VeriComp: theory VeriComp.Well_founded
20:25:33 VeriComp: theory VeriComp.Inf
20:25:33 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_Tree
20:25:33 VeriComp: theory VeriComp.Lifting_Simulation_To_Bisimulation
20:25:33 Timing Sauer_Shelah_Lemma (2 threads, 1.971s elapsed time, 3.515s cpu time, 0.064s GC time, factor 1.78)
20:25:33 Finished Sauer_Shelah_Lemma (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.31)
20:25:34 VeriComp: theory VeriComp.Semantics
20:25:35 VeriComp: theory VeriComp.Language
20:25:35 VeriComp: theory VeriComp.Simulation
20:25:36 VeriComp: theory VeriComp.Compiler
20:25:36 Timing Euler_Partition (2 threads, 21.387s elapsed time, 36.676s cpu time, 1.486s GC time, factor 1.71)
20:25:36 Finished Euler_Partition (0:00:23 elapsed time, 0:00:38 cpu time, factor 1.64)
20:25:36 Timing Pairing_Heap (2 threads, 5.142s elapsed time, 9.451s cpu time, 0.774s GC time, factor 1.84)
20:25:36 Finished Pairing_Heap (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.52)
20:25:36 VeriComp: theory VeriComp.Fixpoint
20:25:37 Timing Szpilrajn (2 threads, 4.806s elapsed time, 6.990s cpu time, 0.192s GC time, factor 1.45)
20:25:37 Finished Szpilrajn (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.28)
20:25:40 Timing VeriComp (2 threads, 6.836s elapsed time, 12.743s cpu time, 0.569s GC time, factor 1.86)
20:25:40 Finished VeriComp (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.67)
20:25:42 Padic_Field: theory Padic_Field.Ring_Powers
20:25:45 Running Collections_Examples (on of3.proof.cit.tum.de+0-5) ...
20:25:46 Collections_Examples: theory Collections_Examples.Examples_Chapter
20:25:46 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples_Chapter
20:25:46 Collections_Examples: theory Collections_Examples.ICF_Examples_Chapter
20:25:46 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples_Chapter
20:25:46 Collections_Examples: theory Containers.Equal
20:25:46 Collections_Examples: theory Containers.Extend_Partial_Order
20:25:46 Collections_Examples: theory Containers.List_Fusion
20:25:46 Collections_Examples: theory Deriving.Derive_Manager
20:25:46 Collections_Examples: theory Deriving.Generator_Aux
20:25:46 Collections_Examples: theory Deriving.Comparator
20:25:46 Collections_Examples: theory HOL-Library.DAList
20:25:46 Collections_Examples: theory Containers.Closure_Set
20:25:46 Collections_Examples: theory Containers.Containers_Auxiliary
20:25:46 Collections_Examples: theory Deriving.Equality_Generator
20:25:46 Collections_Examples: theory HOL-Library.Char_ord
20:25:46 Collections_Examples: theory HOL-Library.Omega_Words_Fun
20:25:47 Collections_Examples: theory HOL-Library.Mapping
20:25:47 Collections_Examples: theory Deriving.Equality_Instances
20:25:47 Collections_Examples: theory Containers.Containers_Generator
20:25:47 Collections_Examples: theory Deriving.Compare
20:25:47 Collections_Examples: theory Deriving.Comparator_Generator
20:25:47 Collections_Examples: theory Containers.AssocList
20:25:47 Collections_Examples: theory CAVA_Automata.Digraph_Basic
20:25:47 Collections_Examples: theory Containers.Lexicographic_Order
20:25:47 Collections_Examples: theory Containers.Collection_Enum
20:25:48 Running Cartan_FP (on 10.195.8.11+6-7) ...
20:25:48 Collections_Examples: theory Containers.Collection_Eq
20:25:48 Collections_Examples: theory Containers.Set_Linorder
20:25:48 Collections_Examples: theory Deriving.Compare_Generator
20:25:48 Collections_Examples: theory Containers.RBT_ext
20:25:48 Collections_Examples: theory Deriving.RBT_Comparator_Impl
20:25:48 Collections_Examples: theory Deriving.Compare_Instances
20:25:48 Collections_Examples: theory HOL-Library.Uprod
20:25:48 Collections_Examples: theory Containers.DList_Set
20:25:48 Collections_Examples: theory Collections_Examples.Bfs_Impl
20:25:49 Collections_Examples: theory Containers.TwoSat_Ex
20:25:49 Collections_Examples: theory Collections_Examples.Foreach_Refine
20:25:49 Collections_Examples: theory Collections_Examples.ICF_Only_Test
20:25:49 Collections_Examples: theory Collections_Examples.Refine_Fold
20:25:50 Collections_Examples: theory Collections_Examples.Exploration
20:25:50 Collections_Examples: theory Collections_Examples.Exploration_DFS
20:25:50 Cartan_FP: theory Cartan_FP.Cartan
20:25:51 Running Irrationals_From_THEBOOK (on 10.195.8.46+4-5) ...
20:25:52 Collections_Examples: theory Collections_Examples.PerformanceTest
20:25:53 Collections_Examples: theory Collections_Examples.itp_2010
20:25:53 Collections_Examples: theory Collections_Examples.Simple_DFS
20:25:53 Collections_Examples: theory Collections_Examples.Succ_Graph
20:25:54 Timing Cartan_FP (2 threads, 3.209s elapsed time, 4.897s cpu time, 0.127s GC time, factor 1.53)
20:25:54 Finished Cartan_FP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.22)
20:25:54 Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
20:25:55 Collections_Examples: theory Containers.Collection_Order
20:25:55 Padic_Field: theory Padic_Field.Padic_Field_Polynomials
20:25:55 Padic_Field: theory Padic_Field.Padic_Field_Topology
20:25:56 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
20:25:57 Collections_Examples: theory Collections_Examples.ICF_Test
20:25:57 Running Weighted_Arithmetic_Geometric_Mean (on 10.195.8.29+2-3) ...
20:25:57 Collections_Examples: theory Containers.RBT_Mapping2
20:25:58 Collections_Examples: theory Containers.RBT_Set2
20:25:58 Weighted_Arithmetic_Geometric_Mean: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
20:25:58 Collections_Examples: theory Collections_Examples.ICF_Examples
20:25:58 Collections_Examples: theory Collections_Examples.Coll_Test
20:25:58 Running Chord_Segments (on 10.195.8.42+3,9) ...
20:25:59 Collections_Examples: theory Collections_Examples.Nested_DFS
20:25:59 Collections_Examples: theory Containers.Set_Impl
20:26:00 Timing Weighted_Arithmetic_Geometric_Mean (2 threads, 1.784s elapsed time, 2.912s cpu time, 0.065s GC time, factor 1.63)
20:26:00 Finished Weighted_Arithmetic_Geometric_Mean (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.26)
20:26:00 Timing Irrationals_From_THEBOOK (2 threads, 5.217s elapsed time, 7.335s cpu time, 0.154s GC time, factor 1.41)
20:26:00 Finished Irrationals_From_THEBOOK (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.21)
20:26:01 Chord_Segments: theory Triangle.Angles
20:26:02 Chord_Segments: theory Triangle.Triangle
20:26:03 Chord_Segments: theory Chord_Segments.Chord_Segments
20:26:04 Running Falling_Factorial_Sum (on 10.195.8.40+7-8) ...
20:26:04 Running Ptolemys_Theorem (on 10.195.6.179+2,4) ...
20:26:05 Running Fresh_Identifiers (on 10.195.7.194+0-1) ...
20:26:06 Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
20:26:06 Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
20:26:06 Running Mereology (on 10.195.8.49+2-3) ...
20:26:06 Falling_Factorial_Sum: theory Discrete_Summation.Factorials
20:26:07 Fresh_Identifiers: theory Fresh_Identifiers.Fresh
20:26:07 Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
20:26:07 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
20:26:07 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
20:26:07 Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
20:26:07 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
20:26:07 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
20:26:07 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
20:26:08 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
20:26:08 Mereology: theory Mereology.PM
20:26:08 Mereology: theory Mereology.M
20:26:08 Mereology: theory Mereology.CM
20:26:09 Mereology: theory Mereology.MM
20:26:09 Timing Chord_Segments (2 threads, 6.932s elapsed time, 9.305s cpu time, 0.352s GC time, factor 1.34)
20:26:09 Finished Chord_Segments (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.22)
20:26:09 Mereology: theory Mereology.EM
20:26:09 Mereology: theory Mereology.GM
20:26:09 Mereology: theory Mereology.GMM
20:26:09 Mereology: theory Mereology.CEM
20:26:10 Mereology: theory Mereology.GEM
20:26:10 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples
20:26:10 Timing Ptolemys_Theorem (2 threads, 2.411s elapsed time, 3.556s cpu time, 0.078s GC time, factor 1.47)
20:26:10 Finished Ptolemys_Theorem (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.15)
20:26:11 Collections_Examples: theory Containers.Mapping_Impl
20:26:11 Timing Automated_Stateful_Protocol_Verification (8 threads, 235.139s elapsed time, 930.762s cpu time, 167.428s GC time, factor 3.96)
20:26:11 Finished Automated_Stateful_Protocol_Verification (0:04:01 elapsed time, 0:16:00 cpu time, factor 3.98)
20:26:12 Timing Fresh_Identifiers (2 threads, 4.363s elapsed time, 7.342s cpu time, 0.140s GC time, factor 1.68)
20:26:12 Finished Fresh_Identifiers (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.43)
20:26:14 Timing Falling_Factorial_Sum (2 threads, 7.117s elapsed time, 13.376s cpu time, 0.440s GC time, factor 1.88)
20:26:14 Finished Falling_Factorial_Sum (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.64)
20:26:17 Timing Mereology (2 threads, 7.769s elapsed time, 9.307s cpu time, 0.441s GC time, factor 1.20)
20:26:17 Finished Mereology (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.14)
20:26:22 Running CYK (on 10.195.8.11+4-5) ...
20:26:23 Running Finite-Map-Extras (on 10.195.8.30+8-9) ...
20:26:24 CYK: theory CYK.CYK
20:26:25 Finite-Map-Extras: theory HOL-Library.AList
20:26:25 Finite-Map-Extras: theory HOL-Library.Conditional_Parametricity
20:26:26 Running Gray_Codes (on 10.195.8.46+2-3) ...
20:26:26 Finite-Map-Extras: theory HOL-Library.Nat_Bijection
20:26:27 Finite-Map-Extras: theory HOL-Library.Old_Datatype
20:26:27 Gray_Codes: theory Gray_Codes.Encoding_Nat
20:26:28 Collections_Examples: theory Collections_Examples.Combined_TwoSat
20:26:28 Finite-Map-Extras: theory HOL-Library.Countable
20:26:29 Gray_Codes: theory Gray_Codes.Code_Word_Dist
20:26:29 Gray_Codes: theory Gray_Codes.Non_Boolean_Gray
20:26:30 Timing CYK (2 threads, 5.619s elapsed time, 9.940s cpu time, 0.459s GC time, factor 1.77)
20:26:30 Finished CYK (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.55)
20:26:30 Finite-Map-Extras: theory HOL-Library.FSet
20:26:30 Running Ackermanns_not_PR (on 10.195.8.29+6-7) ...
20:26:32 Ackermanns_not_PR: theory Ackermanns_not_PR.Primrec
20:26:33 Running Transitive-Closure (on 10.195.8.42+2,4) ...
20:26:34 Timing Gray_Codes (2 threads, 6.620s elapsed time, 10.646s cpu time, 0.331s GC time, factor 1.61)
20:26:34 Finished Gray_Codes (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.46)
20:26:35 Timing Ackermanns_not_PR (2 threads, 2.928s elapsed time, 3.771s cpu time, 0.097s GC time, factor 1.29)
20:26:35 Finished Ackermanns_not_PR (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.11)
20:26:36 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
20:26:36 Transitive-Closure: theory Matrix.Utility
20:26:36 Finite-Map-Extras: theory HOL-Library.Finite_Map
20:26:37 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
20:26:37 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
20:26:37 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
20:26:38 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
20:26:38 Running Pop_Refinement (on 10.195.8.40+6,9) ...
20:26:39 Running Skew_Heap (on 10.195.6.179+7-8) ...
20:26:40 Pop_Refinement: theory Pop_Refinement.Definition
20:26:40 Pop_Refinement: theory Pop_Refinement.First_Example
20:26:40 Pop_Refinement: theory Pop_Refinement.Future_Work
20:26:40 Pop_Refinement: theory Pop_Refinement.General_Remarks
20:26:40 Pop_Refinement: theory Pop_Refinement.Related_Work
20:26:40 Pop_Refinement: theory Pop_Refinement.Second_Example
20:26:40 Running Stellar_Quorums (on 10.195.7.194+2-3) ...
20:26:41 Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
20:26:42 Skew_Heap: theory HOL-Data_Structures.Heaps
20:26:42 Running Valuation (on 10.195.8.49+6-7) ...
20:26:42 Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
20:26:42 Skew_Heap: theory Skew_Heap.Skew_Heap
20:26:42 Timing Transitive-Closure (2 threads, 5.879s elapsed time, 10.841s cpu time, 0.442s GC time, factor 1.84)
20:26:42 Finished Transitive-Closure (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.52)
20:26:44 Valuation: theory Valuation.Valuation1
20:26:44 Timing Skew_Heap (2 threads, 2.340s elapsed time, 3.190s cpu time, 0.163s GC time, factor 1.36)
20:26:44 Finished Skew_Heap (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.12)
20:26:45 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples
20:26:47 Collections_Examples: theory Collections_Examples.Collection_Examples
20:26:48 Finite-Map-Extras: theory Finite-Map-Extras.Finite_Map_Extras
20:26:48 Valuation: theory Valuation.Valuation2
20:26:49 Timing Collections_Examples (6 threads, 61.678s elapsed time, 217.087s cpu time, 22.053s GC time, factor 3.52)
20:26:49 Finished Collections_Examples (0:01:03 elapsed time, 0:03:41 cpu time, factor 3.47)
20:26:50 Valuation: theory Valuation.Valuation3
20:26:50 Padic_Field: theory Padic_Field.Padic_Field_Powers
20:26:51 Timing Pop_Refinement (2 threads, 10.604s elapsed time, 18.180s cpu time, 1.537s GC time, factor 1.71)
20:26:51 Finished Pop_Refinement (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.60)
20:26:52 Timing Stellar_Quorums (2 threads, 10.339s elapsed time, 14.153s cpu time, 0.518s GC time, factor 1.37)
20:26:52 Finished Stellar_Quorums (0:00:12 elapsed time, 0:00:15 cpu time, factor 1.29)
20:26:53 Timing Finite-Map-Extras (2 threads, 27.303s elapsed time, 42.946s cpu time, 1.913s GC time, factor 1.57)
20:26:53 Finished Finite-Map-Extras (0:00:29 elapsed time, 0:00:45 cpu time, factor 1.53)
20:26:54 Running MiniSail (on of1-proof+0-7) ...
20:26:55 MiniSail: theory HOL-Eisbach.Eisbach
20:26:55 MiniSail: theory FinFun.FinFun
20:26:56 MiniSail: theory HOL-Eisbach.Eisbach_Tools
20:26:56 MiniSail: theory Nominal2.Nominal2_Base
20:26:58 Running Monad_Normalisation (on 10.195.8.11+6-7) ...
20:26:58 MiniSail: theory Nominal2.Nominal2_Abs
20:26:59 MiniSail: theory Nominal2.Nominal2_FCB
20:27:00 MiniSail: theory Nominal2.Nominal2
20:27:01 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
20:27:01 Running Latin_Square (on 10.195.8.46+6-7) ...
20:27:01 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
20:27:01 MiniSail: theory MiniSail.Nominal-Utils
20:27:02 MiniSail: theory MiniSail.Syntax
20:27:03 Latin_Square: theory Marriage.Marriage
20:27:03 Timing Monad_Normalisation (2 threads, 1.584s elapsed time, 2.497s cpu time, 0.072s GC time, factor 1.58)
20:27:03 Finished Monad_Normalisation (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.11)
20:27:03 Latin_Square: theory Latin_Square.Latin_Square
20:27:06 Running Fisher_Yates (on 10.195.8.29+0-1) ...
20:27:09 Running Tree_Decomposition (on 10.195.8.42+5-6) ...
20:27:09 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
20:27:10 Tree_Decomposition: theory Tree_Decomposition.Graph
20:27:11 Tree_Decomposition: theory Tree_Decomposition.Tree
20:27:12 Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
20:27:13 Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
20:27:13 Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
20:27:13 Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
20:27:13 Timing Fisher_Yates (2 threads, 4.036s elapsed time, 7.078s cpu time, 0.201s GC time, factor 1.75)
20:27:13 Finished Fisher_Yates (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.40)
20:27:14 Running Noninterference_Inductive_Unwinding (on 10.195.8.40+0-1) ...
20:27:14 Timing Latin_Square (2 threads, 10.558s elapsed time, 16.606s cpu time, 0.424s GC time, factor 1.57)
20:27:14 Finished Latin_Square (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.46)
20:27:15 Running Lifting_Definition_Option (on 10.195.6.179+7-8) ...
20:27:15 Noninterference_Inductive_Unwinding: theory List_Interleaving.ListInterleaving
20:27:15 Noninterference_Inductive_Unwinding: theory Noninterference_CSP.CSPNoninterference
20:27:16 Running SumSquares (on 10.195.7.194+6-7) ...
20:27:16 Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
20:27:17 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
20:27:19 SumSquares: theory SumSquares.FourSquares
20:27:19 SumSquares: theory SumSquares.TwoSquares
20:27:19 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
20:27:19 Noninterference_Inductive_Unwinding: theory Noninterference_Inductive_Unwinding.InductiveUnwinding
20:27:21 Timing Lifting_Definition_Option (2 threads, 3.568s elapsed time, 4.334s cpu time, 0.171s GC time, factor 1.21)
20:27:21 Finished Lifting_Definition_Option (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.11)
20:27:21 Timing Tree_Decomposition (2 threads, 9.858s elapsed time, 16.368s cpu time, 0.716s GC time, factor 1.66)
20:27:21 Finished Tree_Decomposition (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.53)
20:27:23 MiniSail: theory MiniSail.IVSubst
20:27:23 MiniSail: theory MiniSail.BTVSubst
20:27:26 MiniSail: theory MiniSail.Wellformed
20:27:26 MiniSail: theory MiniSail.SyntaxL
20:27:29 Timing Noninterference_Inductive_Unwinding (2 threads, 13.262s elapsed time, 21.322s cpu time, 1.057s GC time, factor 1.61)
20:27:29 Finished Noninterference_Inductive_Unwinding (0:00:15 elapsed time, 0:00:23 cpu time, factor 1.52)
20:27:31 Timing SumSquares (2 threads, 11.838s elapsed time, 16.558s cpu time, 0.421s GC time, factor 1.40)
20:27:31 Finished SumSquares (0:00:14 elapsed time, 0:00:19 cpu time, factor 1.31)
20:27:32 Running Mason_Stothers (on 10.195.8.11+2-3) ...
20:27:34 Running FLP (on 10.195.8.30+6-7) ...
20:27:35 Mason_Stothers: theory Mason_Stothers.Mason_Stothers
20:27:36 FLP: theory FLP.ListUtilities
20:27:36 FLP: theory FLP.Multiset
20:27:36 FLP: theory FLP.AsynchronousSystem
20:27:37 Running Surprise_Paradox (on 10.195.8.46+4-5) ...
20:27:39 Timing Mason_Stothers (2 threads, 4.020s elapsed time, 6.176s cpu time, 0.138s GC time, factor 1.54)
20:27:39 Finished Mason_Stothers (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.28)
20:27:39 Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
20:27:40 FLP: theory FLP.Execution
20:27:40 FLP: theory FLP.FLPSystem
20:27:40 Running Involutions2Squares (on 10.195.8.29+6-7) ...
20:27:41 FLP: theory FLP.FLPTheorem
20:27:42 Involutions2Squares: theory Involutions2Squares.Involutions2Squares
20:27:42 Timing Valuation (2 threads, 56.461s elapsed time, 91.360s cpu time, 5.384s GC time, factor 1.62)
20:27:42 Finished Valuation (0:00:59 elapsed time, 0:01:34 cpu time, factor 1.59)
20:27:42 Padic_Field: theory Padic_Field.Padic_Semialgebraic_Function_Ring
20:27:43 Timing Surprise_Paradox (2 threads, 3.084s elapsed time, 4.547s cpu time, 0.185s GC time, factor 1.47)
20:27:43 Finished Surprise_Paradox (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.20)
20:27:43 FLP: theory FLP.FLPExistingSystem
20:27:46 Timing Involutions2Squares (2 threads, 3.969s elapsed time, 4.947s cpu time, 0.123s GC time, factor 1.25)
20:27:46 Finished Involutions2Squares (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.13)
20:27:49 Running Octonions (on 10.195.8.40+2-3) ...
20:27:50 Running Lazy_Case (on 10.195.6.179+2,4) ...
20:27:51 Running Strong_Security (on 10.195.7.194+4-5) ...
20:27:51 Lazy_Case: theory Lazy_Case.Lazy_Case
20:27:52 Octonions: theory Octonions.Cross_Product_7
20:27:52 Lazy_Case: theory Lazy_Case.Test_Lazy_Case
20:27:52 Strong_Security: theory Strong_Security.Types
20:27:52 Strong_Security: theory Strong_Security.MWLf
20:27:53 Strong_Security: theory Strong_Security.Expr
20:27:53 Octonions: theory Octonions.Octonions
20:27:54 Strong_Security: theory Strong_Security.Domain_example
20:27:55 Strong_Security: theory Strong_Security.Strong_Security
20:27:55 Strong_Security: theory Strong_Security.Up_To_Technique
20:27:55 Strong_Security: theory Strong_Security.Parallel_Composition
20:27:56 Timing Lazy_Case (2 threads, 3.856s elapsed time, 5.955s cpu time, 0.351s GC time, factor 1.54)
20:27:56 Finished Lazy_Case (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.32)
20:27:56 Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
20:27:56 Strong_Security: theory Strong_Security.Language_Composition
20:27:56 Strong_Security: theory Strong_Security.Type_System
20:27:57 Strong_Security: theory Strong_Security.Type_System_example
20:28:01 Timing FLP (2 threads, 24.745s elapsed time, 43.923s cpu time, 2.717s GC time, factor 1.78)
20:28:01 Finished FLP (0:00:27 elapsed time, 0:00:46 cpu time, factor 1.71)
20:28:09 MiniSail: theory MiniSail.RCLogic
20:28:09 MiniSail: theory MiniSail.WellformedL
20:28:10 Timing Strong_Security (2 threads, 16.680s elapsed time, 30.762s cpu time, 2.785s GC time, factor 1.84)
20:28:10 Finished Strong_Security (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.74)
20:28:13 Timing Octonions (2 threads, 20.012s elapsed time, 37.671s cpu time, 1.234s GC time, factor 1.88)
20:28:13 Finished Octonions (0:00:23 elapsed time, 0:00:40 cpu time, factor 1.76)
20:28:20 MiniSail: theory MiniSail.SubstMethods
20:28:21 MiniSail: theory MiniSail.RCLogicL
20:28:21 MiniSail: theory MiniSail.Typing
20:28:30 Running First_Welfare_Theorem (on of1-proof+8-15) ...
20:28:31 First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
20:28:31 First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
20:28:31 First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
20:28:31 First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
20:28:33 First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
20:28:33 Running Priority_Queue_Braun (on of3.proof.cit.tum.de+1) ...
20:28:33 First_Welfare_Theorem: theory First_Welfare_Theorem.Common
20:28:33 First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
20:28:33 First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
20:28:33 First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
20:28:34 Priority_Queue_Braun: theory HOL-Data_Structures.Priority_Queue_Specs
20:28:34 Priority_Queue_Braun: theory HOL-Data_Structures.Braun_Tree
20:28:35 Priority_Queue_Braun: theory Priority_Queue_Braun.Priority_Queue_Braun
20:28:36 Timing First_Welfare_Theorem (8 threads, 3.640s elapsed time, 15.904s cpu time, 1.409s GC time, factor 4.37)
20:28:36 Finished First_Welfare_Theorem (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.34)
20:28:40 Priority_Queue_Braun: theory Priority_Queue_Braun.Priority_Queue_Braun2
20:28:40 Priority_Queue_Braun: theory Priority_Queue_Braun.Sorting_Braun
20:28:46 Running Types_Tableaus_and_Goedels_God (on of2.proof.cit.tum.de+1) ...
20:28:46 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
20:28:46 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
20:28:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
20:28:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
20:28:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
20:28:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
20:28:47 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
20:28:52 Running MHComputation (on 10.195.8.40+0) ...
20:28:53 MHComputation: theory MHComputation.MHComputation
20:28:57 Timing Types_Tableaus_and_Goedels_God (6 threads, 10.140s elapsed time, 9.994s cpu time, 0.614s GC time, factor 0.99)
20:28:57 Finished Types_Tableaus_and_Goedels_God (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.96)
20:28:58 Timing Priority_Queue_Braun (6 threads, 22.474s elapsed time, 22.464s cpu time, 0.550s GC time, factor 1.00)
20:28:58 Finished Priority_Queue_Braun (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)
20:28:58 Running Lorenz_C1 (on 10.195.6.179+2) ...
20:28:59 Timing MHComputation (2 threads, 5.377s elapsed time, 5.377s cpu time, 0.329s GC time, factor 1.00)
20:28:59 Finished MHComputation (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.95)
20:29:02 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
20:29:05 Timing Lorenz_C1 (2 threads, 1.985s elapsed time, 1.982s cpu time, 0.025s GC time, factor 1.00)
20:29:05 Finished Lorenz_C1 (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.95)
20:29:05 Running FOL_Seq_Calc1 (on 10.195.8.49+3) ...
20:29:07 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
20:29:08 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
20:29:09 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
20:29:10 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent2
20:29:12 Running Efficient-Mergesort (on of3.proof.cit.tum.de+2) ...
20:29:13 Efficient-Mergesort: theory HOL-Library.Cancellation
20:29:14 Efficient-Mergesort: theory HOL-Library.Multiset
20:29:21 Timing FOL_Seq_Calc1 (2 threads, 13.583s elapsed time, 13.526s cpu time, 0.326s GC time, factor 1.00)
20:29:21 Finished FOL_Seq_Calc1 (0:00:16 elapsed time, 0:00:15 cpu time, factor 0.97)
20:29:23 Efficient-Mergesort: theory HOL-Data_Structures.Sorting
20:29:23 Efficient-Mergesort: theory Efficient-Mergesort.Efficient_Sort
20:29:24 Running Neumann_Morgenstern_Utility (on of2.proof.cit.tum.de+2) ...
20:29:26 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
20:29:26 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
20:29:26 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
20:29:26 Efficient-Mergesort: theory Efficient-Mergesort.Mergesort_Complexity
20:29:26 MiniSail: theory MiniSail.Operational
20:29:27 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
20:29:27 MiniSail: theory MiniSail.TypingL
20:29:30 Efficient-Mergesort: theory Efficient-Mergesort.Natural_Mergesort
20:29:31 Running Lifting_the_Exponent (on 10.195.8.40+4) ...
20:29:32 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
20:29:33 Running Source_Coding_Theorem (on 10.195.6.179+4) ...
20:29:33 Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
20:29:33 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
20:29:33 MiniSail: theory MiniSail.ContextSubtypingL
20:29:35 MiniSail: theory MiniSail.BTVSubstTypingL
20:29:35 MiniSail: theory MiniSail.IVSubstTypingL
20:29:36 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
20:29:36 Timing Efficient-Mergesort (6 threads, 21.526s elapsed time, 21.525s cpu time, 1.344s GC time, factor 1.00)
20:29:36 Finished Efficient-Mergesort (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
20:29:36 MiniSail: theory MiniSail.Safety
20:29:38 MiniSail: theory MiniSail.MiniSail
20:29:39 Timing Lifting_the_Exponent (2 threads, 4.680s elapsed time, 4.679s cpu time, 0.096s GC time, factor 1.00)
20:29:39 Finished Lifting_the_Exponent (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.95)
20:29:40 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
20:29:40 Running Matroids (on 10.195.8.49+2) ...
20:29:42 Matroids: theory Matroids.Indep_System
20:29:44 Matroids: theory Matroids.Matroid
20:29:45 Timing Source_Coding_Theorem (2 threads, 8.506s elapsed time, 8.477s cpu time, 0.199s GC time, factor 1.00)
20:29:45 Finished Source_Coding_Theorem (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
20:29:46 Timing Neumann_Morgenstern_Utility (6 threads, 18.958s elapsed time, 18.957s cpu time, 1.156s GC time, factor 1.00)
20:29:46 Finished Neumann_Morgenstern_Utility (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
20:29:47 Running Synthetic_Completeness (on of3.proof.cit.tum.de+3) ...
20:29:48 Synthetic_Completeness: theory HOL-Cardinals.Fun_More
20:29:48 Synthetic_Completeness: theory HOL-Cardinals.Order_Relation_More
20:29:48 Synthetic_Completeness: theory HOL-Cardinals.Order_Union
20:29:49 Synthetic_Completeness: theory HOL-Cardinals.Wellfounded_More
20:29:49 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Relation
20:29:49 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Embedding
20:29:50 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Constructions
20:29:52 Synthetic_Completeness: theory HOL-Cardinals.Cardinal_Order_Relation
20:29:53 Timing Matroids (2 threads, 11.083s elapsed time, 11.078s cpu time, 0.221s GC time, factor 1.00)
20:29:54 Finished Matroids (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
20:29:55 Synthetic_Completeness: theory Synthetic_Completeness.Maximal_Consistent_Sets
20:29:57 Synthetic_Completeness: theory Synthetic_Completeness.Derivations
20:29:57 Synthetic_Completeness: theory Synthetic_Completeness.Refutations
20:29:57 Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_Tableau
20:29:58 Synthetic_Completeness: theory Synthetic_Completeness.Example_First_Order_Logic
20:29:58 Synthetic_Completeness: theory Synthetic_Completeness.Example_Hybrid_Logic
20:29:58 Synthetic_Completeness: theory Synthetic_Completeness.Example_Modal_Logic
20:29:59 Running Budan_Fourier (on of2.proof.cit.tum.de+0) ...
20:29:59 Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_SC
20:30:00 Budan_Fourier: theory Sturm_Tarski.PolyMisc
20:30:01 Budan_Fourier: theory Sturm_Tarski.Sturm_Tarski
20:30:04 Budan_Fourier: theory Budan_Fourier.BF_Misc
20:30:04 Running Stalnaker_Logic (on 10.195.8.40+5) ...
20:30:06 Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
20:30:06 Running Zeckendorf (on 10.195.6.179+1) ...
20:30:07 Budan_Fourier: theory Budan_Fourier.Budan_Fourier
20:30:07 Budan_Fourier: theory Budan_Fourier.Sturm_Multiple_Roots
20:30:08 Budan_Fourier: theory Budan_Fourier.Descartes_Roots_Test
20:30:09 Zeckendorf: theory Zeckendorf.Zeckendorf
20:30:14 Timing Stalnaker_Logic (2 threads, 7.293s elapsed time, 6.999s cpu time, 0.155s GC time, factor 0.96)
20:30:14 Finished Stalnaker_Logic (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.93)
20:30:14 Running WorkerWrapper (on 10.195.8.49+4) ...
20:30:16 WorkerWrapper: theory WorkerWrapper.Maybe
20:30:16 WorkerWrapper: theory WorkerWrapper.Nats
20:30:19 WorkerWrapper: theory WorkerWrapper.LList
20:30:21 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
20:30:21 Timing Zeckendorf (2 threads, 12.366s elapsed time, 12.365s cpu time, 0.178s GC time, factor 1.00)
20:30:21 Finished Zeckendorf (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.97)
20:30:21 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
20:30:21 WorkerWrapper: theory WorkerWrapper.CounterExample
20:30:22 WorkerWrapper: theory WorkerWrapper.Last
20:30:22 Timing Synthetic_Completeness (6 threads, 33.568s elapsed time, 33.557s cpu time, 3.573s GC time, factor 1.00)
20:30:22 Finished Synthetic_Completeness (0:00:35 elapsed time, 0:00:34 cpu time, factor 0.99)
20:30:22 WorkerWrapper: theory WorkerWrapper.Streams
20:30:23 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
20:30:23 WorkerWrapper: theory WorkerWrapper.Accumulator
20:30:24 WorkerWrapper: theory WorkerWrapper.Backtracking
20:30:25 WorkerWrapper: theory WorkerWrapper.Continuations
20:30:27 Timing Budan_Fourier (6 threads, 25.949s elapsed time, 25.947s cpu time, 0.633s GC time, factor 1.00)
20:30:27 Finished Budan_Fourier (0:00:27 elapsed time, 0:00:27 cpu time, factor 0.99)
20:30:28 WorkerWrapper: theory WorkerWrapper.Nub
20:30:29 WorkerWrapper: theory WorkerWrapper.UnboxedNats
20:30:37 Timing WorkerWrapper (2 threads, 19.240s elapsed time, 19.039s cpu time, 0.741s GC time, factor 0.99)
20:30:37 Finished WorkerWrapper (0:00:21 elapsed time, 0:00:20 cpu time, factor 0.97)
20:30:37 Running Goodstein_Lambda (on 10.195.8.40+1) ...
20:30:38 Running Real_Power (on 10.195.6.179+3) ...
20:30:39 Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
20:30:39 Real_Power: theory Real_Power.RatPower
20:30:41 Real_Power: theory Real_Power.RealPower
20:30:43 Real_Power: theory Real_Power.Log
20:30:49 Timing Goodstein_Lambda (2 threads, 9.485s elapsed time, 9.484s cpu time, 0.340s GC time, factor 1.00)
20:30:49 Finished Goodstein_Lambda (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
20:30:53 Running Approximation_Algorithms (on of3.proof.cit.tum.de+0) ...
20:30:54 Approximation_Algorithms: theory HOL-Hoare.Hoare_Syntax
20:30:54 Approximation_Algorithms: theory HOL-Hoare.Hoare_Tac
20:30:54 Approximation_Algorithms: theory HOL-Library.FuncSet
20:30:56 Approximation_Algorithms: theory HOL-Library.Disjoint_Sets
20:30:58 Timing Real_Power (2 threads, 18.645s elapsed time, 18.624s cpu time, 0.404s GC time, factor 1.00)
20:30:58 Finished Real_Power (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
20:31:00 Approximation_Algorithms: theory HOL-Hoare.Hoare_Logic
20:31:02 Approximation_Algorithms: theory Approximation_Algorithms.Approx_VC_Hoare
20:31:02 Approximation_Algorithms: theory Approximation_Algorithms.Approx_MIS_Hoare
20:31:02 Approximation_Algorithms: theory Approximation_Algorithms.Approx_BP_Hoare
20:31:02 Approximation_Algorithms: theory Approximation_Algorithms.Approx_LB_Hoare
20:31:02 Approximation_Algorithms: theory Approximation_Algorithms.Approx_SC_Hoare
20:31:04 Approximation_Algorithms: theory Approximation_Algorithms.Center_Selection
20:31:08 Timing Padic_Field (6 threads, 343.462s elapsed time, 1078.002s cpu time, 536.242s GC time, factor 3.14)
20:31:08 Finished Padic_Field (0:05:46 elapsed time, 0:18:05 cpu time, factor 3.13)
20:31:11 Running Noninterference_Concurrent_Composition (on 10.195.6.179+0) ...
20:31:13 Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
20:31:21 Running Case_Labeling (on 10.195.8.49+0) ...
20:31:22 Case_Labeling: theory HOL-Eisbach.Eisbach
20:31:22 Case_Labeling: theory Case_Labeling.Case_Labeling
20:31:24 Case_Labeling: theory HOL-Hoare.Arith2
20:31:24 Case_Labeling: theory HOL-Hoare.Hoare_Syntax
20:31:24 Case_Labeling: theory HOL-Hoare.Hoare_Tac
20:31:26 Case_Labeling: theory Case_Labeling.Conditionals
20:31:27 Case_Labeling: theory Case_Labeling.Monadic_Language
20:31:27 Timing Approximation_Algorithms (6 threads, 33.213s elapsed time, 32.913s cpu time, 1.602s GC time, factor 0.99)
20:31:27 Finished Approximation_Algorithms (0:00:34 elapsed time, 0:00:33 cpu time, factor 0.98)
20:31:29 Case_Labeling: theory HOL-Hoare.Hoare_Logic
20:31:31 Case_Labeling: theory Case_Labeling.Labeled_Hoare
20:31:32 Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
20:31:32 Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
20:31:33 Timing MiniSail (8 threads, 275.411s elapsed time, 1510.299s cpu time, 104.026s GC time, factor 5.48)
20:31:33 Finished MiniSail (0:04:38 elapsed time, 0:25:17 cpu time, factor 5.46)
20:31:34 Timing Noninterference_Concurrent_Composition (2 threads, 20.552s elapsed time, 20.521s cpu time, 0.460s GC time, factor 1.00)
20:31:34 Finished Noninterference_Concurrent_Composition (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
20:31:40 Timing Case_Labeling (2 threads, 17.124s elapsed time, 17.082s cpu time, 0.619s GC time, factor 1.00)
20:31:40 Finished Case_Labeling (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.98)
20:31:47 Running Imperative_Insertion_Sort (on of1-proof+0-7) ...
20:31:48 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
20:31:48 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
20:31:50 Timing Imperative_Insertion_Sort (8 threads, 1.548s elapsed time, 5.011s cpu time, 0.140s GC time, factor 3.24)
20:31:50 Finished Imperative_Insertion_Sort (0:00:02 elapsed time, 0:00:06 cpu time)
20:31:54 Running Lovasz_Local (on of4.proof.cit.tum.de+8-15) ...
20:31:55 Lovasz_Local: theory HOL-Eisbach.Eisbach
20:31:55 Lovasz_Local: theory Graph_Theory.Rtrancl_On
20:31:55 Lovasz_Local: theory HOL-Combinatorics.Stirling
20:31:55 Lovasz_Local: theory HOL-Library.Multiset_Order
20:31:55 Lovasz_Local: theory Card_Partitions.Set_Partition
20:31:55 Lovasz_Local: theory Graph_Theory.Stuff
20:31:55 Lovasz_Local: theory Graph_Theory.Digraph
20:31:55 Lovasz_Local: theory Nested_Multisets_Ordinals.Multiset_More
20:31:55 Running Buffons_Needle (on 10.195.8.29+0-7) ...
20:31:56 Lovasz_Local: theory Card_Partitions.Injectivity_Solver
20:31:56 Lovasz_Local: theory Card_Partitions.Card_Partitions
20:31:56 Lovasz_Local: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
20:31:56 Lovasz_Local: theory Lovasz_Local.PiE_Rel_Extras
20:31:56 Lovasz_Local: theory Design_Theory.Multisets_Extras
20:31:56 Lovasz_Local: theory Lovasz_Local.Prob_Events_Extras
20:31:56 Lovasz_Local: theory Graph_Theory.Arc_Walk
20:31:56 Lovasz_Local: theory Graph_Theory.Bidirected_Digraph
20:31:57 Lovasz_Local: theory Lovasz_Local.Cond_Prob_Extensions
20:31:57 Lovasz_Local: theory Graph_Theory.Pair_Digraph
20:31:57 Lovasz_Local: theory Lovasz_Local.Indep_Events
20:31:58 Lovasz_Local: theory Lovasz_Local.Basic_Method
20:31:58 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
20:32:01 Lovasz_Local: theory Lovasz_Local.Digraph_Extensions
20:32:01 Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Lemma
20:32:02 Lovasz_Local: theory Lovasz_Local.Lovasz_Local_Root
20:32:06 Timing Buffons_Needle (2 threads, 7.436s elapsed time, 12.725s cpu time, 0.406s GC time, factor 1.71)
20:32:06 Finished Buffons_Needle (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.50)
20:32:11 Timing Lovasz_Local (6 threads, 15.007s elapsed time, 76.472s cpu time, 5.695s GC time, factor 5.10)
20:32:11 Finished Lovasz_Local (0:00:16 elapsed time, 0:01:18 cpu time, factor 4.69)
20:32:21 Running GaleStewart_Games (on of1-proof+8-15) ...
20:32:22 Running UpDown_Scheme (on of3.proof.cit.tum.de+8-15) ...
20:32:22 GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
20:32:22 GaleStewart_Games: theory GaleStewart_Games.MoreENat
20:32:22 GaleStewart_Games: theory GaleStewart_Games.MorePrefix
20:32:22 GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
20:32:22 GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
20:32:22 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
20:32:22 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
20:32:23 UpDown_Scheme: theory HOL-Eisbach.Eisbach
20:32:23 UpDown_Scheme: theory HOL-Library.Adhoc_Overloading
20:32:23 UpDown_Scheme: theory HOL-ex.Quicksort
20:32:23 UpDown_Scheme: theory HOL-Library.Option_ord
20:32:23 UpDown_Scheme: theory HOL-Imperative_HOL.Heap
20:32:23 UpDown_Scheme: theory UpDown_Scheme.Grid_Point
20:32:23 UpDown_Scheme: theory HOL-Library.Monad_Syntax
20:32:23 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match
20:32:23 Timing GaleStewart_Games (8 threads, 1.322s elapsed time, 5.829s cpu time, 0.174s GC time, factor 4.41)
20:32:23 Finished GaleStewart_Games (0:00:02 elapsed time, 0:00:07 cpu time)
20:32:24 UpDown_Scheme: theory Automatic_Refinement.Misc
20:32:24 UpDown_Scheme: theory UpDown_Scheme.Grid
20:32:24 UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad
20:32:24 UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
20:32:25 UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
20:32:25 UpDown_Scheme: theory UpDown_Scheme.Down
20:32:25 UpDown_Scheme: theory UpDown_Scheme.Up
20:32:25 UpDown_Scheme: theory HOL-Imperative_HOL.Array
20:32:25 UpDown_Scheme: theory UpDown_Scheme.Up_Down
20:32:25 UpDown_Scheme: theory HOL-Imperative_HOL.Ref
20:32:26 UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL
20:32:26 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
20:32:26 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run
20:32:27 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions
20:32:28 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple
20:32:28 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation
20:32:29 UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main
20:32:29 UpDown_Scheme: theory UpDown_Scheme.Imperative
20:32:33 Timing UpDown_Scheme (6 threads, 9.804s elapsed time, 52.202s cpu time, 5.313s GC time, factor 5.32)
20:32:33 Finished UpDown_Scheme (0:00:11 elapsed time, 0:00:54 cpu time, factor 4.83)
20:32:44 Running Undirected_Graph_Theory (on of3.proof.cit.tum.de+0-7) ...
20:32:45 Undirected_Graph_Theory: theory Card_Partitions.Set_Partition
20:32:45 Undirected_Graph_Theory: theory HOL-Combinatorics.Transposition
20:32:45 Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Multiset_More
20:32:45 Undirected_Graph_Theory: theory Girth_Chromatic.Girth_Chromatic_Misc
20:32:45 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Basics
20:32:45 Undirected_Graph_Theory: theory HOL-Combinatorics.Permutations
20:32:45 Undirected_Graph_Theory: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
20:32:45 Undirected_Graph_Theory: theory Design_Theory.Multisets_Extras
20:32:45 Undirected_Graph_Theory: theory HOL-Combinatorics.Multiset_Permutations
20:32:46 Undirected_Graph_Theory: theory Design_Theory.Design_Basics
20:32:46 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Triangles
20:32:46 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graph_Walks
20:32:46 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Bipartite_Graphs
20:32:46 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Connectivity
20:32:47 Undirected_Graph_Theory: theory Design_Theory.Design_Operations
20:32:48 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Girth_Independence
20:32:48 Undirected_Graph_Theory: theory Design_Theory.Block_Designs
20:32:50 Undirected_Graph_Theory: theory Design_Theory.BIBD
20:32:51 Undirected_Graph_Theory: theory Design_Theory.Resolvable_Designs
20:32:52 Undirected_Graph_Theory: theory Design_Theory.Group_Divisible_Designs
20:32:53 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Graph_Theory_Relations
20:32:55 Undirected_Graph_Theory: theory Undirected_Graph_Theory.Undirected_Graphs_Root
20:33:01 Timing Undirected_Graph_Theory (6 threads, 15.149s elapsed time, 80.786s cpu time, 7.683s GC time, factor 5.33)
20:33:01 Finished Undirected_Graph_Theory (0:00:16 elapsed time, 0:01:22 cpu time, factor 4.95)
21:20:12 Build timed out (after 200 minutes). Marking the build as failed.
21:20:13 Build was aborted
21:20:13 Started calculate disk usage of build
21:20:13 Finished Calculation of disk usage of build in 0 seconds
21:20:13 Started calculate disk usage of workspace
21:20:16 Finished Calculation of disk usage of workspace in  2 second
21:20:17 Finished: FAILURE