Started by upstream project "afp-repo" build number 160
[EnvInject] - Loading node environment variables.
Building remotely on worker4 (lrz-cloud) in workspace /media/data/jenkins/workspace/afp-repo-afp
[afp-repo-afp] $ hg showconfig paths.default
[afp-repo-afp] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
added 1 changesets with 2 changes to 2 files
(run 'hg update' to get a working copy)
[afp-repo-afp] $ hg update --clean --rev default
2 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp-repo-afp] $ hg log --rev . --template {node}
[afp-repo-afp] $ hg log --rev . --template {rev}
[afp] $ hg showconfig paths.default
pulling from https://bitbucket.org/isa-afp/afp-devel/
added 9 changesets with 109 changes to 72 files
(run 'hg update' to get a working copy)
[afp] $ hg update --clean --rev default
72 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp-repo-afp] $ /bin/sh -xe /tmp/hudson8633445860127951110.sh
Linux vm-10-155-208-91 3.16.0-4-amd64 #1 SMP Debian 3.16.7-ckt20-1+deb8u3 (2016-01-17) x86_64 GNU/Linux
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
+ /media/data/jenkins/workspace/afp-repo-afp/bin/isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ /media/data/jenkins/workspace/afp-repo-afp/bin/isabelle scala -J-Xmx4G -howtorun:script -nocompdaemon /media/data/jenkins/.isabelle/ci/ci_build.scala
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/ClockSynchInst (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/Completeness (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Algebra (main)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Pre_Polynomial_Factorization (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Pre_Algebraic_Numbers (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Sort_Encodings (AFP)
Session HOL/HOL-Imperative_HOL
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Library (main)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Descartes_Sign_Rule (AFP)
Session AFP/Efficient-Mergesort (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/MSO_Examples (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Regex_Equivalence_Examples (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session HOL/HOL-Multivariate_Analysis (main)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/SequentInvertibility (AFP)
Session AFP/Pratt_Certificate (AFP)
Session HOL/HOL-Old_Number_Theory
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HotelKeyCards (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/InformationFlowSlicing_Intra (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Koenigsberg_Friendship_Base
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Strong_Security (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Cleaning Well_Quasi_Orders ...
Cleaning WHATandWHERE_Security ...
Cleaning Vickrey_Clarke_Groves ...
Cleaning Transitive-Closure-II ...
Cleaning Tail_Recursive_Functions ...
Cleaning Special_Function_Bounds ...
Cleaning SequentInvertibility ...
Cleaning Separation_Logic_Imperative_HOL ...
Cleaning Separation_Algebra ...
Cleaning Selection_Heap_Sort ...
Cleaning SIFUM_Type_Systems ...
Cleaning SATSolverVerification ...
Cleaning Roy_Floyd_Warshall ...
Cleaning Robbins-Conjecture ...
Cleaning Regex_Equivalence ...
Cleaning Regex_Equivalence_Examples ...
Cleaning RefinementReactive ...
Cleaning Recursion-Theory-I ...
Cleaning Rank_Nullity_Theorem ...
Cleaning Random_Graph_Subgraph_Threshold ...
Cleaning Program-Conflict-Analysis ...
Cleaning Probabilistic_System_Zoo-Non_BNFs ...
Cleaning Probabilistic_System_Zoo-BNFs ...
Cleaning Probabilistic_System_Zoo ...
Cleaning Probabilistic_Noninterference ...
Cleaning Priority_Queue_Braun ...
Cleaning Prime_Harmonic_Series ...
Cleaning Presburger-Automata ...
Cleaning Possibilistic_Noninterference ...
Cleaning Polynomial_Interpolation ...
Cleaning Planarity_Certificates ...
Cleaning Perfect-Number-Thm ...
Cleaning Partial_Function_MR ...
Cleaning POPLmark-deBruijn ...
Cleaning Ordinary_Differential_Equations ...
Cleaning Ordinals_and_Cardinals ...
Cleaning Noninterference_Inductive_Unwinding ...
Cleaning Noninterference_CSP ...
Cleaning Noninterference_Ipurge_Unwinding ...
Cleaning Noninterference_Generic_Unwinding ...
Cleaning Max-Card-Matching ...
Cleaning MSO_Regex_Equivalence ...
Cleaning Lower_Semicontinuous ...
Cleaning Locally-Nameless-Sigma ...
Cleaning List_Interleaving ...
Cleaning Nat-Interval-Logic ...
Cleaning Liouville_Numbers ...
Cleaning LinearQuantifierElim ...
Cleaning Lifting_Definition_Option ...
Cleaning Pratt_Certificate ...
Cleaning LatticeProperties ...
Cleaning MonoBoolTranAlgebra ...
Cleaning Lam-ml-Normalization ...
Cleaning Stuttering_Equivalence ...
Cleaning Koenigsberg_Friendship ...
Cleaning Residuated_Lattices ...
Cleaning JiveDataStoreModel ...
Cleaning Jordan_Normal_Form ...
Cleaning Pre_Polynomial_Factorization ...
Cleaning Polynomial_Factorization ...
Cleaning Pre_Algebraic_Numbers ...
Cleaning Isabelle_Meta_Model ...
Cleaning InformationFlowSlicing_Intra ...
Cleaning Inductive_Confidentiality ...
Cleaning Impossible_Geometry ...
Cleaning Imperative_Insertion_Sort ...
Cleaning IEEE_Floating_Point ...
Cleaning HereditarilyFinite ...
Cleaning InformationFlowSlicing_Inter ...
Cleaning InformationFlowSlicing ...
Cleaning Group-Ring-Module ...
Cleaning Gauss-Jordan-Elim-Fun ...
Cleaning Functional-Automata ...
Cleaning Free-Boolean-Algebra ...
Cleaning Formula_Derivatives ...
Cleaning Formula_Derivatives-Examples ...
Cleaning FocusStreamsCaseStudies ...
Cleaning Finite_Automata_HF ...
Cleaning Featherweight_OCL ...
Cleaning FeatherweightJava ...
Cleaning Example-Submission ...
Cleaning Encodability_Process_Calculi ...
Cleaning Efficient-Mergesort ...
Cleaning Discrete_Summation ...
Cleaning Descartes_Sign_Rule ...
Cleaning Depth-First-Search ...
Cleaning Datatype_Order_Generator ...
Cleaning Old_Datatype_Show ...
Cleaning DataRefinementIBP ...
Cleaning CryptoBasedCompositionalProperties ...
Cleaning Containers-Benchmarks ...
Cleaning Consensus_Refined ...
Cleaning ComponentDependencies ...
Cleaning Compiling-Exceptions-Correctly ...
Cleaning Coinductive_Languages ...
Cleaning Stream_Fusion_Code ...
Cleaning Certification_Monads ...
Cleaning Card_Number_Partitions ...
Cleaning BytecodeLogicJmlTypes ...
Cleaning Bounded_Deducibility_Security ...
Cleaning Boolean_Expression_Checkers ...
Cleaning Automatic_Refinement ...
Cleaning CAVA_LTL_Modelchecker ...
Cleaning Collections_Examples ...
Cleaning Dijkstra_Shortest_Path ...
Cleaning Network_Security_Policy_Verification ...
Cleaning Transitive-Closure ...
Cleaning ArrowImpossibilityGS ...
Cleaning Applicative_Lifting ...
Cleaning Amortized_Complexity ...
Cleaning Algebraic_Numbers ...
Cleaning Affine_Arithmetic ...
Cleaning Abstract_Completeness ...
Cleaning Abstract-Rewriting ...
Cleaning Decreasing-Diagrams ...
Cleaning Decreasing-Diagrams-II ...
Cleaning Abstract-Hoare-Logics ...
Cleaning Abortable_Linearizable_Modules ...
Building Abstract-Rewriting ...
Abstract-Rewriting: theory Regular_Set
Abstract-Rewriting: theory While_Combinator
Kleene_Algebra: theory Signatures
Abstract-Rewriting: theory Regular_Exp
Abstract-Rewriting: theory NDerivative
Abstract-Rewriting: theory Relation_Interpretation
Abstract-Rewriting: theory Equivalence_Checking
Abstract-Rewriting: theory Regexp_Method
Kleene_Algebra: theory Dioid_Models
Kleene_Algebra: theory Finite_Suprema
Abstract-Rewriting: theory Infinite_Set
Kleene_Algebra: theory Inf_Matrix
Abstract-Rewriting: theory Seq
Abstract-Rewriting: theory Abstract_Rewriting
Abstract-Rewriting: theory Relative_Rewriting
Abstract-Rewriting: theory SN_Orders
Abstract-Rewriting: theory SN_Order_Carrier
Kleene_Algebra: theory Kleene_Algebra
Kleene_Algebra: theory Omega_Algebra
Kleene_Algebra: theory Kleene_Algebra_Models
Kleene_Algebra: theory Formal_Power_Series
Kleene_Algebra: theory PHL_DRA
Kleene_Algebra: theory Omega_Algebra_Models
Timing Abstract-Rewriting (4 threads, 43.385s elapsed time, 130.660s cpu time, 3.652s GC time, factor 3.01)
Finished Abstract-Rewriting (0:01:21 elapsed time, 0:02:53 cpu time, factor 2.13)
Coinductive: theory Prefix_Order
Coinductive: theory Norm_Arith
Coinductive: theory Euclidean_Space
Coinductive: theory Linear_Algebra
Timing Kleene_Algebra (4 threads, 51.713s elapsed time, 122.288s cpu time, 4.008s GC time, factor 2.36)
Finished Kleene_Algebra (0:01:35 elapsed time, 0:02:45 cpu time, factor 1.74)
Coinductive: theory Topology_Euclidean_Space
Jinja: theory Code_Abstract_Nat
Jinja: theory While_Combinator
Jinja: theory Code_Target_Numeral
Jinja: theory Transitive_Closure_Table
Coinductive: theory Extended_Real_Limits
Jinja: theory Typing_Framework
Jinja: theory Typing_Framework_err
Coinductive: theory Resumption
Coinductive: theory Coinductive_Nat
Jinja: theory execute_WellType
Coinductive: theory Coinductive_List
Coinductive: theory CCPO_Topology
Coinductive: theory Coinductive_List_Prefix
Coinductive: theory Hamming_Stream
Coinductive: theory Koenigslemma
Coinductive: theory Lazy_LList
Coinductive: theory Quotient_Coinductive_List
Coinductive: theory Coinductive_Stream
Coinductive: theory LList_CCPO_Topology
Coinductive: theory Lazy_TLList
Coinductive: theory Quotient_TLList
Coinductive: theory TLList_CCPO
Coinductive: theory TLList_CCPO_Examples
Coinductive: theory Coinductive
Coinductive: theory Coinductive_Examples
Timing Coinductive (4 threads, 99.898s elapsed time, 327.204s cpu time, 7.192s GC time, factor 3.28)
Finished Coinductive (0:02:47 elapsed time, 0:06:56 cpu time, factor 2.48)
Simpl: theory DistinctTreeProver
Simpl: theory StateSpaceLocale
Simpl: theory StateSpaceSyntax
Simpl: theory HoarePartialProps
Simpl: theory AlternativeSmallStep
Timing Simpl (4 threads, 122.498s elapsed time, 421.584s cpu time, 17.344s GC time, factor 3.44)
Finished Simpl (0:03:32 elapsed time, 0:08:31 cpu time, factor 2.41)
Deriving: theory More_Bits_Int
Deriving: theory Code_Target_Bits_Int
Deriving: theory Code_Target_ICF
Deriving: theory Derive_Manager
Deriving: theory Generator_Aux
Deriving: theory Countable_Generator
Deriving: theory Equality_Generator
Deriving: theory Hash_Generator
Deriving: theory Equality_Instances
Deriving: theory Comparator_Generator
Deriving: theory RBT_Comparator_Impl
Deriving: theory Hash_Instances
Deriving: theory RBT_Compare_Order_Impl
Deriving: theory Compare_Generator
Deriving: theory Compare_Instances
Deriving: theory Compare_Order_Instances
Deriving: theory Derive_Examples
Timing Jinja (4 threads, 298.462s elapsed time, 1109.560s cpu time, 20.592s GC time, factor 3.72)
Finished Jinja (0:07:09 elapsed time, 0:20:40 cpu time, factor 2.89)
Timing Deriving (4 threads, 46.874s elapsed time, 89.404s cpu time, 3.784s GC time, factor 1.91)
Finished Deriving (0:01:57 elapsed time, 0:03:18 cpu time, factor 1.68)
Building LatticeProperties ...
LatticeProperties: theory Conj_Disj
LatticeProperties: theory Lattice_Prop
LatticeProperties: theory WellFoundedTransitive
LatticeProperties: theory Modular_Distrib_Lattice
LatticeProperties: theory Complete_Lattice_Prop
LatticeProperties: theory Lattice_Ordered_Group
Timing LatticeProperties (4 threads, 5.300s elapsed time, 13.500s cpu time, 0.232s GC time, factor 2.55)
Finished LatticeProperties (0:00:24 elapsed time, 0:00:32 cpu time, factor 1.32)
Building MSO_Regex_Equivalence ...
Timing LTL (4 threads, 30.229s elapsed time, 78.436s cpu time, 2.384s GC time, factor 2.59)
Finished LTL (0:01:25 elapsed time, 0:02:13 cpu time, factor 1.56)
MSO_Regex_Equivalence: theory Comparator
MSO_Regex_Equivalence: theory Derive_Manager
MSO_Regex_Equivalence: theory Generator_Aux
MSO_Regex_Equivalence: theory List_Index
MSO_Regex_Equivalence: theory List_More
MSO_Regex_Equivalence: theory Compare
MSO_Regex_Equivalence: theory Comparator_Generator
MSO_Regex_Equivalence: theory Compare_Generator
MSO_Regex_Equivalence: theory Compare_Instances
MSO_Regex_Equivalence: theory Pi_Regular_Set
MSO_Regex_Equivalence: theory Pi_Regular_Exp
HRB-Slicing: theory Postdomination
HRB-Slicing: theory ReturnAndCallNodes
HRB-Slicing: theory CFGExit_wf
HRB-Slicing: theory Observable
HRB-Slicing: theory SemanticsCFG
HRB-Slicing: theory WellFormProgs
HRB-Slicing: theory JVMInterpretation
HRB-Slicing: theory Interpretation
HRB-Slicing: theory WellFormed
HRB-Slicing: theory JVMPostdomination
HRB-Slicing: theory ValidPaths
HRB-Slicing: theory SCDObservable
HRB-Slicing: theory WeakSimulation
HRB-Slicing: theory FundamentalProperty
HRB-Slicing: theory HRBSlicing
MSO_Regex_Equivalence: theory Pi_Derivatives
MSO_Regex_Equivalence: theory Init_Normalization
MSO_Regex_Equivalence: theory Pi_Equivalence_Checking
MSO_Regex_Equivalence: theory PNormalization
MSO_Regex_Equivalence: theory Pi_Regular_Exp_Dual
MSO_Regex_Equivalence: theory Pi_Regular_Operators
MSO_Regex_Equivalence: theory Formula
MSO_Regex_Equivalence: theory M2L
MSO_Regex_Equivalence: theory M2L_Normalization
MSO_Regex_Equivalence: theory WS1S
MSO_Regex_Equivalence: theory WS1S_Normalization
MSO_Regex_Equivalence: theory M2L_Equivalence_Checking
MSO_Regex_Equivalence: theory WS1S_Equivalence_Checking
Timing HRB-Slicing (4 threads, 411.433s elapsed time, 1524.468s cpu time, 29.140s GC time, factor 3.71)
Finished HRB-Slicing (0:10:05 elapsed time, 0:28:38 cpu time, factor 2.84)
Slicing: theory DynDataDependence
Slicing: theory Postdomination
Slicing: theory DataDependence
Slicing: theory DynStandardControlDependence
Slicing: theory DynWeakControlDependence
Slicing: theory WeakControlDependence
Slicing: theory StandardControlDependence
Slicing: theory DependentLiveVariables
Slicing: theory WeakOrderDependence
Slicing: theory ControlDependenceRelations
Timing MSO_Regex_Equivalence (4 threads, 483.357s elapsed time, 1563.240s cpu time, 28.652s GC time, factor 3.23)
Finished MSO_Regex_Equivalence (0:10:20 elapsed time, 0:28:20 cpu time, factor 2.74)
Building Formula_Derivatives ...
Slicing: theory CDepInstantiations
Slicing: theory Interpretation
Slicing: theory AdditionalLemmas
Slicing: theory SemanticsWellFormed
Slicing: theory DynamicControlDependences
Slicing: theory StaticControlDependences
Formula_Derivatives: theory Coinductive_Language
Formula_Derivatives: theory Comparator
Formula_Derivatives: theory FSet_More
Formula_Derivatives: theory Derive_Manager
Formula_Derivatives: theory Generator_Aux
Formula_Derivatives: theory List_Index
Formula_Derivatives: theory While_Default
Slicing: theory JVMInterpretation
Formula_Derivatives: theory Compare
Formula_Derivatives: theory Comparator_Generator
Slicing: theory JVMPostdomination
Formula_Derivatives: theory Compare_Generator
Formula_Derivatives: theory Compare_Instances
Formula_Derivatives: theory Automaton
Formula_Derivatives: theory WS1S_Prelim
Formula_Derivatives: theory Abstract_Formula
Slicing: theory JVMControlDependences
Formula_Derivatives: theory Presburger_Formula
Formula_Derivatives: theory WS1S_Alt_Formula
Formula_Derivatives: theory WS1S_Formula
Formula_Derivatives: theory WS1S_Nameful
Formula_Derivatives: theory WS1S_Presburger_Equivalence
Timing Slicing (4 threads, 387.977s elapsed time, 1494.648s cpu time, 12.392s GC time, factor 3.85)
Finished Slicing (0:07:52 elapsed time, 0:26:18 cpu time, factor 3.34)
Echelon_Form: theory Code_Abstract_Nat
Echelon_Form: theory Dual_Order
Echelon_Form: theory Code_Target_Int
Echelon_Form: theory Code_Target_Nat
Echelon_Form: theory More_List
Echelon_Form: theory Code_Target_Numeral
Echelon_Form: theory Polynomial
Echelon_Form: theory Generalizations
Echelon_Form: theory IArray_Addenda
Echelon_Form: theory Square_Matrix
Echelon_Form: theory Miscellaneous
Echelon_Form: theory Cayley_Hamilton
Echelon_Form: theory Code_Matrix
Echelon_Form: theory Fundamental_Subspaces
Echelon_Form: theory Dim_Formula
Echelon_Form: theory Elementary_Operations
Echelon_Form: theory Matrix_To_IArray
Echelon_Form: theory Gauss_Jordan
Echelon_Form: theory Gauss_Jordan_IArrays
Echelon_Form: theory Linear_Maps
Echelon_Form: theory Gauss_Jordan_PA
Echelon_Form: theory Bases_Of_Fundamental_Subspaces
Echelon_Form: theory Determinants2
Echelon_Form: theory Gauss_Jordan_PA_IArrays
Echelon_Form: theory System_Of_Equations
Echelon_Form: theory Inverse_IArrays
Echelon_Form: theory Examples_Gauss_Jordan_Abstract
Timing Formula_Derivatives (4 threads, 367.119s elapsed time, 901.304s cpu time, 127.688s GC time, factor 2.46)
Finished Formula_Derivatives (0:08:34 elapsed time, 0:17:28 cpu time, factor 2.04)
Building Datatype_Order_Generator ...
Datatype_Order_Generator: theory More_Bits_Int
Datatype_Order_Generator: theory Bits_Integer
Datatype_Order_Generator: theory Word_Misc
Datatype_Order_Generator: theory Code_Target_Bits_Int
Datatype_Order_Generator: theory Code_Target_ICF
Datatype_Order_Generator: theory Uint32
Datatype_Order_Generator: theory HashCode
Datatype_Order_Generator: theory Derive_Manager
Datatype_Order_Generator: theory Derive_Aux
Datatype_Order_Generator: theory Countable_Generator
Datatype_Order_Generator: theory Order_Generator
Datatype_Order_Generator: theory Hash_Generator
Datatype_Order_Generator: theory Derive
Datatype_Order_Generator: theory Derive_Examples
Echelon_Form: theory Euclidean_Algorithm
Echelon_Form: theory Cayley_Hamilton_Compatible
Echelon_Form: theory Code_Cayley_Hamilton
Echelon_Form: theory Echelon_Form
Echelon_Form: theory Echelon_Form_Det
Echelon_Form: theory Echelon_Form_IArrays
Echelon_Form: theory Echelon_Form_Inverse
Echelon_Form: theory Echelon_Form_Det_IArrays
Echelon_Form: theory Examples_Echelon_Form_Abstract
Echelon_Form: theory Code_Cayley_Hamilton_IArrays
Echelon_Form: theory Echelon_Form_Inverse_IArrays
Echelon_Form: theory Examples_Echelon_Form_IArrays
Timing Echelon_Form (4 threads, 246.529s elapsed time, 821.640s cpu time, 15.344s GC time, factor 3.33)
Finished Echelon_Form (0:05:23 elapsed time, 0:14:48 cpu time, factor 2.75)
Building Group-Ring-Module ...
Group-Ring-Module: theory Algebra1
Group-Ring-Module: theory Algebra2
Group-Ring-Module: theory Algebra3
Group-Ring-Module: theory Algebra4
Group-Ring-Module: theory Algebra5
Group-Ring-Module: theory Algebra6
Group-Ring-Module: theory Algebra7
Group-Ring-Module: theory Algebra8
Group-Ring-Module: theory Algebra9
Timing Datatype_Order_Generator (4 threads, 188.388s elapsed time, 335.140s cpu time, 21.716s GC time, factor 1.78)
Finished Datatype_Order_Generator (0:06:11 elapsed time, 0:09:17 cpu time, factor 1.50)
Containers: theory Regular_Set
Containers: theory Regular_Exp
Containers: theory NDerivative
Containers: theory Relation_Interpretation
Containers: theory Equivalence_Checking
Containers: theory Regexp_Method
Containers: theory Extend_Partial_Order
Containers: theory List_Fusion
Containers: theory Closure_Set
Containers: theory Containers_Auxiliary
Containers: theory Card_Datatype
Containers: theory Containers_Generator
Containers: theory Collection_Enum
Containers: theory Collection_Eq
Containers: theory Lexicographic_Order
Containers: theory Set_Linorder
Containers: theory Collection_Order
Containers: theory List_Proper_Interval
Containers: theory RBT_Mapping2
Containers: theory Mapping_Impl
Containers: theory Map_To_Mapping
Containers: theory Containers_Userguide
Containers: theory Compatibility_Containers_Regular_Sets
Containers: theory Card_Datatype_Ex
Containers: theory Map_To_Mapping_Ex
Timing Group-Ring-Module (4 threads, 164.136s elapsed time, 596.740s cpu time, 14.672s GC time, factor 3.64)
Finished Group-Ring-Module (0:03:45 elapsed time, 0:10:58 cpu time, factor 2.92)
Graph_Theory: theory Nat_Bijection
Graph_Theory: theory Infinite_Set
Graph_Theory: theory Old_Datatype
Graph_Theory: theory Liminf_Limsup
Graph_Theory: theory Countable
Graph_Theory: theory Countable_Set
Graph_Theory: theory Countable_Complete_Lattices
Graph_Theory: theory Order_Continuity
Graph_Theory: theory Extended_Nat
Graph_Theory: theory Extended_Real
Graph_Theory: theory Permutations
Graph_Theory: theory Rtrancl_On
Graph_Theory: theory Bidirected_Digraph
Graph_Theory: theory Vertex_Walk
Graph_Theory: theory Pair_Digraph
Graph_Theory: theory Weighted_Graph
Graph_Theory: theory Shortest_Path
Graph_Theory: theory Digraph_Component
Graph_Theory: theory Digraph_Component_Vwalk
Graph_Theory: theory Digraph_Isomorphism
Graph_Theory: theory Subdivision
Graph_Theory: theory Kuratowski
Graph_Theory: theory Graph_Theory
Timing Containers (4 threads, 110.531s elapsed time, 306.740s cpu time, 10.580s GC time, factor 2.78)
Finished Containers (0:03:54 elapsed time, 0:07:15 cpu time, factor 1.86)
JNF-HOL-Lib: theory Lattice_Syntax
JNF-HOL-Lib: theory Order_Union
JNF-HOL-Lib: theory Adhoc_Overloading
JNF-HOL-Lib: theory Permutations
JNF-HOL-Lib: theory Code_Abstract_Nat
JNF-HOL-Lib: theory Code_Binary_Nat
JNF-HOL-Lib: theory Code_Target_Nat
JNF-HOL-Lib: theory Fraction_Field
JNF-HOL-Lib: theory Code_Target_Int
JNF-HOL-Lib: theory Code_Target_Numeral
JNF-HOL-Lib: theory Infinite_Set
JNF-HOL-Lib: theory List_lexord
JNF-HOL-Lib: theory Monad_Syntax
JNF-HOL-Lib: theory UniqueFactorization
JNF-HOL-Lib: theory Phantom_Type
JNF-HOL-Lib: theory Simps_Case_Conv
JNF-HOL-Lib: theory Cardinality
JNF-HOL-Lib: theory Polynomial
JNF-HOL-Lib: theory DAList_Multiset
JNF-HOL-Lib: theory Wellorder_Extension
JNF-HOL-Lib: theory While_Combinator
Timing Graph_Theory (4 threads, 77.588s elapsed time, 268.600s cpu time, 8.580s GC time, factor 3.46)
Finished Graph_Theory (0:02:01 elapsed time, 0:05:12 cpu time, factor 2.57)
JNF-HOL-Lib: theory Fundamental_Theorem_Algebra
Lehmer: theory Multiplicative_Group
Timing Lehmer (4 threads, 58.488s elapsed time, 136.224s cpu time, 5.172s GC time, factor 2.33)
Finished Lehmer (0:01:35 elapsed time, 0:02:52 cpu time, factor 1.80)
Building Regex_Equivalence ...
Regex_Equivalence: theory Efficient_Sort
Regex_Equivalence: theory Regular_Set
Regex_Equivalence: theory Regular_Exp
Regex_Equivalence: theory Derivatives
Regex_Equivalence: theory NDerivative
Regex_Equivalence: theory Derivatives_Finite
Regex_Equivalence: theory Automaton
Regex_Equivalence: theory Position_Autos
Regex_Equivalence: theory After2
Regex_Equivalence: theory Before2
Regex_Equivalence: theory Deriv_PDeriv
Regex_Equivalence: theory Deriv_Autos
Timing JNF-HOL-Lib (4 threads, 70.748s elapsed time, 253.388s cpu time, 7.636s GC time, factor 3.58)
Finished JNF-HOL-Lib (0:02:21 elapsed time, 0:05:23 cpu time, factor 2.29)
JNF-AFP-Lib: theory Comparator
JNF-AFP-Lib: theory Derive_Manager
JNF-AFP-Lib: theory Extend_Partial_Order
JNF-AFP-Lib: theory Closure_Set
JNF-AFP-Lib: theory FunctionLemmas
JNF-AFP-Lib: theory Generator_Aux
JNF-AFP-Lib: theory IArray_Addenda
JNF-AFP-Lib: theory Equality_Generator
JNF-AFP-Lib: theory IArray_Haskell
JNF-AFP-Lib: theory List_Fusion
JNF-AFP-Lib: theory Containers_Auxiliary
JNF-AFP-Lib: theory Equality_Instances
JNF-AFP-Lib: theory Regular_Set
Regex_Equivalence: theory Regex_Equivalence
JNF-AFP-Lib: theory Containers_Generator
JNF-AFP-Lib: theory Comparator_Generator
JNF-AFP-Lib: theory Collection_Enum
JNF-AFP-Lib: theory Lexicographic_Order
JNF-AFP-Lib: theory Compare_Generator
JNF-AFP-Lib: theory Set_Linorder
JNF-AFP-Lib: theory Collection_Eq
JNF-AFP-Lib: theory Compare_Instances
JNF-AFP-Lib: theory RBT_Comparator_Impl
JNF-AFP-Lib: theory Regular_Exp
JNF-AFP-Lib: theory RingModuleFacts
JNF-AFP-Lib: theory MonoidSums
JNF-AFP-Lib: theory LinearCombinations
JNF-AFP-Lib: theory NDerivative
JNF-AFP-Lib: theory Relation_Interpretation
JNF-AFP-Lib: theory Show_Instances
JNF-AFP-Lib: theory Euclidean_Algorithm
JNF-AFP-Lib: theory Missing_Unsorted
JNF-AFP-Lib: theory Collection_Order
JNF-AFP-Lib: theory Equivalence_Checking
JNF-AFP-Lib: theory Regexp_Method
JNF-AFP-Lib: theory Abstract_Rewriting
JNF-AFP-Lib: theory RBT_Mapping2
JNF-AFP-Lib: theory Relative_Rewriting
JNF-AFP-Lib: theory VectorSpace
JNF-AFP-Lib: theory Missing_Polynomial
JNF-AFP-Lib: theory Ordered_Semiring
JNF-AFP-Lib: theory SN_Order_Carrier
Timing Regex_Equivalence (4 threads, 47.730s elapsed time, 160.132s cpu time, 5.452s GC time, factor 3.35)
Finished Regex_Equivalence (0:02:10 elapsed time, 0:04:07 cpu time, factor 1.90)
Building Automatic_Refinement ...
Automatic_Refinement: theory Foldi
Automatic_Refinement: theory Infinite_Set
Automatic_Refinement: theory Multiset
Automatic_Refinement: theory Option_ord
Automatic_Refinement: theory Prio_List
Automatic_Refinement: theory Product_Lexorder
Automatic_Refinement: theory Refine_Util
Automatic_Refinement: theory Omega_Words_Fun
Automatic_Refinement: theory Anti_Unification
Automatic_Refinement: theory Attr_Comb
Automatic_Refinement: theory Mk_Term_Antiquot
Automatic_Refinement: theory Named_Sorted_Thms
Automatic_Refinement: theory Mpat_Antiquot
Automatic_Refinement: theory Tagged_Solver
Automatic_Refinement: theory Select_Solve
Automatic_Refinement: theory Indep_Vars
Automatic_Refinement: theory Mk_Record_Simp
Automatic_Refinement: theory List_More
Automatic_Refinement: theory Quicksort
Automatic_Refinement: theory Misc
Automatic_Refinement: theory Digraph_Basic
Automatic_Refinement: theory Refine_Lib
Automatic_Refinement: theory Param_Chapter
Automatic_Refinement: theory Relators
Automatic_Refinement: theory Param_Tool
Automatic_Refinement: theory Param_HOL
Automatic_Refinement: theory Parametricity
Automatic_Refinement: theory Autoref_Data
Automatic_Refinement: theory Autoref_Tagging
Automatic_Refinement: theory Autoref_Phases
Automatic_Refinement: theory Autoref_Id_Ops
Automatic_Refinement: theory Autoref_Fix_Rel
Automatic_Refinement: theory Autoref_Translate
Automatic_Refinement: theory Autoref_Relator_Interface
Automatic_Refinement: theory Autoref_Gen_Algo
Automatic_Refinement: theory Autoref_Chapter
Automatic_Refinement: theory Autoref_Tool
Automatic_Refinement: theory Autoref_Bindings_HOL
Automatic_Refinement: theory Automatic_Refinement
Timing Automatic_Refinement (4 threads, 44.506s elapsed time, 139.140s cpu time, 3.732s GC time, factor 3.13)
Finished Automatic_Refinement (0:01:18 elapsed time, 0:02:54 cpu time, factor 2.22)
Refine_Monadic: theory Lattice_Syntax
Refine_Monadic: theory Adhoc_Overloading
Refine_Monadic: theory Boolean_Algebra
Refine_Monadic: theory Misc_Numeric
Refine_Monadic: theory Bit_Representation
Refine_Monadic: theory Misc_Typedef
Refine_Monadic: theory Monad_Syntax
Refine_Monadic: theory Phantom_Type
Refine_Monadic: theory While_Combinator
Refine_Monadic: theory Bits_Bit
Refine_Monadic: theory Bits_Int
Refine_Monadic: theory Word_Miscellaneous
Refine_Monadic: theory Cardinality
Refine_Monadic: theory Numeral_Type
Refine_Monadic: theory Bool_List_Representation
Refine_Monadic: theory Type_Length
Refine_Monadic: theory Example_Chapter
Refine_Monadic: theory Refine_Mono_Prover
Refine_Monadic: theory Refine_Chapter
Refine_Monadic: theory Refine_Misc
Refine_Monadic: theory RefineG_Domain
Refine_Monadic: theory RefineG_Transfer
Refine_Monadic: theory RefineG_Assert
Refine_Monadic: theory RefineG_Recursion
Refine_Monadic: theory Refine_Basic
Refine_Monadic: theory RefineG_While
Refine_Monadic: theory Refine_Det
Refine_Monadic: theory Refine_Heuristics
Refine_Monadic: theory Refine_Leof
Refine_Monadic: theory Refine_Pfun
Refine_Monadic: theory Refine_While
Refine_Monadic: theory Refine_Transfer
Refine_Monadic: theory Autoref_Monadic
Refine_Monadic: theory Refine_Automation
Refine_Monadic: theory Refine_Foreach
Refine_Monadic: theory Refine_Monadic
Refine_Monadic: theory Breadth_First_Search
Refine_Monadic: theory WordRefine
Refine_Monadic: theory Examples
Timing JNF-AFP-Lib (4 threads, 141.805s elapsed time, 500.920s cpu time, 16.348s GC time, factor 3.53)
Finished JNF-AFP-Lib (0:04:15 elapsed time, 0:10:19 cpu time, factor 2.42)
Building Pre_Polynomial_Factorization ...
Pre_Polynomial_Factorization: theory Divmod_Int
Pre_Polynomial_Factorization: theory Missing_Ring
Pre_Polynomial_Factorization: theory Partial_Function_MR
Pre_Polynomial_Factorization: theory RBT
Pre_Polynomial_Factorization: theory Improved_Code_Equations
Pre_Polynomial_Factorization: theory Neville_Aitken_Interpolation
Timing Refine_Monadic (4 threads, 44.074s elapsed time, 151.420s cpu time, 4.672s GC time, factor 3.44)
Finished Refine_Monadic (0:01:30 elapsed time, 0:03:14 cpu time, factor 2.16)
Pre_Polynomial_Factorization: theory Show_Poly
Pre_Polynomial_Factorization: theory RBT_Mapping
Pre_Polynomial_Factorization: theory Lagrange_Interpolation
Pre_Polynomial_Factorization: theory CauchysMeanTheorem
Pre_Polynomial_Factorization: theory Sqrt_Babylonian_Auxiliary
Pre_Polynomial_Factorization: theory Missing_Fraction_Field
Pre_Polynomial_Factorization: theory Ring_Hom_Poly
Pre_Polynomial_Factorization: theory Is_Rat_To_Rat
Pre_Polynomial_Factorization: theory NthRoot_Impl
Collections: theory Code_Abstract_Nat
Collections: theory FingerTree
Collections: theory Code_Target_Int
Collections: theory BinomialHeap
Collections: theory Code_Target_Nat
Pre_Polynomial_Factorization: theory Sqrt_Babylonian
Collections: theory SkewBinomialHeap
Collections: theory Code_Target_Numeral
Pre_Polynomial_Factorization: theory Newton_Interpolation
Pre_Polynomial_Factorization: theory Matrix
Pre_Polynomial_Factorization: theory Polynomial_Interpolation
Pre_Polynomial_Factorization: theory Gauss_Jordan
Pre_Polynomial_Factorization: theory Matrix_IArray_Impl
Pre_Polynomial_Factorization: theory Gauss_Jordan_IArray_Impl
Collections: theory More_Bits_Int
Collections: theory Ord_Code_Preproc
Collections: theory Locale_Code
Collections: theory Partial_Equivalence_Relation
Collections: theory SetIterator
Collections: theory Record_Intf
Collections: theory Sorted_List_Operations
Collections: theory Bits_Integer
Collections: theory Idx_Iterator
Collections: theory SetIteratorOperations
Collections: theory Assoc_List
Collections: theory Proper_Iterator
Collections: theory Diff_Array
Collections: theory SetIteratorGA
Collections: theory Gen_Iterator
Collections: theory ICF_Spec_Base
Collections: theory Code_Target_Bits_Int
Collections: theory Code_Target_ICF
Collections: theory Locale_Code_Ex
Timing Pre_Polynomial_Factorization (4 threads, 58.045s elapsed time, 199.408s cpu time, 4.488s GC time, factor 3.44)
Finished Pre_Polynomial_Factorization (0:02:04 elapsed time, 0:04:23 cpu time, factor 2.12)
Building Polynomial_Factorization ...
Polynomial_Factorization: theory Missing_Multiset
Polynomial_Factorization: theory Precomputation
Polynomial_Factorization: theory Missing_List
Polynomial_Factorization: theory Order_Polynomial
Collections: theory SetAbstractionIterator
Polynomial_Factorization: theory Dvd_Int_Poly
Polynomial_Factorization: theory Explicit_Roots
Collections: theory GenCF_Chapter
Collections: theory GenCF_Gen_Chapter
Collections: theory GenCF_Impl_Chapter
Collections: theory GenCF_Intf_Chapter
Collections: theory Impl_Array_Stack
Collections: theory Array_Iterator
Collections: theory Impl_Cfun_Set
Collections: theory Impl_List_Set
Polynomial_Factorization: theory Prime_Factorization
Polynomial_Factorization: theory Gauss_Lemma
Collections: theory Impl_Array_Map
Collections: theory Impl_List_Map
Collections: theory Impl_RBT_Map
Collections: theory Gen_Map2Set
Collections: theory Impl_Array_Hash_Map
Polynomial_Factorization: theory Rational_Root_Test
Polynomial_Factorization: theory Kronecker_Factorization
Polynomial_Factorization: theory Unique_Factorization_Domain
Collections: theory Impl_Bit_Set
Polynomial_Factorization: theory Polynomial_Divisibility
Polynomial_Factorization: theory Square_Free_Factorization
Collections: theory Impl_Uv_Set
Polynomial_Factorization: theory Prime_Field
Polynomial_Factorization: theory Polynomial_Division
Polynomial_Factorization: theory Gauss_Jordan_Field
Polynomial_Factorization: theory Polynomial_Field
Polynomial_Factorization: theory Berlekamp_Hensel_Factorization
Collections: theory ICF_Chapter
Collections: theory ICF_Impl_Chapter
Collections: theory ICF_Gen_Algo_Chapter
Collections: theory ICF_Spec_Chapter
Collections: theory AnnotatedListSpec
Collections: theory BinoPrioImpl
Collections: theory FTAnnotatedListImpl
Polynomial_Factorization: theory External_Factorization
Polynomial_Factorization: theory Factorization_Oracle
Polynomial_Factorization: theory Hybrid_Factorization
Collections: theory PrioByAnnotatedList
Collections: theory SkewPrioImpl
Polynomial_Factorization: theory Select_Berlekamp_Hensel_Factorization
Polynomial_Factorization: theory Select_Hybrid_Factorization
Polynomial_Factorization: theory Select_External_Factorization
Collections: theory PrioUniqueSpec
Polynomial_Factorization: theory Rational_Factorization
Collections: theory PrioUniqueByAnnotatedList
Collections: theory FTPrioImpl
Collections: theory FTPrioUniqueImpl
Collections: theory SetIteratorCollectionsGA
Collections: theory ArrayMapImpl
Collections: theory ListMapImpl
Collections: theory ListMapImpl_Invar
Collections: theory TrieMapImpl
Collections: theory RBTMapImpl
Collections: theory ListSetImpl
Collections: theory ListSetImpl_Invar
Collections: theory ListSetImpl_NotDist
Collections: theory ListSetImpl_Sorted
Collections: theory ArrayHashMap_Impl
Collections: theory HashMap_Impl
Collections: theory ArraySetImpl
Collections: theory TrieSetImpl
Collections: theory RBTSetImpl
Collections: theory ArrayHashMap
Collections: theory ArrayHashSet
Collections: theory MapStdImpl
Collections: theory SetStdImpl
Collections: theory ICF_Refine_Monadic
Collections: theory ICF_Autoref
Collections: theory ICF_Entrypoints_Chapter
Collections: theory Collections
Collections: theory CollectionsV1
Collections: theory Collections_Entrypoints_Chapter
Collections: theory Refine_Dflt_Only_ICF
Collections: theory Refine_Dflt
Collections: theory Refine_Dflt_ICF
Timing Polynomial_Factorization (4 threads, 75.419s elapsed time, 200.832s cpu time, 3.776s GC time, factor 2.66)
Finished Polynomial_Factorization (0:02:26 elapsed time, 0:04:31 cpu time, factor 1.86)
Building Pre_Algebraic_Numbers ...
Collections: theory Userguides_Chapter
Collections: theory ICF_Userguide
Collections: theory Refine_Monadic_Userguide
Pre_Algebraic_Numbers: theory Missing_Permutations
Pre_Algebraic_Numbers: theory Compare_Rat
Pre_Algebraic_Numbers: theory Compare_Real
Pre_Algebraic_Numbers: theory Show_Real
Pre_Algebraic_Numbers: theory Misc_Polynomial
Pre_Algebraic_Numbers: theory Show_Complex
Pre_Algebraic_Numbers: theory Column_Operations
Pre_Algebraic_Numbers: theory Show_Matrix
Pre_Algebraic_Numbers: theory Sturm_Library
Pre_Algebraic_Numbers: theory Sturm_Theorem
Pre_Algebraic_Numbers: theory Determinant
Pre_Algebraic_Numbers: theory Char_Poly
Pre_Algebraic_Numbers: theory Determinant_Impl
Timing Pre_Algebraic_Numbers (4 threads, 40.815s elapsed time, 152.912s cpu time, 2.128s GC time, factor 3.75)
Finished Pre_Algebraic_Numbers (0:01:33 elapsed time, 0:03:25 cpu time, factor 2.19)
Matrix: theory Ordered_Semiring
Matrix: theory Matrix_Comparison
Timing Matrix (4 threads, 36.716s elapsed time, 127.828s cpu time, 3.184s GC time, factor 3.48)
Finished Matrix (0:01:11 elapsed time, 0:02:42 cpu time, factor 2.28)
Matrix_Tensor: theory Matrix_Tensor
Timing Matrix_Tensor (4 threads, 41.482s elapsed time, 95.964s cpu time, 2.260s GC time, factor 2.31)
Finished Matrix_Tensor (0:01:05 elapsed time, 0:02:00 cpu time, factor 1.82)
Building Applicative_Lifting ...
Applicative_Lifting: theory Commutation
Applicative_Lifting: theory Function_Algebras
Applicative_Lifting: theory Free_Ultrafilter
Applicative_Lifting: theory Lambda
Applicative_Lifting: theory StarDef
Applicative_Lifting: theory Function_Division
Applicative_Lifting: theory ParRed
Applicative_Lifting: theory Eta
Applicative_Lifting: theory Applicative
Applicative_Lifting: theory Dlist
Applicative_Lifting: theory Joinable
Applicative_Lifting: theory Beta_Eta
Applicative_Lifting: theory Combinators
Applicative_Lifting: theory Applicative_Environment
Applicative_Lifting: theory Applicative_List
Applicative_Lifting: theory Applicative_Monoid
Applicative_Lifting: theory Applicative_Option
Applicative_Lifting: theory Applicative_Set
Applicative_Lifting: theory Applicative_State
Applicative_Lifting: theory Applicative_Sum
Applicative_Lifting: theory Applicative_Environment_Algebra
Applicative_Lifting: theory Applicative_DNEList
Applicative_Lifting: theory Applicative_Star
Applicative_Lifting: theory Idiomatic_Terms
Applicative_Lifting: theory Applicative_Stream
Applicative_Lifting: theory Tree_Relabelling
Applicative_Lifting: theory Applicative_PMF
Applicative_Lifting: theory Stream_Algebra
Applicative_Lifting: theory Applicative_Functor
Applicative_Lifting: theory Applicative_Examples
Applicative_Lifting: theory Abstract_AF
Applicative_Lifting: theory Applicative_Test
Timing Applicative_Lifting (4 threads, 34.362s elapsed time, 79.160s cpu time, 2.720s GC time, factor 2.30)
Finished Applicative_Lifting (0:01:23 elapsed time, 0:02:08 cpu time, factor 1.54)
Building InformationFlowSlicing_Inter ...
InformationFlowSlicing_Inter: theory NonInterferenceInter
Timing Collections (4 threads, 279.900s elapsed time, 792.496s cpu time, 36.064s GC time, factor 2.83)
Finished Collections (0:09:48 elapsed time, 0:19:35 cpu time, factor 2.00)
InformationFlowSlicing_Inter: theory LiftingInter
Sturm_Sequences: theory Sturm_Library_Document
Sturm_Sequences: theory Misc_Polynomial
Sturm_Sequences: theory Sturm_Library
Sturm_Sequences: theory Sturm_Theorem
Sturm_Sequences: theory Sturm_Method
Sturm_Sequences: theory Sturm_Ex
Timing InformationFlowSlicing_Inter (4 threads, 32.864s elapsed time, 102.284s cpu time, 4.292s GC time, factor 3.11)
Finished InformationFlowSlicing_Inter (0:01:16 elapsed time, 0:02:25 cpu time, factor 1.91)
List-Infinite: theory Util_NatInf
List-Infinite: theory Util_MinMax
List-Infinite: theory Util_Nat
List-Infinite: theory Util_Set
List-Infinite: theory Util_Div
List-Infinite: theory SetInterval2
Timing Sturm_Sequences (4 threads, 31.308s elapsed time, 108.752s cpu time, 1.180s GC time, factor 3.47)
Finished Sturm_Sequences (0:01:10 elapsed time, 0:02:28 cpu time, factor 2.09)
List-Infinite: theory InfiniteSet2
List-Infinite: theory SetIntervalCut
Relation_Algebra: theory More_Boolean_Algebra
Relation_Algebra: theory Relation_Algebra
List-Infinite: theory SetIntervalStep
List-Infinite: theory ListInf_Prefix
Relation_Algebra: theory Relation_Algebra_RTC
List-Infinite: theory ListInfinite
Relation_Algebra: theory Relation_Algebra_Tests
Relation_Algebra: theory Relation_Algebra_Vectors
Relation_Algebra: theory Relation_Algebra_Models
Relation_Algebra: theory Relation_Algebra_Functions
Relation_Algebra: theory Relation_Algebra_Direct_Products
Timing Relation_Algebra (4 threads, 19.599s elapsed time, 64.988s cpu time, 1.352s GC time, factor 3.32)
Finished Relation_Algebra (0:00:53 elapsed time, 0:01:38 cpu time, factor 1.85)
Timing List-Infinite (4 threads, 19.128s elapsed time, 68.444s cpu time, 2.020s GC time, factor 3.58)
Finished List-Infinite (0:01:02 elapsed time, 0:01:51 cpu time, factor 1.79)
Building Nat-Interval-Logic ...
Launchbury: theory AList-Utils
Launchbury: theory Mono-Nat-Fun
Launchbury: theory HOLCF-Join-Classes
Launchbury: theory HOLCF-Utils
Launchbury: theory Nominal-Utils
Nat-Interval-Logic: theory IL_Interval
Launchbury: theory ValueSimilarity
Launchbury: theory AList-Utils-Nominal
Launchbury: theory Nominal-HOLCF
Launchbury: theory CValue-Nominal
Launchbury: theory Env-Nominal
Nat-Interval-Logic: theory IL_IntervalOperators
Launchbury: theory Value-Nominal
Launchbury: theory HeapSemantics
Nat-Interval-Logic: theory IL_TemporalOperators
Launchbury: theory AbstractDenotational
Launchbury: theory Substitution
Launchbury: theory Abstract-Denotational-Props
Launchbury: theory Denotational
Launchbury: theory ResourcedDenotational
Launchbury: theory CorrectnessOriginal
Launchbury: theory Denotational-Related
Launchbury: theory CorrectnessResourced
Launchbury: theory ResourcedAdequacy
Launchbury: theory EverythingAdequacy
Timing Nat-Interval-Logic (4 threads, 33.116s elapsed time, 90.392s cpu time, 1.328s GC time, factor 2.73)
Finished Nat-Interval-Logic (0:01:11 elapsed time, 0:02:08 cpu time, factor 1.80)
CAVA_Base: theory Derive_Manager
CAVA_Base: theory Generator_Aux
CAVA_Base: theory Nat_Bijection
CAVA_Base: theory Equality_Generator
CAVA_Base: theory Old_Datatype
CAVA_Base: theory Equality_Instances
CAVA_Base: theory Hash_Generator
CAVA_Base: theory Comparator_Generator
CAVA_Base: theory Hash_Instances
CAVA_Base: theory CAVA_Code_Target
CAVA_Base: theory Compare_Generator
CAVA_Base: theory Compare_Instances
CAVA_Base: theory All_Of_CAVA_Base
CAVA_Base: theory Countable_Generator
Timing Launchbury (4 threads, 41.306s elapsed time, 149.468s cpu time, 3.872s GC time, factor 3.62)
Finished Launchbury (0:01:31 elapsed time, 0:03:18 cpu time, factor 2.16)
Building Noninterference_CSP ...
Noninterference_CSP: theory CSPNoninterference
Noninterference_CSP: theory ClassicalNoninterference
Noninterference_CSP: theory GeneralizedNoninterference
Timing Noninterference_CSP (4 threads, 8.701s elapsed time, 30.544s cpu time, 0.372s GC time, factor 3.51)
Finished Noninterference_CSP (0:00:33 elapsed time, 0:00:55 cpu time, factor 1.65)
Building Noninterference_Ipurge_Unwinding ...
Noninterference_Ipurge_Unwinding: theory ListInterleaving
Noninterference_Ipurge_Unwinding: theory IpurgeUnwinding
Noninterference_Ipurge_Unwinding: theory DeterministicProcesses
Timing CAVA_Base (4 threads, 12.373s elapsed time, 33.460s cpu time, 1.112s GC time, factor 2.70)
Finished CAVA_Base (0:01:13 elapsed time, 0:01:34 cpu time, factor 1.29)
CAVA_Automata: theory Step_Conv
CAVA_Automata: theory Automata
CAVA_Automata: theory Digraph_Impl
Timing Noninterference_Ipurge_Unwinding (4 threads, 14.198s elapsed time, 43.220s cpu time, 1.020s GC time, factor 3.04)
Finished Noninterference_Ipurge_Unwinding (0:00:38 elapsed time, 0:01:07 cpu time, factor 1.75)
Building Discrete_Summation ...
Discrete_Summation: theory Stirling
Discrete_Summation: theory Summation
Discrete_Summation: theory Factorials
Discrete_Summation: theory Summation_Conversion
Discrete_Summation: theory Examples
CAVA_Automata: theory Simulation
CAVA_Automata: theory Stuttering_Extension
Timing Discrete_Summation (4 threads, 4.758s elapsed time, 16.756s cpu time, 0.164s GC time, factor 3.52)
Finished Discrete_Summation (0:00:24 elapsed time, 0:00:36 cpu time, factor 1.48)
CAVA_Automata: theory Automata_Impl
Timing Lazy-Lists-II (4 threads, 3.595s elapsed time, 13.148s cpu time, 0.232s GC time, factor 3.66)
Finished Lazy-Lists-II (0:00:42 elapsed time, 0:00:52 cpu time, factor 1.22)
Cauchy: theory CauchysMeanTheorem
CAVA_Automata: theory All_Of_CAVA_Automata
Timing Cauchy (4 threads, 4.387s elapsed time, 17.624s cpu time, 0.192s GC time, factor 4.02)
Finished Cauchy (0:00:22 elapsed time, 0:00:35 cpu time, factor 1.58)
Sqrt_Babylonian: theory Sqrt_Babylonian_Auxiliary
Sqrt_Babylonian: theory NthRoot_Impl
Sqrt_Babylonian: theory Sqrt_Babylonian
Timing Sqrt_Babylonian (4 threads, 15.539s elapsed time, 43.100s cpu time, 0.544s GC time, factor 2.77)
Finished Sqrt_Babylonian (0:00:35 elapsed time, 0:01:02 cpu time, factor 1.78)
Timing Marriage (4 threads, 4.488s elapsed time, 12.204s cpu time, 0.080s GC time, factor 2.72)
Finished Marriage (0:00:22 elapsed time, 0:00:30 cpu time, factor 1.34)
Timing CAVA_Automata (4 threads, 102.659s elapsed time, 169.704s cpu time, 6.000s GC time, factor 1.65)
Finished CAVA_Automata (0:02:54 elapsed time, 0:04:06 cpu time, factor 1.41)
Algebraic_Numbers: theory Binary_Exponentiation
Algebraic_Numbers: theory Compare_Complex
Algebraic_Numbers: theory Bivariate_Polynomials
Algebraic_Numbers: theory Complex_Roots_Real_Poly
Algebraic_Numbers: theory Algebraic_Numbers_Prelim
Algebraic_Numbers: theory Unique_Factorization_Poly
Algebraic_Numbers: theory Sturm_Rat
Algebraic_Numbers: theory Resultant
LTL_to_GBA: theory StutterEquivalence
Algebraic_Numbers: theory Algebraic_Numbers
Algebraic_Numbers: theory Real_Algebraic_Numbers
LTL_to_GBA: theory Countable_Set
LTL_to_GBA: theory LTL_Stutter
LTL_to_GBA: theory Countable_Complete_Lattices
LTL_to_GBA: theory Order_Continuity
LTL_to_GBA: theory Extended_Nat
LTL_to_GBA: theory LTL_Rewrite
Algebraic_Numbers: theory Real_Roots
Algebraic_Numbers: theory Show_Real_Alg
Algebraic_Numbers: theory Show_Real_Approx
Algebraic_Numbers: theory Complex_Algebraic_Numbers
Algebraic_Numbers: theory Real_Factorization
LTL_to_GBA: theory LTL_to_GBA_impl
Algebraic_Numbers: theory Show_Real_Precise
Algebraic_Numbers: theory Algebraic_Number_Tests
LTL_to_GBA: theory All_Of_LTL_to_GBA
Timing LTL_to_GBA (4 threads, 219.841s elapsed time, 765.976s cpu time, 14.820s GC time, factor 3.48)
Finished LTL_to_GBA (0:05:34 elapsed time, 0:14:45 cpu time, factor 2.65)
CAVA_buildchain1: theory Find_Path
CAVA_buildchain1: theory Gabow_Skeleton
CAVA_buildchain1: theory Find_Path_Impl
CAVA_buildchain1: theory Gabow_SCC
CAVA_buildchain1: theory Gabow_GBG
CAVA_buildchain1: theory Gabow_Skeleton_Code
CAVA_buildchain1: theory Gabow_GBG_Code
CAVA_buildchain1: theory Gabow_SCC_Code
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/CAVA_buildchain1)
0.047s elapsed time, 0.048s cpu time, 0.000s GC time
0.040s elapsed time, 0.040s cpu time, 0.000s GC time
0.000s elapsed time, 0.000s cpu time, 0.000s GC time
0.648s elapsed time, 0.648s cpu time, 0.000s GC time
1.124s elapsed time, 1.124s cpu time, 0.000s GC time
0.735s elapsed time, 0.736s cpu time, 0.000s GC time
1.026s elapsed time, 1.028s cpu time, 0.000s GC time
0.000s elapsed time, 0.000s cpu time, 0.000s GC time
Failed to identify: op_map_lookup
0.022s elapsed time, 0.024s cpu time, 0.000s GC time
0.101s elapsed time, 0.100s cpu time, 0.000s GC time
0.076s elapsed time, 0.076s cpu time, 0.000s GC time
0.034s elapsed time, 0.036s cpu time, 0.000s GC time
### 94.988s elapsed time, 200.484s cpu time, 4.684s GC time
*** Failed to load theory "All_Of_Gabow_SCC" (unresolved "Gabow_GBG_Code")
*** exception Thread "Unable to allocate thread stack" raised (line 83 of "./basis/PolyMLException.sml")
*** At command "export_code" (line 320 of "~~/afp/thys/Gabow_SCC/Gabow_GBG_Code.thy")
Incompleteness: theory Infinite_Set
Incompleteness: theory Multiset
Incompleteness: theory Nat_Bijection
Incompleteness: theory Old_Datatype
Incompleteness: theory Phantom_Type
Incompleteness: theory Cardinality
Incompleteness: theory Quotient_Syntax
Incompleteness: theory Quotient_Option
Incompleteness: theory Quotient_Product
Incompleteness: theory Ordinal
Incompleteness: theory Quotient_Set
Incompleteness: theory Quotient_List
Incompleteness: theory OrdArith
Incompleteness: theory Nominal2_Base
Incompleteness: theory Nominal2_Abs
Incompleteness: theory Nominal2_FCB
Incompleteness: theory Nominal2
Incompleteness: theory SyntaxN
Incompleteness: theory Predicates
Incompleteness: theory Coding_Predicates
Incompleteness: theory Functions
Incompleteness: theory Pf_Predicates
Incompleteness: theory Goedel_I
Incompleteness: theory II_Prelims
Incompleteness: theory Pseudo_Coding
Incompleteness: theory Goedel_II
Timing Algebraic_Numbers (4 threads, 607.543s elapsed time, 1441.620s cpu time, 278.328s GC time, factor 2.37)
Finished Algebraic_Numbers (0:10:15 elapsed time, 0:24:09 cpu time, factor 2.35)
Psi_Calculi: theory Subst_Term
Psi_Calculi: theory Close_Subst
Psi_Calculi: theory Structural_Congruence
Psi_Calculi: theory Simulation
Psi_Calculi: theory Bisimulation
Psi_Calculi: theory Sim_Struct_Cong
Psi_Calculi: theory Bisim_Pres
Psi_Calculi: theory Bisim_Struct_Cong
Psi_Calculi: theory Bisim_Subst
Psi_Calculi: theory Weak_Simulation
Psi_Calculi: theory Weak_Stat_Imp
Psi_Calculi: theory Weak_Stat_Imp_Pres
Psi_Calculi: theory Weak_Cong_Simulation
Psi_Calculi: theory Weak_Sim_Pres
Psi_Calculi: theory Weak_Bisimulation
Psi_Calculi: theory Weak_Cong_Sim_Pres
Psi_Calculi: theory Weak_Bisim_Pres
Psi_Calculi: theory Weak_Psi_Congruence
Psi_Calculi: theory Weak_Bisim_Struct_Cong
Psi_Calculi: theory Weaken_Transition
Psi_Calculi: theory Weak_Cong_Pres
Psi_Calculi: theory Weaken_Stat_Imp
Psi_Calculi: theory Weak_Cong_Struct_Cong
Psi_Calculi: theory Weaken_Simulation
Psi_Calculi: theory Weaken_Bisimulation
Psi_Calculi: theory Weak_Congruence
Psi_Calculi: theory Tau_Stat_Imp
Psi_Calculi: theory Tau_Laws_No_Weak
Psi_Calculi: theory Tau_Laws_Weak
Timing Psi_Calculi (4 threads, 495.627s elapsed time, 1803.432s cpu time, 40.716s GC time, factor 3.64)
Finished Psi_Calculi (0:08:19 elapsed time, 0:30:06 cpu time, factor 3.62)
Running Ordinary_Differential_Equations ...
Ordinary_Differential_Equations: theory Adhoc_Overloading
Ordinary_Differential_Equations: theory Code_Abstract_Nat
Ordinary_Differential_Equations: theory Dense_Linear_Order
Ordinary_Differential_Equations: theory Code_Target_Int
Ordinary_Differential_Equations: theory Monad_Syntax
Ordinary_Differential_Equations: theory Code_Target_Nat
Ordinary_Differential_Equations: theory Multiset
Ordinary_Differential_Equations: theory Quotient_Syntax
Ordinary_Differential_Equations: theory Quotient_Set
Ordinary_Differential_Equations: theory Code_Target_Numeral
Ordinary_Differential_Equations: theory Lattice_Algebras
Ordinary_Differential_Equations: theory Counterclockwise
Ordinary_Differential_Equations: theory Counterclockwise_Vector
Ordinary_Differential_Equations: theory Counterclockwise_2D_Strict
Ordinary_Differential_Equations: theory Counterclockwise_2D_Arbitrary
Ordinary_Differential_Equations: theory Polygon
Ordinary_Differential_Equations: theory Euclidean_Space_Explicit
Ordinary_Differential_Equations: theory While_Combinator
Ordinary_Differential_Equations: theory Permutation
Ordinary_Differential_Equations: theory Affine_Form
Timing Incompleteness (4 threads, 617.631s elapsed time, 1990.816s cpu time, 15.168s GC time, factor 3.22)
Finished Incompleteness (0:10:25 elapsed time, 0:33:13 cpu time, factor 3.19)
Ordinary_Differential_Equations: theory Float
Ordinary_Differential_Equations: theory Approximation
Ordinary_Differential_Equations: theory Float_Real
Ordinary_Differential_Equations: theory Executable_Euclidean_Space
Ordinary_Differential_Equations: theory Affine_Approximation
Formal_SSA: theory List_lexord
Formal_SSA: theory RBT_Mapping
Formal_SSA: theory Postdomination
Formal_SSA: theory DynStandardControlDependence
Formal_SSA: theory DynWeakControlDependence
Formal_SSA: theory StandardControlDependence
Formal_SSA: theory WeakControlDependence
Formal_SSA: theory DynDataDependence
Formal_SSA: theory DataDependence
Formal_SSA: theory SemanticsCFG
Formal_SSA: theory WeakOrderDependence
Ordinary_Differential_Equations: theory Affine_Code
Ordinary_Differential_Equations: theory Ex_Affine_Approximation
Ordinary_Differential_Equations: theory Ex_Ineqs
Formal_SSA: theory CDepInstantiations
Formal_SSA: theory Interpretation
Ordinary_Differential_Equations: theory Intersection
Formal_SSA: theory AdditionalLemmas
Ordinary_Differential_Equations: theory Ex_Inter
Formal_SSA: theory Disjoin_Transform
Formal_SSA: theory FormalSSA_Misc
Formal_SSA: theory While_Combinator_Exts
Formal_SSA: theory Mapping_Exts
Formal_SSA: theory RBT_Mapping_Exts
Formal_SSA: theory Construct_SSA
Formal_SSA: theory SSA_CFG_code
Formal_SSA: theory Construct_SSA_notriv
Formal_SSA: theory SSA_Semantics
Formal_SSA: theory Construct_SSA_code
Formal_SSA: theory Construct_SSA_notriv_code
Formal_SSA: theory SSA_Transfer_Rules
Formal_SSA: theory Generic_Interpretation
Ordinary_Differential_Equations: theory Affine_Arithmetic
Formal_SSA: theory Generic_Extract
Formal_SSA: theory WhileGraphSSA
Ordinary_Differential_Equations: theory Optimize_Integer
Ordinary_Differential_Equations: theory Diagonal_Subsequence
Ordinary_Differential_Equations: theory Bounded_Linear_Operator
Ordinary_Differential_Equations: theory Print
Ordinary_Differential_Equations: theory ODE_Auxiliarities
Ordinary_Differential_Equations: theory Initial_Value_Problem
Ordinary_Differential_Equations: theory MVT_Ex
Ordinary_Differential_Equations: theory Multivariate_Taylor
Ordinary_Differential_Equations: theory Optimize_Float
Ordinary_Differential_Equations: theory One_Step_Method
Ordinary_Differential_Equations: theory Picard_Lindeloef_Qualitative
Ordinary_Differential_Equations: theory Flow
Ordinary_Differential_Equations: theory Runge_Kutta
Ordinary_Differential_Equations: theory Linear_ODE
Ordinary_Differential_Equations: theory Euler_Affine_Code
Ordinary_Differential_Equations: theory Euler_Affine
Ordinary_Differential_Equations: theory Example1
Ordinary_Differential_Equations: theory Example3
Ordinary_Differential_Equations: theory Example_Exp
Ordinary_Differential_Equations: theory Example_Oil
Ordinary_Differential_Equations: theory Example_van_der_Pol
Ordinary_Differential_Equations: theory Example_Variational_Equation
Ordinary_Differential_Equations: theory Examples
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations
Timing Formal_SSA (4 threads, 405.177s elapsed time, 966.816s cpu time, 15.332s GC time, factor 2.39)
Finished Formal_SSA (0:07:02 elapsed time, 0:16:17 cpu time, factor 2.31)
CAVA_LTL_Modelchecker CANCELLED
Native_Word: theory Code_Target_Int
Native_Word: theory More_Bits_Int
Native_Word: theory Bits_Integer
Timing Ordinary_Differential_Equations (4 threads, 449.307s elapsed time, 1622.912s cpu time, 36.940s GC time, factor 3.61)
Finished Ordinary_Differential_Equations (0:07:36 elapsed time, 0:27:07 cpu time, factor 3.56)
Promela: theory PromelaStatistics
Native_Word: theory Code_Target_Bits_Int
Native_Word: theory Native_Cast
Native_Word: theory Native_Word_Test
Promela: theory PromelaDatastructures
Native_Word: theory Native_Word_Test_Emu
Promela: theory PromelaInvariants
Native_Word: theory Native_Word_Test_GHC
Native_Word: theory Native_Word_Test_MLton2
Native_Word: theory Native_Word_Test_MLton
Native_Word: theory Native_Word_Test_OCaml2
Native_Word: theory Native_Word_Test_OCaml
Native_Word: theory Native_Word_Test_PolyML2
Native_Word: theory Native_Word_Test_PolyML
Native_Word: theory Native_Word_Test_Scala
Promela: theory PromelaLTLConv
Native_Word: theory Native_Word_Test_SMLNJ2
Native_Word: theory Native_Word_Test_SMLNJ
Native_Word: theory Uint_Userguide
Timing Native_Word (4 threads, 266.211s elapsed time, 251.680s cpu time, 6.540s GC time, factor 0.95)
Finished Native_Word (0:04:30 elapsed time, 0:11:34 cpu time, factor 2.57)
QR_Decomposition: theory Char_ord
QR_Decomposition: theory Code_Abstract_Nat
QR_Decomposition: theory Derive_Manager
QR_Decomposition: theory Dual_Order
QR_Decomposition: theory Code_Target_Nat
QR_Decomposition: theory Code_Char
QR_Decomposition: theory Code_Target_Int
QR_Decomposition: theory Primes
QR_Decomposition: theory Generator_Aux
QR_Decomposition: theory Code_Target_Numeral
QR_Decomposition: theory IArray
QR_Decomposition: theory Multiset
QR_Decomposition: theory Code_Bit
QR_Decomposition: theory Code_Set
Promela: theory All_Of_Promela
QR_Decomposition: theory CauchysMeanTheorem
QR_Decomposition: theory Code_Real_Approx_By_Float
QR_Decomposition: theory Show_Instances
QR_Decomposition: theory Show_Real
QR_Decomposition: theory Code_Real_Approx_By_Float_Haskell
QR_Decomposition: theory Mod_Type
QR_Decomposition: theory Generalizations
QR_Decomposition: theory Sqrt_Babylonian_Auxiliary
Timing Promela (4 threads, 248.805s elapsed time, 430.188s cpu time, 15.392s GC time, factor 1.73)
Finished Promela (0:04:24 elapsed time, 0:07:35 cpu time, factor 1.72)
Running Encodability_Process_Calculi ...
QR_Decomposition: theory NthRoot_Impl
QR_Decomposition: theory Miscellaneous
QR_Decomposition: theory UniqueFactorization
QR_Decomposition: theory Sqrt_Babylonian
Encodability_Process_Calculi: theory LaTeXsugar
Encodability_Process_Calculi: theory OptionalSugar
QR_Decomposition: theory Real_Impl
QR_Decomposition: theory Real_Impl_Auxiliary
QR_Decomposition: theory Prime_Product
Encodability_Process_Calculi: theory Relations
QR_Decomposition: theory Code_Matrix
QR_Decomposition: theory Fundamental_Subspaces
Encodability_Process_Calculi: theory ProcessCalculi
QR_Decomposition: theory Dim_Formula
QR_Decomposition: theory Elementary_Operations
QR_Decomposition: theory Real_Unique_Impl
QR_Decomposition: theory Gauss_Jordan
Encodability_Process_Calculi: theory Encodings
Encodability_Process_Calculi: theory SimulationRelations
QR_Decomposition: theory Linear_Maps
Encodability_Process_Calculi: theory SourceTargetRelation
QR_Decomposition: theory Gauss_Jordan_PA
QR_Decomposition: theory Bases_Of_Fundamental_Subspaces
QR_Decomposition: theory Determinants2
QR_Decomposition: theory Inverse
QR_Decomposition: theory System_Of_Equations
QR_Decomposition: theory Examples_Gauss_Jordan_Abstract
Encodability_Process_Calculi: theory DivergenceReflection
Encodability_Process_Calculi: theory FullAbstraction
Encodability_Process_Calculi: theory OperationalCorrespondence
Encodability_Process_Calculi: theory SuccessSensitiveness
QR_Decomposition: theory IArray_Addenda_QR
QR_Decomposition: theory Miscellaneous_QR
QR_Decomposition: theory Generalizations2
QR_Decomposition: theory Matrix_To_IArray_QR
QR_Decomposition: theory Projections
QR_Decomposition: theory Gram_Schmidt
QR_Decomposition: theory QR_Decomposition
QR_Decomposition: theory Examples_QR_Abstract_Float
QR_Decomposition: theory Gram_Schmidt_IArrays
QR_Decomposition: theory Least_Squares_Approximation
QR_Decomposition: theory Examples_QR_Abstract_Symbolic
QR_Decomposition: theory QR_Decomposition_IArrays
QR_Decomposition: theory Examples_QR_IArrays_Float
QR_Decomposition: theory QR_Efficient
Encodability_Process_Calculi: theory CombinedCriteria
QR_Decomposition: theory Examples_QR_IArrays_Symbolic
Timing Encodability_Process_Calculi (4 threads, 234.135s elapsed time, 504.732s cpu time, 10.060s GC time, factor 2.16)
Finished Encodability_Process_Calculi (0:03:56 elapsed time, 0:08:27 cpu time, factor 2.14)
Timing QR_Decomposition (4 threads, 249.844s elapsed time, 919.264s cpu time, 17.020s GC time, factor 3.68)
Finished QR_Decomposition (0:04:14 elapsed time, 0:15:23 cpu time, factor 3.63)
KAD: theory Kleene_Algebra_Models
KAD: theory Antidomain_Semiring
KAD: theory Modal_Kleene_Algebra_Applications
KAD: theory Modal_Kleene_Algebra
KAD: theory Modal_Kleene_Algebra_Models
Timing KAD (4 threads, 213.848s elapsed time, 341.016s cpu time, 9.572s GC time, factor 1.59)
Finished KAD (0:03:36 elapsed time, 0:05:43 cpu time, factor 1.59)
Running Jordan_Normal_Form ...
Jordan_Normal_Form: theory Missing_Ring
Jordan_Normal_Form: theory Missing_Permutations
Jordan_Normal_Form: theory Conjugate
Jordan_Normal_Form: theory Missing_VectorSpace
Jordan_Normal_Form: theory Derivation_Bound
Jordan_Normal_Form: theory Show_Arctic
Jordan_Normal_Form: theory Matrix
Jordan_Normal_Form: theory Missing_Fraction_Field
Jordan_Normal_Form: theory Gauss_Jordan
Jordan_Normal_Form: theory Matrix_Comparison
Jordan_Normal_Form: theory Matrix_IArray_Impl
Jordan_Normal_Form: theory Show_Matrix
Jordan_Normal_Form: theory Strassen_Algorithm
Jordan_Normal_Form: theory VS_Connect
Jordan_Normal_Form: theory Column_Operations
Jordan_Normal_Form: theory Gauss_Jordan_IArray_Impl
Jordan_Normal_Form: theory Determinant
Jordan_Normal_Form: theory Strassen_Algorithm_Code
Jordan_Normal_Form: theory Ring_Hom_Matrix
Jordan_Normal_Form: theory Char_Poly
Jordan_Normal_Form: theory Determinant_Impl
Jordan_Normal_Form: theory Complexity_Carrier
Jordan_Normal_Form: theory Jordan_Normal_Form
Timing CoreC++ (4 threads, 227.615s elapsed time, 747.584s cpu time, 32.588s GC time, factor 3.28)
Finished CoreC++ (0:04:15 elapsed time, 0:12:33 cpu time, factor 2.95)
Running Isabelle_Meta_Model ...
Jordan_Normal_Form: theory Gram_Schmidt
Jordan_Normal_Form: theory Schur_Decomposition
Jordan_Normal_Form: theory Matrix_Complexity
Isabelle_Meta_Model: theory Isabelle_Cartouche_Examples
Isabelle_Meta_Model: theory Isabelle_code_runtime
Isabelle_Meta_Model: theory Isabelle_code_target
Isabelle_Meta_Model: theory Isabelle_parse_spec
Isabelle_Meta_Model: theory Isabelle_typedecl
Isabelle_Meta_Model: theory Isabelle_Main2
Isabelle_Meta_Model: theory Isabelle_function_common
Isabelle_Meta_Model: theory Isabelle_fun
Isabelle_Meta_Model: theory Isabelle_isar_syn
Isabelle_Meta_Model: theory Isabelle_Main1
Isabelle_Meta_Model: theory Isabelle_Main0
Isabelle_Meta_Model: theory Init
Jordan_Normal_Form: theory Jordan_Normal_Form_Existence
Isabelle_Meta_Model: theory Meta_SML
Isabelle_Meta_Model: theory Meta_Pure
Isabelle_Meta_Model: theory Parser_init
Isabelle_Meta_Model: theory Printer_init
Isabelle_Meta_Model: theory Parser_Pure
Isabelle_Meta_Model: theory Printer_Pure
Jordan_Normal_Form: theory Matrix_Impl
Isabelle_Meta_Model: theory Printer_SML
Isabelle_Meta_Model: theory Meta_Isabelle
Isabelle_Meta_Model: theory Printer_Isabelle
Isabelle_Meta_Model: theory Meta_Toy_extended
Isabelle_Meta_Model: theory Init_rbt
Isabelle_Meta_Model: theory Toy_Library_Static
Isabelle_Meta_Model: theory Meta_Toy
Isabelle_Meta_Model: theory Parser_Toy_extended
Isabelle_Meta_Model: theory Meta_META
Isabelle_Meta_Model: theory Parser_Toy
Isabelle_Meta_Model: theory Printer_Toy
Isabelle_Meta_Model: theory Printer_Toy_extended
Isabelle_Meta_Model: theory Parser_META
Isabelle_Meta_Model: theory Core_init
Isabelle_Meta_Model: theory Printer_META
Isabelle_Meta_Model: theory Floor1_access
Isabelle_Meta_Model: theory Floor1_ctxt
Isabelle_Meta_Model: theory Floor1_infra
Isabelle_Meta_Model: theory Floor1_examp
Isabelle_Meta_Model: theory Floor2_examp
Isabelle_Meta_Model: theory Core
Isabelle_Meta_Model: theory Printer
Isabelle_Meta_Model: theory Generator_static
Isabelle_Meta_Model: theory Generator_dynamic
Isabelle_Meta_Model: theory Toy_Library
Isabelle_Meta_Model: theory Design_generated_generated
Isabelle_Meta_Model: theory Design_deep
Isabelle_Meta_Model: theory Design_shallow
Isabelle_Meta_Model: theory Rail
Timing Jordan_Normal_Form (4 threads, 208.604s elapsed time, 778.892s cpu time, 9.572s GC time, factor 3.73)
Finished Jordan_Normal_Form (0:03:39 elapsed time, 0:13:05 cpu time, factor 3.58)
Running Network_Security_Policy_Verification ...
Network_Security_Policy_Verification: theory Char_ord
Network_Security_Policy_Verification: theory FiniteGraph
Network_Security_Policy_Verification: theory List_lexord
Network_Security_Policy_Verification: theory ML_GraphViz_Config
Network_Security_Policy_Verification: theory ML_GraphViz
Network_Security_Policy_Verification: theory Orders
Network_Security_Policy_Verification: theory Code_Char
Network_Security_Policy_Verification: theory ML_GraphViz_Disable
Network_Security_Policy_Verification: theory TopoS_Util
Network_Security_Policy_Verification: theory Transitive_Closure_Impl
Network_Security_Policy_Verification: theory Efficient_Distinct
Network_Security_Policy_Verification: theory Transitive_Closure_List_Impl
Network_Security_Policy_Verification: theory FiniteListGraph
Network_Security_Policy_Verification: theory Bounds
Network_Security_Policy_Verification: theory Lattice
Timing Isabelle_Meta_Model (4 threads, 194.335s elapsed time, 290.772s cpu time, 16.576s GC time, factor 1.50)
Finished Isabelle_Meta_Model (0:03:20 elapsed time, 0:04:56 cpu time, factor 1.48)
Network_Security_Policy_Verification: theory CompleteLattice
Network_Security_Policy_Verification: theory FiniteListGraph_Impl
Affine_Arithmetic: theory Adhoc_Overloading
Affine_Arithmetic: theory Code_Abstract_Nat
Affine_Arithmetic: theory Code_Target_Int
Affine_Arithmetic: theory Multiset
Affine_Arithmetic: theory Monad_Syntax
Affine_Arithmetic: theory Code_Target_Nat
Affine_Arithmetic: theory Lattice_Algebras
Affine_Arithmetic: theory Code_Target_Numeral
Network_Security_Policy_Verification: theory TopoS_Vertices
Network_Security_Policy_Verification: theory TopoS_Interface
Network_Security_Policy_Verification: theory vertex_example_simps
Affine_Arithmetic: theory Permutation
Network_Security_Policy_Verification: theory TopoS_withOffendingFlows
Network_Security_Policy_Verification: theory TopoS_ENF
Network_Security_Policy_Verification: theory TopoS_Helper
Network_Security_Policy_Verification: theory SINVAR_ACLcommunicateWith
Network_Security_Policy_Verification: theory SINVAR_ACLnotCommunicateWith
Network_Security_Policy_Verification: theory SINVAR_BLPbasic
Network_Security_Policy_Verification: theory SINVAR_BLPtrusted
Network_Security_Policy_Verification: theory SINVAR_CommunicationPartners
Network_Security_Policy_Verification: theory SINVAR_Dependability
Affine_Arithmetic: theory Float
Network_Security_Policy_Verification: theory SINVAR_Dependability_norefl
Network_Security_Policy_Verification: theory SINVAR_DomainHierarchyNG
Network_Security_Policy_Verification: theory SINVAR_NoRefl
Network_Security_Policy_Verification: theory SINVAR_NonInterference
Network_Security_Policy_Verification: theory SINVAR_SecGwExt
Network_Security_Policy_Verification: theory SINVAR_Sink
Network_Security_Policy_Verification: theory SINVAR_Subnets
Network_Security_Policy_Verification: theory SINVAR_SubnetsInGW
Network_Security_Policy_Verification: theory TopoS_Composition_Theory
Network_Security_Policy_Verification: theory TopoS_Interface_impl
Network_Security_Policy_Verification: theory TopoS_Stateful_Policy
Network_Security_Policy_Verification: theory SINVAR_ACLcommunicateWith_impl
Network_Security_Policy_Verification: theory SINVAR_ACLnotCommunicateWith_impl
Network_Security_Policy_Verification: theory SINVAR_BLPbasic_impl
Network_Security_Policy_Verification: theory TopoS_Stateful_Policy_Algorithm
Affine_Arithmetic: theory Float_Real
Affine_Arithmetic: theory Affine_Form
Affine_Arithmetic: theory Counterclockwise
Affine_Arithmetic: theory Euclidean_Space_Explicit
Network_Security_Policy_Verification: theory SINVAR_BLPtrusted_impl
Network_Security_Policy_Verification: theory SINVAR_CommunicationPartners_impl
Affine_Arithmetic: theory Executable_Euclidean_Space
Network_Security_Policy_Verification: theory SINVAR_Dependability_impl
Network_Security_Policy_Verification: theory SINVAR_Dependability_norefl_impl
Network_Security_Policy_Verification: theory SINVAR_DomainHierarchyNG_impl
Network_Security_Policy_Verification: theory SINVAR_NoRefl_impl
Affine_Arithmetic: theory Counterclockwise_Vector
Network_Security_Policy_Verification: theory SINVAR_NonInterference_impl
Network_Security_Policy_Verification: theory SINVAR_SecGwExt_impl
Network_Security_Policy_Verification: theory SINVAR_Sink_impl
Network_Security_Policy_Verification: theory SINVAR_SubnetsInGW_impl
Network_Security_Policy_Verification: theory SINVAR_Subnets_impl
Affine_Arithmetic: theory Counterclockwise_2D_Strict
Network_Security_Policy_Verification: theory TopoS_Composition_Theory_impl
Network_Security_Policy_Verification: theory TopoS_Library
Affine_Arithmetic: theory Counterclockwise_2D_Arbitrary
Affine_Arithmetic: theory Polygon
Affine_Arithmetic: theory Affine_Approximation
Network_Security_Policy_Verification: theory TopoS_Stateful_Policy_impl
Network_Security_Policy_Verification: theory Example_BLP
Network_Security_Policy_Verification: theory TopoS_Impl
Network_Security_Policy_Verification: theory TopoS_generateCode
Network_Security_Policy_Verification: theory Network_Security_Policy_Verification
Affine_Arithmetic: theory Affine_Code
Affine_Arithmetic: theory Ex_Affine_Approximation
Affine_Arithmetic: theory Ex_Ineqs
Affine_Arithmetic: theory Intersection
Affine_Arithmetic: theory Ex_Inter
Network_Security_Policy_Verification: theory Example_NetModel
Network_Security_Policy_Verification: theory Example
Network_Security_Policy_Verification: theory Distributed_WebApp
Network_Security_Policy_Verification: theory Example_Forte14
Network_Security_Policy_Verification: theory I8_SSH_Landscape
Network_Security_Policy_Verification: theory Impl_List_Playground
Network_Security_Policy_Verification: theory Impl_List_Playground_ChairNetwork
Network_Security_Policy_Verification: theory Impl_List_Playground_ChairNetwork_statefulpolicy_example
Network_Security_Policy_Verification: theory Impl_List_Playground_statefulpolicycompliance
Network_Security_Policy_Verification: theory attic
Affine_Arithmetic: theory Affine_Arithmetic
Timing Network_Security_Policy_Verification (4 threads, 202.552s elapsed time, 710.148s cpu time, 20.844s GC time, factor 3.51)
Finished Network_Security_Policy_Verification (0:03:32 elapsed time, 0:12:00 cpu time, factor 3.39)
Timing Affine_Arithmetic (4 threads, 195.320s elapsed time, 733.448s cpu time, 12.832s GC time, factor 3.76)
Finished Affine_Arithmetic (0:03:19 elapsed time, 0:12:17 cpu time, factor 3.70)
Running Containers-Benchmarks ...
Timed_Automata: theory Floyd_Warshall
Timed_Automata: theory Timed_Automata
Timed_Automata: theory Paths_Cycles
Timed_Automata: theory Regions
Containers-Benchmarks: theory Trie
Containers-Benchmarks: theory Benchmark_Comparison
Containers-Benchmarks: theory FingerTree
Containers-Benchmarks: theory Foldi
Timed_Automata: theory Closure
Containers-Benchmarks: theory ICF_Tools
Timed_Automata: theory DBM_Basics
Containers-Benchmarks: theory BinomialHeap
Timed_Automata: theory DBM_Normalization
Timed_Automata: theory DBM_Operations
Containers-Benchmarks: theory Benchmark_Default
Containers-Benchmarks: theory List_More
Containers-Benchmarks: theory Quicksort
Containers-Benchmarks: theory Ord_Code_Preproc
Containers-Benchmarks: theory Locale_Code
Containers-Benchmarks: theory Prio_List
Containers-Benchmarks: theory Benchmark_RBT
Containers-Benchmarks: theory Misc
Timed_Automata: theory DBM_Zone_Semantics
Timed_Automata: theory Regions_Beta
Containers-Benchmarks: theory Benchmark_Bool
Containers-Benchmarks: theory Benchmark_LC
Containers-Benchmarks: theory Clauses
Timed_Automata: theory Approx_Beta
Containers-Benchmarks: theory Record_Intf
Containers-Benchmarks: theory Refine_Chapter
Containers-Benchmarks: theory Refine_Util
Containers-Benchmarks: theory Anti_Unification
Containers-Benchmarks: theory Attr_Comb
Containers-Benchmarks: theory Named_Sorted_Thms
Containers-Benchmarks: theory Autoref_Data
Timed_Automata: theory Normalized_Zone_Semantics
Containers-Benchmarks: theory Mk_Term_Antiquot
Containers-Benchmarks: theory Mpat_Antiquot
Containers-Benchmarks: theory Indep_Vars
Containers-Benchmarks: theory Mk_Record_Simp
Containers-Benchmarks: theory Tagged_Solver
Containers-Benchmarks: theory Select_Solve
Containers-Benchmarks: theory SkewBinomialHeap
Containers-Benchmarks: theory DatRef
Containers-Benchmarks: theory Benchmark_Set
Containers-Benchmarks: theory SetIterator
Containers-Benchmarks: theory Digraph_Basic
Containers-Benchmarks: theory SetIteratorOperations
Containers-Benchmarks: theory Refine_Lib
Containers-Benchmarks: theory Sorted_List_Operations
Containers-Benchmarks: theory Autoref_Phases
Containers-Benchmarks: theory Autoref_Tagging
Containers-Benchmarks: theory Refine_Mono_Prover
Containers-Benchmarks: theory Relators
Containers-Benchmarks: theory Benchmark_Set_Default
Containers-Benchmarks: theory Param_Tool
Containers-Benchmarks: theory Assoc_List
Containers-Benchmarks: theory Param_HOL
Containers-Benchmarks: theory Trie_Impl
Containers-Benchmarks: theory Dlist_add
Containers-Benchmarks: theory Trie2
Containers-Benchmarks: theory Proper_Iterator
Containers-Benchmarks: theory Parametricity
Containers-Benchmarks: theory SetIteratorGA
Containers-Benchmarks: theory Autoref_Id_Ops
Containers-Benchmarks: theory Diff_Array
Containers-Benchmarks: theory Autoref_Fix_Rel
Containers-Benchmarks: theory It_to_It
Containers-Benchmarks: theory Benchmark_Set_LC
Containers-Benchmarks: theory Autoref_Translate
Containers-Benchmarks: theory Autoref_Gen_Algo
Containers-Benchmarks: theory Autoref_Relator_Interface
Containers-Benchmarks: theory Autoref_Tool
Containers-Benchmarks: theory Autoref_Bindings_HOL
Containers-Benchmarks: theory Automatic_Refinement
Containers-Benchmarks: theory Idx_Iterator
Containers-Benchmarks: theory Refine_Misc
Containers-Benchmarks: theory RefineG_Domain
Containers-Benchmarks: theory RefineG_Transfer
Containers-Benchmarks: theory RefineG_Assert
Containers-Benchmarks: theory RefineG_Recursion
Containers-Benchmarks: theory Refine_Basic
Containers-Benchmarks: theory RefineG_While
Containers-Benchmarks: theory Refine_Det
Containers-Benchmarks: theory Refine_Heuristics
Containers-Benchmarks: theory Refine_Leof
Containers-Benchmarks: theory Refine_Pfun
Containers-Benchmarks: theory Refine_While
Containers-Benchmarks: theory Refine_Transfer
Containers-Benchmarks: theory Autoref_Monadic
Containers-Benchmarks: theory Refine_Automation
Containers-Benchmarks: theory Refine_Foreach
Containers-Benchmarks: theory Refine_Monadic
Containers-Benchmarks: theory Gen_Iterator
Containers-Benchmarks: theory Intf_Map
Containers-Benchmarks: theory Intf_Set
Containers-Benchmarks: theory Iterator
Containers-Benchmarks: theory Array_Iterator
Containers-Benchmarks: theory ICF_Spec_Base
Containers-Benchmarks: theory RBT_add
Containers-Benchmarks: theory AnnotatedListSpec
Containers-Benchmarks: theory ListSpec
Containers-Benchmarks: theory MapSpec
Containers-Benchmarks: theory ListGA
Containers-Benchmarks: theory FTAnnotatedListImpl
Containers-Benchmarks: theory Fifo
Containers-Benchmarks: theory PrioSpec
Containers-Benchmarks: theory PrioUniqueSpec
Containers-Benchmarks: theory SetSpec
Containers-Benchmarks: theory BinoPrioImpl
Containers-Benchmarks: theory PrioByAnnotatedList
Containers-Benchmarks: theory SkewPrioImpl
Containers-Benchmarks: theory PrioUniqueByAnnotatedList
Containers-Benchmarks: theory FTPrioImpl
Containers-Benchmarks: theory FTPrioUniqueImpl
Containers-Benchmarks: theory Algos
Containers-Benchmarks: theory SetIndex
Containers-Benchmarks: theory SetIteratorCollectionsGA
Containers-Benchmarks: theory MapGA
Containers-Benchmarks: theory SetGA
Containers-Benchmarks: theory ArrayMapImpl
Containers-Benchmarks: theory ListMapImpl
Containers-Benchmarks: theory ListMapImpl_Invar
Containers-Benchmarks: theory TrieMapImpl
Containers-Benchmarks: theory ListSetImpl
Containers-Benchmarks: theory ListSetImpl_Invar
Containers-Benchmarks: theory ListSetImpl_NotDist
Containers-Benchmarks: theory ListSetImpl_Sorted
Containers-Benchmarks: theory SetByMap
Containers-Benchmarks: theory RBTMapImpl
Containers-Benchmarks: theory ArrayHashMap_Impl
Containers-Benchmarks: theory ArraySetImpl
Containers-Benchmarks: theory TrieSetImpl
Containers-Benchmarks: theory RBTSetImpl
Containers-Benchmarks: theory HashMap_Impl
Containers-Benchmarks: theory ArrayHashMap
Containers-Benchmarks: theory HashMap
Containers-Benchmarks: theory ArrayHashSet
Containers-Benchmarks: theory HashSet
Containers-Benchmarks: theory MapStdImpl
Containers-Benchmarks: theory SetStdImpl
Containers-Benchmarks: theory ICF_Impl
Containers-Benchmarks: theory ICF_Refine_Monadic
Containers-Benchmarks: theory ICF_Autoref
Containers-Benchmarks: theory Collections
Containers-Benchmarks: theory CollectionsV1
Containers-Benchmarks: theory Benchmark_ICF
Timing Timed_Automata (4 threads, 195.451s elapsed time, 719.648s cpu time, 12.828s GC time, factor 3.68)
Finished Timed_Automata (0:03:18 elapsed time, 0:12:02 cpu time, factor 3.65)
Running Probabilistic_System_Zoo-BNFs ...
Probabilistic_System_Zoo-BNFs: theory Adhoc_Overloading
Probabilistic_System_Zoo-BNFs: theory Order_Union
Probabilistic_System_Zoo-BNFs: theory Cardinal_Notations
Probabilistic_System_Zoo-BNFs: theory Disjoint_Sets
Probabilistic_System_Zoo-BNFs: theory Fun_More
Probabilistic_System_Zoo-BNFs: theory Monad_Syntax
Probabilistic_System_Zoo-BNFs: theory Multiset
Probabilistic_System_Zoo-BNFs: theory Order_Relation_More
Probabilistic_System_Zoo-BNFs: theory Sigma_Algebra
Probabilistic_System_Zoo-BNFs: theory Wellorder_Extension
Probabilistic_System_Zoo-BNFs: theory Wellfounded_More
Probabilistic_System_Zoo-BNFs: theory Wellorder_Relation
Timing Containers-Benchmarks (4 threads, 189.013s elapsed time, 604.484s cpu time, 37.744s GC time, factor 3.20)
Finished Containers-Benchmarks (0:03:21 elapsed time, 0:10:15 cpu time, factor 3.06)
Probabilistic_System_Zoo-BNFs: theory Wellorder_Embedding
Probabilistic_System_Zoo-BNFs: theory Wellorder_Constructions
Probabilistic_System_Zoo-BNFs: theory Cardinal_Order_Relation
Probabilistic_System_Zoo-BNFs: theory Ordinal_Arithmetic
Probabilistic_System_Zoo-BNFs: theory Cardinal_Arithmetic
Probabilistic_System_Zoo-BNFs: theory Cardinals
Probabilistic_System_Zoo-BNFs: theory Measurable
Probabilistic_System_Zoo-BNFs: theory Borel_Space
Probabilistic_System_Zoo-BNFs: theory Measure_Space
Probabilistic_System_Zoo-BNFs: theory Caratheodory
Probabilistic_System_Zoo-BNFs: theory Nonnegative_Lebesgue_Integration
Probabilistic_System_Zoo-BNFs: theory Binary_Product_Measure
Probabilistic_System_Zoo-BNFs: theory Finite_Product_Measure
Probabilistic_System_Zoo-BNFs: theory Bochner_Integration
Probabilistic_System_Zoo-BNFs: theory Radon_Nikodym
Probabilistic_System_Zoo-BNFs: theory Lebesgue_Measure
Probabilistic_System_Zoo-BNFs: theory Probability_Measure
Probabilistic_System_Zoo-BNFs: theory Set_Integral
Probabilistic_System_Zoo-BNFs: theory Interval_Integral
Probabilistic_System_Zoo-BNFs: theory Lebesgue_Integral_Substitution
Probabilistic_System_Zoo-BNFs: theory Giry_Monad
Flyspeck-Tame: theory IArray_Syntax
Flyspeck-Tame: theory Quasi_Order
Flyspeck-Tame: theory PlaneGraphIso
Flyspeck-Tame: theory Worklist
Flyspeck-Tame: theory Rotation
Flyspeck-Tame: theory Enumerator
Flyspeck-Tame: theory FaceDivision
Flyspeck-Tame: theory GraphProps
Flyspeck-Tame: theory EnumeratorProps
Flyspeck-Tame: theory TameProps
Flyspeck-Tame: theory FaceDivisionProps
Flyspeck-Tame: theory Generator
Flyspeck-Tame: theory TameEnum
Flyspeck-Tame: theory Invariants
Flyspeck-Tame: theory PlaneProps
Flyspeck-Tame: theory Plane1Props
Flyspeck-Tame: theory ScoreProps
Flyspeck-Tame: theory ArchCompAux
Flyspeck-Tame: theory LowerBound
Flyspeck-Tame: theory GeneratorProps
Flyspeck-Tame: theory TameEnumProps
Flyspeck-Tame: theory ArchCompProps
Flyspeck-Tame: theory ArchComp
Flyspeck-Tame: theory Completeness
Probabilistic_System_Zoo-BNFs: theory Probability_Mass_Function
Probabilistic_System_Zoo-BNFs: theory Bounded_Set
Probabilistic_System_Zoo-BNFs: theory Bool_Bounded_Set
Probabilistic_System_Zoo-BNFs: theory Nonempty_Bounded_Set
Timing Probabilistic_System_Zoo-BNFs (4 threads, 178.799s elapsed time, 664.876s cpu time, 10.812s GC time, factor 3.72)
Finished Probabilistic_System_Zoo-BNFs (0:03:03 elapsed time, 0:11:09 cpu time, factor 3.66)
Timing Flyspeck-Tame (4 threads, 176.943s elapsed time, 533.384s cpu time, 25.076s GC time, factor 3.01)
Finished Flyspeck-Tame (0:03:03 elapsed time, 0:08:59 cpu time, factor 2.94)
List_Update: theory Regular_Set
List_Update: theory List_Index
List_Update: theory While_Combinator
List_Update: theory Regular_Exp
Gabow_SCC: theory Gabow_Skeleton
Gabow_SCC: theory Find_Path_Impl
List_Update: theory NDerivative
List_Update: theory Equivalence_Checking
Gabow_SCC: theory Gabow_Skeleton_Code
List_Update: theory Bit_Strings
List_Update: theory Prob_Theory
List_Update: theory Competitive_Analysis
List_Update: theory Move_to_Front
List_Update: theory MTF2_Effects
List_Update: theory Partial_Cost_Model
List_Update: theory List_Factoring
List_Update: theory Phase_Partitioning
List_Update: theory BIT_pairwise
List_Update: theory BIT_2comp_on2
Gabow_SCC: theory Gabow_GBG_Code
Gabow_SCC: theory Gabow_SCC_Code
Timing List_Update (4 threads, 161.422s elapsed time, 567.220s cpu time, 11.088s GC time, factor 3.51)
Finished List_Update (0:02:51 elapsed time, 0:09:38 cpu time, factor 3.37)
Running Probabilistic_Noninterference ...
Gabow_SCC: theory All_Of_Gabow_SCC
Probabilistic_Noninterference: theory Lattice_Syntax
Probabilistic_Noninterference: theory Simps_Case_Conv
Probabilistic_Noninterference: theory Rewrite
Probabilistic_Noninterference: theory Prefix_Order
Probabilistic_Noninterference: theory Complete_Partial_Order2
Timing Gabow_SCC (4 threads, 162.144s elapsed time, 411.096s cpu time, 10.388s GC time, factor 2.54)
Finished Gabow_SCC (0:02:53 elapsed time, 0:07:22 cpu time, factor 2.55)
Running Planarity_Certificates ...
Probabilistic_Noninterference: theory Coinductive_Nat
Probabilistic_Noninterference: theory Coinductive_List
Planarity_Certificates: theory Eisbach
Planarity_Certificates: theory Permutations
Planarity_Certificates: theory Case_Labeling
Planarity_Certificates: theory FuncSet
Planarity_Certificates: theory Infinite_Set
Planarity_Certificates: theory Lib
Planarity_Certificates: theory List_Index
Planarity_Certificates: theory Funpow
Planarity_Certificates: theory NonDetMonad
Planarity_Certificates: theory OptionMonad
Planarity_Certificates: theory Nat_Bijection
Planarity_Certificates: theory Old_Datatype
Planarity_Certificates: theory Rewrite
Planarity_Certificates: theory Rtrancl_On
Planarity_Certificates: theory Simps_Case_Conv
Planarity_Certificates: theory Liminf_Limsup
Planarity_Certificates: theory Transitive_Closure_Impl
Planarity_Certificates: theory NonDetMonadLemmas
Planarity_Certificates: theory OptionMonadND
Planarity_Certificates: theory WP
Planarity_Certificates: theory Countable
Planarity_Certificates: theory OptionMonadWP
Planarity_Certificates: theory Countable_Set
Planarity_Certificates: theory Countable_Complete_Lattices
Probabilistic_Noninterference: theory Coinductive_Stream
Probabilistic_Noninterference: theory Discrete_Time_Markov_Chain
Planarity_Certificates: theory Order_Continuity
Planarity_Certificates: theory Extended_Nat
Planarity_Certificates: theory Extended_Real
Probabilistic_Noninterference: theory Interface
Planarity_Certificates: theory Stuff
Planarity_Certificates: theory Digraph
Planarity_Certificates: theory Arc_Walk
Planarity_Certificates: theory Bidirected_Digraph
Planarity_Certificates: theory Vertex_Walk
Planarity_Certificates: theory Pair_Digraph
Planarity_Certificates: theory Weighted_Graph
Planarity_Certificates: theory Shortest_Path
Planarity_Certificates: theory Digraph_Component
Probabilistic_Noninterference: theory Language_Semantics
Planarity_Certificates: theory Digraph_Component_Vwalk
Planarity_Certificates: theory Digraph_Isomorphism
Planarity_Certificates: theory Subdivision
Planarity_Certificates: theory Kuratowski
Planarity_Certificates: theory Euler
Probabilistic_Noninterference: theory Resumption_Based
Planarity_Certificates: theory Graph_Theory
Probabilistic_Noninterference: theory Compositionality
Probabilistic_Noninterference: theory Trace_Based
Probabilistic_Noninterference: theory Syntactic_Criteria
Probabilistic_Noninterference: theory Concrete
Planarity_Certificates: theory List_Aux
Planarity_Certificates: theory Simpl_Anno
Planarity_Certificates: theory Graph_Genus
Planarity_Certificates: theory Reachablen
Planarity_Certificates: theory Check_Non_Planarity_Impl
Planarity_Certificates: theory Executable_Permutations
Planarity_Certificates: theory AutoCorres_Misc
Planarity_Certificates: theory Setup_AutoCorres
Planarity_Certificates: theory Permutations_2
Planarity_Certificates: theory Digraph_Map_Impl
Planarity_Certificates: theory Check_Planarity_Verification
Planarity_Certificates: theory Planar_Subgraph
Planarity_Certificates: theory Planar_Subdivision
Planarity_Certificates: theory Planar_Complete
Planarity_Certificates: theory Kuratowski_Combinatorial
Planarity_Certificates: theory Check_Non_Planarity_Verification
Planarity_Certificates: theory Planarity_Certificates
Timing Probabilistic_Noninterference (4 threads, 159.866s elapsed time, 577.512s cpu time, 8.948s GC time, factor 3.61)
Finished Probabilistic_Noninterference (0:02:45 elapsed time, 0:09:54 cpu time, factor 3.58)
Timing Planarity_Certificates (4 threads, 151.957s elapsed time, 534.952s cpu time, 17.936s GC time, factor 3.52)
Finished Planarity_Certificates (0:02:38 elapsed time, 0:08:59 cpu time, factor 3.41)
Featherweight_OCL: theory UML_Types
Featherweight_OCL: theory UML_Logic
Markov_Models: theory Lattice_Syntax
Markov_Models: theory Code_Abstract_Nat
Markov_Models: theory Code_Target_Int
Markov_Models: theory Gauss_Jordan_Elim_Fun
Markov_Models: theory Complete_Partial_Order2
Markov_Models: theory Code_Target_Nat
Markov_Models: theory Code_Target_Numeral
Markov_Models: theory Quotient_Syntax
Markov_Models: theory Quotient_Option
Markov_Models: theory Quotient_Product
Markov_Models: theory Quotient_Set
Markov_Models: theory Quotient_Sum
Markov_Models: theory Quotient_List
Markov_Models: theory Simps_Case_Conv
Markov_Models: theory Prefix_Order
Featherweight_OCL: theory UML_PropertyProfiles
Markov_Models: theory While_Combinator
Featherweight_OCL: theory UML_Tools
Featherweight_OCL: theory UML_Boolean
Featherweight_OCL: theory UML_Integer
Featherweight_OCL: theory UML_Pair
Markov_Models: theory Coinductive_Nat
Featherweight_OCL: theory UML_Real
Featherweight_OCL: theory UML_String
Markov_Models: theory Coinductive_List
Featherweight_OCL: theory UML_Void
Featherweight_OCL: theory UML_Sequence
Featherweight_OCL: theory UML_Bag
Featherweight_OCL: theory UML_Set
Markov_Models: theory Coinductive_List_Prefix
Markov_Models: theory Quotient_Coinductive_List
Markov_Models: theory Coinductive_Stream
Markov_Models: theory Quotient_TLList
Featherweight_OCL: theory UML_Library
Markov_Models: theory Coinductive
Markov_Models: theory Discrete_Time_Markov_Chain
Markov_Models: theory Classifying_Markov_Chain_States
Markov_Models: theory Crowds_Protocol
Markov_Models: theory Gossip_Broadcast
Markov_Models: theory Markov_Decision_Process
Markov_Models: theory Trace_Space_Equals_Markov_Processes
Markov_Models: theory Zeroconf_Analysis
Markov_Models: theory Example_A
Markov_Models: theory Example_B
Markov_Models: theory MDP_Reachability_Problem
Markov_Models: theory MDP_RP_Certification
Markov_Models: theory Markov_Models
Featherweight_OCL: theory UML_State
Featherweight_OCL: theory UML_Contracts
Featherweight_OCL: theory UML_Main
Featherweight_OCL: theory Analysis_UML
Featherweight_OCL: theory Design_UML
Featherweight_OCL: theory Analysis_OCL
Timing Markov_Models (4 threads, 135.189s elapsed time, 453.896s cpu time, 11.596s GC time, factor 3.36)
Finished Markov_Models (0:02:20 elapsed time, 0:08:01 cpu time, factor 3.41)
Featherweight_OCL: theory Design_OCL
Density_Compiler: theory Density_Predicates
Density_Compiler: theory PDF_Transformations
Density_Compiler: theory PDF_Values
Timing Featherweight_OCL (4 threads, 148.242s elapsed time, 471.784s cpu time, 11.220s GC time, factor 3.18)
Finished Featherweight_OCL (0:02:30 elapsed time, 0:07:54 cpu time, factor 3.14)
Density_Compiler: theory PDF_Semantics
Density_Compiler: theory PDF_Density_Contexts
Density_Compiler: theory PDF_Target_Semantics
Density_Compiler: theory PDF_Compiler_Pred
Density_Compiler: theory PDF_Target_Density_Contexts
Density_Compiler: theory PDF_Compiler
KBPs: theory Transitive_Closure_Impl
KBPs: theory Transitive_Closure_List_Impl
KBPs: theory SPRViewNonDetIndInit
Timing Density_Compiler (4 threads, 128.540s elapsed time, 390.136s cpu time, 4.976s GC time, factor 3.04)
Finished Density_Compiler (0:02:14 elapsed time, 0:06:35 cpu time, factor 2.95)
Gauss_Jordan: theory Code_Abstract_Nat
Gauss_Jordan: theory Dual_Order
Gauss_Jordan: theory Code_Target_Int
Gauss_Jordan: theory Code_Target_Nat
Gauss_Jordan: theory Generalizations
Gauss_Jordan: theory Code_Target_Numeral
Gauss_Jordan: theory Miscellaneous
Gauss_Jordan: theory Fundamental_Subspaces
Timing KBPs (4 threads, 129.645s elapsed time, 359.632s cpu time, 11.168s GC time, factor 2.77)
Finished KBPs (0:02:15 elapsed time, 0:06:05 cpu time, factor 2.70)
Gauss_Jordan: theory Dim_Formula
PseudoHoops: theory Operations
PseudoHoops: theory LeftComplementedMonoid
PseudoHoops: theory PseudoWaisbergAlgebra
PseudoHoops: theory RightComplementedMonoid
PseudoHoops: theory PseudoHoops
Gauss_Jordan: theory Code_Real_Approx_By_Float
Gauss_Jordan: theory Code_Matrix
Gauss_Jordan: theory Code_Real_Approx_By_Float_Haskell
Gauss_Jordan: theory Elementary_Operations
Gauss_Jordan: theory IArray_Addenda
Gauss_Jordan: theory IArray_Haskell
Gauss_Jordan: theory Matrix_To_IArray
Gauss_Jordan: theory Gauss_Jordan
Gauss_Jordan: theory Gauss_Jordan_IArrays
Gauss_Jordan: theory Linear_Maps
Gauss_Jordan: theory Gauss_Jordan_PA
Gauss_Jordan: theory Bases_Of_Fundamental_Subspaces
Gauss_Jordan: theory Determinants2
Gauss_Jordan: theory Gauss_Jordan_PA_IArrays
Gauss_Jordan: theory System_Of_Equations
Gauss_Jordan: theory Determinants_IArrays
Gauss_Jordan: theory Bases_Of_Fundamental_Subspaces_IArrays
Gauss_Jordan: theory Inverse_IArrays
Gauss_Jordan: theory Examples_Gauss_Jordan_Abstract
Gauss_Jordan: theory System_Of_Equations_IArrays
Gauss_Jordan: theory Examples_Gauss_Jordan_IArrays
Gauss_Jordan: theory Code_Generation_IArrays
Gauss_Jordan: theory Code_Generation_IArrays_SML
Gauss_Jordan: theory Code_Rational
Gauss_Jordan: theory Code_Generation_IArrays_Haskell
PseudoHoops: theory PseudoHoopFilters
PseudoHoops: theory SpecialPseudoHoops
Timing Gauss_Jordan (4 threads, 126.163s elapsed time, 466.780s cpu time, 8.020s GC time, factor 3.70)
Finished Gauss_Jordan (0:02:10 elapsed time, 0:07:51 cpu time, factor 3.61)
LTL_to_DRA: theory Boolean_Expression_Checkers
Timing PseudoHoops (4 threads, 122.590s elapsed time, 180.336s cpu time, 3.596s GC time, factor 1.47)
Finished PseudoHoops (0:02:06 elapsed time, 0:03:02 cpu time, factor 1.45)
Consensus_Refined: theory HOModel
Consensus_Refined: theory Infinite_Set
Consensus_Refined: theory Majorities
Consensus_Refined: theory Omega_Words_Fun
Consensus_Refined: theory Samplers
Consensus_Refined: theory StutterEquivalence
Consensus_Refined: theory Reduction
LTL_to_DRA: theory Boolean_Expression_Checkers_AList_Mapping
LTL_to_DRA: theory Preliminaries2
Consensus_Refined: theory Consensus_Types
Consensus_Refined: theory Consensus_Misc
Consensus_Refined: theory Infra
Consensus_Refined: theory Quorums
Consensus_Refined: theory Ate_Defs
Consensus_Refined: theory OneThirdRule_Defs
Consensus_Refined: theory Uv_Defs
Consensus_Refined: theory Three_Steps
Consensus_Refined: theory Two_Steps
Consensus_Refined: theory BenOr_Defs
Consensus_Refined: theory CT_Defs
Consensus_Refined: theory New_Algorithm_Defs
LTL_to_DRA: theory Semi_Mojmir
Consensus_Refined: theory Paxos_Defs
Consensus_Refined: theory Refinement
Consensus_Refined: theory HO_Transition_System
Consensus_Refined: theory Voting
Consensus_Refined: theory Same_Vote
Consensus_Refined: theory Voting_Opt
Consensus_Refined: theory MRU_Vote
Consensus_Refined: theory Observing_Quorums
Consensus_Refined: theory MRU_Vote_Opt
Consensus_Refined: theory Ate_Proofs
Consensus_Refined: theory OneThirdRule_Proofs
Consensus_Refined: theory Observing_Quorums_Opt
Consensus_Refined: theory Three_Step_MRU
Consensus_Refined: theory Two_Step_Observing
Consensus_Refined: theory CT_Proofs
Consensus_Refined: theory New_Algorithm_Proofs
Consensus_Refined: theory Paxos_Proofs
Consensus_Refined: theory BenOr_Proofs
LTL_to_DRA: theory Mojmir_Rabin
Consensus_Refined: theory Uv_Proofs
LTL_to_DRA: theory Mojmir_Rabin_Impl
LTL_to_DRA: theory Logical_Characterization
LTL_to_DRA: theory LTL_Rabin_Unfold_Opt
LTL_to_DRA: theory LTL_Rabin_Impl
LTL_to_DRA: theory Export_Code
Timing Consensus_Refined (4 threads, 98.028s elapsed time, 212.608s cpu time, 6.020s GC time, factor 2.17)
Finished Consensus_Refined (0:01:40 elapsed time, 0:03:34 cpu time, factor 2.14)
Regular_Algebras: theory Dioid_Power_Sum
Regular_Algebras: theory Regular_Algebras
Timing LTL_to_DRA (4 threads, 120.146s elapsed time, 408.980s cpu time, 17.672s GC time, factor 3.40)
Finished LTL_to_DRA (0:02:07 elapsed time, 0:06:55 cpu time, factor 3.26)
Ergodic_Theory: theory SG_Library_Complement
Ergodic_Theory: theory Banach_Density
Ergodic_Theory: theory Conditional_Expectation
Ergodic_Theory: theory Measure_Preserving_Transformations
Ergodic_Theory: theory Recurrence
Ergodic_Theory: theory Invariants
Ergodic_Theory: theory Ergodicity
Ergodic_Theory: theory Kingman
Ergodic_Theory: theory Gouezel_Karlsson
Regular_Algebras: theory Regular_Algebra_Models
Regular_Algebras: theory Pratts_Counterexamples
Regular_Algebras: theory Regular_Algebra_Variants
Timing Regular_Algebras (4 threads, 114.699s elapsed time, 183.772s cpu time, 3.436s GC time, factor 1.60)
Finished Regular_Algebras (0:01:59 elapsed time, 0:03:14 cpu time, factor 1.63)
Akra_Bazzi: theory Dense_Linear_Order
Akra_Bazzi: theory Code_Abstract_Nat
Akra_Bazzi: theory Function_Algebras
Akra_Bazzi: theory Code_Target_Int
Akra_Bazzi: theory Code_Target_Nat
Akra_Bazzi: theory Landau_Library
Akra_Bazzi: theory Code_Target_Numeral
Akra_Bazzi: theory Landau_Symbols_Definition
Akra_Bazzi: theory Lattice_Algebras
Timing Ergodic_Theory (4 threads, 108.176s elapsed time, 420.496s cpu time, 4.668s GC time, factor 3.89)
Finished Ergodic_Theory (0:01:54 elapsed time, 0:07:06 cpu time, factor 3.73)
Running Collections_Examples ...
Akra_Bazzi: theory Landau_Real_Products
Akra_Bazzi: theory Approximation
Akra_Bazzi: theory Landau_Simprocs
Akra_Bazzi: theory Landau_Symbols
Collections_Examples: theory Collection_Autoref_Examples_Chapter
Collections_Examples: theory Examples_Chapter
Collections_Examples: theory ICF_Examples_Chapter
Collections_Examples: theory Refine_Monadic_Examples_Chapter
Collections_Examples: theory Buchi_Graph_Basic
Collections_Examples: theory Exploration
Collections_Examples: theory PerformanceTest
Collections_Examples: theory Bfs_Impl
Collections_Examples: theory Foreach_Refine
Collections_Examples: theory ICF_Only_Test
Collections_Examples: theory Exploration_DFS
Collections_Examples: theory Refine_Fold
Collections_Examples: theory itp_2010
Collections_Examples: theory Refine_Monadic_Examples
Collections_Examples: theory Simple_DFS
Collections_Examples: theory Succ_Graph
Collections_Examples: theory ICF_Test
Collections_Examples: theory Coll_Test
Collections_Examples: theory Nested_DFS
Collections_Examples: theory ICF_Examples
Akra_Bazzi: theory Eval_Numeral
Akra_Bazzi: theory Akra_Bazzi_Library
Akra_Bazzi: theory Akra_Bazzi_Asymptotics
Akra_Bazzi: theory Akra_Bazzi_Real
Akra_Bazzi: theory Master_Theorem
Akra_Bazzi: theory Akra_Bazzi_Method
Akra_Bazzi: theory Akra_Bazzi_Approximation
Akra_Bazzi: theory Master_Theorem_Examples
Timing Akra_Bazzi (4 threads, 111.316s elapsed time, 378.148s cpu time, 9.068s GC time, factor 3.40)
Finished Akra_Bazzi (0:01:55 elapsed time, 0:06:22 cpu time, factor 3.31)
Collections_Examples: theory Collection_Autoref_Examples
Pi_Calculus: theory Early_Semantics
Pi_Calculus: theory Late_Semantics
Collections_Examples: theory Collection_Examples
Pi_Calculus: theory Early_Tau_Chain
Pi_Calculus: theory Weak_Early_Step_Semantics
Pi_Calculus: theory Strong_Early_Sim
Pi_Calculus: theory Weak_Early_Semantics
Pi_Calculus: theory Strong_Early_Bisim
Pi_Calculus: theory Strong_Early_Sim_Pres
Pi_Calculus: theory Strong_Early_Bisim_Subst
Pi_Calculus: theory Strong_Early_Bisim_Pres
Pi_Calculus: theory Weak_Early_Sim
Pi_Calculus: theory Late_Semantics1
Pi_Calculus: theory Strong_Early_Bisim_Subst_Pres
Timing Collections_Examples (4 threads, 107.422s elapsed time, 279.768s cpu time, 9.312s GC time, factor 2.60)
Finished Collections_Examples (0:01:58 elapsed time, 0:04:56 cpu time, factor 2.50)
Pi_Calculus: theory Late_Tau_Chain
Running Random_Graph_Subgraph_Threshold ...
Pi_Calculus: theory Strong_Late_Sim
Pi_Calculus: theory Weak_Early_Bisim
Pi_Calculus: theory Weak_Early_Sim_Pres
Pi_Calculus: theory Weak_Late_Step_Semantics
Pi_Calculus: theory Weak_Early_Step_Sim
Pi_Calculus: theory Strong_Late_Bisim
Pi_Calculus: theory Weak_Early_Bisim_Subst
Pi_Calculus: theory Weak_Early_Cong
Pi_Calculus: theory Weak_Early_Step_Sim_Pres
Pi_Calculus: theory Weak_Late_Semantics
Pi_Calculus: theory Strong_Late_Bisim_Subst
Pi_Calculus: theory Strong_Late_Sim_Pres
Pi_Calculus: theory Strong_Late_Sim_SC
Pi_Calculus: theory Weak_Early_Cong_Subst
Pi_Calculus: theory Weak_Late_Sim
Pi_Calculus: theory Strong_Late_Bisim_Pres
Pi_Calculus: theory Strong_Late_Bisim_Subst_Pres
Pi_Calculus: theory Strong_Late_Bisim_SC
Pi_Calculus: theory Strong_Late_Bisim_Subst_SC
Pi_Calculus: theory Strong_Late_Expansion_Law
Pi_Calculus: theory Strong_Early_Late_Comp
Pi_Calculus: theory Weak_Late_Bisim
Pi_Calculus: theory Strong_Late_Axiomatisation
Pi_Calculus: theory Weak_Late_Bisim_SC
Pi_Calculus: theory Strong_Early_Bisim_SC
Pi_Calculus: theory Weak_Early_Bisim_SC
Pi_Calculus: theory Weak_Late_Bisim_Subst
Pi_Calculus: theory Weak_Late_Sim_Pres
Pi_Calculus: theory Weak_Early_Bisim_Pres
Pi_Calculus: theory Weak_Late_Step_Sim
Pi_Calculus: theory Weak_Late_Bisim_Pres
Random_Graph_Subgraph_Threshold: theory Code_Abstract_Nat
Random_Graph_Subgraph_Threshold: theory Dense_Linear_Order
Random_Graph_Subgraph_Threshold: theory Code_Target_Int
Random_Graph_Subgraph_Threshold: theory Lattice_Algebras
Pi_Calculus: theory Weak_Early_Cong_Pres
Random_Graph_Subgraph_Threshold: theory Code_Target_Nat
Pi_Calculus: theory Weak_Early_Cong_Subst_Pres
Random_Graph_Subgraph_Threshold: theory Girth_Chromatic_Misc
Random_Graph_Subgraph_Threshold: theory Code_Target_Numeral
Random_Graph_Subgraph_Threshold: theory Ugraphs
Pi_Calculus: theory Weak_Late_Cong
Pi_Calculus: theory Weak_Late_Step_Sim_Pres
Pi_Calculus: theory Weak_Late_Cong_Subst
Pi_Calculus: theory Weak_Late_Cong_Pres
Pi_Calculus: theory Weak_Late_Cong_Subst_SC
Random_Graph_Subgraph_Threshold: theory Float
Random_Graph_Subgraph_Threshold: theory Approximation
Random_Graph_Subgraph_Threshold: theory Girth_Chromatic
Timing Pi_Calculus (4 threads, 103.905s elapsed time, 369.860s cpu time, 7.908s GC time, factor 3.56)
Finished Pi_Calculus (0:01:46 elapsed time, 0:06:12 cpu time, factor 3.49)
Running SATSolverVerification ...
Random_Graph_Subgraph_Threshold: theory Ugraph_Misc
Random_Graph_Subgraph_Threshold: theory Prob_Lemmas
Random_Graph_Subgraph_Threshold: theory Ugraph_Lemmas
Random_Graph_Subgraph_Threshold: theory Ugraph_Properties
Random_Graph_Subgraph_Threshold: theory Subgraph_Threshold
SATSolverVerification: theory MoreList
SATSolverVerification: theory CNF
SATSolverVerification: theory Trail
SATSolverVerification: theory SatSolverVerification
SATSolverVerification: theory BasicDPLL
SATSolverVerification: theory KrsticGoel
SATSolverVerification: theory NieuwenhuisOliverasTinelli
SATSolverVerification: theory SatSolverCode
Timing Random_Graph_Subgraph_Threshold (4 threads, 99.703s elapsed time, 287.876s cpu time, 6.004s GC time, factor 2.89)
Finished Random_Graph_Subgraph_Threshold (0:01:45 elapsed time, 0:04:53 cpu time, factor 2.78)
SATSolverVerification: theory AssertLiteral
SATSolverVerification: theory ConflictAnalysis
SATSolverVerification: theory Decide
SATSolverVerification: theory UnitPropagate
SATSolverVerification: theory Initialization
SATSolverVerification: theory SolveLoop
SATSolverVerification: theory FunctionalImplementation
Timing SATSolverVerification (4 threads, 96.219s elapsed time, 357.516s cpu time, 5.816s GC time, factor 3.72)
Finished SATSolverVerification (0:01:42 elapsed time, 0:06:03 cpu time, factor 3.56)
Running Dijkstra_Shortest_Path ...
Timing AWN (4 threads, 91.079s elapsed time, 298.880s cpu time, 8.700s GC time, factor 3.28)
Finished AWN (0:01:33 elapsed time, 0:05:01 cpu time, factor 3.22)
Girth_Chromatic: theory Code_Abstract_Nat
Girth_Chromatic: theory Dense_Linear_Order
Girth_Chromatic: theory Code_Target_Int
Girth_Chromatic: theory Lattice_Algebras
Girth_Chromatic: theory Code_Target_Nat
Girth_Chromatic: theory Girth_Chromatic_Misc
Girth_Chromatic: theory Code_Target_Numeral
Girth_Chromatic: theory Ugraphs
Dijkstra_Shortest_Path: theory Dijkstra_Misc
Dijkstra_Shortest_Path: theory Graph
Dijkstra_Shortest_Path: theory Introduction
Dijkstra_Shortest_Path: theory Weight
Dijkstra_Shortest_Path: theory GraphSpec
Dijkstra_Shortest_Path: theory Dijkstra
Dijkstra_Shortest_Path: theory GraphGA
Girth_Chromatic: theory Approximation
Dijkstra_Shortest_Path: theory GraphByMap
Dijkstra_Shortest_Path: theory HashGraphImpl
Dijkstra_Shortest_Path: theory Dijkstra_Impl
Dijkstra_Shortest_Path: theory Dijkstra_Impl_Adet
Dijkstra_Shortest_Path: theory Test
Girth_Chromatic: theory Girth_Chromatic
Timing Dijkstra_Shortest_Path (4 threads, 86.764s elapsed time, 152.784s cpu time, 4.120s GC time, factor 1.76)
Finished Dijkstra_Shortest_Path (0:01:37 elapsed time, 0:05:08 cpu time, factor 3.17)
Timing Girth_Chromatic (4 threads, 85.366s elapsed time, 227.676s cpu time, 5.204s GC time, factor 2.67)
Finished Girth_Chromatic (0:01:30 elapsed time, 0:03:53 cpu time, factor 2.56)
Derangements: theory Code_Abstract_Nat
Derangements: theory Permutations
Derangements: theory Dense_Linear_Order
Derangements: theory Code_Target_Int
Derangements: theory Code_Target_Nat
Derangements: theory Lattice_Algebras
Derangements: theory Code_Target_Numeral
Multirelations: theory C_Algebras
Derangements: theory Approximation
Multirelations: theory Multirelations
Timing Multirelations (4 threads, 85.455s elapsed time, 144.316s cpu time, 3.848s GC time, factor 1.69)
Finished Multirelations (0:01:29 elapsed time, 0:07:05 cpu time, factor 4.76)
Running Amortized_Complexity ...
Amortized_Complexity: theory Tree
Amortized_Complexity: theory List_Index
Derangements: theory Derangements
Amortized_Complexity: theory Tree_Multiset
Amortized_Complexity: theory Splay_Tree
Amortized_Complexity: theory Skew_Heap
Timing Derangements (4 threads, 101.015s elapsed time, 222.684s cpu time, 5.416s GC time, factor 2.20)
Finished Derangements (0:01:43 elapsed time, 0:03:45 cpu time, factor 2.17)
Rep_Fin_Groups: theory Function_Algebras
Rep_Fin_Groups: theory Infinite_Set
Rep_Fin_Groups: theory More_List
Rep_Fin_Groups: theory Set_Algebras
Rep_Fin_Groups: theory Polynomial
Rep_Fin_Groups: theory Rep_Fin_Groups
Amortized_Complexity: theory Lemmas_log
Amortized_Complexity: theory Amor
Amortized_Complexity: theory Priority_Queue_ops
Amortized_Complexity: theory Splay_Tree_Analysis_Base
Amortized_Complexity: theory Table
Amortized_Complexity: theory Pairing_Heap_List
Amortized_Complexity: theory Pairing_Heap
Amortized_Complexity: theory Splay_Tree_Analysis
Amortized_Complexity: theory Splay_Tree_Analysis_Optimal
Amortized_Complexity: theory Skew_Heap_Analysis
Amortized_Complexity: theory Splay_Heap
Timing Amortized_Complexity (4 threads, 81.100s elapsed time, 239.176s cpu time, 4.516s GC time, factor 2.95)
Finished Amortized_Complexity (0:01:26 elapsed time, 0:04:04 cpu time, factor 2.82)
Running Abortable_Linearizable_Modules ...
Abortable_Linearizable_Modules: theory Sequences
Abortable_Linearizable_Modules: theory IOA
Abortable_Linearizable_Modules: theory RDR
Timing Rep_Fin_Groups (4 threads, 79.203s elapsed time, 285.380s cpu time, 5.116s GC time, factor 3.60)
Finished Rep_Fin_Groups (0:01:21 elapsed time, 0:04:47 cpu time, factor 3.52)
Running BytecodeLogicJmlTypes ...
Abortable_Linearizable_Modules: theory Consensus
BytecodeLogicJmlTypes: theory AssocLists
BytecodeLogicJmlTypes: theory Language
Abortable_Linearizable_Modules: theory Simulations
Abortable_Linearizable_Modules: theory SLin
BytecodeLogicJmlTypes: theory Logic
BytecodeLogicJmlTypes: theory MultiStep
BytecodeLogicJmlTypes: theory Reachability
BytecodeLogicJmlTypes: theory Cachera
BytecodeLogicJmlTypes: theory Sound
Abortable_Linearizable_Modules: theory Idempotence
Timing Abortable_Linearizable_Modules (4 threads, 78.966s elapsed time, 160.792s cpu time, 4.256s GC time, factor 2.04)
Finished Abortable_Linearizable_Modules (0:01:21 elapsed time, 0:02:43 cpu time, factor 2.00)
Running SequentInvertibility ...
SequentInvertibility: theory Multiset
Timing BytecodeLogicJmlTypes (4 threads, 78.322s elapsed time, 229.636s cpu time, 3.612s GC time, factor 2.93)
Finished BytecodeLogicJmlTypes (0:01:20 elapsed time, 0:03:52 cpu time, factor 2.87)
SequentInvertibility: theory ModalSequents
SequentInvertibility: theory MultiSequents
SequentInvertibility: theory SRCTransforms
SequentInvertibility: theory SingleSuccedent
Knot_Theory: theory Fraction_Field
Knot_Theory: theory Polynomial
SequentInvertibility: theory NominalSequents
Knot_Theory: theory Tangle_Relation
Knot_Theory: theory Preliminaries
Knot_Theory: theory Tangle_Algebra
SequentInvertibility: theory SequentInvertibility
Knot_Theory: theory Tangle_Moves
Knot_Theory: theory Link_Algebra
Knot_Theory: theory Kauffman_Matrix
Knot_Theory: theory Computations
Knot_Theory: theory Linkrel_Kauffman
Knot_Theory: theory Kauffman_Invariance
Knot_Theory: theory Knot_Theory
Timing SequentInvertibility (4 threads, 74.850s elapsed time, 257.048s cpu time, 10.448s GC time, factor 3.43)
Finished SequentInvertibility (0:01:17 elapsed time, 0:04:19 cpu time, factor 3.35)
Timing Knot_Theory (4 threads, 68.568s elapsed time, 249.820s cpu time, 4.260s GC time, factor 3.64)
Finished Knot_Theory (0:01:14 elapsed time, 0:04:13 cpu time, factor 3.42)
Running LinearQuantifierElim ...
Call_Arity: theory BalancedTraces
Call_Arity: theory List-Interleavings
Call_Arity: theory AList-Utils-HOLCF
Call_Arity: theory Cardinality-Domain
Call_Arity: theory Arity-Nominal
Call_Arity: theory Env-Set-Cpo
Call_Arity: theory CoCallGraph
Call_Arity: theory Cardinality-Domain-Lists
LinearQuantifierElim: theory Logic
Call_Arity: theory ArityAnalysisSig
Call_Arity: theory ArityAnalysisAbinds
Call_Arity: theory EtaExpansion
Call_Arity: theory SestoftConf
Call_Arity: theory TransformTools
Call_Arity: theory CoCallGraph-Nominal
Call_Arity: theory CoCallAnalysisSig
Call_Arity: theory ArityAnalysisSpec
Call_Arity: theory TrivialArityAnal
Call_Arity: theory ArityAnalysisFix
Call_Arity: theory CoCallAnalysisBinds
Call_Arity: theory ArityAnalysisFixProps
Call_Arity: theory CoCallAritySig
Call_Arity: theory AbstractTransform
Call_Arity: theory CoCallAnalysisSpec
Call_Arity: theory ArityAnalysisStack
LinearQuantifierElim: theory QE
Call_Arity: theory CardinalityAnalysisSig
Call_Arity: theory ArityConsistent
LinearQuantifierElim: theory PresArith
LinearQuantifierElim: theory DLO
Call_Arity: theory EtaExpansionSafe
LinearQuantifierElim: theory LinArith
Call_Arity: theory CardinalityAnalysisSpec
Call_Arity: theory SestoftCorrect
Call_Arity: theory CoCallAnalysisImpl
Call_Arity: theory ArityEtaExpansion
Call_Arity: theory NoCardinalityAnalysis
Call_Arity: theory ArityEtaExpansionSafe
Call_Arity: theory CoCallImplSafe
Call_Arity: theory TTree-HOLCF
Call_Arity: theory ArityTransform
LinearQuantifierElim: theory Cooper
LinearQuantifierElim: theory QEpres
LinearQuantifierElim: theory QEdlo
LinearQuantifierElim: theory QEdlo_fr
Call_Arity: theory ArityAnalysisCorrDenotational
LinearQuantifierElim: theory QEdlo_inf
LinearQuantifierElim: theory FRE
LinearQuantifierElim: theory QEdlo_ex
LinearQuantifierElim: theory QElin
LinearQuantifierElim: theory QElin_inf
LinearQuantifierElim: theory QElin_opt
Call_Arity: theory CallArityEnd2End
Call_Arity: theory ArityTransformSafe
Call_Arity: theory CardArityTransformSafe
Call_Arity: theory CoCallGraph-TTree
Call_Arity: theory TTreeAnalysisSig
Call_Arity: theory CoCallImplTTree
Call_Arity: theory TTreeAnalysisSpec
Call_Arity: theory TTreeImplCardinality
Call_Arity: theory CoCallImplTTreeSafe
Call_Arity: theory TTreeImplCardinalitySafe
Call_Arity: theory CallArityEnd2EndSafe
Timing Call_Arity (4 threads, 72.920s elapsed time, 250.992s cpu time, 8.948s GC time, factor 3.44)
Finished Call_Arity (0:01:21 elapsed time, 0:04:15 cpu time, factor 3.14)
LinearQuantifierElim: theory CertDlo
LinearQuantifierElim: theory CertLin
Timing LinearQuantifierElim (4 threads, 74.942s elapsed time, 229.816s cpu time, 15.192s GC time, factor 3.07)
Finished LinearQuantifierElim (0:01:20 elapsed time, 0:03:55 cpu time, factor 2.92)
Running Separation_Logic_Imperative_HOL ...
Separation_Logic_Imperative_HOL: theory List_More
Separation_Logic_Imperative_HOL: theory More_Bits_Int
Separation_Logic_Imperative_HOL: theory Quicksort
Separation_Logic_Imperative_HOL: theory Heap
Separation_Logic_Imperative_HOL: theory Syntax_Match
Separation_Logic_Imperative_HOL: theory Misc
BDD: theory ShareReduceRepListProof
Separation_Logic_Imperative_HOL: theory Heap_Monad
BDD: theory NormalizeTotalProof
Separation_Logic_Imperative_HOL: theory Bits_Integer
Separation_Logic_Imperative_HOL: theory Word_Misc
Separation_Logic_Imperative_HOL: theory Array
Separation_Logic_Imperative_HOL: theory Ref
Separation_Logic_Imperative_HOL: theory Imperative_HOL
Separation_Logic_Imperative_HOL: theory Imperative_HOL_Add
Separation_Logic_Imperative_HOL: theory Sep_Misc
Separation_Logic_Imperative_HOL: theory Code_Target_Bits_Int
Separation_Logic_Imperative_HOL: theory Uint32
Separation_Logic_Imperative_HOL: theory Code_Target_ICF
Separation_Logic_Imperative_HOL: theory HashCode
Separation_Logic_Imperative_HOL: theory Run
Separation_Logic_Imperative_HOL: theory Assertions
Separation_Logic_Imperative_HOL: theory Partial_Equivalence_Relation
Separation_Logic_Imperative_HOL: theory Hoare_Triple
Separation_Logic_Imperative_HOL: theory Automation
Separation_Logic_Imperative_HOL: theory Sep_Main
Separation_Logic_Imperative_HOL: theory Imp_List_Spec
Separation_Logic_Imperative_HOL: theory Imp_Map_Spec
Separation_Logic_Imperative_HOL: theory Imp_Set_Spec
Separation_Logic_Imperative_HOL: theory List_Seg
Separation_Logic_Imperative_HOL: theory Union_Find
Separation_Logic_Imperative_HOL: theory Hash_Table
Separation_Logic_Imperative_HOL: theory Circ_List
Separation_Logic_Imperative_HOL: theory Open_List
Separation_Logic_Imperative_HOL: theory Hash_Map
Separation_Logic_Imperative_HOL: theory Hash_Map_Impl
Separation_Logic_Imperative_HOL: theory Hash_Set_Impl
Separation_Logic_Imperative_HOL: theory Idioms
Separation_Logic_Imperative_HOL: theory To_List_GA
Timing BDD (4 threads, 74.547s elapsed time, 257.448s cpu time, 3.364s GC time, factor 3.45)
Finished BDD (0:01:18 elapsed time, 0:04:21 cpu time, factor 3.33)
Timing Separation_Logic_Imperative_HOL (4 threads, 71.795s elapsed time, 181.380s cpu time, 6.140s GC time, factor 2.53)
Finished Separation_Logic_Imperative_HOL (0:01:17 elapsed time, 0:04:41 cpu time, factor 3.63)
Sort_Encodings: theory Nat_Bijection
Sort_Encodings: theory Infinite_Set
Sort_Encodings: theory Old_Datatype
Sort_Encodings: theory Countable
Sort_Encodings: theory Countable_Set
Sort_Encodings: theory Countable_Set_Type
MSO_Examples: theory M2L_Examples
MSO_Examples: theory WS1S_Examples
Sort_Encodings: theory Preliminaries
Sort_Encodings: theory TermsAndClauses
Sort_Encodings: theory Mcalc2C
Sort_Encodings: theory T_G_Prelim
Sort_Encodings: theory Encodings
Timing Sort_Encodings (4 threads, 64.081s elapsed time, 157.716s cpu time, 8.672s GC time, factor 2.46)
Finished Sort_Encodings (0:01:07 elapsed time, 0:02:40 cpu time, factor 2.38)
LightweightJava: theory Infinite_Set
LightweightJava: theory Multiset
LightweightJava: theory Lightweight_Java_Definition
LightweightJava: theory Lightweight_Java_Equivalence
LightweightJava: theory Lightweight_Java_Proof
Timing MSO_Examples (4 threads, 85.503s elapsed time, 193.892s cpu time, 4.276s GC time, factor 2.27)
Finished MSO_Examples (0:01:38 elapsed time, 0:03:21 cpu time, factor 2.06)
Running ComponentDependencies ...
ComponentDependencies: theory DataDependenciesConcreteValues
ComponentDependencies: theory DataDependencies
ComponentDependencies: theory DataDependenciesCaseStudy
Timing LightweightJava (4 threads, 61.839s elapsed time, 138.064s cpu time, 3.604s GC time, factor 2.23)
Finished LightweightJava (0:01:04 elapsed time, 0:02:20 cpu time, factor 2.18)
Running Vickrey_Clarke_Groves ...
Vickrey_Clarke_Groves: theory Argmax
Vickrey_Clarke_Groves: theory SetUtils
Vickrey_Clarke_Groves: theory Partitions
Vickrey_Clarke_Groves: theory RelationOperators
Vickrey_Clarke_Groves: theory RelationProperties
Vickrey_Clarke_Groves: theory MiscTools
Vickrey_Clarke_Groves: theory StrictCombinatorialAuction
Vickrey_Clarke_Groves: theory Universes
Vickrey_Clarke_Groves: theory UniformTieBreaking
Vickrey_Clarke_Groves: theory CombinatorialAuction
Vickrey_Clarke_Groves: theory CombinatorialAuctionCodeExtraction
Timing ComponentDependencies (4 threads, 58.740s elapsed time, 178.540s cpu time, 5.796s GC time, factor 3.04)
Finished ComponentDependencies (0:01:01 elapsed time, 0:03:01 cpu time, factor 2.95)
UpDown_Scheme: theory Quicksort
UpDown_Scheme: theory List_More
UpDown_Scheme: theory Option_ord
UpDown_Scheme: theory Product_Lexorder
UpDown_Scheme: theory Syntax_Match
UpDown_Scheme: theory Heap_Monad
UpDown_Scheme: theory Imperative_HOL
UpDown_Scheme: theory Imperative_HOL_Add
UpDown_Scheme: theory Sep_Misc
UpDown_Scheme: theory Assertions
UpDown_Scheme: theory Hoare_Triple
UpDown_Scheme: theory Automation
UpDown_Scheme: theory Sep_Main
UpDown_Scheme: theory Grid_Point
UpDown_Scheme: theory UpDown_Scheme
UpDown_Scheme: theory Triangular_Function
UpDown_Scheme: theory Imperative
Timing Vickrey_Clarke_Groves (4 threads, 59.736s elapsed time, 201.168s cpu time, 3.708s GC time, factor 3.37)
Finished Vickrey_Clarke_Groves (0:01:05 elapsed time, 0:03:27 cpu time, factor 3.15)
Regular-Sets: theory Regular_Set
Regular-Sets: theory Regular_Exp
Regular-Sets: theory Regular_Exp2
Regular-Sets: theory Equivalence_Checking2
Regular-Sets: theory Derivatives
Regular-Sets: theory NDerivative
Regular-Sets: theory Relation_Interpretation
Regular-Sets: theory Equivalence_Checking
Regular-Sets: theory Regexp_Method
Regular-Sets: theory pEquivalence_Checking
Timing UpDown_Scheme (4 threads, 57.682s elapsed time, 195.960s cpu time, 4.324s GC time, factor 3.40)
Finished UpDown_Scheme (0:01:03 elapsed time, 0:03:22 cpu time, factor 3.20)
Tarskis_Geometry: theory Congruence
Tarskis_Geometry: theory Lattice
Tarskis_Geometry: theory Group
Tarskis_Geometry: theory Action
Tarskis_Geometry: theory Quadratic_Discriminant
Tarskis_Geometry: theory Metric
Tarskis_Geometry: theory Miscellany
Tarskis_Geometry: theory Linear_Algebra2
Tarskis_Geometry: theory Tarski
Tarskis_Geometry: theory Euclid_Tarski
Tarskis_Geometry: theory Projective
Tarskis_Geometry: theory Hyperbolic_Tarski
Timing Regular-Sets (4 threads, 57.745s elapsed time, 124.620s cpu time, 3.460s GC time, factor 2.16)
Finished Regular-Sets (0:01:03 elapsed time, 0:02:15 cpu time, factor 2.12)
Running SIFUM_Type_Systems ...
SIFUM_Type_Systems: theory Lattice_Syntax
SIFUM_Type_Systems: theory Preliminaries
SIFUM_Type_Systems: theory Language
SIFUM_Type_Systems: theory Security
SIFUM_Type_Systems: theory Compositionality
SIFUM_Type_Systems: theory LocallySoundModeUse
SIFUM_Type_Systems: theory TypeSystem
Timing Tarskis_Geometry (4 threads, 58.615s elapsed time, 216.956s cpu time, 3.140s GC time, factor 3.70)
Finished Tarskis_Geometry (0:01:02 elapsed time, 0:03:41 cpu time, factor 3.52)
Running Probabilistic_System_Zoo ...
Probabilistic_System_Zoo: theory Eisbach
Probabilistic_System_Zoo: theory Order_Union
Probabilistic_System_Zoo: theory Cardinal_Notations
Probabilistic_System_Zoo: theory Fun_More
Probabilistic_System_Zoo: theory Order_Relation_More
Probabilistic_System_Zoo: theory Wellorder_Extension
Probabilistic_System_Zoo: theory Wellfounded_More
Probabilistic_System_Zoo: theory Wellorder_Relation
Probabilistic_System_Zoo: theory Wellorder_Embedding
Probabilistic_System_Zoo: theory Wellorder_Constructions
Probabilistic_System_Zoo: theory Cardinal_Order_Relation
Probabilistic_System_Zoo: theory Ordinal_Arithmetic
Probabilistic_System_Zoo: theory Cardinal_Arithmetic
Probabilistic_System_Zoo: theory Cardinals
Probabilistic_System_Zoo: theory Bounded_Set
Probabilistic_System_Zoo: theory Nonempty_Bounded_Set
Probabilistic_System_Zoo: theory Probabilistic_Hierarchy
Timing SIFUM_Type_Systems (4 threads, 57.977s elapsed time, 182.064s cpu time, 5.012s GC time, factor 3.14)
Finished SIFUM_Type_Systems (0:01:00 elapsed time, 0:03:04 cpu time, factor 3.04)
Free-Groups: theory Cardinal_Notations
Free-Groups: theory Order_Union
Free-Groups: theory Commutation
Free-Groups: theory Congruence
Free-Groups: theory Order_Relation_More
Free-Groups: theory Wellfounded_More
Free-Groups: theory Wellorder_Relation
Free-Groups: theory Wellorder_Embedding
Free-Groups: theory Wellorder_Constructions
Free-Groups: theory Cardinal_Order_Relation
Free-Groups: theory FiniteProduct
Probabilistic_System_Zoo: theory Vardi
Timing Probabilistic_System_Zoo (4 threads, 56.655s elapsed time, 154.276s cpu time, 4.596s GC time, factor 2.72)
Finished Probabilistic_System_Zoo (0:01:02 elapsed time, 0:02:39 cpu time, factor 2.56)
RSAPSS: theory Code_Target_Int
RSAPSS: theory Code_Abstract_Nat
RSAPSS: theory Code_Target_Nat
RSAPSS: theory Code_Target_Numeral
RSAPSS: theory UniqueFactorization
Free-Groups: theory Cancelation
Free-Groups: theory Generators
Free-Groups: theory FreeGroups
Free-Groups: theory PingPongLemma
Free-Groups: theory Isomorphisms
Timing Free-Groups (4 threads, 57.167s elapsed time, 196.524s cpu time, 6.524s GC time, factor 3.44)
Finished Free-Groups (0:00:59 elapsed time, 0:03:19 cpu time, factor 3.33)
Statecharts: theory CarAudioSystem
Timing RSAPSS (4 threads, 55.826s elapsed time, 200.224s cpu time, 4.980s GC time, factor 3.59)
Finished RSAPSS (0:00:58 elapsed time, 0:03:22 cpu time, factor 3.47)
Running Probabilistic_System_Zoo-Non_BNFs ...
Probabilistic_System_Zoo-Non_BNFs: theory Eisbach
Probabilistic_System_Zoo-Non_BNFs: theory Cardinal_Notations
Probabilistic_System_Zoo-Non_BNFs: theory Fun_More
Probabilistic_System_Zoo-Non_BNFs: theory Order_Union
Probabilistic_System_Zoo-Non_BNFs: theory Order_Relation_More
Probabilistic_System_Zoo-Non_BNFs: theory Wellorder_Extension
Probabilistic_System_Zoo-Non_BNFs: theory Wellfounded_More
Probabilistic_System_Zoo-Non_BNFs: theory Wellorder_Relation
Probabilistic_System_Zoo-Non_BNFs: theory Wellorder_Embedding
Probabilistic_System_Zoo-Non_BNFs: theory Wellorder_Constructions
Probabilistic_System_Zoo-Non_BNFs: theory Cardinal_Order_Relation
Probabilistic_System_Zoo-Non_BNFs: theory Ordinal_Arithmetic
Probabilistic_System_Zoo-Non_BNFs: theory Cardinal_Arithmetic
Probabilistic_System_Zoo-Non_BNFs: theory Cardinals
Probabilistic_System_Zoo-Non_BNFs: theory Bounded_Set
Probabilistic_System_Zoo-Non_BNFs: theory Nonempty_Bounded_Set
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_Hierarchy
Timing Statecharts (4 threads, 53.374s elapsed time, 187.396s cpu time, 2.828s GC time, factor 3.51)
Finished Statecharts (0:00:55 elapsed time, 0:03:09 cpu time, factor 3.40)
Probabilistic_System_Zoo-Non_BNFs: theory Vardi
AutoFocus-Stream: theory ListSlice
AutoFocus-Stream: theory AF_Stream
Probabilistic_System_Zoo-Non_BNFs: theory Finitely_Bounded_Set_Counterexample
Probabilistic_System_Zoo-Non_BNFs: theory Vardi_Counterexample
AutoFocus-Stream: theory AF_Stream_Exec
AutoFocus-Stream: theory IL_AF_Stream
AutoFocus-Stream: theory IL_AF_Stream_Exec
Timing Probabilistic_System_Zoo-Non_BNFs (4 threads, 51.713s elapsed time, 166.800s cpu time, 6.128s GC time, factor 3.23)
Finished Probabilistic_System_Zoo-Non_BNFs (0:00:57 elapsed time, 0:02:52 cpu time, factor 3.00)
Running Koenigsberg_Friendship ...
Koenigsberg_Friendship: theory MoreGraph
Koenigsberg_Friendship: theory FriendshipTheory
Koenigsberg_Friendship: theory KoenigsbergBridge
Timing AutoFocus-Stream (4 threads, 50.633s elapsed time, 162.092s cpu time, 1.512s GC time, factor 3.20)
Finished AutoFocus-Stream (0:01:01 elapsed time, 0:02:48 cpu time, factor 2.75)
VectorSpace: theory FunctionLemmas
VectorSpace: theory RingModuleFacts
VectorSpace: theory MonoidSums
VectorSpace: theory LinearCombinations
Timing Koenigsberg_Friendship (4 threads, 50.380s elapsed time, 183.704s cpu time, 3.680s GC time, factor 3.65)
Finished Koenigsberg_Friendship (0:00:54 elapsed time, 0:03:06 cpu time, factor 3.41)
Running Formula_Derivatives-Examples ...
VectorSpace: theory VectorSpace
Formula_Derivatives-Examples: theory Presburger_Examples
Formula_Derivatives-Examples: theory Show
Formula_Derivatives-Examples: theory WS1S_Alt_Examples
Formula_Derivatives-Examples: theory WS1S_Examples
Formula_Derivatives-Examples: theory WS1S_Presburger_Examples
Formula_Derivatives-Examples: theory Show_Instances
Formula_Derivatives-Examples: theory WS1S_Nameful_Examples
Timing VectorSpace (4 threads, 49.501s elapsed time, 145.700s cpu time, 3.516s GC time, factor 2.94)
Finished VectorSpace (0:00:53 elapsed time, 0:02:29 cpu time, factor 2.81)
pGCL: theory StructuredReasoning
Timing Formula_Derivatives-Examples (4 threads, 53.877s elapsed time, 164.336s cpu time, 12.036s GC time, factor 3.05)
Finished Formula_Derivatives-Examples (0:01:14 elapsed time, 0:02:58 cpu time, factor 2.39)
Timing pGCL (4 threads, 51.267s elapsed time, 191.124s cpu time, 2.660s GC time, factor 3.73)
Finished pGCL (0:00:55 elapsed time, 0:03:15 cpu time, factor 3.52)
Circus: theory Reactive_Processes
Circus: theory Denotational_Semantics
Timing PCF (4 threads, 47.867s elapsed time, 143.716s cpu time, 2.948s GC time, factor 3.00)
Finished PCF (0:00:51 elapsed time, 0:02:26 cpu time, factor 2.88)
Circus: theory Refinement_Example
Timing Circus (4 threads, 47.632s elapsed time, 147.108s cpu time, 3.104s GC time, factor 3.09)
Finished Circus (0:00:50 elapsed time, 0:02:30 cpu time, factor 2.96)
Timing SIFPL (4 threads, 45.684s elapsed time, 127.152s cpu time, 3.760s GC time, factor 2.78)
Finished SIFPL (0:00:48 elapsed time, 0:02:09 cpu time, factor 2.68)
Tree-Automata: theory Exploration
Timing Valuation (4 threads, 43.970s elapsed time, 145.816s cpu time, 2.988s GC time, factor 3.32)
Finished Valuation (0:00:57 elapsed time, 0:02:32 cpu time, factor 2.66)
Running Prime_Harmonic_Series ...
Prime_Harmonic_Series: theory Fib
Prime_Harmonic_Series: theory Primes
Prime_Harmonic_Series: theory Congruence
Prime_Harmonic_Series: theory Multiset
Prime_Harmonic_Series: theory Cong
Prime_Harmonic_Series: theory Eratosthenes
Prime_Harmonic_Series: theory Lattice
Prime_Harmonic_Series: theory Group
Prime_Harmonic_Series: theory UniqueFactorization
Prime_Harmonic_Series: theory FiniteProduct
Prime_Harmonic_Series: theory Ring
Prime_Harmonic_Series: theory MiscAlgebra
Prime_Harmonic_Series: theory Residues
Tree-Automata: theory Ta_impl_codegen
Prime_Harmonic_Series: theory Number_Theory
Timing Tree-Automata (4 threads, 43.832s elapsed time, 120.836s cpu time, 2.868s GC time, factor 2.76)
Finished Tree-Automata (0:00:54 elapsed time, 0:02:11 cpu time, factor 2.41)
Prime_Harmonic_Series: theory Prime_Harmonic_Misc
Prime_Harmonic_Series: theory Squarefree_Nat
Prime_Harmonic_Series: theory Prime_Harmonic
Timing Prime_Harmonic_Series (4 threads, 42.705s elapsed time, 150.904s cpu time, 3.620s GC time, factor 3.53)
Finished Prime_Harmonic_Series (0:00:47 elapsed time, 0:02:35 cpu time, factor 3.30)
Hermite: theory Hermite_IArrays
Timing Splay_Tree (4 threads, 40.803s elapsed time, 83.920s cpu time, 0.580s GC time, factor 2.06)
Finished Splay_Tree (0:00:43 elapsed time, 0:01:26 cpu time, factor 1.99)
Heard_Of: theory Omega_Words_Fun
Heard_Of: theory StutterEquivalence
Heard_Of: theory OneThirdRuleDefs
Heard_Of: theory LastVotingDefs
Heard_Of: theory LastVotingProof
Heard_Of: theory OneThirdRuleProof
Timing Hermite (4 threads, 38.135s elapsed time, 106.964s cpu time, 1.828s GC time, factor 2.80)
Finished Hermite (0:00:44 elapsed time, 0:01:52 cpu time, factor 2.51)
Running WHATandWHERE_Security ...
WHATandWHERE_Security: theory Types
WHATandWHERE_Security: theory Expr
WHATandWHERE_Security: theory MWLs
WHATandWHERE_Security: theory WHATWHERE_Security
WHATandWHERE_Security: theory Up_To_Technique
WHATandWHERE_Security: theory Domain_example
WHATandWHERE_Security: theory Parallel_Composition
WHATandWHERE_Security: theory WHATWHERE_Secure_Skip_Assign
WHATandWHERE_Security: theory Language_Composition
WHATandWHERE_Security: theory Type_System
WHATandWHERE_Security: theory Type_System_example
Timing Heard_Of (4 threads, 39.493s elapsed time, 137.684s cpu time, 3.000s GC time, factor 3.49)
Finished Heard_Of (0:00:42 elapsed time, 0:02:20 cpu time, factor 3.34)
SumSquares: theory BijectionRel
SumSquares: theory Infinite_Set
SumSquares: theory EulerFermat
SumSquares: theory Permutation
SumSquares: theory Factorization
SumSquares: theory Quadratic_Reciprocity
Timing WHATandWHERE_Security (4 threads, 40.690s elapsed time, 141.212s cpu time, 3.180s GC time, factor 3.47)
Finished WHATandWHERE_Security (0:00:43 elapsed time, 0:02:23 cpu time, factor 3.32)
Running Program-Conflict-Analysis ...
Program-Conflict-Analysis: theory Misc
Program-Conflict-Analysis: theory Interleave
SumSquares: theory FourSquares
Program-Conflict-Analysis: theory LTS
Program-Conflict-Analysis: theory Flowgraph
Program-Conflict-Analysis: theory ConsInterleave
Program-Conflict-Analysis: theory ThreadTracking
Program-Conflict-Analysis: theory AcquisitionHistory
Timing SumSquares (4 threads, 39.391s elapsed time, 144.404s cpu time, 2.444s GC time, factor 3.67)
Finished SumSquares (0:00:41 elapsed time, 0:02:26 cpu time, factor 3.50)
Program-Conflict-Analysis: theory Semantics
DiskPaxos: theory DiskPaxos_Model
DiskPaxos: theory DiskPaxos_Inv1
DiskPaxos: theory DiskPaxos_Inv2
Program-Conflict-Analysis: theory Normalization
DiskPaxos: theory DiskPaxos_Inv3
DiskPaxos: theory DiskPaxos_Inv4
DiskPaxos: theory DiskPaxos_Inv5
Program-Conflict-Analysis: theory ConstraintSystems
DiskPaxos: theory DiskPaxos_Chosen
DiskPaxos: theory DiskPaxos_Inv6
DiskPaxos: theory DiskPaxos_Invariant
Program-Conflict-Analysis: theory MainResult
Timing Program-Conflict-Analysis (4 threads, 41.003s elapsed time, 108.600s cpu time, 4.116s GC time, factor 2.65)
Finished Program-Conflict-Analysis (0:00:47 elapsed time, 0:02:02 cpu time, factor 2.61)
Real_Impl: theory Derive_Manager
Real_Impl: theory Generator_Aux
Real_Impl: theory Show_Instances
Real_Impl: theory UniqueFactorization
Timing DiskPaxos (4 threads, 39.418s elapsed time, 135.268s cpu time, 1.136s GC time, factor 3.43)
Finished DiskPaxos (0:00:41 elapsed time, 0:02:17 cpu time, factor 3.29)
Real_Impl: theory Real_Impl_Auxiliary
Real_Impl: theory Prime_Product
Myhill-Nerode: theory Regular_Set
Real_Impl: theory Real_Unique_Impl
Myhill-Nerode: theory Regular_Exp
Myhill-Nerode: theory Derivatives
Myhill-Nerode: theory Infinite_Sequences
Myhill-Nerode: theory Least_Enum
Myhill-Nerode: theory NDerivative
Myhill-Nerode: theory Relation_Interpretation
Myhill-Nerode: theory Restricted_Predicates
Myhill-Nerode: theory Myhill_1
Myhill-Nerode: theory Minimal_Elements
Myhill-Nerode: theory Myhill_2
Myhill-Nerode: theory Closures
Timing Real_Impl (4 threads, 37.818s elapsed time, 133.464s cpu time, 2.376s GC time, factor 3.53)
Finished Real_Impl (0:00:41 elapsed time, 0:02:16 cpu time, factor 3.31)
Running Locally-Nameless-Sigma ...
Myhill-Nerode: theory Equivalence_Checking
Myhill-Nerode: theory Regexp_Method
Locally-Nameless-Sigma: theory Commutation
Myhill-Nerode: theory Almost_Full
Myhill-Nerode: theory Minimal_Bad_Sequences
Myhill-Nerode: theory Almost_Full_Relations
Myhill-Nerode: theory Well_Quasi_Orders
Myhill-Nerode: theory Closures2
Locally-Nameless-Sigma: theory Environments
Locally-Nameless-Sigma: theory ListPre
Locally-Nameless-Sigma: theory FMap
Locally-Nameless-Sigma: theory Sigma
Locally-Nameless-Sigma: theory ParRed
Locally-Nameless-Sigma: theory TypedSigma
Timing Myhill-Nerode (4 threads, 37.114s elapsed time, 100.820s cpu time, 2.904s GC time, factor 2.72)
Finished Myhill-Nerode (0:00:43 elapsed time, 0:01:51 cpu time, factor 2.60)
Running Possibilistic_Noninterference ...
Possibilistic_Noninterference: theory MyTactics
Possibilistic_Noninterference: theory Interface
Locally-Nameless-Sigma: theory Locally_Nameless_Sigma
Possibilistic_Noninterference: theory Bisim
Possibilistic_Noninterference: theory Language_Semantics
Possibilistic_Noninterference: theory During_Execution
Possibilistic_Noninterference: theory After_Execution
Possibilistic_Noninterference: theory Compositionality
Possibilistic_Noninterference: theory Syntactic_Criteria
Possibilistic_Noninterference: theory Concrete
Timing Locally-Nameless-Sigma (4 threads, 38.278s elapsed time, 128.848s cpu time, 2.320s GC time, factor 3.37)
Finished Locally-Nameless-Sigma (0:00:41 elapsed time, 0:02:11 cpu time, factor 3.19)
KAT_and_DRA: theory Test_Dioid
KAT_and_DRA: theory Conway_Tests
Timing Possibilistic_Noninterference (4 threads, 35.586s elapsed time, 112.808s cpu time, 3.212s GC time, factor 3.17)
Finished Possibilistic_Noninterference (0:00:38 elapsed time, 0:01:55 cpu time, factor 3.03)
Running Polynomial_Interpolation ...
Polynomial_Interpolation: theory Infinite_Set
Polynomial_Interpolation: theory Adhoc_Overloading
Polynomial_Interpolation: theory More_List
Polynomial_Interpolation: theory Sqrt_Babylonian_Auxiliary
Polynomial_Interpolation: theory Monad_Syntax
Polynomial_Interpolation: theory Polynomial
KAT_and_DRA: theory KAT_Models
KAT_and_DRA: theory DRA_Models
KAT_and_DRA: theory FolkTheorem
Polynomial_Interpolation: theory Divmod_Int
Polynomial_Interpolation: theory Euclidean_Algorithm
Polynomial_Interpolation: theory Improved_Code_Equations
Polynomial_Interpolation: theory Neville_Aitken_Interpolation
Polynomial_Interpolation: theory Missing_Unsorted
Polynomial_Interpolation: theory Is_Rat_To_Rat
Polynomial_Interpolation: theory Ring_Hom
Timing KAT_and_DRA (4 threads, 34.242s elapsed time, 111.540s cpu time, 2.592s GC time, factor 3.26)
Finished KAT_and_DRA (0:00:38 elapsed time, 0:02:00 cpu time, factor 3.16)
Running Residuated_Lattices ...
Polynomial_Interpolation: theory Missing_Polynomial
Polynomial_Interpolation: theory Lagrange_Interpolation
Polynomial_Interpolation: theory Ring_Hom_Poly
Polynomial_Interpolation: theory Newton_Interpolation
Residuated_Lattices: theory Residuated_Lattices
Polynomial_Interpolation: theory Polynomial_Interpolation
Timing Polynomial_Interpolation (4 threads, 35.282s elapsed time, 115.824s cpu time, 2.760s GC time, factor 3.28)
Finished Polynomial_Interpolation (0:00:37 elapsed time, 0:01:58 cpu time, factor 3.13)
Running Noninterference_Generic_Unwinding ...
Noninterference_Generic_Unwinding: theory GenericUnwinding
Residuated_Lattices: theory Action_Algebra
Residuated_Lattices: theory Involutive_Residuated
Residuated_Lattices: theory Residuated_Boolean_Algebras
Residuated_Lattices: theory Residuated_Relation_Algebra
Residuated_Lattices: theory Action_Algebra_Models
Timing Residuated_Lattices (4 threads, 32.793s elapsed time, 67.824s cpu time, 1.264s GC time, factor 2.07)
Finished Residuated_Lattices (0:00:38 elapsed time, 0:01:11 cpu time, factor 1.89)
Well_Quasi_Orders: theory Restricted_Predicates
Well_Quasi_Orders: theory Regular_Set
Well_Quasi_Orders: theory Open_Induction
Well_Quasi_Orders: theory Regular_Exp
Timing Noninterference_Generic_Unwinding (4 threads, 31.235s elapsed time, 41.428s cpu time, 0.340s GC time, factor 1.33)
Finished Noninterference_Generic_Unwinding (0:00:34 elapsed time, 0:00:43 cpu time, factor 1.28)
Nominal2: theory Quotient_Syntax
Nominal2: theory Quotient_Option
Nominal2: theory Quotient_Product
Nominal2: theory Quotient_List
Well_Quasi_Orders: theory NDerivative
Well_Quasi_Orders: theory Relation_Interpretation
Well_Quasi_Orders: theory Equivalence_Checking
Well_Quasi_Orders: theory Regexp_Method
Nominal2: theory Nominal2_Base
Well_Quasi_Orders: theory Infinite_Sequences
Well_Quasi_Orders: theory Multiset_Extension
Well_Quasi_Orders: theory Least_Enum
Well_Quasi_Orders: theory Minimal_Elements
Well_Quasi_Orders: theory Almost_Full
Well_Quasi_Orders: theory Higman_OI
Well_Quasi_Orders: theory Minimal_Bad_Sequences
Well_Quasi_Orders: theory Almost_Full_Relations
Well_Quasi_Orders: theory Well_Quasi_Orders
Well_Quasi_Orders: theory Kruskal
Well_Quasi_Orders: theory Wqo_Multiset
Well_Quasi_Orders: theory Kruskal_Examples
Well_Quasi_Orders: theory Wqo_Instances
Timing Well_Quasi_Orders (4 threads, 31.598s elapsed time, 96.136s cpu time, 3.008s GC time, factor 3.04)
Finished Well_Quasi_Orders (0:00:37 elapsed time, 0:01:46 cpu time, factor 2.84)
Running Decreasing-Diagrams-II ...
Decreasing-Diagrams-II: theory Order_Union
Decreasing-Diagrams-II: theory Least_Enum
Decreasing-Diagrams-II: theory Infinite_Sequences
Decreasing-Diagrams-II: theory Multiset
Decreasing-Diagrams-II: theory Ramsey
Decreasing-Diagrams-II: theory Restricted_Predicates
Decreasing-Diagrams-II: theory Sublist
Decreasing-Diagrams-II: theory Wellorder_Extension
Decreasing-Diagrams-II: theory Minimal_Elements
Decreasing-Diagrams-II: theory Almost_Full
Decreasing-Diagrams-II: theory Minimal_Bad_Sequences
Timing Nominal2 (4 threads, 31.770s elapsed time, 110.512s cpu time, 3.528s GC time, factor 3.48)
Finished Nominal2 (0:00:34 elapsed time, 0:01:52 cpu time, factor 3.30)
Running Presburger-Automata ...
Decreasing-Diagrams-II: theory Almost_Full_Relations
Decreasing-Diagrams-II: theory Well_Quasi_Orders
Decreasing-Diagrams-II: theory Multiset_Extension
Presburger-Automata: theory DFS
Presburger-Automata: theory Presburger_Automata
Decreasing-Diagrams-II: theory Decreasing_Diagrams_II_Aux
Decreasing-Diagrams-II: theory Decreasing_Diagrams_II
Timing Decreasing-Diagrams-II (4 threads, 31.422s elapsed time, 108.168s cpu time, 2.764s GC time, factor 3.44)
Finished Decreasing-Diagrams-II (0:00:34 elapsed time, 0:01:51 cpu time, factor 3.22)
UPF: theory ElementaryPolicies
UPF: theory ParallelComposition
Presburger-Automata: theory Exec
UPF: theory NormalisationTestSpecification
Timing Presburger-Automata (4 threads, 32.382s elapsed time, 108.244s cpu time, 2.576s GC time, factor 3.34)
Finished Presburger-Automata (0:00:38 elapsed time, 0:01:54 cpu time, factor 2.98)
Running Abstract_Completeness ...
Abstract_Completeness: theory ICF_Tools
Abstract_Completeness: theory Infinite_Set
Abstract_Completeness: theory Nat_Bijection
Abstract_Completeness: theory Code_Abstract_Nat
Abstract_Completeness: theory Code_Target_Nat
Abstract_Completeness: theory Old_Datatype
Abstract_Completeness: theory Ord_Code_Preproc
Abstract_Completeness: theory Sublist
Abstract_Completeness: theory Locale_Code
Abstract_Completeness: theory Stream
Abstract_Completeness: theory Countable
Abstract_Completeness: theory Countable_Set
Abstract_Completeness: theory Countable_Complete_Lattices
Abstract_Completeness: theory Order_Continuity
Abstract_Completeness: theory Extended_Nat
Abstract_Completeness: theory Linear_Temporal_Logic_on_Streams
Abstract_Completeness: theory FSet
Timing UPF (4 threads, 30.111s elapsed time, 90.660s cpu time, 2.512s GC time, factor 3.01)
Finished UPF (0:00:32 elapsed time, 0:01:33 cpu time, factor 2.85)
Running FocusStreamsCaseStudies ...
FocusStreamsCaseStudies: theory ArithExtras
FocusStreamsCaseStudies: theory ListExtras
FocusStreamsCaseStudies: theory arith_hints
Abstract_Completeness: theory Abstract_Completeness
FocusStreamsCaseStudies: theory stream
Abstract_Completeness: theory Propositional_Logic
FocusStreamsCaseStudies: theory BitBoolTS
FocusStreamsCaseStudies: theory FR_types
FocusStreamsCaseStudies: theory Gateway_types
FocusStreamsCaseStudies: theory JoinSplitTime
FocusStreamsCaseStudies: theory SteamBoiler
FocusStreamsCaseStudies: theory SteamBoiler_proof
FocusStreamsCaseStudies: theory FR
FocusStreamsCaseStudies: theory FR_proof
Timing Abstract_Completeness (4 threads, 30.591s elapsed time, 89.444s cpu time, 2.444s GC time, factor 2.92)
Finished Abstract_Completeness (0:00:33 elapsed time, 0:01:31 cpu time, factor 2.77)
Shivers-CFA: theory Adhoc_Overloading
Shivers-CFA: theory FixTransform
Shivers-CFA: theory HOLCFUtils
FocusStreamsCaseStudies: theory Gateway
FocusStreamsCaseStudies: theory Gateway_proof_aux
Shivers-CFA: theory Computability
FocusStreamsCaseStudies: theory Gateway_proof
Shivers-CFA: theory AbsCFCorrect
Timing FocusStreamsCaseStudies (4 threads, 29.468s elapsed time, 94.456s cpu time, 2.240s GC time, factor 3.21)
Finished FocusStreamsCaseStudies (0:00:32 elapsed time, 0:01:37 cpu time, factor 3.02)
Timing Shivers-CFA (4 threads, 28.716s elapsed time, 88.316s cpu time, 2.752s GC time, factor 3.08)
Finished Shivers-CFA (0:00:31 elapsed time, 0:01:31 cpu time, factor 2.88)
Timing Trie (4 threads, 27.813s elapsed time, 41.080s cpu time, 0.808s GC time, factor 1.48)
Finished Trie (0:00:30 elapsed time, 0:00:43 cpu time, factor 1.43)
ConcurrentIMP: theory Prefix_Order
ConcurrentIMP: theory CIMP_pred
ConcurrentIMP: theory CIMP_lang
Timing NormByEval (4 threads, 25.979s elapsed time, 73.664s cpu time, 1.640s GC time, factor 2.84)
Finished NormByEval (0:00:28 elapsed time, 0:01:16 cpu time, factor 2.68)
Running Recursion-Theory-I ...
Recursion-Theory-I: theory CPair
Recursion-Theory-I: theory PRecFun
Recursion-Theory-I: theory PRecFinSet
Recursion-Theory-I: theory PRecFun2
Recursion-Theory-I: theory PRecList
Recursion-Theory-I: theory PRecUnGr
Recursion-Theory-I: theory RecEnSet
ConcurrentIMP: theory CIMP_vcg
ConcurrentIMP: theory CIMP_one_place_buffer_ex
ConcurrentIMP: theory CIMP_unbounded_buffer_ex
Timing ConcurrentIMP (4 threads, 28.371s elapsed time, 57.704s cpu time, 2.700s GC time, factor 2.03)
Finished ConcurrentIMP (0:00:34 elapsed time, 0:01:03 cpu time, factor 1.85)
Timing Recursion-Theory-I (4 threads, 25.066s elapsed time, 93.028s cpu time, 1.784s GC time, factor 3.71)
Finished Recursion-Theory-I (0:00:27 elapsed time, 0:01:35 cpu time, factor 3.47)
XML: theory Partial_Function_MR
GraphMarkingIBP: theory Conj_Disj
GraphMarkingIBP: theory WellFoundedTransitive
GraphMarkingIBP: theory Complete_Lattice_Prop
GraphMarkingIBP: theory Preliminaries
GraphMarkingIBP: theory Statements
GraphMarkingIBP: theory Diagram
GraphMarkingIBP: theory DataRefinement
GraphMarkingIBP: theory SetMark
GraphMarkingIBP: theory StackMark
GraphMarkingIBP: theory LinkMark
GraphMarkingIBP: theory DSWMark
Timing XML (4 threads, 26.491s elapsed time, 48.892s cpu time, 2.368s GC time, factor 1.85)
Finished XML (0:00:28 elapsed time, 0:00:51 cpu time, factor 1.77)
Running Decreasing-Diagrams ...
Timing GraphMarkingIBP (4 threads, 25.224s elapsed time, 70.952s cpu time, 0.752s GC time, factor 2.81)
Finished GraphMarkingIBP (0:00:27 elapsed time, 0:01:13 cpu time, factor 2.65)
Running Special_Function_Bounds ...
Decreasing-Diagrams: theory Multiset
Special_Function_Bounds: theory Bounds_Lemmas
Special_Function_Bounds: theory Log_CF_Bounds
Special_Function_Bounds: theory Sin_Cos_Bounds
Special_Function_Bounds: theory Atan_CF_Bounds
Special_Function_Bounds: theory Exp_Bounds
Special_Function_Bounds: theory Sqrt_Bounds
Decreasing-Diagrams: theory Decreasing_Diagrams
Timing Decreasing-Diagrams (4 threads, 26.316s elapsed time, 90.912s cpu time, 1.848s GC time, factor 3.45)
Finished Decreasing-Diagrams (0:00:29 elapsed time, 0:01:33 cpu time, factor 3.21)
Running Boolean_Expression_Checkers ...
Timing Special_Function_Bounds (4 threads, 26.716s elapsed time, 85.048s cpu time, 0.920s GC time, factor 3.18)
Finished Special_Function_Bounds (0:00:32 elapsed time, 0:01:30 cpu time, factor 2.75)
Boolean_Expression_Checkers: theory Boolean_Expression_Checkers
Sturm_Tarski: theory Infinite_Set
Sturm_Tarski: theory More_List
Sturm_Tarski: theory Polynomial
Sturm_Tarski: theory Polynomial_GCD_euclidean
Boolean_Expression_Checkers: theory Boolean_Expression_Checkers_AList_Mapping
Boolean_Expression_Checkers: theory Boolean_Expression_Example
Sturm_Tarski: theory Sturm_Tarski
Timing Sturm_Tarski (4 threads, 23.454s elapsed time, 76.868s cpu time, 1.156s GC time, factor 3.28)
Finished Sturm_Tarski (0:00:25 elapsed time, 0:01:19 cpu time, factor 3.06)
Timing Boolean_Expression_Checkers (4 threads, 25.214s elapsed time, 44.768s cpu time, 1.632s GC time, factor 1.78)
Finished Boolean_Expression_Checkers (0:00:30 elapsed time, 0:00:50 cpu time, factor 1.63)
Jordan_Hoelder: theory GroupAction
Jordan_Hoelder: theory SubgroupConjugation
Jordan_Hoelder: theory SndSylow
Jordan_Hoelder: theory GroupIsoClasses
Jordan_Hoelder: theory SndIsomorphismGrp
Jordan_Hoelder: theory SubgroupsAndNormalSubgroups
Jordan_Hoelder: theory SimpleGroups
Jordan_Hoelder: theory MaximalNormalSubgroups
Jordan_Hoelder: theory CompositionSeries
Jordan_Hoelder: theory JordanHolder
Timing Jordan_Hoelder (4 threads, 25.143s elapsed time, 86.940s cpu time, 1.644s GC time, factor 3.46)
Finished Jordan_Hoelder (0:00:28 elapsed time, 0:01:30 cpu time, factor 3.16)
Timing Fermat3_4 (4 threads, 25.580s elapsed time, 93.588s cpu time, 1.092s GC time, factor 3.66)
Finished Fermat3_4 (0:00:28 elapsed time, 0:01:36 cpu time, factor 3.33)
POPLmark-deBruijn: theory Basis
POPLmark-deBruijn: theory POPLmark
POPLmark-deBruijn: theory POPLmarkRecord
Category2: theory MonadicEquationalTheory
POPLmark-deBruijn: theory POPLmarkRecordCtxt
POPLmark-deBruijn: theory Execute
Timing Category2 (4 threads, 23.707s elapsed time, 82.168s cpu time, 3.040s GC time, factor 3.47)
Finished Category2 (0:00:29 elapsed time, 0:01:27 cpu time, factor 2.98)
Timing POPLmark-deBruijn (4 threads, 24.346s elapsed time, 74.608s cpu time, 2.784s GC time, factor 3.06)
Finished POPLmark-deBruijn (0:00:30 elapsed time, 0:01:20 cpu time, factor 2.67)
WorkerWrapper: theory FixedPointTheorems
WorkerWrapper: theory WorkerWrapper
WorkerWrapper: theory CounterExample
WorkerWrapper: theory WorkerWrapperNew
WorkerWrapper: theory Accumulator
WorkerWrapper: theory Backtracking
CCS: theory Weak_Cong_Semantics
WorkerWrapper: theory Continuations
WorkerWrapper: theory UnboxedNats
CCS: theory Weak_Cong_Sim_Pres
Timing CCS (4 threads, 22.254s elapsed time, 62.928s cpu time, 1.036s GC time, factor 2.83)
Finished CCS (0:00:24 elapsed time, 0:01:05 cpu time, factor 2.63)
Timing WorkerWrapper (4 threads, 23.037s elapsed time, 54.164s cpu time, 1.204s GC time, factor 2.35)
Finished WorkerWrapper (0:00:26 elapsed time, 0:00:57 cpu time, factor 2.19)
CISC-Kernel: theory List_Theorems
CISC-Kernel: theory Option_Binders
CISC-Kernel: theory Step_configuration
CISC-Kernel: theory Step_policies
Parity_Game: theory MoreCoinductiveList
Parity_Game: theory ParityGame
CISC-Kernel: theory Step_invariants
CISC-Kernel: theory Step_vpeq_locally_respects
CISC-Kernel: theory Step_vpeq_weakly_step_consistent
CISC-Kernel: theory Separation_kernel_model
CISC-Kernel: theory Link_separation_kernel_model_to_CISK
Parity_Game: theory AttractingStrategy
Parity_Game: theory WellOrderedStrategy
Parity_Game: theory WinningStrategy
Parity_Game: theory WinningRegion
Parity_Game: theory UniformStrategy
Parity_Game: theory AttractorInductive
Parity_Game: theory AttractorStrategy
Parity_Game: theory PositionalDeterminacy
Timing CISC-Kernel (4 threads, 22.338s elapsed time, 75.324s cpu time, 2.520s GC time, factor 3.37)
Finished CISC-Kernel (0:00:24 elapsed time, 0:01:17 cpu time, factor 3.12)
Strong_Security: theory Strong_Security
Strong_Security: theory Up_To_Technique
Strong_Security: theory Parallel_Composition
Strong_Security: theory Domain_example
Strong_Security: theory Strongly_Secure_Skip_Assign
Timing Parity_Game (4 threads, 22.916s elapsed time, 74.832s cpu time, 1.368s GC time, factor 3.27)
Finished Parity_Game (0:00:30 elapsed time, 0:01:21 cpu time, factor 2.64)
Strong_Security: theory Language_Composition
Strong_Security: theory Type_System
Strong_Security: theory Type_System_example
Finger-Trees: theory FingerTree
Timing Strong_Security (4 threads, 21.610s elapsed time, 65.876s cpu time, 1.704s GC time, factor 3.05)
Finished Strong_Security (0:00:24 elapsed time, 0:01:08 cpu time, factor 2.83)
Binomial-Heaps: theory BinomialHeap
Binomial-Heaps: theory SkewBinomialHeap
Timing Finger-Trees (4 threads, 21.146s elapsed time, 43.208s cpu time, 2.168s GC time, factor 2.04)
Finished Finger-Trees (0:00:27 elapsed time, 0:00:49 cpu time, factor 1.81)
FunWithTilings: theory Tilings
Timing Binomial-Heaps (4 threads, 20.943s elapsed time, 62.628s cpu time, 3.360s GC time, factor 2.99)
Finished Binomial-Heaps (0:00:26 elapsed time, 0:01:08 cpu time, factor 2.55)
Running Separation_Algebra ...
Separation_Algebra: theory Hoare_Logic_Abort
Separation_Algebra: theory Map_Extra
Separation_Algebra: theory Separation_Algebra
Separation_Algebra: theory Separation_Algebra_Alt
Separation_Algebra: theory Types_D
Separation_Algebra: theory Sep_Heap_Instance
Separation_Algebra: theory Sep_Tactics
Separation_Algebra: theory Sep_Eq
Separation_Algebra: theory Sep_Tactics_Test
Separation_Algebra: theory Simple_Separation_Example
Separation_Algebra: theory VM_Example
Timing FunWithTilings (4 threads, 21.791s elapsed time, 66.260s cpu time, 0.128s GC time, factor 3.04)
Finished FunWithTilings (0:00:24 elapsed time, 0:01:08 cpu time, factor 2.82)
FOL-Fitting: theory FOL_Fitting
Separation_Algebra: theory Abstract_Separation_D
Separation_Algebra: theory Separation_D
Timing Separation_Algebra (4 threads, 19.741s elapsed time, 51.168s cpu time, 1.964s GC time, factor 2.59)
Finished Separation_Algebra (0:00:22 elapsed time, 0:00:54 cpu time, factor 2.38)
Ribbon_Proofs: theory Finite_Map
Ribbon_Proofs: theory Ribbons_Basic
Ribbon_Proofs: theory Proofchain
Ribbon_Proofs: theory Ribbons_Interfaces
Timing FOL-Fitting (4 threads, 20.680s elapsed time, 39.272s cpu time, 2.064s GC time, factor 1.90)
Finished FOL-Fitting (0:00:26 elapsed time, 0:00:44 cpu time, factor 1.70)
Running Transitive-Closure-II ...
Ribbon_Proofs: theory Ribbons_Graphical
Ribbon_Proofs: theory Ribbons_Stratified
Transitive-Closure-II: theory Regular_Set
Transitive-Closure-II: theory While_Combinator
Transitive-Closure-II: theory Regular_Exp
Ribbon_Proofs: theory Ribbons_Graphical_Soundness
Transitive-Closure-II: theory NDerivative
Transitive-Closure-II: theory Relation_Interpretation
Transitive-Closure-II: theory Equivalence_Checking
Timing Ribbon_Proofs (4 threads, 22.287s elapsed time, 45.000s cpu time, 1.852s GC time, factor 2.02)
Finished Ribbon_Proofs (0:00:28 elapsed time, 0:00:50 cpu time, factor 1.81)
Transitive-Closure-II: theory Regexp_Method
Transitive-Closure-II: theory RTrancl
Timing Transitive-Closure-II (4 threads, 19.976s elapsed time, 44.960s cpu time, 1.324s GC time, factor 2.25)
Finished Transitive-Closure-II (0:00:22 elapsed time, 0:00:52 cpu time, factor 2.33)
Polynomials: theory Polynomials
Dynamic_Tables: theory Tables_real
Dynamic_Tables: theory Tables_nat
Timing Dynamic_Tables (4 threads, 20.242s elapsed time, 61.104s cpu time, 1.080s GC time, factor 3.02)
Finished Dynamic_Tables (0:00:22 elapsed time, 0:01:03 cpu time, factor 2.79)
Timing Polynomials (4 threads, 19.652s elapsed time, 47.892s cpu time, 1.320s GC time, factor 2.44)
Finished Polynomials (0:00:22 elapsed time, 0:00:50 cpu time, factor 2.24)
Timing SenSocialChoice (4 threads, 20.002s elapsed time, 67.288s cpu time, 0.692s GC time, factor 3.36)
Finished SenSocialChoice (0:00:22 elapsed time, 0:01:09 cpu time, factor 3.10)
Integration: theory Nat_Bijection
Integration: theory Old_Datatype
Integration: theory Sigma_Algebra
Timing TLA (4 threads, 20.512s elapsed time, 69.756s cpu time, 1.388s GC time, factor 3.40)
Finished TLA (0:00:23 elapsed time, 0:01:12 cpu time, factor 3.13)
Running Stream_Fusion_Code ...
Integration: theory RealRandVar
Stream_Fusion_Code: theory Stream_Fusion
Stream_Fusion_Code: theory Stream_Fusion_List
Timing Integration (4 threads, 19.556s elapsed time, 71.628s cpu time, 1.292s GC time, factor 3.66)
Finished Integration (0:00:22 elapsed time, 0:01:14 cpu time, factor 3.35)
Running Rank_Nullity_Theorem ...
Rank_Nullity_Theorem: theory Bit
Stream_Fusion_Code: theory Stream_Fusion_LList
Rank_Nullity_Theorem: theory Dual_Order
Rank_Nullity_Theorem: theory Generalizations
Rank_Nullity_Theorem: theory Mod_Type
Stream_Fusion_Code: theory Stream_Fusion_Examples
Rank_Nullity_Theorem: theory Miscellaneous
Timing Stream_Fusion_Code (4 threads, 20.059s elapsed time, 57.284s cpu time, 1.484s GC time, factor 2.86)
Finished Stream_Fusion_Code (0:00:27 elapsed time, 0:01:04 cpu time, factor 2.37)
Running Functional-Automata ...
Rank_Nullity_Theorem: theory Fundamental_Subspaces
Rank_Nullity_Theorem: theory Dim_Formula
Functional-Automata: theory Regular_Set
Functional-Automata: theory Regular_Exp
Timing Rank_Nullity_Theorem (4 threads, 19.208s elapsed time, 68.052s cpu time, 1.380s GC time, factor 3.54)
Finished Rank_Nullity_Theorem (0:00:23 elapsed time, 0:01:12 cpu time, factor 3.09)
Running Finite_Automata_HF ...
Finite_Automata_HF: theory Nat_Bijection
Finite_Automata_HF: theory Regular_Set
Functional-Automata: theory AutoProj
Functional-Automata: theory MaxPrefix
Functional-Automata: theory DA
Functional-Automata: theory NA
Functional-Automata: theory MaxChop
Functional-Automata: theory RegSet_of_nat_DA
Functional-Automata: theory NAe
Functional-Automata: theory RegExp2NA
Functional-Automata: theory Automata
Functional-Automata: theory RegExp2NAe
Functional-Automata: theory AutoMaxChop
Finite_Automata_HF: theory Regular_Exp
Finite_Automata_HF: theory Ordinal
Functional-Automata: theory AutoRegExp
Functional-Automata: theory Execute
Functional-Automata: theory Functional_Automata
Finite_Automata_HF: theory Finite_Automata_HF
Timing Functional-Automata (4 threads, 20.852s elapsed time, 40.688s cpu time, 1.020s GC time, factor 1.95)
Finished Functional-Automata (0:00:26 elapsed time, 0:00:51 cpu time, factor 1.91)
HyperCTL: theory Nat_Bijection
Timing Finite_Automata_HF (4 threads, 17.972s elapsed time, 55.196s cpu time, 1.460s GC time, factor 3.07)
Finished Finite_Automata_HF (0:00:20 elapsed time, 0:01:02 cpu time, factor 3.07)
Running IEEE_Floating_Point ...
HyperCTL: theory Noninterference
IEEE_Floating_Point: theory IEEE
IEEE_Floating_Point: theory Code_Float
IEEE_Floating_Point: theory FloatProperty
HyperCTL: theory Finite_Noninterference
IEEE_Floating_Point: theory RoundError
Timing HyperCTL (4 threads, 18.049s elapsed time, 57.600s cpu time, 1.936s GC time, factor 3.19)
Finished HyperCTL (0:00:20 elapsed time, 0:01:00 cpu time, factor 2.91)
Running Noninterference_Inductive_Unwinding ...
Noninterference_Inductive_Unwinding: theory CSPNoninterference
Noninterference_Inductive_Unwinding: theory ListInterleaving
Noninterference_Inductive_Unwinding: theory IpurgeUnwinding
Timing IEEE_Floating_Point (4 threads, 18.602s elapsed time, 55.784s cpu time, 0.652s GC time, factor 3.00)
Finished IEEE_Floating_Point (0:00:21 elapsed time, 0:00:58 cpu time, factor 2.75)
Noninterference_Inductive_Unwinding: theory DeterministicProcesses
PropResPI: theory Propositional_Resolution
PropResPI: theory Prime_Implicates
Noninterference_Inductive_Unwinding: theory InductiveUnwinding
Timing Noninterference_Inductive_Unwinding (4 threads, 17.883s elapsed time, 55.604s cpu time, 1.264s GC time, factor 3.11)
Finished Noninterference_Inductive_Unwinding (0:00:20 elapsed time, 0:00:58 cpu time, factor 2.84)
Timing PropResPI (4 threads, 18.369s elapsed time, 54.140s cpu time, 1.188s GC time, factor 2.95)
Finished PropResPI (0:00:20 elapsed time, 0:00:56 cpu time, factor 2.71)
FeatherweightJava: theory FJDefs
Completeness: theory Permutation
Completeness: theory PermutationLemmas
FeatherweightJava: theory FJAux
FeatherweightJava: theory FJSound
FeatherweightJava: theory Execute
Completeness: theory Completeness
Completeness: theory Soundness
Timing Completeness (4 threads, 17.749s elapsed time, 51.392s cpu time, 1.404s GC time, factor 2.90)
Finished Completeness (0:00:20 elapsed time, 0:00:53 cpu time, factor 2.65)
FeatherweightJava: theory Featherweight_Java
Timing FeatherweightJava (4 threads, 16.963s elapsed time, 48.068s cpu time, 1.216s GC time, factor 2.83)
Finished FeatherweightJava (0:00:19 elapsed time, 0:00:50 cpu time, factor 2.59)
Running JiveDataStoreModel ...
JiveDataStoreModel: theory TypeIds
JiveDataStoreModel: theory JavaType
JiveDataStoreModel: theory DirectSubtypes
JiveDataStoreModel: theory Subtype
JiveDataStoreModel: theory Attributes
JiveDataStoreModel: theory Value
JiveDataStoreModel: theory AttributesIndep
JiveDataStoreModel: theory Location
Timing AVL-Trees (4 threads, 17.056s elapsed time, 60.320s cpu time, 0.776s GC time, factor 3.54)
Finished AVL-Trees (0:00:19 elapsed time, 0:01:02 cpu time, factor 3.19)
Running Regex_Equivalence_Examples ...
JiveDataStoreModel: theory Store
JiveDataStoreModel: theory StoreProperties
JiveDataStoreModel: theory JML
JiveDataStoreModel: theory UnivSpec
Timing JiveDataStoreModel (4 threads, 16.784s elapsed time, 44.048s cpu time, 1.096s GC time, factor 2.62)
Finished JiveDataStoreModel (0:00:19 elapsed time, 0:00:46 cpu time, factor 2.39)
Running CryptoBasedCompositionalProperties ...
CryptoBasedCompositionalProperties: theory ListExtras
CryptoBasedCompositionalProperties: theory Secrecy_types
Regex_Equivalence_Examples: theory Examples
Regex_Equivalence_Examples: theory Spec_Check
Regex_Equivalence_Examples: theory Benchmark
CryptoBasedCompositionalProperties: theory inout
CryptoBasedCompositionalProperties: theory Secrecy
CryptoBasedCompositionalProperties: theory CompLocalSecrets
CryptoBasedCompositionalProperties: theory KnowledgeKeysSecrets
Timing CryptoBasedCompositionalProperties (4 threads, 15.879s elapsed time, 38.808s cpu time, 0.772s GC time, factor 2.44)
Finished CryptoBasedCompositionalProperties (0:00:18 elapsed time, 0:00:41 cpu time, factor 2.25)
Running Inductive_Confidentiality ...
Inductive_Confidentiality: theory Message
Inductive_Confidentiality: theory MessageGA
Timing Regex_Equivalence_Examples (4 threads, 17.255s elapsed time, 46.684s cpu time, 6.060s GC time, factor 2.71)
Finished Regex_Equivalence_Examples (0:00:27 elapsed time, 0:00:53 cpu time, factor 1.92)
Running Priority_Queue_Braun ...
Priority_Queue_Braun: theory Multiset
Priority_Queue_Braun: theory Tree
Inductive_Confidentiality: theory Event
Inductive_Confidentiality: theory EventGA
Inductive_Confidentiality: theory PublicGA
Inductive_Confidentiality: theory Public
Inductive_Confidentiality: theory NS_Public_Bad_GA
Inductive_Confidentiality: theory NS_Public_Bad
Inductive_Confidentiality: theory ConfidentialityGA
Inductive_Confidentiality: theory Knowledge
Inductive_Confidentiality: theory ConfidentialityDY
Priority_Queue_Braun: theory Tree_Multiset
Priority_Queue_Braun: theory Priority_Queue_Braun
Timing Inductive_Confidentiality (4 threads, 16.253s elapsed time, 44.140s cpu time, 1.528s GC time, factor 2.72)
Finished Inductive_Confidentiality (0:00:18 elapsed time, 0:00:46 cpu time, factor 2.48)
Running Efficient-Mergesort ...
Timing Priority_Queue_Braun (4 threads, 16.154s elapsed time, 50.404s cpu time, 1.416s GC time, factor 3.12)
Finished Priority_Queue_Braun (0:00:18 elapsed time, 0:00:52 cpu time, factor 2.83)
Efficient-Mergesort: theory Efficient_Sort
Landau_Symbols: theory Group_Sort
Landau_Symbols: theory Landau_Library
Landau_Symbols: theory Landau_Symbols_Definition
Landau_Symbols: theory Landau_Real_Products
Landau_Symbols: theory Landau_Simprocs
Landau_Symbols: theory Landau_Symbols
Timing Efficient-Mergesort (4 threads, 15.540s elapsed time, 29.532s cpu time, 0.656s GC time, factor 1.90)
Finished Efficient-Mergesort (0:00:21 elapsed time, 0:00:35 cpu time, factor 1.64)
Timing Landau_Symbols (4 threads, 15.070s elapsed time, 53.432s cpu time, 1.304s GC time, factor 3.55)
Finished Landau_Symbols (0:00:20 elapsed time, 0:00:59 cpu time, factor 2.83)
Running Selection_Heap_Sort ...
Cayley_Hamilton: theory More_List
Cayley_Hamilton: theory Polynomial
Selection_Heap_Sort: theory Sort
Selection_Heap_Sort: theory RemoveMax
Selection_Heap_Sort: theory Heap
Selection_Heap_Sort: theory SelectionSort_Functional
Selection_Heap_Sort: theory HeapFunctional
Selection_Heap_Sort: theory HeapImperative
Cayley_Hamilton: theory Square_Matrix
Cayley_Hamilton: theory Cayley_Hamilton
Timing Cayley_Hamilton (4 threads, 14.237s elapsed time, 48.000s cpu time, 0.812s GC time, factor 3.37)
Finished Cayley_Hamilton (0:00:18 elapsed time, 0:00:52 cpu time, factor 2.83)
Timing Selection_Heap_Sort (4 threads, 16.127s elapsed time, 46.756s cpu time, 1.016s GC time, factor 2.90)
Finished Selection_Heap_Sort (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.40)
Running Lam-ml-Normalization ...
Lam-ml-Normalization: theory LaTeXsugar
Old_Datatype_Show: theory Old_Show
Lam-ml-Normalization: theory Lam_ml
Old_Datatype_Show: theory Old_Show_Generator
Old_Datatype_Show: theory Old_Show_Instances
Old_Datatype_Show: theory Old_Show_Examples
Timing Lam-ml-Normalization (4 threads, 14.237s elapsed time, 32.828s cpu time, 0.944s GC time, factor 2.31)
Finished Lam-ml-Normalization (0:00:16 elapsed time, 0:00:35 cpu time, factor 2.09)
Running RefinementReactive ...
Timing Old_Datatype_Show (4 threads, 14.896s elapsed time, 18.832s cpu time, 0.236s GC time, factor 1.26)
Finished Old_Datatype_Show (0:00:24 elapsed time, 0:00:26 cpu time, factor 1.09)
Running InformationFlowSlicing_Intra ...
RefinementReactive: theory Refinement
RefinementReactive: theory Temporal
RefinementReactive: theory Reactive
InformationFlowSlicing_Intra: theory NonInterferenceIntra
InformationFlowSlicing_Intra: theory LiftingIntra
InformationFlowSlicing_Intra: theory NonInterferenceWhile
Timing RefinementReactive (4 threads, 12.597s elapsed time, 35.324s cpu time, 0.436s GC time, factor 2.80)
Finished RefinementReactive (0:00:15 elapsed time, 0:00:37 cpu time, factor 2.49)
Timing InformationFlowSlicing_Intra (4 threads, 13.627s elapsed time, 45.116s cpu time, 1.080s GC time, factor 3.31)
Finished InformationFlowSlicing_Intra (0:00:21 elapsed time, 0:00:49 cpu time, factor 2.32)
Stream-Fusion: theory Int_Discrete
Stream-Fusion: theory LazyList
Stream-Fusion: theory StreamFusion
Timing MiniML (4 threads, 12.973s elapsed time, 27.636s cpu time, 0.660s GC time, factor 2.13)
Finished MiniML (0:00:15 elapsed time, 0:00:30 cpu time, factor 1.94)
Running Lower_Semicontinuous ...
Lower_Semicontinuous: theory Lower_Semicontinuous
Timing Stream-Fusion (4 threads, 12.414s elapsed time, 20.260s cpu time, 0.232s GC time, factor 1.63)
Finished Stream-Fusion (0:00:15 elapsed time, 0:00:23 cpu time, factor 1.51)
Liouville_Numbers: theory Infinite_Set
Liouville_Numbers: theory More_List
Liouville_Numbers: theory Polynomial
Timing Lower_Semicontinuous (4 threads, 12.769s elapsed time, 50.576s cpu time, 0.448s GC time, factor 3.96)
Finished Lower_Semicontinuous (0:00:16 elapsed time, 0:00:54 cpu time, factor 3.22)
Running Impossible_Geometry ...
Liouville_Numbers: theory Liouville_Numbers_Misc
Liouville_Numbers: theory Liouville_Numbers
Impossible_Geometry: theory Impossible_Geometry
Timing Liouville_Numbers (4 threads, 12.056s elapsed time, 40.492s cpu time, 0.760s GC time, factor 3.36)
Finished Liouville_Numbers (0:00:14 elapsed time, 0:00:42 cpu time, factor 2.94)
VolpanoSmith: theory Semantics
Timing Impossible_Geometry (4 threads, 13.027s elapsed time, 32.980s cpu time, 0.692s GC time, factor 2.53)
Finished Impossible_Geometry (0:00:15 elapsed time, 0:00:35 cpu time, factor 2.28)
Timing VolpanoSmith (4 threads, 13.188s elapsed time, 32.964s cpu time, 0.756s GC time, factor 2.50)
Finished VolpanoSmith (0:00:15 elapsed time, 0:00:35 cpu time, factor 2.25)
Running Abstract-Hoare-Logics ...
Abstract-Hoare-Logics: theory Lang
Abstract-Hoare-Logics: theory PLang
Abstract-Hoare-Logics: theory PsLang
Abstract-Hoare-Logics: theory Hoare
Abstract-Hoare-Logics: theory Termi
Abstract-Hoare-Logics: theory HoareTotal
Abstract-Hoare-Logics: theory PsHoare
Abstract-Hoare-Logics: theory PsTermi
Abstract-Hoare-Logics: theory PHoare
Abstract-Hoare-Logics: theory PTermi
Abstract-Hoare-Logics: theory PsHoareTotal
Abstract-Hoare-Logics: theory PHoareTotal
Timing Huffman (4 threads, 13.026s elapsed time, 39.492s cpu time, 0.512s GC time, factor 3.03)
Finished Huffman (0:00:15 elapsed time, 0:00:41 cpu time, factor 2.69)
Timing Abstract-Hoare-Logics (4 threads, 12.126s elapsed time, 37.788s cpu time, 1.756s GC time, factor 3.12)
Finished Abstract-Hoare-Logics (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.75)
Running Coinductive_Languages ...
Coinductive_Languages: theory Regular_Set
Coinductive_Languages: theory Coinductive_Language
Coinductive_Languages: theory CFG_Examples
Skew_Heap: theory Tree_Multiset
Coinductive_Languages: theory Coinductive_Regular_Set
Timing Skew_Heap (4 threads, 12.546s elapsed time, 40.708s cpu time, 1.084s GC time, factor 3.24)
Finished Skew_Heap (0:00:15 elapsed time, 0:00:43 cpu time, factor 2.84)
Pop_Refinement: theory Definition
Pop_Refinement: theory First_Example
Pop_Refinement: theory Future_Work
Pop_Refinement: theory General_Remarks
Pop_Refinement: theory Related_Work
Pop_Refinement: theory Second_Example
Timing Coinductive_Languages (4 threads, 11.618s elapsed time, 31.264s cpu time, 0.484s GC time, factor 2.69)
Finished Coinductive_Languages (0:00:14 elapsed time, 0:00:38 cpu time, factor 2.71)
GPU_Kernel_PL: theory KPL_syntax
GPU_Kernel_PL: theory KPL_state
GPU_Kernel_PL: theory KPL_wellformedness
GPU_Kernel_PL: theory KPL_execution_thread
GPU_Kernel_PL: theory KPL_execution_group
GPU_Kernel_PL: theory KPL_execution_kernel
Timing Pop_Refinement (4 threads, 10.600s elapsed time, 31.500s cpu time, 0.760s GC time, factor 2.97)
Finished Pop_Refinement (0:00:13 elapsed time, 0:00:33 cpu time, factor 2.59)
Running HereditarilyFinite ...
HereditarilyFinite: theory Nat_Bijection
GPU_Kernel_PL: theory Kernel_programming_language
Timing GPU_Kernel_PL (4 threads, 11.011s elapsed time, 19.120s cpu time, 0.456s GC time, factor 1.74)
Finished GPU_Kernel_PL (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.60)
HereditarilyFinite: theory Ordinal
HereditarilyFinite: theory Finitary
HereditarilyFinite: theory Finite_Automata
HereditarilyFinite: theory Rank
Timing HereditarilyFinite (4 threads, 10.900s elapsed time, 35.448s cpu time, 0.556s GC time, factor 3.25)
Finished HereditarilyFinite (0:00:13 elapsed time, 0:00:37 cpu time, factor 2.83)
Running MonoBoolTranAlgebra ...
MonoBoolTranAlgebra: theory Mono_Bool_Tran
Timing GoedelGod (4 threads, 11.085s elapsed time, 13.060s cpu time, 0.076s GC time, factor 1.18)
Finished GoedelGod (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.30)
MonoBoolTranAlgebra: theory Mono_Bool_Tran_Algebra
HotelKeyCards: theory LaTeXsugar
HotelKeyCards: theory Notation
HotelKeyCards: theory Equivalence
MonoBoolTranAlgebra: theory Assertion_Algebra
MonoBoolTranAlgebra: theory Statements
Timing MonoBoolTranAlgebra (4 threads, 10.906s elapsed time, 22.220s cpu time, 0.288s GC time, factor 2.04)
Finished MonoBoolTranAlgebra (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.85)
Running Robbins-Conjecture ...
Robbins-Conjecture: theory Robbins_Conjecture
Timing HotelKeyCards (4 threads, 10.301s elapsed time, 27.060s cpu time, 0.396s GC time, factor 2.63)
Finished HotelKeyCards (0:00:12 elapsed time, 0:00:29 cpu time, factor 2.30)
FileRefinement: theory CArrays
FileRefinement: theory ResizableArrays
FileRefinement: theory FileRefinement
Timing Robbins-Conjecture (4 threads, 10.545s elapsed time, 33.680s cpu time, 0.352s GC time, factor 3.19)
Finished Robbins-Conjecture (0:00:13 elapsed time, 0:00:36 cpu time, factor 2.75)
Verified-Prover: theory Prover
Timing FileRefinement (4 threads, 10.408s elapsed time, 25.972s cpu time, 0.096s GC time, factor 2.50)
Finished FileRefinement (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.19)
Timing Verified-Prover (4 threads, 9.292s elapsed time, 18.840s cpu time, 0.292s GC time, factor 2.03)
Finished Verified-Prover (0:00:11 elapsed time, 0:00:21 cpu time, factor 1.80)
Stern_Brocot: theory Cotree_Algebra
Stern_Brocot: theory Stern_Brocot_Tree
Stern_Brocot: theory Bird_Tree
Tycon: theory Binary_Tree_Monad
Tycon: theory Resumption_Transformer
Timing Stern_Brocot (4 threads, 9.383s elapsed time, 22.040s cpu time, 0.312s GC time, factor 2.35)
Finished Stern_Brocot (0:00:16 elapsed time, 0:00:28 cpu time, factor 1.73)
Running Partial_Function_MR ...
Tycon: theory Error_Transformer
Tycon: theory State_Transformer
Tycon: theory Writer_Transformer
Partial_Function_MR: theory Adhoc_Overloading
Partial_Function_MR: theory Monad_Syntax
Partial_Function_MR: theory Partial_Function_MR
Partial_Function_MR: theory Partial_Function_MR_Examples
Timing Tycon (4 threads, 9.380s elapsed time, 28.880s cpu time, 0.256s GC time, factor 3.08)
Finished Tycon (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.56)
Timing Partial_Function_MR (4 threads, 9.258s elapsed time, 13.944s cpu time, 0.312s GC time, factor 1.51)
Finished Partial_Function_MR (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.40)
Running Imperative_Insertion_Sort ...
Topology: theory LList_Topology
Timing Topology (4 threads, 7.844s elapsed time, 29.560s cpu time, 0.444s GC time, factor 3.77)
Finished Topology (0:00:15 elapsed time, 0:00:36 cpu time, factor 2.42)
Imperative_Insertion_Sort: theory Imperative_Loops
Imperative_Insertion_Sort: theory Imperative_Insertion_Sort
Binomial-Queues: theory Binomial_Queue
Binomial-Queues: theory PQ_Implementation
Timing Imperative_Insertion_Sort (4 threads, 8.507s elapsed time, 24.560s cpu time, 0.144s GC time, factor 2.89)
Finished Imperative_Insertion_Sort (0:00:17 elapsed time, 0:00:28 cpu time, factor 1.63)
Running Perfect-Number-Thm ...
Perfect-Number-Thm: theory Primes
Perfect-Number-Thm: theory Infinite_Set
Timing Binomial-Queues (4 threads, 8.343s elapsed time, 21.460s cpu time, 0.416s GC time, factor 2.57)
Finished Binomial-Queues (0:00:10 elapsed time, 0:00:23 cpu time, factor 2.22)
Perfect-Number-Thm: theory Exponent
Perfect-Number-Thm: theory PerfectBasics
Perfect-Number-Thm: theory Sigma
Perfect-Number-Thm: theory Perfect
TortoiseHare: theory While_Combinator
TortoiseHare: theory TortoiseHare
Timing Perfect-Number-Thm (4 threads, 7.803s elapsed time, 27.280s cpu time, 0.220s GC time, factor 3.50)
Finished Perfect-Number-Thm (0:00:10 elapsed time, 0:00:29 cpu time, factor 2.86)
Timing TortoiseHare (4 threads, 8.187s elapsed time, 23.384s cpu time, 0.144s GC time, factor 2.86)
Finished TortoiseHare (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.43)
Card_Partitions: theory Card_Partitions
MuchAdoAboutTwo: theory MuchAdoAboutTwo
Timing Card_Partitions (4 threads, 7.653s elapsed time, 25.280s cpu time, 0.172s GC time, factor 3.30)
Finished Card_Partitions (0:00:10 elapsed time, 0:00:27 cpu time, factor 2.65)
Timing MuchAdoAboutTwo (4 threads, 7.853s elapsed time, 22.316s cpu time, 0.420s GC time, factor 2.84)
Finished MuchAdoAboutTwo (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.08)
Running Transitive-Closure ...
Secondary_Sylow: theory GroupAction
Secondary_Sylow: theory SubgroupConjugation
Secondary_Sylow: theory SndSylow
Timing Secondary_Sylow (4 threads, 6.710s elapsed time, 24.800s cpu time, 0.320s GC time, factor 3.70)
Finished Secondary_Sylow (0:00:09 elapsed time, 0:00:27 cpu time, factor 2.83)
Running Bounded_Deducibility_Security ...
Bounded_Deducibility_Security: theory Trivia
Bounded_Deducibility_Security: theory IO_Automaton
Transitive-Closure: theory Transitive_Closure_Impl
Transitive-Closure: theory Utility
Transitive-Closure: theory RBT_Map_Set_Extension
Transitive-Closure: theory Transitive_Closure_List_Impl
Transitive-Closure: theory Finite_Transitive_Closure_Simprocs
Bounded_Deducibility_Security: theory BD_Security
Transitive-Closure: theory Transitive_Closure_RBT_Impl
Bounded_Deducibility_Security: theory Compositional_Reasoning
Bounded_Deducibility_Security: theory Bounded_Deducibility_Security
Timing Transitive-Closure (4 threads, 7.643s elapsed time, 21.448s cpu time, 0.260s GC time, factor 2.81)
Finished Transitive-Closure (0:00:17 elapsed time, 0:00:31 cpu time, factor 1.77)
Running Tail_Recursive_Functions ...
Timing Bounded_Deducibility_Security (4 threads, 7.555s elapsed time, 19.060s cpu time, 0.348s GC time, factor 2.52)
Finished Bounded_Deducibility_Security (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.15)
Tail_Recursive_Functions: theory CaseStudy1
Tail_Recursive_Functions: theory Method
Tail_Recursive_Functions: theory CaseStudy2
ShortestPath: theory ShortestPath
ShortestPath: theory ShortestPathNeg
Timing Tail_Recursive_Functions (4 threads, 7.172s elapsed time, 17.516s cpu time, 0.368s GC time, factor 2.44)
Finished Tail_Recursive_Functions (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.81)
Latin_Square: theory Latin_Square
Timing ShortestPath (4 threads, 6.853s elapsed time, 15.612s cpu time, 0.216s GC time, factor 2.28)
Finished ShortestPath (0:00:14 elapsed time, 0:00:18 cpu time, factor 1.32)
Ramsey-Infinite: theory Infinite_Set
Ramsey-Infinite: theory Ramsey
Timing Latin_Square (4 threads, 7.556s elapsed time, 25.564s cpu time, 0.192s GC time, factor 3.38)
Finished Latin_Square (0:00:10 elapsed time, 0:00:27 cpu time, factor 2.75)
Timing Ramsey-Infinite (4 threads, 7.071s elapsed time, 11.352s cpu time, 0.164s GC time, factor 1.61)
Finished Ramsey-Infinite (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.46)
Running Certification_Monads ...
Certification_Monads: theory Adhoc_Overloading
Certification_Monads: theory Partial_Function_MR
Certification_Monads: theory Generator_Aux
Certification_Monads: theory Derive_Manager
Certification_Monads: theory Monad_Syntax
Certification_Monads: theory Show
Certification_Monads: theory Error_Syntax
Certification_Monads: theory Error_Monad
Certification_Monads: theory Strict_Sum
Certification_Monads: theory Check_Monad
Certification_Monads: theory Parser_Monad
Timing Triangle (4 threads, 6.543s elapsed time, 12.332s cpu time, 0.088s GC time, factor 1.88)
Finished Triangle (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.54)
Running Compiling-Exceptions-Correctly ...
Timing Certification_Monads (4 threads, 6.255s elapsed time, 16.712s cpu time, 0.240s GC time, factor 2.67)
Finished Certification_Monads (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.21)
Compiling-Exceptions-Correctly: theory Exceptions
Timing Compiling-Exceptions-Correctly (4 threads, 5.693s elapsed time, 9.676s cpu time, 0.380s GC time, factor 1.70)
Finished Compiling-Exceptions-Correctly (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.49)
Case_Labeling: theory Hoare_Logic
Case_Labeling: theory Case_Labeling
Case_Labeling: theory Labeled_Hoare
Case_Labeling: theory Conditionals
Case_Labeling: theory Monadic_Language
Timing Show (4 threads, 5.886s elapsed time, 9.928s cpu time, 0.292s GC time, factor 1.69)
Finished Show (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.31)
Case_Labeling: theory Labeled_Hoare_Examples
Case_Labeling: theory Case_Labeling_Examples
ClockSynchInst: theory ICAInstance
ClockSynchInst: theory LynchInstance
Timing Case_Labeling (4 threads, 6.116s elapsed time, 16.356s cpu time, 0.248s GC time, factor 2.67)
Finished Case_Labeling (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.20)
Timing ClockSynchInst (4 threads, 5.476s elapsed time, 21.192s cpu time, 0.156s GC time, factor 3.87)
Finished ClockSynchInst (0:00:07 elapsed time, 0:00:23 cpu time, factor 3.00)
Running ArrowImpossibilityGS ...
Ordinal: theory OrdinalInverse
Timing Ordinal (4 threads, 5.546s elapsed time, 11.044s cpu time, 0.404s GC time, factor 1.99)
Finished Ordinal (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.70)
ArrowImpossibilityGS: theory Arrow_Order
ArrowImpossibilityGS: theory Arrow_Utility
Euler_Partition: theory Additions_to_Main
Euler_Partition: theory Number_Partition
ArrowImpossibilityGS: theory GS
Euler_Partition: theory Euler_Partition
Timing Euler_Partition (4 threads, 5.609s elapsed time, 20.316s cpu time, 0.148s GC time, factor 3.62)
Finished Euler_Partition (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.87)
Timing ArrowImpossibilityGS (4 threads, 6.065s elapsed time, 18.596s cpu time, 0.512s GC time, factor 3.07)
Finished ArrowImpossibilityGS (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.08)
Timing GenClock (4 threads, 5.663s elapsed time, 20.752s cpu time, 0.172s GC time, factor 3.66)
Finished GenClock (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.90)
List_Interleaving: theory ListInterleaving
Timing Cartan_FP (4 threads, 6.124s elapsed time, 16.456s cpu time, 0.116s GC time, factor 2.69)
Finished Cartan_FP (0:00:10 elapsed time, 0:00:20 cpu time, factor 2.02)
Running Stuttering_Equivalence ...
Timing List_Interleaving (4 threads, 5.048s elapsed time, 16.312s cpu time, 0.344s GC time, factor 3.23)
Finished List_Interleaving (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.53)
Stuttering_Equivalence: theory Samplers
Stuttering_Equivalence: theory StutterEquivalence
BinarySearchTree: theory BinaryTree
BinarySearchTree: theory BinaryTree_TacticStyle
Stuttering_Equivalence: theory PLTL
BinarySearchTree: theory BinaryTree_Map
Timing Stuttering_Equivalence (4 threads, 5.187s elapsed time, 19.800s cpu time, 0.264s GC time, factor 3.82)
Finished Stuttering_Equivalence (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.29)
Running Card_Number_Partitions ...
Timing BinarySearchTree (4 threads, 5.478s elapsed time, 17.732s cpu time, 0.328s GC time, factor 3.24)
Finished BinarySearchTree (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.56)
Card_Number_Partitions: theory Additions_to_Main
Card_Number_Partitions: theory Number_Partition
Card_Number_Partitions: theory Card_Number_Partitions
Timing Card_Number_Partitions (4 threads, 5.413s elapsed time, 17.996s cpu time, 0.124s GC time, factor 3.32)
Finished Card_Number_Partitions (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.63)
Timing FinFun (4 threads, 5.604s elapsed time, 19.116s cpu time, 0.372s GC time, factor 3.41)
Finished FinFun (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.71)
Open_Induction: theory Restricted_Predicates
Open_Induction: theory Open_Induction
Pratt_Certificate: theory Pratt_Certificate
Timing Open_Induction (4 threads, 4.645s elapsed time, 12.596s cpu time, 0.168s GC time, factor 2.71)
Finished Open_Induction (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.13)
Timing Pratt_Certificate (4 threads, 5.020s elapsed time, 15.940s cpu time, 0.180s GC time, factor 3.18)
Finished Pratt_Certificate (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.86)
Running Gauss-Jordan-Elim-Fun ...
Gauss-Jordan-Elim-Fun: theory Gauss_Jordan_Elim_Fun
Timing Gauss-Jordan-Elim-Fun (4 threads, 3.890s elapsed time, 11.408s cpu time, 0.092s GC time, factor 2.93)
Finished Gauss-Jordan-Elim-Fun (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.21)
DataRefinementIBP: theory Conj_Disj
DataRefinementIBP: theory WellFoundedTransitive
Timing Category (4 threads, 5.064s elapsed time, 14.624s cpu time, 0.492s GC time, factor 2.89)
Finished Category (0:00:10 elapsed time, 0:00:20 cpu time, factor 1.89)
Running Descartes_Sign_Rule ...
DataRefinementIBP: theory Complete_Lattice_Prop
DataRefinementIBP: theory Preliminaries
DataRefinementIBP: theory Statements
DataRefinementIBP: theory Hoare
DataRefinementIBP: theory Diagram
DataRefinementIBP: theory DataRefinement
Timing DataRefinementIBP (4 threads, 4.267s elapsed time, 12.240s cpu time, 0.128s GC time, factor 2.87)
Finished DataRefinementIBP (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.20)
Running Lifting_Definition_Option ...
Descartes_Sign_Rule: theory Descartes_Sign_Rule
Lifting_Definition_Option: theory Lifting_Definition_Option_Examples
Timing Descartes_Sign_Rule (4 threads, 4.212s elapsed time, 15.264s cpu time, 0.144s GC time, factor 3.62)
Finished Descartes_Sign_Rule (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.11)
Timing Lifting_Definition_Option (4 threads, 3.854s elapsed time, 5.772s cpu time, 0.000s GC time, factor 1.50)
Finished Lifting_Definition_Option (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.31)
DPT-SAT-Solver: theory DPT_SAT_Solver
DPT-SAT-Solver: theory DPT_SAT_Tests
Timing DPT-SAT-Solver (4 threads, 3.423s elapsed time, 8.788s cpu time, 0.036s GC time, factor 2.57)
Finished DPT-SAT-Solver (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.93)
Timing List-Index (4 threads, 3.070s elapsed time, 9.976s cpu time, 0.080s GC time, factor 3.25)
Finished List-Index (0:00:05 elapsed time, 0:00:12 cpu time, factor 2.29)
FunWithFunctions: theory FunWithFunctions
Timing FFT (4 threads, 2.794s elapsed time, 8.036s cpu time, 0.000s GC time, factor 2.88)
Finished FFT (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.03)
Timing FunWithFunctions (4 threads, 2.707s elapsed time, 8.604s cpu time, 0.000s GC time, factor 3.18)
Finished FunWithFunctions (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.18)
General-Triangle: theory GeneralTriangle
Max-Card-Matching: theory Matching
Timing General-Triangle (4 threads, 2.155s elapsed time, 4.128s cpu time, 0.000s GC time, factor 1.92)
Finished General-Triangle (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.44)
Timing Max-Card-Matching (4 threads, 2.250s elapsed time, 7.776s cpu time, 0.000s GC time, factor 3.46)
Finished Max-Card-Matching (0:00:04 elapsed time, 0:00:09 cpu time, factor 2.22)
Timing CofGroups (4 threads, 1.665s elapsed time, 6.228s cpu time, 0.000s GC time, factor 3.74)
Finished CofGroups (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.58)
Running InformationFlowSlicing ...
RIPEMD-160-SPARK: theory RIPEMD_160_SPARK
Timing RIPEMD-160-SPARK (4 threads, 1.995s elapsed time, 3.408s cpu time, 0.000s GC time, factor 1.71)
Finished RIPEMD-160-SPARK (0:00:14 elapsed time, 0:00:05 cpu time, factor 0.41)
Running Depth-First-Search ...
Depth-First-Search: theory DFS
Timing Depth-First-Search (4 threads, 1.546s elapsed time, 4.232s cpu time, 0.000s GC time, factor 2.74)
Finished Depth-First-Search (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.72)
Running Roy_Floyd_Warshall ...
Timing InformationFlowSlicing (4 threads, 1.765s elapsed time, 1.776s cpu time, 0.000s GC time, factor 1.01)
Finished InformationFlowSlicing (0:00:10 elapsed time, 0:00:07 cpu time, factor 0.71)
Running Ordinals_and_Cardinals ...
Roy_Floyd_Warshall: theory Roy_Floyd_Warshall
Ordinals_and_Cardinals: theory Cardinal_Order_Relation_discontinued
Timing Roy_Floyd_Warshall (4 threads, 1.515s elapsed time, 3.208s cpu time, 0.000s GC time, factor 2.12)
Finished Roy_Floyd_Warshall (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.44)
Running Free-Boolean-Algebra ...
Timing Ordinals_and_Cardinals (4 threads, 1.317s elapsed time, 1.400s cpu time, 0.000s GC time, factor 1.06)
Finished Ordinals_and_Cardinals (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
Timing Bondy (4 threads, 1.360s elapsed time, 2.892s cpu time, 0.000s GC time, factor 2.13)
Finished Bondy (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.43)
Running Example-Submission ...
Free-Boolean-Algebra: theory Free_Boolean_Algebra
Example-Submission: theory Submission
Timing Free-Boolean-Algebra (4 threads, 1.550s elapsed time, 4.836s cpu time, 0.000s GC time, factor 3.12)
Finished Free-Boolean-Algebra (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.46)
Timing Example-Submission (4 threads, 1.290s elapsed time, 1.388s cpu time, 0.000s GC time, factor 1.08)
Finished Example-Submission (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, CAVA_buildchain3
CAVA_LTL_Modelchecker: CANCELLED