Skipping 884 KB.. Full Log

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