Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
02:00:31Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
02:00:31Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
02:00:31Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
02:00:31Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
02:00:31Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
02:00:32Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
02:00:33Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
02:00:33Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
02:00:33Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
02:00:34Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
02:00:34Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
02:00:34Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
02:00:38Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
02:00:42Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
02:01:10Preparing Game_Based_Crypto/document ...
02:01:21Finished Game_Based_Crypto/document (0:00:10 elapsed time)
02:01:21Preparing Game_Based_Crypto/outline ...
02:01:29Finished Game_Based_Crypto/outline (0:00:08 elapsed time)
02:01:29Timing Game_Based_Crypto (8 threads, 19.561s elapsed time, 115.443s cpu time, 2.147s GC time, factor 5.90)
02:01:29Finished Game_Based_Crypto (0:00:41 elapsed time, 0:02:35 cpu time, factor 3.80)
02:01:30Running Algebraic_VCs (on hpcisabelle/7) ...
02:01:31Algebraic_VCs: theory Algebraic_VCs.P2S2R
02:01:31Algebraic_VCs: theory Algebraic_VCs.VC_KAT_scratch
02:01:31Algebraic_VCs: theory Algebraic_VCs.VC_KAD_scratch
02:01:31Algebraic_VCs: theory HOL-Eisbach.Eisbach
02:01:31Algebraic_VCs: theory HOL-Hoare.Heap
02:01:31Algebraic_VCs: theory KAD.Domain_Semiring
02:01:32Algebraic_VCs: theory Algebraic_VCs.VC_KAT
02:01:35Algebraic_VCs: theory Algebraic_VCs.RKAT
02:01:35Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples
02:01:35Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples2
02:01:37Algebraic_VCs: theory Algebraic_VCs.RKAT_Models
02:01:37Algebraic_VCs: theory Algebraic_VCs.VC_RKAT
02:01:37Algebraic_VCs: theory Algebraic_VCs.VC_RKAT_Examples
02:01:47Algebraic_VCs: theory KAD.Antidomain_Semiring
02:02:07Algebraic_VCs: theory KAD.Range_Semiring
02:02:07Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Applications
02:02:30Algebraic_VCs: theory KAD.Modal_Kleene_Algebra
02:02:41Algebraic_VCs: theory Algebraic_VCs.Domain_Quantale
02:02:41Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Models
02:02:50Algebraic_VCs: theory Algebraic_VCs.VC_KAD
02:03:03Algebraic_VCs: theory Algebraic_VCs.Path_Model_Example
02:03:03Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples2
02:03:03Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples
02:03:03Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual
02:03:03Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf
02:03:03Algebraic_VCs: theory Algebraic_VCs.KAD_is_KAT
02:03:04Algebraic_VCs: theory Algebraic_VCs.Pointer_Examples
02:03:06Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf_Examples
02:03:06Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual_Examples
02:03:53Preparing Algebraic_VCs/document ...
02:03:58Finished Algebraic_VCs/document (0:00:05 elapsed time)
02:03:58Preparing Algebraic_VCs/outline ...
02:04:03Finished Algebraic_VCs/outline (0:00:04 elapsed time)
02:04:03Timing Algebraic_VCs (8 threads, 139.618s elapsed time, 337.679s cpu time, 7.744s GC time, factor 2.42)
02:04:03Finished Algebraic_VCs (0:02:22 elapsed time, 0:05:44 cpu time, factor 2.42)
02:04:03Running Continued_Fractions (on hpcisabelle/0) ...
02:04:05Continued_Fractions: theory HOL-Computational_Algebra.Squarefree
02:04:05Continued_Fractions: theory HOL-Library.Adhoc_Overloading
02:04:05Continued_Fractions: theory HOL-Decision_Procs.Dense_Linear_Order
02:04:05Continued_Fractions: theory HOL-Computational_Algebra.Fraction_Field
02:04:05Continued_Fractions: theory HOL-Computational_Algebra.Group_Closure
02:04:05Continued_Fractions: theory HOL-Computational_Algebra.Nth_Powers
02:04:05Continued_Fractions: theory HOL-Library.Case_Converter
02:04:05Continued_Fractions: theory HOL-Library.Code_Abstract_Nat
02:04:06Continued_Fractions: theory HOL-Library.Code_Target_Nat
02:04:06Continued_Fractions: theory HOL-Library.Monad_Syntax
02:04:06Continued_Fractions: theory HOL-Library.Code_Target_Int
02:04:06Continued_Fractions: theory HOL-Library.Complete_Partial_Order2
02:04:06Continued_Fractions: theory HOL-Library.IArray
02:04:06Continued_Fractions: theory HOL-Library.More_List
02:04:07Continued_Fractions: theory HOL-Library.Code_Lazy
02:04:07Continued_Fractions: theory HOL-Library.Simps_Case_Conv
02:04:07Continued_Fractions: theory HOL-Library.Code_Target_Numeral
02:04:07Continued_Fractions: theory HOL-Library.Stream
02:04:07Continued_Fractions: theory HOL-Library.Sublist
02:04:07Continued_Fractions: theory HOL-Library.Tree
02:04:08Continued_Fractions: theory HOL-Library.While_Combinator
02:04:08Continued_Fractions: theory HOL-Computational_Algebra.Normalized_Fraction
02:04:08Continued_Fractions: theory HOL-Computational_Algebra.Polynomial
02:04:09Continued_Fractions: theory HOL-Library.Lattice_Algebras
02:04:09Continued_Fractions: theory HOL-Library.Log_Nat
02:04:09Continued_Fractions: theory HOL-Number_Theory.Fib
02:04:09Continued_Fractions: theory Matrix.Utility
02:04:10Continued_Fractions: theory Polynomial_Factorization.Missing_List
02:04:10Continued_Fractions: theory HOL-Library.Linear_Temporal_Logic_on_Streams
02:04:12Continued_Fractions: theory Coinductive.Coinductive_Nat
02:04:14Continued_Fractions: theory Coinductive.Coinductive_List
02:04:14Continued_Fractions: theory Polynomial_Factorization.Missing_Multiset
02:04:14Continued_Fractions: theory Polynomial_Factorization.Prime_Factorization
02:04:15Continued_Fractions: theory HOL-Library.Interval
02:04:15Continued_Fractions: theory HOL-Library.Float
02:04:19Continued_Fractions: theory HOL-Library.Code_Target_Numeral_Float
02:04:19Continued_Fractions: theory HOL-Library.Interval_Float
02:04:20Continued_Fractions: theory HOL-Decision_Procs.Approximation_Bounds
02:04:20Continued_Fractions: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
02:04:20Continued_Fractions: theory HOL-Computational_Algebra.Polynomial_FPS
02:04:20Continued_Fractions: theory HOL-Computational_Algebra.Polynomial_Factorial
02:04:20Continued_Fractions: theory Coinductive.Lazy_LList
02:04:20Continued_Fractions: theory Coinductive.Coinductive_Stream
02:04:21Continued_Fractions: theory HOL-Computational_Algebra.Formal_Laurent_Series
02:04:22Continued_Fractions: theory Continued_Fractions.Continued_Fractions
02:04:24Continued_Fractions: theory HOL-Computational_Algebra.Computational_Algebra
02:04:26Continued_Fractions: theory HOL-Decision_Procs.Approximation
02:04:26Continued_Fractions: theory Continued_Fractions.Quadratic_Irrationals
02:04:26Continued_Fractions: theory Pell.Efficient_Discrete_Sqrt
02:04:26Continued_Fractions: theory Pell.Pell
02:04:28Continued_Fractions: theory Continued_Fractions.Sqrt_Nat_Cfrac
02:04:28Continued_Fractions: theory Continued_Fractions.E_CFrac
02:04:28Continued_Fractions: theory Pell.Pell_Algorithm
02:04:30Continued_Fractions: theory Continued_Fractions.Pell_Lifting
02:04:31Continued_Fractions: theory Continued_Fractions.Pell_Continued_Fraction
02:04:32Continued_Fractions: theory Continued_Fractions.Pell_Continued_Fraction_Tests
02:05:17Continued_Fractions: theory Continued_Fractions.Continued_Fraction_Approximation
02:06:04Preparing Continued_Fractions/document ...
02:06:18Finished Continued_Fractions/document (0:00:14 elapsed time)
02:06:18Preparing Continued_Fractions/outline ...
02:06:24Finished Continued_Fractions/outline (0:00:05 elapsed time)
02:06:24Timing Continued_Fractions (8 threads, 114.423s elapsed time, 751.507s cpu time, 18.600s GC time, factor 6.57)
02:06:24Finished Continued_Fractions (0:01:58 elapsed time, 0:12:39 cpu time, factor 6.42)
02:06:25Building Transitive_Models (on hpcisabelle/1) ...
02:06:25Transitive_Models: theory Transitive_Models.Utils
02:06:25Transitive_Models: theory Transitive_Models.Nat_Miscellanea
02:06:25Transitive_Models: theory Transitive_Models.Eclose_Absolute
02:06:25Transitive_Models: theory Transitive_Models.M_Basic_No_Repl
02:06:25Transitive_Models: theory Transitive_Models.Synthetic_Definition
02:06:26Transitive_Models: theory Transitive_Models.ZF_Miscellanea
02:06:26Transitive_Models: theory Transitive_Models.Renaming
02:06:26Transitive_Models: theory Transitive_Models.Renaming_Auto
02:06:27Transitive_Models: theory Transitive_Models.Datatype_absolute
02:06:27Transitive_Models: theory Transitive_Models.Internalize
02:06:27Transitive_Models: theory Transitive_Models.Recursion_Thms
02:06:28Transitive_Models: theory Transitive_Models.Rec_Separation
02:06:29Transitive_Models: theory Transitive_Models.Satisfies_absolute
02:06:29Transitive_Models: theory Transitive_Models.DPow_absolute
02:06:30Transitive_Models: theory Transitive_Models.Internalizations
02:06:30Transitive_Models: theory Transitive_Models.Least
02:06:30Transitive_Models: theory Transitive_Models.Higher_Order_Constructs
02:06:30Transitive_Models: theory Transitive_Models.Relativization
02:06:32Transitive_Models: theory Transitive_Models.Discipline_Base
02:06:32Transitive_Models: theory Transitive_Models.Arities
02:06:33Transitive_Models: theory Transitive_Models.Discipline_Function
02:06:35Transitive_Models: theory Transitive_Models.Discipline_Cardinal
02:06:36Transitive_Models: theory Transitive_Models.Univ_Relative
02:06:36Transitive_Models: theory Transitive_Models.Lambda_Replacement
02:06:38Transitive_Models: theory Transitive_Models.Cardinal_Relative
02:06:38Transitive_Models: theory Transitive_Models.FiniteFun_Relative
02:06:39Transitive_Models: theory Transitive_Models.CardinalArith_Relative
02:06:41Transitive_Models: theory Transitive_Models.Aleph_Relative
02:06:42Transitive_Models: theory Transitive_Models.Cardinal_AC_Relative
02:06:43Transitive_Models: theory Transitive_Models.ZF_Library_Relative
02:06:45Transitive_Models: theory Transitive_Models.Replacement_Lepoll
02:06:45Transitive_Models: theory Transitive_Models.Cardinal_Library_Relative
02:06:47Transitive_Models: theory Transitive_Models.Delta_System_Relative
02:06:48Transitive_Models: theory Transitive_Models.Partial_Functions_Relative
02:06:48Transitive_Models: theory Transitive_Models.Pointed_DC_Relative
02:07:18Preparing Transitive_Models/document ...
02:07:54Finished Transitive_Models/document (0:00:35 elapsed time)
02:07:54Preparing Transitive_Models/outline ...
02:08:13Finished Transitive_Models/outline (0:00:19 elapsed time)
02:08:13Timing Transitive_Models (8 threads, 49.325s elapsed time, 212.302s cpu time, 4.912s GC time, factor 4.30)
02:08:13Finished Transitive_Models (0:00:52 elapsed time, 0:03:38 cpu time, factor 4.19)
02:08:14Running HOL-Proofs-Lambda (on hpcisabelle/2) ...
02:08:16HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation
02:08:16HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int
02:08:16HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda
02:08:16HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder
02:08:19HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication
02:08:19HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed
02:08:19HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType
02:08:19HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta
02:08:20HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta
02:08:20HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi
02:08:20HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm
02:08:21HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization
02:08:22HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm
02:08:22HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm
02:10:35Preparing HOL-Proofs-Lambda/document ...
02:10:41Finished HOL-Proofs-Lambda/document (0:00:05 elapsed time)
02:10:41Preparing HOL-Proofs-Lambda/outline ...
02:10:44Finished HOL-Proofs-Lambda/outline (0:00:03 elapsed time)
02:10:44Timing HOL-Proofs-Lambda (8 threads, 138.607s elapsed time, 161.766s cpu time, 4.137s GC time, factor 1.17)
02:10:44Finished HOL-Proofs-Lambda (0:02:21 elapsed time, 0:02:46 cpu time, factor 1.18)
02:10:45Building Monad_Memo_DP (on hpcisabelle/3) ...
02:10:46Monad_Memo_DP: theory Deriving.Derive_Manager
02:10:46Monad_Memo_DP: theory HOL-Eisbach.Eisbach
02:10:46Monad_Memo_DP: theory Deriving.Generator_Aux
02:10:46Monad_Memo_DP: theory HOL-Library.AList
02:10:46Monad_Memo_DP: theory HOL-Library.Code_Abstract_Nat
02:10:46Monad_Memo_DP: theory HOL-Library.Case_Converter
02:10:46Monad_Memo_DP: theory HOL-Library.Adhoc_Overloading
02:10:46Monad_Memo_DP: theory HOL-Library.Code_Target_Int
02:10:46Monad_Memo_DP: theory HOL-Library.IArray
02:10:46Monad_Memo_DP: theory HOL-Library.Code_Target_Nat
02:10:47Monad_Memo_DP: theory HOL-Library.Monad_Syntax
02:10:47Monad_Memo_DP: theory HOL-Library.Nat_Bijection
02:10:47Monad_Memo_DP: theory HOL-Library.Old_Datatype
02:10:47Monad_Memo_DP: theory HOL-Library.State_Monad
02:10:47Monad_Memo_DP: theory HOL-Library.Code_Target_Numeral
02:10:47Monad_Memo_DP: theory HOL-Library.Simps_Case_Conv
02:10:47Monad_Memo_DP: theory HOL-Library.Extended
02:10:47Monad_Memo_DP: theory HOL-Library.Product_Lexorder
02:10:48Monad_Memo_DP: theory HOL-Library.RBT_Impl
02:10:48Monad_Memo_DP: theory HOL-Library.Sublist
02:10:48Monad_Memo_DP: theory HOL-Library.Tree
02:10:48Monad_Memo_DP: theory Monad_Memo_DP.Ground_Function
02:10:48Monad_Memo_DP: theory HOL-Library.Countable
02:10:48Monad_Memo_DP: theory Monad_Memo_DP.Indexing
02:10:49Monad_Memo_DP: theory Monad_Memo_DP.State_Monad_Ext
02:10:49Monad_Memo_DP: theory HOL-Library.Mapping
02:10:49Monad_Memo_DP: theory Monad_Memo_DP.Pure_Monad
02:10:49Monad_Memo_DP: theory Monad_Memo_DP.DP_CRelVS
02:10:49Monad_Memo_DP: theory Monad_Memo_DP.Solve_Cong
02:10:50Monad_Memo_DP: theory HOL-Imperative_HOL.Heap
02:10:50Monad_Memo_DP: theory Monad_Memo_DP.State_Heap_Misc
02:10:50Monad_Memo_DP: theory Show.Show
02:10:50Monad_Memo_DP: theory Monad_Memo_DP.Memory
02:10:51Monad_Memo_DP: theory Monad_Memo_DP.Bottom_Up_Computation
02:10:51Monad_Memo_DP: theory Monad_Memo_DP.Pair_Memory
02:10:51Monad_Memo_DP: theory Show.Show_Instances
02:10:51Monad_Memo_DP: theory HOL-Imperative_HOL.Heap_Monad
02:10:54Monad_Memo_DP: theory HOL-Imperative_HOL.Array
02:10:55Monad_Memo_DP: theory HOL-Imperative_HOL.Ref
02:10:55Monad_Memo_DP: theory HOL-Imperative_HOL.Imperative_HOL
02:10:55Monad_Memo_DP: theory Monad_Memo_DP.Heap_Monad_Ext
02:10:55Monad_Memo_DP: theory Monad_Memo_DP.State_Heap
02:10:57Monad_Memo_DP: theory Monad_Memo_DP.DP_CRelVH
02:10:58Monad_Memo_DP: theory Monad_Memo_DP.Transform_Cmd
02:10:58Monad_Memo_DP: theory Monad_Memo_DP.Bottom_Up_Computation_Heap
02:10:58Monad_Memo_DP: theory Monad_Memo_DP.Memory_Heap
02:10:58Monad_Memo_DP: theory Monad_Memo_DP.State_Main
02:11:00Monad_Memo_DP: theory Monad_Memo_DP.Example_Misc
02:11:00Monad_Memo_DP: theory Monad_Memo_DP.Heap_Main
02:11:07Monad_Memo_DP: theory Monad_Memo_DP.Heap_Default
02:11:07Monad_Memo_DP: theory Monad_Memo_DP.Tracing
02:11:07Monad_Memo_DP: theory Monad_Memo_DP.Knapsack
02:11:53Monad_Memo_DP: theory HOL-Library.RBT
02:11:53Monad_Memo_DP: theory HOL-Library.RBT_Mapping
02:11:54Monad_Memo_DP: theory Monad_Memo_DP.Counting_Tiles
02:11:54Monad_Memo_DP: theory Monad_Memo_DP.CYK
02:11:54Monad_Memo_DP: theory Monad_Memo_DP.Longest_Common_Subsequence
02:11:56Monad_Memo_DP: theory Monad_Memo_DP.OptBST
02:11:56Monad_Memo_DP: theory Monad_Memo_DP.Bellman_Ford
02:11:57Monad_Memo_DP: theory Monad_Memo_DP.Min_Ed_Dist0
02:12:11Monad_Memo_DP: theory Monad_Memo_DP.All_Examples
02:13:19Preparing Monad_Memo_DP/document ...
02:13:27Finished Monad_Memo_DP/document (0:00:08 elapsed time)
02:13:27Preparing Monad_Memo_DP/outline ...
02:13:33Finished Monad_Memo_DP/outline (0:00:05 elapsed time)
02:13:33Timing Monad_Memo_DP (8 threads, 126.881s elapsed time, 815.918s cpu time, 16.993s GC time, factor 6.43)
02:13:33Finished Monad_Memo_DP (0:02:33 elapsed time, 0:14:36 cpu time, factor 5.73)
02:13:33Building Conditional_Transfer_Rule (on hpcisabelle/4) ...
02:13:35Conditional_Transfer_Rule: theory SpecCheck.SpecCheck_Base
02:13:35Conditional_Transfer_Rule: theory SpecCheck.SpecCheck_Show
02:13:35Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.CTR_Tools
02:13:35Conditional_Transfer_Rule: theory HOL-Library.LaTeXsugar
02:13:35Conditional_Transfer_Rule: theory HOL-Library.Conditional_Parametricity
02:13:35Conditional_Transfer_Rule: theory SpecCheck.SpecCheck_Generators
02:13:35Conditional_Transfer_Rule: theory SpecCheck.SpecCheck_Output_Style
02:13:35Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.Reference_Prerequisites
02:13:35Conditional_Transfer_Rule: theory SpecCheck.SpecCheck_Shrink
02:13:36Conditional_Transfer_Rule: theory SpecCheck.SpecCheck
02:13:36Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.UD
02:13:36Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.IML_UT
02:13:36Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.UD_Tests
02:13:36Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.CTR
02:13:37Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.CTR_Tests
02:13:38Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.UD_Reference
02:13:38Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.CTR_Introduction
02:13:38Conditional_Transfer_Rule: theory Conditional_Transfer_Rule.CTR_Reference
02:13:44Preparing Conditional_Transfer_Rule/document ...
02:13:50Finished Conditional_Transfer_Rule/document (0:00:05 elapsed time)
02:13:50Preparing Conditional_Transfer_Rule/outline ...
02:13:56Finished Conditional_Transfer_Rule/outline (0:00:05 elapsed time)
02:13:56Timing Conditional_Transfer_Rule (8 threads, 3.886s elapsed time, 7.261s cpu time, 0.127s GC time, factor 1.87)
02:13:56Finished Conditional_Transfer_Rule (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.75)
02:13:56Running Safe_Distance (on hpcisabelle/5) ...
02:13:59Safe_Distance: theory Pure-ex.Guess
02:13:59Safe_Distance: theory HOL-Computational_Algebra.Fraction_Field
02:13:59Safe_Distance: theory HOL-Decision_Procs.Dense_Linear_Order
02:13:59Safe_Distance: theory HOL-Library.Code_Abstract_Nat
02:13:59Safe_Distance: theory HOL-Library.Code_Target_Int
02:13:59Safe_Distance: theory HOL-Library.More_List
02:13:59Safe_Distance: theory HOL-Computational_Algebra.Field_as_Ring
02:13:59Safe_Distance: theory HOL-Library.Lattice_Algebras
02:13:59Safe_Distance: theory HOL-Library.Log_Nat
02:13:59Safe_Distance: theory HOL-Library.Code_Target_Nat
02:14:00Safe_Distance: theory HOL-Computational_Algebra.Polynomial
02:14:00Safe_Distance: theory HOL-Library.Code_Target_Numeral
02:14:01Safe_Distance: theory HOL-Computational_Algebra.Normalized_Fraction
02:14:07Safe_Distance: theory HOL-Library.Interval
02:14:07Safe_Distance: theory HOL-Library.Float
02:14:10Safe_Distance: theory HOL-Library.Code_Target_Numeral_Float
02:14:10Safe_Distance: theory HOL-Library.Interval_Float
02:14:12Safe_Distance: theory HOL-Decision_Procs.Approximation_Bounds
02:14:12Safe_Distance: theory HOL-Computational_Algebra.Polynomial_Factorial
02:14:14Safe_Distance: theory Sturm_Sequences.Misc_Polynomial
02:14:15Safe_Distance: theory Sturm_Sequences.Sturm_Library
02:14:15Safe_Distance: theory Sturm_Sequences.Sturm_Theorem
02:14:17Safe_Distance: theory Sturm_Sequences.Sturm_Method
02:14:17Safe_Distance: theory Sturm_Sequences.Sturm
02:14:17Safe_Distance: theory HOL-Decision_Procs.Approximation
02:15:04Safe_Distance: theory Safe_Distance.Safe_Distance
02:15:09Safe_Distance: theory Safe_Distance.Evaluation
02:15:09Safe_Distance: theory Safe_Distance.Safe_Distance_Reaction
02:15:42Preparing Safe_Distance/document ...
02:15:49Finished Safe_Distance/document (0:00:06 elapsed time)
02:15:49Preparing Safe_Distance/outline ...
02:15:52Finished Safe_Distance/outline (0:00:03 elapsed time)
02:15:52Timing Safe_Distance (8 threads, 101.162s elapsed time, 482.972s cpu time, 24.737s GC time, factor 4.77)
02:15:52Finished Safe_Distance (0:01:44 elapsed time, 0:08:08 cpu time, factor 4.68)
02:15:52Running Isabelle_Meta_Model (on hpcisabelle/6) ...
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Antiquote_Setup
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Cartouche_Examples
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_code_runtime
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_typedecl
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_code_target
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main0
02:15:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main2
02:15:55Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main1
02:15:55Isabelle_Meta_Model: theory Isabelle_Meta_Model.Init
02:15:59Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Pure
02:15:59Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_SML
02:15:59Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_init
02:15:59Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_init
02:16:01Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Pure
02:16:01Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Pure
02:16:02Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Isabelle
02:16:02Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_SML
02:16:18Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Isabelle
02:16:27Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Toy_extended
02:16:27Isabelle_Meta_Model: theory Isabelle_Meta_Model.Init_rbt
02:16:27Isabelle_Meta_Model: theory Isabelle_Meta_Model.Toy_Library_Static
02:16:28Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Toy
02:16:33Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Toy_extended
02:16:43Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_META
02:16:43Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Toy
02:16:43Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Toy
02:16:44Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Toy_extended
02:16:50Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_META
02:16:50Isabelle_Meta_Model: theory Isabelle_Meta_Model.Core_init
02:16:52Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_META
02:16:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_access
02:16:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_infra
02:16:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_ctxt
02:16:54Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_examp
02:16:55Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor2_examp
02:16:55Isabelle_Meta_Model: theory Isabelle_Meta_Model.Core
02:16:58Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer
02:17:01Isabelle_Meta_Model: theory Isabelle_Meta_Model.Toy_Library
02:17:01Isabelle_Meta_Model: theory Isabelle_Meta_Model.Generator_dynamic_sequential
02:17:01Isabelle_Meta_Model: theory Isabelle_Meta_Model.Generator_static
02:17:22Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_deep
02:17:22Isabelle_Meta_Model: theory Isabelle_Meta_Model.Rail
02:17:22Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_shallow
02:17:46Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_generated_generated
02:17:46Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_generated
02:18:07Preparing Isabelle_Meta_Model/document ...
02:18:14Finished Isabelle_Meta_Model/document (0:00:07 elapsed time)
02:18:14Preparing Isabelle_Meta_Model/outline ...
02:18:21Finished Isabelle_Meta_Model/outline (0:00:06 elapsed time)
02:18:21Timing Isabelle_Meta_Model (8 threads, 130.638s elapsed time, 236.773s cpu time, 7.123s GC time, factor 1.81)
02:18:21Finished Isabelle_Meta_Model (0:02:13 elapsed time, 0:04:03 cpu time, factor 1.82)
02:18:21Building Group-Ring-Module (on hpcisabelle/7) ...
02:18:47Group-Ring-Module: theory Group-Ring-Module.Algebra1
02:18:52Group-Ring-Module: theory Group-Ring-Module.Algebra2
02:18:56Group-Ring-Module: theory Group-Ring-Module.Algebra3
02:19:01Group-Ring-Module: theory Group-Ring-Module.Algebra4
02:19:08Group-Ring-Module: theory Group-Ring-Module.Algebra5
02:19:13Group-Ring-Module: theory Group-Ring-Module.Algebra6
02:19:18Group-Ring-Module: theory Group-Ring-Module.Algebra7
02:19:24Group-Ring-Module: theory Group-Ring-Module.Algebra8
02:19:26Group-Ring-Module: theory Group-Ring-Module.Algebra9
02:20:36Preparing Group-Ring-Module/document ...
02:21:14Finished Group-Ring-Module/document (0:00:38 elapsed time)
02:21:14Preparing Group-Ring-Module/outline ...
02:21:27Finished Group-Ring-Module/outline (0:00:13 elapsed time)
02:21:27Timing Group-Ring-Module (8 threads, 112.282s elapsed time, 618.683s cpu time, 22.169s GC time, factor 5.51)
02:21:27Finished Group-Ring-Module (0:02:09 elapsed time, 0:10:54 cpu time, factor 5.05)
02:21:27Running Types_To_Sets_Extension (on hpcisabelle/0) ...
02:21:29Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Tools
02:21:29Types_To_Sets_Extension: theory HOL-Eisbach.Eisbach
02:21:29Types_To_Sets_Extension: theory HOL-Types_To_Sets.Types_To_Sets
02:21:30Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS
02:21:32Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Auxiliary
02:21:32Types_To_Sets_Extension: theory Types_To_Sets_Extension.Manual_Prerequisites
02:21:32Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Tests
02:21:34Types_To_Sets_Extension: theory HOL-Library.FuncSet
02:21:34Types_To_Sets_Extension: theory HOL-Library.Product_Plus
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Auxiliary
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.Introduction
02:21:34Types_To_Sets_Extension: theory HOL-Library.Infinite_Set
02:21:34Types_To_Sets_Extension: theory HOL-Library.Nat_Bijection
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Prerequisites
02:21:34Types_To_Sets_Extension: theory HOL-Library.Old_Datatype
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Introduction
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Introduction
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Introduction
02:21:34Types_To_Sets_Extension: theory HOL-Analysis.Product_Vector
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Definite_Description
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Groups
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Theory
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Syntax
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.Type_Simple_Orders
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Examples
02:21:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Lifting_Set_Ext
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Set_Ext
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.Lifting_Set_Ext
02:21:35Types_To_Sets_Extension: theory HOL-Library.Disjoint_Sets
02:21:35Types_To_Sets_Extension: theory HOL-Library.Countable
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.Product_Type_Ext
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Modules
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Relations
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semigroups
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Ext
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.Transfer_Ext
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_CR
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.Type_Semigroups
02:21:35Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Simple_Orders
02:21:36Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Semigroups
02:21:36Types_To_Sets_Extension: theory HOL-Library.Countable_Set
02:21:36Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Monoids
02:21:37Types_To_Sets_Extension: theory HOL-Library.Set_Idioms
02:21:38Types_To_Sets_Extension: theory HOL-Analysis.Elementary_Topology
02:21:38Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Groups
02:21:40Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semirings
02:21:41Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Simple_Orders
02:21:45Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Rings
02:21:52Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semilattices
02:21:52Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Topological_Space
02:21:57Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Lattices
02:21:57Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Linorders
02:22:00Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Vector_Spaces
02:22:01Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Conclusions
02:22:05Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Ordered_Topological_Spaces
02:22:05Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Product_Topology
02:22:05Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Topological_Space_Countability
02:22:05Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Complete_Lattices
02:22:34Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Conclusions
02:22:37Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Conclusions
02:22:42Preparing Types_To_Sets_Extension/document ...
02:23:25Finished Types_To_Sets_Extension/document (0:00:43 elapsed time)
02:23:25Preparing Types_To_Sets_Extension/outline ...
02:24:02Finished Types_To_Sets_Extension/outline (0:00:36 elapsed time)
02:24:02Timing Types_To_Sets_Extension (8 threads, 70.270s elapsed time, 356.790s cpu time, 7.993s GC time, factor 5.08)
02:24:02Finished Types_To_Sets_Extension (0:01:12 elapsed time, 0:06:02 cpu time, factor 4.98)
02:24:02Running Transport (on hpcisabelle/1) ...
02:24:03Transport: theory ML_Unification.ML_Attribute_Utils
02:24:03Transport: theory ML_Unification.ML_Code_Utils
02:24:03Transport: theory ML_Unification.ML_Conversion_Utils
02:24:03Transport: theory ML_Unification.ML_General_Utils
02:24:03Transport: theory ML_Unification.ML_Generic_Data_Utils
02:24:03Transport: theory ML_Unification.ML_Method_Utils
02:24:03Transport: theory SpecCheck.SpecCheck_Show
02:24:03Transport: theory ML_Unification.Setup_Result_Commands
02:24:03Transport: theory Transport.HOL_Syntax_Bundles_Functions
02:24:03Transport: theory Transport.HOL_Syntax_Bundles_Lattices
02:24:03Transport: theory Transport.HOL_Syntax_Bundles_Relations
02:24:03Transport: theory Transport.Predicates_Lattice
02:24:03Transport: theory HOL-Library.FuncSet
02:24:03Transport: theory ML_Unification.ML_Normalisations
02:24:03Transport: theory HOL-Library.IArray
02:24:03Transport: theory HOL-Library.Nat_Bijection
02:24:03Transport: theory HOL-Library.Old_Datatype
02:24:03Transport: theory HOL-Library.Preorder
02:24:03Transport: theory ML_Unification.ML_Attributes
02:24:03Transport: theory Transport.HOL_Syntax_Bundles_Groups
02:24:03Transport: theory ML_Unification.ML_Term_Index
02:24:03Transport: theory ML_Unification.ML_Binders
02:24:03Transport: theory ML_Unification.ML_Term_Utils
02:24:03Transport: theory Transport.HOL_Syntax_Bundles_Orders
02:24:04Transport: theory ML_Unification.ML_Logger
02:24:04Transport: theory ML_Unification.ML_Parsing_Utils
02:24:04Transport: theory Transport.Predicates_Order
02:24:04Transport: theory Transport.Adhoc_Overloading
02:24:04Transport: theory Transport.HOL_Basics_Base
02:24:04Transport: theory ML_Unification.ML_Theorem_Utils
02:24:04Transport: theory Transport.Functions_Restrict
02:24:04Transport: theory ML_Unification.ML_Unification_Base
02:24:04Transport: theory Transport.HOL_Syntax_Bundles_Base
02:24:04Transport: theory Transport.HOL_Syntax_Bundles
02:24:04Transport: theory ML_Unification.ML_Tactic_Utils
02:24:05Transport: theory ML_Unification.ML_Unifiers_Base
02:24:05Transport: theory ML_Unification.ML_Functor_Instances
02:24:05Transport: theory ML_Unification.ML_Priorities
02:24:05Transport: theory ML_Unification.ML_Unification_Parsers
02:24:05Transport: theory ML_Unification.Simps_To
02:24:05Transport: theory ML_Unification.Unify_Assumption_Tactic_Base
02:24:05Transport: theory HOL-Library.Countable
02:24:05Transport: theory HOL-Algebra.Congruence
02:24:06Transport: theory ML_Unification.ML_Unification_Hints_Base
02:24:06Transport: theory ML_Unification.ML_Unifiers
02:24:06Transport: theory ML_Unification.Unify_Resolve_Tactics_Base
02:24:07Transport: theory HOL-Algebra.Order
02:24:07Transport: theory ML_Unification.Unify_Resolve_Tactics
02:24:08Transport: theory ML_Unification.ML_Unification_Hints
02:24:08Transport: theory HOL-Library.FSet
02:24:08Transport: theory ML_Unification.ML_Unification_HOL_Setup
02:24:08Transport: theory Transport.Binary_Relations_Irreflexive
02:24:08Transport: theory Transport.HOL_Mem_Of
02:24:08Transport: theory Transport.Bounded_Quantifiers
02:24:08Transport: theory HOL-Algebra.Lattice
02:24:08Transport: theory Transport.Binary_Relation_Functions
02:24:08Transport: theory Transport.Bounded_Definite_Description
02:24:09Transport: theory Transport.Binary_Relations_Antisymmetric
02:24:09Transport: theory Transport.Binary_Relations_Connected
02:24:09Transport: theory Transport.Binary_Relations_Order_Base
02:24:09Transport: theory Transport.Binary_Relations_Lattice
02:24:09Transport: theory Transport.Functions_Base
02:24:09Transport: theory Transport.Reverse_Implies
02:24:09Transport: theory Transport.Function_Relators
02:24:09Transport: theory Transport.Functions_Surjective
02:24:09Transport: theory Transport.Predicate_Functions
02:24:09Transport: theory Transport.Functions_Injective
02:24:09Transport: theory Transport.Predicates
02:24:09Transport: theory HOL-Algebra.Complete_Lattice
02:24:09Transport: theory Transport.HOL_Alignment_Predicates
02:24:10Transport: theory Transport.Functions_Monotone
02:24:10Transport: theory Transport.Binary_Relations_Agree
02:24:10Transport: theory Transport.Binary_Relations_Left_Total
02:24:10Transport: theory Transport.Binary_Relations_Reflexive
02:24:11Transport: theory Transport.Dependent_Binary_Relations
02:24:11Transport: theory HOL-Algebra.Galois_Connection
02:24:11Transport: theory Transport.Binary_Relations_Symmetric
02:24:11Transport: theory Transport.Binary_Relations_Surjective
02:24:11Transport: theory Transport.Binary_Relations_Transitive
02:24:11Transport: theory Transport.Binary_Relations_Injective
02:24:11Transport: theory Transport.Binary_Relations_Bi_Total
02:24:11Transport: theory Transport.Binary_Relations_Extend
02:24:11Transport: theory Transport.Binary_Relations_Order
02:24:11Transport: theory Transport.Preorders
02:24:11Transport: theory Transport.Binary_Relations_Right_Unique
02:24:11Transport: theory Transport.Partial_Equivalence_Relations
02:24:11Transport: theory Transport.Partial_Orders
02:24:11Transport: theory Transport.Order_Functions_Base
02:24:11Transport: theory Transport.Linear_Orders
02:24:11Transport: theory Transport.Equivalence_Relations
02:24:11Transport: theory Transport.Binary_Relations_Bi_Unique
02:24:11Transport: theory Transport.Binary_Relations_Function_Evaluation
02:24:11Transport: theory Transport.Restricted_Equality
02:24:11Transport: theory Transport.Binary_Relation_Properties
02:24:11Transport: theory Transport.Binary_Relations_Function_Base
02:24:11Transport: theory Transport.Functions_Inverse
02:24:12Transport: theory Transport.Functions_Bijection
02:24:12Transport: theory Transport.Closure_Operators
02:24:12Transport: theory Transport.Order_Functors_Base
02:24:12Transport: theory Transport.Binary_Relations_Clean_Functions
02:24:12Transport: theory Transport.Function_Properties
02:24:12Transport: theory Transport.LFunctions
02:24:12Transport: theory Transport.Order_Functions
02:24:12Transport: theory Transport.Galois_Base
02:24:12Transport: theory Transport.Order_Equivalences
02:24:12Transport: theory Transport.Galois_Relator_Base
02:24:12Transport: theory Transport.Binary_Relations_Function_Composition
02:24:12Transport: theory Transport.Binary_Relations_Function_Extend
02:24:12Transport: theory Transport.Binary_Relations_Function_Lambda
02:24:12Transport: theory Transport.Half_Galois_Property
02:24:12Transport: theory Transport.Order_Functors
02:24:12Transport: theory Transport.Orders
02:24:12Transport: theory Transport.Binary_Relations_Functions
02:24:12Transport: theory Transport.LBinary_Relations
02:24:12Transport: theory Transport.HOL_Alignment_Binary_Relations
02:24:12Transport: theory Transport.Galois_Property
02:24:13Transport: theory Transport.Galois_Connections
02:24:13Transport: theory Transport.Galois_Relator
02:24:13Transport: theory Transport.Galois_Equivalences
02:24:13Transport: theory Transport.Galois
02:24:13Transport: theory Transport.Reflexive_Relator
02:24:13Transport: theory Transport.Transport_Base
02:24:13Transport: theory Transport.HOL_Basics
02:24:13Transport: theory Transport.HOL_Alignment_Orders
02:24:13Transport: theory Transport.HOL_Alignment_Functions
02:24:14Transport: theory Transport.Monotone_Function_Relator
02:24:14Transport: theory Transport.Transport_Bijections
02:24:14Transport: theory Transport.Transport_Compositions_Agree_Base
02:24:14Transport: theory Transport.Transport_Compositions_Generic_Base
02:24:14Transport: theory Transport.Transport_Functions_Base
02:24:14Transport: theory Transport.HOL_Algebra_Alignment_Orders
02:24:15Transport: theory Transport.HOL_Algebra_Alignment_Galois
02:24:15Transport: theory Transport.Transport_Identity
02:24:16Transport: theory Transport.Transport_Typedef_Base
02:24:16Transport: theory Transport.HOL_Alignments
02:24:16Transport: theory Transport.Transport_Natural_Functors_Base
02:24:16Transport: theory Transport.HOL_Algebra_Alignments
02:24:16Transport: theory Transport.Transport_Compositions_Agree_Galois_Property
02:24:16Transport: theory Transport.Transport_Compositions_Agree_Galois_Relator
02:24:17Transport: theory Transport.Transport_Compositions_Agree_Monotone
02:24:18Transport: theory Transport.Transport_Compositions_Agree_Galois_Connection
02:24:18Transport: theory Transport.Transport_Compositions_Agree_Order_Equivalence
02:24:20Transport: theory Transport.Transport_Compositions_Agree_Galois_Equivalence
02:24:23Transport: theory Transport.Transport_Compositions_Agree
02:24:28Transport: theory Transport.Transport_Compositions_Generic_Galois_Property
02:24:28Transport: theory Transport.Transport_Compositions_Generic_Galois_Relator
02:24:28Transport: theory Transport.Transport_Compositions_Generic_Monotone
02:24:28Transport: theory Transport.Transport_Compositions_Generic_Order_Base
02:24:29Transport: theory Transport.Transport_Compositions_Generic_Order_Equivalence
02:24:31Transport: theory Transport.Transport_Compositions_Generic_Galois_Connection
02:24:33Transport: theory Transport.Transport_Compositions_Generic_Galois_Equivalence
02:24:36Transport: theory Transport.Transport_Compositions_Generic
02:24:36Transport: theory Transport.Transport_Functions_Monotone
02:24:36Transport: theory Transport.Transport_Functions_Order_Base
02:24:36Transport: theory Transport.Transport_Natural_Functors_Galois
02:24:37Transport: theory Transport.Transport_Natural_Functors_Galois_Relator
02:24:38Transport: theory Transport.Transport_Natural_Functors_Order_Base
02:24:38Transport: theory Transport.Transport_Natural_Functors_Order_Equivalence
02:24:39Transport: theory Transport.Transport_Compositions
02:24:47Transport: theory Transport.Transport_Functions_Galois_Property
02:24:53Transport: theory Transport.Transport_Natural_Functors
02:25:01Transport: theory Transport.Transport_Functions_Galois_Connection
02:25:09Transport: theory Transport.Transport_Functions_Galois_Equivalence
02:25:24Transport: theory Transport.Transport_Functions_Order_Equivalence
02:25:24Transport: theory Transport.Transport_Functions_Relation_Simplifications
02:25:27Transport: theory Transport.Transport_Functions_Galois_Relator
02:25:46Transport: theory Transport.Transport_Functions
02:26:02Transport: theory Transport.Transport
02:26:02Transport: theory Transport.Transport_Partial_Quotient_Types
02:26:02Transport: theory Transport.Transport_Rel_If
02:26:02Transport: theory Transport.Transport_Syntax
02:26:04Transport: theory Transport.Transport_Prototype
02:26:06Transport: theory Transport.Transport_Dep_Fun_Rel_Examples
02:26:06Transport: theory Transport.Transport_Typedef
02:26:06Transport: theory Transport.Transport_Lists_Sets_Examples
02:26:09Transport: theory Transport.Transport_Via_Partial_Galois_Connections_Equivalences_Paper
02:26:15Preparing Transport/document ...
02:26:41Finished Transport/document (0:00:25 elapsed time)
02:26:41Preparing Transport/outline ...
02:27:01Finished Transport/outline (0:00:20 elapsed time)
02:27:01Timing Transport (8 threads, 129.287s elapsed time, 633.257s cpu time, 15.060s GC time, factor 4.90)
02:27:01Finished Transport (0:02:11 elapsed time, 0:10:38 cpu time, factor 4.85)
02:27:01Running Modal_Logics_for_NTS (on hpcisabelle/2) ...
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Fun_More
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Union
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Relation_More
02:27:03Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FS_Set
02:27:03Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Wellfounded
02:27:03Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Residual
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Extension
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Wellfounded_More
02:27:03Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Relation
02:27:04Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Embedding
02:27:04Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Transition_System
02:27:04Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Transition_System
02:27:04Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Constructions
02:27:04Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Transition_System
02:27:05Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Order_Relation
02:27:05Modal_Logics_for_NTS: theory HOL-Cardinals.Ordinal_Arithmetic
02:27:06Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Arithmetic
02:27:07Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinals
02:27:07Modal_Logics_for_NTS: theory HOL-Cardinals.Bounded_Set
02:27:08Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Bounded_Set
02:27:08Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Formula
02:27:08Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Formula
02:27:13Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Validity
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Disjunction
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Logical_Equivalence
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Validity
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Formula
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity
02:27:14Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Expressive_Completeness
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Logical_Equivalence
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Validity
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Logical_Equivalence
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.L_Transform
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence
02:27:15Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity
02:27:16Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Expressive_Completeness
02:27:16Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.S_Transform
02:29:20Preparing Modal_Logics_for_NTS/document ...
02:29:32Finished Modal_Logics_for_NTS/document (0:00:12 elapsed time)
02:29:32Preparing Modal_Logics_for_NTS/outline ...
02:29:37Finished Modal_Logics_for_NTS/outline (0:00:05 elapsed time)
02:29:37Timing Modal_Logics_for_NTS (8 threads, 133.490s elapsed time, 562.511s cpu time, 36.923s GC time, factor 4.21)
02:29:37Finished Modal_Logics_for_NTS (0:02:16 elapsed time, 0:09:32 cpu time, factor 4.19)
02:29:38Running Prpu_Maxflow (on hpcisabelle/3) ...
02:29:41Prpu_Maxflow: theory Prpu_Maxflow.Generic_Push_Relabel
02:29:41Prpu_Maxflow: theory Prpu_Maxflow.Graph_Topological_Ordering
02:29:56Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel
02:29:56Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Inst
02:29:58Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Impl
02:29:58Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front
02:30:20Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front_Impl
02:30:20Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
02:31:34Prpu_Maxflow: theory Prpu_Maxflow.Generated_Code_Test
02:31:53Preparing Prpu_Maxflow/document ...
02:32:00Finished Prpu_Maxflow/document (0:00:07 elapsed time)
02:32:00Preparing Prpu_Maxflow/outline ...
02:32:05Finished Prpu_Maxflow/outline (0:00:05 elapsed time)
02:32:05Timing Prpu_Maxflow (8 threads, 130.706s elapsed time, 306.168s cpu time, 6.389s GC time, factor 2.34)
02:32:05Finished Prpu_Maxflow (0:02:14 elapsed time, 0:05:11 cpu time, factor 2.32)
02:32:05Running Progress_Tracking (on hpcisabelle/4) ...
02:32:07Progress_Tracking: theory HOL-Library.Stream
02:32:07Progress_Tracking: theory HOL-Library.While_Combinator
02:32:09Progress_Tracking: theory HOL-Library.Linear_Temporal_Logic_on_Streams
02:32:11Progress_Tracking: theory Progress_Tracking.Auxiliary
02:32:12Progress_Tracking: theory Progress_Tracking.Antichain
02:32:12Progress_Tracking: theory Progress_Tracking.Exchange
02:32:12Progress_Tracking: theory Progress_Tracking.Exchange_Abadi
02:32:13Progress_Tracking: theory Progress_Tracking.Graph
02:32:14Progress_Tracking: theory Progress_Tracking.Propagate
02:32:19Progress_Tracking: theory Progress_Tracking.Combined
02:34:18Preparing Progress_Tracking/document ...
02:34:31Finished Progress_Tracking/document (0:00:13 elapsed time)
02:34:31Preparing Progress_Tracking/outline ...
02:34:38Finished Progress_Tracking/outline (0:00:06 elapsed time)
02:34:38Timing Progress_Tracking (8 threads, 129.401s elapsed time, 534.574s cpu time, 4.900s GC time, factor 4.13)
02:34:38Finished Progress_Tracking (0:02:11 elapsed time, 0:08:57 cpu time, factor 4.09)
02:34:38Running PseudoHoops (on hpcisabelle/5) ...
02:34:40PseudoHoops: theory LatticeProperties.Lattice_Prop
02:34:40PseudoHoops: theory PseudoHoops.Operations
02:34:40PseudoHoops: theory PseudoHoops.PseudoWaisbergAlgebra
02:34:40PseudoHoops: theory LatticeProperties.Modular_Distrib_Lattice
02:34:40PseudoHoops: theory PseudoHoops.LeftComplementedMonoid
02:34:43PseudoHoops: theory LatticeProperties.Lattice_Ordered_Group
02:34:44PseudoHoops: theory PseudoHoops.RightComplementedMonoid
02:34:49PseudoHoops: theory PseudoHoops.PseudoHoops
02:35:15PseudoHoops: theory PseudoHoops.PseudoHoopFilters
02:35:32PseudoHoops: theory PseudoHoops.SpecialPseudoHoops
02:36:28PseudoHoops: theory PseudoHoops.Examples
02:36:52Preparing PseudoHoops/document ...
02:36:58Finished PseudoHoops/document (0:00:06 elapsed time)
02:36:58Preparing PseudoHoops/outline ...
02:37:02Finished PseudoHoops/outline (0:00:03 elapsed time)
02:37:02Timing PseudoHoops (8 threads, 130.876s elapsed time, 193.793s cpu time, 4.539s GC time, factor 1.48)
02:37:02Finished PseudoHoops (0:02:12 elapsed time, 0:03:16 cpu time, factor 1.48)
02:37:02Running Resolution_FOL (on hpcisabelle/6) ...
02:37:05Resolution_FOL: theory Fresh_Identifiers.Fresh
02:37:05Resolution_FOL: theory HOL-Library.Adhoc_Overloading
02:37:05Resolution_FOL: theory HOL-Library.Cancellation
02:37:05Resolution_FOL: theory HOL-Library.Infinite_Set
02:37:05Resolution_FOL: theory HOL-Library.Nat_Bijection
02:37:05Resolution_FOL: theory HOL-Library.Old_Datatype
02:37:05Resolution_FOL: theory Regular-Sets.Regular_Set
02:37:05Resolution_FOL: theory HOL-Library.While_Combinator
02:37:06Resolution_FOL: theory HOL-Library.Monad_Syntax
02:37:06Resolution_FOL: theory First_Order_Terms.Option_Monad
02:37:06Resolution_FOL: theory First_Order_Terms.Renaming2
02:37:06Resolution_FOL: theory Abstract-Rewriting.Seq
02:37:06Resolution_FOL: theory Resolution_FOL.Tree
02:37:06Resolution_FOL: theory HOL-Library.Countable
02:37:06Resolution_FOL: theory HOL-Library.Multiset
02:37:08Resolution_FOL: theory HOL-Library.Countable_Set
02:37:08Resolution_FOL: theory Resolution_FOL.TermsAndLiterals
02:37:10Resolution_FOL: theory Regular-Sets.Regular_Exp
02:37:11Resolution_FOL: theory Resolution_FOL.Resolution
02:37:13Resolution_FOL: theory First_Order_Terms.Term
02:37:13Resolution_FOL: theory Regular-Sets.NDerivative
02:37:13Resolution_FOL: theory Regular-Sets.Relation_Interpretation
02:37:14Resolution_FOL: theory Resolution_FOL.Completeness
02:37:14Resolution_FOL: theory Resolution_FOL.Examples
02:37:16Resolution_FOL: theory First_Order_Terms.Unifiers
02:37:16Resolution_FOL: theory First_Order_Terms.Term_Pair_Multiset
02:37:18Resolution_FOL: theory Regular-Sets.Equivalence_Checking
02:37:18Resolution_FOL: theory Regular-Sets.Regexp_Method
02:37:19Resolution_FOL: theory Abstract-Rewriting.Abstract_Rewriting
02:37:22Resolution_FOL: theory First_Order_Terms.Abstract_Unification
02:37:22Resolution_FOL: theory First_Order_Terms.Unification
02:37:24Resolution_FOL: theory Resolution_FOL.Unification_Theorem
02:37:25Resolution_FOL: theory Resolution_FOL.Completeness_Instance
02:39:06Preparing Resolution_FOL/document ...
02:39:12Finished Resolution_FOL/document (0:00:05 elapsed time)
02:39:12Preparing Resolution_FOL/outline ...
02:39:16Finished Resolution_FOL/outline (0:00:03 elapsed time)
02:39:16Timing Resolution_FOL (8 threads, 120.985s elapsed time, 280.993s cpu time, 6.253s GC time, factor 2.32)
02:39:16Finished Resolution_FOL (0:02:03 elapsed time, 0:04:45 cpu time, factor 2.32)
02:39:16Building Extended_Finite_State_Machines (on hpcisabelle/7) ...
02:39:18Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.VName
02:39:18Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Trilean
02:39:18Extended_Finite_State_Machines: theory FinFun.FinFun
02:39:18Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.FSet_Utils
02:39:19Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Value
02:39:21Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Value_Lexorder
02:39:21Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.AExp
02:39:27Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.AExp_Lexorder
02:39:27Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.GExp
02:39:33Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Transition
02:39:33Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.GExp_Lexorder
02:39:34Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.EFSM
02:39:35Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Transition_Lexorder
02:39:37Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Drinks_Machine
02:39:38Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Drinks_Machine_2
02:39:38Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.EFSM_LTL
02:39:40Extended_Finite_State_Machines: theory Extended_Finite_State_Machines.Drinks_Machine_LTL
02:39:58Preparing Extended_Finite_State_Machines/document ...
02:40:04Finished Extended_Finite_State_Machines/document (0:00:06 elapsed time)
02:40:04Preparing Extended_Finite_State_Machines/outline ...
02:40:09Finished Extended_Finite_State_Machines/outline (0:00:05 elapsed time)
02:40:09Timing Extended_Finite_State_Machines (8 threads, 25.978s elapsed time, 150.526s cpu time, 3.616s GC time, factor 5.79)
02:40:10Finished Extended_Finite_State_Machines (0:00:41 elapsed time, 0:02:59 cpu time, factor 4.37)
02:40:10Building Parity_Game (on hpcisabelle/0) ...
02:40:11Parity_Game: theory Graph_Theory.Rtrancl_On
02:40:11Parity_Game: theory HOL-Combinatorics.Transposition
02:40:11Parity_Game: theory HOL-Library.Case_Converter
02:40:11Parity_Game: theory HOL-Library.Cancellation
02:40:11Parity_Game: theory HOL-Library.Complete_Partial_Order2
02:40:11Parity_Game: theory HOL-Library.FuncSet
02:40:11Parity_Game: theory HOL-Library.Infinite_Set
02:40:11Parity_Game: theory HOL-Library.Nat_Bijection
02:40:12Parity_Game: theory HOL-Library.Old_Datatype
02:40:12Parity_Game: theory HOL-Library.Sublist
02:40:12Parity_Game: theory HOL-Library.Simps_Case_Conv
02:40:13Parity_Game: theory HOL-Library.Liminf_Limsup
02:40:13Parity_Game: theory HOL-Library.Disjoint_Sets
02:40:13Parity_Game: theory HOL-Library.Multiset
02:40:14Parity_Game: theory HOL-Library.Countable
02:40:16Parity_Game: theory HOL-Library.Countable_Set
02:40:16Parity_Game: theory HOL-Library.Countable_Complete_Lattices
02:40:19Parity_Game: theory HOL-Library.Order_Continuity
02:40:19Parity_Game: theory HOL-Combinatorics.Permutations
02:40:20Parity_Game: theory HOL-Library.Extended_Nat
02:40:22Parity_Game: theory Coinductive.Coinductive_Nat
02:40:22Parity_Game: theory HOL-Library.Extended_Real
02:40:22Parity_Game: theory Coinductive.Coinductive_List
02:40:26Parity_Game: theory Graph_Theory.Stuff
02:40:27Parity_Game: theory Graph_Theory.Digraph
02:40:28Parity_Game: theory Graph_Theory.Arc_Walk
02:40:28Parity_Game: theory Graph_Theory.Bidirected_Digraph
02:40:30Parity_Game: theory Graph_Theory.Pair_Digraph
02:40:31Parity_Game: theory Parity_Game.MoreCoinductiveList
02:40:31Parity_Game: theory Parity_Game.ParityGame
02:40:34Parity_Game: theory Parity_Game.Strategy
02:40:35Parity_Game: theory Parity_Game.AttractingStrategy
02:40:35Parity_Game: theory Parity_Game.WellOrderedStrategy
02:40:35Parity_Game: theory Parity_Game.WinningStrategy
02:40:35Parity_Game: theory Parity_Game.WinningRegion
02:40:36Parity_Game: theory Parity_Game.Attractor
02:40:36Parity_Game: theory Parity_Game.UniformStrategy
02:40:36Parity_Game: theory Parity_Game.AttractorInductive
02:40:36Parity_Game: theory Parity_Game.AttractorStrategy
02:40:37Parity_Game: theory Parity_Game.PositionalDeterminacy
02:40:37Parity_Game: theory Graph_Theory.Digraph_Component
02:40:41Parity_Game: theory Graph_Theory.Digraph_Isomorphism
02:40:44Parity_Game: theory Parity_Game.Graph_TheoryCompatibility
02:41:12Preparing Parity_Game/document ...
02:41:19Finished Parity_Game/document (0:00:07 elapsed time)
02:41:19Preparing Parity_Game/outline ...
02:41:25Finished Parity_Game/outline (0:00:05 elapsed time)
02:41:25Timing Parity_Game (8 threads, 44.960s elapsed time, 322.215s cpu time, 9.783s GC time, factor 7.17)
02:41:25Finished Parity_Game (0:00:59 elapsed time, 0:05:54 cpu time, factor 5.91)
02:41:25Building LTL (on hpcisabelle/1) ...
02:41:27LTL: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
02:41:27LTL: theory LTL.LTL
02:41:32LTL: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
02:41:43LTL: theory LTL.Equivalence_Relations
02:41:43LTL: theory LTL.Rewriting
02:41:46LTL: theory LTL.Code_Equations
02:41:46LTL: theory LTL.Disjunctive_Normal_Form
02:41:52LTL: theory LTL.Example
02:42:30Preparing LTL/document ...
02:42:36Finished LTL/document (0:00:05 elapsed time)
02:42:36Preparing LTL/outline ...
02:42:40Finished LTL/outline (0:00:04 elapsed time)
02:42:40Timing LTL (8 threads, 44.870s elapsed time, 186.018s cpu time, 5.056s GC time, factor 4.15)
02:42:40Finished LTL (0:01:04 elapsed time, 0:03:47 cpu time, factor 3.54)
02:42:40Running Proof_Strategy_Language (on hpcisabelle/2) ...
02:42:42Proof_Strategy_Language: theory Proof_Strategy_Language.Try_Hard
02:42:42Proof_Strategy_Language: theory HOL-Eisbach.Eisbach
02:42:44Proof_Strategy_Language: theory Proof_Strategy_Language.PSL
02:42:44Proof_Strategy_Language: theory Proof_Strategy_Language.Example
02:44:56Preparing Proof_Strategy_Language/document ...
02:44:58Finished Proof_Strategy_Language/document (0:00:02 elapsed time)
02:44:58Preparing Proof_Strategy_Language/outline ...
02:45:00Finished Proof_Strategy_Language/outline (0:00:02 elapsed time)
02:45:00Timing Proof_Strategy_Language (8 threads, 132.993s elapsed time, 217.359s cpu time, 7.169s GC time, factor 1.63)
02:45:00Finished Proof_Strategy_Language (0:02:15 elapsed time, 0:03:41 cpu time, factor 1.64)
02:45:01Running MFOTL_Checker (on hpcisabelle/3) ...
02:45:03MFOTL_Checker: theory MFOTL_Checker.Event_Data
02:45:03MFOTL_Checker: theory MFOTL_Checker.Partition
02:45:03MFOTL_Checker: theory MFOTL_Checker.Trace
02:45:03MFOTL_Checker: theory MFOTL_Checker.Prelim
02:45:05MFOTL_Checker: theory MFOTL_Checker.Formula
02:45:14MFOTL_Checker: theory MFOTL_Checker.Proof_Object
02:45:14MFOTL_Checker: theory MFOTL_Checker.Proof_System
02:45:38MFOTL_Checker: theory MFOTL_Checker.Checker
02:46:19MFOTL_Checker: theory MFOTL_Checker.Checker_Code
02:46:32MFOTL_Checker: theory MFOTL_Checker.Monitor
02:46:50MFOTL_Checker: theory MFOTL_Checker.Examples
02:47:13Preparing MFOTL_Checker/document ...
02:47:22Finished MFOTL_Checker/document (0:00:09 elapsed time)
02:47:22Preparing MFOTL_Checker/outline ...
02:47:28Finished MFOTL_Checker/outline (0:00:05 elapsed time)
02:47:28Timing MFOTL_Checker (8 threads, 127.474s elapsed time, 601.780s cpu time, 40.809s GC time, factor 4.72)
02:47:28Finished MFOTL_Checker (0:02:11 elapsed time, 0:10:12 cpu time, factor 4.66)
02:47:28Running Planarity_Certificates (on hpcisabelle/4) ...
02:47:30Planarity_Certificates: theory Planarity_Certificates.Lib
02:47:30Planarity_Certificates: theory Planarity_Certificates.WP
02:47:30Planarity_Certificates: theory Planarity_Certificates.NonDetMonad
02:47:30Planarity_Certificates: theory Planarity_Certificates.OptionMonad
02:47:31Planarity_Certificates: theory Planarity_Certificates.NonDetMonadLemmas
02:47:32Planarity_Certificates: theory Planarity_Certificates.OptionMonadND
02:47:32Planarity_Certificates: theory Planarity_Certificates.OptionMonadWP
02:47:34Planarity_Certificates: theory HOL-Eisbach.Eisbach
02:47:34Planarity_Certificates: theory Case_Labeling.Case_Labeling
02:47:34Planarity_Certificates: theory HOL-Combinatorics.Transposition
02:47:34Planarity_Certificates: theory Graph_Theory.Rtrancl_On
02:47:34Planarity_Certificates: theory HOL-Library.Case_Converter
02:47:34Planarity_Certificates: theory HOL-Library.FuncSet
02:47:34Planarity_Certificates: theory HOL-Library.Infinite_Set
02:47:34Planarity_Certificates: theory HOL-Library.Nat_Bijection
02:47:34Planarity_Certificates: theory HOL-Library.Old_Datatype
02:47:34Planarity_Certificates: theory HOL-Library.Rewrite
02:47:35Planarity_Certificates: theory HOL-Library.Simps_Case_Conv
02:47:35Planarity_Certificates: theory Planarity_Certificates.Simpl_Anno
02:47:35Planarity_Certificates: theory HOL-Library.Liminf_Limsup
02:47:35Planarity_Certificates: theory List-Index.List_Index
02:47:35Planarity_Certificates: theory Planarity_Certificates.AutoCorres_Misc
02:47:36Planarity_Certificates: theory Transitive-Closure.Transitive_Closure_Impl
02:47:36Planarity_Certificates: theory HOL-Library.Disjoint_Sets
02:47:37Planarity_Certificates: theory HOL-Library.Countable
02:47:37Planarity_Certificates: theory Planarity_Certificates.Setup_AutoCorres
02:47:37Planarity_Certificates: theory Planarity_Certificates.List_Aux
02:47:37Planarity_Certificates: theory HOL-Combinatorics.Permutations
02:47:38Planarity_Certificates: theory HOL-Library.Countable_Set
02:47:39Planarity_Certificates: theory HOL-Combinatorics.Orbits
02:47:39Planarity_Certificates: theory Graph_Theory.Auxiliary
02:47:39Planarity_Certificates: theory HOL-Library.Countable_Complete_Lattices
02:47:39Planarity_Certificates: theory Planarity_Certificates.Executable_Permutations
02:47:40Planarity_Certificates: theory Planarity_Certificates.Permutations_2
02:47:41Planarity_Certificates: theory HOL-Library.Order_Continuity
02:47:42Planarity_Certificates: theory HOL-Library.Extended_Nat
02:47:44Planarity_Certificates: theory HOL-Library.Extended_Real
02:47:48Planarity_Certificates: theory Graph_Theory.Stuff
02:47:49Planarity_Certificates: theory Graph_Theory.Digraph
02:47:51Planarity_Certificates: theory Graph_Theory.Arc_Walk
02:47:51Planarity_Certificates: theory Graph_Theory.Bidirected_Digraph
02:47:53Planarity_Certificates: theory Graph_Theory.Vertex_Walk
02:47:53Planarity_Certificates: theory Graph_Theory.Pair_Digraph
02:47:53Planarity_Certificates: theory Graph_Theory.Weighted_Graph
02:47:53Planarity_Certificates: theory Graph_Theory.Shortest_Path
02:48:00Planarity_Certificates: theory Graph_Theory.Digraph_Component
02:48:04Planarity_Certificates: theory Graph_Theory.Digraph_Component_Vwalk
02:48:04Planarity_Certificates: theory Graph_Theory.Digraph_Isomorphism
02:48:04Planarity_Certificates: theory Graph_Theory.Subdivision
02:48:06Planarity_Certificates: theory Graph_Theory.Kuratowski
02:48:06Planarity_Certificates: theory Graph_Theory.Euler
02:48:12Planarity_Certificates: theory Graph_Theory.Graph_Theory
02:48:13Planarity_Certificates: theory Planarity_Certificates.Check_Non_Planarity_Impl
02:48:13Planarity_Certificates: theory Planarity_Certificates.Graph_Genus
02:48:13Planarity_Certificates: theory Planarity_Certificates.Reachablen
02:48:16Planarity_Certificates: theory Planarity_Certificates.Planar_Subdivision
02:48:16Planarity_Certificates: theory Planarity_Certificates.Planar_Subgraph
02:48:16Planarity_Certificates: theory Planarity_Certificates.Check_Planarity_Verification
02:48:16Planarity_Certificates: theory Planarity_Certificates.Digraph_Map_Impl
02:48:19Planarity_Certificates: theory Planarity_Certificates.Planar_Complete
02:48:43Planarity_Certificates: theory Planarity_Certificates.Kuratowski_Combinatorial
02:48:43Planarity_Certificates: theory Planarity_Certificates.Check_Non_Planarity_Verification
02:48:46Planarity_Certificates: theory Planarity_Certificates.Planarity_Certificates
02:49:01Preparing Planarity_Certificates/document ...
02:49:12Finished Planarity_Certificates/document (0:00:11 elapsed time)
02:49:12Preparing Planarity_Certificates/outline ...
02:49:18Finished Planarity_Certificates/outline (0:00:05 elapsed time)
02:49:18Timing Planarity_Certificates (8 threads, 87.457s elapsed time, 468.793s cpu time, 15.260s GC time, factor 5.36)
02:49:18Finished Planarity_Certificates (0:01:30 elapsed time, 0:07:55 cpu time, factor 5.28)
02:49:18Building Symmetric_Polynomials (on hpcisabelle/5) ...
02:49:20Symmetric_Polynomials: theory Polynomials.MPoly_Type
02:49:20Symmetric_Polynomials: theory Abstract-Rewriting.Seq
02:49:20Symmetric_Polynomials: theory HOL-Combinatorics.Transposition
02:49:20Symmetric_Polynomials: theory Polynomials.More_Modules
02:49:20Symmetric_Polynomials: theory Open_Induction.Restricted_Predicates
02:49:20Symmetric_Polynomials: theory Regular-Sets.Regular_Set
02:49:20Symmetric_Polynomials: theory Symmetric_Polynomials.Vieta
02:49:20Symmetric_Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
02:49:20Symmetric_Polynomials: theory Well_Quasi_Orders.Least_Enum
02:49:21Symmetric_Polynomials: theory HOL-Combinatorics.Permutations
02:49:21Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Elements
02:49:21Symmetric_Polynomials: theory Polynomials.More_MPoly_Type
02:49:22Symmetric_Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
02:49:22Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials
02:49:24Symmetric_Polynomials: theory Regular-Sets.Regular_Exp
02:49:28Symmetric_Polynomials: theory Regular-Sets.NDerivative
02:49:28Symmetric_Polynomials: theory Regular-Sets.Relation_Interpretation
02:49:33Symmetric_Polynomials: theory Regular-Sets.Equivalence_Checking
02:49:33Symmetric_Polynomials: theory Regular-Sets.Regexp_Method
02:49:34Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full
02:49:36Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
02:49:37Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
02:49:37Symmetric_Polynomials: theory Polynomials.Utils
02:49:37Symmetric_Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
02:49:38Symmetric_Polynomials: theory Polynomials.Power_Products
02:49:53Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class
02:49:57Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
02:50:12Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_FMap
02:50:16Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials_Code
02:50:41Preparing Symmetric_Polynomials/document ...
02:50:47Finished Symmetric_Polynomials/document (0:00:05 elapsed time)
02:50:47Preparing Symmetric_Polynomials/outline ...
02:50:50Finished Symmetric_Polynomials/outline (0:00:03 elapsed time)
02:50:50Timing Symmetric_Polynomials (8 threads, 63.608s elapsed time, 230.444s cpu time, 6.950s GC time, factor 3.62)
02:50:50Finished Symmetric_Polynomials (0:01:21 elapsed time, 0:04:27 cpu time, factor 3.26)
02:50:50Building Quantales (on hpcisabelle/6) ...
02:50:53Quantales: theory Kleene_Algebra.Signatures
02:50:53Quantales: theory Kleene_Algebra.Dioid
02:51:11Quantales: theory Quantales.Dioid_Models_New
02:51:21Quantales: theory Quantales.Quantales
02:51:21Quantales: theory Kleene_Algebra.Conway
02:51:32Quantales: theory Kleene_Algebra.Kleene_Algebra
02:52:26Quantales: theory Quantales.Quantale_Models
02:52:26Quantales: theory Quantales.Quantale_Star
02:52:29Quantales: theory Quantales.Quantic_Nuclei_Conuclei
02:52:32Quantales: theory Quantales.Quantale_Left_Sided
02:52:47Quantales: theory Quantales.Quantale_Modules
02:53:05Preparing Quantales/document ...
02:53:09Finished Quantales/document (0:00:04 elapsed time)
02:53:09Preparing Quantales/outline ...
02:53:13Finished Quantales/outline (0:00:03 elapsed time)
02:53:13Timing Quantales (8 threads, 117.995s elapsed time, 214.937s cpu time, 5.113s GC time, factor 1.82)
02:53:13Finished Quantales (0:02:14 elapsed time, 0:04:08 cpu time, factor 1.85)
02:53:13Building Bernoulli (on hpcisabelle/7) ...
02:53:16Bernoulli: theory HOL-Computational_Algebra.Group_Closure
02:53:16Bernoulli: theory HOL-Combinatorics.Stirling
02:53:16Bernoulli: theory HOL-Computational_Algebra.Fraction_Field
02:53:16Bernoulli: theory HOL-Computational_Algebra.Nth_Powers
02:53:16Bernoulli: theory HOL-Computational_Algebra.Squarefree
02:53:16Bernoulli: theory HOL-Number_Theory.Cong
02:53:16Bernoulli: theory HOL-Algebra.Congruence
02:53:16Bernoulli: theory HOL-Library.Power_By_Squaring
02:53:16Bernoulli: theory HOL-Number_Theory.Eratosthenes
02:53:16Bernoulli: theory Bernoulli.Bernoulli
02:53:16Bernoulli: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
02:53:17Bernoulli: theory HOL-Number_Theory.Fib
02:53:17Bernoulli: theory HOL-Number_Theory.Prime_Powers
02:53:17Bernoulli: theory Bernoulli.Periodic_Bernpoly
02:53:17Bernoulli: theory HOL-Algebra.Order
02:53:18Bernoulli: theory HOL-Computational_Algebra.Normalized_Fraction
02:53:18Bernoulli: theory HOL-Number_Theory.Mod_Exp
02:53:18Bernoulli: theory HOL-Number_Theory.Totient
02:53:19Bernoulli: theory HOL-Computational_Algebra.Polynomial_Factorial
02:53:19Bernoulli: theory HOL-Algebra.Lattice
02:53:20Bernoulli: theory HOL-Algebra.Complete_Lattice
02:53:20Bernoulli: theory HOL-Computational_Algebra.Computational_Algebra
02:53:21Bernoulli: theory HOL-Algebra.Group
02:53:24Bernoulli: theory HOL-Algebra.Coset
02:53:24Bernoulli: theory HOL-Algebra.FiniteProduct
02:53:25Bernoulli: theory HOL-Algebra.Ring
02:53:27Bernoulli: theory HOL-Algebra.Generated_Groups
02:53:28Bernoulli: theory HOL-Algebra.Elementary_Groups
02:53:30Bernoulli: theory HOL-Algebra.AbelCoset
02:53:30Bernoulli: theory HOL-Algebra.Module
02:53:35Bernoulli: theory HOL-Algebra.Ideal
02:53:38Bernoulli: theory HOL-Algebra.RingHom
02:53:40Bernoulli: theory HOL-Algebra.UnivPoly
02:53:55Bernoulli: theory HOL-Algebra.Multiplicative_Group
02:53:59Bernoulli: theory HOL-Number_Theory.Residues
02:54:02Bernoulli: theory HOL-Number_Theory.Euler_Criterion
02:54:02Bernoulli: theory HOL-Number_Theory.Pocklington
02:54:02Bernoulli: theory HOL-Number_Theory.Gauss
02:54:03Bernoulli: theory HOL-Number_Theory.Quadratic_Reciprocity
02:54:03Bernoulli: theory HOL-Number_Theory.Residue_Primitive_Roots
02:54:03Bernoulli: theory HOL-Number_Theory.Number_Theory
02:54:05Bernoulli: theory Bernoulli.Bernoulli_FPS
02:54:09Bernoulli: theory Bernoulli.Bernoulli_Zeta
02:54:45Preparing Bernoulli/document ...
02:54:50Finished Bernoulli/document (0:00:04 elapsed time)
02:54:50Preparing Bernoulli/outline ...
02:54:53Finished Bernoulli/outline (0:00:03 elapsed time)
02:54:54Timing Bernoulli (8 threads, 67.683s elapsed time, 439.141s cpu time, 13.032s GC time, factor 6.49)
02:54:54Finished Bernoulli (0:01:30 elapsed time, 0:08:04 cpu time, factor 5.36)
02:54:54Running BirdKMP (on hpcisabelle/0) ...
02:54:55BirdKMP: theory BirdKMP.HOLCF_ROOT
02:54:56BirdKMP: theory BirdKMP.Theory_Of_Lists
02:55:00BirdKMP: theory BirdKMP.KMP
02:57:03Preparing BirdKMP/document ...
02:57:13Finished BirdKMP/document (0:00:09 elapsed time)
02:57:13Preparing BirdKMP/outline ...
02:57:21Finished BirdKMP/outline (0:00:08 elapsed time)
02:57:21Timing BirdKMP (8 threads, 125.827s elapsed time, 241.900s cpu time, 3.648s GC time, factor 1.92)
02:57:21Finished BirdKMP (0:02:08 elapsed time, 0:04:08 cpu time, factor 1.93)
02:57:21Running Transcendence_Series_Hancl_Rucki (on hpcisabelle/1) ...
02:57:24Transcendence_Series_Hancl_Rucki: theory Pure-ex.Guess
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fraction_Field
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Combinatorics.Stirling
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Nth_Powers
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Group_Closure
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Squarefree
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Cong
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Congruence
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Library.Power_By_Squaring
02:57:24Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Eratosthenes
02:57:24Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Field_as_Ring
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Library.Going_To_Filter
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach_Tools
02:57:25Transcendence_Series_Hancl_Rucki: theory Bernoulli.Periodic_Bernpoly
02:57:25Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Topology
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Fib
02:57:25Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Order
02:57:26Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Prime_Powers
02:57:26Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Analysis
02:57:26Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Normalized_Fraction
02:57:26Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Mod_Exp
02:57:26Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Totient
02:57:27Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_Factorial
02:57:27Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Lattice
02:57:28Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Complete_Lattice
02:57:28Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Computational_Algebra
02:57:28Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.PolyMisc
02:57:28Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.Sturm_Tarski
02:57:29Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Group
02:57:30Transcendence_Series_Hancl_Rucki: theory Budan_Fourier.BF_Misc
02:57:31Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Algebraic
02:57:32Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Coset
02:57:32Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.FiniteProduct
02:57:33Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Transcendental
02:57:33Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ring
02:57:33Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Cauchy_Index_Theorem
02:57:34Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Generated_Groups
02:57:36Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Elementary_Groups
02:57:37Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Winding_Number_Eval
02:57:38Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.AbelCoset
02:57:38Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Module
02:57:42Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ideal
02:57:46Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.RingHom
02:57:48Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.UnivPoly
02:58:04Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Multiplicative_Group
02:58:08Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residues
02:58:12Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Euler_Criterion
02:58:12Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Pocklington
02:58:12Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Gauss
02:58:13Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Quadratic_Reciprocity
02:58:13Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residue_Primitive_Roots
02:58:14Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Number_Theory
02:58:15Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_FPS
02:58:15Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Misc
02:58:15Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Multiplicative_Function
02:58:16Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Product
02:58:16Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Euler_Products
02:58:16Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series
02:58:19Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_Zeta
02:58:20Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin
02:58:21Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Moebius_Mu
02:58:22Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.More_Totient
02:58:22Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Liouville_Lambda
02:58:22Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count
02:58:22Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory
02:58:23Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation
02:58:24Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis
02:58:33Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Library
02:58:34Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function
02:58:39Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
02:58:41Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
02:59:30Preparing Transcendence_Series_Hancl_Rucki/document ...
02:59:34Finished Transcendence_Series_Hancl_Rucki/document (0:00:03 elapsed time)
02:59:34Preparing Transcendence_Series_Hancl_Rucki/outline ...
02:59:36Finished Transcendence_Series_Hancl_Rucki/outline (0:00:02 elapsed time)
02:59:36Timing Transcendence_Series_Hancl_Rucki (8 threads, 120.944s elapsed time, 802.086s cpu time, 22.868s GC time, factor 6.63)
02:59:36Finished Transcendence_Series_Hancl_Rucki (0:02:04 elapsed time, 0:13:31 cpu time, factor 6.50)
02:59:36Running Poincare_Bendixson (on hpcisabelle/2) ...
02:59:40Poincare_Bendixson: theory Poincare_Bendixson.Analysis_Misc
02:59:40Poincare_Bendixson: theory Poincare_Bendixson.Affine_Arithmetic_Misc
02:59:41Poincare_Bendixson: theory Poincare_Bendixson.ODE_Misc
02:59:47Poincare_Bendixson: theory Poincare_Bendixson.Invariance
02:59:50Poincare_Bendixson: theory Poincare_Bendixson.Limit_Set
02:59:52Poincare_Bendixson: theory Poincare_Bendixson.Periodic_Orbit
02:59:54Poincare_Bendixson: theory Poincare_Bendixson.Poincare_Bendixson
03:00:00Poincare_Bendixson: theory Poincare_Bendixson.Examples
03:01:46Preparing Poincare_Bendixson/document ...
03:01:53Finished Poincare_Bendixson/document (0:00:06 elapsed time)
03:01:53Preparing Poincare_Bendixson/outline ...
03:01:56Finished Poincare_Bendixson/outline (0:00:03 elapsed time)
03:01:56Timing Poincare_Bendixson (8 threads, 124.682s elapsed time, 305.860s cpu time, 5.335s GC time, factor 2.45)
03:01:56Finished Poincare_Bendixson (0:02:09 elapsed time, 0:05:11 cpu time, factor 2.42)
03:01:56Running Gale_Shapley (on hpcisabelle/3) ...
03:01:58Gale_Shapley: theory HOL-Eisbach.Eisbach
03:01:58Gale_Shapley: theory Automatic_Refinement.Foldi
03:01:58Gale_Shapley: theory Automatic_Refinement.Prio_List
03:01:58Gale_Shapley: theory Automatic_Refinement.Refine_Util_Bootstrap1
03:01:58Gale_Shapley: theory HOL-Hoare.Hoare_Syntax
03:01:58Gale_Shapley: theory HOL-Hoare.Hoare_Tac
03:01:58Gale_Shapley: theory HOL-Library.Cancellation
03:01:58Gale_Shapley: theory HOL-Library.AList
03:01:58Gale_Shapley: theory Automatic_Refinement.Mk_Term_Antiquot
03:01:58Gale_Shapley: theory Automatic_Refinement.Mpat_Antiquot
03:01:58Gale_Shapley: theory HOL-Library.Code_Abstract_Nat
03:01:58Gale_Shapley: theory HOL-Library.Code_Target_Int
03:01:58Gale_Shapley: theory Automatic_Refinement.Refine_Util
03:01:58Gale_Shapley: theory HOL-Library.Code_Target_Nat
03:01:59Gale_Shapley: theory HOL-Library.Infinite_Set
03:01:59Gale_Shapley: theory HOL-Library.Code_Target_Numeral
03:01:59Gale_Shapley: theory HOL-Library.LaTeXsugar
03:01:59Gale_Shapley: theory HOL-Library.Multiset
03:01:59Gale_Shapley: theory Automatic_Refinement.Anti_Unification
03:01:59Gale_Shapley: theory Automatic_Refinement.Attr_Comb
03:02:00Gale_Shapley: theory Automatic_Refinement.Indep_Vars
03:02:00Gale_Shapley: theory Automatic_Refinement.Mk_Record_Simp
03:02:00Gale_Shapley: theory Automatic_Refinement.Tagged_Solver
03:02:00Gale_Shapley: theory Automatic_Refinement.Named_Sorted_Thms
03:02:00Gale_Shapley: theory Automatic_Refinement.Select_Solve
03:02:00Gale_Shapley: theory HOL-Library.Option_ord
03:02:00Gale_Shapley: theory HOL-Library.While_Combinator
03:02:00Gale_Shapley: theory List-Index.List_Index
03:02:02Gale_Shapley: theory HOL-Hoare.Hoare_Logic
03:02:03Gale_Shapley: theory Gale_Shapley.Gale_Shapley1
03:02:06Gale_Shapley: theory HOL-ex.Quicksort
03:02:06Gale_Shapley: theory Automatic_Refinement.Misc
03:02:13Gale_Shapley: theory Automatic_Refinement.Refine_Lib
03:02:14Gale_Shapley: theory Collections.SetIterator
03:02:15Gale_Shapley: theory Automatic_Refinement.Relators
03:02:16Gale_Shapley: theory Collections.SetIteratorOperations
03:02:16Gale_Shapley: theory Automatic_Refinement.Param_Tool
03:02:17Gale_Shapley: theory Automatic_Refinement.Param_HOL
03:02:18Gale_Shapley: theory Automatic_Refinement.Parametricity
03:02:19Gale_Shapley: theory Collections.Assoc_List
03:02:19Gale_Shapley: theory Collections.Diff_Array
03:02:31Gale_Shapley: theory Gale_Shapley.Gale_Shapley2
03:02:52Preparing Gale_Shapley/document ...
03:02:57Finished Gale_Shapley/document (0:00:05 elapsed time)
03:02:57Preparing Gale_Shapley/outline ...
03:03:01Finished Gale_Shapley/outline (0:00:03 elapsed time)
03:03:01Timing Gale_Shapley (8 threads, 52.288s elapsed time, 347.669s cpu time, 6.800s GC time, factor 6.65)
03:03:01Finished Gale_Shapley (0:00:54 elapsed time, 0:05:53 cpu time, factor 6.47)
03:03:01Running Interpreter_Optimizations (on hpcisabelle/4) ...
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Env
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.List_util
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Dynamic
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Map_Extra
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Op
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Option_Extra
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.Result
03:03:03Interpreter_Optimizations: theory VeriComp.Behaviour
03:03:03Interpreter_Optimizations: theory Interpreter_Optimizations.OpInl
03:03:03Interpreter_Optimizations: theory VeriComp.Transfer_Extras
03:03:03Interpreter_Optimizations: theory VeriComp.Well_founded
03:03:03Interpreter_Optimizations: theory VeriComp.Inf
03:03:04Interpreter_Optimizations: theory VeriComp.Lifting_Simulation_To_Bisimulation
03:03:04Interpreter_Optimizations: theory Interpreter_Optimizations.AList_Extra
03:03:04Interpreter_Optimizations: theory Interpreter_Optimizations.Env_list
03:03:04Interpreter_Optimizations: theory VeriComp.Semantics
03:03:05Interpreter_Optimizations: theory VeriComp.Language
03:03:05Interpreter_Optimizations: theory VeriComp.Simulation
03:03:05Interpreter_Optimizations: theory Interpreter_Optimizations.Global
03:03:06Interpreter_Optimizations: theory VeriComp.Compiler
03:03:15Interpreter_Optimizations: theory Interpreter_Optimizations.Unboxed
03:03:15Interpreter_Optimizations: theory Interpreter_Optimizations.Inca
03:03:15Interpreter_Optimizations: theory Interpreter_Optimizations.Std
03:03:19Interpreter_Optimizations: theory Interpreter_Optimizations.OpUbx
03:03:19Interpreter_Optimizations: theory Interpreter_Optimizations.Unboxed_lemmas
03:03:22Interpreter_Optimizations: theory Interpreter_Optimizations.Ubx
03:03:22Interpreter_Optimizations: theory Interpreter_Optimizations.Op_example
03:03:23Interpreter_Optimizations: theory Interpreter_Optimizations.Inca_Verification
03:03:23Interpreter_Optimizations: theory Interpreter_Optimizations.Std_to_Inca_simulation
03:03:26Interpreter_Optimizations: theory Interpreter_Optimizations.Std_to_Inca_compiler
03:03:45Interpreter_Optimizations: theory Interpreter_Optimizations.Ubx_Verification
03:03:51Interpreter_Optimizations: theory Interpreter_Optimizations.Inca_to_Ubx_simulation
03:04:00Interpreter_Optimizations: theory Interpreter_Optimizations.Inca_to_Ubx_compiler
03:05:08Preparing Interpreter_Optimizations/document ...
03:05:17Finished Interpreter_Optimizations/document (0:00:08 elapsed time)
03:05:17Preparing Interpreter_Optimizations/outline ...
03:05:22Finished Interpreter_Optimizations/outline (0:00:05 elapsed time)
03:05:22Timing Interpreter_Optimizations (8 threads, 122.975s elapsed time, 492.898s cpu time, 14.475s GC time, factor 4.01)
03:05:22Finished Interpreter_Optimizations (0:02:06 elapsed time, 0:08:22 cpu time, factor 3.98)
03:05:22Running Wieferich_Kempner (on hpcisabelle/5) ...
03:05:25Wieferich_Kempner: theory Wieferich_Kempner.Wieferich_Kempner
03:07:18Preparing Wieferich_Kempner/document ...
03:07:22Finished Wieferich_Kempner/document (0:00:03 elapsed time)
03:07:22Preparing Wieferich_Kempner/outline ...
03:07:24Finished Wieferich_Kempner/outline (0:00:02 elapsed time)
03:07:24Timing Wieferich_Kempner (8 threads, 111.970s elapsed time, 603.168s cpu time, 3.684s GC time, factor 5.39)
03:07:24Finished Wieferich_Kempner (0:01:55 elapsed time, 0:10:08 cpu time, factor 5.26)
03:07:24Building Datatypes (on hpcisabelle/6) ...
03:07:26Datatypes: theory Datatypes.Setup
03:07:26Datatypes: theory HOL-Library.BNF_Axiomatization
03:07:26Datatypes: theory HOL-Library.Case_Converter
03:07:26Datatypes: theory HOL-Library.Old_Datatype
03:07:26Datatypes: theory HOL-Library.Nat_Bijection
03:07:27Datatypes: theory HOL-Library.Simps_Case_Conv
03:07:27Datatypes: theory HOL-Library.Countable
03:07:29Datatypes: theory HOL-Library.FSet
03:07:33Datatypes: theory Datatypes.Datatypes
03:08:34Preparing Datatypes/datatypes ...
03:08:39Finished Datatypes/datatypes (0:00:05 elapsed time)
03:08:39Timing Datatypes (8 threads, 50.847s elapsed time, 108.238s cpu time, 4.195s GC time, factor 2.13)
03:08:39Finished Datatypes (0:01:08 elapsed time, 0:02:27 cpu time, factor 2.15)
03:08:39Running Interval_Arithmetic_Word32 (on hpcisabelle/7) ...
03:08:41Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Interval_Word32
03:08:41Interval_Arithmetic_Word32: theory HOL-Library.Code_Target_Int
03:08:41Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Finite_String
03:08:52Interval_Arithmetic_Word32: theory Interval_Arithmetic_Word32.Interpreter
03:10:18Preparing Interval_Arithmetic_Word32/document ...
03:10:25Finished Interval_Arithmetic_Word32/document (0:00:07 elapsed time)
03:10:25Preparing Interval_Arithmetic_Word32/outline ...
03:10:29Finished Interval_Arithmetic_Word32/outline (0:00:03 elapsed time)
03:10:29Timing Interval_Arithmetic_Word32 (8 threads, 96.064s elapsed time, 555.684s cpu time, 14.598s GC time, factor 5.78)
03:10:29Finished Interval_Arithmetic_Word32 (0:01:38 elapsed time, 0:09:19 cpu time, factor 5.70)
03:10:29Running Timed_Automata (on hpcisabelle/0) ...
03:10:30Timed_Automata: theory Timed_Automata.Misc
03:10:30Timed_Automata: theory Timed_Automata.Floyd_Warshall
03:10:30Timed_Automata: theory Timed_Automata.Timed_Automata
03:10:35Timed_Automata: theory Timed_Automata.DBM
03:10:35Timed_Automata: theory Timed_Automata.Paths_Cycles
03:10:35Timed_Automata: theory Timed_Automata.Regions
03:10:39Timed_Automata: theory Timed_Automata.Closure
03:10:39Timed_Automata: theory Timed_Automata.DBM_Basics
03:10:40Timed_Automata: theory Timed_Automata.DBM_Normalization
03:10:41Timed_Automata: theory Timed_Automata.DBM_Operations
03:10:43Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
03:10:43Timed_Automata: theory Timed_Automata.Regions_Beta
03:10:47Timed_Automata: theory Timed_Automata.Approx_Beta
03:10:49Timed_Automata: theory Timed_Automata.Normalized_Zone_Semantics
03:12:37Preparing Timed_Automata/document ...
03:12:59Finished Timed_Automata/document (0:00:21 elapsed time)
03:12:59Preparing Timed_Automata/outline ...
03:13:06Finished Timed_Automata/outline (0:00:07 elapsed time)
03:13:06Timing Timed_Automata (8 threads, 124.035s elapsed time, 544.984s cpu time, 8.591s GC time, factor 4.39)
03:13:06Finished Timed_Automata (0:02:06 elapsed time, 0:09:10 cpu time, factor 4.36)
03:13:06Running Featherweight_OCL (on hpcisabelle/1) ...
03:13:13Featherweight_OCL: theory Featherweight_OCL.UML_Types
03:13:14Featherweight_OCL: theory Featherweight_OCL.UML_Logic
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_PropertyProfiles
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_Tools
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_Boolean
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_Integer
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_Pair
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_Real
03:13:16Featherweight_OCL: theory Featherweight_OCL.UML_String
03:13:17Featherweight_OCL: theory Featherweight_OCL.UML_Void
03:13:27Featherweight_OCL: theory Featherweight_OCL.UML_Sequence
03:13:29Featherweight_OCL: theory Featherweight_OCL.UML_Bag
03:13:29Featherweight_OCL: theory Featherweight_OCL.UML_Set
03:13:35Featherweight_OCL: theory Featherweight_OCL.UML_Library
03:14:24Featherweight_OCL: theory Featherweight_OCL.UML_State
03:14:26Featherweight_OCL: theory Featherweight_OCL.UML_Contracts
03:14:27Featherweight_OCL: theory Featherweight_OCL.UML_Main
03:14:28Featherweight_OCL: theory Featherweight_OCL.Analysis_UML
03:14:28Featherweight_OCL: theory Featherweight_OCL.Design_UML
03:14:44Featherweight_OCL: theory Featherweight_OCL.Analysis_OCL
03:15:08Featherweight_OCL: theory Featherweight_OCL.Design_OCL
03:15:12Preparing Featherweight_OCL/annex-a ...
03:16:22Finished Featherweight_OCL/annex-a (0:01:10 elapsed time)
03:16:22Preparing Featherweight_OCL/document ...
03:17:07Finished Featherweight_OCL/document (0:00:44 elapsed time)
03:17:07Preparing Featherweight_OCL/outline ...
03:17:45Finished Featherweight_OCL/outline (0:00:38 elapsed time)
03:17:45Timing Featherweight_OCL (8 threads, 121.732s elapsed time, 376.202s cpu time, 17.134s GC time, factor 3.09)
03:17:45Finished Featherweight_OCL (0:02:03 elapsed time, 0:06:20 cpu time, factor 3.07)
03:17:45Running Factored_Transition_System_Bounding (on hpcisabelle/2) ...
03:17:46Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.Acyclicity
03:17:46Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.RelUtils
03:17:46Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.HoArithUtils
03:17:46Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.SetUtils
03:17:46Factored_Transition_System_Bounding: theory HOL-Library.Conditional_Parametricity
03:17:46Factored_Transition_System_Bounding: theory HOL-Library.AList
03:17:46Factored_Transition_System_Bounding: theory HOL-Library.Old_Datatype
03:17:46Factored_Transition_System_Bounding: theory HOL-Library.Nat_Bijection
03:17:47Factored_Transition_System_Bounding: theory HOL-Library.Sublist
03:17:48Factored_Transition_System_Bounding: theory HOL-Library.Countable
03:17:49Factored_Transition_System_Bounding: theory HOL-Library.FSet
03:17:50Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.ListUtils
03:17:50Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.FSSublist
03:17:54Factored_Transition_System_Bounding: theory HOL-Library.Finite_Map
03:18:07Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.FactoredSystemLib
03:18:08Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.FmapUtils
03:18:08Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.FactoredSystem
03:18:10Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.ActionSeqProcess
03:18:10Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.Invariants
03:18:11Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.Dependency
03:18:11Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.TopologicalProps
03:18:13Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.SystemAbstraction
03:18:14Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.AcycSspace
03:19:09Preparing Factored_Transition_System_Bounding/document ...
03:19:20Finished Factored_Transition_System_Bounding/document (0:00:11 elapsed time)
03:19:20Preparing Factored_Transition_System_Bounding/outline ...
03:19:26Finished Factored_Transition_System_Bounding/outline (0:00:05 elapsed time)
03:19:26Timing Factored_Transition_System_Bounding (8 threads, 80.279s elapsed time, 189.517s cpu time, 3.989s GC time, factor 2.36)
03:19:26Finished Factored_Transition_System_Bounding (0:01:22 elapsed time, 0:03:13 cpu time, factor 2.35)
03:19:26Building Relational_Disjoint_Set_Forests (on hpcisabelle/3) ...
03:19:28Relational_Disjoint_Set_Forests: theory HOL-Hoare.Hoare_Syntax
03:19:28Relational_Disjoint_Set_Forests: theory HOL-Hoare.Hoare_Tac
03:19:31Relational_Disjoint_Set_Forests: theory HOL-Hoare.Hoare_Logic
03:19:32Relational_Disjoint_Set_Forests: theory Relational_Disjoint_Set_Forests.Disjoint_Set_Forests
03:20:03Relational_Disjoint_Set_Forests: theory Relational_Disjoint_Set_Forests.More_Disjoint_Set_Forests
03:20:42Relational_Disjoint_Set_Forests: theory Relational_Disjoint_Set_Forests.Matrix_Peano_Algebras
03:21:10Preparing Relational_Disjoint_Set_Forests/document ...
03:21:19Finished Relational_Disjoint_Set_Forests/document (0:00:09 elapsed time)
03:21:19Preparing Relational_Disjoint_Set_Forests/outline ...
03:21:23Finished Relational_Disjoint_Set_Forests/outline (0:00:03 elapsed time)
03:21:23Timing Relational_Disjoint_Set_Forests (8 threads, 87.751s elapsed time, 309.933s cpu time, 11.969s GC time, factor 3.53)
03:21:23Finished Relational_Disjoint_Set_Forests (0:01:43 elapsed time, 0:05:42 cpu time, factor 3.31)
03:21:23Running Polynomial_Factorization (on hpcisabelle/4) ...
03:21:26Polynomial_Factorization: theory Deriving.Derive_Manager
03:21:26Polynomial_Factorization: theory Deriving.Comparator
03:21:26Polynomial_Factorization: theory Containers.Extend_Partial_Order
03:21:26Polynomial_Factorization: theory Containers.List_Fusion
03:21:26Polynomial_Factorization: theory Deriving.Generator_Aux
03:21:26Polynomial_Factorization: theory Containers.Containers_Auxiliary
03:21:26Polynomial_Factorization: theory Polynomial_Interpolation.Missing_Unsorted
03:21:26Polynomial_Factorization: theory Cauchy.CauchysMeanTheorem
03:21:26Polynomial_Factorization: theory Polynomial_Interpolation.Improved_Code_Equations
03:21:27Polynomial_Factorization: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
03:21:27Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
03:21:27Polynomial_Factorization: theory Matrix.Utility
03:21:27Polynomial_Factorization: theory Containers.Containers_Generator
03:21:27Polynomial_Factorization: theory Polynomial_Interpolation.Divmod_Int
03:21:27Polynomial_Factorization: theory Polynomial_Interpolation.Ring_Hom
03:21:27Polynomial_Factorization: theory Polynomial_Factorization.Missing_List
03:21:28Polynomial_Factorization: theory Polynomial_Interpolation.Is_Rat_To_Rat
03:21:28Polynomial_Factorization: theory Sqrt_Babylonian.Log_Impl
03:21:28Polynomial_Factorization: theory Show.Show
03:21:28Polynomial_Factorization: theory Deriving.Compare
03:21:28Polynomial_Factorization: theory Deriving.Comparator_Generator
03:21:29Polynomial_Factorization: theory Containers.Lexicographic_Order
03:21:29Polynomial_Factorization: theory Containers.RBT_ext
03:21:29Polynomial_Factorization: theory Containers.Set_Linorder
03:21:29Polynomial_Factorization: theory Deriving.RBT_Comparator_Impl
03:21:29Polynomial_Factorization: theory Deriving.Compare_Generator
03:21:30Polynomial_Factorization: theory Polynomial_Interpolation.Missing_Polynomial
03:21:30Polynomial_Factorization: theory Deriving.Compare_Instances
03:21:30Polynomial_Factorization: theory Sqrt_Babylonian.NthRoot_Impl
03:21:31Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset
03:21:31Polynomial_Factorization: theory Show.Show_Instances
03:21:31Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian
03:21:31Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization
03:21:32Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial
03:21:32Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial
03:21:32Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Irreducibility
03:21:32Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
03:21:32Polynomial_Factorization: theory Polynomial_Interpolation.Lagrange_Interpolation
03:21:32Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots
03:21:32Polynomial_Factorization: theory Show.Show_Poly
03:21:34Polynomial_Factorization: theory Polynomial_Interpolation.Ring_Hom_Poly
03:21:38Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly
03:21:38Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma
03:21:38Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization
03:21:38Polynomial_Factorization: theory Polynomial_Interpolation.Newton_Interpolation
03:21:40Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly
03:21:40Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test
03:21:42Polynomial_Factorization: theory Polynomial_Interpolation.Polynomial_Interpolation
03:21:44Polynomial_Factorization: theory Containers.Collection_Order
03:21:47Polynomial_Factorization: theory Containers.RBT_Mapping2
03:21:49Polynomial_Factorization: theory Containers.RBT_Set2
03:21:51Polynomial_Factorization: theory Polynomial_Factorization.Precomputation
03:21:51Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization
03:21:54Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization
03:22:34Preparing Polynomial_Factorization/document ...
03:22:42Finished Polynomial_Factorization/document (0:00:08 elapsed time)
03:22:42Preparing Polynomial_Factorization/outline ...
03:22:47Finished Polynomial_Factorization/outline (0:00:04 elapsed time)
03:22:47Timing Polynomial_Factorization (8 threads, 65.203s elapsed time, 393.747s cpu time, 16.448s GC time, factor 6.04)
03:22:47Finished Polynomial_Factorization (0:01:08 elapsed time, 0:06:41 cpu time, factor 5.85)
03:22:47Running LTL_to_GBA (on hpcisabelle/5) ...
03:22:50LTL_to_GBA: theory LTL.LTL
03:23:07LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA
03:23:14LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA_impl
03:24:47LTL_to_GBA: theory LTL_to_GBA.All_Of_LTL_to_GBA
03:24:49Preparing LTL_to_GBA/document ...
03:24:55Finished LTL_to_GBA/document (0:00:06 elapsed time)
03:24:55Preparing LTL_to_GBA/outline ...
03:24:59Finished LTL_to_GBA/outline (0:00:03 elapsed time)
03:24:59Timing LTL_to_GBA (8 threads, 117.990s elapsed time, 608.012s cpu time, 22.779s GC time, factor 5.15)
03:24:59Finished LTL_to_GBA (0:02:01 elapsed time, 0:10:15 cpu time, factor 5.05)
03:24:59Running CRYSTALS-Kyber_Security (on hpcisabelle/6) ...
03:25:03CRYSTALS-Kyber_Security: theory Containers.Containers_Auxiliary
03:25:03CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Fraction_Field
03:25:03CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Group_Closure
03:25:03CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Nth_Powers
03:25:03CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Squarefree
03:25:03CRYSTALS-Kyber_Security: theory HOL-Number_Theory.Cong
03:25:03CRYSTALS-Kyber_Security: theory HOL-Algebra.FiniteProduct
03:25:03CRYSTALS-Kyber_Security: theory HOL-Algebra.Generated_Groups
03:25:03CRYSTALS-Kyber_Security: theory HOL-Combinatorics.List_Permutation
03:25:04CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Missing_Misc
03:25:04CRYSTALS-Kyber_Security: theory HOL-Algebra.Divisibility
03:25:04CRYSTALS-Kyber_Security: theory HOL-Library.LaTeXsugar
03:25:04CRYSTALS-Kyber_Security: theory HOL-Library.More_List
03:25:04CRYSTALS-Kyber_Security: theory Polynomial_Interpolation.Missing_Unsorted
03:25:04CRYSTALS-Kyber_Security: theory HOL-Algebra.Ring
03:25:04CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Field_as_Ring
03:25:04CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Polynomial
03:25:04CRYSTALS-Kyber_Security: theory HOL-Algebra.Elementary_Groups
03:25:05CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Normalized_Fraction
03:25:06CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Conjugate
03:25:06CRYSTALS-Kyber_Security: theory HOL-Number_Theory.Totient
03:25:06CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Delta_Correct
03:25:06CRYSTALS-Kyber_Security: theory Game_Based_Crypto.CryptHOL_Tutorial
03:25:06CRYSTALS-Kyber_Security: theory Matrix.Utility
03:25:06CRYSTALS-Kyber_Security: theory Polynomial_Interpolation.Ring_Hom
03:25:06CRYSTALS-Kyber_Security: theory Subresultants.Binary_Exponentiation
03:25:07CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Missing_List
03:25:09CRYSTALS-Kyber_Security: theory HOL-Algebra.AbelCoset
03:25:09CRYSTALS-Kyber_Security: theory HOL-Algebra.Module
03:25:10CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Missing_Ring
03:25:10CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Missing_Multiset
03:25:10CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.More_Missing_Multiset
03:25:13CRYSTALS-Kyber_Security: theory HOL-Algebra.Ideal
03:25:16CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Matrix
03:25:17CRYSTALS-Kyber_Security: theory HOL-Algebra.RingHom
03:25:17CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
03:25:17CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Polynomial_FPS
03:25:17CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Polynomial_Factorial
03:25:18CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Formal_Laurent_Series
03:25:19CRYSTALS-Kyber_Security: theory HOL-Algebra.UnivPoly
03:25:19CRYSTALS-Kyber_Security: theory Polynomial_Interpolation.Missing_Polynomial
03:25:21CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Missing_Polynomial_Factorial
03:25:21CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Order_Polynomial
03:25:21CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Polynomial_Irreducibility
03:25:22CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
03:25:22CRYSTALS-Kyber_Security: theory Polynomial_Interpolation.Ring_Hom_Poly
03:25:22CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
03:25:23CRYSTALS-Kyber_Security: theory HOL-Computational_Algebra.Computational_Algebra
03:25:24CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Column_Operations
03:25:25CRYSTALS-Kyber_Security: theory Jordan_Normal_Form.Determinant
03:25:25CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.Unique_Factorization
03:25:25CRYSTALS-Kyber_Security: theory Polynomial_Factorization.Square_Free_Factorization
03:25:27CRYSTALS-Kyber_Security: theory Subresultants.More_Homomorphisms
03:25:35CRYSTALS-Kyber_Security: theory HOL-Algebra.Multiplicative_Group
03:25:39CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
03:25:40CRYSTALS-Kyber_Security: theory HOL-Number_Theory.Residues
03:25:42CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.Poly_Mod
03:25:44CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.Finite_Field
03:25:47CRYSTALS-Kyber_Security: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
03:25:50CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber.Kyber_spec
03:25:52CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber.Mod_Plus_Minus
03:25:53CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Finite_UNIV
03:25:53CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber.Abs_Qr
03:25:53CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber.Compress
03:25:55CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Lemmas_for_spmf
03:25:55CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber.Crypto_Scheme
03:25:55CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Crypto_Scheme_new
03:25:56CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Kyber_new_Values
03:25:58CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.MLWE
03:26:00CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Correct
03:26:01CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Correct_new
03:26:07CRYSTALS-Kyber_Security: theory CRYSTALS-Kyber_Security.Kyber_gpv_IND_CPA
03:27:04Preparing CRYSTALS-Kyber_Security/document ...
03:27:08Finished CRYSTALS-Kyber_Security/document (0:00:03 elapsed time)
03:27:08Preparing CRYSTALS-Kyber_Security/outline ...
03:27:11Finished CRYSTALS-Kyber_Security/outline (0:00:03 elapsed time)
03:27:11Timing CRYSTALS-Kyber_Security (8 threads, 116.146s elapsed time, 807.115s cpu time, 58.143s GC time, factor 6.95)
03:27:11Finished CRYSTALS-Kyber_Security (0:02:00 elapsed time, 0:13:37 cpu time, factor 6.78)
03:27:11Building IMP2 (on hpcisabelle/7) ...
03:27:12IMP2: theory IMP2.IMP2_Utils
03:27:12IMP2: theory IMP2.Subgoal_Focus_Some
03:27:12IMP2: theory IMP2.Named_Simpsets
03:27:12IMP2: theory HOL-Library.Rewrite
03:27:12IMP2: theory HOL-Library.Cancellation
03:27:13IMP2: theory HOL-Library.Multiset
03:27:20IMP2: theory IMP2.IMP2_Aux_Lemmas
03:27:25IMP2: theory HOL-Eisbach.Eisbach
03:27:25IMP2: theory IMP2.Syntax
03:27:26IMP2: theory HOL-Eisbach.Eisbach_Tools
03:27:29IMP2: theory IMP2.Semantics
03:27:34IMP2: theory IMP2.Annotated_Syntax
03:27:35IMP2: theory IMP2.Parser
03:27:35IMP2: theory IMP2.IMP2_Basic_Simpset
03:27:35IMP2: theory IMP2.IMP2_Basic_Decls
03:27:35IMP2: theory IMP2.IMP2_Var_Abs
03:27:35IMP2: theory IMP2.IMP2_Var_Postprocessor
03:27:36IMP2: theory IMP2.IMP2_Program_Analysis
03:27:37IMP2: theory IMP2.IMP2_Specification
03:27:37IMP2: theory IMP2.IMP2_VCG
03:27:38IMP2: theory IMP2.IMP2
03:27:47IMP2: theory IMP2.IMP2_from_IMP
03:27:47IMP2: theory IMP2.Examples
03:27:47IMP2: theory IMP2.Quickstart_Guide
03:29:07Preparing IMP2/document ...
03:29:10Finished IMP2/document (0:00:03 elapsed time)
03:29:10Preparing IMP2/outline ...
03:29:13Finished IMP2/outline (0:00:03 elapsed time)
03:29:13Timing IMP2 (8 threads, 104.414s elapsed time, 339.430s cpu time, 4.379s GC time, factor 3.25)
03:29:13Finished IMP2 (0:01:54 elapsed time, 0:05:59 cpu time, factor 3.14)
03:29:13Running KAD (on hpcisabelle/0) ...
03:29:15KAD: theory Kleene_Algebra.Signatures
03:29:15KAD: theory Kleene_Algebra.Dioid
03:29:33KAD: theory Kleene_Algebra.Conway
03:29:33KAD: theory Kleene_Algebra.Dioid_Models
03:29:44KAD: theory Kleene_Algebra.Kleene_Algebra
03:29:53KAD: theory KAD.Domain_Semiring
03:29:53KAD: theory Kleene_Algebra.Kleene_Algebra_Models
03:30:07KAD: theory KAD.Antidomain_Semiring
03:30:27KAD: theory KAD.Modal_Kleene_Algebra_Applications
03:30:27KAD: theory KAD.Range_Semiring
03:30:50KAD: theory KAD.Modal_Kleene_Algebra
03:31:01KAD: theory KAD.Modal_Kleene_Algebra_Models
03:31:15Preparing KAD/document ...
03:31:20Finished KAD/document (0:00:04 elapsed time)
03:31:20Preparing KAD/outline ...
03:31:23Finished KAD/outline (0:00:03 elapsed time)
03:31:23Timing KAD (8 threads, 118.763s elapsed time, 232.571s cpu time, 5.698s GC time, factor 1.96)
03:31:23Finished KAD (0:02:00 elapsed time, 0:03:57 cpu time, factor 1.96)
03:31:23Running Regular_Algebras (on hpcisabelle/1) ...
03:31:25Regular_Algebras: theory Regular_Algebras.Dioid_Power_Sum
03:31:26Regular_Algebras: theory Regular_Algebras.Regular_Algebras
03:32:53Regular_Algebras: theory Regular_Algebras.Pratts_Counterexamples
03:32:53Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Models
03:32:56Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Variants
03:33:25Preparing Regular_Algebras/document ...
03:33:30Finished Regular_Algebras/document (0:00:04 elapsed time)
03:33:30Preparing Regular_Algebras/outline ...
03:33:33Finished Regular_Algebras/outline (0:00:03 elapsed time)
03:33:33Timing Regular_Algebras (8 threads, 119.503s elapsed time, 200.345s cpu time, 4.359s GC time, factor 1.68)
03:33:33Finished Regular_Algebras (0:02:01 elapsed time, 0:03:25 cpu time, factor 1.68)
03:33:33Running Linear_Programming (on hpcisabelle/2) ...
03:33:36Linear_Programming: theory Simplex.Simplex_Auxiliary
03:33:36Linear_Programming: theory Simplex.Simplex_Algebra
03:33:36Linear_Programming: theory Linear_Programming.More_Jordan_Normal_Forms
03:33:36Linear_Programming: theory Simplex.Rel_Chain
03:33:40Linear_Programming: theory Simplex.Abstract_Linear_Poly
03:33:41Linear_Programming: theory Simplex.Linear_Poly_Maps
03:33:41Linear_Programming: theory Simplex.QDelta
03:33:42Linear_Programming: theory Simplex.Simplex
03:34:03Linear_Programming: theory Farkas.Farkas
03:34:04Linear_Programming: theory Simplex.Simplex_Incremental
03:34:08Linear_Programming: theory Farkas.Matrix_Farkas
03:34:14Linear_Programming: theory Farkas.Simplex_for_Reals
03:34:15Linear_Programming: theory Linear_Programming.Matrix_LinPoly
03:34:18Linear_Programming: theory Linear_Programming.LP_Preliminaries
03:34:28Linear_Programming: theory Linear_Programming.Linear_Programming
03:35:33Preparing Linear_Programming/document ...
03:35:38Finished Linear_Programming/document (0:00:05 elapsed time)
03:35:38Preparing Linear_Programming/outline ...
03:35:42Finished Linear_Programming/outline (0:00:03 elapsed time)
03:35:42Timing Linear_Programming (8 threads, 114.785s elapsed time, 505.192s cpu time, 17.083s GC time, factor 4.40)
03:35:42Finished Linear_Programming (0:01:58 elapsed time, 0:08:31 cpu time, factor 4.32)
03:35:42Running Simple_Clause_Learning (on hpcisabelle/3) ...
03:35:44Simple_Clause_Learning: theory Deriving.Comparator
03:35:44Simple_Clause_Learning: theory Deriving.Equality_Generator
03:35:44Simple_Clause_Learning: theory Simple_Clause_Learning.Multiset_Order_Extra
03:35:44Simple_Clause_Learning: theory HOL-Cardinals.Order_Union
03:35:44Simple_Clause_Learning: theory Word_Lib.More_Divides
03:35:44Simple_Clause_Learning: theory Word_Lib.Bit_Comprehension
03:35:44Simple_Clause_Learning: theory Word_Lib.Signed_Division_Word
03:35:44Simple_Clause_Learning: theory Nested_Multisets_Ordinals.Multiset_More
03:35:44Simple_Clause_Learning: theory Deriving.Countable_Generator
03:35:44Simple_Clause_Learning: theory HOL-Cardinals.Wellorder_Extension
03:35:44Simple_Clause_Learning: theory Coinductive.Coinductive_Nat
03:35:45Simple_Clause_Learning: theory List-Index.List_Index
03:35:45Simple_Clause_Learning: theory Native_Word.Code_Int_Integer_Conversion
03:35:45Simple_Clause_Learning: theory Open_Induction.Restricted_Predicates
03:35:45Simple_Clause_Learning: theory Deriving.Equality_Instances
03:35:45Simple_Clause_Learning: theory Ordered_Resolution_Prover.Map2
03:35:45Simple_Clause_Learning: theory Knuth_Bendix_Order.Order_Pair
03:35:45Simple_Clause_Learning: theory Simple_Clause_Learning.Abstract_Renaming_Apart
03:35:45Simple_Clause_Learning: theory Word_Lib.More_Arithmetic
03:35:46Simple_Clause_Learning: theory Word_Lib.More_Bit_Ring
03:35:46Simple_Clause_Learning: theory Ordered_Resolution_Prover.Clausal_Logic
03:35:46Simple_Clause_Learning: theory Knuth_Bendix_Order.Lexicographic_Extension
03:35:46Simple_Clause_Learning: theory Simple_Clause_Learning.Trail_Induced_Ordering
03:35:46Simple_Clause_Learning: theory Deriving.Compare
03:35:46Simple_Clause_Learning: theory Deriving.Comparator_Generator
03:35:46Simple_Clause_Learning: theory Coinductive.Coinductive_List
03:35:47Simple_Clause_Learning: theory Ordered_Resolution_Prover.Herbrand_Interpretation
03:35:47Simple_Clause_Learning: theory Ordered_Resolution_Prover.Abstract_Substitution
03:35:47Simple_Clause_Learning: theory Word_Lib.More_Word
03:35:47Simple_Clause_Learning: theory Knuth_Bendix_Order.KBO
03:35:47Simple_Clause_Learning: theory Ordered_Resolution_Prover.Ground_Resolution_Model
03:35:47Simple_Clause_Learning: theory Ordered_Resolution_Prover.Inference_System
03:35:47Simple_Clause_Learning: theory Deriving.Compare_Generator
03:35:48Simple_Clause_Learning: theory Deriving.Compare_Instances
03:35:49Simple_Clause_Learning: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
03:35:49Simple_Clause_Learning: theory Native_Word.Code_Target_Word_Base
03:35:49Simple_Clause_Learning: theory Word_Lib.Bit_Shifts_Infix_Syntax
03:35:49Simple_Clause_Learning: theory Word_Lib.Least_significant_bit
03:35:50Simple_Clause_Learning: theory Simple_Clause_Learning.Ordered_Resolution_Prover_Extra
03:35:51Simple_Clause_Learning: theory Word_Lib.Most_significant_bit
03:35:51Simple_Clause_Learning: theory Word_Lib.Generic_set_bit
03:35:52Simple_Clause_Learning: theory Native_Word.Code_Target_Integer_Bit
03:35:52Simple_Clause_Learning: theory Native_Word.Word_Type_Copies
03:35:54Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Liminf
03:35:55Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Chain
03:36:04Simple_Clause_Learning: theory Saturation_Framework.Calculus
03:36:04Simple_Clause_Learning: theory Simple_Clause_Learning.Wellfounded_Extra
03:36:06Simple_Clause_Learning: theory Saturation_Framework_Extensions.Soundness
03:36:06Simple_Clause_Learning: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
03:36:07Simple_Clause_Learning: theory Saturation_Framework_Extensions.Clausal_Calculus
03:36:07Simple_Clause_Learning: theory Native_Word.Uint32
03:36:08Simple_Clause_Learning: theory Simple_Clause_Learning.SCL_FOL
03:36:09Simple_Clause_Learning: theory Collections.HashCode
03:36:10Simple_Clause_Learning: theory Deriving.Hash_Generator
03:36:11Simple_Clause_Learning: theory Deriving.Hash_Instances
03:36:11Simple_Clause_Learning: theory Deriving.Derive
03:36:12Simple_Clause_Learning: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
03:36:18Simple_Clause_Learning: theory Simple_Clause_Learning.Correct_Termination
03:36:18Simple_Clause_Learning: theory Simple_Clause_Learning.Initial_Literals_Generalize_Learned_Literals
03:36:19Simple_Clause_Learning: theory Simple_Clause_Learning.Invariants
03:36:19Simple_Clause_Learning: theory Simple_Clause_Learning.Non_Redundancy
03:36:23Simple_Clause_Learning: theory Simple_Clause_Learning.Termination
03:36:25Simple_Clause_Learning: theory Simple_Clause_Learning.Completeness
03:37:47Preparing Simple_Clause_Learning/document ...
03:37:59Finished Simple_Clause_Learning/document (0:00:12 elapsed time)
03:37:59Preparing Simple_Clause_Learning/outline ...
03:38:05Finished Simple_Clause_Learning/outline (0:00:05 elapsed time)
03:38:05Timing Simple_Clause_Learning (8 threads, 118.020s elapsed time, 609.739s cpu time, 19.775s GC time, factor 5.17)
03:38:05Finished Simple_Clause_Learning (0:02:01 elapsed time, 0:10:20 cpu time, factor 5.09)
03:38:05Running Karatsuba (on hpcisabelle/4) ...
03:38:08Karatsuba: theory HOL-Eisbach.Eisbach
03:38:08Karatsuba: theory HOL-Library.Adhoc_Overloading
03:38:08Karatsuba: theory HOL-Number_Theory.Cong
03:38:08Karatsuba: theory HOL-Library.Code_Binary_Nat
03:38:08Karatsuba: theory HOL-Algebra.Congruence
03:38:08Karatsuba: theory Karatsuba.Abstract_Representations
03:38:08Karatsuba: theory Karatsuba.Abstract_Representations_2
03:38:08Karatsuba: theory Karatsuba.Karatsuba_Runtime_Lemmas
03:38:08Karatsuba: theory HOL-Library.Monad_Syntax
03:38:09Karatsuba: theory Root_Balanced_Tree.Time_Monad
03:38:09Karatsuba: theory HOL-Eisbach.Eisbach_Tools
03:38:10Karatsuba: theory Expander_Graphs.Extra_Congruence_Method
03:38:10Karatsuba: theory Karatsuba.Estimation_Method
03:38:10Karatsuba: theory HOL-Algebra.Order
03:38:10Karatsuba: theory Karatsuba.Time_Monad_Extended
03:38:10Karatsuba: theory Karatsuba.Main_TM
03:38:10Karatsuba: theory HOL-Number_Theory.Totient
03:38:11Karatsuba: theory HOL-Algebra.Lattice
03:38:12Karatsuba: theory HOL-Algebra.Complete_Lattice
03:38:14Karatsuba: theory HOL-Algebra.Group
03:38:17Karatsuba: theory HOL-Algebra.Coset
03:38:17Karatsuba: theory HOL-Algebra.FiniteProduct
03:38:18Karatsuba: theory HOL-Algebra.Ring
03:38:20Karatsuba: theory HOL-Algebra.Generated_Groups
03:38:21Karatsuba: theory HOL-Algebra.Elementary_Groups
03:38:23Karatsuba: theory HOL-Algebra.AbelCoset
03:38:23Karatsuba: theory HOL-Algebra.Module
03:38:28Karatsuba: theory HOL-Algebra.Ideal
03:38:31Karatsuba: theory HOL-Algebra.RingHom
03:38:32Karatsuba: theory HOL-Algebra.QuotRing
03:38:32Karatsuba: theory HOL-Algebra.UnivPoly
03:38:36Karatsuba: theory HOL-Algebra.IntRing
03:38:47Karatsuba: theory HOL-Algebra.Multiplicative_Group
03:38:52Karatsuba: theory HOL-Number_Theory.Residues
03:38:55Karatsuba: theory Karatsuba.Karatsuba_Preliminaries
03:38:58Karatsuba: theory Karatsuba.Karatsuba_Sum_Lemmas
03:38:59Karatsuba: theory Karatsuba.Monoid_Sums
03:38:59Karatsuba: theory Karatsuba.Nat_LSBF
03:39:03Karatsuba: theory Karatsuba.Int_LSBF
03:39:03Karatsuba: theory Karatsuba.Nat_LSBF_TM
03:39:05Karatsuba: theory Karatsuba.Karatsuba
03:39:07Karatsuba: theory Karatsuba.Karatsuba_Code_Nat
03:39:08Karatsuba: theory Karatsuba.Karatsuba_TM
03:39:22Preparing Karatsuba/document ...
03:39:31Finished Karatsuba/document (0:00:08 elapsed time)
03:39:31Preparing Karatsuba/outline ...
03:39:36Finished Karatsuba/outline (0:00:05 elapsed time)
03:39:36Timing Karatsuba (8 threads, 71.458s elapsed time, 365.098s cpu time, 13.804s GC time, factor 5.11)
03:39:36Finished Karatsuba (0:01:15 elapsed time, 0:06:13 cpu time, factor 4.96)
03:39:36Running Grothendieck_Schemes (on hpcisabelle/5) ...
03:39:38Grothendieck_Schemes: theory HOL-Library.FuncSet
03:39:39Grothendieck_Schemes: theory Jacobson_Basic_Algebra.Set_Theory
03:39:39Grothendieck_Schemes: theory Grothendieck_Schemes.Set_Extras
03:39:39Grothendieck_Schemes: theory Jacobson_Basic_Algebra.Group_Theory
03:39:39Grothendieck_Schemes: theory Grothendieck_Schemes.Topological_Space
03:39:56Grothendieck_Schemes: theory Grothendieck_Schemes.Group_Extras
03:39:56Grothendieck_Schemes: theory Jacobson_Basic_Algebra.Ring_Theory
03:40:30Grothendieck_Schemes: theory Grothendieck_Schemes.Comm_Ring
03:40:54Grothendieck_Schemes: theory Grothendieck_Schemes.Scheme
03:41:38Preparing Grothendieck_Schemes/document ...
03:41:46Finished Grothendieck_Schemes/document (0:00:07 elapsed time)
03:41:46Preparing Grothendieck_Schemes/outline ...
03:41:50Finished Grothendieck_Schemes/outline (0:00:04 elapsed time)
03:41:50Timing Grothendieck_Schemes (8 threads, 118.343s elapsed time, 446.262s cpu time, 15.105s GC time, factor 3.77)
03:41:50Finished Grothendieck_Schemes (0:02:00 elapsed time, 0:07:32 cpu time, factor 3.75)
03:41:50Running WebAssembly (on hpcisabelle/6) ...
03:41:52WebAssembly: theory Word_Lib.Bit_Comprehension
03:41:52WebAssembly: theory Word_Lib.Legacy_Aliases
03:41:52WebAssembly: theory Word_Lib.More_Divides
03:41:52WebAssembly: theory Word_Lib.Signed_Division_Word
03:41:52WebAssembly: theory Native_Word.Code_Int_Integer_Conversion
03:41:52WebAssembly: theory WebAssembly.Wasm_Type_Abs
03:41:52WebAssembly: theory Word_Lib.Even_More_List
03:41:52WebAssembly: theory Word_Lib.More_Arithmetic
03:41:53WebAssembly: theory Word_Lib.More_Bit_Ring
03:41:54WebAssembly: theory Word_Lib.More_Word
03:41:56WebAssembly: theory Native_Word.Code_Target_Word_Base
03:41:56WebAssembly: theory Word_Lib.Bit_Shifts_Infix_Syntax
03:41:56WebAssembly: theory Word_Lib.Least_significant_bit
03:41:58WebAssembly: theory Word_Lib.Aligned
03:41:58WebAssembly: theory Word_Lib.Most_significant_bit
03:41:58WebAssembly: theory Word_Lib.Singleton_Bit_Shifts
03:41:59WebAssembly: theory Word_Lib.Generic_set_bit
03:42:00WebAssembly: theory Word_Lib.Bits_Int
03:42:00WebAssembly: theory Native_Word.Word_Type_Copies
03:42:00WebAssembly: theory Native_Word.Code_Target_Integer_Bit
03:42:04WebAssembly: theory Word_Lib.Typedef_Morphisms
03:42:04WebAssembly: theory Word_Lib.Reversed_Bit_Lists
03:42:14WebAssembly: theory Native_Word.Uint8
03:42:16WebAssembly: theory WebAssembly.Wasm_Ast
03:42:34WebAssembly: theory WebAssembly.Wasm_Base_Defs
03:42:35WebAssembly: theory WebAssembly.Wasm
03:42:37WebAssembly: theory WebAssembly.Wasm_Axioms
03:42:37WebAssembly: theory WebAssembly.Wasm_Checker_Types
03:42:37WebAssembly: theory WebAssembly.Wasm_Interpreter
03:42:37WebAssembly: theory WebAssembly.Wasm_Properties_Aux
03:42:38WebAssembly: theory WebAssembly.Wasm_Properties
03:42:38WebAssembly: theory WebAssembly.Wasm_Soundness
03:42:40WebAssembly: theory WebAssembly.Wasm_Checker
03:42:47WebAssembly: theory WebAssembly.Wasm_Checker_Properties
03:42:47WebAssembly: theory WebAssembly.Wasm_Interpreter_Properties
03:43:22WebAssembly: theory Native_Word.Code_Target_Int_Bit
03:43:22WebAssembly: theory WebAssembly.Wasm_Checker_Printing
03:43:22WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing
03:43:22WebAssembly: theory WebAssembly.Wasm_Type_Abs_Printing
03:43:22WebAssembly: theory WebAssembly.Wasm_Printing
03:43:22WebAssembly: theory WebAssembly.Wasm_Interpreter_Printing_Pure
03:43:28Preparing WebAssembly/document ...
03:43:40Finished WebAssembly/document (0:00:12 elapsed time)
03:43:40Preparing WebAssembly/outline ...
03:43:46Finished WebAssembly/outline (0:00:05 elapsed time)
03:43:47Timing WebAssembly (8 threads, 93.515s elapsed time, 472.639s cpu time, 8.912s GC time, factor 5.05)
03:43:47Finished WebAssembly (0:01:36 elapsed time, 0:07:58 cpu time, factor 4.96)
03:43:47Running Inductive_Inference (on hpcisabelle/7) ...
03:43:48Inductive_Inference: theory HOL-Library.Nat_Bijection
03:43:49Inductive_Inference: theory Inductive_Inference.Partial_Recursive
03:43:53Inductive_Inference: theory Inductive_Inference.Universal
03:43:56Inductive_Inference: theory Inductive_Inference.Standard_Results
03:43:57Inductive_Inference: theory Inductive_Inference.Inductive_Inference_Basics
03:43:58Inductive_Inference: theory Inductive_Inference.CONS_LIM
03:43:58Inductive_Inference: theory Inductive_Inference.CP_FIN_NUM
03:43:58Inductive_Inference: theory Inductive_Inference.Lemma_R
03:43:59Inductive_Inference: theory Inductive_Inference.LIM_BC
03:43:59Inductive_Inference: theory Inductive_Inference.R1_BC
03:44:00Inductive_Inference: theory Inductive_Inference.TOTAL_CONS
03:44:01Inductive_Inference: theory Inductive_Inference.Union
03:45:25Preparing Inductive_Inference/document ...
03:45:40Finished Inductive_Inference/document (0:00:14 elapsed time)
03:45:40Preparing Inductive_Inference/outline ...
03:45:47Finished Inductive_Inference/outline (0:00:07 elapsed time)
03:45:47Timing Inductive_Inference (8 threads, 95.407s elapsed time, 387.397s cpu time, 3.190s GC time, factor 4.06)
03:45:47Finished Inductive_Inference (0:01:37 elapsed time, 0:06:30 cpu time, factor 4.02)
03:45:47Running Dependent_SIFUM_Refinement (on hpcisabelle/0) ...
03:45:49Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.CompositionalRefinement
03:46:02Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg2
03:46:02Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.EgHighBranchRevC
03:46:02Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1
03:46:09Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2
03:46:09Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial
03:46:17Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple
03:47:46Preparing Dependent_SIFUM_Refinement/document ...
03:47:52Finished Dependent_SIFUM_Refinement/document (0:00:05 elapsed time)
03:47:52Preparing Dependent_SIFUM_Refinement/outline ...
03:47:56Finished Dependent_SIFUM_Refinement/outline (0:00:03 elapsed time)
03:47:56Timing Dependent_SIFUM_Refinement (8 threads, 114.765s elapsed time, 416.345s cpu time, 7.399s GC time, factor 3.63)
03:47:56Finished Dependent_SIFUM_Refinement (0:01:57 elapsed time, 0:07:00 cpu time, factor 3.59)
03:47:56Building Simplex (on hpcisabelle/1) ...
03:47:58Simplex: theory Simplex.Simplex_Auxiliary
03:47:58Simplex: theory Simplex.Simplex_Algebra
03:47:58Simplex: theory Simplex.Rel_Chain
03:48:02Simplex: theory Simplex.Abstract_Linear_Poly
03:48:03Simplex: theory Simplex.Linear_Poly_Maps
03:48:03Simplex: theory Simplex.QDelta
03:48:04Simplex: theory Simplex.Simplex
03:48:25Simplex: theory Simplex.Simplex_Incremental
03:49:17Preparing Simplex/document ...
03:49:30Finished Simplex/document (0:00:13 elapsed time)
03:49:30Preparing Simplex/outline ...
03:49:37Finished Simplex/outline (0:00:06 elapsed time)
03:49:37Timing Simplex (8 threads, 61.139s elapsed time, 291.562s cpu time, 13.176s GC time, factor 4.77)
03:49:37Finished Simplex (0:01:19 elapsed time, 0:05:29 cpu time, factor 4.13)
03:49:37Running KBPs (on hpcisabelle/2) ...
03:49:39KBPs: theory KBPs.Extra
03:49:39KBPs: theory KBPs.List_local
03:50:08KBPs: theory Trie.Trie
03:50:08KBPs: theory KBPs.ODList
03:50:08KBPs: theory KBPs.DFS
03:50:08KBPs: theory KBPs.Kripke
03:50:08KBPs: theory KBPs.MapOps
03:50:08KBPs: theory KBPs.Traces
03:50:08KBPs: theory Transitive-Closure.Transitive_Closure_Impl
03:50:09KBPs: theory Transitive-Closure.Transitive_Closure_List_Impl
03:50:11KBPs: theory KBPs.Trie2
03:50:11KBPs: theory KBPs.Eval
03:50:11KBPs: theory KBPs.KBPs
03:50:13KBPs: theory KBPs.KBPsAuto
03:50:16KBPs: theory KBPs.KBPsAlg
03:50:18KBPs: theory KBPs.SPRView
03:50:18KBPs: theory KBPs.SPRViewNonDet
03:50:19KBPs: theory KBPs.SPRViewSingle
03:50:22KBPs: theory KBPs.SPRViewNonDetIndInit
03:50:24KBPs: theory KBPs.ClockView
03:50:25KBPs: theory KBPs.SPRViewDet
03:50:30KBPs: theory KBPs.Robot
03:50:35KBPs: theory KBPs.MuddyChildren
03:50:36KBPs: theory KBPs.Views
03:50:43KBPs: theory KBPs.Examples
03:50:46KBPs: theory KBPs.KBPs_Main
03:51:26Preparing KBPs/document ...
03:51:30Finished KBPs/document (0:00:04 elapsed time)
03:51:30Preparing KBPs/outline ...
03:51:35Finished KBPs/outline (0:00:04 elapsed time)
03:51:35Timing KBPs (8 threads, 105.196s elapsed time, 417.075s cpu time, 8.033s GC time, factor 3.96)
03:51:35Finished KBPs (0:01:47 elapsed time, 0:07:02 cpu time, factor 3.91)
03:51:35Running Containers-Benchmarks (on hpcisabelle/3) ...
03:51:38Containers-Benchmarks: theory HOL-Eisbach.Eisbach
03:51:38Containers-Benchmarks: theory Automatic_Refinement.Foldi
03:51:38Containers-Benchmarks: theory Automatic_Refinement.Refine_Util_Bootstrap1
03:51:38Containers-Benchmarks: theory Automatic_Refinement.Prio_List
03:51:38Containers-Benchmarks: theory Collections.ICF_Tools
03:51:38Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Comparison
03:51:38Containers-Benchmarks: theory Finger-Trees.FingerTree
03:51:38Containers-Benchmarks: theory Trie.Trie
03:51:38Containers-Benchmarks: theory Automatic_Refinement.Mk_Term_Antiquot
03:51:38Containers-Benchmarks: theory Automatic_Refinement.Mpat_Antiquot
03:51:38Containers-Benchmarks: theory Collections.Ord_Code_Preproc
03:51:38Containers-Benchmarks: theory Binomial-Heaps.BinomialHeap
03:51:38Containers-Benchmarks: theory Binomial-Heaps.SkewBinomialHeap
03:51:39Containers-Benchmarks: theory Collections.Locale_Code
03:51:39Containers-Benchmarks: theory Automatic_Refinement.Refine_Util
03:51:39Containers-Benchmarks: theory Collections.Record_Intf
03:51:39Containers-Benchmarks: theory HOL-ex.Quicksort
03:51:39Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set
03:51:39Containers-Benchmarks: theory Automatic_Refinement.Anti_Unification
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Attr_Comb
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Named_Sorted_Thms
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Autoref_Data
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Indep_Vars
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Mk_Record_Simp
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Tagged_Solver
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Select_Solve
03:51:40Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Default
03:51:40Containers-Benchmarks: theory Automatic_Refinement.Misc
03:51:40Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_RBT
03:51:40Containers-Benchmarks: theory Collections.DatRef
03:51:40Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Bool
03:51:41Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_LC
03:51:41Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_Default
03:51:41Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_LC
03:51:43Containers-Benchmarks: theory Containers-Benchmarks.Clauses
03:51:43Containers-Benchmarks: theory Refine_Monadic.Refine_Chapter
03:51:43Containers-Benchmarks: theory Native_Word.Code_Target_Int_Bit
03:51:43Containers-Benchmarks: theory Collections.Code_Target_ICF
03:51:48Containers-Benchmarks: theory Automatic_Refinement.Refine_Lib
03:51:48Containers-Benchmarks: theory Collections.SetIterator
03:51:49Containers-Benchmarks: theory Collections.Sorted_List_Operations
03:51:50Containers-Benchmarks: theory Automatic_Refinement.Autoref_Phases
03:51:50Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tagging
03:51:50Containers-Benchmarks: theory Automatic_Refinement.Relators
03:51:50Containers-Benchmarks: theory Refine_Monadic.Refine_Mono_Prover
03:51:51Containers-Benchmarks: theory Collections.SetIteratorOperations
03:51:52Containers-Benchmarks: theory Automatic_Refinement.Param_Tool
03:51:52Containers-Benchmarks: theory Automatic_Refinement.Param_HOL
03:51:53Containers-Benchmarks: theory Automatic_Refinement.Parametricity
03:51:53Containers-Benchmarks: theory Automatic_Refinement.Autoref_Id_Ops
03:51:54Containers-Benchmarks: theory Collections.Assoc_List
03:51:54Containers-Benchmarks: theory Collections.Dlist_add
03:51:54Containers-Benchmarks: theory Collections.Proper_Iterator
03:51:54Containers-Benchmarks: theory Collections.SetIteratorGA
03:51:54Containers-Benchmarks: theory Collections.Diff_Array
03:51:54Containers-Benchmarks: theory Collections.Trie_Impl
03:51:55Containers-Benchmarks: theory Collections.It_to_It
03:51:55Containers-Benchmarks: theory Automatic_Refinement.Autoref_Fix_Rel
03:51:55Containers-Benchmarks: theory Collections.Trie2
03:51:56Containers-Benchmarks: theory Automatic_Refinement.Autoref_Translate
03:51:56Containers-Benchmarks: theory Automatic_Refinement.Autoref_Relator_Interface
03:51:56Containers-Benchmarks: theory Automatic_Refinement.Autoref_Gen_Algo
03:51:56Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tool
03:51:56Containers-Benchmarks: theory Automatic_Refinement.Autoref_Bindings_HOL
03:52:01Containers-Benchmarks: theory Automatic_Refinement.Automatic_Refinement
03:52:01Containers-Benchmarks: theory Collections.Idx_Iterator
03:52:01Containers-Benchmarks: theory Refine_Monadic.Refine_Misc
03:52:02Containers-Benchmarks: theory Refine_Monadic.RefineG_Domain
03:52:02Containers-Benchmarks: theory Refine_Monadic.RefineG_Transfer
03:52:03Containers-Benchmarks: theory Refine_Monadic.RefineG_Assert
03:52:04Containers-Benchmarks: theory Refine_Monadic.RefineG_Recursion
03:52:04Containers-Benchmarks: theory Refine_Monadic.RefineG_While
03:52:04Containers-Benchmarks: theory Refine_Monadic.Refine_Basic
03:52:05Containers-Benchmarks: theory Refine_Monadic.Refine_Det
03:52:09Containers-Benchmarks: theory Refine_Monadic.Refine_Heuristics
03:52:09Containers-Benchmarks: theory Refine_Monadic.Refine_Leof
03:52:09Containers-Benchmarks: theory Refine_Monadic.Refine_Pfun
03:52:09Containers-Benchmarks: theory Refine_Monadic.Refine_While
03:52:09Containers-Benchmarks: theory Refine_Monadic.Refine_More_Comb
03:52:11Containers-Benchmarks: theory Refine_Monadic.Refine_Transfer
03:52:12Containers-Benchmarks: theory Refine_Monadic.Autoref_Monadic
03:52:12Containers-Benchmarks: theory Refine_Monadic.Refine_Automation
03:52:12Containers-Benchmarks: theory Refine_Monadic.Refine_Foreach
03:52:15Containers-Benchmarks: theory Refine_Monadic.Refine_Monadic
03:52:16Containers-Benchmarks: theory Collections.Gen_Iterator
03:52:16Containers-Benchmarks: theory Collections.Intf_Map
03:52:16Containers-Benchmarks: theory Collections.Intf_Set
03:52:17Containers-Benchmarks: theory Collections.Iterator
03:52:18Containers-Benchmarks: theory Collections.Array_Iterator
03:52:18Containers-Benchmarks: theory Collections.ICF_Spec_Base
03:52:18Containers-Benchmarks: theory Collections.RBT_add
03:52:19Containers-Benchmarks: theory Collections.AnnotatedListSpec
03:52:20Containers-Benchmarks: theory Collections.ListSpec
03:52:21Containers-Benchmarks: theory Collections.FTAnnotatedListImpl
03:52:22Containers-Benchmarks: theory Collections.ListGA
03:52:22Containers-Benchmarks: theory Collections.Fifo
03:52:25Containers-Benchmarks: theory Collections.MapSpec
03:52:26Containers-Benchmarks: theory Collections.PrioSpec
03:52:27Containers-Benchmarks: theory Collections.BinoPrioImpl
03:52:29Containers-Benchmarks: theory Collections.PrioByAnnotatedList
03:52:31Containers-Benchmarks: theory Collections.SkewPrioImpl
03:52:31Containers-Benchmarks: theory Collections.FTPrioImpl
03:52:32Containers-Benchmarks: theory Collections.PrioUniqueSpec
03:52:32Containers-Benchmarks: theory Collections.SetSpec
03:52:33Containers-Benchmarks: theory Collections.PrioUniqueByAnnotatedList
03:52:38Containers-Benchmarks: theory Collections.FTPrioUniqueImpl
03:52:39Containers-Benchmarks: theory Collections.Algos
03:52:39Containers-Benchmarks: theory Collections.SetIndex
03:52:39Containers-Benchmarks: theory Collections.SetIteratorCollectionsGA
03:52:39Containers-Benchmarks: theory Collections.MapGA
03:52:39Containers-Benchmarks: theory Collections.SetGA
03:52:42Containers-Benchmarks: theory Collections.ArrayMapImpl
03:52:42Containers-Benchmarks: theory Collections.ListMapImpl
03:52:42Containers-Benchmarks: theory Collections.ListMapImpl_Invar
03:52:43Containers-Benchmarks: theory Collections.TrieMapImpl
03:52:43Containers-Benchmarks: theory Collections.RBTMapImpl
03:52:45Containers-Benchmarks: theory Collections.ListSetImpl
03:52:45Containers-Benchmarks: theory Collections.ListSetImpl_Invar
03:52:45Containers-Benchmarks: theory Collections.ListSetImpl_NotDist
03:52:47Containers-Benchmarks: theory Collections.ListSetImpl_Sorted
03:52:48Containers-Benchmarks: theory Collections.SetByMap
03:52:48Containers-Benchmarks: theory Collections.ArrayHashMap_Impl
03:52:50Containers-Benchmarks: theory Collections.HashMap_Impl
03:52:51Containers-Benchmarks: theory Collections.ArraySetImpl
03:52:51Containers-Benchmarks: theory Collections.TrieSetImpl
03:52:51Containers-Benchmarks: theory Collections.RBTSetImpl
03:52:52Containers-Benchmarks: theory Collections.HashMap
03:52:52Containers-Benchmarks: theory Collections.ArrayHashMap
03:52:58Containers-Benchmarks: theory Collections.HashSet
03:52:59Containers-Benchmarks: theory Collections.ArrayHashSet
03:52:59Containers-Benchmarks: theory Collections.MapStdImpl
03:53:05Containers-Benchmarks: theory Collections.SetStdImpl
03:53:08Containers-Benchmarks: theory Collections.ICF_Impl
03:53:11Containers-Benchmarks: theory Collections.ICF_Refine_Monadic
03:53:12Containers-Benchmarks: theory Collections.ICF_Autoref
03:53:15Containers-Benchmarks: theory Collections.Collections
03:53:16Containers-Benchmarks: theory Collections.CollectionsV1
03:53:22Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_ICF
03:53:41Timing Containers-Benchmarks (8 threads, 117.679s elapsed time, 545.525s cpu time, 46.086s GC time, factor 4.64)
03:53:41Finished Containers-Benchmarks (0:02:02 elapsed time, 0:09:21 cpu time, factor 4.58)
03:53:41Building Graph_Theory (on hpcisabelle/4) ...
03:53:43Graph_Theory: theory Graph_Theory.Rtrancl_On
03:53:43Graph_Theory: theory HOL-Combinatorics.Transposition
03:53:43Graph_Theory: theory Graph_Theory.Stuff
03:53:43Graph_Theory: theory HOL-Combinatorics.Permutations
03:53:43Graph_Theory: theory Graph_Theory.Digraph
03:53:45Graph_Theory: theory HOL-Combinatorics.Orbits
03:53:46Graph_Theory: theory Graph_Theory.Arc_Walk
03:53:46Graph_Theory: theory Graph_Theory.Bidirected_Digraph
03:53:46Graph_Theory: theory Graph_Theory.Auxiliary
03:53:48Graph_Theory: theory Graph_Theory.Vertex_Walk
03:53:48Graph_Theory: theory Graph_Theory.Pair_Digraph
03:53:48Graph_Theory: theory Graph_Theory.Weighted_Graph
03:53:48Graph_Theory: theory Graph_Theory.Shortest_Path
03:53:55Graph_Theory: theory Graph_Theory.Digraph_Component
03:53:59Graph_Theory: theory Graph_Theory.Digraph_Component_Vwalk
03:53:59Graph_Theory: theory Graph_Theory.Subdivision
03:53:59Graph_Theory: theory Graph_Theory.Digraph_Isomorphism
03:54:01Graph_Theory: theory Graph_Theory.Kuratowski
03:54:01Graph_Theory: theory Graph_Theory.Euler
03:54:06Graph_Theory: theory Graph_Theory.Graph_Theory
03:54:23Preparing Graph_Theory/document ...
03:54:33Finished Graph_Theory/document (0:00:10 elapsed time)
03:54:33Preparing Graph_Theory/outline ...
03:54:39Finished Graph_Theory/outline (0:00:05 elapsed time)
03:54:39Timing Graph_Theory (8 threads, 27.497s elapsed time, 132.962s cpu time, 4.467s GC time, factor 4.84)
03:54:39Finished Graph_Theory (0:00:41 elapsed time, 0:02:38 cpu time, factor 3.85)
03:54:39Running Matrices_for_ODEs (on hpcisabelle/5) ...
03:54:42Matrices_for_ODEs: theory HOL-Library.Code_Cardinality
03:54:42Matrices_for_ODEs: theory HOL-Library.Log_Nat
03:54:42Matrices_for_ODEs: theory HOL-Library.Lattice_Algebras
03:54:42Matrices_for_ODEs: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
03:54:42Matrices_for_ODEs: theory Ordinary_Differential_Equations.Vector_Derivative_On
03:54:42Matrices_for_ODEs: theory List-Index.List_Index
03:54:42Matrices_for_ODEs: theory Ordinary_Differential_Equations.Gronwall
03:54:42Matrices_for_ODEs: theory Ordinary_Differential_Equations.Interval_Integral_HK
03:54:49Matrices_for_ODEs: theory HOL-Library.Float
03:54:52Matrices_for_ODEs: theory Affine_Arithmetic.Executable_Euclidean_Space
03:54:56Matrices_for_ODEs: theory Ordinary_Differential_Equations.ODE_Auxiliarities
03:54:57Matrices_for_ODEs: theory Ordinary_Differential_Equations.Initial_Value_Problem
03:55:00Matrices_for_ODEs: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
03:55:01Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_Preliminaries
03:55:02Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_ODEs
03:55:02Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Preliminaries
03:55:03Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Norms
03:55:04Matrices_for_ODEs: theory Matrices_for_ODEs.SQ_MTX
03:55:04Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_VC_Spartan
03:55:05Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Flows
03:55:06Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Examples
03:56:34Preparing Matrices_for_ODEs/document ...
03:56:39Finished Matrices_for_ODEs/document (0:00:04 elapsed time)
03:56:39Preparing Matrices_for_ODEs/outline ...
03:56:43Finished Matrices_for_ODEs/outline (0:00:03 elapsed time)
03:56:43Timing Matrices_for_ODEs (8 threads, 111.167s elapsed time, 331.954s cpu time, 4.058s GC time, factor 2.99)
03:56:43Finished Matrices_for_ODEs (0:01:54 elapsed time, 0:05:36 cpu time, factor 2.95)
03:56:43Running QR_Decomposition (on hpcisabelle/6) ...
03:56:45QR_Decomposition: theory Deriving.Derive_Manager
03:56:45QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary
03:56:45QR_Decomposition: theory Deriving.Generator_Aux
03:56:45QR_Decomposition: theory HOL-Library.Code_Abstract_Nat
03:56:45QR_Decomposition: theory HOL-Library.Code_Target_Int
03:56:45QR_Decomposition: theory HOL-Library.Function_Algebras
03:56:45QR_Decomposition: theory HOL-Library.IArray
03:56:46QR_Decomposition: theory HOL-Library.Code_Cardinality
03:56:46QR_Decomposition: theory HOL-Library.Z2
03:56:46QR_Decomposition: theory Cauchy.CauchysMeanTheorem
03:56:46QR_Decomposition: theory HOL-Library.Code_Target_Nat
03:56:46QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
03:56:46QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order
03:56:46QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float
03:56:46QR_Decomposition: theory HOL-Library.Code_Target_Numeral
03:56:46QR_Decomposition: theory Gauss_Jordan.Code_Set
03:56:46QR_Decomposition: theory Show.Show
03:56:46QR_Decomposition: theory Gauss_Jordan.Code_Z2
03:56:47QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR
03:56:47QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type
03:56:47QR_Decomposition: theory Sqrt_Babylonian.Log_Impl
03:56:47QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl
03:56:48QR_Decomposition: theory Show.Show_Instances
03:56:48QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian
03:56:49QR_Decomposition: theory Real_Impl.Prime_Product
03:56:49QR_Decomposition: theory Real_Impl.Real_Impl
03:56:49QR_Decomposition: theory Show.Shows_Literal
03:56:50QR_Decomposition: theory Show.Show_Real
03:56:50QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous
03:56:51QR_Decomposition: theory Real_Impl.Real_Unique_Impl
03:56:52QR_Decomposition: theory Gauss_Jordan.Code_Matrix
03:56:52QR_Decomposition: theory Gauss_Jordan.Rref
03:56:52QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces
03:56:52QR_Decomposition: theory QR_Decomposition.Generalizations2
03:56:53QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula
03:56:53QR_Decomposition: theory Gauss_Jordan.Elementary_Operations
03:56:53QR_Decomposition: theory Gauss_Jordan.Rank
03:56:54QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR
03:56:54QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan
03:56:56QR_Decomposition: theory Gauss_Jordan.Linear_Maps
03:56:57QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA
03:56:58QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
03:56:58QR_Decomposition: theory Gauss_Jordan.Determinants2
03:56:58QR_Decomposition: theory Gauss_Jordan.Inverse
03:56:58QR_Decomposition: theory Gauss_Jordan.System_Of_Equations
03:56:59QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
03:57:00QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR
03:57:01QR_Decomposition: theory QR_Decomposition.Projections
03:57:01QR_Decomposition: theory QR_Decomposition.Gram_Schmidt
03:57:01QR_Decomposition: theory QR_Decomposition.QR_Decomposition
03:57:02QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float
03:57:02QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays
03:57:03QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays
03:57:03QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float
03:57:05QR_Decomposition: theory QR_Decomposition.QR_Efficient
03:57:05QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation
03:57:05QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic
03:57:15QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic
03:58:33Preparing QR_Decomposition/document ...
03:58:38Finished QR_Decomposition/document (0:00:05 elapsed time)
03:58:38Preparing QR_Decomposition/outline ...
03:58:42Finished QR_Decomposition/outline (0:00:03 elapsed time)
03:58:42Timing QR_Decomposition (8 threads, 104.746s elapsed time, 739.854s cpu time, 26.824s GC time, factor 7.06)
03:58:42Finished QR_Decomposition (0:01:48 elapsed time, 0:12:26 cpu time, factor 6.91)
03:58:42Building Matrix (on hpcisabelle/7) ...
03:58:45Matrix: theory Matrix.Utility
03:58:45Matrix: theory HOL-Algebra.Congruence
03:58:46Matrix: theory HOL-Algebra.Order
03:58:47Matrix: theory HOL-Algebra.Lattice
03:58:49Matrix: theory HOL-Algebra.Complete_Lattice
03:58:50Matrix: theory HOL-Algebra.Group
03:58:53Matrix: theory HOL-Algebra.FiniteProduct
03:58:54Matrix: theory HOL-Algebra.Ring
03:58:58Matrix: theory Matrix.Ordered_Semiring
03:58:59Matrix: theory Matrix.Matrix_Legacy
03:59:16Preparing Matrix/document ...
03:59:19Finished Matrix/document (0:00:03 elapsed time)
03:59:19Preparing Matrix/outline ...
03:59:22Finished Matrix/outline (0:00:02 elapsed time)
03:59:22Timing Matrix (8 threads, 18.386s elapsed time, 93.146s cpu time, 2.615s GC time, factor 5.07)
03:59:22Finished Matrix (0:00:32 elapsed time, 0:02:01 cpu time, factor 3.69)
03:59:22Running IsaNet (on hpcisabelle/0) ...
03:59:24IsaNet: theory HOL-Library.Nat_Bijection
03:59:24IsaNet: theory HOL-Library.Old_Datatype
03:59:24IsaNet: theory IsaNet.Agents
03:59:24IsaNet: theory IsaNet.Event_Systems
03:59:24IsaNet: theory HOL-Library.Sublist
03:59:25IsaNet: theory IsaNet.Keys
03:59:25IsaNet: theory HOL-Library.Countable
03:59:27IsaNet: theory HOL-Library.FSet
03:59:27IsaNet: theory IsaNet.Tools
03:59:27IsaNet: theory IsaNet.Take_While
03:59:27IsaNet: theory IsaNet.Take_While_Update
03:59:28IsaNet: theory IsaNet.Network_Model
03:59:29IsaNet: theory IsaNet.Network_Assumptions
03:59:29IsaNet: theory IsaNet.Parametrized_Dataplane_0
03:59:31IsaNet: theory IsaNet.Message
03:59:34IsaNet: theory IsaNet.Abstract_XOR
03:59:34IsaNet: theory IsaNet.Parametrized_Dataplane_1
03:59:37IsaNet: theory IsaNet.Parametrized_Dataplane_2
03:59:44IsaNet: theory IsaNet.Parametrized_Dataplane_3_undirected
03:59:44IsaNet: theory IsaNet.Parametrized_Dataplane_3_directed
03:59:48IsaNet: theory IsaNet.ICING
03:59:49IsaNet: theory IsaNet.ICING_variant
03:59:49IsaNet: theory IsaNet.ICING_variant2
03:59:49IsaNet: theory IsaNet.Anapaya_SCION
03:59:49IsaNet: theory IsaNet.EPIC_L1_BA
03:59:49IsaNet: theory IsaNet.EPIC_L1_SA
03:59:49IsaNet: theory IsaNet.EPIC_L2_SA
03:59:49IsaNet: theory IsaNet.SCION
03:59:55IsaNet: theory IsaNet.SCION_variant
04:00:05IsaNet: theory IsaNet.EPIC_L1_SA_Example
04:00:10IsaNet: theory IsaNet.All_Protocols
04:01:14Preparing IsaNet/document ...
04:01:24Finished IsaNet/document (0:00:09 elapsed time)
04:01:24Preparing IsaNet/outline ...
04:01:31Finished IsaNet/outline (0:00:07 elapsed time)
04:01:32Timing IsaNet (8 threads, 108.690s elapsed time, 701.999s cpu time, 12.503s GC time, factor 6.46)
04:01:32Finished IsaNet (0:01:51 elapsed time, 0:11:47 cpu time, factor 6.38)
04:01:32Running MLSS_Decision_Proc (on hpcisabelle/1) ...
04:01:33MLSS_Decision_Proc: theory Graph_Theory.Rtrancl_On
04:01:33MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh
04:01:33MLSS_Decision_Proc: theory HOL-Combinatorics.Transposition
04:01:33MLSS_Decision_Proc: theory HOL-Library.Adhoc_Overloading
04:01:33MLSS_Decision_Proc: theory HOL-Library.Cancellation
04:01:33MLSS_Decision_Proc: theory HOL-Library.Nat_Bijection
04:01:33MLSS_Decision_Proc: theory HOL-Library.FuncSet
04:01:33MLSS_Decision_Proc: theory HOL-Library.Infinite_Set
04:01:34MLSS_Decision_Proc: theory HOL-Library.Old_Datatype
04:01:34MLSS_Decision_Proc: theory HOL-Library.Rewrite
04:01:34MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh_Nat
04:01:34MLSS_Decision_Proc: theory HOL-Library.Sublist
04:01:34MLSS_Decision_Proc: theory HOL-Library.Liminf_Limsup
04:01:34MLSS_Decision_Proc: theory List-Index.List_Index
04:01:34MLSS_Decision_Proc: theory HereditarilyFinite.HF
04:01:35MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Logic
04:01:35MLSS_Decision_Proc: theory HOL-Library.Disjoint_Sets
04:01:35MLSS_Decision_Proc: theory HOL-Library.Multiset
04:01:35MLSS_Decision_Proc: theory HOL-Library.Countable
04:01:35MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Suc_Theory
04:01:36MLSS_Decision_Proc: theory HereditarilyFinite.Ordinal
04:01:37MLSS_Decision_Proc: theory HereditarilyFinite.Finitary
04:01:37MLSS_Decision_Proc: theory HereditarilyFinite.Rank
04:01:37MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Semantics
04:01:37MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_HF_Extras
04:01:37MLSS_Decision_Proc: theory HOL-Library.Countable_Set
04:01:38MLSS_Decision_Proc: theory HOL-Library.Countable_Complete_Lattices
04:01:41MLSS_Decision_Proc: theory HOL-Library.Order_Continuity
04:01:41MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Defs
04:01:41MLSS_Decision_Proc: theory HOL-Combinatorics.Permutations
04:01:41MLSS_Decision_Proc: theory HOL-Library.Extended_Nat
04:01:42MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Calculus
04:01:43MLSS_Decision_Proc: theory HOL-Library.Extended_Real
04:01:43MLSS_Decision_Proc: theory HOL-Combinatorics.Orbits
04:01:43MLSS_Decision_Proc: theory Graph_Theory.Auxiliary
04:01:44MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing
04:01:45MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Urelems
04:01:47MLSS_Decision_Proc: theory Graph_Theory.Stuff
04:01:48MLSS_Decision_Proc: theory Graph_Theory.Digraph
04:01:50MLSS_Decision_Proc: theory Graph_Theory.Arc_Walk
04:01:50MLSS_Decision_Proc: theory Graph_Theory.Bidirected_Digraph
04:01:52MLSS_Decision_Proc: theory Graph_Theory.Vertex_Walk
04:01:52MLSS_Decision_Proc: theory Graph_Theory.Pair_Digraph
04:01:52MLSS_Decision_Proc: theory Graph_Theory.Weighted_Graph
04:01:52MLSS_Decision_Proc: theory Graph_Theory.Shortest_Path
04:01:59MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component
04:02:04MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component_Vwalk
04:02:04MLSS_Decision_Proc: theory Graph_Theory.Digraph_Isomorphism
04:02:04MLSS_Decision_Proc: theory Graph_Theory.Subdivision
04:02:06MLSS_Decision_Proc: theory Graph_Theory.Kuratowski
04:02:06MLSS_Decision_Proc: theory Graph_Theory.Euler
04:02:11MLSS_Decision_Proc: theory Graph_Theory.Graph_Theory
04:02:12MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Realisation
04:02:15MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc
04:02:20MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_Code
04:02:31MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_All
04:03:20Preparing MLSS_Decision_Proc/document ...
04:03:22Finished MLSS_Decision_Proc/document (0:00:02 elapsed time)
04:03:22Preparing MLSS_Decision_Proc/outline ...
04:03:25Finished MLSS_Decision_Proc/outline (0:00:02 elapsed time)
04:03:25Timing MLSS_Decision_Proc (8 threads, 103.264s elapsed time, 573.922s cpu time, 16.722s GC time, factor 5.56)
04:03:25Finished MLSS_Decision_Proc (0:01:45 elapsed time, 0:09:41 cpu time, factor 5.49)
04:03:25Running Gabow_SCC (on hpcisabelle/2) ...
04:03:28Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton
04:03:28Gabow_SCC: theory Gabow_SCC.Find_Path
04:03:28Gabow_SCC: theory Gabow_SCC.Find_Path_Impl
04:03:33Gabow_SCC: theory Gabow_SCC.Gabow_SCC
04:03:33Gabow_SCC: theory Gabow_SCC.Gabow_GBG
04:03:34Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton_Code
04:04:03Gabow_SCC: theory Gabow_SCC.Gabow_GBG_Code
04:04:03Gabow_SCC: theory Gabow_SCC.Gabow_SCC_Code
04:05:12Gabow_SCC: theory Gabow_SCC.All_Of_Gabow_SCC
04:05:14Preparing Gabow_SCC/document ...
04:05:22Finished Gabow_SCC/document (0:00:07 elapsed time)
04:05:22Preparing Gabow_SCC/outline ...
04:05:27Finished Gabow_SCC/outline (0:00:05 elapsed time)
04:05:27Timing Gabow_SCC (8 threads, 105.425s elapsed time, 300.212s cpu time, 6.723s GC time, factor 2.85)
04:05:28Finished Gabow_SCC (0:01:48 elapsed time, 0:05:04 cpu time, factor 2.81)
04:05:28Running Codegen (on hpcisabelle/3) ...
04:05:29Codegen: theory HOL-Library.AList
04:05:29Codegen: theory HOL-Library.IArray
04:05:29Codegen: theory HOL-Library.Confluence
04:05:29Codegen: theory HOL-Library.RBT_Impl
04:05:29Codegen: theory HOL-Library.Confluent_Quotient
04:05:29Codegen: theory HOL-Library.Dlist
04:05:31Codegen: theory HOL-Library.Mapping
04:06:30Codegen: theory HOL-Library.RBT
04:06:31Codegen: theory Codegen.Setup
04:07:03Codegen: theory HOL-Library.Adhoc_Overloading
04:07:03Codegen: theory Codegen.Adaptation
04:07:03Codegen: theory HOL-Library.Code_Target_Int
04:07:03Codegen: theory Codegen.Further
04:07:03Codegen: theory Codegen.Evaluation
04:07:03Codegen: theory Codegen.Inductive_Predicate
04:07:03Codegen: theory Codegen.Introduction
04:07:03Codegen: theory Codegen.Refinement
04:07:03Codegen: theory HOL-Library.Monad_Syntax
04:07:03Codegen: theory Codegen.Computations
04:07:03Codegen: theory Codegen.Partial_Functions
04:07:04Codegen: theory Codegen.Foundations
04:07:12Preparing Codegen/codegen ...
04:07:17Finished Codegen/codegen (0:00:05 elapsed time)
04:07:17Timing Codegen (8 threads, 100.795s elapsed time, 436.218s cpu time, 7.723s GC time, factor 4.33)
04:07:17Finished Codegen (0:01:43 elapsed time, 0:07:21 cpu time, factor 4.28)
04:07:17Building HOL-Imperative_HOL (on hpcisabelle/4) ...
04:07:19HOL-Imperative_HOL: theory HOL-Library.Nat_Bijection
04:07:19HOL-Imperative_HOL: theory HOL-Library.Code_Abstract_Nat
04:07:19HOL-Imperative_HOL: theory HOL-Library.Cancellation
04:07:19HOL-Imperative_HOL: theory HOL-Library.Adhoc_Overloading
04:07:19HOL-Imperative_HOL: theory HOL-Library.Code_Target_Int
04:07:19HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List
04:07:19HOL-Imperative_HOL: theory HOL-Library.LaTeXsugar
04:07:19HOL-Imperative_HOL: theory HOL-Library.Old_Datatype
04:07:19HOL-Imperative_HOL: theory HOL-Library.Code_Target_Nat
04:07:19HOL-Imperative_HOL: theory HOL-Library.RBT_Impl
04:07:19HOL-Imperative_HOL: theory HOL-Library.Monad_Syntax
04:07:19HOL-Imperative_HOL: theory HOL-Library.Code_Target_Numeral
04:07:20HOL-Imperative_HOL: theory HOL-Library.Countable
04:07:20HOL-Imperative_HOL: theory HOL-Library.Multiset
04:07:22HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap
04:07:24HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
04:07:26HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array
04:07:27HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref
04:07:27HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist
04:07:27HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
04:07:28HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists
04:07:28HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview
04:07:28HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray
04:07:28HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort
04:07:28HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse
04:08:23HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker
04:08:34HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex
04:09:19Preparing HOL-Imperative_HOL/document ...
04:09:22Finished HOL-Imperative_HOL/document (0:00:03 elapsed time)
04:09:22Preparing HOL-Imperative_HOL/outline ...
04:09:26Finished HOL-Imperative_HOL/outline (0:00:03 elapsed time)
04:09:26Timing HOL-Imperative_HOL (8 threads, 101.012s elapsed time, 547.126s cpu time, 11.024s GC time, factor 5.42)
04:09:26Finished HOL-Imperative_HOL (0:02:00 elapsed time, 0:09:52 cpu time, factor 4.90)
04:09:26Running HOL-Quickcheck_Examples (on hpcisabelle/5) ...
04:09:27HOL-Quickcheck_Examples: theory HOL-Library.Confluence
04:09:27HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness
04:09:27HOL-Quickcheck_Examples: theory HOL-Library.Cancellation
04:09:27HOL-Quickcheck_Examples: theory HOL-Library.AList
04:09:27HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces
04:09:27HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting
04:09:27HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples
04:09:27HOL-Quickcheck_Examples: theory HOL-Library.Confluent_Quotient
04:09:28HOL-Quickcheck_Examples: theory HOL-Library.Dlist
04:09:28HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example
04:09:28HOL-Quickcheck_Examples: theory HOL-Library.Multiset
04:09:29HOL-Quickcheck_Examples: theory HOL-Library.DAList
04:09:35HOL-Quickcheck_Examples: theory HOL-Library.DAList_Multiset
04:09:36HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples
04:09:58HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples
04:09:58HOL-Quickcheck_Examples: theory HOL-Library.Predicate_Compile_Alternative_Defs
04:09:59HOL-Quickcheck_Examples: theory HOL-Library.Predicate_Compile_Quickcheck
04:09:59HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example
04:11:11Timing HOL-Quickcheck_Examples (8 threads, 102.042s elapsed time, 252.733s cpu time, 6.600s GC time, factor 2.48)
04:11:11Finished HOL-Quickcheck_Examples (0:01:44 elapsed time, 0:04:16 cpu time, factor 2.46)
04:11:11Running Balog_Szemeredi_Gowers (on hpcisabelle/6) ...
04:11:14Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Dense_Linear_Order
04:11:14Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Set_Theory
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Code_Abstract_Nat
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Int
04:11:14Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Miscellaneous_Lemmas
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Lattice_Algebras
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Log_Nat
04:11:14Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic_Misc
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Nat
04:11:14Balog_Szemeredi_Gowers: theory Girth_Chromatic.Ugraphs
04:11:14Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
04:11:14Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Basics
04:11:14Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Numeral
04:11:14Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Group_Theory
04:11:17Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Undirected_Graph_Walks
04:11:18Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Bipartite_Graphs
04:11:18Balog_Szemeredi_Gowers: theory Undirected_Graph_Theory.Connectivity
04:11:20Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Graph_Theory_Preliminaries
04:11:21Balog_Szemeredi_Gowers: theory HOL-Library.Interval
04:11:21Balog_Szemeredi_Gowers: theory HOL-Library.Float
04:11:24Balog_Szemeredi_Gowers: theory HOL-Library.Code_Target_Numeral_Float
04:11:24Balog_Szemeredi_Gowers: theory HOL-Library.Interval_Float
04:11:26Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation_Bounds
04:11:32Balog_Szemeredi_Gowers: theory HOL-Decision_Procs.Approximation
04:11:34Balog_Szemeredi_Gowers: theory Jacobson_Basic_Algebra.Ring_Theory
04:12:11Balog_Szemeredi_Gowers: theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
04:12:12Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Combinatorics_Preliminaries
04:12:12Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Sumset_Triangle_Inequality
04:12:13Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Additive_Energy_Lower_Bounds
04:12:22Balog_Szemeredi_Gowers: theory Girth_Chromatic.Girth_Chromatic
04:12:25Balog_Szemeredi_Gowers: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
04:12:27Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Prob_Space_Lemmas
04:12:27Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof
04:12:29Balog_Szemeredi_Gowers: theory Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary
04:12:54Preparing Balog_Szemeredi_Gowers/document ...
04:13:00Finished Balog_Szemeredi_Gowers/document (0:00:06 elapsed time)
04:13:00Preparing Balog_Szemeredi_Gowers/outline ...
04:13:03Finished Balog_Szemeredi_Gowers/outline (0:00:03 elapsed time)
04:13:03Timing Balog_Szemeredi_Gowers (8 threads, 97.657s elapsed time, 602.082s cpu time, 23.064s GC time, factor 6.17)
04:13:03Finished Balog_Szemeredi_Gowers (0:01:41 elapsed time, 0:10:08 cpu time, factor 6.02)
04:13:04Running Extended_Finite_State_Machine_Inference (on hpcisabelle/7) ...
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Group_By
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Code_Target_List
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Code_Target_FSet
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Code_Target_Set
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Subsumption
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Inference
04:13:06Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Drinks_Subsumption
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Increment_Reset
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Distinguishing_Guards
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.EFSM_Dot
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Least_Upper_Bound
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Same_Register
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Store_Reuse
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.SelectionStrategies
04:13:12Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Weak_Subsumption
04:13:13Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.PTA_Generalisation
04:13:14Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Store_Reuse_Subsumption
04:13:14Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.efsm2sal
04:13:50Extended_Finite_State_Machine_Inference: theory Extended_Finite_State_Machine_Inference.Code_Generation
04:14:46Preparing Extended_Finite_State_Machine_Inference/document ...
04:14:53Finished Extended_Finite_State_Machine_Inference/document (0:00:06 elapsed time)
04:14:53Preparing Extended_Finite_State_Machine_Inference/outline ...
04:14:58Finished Extended_Finite_State_Machine_Inference/outline (0:00:05 elapsed time)
04:14:58Timing Extended_Finite_State_Machine_Inference (8 threads, 99.201s elapsed time, 275.147s cpu time, 4.499s GC time, factor 2.77)
04:14:58Finished Extended_Finite_State_Machine_Inference (0:01:42 elapsed time, 0:04:40 cpu time, factor 2.74)
04:14:58Running Isabelle_C (on hpcisabelle/0) ...
04:15:00Isabelle_C: theory HOL-ex.Cartouche_Examples
04:15:00Isabelle_C: theory Isabelle_C.C_Ast
04:15:00Isabelle_C: theory Isabelle_C.C_Lexer_Language
04:15:02Isabelle_C: theory Isabelle_C.C_Lexer_Annotation
04:15:47Isabelle_C: theory Isabelle_C.C_Environment
04:15:47Isabelle_C: theory Isabelle_C.C_Parser_Language
04:15:47Isabelle_C: theory Isabelle_C.C_Parser_Annotation
04:15:55Isabelle_C: theory Isabelle_C.C_Eval
04:15:56Isabelle_C: theory Isabelle_C.C_Command
04:15:56Isabelle_C: theory Isabelle_C.C_Document
04:15:56Isabelle_C: theory Isabelle_C.C_Main
04:15:56Isabelle_C: theory Isabelle_C.C0
04:15:56Isabelle_C: theory Isabelle_C.C1
04:15:56Isabelle_C: theory Isabelle_C.C2
04:15:56Isabelle_C: theory Isabelle_C.C_paper
04:15:58Isabelle_C: theory Isar_Ref.Base
04:15:58Isabelle_C: theory Isabelle_C.README
04:15:59Isabelle_C: theory Isabelle_C.C_Appendices
04:16:05Preparing Isabelle_C/document ...
04:16:27Finished Isabelle_C/document (0:00:21 elapsed time)
04:16:27Preparing Isabelle_C/outline ...
04:16:49Finished Isabelle_C/outline (0:00:21 elapsed time)
04:16:49Timing Isabelle_C (8 threads, 61.226s elapsed time, 74.277s cpu time, 16.338s GC time, factor 1.21)
04:16:49Finished Isabelle_C (0:01:03 elapsed time, 0:01:17 cpu time, factor 1.23)
04:16:49Running Deep_Learning (on hpcisabelle/1) ...
04:16:52Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
04:16:52Deep_Learning: theory Deep_Learning.Tensor
04:16:52Deep_Learning: theory HOL-Computational_Algebra.Fraction_Field
04:16:52Deep_Learning: theory HOL-Library.Fun_Lexorder
04:16:52Deep_Learning: theory HOL-Algebra.Congruence
04:16:52Deep_Learning: theory Jordan_Normal_Form.Missing_Misc
04:16:52Deep_Learning: theory HOL-Library.Groups_Big_Fun
04:16:52Deep_Learning: theory HOL-Library.More_List
04:16:52Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted
04:16:52Deep_Learning: theory Jordan_Normal_Form.Conjugate
04:16:52Deep_Learning: theory Deep_Learning.Lebesgue_Functional
04:16:52Deep_Learning: theory HOL-Computational_Algebra.Polynomial
04:16:53Deep_Learning: theory HOL-Library.Poly_Mapping
04:16:53Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List
04:16:53Deep_Learning: theory Deep_Learning.Tensor_Subtensor
04:16:53Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist
04:16:53Deep_Learning: theory Deep_Learning.Tensor_Plus
04:16:53Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
04:16:53Deep_Learning: theory Polynomial_Interpolation.Ring_Hom
04:16:53Deep_Learning: theory HOL-Algebra.Order
04:16:53Deep_Learning: theory Deep_Learning.Tensor_Product
04:16:54Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
04:16:54Deep_Learning: theory Deep_Learning.Tensor_Rank
04:16:54Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction
04:16:54Deep_Learning: theory VectorSpace.FunctionLemmas
04:16:55Deep_Learning: theory Polynomials.MPoly_Type
04:16:55Deep_Learning: theory HOL-Algebra.Lattice
04:16:56Deep_Learning: theory Polynomials.More_MPoly_Type
04:16:57Deep_Learning: theory HOL-Algebra.Complete_Lattice
04:16:58Deep_Learning: theory HOL-Algebra.Group
04:17:00Deep_Learning: theory HOL-Algebra.Coset
04:17:00Deep_Learning: theory HOL-Algebra.FiniteProduct
04:17:01Deep_Learning: theory HOL-Algebra.Ring
04:17:05Deep_Learning: theory Polynomials.MPoly_Type_Univariate
04:17:06Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial
04:17:06Deep_Learning: theory HOL-Algebra.Module
04:17:06Deep_Learning: theory Jordan_Normal_Form.Missing_Ring
04:17:06Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
04:17:09Deep_Learning: theory VectorSpace.RingModuleFacts
04:17:10Deep_Learning: theory VectorSpace.MonoidSums
04:17:10Deep_Learning: theory VectorSpace.LinearCombinations
04:17:12Deep_Learning: theory Jordan_Normal_Form.Matrix
04:17:17Deep_Learning: theory VectorSpace.SumSpaces
04:17:18Deep_Learning: theory VectorSpace.VectorSpace
04:17:18Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
04:17:18Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
04:17:18Deep_Learning: theory Deep_Learning.Tensor_Matricization
04:17:19Deep_Learning: theory Deep_Learning.DL_Network
04:17:19Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
04:17:19Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
04:17:21Deep_Learning: theory Jordan_Normal_Form.Column_Operations
04:17:22Deep_Learning: theory Jordan_Normal_Form.Determinant
04:17:23Deep_Learning: theory Deep_Learning.DL_Shallow_Model
04:17:24Deep_Learning: theory Deep_Learning.DL_Deep_Model
04:17:25Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
04:17:28Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
04:17:29Deep_Learning: theory Jordan_Normal_Form.VS_Connect
04:17:43Deep_Learning: theory Jordan_Normal_Form.DL_Rank
04:17:51Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
04:17:51Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
04:17:54Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
04:18:34Preparing Deep_Learning/document ...
04:18:42Finished Deep_Learning/document (0:00:07 elapsed time)
04:18:42Preparing Deep_Learning/outline ...
04:18:46Finished Deep_Learning/outline (0:00:03 elapsed time)
04:18:46Timing Deep_Learning (8 threads, 97.956s elapsed time, 723.904s cpu time, 36.163s GC time, factor 7.39)
04:18:46Finished Deep_Learning (0:01:41 elapsed time, 0:12:12 cpu time, factor 7.19)
04:18:46Building HOL-Auth (on hpcisabelle/2) ...
04:18:47HOL-Auth: theory HOL-Auth.README
04:18:47HOL-Auth: theory HOL-Auth.Message
04:18:47HOL-Auth: theory HOL-Library.Case_Converter
04:18:47HOL-Auth: theory HOL-Library.Nat_Bijection
04:18:48HOL-Auth: theory HOL-Library.Simps_Case_Conv
04:18:50HOL-Auth: theory HOL-Auth.EventSC
04:18:50HOL-Auth: theory HOL-Auth.All_Symmetric
04:18:50HOL-Auth: theory HOL-Auth.Event
04:18:52HOL-Auth: theory HOL-Auth.Public
04:18:52HOL-Auth: theory HOL-Auth.CertifiedEmail
04:18:52HOL-Auth: theory HOL-Auth.KerberosIV
04:18:52HOL-Auth: theory HOL-Auth.KerberosIV_Gets
04:18:52HOL-Auth: theory HOL-Auth.KerberosV
04:18:52HOL-Auth: theory HOL-Auth.Kerberos_BAN
04:18:52HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets
04:18:53HOL-Auth: theory HOL-Auth.NS_Public
04:18:53HOL-Auth: theory HOL-Auth.NS_Public_Bad
04:18:53HOL-Auth: theory HOL-Auth.NS_Shared
04:18:53HOL-Auth: theory HOL-Auth.OtwayRees
04:18:54HOL-Auth: theory HOL-Auth.OtwayReesBella
04:18:54HOL-Auth: theory HOL-Auth.OtwayRees_AN
04:18:54HOL-Auth: theory HOL-Auth.OtwayRees_Bad
04:18:55HOL-Auth: theory HOL-Auth.Recur
04:18:55HOL-Auth: theory HOL-Auth.WooLam
04:18:55HOL-Auth: theory HOL-Auth.Yahalom
04:18:55HOL-Auth: theory HOL-Auth.Yahalom2
04:18:55HOL-Auth: theory HOL-Auth.Yahalom_Bad
04:18:55HOL-Auth: theory HOL-Auth.ZhouGollmann
04:18:55HOL-Auth: theory HOL-Auth.Smartcard
04:18:55HOL-Auth: theory HOL-Auth.TLS
04:18:56HOL-Auth: theory HOL-Auth.ShoupRubin
04:18:56HOL-Auth: theory HOL-Auth.ShoupRubinBella
04:18:56HOL-Auth: theory HOL-Auth.Auth_Shared
04:18:57HOL-Auth: theory HOL-Auth.Auth_Public
04:18:57HOL-Auth: theory HOL-Auth.Auth_Smartcard
04:19:37HOL-Auth: theory HOL-Auth.README_Guard
04:19:37HOL-Auth: theory HOL-Auth.Extensions
04:19:37HOL-Auth: theory HOL-Auth.Shared
04:19:38HOL-Auth: theory HOL-Auth.Analz
04:19:38HOL-Auth: theory HOL-Auth.List_Msg
04:19:38HOL-Auth: theory HOL-Auth.Guard
04:19:38HOL-Auth: theory HOL-Auth.GuardK
04:19:39HOL-Auth: theory HOL-Auth.Guard_Public
04:19:39HOL-Auth: theory HOL-Auth.Guard_Shared
04:19:39HOL-Auth: theory HOL-Auth.Guard_NS_Public
04:19:39HOL-Auth: theory HOL-Auth.Proto
04:19:40HOL-Auth: theory HOL-Auth.Guard_OtwayRees
04:19:40HOL-Auth: theory HOL-Auth.Guard_Yahalom
04:19:40HOL-Auth: theory HOL-Auth.P2
04:19:40HOL-Auth: theory HOL-Auth.P1
04:19:40HOL-Auth: theory HOL-Auth.Auth_Guard_Shared
04:19:46HOL-Auth: theory HOL-Auth.Auth_Guard_Public
04:20:07Preparing HOL-Auth/document ...
04:20:17Finished HOL-Auth/document (0:00:10 elapsed time)
04:20:17Preparing HOL-Auth/outline ...
04:20:26Finished HOL-Auth/outline (0:00:08 elapsed time)
04:20:26Timing HOL-Auth (8 threads, 70.797s elapsed time, 454.440s cpu time, 7.522s GC time, factor 6.42)
04:20:26Finished HOL-Auth (0:01:19 elapsed time, 0:07:51 cpu time, factor 5.89)
04:20:26Running Regression_Test_Selection (on hpcisabelle/3) ...
04:20:28Regression_Test_Selection: theory Jinja.Semilat
04:20:28Regression_Test_Selection: theory JinjaDCI.Auxiliary
04:20:28Regression_Test_Selection: theory Regression_Test_Selection.RTS_safe
04:20:28Regression_Test_Selection: theory Regression_Test_Selection.Semantics
04:20:28Regression_Test_Selection: theory Regression_Test_Selection.CollectionSemantics
04:20:28Regression_Test_Selection: theory JinjaDCI.Type
04:20:29Regression_Test_Selection: theory Regression_Test_Selection.CollectionBasedRTS
04:20:29Regression_Test_Selection: theory Jinja.Err
04:20:30Regression_Test_Selection: theory JinjaDCI.Decl
04:20:30Regression_Test_Selection: theory JinjaDCI.TypeRel
04:20:30Regression_Test_Selection: theory Regression_Test_Selection.ClassesChanged
04:20:30Regression_Test_Selection: theory Jinja.Listn
04:20:30Regression_Test_Selection: theory Jinja.Opt
04:20:30Regression_Test_Selection: theory Jinja.Product
04:20:31Regression_Test_Selection: theory Jinja.Semilattices
04:20:31Regression_Test_Selection: theory JinjaDCI.Value
04:20:31Regression_Test_Selection: theory Regression_Test_Selection.Subcls
04:20:32Regression_Test_Selection: theory JinjaDCI.Objects
04:20:33Regression_Test_Selection: theory JinjaDCI.Exceptions
04:20:33Regression_Test_Selection: theory JinjaDCI.JVMState
04:20:33Regression_Test_Selection: theory JinjaDCI.Conform
04:20:33Regression_Test_Selection: theory JinjaDCI.SystemClasses
04:20:33Regression_Test_Selection: theory Regression_Test_Selection.ClassesAbove
04:20:33Regression_Test_Selection: theory JinjaDCI.WellForm
04:20:34Regression_Test_Selection: theory JinjaDCI.SemiType
04:20:34Regression_Test_Selection: theory JinjaDCI.JVM_SemiType
04:20:35Regression_Test_Selection: theory JinjaDCI.JVMInstructions
04:20:38Regression_Test_Selection: theory JinjaDCI.JVMExceptions
04:20:39Regression_Test_Selection: theory JinjaDCI.JVMExecInstr
04:20:39Regression_Test_Selection: theory JinjaDCI.Effect
04:20:41Regression_Test_Selection: theory JinjaDCI.JVMExec
04:20:44Regression_Test_Selection: theory Regression_Test_Selection.JVMExecStepInductive
04:20:44Regression_Test_Selection: theory Regression_Test_Selection.JVMSemantics
04:20:45Regression_Test_Selection: theory Regression_Test_Selection.JVMCollectionSemantics
04:20:55Regression_Test_Selection: theory JinjaDCI.BVSpec
04:20:55Regression_Test_Selection: theory JinjaDCI.BVConform
04:20:59Regression_Test_Selection: theory JinjaDCI.ClassAdd
04:21:00Regression_Test_Selection: theory JinjaDCI.StartProg
04:21:00Regression_Test_Selection: theory JinjaDCI.BVSpecTypeSafe
04:21:04Regression_Test_Selection: theory Regression_Test_Selection.JVMCollectionBasedRTS
04:21:10Regression_Test_Selection: theory Regression_Test_Selection.RTS
04:22:15Preparing Regression_Test_Selection/document ...
04:22:25Finished Regression_Test_Selection/document (0:00:10 elapsed time)
04:22:25Preparing Regression_Test_Selection/outline ...
04:22:31Finished Regression_Test_Selection/outline (0:00:05 elapsed time)
04:22:31Timing Regression_Test_Selection (8 threads, 104.178s elapsed time, 706.546s cpu time, 8.318s GC time, factor 6.78)
04:22:31Finished Regression_Test_Selection (0:01:47 elapsed time, 0:11:52 cpu time, factor 6.65)
04:22:31Running CVP_Hardness (on hpcisabelle/4) ...
04:22:35CVP_Hardness: theory CVP_Hardness.Reduction
04:22:35CVP_Hardness: theory CVP_Hardness.Digits_int
04:22:35CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
04:22:35CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
04:22:35CVP_Hardness: theory CVP_Hardness.Partition
04:22:35CVP_Hardness: theory CVP_Hardness.Subset_Sum
04:22:38CVP_Hardness: theory Algebraic_Numbers.Resultant
04:22:39CVP_Hardness: theory CVP_Hardness.Lattice_int
04:22:40CVP_Hardness: theory CVP_Hardness.CVP_p
04:22:40CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
04:22:55CVP_Hardness: theory LLL_Basis_Reduction.Norms
04:23:30CVP_Hardness: theory CVP_Hardness.infnorm
04:23:30CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
04:23:30CVP_Hardness: theory CVP_Hardness.CVP_vec
04:23:32CVP_Hardness: theory CVP_Hardness.BHLE
04:23:33CVP_Hardness: theory CVP_Hardness.SVP_vec
04:24:05Preparing CVP_Hardness/document ...
04:24:11Finished CVP_Hardness/document (0:00:06 elapsed time)
04:24:11Preparing CVP_Hardness/outline ...
04:24:14Finished CVP_Hardness/outline (0:00:03 elapsed time)
04:24:14Timing CVP_Hardness (8 threads, 88.651s elapsed time, 439.847s cpu time, 6.789s GC time, factor 4.96)
04:24:14Finished CVP_Hardness (0:01:32 elapsed time, 0:07:26 cpu time, factor 4.81)
04:24:15Running Rep_Fin_Groups (on hpcisabelle/5) ...
04:24:17Rep_Fin_Groups: theory Rep_Fin_Groups.Rep_Fin_Groups
04:25:55Preparing Rep_Fin_Groups/document ...
04:26:06Finished Rep_Fin_Groups/document (0:00:11 elapsed time)
04:26:06Preparing Rep_Fin_Groups/outline ...
04:26:12Finished Rep_Fin_Groups/outline (0:00:06 elapsed time)
04:26:12Timing Rep_Fin_Groups (8 threads, 97.122s elapsed time, 263.325s cpu time, 3.970s GC time, factor 2.71)
04:26:12Finished Rep_Fin_Groups (0:01:39 elapsed time, 0:04:27 cpu time, factor 2.67)
04:26:12Running Dirichlet_L (on hpcisabelle/6) ...
04:26:15Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
04:26:15Dirichlet_L: theory HOL-Library.Lattice_Algebras
04:26:15Dirichlet_L: theory HOL-Library.Log_Nat
04:26:15Dirichlet_L: theory Lehmer.Lehmer
04:26:16Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
04:26:23Dirichlet_L: theory HOL-Library.Interval
04:26:23Dirichlet_L: theory HOL-Library.Float
04:26:26Dirichlet_L: theory HOL-Library.Interval_Float
04:26:27Build timed out (after 300 minutes). Marking the build as failed.
04:26:28Build was aborted
04:26:28Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
04:30:52Started calculate disk usage of build
04:30:52Finished Calculation of disk usage of build in 0 seconds
04:30:52Started calculate disk usage of workspace
04:30:53Finished Calculation of disk usage of workspace in 1 second
04:30:54No emails were triggered.
04:30:54Finished: FAILURE
![[Jenkins]](/jenkins/static/0ab21b84/images/svgs/logo.svg){kind=logo}
