Skip to content
Failed

Console Output

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