Epistemic_Logic: theory Epistemic_Logic.Maximal_Consistent_Sets
23:25:01Epistemic_Logic: theory Epistemic_Logic.Epistemic_Logic
23:25:01Running Lowe_Ontological_Argument (on 10.195.8.49) ...
23:25:01Timing Padic_Field (2 threads, 1160.524s elapsed time, 2246.767s cpu time, 1092.640s GC time, factor 1.94)
23:25:01Finished Padic_Field (0:19:28 elapsed time, 0:37:39 cpu time, factor 1.93)
23:25:01Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness
23:25:01Hypergraph_Basics: theory Design_Theory.Design_Basics
23:25:01Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness
23:25:01Fourier: theory HOL-Library.Function_Algebras
23:25:01Fourier: theory Fourier.Confine
23:25:01Fourier: theory Fourier.Periodic
23:25:01Fourier: theory Fourier.Fourier_Aux2
23:25:01Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
23:25:01Fourier: theory Ergodic_Theory.SG_Library_Complement
23:25:01Hypergraph_Basics: theory Undirected_Graph_Theory.Undirected_Graph_Walks
23:25:01Hypergraph_Basics: theory Fishers_Inequality.Set_Multiset_Extras
23:25:01Generalized_Counting_Sort: theory Generalized_Counting_Sort.Sorting
23:25:02Fourier: theory Lp.Functional_Spaces
23:25:02Generalized_Counting_Sort: theory Generalized_Counting_Sort.Stability
23:25:02Hidden_Markov_Models: theory HOL-Library.State_Monad
23:25:02Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
23:25:02Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
23:25:02Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
23:25:02Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
23:25:02Hypergraph_Basics: theory Undirected_Graph_Theory.Bipartite_Graphs
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.Relations
23:25:03Running Knot_Theory (on 10.195.8.32) ...
23:25:03Running Jordan_Hoelder (on 10.195.8.32) ...
23:25:03Running Functional-Automata (on 10.195.8.32) ...
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.QML
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
23:25:03Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
23:25:03Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
23:25:03Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
23:25:03Hypergraph_Basics: theory Design_Theory.Design_Operations
23:25:04Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
23:25:04Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
23:25:04Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
23:25:04Fourier: theory Lp.Lp
23:25:04Lowe_Ontological_Argument: theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
23:25:04Running DiscretePricing (on 10.195.8.46) ...
23:25:04Running Modular_Assembly_Kit_Security (on 10.195.8.46) ...
23:25:04Running Foundation_of_geometry (on 10.195.8.46) ...
23:25:04Running FOL_Seq_Calc3 (on 10.195.8.46) ...
23:25:04Hidden_Markov_Models: theory Monad_Memo_DP.Memory
23:25:04Fourier: theory Fourier.Lspace
23:25:04Fourier: theory Fourier.Square_Integrable
23:25:04Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
23:25:04Hypergraph_Basics: theory Design_Theory.Block_Designs
23:25:04Hypergraph_Basics: theory Design_Theory.Sub_Designs
23:25:05Fourier: theory Fourier.Fourier
23:25:05Functional-Automata: theory Functional-Automata.AutoProj
23:25:05Functional-Automata: theory Functional-Automata.MaxPrefix
23:25:05Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
23:25:05Knot_Theory: theory HOL-Computational_Algebra.Fraction_Field
23:25:05Knot_Theory: theory HOL-Computational_Algebra.Factorial_Ring
23:25:05Functional-Automata: theory Functional-Automata.DA
23:25:05Running Trie (on 10.195.8.40) ...
23:25:05Functional-Automata: theory Functional-Automata.NA
23:25:05Jordan_Hoelder: theory Secondary_Sylow.GroupAction
23:25:05Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
23:25:05Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
23:25:05Functional-Automata: theory Functional-Automata.NAe
23:25:05Functional-Automata: theory Functional-Automata.MaxChop
23:25:05Functional-Automata: theory Functional-Automata.Automata
23:25:05Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
23:25:05Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.Projection
23:25:05Foundation_of_geometry: theory Foundation_of_geometry.Incidence
23:25:05Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.Prefix
23:25:05Functional-Automata: theory Functional-Automata.AutoMaxChop
23:25:06Functional-Automata: theory Regular-Sets.Regular_Set
23:25:06Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.Views
23:25:06Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
23:25:06Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
23:25:06Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
23:25:06Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
23:25:06Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.FlowPolicies
23:25:06Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.EventSystems
23:25:06FOL_Seq_Calc3: theory FOL_Seq_Calc3.List_Syntax
23:25:06FOL_Seq_Calc3: theory Collections.ICF_Tools
23:25:06Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
23:25:06FOL_Seq_Calc3: theory FOL_Seq_Calc3.Syntax
23:25:07Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
23:25:07FOL_Seq_Calc3: theory Collections.Ord_Code_Preproc
23:25:07Jordan_Hoelder: theory Secondary_Sylow.SndSylow
23:25:07FOL_Seq_Calc3: theory Collections.Locale_Code
23:25:07Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.BasicSecurityPredicates
23:25:07DiscretePricing: theory DiscretePricing.Filtration
23:25:07Knot_Theory: theory Knot_Theory.Preliminaries
23:25:07DiscretePricing: theory DiscretePricing.Generated_Subalgebra
23:25:07Running Koenigsberg_Friendship (on 10.195.8.30) ...
23:25:07Running Treaps (on 10.195.8.30) ...
23:25:07Running Gaussian_Integers (on 10.195.8.30) ...
23:25:07Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
23:25:07Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.StateEventSystems
23:25:07FOL_Seq_Calc3: theory FOL_Seq_Calc3.Fair_Stream
23:25:07Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
23:25:07FOL_Seq_Calc3: theory Abstract_Completeness.Abstract_Completeness
23:25:07Trie: theory Trie.Trie
23:25:07Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
23:25:07Hypergraph_Basics: theory Design_Theory.BIBD
23:25:08Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.BSPTaxonomy
23:25:08Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.InformationFlowProperties
23:25:08Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.SecureSystems
23:25:08DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
23:25:08Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
23:25:08Running BDD (on 10.195.8.30) ...
23:25:08FOL_Seq_Calc3: theory FOL_Seq_Calc3.Semantics
23:25:09Timing Abstract_Soundness (6 threads, 7.390s elapsed time, 15.694s cpu time, 1.205s GC time, factor 2.12)
23:25:09FOL_Seq_Calc3: theory FOL_Seq_Calc3.Encoding
23:25:09Finished Abstract_Soundness (0:00:08 elapsed time, 0:00:17 cpu time, factor 1.98)
23:25:09Hypergraph_Basics: theory Fishers_Inequality.Design_Extras
23:25:09Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.CompositionBase
23:25:09Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.UnwindingConditions
23:25:09Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.CompositionSupport
23:25:09Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.GeneralizedZippingLemma
23:25:09Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
23:25:09Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph
23:25:10Running Digit_Expansions (on 10.195.7.194) ...
23:25:10Running Boolean_Expression_Checkers (on 10.195.7.194) ...
23:25:10Timing Random_BSTs (2 threads, 11.533s elapsed time, 17.646s cpu time, 1.721s GC time, factor 1.53)
23:25:10Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.AuxiliaryLemmas
23:25:10Trie: theory Trie.Tries
23:25:10Finished Random_BSTs (0:00:51 elapsed time, 0:01:03 cpu time, factor 1.24)
23:25:10Koenigsberg_Friendship: theory Dijkstra_Shortest_Path.Graph
23:25:10Knot_Theory: theory Knot_Theory.Tangles
23:25:10DiscretePricing: theory DiscretePricing.Martingale
23:25:10Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph_Variations
23:25:11Knot_Theory: theory Knot_Theory.Tangle_Algebra
23:25:11DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
23:25:11Functional-Automata: theory Functional-Automata.RegSet_of_nat_DA
23:25:11Treaps: theory HOL-Data_Structures.Cmp
23:25:11Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.CompositionalityResults
23:25:11Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.UnwindingResults
23:25:11Treaps: theory HOL-Data_Structures.Less_False
23:25:11Modular_Assembly_Kit_Security: theory Modular_Assembly_Kit_Security.PropertyLibrary
23:25:11Functional-Automata: theory Regular-Sets.Regular_Exp
23:25:11Treaps: theory HOL-Data_Structures.Sorted_Less
23:25:11Foundation_of_geometry: theory Foundation_of_geometry.Order
23:25:11Treaps: theory HOL-Data_Structures.List_Ins_Del
23:25:11Running Transformer_Semantics (on 10.195.7.194) ...
23:25:11Timing Epistemic_Logic (6 threads, 2.658s elapsed time, 7.726s cpu time, 0.723s GC time, factor 2.91)
23:25:11Finished Epistemic_Logic (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.74)
23:25:11Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers
23:25:12Digit_Expansions: theory Digit_Expansions.Bits_Digits
23:25:12Gaussian_Integers: theory Matrix.Utility
23:25:12Treaps: theory HOL-Library.Function_Algebras
23:25:12Knot_Theory: theory Knot_Theory.Tangle_Relation
23:25:12Treaps: theory HOL-Data_Structures.Set_Specs
23:25:12Knot_Theory: theory Knot_Theory.Tangle_Moves
23:25:12Treaps: theory Landau_Symbols.Group_Sort
23:25:12Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph
23:25:12FOL_Seq_Calc3: theory Abstract_Soundness.Finite_Proof_Soundness
23:25:12FOL_Seq_Calc3: theory FOL_Seq_Calc3.Prover
23:25:12Digit_Expansions: theory Digit_Expansions.Carries
23:25:12Treaps: theory HOL-Data_Structures.Tree_Set
23:25:12Digit_Expansions: theory Digit_Expansions.Binary_Operations
23:25:12Hypergraph_Basics: theory Hypergraph_Basics.Hypergraph_Basics_Root
23:25:13Gaussian_Integers: theory Polynomial_Factorization.Missing_List
23:25:13Running Winding_Number_Eval (on 10.195.8.11) ...
23:25:13Knot_Theory: theory Knot_Theory.Link_Algebra
23:25:13Building Bell_Numbers_Spivey (on 10.195.8.11) ...
23:25:13Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
23:25:13Timing Hypergraph_Basics (8 threads, 13.243s elapsed time, 85.435s cpu time, 7.083s GC time, factor 6.45)
23:25:13Finished Hypergraph_Basics (0:00:14 elapsed time, 0:01:27 cpu time, factor 5.94)
23:25:14Foundation_of_geometry: theory Foundation_of_geometry.Congruence
23:25:14Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
23:25:14Knot_Theory: theory Knot_Theory.Example
23:25:14FOL_Seq_Calc3: theory FOL_Seq_Calc3.Completeness
23:25:14FOL_Seq_Calc3: theory FOL_Seq_Calc3.Export
23:25:14Treaps: theory Landau_Symbols.Landau_Real_Products
23:25:14Transformer_Semantics: theory Transformer_Semantics.Isotone_Transformers
23:25:14Transformer_Semantics: theory Transformer_Semantics.Powerset_Monad
23:25:14Running RSAPSS (on 10.195.8.42) ...
23:25:14Treaps: theory List-Index.List_Index
23:25:14Running Separation_Algebra (on 10.195.8.42) ...
23:25:14Running Synthetic_Completeness (on 10.195.8.42) ...
23:25:14Running Generic_Deriving (on 10.195.8.42) ...
23:25:14FOL_Seq_Calc3: theory FOL_Seq_Calc3.Soundness
23:25:14Timing Generalized_Counting_Sort (8 threads, 14.669s elapsed time, 64.156s cpu time, 1.787s GC time, factor 4.37)
23:25:14Finished Generalized_Counting_Sort (0:00:16 elapsed time, 0:01:06 cpu time, factor 4.09)
23:25:15Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
23:25:15Bell_Numbers_Spivey: theory HOL-Eisbach.Eisbach
23:25:15Bell_Numbers_Spivey: theory HOL-Combinatorics.Stirling
23:25:15Timing SATSolverVerification (2 threads, 118.879s elapsed time, 220.869s cpu time, 25.989s GC time, factor 1.86)
23:25:15FOL_Seq_Calc3: theory FOL_Seq_Calc3.Result
23:25:15Finished SATSolverVerification (0:02:02 elapsed time, 0:03:45 cpu time, factor 1.84)
23:25:15Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples
23:25:16Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares
23:25:16Transformer_Semantics: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
23:25:16Synthetic_Completeness: theory HOL-Cardinals.Order_Relation_More
23:25:16Synthetic_Completeness: theory HOL-Cardinals.Fun_More
23:25:16Winding_Number_Eval: theory HOL-Eisbach.Eisbach
23:25:16Separation_Algebra: theory HOL-Hoare.Hoare_Syntax
23:25:16Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field
23:25:16Generic_Deriving: theory Generic_Deriving.Tagged_Prod_Sum
23:25:16Generic_Deriving: theory Generic_Deriving.Derive_Datatypes
23:25:16Separation_Algebra: theory HOL-Hoare.Hoare_Tac
23:25:16Functional-Automata: theory Functional-Automata.RegExp2NA
23:25:16Bell_Numbers_Spivey: theory Card_Partitions.Set_Partition
23:25:16Functional-Automata: theory Functional-Automata.RegExp2NAe
23:25:16Synthetic_Completeness: theory HOL-Cardinals.Order_Union
23:25:17Timing Fourier (6 threads, 14.862s elapsed time, 70.253s cpu time, 4.324s GC time, factor 4.73)
23:25:17Finished Fourier (0:00:16 elapsed time, 0:01:12 cpu time, factor 4.36)
23:25:17Synthetic_Completeness: theory HOL-Cardinals.Wellfounded_More
23:25:17Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Relation
23:25:17Gaussian_Integers: theory Polynomial_Factorization.Missing_Multiset
23:25:17Bell_Numbers_Spivey: theory Card_Partitions.Injectivity_Solver
23:25:17RSAPSS: theory RSAPSS.Word
23:25:17BDD: theory BDD.BinDag
23:25:17Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory
23:25:17Transformer_Semantics: theory Transformer_Semantics.Kleisli_Transformers
23:25:17Gaussian_Integers: theory Polynomial_Factorization.Prime_Factorization
23:25:17Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Embedding
23:25:17Functional-Automata: theory Functional-Automata.AutoRegExp
23:25:17Bell_Numbers_Spivey: theory Card_Partitions.Card_Partitions
23:25:17Synthetic_Completeness: theory HOL-Cardinals.Wellorder_Constructions
23:25:17Running ABY3_Protocols (on 10.195.8.29) ...
23:25:17Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
23:25:17Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring
23:25:18Timing Hidden_Markov_Models (6 threads, 15.740s elapsed time, 42.251s cpu time, 5.458s GC time, factor 2.68)
23:25:18Finished Hidden_Markov_Models (0:00:17 elapsed time, 0:00:44 cpu time, factor 2.50)
23:25:18BDD: theory BDD.General
23:25:18Separation_Algebra: theory HOL-Library.Phantom_Type
23:25:18Bell_Numbers_Spivey: theory Bell_Numbers_Spivey.Bell_Numbers
23:25:18Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
23:25:18Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge
23:25:18Functional-Automata: theory Functional-Automata.Execute
23:25:18Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Test
23:25:18Functional-Automata: theory Functional-Automata.Functional_Automata
23:25:18Synthetic_Completeness: theory HOL-Cardinals.Cardinal_Order_Relation
23:25:18Separation_Algebra: theory HOL-Library.Cardinality
23:25:19Running Relational_Minimum_Spanning_Trees (on 10.195.8.29) ...
23:25:19Running AxiomaticCategoryTheory (on 10.195.8.29) ...
23:25:19Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:25:19Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Everything
23:25:19Generic_Deriving: theory Generic_Deriving.Derive
23:25:19Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
23:25:19Knot_Theory: theory HOL-Computational_Algebra.Polynomial
23:25:19Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
23:25:19Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantaloid
23:25:19Running Real_Power (on of2.proof.cit.tum.de) ...
23:25:19Running SCC_Bloemen_Sequential (on of2.proof.cit.tum.de) ...
23:25:19Separation_Algebra: theory HOL-Library.Numeral_Type
23:25:20Running Belief_Revision (on of2.proof.cit.tum.de) ...
23:25:20Running Dict_Construction (on of2.proof.cit.tum.de) ...
23:25:20Transformer_Semantics: theory Transformer_Semantics.Kleisli_Quantale
23:25:20Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
23:25:20Separation_Algebra: theory HOL-Hoare.Hoare_Logic_Abort
23:25:20Real_Power: theory Real_Power.RatPower
23:25:20Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
23:25:20Running Error_Function (on of4.proof.cit.tum.de) ...
23:25:20Belief_Revision: theory Belief_Revision.AGM_Logic
23:25:20Dict_Construction: theory Automatic_Refinement.Refine_Util_Bootstrap1
23:25:20Running Quasi_Borel_Spaces (on of4.proof.cit.tum.de) ...
23:25:20Dict_Construction: theory Deriving.Derive_Manager
23:25:20Dict_Construction: theory Deriving.Generator_Aux
23:25:20Dict_Construction: theory Dict_Construction.Introduction
23:25:20Dict_Construction: theory Dict_Construction.Impossibility
23:25:20Dict_Construction: theory HOL-Library.ListVector
23:25:20Synthetic_Completeness: theory Synthetic_Completeness.Maximal_Consistent_Sets
23:25:20Dict_Construction: theory Automatic_Refinement.Mk_Term_Antiquot
23:25:20Dict_Construction: theory Automatic_Refinement.Mpat_Antiquot
23:25:20Dict_Construction: theory Lazy_Case.Lazy_Case
23:25:21Dict_Construction: theory Show.Show
23:25:21Real_Power: theory Real_Power.RealPower
23:25:21Dict_Construction: theory Automatic_Refinement.Refine_Util
23:25:21Treaps: theory Landau_Symbols.Landau_Simprocs
23:25:21Running Probability_Inequality_Completeness (on of4.proof.cit.tum.de) ...
23:25:21AxiomaticCategoryTheory: theory AxiomaticCategoryTheory.AxiomaticCategoryTheory
23:25:21Running Attack_Trees (on of4.proof.cit.tum.de) ...
23:25:21Boolean_Expression_Checkers: theory Boolean_Expression_Checkers.Boolean_Expression_Example
23:25:21Belief_Revision: theory Belief_Revision.AGM_Remainder
23:25:21DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
23:25:21Belief_Revision: theory Belief_Revision.AGM_Contraction
23:25:21Synthetic_Completeness: theory Synthetic_Completeness.Derivations
23:25:21Synthetic_Completeness: theory Synthetic_Completeness.Refutations
23:25:21Real_Power: theory Real_Power.Log
23:25:21Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Kruskal
23:25:21Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_Tableau
23:25:21Dict_Construction: theory Dict_Construction.Dict_Construction
23:25:21Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Prim
23:25:21Separation_Algebra: theory HOL-Library.Type_Length
23:25:21Probability_Inequality_Completeness: theory Probability_Inequality_Completeness.Probability_Inequality_Completeness
23:25:21Attack_Trees: theory Attack_Trees.MC
23:25:21Synthetic_Completeness: theory Synthetic_Completeness.Example_First_Order_Logic
23:25:21SCC_Bloemen_Sequential: theory SCC_Bloemen_Sequential.SCC_Bloemen_Sequential
23:25:22Error_Function: theory HOL-Library.Function_Algebras
23:25:22Error_Function: theory Error_Function.Error_Function
23:25:22Error_Function: theory Landau_Symbols.Group_Sort
23:25:22Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.StandardBorel
23:25:22DiscretePricing: theory DiscretePricing.Fair_Price
23:25:22Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
23:25:22Dict_Construction: theory Show.Show_Instances
23:25:22Belief_Revision: theory Belief_Revision.AGM_Revision
23:25:22BDD: theory BDD.ProcedureSpecs
23:25:22Attack_Trees: theory Attack_Trees.AT
23:25:22Timing Lowe_Ontological_Argument (2 threads, 19.304s elapsed time, 12.320s cpu time, 0.418s GC time, factor 0.64)
23:25:22Finished Lowe_Ontological_Argument (0:00:21 elapsed time, 0:00:13 cpu time, factor 0.65)
23:25:22Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
23:25:22Dict_Construction: theory Dict_Construction.Termination
23:25:22Dict_Construction: theory Dict_Construction.Test_Side_Conditions
23:25:22Dict_Construction: theory Dict_Construction.Test_Dict_Construction
23:25:22Treaps: theory Landau_Symbols.Landau_More
23:25:22RSAPSS: theory RSAPSS.Mod
23:25:22RSAPSS: theory RSAPSS.WordOperations
23:25:22RSAPSS: theory RSAPSS.Crypt
23:25:22Dict_Construction: theory Dict_Construction.Test_Lazy_Case
23:25:22RSAPSS: theory RSAPSS.Pdifference
23:25:22Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
23:25:22ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
23:25:23ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
23:25:23Synthetic_Completeness: theory Synthetic_Completeness.Example_Hybrid_Logic
23:25:23Separation_Algebra: theory Separation_Algebra.Map_Extra
23:25:23RSAPSS: theory RSAPSS.Productdivides
23:25:23Error_Function: theory Landau_Symbols.Landau_Real_Products
23:25:23RSAPSS: theory RSAPSS.Cryptinverts
23:25:23Separation_Algebra: theory HOL-Library.Word
23:25:23BDD: theory BDD.EvalProof
23:25:23ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
23:25:23BDD: theory BDD.RepointProof
23:25:23BDD: theory BDD.LevellistProof
23:25:23Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.QuasiBorel
23:25:24BDD: theory BDD.ShareRepProof
23:25:24Separation_Algebra: theory Separation_Algebra.Separation_Algebra
23:25:24Winding_Number_Eval: theory Budan_Fourier.BF_Misc
23:25:24Attack_Trees: theory Attack_Trees.Infrastructure
23:25:24BDD: theory BDD.ShareReduceRepListProof
23:25:24BDD: theory BDD.NormalizeTotalProof
23:25:24Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction
23:25:25Timing Real_Power (6 threads, 4.048s elapsed time, 12.238s cpu time, 0.370s GC time, factor 3.02)
23:25:25Finished Real_Power (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.60)
23:25:25Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel
23:25:25Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel
23:25:25Timing Belief_Revision (6 threads, 4.384s elapsed time, 16.993s cpu time, 0.712s GC time, factor 3.88)
23:25:25Finished Belief_Revision (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.33)
23:25:25Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Product_QuasiBorel
23:25:25Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
23:25:25Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.CoProduct_QuasiBorel
23:25:25Separation_Algebra: theory Separation_Algebra.Sep_Heap_Instance
23:25:26Relational_Minimum_Spanning_Trees: theory Relational_Minimum_Spanning_Trees.Boruvka
23:25:26Separation_Algebra: theory Separation_Algebra.Sep_Tactics
23:25:26RSAPSS: theory RSAPSS.SHA1Padding
23:25:26RSAPSS: theory RSAPSS.Wordarith
23:25:26RSAPSS: theory RSAPSS.SHA1
23:25:26Attack_Trees: theory Attack_Trees.GDPRhealthcare
23:25:26Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Exponent_QuasiBorel
23:25:26Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel
23:25:26Timing Trie (2 threads, 18.385s elapsed time, 20.851s cpu time, 0.822s GC time, factor 1.13)
23:25:26Separation_Algebra: theory Separation_Algebra.Sep_Tactics_Test
23:25:26Finished Trie (0:00:20 elapsed time, 0:00:23 cpu time, factor 1.11)
23:25:26Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
23:25:26Timing Buildings (2 threads, 136.991s elapsed time, 236.167s cpu time, 14.263s GC time, factor 1.72)
23:25:26Finished Buildings (0:02:20 elapsed time, 0:03:59 cpu time, factor 1.71)
23:25:27Separation_Algebra: theory Separation_Algebra.Simple_Separation_Example
23:25:27Error_Function: theory Landau_Symbols.Landau_Simprocs
23:25:27RSAPSS: theory RSAPSS.EMSAPSS
23:25:27ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
23:25:27Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
23:25:27Generic_Deriving: theory Generic_Deriving.Derive_Algebra
23:25:27Generic_Deriving: theory Generic_Deriving.Derive_Algebra_Laws
23:25:27Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
23:25:27ABY3_Protocols: theory ABY3_Protocols.Multiplication
23:25:27Timing Jordan_Hoelder (2 threads, 21.547s elapsed time, 33.315s cpu time, 2.210s GC time, factor 1.55)
23:25:27Finished Jordan_Hoelder (0:00:24 elapsed time, 0:00:36 cpu time, factor 1.48)
23:25:27Error_Function: theory Landau_Symbols.Landau_More
23:25:27Separation_Algebra: theory Separation_Algebra.VM_Example
23:25:27Timing Attack_Trees (6 threads, 5.450s elapsed time, 12.725s cpu time, 0.685s GC time, factor 2.33)
23:25:27Finished Attack_Trees (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.13)
23:25:28Error_Function: theory Error_Function.Error_Function_Asymptotics
23:25:28Timing Functional-Automata (2 threads, 22.193s elapsed time, 30.042s cpu time, 2.441s GC time, factor 1.35)
23:25:28Finished Functional-Automata (0:00:25 elapsed time, 0:00:32 cpu time, factor 1.31)
23:25:28RSAPSS: theory RSAPSS.RSAPSS
23:25:28Treaps: theory Random_BSTs.Random_BSTs
23:25:28ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
23:25:28ABY3_Protocols: theory ABY3_Protocols.Shuffle
23:25:28Timing Digit_Expansions (2 threads, 16.551s elapsed time, 30.212s cpu time, 0.944s GC time, factor 1.83)
23:25:28Finished Digit_Expansions (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.72)
23:25:29Knot_Theory: theory Knot_Theory.Kauffman_Matrix
23:25:29DiscretePricing: theory DiscretePricing.CRR_Model
23:25:29Timing SCC_Bloemen_Sequential (6 threads, 8.440s elapsed time, 24.961s cpu time, 1.474s GC time, factor 2.96)
23:25:29Finished SCC_Bloemen_Sequential (0:00:09 elapsed time, 0:00:25 cpu time, factor 2.74)
23:25:29Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Monad_QuasiBorel
23:25:29Timing Error_Function (6 threads, 7.327s elapsed time, 19.633s cpu time, 1.967s GC time, factor 2.68)
23:25:29Finished Error_Function (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.36)
23:25:30Timing FOL_Seq_Calc3 (2 threads, 22.652s elapsed time, 31.264s cpu time, 2.057s GC time, factor 1.38)
23:25:30Finished FOL_Seq_Calc3 (0:00:25 elapsed time, 0:00:33 cpu time, factor 1.33)
23:25:30Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure
23:25:30Synthetic_Completeness: theory Synthetic_Completeness.Example_Modal_Logic
23:25:30Separation_Algebra: theory Separation_Algebra.Separation_Algebra_Alt
23:25:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure
23:25:31Synthetic_Completeness: theory Synthetic_Completeness.Example_Propositional_SC
23:25:31Separation_Algebra: theory Separation_Algebra.Sep_Eq
23:25:31Quasi_Borel_Spaces: theory Quasi_Borel_Spaces.Bayesian_Linear_Regression
23:25:32Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
23:25:32Timing Transformer_Semantics (2 threads, 17.356s elapsed time, 31.546s cpu time, 2.326s GC time, factor 1.82)
23:25:32Finished Transformer_Semantics (0:00:20 elapsed time, 0:00:34 cpu time, factor 1.67)
23:25:32Timing Boolean_Expression_Checkers (2 threads, 17.877s elapsed time, 31.267s cpu time, 6.337s GC time, factor 1.75)
23:25:32Finished Boolean_Expression_Checkers (0:00:21 elapsed time, 0:00:34 cpu time, factor 1.64)
23:25:33Generic_Deriving: theory Generic_Deriving.Derive_Encode
23:25:33Knot_Theory: theory Knot_Theory.Computations
23:25:34Knot_Theory: theory Knot_Theory.Linkrel_Kauffman
23:25:34Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
23:25:34Knot_Theory: theory Knot_Theory.Kauffman_Invariance
23:25:34Knot_Theory: theory Knot_Theory.Knot_Theory
23:25:34Separation_Algebra: theory Separation_Algebra.Types_D
23:25:35Timing Probability_Inequality_Completeness (6 threads, 12.866s elapsed time, 45.685s cpu time, 3.475s GC time, factor 3.55)
23:25:35Finished Probability_Inequality_Completeness (0:00:13 elapsed time, 0:00:46 cpu time, factor 3.38)
23:25:36Timing Dict_Construction (6 threads, 14.697s elapsed time, 32.852s cpu time, 4.454s GC time, factor 2.24)
23:25:36Finished Dict_Construction (0:00:16 elapsed time, 0:00:35 cpu time, factor 2.19)
23:25:37Timing Quasi_Borel_Spaces (6 threads, 14.761s elapsed time, 56.908s cpu time, 4.623s GC time, factor 3.86)
23:25:37Finished Quasi_Borel_Spaces (0:00:16 elapsed time, 0:00:58 cpu time, factor 3.57)
23:25:38DiscretePricing: theory DiscretePricing.Option_Price_Examples
23:25:39Timing Applicative_Lifting (2 threads, 44.454s elapsed time, 71.816s cpu time, 8.509s GC time, factor 1.62)
23:25:39Finished Applicative_Lifting (0:01:36 elapsed time, 0:01:55 cpu time, factor 1.20)
23:25:40Separation_Algebra: theory Separation_Algebra.Abstract_Separation_D
23:25:41Generic_Deriving: theory Generic_Deriving.Derive_Eq
23:25:43Separation_Algebra: theory Separation_Algebra.Separation_D
23:25:45Generic_Deriving: theory Generic_Deriving.Derive_Eq_Laws
23:25:45Treaps: theory Treaps.Treap
23:25:45Treaps: theory Treaps.Probability_Misc
23:25:45Treaps: theory Treaps.Random_List_Permutation
23:25:46Treaps: theory Treaps.Treap_Sort_and_BSTs
23:25:48Generic_Deriving: theory Generic_Deriving.Derive_Show
23:25:50Treaps: theory Treaps.Random_Treap
23:25:50Timing ABY3_Protocols (2 threads, 25.688s elapsed time, 36.110s cpu time, 2.238s GC time, factor 1.41)
23:25:50Finished ABY3_Protocols (0:00:30 elapsed time, 0:00:40 cpu time, factor 1.34)
23:25:51Timing Shadow_SC_DOM (2 threads, 1355.799s elapsed time, 2346.524s cpu time, 308.806s GC time, factor 1.73)
23:25:51Finished Shadow_SC_DOM (0:24:12 elapsed time, 0:41:21 cpu time, factor 1.71)
23:25:52Timing Modular_Assembly_Kit_Security (2 threads, 44.482s elapsed time, 75.518s cpu time, 7.783s GC time, factor 1.70)
23:25:52Finished Modular_Assembly_Kit_Security (0:00:46 elapsed time, 0:01:17 cpu time, factor 1.67)
23:25:52Running PLM (on of1-proof+8-15) ...
23:25:52Running Heard_Of (on of1-proof+0-7) ...
23:25:52PLM: theory HOL-Eisbach.Eisbach
23:25:52Heard_Of: theory Heard_Of.HOModel
23:25:52PLM: theory HOL-Library.LaTeXsugar
23:25:52Heard_Of: theory HOL-Library.Infinite_Set
23:25:52PLM: theory PLM.TAO_1_Embedding
23:25:52Running JiveDataStoreModel (on of3.proof.cit.tum.de) ...
23:25:52Heard_Of: theory Heard_Of.Majorities
23:25:53Running FocusStreamsCaseStudies (on of3.proof.cit.tum.de) ...
23:25:53Running FeatherweightJava (on of3.proof.cit.tum.de) ...
23:25:53PLM: theory HOL-Library.OptionalSugar
23:25:53Running Lam-ml-Normalization (on of3.proof.cit.tum.de) ...
23:25:53Heard_Of: theory HOL-Library.Omega_Words_Fun
23:25:53PLM: theory HOL-Eisbach.Eisbach_Tools
23:25:53Heard_Of: theory Stuttering_Equivalence.Samplers
23:25:53FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ArithExtras
23:25:53FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ListExtras
23:25:53FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.arith_hints
23:25:53JiveDataStoreModel: theory JiveDataStoreModel.TypeIds
23:25:53FeatherweightJava: theory FeatherweightJava.FJDefs
23:25:53Lam-ml-Normalization: theory HOL-Library.LaTeXsugar
23:25:53PLM: theory PLM.TAO_2_Semantics
23:25:53Heard_Of: theory Stuttering_Equivalence.StutterEquivalence
23:25:54Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
23:25:54FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.stream
23:25:54Timing VerifyThis2018 (2 threads, 94.110s elapsed time, 142.358s cpu time, 6.738s GC time, factor 1.51)
23:25:54Finished VerifyThis2018 (0:01:38 elapsed time, 0:02:27 cpu time, factor 1.49)
23:25:54Heard_Of: theory Heard_Of.AteDefs
23:25:54Heard_Of: theory Heard_Of.EigbyzDefs
23:25:54Heard_Of: theory Heard_Of.LastVotingDefs
23:25:54Heard_Of: theory Heard_Of.OneThirdRuleDefs
23:25:54Heard_Of: theory Heard_Of.UteDefs
23:25:54Heard_Of: theory Heard_Of.UvDefs
23:25:54Heard_Of: theory Heard_Of.Reduction
23:25:54PLM: theory PLM.TAO_3_Quantifiable
23:25:54Running Noninterference_Concurrent_Composition (on 10.195.8.49) ...
23:25:54JiveDataStoreModel: theory JiveDataStoreModel.JavaType
23:25:54PLM: theory PLM.TAO_4_BasicDefinitions
23:25:54Running Selection_Heap_Sort (on 10.195.8.49) ...
23:25:54PLM: theory PLM.TAO_5_MetaSolver
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.BitBoolTS
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_types
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_types
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.JoinSplitTime
23:25:55PLM: theory PLM.TAO_6_Identifiable
23:25:55JiveDataStoreModel: theory JiveDataStoreModel.DirectSubtypes
23:25:55Heard_Of: theory Heard_Of.AteProof
23:25:55Heard_Of: theory Heard_Of.EigbyzProof
23:25:55JiveDataStoreModel: theory JiveDataStoreModel.Subtype
23:25:55Heard_Of: theory Heard_Of.LastVotingProof
23:25:55Heard_Of: theory Heard_Of.OneThirdRuleProof
23:25:55PLM: theory PLM.TAO_7_Axioms
23:25:55JiveDataStoreModel: theory JiveDataStoreModel.Attributes
23:25:55JiveDataStoreModel: theory JiveDataStoreModel.Value
23:25:55Heard_Of: theory Heard_Of.UteProof
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler
23:25:55Heard_Of: theory Heard_Of.UvProof
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler_proof
23:25:55FeatherweightJava: theory FeatherweightJava.FJAux
23:25:55Running Consensus_Refined (on 10.195.8.32) ...
23:25:55PLM: theory PLM.TAO_8_Definitions
23:25:55PLM: theory PLM.TAO_98_ArtificialTheorems
23:25:55FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR
23:25:55PLM: theory PLM.TAO_99_SanityTests
23:25:56Building Noninterference_CSP (on 10.195.8.32) ...
23:25:56Noninterference_Concurrent_Composition: theory Noninterference_Concurrent_Composition.ConcurrentComposition
23:25:56FeatherweightJava: theory FeatherweightJava.FJSound
23:25:56FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_proof
23:25:56FeatherweightJava: theory FeatherweightJava.Execute
23:25:56PLM: theory PLM.TAO_9_PLM
23:25:57JiveDataStoreModel: theory JiveDataStoreModel.AttributesIndep
23:25:57JiveDataStoreModel: theory JiveDataStoreModel.Location
23:25:57Running PAL (on 10.195.8.46) ...
23:25:57Timing Closest_Pair_Points (2 threads, 108.560s elapsed time, 194.402s cpu time, 9.124s GC time, factor 1.79)
23:25:57Finished Closest_Pair_Points (0:01:52 elapsed time, 0:03:18 cpu time, factor 1.77)
23:25:58Consensus_Refined: theory Consensus_Refined.Consensus_Misc
23:25:58FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway
23:25:58Consensus_Refined: theory Consensus_Refined.Consensus_Types
23:25:58Noninterference_CSP: theory Noninterference_CSP.CSPNoninterference
23:25:58JiveDataStoreModel: theory JiveDataStoreModel.Store
23:25:58Consensus_Refined: theory Consensus_Refined.Quorums
23:25:58FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof_aux
23:25:58Consensus_Refined: theory Consensus_Refined.Infra
23:25:58Consensus_Refined: theory Consensus_Refined.Refinement
23:25:58FeatherweightJava: theory FeatherweightJava.Featherweight_Java
23:25:58FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof
23:25:58Consensus_Refined: theory Consensus_Refined.Three_Steps
23:25:58Running Myhill-Nerode (on 10.195.8.40) ...
23:25:58Consensus_Refined: theory Consensus_Refined.Two_Steps
23:25:58Consensus_Refined: theory HOL-Library.Infinite_Set
23:25:59JiveDataStoreModel: theory JiveDataStoreModel.StoreProperties
23:25:59PAL: theory PAL.PAL
23:25:59Running Randomised_BSTs (on 10.195.8.40) ...
23:25:59Noninterference_CSP: theory Noninterference_CSP.ClassicalNoninterference
23:25:59JiveDataStoreModel: theory JiveDataStoreModel.JML
23:25:59JiveDataStoreModel: theory JiveDataStoreModel.UnivSpec
23:25:59Timing Synthetic_Completeness (2 threads, 41.242s elapsed time, 66.749s cpu time, 6.926s GC time, factor 1.62)
23:25:59Finished Synthetic_Completeness (0:00:43 elapsed time, 0:01:09 cpu time, factor 1.59)
23:25:59Consensus_Refined: theory HOL-Library.Omega_Words_Fun
23:25:59Selection_Heap_Sort: theory Selection_Heap_Sort.Sort
23:25:59Timing FeatherweightJava (6 threads, 4.888s elapsed time, 13.788s cpu time, 0.981s GC time, factor 2.82)
23:25:59Finished FeatherweightJava (0:00:05 elapsed time, 0:00:14 cpu time, factor 2.48)
23:25:59Selection_Heap_Sort: theory Selection_Heap_Sort.RemoveMax
23:25:59Timing Lam-ml-Normalization (6 threads, 5.464s elapsed time, 10.182s cpu time, 0.968s GC time, factor 1.86)
23:25:59Finished Lam-ml-Normalization (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.72)
23:25:59Consensus_Refined: theory Heard_Of.HOModel
23:25:59Selection_Heap_Sort: theory Selection_Heap_Sort.Heap
23:25:59PLM: theory PLM.TAO_10_PossibleWorlds
23:25:59PLM: theory PLM.TAO_99_Paradox
23:26:00Timing JiveDataStoreModel (6 threads, 5.657s elapsed time, 14.154s cpu time, 1.176s GC time, factor 2.50)
23:26:00Finished JiveDataStoreModel (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.28)
23:26:00Selection_Heap_Sort: theory Selection_Heap_Sort.SelectionSort_Functional
23:26:00Consensus_Refined: theory Consensus_Refined.Voting
23:26:00Running Propositional_Logic_Class (on 10.195.8.30) ...
23:26:00Noninterference_CSP: theory Noninterference_CSP.GeneralizedNoninterference
23:26:00PLM: theory PLM.Thesis
23:26:01Consensus_Refined: theory Consensus_Refined.Same_Vote
23:26:01Running Possibilistic_Noninterference (on 10.195.7.194) ...
23:26:01Consensus_Refined: theory Consensus_Refined.MRU_Vote
23:26:01Consensus_Refined: theory Consensus_Refined.MRU_Vote_Opt
23:26:01Consensus_Refined: theory Consensus_Refined.Three_Step_MRU
23:26:01Selection_Heap_Sort: theory Selection_Heap_Sort.HeapFunctional
23:26:01Selection_Heap_Sort: theory Selection_Heap_Sort.HeapImperative
23:26:01Consensus_Refined: theory Consensus_Refined.Observing_Quorums
23:26:01Propositional_Logic_Class: theory HOL-Combinatorics.Transposition
23:26:01Myhill-Nerode: theory Open_Induction.Restricted_Predicates
23:26:01Propositional_Logic_Class: theory HOL-Library.Cancellation
23:26:01Myhill-Nerode: theory Abstract-Rewriting.Seq
23:26:01Running Valuation (on 10.195.7.194) ...
23:26:01Timing RSAPSS (2 threads, 43.689s elapsed time, 59.949s cpu time, 2.393s GC time, factor 1.37)
23:26:01Finished RSAPSS (0:00:46 elapsed time, 0:01:03 cpu time, factor 1.35)
23:26:01Timing Heard_Of (8 threads, 8.491s elapsed time, 42.344s cpu time, 3.210s GC time, factor 4.99)
23:26:01Finished Heard_Of (0:00:09 elapsed time, 0:00:43 cpu time, factor 4.56)
23:26:02Timing FocusStreamsCaseStudies (6 threads, 7.802s elapsed time, 27.160s cpu time, 2.240s GC time, factor 3.48)
23:26:02Finished FocusStreamsCaseStudies (0:00:08 elapsed time, 0:00:28 cpu time, factor 3.20)
23:26:02Propositional_Logic_Class: theory HOL-Library.FuncSet
23:26:02Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
23:26:02Timing PLM (8 threads, 8.974s elapsed time, 37.204s cpu time, 3.608s GC time, factor 4.15)
23:26:02Finished PLM (0:00:09 elapsed time, 0:00:38 cpu time, factor 3.87)
23:26:03Myhill-Nerode: theory Regular-Sets.Regular_Set
23:26:03Myhill-Nerode: theory Well_Quasi_Orders.Infinite_Sequences
23:26:03Timing Password_Authentication_Protocol (2 threads, 103.439s elapsed time, 156.535s cpu time, 7.438s GC time, factor 1.51)
23:26:03Finished Password_Authentication_Protocol (0:01:46 elapsed time, 0:02:39 cpu time, factor 1.50)
23:26:03Myhill-Nerode: theory Well_Quasi_Orders.Minimal_Elements
23:26:03Consensus_Refined: theory Consensus_Refined.Observing_Quorums_Opt
23:26:03Consensus_Refined: theory Consensus_Refined.Voting_Opt
23:26:03Propositional_Logic_Class: theory HOL-Library.Multiset
23:26:03Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
23:26:03Myhill-Nerode: theory Well_Quasi_Orders.Least_Enum
23:26:03Consensus_Refined: theory Consensus_Refined.Two_Step_Observing
23:26:03Consensus_Refined: theory Consensus_Refined.Ate_Defs
23:26:03Propositional_Logic_Class: theory HOL-Library.Disjoint_Sets
23:26:03Possibilistic_Noninterference: theory Possibilistic_Noninterference.MyTactics
23:26:04Possibilistic_Noninterference: theory Possibilistic_Noninterference.Interface
23:26:04Possibilistic_Noninterference: theory Possibilistic_Noninterference.Language_Semantics
23:26:04Possibilistic_Noninterference: theory Possibilistic_Noninterference.Bisim
23:26:04Propositional_Logic_Class: theory Propositional_Logic_Class.Implication_Logic
23:26:04Consensus_Refined: theory Consensus_Refined.BenOr_Defs
23:26:04Consensus_Refined: theory Consensus_Refined.CT_Defs
23:26:04Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Logic
23:26:05Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Logic_Completeness
23:26:05Running Nullstellensatz (on 10.195.7.194) ...
23:26:06Running MiniML (on 10.195.7.194) ...
23:26:06Timing Gaussian_Integers (2 threads, 52.646s elapsed time, 84.405s cpu time, 3.740s GC time, factor 1.60)
23:26:06Finished Gaussian_Integers (0:00:56 elapsed time, 0:01:27 cpu time, factor 1.56)
23:26:06Running WorkerWrapper (on 10.195.7.194) ...
23:26:06Timing Bell_Numbers_Spivey (2 threads, 20.146s elapsed time, 36.177s cpu time, 1.578s GC time, factor 1.80)
23:26:06Finished Bell_Numbers_Spivey (0:00:49 elapsed time, 0:01:10 cpu time, factor 1.41)
23:26:06Myhill-Nerode: theory Regular-Sets.Regular_Exp
23:26:07Consensus_Refined: theory Consensus_Refined.HO_Transition_System
23:26:07Consensus_Refined: theory Consensus_Refined.New_Algorithm_Defs
23:26:07Running VectorSpace (on 10.195.8.11) ...
23:26:07Consensus_Refined: theory Consensus_Refined.OneThirdRule_Defs
23:26:07MiniML: theory MiniML.Maybe
23:26:07WorkerWrapper: theory WorkerWrapper.Maybe
23:26:07WorkerWrapper: theory WorkerWrapper.Nats
23:26:07MiniML: theory MiniML.Type
23:26:08Consensus_Refined: theory Consensus_Refined.Paxos_Defs
23:26:08Valuation: theory Valuation.Valuation1
23:26:08Running Old_Datatype_Show (on 10.195.8.11) ...
23:26:08Consensus_Refined: theory Consensus_Refined.Uv_Defs
23:26:08Running Wetzels_Problem (on 10.195.8.11) ...
23:26:09Timing Foundation_of_geometry (2 threads, 61.108s elapsed time, 98.684s cpu time, 20.784s GC time, factor 1.61)
23:26:09Finished Foundation_of_geometry (0:01:03 elapsed time, 0:01:41 cpu time, factor 1.60)
23:26:09WorkerWrapper: theory WorkerWrapper.LList
23:26:09Possibilistic_Noninterference: theory Possibilistic_Noninterference.During_Execution
23:26:09Timing Noninterference_Concurrent_Composition (2 threads, 12.374s elapsed time, 22.276s cpu time, 0.705s GC time, factor 1.80)
23:26:09Finished Noninterference_Concurrent_Composition (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.69)
23:26:09Propositional_Logic_Class: theory HOL-Combinatorics.Permutations
23:26:09Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
23:26:09Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
23:26:10Consensus_Refined: theory Heard_Of.Majorities
23:26:10Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
23:26:10Nullstellensatz: theory Nullstellensatz.Univariate_PM
23:26:10Propositional_Logic_Class: theory HOL-Combinatorics.List_Permutation
23:26:10Propositional_Logic_Class: theory Propositional_Logic_Class.List_Utilities
23:26:11Timing Mersenne_Primes (2 threads, 173.919s elapsed time, 285.427s cpu time, 47.313s GC time, factor 1.64)
23:26:11Finished Mersenne_Primes (0:02:57 elapsed time, 0:04:49 cpu time, factor 1.63)
23:26:11Propositional_Logic_Class: theory Propositional_Logic_Class.Classical_Connectives
23:26:11Timing PAL (2 threads, 11.595s elapsed time, 18.827s cpu time, 1.061s GC time, factor 1.62)
23:26:11Finished PAL (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.53)
23:26:11Myhill-Nerode: theory Myhill-Nerode.Folds
23:26:11Myhill-Nerode: theory Regular-Sets.Derivatives
23:26:11Myhill-Nerode: theory Myhill-Nerode.Myhill_1
23:26:11Consensus_Refined: theory Stuttering_Equivalence.Samplers
23:26:11Consensus_Refined: theory Consensus_Refined.Ate_Proofs
23:26:11Old_Datatype_Show: theory Old_Datatype_Show.Old_Show
23:26:11VectorSpace: theory VectorSpace.FunctionLemmas
23:26:11VectorSpace: theory VectorSpace.RingModuleFacts
23:26:11Running Separata (on of2.proof.cit.tum.de) ...
23:26:11WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
23:26:11Consensus_Refined: theory Consensus_Refined.CT_Proofs
23:26:12Timing Free-Groups (2 threads, 182.284s elapsed time, 325.841s cpu time, 90.831s GC time, factor 1.79)
23:26:12Finished Free-Groups (0:03:05 elapsed time, 0:05:29 cpu time, factor 1.78)
23:26:12MiniML: theory MiniML.Instance
23:26:12Wetzels_Problem: theory HOL-Cardinals.Fun_More
23:26:12WorkerWrapper: theory WorkerWrapper.WorkerWrapper
23:26:12Wetzels_Problem: theory HOL-Cardinals.Order_Relation_More
23:26:12Running Random_Graph_Subgraph_Threshold (on of2.proof.cit.tum.de) ...
23:26:12Running ADS_Functor (on of2.proof.cit.tum.de) ...
23:26:12WorkerWrapper: theory WorkerWrapper.CounterExample
23:26:12WorkerWrapper: theory WorkerWrapper.Last
23:26:12Running Polynomial_Interpolation (on of2.proof.cit.tum.de) ...
23:26:12Wetzels_Problem: theory HOL-Cardinals.Order_Union
23:26:12Consensus_Refined: theory Consensus_Refined.New_Algorithm_Proofs
23:26:12MiniML: theory MiniML.Generalize
23:26:12Timing Selection_Heap_Sort (2 threads, 11.882s elapsed time, 21.989s cpu time, 1.910s GC time, factor 1.85)
23:26:12Finished Selection_Heap_Sort (0:00:17 elapsed time, 0:00:24 cpu time, factor 1.46)
23:26:12MiniML: theory MiniML.MiniML
23:26:12Nullstellensatz: theory Nullstellensatz.Nullstellensatz
23:26:12Possibilistic_Noninterference: theory Possibilistic_Noninterference.After_Execution
23:26:12Possibilistic_Noninterference: theory Possibilistic_Noninterference.Compositionality
23:26:12Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Generator
23:26:12Wetzels_Problem: theory HOL-Cardinals.Wellorder_Extension
23:26:12Consensus_Refined: theory Consensus_Refined.OneThirdRule_Proofs
23:26:12Wetzels_Problem: theory HOL-Cardinals.Wellfounded_More
23:26:12Wetzels_Problem: theory HOL-Cardinals.Wellorder_Relation
23:26:12WorkerWrapper: theory WorkerWrapper.Streams
23:26:13Valuation: theory Valuation.Valuation2
23:26:13Wetzels_Problem: theory HOL-Cardinals.Wellorder_Embedding
23:26:13VectorSpace: theory VectorSpace.MonoidSums
23:26:13Myhill-Nerode: theory Regular-Sets.NDerivative
23:26:13Consensus_Refined: theory Consensus_Refined.Paxos_Proofs
23:26:13Separata: theory HOL-Eisbach.Eisbach
23:26:13WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
23:26:13Separata: theory Separation_Algebra.Separation_Algebra
23:26:13ADS_Functor: theory ADS_Functor.Merkle_Interface
23:26:13Running Tycon (on of4.proof.cit.tum.de) ...
23:26:13Running Landau_Symbols (on of4.proof.cit.tum.de) ...
23:26:13Timing Separation_Algebra (2 threads, 55.257s elapsed time, 94.077s cpu time, 7.414s GC time, factor 1.70)
23:26:13WorkerWrapper: theory WorkerWrapper.Accumulator
23:26:13Finished Separation_Algebra (0:00:57 elapsed time, 0:01:36 cpu time, factor 1.68)
23:26:13Running Integration (on of4.proof.cit.tum.de) ...
23:26:13Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Instances
23:26:13Running Menger (on of4.proof.cit.tum.de) ...
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Unsorted
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Improved_Code_Equations
23:26:13Polynomial_Interpolation: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Divmod_Int
23:26:13MiniML: theory MiniML.W
23:26:13Consensus_Refined: theory Stuttering_Equivalence.StutterEquivalence
23:26:13Wetzels_Problem: theory HOL-Cardinals.Wellorder_Constructions
23:26:13Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
23:26:13Consensus_Refined: theory Heard_Of.Reduction
23:26:13VectorSpace: theory VectorSpace.LinearCombinations
23:26:13Separata: theory HOL-Eisbach.Eisbach_Tools
23:26:13Polynomial_Interpolation: theory Polynomial_Interpolation.Is_Rat_To_Rat
23:26:14Tycon: theory Tycon.TypeApp
23:26:14Tycon: theory Tycon.Coerce
23:26:14Menger: theory Menger.Helpers
23:26:14Menger: theory Menger.Graph
23:26:14WorkerWrapper: theory WorkerWrapper.Backtracking
23:26:14Separata: theory Separata.Separata
23:26:14Tycon: theory Tycon.Functor
23:26:14Landau_Symbols: theory Landau_Symbols.Group_Sort
23:26:14Integration: theory Integration.MonConv
23:26:14Integration: theory Integration.Sigma_Algebra
23:26:14Timing AxiomaticCategoryTheory (2 threads, 52.198s elapsed time, 48.670s cpu time, 4.257s GC time, factor 0.93)
23:26:14Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
23:26:14Myhill-Nerode: theory Myhill-Nerode.Myhill_2
23:26:14Finished AxiomaticCategoryTheory (0:00:54 elapsed time, 0:00:50 cpu time, factor 0.93)
23:26:14WorkerWrapper: theory WorkerWrapper.Continuations
23:26:14Wetzels_Problem: theory HOL-Cardinals.Cardinal_Order_Relation
23:26:14Integration: theory Integration.Measure
23:26:14Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Polynomial
23:26:14Menger: theory Menger.Separations
23:26:14ADS_Functor: theory ADS_Functor.ADS_Construction
23:26:14Old_Datatype_Show: theory Old_Datatype_Show.Old_Show_Examples
23:26:14ADS_Functor: theory ADS_Functor.Generic_ADS_Construction
23:26:14Menger: theory Menger.DisjointPaths
23:26:14Consensus_Refined: theory Consensus_Refined.BenOr_Proofs
23:26:14Consensus_Refined: theory Consensus_Refined.Uv_Proofs
23:26:14Integration: theory Integration.RealRandVar
23:26:14Wetzels_Problem: theory HOL-Cardinals.Ordinal_Arithmetic
23:26:15Myhill-Nerode: theory Myhill-Nerode.Myhill
23:26:15Menger: theory Menger.MengerInduction
23:26:15Myhill-Nerode: theory Myhill-Nerode.Closures
23:26:15Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
23:26:15Landau_Symbols: theory Landau_Symbols.Landau_Real_Products
23:26:15Tycon: theory Tycon.Monad
23:26:15Tycon: theory Tycon.Binary_Tree_Monad
23:26:15Tycon: theory Tycon.Lift_Monad
23:26:15Timing Actuarial_Mathematics (2 threads, 106.252s elapsed time, 172.446s cpu time, 7.577s GC time, factor 1.62)
23:26:15Tycon: theory Tycon.Writer_Monad
23:26:15Finished Actuarial_Mathematics (0:01:50 elapsed time, 0:02:56 cpu time, factor 1.60)
23:26:15Tycon: theory Tycon.Monad_Plus
23:26:15Wetzels_Problem: theory HOL-Cardinals.Cardinal_Arithmetic
23:26:15Integration: theory Integration.Failure
23:26:15Tycon: theory Tycon.Monad_Zero
23:26:15Tycon: theory Tycon.Writer_Transformer
23:26:15Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
23:26:15Integration: theory Integration.Integral
23:26:15Tycon: theory Tycon.Error_Monad
23:26:15Tycon: theory Tycon.Resumption_Transformer
23:26:15Tycon: theory Tycon.Monad_Zero_Plus
23:26:15Menger: theory Menger.Y_neq_new_last
23:26:15Menger: theory Menger.Y_eq_new_last
23:26:15Myhill-Nerode: theory Myhill-Nerode.Non_Regular_Languages
23:26:16Tycon: theory Tycon.Error_Transformer
23:26:16Myhill-Nerode: theory Regular-Sets.Relation_Interpretation
23:26:16Tycon: theory Tycon.Lazy_List_Monad
23:26:16Tycon: theory Tycon.Maybe_Monad
23:26:16Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
23:26:16Tycon: theory Tycon.State_Transformer
23:26:16Polynomial_Interpolation: theory Polynomial_Interpolation.Lagrange_Interpolation
23:26:16Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
23:26:16Menger: theory Menger.Menger
23:26:16Possibilistic_Noninterference: theory Possibilistic_Noninterference.Syntactic_Criteria
23:26:16Wetzels_Problem: theory HOL-Cardinals.Cardinals
23:26:16Tycon: theory Tycon.Monad_Transformer
23:26:16Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom_Poly
23:26:17WorkerWrapper: theory WorkerWrapper.Nub
23:26:17Valuation: theory Valuation.Valuation3
23:26:17Wetzels_Problem: theory ZFC_in_HOL.ZFC_Library
23:26:17WorkerWrapper: theory WorkerWrapper.UnboxedNats
23:26:17Timing Menger (6 threads, 3.204s elapsed time, 11.459s cpu time, 0.534s GC time, factor 3.58)
23:26:17Finished Menger (0:00:04 elapsed time, 0:00:12 cpu time, factor 2.95)
23:26:17Wetzels_Problem: theory ZFC_in_HOL.ZFC_in_HOL
23:26:18Landau_Symbols: theory Landau_Symbols.Landau_Simprocs
23:26:18Timing Treaps (2 threads, 65.644s elapsed time, 114.161s cpu time, 8.446s GC time, factor 1.74)
23:26:18Finished Treaps (0:01:09 elapsed time, 0:01:58 cpu time, factor 1.70)
23:26:18Possibilistic_Noninterference: theory Possibilistic_Noninterference.Concrete
23:26:18Landau_Symbols: theory Landau_Symbols.Landau_More
23:26:18Timing Separata (6 threads, 4.723s elapsed time, 15.179s cpu time, 0.637s GC time, factor 3.21)
23:26:18Polynomial_Interpolation: theory Polynomial_Interpolation.Newton_Interpolation
23:26:18Finished Separata (0:00:06 elapsed time, 0:00:16 cpu time, factor 2.71)
23:26:18Timing Tycon (6 threads, 3.899s elapsed time, 10.311s cpu time, 1.041s GC time, factor 2.64)
23:26:18Finished Tycon (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.28)
23:26:18Timing Integration (6 threads, 3.677s elapsed time, 8.027s cpu time, 0.333s GC time, factor 2.18)
23:26:18Finished Integration (0:00:04 elapsed time, 0:00:09 cpu time, factor 1.84)
23:26:18Myhill-Nerode: theory Regular-Sets.Equivalence_Checking
23:26:18Wetzels_Problem: theory ZFC_in_HOL.ZFC_Cardinals
23:26:18Timing Random_Graph_Subgraph_Threshold (6 threads, 4.867s elapsed time, 12.378s cpu time, 0.434s GC time, factor 2.54)
23:26:18Finished Random_Graph_Subgraph_Threshold (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.12)
23:26:19Myhill-Nerode: theory Regular-Sets.Regexp_Method
23:26:19Timing Randomised_BSTs (2 threads, 15.601s elapsed time, 28.597s cpu time, 1.192s GC time, factor 1.83)
23:26:19Finished Randomised_BSTs (0:00:19 elapsed time, 0:00:32 cpu time, factor 1.66)
23:26:19Timing Landau_Symbols (6 threads, 4.588s elapsed time, 10.658s cpu time, 0.828s GC time, factor 2.32)
23:26:19Finished Landau_Symbols (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.01)
23:26:19Myhill-Nerode: theory Well_Quasi_Orders.Almost_Full
23:26:19Polynomial_Interpolation: theory Polynomial_Interpolation.Polynomial_Interpolation
23:26:20Timing Noninterference_CSP (2 threads, 7.974s elapsed time, 13.356s cpu time, 1.458s GC time, factor 1.67)
23:26:20Finished Noninterference_CSP (0:00:23 elapsed time, 0:00:30 cpu time, factor 1.32)
23:26:20ADS_Functor: theory ADS_Functor.Inclusion_Proof_Construction
23:26:20Wetzels_Problem: theory ZFC_in_HOL.ZFC_Typeclasses
23:26:20VectorSpace: theory VectorSpace.SumSpaces
23:26:21Myhill-Nerode: theory Well_Quasi_Orders.Minimal_Bad_Sequences
23:26:21ADS_Functor: theory ADS_Functor.Canton_Transaction_Tree
23:26:21Myhill-Nerode: theory Well_Quasi_Orders.Almost_Full_Relations
23:26:21VectorSpace: theory VectorSpace.VectorSpace
23:26:21Timing MiniML (2 threads, 13.280s elapsed time, 17.140s cpu time, 1.263s GC time, factor 1.29)
23:26:21Finished MiniML (0:00:15 elapsed time, 0:00:19 cpu time, factor 1.23)
23:26:21Myhill-Nerode: theory Well_Quasi_Orders.Well_Quasi_Orders
23:26:21Timing Polynomial_Interpolation (6 threads, 8.079s elapsed time, 30.727s cpu time, 2.483s GC time, factor 3.80)
23:26:21Finished Polynomial_Interpolation (0:00:09 elapsed time, 0:00:32 cpu time, factor 3.39)
23:26:22Myhill-Nerode: theory Myhill-Nerode.Closures2
23:26:22Wetzels_Problem: theory ZFC_in_HOL.General_Cardinals
23:26:22Wetzels_Problem: theory Wetzels_Problem.Wetzels_Problem
23:26:23Timing Nullstellensatz (2 threads, 12.467s elapsed time, 17.504s cpu time, 1.251s GC time, factor 1.40)
23:26:23Finished Nullstellensatz (0:00:16 elapsed time, 0:00:21 cpu time, factor 1.28)
23:26:23Timing WorkerWrapper (2 threads, 14.682s elapsed time, 20.519s cpu time, 0.998s GC time, factor 1.40)
23:26:23Finished WorkerWrapper (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.34)
23:26:23Timing Old_Datatype_Show (2 threads, 11.963s elapsed time, 13.735s cpu time, 1.875s GC time, factor 1.15)
23:26:23Finished Old_Datatype_Show (0:00:15 elapsed time, 0:00:16 cpu time, factor 1.11)
23:26:24Timing ADS_Functor (6 threads, 10.564s elapsed time, 26.689s cpu time, 4.267s GC time, factor 2.53)
23:26:24Finished ADS_Functor (0:00:11 elapsed time, 0:00:28 cpu time, factor 2.37)
23:26:27Timing Koenigsberg_Friendship (2 threads, 75.071s elapsed time, 130.586s cpu time, 14.372s GC time, factor 1.74)
23:26:27Finished Koenigsberg_Friendship (0:01:18 elapsed time, 0:02:14 cpu time, factor 1.71)
23:26:30Timing Amortized_Complexity (2 threads, 96.931s elapsed time, 159.254s cpu time, 15.708s GC time, factor 1.64)
23:26:30Finished Amortized_Complexity (0:02:23 elapsed time, 0:03:39 cpu time, factor 1.53)
23:26:33Timing Generic_Deriving (2 threads, 74.098s elapsed time, 134.129s cpu time, 15.935s GC time, factor 1.81)
23:26:33Finished Generic_Deriving (0:01:17 elapsed time, 0:02:19 cpu time, factor 1.80)
23:26:34Timing BDD (2 threads, 81.542s elapsed time, 144.197s cpu time, 4.801s GC time, factor 1.77)
23:26:34Finished BDD (0:01:24 elapsed time, 0:02:26 cpu time, factor 1.75)
23:26:34Timing Knot_Theory (2 threads, 87.293s elapsed time, 162.650s cpu time, 11.368s GC time, factor 1.86)
23:26:34Finished Knot_Theory (0:01:30 elapsed time, 0:02:46 cpu time, factor 1.84)
23:26:40Running Lambda_Free_RPOs (on of1-proof+8-15) ...
23:26:41Running Forcing (on of1-proof+0-7) ...
23:26:41Forcing: theory Forcing.Utils
23:26:41Forcing: theory Forcing.Recursion_Thms
23:26:41Forcing: theory Forcing.Nat_Miscellanea
23:26:41Forcing: theory Forcing.Synthetic_Definition
23:26:41Forcing: theory Forcing.Forcing_Notions
23:26:41Forcing: theory Forcing.Internalizations
23:26:41Forcing: theory Forcing.Pointed_DC
23:26:41Forcing: theory Forcing.Relative_Univ
23:26:41Forcing: theory Forcing.Renaming
23:26:41Forcing: theory Forcing.Rasiowa_Sikorski
23:26:41Forcing: theory Forcing.Renaming_Auto
23:26:41Forcing: theory Forcing.Interface
23:26:42Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
23:26:42Lambda_Free_RPOs: theory Nested_Multisets_Ordinals.Multiset_More
23:26:42Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
23:26:42Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
23:26:42Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
23:26:42Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
23:26:42Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
23:26:42Running SC_DOM_Components (on of3.proof.cit.tum.de) ...
23:26:42Forcing: theory Forcing.Forcing_Data
23:26:42Forcing: theory Forcing.Separation_Rename
23:26:43Running Stern_Brocot (on of3.proof.cit.tum.de) ...
23:26:43Running LambdaMu (on of3.proof.cit.tum.de) ...
23:26:43Running CryptoBasedCompositionalProperties (on of3.proof.cit.tum.de) ...
23:26:43Forcing: theory Forcing.Internal_ZFC_Axioms
23:26:43Forcing: theory Forcing.Names
23:26:44LambdaMu: theory LambdaMu.Syntax
23:26:44Forcing: theory Forcing.Extensionality_Axiom
23:26:44CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.ListExtras
23:26:44Forcing: theory Forcing.Foundation_Axiom
23:26:44Forcing: theory Forcing.FrecR
23:26:44Forcing: theory Forcing.Least
23:26:44Forcing: theory Forcing.Pairing_Axiom
23:26:44Forcing: theory Forcing.Proper_Extension
23:26:44Forcing: theory Forcing.Union_Axiom
23:26:44CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy_types
23:26:44Running Lambda_Free_EPO (on 10.195.8.49) ...
23:26:44Running Huffman (on 10.195.8.49) ...
23:26:44Running Stellar_Quorums (on 10.195.8.49) ...
23:26:44Running Dedekind_Real (on 10.195.8.49) ...
23:26:44Stern_Brocot: theory Stern_Brocot.Cotree
23:26:44Forcing: theory Forcing.Arities
23:26:45Forcing: theory Forcing.Forces_Definition
23:26:45Forcing: theory Forcing.Succession_Poset
23:26:45Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
23:26:45Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
23:26:45Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
23:26:45LambdaMu: theory LambdaMu.Types
23:26:45LambdaMu: theory LambdaMu.DeBruijn
23:26:45LambdaMu: theory LambdaMu.Substitution
23:26:45LambdaMu: theory LambdaMu.Peirce
23:26:45LambdaMu: theory LambdaMu.Reduction
23:26:45LambdaMu: theory LambdaMu.ContextFacts
23:26:45LambdaMu: theory LambdaMu.TypePreservation
23:26:45LambdaMu: theory LambdaMu.Progress
23:26:45Running StrictOmegaCategories (on 10.195.8.32) ...
23:26:45Running Types_Tableaus_and_Goedels_God (on 10.195.8.32) ...
23:26:45CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.inout
23:26:45CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.Secrecy
23:26:45Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
23:26:46Dedekind_Real: theory Dedekind_Real.Dedekind_Real
23:26:46Stellar_Quorums: theory Stellar_Quorums.Stellar_Quorums
23:26:46Forcing: theory Forcing.Forcing_Theorems
23:26:46Huffman: theory Huffman.Huffman
23:26:46Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
23:26:46CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.CompLocalSecrets
23:26:46CryptoBasedCompositionalProperties: theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
23:26:46Forcing: theory Forcing.Separation_Axiom
23:26:46Forcing: theory Forcing.Ordinals_In_MG
23:26:46Forcing: theory Forcing.Infinity_Axiom
23:26:46Forcing: theory Forcing.Powerset_Axiom
23:26:46Forcing: theory Forcing.Replacement_Axiom
23:26:47Lambda_Free_EPO: theory HOL-Cardinals.Order_Union
23:26:47Lambda_Free_EPO: theory Nested_Multisets_Ordinals.Multiset_More
23:26:47SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
23:26:47Running IMO2019 (on 10.195.8.46) ...
23:26:47Forcing: theory Forcing.Choice_Axiom
23:26:47Running Impossible_Geometry (on 10.195.8.46) ...
23:26:47Timing LambdaMu (6 threads, 3.059s elapsed time, 6.900s cpu time, 0.294s GC time, factor 2.26)
23:26:47Finished LambdaMu (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.96)
23:26:47StrictOmegaCategories: theory HOL-Library.FuncSet
23:26:47Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.Relations
23:26:47Forcing: theory Forcing.Forcing_Main
23:26:48Timing Myhill-Nerode (2 threads, 44.911s elapsed time, 79.320s cpu time, 6.842s GC time, factor 1.77)
23:26:48Finished Myhill-Nerode (0:00:48 elapsed time, 0:01:23 cpu time, factor 1.72)
23:26:48Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension
23:26:48Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML
23:26:48Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util
23:26:48Timing CryptoBasedCompositionalProperties (6 threads, 3.614s elapsed time, 9.786s cpu time, 0.856s GC time, factor 2.71)
23:26:48Finished CryptoBasedCompositionalProperties (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.31)
23:26:48Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.AndersonProof
23:26:49Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
23:26:49Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.FittingProof
23:26:49Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
23:26:49StrictOmegaCategories: theory StrictOmegaCategories.Globular_Set
23:26:49Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
23:26:49Running InformationFlowSlicing (on 10.195.8.46) ...
23:26:49Types_Tableaus_and_Goedels_God: theory Types_Tableaus_and_Goedels_God.IHOML_Examples
23:26:49Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain
23:26:49Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders
23:26:49Timing Consensus_Refined (2 threads, 49.701s elapsed time, 92.429s cpu time, 8.300s GC time, factor 1.86)
23:26:49Finished Consensus_Refined (0:00:52 elapsed time, 0:01:35 cpu time, factor 1.83)
23:26:49Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term
23:26:50Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
23:26:50Running Orbit_Stabiliser (on 10.195.8.40) ...
23:26:50StrictOmegaCategories: theory StrictOmegaCategories.Strict_Omega_Category
23:26:50Timing Forcing (8 threads, 8.046s elapsed time, 49.012s cpu time, 2.805s GC time, factor 6.09)
23:26:50Finished Forcing (0:00:08 elapsed time, 0:00:49 cpu time, factor 5.73)
23:26:51Impossible_Geometry: theory Impossible_Geometry.Impossible_Geometry
23:26:51IMO2019: theory IMO2019.IMO2019_Q5
23:26:51IMO2019: theory IMO2019.IMO2019_Q1
23:26:51Running SumSquares (on 10.195.8.40) ...
23:26:51StrictOmegaCategories: theory StrictOmegaCategories.Pasting_Diagram
23:26:51IMO2019: theory IMO2019.IMO2019_Q4
23:26:51Timing Propositional_Logic_Class (2 threads, 47.821s elapsed time, 85.452s cpu time, 9.511s GC time, factor 1.79)
23:26:51Finished Propositional_Logic_Class (0:00:50 elapsed time, 0:01:28 cpu time, factor 1.76)
23:26:51Building Noninterference_Ipurge_Unwinding (on 10.195.8.40) ...
23:26:51Running Youngs_Inequality (on 10.195.8.40) ...
23:26:51InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
23:26:51Timing Lambda_Free_RPOs (8 threads, 9.064s elapsed time, 38.827s cpu time, 4.530s GC time, factor 4.28)
23:26:51Finished Lambda_Free_RPOs (0:00:10 elapsed time, 0:00:40 cpu time, factor 3.85)
23:26:52Running Concurrent_Ref_Alg (on 10.195.8.30) ...
23:26:52Timing Winding_Number_Eval (2 threads, 94.419s elapsed time, 180.905s cpu time, 13.384s GC time, factor 1.92)
23:26:52Finished Winding_Number_Eval (0:01:38 elapsed time, 0:03:05 cpu time, factor 1.88)
23:26:52SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
23:26:52Running Special_Function_Bounds (on 10.195.8.30) ...
23:26:52Running Van_der_Waerden (on 10.195.8.30) ...
23:26:52Noninterference_Ipurge_Unwinding: theory List_Interleaving.ListInterleaving
23:26:52InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
23:26:53Running VolpanoSmith (on 10.195.7.194) ...
23:26:53Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
23:26:53Running Budan_Fourier (on 10.195.7.194) ...
23:26:53Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings
23:26:53SumSquares: theory SumSquares.FourSquares
23:26:53SumSquares: theory SumSquares.TwoSquares
23:26:53Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Refinement_Lattice
23:26:53Running FOL_Seq_Calc1 (on 10.195.7.194) ...
23:26:53Youngs_Inequality: theory Youngs_Inequality.Youngs
23:26:54Van_der_Waerden: theory HOL-Library.FuncSet
23:26:54Van_der_Waerden: theory Van_der_Waerden.Digits
23:26:54Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
23:26:54InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
23:26:55Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
23:26:55Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
23:26:55Van_der_Waerden: theory Van_der_Waerden.Van_der_Waerden
23:26:55Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
23:26:55VolpanoSmith: theory VolpanoSmith.Semantics
23:26:55Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunction
23:26:55Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
23:26:55Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Galois_Connections
23:26:55Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Infimum_Nat
23:26:55Lambda_Free_EPO: theory Lambda_Free_EPO.Chop
23:26:55Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Parallel
23:26:55Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Sequential
23:26:55Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO
23:26:56Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.CRA
23:26:56Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Sequential
23:26:56Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
23:26:56Budan_Fourier: theory Sturm_Tarski.PolyMisc
23:26:56Running Architectural_Design_Patterns (on 10.195.8.11) ...
23:26:56Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Iteration
23:26:56Running Hood_Melville_Queue (on 10.195.8.11) ...
23:26:56FOL_Seq_Calc1: theory FOL_Seq_Calc1.Common
23:26:56FOL_Seq_Calc1: theory FOL_Seq_Calc1.Tableau
23:26:57SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
23:26:57Budan_Fourier: theory Sturm_Tarski.Sturm_Tarski
23:26:57Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
23:26:57Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
23:26:57Timing Possibilistic_Noninterference (2 threads, 52.705s elapsed time, 88.505s cpu time, 7.522s GC time, factor 1.68)
23:26:57Finished Possibilistic_Noninterference (0:00:55 elapsed time, 0:01:31 cpu time, factor 1.65)
23:26:57FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent
23:26:57Timing VectorSpace (2 threads, 45.484s elapsed time, 77.786s cpu time, 8.044s GC time, factor 1.71)
23:26:57Finished VectorSpace (0:00:49 elapsed time, 0:01:21 cpu time, factor 1.65)
23:26:57Timing Stellar_Quorums (2 threads, 10.951s elapsed time, 15.069s cpu time, 0.512s GC time, factor 1.38)
23:26:57Finished Stellar_Quorums (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.29)
23:26:57Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
23:26:57Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Conjunctive_Iteration
23:26:59Running Public_Announcement_Logic (on 10.195.8.42) ...
23:26:59Running List_Inversions (on 10.195.8.42) ...
23:26:59Running Case_Labeling (on 10.195.8.42) ...
23:26:59Running Banach_Steinhaus (on 10.195.8.42) ...
23:26:59Running Stream-Fusion (on 10.195.8.42) ...
23:26:59Hood_Melville_Queue: theory HOL-Data_Structures.Queue_Spec
23:26:59FOL_Seq_Calc1: theory FOL_Seq_Calc1.Sequent2
23:26:59Hood_Melville_Queue: theory Hood_Melville_Queue.Hood_Melville_Queue
23:26:59Concurrent_Ref_Alg: theory Concurrent_Ref_Alg.Rely_Quotient
23:26:59Timing Huffman (2 threads, 11.708s elapsed time, 19.078s cpu time, 0.634s GC time, factor 1.63)
23:26:59Finished Huffman (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.52)
23:26:59Timing Dedekind_Real (2 threads, 11.846s elapsed time, 15.914s cpu time, 0.277s GC time, factor 1.34)
23:26:59Finished Dedekind_Real (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.27)
23:26:59PAC_Checker: theory PAC_Checker.PAC_Checker_MLton
23:27:00Budan_Fourier: theory Budan_Fourier.BF_Misc
23:27:00Running Rank_Nullity_Theorem (on 10.195.8.29) ...
23:27:00Running Derangements (on 10.195.8.29) ...
23:27:00Case_Labeling: theory HOL-Eisbach.Eisbach
23:27:00Running Binomial-Queues (on 10.195.8.29) ...
23:27:00Case_Labeling: theory Case_Labeling.Case_Labeling
23:27:00Stern_Brocot: theory Stern_Brocot.Bird_Tree
23:27:00Architectural_Design_Patterns: theory Architectural_Design_Patterns.Auxiliary
23:27:00Public_Announcement_Logic: theory Public_Announcement_Logic.PAL
23:27:00Architectural_Design_Patterns: theory Architectural_Design_Patterns.Singleton
23:27:00List_Inversions: theory HOL-Combinatorics.Transposition
23:27:00List_Inversions: theory HOL-Library.Cancellation
23:27:00Architectural_Design_Patterns: theory Architectural_Design_Patterns.RF_LTL
23:27:00Stream-Fusion: theory HOLCF-Library.Int_Discrete
23:27:01List_Inversions: theory HOL-Library.FuncSet
23:27:01Running XML (on of2.proof.cit.tum.de) ...
23:27:01Running BNF_CC (on of2.proof.cit.tum.de) ...
23:27:01Running Tree_Decomposition (on of2.proof.cit.tum.de) ...
23:27:01Timing StrictOmegaCategories (2 threads, 12.044s elapsed time, 21.628s cpu time, 0.994s GC time, factor 1.80)
23:27:01Finished StrictOmegaCategories (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.66)
23:27:01Stream-Fusion: theory Stream-Fusion.LazyList
23:27:01Architectural_Design_Patterns: theory Architectural_Design_Patterns.Publisher_Subscriber
23:27:01VolpanoSmith: theory VolpanoSmith.secTypes
23:27:01Running Saturation_Framework_Extensions (on of2.proof.cit.tum.de) ...
23:27:01Budan_Fourier: theory Budan_Fourier.Budan_Fourier
23:27:01Case_Labeling: theory HOL-Hoare.Arith2
23:27:01Budan_Fourier: theory Budan_Fourier.Sturm_Multiple_Roots
23:27:01List_Inversions: theory HOL-Library.Multiset
23:27:01Timing Stern_Brocot (6 threads, 15.271s elapsed time, 29.225s cpu time, 4.243s GC time, factor 1.91)
23:27:01Finished Stern_Brocot (0:00:17 elapsed time, 0:00:31 cpu time, factor 1.85)
23:27:01Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus_Missing
23:27:01Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blockchain
23:27:01BNF_CC: theory HOL-Library.BNF_Axiomatization
23:27:01BNF_CC: theory BNF_CC.Preliminaries
23:27:01BNF_CC: theory HOL-Library.Old_Datatype
23:27:01BNF_CC: theory HOL-Library.Phantom_Type
23:27:01BNF_CC: theory HOL-Library.Nat_Bijection
23:27:01BNF_CC: theory HOL-Library.Rewrite
23:27:01Derangements: theory HOL-Library.Cancellation
23:27:01Case_Labeling: theory HOL-Hoare.Hoare_Syntax
23:27:01Case_Labeling: theory HOL-Hoare.Hoare_Tac
23:27:02List_Inversions: theory HOL-Library.Disjoint_Sets
23:27:02Derangements: theory HOL-Combinatorics.Transposition
23:27:02Running Two_Generated_Word_Monoids_Intersection (on of4.proof.cit.tum.de) ...
23:27:02Tree_Decomposition: theory Tree_Decomposition.Graph
23:27:02Running OpSets (on of4.proof.cit.tum.de) ...
23:27:02Binomial-Queues: theory Binomial-Queues.PQ
23:27:02Budan_Fourier: theory Budan_Fourier.Descartes_Roots_Test
23:27:02Running Fishburn_Impossibility (on of4.proof.cit.tum.de) ...
23:27:02Running MonoBoolTranAlgebra (on of4.proof.cit.tum.de) ...
23:27:02XML: theory Deriving.Derive_Manager
23:27:02BNF_CC: theory BNF_CC.Axiomatised_BNF_CC
23:27:02XML: theory Certification_Monads.Error_Syntax
23:27:02XML: theory Partial_Function_MR.Partial_Function_MR
23:27:02XML: theory Deriving.Generator_Aux
23:27:02XML: theory Certification_Monads.Error_Monad
23:27:02Derangements: theory HOL-Library.FuncSet
23:27:02Timing Relational_Minimum_Spanning_Trees (2 threads, 98.779s elapsed time, 161.596s cpu time, 14.597s GC time, factor 1.64)
23:27:02BNF_CC: theory HOL-Library.Countable
23:27:02Finished Relational_Minimum_Spanning_Trees (0:01:41 elapsed time, 0:02:44 cpu time, factor 1.62)
23:27:02BNF_CC: theory HOL-Library.Cardinality
23:27:02XML: theory Certification_Monads.Strict_Sum
23:27:02Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Soundness
23:27:02Stream-Fusion: theory Stream-Fusion.Stream
23:27:02Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
23:27:02XML: theory Show.Show
23:27:02Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited
23:27:02Case_Labeling: theory Case_Labeling.Conditionals
23:27:02Binomial-Queues: theory Binomial-Queues.Binomial_Queue
23:27:02VolpanoSmith: theory VolpanoSmith.Execute
23:27:02Tree_Decomposition: theory Tree_Decomposition.Tree
23:27:02OpSets: theory OpSets.OpSet
23:27:02Fishburn_Impossibility: theory HOL-Combinatorics.Transposition
23:27:02Fishburn_Impossibility: theory HOL-Library.Cancellation
23:27:02Timing Impossible_Geometry (2 threads, 10.999s elapsed time, 17.144s cpu time, 1.286s GC time, factor 1.56)
23:27:02Fishburn_Impossibility: theory HOL-Library.FuncSet
23:27:02Finished Impossible_Geometry (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.46)
23:27:02MonoBoolTranAlgebra: theory LatticeProperties.WellFoundedTransitive
23:27:02Fishburn_Impossibility: theory List-Index.List_Index
23:27:02Two_Generated_Word_Monoids_Intersection: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
23:27:02MonoBoolTranAlgebra: theory LatticeProperties.Conj_Disj
23:27:03Banach_Steinhaus: theory Banach_Steinhaus.Banach_Steinhaus
23:27:03Derangements: theory HOL-Library.Multiset
23:27:03Tree_Decomposition: theory Tree_Decomposition.TreeDecomposition
23:27:03Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
23:27:03Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
23:27:03Derangements: theory HOL-Library.Disjoint_Sets
23:27:03BNF_CC: theory BNF_CC.Concrete_Examples
23:27:03Case_Labeling: theory Case_Labeling.Monadic_Language
23:27:03MonoBoolTranAlgebra: theory LatticeProperties.Complete_Lattice_Prop
23:27:03OpSets: theory OpSets.Insert_Spec
23:27:03Fishburn_Impossibility: theory HOL-Library.Multiset
23:27:03Fishburn_Impossibility: theory HOL-Library.Disjoint_Sets
23:27:03BNF_CC: theory BNF_CC.Composition
23:27:03Tree_Decomposition: theory Tree_Decomposition.TreewidthCompleteGraph
23:27:03BNF_CC: theory BNF_CC.Fixpoints
23:27:03Tree_Decomposition: theory Tree_Decomposition.TreewidthTree
23:27:03Tree_Decomposition: theory Tree_Decomposition.ExampleInstantiations
23:27:03BNF_CC: theory BNF_CC.Quotient_Preservation
23:27:03BNF_CC: theory BNF_CC.Subtypes
23:27:03BNF_CC: theory HOL-Library.FSet
23:27:03MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran
23:27:03Two_Generated_Word_Monoids_Intersection: theory Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection
23:27:03XML: theory Certification_Monads.Parser_Monad
23:27:03Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Clausal_Calculus
23:27:04Timing IMO2019 (2 threads, 11.235s elapsed time, 14.050s cpu time, 0.887s GC time, factor 1.25)
23:27:04OpSets: theory OpSets.Interleaving
23:27:04Finished IMO2019 (0:00:14 elapsed time, 0:00:17 cpu time, factor 1.18)
23:27:04OpSets: theory OpSets.List_Spec
23:27:04OpSets: theory OpSets.RGA
23:27:04Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
23:27:04Timing InformationFlowSlicing (2 threads, 11.114s elapsed time, 19.158s cpu time, 0.949s GC time, factor 1.72)
23:27:04Finished InformationFlowSlicing (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.55)
23:27:04MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
23:27:04Case_Labeling: theory HOL-Hoare.Hoare_Logic
23:27:04Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited
23:27:04XML: theory XML.Xml
23:27:05SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
23:27:05Stream-Fusion: theory Stream-Fusion.StreamFusion
23:27:05Binomial-Queues: theory Binomial-Queues.PQ_Implementation
23:27:05Timing DiscretePricing (2 threads, 114.752s elapsed time, 199.101s cpu time, 12.621s GC time, factor 1.74)
23:27:05Finished DiscretePricing (0:01:58 elapsed time, 0:03:23 cpu time, factor 1.71)
23:27:05Timing Tree_Decomposition (6 threads, 3.018s elapsed time, 9.172s cpu time, 0.403s GC time, factor 3.04)
23:27:05Finished Tree_Decomposition (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.58)
23:27:05Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blackboard
23:27:05Timing SumSquares (2 threads, 10.366s elapsed time, 17.262s cpu time, 0.557s GC time, factor 1.67)
23:27:05Finished SumSquares (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.49)
23:27:06BNF_CC: theory BNF_CC.Operation_Examples
23:27:06Case_Labeling: theory Case_Labeling.Labeled_Hoare
23:27:06BNF_CC: theory BNF_CC.DDS
23:27:07Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples
23:27:07Timing Orbit_Stabiliser (2 threads, 12.064s elapsed time, 17.282s cpu time, 1.161s GC time, factor 1.43)
23:27:07Finished Orbit_Stabiliser (0:00:15 elapsed time, 0:00:20 cpu time, factor 1.34)
23:27:07Timing Youngs_Inequality (2 threads, 11.752s elapsed time, 18.792s cpu time, 0.628s GC time, factor 1.60)
23:27:07Finished Youngs_Inequality (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.44)
23:27:07Timing Van_der_Waerden (2 threads, 11.715s elapsed time, 22.465s cpu time, 0.802s GC time, factor 1.92)
23:27:07Finished Van_der_Waerden (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.77)
23:27:07Case_Labeling: theory Case_Labeling.Case_Labeling_Examples
23:27:07XML: theory XML.Xmlt
23:27:07Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
23:27:07Timing VolpanoSmith (2 threads, 10.796s elapsed time, 17.954s cpu time, 1.518s GC time, factor 1.66)
23:27:07Finished VolpanoSmith (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.54)
23:27:08Fishburn_Impossibility: theory HOL-Combinatorics.Permutations
23:27:08MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Assertion_Algebra
23:27:08MonoBoolTranAlgebra: theory MonoBoolTranAlgebra.Statements
23:27:08List_Inversions: theory HOL-Combinatorics.Permutations
23:27:08Timing FOL_Seq_Calc1 (2 threads, 10.435s elapsed time, 16.788s cpu time, 0.503s GC time, factor 1.61)
23:27:08Finished FOL_Seq_Calc1 (0:00:13 elapsed time, 0:00:19 cpu time, factor 1.45)
23:27:08Derangements: theory HOL-Combinatorics.Permutations
23:27:08Fishburn_Impossibility: theory Randomised_Social_Choice.Order_Predicates
23:27:09Timing Concurrent_Ref_Alg (2 threads, 13.744s elapsed time, 23.553s cpu time, 1.909s GC time, factor 1.71)
23:27:09Finished Concurrent_Ref_Alg (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.61)
23:27:09Fishburn_Impossibility: theory Randomised_Social_Choice.Preference_Profiles
23:27:09Timing BNF_CC (6 threads, 6.734s elapsed time, 26.572s cpu time, 3.212s GC time, factor 3.95)
23:27:09Finished BNF_CC (0:00:07 elapsed time, 0:00:27 cpu time, factor 3.58)
23:27:09Timing MonoBoolTranAlgebra (6 threads, 6.081s elapsed time, 9.783s cpu time, 0.420s GC time, factor 1.61)
23:27:09Finished MonoBoolTranAlgebra (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.51)
23:27:09Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
23:27:09Fishburn_Impossibility: theory Randomised_Social_Choice.Elections
23:27:09Fishburn_Impossibility: theory Randomised_Social_Choice.Preference_Profile_Cmd
23:27:09Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
23:27:10Fishburn_Impossibility: theory Fishburn_Impossibility.Social_Choice_Functions
23:27:10Derangements: theory Derangements.Derangements
23:27:10List_Inversions: theory List_Inversions.List_Inversions
23:27:10Fishburn_Impossibility: theory Fishburn_Impossibility.Fishburn_Impossibility
23:27:10Timing OpSets (6 threads, 7.207s elapsed time, 28.295s cpu time, 1.398s GC time, factor 3.93)
23:27:10Finished OpSets (0:00:08 elapsed time, 0:00:29 cpu time, factor 3.56)
23:27:10Timing Saturation_Framework_Extensions (6 threads, 7.607s elapsed time, 21.508s cpu time, 1.499s GC time, factor 2.83)
23:27:10Finished Saturation_Framework_Extensions (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.51)
23:27:11Timing Public_Announcement_Logic (2 threads, 10.283s elapsed time, 14.551s cpu time, 1.286s GC time, factor 1.42)
23:27:11Finished Public_Announcement_Logic (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.34)
23:27:12Timing Valuation (2 threads, 61.762s elapsed time, 100.111s cpu time, 6.940s GC time, factor 1.62)
23:27:12Finished Valuation (0:01:04 elapsed time, 0:01:43 cpu time, factor 1.59)
23:27:12Timing Binomial-Queues (2 threads, 9.601s elapsed time, 15.492s cpu time, 1.309s GC time, factor 1.61)
23:27:12Finished Binomial-Queues (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.49)
23:27:12Timing Stream-Fusion (2 threads, 11.081s elapsed time, 12.582s cpu time, 0.524s GC time, factor 1.14)
23:27:12Finished Stream-Fusion (0:00:13 elapsed time, 0:00:14 cpu time, factor 1.11)
23:27:12Timing XML (6 threads, 9.747s elapsed time, 19.116s cpu time, 2.428s GC time, factor 1.96)
23:27:12Finished XML (0:00:11 elapsed time, 0:00:21 cpu time, factor 1.88)
23:27:12Timing Banach_Steinhaus (2 threads, 10.340s elapsed time, 16.869s cpu time, 0.476s GC time, factor 1.63)
23:27:12Finished Banach_Steinhaus (0:00:13 elapsed time, 0:00:19 cpu time, factor 1.46)
23:27:13Timing Fishburn_Impossibility (6 threads, 10.138s elapsed time, 43.031s cpu time, 3.975s GC time, factor 4.24)
23:27:13Finished Fishburn_Impossibility (0:00:11 elapsed time, 0:00:44 cpu time, factor 3.96)
23:27:13Timing Case_Labeling (2 threads, 12.450s elapsed time, 22.812s cpu time, 1.461s GC time, factor 1.83)
23:27:13Finished Case_Labeling (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.72)
23:27:14Timing Rank_Nullity_Theorem (2 threads, 10.624s elapsed time, 15.884s cpu time, 0.803s GC time, factor 1.50)
23:27:14Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.35)
23:27:14Timing Types_Tableaus_and_Goedels_God (2 threads, 25.547s elapsed time, 20.722s cpu time, 0.688s GC time, factor 0.81)
23:27:14Finished Types_Tableaus_and_Goedels_God (0:00:27 elapsed time, 0:00:22 cpu time, factor 0.82)
23:27:14Timing Two_Generated_Word_Monoids_Intersection (6 threads, 11.336s elapsed time, 15.613s cpu time, 2.204s GC time, factor 1.38)
23:27:14Finished Two_Generated_Word_Monoids_Intersection (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.34)
23:27:22Timing Noninterference_Ipurge_Unwinding (2 threads, 10.009s elapsed time, 16.527s cpu time, 1.415s GC time, factor 1.65)
23:27:22Finished Noninterference_Ipurge_Unwinding (0:00:29 elapsed time, 0:00:38 cpu time, factor 1.30)
23:27:22Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
23:27:27Running Cayley_Hamilton (on of1-proof+8-15) ...
23:27:27Running Finitely_Generated_Abelian_Groups (on of1-proof+0-7) ...
23:27:28Running Zeckendorf (on of3.proof.cit.tum.de) ...
23:27:28Running Combinatorial_Enumeration_Algorithms (on of3.proof.cit.tum.de) ...
23:27:28Running GPU_Kernel_PL (on of3.proof.cit.tum.de) ...
23:27:28Cayley_Hamilton: theory HOL-Library.More_List
23:27:28Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
23:27:28Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
23:27:28Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
23:27:28Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
23:27:28Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Hom
23:27:28Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
23:27:29Timing Wetzels_Problem (2 threads, 75.658s elapsed time, 130.992s cpu time, 11.797s GC time, factor 1.73)
23:27:29Finished Wetzels_Problem (0:01:19 elapsed time, 0:02:15 cpu time, factor 1.69)
23:27:29Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
23:27:29GPU_Kernel_PL: theory GPU_Kernel_PL.Misc
23:27:29GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax
23:27:29Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
23:27:29Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.IDirProds
23:27:30Combinatorial_Enumeration_Algorithms: theory HOL-Eisbach.Eisbach
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Filter_Bool_List
23:27:30Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Stirling
23:27:30Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Transposition
23:27:30Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Additions_to_Main
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Common_Lemmas
23:27:30Zeckendorf: theory Zeckendorf.Zeckendorf
23:27:30Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Number_Partition
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Integer_Compositions
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Sequences
23:27:30Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Permutations
23:27:30Combinatorial_Enumeration_Algorithms: theory Card_Number_Partitions.Card_Number_Partitions
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Powerset
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Trees
23:27:30Combinatorial_Enumeration_Algorithms: theory Discrete_Summation.Factorials
23:27:30Running Szemeredi_Regularity (on 10.195.8.49) ...
23:27:30Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Integer_Partitions
23:27:30Combinatorial_Enumeration_Algorithms: theory Card_Partitions.Injectivity_Solver
23:27:30Running Combinatorics_Words_Lyndon (on 10.195.8.49) ...
23:27:30Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
23:27:31Running Secondary_Sylow (on 10.195.8.49) ...
23:27:31Combinatorial_Enumeration_Algorithms: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
23:27:31Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.DirProds
23:27:31Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Group_Relations
23:27:31Combinatorial_Enumeration_Algorithms: theory HOL-Combinatorics.Multiset_Permutations
23:27:31Finitely_Generated_Abelian_Groups: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
23:27:32GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state
23:27:32GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness
23:27:32Timing List_Inversions (2 threads, 31.159s elapsed time, 55.898s cpu time, 4.153s GC time, factor 1.79)
23:27:32Finished List_Inversions (0:00:33 elapsed time, 0:00:58 cpu time, factor 1.74)
23:27:32Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Derangements_Enum
23:27:32Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Weak_Integer_Compositions
23:27:32Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon
23:27:32Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Permutations
23:27:32Combinatorics_Words_Lyndon: theory Szpilrajn.Szpilrajn
23:27:32Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.n_Subsets
23:27:32Timing Budan_Fourier (2 threads, 34.571s elapsed time, 63.320s cpu time, 4.396s GC time, factor 1.83)
23:27:32Finished Budan_Fourier (0:00:37 elapsed time, 0:01:06 cpu time, factor 1.76)
23:27:32GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread
23:27:32Timing Derangements (2 threads, 30.307s elapsed time, 55.792s cpu time, 5.606s GC time, factor 1.84)
23:27:32Finished Derangements (0:00:32 elapsed time, 0:00:57 cpu time, factor 1.79)
23:27:33Running Stream_Fusion_Code (on 10.195.8.32) ...
23:27:33Running Finite_Automata_HF (on 10.195.8.32) ...
23:27:33Running Hahn_Jordan_Decomposition (on 10.195.8.32) ...
23:27:33Running Category (on 10.195.8.32) ...
23:27:33Running Matroids (on 10.195.8.32) ...
23:27:33Timing Zeckendorf (6 threads, 2.796s elapsed time, 9.040s cpu time, 0.187s GC time, factor 3.23)
23:27:33Finished Zeckendorf (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.37)
23:27:33Combinatorial_Enumeration_Algorithms: theory Combinatorial_Enumeration_Algorithms.Combinatorial_Enumeration_Algorithms
23:27:33Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
23:27:34GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group
23:27:34Szemeredi_Regularity: theory Szemeredi_Regularity.Szemeredi
23:27:34GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel
23:27:34Running LP_Duality (on 10.195.8.46) ...
23:27:34Finite_Automata_HF: theory Regular-Sets.Regular_Set
23:27:34Finite_Automata_HF: theory HOL-Library.Nat_Bijection
23:27:34Running Tail_Recursive_Functions (on 10.195.8.46) ...
23:27:34Category: theory HOL-Library.FuncSet
23:27:34Running Latin_Square (on 10.195.8.46) ...
23:27:34Matroids: theory Matroids.Indep_System
23:27:34Running Fixed_Length_Vector (on 10.195.8.46) ...
23:27:34Timing Cayley_Hamilton (8 threads, 5.620s elapsed time, 23.288s cpu time, 2.338s GC time, factor 4.14)
23:27:34Finished Cayley_Hamilton (0:00:07 elapsed time, 0:00:25 cpu time, factor 3.46)
23:27:35GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language
23:27:35Finite_Automata_HF: theory HereditarilyFinite.HF
23:27:35Timing Finitely_Generated_Abelian_Groups (8 threads, 5.947s elapsed time, 25.710s cpu time, 2.858s GC time, factor 4.32)
23:27:35Finished Finitely_Generated_Abelian_Groups (0:00:07 elapsed time, 0:00:27 cpu time, factor 3.63)
23:27:36Matroids: theory Matroids.Matroid
23:27:36Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion
23:27:36Running SenSocialChoice (on 10.195.8.40) ...
23:27:36Category: theory Category.Cat
23:27:36Combinatorics_Words_Lyndon: theory Combinatorics_Words_Lyndon.Lyndon_Addition
23:27:36Running Falling_Factorial_Sum (on 10.195.8.40) ...
23:27:36Running TortoiseHare (on 10.195.8.40) ...
23:27:36Timing GPU_Kernel_PL (6 threads, 5.982s elapsed time, 8.852s cpu time, 1.131s GC time, factor 1.48)
23:27:36Running CISC-Kernel (on 10.195.8.40) ...
23:27:36Finished GPU_Kernel_PL (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.41)
23:27:36Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List
23:27:36Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl
23:27:36Latin_Square: theory Marriage.Marriage
23:27:36Fixed_Length_Vector: theory HOL-Library.Phantom_Type
23:27:36Latin_Square: theory Latin_Square.Latin_Square
23:27:37Category: theory Category.Functors
23:27:37Category: theory Category.SetCat
23:27:37Timing Combinatorial_Enumeration_Algorithms (6 threads, 6.683s elapsed time, 31.816s cpu time, 1.336s GC time, factor 4.76)
23:27:37Finished Combinatorial_Enumeration_Algorithms (0:00:08 elapsed time, 0:00:33 cpu time, factor 4.12)
23:27:37Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims
23:27:37Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
23:27:37Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
23:27:37Finite_Automata_HF: theory HereditarilyFinite.Ordinal
23:27:37Fixed_Length_Vector: theory HOL-Library.Cardinality
23:27:38SenSocialChoice: theory SenSocialChoice.FSext
23:27:38CISC-Kernel: theory CISC-Kernel.Option_Binders
23:27:38CISC-Kernel: theory CISC-Kernel.List_Theorems
23:27:38Category: theory Category.NatTrans
23:27:38CISC-Kernel: theory CISC-Kernel.Step_configuration
23:27:38SenSocialChoice: theory SenSocialChoice.RPRs
23:27:38Category: theory Category.HomFunctors
23:27:38CISC-Kernel: theory CISC-Kernel.K
23:27:38SenSocialChoice: theory SenSocialChoice.SCFs
23:27:38Falling_Factorial_Sum: theory HOL-Combinatorics.Stirling
23:27:38Falling_Factorial_Sum: theory HOL-Eisbach.Eisbach
23:27:39TortoiseHare: theory TortoiseHare.Basis
23:27:39Category: theory Category.Yoneda
23:27:39Fixed_Length_Vector: theory HOL-Library.Code_Cardinality
23:27:39Fixed_Length_Vector: theory HOL-Library.Numeral_Type
23:27:39Timing Lambda_Free_EPO (2 threads, 49.997s elapsed time, 93.867s cpu time, 6.991s GC time, factor 1.88)
23:27:39Finished Lambda_Free_EPO (0:00:53 elapsed time, 0:01:37 cpu time, factor 1.83)
23:27:39SenSocialChoice: theory SenSocialChoice.Arrow
23:27:39LP_Duality: theory LP_Duality.Minimum_Maximum
23:27:39Finite_Automata_HF: theory Regular-Sets.Regular_Exp
23:27:39Running Floyd_Warshall (on 10.195.8.30) ...
23:27:39CISC-Kernel: theory CISC-Kernel.SK
23:27:39Running FLP (on 10.195.8.30) ...
23:27:39Falling_Factorial_Sum: theory Discrete_Summation.Factorials
23:27:39Running Maximum_Segment_Sum (on 10.195.8.30) ...
23:27:39Running FinFun (on 10.195.8.30) ...
23:27:39Secondary_Sylow: theory Secondary_Sylow.GroupAction
23:27:39SenSocialChoice: theory SenSocialChoice.May
23:27:39LP_Duality: theory LP_Duality.LP_Duality
23:27:39CISC-Kernel: theory CISC-Kernel.Step_policies
23:27:40TortoiseHare: theory TortoiseHare.Brent
23:27:40Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
23:27:40CISC-Kernel: theory CISC-Kernel.Step
23:27:40TortoiseHare: theory TortoiseHare.TortoiseHare
23:27:40SenSocialChoice: theory SenSocialChoice.Sen
23:27:40Fixed_Length_Vector: theory Fixed_Length_Vector.Fixed_Length_Vector
23:27:40CISC-Kernel: theory CISC-Kernel.ISK
23:27:40Running Arith_Prog_Rel_Primes (on 10.195.7.194) ...
23:27:41Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
23:27:41Running Partial_Function_MR (on 10.195.7.194) ...
23:27:41Timing Combinatorics_Words_Lyndon (2 threads, 7.648s elapsed time, 13.639s cpu time, 0.637s GC time, factor 1.78)
23:27:41Finished Combinatorics_Words_Lyndon (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.59)
23:27:41Maximum_Segment_Sum: theory Maximum_Segment_Sum.Maximum_Segment_Sum
23:27:41Secondary_Sylow: theory Secondary_Sylow.SndSylow
23:27:41FLP: theory FLP.ListUtilities
23:27:41Falling_Factorial_Sum: theory Card_Partitions.Injectivity_Solver
23:27:41FLP: theory FLP.Multiset
23:27:41FinFun: theory HOL-Library.Phantom_Type
23:27:41Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction
23:27:41Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde
23:27:41FLP: theory FLP.AsynchronousSystem
23:27:41CISC-Kernel: theory CISC-Kernel.CISK
23:27:41Falling_Factorial_Sum: theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics
23:27:42Hahn_Jordan_Decomposition: theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
23:27:42Running GaleStewart_Games (on 10.195.7.194) ...
23:27:42Running Quaternions (on 10.195.7.194) ...
23:27:42FinFun: theory HOL-Library.Cardinality
23:27:43Floyd_Warshall: theory Floyd_Warshall.Recursion_Combinators
23:27:43Floyd_Warshall: theory Floyd_Warshall.Floyd_Warshall
23:27:43Running Certification_Monads (on 10.195.8.11) ...
23:27:43Running Sunflowers (on 10.195.8.11) ...
23:27:43Timing Szemeredi_Regularity (2 threads, 8.692s elapsed time, 13.558s cpu time, 0.494s GC time, factor 1.56)
23:27:43Finished Szemeredi_Regularity (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.38)
23:27:43Arith_Prog_Rel_Primes: theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes
23:27:43Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
23:27:43Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
23:27:44Timing Category (2 threads, 8.374s elapsed time, 13.413s cpu time, 0.643s GC time, factor 1.60)
23:27:44Finished Category (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.46)
23:27:44GaleStewart_Games: theory GaleStewart_Games.MoreCoinductiveList2
23:27:44Partial_Function_MR: theory HOL-Library.Monad_Syntax
23:27:44FinFun: theory FinFun.FinFun
23:27:44Finite_Automata_HF: theory Finite_Automata_HF.Finite_Automata_HF
23:27:44GaleStewart_Games: theory GaleStewart_Games.MoreENat
23:27:44Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
23:27:44Timing Special_Function_Bounds (2 threads, 47.815s elapsed time, 75.993s cpu time, 5.446s GC time, factor 1.59)
23:27:44Finished Special_Function_Bounds (0:00:51 elapsed time, 0:01:19 cpu time, factor 1.54)
23:27:44Running GoedelGod (on 10.195.8.42) ...
23:27:44Timing Matroids (2 threads, 8.893s elapsed time, 12.349s cpu time, 0.327s GC time, factor 1.39)
23:27:44Finished Matroids (0:00:10 elapsed time, 0:00:14 cpu time, factor 1.29)
23:27:44Running Sliding_Window_Algorithm (on 10.195.8.42) ...
23:27:44Running Prefix_Free_Code_Combinators (on 10.195.8.42) ...
23:27:44Running Birkhoff_Finite_Distributive_Lattices (on 10.195.8.42) ...
23:27:44GaleStewart_Games: theory GaleStewart_Games.MorePrefix
23:27:44Timing Architectural_Design_Patterns (2 threads, 42.992s elapsed time, 74.333s cpu time, 8.393s GC time, factor 1.73)
23:27:44Finished Architectural_Design_Patterns (0:00:46 elapsed time, 0:01:18 cpu time, factor 1.68)
23:27:45Certification_Monads: theory Certification_Monads.Misc
23:27:45Quaternions: theory Quaternions.Quaternions
23:27:45Certification_Monads: theory Deriving.Derive_Manager
23:27:45CISC-Kernel: theory CISC-Kernel.Step_invariants
23:27:45Sunflowers: theory HOL-Library.FuncSet
23:27:45Certification_Monads: theory Deriving.Generator_Aux
23:27:45Certification_Monads: theory HOL-Library.Adhoc_Overloading
23:27:45CISC-Kernel: theory CISC-Kernel.Step_vpeq
23:27:45CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects
23:27:45CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent
23:27:45Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList
23:27:45FLP: theory FLP.Execution
23:27:45Running Strong_Security (on 10.195.8.29) ...
23:27:45CISC-Kernel: theory CISC-Kernel.Separation_kernel_model
23:27:45Certification_Monads: theory Certification_Monads.Error_Syntax
23:27:45Timing Latin_Square (2 threads, 8.812s elapsed time, 16.092s cpu time, 0.485s GC time, factor 1.83)
23:27:46Running Transitive-Closure (on 10.195.8.29) ...
23:27:46Finished Latin_Square (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.64)
23:27:46Running Chord_Segments (on 10.195.8.29) ...
23:27:46FinFun: theory FinFun.FinFunPred
23:27:46Timing Tail_Recursive_Functions (2 threads, 7.845s elapsed time, 12.284s cpu time, 1.456s GC time, factor 1.57)
23:27:46Certification_Monads: theory HOL-Library.Monad_Syntax
23:27:46Finished Tail_Recursive_Functions (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.39)
23:27:46Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
23:27:46GoedelGod: theory GoedelGod.GoedelGod
23:27:46Certification_Monads: theory Certification_Monads.Error_Monad
23:27:46Sliding_Window_Algorithm: theory Sliding_Window_Algorithm.SWA
23:27:46Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Plus
23:27:46GaleStewart_Games: theory GaleStewart_Games.AlternatingLists
23:27:46Certification_Monads: theory Certification_Monads.Strict_Sum
23:27:46Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Product_Order
23:27:46Sunflowers: theory Sunflowers.Sunflower
23:27:46Timing Fixed_Length_Vector (2 threads, 9.279s elapsed time, 11.590s cpu time, 0.522s GC time, factor 1.25)
23:27:46Finished Fixed_Length_Vector (0:00:11 elapsed time, 0:00:13 cpu time, factor 1.20)
23:27:46GaleStewart_Games: theory GaleStewart_Games.GaleStewartGames
23:27:46Timing Hood_Melville_Queue (2 threads, 46.518s elapsed time, 78.755s cpu time, 4.522s GC time, factor 1.69)
23:27:46Finished Hood_Melville_Queue (0:00:49 elapsed time, 0:01:21 cpu time, factor 1.66)
23:27:46Timing TortoiseHare (2 threads, 6.814s elapsed time, 10.979s cpu time, 0.451s GC time, factor 1.61)
23:27:46Finished TortoiseHare (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.39)
23:27:46Running PropResPI (on of2.proof.cit.tum.de) ...
23:27:46Running CYK (on of2.proof.cit.tum.de) ...
23:27:46Running DataRefinementIBP (on of2.proof.cit.tum.de) ...
23:27:46Running IO_Language_Conformance (on of2.proof.cit.tum.de) ...
23:27:46Sunflowers: theory Sunflowers.Erdos_Rado_Sunflower
23:27:46Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
23:27:47Birkhoff_Finite_Distributive_Lattices: theory HOL-Library.Finite_Lattice
23:27:47Timing Secondary_Sylow (2 threads, 6.588s elapsed time, 11.405s cpu time, 0.627s GC time, factor 1.73)
23:27:47Finished Secondary_Sylow (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.93)
23:27:47Strong_Security: theory Strong_Security.Types
23:27:47CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK
23:27:47PropResPI: theory PropResPI.Propositional_Resolution
23:27:47CYK: theory CYK.CYK
23:27:47DataRefinementIBP: theory LatticeProperties.WellFoundedTransitive
23:27:47Strong_Security: theory Strong_Security.MWLf
23:27:47Strong_Security: theory Strong_Security.Expr
23:27:47GaleStewart_Games: theory GaleStewart_Games.GaleStewartDefensiveStrategies
23:27:47Running FunWithTilings (on of4.proof.cit.tum.de) ...
23:27:47DataRefinementIBP: theory LatticeProperties.Conj_Disj
23:27:47Running LatticeProperties (on of4.proof.cit.tum.de) ...
23:27:47Running Nano_JSON (on of4.proof.cit.tum.de) ...
23:27:47Running Recursion-Theory-I (on of4.proof.cit.tum.de) ...
23:27:47FLP: theory FLP.FLPSystem
23:27:47GaleStewart_Games: theory GaleStewart_Games.GaleStewartDeterminedGames
23:27:47DataRefinementIBP: theory LatticeProperties.Complete_Lattice_Prop
23:27:47IO_Language_Conformance: theory IO_Language_Conformance.Input_Output_Language_Conformance
23:27:47Timing LP_Duality (2 threads, 7.995s elapsed time, 10.062s cpu time, 0.266s GC time, factor 1.26)
23:27:47Finished LP_Duality (0:00:12 elapsed time, 0:00:14 cpu time, factor 1.15)
23:27:48Certification_Monads: theory Certification_Monads.Check_Monad
23:27:48DataRefinementIBP: theory DataRefinementIBP.Preliminaries
23:27:48Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples
23:27:48Timing Falling_Factorial_Sum (2 threads, 8.403s elapsed time, 14.950s cpu time, 0.637s GC time, factor 1.78)
23:27:48Finished Falling_Factorial_Sum (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.55)
23:27:48DataRefinementIBP: theory DataRefinementIBP.Statements
23:27:48DataRefinementIBP: theory DataRefinementIBP.Hoare
23:27:48FunWithTilings: theory FunWithTilings.Tilings
23:27:48DataRefinementIBP: theory DataRefinementIBP.Diagram
23:27:48LatticeProperties: theory LatticeProperties.Lattice_Prop
23:27:48Nano_JSON: theory Nano_JSON.Nano_JSON
23:27:48LatticeProperties: theory LatticeProperties.Conj_Disj
23:27:48LatticeProperties: theory LatticeProperties.WellFoundedTransitive
23:27:48Recursion-Theory-I: theory Recursion-Theory-I.CPair
23:27:48FLP: theory FLP.FLPTheorem
23:27:48DataRefinementIBP: theory DataRefinementIBP.DataRefinement
23:27:48Certification_Monads: theory Show.Show
23:27:48LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice
23:27:48Recursion-Theory-I: theory Recursion-Theory-I.PRecFun
23:27:48Transitive-Closure: theory Matrix.Utility
23:27:48Chord_Segments: theory Triangle.Angles
23:27:48Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl
23:27:48LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop
23:27:48Strong_Security: theory Strong_Security.Domain_example
23:27:48Timing FinFun (2 threads, 6.875s elapsed time, 12.036s cpu time, 0.677s GC time, factor 1.75)
23:27:49Finished FinFun (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.57)
23:27:49Timing Maximum_Segment_Sum (2 threads, 7.144s elapsed time, 7.763s cpu time, 0.249s GC time, factor 1.09)
23:27:49Finished Maximum_Segment_Sum (0:00:09 elapsed time, 0:00:09 cpu time, factor 1.03)
23:27:49Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension
23:27:49Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl
23:27:49Strong_Security: theory Strong_Security.Strong_Security
23:27:49Chord_Segments: theory Triangle.Triangle
23:27:49Nano_JSON: theory Nano_JSON.Nano_JSON_Query
23:27:49Timing CYK (6 threads, 1.625s elapsed time, 4.866s cpu time, 0.290s GC time, factor 2.99)
23:27:49Finished CYK (0:00:02 elapsed time, 0:00:05 cpu time)
23:27:49Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet
23:27:49Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2
23:27:49Recursion-Theory-I: theory Recursion-Theory-I.PRecList
23:27:49Prefix_Free_Code_Combinators: theory Prefix_Free_Code_Combinators.Examples
23:27:49Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
23:27:49Timing DataRefinementIBP (6 threads, 1.778s elapsed time, 3.487s cpu time, 0.119s GC time, factor 1.96)
23:27:49Finished DataRefinementIBP (0:00:02 elapsed time, 0:00:04 cpu time)
23:27:49PropResPI: theory PropResPI.Prime_Implicates
23:27:49Strong_Security: theory Strong_Security.Up_To_Technique
23:27:49Strong_Security: theory Strong_Security.Parallel_Composition
23:27:49LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group
23:27:50Nano_JSON: theory Nano_JSON.Nano_JSON_Main
23:27:50Nano_JSON: theory Nano_JSON.Nano_JSON_Manual
23:27:50FLP: theory FLP.FLPExistingSystem
23:27:50Nano_JSON: theory Nano_JSON.Example_Real
23:27:50Nano_JSON: theory Nano_JSON.Example
23:27:50Chord_Segments: theory Chord_Segments.Chord_Segments
23:27:50Strong_Security: theory Strong_Security.Strongly_Secure_Skip_Assign
23:27:50Floyd_Warshall: theory Floyd_Warshall.FW_Code
23:27:50Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl
23:27:50Timing PAC_Checker (2 threads, 735.056s elapsed time, 1192.491s cpu time, 294.004s GC time, factor 1.62)
23:27:50Finished PAC_Checker (0:12:22 elapsed time, 0:20:03 cpu time, factor 1.62)
23:27:50Strong_Security: theory Strong_Security.Language_Composition
23:27:50Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr
23:27:50Strong_Security: theory Strong_Security.Type_System
23:27:51Timing Nano_JSON (6 threads, 2.178s elapsed time, 3.531s cpu time, 0.259s GC time, factor 1.62)
23:27:51Certification_Monads: theory Certification_Monads.Parser_Monad
23:27:51Timing LatticeProperties (6 threads, 2.303s elapsed time, 4.394s cpu time, 0.172s GC time, factor 1.91)
23:27:51Finished Nano_JSON (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.38)
23:27:51Finished LatticeProperties (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.63)
23:27:51Birkhoff_Finite_Distributive_Lattices: theory Birkhoff_Finite_Distributive_Lattices.Birkhoff_Finite_Distributive_Lattices
23:27:51Strong_Security: theory Strong_Security.Type_System_example
23:27:51Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet
23:27:51Timing Arith_Prog_Rel_Primes (2 threads, 7.118s elapsed time, 12.172s cpu time, 0.563s GC time, factor 1.71)
23:27:51Finished Arith_Prog_Rel_Primes (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.46)
23:27:52Timing IO_Language_Conformance (6 threads, 4.364s elapsed time, 19.507s cpu time, 1.426s GC time, factor 4.47)
23:27:52Finished IO_Language_Conformance (0:00:05 elapsed time, 0:00:20 cpu time, factor 3.72)
23:27:52Timing GaleStewart_Games (2 threads, 7.998s elapsed time, 13.475s cpu time, 0.423s GC time, factor 1.68)
23:27:52Finished GaleStewart_Games (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.51)
23:27:52Timing Recursion-Theory-I (6 threads, 3.886s elapsed time, 16.185s cpu time, 1.339s GC time, factor 4.16)
23:27:52Timing Sunflowers (2 threads, 6.720s elapsed time, 12.717s cpu time, 0.558s GC time, factor 1.89)
23:27:52Finished Sunflowers (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.65)
23:27:52Finished Recursion-Theory-I (0:00:04 elapsed time, 0:00:17 cpu time, factor 3.52)
23:27:53Timing Partial_Function_MR (2 threads, 8.568s elapsed time, 12.246s cpu time, 1.590s GC time, factor 1.43)
23:27:53Finished Partial_Function_MR (0:00:10 elapsed time, 0:00:14 cpu time, factor 1.35)
23:27:53Timing PropResPI (6 threads, 5.198s elapsed time, 14.324s cpu time, 1.572s GC time, factor 2.76)
23:27:53Finished PropResPI (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.46)
23:27:53Timing Prefix_Free_Code_Combinators (2 threads, 5.739s elapsed time, 8.723s cpu time, 0.314s GC time, factor 1.52)
23:27:53Finished Prefix_Free_Code_Combinators (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.33)
23:27:53Timing GoedelGod (2 threads, 6.798s elapsed time, 6.296s cpu time, 0.184s GC time, factor 0.93)
23:27:53Finished GoedelGod (0:00:08 elapsed time, 0:00:07 cpu time, factor 0.89)
23:27:53Timing FunWithTilings (6 threads, 4.944s elapsed time, 17.760s cpu time, 0.301s GC time, factor 3.59)
23:27:53Finished FunWithTilings (0:00:06 elapsed time, 0:00:18 cpu time, factor 3.09)
23:27:54Timing Certification_Monads (2 threads, 8.134s elapsed time, 15.919s cpu time, 1.972s GC time, factor 1.96)
23:27:54Finished Certification_Monads (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.76)
23:27:55Timing Transitive-Closure (2 threads, 6.026s elapsed time, 10.811s cpu time, 0.502s GC time, factor 1.79)
23:27:55Finished Transitive-Closure (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.51)
23:27:56Timing Chord_Segments (2 threads, 6.894s elapsed time, 8.908s cpu time, 0.387s GC time, factor 1.29)
23:27:56Finished Chord_Segments (0:00:09 elapsed time, 0:00:11 cpu time, factor 1.19)
23:28:01Timing Birkhoff_Finite_Distributive_Lattices (2 threads, 14.828s elapsed time, 23.686s cpu time, 2.392s GC time, factor 1.60)
23:28:01Finished Birkhoff_Finite_Distributive_Lattices (0:00:16 elapsed time, 0:00:25 cpu time, factor 1.52)
23:28:01Timing Finite_Automata_HF (2 threads, 26.067s elapsed time, 41.345s cpu time, 2.491s GC time, factor 1.59)
23:28:01Finished Finite_Automata_HF (0:00:28 elapsed time, 0:00:43 cpu time, factor 1.54)
23:28:02Timing Stream_Fusion_Code (2 threads, 25.454s elapsed time, 44.693s cpu time, 2.748s GC time, factor 1.76)
23:28:02Finished Stream_Fusion_Code (0:00:28 elapsed time, 0:00:48 cpu time, factor 1.67)
23:28:05Timing SenSocialChoice (2 threads, 27.325s elapsed time, 44.517s cpu time, 2.984s GC time, factor 1.63)
23:28:05Finished SenSocialChoice (0:00:29 elapsed time, 0:00:46 cpu time, factor 1.58)
23:28:07Timing Quaternions (2 threads, 21.396s elapsed time, 25.215s cpu time, 1.582s GC time, factor 1.18)
23:28:07Finished Quaternions (0:00:24 elapsed time, 0:00:28 cpu time, factor 1.15)
23:28:07Timing Strong_Security (2 threads, 19.357s elapsed time, 34.021s cpu time, 2.933s GC time, factor 1.76)
23:28:07Finished Strong_Security (0:00:21 elapsed time, 0:00:36 cpu time, factor 1.69)
23:28:07Timing CISC-Kernel (2 threads, 28.338s elapsed time, 52.706s cpu time, 5.802s GC time, factor 1.86)
23:28:07Finished CISC-Kernel (0:00:30 elapsed time, 0:00:55 cpu time, factor 1.81)
23:28:09Timing FLP (2 threads, 26.442s elapsed time, 50.121s cpu time, 4.027s GC time, factor 1.90)
23:28:09Finished FLP (0:00:29 elapsed time, 0:00:53 cpu time, factor 1.82)
23:28:10Timing Hahn_Jordan_Decomposition (2 threads, 33.903s elapsed time, 50.345s cpu time, 2.781s GC time, factor 1.48)
23:28:10Finished Hahn_Jordan_Decomposition (0:00:37 elapsed time, 0:00:53 cpu time, factor 1.44)
23:28:11Running Noninterference_Generic_Unwinding (on 10.195.6.179) ...
23:28:11Timing Sliding_Window_Algorithm (2 threads, 25.467s elapsed time, 43.363s cpu time, 1.744s GC time, factor 1.70)
23:28:11Finished Sliding_Window_Algorithm (0:00:27 elapsed time, 0:00:45 cpu time, factor 1.65)
23:28:12Timing Floyd_Warshall (2 threads, 29.263s elapsed time, 55.349s cpu time, 3.618s GC time, factor 1.89)
23:28:12Finished Floyd_Warshall (0:00:33 elapsed time, 0:00:59 cpu time, factor 1.78)
23:28:12Running Minimal_SSA (on of1-proof+8-15) ...
23:28:13Running Abstract-Hoare-Logics (on of1-proof+0-7) ...
23:28:13Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PLang
23:28:13Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Lang
23:28:13Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsLang
23:28:14Running Goodstein_Lambda (on of3.proof.cit.tum.de) ...
23:28:14Running Cotangent_PFD_Formula (on of3.proof.cit.tum.de) ...
23:28:14Running Equivalence_Relation_Enumeration (on of3.proof.cit.tum.de) ...
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Hoare
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.Termi
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.HoareTotal
23:28:14Minimal_SSA: theory Minimal_SSA.Irreducible
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsTermi
23:28:14Goodstein_Lambda: theory Goodstein_Lambda.Goodstein_Lambda
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoare
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PTermi
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoare
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PHoareTotal
23:28:14Abstract-Hoare-Logics: theory Abstract-Hoare-Logics.PsHoareTotal
23:28:15Running Boolos_Curious_Inference_Automated (on 10.195.8.49) ...
23:28:15Equivalence_Relation_Enumeration: theory HOL-Eisbach.Eisbach
23:28:15Equivalence_Relation_Enumeration: theory HOL-Combinatorics.Stirling
23:28:15Equivalence_Relation_Enumeration: theory Card_Partitions.Set_Partition
23:28:15Running Mason_Stothers (on 10.195.8.49) ...
23:28:15Running Triangle (on 10.195.8.49) ...
23:28:15Running Pell (on 10.195.8.49) ...
23:28:15Cotangent_PFD_Formula: theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
23:28:16Equivalence_Relation_Enumeration: theory Card_Partitions.Injectivity_Solver
23:28:16Equivalence_Relation_Enumeration: theory Card_Partitions.Card_Partitions
23:28:16Running Stewart_Apollonius (on 10.195.8.32) ...
23:28:16Running Card_Multisets (on 10.195.8.32) ...
23:28:16Running KD_Tree (on 10.195.8.32) ...
23:28:16Boolos_Curious_Inference_Automated: theory Boolos_Curious_Inference_Automated.Boolos_Curious_Inference_Automated
23:28:16Equivalence_Relation_Enumeration: theory Bell_Numbers_Spivey.Bell_Numbers
23:28:16Timing Abstract-Hoare-Logics (8 threads, 2.556s elapsed time, 13.278s cpu time, 1.373s GC time, factor 5.19)
23:28:16Finished Abstract-Hoare-Logics (0:00:03 elapsed time, 0:00:14 cpu time, factor 4.04)
23:28:17Equivalence_Relation_Enumeration: theory Card_Equiv_Relations.Card_Equiv_Relations
23:28:17Equivalence_Relation_Enumeration: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
23:28:17Timing Cotangent_PFD_Formula (6 threads, 1.718s elapsed time, 3.702s cpu time, 0.116s GC time, factor 2.15)
23:28:17Finished Cotangent_PFD_Formula (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.57)
23:28:17Mason_Stothers: theory Mason_Stothers.Mason_Stothers
23:28:17Running Fresh_Identifiers (on 10.195.8.46) ...
23:28:17Timing Goodstein_Lambda (6 threads, 2.604s elapsed time, 5.273s cpu time, 0.205s GC time, factor 2.02)
23:28:17Finished Goodstein_Lambda (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.75)
23:28:17Running Pairing_Heap (on 10.195.8.46) ...
23:28:17Pell: theory Pell.Pell
23:28:17Pell: theory Pell.Efficient_Discrete_Sqrt
23:28:17Running Lazy_Case (on 10.195.8.46) ...
23:28:17Running Octonions (on 10.195.8.46) ...
23:28:17Timing Minimal_SSA (8 threads, 2.724s elapsed time, 9.575s cpu time, 0.383s GC time, factor 3.52)
23:28:17Finished Minimal_SSA (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.59)
23:28:18Card_Multisets: theory HOL-Library.Cancellation
23:28:18Triangle: theory Triangle.Angles
23:28:18Triangle: theory Triangle.Triangle
23:28:19Card_Multisets: theory HOL-Library.Multiset
23:28:19KD_Tree: theory KD_Tree.KD_Tree
23:28:19KD_Tree: theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
23:28:19Stewart_Apollonius: theory Triangle.Angles
23:28:19Fresh_Identifiers: theory Fresh_Identifiers.Fresh
23:28:19Running Stalnaker_Logic (on 10.195.8.40) ...
23:28:19Running GenClock (on 10.195.8.40) ...
23:28:19Running Catalan_Numbers (on 10.195.8.40) ...
23:28:19Lazy_Case: theory Lazy_Case.Lazy_Case
23:28:19Pell: theory Pell.Pell_Algorithm
23:28:20Stewart_Apollonius: theory Triangle.Triangle
23:28:20Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Infinite
23:28:20Fresh_Identifiers: theory Fresh_Identifiers.Fresh_Nat
23:28:20Lazy_Case: theory Lazy_Case.Test_Lazy_Case
23:28:20Fresh_Identifiers: theory Fresh_Identifiers.Fresh_String
23:28:20Timing Equivalence_Relation_Enumeration (6 threads, 4.513s elapsed time, 20.232s cpu time, 0.781s GC time, factor 4.48)
23:28:20Pairing_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
23:28:20Finished Equivalence_Relation_Enumeration (0:00:05 elapsed time, 0:00:21 cpu time, factor 3.66)
23:28:20Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
23:28:20Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List2
23:28:20Pairing_Heap: theory Pairing_Heap.Pairing_Heap_List1
23:28:20Running Compiling-Exceptions-Correctly (on 10.195.8.30) ...
23:28:20Running Szpilrajn (on 10.195.8.30) ...
23:28:21Octonions: theory Octonions.Cross_Product_7
23:28:21GenClock: theory GenClock.GenClock
23:28:21Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
23:28:21Running Gauss-Jordan-Elim-Fun (on 10.195.8.30) ...
23:28:21Pell: theory Pell.Pell_Algorithm_Test
23:28:21Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding
23:28:21KD_Tree: theory KD_Tree.Nearest_Neighbors
23:28:21KD_Tree: theory KD_Tree.Range_Search
23:28:22KD_Tree: theory KD_Tree.Build
23:28:22Timing Mason_Stothers (2 threads, 4.023s elapsed time, 5.663s cpu time, 0.138s GC time, factor 1.41)
23:28:22Finished Mason_Stothers (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.21)
23:28:22Compiling-Exceptions-Correctly: theory Compiling-Exceptions-Correctly.Exceptions
23:28:22Running Ramsey-Infinite (on 10.195.7.194) ...
23:28:22Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
23:28:22Catalan_Numbers: theory HOL-Library.Function_Algebras
23:28:22Pairing_Heap: theory Pairing_Heap.Pairing_Heap_Tree
23:28:22Szpilrajn: theory Szpilrajn.Szpilrajn
23:28:22Octonions: theory Octonions.Octonions
23:28:23Gauss-Jordan-Elim-Fun: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
23:28:23Catalan_Numbers: theory Landau_Symbols.Group_Sort
23:28:23Running Stuttering_Equivalence (on 10.195.7.194) ...
23:28:23Running DPT-SAT-Solver (on 10.195.7.194) ...
23:28:23Running Neumann_Morgenstern_Utility (on 10.195.7.194) ...
23:28:23Timing Triangle (2 threads, 4.902s elapsed time, 5.833s cpu time, 0.183s GC time, factor 1.19)
23:28:23Finished Triangle (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.09)
23:28:24Timing Lazy_Case (2 threads, 4.311s elapsed time, 5.870s cpu time, 0.398s GC time, factor 1.36)
23:28:24Finished Lazy_Case (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.20)
23:28:24Running Constructor_Funs (on 10.195.8.11) ...
23:28:24Running FOL_Axiomatic (on 10.195.8.11) ...
23:28:24Timing Fresh_Identifiers (2 threads, 4.926s elapsed time, 7.736s cpu time, 0.164s GC time, factor 1.57)
23:28:24Finished Fresh_Identifiers (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.39)
23:28:25Ramsey-Infinite: theory HOL-Library.Infinite_Set
23:28:25Ramsey-Infinite: theory HOL-Library.FuncSet
23:28:25DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Solver
23:28:25Card_Multisets: theory Card_Multisets.Card_Multisets
23:28:25Timing Stewart_Apollonius (2 threads, 5.236s elapsed time, 7.028s cpu time, 0.271s GC time, factor 1.34)
23:28:25Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.17)
23:28:25Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
23:28:25Running Pratt_Certificate (on 10.195.8.11) ...
23:28:25Running Mereology (on 10.195.8.11) ...
23:28:25Running AnselmGod (on 10.195.8.11) ...
23:28:26Stuttering_Equivalence: theory Stuttering_Equivalence.Samplers
23:28:26Timing Pairing_Heap (2 threads, 5.170s elapsed time, 8.890s cpu time, 0.715s GC time, factor 1.72)
23:28:26Finished Pairing_Heap (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.45)
23:28:26Timing Stalnaker_Logic (2 threads, 4.512s elapsed time, 7.396s cpu time, 0.262s GC time, factor 1.64)
23:28:26Constructor_Funs: theory Constructor_Funs.Constructor_Funs
23:28:26Finished Stalnaker_Logic (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.41)
23:28:26Ramsey-Infinite: theory HOL-Library.Ramsey
23:28:26Constructor_Funs: theory Constructor_Funs.Test_Constructor_Funs
23:28:26Timing GenClock (2 threads, 5.070s elapsed time, 9.343s cpu time, 0.339s GC time, factor 1.84)
23:28:26Finished GenClock (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.60)
23:28:26Stuttering_Equivalence: theory Stuttering_Equivalence.StutterEquivalence
23:28:27Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
23:28:27Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
23:28:27FOL_Axiomatic: theory HOL-Library.Nat_Bijection
23:28:27Mereology: theory Mereology.PM
23:28:27FOL_Axiomatic: theory HOL-Library.Old_Datatype
23:28:27DPT-SAT-Solver: theory DPT-SAT-Solver.DPT_SAT_Tests
23:28:27Running Binary_Code_Imprimitive (on 10.195.8.42) ...
23:28:27Running Descartes_Sign_Rule (on 10.195.8.42) ...
23:28:27Stuttering_Equivalence: theory Stuttering_Equivalence.PLTL
23:28:27Running BinarySearchTree (on 10.195.8.42) ...
23:28:27Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
23:28:27AnselmGod: theory AnselmGod.AnselmGod
23:28:27Running C2KA_DistributedSystems (on 10.195.8.42) ...
23:28:27Mereology: theory Mereology.M
23:28:27Ramsey-Infinite: theory Ramsey-Infinite.Ramsey
23:28:27Timing Gauss-Jordan-Elim-Fun (2 threads, 4.236s elapsed time, 6.597s cpu time, 0.238s GC time, factor 1.56)
23:28:27Finished Gauss-Jordan-Elim-Fun (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33)
23:28:27Mereology: theory Mereology.CM
23:28:27Mereology: theory Mereology.MM
23:28:27Timing Compiling-Exceptions-Correctly (2 threads, 4.841s elapsed time, 7.402s cpu time, 0.538s GC time, factor 1.53)
23:28:27Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.34)
23:28:28Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
23:28:28Mereology: theory Mereology.EM
23:28:28Mereology: theory Mereology.GM
23:28:28Pratt_Certificate: theory Lehmer.Lehmer
23:28:28Mereology: theory Mereology.CEM
23:28:28Mereology: theory Mereology.GMM
23:28:28Running Ceva (on 10.195.8.29) ...
23:28:28FOL_Axiomatic: theory HOL-Library.Countable
23:28:28Running First_Welfare_Theorem (on 10.195.8.29) ...
23:28:28Running Lower_Semicontinuous (on 10.195.8.29) ...
23:28:28Running Verified-Prover (on 10.195.8.29) ...
23:28:28Timing Szpilrajn (2 threads, 5.357s elapsed time, 8.028s cpu time, 0.321s GC time, factor 1.50)
23:28:28Finished Szpilrajn (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.35)
23:28:28Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Square_Interpretation
23:28:29Binary_Code_Imprimitive: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
23:28:29Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
23:28:29BinarySearchTree: theory BinarySearchTree.BinaryTree
23:28:29Mereology: theory Mereology.GEM
23:28:29BinarySearchTree: theory BinarySearchTree.BinaryTree_TacticStyle
23:28:29C2KA_DistributedSystems: theory C2KA_DistributedSystems.CKA
23:28:29C2KA_DistributedSystems: theory C2KA_DistributedSystems.Stimuli
23:28:29Running Noninterference_Inductive_Unwinding (on of2.proof.cit.tum.de) ...
23:28:29Running Risk_Free_Lending (on of2.proof.cit.tum.de) ...
23:28:29Running List-Index (on of2.proof.cit.tum.de) ...
23:28:29Running Implicational_Logic (on of2.proof.cit.tum.de) ...
23:28:29Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
23:28:30Noninterference_Inductive_Unwinding: theory List_Interleaving.ListInterleaving
23:28:30Noninterference_Inductive_Unwinding: theory Noninterference_CSP.CSPNoninterference
23:28:30Risk_Free_Lending: theory Risk_Free_Lending.Risk_Free_Lending
23:28:30List-Index: theory List-Index.List_Index
23:28:30Running List_Interleaving (on of4.proof.cit.tum.de) ...
23:28:30Implicational_Logic: theory Implicational_Logic.Implicational_Logic_Appendix
23:28:30Running Pop_Refinement (on of4.proof.cit.tum.de) ...
23:28:30Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
23:28:30Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Code_Imprimitive
23:28:30Implicational_Logic: theory Implicational_Logic.Implicational_Logic
23:28:30Running Skip_Lists (on of4.proof.cit.tum.de) ...
23:28:30Verified-Prover: theory Verified-Prover.Prover
23:28:30Running Laplace_Transform (on of4.proof.cit.tum.de) ...
23:28:30FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic
23:28:30FOL_Axiomatic: theory FOL_Axiomatic.FOL_Axiomatic_Variant
23:28:31BinarySearchTree: theory BinarySearchTree.BinaryTree_Map
23:28:31List_Interleaving: theory List_Interleaving.ListInterleaving
23:28:31Pop_Refinement: theory Pop_Refinement.First_Example
23:28:31Pop_Refinement: theory Pop_Refinement.Definition
23:28:31Pop_Refinement: theory Pop_Refinement.Future_Work
23:28:31Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
23:28:31Pop_Refinement: theory Pop_Refinement.General_Remarks
23:28:31Pop_Refinement: theory Pop_Refinement.Related_Work
23:28:31Pop_Refinement: theory Pop_Refinement.Second_Example
23:28:31Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
23:28:31Timing DPT-SAT-Solver (2 threads, 5.481s elapsed time, 8.033s cpu time, 0.219s GC time, factor 1.47)
23:28:31Finished DPT-SAT-Solver (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.32)
23:28:31Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Imprimitive_Decision
23:28:31Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
23:28:31Ceva: theory Triangle.Angles
23:28:31Timing List-Index (6 threads, 0.840s elapsed time, 3.441s cpu time, 0.091s GC time, factor 4.10)
23:28:31Finished List-Index (0:00:01 elapsed time, 0:00:04 cpu time)
23:28:31First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
23:28:31C2KA_DistributedSystems: theory C2KA_DistributedSystems.C2KA
23:28:31First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
23:28:31Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
23:28:31Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
23:28:31Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
23:28:31Skip_Lists: theory Skip_Lists.Pi_pmf
23:28:31Timing Implicational_Logic (6 threads, 1.069s elapsed time, 3.047s cpu time, 0.162s GC time, factor 2.85)
23:28:31Skip_Lists: theory Skip_Lists.Misc
23:28:31Skip_Lists: theory Monad_Normalisation.Monad_Normalisation
23:28:31First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
23:28:31Finished Implicational_Logic (0:00:02 elapsed time, 0:00:03 cpu time)
23:28:32Catalan_Numbers: theory Landau_Symbols.Landau_More
23:28:32First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
23:28:32Timing Stuttering_Equivalence (2 threads, 5.361s elapsed time, 9.179s cpu time, 0.396s GC time, factor 1.71)
23:28:32Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
23:28:32Finished Stuttering_Equivalence (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.44)
23:28:32C2KA_DistributedSystems: theory C2KA_DistributedSystems.Topology_C2KA
23:28:32Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
23:28:32Ceva: theory Triangle.Triangle
23:28:32Noninterference_Inductive_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
23:28:32C2KA_DistributedSystems: theory C2KA_DistributedSystems.Communication_C2KA
23:28:32Skip_Lists: theory Skip_Lists.Geometric_PMF
23:28:32Noninterference_Inductive_Unwinding: theory Noninterference_Inductive_Unwinding.InductiveUnwinding
23:28:32Laplace_Transform: theory Laplace_Transform.Existence
23:28:32Timing List_Interleaving (6 threads, 0.953s elapsed time, 3.037s cpu time, 0.157s GC time, factor 3.19)
23:28:32Finished List_Interleaving (0:00:01 elapsed time, 0:00:03 cpu time)
23:28:32Timing Boolos_Curious_Inference_Automated (2 threads, 15.611s elapsed time, 17.850s cpu time, 2.867s GC time, factor 1.14)
23:28:32Finished Boolos_Curious_Inference_Automated (0:00:17 elapsed time, 0:00:19 cpu time, factor 1.11)
23:28:32Timing AnselmGod (2 threads, 5.018s elapsed time, 3.703s cpu time, 0.115s GC time, factor 0.74)
23:28:32Finished AnselmGod (0:00:07 elapsed time, 0:00:05 cpu time, factor 0.77)
23:28:32Skip_Lists: theory Skip_Lists.Skip_List
23:28:33Laplace_Transform: theory Laplace_Transform.Uniqueness
23:28:33Ceva: theory Ceva.Ceva
23:28:33Laplace_Transform: theory Laplace_Transform.Laplace_Transform
23:28:33Timing Risk_Free_Lending (6 threads, 3.010s elapsed time, 8.674s cpu time, 0.330s GC time, factor 2.88)
23:28:33Finished Risk_Free_Lending (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.47)
23:28:33Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
23:28:33Timing Noninterference_Inductive_Unwinding (6 threads, 2.831s elapsed time, 9.756s cpu time, 0.952s GC time, factor 3.45)
23:28:33Finished Noninterference_Inductive_Unwinding (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.76)
23:28:33Timing Card_Multisets (2 threads, 15.098s elapsed time, 26.007s cpu time, 1.416s GC time, factor 1.72)
23:28:33Finished Card_Multisets (0:00:17 elapsed time, 0:00:27 cpu time, factor 1.63)
23:28:33Timing C2KA_DistributedSystems (2 threads, 4.213s elapsed time, 5.240s cpu time, 0.206s GC time, factor 1.24)
23:28:33Finished C2KA_DistributedSystems (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.11)
23:28:34Timing BinarySearchTree (2 threads, 4.453s elapsed time, 7.579s cpu time, 0.514s GC time, factor 1.70)
23:28:34Finished BinarySearchTree (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.43)
23:28:34Timing Descartes_Sign_Rule (2 threads, 3.681s elapsed time, 6.444s cpu time, 0.160s GC time, factor 1.75)
23:28:34Finished Descartes_Sign_Rule (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.35)
23:28:35Timing Pop_Refinement (6 threads, 3.312s elapsed time, 9.345s cpu time, 0.981s GC time, factor 2.82)
23:28:35Finished Pop_Refinement (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.34)
23:28:35First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
23:28:35Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
23:28:35First_Welfare_Theorem: theory First_Welfare_Theorem.Common
23:28:36Timing Laplace_Transform (6 threads, 3.775s elapsed time, 16.449s cpu time, 0.450s GC time, factor 4.36)
23:28:36Finished Laplace_Transform (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.31)
23:28:36Timing Skip_Lists (6 threads, 4.006s elapsed time, 17.225s cpu time, 0.492s GC time, factor 4.30)
23:28:36Finished Skip_Lists (0:00:05 elapsed time, 0:00:18 cpu time, factor 3.34)
23:28:36First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
23:28:36First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
23:28:37First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
23:28:37Timing Mereology (2 threads, 9.818s elapsed time, 9.730s cpu time, 0.597s GC time, factor 0.99)
23:28:37Finished Mereology (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.97)
23:28:38Timing Binary_Code_Imprimitive (2 threads, 8.635s elapsed time, 15.950s cpu time, 0.772s GC time, factor 1.85)
23:28:38Finished Binary_Code_Imprimitive (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.68)
23:28:40Timing Constructor_Funs (2 threads, 14.039s elapsed time, 7.894s cpu time, 0.647s GC time, factor 0.56)
23:28:40Finished Constructor_Funs (0:00:16 elapsed time, 0:00:09 cpu time, factor 0.61)
23:28:40Timing Catalan_Numbers (2 threads, 17.520s elapsed time, 34.955s cpu time, 2.801s GC time, factor 2.00)
23:28:40Finished Catalan_Numbers (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.84)
23:28:41Timing Pell (2 threads, 22.674s elapsed time, 35.408s cpu time, 0.893s GC time, factor 1.56)
23:28:41Finished Pell (0:00:25 elapsed time, 0:00:37 cpu time, factor 1.49)
23:28:41Timing Noninterference_Generic_Unwinding (2 threads, 19.016s elapsed time, 20.785s cpu time, 0.526s GC time, factor 1.09)
23:28:41Finished Noninterference_Generic_Unwinding (0:00:29 elapsed time, 0:00:22 cpu time, factor 0.79)
23:28:42Timing KD_Tree (2 threads, 22.084s elapsed time, 38.578s cpu time, 2.436s GC time, factor 1.75)
23:28:42Finished KD_Tree (0:00:25 elapsed time, 0:00:41 cpu time, factor 1.65)
23:28:42Timing FOL_Axiomatic (2 threads, 14.667s elapsed time, 25.172s cpu time, 2.753s GC time, factor 1.72)
23:28:42Finished FOL_Axiomatic (0:00:16 elapsed time, 0:00:27 cpu time, factor 1.62)
23:28:44Timing Ramsey-Infinite (2 threads, 18.345s elapsed time, 33.847s cpu time, 2.116s GC time, factor 1.85)
23:28:44Finished Ramsey-Infinite (0:00:20 elapsed time, 0:00:35 cpu time, factor 1.75)
23:28:45Timing Verified-Prover (2 threads, 13.990s elapsed time, 17.171s cpu time, 0.662s GC time, factor 1.23)
23:28:45Finished Verified-Prover (0:00:16 elapsed time, 0:00:18 cpu time, factor 1.18)
23:28:45Timing Octonions (2 threads, 23.674s elapsed time, 44.148s cpu time, 4.366s GC time, factor 1.86)
23:28:45Finished Octonions (0:00:27 elapsed time, 0:00:47 cpu time, factor 1.75)
23:28:45Timing Pratt_Certificate (2 threads, 17.015s elapsed time, 29.015s cpu time, 0.909s GC time, factor 1.71)
23:28:46Finished Pratt_Certificate (0:00:20 elapsed time, 0:00:32 cpu time, factor 1.57)
23:28:46Timing MDP-Algorithms (2 threads, 1473.225s elapsed time, 2580.872s cpu time, 890.061s GC time, factor 1.75)
23:28:46Finished MDP-Algorithms (0:24:43 elapsed time, 0:43:16 cpu time, factor 1.75)
23:28:47Timing Expander_Graphs (2 threads, 800.759s elapsed time, 1334.726s cpu time, 254.917s GC time, factor 1.67)
23:28:47Finished Expander_Graphs (0:14:45 elapsed time, 0:24:09 cpu time, factor 1.64)
23:28:47Timing Lower_Semicontinuous (2 threads, 15.559s elapsed time, 23.245s cpu time, 0.572s GC time, factor 1.49)
23:28:47Finished Lower_Semicontinuous (0:00:18 elapsed time, 0:00:26 cpu time, factor 1.40)
23:28:48Timing Ceva (2 threads, 16.078s elapsed time, 20.934s cpu time, 0.790s GC time, factor 1.30)
23:28:48Finished Ceva (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.24)
23:28:51Timing First_Welfare_Theorem (2 threads, 19.125s elapsed time, 33.548s cpu time, 2.990s GC time, factor 1.75)
23:28:51Finished First_Welfare_Theorem (0:00:22 elapsed time, 0:00:36 cpu time, factor 1.63)
23:28:53Running Cartan_FP (on 10.195.6.179) ...
23:28:54Running Card_Partitions (on of1-proof+8-15) ...
23:28:54Running Median_Method (on of1-proof+0-7) ...
23:28:55Running Robbins-Conjecture (on of3.proof.cit.tum.de) ...
23:28:55Card_Partitions: theory HOL-Eisbach.Eisbach
23:28:55Card_Partitions: theory HOL-Library.Adhoc_Overloading
23:28:55Card_Partitions: theory HOL-Library.FuncSet
23:28:55Card_Partitions: theory HOL-Combinatorics.Stirling
23:28:55Running Topology (on of3.proof.cit.tum.de) ...
23:28:55Running Lifting_Definition_Option (on of3.proof.cit.tum.de) ...
23:28:55Card_Partitions: theory HOL-Library.Monad_Syntax
23:28:55Robbins-Conjecture: theory Robbins-Conjecture.Robbins_Conjecture
23:28:55Median_Method: theory Universal_Hash_Families.Universal_Hash_Families
23:28:55Card_Partitions: theory HOL-Library.Disjoint_Sets
23:28:55Lifting_Definition_Option: theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
23:28:55Median_Method: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
23:28:55Card_Partitions: theory Card_Partitions.Injectivity_Solver
23:28:55Card_Partitions: theory Card_Partitions.Set_Partition
23:28:56Running DCR-ExecutionEquivalence (on 10.195.8.49) ...
23:28:56Card_Partitions: theory Card_Partitions.Card_Partitions
23:28:56Topology: theory Lazy-Lists-II.LList2
23:28:56Topology: theory Topology.Topology
23:28:56Median_Method: theory Median_Method.Median
23:28:57Timing Neumann_Morgenstern_Utility (2 threads, 29.747s elapsed time, 53.251s cpu time, 4.165s GC time, factor 1.79)
23:28:57Finished Neumann_Morgenstern_Utility (0:00:33 elapsed time, 0:00:57 cpu time, factor 1.69)
23:28:57Timing Lifting_Definition_Option (6 threads, 1.370s elapsed time, 1.628s cpu time, 0.080s GC time, factor 1.19)
23:28:58Topology: theory Topology.LList_Topology
23:28:58Finished Lifting_Definition_Option (0:00:02 elapsed time)
23:28:58Running Comparison_Sort_Lower_Bound (on 10.195.8.49) ...
23:28:58Running Max-Card-Matching (on 10.195.8.49) ...
23:28:58Running MuchAdoAboutTwo (on 10.195.8.49) ...
23:28:58Timing Card_Partitions (8 threads, 2.510s elapsed time, 14.012s cpu time, 0.837s GC time, factor 5.58)
23:28:58Finished Card_Partitions (0:00:03 elapsed time, 0:00:14 cpu time, factor 4.21)
23:28:58Timing Median_Method (8 threads, 2.537s elapsed time, 7.628s cpu time, 0.305s GC time, factor 3.01)
23:28:58Finished Median_Method (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.26)
23:28:59Timing Topology (6 threads, 2.239s elapsed time, 8.230s cpu time, 0.997s GC time, factor 3.68)
23:28:59Finished Topology (0:00:03 elapsed time, 0:00:09 cpu time, factor 2.56)
23:28:59Running FileRefinement (on 10.195.8.32) ...
23:28:59Running Marriage (on 10.195.8.32) ...
23:28:59Timing Robbins-Conjecture (6 threads, 3.040s elapsed time, 9.751s cpu time, 0.352s GC time, factor 3.21)
23:28:59Finished Robbins-Conjecture (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.63)
23:28:59Max-Card-Matching: theory Max-Card-Matching.Matching
23:28:59DCR-ExecutionEquivalence: theory DCR-ExecutionEquivalence.DCRExecutionEquivalence
23:28:59Running Lifting_the_Exponent (on 10.195.8.32) ...
23:28:59Running Lazy-Lists-II (on 10.195.8.32) ...
23:29:00Running Laws_of_Large_Numbers (on 10.195.8.32) ...
23:29:00MuchAdoAboutTwo: theory HOL-Combinatorics.Transposition
23:29:00FileRefinement: theory FileRefinement.CArrays
23:29:00FileRefinement: theory FileRefinement.ResizableArrays
23:29:00MuchAdoAboutTwo: theory HOL-Combinatorics.Permutations
23:29:00FileRefinement: theory FileRefinement.FileRefinement
23:29:00Comparison_Sort_Lower_Bound: theory HOL-Combinatorics.Multiset_Permutations
23:29:01Comparison_Sort_Lower_Bound: theory List-Index.List_Index
23:29:01Marriage: theory Marriage.Marriage
23:29:01Running CofGroups (on 10.195.8.46) ...
23:29:01Running Sauer_Shelah_Lemma (on 10.195.8.46) ...
23:29:01Running Perfect-Number-Thm (on 10.195.8.46) ...
23:29:01Running Minkowskis_Theorem (on 10.195.8.46) ...
23:29:02Timing SC_DOM_Components (6 threads, 136.455s elapsed time, 692.061s cpu time, 44.237s GC time, factor 5.07)
23:29:02Finished SC_DOM_Components (0:02:18 elapsed time, 0:11:37 cpu time, factor 5.03)
23:29:02Lifting_the_Exponent: theory Lifting_the_Exponent.LTE
23:29:02MuchAdoAboutTwo: theory MuchAdoAboutTwo.MuchAdoAboutTwo
23:29:02Timing Max-Card-Matching (2 threads, 2.347s elapsed time, 3.459s cpu time, 0.082s GC time, factor 1.47)
23:29:02Finished Max-Card-Matching (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.23)
23:29:02Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
23:29:02Running Ptolemys_Theorem (on 10.195.8.40) ...
23:29:02Running FunWithFunctions (on 10.195.8.40) ...
23:29:02Lazy-Lists-II: theory Lazy-Lists-II.LList2
23:29:02Running Weighted_Arithmetic_Geometric_Mean (on 10.195.8.40) ...
23:29:02Timing DCR-ExecutionEquivalence (2 threads, 2.857s elapsed time, 3.004s cpu time, 0.136s GC time, factor 1.05)
23:29:02Finished DCR-ExecutionEquivalence (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.96)
23:29:02CofGroups: theory HOL-Library.Nat_Bijection
23:29:03Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Binomial_Lemmas
23:29:03Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Card_Lemmas
23:29:03Running ShortestPath (on 10.195.8.40) ...
23:29:03Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
23:29:03Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Shattering
23:29:03Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
23:29:03Sauer_Shelah_Lemma: theory Sauer_Shelah_Lemma.Sauer_Shelah_Lemma
23:29:03CofGroups: theory CofGroups.CofGroups
23:29:03Laws_of_Large_Numbers: theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
23:29:04Timing Marriage (2 threads, 2.416s elapsed time, 4.582s cpu time, 0.117s GC time, factor 1.90)
23:29:04Finished Marriage (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.42)
23:29:04FunWithFunctions: theory FunWithFunctions.FunWithFunctions
23:29:04Running Dynamic_Tables (on 10.195.8.40) ...
23:29:04Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
23:29:04Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
23:29:04Weighted_Arithmetic_Geometric_Mean: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
23:29:04Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
23:29:05Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
23:29:05Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
23:29:05Timing Lifting_the_Exponent (2 threads, 2.838s elapsed time, 4.464s cpu time, 0.134s GC time, factor 1.57)
23:29:05Finished Lifting_the_Exponent (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.22)
23:29:05Running Depth-First-Search (on 10.195.8.30) ...
23:29:05Timing CofGroups (2 threads, 2.186s elapsed time, 3.887s cpu time, 0.156s GC time, factor 1.78)
23:29:05Finished CofGroups (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.37)
23:29:05Running Skew_Heap (on 10.195.8.30) ...
23:29:05Running RefinementReactive (on 10.195.8.30) ...
23:29:05Running Lehmer (on 10.195.8.30) ...
23:29:05Timing Lazy-Lists-II (2 threads, 2.618s elapsed time, 4.507s cpu time, 0.184s GC time, factor 1.72)
23:29:05Finished Lazy-Lists-II (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.32)
23:29:05Running Blue_Eyes (on 10.195.8.30) ...
23:29:06Timing Sauer_Shelah_Lemma (2 threads, 2.414s elapsed time, 3.730s cpu time, 0.093s GC time, factor 1.55)
23:29:06Finished Sauer_Shelah_Lemma (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.22)
23:29:06Timing Laws_of_Large_Numbers (2 threads, 2.273s elapsed time, 3.297s cpu time, 0.145s GC time, factor 1.45)
23:29:06Finished Laws_of_Large_Numbers (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.13)
23:29:07Cartan_FP: theory Cartan_FP.Cartan
23:29:07Running HotelKeyCards (on 10.195.7.194) ...
23:29:07ShortestPath: theory ShortestPath.ShortestPath
23:29:07Running Hello_World (on 10.195.7.194) ...
23:29:07Timing Weighted_Arithmetic_Geometric_Mean (2 threads, 2.012s elapsed time, 3.418s cpu time, 0.109s GC time, factor 1.70)
23:29:07Finished Weighted_Arithmetic_Geometric_Mean (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.30)
23:29:07Timing FunWithFunctions (2 threads, 2.235s elapsed time, 3.422s cpu time, 0.097s GC time, factor 1.53)
23:29:07Depth-First-Search: theory Depth-First-Search.DFS
23:29:07Finished FunWithFunctions (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.23)
23:29:07RefinementReactive: theory RefinementReactive.Refinement
23:29:07RefinementReactive: theory RefinementReactive.Temporal
23:29:07Dynamic_Tables: theory Dynamic_Tables.Tables_real
23:29:07Running RIPEMD-160-SPARK (on 10.195.7.194) ...
23:29:07Blue_Eyes: theory Blue_Eyes.Blue_Eyes
23:29:07Running MHComputation (on 10.195.7.194) ...
23:29:07Timing Perfect-Number-Thm (2 threads, 2.560s elapsed time, 3.959s cpu time, 0.087s GC time, factor 1.55)
23:29:07Finished Perfect-Number-Thm (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.17)
23:29:07Timing Minkowskis_Theorem (2 threads, 2.780s elapsed time, 4.316s cpu time, 0.098s GC time, factor 1.55)
23:29:07Finished Minkowskis_Theorem (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.19)
23:29:08Skew_Heap: theory HOL-Data_Structures.Priority_Queue_Specs
23:29:08Skew_Heap: theory HOL-Data_Structures.Heaps
23:29:08HotelKeyCards: theory HOL-Library.LaTeXsugar
23:29:08Timing Ptolemys_Theorem (2 threads, 2.694s elapsed time, 3.658s cpu time, 0.109s GC time, factor 1.36)
23:29:08Finished Ptolemys_Theorem (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.15)
23:29:08Running Buffons_Needle (on 10.195.8.11) ...
23:29:08Running VeriComp (on 10.195.8.11) ...
23:29:08Lehmer: theory Lehmer.Lehmer
23:29:08Running ArrowImpossibilityGS (on 10.195.8.11) ...
23:29:09Running Free-Boolean-Algebra (on 10.195.8.11) ...
23:29:09Running FFT (on 10.195.8.11) ...
23:29:09HotelKeyCards: theory HotelKeyCards.Notation
23:29:09Hello_World: theory HOL-Library.Adhoc_Overloading
23:29:09HotelKeyCards: theory HotelKeyCards.Basis
23:29:09MHComputation: theory MHComputation.MHComputation
23:29:09Dynamic_Tables: theory Dynamic_Tables.Tables_nat
23:29:09RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
23:29:09HotelKeyCards: theory HotelKeyCards.State
23:29:09HotelKeyCards: theory HotelKeyCards.Trace
23:29:09Hello_World: theory HOL-Library.Monad_Syntax
23:29:09Timing Depth-First-Search (2 threads, 1.649s elapsed time, 2.632s cpu time, 0.059s GC time, factor 1.60)
23:29:09Finished Depth-First-Search (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.18)
23:29:09Skew_Heap: theory Skew_Heap.Skew_Heap
23:29:09ShortestPath: theory ShortestPath.ShortestPathNeg
23:29:09Hello_World: theory Hello_World.IO
23:29:10Hello_World: theory Hello_World.HelloWorld
23:29:10Timing Cartan_FP (2 threads, 2.663s elapsed time, 4.573s cpu time, 0.143s GC time, factor 1.72)
23:29:10Finished Cartan_FP (0:00:16 elapsed time, 0:00:08 cpu time, factor 0.51)
23:29:10Running Combinatorics_Words_Graph_Lemma (on 10.195.8.42) ...
23:29:10RefinementReactive: theory RefinementReactive.Reactive
23:29:10Timing FileRefinement (2 threads, 9.232s elapsed time, 14.579s cpu time, 0.214s GC time, factor 1.58)
23:29:10Finished FileRefinement (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.46)
23:29:10Timing Comparison_Sort_Lower_Bound (2 threads, 8.843s elapsed time, 16.665s cpu time, 0.815s GC time, factor 1.88)
23:29:10Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.62)
23:29:10HotelKeyCards: theory HotelKeyCards.NewCard
23:29:10VeriComp: theory VeriComp.Behaviour
23:29:10VeriComp: theory VeriComp.Transfer_Extras
23:29:10HotelKeyCards: theory HotelKeyCards.Equivalence
23:29:10Timing Blue_Eyes (2 threads, 2.400s elapsed time, 3.267s cpu time, 0.124s GC time, factor 1.36)
23:29:10Finished Blue_Eyes (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.13)
23:29:10ArrowImpossibilityGS: theory HOL-Library.FuncSet
23:29:10FFT: theory FFT.FFT
23:29:10ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Utility
23:29:10Free-Boolean-Algebra: theory Free-Boolean-Algebra.Free_Boolean_Algebra
23:29:10VeriComp: theory VeriComp.Well_founded
23:29:11Timing MuchAdoAboutTwo (2 threads, 10.115s elapsed time, 17.797s cpu time, 1.485s GC time, factor 1.76)
23:29:11Finished MuchAdoAboutTwo (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.58)
23:29:11VeriComp: theory VeriComp.Inf
23:29:11Running Relational-Incorrectness-Logic (on 10.195.8.42) ...
23:29:11VeriComp: theory VeriComp.Lifting_Simulation_To_Bisimulation
23:29:11Running Gray_Codes (on 10.195.8.42) ...
23:29:11Running Source_Coding_Theorem (on 10.195.8.42) ...
23:29:11Timing Skew_Heap (2 threads, 3.062s elapsed time, 3.730s cpu time, 0.205s GC time, factor 1.22)
23:29:12Finished Skew_Heap (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.09)
23:29:12Timing RIPEMD-160-SPARK (2 threads, 1.997s elapsed time, 2.071s cpu time, 0.031s GC time, factor 1.04)
23:29:12Finished RIPEMD-160-SPARK (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.92)
23:29:12Timing Lehmer (2 threads, 2.452s elapsed time, 3.903s cpu time, 0.095s GC time, factor 1.59)
23:29:12Finished Lehmer (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.21)
23:29:12ArrowImpossibilityGS: theory ArrowImpossibilityGS.Arrow_Order
23:29:12VeriComp: theory VeriComp.Semantics
23:29:12Buffons_Needle: theory Buffons_Needle.Buffons_Needle
23:29:12ArrowImpossibilityGS: theory ArrowImpossibilityGS.GS
23:29:12Running Imperative_Insertion_Sort (on 10.195.8.42) ...
23:29:14VeriComp: theory VeriComp.Language
23:29:14VeriComp: theory VeriComp.Simulation
23:29:14Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
23:29:14Gray_Codes: theory Gray_Codes.Encoding_Nat
23:29:14Hello_World: theory Hello_World.HelloWorld_Proof
23:29:14Timing FFT (2 threads, 2.337s elapsed time, 3.648s cpu time, 0.084s GC time, factor 1.56)
23:29:14Finished FFT (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.24)
23:29:14Timing Free-Boolean-Algebra (2 threads, 2.215s elapsed time, 2.658s cpu time, 0.065s GC time, factor 1.20)
23:29:14Finished Free-Boolean-Algebra (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.04)
23:29:14Running Conditional_Simplification (on 10.195.8.29) ...
23:29:15VeriComp: theory VeriComp.Compiler
23:29:15Timing ShortestPath (2 threads, 6.905s elapsed time, 9.757s cpu time, 1.470s GC time, factor 1.41)
23:29:15Finished ShortestPath (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.27)
23:29:15Relational-Incorrectness-Logic: theory Relational-Incorrectness-Logic.RelationalIncorrectness
23:29:15Gray_Codes: theory Gray_Codes.Code_Word_Dist
23:29:15VeriComp: theory VeriComp.Fixpoint
23:29:15Running DigitsInBase (on 10.195.8.29) ...
23:29:15Hello_World: theory Hello_World.RunningCodeFromIsabelle
23:29:15Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
23:29:16Combinatorics_Words_Graph_Lemma: theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
23:29:16Gray_Codes: theory Gray_Codes.Non_Boolean_Gray
23:29:16Timing Hello_World (2 threads, 5.742s elapsed time, 3.101s cpu time, 0.107s GC time, factor 0.54)
23:29:16Finished Hello_World (0:00:07 elapsed time, 0:00:04 cpu time, factor 0.62)
23:29:16Timing MHComputation (2 threads, 5.900s elapsed time, 6.156s cpu time, 0.472s GC time, factor 1.04)
23:29:16Finished MHComputation (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.01)
23:29:16Running Irrationals_From_THEBOOK (on 10.195.8.29) ...
23:29:16Running Discrete_Summation (on 10.195.8.29) ...
23:29:16Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
23:29:16Running General-Triangle (on 10.195.8.29) ...
23:29:17Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
23:29:17Conditional_Simplification: theory HOL-Library.LaTeXsugar
23:29:17Timing Dynamic_Tables (2 threads, 8.181s elapsed time, 15.984s cpu time, 0.876s GC time, factor 1.95)
23:29:17Finished Dynamic_Tables (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.66)
23:29:17Conditional_Simplification: theory Conditional_Simplification.CS_Tools
23:29:17Conditional_Simplification: theory Conditional_Simplification.IHOL_CS
23:29:17Timing HotelKeyCards (2 threads, 7.250s elapsed time, 13.447s cpu time, 0.565s GC time, factor 1.85)
23:29:17Finished HotelKeyCards (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.64)
23:29:17Timing Combinatorics_Words_Graph_Lemma (2 threads, 2.640s elapsed time, 4.224s cpu time, 0.142s GC time, factor 1.60)
23:29:17Finished Combinatorics_Words_Graph_Lemma (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.29)
23:29:17Running Open_Induction (on of2.proof.cit.tum.de) ...
23:29:17Running Card_Number_Partitions (on of2.proof.cit.tum.de) ...
23:29:17Running Surprise_Paradox (on of2.proof.cit.tum.de) ...
23:29:17Conditional_Simplification: theory Conditional_Simplification.Reference_Prerequisites
23:29:17Running Fisher_Yates (on of2.proof.cit.tum.de) ...
23:29:17Conditional_Simplification: theory Conditional_Simplification.CS_Reference
23:29:18Open_Induction: theory Open_Induction.Restricted_Predicates
23:29:18Running Lucas_Theorem (on of4.proof.cit.tum.de) ...
23:29:18Running ClockSynchInst (on of4.proof.cit.tum.de) ...
23:29:18Running Aristotles_Assertoric_Syllogistic (on of4.proof.cit.tum.de) ...
23:29:18Discrete_Summation: theory Discrete_Summation.Discrete_Summation
23:29:18Running Ackermanns_not_PR (on of4.proof.cit.tum.de) ...
23:29:18Discrete_Summation: theory HOL-Combinatorics.Stirling
23:29:18General-Triangle: theory General-Triangle.GeneralTriangle
23:29:18Open_Induction: theory Open_Induction.Open_Induction
23:29:18Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
23:29:18Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
23:29:18Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
23:29:18Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
23:29:18Timing Conditional_Simplification (2 threads, 1.145s elapsed time, 1.826s cpu time, 0.061s GC time, factor 1.59)
23:29:18Finished Conditional_Simplification (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.14)
23:29:19Fisher_Yates: theory Fisher_Yates.Fisher_Yates
23:29:19ClockSynchInst: theory ClockSynchInst.LynchInstance
23:29:19ClockSynchInst: theory ClockSynchInst.ICAInstance
23:29:19Aristotles_Assertoric_Syllogistic: theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
23:29:19Discrete_Summation: theory Discrete_Summation.Factorials
23:29:19Ackermanns_not_PR: theory Ackermanns_not_PR.Primrec
23:29:19Lucas_Theorem: theory Lucas_Theorem.Lucas_Theorem
23:29:19DigitsInBase: theory DigitsInBase.DigitsInBase
23:29:19Timing Aristotles_Assertoric_Syllogistic (6 threads, 0.231s elapsed time, 0.550s cpu time, 0.019s GC time, factor 2.38)
23:29:19Finished Aristotles_Assertoric_Syllogistic (0:00:01 elapsed time)
23:29:19Timing Open_Induction (6 threads, 1.066s elapsed time, 2.691s cpu time, 0.092s GC time, factor 2.52)
23:29:19Finished Open_Induction (0:00:02 elapsed time, 0:00:03 cpu time)
23:29:19Discrete_Summation: theory Discrete_Summation.Summation_Conversion
23:29:19Timing VeriComp (2 threads, 7.593s elapsed time, 12.967s cpu time, 0.666s GC time, factor 1.71)
23:29:19Finished VeriComp (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.54)
23:29:19Timing Card_Number_Partitions (6 threads, 0.871s elapsed time, 3.787s cpu time, 0.109s GC time, factor 4.35)
23:29:19Finished Card_Number_Partitions (0:00:02 elapsed time, 0:00:04 cpu time)
23:29:20Timing General-Triangle (2 threads, 1.202s elapsed time, 1.775s cpu time, 0.057s GC time, factor 1.48)
23:29:20Finished General-Triangle (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.11)
23:29:20Timing Surprise_Paradox (6 threads, 1.070s elapsed time, 1.808s cpu time, 0.118s GC time, factor 1.69)
23:29:20Finished Surprise_Paradox (0:00:02 elapsed time)
23:29:20Timing ClockSynchInst (6 threads, 0.882s elapsed time, 3.606s cpu time, 0.099s GC time, factor 4.09)
23:29:20Finished ClockSynchInst (0:00:01 elapsed time, 0:00:04 cpu time)
23:29:20Irrationals_From_THEBOOK: theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
23:29:20Timing Ackermanns_not_PR (6 threads, 0.793s elapsed time, 1.654s cpu time, 0.051s GC time, factor 2.09)
23:29:20Finished Ackermanns_not_PR (0:00:01 elapsed time)
23:29:20Discrete_Summation: theory Discrete_Summation.Examples
23:29:20Timing Fisher_Yates (6 threads, 1.092s elapsed time, 3.156s cpu time, 0.121s GC time, factor 2.89)
23:29:20Finished Fisher_Yates (0:00:02 elapsed time, 0:00:04 cpu time)
23:29:20Timing Lucas_Theorem (6 threads, 0.667s elapsed time, 2.128s cpu time, 0.062s GC time, factor 3.19)
23:29:20Finished Lucas_Theorem (0:00:02 elapsed time, 0:00:03 cpu time)
23:29:21Timing RefinementReactive (2 threads, 12.534s elapsed time, 20.418s cpu time, 1.610s GC time, factor 1.63)
23:29:21Finished RefinementReactive (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.52)
23:29:21Timing Gray_Codes (2 threads, 6.797s elapsed time, 10.940s cpu time, 0.412s GC time, factor 1.61)
23:29:21Finished Gray_Codes (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.44)
23:29:22Timing Buffons_Needle (2 threads, 8.358s elapsed time, 14.066s cpu time, 0.345s GC time, factor 1.68)
23:29:22Finished Buffons_Needle (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.44)
23:29:22Timing ArrowImpossibilityGS (2 threads, 10.029s elapsed time, 17.451s cpu time, 1.707s GC time, factor 1.74)
23:29:22Finished ArrowImpossibilityGS (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.59)
23:29:23Timing Imperative_Insertion_Sort (2 threads, 7.079s elapsed time, 12.107s cpu time, 0.318s GC time, factor 1.71)
23:29:23Finished Imperative_Insertion_Sort (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.50)
23:29:24Timing Source_Coding_Theorem (2 threads, 6.699s elapsed time, 10.490s cpu time, 0.345s GC time, factor 1.57)
23:29:24Finished Source_Coding_Theorem (0:00:10 elapsed time, 0:00:14 cpu time, factor 1.34)
23:29:24Timing Discrete_Summation (2 threads, 5.388s elapsed time, 9.954s cpu time, 0.245s GC time, factor 1.85)
23:29:24Finished Discrete_Summation (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.58)
23:29:25Timing Relational-Incorrectness-Logic (2 threads, 9.818s elapsed time, 15.066s cpu time, 1.164s GC time, factor 1.53)
23:29:25Finished Relational-Incorrectness-Logic (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.37)
23:29:26Timing Irrationals_From_THEBOOK (2 threads, 5.188s elapsed time, 7.428s cpu time, 0.195s GC time, factor 1.43)
23:29:26Finished Irrationals_From_THEBOOK (0:00:09 elapsed time, 0:00:11 cpu time, factor 1.21)
23:29:26Timing DigitsInBase (2 threads, 6.790s elapsed time, 9.227s cpu time, 0.395s GC time, factor 1.36)
23:29:26Finished DigitsInBase (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.23)
23:29:41Running Distributed_Distinct_Elements (on 10.195.6.179) ...
23:29:41Running Boolos_Curious_Inference (on 10.195.6.179) ...
23:29:41Running Bondy (on of1-proof+8-15) ...
23:29:41Running Roy_Floyd_Warshall (on of1-proof+0-7) ...
23:29:42Bondy: theory Bondy.Bondy
23:29:42Roy_Floyd_Warshall: theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
23:29:43Running Involutions2Squares (on of3.proof.cit.tum.de) ...
23:29:43Running Monad_Normalisation (on of3.proof.cit.tum.de) ...
23:29:43Running Liouville_Numbers (on of3.proof.cit.tum.de) ...
23:29:43Running Sophomores_Dream (on of3.proof.cit.tum.de) ...
23:29:43Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo2
23:29:43Boolos_Curious_Inference: theory Boolos_Curious_Inference.Boo1
23:29:43Involutions2Squares: theory Involutions2Squares.Involutions2Squares
23:29:43Timing Roy_Floyd_Warshall (8 threads, 0.258s elapsed time, 0.517s cpu time, 0.021s GC time, factor 2.00)
23:29:43Finished Roy_Floyd_Warshall (0:00:01 elapsed time)
23:29:43Timing Bondy (8 threads, 0.319s elapsed time, 0.417s cpu time, 0.016s GC time, factor 1.31)
23:29:43Finished Bondy (0:00:01 elapsed time)
23:29:44Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
23:29:44Running Intro_Dest_Elim (on 10.195.8.49) ...
23:29:44Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
23:29:44Sophomores_Dream: theory Sophomores_Dream.Sophomores_Dream
23:29:44Running Card_Equiv_Relations (on 10.195.8.49) ...
23:29:44Running Example-Submission (on 10.195.8.49) ...
23:29:44Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
23:29:44Running Ordinals_and_Cardinals (on 10.195.8.49) ...
23:29:44Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
23:29:45Timing Boolos_Curious_Inference (2 threads, 0.741s elapsed time, 1.290s cpu time, 0.048s GC time, factor 1.74)
23:29:45Finished Boolos_Curious_Inference (0:00:02 elapsed time)
23:29:45Timing Involutions2Squares (6 threads, 0.880s elapsed time, 2.151s cpu time, 0.079s GC time, factor 2.44)
23:29:45Finished Involutions2Squares (0:00:01 elapsed time)
23:29:45Timing Liouville_Numbers (6 threads, 0.678s elapsed time, 1.747s cpu time, 0.047s GC time, factor 2.58)
23:29:45Finished Liouville_Numbers (0:00:02 elapsed time)
23:29:45Timing Sophomores_Dream (6 threads, 0.509s elapsed time, 1.607s cpu time, 0.049s GC time, factor 3.16)
23:29:45Finished Sophomores_Dream (0:00:02 elapsed time)
23:29:45Timing Monad_Normalisation (6 threads, 0.592s elapsed time, 0.960s cpu time, 0.031s GC time, factor 1.62)
23:29:45Finished Monad_Normalisation (0:00:02 elapsed time)
23:29:46Intro_Dest_Elim: theory HOL-Library.LaTeXsugar
23:29:46Intro_Dest_Elim: theory Intro_Dest_Elim.IHOL_IDE
23:29:46Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
23:29:46Example-Submission: theory Example-Submission.Submission
23:29:46Intro_Dest_Elim: theory Intro_Dest_Elim.Reference_Prerequisites
23:29:46Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Equiv_Relations
23:29:46Timing Ordinals_and_Cardinals (2 threads, 0.130s elapsed time, 0.165s cpu time, 0.000s GC time, factor 1.27)
23:29:46Finished Ordinals_and_Cardinals (0:00:01 elapsed time)
23:29:46Intro_Dest_Elim: theory Intro_Dest_Elim.IDE_Reference
23:29:46Card_Equiv_Relations: theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
23:29:46Timing Example-Submission (2 threads, 0.260s elapsed time, 0.296s cpu time, 0.000s GC time, factor 1.14)
23:29:47Finished Example-Submission (0:00:02 elapsed time)
23:29:47Timing Intro_Dest_Elim (2 threads, 1.215s elapsed time, 1.309s cpu time, 0.056s GC time, factor 1.08)
23:29:47Finished Intro_Dest_Elim (0:00:02 elapsed time)
23:29:48Timing Card_Equiv_Relations (2 threads, 1.476s elapsed time, 2.240s cpu time, 0.054s GC time, factor 1.52)
23:29:48Finished Card_Equiv_Relations (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.15)
23:29:53Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
23:29:53Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
23:29:54Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
23:29:54Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
23:29:54Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
23:29:54Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
23:29:55Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
23:29:55Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:30:00Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
23:30:02Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
23:30:02Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
23:30:02Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
23:30:03Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
23:30:04Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
23:30:08Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
23:30:09Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
23:30:09Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
23:30:10Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
23:30:14Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
23:30:15Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
23:30:15Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
23:30:16Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
23:30:19Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
23:30:20Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
23:30:29Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
23:30:30Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
23:30:38Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
23:30:41Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
23:30:42Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
23:30:46Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
23:32:32Timing Distributed_Distinct_Elements (2 threads, 150.791s elapsed time, 277.180s cpu time, 37.167s GC time, factor 1.84)
23:32:32Finished Distributed_Distinct_Elements (0:02:48 elapsed time, 0:04:56 cpu time, factor 1.75)
23:38:03Timing CAVA_Setup (2 threads, 1472.029s elapsed time, 2562.664s cpu time, 877.129s GC time, factor 1.74)
23:38:03Finished CAVA_Setup (0:25:50 elapsed time, 0:44:32 cpu time, factor 1.72)
23:38:10Running CAVA_LTL_Modelchecker (on 10.195.8.40) ...
23:38:14CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
23:38:18CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
23:38:18CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
23:38:20CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
23:40:10CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
23:40:10CAVA_LTL_Modelchecker: theory LTL.Rewriting
23:40:10CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
23:40:12CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
23:40:18CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
23:40:22CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
23:40:25CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
23:40:27CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
23:40:29CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
23:40:30CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
23:43:55CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
23:44:57CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
23:44:57CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
23:45:08Timing CAVA_LTL_Modelchecker (2 threads, 411.181s elapsed time, 523.123s cpu time, 43.140s GC time, factor 1.27)
23:45:08Finished CAVA_LTL_Modelchecker (0:06:57 elapsed time, 0:08:50 cpu time, factor 1.27)
23:45:24Timing HOL-ODE-Numerics (2 threads, 2500.865s elapsed time, 4572.524s cpu time, 650.788s GC time, factor 1.83)
23:45:24Finished HOL-ODE-Numerics (0:43:38 elapsed time, 1:18:59 cpu time, factor 1.81)
23:45:29Building Lorenz_Approximation (on of3.proof.cit.tum.de) ...
23:45:30Running HOL-ODE-ARCH-COMP (on of3.proof.cit.tum.de) ...
23:45:30Running HOL-ODE-Examples (on of3.proof.cit.tum.de) ...
23:45:30Running Poincare_Bendixson (on of3.proof.cit.tum.de) ...
23:45:31HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
23:45:31Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
23:45:31HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
23:45:31Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
23:45:31HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
23:45:32Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
23:45:32HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
23:45:32Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
23:45:34Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
23:45:36Poincare_Bendixson: theory Poincare_Bendixson.Invariance
23:45:37Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
23:45:38Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
23:45:39Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
23:45:42Poincare_Bendixson: theory Poincare_Bendixson.Examples
23:45:48Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
23:46:23Timing Poincare_Bendixson (6 threads, 50.269s elapsed time, 130.824s cpu time, 9.175s GC time, factor 2.60)
23:46:23Finished Poincare_Bendixson (0:00:52 elapsed time, 0:02:13 cpu time, factor 2.54)
23:46:36HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
23:47:14Timing HOL-ODE-Examples (6 threads, 101.861s elapsed time, 405.146s cpu time, 14.050s GC time, factor 3.98)
23:47:14Finished HOL-ODE-Examples (0:01:44 elapsed time, 0:06:47 cpu time, factor 3.91)
23:47:46Timing Lorenz_Approximation (6 threads, 115.319s elapsed time, 283.902s cpu time, 33.664s GC time, factor 2.46)
23:47:46Finished Lorenz_Approximation (0:02:15 elapsed time, 0:05:19 cpu time, factor 2.35)
23:47:47Running Lorenz_C0 (on of3.proof.cit.tum.de) ...
23:47:47Running Lorenz_C1 (on of3.proof.cit.tum.de) ...
23:47:49Lorenz_C0: theory Lorenz_C0.Lorenz_C0
23:47:49Lorenz_C1: theory Lorenz_C1.Lorenz_C1
23:47:50Timing Lorenz_C1 (6 threads, 0.641s elapsed time, 0.915s cpu time, 0.020s GC time, factor 1.43)
23:47:50Finished Lorenz_C1 (0:00:02 elapsed time)
23:48:00Timing HOL-ODE-ARCH-COMP (6 threads, 148.017s elapsed time, 425.375s cpu time, 38.206s GC time, factor 2.87)
23:48:00Finished HOL-ODE-ARCH-COMP (0:02:30 elapsed time, 0:07:07 cpu time, factor 2.85)
23:51:38Timing Crypto_Standards (2 threads, 3394.676s elapsed time, 6400.817s cpu time, 1180.837s GC time, factor 1.89)
23:51:38Finished Crypto_Standards (0:56:44 elapsed time, 1:46:59 cpu time, factor 1.89)
23:52:10Timing Lorenz_C0 (6 threads, 260.448s elapsed time, 1477.046s cpu time, 20.054s GC time, factor 5.67)
23:52:10Finished Lorenz_C0 (0:04:22 elapsed time, 0:24:39 cpu time, factor 5.63)
23:58:49Timing Modular_arithmetic_LLL_and_HNF_algorithms (2 threads, 2441.879s elapsed time, 4336.107s cpu time, 1117.865s GC time, factor 1.78)
23:58:49Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:41:58 elapsed time, 1:14:35 cpu time, factor 1.78)
00:05:18Timing CZH_Universal_Constructions (2 threads, 4033.679s elapsed time, 6201.039s cpu time, 2053.304s GC time, factor 1.54)
00:05:18Finished CZH_Universal_Constructions (1:07:18 elapsed time, 1:43:27 cpu time, factor 1.54)
00:05:3000:05:30Finished at Wed Dec 6 00:05:30 GMT+1 2023
00:05:301:29:09 elapsed time, 56:11:05 cpu time, factor 37.81
00:05:31Started calculate disk usage of build
00:05:31Finished Calculation of disk usage of build in 0 seconds
00:05:58Started calculate disk usage of workspace
00:05:58Finished Calculation of disk usage of workspace in 0 seconds
00:05:59Finished: SUCCESS