Building Formal_SSA ...
20:40:41Formal_SSA: theory Formal_SSA.Serial_Rel
20:40:41Formal_SSA: theory Dijkstra_Shortest_Path.Graph
20:40:41Formal_SSA: theory HOL-Library.Char_ord
20:40:41Formal_SSA: theory HOL-Library.Omega_Words_Fun
20:40:42Formal_SSA: theory HOL-Library.List_Lexorder
20:40:43Formal_SSA: theory HOL-Library.Mapping
20:40:43Formal_SSA: theory HOL-Library.RBT_Set
20:40:43Formal_SSA: theory CAVA_Automata.Digraph_Basic
20:40:44Formal_SSA: theory HOL-Library.Sublist
20:40:45Formal_SSA: theory Formal_SSA.While_Combinator_Exts
20:40:45Formal_SSA: theory Slicing.AuxLemmas
20:40:45Formal_SSA: theory Slicing.BasicDefs
20:40:46Formal_SSA: theory Slicing.Com
20:40:46Formal_SSA: theory HOL-Library.RBT_Mapping
20:40:46Formal_SSA: theory Dijkstra_Shortest_Path.GraphSpec
20:40:47Formal_SSA: theory Slicing.CFG
20:40:47Formal_SSA: theory Slicing.CFGExit
20:40:47Formal_SSA: theory Slicing.Postdomination
20:40:47Formal_SSA: theory Slicing.DynStandardControlDependence
20:40:48Formal_SSA: theory Slicing.DynWeakControlDependence
20:40:48Formal_SSA: theory Slicing.StandardControlDependence
20:40:48Formal_SSA: theory Formal_SSA.FormalSSA_Misc
20:40:48Formal_SSA: theory Slicing.WeakControlDependence
20:40:48Formal_SSA: theory Slicing.CFG_wf
20:40:48Formal_SSA: theory Formal_SSA.Mapping_Exts
20:40:48Formal_SSA: theory Slicing.CFGExit_wf
20:40:49Formal_SSA: theory Slicing.DynDataDependence
20:40:49Formal_SSA: theory Slicing.DataDependence
20:40:49Formal_SSA: theory Formal_SSA.RBT_Mapping_Exts
20:40:49Formal_SSA: theory Slicing.PDG
20:40:50Formal_SSA: theory Slicing.Distance
20:40:50Groebner_Bases: theory Polynomials.MPoly_Type_Class
20:40:50Formal_SSA: theory Slicing.Observable
20:40:50Formal_SSA: theory Slicing.SemanticsCFG
20:40:50Formal_SSA: theory Slicing.WeakOrderDependence
20:40:51Formal_SSA: theory Slicing.Slice
20:40:51Formal_SSA: theory Slicing.Labels
20:40:51Formal_SSA: theory Slicing.WCFG
20:40:51Groebner_Bases: theory Polynomials.PP_Type
20:40:52Formal_SSA: theory Formal_SSA.Graph_path
20:40:54Formal_SSA: theory Slicing.Interpretation
20:40:55Formal_SSA: theory Slicing.CDepInstantiations
20:40:55Formal_SSA: theory Slicing.WellFormed
20:40:56Groebner_Bases: theory Polynomials.MPoly_Type_Class_Ordered
20:40:57Formal_SSA: theory Slicing.AdditionalLemmas
20:40:57Formal_SSA: theory Formal_SSA.Disjoin_Transform
20:41:01Formal_SSA: theory Formal_SSA.SSA_CFG
20:41:06Formal_SSA: theory Formal_SSA.Construct_SSA
20:41:06Formal_SSA: theory Formal_SSA.Minimality
20:41:06Formal_SSA: theory Formal_SSA.SSA_CFG_code
20:41:09Formal_SSA: theory Formal_SSA.Construct_SSA_notriv
20:41:10Formal_SSA: theory Formal_SSA.SSA_Semantics
20:41:12Formal_SSA: theory Formal_SSA.Construct_SSA_code
20:41:13Formal_SSA: theory Formal_SSA.Construct_SSA_notriv_code
20:41:16Formal_SSA: theory Formal_SSA.SSA_Transfer_Rules
20:41:21Groebner_Bases: theory Groebner_Bases.More_MPoly_Type_Class
20:41:21Groebner_Bases: theory Groebner_Bases.Reduction
20:41:21Groebner_Bases: theory Polynomials.Quasi_PM_Power_Products
20:41:25Groebner_Bases: theory Groebner_Bases.Macaulay_Matrix
20:41:25Formal_SSA: theory Formal_SSA.Generic_Interpretation
20:41:28Groebner_Bases: theory Polynomials.MPoly_PM
20:41:32Groebner_Bases: theory Polynomials.OAlist_Poly_Mapping
20:41:33Groebner_Bases: theory Groebner_Bases.Auto_Reduction
20:41:33MDP-Algorithms FAILED (see also "isabelle build_log -H Error MDP-Algorithms")
20:41:33*** Failed to load theory "Jordan_Normal_Form.Matrix_IArray_Impl" (unresolved "Containers.Set_Impl")
20:41:33*** Failed to load theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl" (unresolved "Jordan_Normal_Form.Matrix_IArray_Impl")
20:41:33*** Failed to load theory "Jordan_Normal_Form.Matrix_Impl" (unresolved "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl", "Jordan_Normal_Form.Matrix_IArray_Impl")
20:41:33*** Failed to load theory "MDP-Algorithms.PI_Code" (unresolved "Jordan_Normal_Form.Matrix_Impl")
20:41:33*** Failed to load theory "MDP-Algorithms.PI_Code_Export_Float" (unresolved "MDP-Algorithms.PI_Code")
20:41:33*** Failed to load theory "MDP-Algorithms.PI_Code_Export_Rat" (unresolved "MDP-Algorithms.PI_Code")
20:41:33*** Not a constant: wf
20:41:33*** At command "declare" (line 287 of "$AFP/Containers/Set_Impl.thy")
20:41:33Building Constructive_Cryptography ...
20:41:34Groebner_Bases: theory Groebner_Bases.Groebner_Bases
20:41:38Constructive_Cryptography: theory Constructive_Cryptography.Resource
20:41:44Constructive_Cryptography: theory Constructive_Cryptography.Converter
20:41:46Groebner_Bases: theory Polynomials.Term_Order
20:41:55Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
20:41:56Groebner_Bases: theory Polynomials.MPoly_Type_Class_OAlist
20:41:57Constructive_Cryptography: theory Constructive_Cryptography.Random_System
20:41:57Formal_SSA: theory Formal_SSA.Generic_Extract
20:41:57Formal_SSA: theory Formal_SSA.WhileGraphSSA
20:41:58Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
20:41:59Constructive_Cryptography: theory Constructive_Cryptography.Wiring
20:41:59Groebner_Bases: theory Groebner_Bases.Algorithm_Schema
20:41:59Groebner_Bases: theory Groebner_Bases.Reduced_GB
20:42:01Groebner_Bases: theory Groebner_Bases.Syzygy
20:42:02Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
20:42:02Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
20:42:12Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
20:42:12Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
20:42:18Groebner_Bases: theory Groebner_Bases.Groebner_PM
20:42:22Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
20:42:23Groebner_Bases: theory Groebner_Bases.Benchmarks
20:42:25Constructive_Cryptography: theory Constructive_Cryptography.Examples
20:43:11Groebner_Bases: theory Groebner_Bases.Buchberger
20:43:11Groebner_Bases: theory Groebner_Bases.F4
20:43:11Groebner_Bases: theory Groebner_Bases.Algorithm_Schema_Impl
20:43:17Preparing HOL-CSP/document ...
20:43:31Groebner_Bases: theory Groebner_Bases.Buchberger_Examples
20:43:31Groebner_Bases: theory Groebner_Bases.Syzygy_Examples
20:43:31Groebner_Bases: theory Groebner_Bases.Reduced_GB_Examples
20:43:43Preparing Three_Squares/document ...
20:43:49Finished Three_Squares/document (0:00:06 elapsed time)
20:43:49Preparing Three_Squares/outline ...
20:43:53Finished HOL-CSP/document (0:00:35 elapsed time)
20:43:53Preparing HOL-CSP/outline ...
20:43:53Finished Three_Squares/outline (0:00:03 elapsed time)
20:43:54Timing Three_Squares (4 threads, 581.000s elapsed time, 1860.232s cpu time, 119.430s GC time, factor 3.20)
20:43:54Finished Three_Squares (0:10:37 elapsed time, 0:32:44 cpu time, factor 3.08)
20:43:54Building Incompleteness ...
20:43:57Incompleteness: theory FinFun.FinFun
20:44:00Incompleteness: theory Nominal2.Nominal2_Base
20:44:06Finished HOL-CSP/outline (0:00:13 elapsed time)
20:44:06Timing HOL-CSP (4 threads, 333.946s elapsed time, 1062.235s cpu time, 13.351s GC time, factor 3.18)
20:44:06Finished HOL-CSP (0:06:04 elapsed time, 0:18:36 cpu time, factor 3.06)
20:44:06Running Correctness_Algebras ...
20:44:08Incompleteness: theory Nominal2.Nominal2_Abs
20:44:10Correctness_Algebras: theory LatticeProperties.Conj_Disj
20:44:10Correctness_Algebras: theory LatticeProperties.WellFoundedTransitive
20:44:10Correctness_Algebras: theory Stone_Algebras.Lattice_Basics
20:44:11Correctness_Algebras: theory LatticeProperties.Complete_Lattice_Prop
20:44:11Incompleteness: theory Nominal2.Nominal2_FCB
20:44:12Correctness_Algebras: theory MonoBoolTranAlgebra.Mono_Bool_Tran
20:44:12Incompleteness: theory Nominal2.Nominal2
20:44:13Correctness_Algebras: theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
20:44:18Incompleteness: theory Incompleteness.SyntaxN
20:44:21Correctness_Algebras: theory MonoBoolTranAlgebra.Assertion_Algebra
20:44:24Preparing Van_Emde_Boas_Trees/document ...
20:44:25Incompleteness: theory Incompleteness.Coding
20:44:26Incompleteness: theory Incompleteness.Predicates
20:44:28Incompleteness: theory Incompleteness.Sigma
20:44:32Correctness_Algebras: theory Stone_Algebras.P_Algebras
20:44:32Correctness_Algebras: theory Stone_Relation_Algebras.Fixpoints
20:44:35Preparing Constructive_Cryptography/document ...
20:44:36Incompleteness: theory Incompleteness.Coding_Predicates
20:44:36Correctness_Algebras: theory Stone_Relation_Algebras.Semirings
20:44:41Incompleteness: theory Incompleteness.Functions
20:44:41Incompleteness: theory Incompleteness.Pf_Predicates
20:44:44Incompleteness: theory Incompleteness.Goedel_I
20:44:45Incompleteness: theory Incompleteness.II_Prelims
20:44:47Incompleteness: theory Incompleteness.Pseudo_Coding
20:44:47Incompleteness: theory Incompleteness.Quote
20:44:48Finished Constructive_Cryptography/document (0:00:13 elapsed time)
20:44:48Preparing Constructive_Cryptography/outline ...
20:44:48Incompleteness: theory Incompleteness.Goedel_II
20:44:50Correctness_Algebras: theory Correctness_Algebras.Base
20:44:50Correctness_Algebras: theory Correctness_Algebras.Lattice_Ordered_Semirings
20:44:50Correctness_Algebras: theory Stone_Kleene_Relation_Algebras.Iterings
20:44:53Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings
20:44:56Finished Constructive_Cryptography/outline (0:00:07 elapsed time)
20:44:56Timing Constructive_Cryptography (4 threads, 151.059s elapsed time, 489.018s cpu time, 3.688s GC time, factor 3.24)
20:44:56Finished Constructive_Cryptography (0:03:00 elapsed time, 0:08:56 cpu time, factor 2.97)
20:44:56Building Stone_Algebras ...
20:45:00Stone_Algebras: theory Stone_Algebras.Lattice_Basics
20:45:01Correctness_Algebras: theory Correctness_Algebras.Monotonic_Boolean_Transformers
20:45:08Correctness_Algebras: theory Correctness_Algebras.Approximation
20:45:11Correctness_Algebras: theory Subset_Boolean_Algebras.Subset_Boolean_Algebras
20:45:12Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings_Strict
20:45:14Correctness_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Algebras
20:45:18Finished Van_Emde_Boas_Trees/document (0:00:54 elapsed time)
20:45:18Preparing Van_Emde_Boas_Trees/outline ...
20:45:18Correctness_Algebras: theory Stone_Relation_Algebras.Relation_Algebras
20:45:22Stone_Algebras: theory Stone_Algebras.Filters
20:45:22Stone_Algebras: theory Stone_Algebras.P_Algebras
20:45:28Correctness_Algebras: theory Correctness_Algebras.Boolean_Semirings
20:45:31Correctness_Algebras: theory Correctness_Algebras.N_Algebras
20:45:33Finished Van_Emde_Boas_Trees/outline (0:00:15 elapsed time)
20:45:33Timing Van_Emde_Boas_Trees (4 threads, 461.348s elapsed time, 1373.434s cpu time, 23.122s GC time, factor 2.98)
20:45:33Finished Van_Emde_Boas_Trees (0:07:45 elapsed time, 0:23:01 cpu time, factor 2.97)
20:45:33Building Simple_Firewall ...
20:45:35Simple_Firewall: theory Simple_Firewall.GroupF
20:45:35Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
20:45:35Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
20:45:35Simple_Firewall: theory HOL-Library.Char_ord
20:45:35Simple_Firewall: theory Simple_Firewall.Iface
20:45:37Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
20:45:38Simple_Firewall: theory Simple_Firewall.L4_Protocol
20:45:38Simple_Firewall: theory Simple_Firewall.List_Product_More
20:45:38Simple_Firewall: theory Simple_Firewall.Option_Helpers
20:45:38Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
20:45:41Simple_Firewall: theory Simple_Firewall.Simple_Packet
20:45:41Simple_Firewall: theory Simple_Firewall.Primitives_toString
20:45:43Correctness_Algebras: theory Correctness_Algebras.Recursion
20:45:44Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
20:45:47Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
20:45:47Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
20:45:50Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
20:45:50Simple_Firewall: theory Simple_Firewall.Shadowed
20:45:50Simple_Firewall: theory Simple_Firewall.Service_Matrix
20:45:53Correctness_Algebras: theory Correctness_Algebras.Tests
20:45:56Correctness_Algebras: theory Correctness_Algebras.Complete_Tests
20:45:57Correctness_Algebras: theory Correctness_Algebras.Preconditions
20:45:57Correctness_Algebras: theory Correctness_Algebras.Relative_Domain
20:45:59Preparing SC_DOM_Components/document ...
20:46:00Stone_Algebras: theory Stone_Algebras.Stone_Construction
20:46:04Correctness_Algebras: theory Correctness_Algebras.Hoare
20:46:12Correctness_Algebras: theory Correctness_Algebras.Pre_Post
20:46:12Finished SC_DOM_Components/document (0:00:13 elapsed time)
20:46:12Preparing SC_DOM_Components/outline ...
20:46:16Preparing Simple_Firewall/document ...
20:46:20Groebner_Bases FAILED (see also "isabelle build_log -H Error Groebner_Bases")
20:46:20*** Failed to load theory "Jordan_Normal_Form.Matrix_IArray_Impl" (unresolved "Containers.Set_Impl")
20:46:20*** Failed to load theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl" (unresolved "Jordan_Normal_Form.Matrix_IArray_Impl")
20:46:20*** Failed to load theory "Groebner_Bases.F4_Examples" (unresolved "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl")
20:46:20*** Not a constant: wf
20:46:20*** At command "declare" (line 287 of "$AFP/Containers/Set_Impl.thy")
20:46:20Building Affine_Arithmetic ...
20:46:20Finished SC_DOM_Components/outline (0:00:07 elapsed time)
20:46:20Timing SC_DOM_Components (4 threads, 758.585s elapsed time, 2591.094s cpu time, 93.781s GC time, factor 3.42)
20:46:20Finished SC_DOM_Components (0:12:45 elapsed time, 0:43:26 cpu time, factor 3.41)
20:46:20Building Quantales_Converse ...
20:46:21Correctness_Algebras: theory Correctness_Algebras.Complete_Domain
20:46:22Quantales_Converse: theory Kleene_Algebra.Signatures
20:46:22Quantales_Converse: theory Order_Lattice_Props.Sup_Lattice
20:46:22Correctness_Algebras: theory Correctness_Algebras.Relative_Modal
20:46:22Quantales_Converse: theory Kleene_Algebra.Dioid
20:46:23Affine_Arithmetic: theory Deriving.Comparator
20:46:23Affine_Arithmetic: theory Deriving.Generator_Aux
20:46:23Affine_Arithmetic: theory Deriving.Derive_Manager
20:46:23Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order
20:46:23Affine_Arithmetic: theory HOL-Library.AList
20:46:24Correctness_Algebras: theory Correctness_Algebras.Domain
20:46:24Affine_Arithmetic: theory Deriving.Equality_Generator
20:46:24Preparing Stone_Algebras/document ...
20:46:25Affine_Arithmetic: theory Deriving.Equality_Instances
20:46:25Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
20:46:25Affine_Arithmetic: theory HOL-Library.Monad_Syntax
20:46:25Affine_Arithmetic: theory Deriving.Compare
20:46:25Affine_Arithmetic: theory Deriving.Comparator_Generator
20:46:25Affine_Arithmetic: theory HOL-Library.Char_ord
20:46:26Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
20:46:26Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
20:46:26Affine_Arithmetic: theory HOL-Library.Code_Target_Int
20:46:26Affine_Arithmetic: theory HOL-Combinatorics.List_Permutation
20:46:26Affine_Arithmetic: theory Deriving.Compare_Generator
20:46:26Affine_Arithmetic: theory HOL-Library.Mapping
20:46:26Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
20:46:26Finished Simple_Firewall/document (0:00:10 elapsed time)
20:46:26Preparing Simple_Firewall/outline ...
20:46:27Affine_Arithmetic: theory HOL-Library.Code_Cardinality
20:46:27Affine_Arithmetic: theory Deriving.Compare_Instances
20:46:27Affine_Arithmetic: theory HOL-Library.Type_Length
20:46:27Correctness_Algebras: theory Correctness_Algebras.Test_Iterings
20:46:28Affine_Arithmetic: theory HOL-Library.RBT_Impl
20:46:28Affine_Arithmetic: theory HOL-Library.Signed_Division
20:46:28Affine_Arithmetic: theory HOL-Library.Word
20:46:28Affine_Arithmetic: theory Deriving.Countable_Generator
20:46:28Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
20:46:29Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
20:46:29Affine_Arithmetic: theory HOL-Library.Log_Nat
20:46:29Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
20:46:30Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
20:46:30Correctness_Algebras: theory Correctness_Algebras.Omega_Algebras
20:46:30Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
20:46:31Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
20:46:31Quantales_Converse: theory Order_Lattice_Props.Order_Duality
20:46:32Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
20:46:32Correctness_Algebras: theory Correctness_Algebras.Hoare_Modal
20:46:33Affine_Arithmetic: theory Affine_Arithmetic.Polygon
20:46:33Affine_Arithmetic: theory List-Index.List_Index
20:46:34Finished Stone_Algebras/document (0:00:09 elapsed time)
20:46:34Preparing Stone_Algebras/outline ...
20:46:34Affine_Arithmetic: theory Native_Word.Code_Int_Integer_Conversion
20:46:34Affine_Arithmetic: theory Show.Show
20:46:35Finished Simple_Firewall/outline (0:00:08 elapsed time)
20:46:35Timing Simple_Firewall (4 threads, 26.764s elapsed time, 96.114s cpu time, 2.455s GC time, factor 3.59)
20:46:35Finished Simple_Firewall (0:00:42 elapsed time, 0:02:01 cpu time, factor 2.83)
20:46:35Building HRB-Slicing ...
20:46:36Affine_Arithmetic: theory Show.Show_Instances
20:46:36Affine_Arithmetic: theory HOL-Library.Interval
20:46:37Affine_Arithmetic: theory HOL-Library.Float
20:46:37HRB-Slicing: theory HRB-Slicing.AuxLemmas
20:46:38HRB-Slicing: theory HRB-Slicing.BasicDefs
20:46:39Finished Stone_Algebras/outline (0:00:05 elapsed time)
20:46:39Timing Stone_Algebras (4 threads, 75.860s elapsed time, 141.167s cpu time, 3.354s GC time, factor 1.86)
20:46:39Finished Stone_Algebras (0:01:27 elapsed time, 0:02:38 cpu time, factor 1.81)
20:46:39Building Ordinal ...
20:46:39Affine_Arithmetic: theory Word_Lib.Bit_Comprehension
20:46:40Affine_Arithmetic: theory Word_Lib.More_Divides
20:46:40HRB-Slicing: theory HRB-Slicing.Com
20:46:40HRB-Slicing: theory HRB-Slicing.CFG
20:46:40HRB-Slicing: theory HRB-Slicing.JVMCFG
20:46:40Affine_Arithmetic: theory Word_Lib.Signed_Division_Word
20:46:40Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
20:46:40Ordinal: theory Ordinal.OrdinalDef
20:46:41Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral_Float
20:46:41Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
20:46:41Affine_Arithmetic: theory HOL-Library.Interval_Float
20:46:41Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
20:46:41Affine_Arithmetic: theory Word_Lib.More_Arithmetic
20:46:41Affine_Arithmetic: theory Word_Lib.More_Bit_Ring
20:46:42Quantales_Converse: theory Kleene_Algebra.Conway
20:46:42Ordinal: theory Ordinal.OrdinalInduct
20:46:42Ordinal: theory Ordinal.OrdinalCont
20:46:42Ordinal: theory Ordinal.OrdinalRec
20:46:43Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
20:46:43Ordinal: theory Ordinal.OrdinalArith
20:46:43Affine_Arithmetic: theory Word_Lib.More_Word
20:46:43Ordinal: theory Ordinal.OrdinalInverse
20:46:43Quantales_Converse: theory Order_Lattice_Props.Order_Lattice_Props
20:46:43Ordinal: theory Ordinal.OrdinalFix
20:46:44Ordinal: theory Ordinal.OrdinalOmega
20:46:44Ordinal: theory Ordinal.OrdinalVeblen
20:46:45Ordinal: theory Ordinal.Ordinal
20:46:45HRB-Slicing: theory HRB-Slicing.Labels
20:46:46HRB-Slicing: theory HRB-Slicing.ProcState
20:46:48Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base
20:46:48HRB-Slicing: theory HRB-Slicing.PCFG
20:46:49Affine_Arithmetic: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:46:49Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
20:46:50HRB-Slicing: theory HRB-Slicing.CFGExit
20:46:50Affine_Arithmetic: theory Word_Lib.Least_significant_bit
20:46:50HRB-Slicing: theory HRB-Slicing.CFG_wf
20:46:51Affine_Arithmetic: theory Word_Lib.Most_significant_bit
20:46:51HRB-Slicing: theory HRB-Slicing.Distance
20:46:51HRB-Slicing: theory HRB-Slicing.Postdomination
20:46:51Affine_Arithmetic: theory Word_Lib.Generic_set_bit
20:46:51HRB-Slicing: theory HRB-Slicing.ReturnAndCallNodes
20:46:51HRB-Slicing: theory HRB-Slicing.SemanticsCFG
20:46:52HRB-Slicing: theory HRB-Slicing.Observable
20:46:52Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
20:46:52HRB-Slicing: theory HRB-Slicing.CFGExit_wf
20:46:52HRB-Slicing: theory HRB-Slicing.WellFormProgs
20:46:52Correctness_Algebras: theory Correctness_Algebras.Binary_Iterings_Nonstrict
20:46:52Affine_Arithmetic: theory Affine_Arithmetic.Intersection
20:46:52Correctness_Algebras: theory Correctness_Algebras.Capped_Omega_Algebras
20:46:53HRB-Slicing: theory HRB-Slicing.Interpretation
20:46:53Affine_Arithmetic: theory Native_Word.Code_Target_Integer_Bit
20:46:53HRB-Slicing: theory HRB-Slicing.JVMInterpretation
20:46:54HRB-Slicing: theory HRB-Slicing.SDG
20:46:55HRB-Slicing: theory HRB-Slicing.WellFormed
20:46:55HRB-Slicing: theory HRB-Slicing.JVMCFG_wf
20:46:55HRB-Slicing: theory HRB-Slicing.JVMPostdomination
20:46:56Quantales_Converse: theory Kleene_Algebra.Kleene_Algebra
20:46:56HRB-Slicing: theory HRB-Slicing.ValidPaths
20:46:56Correctness_Algebras: theory Correctness_Algebras.Domain_Iterings
20:46:58Affine_Arithmetic: theory Native_Word.Word_Type_Copies
20:47:02HRB-Slicing: theory HRB-Slicing.HRBSlice
20:47:02HRB-Slicing: theory HRB-Slicing.ProcSDG
20:47:02HRB-Slicing: theory HRB-Slicing.JVMSDG
20:47:02Quantales_Converse: theory Order_Lattice_Props.Galois_Connections
20:47:02Quantales_Converse: theory Order_Lattice_Props.Closure_Operators
20:47:04Preparing Ordinal/document ...
20:47:04Correctness_Algebras: theory Correctness_Algebras.Extended_Designs
20:47:04HRB-Slicing: theory HRB-Slicing.SCDObservable
20:47:05Correctness_Algebras: theory Correctness_Algebras.General_Refinement_Algebras
20:47:05Quantales_Converse: theory Quantales.Quantales
20:47:06HRB-Slicing: theory HRB-Slicing.Slice
20:47:08Finished Ordinal/document (0:00:04 elapsed time)
20:47:08Preparing Ordinal/outline ...
20:47:09Quantales_Converse: theory KAD.Domain_Semiring
20:47:09Quantales_Converse: theory Quantales_Converse.Kleene_Algebra_Converse
20:47:09HRB-Slicing: theory HRB-Slicing.WeakSimulation
20:47:11Finished Ordinal/outline (0:00:03 elapsed time)
20:47:11Affine_Arithmetic: theory Native_Word.Uint32
20:47:11Timing Ordinal (4 threads, 14.699s elapsed time, 38.337s cpu time, 0.594s GC time, factor 2.61)
20:47:11Finished Ordinal (0:00:24 elapsed time, 0:00:52 cpu time, factor 2.15)
20:47:11Building Routing ...
20:47:13Affine_Arithmetic: theory Collections.HashCode
20:47:13HRB-Slicing: theory HRB-Slicing.FundamentalProperty
20:47:14Routing: theory Routing.Linorder_Helper
20:47:14Routing: theory Pure-ex.Guess
20:47:14Routing: theory HOL-Library.Adhoc_Overloading
20:47:14Affine_Arithmetic: theory Deriving.Hash_Generator
20:47:15Routing: theory HOL-Library.Monad_Syntax
20:47:16Routing: theory Routing.Routing_Table
20:47:16Affine_Arithmetic: theory Deriving.Hash_Instances
20:47:16Affine_Arithmetic: theory Deriving.Derive
20:47:19Correctness_Algebras: theory Correctness_Algebras.Domain_Recursion
20:47:20Routing: theory Routing.IpRoute_Parser
20:47:20HRB-Slicing: theory HRB-Slicing.HRBSlicing
20:47:20Routing: theory Routing.Linux_Router
20:47:22Correctness_Algebras: theory Correctness_Algebras.N_Omega_Algebras
20:47:25Correctness_Algebras: theory Correctness_Algebras.N_Semirings
20:47:28Quantales_Converse: theory KAD.Antidomain_Semiring
20:47:41Correctness_Algebras: theory Correctness_Algebras.Pre_Post_Modal
20:47:43Preparing Routing/document ...
20:47:45Correctness_Algebras: theory Correctness_Algebras.N_Semirings_Boolean
20:47:46Finished Routing/document (0:00:03 elapsed time)
20:47:46Preparing Routing/outline ...
20:47:46Correctness_Algebras: theory Correctness_Algebras.Recursion_Strict
20:47:49Finished Routing/outline (0:00:02 elapsed time)
20:47:49Timing Routing (4 threads, 15.359s elapsed time, 43.775s cpu time, 0.619s GC time, factor 2.85)
20:47:49Finished Routing (0:00:31 elapsed time, 0:01:07 cpu time, factor 2.15)
20:47:49Running Network_Security_Policy_Verification ...
20:47:51Affine_Arithmetic: theory HOL-Library.RBT
20:47:51Network_Security_Policy_Verification: theory HOL-Eisbach.Eisbach
20:47:51Network_Security_Policy_Verification: theory HOL-Library.Cancellation
20:47:51Network_Security_Policy_Verification: theory HOL-Library.Char_ord
20:47:51Network_Security_Policy_Verification: theory HOL-Library.Code_Abstract_Nat
20:47:52Network_Security_Policy_Verification: theory HOL-Library.Infinite_Set
20:47:52Network_Security_Policy_Verification: theory HOL-Library.Code_Target_Nat
20:47:52Correctness_Algebras: theory Correctness_Algebras.N_Omega_Binary_Iterings
20:47:52Network_Security_Policy_Verification: theory HOL-Library.List_Lexorder
20:47:52Network_Security_Policy_Verification: theory HOL-Library.Option_ord
20:47:53Network_Security_Policy_Verification: theory HOL-Library.Product_Lexorder
20:47:54Network_Security_Policy_Verification: theory HOL-Library.RBT_Impl
20:47:54Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph
20:47:54Network_Security_Policy_Verification: theory HOL-Library.Multiset
20:47:54Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz
20:47:54Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable
20:47:54Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util
20:47:54Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_Impl
20:47:54Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_List_Impl
20:47:55Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph
20:47:55Affine_Arithmetic: theory HOL-Library.RBT_Mapping
20:47:56Quantales_Converse: theory KAD.Range_Semiring
20:48:00Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
20:48:02Correctness_Algebras: theory Correctness_Algebras.N_Semirings_Modal
20:48:03Network_Security_Policy_Verification: theory HOL-ex.Quicksort
20:48:04Network_Security_Policy_Verification: theory Automatic_Refinement.Misc
20:48:05Native_Word: theory Native_Word.Native_Word_Test_Emu
20:48:05Native_Word: theory Native_Word.Native_Word_Test_PolyML64
20:48:05Native_Word: theory Native_Word.Native_Word_Test_PolyML
20:48:05Native_Word: theory Native_Word.Native_Word_Test_Scala
20:48:07Correctness_Algebras: theory Correctness_Algebras.Monotonic_Boolean_Transformers_Instances
20:48:13Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct
20:48:15Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
20:48:16Correctness_Algebras: theory Correctness_Algebras.N_Relation_Algebras
20:48:26Preparing Goedel_HFSet_Semantic/document ...
20:48:28Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
20:48:29Finished Goedel_HFSet_Semantic/document (0:00:02 elapsed time)
20:48:29Preparing Goedel_HFSet_Semantic/outline ...
20:48:31Finished Goedel_HFSet_Semantic/outline (0:00:02 elapsed time)
20:48:31Timing Goedel_HFSet_Semantic (4 threads, 805.734s elapsed time, 1978.446s cpu time, 15.489s GC time, factor 2.46)
20:48:31Finished Goedel_HFSet_Semantic (0:13:29 elapsed time, 0:33:04 cpu time, factor 2.45)
20:48:31Building Nested_Multisets_Ordinals ...
20:48:33Quantales_Converse: theory KAD.Modal_Kleene_Algebra
20:48:33Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Var
20:48:33Nested_Multisets_Ordinals: theory HOL-Library.Cancellation
20:48:33Nested_Multisets_Ordinals: theory HOL-Library.Infinite_Set
20:48:33Nested_Multisets_Ordinals: theory HOL-Library.Nat_Bijection
20:48:33Nested_Multisets_Ordinals: theory HOL-Library.Old_Datatype
20:48:34Nested_Multisets_Ordinals: theory HOL-Library.Product_Plus
20:48:35Nested_Multisets_Ordinals: theory HOL-Library.Sublist
20:48:36Nested_Multisets_Ordinals: theory HOL-Library.Product_Order
20:48:36Nested_Multisets_Ordinals: theory HOL-Library.Countable
20:48:36Nested_Multisets_Ordinals: theory HOL-Library.Multiset
20:48:36Nested_Multisets_Ordinals: theory List-Index.List_Index
20:48:38Nested_Multisets_Ordinals: theory HOL-Library.Countable_Set
20:48:38Nested_Multisets_Ordinals: theory HOL-Library.FSet
20:48:39Nested_Multisets_Ordinals: theory HOL-Library.Countable_Complete_Lattices
20:48:39Nested_Multisets_Ordinals: theory HOL-Library.Countable_Set_Type
20:48:40Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
20:48:40Native_Word: theory Native_Word.Native_Word_Test_PolyML2
20:48:44Affine_Arithmetic: theory Affine_Arithmetic.Print
20:48:44Nested_Multisets_Ordinals: theory HOL-Library.Order_Continuity
20:48:45Quantales_Converse: theory Quantales.Quantale_Star
20:48:46Nested_Multisets_Ordinals: theory HOL-Library.Extended_Nat
20:48:46Nested_Multisets_Ordinals: theory HOL-Library.Multiset_Order
20:48:47Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.McCarthy_91
20:48:47Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nested_Multiset
20:48:47Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_More
20:48:48Native_Word: theory Native_Word.Native_Word_Test_GHC
20:48:48Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
20:48:48Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
20:48:48Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Multiset
20:48:48Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hereditary_Multiset
20:48:48Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Converse
20:48:49Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
20:48:50Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal
20:48:50Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Unary_PCF
20:48:51Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset
20:48:51Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Goodstein_Sequence
20:48:51Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hydra_Battle
20:48:52Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal
20:48:52Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge
20:49:06Native_Word: theory Native_Word.Native_Word_Test_MLton
20:49:06Native_Word: theory Native_Word.Native_Word_Test_MLton2
20:49:21Quantales_Converse: theory Quantales_Converse.Modal_Quantale
20:49:22Network_Security_Policy_Verification: theory HOL-Library.RBT
20:49:23Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl
20:49:24Native_Word: theory Native_Word.Native_Word_Test_OCaml
20:49:24Native_Word: theory Native_Word.Native_Word_Test_OCaml2
20:49:35Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
20:49:36Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2
20:49:36Native_Word: theory Native_Word.Native_Word_Test_SMLNJ
20:49:50Native_Word: theory Native_Word.Uint_Userguide
20:50:03Preparing Native_Word/document ...
20:50:14Finished Native_Word/document (0:00:10 elapsed time)
20:50:14Preparing Native_Word/outline ...
20:50:24Finished Native_Word/outline (0:00:10 elapsed time)
20:50:25Timing Native_Word (4 threads, 782.769s elapsed time, 839.933s cpu time, 23.843s GC time, factor 1.07)
20:50:25Finished Native_Word (0:13:06 elapsed time, 0:14:05 cpu time, factor 1.08)
20:50:25Building Projective_Measurements ...
20:50:32Projective_Measurements: theory HOL-Computational_Algebra.Fraction_Field
20:50:32Projective_Measurements: theory HOL-Algebra.Congruence
20:50:32Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
20:50:32Projective_Measurements: theory Abstract-Rewriting.Seq
20:50:32Projective_Measurements: theory HOL-Library.More_List
20:50:33Projective_Measurements: theory HOL-Library.While_Combinator
20:50:33Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
20:50:33Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
20:50:34Projective_Measurements: theory HOL-Algebra.Order
20:50:34Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
20:50:34Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
20:50:34Projective_Measurements: theory HOL-Computational_Algebra.Normalized_Fraction
20:50:36Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
20:50:36Projective_Measurements: theory HOL-Algebra.Lattice
20:50:36Projective_Measurements: theory Jordan_Normal_Form.Conjugate
20:50:37Projective_Measurements: theory Matrix.Utility
20:50:37Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
20:50:37Projective_Measurements: theory HOL-Algebra.Complete_Lattice
20:50:39Projective_Measurements: theory HOL-Algebra.Group
20:50:42Projective_Measurements: theory HOL-Algebra.Coset
20:50:43Projective_Measurements: theory HOL-Algebra.FiniteProduct
20:50:44Projective_Measurements: theory HOL-Algebra.Ring
20:50:45Projective_Measurements: theory Regular-Sets.Regular_Set
20:50:46Projective_Measurements: theory VectorSpace.FunctionLemmas
20:50:48Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
20:50:48Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
20:50:50Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
20:50:50Projective_Measurements: theory HOL-Algebra.Module
20:50:50Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
20:50:50Projective_Measurements: theory Regular-Sets.Regular_Exp
20:50:51Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
20:50:51Network_Security_Policy_Verification: theory HOL-Lattice.Orders
20:50:51Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Vertices
20:50:52Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
20:50:52Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
20:50:52Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface
20:50:52Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.vertex_example_simps
20:50:53Network_Security_Policy_Verification: theory HOL-Lattice.Bounds
20:50:53Projective_Measurements: theory VectorSpace.RingModuleFacts
20:50:53Network_Security_Policy_Verification: theory HOL-Lattice.Lattice
20:50:54Network_Security_Policy_Verification: theory HOL-Lattice.CompleteLattice
20:50:54Projective_Measurements: theory VectorSpace.MonoidSums
20:50:54Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_withOffendingFlows
20:50:55Projective_Measurements: theory VectorSpace.LinearCombinations
20:50:56Projective_Measurements: theory Regular-Sets.NDerivative
20:50:56Projective_Measurements: theory Regular-Sets.Relation_Interpretation
20:50:57Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_ENF
20:50:57Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Helper
20:50:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith
20:50:58Projective_Measurements: theory Jordan_Normal_Form.Matrix
20:50:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic
20:50:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPstrict
20:50:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith
20:50:58Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted
20:50:59Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners
20:50:59Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability
20:50:59Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl
20:51:00Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG
20:51:00Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl
20:51:00Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference
20:51:01Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt
20:51:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink
20:51:02Projective_Measurements: theory Regular-Sets.Equivalence_Checking
20:51:02Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets
20:51:02Projective_Measurements: theory Regular-Sets.Regexp_Method
20:51:02Projective_Measurements: theory VectorSpace.SumSpaces
20:51:03Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
20:51:03Projective_Measurements: theory VectorSpace.VectorSpace
20:51:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets2
20:51:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW
20:51:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting
20:51:05Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
20:51:05Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted
20:51:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory
20:51:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface_impl
20:51:07Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Analysis_Tainting
20:51:07Projective_Measurements: theory Abstract-Rewriting.SN_Orders
20:51:08Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
20:51:08Projective_Measurements: theory Jordan_Normal_Form.Determinant
20:51:08Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy
20:51:08Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl
20:51:08Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl
20:51:09Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl
20:51:09Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl
20:51:09Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl
20:51:09Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm
20:51:10Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_impl
20:51:10Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
20:51:11Projective_Measurements: theory Matrix.Ordered_Semiring
20:51:11Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl
20:51:11Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl
20:51:11Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
20:51:11Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl
20:51:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl
20:51:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl
20:51:12Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
20:51:12Projective_Measurements: theory Matrix.Matrix_Legacy
20:51:13Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink_impl
20:51:13Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
20:51:13Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
20:51:14Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl
20:51:14Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
20:51:14Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets_impl
20:51:15Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl
20:51:15Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
20:51:18Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
20:51:19Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
20:51:19Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting_impl
20:51:19Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl
20:51:19Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
20:51:20Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
20:51:22Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary
20:51:24Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl
20:51:36Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
20:51:39Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
20:51:40Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Library
20:51:45Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
20:51:46Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_BLP
20:51:46Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Impl
20:51:46Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_generateCode
20:51:47Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Network_Security_Policy_Verification
20:51:51Projective_Measurements: theory QHLProver.Complex_Matrix
20:51:57Projective_Measurements: theory QHLProver.Gates
20:51:57Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
20:52:06Projective_Measurements: theory Projective_Measurements.Projective_Measurements
20:52:08Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.attic
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_NetModel
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CryptoDB
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Distributed_WebApp
20:52:12Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_Forte14
20:52:13Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.I8_SSH_Landscape
20:52:17Quantales_Converse: theory Quantales_Converse.Quantale_Converse
20:52:19Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.IDEM
20:52:20Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground
20:52:21Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork
20:52:21Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example
20:52:22Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance
20:52:22Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.MeasrDroid
20:52:25Preparing Formal_SSA/document ...
20:52:43Finished Formal_SSA/document (0:00:17 elapsed time)
20:52:43Preparing Formal_SSA/outline ...
20:52:53Finished Formal_SSA/outline (0:00:09 elapsed time)
20:52:53Timing Formal_SSA (4 threads, 660.009s elapsed time, 1277.179s cpu time, 15.112s GC time, factor 1.94)
20:52:53Finished Formal_SSA (0:11:45 elapsed time, 0:22:39 cpu time, factor 1.93)
20:52:53Building Iptables_Semantics ...
20:52:56Iptables_Semantics: theory Iptables_Semantics.List_Misc
20:52:56Iptables_Semantics: theory Iptables_Semantics.Negation_Type
20:52:59Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
20:53:00Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
20:53:00Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
20:53:00Iptables_Semantics: theory HOL-Library.Code_Target_Int
20:53:00Iptables_Semantics: theory HOL-Library.LaTeXsugar
20:53:01Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
20:53:01Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
20:53:01Iptables_Semantics: theory Iptables_Semantics.Ternary
20:53:01Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion
20:53:01Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
20:53:01Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
20:53:01Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
20:53:03Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit
20:53:03Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
20:53:04Iptables_Semantics: theory Iptables_Semantics.Ports
20:53:06Iptables_Semantics: theory Iptables_Semantics.Word_Upto
20:53:06Iptables_Semantics: theory Iptables_Semantics.IpAddresses
20:53:10Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
20:53:27Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
20:53:27Iptables_Semantics: theory Iptables_Semantics.Semantics
20:53:28Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
20:53:30Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
20:53:32Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
20:53:32Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
20:53:33Iptables_Semantics: theory Iptables_Semantics.Matching
20:53:33Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
20:53:34Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
20:53:34Iptables_Semantics: theory Iptables_Semantics.Optimizing
20:53:34Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
20:53:35Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
20:53:35Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
20:53:35Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
20:53:37Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
20:53:38Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
20:53:39Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit
20:53:39Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
20:53:42Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
20:53:42Iptables_Semantics: theory Iptables_Semantics.Ipassmt
20:53:44Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
20:53:46Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
20:53:50Preparing Nested_Multisets_Ordinals/document ...
20:53:57Finished Nested_Multisets_Ordinals/document (0:00:07 elapsed time)
20:53:57Preparing Nested_Multisets_Ordinals/outline ...
20:54:02Finished Nested_Multisets_Ordinals/outline (0:00:05 elapsed time)
20:54:03Timing Nested_Multisets_Ordinals (4 threads, 293.148s elapsed time, 540.298s cpu time, 9.963s GC time, factor 1.84)
20:54:03Finished Nested_Multisets_Ordinals (0:05:15 elapsed time, 0:09:37 cpu time, factor 1.83)
20:54:03Running Universal_Hash_Families ...
20:54:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Examples
20:54:04Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Imaginary_Factory_Network
20:54:07Universal_Hash_Families: theory Flow_Networks.Graph
20:54:07Universal_Hash_Families: theory Digit_Expansions.Bits_Digits
20:54:08Universal_Hash_Families: theory HOL-Computational_Algebra.Group_Closure
20:54:08Universal_Hash_Families: theory HOL-Computational_Algebra.Fraction_Field
20:54:09Universal_Hash_Families: theory HOL-Computational_Algebra.Nth_Powers
20:54:10Universal_Hash_Families: theory HOL-Computational_Algebra.Squarefree
20:54:10Universal_Hash_Families: theory HOL-Number_Theory.Cong
20:54:10Universal_Hash_Families: theory HOL-Library.Case_Converter
20:54:11Universal_Hash_Families: theory HOL-Library.Code_Lazy
20:54:11Universal_Hash_Families: theory HOL-Computational_Algebra.Normalized_Fraction
20:54:12Universal_Hash_Families: theory Flow_Networks.Network
20:54:12Universal_Hash_Families: theory Finite_Fields.Finite_Fields_More_Bijections
20:54:13Universal_Hash_Families: theory HOL-Algebra.Congruence
20:54:13Universal_Hash_Families: theory HOL-Combinatorics.List_Permutation
20:54:13Universal_Hash_Families: theory HOL-Library.Function_Algebras
20:54:13Universal_Hash_Families: theory HOL-Library.More_List
20:54:13Universal_Hash_Families: theory HOL-Library.Power_By_Squaring
20:54:14Universal_Hash_Families: theory HOL-Library.Transitive_Closure_Table
20:54:14Universal_Hash_Families: theory HOL-Number_Theory.Mod_Exp
20:54:14Universal_Hash_Families: theory HOL-Algebra.Order
20:54:14Universal_Hash_Families: theory HOL-Library.While_Combinator
20:54:14Universal_Hash_Families: theory Flow_Networks.Residual_Graph
20:54:14Universal_Hash_Families: theory HOL-Number_Theory.Eratosthenes
20:54:15Universal_Hash_Families: theory HOL-Types_To_Sets.Types_To_Sets
20:54:15Universal_Hash_Families: theory HOL-Library.Bourbaki_Witt_Fixpoint
20:54:16Universal_Hash_Families: theory HOL-Algebra.Lattice
20:54:16Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial
20:54:17Universal_Hash_Families: theory HOL-Library.Going_To_Filter
20:54:17Universal_Hash_Families: theory HOL-Library.Log_Nat
20:54:17Universal_Hash_Families: theory Executable_Randomized_Algorithms.Tau_Additivity
20:54:17Universal_Hash_Families: theory HOL-Number_Theory.Fib
20:54:18Universal_Hash_Families: theory HOL-Algebra.Complete_Lattice
20:54:18Universal_Hash_Families: theory HOL-Number_Theory.Prime_Powers
20:54:18Universal_Hash_Families: theory Flow_Networks.Augmenting_Flow
20:54:18Universal_Hash_Families: theory Flow_Networks.Augmenting_Path
20:54:18Universal_Hash_Families: theory Flow_Networks.Ford_Fulkerson
20:54:19Universal_Hash_Families: theory HOL-Algebra.Group
20:54:19Universal_Hash_Families: theory HOL-Number_Theory.Totient
20:54:19Universal_Hash_Families: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
20:54:20Universal_Hash_Families: theory HOL-Complex_Analysis.Contour_Integration
20:54:22Universal_Hash_Families: theory MFMC_Countable.MFMC_Finite
20:54:23Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families
20:54:25Universal_Hash_Families: theory HOL-Algebra.Coset
20:54:25Universal_Hash_Families: theory HOL-Algebra.FiniteProduct
20:54:25Universal_Hash_Families: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
20:54:26Universal_Hash_Families: theory HOL-Algebra.Ring
20:54:28Universal_Hash_Families: theory HOL-Complex_Analysis.Winding_Numbers
20:54:30Universal_Hash_Families: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
20:54:30Universal_Hash_Families: theory HOL-Algebra.Generated_Groups
20:54:32Universal_Hash_Families: theory HOL-Algebra.Divisibility
20:54:34Universal_Hash_Families: theory HOL-Algebra.Elementary_Groups
20:54:35Universal_Hash_Families: theory HOL-Complex_Analysis.Conformal_Mappings
20:54:35Universal_Hash_Families: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
20:54:37Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
20:54:37Universal_Hash_Families: theory HOL-Algebra.AbelCoset
20:54:37Universal_Hash_Families: theory HOL-Algebra.Module
20:54:39Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial_FPS
20:54:39Universal_Hash_Families: theory HOL-Computational_Algebra.Polynomial_Factorial
20:54:39Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Singularities
20:54:40Universal_Hash_Families: theory HOL-Computational_Algebra.Formal_Laurent_Series
20:54:42Universal_Hash_Families: theory HOL-Complex_Analysis.Great_Picard
20:54:43Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Residues
20:54:43Universal_Hash_Families: theory HOL-Algebra.Ideal
20:54:44Universal_Hash_Families: theory HOL-Complex_Analysis.Residue_Theorem
20:54:44Universal_Hash_Families: theory HOL-Complex_Analysis.Riemann_Mapping
20:54:45Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
20:54:45Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
20:54:45Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
20:54:46Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
20:54:46Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
20:54:46Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
20:54:46Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
20:54:46Universal_Hash_Families: theory Ergodic_Theory.SG_Library_Complement
20:54:48Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
20:54:48Iptables_Semantics: theory Iptables_Semantics.No_Spoof
20:54:49Universal_Hash_Families: theory Executable_Randomized_Algorithms.Coin_Space
20:54:49Universal_Hash_Families: theory MFMC_Countable.MFMC_Misc
20:54:50Universal_Hash_Families: theory HOL-Computational_Algebra.Computational_Algebra
20:54:50Universal_Hash_Families: theory HOL-Complex_Analysis.Laurent_Convergence
20:54:50Universal_Hash_Families: theory HOL-Algebra.RingHom
20:54:51Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
20:54:51Universal_Hash_Families: theory MFMC_Countable.Matrix_For_Marginals
20:54:52Universal_Hash_Families: theory Lp.Functional_Spaces
20:54:52Universal_Hash_Families: theory HOL-Algebra.QuotRing
20:54:54Universal_Hash_Families: theory HOL-Algebra.UnivPoly
20:54:55Universal_Hash_Families: theory HOL-Complex_Analysis.Meromorphic
20:54:55Universal_Hash_Families: theory HOL-Algebra.IntRing
20:54:56Universal_Hash_Families: theory MFMC_Countable.Rel_PMF_Characterisation
20:54:56Universal_Hash_Families: theory HOL-Complex_Analysis.Weierstrass_Factorization
20:54:56Universal_Hash_Families: theory Probabilistic_While.While_SPMF
20:54:57Universal_Hash_Families: theory HOL-Complex_Analysis.Complex_Analysis
20:54:57Universal_Hash_Families: theory Lp.Lp
20:54:57Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
20:54:59Universal_Hash_Families: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
20:55:00Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
20:55:00Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
20:55:01Universal_Hash_Families: theory Universal_Hash_Families.Pseudorandom_Objects
20:55:03Iptables_Semantics: theory Iptables_Semantics.Transform
20:55:07Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
20:55:08Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
20:55:12Universal_Hash_Families: theory HOL-Algebra.Multiplicative_Group
20:55:14Iptables_Semantics: theory Iptables_Semantics.Code_Interface
20:55:14Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
20:55:16Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
20:55:16Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
20:55:16Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
20:55:17Universal_Hash_Families: theory HOL-Algebra.Ring_Divisibility
20:55:17Universal_Hash_Families: theory HOL-Algebra.Subrings
20:55:18Universal_Hash_Families: theory HOL-Number_Theory.Residues
20:55:21Universal_Hash_Families: theory HOL-Algebra.Embedded_Algebras
20:55:21Iptables_Semantics: theory Iptables_Semantics.Parser
20:55:21Iptables_Semantics: theory Iptables_Semantics.Parser6
20:55:22Universal_Hash_Families: theory HOL-Number_Theory.Euler_Criterion
20:55:22Universal_Hash_Families: theory HOL-Number_Theory.Pocklington
20:55:22Universal_Hash_Families: theory HOL-Number_Theory.Gauss
20:55:23Iptables_Semantics: theory Iptables_Semantics.Documentation
20:55:23Universal_Hash_Families: theory HOL-Number_Theory.Quadratic_Reciprocity
20:55:23Universal_Hash_Families: theory HOL-Number_Theory.Residue_Primitive_Roots
20:55:23Iptables_Semantics: theory Iptables_Semantics.Code_haskell
20:55:24Preparing Correctness_Algebras/document ...
20:55:24Universal_Hash_Families: theory HOL-Number_Theory.Number_Theory
20:55:29Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Misc
20:55:29Universal_Hash_Families: theory Dirichlet_Series.Multiplicative_Function
20:55:30Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Product
20:55:30Universal_Hash_Families: theory Dirichlet_Series.Euler_Products
20:55:31Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Series
20:55:34Universal_Hash_Families: theory HOL-Algebra.Polynomials
20:55:38Universal_Hash_Families: theory Dirichlet_Series.Moebius_Mu
20:55:38Universal_Hash_Families: theory Dirichlet_Series.More_Totient
20:55:38Universal_Hash_Families: theory Dirichlet_Series.Divisor_Count
20:55:38Universal_Hash_Families: theory Dirichlet_Series.Liouville_Lambda
20:55:39Universal_Hash_Families: theory Dirichlet_Series.Arithmetic_Summatory
20:55:39Universal_Hash_Families: theory Dirichlet_Series.Partial_Summation
20:55:41Preparing Network_Security_Policy_Verification/document ...
20:55:42Universal_Hash_Families: theory Dirichlet_Series.Dirichlet_Series_Analysis
20:55:49Finished Correctness_Algebras/document (0:00:24 elapsed time)
20:55:49Preparing Correctness_Algebras/outline ...
20:55:52Universal_Hash_Families: theory Zeta_Function.Zeta_Library
20:55:52Universal_Hash_Families: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
20:55:55Universal_Hash_Families: theory HOL-Algebra.Polynomial_Divisibility
20:55:56Universal_Hash_Families: theory Executable_Randomized_Algorithms.Randomized_Algorithm
20:56:01Finished Network_Security_Policy_Verification/document (0:00:20 elapsed time)
20:56:01Preparing Network_Security_Policy_Verification/outline ...
20:56:02Finished Correctness_Algebras/outline (0:00:13 elapsed time)
20:56:03Timing Correctness_Algebras (4 threads, 668.928s elapsed time, 1883.076s cpu time, 86.064s GC time, factor 2.82)
20:56:03Finished Correctness_Algebras (0:11:14 elapsed time, 0:31:37 cpu time, factor 2.81)
20:56:03Running FSM_Tests ...
20:56:05FSM_Tests: theory HOL-Eisbach.Eisbach
20:56:05FSM_Tests: theory Containers.Equal
20:56:05FSM_Tests: theory Containers.Extend_Partial_Order
20:56:05FSM_Tests: theory Containers.List_Fusion
20:56:05FSM_Tests: theory Containers.Closure_Set
20:56:05FSM_Tests: theory Deriving.Comparator
20:56:06FSM_Tests: theory Deriving.Derive_Manager
20:56:06FSM_Tests: theory Datatype_Order_Generator.Derive_Aux
20:56:06FSM_Tests: theory Datatype_Order_Generator.Order_Generator
20:56:07FSM_Tests: theory Deriving.Generator_Aux
20:56:08FSM_Tests: theory Containers.AssocList
20:56:09FSM_Tests: theory Deriving.Equality_Generator
20:56:09FSM_Tests: theory Deriving.Compare
20:56:09FSM_Tests: theory Deriving.Comparator_Generator
20:56:09FSM_Tests: theory Deriving.Equality_Instances
20:56:09FSM_Tests: theory Containers.Containers_Auxiliary
20:56:09FSM_Tests: theory HOL-ex.Quicksort
20:56:10FSM_Tests: theory Containers.Lexicographic_Order
20:56:10FSM_Tests: theory Containers.Containers_Generator
20:56:10FSM_Tests: theory Deriving.Compare_Generator
20:56:10FSM_Tests: theory Automatic_Refinement.Misc
20:56:10FSM_Tests: theory Containers.Set_Linorder
20:56:10FSM_Tests: theory Deriving.Compare_Instances
20:56:10FSM_Tests: theory Containers.Collection_Enum
20:56:11FSM_Tests: theory Containers.Collection_Eq
20:56:11FSM_Tests: theory Word_Lib.Bit_Comprehension
20:56:12FSM_Tests: theory Containers.DList_Set
20:56:12FSM_Tests: theory Word_Lib.More_Divides
20:56:13FSM_Tests: theory Containers.RBT_ext
20:56:13FSM_Tests: theory Deriving.RBT_Comparator_Impl
20:56:13Finished Network_Security_Policy_Verification/outline (0:00:12 elapsed time)
20:56:14Timing Network_Security_Policy_Verification (4 threads, 463.761s elapsed time, 1624.185s cpu time, 54.756s GC time, factor 3.50)
20:56:14Finished Network_Security_Policy_Verification (0:07:48 elapsed time, 0:27:13 cpu time, factor 3.49)
20:56:14Building Sepref_Basic ...
20:56:16FSM_Tests: theory Word_Lib.Signed_Division_Word
20:56:16FSM_Tests: theory FSM_Tests.Util
20:56:17FSM_Tests: theory Native_Word.Code_Int_Integer_Conversion
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.User_Smashing
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.PO_Normalizer
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.Pf_Add
20:56:17Sepref_Basic: theory HOL-Library.Rewrite
20:56:17FSM_Tests: theory Word_Lib.More_Arithmetic
20:56:17Sepref_Basic: theory List-Index.List_Index
20:56:17FSM_Tests: theory Word_Lib.More_Bit_Ring
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.Concl_Pres_Clarification
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.Named_Theorems_Rev
20:56:17Sepref_Basic: theory Refine_Imperative_HOL.Structured_Apply
20:56:18Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Id_Op
20:56:18Sepref_Basic: theory Separation_Logic_Imperative_HOL.Default_Insts
20:56:19FSM_Tests: theory Word_Lib.More_Word
20:56:19Sepref_Basic: theory Refine_Imperative_HOL.Pf_Mono_Prover
20:56:19Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Misc
20:56:19Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Basic
20:56:19Sepref_Basic: theory Refine_Imperative_HOL.Term_Synth
20:56:21FSM_Tests: theory Native_Word.Code_Target_Word_Base
20:56:21FSM_Tests: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:56:22Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Constraints
20:56:22Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Monadify
20:56:22Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Frame
20:56:22Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Rules
20:56:23FSM_Tests: theory FSM_Tests.FSM_Impl
20:56:24FSM_Tests: theory FSM_Tests.Maximal_Path_Trie
20:56:24FSM_Tests: theory FSM_Tests.Prefix_Tree
20:56:24FSM_Tests: theory Containers.Collection_Order
20:56:27FSM_Tests: theory Word_Lib.Least_significant_bit
20:56:27Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Preliminary_Results
20:56:27Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
20:56:28Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Definition
20:56:28Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
20:56:28Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
20:56:29FSM_Tests: theory Word_Lib.Most_significant_bit
20:56:29FSM_Tests: theory Word_Lib.Generic_set_bit
20:56:29FSM_Tests: theory Containers.RBT_Mapping2
20:56:29Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Translate
20:56:30FSM_Tests: theory Native_Word.Code_Target_Integer_Bit
20:56:30FSM_Tests: theory Native_Word.Word_Type_Copies
20:56:31FSM_Tests: theory Containers.RBT_Set2
20:56:31FSM_Tests: theory FSM_Tests.FSM
20:56:31Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Intf_Util
20:56:33FSM_Tests: theory Containers.Set_Impl
20:56:34Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Tool
20:56:35Sepref_Basic: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
20:56:39Universal_Hash_Families: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
20:56:40Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Foreach
20:56:41Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Factorization_Ext
20:56:42Preparing Affine_Arithmetic/document ...
20:56:42Universal_Hash_Families: theory Finite_Fields.Ring_Characteristic
20:56:42Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Improper
20:56:42Sepref_Basic: theory Refine_Imperative_HOL.Sepref
20:56:43Universal_Hash_Families: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
20:56:48FSM_Tests: theory Native_Word.Uint64
20:56:49FSM_Tests: theory FSM_Tests.Backwards_Reachability_Analysis
20:56:49FSM_Tests: theory FSM_Tests.IO_Sequence_Set
20:56:50FSM_Tests: theory FSM_Tests.Minimisation
20:56:50FSM_Tests: theory FSM_Tests.Observability
20:56:51FSM_Tests: theory FSM_Tests.Product_FSM
20:56:52FSM_Tests: theory FSM_Tests.State_Preamble
20:56:53FSM_Tests: theory FSM_Tests.State_Separator
20:56:53Preparing Quantales_Converse/document ...
20:56:53FSM_Tests: theory FSM_Tests.Distinguishability
20:56:54Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
20:56:54FSM_Tests: theory FSM_Tests.State_Cover
20:56:54Universal_Hash_Families: theory Finite_Fields.Formal_Polynomial_Derivatives
20:56:55Universal_Hash_Families: theory Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
20:56:55Universal_Hash_Families: theory Finite_Fields.Monic_Polynomial_Factorization
20:56:57FSM_Tests: theory FSM_Tests.Adaptive_Test_Case
20:56:58FSM_Tests: theory FSM_Tests.Helper_Algorithms
20:56:59Finished Quantales_Converse/document (0:00:05 elapsed time)
20:56:59Preparing Quantales_Converse/outline ...
20:56:59FSM_Tests: theory FSM_Tests.R_Distinguishability
20:56:59FSM_Tests: theory FSM_Tests.Traversal_Set
20:57:00FSM_Tests: theory FSM_Tests.Test_Suite
20:57:00FSM_Tests: theory FSM_Tests.Test_Suite_Representations
20:57:00FSM_Tests: theory FSM_Tests.OFSM_Tables_Refined
20:57:01FSM_Tests: theory FSM_Tests.Convergence
20:57:02Preparing Iptables_Semantics/document ...
20:57:03Timing Sepref_Basic (4 threads, 27.464s elapsed time, 66.632s cpu time, 1.410s GC time, factor 2.43)
20:57:03Finished Sepref_Basic (0:00:47 elapsed time, 0:01:38 cpu time, factor 2.06)
20:57:03Running AI_Planning_Languages_Semantics ...
20:57:03Universal_Hash_Families: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
20:57:03Finished Quantales_Converse/outline (0:00:04 elapsed time)
20:57:03FSM_Tests: theory FSM_Tests.Convergence_Graph
20:57:03Timing Quantales_Converse (4 threads, 609.206s elapsed time, 966.059s cpu time, 17.376s GC time, factor 1.59)
20:57:03Finished Quantales_Converse (0:10:32 elapsed time, 0:16:47 cpu time, factor 1.59)
20:57:03MFODL_Monitor_Optimized CANCELLED
20:57:04FSM_Tests: theory FSM_Tests.Empty_Convergence_Graph
20:57:04Building Stone_Relation_Algebras ...
20:57:04FSM_Tests: theory FSM_Tests.Simple_Convergence_Graph
20:57:04FSM_Tests: theory FSM_Tests.H_Framework
20:57:04AI_Planning_Languages_Semantics: theory Containers.Equal
20:57:04AI_Planning_Languages_Semantics: theory Containers.Extend_Partial_Order
20:57:04AI_Planning_Languages_Semantics: theory Containers.List_Fusion
20:57:04AI_Planning_Languages_Semantics: theory Deriving.Comparator
20:57:05AI_Planning_Languages_Semantics: theory Containers.Closure_Set
20:57:05AI_Planning_Languages_Semantics: theory Deriving.Derive_Manager
20:57:05Finished Affine_Arithmetic/document (0:00:23 elapsed time)
20:57:05Preparing Affine_Arithmetic/outline ...
20:57:05AI_Planning_Languages_Semantics: theory Deriving.Generator_Aux
20:57:05AI_Planning_Languages_Semantics: theory HOL-Library.AList
20:57:06AI_Planning_Languages_Semantics: theory Deriving.Equality_Generator
20:57:07Stone_Relation_Algebras: theory Stone_Relation_Algebras.Fixpoints
20:57:07AI_Planning_Languages_Semantics: theory Deriving.Equality_Instances
20:57:07AI_Planning_Languages_Semantics: theory Deriving.Compare
20:57:07AI_Planning_Languages_Semantics: theory Deriving.Comparator_Generator
20:57:07FSM_Tests: theory FSM_Tests.Pair_Framework
20:57:07FSM_Tests: theory FSM_Tests.Test_Suite_IO
20:57:08AI_Planning_Languages_Semantics: theory HOL-Library.Adhoc_Overloading
20:57:08AI_Planning_Languages_Semantics: theory Certification_Monads.Error_Syntax
20:57:08AI_Planning_Languages_Semantics: theory HOL-Library.Monad_Syntax
20:57:08AI_Planning_Languages_Semantics: theory HOL-Library.DAList
20:57:08AI_Planning_Languages_Semantics: theory Certification_Monads.Error_Monad
20:57:08AI_Planning_Languages_Semantics: theory Containers.Containers_Auxiliary
20:57:09FSM_Tests: theory FSM_Tests.Test_Suite_Calculation
20:57:09AI_Planning_Languages_Semantics: theory Deriving.Compare_Generator
20:57:09AI_Planning_Languages_Semantics: theory HOL-Library.Char_ord
20:57:09AI_Planning_Languages_Semantics: theory Containers.Lexicographic_Order
20:57:09AI_Planning_Languages_Semantics: theory Deriving.Compare_Instances
20:57:10AI_Planning_Languages_Semantics: theory Containers.AssocList
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.Code_Abstract_Nat
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.Code_Target_Nat
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.Mapping
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.Phantom_Type
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.RBT_Impl
20:57:10AI_Planning_Languages_Semantics: theory HOL-Library.Rewrite
20:57:10Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
20:57:10Universal_Hash_Families: theory Finite_Fields.Rabin_Irreducibility_Test
20:57:10Universal_Hash_Families: theory Finite_Fields.Card_Irreducible_Polynomials
20:57:10Stone_Relation_Algebras: theory Stone_Relation_Algebras.Semirings
20:57:11AI_Planning_Languages_Semantics: theory Show.Show
20:57:11FSM_Tests: theory FSM_Tests.SPY_Framework
20:57:11AI_Planning_Languages_Semantics: theory Containers.Containers_Generator
20:57:12AI_Planning_Languages_Semantics: theory HOL-Library.Cardinality
20:57:13AI_Planning_Languages_Semantics: theory Containers.Collection_Enum
20:57:13AI_Planning_Languages_Semantics: theory Containers.Collection_Eq
20:57:14AI_Planning_Languages_Semantics: theory Containers.Set_Linorder
20:57:14AI_Planning_Languages_Semantics: theory Containers.DList_Set
20:57:15FSM_Tests: theory FSM_Tests.Prime_Transformation
20:57:17Universal_Hash_Families: theory Finite_Fields.Rabin_Irreducibility_Test_Code
20:57:18Finished Affine_Arithmetic/outline (0:00:12 elapsed time)
20:57:19Timing Affine_Arithmetic (4 threads, 564.342s elapsed time, 1937.150s cpu time, 93.593s GC time, factor 3.43)
20:57:19Finished Affine_Arithmetic (0:10:17 elapsed time, 0:33:54 cpu time, factor 3.30)
20:57:19Building Sepref_IICF ...
20:57:22Sepref_IICF: theory Refine_Imperative_HOL.IICF_Map
20:57:22Sepref_IICF: theory Refine_Imperative_HOL.IICF_List
20:57:22Sepref_IICF: theory Refine_Imperative_HOL.IICF_Matrix
20:57:22Sepref_IICF: theory Refine_Imperative_HOL.IICF_Multiset
20:57:24Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Map
20:57:24Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_Mset
20:57:25Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array
20:57:25Stone_Relation_Algebras: theory Stone_Relation_Algebras.Relation_Algebras
20:57:26Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_List
20:57:26Sepref_IICF: theory Refine_Imperative_HOL.IICF_HOL_List
20:57:27AI_Planning_Languages_Semantics: theory Containers.Collection_Order
20:57:27Universal_Hash_Families: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
20:57:27Sepref_IICF: theory Refine_Imperative_HOL.IICF_MS_Array_List
20:57:28Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_MsetO
20:57:28Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Bag
20:57:28FSM_Tests: theory FSM_Tests.Intermediate_Implementations
20:57:28Sepref_IICF: theory Refine_Imperative_HOL.IICF_Set
20:57:29Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heap
20:57:29Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_Matrix
20:57:30Sepref_IICF: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
20:57:30Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_SetO
20:57:31Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
20:57:31Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heap
20:57:33Sepref_IICF: theory Refine_Imperative_HOL.IICF_Sepl_Binding
20:57:34Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
20:57:34Finished Iptables_Semantics/document (0:00:31 elapsed time)
20:57:34Preparing Iptables_Semantics/outline ...
20:57:37Universal_Hash_Families: theory Finite_Fields.Find_Irreducible_Poly
20:57:46Preparing Incompleteness/document ...
20:57:47Universal_Hash_Families: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
20:57:50Preparing HRB-Slicing/document ...
20:57:52Finished Iptables_Semantics/outline (0:00:17 elapsed time)
20:57:52Timing Iptables_Semantics (4 threads, 205.607s elapsed time, 749.409s cpu time, 22.584s GC time, factor 3.64)
20:57:52Finished Iptables_Semantics (0:04:07 elapsed time, 0:13:47 cpu time, factor 3.34)
20:57:52Running OmegaCatoidsQuantales ...
20:57:54Sepref_IICF: theory Refine_Imperative_HOL.IICF
20:57:54OmegaCatoidsQuantales: theory Catoids.Catoid
20:57:54OmegaCatoidsQuantales: theory Kleene_Algebra.Signatures
20:57:54OmegaCatoidsQuantales: theory Order_Lattice_Props.Sup_Lattice
20:57:55OmegaCatoidsQuantales: theory Kleene_Algebra.Dioid
20:58:01OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid
20:58:07OmegaCatoidsQuantales: theory Order_Lattice_Props.Order_Duality
20:58:13Finished Incompleteness/document (0:00:27 elapsed time)
20:58:13Preparing Incompleteness/outline ...
20:58:17OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Catoid
20:58:19OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid_Collapse
20:58:21OmegaCatoidsQuantales: theory Kleene_Algebra.Conway
20:58:22OmegaCatoidsQuantales: theory Order_Lattice_Props.Order_Lattice_Props
20:58:27AI_Planning_Languages_Semantics: theory Containers.RBT_ext
20:58:27AI_Planning_Languages_Semantics: theory Deriving.RBT_Comparator_Impl
20:58:28Finished Incompleteness/outline (0:00:14 elapsed time)
20:58:28Timing Incompleteness (4 threads, 806.234s elapsed time, 1929.903s cpu time, 10.693s GC time, factor 2.39)
20:58:28Finished Incompleteness (0:13:48 elapsed time, 0:32:45 cpu time, factor 2.37)
20:58:28Running FO_Theory_Rewriting ...
20:58:30Finished HRB-Slicing/document (0:00:39 elapsed time)
20:58:30Preparing HRB-Slicing/outline ...
20:58:34FO_Theory_Rewriting: theory Containers.Equal
20:58:34FO_Theory_Rewriting: theory Containers.Extend_Partial_Order
20:58:34FO_Theory_Rewriting: theory Containers.List_Fusion
20:58:34FO_Theory_Rewriting: theory Deriving.Comparator
20:58:34FO_Theory_Rewriting: theory Containers.Closure_Set
20:58:34FO_Theory_Rewriting: theory Deriving.Derive_Manager
20:58:35FO_Theory_Rewriting: theory Deriving.Generator_Aux
20:58:35FO_Theory_Rewriting: theory FO_Theory_Rewriting.Saturation
20:58:35FO_Theory_Rewriting: theory Deriving.Equality_Generator
20:58:35Stone_Relation_Algebras: theory Stone_Relation_Algebras.Matrix_Relation_Algebras
20:58:35Stone_Relation_Algebras: theory Stone_Relation_Algebras.Relation_Subalgebras
20:58:35Stone_Relation_Algebras: theory Stone_Relation_Algebras.Choose_Component
20:58:36FO_Theory_Rewriting: theory Deriving.Equality_Instances
20:58:36OmegaCatoidsQuantales: theory Kleene_Algebra.Kleene_Algebra
20:58:36FO_Theory_Rewriting: theory Deriving.Compare
20:58:36FO_Theory_Rewriting: theory Deriving.Comparator_Generator
20:58:37FO_Theory_Rewriting: theory Containers.AssocList
20:58:38FO_Theory_Rewriting: theory Containers.Containers_Auxiliary
20:58:38FO_Theory_Rewriting: theory First_Order_Terms.Option_Monad
20:58:39AI_Planning_Languages_Semantics: theory Containers.RBT_Mapping2
20:58:39FO_Theory_Rewriting: theory First_Order_Terms.Term
20:58:39FO_Theory_Rewriting: theory Deriving.Compare_Generator
20:58:39FO_Theory_Rewriting: theory Containers.Lexicographic_Order
20:58:39FO_Theory_Rewriting: theory Abstract-Rewriting.Seq
20:58:40FO_Theory_Rewriting: theory Deriving.Compare_Instances
20:58:40FO_Theory_Rewriting: theory Containers.Containers_Generator
20:58:40FO_Theory_Rewriting: theory Containers.Set_Linorder
20:58:40FO_Theory_Rewriting: theory Containers.Collection_Enum
20:58:40FO_Theory_Rewriting: theory Containers.Collection_Eq
20:58:41Finished HRB-Slicing/outline (0:00:11 elapsed time)
20:58:41AI_Planning_Languages_Semantics: theory Containers.RBT_Set2
20:58:41FO_Theory_Rewriting: theory Containers.RBT_ext
20:58:41FO_Theory_Rewriting: theory Containers.DList_Set
20:58:41FO_Theory_Rewriting: theory Deriving.RBT_Comparator_Impl
20:58:42Timing HRB-Slicing (4 threads, 623.333s elapsed time, 1675.471s cpu time, 20.062s GC time, factor 2.69)
20:58:42Finished HRB-Slicing (0:11:08 elapsed time, 0:29:17 cpu time, factor 2.63)
20:58:42Building HOL-Nominal ...
20:58:42FO_Theory_Rewriting: theory FOL-Fitting.FOL_Fitting
20:58:43OmegaCatoidsQuantales: theory Order_Lattice_Props.Galois_Connections
20:58:43OmegaCatoidsQuantales: theory Order_Lattice_Props.Closure_Operators
20:58:43HOL-Nominal: theory HOL-Library.Old_Datatype
20:58:43HOL-Nominal: theory HOL-Library.Infinite_Set
20:58:44AI_Planning_Languages_Semantics: theory Containers.Set_Impl
20:58:45FO_Theory_Rewriting: theory Matrix.Utility
20:58:46FO_Theory_Rewriting: theory Polynomial_Factorization.Missing_List
20:58:46HOL-Nominal: theory HOL-Nominal.Nominal
20:58:46OmegaCatoidsQuantales: theory Quantales.Quantales
20:58:46Stone_Relation_Algebras: theory Stone_Relation_Algebras.Linear_Order_Matrices
20:58:51OmegaCatoidsQuantales: theory KAD.Domain_Semiring
20:58:52FO_Theory_Rewriting: theory Regular-Sets.Regular_Set
20:58:55FSM_Tests: theory FSM_Tests.Intermediate_Frameworks
20:58:58FSM_Tests: theory FSM_Tests.HSI_Method_Implementations
20:58:58FSM_Tests: theory FSM_Tests.H_Method_Implementations
20:58:59FSM_Tests: theory FSM_Tests.Partial_S_Method_Implementations
20:59:00FSM_Tests: theory FSM_Tests.SPYH_Method_Implementations
20:59:00FO_Theory_Rewriting: theory Regular-Sets.Regular_Exp
20:59:00FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Inference
20:59:00FSM_Tests: theory FSM_Tests.SPY_Method_Implementations
20:59:01FSM_Tests: theory FSM_Tests.W_Method_Implementations
20:59:01FSM_Tests: theory FSM_Tests.Wp_Method_Implementations
20:59:03FO_Theory_Rewriting: theory Containers.Collection_Order
20:59:06FO_Theory_Rewriting: theory Regular-Sets.NDerivative
20:59:06FO_Theory_Rewriting: theory Regular-Sets.Relation_Interpretation
20:59:06FO_Theory_Rewriting: theory Containers.RBT_Mapping2
20:59:07FO_Theory_Rewriting: theory Containers.RBT_Set2
20:59:09FO_Theory_Rewriting: theory Containers.Set_Impl
20:59:10FO_Theory_Rewriting: theory Regular-Sets.Equivalence_Checking
20:59:10FO_Theory_Rewriting: theory Regular-Sets.Regexp_Method
20:59:11FO_Theory_Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
20:59:13OmegaCatoidsQuantales: theory KAD.Antidomain_Semiring
20:59:13Timing HOL-Nominal (4 threads, 13.409s elapsed time, 33.388s cpu time, 1.043s GC time, factor 2.49)
20:59:13Finished HOL-Nominal (0:00:30 elapsed time, 0:00:49 cpu time, factor 1.61)
20:59:14Building Formula_Derivatives ...
20:59:14FO_Theory_Rewriting: theory First_Order_Terms.Subterm_and_Context
20:59:14Timing Sepref_IICF (4 threads, 84.154s elapsed time, 262.160s cpu time, 3.406s GC time, factor 3.12)
20:59:14Finished Sepref_IICF (0:01:54 elapsed time, 0:05:09 cpu time, factor 2.72)
20:59:14Running HOL-Nominal-Examples ...
20:59:16HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile
20:59:16HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1
20:59:16HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine
20:59:16HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi
20:59:18Formula_Derivatives: theory Formula_Derivatives.FSet_More
20:59:18Formula_Derivatives: theory Formula_Derivatives.While_Default
20:59:18Formula_Derivatives: theory Coinductive_Languages.Coinductive_Language
20:59:18Formula_Derivatives: theory Deriving.Comparator
20:59:18Formula_Derivatives: theory Deriving.Derive_Manager
20:59:18Formula_Derivatives: theory Deriving.Generator_Aux
20:59:18Formula_Derivatives: theory List-Index.List_Index
20:59:19FO_Theory_Rewriting: theory Regular_Tree_Relations.Term_Context
20:59:20Formula_Derivatives: theory Deriving.Compare
20:59:20Formula_Derivatives: theory Deriving.Comparator_Generator
20:59:21Formula_Derivatives: theory Formula_Derivatives.Automaton
20:59:22Preparing Stone_Relation_Algebras/document ...
20:59:22HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts
20:59:23Formula_Derivatives: theory Deriving.Compare_Generator
20:59:23FO_Theory_Rewriting: theory Regular_Tree_Relations.Basic_Utils
20:59:23Formula_Derivatives: theory Deriving.Compare_Instances
20:59:24Formula_Derivatives: theory Formula_Derivatives.Abstract_Formula
20:59:24FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Terms
20:59:24Formula_Derivatives: theory Formula_Derivatives.WS1S_Prelim
20:59:27HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary
20:59:28FO_Theory_Rewriting: theory Regular_Tree_Relations.FSet_Utils
20:59:28FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Closure
20:59:28FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Ctxt
20:59:33Finished Stone_Relation_Algebras/document (0:00:11 elapsed time)
20:59:33Preparing Stone_Relation_Algebras/outline ...
20:59:34FO_Theory_Rewriting: theory FO_Theory_Rewriting.Utils
20:59:34FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata
20:59:34FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Fset
20:59:36FO_Theory_Rewriting: theory FO_Theory_Rewriting.Bot_Terms
20:59:36FO_Theory_Rewriting: theory FO_Theory_Rewriting.Multihole_Context
20:59:36FO_Theory_Rewriting: theory FO_Theory_Rewriting.Rewriting
20:59:37FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Certificate
20:59:38HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub
20:59:39HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height
20:59:41Finished Stone_Relation_Algebras/outline (0:00:08 elapsed time)
20:59:42Timing Stone_Relation_Algebras (4 threads, 120.212s elapsed time, 231.864s cpu time, 4.071s GC time, factor 1.93)
20:59:42Finished Stone_Relation_Algebras (0:02:17 elapsed time, 0:04:19 cpu time, factor 1.89)
20:59:42Building Slicing ...
20:59:43FO_Theory_Rewriting: theory FO_Theory_Rewriting.Ground_MCtxt
20:59:44HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs
20:59:44HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu
20:59:45OmegaCatoidsQuantales: theory KAD.Range_Semiring
20:59:45FO_Theory_Rewriting: theory FO_Theory_Rewriting.NF
20:59:45FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Det
20:59:45Slicing: theory Slicing.AuxLemmas
20:59:45Slicing: theory Slicing.Com
20:59:45Slicing: theory Slicing.BitVector
20:59:46Slicing: theory Slicing.BasicDefs
20:59:46FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Complement
20:59:47FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Pumping
20:59:47FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT
20:59:48Slicing: theory Slicing.CFG
20:59:48Slicing: theory Slicing.JVMCFG
20:59:48Slicing: theory Slicing.CFGExit
20:59:48Slicing: theory Slicing.CFG_wf
20:59:48Slicing: theory Slicing.Postdomination
20:59:49Slicing: theory Slicing.CFGExit_wf
20:59:50Slicing: theory Slicing.DynDataDependence
20:59:50Slicing: theory Slicing.DataDependence
20:59:50Slicing: theory Slicing.DynStandardControlDependence
20:59:50Slicing: theory Slicing.DynWeakControlDependence
20:59:50Slicing: theory Slicing.WeakControlDependence
20:59:51HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR
20:59:51Slicing: theory Slicing.StandardControlDependence
20:59:51Slicing: theory Slicing.DynPDG
20:59:51Slicing: theory Slicing.PDG
20:59:51Slicing: theory Slicing.DependentLiveVariables
20:59:52Slicing: theory Slicing.Distance
20:59:52HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN
20:59:52Slicing: theory Slicing.Observable
20:59:52Slicing: theory Slicing.SemanticsCFG
20:59:52HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening
20:59:52Slicing: theory Slicing.WeakOrderDependence
20:59:52Slicing: theory Slicing.Slice
20:59:52FO_Theory_Rewriting: theory Regular_Tree_Relations.RRn_Automata
20:59:52FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Compose
20:59:52Slicing: theory Slicing.DynSlice
20:59:52Slicing: theory Slicing.ControlDependenceRelations
20:59:53Slicing: theory Slicing.Labels
20:59:53Slicing: theory Slicing.Semantics
20:59:54HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern
20:59:54Slicing: theory Slicing.WCFG
20:59:54HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS
20:59:55FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Transitive_Closure
20:59:56HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization
20:59:56Slicing: theory Slicing.CDepInstantiations
20:59:57Slicing: theory Slicing.Interpretation
20:59:57Slicing: theory Slicing.WEquivalence
20:59:57FO_Theory_Rewriting: theory Regular_Tree_Relations.Pair_Automaton
20:59:58FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_Extensions
20:59:58Slicing: theory Slicing.WellFormed
20:59:59FO_Theory_Rewriting: theory FO_Theory_Rewriting.Tree_Automata_Derivation_Split
21:00:00FO_Theory_Rewriting: theory FO_Theory_Rewriting.LV_to_GTT
21:00:00HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support
21:00:01HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation
21:00:02Slicing: theory Slicing.AdditionalLemmas
21:00:02FO_Theory_Rewriting: theory Regular_Tree_Relations.AGTT
21:00:02HOL-Nominal-Examples: theory HOL-Nominal-Examples.W
21:00:02FO_Theory_Rewriting: theory FO_Theory_Rewriting.TA_Clousure_Const
21:00:02Slicing: theory Slicing.DynamicControlDependences
21:00:02Slicing: theory Slicing.SemanticsWellFormed
21:00:03Slicing: theory Slicing.StaticControlDependences
21:00:03Slicing: theory Slicing.JVMInterpretation
21:00:03FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_RR2
21:00:03FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite
21:00:04Slicing: theory Slicing.JVMCFG_wf
21:00:04Slicing: theory Slicing.JVMPostdomination
21:00:04FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite_Q_infinity
21:00:04Slicing: theory Slicing.SemanticsWF
21:00:04FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl
21:00:06FO_Theory_Rewriting: theory Regular_Tree_Relations.Regular_Relation_Abstract_Impl
21:00:08HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
21:00:08Preparing Projective_Measurements/document ...
21:00:11Slicing: theory Slicing.JVMControlDependences
21:00:12Slicing: theory Slicing.Slicing
21:00:13FO_Theory_Rewriting: theory FO_Theory_Rewriting.Lift_Root_Step
21:00:16FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Semantics
21:00:17FO_Theory_Rewriting: theory FO_Theory_Rewriting.GTT_RRn
21:00:17Finished Projective_Measurements/document (0:00:09 elapsed time)
21:00:17Preparing Projective_Measurements/outline ...
21:00:21Finished Projective_Measurements/outline (0:00:03 elapsed time)
21:00:22Timing Projective_Measurements (4 threads, 507.336s elapsed time, 1598.519s cpu time, 64.772s GC time, factor 3.15)
21:00:22Finished Projective_Measurements (0:09:35 elapsed time, 0:28:40 cpu time, factor 2.99)
21:00:22Running CAVA_LTL_Modelchecker ...
21:00:22OmegaCatoidsQuantales: theory KAD.Modal_Kleene_Algebra
21:00:22OmegaCatoidsQuantales: theory Quantales_Converse.Modal_Kleene_Algebra_Var
21:00:27CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
21:00:29OmegaCatoidsQuantales: theory Quantales.Quantale_Star
21:00:32CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
21:00:32CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
21:00:32CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
21:00:36OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Kleene_Algebra
21:00:36OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Kleene_Algebra
21:00:45Formula_Derivatives: theory Formula_Derivatives.Presburger_Formula
21:00:45Formula_Derivatives: theory Formula_Derivatives.WS1S_Alt_Formula
21:00:46Formula_Derivatives: theory Formula_Derivatives.WS1S_Formula
21:00:49AI_Planning_Languages_Semantics FAILED (see also "isabelle build_log -H Error AI_Planning_Languages_Semantics")
21:00:49*** Failed to load theory "Containers.Mapping_Impl" (unresolved "Containers.Set_Impl")
21:00:49*** Failed to load theory "Containers.Map_To_Mapping" (unresolved "Containers.Mapping_Impl")
21:00:49*** Failed to load theory "Containers.Containers" (unresolved "Containers.Map_To_Mapping", "Containers.Mapping_Impl")
21:00:49*** Not a constant: wf
21:00:49*** At command "declare" (line 287 of "$AFP/Containers/Set_Impl.thy")
21:00:49Building Markov_Models ...
21:00:53Markov_Models: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
21:00:53Markov_Models: theory HOL-Library.Code_Abstract_Nat
21:00:53Markov_Models: theory HOL-Computational_Algebra.Group_Closure
21:00:53Markov_Models: theory HOL-Library.Case_Converter
21:00:53Markov_Models: theory HOL-Library.Code_Target_Nat
21:00:54Markov_Models: theory HOL-Library.Simps_Case_Conv
21:00:54Markov_Models: theory HOL-Library.Code_Target_Int
21:00:54Markov_Models: theory HOL-Library.IArray
21:00:55Markov_Models: theory HOL-Library.While_Combinator
21:00:55Markov_Models: theory HOL-Library.Code_Target_Numeral
21:00:55Markov_Models: theory Coinductive.Coinductive_Nat
21:00:57Markov_Models: theory Coinductive.Coinductive_List
21:01:05OmegaCatoidsQuantales: theory Quantales_Converse.Modal_Quantale
21:01:09Markov_Models: theory Coinductive.Coinductive_Stream
21:01:10Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
21:01:15Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
21:01:16Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
21:01:19Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
21:01:19Markov_Models: theory Markov_Models.Crowds_Protocol
21:01:19Markov_Models: theory Markov_Models.Gossip_Broadcast
21:01:20Markov_Models: theory Markov_Models.Markov_Decision_Process
21:01:21Markov_Models: theory Markov_Models.PCTL
21:01:24Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
21:01:25Markov_Models: theory Markov_Models.Zeroconf_Analysis
21:01:25Markov_Models: theory Markov_Models.MDP_Reachability_Problem
21:01:26Markov_Models: theory Markov_Models.Example_A
21:01:27Markov_Models: theory Markov_Models.Example_B
21:01:28Markov_Models: theory Markov_Models.MDP_RP_Certification
21:01:28Markov_Models: theory Markov_Models.PGCL
21:01:29Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
21:01:33Markov_Models: theory Markov_Models.Markov_Models
21:01:50Formula_Derivatives: theory Formula_Derivatives.WS1S_Nameful
21:01:50Formula_Derivatives: theory Formula_Derivatives.WS1S_Presburger_Equivalence
21:03:01Markov_Models: theory Markov_Models.MDP_RP
21:03:21HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
21:03:24HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
21:03:25CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
21:03:25CAVA_LTL_Modelchecker: theory LTL.Rewriting
21:03:25CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
21:03:28CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
21:03:28CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
21:03:28CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
21:03:29CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
21:03:29CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
21:03:30CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
21:03:36CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
21:03:58Preparing Markov_Models/document ...
21:04:06OmegaCatoidsQuantales: theory Catoids.Catoid_Lifting
21:04:06OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Quantale
21:04:06OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Quantale
21:04:20Finished Markov_Models/document (0:00:22 elapsed time)
21:04:20Preparing Markov_Models/outline ...
21:04:30Finished Markov_Models/outline (0:00:10 elapsed time)
21:04:31Timing Markov_Models (4 threads, 144.050s elapsed time, 479.966s cpu time, 9.961s GC time, factor 3.33)
21:04:31Finished Markov_Models (0:03:05 elapsed time, 0:09:08 cpu time, factor 2.96)
21:04:31Running Universal_Turing_Machine ...
21:04:33Universal_Turing_Machine: theory HOL-Library.Code_Target_Int
21:04:33Universal_Turing_Machine: theory HOL-Library.Code_Abstract_Nat
21:04:33Universal_Turing_Machine: theory HOL-Library.Code_Binary_Nat
21:04:33Universal_Turing_Machine: theory HOL-Library.Code_Target_Nat
21:04:34Universal_Turing_Machine: theory HOL-Library.Code_Target_Numeral
21:04:35Universal_Turing_Machine: theory HOL-Library.Nat_Bijection
21:04:35Universal_Turing_Machine: theory Universal_Turing_Machine.Rec_Def
21:04:35Universal_Turing_Machine: theory Universal_Turing_Machine.Turing
21:04:35Universal_Turing_Machine: theory HOL-Library.Discrete
21:04:36Universal_Turing_Machine: theory Universal_Turing_Machine.Recs_alt_Def
21:04:37Universal_Turing_Machine: theory Universal_Turing_Machine.Rec_Ex
21:04:38Universal_Turing_Machine: theory Universal_Turing_Machine.BlanksDoNotMatter
21:04:38Universal_Turing_Machine: theory Universal_Turing_Machine.ComposableTMs
21:04:38Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_aux
21:04:40Universal_Turing_Machine: theory Universal_Turing_Machine.ComposedTMs
21:04:40Universal_Turing_Machine: theory Universal_Turing_Machine.Numerals
21:04:41Universal_Turing_Machine: theory Universal_Turing_Machine.Numerals_Ex
21:04:41Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_Hoare
21:04:41Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_Mopup
21:04:41Universal_Turing_Machine: theory Universal_Turing_Machine.DitherTM
21:04:41Universal_Turing_Machine: theory Universal_Turing_Machine.Recs_alt_Ex
21:04:42Universal_Turing_Machine: theory Universal_Turing_Machine.OneStrokeTM
21:04:42Universal_Turing_Machine: theory Universal_Turing_Machine.SemiIdTM
21:04:42Universal_Turing_Machine: theory Universal_Turing_Machine.Turing_HaltingConditions
21:04:43Universal_Turing_Machine: theory Universal_Turing_Machine.CopyTM
21:04:43Universal_Turing_Machine: theory Universal_Turing_Machine.SimpleGoedelEncoding
21:04:43Universal_Turing_Machine: theory Universal_Turing_Machine.TuringDecidable
21:04:43Universal_Turing_Machine: theory Universal_Turing_Machine.WeakCopyTM
21:04:46Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus
21:04:52Universal_Turing_Machine: theory Universal_Turing_Machine.TuringUnComputable_H2
21:04:52Universal_Turing_Machine: theory Universal_Turing_Machine.TuringUnComputable_H2_original
21:04:52Universal_Turing_Machine: theory Universal_Turing_Machine.StrongCopyTM
21:04:59Universal_Turing_Machine: theory Universal_Turing_Machine.TuringReducible
21:04:59Universal_Turing_Machine: theory Universal_Turing_Machine.HaltingProblems_K_H
21:04:59Universal_Turing_Machine: theory Universal_Turing_Machine.HaltingProblems_K_aux
21:04:59Universal_Turing_Machine: theory Universal_Turing_Machine.TuringComputable
21:05:04FSM_Tests FAILED (see also "isabelle build_log -H Error FSM_Tests")
21:05:04*** Failed to load theory "Containers.Mapping_Impl" (unresolved "Containers.Set_Impl")
21:05:04*** Failed to load theory "Containers.Map_To_Mapping" (unresolved "Containers.Mapping_Impl")
21:05:04*** Failed to load theory "Containers.Containers" (unresolved "Containers.Map_To_Mapping", "Containers.Mapping_Impl")
21:05:04*** Failed to load theory "FSM_Tests.Prefix_Tree_Refined" (unresolved "Containers.Containers")
21:05:04*** Failed to load theory "FSM_Tests.Util_Refined" (unresolved "Containers.Containers")
21:05:04*** Failed to load theory "FSM_Tests.FSM_Code_Datatype" (unresolved "Containers.Containers")
21:05:04*** Failed to load theory "FSM_Tests.Test_Suite_Representations_Refined" (unresolved "FSM_Tests.Prefix_Tree_Refined", "FSM_Tests.Util_Refined")
21:05:04*** Failed to load theory "FSM_Tests.Test_Suite_Calculation_Refined" (unresolved "Containers.Containers", "FSM_Tests.Util_Refined")
21:05:04*** Failed to load theory "FSM_Tests.Test_Suite_Generator_Code_Export" (unresolved "FSM_Tests.FSM_Code_Datatype", "FSM_Tests.Prefix_Tree_Refined", "FSM_Tests.Test_Suite_Calculation_Refined", "FSM_Tests.Test_Suite_Representations_Refined")
21:05:04*** Not a constant: wf
21:05:04*** At command "declare" (line 287 of "$AFP/Containers/Set_Impl.thy")
21:05:04Building HOL-Auth ...
21:05:05Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_Hoare
21:05:05Universal_Turing_Machine: theory Universal_Turing_Machine.Abacus_alt_Compile
21:05:05HOL-Auth: theory HOL-Auth.README
21:05:06Universal_Turing_Machine: theory Universal_Turing_Machine.Recursive
21:05:06HOL-Auth: theory HOL-Auth.Message
21:05:06HOL-Auth: theory HOL-Library.Case_Converter
21:05:06HOL-Auth: theory HOL-Library.Nat_Bijection
21:05:06Universal_Turing_Machine: theory Universal_Turing_Machine.UF
21:05:06Universal_Turing_Machine: theory Universal_Turing_Machine.GeneratedCode
21:05:07HOL-Auth: theory HOL-Library.Simps_Case_Conv
21:05:10HOL-Auth: theory HOL-Auth.All_Symmetric
21:05:10HOL-Auth: theory HOL-Auth.Event
21:05:10HOL-Auth: theory HOL-Auth.EventSC
21:05:11Preparing Universal_Hash_Families/document ...
21:05:11HOL-Auth: theory HOL-Auth.Public
21:05:12HOL-Auth: theory HOL-Auth.Smartcard
21:05:13HOL-Auth: theory HOL-Auth.CertifiedEmail
21:05:13HOL-Auth: theory HOL-Auth.KerberosIV
21:05:13HOL-Auth: theory HOL-Auth.KerberosIV_Gets
21:05:13HOL-Auth: theory HOL-Auth.KerberosV
21:05:14HOL-Auth: theory HOL-Auth.Kerberos_BAN
21:05:17HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets
21:05:18HOL-Auth: theory HOL-Auth.NS_Public
21:05:18Finished Universal_Hash_Families/document (0:00:06 elapsed time)
21:05:18Preparing Universal_Hash_Families/outline ...
21:05:18HOL-Auth: theory HOL-Auth.NS_Public_Bad
21:05:18HOL-Auth: theory HOL-Auth.NS_Shared
21:05:19HOL-Auth: theory HOL-Auth.OtwayRees
21:05:19HOL-Auth: theory HOL-Auth.OtwayReesBella
21:05:19HOL-Auth: theory HOL-Auth.OtwayRees_AN
21:05:19HOL-Auth: theory HOL-Auth.OtwayRees_Bad
21:05:20HOL-Auth: theory HOL-Auth.Recur
21:05:20HOL-Auth: theory HOL-Auth.WooLam
21:05:22HOL-Auth: theory HOL-Auth.Yahalom
21:05:22HOL-Auth: theory HOL-Auth.Yahalom2
21:05:22HOL-Auth: theory HOL-Auth.Yahalom_Bad
21:05:22HOL-Auth: theory HOL-Auth.ZhouGollmann
21:05:22HOL-Auth: theory HOL-Auth.ShoupRubin
21:05:22HOL-Auth: theory HOL-Auth.ShoupRubinBella
21:05:23Finished Universal_Hash_Families/outline (0:00:04 elapsed time)
21:05:23HOL-Auth: theory HOL-Auth.TLS
21:05:23Timing Universal_Hash_Families (4 threads, 651.017s elapsed time, 2246.577s cpu time, 194.243s GC time, factor 3.45)
21:05:23Finished Universal_Hash_Families (0:10:58 elapsed time, 0:37:42 cpu time, factor 3.44)
21:05:23Running Constructive_Cryptography_CM ...
21:05:23HOL-Auth: theory HOL-Auth.Auth_Shared
21:05:24HOL-Auth: theory HOL-Auth.Auth_Smartcard
21:05:25HOL-Auth: theory HOL-Auth.Auth_Public
21:05:27Constructive_Cryptography_CM: theory Game_Based_Crypto.Diffie_Hellman
21:05:27Constructive_Cryptography_CM: theory Sigma_Commit_Crypto.Xor
21:05:27Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.More_CC
21:05:31Universal_Turing_Machine: theory Universal_Turing_Machine.UTM
21:05:37Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fold_Spmf
21:05:38Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Observe_Failure
21:05:38Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.State_Isomorphism
21:05:38Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Fused_Resource
21:05:57FO_Theory_Rewriting FAILED (see also "isabelle build_log -H Error FO_Theory_Rewriting")
21:05:57*** Failed to load theory "Containers.Mapping_Impl" (unresolved "Containers.Set_Impl")
21:05:57*** Failed to load theory "Containers.Map_To_Mapping" (unresolved "Containers.Mapping_Impl")
21:05:57*** Failed to load theory "Containers.Containers" (unresolved "Containers.Map_To_Mapping", "Containers.Mapping_Impl")
21:05:57*** Failed to load theory "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl" (unresolved "Containers.Mapping_Impl", "Containers.Set_Impl")
21:05:57*** Failed to load theory "FO_Theory_Rewriting.Type_Instances_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl")
21:05:57*** Failed to load theory "FO_Theory_Rewriting.FOL_Extra" (unresolved "FO_Theory_Rewriting.Type_Instances_Impl")
21:05:57*** Failed to load theory "FO_Theory_Rewriting.NF_Impl" (unresolved "FO_Theory_Rewriting.Type_Instances_Impl")
21:05:57*** Failed to load theory "Regular_Tree_Relations.Tree_Automata_Impl" (unresolved "Containers.Containers", "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl")
21:05:57*** Failed to load theory "Regular_Tree_Relations.Regular_Relation_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Impl")
21:05:57*** Failed to load theory "FO_Theory_Rewriting.FOR_Check" (unresolved "FO_Theory_Rewriting.FOL_Extra")
21:05:57*** Failed to load theory "FO_Theory_Rewriting.FOR_Check_Impl" (unresolved "FO_Theory_Rewriting.FOR_Check", "FO_Theory_Rewriting.NF_Impl", "Regular_Tree_Relations.Regular_Relation_Impl")
21:05:57*** Not a constant: wf
21:05:57*** At command "declare" (line 287 of "$AFP/Containers/Set_Impl.thy")
21:05:57Running HOL-Decision_Procs ...
21:06:00HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions
21:06:00HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order
21:06:00HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library
21:06:00HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux
21:06:01HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper
21:06:02HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List
21:06:03HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring
21:06:07HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex
21:06:07HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack
21:06:09Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Channel
21:06:09Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Key
21:06:09Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Construction_Utility
21:06:11Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Concrete_Security
21:06:14Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Asymptotic_Security
21:06:19HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete
21:06:21HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field
21:06:23HOL-Decision_Procs: theory HOL-Decision_Procs.MIR
21:06:31OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Omega_Catoid_Lifting
21:06:34Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.One_Time_Pad
21:06:34Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.Diffie_Hellman_CC
21:06:39HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex
21:06:41HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair
21:06:41HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial
21:07:00HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff
21:07:08HOL-Auth: theory HOL-Auth.README_Guard
21:07:08HOL-Auth: theory HOL-Auth.Extensions
21:07:08HOL-Auth: theory HOL-Auth.Shared
21:07:09HOL-Auth: theory HOL-Auth.Analz
21:07:09HOL-Auth: theory HOL-Auth.List_Msg
21:07:10HOL-Auth: theory HOL-Auth.Guard
21:07:10HOL-Auth: theory HOL-Auth.GuardK
21:07:11HOL-Auth: theory HOL-Auth.Guard_Public
21:07:11HOL-Auth: theory HOL-Auth.Guard_Shared
21:07:11HOL-Auth: theory HOL-Auth.Guard_NS_Public
21:07:11HOL-Auth: theory HOL-Auth.Proto
21:07:12HOL-Auth: theory HOL-Auth.Guard_OtwayRees
21:07:12HOL-Auth: theory HOL-Auth.P2
21:07:12HOL-Auth: theory HOL-Auth.P1
21:07:13HOL-Auth: theory HOL-Auth.Guard_Yahalom
21:07:13HOL-Auth: theory HOL-Auth.Auth_Guard_Shared
21:07:20HOL-Auth: theory HOL-Auth.Auth_Guard_Public
21:07:32Constructive_Cryptography_CM: theory Constructive_Cryptography_CM.DH_OTP
21:07:43OmegaCatoidsQuantales: theory OmegaCatoidsQuantales.Two_Catoid_Lifting
21:07:45HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds
21:07:52HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation
21:07:55Preparing OmegaCatoidsQuantales/document ...
21:08:05Finished OmegaCatoidsQuantales/document (0:00:09 elapsed time)
21:08:05Preparing OmegaCatoidsQuantales/outline ...
21:08:11Finished OmegaCatoidsQuantales/outline (0:00:06 elapsed time)
21:08:11Timing OmegaCatoidsQuantales (4 threads, 597.580s elapsed time, 1399.210s cpu time, 35.575s GC time, factor 2.34)
21:08:11Finished OmegaCatoidsQuantales (0:10:01 elapsed time, 0:23:28 cpu time, factor 2.34)
21:08:12Building Transition_Systems_and_Automata ...
21:08:15Transition_Systems_and_Automata: theory CAVA_Base.Statistics
21:08:15Transition_Systems_and_Automata: theory HOL-Library.Omega_Words_Fun
21:08:15Transition_Systems_and_Automata: theory HOL-Library.Nat_Bijection
21:08:15Transition_Systems_and_Automata: theory HOL-Library.Old_Datatype
21:08:15Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Misc
21:08:15Transition_Systems_and_Automata: theory HOL-Library.Sublist
21:08:16Preparing HOL-Auth/document ...
21:08:16Transition_Systems_and_Automata: theory HOL-Library.Stream
21:08:16Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Basic
21:08:16Transition_Systems_and_Automata: theory HOL-Library.Countable
21:08:18Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Refine_Aux
21:08:18Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Basic
21:08:18Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence
21:08:19Transition_Systems_and_Automata: theory HOL-Library.Countable_Set
21:08:19Transition_Systems_and_Automata: theory CAVA_Base.Code_String
21:08:19Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Code_Target
21:08:19Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Base
21:08:19Transition_Systems_and_Automata: theory HOL-Library.Countable_Complete_Lattices
21:08:20Transition_Systems_and_Automata: theory CAVA_Automata.Digraph
21:08:20Transition_Systems_and_Automata: theory DFS_Framework.Impl_Rev_Array_Stack
21:08:20Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System
21:08:22Transition_Systems_and_Automata: theory CAVA_Automata.Automata
21:08:22Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Impl
21:08:23Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton
21:08:24Transition_Systems_and_Automata: theory HOL-Library.Order_Continuity
21:08:25Transition_Systems_and_Automata: theory HOL-Library.Extended_Nat
21:08:27Transition_Systems_and_Automata: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:08:28Transition_Systems_and_Automata: theory DFS_Framework.Param_DFS
21:08:29Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_LTL
21:08:30CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
21:08:30Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance
21:08:30Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_Zip
21:08:30Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization
21:08:31Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Maps
21:08:31Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Construction
21:08:31Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Refine
21:08:31Finished HOL-Auth/document (0:00:15 elapsed time)
21:08:31Preparing HOL-Auth/outline ...
21:08:31Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Extra
21:08:32Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Deterministic
21:08:33Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance_Refine
21:08:34Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization_Refine
21:08:34Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Nondeterministic
21:08:34Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Refine
21:08:35Transition_Systems_and_Automata: theory CAVA_Automata.Lasso
21:08:37Preparing Formula_Derivatives/document ...
21:08:38Transition_Systems_and_Automata: theory DFS_Framework.DFS_Invars_Basic
21:08:41Transition_Systems_and_Automata: theory DFS_Framework.General_DFS_Structure
21:08:44Finished Formula_Derivatives/document (0:00:06 elapsed time)
21:08:44Preparing Formula_Derivatives/outline ...
21:08:44Finished HOL-Auth/outline (0:00:12 elapsed time)
21:08:44Timing HOL-Auth (4 threads, 176.785s elapsed time, 605.047s cpu time, 8.222s GC time, factor 3.42)
21:08:44Finished HOL-Auth (0:03:10 elapsed time, 0:10:26 cpu time, factor 3.29)
21:08:45Running Virtual_Substitution ...
21:08:46Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA
21:08:48Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA
21:08:49Finished Formula_Derivatives/outline (0:00:05 elapsed time)
21:08:49Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA
21:08:49Timing Formula_Derivatives (4 threads, 516.533s elapsed time, 1109.999s cpu time, 182.198s GC time, factor 2.15)
21:08:49Finished Formula_Derivatives (0:09:22 elapsed time, 0:19:55 cpu time, factor 2.13)
21:08:50Building Nominal2 ...
21:08:50Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DFA
21:08:51HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition
21:08:51Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBA
21:08:51Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBTA
21:08:51Nominal2: theory HOL-Library.Infinite_Set
21:08:51Nominal2: theory HOL-Library.Old_Datatype
21:08:51Nominal2: theory HOL-Library.Nat_Bijection
21:08:51Nominal2: theory HOL-Library.Cancellation
21:08:52Virtual_Substitution: theory Deriving.Derive_Manager
21:08:52Virtual_Substitution: theory Deriving.Generator_Aux
21:08:52Virtual_Substitution: theory HOL-Library.AList
21:08:52Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat
21:08:52Nominal2: theory HOL-Library.Phantom_Type
21:08:52Virtual_Substitution: theory HOL-Library.Code_Target_Int
21:08:52Nominal2: theory HOL-Library.Quotient_Syntax
21:08:53Nominal2: theory HOL-Library.Quotient_Option
21:08:53Nominal2: theory HOL-Library.Quotient_Product
21:08:53Virtual_Substitution: theory HOL-Library.Code_Target_Nat
21:08:53Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGCA
21:08:53Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA_Combine
21:08:53Nominal2: theory HOL-Library.Quotient_Set
21:08:53Nominal2: theory HOL-Library.Multiset
21:08:53Nominal2: theory HOL-Library.Countable
21:08:53Nominal2: theory HOL-Library.Quotient_List
21:08:53Virtual_Substitution: theory HOL-Library.Conditional_Parametricity
21:08:53Virtual_Substitution: theory HOL-Library.Fun_Lexorder
21:08:53Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA_Combine
21:08:54Virtual_Substitution: theory HOL-Library.Function_Algebras
21:08:54Virtual_Substitution: theory HOL-Library.Groups_Big_Fun
21:08:54Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA
21:08:54Virtual_Substitution: theory Abstract-Rewriting.Seq
21:08:54Nominal2: theory HOL-Library.Cardinality
21:08:55Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA
21:08:56Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA_Combine
21:08:56Virtual_Substitution: theory HOL-Library.More_List
21:08:56Virtual_Substitution: theory HOL-Library.Sublist
21:08:56Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA
21:08:56Nominal2: theory HOL-Library.FSet
21:08:56Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Combine
21:08:56Nominal2: theory FinFun.FinFun
21:08:56Virtual_Substitution: theory HOL-Library.While_Combinator
21:08:57Virtual_Substitution: theory HOL-Library.Poly_Mapping
21:08:57Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NFA
21:08:57Virtual_Substitution: theory HOL-Library.Ramsey
21:08:57Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA
21:08:57Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBTA
21:08:57Virtual_Substitution: theory HOL-Library.FSet
21:08:58Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Refine
21:08:59Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Refine
21:09:00Virtual_Substitution: theory Polynomials.More_Modules
21:09:00Transition_Systems_and_Automata: theory CAVA_Automata.Automata_Impl
21:09:00Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Combine
21:09:00Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Refine
21:09:00Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA_Combine
21:09:00Virtual_Substitution: theory Polynomials.MPoly_Type
21:09:01Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial
21:09:01Transition_Systems_and_Automata: theory DFS_Framework.Rec_Impl
21:09:01Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant
21:09:01Transition_Systems_and_Automata: theory DFS_Framework.Tailrec_Impl
21:09:02Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path
21:09:02Virtual_Substitution: theory Matrix.Utility
21:09:02Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path_Impl
21:09:02Virtual_Substitution: theory Polynomials.More_MPoly_Type
21:09:02Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG
21:09:02Virtual_Substitution: theory Open_Induction.Restricted_Predicates
21:09:04Timing HOL-Nominal-Examples (4 threads, 579.157s elapsed time, 2136.242s cpu time, 113.346s GC time, factor 3.69)
21:09:04Finished HOL-Nominal-Examples (0:09:44 elapsed time, 0:35:50 cpu time, factor 3.68)
21:09:04Nominal2: theory Nominal2.Nominal2_Base
21:09:04Building Simpl ...
21:09:05Virtual_Substitution: theory Regular-Sets.Regular_Set
21:09:05Virtual_Substitution: theory Show.Show
21:09:06Simpl: theory HOL-Library.Cancellation
21:09:06Simpl: theory HOL-Library.LaTeXsugar
21:09:06Simpl: theory HOL-Library.Old_Recdef
21:09:06Simpl: theory HOL-Statespace.DistinctTreeProver
21:09:07HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex
21:09:07HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex
21:09:07Simpl: theory Simpl.Simpl_Heap
21:09:08Simpl: theory Simpl.HeapList
21:09:08Virtual_Substitution: theory Show.Show_Instances
21:09:08Simpl: theory HOL-Library.Multiset
21:09:09Virtual_Substitution: theory HOL-Library.Finite_Map
21:09:10Simpl: theory HOL-Statespace.StateFun
21:09:10Simpl: theory Simpl.Generalise
21:09:11Virtual_Substitution: theory Show.Show_Real
21:09:12Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences
21:09:12Nominal2: theory Nominal2.Atoms
21:09:12Nominal2: theory Nominal2.Eqvt
21:09:12Nominal2: theory Nominal2.Nominal2_Abs
21:09:12Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements
21:09:13Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum
21:09:14Simpl: theory Simpl.Language
21:09:14Simpl: theory HOL-Statespace.StateSpaceLocale
21:09:15Transition_Systems_and_Automata: theory DFS_Framework.Simple_Impl
21:09:15Nominal2: theory Nominal2.Nominal2_FCB
21:09:16Nominal2: theory Nominal2.Nominal2
21:09:16Preparing Slicing/document ...
21:09:16Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate
21:09:16Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton_Code
21:09:17Simpl: theory HOL-Statespace.StateSpaceSyntax
21:09:19Virtual_Substitution: theory Regular-Sets.Regular_Exp
21:09:21Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Implement
21:09:22Virtual_Substitution: theory Regular-Sets.NDerivative
21:09:22Virtual_Substitution: theory Regular-Sets.Relation_Interpretation
21:09:25Transition_Systems_and_Automata: theory DFS_Framework.Restr_Impl
21:09:26Simpl: theory Simpl.Semantic
21:09:27Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Implement
21:09:29Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework
21:09:29Virtual_Substitution: theory Regular-Sets.Equivalence_Checking
21:09:30Transition_Systems_and_Automata: theory DFS_Framework.Reachable_Nodes
21:09:30Virtual_Substitution: theory Regular-Sets.Regexp_Method
21:09:31Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map
21:09:32Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Implement
21:09:32Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting
21:09:32Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full
21:09:32Simpl: theory Simpl.HoarePartialDef
21:09:32Simpl: theory Simpl.Termination
21:09:33Simpl: theory Simpl.HoarePartialProps
21:09:34Simpl: theory Simpl.HoareTotalDef
21:09:34Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences
21:09:35Simpl: theory Simpl.SmallStep
21:09:35Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations
21:09:35Virtual_Substitution: theory Abstract-Rewriting.SN_Orders
21:09:35Simpl: theory Simpl.HoarePartial
21:09:36Virtual_Substitution: theory Polynomials.Utils
21:09:36Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders
21:09:36Simpl: theory Simpl.AlternativeSmallStep
21:09:36Virtual_Substitution: theory Polynomials.Power_Products
21:09:37Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Implement
21:09:38Simpl: theory Simpl.HoareTotalProps
21:09:38Finished Slicing/document (0:00:22 elapsed time)
21:09:38Preparing Slicing/outline ...
21:09:40CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
21:09:40CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
21:09:40Virtual_Substitution: theory Polynomials.Polynomials
21:09:40Simpl: theory Simpl.Compose
21:09:41Simpl: theory Simpl.HoareTotal
21:09:43Simpl: theory Simpl.Hoare
21:09:44Simpl: theory Simpl.Closure
21:09:44Simpl: theory Simpl.StateSpace
21:09:44Simpl: theory Simpl.Vcg
21:09:46Finished Slicing/outline (0:00:07 elapsed time)
21:09:47Timing Slicing (4 threads, 540.165s elapsed time, 1792.164s cpu time, 12.093s GC time, factor 3.32)
21:09:47Finished Slicing (0:09:30 elapsed time, 0:30:42 cpu time, factor 3.23)
21:09:47Building HOLCF-Prelude ...
21:09:47Preparing Nominal2/document ...
21:09:50HOLCF-Prelude: theory HOL-Library.Adhoc_Overloading
21:09:50HOLCF-Prelude: theory HOL-Library.Cancellation
21:09:50HOLCF-Prelude: theory HOLCF-Library.Int_Discrete
21:09:50HOLCF-Prelude: theory HOLCF-Prelude.HOLCF_Main
21:09:51Virtual_Substitution: theory Polynomials.Show_Polynomials
21:09:51HOLCF-Prelude: theory HOL-Library.Multiset
21:09:51HOLCF-Prelude: theory HOLCF-Prelude.Data_Function
21:09:51HOLCF-Prelude: theory HOLCF-Prelude.Numeral_Cpo
21:09:51HOLCF-Prelude: theory HOLCF-Prelude.Type_Classes
21:09:54Simpl: theory Simpl.ProcParEx
21:09:54Simpl: theory Simpl.ProcParExSP
21:09:54Simpl: theory Simpl.XVcg
21:09:54Simpl: theory Simpl.ClosureEx
21:09:54Simpl: theory Simpl.XVcgEx
21:09:55Simpl: theory Simpl.ComposeEx
21:09:55Simpl: theory Simpl.Quicksort
21:09:55Simpl: theory Simpl.SyntaxTest
21:09:55Simpl: theory Simpl.UserGuide
21:09:55Simpl: theory Simpl.VcgEx
21:09:55HOLCF-Prelude: theory HOLCF-Prelude.Data_Bool
21:09:55Preparing CAVA_LTL_Modelchecker/document ...
21:09:55HOLCF-Prelude: theory HOLCF-Prelude.Data_Integer
21:09:55HOLCF-Prelude: theory HOLCF-Prelude.Data_Tuple
21:09:56Simpl: theory Simpl.VcgExSP
21:09:56Simpl: theory Simpl.VcgExTotal
21:09:56Finished Nominal2/document (0:00:08 elapsed time)
21:09:56Preparing Nominal2/outline ...
21:09:59HOLCF-Prelude: theory HOLCF-Prelude.Data_List
21:09:59HOLCF-Prelude: theory HOLCF-Prelude.Num_Class
21:09:59Virtual_Substitution: theory Polynomials.MPoly_Type_Class
21:10:02Finished Nominal2/outline (0:00:06 elapsed time)
21:10:03Finished CAVA_LTL_Modelchecker/document (0:00:07 elapsed time)
21:10:03Timing Nominal2 (4 threads, 40.227s elapsed time, 147.110s cpu time, 4.139s GC time, factor 3.66)
21:10:03Finished Nominal2 (0:00:55 elapsed time, 0:02:51 cpu time, factor 3.08)
21:10:03Preparing CAVA_LTL_Modelchecker/outline ...
21:10:03Running HOL-Proofs-Extraction ...
21:10:03HOLCF-Prelude: theory HOL-Computational_Algebra.Factorial_Ring
21:10:03Simpl: theory Simpl.Simpl
21:10:05Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered
21:10:06HOL-Proofs-Extraction: theory HOL-Library.Cancellation
21:10:06HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat
21:10:06HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int
21:10:06HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax
21:10:07HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall
21:10:07HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat
21:10:08HOL-Proofs-Extraction: theory HOL-Library.Multiset
21:10:08HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman
21:10:08Finished CAVA_LTL_Modelchecker/outline (0:00:05 elapsed time)
21:10:09Timing CAVA_LTL_Modelchecker (4 threads, 565.996s elapsed time, 739.345s cpu time, 19.293s GC time, factor 1.31)
21:10:09Finished CAVA_LTL_Modelchecker (0:09:32 elapsed time, 0:12:28 cpu time, factor 1.31)
21:10:09HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral
21:10:09Running PAC_Checker ...
21:10:09HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util
21:10:09HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole
21:10:09HOLCF-Prelude: theory HOLCF-Prelude.Data_Maybe
21:10:09HOLCF-Prelude: theory HOLCF-Prelude.Definedness
21:10:09HOLCF-Prelude: theory HOLCF-Prelude.List_Comprehension
21:10:10Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Graphs
21:10:10Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Graphs
21:10:10HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction
21:10:10HOLCF-Prelude: theory HOLCF-Prelude.HOLCF_Prelude
21:10:10HOLCF-Prelude: theory HOLCF-Prelude.Fibs
21:10:10HOLCF-Prelude: theory HOLCF-Prelude.GHC_Rewrite_Rules
21:10:10HOLCF-Prelude: theory HOLCF-Prelude.HLint
21:10:12Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG_Code
21:10:12HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem
21:10:13PAC_Checker: theory Deriving.Generator_Aux
21:10:13PAC_Checker: theory Deriving.Derive_Manager
21:10:13PAC_Checker: theory HOL-Library.Multiset_Order
21:10:13PAC_Checker: theory HOL-Combinatorics.Transposition
21:10:13PAC_Checker: theory HOL-Library.Conditional_Parametricity
21:10:15PAC_Checker: theory HOL-Library.Fun_Lexorder
21:10:15PAC_Checker: theory HOL-Library.FuncSet
21:10:15PAC_Checker: theory HOL-Library.Function_Algebras
21:10:15PAC_Checker: theory HOL-Library.Groups_Big_Fun
21:10:16PAC_Checker: theory Abstract-Rewriting.Seq
21:10:16PAC_Checker: theory HOL-Library.More_List
21:10:18PAC_Checker: theory HOL-Library.Sublist
21:10:18PAC_Checker: theory HOL-Algebra.Congruence
21:10:18PAC_Checker: theory HOL-Library.Disjoint_Sets
21:10:19HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor
21:10:19PAC_Checker: theory HOL-Library.Poly_Mapping
21:10:20HOLCF-Prelude: theory HOL-Computational_Algebra.Euclidean_Algorithm
21:10:21PAC_Checker: theory HOL-Combinatorics.Permutations
21:10:25PAC_Checker: theory HOL-Algebra.Order
21:10:29PAC_Checker: theory HOL-Combinatorics.List_Permutation
21:10:30PAC_Checker: theory HOL-Library.Countable_Set
21:10:30PAC_Checker: theory Polynomials.MPoly_Type
21:10:30PAC_Checker: theory HOL-Algebra.Lattice
21:10:31PAC_Checker: theory Nested_Multisets_Ordinals.Multiset_More
21:10:32PAC_Checker: theory HOL-Library.Equipollence
21:10:32Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap
21:10:32PAC_Checker: theory Polynomials.More_MPoly_Type
21:10:36PAC_Checker: theory HOL-Library.FSet
21:10:37PAC_Checker: theory HOL-Library.Ramsey
21:10:37PAC_Checker: theory HOL-Algebra.Complete_Lattice
21:10:37PAC_Checker: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
21:10:37Virtual_Substitution: theory Virtual_Substitution.MPolyExtension
21:10:38Virtual_Substitution: theory Virtual_Substitution.QE
21:10:38PAC_Checker: theory Polynomials.More_Modules
21:10:38PAC_Checker: theory Open_Induction.Restricted_Predicates
21:10:40PAC_Checker: theory HOL-Algebra.Group
21:10:40PAC_Checker: theory PAC_Checker.PAC_Misc
21:10:40PAC_Checker: theory PAC_Checker.PAC_Version
21:10:40PAC_Checker: theory PAC_Checker.More_Loops
21:10:40PAC_Checker: theory Regular-Sets.Regular_Set
21:10:40Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps
21:10:41PAC_Checker: theory Show.Show
21:10:44HOLCF-Prelude: theory HOL-Computational_Algebra.Primes
21:10:46Virtual_Substitution: theory Virtual_Substitution.PolyAtoms
21:10:46PAC_Checker: theory Show.Show_Instances
21:10:46HOLCF-Prelude: theory HOLCF-Prelude.Sieve_Primes
21:10:47Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Nodes
21:10:48PAC_Checker: theory HOL-Algebra.Coset
21:10:48PAC_Checker: theory HOL-Algebra.FiniteProduct
21:10:50PAC_Checker: theory HOL-Library.Finite_Map
21:10:51PAC_Checker: theory HOL-Algebra.Ring
21:10:53PAC_Checker: theory HOL-Algebra.Generated_Groups
21:10:54Virtual_Substitution: theory Virtual_Substitution.Debruijn
21:10:55Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting
21:10:55PAC_Checker: theory HOL-Algebra.Divisibility
21:10:55HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring
21:10:56Virtual_Substitution: theory Virtual_Substitution.Optimizations
21:10:57Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Explicit
21:10:59PAC_Checker: theory HOL-Algebra.AbelCoset
21:10:59Virtual_Substitution: theory Virtual_Substitution.Reindex
21:11:00PAC_Checker: theory HOL-Algebra.Module
21:11:00PAC_Checker: theory HOL-Algebra.Elementary_Groups
21:11:00PAC_Checker: theory HOL-Algebra.Ideal
21:11:00PAC_Checker: theory Well_Quasi_Orders.Infinite_Sequences
21:11:00PAC_Checker: theory Well_Quasi_Orders.Minimal_Elements
21:11:01PAC_Checker: theory Well_Quasi_Orders.Least_Enum
21:11:01PAC_Checker: theory PAC_Checker.WB_Sort
21:11:01Virtual_Substitution: theory Virtual_Substitution.UniAtoms
21:11:02PAC_Checker: theory Native_Word.Uint64
21:11:02PAC_Checker: theory HOL-Algebra.RingHom
21:11:02PAC_Checker: theory HOL-Algebra.QuotRing
21:11:02PAC_Checker: theory HOL-Algebra.UnivPoly
21:11:04PAC_Checker: theory Regular-Sets.Regular_Exp
21:11:05Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Translate
21:11:07PAC_Checker: theory Regular-Sets.NDerivative
21:11:08PAC_Checker: theory Regular-Sets.Relation_Interpretation
21:11:09Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs
21:11:10Virtual_Substitution: theory Virtual_Substitution.VSAlgos
21:11:14PAC_Checker: theory PAC_Checker.Finite_Map_Multiset
21:11:15PAC_Checker: theory PAC_Checker.PAC_Map_Rel
21:11:15PAC_Checker: theory Regular-Sets.Equivalence_Checking
21:11:16PAC_Checker: theory Regular-Sets.Regexp_Method
21:11:16Preparing HOLCF-Prelude/document ...
21:11:17PAC_Checker: theory Well_Quasi_Orders.Almost_Full
21:11:19PAC_Checker: theory PAC_Checker.PAC_Assoc_Map_Rel
21:11:19PAC_Checker: theory HOL-Algebra.Multiplicative_Group
21:11:20PAC_Checker: theory Well_Quasi_Orders.Minimal_Bad_Sequences
21:11:20PAC_Checker: theory Well_Quasi_Orders.Almost_Full_Relations
21:11:21PAC_Checker: theory Polynomials.Utils
21:11:21PAC_Checker: theory Well_Quasi_Orders.Well_Quasi_Orders
21:11:22PAC_Checker: theory Polynomials.Power_Products
21:11:24PAC_Checker: theory HOL-Algebra.Ring_Divisibility
21:11:24PAC_Checker: theory HOL-Algebra.Subrings
21:11:26Finished HOLCF-Prelude/document (0:00:09 elapsed time)
21:11:26Preparing HOLCF-Prelude/outline ...
21:11:27Virtual_Substitution: theory Virtual_Substitution.DNF
21:11:27Virtual_Substitution: theory Virtual_Substitution.Heuristic
21:11:32Finished HOLCF-Prelude/outline (0:00:06 elapsed time)
21:11:33Timing HOLCF-Prelude (4 threads, 69.765s elapsed time, 195.978s cpu time, 4.276s GC time, factor 2.81)
21:11:33Finished HOLCF-Prelude (0:01:27 elapsed time, 0:03:43 cpu time, factor 2.55)
21:11:33Building IMP2 ...
21:11:33HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm
21:11:35IMP2: theory HOL-Library.Cancellation
21:11:35IMP2: theory IMP2.Named_Simpsets
21:11:35IMP2: theory IMP2.IMP2_Utils
21:11:35IMP2: theory HOL-Library.Rewrite
21:11:35IMP2: theory IMP2.Subgoal_Focus_Some
21:11:36IMP2: theory HOL-Library.Multiset
21:11:36PAC_Checker: theory HOL-Algebra.Polynomials
21:11:37Virtual_Substitution: theory Virtual_Substitution.LinearCase
21:11:38Virtual_Substitution: theory Virtual_Substitution.NegInfinity
21:11:39Virtual_Substitution: theory Virtual_Substitution.QuadraticCase
21:11:40Virtual_Substitution: theory Virtual_Substitution.EliminateVariable
21:11:41Virtual_Substitution: theory Virtual_Substitution.LuckyFind
21:11:41Virtual_Substitution: theory Virtual_Substitution.EqualityVS
21:11:42Virtual_Substitution: theory Virtual_Substitution.Infinitesimals
21:11:42HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs
21:11:42Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni
21:11:44Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni
21:11:46IMP2: theory IMP2.IMP2_Aux_Lemmas
21:11:46Virtual_Substitution: theory Virtual_Substitution.DNFUni
21:11:47Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs
21:11:48PAC_Checker: theory Polynomials.MPoly_Type_Class
21:11:51IMP2: theory HOL-Eisbach.Eisbach
21:11:51IMP2: theory IMP2.Syntax
21:11:51Virtual_Substitution: theory Virtual_Substitution.VSQuad
21:11:52Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs
21:11:52Preparing Simpl/document ...
21:11:52IMP2: theory HOL-Eisbach.Eisbach_Tools
21:11:53Virtual_Substitution: theory Virtual_Substitution.Exports
21:11:56IMP2: theory IMP2.Semantics
21:12:01Virtual_Substitution: theory Virtual_Substitution.ExportProofs
21:12:03IMP2: theory IMP2.Annotated_Syntax
21:12:03PAC_Checker: theory PAC_Checker.PAC_More_Poly
21:12:05PAC_Checker: theory PAC_Checker.PAC_Specification
21:12:05IMP2: theory IMP2.Parser
21:12:05IMP2: theory IMP2.IMP2_Basic_Simpset
21:12:05PAC_Checker: theory PAC_Checker.PAC_Polynomials
21:12:05PAC_Checker: theory PAC_Checker.PAC_Checker_Specification
21:12:05IMP2: theory IMP2.IMP2_Var_Postprocessor
21:12:05IMP2: theory IMP2.IMP2_Basic_Decls
21:12:05IMP2: theory IMP2.IMP2_Var_Abs
21:12:06IMP2: theory IMP2.IMP2_Program_Analysis
21:12:07HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes
21:12:07PAC_Checker: theory PAC_Checker.PAC_Polynomials_Term
21:12:08IMP2: theory IMP2.IMP2_Specification
21:12:08IMP2: theory IMP2.IMP2_VCG
21:12:08Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Algorithms
21:12:09IMP2: theory IMP2.IMP2
21:12:17PAC_Checker: theory PAC_Checker.PAC_Polynomials_Operations
21:12:21IMP2: theory IMP2.Examples
21:12:21IMP2: theory IMP2.IMP2_from_IMP
21:12:21IMP2: theory IMP2.Quickstart_Guide
21:12:28Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Explicit
21:12:28PAC_Checker: theory PAC_Checker.PAC_Checker
21:12:28Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Algorithms
21:12:32HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid
21:12:38Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Translate
21:12:42Finished Simpl/document (0:00:50 elapsed time)
21:12:42Preparing Simpl/outline ...
21:12:45PAC_Checker: theory PAC_Checker.PAC_Checker_Relation
21:12:48PAC_Checker: theory PAC_Checker.PAC_Checker_Init
21:13:07Finished Simpl/outline (0:00:25 elapsed time)
21:13:08Timing Simpl (4 threads, 129.526s elapsed time, 450.063s cpu time, 14.790s GC time, factor 3.47)
21:13:08Finished Simpl (0:02:41 elapsed time, 0:08:28 cpu time, factor 3.14)
21:13:08Running CoSMed ...
21:13:10CoSMed: theory Fresh_Identifiers.Fresh
21:13:10CoSMed: theory Fresh_Identifiers.Fresh_String
21:13:11CoSMed: theory CoSMed.Prelim
21:13:19CoSMed: theory CoSMed.System_Specification
21:13:20Preparing HOL-Proofs-Extraction/document ...
21:13:23PAC_Checker: theory PAC_Checker.PAC_Checker_Synthesis
21:13:25Finished HOL-Proofs-Extraction/document (0:00:05 elapsed time)
21:13:25Preparing HOL-Proofs-Extraction/outline ...
21:13:30Finished HOL-Proofs-Extraction/outline (0:00:04 elapsed time)
21:13:30Timing HOL-Proofs-Extraction (4 threads, 191.164s elapsed time, 313.861s cpu time, 10.095s GC time, factor 1.64)
21:13:30Finished HOL-Proofs-Extraction (0:03:16 elapsed time, 0:05:21 cpu time, factor 1.64)
21:13:30Running Distributed_Distinct_Elements ...
21:13:35CoSMed: theory CoSMed.Automation_Setup
21:13:35CoSMed: theory CoSMed.Safety_Properties
21:13:36Distributed_Distinct_Elements: theory Flow_Networks.Graph
21:13:36Distributed_Distinct_Elements: theory HOL-Combinatorics.Stirling
21:13:36Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
21:13:36Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
21:13:36CoSMed: theory CoSMed.Observation_Setup
21:13:36CoSMed: theory CoSMed.Friend_Intro
21:13:36CoSMed: theory CoSMed.Friend_Value_Setup
21:13:37Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
21:13:37Distributed_Distinct_Elements: theory HOL-Number_Theory.Cong
21:13:37CoSMed: theory CoSMed.Friend_Request_Intro
21:13:37CoSMed: theory CoSMed.Friend_Request_Value_Setup
21:13:37CoSMed: theory CoSMed.Post_Intro
21:13:37CoSMed: theory CoSMed.Post_Value_Setup
21:13:37Distributed_Distinct_Elements: theory HOL-Library.Case_Converter
21:13:38Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
21:13:38Distributed_Distinct_Elements: theory HOL-Library.Code_Lazy
21:13:38CoSMed: theory CoSMed.Traceback_Intro
21:13:38CoSMed: theory CoSMed.Friend_Traceback
21:13:39CoSMed: theory CoSMed.Post
21:13:39Distributed_Distinct_Elements: theory HOL-Algebra.IntRing
21:13:40Distributed_Distinct_Elements: theory HOL-Library.List_Lexorder
21:13:40Distributed_Distinct_Elements: theory HOL-Library.Power_By_Squaring
21:13:40Distributed_Distinct_Elements: theory Flow_Networks.Network
21:13:40CoSMed: theory CoSMed.Friend
21:13:40Distributed_Distinct_Elements: theory HOL-Number_Theory.Mod_Exp
21:13:40Distributed_Distinct_Elements: theory HOL-Library.Transitive_Closure_Table
21:13:40CoSMed: theory CoSMed.Post_Visibility_Traceback
21:13:41Distributed_Distinct_Elements: theory HOL-Library.Bourbaki_Witt_Fixpoint
21:13:41Distributed_Distinct_Elements: theory HOL-Number_Theory.Eratosthenes
21:13:41Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
21:13:42CoSMed: theory CoSMed.Friend_Request
21:13:42Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Preliminary_Results
21:13:42Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
21:13:42Distributed_Distinct_Elements: theory HOL-Library.Going_To_Filter
21:13:42Distributed_Distinct_Elements: theory Flow_Networks.Residual_Graph
21:13:42Distributed_Distinct_Elements: theory Frequency_Moments.Landau_Ext
21:13:42Distributed_Distinct_Elements: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
21:13:44Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
21:13:45Preparing Universal_Turing_Machine/document ...
21:13:46Distributed_Distinct_Elements: theory Flow_Networks.Augmenting_Flow
21:13:46Distributed_Distinct_Elements: theory Flow_Networks.Augmenting_Path
21:13:46Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Tau_Additivity
21:13:46Distributed_Distinct_Elements: theory Flow_Networks.Ford_Fulkerson
21:13:47Distributed_Distinct_Elements: theory HOL-Number_Theory.Fib
21:13:47Distributed_Distinct_Elements: theory HOL-Number_Theory.Prime_Powers
21:13:48Distributed_Distinct_Elements: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
21:13:49Distributed_Distinct_Elements: theory MFMC_Countable.MFMC_Finite
21:13:49Distributed_Distinct_Elements: theory HOL-Number_Theory.Totient
21:13:50Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
21:13:50Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Contour_Integration
21:13:50Distributed_Distinct_Elements: theory HOL-Number_Theory.Residues
21:13:51Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Factorization_Ext
21:13:52Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
21:13:52Distributed_Distinct_Elements: theory Finite_Fields.Ring_Characteristic
21:13:52Distributed_Distinct_Elements: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
21:13:53Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Winding_Numbers
21:13:54Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
21:13:57Distributed_Distinct_Elements: theory HOL-Number_Theory.Euler_Criterion
21:13:57Distributed_Distinct_Elements: theory HOL-Number_Theory.Pocklington
21:13:57Distributed_Distinct_Elements: theory HOL-Number_Theory.Gauss
21:13:58Distributed_Distinct_Elements: theory HOL-Number_Theory.Quadratic_Reciprocity
21:13:58Distributed_Distinct_Elements: theory HOL-Number_Theory.Residue_Primitive_Roots
21:13:58Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Conformal_Mappings
21:13:58Distributed_Distinct_Elements: theory HOL-Number_Theory.Number_Theory
21:14:00Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Singularities
21:14:01Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
21:14:01Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Residues
21:14:01Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Residue_Theorem
21:14:01Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
21:14:02Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
21:14:02Distributed_Distinct_Elements: theory Dirichlet_Series.Euler_Products
21:14:03Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
21:14:03Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Laurent_Convergence
21:14:03Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Great_Picard
21:14:03Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Riemann_Mapping
21:14:04Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Coin_Space
21:14:06Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
21:14:07Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
21:14:08Distributed_Distinct_Elements: theory MFMC_Countable.MFMC_Misc
21:14:09Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Meromorphic
21:14:10Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
21:14:10Distributed_Distinct_Elements: theory MFMC_Countable.Matrix_For_Marginals
21:14:11Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
21:14:11Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Weierstrass_Factorization
21:14:11Distributed_Distinct_Elements: theory Dirichlet_Series.More_Totient
21:14:11Distributed_Distinct_Elements: theory Dirichlet_Series.Divisor_Count
21:14:12Distributed_Distinct_Elements: theory Dirichlet_Series.Liouville_Lambda
21:14:12Distributed_Distinct_Elements: theory HOL-Complex_Analysis.Complex_Analysis
21:14:12Distributed_Distinct_Elements: theory Dirichlet_Series.Arithmetic_Summatory
21:14:12Distributed_Distinct_Elements: theory Dirichlet_Series.Partial_Summation
21:14:12Distributed_Distinct_Elements: theory Median_Method.Median
21:14:13Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series_Analysis
21:14:13Distributed_Distinct_Elements: theory MFMC_Countable.Rel_PMF_Characterisation
21:14:13Distributed_Distinct_Elements: theory Probabilistic_While.While_SPMF
21:14:13Distributed_Distinct_Elements: theory Concentration_Inequalities.Bienaymes_Identity
21:14:14Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
21:14:15Distributed_Distinct_Elements: theory Lehmer.Lehmer
21:14:15Distributed_Distinct_Elements: theory Pratt_Certificate.Pratt_Certificate
21:14:16Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
21:14:16Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
21:14:21Distributed_Distinct_Elements: theory Bertrands_Postulate.Bertrand
21:14:23Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
21:14:25Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
21:14:25Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
21:14:25Distributed_Distinct_Elements: theory Finite_Fields.Rabin_Irreducibility_Test
21:14:26Finished Universal_Turing_Machine/document (0:00:41 elapsed time)
21:14:26Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
21:14:26Preparing Universal_Turing_Machine/outline ...
21:14:29Distributed_Distinct_Elements: theory Zeta_Function.Zeta_Library
21:14:30Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
21:14:31Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
21:14:32Distributed_Distinct_Elements: theory Finite_Fields.Rabin_Irreducibility_Test_Code
21:14:32Preparing IMP2/document ...
21:14:34Distributed_Distinct_Elements: theory Executable_Randomized_Algorithms.Randomized_Algorithm
21:14:36Distributed_Distinct_Elements: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
21:14:38Finished IMP2/document (0:00:05 elapsed time)
21:14:38Preparing IMP2/outline ...
21:14:42Preparing Constructive_Cryptography_CM/document ...
21:14:42Finished IMP2/outline (0:00:04 elapsed time)
21:14:42Timing IMP2 (4 threads, 161.530s elapsed time, 437.529s cpu time, 4.412s GC time, factor 2.71)
21:14:42Finished IMP2 (0:02:57 elapsed time, 0:07:43 cpu time, factor 2.60)
21:14:42Building Dirichlet_Series ...
21:14:44Finished Universal_Turing_Machine/outline (0:00:18 elapsed time)
21:14:44Timing Universal_Turing_Machine (4 threads, 544.886s elapsed time, 1728.767s cpu time, 20.388s GC time, factor 3.17)
21:14:44Finished Universal_Turing_Machine (0:09:08 elapsed time, 0:28:55 cpu time, factor 3.16)
21:14:44Building SM_Base ...
21:14:45Distributed_Distinct_Elements: theory Finite_Fields.Find_Irreducible_Poly
21:14:46Dirichlet_Series: theory HOL-Combinatorics.Stirling
21:14:46Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure
21:14:46Dirichlet_Series: theory HOL-Library.Adhoc_Overloading
21:14:46Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field
21:14:47Dirichlet_Series: theory HOL-Library.Monad_Syntax
21:14:47Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers
21:14:47Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree
21:14:48Dirichlet_Series: theory HOL-Number_Theory.Cong
21:14:48Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat
21:14:48Dirichlet_Series: theory HOL-Library.Code_Target_Nat
21:14:48Dirichlet_Series: theory HOL-Library.Code_Target_Int
21:14:48Dirichlet_Series: theory HOL-Algebra.Congruence
21:14:48Dirichlet_Series: theory HOL-Library.Code_Target_Numeral
21:14:48Dirichlet_Series: theory HOL-Library.Function_Algebras
21:14:49SM_Base: theory Partial_Order_Reduction.Set_Extensions
21:14:49SM_Base: theory Partial_Order_Reduction.Basic_Extensions
21:14:49SM_Base: theory HOL-Library.Complete_Partial_Order2
21:14:49SM_Base: theory HOL-Library.Case_Converter
21:14:49Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction
21:14:49Dirichlet_Series: theory HOL-Library.Power_By_Squaring
21:14:49SM_Base: theory Partial_Order_Reduction.Functions
21:14:49Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes
21:14:50Dirichlet_Series: theory HOL-Algebra.Order
21:14:50SM_Base: theory HOL-Library.Simps_Case_Conv
21:14:50SM_Base: theory HOL-Library.Stream
21:14:50SM_Base: theory Partial_Order_Reduction.Relation_Extensions
21:14:51SM_Base: theory DFS_Framework.DFS_Framework_Misc
21:14:51Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp
21:14:51Dirichlet_Series: theory Bernoulli.Bernoulli
21:14:51SM_Base: theory HOL-Library.Sublist
21:14:51SM_Base: theory HOL-Library.Countable_Set
21:14:51Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:14:51Distributed_Distinct_Elements: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
21:14:51Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial
21:14:52Dirichlet_Series: theory HOL-Library.Going_To_Filter
21:14:52Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly
21:14:52Dirichlet_Series: theory HOL-Number_Theory.Fib
21:14:52Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
21:14:52SM_Base: theory HOL-Library.Countable_Complete_Lattices
21:14:52Dirichlet_Series: theory HOL-Algebra.Lattice
21:14:53Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers
21:14:53Dirichlet_Series: theory HOL-Number_Theory.Totient
21:14:53SM_Base: theory LTL.LTL
21:14:54Dirichlet_Series: theory Landau_Symbols.Group_Sort
21:14:54Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra
21:14:54Dirichlet_Series: theory Matrix.Utility
21:14:54Dirichlet_Series: theory HOL-Algebra.Complete_Lattice
21:14:55Dirichlet_Series: theory Polynomial_Factorization.Missing_List
21:14:56Distributed_Distinct_Elements: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
21:14:56SM_Base: theory HOL-Library.Prefix_Order
21:14:56SM_Base: theory Partial_Order_Reduction.List_Prefixes
21:14:56SM_Base: theory Partial_Order_Reduction.List_Extensions
21:14:56SM_Base: theory DFS_Framework.DFS_Framework_Refine_Aux
21:14:56SM_Base: theory Stuttering_Equivalence.Samplers
21:14:56SM_Base: theory HOL-Library.Order_Continuity
21:14:56Dirichlet_Series: theory HOL-Algebra.Group
21:14:57SM_Base: theory Stuttering_Equivalence.StutterEquivalence
21:14:57SM_Base: theory Transition_Systems_and_Automata.Basic
21:14:57SM_Base: theory Transition_Systems_and_Automata.Sequence
21:14:57SM_Base: theory DFS_Framework.Impl_Rev_Array_Stack
21:14:57Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products
21:14:57SM_Base: theory HOL-Library.Extended_Nat
21:14:58Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
21:14:58Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
21:14:58SM_Base: theory Partial_Order_Reduction.Word_Prefixes
21:14:59SM_Base: theory Coinductive.Coinductive_Nat
21:14:59Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
21:14:59SM_Base: theory HOL-Library.Linear_Temporal_Logic_on_Streams
21:14:59Dirichlet_Series: theory HOL-Algebra.Coset
21:14:59Dirichlet_Series: theory HOL-Algebra.FiniteProduct
21:15:00Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset
21:15:00SM_Base: theory Partial_Order_Reduction.Traces
21:15:00SM_Base: theory Coinductive.Coinductive_List
21:15:00Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization
21:15:01SM_Base: theory Partial_Order_Reduction.ENat_Extensions
21:15:01SM_Base: theory Partial_Order_Reduction.CCPO_Extensions
21:15:01Dirichlet_Series: theory HOL-Algebra.Ring
21:15:01SM_Base: theory Transition_Systems_and_Automata.Sequence_LTL
21:15:02SM_Base: theory Transition_Systems_and_Automata.Transition_System
21:15:02SM_Base: theory Partial_Order_Reduction.ESet_Extensions
21:15:04SM_Base: theory Transition_Systems_and_Automata.Transition_System_Construction
21:15:05Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
21:15:05SM_Base: theory Transition_Systems_and_Automata.Transition_System_Extra
21:15:06Dirichlet_Series: theory HOL-Algebra.Generated_Groups
21:15:06SM_Base: theory DFS_Framework.Param_DFS
21:15:06SM_Base: theory Partial_Order_Reduction.Transition_System_Extensions
21:15:07Dirichlet_Series: theory HOL-Algebra.Elementary_Groups
21:15:07Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs
21:15:09Dirichlet_Series: theory Landau_Symbols.Landau_More
21:15:10SM_Base: theory Partial_Order_Reduction.Transition_System_Traces
21:15:10Dirichlet_Series: theory HOL-Algebra.AbelCoset
21:15:10Dirichlet_Series: theory HOL-Algebra.Module
21:15:12Timing HOL-Decision_Procs (4 threads, 543.946s elapsed time, 1875.554s cpu time, 104.489s GC time, factor 3.45)
21:15:12Finished HOL-Decision_Procs (0:09:10 elapsed time, 0:31:28 cpu time, factor 3.43)
21:15:12Building Regular-Sets ...
21:15:14SM_Base: theory Coinductive.Coinductive_List_Prefix
21:15:14SM_Base: theory Coinductive.Coinductive_Stream
21:15:14SM_Base: theory DFS_Framework.DFS_Invars_Basic
21:15:14SM_Base: theory DFS_Framework.General_DFS_Structure
21:15:14Dirichlet_Series: theory HOL-Algebra.Ideal
21:15:15Regular-Sets: theory Regular-Sets.Regular_Set
21:15:15SM_Base: theory Partial_Order_Reduction.Coinductive_List_Extensions
21:15:18Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
21:15:18SM_Base: theory Partial_Order_Reduction.LList_Prefixes
21:15:19SM_Base: theory Stuttering_Equivalence.PLTL
21:15:19SM_Base: theory Partial_Order_Reduction.Stuttering
21:15:19Dirichlet_Series: theory HOL-Algebra.RingHom
21:15:20SM_Base: theory Partial_Order_Reduction.Formula
21:15:20SM_Base: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
21:15:20Regular-Sets: theory Regular-Sets.Regular_Exp
21:15:20Regular-Sets: theory Regular-Sets.Regular_Exp2
21:15:20Finished Constructive_Cryptography_CM/document (0:00:38 elapsed time)
21:15:20Preparing Constructive_Cryptography_CM/outline ...
21:15:21SM_Base: theory Partial_Order_Reduction.Ample_Abstract
21:15:21Dirichlet_Series: theory HOL-Algebra.UnivPoly
21:15:23SM_Base: theory Partial_Order_Reduction.Ample_Analysis
21:15:23SM_Base: theory Partial_Order_Reduction.Ample_Correctness
21:15:23SM_Base: theory DFS_Framework.Rec_Impl
21:15:24SM_Base: theory DFS_Framework.Tailrec_Impl
21:15:24Regular-Sets: theory Regular-Sets.Equivalence_Checking2
21:15:26Regular-Sets: theory Regular-Sets.Derivatives
21:15:26Regular-Sets: theory Regular-Sets.NDerivative
21:15:26Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
21:15:26Regular-Sets: theory Regular-Sets.Regexp_Constructions
21:15:27Regular-Sets: theory Regular-Sets.Relation_Interpretation
21:15:27Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
21:15:30Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
21:15:33Regular-Sets: theory Regular-Sets.Equivalence_Checking
21:15:33Regular-Sets: theory Regular-Sets.pEquivalence_Checking
21:15:35Regular-Sets: theory Regular-Sets.Regexp_Method
21:15:35SM_Base: theory DFS_Framework.Simple_Impl
21:15:40Finished Constructive_Cryptography_CM/outline (0:00:20 elapsed time)
21:15:40Timing Constructive_Cryptography_CM (4 threads, 549.085s elapsed time, 1927.938s cpu time, 28.320s GC time, factor 3.51)
21:15:40Finished Constructive_Cryptography_CM (0:09:16 elapsed time, 0:32:22 cpu time, factor 3.49)
21:15:41Running Psi_Calculi ...
21:15:43Psi_Calculi: theory Psi_Calculi.Chain
21:15:43SM_Base: theory DFS_Framework.Restr_Impl
21:15:44Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group
21:15:45Psi_Calculi: theory Psi_Calculi.Subst_Term
21:15:46Psi_Calculi: theory Psi_Calculi.Agent
21:15:46SM_Base: theory DFS_Framework.DFS_Framework
21:15:47SM_Base: theory DFS_Framework.Reachable_Nodes
21:15:51Dirichlet_Series: theory HOL-Number_Theory.Residues
21:15:53Preparing Transition_Systems_and_Automata/document ...
21:15:55Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion
21:15:55Dirichlet_Series: theory HOL-Number_Theory.Pocklington
21:15:55Dirichlet_Series: theory HOL-Number_Theory.Gauss
21:15:56Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
21:15:56Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
21:15:57Dirichlet_Series: theory HOL-Number_Theory.Number_Theory
21:15:58Dirichlet_Series: theory Bernoulli.Bernoulli_FPS
21:15:58Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc
21:15:59Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function
21:15:59Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product
21:15:59Dirichlet_Series: theory Dirichlet_Series.Euler_Products
21:16:00Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series
21:16:03Finished Transition_Systems_and_Automata/document (0:00:10 elapsed time)
21:16:03Preparing Transition_Systems_and_Automata/outline ...
21:16:03Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
21:16:06Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu
21:16:07Dirichlet_Series: theory Dirichlet_Series.More_Totient
21:16:07Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda
21:16:07Dirichlet_Series: theory Dirichlet_Series.Divisor_Count
21:16:08Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory
21:16:08Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code
21:16:08Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
21:16:08Dirichlet_Series: theory Dirichlet_Series.Partial_Summation
21:16:08Psi_Calculi: theory Psi_Calculi.Close_Subst
21:16:08Psi_Calculi: theory Psi_Calculi.Frame
21:16:08Psi_Calculi: theory Psi_Calculi.Structural_Congruence
21:16:10Finished Transition_Systems_and_Automata/outline (0:00:06 elapsed time)
21:16:10Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
21:16:11Timing Transition_Systems_and_Automata (4 threads, 389.688s elapsed time, 1429.720s cpu time, 94.898s GC time, factor 3.67)
21:16:11Finished Transition_Systems_and_Automata (0:07:38 elapsed time, 0:25:55 cpu time, factor 3.40)
21:16:11Running Security_Protocol_Refinement ...
21:16:13Security_Protocol_Refinement: theory Security_Protocol_Refinement.Infra
21:16:13Security_Protocol_Refinement: theory Security_Protocol_Refinement.Agents
21:16:14Security_Protocol_Refinement: theory Security_Protocol_Refinement.Refinement
21:16:14Psi_Calculi: theory Psi_Calculi.Semantics
21:16:14Security_Protocol_Refinement: theory Security_Protocol_Refinement.Keys
21:16:16Security_Protocol_Refinement: theory Security_Protocol_Refinement.a0n_agree
21:16:16Security_Protocol_Refinement: theory Security_Protocol_Refinement.s0g_secrecy
21:16:17Security_Protocol_Refinement: theory Security_Protocol_Refinement.Atoms
21:16:17Security_Protocol_Refinement: theory Security_Protocol_Refinement.Message
21:16:17Security_Protocol_Refinement: theory Security_Protocol_Refinement.Channels
21:16:17Security_Protocol_Refinement: theory Security_Protocol_Refinement.Runs
21:16:18Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist
21:16:19Security_Protocol_Refinement: theory Security_Protocol_Refinement.a0i_agree
21:16:19Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_auth
21:16:20Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist_iirn
21:16:22Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_auth_chan
21:16:22Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_sig
21:16:23Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_confid_chan
21:16:24Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_kerberos
21:16:24Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
21:16:24Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_enc
21:16:26Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_nssk
21:16:27Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist_inrn
21:16:28Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_kerberos
21:16:30Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_nssk
21:16:32Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos4
21:16:32Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos5
21:16:32Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos_par
21:16:34Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_nssk
21:16:36Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_nssk_par
21:16:37Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_ds
21:16:37Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_ds
21:16:38Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_ds
21:16:38Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_ds_par
21:16:39Preparing Regular-Sets/document ...
21:16:41Psi_Calculi: theory Psi_Calculi.Simulation
21:16:41Psi_Calculi: theory Psi_Calculi.Sum
21:16:41Psi_Calculi: theory Psi_Calculi.Tau_Chain
21:16:41Psi_Calculi: theory Psi_Calculi.Bisimulation
21:16:42Psi_Calculi: theory Psi_Calculi.Sim_Pres
21:16:44Psi_Calculi: theory Psi_Calculi.Sim_Struct_Cong
21:16:44Psi_Calculi: theory Psi_Calculi.Weak_Simulation
21:16:44Psi_Calculi: theory Psi_Calculi.Bisim_Pres
21:16:49Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp
21:18:09Psi_Calculi: theory Psi_Calculi.Weak_Cong_Simulation
21:18:10Finished Regular-Sets/document (0:00:07 elapsed time)
21:18:10Preparing Regular-Sets/outline ...
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Sim_Pres
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp_Pres
21:18:10Psi_Calculi: theory Psi_Calculi.Bisim_Struct_Cong
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Cong_Sim_Pres
21:18:10Psi_Calculi: theory Psi_Calculi.Bisim_Subst
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Bisimulation
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Pres
21:18:10Finished Regular-Sets/outline (0:00:05 elapsed time)
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Struct_Cong
21:18:10Timing Regular-Sets (4 threads, 63.392s elapsed time, 150.316s cpu time, 2.401s GC time, factor 2.37)
21:18:10Finished Regular-Sets (0:01:26 elapsed time, 0:03:05 cpu time, factor 2.14)
21:18:10Running ResiduatedTransitionSystem ...
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Subst
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Psi_Congruence
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Cong_Pres
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Cong_Struct_Cong
21:18:10Psi_Calculi: theory Psi_Calculi.Weak_Congruence
21:18:10Psi_Calculi: theory Psi_Calculi.Tau
21:18:10Psi_Calculi: theory Psi_Calculi.Weakening
21:18:10Psi_Calculi: theory Psi_Calculi.Tau_Sim
21:18:10Psi_Calculi: theory Psi_Calculi.Weaken_Transition
21:18:10Psi_Calculi: theory Psi_Calculi.Weaken_Stat_Imp
21:18:10SM_Base: theory DFS_Framework.Feedback_Arcs
21:18:10Psi_Calculi: theory Psi_Calculi.Weaken_Simulation
21:18:10Psi_Calculi: theory Psi_Calculi.Weaken_Bisimulation
21:18:10Psi_Calculi: theory Psi_Calculi.Tau_Stat_Imp
21:18:10Psi_Calculi: theory Psi_Calculi.Tau_Laws_No_Weak
21:18:10Psi_Calculi: theory Psi_Calculi.Tau_Laws_Weak
21:18:10ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.ResiduatedTransitionSystem
21:18:10ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.LambdaCalculus
21:18:20Preparing Virtual_Substitution/document ...
21:20:00PAC_Checker: theory PAC_Checker.PAC_Checker_MLton
21:20:00Timing SM_Base (4 threads, 228.745s elapsed time, 769.465s cpu time, 28.941s GC time, factor 3.36)
21:20:00Finished SM_Base (0:04:32 elapsed time, 0:14:08 cpu time, factor 3.11)
21:20:00Perron_Frobenius CANCELLED
21:20:00Building Stone_Kleene_Relation_Algebras ...
21:20:00Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Iterings
21:20:00Finished Virtual_Substitution/document (0:01:04 elapsed time)
21:20:00Preparing Virtual_Substitution/outline ...
21:20:00Preparing Dirichlet_Series/document ...
21:20:00Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Algebras
21:20:00Finished Virtual_Substitution/outline (0:00:17 elapsed time)
21:20:00Timing Virtual_Substitution (4 threads, 562.236s elapsed time, 1628.277s cpu time, 78.330s GC time, factor 2.90)
21:20:00Finished Virtual_Substitution (0:09:28 elapsed time, 0:27:20 cpu time, factor 2.89)
21:20:00Running HOL-Quickcheck_Examples ...
21:20:00Preparing PAC_Checker/document ...
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.AList
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.Cancellation
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.Confluence
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness
21:20:00Finished Dirichlet_Series/document (0:00:15 elapsed time)
21:20:00Preparing Dirichlet_Series/outline ...
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.Confluent_Quotient
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.Dlist
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.Multiset
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.DAList
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example
21:20:00Finished Dirichlet_Series/outline (0:00:08 elapsed time)
21:20:00HOL-Quickcheck_Examples: theory HOL-Library.DAList_Multiset
21:20:00Timing Dirichlet_Series (4 threads, 247.712s elapsed time, 817.223s cpu time, 33.302s GC time, factor 3.30)
21:20:00Finished Dirichlet_Series (0:04:42 elapsed time, 0:14:38 cpu time, factor 3.11)
21:20:00Running No_FTL_observers_Gen_Rel ...
21:20:00HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples
21:20:00No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sorts
21:20:00Stone_Kleene_Relation_Algebras: theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras
21:20:00Finished PAC_Checker/document (0:00:16 elapsed time)
21:20:00Preparing PAC_Checker/outline ...
21:20:02No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEField
21:20:02No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Points
21:20:10Finished PAC_Checker/outline (0:00:10 elapsed time)
21:20:10Timing PAC_Checker (4 threads, 561.780s elapsed time, 1988.424s cpu time, 147.717s GC time, factor 3.54)
21:20:10Finished PAC_Checker (0:09:28 elapsed time, 0:33:20 cpu time, factor 3.52)
21:20:10Running HOL-ex ...
21:20:13HOL-ex: theory HOL-ex.Quicksort
21:20:13HOL-ex: theory HOL-ex.Bubblesort
21:20:13HOL-ex: theory HOL-ex.MergeSort
21:20:13HOL-ex: theory HOL-Combinatorics.Transposition
21:20:14HOL-ex: theory HOL-Combinatorics.Perm
21:20:15HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples
21:20:15HOL-ex: theory HOL-ex.Specifications_with_bundle_mixins
21:20:15HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples
21:20:15HOL-ex: theory HOL-ex.Perm_Fragments
21:20:15HOL-ex: theory HOL-ex.Datatype_Record_Examples
21:20:16HOL-ex: theory HOL-ex.IArray_Examples
21:20:16HOL-ex: theory HOL-ex.Code_Lazy_Demo
21:20:16HOL-ex: theory HOL-ex.Refute_Examples
21:20:22HOL-ex: theory HOL-ex.Radix_Sort
21:20:22HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex
21:20:22HOL-ex: theory HOL-ex.While_Combinator_Example
21:20:22HOL-ex: theory HOL-ex.Code_Timing
21:20:22HOL-ex: theory HOL-ex.Antiquote
21:20:22HOL-ex: theory HOL-ex.Arith_Examples
21:20:23HOL-ex: theory HOL-ex.Birthday_Paradox
21:20:23HOL-ex: theory HOL-ex.CTL
21:20:23HOL-ex: theory HOL-ex.Cartouche_Examples
21:20:24HOL-ex: theory HOL-ex.Case_Product
21:20:24HOL-ex: theory HOL-ex.Chinese
21:20:24HOL-ex: theory HOL-ex.Classical
21:20:24HOL-ex: theory HOL-ex.Coercion_Examples
21:20:24HOL-ex: theory HOL-ex.Computations
21:20:25HOL-ex: theory HOL-ex.Erdoes_Szekeres
21:20:25HOL-ex: theory HOL-ex.Executable_Relation
21:20:25HOL-ex: theory HOL-ex.Execute_Choice
21:20:25HOL-ex: theory HOL-ex.Hebrew
21:20:25HOL-ex: theory HOL-ex.Hex_Bin_Examples
21:20:25HOL-ex: theory HOL-ex.Intuitionistic
21:20:26HOL-ex: theory HOL-ex.Join_Theory
21:20:26HOL-ex: theory HOL-ex.Lagrange
21:20:26HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples
21:20:26HOL-ex: theory HOL-ex.LocaleTest2
21:20:27HOL-ex: theory HOL-ex.MonoidGroup
21:20:27HOL-ex: theory HOL-ex.Multiquote
21:20:28HOL-ex: theory HOL-ex.NatSum
21:20:28HOL-ex: theory HOL-ex.PER
21:20:28HOL-ex: theory HOL-ex.Peano_Axioms
21:20:28HOL-ex: theory HOL-ex.PresburgerEx
21:20:28HOL-ex: theory HOL-ex.Residue_Ring
21:20:28HOL-ex: theory HOL-ex.Serbian
21:20:28HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples
21:20:29HOL-ex: theory HOL-ex.Set_Theory
21:20:30HOL-ex: theory HOL-ex.Simproc_Tests
21:20:31HOL-ex: theory HOL-ex.Sketch_and_Explore
21:20:31HOL-ex: theory HOL-ex.Sorting_Algorithms_Examples
21:20:32No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Norms
21:20:32No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Functions
21:20:32No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.WorldView
21:20:33HOL-ex: theory HOL-ex.Sudoku
21:20:33HOL-ex: theory HOL-ex.Tarski
21:20:34HOL-ex: theory HOL-ex.Termination
21:20:35HOL-ex: theory HOL-ex.ThreeDivides
21:20:35HOL-ex: theory HOL-ex.Transfer_Int_Nat
21:20:35HOL-ex: theory HOL-ex.Tree23
21:20:35HOL-ex: theory HOL-ex.Unification
21:20:39HOL-ex: theory HOL-ex.veriT_Preprocessing
21:20:41HOL-ex: theory HOL-ex.Transfer_Debug
21:20:41HOL-ex: theory HOL-ex.Function_Growth
21:20:43No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxTriangleInequality
21:20:43HOL-ex: theory HOL-ex.SOS
21:20:43HOL-ex: theory HOL-ex.SOS_Cert
21:20:43HOL-ex: theory HOL-ex.Argo_Examples
21:20:43HOL-ex: theory HOL-ex.Ballot
21:20:44No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Vectors
21:20:46HOL-ex: theory HOL-ex.BigO
21:20:46No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEventMinus
21:20:46HOL-ex: theory HOL-ex.BinEx
21:20:46HOL-ex: theory HOL-ex.Code_Binary_Nat_examples
21:23:05FATAL: command execution failed
21:23:05java.io.EOFException
21:23:05 at java.base/java.io.ObjectInputStream$PeekInputStream.readFully(ObjectInputStream.java:2915)
21:23:05 at java.base/java.io.ObjectInputStream$BlockDataInputStream.readShort(ObjectInputStream.java:3410)
21:23:05 at java.base/java.io.ObjectInputStream.readStreamHeader(ObjectInputStream.java:954)
21:23:05 at java.base/java.io.ObjectInputStream.<init>(ObjectInputStream.java:392)
21:23:05 at hudson.remoting.ObjectInputStreamEx.<init>(ObjectInputStreamEx.java:50)
21:23:05 at hudson.remoting.Command.readFrom(Command.java:142)
21:23:05 at hudson.remoting.Command.readFrom(Command.java:128)
21:23:05 at hudson.remoting.AbstractSynchronousByteArrayCommandTransport.read(AbstractSynchronousByteArrayCommandTransport.java:35)
21:23:05 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:61)
21:23:05Caused: java.io.IOException: Unexpected termination of the channel
21:23:05 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:75)
21:23:05Caused: java.io.IOException: Backing channel 'workermta1' is disconnected.
21:23:05 at hudson.remoting.RemoteInvocationHandler.channelOrFail(RemoteInvocationHandler.java:215)
21:23:05 at hudson.remoting.RemoteInvocationHandler.invoke(RemoteInvocationHandler.java:285)
21:23:05 at jdk.proxy2/jdk.proxy2.$Proxy156.isAlive(Unknown Source)
21:23:05 at hudson.Launcher$RemoteLauncher$ProcImpl.isAlive(Launcher.java:1212)
21:23:05 at hudson.Launcher$RemoteLauncher$ProcImpl.join(Launcher.java:1204)
21:23:05 at hudson.tasks.CommandInterpreter.join(CommandInterpreter.java:195)
21:23:05 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:145)
21:23:05 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:92)
21:23:05 at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
21:23:05 at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
21:23:05 at hudson.model.Build$BuildExecution.build(Build.java:199)
21:23:05 at hudson.model.Build$BuildExecution.doRun(Build.java:164)
21:23:05 at hudson.model.AbstractBuild$AbstractBuildExecution.run(AbstractBuild.java:526)
21:23:05 at hudson.model.Run.execute(Run.java:1895)
21:23:05 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
21:23:05 at hudson.model.ResourceController.execute(ResourceController.java:101)
21:23:05 at hudson.model.Executor.run(Executor.java:442)
21:23:05FATAL: Unable to delete script file /tmp/jenkins2977138066680684822.sh
21:23:05java.io.EOFException
21:23:05 at java.base/java.io.ObjectInputStream$PeekInputStream.readFully(ObjectInputStream.java:2915)
21:23:05 at java.base/java.io.ObjectInputStream$BlockDataInputStream.readShort(ObjectInputStream.java:3410)
21:23:05 at java.base/java.io.ObjectInputStream.readStreamHeader(ObjectInputStream.java:954)
21:23:05 at java.base/java.io.ObjectInputStream.<init>(ObjectInputStream.java:392)
21:23:05 at hudson.remoting.ObjectInputStreamEx.<init>(ObjectInputStreamEx.java:50)
21:23:05 at hudson.remoting.Command.readFrom(Command.java:142)
21:23:05 at hudson.remoting.Command.readFrom(Command.java:128)
21:23:05 at hudson.remoting.AbstractSynchronousByteArrayCommandTransport.read(AbstractSynchronousByteArrayCommandTransport.java:35)
21:23:05 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:61)
21:23:05Caused: java.io.IOException: Unexpected termination of the channel
21:23:05 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:75)
21:23:05Caused: hudson.remoting.ChannelClosedException: Channel "hudson.remoting.Channel@2d2c750c:workermta1": Remote call on workermta1 failed. The channel is closing down or has closed down
21:23:05 at hudson.remoting.Channel.call(Channel.java:996)
21:23:05 at hudson.FilePath.act(FilePath.java:1230)
21:23:05 at hudson.FilePath.act(FilePath.java:1219)
21:23:05 at hudson.FilePath.delete(FilePath.java:1766)
21:23:05 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:163)
21:23:05 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:92)
21:23:05 at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
21:23:05 at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
21:23:05 at hudson.model.Build$BuildExecution.build(Build.java:199)
21:23:05 at hudson.model.Build$BuildExecution.doRun(Build.java:164)
21:23:05 at hudson.model.AbstractBuild$AbstractBuildExecution.run(AbstractBuild.java:526)
21:23:05 at hudson.model.Run.execute(Run.java:1895)
21:23:05 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
21:23:05 at hudson.model.ResourceController.execute(ResourceController.java:101)
21:23:05 at hudson.model.Executor.run(Executor.java:442)
21:23:05Build step 'Execute shell' marked build as failure
21:23:06ERROR: Failed to evaluate groovy script.
21:23:06java.lang.NullPointerException: Cannot invoke method child() on null object
21:23:06 at org.codehaus.groovy.runtime.NullObject.invokeMethod(NullObject.java:91)
21:23:06 at org.codehaus.groovy.runtime.callsite.PogoMetaClassSite.call(PogoMetaClassSite.java:47)
21:23:06 at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47)
21:23:06 at org.codehaus.groovy.runtime.callsite.NullCallSite.call(NullCallSite.java:34)
21:23:06 at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47)
21:23:06 at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:116)
21:23:06 at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:128)
21:23:06 at Script1.run(Script1.groovy:4)
21:23:06 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:574)
21:23:06 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:612)
21:23:06 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:583)
21:23:06 at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:373)
21:23:06 at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:310)
21:23:06 at org.jvnet.hudson.plugins.groovypostbuild.GroovyPostbuildRecorder.perform(GroovyPostbuildRecorder.java:434)
21:23:06 at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
21:23:06 at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
21:23:06 at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767)
21:23:06 at hudson.model.Build$BuildExecution.post2(Build.java:179)
21:23:06 at hudson.model.AbstractBuild$AbstractBuildExecution.post(AbstractBuild.java:711)
21:23:06 at hudson.model.Run.execute(Run.java:1918)
21:23:06 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
21:23:06 at hudson.model.ResourceController.execute(ResourceController.java:101)
21:23:06 at hudson.model.Executor.run(Executor.java:442)
21:23:06Build step 'Groovy Postbuild' marked build as failure
21:23:06Started calculate disk usage of build
21:23:06Finished Calculation of disk usage of build in 0 seconds
21:23:07Finished: FAILURE
![[Jenkins]](/jenkins/static/f7776f3e/images/svgs/logo.svg){kind=logo}
