Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix
20:14:09Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query
20:14:09Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm
20:15:03Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs
20:15:13Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs
20:17:56Preparing Quantifier_Elimination_Hybrid/document ...
20:18:14Finished Quantifier_Elimination_Hybrid/document (0:00:18 elapsed time)
20:18:14Preparing Quantifier_Elimination_Hybrid/outline ...
20:18:20Finished Quantifier_Elimination_Hybrid/outline (0:00:06 elapsed time)
20:18:20Timing Quantifier_Elimination_Hybrid (8 threads, 342.314s elapsed time, 1861.728s cpu time, 75.122s GC time, factor 5.44)
20:18:20Finished Quantifier_Elimination_Hybrid (0:05:47 elapsed time, 0:31:16 cpu time, factor 5.39)
20:18:21Building Sepref_Basic (on hpcisabelle/6) ...
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.User_Smashing
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.PO_Normalizer
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.Pf_Add
20:18:23Sepref_Basic: theory List-Index.List_Index
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.Concl_Pres_Clarification
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.Named_Theorems_Rev
20:18:23Sepref_Basic: theory HOL-Library.Rewrite
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.Structured_Apply
20:18:23Sepref_Basic: theory Separation_Logic_Imperative_HOL.Default_Insts
20:18:23Sepref_Basic: theory Refine_Imperative_HOL.Pf_Mono_Prover
20:18:24Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Id_Op
20:18:24Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Misc
20:18:26Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Basic
20:18:26Sepref_Basic: theory Refine_Imperative_HOL.Term_Synth
20:18:27Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Constraints
20:18:27Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Monadify
20:18:28Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Frame
20:18:28Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Rules
20:18:33Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Definition
20:18:33Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
20:18:34Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Translate
20:18:35Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Intf_Util
20:18:38Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Tool
20:18:39Sepref_Basic: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
20:18:42Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Foreach
20:18:44Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Improper
20:18:44Sepref_Basic: theory Refine_Imperative_HOL.Sepref
20:19:00Timing Sepref_Basic (8 threads, 22.257s elapsed time, 56.108s cpu time, 1.418s GC time, factor 2.52)
20:19:00Finished Sepref_Basic (0:00:38 elapsed time, 0:01:26 cpu time, factor 2.25)
20:19:00Running JinjaDCI (on hpcisabelle/7) ...
20:19:02JinjaDCI: theory Jinja.Semilat
20:19:02JinjaDCI: theory JinjaDCI.Auxiliary
20:19:02JinjaDCI: theory List-Index.List_Index
20:19:03JinjaDCI: theory JinjaDCI.Type
20:19:03JinjaDCI: theory Jinja.Err
20:19:03JinjaDCI: theory JinjaDCI.Hidden
20:19:04JinjaDCI: theory JinjaDCI.Decl
20:19:04JinjaDCI: theory Jinja.Listn
20:19:04JinjaDCI: theory Jinja.Opt
20:19:04JinjaDCI: theory Jinja.Product
20:19:05JinjaDCI: theory JinjaDCI.TypeRel
20:19:05JinjaDCI: theory Jinja.Semilattices
20:19:06JinjaDCI: theory JinjaDCI.Value
20:19:06JinjaDCI: theory Jinja.Typing_Framework_1
20:19:06JinjaDCI: theory Jinja.SemilatAlg
20:19:06JinjaDCI: theory Jinja.Typing_Framework_2
20:19:06JinjaDCI: theory Jinja.Kildall_1
20:19:06JinjaDCI: theory Jinja.Kildall_2
20:19:06JinjaDCI: theory Jinja.LBVSpec
20:19:06JinjaDCI: theory Jinja.Typing_Framework_err
20:19:06JinjaDCI: theory JinjaDCI.Objects
20:19:07JinjaDCI: theory Jinja.LBVComplete
20:19:07JinjaDCI: theory Jinja.LBVCorrect
20:19:07JinjaDCI: theory Jinja.Abstract_BV
20:19:07JinjaDCI: theory JinjaDCI.Exceptions
20:19:07JinjaDCI: theory JinjaDCI.JVMState
20:19:08JinjaDCI: theory JinjaDCI.Conform
20:19:08JinjaDCI: theory JinjaDCI.Expr
20:19:08JinjaDCI: theory JinjaDCI.State
20:19:08JinjaDCI: theory JinjaDCI.SystemClasses
20:19:08JinjaDCI: theory JinjaDCI.WellForm
20:19:09JinjaDCI: theory JinjaDCI.PCompiler
20:19:09JinjaDCI: theory JinjaDCI.SemiType
20:19:09JinjaDCI: theory JinjaDCI.JVM_SemiType
20:19:09JinjaDCI: theory JinjaDCI.JVMInstructions
20:19:12JinjaDCI: theory JinjaDCI.JVMExceptions
20:19:14JinjaDCI: theory JinjaDCI.JVMExecInstr
20:19:14JinjaDCI: theory JinjaDCI.Effect
20:19:15JinjaDCI: theory JinjaDCI.JVMExec
20:19:19JinjaDCI: theory JinjaDCI.JVMDefensive
20:19:26JinjaDCI: theory JinjaDCI.WellType
20:19:26JinjaDCI: theory JinjaDCI.WWellForm
20:19:26JinjaDCI: theory JinjaDCI.BigStep
20:19:27JinjaDCI: theory JinjaDCI.SmallStep
20:19:28JinjaDCI: theory JinjaDCI.Annotate
20:19:28JinjaDCI: theory JinjaDCI.WellTypeRT
20:19:29JinjaDCI: theory JinjaDCI.BVSpec
20:19:29JinjaDCI: theory JinjaDCI.BVConform
20:19:31JinjaDCI: theory JinjaDCI.EffectMono
20:19:31JinjaDCI: theory JinjaDCI.TF_JVM
20:19:32JinjaDCI: theory JinjaDCI.BVExec
20:19:32JinjaDCI: theory JinjaDCI.LBVJVM
20:19:34JinjaDCI: theory JinjaDCI.ClassAdd
20:19:34JinjaDCI: theory JinjaDCI.StartProg
20:19:35JinjaDCI: theory JinjaDCI.BVSpecTypeSafe
20:19:36JinjaDCI: theory JinjaDCI.BVNoTypeError
20:19:42JinjaDCI: theory JinjaDCI.DefAss
20:19:42JinjaDCI: theory JinjaDCI.J1
20:19:42JinjaDCI: theory JinjaDCI.JWellForm
20:19:51JinjaDCI: theory JinjaDCI.EConform
20:19:55JinjaDCI: theory JinjaDCI.Compiler2
20:19:55JinjaDCI: theory JinjaDCI.J1WellForm
20:19:56JinjaDCI: theory JinjaDCI.Compiler1
20:20:00JinjaDCI: theory JinjaDCI.Correctness1
20:20:00JinjaDCI: theory JinjaDCI.Correctness2
20:20:01JinjaDCI: theory JinjaDCI.Progress
20:20:03JinjaDCI: theory JinjaDCI.TypeSafe
20:20:04JinjaDCI: theory JinjaDCI.Equivalence
20:21:12JinjaDCI: theory JinjaDCI.Compiler
20:21:12JinjaDCI: theory JinjaDCI.TypeComp
20:21:16JinjaDCI: theory JinjaDCI.JinjaDCI
20:24:39Preparing JinjaDCI/document ...
20:24:56Finished JinjaDCI/document (0:00:16 elapsed time)
20:24:56Preparing JinjaDCI/outline ...
20:25:09Finished JinjaDCI/outline (0:00:13 elapsed time)
20:25:10Timing JinjaDCI (8 threads, 331.645s elapsed time, 2143.557s cpu time, 33.308s GC time, factor 6.46)
20:25:10Finished JinjaDCI (0:05:35 elapsed time, 0:35:52 cpu time, factor 6.43)
20:25:10Building Iptables_Semantics (on hpcisabelle/0) ...
20:25:12Iptables_Semantics: theory Iptables_Semantics.List_Misc
20:25:12Iptables_Semantics: theory Iptables_Semantics.Negation_Type
20:25:13Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
20:25:14Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
20:25:14Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
20:25:14Iptables_Semantics: theory HOL-Library.Code_Target_Int
20:25:14Iptables_Semantics: theory HOL-Library.LaTeXsugar
20:25:14Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
20:25:14Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
20:25:14Iptables_Semantics: theory Iptables_Semantics.Ternary
20:25:14Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion
20:25:14Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
20:25:14Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
20:25:14Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit
20:25:15Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
20:25:15Iptables_Semantics: theory Iptables_Semantics.Word_Upto
20:25:15Iptables_Semantics: theory Iptables_Semantics.IpAddresses
20:25:16Iptables_Semantics: theory Iptables_Semantics.Ports
20:25:16Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
20:25:17Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
20:25:29Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
20:25:29Iptables_Semantics: theory Iptables_Semantics.Semantics
20:25:29Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
20:25:30Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit
20:25:30Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
20:25:31Iptables_Semantics: theory Iptables_Semantics.Matching
20:25:31Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
20:25:31Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
20:25:32Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
20:25:32Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
20:25:32Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
20:25:32Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
20:25:33Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
20:25:33Iptables_Semantics: theory Iptables_Semantics.Optimizing
20:25:33Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
20:25:34Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
20:25:35Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
20:25:36Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
20:25:38Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
20:25:40Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
20:25:40Iptables_Semantics: theory Iptables_Semantics.Ipassmt
20:25:43Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
20:26:21Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
20:26:21Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
20:26:21Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
20:26:21Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
20:26:21Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
20:26:21Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
20:26:21Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
20:26:21Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
20:26:22Iptables_Semantics: theory Iptables_Semantics.No_Spoof
20:26:26Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
20:26:27Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
20:26:30Iptables_Semantics: theory Iptables_Semantics.Transform
20:26:34Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
20:26:35Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
20:26:40Iptables_Semantics: theory Iptables_Semantics.Code_Interface
20:26:42Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
20:26:43Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
20:26:43Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
20:26:43Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
20:26:46Iptables_Semantics: theory Iptables_Semantics.Parser
20:26:46Iptables_Semantics: theory Iptables_Semantics.Parser6
20:26:46Iptables_Semantics: theory Iptables_Semantics.Documentation
20:26:47Iptables_Semantics: theory Iptables_Semantics.Code_haskell
20:27:38Preparing Iptables_Semantics/document ...
20:28:01Finished Iptables_Semantics/document (0:00:23 elapsed time)
20:28:01Preparing Iptables_Semantics/outline ...
20:28:13Finished Iptables_Semantics/outline (0:00:12 elapsed time)
20:28:13Timing Iptables_Semantics (8 threads, 116.362s elapsed time, 590.355s cpu time, 31.122s GC time, factor 5.07)
20:28:13Finished Iptables_Semantics (0:02:26 elapsed time, 0:10:58 cpu time, factor 4.50)
20:28:14Building MFOTL_Monitor (on hpcisabelle/1) ...
20:28:16MFOTL_Monitor: theory MFOTL_Monitor.Trace
20:28:16MFOTL_Monitor: theory MFOTL_Monitor.Interval
20:28:16MFOTL_Monitor: theory MFOTL_Monitor.Table
20:28:17MFOTL_Monitor: theory MFOTL_Monitor.Abstract_Monitor
20:28:18MFOTL_Monitor: theory MFOTL_Monitor.MFOTL
20:28:25MFOTL_Monitor: theory MFOTL_Monitor.Slicing
20:28:25MFOTL_Monitor: theory MFOTL_Monitor.Monitor
20:28:57MFOTL_Monitor: theory MFOTL_Monitor.Monitor_Code
20:29:07MFOTL_Monitor: theory MFOTL_Monitor.Examples
20:29:39Preparing MFOTL_Monitor/document ...
20:29:45Finished MFOTL_Monitor/document (0:00:06 elapsed time)
20:29:45Preparing MFOTL_Monitor/outline ...
20:29:49Finished MFOTL_Monitor/outline (0:00:04 elapsed time)
20:29:49Timing MFOTL_Monitor (8 threads, 64.082s elapsed time, 322.550s cpu time, 6.038s GC time, factor 5.03)
20:29:49Finished MFOTL_Monitor (0:01:24 elapsed time, 0:06:03 cpu time, factor 4.31)
20:29:49Running Posix-Lexing (on hpcisabelle/2) ...
20:29:51Posix-Lexing: theory Posix-Lexing.Regular_Exps3
20:29:51Posix-Lexing: theory Posix-Lexing.Lexer
20:29:55Posix-Lexing: theory Posix-Lexing.Derivatives3
20:29:56Posix-Lexing: theory Posix-Lexing.Lexer3
20:29:59Posix-Lexing: theory Posix-Lexing.LexicalVals
20:29:59Posix-Lexing: theory Posix-Lexing.Simplifying
20:29:59Posix-Lexing: theory Posix-Lexing.Positions
20:32:38Posix-Lexing: theory Posix-Lexing.LexicalVals3
20:32:38Posix-Lexing: theory Posix-Lexing.Simplifying3
20:32:39Posix-Lexing: theory Posix-Lexing.Positions3
20:35:22Preparing Posix-Lexing/document ...
20:35:29Finished Posix-Lexing/document (0:00:06 elapsed time)
20:35:29Preparing Posix-Lexing/outline ...
20:35:32Finished Posix-Lexing/outline (0:00:03 elapsed time)
20:35:32Timing Posix-Lexing (8 threads, 328.900s elapsed time, 624.032s cpu time, 47.138s GC time, factor 1.90)
20:35:32Finished Posix-Lexing (0:05:32 elapsed time, 0:10:35 cpu time, factor 1.91)
20:35:33Running HOL-Nominal-Examples (on hpcisabelle/3) ...
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub
20:35:34HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height
20:35:37HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs
20:35:38HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu
20:35:38HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening
20:35:42HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern
20:35:42HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR
20:35:43HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN
20:35:43HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS
20:35:44HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization
20:35:45HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support
20:35:46HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation
20:35:46HOL-Nominal-Examples: theory HOL-Nominal-Examples.W
20:35:48HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
20:38:25HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
20:38:28HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
20:40:42HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition
20:40:51Timing HOL-Nominal-Examples (8 threads, 311.111s elapsed time, 1761.474s cpu time, 88.517s GC time, factor 5.66)
20:40:51Finished HOL-Nominal-Examples (0:05:14 elapsed time, 0:29:36 cpu time, factor 5.64)
20:40:51Building Affine_Arithmetic (on hpcisabelle/4) ...
20:40:53Affine_Arithmetic: theory Deriving.Derive_Manager
20:40:53Affine_Arithmetic: theory Deriving.Comparator
20:40:53Affine_Arithmetic: theory Deriving.Generator_Aux
20:40:53Affine_Arithmetic: theory HOL-Library.AList
20:40:53Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
20:40:53Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order
20:40:53Affine_Arithmetic: theory HOL-Library.Char_ord
20:40:53Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
20:40:54Affine_Arithmetic: theory HOL-Library.Code_Target_Int
20:40:54Affine_Arithmetic: theory HOL-Combinatorics.List_Permutation
20:40:54Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
20:40:54Affine_Arithmetic: theory HOL-Library.Monad_Syntax
20:40:54Affine_Arithmetic: theory HOL-Library.Code_Cardinality
20:40:54Affine_Arithmetic: theory HOL-Library.Type_Length
20:40:54Affine_Arithmetic: theory Deriving.Equality_Generator
20:40:54Affine_Arithmetic: theory HOL-Library.RBT_Impl
20:40:54Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
20:40:55Affine_Arithmetic: theory HOL-Library.Signed_Division
20:40:55Affine_Arithmetic: theory Deriving.Countable_Generator
20:40:55Affine_Arithmetic: theory Deriving.Equality_Instances
20:40:55Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
20:40:55Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
20:40:55Affine_Arithmetic: theory Deriving.Compare
20:40:55Affine_Arithmetic: theory Deriving.Comparator_Generator
20:40:55Affine_Arithmetic: theory HOL-Library.Word
20:40:55Affine_Arithmetic: theory HOL-Library.Mapping
20:40:56Affine_Arithmetic: theory HOL-Library.Log_Nat
20:40:56Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
20:40:56Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
20:40:57Affine_Arithmetic: theory List-Index.List_Index
20:40:57Affine_Arithmetic: theory Deriving.Compare_Generator
20:40:57Affine_Arithmetic: theory Deriving.Compare_Instances
20:40:57Affine_Arithmetic: theory Native_Word.Code_Int_Integer_Conversion
20:40:58Affine_Arithmetic: theory Show.Show
20:40:58Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
20:40:58Affine_Arithmetic: theory Word_Lib.More_Arithmetic
20:40:58Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
20:40:58Affine_Arithmetic: theory Word_Lib.More_Bit_Ring
20:40:59Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
20:40:59Affine_Arithmetic: theory Affine_Arithmetic.Polygon
20:40:59Affine_Arithmetic: theory Show.Show_Instances
20:41:02Affine_Arithmetic: theory HOL-Library.Interval
20:41:02Affine_Arithmetic: theory HOL-Library.Float
20:41:05Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
20:41:05Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral_Float
20:41:05Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
20:41:05Affine_Arithmetic: theory HOL-Library.Interval_Float
20:41:06Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
20:41:06Affine_Arithmetic: theory Word_Lib.Bit_Comprehension
20:41:06Affine_Arithmetic: theory Word_Lib.More_Divides
20:41:06Affine_Arithmetic: theory Word_Lib.Signed_Division_Word
20:41:06Affine_Arithmetic: theory Word_Lib.More_Word
20:41:07Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
20:41:09Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base
20:41:09Affine_Arithmetic: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:41:09Affine_Arithmetic: theory Word_Lib.Least_significant_bit
20:41:10Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
20:41:11Affine_Arithmetic: theory Word_Lib.Most_significant_bit
20:41:11Affine_Arithmetic: theory Word_Lib.Generic_set_bit
20:41:12Affine_Arithmetic: theory Native_Word.Code_Target_Integer_Bit
20:41:12Affine_Arithmetic: theory Native_Word.Word_Type_Copies
20:41:14Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
20:41:14Affine_Arithmetic: theory Affine_Arithmetic.Intersection
20:41:27Affine_Arithmetic: theory Native_Word.Uint32
20:41:30Affine_Arithmetic: theory Collections.HashCode
20:41:30Affine_Arithmetic: theory Deriving.Hash_Generator
20:41:31Affine_Arithmetic: theory Deriving.Hash_Instances
20:41:31Affine_Arithmetic: theory Deriving.Derive
20:42:05Affine_Arithmetic: theory HOL-Library.RBT
20:42:06Affine_Arithmetic: theory HOL-Library.RBT_Mapping
20:42:07Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
20:42:17Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
20:42:25Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
20:42:34Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
20:42:37Affine_Arithmetic: theory Affine_Arithmetic.Print
20:42:40Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
20:42:41Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
20:42:42Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
20:43:24Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
20:45:18Preparing Affine_Arithmetic/document ...
20:45:37Finished Affine_Arithmetic/document (0:00:18 elapsed time)
20:45:37Preparing Affine_Arithmetic/outline ...
20:45:48Finished Affine_Arithmetic/outline (0:00:10 elapsed time)
20:45:48Timing Affine_Arithmetic (8 threads, 225.173s elapsed time, 1573.758s cpu time, 77.901s GC time, factor 6.99)
20:45:48Finished Affine_Arithmetic (0:04:24 elapsed time, 0:27:42 cpu time, factor 6.29)
20:45:48Building Sepref_IICF (on hpcisabelle/5) ...
20:45:51Sepref_IICF: theory Refine_Imperative_HOL.IICF_List
20:45:51Sepref_IICF: theory Refine_Imperative_HOL.IICF_Map
20:45:51Sepref_IICF: theory Refine_Imperative_HOL.IICF_Matrix
20:45:51Sepref_IICF: theory Refine_Imperative_HOL.IICF_Multiset
20:45:51Sepref_IICF: theory Refine_Imperative_HOL.IICF_Set
20:45:52Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Map
20:45:52Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_Mset
20:45:52Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_MsetO
20:45:52Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Bag
20:45:52Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_SetO
20:45:53Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_List
20:45:53Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array
20:45:53Sepref_IICF: theory Refine_Imperative_HOL.IICF_HOL_List
20:45:53Sepref_IICF: theory Refine_Imperative_HOL.IICF_MS_Array_List
20:45:53Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heap
20:45:54Sepref_IICF: theory Refine_Imperative_HOL.IICF_Sepl_Binding
20:45:54Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
20:45:54Sepref_IICF: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
20:45:55Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heap
20:45:55Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_Matrix
20:45:57Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
20:46:13Sepref_IICF: theory Refine_Imperative_HOL.IICF
20:46:39Timing Sepref_IICF (8 threads, 31.150s elapsed time, 206.018s cpu time, 3.347s GC time, factor 6.61)
20:46:39Finished Sepref_IICF (0:00:50 elapsed time, 0:04:03 cpu time, factor 4.84)
20:46:39Running Universal_Hash_Families (on hpcisabelle/6) ...
20:46:42Universal_Hash_Families: theory Flow_Networks.Graph
20:46:42Universal_Hash_Families: theory Digit_Expansions.Bits_Digits
20:46:42Universal_Hash_Families: theory HOL-Computational_Algebra.Fraction_Field
20:46:42Universal_Hash_Families: theory HOL-Computational_Algebra.Group_Closure
20:46:42Universal_Hash_Families: theory HOL-Computational_Algebra.Nth_Powers
20:46:42Universal_Hash_Families: theory HOL-Computational_Algebra.Squarefree
20:46:42Universal_Hash_Families: theory HOL-Number_Theory.Cong
20:46:42Universal_Hash_Families: theory HOL-Library.Case_Converter
20:46:43Universal_Hash_Families: theory Finite_Fields.Finite_Fields_More_Bijections
20:46:43Universal_Hash_Families: theory HOL-Algebra.Congruence
20:46:43Universal_Hash_Families: theory HOL-Combinatorics.List_Permutation
20:46:43Universal_Hash_Families: theory HOL-Library.Code_Lazy
20:46:44Universal_Hash_Families: theory HOL-Library.Function_Algebras
20:46:44Universal_Hash_Families: theory HOL-Library.More_List
20:46:44Universal_Hash_Families: theory HOL-Library.Power_By_Squaring
20:46:44Universal_Hash_Families: theory HOL-Library.Transitive_Closure_Table
20:46:44Universal_Hash_Families: theory HOL-Library.While_Combinator
20:46:44Universal_Hash_Families: theory HOL-Number_Theory.Eratosthenes
20:46:44Universal_Hash_Families: theory HOL-Types_To_Sets.Types_To_Sets
20:46:45Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial
20:46:45Universal_Hash_Families: theory HOL-Library.Going_To_Filter
20:46:45Universal_Hash_Families: theory HOL-Algebra.Order
20:46:45Universal_Hash_Families: theory HOL-Computational_Algebra.Normalized_Fraction
20:46:46Universal_Hash_Families: theory HOL-Library.Log_Nat
20:46:46Universal_Hash_Families: theory Executable_Randomized_Algorithms.Tau_Additivity
20:46:46Universal_Hash_Families: theory HOL-Library.Bourbaki_Witt_Fixpoint
20:46:46Universal_Hash_Families: theory HOL-Number_Theory.Mod_Exp
20:46:46Universal_Hash_Families: theory HOL-Number_Theory.Fib
20:46:46Universal_Hash_Families: theory HOL-Number_Theory.Prime_Powers
20:46:46Universal_Hash_Families: theory Flow_Networks.Network
20:46:46Universal_Hash_Families: theory HOL-Number_Theory.Totient
20:46:46Universal_Hash_Families: theory HOL-Complex_Analysis.Contour_Integration
20:46:46Universal_Hash_Families: theory Finite_Fields.Finite_Fields_More_PMF
20:46:46Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families
20:46:46Universal_Hash_Families: theory Ergodic_Theory.SG_Library_Complement
20:46:47Universal_Hash_Families: theory HOL-Algebra.Lattice
20:46:47Universal_Hash_Families: theory Executable_Randomized_Algorithms.Coin_Space
20:46:47Universal_Hash_Families: theory MFMC_Countable.MFMC_Misc
20:46:47Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
20:46:48Universal_Hash_Families: theory Flow_Networks.Residual_Graph
20:46:48Universal_Hash_Families: theory Lp.Functional_Spaces
20:46:49Universal_Hash_Families: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
20:46:50Universal_Hash_Families: theory HOL-Algebra.Complete_Lattice
20:46:50Universal_Hash_Families: theory HOL-Complex_Analysis.Winding_Numbers
20:46:51Universal_Hash_Families: theory HOL-Algebra.Group
20:46:52Universal_Hash_Families: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
20:46:52Universal_Hash_Families: theory Flow_Networks.Augmenting_Flow
20:46:52Universal_Hash_Families: theory Flow_Networks.Augmenting_Path
20:46:53Universal_Hash_Families: theory Flow_Networks.Ford_Fulkerson
20:46:54Universal_Hash_Families: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
20:46:54Universal_Hash_Families: theory HOL-Complex_Analysis.Conformal_Mappings
20:46:55Universal_Hash_Families: theory Lp.Lp
20:46:55Universal_Hash_Families: theory HOL-Algebra.Coset
20:46:55Universal_Hash_Families: theory HOL-Algebra.FiniteProduct
20:46:55Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Singularities
20:46:55Universal_Hash_Families: theory HOL-Complex_Analysis.Great_Picard
20:46:56Universal_Hash_Families: theory MFMC_Countable.MFMC_Finite
20:46:57Universal_Hash_Families: theory HOL-Algebra.Ring
20:46:57Universal_Hash_Families: theory HOL-Complex_Analysis.Riemann_Mapping
20:46:57Universal_Hash_Families: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
20:46:57Universal_Hash_Families: theory MFMC_Countable.Matrix_For_Marginals
20:46:57Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
20:46:58Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Residues
20:46:59Universal_Hash_Families: theory HOL-Complex_Analysis.Residue_Theorem
20:46:59Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
20:46:59Universal_Hash_Families: theory HOL-Algebra.Divisibility
20:46:59Universal_Hash_Families: theory Universal_Hash_Families.Pseudorandom_Objects
20:47:00Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
20:47:01Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
20:47:01Universal_Hash_Families: theory HOL-Algebra.AbelCoset
20:47:01Universal_Hash_Families: theory HOL-Algebra.Module
20:47:01Universal_Hash_Families: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
20:47:02Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial_FPS
20:47:02Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial_Factorial
20:47:02Universal_Hash_Families: theory HOL-Computational_Algebra.Formal_Laurent_Series
20:47:04Universal_Hash_Families: theory MFMC_Countable.Rel_PMF_Characterisation
20:47:04Universal_Hash_Families: theory Probabilistic_While.While_SPMF
20:47:04Universal_Hash_Families: theory HOL-Algebra.Ideal
20:47:05Universal_Hash_Families: theory HOL-Computational_Algebra.Computational_Algebra
20:47:05Universal_Hash_Families: theory HOL-Complex_Analysis.Laurent_Convergence
20:47:06Universal_Hash_Families: theory HOL-Algebra.RingHom
20:47:08Universal_Hash_Families: theory HOL-Algebra.QuotRing
20:47:08Universal_Hash_Families: theory HOL-Algebra.UnivPoly
20:47:08Universal_Hash_Families: theory HOL-Complex_Analysis.Meromorphic
20:47:09Universal_Hash_Families: theory HOL-Complex_Analysis.Weierstrass_Factorization
20:47:10Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Analysis
20:47:11Universal_Hash_Families: theory HOL-Algebra.IntRing
20:47:24Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
20:47:28Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
20:47:28Universal_Hash_Families: theory HOL-Algebra.Subrings
20:47:28Universal_Hash_Families: theory HOL-Number_Theory.Residues
20:47:31Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
20:47:32Universal_Hash_Families: theory HOL-Number_Theory.Euler_Criterion
20:47:32Universal_Hash_Families: theory HOL-Number_Theory.Pocklington
20:47:32Universal_Hash_Families: theory HOL-Number_Theory.Gauss
20:47:33Universal_Hash_Families: theory HOL-Number_Theory.Residue_Primitive_Roots
20:47:33Universal_Hash_Families: theory HOL-Number_Theory.Quadratic_Reciprocity
20:47:33Universal_Hash_Families: theory HOL-Number_Theory.Number_Theory
20:47:35Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Misc
20:47:35Universal_Hash_Families: theory Dirichlet_Series.Multiplicative_Function
20:47:35Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Product
20:47:36Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Series
20:47:36Universal_Hash_Families: theory Dirichlet_Series.Euler_Products
20:47:38Universal_Hash_Families: theory HOL-Algebra.Polynomials
20:47:41Universal_Hash_Families: theory Dirichlet_Series.Moebius_Mu
20:47:41Universal_Hash_Families: theory Dirichlet_Series.More_Totient
20:47:41Universal_Hash_Families: theory Dirichlet_Series.Liouville_Lambda
20:47:41Universal_Hash_Families: theory Dirichlet_Series.Divisor_Count
20:47:42Universal_Hash_Families: theory Dirichlet_Series.Arithmetic_Summatory
20:47:42Universal_Hash_Families: theory Dirichlet_Series.Partial_Summation
20:47:44Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Series_Analysis
20:47:54Universal_Hash_Families: theory Zeta_Function.Zeta_Library
20:47:55Universal_Hash_Families: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
20:47:57Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
20:47:58Universal_Hash_Families: theory Executable_Randomized_Algorithms.Randomized_Algorithm
20:48:30Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
20:48:30Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
20:48:30Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
20:48:35Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
20:48:38Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
20:48:38Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
20:48:39Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
20:48:54Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
20:48:54Universal_Hash_Families: theory Finite_Fields.Formal_Polynomial_Derivatives
20:48:56Universal_Hash_Families: theory Finite_Fields.Monic_Polynomial_Factorization
20:49:03Universal_Hash_Families: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
20:49:10Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
20:49:10Universal_Hash_Families: theory Finite_Fields.Rabin_Irreducibility_Test
20:49:10Universal_Hash_Families: theory Finite_Fields.Card_Irreducible_Polynomials
20:49:21Universal_Hash_Families: theory Finite_Fields.Rabin_Irreducibility_Test_Code
20:49:25Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
20:49:35Universal_Hash_Families: theory Finite_Fields.Find_Irreducible_Poly
20:49:42Universal_Hash_Families: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
20:51:38Preparing Universal_Hash_Families/document ...
20:51:42Finished Universal_Hash_Families/document (0:00:04 elapsed time)
20:51:42Preparing Universal_Hash_Families/outline ...
20:51:45Finished Universal_Hash_Families/outline (0:00:02 elapsed time)
20:51:45Timing Universal_Hash_Families (8 threads, 285.425s elapsed time, 1930.786s cpu time, 200.780s GC time, factor 6.76)
20:51:45Finished Universal_Hash_Families (0:04:51 elapsed time, 0:32:29 cpu time, factor 6.69)
20:51:45Running Universal_Turing_Machine (on hpcisabelle/7) ...
20:51:47Universal_Turing_Machine: theory HOL-Library.Code_Abstract_Nat
20:51:47Universal_Turing_Machine: theory HOL-Library.Code_Target_Int
20:51:47Universal_Turing_Machine: theory HOL-Library.Code_Binary_Nat
20:51:47Universal_Turing_Machine: theory HOL-Library.Code_Target_Nat
20:51:47Universal_Turing_Machine: theory HOL-Library.Code_Target_Numeral
20:51:48Universal_Turing_Machine: theory HOL-Library.Discrete
20:51:48Universal_Turing_Machine: theory HOL-Library.Nat_Bijection
20:51:48Universal_Turing_Machine: theory Universal_Turing_Machine.Rec_Def
20:51:48Universal_Turing_Machine: theory Universal_Turing_Machine.Turing
20:51:48Universal_Turing_Machine: theory Universal_Turing_Machine.Recs_alt_Def
20:51:49Universal_Turing_Machine: theory Universal_Turing_Machine.Rec_Ex
20:51:50Universal_Turing_Machine: theory Universal_Turing_Machine.BlanksDoNotMatter
20:51:50Universal_Turing_Machine: theory Universal_Turing_Machine.ComposableTMs
20:51:50Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_aux
20:51:51Universal_Turing_Machine: theory Universal_Turing_Machine.ComposedTMs
20:51:51Universal_Turing_Machine: theory Universal_Turing_Machine.Numerals
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.Numerals_Ex
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_Hoare
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_Mopup
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.Recs_alt_Ex
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.DitherTM
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.OneStrokeTM
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.SemiIdTM
20:51:53Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_HaltingConditions
20:51:54Universal_Turing_Machine: theory Universal_Turing_Machine.CopyTM
20:51:54Universal_Turing_Machine: theory Universal_Turing_Machine.SimpleGoedelEncoding
20:51:54Universal_Turing_Machine: theory Universal_Turing_Machine.TuringDecidable
20:51:54Universal_Turing_Machine: theory Universal_Turing_Machine.WeakCopyTM
20:51:56Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus
20:51:58Universal_Turing_Machine: theory Universal_Turing_Machine.TuringUnComputable_H2
20:51:58Universal_Turing_Machine: theory Universal_Turing_Machine.TuringUnComputable_H2_original
20:51:58Universal_Turing_Machine: theory Universal_Turing_Machine.StrongCopyTM
20:52:03Universal_Turing_Machine: theory Universal_Turing_Machine.TuringReducible
20:52:03Universal_Turing_Machine: theory Universal_Turing_Machine.HaltingProblems_K_H
20:52:04Universal_Turing_Machine: theory Universal_Turing_Machine.HaltingProblems_K_aux
20:52:04Universal_Turing_Machine: theory Universal_Turing_Machine.TuringComputable
20:52:10Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_Hoare
20:52:10Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_alt_Compile
20:52:10Universal_Turing_Machine: theory Universal_Turing_Machine.UF
20:52:11Universal_Turing_Machine: theory Universal_Turing_Machine.Recursive
20:52:11Universal_Turing_Machine: theory Universal_Turing_Machine.GeneratedCode
20:52:34Universal_Turing_Machine: theory Universal_Turing_Machine.UTM
20:56:13Preparing Universal_Turing_Machine/document ...
20:56:41Finished Universal_Turing_Machine/document (0:00:27 elapsed time)
20:56:41Preparing Universal_Turing_Machine/outline ...
20:56:55Finished Universal_Turing_Machine/outline (0:00:14 elapsed time)
20:56:55Timing Universal_Turing_Machine (8 threads, 262.198s elapsed time, 1585.181s cpu time, 14.025s GC time, factor 6.05)
20:56:55Finished Universal_Turing_Machine (0:04:24 elapsed time, 0:26:32 cpu time, factor 6.01)
20:56:55Running HOL-ex (on hpcisabelle/0) ...
20:56:57HOL-ex: theory HOL-Combinatorics.Transposition
20:56:57HOL-ex: theory HOL-ex.Bubblesort
20:56:57HOL-ex: theory HOL-ex.Quicksort
20:56:57HOL-ex: theory HOL-ex.MergeSort
20:56:57HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples
20:56:57HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples
20:56:57HOL-ex: theory HOL-ex.IArray_Examples
20:56:57HOL-ex: theory HOL-ex.Datatype_Record_Examples
20:56:58HOL-ex: theory HOL-Combinatorics.Perm
20:56:58HOL-ex: theory HOL-ex.Code_Lazy_Demo
20:56:58HOL-ex: theory HOL-ex.Refute_Examples
20:56:58HOL-ex: theory HOL-ex.Radix_Sort
20:56:58HOL-ex: theory HOL-ex.Specifications_with_bundle_mixins
20:56:59HOL-ex: theory HOL-ex.Perm_Fragments
20:56:59HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex
20:56:59HOL-ex: theory HOL-ex.While_Combinator_Example
20:56:59HOL-ex: theory HOL-ex.Code_Timing
20:56:59HOL-ex: theory HOL-ex.Antiquote
20:56:59HOL-ex: theory HOL-ex.Arith_Examples
20:56:59HOL-ex: theory HOL-ex.Birthday_Paradox
20:56:59HOL-ex: theory HOL-ex.CTL
20:56:59HOL-ex: theory HOL-ex.Cartouche_Examples
20:57:00HOL-ex: theory HOL-ex.Case_Product
20:57:00HOL-ex: theory HOL-ex.Chinese
20:57:00HOL-ex: theory HOL-ex.Classical
20:57:00HOL-ex: theory HOL-ex.Coercion_Examples
20:57:00HOL-ex: theory HOL-ex.Computations
20:57:01HOL-ex: theory HOL-ex.Erdoes_Szekeres
20:57:01HOL-ex: theory HOL-ex.Executable_Relation
20:57:01HOL-ex: theory HOL-ex.Execute_Choice
20:57:01HOL-ex: theory HOL-ex.Hebrew
20:57:01HOL-ex: theory HOL-ex.Hex_Bin_Examples
20:57:01HOL-ex: theory HOL-ex.Intuitionistic
20:57:01HOL-ex: theory HOL-ex.Join_Theory
20:57:01HOL-ex: theory HOL-ex.Lagrange
20:57:01HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples
20:57:01HOL-ex: theory HOL-ex.LocaleTest2
20:57:01HOL-ex: theory HOL-ex.MonoidGroup
20:57:01HOL-ex: theory HOL-ex.Multiquote
20:57:01HOL-ex: theory HOL-ex.NatSum
20:57:01HOL-ex: theory HOL-ex.PER
20:57:02HOL-ex: theory HOL-ex.Peano_Axioms
20:57:02HOL-ex: theory HOL-ex.PresburgerEx
20:57:02HOL-ex: theory HOL-ex.Residue_Ring
20:57:02HOL-ex: theory HOL-ex.Serbian
20:57:02HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples
20:57:02HOL-ex: theory HOL-ex.Set_Theory
20:57:02HOL-ex: theory HOL-ex.Simproc_Tests
20:57:02HOL-ex: theory HOL-ex.Sketch_and_Explore
20:57:02HOL-ex: theory HOL-ex.Sorting_Algorithms_Examples
20:57:03HOL-ex: theory HOL-ex.Sudoku
20:57:03HOL-ex: theory HOL-ex.Tarski
20:57:03HOL-ex: theory HOL-ex.Termination
20:57:04HOL-ex: theory HOL-ex.ThreeDivides
20:57:04HOL-ex: theory HOL-ex.Transfer_Int_Nat
20:57:04HOL-ex: theory HOL-ex.Tree23
20:57:04HOL-ex: theory HOL-ex.Unification
20:57:04HOL-ex: theory HOL-ex.veriT_Preprocessing
20:57:05HOL-ex: theory HOL-ex.Transfer_Debug
20:57:05HOL-ex: theory HOL-ex.Function_Growth
20:57:05HOL-ex: theory HOL-ex.SOS
20:57:05HOL-ex: theory HOL-ex.SOS_Cert
20:57:05HOL-ex: theory HOL-ex.Argo_Examples
20:57:06HOL-ex: theory HOL-ex.Ballot
20:57:06HOL-ex: theory HOL-ex.BigO
20:57:06HOL-ex: theory HOL-ex.BinEx
20:57:08HOL-ex: theory HOL-ex.Code_Binary_Nat_examples
20:57:08HOL-ex: theory HOL-ex.Cubic_Quartic
20:57:08HOL-ex: theory HOL-ex.Eval_Examples
20:57:08HOL-ex: theory HOL-ex.Gauge_Integration
20:57:08HOL-ex: theory HOL-ex.HarmonicSeries
20:57:08HOL-ex: theory HOL-ex.Normalization_by_Evaluation
20:57:08HOL-ex: theory HOL-ex.Parallel_Example
20:57:08HOL-ex: theory HOL-ex.Pythagoras
20:57:08HOL-ex: theory HOL-ex.Reflection_Examples
20:57:09HOL-ex: theory HOL-ex.Sqrt_Script
20:57:09HOL-ex: theory HOL-ex.Triangular_Numbers
21:00:58HOL-ex: theory HOL-ex.Meson_Test
21:00:58HOL-ex: theory HOL-ex.SAT_Examples
21:01:50Timing HOL-ex (8 threads, 289.310s elapsed time, 1309.342s cpu time, 86.358s GC time, factor 4.53)
21:01:50Finished HOL-ex (0:04:53 elapsed time, 0:21:58 cpu time, factor 4.50)
21:01:50Building Markov_Models (on hpcisabelle/1) ...
21:01:53Markov_Models: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
21:01:53Markov_Models: theory HOL-Computational_Algebra.Group_Closure
21:01:53Markov_Models: theory HOL-Library.Case_Converter
21:01:53Markov_Models: theory HOL-Library.Code_Abstract_Nat
21:01:53Markov_Models: theory HOL-Library.Code_Target_Int
21:01:53Markov_Models: theory HOL-Library.IArray
21:01:53Markov_Models: theory HOL-Library.While_Combinator
21:01:53Markov_Models: theory Coinductive.Coinductive_Nat
21:01:53Markov_Models: theory HOL-Library.Code_Target_Nat
21:01:53Markov_Models: theory HOL-Library.Code_Target_Numeral
21:01:54Markov_Models: theory HOL-Library.Simps_Case_Conv
21:01:54Markov_Models: theory Coinductive.Coinductive_List
21:02:02Markov_Models: theory Coinductive.Coinductive_Stream
21:02:04Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
21:02:07Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
21:02:07Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
21:02:09Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
21:02:09Markov_Models: theory Markov_Models.Crowds_Protocol
21:02:09Markov_Models: theory Markov_Models.Gossip_Broadcast
21:02:09Markov_Models: theory Markov_Models.PCTL
21:02:09Markov_Models: theory Markov_Models.Markov_Decision_Process
21:02:09Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
21:02:09Markov_Models: theory Markov_Models.Zeroconf_Analysis
21:02:10Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
21:02:13Markov_Models: theory Markov_Models.MDP_Reachability_Problem
21:02:13Markov_Models: theory Markov_Models.PGCL
21:02:14Markov_Models: theory Markov_Models.Example_A
21:02:14Markov_Models: theory Markov_Models.Example_B
21:02:14Markov_Models: theory Markov_Models.MDP_RP_Certification
21:02:14Markov_Models: theory Markov_Models.Markov_Models
21:02:48Markov_Models: theory Markov_Models.MDP_RP
21:03:27Preparing Markov_Models/document ...
21:03:45Finished Markov_Models/document (0:00:18 elapsed time)
21:03:45Preparing Markov_Models/outline ...
21:03:53Finished Markov_Models/outline (0:00:07 elapsed time)
21:03:53Timing Markov_Models (8 threads, 69.373s elapsed time, 393.974s cpu time, 9.229s GC time, factor 5.68)
21:03:53Finished Markov_Models (0:01:34 elapsed time, 0:07:25 cpu time, factor 4.70)
21:03:53Running Picks_Theorem (on hpcisabelle/2) ...
21:03:56Picks_Theorem: theory HOL-Decision_Procs.Dense_Linear_Order
21:03:56Picks_Theorem: theory HOL-Library.Code_Abstract_Nat
21:03:56Picks_Theorem: theory HOL-Library.Code_Target_Int
21:03:56Picks_Theorem: theory HOL-Library.Code_Cardinality
21:03:56Picks_Theorem: theory HOL-Library.Sublist
21:03:56Picks_Theorem: theory HOL-Library.Diagonal_Subsequence
21:03:56Picks_Theorem: theory HOL-Library.Lattice_Algebras
21:03:56Picks_Theorem: theory HOL-Library.Log_Nat
21:03:56Picks_Theorem: theory HOL-Library.Code_Target_Nat
21:03:56Picks_Theorem: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
21:03:56Picks_Theorem: theory Triangle.Angles
21:03:56Picks_Theorem: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
21:03:56Picks_Theorem: theory HOL-Library.Code_Target_Numeral
21:03:56Picks_Theorem: theory Ordinary_Differential_Equations.Vector_Derivative_On
21:03:57Picks_Theorem: theory Picks_Theorem.Integral_Matrix
21:03:57Picks_Theorem: theory List-Index.List_Index
21:03:57Picks_Theorem: theory Triangle.Triangle
21:03:57Picks_Theorem: theory Ordinary_Differential_Equations.Gronwall
21:03:57Picks_Theorem: theory Ordinary_Differential_Equations.Interval_Integral_HK
21:04:03Picks_Theorem: theory HOL-Library.Interval
21:04:03Picks_Theorem: theory HOL-Library.Float
21:04:06Picks_Theorem: theory HOL-Library.Code_Target_Numeral_Float
21:04:06Picks_Theorem: theory HOL-Library.Interval_Float
21:04:06Picks_Theorem: theory Affine_Arithmetic.Executable_Euclidean_Space
21:04:08Picks_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
21:04:11Picks_Theorem: theory Ordinary_Differential_Equations.ODE_Auxiliarities
21:04:12Picks_Theorem: theory Ordinary_Differential_Equations.Cones
21:04:13Picks_Theorem: theory Ordinary_Differential_Equations.Initial_Value_Problem
21:04:13Picks_Theorem: theory Ordinary_Differential_Equations.Multivariate_Taylor
21:04:14Picks_Theorem: theory HOL-Decision_Procs.Approximation
21:04:16Picks_Theorem: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
21:04:17Picks_Theorem: theory Ordinary_Differential_Equations.Flow
21:04:22Picks_Theorem: theory Ordinary_Differential_Equations.Poincare_Map
21:04:22Picks_Theorem: theory Ordinary_Differential_Equations.Upper_Lower_Solution
21:04:22Picks_Theorem: theory Ordinary_Differential_Equations.Linear_ODE
21:04:25Picks_Theorem: theory Ordinary_Differential_Equations.Reachability_Analysis
21:04:27Picks_Theorem: theory Ordinary_Differential_Equations.Flow_Congs
21:05:04Picks_Theorem: theory Affine_Arithmetic.Floatarith_Expression
21:05:04Picks_Theorem: theory Ordinary_Differential_Equations.MVT_Ex
21:05:07Picks_Theorem: theory Ordinary_Differential_Equations.ODE_Analysis
21:05:10Picks_Theorem: theory Poincare_Bendixson.Analysis_Misc
21:05:11Picks_Theorem: theory Poincare_Bendixson.ODE_Misc
21:05:16Picks_Theorem: theory Poincare_Bendixson.Invariance
21:05:19Picks_Theorem: theory Poincare_Bendixson.Limit_Set
21:05:21Picks_Theorem: theory Poincare_Bendixson.Periodic_Orbit
21:05:23Picks_Theorem: theory Poincare_Bendixson.Poincare_Bendixson
21:05:28Picks_Theorem: theory Picks_Theorem.Polygon_Jordan_Curve
21:05:30Picks_Theorem: theory Picks_Theorem.Polygon_Lemmas
21:05:31Picks_Theorem: theory Picks_Theorem.Linepath_Collinearity
21:05:32Picks_Theorem: theory Picks_Theorem.Polygon_Convex_Lemmas
21:05:32Picks_Theorem: theory Picks_Theorem.Triangle_Lemmas
21:05:33Picks_Theorem: theory Picks_Theorem.Polygon_Splitting
21:05:34Picks_Theorem: theory Picks_Theorem.Unit_Geometry
21:05:34Picks_Theorem: theory Picks_Theorem.Elementary_Triangle_Area
21:05:34Picks_Theorem: theory Picks_Theorem.Pick
21:08:44Preparing Picks_Theorem/document ...
21:09:04Finished Picks_Theorem/document (0:00:20 elapsed time)
21:09:04Preparing Picks_Theorem/outline ...
21:09:09Finished Picks_Theorem/outline (0:00:05 elapsed time)
21:09:10Timing Picks_Theorem (8 threads, 282.849s elapsed time, 1718.554s cpu time, 33.500s GC time, factor 6.08)
21:09:10Finished Picks_Theorem (0:04:46 elapsed time, 0:28:48 cpu time, factor 6.03)
21:09:10Running ResiduatedTransitionSystem (on hpcisabelle/3) ...
21:09:24ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.ResiduatedTransitionSystem
21:09:47ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.LambdaCalculus
21:14:06Preparing ResiduatedTransitionSystem/document ...
21:14:32Finished ResiduatedTransitionSystem/document (0:00:26 elapsed time)
21:14:32Preparing ResiduatedTransitionSystem/outline ...
21:14:41Finished ResiduatedTransitionSystem/outline (0:00:08 elapsed time)
21:14:41Timing ResiduatedTransitionSystem (8 threads, 292.185s elapsed time, 1113.185s cpu time, 24.671s GC time, factor 3.81)
21:14:41Finished ResiduatedTransitionSystem (0:04:55 elapsed time, 0:18:41 cpu time, factor 3.80)
21:14:41Building SM_Base (on hpcisabelle/4) ...
21:14:44SM_Base: theory Partial_Order_Reduction.Basic_Extensions
21:14:44SM_Base: theory HOL-Library.Case_Converter
21:14:44SM_Base: theory Partial_Order_Reduction.Set_Extensions
21:14:44SM_Base: theory HOL-Library.Complete_Partial_Order2
21:14:44SM_Base: theory DFS_Framework.DFS_Framework_Misc
21:14:44SM_Base: theory HOL-Library.Stream
21:14:44SM_Base: theory HOL-Library.Sublist
21:14:44SM_Base: theory HOL-Library.Countable_Set
21:14:44SM_Base: theory LTL.LTL
21:14:44SM_Base: theory Partial_Order_Reduction.Functions
21:14:45SM_Base: theory HOL-Library.Simps_Case_Conv
21:14:45SM_Base: theory DFS_Framework.DFS_Framework_Refine_Aux
21:14:45SM_Base: theory Stuttering_Equivalence.Samplers
21:14:45SM_Base: theory Partial_Order_Reduction.Relation_Extensions
21:14:45SM_Base: theory HOL-Library.Countable_Complete_Lattices
21:14:45SM_Base: theory Transition_Systems_and_Automata.Basic
21:14:46SM_Base: theory Stuttering_Equivalence.StutterEquivalence
21:14:46SM_Base: theory DFS_Framework.Impl_Rev_Array_Stack
21:14:46SM_Base: theory DFS_Framework.Param_DFS
21:14:47SM_Base: theory Transition_Systems_and_Automata.Sequence
21:14:48SM_Base: theory HOL-Library.Prefix_Order
21:14:48SM_Base: theory Partial_Order_Reduction.List_Extensions
21:14:48SM_Base: theory Transition_Systems_and_Automata.Transition_System
21:14:48SM_Base: theory Partial_Order_Reduction.List_Prefixes
21:14:48SM_Base: theory Partial_Order_Reduction.Word_Prefixes
21:14:48SM_Base: theory Partial_Order_Reduction.Traces
21:14:49SM_Base: theory HOL-Library.Order_Continuity
21:14:50SM_Base: theory HOL-Library.Extended_Nat
21:14:51SM_Base: theory Coinductive.Coinductive_Nat
21:14:51SM_Base: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:14:51SM_Base: theory DFS_Framework.DFS_Invars_Basic
21:14:51SM_Base: theory DFS_Framework.General_DFS_Structure
21:14:52SM_Base: theory Coinductive.Coinductive_List
21:14:52SM_Base: theory Partial_Order_Reduction.ENat_Extensions
21:14:52SM_Base: theory Partial_Order_Reduction.CCPO_Extensions
21:14:53SM_Base: theory Transition_Systems_and_Automata.Sequence_LTL
21:14:54SM_Base: theory Partial_Order_Reduction.ESet_Extensions
21:14:54SM_Base: theory Transition_Systems_and_Automata.Transition_System_Construction
21:14:54SM_Base: theory Transition_Systems_and_Automata.Transition_System_Extra
21:14:55SM_Base: theory Partial_Order_Reduction.Transition_System_Extensions
21:14:57SM_Base: theory Partial_Order_Reduction.Transition_System_Traces
21:15:00SM_Base: theory DFS_Framework.Rec_Impl
21:15:00SM_Base: theory DFS_Framework.Tailrec_Impl
21:15:01SM_Base: theory Coinductive.Coinductive_List_Prefix
21:15:01SM_Base: theory Coinductive.Coinductive_Stream
21:15:02SM_Base: theory Partial_Order_Reduction.Coinductive_List_Extensions
21:15:03SM_Base: theory Stuttering_Equivalence.PLTL
21:15:04SM_Base: theory Partial_Order_Reduction.LList_Prefixes
21:15:05SM_Base: theory Partial_Order_Reduction.Stuttering
21:15:06SM_Base: theory Partial_Order_Reduction.Formula
21:15:06SM_Base: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
21:15:07SM_Base: theory Partial_Order_Reduction.Ample_Abstract
21:15:08SM_Base: theory Partial_Order_Reduction.Ample_Analysis
21:15:08SM_Base: theory Partial_Order_Reduction.Ample_Correctness
21:15:09SM_Base: theory DFS_Framework.Simple_Impl
21:15:15SM_Base: theory DFS_Framework.Restr_Impl
21:15:17SM_Base: theory DFS_Framework.DFS_Framework
21:15:18SM_Base: theory DFS_Framework.Reachable_Nodes
21:16:11SM_Base: theory DFS_Framework.Feedback_Arcs
21:17:23Timing SM_Base (8 threads, 127.787s elapsed time, 603.103s cpu time, 38.328s GC time, factor 4.72)
21:17:23Finished SM_Base (0:02:39 elapsed time, 0:11:12 cpu time, factor 4.23)
21:17:23Running HOL-Data_Structures (on hpcisabelle/5) ...
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Less_False
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Cmp
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Define_Time_Function
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Queue_Spec
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Tree23
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.Tree234
21:17:24HOL-Data_Structures: theory HOL-Library.Cancellation
21:17:24HOL-Data_Structures: theory HOL-Library.Pattern_Aliases
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del
21:17:24HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del
21:17:25HOL-Data_Structures: theory HOL-Library.Tree
21:17:25HOL-Data_Structures: theory HOL-Data_Structures.Reverse
21:17:25HOL-Data_Structures: theory HOL-Data_Structures.Time_Funs
21:17:25HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs
21:17:25HOL-Data_Structures: theory HOL-Data_Structures.Trie_Fun
21:17:26HOL-Data_Structures: theory HOL-Data_Structures.Tries_Binary
21:17:26HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs
21:17:26HOL-Data_Structures: theory HOL-Data_Structures.Queue_2Lists
21:17:26HOL-Data_Structures: theory HOL-Library.Multiset
21:17:26HOL-Data_Structures: theory HOL-Number_Theory.Fib
21:17:27HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set
21:17:27HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set
21:17:27HOL-Data_Structures: theory HOL-Data_Structures.Tree23_of_List
21:17:28HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set
21:17:29HOL-Data_Structures: theory HOL-Data_Structures.Tree2
21:17:29HOL-Data_Structures: theory HOL-Data_Structures.Tree_Rotations
21:17:29HOL-Data_Structures: theory HOL-Data_Structures.Isin2
21:17:29HOL-Data_Structures: theory HOL-Data_Structures.Lookup2
21:17:30HOL-Data_Structures: theory HOL-Data_Structures.RBT
21:17:30HOL-Data_Structures: theory HOL-Data_Structures.AA_Set
21:17:30HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal2_Set
21:17:30HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal_Set
21:17:32HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set_Code
21:17:34HOL-Data_Structures: theory HOL-Data_Structures.Height_Balanced_Tree
21:17:34HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs
21:17:34HOL-Data_Structures: theory HOL-Data_Structures.Interval_Tree
21:17:34HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join
21:17:35HOL-Data_Structures: theory HOL-Data_Structures.AA_Map
21:17:35HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set
21:17:36HOL-Data_Structures: theory HOL-Library.Tree_Multiset
21:17:36HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap
21:17:36HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap
21:17:36HOL-Data_Structures: theory HOL-Data_Structures.Heaps
21:17:37HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map
21:17:37HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set
21:17:37HOL-Data_Structures: theory HOL-Data_Structures.Sorting
21:17:38HOL-Data_Structures: theory HOL-Data_Structures.Trie_Map
21:17:38HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map
21:17:39HOL-Data_Structures: theory HOL-Library.Tree_Real
21:17:40HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map
21:17:40HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set2
21:17:40HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap_List
21:17:40HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT
21:17:41HOL-Data_Structures: theory HOL-Data_Structures.Balance
21:17:41HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree
21:17:41HOL-Data_Structures: theory HOL-Data_Structures.Selection
21:17:41HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set
21:17:42HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun
21:17:43HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map
21:17:57HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map
21:19:04HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map
21:22:04Preparing HOL-Data_Structures/document ...
21:22:16Finished HOL-Data_Structures/document (0:00:11 elapsed time)
21:22:16Timing HOL-Data_Structures (8 threads, 275.955s elapsed time, 2198.385s cpu time, 147.401s GC time, factor 7.97)
21:22:16Finished HOL-Data_Structures (0:04:40 elapsed time, 0:36:56 cpu time, factor 7.91)
21:22:16Running Psi_Calculi (on hpcisabelle/6) ...
21:22:17Psi_Calculi: theory Psi_Calculi.Chain
21:22:19Psi_Calculi: theory Psi_Calculi.Subst_Term
21:22:19Psi_Calculi: theory Psi_Calculi.Agent
21:22:35Psi_Calculi: theory Psi_Calculi.Close_Subst
21:22:35Psi_Calculi: theory Psi_Calculi.Frame
21:22:35Psi_Calculi: theory Psi_Calculi.Structural_Congruence
21:22:39Psi_Calculi: theory Psi_Calculi.Semantics
21:22:52Psi_Calculi: theory Psi_Calculi.Simulation
21:22:53Psi_Calculi: theory Psi_Calculi.Sum
21:22:53Psi_Calculi: theory Psi_Calculi.Bisimulation
21:22:54Psi_Calculi: theory Psi_Calculi.Sim_Pres
21:22:54Psi_Calculi: theory Psi_Calculi.Sim_Struct_Cong
21:22:55Psi_Calculi: theory Psi_Calculi.Tau_Chain
21:22:55Psi_Calculi: theory Psi_Calculi.Bisim_Pres
21:22:56Psi_Calculi: theory Psi_Calculi.Bisim_Struct_Cong
21:22:56Psi_Calculi: theory Psi_Calculi.Weak_Simulation
21:22:57Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp
21:22:57Psi_Calculi: theory Psi_Calculi.Weak_Cong_Simulation
21:22:57Psi_Calculi: theory Psi_Calculi.Weak_Sim_Pres
21:22:58Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp_Pres
21:22:58Psi_Calculi: theory Psi_Calculi.Bisim_Subst
21:22:58Psi_Calculi: theory Psi_Calculi.Weak_Bisimulation
21:22:59Psi_Calculi: theory Psi_Calculi.Weak_Cong_Sim_Pres
21:23:00Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Pres
21:23:00Psi_Calculi: theory Psi_Calculi.Weak_Psi_Congruence
21:23:00Psi_Calculi: theory Psi_Calculi.Weakening
21:23:01Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Struct_Cong
21:23:01Psi_Calculi: theory Psi_Calculi.Weaken_Transition
21:23:01Psi_Calculi: theory Psi_Calculi.Weak_Cong_Pres
21:23:02Psi_Calculi: theory Psi_Calculi.Weaken_Stat_Imp
21:23:02Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Subst
21:23:02Psi_Calculi: theory Psi_Calculi.Weak_Cong_Struct_Cong
21:23:03Psi_Calculi: theory Psi_Calculi.Weaken_Simulation
21:23:03Psi_Calculi: theory Psi_Calculi.Weak_Congruence
21:23:03Psi_Calculi: theory Psi_Calculi.Weaken_Bisimulation
21:23:04Psi_Calculi: theory Psi_Calculi.Tau
21:23:06Psi_Calculi: theory Psi_Calculi.Tau_Sim
21:23:10Psi_Calculi: theory Psi_Calculi.Tau_Stat_Imp
21:23:12Psi_Calculi: theory Psi_Calculi.Tau_Laws_No_Weak
21:23:12Psi_Calculi: theory Psi_Calculi.Tau_Laws_Weak
21:26:56Preparing Psi_Calculi/document ...
21:27:46Finished Psi_Calculi/document (0:00:50 elapsed time)
21:27:46Preparing Psi_Calculi/outline ...
21:28:02Finished Psi_Calculi/outline (0:00:16 elapsed time)
21:28:02Timing Psi_Calculi (8 threads, 273.549s elapsed time, 1223.824s cpu time, 42.824s GC time, factor 4.47)
21:28:02Finished Psi_Calculi (0:04:36 elapsed time, 0:20:31 cpu time, factor 4.46)
21:28:03Building LEM (on hpcisabelle/7) ...
21:28:04LEM: theory HOL-Combinatorics.Transposition
21:28:04LEM: theory HOL-Library.Cancellation
21:28:04LEM: theory HOL-Library.Phantom_Type
21:28:04LEM: theory HOL-Library.FuncSet
21:28:04LEM: theory LEM.Lem_bool
21:28:04LEM: theory HOL-Library.While_Combinator
21:28:04LEM: theory HOL-Library.Sublist
21:28:04LEM: theory Word_Lib.Even_More_List
21:28:04LEM: theory LEM.Lem_basic_classes
21:28:04LEM: theory Word_Lib.More_Bit_Ring
21:28:05LEM: theory HOL-Library.Disjoint_Sets
21:28:05LEM: theory HOL-Library.Multiset
21:28:06LEM: theory HOL-Library.Cardinality
21:28:07LEM: theory HOL-Library.Numeral_Type
21:28:08LEM: theory HOL-Library.Type_Length
21:28:09LEM: theory HOL-Library.Word
21:28:09LEM: theory Word_Lib.More_Arithmetic
21:28:11LEM: theory LEM.Lem_function
21:28:11LEM: theory LEM.Lem_tuple
21:28:11LEM: theory LEM.Lem_maybe
21:28:12LEM: theory HOL-Combinatorics.Permutations
21:28:14LEM: theory HOL-Combinatorics.List_Permutation
21:28:14LEM: theory LEM.LemExtraDefs
21:28:20LEM: theory Word_Lib.Bit_Comprehension
21:28:20LEM: theory Word_Lib.Legacy_Aliases
21:28:20LEM: theory Word_Lib.More_Divides
21:28:20LEM: theory LEM.Lem_num
21:28:20LEM: theory Word_Lib.More_Word
21:28:22LEM: theory Word_Lib.Bit_Shifts_Infix_Syntax
21:28:22LEM: theory Word_Lib.Least_significant_bit
21:28:24LEM: theory Word_Lib.Aligned
21:28:24LEM: theory Word_Lib.Singleton_Bit_Shifts
21:28:24LEM: theory Word_Lib.Most_significant_bit
21:28:25LEM: theory Word_Lib.Generic_set_bit
21:28:26LEM: theory Word_Lib.Bits_Int
21:28:28LEM: theory LEM.Lem_set_helpers
21:28:30LEM: theory Word_Lib.Typedef_Morphisms
21:28:31LEM: theory Word_Lib.Reversed_Bit_Lists
21:28:34LEM: theory LEM.Lem
21:28:35LEM: theory LEM.Lem_assert_extra
21:28:35LEM: theory LEM.Lem_function_extra
21:28:35LEM: theory LEM.Lem_list
21:28:35LEM: theory LEM.Lem_maybe_extra
21:28:40LEM: theory LEM.Lem_either
21:28:40LEM: theory LEM.Lem_list_extra
21:28:40LEM: theory LEM.Lem_word
21:28:40LEM: theory LEM.Lem_set
21:28:40LEM: theory LEM.Lem_string
21:28:40LEM: theory LEM.Lem_sorting
21:28:40LEM: theory LEM.Lem_num_extra
21:28:40LEM: theory LEM.Lem_show
21:28:40LEM: theory LEM.Lem_map
21:28:40LEM: theory LEM.Lem_relation
21:28:40LEM: theory LEM.Lem_set_extra
21:28:41LEM: theory LEM.Lem_map_extra
21:28:41LEM: theory LEM.Lem_machine_word
21:28:41LEM: theory LEM.Lem_string_extra
21:28:42LEM: theory LEM.Lem_show_extra
21:28:46LEM: theory LEM.Lem_pervasives
21:28:47LEM: theory LEM.Lem_pervasives_extra
21:29:11Timing LEM (8 threads, 48.314s elapsed time, 302.315s cpu time, 8.966s GC time, factor 6.26)
21:29:11Finished LEM (0:01:06 elapsed time, 0:05:43 cpu time, factor 5.14)
21:29:11Running Schoenhage_Strassen (on hpcisabelle/0) ...
21:29:14Schoenhage_Strassen: theory Pure-ex.Guess
21:29:14Schoenhage_Strassen: theory HOL-Eisbach.Eisbach
21:29:14Schoenhage_Strassen: theory HOL-Number_Theory.Cong
21:29:14Schoenhage_Strassen: theory HOL-Library.Adhoc_Overloading
21:29:14Schoenhage_Strassen: theory HOL-Computational_Algebra.Fraction_Field
21:29:14Schoenhage_Strassen: theory HOL-Algebra.Congruence
21:29:14Schoenhage_Strassen: theory HOL-Combinatorics.List_Permutation
21:29:14Schoenhage_Strassen: theory HOL-Library.Function_Algebras
21:29:14Schoenhage_Strassen: theory HOL-Library.More_List
21:29:15Schoenhage_Strassen: theory HOL-Library.Type_Length
21:29:15Schoenhage_Strassen: theory HOL-Library.Power_By_Squaring
21:29:15Schoenhage_Strassen: theory HOL-Library.Monad_Syntax
21:29:15Schoenhage_Strassen: theory HOL-Number_Theory.Eratosthenes
21:29:15Schoenhage_Strassen: theory Polynomial_Interpolation.Missing_Unsorted
21:29:15Schoenhage_Strassen: theory Akra_Bazzi.Eval_Numeral
21:29:15Schoenhage_Strassen: theory HOL-Computational_Algebra.Polynomial
21:29:15Schoenhage_Strassen: theory HOL-Library.Log_Nat
21:29:16Schoenhage_Strassen: theory HOL-Number_Theory.Fib
21:29:16Schoenhage_Strassen: theory HOL-Eisbach.Eisbach_Tools
21:29:16Schoenhage_Strassen: theory Expander_Graphs.Extra_Congruence_Method
21:29:16Schoenhage_Strassen: theory HOL-Algebra.Order
21:29:16Schoenhage_Strassen: theory HOL-Library.Word
21:29:17Schoenhage_Strassen: theory HOL-Computational_Algebra.Normalized_Fraction
21:29:17Schoenhage_Strassen: theory HOL-Number_Theory.Prime_Powers
21:29:17Schoenhage_Strassen: theory HOL-Number_Theory.Mod_Exp
21:29:17Schoenhage_Strassen: theory HOL-Number_Theory.Totient
21:29:17Schoenhage_Strassen: theory Karatsuba.Abstract_Representations
21:29:17Schoenhage_Strassen: theory Karatsuba.Abstract_Representations_2
21:29:17Schoenhage_Strassen: theory Karatsuba.Estimation_Method
21:29:17Schoenhage_Strassen: theory Landau_Symbols.Group_Sort
21:29:18Schoenhage_Strassen: theory Polynomial_Interpolation.Ring_Hom
21:29:18Schoenhage_Strassen: theory HOL-Algebra.Lattice
21:29:18Schoenhage_Strassen: theory Root_Balanced_Tree.Time_Monad
21:29:18Schoenhage_Strassen: theory Subresultants.Binary_Exponentiation
21:29:19Schoenhage_Strassen: theory Karatsuba.Time_Monad_Extended
21:29:20Schoenhage_Strassen: theory HOL-Algebra.Complete_Lattice
21:29:20Schoenhage_Strassen: theory Karatsuba.Main_TM
21:29:20Schoenhage_Strassen: theory Landau_Symbols.Landau_Real_Products
21:29:21Schoenhage_Strassen: theory HOL-Algebra.Group
21:29:24Schoenhage_Strassen: theory HOL-Algebra.Coset
21:29:24Schoenhage_Strassen: theory HOL-Algebra.FiniteProduct
21:29:24Schoenhage_Strassen: theory Landau_Symbols.Landau_Simprocs
21:29:25Schoenhage_Strassen: theory HOL-Algebra.Ring
21:29:25Schoenhage_Strassen: theory Landau_Symbols.Landau_More
21:29:25Schoenhage_Strassen: theory Akra_Bazzi.Akra_Bazzi_Library
21:29:26Schoenhage_Strassen: theory Akra_Bazzi.Akra_Bazzi_Asymptotics
21:29:27Schoenhage_Strassen: theory HOL-Algebra.Generated_Groups
21:29:27Schoenhage_Strassen: theory HOL-Algebra.Divisibility
21:29:27Schoenhage_Strassen: theory Akra_Bazzi.Akra_Bazzi_Real
21:29:29Schoenhage_Strassen: theory HOL-Algebra.Elementary_Groups
21:29:30Schoenhage_Strassen: theory Akra_Bazzi.Akra_Bazzi
21:29:30Schoenhage_Strassen: theory Word_Lib.Bit_Comprehension
21:29:31Schoenhage_Strassen: theory HOL-Computational_Algebra.Polynomial_Factorial
21:29:31Schoenhage_Strassen: theory Akra_Bazzi.Master_Theorem
21:29:31Schoenhage_Strassen: theory HOL-Algebra.AbelCoset
21:29:31Schoenhage_Strassen: theory HOL-Algebra.Module
21:29:32Schoenhage_Strassen: theory Akra_Bazzi.Akra_Bazzi_Method
21:29:32Schoenhage_Strassen: theory Polynomial_Interpolation.Missing_Polynomial
21:29:34Schoenhage_Strassen: theory Karatsuba.Karatsuba_Runtime_Lemmas
21:29:34Schoenhage_Strassen: theory Polynomial_Interpolation.Ring_Hom_Poly
21:29:36Schoenhage_Strassen: theory HOL-Algebra.Ideal
21:29:40Schoenhage_Strassen: theory HOL-Algebra.Ideal_Product
21:29:40Schoenhage_Strassen: theory HOL-Algebra.RingHom
21:29:41Schoenhage_Strassen: theory HOL-Algebra.QuotRing
21:29:41Schoenhage_Strassen: theory HOL-Algebra.UnivPoly
21:29:46Schoenhage_Strassen: theory HOL-Algebra.IntRing
21:29:46Schoenhage_Strassen: theory HOL-Algebra.Weak_Morphisms
21:29:47Schoenhage_Strassen: theory HOL-Algebra.Chinese_Remainder
21:29:58Schoenhage_Strassen: theory HOL-Algebra.Multiplicative_Group
21:30:03Schoenhage_Strassen: theory HOL-Algebra.Ring_Divisibility
21:30:03Schoenhage_Strassen: theory HOL-Algebra.Subrings
21:30:03Schoenhage_Strassen: theory Schoenhage_Strassen.Schoenhage_Strassen_Ring_Lemmas
21:30:03Schoenhage_Strassen: theory HOL-Number_Theory.Residues
21:30:07Schoenhage_Strassen: theory HOL-Algebra.Embedded_Algebras
21:30:07Schoenhage_Strassen: theory HOL-Number_Theory.Euler_Criterion
21:30:07Schoenhage_Strassen: theory HOL-Number_Theory.Pocklington
21:30:07Schoenhage_Strassen: theory HOL-Number_Theory.Gauss
21:30:08Schoenhage_Strassen: theory HOL-Number_Theory.Residue_Primitive_Roots
21:30:08Schoenhage_Strassen: theory HOL-Number_Theory.Quadratic_Reciprocity
21:30:08Schoenhage_Strassen: theory Karatsuba.Karatsuba_Preliminaries
21:30:08Schoenhage_Strassen: theory Berlekamp_Zassenhaus.Finite_Field
21:30:08Schoenhage_Strassen: theory HOL-Number_Theory.Number_Theory
21:30:11Schoenhage_Strassen: theory Karatsuba.Karatsuba_Sum_Lemmas
21:30:11Schoenhage_Strassen: theory Number_Theoretic_Transform.Preliminary_Lemmas
21:30:12Schoenhage_Strassen: theory Number_Theoretic_Transform.NTT
21:30:12Schoenhage_Strassen: theory Karatsuba.Monoid_Sums
21:30:12Schoenhage_Strassen: theory Karatsuba.Nat_LSBF
21:30:13Schoenhage_Strassen: theory Number_Theoretic_Transform.Butterfly
21:30:13Schoenhage_Strassen: theory HOL-Algebra.Polynomials
21:30:16Schoenhage_Strassen: theory Karatsuba.Int_LSBF
21:30:16Schoenhage_Strassen: theory Karatsuba.Nat_LSBF_TM
21:30:17Schoenhage_Strassen: theory Schoenhage_Strassen.Schoenhage_Strassen_Preliminaries
21:30:17Schoenhage_Strassen: theory Schoenhage_Strassen.NTT_Rings
21:30:18Schoenhage_Strassen: theory Karatsuba.Karatsuba
21:30:22Schoenhage_Strassen: theory Karatsuba.Karatsuba_TM
21:30:22Schoenhage_Strassen: theory Schoenhage_Strassen.Schoenhage_Strassen_Runtime_Preliminaries
21:30:28Schoenhage_Strassen: theory Schoenhage_Strassen.FNTT_Rings
21:30:32Schoenhage_Strassen: theory HOL-Algebra.Polynomial_Divisibility
21:31:04Schoenhage_Strassen: theory Finite_Fields.Finite_Fields_Preliminary_Results
21:31:12Schoenhage_Strassen: theory Finite_Fields.Finite_Fields_Factorization_Ext
21:31:12Schoenhage_Strassen: theory Finite_Fields.Ring_Characteristic
21:31:32Schoenhage_Strassen: theory Schoenhage_Strassen.Z_mod_power_of_2
21:31:37Schoenhage_Strassen: theory Schoenhage_Strassen.Z_mod_power_of_2_TM
21:31:37Schoenhage_Strassen: theory Schoenhage_Strassen.Z_mod_Fermat
21:31:59Schoenhage_Strassen: theory Schoenhage_Strassen.Schoenhage_Strassen
21:31:59Schoenhage_Strassen: theory Schoenhage_Strassen.Z_mod_Fermat_TM
21:32:48Schoenhage_Strassen: theory Schoenhage_Strassen.Schoenhage_Strassen_TM
21:33:53Preparing Schoenhage_Strassen/document ...
21:34:07Finished Schoenhage_Strassen/document (0:00:14 elapsed time)
21:34:07Preparing Schoenhage_Strassen/outline ...
21:34:13Finished Schoenhage_Strassen/outline (0:00:05 elapsed time)
21:34:13Timing Schoenhage_Strassen (8 threads, 271.503s elapsed time, 1536.155s cpu time, 123.807s GC time, factor 5.66)
21:34:13Finished Schoenhage_Strassen (0:04:36 elapsed time, 0:25:51 cpu time, factor 5.61)
21:34:13Running Virtual_Substitution (on hpcisabelle/1) ...
21:34:18Virtual_Substitution: theory Deriving.Generator_Aux
21:34:18Virtual_Substitution: theory Deriving.Derive_Manager
21:34:18Virtual_Substitution: theory HOL-Library.AList
21:34:18Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat
21:34:18Virtual_Substitution: theory HOL-Library.Conditional_Parametricity
21:34:18Virtual_Substitution: theory HOL-Library.Code_Target_Int
21:34:18Virtual_Substitution: theory HOL-Library.Fun_Lexorder
21:34:18Virtual_Substitution: theory HOL-Library.Function_Algebras
21:34:18Virtual_Substitution: theory HOL-Library.Groups_Big_Fun
21:34:18Virtual_Substitution: theory Abstract-Rewriting.Seq
21:34:18Virtual_Substitution: theory HOL-Library.Code_Target_Nat
21:34:18Virtual_Substitution: theory HOL-Library.More_List
21:34:18Virtual_Substitution: theory HOL-Library.Sublist
21:34:18Virtual_Substitution: theory HOL-Library.While_Combinator
21:34:19Virtual_Substitution: theory HOL-Library.Ramsey
21:34:19Virtual_Substitution: theory HOL-Library.FSet
21:34:19Virtual_Substitution: theory HOL-Library.Poly_Mapping
21:34:19Virtual_Substitution: theory Polynomials.More_Modules
21:34:19Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial
21:34:19Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant
21:34:20Virtual_Substitution: theory Matrix.Utility
21:34:20Virtual_Substitution: theory Open_Induction.Restricted_Predicates
21:34:20Virtual_Substitution: theory Regular-Sets.Regular_Set
21:34:20Virtual_Substitution: theory Show.Show
21:34:20Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences
21:34:20Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum
21:34:21Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements
21:34:22Virtual_Substitution: theory Polynomials.MPoly_Type
21:34:22Virtual_Substitution: theory Show.Show_Instances
21:34:22Virtual_Substitution: theory Polynomials.More_MPoly_Type
21:34:23Virtual_Substitution: theory Show.Shows_Literal
21:34:24Virtual_Substitution: theory HOL-Library.Finite_Map
21:34:24Virtual_Substitution: theory Show.Show_Real
21:34:25Virtual_Substitution: theory Regular-Sets.Regular_Exp
21:34:29Virtual_Substitution: theory Regular-Sets.NDerivative
21:34:29Virtual_Substitution: theory Regular-Sets.Relation_Interpretation
21:34:31Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate
21:34:33Virtual_Substitution: theory Regular-Sets.Equivalence_Checking
21:34:34Virtual_Substitution: theory Regular-Sets.Regexp_Method
21:34:35Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting
21:34:35Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full
21:34:37Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences
21:34:37Virtual_Substitution: theory Abstract-Rewriting.SN_Orders
21:34:37Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations
21:34:38Virtual_Substitution: theory Polynomials.Utils
21:34:38Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders
21:34:38Virtual_Substitution: theory Polynomials.Power_Products
21:34:39Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map
21:34:40Virtual_Substitution: theory Polynomials.Polynomials
21:34:48Virtual_Substitution: theory Polynomials.Show_Polynomials
21:34:57Virtual_Substitution: theory Polynomials.MPoly_Type_Class
21:35:00Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered
21:35:16Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap
21:35:19Virtual_Substitution: theory Virtual_Substitution.MPolyExtension
21:35:21Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps
21:35:22Virtual_Substitution: theory Virtual_Substitution.PolyAtoms
21:35:28Virtual_Substitution: theory Virtual_Substitution.Debruijn
21:35:31Virtual_Substitution: theory Virtual_Substitution.Optimizations
21:35:39Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs
21:35:39Virtual_Substitution: theory Virtual_Substitution.Reindex
21:35:40Virtual_Substitution: theory Virtual_Substitution.UniAtoms
21:35:47Virtual_Substitution: theory Virtual_Substitution.VSAlgos
21:35:56Virtual_Substitution: theory Virtual_Substitution.QE
21:35:56Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting
21:35:59Virtual_Substitution: theory Virtual_Substitution.DNF
21:35:59Virtual_Substitution: theory Virtual_Substitution.Heuristic
21:35:59Virtual_Substitution: theory Virtual_Substitution.LinearCase
21:35:59Virtual_Substitution: theory Virtual_Substitution.NegInfinity
21:35:59Virtual_Substitution: theory Virtual_Substitution.QuadraticCase
21:36:00Virtual_Substitution: theory Virtual_Substitution.EliminateVariable
21:36:01Virtual_Substitution: theory Virtual_Substitution.Infinitesimals
21:36:01Virtual_Substitution: theory Virtual_Substitution.LuckyFind
21:36:02Virtual_Substitution: theory Virtual_Substitution.EqualityVS
21:36:06Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni
21:36:08Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni
21:36:09Virtual_Substitution: theory Virtual_Substitution.Exports
21:36:10Virtual_Substitution: theory Virtual_Substitution.DNFUni
21:36:11Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs
21:36:13Virtual_Substitution: theory Virtual_Substitution.VSQuad
21:36:15Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs
21:36:17Virtual_Substitution: theory Virtual_Substitution.ExportProofs
21:38:43Preparing Virtual_Substitution/document ...
21:39:28Finished Virtual_Substitution/document (0:00:45 elapsed time)
21:39:28Preparing Virtual_Substitution/outline ...
21:39:42Finished Virtual_Substitution/outline (0:00:13 elapsed time)
21:39:42Timing Virtual_Substitution (8 threads, 261.172s elapsed time, 1305.687s cpu time, 90.664s GC time, factor 5.00)
21:39:42Finished Virtual_Substitution (0:04:25 elapsed time, 0:21:57 cpu time, factor 4.96)
21:39:42Running MFODL_Monitor_Optimized (on hpcisabelle/2) ...
21:39:45MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach
21:39:45MFODL_Monitor_Optimized: theory Word_Lib.Signed_Words
21:39:45MFODL_Monitor_Optimized: theory Word_Lib.Type_Syntax
21:39:45MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Regex
21:39:45MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join
21:39:45MFODL_Monitor_Optimized: theory Word_Lib.Even_More_List
21:39:45MFODL_Monitor_Optimized: theory Word_Lib.Enumeration
21:39:45MFODL_Monitor_Optimized: theory Word_Lib.Aligned
21:39:46MFODL_Monitor_Optimized: theory Word_Lib.Enumeration_Word
21:39:46MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach_Tools
21:39:46MFODL_Monitor_Optimized: theory Word_Lib.Word_EqI
21:39:49MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join_Correctness
21:39:50MFODL_Monitor_Optimized: theory Word_Lib.Boolean_Inequalities
21:39:50MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_Join
21:39:53MFODL_Monitor_Optimized: theory Word_Lib.Word_Lemmas
21:39:56MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE
21:39:59MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE_Properties
21:40:00MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Code_Double
21:40:03MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Event_Data
21:40:06MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Formula
21:40:43MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor
21:41:31MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_MTL
21:41:47MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Impl
21:43:19MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Code
21:44:03Preparing MFODL_Monitor_Optimized/document ...
21:44:18Finished MFODL_Monitor_Optimized/document (0:00:14 elapsed time)
21:44:18Preparing MFODL_Monitor_Optimized/outline ...
21:44:26Finished MFODL_Monitor_Optimized/outline (0:00:07 elapsed time)
21:44:26Timing MFODL_Monitor_Optimized (8 threads, 254.938s elapsed time, 1286.021s cpu time, 21.987s GC time, factor 5.04)
21:44:26Finished MFODL_Monitor_Optimized (0:04:19 elapsed time, 0:21:36 cpu time, factor 5.00)
21:44:26Building Flow_Networks (on hpcisabelle/3) ...
21:44:29Flow_Networks: theory Flow_Networks.Graph
21:44:29Flow_Networks: theory CAVA_Base.Statistics
21:44:29Flow_Networks: theory HOL-Library.Omega_Words_Fun
21:44:29Flow_Networks: theory DFS_Framework.DFS_Framework_Misc
21:44:29Flow_Networks: theory Program-Conflict-Analysis.LTS
21:44:29Flow_Networks: theory CAVA_Base.Code_String
21:44:29Flow_Networks: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
21:44:29Flow_Networks: theory DFS_Framework.DFS_Framework_Refine_Aux
21:44:29Flow_Networks: theory CAVA_Base.CAVA_Code_Target
21:44:29Flow_Networks: theory CAVA_Base.CAVA_Base
21:44:30Flow_Networks: theory Flow_Networks.Fofu_Abs_Base
21:44:30Flow_Networks: theory CAVA_Automata.Digraph_Basic
21:44:31Flow_Networks: theory DFS_Framework.Impl_Rev_Array_Stack
21:44:31Flow_Networks: theory CAVA_Automata.Digraph
21:44:32Flow_Networks: theory Flow_Networks.Fofu_Impl_Base
21:44:33Flow_Networks: theory CAVA_Automata.Digraph_Impl
21:44:33Flow_Networks: theory DFS_Framework.Param_DFS
21:44:36Flow_Networks: theory Flow_Networks.Refine_Add_Fofu
21:44:38Flow_Networks: theory DFS_Framework.DFS_Invars_Basic
21:44:39Flow_Networks: theory DFS_Framework.General_DFS_Structure
21:44:46Flow_Networks: theory DFS_Framework.Rec_Impl
21:44:46Flow_Networks: theory DFS_Framework.Tailrec_Impl
21:44:54Flow_Networks: theory DFS_Framework.Simple_Impl
21:45:02Flow_Networks: theory DFS_Framework.Restr_Impl
21:45:05Flow_Networks: theory DFS_Framework.DFS_Framework
21:45:05Flow_Networks: theory DFS_Framework.Reachable_Nodes
21:45:53Flow_Networks: theory Flow_Networks.Network
21:45:55Flow_Networks: theory Flow_Networks.Residual_Graph
21:45:57Flow_Networks: theory Flow_Networks.Augmenting_Flow
21:45:57Flow_Networks: theory Flow_Networks.Augmenting_Path
21:45:58Flow_Networks: theory Flow_Networks.Ford_Fulkerson
21:46:00Flow_Networks: theory Flow_Networks.Graph_Impl
21:46:00Flow_Networks: theory Flow_Networks.Network_Impl
21:46:01Flow_Networks: theory Flow_Networks.NetCheck
21:46:56Preparing Flow_Networks/document ...
21:47:00Finished Flow_Networks/document (0:00:03 elapsed time)
21:47:00Preparing Flow_Networks/outline ...
21:47:03Finished Flow_Networks/outline (0:00:02 elapsed time)
21:47:03Timing Flow_Networks (8 threads, 125.949s elapsed time, 432.243s cpu time, 18.330s GC time, factor 3.43)
21:47:03Finished Flow_Networks (0:02:29 elapsed time, 0:07:59 cpu time, factor 3.22)
21:47:03Building Distributed_Distinct_Elements (on hpcisabelle/4) ...
21:47:07Distributed_Distinct_Elements: theory Flow_Networks.Graph
21:47:07Distributed_Distinct_Elements: theory HOL-Combinatorics.Stirling
21:47:07Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
21:47:07Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
21:47:07Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
21:47:07Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
21:47:07Distributed_Distinct_Elements: theory HOL-Number_Theory.Cong
21:47:07Distributed_Distinct_Elements: theory HOL-Library.Case_Converter
21:47:08Distributed_Distinct_Elements: theory HOL-Algebra.IntRing
21:47:08Distributed_Distinct_Elements: theory HOL-Library.List_Lexorder
21:47:08Distributed_Distinct_Elements: theory HOL-Library.Code_Lazy
21:47:08Distributed_Distinct_Elements: theory HOL-Library.Power_By_Squaring
21:47:08Distributed_Distinct_Elements: theory HOL-Library.Transitive_Closure_Table
21:47:08Distributed_Distinct_Elements: theory HOL-Library.Bourbaki_Witt_Fixpoint
21:47:08Distributed_Distinct_Elements: theory HOL-Number_Theory.Eratosthenes
21:47:08Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
21:47:09Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Preliminary_Results
21:47:09Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
21:47:09Distributed_Distinct_Elements: theory HOL-Library.Going_To_Filter
21:47:09Distributed_Distinct_Elements: theory Frequency_Moments.Landau_Ext
21:47:09Distributed_Distinct_Elements: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
21:47:10Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Tau_Additivity
21:47:10Distributed_Distinct_Elements: theory HOL-Number_Theory.Fib
21:47:10Distributed_Distinct_Elements: theory HOL-Number_Theory.Mod_Exp
21:47:10Distributed_Distinct_Elements: theory HOL-Number_Theory.Prime_Powers
21:47:10Distributed_Distinct_Elements: theory Flow_Networks.Network
21:47:10Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
21:47:10Distributed_Distinct_Elements: theory HOL-Number_Theory.Totient
21:47:10Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Contour_Integration
21:47:10Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_More_PMF
21:47:11Distributed_Distinct_Elements: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
21:47:11Distributed_Distinct_Elements: theory HOL-Number_Theory.Residues
21:47:11Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Coin_Space
21:47:12Distributed_Distinct_Elements: theory Flow_Networks.Residual_Graph
21:47:13Distributed_Distinct_Elements: theory MFMC_Countable.MFMC_Misc
21:47:13Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
21:47:14Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Winding_Numbers
21:47:14Distributed_Distinct_Elements: theory Median_Method.Median
21:47:15Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
21:47:15Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
21:47:15Distributed_Distinct_Elements: theory Concentration_Inequalities.Bienaymes_Identity
21:47:15Distributed_Distinct_Elements: theory HOL-Number_Theory.Euler_Criterion
21:47:15Distributed_Distinct_Elements: theory Flow_Networks.Augmenting_Flow
21:47:16Distributed_Distinct_Elements: theory Flow_Networks.Augmenting_Path
21:47:16Distributed_Distinct_Elements: theory HOL-Number_Theory.Gauss
21:47:16Distributed_Distinct_Elements: theory HOL-Number_Theory.Pocklington
21:47:16Distributed_Distinct_Elements: theory Flow_Networks.Ford_Fulkerson
21:47:16Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
21:47:16Distributed_Distinct_Elements: theory HOL-Number_Theory.Quadratic_Reciprocity
21:47:17Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Conformal_Mappings
21:47:17Distributed_Distinct_Elements: theory HOL-Number_Theory.Residue_Primitive_Roots
21:47:17Distributed_Distinct_Elements: theory Lehmer.Lehmer
21:47:17Distributed_Distinct_Elements: theory Pratt_Certificate.Pratt_Certificate
21:47:17Distributed_Distinct_Elements: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
21:47:17Distributed_Distinct_Elements: theory HOL-Number_Theory.Number_Theory
21:47:18Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Singularities
21:47:18Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Great_Picard
21:47:18Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Factorization_Ext
21:47:18Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
21:47:19Distributed_Distinct_Elements: theory Finite_Fields.Ring_Characteristic
21:47:19Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Riemann_Mapping
21:47:19Distributed_Distinct_Elements: theory MFMC_Countable.MFMC_Finite
21:47:20Distributed_Distinct_Elements: theory MFMC_Countable.Matrix_For_Marginals
21:47:20Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
21:47:20Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Residues
21:47:20Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
21:47:21Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Residue_Theorem
21:47:21Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
21:47:21Distributed_Distinct_Elements: theory Dirichlet_Series.Euler_Products
21:47:21Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Laurent_Convergence
21:47:21Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
21:47:21Distributed_Distinct_Elements: theory Bertrands_Postulate.Bertrand
21:47:22Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
21:47:23Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
21:47:23Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
21:47:24Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Meromorphic
21:47:24Distributed_Distinct_Elements: theory MFMC_Countable.Rel_PMF_Characterisation
21:47:24Distributed_Distinct_Elements: theory Probabilistic_While.While_SPMF
21:47:25Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
21:47:25Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Weierstrass_Factorization
21:47:25Distributed_Distinct_Elements: theory Dirichlet_Series.More_Totient
21:47:25Distributed_Distinct_Elements: theory Dirichlet_Series.Liouville_Lambda
21:47:25Distributed_Distinct_Elements: theory Dirichlet_Series.Divisor_Count
21:47:26Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Analysis
21:47:26Distributed_Distinct_Elements: theory Dirichlet_Series.Arithmetic_Summatory
21:47:26Distributed_Distinct_Elements: theory Dirichlet_Series.Partial_Summation
21:47:26Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
21:47:26Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
21:47:26Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series_Analysis
21:47:27Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
21:47:33Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
21:47:36Distributed_Distinct_Elements: theory Zeta_Function.Zeta_Library
21:47:36Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
21:47:40Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
21:47:40Distributed_Distinct_Elements: theory Finite_Fields.Rabin_Irreducibility_Test
21:47:40Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
21:47:40Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Randomized_Algorithm
21:47:41Distributed_Distinct_Elements: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
21:47:42Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
21:47:45Distributed_Distinct_Elements: theory Finite_Fields.Rabin_Irreducibility_Test_Code
21:47:48Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
21:47:48Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
21:47:49Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
21:47:58Distributed_Distinct_Elements: theory Finite_Fields.Find_Irreducible_Poly
21:48:05Distributed_Distinct_Elements: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
21:48:09Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
21:48:22Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
21:48:29Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
21:48:30Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
21:48:33Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
21:51:08Preparing Distributed_Distinct_Elements/document ...
21:51:19Finished Distributed_Distinct_Elements/document (0:00:10 elapsed time)
21:51:19Preparing Distributed_Distinct_Elements/outline ...
21:51:22Finished Distributed_Distinct_Elements/outline (0:00:03 elapsed time)
21:51:23Timing Distributed_Distinct_Elements (8 threads, 198.751s elapsed time, 1419.435s cpu time, 83.755s GC time, factor 7.14)
21:51:23Finished Distributed_Distinct_Elements (0:03:59 elapsed time, 0:25:07 cpu time, factor 6.29)
21:51:23Building AutoCorres2_Main (on hpcisabelle/5) ...
21:51:25AutoCorres2_Main: theory AutoCorres2.MkTermAntiquote
21:51:25AutoCorres2_Main: theory AutoCorres2.TermPatternAntiquote
21:51:25AutoCorres2_Main: theory AutoCorres2.ML_Fun_Cache
21:51:25AutoCorres2_Main: theory HOL-Eisbach.Eisbach
21:51:25AutoCorres2_Main: theory AutoCorres2.ML_Infer_Instantiate
21:51:25AutoCorres2_Main: theory AutoCorres2.Introduction_AutoCorres2
21:51:25AutoCorres2_Main: theory AutoCorres2.ML_Record_Antiquotation
21:51:25AutoCorres2_Main: theory AutoCorres2.MapExtra
21:51:25AutoCorres2_Main: theory AutoCorres2.Misc_Antiquotation
21:51:25AutoCorres2_Main: theory AutoCorres2.Named_Rules
21:51:25AutoCorres2_Main: theory AutoCorres2.Padding
21:51:25AutoCorres2_Main: theory AutoCorres2.Print_Annotated
21:51:25AutoCorres2_Main: theory AutoCorres2.StaticFun
21:51:25AutoCorres2_Main: theory AutoCorres2.Subgoals
21:51:25AutoCorres2_Main: theory AutoCorres2.AutoCorres_Utils
21:51:25AutoCorres2_Main: theory AutoCorres2.Option_Scanner
21:51:25AutoCorres2_Main: theory AutoCorres2.Target_Architecture
21:51:25AutoCorres2_Main: theory AutoCorres2.Tuple_Tools
21:51:25AutoCorres2_Main: theory HOL-Library.Adhoc_Overloading
21:51:25AutoCorres2_Main: theory HOL-Library.Code_Abstract_Nat
21:51:26AutoCorres2_Main: theory HOL-Library.Code_Binary_Nat
21:51:26AutoCorres2_Main: theory HOL-Library.Monad_Syntax
21:51:26AutoCorres2_Main: theory HOL-Library.Complete_Partial_Order2
21:51:26AutoCorres2_Main: theory AutoCorres2.Less_Monad_Syntax
21:51:26AutoCorres2_Main: theory HOL-Library.Phantom_Type
21:51:26AutoCorres2_Main: theory AutoCorres2.MapExtraTrans
21:51:26AutoCorres2_Main: theory HOL-Library.Signed_Division
21:51:26AutoCorres2_Main: theory HOL-Library.Sublist
21:51:27AutoCorres2_Main: theory HOL-Eisbach.Eisbach_Tools
21:51:27AutoCorres2_Main: theory AutoCorres2.Cong_Tactic
21:51:27AutoCorres2_Main: theory AutoCorres2.Tagging
21:51:28AutoCorres2_Main: theory AutoCorres2.Match_Cterm
21:51:28AutoCorres2_Main: theory AutoCorres2.Simp_Trace
21:51:29AutoCorres2_Main: theory AutoCorres2.PrettyProgs
21:51:29AutoCorres2_Main: theory HOL-Library.Cardinality
21:51:29AutoCorres2_Main: theory Word_Lib.Enumeration
21:51:29AutoCorres2_Main: theory AutoCorres2.IndirectCalls
21:51:29AutoCorres2_Main: theory Word_Lib.Even_More_List
21:51:30AutoCorres2_Main: theory Word_Lib.More_Bit_Ring
21:51:30AutoCorres2_Main: theory Word_Lib.More_Misc
21:51:30AutoCorres2_Main: theory AutoCorres2.Basic_Runs_To_VCG
21:51:30AutoCorres2_Main: theory HOL-Library.Numeral_Type
21:51:31AutoCorres2_Main: theory HOL-Library.Prefix_Order
21:51:31AutoCorres2_Main: theory Word_Lib.More_Sublist
21:51:31AutoCorres2_Main: theory AutoCorres2.Arrays
21:51:31AutoCorres2_Main: theory HOL-Library.Type_Length
21:51:31AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG
21:51:32AutoCorres2_Main: theory HOL-Library.Word
21:51:32AutoCorres2_Main: theory Word_Lib.More_Arithmetic
21:51:32AutoCorres2_Main: theory AutoCorres2.Mutual_CCPO_Recursion
21:51:32AutoCorres2_Main: theory AutoCorres2.Spec_Monad
21:51:39AutoCorres2_Main: theory AutoCorres2.Synthesize
21:51:43AutoCorres2_Main: theory Word_Lib.Bit_Comprehension
21:51:43AutoCorres2_Main: theory Word_Lib.Hex_Words
21:51:43AutoCorres2_Main: theory Word_Lib.Legacy_Aliases
21:51:43AutoCorres2_Main: theory Word_Lib.More_Divides
21:51:43AutoCorres2_Main: theory Word_Lib.Signed_Words
21:51:43AutoCorres2_Main: theory Word_Lib.Syntax_Bundles
21:51:43AutoCorres2_Main: theory Word_Lib.Type_Syntax
21:51:43AutoCorres2_Main: theory Word_Lib.Word_Syntax
21:51:44AutoCorres2_Main: theory Word_Lib.Norm_Words
21:51:44AutoCorres2_Main: theory Word_Lib.Word_Names
21:51:44AutoCorres2_Main: theory Word_Lib.Signed_Division_Word
21:51:44AutoCorres2_Main: theory Word_Lib.More_Word
21:51:44AutoCorres2_Main: theory AutoCorres2.Reaches
21:51:45AutoCorres2_Main: theory Word_Lib.Bit_Comprehension_Int
21:51:46AutoCorres2_Main: theory Word_Lib.Bit_Shifts_Infix_Syntax
21:51:46AutoCorres2_Main: theory Word_Lib.Enumeration_Word
21:51:46AutoCorres2_Main: theory Word_Lib.Least_significant_bit
21:51:46AutoCorres2_Main: theory Word_Lib.Many_More
21:51:46AutoCorres2_Main: theory Word_Lib.Strict_part_mono
21:51:46AutoCorres2_Main: theory Word_Lib.Word_16
21:51:46AutoCorres2_Main: theory AutoCorres2.Distinct_Prop
21:51:47AutoCorres2_Main: theory AutoCorres2.Lens
21:51:47AutoCorres2_Main: theory Word_Lib.Aligned
21:51:47AutoCorres2_Main: theory Word_Lib.Singleton_Bit_Shifts
21:51:47AutoCorres2_Main: theory Word_Lib.Most_significant_bit
21:51:48AutoCorres2_Main: theory Word_Lib.Generic_set_bit
21:51:48AutoCorres2_Main: theory Word_Lib.Sgn_Abs
21:51:48AutoCorres2_Main: theory Word_Lib.Next_and_Prev
21:51:48AutoCorres2_Main: theory Word_Lib.Word_EqI
21:51:49AutoCorres2_Main: theory Word_Lib.Bits_Int
21:51:52AutoCorres2_Main: theory Word_Lib.Boolean_Inequalities
21:51:53AutoCorres2_Main: theory Word_Lib.Rsplit
21:51:53AutoCorres2_Main: theory Word_Lib.Typedef_Morphisms
21:51:54AutoCorres2_Main: theory Word_Lib.Reversed_Bit_Lists
21:51:55AutoCorres2_Main: theory Word_Lib.Word_Lemmas
21:51:58AutoCorres2_Main: theory Word_Lib.Bitwise
21:51:58AutoCorres2_Main: theory Word_Lib.Bitwise_Signed
21:51:58AutoCorres2_Main: theory Word_Lib.Word_8
21:51:58AutoCorres2_Main: theory Word_Lib.More_Word_Operations
21:52:00AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_Internal
21:52:00AutoCorres2_Main: theory Word_Lib.Word_32
21:52:00AutoCorres2_Main: theory Word_Lib.Word_64
21:52:01AutoCorres2_Main: theory Word_Lib.Machine_Word_64_Basics
21:52:01AutoCorres2_Main: theory Word_Lib.Machine_Word_64
21:52:01AutoCorres2_Main: theory Word_Lib.Machine_Word_32_Basics
21:52:01AutoCorres2_Main: theory Word_Lib.Word_Lib_Sumo
21:52:01AutoCorres2_Main: theory Word_Lib.Machine_Word_32
21:52:04AutoCorres2_Main: theory AutoCorres2.More_Lib
21:52:04AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_32_Internal
21:52:04AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_64_Internal
21:52:05AutoCorres2_Main: theory AutoCorres2.WordSetup
21:52:05AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM
21:52:05AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM64
21:52:05AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM_HYP
21:52:06AutoCorres2_Main: theory AutoCorres2.Addr_Type_RISCV64
21:52:06AutoCorres2_Main: theory AutoCorres2.Addr_Type_X64
21:52:06AutoCorres2_Main: theory AutoCorres2.Addr_Type
21:52:07AutoCorres2_Main: theory AutoCorres2.NatBitwise
21:52:07AutoCorres2_Main: theory AutoCorres2.Reader_Monad
21:52:08AutoCorres2_Main: theory AutoCorres2.CTypesBase
21:52:08AutoCorres2_Main: theory AutoCorres2.Option_MonadND
21:52:10AutoCorres2_Main: theory AutoCorres2.CTypesDefs
21:52:25AutoCorres2_Main: theory AutoCorres2.CTypes
21:52:29AutoCorres2_Main: theory AutoCorres2.HeapRawState
21:52:29AutoCorres2_Main: theory AutoCorres2.Vanilla32_Preliminaries
21:52:29AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM
21:52:29AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM64
21:52:30AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
21:52:30AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_RISCV64
21:52:30AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_X64
21:52:30AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding
21:52:30AutoCorres2_Main: theory AutoCorres2.Vanilla32
21:52:32AutoCorres2_Main: theory AutoCorres2.CompoundCTypes
21:52:37AutoCorres2_Main: theory AutoCorres2.ArraysMemInstance
21:52:39AutoCorres2_Main: theory AutoCorres2.ArchArraysMemInstance
21:52:41AutoCorres2_Main: theory AutoCorres2.TypHeap
21:52:49AutoCorres2_Main: theory AutoCorres2.Separation_UMM
21:52:50AutoCorres2_Main: theory AutoCorres2.SepCode
21:52:52AutoCorres2_Main: theory AutoCorres2.SepInv
21:52:54AutoCorres2_Main: theory AutoCorres2.SepTactic
21:52:54AutoCorres2_Main: theory AutoCorres2.SepFrame
21:52:56AutoCorres2_Main: theory AutoCorres2.StructSupport
21:52:57AutoCorres2_Main: theory AutoCorres2.ArrayAssertion
21:52:58AutoCorres2_Main: theory AutoCorres2.CProof
21:53:07AutoCorres2_Main: theory AutoCorres2.CLanguage
21:53:07AutoCorres2_Main: theory AutoCorres2.Padding_Equivalence
21:53:07AutoCorres2_Main: theory AutoCorres2.PackedTypes
21:53:14AutoCorres2_Main: theory AutoCorres2.ModifiesProofs
21:53:17AutoCorres2_Main: theory AutoCorres2.UMM
21:53:25AutoCorres2_Main: theory AutoCorres2.CLocals
21:53:29AutoCorres2_Main: theory AutoCorres2.CTranslationSetup
21:53:58AutoCorres2_Main: theory AutoCorres2.Array_Selectors
21:53:58AutoCorres2_Main: theory AutoCorres2.CTranslation
21:53:59AutoCorres2_Main: theory AutoCorres2.TypHeapLib
21:54:00AutoCorres2_Main: theory AutoCorres2.AbstractArrays
21:54:00AutoCorres2_Main: theory AutoCorres2.LemmaBucket_C
21:54:00AutoCorres2_Main: theory AutoCorres2.AutoCorres_Base
21:54:04AutoCorres2_Main: theory AutoCorres2.SimplBucket
21:54:04AutoCorres2_Main: theory AutoCorres2.TypHeapSimple
21:54:05AutoCorres2_Main: theory AutoCorres2.AutoCorresSimpset
21:54:05AutoCorres2_Main: theory AutoCorres2.CCorresE
21:54:06AutoCorres2_Main: theory AutoCorres2.CorresXF
21:54:06AutoCorres2_Main: theory AutoCorres2.L1Defs
21:54:09AutoCorres2_Main: theory AutoCorres2.L1Peephole
21:54:09AutoCorres2_Main: theory AutoCorres2.L1Valid
21:54:10AutoCorres2_Main: theory AutoCorres2.ExceptionRewrite
21:54:10AutoCorres2_Main: theory AutoCorres2.SimplConv
21:54:10AutoCorres2_Main: theory AutoCorres2.L2Defs
21:54:15AutoCorres2_Main: theory AutoCorres2.Split_Heap
21:54:17AutoCorres2_Main: theory AutoCorres2.L2ExceptionRewrite
21:54:17AutoCorres2_Main: theory AutoCorres2.L2Peephole
21:54:17AutoCorres2_Main: theory AutoCorres2.LocalVarExtract
21:54:18AutoCorres2_Main: theory AutoCorres2.Stack_Typing
21:54:18AutoCorres2_Main: theory AutoCorres2.WordAbstract
21:54:20AutoCorres2_Main: theory AutoCorres2.Refines_Spec
21:54:20AutoCorres2_Main: theory AutoCorres2.In_Out_Parameters
21:54:22AutoCorres2_Main: theory AutoCorres2.WordPolish
21:54:39AutoCorres2_Main: theory AutoCorres2.HeapLift
21:54:39AutoCorres2_Main: theory AutoCorres2.TypeStrengthen
21:55:03AutoCorres2_Main: theory AutoCorres2.Polish
21:55:03AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG_StackPointer
21:55:12AutoCorres2_Main: theory AutoCorres2.AutoCorres
21:55:39AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Main
21:55:39AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Nondet_Syntax
21:56:49Timing AutoCorres2_Main (8 threads, 263.061s elapsed time, 1786.712s cpu time, 49.318s GC time, factor 6.79)
21:56:49Finished AutoCorres2_Main (0:05:14 elapsed time, 0:31:56 cpu time, factor 6.09)
21:56:49Building HRB-Slicing (on hpcisabelle/6) ...
21:56:51HRB-Slicing: theory HRB-Slicing.AuxLemmas
21:56:51HRB-Slicing: theory HRB-Slicing.BasicDefs
21:56:53HRB-Slicing: theory HRB-Slicing.Com
21:56:53HRB-Slicing: theory HRB-Slicing.CFG
21:56:53HRB-Slicing: theory HRB-Slicing.JVMCFG
21:56:57HRB-Slicing: theory HRB-Slicing.Labels
21:56:57HRB-Slicing: theory HRB-Slicing.ProcState
21:56:57HRB-Slicing: theory HRB-Slicing.PCFG
21:56:59HRB-Slicing: theory HRB-Slicing.CFGExit
21:56:59HRB-Slicing: theory HRB-Slicing.CFG_wf
21:56:59HRB-Slicing: theory HRB-Slicing.Distance
21:56:59HRB-Slicing: theory HRB-Slicing.ReturnAndCallNodes
21:56:59HRB-Slicing: theory HRB-Slicing.SemanticsCFG
21:57:00HRB-Slicing: theory HRB-Slicing.Observable
21:57:00HRB-Slicing: theory HRB-Slicing.Postdomination
21:57:00HRB-Slicing: theory HRB-Slicing.CFGExit_wf
21:57:00HRB-Slicing: theory HRB-Slicing.WellFormProgs
21:57:01HRB-Slicing: theory HRB-Slicing.JVMInterpretation
21:57:01HRB-Slicing: theory HRB-Slicing.Interpretation
21:57:01HRB-Slicing: theory HRB-Slicing.SDG
21:57:04HRB-Slicing: theory HRB-Slicing.WellFormed
21:57:06HRB-Slicing: theory HRB-Slicing.ValidPaths
21:57:06HRB-Slicing: theory HRB-Slicing.JVMCFG_wf
21:57:07HRB-Slicing: theory HRB-Slicing.JVMPostdomination
21:57:10HRB-Slicing: theory HRB-Slicing.HRBSlice
21:57:10HRB-Slicing: theory HRB-Slicing.ProcSDG
21:57:12HRB-Slicing: theory HRB-Slicing.SCDObservable
21:57:12HRB-Slicing: theory HRB-Slicing.JVMSDG
21:57:13HRB-Slicing: theory HRB-Slicing.Slice
21:57:16HRB-Slicing: theory HRB-Slicing.WeakSimulation
21:57:19HRB-Slicing: theory HRB-Slicing.FundamentalProperty
21:57:24HRB-Slicing: theory HRB-Slicing.HRBSlicing
22:01:24Preparing HRB-Slicing/document ...
22:01:52Finished HRB-Slicing/document (0:00:28 elapsed time)
22:01:52Preparing HRB-Slicing/outline ...
22:01:59Finished HRB-Slicing/outline (0:00:07 elapsed time)
22:01:59Timing HRB-Slicing (8 threads, 238.607s elapsed time, 1303.474s cpu time, 20.855s GC time, factor 5.46)
22:01:59Finished HRB-Slicing (0:04:29 elapsed time, 0:22:54 cpu time, factor 5.09)
22:01:59Building Dirichlet_Series (on hpcisabelle/7) ...
22:02:02Dirichlet_Series: theory HOL-Library.Adhoc_Overloading
22:02:02Dirichlet_Series: theory HOL-Combinatorics.Stirling
22:02:02Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field
22:02:02Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure
22:02:02Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers
22:02:02Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat
22:02:02Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree
22:02:02Dirichlet_Series: theory HOL-Number_Theory.Cong
22:02:03Dirichlet_Series: theory HOL-Library.Code_Target_Nat
22:02:03Dirichlet_Series: theory HOL-Library.Monad_Syntax
22:02:03Dirichlet_Series: theory HOL-Library.Code_Target_Int
22:02:03Dirichlet_Series: theory HOL-Algebra.Congruence
22:02:03Dirichlet_Series: theory HOL-Library.Function_Algebras
22:02:03Dirichlet_Series: theory HOL-Library.Power_By_Squaring
22:02:03Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes
22:02:03Dirichlet_Series: theory Bernoulli.Bernoulli
22:02:03Dirichlet_Series: theory HOL-Library.Code_Target_Numeral
22:02:03Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:02:03Dirichlet_Series: theory HOL-Library.Going_To_Filter
22:02:03Dirichlet_Series: theory HOL-Number_Theory.Fib
22:02:04Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers
22:02:04Dirichlet_Series: theory Landau_Symbols.Group_Sort
22:02:04Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly
22:02:04Dirichlet_Series: theory Matrix.Utility
22:02:04Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction
22:02:05Dirichlet_Series: theory HOL-Algebra.Order
22:02:05Dirichlet_Series: theory Polynomial_Factorization.Missing_List
22:02:05Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp
22:02:05Dirichlet_Series: theory HOL-Number_Theory.Totient
22:02:05Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial
22:02:05Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products
22:02:06Dirichlet_Series: theory HOL-Algebra.Lattice
22:02:07Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra
22:02:07Dirichlet_Series: theory HOL-Algebra.Complete_Lattice
22:02:07Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset
22:02:08Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization
22:02:08Dirichlet_Series: theory HOL-Algebra.Group
22:02:10Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs
22:02:11Dirichlet_Series: theory Landau_Symbols.Landau_More
22:02:11Dirichlet_Series: theory HOL-Algebra.Coset
22:02:13Dirichlet_Series: theory HOL-Algebra.FiniteProduct
22:02:13Dirichlet_Series: theory HOL-Algebra.Ring
22:02:14Dirichlet_Series: theory HOL-Algebra.Generated_Groups
22:02:15Dirichlet_Series: theory HOL-Algebra.Elementary_Groups
22:02:18Dirichlet_Series: theory HOL-Algebra.AbelCoset
22:02:18Dirichlet_Series: theory HOL-Algebra.Module
22:02:23Dirichlet_Series: theory HOL-Algebra.Ideal
22:02:27Dirichlet_Series: theory HOL-Algebra.RingHom
22:02:28Dirichlet_Series: theory HOL-Algebra.UnivPoly
22:02:43Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group
22:02:47Dirichlet_Series: theory HOL-Number_Theory.Residues
22:02:51Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion
22:02:51Dirichlet_Series: theory HOL-Number_Theory.Pocklington
22:02:51Dirichlet_Series: theory HOL-Number_Theory.Gauss
22:02:52Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
22:02:52Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
22:02:52Dirichlet_Series: theory HOL-Number_Theory.Number_Theory
22:02:54Dirichlet_Series: theory Bernoulli.Bernoulli_FPS
22:02:54Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc
22:02:55Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function
22:02:55Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product
22:02:55Dirichlet_Series: theory Dirichlet_Series.Euler_Products
22:02:56Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series
22:02:58Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
22:03:01Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu
22:03:01Dirichlet_Series: theory Dirichlet_Series.More_Totient
22:03:01Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda
22:03:01Dirichlet_Series: theory Dirichlet_Series.Divisor_Count
22:03:01Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
22:03:01Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory
22:03:01Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code
22:03:02Dirichlet_Series: theory Dirichlet_Series.Partial_Summation
22:03:03Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
22:03:13Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
22:04:11Preparing Dirichlet_Series/document ...
22:04:23Finished Dirichlet_Series/document (0:00:11 elapsed time)
22:04:23Preparing Dirichlet_Series/outline ...
22:04:29Finished Dirichlet_Series/outline (0:00:05 elapsed time)
22:04:29Timing Dirichlet_Series (8 threads, 102.037s elapsed time, 658.955s cpu time, 30.956s GC time, factor 6.46)
22:04:29Finished Dirichlet_Series (0:02:09 elapsed time, 0:11:56 cpu time, factor 5.55)
22:04:29Running Constructive_Cryptography_CM (on hpcisabelle/0) ...
22:04:32Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
22:04:32Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
22:04:32Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
22:04:39Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
22:04:40Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
22:04:40Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
22:04:40Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
22:05:02Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
22:05:02Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
22:05:03Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
22:05:05Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
22:05:06Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
22:05:21Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
22:05:21Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
22:06:10Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
22:08:45Preparing Constructive_Cryptography_CM/document ...
22:09:07Finished Constructive_Cryptography_CM/document (0:00:21 elapsed time)
22:09:07Preparing Constructive_Cryptography_CM/outline ...
22:09:19Finished Constructive_Cryptography_CM/outline (0:00:11 elapsed time)
22:09:19Timing Constructive_Cryptography_CM (8 threads, 249.668s elapsed time, 1391.654s cpu time, 25.633s GC time, factor 5.57)
22:09:19Finished Constructive_Cryptography_CM (0:04:14 elapsed time, 0:23:24 cpu time, factor 5.51)
22:09:19Building Slicing (on hpcisabelle/1) ...
22:09:21Slicing: theory Slicing.AuxLemmas
22:09:21Slicing: theory Slicing.Com
22:09:21Slicing: theory Slicing.BitVector
22:09:21Slicing: theory Slicing.BasicDefs
22:09:23Slicing: theory Slicing.CFG
22:09:23Slicing: theory Slicing.JVMCFG
22:09:23Slicing: theory Slicing.CFGExit
22:09:23Slicing: theory Slicing.CFG_wf
22:09:23Slicing: theory Slicing.Distance
22:09:23Slicing: theory Slicing.SemanticsCFG
22:09:23Slicing: theory Slicing.Observable
22:09:23Slicing: theory Slicing.Postdomination
22:09:23Slicing: theory Slicing.CFGExit_wf
22:09:23Slicing: theory Slicing.DynDataDependence
22:09:23Slicing: theory Slicing.DataDependence
22:09:24Slicing: theory Slicing.Slice
22:09:24Slicing: theory Slicing.WeakOrderDependence
22:09:24Slicing: theory Slicing.DynStandardControlDependence
22:09:24Slicing: theory Slicing.DynWeakControlDependence
22:09:24Slicing: theory Slicing.WeakControlDependence
22:09:24Slicing: theory Slicing.StandardControlDependence
22:09:24Slicing: theory Slicing.DynPDG
22:09:24Slicing: theory Slicing.PDG
22:09:24Slicing: theory Slicing.ControlDependenceRelations
22:09:25Slicing: theory Slicing.Labels
22:09:25Slicing: theory Slicing.WCFG
22:09:25Slicing: theory Slicing.DependentLiveVariables
22:09:25Slicing: theory Slicing.Semantics
22:09:26Slicing: theory Slicing.CDepInstantiations
22:09:26Slicing: theory Slicing.DynSlice
22:09:27Slicing: theory Slicing.Interpretation
22:09:27Slicing: theory Slicing.WEquivalence
22:09:27Slicing: theory Slicing.WellFormed
22:09:28Slicing: theory Slicing.AdditionalLemmas
22:09:28Slicing: theory Slicing.DynamicControlDependences
22:09:28Slicing: theory Slicing.SemanticsWellFormed
22:09:29Slicing: theory Slicing.StaticControlDependences
22:09:30Slicing: theory Slicing.JVMInterpretation
22:09:32Slicing: theory Slicing.JVMCFG_wf
22:09:32Slicing: theory Slicing.JVMPostdomination
22:09:32Slicing: theory Slicing.SemanticsWF
22:09:37Slicing: theory Slicing.JVMControlDependences
22:09:37Slicing: theory Slicing.Slicing
22:13:39Preparing Slicing/document ...
22:13:54Finished Slicing/document (0:00:14 elapsed time)
22:13:54Preparing Slicing/outline ...
22:13:59Finished Slicing/outline (0:00:05 elapsed time)
22:13:59Timing Slicing (8 threads, 239.090s elapsed time, 1517.370s cpu time, 13.251s GC time, factor 6.35)
22:13:59Finished Slicing (0:04:18 elapsed time, 0:25:57 cpu time, factor 6.03)
22:13:59Running No_FTL_observers (on hpcisabelle/2) ...
22:14:00No_FTL_observers: theory No_FTL_observers.SomeFunc
22:14:00No_FTL_observers: theory No_FTL_observers.SpaceTime
22:16:08No_FTL_observers: theory No_FTL_observers.Axioms
22:17:46No_FTL_observers: theory No_FTL_observers.SpecRel
22:18:04Preparing No_FTL_observers/document ...
22:18:07Finished No_FTL_observers/document (0:00:03 elapsed time)
22:18:07Preparing No_FTL_observers/outline ...
22:18:10Finished No_FTL_observers/outline (0:00:02 elapsed time)
22:18:10Timing No_FTL_observers (8 threads, 243.071s elapsed time, 276.643s cpu time, 4.620s GC time, factor 1.14)
22:18:10Finished No_FTL_observers (0:04:05 elapsed time, 0:04:39 cpu time, factor 1.14)
22:18:10Running FO_Theory_Rewriting (on hpcisabelle/3) ...
22:18:14FO_Theory_Rewriting: theory Deriving.Comparator
22:18:14FO_Theory_Rewriting: theory Containers.Equal
22:18:14FO_Theory_Rewriting: theory Deriving.Derive_Manager
22:18:14FO_Theory_Rewriting: theory Deriving.Generator_Aux
22:18:14FO_Theory_Rewriting: theory Containers.Extend_Partial_Order
22:18:14FO_Theory_Rewriting: theory FO_Theory_Rewriting.Saturation
22:18:14FO_Theory_Rewriting: theory Containers.AssocList
22:18:14FO_Theory_Rewriting: theory Containers.List_Fusion
22:18:14FO_Theory_Rewriting: theory Containers.Closure_Set
22:18:14FO_Theory_Rewriting: theory Containers.Containers_Auxiliary
22:18:14FO_Theory_Rewriting: theory First_Order_Terms.Option_Monad
22:18:14FO_Theory_Rewriting: theory First_Order_Terms.Term
22:18:15FO_Theory_Rewriting: theory Deriving.Equality_Generator
22:18:15FO_Theory_Rewriting: theory Abstract-Rewriting.Seq
22:18:15FO_Theory_Rewriting: theory FOL-Fitting.FOL_Fitting
22:18:15FO_Theory_Rewriting: theory Containers.Containers_Generator
22:18:16FO_Theory_Rewriting: theory Deriving.Equality_Instances
22:18:16FO_Theory_Rewriting: theory Matrix.Utility
22:18:16FO_Theory_Rewriting: theory Regular-Sets.Regular_Set
22:18:16FO_Theory_Rewriting: theory Deriving.Compare
22:18:16FO_Theory_Rewriting: theory Deriving.Comparator_Generator
22:18:16FO_Theory_Rewriting: theory Containers.Collection_Enum
22:18:16FO_Theory_Rewriting: theory Containers.Lexicographic_Order
22:18:16FO_Theory_Rewriting: theory Containers.Collection_Eq
22:18:17FO_Theory_Rewriting: theory Containers.Set_Linorder
22:18:17FO_Theory_Rewriting: theory Containers.RBT_ext
22:18:17FO_Theory_Rewriting: theory Deriving.RBT_Comparator_Impl
22:18:17FO_Theory_Rewriting: theory Containers.DList_Set
22:18:17FO_Theory_Rewriting: theory Deriving.Compare_Generator
22:18:17FO_Theory_Rewriting: theory Polynomial_Factorization.Missing_List
22:18:17FO_Theory_Rewriting: theory Deriving.Compare_Instances
22:18:18FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Inference
22:18:21FO_Theory_Rewriting: theory Regular-Sets.Regular_Exp
22:18:25FO_Theory_Rewriting: theory Regular-Sets.NDerivative
22:18:25FO_Theory_Rewriting: theory Regular-Sets.Relation_Interpretation
22:18:30FO_Theory_Rewriting: theory Regular-Sets.Equivalence_Checking
22:18:30FO_Theory_Rewriting: theory Regular-Sets.Regexp_Method
22:18:31FO_Theory_Rewriting: theory Containers.Collection_Order
22:18:31FO_Theory_Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
22:18:33FO_Theory_Rewriting: theory Containers.RBT_Mapping2
22:18:34FO_Theory_Rewriting: theory First_Order_Terms.Subterm_and_Context
22:18:35FO_Theory_Rewriting: theory Containers.RBT_Set2
22:18:37FO_Theory_Rewriting: theory Regular_Tree_Relations.Term_Context
22:18:38FO_Theory_Rewriting: theory Containers.Set_Impl
22:18:41FO_Theory_Rewriting: theory Regular_Tree_Relations.Basic_Utils
22:18:41FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Terms
22:18:44FO_Theory_Rewriting: theory Regular_Tree_Relations.FSet_Utils
22:18:44FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Closure
22:18:44FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Ctxt
22:18:48FO_Theory_Rewriting: theory FO_Theory_Rewriting.Utils
22:18:49FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata
22:18:49FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Fset
22:18:49FO_Theory_Rewriting: theory FO_Theory_Rewriting.Bot_Terms
22:18:50FO_Theory_Rewriting: theory FO_Theory_Rewriting.Multihole_Context
22:18:50FO_Theory_Rewriting: theory FO_Theory_Rewriting.Rewriting
22:18:51FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Certificate
22:18:55FO_Theory_Rewriting: theory FO_Theory_Rewriting.Ground_MCtxt
22:18:56FO_Theory_Rewriting: theory FO_Theory_Rewriting.NF
22:18:57FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Det
22:18:57FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Pumping
22:18:57FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Complement
22:18:57FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT
22:18:57FO_Theory_Rewriting: theory Regular_Tree_Relations.RRn_Automata
22:18:58FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Compose
22:18:58FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl
22:18:59FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Transitive_Closure
22:19:00FO_Theory_Rewriting: theory Regular_Tree_Relations.Pair_Automaton
22:19:00FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite
22:19:01FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_Extensions
22:19:01FO_Theory_Rewriting: theory FO_Theory_Rewriting.LV_to_GTT
22:19:01FO_Theory_Rewriting: theory Regular_Tree_Relations.AGTT
22:19:01FO_Theory_Rewriting: theory Containers.Mapping_Impl
22:19:01FO_Theory_Rewriting: theory FO_Theory_Rewriting.Tree_Automata_Derivation_Split
22:19:02FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite_Q_infinity
22:19:02FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_RR2
22:19:03FO_Theory_Rewriting: theory FO_Theory_Rewriting.TA_Clousure_Const
22:19:03FO_Theory_Rewriting: theory Regular_Tree_Relations.Regular_Relation_Abstract_Impl
22:19:04FO_Theory_Rewriting: theory Containers.Map_To_Mapping
22:19:04FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl
22:19:04FO_Theory_Rewriting: theory Containers.Containers
22:19:06FO_Theory_Rewriting: theory FO_Theory_Rewriting.Type_Instances_Impl
22:19:06FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Impl
22:19:09FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOL_Extra
22:19:09FO_Theory_Rewriting: theory FO_Theory_Rewriting.NF_Impl
22:19:10FO_Theory_Rewriting: theory Regular_Tree_Relations.Regular_Relation_Impl
22:19:14FO_Theory_Rewriting: theory FO_Theory_Rewriting.Lift_Root_Step
22:19:16FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Semantics
22:19:16FO_Theory_Rewriting: theory FO_Theory_Rewriting.GTT_RRn
22:19:40FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Check
22:19:55FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Check_Impl
22:22:09Preparing FO_Theory_Rewriting/document ...
22:22:30Finished FO_Theory_Rewriting/document (0:00:21 elapsed time)
22:22:30Preparing FO_Theory_Rewriting/outline ...
22:22:42Finished FO_Theory_Rewriting/outline (0:00:12 elapsed time)
22:22:43Timing FO_Theory_Rewriting (8 threads, 229.529s elapsed time, 1609.309s cpu time, 125.289s GC time, factor 7.01)
22:22:43Finished FO_Theory_Rewriting (0:03:54 elapsed time, 0:27:08 cpu time, factor 6.94)
22:22:43Running HOL-Decision_Procs (on hpcisabelle/4) ...
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List
22:22:45HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair
22:22:47HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring
22:22:49HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex
22:22:49HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack
22:22:49HOL-Decision_Procs: theory HOL-Decision_Procs.MIR
22:22:49HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds
22:22:56HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation
22:22:59HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete
22:22:59HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field
22:23:03HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial
22:23:14HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex
22:23:16HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff
22:23:58HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex
22:23:58HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex
22:26:43HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs
22:26:56Timing HOL-Decision_Procs (8 threads, 246.716s elapsed time, 1517.814s cpu time, 131.348s GC time, factor 6.15)
22:26:56Finished HOL-Decision_Procs (0:04:11 elapsed time, 0:25:31 cpu time, factor 6.09)
22:26:57Running FSM_Tests (on hpcisabelle/5) ...
22:26:59FSM_Tests: theory Containers.List_Fusion
22:26:59FSM_Tests: theory Containers.Equal
22:26:59FSM_Tests: theory Containers.Extend_Partial_Order
22:26:59FSM_Tests: theory HOL-Eisbach.Eisbach
22:26:59FSM_Tests: theory Deriving.Comparator
22:26:59FSM_Tests: theory Deriving.Generator_Aux
22:26:59FSM_Tests: theory Deriving.Derive_Manager
22:26:59FSM_Tests: theory Containers.AssocList
22:26:59FSM_Tests: theory Containers.Closure_Set
22:26:59FSM_Tests: theory Datatype_Order_Generator.Derive_Aux
22:26:59FSM_Tests: theory Containers.Containers_Auxiliary
22:26:59FSM_Tests: theory HOL-ex.Quicksort
22:26:59FSM_Tests: theory Deriving.Equality_Generator
22:27:00FSM_Tests: theory Datatype_Order_Generator.Order_Generator
22:27:00FSM_Tests: theory Word_Lib.Bit_Comprehension
22:27:00FSM_Tests: theory Containers.Containers_Generator
22:27:00FSM_Tests: theory Word_Lib.More_Divides
22:27:01FSM_Tests: theory Deriving.Equality_Instances
22:27:01FSM_Tests: theory Word_Lib.Signed_Division_Word
22:27:01FSM_Tests: theory FSM_Tests.Util
22:27:01FSM_Tests: theory Native_Word.Code_Int_Integer_Conversion
22:27:01FSM_Tests: theory Automatic_Refinement.Misc
22:27:01FSM_Tests: theory Word_Lib.More_Arithmetic
22:27:01FSM_Tests: theory Deriving.Compare
22:27:01FSM_Tests: theory Deriving.Comparator_Generator
22:27:01FSM_Tests: theory Containers.Collection_Enum
22:27:01FSM_Tests: theory Containers.Lexicographic_Order
22:27:01FSM_Tests: theory Containers.Collection_Eq
22:27:02FSM_Tests: theory Containers.Set_Linorder
22:27:02FSM_Tests: theory Containers.RBT_ext
22:27:03FSM_Tests: theory Deriving.RBT_Comparator_Impl
22:27:03FSM_Tests: theory Deriving.Compare_Generator
22:27:03FSM_Tests: theory Word_Lib.More_Bit_Ring
22:27:03FSM_Tests: theory Containers.DList_Set
22:27:03FSM_Tests: theory Deriving.Compare_Instances
22:27:04FSM_Tests: theory Word_Lib.More_Word
22:27:07FSM_Tests: theory Native_Word.Code_Target_Word_Base
22:27:07FSM_Tests: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:27:07FSM_Tests: theory Word_Lib.Least_significant_bit
22:27:08FSM_Tests: theory FSM_Tests.FSM_Impl
22:27:08FSM_Tests: theory FSM_Tests.Maximal_Path_Trie
22:27:08FSM_Tests: theory FSM_Tests.Prefix_Tree
22:27:09FSM_Tests: theory Word_Lib.Most_significant_bit
22:27:09FSM_Tests: theory Word_Lib.Generic_set_bit
22:27:10FSM_Tests: theory Native_Word.Code_Target_Integer_Bit
22:27:10FSM_Tests: theory Native_Word.Word_Type_Copies
22:27:13FSM_Tests: theory FSM_Tests.FSM
22:27:16FSM_Tests: theory Containers.Collection_Order
22:27:18FSM_Tests: theory Containers.RBT_Mapping2
22:27:20FSM_Tests: theory Containers.RBT_Set2
22:27:23FSM_Tests: theory Containers.Set_Impl
22:27:26FSM_Tests: theory Native_Word.Uint64
22:27:28FSM_Tests: theory FSM_Tests.Backwards_Reachability_Analysis
22:27:28FSM_Tests: theory FSM_Tests.IO_Sequence_Set
22:27:28FSM_Tests: theory FSM_Tests.Minimisation
22:27:28FSM_Tests: theory FSM_Tests.Observability
22:27:29FSM_Tests: theory FSM_Tests.Product_FSM
22:27:29FSM_Tests: theory FSM_Tests.State_Cover
22:27:31FSM_Tests: theory FSM_Tests.State_Preamble
22:27:31FSM_Tests: theory FSM_Tests.State_Separator
22:27:32FSM_Tests: theory FSM_Tests.Distinguishability
22:27:32FSM_Tests: theory FSM_Tests.Test_Suite_Representations
22:27:35FSM_Tests: theory FSM_Tests.Adaptive_Test_Case
22:27:35FSM_Tests: theory FSM_Tests.Helper_Algorithms
22:27:35FSM_Tests: theory FSM_Tests.R_Distinguishability
22:27:36FSM_Tests: theory FSM_Tests.Traversal_Set
22:27:37FSM_Tests: theory FSM_Tests.Test_Suite
22:27:38FSM_Tests: theory FSM_Tests.OFSM_Tables_Refined
22:27:38FSM_Tests: theory FSM_Tests.Convergence
22:27:40FSM_Tests: theory FSM_Tests.Convergence_Graph
22:27:41FSM_Tests: theory FSM_Tests.Empty_Convergence_Graph
22:27:41FSM_Tests: theory FSM_Tests.Simple_Convergence_Graph
22:27:41FSM_Tests: theory FSM_Tests.H_Framework
22:27:42FSM_Tests: theory FSM_Tests.Pair_Framework
22:27:43FSM_Tests: theory FSM_Tests.SPY_Framework
22:27:43FSM_Tests: theory FSM_Tests.Test_Suite_IO
22:27:45FSM_Tests: theory FSM_Tests.Test_Suite_Calculation
22:27:47FSM_Tests: theory Containers.Mapping_Impl
22:27:49FSM_Tests: theory Containers.Map_To_Mapping
22:27:50FSM_Tests: theory Containers.Containers
22:27:50FSM_Tests: theory FSM_Tests.FSM_Code_Datatype
22:27:50FSM_Tests: theory FSM_Tests.Prefix_Tree_Refined
22:27:51FSM_Tests: theory FSM_Tests.Util_Refined
22:27:51FSM_Tests: theory FSM_Tests.Prime_Transformation
22:27:52FSM_Tests: theory FSM_Tests.Test_Suite_Calculation_Refined
22:27:52FSM_Tests: theory FSM_Tests.Test_Suite_Representations_Refined
22:28:03FSM_Tests: theory FSM_Tests.Intermediate_Implementations
22:29:19FSM_Tests: theory FSM_Tests.Intermediate_Frameworks
22:29:21FSM_Tests: theory FSM_Tests.HSI_Method_Implementations
22:29:21FSM_Tests: theory FSM_Tests.H_Method_Implementations
22:29:21FSM_Tests: theory FSM_Tests.Partial_S_Method_Implementations
22:29:22FSM_Tests: theory FSM_Tests.SPYH_Method_Implementations
22:29:22FSM_Tests: theory FSM_Tests.SPY_Method_Implementations
22:29:22FSM_Tests: theory FSM_Tests.W_Method_Implementations
22:29:22FSM_Tests: theory FSM_Tests.Wp_Method_Implementations
22:29:26FSM_Tests: theory FSM_Tests.Test_Suite_Generator_Code_Export
22:31:24Preparing FSM_Tests/document ...
22:33:17Finished FSM_Tests/document (0:01:53 elapsed time)
22:33:17Preparing FSM_Tests/outline ...
22:33:46Finished FSM_Tests/outline (0:00:28 elapsed time)
22:33:46Timing FSM_Tests (8 threads, 252.049s elapsed time, 1810.659s cpu time, 147.288s GC time, factor 7.18)
22:33:46Finished FSM_Tests (0:04:17 elapsed time, 0:30:35 cpu time, factor 7.11)
22:33:46Running Differential_Dynamic_Logic (on hpcisabelle/6) ...
22:33:49Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
22:33:49Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
22:33:49Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
22:34:01Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
22:34:01Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
22:34:08Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
22:34:08Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
22:34:09Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
22:34:12Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
22:34:12Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
22:34:13Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
22:34:13Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
22:34:13Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
22:34:25Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
22:34:28Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
22:34:57Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
22:37:54Preparing Differential_Dynamic_Logic/document ...
22:38:15Finished Differential_Dynamic_Logic/document (0:00:20 elapsed time)
22:38:15Preparing Differential_Dynamic_Logic/outline ...
22:38:22Finished Differential_Dynamic_Logic/outline (0:00:07 elapsed time)
22:38:22Timing Differential_Dynamic_Logic (8 threads, 241.489s elapsed time, 631.561s cpu time, 14.483s GC time, factor 2.62)
22:38:22Finished Differential_Dynamic_Logic (0:04:05 elapsed time, 0:10:42 cpu time, factor 2.61)
22:38:22Building Aggregation_Algebras (on hpcisabelle/7) ...
22:38:24Aggregation_Algebras: theory Aggregation_Algebras.Aggregation_Algebras
22:38:24Aggregation_Algebras: theory Aggregation_Algebras.Semigroups_Big
22:38:37Aggregation_Algebras: theory Aggregation_Algebras.Matrix_Aggregation_Algebras
22:39:26Aggregation_Algebras: theory Aggregation_Algebras.Linear_Aggregation_Algebras
22:39:26Aggregation_Algebras: theory Aggregation_Algebras.M_Choose_Component
22:40:30Preparing Aggregation_Algebras/document ...
22:40:35Finished Aggregation_Algebras/document (0:00:05 elapsed time)
22:40:35Preparing Aggregation_Algebras/outline ...
22:40:39Finished Aggregation_Algebras/outline (0:00:03 elapsed time)
22:40:39Timing Aggregation_Algebras (8 threads, 114.005s elapsed time, 187.015s cpu time, 4.469s GC time, factor 1.64)
22:40:39Finished Aggregation_Algebras (0:02:07 elapsed time, 0:03:33 cpu time, factor 1.68)
22:40:39Building Coinductive (on hpcisabelle/0) ...
22:40:41Coinductive: theory Coinductive.Resumption
22:40:41Coinductive: theory HOL-Analysis.Abstract_Topology
22:40:41Coinductive: theory HOL-Combinatorics.Transposition
22:40:41Coinductive: theory HOL-Analysis.Continuum_Not_Denumerable
22:40:41Coinductive: theory HOL-Analysis.Metric_Arith
22:40:41Coinductive: theory HOL-Analysis.L2_Norm
22:40:41Coinductive: theory HOL-Analysis.Inner_Product
22:40:41Coinductive: theory HOL-Analysis.Product_Vector
22:40:42Coinductive: theory Coinductive.Coinductive_Nat
22:40:42Coinductive: theory HOL-Analysis.Norm_Arith
22:40:44Coinductive: theory Coinductive.Coinductive_List
22:40:45Coinductive: theory HOL-Analysis.Elementary_Topology
22:40:45Coinductive: theory HOL-Analysis.Euclidean_Space
22:40:48Coinductive: theory HOL-Analysis.Finite_Cartesian_Product
22:40:48Coinductive: theory HOL-Analysis.Linear_Algebra
22:40:48Coinductive: theory HOL-Analysis.Abstract_Topology_2
22:40:51Coinductive: theory HOL-Analysis.Cartesian_Space
22:40:52Coinductive: theory HOL-Analysis.Connected
22:40:52Coinductive: theory HOL-Analysis.Elementary_Metric_Spaces
22:40:54Coinductive: theory Coinductive.Coinductive_List_Prefix
22:40:54Coinductive: theory Coinductive.Hamming_Stream
22:40:54Coinductive: theory Coinductive.Koenigslemma
22:40:54Coinductive: theory Coinductive.LMirror
22:40:54Coinductive: theory Coinductive.Lazy_LList
22:40:54Coinductive: theory Coinductive.Quotient_Coinductive_List
22:40:55Coinductive: theory Coinductive.TLList
22:40:55Coinductive: theory HOL-Analysis.Elementary_Normed_Spaces
22:40:55Coinductive: theory Coinductive.Coinductive_Stream
22:40:56Coinductive: theory HOL-Analysis.Topology_Euclidean_Space
22:40:57Coinductive: theory Coinductive.Lazy_TLList
22:40:57Coinductive: theory Coinductive.Quotient_TLList
22:40:57Coinductive: theory Coinductive.TLList_CCPO
22:40:58Coinductive: theory Coinductive.TLList_CCPO_Examples
22:40:58Coinductive: theory HOL-Analysis.Extended_Real_Limits
22:40:58Coinductive: theory Coinductive.Coinductive
22:41:00Coinductive: theory Coinductive.CCPO_Topology
22:41:02Coinductive: theory Coinductive.LList_CCPO_Topology
22:41:04Coinductive: theory Coinductive.Coinductive_Examples
22:42:11Preparing Coinductive/document ...
22:42:20Finished Coinductive/document (0:00:09 elapsed time)
22:42:20Preparing Coinductive/outline ...
22:42:26Finished Coinductive/outline (0:00:05 elapsed time)
22:42:26Timing Coinductive (8 threads, 66.316s elapsed time, 484.617s cpu time, 12.027s GC time, factor 7.31)
22:42:26Finished Coinductive (0:01:29 elapsed time, 0:08:53 cpu time, factor 5.96)
22:42:26Running Van_Emde_Boas_Trees (on hpcisabelle/1) ...
22:42:28Van_Emde_Boas_Trees: theory HOL-Eisbach.Eisbach
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Cancellation
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Adhoc_Overloading
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Infinite_Set
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Old_Datatype
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Nat_Bijection
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Option_ord
22:42:28Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Syntax_Match
22:42:28Van_Emde_Boas_Trees: theory HOL-Library.Monad_Syntax
22:42:29Van_Emde_Boas_Trees: theory HOL-Library.Countable
22:42:30Van_Emde_Boas_Trees: theory HOL-Library.Multiset
22:42:31Van_Emde_Boas_Trees: theory HOL-Imperative_HOL.Heap
22:42:33Van_Emde_Boas_Trees: theory HOL-Imperative_HOL.Heap_Monad
22:42:33Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Heap_Time_Monad
22:42:35Van_Emde_Boas_Trees: theory HOL-Imperative_HOL.Array
22:42:36Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Array_Time
22:42:36Van_Emde_Boas_Trees: theory HOL-Imperative_HOL.Ref
22:42:36Van_Emde_Boas_Trees: theory HOL-ex.Quicksort
22:42:37Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Ref_Time
22:42:37Van_Emde_Boas_Trees: theory HOL-Imperative_HOL.Imperative_HOL
22:42:37Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Imperative_HOL_Add
22:42:37Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Imperative_HOL_Time
22:42:37Van_Emde_Boas_Trees: theory Automatic_Refinement.Misc
22:42:43Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Assertions
22:42:46Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Hoare_Triple
22:42:46Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Refine_Imp_Hol
22:42:46Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Automation
22:42:48Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Sep_Main
22:42:49Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Time_Reasoning
22:42:50Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.Simple_TBOUND_Cond
22:42:51Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Example_Setup
22:42:51Van_Emde_Boas_Trees: theory Deriving.Generator_Aux
22:42:51Van_Emde_Boas_Trees: theory Deriving.Comparator
22:42:51Van_Emde_Boas_Trees: theory Deriving.Derive_Manager
22:42:51Van_Emde_Boas_Trees: theory HOL-Library.Char_ord
22:42:51Van_Emde_Boas_Trees: theory HOL-Library.Code_Abstract_Nat
22:42:51Van_Emde_Boas_Trees: theory HOL-Library.Code_Target_Int
22:42:51Van_Emde_Boas_Trees: theory HOL-Library.Phantom_Type
22:42:51Van_Emde_Boas_Trees: theory HOL-Library.Rewrite
22:42:52Van_Emde_Boas_Trees: theory HOL-Library.Signed_Division
22:42:52Van_Emde_Boas_Trees: theory Deriving.Countable_Generator
22:42:52Van_Emde_Boas_Trees: theory HOL-Library.Code_Target_Nat
22:42:52Van_Emde_Boas_Trees: theory Deriving.Equality_Generator
22:42:52Van_Emde_Boas_Trees: theory HOL-Library.Countable_Set
22:42:52Van_Emde_Boas_Trees: theory Native_Word.Code_Int_Integer_Conversion
22:42:52Van_Emde_Boas_Trees: theory HOL-Library.Code_Target_Numeral
22:42:52Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_List_Assn
22:42:52Van_Emde_Boas_Trees: theory Word_Lib.More_Bit_Ring
22:42:52Van_Emde_Boas_Trees: theory Deriving.Equality_Instances
22:42:52Van_Emde_Boas_Trees: theory HOL-Library.Cardinality
22:42:53Van_Emde_Boas_Trees: theory HOL-Library.Countable_Complete_Lattices
22:42:53Van_Emde_Boas_Trees: theory Deriving.Compare
22:42:53Van_Emde_Boas_Trees: theory Deriving.Comparator_Generator
22:42:53Van_Emde_Boas_Trees: theory HOL-Library.Numeral_Type
22:42:54Van_Emde_Boas_Trees: theory Deriving.Compare_Generator
22:42:55Van_Emde_Boas_Trees: theory Deriving.Compare_Instances
22:42:55Van_Emde_Boas_Trees: theory HOL-Library.Type_Length
22:42:55Van_Emde_Boas_Trees: theory HOL-Library.Word
22:42:55Van_Emde_Boas_Trees: theory Word_Lib.More_Arithmetic
22:42:56Van_Emde_Boas_Trees: theory HOL-Library.Order_Continuity
22:42:57Van_Emde_Boas_Trees: theory HOL-Library.Extended_Nat
22:42:58Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Definitions
22:43:03Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Height
22:43:03Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Member
22:43:03Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Space
22:43:04Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Insert
22:43:04Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_MinMax
22:43:06Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_InsertCorrectness
22:43:06Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Pred
22:43:06Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Succ
22:43:06Van_Emde_Boas_Trees: theory Word_Lib.Bit_Comprehension
22:43:06Van_Emde_Boas_Trees: theory Word_Lib.More_Divides
22:43:07Van_Emde_Boas_Trees: theory Word_Lib.Signed_Division_Word
22:43:07Van_Emde_Boas_Trees: theory Word_Lib.More_Word
22:43:09Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Bounds
22:43:09Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Delete
22:43:09Van_Emde_Boas_Trees: theory Native_Word.Code_Target_Word_Base
22:43:09Van_Emde_Boas_Trees: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:43:10Van_Emde_Boas_Trees: theory Word_Lib.Least_significant_bit
22:43:11Van_Emde_Boas_Trees: theory Word_Lib.Most_significant_bit
22:43:12Van_Emde_Boas_Trees: theory Word_Lib.Generic_set_bit
22:43:12Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_DeleteCorrectness
22:43:13Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Uniqueness
22:43:13Van_Emde_Boas_Trees: theory Native_Word.Code_Target_Integer_Bit
22:43:13Van_Emde_Boas_Trees: theory Native_Word.Word_Type_Copies
22:43:17Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_DeleteBounds
22:43:23Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Intf_Functional
22:43:28Van_Emde_Boas_Trees: theory Native_Word.Uint32
22:43:30Van_Emde_Boas_Trees: theory Collections.HashCode
22:43:31Van_Emde_Boas_Trees: theory Deriving.Hash_Generator
22:43:32Van_Emde_Boas_Trees: theory Deriving.Hash_Instances
22:43:32Van_Emde_Boas_Trees: theory Deriving.Derive
22:43:34Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_BuildupMemImp
22:43:48Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_SuccPredImperative
22:43:52Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_DelImperative
22:43:55Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Intf_Imperative
22:44:04Van_Emde_Boas_Trees: theory Van_Emde_Boas_Trees.VEBT_Example
22:46:28Preparing Van_Emde_Boas_Trees/document ...
22:47:05Finished Van_Emde_Boas_Trees/document (0:00:36 elapsed time)
22:47:05Preparing Van_Emde_Boas_Trees/outline ...
22:47:16Finished Van_Emde_Boas_Trees/outline (0:00:11 elapsed time)
22:47:17Timing Van_Emde_Boas_Trees (8 threads, 235.917s elapsed time, 1317.071s cpu time, 47.795s GC time, factor 5.58)
22:47:17Finished Van_Emde_Boas_Trees (0:03:58 elapsed time, 0:22:03 cpu time, factor 5.56)
22:47:17Running Network_Security_Policy_Verification (on hpcisabelle/2) ...
22:47:18Network_Security_Policy_Verification: theory HOL-Eisbach.Eisbach
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Cancellation
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Char_ord
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Code_Abstract_Nat
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Option_ord
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Infinite_Set
22:47:18Network_Security_Policy_Verification: theory HOL-Library.List_Lexorder
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Product_Lexorder
22:47:18Network_Security_Policy_Verification: theory HOL-Library.RBT_Impl
22:47:18Network_Security_Policy_Verification: theory HOL-Library.Code_Target_Nat
22:47:18Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph
22:47:18Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz
22:47:19Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable
22:47:19Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util
22:47:19Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_Impl
22:47:20Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_List_Impl
22:47:20Network_Security_Policy_Verification: theory HOL-Library.Multiset
22:47:20Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph
22:47:26Network_Security_Policy_Verification: theory HOL-ex.Quicksort
22:47:27Network_Security_Policy_Verification: theory Automatic_Refinement.Misc
22:47:34Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct
22:48:22Network_Security_Policy_Verification: theory HOL-Library.RBT
22:48:23Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl
22:48:56Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Vertices
22:48:56Network_Security_Policy_Verification: theory HOL-Lattice.Orders
22:48:57Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface
22:48:57Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.vertex_example_simps
22:48:57Network_Security_Policy_Verification: theory HOL-Lattice.Bounds
22:48:58Network_Security_Policy_Verification: theory HOL-Lattice.Lattice
22:48:58Network_Security_Policy_Verification: theory HOL-Lattice.CompleteLattice
22:48:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_withOffendingFlows
22:49:00Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_ENF
22:49:00Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Helper
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPstrict
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl
22:49:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets2
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW
22:49:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting
22:49:03Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted
22:49:03Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory
22:49:03Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface_impl
22:49:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Analysis_Tainting
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl
22:49:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink_impl
22:49:06Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl
22:49:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl
22:49:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets_impl
22:49:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl
22:49:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting_impl
22:49:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl
22:49:09Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl
22:49:13Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary
22:49:25Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Library
22:49:29Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_BLP
22:49:29Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Impl
22:49:29Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_generateCode
22:49:30Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Network_Security_Policy_Verification
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_NetModel
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.attic
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CryptoDB
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_Forte14
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Distributed_WebApp
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.I8_SSH_Landscape
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.IDEM
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork
22:49:39Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example
22:49:40Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance
22:49:40Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.MeasrDroid
22:50:29Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Imaginary_Factory_Network
22:50:29Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Examples
22:51:22Preparing Network_Security_Policy_Verification/document ...
22:51:37Finished Network_Security_Policy_Verification/document (0:00:14 elapsed time)
22:51:37Preparing Network_Security_Policy_Verification/outline ...
22:51:45Finished Network_Security_Policy_Verification/outline (0:00:08 elapsed time)
22:51:45Timing Network_Security_Policy_Verification (8 threads, 239.595s elapsed time, 1316.153s cpu time, 58.748s GC time, factor 5.49)
22:51:45Finished Network_Security_Policy_Verification (0:04:02 elapsed time, 0:22:06 cpu time, factor 5.46)
22:51:45Building HOLCF (on hpcisabelle/3) ...
22:51:47HOLCF: theory HOLCF.README
22:51:47HOLCF: theory HOL-Library.Nat_Bijection
22:51:47HOLCF: theory HOL-Library.Old_Datatype
22:51:47HOLCF: theory HOLCF.Porder
22:51:48HOLCF: theory HOLCF.Pcpo
22:51:48HOLCF: theory HOL-Library.Countable
22:51:49HOLCF: theory HOLCF.Cont
22:51:50HOLCF: theory HOLCF.Adm
22:51:50HOLCF: theory HOLCF.Discrete
22:51:50HOLCF: theory HOLCF.Cpodef
22:51:50HOLCF: theory HOLCF.Fun_Cpo
22:51:50HOLCF: theory HOLCF.Product_Cpo
22:51:50HOLCF: theory HOLCF.Cfun
22:51:51HOLCF: theory HOLCF.Completion
22:51:51HOLCF: theory HOLCF.Fix
22:51:51HOLCF: theory HOLCF.Sfun
22:51:51HOLCF: theory HOLCF.Cprod
22:51:51HOLCF: theory HOLCF.Up
22:51:51HOLCF: theory HOLCF.Deflation
22:51:51HOLCF: theory HOLCF.Sprod
22:51:52HOLCF: theory HOLCF.Lift
22:51:53HOLCF: theory HOLCF.One
22:51:53HOLCF: theory HOLCF.Tr
22:51:53HOLCF: theory HOLCF.Ssum
22:51:53HOLCF: theory HOLCF.Fixrec
22:51:53HOLCF: theory HOLCF.Map_Functions
22:51:54HOLCF: theory HOLCF.Bifinite
22:51:54HOLCF: theory HOLCF.Domain_Aux
22:51:55HOLCF: theory HOLCF.Universal
22:51:57HOLCF: theory HOLCF.Algebraic
22:51:57HOLCF: theory HOLCF.Compact_Basis
22:51:57HOLCF: theory HOLCF.LowerPD
22:51:57HOLCF: theory HOLCF.UpperPD
22:51:57HOLCF: theory HOLCF.Representable
22:51:57HOLCF: theory HOLCF.ConvexPD
22:51:59HOLCF: theory HOLCF.Domain
22:52:01HOLCF: theory HOLCF.Powerdomains
22:52:02HOLCF: theory HOLCF
22:52:11Preparing HOLCF/document ...
22:52:18Finished HOLCF/document (0:00:07 elapsed time)
22:52:18Preparing HOLCF/outline ...
22:52:23Finished HOLCF/outline (0:00:04 elapsed time)
22:52:23Timing HOLCF (8 threads, 16.298s elapsed time, 52.927s cpu time, 1.860s GC time, factor 3.25)
22:52:23Finished HOLCF (0:00:24 elapsed time, 0:01:08 cpu time, factor 2.75)
22:52:24Building Complex_Bounded_Operators (on hpcisabelle/4) ...
22:52:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
22:52:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
22:52:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
22:52:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
22:52:27Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
22:52:30Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
22:52:31Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
22:52:46Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
22:52:52Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
22:52:55Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
22:52:58Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
22:52:59Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
22:53:01Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
22:53:03Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
22:53:09Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
22:53:11Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
22:53:15Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
22:53:19Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
22:55:39Preparing Complex_Bounded_Operators/document ...
22:56:17Finished Complex_Bounded_Operators/document (0:00:37 elapsed time)
22:56:17Preparing Complex_Bounded_Operators/outline ...
22:56:33Finished Complex_Bounded_Operators/outline (0:00:15 elapsed time)
22:56:33Timing Complex_Bounded_Operators (8 threads, 169.211s elapsed time, 733.317s cpu time, 36.171s GC time, factor 4.33)
22:56:33Finished Complex_Bounded_Operators (0:03:14 elapsed time, 0:13:03 cpu time, factor 4.03)
22:56:33Running HOL-Corec_Examples (on hpcisabelle/5) ...
22:56:35HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV
22:56:35HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples
22:56:35HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter
22:56:35HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting
22:56:35HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete
22:57:23HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends
22:57:31HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B
22:57:35HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C
22:57:36HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class
22:57:42HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D
23:00:16Timing HOL-Corec_Examples (8 threads, 216.533s elapsed time, 674.530s cpu time, 63.762s GC time, factor 3.12)
23:00:16Finished HOL-Corec_Examples (0:03:42 elapsed time, 0:11:38 cpu time, factor 3.14)
23:00:16Running Executable_Randomized_Algorithms (on hpcisabelle/6) ...
23:00:19Executable_Randomized_Algorithms: theory Flow_Networks.Graph
23:00:19Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Fraction_Field
23:00:19Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Group_Closure
23:00:19Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Squarefree
23:00:19Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Nth_Powers
23:00:19Executable_Randomized_Algorithms: theory HOL-Library.Case_Converter
23:00:19Executable_Randomized_Algorithms: theory HOL-Number_Theory.Cong
23:00:19Executable_Randomized_Algorithms: theory HOL-Algebra.Congruence
23:00:19Executable_Randomized_Algorithms: theory HOL-Library.More_List
23:00:20Executable_Randomized_Algorithms: theory HOL-Library.Type_Length
23:00:20Executable_Randomized_Algorithms: theory HOL-Library.Code_Lazy
23:00:20Executable_Randomized_Algorithms: theory HOL-Library.Power_By_Squaring
23:00:20Executable_Randomized_Algorithms: theory HOL-Library.Transitive_Closure_Table
23:00:20Executable_Randomized_Algorithms: theory HOL-Library.While_Combinator
23:00:21Executable_Randomized_Algorithms: theory HOL-Number_Theory.Eratosthenes
23:00:21Executable_Randomized_Algorithms: theory HOL-Algebra.Order
23:00:21Executable_Randomized_Algorithms: theory HOL-Library.Word
23:00:21Executable_Randomized_Algorithms: theory HOL-Types_To_Sets.Types_To_Sets
23:00:21Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
23:00:21Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial
23:00:22Executable_Randomized_Algorithms: theory HOL-Library.Bourbaki_Witt_Fixpoint
23:00:22Executable_Randomized_Algorithms: theory HOL-Number_Theory.Mod_Exp
23:00:22Executable_Randomized_Algorithms: theory HOL-Library.Going_To_Filter
23:00:22Executable_Randomized_Algorithms: theory Flow_Networks.Network
23:00:22Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tau_Additivity
23:00:22Executable_Randomized_Algorithms: theory HOL-Number_Theory.Fib
23:00:22Executable_Randomized_Algorithms: theory HOL-Number_Theory.Prime_Powers
23:00:22Executable_Randomized_Algorithms: theory HOL-Number_Theory.Totient
23:00:22Executable_Randomized_Algorithms: theory HOL-Algebra.Lattice
23:00:22Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Contour_Integration
23:00:22Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Coin_Space
23:00:23Executable_Randomized_Algorithms: theory MFMC_Countable.MFMC_Misc
23:00:24Executable_Randomized_Algorithms: theory Probabilistic_While.Bernoulli
23:00:24Executable_Randomized_Algorithms: theory Flow_Networks.Residual_Graph
23:00:24Executable_Randomized_Algorithms: theory HOL-Algebra.Complete_Lattice
23:00:25Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
23:00:26Executable_Randomized_Algorithms: theory HOL-Algebra.Group
23:00:26Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Winding_Numbers
23:00:28Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
23:00:28Executable_Randomized_Algorithms: theory Flow_Networks.Augmenting_Flow
23:00:28Executable_Randomized_Algorithms: theory Flow_Networks.Augmenting_Path
23:00:28Executable_Randomized_Algorithms: theory Flow_Networks.Ford_Fulkerson
23:00:29Executable_Randomized_Algorithms: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
23:00:29Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Conformal_Mappings
23:00:29Executable_Randomized_Algorithms: theory HOL-Algebra.Coset
23:00:29Executable_Randomized_Algorithms: theory HOL-Algebra.FiniteProduct
23:00:31Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Singularities
23:00:31Executable_Randomized_Algorithms: theory HOL-Algebra.Ring
23:00:31Executable_Randomized_Algorithms: theory MFMC_Countable.MFMC_Finite
23:00:32Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Great_Picard
23:00:32Executable_Randomized_Algorithms: theory MFMC_Countable.Matrix_For_Marginals
23:00:32Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Riemann_Mapping
23:00:34Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Residues
23:00:34Executable_Randomized_Algorithms: theory HOL-Algebra.Generated_Groups
23:00:34Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Residue_Theorem
23:00:36Executable_Randomized_Algorithms: theory HOL-Algebra.Elementary_Groups
23:00:37Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Permuted_Congruential_Generator
23:00:37Executable_Randomized_Algorithms: theory HOL-Algebra.AbelCoset
23:00:37Executable_Randomized_Algorithms: theory HOL-Algebra.Module
23:00:37Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:00:37Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial_FPS
23:00:38Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Polynomial_Factorial
23:00:38Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Formal_Laurent_Series
23:00:39Executable_Randomized_Algorithms: theory MFMC_Countable.Rel_PMF_Characterisation
23:00:39Executable_Randomized_Algorithms: theory Probabilistic_While.While_SPMF
23:00:40Executable_Randomized_Algorithms: theory Probabilistic_While.Geometric
23:00:40Executable_Randomized_Algorithms: theory HOL-Algebra.Ideal
23:00:41Executable_Randomized_Algorithms: theory HOL-Computational_Algebra.Computational_Algebra
23:00:41Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Laurent_Convergence
23:00:43Executable_Randomized_Algorithms: theory HOL-Algebra.RingHom
23:00:43Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Meromorphic
23:00:44Executable_Randomized_Algorithms: theory HOL-Algebra.UnivPoly
23:00:45Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Weierstrass_Factorization
23:00:45Executable_Randomized_Algorithms: theory HOL-Complex_Analysis.Complex_Analysis
23:01:01Executable_Randomized_Algorithms: theory HOL-Algebra.Multiplicative_Group
23:01:05Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residues
23:01:09Executable_Randomized_Algorithms: theory HOL-Number_Theory.Euler_Criterion
23:01:09Executable_Randomized_Algorithms: theory HOL-Number_Theory.Pocklington
23:01:09Executable_Randomized_Algorithms: theory HOL-Number_Theory.Gauss
23:01:10Executable_Randomized_Algorithms: theory HOL-Number_Theory.Quadratic_Reciprocity
23:01:10Executable_Randomized_Algorithms: theory HOL-Number_Theory.Residue_Primitive_Roots
23:01:10Executable_Randomized_Algorithms: theory HOL-Number_Theory.Number_Theory
23:01:12Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Misc
23:01:12Executable_Randomized_Algorithms: theory Dirichlet_Series.Multiplicative_Function
23:01:12Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Product
23:01:12Executable_Randomized_Algorithms: theory Dirichlet_Series.Euler_Products
23:01:13Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series
23:01:18Executable_Randomized_Algorithms: theory Dirichlet_Series.Moebius_Mu
23:01:19Executable_Randomized_Algorithms: theory Dirichlet_Series.More_Totient
23:01:19Executable_Randomized_Algorithms: theory Dirichlet_Series.Liouville_Lambda
23:01:19Executable_Randomized_Algorithms: theory Dirichlet_Series.Divisor_Count
23:01:19Executable_Randomized_Algorithms: theory Dirichlet_Series.Arithmetic_Summatory
23:01:20Executable_Randomized_Algorithms: theory Dirichlet_Series.Partial_Summation
23:01:22Executable_Randomized_Algorithms: theory Dirichlet_Series.Dirichlet_Series_Analysis
23:01:32Executable_Randomized_Algorithms: theory Zeta_Function.Zeta_Library
23:01:32Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
23:01:36Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Randomized_Algorithm
23:01:37Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Basic_Randomized_Algorithms
23:01:37Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm
23:01:38Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Tracking_SPMF
23:01:39Executable_Randomized_Algorithms: theory Executable_Randomized_Algorithms.Dice_Roll
23:03:15Preparing Executable_Randomized_Algorithms/document ...
23:03:22Finished Executable_Randomized_Algorithms/document (0:00:07 elapsed time)
23:03:22Preparing Executable_Randomized_Algorithms/outline ...
23:03:26Finished Executable_Randomized_Algorithms/outline (0:00:04 elapsed time)
23:03:26Timing Executable_Randomized_Algorithms (8 threads, 168.526s elapsed time, 1190.761s cpu time, 46.573s GC time, factor 7.07)
23:03:26Finished Executable_Randomized_Algorithms (0:02:52 elapsed time, 0:20:01 cpu time, factor 6.95)
23:03:27Running Stochastic_Matrices (on hpcisabelle/7) ...
23:03:30Stochastic_Matrices: theory HOL-Eisbach.Eisbach
23:03:30Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
23:03:30Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Misc
23:03:30Stochastic_Matrices: theory HOL-Algebra.Congruence
23:03:30Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
23:03:30Stochastic_Matrices: theory HOL-Library.More_List
23:03:30Stochastic_Matrices: theory HOL-Library.Function_Algebras
23:03:30Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
23:03:30Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
23:03:31Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
23:03:31Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
23:03:31Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
23:03:31Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
23:03:32Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
23:03:32Stochastic_Matrices: theory VectorSpace.FunctionLemmas
23:03:32Stochastic_Matrices: theory HOL-Algebra.Order
23:03:32Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
23:03:32Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
23:03:33Stochastic_Matrices: theory HOL-Algebra.Lattice
23:03:34Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
23:03:35Stochastic_Matrices: theory HOL-Algebra.Group
23:03:36Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
23:03:38Stochastic_Matrices: theory HOL-Algebra.Coset
23:03:38Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
23:03:39Stochastic_Matrices: theory HOL-Algebra.Ring
23:03:43Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
23:03:43Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
23:03:44Stochastic_Matrices: theory HOL-Algebra.Module
23:03:44Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
23:03:45Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
23:03:47Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
23:03:47Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
23:03:47Stochastic_Matrices: theory VectorSpace.RingModuleFacts
23:03:47Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:03:48Stochastic_Matrices: theory VectorSpace.MonoidSums
23:03:49Stochastic_Matrices: theory VectorSpace.LinearCombinations
23:03:50Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
23:03:50Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
23:03:55Stochastic_Matrices: theory VectorSpace.SumSpaces
23:03:56Stochastic_Matrices: theory VectorSpace.VectorSpace
23:03:57Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
23:03:58Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
23:03:59Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
23:04:02Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
23:04:03Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
23:04:03Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
23:04:07Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
23:04:21Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
23:04:21Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
23:04:23Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
23:04:25Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
23:04:28Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
23:04:33Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
23:04:33Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
23:04:38Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
23:04:39Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
23:04:41Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
23:07:12Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
23:07:12Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
23:07:12Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
23:07:16Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
23:07:19Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
23:07:27Preparing Stochastic_Matrices/document ...
23:07:30Finished Stochastic_Matrices/document (0:00:02 elapsed time)
23:07:30Preparing Stochastic_Matrices/outline ...
23:07:32Finished Stochastic_Matrices/outline (0:00:02 elapsed time)
23:07:32Timing Stochastic_Matrices (8 threads, 232.568s elapsed time, 1274.326s cpu time, 42.364s GC time, factor 5.48)
23:07:32Finished Stochastic_Matrices (0:03:56 elapsed time, 0:21:25 cpu time, factor 5.42)
23:07:32Running MonoidalCategory (on hpcisabelle/0) ...
23:07:35MonoidalCategory: theory MonoidalCategory.MonoidalCategory
23:08:46MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
23:08:52MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
23:09:00MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
23:11:24Preparing MonoidalCategory/document ...
23:11:39Finished MonoidalCategory/document (0:00:14 elapsed time)
23:11:39Preparing MonoidalCategory/outline ...
23:11:45Finished MonoidalCategory/outline (0:00:06 elapsed time)
23:11:45Timing MonoidalCategory (8 threads, 227.256s elapsed time, 950.566s cpu time, 54.761s GC time, factor 4.18)
23:11:45Finished MonoidalCategory (0:03:50 elapsed time, 0:15:57 cpu time, factor 4.15)
23:11:45Building Formula_Derivatives (on hpcisabelle/1) ...
23:11:47Formula_Derivatives: theory Formula_Derivatives.While_Default
23:11:47Formula_Derivatives: theory Formula_Derivatives.FSet_More
23:11:47Formula_Derivatives: theory Coinductive_Languages.Coinductive_Language
23:11:47Formula_Derivatives: theory Deriving.Comparator
23:11:47Formula_Derivatives: theory Deriving.Derive_Manager
23:11:47Formula_Derivatives: theory Deriving.Generator_Aux
23:11:47Formula_Derivatives: theory List-Index.List_Index
23:11:49Formula_Derivatives: theory Deriving.Compare
23:11:49Formula_Derivatives: theory Deriving.Comparator_Generator
23:11:50Formula_Derivatives: theory Formula_Derivatives.Automaton
23:11:50Formula_Derivatives: theory Deriving.Compare_Generator
23:11:51Formula_Derivatives: theory Deriving.Compare_Instances
23:11:51Formula_Derivatives: theory Formula_Derivatives.Abstract_Formula
23:11:51Formula_Derivatives: theory Formula_Derivatives.WS1S_Prelim
23:12:41Formula_Derivatives: theory Formula_Derivatives.Presburger_Formula
23:12:41Formula_Derivatives: theory Formula_Derivatives.WS1S_Alt_Formula
23:12:41Formula_Derivatives: theory Formula_Derivatives.WS1S_Formula
23:13:23Formula_Derivatives: theory Formula_Derivatives.WS1S_Nameful
23:13:28Formula_Derivatives: theory Formula_Derivatives.WS1S_Presburger_Equivalence
23:15:35Preparing Formula_Derivatives/document ...
23:15:40Finished Formula_Derivatives/document (0:00:04 elapsed time)
23:15:40Preparing Formula_Derivatives/outline ...
23:15:43Finished Formula_Derivatives/outline (0:00:03 elapsed time)
23:15:43Timing Formula_Derivatives (8 threads, 200.959s elapsed time, 912.469s cpu time, 195.262s GC time, factor 4.54)
23:15:43Finished Formula_Derivatives (0:03:49 elapsed time, 0:16:18 cpu time, factor 4.27)
23:15:43Building CakeML (on hpcisabelle/2) ...
23:15:45CakeML: theory HOL-Eisbach.Eisbach
23:15:45CakeML: theory CakeML.Doc_Generated
23:15:45CakeML: theory CakeML.Doc_Proofs
23:15:45CakeML: theory Deriving.Generator_Aux
23:15:45CakeML: theory Deriving.Derive_Manager
23:15:45CakeML: theory HOL-Library.Case_Converter
23:15:45CakeML: theory HOL-Library.Complete_Partial_Order2
23:15:45CakeML: theory HOL-Library.Datatype_Records
23:15:45CakeML: theory HOL-Library.Infinite_Set
23:15:45CakeML: theory HOL-Library.Nat_Bijection
23:15:45CakeML: theory HOL-Library.Old_Datatype
23:15:46CakeML: theory Word_Lib.Signed_Words
23:15:46CakeML: theory HOL-Library.Simps_Case_Conv
23:15:46CakeML: theory Word_Lib.Type_Syntax
23:15:46CakeML: theory Word_Lib.Word_Names
23:15:46CakeML: theory Word_Lib.Word_Syntax
23:15:46CakeML: theory HOL-Library.Signed_Division
23:15:47CakeML: theory HOL-Library.Lattice_Algebras
23:15:47CakeML: theory HOL-Library.Log_Nat
23:15:47CakeML: theory Show.Show
23:15:47CakeML: theory HOL-Library.Countable
23:15:47CakeML: theory Word_Lib.Enumeration
23:15:47CakeML: theory HOL-Eisbach.Eisbach_Tools
23:15:47CakeML: theory Word_Lib.Many_More
23:15:47CakeML: theory Word_Lib.Rsplit
23:15:48CakeML: theory Word_Lib.Word_EqI
23:15:48CakeML: theory Word_Lib.Enumeration_Word
23:15:48CakeML: theory Word_Lib.Signed_Division_Word
23:15:48CakeML: theory Word_Lib.More_Misc
23:15:48CakeML: theory CakeML.Namespace
23:15:48CakeML: theory Show.Show_Instances
23:15:49CakeML: theory CakeML.Tokens
23:15:49CakeML: theory HOL-Library.Countable_Set
23:15:49CakeML: theory HOL-Library.Countable_Complete_Lattices
23:15:50CakeML: theory Word_Lib.Boolean_Inequalities
23:15:52CakeML: theory HOL-Library.Order_Continuity
23:15:53CakeML: theory HOL-Library.Float
23:15:53CakeML: theory HOL-Library.Extended_Nat
23:15:53CakeML: theory Word_Lib.Word_Lemmas
23:15:54CakeML: theory CakeML.NamespaceAuxiliary
23:15:54CakeML: theory Coinductive.Coinductive_Nat
23:15:56CakeML: theory Coinductive.Coinductive_List
23:15:57CakeML: theory IEEE_Floating_Point.IEEE
23:15:57CakeML: theory Word_Lib.More_Word_Operations
23:15:58CakeML: theory Word_Lib.Word_64
23:16:01CakeML: theory IEEE_Floating_Point.FP64
23:16:04CakeML: theory CakeML.Lib
23:16:08CakeML: theory CakeML.LibAuxiliary
23:16:08CakeML: theory CakeML.Ffi
23:16:08CakeML: theory CakeML.FpSem
23:16:12CakeML: theory CakeML.Ast
23:16:17CakeML: theory CakeML.SimpleIO
23:16:44CakeML: theory CakeML.CakeML_Compiler
23:16:44CakeML: theory CakeML.AstAuxiliary
23:16:44CakeML: theory CakeML.SemanticPrimitives
23:17:17CakeML: theory CakeML.CakeML_Quickcheck
23:17:17CakeML: theory CakeML.SmallStep
23:17:17CakeML: theory CakeML.TypeSystem
23:17:17CakeML: theory CakeML.Evaluate
23:17:17CakeML: theory CakeML.SemanticPrimitivesAuxiliary
23:17:23CakeML: theory CakeML.BigStep
23:17:24CakeML: theory CakeML.PrimTypes
23:17:30CakeML: theory CakeML.BigSmallInvariants
23:17:30CakeML: theory CakeML.Semantic_Extras
23:17:41CakeML: theory CakeML.TypeSystemAuxiliary
23:17:44CakeML: theory CakeML.Big_Step_Determ
23:17:44CakeML: theory CakeML.Big_Step_Total
23:17:45CakeML: theory CakeML.Big_Step_Clocked
23:17:45CakeML: theory CakeML.Big_Step_Unclocked
23:17:46CakeML: theory CakeML.Evaluate_Termination
23:17:46CakeML: theory CakeML.Evaluate_Clock
23:17:46CakeML: theory CakeML.Matching
23:17:46CakeML: theory CakeML.Big_Step_Fun_Equiv
23:17:46CakeML: theory CakeML.Evaluate_Single
23:17:49CakeML: theory CakeML.Big_Step_Unclocked_Single
23:17:57CakeML: theory CakeML.CakeML_Code
23:19:06CakeML: theory CakeML.Compiler_Test
23:19:14CakeML: theory CakeML.Code_Test_Haskell
23:19:48Build timed out (after 300 minutes). Marking the build as failed.
23:19:48Build was aborted
23:24:13Started calculate disk usage of build
23:24:13Finished Calculation of disk usage of build in 0 seconds
23:24:14Started calculate disk usage of workspace
23:24:15Finished Calculation of disk usage of workspace in 1 second
23:24:16No emails were triggered.
23:24:16Finished: FAILURE
![[Jenkins]](/jenkins/static/858a1f95/images/svgs/logo.svg){kind=logo}
