Skipping 893 KB.. Full Log

PCF: theory PCF.Basis
14:29:58 Timing Finite_Automata_HF (2 threads, 42.202s elapsed time, 42.033s cpu time, 1.780s GC time, factor 1.00)
14:29:58 Finished Finite_Automata_HF (0:00:44 elapsed time, 0:00:43 cpu time, factor 0.99)
14:29:58 Derangements: theory HOL-Library.FuncSet
14:29:58 Well_Quasi_Orders: theory Abstract-Rewriting.Seq
14:29:58 Heard_Of: theory HOL-Library.Infinite_Set
14:29:58 Well_Quasi_Orders: theory Open_Induction.Restricted_Predicates
14:29:58 Heard_Of: theory Heard_Of.HOModel
14:29:58 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.Relations
14:29:58 Timing Efficient-Mergesort (8 threads, 7.548s elapsed time, 25.783s cpu time, 1.834s GC time, factor 3.42)
14:29:58 Finished Efficient-Mergesort (0:00:08 elapsed time, 0:00:27 cpu time, factor 3.18)
14:29:59 Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding
14:29:59 PCF: theory PCF.Logical_Relations
14:29:59 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.QML
14:29:59 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
14:30:00 Derangements: theory HOL-Library.Multiset
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
14:30:00 Heard_Of: theory HOL-Library.Omega_Words_Fun
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
14:30:00 Well_Quasi_Orders: theory Open_Induction.Open_Induction
14:30:00 Running Category2 (on 10.195.8.11+2) ...
14:30:00 Well_Quasi_Orders: theory Well_Quasi_Orders.Multiset_Extension
14:30:00 Timing Combinatorial_Enumeration_Algorithms (2 threads, 46.541s elapsed time, 46.476s cpu time, 1.426s GC time, factor 1.00)
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
14:30:00 Finished Combinatorial_Enumeration_Algorithms (0:00:49 elapsed time, 0:00:49 cpu time, factor 0.99)
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
14:30:00 Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
14:30:00 Timing Formal_Puiseux_Series (2 threads, 45.196s elapsed time, 45.121s cpu time, 1.373s GC time, factor 1.00)
14:30:00 Finished Formal_Puiseux_Series (0:00:48 elapsed time, 0:00:47 cpu time, factor 0.99)
14:30:01 Derangements: theory HOL-Library.Disjoint_Sets
14:30:02 Heard_Of: theory Heard_Of.Majorities
14:30:02 Well_Quasi_Orders: theory Regular-Sets.Regular_Set
14:30:02 Heard_Of: theory Stuttering_Equivalence.Samplers
14:30:02 Well_Quasi_Orders: theory Well_Quasi_Orders.Infinite_Sequences
14:30:02 Knuth_Morris_Pratt: theory Knuth_Morris_Pratt.KMP
14:30:02 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Elements
14:30:02 Category2: theory HOL-ZF.LProd
14:30:03 Heard_Of: theory Stuttering_Equivalence.StutterEquivalence
14:30:03 Category2: theory Category2.Category
14:30:03 Well_Quasi_Orders: theory Well_Quasi_Orders.Least_Enum
14:30:03 Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blackboard
14:30:03 Timing SDS_Impossibility (8 threads, 11.827s elapsed time, 45.453s cpu time, 3.232s GC time, factor 3.84)
14:30:03 Finished SDS_Impossibility (0:00:13 elapsed time, 0:00:47 cpu time, factor 3.52)
14:30:04 Heard_Of: theory Heard_Of.AteDefs
14:30:04 PCF: theory PCF.PCF
14:30:04 Category2: theory HOL-ZF.HOLZF
14:30:04 Heard_Of: theory Heard_Of.EigbyzDefs
14:30:05 Running ABY3_Protocols (on 10.195.6.179+1) ...
14:30:05 Running Boolean_Expression_Checkers (on 10.195.6.179+3) ...
14:30:05 Heard_Of: theory Heard_Of.LastVotingDefs
14:30:05 Building Epistemic_Logic (on 10.195.6.179+2) ...
14:30:05 Running SenSocialChoice (on 10.195.6.179+4) ...
14:30:05 Heard_Of: theory Heard_Of.OneThirdRuleDefs
14:30:06 Well_Quasi_Orders: theory Regular-Sets.Regular_Exp
14:30:06 Category2: theory Category2.Functors
14:30:06 Category2: theory HOL-ZF.Zet
14:30:06 Heard_Of: theory Heard_Of.UteDefs
14:30:06 Category2: theory HOL-ZF.MainZF
14:30:07 SenSocialChoice: theory SenSocialChoice.FSext
14:30:07 Epistemic_Logic: theory Epistemic_Logic.Maximal_Consistent_Sets
14:30:07 Category2: theory Category2.Universe
14:30:07 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
14:30:07 Timing Fourier (2 threads, 139.310s elapsed time, 139.241s cpu time, 4.725s GC time, factor 1.00)
14:30:07 Finished Fourier (0:02:23 elapsed time, 0:02:22 cpu time, factor 1.00)
14:30:07 SenSocialChoice: theory SenSocialChoice.RPRs
14:30:07 Epistemic_Logic: theory Epistemic_Logic.Epistemic_Logic
14:30:08 Category2: theory Category2.MonadicEquationalTheory
14:30:08 SenSocialChoice: theory SenSocialChoice.SCFs
14:30:08 ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
14:30:08 ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
14:30:08 Timing Minsky_Machines (2 threads, 47.253s elapsed time, 46.929s cpu time, 2.704s GC time, factor 0.99)
14:30:08 Finished Minsky_Machines (0:00:50 elapsed time, 0:00:49 cpu time, factor 0.98)
14:30:09 Category2: theory Category2.NatTrans
14:30:09 SenSocialChoice: theory SenSocialChoice.Arrow
14:30:09 PCF: theory PCF.Continuations
14:30:09 Heard_Of: theory Heard_Of.UvDefs
14:30:09 ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
14:30:09 PCF: theory PCF.OpSem
14:30:10 SenSocialChoice: theory SenSocialChoice.May
14:30:10 Heard_Of: theory Heard_Of.Reduction
14:30:11 SenSocialChoice: theory SenSocialChoice.Sen
14:30:12 Derangements: theory HOL-Combinatorics.Permutations
14:30:13 Heard_Of: theory Heard_Of.AteProof
14:30:13 Heard_Of: theory Heard_Of.EigbyzProof
14:30:13 Category2: theory Category2.SetCat
14:30:13 Heard_Of: theory Heard_Of.LastVotingProof
14:30:14 Heard_Of: theory Heard_Of.OneThirdRuleProof
14:30:14 ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
14:30:14 Well_Quasi_Orders: theory Regular-Sets.NDerivative
14:30:15 Timing FunWithTilings (6 threads, 18.517s elapsed time, 18.517s cpu time, 0.304s GC time, factor 1.00)
14:30:15 Well_Quasi_Orders: theory Regular-Sets.Relation_Interpretation
14:30:15 Finished FunWithTilings (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
14:30:15 Derangements: theory Derangements.Derangements
14:30:15 ABY3_Protocols: theory ABY3_Protocols.Multiplication
14:30:15 Heard_Of: theory Heard_Of.UteProof
14:30:15 Heard_Of: theory Heard_Of.UvProof
14:30:17 ABY3_Protocols: theory ABY3_Protocols.Shuffle
14:30:17 Category2: theory Category2.Yoneda
14:30:17 ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
14:30:17 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
14:30:18 Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Example
14:30:18 Timing Given_Clause_Loops (6 threads, 108.005s elapsed time, 108.004s cpu time, 28.086s GC time, factor 1.00)
14:30:18 Finished Given_Clause_Loops (0:01:50 elapsed time, 0:01:50 cpu time, factor 1.00)
14:30:19 Timing Noninterference_Generic_Unwinding (2 threads, 19.597s elapsed time, 19.156s cpu time, 0.279s GC time, factor 0.98)
14:30:19 Finished Noninterference_Generic_Unwinding (0:00:21 elapsed time, 0:00:20 cpu time, factor 0.96)
14:30:21 Timing Lowe_Ontological_Argument (2 threads, 22.121s elapsed time, 13.097s cpu time, 0.365s GC time, factor 0.59)
14:30:21 Finished Lowe_Ontological_Argument (0:00:24 elapsed time, 0:00:14 cpu time, factor 0.61)
14:30:24 Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
14:30:25 Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
14:30:25 Timing Fermat3_4 (2 threads, 30.944s elapsed time, 30.914s cpu time, 0.724s GC time, factor 1.00)
14:30:25 Finished Fermat3_4 (0:00:34 elapsed time, 0:00:33 cpu time, factor 0.99)
14:30:25 PCF: theory PCF.SmallStep
14:30:27 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
14:30:29 Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
14:30:29 Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
14:30:30 Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
14:30:31 Timing Knuth_Morris_Pratt (6 threads, 33.608s elapsed time, 33.593s cpu time, 1.650s GC time, factor 1.00)
14:30:31 Finished Knuth_Morris_Pratt (0:00:35 elapsed time, 0:00:35 cpu time, factor 0.99)
14:30:31 Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
14:30:32 Timing Hales_Jewett (2 threads, 38.489s elapsed time, 38.446s cpu time, 0.863s GC time, factor 1.00)
14:30:32 Finished Hales_Jewett (0:00:40 elapsed time, 0:00:40 cpu time, factor 0.99)
14:30:32 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
14:30:32 Timing Epistemic_Logic (2 threads, 14.501s elapsed time, 14.444s cpu time, 0.692s GC time, factor 1.00)
14:30:32 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
14:30:32 Finished Epistemic_Logic (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.98)
14:30:33 Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
14:30:33 Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
14:30:34 Timing Boolean_Expression_Checkers (2 threads, 26.204s elapsed time, 26.071s cpu time, 4.489s GC time, factor 0.99)
14:30:34 Finished Boolean_Expression_Checkers (0:00:29 elapsed time, 0:00:28 cpu time, factor 0.98)
14:30:35 Running FLP (on of1-proof+0-7) ...
14:30:35 Building HOL-SPARK-Examples (on of1-proof+8-15) ...
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor
14:30:36 FLP: theory FLP.ListUtilities
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas
14:30:36 FLP: theory FLP.Multiset
14:30:36 FLP: theory FLP.AsynchronousSystem
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification
14:30:36 Timing Partial_Order_Reduction (2 threads, 158.652s elapsed time, 157.353s cpu time, 13.260s GC time, factor 0.99)
14:30:36 Finished Partial_Order_Reduction (0:02:44 elapsed time, 0:02:42 cpu time, factor 0.99)
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round
14:30:36 Running Forcing (on 10.195.8.49+3) ...
14:30:36 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L
14:30:37 Running IO_Language_Conformance (on 10.195.8.49+0) ...
14:30:37 Running PAL (on 10.195.8.49+4) ...
14:30:37 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R
14:30:37 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L
14:30:37 Timing ABY3_Protocols (2 threads, 28.622s elapsed time, 28.538s cpu time, 0.940s GC time, factor 1.00)
14:30:37 Finished ABY3_Protocols (0:00:32 elapsed time, 0:00:32 cpu time, factor 0.99)
14:30:37 Forcing: theory Forcing.Utils
14:30:37 Running Ceva (on of3.proof.cit.tum.de+1) ...
14:30:37 Running FocusStreamsCaseStudies (on of3.proof.cit.tum.de+3) ...
14:30:37 Forcing: theory Forcing.Recursion_Thms
14:30:37 Forcing: theory Forcing.Nat_Miscellanea
14:30:37 FLP: theory FLP.FLPSystem
14:30:37 FLP: theory FLP.Execution
14:30:37 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R
14:30:38 Building Random_BSTs (on of3.proof.cit.tum.de+2) ...
14:30:38 Forcing: theory Forcing.Synthetic_Definition
14:30:38 FLP: theory FLP.FLPTheorem
14:30:39 Forcing: theory Forcing.Forcing_Notions
14:30:39 PAL: theory PAL.PAL
14:30:39 Forcing: theory Forcing.Renaming
14:30:39 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ArithExtras
14:30:39 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ListExtras
14:30:39 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.arith_hints
14:30:39 Building Bell_Numbers_Spivey (on 10.195.8.29+0) ...
14:30:39 Running Finger-Trees (on 10.195.8.29+3) ...
14:30:39 IO_Language_Conformance: theory IO_Language_Conformance.Input_Output_Language_Conformance
14:30:39 FLP: theory FLP.FLPExistingSystem
14:30:40 Ceva: theory Triangle.Angles
14:30:40 Forcing: theory Forcing.Renaming_Auto
14:30:40 Timing Topological_Semantics (2 threads, 122.424s elapsed time, 89.617s cpu time, 2.795s GC time, factor 0.73)
14:30:40 Finished Topological_Semantics (0:02:04 elapsed time, 0:01:31 cpu time, factor 0.73)
14:30:40 Forcing: theory Forcing.Internalizations
14:30:40 Forcing: theory Forcing.Relative_Univ
14:30:40 Random_BSTs: theory HOL-Data_Structures.Cmp
14:30:40 Forcing: theory Forcing.Pointed_DC
14:30:40 Random_BSTs: theory HOL-Data_Structures.Less_False
14:30:40 Random_BSTs: theory HOL-Data_Structures.Sorted_Less
14:30:40 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.stream
14:30:40 Ceva: theory Triangle.Triangle
14:30:41 Forcing: theory Forcing.Rasiowa_Sikorski
14:30:41 Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
14:30:41 Running Zeta_3_Irrational (on 10.195.8.29+4) ...
14:30:41 Forcing: theory Forcing.Interface
14:30:42 Random_BSTs: theory HOL-Data_Structures.Set_Specs
14:30:42 Random_BSTs: theory HOL-Data_Structures.Tree_Set
14:30:42 Running FOL_Seq_Calc3 (on 10.195.8.32+2) ...
14:30:42 Running Functional-Automata (on 10.195.8.32+1) ...
14:30:42 Running Rewriting_Z (on 10.195.8.32+0) ...
14:30:42 Running TLA (on 10.195.8.32+4) ...
14:30:42 Timing FLP (8 threads, 5.770s elapsed time, 23.257s cpu time, 1.653s GC time, factor 4.03)
14:30:42 Finished FLP (0:00:06 elapsed time, 0:00:24 cpu time, factor 3.58)
14:30:43 Ceva: theory Ceva.Ceva
14:30:43 Random_BSTs: theory Random_BSTs.Random_BSTs
14:30:43 Bell_Numbers_Spivey: theory HOL-Eisbach.Eisbach
14:30:43 Bell_Numbers_Spivey: theory HOL-Combinatorics.Stirling
14:30:43 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_types
14:30:43 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.BitBoolTS
14:30:43 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_types
14:30:43 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.JoinSplitTime
14:30:43 Finger-Trees: theory Finger-Trees.FingerTree
14:30:44 TLA: theory TLA.Intensional
14:30:44 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primes_Omega
14:30:44 TLA: theory TLA.Sequence
14:30:44 Zeta_3_Irrational: theory E_Transcendental.E_Transcendental
14:30:44 FOL_Seq_Calc3: theory Collections.ICF_Tools
14:30:44 FOL_Seq_Calc3: theory FOL_Seq_Calc3.List_Syntax
14:30:44 Bell_Numbers_Spivey: theory Card_Partitions.Set_Partition
14:30:44 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Syntax
14:30:45 Functional-Automata: theory Functional-Automata.AutoProj
14:30:45 FOL_Seq_Calc3: theory Collections.Ord_Code_Preproc
14:30:45 Functional-Automata: theory Functional-Automata.MaxPrefix
14:30:45 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler
14:30:45 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler_proof
14:30:45 FOL_Seq_Calc3: theory Collections.Locale_Code
14:30:45 Functional-Automata: theory Functional-Automata.DA
14:30:45 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
14:30:45 Functional-Automata: theory Functional-Automata.NA
14:30:45 Bell_Numbers_Spivey: theory Card_Partitions.Injectivity_Solver
14:30:45 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Fair_Stream
14:30:46 Forcing: theory Forcing.Forcing_Data
14:30:46 TLA: theory TLA.Semantics
14:30:46 Functional-Automata: theory Functional-Automata.MaxChop
14:30:46 Functional-Automata: theory Functional-Automata.NAe
14:30:46 Forcing: theory Forcing.Separation_Rename
14:30:46 FOL_Seq_Calc3: theory Abstract_Completeness.Abstract_Completeness
14:30:46 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR
14:30:46 Functional-Automata: theory Functional-Automata.Automata
14:30:46 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
14:30:46 Functional-Automata: theory Functional-Automata.AutoMaxChop
14:30:46 Rewriting_Z: theory HOL-Eisbach.Eisbach
14:30:46 Rewriting_Z: theory Abstract-Rewriting.Seq
14:30:46 Running Old_Datatype_Show (on 10.195.8.11+4) ...
14:30:46 Running Ribbon_Proofs (on 10.195.8.11+3) ...
14:30:46 Timing SenSocialChoice (2 threads, 39.077s elapsed time, 38.997s cpu time, 1.633s GC time, factor 1.00)
14:30:46 Finished SenSocialChoice (0:00:40 elapsed time, 0:00:40 cpu time, factor 0.99)
14:30:46 Functional-Automata: theory Regular-Sets.Regular_Set
14:30:47 Bell_Numbers_Spivey: theory Card_Partitions.Card_Partitions
14:30:47 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_proof
14:30:47 TLA: theory TLA.PreFormulas
14:30:47 Timing HOL-SPARK-Examples (8 threads, 5.539s elapsed time, 16.040s cpu time, 0.587s GC time, factor 2.90)
14:30:47 Finished HOL-SPARK-Examples (0:00:11 elapsed time, 0:00:26 cpu time, factor 2.23)
14:30:48 Forcing: theory Forcing.Internal_ZFC_Axioms
14:30:48 Rewriting_Z: theory HOL-Library.While_Combinator
14:30:48 Bell_Numbers_Spivey: theory Bell_Numbers_Spivey.Bell_Numbers
14:30:48 TLA: theory TLA.Rules
14:30:48 Timing PCF (6 threads, 51.085s elapsed time, 51.071s cpu time, 2.183s GC time, factor 1.00)
14:30:48 Finished PCF (0:00:53 elapsed time, 0:00:52 cpu time, factor 0.99)
14:30:48 Timing Derangements (2 threads, 49.525s elapsed time, 49.490s cpu time, 1.679s GC time, factor 1.00)
14:30:48 Finished Derangements (0:00:51 elapsed time, 0:00:51 cpu time, factor 0.99)
14:30:48 Rewriting_Z: theory Regular-Sets.Regular_Set
14:30:49 Ribbon_Proofs: theory Ribbon_Proofs.More_Finite_Map
14:30:49 Ribbon_Proofs: theory Ribbon_Proofs.JHelper
14:30:49 Forcing: theory Forcing.Names
14:30:49 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Semantics
14:30:49 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
14:30:49 Ribbon_Proofs: theory Ribbon_Proofs.Proofchain
14:30:49 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Encoding
14:30:49 Timing Ceva (6 threads, 9.617s elapsed time, 9.611s cpu time, 0.337s GC time, factor 1.00)
14:30:49 Finished Ceva (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:30:50 Timing Category2 (2 threads, 45.124s elapsed time, 44.415s cpu time, 3.335s GC time, factor 0.98)
14:30:50 Finished Category2 (0:00:48 elapsed time, 0:00:47 cpu time, factor 0.97)
14:30:50 Zeta_3_Irrational: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
14:30:50 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Basic
14:30:50 TLA: theory TLA.Liveness
14:30:50 Timing Architectural_Design_Patterns (2 threads, 54.915s elapsed time, 54.878s cpu time, 4.699s GC time, factor 1.00)
14:30:50 Finished Architectural_Design_Patterns (0:00:58 elapsed time, 0:00:57 cpu time, factor 0.99)
14:30:50 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
14:30:50 Timing Lambda_Free_EPO (2 threads, 87.687s elapsed time, 87.663s cpu time, 5.980s GC time, factor 1.00)
14:30:50 Finished Lambda_Free_EPO (0:01:30 elapsed time, 0:01:30 cpu time, factor 1.00)
14:30:50 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
14:30:50 TLA: theory TLA.State
14:30:51 Forcing: theory Forcing.Extensionality_Axiom
14:30:51 TLA: theory TLA.Buffer
14:30:51 Forcing: theory Forcing.Foundation_Axiom
14:30:51 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
14:30:51 TLA: theory TLA.Even
14:30:51 Forcing: theory Forcing.FrecR
14:30:51 Forcing: theory Forcing.Least
14:30:51 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
14:30:51 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Primorial
14:30:51 TLA: theory TLA.Inc
14:30:51 Forcing: theory Forcing.Pairing_Axiom
14:30:51 Forcing: theory Forcing.Proper_Extension
14:30:52 Forcing: theory Forcing.Union_Axiom
14:30:52 Functional-Automata: theory Functional-Automata.RegSet_of_nat_DA
14:30:52 FOL_Seq_Calc3: theory Abstract_Soundness.Finite_Proof_Soundness
14:30:52 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Prover
14:30:52 Functional-Automata: theory Regular-Sets.Regular_Exp
14:30:52 Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
14:30:52 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Shapiro_Tauberian
14:30:52 Forcing: theory Forcing.Arities
14:30:53 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway
14:30:53 Rewriting_Z: theory Regular-Sets.Regular_Exp
14:30:53 Forcing: theory Forcing.Forces_Definition
14:30:53 Zeta_3_Irrational: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
14:30:53 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof_aux
14:30:53 Forcing: theory Forcing.Succession_Poset
14:30:54 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Interfaces
14:30:54 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Completeness
14:30:55 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Export
14:30:56 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Soundness
14:30:56 Zeta_3_Irrational: theory Prime_Distribution_Elementary.PNT_Consequences
14:30:56 Timing PAL (2 threads, 16.873s elapsed time, 16.518s cpu time, 0.469s GC time, factor 0.98)
14:30:56 Finished PAL (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.96)
14:30:56 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical
14:30:56 FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof
14:30:56 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Stratified
14:30:57 FOL_Seq_Calc3: theory FOL_Seq_Calc3.Result
14:30:58 Forcing: theory Forcing.Forcing_Theorems
14:30:59 Forcing: theory Forcing.Separation_Axiom
14:30:59 Forcing: theory Forcing.Infinity_Axiom
14:30:59 Forcing: theory Forcing.Powerset_Axiom
14:31:00 Functional-Automata: theory Functional-Automata.RegExp2NA
14:31:00 Functional-Automata: theory Functional-Automata.RegExp2NAe
14:31:00 Forcing: theory Forcing.Ordinals_In_MG
14:31:00 Rewriting_Z: theory Regular-Sets.NDerivative
14:31:00 Rewriting_Z: theory Regular-Sets.Relation_Interpretation
14:31:00 Forcing: theory Forcing.Replacement_Axiom
14:31:01 Zeta_3_Irrational: theory Zeta_3_Irrational.Zeta_3_Irrational
14:31:01 Timing Old_Datatype_Show (2 threads, 12.019s elapsed time, 12.016s cpu time, 1.368s GC time, factor 1.00)
14:31:01 Finished Old_Datatype_Show (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.98)
14:31:02 Forcing: theory Forcing.Choice_Axiom
14:31:02 Functional-Automata: theory Functional-Automata.AutoRegExp
14:31:02 Timing Random_BSTs (6 threads, 7.407s elapsed time, 7.407s cpu time, 0.318s GC time, factor 1.00)
14:31:02 Finished Random_BSTs (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)
14:31:03 Forcing: theory Forcing.Forcing_Main
14:31:03 Functional-Automata: theory Functional-Automata.Execute
14:31:03 Functional-Automata: theory Functional-Automata.Functional_Automata
14:31:04 Ribbon_Proofs: theory Ribbon_Proofs.Ribbons_Graphical_Soundness
14:31:07 Timing Well_Quasi_Orders (2 threads, 67.018s elapsed time, 66.961s cpu time, 5.124s GC time, factor 1.00)
14:31:07 Finished Well_Quasi_Orders (0:01:10 elapsed time, 0:01:10 cpu time, factor 0.99)
14:31:08 Timing Heard_Of (2 threads, 68.384s elapsed time, 67.796s cpu time, 2.954s GC time, factor 0.99)
14:31:08 Finished Heard_Of (0:01:11 elapsed time, 0:01:10 cpu time, factor 0.99)
14:31:09 Rewriting_Z: theory Regular-Sets.Equivalence_Checking
14:31:09 Timing FocusStreamsCaseStudies (6 threads, 28.983s elapsed time, 28.983s cpu time, 2.047s GC time, factor 1.00)
14:31:09 Finished FocusStreamsCaseStudies (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.99)
14:31:09 Rewriting_Z: theory Regular-Sets.Regexp_Method
14:31:11 Rewriting_Z: theory Abstract-Rewriting.Abstract_Rewriting
14:31:13 Timing FOL_Seq_Calc3 (2 threads, 27.995s elapsed time, 27.994s cpu time, 1.057s GC time, factor 1.00)
14:31:13 Finished FOL_Seq_Calc3 (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.99)
14:31:13 Timing Functional-Automata (2 threads, 27.838s elapsed time, 27.665s cpu time, 1.870s GC time, factor 0.99)
14:31:13 Finished Functional-Automata (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.98)
14:31:13 Finger-Trees: theory Finger-Trees.Test
14:31:13 Timing IO_Language_Conformance (2 threads, 33.311s elapsed time, 33.283s cpu time, 1.268s GC time, factor 1.00)
14:31:14 Finished IO_Language_Conformance (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
14:31:15 Running Abstract_Soundness (on of1-proof+0-7) ...
14:31:15 Timing Wetzels_Problem (2 threads, 113.482s elapsed time, 111.967s cpu time, 4.665s GC time, factor 0.99)
14:31:15 Finished Wetzels_Problem (0:01:57 elapsed time, 0:01:55 cpu time, factor 0.98)
14:31:15 Running VectorSpace (on of1-proof+8-15) ...
14:31:16 Rewriting_Z: theory Rewriting_Z.Z
14:31:16 Rewriting_Z: theory Rewriting_Z.CL_Z
14:31:16 Rewriting_Z: theory Rewriting_Z.Lambda_Z
14:31:16 Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
14:31:16 Running Combinable_Wands (on 10.195.8.49+1) ...
14:31:16 Running Finitely_Generated_Abelian_Groups (on 10.195.8.49+2) ...
14:31:16 Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
14:31:16 Running Special_Function_Bounds (on 10.195.8.49+4) ...
14:31:16 VectorSpace: theory VectorSpace.FunctionLemmas
14:31:16 VectorSpace: theory VectorSpace.RingModuleFacts
14:31:16 VectorSpace: theory VectorSpace.MonoidSums
14:31:17 VectorSpace: theory VectorSpace.LinearCombinations
14:31:18 Running Constructor_Funs (on of3.proof.cit.tum.de+2) ...
14:31:18 Running Euler_Polyhedron_Formula (on of3.proof.cit.tum.de+1) ...
14:31:18 Running Pell (on of3.proof.cit.tum.de+3) ...
14:31:18 Timing Finger-Trees (2 threads, 32.876s elapsed time, 32.825s cpu time, 3.121s GC time, factor 1.00)
14:31:18 Finished Finger-Trees (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
14:31:18 Running Stern_Brocot (on of3.proof.cit.tum.de+0) ...
14:31:18 Combinable_Wands: theory Combinable_Wands.PosRat
14:31:18 Constructor_Funs: theory Constructor_Funs.Constructor_Funs
14:31:19 Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
14:31:19 Timing TLA (2 threads, 33.668s elapsed time, 33.607s cpu time, 1.051s GC time, factor 1.00)
14:31:19 Finished TLA (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
14:31:19 Running Inductive_Confidentiality (on 10.195.8.29+1) ...
14:31:19 Running Recursion-Theory-I (on 10.195.8.29+2) ...
14:31:19 Euler_Polyhedron_Formula: theory Euler_Polyhedron_Formula.Euler_Formula
14:31:19 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
14:31:19 Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
14:31:19 Pell: theory Pell.Efficient_Discrete_Sqrt
14:31:19 Combinable_Wands: theory Combinable_Wands.Mask
14:31:19 Pell: theory Pell.Pell
14:31:19 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
14:31:19 Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
14:31:19 Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
14:31:19 VectorSpace: theory VectorSpace.SumSpaces
14:31:19 Stern_Brocot: theory Stern_Brocot.Cotree
14:31:19 Running GPU_Kernel_PL (on 10.195.8.32+3) ...
14:31:19 VectorSpace: theory VectorSpace.VectorSpace
14:31:20 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom
14:31:20 Inductive_Confidentiality: theory Inductive_Confidentiality.Message
14:31:20 Inductive_Confidentiality: theory Inductive_Confidentiality.MessageGA
14:31:20 Recursion-Theory-I: theory Recursion-Theory-I.CPair
14:31:21 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
14:31:21 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun
14:31:21 GPU_Kernel_PL: theory GPU_Kernel_PL.Misc
14:31:21 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax
14:31:21 Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
14:31:22 Combinable_Wands: theory Combinable_Wands.PartialHeapSA
14:31:22 Timing Abstract_Soundness (8 threads, 5.771s elapsed time, 14.564s cpu time, 1.628s GC time, factor 2.52)
14:31:22 Finished Abstract_Soundness (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.27)
14:31:23 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
14:31:23 Running Decreasing-Diagrams (on 10.195.8.11+0) ...
14:31:23 Running Lambda_Free_RPOs (on 10.195.8.11+4) ...
14:31:23 Timing Ribbon_Proofs (2 threads, 32.920s elapsed time, 32.866s cpu time, 3.128s GC time, factor 1.00)
14:31:23 Finished Ribbon_Proofs (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.99)
14:31:23 Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
14:31:23 Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
14:31:23 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
14:31:24 Pell: theory Pell.Pell_Algorithm
14:31:24 Running Optimal_BST (on 10.195.8.11+2) ...
14:31:25 Timing Constructor_Funs (6 threads, 6.418s elapsed time, 3.863s cpu time, 0.255s GC time, factor 0.60)
14:31:25 Finished Constructor_Funs (0:00:07 elapsed time, 0:00:04 cpu time, factor 0.62)
14:31:25 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds
14:31:25 Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet
14:31:25 Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2
14:31:25 Decreasing-Diagrams: theory Decreasing-Diagrams.Decreasing_Diagrams
14:31:25 Running Attack_Trees (on 10.195.6.179+3) ...
14:31:26 Running CCS (on 10.195.6.179+2) ...
14:31:26 Combinable_Wands: theory Combinable_Wands.CombinableWands
14:31:26 Recursion-Theory-I: theory Recursion-Theory-I.PRecList
14:31:26 Optimal_BST: theory Optimal_BST.Optimal_BST_Examples
14:31:26 Optimal_BST: theory Optimal_BST.Weighted_Path_Length
14:31:27 Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
14:31:27 Lambda_Free_RPOs: theory Nested_Multisets_Ordinals.Multiset_More
14:31:27 Optimal_BST: theory Optimal_BST.Quadrilateral_Inequality
14:31:27 Inductive_Confidentiality: theory Inductive_Confidentiality.EventGA
14:31:27 Attack_Trees: theory Attack_Trees.MC
14:31:27 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
14:31:27 Inductive_Confidentiality: theory Inductive_Confidentiality.Event
14:31:27 Pell: theory Pell.Pell_Algorithm_Test
14:31:27 Running InformationFlowSlicing_Inter (on 10.195.6.179+4) ...
14:31:27 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state
14:31:27 Running Separata (on 10.195.6.179+1) ...
14:31:27 Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
14:31:27 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness
14:31:27 Timing VectorSpace (8 threads, 10.735s elapsed time, 32.516s cpu time, 2.664s GC time, factor 3.03)
14:31:27 Finished VectorSpace (0:00:12 elapsed time, 0:00:34 cpu time, factor 2.79)
14:31:28 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
14:31:28 Optimal_BST: theory Optimal_BST.Optimal_BST
14:31:28 Inductive_Confidentiality: theory Inductive_Confidentiality.PublicGA
14:31:28 Running VerifyThis2019 (on 10.195.6.179+0) ...
14:31:29 CCS: theory CCS.Agent
14:31:29 Inductive_Confidentiality: theory Inductive_Confidentiality.Public
14:31:29 Timing Bell_Numbers_Spivey (2 threads, 29.696s elapsed time, 29.679s cpu time, 0.775s GC time, factor 1.00)
14:31:29 Finished Bell_Numbers_Spivey (0:00:48 elapsed time, 0:00:47 cpu time, factor 0.99)
14:31:29 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread
14:31:29 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
14:31:29 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
14:31:29 Attack_Trees: theory Attack_Trees.AT
14:31:30 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
14:31:30 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
14:31:30 Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr
14:31:31 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
14:31:31 Optimal_BST: theory Optimal_BST.Optimal_BST_Memo
14:31:31 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds
14:31:31 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations
14:31:31 Separata: theory HOL-Eisbach.Eisbach
14:31:31 Separata: theory Separation_Algebra.Separation_Algebra
14:31:31 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
14:31:31 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad_GA
14:31:31 Inductive_Confidentiality: theory Inductive_Confidentiality.NS_Public_Bad
14:31:32 VerifyThis2019: theory VerifyThis2019.Exc_Nres_Monad
14:31:32 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityGA
14:31:32 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group
14:31:32 Inductive_Confidentiality: theory Inductive_Confidentiality.Knowledge
14:31:32 Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
14:31:33 GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel
14:31:33 Inductive_Confidentiality: theory Inductive_Confidentiality.ConfidentialityDY
14:31:33 Attack_Trees: theory Attack_Trees.Infrastructure
14:31:33 Optimal_BST: theory Optimal_BST.Optimal_BST2
14:31:33 Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet
14:31:34 Separata: theory HOL-Eisbach.Eisbach_Tools
14:31:35 Timing Pell (6 threads, 15.500s elapsed time, 15.500s cpu time, 0.421s GC time, factor 1.00)
14:31:35 Finished Pell (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.98)
14:31:35 GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language
14:31:35 Separata: theory Separata.Separata
14:31:35 Optimal_BST: theory Optimal_BST.Optimal_BST_Code
14:31:35 CCS: theory CCS.Strong_Sim
14:31:36 CCS: theory CCS.Struct_Cong
14:31:36 CCS: theory CCS.Strong_Bisim
14:31:36 CCS: theory CCS.Strong_Sim_Pres
14:31:36 CCS: theory CCS.Strong_Bisim_Pres
14:31:36 VerifyThis2019: theory VerifyThis2019.VTcomp
14:31:36 CCS: theory CCS.Strong_Sim_SC
14:31:36 Timing GPU_Kernel_PL (2 threads, 14.555s elapsed time, 14.555s cpu time, 1.240s GC time, factor 1.00)
14:31:36 Finished GPU_Kernel_PL (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
14:31:37 InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
14:31:37 CCS: theory CCS.Tau_Chain
14:31:37 CCS: theory CCS.Strong_Bisim_SC
14:31:37 CCS: theory CCS.Weak_Cong_Semantics
14:31:37 CCS: theory CCS.Weak_Semantics
14:31:37 CCS: theory CCS.Weak_Sim
14:31:38 CCS: theory CCS.Weak_Bisim
14:31:38 CCS: theory CCS.Weak_Cong_Sim
14:31:38 CCS: theory CCS.Weak_Cong_Sim_Pres
14:31:38 CCS: theory CCS.Weak_Sim_Pres
14:31:39 Attack_Trees: theory Attack_Trees.GDPRhealthcare
14:31:39 CCS: theory CCS.Weak_Cong
14:31:39 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
14:31:39 CCS: theory CCS.Weak_Bisim_Pres
14:31:39 CCS: theory CCS.Weak_Cong_Pres
14:31:39 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
14:31:39 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
14:31:42 VerifyThis2019: theory VerifyThis2019.Parallel_Multiset_Fold
14:31:42 VerifyThis2019: theory VerifyThis2019.Challenge1A
14:31:43 Timing Rewriting_Z (2 threads, 56.564s elapsed time, 56.190s cpu time, 3.438s GC time, factor 0.99)
14:31:43 Finished Rewriting_Z (0:00:59 elapsed time, 0:00:58 cpu time, factor 0.99)
14:31:43 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
14:31:43 VerifyThis2019: theory VerifyThis2019.Challenge3
14:31:44 Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
14:31:45 VerifyThis2019: theory VerifyThis2019.Challenge1B
14:31:46 VerifyThis2019: theory VerifyThis2019.Challenge2A
14:31:50 Timing Combinable_Wands (2 threads, 30.178s elapsed time, 30.083s cpu time, 1.524s GC time, factor 1.00)
14:31:50 Finished Combinable_Wands (0:00:32 elapsed time, 0:00:31 cpu time, factor 0.99)
14:31:50 Timing Euler_Polyhedron_Formula (6 threads, 29.956s elapsed time, 29.931s cpu time, 1.607s GC time, factor 1.00)
14:31:50 Finished Euler_Polyhedron_Formula (0:00:31 elapsed time, 0:00:31 cpu time, factor 0.99)
14:31:52 Timing Attack_Trees (2 threads, 23.184s elapsed time, 22.904s cpu time, 1.887s GC time, factor 0.99)
14:31:52 Finished Attack_Trees (0:00:25 elapsed time, 0:00:24 cpu time, factor 0.97)
14:31:52 Timing Inductive_Confidentiality (2 threads, 30.614s elapsed time, 30.573s cpu time, 1.798s GC time, factor 1.00)
14:31:52 Finished Inductive_Confidentiality (0:00:32 elapsed time, 0:00:32 cpu time, factor 0.99)
14:31:55 Timing Recursion-Theory-I (2 threads, 32.725s elapsed time, 32.715s cpu time, 1.504s GC time, factor 1.00)
14:31:55 Finished Recursion-Theory-I (0:00:34 elapsed time, 0:00:34 cpu time, factor 0.99)
14:31:55 Stern_Brocot: theory Stern_Brocot.Bird_Tree
14:31:57 Timing Stern_Brocot (6 threads, 35.975s elapsed time, 35.965s cpu time, 3.524s GC time, factor 1.00)
14:31:57 Finished Stern_Brocot (0:00:38 elapsed time, 0:00:38 cpu time, factor 0.99)
14:31:57 Running PLM (on of1-proof+8-15) ...
14:31:57 Running Strong_Security (on of1-proof+0-7) ...
14:31:57 VerifyThis2019: theory VerifyThis2019.Challenge2B
14:31:57 Timing Separata (2 threads, 26.002s elapsed time, 25.825s cpu time, 0.975s GC time, factor 0.99)
14:31:57 Finished Separata (0:00:28 elapsed time, 0:00:28 cpu time, factor 0.98)
14:31:57 Strong_Security: theory Strong_Security.Types
14:31:57 PLM: theory HOL-Eisbach.Eisbach
14:31:57 PLM: theory PLM.TAO_1_Embedding
14:31:57 PLM: theory HOL-Library.LaTeXsugar
14:31:58 Timing Forcing (2 threads, 78.954s elapsed time, 78.873s cpu time, 2.558s GC time, factor 1.00)
14:31:58 Finished Forcing (0:01:20 elapsed time, 0:01:19 cpu time, factor 0.99)
14:31:58 Strong_Security: theory Strong_Security.Expr
14:31:58 Strong_Security: theory Strong_Security.MWLf
14:31:58 Strong_Security: theory Strong_Security.Strong_Security
14:31:58 PLM: theory HOL-Library.OptionalSugar
14:31:58 Strong_Security: theory Strong_Security.Up_To_Technique
14:31:58 Strong_Security: theory Strong_Security.Parallel_Composition
14:31:58 Running Comparison_Sort_Lower_Bound (on 10.195.8.49+0) ...
14:31:58 Running Digit_Expansions (on 10.195.8.49+1) ...
14:31:58 PLM: theory HOL-Eisbach.Eisbach_Tools
14:31:58 Strong_Security: theory Strong_Security.Domain_example
14:31:58 PLM: theory PLM.TAO_2_Semantics
14:31:59 Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
14:31:59 PLM: theory PLM.TAO_3_Quantifiable
14:31:59 PLM: theory PLM.TAO_4_BasicDefinitions
14:31:59 Strong_Security: theory Strong_Security.Language_Composition
14:31:59 Strong_Security: theory Strong_Security.Type_System
14:31:59 PLM: theory PLM.TAO_5_MetaSolver
14:31:59 Digit_Expansions: theory Digit_Expansions.Bits_Digits
14:31:59 Strong_Security: theory Strong_Security.Type_System_example
14:32:00 Running Euler_MacLaurin (on of3.proof.cit.tum.de+2) ...
14:32:00 Running Impossible_Geometry (on of3.proof.cit.tum.de+1) ...
14:32:00 Running NormByEval (on of3.proof.cit.tum.de+3) ...
14:32:00 Running Types_Tableaus_and_Goedels_God (on of3.proof.cit.tum.de+0) ...
14:32:00 PLM: theory PLM.TAO_6_Identifiable
14:32:00 PLM: theory PLM.TAO_7_Axioms
14:32:00 PLM: theory PLM.TAO_8_Definitions
14:32:00 PLM: theory PLM.TAO_98_ArtificialTheorems
14:32:00 PLM: theory PLM.TAO_99_SanityTests
14:32:01 Digit_Expansions: theory Digit_Expansions.Carries
14:32:01 Impossible_Geometry: theory Impossible_Geometry.Impossible_Geometry
14:32:01 NormByEval: theory NormByEval.NBE
14:32:01 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
14:32:01 Running FeatherweightJava (on 10.195.8.29+0) ...
14:32:01 Running Lam-ml-Normalization (on 10.195.8.29+3) ...
14:32:01 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
14:32:01 Digit_Expansions: theory Digit_Expansions.Binary_Operations
14:32:01 PLM: theory PLM.TAO_9_PLM
14:32:02 Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
14:32:02 Comparison_Sort_Lower_Bound: theory List-Index.List_Index
14:32:02 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
14:32:02 Euler_MacLaurin: theory HOL-Library.Function_Algebras
14:32:02 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
14:32:02 Euler_MacLaurin: theory Landau_Symbols.Group_Sort
14:32:02 Running FOL_Axiomatic (on 10.195.8.32+4) ...
14:32:02 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
14:32:02 Timing Finitely_Generated_Abelian_Groups (2 threads, 41.683s elapsed time, 41.653s cpu time, 2.940s GC time, factor 1.00)
14:32:02 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
14:32:02 Finished Finitely_Generated_Abelian_Groups (0:00:44 elapsed time, 0:00:44 cpu time, factor 0.99)
14:32:02 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
14:32:02 Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
14:32:03 Timing Decreasing-Diagrams (2 threads, 36.058s elapsed time, 36.008s cpu time, 0.972s GC time, factor 1.00)
14:32:03 Finished Decreasing-Diagrams (0:00:39 elapsed time, 0:00:38 cpu time, factor 0.99)
14:32:03 Running IMO2019 (on 10.195.8.32+0) ...
14:32:03 Running Landau_Symbols (on 10.195.8.32+1) ...
14:32:03 Running Random_Graph_Subgraph_Threshold (on 10.195.8.32+2) ...
14:32:03 Running Synthetic_Completeness (on 10.195.8.32+3) ...
14:32:03 Lam-ml-Normalization: theory HOL-Library.LaTeXsugar
14:32:03 FeatherweightJava: theory FeatherweightJava.FJDefs
14:32:03 Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
14:32:03 Timing Strong_Security (8 threads, 4.799s elapsed time, 15.801s cpu time, 1.537s GC time, factor 3.29)
14:32:03 Finished Strong_Security (0:00:05 elapsed time, 0:00:17 cpu time, factor 2.91)
14:32:04 FOL_Axiomatic: theory HOL-Library.Nat_Bijection
14:32:04 FOL_Axiomatic: theory HOL-Library.Old_Datatype
14:32:04 Synthetic_Completeness: theory HOL-Cardinals.Fun_More
14:32:04 Synthetic_Completeness: theory HOL-Cardinals.Order_Relation_More
14:32:04 PLM: theory PLM.TAO_10_PossibleWorlds
14:32:04 PLM: theory PLM.TAO_99_Paradox
14:32:04 PLM: theory PLM.Thesis
14:32:05 Running Lp (on 10.195.8.11+3) ...
14:32:05 Running PropResPI (on 10.195.8.11+1) ...
14:32:05 Synthetic_Completeness: theory HOL-Cardinals.Order_Union
14:32:05 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
14:32:05 Landau_Symbols: theory Landau_Symbols.Group_Sort
14:32:06 Synthetic_Completeness: theory HOL-Cardinals.Wellfounded_More
14:32:06 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Relation
14:32:06 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
14:32:06 IMO2019: theory IMO2019.IMO2019_Q5
14:32:06 IMO2019: theory IMO2019.IMO2019_Q1
14:32:06 PropResPI: theory PropResPI.Propositional_Resolution
14:32:06 Timing Optimal_BST (2 threads, 38.743s elapsed time, 38.717s cpu time, 0.845s GC time, factor 1.00)
14:32:06 Finished Optimal_BST (0:00:41 elapsed time, 0:00:40 cpu time, factor 0.99)
14:32:06 FOL_Axiomatic: theory HOL-Library.Countable
14:32:06 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
14:32:06 IMO2019: theory IMO2019.IMO2019_Q4
14:32:06 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Embedding
14:32:06 Timing PLM (8 threads, 8.162s elapsed time, 34.638s cpu time, 3.745s GC time, factor 4.24)
14:32:06 Finished PLM (0:00:09 elapsed time, 0:00:36 cpu time, factor 3.87)
14:32:07 Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
14:32:07 Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Constructions
14:32:07 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
14:32:07 Lp: theory HOL-Library.Function_Algebras
14:32:07 Lp: theory Ergodic_Theory.SG_Library_Complement
14:32:08 Timing CCS (2 threads, 38.206s elapsed time, 38.001s cpu time, 0.947s GC time, factor 0.99)
14:32:08 Finished CCS (0:00:40 elapsed time, 0:00:39 cpu time, factor 0.99)
14:32:08 Landau_Symbols: theory Landau_Symbols.Landau_Real_Products
14:32:09 Synthetic_Completeness: theory HOL-Cardinals.Cardinal_Order_Relation
14:32:10 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
14:32:10 FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic_Variant
14:32:10 FeatherweightJava: theory FeatherweightJava.FJAux
14:32:10 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
14:32:11 Timing VerifyThis2019 (2 threads, 38.341s elapsed time, 33.052s cpu time, 1.538s GC time, factor 0.86)
14:32:11 Finished VerifyThis2019 (0:00:41 elapsed time, 0:00:36 cpu time, factor 0.87)
14:32:11 FeatherweightJava: theory FeatherweightJava.FJSound
14:32:11 Lp: theory Lp.Functional_Spaces
14:32:11 Synthetic_Completeness: theory Synthetic_Completeness.Maximal_Consistent_Sets
14:32:11 FeatherweightJava: theory FeatherweightJava.Execute
14:32:11 Timing Impossible_Geometry (6 threads, 10.365s elapsed time, 10.266s cpu time, 0.756s GC time, factor 0.99)
14:32:11 Finished Impossible_Geometry (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.96)
14:32:12 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
14:32:12 PropResPI: theory PropResPI.Prime_Implicates
14:32:12 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
14:32:13 Synthetic_Completeness: theory Synthetic_Completeness.Derivations
14:32:13 Synthetic_Completeness: theory Synthetic_Completeness.Refutations
14:32:13 Timing Types_Tableaus_and_Goedels_God (6 threads, 11.790s elapsed time, 11.235s cpu time, 0.441s GC time, factor 0.95)
14:32:13 Finished Types_Tableaus_and_Goedels_God (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.93)
14:32:13 Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_Tableau
14:32:13 Synthetic_Completeness: theory Synthetic_Completeness.Example_First_Order_Logic
14:32:15 Timing Special_Function_Bounds (2 threads, 55.567s elapsed time, 55.539s cpu time, 1.863s GC time, factor 1.00)
14:32:15 Finished Special_Function_Bounds (0:00:58 elapsed time, 0:00:58 cpu time, factor 0.99)
14:32:16 FeatherweightJava: theory FeatherweightJava.Featherweight_Java
14:32:17 Synthetic_Completeness: theory Synthetic_Completeness.Example_Hybrid_Logic
14:32:17 Landau_Symbols: theory Landau_Symbols.Landau_Simprocs
14:32:18 Lp: theory Lp.Lp
14:32:19 Timing InformationFlowSlicing_Inter (2 threads, 47.657s elapsed time, 47.427s cpu time, 4.817s GC time, factor 1.00)
14:32:19 Finished InformationFlowSlicing_Inter (0:00:51 elapsed time, 0:00:50 cpu time, factor 0.99)
14:32:19 Timing IMO2019 (2 threads, 13.055s elapsed time, 13.036s cpu time, 0.447s GC time, factor 1.00)
14:32:19 Finished IMO2019 (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
14:32:19 Landau_Symbols: theory Landau_Symbols.Landau_More
14:32:20 Timing Comparison_Sort_Lower_Bound (2 threads, 17.929s elapsed time, 17.924s cpu time, 1.115s GC time, factor 1.00)
14:32:20 Finished Comparison_Sort_Lower_Bound (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
14:32:21 Timing Zeta_3_Irrational (2 threads, 96.351s elapsed time, 96.263s cpu time, 2.099s GC time, factor 1.00)
14:32:21 Finished Zeta_3_Irrational (0:01:40 elapsed time, 0:01:39 cpu time, factor 1.00)
14:32:24 Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
14:32:24 Timing Lam-ml-Normalization (2 threads, 20.133s elapsed time, 20.098s cpu time, 0.959s GC time, factor 1.00)
14:32:24 Finished Lam-ml-Normalization (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98)
14:32:24 Euler_MacLaurin: theory Landau_Symbols.Landau_More
14:32:25 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
14:32:26 Timing Digit_Expansions (2 threads, 24.748s elapsed time, 24.704s cpu time, 0.443s GC time, factor 1.00)
14:32:26 Finished Digit_Expansions (0:00:26 elapsed time, 0:00:26 cpu time, factor 0.99)
14:32:26 Timing FeatherweightJava (2 threads, 21.776s elapsed time, 21.727s cpu time, 0.782s GC time, factor 1.00)
14:32:26 Finished FeatherweightJava (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)
14:32:28 Timing Random_Graph_Subgraph_Threshold (2 threads, 20.864s elapsed time, 20.818s cpu time, 0.535s GC time, factor 1.00)
14:32:28 Finished Random_Graph_Subgraph_Threshold (0:00:24 elapsed time, 0:00:24 cpu time, factor 0.98)
14:32:29 Timing Landau_Symbols (2 threads, 22.567s elapsed time, 22.549s cpu time, 1.449s GC time, factor 1.00)
14:32:29 Finished Landau_Symbols (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.98)
14:32:29 Timing Euler_MacLaurin (6 threads, 25.957s elapsed time, 25.849s cpu time, 1.372s GC time, factor 1.00)
14:32:29 Finished Euler_MacLaurin (0:00:28 elapsed time, 0:00:27 cpu time, factor 0.98)
14:32:30 Synthetic_Completeness: theory Synthetic_Completeness.Example_Modal_Logic
14:32:30 Timing Lambda_Free_RPOs (2 threads, 62.013s elapsed time, 62.009s cpu time, 3.679s GC time, factor 1.00)
14:32:30 Finished Lambda_Free_RPOs (0:01:05 elapsed time, 0:01:04 cpu time, factor 0.99)
14:32:31 Timing FOL_Axiomatic (2 threads, 25.472s elapsed time, 25.461s cpu time, 2.490s GC time, factor 1.00)
14:32:31 Finished FOL_Axiomatic (0:00:27 elapsed time, 0:00:27 cpu time, factor 0.98)
14:32:31 Running Case_Labeling (on of1-proof+0-7) ...
14:32:31 Running Octonions (on of1-proof+8-15) ...
14:32:32 Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_SC
14:32:32 Case_Labeling: theory Case_Labeling.Case_Labeling
14:32:32 Case_Labeling: theory HOL-Eisbach.Eisbach
14:32:32 Case_Labeling: theory HOL-Hoare.Arith2
14:32:32 Case_Labeling: theory HOL-Hoare.Hoare_Syntax
14:32:32 Case_Labeling: theory HOL-Hoare.Hoare_Tac
14:32:32 Running Binomial-Queues (on 10.195.8.49+2) ...
14:32:32 Running BNF_Operations (on 10.195.8.49+4) ...
14:32:32 Running Fixed_Length_Vector (on 10.195.8.49+3) ...
14:32:32 Octonions: theory Octonions.Cross_Product_7
14:32:32 Case_Labeling: theory Case_Labeling.Conditionals
14:32:32 Case_Labeling: theory Case_Labeling.Monadic_Language
14:32:33 Octonions: theory Octonions.Octonions
14:32:33 Case_Labeling: theory HOL-Hoare.Hoare_Logic
14:32:34 Running Relational-Incorrectness-Logic (on 10.195.8.49+0) ...
14:32:34 Running Tycon (on 10.195.8.49+1) ...
14:32:34 Timing NormByEval (6 threads, 32.528s elapsed time, 32.242s cpu time, 2.166s GC time, factor 0.99)
14:32:34 Finished NormByEval (0:00:34 elapsed time, 0:00:33 cpu time, factor 0.98)
14:32:34 Case_Labeling: theory Case_Labeling.Labeled_Hoare
14:32:34 Binomial-Queues: theory Binomial-Queues.PQ
14:32:34 BNF_Operations: theory HOL-Library.BNF_Axiomatization
14:32:34 Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
14:32:34 Timing PropResPI (2 threads, 27.906s elapsed time, 27.848s cpu time, 1.412s GC time, factor 1.00)
14:32:34 Finished PropResPI (0:00:29 elapsed time, 0:00:29 cpu time, factor 0.99)
14:32:34 Running Certification_Monads (on of3.proof.cit.tum.de+3) ...
14:32:34 Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
14:32:35 Running Combinatorics_Words_Lyndon (on of3.proof.cit.tum.de+2) ...
14:32:35 BNF_Operations: theory BNF_Operations.Compose
14:32:35 BNF_Operations: theory BNF_Operations.GFP
14:32:35 Running IMP2_Binary_Heap (on of3.proof.cit.tum.de+0) ...
14:32:35 Fixed_Length_Vector: theory HOL-Library.Phantom_Type
14:32:35 Binomial-Queues: theory Binomial-Queues.Binomial_Queue
14:32:36 Tycon: theory Tycon.Coerce
14:32:36 Tycon: theory Tycon.TypeApp
14:32:36 Running Jordan_Hoelder (on of3.proof.cit.tum.de+1) ...
14:32:36 Certification_Monads: theory Certification_Monads.Misc
14:32:36 Certification_Monads: theory Deriving.Derive_Manager
14:32:36 Certification_Monads: theory Deriving.Generator_Aux
14:32:36 Certification_Monads: theory HOL-Library.Adhoc_Overloading
14:32:36 Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
14:32:36 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
14:32:36 Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
14:32:36 Timing Case_Labeling (8 threads, 3.577s elapsed time, 11.106s cpu time, 0.960s GC time, factor 3.10)
14:32:36 Finished Case_Labeling (0:00:04 elapsed time, 0:00:12 cpu time, factor 2.64)
14:32:37 Certification_Monads: theory Certification_Monads.Error_Syntax
14:32:37 Certification_Monads: theory HOL-Library.Monad_Syntax
14:32:37 Certification_Monads: theory Show.Show
14:32:37 Certification_Monads: theory Certification_Monads.Strict_Sum
14:32:37 Certification_Monads: theory Certification_Monads.Error_Monad
14:32:37 Relational-Incorrectness-Logic: theory Relational-Incorrectness-Logic.RelationalIncorrectness
14:32:37 Running Orbit_Stabiliser (on 10.195.8.29+3) ...
14:32:37 IMP2_Binary_Heap: theory IMP2_Binary_Heap.IMP2_Binary_Heap
14:32:37 Timing Octonions (8 threads, 3.761s elapsed time, 22.275s cpu time, 1.792s GC time, factor 5.92)
14:32:37 Finished Octonions (0:00:05 elapsed time, 0:00:23 cpu time, factor 4.46)
14:32:38 Tycon: theory Tycon.Functor
14:32:38 Running Randomised_BSTs (on 10.195.8.29+4) ...
14:32:38 Running RefinementReactive (on 10.195.8.29+0) ...
14:32:38 Running Risk_Free_Lending (on 10.195.8.29+1) ...
14:32:38 Fixed_Length_Vector: theory HOL-Library.Cardinality
14:32:38 Jordan_Hoelder: theory Secondary_Sylow.GroupAction
14:32:38 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
14:32:38 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
14:32:39 Running Transformer_Semantics (on 10.195.8.29+2) ...
14:32:39 BNF_Operations: theory BNF_Operations.Kill
14:32:40 RefinementReactive: theory RefinementReactive.Refinement
14:32:40 RefinementReactive: theory RefinementReactive.Temporal
14:32:40 Tycon: theory Tycon.Monad
14:32:40 Tycon: theory Tycon.Lift_Monad
14:32:40 Tycon: theory Tycon.Binary_Tree_Monad
14:32:40 Running FileRefinement (on 10.195.8.32+4) ...
14:32:40 Running First_Welfare_Theorem (on 10.195.8.32+1) ...
14:32:40 Binomial-Queues: theory Binomial-Queues.PQ_Implementation
14:32:40 BNF_Operations: theory BNF_Operations.LFP
14:32:40 Fixed_Length_Vector: theory HOL-Library.Code_Cardinality
14:32:40 Fixed_Length_Vector: theory HOL-Library.Numeral_Type
14:32:41 Tycon: theory Tycon.Monad_Plus
14:32:41 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
14:32:41 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
14:32:41 Risk_Free_Lending: theory Risk_Free_Lending.Risk_Free_Lending
14:32:41 Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
14:32:41 Certification_Monads: theory Certification_Monads.Check_Monad
14:32:41 Tycon: theory Tycon.Monad_Zero
14:32:41 Certification_Monads: theory Certification_Monads.Parser_Monad
14:32:41 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
14:32:41 Jordan_Hoelder: theory Secondary_Sylow.SndSylow
14:32:41 FileRefinement: theory FileRefinement.CArrays
14:32:42 FileRefinement: theory FileRefinement.ResizableArrays
14:32:42 Tycon: theory Tycon.Error_Monad
14:32:42 FileRefinement: theory FileRefinement.FileRefinement
14:32:42 Running InformationFlowSlicing (on 10.195.8.32+2) ...
14:32:42 Running Trie (on 10.195.8.32+0) ...
14:32:42 Tycon: theory Tycon.Resumption_Transformer
14:32:42 Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
14:32:42 Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
14:32:42 Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
14:32:43 Tycon: theory Tycon.Error_Transformer
14:32:43 Running JiveDataStoreModel (on 10.195.8.11+2) ...
14:32:43 Running XML (on 10.195.8.11+0) ...
14:32:43 Fixed_Length_Vector: theory Fixed_Length_Vector.Fixed_Length_Vector
14:32:43 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
14:32:44 Timing Certification_Monads (6 threads, 6.874s elapsed time, 6.874s cpu time, 0.379s GC time, factor 1.00)
14:32:44 Finished Certification_Monads (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.95)
14:32:44 Tycon: theory Tycon.Monad_Zero_Plus
14:32:44 Trie: theory Trie.Trie
14:32:44 First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
14:32:44 First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
14:32:44 JiveDataStoreModel: theory JiveDataStoreModel.TypeIds
14:32:44 RefinementReactive: theory RefinementReactive.Reactive
14:32:45 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
14:32:45 Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
14:32:45 Tycon: theory Tycon.Writer_Monad
14:32:45 First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
14:32:45 Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
14:32:45 First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
14:32:45 XML: theory Deriving.Derive_Manager
14:32:45 XML: theory Deriving.Generator_Aux
14:32:45 BNF_Operations: theory BNF_Operations.Lift
14:32:45 Tycon: theory Tycon.Lazy_List_Monad
14:32:45 XML: theory Certification_Monads.Error_Syntax
14:32:46 XML: theory Certification_Monads.Error_Monad
14:32:46 Timing Combinatorics_Words_Lyndon (6 threads, 8.738s elapsed time, 8.738s cpu time, 0.269s GC time, factor 1.00)
14:32:46 Finished Combinatorics_Words_Lyndon (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.97)
14:32:46 Tycon: theory Tycon.Maybe_Monad
14:32:46 XML: theory Partial_Function_MR.Partial_Function_MR
14:32:46 BNF_Operations: theory BNF_Operations.N2M
14:32:46 InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
14:32:47 XML: theory Certification_Monads.Strict_Sum
14:32:47 Running Belief_Revision (on 10.195.6.179+4) ...
14:32:47 Running Card_Multisets (on 10.195.6.179+1) ...
14:32:47 Running Ramsey-Infinite (on 10.195.6.179+0) ...
14:32:47 Running Robbins-Conjecture (on 10.195.6.179+2) ...
14:32:47 JiveDataStoreModel: theory JiveDataStoreModel.JavaType
14:32:47 Running StrictOmegaCategories (on 10.195.6.179+3) ...
14:32:47 Tycon: theory Tycon.State_Transformer
14:32:48 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
14:32:48 Tycon: theory Tycon.Writer_Transformer
14:32:48 BNF_Operations: theory BNF_Operations.Permute
14:32:48 Trie: theory Trie.Tries
14:32:48 Belief_Revision: theory Belief_Revision.AGM_Logic
14:32:48 Card_Multisets: theory HOL-Library.Cancellation
14:32:48 Ramsey-Infinite: theory HOL-Library.FuncSet
14:32:48 Robbins-Conjecture: theory Robbins-Conjecture.Robbins_Conjecture
14:32:48 Ramsey-Infinite: theory HOL-Library.Infinite_Set
14:32:49 StrictOmegaCategories: theory HOL-Library.FuncSet
14:32:49 Timing Relational-Incorrectness-Logic (2 threads, 11.043s elapsed time, 10.981s cpu time, 0.308s GC time, factor 0.99)
14:32:49 Finished Relational-Incorrectness-Logic (0:00:14 elapsed time, 0:00:13 cpu time, factor 0.97)
14:32:49 XML: theory Show.Show
14:32:49 First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
14:32:50 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
14:32:50 Timing Binomial-Queues (2 threads, 14.174s elapsed time, 14.155s cpu time, 0.583s GC time, factor 1.00)
14:32:50 Finished Binomial-Queues (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.98)
14:32:50 Card_Multisets: theory HOL-Library.Multiset
14:32:50 JiveDataStoreModel: theory JiveDataStoreModel.DirectSubtypes
14:32:50 Belief_Revision: theory Belief_Revision.AGM_Remainder
14:32:50 JiveDataStoreModel: theory JiveDataStoreModel.Subtype
14:32:50 Tycon: theory Tycon.Monad_Transformer
14:32:50 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
14:32:50 JiveDataStoreModel: theory JiveDataStoreModel.Attributes
14:32:50 JiveDataStoreModel: theory JiveDataStoreModel.Value
14:32:50 Belief_Revision: theory Belief_Revision.AGM_Contraction
14:32:50 InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
14:32:51 Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
14:32:51 Timing Fixed_Length_Vector (2 threads, 14.053s elapsed time, 12.926s cpu time, 0.480s GC time, factor 0.92)
14:32:51 Finished Fixed_Length_Vector (0:00:16 elapsed time, 0:00:14 cpu time, factor 0.91)
14:32:51 First_Welfare_Theorem: theory First_Welfare_Theorem.Common
14:32:51 StrictOmegaCategories: theory StrictOmegaCategories.Globular_Set
14:32:51 Ramsey-Infinite: theory HOL-Library.Ramsey
14:32:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
14:32:52 XML: theory Certification_Monads.Parser_Monad
14:32:52 First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
14:32:53 Ramsey-Infinite: theory Ramsey-Infinite.Ramsey
14:32:53 Belief_Revision: theory Belief_Revision.AGM_Revision
14:32:53 First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
14:32:54 JiveDataStoreModel: theory JiveDataStoreModel.AttributesIndep
14:32:54 JiveDataStoreModel: theory JiveDataStoreModel.Location
14:32:54 StrictOmegaCategories: theory StrictOmegaCategories.Strict_Omega_Category
14:32:55 XML: theory XML.Xml
14:32:56 StrictOmegaCategories: theory StrictOmegaCategories.Pasting_Diagram
14:32:56 Timing FileRefinement (2 threads, 13.864s elapsed time, 13.863s cpu time, 0.138s GC time, factor 1.00)
14:32:56 Finished FileRefinement (0:00:15 elapsed time, 0:00:15 cpu time, factor 0.98)
14:32:56 JiveDataStoreModel: theory JiveDataStoreModel.Store
14:32:57 Timing RefinementReactive (2 threads, 16.492s elapsed time, 16.486s cpu time, 0.444s GC time, factor 1.00)
14:32:57 Finished RefinementReactive (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.97)
14:32:58 Timing Tycon (2 threads, 20.469s elapsed time, 20.373s cpu time, 0.840s GC time, factor 1.00)
14:32:58 Finished Tycon (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
14:32:58 Timing IMP2_Binary_Heap (6 threads, 20.123s elapsed time, 20.122s cpu time, 0.772s GC time, factor 1.00)
14:32:58 Finished IMP2_Binary_Heap (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
14:32:58 Timing Risk_Free_Lending (2 threads, 16.771s elapsed time, 16.712s cpu time, 0.429s GC time, factor 1.00)
14:32:58 Finished Risk_Free_Lending (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
14:32:58 Timing Orbit_Stabiliser (2 threads, 17.036s elapsed time, 17.034s cpu time, 0.540s GC time, factor 1.00)
14:32:58 Finished Orbit_Stabiliser (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
14:32:58 JiveDataStoreModel: theory JiveDataStoreModel.StoreProperties
14:32:59 Timing Jordan_Hoelder (6 threads, 20.382s elapsed time, 20.373s cpu time, 0.910s GC time, factor 1.00)
14:32:59 Finished Jordan_Hoelder (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
14:32:59 JiveDataStoreModel: theory JiveDataStoreModel.JML
14:32:59 JiveDataStoreModel: theory JiveDataStoreModel.UnivSpec
14:33:02 XML: theory XML.Xmlt
14:33:03 Card_Multisets: theory Card_Multisets.Card_Multisets
14:33:05 Timing Trie (2 threads, 20.170s elapsed time, 20.128s cpu time, 0.609s GC time, factor 1.00)
14:33:05 Finished Trie (0:00:22 elapsed time, 0:00:22 cpu time, factor 0.98)
14:33:05 Timing InformationFlowSlicing (2 threads, 20.194s elapsed time, 20.058s cpu time, 0.751s GC time, factor 0.99)
14:33:05 Finished InformationFlowSlicing (0:00:23 elapsed time, 0:00:22 cpu time, factor 0.98)
14:33:06 Timing Randomised_BSTs (2 threads, 24.488s elapsed time, 24.487s cpu time, 0.734s GC time, factor 1.00)
14:33:06 Finished Randomised_BSTs (0:00:28 elapsed time, 0:00:27 cpu time, factor 0.99)
14:33:08 Timing Robbins-Conjecture (2 threads, 18.751s elapsed time, 18.662s cpu time, 0.498s GC time, factor 1.00)
14:33:08 Finished Robbins-Conjecture (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
14:33:08 Timing JiveDataStoreModel (2 threads, 23.260s elapsed time, 23.037s cpu time, 1.433s GC time, factor 0.99)
14:33:08 Finished JiveDataStoreModel (0:00:25 elapsed time, 0:00:24 cpu time, factor 0.98)
14:33:10 Timing Transformer_Semantics (2 threads, 27.034s elapsed time, 26.929s cpu time, 0.856s GC time, factor 1.00)
14:33:10 Finished Transformer_Semantics (0:00:30 elapsed time, 0:00:29 cpu time, factor 0.98)
14:33:10 Timing First_Welfare_Theorem (2 threads, 24.855s elapsed time, 24.852s cpu time, 0.851s GC time, factor 1.00)
14:33:10 Finished First_Welfare_Theorem (0:00:27 elapsed time, 0:00:27 cpu time, factor 0.99)
14:33:12 Timing StrictOmegaCategories (2 threads, 23.005s elapsed time, 22.932s cpu time, 0.687s GC time, factor 1.00)
14:33:12 Finished StrictOmegaCategories (0:00:25 elapsed time, 0:00:24 cpu time, factor 0.98)
14:33:13 Running Cayley_Hamilton (on of1-proof+8-15) ...
14:33:13 Running CryptoBasedCompositionalProperties (on of1-proof+0-7) ...
14:33:14 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.ListExtras
14:33:14 Timing Belief_Revision (2 threads, 25.260s elapsed time, 25.258s cpu time, 0.762s GC time, factor 1.00)
14:33:14 Finished Belief_Revision (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.99)
14:33:14 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy_types
14:33:14 Running HotelKeyCards (on 10.195.8.49+2) ...
14:33:14 Running Laplace_Transform (on 10.195.8.49+0) ...
14:33:14 Running Lower_Semicontinuous (on 10.195.8.49+3) ...
14:33:14 Running Maximum_Segment_Sum (on 10.195.8.49+1) ...
14:33:14 Cayley_Hamilton: theory HOL-Library.More_List
14:33:14 Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
14:33:14 Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
14:33:15 Running Catalan_Numbers (on of3.proof.cit.tum.de+2) ...
14:33:15 Running Euler_Partition (on of3.proof.cit.tum.de+3) ...
14:33:15 Running Finite-Map-Extras (on of3.proof.cit.tum.de+0) ...
14:33:15 Running HyperCTL (on of3.proof.cit.tum.de+1) ...
14:33:15 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.inout
14:33:15 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy
14:33:16 Timing Lp (2 threads, 67.371s elapsed time, 67.204s cpu time, 1.502s GC time, factor 1.00)
14:33:16 Finished Lp (0:01:11 elapsed time, 0:01:10 cpu time, factor 0.99)
14:33:16 HotelKeyCards: theory HOL-Library.LaTeXsugar
14:33:16 Maximum_Segment_Sum: theory Maximum_Segment_Sum.Maximum_Segment_Sum
14:33:16 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.CompLocalSecrets
14:33:16 Running LambdaMu (on 10.195.8.29+0) ...
14:33:16 Running Neumann_Morgenstern_Utility (on 10.195.8.29+3) ...
14:33:16 Euler_Partition: theory HOL-Library.Cancellation
14:33:16 Running Youngs_Inequality (on 10.195.8.29+1) ...
14:33:16 Finite-Map-Extras: theory HOL-Library.AList
14:33:16 Finite-Map-Extras: theory HOL-Library.Conditional_Parametricity
14:33:16 Finite-Map-Extras: theory HOL-Library.Nat_Bijection
14:33:16 Finite-Map-Extras: theory HOL-Library.Old_Datatype
14:33:16 CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
14:33:17 HotelKeyCards: theory HotelKeyCards.Notation
14:33:17 HotelKeyCards: theory HotelKeyCards.Basis
14:33:17 Timing Card_Multisets (2 threads, 27.274s elapsed time, 27.274s cpu time, 0.936s GC time, factor 1.00)
14:33:17 Finished Card_Multisets (0:00:29 elapsed time, 0:00:29 cpu time, factor 0.99)
14:33:17 HyperCTL: theory HyperCTL.Prelim
14:33:17 Timing Ramsey-Infinite (2 threads, 27.619s elapsed time, 27.601s cpu time, 0.573s GC time, factor 1.00)
14:33:17 Finished Ramsey-Infinite (0:00:29 elapsed time, 0:00:29 cpu time, factor 0.99)
14:33:17 HotelKeyCards: theory HotelKeyCards.State
14:33:17 HyperCTL: theory HyperCTL.Shallow
14:33:17 Euler_Partition: theory HOL-Library.Multiset
14:33:17 HotelKeyCards: theory HotelKeyCards.Trace
14:33:17 Catalan_Numbers: theory HOL-Library.Function_Algebras
14:33:17 Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
14:33:17 Catalan_Numbers: theory Landau_Symbols.Group_Sort
14:33:17 Timing BNF_Operations (2 threads, 39.953s elapsed time, 39.917s cpu time, 5.395s GC time, factor 1.00)
14:33:17 Finished BNF_Operations (0:00:43 elapsed time, 0:00:43 cpu time, factor 0.99)
14:33:17 Running Latin_Square (on 10.195.8.32+0) ...
14:33:17 Running Median_Method (on 10.195.8.32+2) ...
14:33:17 Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
14:33:17 Running Pratt_Certificate (on 10.195.8.32+1) ...
14:33:17 Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
14:33:18 Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
14:33:18 Running Public_Announcement_Logic (on 10.195.8.32+4) ...
14:33:18 LambdaMu: theory LambdaMu.Syntax
14:33:18 Timing CryptoBasedCompositionalProperties (8 threads, 3.649s elapsed time, 11.712s cpu time, 1.483s GC time, factor 3.21)
14:33:18 Finished CryptoBasedCompositionalProperties (0:00:04 elapsed time, 0:00:12 cpu time, factor 2.72)
14:33:18 Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
14:33:18 Running CISC-Kernel (on 10.195.8.11+1) ...
14:33:18 Running Dedekind_Real (on 10.195.8.11+4) ...
14:33:18 Running LatticeProperties (on 10.195.8.11+2) ...
14:33:18 Latin_Square: theory Marriage.Marriage
14:33:18 Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
14:33:19 Youngs_Inequality: theory Youngs_Inequality.Youngs
14:33:19 HotelKeyCards: theory HotelKeyCards.NewCard
14:33:19 HotelKeyCards: theory HotelKeyCards.Equivalence
14:33:19 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
14:33:19 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
14:33:19 Latin_Square: theory Latin_Square.Latin_Square
14:33:19 Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
14:33:19 Finite-Map-Extras: theory HOL-Library.Countable
14:33:19 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
14:33:19 Timing Synthetic_Completeness (2 threads, 73.280s elapsed time, 73.274s cpu time, 6.511s GC time, factor 1.00)
14:33:19 Finished Synthetic_Completeness (0:01:16 elapsed time, 0:01:16 cpu time, factor 0.99)
14:33:19 Laplace_Transform: theory Laplace_Transform.Existence
14:33:19 HyperCTL: theory HyperCTL.Deep
14:33:20 HyperCTL: theory HyperCTL.Noninterference
14:33:20 Pratt_Certificate: theory Lehmer.Lehmer
14:33:20 CISC-Kernel: theory CISC-Kernel.List_Theorems
14:33:20 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
14:33:20 CISC-Kernel: theory CISC-Kernel.Option_Binders
14:33:20 Dedekind_Real: theory Dedekind_Real.Dedekind_Real
14:33:20 LatticeProperties: theory LatticeProperties.Conj_Disj
14:33:20 LatticeProperties: theory LatticeProperties.Lattice_Prop
14:33:20 Timing Cayley_Hamilton (8 threads, 5.363s elapsed time, 22.558s cpu time, 2.276s GC time, factor 4.21)
14:33:20 Finished Cayley_Hamilton (0:00:06 elapsed time, 0:00:24 cpu time, factor 3.51)
14:33:21 CISC-Kernel: theory CISC-Kernel.Step_configuration
14:33:21 CISC-Kernel: theory CISC-Kernel.K
14:33:21 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
14:33:21 Laplace_Transform: theory Laplace_Transform.Uniqueness
14:33:21 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
14:33:21 Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
14:33:21 LatticeProperties: theory LatticeProperties.WellFoundedTransitive
14:33:21 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice
14:33:22 Laplace_Transform: theory Laplace_Transform.Laplace_Transform
14:33:22 Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
14:33:22 Timing XML (2 threads, 35.733s elapsed time, 35.685s cpu time, 3.714s GC time, factor 1.00)
14:33:22 Finished XML (0:00:39 elapsed time, 0:00:38 cpu time, factor 0.99)
14:33:23 CISC-Kernel: theory CISC-Kernel.SK
14:33:23 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop
14:33:23 LambdaMu: theory LambdaMu.DeBruijn
14:33:23 LambdaMu: theory LambdaMu.Types
14:33:23 Timing Maximum_Segment_Sum (2 threads, 6.428s elapsed time, 6.227s cpu time, 0.129s GC time, factor 0.97)
14:33:23 Finished Maximum_Segment_Sum (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.94)
14:33:23 CISC-Kernel: theory CISC-Kernel.Step_policies
14:33:23 Median_Method: theory Median_Method.Median
14:33:23 CISC-Kernel: theory CISC-Kernel.Step
14:33:23 LambdaMu: theory LambdaMu.Substitution
14:33:24 LambdaMu: theory LambdaMu.Peirce
14:33:24 Running Minimal_SSA (on 10.195.6.179+3) ...
14:33:24 Running Rank_Nullity_Theorem (on 10.195.6.179+2) ...
14:33:24 Finite-Map-Extras: theory HOL-Library.FSet
14:33:24 LambdaMu: theory LambdaMu.Reduction
14:33:24 CISC-Kernel: theory CISC-Kernel.ISK
14:33:25 LambdaMu: theory LambdaMu.ContextFacts
14:33:25 Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
14:33:26 LambdaMu: theory LambdaMu.TypePreservation
14:33:26 LambdaMu: theory LambdaMu.Progress
14:33:26 CISC-Kernel: theory CISC-Kernel.CISK
14:33:26 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group
14:33:26 Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
14:33:27 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
14:33:27 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
14:33:27 Minimal_SSA: theory Minimal_SSA.Irreducible
14:33:27 Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
14:33:28 Timing HotelKeyCards (2 threads, 11.485s elapsed time, 11.457s cpu time, 0.339s GC time, factor 1.00)
14:33:28 Finished HotelKeyCards (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
14:33:28 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
14:33:28 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
14:33:29 Catalan_Numbers: theory Landau_Symbols.Landau_More
14:33:29 Timing LatticeProperties (2 threads, 8.436s elapsed time, 8.434s cpu time, 0.250s GC time, factor 1.00)
14:33:29 Finished LatticeProperties (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.96)
14:33:30 Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
14:33:31 Finite-Map-Extras: theory HOL-Library.Finite_Map
14:33:31 Euler_Partition: theory Card_Number_Partitions.Additions_to_Main
14:33:31 CISC-Kernel: theory CISC-Kernel.Step_invariants
14:33:32 Euler_Partition: theory Card_Number_Partitions.Number_Partition
14:33:32 CISC-Kernel: theory CISC-Kernel.Step_vpeq
14:33:32 CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects
14:33:32 CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent
14:33:32 CISC-Kernel: theory CISC-Kernel.Separation_kernel_model
14:33:32 Euler_Partition: theory Euler_Partition.Euler_Partition
14:33:32 HyperCTL: theory HyperCTL.Finite_Noninterference
14:33:33 Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
14:33:33 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
14:33:34 Timing LambdaMu (2 threads, 15.951s elapsed time, 15.858s cpu time, 0.573s GC time, factor 0.99)
14:33:34 Finished LambdaMu (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.98)
14:33:34 CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK
14:33:35 Timing Public_Announcement_Logic (2 threads, 15.336s elapsed time, 15.301s cpu time, 1.114s GC time, factor 1.00)
14:33:35 Finished Public_Announcement_Logic (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.98)
14:33:35 HyperCTL: theory HyperCTL.HyperCTL
14:33:36 Timing Catalan_Numbers (6 threads, 18.000s elapsed time, 17.983s cpu time, 1.059s GC time, factor 1.00)
14:33:36 Finished Catalan_Numbers (0:00:20 elapsed time, 0:00:19 cpu time, factor 0.98)
14:33:36 Timing Latin_Square (2 threads, 16.257s elapsed time, 16.232s cpu time, 0.379s GC time, factor 1.00)
14:33:36 Finished Latin_Square (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.97)
14:33:36 Timing Youngs_Inequality (2 threads, 16.790s elapsed time, 16.693s cpu time, 0.383s GC time, factor 0.99)
14:33:36 Finished Youngs_Inequality (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
14:33:36 Timing Median_Method (2 threads, 15.440s elapsed time, 15.440s cpu time, 0.429s GC time, factor 1.00)
14:33:36 Finished Median_Method (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
14:33:36 Timing Dedekind_Real (2 threads, 15.530s elapsed time, 15.523s cpu time, 0.230s GC time, factor 1.00)
14:33:36 Finished Dedekind_Real (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.97)
14:33:36 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
14:33:37 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
14:33:37 Timing HyperCTL (6 threads, 19.578s elapsed time, 19.569s cpu time, 1.684s GC time, factor 1.00)
14:33:37 Finished HyperCTL (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
14:33:37 Timing Euler_Partition (6 threads, 20.766s elapsed time, 20.757s cpu time, 1.006s GC time, factor 1.00)
14:33:37 Finished Euler_Partition (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98)
14:33:39 Timing Lower_Semicontinuous (2 threads, 20.387s elapsed time, 20.337s cpu time, 0.386s GC time, factor 1.00)
14:33:39 Finished Lower_Semicontinuous (0:00:23 elapsed time, 0:00:23 cpu time, factor 0.98)
14:33:40 Finite-Map-Extras: theory Finite-Map-Extras.Finite_Map_Extras
14:33:42 Timing Rank_Nullity_Theorem (2 threads, 14.877s elapsed time, 14.856s cpu time, 0.508s GC time, factor 1.00)
14:33:42 Finished Rank_Nullity_Theorem (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.98)
14:33:43 Timing Laplace_Transform (2 threads, 25.396s elapsed time, 25.355s cpu time, 0.492s GC time, factor 1.00)
14:33:43 Finished Laplace_Transform (0:00:28 elapsed time, 0:00:28 cpu time, factor 0.98)
14:33:43 Timing Finite-Map-Extras (6 threads, 26.625s elapsed time, 23.530s cpu time, 0.869s GC time, factor 0.88)
14:33:43 Finished Finite-Map-Extras (0:00:28 elapsed time, 0:00:24 cpu time, factor 0.88)
14:33:44 Timing Minimal_SSA (2 threads, 17.120s elapsed time, 17.009s cpu time, 0.516s GC time, factor 0.99)
14:33:44 Finished Minimal_SSA (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
14:33:48 Timing Pratt_Certificate (2 threads, 27.540s elapsed time, 27.537s cpu time, 0.589s GC time, factor 1.00)
14:33:48 Finished Pratt_Certificate (0:00:30 elapsed time, 0:00:30 cpu time, factor 0.99)
14:33:49 Running MiniML (on of1-proof+8-15) ...
14:33:49 Running MuchAdoAboutTwo (on of1-proof+0-7) ...
14:33:49 MiniML: theory MiniML.Maybe
14:33:49 MiniML: theory MiniML.Type
14:33:50 MuchAdoAboutTwo: theory HOL-Combinatorics.Transposition
14:33:50 Running C2KA_DistributedSystems (on 10.195.8.49+3) ...
14:33:50 Running CYK (on 10.195.8.49+2) ...
14:33:50 Running Lazy-Lists-II (on 10.195.8.49+1) ...
14:33:50 MuchAdoAboutTwo: theory HOL-Combinatorics.Permutations
14:33:51 Running Pop_Refinement (on 10.195.8.49+4) ...
14:33:51 Running Binomial-Heaps (on of3.proof.cit.tum.de+2) ...
14:33:51 Running DPT-SAT-Solver (on of3.proof.cit.tum.de+1) ...
14:33:51 MiniML: theory MiniML.Instance
14:33:51 MuchAdoAboutTwo: theory MuchAdoAboutTwo.MuchAdoAboutTwo
14:33:51 MiniML: theory MiniML.Generalize
14:33:51 MiniML: theory MiniML.MiniML
14:33:51 MiniML: theory MiniML.W
14:33:52 Running GaleStewart_Games (on of3.proof.cit.tum.de+0) ...
14:33:52 Running Verified-Prover (on of3.proof.cit.tum.de+3) ...
14:33:52 CYK: theory CYK.CYK
14:33:52 Pop_Refinement: theory Pop_Refinement.Definition
14:33:52 C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
14:33:52 Pop_Refinement: theory Pop_Refinement.First_Example
14:33:52 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
14:33:52 Pop_Refinement: theory Pop_Refinement.Future_Work
14:33:52 Binomial-Heaps: theory Binomial-Heaps.BinomialHeap
14:33:52 Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap
14:33:52 Pop_Refinement: theory Pop_Refinement.General_Remarks
14:33:52 Pop_Refinement: theory Pop_Refinement.Related_Work
14:33:53 Verified-Prover: theory Verified-Prover.Prover
14:33:53 Pop_Refinement: theory Pop_Refinement.Second_Example
14:33:53 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Solver
14:33:53 GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
14:33:53 Timing MuchAdoAboutTwo (8 threads, 2.598s elapsed time, 9.798s cpu time, 0.882s GC time, factor 3.77)
14:33:53 Finished MuchAdoAboutTwo (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.85)
14:33:53 GaleStewart_Games: theory GaleStewart_Games.MorePrefix
14:33:53 GaleStewart_Games: theory GaleStewart_Games.MoreENat
14:33:53 DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Tests
14:33:53 Running DigitsInBase (on 10.195.8.29+1) ...
14:33:53 Running Hello_World (on 10.195.8.29+4) ...
14:33:53 Lazy-Lists-II: theory Lazy-Lists-II.LList2
14:33:53 Running Nano_JSON (on 10.195.8.29+2) ...
14:33:53 Running Pairing_Heap (on 10.195.8.29+0) ...
14:33:53 Timing MiniML (8 threads, 3.406s elapsed time, 8.514s cpu time, 0.796s GC time, factor 2.50)
14:33:53 Finished MiniML (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.18)
14:33:54 GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
14:33:54 Running ArrowImpossibilityGS (on 10.195.8.32+0) ...
14:33:54 Running Category (on 10.195.8.32+4) ...
14:33:54 Running FinFun (on 10.195.8.32+3) ...
14:33:54 Running Skip_Lists (on 10.195.8.32+2) ...
14:33:55 GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
14:33:55 Nano_JSON: theory Nano_JSON.Nano_JSON
14:33:55 Hello_World: theory HOL-Library.Adhoc_Overloading
14:33:55 Hello_World: theory HOL-Library.Monad_Syntax
14:33:55 Hello_World: theory Hello_World.IO
14:33:55 Running Banach_Steinhaus (on 10.195.8.11+2) ...
14:33:55 C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
14:33:55 Pairing_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
14:33:55 DigitsInBase: theory DigitsInBase.DigitsInBase
14:33:56 Hello_World: theory Hello_World.HelloWorld
14:33:56 ArrowImpossibilityGS: theory HOL-Library.FuncSet
14:33:56 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Utility
14:33:56 Category: theory HOL-Library.FuncSet
14:33:56 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List2
14:33:56 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List1
14:33:56 FinFun: theory HOL-Library.Phantom_Type
14:33:56 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
14:33:56 Timing DPT-SAT-Solver (6 threads, 3.071s elapsed time, 3.071s cpu time, 0.110s GC time, factor 1.00)
14:33:56 Finished DPT-SAT-Solver (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.92)
14:33:56 Running LP_Duality (on 10.195.8.11+3) ...
14:33:56 Running Menger (on 10.195.8.11+4) ...
14:33:56 Running Transitive-Closure-II (on 10.195.8.11+0) ...
14:33:56 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
14:33:57 GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
14:33:57 C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
14:33:57 Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
14:33:57 Skip_Lists: theory Skip_Lists.Pi_pmf
14:33:57 FinFun: theory HOL-Library.Cardinality
14:33:58 Menger: theory Menger.Graph
14:33:58 Menger: theory Menger.Helpers
14:33:58 Transitive-Closure-II: theory HOL-Library.While_Combinator
14:33:58 Transitive-Closure-II: theory Regular-Sets.Regular_Set
14:33:58 Category: theory Category.Cat
14:33:58 ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Order
14:33:59 Timing C2KA_DistributedSystems (2 threads, 6.348s elapsed time, 6.169s cpu time, 0.219s GC time, factor 0.97)
14:33:59 Nano_JSON: theory Nano_JSON.Nano_JSON_Query
14:33:59 Finished C2KA_DistributedSystems (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.93)
14:33:59 Hello_World: theory Hello_World.HelloWorld_Proof
14:33:59 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
14:33:59 Timing GaleStewart_Games (6 threads, 5.810s elapsed time, 5.807s cpu time, 0.148s GC time, factor 1.00)
14:33:59 Finished GaleStewart_Games (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.95)
14:33:59 Timing Lazy-Lists-II (2 threads, 5.298s elapsed time, 5.279s cpu time, 0.156s GC time, factor 1.00)
14:33:59 Finished Lazy-Lists-II (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.95)
14:33:59 Running Discrete_Summation (on 10.195.6.179+3) ...
14:33:59 ArrowImpossibilityGS: theory ArrowImpossibilityGS.GS
14:33:59 Running GoedelGod (on 10.195.6.179+0) ...
14:33:59 Skip_Lists: theory Skip_Lists.Misc
14:33:59 Skip_Lists: theory Skip_Lists.Geometric_PMF
14:33:59 Category: theory Category.Functors
14:34:00 Category: theory Category.SetCat
14:34:00 Nano_JSON: theory Nano_JSON.Nano_JSON_Main
14:34:00 Nano_JSON: theory Nano_JSON.Example
14:34:00 FinFun: theory FinFun.FinFun
14:34:00 Hello_World: theory Hello_World.RunningCodeFromIsabelle
14:34:00 Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
14:34:00 LP_Duality: theory LP_Duality.Minimum_Maximum
14:34:00 Pairing_Heap: theory Pairing_Heap.Pairing_Heap_Tree
14:34:00 Nano_JSON: theory Nano_JSON.Example_Real
14:34:00 Nano_JSON: theory Nano_JSON.Nano_JSON_Manual
14:34:01 LP_Duality: theory LP_Duality.LP_Duality
14:34:01 Menger: theory Menger.Separations
14:34:01 Timing Hello_World (2 threads, 5.774s elapsed time, 2.806s cpu time, 0.068s GC time, factor 0.49)
14:34:01 Finished Hello_World (0:00:07 elapsed time, 0:00:04 cpu time, factor 0.56)
14:34:01 Skip_Lists: theory Skip_Lists.Skip_List
14:34:01 Discrete_Summation: theory Discrete_Summation.Discrete_Summation
14:34:01 Discrete_Summation: theory HOL-Combinatorics.Stirling
14:34:01 Category: theory Category.NatTrans
14:34:01 Menger: theory Menger.DisjointPaths
14:34:02 Category: theory Category.HomFunctors
14:34:02 Timing CYK (2 threads, 9.207s elapsed time, 9.185s cpu time, 0.392s GC time, factor 1.00)
14:34:02 Finished CYK (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.97)
14:34:02 Timing Neumann_Morgenstern_Utility (2 threads, 42.078s elapsed time, 41.966s cpu time, 1.281s GC time, factor 1.00)
14:34:02 Finished Neumann_Morgenstern_Utility (0:00:45 elapsed time, 0:00:45 cpu time, factor 0.99)
14:34:02 Discrete_Summation: theory Discrete_Summation.Factorials
14:34:02 Timing Verified-Prover (6 threads, 9.500s elapsed time, 9.500s cpu time, 0.290s GC time, factor 1.00)
14:34:02 Finished Verified-Prover (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.97)
14:34:02 Running Nullstellensatz (on 10.195.6.179+2) ...
14:34:02 Running Partial_Function_MR (on 10.195.6.179+1) ...
14:34:02 Timing Nano_JSON (2 threads, 7.043s elapsed time, 6.989s cpu time, 0.372s GC time, factor 0.99)
14:34:02 Finished Nano_JSON (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.95)
14:34:02 Running Prefix_Free_Code_Combinators (on 10.195.6.179+4) ...
14:34:02 Category: theory Category.Yoneda
14:34:03 Transitive-Closure-II: theory Regular-Sets.Regular_Exp
14:34:03 Menger: theory Menger.MengerInduction
14:34:04 Discrete_Summation: theory Discrete_Summation.Summation_Conversion
14:34:04 FinFun: theory FinFun.FinFunPred
14:34:04 GoedelGod: theory GoedelGod.GoedelGod
14:34:04 Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
14:34:04 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
14:34:04 Timing CISC-Kernel (2 threads, 42.651s elapsed time, 42.575s cpu time, 3.213s GC time, factor 1.00)
14:34:04 Finished CISC-Kernel (0:00:45 elapsed time, 0:00:44 cpu time, factor 0.99)
14:34:04 Partial_Function_MR: theory HOL-Library.Monad_Syntax
14:34:05 Timing DigitsInBase (2 threads, 8.487s elapsed time, 8.408s cpu time, 0.208s GC time, factor 0.99)
14:34:05 Menger: theory Menger.Y_eq_new_last
14:34:05 Finished DigitsInBase (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.96)
14:34:05 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
14:34:05 Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
14:34:05 Menger: theory Menger.Y_neq_new_last
14:34:05 Timing Pairing_Heap (2 threads, 8.968s elapsed time, 8.944s cpu time, 0.646s GC time, factor 1.00)
14:34:05 Finished Pairing_Heap (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:34:05 Discrete_Summation: theory Discrete_Summation.Examples
14:34:06 Menger: theory Menger.Menger
14:34:06 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
14:34:06 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
14:34:07 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
14:34:07 Nullstellensatz: theory Nullstellensatz.Univariate_PM
14:34:08 Timing Pop_Refinement (2 threads, 15.700s elapsed time, 15.622s cpu time, 0.765s GC time, factor 1.00)
14:34:08 Finished Pop_Refinement (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.98)
14:34:08 Timing FinFun (2 threads, 11.885s elapsed time, 11.853s cpu time, 0.438s GC time, factor 1.00)
14:34:08 Finished FinFun (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
14:34:09 Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Examples
14:34:10 Timing Category (2 threads, 13.626s elapsed time, 13.560s cpu time, 0.545s GC time, factor 1.00)
14:34:10 Finished Category (0:00:15 elapsed time, 0:00:15 cpu time, factor 0.97)
14:34:10 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
14:34:10 Transitive-Closure-II: theory Regular-Sets.NDerivative
14:34:11 Transitive-Closure-II: theory Regular-Sets.Relation_Interpretation
14:34:11 Timing Discrete_Summation (2 threads, 9.476s elapsed time, 9.475s cpu time, 0.186s GC time, factor 1.00)
14:34:11 Finished Discrete_Summation (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.96)
14:34:12 Timing GoedelGod (2 threads, 7.305s elapsed time, 6.421s cpu time, 0.143s GC time, factor 0.88)
14:34:12 Finished GoedelGod (0:00:09 elapsed time, 0:00:07 cpu time, factor 0.86)
14:34:12 Timing ArrowImpossibilityGS (2 threads, 15.645s elapsed time, 15.603s cpu time, 0.980s GC time, factor 1.00)
14:34:12 Finished ArrowImpossibilityGS (0:00:17 elapsed time, 0:00:17 cpu time, factor 0.98)
14:34:12 Timing LP_Duality (2 threads, 11.425s elapsed time, 11.347s cpu time, 0.205s GC time, factor 0.99)
14:34:12 Finished LP_Duality (0:00:15 elapsed time, 0:00:15 cpu time, factor 0.97)
14:34:13 Binomial-Heaps: theory Binomial-Heaps.Test
14:34:14 Timing Prefix_Free_Code_Combinators (2 threads, 9.099s elapsed time, 9.090s cpu time, 0.208s GC time, factor 1.00)
14:34:14 Finished Prefix_Free_Code_Combinators (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:34:14 Timing Partial_Function_MR (2 threads, 9.947s elapsed time, 9.935s cpu time, 0.964s GC time, factor 1.00)
14:34:14 Finished Partial_Function_MR (0:00:12 elapsed time, 0:00:11 cpu time, factor 0.96)
14:34:15 Timing Binomial-Heaps (6 threads, 22.256s elapsed time, 22.240s cpu time, 2.205s GC time, factor 1.00)
14:34:15 Finished Binomial-Heaps (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)
14:34:15 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
14:34:16 Timing Banach_Steinhaus (2 threads, 16.928s elapsed time, 16.824s cpu time, 0.413s GC time, factor 0.99)
14:34:16 Finished Banach_Steinhaus (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.97)
14:34:17 Transitive-Closure-II: theory Regular-Sets.Equivalence_Checking
14:34:18 Transitive-Closure-II: theory Regular-Sets.Regexp_Method
14:34:19 Timing Menger (2 threads, 20.310s elapsed time, 20.255s cpu time, 0.708s GC time, factor 1.00)
14:34:19 Finished Menger (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98)
14:34:19 Transitive-Closure-II: theory Transitive-Closure-II.RTrancl
14:34:26 Timing Transitive-Closure-II (2 threads, 26.506s elapsed time, 26.475s cpu time, 2.564s GC time, factor 1.00)
14:34:26 Finished Transitive-Closure-II (0:00:28 elapsed time, 0:00:28 cpu time, factor 0.99)
14:34:27 Timing Nullstellensatz (2 threads, 19.075s elapsed time, 18.898s cpu time, 0.685s GC time, factor 0.99)
14:34:27 Finished Nullstellensatz (0:00:23 elapsed time, 0:00:22 cpu time, factor 0.97)
14:34:27 Running FOL_Seq_Calc1 (on of1-proof+0-7) ...
14:34:27 Running SumSquares (on of1-proof+8-15) ...
14:34:28 Timing Skip_Lists (2 threads, 29.986s elapsed time, 29.983s cpu time, 0.653s GC time, factor 1.00)
14:34:28 Finished Skip_Lists (0:00:33 elapsed time, 0:00:32 cpu time, factor 0.99)
14:34:28 Running Falling_Factorial_Sum (on 10.195.8.49+1) ...
14:34:28 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
14:34:28 Running Fresh_Identifiers (on 10.195.8.49+4) ...
14:34:28 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
14:34:28 Running Lifting_Definition_Option (on 10.195.8.49+0) ...
14:34:28 Running Real_Power (on 10.195.8.49+2) ...
14:34:28 SumSquares: theory SumSquares.FourSquares
14:34:28 Running Source_Coding_Theorem (on 10.195.8.49+3) ...
14:34:28 SumSquares: theory SumSquares.TwoSquares
14:34:28 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
14:34:28 FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent2
14:34:29 Running Birkhoff_Finite_Distributive_Lattices (on of3.proof.cit.tum.de+2) ...
14:34:29 Running Boolos_Curious_Inference_Automated (on of3.proof.cit.tum.de+0) ...
14:34:29 Running Huffman (on of3.proof.cit.tum.de+3) ...
14:34:29 Running Weight_Balanced_Trees (on of3.proof.cit.tum.de+1) ...
14:34:30 Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
14:34:30 Real_Power: theory Real_Power.RatPower
14:34:30 Fresh_Identifiers: theory Fresh_Identifiers.Fresh
14:34:30 Boolos_Curious_Inference_Automated: theory Boolos_Curious_Inference_Automated.Boolos_Curious_Inference_Automated
14:34:30 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Plus
14:34:30 Huffman: theory Huffman.Huffman
14:34:30 Weight_Balanced_Trees: theory HOL-Data_Structures.Cmp
14:34:30 Running Buffons_Needle (on 10.195.8.29+2) ...
14:34:30 Running GenClock (on 10.195.8.29+1) ...
14:34:30 Weight_Balanced_Trees: theory HOL-Data_Structures.Less_False
14:34:30 Weight_Balanced_Trees: theory HOL-Library.Tree
14:34:30 Running Noninterference_Concurrent_Composition (on 10.195.8.29+3) ...
14:34:30 Weight_Balanced_Trees: theory HOL-Data_Structures.Sorted_Less
14:34:30 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Order
14:34:30 Running ShortestPath (on 10.195.8.29+4) ...
14:34:30 Running Topology (on 10.195.8.29+0) ...
14:34:30 Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
14:34:30 Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
14:34:30 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
14:34:30 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
14:34:30 Weight_Balanced_Trees: theory HOL-Data_Structures.List_Ins_Del
14:34:30 Timing SumSquares (8 threads, 2.073s elapsed time, 8.316s cpu time, 0.255s GC time, factor 4.01)
14:34:30 Finished SumSquares (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.71)
14:34:31 Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
14:34:31 Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Finite_Lattice
14:34:31 Timing FOL_Seq_Calc1 (8 threads, 2.557s elapsed time, 8.709s cpu time, 0.274s GC time, factor 3.41)
14:34:31 Finished FOL_Seq_Calc1 (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.56)
14:34:32 Real_Power: theory Real_Power.RealPower
14:34:32 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
14:34:32 GenClock: theory GenClock.GenClock
14:34:32 Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
14:34:32 Falling_Factorial_Sum: theory Discrete_Summation.Factorials
14:34:32 Weight_Balanced_Trees: theory HOL-Data_Structures.Set_Specs
14:34:33 Running Imperative_Insertion_Sort (on 10.195.8.32+0) ...
14:34:33 Running Integration (on 10.195.8.32+3) ...
14:34:33 ShortestPath: theory ShortestPath.ShortestPath
14:34:33 Buffons_Needle: theory Buffons_Needle.Buffons_Needle
14:34:34 Topology: theory Topology.Topology
14:34:34 Topology: theory Lazy-Lists-II.LList2
14:34:34 Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
14:34:34 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
14:34:34 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
14:34:34 Running Irrationals_From_THEBOOK (on 10.195.8.32+1) ...
14:34:34 Running Van_der_Waerden (on 10.195.8.32+4) ...
14:34:34 Birkhoff_Finite_Distributive_Lattices: theory Birkhoff_Finite_Distributive_Lattices.Birkhoff_Finite_Distributive_Lattices
14:34:34 Real_Power: theory Real_Power.Log
14:34:34 Timing Lifting_Definition_Option (2 threads, 3.527s elapsed time, 3.494s cpu time, 0.102s GC time, factor 0.99)
14:34:34 Finished Lifting_Definition_Option (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.92)
14:34:34 Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
14:34:35 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
14:34:35 Running Arith_Prog_Rel_Primes (on 10.195.8.11+1) ...
14:34:35 Van_der_Waerden: theory HOL-Library.FuncSet
14:34:35 Van_der_Waerden: theory Van_der_Waerden.Digits
14:34:36 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
14:34:36 Weight_Balanced_Trees: theory HOL-Data_Structures.Tree2
14:34:36 Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees_log
14:34:36 Integration: theory Integration.MonConv
14:34:36 Integration: theory Integration.Sigma_Algebra
14:34:36 Running Dynamic_Tables (on 10.195.8.11+3) ...
14:34:36 Running List-Index (on 10.195.8.11+4) ...
14:34:36 Running Secondary_Sylow (on 10.195.8.11+2) ...
14:34:36 ShortestPath: theory ShortestPath.ShortestPathNeg
14:34:37 Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
14:34:37 Integration: theory Integration.Measure
14:34:37 Weight_Balanced_Trees: theory HOL-Data_Structures.Isin2
14:34:37 Timing Boolos_Curious_Inference_Automated (6 threads, 6.761s elapsed time, 6.761s cpu time, 1.250s GC time, factor 1.00)
14:34:37 Finished Boolos_Curious_Inference_Automated (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.96)
14:34:38 List-Index: theory List-Index.List_Index
14:34:38 Weight_Balanced_Trees: theory Weight_Balanced_Trees.Weight_Balanced_Trees
14:34:38 Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
14:34:38 Running Card_Partitions (on 10.195.6.179+3) ...
14:34:38 Running Liouville_Numbers (on 10.195.6.179+4) ...
14:34:38 Running Mason_Stothers (on 10.195.6.179+0) ...
14:34:38 Running WorkerWrapper (on 10.195.6.179+1) ...
14:34:38 Timing Fresh_Identifiers (2 threads, 7.407s elapsed time, 7.363s cpu time, 0.166s GC time, factor 0.99)
14:34:38 Finished Fresh_Identifiers (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.96)
14:34:39 Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
14:34:39 Integration: theory Integration.RealRandVar
14:34:39 Dynamic_Tables: theory Dynamic_Tables.Tables_real
14:34:39 Secondary_Sylow: theory Secondary_Sylow.GroupAction
14:34:40 Card_Partitions: theory HOL-Eisbach.Eisbach
14:34:40 Card_Partitions: theory HOL-Combinatorics.Stirling
14:34:40 WorkerWrapper: theory WorkerWrapper.Maybe
14:34:40 WorkerWrapper: theory WorkerWrapper.Nats
14:34:40 Topology: theory Topology.LList_Topology
14:34:40 Integration: theory Integration.Failure
14:34:41 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
14:34:41 Mason_Stothers: theory Mason_Stothers.Mason_Stothers
14:34:41 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
14:34:41 Timing Source_Coding_Theorem (2 threads, 8.290s elapsed time, 8.268s cpu time, 0.194s GC time, factor 1.00)
14:34:41 Finished Source_Coding_Theorem (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:34:41 Integration: theory Integration.Integral
14:34:41 Card_Partitions: theory HOL-Library.Adhoc_Overloading
14:34:41 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
14:34:41 Timing ShortestPath (2 threads, 7.341s elapsed time, 7.320s cpu time, 0.322s GC time, factor 1.00)
14:34:41 Finished ShortestPath (0:00:10 elapsed time, 0:00:09 cpu time, factor 0.96)
14:34:41 Secondary_Sylow: theory Secondary_Sylow.SndSylow
14:34:41 Card_Partitions: theory HOL-Library.Monad_Syntax
14:34:42 Dynamic_Tables: theory Dynamic_Tables.Tables_nat
14:34:42 Timing GenClock (2 threads, 9.337s elapsed time, 9.309s cpu time, 0.196s GC time, factor 1.00)
14:34:42 Finished GenClock (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.96)
14:34:42 Timing Birkhoff_Finite_Distributive_Lattices (6 threads, 11.230s elapsed time, 11.229s cpu time, 0.457s GC time, factor 1.00)
14:34:42 Finished Birkhoff_Finite_Distributive_Lattices (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
14:34:42 Card_Partitions: theory HOL-Library.FuncSet
14:34:43 Timing Falling_Factorial_Sum (2 threads, 11.491s elapsed time, 11.477s cpu time, 0.332s GC time, factor 1.00)
14:34:43 Finished Falling_Factorial_Sum (0:00:14 elapsed time, 0:00:13 cpu time, factor 0.97)
14:34:43 WorkerWrapper: theory WorkerWrapper.LList
14:34:44 Timing Huffman (6 threads, 13.092s elapsed time, 13.091s cpu time, 0.353s GC time, factor 1.00)
14:34:44 Finished Huffman (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.98)
14:34:44 Card_Partitions: theory HOL-Library.Disjoint_Sets
14:34:44 Timing Irrationals_From_THEBOOK (2 threads, 6.781s elapsed time, 6.762s cpu time, 0.113s GC time, factor 1.00)
14:34:44 Finished Irrationals_From_THEBOOK (0:00:10 elapsed time, 0:00:09 cpu time, factor 0.96)
14:34:45 Timing List-Index (2 threads, 6.486s elapsed time, 6.483s cpu time, 0.133s GC time, factor 1.00)
14:34:45 Finished List-Index (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.95)
14:34:45 Card_Partitions: theory Card_Partitions.Injectivity_Solver
14:34:45 Card_Partitions: theory Card_Partitions.Set_Partition
14:34:45 Timing Liouville_Numbers (2 threads, 4.162s elapsed time, 4.161s cpu time, 0.099s GC time, factor 1.00)
14:34:45 Finished Liouville_Numbers (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.95)
14:34:46 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
14:34:46 Timing Imperative_Insertion_Sort (2 threads, 10.722s elapsed time, 10.718s cpu time, 0.211s GC time, factor 1.00)
14:34:46 Finished Imperative_Insertion_Sort (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
14:34:46 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
14:34:46 WorkerWrapper: theory WorkerWrapper.CounterExample
14:34:46 Timing Buffons_Needle (2 threads, 12.372s elapsed time, 12.371s cpu time, 0.171s GC time, factor 1.00)
14:34:46 Finished Buffons_Needle (0:00:15 elapsed time, 0:00:15 cpu time, factor 0.97)
14:34:46 WorkerWrapper: theory WorkerWrapper.Last
14:34:46 Card_Partitions: theory Card_Partitions.Card_Partitions
14:34:47 WorkerWrapper: theory WorkerWrapper.Streams
14:34:47 Timing Mason_Stothers (2 threads, 6.232s elapsed time, 6.094s cpu time, 0.123s GC time, factor 0.98)
14:34:47 Finished Mason_Stothers (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.94)
14:34:47 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
14:34:48 WorkerWrapper: theory WorkerWrapper.Accumulator
14:34:49 WorkerWrapper: theory WorkerWrapper.Backtracking
14:34:49 Timing Arith_Prog_Rel_Primes (2 threads, 9.914s elapsed time, 9.886s cpu time, 0.266s GC time, factor 1.00)
14:34:49 Finished Arith_Prog_Rel_Primes (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
14:34:49 Timing Weight_Balanced_Trees (6 threads, 18.081s elapsed time, 18.072s cpu time, 1.562s GC time, factor 1.00)
14:34:49 Finished Weight_Balanced_Trees (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
14:34:49 WorkerWrapper: theory WorkerWrapper.Continuations
14:34:50 Timing Real_Power (2 threads, 19.787s elapsed time, 19.757s cpu time, 0.419s GC time, factor 1.00)
14:34:50 Finished Real_Power (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)
14:34:51 Timing Topology (2 threads, 16.677s elapsed time, 16.648s cpu time, 0.789s GC time, factor 1.00)
14:34:51 Finished Topology (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.98)
14:34:51 Timing Secondary_Sylow (2 threads, 11.218s elapsed time, 11.202s cpu time, 0.395s GC time, factor 1.00)
14:34:51 Finished Secondary_Sylow (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.97)
14:34:53 Timing Integration (2 threads, 16.087s elapsed time, 16.031s cpu time, 0.431s GC time, factor 1.00)
14:34:53 Finished Integration (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
14:34:53 WorkerWrapper: theory WorkerWrapper.Nub
14:34:53 Timing Dynamic_Tables (2 threads, 14.225s elapsed time, 14.149s cpu time, 0.451s GC time, factor 0.99)
14:34:53 Finished Dynamic_Tables (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.98)
14:34:54 WorkerWrapper: theory WorkerWrapper.UnboxedNats
14:34:55 Timing Van_der_Waerden (2 threads, 18.524s elapsed time, 18.474s cpu time, 0.396s GC time, factor 1.00)
14:34:55 Finished Van_der_Waerden (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.98)
14:34:57 Timing Noninterference_Concurrent_Composition (2 threads, 23.979s elapsed time, 23.940s cpu time, 0.550s GC time, factor 1.00)
14:34:57 Finished Noninterference_Concurrent_Composition (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.99)
14:35:02 Running MHComputation (on of1-proof+0-7) ...
14:35:02 Running Selection_Heap_Sort (on of1-proof+8-15) ...
14:35:02 Timing WorkerWrapper (2 threads, 21.699s elapsed time, 21.612s cpu time, 0.841s GC time, factor 1.00)
14:35:02 Finished WorkerWrapper (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)
14:35:02 MHComputation: theory MHComputation.MHComputation
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
14:35:03 Running DCR-ExecutionEquivalence (on 10.195.8.49+2) ...
14:35:03 Running Goodstein_Lambda (on 10.195.8.49+1) ...
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
14:35:03 Running Laws_of_Large_Numbers (on 10.195.8.49+3) ...
14:35:03 Running Lifting_the_Exponent (on 10.195.8.49+4) ...
14:35:03 Running VeriComp (on 10.195.8.49+0) ...
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
14:35:03 Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
14:35:04 Running GraphMarkingIBP (on of3.proof.cit.tum.de+0) ...
14:35:04 Running MonoBoolTranAlgebra (on of3.proof.cit.tum.de+2) ...
14:35:04 Running Noninterference_Inductive_Unwinding (on of3.proof.cit.tum.de+3) ...
14:35:04 Running Szemeredi_Regularity (on of3.proof.cit.tum.de+1) ...
14:35:04 DCR-ExecutionEquivalence: theory DCR-ExecutionEquivalence.DCRExecutionEquivalence
14:35:04 Timing MHComputation (8 threads, 1.764s elapsed time, 1.981s cpu time, 0.192s GC time, factor 1.12)
14:35:04 Finished MHComputation (0:00:02 elapsed time)
14:35:05 Timing Card_Partitions (2 threads, 24.751s elapsed time, 24.726s cpu time, 0.614s GC time, factor 1.00)
14:35:05 Finished Card_Partitions (0:00:26 elapsed time, 0:00:26 cpu time, factor 0.99)
14:35:05 Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
14:35:05 VeriComp: theory VeriComp.Behaviour
14:35:05 VeriComp: theory VeriComp.Transfer_Extras
14:35:05 MonoBoolTranAlgebra: theory LatticeProperties.Conj_Disj
14:35:05 GraphMarkingIBP: theory GraphMarkingIBP.Graph
14:35:05 MonoBoolTranAlgebra: theory LatticeProperties.WellFoundedTransitive
14:35:05 GraphMarkingIBP: theory LatticeProperties.Conj_Disj
14:35:05 GraphMarkingIBP: theory LatticeProperties.WellFoundedTransitive
14:35:05 VeriComp: theory VeriComp.Well_founded
14:35:05 Noninterference_Inductive_Unwinding: theory List_Interleaving.ListInterleaving
14:35:05 Noninterference_Inductive_Unwinding: theory Noninterference_CSP.CSPNoninterference
14:35:05 Running Card_Equiv_Relations (on 10.195.8.29+3) ...
14:35:05 Running Cotangent_PFD_Formula (on 10.195.8.29+1) ...
14:35:05 Running Involutions2Squares (on 10.195.8.29+2) ...
14:35:06 Running Sophomores_Dream (on 10.195.8.29+0) ...
14:35:06 Running Stuttering_Equivalence (on 10.195.8.29+4) ...
14:35:06 VeriComp: theory VeriComp.Inf
14:35:06 Timing Selection_Heap_Sort (8 threads, 2.718s elapsed time, 11.180s cpu time, 0.891s GC time, factor 4.11)
14:35:06 Finished Selection_Heap_Sort (0:00:04 elapsed time, 0:00:12 cpu time, factor 3.13)
14:35:07 MonoBoolTranAlgebra: theory LatticeProperties.Complete_Lattice_Prop
14:35:07 GraphMarkingIBP: theory LatticeProperties.Complete_Lattice_Prop
14:35:07 Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
14:35:07 VeriComp: theory VeriComp.Lifting_Simulation_To_Bisimulation
14:35:07 Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
14:35:07 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
14:35:07 GraphMarkingIBP: theory DataRefinementIBP.Preliminaries
14:35:07 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran
14:35:07 Running BinarySearchTree (on 10.195.8.32+2) ...
14:35:07 GraphMarkingIBP: theory DataRefinementIBP.Statements
14:35:07 Running FFT (on 10.195.8.32+4) ...
14:35:07 Running Fisher_Yates (on 10.195.8.32+3) ...
14:35:07 Running List_Interleaving (on 10.195.8.32+1) ...
14:35:07 Running Ptolemys_Theorem (on 10.195.8.32+0) ...
14:35:07 GraphMarkingIBP: theory DataRefinementIBP.Hoare
14:35:07 Involutions2Squares: theory Involutions2Squares.Involutions2Squares
14:35:08 GraphMarkingIBP: theory DataRefinementIBP.Diagram
14:35:08 Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
14:35:08 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Equiv_Relations
14:35:08 Running Abstract-Hoare-Logics (on 10.195.8.11+3) ...
14:35:08 Running Binary_Code_Imprimitive (on 10.195.8.11+2) ...
14:35:08 GraphMarkingIBP: theory DataRefinementIBP.DataRefinement
14:35:08 Running Compiling-Exceptions-Correctly (on 10.195.8.11+4) ...
14:35:08 Running Stewart_Apollonius (on 10.195.8.11+0) ...
14:35:08 Running VolpanoSmith (on 10.195.8.11+1) ...
14:35:09 Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
14:35:09 VeriComp: theory VeriComp.Semantics
14:35:09 Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
14:35:09 Sophomores_Dream: theory Sophomores_Dream.Sophomores_Dream
14:35:09 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
14:35:09 Cotangent_PFD_Formula: theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
14:35:09 GraphMarkingIBP: theory GraphMarkingIBP.SetMark
14:35:09 FFT: theory FFT.FFT
14:35:09 BinarySearchTree: theory BinarySearchTree.BinaryTree
14:35:09 List_Interleaving: theory List_Interleaving.ListInterleaving
14:35:09 BinarySearchTree: theory BinarySearchTree.BinaryTree_TacticStyle
14:35:09 Timing DCR-ExecutionEquivalence (2 threads, 3.645s elapsed time, 3.644s cpu time, 0.175s GC time, factor 1.00)
14:35:09 Finished DCR-ExecutionEquivalence (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:09 VeriComp: theory VeriComp.Language
14:35:10 Compiling-Exceptions-Correctly: theory Compiling-Exceptions-Correctly.Exceptions
14:35:10 VeriComp: theory VeriComp.Simulation
14:35:10 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Lang
14:35:10 Running Blue_Eyes (on 10.195.6.179+1) ...
14:35:10 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PLang
14:35:10 Running Implicational_Logic (on 10.195.6.179+4) ...
14:35:10 Running Lucas_Theorem (on 10.195.6.179+0) ...
14:35:10 Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
14:35:10 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Square_Interpretation
14:35:10 Running Transitive-Closure (on 10.195.6.179+2) ...
14:35:10 Binary_Code_Imprimitive: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
14:35:10 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
14:35:10 VolpanoSmith: theory VolpanoSmith.Semantics
14:35:10 Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
14:35:10 Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
14:35:10 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
14:35:11 Timing Laws_of_Large_Numbers (2 threads, 3.218s elapsed time, 3.217s cpu time, 0.099s GC time, factor 1.00)
14:35:11 Finished Laws_of_Large_Numbers (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.95)
14:35:11 Stewart_Apollonius: theory Triangle.Angles
14:35:11 VeriComp: theory VeriComp.Compiler
14:35:11 Timing Card_Equiv_Relations (2 threads, 2.432s elapsed time, 2.430s cpu time, 0.041s GC time, factor 1.00)
14:35:11 Finished Card_Equiv_Relations (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.93)
14:35:11 Blue_Eyes: theory Blue_Eyes.Blue_Eyes
14:35:11 Implicational_Logic: theory Implicational_Logic.Implicational_Logic
14:35:11 Implicational_Logic: theory Implicational_Logic.Implicational_Logic_Appendix
14:35:11 GraphMarkingIBP: theory GraphMarkingIBP.StackMark
14:35:12 Timing Lifting_the_Exponent (2 threads, 4.556s elapsed time, 4.554s cpu time, 0.114s GC time, factor 1.00)
14:35:12 Finished Lifting_the_Exponent (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.95)
14:35:12 VeriComp: theory VeriComp.Fixpoint
14:35:12 Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem
14:35:12 Stewart_Apollonius: theory Triangle.Triangle
14:35:12 Transitive-Closure: theory Matrix.Utility
14:35:12 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
14:35:13 BinarySearchTree: theory BinarySearchTree.BinaryTree_Map
14:35:13 GraphMarkingIBP: theory GraphMarkingIBP.LinkMark
14:35:13 Timing FFT (2 threads, 3.362s elapsed time, 3.359s cpu time, 0.062s GC time, factor 1.00)
14:35:13 Finished FFT (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.94)
14:35:13 Timing Sophomores_Dream (2 threads, 3.754s elapsed time, 3.753s cpu time, 0.086s GC time, factor 1.00)
14:35:13 Finished Sophomores_Dream (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.95)
14:35:13 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Hoare
14:35:13 Timing Involutions2Squares (2 threads, 5.255s elapsed time, 5.193s cpu time, 0.091s GC time, factor 0.99)
14:35:13 Finished Involutions2Squares (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.94)
14:35:13 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Code_Imprimitive
14:35:13 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Termi
14:35:13 Timing Goodstein_Lambda (2 threads, 7.762s elapsed time, 7.751s cpu time, 0.242s GC time, factor 1.00)
14:35:13 Finished Goodstein_Lambda (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.96)
14:35:13 Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
14:35:14 Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
14:35:14 Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
14:35:14 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Assertion_Algebra
14:35:14 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
14:35:14 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.HoareTotal
14:35:14 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoare
14:35:14 Timing Ptolemys_Theorem (2 threads, 3.438s elapsed time, 3.436s cpu time, 0.064s GC time, factor 1.00)
14:35:14 Finished Ptolemys_Theorem (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.94)
14:35:14 Noninterference_Inductive_Unwinding: theory Noninterference_Inductive_Unwinding.InductiveUnwinding
14:35:14 MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Statements
14:35:14 Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
14:35:15 Timing Blue_Eyes (2 threads, 2.913s elapsed time, 2.913s cpu time, 0.084s GC time, factor 1.00)
14:35:15 Finished Blue_Eyes (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.93)
14:35:15 Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Imprimitive_Decision
14:35:15 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PTermi
14:35:15 GraphMarkingIBP: theory GraphMarkingIBP.DSWMark
14:35:15 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsLang
14:35:15 Timing Cotangent_PFD_Formula (2 threads, 5.981s elapsed time, 5.980s cpu time, 0.130s GC time, factor 1.00)
14:35:15 Finished Cotangent_PFD_Formula (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:15 Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
14:35:16 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoareTotal
14:35:16 Timing MonoBoolTranAlgebra (6 threads, 10.226s elapsed time, 10.226s cpu time, 0.363s GC time, factor 1.00)
14:35:16 Finished MonoBoolTranAlgebra (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:35:16 Timing Szemeredi_Regularity (6 threads, 9.105s elapsed time, 9.095s cpu time, 0.250s GC time, factor 1.00)
14:35:16 Finished Szemeredi_Regularity (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
14:35:17 Timing List_Interleaving (2 threads, 7.109s elapsed time, 7.069s cpu time, 0.290s GC time, factor 0.99)
14:35:17 Finished List_Interleaving (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:17 Timing Compiling-Exceptions-Correctly (2 threads, 6.782s elapsed time, 6.740s cpu time, 0.379s GC time, factor 0.99)
14:35:17 Finished Compiling-Exceptions-Correctly (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:17 VolpanoSmith: theory VolpanoSmith.secTypes
14:35:17 Timing Noninterference_Inductive_Unwinding (6 threads, 11.258s elapsed time, 11.258s cpu time, 0.520s GC time, factor 1.00)
14:35:18 Finished Noninterference_Inductive_Unwinding (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
14:35:18 Timing VeriComp (2 threads, 11.880s elapsed time, 11.840s cpu time, 0.454s GC time, factor 1.00)
14:35:18 Finished VeriComp (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.97)
14:35:18 Timing Lucas_Theorem (2 threads, 5.175s elapsed time, 5.159s cpu time, 0.091s GC time, factor 1.00)
14:35:18 Finished Lucas_Theorem (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.95)
14:35:18 Timing BinarySearchTree (2 threads, 8.517s elapsed time, 8.485s cpu time, 0.370s GC time, factor 1.00)
14:35:18 Finished BinarySearchTree (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.96)
14:35:18 Timing Implicational_Logic (2 threads, 6.241s elapsed time, 6.239s cpu time, 0.280s GC time, factor 1.00)
14:35:18 Finished Implicational_Logic (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.96)
14:35:18 Timing Fisher_Yates (2 threads, 7.201s elapsed time, 7.200s cpu time, 0.185s GC time, factor 1.00)
14:35:18 Finished Fisher_Yates (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.97)
14:35:18 Timing Stuttering_Equivalence (2 threads, 9.106s elapsed time, 9.099s cpu time, 0.240s GC time, factor 1.00)
14:35:18 Finished Stuttering_Equivalence (0:00:12 elapsed time, 0:00:11 cpu time, factor 0.97)
14:35:19 VolpanoSmith: theory VolpanoSmith.Execute
14:35:20 Timing Stewart_Apollonius (2 threads, 8.163s elapsed time, 7.998s cpu time, 0.227s GC time, factor 0.98)
14:35:20 Finished Stewart_Apollonius (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.95)
14:35:20 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoare
14:35:21 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsTermi
14:35:21 Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoareTotal
14:35:22 Timing Transitive-Closure (2 threads, 9.060s elapsed time, 9.039s cpu time, 0.309s GC time, factor 1.00)
14:35:22 Finished Transitive-Closure (0:00:12 elapsed time, 0:00:11 cpu time, factor 0.97)
14:35:26 Timing GraphMarkingIBP (6 threads, 20.065s elapsed time, 20.064s cpu time, 0.385s GC time, factor 1.00)
14:35:26 Finished GraphMarkingIBP (0:00:21 elapsed time, 0:00:20 cpu time, factor 0.98)
14:35:27 Timing VolpanoSmith (2 threads, 16.828s elapsed time, 16.804s cpu time, 0.738s GC time, factor 1.00)
14:35:27 Finished VolpanoSmith (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
14:35:29 Timing Binary_Code_Imprimitive (2 threads, 18.342s elapsed time, 18.334s cpu time, 0.557s GC time, factor 1.00)
14:35:29 Finished Binary_Code_Imprimitive (0:00:20 elapsed time, 0:00:19 cpu time, factor 0.98)
14:35:33 Running ClockSynchInst (on of1-proof+0-7) ...
14:35:33 Running Tail_Recursive_Functions (on of1-proof+8-15) ...
14:35:34 ClockSynchInst: theory ClockSynchInst.ICAInstance
14:35:34 ClockSynchInst: theory ClockSynchInst.LynchInstance
14:35:34 Running DataRefinementIBP (on of2.proof.cit.tum.de+3) ...
14:35:34 Running Descartes_Sign_Rule (on of2.proof.cit.tum.de+1) ...
14:35:34 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
14:35:34 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
14:35:34 Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
14:35:35 Running Stream-Fusion (on of2.proof.cit.tum.de+0) ...
14:35:35 Running Zeckendorf (on of2.proof.cit.tum.de+2) ...
14:35:35 Timing ClockSynchInst (8 threads, 0.800s elapsed time, 3.923s cpu time, 0.112s GC time, factor 4.90)
14:35:35 Finished ClockSynchInst (0:00:01 elapsed time, 0:00:04 cpu time)
14:35:36 DataRefinementIBP: theory LatticeProperties.Conj_Disj
14:35:36 DataRefinementIBP: theory LatticeProperties.WellFoundedTransitive
14:35:36 Running Boolos_Curious_Inference (on 10.195.8.49+2) ...
14:35:36 Running Example-Submission (on 10.195.8.49+4) ...
14:35:36 Stream-Fusion: theory HOLCF-Library.Int_Discrete
14:35:36 Running Recursion-Addition (on 10.195.8.49+1) ...
14:35:36 Running Sauer_Shelah_Lemma (on 10.195.8.49+0) ...
14:35:36 Running Weighted_Arithmetic_Geometric_Mean (on 10.195.8.49+3) ...
14:35:36 Stream-Fusion: theory Stream-Fusion.LazyList
14:35:36 Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
14:35:37 Zeckendorf: theory Zeckendorf.Zeckendorf
14:35:37 DataRefinementIBP: theory LatticeProperties.Complete_Lattice_Prop
14:35:37 Recursion-Addition: theory Recursion-Addition.recursion
14:35:37 Running Chord_Segments (on of3.proof.cit.tum.de+3) ...
14:35:37 Running Concurrent_Ref_Alg (on of3.proof.cit.tum.de+1) ...
14:35:37 Running Matroids (on of3.proof.cit.tum.de+2) ...
14:35:37 Stream-Fusion: theory Stream-Fusion.Stream
14:35:37 Timing Tail_Recursive_Functions (8 threads, 1.917s elapsed time, 5.101s cpu time, 0.686s GC time, factor 2.66)
14:35:37 Finished Tail_Recursive_Functions (0:00:03 elapsed time, 0:00:06 cpu time, factor 2.04)
14:35:38 DataRefinementIBP: theory DataRefinementIBP.Preliminaries
14:35:38 DataRefinementIBP: theory DataRefinementIBP.Statements
14:35:38 DataRefinementIBP: theory DataRefinementIBP.Hoare
14:35:38 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Refinement_Lattice
14:35:38 Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo1
14:35:38 Example-Submission: theory Example-Submission.Submission
14:35:38 Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo2
14:35:38 DataRefinementIBP: theory DataRefinementIBP.Diagram
14:35:38 Weighted_Arithmetic_Geometric_Mean: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
14:35:38 Running CofGroups (on 10.195.8.29+0) ...
14:35:38 Running Monad_Normalisation (on 10.195.8.29+4) ...
14:35:38 Matroids: theory Matroids.Indep_System
14:35:38 Running Skew_Heap (on 10.195.8.29+1) ...
14:35:38 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Binomial_Lemmas
14:35:38 Stream-Fusion: theory Stream-Fusion.StreamFusion
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunction
14:35:39 Timing Abstract-Hoare-Logics (2 threads, 27.406s elapsed time, 27.403s cpu time, 2.189s GC time, factor 1.00)
14:35:39 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Card_Lemmas
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Galois_Connections
14:35:39 Finished Abstract-Hoare-Logics (0:00:29 elapsed time, 0:00:29 cpu time, factor 0.99)
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Infimum_Nat
14:35:39 Running Stalnaker_Logic (on 10.195.8.29+3) ...
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Parallel
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Sequential
14:35:39 Running Szpilrajn (on 10.195.8.29+2) ...
14:35:39 DataRefinementIBP: theory DataRefinementIBP.DataRefinement
14:35:39 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Shattering
14:35:39 Chord_Segments: theory Triangle.Angles
14:35:39 Timing Example-Submission (2 threads, 0.359s elapsed time, 0.335s cpu time, 0.000s GC time, factor 0.93)
14:35:39 Finished Example-Submission (0:00:02 elapsed time)
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.CRA
14:35:39 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Sequential
14:35:39 Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Sauer_Shelah_Lemma
14:35:40 Running AnselmGod (on 10.195.8.32+2) ...
14:35:40 Running Gray_Codes (on 10.195.8.32+0) ...
14:35:40 Running Max-Card-Matching (on 10.195.8.32+3) ...
14:35:40 Running Perfect-Number-Thm (on 10.195.8.32+4) ...
14:35:40 Chord_Segments: theory Triangle.Triangle
14:35:40 CofGroups: theory HOL-Library.Nat_Bijection
14:35:40 Timing Boolos_Curious_Inference (2 threads, 1.508s elapsed time, 1.481s cpu time, 0.064s GC time, factor 0.98)
14:35:40 Matroids: theory Matroids.Matroid
14:35:40 Finished Boolos_Curious_Inference (0:00:03 elapsed time)
14:35:40 Szpilrajn: theory Szpilrajn.Szpilrajn
14:35:40 Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
14:35:41 Timing Recursion-Addition (2 threads, 2.763s elapsed time, 2.725s cpu time, 0.058s GC time, factor 0.99)
14:35:41 Finished Recursion-Addition (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.90)
14:35:41 Running Surprise_Paradox (on 10.195.8.32+1) ...
14:35:41 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Iteration
14:35:41 Timing DataRefinementIBP (6 threads, 4.296s elapsed time, 4.296s cpu time, 0.105s GC time, factor 1.00)
14:35:41 Finished DataRefinementIBP (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.94)
14:35:41 Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
14:35:41 Skew_Heap: theory HOL-Data_Structures.Heaps
14:35:41 AnselmGod: theory AnselmGod.AnselmGod
14:35:41 Gray_Codes: theory Gray_Codes.Encoding_Nat
14:35:41 Timing Descartes_Sign_Rule (6 threads, 4.185s elapsed time, 4.185s cpu time, 0.079s GC time, factor 1.00)
14:35:41 Finished Descartes_Sign_Rule (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.94)
14:35:41 Max-Card-Matching: theory Max-Card-Matching.Matching
14:35:41 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
14:35:41 CofGroups: theory CofGroups.CofGroups
14:35:42 Running Card_Number_Partitions (on 10.195.8.11+0) ...
14:35:42 Running Stellar_Quorums (on 10.195.8.11+4) ...
14:35:42 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Iteration
14:35:42 Timing Weighted_Arithmetic_Geometric_Mean (2 threads, 3.125s elapsed time, 3.081s cpu time, 0.061s GC time, factor 0.99)
14:35:42 Finished Weighted_Arithmetic_Geometric_Mean (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.92)
14:35:42 Skew_Heap: theory Skew_Heap.Skew_Heap
14:35:42 Chord_Segments: theory Chord_Segments.Chord_Segments
14:35:42 Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
14:35:43 Running Ackermanns_not_PR (on 10.195.6.179+3) ...
14:35:43 Gray_Codes: theory Gray_Codes.Code_Word_Dist
14:35:43 Timing Stream-Fusion (6 threads, 5.973s elapsed time, 5.973s cpu time, 0.267s GC time, factor 1.00)
14:35:43 Finished Stream-Fusion (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.96)
14:35:43 Running Combinatorics_Words_Graph_Lemma (on 10.195.6.179+2) ...
14:35:43 Running Lazy_Case (on 10.195.6.179+0) ...
14:35:43 Running Marriage (on 10.195.6.179+1) ...
14:35:43 Running Sunflowers (on 10.195.6.179+4) ...
14:35:43 Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Rely_Quotient
14:35:43 Timing Sauer_Shelah_Lemma (2 threads, 4.029s elapsed time, 3.970s cpu time, 0.076s GC time, factor 0.99)
14:35:43 Finished Sauer_Shelah_Lemma (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.91)
14:35:43 Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
14:35:43 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
14:35:44 Timing Chord_Segments (6 threads, 4.165s elapsed time, 4.165s cpu time, 0.132s GC time, factor 1.00)
14:35:44 Finished Chord_Segments (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.94)
14:35:44 Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
14:35:44 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
14:35:44 Gray_Codes: theory Gray_Codes.Non_Boolean_Gray
14:35:44 Timing Monad_Normalisation (2 threads, 2.414s elapsed time, 2.414s cpu time, 0.077s GC time, factor 1.00)
14:35:44 Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:44 Ackermanns_not_PR: theory Ackermanns_not_PR.Primrec
14:35:44 Timing Zeckendorf (6 threads, 6.844s elapsed time, 6.844s cpu time, 0.128s GC time, factor 1.00)
14:35:44 Finished Zeckendorf (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:44 Marriage: theory Marriage.Marriage
14:35:44 Lazy_Case: theory Lazy_Case.Lazy_Case
14:35:44 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
14:35:44 Timing Skew_Heap (2 threads, 3.190s elapsed time, 3.133s cpu time, 0.141s GC time, factor 0.98)
14:35:44 Finished Skew_Heap (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.92)
14:35:45 Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
14:35:45 Sunflowers: theory HOL-Library.FuncSet
14:35:45 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
14:35:45 Timing CofGroups (2 threads, 4.196s elapsed time, 4.192s cpu time, 0.107s GC time, factor 1.00)
14:35:45 Finished CofGroups (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:45 Lazy_Case: theory Lazy_Case.Test_Lazy_Case
14:35:45 Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
14:35:46 Timing AnselmGod (2 threads, 4.090s elapsed time, 3.240s cpu time, 0.072s GC time, factor 0.79)
14:35:46 Finished AnselmGod (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.80)
14:35:46 Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
14:35:46 Timing Max-Card-Matching (2 threads, 3.984s elapsed time, 3.908s cpu time, 0.063s GC time, factor 0.98)
14:35:46 Finished Max-Card-Matching (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:46 Timing Concurrent_Ref_Alg (6 threads, 7.705s elapsed time, 7.702s cpu time, 0.518s GC time, factor 1.00)
14:35:46 Finished Concurrent_Ref_Alg (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:47 Timing Matroids (6 threads, 7.954s elapsed time, 7.954s cpu time, 0.192s GC time, factor 1.00)
14:35:47 Finished Matroids (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:47 Sunflowers: theory Sunflowers.Sunflower
14:35:47 Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
14:35:47 Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
14:35:48 Timing Surprise_Paradox (2 threads, 3.974s elapsed time, 3.972s cpu time, 0.164s GC time, factor 1.00)
14:35:48 Finished Surprise_Paradox (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.95)
14:35:48 Timing Szpilrajn (2 threads, 7.097s elapsed time, 7.079s cpu time, 0.153s GC time, factor 1.00)
14:35:48 Finished Szpilrajn (0:00:08 elapsed time, 0:00:08 cpu time, factor 0.96)
14:35:48 Timing Stalnaker_Logic (2 threads, 7.255s elapsed time, 6.936s cpu time, 0.146s GC time, factor 0.96)
14:35:48 Finished Stalnaker_Logic (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.92)
14:35:48 Timing Perfect-Number-Thm (2 threads, 4.364s elapsed time, 4.361s cpu time, 0.068s GC time, factor 1.00)
14:35:48 Finished Perfect-Number-Thm (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.93)
14:35:49 Timing Combinatorics_Words_Graph_Lemma (2 threads, 3.652s elapsed time, 3.633s cpu time, 0.098s GC time, factor 0.99)
14:35:49 Finished Combinatorics_Words_Graph_Lemma (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:49 Timing Ackermanns_not_PR (2 threads, 3.962s elapsed time, 3.918s cpu time, 0.097s GC time, factor 0.99)
14:35:49 Finished Ackermanns_not_PR (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.93)
14:35:49 Timing Marriage (2 threads, 4.563s elapsed time, 4.532s cpu time, 0.081s GC time, factor 0.99)
14:35:49 Finished Marriage (0:00:06 elapsed time, 0:00:06 cpu time, factor 0.94)
14:35:51 Timing Lazy_Case (2 threads, 5.710s elapsed time, 5.667s cpu time, 0.332s GC time, factor 0.99)
14:35:51 Finished Lazy_Case (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.94)
14:35:52 Timing Gray_Codes (2 threads, 10.178s elapsed time, 10.157s cpu time, 0.273s GC time, factor 1.00)
14:35:52 Finished Gray_Codes (0:00:12 elapsed time, 0:00:11 cpu time, factor 0.96)
14:35:55 Timing Card_Number_Partitions (2 threads, 10.146s elapsed time, 10.146s cpu time, 0.207s GC time, factor 1.00)
14:35:55 Finished Card_Number_Partitions (0:00:13 elapsed time, 0:00:12 cpu time, factor 0.97)
14:35:56 Timing Sunflowers (2 threads, 11.385s elapsed time, 11.350s cpu time, 0.227s GC time, factor 1.00)
14:35:56 Finished Sunflowers (0:00:13 elapsed time, 0:00:12 cpu time, factor 0.97)
14:36:01 Timing Stellar_Quorums (2 threads, 16.779s elapsed time, 16.689s cpu time, 0.552s GC time, factor 0.99)
14:36:01 Finished Stellar_Quorums (0:00:18 elapsed time, 0:00:18 cpu time, factor 0.98)
14:36:06 Running Cartan_FP (on of1-proof+0-7) ...
14:36:06 Running Triangle (on of1-proof+8-15) ...
14:36:07 Triangle: theory Triangle.Angles
14:36:07 Building CZH_Foundations (on of4.proof.cit.tum.de+0-7) ...
14:36:07 Cartan_FP: theory Cartan_FP.Cartan
14:36:07 Triangle: theory Triangle.Triangle
14:36:08 Building Echelon_Form (on of4.proof.cit.tum.de+8-15) ...
14:36:08 Timing Cartan_FP (8 threads, 0.730s elapsed time, 2.586s cpu time, 0.081s GC time, factor 3.54)
14:36:08 Finished Cartan_FP (0:00:02 elapsed time, 0:00:03 cpu time)
14:36:09 CZH_Foundations: theory CZH_Foundations.CZH_Sets_MIF
14:36:09 CZH_Foundations: theory CZH_Foundations.CZH_Utilities
14:36:09 Running Gauss-Jordan-Elim-Fun (on of2.proof.cit.tum.de+1) ...
14:36:09 CZH_Foundations: theory HOL-Eisbach.Eisbach
14:36:09 Running Mereology (on of2.proof.cit.tum.de+0) ...
14:36:09 CZH_Foundations: theory Conditional_Simplification.CS_Tools
14:36:09 CZH_Foundations: theory HOL-Library.Rewrite
14:36:09 CZH_Foundations: theory Intro_Dest_Elim.IHOL_IDE
14:36:09 Running TortoiseHare (on of2.proof.cit.tum.de+2) ...
14:36:09 CZH_Foundations: theory CZH_Foundations.CZH_Introduction
14:36:09 CZH_Foundations: theory Conditional_Simplification.IHOL_CS
14:36:09 Running Tree_Decomposition (on of2.proof.cit.tum.de+3) ...
14:36:09 Timing Triangle (8 threads, 1.345s elapsed time, 2.833s cpu time, 0.109s GC time, factor 2.11)
14:36:09 Finished Triangle (0:00:02 elapsed time, 0:00:04 cpu time)
14:36:10 Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field
14:36:10 Echelon_Form: theory HOL-Library.Code_Target_Int
14:36:10 Echelon_Form: theory HOL-Library.Code_Abstract_Nat
14:36:10 Echelon_Form: theory HOL-Library.Function_Algebras
14:36:10 Echelon_Form: theory HOL-Library.IArray
14:36:10 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Introduction
14:36:10 Echelon_Form: theory HOL-Library.More_List
14:36:10 Echelon_Form: theory HOL-Library.Code_Target_Nat
14:36:10 Echelon_Form: theory HOL-Library.Code_Cardinality
14:36:10 Echelon_Form: theory HOL-Library.Z2
14:36:10 Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
14:36:10 Echelon_Form: theory HOL-Library.Code_Target_Numeral
14:36:10 Echelon_Form: theory HOL-Computational_Algebra.Polynomial
14:36:10 Echelon_Form: theory Gauss_Jordan.Code_Set
14:36:10 Echelon_Form: theory Cayley_Hamilton.Square_Matrix
14:36:10 Echelon_Form: theory Gauss_Jordan.Code_Z2
14:36:10 Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
14:36:10 Echelon_Form: theory Gauss_Jordan.IArray_Addenda
14:36:10 Mereology: theory Mereology.PM
14:36:10 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Sets
14:36:10 CZH_Foundations: theory CZH_Foundations.HOL_CContinuum
14:36:10 Tree_Decomposition: theory Tree_Decomposition.Graph
14:36:10 Gauss-Jordan-Elim-Fun: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
14:36:10 Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
14:36:10 Mereology: theory Mereology.M
14:36:10 Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
14:36:11 TortoiseHare: theory TortoiseHare.Basis
14:36:11 Mereology: theory Mereology.CM
14:36:11 Mereology: theory Mereology.MM
14:36:11 Running Lehmer (on of3.proof.cit.tum.de+2) ...
14:36:11 CZH_Foundations: theory CZH_Foundations.CZH_Sets_BRelations
14:36:11 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Nat
14:36:11 Running Lorenz_C1 (on of3.proof.cit.tum.de+0) ...
14:36:11 Running Minkowskis_Theorem (on of3.proof.cit.tum.de+3) ...
14:36:11 Running Open_Induction (on of3.proof.cit.tum.de+1) ...
14:36:11 Mereology: theory Mereology.EM
14:36:11 TortoiseHare: theory TortoiseHare.Brent
14:36:11 TortoiseHare: theory TortoiseHare.TortoiseHare
14:36:12 Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
14:36:12 Mereology: theory Mereology.CEM
14:36:12 Mereology: theory Mereology.GM
14:36:12 Open_Induction: theory Open_Induction.Restricted_Predicates
14:36:12 Mereology: theory Mereology.GMM
14:36:13 CZH_Foundations: theory CZH_Foundations.CZH_Sets_IF
14:36:13 Lehmer: theory Lehmer.Lehmer
14:36:13 Echelon_Form: theory Gauss_Jordan.Code_Matrix
14:36:13 Echelon_Form: theory Gauss_Jordan.Rref
14:36:13 Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
14:36:13 Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
14:36:13 Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
14:36:13 Tree_Decomposition: theory Tree_Decomposition.Tree
14:36:13 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Equipollence
14:36:13 Echelon_Form: theory Gauss_Jordan.Rank
14:36:13 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Cardinality
14:36:13 Echelon_Form: theory Gauss_Jordan.Elementary_Operations
14:36:13 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Ordinals
14:36:13 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FSequences
14:36:13 Mereology: theory Mereology.GEM
14:36:14 Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
14:36:14 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
14:36:14 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
14:36:14 Open_Induction: theory Open_Induction.Open_Induction
14:36:14 Running Conditional_Simplification (on 10.195.8.11+3) ...
14:36:14 Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
14:36:14 Timing Gauss-Jordan-Elim-Fun (6 threads, 3.230s elapsed time, 3.221s cpu time, 0.072s GC time, factor 1.00)
14:36:14 Running Depth-First-Search (on 10.195.8.11+0) ...
14:36:14 Finished Gauss-Jordan-Elim-Fun (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.91)
14:36:14 Running FunWithFunctions (on 10.195.8.11+1) ...
14:36:14 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FBRelations
14:36:14 Running RIPEMD-160-SPARK (on 10.195.8.11+2) ...
14:36:15 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
14:36:15 Echelon_Form: theory Gauss_Jordan.Linear_Maps
14:36:15 Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
14:36:15 Timing Lehmer (6 threads, 1.831s elapsed time, 1.831s cpu time, 0.030s GC time, factor 1.00)
14:36:15 Finished Lehmer (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.91)
14:36:15 Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
14:36:15 Timing Mereology (6 threads, 4.578s elapsed time, 4.573s cpu time, 0.271s GC time, factor 1.00)
14:36:15 Finished Mereology (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.94)
14:36:15 Timing Lorenz_C1 (6 threads, 1.152s elapsed time, 1.152s cpu time, 0.019s GC time, factor 1.00)
14:36:15 Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.92)
14:36:15 Conditional_Simplification: theory Conditional_Simplification.CS_Tools
14:36:15 CZH_Foundations: theory CZH_Foundations.CZH_Sets_NOP
14:36:15 CZH_Foundations: theory CZH_Foundations.CZH_Sets_VNHS
14:36:15 Depth-First-Search: theory Depth-First-Search.DFS
14:36:15 Conditional_Simplification: theory HOL-Library.LaTeXsugar
14:36:15 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
14:36:15 Timing Minkowskis_Theorem (6 threads, 2.277s elapsed time, 2.277s cpu time, 0.055s GC time, factor 1.00)
14:36:15 Finished Minkowskis_Theorem (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.92)
14:36:16 Conditional_Simplification: theory Conditional_Simplification.IHOL_CS
14:36:16 Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
14:36:16 Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
14:36:16 Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
14:36:16 Echelon_Form: theory Gauss_Jordan.Determinants2
14:36:16 FunWithFunctions: theory FunWithFunctions.FunWithFunctions
14:36:16 Timing Open_Induction (6 threads, 3.303s elapsed time, 3.297s cpu time, 0.097s GC time, factor 1.00)
14:36:16 Finished Open_Induction (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.92)
14:36:16 Echelon_Form: theory Echelon_Form.Rings2
14:36:16 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
14:36:16 Echelon_Form: theory Gauss_Jordan.Inverse
14:36:16 Echelon_Form: theory Gauss_Jordan.System_Of_Equations
14:36:16 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
14:36:16 Conditional_Simplification: theory Conditional_Simplification.Reference_Prerequisites
14:36:16 CZH_Foundations: theory CZH_Foundations.CZH_DG_Introduction
14:36:16 CZH_Foundations: theory CZH_Foundations.CZH_Sets_ZQR
14:36:16 Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
14:36:16 Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
14:36:16 Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
14:36:16 Conditional_Simplification: theory Conditional_Simplification.CS_Reference
14:36:16 Timing TortoiseHare (6 threads, 5.494s elapsed time, 5.492s cpu time, 0.169s GC time, factor 1.00)
14:36:16 Finished TortoiseHare (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.95)
14:36:18 Timing Conditional_Simplification (2 threads, 1.730s elapsed time, 1.533s cpu time, 0.038s GC time, factor 0.89)
14:36:18 Finished Conditional_Simplification (0:00:03 elapsed time)
14:36:18 Timing RIPEMD-160-SPARK (2 threads, 1.525s elapsed time, 1.524s cpu time, 0.018s GC time, factor 1.00)
14:36:18 Finished RIPEMD-160-SPARK (0:00:03 elapsed time)
14:36:18 Timing Depth-First-Search (2 threads, 2.243s elapsed time, 2.242s cpu time, 0.039s GC time, factor 1.00)
14:36:18 Finished Depth-First-Search (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.91)
14:36:19 Timing Tree_Decomposition (6 threads, 8.275s elapsed time, 8.268s cpu time, 0.320s GC time, factor 1.00)
14:36:19 Finished Tree_Decomposition (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.96)
14:36:19 Timing FunWithFunctions (2 threads, 2.949s elapsed time, 2.944s cpu time, 0.071s GC time, factor 1.00)
14:36:19 Finished FunWithFunctions (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.93)
14:36:19 CZH_Foundations: theory CZH_Foundations.CZH_EX_Replacement
14:36:19 CZH_Foundations: theory CZH_Foundations.CZH_EX_TS
14:36:20 CZH_Foundations: theory CZH_Foundations.CZH_DG_Digraph
14:36:20 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Introduction
14:36:20 CZH_Foundations: theory CZH_Foundations.CZH_EX_Algebra
14:36:21 CZH_Foundations: theory CZH_Foundations.CZH_DG_DGHM
14:36:21 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_Digraph
14:36:21 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semicategory
14:36:22 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Conclusions
14:36:23 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semicategory
14:36:30 CZH_Foundations: theory CZH_Foundations.CZH_DG_TDGHM
14:36:31 CZH_Foundations: theory CZH_Foundations.CZH_DG_GRPH
14:36:31 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_DGHM
14:36:31 CZH_Foundations: theory CZH_Foundations.CZH_DG_Subdigraph
14:36:31 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semifunctor
14:36:32 CZH_Foundations: theory CZH_Foundations.CZH_DG_Simple
14:36:32 CZH_Foundations: theory CZH_Foundations.CZH_DG_PDigraph
14:36:33 CZH_Foundations: theory CZH_Foundations.CZH_SMC_GRPH
14:36:33 CZH_Foundations: theory CZH_Foundations.CZH_DG_Rel
14:36:33 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_TDGHM
14:36:34 CZH_Foundations: theory CZH_Foundations.CZH_DG_Par
14:36:35 CZH_Foundations: theory CZH_Foundations.CZH_DG_Set
14:36:37 CZH_Foundations: theory CZH_Foundations.CZH_DG_Conclusions
14:36:37 Running Free-Boolean-Algebra (on of1-proof+8-15) ...
14:36:37 Running Roy_Floyd_Warshall (on of1-proof+0-7) ...
14:36:38 Free-Boolean-Algebra: theory Free-Boolean-Algebra.Free_Boolean_Algebra
14:36:38 Roy_Floyd_Warshall: theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
14:36:39 Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
14:36:39 Timing Roy_Floyd_Warshall (8 threads, 0.265s elapsed time, 0.531s cpu time, 0.022s GC time, factor 2.00)
14:36:39 Finished Roy_Floyd_Warshall (0:00:01 elapsed time)
14:36:39 Timing Free-Boolean-Algebra (8 threads, 0.402s elapsed time, 0.981s cpu time, 0.028s GC time, factor 2.44)
14:36:39 Finished Free-Boolean-Algebra (0:00:01 elapsed time)
14:36:40 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
14:36:40 Echelon_Form: theory Echelon_Form.Echelon_Form
14:36:40 Running Aristotles_Assertoric_Syllogistic (on of2.proof.cit.tum.de+0-7) ...
14:36:40 Running Bondy (on of2.proof.cit.tum.de+8-15) ...
14:36:41 Running General-Triangle (on of3.proof.cit.tum.de+8-15) ...
14:36:41 Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
14:36:41 Bondy: theory Bondy.Bondy
14:36:41 Running Intro_Dest_Elim (on of3.proof.cit.tum.de+0-7) ...
14:36:41 Echelon_Form: theory Echelon_Form.Echelon_Form_Det
14:36:41 Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
14:36:41 CZH_Foundations: theory CZH_Foundations.CZH_DG_SemiCAT
14:36:41 CZH_Foundations: theory CZH_Foundations.CZH_SMC_NTSMCF
14:36:42 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
14:36:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Subsemicategory
14:36:42 Timing Aristotles_Assertoric_Syllogistic (6 threads, 0.195s elapsed time, 0.489s cpu time, 0.021s GC time, factor 2.51)
14:36:42 Finished Aristotles_Assertoric_Syllogistic (0:00:01 elapsed time)
14:36:42 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
14:36:42 Timing Bondy (6 threads, 0.243s elapsed time, 0.462s cpu time, 0.015s GC time, factor 1.90)
14:36:42 Finished Bondy (0:00:01 elapsed time)
14:36:42 Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
14:36:42 General-Triangle: theory General-Triangle.GeneralTriangle
14:36:42 Intro_Dest_Elim: theory Intro_Dest_Elim.IHOL_IDE
14:36:42 Intro_Dest_Elim: theory HOL-Library.LaTeXsugar
14:36:42 Intro_Dest_Elim: theory Intro_Dest_Elim.Reference_Prerequisites
14:36:42 Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Reference
14:36:42 CZH_Foundations: theory CZH_Foundations.CZH_SMC_PSemicategory
14:36:42 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
14:36:42 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
14:36:43 Timing General-Triangle (6 threads, 0.269s elapsed time, 0.577s cpu time, 0.019s GC time, factor 2.14)
14:36:43 Finished General-Triangle (0:00:01 elapsed time)
14:36:43 Timing Intro_Dest_Elim (6 threads, 0.296s elapsed time, 0.435s cpu time, 0.021s GC time, factor 1.47)
14:36:43 Finished Intro_Dest_Elim (0:00:01 elapsed time)
14:36:44 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
14:36:44 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Rel
14:36:44 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semifunctor
14:36:45 Running Ordinals_and_Cardinals (on 10.195.8.11+0-7) ...
14:36:47 Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
14:36:47 Timing Ordinals_and_Cardinals (2 threads, 0.144s elapsed time, 0.212s cpu time, 0.000s GC time, factor 1.47)
14:36:47 Finished Ordinals_and_Cardinals (0:00:01 elapsed time)
14:37:07 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Par
14:37:07 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Simple
14:37:07 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_NTSMCF
14:37:07 CZH_Foundations: theory CZH_Foundations.CZH_SMC_SemiCAT
14:37:08 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Set
14:37:16 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Conclusions
14:37:41 Timing Echelon_Form (6 threads, 77.294s elapsed time, 391.736s cpu time, 60.269s GC time, factor 5.07)
14:37:41 Finished Echelon_Form (0:01:31 elapsed time, 0:06:57 cpu time, factor 4.58)
14:37:51 Timing CZH_Foundations (6 threads, 93.145s elapsed time, 521.120s cpu time, 239.253s GC time, factor 5.59)
14:37:51 Finished CZH_Foundations (0:01:41 elapsed time, 0:08:55 cpu time, factor 5.30)
14:37:51 Building Hermite (on of4.proof.cit.tum.de+8-15) ...
14:37:52 Hermite: theory Hermite.Hermite
14:37:54 Hermite: theory Hermite.Hermite_IArrays
14:38:13 Timing Hermite (6 threads, 12.031s elapsed time, 43.641s cpu time, 3.601s GC time, factor 3.63)
14:38:13 Finished Hermite (0:00:22 elapsed time, 0:01:00 cpu time, factor 2.71)
14:38:16 Building CZH_Elementary_Categories (on of4.proof.cit.tum.de+0-7) ...
14:38:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Introduction
14:38:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Category
14:38:21 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Functor
14:38:21 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
14:38:22 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_GRPH
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Order
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_NTCF
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_CAT
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Rel
14:38:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
14:38:35 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Parallel
14:38:35 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SS
14:38:35 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
14:38:40 Building Smith_Normal_Form (on of4.proof.cit.tum.de+8-15) ...
14:38:41 Smith_Normal_Form: theory HOL-Eisbach.Eisbach
14:38:41 Smith_Normal_Form: theory Deriving.Generator_Aux
14:38:41 Smith_Normal_Form: theory Deriving.Derive_Manager
14:38:41 Smith_Normal_Form: theory HOL-Number_Theory.Cong
14:38:41 Smith_Normal_Form: theory HOL-Algebra.Congruence
14:38:41 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
14:38:41 Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
14:38:41 Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
14:38:42 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
14:38:42 Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:38:42 Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
14:38:42 Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
14:38:42 Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
14:38:42 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
14:38:42 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
14:38:42 Smith_Normal_Form: theory HOL-Algebra.Order
14:38:42 Smith_Normal_Form: theory List-Index.List_Index
14:38:42 Smith_Normal_Form: theory HOL-Number_Theory.Totient
14:38:43 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
14:38:43 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
14:38:43 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
14:38:43 Smith_Normal_Form: theory HOL-Algebra.Lattice
14:38:43 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
14:38:43 Smith_Normal_Form: theory Show.Show
14:38:44 Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
14:38:44 Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
14:38:44 Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:38:44 Smith_Normal_Form: theory Show.Show_Instances
14:38:44 Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
14:38:44 Smith_Normal_Form: theory VectorSpace.FunctionLemmas
14:38:44 Smith_Normal_Form: theory HOL-Algebra.Group
14:38:45 Smith_Normal_Form: theory Show.Show_Poly
14:38:46 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
14:38:46 Smith_Normal_Form: theory HOL-Algebra.Coset
14:38:46 Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
14:38:47 Smith_Normal_Form: theory HOL-Algebra.Ring
14:38:48 Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
14:38:48 Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
14:38:49 Smith_Normal_Form: theory HOL-Algebra.AbelCoset
14:38:49 Smith_Normal_Form: theory HOL-Algebra.Module
14:38:49 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
14:38:50 Smith_Normal_Form: theory VectorSpace.RingModuleFacts
14:38:51 Smith_Normal_Form: theory VectorSpace.MonoidSums
14:38:51 Smith_Normal_Form: theory HOL-Algebra.Ideal
14:38:51 Smith_Normal_Form: theory VectorSpace.LinearCombinations
14:38:52 Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
14:38:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
14:38:53 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
14:38:53 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Par
14:38:53 Smith_Normal_Form: theory HOL-Algebra.RingHom
14:38:54 Smith_Normal_Form: theory HOL-Algebra.UnivPoly
14:38:56 Smith_Normal_Form: theory VectorSpace.SumSpaces
14:38:56 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
14:38:56 Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:38:56 Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
14:38:56 Smith_Normal_Form: theory VectorSpace.VectorSpace
14:38:57 Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
14:38:58 Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
14:38:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_PCategory
14:38:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Simple
14:38:58 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
14:39:00 Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
14:39:00 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
14:39:01 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
14:39:01 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Comma
14:39:01 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Discrete
14:39:04 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
14:39:05 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_CAT
14:39:07 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CAT
14:39:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_FUNCT
14:39:11 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Set
14:39:16 Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
14:39:17 Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
14:39:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Hom
14:39:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
14:39:19 Smith_Normal_Form: theory HOL-Number_Theory.Residues
14:39:21 Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
14:39:22 Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
14:39:23 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
14:39:23 Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
14:39:26 Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
14:39:26 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_FUNCT
14:39:28 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:39:28 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
14:39:28 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
14:39:31 Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
14:39:31 Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
14:39:33 Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
14:39:34 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
14:39:36 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
14:39:36 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
14:39:36 Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
14:39:36 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
14:39:37 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
14:39:38 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
14:39:38 Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
14:39:38 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
14:39:38 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
14:39:38 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Cone
14:39:39 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
14:39:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
14:39:41 Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
14:39:41 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
14:39:42 Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
14:39:42 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
14:39:46 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
14:39:53 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Cone
14:41:07 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
14:42:18 Timing Smith_Normal_Form (6 threads, 179.710s elapsed time, 818.511s cpu time, 178.262s GC time, factor 4.55)
14:42:18 Finished Smith_Normal_Form (0:03:35 elapsed time, 0:15:02 cpu time, factor 4.19)
14:42:30 Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1), fast hosts: per critical node) (took 0.007s)
14:42:31 Running Modular_arithmetic_LLL_and_HNF_algorithms (on of4.proof.cit.tum.de+8-15) ...
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
14:42:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
14:42:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
14:42:36 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
14:42:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
14:42:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
14:42:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
14:42:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
14:42:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
14:42:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
14:42:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
14:42:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
14:42:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
14:42:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
14:42:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
14:42:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
14:42:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
14:42:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
14:42:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
14:42:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
14:42:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
14:42:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
14:42:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
14:42:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
14:42:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
14:42:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
14:42:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
14:42:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
14:42:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
14:42:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
14:42:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
14:42:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
14:42:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
14:42:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
14:42:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
14:42:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
14:42:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
14:42:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
14:42:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
14:42:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
14:42:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
14:42:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
14:42:58 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
14:42:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
14:43:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
14:43:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
14:43:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
14:43:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
14:43:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
14:43:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
14:43:09 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
14:43:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
14:43:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
14:43:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
14:43:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
14:43:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
14:43:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
14:43:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
14:43:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
14:43:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
14:43:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
14:43:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
14:43:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
14:43:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
14:43:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
14:43:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
14:43:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
14:43:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
14:43:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
14:43:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
14:43:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
14:43:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
14:43:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
14:43:42 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
14:43:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
14:43:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
14:43:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
14:44:37 Timing CZH_Elementary_Categories (6 threads, 371.862s elapsed time, 1760.272s cpu time, 874.199s GC time, factor 4.73)
14:44:37 Finished CZH_Elementary_Categories (0:06:20 elapsed time, 0:29:35 cpu time, factor 4.67)
14:44:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
14:44:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
14:44:49 Estimated 0:18:17 build time with path time heuristic (critical: absolute time (0:05:00), parallel: fixed threads (1), fast hosts: per critical node) (took 0.004s)
14:44:50 Running CZH_Universal_Constructions (on of4.proof.cit.tum.de+0-7) ...
14:44:50 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
14:44:50 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
14:44:51 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
14:44:57 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
14:45:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
14:45:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
14:45:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
14:45:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
14:45:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
14:45:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
14:45:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
14:45:16 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
14:45:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
14:45:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
14:45:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
14:45:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
14:45:43 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
14:45:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
14:45:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
14:45:53 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
14:45:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
14:46:13 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
14:46:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
14:46:14 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
14:46:16 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
14:46:44 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
14:47:04 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
14:47:12 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
14:50:14 Timing Modular_arithmetic_LLL_and_HNF_algorithms (6 threads, 456.726s elapsed time, 2283.586s cpu time, 687.261s GC time, factor 5.00)
14:50:14 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:07:40 elapsed time, 0:38:17 cpu time, factor 4.99)
14:57:04 Timing CZH_Universal_Constructions (6 threads, 732.228s elapsed time, 2897.047s cpu time, 1163.875s GC time, factor 3.96)
14:57:04 Finished CZH_Universal_Constructions (0:12:13 elapsed time, 0:48:20 cpu time, factor 3.95)
14:57:16 *** Host "of2.proof.cit.tum.de": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.40": failed to work
14:57:16 *** Error
14:57:16 *** Host "of3.proof.cit.tum.de": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.29": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.49": failed to work
14:57:16 *** ### Ignored report message: int
14:57:16 *** ### Ignored report message: array\ int
14:57:16 *** ### Ignored report message: int
14:57:16 *** Host "10.195.8.32": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.11": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.6.179": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.7.194": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.46": failed to work
14:57:16 *** Error
14:57:16 *** Host "of4.proof.cit.tum.de": failed to work
14:57:16 *** Error
14:57:16 *** Host "10.195.8.42": failed to work
14:57:16 *** Error
14:57:17 *** Host "10.195.8.30": failed to work
14:57:17 *** Error
14:57:17 Unfinished session(s): Universal_Hash_Families
14:57:17 
14:57:17 Finished at Fri Dec 8 14:57:17 GMT+1 2023
14:57:17 2:21:23 elapsed time, 51:28:53 cpu time, factor 21.85
14:57:17 Build step 'Execute shell' marked build as failure
14:57:18 Started calculate disk usage of build
14:57:18 Finished Calculation of disk usage of build in 0 seconds
14:57:38 Started calculate disk usage of workspace
14:57:38 Finished Calculation of disk usage of workspace in 0 seconds
14:57:39 Finished: FAILURE