Skipping 392 KB.. Full Log

Affine_Arithmetic: theory Word_Lib.Signed_Division_Word
22:25:18 CAVA_Setup: theory DFS_Framework.Restr_Impl
22:25:18 CAVA_Setup: theory SM.Type_System
22:25:18 Affine_Arithmetic: theory Word_Lib.More_Word
22:25:19 Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
22:25:19 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
22:25:20 Datatype_Order_Generator: theory Native_Word.Uint32
22:25:20 CAVA_Setup: theory DFS_Framework.DFS_Framework
22:25:20 CAVA_Setup: theory DFS_Framework.Reachable_Nodes
22:25:21 Timing E_Transcendental (1 threads, 248.994s elapsed time, 267.705s cpu time, 21.867s GC time, factor 1.08)
22:25:21 Finished E_Transcendental (0:04:35 elapsed time, 0:05:10 cpu time, factor 1.13)
22:25:21 CAVA_Setup: theory SM.SM_Finite_Reachable
22:25:21 MSO_Regex_Equivalence: theory MSO_Regex_Equivalence.M2L_Equivalence_Checking
22:25:21 MSO_Regex_Equivalence: theory MSO_Regex_Equivalence.WS1S_Equivalence_Checking
22:25:21 Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base
22:25:21 Datatype_Order_Generator: theory Collections.HashCode
22:25:21 Affine_Arithmetic: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:25:21 Datatype_Order_Generator: theory Datatype_Order_Generator.Hash_Generator
22:25:21 Datatype_Order_Generator: theory Datatype_Order_Generator.Derive
22:25:21 Affine_Arithmetic: theory Word_Lib.Least_significant_bit
22:25:22 Datatype_Order_Generator: theory Datatype_Order_Generator.Derive_Examples
22:25:23 Affine_Arithmetic: theory Word_Lib.Most_significant_bit
22:25:23 Affine_Arithmetic: theory Word_Lib.Generic_set_bit
22:25:23 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
22:25:24 Affine_Arithmetic: theory Affine_Arithmetic.Intersection
22:25:24 Affine_Arithmetic: theory Native_Word.Code_Target_Integer_Bit
22:25:24 Affine_Arithmetic: theory Native_Word.Word_Type_Copies
22:25:25 Turans_Graph_Theorem: theory HOL-Library.Log_Nat
22:25:26 Turans_Graph_Theorem: theory HOL-Library.Float
22:25:30 Quantales: theory Kleene_Algebra.Conway
22:25:30 Timing No_FTL_observers_Gen_Rel (1 threads, 1094.267s elapsed time, 1136.254s cpu time, 57.572s GC time, factor 1.04)
22:25:30 Finished No_FTL_observers_Gen_Rel (0:18:16 elapsed time, 0:19:01 cpu time, factor 1.04)
22:25:31 Affine_Arithmetic: theory Native_Word.Uint32
22:25:33 CommCSL: theory CommCSL.NonInterference
22:25:33 Affine_Arithmetic: theory Collections.HashCode
22:25:33 Affine_Arithmetic: theory Deriving.Hash_Generator
22:25:34 Affine_Arithmetic: theory Deriving.Hash_Instances
22:25:34 Affine_Arithmetic: theory Deriving.Derive
22:25:36 Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
22:25:37 Running Linear_Recurrences_Solver (on 10.195.8.32+4-7) ...
22:25:38 Finite_Fields: theory Finite_Fields.Ring_Characteristic
22:25:39 DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
22:25:39 Timing CommCSL (1 threads, 296.168s elapsed time, 296.118s cpu time, 72.067s GC time, factor 1.00)
22:25:39 Finished CommCSL (0:05:00 elapsed time, 0:05:00 cpu time, factor 1.00)
22:25:39 Quantales: theory Kleene_Algebra.Kleene_Algebra
22:25:39 CAVA_Setup: theory SM.Rename_Cfg
22:25:41 CAVA_Setup: theory Gabow_SCC.Gabow_GBG_Code
22:25:41 CAVA_Setup: theory Gabow_SCC.Gabow_SCC_Code
22:25:44 Turans_Graph_Theorem: theory HOL-Library.Code_Target_Numeral_Float
22:25:44 Turans_Graph_Theorem: theory HOL-Library.Interval_Float
22:25:44 CAVA_Setup: theory SM.SM_Visible
22:25:45 CAVA_Setup: theory SM.SM_Pid
22:25:48 Zeta_Function: theory Budan_Fourier.BF_Misc
22:25:48 CAVA_Setup: theory SM.SM_Variables
22:25:49 CAVA_Setup: theory SM.SM_Indep
22:25:49 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation_Bounds
22:25:49 Running VerifyThis2018 (on 10.195.8.29+8) ...
22:25:50 Linear_Recurrences_Solver: theory Pure-ex.Guess
22:25:50 Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
22:25:52 Building Pi_Transcendental (on 10.195.8.49+8) ...
22:25:52 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
22:25:52 VerifyThis2018: theory VerifyThis2018.Synth_Definition
22:25:52 Quantales: theory Quantales.Quantales
22:25:53 VerifyThis2018: theory VerifyThis2018.Dynamic_Array
22:25:55 Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
22:25:55 Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
22:25:55 VerifyThis2018: theory VerifyThis2018.DF_System
22:25:55 Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
22:25:55 Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
22:25:57 Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
22:25:58 VerifyThis2018: theory VerifyThis2018.DRAT_Misc
22:25:58 VerifyThis2018: theory VerifyThis2018.Array_Map_Default
22:25:58 Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
22:25:58 Affine_Arithmetic: theory HOL-Library.RBT
22:25:58 Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
22:25:58 Affine_Arithmetic: theory HOL-Library.RBT_Mapping
22:25:59 Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
22:26:00 VerifyThis2018: theory VerifyThis2018.Exc_Nres_Monad
22:26:00 Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
22:26:01 Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
22:26:01 Linear_Recurrences_Solver: theory Deriving.Compare_Rat
22:26:01 CAVA_Setup: theory LTL_to_GBA.All_Of_LTL_to_GBA
22:26:02 Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
22:26:02 Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
22:26:02 Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
22:26:03 Linear_Recurrences_Solver: theory Deriving.Compare_Real
22:26:03 Pi_Transcendental: theory HOL-Library.Fun_Lexorder
22:26:03 Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
22:26:04 Linear_Recurrences_Solver: theory Polynomials.More_Modules
22:26:05 Pi_Transcendental: theory HOL-Library.Poly_Mapping
22:26:05 Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
22:26:05 CAVA_Setup: theory DFS_Framework.Feedback_Arcs
22:26:05 Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
22:26:08 VerifyThis2018: theory VerifyThis2018.VTcomp
22:26:08 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
22:26:08 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
22:26:10 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
22:26:11 VerifyThis2018: theory VerifyThis2018.Snippets
22:26:11 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
22:26:14 Pi_Transcendental: theory Polynomials.MPoly_Type
22:26:14 Running Density_Compiler (on 10.195.8.40+8) ...
22:26:14 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
22:26:15 Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
22:26:15 Turans_Graph_Theorem: theory HOL-Decision_Procs.Approximation
22:26:16 Pi_Transcendental: theory Polynomials.More_MPoly_Type
22:26:16 Affine_Arithmetic: theory Affine_Arithmetic.Print
22:26:17 Density_Compiler: theory Density_Compiler.Density_Predicates
22:26:18 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
22:26:18 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
22:26:18 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
22:26:21 CAVA_Setup: theory Promela.PromelaInvariants
22:26:22 CAVA_Setup: theory Promela.Promela
22:26:23 Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:26:24 CAVA_Setup: theory Gabow_SCC.All_Of_Gabow_SCC
22:26:25 Density_Compiler: theory Density_Compiler.PDF_Transformations
22:26:25 CAVA_Setup: theory SM.SM_Datastructures
22:26:25 CAVA_Setup: theory SM.SM_Sticky
22:26:26 VerifyThis2018: theory VerifyThis2018.Challenge1
22:26:29 Building Flow_Networks (on 10.195.8.30+4-7) ...
22:26:31 CAVA_Setup: theory SM.SM_POR
22:26:32 DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
22:26:32 Flow_Networks: theory CAVA_Base.Statistics
22:26:32 Flow_Networks: theory Flow_Networks.Graph
22:26:33 Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
22:26:34 DiscretePricing: theory DiscretePricing.Fair_Price
22:26:35 Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
22:26:35 Density_Compiler: theory Density_Compiler.PDF_Values
22:26:35 CAVA_Setup: theory SM.SM_Ample_Impl
22:26:36 Finite_Fields: theory HOL-Number_Theory.Fib
22:26:37 VerifyThis2018: theory VerifyThis2018.Challenge1_short
22:26:37 Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
22:26:37 Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
22:26:37 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
22:26:38 Finite_Fields: theory HOL-Number_Theory.Prime_Powers
22:26:38 Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
22:26:41 Finite_Fields: theory HOL-Number_Theory.Totient
22:26:42 Flow_Networks: theory HOL-Library.Omega_Words_Fun
22:26:45 Flow_Networks: theory CAVA_Automata.Digraph_Basic
22:26:45 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
22:26:45 Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
22:26:45 Finite_Fields: theory HOL-Number_Theory.Residues
22:26:46 Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
22:26:47 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
22:26:47 VerifyThis2018: theory VerifyThis2018.Challenge2
22:26:48 Pi_Transcendental: theory Symmetric_Polynomials.Vieta
22:26:49 Quantales: theory Quantales.Quantale_Models
22:26:51 Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
22:26:51 Density_Compiler: theory Density_Compiler.PDF_Semantics
22:26:53 CAVA_Setup: theory Promela.PromelaLTL
22:26:53 CAVA_Setup: theory Promela.PromelaLTLConv
22:26:53 Quantales: theory Quantales.Quantic_Nuclei_Conuclei
22:26:58 CAVA_Setup: theory Promela.All_Of_Promela
22:26:58 Flow_Networks: theory DFS_Framework.DFS_Framework_Misc
22:26:58 Flow_Networks: theory Program-Conflict-Analysis.LTS
22:26:59 Flow_Networks: theory DFS_Framework.DFS_Framework_Refine_Aux
22:27:00 Flow_Networks: theory Flow_Networks.Fofu_Abs_Base
22:27:01 Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
22:27:01 Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
22:27:02 Flow_Networks: theory CAVA_Base.Code_String
22:27:02 Flow_Networks: theory CAVA_Base.CAVA_Code_Target
22:27:02 Flow_Networks: theory CAVA_Base.CAVA_Base
22:27:02 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
22:27:02 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
22:27:03 Flow_Networks: theory CAVA_Automata.Digraph
22:27:03 Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
22:27:03 Zeta_Function: theory Zeta_Function.Zeta_Function
22:27:04 Finite_Fields: theory HOL-Number_Theory.Gauss
22:27:04 Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
22:27:05 Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
22:27:05 Flow_Networks: theory CAVA_Automata.Digraph_Impl
22:27:05 Timing Datatype_Order_Generator (8 threads, 85.601s elapsed time, 227.093s cpu time, 78.532s GC time, factor 2.65)
22:27:05 Finished Datatype_Order_Generator (0:01:55 elapsed time, 0:04:45 cpu time, factor 2.48)
22:27:06 Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
22:27:08 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic_Misc
22:27:08 Turans_Graph_Theorem: theory Girth_Chromatic.Ugraphs
22:27:09 Quantales: theory Quantales.Quantale_Left_Sided
22:27:10 Turans_Graph_Theorem: theory Girth_Chromatic.Girth_Chromatic
22:27:13 DiscretePricing: theory DiscretePricing.CRR_Model
22:27:13 Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
22:27:14 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
22:27:14 Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
22:27:16 Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
22:27:18 Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
22:27:19 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
22:27:20 VerifyThis2018: theory VerifyThis2018.Challenge3
22:27:20 CAVA_Setup: theory SM.SM_Wrapup
22:27:22 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
22:27:23 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
22:27:24 Quantales: theory Quantales.Quantale_Star
22:27:24 Turans_Graph_Theorem: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
22:27:29 Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
22:27:29 Turans_Graph_Theorem: theory Turans_Graph_Theorem.Turan
22:27:30 Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
22:27:32 Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
22:27:33 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
22:27:34 Timing Pi_Transcendental (1 threads, 78.605s elapsed time, 77.060s cpu time, 3.245s GC time, factor 0.98)
22:27:34 Finished Pi_Transcendental (0:01:41 elapsed time, 0:01:39 cpu time, factor 0.98)
22:27:35 Zeta_Function: theory Zeta_Function.Zeta_Laurent_Expansion
22:27:36 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
22:27:37 Flow_Networks: theory DFS_Framework.Impl_Rev_Array_Stack
22:27:40 Zeta_Function: theory Zeta_Function.Hadjicostas_Chapman
22:27:40 Quantales: theory Quantales.Quantale_Modules
22:27:41 Flow_Networks: theory DFS_Framework.Param_DFS
22:27:42 Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
22:27:43 Timing Affine_Arithmetic (8 threads, 130.695s elapsed time, 722.778s cpu time, 69.459s GC time, factor 5.53)
22:27:43 Finished Affine_Arithmetic (0:02:43 elapsed time, 0:13:17 cpu time, factor 4.87)
22:27:49 DiscretePricing: theory DiscretePricing.Option_Price_Examples
22:27:52 Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
22:27:52 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
22:27:54 Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
22:27:55 Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
22:27:59 Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
22:28:06 Timing Quantales (1 threads, 165.853s elapsed time, 163.006s cpu time, 9.151s GC time, factor 0.98)
22:28:06 Finished Quantales (0:03:09 elapsed time, 0:03:06 cpu time, factor 0.98)
22:28:07 Timing Turans_Graph_Theorem (1 threads, 209.215s elapsed time, 205.637s cpu time, 10.604s GC time, factor 0.98)
22:28:07 Finished Turans_Graph_Theorem (0:03:34 elapsed time, 0:03:30 cpu time, factor 0.98)
22:28:08 Timing DiscretePricing (1 threads, 183.181s elapsed time, 182.896s cpu time, 16.162s GC time, factor 1.00)
22:28:08 Finished DiscretePricing (0:03:12 elapsed time, 0:03:11 cpu time, factor 1.00)
22:28:08 Timing VerifyThis2018 (1 threads, 135.152s elapsed time, 126.703s cpu time, 2.663s GC time, factor 0.94)
22:28:08 Finished VerifyThis2018 (0:02:18 elapsed time, 0:02:10 cpu time, factor 0.94)
22:28:09 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
22:28:13 Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
22:28:13 Flow_Networks: theory DFS_Framework.DFS_Invars_Basic
22:28:15 Timing Zeta_Function (1 threads, 174.011s elapsed time, 173.015s cpu time, 6.089s GC time, factor 0.99)
22:28:15 Finished Zeta_Function (0:03:21 elapsed time, 0:03:20 cpu time, factor 0.99)
22:28:16 Finite_Fields: theory HOL-Number_Theory.Pocklington
22:28:19 Density_Compiler: theory Density_Compiler.PDF_Compiler
22:28:21 Timing Goedel_HFSet_Semanticless (8 threads, 240.817s elapsed time, 817.253s cpu time, 92.235s GC time, factor 3.39)
22:28:21 Finished Goedel_HFSet_Semanticless (0:04:02 elapsed time, 0:13:40 cpu time, factor 3.38)
22:28:26 Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
22:28:26 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
22:28:27 Linear_Recurrences_Solver: theory Show.Show_Real
22:28:28 Linear_Recurrences_Solver: theory Show.Show_Complex
22:28:28 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
22:28:32 Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
22:28:35 Finite_Fields: theory HOL-Number_Theory.Number_Theory
22:28:36 Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
22:28:37 Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
22:28:39 Timing CAVA_Setup (8 threads, 173.588s elapsed time, 1118.592s cpu time, 203.524s GC time, factor 6.44)
22:28:39 Finished CAVA_Setup (0:03:38 elapsed time, 0:20:27 cpu time, factor 5.62)
22:28:39 Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
22:28:40 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
22:28:41 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
22:28:41 Building Quantales_Converse (on of2.proof.cit.tum.de+12-15) ...
22:28:42 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
22:28:42 Quantales_Converse: theory Kleene_Algebra.Signatures
22:28:42 Quantales_Converse: theory Order_Lattice_Props.Sup_Lattice
22:28:42 Quantales_Converse: theory Kleene_Algebra.Dioid
22:28:43 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
22:28:43 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
22:28:45 Quantales_Converse: theory Order_Lattice_Props.Order_Duality
22:28:45 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:28:46 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
22:28:48 Linear_Recurrences_Solver: theory Polynomials.Utils
22:28:49 Quantales_Converse: theory Kleene_Algebra.Conway
22:28:49 Quantales_Converse: theory Order_Lattice_Props.Order_Lattice_Props
22:28:49 Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
22:28:52 Finite_Fields: theory Dirichlet_Series.Moebius_Mu
22:28:53 Linear_Recurrences_Solver: theory Polynomials.Power_Products
22:28:54 Flow_Networks: theory DFS_Framework.General_DFS_Structure
22:28:54 Quantales_Converse: theory Kleene_Algebra.Kleene_Algebra
22:28:55 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
22:28:56 Quantales_Converse: theory Order_Lattice_Props.Galois_Connections
22:28:56 Quantales_Converse: theory Order_Lattice_Props.Closure_Operators
22:28:58 Quantales_Converse: theory Quantales.Quantales
22:28:59 Quantales_Converse: theory KAD.Domain_Semiring
22:28:59 Quantales_Converse: theory Quantales_Converse.Kleene_Algebra_Converse
22:29:00 Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
22:29:00 Running AWN (on 10.195.7.194+9) ...
22:29:02 AWN: theory AWN.Lib
22:29:02 AWN: theory AWN.AWN
22:29:05 Quantales_Converse: theory KAD.Antidomain_Semiring
22:29:07 Flow_Networks: theory DFS_Framework.Rec_Impl
22:29:09 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
22:29:14 Running Fishers_Inequality (on 10.195.6.179+9) ...
22:29:14 Quantales_Converse: theory KAD.Range_Semiring
22:29:16 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
22:29:17 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
22:29:17 Running Multirelations (on 10.195.8.42+9) ...
22:29:18 Fishers_Inequality: theory Card_Partitions.Set_Partition
22:29:18 Timing Finite_Fields (1 threads, 265.208s elapsed time, 263.921s cpu time, 52.368s GC time, factor 1.00)
22:29:18 Finished Finite_Fields (0:04:29 elapsed time, 0:04:27 cpu time, factor 0.99)
22:29:18 Running Mersenne_Primes (on 10.195.8.46+8) ...
22:29:19 Multirelations: theory Multirelations.C_Algebras
22:29:20 Running Schwartz_Zippel (on of1-proof+0-7) ...
22:29:21 Building Count_Complex_Roots (on of4.proof.cit.tum.de+4-7) ...
22:29:21 Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Misc
22:29:21 Schwartz_Zippel: theory HOL-Computational_Algebra.Fraction_Field
22:29:21 Schwartz_Zippel: theory HOL-Computational_Algebra.Squarefree
22:29:21 Schwartz_Zippel: theory HOL-Library.Fun_Lexorder
22:29:21 Schwartz_Zippel: theory HOL-Library.Function_Algebras
22:29:21 Schwartz_Zippel: theory HOL-Algebra.Congruence
22:29:21 Schwartz_Zippel: theory HOL-Computational_Algebra.Nth_Powers
22:29:21 Schwartz_Zippel: theory HOL-Computational_Algebra.Group_Closure
22:29:21 Schwartz_Zippel: theory HOL-Library.Groups_Big_Fun
22:29:21 Quantales_Converse: theory KAD.Modal_Kleene_Algebra
22:29:21 Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Var
22:29:21 Schwartz_Zippel: theory Abstract-Rewriting.Seq
22:29:21 Mersenne_Primes: theory HOL-Number_Theory.Cong
22:29:21 Schwartz_Zippel: theory HOL-Library.Ramsey
22:29:21 Schwartz_Zippel: theory HOL-Library.More_List
22:29:21 Schwartz_Zippel: theory HOL-Library.While_Combinator
22:29:22 Schwartz_Zippel: theory Polynomials.More_Modules
22:29:22 Schwartz_Zippel: theory HOL-Library.Poly_Mapping
22:29:22 Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Unsorted
22:29:22 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
22:29:22 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial
22:29:22 Schwartz_Zippel: theory Jordan_Normal_Form.Conjugate
22:29:22 Schwartz_Zippel: theory Open_Induction.Restricted_Predicates
22:29:22 Schwartz_Zippel: theory HOL-Algebra.Order
22:29:22 Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom
22:29:22 Count_Complex_Roots: theory HOL-Eisbach.Eisbach
22:29:22 Schwartz_Zippel: theory HOL-Computational_Algebra.Normalized_Fraction
22:29:22 Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field
22:29:22 Count_Complex_Roots: theory Polynomial_Interpolation.Missing_Unsorted
22:29:22 Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring
22:29:22 Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:29:22 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology
22:29:22 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis
22:29:22 Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom
22:29:22 Schwartz_Zippel: theory Regular-Sets.Regular_Set
22:29:23 AWN: theory AWN.AWN_Cterms
22:29:23 Running LocalLexing (on 10.195.8.29+8) ...
22:29:23 Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
22:29:23 Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
22:29:23 Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
22:29:23 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
22:29:23 Fishers_Inequality: theory Polynomials.MPoly_Type
22:29:23 Schwartz_Zippel: theory HOL-Algebra.Lattice
22:29:23 Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools
22:29:23 Schwartz_Zippel: theory Polynomials.MPoly_Type
22:29:24 Schwartz_Zippel: theory Polynomials.More_MPoly_Type
22:29:24 Running Multirelations_Heterogeneous (on 10.195.8.49+9) ...
22:29:24 Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice
22:29:24 Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction
22:29:24 Quantales_Converse: theory Quantales.Quantale_Star
22:29:24 LocalLexing: theory LocalLexing.CFG
22:29:24 Schwartz_Zippel: theory Regular-Sets.Regular_Exp
22:29:25 LocalLexing: theory LocalLexing.LocalLexing
22:29:25 Schwartz_Zippel: theory HOL-Algebra.Group
22:29:26 Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial
22:29:26 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Relational_Properties
22:29:26 Quantales_Converse: theory Quantales_Converse.Modal_Kleene_Algebra_Converse
22:29:26 Running Containers-Benchmarks (on of3.proof.cit.tum.de+12-15) ...
22:29:27 Fishers_Inequality: theory Polynomials.More_MPoly_Type
22:29:27 LocalLexing: theory LocalLexing.LLEarleyParsing
22:29:27 Mersenne_Primes: theory Word_Lib.Bit_Comprehension
22:29:27 Containers-Benchmarks: theory HOL-Eisbach.Eisbach
22:29:27 Containers-Benchmarks: theory Automatic_Refinement.Refine_Util_Bootstrap1
22:29:27 Containers-Benchmarks: theory Automatic_Refinement.Foldi
22:29:27 Containers-Benchmarks: theory Automatic_Refinement.Prio_List
22:29:27 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Comparison
22:29:27 Containers-Benchmarks: theory Collections.ICF_Tools
22:29:27 Containers-Benchmarks: theory Finger-Trees.FingerTree
22:29:27 Containers-Benchmarks: theory Trie.Trie
22:29:27 Containers-Benchmarks: theory Binomial-Heaps.BinomialHeap
22:29:27 Containers-Benchmarks: theory Automatic_Refinement.Mk_Term_Antiquot
22:29:27 Schwartz_Zippel: theory HOL-Algebra.FiniteProduct
22:29:27 Schwartz_Zippel: theory Regular-Sets.NDerivative
22:29:27 Containers-Benchmarks: theory Automatic_Refinement.Mpat_Antiquot
22:29:27 Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
22:29:28 Containers-Benchmarks: theory Collections.Ord_Code_Preproc
22:29:28 Containers-Benchmarks: theory Collections.Locale_Code
22:29:28 Count_Complex_Roots: theory Polynomial_Interpolation.Missing_Polynomial
22:29:28 Containers-Benchmarks: theory Collections.Record_Intf
22:29:28 Count_Complex_Roots: theory Sturm_Tarski.PolyMisc
22:29:28 LocalLexing: theory LocalLexing.Limit
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Refine_Util
22:29:28 Containers-Benchmarks: theory Binomial-Heaps.SkewBinomialHeap
22:29:28 Containers-Benchmarks: theory HOL-ex.Quicksort
22:29:28 Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski
22:29:28 Schwartz_Zippel: theory HOL-Algebra.Ring
22:29:28 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set
22:29:28 Mersenne_Primes: theory Word_Lib.More_Divides
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Anti_Unification
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Attr_Comb
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Named_Sorted_Thms
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Data
22:29:28 Containers-Benchmarks: theory Automatic_Refinement.Indep_Vars
22:29:28 Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:29:29 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS
22:29:29 Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate
22:29:29 Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial
22:29:29 Containers-Benchmarks: theory Automatic_Refinement.Mk_Record_Simp
22:29:29 Containers-Benchmarks: theory Automatic_Refinement.Tagged_Solver
22:29:29 Containers-Benchmarks: theory Automatic_Refinement.Select_Solve
22:29:29 Containers-Benchmarks: theory Automatic_Refinement.Misc
22:29:29 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Default
22:29:29 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_RBT
22:29:29 Containers-Benchmarks: theory Collections.DatRef
22:29:29 Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series
22:29:30 Count_Complex_Roots: theory Polynomial_Interpolation.Ring_Hom_Poly
22:29:30 Count_Complex_Roots: theory Budan_Fourier.BF_Misc
22:29:30 Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
22:29:30 MSO_Regex_Equivalence: theory HOL-Library.Product_Lexorder
22:29:30 Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial
22:29:30 Schwartz_Zippel: theory Regular-Sets.Regexp_Method
22:29:31 MSO_Regex_Equivalence: theory MSO_Regex_Equivalence.M2L_Examples
22:29:31 MSO_Regex_Equivalence: theory MSO_Regex_Equivalence.WS1S_Examples
22:29:31 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Bool
22:29:31 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_Default
22:29:31 Mersenne_Primes: theory HOL-Number_Theory.Mod_Exp
22:29:31 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_LC
22:29:31 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_LC
22:29:31 Count_Complex_Roots: theory Budan_Fourier.Sturm_Multiple_Roots
22:29:31 AWN: theory AWN.AWN_Labels
22:29:31 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic
22:29:31 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
22:29:32 Mersenne_Primes: theory HOL-Number_Theory.Eratosthenes
22:29:32 Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial
22:29:32 Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
22:29:32 Schwartz_Zippel: theory HOL-Algebra.Module
22:29:32 Containers-Benchmarks: theory Containers-Benchmarks.Clauses
22:29:32 Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring
22:29:32 Containers-Benchmarks: theory Refine_Monadic.Refine_Chapter
22:29:32 Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
22:29:33 Containers-Benchmarks: theory Native_Word.Code_Target_Int_Bit
22:29:33 Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental
22:29:33 Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
22:29:33 Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem
22:29:33 Containers-Benchmarks: theory Collections.Code_Target_ICF
22:29:33 Quantales_Converse: theory Quantales_Converse.Modal_Quantale
22:29:33 Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:29:33 AWN: theory AWN.Inv_Cterms
22:29:33 Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
22:29:34 Count_Complex_Roots: theory Count_Complex_Roots.CC_Polynomials_Extra
22:29:34 Schwartz_Zippel: theory Polynomials.Utils
22:29:34 Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
22:29:35 AWN: theory AWN.TransitionSystems
22:29:35 Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra
22:29:35 AWN: theory AWN.AWN_SOS
22:29:35 Schwartz_Zippel: theory Polynomials.Power_Products
22:29:36 Schwartz_Zippel: theory Symmetric_Polynomials.Vieta
22:29:37 Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval
22:29:37 Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm
22:29:37 Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials
22:29:38 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Power_Allegories_Properties
22:29:38 Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
22:29:39 Containers-Benchmarks: theory Automatic_Refinement.Refine_Lib
22:29:39 Containers-Benchmarks: theory Collections.SetIterator
22:29:40 Containers-Benchmarks: theory Collections.Sorted_List_Operations
22:29:40 Mersenne_Primes: theory HOL-Number_Theory.Fib
22:29:40 Count_Complex_Roots: theory Count_Complex_Roots.Count_Line
22:29:40 LocalLexing: theory LocalLexing.LocalLexingLemmas
22:29:40 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Phases
22:29:40 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tagging
22:29:40 Containers-Benchmarks: theory Automatic_Refinement.Relators
22:29:41 Containers-Benchmarks: theory Refine_Monadic.Refine_Mono_Prover
22:29:41 LocalLexing: theory LocalLexing.InductRules
22:29:41 LocalLexing: theory LocalLexing.ListTools
22:29:41 Count_Complex_Roots: theory Count_Complex_Roots.Count_Half_Plane
22:29:41 Containers-Benchmarks: theory Collections.SetIteratorOperations
22:29:41 Count_Complex_Roots: theory Count_Complex_Roots.Count_Rectangle
22:29:41 Count_Complex_Roots: theory Count_Complex_Roots.Count_Circle
22:29:41 Mersenne_Primes: theory HOL-Number_Theory.Prime_Powers
22:29:41 LocalLexing: theory LocalLexing.Derivations
22:29:41 Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
22:29:42 Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots
22:29:42 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Multirelations_Basics
22:29:42 Containers-Benchmarks: theory Automatic_Refinement.Param_Tool
22:29:42 Containers-Benchmarks: theory Automatic_Refinement.Param_HOL
22:29:42 Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples
22:29:43 Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
22:29:44 Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
22:29:44 Mersenne_Primes: theory HOL-Number_Theory.Totient
22:29:45 AWN: theory AWN.AWN_SOS_Labels
22:29:45 Containers-Benchmarks: theory Automatic_Refinement.Parametricity
22:29:45 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Id_Ops
22:29:45 Containers-Benchmarks: theory Collections.Assoc_List
22:29:45 Containers-Benchmarks: theory Collections.Dlist_add
22:29:45 Containers-Benchmarks: theory Collections.Proper_Iterator
22:29:45 AWN: theory AWN.Invariants
22:29:45 Containers-Benchmarks: theory Collections.SetIteratorGA
22:29:46 Containers-Benchmarks: theory Collections.Diff_Array
22:29:46 Containers-Benchmarks: theory Collections.Trie_Impl
22:29:46 Containers-Benchmarks: theory Collections.It_to_It
22:29:46 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Fix_Rel
22:29:46 AWN: theory AWN.AWN_Invariants
22:29:46 Containers-Benchmarks: theory Collections.Trie2
22:29:46 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Translate
22:29:46 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Relator_Interface
22:29:46 Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
22:29:47 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Gen_Algo
22:29:47 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tool
22:29:47 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Bindings_HOL
22:29:47 Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
22:29:48 AWN: theory AWN.Qmsg
22:29:48 Mersenne_Primes: theory HOL-Number_Theory.Residues
22:29:48 Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
22:29:49 AWN: theory AWN.OInvariants
22:29:50 Running Chandy_Lamport (on 10.195.8.11+8) ...
22:29:50 Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
22:29:51 AWN: theory AWN.Pnet
22:29:52 Containers-Benchmarks: theory Automatic_Refinement.Automatic_Refinement
22:29:52 Containers-Benchmarks: theory Collections.Idx_Iterator
22:29:52 Containers-Benchmarks: theory Refine_Monadic.Refine_Misc
22:29:52 Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
22:29:52 Chandy_Lamport: theory Chandy_Lamport.Distributed_System
22:29:53 Containers-Benchmarks: theory Refine_Monadic.RefineG_Domain
22:29:53 Containers-Benchmarks: theory Refine_Monadic.RefineG_Transfer
22:29:53 Fishers_Inequality: theory Design_Theory.Multisets_Extras
22:29:53 Containers-Benchmarks: theory Refine_Monadic.RefineG_Assert
22:29:53 Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
22:29:54 Containers-Benchmarks: theory Refine_Monadic.RefineG_Recursion
22:29:54 Flow_Networks: theory DFS_Framework.Tailrec_Impl
22:29:55 Containers-Benchmarks: theory Refine_Monadic.RefineG_While
22:29:55 Containers-Benchmarks: theory Refine_Monadic.Refine_Basic
22:29:55 Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
22:29:56 Containers-Benchmarks: theory Refine_Monadic.Refine_Det
22:29:56 AWN: theory AWN.Closed
22:29:56 Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
22:29:57 AWN: theory AWN.OAWN_SOS
22:29:59 Timing MSO_Regex_Equivalence (8 threads, 335.429s elapsed time, 664.851s cpu time, 29.239s GC time, factor 1.98)
22:29:59 Finished MSO_Regex_Equivalence (0:05:37 elapsed time, 0:11:09 cpu time, factor 1.98)
22:29:59 Containers-Benchmarks: theory Refine_Monadic.Refine_Heuristics
22:29:59 Containers-Benchmarks: theory Refine_Monadic.Refine_Leof
22:29:59 Containers-Benchmarks: theory Refine_Monadic.Refine_More_Comb
22:30:00 Containers-Benchmarks: theory Refine_Monadic.Refine_Pfun
22:30:00 Containers-Benchmarks: theory Refine_Monadic.Refine_While
22:30:03 Containers-Benchmarks: theory Refine_Monadic.Refine_Transfer
22:30:03 Mersenne_Primes: theory HOL-Number_Theory.Euler_Criterion
22:30:03 Timing Density_Compiler (1 threads, 223.335s elapsed time, 223.284s cpu time, 5.109s GC time, factor 1.00)
22:30:03 Finished Density_Compiler (0:03:47 elapsed time, 0:03:47 cpu time, factor 1.00)
22:30:03 Containers-Benchmarks: theory Refine_Monadic.Autoref_Monadic
22:30:03 Containers-Benchmarks: theory Refine_Monadic.Refine_Automation
22:30:03 Containers-Benchmarks: theory Refine_Monadic.Refine_Foreach
22:30:03 Fishers_Inequality: theory Design_Theory.Design_Basics
22:30:04 Running CHERI-C_Memory_Model (on of1.proof.cit.tum.de+0-7) ...
22:30:05 Mersenne_Primes: theory HOL-Number_Theory.Gauss
22:30:05 Containers-Benchmarks: theory Refine_Monadic.Refine_Monadic
22:30:05 Containers-Benchmarks: theory Collections.Gen_Iterator
22:30:06 LocalLexing: theory LocalLexing.Validity
22:30:06 Containers-Benchmarks: theory Collections.Iterator
22:30:06 Containers-Benchmarks: theory Collections.Array_Iterator
22:30:06 Containers-Benchmarks: theory Collections.ICF_Spec_Base
22:30:06 CHERI-C_Memory_Model: theory HOL-Eisbach.Eisbach
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Signed_Words
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Legacy_Aliases
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Bit_Comprehension_Int
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Syntax_Bundles
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Hex_Words
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Type_Syntax
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Word_Syntax
22:30:06 Containers-Benchmarks: theory Collections.AnnotatedListSpec
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.More_Sublist
22:30:06 CHERI-C_Memory_Model: theory Separation_Algebra.Separation_Algebra
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Enumeration
22:30:06 CHERI-C_Memory_Model: theory Word_Lib.Even_More_List
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Norm_Words
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Word_Names
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Aligned
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Singleton_Bit_Shifts
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Many_More
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Bits_Int
22:30:07 LocalLexing: theory LocalLexing.TheoremD2
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Sgn_Abs
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Strict_part_mono
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.Word_16
22:30:07 CHERI-C_Memory_Model: theory Word_Lib.More_Misc
22:30:07 CHERI-C_Memory_Model: theory HOL-Eisbach.Eisbach_Tools
22:30:08 CHERI-C_Memory_Model: theory Word_Lib.Enumeration_Word
22:30:08 CHERI-C_Memory_Model: theory Word_Lib.Next_and_Prev
22:30:08 CHERI-C_Memory_Model: theory Word_Lib.Word_EqI
22:30:08 Containers-Benchmarks: theory Collections.FTAnnotatedListImpl
22:30:09 Fishers_Inequality: theory Design_Theory.Design_Operations
22:30:09 Multirelations: theory Multirelations.Multirelations
22:30:09 Quantales_Converse: theory Quantales_Converse.Quantale_Converse
22:30:10 Containers-Benchmarks: theory Collections.ListSpec
22:30:10 Containers-Benchmarks: theory Collections.MapSpec
22:30:10 Containers-Benchmarks: theory Collections.PrioSpec
22:30:10 Containers-Benchmarks: theory Collections.PrioUniqueSpec
22:30:10 Containers-Benchmarks: theory Collections.SetSpec
22:30:10 Containers-Benchmarks: theory Collections.RBT_add
22:30:10 Containers-Benchmarks: theory Collections.Intf_Map
22:30:10 AWN: theory AWN.OAWN_Invariants
22:30:10 Containers-Benchmarks: theory Collections.Intf_Set
22:30:10 Flow_Networks: theory DFS_Framework.Simple_Impl
22:30:11 CHERI-C_Memory_Model: theory Word_Lib.Boolean_Inequalities
22:30:11 Mersenne_Primes: theory HOL-Number_Theory.Quadratic_Reciprocity
22:30:11 CHERI-C_Memory_Model: theory Word_Lib.Rsplit
22:30:11 CHERI-C_Memory_Model: theory Word_Lib.Typedef_Morphisms
22:30:12 Containers-Benchmarks: theory Collections.BinoPrioImpl
22:30:12 Containers-Benchmarks: theory Collections.PrioByAnnotatedList
22:30:12 Containers-Benchmarks: theory Collections.SkewPrioImpl
22:30:12 Containers-Benchmarks: theory Collections.ListGA
22:30:12 CHERI-C_Memory_Model: theory Word_Lib.Reversed_Bit_Lists
22:30:12 Containers-Benchmarks: theory Collections.PrioUniqueByAnnotatedList
22:30:13 CHERI-C_Memory_Model: theory Word_Lib.Word_Lemmas
22:30:13 AWN: theory AWN.OAWN_Convert
22:30:13 Containers-Benchmarks: theory Collections.Fifo
22:30:14 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
22:30:14 Containers-Benchmarks: theory Collections.FTPrioImpl
22:30:15 Containers-Benchmarks: theory Collections.FTPrioUniqueImpl
22:30:16 CHERI-C_Memory_Model: theory Word_Lib.Word_8
22:30:16 LocalLexing: theory LocalLexing.TheoremD4
22:30:16 Containers-Benchmarks: theory Collections.Algos
22:30:16 Containers-Benchmarks: theory Collections.SetIndex
22:30:16 Containers-Benchmarks: theory Collections.SetIteratorCollectionsGA
22:30:16 Fishers_Inequality: theory Design_Theory.Block_Designs
22:30:16 Containers-Benchmarks: theory Collections.MapGA
22:30:16 Containers-Benchmarks: theory Collections.SetGA
22:30:17 CHERI-C_Memory_Model: theory Word_Lib.Bitwise
22:30:17 CHERI-C_Memory_Model: theory Word_Lib.More_Word_Operations
22:30:17 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Power_Allegories_Multirelations
22:30:17 CHERI-C_Memory_Model: theory Word_Lib.Bitwise_Signed
22:30:19 AWN: theory AWN.OAWN_SOS_Labels
22:30:19 AWN: theory AWN.ONode_Lifting
22:30:19 CHERI-C_Memory_Model: theory Word_Lib.Word_32
22:30:19 Containers-Benchmarks: theory Collections.ArrayMapImpl
22:30:19 Containers-Benchmarks: theory Collections.ListMapImpl
22:30:19 Containers-Benchmarks: theory Collections.ListMapImpl_Invar
22:30:19 Containers-Benchmarks: theory Collections.TrieMapImpl
22:30:19 Containers-Benchmarks: theory Collections.RBTMapImpl
22:30:20 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
22:30:20 CHERI-C_Memory_Model: theory Word_Lib.Word_Lib_Sumo
22:30:22 CHERI-C_Memory_Model: theory CHERI-C_Memory_Model.Preliminary_Library
22:30:22 Fishers_Inequality: theory Design_Theory.BIBD
22:30:22 Containers-Benchmarks: theory Collections.ListSetImpl
22:30:22 Containers-Benchmarks: theory Collections.ListSetImpl_Invar
22:30:22 Containers-Benchmarks: theory Collections.ListSetImpl_NotDist
22:30:23 Containers-Benchmarks: theory Collections.ListSetImpl_Sorted
22:30:23 Timing Schwartz_Zippel (8 threads, 60.321s elapsed time, 299.445s cpu time, 32.819s GC time, factor 4.96)
22:30:23 Finished Schwartz_Zippel (0:01:02 elapsed time, 0:05:03 cpu time, factor 4.86)
22:30:24 Containers-Benchmarks: theory Collections.SetByMap
22:30:25 CHERI-C_Memory_Model: theory CHERI-C_Memory_Model.CHERI_C_Concrete_Memory_Model
22:30:25 Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
22:30:25 AWN: theory AWN.OPnet
22:30:26 Containers-Benchmarks: theory Collections.ArrayHashMap_Impl
22:30:26 Containers-Benchmarks: theory Collections.HashMap_Impl
22:30:27 AWN: theory AWN.OPnet_Lifting
22:30:27 Containers-Benchmarks: theory Collections.HashMap
22:30:27 Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
22:30:28 Running SimplifiedOntologicalArgument (on 10.195.8.40+8) ...
22:30:28 Containers-Benchmarks: theory Collections.ArraySetImpl
22:30:28 Containers-Benchmarks: theory Collections.TrieSetImpl
22:30:28 Containers-Benchmarks: theory Collections.RBTSetImpl
22:30:29 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.HOML
22:30:30 Containers-Benchmarks: theory Collections.ArrayHashMap
22:30:30 Timing Count_Complex_Roots (8 threads, 53.758s elapsed time, 198.727s cpu time, 21.532s GC time, factor 3.70)
22:30:30 Finished Count_Complex_Roots (0:01:07 elapsed time, 0:03:41 cpu time, factor 3.26)
22:30:31 CHERI-C_Memory_Model: theory CHERI-C_Memory_Model.CHERI_C_Global_Environment
22:30:31 Containers-Benchmarks: theory Collections.HashSet
22:30:31 LocalLexing: theory LocalLexing.TheoremD5
22:30:32 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.BaseDefs
22:30:33 Multirelations_Heterogeneous: theory Multirelations_Heterogeneous.Multirelations
22:30:33 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.MFilter
22:30:34 Containers-Benchmarks: theory Collections.ArrayHashSet
22:30:34 Containers-Benchmarks: theory Collections.MapStdImpl
22:30:34 Chandy_Lamport: theory Chandy_Lamport.Swap
22:30:36 AWN: theory AWN.OClosed_Lifting
22:30:36 Containers-Benchmarks: theory Collections.SetStdImpl
22:30:37 Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
22:30:37 Containers-Benchmarks: theory Collections.ICF_Impl
22:30:37 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
22:30:38 Flow_Networks: theory DFS_Framework.Restr_Impl
22:30:38 Containers-Benchmarks: theory Collections.ICF_Refine_Monadic
22:30:39 AWN: theory AWN.OClosed_Transfer
22:30:39 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.KanckosLethenNo2Possibilist
22:30:39 Mersenne_Primes: theory HOL-Number_Theory.Pocklington
22:30:40 LocalLexing: theory LocalLexing.TheoremD6
22:30:44 Flow_Networks: theory DFS_Framework.DFS_Framework
22:30:45 Flow_Networks: theory DFS_Framework.Reachable_Nodes
22:30:46 LocalLexing: theory LocalLexing.TheoremD7
22:30:47 Fishers_Inequality: theory Design_Theory.Sub_Designs
22:30:48 LocalLexing: theory LocalLexing.TheoremD8
22:30:48 LocalLexing: theory LocalLexing.TheoremD9
22:30:49 Mersenne_Primes: theory HOL-Number_Theory.Residue_Primitive_Roots
22:30:52 Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
22:30:52 LocalLexing: theory LocalLexing.Ladder
22:30:52 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.ScottVariant
22:30:52 Building Incompleteness (on of1-proof+0-7) ...
22:30:53 AWN: theory AWN.AWN_Main
22:30:53 AWN: theory AWN.Qmsg_Lifting
22:30:53 Incompleteness: theory FinFun.FinFun
22:30:54 Running CAVA_LTL_Modelchecker (on of4.proof.cit.tum.de+0-3) ...
22:30:54 Incompleteness: theory Nominal2.Nominal2_Base
22:30:55 Mersenne_Primes: theory HOL-Number_Theory.Number_Theory
22:30:56 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
22:30:57 Mersenne_Primes: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
22:30:57 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
22:30:57 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
22:30:57 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
22:30:57 Incompleteness: theory Nominal2.Nominal2_Abs
22:30:58 AWN: theory AWN.Toy
22:30:59 Incompleteness: theory Nominal2.Nominal2_FCB
22:31:00 Incompleteness: theory Nominal2.Nominal2
22:31:01 Mersenne_Primes: theory Probabilistic_Prime_Tests.Legendre_Symbol
22:31:03 Incompleteness: theory Incompleteness.SyntaxN
22:31:05 Fishers_Inequality: theory Polynomials.More_Modules
22:31:06 Containers-Benchmarks: theory Collections.ICF_Autoref
22:31:07 Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
22:31:08 Containers-Benchmarks: theory Collections.Collections
22:31:08 Containers-Benchmarks: theory Collections.CollectionsV1
22:31:09 Mersenne_Primes: theory Probabilistic_Prime_Tests.Jacobi_Symbol
22:31:09 Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
22:31:09 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_ICF
22:31:09 Incompleteness: theory Incompleteness.Coding
22:31:09 Incompleteness: theory Incompleteness.Predicates
22:31:12 Fishers_Inequality: theory Fishers_Inequality.Design_Extras
22:31:12 Timing Quantales_Converse (8 threads, 139.225s elapsed time, 244.265s cpu time, 19.756s GC time, factor 1.75)
22:31:12 Finished Quantales_Converse (0:02:30 elapsed time, 0:04:23 cpu time, factor 1.75)
22:31:12 Incompleteness: theory Incompleteness.Sigma
22:31:17 Fishers_Inequality: theory List-Index.List_Index
22:31:17 Timing Containers-Benchmarks (8 threads, 107.382s elapsed time, 346.201s cpu time, 122.785s GC time, factor 3.22)
22:31:17 Finished Containers-Benchmarks (0:01:50 elapsed time, 0:05:52 cpu time, factor 3.19)
22:31:17 Incompleteness: theory Incompleteness.Coding_Predicates
22:31:21 Building Formula_Derivatives (on of2.proof.cit.tum.de+8-11) ...
22:31:21 Incompleteness: theory Incompleteness.Functions
22:31:21 Incompleteness: theory Incompleteness.Pf_Predicates
22:31:22 Fishers_Inequality: theory Open_Induction.Restricted_Predicates
22:31:22 Chandy_Lamport: theory Chandy_Lamport.Trace
22:31:22 Formula_Derivatives: theory Formula_Derivatives.FSet_More
22:31:22 Formula_Derivatives: theory Formula_Derivatives.While_Default
22:31:22 Incompleteness: theory Incompleteness.Goedel_I
22:31:22 Incompleteness: theory Incompleteness.II_Prelims
22:31:23 Formula_Derivatives: theory Coinductive_Languages.Coinductive_Language
22:31:23 Formula_Derivatives: theory Deriving.Derive_Manager
22:31:23 Formula_Derivatives: theory Deriving.Comparator
22:31:23 Formula_Derivatives: theory Deriving.Generator_Aux
22:31:23 Formula_Derivatives: theory List-Index.List_Index
22:31:23 Incompleteness: theory Incompleteness.Pseudo_Coding
22:31:23 Incompleteness: theory Incompleteness.Quote
22:31:23 Incompleteness: theory Incompleteness.Goedel_II
22:31:24 Formula_Derivatives: theory Deriving.Compare
22:31:24 Formula_Derivatives: theory Deriving.Comparator_Generator
22:31:25 Formula_Derivatives: theory Deriving.Compare_Generator
22:31:25 Formula_Derivatives: theory Formula_Derivatives.Automaton
22:31:25 Formula_Derivatives: theory Deriving.Compare_Instances
22:31:25 Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
22:31:25 Formula_Derivatives: theory Formula_Derivatives.Abstract_Formula
22:31:26 Formula_Derivatives: theory Formula_Derivatives.WS1S_Prelim
22:31:29 LocalLexing: theory LocalLexing.TheoremD10
22:31:30 Chandy_Lamport: theory Chandy_Lamport.Util
22:31:33 LocalLexing: theory LocalLexing.TheoremD11
22:31:35 AWN: theory AWN.AWN_Term_Graph
22:31:36 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Auxiliary
22:31:36 Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
22:31:37 LocalLexing: theory LocalLexing.TheoremD12
22:31:39 CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping
22:31:39 CAVA_LTL_Modelchecker: theory LTL.Rewriting
22:31:39 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
22:31:39 Flow_Networks: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
22:31:40 Chandy_Lamport: theory Chandy_Lamport.Snapshot
22:31:40 LocalLexing: theory LocalLexing.TheoremD13
22:31:41 LocalLexing: theory LocalLexing.TheoremD14
22:31:41 Timing CHERI-C_Memory_Model (8 threads, 92.020s elapsed time, 308.861s cpu time, 27.035s GC time, factor 3.36)
22:31:41 Finished CHERI-C_Memory_Model (0:01:35 elapsed time, 0:05:15 cpu time, factor 3.30)
22:31:41 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
22:31:41 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
22:31:41 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
22:31:41 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
22:31:42 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
22:31:42 Flow_Networks: theory Flow_Networks.Fofu_Impl_Base
22:31:42 Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
22:31:44 Timing AWN (1 threads, 158.323s elapsed time, 158.281s cpu time, 11.339s GC time, factor 1.00)
22:31:44 Finished AWN (0:02:42 elapsed time, 0:02:41 cpu time, factor 1.00)
22:31:45 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
22:31:46 Flow_Networks: theory Flow_Networks.Refine_Add_Fofu
22:31:47 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
22:31:48 Mersenne_Primes: theory Pell.Pell
22:31:48 Flow_Networks: theory Flow_Networks.Network
22:31:50 LocalLexing: theory LocalLexing.PathLemmas
22:31:50 Flow_Networks: theory Flow_Networks.Residual_Graph
22:31:51 LocalLexing: theory LocalLexing.MainTheorems
22:31:53 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
22:31:53 Formula_Derivatives: theory Formula_Derivatives.Presburger_Formula
22:31:53 Formula_Derivatives: theory Formula_Derivatives.WS1S_Alt_Formula
22:31:53 Formula_Derivatives: theory Formula_Derivatives.WS1S_Formula
22:31:56 Flow_Networks: theory Flow_Networks.Augmenting_Flow
22:31:57 Flow_Networks: theory Flow_Networks.Augmenting_Path
22:31:58 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer
22:31:58 Timing LocalLexing (1 threads, 150.403s elapsed time, 150.394s cpu time, 9.286s GC time, factor 1.00)
22:31:58 Finished LocalLexing (0:02:33 elapsed time, 0:02:32 cpu time, factor 1.00)
22:32:00 Flow_Networks: theory Flow_Networks.Ford_Fulkerson
22:32:02 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
22:32:02 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
22:32:03 Flow_Networks: theory Flow_Networks.Graph_Impl
22:32:04 Flow_Networks: theory Flow_Networks.NetCheck
22:32:06 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimpleVariant
22:32:09 Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
22:32:10 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
22:32:14 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimpleVariantHF
22:32:15 Timing Multirelations (1 threads, 174.043s elapsed time, 129.395s cpu time, 10.988s GC time, factor 0.74)
22:32:15 Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
22:32:15 Finished Multirelations (0:02:56 elapsed time, 0:02:11 cpu time, factor 0.75)
22:32:15 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
22:32:16 Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
22:32:17 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
22:32:17 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
22:32:18 Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
22:32:19 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimpleVariantPG
22:32:20 Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:32:21 Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
22:32:22 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimpleVariantSE
22:32:22 Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
22:32:23 Fishers_Inequality: theory Polynomials.Utils
22:32:23 Mersenne_Primes: theory Native_Word.Code_Int_Integer_Conversion
22:32:23 Mersenne_Primes: theory Word_Lib.More_Arithmetic
22:32:23 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimpleVariantSEinT
22:32:24 Mersenne_Primes: theory Word_Lib.More_Bit_Ring
22:32:24 Fishers_Inequality: theory Groebner_Bases.General
22:32:24 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.SimplifiedOntologicalArgument
22:32:26 Mersenne_Primes: theory Word_Lib.More_Word
22:32:27 SimplifiedOntologicalArgument: theory SimplifiedOntologicalArgument.UFilterVariant
22:32:28 Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
22:32:31 Timing SimplifiedOntologicalArgument (1 threads, 120.872s elapsed time, 101.337s cpu time, 3.080s GC time, factor 0.84)
22:32:31 Finished SimplifiedOntologicalArgument (0:02:02 elapsed time, 0:01:42 cpu time, factor 0.84)
22:32:32 Fishers_Inequality: theory Polynomials.Power_Products
22:32:41 Formula_Derivatives: theory Formula_Derivatives.WS1S_Nameful
22:32:41 Formula_Derivatives: theory Formula_Derivatives.WS1S_Presburger_Equivalence
22:32:41 Mersenne_Primes: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:32:43 Mersenne_Primes: theory Word_Lib.Least_significant_bit
22:32:44 Mersenne_Primes: theory Word_Lib.Most_significant_bit
22:32:45 Mersenne_Primes: theory Word_Lib.Generic_set_bit
22:32:46 Mersenne_Primes: theory Native_Word.Code_Target_Integer_Bit
22:32:49 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mulog
22:32:51 Fishers_Inequality: theory Polynomials.MPoly_Type_Class
22:32:59 Mersenne_Primes: theory Native_Word.Code_Target_Int_Bit
22:32:59 Mersenne_Primes: theory Mersenne_Primes.Lucas_Lehmer_Code
22:33:00 Estimated 0:48:37 build time with default build heuristic (took 78.746s)
22:33:02 Building HOLCF-Library (on of4.proof.cit.tum.de+4-11) ...
22:33:02 Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
22:33:02 HOLCF-Library: theory HOL-Library.Infinite_Set
22:33:02 HOLCF-Library: theory HOLCF-Library.Bool_Discrete
22:33:02 HOLCF-Library: theory HOLCF-Library.Char_Discrete
22:33:02 HOLCF-Library: theory HOLCF-Library.Int_Discrete
22:33:03 HOLCF-Library: theory HOLCF-Library.Nat_Discrete
22:33:03 HOLCF-Library: theory HOLCF-Library.List_Cpo
22:33:03 HOLCF-Library: theory HOLCF-Library.Sum_Cpo
22:33:03 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
22:33:03 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
22:33:03 HOLCF-Library: theory HOL-Library.Countable_Set
22:33:03 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite
22:33:03 HOLCF-Library: theory HOLCF-Library.List_Predomain
22:33:03 HOLCF-Library: theory HOLCF-Library.Option_Cpo
22:33:03 HOLCF-Library: theory HOL-Library.Countable_Complete_Lattices
22:33:03 HOLCF-Library: theory HOLCF-Library.HOL_Cpo
22:33:04 Building HOL-IMP (on of2.proof.cit.tum.de+0-7) ...
22:33:05 HOLCF-Library: theory HOL-Library.Order_Continuity
22:33:05 HOLCF-Library: theory HOL-Library.Extended_Nat
22:33:05 HOL-IMP: theory HOL-IMP.AExp
22:33:05 HOL-IMP: theory HOL-IMP.C_like
22:33:05 HOL-IMP: theory HOL-IMP.Complete_Lattice
22:33:05 HOL-IMP: theory HOL-IMP.OO
22:33:05 HOL-IMP: theory HOL-IMP.Star
22:33:05 HOL-IMP: theory HOL-IMP.Types
22:33:05 HOLCF-Library: theory HOLCF-Library.Stream
22:33:06 HOLCF-Library: theory HOLCF-Library.HOLCF_Library
22:33:06 HOL-IMP: theory HOL-IMP.ASM
22:33:06 HOL-IMP: theory HOL-IMP.BExp
22:33:07 Timing CAVA_LTL_Modelchecker (8 threads, 129.224s elapsed time, 190.114s cpu time, 17.970s GC time, factor 1.47)
22:33:07 Finished CAVA_LTL_Modelchecker (0:02:11 elapsed time, 0:03:13 cpu time, factor 1.47)
22:33:07 HOL-IMP: theory HOL-IMP.Com
22:33:07 HOL-IMP: theory HOL-IMP.Procs
22:33:08 HOL-IMP: theory HOL-IMP.ACom
22:33:08 HOL-IMP: theory HOL-IMP.Abs_Int_Tests
22:33:08 HOL-IMP: theory HOL-IMP.Big_Step
22:33:08 HOL-IMP: theory HOL-IMP.Vars
22:33:08 HOL-IMP: theory HOL-IMP.Denotational
22:33:08 HOL-IMP: theory HOL-IMP.Hoare
22:33:08 HOL-IMP: theory HOL-IMP.Sec_Type_Expr
22:33:08 HOL-IMP: theory HOL-IMP.Sem_Equiv
22:33:08 HOL-IMP: theory HOL-IMP.Def_Init
22:33:08 HOL-IMP: theory HOL-IMP.Hoare_Examples
22:33:08 HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete
22:33:09 HOL-IMP: theory HOL-IMP.Hoare_Total_EX
22:33:09 HOL-IMP: theory HOL-IMP.Hoare_Total_EX2
22:33:09 HOL-IMP: theory HOL-IMP.VCG
22:33:09 HOL-IMP: theory HOL-IMP.Hoare_Total
22:33:09 HOL-IMP: theory HOL-IMP.Def_Init_Exp
22:33:09 HOL-IMP: theory HOL-IMP.Sec_Typing
22:33:09 HOL-IMP: theory HOL-IMP.Sec_TypingT
22:33:09 HOL-IMP: theory HOL-IMP.Def_Init_Big
22:33:09 HOL-IMP: theory HOL-IMP.VCG_Total_EX
22:33:09 HOL-IMP: theory HOL-IMP.VCG_Total_EX2
22:33:09 HOL-IMP: theory HOL-IMP.Fold
22:33:09 HOL-IMP: theory HOL-IMP.Live
22:33:09 HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn
22:33:09 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn
22:33:09 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat
22:33:10 HOL-IMP: theory HOL-IMP.Compiler
22:33:10 HOL-IMP: theory HOL-IMP.Def_Init_Small
22:33:10 HOL-IMP: theory HOL-IMP.Small_Step
22:33:10 HOL-IMP: theory HOL-IMP.Live_True
22:33:10 HOL-IMP: theory HOL-IMP.Poly_Types
22:33:10 HOL-IMP: theory HOL-IMP.Collecting
22:33:10 HOL-IMP: theory HOL-IMP.Finite_Reachable
22:33:11 HOL-IMP: theory HOL-IMP.Collecting1
22:33:11 HOL-IMP: theory HOL-IMP.Collecting_Examples
22:33:11 HOL-IMP: theory HOL-IMP.Abs_Int_init
22:33:11 HOL-IMP: theory HOL-IMP.Abs_Int0
22:33:12 HOL-IMP: theory HOL-IMP.Compiler2
22:33:12 HOL-IMP: theory HOL-IMP.Abs_State
22:33:13 HOL-IMP: theory HOL-IMP.Abs_Int1
22:33:13 HOL-IMP: theory HOL-IMP.Abs_Int1_const
22:33:13 HOL-IMP: theory HOL-IMP.Abs_Int1_parity
22:33:13 HOL-IMP: theory HOL-IMP.Abs_Int2
22:33:14 HOL-IMP: theory HOL-IMP.Abs_Int2_ivl
22:33:16 HOL-IMP: theory HOL-IMP.Abs_Int3
22:33:17 Running Groebner_Macaulay (on 10.195.8.29+0-7) ...
22:33:17 Timing HOLCF-Library (8 threads, 4.467s elapsed time, 17.085s cpu time, 1.259s GC time, factor 3.82)
22:33:17 Finished HOLCF-Library (0:00:10 elapsed time, 0:00:28 cpu time, factor 2.60)
22:33:19 Timing Mersenne_Primes (1 threads, 235.096s elapsed time, 224.693s cpu time, 8.513s GC time, factor 0.96)
22:33:19 Finished Mersenne_Primes (0:03:59 elapsed time, 0:03:48 cpu time, factor 0.96)
22:33:20 Groebner_Macaulay: theory Groebner_Macaulay.Binomial_Int
22:33:22 Groebner_Macaulay: theory Groebner_Macaulay.Poly_Fun
22:33:23 Running Decreasing-Diagrams (on 10.195.8.49+0-7) ...
22:33:23 Groebner_Macaulay: theory Groebner_Macaulay.Dube_Prelims
22:33:24 Running Signature_Groebner (on of1.proof.cit.tum.de+0-7) ...
22:33:25 Groebner_Macaulay: theory Groebner_Macaulay.Monomial_Module
22:33:25 Decreasing-Diagrams: theory Decreasing-Diagrams.Decreasing_Diagrams
22:33:26 Signature_Groebner: theory Signature_Groebner.Prelims
22:33:26 Signature_Groebner: theory Signature_Groebner.More_MPoly
22:33:27 Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
22:33:27 Signature_Groebner: theory Signature_Groebner.Signature_Groebner
22:33:27 Timing Multirelations_Heterogeneous (1 threads, 239.439s elapsed time, 217.076s cpu time, 15.030s GC time, factor 0.91)
22:33:27 Finished Multirelations_Heterogeneous (0:04:02 elapsed time, 0:03:39 cpu time, factor 0.91)
22:33:30 Groebner_Macaulay: theory Groebner_Macaulay.Degree_Bound_Utils
22:33:30 Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
22:33:31 Timing Incompleteness (8 threads, 142.155s elapsed time, 552.295s cpu time, 29.312s GC time, factor 3.89)
22:33:31 Finished Incompleteness (0:02:37 elapsed time, 0:09:44 cpu time, factor 3.70)
22:33:34 Groebner_Macaulay: theory Groebner_Macaulay.Degree_Section
22:33:36 Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay
22:33:37 Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
22:33:37 Building HOL-Combinatorics (on of3.proof.cit.tum.de+8-15) ...
22:33:38 Flow_Networks: theory Flow_Networks.Network_Impl
22:33:38 HOL-Combinatorics: theory HOL-Combinatorics.Stirling
22:33:38 HOL-Combinatorics: theory HOL-Combinatorics.Transposition
22:33:38 HOL-Combinatorics: theory HOL-Library.Cancellation
22:33:38 HOL-Combinatorics: theory HOL-Library.FuncSet
22:33:38 HOL-Combinatorics: theory HOL-Combinatorics.Perm
22:33:38 HOL-Combinatorics: theory HOL-Library.Disjoint_Sets
22:33:38 HOL-Combinatorics: theory HOL-Library.Multiset
22:33:39 Signature_Groebner: theory Signature_Groebner.Signature_Examples
22:33:40 Running Automated_Stateful_Protocol_Verification (on 10.195.7.194+0-7) ...
22:33:40 Groebner_Macaulay: theory Groebner_Macaulay.Hilbert_Function
22:33:42 HOL-Combinatorics: theory HOL-Combinatorics.Permutations
22:33:42 HOL-Combinatorics: theory HOL-Combinatorics.Cycles
22:33:42 HOL-Combinatorics: theory HOL-Combinatorics.List_Permutation
22:33:43 HOL-Combinatorics: theory HOL-Combinatorics.Orbits
22:33:43 HOL-Combinatorics: theory HOL-Combinatorics.Multiset_Permutations
22:33:43 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
22:33:43 HOL-Combinatorics: theory HOL-Combinatorics.Combinatorics
22:33:44 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
22:33:44 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
22:33:44 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
22:33:45 Running HOL-ODE-Examples (on 10.195.8.40+0-7) ...
22:33:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
22:33:46 Groebner_Macaulay: theory Groebner_Macaulay.Cone_Decomposition
22:33:46 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
22:33:47 Running IEEE_Floating_Point (on 10.195.8.11+0-7) ...
22:33:47 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
22:33:49 IEEE_Floating_Point: theory HOL-Library.Adhoc_Overloading
22:33:49 IEEE_Floating_Point: theory HOL-Library.Monad_Syntax
22:33:49 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
22:33:49 IEEE_Floating_Point: theory HOL-Library.Code_Abstract_Nat
22:33:50 IEEE_Floating_Point: theory HOL-Library.Code_Target_Nat
22:33:50 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
22:33:50 IEEE_Floating_Point: theory HOL-Library.Code_Target_Int
22:33:50 Timing HOL-Combinatorics (8 threads, 6.224s elapsed time, 34.425s cpu time, 2.863s GC time, factor 5.53)
22:33:50 Finished HOL-Combinatorics (0:00:12 elapsed time, 0:00:45 cpu time, factor 3.53)
22:33:51 IEEE_Floating_Point: theory HOL-Library.Code_Target_Numeral
22:33:51 Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
22:33:51 IEEE_Floating_Point: theory HOL-Library.Lattice_Algebras
22:33:53 Running DOM_Components (on 10.195.8.42+0-7) ...
22:33:58 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
22:33:58 DOM_Components: theory DOM_Components.Core_DOM_Components
22:33:58 Running HOL-ODE-ARCH-COMP (on 10.195.8.46+0-7) ...
22:33:59 Timing Signature_Groebner (8 threads, 32.482s elapsed time, 73.603s cpu time, 13.046s GC time, factor 2.27)
22:33:59 Finished Signature_Groebner (0:00:35 elapsed time, 0:01:18 cpu time, factor 2.23)
22:34:00 Timing Decreasing-Diagrams (1 threads, 34.509s elapsed time, 37.623s cpu time, 3.815s GC time, factor 1.09)
22:34:00 Finished Decreasing-Diagrams (0:00:37 elapsed time, 0:00:40 cpu time, factor 1.09)
22:34:01 IEEE_Floating_Point: theory HOL-Library.Log_Nat
22:34:02 IEEE_Floating_Point: theory HOL-Library.Float
22:34:02 HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
22:34:04 Building LLL_Basis_Reduction (on of4.proof.cit.tum.de+4-11) ...
22:34:07 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
22:34:07 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
22:34:07 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
22:34:07 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
22:34:08 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
22:34:09 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
22:34:10 Chandy_Lamport: theory Chandy_Lamport.Example
22:34:13 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
22:34:15 Groebner_Macaulay: theory Groebner_Macaulay.Dube_Bound
22:34:17 Chandy_Lamport: theory Chandy_Lamport.Co_Snapshot
22:34:19 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE
22:34:20 Running Pratt_Certificate (on 10.195.8.49+0-7) ...
22:34:21 Building HOL-Imperative_HOL (on of1.proof.cit.tum.de+8-15) ...
22:34:22 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Adhoc_Overloading
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Code_Abstract_Nat
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Cancellation
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Int
22:34:22 HOL-Imperative_HOL: theory HOL-Library.LaTeXsugar
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Nat_Bijection
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Old_Datatype
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Nat
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Monad_Syntax
22:34:22 HOL-Imperative_HOL: theory HOL-Library.RBT_Impl
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Numeral
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Countable
22:34:22 HOL-Imperative_HOL: theory HOL-Library.Multiset
22:34:22 Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
22:34:23 Pratt_Certificate: theory Lehmer.Lehmer
22:34:23 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Properties
22:34:23 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap
22:34:24 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
22:34:26 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
22:34:26 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
22:34:26 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview
22:34:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray
22:34:27 Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
22:34:27 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort
22:34:27 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse
22:34:27 Timing Chandy_Lamport (1 threads, 272.829s elapsed time, 272.271s cpu time, 18.904s GC time, factor 1.00)
22:34:27 Finished Chandy_Lamport (0:04:37 elapsed time, 0:04:36 cpu time, factor 1.00)
22:34:30 Timing Flow_Networks (1 threads, 435.647s elapsed time, 475.991s cpu time, 102.140s GC time, factor 1.09)
22:34:30 Finished Flow_Networks (0:07:59 elapsed time, 0:08:57 cpu time, factor 1.12)
22:34:33 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
22:34:33 Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
22:34:34 Building HOL-SPARK (on of3.proof.cit.tum.de+0-7) ...
22:34:35 HOL-SPARK: theory HOL-Library.Phantom_Type
22:34:36 HOL-SPARK: theory HOL-Library.Cardinality
22:34:36 HOL-SPARK: theory HOL-Library.Numeral_Type
22:34:36 HOL-SPARK: theory HOL-Library.Type_Length
22:34:37 HOL-SPARK: theory HOL-Library.Word
22:34:37 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
22:34:39 Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay_Examples
22:34:41 Running Simple_Clause_Learning (on of1-proof+0-7) ...
22:34:42 HOL-SPARK: theory HOL-SPARK.SPARK_Setup
22:34:42 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
22:34:42 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
22:34:42 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
22:34:42 Simple_Clause_Learning: theory Deriving.Comparator
22:34:42 Simple_Clause_Learning: theory Deriving.Derive_Manager
22:34:42 Simple_Clause_Learning: theory Deriving.Generator_Aux
22:34:42 Simple_Clause_Learning: theory Simple_Clause_Learning.Multiset_Order_Extra
22:34:42 Simple_Clause_Learning: theory HOL-Cardinals.Order_Union
22:34:42 Simple_Clause_Learning: theory Word_Lib.More_Divides
22:34:42 Simple_Clause_Learning: theory Word_Lib.Bit_Comprehension
22:34:42 Simple_Clause_Learning: theory Word_Lib.Signed_Division_Word
22:34:42 Simple_Clause_Learning: theory Nested_Multisets_Ordinals.Multiset_More
22:34:42 Simple_Clause_Learning: theory Deriving.Countable_Generator
22:34:42 Simple_Clause_Learning: theory Deriving.Equality_Generator
22:34:42 Simple_Clause_Learning: theory HOL-Cardinals.Wellorder_Extension
22:34:42 Simple_Clause_Learning: theory Coinductive.Coinductive_Nat
22:34:42 Simple_Clause_Learning: theory List-Index.List_Index
22:34:42 Simple_Clause_Learning: theory Matrix.Utility
22:34:42 HOL-SPARK: theory HOL-SPARK.SPARK
22:34:42 Simple_Clause_Learning: theory Native_Word.Code_Int_Integer_Conversion
22:34:42 Simple_Clause_Learning: theory Open_Induction.Restricted_Predicates
22:34:43 Simple_Clause_Learning: theory Deriving.Equality_Instances
22:34:43 Simple_Clause_Learning: theory Polynomial_Factorization.Missing_List
22:34:43 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Map2
22:34:43 Simple_Clause_Learning: theory Knuth_Bendix_Order.Order_Pair
22:34:43 Simple_Clause_Learning: theory Simple_Clause_Learning.Abstract_Renaming_Apart
22:34:43 Simple_Clause_Learning: theory Simple_Clause_Learning.Trail_Induced_Ordering
22:34:43 Simple_Clause_Learning: theory Deriving.Compare
22:34:43 Simple_Clause_Learning: theory Deriving.Comparator_Generator
22:34:43 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
22:34:43 Simple_Clause_Learning: theory Knuth_Bendix_Order.Lexicographic_Extension
22:34:43 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Clausal_Logic
22:34:43 Simple_Clause_Learning: theory Word_Lib.More_Arithmetic
22:34:43 Simple_Clause_Learning: theory Word_Lib.More_Bit_Ring
22:34:43 Simple_Clause_Learning: theory Coinductive.Coinductive_List
22:34:44 Simple_Clause_Learning: theory Deriving.Compare_Generator
22:34:44 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Herbrand_Interpretation
22:34:44 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Abstract_Substitution
22:34:44 Simple_Clause_Learning: theory Word_Lib.More_Word
22:34:44 Simple_Clause_Learning: theory Deriving.Compare_Instances
22:34:44 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Ground_Resolution_Model
22:34:44 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Inference_System
22:34:45 IEEE_Floating_Point: theory IEEE_Floating_Point.Conversion_IEEE_Float
22:34:45 Simple_Clause_Learning: theory Knuth_Bendix_Order.KBO
22:34:45 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
22:34:46 Simple_Clause_Learning: theory Native_Word.Code_Target_Word_Base
22:34:46 Simple_Clause_Learning: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:34:46 Simple_Clause_Learning: theory Word_Lib.Least_significant_bit
22:34:47 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate_Code
22:34:47 Simple_Clause_Learning: theory Word_Lib.Most_significant_bit
22:34:47 Simple_Clause_Learning: theory Word_Lib.Generic_set_bit
22:34:47 Simple_Clause_Learning: theory Native_Word.Code_Target_Integer_Bit
22:34:47 Simple_Clause_Learning: theory Native_Word.Word_Type_Copies
22:34:48 Simple_Clause_Learning: theory Simple_Clause_Learning.Ordered_Resolution_Prover_Extra
22:34:49 Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
22:34:49 Timing Pratt_Certificate (1 threads, 26.070s elapsed time, 27.163s cpu time, 1.662s GC time, factor 1.04)
22:34:49 Finished Pratt_Certificate (0:00:28 elapsed time, 0:00:29 cpu time, factor 1.05)
22:34:49 Timing HOL-SPARK (8 threads, 7.699s elapsed time, 28.653s cpu time, 2.533s GC time, factor 3.72)
22:34:49 Finished HOL-SPARK (0:00:13 elapsed time, 0:00:39 cpu time, factor 2.89)
22:34:49 Timing HOL-IMP (8 threads, 89.406s elapsed time, 243.586s cpu time, 25.436s GC time, factor 2.72)
22:34:49 Finished HOL-IMP (0:01:44 elapsed time, 0:04:36 cpu time, factor 2.64)
22:34:49 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Liminf
22:34:49 Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Chain
22:34:51 IEEE_Floating_Point: theory IEEE_Floating_Point.Double
22:34:52 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker
22:34:53 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
22:34:54 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN
22:34:55 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
22:34:55 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
22:34:56 Simple_Clause_Learning: theory Saturation_Framework.Calculus
22:34:56 Simple_Clause_Learning: theory Simple_Clause_Learning.Wellfounded_Extra
22:34:57 Simple_Clause_Learning: theory Native_Word.Uint32
22:34:57 Running Implicational_Logic (on 10.195.8.30+0-7) ...
22:34:57 Simple_Clause_Learning: theory Saturation_Framework_Extensions.Soundness
22:34:57 Simple_Clause_Learning: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
22:34:58 Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
22:34:58 Simple_Clause_Learning: theory Saturation_Framework_Extensions.Clausal_Calculus
22:34:58 Simple_Clause_Learning: theory Collections.HashCode
22:34:59 Implicational_Logic: theory Implicational_Logic.Implicational_Logic
22:34:59 Simple_Clause_Learning: theory Deriving.Hash_Generator
22:34:59 Simple_Clause_Learning: theory Simple_Clause_Learning.SCL_FOL
22:34:59 Simple_Clause_Learning: theory Deriving.Hash_Instances
22:34:59 Simple_Clause_Learning: theory Deriving.Derive
22:35:00 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex
22:35:00 IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN_SMTLIB
22:35:00 IEEE_Floating_Point: theory IEEE_Floating_Point.FP64
22:35:00 Simple_Clause_Learning: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
22:35:02 Implicational_Logic: theory Implicational_Logic.Implicational_Logic_Appendix
22:35:03 Timing IEEE_Floating_Point (1 threads, 73.206s elapsed time, 78.575s cpu time, 6.285s GC time, factor 1.07)
22:35:03 Finished IEEE_Floating_Point (0:01:15 elapsed time, 0:01:20 cpu time, factor 1.08)
22:35:05 Timing Implicational_Logic (1 threads, 5.567s elapsed time, 6.167s cpu time, 0.548s GC time, factor 1.11)
22:35:05 Finished Implicational_Logic (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.12)
22:35:05 Timing Fishers_Inequality (1 threads, 343.313s elapsed time, 336.095s cpu time, 22.507s GC time, factor 0.98)
22:35:05 Finished Fishers_Inequality (0:05:49 elapsed time, 0:05:41 cpu time, factor 0.98)
22:35:08 Simple_Clause_Learning: theory Simple_Clause_Learning.Correct_Termination
22:35:08 Simple_Clause_Learning: theory Simple_Clause_Learning.Initial_Literals_Generalize_Learned_Literals
22:35:08 Simple_Clause_Learning: theory Simple_Clause_Learning.Invariants
22:35:08 Simple_Clause_Learning: theory Simple_Clause_Learning.Non_Redundancy
22:35:10 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
22:35:10 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
22:35:10 Timing Formula_Derivatives (8 threads, 213.271s elapsed time, 625.391s cpu time, 362.767s GC time, factor 2.93)
22:35:10 Finished Formula_Derivatives (0:03:48 elapsed time, 0:10:52 cpu time, factor 2.86)
22:35:11 Simple_Clause_Learning: theory Simple_Clause_Learning.Termination
22:35:12 Running Lehmer (on of3.proof.cit.tum.de+8-15) ...
22:35:12 Simple_Clause_Learning: theory Simple_Clause_Learning.Completeness
22:35:14 Lehmer: theory Lehmer.Lehmer
22:35:15 Timing Lehmer (8 threads, 0.677s elapsed time, 1.352s cpu time, 0.031s GC time, factor 2.00)
22:35:15 Finished Lehmer (0:00:02 elapsed time, 0:00:03 cpu time)
22:35:16 LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
22:35:27 Timing HOL-Imperative_HOL (8 threads, 48.253s elapsed time, 242.379s cpu time, 23.745s GC time, factor 5.02)
22:35:27 Finished HOL-Imperative_HOL (0:01:05 elapsed time, 0:04:37 cpu time, factor 4.27)
22:35:33 Timing LLL_Basis_Reduction (8 threads, 71.787s elapsed time, 232.516s cpu time, 51.141s GC time, factor 3.24)
22:35:33 Finished LLL_Basis_Reduction (0:01:28 elapsed time, 0:04:22 cpu time, factor 2.98)
22:35:36 Running Koenigsberg_Friendship (on 10.195.8.30+0-7) ...
22:35:38 Running Sort_Encodings (on 10.195.8.49+0-7) ...
22:35:39 Sort_Encodings: theory HOL-Library.Infinite_Set
22:35:39 Koenigsberg_Friendship: theory Dijkstra_Shortest_Path.Graph
22:35:41 Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph
22:35:43 Sort_Encodings: theory HOL-Library.Nat_Bijection
22:35:44 Sort_Encodings: theory HOL-Library.Old_Datatype
22:35:45 Sort_Encodings: theory HOL-Library.Countable
22:35:47 Sort_Encodings: theory HOL-Library.Countable_Set
22:35:50 Sort_Encodings: theory HOL-Library.Countable_Set_Type
22:35:50 Building HOL-SPARK-Examples (on of3.proof.cit.tum.de+0-7) ...
22:35:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor
22:35:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD
22:35:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence
22:35:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt
22:35:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R
22:35:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L
22:35:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R
22:35:53 Sort_Encodings: theory Sort_Encodings.Preliminaries
22:35:57 Sort_Encodings: theory Sort_Encodings.Sig
22:35:57 Running Nullstellensatz (on 10.195.8.11+0-7) ...
22:35:59 Running Complx (on 10.195.6.179+0-7) ...
22:36:00 Sort_Encodings: theory Sort_Encodings.TermsAndClauses
22:36:01 Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
22:36:01 Complx: theory Complx.Cache_Tactics
22:36:01 Complx: theory Complx.Language
22:36:02 Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
22:36:02 Timing HOL-SPARK-Examples (8 threads, 4.005s elapsed time, 16.096s cpu time, 1.025s GC time, factor 4.02)
22:36:02 Finished HOL-SPARK-Examples (0:00:10 elapsed time, 0:00:26 cpu time, factor 2.56)
22:36:03 Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
22:36:03 Nullstellensatz: theory Nullstellensatz.Univariate_PM
22:36:03 Sort_Encodings: theory Sort_Encodings.M
22:36:05 Nullstellensatz: theory Nullstellensatz.Nullstellensatz
22:36:09 Complx: theory Complx.SmallStep
22:36:09 Sort_Encodings: theory Sort_Encodings.CM
22:36:11 Sort_Encodings: theory Sort_Encodings.Mono
22:36:14 Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
22:36:18 Sort_Encodings: theory Sort_Encodings.Mcalc
22:36:19 Timing Nullstellensatz (1 threads, 17.631s elapsed time, 19.761s cpu time, 1.976s GC time, factor 1.12)
22:36:19 Finished Nullstellensatz (0:00:21 elapsed time, 0:00:23 cpu time, factor 1.11)
22:36:20 Complx: theory Complx.OG_Annotations
22:36:21 Sort_Encodings: theory Sort_Encodings.T_G_Prelim
22:36:22 Sort_Encodings: theory Sort_Encodings.T
22:36:23 Complx: theory Complx.OG_Hoare
22:36:26 Complx: theory Complx.SeqCatch_decomp
22:36:30 Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory
22:36:33 DOM_Components: theory DOM_Components.Shadow_DOM_Components
22:36:36 Sort_Encodings: theory Sort_Encodings.Mcalc2
22:36:38 Sort_Encodings: theory Sort_Encodings.Mcalc2C
22:36:39 Complx: theory Complx.OG_Soundness
22:36:43 Sort_Encodings: theory Sort_Encodings.G
22:36:48 Timing Simple_Clause_Learning (8 threads, 123.971s elapsed time, 476.869s cpu time, 42.287s GC time, factor 3.85)
22:36:48 Finished Simple_Clause_Learning (0:02:06 elapsed time, 0:08:02 cpu time, factor 3.83)
22:36:59 Sort_Encodings: theory Sort_Encodings.U
22:37:00 Sort_Encodings: theory Sort_Encodings.CU
22:37:01 Sort_Encodings: theory Sort_Encodings.E
22:37:08 Estimated 0:48:06 build time with default build heuristic (took 67.659s)
22:37:11 Running Matrices_for_ODEs (on of4.proof.cit.tum.de+0-3,12-15) ...
22:37:12 Sort_Encodings: theory Sort_Encodings.Encodings
22:37:12 Running SC_DOM_Components (on of2.proof.cit.tum.de+0-7) ...
22:37:13 Matrices_for_ODEs: theory HOL-Library.Code_Cardinality
22:37:13 Matrices_for_ODEs: theory HOL-Library.Lattice_Algebras
22:37:13 Matrices_for_ODEs: theory HOL-Library.Log_Nat
22:37:13 Matrices_for_ODEs: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
22:37:13 Matrices_for_ODEs: theory List-Index.List_Index
22:37:13 Matrices_for_ODEs: theory Ordinary_Differential_Equations.Vector_Derivative_On
22:37:13 Matrices_for_ODEs: theory Ordinary_Differential_Equations.Gronwall
22:37:13 Matrices_for_ODEs: theory Ordinary_Differential_Equations.Interval_Integral_HK
22:37:14 Timing Sort_Encodings (1 threads, 93.968s elapsed time, 106.107s cpu time, 13.116s GC time, factor 1.13)
22:37:14 Finished Sort_Encodings (0:01:35 elapsed time, 0:01:49 cpu time, factor 1.14)
22:37:16 Matrices_for_ODEs: theory HOL-Library.Float
22:37:16 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_DOM_Components
22:37:17 Matrices_for_ODEs: theory Affine_Arithmetic.Executable_Euclidean_Space
22:37:19 Matrices_for_ODEs: theory Ordinary_Differential_Equations.ODE_Auxiliarities
22:37:20 Matrices_for_ODEs: theory Ordinary_Differential_Equations.Initial_Value_Problem
22:37:21 Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge
22:37:21 Matrices_for_ODEs: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
22:37:21 SC_DOM_Components: theory SC_DOM_Components.Core_DOM_SC_DOM_Components
22:37:22 Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_Preliminaries
22:37:22 Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_ODEs
22:37:22 Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Preliminaries
22:37:23 Matrices_for_ODEs: theory Hybrid_Systems_VCs.HS_VC_Spartan
22:37:23 Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Norms
22:37:23 Matrices_for_ODEs: theory Matrices_for_ODEs.SQ_MTX
22:37:25 Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Flows
22:37:25 Matrices_for_ODEs: theory Matrices_for_ODEs.MTX_Examples
22:37:27 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_DOM_Components
22:37:32 Building Transition_Systems_and_Automata (on 10.195.8.49+0-7) ...
22:37:34 Timing Groebner_Macaulay (1 threads, 251.840s elapsed time, 307.237s cpu time, 64.622s GC time, factor 1.22)
22:37:34 Finished Groebner_Macaulay (0:04:16 elapsed time, 0:05:17 cpu time, factor 1.24)
22:37:35 Transition_Systems_and_Automata: theory CAVA_Base.Statistics
22:37:35 Running BTree (on of1.proof.cit.tum.de+0-7) ...
22:37:35 Transition_Systems_and_Automata: theory HOL-Library.Omega_Words_Fun
22:37:36 BTree: theory HOL-Data_Structures.Cmp
22:37:36 BTree: theory HOL-Data_Structures.Less_False
22:37:36 BTree: theory HOL-Library.Sublist
22:37:36 BTree: theory HOL-Data_Structures.Sorted_Less
22:37:37 BTree: theory HOL-Data_Structures.List_Ins_Del
22:37:37 BTree: theory BTree.BTree
22:37:37 BTree: theory BTree.BPlusTree
22:37:37 BTree: theory HOL-Data_Structures.Set_Specs
22:37:38 SC_DOM_Components: theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components
22:37:38 Transition_Systems_and_Automata: theory HOL-Library.Nat_Bijection
22:37:38 BTree: theory BTree.BTree_Height
22:37:38 BTree: theory BTree.BTree_Set
22:37:39 Transition_Systems_and_Automata: theory HOL-Library.Stream
22:37:39 BTree: theory BTree.BPlusTree_Split
22:37:40 BTree: theory BTree.BPlusTree_Range
22:37:40 BTree: theory BTree.BPlusTree_Set
22:37:42 BTree: theory BTree.BTree_Split
22:37:43 Transition_Systems_and_Automata: theory HOL-Library.Old_Datatype
22:37:44 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Basic
22:37:45 BTree: theory BTree.BPlusTree_SplitCE
22:37:46 Timing Koenigsberg_Friendship (1 threads, 125.132s elapsed time, 138.494s cpu time, 16.142s GC time, factor 1.11)
22:37:46 Finished Koenigsberg_Friendship (0:02:08 elapsed time, 0:02:22 cpu time, factor 1.11)
22:37:47 Running Network_Security_Policy_Verification (on of3.proof.cit.tum.de+0-7) ...
22:37:48 Network_Security_Policy_Verification: theory HOL-Eisbach.Eisbach
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Cancellation
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Char_ord
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Code_Abstract_Nat
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Infinite_Set
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.List_Lexorder
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Option_ord
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Product_Lexorder
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Code_Target_Nat
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.RBT_Impl
22:37:48 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph
22:37:48 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz
22:37:48 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable
22:37:48 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util
22:37:48 Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_Impl
22:37:48 Network_Security_Policy_Verification: theory HOL-Library.Multiset
22:37:49 Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_List_Impl
22:37:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph
22:37:49 Timing Matrices_for_ODEs (8 threads, 35.544s elapsed time, 117.863s cpu time, 7.199s GC time, factor 3.32)
22:37:49 Finished Matrices_for_ODEs (0:00:37 elapsed time, 0:02:00 cpu time, factor 3.22)
22:37:50 Running ShortestPath (on 10.195.8.11+0-7) ...
22:37:53 Network_Security_Policy_Verification: theory HOL-ex.Quicksort
22:37:53 ShortestPath: theory ShortestPath.ShortestPath
22:37:53 Network_Security_Policy_Verification: theory Automatic_Refinement.Misc
22:37:55 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Misc
22:37:55 Transition_Systems_and_Automata: theory HOL-Library.Sublist
22:37:56 ShortestPath: theory ShortestPath.ShortestPathNeg
22:37:57 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct
22:38:01 Timing ShortestPath (1 threads, 7.854s elapsed time, 9.025s cpu time, 1.454s GC time, factor 1.15)
22:38:01 Finished ShortestPath (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.11)
22:38:03 Transition_Systems_and_Automata: theory HOL-Library.Countable
22:38:05 Transition_Systems_and_Automata: theory HOL-Library.Countable_Set
22:38:06 Running X86_Semantics (on 10.195.8.29+0-7) ...
22:38:07 X86_Semantics: theory HOL-Eisbach.Eisbach
22:38:08 Transition_Systems_and_Automata: theory HOL-Library.Countable_Complete_Lattices
22:38:08 X86_Semantics: theory HOL-Library.Phantom_Type
22:38:09 X86_Semantics: theory HOL-Library.Cardinality
22:38:11 Building Three_Squares (on 10.195.8.30+0-7) ...
22:38:11 X86_Semantics: theory HOL-Library.Numeral_Type
22:38:11 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
22:38:13 X86_Semantics: theory HOL-Library.Type_Length
22:38:13 Network_Security_Policy_Verification: theory HOL-Library.RBT
22:38:14 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl
22:38:14 X86_Semantics: theory HOL-Library.Word
22:38:14 Transition_Systems_and_Automata: theory HOL-Library.Order_Continuity
22:38:15 Three_Squares: theory HOL-Eisbach.Eisbach
22:38:15 Transition_Systems_and_Automata: theory HOL-Library.Extended_Nat
22:38:16 Three_Squares: theory HOL-Eisbach.Eisbach_Tools
22:38:16 Three_Squares: theory Pure-ex.Guess
22:38:16 Three_Squares: theory HOL-Combinatorics.Stirling
22:38:17 Transition_Systems_and_Automata: theory HOL-Library.Linear_Temporal_Logic_on_Streams
22:38:17 Three_Squares: theory HOL-Computational_Algebra.Fraction_Field
22:38:20 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
22:38:21 Three_Squares: theory HOL-Computational_Algebra.Group_Closure
22:38:22 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework_Refine_Aux
22:38:23 Three_Squares: theory HOL-Decision_Procs.Dense_Linear_Order
22:38:23 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Basic
22:38:24 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence
22:38:27 Three_Squares: theory HOL-Library.Adhoc_Overloading
22:38:28 Three_Squares: theory Three_Squares.Low_Dimensional_Linear_Algebra
22:38:29 Network_Security_Policy_Verification: theory HOL-Lattice.Orders
22:38:29 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Vertices
22:38:29 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface
22:38:29 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.vertex_example_simps
22:38:29 Running Tail_Recursive_Functions (on 10.195.8.11+0-7) ...
22:38:29 Network_Security_Policy_Verification: theory HOL-Lattice.Bounds
22:38:30 Network_Security_Policy_Verification: theory HOL-Lattice.Lattice
22:38:30 Network_Security_Policy_Verification: theory HOL-Lattice.CompleteLattice
22:38:30 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_withOffendingFlows
22:38:31 Complx: theory Complx.OG_Tactics
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_ENF
22:38:31 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy1
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Helper
22:38:31 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_LTL
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPstrict
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl
22:38:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets2
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting
22:38:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted
22:38:32 Three_Squares: theory HOL-Computational_Algebra.Normalized_Fraction
22:38:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory
22:38:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface_impl
22:38:33 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance
22:38:33 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_Zip
22:38:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Analysis_Tainting
22:38:33 Tail_Recursive_Functions: theory Tail_Recursive_Functions.CaseStudy2
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl
22:38:34 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl
22:38:34 Running Native_Word (on of4.proof.cit.tum.de+4-11) ...
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets_impl
22:38:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl
22:38:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl
22:38:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting_impl
22:38:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl
22:38:35 Native_Word: theory HOL-Library.Adhoc_Overloading
22:38:35 Native_Word: theory HOL-Library.Code_Target_Int
22:38:35 Native_Word: theory HOL-Library.Code_Test
22:38:35 Native_Word: theory HOL-Library.Nat_Bijection
22:38:35 Native_Word: theory HOL-Library.Old_Datatype
22:38:35 Native_Word: theory Native_Word.Code_Int_Integer_Conversion
22:38:35 Native_Word: theory Native_Word.Code_Target_Word_Base
22:38:35 Native_Word: theory Native_Word.Code_Target_Integer_Bit
22:38:35 Native_Word: theory HOL-Library.Monad_Syntax
22:38:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl
22:38:35 Native_Word: theory Native_Word.Word_Type_Copies
22:38:36 Native_Word: theory HOL-Library.Countable
22:38:36 Three_Squares: theory HOL-Computational_Algebra.Nth_Powers
22:38:36 Native_Word: theory HOL-Imperative_HOL.Heap
22:38:37 Three_Squares: theory HOL-Computational_Algebra.Squarefree
22:38:37 Native_Word: theory HOL-Imperative_HOL.Heap_Monad
22:38:38 Three_Squares: theory HOL-Number_Theory.Cong
22:38:38 Native_Word: theory Native_Word.Native_Word_Imperative_HOL
22:38:39 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary
22:38:39 Complx: theory Complx.OG_Syntax
22:38:39 Native_Word: theory Native_Word.Code_Target_Int_Bit
22:38:39 Native_Word: theory Native_Word.Uint
22:38:39 Native_Word: theory Native_Word.Uint16
22:38:39 Native_Word: theory Native_Word.Uint32
22:38:39 Native_Word: theory Native_Word.Uint64
22:38:39 Native_Word: theory Native_Word.Uint8
22:38:40 Complx: theory Complx.Examples
22:38:40 Tail_Recursive_Functions: theory Tail_Recursive_Functions.Method
22:38:41 Native_Word: theory Native_Word.Native_Cast
22:38:41 Native_Word: theory Native_Word.Native_Cast_Uint
22:38:41 Native_Word: theory Native_Word.Native_Word_Test
22:38:41 Timing Tail_Recursive_Functions (1 threads, 10.047s elapsed time, 11.053s cpu time, 1.608s GC time, factor 1.10)
22:38:41 Finished Tail_Recursive_Functions (0:00:12 elapsed time, 0:00:13 cpu time, factor 1.11)
22:38:42 Three_Squares: theory HOL-Library.Code_Abstract_Nat
22:38:42 Three_Squares: theory HOL-Library.Code_Target_Nat
22:38:42 Three_Squares: theory HOL-Library.Code_Target_Int
22:38:42 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Maps
22:38:42 Three_Squares: theory HOL-Library.Code_Target_Numeral
22:38:43 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Refine
22:38:43 Three_Squares: theory HOL-Algebra.Congruence
22:38:44 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Library
22:38:45 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_BLP
22:38:45 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Impl
22:38:45 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_generateCode
22:38:45 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Network_Security_Policy_Verification
22:38:46 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Acceptance_Refine
22:38:46 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Degeneralization_Refine
22:38:47 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System
22:38:48 Three_Squares: theory HOL-Algebra.Order
22:38:49 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Construction
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_NetModel
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.attic
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CryptoDB
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Distributed_WebApp
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_Forte14
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.I8_SSH_Landscape
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.IDEM
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance
22:38:49 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.MeasrDroid
22:38:49 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Extra
22:38:50 Complx: theory Complx.SumArr
22:38:50 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Deterministic
22:38:51 Three_Squares: theory HOL-Algebra.Lattice
22:38:54 X86_Semantics: theory Word_Lib.Bit_Comprehension
22:38:55 Three_Squares: theory HOL-Algebra.Complete_Lattice
22:38:55 X86_Semantics: theory Word_Lib.Legacy_Aliases
22:38:55 X86_Semantics: theory Word_Lib.More_Divides
22:38:57 X86_Semantics: theory Word_Lib.Syntax_Bundles
22:38:57 X86_Semantics: theory HOL-Library.Sublist
22:39:00 Running PAC_Checker (on 10.195.8.11+0-7) ...
22:39:01 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA
22:39:02 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA
22:39:04 PAC_Checker: theory Deriving.Derive_Manager
22:39:04 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA
22:39:04 PAC_Checker: theory Deriving.Generator_Aux
22:39:04 PAC_Checker: theory HOL-Combinatorics.Transposition
22:39:05 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DFA
22:39:05 PAC_Checker: theory HOL-Library.Multiset_Order
22:39:05 X86_Semantics: theory Word_Lib.Even_More_List
22:39:06 X86_Semantics: theory Word_Lib.More_Arithmetic
22:39:06 X86_Semantics: theory Word_Lib.More_Bit_Ring
22:39:07 Three_Squares: theory HOL-Algebra.Group
22:39:08 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBA
22:39:09 X86_Semantics: theory Word_Lib.More_Word
22:39:09 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBA_Combine
22:39:10 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGBTA
22:39:11 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Imaginary_Factory_Network
22:39:11 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Examples
22:39:12 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DBTA_Combine
22:39:14 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DGCA
22:39:15 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DCA_Combine
22:39:16 PAC_Checker: theory HOL-Library.Conditional_Parametricity
22:39:16 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA
22:39:17 PAC_Checker: theory HOL-Library.Fun_Lexorder
22:39:17 PAC_Checker: theory HOL-Library.FuncSet
22:39:19 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Combine
22:39:20 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Nondeterministic
22:39:21 Skipping theories "Array_SBlit", "Partially_Filled_Array", "BTree_Imp", "BTree_ImpSet", "BTree_ImpSplit", "Flatten_Iter_Spec", "Flatten_Iter", "BPlusTree_Imp", "BPlusTree_ImpSplit", "BPlusTree_ImpSet", "BPlusTree_Iter_OneWay", "BPlusTree_Iter", "BPlusTree_ImpRange", "BPlusTree_ImpSplitCE" (undefined ISABELLE_OCAMLFIND)
22:39:21 Timing BTree (8 threads, 103.999s elapsed time, 283.795s cpu time, 10.836s GC time, factor 2.73)
22:39:21 Finished BTree (0:01:46 elapsed time, 0:04:47 cpu time, factor 2.71)
22:39:22 Three_Squares: theory HOL-Algebra.Coset
22:39:22 X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:39:23 X86_Semantics: theory Word_Lib.Aligned
22:39:24 PAC_Checker: theory HOL-Algebra.Congruence
22:39:28 X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
22:39:30 X86_Semantics: theory Word_Lib.Least_significant_bit
22:39:31 PAC_Checker: theory HOL-Algebra.Order
22:39:31 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
22:39:31 X86_Semantics: theory Word_Lib.Most_significant_bit
22:39:31 X86_Semantics: theory Word_Lib.Generic_set_bit
22:39:32 X86_Semantics: theory Word_Lib.Bits_Int
22:39:33 Running Auto2_Imperative_HOL (on of1.proof.cit.tum.de+8-15) ...
22:39:34 Auto2_Imperative_HOL: theory HOL-Library.Adhoc_Overloading
22:39:34 Auto2_Imperative_HOL: theory HOL-Library.Nat_Bijection
22:39:34 Auto2_Imperative_HOL: theory HOL-Library.Old_Datatype
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Interval
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Arrays_Ex
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Partial_Equiv_Rel
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.SepLogic_Base
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Mapping_Str
22:39:34 Auto2_Imperative_HOL: theory HOL-Library.Monad_Syntax
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Union_Find
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Connectivity
22:39:34 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Quicksort
22:39:34 Auto2_Imperative_HOL: theory HOL-Library.Countable
22:39:34 PAC_Checker: theory HOL-Algebra.Lattice
22:39:35 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Dijkstra
22:39:35 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Indexed_PQueue
22:39:35 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Lists_Ex
22:39:35 Auto2_Imperative_HOL: theory HOL-Imperative_HOL.Heap
22:39:35 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.BST
22:39:35 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Interval_Tree
22:39:36 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.RBTree
22:39:36 Auto2_Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
22:39:37 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Rect_Intersect
22:39:38 Auto2_Imperative_HOL: theory HOL-Imperative_HOL.Array
22:39:38 PAC_Checker: theory HOL-Algebra.Complete_Lattice
22:39:38 Auto2_Imperative_HOL: theory HOL-Imperative_HOL.Ref
22:39:39 Auto2_Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
22:39:39 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.SepAuto
22:39:41 Three_Squares: theory HOL-Algebra.FiniteProduct
22:39:41 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Arrays_Impl
22:39:41 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.BST_Impl
22:39:41 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.GCD_Impl
22:39:41 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.DynamicArray
22:39:41 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Quicksort_Impl
22:39:42 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.IntervalTree_Impl
22:39:42 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.LinkedList
22:39:42 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.RBTree_Impl
22:39:43 X86_Semantics: theory Word_Lib.Typedef_Morphisms
22:39:43 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Union_Find_Impl
22:39:43 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Connectivity_Impl
22:39:43 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Indexed_PQueue_Impl
22:39:44 X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
22:39:44 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Rect_Intersect_Impl
22:39:44 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Dijkstra_Impl
22:39:45 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA
22:39:46 Three_Squares: theory HOL-Algebra.Ring
22:39:46 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA
22:39:48 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NFA
22:39:49 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA
22:39:50 PAC_Checker: theory HOL-Algebra.Group
22:39:50 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Combine
22:39:51 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBTA
22:39:52 Timing Network_Security_Policy_Verification (8 threads, 121.916s elapsed time, 629.895s cpu time, 136.394s GC time, factor 5.17)
22:39:52 Finished Network_Security_Policy_Verification (0:02:03 elapsed time, 0:10:35 cpu time, factor 5.14)
22:39:53 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBTA_Combine
22:39:54 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Refine
22:39:56 Three_Squares: theory HOL-Algebra.AbelCoset
22:40:01 Building Commuting_Hermitian (on of3.proof.cit.tum.de+0-7) ...
22:40:02 Three_Squares: theory HOL-Algebra.Ideal
22:40:03 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
22:40:03 PAC_Checker: theory HOL-Algebra.Coset
22:40:04 Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
22:40:04 Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
22:40:05 X86_Semantics: theory Word_Lib.Bitwise
22:40:06 X86_Semantics: theory X86_Semantics.BitByte
22:40:08 Timing SC_DOM_Components (8 threads, 172.938s elapsed time, 980.771s cpu time, 140.641s GC time, factor 5.67)
22:40:08 Finished SC_DOM_Components (0:02:55 elapsed time, 0:16:26 cpu time, factor 5.63)
22:40:09 Three_Squares: theory HOL-Algebra.RingHom
22:40:10 X86_Semantics: theory X86_Semantics.Memory
22:40:12 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DRA_Refine
22:40:12 Three_Squares: theory HOL-Algebra.QuotRing
22:40:13 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Refine
22:40:15 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Refine
22:40:16 Transition_Systems_and_Automata: theory CAVA_Base.Code_String
22:40:16 Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Code_Target
22:40:16 Transition_Systems_and_Automata: theory CAVA_Base.CAVA_Base
22:40:16 X86_Semantics: theory X86_Semantics.State
22:40:17 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph
22:40:18 Transition_Systems_and_Automata: theory CAVA_Automata.Automata
22:40:20 PAC_Checker: theory HOL-Algebra.FiniteProduct
22:40:24 Timing Commuting_Hermitian (8 threads, 7.861s elapsed time, 44.723s cpu time, 3.523s GC time, factor 5.69)
22:40:24 Finished Commuting_Hermitian (0:00:22 elapsed time, 0:01:09 cpu time, factor 3.16)
22:40:25 PAC_Checker: theory HOL-Algebra.Ring
22:40:26 Three_Squares: theory HOL-Algebra.IntRing
22:40:26 X86_Semantics: theory X86_Semantics.StateCleanUp
22:40:29 Transition_Systems_and_Automata: theory CAVA_Automata.Lasso
22:40:30 Three_Squares: theory HOL-Algebra.Module
22:40:31 X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
22:40:32 Transition_Systems_and_Automata: theory CAVA_Automata.Digraph_Impl
22:40:33 Three_Squares: theory HOL-Algebra.UnivPoly
22:40:35 PAC_Checker: theory HOL-Algebra.AbelCoset
22:40:37 Timing Linear_Recurrences_Solver (1 threads, 891.212s elapsed time, 959.392s cpu time, 93.101s GC time, factor 1.08)
22:40:37 Finished Linear_Recurrences_Solver (0:14:57 elapsed time, 0:16:08 cpu time, factor 1.08)
22:40:41 PAC_Checker: theory HOL-Algebra.Ideal
22:40:47 X86_Semantics: theory X86_Semantics.SymbolicExecution
22:40:47 Auto2_Imperative_HOL: theory Auto2_Imperative_HOL.Sep_Examples
22:40:48 Timing Auto2_Imperative_HOL (8 threads, 73.752s elapsed time, 524.697s cpu time, 14.996s GC time, factor 7.11)
22:40:48 Finished Auto2_Imperative_HOL (0:01:15 elapsed time, 0:08:47 cpu time, factor 7.03)
22:40:49 PAC_Checker: theory HOL-Algebra.RingHom
22:40:49 X86_Semantics: theory X86_Semantics.Examples
22:40:52 PAC_Checker: theory HOL-Algebra.QuotRing
22:40:55 Transition_Systems_and_Automata: theory CAVA_Automata.Automata_Impl
22:41:00 X86_Semantics: theory X86_Semantics.X86_Parse
22:41:01 X86_Semantics: theory X86_Semantics.Example_WC
22:41:02 Native_Word: theory Native_Word.Native_Word_Test_Emu
22:41:02 Native_Word: theory Native_Word.Native_Word_Test_PolyML
22:41:02 Native_Word: theory Native_Word.Native_Word_Test_Scala
22:41:02 Native_Word: theory Native_Word.Native_Word_Test_PolyML64
22:41:03 PAC_Checker: theory HOL-Algebra.Module
22:41:07 PAC_Checker: theory HOL-Algebra.UnivPoly
22:41:07 Three_Squares: theory HOL-Algebra.Generated_Groups
22:41:09 Native_Word: theory Native_Word.Native_Word_Test_PolyML2
22:41:11 Native_Word: theory Native_Word.Native_Word_Test_MLton2
22:41:11 Native_Word: theory Native_Word.Native_Word_Test_MLton
22:41:12 Three_Squares: theory HOL-Library.Function_Algebras
22:41:13 Three_Squares: theory HOL-Algebra.Elementary_Groups
22:41:15 Native_Word: theory Native_Word.Uint_Userguide
22:41:19 Skipping theories "Native_Word_Test_GHC" (undefined ISABELLE_GHC)
22:41:19 Skipping theories "Native_Word_Test_OCaml", "Native_Word_Test_OCaml2" (undefined ISABELLE_OCAMLFIND)
22:41:19 Skipping theories "Native_Word_Test_SMLNJ", "Native_Word_Test_SMLNJ2" (undefined ISABELLE_SMLNJ)
22:41:19 Timing Native_Word (8 threads, 163.004s elapsed time, 192.089s cpu time, 17.570s GC time, factor 1.18)
22:41:19 Finished Native_Word (0:02:44 elapsed time, 0:03:14 cpu time, factor 1.18)
22:41:21 Three_Squares: theory HOL-Library.Power_By_Squaring
22:41:22 Three_Squares: theory HOL-Number_Theory.Mod_Exp
22:41:23 Three_Squares: theory HOL-Number_Theory.Eratosthenes
22:41:29 Estimated 0:46:09 build time with default build heuristic (took 69.831s)
22:41:33 Three_Squares: theory Bernoulli.Bernoulli
22:41:35 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NBA_Graphs
22:41:35 Three_Squares: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
22:41:37 PAC_Checker: theory HOL-Algebra.Generated_Groups
22:41:38 Running DFS_Framework (on of2.proof.cit.tum.de+0-7) ...
22:41:38 Three_Squares: theory HOL-Algebra.Multiplicative_Group
22:41:39 Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NGBA_Graphs
22:41:39 DFS_Framework: theory DFS_Framework.DFS_Framework_Misc
22:41:39 DFS_Framework: theory DFS_Framework.On_Stack
22:41:39 DFS_Framework: theory DFS_Framework.DFS_Framework_Refine_Aux
22:41:39 DFS_Framework: theory DFS_Framework.Impl_Rev_Array_Stack
22:41:40 DFS_Framework: theory DFS_Framework.DFS_Chapter_Examples
22:41:40 DFS_Framework: theory DFS_Framework.DFS_Chapter_Framework
22:41:40 DFS_Framework: theory DFS_Framework.Param_DFS
22:41:42 PAC_Checker: theory HOL-Library.Disjoint_Sets
22:41:42 DFS_Framework: theory DFS_Framework.DFS_Invars_Basic
22:41:42 DFS_Framework: theory DFS_Framework.General_DFS_Structure
22:41:44 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton
22:41:44 DFS_Framework: theory DFS_Framework.DFS_Invars_SCC
22:41:46 DFS_Framework: theory DFS_Framework.Rec_Impl
22:41:46 DFS_Framework: theory DFS_Framework.Tailrec_Impl
22:41:46 Running ResiduatedTransitionSystem (on of1.proof.cit.tum.de+8-15) ...
22:41:46 PAC_Checker: theory HOL-Combinatorics.Permutations
22:41:48 Building Prime_Distribution_Elementary (on of3.proof.cit.tum.de+0-7) ...
22:41:49 DFS_Framework: theory DFS_Framework.Simple_Impl
22:41:50 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega
22:41:50 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
22:41:50 Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula
22:41:51 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
22:41:51 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
22:41:51 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
22:41:51 Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
22:41:52 Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
22:41:52 PAC_Checker: theory HOL-Combinatorics.List_Permutation
22:41:52 PAC_Checker: theory HOL-Algebra.Divisibility
22:41:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
22:41:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
22:41:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial
22:41:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
22:41:52 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian
22:41:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
22:41:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
22:41:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
22:41:53 DFS_Framework: theory DFS_Framework.Restr_Impl
22:41:53 Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
22:41:54 DFS_Framework: theory DFS_Framework.DFS_Framework
22:41:55 DFS_Framework: theory DFS_Framework.Cyc_Check
22:41:55 ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.ResiduatedTransitionSystem
22:41:55 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom
22:41:55 DFS_Framework: theory DFS_Framework.DFS_Find_Path
22:41:55 DFS_Framework: theory DFS_Framework.Reachable_Nodes
22:41:55 DFS_Framework: theory DFS_Framework.Tarjan_LowLink
22:41:55 DFS_Framework: theory DFS_Framework.Tarjan
22:41:57 Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
22:41:59 Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
22:42:00 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
22:42:06 Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds
22:42:06 ResiduatedTransitionSystem: theory ResiduatedTransitionSystem.LambdaCalculus
22:42:06 PAC_Checker: theory HOL-Library.Function_Algebras
22:42:06 PAC_Checker: theory HOL-Library.Groups_Big_Fun
22:42:09 PAC_Checker: theory Abstract-Rewriting.Seq
22:42:11 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
22:42:11 PAC_Checker: theory HOL-Algebra.Elementary_Groups
22:42:16 DFS_Framework: theory DFS_Framework.Feedback_Arcs
22:42:16 Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds
22:42:18 Running MDP-Algorithms (on 10.195.8.32+0-7) ...
22:42:18 PAC_Checker: theory HOL-Library.Ramsey
22:42:18 Timing Prime_Distribution_Elementary (8 threads, 10.645s elapsed time, 69.728s cpu time, 3.459s GC time, factor 6.55)
22:42:18 Finished Prime_Distribution_Elementary (0:00:24 elapsed time, 0:01:33 cpu time, factor 3.87)
22:42:21 DFS_Framework: theory DFS_Framework.Nested_DFS
22:42:22 MDP-Algorithms: theory HOL-Eisbach.Eisbach
22:42:22 Running Algebraic_VCs (on of4.proof.cit.tum.de+0-3,12-15) ...
22:42:23 MDP-Algorithms: theory Containers.Equal
22:42:23 MDP-Algorithms: theory Containers.Closure_Set
22:42:23 MDP-Algorithms: theory Containers.Extend_Partial_Order
22:42:23 Algebraic_VCs: theory HOL-Eisbach.Eisbach
22:42:23 Algebraic_VCs: theory HOL-Hoare.Heap
22:42:23 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_scratch
22:42:23 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_scratch
22:42:23 Algebraic_VCs: theory KAD.Domain_Semiring
22:42:23 Algebraic_VCs: theory Algebraic_VCs.P2S2R
22:42:23 Algebraic_VCs: theory Algebraic_VCs.VC_KAT
22:42:24 Transition_Systems_and_Automata: theory DFS_Framework.Impl_Rev_Array_Stack
22:42:24 MDP-Algorithms: theory Containers.List_Fusion
22:42:24 Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations
22:42:25 Algebraic_VCs: theory Algebraic_VCs.RKAT
22:42:25 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples
22:42:25 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples2
22:42:26 Algebraic_VCs: theory Algebraic_VCs.RKAT_Models
22:42:26 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT
22:42:26 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT_Examples
22:42:26 Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
22:42:27 MDP-Algorithms: theory Deriving.Comparator
22:42:27 Transition_Systems_and_Automata: theory DFS_Framework.Param_DFS
22:42:29 Algebraic_VCs: theory KAD.Antidomain_Semiring
22:42:29 MDP-Algorithms: theory Deriving.Compare
22:42:31 MDP-Algorithms: theory Deriving.Derive_Manager
22:42:31 MDP-Algorithms: theory Deriving.Generator_Aux
22:42:31 MDP-Algorithms: theory Deriving.Comparator_Generator
22:42:33 Running TsirelsonBound (on of3.proof.cit.tum.de+0-7) ...
22:42:33 MDP-Algorithms: theory Deriving.Compare_Generator
22:42:34 MDP-Algorithms: theory Deriving.Equality_Generator
22:42:34 PAC_Checker: theory HOL-Library.More_List
22:42:35 TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
22:42:35 MDP-Algorithms: theory Deriving.Equality_Instances
22:42:35 MDP-Algorithms: theory HOL-Computational_Algebra.Fraction_Field
22:42:35 PAC_Checker: theory HOL-Library.Poly_Mapping
22:42:36 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Applications
22:42:36 Algebraic_VCs: theory KAD.Range_Semiring
22:42:36 TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
22:42:36 DFS_Framework: theory DFS_Framework.DFS_All_Examples
22:42:36 TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
22:42:37 TsirelsonBound: theory TsirelsonBound.Tsirelson
22:42:37 Three_Squares: theory Dirichlet_L.Multiplicative_Characters
22:42:38 MDP-Algorithms: theory HOL-Data_Structures.Array_Specs
22:42:38 MDP-Algorithms: theory HOL-Data_Structures.Cmp
22:42:38 Timing DFS_Framework (8 threads, 58.045s elapsed time, 235.940s cpu time, 28.198s GC time, factor 4.06)
22:42:39 Finished DFS_Framework (0:01:00 elapsed time, 0:04:00 cpu time, factor 3.99)
22:42:39 MDP-Algorithms: theory HOL-Data_Structures.Less_False
22:42:39 MDP-Algorithms: theory HOL-Data_Structures.Sorted_Less
22:42:39 MDP-Algorithms: theory HOL-Data_Structures.AList_Upd_Del
22:42:41 MDP-Algorithms: theory HOL-Data_Structures.Map_Specs
22:42:41 MDP-Algorithms: theory HOL-Data_Structures.List_Ins_Del
22:42:41 MDP-Algorithms: theory HOL-Data_Structures.Set_Specs
22:42:42 MDP-Algorithms: theory Containers.Containers_Auxiliary
22:42:42 MDP-Algorithms: theory HOL-Computational_Algebra.Normalized_Fraction
22:42:43 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra
22:42:44 PAC_Checker: theory Polynomials.MPoly_Type
22:42:46 MDP-Algorithms: theory HOL-Library.Char_ord
22:42:46 MDP-Algorithms: theory Containers.Lexicographic_Order
22:42:46 Algebraic_VCs: theory Algebraic_VCs.Domain_Quantale
22:42:46 Algebraic_VCs: theory KAD.Modal_Kleene_Algebra_Models
22:42:47 MDP-Algorithms: theory Deriving.Compare_Instances
22:42:47 PAC_Checker: theory Polynomials.More_MPoly_Type
22:42:48 Timing TsirelsonBound (8 threads, 12.638s elapsed time, 64.259s cpu time, 3.261s GC time, factor 5.08)
22:42:48 Finished TsirelsonBound (0:00:14 elapsed time, 0:01:06 cpu time, factor 4.52)
22:42:48 MDP-Algorithms: theory HOL-Library.Code_Abstract_Nat
22:42:48 MDP-Algorithms: theory HOL-Library.Code_Target_Nat
22:42:49 MDP-Algorithms: theory HOL-Library.Code_Target_Int
22:42:49 MDP-Algorithms: theory HOL-Library.Code_Target_Numeral
22:42:49 MDP-Algorithms: theory HOL-Algebra.Congruence
22:42:49 Algebraic_VCs: theory Algebraic_VCs.VC_KAD
22:42:51 Three_Squares: theory HOL-Computational_Algebra.Field_as_Ring
22:42:53 Three_Squares: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:42:54 Algebraic_VCs: theory Algebraic_VCs.Path_Model_Example
22:42:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples
22:42:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual
22:42:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples2
22:42:54 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf
22:42:54 Algebraic_VCs: theory Algebraic_VCs.KAD_is_KAT
22:42:54 PAC_Checker: theory HOL-Library.Sublist
22:42:54 MDP-Algorithms: theory HOL-Algebra.Order
22:42:54 Algebraic_VCs: theory Algebraic_VCs.Pointer_Examples
22:42:56 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf_Examples
22:42:56 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual_Examples
22:42:56 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Invars_Basic
22:42:56 MDP-Algorithms: theory HOL-Algebra.Lattice
22:42:57 Running Key_Agreement_Strong_Adversaries (on of2.proof.cit.tum.de+8-15) ...
22:42:58 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Messages
22:42:58 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Infra
22:42:58 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Refinement
22:43:00 MDP-Algorithms: theory HOL-Algebra.Complete_Lattice
22:43:00 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationN
22:43:00 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Message_derivation
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Runs
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationI
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Channels
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.IK
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Payloads
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Secrecy
22:43:01 PAC_Checker: theory Nested_Multisets_Ordinals.Multiset_More
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl1
22:43:01 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_asymmetric
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_lemmas
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl1
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_symmetric
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl2
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl1
22:43:02 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl2
22:43:03 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3
22:43:03 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl2
22:43:03 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3
22:43:04 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric
22:43:04 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric
22:43:04 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric
22:43:04 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3
22:43:04 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric
22:43:05 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric
22:43:05 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric
22:43:07 Running MonoidalCategory (on of3.proof.cit.tum.de+8-15) ...
22:43:08 MonoidalCategory: theory MonoidalCategory.MonoidalCategory
22:43:10 MDP-Algorithms: theory HOL-Algebra.Group
22:43:12 Timing Algebraic_VCs (8 threads, 48.313s elapsed time, 131.712s cpu time, 17.920s GC time, factor 2.73)
22:43:13 Finished Algebraic_VCs (0:00:49 elapsed time, 0:02:14 cpu time, factor 2.70)
22:43:24 MDP-Algorithms: theory HOL-Algebra.Coset
22:43:25 PAC_Checker: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
22:43:26 PAC_Checker: theory HOL-Library.Countable_Set
22:43:27 Three_Squares: theory HOL-Computational_Algebra.Polynomial_Factorial
22:43:30 PAC_Checker: theory HOL-Library.FSet
22:43:31 Running Differential_Game_Logic (on of4.proof.cit.tum.de+0-3,12-15) ...
22:43:32 Differential_Game_Logic: theory Differential_Game_Logic.Identifiers
22:43:32 Differential_Game_Logic: theory Differential_Game_Logic.Lib
22:43:32 Differential_Game_Logic: theory Differential_Game_Logic.Syntax
22:43:32 Transition_Systems_and_Automata: theory DFS_Framework.General_DFS_Structure
22:43:33 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
22:43:33 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
22:43:34 Differential_Game_Logic: theory Differential_Game_Logic.Ids
22:43:34 Differential_Game_Logic: theory Differential_Game_Logic.Denotational_Semantics
22:43:35 Differential_Game_Logic: theory Differential_Game_Logic.Static_Semantics
22:43:35 Differential_Game_Logic: theory Differential_Game_Logic.Axioms
22:43:35 Differential_Game_Logic: theory Differential_Game_Logic.Coincidence
22:43:36 Differential_Game_Logic: theory Differential_Game_Logic.USubst
22:43:37 Timing ResiduatedTransitionSystem (8 threads, 108.469s elapsed time, 409.418s cpu time, 34.215s GC time, factor 3.77)
22:43:37 Finished ResiduatedTransitionSystem (0:01:50 elapsed time, 0:06:54 cpu time, factor 3.75)
22:43:38 Three_Squares: theory HOL-Computational_Algebra.Computational_Algebra
22:43:38 Differential_Game_Logic: theory Differential_Game_Logic.Differential_Game_Logic
22:43:39 MDP-Algorithms: theory HOL-Algebra.FiniteProduct
22:43:39 Three_Squares: theory Sturm_Tarski.PolyMisc
22:43:41 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
22:43:42 Three_Squares: theory HOL-Library.Going_To_Filter
22:43:42 Three_Squares: theory HOL-Library.Lattice_Algebras
22:43:44 MDP-Algorithms: theory HOL-Algebra.Ring
22:43:44 PAC_Checker: theory HOL-Library.Finite_Map
22:43:50 Three_Squares: theory HOL-Library.Interval
22:43:51 Timing Differential_Game_Logic (8 threads, 18.858s elapsed time, 57.726s cpu time, 5.240s GC time, factor 3.06)
22:43:51 Finished Differential_Game_Logic (0:00:20 elapsed time, 0:01:00 cpu time, factor 2.92)
22:43:53 Running Virtual_Substitution (on of1.proof.cit.tum.de+0-7) ...
22:43:53 MDP-Algorithms: theory HOL-Algebra.Module
22:43:55 Virtual_Substitution: theory Deriving.Derive_Manager
22:43:55 Virtual_Substitution: theory HOL-Library.AList
22:43:55 Virtual_Substitution: theory Deriving.Generator_Aux
22:43:55 Virtual_Substitution: theory HOL-Library.Code_Target_Int
22:43:55 Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat
22:43:55 Virtual_Substitution: theory HOL-Library.Conditional_Parametricity
22:43:56 Virtual_Substitution: theory HOL-Library.Fun_Lexorder
22:43:56 Virtual_Substitution: theory HOL-Library.Function_Algebras
22:43:56 Virtual_Substitution: theory HOL-Library.Groups_Big_Fun
22:43:56 Virtual_Substitution: theory Abstract-Rewriting.Seq
22:43:56 Virtual_Substitution: theory HOL-Library.Code_Target_Nat
22:43:56 Virtual_Substitution: theory HOL-Library.Ramsey
22:43:56 Virtual_Substitution: theory HOL-Library.More_List
22:43:56 Virtual_Substitution: theory HOL-Library.Sublist
22:43:56 Virtual_Substitution: theory HOL-Library.While_Combinator
22:43:56 Virtual_Substitution: theory HOL-Library.FSet
22:43:56 Virtual_Substitution: theory HOL-Library.Poly_Mapping
22:43:56 Virtual_Substitution: theory Polynomials.More_Modules
22:43:56 Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial
22:43:56 Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant
22:43:56 Virtual_Substitution: theory Matrix.Utility
22:43:56 Virtual_Substitution: theory Open_Induction.Restricted_Predicates
22:43:56 Virtual_Substitution: theory Regular-Sets.Regular_Set
22:43:56 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Misc
22:43:56 Virtual_Substitution: theory Show.Show
22:43:57 Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences
22:43:57 Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements
22:43:57 Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum
22:43:57 MDP-Algorithms: theory Jordan_Normal_Form.Missing_Ring
22:43:57 Virtual_Substitution: theory Polynomials.MPoly_Type
22:43:58 Virtual_Substitution: theory Show.Show_Instances
22:43:58 Virtual_Substitution: theory Show.Show_Real
22:43:58 Virtual_Substitution: theory Regular-Sets.Regular_Exp
22:43:58 Virtual_Substitution: theory Polynomials.More_MPoly_Type
22:43:58 PAC_Checker: theory PAC_Checker.Finite_Map_Multiset
22:43:59 Virtual_Substitution: theory HOL-Library.Finite_Map
22:44:00 PAC_Checker: theory Polynomials.More_Modules
22:44:00 Virtual_Substitution: theory Regular-Sets.NDerivative
22:44:00 Virtual_Substitution: theory Regular-Sets.Relation_Interpretation
22:44:00 PAC_Checker: theory HOL-Algebra.Multiplicative_Group
22:44:02 Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate
22:44:02 Virtual_Substitution: theory Regular-Sets.Equivalence_Checking
22:44:02 Virtual_Substitution: theory Regular-Sets.Regexp_Method
22:44:02 Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting
22:44:02 Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full
22:44:03 MDP-Algorithms: theory HOL-Library.IArray
22:44:03 Timing Key_Agreement_Strong_Adversaries (8 threads, 64.007s elapsed time, 378.689s cpu time, 17.460s GC time, factor 5.92)
22:44:03 Finished Key_Agreement_Strong_Adversaries (0:01:05 elapsed time, 0:06:21 cpu time, factor 5.85)
22:44:03 Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:44:03 Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations
22:44:03 Virtual_Substitution: theory Abstract-Rewriting.SN_Orders
22:44:05 Virtual_Substitution: theory Polynomials.Utils
22:44:05 Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders
22:44:05 MDP-Algorithms: theory HOL-Library.More_List
22:44:05 Virtual_Substitution: theory Polynomials.Power_Products
22:44:06 MDP-Algorithms: theory Containers.Containers_Generator
22:44:06 Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map
22:44:06 MDP-Algorithms: theory Containers.Collection_Enum
22:44:06 Virtual_Substitution: theory Polynomials.Polynomials
22:44:08 MDP-Algorithms: theory Containers.Collection_Eq
22:44:09 MDP-Algorithms: theory Containers.DList_Set
22:44:10 Virtual_Substitution: theory Polynomials.Show_Polynomials
22:44:10 Transition_Systems_and_Automata: theory DFS_Framework.Rec_Impl
22:44:11 MDP-Algorithms: theory Containers.Set_Linorder
22:44:13 PAC_Checker: theory HOL-Algebra.Ring_Divisibility
22:44:14 Virtual_Substitution: theory Polynomials.MPoly_Type_Class
22:44:15 Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered
22:44:19 Running CoreC++ (on of4.proof.cit.tum.de+4-11) ...
22:44:20 CoreC++: theory CoreC++.Auxiliary
22:44:20 CoreC++: theory CoreC++.Type
22:44:21 CoreC++: theory CoreC++.Value
22:44:21 CoreC++: theory CoreC++.Expr
22:44:22 Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap
22:44:23 Running Dirichlet_L (on of2.proof.cit.tum.de+0-7) ...
22:44:23 Virtual_Substitution: theory Virtual_Substitution.MPolyExtension
22:44:23 CoreC++: theory CoreC++.Decl
22:44:23 CoreC++: theory CoreC++.ClassRel
22:44:24 CoreC++: theory CoreC++.SubObj
22:44:24 Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps
22:44:24 Virtual_Substitution: theory Virtual_Substitution.PolyAtoms
22:44:24 CoreC++: theory CoreC++.Objects
22:44:24 CoreC++: theory CoreC++.TypeRel
22:44:24 CoreC++: theory CoreC++.Exceptions
22:44:24 CoreC++: theory CoreC++.State
22:44:24 CoreC++: theory CoreC++.Syntax
22:44:24 CoreC++: theory CoreC++.SystemClasses
22:44:24 CoreC++: theory CoreC++.WellType
22:44:24 CoreC++: theory CoreC++.BigStep
22:44:24 CoreC++: theory CoreC++.SmallStep
22:44:25 Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
22:44:25 Dirichlet_L: theory HOL-Library.Lattice_Algebras
22:44:25 Dirichlet_L: theory HOL-Library.Log_Nat
22:44:25 Dirichlet_L: theory Lehmer.Lehmer
22:44:25 Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
22:44:25 CoreC++: theory CoreC++.Annotate
22:44:25 CoreC++: theory CoreC++.WellForm
22:44:25 CoreC++: theory CoreC++.WellTypeRT
22:44:26 Virtual_Substitution: theory Virtual_Substitution.Debruijn
22:44:26 CoreC++: theory CoreC++.WWellForm
22:44:26 CoreC++: theory CoreC++.Conform
22:44:27 Virtual_Substitution: theory Virtual_Substitution.Optimizations
22:44:27 CoreC++: theory CoreC++.DefAss
22:44:28 CoreC++: theory CoreC++.Execute
22:44:28 Dirichlet_L: theory HOL-Library.Interval
22:44:28 Dirichlet_L: theory HOL-Library.Float
22:44:28 CoreC++: theory CoreC++.CWellForm
22:44:28 CoreC++: theory CoreC++.Equivalence
22:44:29 Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs
22:44:29 CoreC++: theory CoreC++.Progress
22:44:30 Dirichlet_L: theory HOL-Library.Interval_Float
22:44:30 Virtual_Substitution: theory Virtual_Substitution.Reindex
22:44:30 Virtual_Substitution: theory Virtual_Substitution.UniAtoms
22:44:30 CoreC++: theory CoreC++.HeapExtension
22:44:30 Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
22:44:31 CoreC++: theory CoreC++.TypeSafe
22:44:31 PAC_Checker: theory HOL-Algebra.Subrings
22:44:31 CoreC++: theory CoreC++.Determinism
22:44:32 Virtual_Substitution: theory Virtual_Substitution.VSAlgos
22:44:34 Dirichlet_L: theory Bertrands_Postulate.Bertrand
22:44:34 Virtual_Substitution: theory Virtual_Substitution.QE
22:44:34 Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting
22:44:36 PAC_Checker: theory HOL-Algebra.Polynomials
22:44:37 Virtual_Substitution: theory Virtual_Substitution.DNF
22:44:37 Virtual_Substitution: theory Virtual_Substitution.Heuristic
22:44:37 Virtual_Substitution: theory Virtual_Substitution.LinearCase
22:44:37 Timing MonoidalCategory (8 threads, 88.515s elapsed time, 364.823s cpu time, 38.209s GC time, factor 4.12)
22:44:37 Finished MonoidalCategory (0:01:30 elapsed time, 0:06:08 cpu time, factor 4.07)
22:44:37 Virtual_Substitution: theory Virtual_Substitution.NegInfinity
22:44:38 Virtual_Substitution: theory Virtual_Substitution.QuadraticCase
22:44:38 Three_Squares: theory HOL-Library.Log_Nat
22:44:38 Virtual_Substitution: theory Virtual_Substitution.EliminateVariable
22:44:38 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
22:44:38 Virtual_Substitution: theory Virtual_Substitution.Infinitesimals
22:44:39 Virtual_Substitution: theory Virtual_Substitution.LuckyFind
22:44:39 Virtual_Substitution: theory Virtual_Substitution.EqualityVS
22:44:39 Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni
22:44:39 Three_Squares: theory HOL-Library.Float
22:44:40 Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni
22:44:41 Virtual_Substitution: theory Virtual_Substitution.DNFUni
22:44:41 Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs
22:44:42 Virtual_Substitution: theory Virtual_Substitution.Exports
22:44:42 Virtual_Substitution: theory Virtual_Substitution.VSQuad
22:44:43 Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs
22:44:45 Dirichlet_L: theory HOL-Algebra.QuotRing
22:44:45 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
22:44:45 Virtual_Substitution: theory Virtual_Substitution.ExportProofs
22:44:45 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Hom
22:44:45 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
22:44:46 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
22:44:47 Dirichlet_L: theory HOL-Algebra.IntRing
22:44:48 Transition_Systems_and_Automata: theory DFS_Framework.Tailrec_Impl
22:44:48 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
22:44:48 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
22:44:48 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.IDirProds
22:44:49 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
22:44:49 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.DirProds
22:44:49 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Group_Relations
22:44:50 Dirichlet_L: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
22:44:50 MDP-Algorithms: theory Containers.Collection_Order
22:44:50 CoreC++: theory CoreC++.CoreC++
22:44:50 Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
22:44:51 Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
22:44:52 Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
22:44:53 MDP-Algorithms: theory Perron_Frobenius.Bij_Nat
22:44:53 MDP-Algorithms: theory HOL-Library.RBT_Impl
22:44:55 Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
22:44:57 Three_Squares: theory HOL-Library.Interval_Float
22:44:59 Timing Dirichlet_L (8 threads, 33.846s elapsed time, 175.586s cpu time, 17.617s GC time, factor 5.19)
22:44:59 Finished Dirichlet_L (0:00:35 elapsed time, 0:02:58 cpu time, factor 4.99)
22:45:00 Transition_Systems_and_Automata: theory DFS_Framework.Simple_Impl
22:45:02 Three_Squares: theory HOL-Decision_Procs.Approximation_Bounds
22:45:20 Transition_Systems_and_Automata: theory DFS_Framework.Restr_Impl
22:45:23 PAC_Checker: theory Open_Induction.Restricted_Predicates
22:45:23 Timing CoreC++ (8 threads, 62.027s elapsed time, 324.296s cpu time, 56.457s GC time, factor 5.23)
22:45:23 Finished CoreC++ (0:01:03 elapsed time, 0:05:28 cpu time, factor 5.14)
22:45:26 Transition_Systems_and_Automata: theory DFS_Framework.DFS_Framework
22:45:26 Transition_Systems_and_Automata: theory DFS_Framework.Reachable_Nodes
22:45:27 PAC_Checker: theory PAC_Checker.PAC_Misc
22:45:27 PAC_Checker: theory PAC_Checker.PAC_Version
22:45:27 PAC_Checker: theory PAC_Checker.More_Loops
22:45:28 PAC_Checker: theory Regular-Sets.Regular_Set
22:45:33 Three_Squares: theory Bernoulli.Periodic_Bernpoly
22:45:35 Three_Squares: theory Winding_Number_Eval.Missing_Topology
22:45:39 Three_Squares: theory HOL-Number_Theory.Fib
22:45:40 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
22:45:42 Three_Squares: theory HOL-Number_Theory.Prime_Powers
22:45:43 Timing HOL-ODE-Examples (1 threads, 712.166s elapsed time, 731.044s cpu time, 35.108s GC time, factor 1.03)
22:45:43 Finished HOL-ODE-Examples (0:11:56 elapsed time, 0:12:15 cpu time, factor 1.03)
22:45:44 Three_Squares: theory HOL-Number_Theory.Totient
22:45:44 PAC_Checker: theory Regular-Sets.Regular_Exp
22:45:44 PAC_Checker: theory Regular-Sets.NDerivative
22:45:45 PAC_Checker: theory Regular-Sets.Equivalence_Checking
22:45:48 PAC_Checker: theory Regular-Sets.Relation_Interpretation
22:45:49 PAC_Checker: theory Regular-Sets.Regexp_Method
22:45:49 Three_Squares: theory HOL-Number_Theory.Residues
22:45:50 PAC_Checker: theory Show.Show
22:45:51 PAC_Checker: theory Show.Show_Instances
22:45:53 PAC_Checker: theory Well_Quasi_Orders.Infinite_Sequences
22:45:53 PAC_Checker: theory Well_Quasi_Orders.Minimal_Elements
22:45:55 PAC_Checker: theory Well_Quasi_Orders.Least_Enum
22:45:56 PAC_Checker: theory Well_Quasi_Orders.Almost_Full
22:45:59 PAC_Checker: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:46:00 PAC_Checker: theory Well_Quasi_Orders.Almost_Full_Relations
22:46:00 Running Collections_Examples (on 10.195.8.40+0-7) ...
22:46:02 PAC_Checker: theory Polynomials.Utils
22:46:03 PAC_Checker: theory Well_Quasi_Orders.Well_Quasi_Orders
22:46:03 Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples_Chapter
22:46:03 Collections_Examples: theory Collections_Examples.Examples_Chapter
22:46:03 Collections_Examples: theory Collections_Examples.ICF_Examples_Chapter
22:46:03 Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples_Chapter
22:46:03 Collections_Examples: theory Containers.Equal
22:46:04 Collections_Examples: theory Containers.Closure_Set
22:46:04 Collections_Examples: theory Containers.Extend_Partial_Order
22:46:05 Collections_Examples: theory Containers.List_Fusion
22:46:06 Running Formal_Puiseux_Series (on of4.proof.cit.tum.de+0-3,12-15) ...
22:46:07 PAC_Checker: theory Polynomials.Power_Products
22:46:07 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom
22:46:07 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Unsorted
22:46:08 Collections_Examples: theory Deriving.Comparator
22:46:08 Formal_Puiseux_Series: theory Polynomial_Interpolation.Missing_Polynomial
22:46:09 Timing Virtual_Substitution (8 threads, 131.131s elapsed time, 594.358s cpu time, 67.695s GC time, factor 4.53)
22:46:09 Finished Virtual_Substitution (0:02:13 elapsed time, 0:10:02 cpu time, factor 4.50)
22:46:09 Formal_Puiseux_Series: theory Polynomial_Interpolation.Ring_Hom_Poly
22:46:10 Collections_Examples: theory Deriving.Compare
22:46:10 Three_Squares: theory HOL-Number_Theory.Euler_Criterion
22:46:10 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Puiseux_Polynomial_Library
22:46:11 Formal_Puiseux_Series: theory Formal_Puiseux_Series.FPS_Hensel
22:46:11 Collections_Examples: theory Deriving.Derive_Manager
22:46:11 Collections_Examples: theory Deriving.Generator_Aux
22:46:12 Formal_Puiseux_Series: theory Formal_Puiseux_Series.Formal_Puiseux_Series
22:46:12 Collections_Examples: theory Deriving.Comparator_Generator
22:46:12 Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path
22:46:13 Transition_Systems_and_Automata: theory Gabow_SCC.Find_Path_Impl
22:46:13 Three_Squares: theory HOL-Number_Theory.Gauss
22:46:14 Timing Formal_Puiseux_Series (8 threads, 6.332s elapsed time, 23.123s cpu time, 2.101s GC time, factor 3.65)
22:46:14 Finished Formal_Puiseux_Series (0:00:07 elapsed time, 0:00:24 cpu time, factor 3.17)
22:46:14 Collections_Examples: theory Deriving.Compare_Generator
22:46:15 Collections_Examples: theory Deriving.Equality_Generator
22:46:15 Collections_Examples: theory Deriving.Equality_Instances
22:46:15 Collections_Examples: theory HOL-Library.DAList
22:46:17 Collections_Examples: theory Containers.AssocList
22:46:19 Collections_Examples: theory Containers.Containers_Auxiliary
22:46:20 Collections_Examples: theory HOL-Library.Char_ord
22:46:20 Collections_Examples: theory Containers.Lexicographic_Order
22:46:21 Collections_Examples: theory Deriving.Compare_Instances
22:46:22 Collections_Examples: theory HOL-Library.Omega_Words_Fun
22:46:22 Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity
22:46:23 Building Expander_Graphs (on of2.proof.cit.tum.de+8-15) ...
22:46:24 Collections_Examples: theory HOL-Library.Mapping
22:46:27 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
22:46:27 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
22:46:27 Expander_Graphs: theory Graph_Theory.Rtrancl_On
22:46:27 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
22:46:27 Expander_Graphs: theory HOL-Library.More_List
22:46:27 Expander_Graphs: theory Abstract-Rewriting.Seq
22:46:27 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
22:46:27 Expander_Graphs: theory HOL-Library.While_Combinator
22:46:27 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
22:46:27 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
22:46:28 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
22:46:28 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
22:46:28 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
22:46:28 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
22:46:28 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
22:46:28 Expander_Graphs: theory Graph_Theory.Stuff
22:46:28 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
22:46:28 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
22:46:28 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG
22:46:28 Expander_Graphs: theory HOL-Decision_Procs.Approximation
22:46:28 Expander_Graphs: theory Graph_Theory.Digraph
22:46:28 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
22:46:29 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
22:46:29 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
22:46:29 Expander_Graphs: theory Matrix.Utility
22:46:29 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
22:46:29 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
22:46:29 Expander_Graphs: theory Regular-Sets.Regular_Set
22:46:30 Expander_Graphs: theory Graph_Theory.Arc_Walk
22:46:30 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
22:46:30 Building Monad_Memo_DP (on of1.proof.cit.tum.de+8-15) ...
22:46:30 PAC_Checker: theory Polynomials.MPoly_Type_Class
22:46:30 Expander_Graphs: theory VectorSpace.FunctionLemmas
22:46:30 Expander_Graphs: theory VectorSpace.RingModuleFacts
22:46:30 Monad_Memo_DP: theory HOL-Eisbach.Eisbach
22:46:30 Monad_Memo_DP: theory Deriving.Derive_Manager
22:46:30 Monad_Memo_DP: theory Deriving.Generator_Aux
22:46:30 Monad_Memo_DP: theory HOL-Library.AList
22:46:30 Monad_Memo_DP: theory HOL-Library.Case_Converter
22:46:30 Monad_Memo_DP: theory HOL-Library.Adhoc_Overloading
22:46:30 Monad_Memo_DP: theory HOL-Library.Code_Target_Int
22:46:30 Monad_Memo_DP: theory HOL-Library.Code_Abstract_Nat
22:46:31 Monad_Memo_DP: theory HOL-Library.IArray
22:46:31 Monad_Memo_DP: theory HOL-Library.Monad_Syntax
22:46:31 Monad_Memo_DP: theory HOL-Library.Code_Target_Nat
22:46:31 Expander_Graphs: theory VectorSpace.MonoidSums
22:46:31 Monad_Memo_DP: theory HOL-Library.Nat_Bijection
22:46:31 Monad_Memo_DP: theory HOL-Library.State_Monad
22:46:31 Expander_Graphs: theory Graph_Theory.Pair_Digraph
22:46:31 Monad_Memo_DP: theory HOL-Library.Simps_Case_Conv
22:46:31 Monad_Memo_DP: theory HOL-Library.Old_Datatype
22:46:31 Monad_Memo_DP: theory HOL-Library.Extended
22:46:31 Monad_Memo_DP: theory HOL-Library.Code_Target_Numeral
22:46:31 Monad_Memo_DP: theory HOL-Library.Product_Lexorder
22:46:31 Expander_Graphs: theory VectorSpace.LinearCombinations
22:46:31 Expander_Graphs: theory Regular-Sets.Regular_Exp
22:46:31 Monad_Memo_DP: theory HOL-Library.RBT_Impl
22:46:31 Monad_Memo_DP: theory HOL-Library.Sublist
22:46:31 Monad_Memo_DP: theory HOL-Library.Tree
22:46:31 Monad_Memo_DP: theory Monad_Memo_DP.Ground_Function
22:46:31 Monad_Memo_DP: theory Monad_Memo_DP.Indexing
22:46:31 Running Probabilistic_Prime_Tests (on of3.proof.cit.tum.de+8-15) ...
22:46:31 Monad_Memo_DP: theory HOL-Library.Countable
22:46:32 Monad_Memo_DP: theory Monad_Memo_DP.State_Monad_Ext
22:46:32 Monad_Memo_DP: theory Monad_Memo_DP.Pure_Monad
22:46:32 Monad_Memo_DP: theory Monad_Memo_DP.DP_CRelVS
22:46:32 Monad_Memo_DP: theory HOL-Library.Mapping
22:46:32 Monad_Memo_DP: theory Monad_Memo_DP.Solve_Cong
22:46:32 Monad_Memo_DP: theory Monad_Memo_DP.State_Heap_Misc
22:46:32 Monad_Memo_DP: theory HOL-Imperative_HOL.Heap
22:46:32 Monad_Memo_DP: theory Show.Show
22:46:33 Expander_Graphs: theory Jordan_Normal_Form.Matrix
22:46:33 Monad_Memo_DP: theory Monad_Memo_DP.Memory
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Fun_More
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Relation_More
22:46:33 Probabilistic_Prime_Tests: theory HOL-Computational_Algebra.Squarefree
22:46:33 Probabilistic_Prime_Tests: theory HOL-Algebra.Exponent
22:46:33 Probabilistic_Prime_Tests: theory HOL-Library.Fun_Lexorder
22:46:33 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Cong
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Union
22:46:33 Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence
22:46:33 Probabilistic_Prime_Tests: theory HOL-Combinatorics.Cycles
22:46:33 Probabilistic_Prime_Tests: theory HOL-Combinatorics.List_Permutation
22:46:33 Probabilistic_Prime_Tests: theory HOL-Library.Groups_Big_Fun
22:46:33 Probabilistic_Prime_Tests: theory HOL-Library.More_List
22:46:33 Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellfounded_More
22:46:33 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Relation
22:46:33 Expander_Graphs: theory Regular-Sets.NDerivative
22:46:33 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
22:46:33 Monad_Memo_DP: theory Show.Show_Instances
22:46:33 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
22:46:33 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
22:46:33 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Embedding
22:46:33 Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping
22:46:33 Monad_Memo_DP: theory HOL-Imperative_HOL.Heap_Monad
22:46:34 Monad_Memo_DP: theory Monad_Memo_DP.Bottom_Up_Computation
22:46:34 Monad_Memo_DP: theory Monad_Memo_DP.Pair_Memory
22:46:34 Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Constructions
22:46:34 Probabilistic_Prime_Tests: theory HOL-Algebra.Order
22:46:34 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:46:34 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
22:46:34 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
22:46:34 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
22:46:34 Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Order_Relation
22:46:35 Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Arithmetic
22:46:35 Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
22:46:35 Expander_Graphs: theory VectorSpace.SumSpaces
22:46:35 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
22:46:35 Monad_Memo_DP: theory HOL-Imperative_HOL.Array
22:46:35 Collections_Examples: theory CAVA_Automata.Digraph_Basic
22:46:36 Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
22:46:36 Monad_Memo_DP: theory HOL-Imperative_HOL.Ref
22:46:36 Monad_Memo_DP: theory HOL-Imperative_HOL.Imperative_HOL
22:46:36 Monad_Memo_DP: theory Monad_Memo_DP.Heap_Monad_Ext
22:46:36 Monad_Memo_DP: theory Monad_Memo_DP.State_Heap
22:46:36 Expander_Graphs: theory Graph_Theory.Digraph_Component
22:46:36 Expander_Graphs: theory VectorSpace.VectorSpace
22:46:36 Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
22:46:36 Probabilistic_Prime_Tests: theory HOL-Algebra.Group
22:46:36 Monad_Memo_DP: theory Monad_Memo_DP.DP_CRelVH
22:46:37 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
22:46:37 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
22:46:37 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
22:46:37 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
22:46:37 Expander_Graphs: theory Regular-Sets.Regexp_Method
22:46:37 Monad_Memo_DP: theory Monad_Memo_DP.Bottom_Up_Computation_Heap
22:46:37 Monad_Memo_DP: theory Monad_Memo_DP.Transform_Cmd
22:46:37 Monad_Memo_DP: theory Monad_Memo_DP.Memory_Heap
22:46:37 Monad_Memo_DP: theory Monad_Memo_DP.State_Main
22:46:38 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
22:46:38 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
22:46:38 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
22:46:38 Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
22:46:38 Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
22:46:38 Monad_Memo_DP: theory Monad_Memo_DP.Example_Misc
22:46:39 Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
22:46:39 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
22:46:39 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
22:46:39 Monad_Memo_DP: theory Monad_Memo_DP.Heap_Main
22:46:39 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
22:46:39 Expander_Graphs: theory Jordan_Normal_Form.Determinant
22:46:39 Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
22:46:40 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
22:46:40 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Left_Coset
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.SimpleGroups
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.SndIsomorphismGrp
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
22:46:40 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
22:46:40 Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
22:46:41 Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
22:46:41 Probabilistic_Prime_Tests: theory HOL-Algebra.Elementary_Groups
22:46:41 Expander_Graphs: theory Matrix.Ordered_Semiring
22:46:41 Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
22:46:41 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
22:46:41 Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
22:46:41 Probabilistic_Prime_Tests: theory HOL-Algebra.Product_Groups
22:46:41 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
22:46:42 Expander_Graphs: theory Matrix.Matrix_Legacy
22:46:42 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
22:46:42 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
22:46:42 Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups
22:46:42 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
22:46:42 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
22:46:42 Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
22:46:42 Probabilistic_Prime_Tests: theory HOL-Algebra.Module
22:46:42 Monad_Memo_DP: theory Monad_Memo_DP.Heap_Default
22:46:42 Monad_Memo_DP: theory Monad_Memo_DP.Tracing
22:46:43 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
22:46:43 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
22:46:43 Monad_Memo_DP: theory Monad_Memo_DP.Knapsack
22:46:43 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
22:46:44 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
22:46:44 Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
22:46:45 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
22:46:45 Running Gaussian_Integers (on of4.proof.cit.tum.de+0-3,12-15) ...
22:46:46 Collections_Examples: theory Containers.Containers_Generator
22:46:46 Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
22:46:46 Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
22:46:46 Collections_Examples: theory Containers.Collection_Enum
22:46:46 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers
22:46:47 Gaussian_Integers: theory Matrix.Utility
22:46:47 Gaussian_Integers: theory Polynomial_Factorization.Missing_List
22:46:47 Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
22:46:47 Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
22:46:48 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples
22:46:48 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares
22:46:48 Collections_Examples: theory Containers.Collection_Eq
22:46:48 Gaussian_Integers: theory Polynomial_Factorization.Missing_Multiset
22:46:48 Gaussian_Integers: theory Polynomial_Factorization.Prime_Factorization
22:46:49 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
22:46:49 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Test
22:46:49 Collections_Examples: theory Containers.DList_Set
22:46:49 Gaussian_Integers: theory Gaussian_Integers.Gaussian_Integers_Everything
22:46:49 Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
22:46:49 Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
22:46:50 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
22:46:50 Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
22:46:51 DOM_Components: theory DOM_Components.fancy_tabs
22:46:51 Collections_Examples: theory Containers.Set_Linorder
22:46:53 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
22:46:55 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
22:46:56 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
22:46:56 Expander_Graphs: theory QHLProver.Complex_Matrix
22:46:56 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
22:46:57 Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
22:46:59 Timing Gaussian_Integers (8 threads, 11.779s elapsed time, 47.345s cpu time, 3.571s GC time, factor 4.02)
22:46:59 Finished Gaussian_Integers (0:00:13 elapsed time, 0:00:49 cpu time, factor 3.67)
22:47:01 Monad_Memo_DP: theory HOL-Library.RBT
22:47:01 Monad_Memo_DP: theory HOL-Library.RBT_Mapping
22:47:02 Monad_Memo_DP: theory Monad_Memo_DP.Counting_Tiles
22:47:02 Three_Squares: theory Three_Squares.Residues_Properties
22:47:02 Monad_Memo_DP: theory Monad_Memo_DP.Longest_Common_Subsequence
22:47:02 Monad_Memo_DP: theory Monad_Memo_DP.CYK
22:47:02 Monad_Memo_DP: theory Monad_Memo_DP.OptBST
22:47:03 Monad_Memo_DP: theory Monad_Memo_DP.Bellman_Ford
22:47:03 Monad_Memo_DP: theory Monad_Memo_DP.Min_Ed_Dist0
22:47:09 Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility
22:47:09 Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings
22:47:09 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues
22:47:09 Running Furstenberg_Topology (on of4.proof.cit.tum.de+4-11) ...
22:47:10 PAC_Checker: theory PAC_Checker.PAC_More_Poly
22:47:10 Monad_Memo_DP: theory Monad_Memo_DP.All_Examples
22:47:11 Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
22:47:11 Furstenberg_Topology: theory HOL-Algebra.Congruence
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Cong
22:47:11 Furstenberg_Topology: theory HOL-Library.Power_By_Squaring
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Eratosthenes
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Fib
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Prime_Powers
22:47:11 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
22:47:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion
22:47:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
22:47:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss
22:47:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
22:47:11 Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
22:47:11 Furstenberg_Topology: theory HOL-Algebra.Order
22:47:11 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Mod_Exp
22:47:11 Furstenberg_Topology: theory HOL-Number_Theory.Totient
22:47:12 Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
22:47:12 Furstenberg_Topology: theory HOL-Algebra.Lattice
22:47:13 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
22:47:13 Furstenberg_Topology: theory HOL-Algebra.Complete_Lattice
22:47:13 Expander_Graphs: theory QHLProver.Gates
22:47:13 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
22:47:13 Timing DOM_Components (1 threads, 777.003s elapsed time, 809.604s cpu time, 50.412s GC time, factor 1.04)
22:47:13 Finished DOM_Components (0:13:20 elapsed time, 0:14:35 cpu time, factor 1.09)
22:47:14 Furstenberg_Topology: theory HOL-Algebra.Group
22:47:14 Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
22:47:15 Furstenberg_Topology: theory HOL-Algebra.Coset
22:47:15 Furstenberg_Topology: theory HOL-Algebra.FiniteProduct
22:47:16 Furstenberg_Topology: theory HOL-Algebra.Ring
22:47:16 Three_Squares: theory HOL-Number_Theory.Pocklington
22:47:16 Furstenberg_Topology: theory HOL-Algebra.Generated_Groups
22:47:17 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
22:47:17 Furstenberg_Topology: theory HOL-Algebra.Elementary_Groups
22:47:18 Furstenberg_Topology: theory HOL-Algebra.AbelCoset
22:47:18 Furstenberg_Topology: theory HOL-Algebra.Module
22:47:18 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
22:47:19 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
22:47:20 PAC_Checker: theory PAC_Checker.PAC_Specification
22:47:20 Furstenberg_Topology: theory HOL-Algebra.Ideal
22:47:21 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
22:47:21 Furstenberg_Topology: theory HOL-Algebra.RingHom
22:47:22 Furstenberg_Topology: theory HOL-Algebra.UnivPoly
22:47:24 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
22:47:24 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
22:47:25 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_Skeleton_Code
22:47:26 Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility
22:47:26 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
22:47:27 Furstenberg_Topology: theory HOL-Algebra.Multiplicative_Group
22:47:27 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
22:47:28 Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots
22:47:30 Furstenberg_Topology: theory HOL-Number_Theory.Residues
22:47:30 PAC_Checker: theory PAC_Checker.PAC_Polynomials
22:47:31 Running Stochastic_Matrices (on 10.195.8.42+0-7) ...
22:47:31 Furstenberg_Topology: theory HOL-Number_Theory.Euler_Criterion
22:47:31 Furstenberg_Topology: theory HOL-Number_Theory.Pocklington
22:47:31 Furstenberg_Topology: theory HOL-Number_Theory.Gauss
22:47:32 Furstenberg_Topology: theory HOL-Number_Theory.Quadratic_Reciprocity
22:47:32 Furstenberg_Topology: theory HOL-Number_Theory.Residue_Primitive_Roots
22:47:32 Furstenberg_Topology: theory HOL-Number_Theory.Number_Theory
22:47:32 Collections_Examples: theory Containers.Collection_Order
22:47:33 Furstenberg_Topology: theory Furstenberg_Topology.Furstenberg_Topology
22:47:35 Stochastic_Matrices: theory HOL-Eisbach.Eisbach
22:47:36 PAC_Checker: theory PAC_Checker.PAC_Checker_Specification
22:47:36 Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
22:47:36 Collections_Examples: theory Containers.RBT_ext
22:47:37 Three_Squares: theory HOL-Number_Theory.Number_Theory
22:47:38 Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
22:47:39 Three_Squares: theory Bernoulli.Bernoulli_FPS
22:47:42 Collections_Examples: theory Deriving.RBT_Comparator_Impl
22:47:42 Stochastic_Matrices: theory HOL-Algebra.Congruence
22:47:42 Timing Furstenberg_Topology (8 threads, 28.392s elapsed time, 152.435s cpu time, 19.414s GC time, factor 5.37)
22:47:42 Finished Furstenberg_Topology (0:00:32 elapsed time, 0:02:43 cpu time, factor 5.06)
22:47:44 Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions
22:47:44 Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
22:47:44 Timing Monad_Memo_DP (8 threads, 55.662s elapsed time, 359.785s cpu time, 29.877s GC time, factor 6.46)
22:47:44 Finished Monad_Memo_DP (0:01:13 elapsed time, 0:06:40 cpu time, factor 5.45)
22:47:49 Stochastic_Matrices: theory HOL-Algebra.Order
22:47:51 Transition_Systems_and_Automata: theory Gabow_SCC.Gabow_GBG_Code
22:47:52 Stochastic_Matrices: theory HOL-Algebra.Lattice
22:47:52 Building Group-Ring-Module (on of4.proof.cit.tum.de+0-3,12-15) ...
22:47:53 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
22:47:57 Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
22:47:58 Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
22:47:59 Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
22:48:00 Three_Squares: theory Dirichlet_Series.Multiplicative_Function
22:48:01 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
22:48:01 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
22:48:01 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
22:48:01 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
22:48:02 Three_Squares: theory Dirichlet_L.Dirichlet_Characters
22:48:02 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
22:48:04 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
22:48:04 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
22:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
22:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
22:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
22:48:05 Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
22:48:06 Timing HOL-ODE-ARCH-COMP (1 threads, 843.009s elapsed time, 906.065s cpu time, 98.897s GC time, factor 1.07)
22:48:06 Group-Ring-Module: theory Group-Ring-Module.Algebra1
22:48:06 Finished HOL-ODE-ARCH-COMP (0:14:07 elapsed time, 0:15:10 cpu time, factor 1.08)
22:48:06 Three_Squares: theory Dirichlet_Series.Dirichlet_Product
22:48:09 Group-Ring-Module: theory Group-Ring-Module.Algebra2
22:48:10 Stochastic_Matrices: theory HOL-Algebra.Group
22:48:11 Group-Ring-Module: theory Group-Ring-Module.Algebra3
22:48:11 Three_Squares: theory Dirichlet_Series.Dirichlet_Series
22:48:14 Group-Ring-Module: theory Group-Ring-Module.Algebra4
22:48:16 Running Polynomials (on of1.proof.cit.tum.de+0-7) ...
22:48:18 Polynomials: theory Deriving.Comparator
22:48:18 Polynomials: theory Deriving.Generator_Aux
22:48:18 Polynomials: theory HOL-Computational_Algebra.Factorial_Ring
22:48:18 Polynomials: theory Polynomials.More_Modules
22:48:18 Polynomials: theory Polynomials.MPoly_Type
22:48:18 Polynomials: theory Matrix.Utility
22:48:18 Polynomials: theory Open_Induction.Restricted_Predicates
22:48:18 Polynomials: theory Deriving.Derive_Manager
22:48:18 Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
22:48:18 Polynomials: theory Well_Quasi_Orders.Least_Enum
22:48:18 Polynomials: theory Show.Show
22:48:18 Polynomials: theory Polynomials.Polynomials
22:48:18 Polynomials: theory Well_Quasi_Orders.Almost_Full
22:48:18 Polynomials: theory Well_Quasi_Orders.Minimal_Elements
22:48:18 Group-Ring-Module: theory Group-Ring-Module.Algebra5
22:48:18 Polynomials: theory Polynomials.More_MPoly_Type
22:48:19 Polynomials: theory Polynomials.OAlist
22:48:19 Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
22:48:19 Polynomials: theory Show.Show_Instances
22:48:19 Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
22:48:20 Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
22:48:20 Polynomials: theory Polynomials.Utils
22:48:20 Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
22:48:20 Polynomials: theory Polynomials.Power_Products
22:48:21 Group-Ring-Module: theory Group-Ring-Module.Algebra6
22:48:22 Three_Squares: theory Dirichlet_Series.Moebius_Mu
22:48:22 Collections_Examples: theory Containers.RBT_Mapping2
22:48:23 Polynomials: theory Polynomials.NZM
22:48:23 Polynomials: theory Polynomials.Show_Polynomials
22:48:24 Polynomials: theory HOL-Computational_Algebra.Polynomial
22:48:25 Collections_Examples: theory Containers.RBT_Set2
22:48:25 Group-Ring-Module: theory Group-Ring-Module.Algebra7
22:48:25 Three_Squares: theory Dirichlet_Series.More_Totient
22:48:26 Three_Squares: theory Dirichlet_Series.Divisor_Count
22:48:26 Stochastic_Matrices: theory HOL-Algebra.Coset
22:48:27 Three_Squares: theory Dirichlet_Series.Liouville_Lambda
22:48:28 Group-Ring-Module: theory Group-Ring-Module.Algebra8
22:48:28 Polynomials: theory Polynomials.MPoly_Type_Univariate
22:48:28 Polynomials: theory Polynomials.MPoly_Type_Class
22:48:29 Polynomials: theory Polynomials.PP_Type
22:48:29 Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
22:48:29 Collections_Examples: theory HOL-Library.Uprod
22:48:29 Group-Ring-Module: theory Group-Ring-Module.Algebra9
22:48:30 Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
22:48:30 Three_Squares: theory Dirichlet_Series.Euler_Products
22:48:33 Three_Squares: theory Dirichlet_Series.Partial_Summation
22:48:33 Collections_Examples: theory Containers.TwoSat_Ex
22:48:35 Polynomials: theory Polynomials.MPoly_Type_Class_FMap
22:48:36 Three_Squares: theory Bernoulli.Bernoulli_Zeta
22:48:36 Polynomials: theory Polynomials.Quasi_PM_Power_Products
22:48:37 Collections_Examples: theory Containers.Set_Impl
22:48:37 Polynomials: theory Polynomials.MPoly_PM
22:48:38 Running Executable_Randomized_Algorithms (on 10.195.8.46+0-7) ...
22:48:41 Polynomials: theory Polynomials.OAlist_Poly_Mapping
22:48:42 Executable_Randomized_Algorithms: theory Flow_Networks.Graph
22:48:44 Polynomials: theory Polynomials.Term_Order
22:48:44 Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
22:48:45 PAC_Checker: theory PAC_Checker.PAC_Map_Rel
22:48:45 Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
22:48:47 Polynomials: theory Polynomials.MPoly_Type_Class_OAlist
22:48:47 Timing Probabilistic_Prime_Tests (8 threads, 133.168s elapsed time, 733.346s cpu time, 336.719s GC time, factor 5.51)
22:48:47 Finished Probabilistic_Prime_Tests (0:02:15 elapsed time, 0:12:18 cpu time, factor 5.45)
22:48:49 PAC_Checker: theory PAC_Checker.PAC_Assoc_Map_Rel
22:48:51 Stochastic_Matrices: theory HOL-Algebra.Ring
22:48:51 PAC_Checker: theory PAC_Checker.PAC_Polynomials_Term
22:48:51 Executable_Randomized_Algorithms: theory Flow_Networks.Network
22:50:39 *** Host "10.195.8.40": failed to work
22:50:39 *** Error
22:50:39 *** Host "10.195.8.30": failed to work
22:50:39 *** Error
22:50:39 *** Host "10.195.7.194": failed to work
22:50:39 *** Error
22:50:39 *** Host "10.195.8.49": failed to work
22:50:39 *** Error
22:50:39 *** Host "10.195.8.29": failed to work
22:50:39 *** Error
22:51:09 *** Host "10.195.8.46": failed to work
22:51:09 *** Error
22:51:09 *** Host "10.195.8.42": failed to work
22:51:09 *** Error
22:51:09 *** Host "10.195.8.11": failed to work
22:51:09 *** Error
22:51:39 *** Host "10.195.8.32": failed to work
22:51:39 *** Error
22:51:39 *** Host "10.195.6.179": failed to work
22:51:39 *** Error
00:42:26 Build timed out (after 200 minutes). Marking the build as failed.
00:42:26 Build was aborted
00:42:27 Started calculate disk usage of build
00:42:27 Finished Calculation of disk usage of build in 0 seconds
00:42:45 Started calculate disk usage of workspace
00:42:45 Finished Calculation of disk usage of workspace in 0 seconds
00:42:46 Finished: FAILURE