Console Output

Started by upstream project "isabelle-repo" build number 135
originally caused by:
 Started by an SCM change
[EnvInject] - Loading node environment variables.
Building remotely on worker2 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-repo-afp
[isabelle-repo-afp] $ hg showconfig paths.default
[isabelle-repo-afp] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
searching for changes
adding changesets
adding manifests
adding file changes
added 3 changesets with 16 changes to 11 files
(run 'hg update' to get a working copy)
[isabelle-repo-afp] $ hg update --clean --rev default
11 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-repo-afp] $ hg log --rev . --template {node}
[isabelle-repo-afp] $ hg log --rev . --template {rev}
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://bitbucket.org/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
0 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}
[isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson4190043084664703275.sh
+ bin/isabelle components -a
+ bin/isabelle ci_build afp
+ uname -a
Linux vm-10-155-208-87 3.16.0-4-amd64 #1 SMP Debian 3.16.7-ckt20-1+deb8u3 (2016-01-17) x86_64 GNU/Linux
+ hg id
9ad0bac25a84 tip
+ date
Thu  7 Apr 20:38:24 CEST 2016
+ show_settings
+ set +x
ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 8000"
+ export ISABELLE_CI_TYPE=afp
+ ISABELLE_CI_TYPE=afp
+ /media/data/jenkins/workspace/isabelle-repo-afp/bin/isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ /media/data/jenkins/workspace/isabelle-repo-afp/bin/isabelle scala -J-Xmx4G -howtorun:script -nocompdaemon /media/data/jenkins/.isabelle/ci/ci_build.scala
Session Pure/Pure
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
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 (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Collections (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/CAVA_buildchain1
Session AFP/CAVA_buildchain3
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Promela (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Formal_SSA (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/Bondy (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session AFP/Real_Impl (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/DiskPaxos (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FinFun (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Algebra (main)
Session AFP/JNF-HOL-Lib (AFP)
Session AFP/JNF-AFP-Lib (AFP)
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/VectorSpace (AFP)
Session HOL/HOL-Cardinals
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/Category (AFP)
Session AFP/Category2 (AFP)
Session AFP/CofGroups (AFP)
Session AFP/Coinductive (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Topology (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Deriving (AFP)
Session AFP/Containers (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Show (AFP)
Session AFP/Descartes_Sign_Rule (AFP)
Session AFP/Efficient-Mergesort (AFP)
Session AFP/FOL-Fitting (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/Valuation (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/KBPs (AFP)
Session AFP/LTL (AFP)
Session AFP/LTL_to_DRA (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/Akra_Bazzi (AFP)
Session AFP/Cartan_FP (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/Gauss_Jordan (AFP)
Session HOL/HOL-Probability
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/List_Update (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/Triangle (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Number_Theory
Session AFP/Lehmer (AFP)
Session AFP/Pratt_Certificate (AFP)
Session HOL/HOL-Old_Number_Theory
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Word (main)
Session HOL/HOL-SPARK (main)
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Separation_Algebra (AFP)
Session HOL/HOLCF (main)
Session AFP/Circus (AFP)
Session AFP/HOLCF-HOL-Library
Session AFP/HOLCF-Nominal2
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/PCF (AFP)
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Heard_Of (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HotelKeyCards (AFP)
Session AFP/Huffman (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Integration (AFP)
Session AFP/Jinja (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/Slicing (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/PseudoHoops (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/List-Index (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/MiniML (AFP)
Session AFP/Nominal2 (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/NormByEval (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Ordinal (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/PropResPI (AFP)
Session AFP/RSAPSS (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/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Strong_Security (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/SumSquares (AFP)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Trie (AFP)
Session AFP/UPF (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/XML (AFP)
Cleaning pGCL ...
Cleaning Vickrey_Clarke_Groves ...
Cleaning VectorSpace ...
Cleaning UpDown_Scheme ...
Cleaning Timed_Automata ...
Cleaning Tarskis_Geometry ...
Cleaning SumSquares ...
Cleaning Sturm_Sequences ...
Cleaning Statecharts ...
Cleaning Splay_Tree ...
Cleaning Sort_Encodings ...
Cleaning Simpl ...
Cleaning SequentInvertibility ...
Cleaning Separation_Logic_Imperative_HOL ...
Cleaning SIFUM_Type_Systems ...
Cleaning SIFPL ...
Cleaning SATSolverVerification ...
Cleaning Rep_Fin_Groups ...
Cleaning Regular-Sets ...
Cleaning Regex_Equivalence ...
Cleaning Random_Graph_Subgraph_Threshold ...
Cleaning RSAPSS ...
Cleaning QR_Decomposition ...
Cleaning Psi_Calculi ...
Cleaning Probabilistic_System_Zoo-Non_BNFs ...
Cleaning Probabilistic_System_Zoo-BNFs ...
Cleaning Probabilistic_System_Zoo ...
Cleaning Probabilistic_Noninterference ...
Cleaning Prime_Harmonic_Series ...
Cleaning Planarity_Certificates ...
Cleaning Pi_Calculus ...
Cleaning PCF ...
Cleaning Ordinary_Differential_Equations ...
Cleaning Noninterference_CSP ...
Cleaning Noninterference_Ipurge_Unwinding ...
Cleaning Native_Word ...
Cleaning Marriage ...
Cleaning Markov_Models ...
Cleaning MSO_Regex_Equivalence ...
Cleaning MSO_Examples ...
Cleaning List_Update ...
Cleaning List-Infinite ...
Cleaning Nat-Interval-Logic ...
Cleaning LinearQuantifierElim ...
Cleaning LightweightJava ...
Cleaning Lehmer ...
Cleaning Launchbury ...
Cleaning LatticeProperties ...
Cleaning PseudoHoops ...
Cleaning LTL ...
Cleaning LTL_to_DRA ...
Cleaning Koenigsberg_Friendship ...
Cleaning Kleene_Algebra ...
Cleaning Multirelations ...
Cleaning Regular_Algebras ...
Cleaning Relation_Algebra ...
Cleaning KBPs ...
Cleaning Jinja ...
Cleaning Slicing ...
Cleaning JNF-HOL-Lib ...
Cleaning JNF-AFP-Lib ...
Cleaning Jordan_Normal_Form ...
Cleaning Pre_Polynomial_Factorization ...
Cleaning Polynomial_Factorization ...
Cleaning Pre_Algebraic_Numbers ...
Cleaning Incompleteness ...
Cleaning Heard_Of ...
Cleaning HRB-Slicing ...
Cleaning InformationFlowSlicing_Inter ...
Cleaning Group-Ring-Module ...
Cleaning Valuation ...
Cleaning Graph_Theory ...
Cleaning Girth_Chromatic ...
Cleaning Gauss_Jordan ...
Cleaning Free-Groups ...
Cleaning Formula_Derivatives ...
Cleaning Formula_Derivatives-Examples ...
Cleaning Flyspeck-Tame ...
Cleaning Featherweight_OCL ...
Cleaning Ergodic_Theory ...
Cleaning Encodability_Process_Calculi ...
Cleaning Echelon_Form ...
Cleaning Discrete_Summation ...
Cleaning Deriving ...
Cleaning Derangements ...
Cleaning Density_Compiler ...
Cleaning Datatype_Order_Generator ...
Cleaning CoreC++ ...
Cleaning Containers ...
Cleaning Containers-Benchmarks ...
Cleaning Consensus_Refined ...
Cleaning ComponentDependencies ...
Cleaning Coinductive ...
Cleaning Lazy-Lists-II ...
Cleaning Circus ...
Cleaning Cauchy ...
Cleaning Sqrt_Babylonian ...
Cleaning Call_Arity ...
Cleaning BytecodeLogicJmlTypes ...
Cleaning BDD ...
Cleaning Automatic_Refinement ...
Cleaning Refine_Monadic ...
Cleaning Collections ...
Cleaning CAVA_Base ...
Cleaning CAVA_Automata ...
Cleaning Gabow_SCC ...
Cleaning LTL_to_GBA ...
Cleaning CAVA_buildchain1 ...
Cleaning CAVA_buildchain3 ...
Cleaning CAVA_LTL_Modelchecker ...
Cleaning Promela ...
Cleaning Collections_Examples ...
Cleaning Dijkstra_Shortest_Path ...
Cleaning Formal_SSA ...
Cleaning Network_Security_Policy_Verification ...
Cleaning Tree-Automata ...
Cleaning AutoFocus-Stream ...
Cleaning Applicative_Lifting ...
Cleaning Amortized_Complexity ...
Cleaning Algebraic_Numbers ...
Cleaning Akra_Bazzi ...
Cleaning Affine_Arithmetic ...
Cleaning Abstract-Rewriting ...
Cleaning Matrix ...
Cleaning Matrix_Tensor ...
Cleaning Knot_Theory ...
Cleaning Abortable_Linearizable_Modules ...
Cleaning AWN ...
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Ctr_Sugar
HOL: theory Orderings
HOL: theory SAT
HOL: theory Coinduction
HOL: theory Groups
HOL: theory Lattices
HOL: theory Set
HOL: theory Typedef
HOL: theory Rings
HOL: theory Fun
HOL: theory Complete_Lattices
HOL: theory Inductive
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Fields
HOL: theory Meson
HOL: theory ATP
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory Fun_Def_Base
HOL: theory Hilbert_Choice
HOL: theory Wfrec
HOL: theory Order_Relation
HOL: theory BNF_Wellorder_Relation
HOL: theory Zorn
HOL: theory BNF_Wellorder_Embedding
HOL: theory BNF_Wellorder_Constructions
HOL: theory BNF_Cardinal_Order_Relation
HOL: theory BNF_Cardinal_Arithmetic
HOL: theory BNF_Def
HOL: theory BNF_Composition
HOL: theory Basic_BNFs
HOL: theory BNF_Fixpoint_Base
HOL: theory BNF_Least_Fixpoint
HOL: theory Basic_BNF_LFPs
HOL: theory Num
HOL: theory Transfer
HOL: theory Power
HOL: theory Groups_Big
HOL: theory Equiv_Relations
HOL: theory Lifting
HOL: theory Lifting_Set
HOL: theory Option
HOL: theory Quotient
HOL: theory Extraction
HOL: theory Lattices_Big
HOL: theory Partial_Function
HOL: theory Fun_Def
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Parity
HOL: theory Set_Interval
HOL: theory Divides
HOL: theory Filter
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory SMT
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory Sledgehammer
HOL: theory List
HOL: theory Groups_List
HOL: theory Map
HOL: theory Enum
HOL: theory Random
HOL: theory String
HOL: theory BNF_Greatest_Fixpoint
HOL: theory Predicate
HOL: theory Typerep
HOL: theory Lazy_Sequence
HOL: theory Limited_Sequence
HOL: theory Code_Evaluation
HOL: theory Quickcheck_Random
HOL: theory Quickcheck_Exhaustive
HOL: theory Quickcheck_Narrowing
HOL: theory Random_Pred
HOL: theory Record
HOL: theory Random_Sequence
HOL: theory Predicate_Compile
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Binomial
HOL: theory Conditionally_Complete_Lattices
HOL: theory GCD
HOL: theory Topological_Spaces
HOL: theory Rat
HOL: theory Real
HOL: theory Real_Vector_Spaces
HOL: theory Inequalities
HOL: theory Limits
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (4 threads, 241.699s elapsed time, 726.924s cpu time, 27.756s GC time, factor 3.01)
Finished HOL (0:05:55 elapsed time, 0:14:00 cpu time, factor 2.37)
Building HOL-Library ...
Building HOL-Multivariate_Analysis ...
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Preorder
HOL-Library: theory AList
HOL-Library: theory BNF_Axiomatization
HOL-Library: theory BNF_Corec
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Library: theory Permutations
HOL-Library: theory Bit
HOL-Multivariate_Analysis: theory Old_Datatype
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Product_plus
HOL-Library: theory Bits
HOL-Library: theory Boolean_Algebra
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Product_Order
HOL-Library: theory Bits_Bit
HOL-Library: theory Bourbaki_Witt_Fixpoint
HOL-Library: theory Cardinal_Notations
HOL-Library: theory Char_ord
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Library: theory Code_Abstract_Nat
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Library: theory Code_Char
HOL-Library: theory Code_Binary_Nat
HOL-Multivariate_Analysis: theory Liminf_Limsup
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Code_Prolog
HOL-Library: theory Code_Test
HOL-Library: theory DAList
HOL-Multivariate_Analysis: theory Countable
HOL-Library: theory Complete_Partial_Order2
HOL-Multivariate_Analysis: theory Nonpos_Ints
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Library: theory FSet
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Periodic_Fun
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Library: theory Debug
HOL-Multivariate_Analysis: theory PolyRoots
HOL-Library: theory Discrete
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Library: theory Disjoint_Sets
HOL-Multivariate_Analysis: theory Countable_Complete_Lattices
HOL-Library: theory Dlist
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Library: theory Fraction_Field
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Library: theory Fun_Lexorder
HOL-Library: theory FuncSet
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Growth
HOL-Library: theory Function_Division
HOL-Library: theory Code_Target_Int
HOL-Library: theory Groups_Big_Fun
HOL-Library: theory IArray
HOL-Library: theory Code_Target_Numeral
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Order_Continuity
HOL-Library: theory Infinite_Set
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Library: theory LaTeXsugar
HOL-Library: theory Lattice_Constructions
HOL-Library: theory ListVector
HOL-Library: theory Omega_Words_Fun
HOL-Library: theory List_lexord
HOL-Library: theory Mapping
HOL-Library: theory Misc_Numeric
HOL-Library: theory Misc_Typedef
HOL-Library: theory Bit_Representation
HOL-Library: theory Monad_Syntax
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Library: theory More_List
HOL-Library: theory AList_Mapping
HOL-Library: theory Multiset
HOL-Library: theory Bits_Int
HOL-Library: theory Nat_Bijection
HOL-Library: theory Stream
HOL-Library: theory Old_Datatype
HOL-Library: theory Bool_List_Representation
HOL-Library: theory Old_Recdef
HOL-Library: theory Option_ord
HOL-Library: theory Countable
HOL-Library: theory Parallel
HOL-Library: theory Phantom_Type
HOL-Multivariate_Analysis: theory Extended_Nonnegative_Real
HOL-Multivariate_Analysis: theory Summation
HOL-Library: theory Product_Lexorder
HOL-Library: theory Product_plus
HOL-Library: theory Cardinality
HOL-Library: theory Product_Order
HOL-Library: theory DAList_Multiset
HOL-Library: theory Multiset_Order
HOL-Library: theory Permutation
HOL-Library: theory Countable_Set
HOL-Library: theory Finite_Lattice
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Countable_Complete_Lattices
HOL-Multivariate_Analysis: theory Bounded_Linear_Function
HOL-Library: theory Countable_Set_Type
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Uniform_Limit
HOL-Library: theory Type_Length
HOL-Library: theory Saturated
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_List
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Refute
HOL-Library: theory Rewrite
HOL-Library: theory Set_Algebras
HOL-Library: theory Simps_Case_Conv
HOL-Library: theory Extended
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Polynomial
HOL-Library: theory Sublist_Order
HOL-Library: theory BigO
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Indicator_Function
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Euclidean_Algorithm
HOL-Library: theory Polynomial_GCD_euclidean
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Multivariate_Analysis: theory Weierstrass
HOL-Multivariate_Analysis: theory Integration
HOL-Library: theory Product_Vector
HOL-Library: theory Convex
HOL-Library: theory Liminf_Limsup
HOL-Library: theory Lub_Glb
HOL-Library: theory OptionalSugar
HOL-Library: theory Order_Continuity
HOL-Library: theory Float
HOL-Library: theory Extended_Nat
HOL-Library: theory Extended_Real
HOL-Multivariate_Analysis: theory Bounded_Continuous_Function
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Integral_Test
HOL-Library: theory Linear_Temporal_Logic_on_Streams
HOL-Library: theory Formal_Power_Series
HOL-Multivariate_Analysis: theory Complex_Analysis_Basics
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Ordered_Euclidean_Space
HOL-Library: theory Quadratic_Discriminant
HOL-Library: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Complex_Transcendental
HOL-Library: theory Extended_Nonnegative_Real
HOL-Multivariate_Analysis: theory Generalised_Binomial_Theorem
HOL-Multivariate_Analysis: theory Harmonic_Numbers
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Tree
HOL-Library: theory While_Combinator
HOL-Multivariate_Analysis: theory Gamma
HOL-Library: theory Word_Miscellaneous
HOL-Library: theory Word
HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm
HOL-Library: theory Tree_Multiset
HOL-Library: theory Library
HOL-Multivariate_Analysis: theory Conformal_Mappings
HOL-Library: theory Old_SMT
HOL-Multivariate_Analysis: theory Multivariate_Analysis
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory RBT_Set
Timing HOL-Library (4 threads, 211.617s elapsed time, 754.840s cpu time, 24.228s GC time, factor 3.57)
Finished HOL-Library (0:05:59 elapsed time, 0:15:02 cpu time, factor 2.51)
Building HOLCF ...
HOLCF: theory Nat_Bijection
HOLCF: theory Old_Datatype
HOLCF: theory Countable
HOLCF: theory Porder
HOLCF: theory Pcpo
HOLCF: theory Cont
HOLCF: theory Adm
HOLCF: theory Discrete
HOLCF: theory Fun_Cpo
HOLCF: theory Product_Cpo
HOLCF: theory Cpodef
HOLCF: theory Cfun
HOLCF: theory Cprod
HOLCF: theory Sprod
HOLCF: theory Sfun
HOLCF: theory Fix
HOLCF: theory Up
HOLCF: theory Lift
HOLCF: theory One
HOLCF: theory Tr
HOLCF: theory Ssum
HOLCF: theory Plain_HOLCF
HOLCF: theory Completion
HOLCF: theory Fixrec
HOLCF: theory Deflation
HOLCF: theory Map_Functions
HOLCF: theory Bifinite
HOLCF: theory Domain_Aux
HOLCF: theory Universal
HOLCF: theory Algebraic
HOLCF: theory Compact_Basis
HOLCF: theory LowerPD
HOLCF: theory UpperPD
HOLCF: theory Representable
HOLCF: theory ConvexPD
HOLCF: theory Domain
HOLCF: theory Powerdomains
HOLCF: theory HOLCF
Timing HOL-Multivariate_Analysis (4 threads, 328.434s elapsed time, 1232.252s cpu time, 21.448s GC time, factor 3.75)
Finished HOL-Multivariate_Analysis (0:06:48 elapsed time, 0:21:52 cpu time, factor 3.21)
Building HOL-Probability ...
HOL-Probability: theory Multiset
HOL-Probability: theory Diagonal_Subsequence
Timing HOLCF (4 threads, 25.175s elapsed time, 59.772s cpu time, 2.184s GC time, factor 2.37)
Finished HOLCF (0:00:54 elapsed time, 0:01:29 cpu time, factor 1.63)
Building HOL-Nominal ...
HOL-Nominal: theory Old_Datatype
HOL-Nominal: theory Infinite_Set
HOL-Probability: theory Permutation
HOL-Nominal: theory Nominal
HOL-Probability: theory Adhoc_Overloading
HOL-Probability: theory Disjoint_Sets
HOL-Probability: theory Stream
HOL-Probability: theory Sublist
HOL-Probability: theory Monad_Syntax
HOL-Probability: theory ContNotDenum
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Linear_Temporal_Logic_on_Streams
HOL-Probability: theory Measurable
HOL-Probability: theory Borel_Space
HOL-Probability: theory Measure_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Nonnegative_Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Embed_Measure
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Bochner_Integration
HOL-Probability: theory Fin_Map
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Set_Integral
HOL-Probability: theory Interval_Integral
HOL-Probability: theory Lebesgue_Integral_Substitution
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Distribution_Functions
HOL-Probability: theory Giry_Monad
HOL-Probability: theory Weak_Convergence
HOL-Probability: theory Helly_Selection
HOL-Probability: theory Probability_Mass_Function
HOL-Probability: theory Projective_Family
Timing HOL-Nominal (4 threads, 13.745s elapsed time, 33.968s cpu time, 1.020s GC time, factor 2.47)
Finished HOL-Nominal (0:00:37 elapsed time, 0:00:57 cpu time, factor 1.53)
HOL-Probability: theory Infinite_Product_Measure
Building HOL-Algebra ...
HOL-Probability: theory Independent_Family
HOL-Probability: theory Stream_Space
HOL-Probability: theory Projective_Limit
HOL-Algebra: theory FuncSet
HOL-Algebra: theory Primes
HOL-Algebra: theory Multiset
HOL-Probability: theory Convolution
HOL-Probability: theory Information
HOL-Probability: theory Distributions
HOL-Algebra: theory Permutation
HOL-Probability: theory Characteristic_Functions
HOL-Probability: theory Sinc_Integral
HOL-Probability: theory Levy
HOL-Probability: theory Central_Limit_Theorem
HOL-Probability: theory Probability
HOL-Algebra: theory Congruence
HOL-Algebra: theory Exponent
HOL-Algebra: theory Lattice
HOL-Algebra: theory Group
HOL-Algebra: theory Bij
HOL-Algebra: theory Coset
HOL-Algebra: theory FiniteProduct
HOL-Algebra: theory Ring
HOL-Algebra: theory Sylow
HOL-Algebra: theory Divisibility
HOL-Algebra: theory AbelCoset
HOL-Algebra: theory Module
HOL-Algebra: theory Ideal
HOL-Algebra: theory RingHom
HOL-Algebra: theory QuotRing
HOL-Algebra: theory UnivPoly
HOL-Algebra: theory IntRing
Timing HOL-Algebra (4 threads, 75.551s elapsed time, 253.312s cpu time, 9.740s GC time, factor 3.35)
Finished HOL-Algebra (0:02:08 elapsed time, 0:05:05 cpu time, factor 2.39)
Building Abstract-Rewriting ...
Abstract-Rewriting: theory Regular_Set
Abstract-Rewriting: theory While_Combinator
Abstract-Rewriting: theory Regular_Exp
Abstract-Rewriting: theory NDerivative
Abstract-Rewriting: theory Relation_Interpretation
Abstract-Rewriting: theory Equivalence_Checking
Abstract-Rewriting: theory Regexp_Method
Abstract-Rewriting: theory Infinite_Set
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
Timing Abstract-Rewriting (4 threads, 46.122s elapsed time, 136.208s cpu time, 3.844s GC time, factor 2.95)
Finished Abstract-Rewriting (0:01:28 elapsed time, 0:03:03 cpu time, factor 2.07)
Building HOL-Word ...
HOL-Word: theory Bit
HOL-Word: theory Bits
HOL-Word: theory Boolean_Algebra
HOL-Word: theory Misc_Numeric
HOL-Word: theory Bit_Representation
HOL-Word: theory Misc_Typedef
HOL-Word: theory Phantom_Type
HOL-Word: theory Bits_Bit
HOL-Word: theory Word_Miscellaneous
HOL-Word: theory Bits_Int
HOL-Word: theory Cardinality
HOL-Word: theory Numeral_Type
HOL-Word: theory Bool_List_Representation
HOL-Word: theory Type_Length
HOL-Word: theory Word
Timing HOL-Word (4 threads, 17.623s elapsed time, 61.508s cpu time, 1.912s GC time, factor 3.49)
Finished HOL-Word (0:00:43 elapsed time, 0:01:27 cpu time, factor 2.00)
Building Kleene_Algebra ...
Kleene_Algebra: theory Signatures
Kleene_Algebra: theory Dioid
Kleene_Algebra: theory Conway
Kleene_Algebra: theory Finite_Suprema
Kleene_Algebra: theory Matrix
Kleene_Algebra: theory Dioid_Models
Kleene_Algebra: theory Inf_Matrix
Timing HOL-Probability (4 threads, 263.371s elapsed time, 980.852s cpu time, 15.276s GC time, factor 3.72)
Finished HOL-Probability (0:05:34 elapsed time, 0:17:31 cpu time, factor 3.15)
Building Coinductive ...
Kleene_Algebra: theory Kleene_Algebra
Coinductive: theory Prefix_Order
Coinductive: theory L2_Norm
Coinductive: theory Primes
Coinductive: theory Norm_Arith
Coinductive: theory Euclidean_Space
Coinductive: theory Linear_Algebra
Kleene_Algebra: theory DRA
Kleene_Algebra: theory Omega_Algebra
Kleene_Algebra: theory PHL_KA
Kleene_Algebra: theory Kleene_Algebra_Models
Coinductive: theory Topology_Euclidean_Space
Kleene_Algebra: theory Formal_Power_Series
Kleene_Algebra: theory PHL_DRA
Kleene_Algebra: theory Omega_Algebra_Models
Coinductive: theory Extended_Real_Limits
Coinductive: theory Coinductive_Nat
Coinductive: theory Resumption
Coinductive: theory Coinductive_List
Coinductive: theory CCPO_Topology
Coinductive: theory Coinductive_List_Prefix
Coinductive: theory Hamming_Stream
Coinductive: theory Koenigslemma
Coinductive: theory LMirror
Coinductive: theory Lazy_LList
Coinductive: theory Quotient_Coinductive_List
Coinductive: theory TLList
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 Kleene_Algebra (4 threads, 53.301s elapsed time, 125.364s cpu time, 4.096s GC time, factor 2.35)
Finished Kleene_Algebra (0:01:40 elapsed time, 0:02:52 cpu time, factor 1.72)
Building Jinja ...
Jinja: theory Code_Abstract_Nat
Jinja: theory Code_Target_Int
Jinja: theory Sublist
Jinja: theory While_Combinator
Jinja: theory Code_Target_Nat
Jinja: theory Code_Target_Numeral
Jinja: theory Auxiliary
Jinja: theory List_Index
Jinja: theory Transitive_Closure_Table
Jinja: theory Semilat
Jinja: theory Type
Jinja: theory Hidden
Jinja: theory Err
Jinja: theory Decl
Jinja: theory TypeRel
Jinja: theory Listn
Jinja: theory Opt
Jinja: theory Product
Jinja: theory Semilattices
Jinja: theory Typing_Framework
Jinja: theory SemilatAlg
Jinja: theory Kildall
Jinja: theory LBVSpec
Jinja: theory Value
Jinja: theory Typing_Framework_err
Jinja: theory LBVComplete
Jinja: theory LBVCorrect
Jinja: theory Objects
Jinja: theory Abstract_BV
Jinja: theory Exceptions
Jinja: theory JVMState
Jinja: theory JVMInstructions
Jinja: theory Conform
Jinja: theory Expr
Jinja: theory State
Jinja: theory SystemClasses
Jinja: theory WellForm
Jinja: theory PCompiler
Jinja: theory SemiType
Jinja: theory JVM_SemiType
Jinja: theory JVMExceptions
Jinja: theory JVMExecInstr
Jinja: theory Effect
Jinja: theory JVMExec
Jinja: theory JVMDefensive
Jinja: theory JVMListExample
Jinja: theory Examples
Jinja: theory BigStep
Jinja: theory SmallStep
Jinja: theory WellType
Jinja: theory Annotate
Jinja: theory WellTypeRT
Jinja: theory DefAss
Jinja: theory J1
Jinja: theory execute_Bigstep
Jinja: theory execute_WellType
Jinja: theory Compiler1
Jinja: theory Compiler2
Jinja: theory WWellForm
Jinja: theory Correctness2
Jinja: theory Equivalence
Jinja: theory Progress
Jinja: theory JWellForm
Jinja: theory J1WellForm
Jinja: theory BVSpec
Jinja: theory BVConform
Jinja: theory TypeSafe
Jinja: theory BVSpecTypeSafe
Jinja: theory Correctness1
Jinja: theory Compiler
Jinja: theory EffectMono
Jinja: theory TF_JVM
Jinja: theory TypeComp
Jinja: theory BVExec
Jinja: theory BVNoTypeError
Jinja: theory BVExample
Jinja: theory LBVJVM
Jinja: theory Jinja
Timing Coinductive (4 threads, 96.098s elapsed time, 315.456s cpu time, 6.736s GC time, factor 3.28)
Finished Coinductive (0:02:43 elapsed time, 0:06:44 cpu time, factor 2.47)
Building Simpl ...
Simpl: theory DistinctTreeProver
Simpl: theory LaTeXsugar
Simpl: theory Multiset
Simpl: theory Old_Recdef
Simpl: theory Simpl_Heap
Simpl: theory HeapList
Simpl: theory Language
Simpl: theory Generalise
Simpl: theory StateFun
Simpl: theory StateSpaceLocale
Simpl: theory StateSpaceSyntax
Simpl: theory Permutation
Simpl: theory Semantic
Simpl: theory HoarePartialDef
Simpl: theory Termination
Simpl: theory HoarePartialProps
Simpl: theory HoareTotalDef
Simpl: theory SmallStep
Simpl: theory AlternativeSmallStep
Simpl: theory HoarePartial
Simpl: theory HoareTotalProps
Simpl: theory Compose
Simpl: theory HoareTotal
Simpl: theory Hoare
Simpl: theory Closure
Simpl: theory StateSpace
Simpl: theory Vcg
Simpl: theory ProcParEx
Simpl: theory ProcParExSP
Simpl: theory XVcg
Simpl: theory ClosureEx
Simpl: theory XVcgEx
Simpl: theory ComposeEx
Simpl: theory Quicksort
Simpl: theory SyntaxTest
Simpl: theory UserGuide
Simpl: theory VcgEx
Simpl: theory VcgExSP
Simpl: theory VcgExTotal
Simpl: theory Simpl
Jinja FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/Jinja)
val fs4 = fn:
   Isabelle1268989.Generated_Code.char list *
   Isabelle1268989.Generated_Code.char list
     -> Isabelle1268989.Generated_Code.vala option
val F = [Char (Bit0 (Bit1 (Bit1 (Bit0 (Bit0 (Bit0 One))))))]:
   Isabelle1268989.Generated_Code.char list
val L = [Char (Bit0 (Bit0 (Bit1 (Bit1 (Bit0 (Bit0 One))))))]:
   Isabelle1268989.Generated_Code.char list
val N = [Char (Bit0 (Bit1 (Bit1 (Bit1 (Bit0 (Bit0 One))))))]:
   Isabelle1268989.Generated_Code.char list
val it = (): unit
val l = fn:
   Isabelle1268827.Generated_Code.char list ->
     Isabelle1268827.Generated_Code.vala option
val h = fn:
   Isabelle1268827.Generated_Code.nat ->
     (Isabelle1268827.Generated_Code.char list *
      (Isabelle1268827.Generated_Code.char list *
       Isabelle1268827.Generated_Code.char list
         -> Isabelle1268827.Generated_Code.vala option)
     )
     option
val c = [Char (Bit1 (Bit1 (Bit0 (Bit0 (Bit0 (Bit0 One))))))]:
   Isabelle1268827.Generated_Code.char list
val fs = fn:
   Isabelle1268827.Generated_Code.char list *
   Isabelle1268827.Generated_Code.char list
     -> Isabelle1268827.Generated_Code.vala option
val obj =
   [Char (Bit1 (Bit1 (Bit1 (Bit1 (Bit0 (Bit0 One)))))),
    Char (Bit0 (Bit1 (Bit0 (Bit0 (Bit0 (Bit1 One)))))),
    Char (Bit0 (Bit1 (Bit0 (Bit1 (Bit0 (Bit1 One)))))),
    Char (Bit1 (Bit0 (Bit1 (Bit0 (Bit0 (Bit1 One)))))),
    Char (Bit1 (Bit1 (Bit0 (Bit0 (Bit0 (Bit1 One)))))),
    Char (Bit0 (Bit0 (Bit1 (Bit0 (Bit1 (Bit1 One))))))]:
   Isabelle1268827.Generated_Code.char list
val i = Int_of_integer 42: Isabelle1268827.Generated_Code.inta
val it = (): unit
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Building Deriving ...
Deriving: theory More_Bits_Int
Deriving: theory Bits_Integer
Deriving: theory Word_Misc
Timing Simpl (4 threads, 121.553s elapsed time, 421.328s cpu time, 17.064s GC time, factor 3.47)
Finished Simpl (0:03:39 elapsed time, 0:08:39 cpu time, factor 2.36)
Building LTL ...
LTL: theory LTL
Deriving: theory Code_Target_Bits_Int
Deriving: theory Code_Target_ICF
Deriving: theory Uint32
Deriving: theory HashCode
Deriving: theory Comparator
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 Compare
Deriving: theory Comparator_Generator
Deriving: theory RBT_Comparator_Impl
Deriving: theory Hash_Instances
LTL: theory LTL_Rewrite
Deriving: theory RBT_Compare_Order_Impl
Deriving: theory Compare_Generator
Deriving: theory Compare_Instances
Deriving: theory Compare_Rat
Deriving: theory Compare_Real
Deriving: theory Compare_Order_Instances
Deriving: theory Derive
Deriving: theory Derive_Examples
LTL: theory LTL_Example
Timing LTL (4 threads, 31.936s elapsed time, 80.180s cpu time, 2.488s GC time, factor 2.51)
Finished LTL (0:01:26 elapsed time, 0:02:14 cpu time, factor 1.55)
Building HOL-Cardinals ...
HOL-Cardinals: theory Order_Union
HOL-Cardinals: theory Cardinal_Notations
HOL-Cardinals: theory Fun_More
HOL-Cardinals: theory Order_Relation_More
HOL-Cardinals: theory Wellorder_Extension
HOL-Cardinals: theory Wellfounded_More
HOL-Cardinals: theory Wellorder_Relation
HOL-Cardinals: theory Wellorder_Embedding
HOL-Cardinals: theory Wellorder_Constructions
HOL-Cardinals: theory Cardinal_Order_Relation
HOL-Cardinals: theory Ordinal_Arithmetic
HOL-Cardinals: theory Cardinal_Arithmetic
HOL-Cardinals: theory Cardinals
HOL-Cardinals: theory Bounded_Set
Timing Deriving (4 threads, 48.220s elapsed time, 91.024s cpu time, 3.884s GC time, factor 1.89)
Finished Deriving (0:01:59 elapsed time, 0:03:20 cpu time, factor 1.69)
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.447s elapsed time, 13.584s cpu time, 0.224s GC time, factor 2.49)
Finished LatticeProperties (0:00:24 elapsed time, 0:00:32 cpu time, factor 1.33)
Building MSO_Regex_Equivalence ...
Timing HOL-Cardinals (4 threads, 23.127s elapsed time, 84.584s cpu time, 1.960s GC time, factor 3.66)
Finished HOL-Cardinals (0:00:47 elapsed time, 0:01:49 cpu time, factor 2.28)
HRB-Slicing CANCELLED
Slicing CANCELLED
Building Formula_Derivatives ...
MSO_Regex_Equivalence: theory Derive_Manager
MSO_Regex_Equivalence: theory Comparator
MSO_Regex_Equivalence: theory Generator_Aux
MSO_Regex_Equivalence: theory List_Index
MSO_Regex_Equivalence: theory List_More
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
MSO_Regex_Equivalence: theory Compare
MSO_Regex_Equivalence: theory Comparator_Generator
MSO_Regex_Equivalence: theory Compare_Generator
Formula_Derivatives: theory Compare
Formula_Derivatives: theory Comparator_Generator
MSO_Regex_Equivalence: theory Compare_Instances
Formula_Derivatives: theory Compare_Generator
Formula_Derivatives: theory Compare_Instances
MSO_Regex_Equivalence FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/MSO_Regex_Equivalence)
### theory "Compare_Instances"
### 0.777s elapsed time, 3.108s cpu time, 0.000s GC time
(if ?x \<le> ?y then if ?x = ?y then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y = ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y \<le> ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?x < ?y then ?Q else ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x \<le> ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y \<le> ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x \<le> ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Building Echelon_Form ...
Echelon_Form: theory Bit
Echelon_Form: theory Code_Abstract_Nat
Echelon_Form: theory Dual_Order
Echelon_Form: theory Code_Target_Int
Echelon_Form: theory Code_Target_Nat
Formula_Derivatives FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/Formula_Derivatives)
### theory "Compare_Instances"
### 0.828s elapsed time, 3.216s cpu time, 0.000s GC time
(if ?x \<le> ?y then if ?x = ?y then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y = ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y \<le> ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?x < ?y then ?Q else ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x \<le> ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y \<le> ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x \<le> ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Building Datatype_Order_Generator ...
Echelon_Form: theory IArray
Echelon_Form: theory More_List
Echelon_Form: theory Code_Target_Numeral
Echelon_Form: theory Code_Set
Echelon_Form: theory Mod_Type
Echelon_Form: theory Polynomial
Echelon_Form: theory Code_Bit
Echelon_Form: theory Generalizations
Echelon_Form: theory IArray_Addenda
Echelon_Form: theory Square_Matrix
Datatype_Order_Generator: theory More_Bits_Int
Echelon_Form: theory Miscellaneous
Echelon_Form: theory Cayley_Hamilton
Datatype_Order_Generator: theory Bits_Integer
Datatype_Order_Generator: theory Word_Misc
Echelon_Form: theory Code_Matrix
Echelon_Form: theory Fundamental_Subspaces
Echelon_Form: theory Rref
Echelon_Form: theory Dim_Formula
Echelon_Form: theory Elementary_Operations
Echelon_Form: theory Rank
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 Inverse
Echelon_Form: theory System_Of_Equations
Echelon_Form: theory Inverse_IArrays
Echelon_Form: theory Examples_Gauss_Jordan_Abstract
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 Rings2
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 Examples_Echelon_Form_Abstract
Echelon_Form: theory Echelon_Form_Det_IArrays
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, 247.480s elapsed time, 825.204s cpu time, 14.984s GC time, factor 3.33)
Finished Echelon_Form (0:05:11 elapsed time, 0:14:49 cpu time, factor 2.85)
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
Timing Datatype_Order_Generator (4 threads, 176.668s elapsed time, 332.564s cpu time, 21.416s GC time, factor 1.88)
Finished Datatype_Order_Generator (0:05:59 elapsed time, 0:09:13 cpu time, factor 1.54)
Building HOL-Imperative_HOL ...
HOL-Imperative_HOL: theory LaTeXsugar
HOL-Imperative_HOL: theory Adhoc_Overloading
HOL-Imperative_HOL: theory Nat_Bijection
HOL-Imperative_HOL: theory Old_Datatype
HOL-Imperative_HOL: theory Monad_Syntax
Group-Ring-Module: theory Algebra7
HOL-Imperative_HOL: theory Countable
HOL-Imperative_HOL: theory Code_Target_Int
HOL-Imperative_HOL: theory Multiset
HOL-Imperative_HOL: theory Heap
HOL-Imperative_HOL: theory Code_Abstract_Nat
HOL-Imperative_HOL: theory Code_Target_Nat
HOL-Imperative_HOL: theory RBT_Impl
HOL-Imperative_HOL: theory Code_Target_Numeral
HOL-Imperative_HOL: theory Sorted_List
HOL-Imperative_HOL: theory Heap_Monad
Group-Ring-Module: theory Algebra8
HOL-Imperative_HOL: theory Array
HOL-Imperative_HOL: theory List_Sublist
HOL-Imperative_HOL: theory Ref
HOL-Imperative_HOL: theory Subarray
HOL-Imperative_HOL: theory Imperative_HOL
HOL-Imperative_HOL: theory Linked_Lists
HOL-Imperative_HOL: theory Overview
HOL-Imperative_HOL: theory Imperative_Quicksort
HOL-Imperative_HOL: theory Imperative_Reverse
Group-Ring-Module: theory Algebra9
HOL-Imperative_HOL: theory SatChecker
HOL-Imperative_HOL: theory Imperative_HOL_ex
Timing Group-Ring-Module (4 threads, 189.362s elapsed time, 607.416s cpu time, 15.324s GC time, factor 3.21)
Finished Group-Ring-Module (0:04:05 elapsed time, 0:11:03 cpu time, factor 2.70)
Building Containers ...
Containers: theory Regular_Set
Timing HOL-Imperative_HOL (4 threads, 128.502s elapsed time, 298.936s cpu time, 8.324s GC time, factor 2.33)
Finished HOL-Imperative_HOL (0:03:23 elapsed time, 0:10:46 cpu time, factor 3.18)
Building Graph_Theory ...
Containers: theory Regular_Exp
Graph_Theory: theory Nat_Bijection
Graph_Theory: theory Infinite_Set
Graph_Theory: theory Old_Datatype
Graph_Theory: theory Liminf_Limsup
Containers: theory NDerivative
Containers: theory Relation_Interpretation
Graph_Theory: theory Countable
Graph_Theory: theory Countable_Set
Graph_Theory: theory Countable_Complete_Lattices
Containers: theory Equivalence_Checking
Graph_Theory: theory Order_Continuity
Containers: theory Regexp_Method
Graph_Theory: theory Extended_Nat
Graph_Theory: theory Extended_Real
Containers: theory Equal
Containers: theory AssocList
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 RBT_ext
Containers: theory DList_Set
Containers: theory Set_Linorder
Graph_Theory: theory FuncSet
Graph_Theory: theory Permutations
Graph_Theory: theory Rewrite
Graph_Theory: theory Rtrancl_On
Graph_Theory: theory Stuff
Graph_Theory: theory Digraph
Graph_Theory: theory Funpow
Graph_Theory: theory Arc_Walk
Graph_Theory: theory Bidirected_Digraph
Containers: theory Collection_Order
Graph_Theory: theory Vertex_Walk
Graph_Theory: theory Pair_Digraph
Graph_Theory: theory Weighted_Graph
Graph_Theory: theory Shortest_Path
Containers: theory List_Proper_Interval
Containers: theory RBT_Mapping2
Containers: theory RBT_Set2
Containers: theory Set_Impl
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 Euler
Graph_Theory: theory Graph_Theory
Containers: theory Mapping_Impl
Containers: theory Map_To_Mapping
Containers: theory Containers
Containers: theory Containers_Userguide
Containers: theory Compatibility_Containers_Regular_Sets
Containers: theory Map_To_Mapping_Ex
Containers: theory Card_Datatype_Ex
Timing Graph_Theory (4 threads, 81.382s elapsed time, 280.672s cpu time, 8.816s GC time, factor 3.45)
Finished Graph_Theory (0:02:04 elapsed time, 0:05:23 cpu time, factor 2.60)
Building JNF-HOL-Lib ...
JNF-HOL-Lib: theory Adhoc_Overloading
JNF-HOL-Lib: theory Lattice_Syntax
JNF-HOL-Lib: theory Order_Union
JNF-HOL-Lib: theory AList
JNF-HOL-Lib: theory Permutations
JNF-HOL-Lib: theory Char_ord
JNF-HOL-Lib: theory Code_Abstract_Nat
JNF-HOL-Lib: theory Code_Char
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 Cong
JNF-HOL-Lib: theory Code_Target_Numeral
JNF-HOL-Lib: theory IArray
JNF-HOL-Lib: theory Infinite_Set
JNF-HOL-Lib: theory List_lexord
JNF-HOL-Lib: theory DAList
JNF-HOL-Lib: theory Mapping
JNF-HOL-Lib: theory Monad_Syntax
JNF-HOL-Lib: theory More_List
JNF-HOL-Lib: theory UniqueFactorization
JNF-HOL-Lib: theory Phantom_Type
JNF-HOL-Lib: theory RBT_Impl
JNF-HOL-Lib: theory Ramsey
JNF-HOL-Lib: theory Cardinality
JNF-HOL-Lib: theory Simps_Case_Conv
JNF-HOL-Lib: theory DAList_Multiset
JNF-HOL-Lib: theory Polynomial
JNF-HOL-Lib: theory Wellorder_Extension
JNF-HOL-Lib: theory While_Combinator
JNF-HOL-Lib: theory Fundamental_Theorem_Algebra
Timing Containers (4 threads, 111.320s elapsed time, 310.204s cpu time, 10.720s GC time, factor 2.79)
Finished Containers (0:03:55 elapsed time, 0:07:18 cpu time, factor 1.87)
Building HOL-Number_Theory ...
HOL-Number_Theory: theory FuncSet
HOL-Number_Theory: theory Congruence
HOL-Number_Theory: theory Multiset
HOL-Number_Theory: theory Lattice
HOL-Number_Theory: theory Group
HOL-Number_Theory: theory FiniteProduct
HOL-Number_Theory: theory Ring
HOL-Number_Theory: theory MiscAlgebra
HOL-Number_Theory: theory Fib
HOL-Number_Theory: theory Infinite_Set
HOL-Number_Theory: theory Primes
HOL-Number_Theory: theory More_List
HOL-Number_Theory: theory Cong
HOL-Number_Theory: theory Eratosthenes
HOL-Number_Theory: theory Factorial_Ring
HOL-Number_Theory: theory Polynomial
HOL-Number_Theory: theory UniqueFactorization
HOL-Number_Theory: theory Residues
HOL-Number_Theory: theory Gauss
HOL-Number_Theory: theory Number_Theory
HOL-Number_Theory: theory Pocklington
HOL-Number_Theory: theory Euclidean_Algorithm
Timing JNF-HOL-Lib (4 threads, 68.828s elapsed time, 247.452s cpu time, 7.328s GC time, factor 3.60)
Finished JNF-HOL-Lib (0:02:20 elapsed time, 0:05:19 cpu time, factor 2.27)
Building JNF-AFP-Lib ...
JNF-AFP-Lib: theory Comparator
JNF-AFP-Lib: theory Derive_Manager
JNF-AFP-Lib: theory Equal
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 List_Fusion
JNF-AFP-Lib: theory Equality_Generator
JNF-AFP-Lib: theory IArray_Haskell
JNF-AFP-Lib: theory Containers_Auxiliary
JNF-AFP-Lib: theory Containers_Generator
JNF-AFP-Lib: theory Equality_Instances
JNF-AFP-Lib: theory Compare
JNF-AFP-Lib: theory Comparator_Generator
JNF-AFP-Lib: theory Collection_Enum
JNF-AFP-Lib: theory Lexicographic_Order
JNF-AFP-Lib: theory Collection_Eq
JNF-AFP-Lib: theory Compare_Generator
JNF-AFP-Lib: theory Set_Linorder
JNF-AFP-Lib: theory Compare_Instances
JNF-AFP-Lib: theory RBT_Comparator_Impl
JNF-AFP-Lib: theory DList_Set
JNF-AFP-Lib: theory RBT_ext
JNF-AFP-Lib: theory Regular_Set
JNF-AFP-Lib: theory RingModuleFacts
JNF-AFP-Lib: theory Regular_Exp
JNF-AFP-Lib: theory MonoidSums
JNF-AFP-Lib: theory LinearCombinations
JNF-AFP-Lib: theory Seq
JNF-AFP-Lib: theory Show
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 Utility
JNF-AFP-Lib: theory Equivalence_Checking
JNF-AFP-Lib: theory Regexp_Method
JNF-AFP-Lib: theory RBT_Mapping2
JNF-AFP-Lib: theory Abstract_Rewriting
JNF-AFP-Lib: theory RBT_Set2
JNF-AFP-Lib: theory SumSpaces
JNF-AFP-Lib: theory Relative_Rewriting
JNF-AFP-Lib: theory Set_Impl
JNF-AFP-Lib: theory VectorSpace
JNF-AFP-Lib: theory Missing_Polynomial
JNF-AFP-Lib: theory SN_Orders
JNF-AFP-Lib: theory Ring_Hom
JNF-AFP-Lib: theory Ordered_Semiring
JNF-AFP-Lib: theory SN_Order_Carrier
Timing HOL-Number_Theory (4 threads, 64.192s elapsed time, 222.364s cpu time, 5.184s GC time, factor 3.46)
Finished HOL-Number_Theory (0:01:47 elapsed time, 0:04:25 cpu time, factor 2.47)
Building Lehmer ...
Lehmer: theory Coset
Lehmer: theory Module
Lehmer: theory AbelCoset
Lehmer: theory Ideal
Lehmer: theory RingHom
Lehmer: theory UnivPoly
Lehmer: theory Multiplicative_Group
Lehmer: theory Lehmer
Timing Lehmer (4 threads, 59.426s elapsed time, 138.752s cpu time, 5.156s GC time, factor 2.33)
Finished Lehmer (0:01:37 elapsed time, 0:02:56 cpu time, factor 1.82)
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
Regex_Equivalence: theory Regex_Equivalence
Timing JNF-AFP-Lib (4 threads, 141.860s elapsed time, 501.020s cpu time, 16.060s GC time, factor 3.53)
Finished JNF-AFP-Lib (0:04:16 elapsed time, 0:10:20 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
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
Pre_Polynomial_Factorization: theory Sqrt_Babylonian
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
Timing Regex_Equivalence (4 threads, 47.275s elapsed time, 159.308s cpu time, 5.376s GC time, factor 3.37)
Finished Regex_Equivalence (0:02:04 elapsed time, 0:04:01 cpu time, factor 1.94)
Building Koenigsberg_Friendship_Base ...
Koenigsberg_Friendship_Base: theory AList
Koenigsberg_Friendship_Base: theory FuncSet
Koenigsberg_Friendship_Base: theory Congruence
Koenigsberg_Friendship_Base: theory Fib
Koenigsberg_Friendship_Base: theory Primes
Koenigsberg_Friendship_Base: theory Graph
Koenigsberg_Friendship_Base: theory Cong
Koenigsberg_Friendship_Base: theory Lattice
Koenigsberg_Friendship_Base: theory Eratosthenes
Koenigsberg_Friendship_Base: theory DAList
Koenigsberg_Friendship_Base: theory Multiset
Koenigsberg_Friendship_Base: theory Group
Koenigsberg_Friendship_Base: theory FiniteProduct
Koenigsberg_Friendship_Base: theory Ring
Koenigsberg_Friendship_Base: theory UniqueFactorization
Koenigsberg_Friendship_Base: theory MiscAlgebra
Koenigsberg_Friendship_Base: theory Residues
Koenigsberg_Friendship_Base: theory Number_Theory
Timing Koenigsberg_Friendship_Base (4 threads, 42.713s elapsed time, 152.796s cpu time, 4.896s GC time, factor 3.58)
Finished Koenigsberg_Friendship_Base (0:01:18 elapsed time, 0:03:08 cpu time, factor 2.39)
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
Timing Pre_Polynomial_Factorization (4 threads, 55.022s elapsed time, 192.580s cpu time, 4.600s GC time, factor 3.50)
Finished Pre_Polynomial_Factorization (0:01:54 elapsed time, 0:04:11 cpu time, factor 2.20)
Automatic_Refinement: theory Refine_Util
Automatic_Refinement: theory Omega_Words_Fun
Building Polynomial_Factorization ...
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
Polynomial_Factorization: theory Missing_Multiset
Polynomial_Factorization: theory Precomputation
Polynomial_Factorization: theory Order_Polynomial
Polynomial_Factorization: theory Missing_List
Automatic_Refinement: theory Misc
Polynomial_Factorization: theory Explicit_Roots
Polynomial_Factorization: theory Dvd_Int_Poly
Polynomial_Factorization: theory Prime_Factorization
Polynomial_Factorization: theory Gauss_Lemma
Polynomial_Factorization: theory Rational_Root_Test
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_Phases
Automatic_Refinement: theory Autoref_Tagging
Automatic_Refinement: theory Autoref_Id_Ops
Polynomial_Factorization: theory Kronecker_Factorization
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_Tool
Automatic_Refinement: theory Autoref_Chapter
Automatic_Refinement: theory Autoref_Bindings_HOL
Polynomial_Factorization: theory Unique_Factorization_Domain
Automatic_Refinement: theory Automatic_Refinement
Polynomial_Factorization: theory Polynomial_Divisibility
Polynomial_Factorization: theory Square_Free_Factorization
Polynomial_Factorization: theory Prime_Field
Polynomial_Factorization: theory Polynomial_Division
Polynomial_Factorization: theory Polynomial_Field
Polynomial_Factorization: theory Gauss_Jordan_Field
Polynomial_Factorization: theory Berlekamp_Hensel_Factorization
Polynomial_Factorization: theory External_Factorization
Polynomial_Factorization: theory Factorization_Oracle
Polynomial_Factorization: theory Hybrid_Factorization
Polynomial_Factorization: theory Select_Berlekamp_Hensel_Factorization
Polynomial_Factorization: theory Select_Hybrid_Factorization
Polynomial_Factorization: theory Select_External_Factorization
Polynomial_Factorization: theory Rational_Factorization
Timing Automatic_Refinement (4 threads, 42.771s elapsed time, 134.384s cpu time, 3.612s GC time, factor 3.14)
Finished Automatic_Refinement (0:01:17 elapsed time, 0:02:50 cpu time, factor 2.19)
Building Refine_Monadic ...
Refine_Monadic: theory Lattice_Syntax
Refine_Monadic: theory Adhoc_Overloading
Refine_Monadic: theory Bit
Refine_Monadic: theory Bits
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 Word
Refine_Monadic: theory Refine_Chapter
Refine_Monadic: theory Example_Chapter
Refine_Monadic: theory Refine_Mono_Prover
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 Polynomial_Factorization (4 threads, 73.369s elapsed time, 196.400s cpu time, 3.684s GC time, factor 2.68)
Finished Polynomial_Factorization (0:02:23 elapsed time, 0:04:26 cpu time, factor 1.85)
Building Pre_Algebraic_Numbers ...
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 Refine_Monadic (4 threads, 44.438s elapsed time, 152.460s cpu time, 4.620s GC time, factor 3.43)
Finished Refine_Monadic (0:01:28 elapsed time, 0:03:16 cpu time, factor 2.23)
Building Collections ...
Collections: theory Code_Abstract_Nat
Collections: theory Code_Target_Int
Collections: theory FingerTree
Collections: theory BinomialHeap
Collections: theory Code_Target_Nat
Collections: theory SkewBinomialHeap
Collections: theory Code_Target_Numeral
Collections: theory Dlist
Collections: theory ICF_Tools
Collections: theory More_Bits_Int
Collections: theory AList
Collections: theory Ord_Code_Preproc
Collections: theory Locale_Code
Collections: theory Partial_Equivalence_Relation
Collections: theory SetIterator
Collections: theory RBT_Impl
Collections: theory Record_Intf
Collections: theory Sorted_List_Operations
Collections: theory Bits_Integer
Collections: theory Idx_Iterator
Collections: theory SetIteratorOperations
Collections: theory Word_Misc
Collections: theory Assoc_List
Collections: theory Diff_Array
Collections: theory Dlist_add
Collections: theory Proper_Iterator
Collections: theory It_to_It
Collections: theory SetIteratorGA
Collections: theory Gen_Iterator
Collections: theory Iterator
Collections: theory ICF_Spec_Base
Collections: theory MapSpec
Collections: theory Robdd
Collections: theory Code_Target_Bits_Int
Collections: theory Uint32
Collections: theory Code_Target_ICF
Collections: theory Locale_Code_Ex
Collections: theory HashCode
Timing Pre_Algebraic_Numbers (4 threads, 41.532s elapsed time, 154.996s cpu time, 2.124s GC time, factor 3.73)
Finished Pre_Algebraic_Numbers (0:01:38 elapsed time, 0:03:31 cpu time, factor 2.15)
Building HOL-Old_Number_Theory ...
HOL-Old_Number_Theory: theory Multiset
HOL-Old_Number_Theory: theory Infinite_Set
HOL-Old_Number_Theory: theory Permutation
Collections: theory RBT_add
HOL-Old_Number_Theory: theory BijectionRel
HOL-Old_Number_Theory: theory Legacy_GCD
HOL-Old_Number_Theory: theory Primes
HOL-Old_Number_Theory: theory Factorization
HOL-Old_Number_Theory: theory Fib
HOL-Old_Number_Theory: theory IntPrimes
HOL-Old_Number_Theory: theory Pocklington
HOL-Old_Number_Theory: theory Chinese
HOL-Old_Number_Theory: theory IntFact
HOL-Old_Number_Theory: theory EulerFermat
HOL-Old_Number_Theory: theory Finite2
HOL-Old_Number_Theory: theory WilsonBij
HOL-Old_Number_Theory: theory WilsonRuss
HOL-Old_Number_Theory: theory Int2
HOL-Old_Number_Theory: theory EvenOdd
HOL-Old_Number_Theory: theory Residues
HOL-Old_Number_Theory: theory Euler
HOL-Old_Number_Theory: theory Gauss
HOL-Old_Number_Theory: theory Quadratic_Reciprocity
Collections: theory DatRef
Collections: theory SetAbstractionIterator
Collections: theory GenCF_Chapter
Collections: theory GenCF_Intf_Chapter
Collections: theory GenCF_Gen_Chapter
Collections: theory GenCF_Impl_Chapter
Collections: theory Intf_Comp
Collections: theory Impl_Array_Stack
Collections: theory Array_Iterator
Collections: theory Intf_Map
Collections: theory Intf_Set
Collections: theory Gen_Map
Collections: theory Intf_Hash
Collections: theory Gen_Set
Collections: theory Impl_Cfun_Set
Collections: theory Impl_List_Set
Collections: theory Gen_Comp
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
Timing HOL-Old_Number_Theory (4 threads, 41.202s elapsed time, 146.016s cpu time, 2.728s GC time, factor 3.54)
Finished HOL-Old_Number_Theory (0:01:10 elapsed time, 0:02:55 cpu time, factor 2.49)
Building Matrix ...
Matrix: theory Congruence
Matrix: theory FuncSet
Matrix: theory Lattice
Collections: theory Impl_Bit_Set
Collections: theory Uint
Collections: theory Gen_Hash
Matrix: theory Group
Collections: theory Impl_Uv_Set
Matrix: theory FiniteProduct
Matrix: theory Ring
Matrix: theory Utility
Matrix: theory Ordered_Semiring
Matrix: theory Matrix_Arith
Matrix: theory Matrix_Comparison
Collections: theory GenCF
Matrix: theory Matrix
Collections: theory Trie
Collections: theory ICF_Gen_Algo_Chapter
Collections: theory ICF_Chapter
Collections: theory ICF_Impl_Chapter
Collections: theory ICF_Spec_Chapter
Collections: theory RBT
Collections: theory AnnotatedListSpec
Collections: theory ListSpec
Collections: theory PrioSpec
Collections: theory ListGA
Collections: theory Trie_Impl
Collections: theory BinoPrioImpl
Collections: theory FTAnnotatedListImpl
Collections: theory Trie2
Collections: theory Fifo
Collections: theory PrioByAnnotatedList
Collections: theory SkewPrioImpl
Collections: theory PrioUniqueSpec
Collections: theory SetSpec
Collections: theory PrioUniqueByAnnotatedList
Collections: theory FTPrioImpl
Collections: theory FTPrioUniqueImpl
Collections: theory Algos
Collections: theory SetIndex
Collections: theory SetIteratorCollectionsGA
Collections: theory MapGA
Collections: theory SetGA
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 SetByMap
Collections: theory ArrayHashMap_Impl
Collections: theory HashMap_Impl
Collections: theory ArraySetImpl
Collections: theory TrieSetImpl
Collections: theory RBTSetImpl
Collections: theory ArrayHashMap
Collections: theory HashMap
Collections: theory ArrayHashSet
Collections: theory HashSet
Collections: theory MapStdImpl
Collections: theory SetStdImpl
Timing Matrix (4 threads, 39.281s elapsed time, 133.468s cpu time, 3.460s GC time, factor 3.40)
Finished Matrix (0:01:16 elapsed time, 0:02:50 cpu time, factor 2.22)
Building Matrix_Tensor ...
Matrix_Tensor: theory Matrix_Tensor
Collections: theory ICF_Impl
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_ICF
Collections: theory Refine_Dflt
Collections: theory Userguides_Chapter
Collections: theory ICF_Userguide
Collections: theory Refine_Monadic_Userguide
Timing Matrix_Tensor (4 threads, 42.846s elapsed time, 98.620s cpu time, 2.428s GC time, factor 2.30)
Finished Matrix_Tensor (0:01:07 elapsed time, 0:02:02 cpu time, factor 1.83)
Building Applicative_Lifting ...
Applicative_Lifting: theory Function_Algebras
Applicative_Lifting: theory Commutation
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_Examples
Applicative_Lifting: theory Applicative_Functor
Applicative_Lifting: theory Abstract_AF
Applicative_Lifting: theory Applicative_Test
Timing Applicative_Lifting (4 threads, 34.382s elapsed time, 79.988s cpu time, 2.680s GC time, factor 2.33)
Finished Applicative_Lifting (0:01:23 elapsed time, 0:02:09 cpu time, factor 1.55)
InformationFlowSlicing_Inter CANCELLED
Building Sturm_Sequences ...
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
Sturm_Sequences: theory Sturm_Ex
Timing Sturm_Sequences (4 threads, 29.486s elapsed time, 105.084s cpu time, 1.232s GC time, factor 3.56)
Finished Sturm_Sequences (0:01:07 elapsed time, 0:02:23 cpu time, factor 2.11)
Building Relation_Algebra ...
Relation_Algebra: theory More_Boolean_Algebra
Relation_Algebra: theory Relation_Algebra
Relation_Algebra: theory Relation_Algebra_RTC
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.234s elapsed time, 64.480s cpu time, 2.256s GC time, factor 3.35)
Finished Relation_Algebra (0:00:52 elapsed time, 0:01:37 cpu time, factor 1.85)
Building List-Infinite ...
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
List-Infinite: theory InfiniteSet2
List-Infinite: theory SetIntervalCut
List-Infinite: theory List2
List-Infinite: theory SetIntervalStep
List-Infinite: theory ListInf
List-Infinite: theory ListInf_Prefix
List-Infinite: theory ListInfinite
Timing List-Infinite (4 threads, 18.204s elapsed time, 66.480s cpu time, 2.096s GC time, factor 3.65)
Finished List-Infinite (0:00:59 elapsed time, 0:01:47 cpu time, factor 1.80)
Building Nat-Interval-Logic ...
Nat-Interval-Logic: theory IL_Interval
Nat-Interval-Logic: theory IL_IntervalOperators
Nat-Interval-Logic: theory IL_TemporalOperators
Timing Collections (4 threads, 278.691s elapsed time, 795.208s cpu time, 35.488s GC time, factor 2.85)
Finished Collections (0:09:43 elapsed time, 0:19:34 cpu time, factor 2.01)
Building HOLCF-HOL-Library ...
HOLCF-HOL-Library: theory AList
HOLCF-HOL-Library: theory FuncSet
HOLCF-HOL-Library: theory Infinite_Set
HOLCF-HOL-Library: theory LaTeXsugar
HOLCF-HOL-Library: theory Multiset
HOLCF-HOL-Library: theory Quotient_Syntax
HOLCF-HOL-Library: theory Quotient_Option
HOLCF-HOL-Library: theory Permutation
Timing HOLCF-HOL-Library (4 threads, 14.108s elapsed time, 49.880s cpu time, 1.332s GC time, factor 3.54)
Finished HOLCF-HOL-Library (0:00:40 elapsed time, 0:01:15 cpu time, factor 1.89)
Building HOLCF-Nominal2 ...
HOLCF-Nominal2: theory Phantom_Type
HOLCF-Nominal2: theory Quotient_Product
HOLCF-Nominal2: theory Quotient_Set
HOLCF-Nominal2: theory Quotient_List
Timing Nat-Interval-Logic (4 threads, 31.692s elapsed time, 87.580s cpu time, 1.132s GC time, factor 2.76)
Finished Nat-Interval-Logic (0:01:10 elapsed time, 0:02:06 cpu time, factor 1.79)
Building CAVA_Base ...
HOLCF-Nominal2: theory FSet
HOLCF-Nominal2: theory Cardinality
HOLCF-Nominal2: theory FinFun
HOLCF-Nominal2: theory Nominal2_Base
CAVA_Base: theory Char_ord
CAVA_Base: theory Derive_Manager
CAVA_Base: theory Comparator
CAVA_Base: theory Generator_Aux
CAVA_Base: theory Nat_Bijection
CAVA_Base: theory Code_Char
CAVA_Base: theory Old_Datatype
CAVA_Base: theory Equality_Generator
CAVA_Base: theory Statistics
CAVA_Base: theory Equality_Instances
CAVA_Base: theory Hash_Generator
CAVA_Base: theory Code_String
HOLCF-Nominal2: theory Atoms
HOLCF-Nominal2: theory Eqvt
HOLCF-Nominal2: theory Nominal2_Abs
CAVA_Base: theory Compare
CAVA_Base: theory Comparator_Generator
CAVA_Base: theory Countable
CAVA_Base: theory Hash_Instances
CAVA_Base: theory CAVA_Code_Target
CAVA_Base: theory CAVA_Base
CAVA_Base: theory Compare_Generator
CAVA_Base: theory Compare_Instances
CAVA_Base: theory Countable_Generator
HOLCF-Nominal2: theory Nominal2_FCB
CAVA_Base: theory All_Of_CAVA_Base
CAVA_Base: theory Derive
HOLCF-Nominal2: theory Nominal2
Timing HOLCF-Nominal2 (4 threads, 21.883s elapsed time, 78.624s cpu time, 2.288s GC time, factor 3.59)
Finished HOLCF-Nominal2 (0:00:54 elapsed time, 0:01:51 cpu time, factor 2.03)
Building Launchbury ...
Launchbury: theory AList-Utils
Launchbury: theory Pointwise
Launchbury: theory Mono-Nat-Fun
Launchbury: theory HOLCF-Join
Launchbury: theory HOLCF-Meet
Launchbury: theory C
Launchbury: theory HOLCF-Join-Classes
Launchbury: theory HOLCF-Utils
Launchbury: theory Value
Launchbury: theory CValue
Launchbury: theory C-Meet
Launchbury: theory C-restr
Launchbury: theory Env
Launchbury: theory Nominal-Utils
Launchbury: theory ValueSimilarity
Launchbury: theory Vars
Launchbury: theory Env-HOLCF
Launchbury: theory EvalHeap
Launchbury: theory AList-Utils-Nominal
Launchbury: theory Iterative
Launchbury: theory Nominal-HOLCF
Launchbury: theory Terms
Launchbury: theory CValue-Nominal
Launchbury: theory Env-Nominal
Launchbury: theory HasESem
Launchbury: theory Value-Nominal
Launchbury: theory HeapSemantics
Launchbury: theory AbstractDenotational
Launchbury: theory Substitution
Launchbury: theory Abstract-Denotational-Props
Launchbury: theory Launchbury
Launchbury: theory Denotational
Launchbury: theory ResourcedDenotational
Timing CAVA_Base (4 threads, 13.410s elapsed time, 35.400s cpu time, 1.184s GC time, factor 2.64)
Finished CAVA_Base (0:01:15 elapsed time, 0:01:37 cpu time, factor 1.29)
Building CAVA_Automata ...
Launchbury: theory CorrectnessOriginal
Launchbury: theory Denotational-Related
Launchbury: theory CorrectnessResourced
Launchbury: theory ResourcedAdequacy
Launchbury: theory Adequacy
Launchbury: theory EverythingAdequacy
CAVA_Automata: theory Step_Conv
CAVA_Automata: theory Digraph
CAVA_Automata: theory Automata
CAVA_Automata: theory Digraph_Impl
CAVA_Automata: theory Lasso
CAVA_Automata: theory Simulation
CAVA_Automata: theory Stuttering_Extension
CAVA_Automata: theory Automata_Impl
Timing Launchbury (4 threads, 40.256s elapsed time, 146.484s cpu time, 3.804s GC time, factor 3.64)
Finished Launchbury (0:01:29 elapsed time, 0:03:15 cpu time, factor 2.19)
Building Noninterference_CSP ...
Noninterference_CSP: theory CSPNoninterference
Noninterference_CSP: theory ClassicalNoninterference
Noninterference_CSP: theory GeneralizedNoninterference
Timing Noninterference_CSP (4 threads, 8.990s elapsed time, 31.072s cpu time, 0.360s GC time, factor 3.46)
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
CAVA_Automata: theory All_Of_CAVA_Automata
Noninterference_Ipurge_Unwinding: theory IpurgeUnwinding
Noninterference_Ipurge_Unwinding: theory DeterministicProcesses
Timing Noninterference_Ipurge_Unwinding (4 threads, 14.396s elapsed time, 44.012s cpu time, 0.992s GC time, factor 3.06)
Finished Noninterference_Ipurge_Unwinding (0:00:37 elapsed time, 0:01:07 cpu time, factor 1.79)
Building Marriage ...
Marriage: theory Marriage
Timing Marriage (4 threads, 4.439s elapsed time, 12.168s cpu time, 0.100s GC time, factor 2.74)
Finished Marriage (0:00:22 elapsed time, 0:00:30 cpu time, factor 1.34)
Building HOL-SPARK ...
HOL-SPARK: theory Bit_Comparison
HOL-SPARK: theory SPARK_Setup
HOL-SPARK: theory SPARK
Timing CAVA_Automata (4 threads, 102.092s elapsed time, 169.156s cpu time, 5.704s GC time, factor 1.66)
Finished CAVA_Automata (0:02:51 elapsed time, 0:04:03 cpu time, factor 1.42)
Building LTL_to_GBA ...
LTL_to_GBA: theory LTL
LTL_to_GBA: theory Samplers
LTL_to_GBA: theory StutterEquivalence
Timing HOL-SPARK (4 threads, 3.494s elapsed time, 8.528s cpu time, 0.000s GC time, factor 2.44)
Finished HOL-SPARK (0:00:24 elapsed time, 0:00:29 cpu time, factor 1.20)
Building HOL-SPARK-Examples ...
HOL-SPARK-Examples: theory RMD_Lemmas
HOL-SPARK-Examples: theory Greatest_Common_Divisor
HOL-SPARK-Examples: theory Longest_Increasing_Subsequence
HOL-SPARK-Examples: theory RMD
HOL-SPARK-Examples: theory Sqrt
HOL-SPARK-Examples: theory RMD_Specification
HOL-SPARK-Examples: theory F
HOL-SPARK-Examples: theory Hash
HOL-SPARK-Examples: theory K_L
HOL-SPARK-Examples: theory K_R
HOL-SPARK-Examples: theory R_L
HOL-SPARK-Examples: theory R_R
HOL-SPARK-Examples: theory Round
HOL-SPARK-Examples: theory S_L
HOL-SPARK-Examples: theory S_R
LTL_to_GBA: theory PLTL
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
LTL_to_GBA: theory LTL_to_GBA
LTL_to_GBA: theory LTL_to_GBA_impl
Timing HOL-SPARK-Examples (4 threads, 21.219s elapsed time, 56.340s cpu time, 1.100s GC time, factor 2.66)
Finished HOL-SPARK-Examples (0:00:52 elapsed time, 0:01:27 cpu time, factor 1.66)
Building Cauchy ...
Cauchy: theory CauchySchwarz
Cauchy: theory CauchysMeanTheorem
Timing Cauchy (4 threads, 5.431s elapsed time, 19.472s cpu time, 0.184s GC time, factor 3.59)
Finished Cauchy (0:00:25 elapsed time, 0:00:39 cpu time, factor 1.55)
Building Sqrt_Babylonian ...
Sqrt_Babylonian: theory Sqrt_Babylonian_Auxiliary
Sqrt_Babylonian: theory NthRoot_Impl
Sqrt_Babylonian: theory Sqrt_Babylonian
Timing Sqrt_Babylonian (4 threads, 17.606s elapsed time, 47.160s cpu time, 0.580s GC time, factor 2.68)
Finished Sqrt_Babylonian (0:00:40 elapsed time, 0:01:10 cpu time, factor 1.72)
Building Discrete_Summation ...
Discrete_Summation: theory Stirling
Discrete_Summation: theory Summation
Discrete_Summation: theory Factorials
Discrete_Summation: theory Summation_Conversion
Discrete_Summation: theory Examples
Timing Discrete_Summation (4 threads, 5.015s elapsed time, 16.284s cpu time, 0.152s GC time, factor 3.25)
Finished Discrete_Summation (0:00:26 elapsed time, 0:00:37 cpu time, factor 1.42)
Building Lazy-Lists-II ...
Lazy-Lists-II: theory LList2
Timing Lazy-Lists-II (4 threads, 4.637s elapsed time, 14.116s cpu time, 0.256s GC time, factor 3.04)
Finished Lazy-Lists-II (0:00:48 elapsed time, 0:00:57 cpu time, factor 1.19)
Running Decreasing-Diagrams ...
Decreasing-Diagrams: theory Multiset
LTL_to_GBA: theory All_Of_LTL_to_GBA
Decreasing-Diagrams: theory Decreasing_Diagrams
Timing Decreasing-Diagrams (4 threads, 24.866s elapsed time, 86.648s cpu time, 1.832s GC time, factor 3.48)
Finished Decreasing-Diagrams (0:00:27 elapsed time, 0:01:29 cpu time, factor 3.22)
Running IEEE_Floating_Point ...
IEEE_Floating_Point: theory IEEE
IEEE_Floating_Point: theory Code_Float
IEEE_Floating_Point: theory FloatProperty
IEEE_Floating_Point: theory RoundError
Timing IEEE_Floating_Point (4 threads, 17.414s elapsed time, 53.512s cpu time, 0.616s GC time, factor 3.07)
Finished IEEE_Floating_Point (0:00:19 elapsed time, 0:00:55 cpu time, factor 2.82)
Running Pratt_Certificate ...
Pratt_Certificate: theory Pratt_Certificate
Timing Pratt_Certificate (4 threads, 4.934s elapsed time, 15.768s cpu time, 0.176s GC time, factor 3.20)
Finished Pratt_Certificate (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.29)
Running ShortestPath ...
ShortestPath: theory ShortestPath
ShortestPath: theory ShortestPathNeg
Timing ShortestPath (4 threads, 6.349s elapsed time, 15.044s cpu time, 0.212s GC time, factor 2.37)
Finished ShortestPath (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.92)
Running Tail_Recursive_Functions ...
Tail_Recursive_Functions: theory CaseStudy1
Tail_Recursive_Functions: theory Method
Tail_Recursive_Functions: theory CaseStudy2
Timing Tail_Recursive_Functions (4 threads, 7.103s elapsed time, 16.964s cpu time, 0.352s GC time, factor 2.39)
Finished Tail_Recursive_Functions (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.78)
Running Algebraic_Numbers ...
Algebraic_Numbers: theory Compare_Complex
Algebraic_Numbers: theory Binary_Exponentiation
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
Algebraic_Numbers: theory Algebraic_Numbers
Algebraic_Numbers: theory Real_Algebraic_Numbers
Timing LTL_to_GBA (4 threads, 216.707s elapsed time, 753.680s cpu time, 14.820s GC time, factor 3.48)
Finished LTL_to_GBA (0:05:33 elapsed time, 0:14:35 cpu time, factor 2.63)
Building CAVA_buildchain1 ...
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
CAVA_buildchain1: theory Gabow_Skeleton
CAVA_buildchain1: theory Find_Path
CAVA_buildchain1: theory Find_Path_Impl
CAVA_buildchain1: theory Gabow_SCC
CAVA_buildchain1: theory Gabow_GBG
CAVA_buildchain1: theory Gabow_Skeleton_Code
Algebraic_Numbers: theory Show_Real_Precise
Algebraic_Numbers: theory Algebraic_Number_Tests
CAVA_buildchain1: theory Gabow_GBG_Code
CAVA_buildchain1: theory Gabow_SCC_Code
CAVA_buildchain1: theory All_Of_Gabow_SCC
Timing CAVA_buildchain1 (4 threads, 154.444s elapsed time, 401.284s cpu time, 8.772s GC time, factor 2.60)
Finished CAVA_buildchain1 (0:04:20 elapsed time, 0:08:48 cpu time, factor 2.03)
Building CAVA_buildchain3 ...
CAVA_buildchain3: theory Lexord_List
CAVA_buildchain3: theory PromelaAST
CAVA_buildchain3: theory IArray
CAVA_buildchain3: theory PromelaStatistics
CAVA_buildchain3: theory PromelaDatastructures
CAVA_buildchain3: theory PromelaInvariants
CAVA_buildchain3: theory Promela
CAVA_buildchain3: theory PromelaLTL
CAVA_buildchain3: theory PromelaLTLConv
CAVA_buildchain3: theory All_Of_Promela
Timing Algebraic_Numbers (4 threads, 580.537s elapsed time, 1408.560s cpu time, 252.076s GC time, factor 2.43)
Finished Algebraic_Numbers (0:09:49 elapsed time, 0:23:37 cpu time, factor 2.40)
Running Incompleteness ...
Incompleteness: theory Infinite_Set
Incompleteness: theory Nat_Bijection
Incompleteness: theory Multiset
Incompleteness: theory Old_Datatype
Incompleteness: theory Phantom_Type
Incompleteness: theory HF
Incompleteness: theory Cardinality
Incompleteness: theory Quotient_Syntax
Incompleteness: theory Ordinal
Incompleteness: theory Quotient_Option
Incompleteness: theory Quotient_Product
Incompleteness: theory Quotient_Set
Incompleteness: theory Quotient_List
Incompleteness: theory Rank
Incompleteness: theory FinFun
Incompleteness: theory OrdArith
Incompleteness: theory FSet
Incompleteness: theory Nominal2_Base
Incompleteness: theory Nominal2_Abs
Incompleteness: theory Nominal2_FCB
Incompleteness: theory Nominal2
Incompleteness: theory SyntaxN
Incompleteness: theory Coding
Incompleteness: theory Predicates
Incompleteness: theory Sigma
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 Quote
Incompleteness: theory Goedel_II
Timing CAVA_buildchain3 (4 threads, 255.098s elapsed time, 432.352s cpu time, 24.020s GC time, factor 1.69)
Finished CAVA_buildchain3 (0:08:24 elapsed time, 0:11:34 cpu time, factor 1.38)
Running Psi_Calculi ...
Psi_Calculi: theory Chain
Psi_Calculi: theory Subst_Term
Psi_Calculi: theory Agent
Psi_Calculi: theory Close_Subst
Psi_Calculi: theory Frame
Psi_Calculi: theory Structural_Congruence
Psi_Calculi: theory Semantics
Psi_Calculi: theory Simulation
Psi_Calculi: theory Bisimulation
Psi_Calculi: theory Sim_Pres
Psi_Calculi: theory Sim_Struct_Cong
Psi_Calculi: theory Sum
Psi_Calculi: theory Bisim_Pres
Psi_Calculi: theory Tau_Chain
Psi_Calculi: theory Bisim_Struct_Cong
Psi_Calculi: theory Weak_Simulation
Psi_Calculi: theory Weak_Stat_Imp
Psi_Calculi: theory Bisim_Subst
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 Weakening
Psi_Calculi: theory Weak_Bisim_Struct_Cong
Psi_Calculi: theory Weak_Cong_Pres
Psi_Calculi: theory Weaken_Transition
Psi_Calculi: theory Weaken_Stat_Imp
Psi_Calculi: theory Weak_Cong_Struct_Cong
Psi_Calculi: theory Weaken_Simulation
Psi_Calculi: theory Weak_Congruence
Psi_Calculi: theory Weaken_Bisimulation
Psi_Calculi: theory Tau
Psi_Calculi: theory Tau_Sim
Psi_Calculi: theory Tau_Stat_Imp
Psi_Calculi: theory Tau_Laws_No_Weak
Psi_Calculi: theory Tau_Laws_Weak
Timing Incompleteness (4 threads, 611.485s elapsed time, 1971.904s cpu time, 14.524s GC time, factor 3.22)
Finished Incompleteness (0:10:19 elapsed time, 0:32:54 cpu time, factor 3.18)
Running CAVA_LTL_Modelchecker ...
CAVA_LTL_Modelchecker: theory NDFS_SI_Statistics
CAVA_LTL_Modelchecker: theory NDFS_SI
Timing Psi_Calculi (4 threads, 490.139s elapsed time, 1787.068s cpu time, 39.180s GC time, factor 3.65)
Finished Psi_Calculi (0:08:14 elapsed time, 0:29:49 cpu time, factor 3.62)
Running CoreC++ ...
CoreC++: theory Auxiliary
CoreC++: theory Type
CoreC++: theory Value
CoreC++: theory Expr
CoreC++: theory Decl
CoreC++: theory ClassRel
CoreC++: theory SubObj
CoreC++: theory Objects
CoreC++: theory TypeRel
CoreC++: theory Exceptions
CoreC++: theory State
CoreC++: theory Syntax
CoreC++: theory SystemClasses
CoreC++: theory BigStep
CoreC++: theory SmallStep
CoreC++: theory WellType
CoreC++: theory Annotate
CoreC++: theory WellForm
CoreC++: theory WellTypeRT
CoreC++: theory WWellForm
CoreC++: theory Conform
CoreC++: theory DefAss
CoreC++: theory Execute
CoreC++: theory CWellForm
CoreC++: theory Equivalence
CoreC++: theory Progress
CoreC++: theory HeapExtension
CoreC++: theory TypeSafe
CoreC++: theory Determinism
CAVA_LTL_Modelchecker: theory CAVA_Abstract
CAVA_LTL_Modelchecker: theory Mapping
CAVA_LTL_Modelchecker: theory AList_Mapping
CAVA_LTL_Modelchecker: theory BoolProgs
CAVA_LTL_Modelchecker: theory BoolProgs_Extras
CAVA_LTL_Modelchecker: theory BoolProgs_LTL_Conv
CAVA_LTL_Modelchecker: theory BoolProgs_Philosophers
CAVA_LTL_Modelchecker: theory BoolProgs_LeaderFilters
CAVA_LTL_Modelchecker: theory BoolProgs_ReaderWriter
CAVA_LTL_Modelchecker: theory BoolProgs_Simple
CAVA_LTL_Modelchecker: theory BoolProgs_Programs
CAVA_LTL_Modelchecker: theory CAVA_Impl
CoreC++: theory CoreC++
Timing CoreC++ (4 threads, 198.004s elapsed time, 654.884s cpu time, 24.600s GC time, factor 3.31)
Finished CoreC++ (0:03:29 elapsed time, 0:11:00 cpu time, factor 3.16)
Running Affine_Arithmetic ...
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
Affine_Arithmetic: theory Permutation
Affine_Arithmetic: theory Float
Affine_Arithmetic: theory Float_Real
Affine_Arithmetic: theory Affine_Form
Affine_Arithmetic: theory Counterclockwise
Affine_Arithmetic: theory Euclidean_Space_Explicit
Affine_Arithmetic: theory Executable_Euclidean_Space
Affine_Arithmetic: theory Counterclockwise_Vector
Affine_Arithmetic: theory Counterclockwise_2D_Strict
Affine_Arithmetic: theory Counterclockwise_2D_Arbitrary
Affine_Arithmetic: theory Polygon
Affine_Arithmetic: theory Affine_Approximation
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
CAVA_LTL_Modelchecker: theory All_Of_Nested_DFS
CAVA_LTL_Modelchecker: theory All_Of_CAVA_LTL_Modelchecker
Timing CAVA_LTL_Modelchecker (4 threads, 366.495s elapsed time, 426.792s cpu time, 8.984s GC time, factor 1.16)
Finished CAVA_LTL_Modelchecker (0:06:33 elapsed time, 0:08:26 cpu time, factor 1.29)
Running Flyspeck-Tame ...
Flyspeck-Tame: theory Trie
Flyspeck-Tame: theory Tries
Affine_Arithmetic: theory Affine_Arithmetic
Flyspeck-Tame: theory Arch
Flyspeck-Tame: theory IArray_Syntax
Flyspeck-Tame: theory Quasi_Order
Flyspeck-Tame: theory ListAux
Flyspeck-Tame: theory RTranCl
Flyspeck-Tame: theory PlaneGraphIso
Flyspeck-Tame: theory Worklist
Flyspeck-Tame: theory Maps
Flyspeck-Tame: theory ListSum
Flyspeck-Tame: theory Rotation
Flyspeck-Tame: theory Graph
Flyspeck-Tame: theory Enumerator
Flyspeck-Tame: theory FaceDivision
Flyspeck-Tame: theory GraphProps
Flyspeck-Tame: theory Tame
Flyspeck-Tame: theory Plane
Flyspeck-Tame: theory EnumeratorProps
Flyspeck-Tame: theory TameProps
Flyspeck-Tame: theory Plane1
Flyspeck-Tame: theory Generator
Flyspeck-Tame: theory FaceDivisionProps
Flyspeck-Tame: theory TameEnum
Flyspeck-Tame: theory Invariants
Flyspeck-Tame: theory PlaneProps
Flyspeck-Tame: theory Plane1Props
Flyspeck-Tame: theory ScoreProps
Flyspeck-Tame: theory LowerBound
Flyspeck-Tame: theory GeneratorProps
Flyspeck-Tame: theory ArchCompAux
Flyspeck-Tame: theory TameEnumProps
Flyspeck-Tame: theory ArchCompProps
Flyspeck-Tame: theory ArchComp
Flyspeck-Tame: theory Completeness
Timing Affine_Arithmetic (4 threads, 186.212s elapsed time, 706.408s cpu time, 11.876s GC time, factor 3.79)
Finished Affine_Arithmetic (0:03:12 elapsed time, 0:11:50 cpu time, factor 3.69)
Running Stream_Fusion_Code ...
Stream_Fusion_Code: theory Stream_Fusion
Stream_Fusion_Code: theory Stream_Fusion_List
Stream_Fusion_Code: theory Stream_Fusion_LList
Stream_Fusion_Code: theory Stream_Fusion_Examples
Timing Stream_Fusion_Code (4 threads, 19.994s elapsed time, 57.932s cpu time, 1.488s GC time, factor 2.90)
Finished Stream_Fusion_Code (0:00:28 elapsed time, 0:01:04 cpu time, factor 2.30)
Running Regular_Algebras ...
Regular_Algebras: theory Dioid_Power_Sum
Regular_Algebras: theory Regular_Algebras
Timing Flyspeck-Tame (4 threads, 177.692s elapsed time, 531.728s cpu time, 25.116s GC time, factor 2.99)
Finished Flyspeck-Tame (0:03:04 elapsed time, 0:08:58 cpu time, factor 2.92)
Running AVL-Trees ...
AVL-Trees: theory AVL2
AVL-Trees: theory AVL
Timing AVL-Trees (4 threads, 16.216s elapsed time, 57.744s cpu time, 0.796s GC time, factor 3.56)
Finished AVL-Trees (0:00:18 elapsed time, 0:01:00 cpu time, factor 3.21)
Running Akra_Bazzi ...
Akra_Bazzi: theory Code_Abstract_Nat
Akra_Bazzi: theory Function_Algebras
Akra_Bazzi: theory Dense_Linear_Order
Akra_Bazzi: theory Code_Target_Int
Akra_Bazzi: theory Code_Target_Nat
Akra_Bazzi: theory Multiset
Akra_Bazzi: theory Landau_Library
Akra_Bazzi: theory Code_Target_Numeral
Akra_Bazzi: theory Lattice_Algebras
Akra_Bazzi: theory Landau_Symbols_Definition
Akra_Bazzi: theory Group_Sort
Akra_Bazzi: theory Landau_Real_Products
Akra_Bazzi: theory Float
Akra_Bazzi: theory Approximation
Akra_Bazzi: theory Landau_Simprocs
Akra_Bazzi: theory Landau_Symbols
Regular_Algebras: theory Pratts_Counterexamples
Regular_Algebras: theory Regular_Algebra_Models
Regular_Algebras: theory Regular_Algebra_Variants
Timing Regular_Algebras (4 threads, 114.441s elapsed time, 185.196s cpu time, 3.456s GC time, factor 1.62)
Finished Regular_Algebras (0:02:00 elapsed time, 0:03:16 cpu time, factor 1.63)
Running AWN ...
AWN: theory TransitionSystems
AWN: theory Lib
AWN: theory AWN
AWN: theory Invariants
AWN: theory OInvariants
AWN: theory AWN_Cterms
AWN: theory AWN_SOS
AWN: theory OAWN_SOS
AWN: theory AWN_Labels
AWN: theory Inv_Cterms
AWN: theory AWN_Invariants
AWN: theory Pnet
AWN: theory AWN_SOS_Labels
AWN: theory Closed
Akra_Bazzi: theory Eval_Numeral
Akra_Bazzi: theory Akra_Bazzi_Library
AWN: theory Qmsg
Akra_Bazzi: theory Akra_Bazzi_Asymptotics
Akra_Bazzi: theory Akra_Bazzi_Real
AWN: theory OAWN_Invariants
AWN: theory OAWN_SOS_Labels
AWN: theory ONode_Lifting
AWN: theory OPnet
Akra_Bazzi: theory Akra_Bazzi
AWN: theory OPnet_Lifting
AWN: theory OClosed_Lifting
AWN: theory OClosed_Transfer
AWN: theory OAWN_Convert
AWN: theory Qmsg_Lifting
Akra_Bazzi: theory Master_Theorem
AWN: theory AWN_Main
AWN: theory Toy
Akra_Bazzi: theory Akra_Bazzi_Method
Akra_Bazzi: theory Akra_Bazzi_Approximation
Akra_Bazzi: theory Master_Theorem_Examples
Timing Akra_Bazzi (4 threads, 110.443s elapsed time, 379.572s cpu time, 9.136s GC time, factor 3.44)
Finished Akra_Bazzi (0:01:54 elapsed time, 0:06:23 cpu time, factor 3.35)
Running Collections_Examples ...
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
Timing AWN (4 threads, 91.288s elapsed time, 297.232s cpu time, 8.692s GC time, factor 3.26)
Finished AWN (0:01:33 elapsed time, 0:04:59 cpu time, factor 3.19)
Running Pi_Calculus ...
Pi_Calculus: theory Agent
Pi_Calculus: theory Early_Semantics
Pi_Calculus: theory Late_Semantics
Pi_Calculus: theory Rel
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 Strong_Early_Bisim_Subst_Pres
Pi_Calculus: theory Late_Semantics1
Pi_Calculus: theory Weak_Early_Bisim
Pi_Calculus: theory Weak_Early_Sim_Pres
Pi_Calculus: theory Late_Tau_Chain
Pi_Calculus: theory Weak_Late_Step_Semantics
Pi_Calculus: theory Weak_Early_Step_Sim
Pi_Calculus: theory Strong_Late_Sim
Pi_Calculus: theory Weak_Early_Bisim_Subst
Pi_Calculus: theory Weak_Early_Cong
Pi_Calculus: theory Weak_Early_Step_Sim_Pres
Pi_Calculus: theory Strong_Late_Bisim
Pi_Calculus: theory Weak_Early_Cong_Subst
Pi_Calculus: theory Weak_Late_Semantics
Pi_Calculus: theory Strong_Late_Sim_Pres
Pi_Calculus: theory Strong_Late_Bisim_Subst
Pi_Calculus: theory Strong_Late_Sim_SC
Pi_Calculus: theory Strong_Late_Bisim_Pres
Pi_Calculus: theory Weak_Late_Sim
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 Strong_Early_Bisim_SC
Pi_Calculus: theory Weak_Early_Bisim_SC
Pi_Calculus: theory Weak_Late_Bisim_SC
Pi_Calculus: theory Weak_Early_Bisim_Pres
Pi_Calculus: theory Weak_Late_Bisim_Subst
Pi_Calculus: theory Weak_Late_Sim_Pres
Pi_Calculus: theory Weak_Late_Step_Sim
Pi_Calculus: theory Weak_Early_Cong_Pres
Pi_Calculus: theory Weak_Late_Bisim_Pres
Pi_Calculus: theory Weak_Early_Cong_Subst_Pres
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
Collections_Examples: theory Collection_Autoref_Examples
Collections_Examples: theory Collection_Examples
Timing Collections_Examples (4 threads, 104.925s elapsed time, 276.532s cpu time, 8.428s GC time, factor 2.64)
Finished Collections_Examples (0:01:55 elapsed time, 0:04:52 cpu time, factor 2.54)
Running Abortable_Linearizable_Modules ...
Abortable_Linearizable_Modules: theory Sequences
Abortable_Linearizable_Modules: theory IOA
Abortable_Linearizable_Modules: theory RDR
Abortable_Linearizable_Modules: theory Consensus
Timing Pi_Calculus (4 threads, 102.023s elapsed time, 363.616s cpu time, 7.784s GC time, factor 3.56)
Finished Pi_Calculus (0:01:44 elapsed time, 0:06:06 cpu time, factor 3.50)
Running Sort_Encodings ...
Abortable_Linearizable_Modules: theory Simulations
Abortable_Linearizable_Modules: theory SLin
Sort_Encodings: theory Infinite_Set
Sort_Encodings: theory Nat_Bijection
Sort_Encodings: theory Old_Datatype
Sort_Encodings: theory Countable
Sort_Encodings: theory Countable_Set
Sort_Encodings: theory Countable_Set_Type
Sort_Encodings: theory Preliminaries
Abortable_Linearizable_Modules: theory Idempotence
Sort_Encodings: theory Sig
Sort_Encodings: theory TermsAndClauses
Sort_Encodings: theory M
Sort_Encodings: theory U
Sort_Encodings: theory CU
Sort_Encodings: theory CM
Sort_Encodings: theory Mono
Sort_Encodings: theory Mcalc
Sort_Encodings: theory E
Sort_Encodings: theory Mcalc2
Sort_Encodings: theory Mcalc2C
Sort_Encodings: theory T_G_Prelim
Sort_Encodings: theory T
Sort_Encodings: theory G
Timing Abortable_Linearizable_Modules (4 threads, 78.492s elapsed time, 161.216s cpu time, 4.204s GC time, factor 2.05)
Finished Abortable_Linearizable_Modules (0:01:21 elapsed time, 0:02:43 cpu time, factor 2.02)
Running Abstract-Hoare-Logics ...
Sort_Encodings: theory Encodings
Abstract-Hoare-Logics: theory Lang
Abstract-Hoare-Logics: theory PLang
Abstract-Hoare-Logics: theory PsLang
Timing Sort_Encodings (4 threads, 62.416s elapsed time, 151.720s cpu time, 8.368s GC time, factor 2.43)
Finished Sort_Encodings (0:01:05 elapsed time, 0:02:34 cpu time, factor 2.35)
Running Amortized_Complexity ...
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
Amortized_Complexity: theory List_Index
Amortized_Complexity: theory Tree
Timing Abstract-Hoare-Logics (4 threads, 11.785s elapsed time, 37.784s cpu time, 1.748s GC time, factor 3.21)
Finished Abstract-Hoare-Logics (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.80)
Running ArrowImpossibilityGS ...
Amortized_Complexity: theory Tree_Multiset
Amortized_Complexity: theory Splay_Tree
Amortized_Complexity: theory Skew_Heap
ArrowImpossibilityGS: theory Arrow_Order
ArrowImpossibilityGS: theory Arrow_Utility
ArrowImpossibilityGS: theory GS
Timing ArrowImpossibilityGS (4 threads, 5.792s elapsed time, 18.552s cpu time, 0.500s GC time, factor 3.20)
Finished ArrowImpossibilityGS (0:00:11 elapsed time, 0:00:23 cpu time, factor 2.12)
Running BytecodeLogicJmlTypes ...
BytecodeLogicJmlTypes: theory AssocLists
BytecodeLogicJmlTypes: theory Language
BytecodeLogicJmlTypes: theory Logic
BytecodeLogicJmlTypes: theory MultiStep
BytecodeLogicJmlTypes: theory Reachability
BytecodeLogicJmlTypes: theory Cachera
BytecodeLogicJmlTypes: theory Sound
Amortized_Complexity FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/Amortized_Complexity)
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
### Metis: Unused theorems: "Tree.tree.exhaust", "Orderings.linorder_class.le_less_linear", "Orderings.linorder_class.less_linear"
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Running BDD ...
BDD: theory BinDag
BDD: theory General
BDD: theory ProcedureSpecs
BDD: theory EvalProof
BDD: theory RepointProof
BDD: theory LevellistProof
BDD: theory ShareRepProof
BDD: theory ShareReduceRepListProof
BDD: theory NormalizeTotalProof
Timing BytecodeLogicJmlTypes (4 threads, 79.176s elapsed time, 232.140s cpu time, 3.616s GC time, factor 2.93)
Finished BytecodeLogicJmlTypes (0:01:21 elapsed time, 0:03:54 cpu time, factor 2.87)
Running Call_Arity ...
Call_Arity: theory BalancedTraces
Call_Arity: theory ConstOn
Call_Arity: theory List-Interleavings
Call_Arity: theory Arity
Call_Arity: theory AList-Utils-HOLCF
Call_Arity: theory Cardinality-Domain
Call_Arity: theory Set-Cpo
Call_Arity: theory Arity-Nominal
Call_Arity: theory AEnv
Call_Arity: theory AnalBinds
Call_Arity: theory Env-Set-Cpo
Call_Arity: theory Cardinality-Domain-Lists
Call_Arity: theory CoCallGraph
Call_Arity: theory ArityAnalysisSig
Call_Arity: theory EtaExpansion
Call_Arity: theory SestoftConf
Call_Arity: theory ArityAnalysisAbinds
Call_Arity: theory TransformTools
Call_Arity: theory ArityAnalysisSpec
Call_Arity: theory TrivialArityAnal
Call_Arity: theory CoCallGraph-Nominal
Call_Arity: theory CoCallAnalysisSig
Call_Arity: theory ArityAnalysisFix
Call_Arity: theory ArityAnalysisFixProps
Call_Arity: theory AbstractTransform
Call_Arity: theory ArityEtaExpansion
Call_Arity: theory ArityAnalysisStack
Call_Arity: theory CoCallAnalysisBinds
Call_Arity: theory CoCallAritySig
Call_Arity: theory ArityStack
Call_Arity: theory CoCallAnalysisSpec
Call_Arity: theory CardinalityAnalysisSig
Call_Arity: theory Sestoft
Call_Arity: theory CoCallFix
Call_Arity: theory CardinalityAnalysisSpec
Call_Arity: theory ArityConsistent
Call_Arity: theory EtaExpansionSafe
Timing BDD (4 threads, 68.860s elapsed time, 254.620s cpu time, 3.340s GC time, factor 3.70)
Finished BDD (0:01:17 elapsed time, 0:04:18 cpu time, factor 3.35)
Running AutoFocus-Stream ...
Call_Arity: theory SestoftCorrect
Call_Arity: theory NoCardinalityAnalysis
Call_Arity: theory CoCallAnalysisImpl
Call_Arity: theory SestoftGC
Call_Arity: theory ArityEtaExpansionSafe
Call_Arity: theory TTree
Call_Arity: theory ArityTransform
Call_Arity: theory TTree-HOLCF
Call_Arity: theory CoCallImplSafe
Call_Arity: theory ArityAnalysisCorrDenotational
Call_Arity: theory CallArityEnd2End
Call_Arity: theory ArityTransformSafe
Call_Arity: theory CardArityTransformSafe
Call_Arity: theory CoCallGraph-TTree
Call_Arity: theory TTreeAnalysisSig
AutoFocus-Stream: theory ListSlice
Call_Arity: theory CoCallImplTTree
AutoFocus-Stream: theory AF_Stream
Call_Arity: theory TTreeAnalysisSpec
Call_Arity: theory TTreeImplCardinality
Call_Arity: theory CoCallImplTTreeSafe
Call_Arity: theory TTreeImplCardinalitySafe
Call_Arity: theory CallArityEnd2EndSafe
AutoFocus-Stream: theory AF_Stream_Exec
AutoFocus-Stream: theory IL_AF_Stream
AutoFocus-Stream: theory IL_AF_Stream_Exec
Timing AutoFocus-Stream (4 threads, 51.351s elapsed time, 164.084s cpu time, 1.628s GC time, factor 3.20)
Finished AutoFocus-Stream (0:00:58 elapsed time, 0:02:50 cpu time, factor 2.91)
Running BinarySearchTree ...
Timing Call_Arity (4 threads, 71.376s elapsed time, 251.668s cpu time, 6.392s GC time, factor 3.53)
Finished Call_Arity (0:01:22 elapsed time, 0:04:15 cpu time, factor 3.09)
Running Binomial-Heaps ...
BinarySearchTree: theory BinaryTree
BinarySearchTree: theory BinaryTree_TacticStyle
BinarySearchTree: theory BinaryTree_Map
Binomial-Heaps: theory BinomialHeap
Binomial-Heaps: theory SkewBinomialHeap
Timing BinarySearchTree (4 threads, 4.863s elapsed time, 16.892s cpu time, 0.308s GC time, factor 3.47)
Finished BinarySearchTree (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.68)
Running Binomial-Queues ...
Binomial-Queues: theory PQ
Binomial-Queues: theory Binomial_Queue
Binomial-Queues: theory PQ_Implementation
Timing Binomial-Queues (4 threads, 8.478s elapsed time, 22.348s cpu time, 0.420s GC time, factor 2.64)
Finished Binomial-Queues (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.28)
Running Bondy ...
Bondy: theory Bondy
Timing Bondy (4 threads, 1.518s elapsed time, 3.136s cpu time, 0.000s GC time, factor 2.07)
Finished Bondy (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.42)
Running Boolean_Expression_Checkers ...
Binomial-Heaps: theory Test
Timing Binomial-Heaps (4 threads, 20.339s elapsed time, 60.876s cpu time, 3.280s GC time, factor 2.99)
Finished Binomial-Heaps (0:00:26 elapsed time, 0:01:06 cpu time, factor 2.55)
Running Bounded_Deducibility_Security ...
Boolean_Expression_Checkers: theory Boolean_Expression_Checkers
Bounded_Deducibility_Security: theory Trivia
Bounded_Deducibility_Security: theory IO_Automaton
Bounded_Deducibility_Security: theory BD_Security
Bounded_Deducibility_Security: theory Compositional_Reasoning
Bounded_Deducibility_Security: theory Bounded_Deducibility_Security
Boolean_Expression_Checkers: theory Boolean_Expression_Checkers_AList_Mapping
Boolean_Expression_Checkers: theory Boolean_Expression_Example
Timing Bounded_Deducibility_Security (4 threads, 6.970s elapsed time, 18.580s cpu time, 0.312s GC time, factor 2.67)
Finished Bounded_Deducibility_Security (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.23)
Running CCS ...
CCS: theory Agent
CCS: theory Strong_Sim
CCS: theory Struct_Cong
CCS: theory Tau_Chain
CCS: theory Strong_Bisim
CCS: theory Strong_Sim_Pres
CCS: theory Strong_Sim_SC
CCS: theory Weak_Cong_Semantics
CCS: theory Strong_Bisim_Pres
CCS: theory Weak_Semantics
CCS: theory Strong_Bisim_SC
CCS: theory Weak_Sim
CCS: theory Weak_Cong_Sim
CCS: theory Weak_Sim_Pres
CCS: theory Weak_Bisim
CCS: theory Weak_Cong_Sim_Pres
CCS: theory Weak_Cong
CCS: theory Weak_Bisim_Pres
CCS: theory Weak_Cong_Pres
Timing Boolean_Expression_Checkers (4 threads, 24.975s elapsed time, 44.496s 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)
Running CISC-Kernel ...
CISC-Kernel: theory List_Theorems
CISC-Kernel: theory Option_Binders
CISC-Kernel: theory Step_configuration
CISC-Kernel: theory K
CISC-Kernel: theory Step_policies
CISC-Kernel: theory SK
CISC-Kernel: theory Step
CISC-Kernel: theory ISK
CISC-Kernel: theory CISK
Timing CCS (4 threads, 22.013s elapsed time, 63.732s cpu time, 0.972s GC time, factor 2.90)
Finished CCS (0:00:24 elapsed time, 0:01:06 cpu time, factor 2.70)
Running Card_Number_Partitions ...
CISC-Kernel: theory Step_invariants
Card_Number_Partitions: theory Additions_to_Main
CISC-Kernel: theory Step_vpeq
Card_Number_Partitions: theory Number_Partition
CISC-Kernel: theory Step_vpeq_locally_respects
CISC-Kernel: theory Step_vpeq_weakly_step_consistent
Card_Number_Partitions: theory Card_Number_Partitions
CISC-Kernel: theory Separation_kernel_model
CISC-Kernel: theory Link_separation_kernel_model_to_CISK
Timing Card_Number_Partitions (4 threads, 5.317s elapsed time, 17.892s cpu time, 0.120s GC time, factor 3.37)
Finished Card_Number_Partitions (0:00:07 elapsed time, 0:00:20 cpu time, factor 2.64)
Running Card_Partitions ...
Card_Partitions: theory Card_Partitions
Timing CISC-Kernel (4 threads, 22.421s elapsed time, 75.132s cpu time, 2.396s GC time, factor 3.35)
Finished CISC-Kernel (0:00:25 elapsed time, 0:01:17 cpu time, factor 3.09)
Running Category ...
Timing Card_Partitions (4 threads, 8.164s elapsed time, 25.528s cpu time, 0.068s GC time, factor 3.13)
Finished Card_Partitions (0:00:10 elapsed time, 0:00:27 cpu time, factor 2.58)
Running Category2 ...
Category: theory Cat
Category: theory Functors
Category: theory SetCat
Category: theory NatTrans
Category: theory HomFunctors
Category2: theory LProd
Category2: theory HOLZF
Category: theory Yoneda
Category2: theory Zet
Category2: theory MainZF
Timing Category (4 threads, 5.072s elapsed time, 14.660s cpu time, 0.476s GC time, factor 2.89)
Finished Category (0:00:10 elapsed time, 0:00:20 cpu time, factor 1.90)
Running Cayley_Hamilton ...
Category2: theory Universe
Category2: theory Category
Category2: theory Functors
Category2: theory MonadicEquationalTheory
Category2: theory NatTrans
Category2: theory SetCat
Cayley_Hamilton: theory More_List
Cayley_Hamilton: theory Polynomial
Category2: theory Yoneda
Cayley_Hamilton: theory Square_Matrix
Cayley_Hamilton: theory Cayley_Hamilton
Timing Cayley_Hamilton (4 threads, 15.653s elapsed time, 49.132s cpu time, 0.824s GC time, factor 3.14)
Finished Cayley_Hamilton (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.69)
Running Certification_Monads ...
Timing Category2 (4 threads, 23.527s elapsed time, 79.796s cpu time, 2.996s GC time, factor 3.39)
Finished Category2 (0:00:29 elapsed time, 0:01:25 cpu time, factor 2.92)
Running Circus ...
Certification_Monads: theory Adhoc_Overloading
Certification_Monads: theory Derive_Manager
Certification_Monads: theory Generator_Aux
Certification_Monads: theory Partial_Function_MR
Certification_Monads: theory Monad_Syntax
Certification_Monads: theory Show
Circus: theory Sublist
Certification_Monads: theory Error_Syntax
Certification_Monads: theory Error_Monad
Certification_Monads: theory Strict_Sum
Circus: theory Var
Circus: theory Var_list
Circus: theory Relations
Certification_Monads: theory Check_Monad
Certification_Monads: theory Parser_Monad
Circus: theory Designs
Circus: theory Reactive_Processes
Timing Certification_Monads (4 threads, 6.654s elapsed time, 17.448s cpu time, 0.260s GC time, factor 2.62)
Finished Certification_Monads (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.21)
Running ClockSynchInst ...
ClockSynchInst: theory ICAInstance
ClockSynchInst: theory LynchInstance
Circus: theory CSP_Processes
Circus: theory Circus_Actions
Circus: theory Denotational_Semantics
Timing ClockSynchInst (4 threads, 6.026s elapsed time, 22.076s cpu time, 0.156s GC time, factor 3.66)
Finished ClockSynchInst (0:00:08 elapsed time, 0:00:24 cpu time, factor 2.94)
Running CofGroups ...
CofGroups: theory CofGroups
Timing CofGroups (4 threads, 2.242s elapsed time, 6.852s cpu time, 0.000s GC time, factor 3.06)
Finished CofGroups (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.58)
Running Compiling-Exceptions-Correctly ...
Compiling-Exceptions-Correctly: theory Exceptions
Circus: theory Circus_Syntax
Circus: theory Refinement
Timing Compiling-Exceptions-Correctly (4 threads, 6.081s elapsed time, 10.268s cpu time, 0.404s GC time, factor 1.69)
Finished Compiling-Exceptions-Correctly (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.49)
Running Completeness ...
Circus: theory Refinement_Example
Completeness: theory Multiset
Completeness: theory Permutation
Completeness: theory PermutationLemmas
Completeness: theory Tree
Completeness: theory Base
Completeness: theory Formula
Completeness: theory Sequents
Timing Circus (4 threads, 46.708s elapsed time, 145.016s cpu time, 3.064s GC time, factor 3.10)
Finished Circus (0:00:49 elapsed time, 0:02:27 cpu time, factor 2.97)
Running Formal_SSA ...
Completeness: theory Completeness
Completeness: theory Soundness
Timing Completeness (4 threads, 17.676s elapsed time, 52.112s cpu time, 1.360s GC time, factor 2.95)
Finished Completeness (0:00:20 elapsed time, 0:00:54 cpu time, factor 2.71)
Running Ordinary_Differential_Equations ...
Ordinary_Differential_Equations: theory Code_Abstract_Nat
Ordinary_Differential_Equations: theory Adhoc_Overloading
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 Code_Target_Numeral
Ordinary_Differential_Equations: theory Quotient_Set
Ordinary_Differential_Equations: theory Lattice_Algebras
Ordinary_Differential_Equations: theory Counterclockwise
Ordinary_Differential_Equations: theory Counterclockwise_Vector
Formal_SSA: theory AuxLemmas
Formal_SSA: theory Char_ord
Formal_SSA: theory Com
Formal_SSA: theory Graph
Formal_SSA: theory BasicDefs
Formal_SSA: theory List_lexord
Ordinary_Differential_Equations: theory Counterclockwise_2D_Strict
Formal_SSA: theory Mapping
Ordinary_Differential_Equations: theory Euclidean_Space_Explicit
Ordinary_Differential_Equations: theory Counterclockwise_2D_Arbitrary
Formal_SSA: theory RBT_Set
Ordinary_Differential_Equations: theory Polygon
Formal_SSA: theory RBT_Mapping
Ordinary_Differential_Equations: theory While_Combinator
Formal_SSA: theory CFG
Formal_SSA: theory Sublist
Formal_SSA: theory CFGExit
Formal_SSA: theory Postdomination
Formal_SSA: theory CFG_wf
Formal_SSA: theory Distance
Formal_SSA: theory DynStandardControlDependence
Formal_SSA: theory DynWeakControlDependence
Formal_SSA: theory CFGExit_wf
Formal_SSA: theory StandardControlDependence
Formal_SSA: theory WeakControlDependence
Formal_SSA: theory DynDataDependence
Formal_SSA: theory Observable
Formal_SSA: theory SemanticsCFG
Formal_SSA: theory DataDependence
Formal_SSA: theory GraphSpec
Formal_SSA: theory PDG
Formal_SSA: theory Slice
Ordinary_Differential_Equations: theory Permutation
Ordinary_Differential_Equations: theory Affine_Form
Formal_SSA: theory WeakOrderDependence
Formal_SSA: theory Labels
Formal_SSA: theory WCFG
Ordinary_Differential_Equations: theory Float
Formal_SSA: theory CDepInstantiations
Formal_SSA: theory Interpretation
Formal_SSA: theory WellFormed
Ordinary_Differential_Equations: theory Approximation
Formal_SSA: theory AdditionalLemmas
Ordinary_Differential_Equations: theory Float_Real
Ordinary_Differential_Equations: theory Executable_Euclidean_Space
Ordinary_Differential_Equations: theory Affine_Approximation
Ordinary_Differential_Equations: theory Affine_Code
Ordinary_Differential_Equations: theory Ex_Affine_Approximation
Ordinary_Differential_Equations: theory Ex_Ineqs
Ordinary_Differential_Equations: theory Intersection
Ordinary_Differential_Equations: theory Ex_Inter
Formal_SSA: theory Disjoin_Transform
Formal_SSA: theory FormalSSA_Misc
Formal_SSA: theory Serial_Rel
Formal_SSA: theory While_Combinator_Exts
Formal_SSA: theory Mapping_Exts
Formal_SSA: theory Graph_path
Formal_SSA: theory RBT_Mapping_Exts
Formal_SSA: theory SSA_CFG
Formal_SSA: theory Construct_SSA
Formal_SSA: theory Minimality
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
Formal_SSA: theory Generic_Extract
Formal_SSA: theory WhileGraphSSA
Ordinary_Differential_Equations: theory Affine_Arithmetic
Ordinary_Differential_Equations: theory Optimize_Integer
Ordinary_Differential_Equations: theory ODE_Auxiliarities
Ordinary_Differential_Equations: theory Print
Ordinary_Differential_Equations: theory Higher_Derivative
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 Runge_Kutta
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 Examples
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations
Timing Ordinary_Differential_Equations (4 threads, 342.232s elapsed time, 1219.676s cpu time, 27.956s GC time, factor 3.56)
Finished Ordinary_Differential_Equations (0:05:46 elapsed time, 0:20:23 cpu time, factor 3.53)
Running Native_Word ...
Native_Word: theory Code_Test
Native_Word: theory Char_ord
Native_Word: theory Code_Target_Int
Native_Word: theory Code_Char
Native_Word: theory More_Bits_Int
Native_Word: theory Bits_Integer
Native_Word: theory Word_Misc
Native_Word: theory Code_Target_Bits_Int
Native_Word: theory Uint
Native_Word: theory Uint16
Native_Word: theory Uint32
Native_Word: theory Uint8
Native_Word: theory Native_Cast
Native_Word: theory Native_Word_Test
Timing Formal_SSA (4 threads, 404.076s elapsed time, 964.848s cpu time, 15.160s GC time, factor 2.39)
Finished Formal_SSA (0:06:54 elapsed time, 0:16:15 cpu time, factor 2.35)
Running QR_Decomposition ...
QR_Decomposition: theory Bit
QR_Decomposition: theory Char_ord
QR_Decomposition: theory Derive_Manager
QR_Decomposition: theory Code_Abstract_Nat
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 Cong
QR_Decomposition: theory Code_Set
QR_Decomposition: theory Show
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
QR_Decomposition: theory NthRoot_Impl
QR_Decomposition: theory Miscellaneous
QR_Decomposition: theory UniqueFactorization
QR_Decomposition: theory Sqrt_Babylonian
QR_Decomposition: theory Real_Impl_Auxiliary
QR_Decomposition: theory Prime_Product
QR_Decomposition: theory Real_Impl
QR_Decomposition: theory Code_Matrix
QR_Decomposition: theory Fundamental_Subspaces
QR_Decomposition: theory Rref
QR_Decomposition: theory Dim_Formula
QR_Decomposition: theory Elementary_Operations
QR_Decomposition: theory Real_Unique_Impl
QR_Decomposition: theory Rank
QR_Decomposition: theory Gauss_Jordan
QR_Decomposition: theory Linear_Maps
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
Native_Word: theory Native_Word_Test_Emu
Native_Word: theory Native_Word_Test_GHC
QR_Decomposition: theory IArray_Addenda_QR
QR_Decomposition: theory Generalizations2
QR_Decomposition: theory Miscellaneous_QR
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
Native_Word: theory Native_Word_Test_MLton2
Native_Word: theory Native_Word_Test_MLton
QR_Decomposition: theory Examples_QR_IArrays_Symbolic
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
Native_Word: theory Native_Word_Test_SMLNJ2
Native_Word: theory Native_Word_Test_SMLNJ
Native_Word: theory Uint_Userguide
Timing Native_Word (4 threads, 270.325s elapsed time, 258.260s cpu time, 6.492s GC time, factor 0.96)
Finished Native_Word (0:04:33 elapsed time, 0:11:54 cpu time, factor 2.61)
Running Promela ...
Promela: theory IArray
Promela: theory PromelaStatistics
Promela: theory Lexord_List
Promela: theory PromelaAST
Timing QR_Decomposition (4 threads, 250.690s elapsed time, 915.244s cpu time, 16.760s GC time, factor 3.65)
Finished QR_Decomposition (0:04:14 elapsed time, 0:15:19 cpu time, factor 3.61)
Running Encodability_Process_Calculi ...
Promela: theory PromelaDatastructures
Encodability_Process_Calculi: theory LaTeXsugar
Encodability_Process_Calculi: theory OptionalSugar
Encodability_Process_Calculi: theory Relations
Encodability_Process_Calculi: theory ProcessCalculi
Encodability_Process_Calculi: theory Encodings
Encodability_Process_Calculi: theory SimulationRelations
Encodability_Process_Calculi: theory SourceTargetRelation
Encodability_Process_Calculi: theory DivergenceReflection
Encodability_Process_Calculi: theory FullAbstraction
Encodability_Process_Calculi: theory OperationalCorrespondence
Encodability_Process_Calculi: theory SuccessSensitiveness
Promela: theory PromelaInvariants
Promela: theory Promela
Encodability_Process_Calculi: theory CombinedCriteria
Promela: theory PromelaLTL
Promela: theory PromelaLTLConv
Promela: theory All_Of_Promela
Timing Promela (4 threads, 245.958s elapsed time, 430.968s cpu time, 15.300s GC time, factor 1.75)
Finished Promela (0:04:18 elapsed time, 0:07:35 cpu time, factor 1.76)
Running Jordan_Normal_Form ...
Jordan_Normal_Form: theory Missing_Ring
Jordan_Normal_Form: theory Missing_Permutations
Timing Encodability_Process_Calculi (4 threads, 225.991s elapsed time, 482.824s cpu time, 9.428s GC time, factor 2.14)
Finished Encodability_Process_Calculi (0:03:48 elapsed time, 0:08:05 cpu time, factor 2.12)
Running Network_Security_Policy_Verification ...
Jordan_Normal_Form: theory Conjugate
Jordan_Normal_Form: theory Missing_VectorSpace
Jordan_Normal_Form: theory Show_Arctic
Jordan_Normal_Form: theory Derivation_Bound
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
Network_Security_Policy_Verification: theory FiniteGraph
Network_Security_Policy_Verification: theory Char_ord
Network_Security_Policy_Verification: theory List_lexord
Network_Security_Policy_Verification: theory ML_GraphViz_Config
Jordan_Normal_Form: theory Gauss_Jordan_IArray_Impl
Network_Security_Policy_Verification: theory ML_GraphViz
Network_Security_Policy_Verification: theory ML_GraphViz_Disable
Network_Security_Policy_Verification: theory Code_Char
Network_Security_Policy_Verification: theory Orders
Network_Security_Policy_Verification: theory TopoS_Util
Jordan_Normal_Form: theory Determinant
Network_Security_Policy_Verification: theory Transitive_Closure_Impl
Network_Security_Policy_Verification: theory Efficient_Distinct
Jordan_Normal_Form: theory Strassen_Algorithm_Code
Jordan_Normal_Form: theory Ring_Hom_Matrix
Network_Security_Policy_Verification: theory Transitive_Closure_List_Impl
Network_Security_Policy_Verification: theory Bounds
Network_Security_Policy_Verification: theory FiniteListGraph
Network_Security_Policy_Verification: theory Lattice
Jordan_Normal_Form: theory Char_Poly
Jordan_Normal_Form: theory Determinant_Impl
Network_Security_Policy_Verification: theory CompleteLattice
Network_Security_Policy_Verification: theory FiniteListGraph_Impl
Jordan_Normal_Form: theory Complexity_Carrier
Jordan_Normal_Form: theory Jordan_Normal_Form
Jordan_Normal_Form: theory Gram_Schmidt
Jordan_Normal_Form: theory Schur_Decomposition
Jordan_Normal_Form: theory Matrix_Complexity
Network_Security_Policy_Verification: theory TopoS_Vertices
Network_Security_Policy_Verification: theory TopoS_Interface
Network_Security_Policy_Verification: theory vertex_example_simps
Jordan_Normal_Form: theory Jordan_Normal_Form_Existence
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
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
Jordan_Normal_Form: theory Matrix_Impl
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
Network_Security_Policy_Verification: theory SINVAR_BLPtrusted_impl
Network_Security_Policy_Verification: theory SINVAR_CommunicationPartners_impl
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
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
Network_Security_Policy_Verification: theory TopoS_Composition_Theory_impl
Network_Security_Policy_Verification: theory TopoS_Library
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
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
Timing Jordan_Normal_Form (4 threads, 213.833s elapsed time, 804.416s cpu time, 9.776s GC time, factor 3.76)
Finished Jordan_Normal_Form (0:03:44 elapsed time, 0:13:31 cpu time, factor 3.62)
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
Probabilistic_System_Zoo-BNFs: theory Wellorder_Embedding
Timing Network_Security_Policy_Verification (4 threads, 202.265s elapsed time, 724.604s cpu time, 20.208s GC time, factor 3.58)
Finished Network_Security_Policy_Verification (0:03:32 elapsed time, 0:12:14 cpu time, factor 3.46)
Running Containers-Benchmarks ...
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
Containers-Benchmarks: theory Trie
Containers-Benchmarks: theory FingerTree
Containers-Benchmarks: theory Benchmark_Comparison
Containers-Benchmarks: theory Foldi
Containers-Benchmarks: theory ICF_Tools
Containers-Benchmarks: theory BinomialHeap
Probabilistic_System_Zoo-BNFs: theory Bochner_Integration
Containers-Benchmarks: theory Benchmark_Default
Containers-Benchmarks: theory List_More
Containers-Benchmarks: theory Quicksort
Containers-Benchmarks: theory Ord_Code_Preproc
Probabilistic_System_Zoo-BNFs: theory Radon_Nikodym
Probabilistic_System_Zoo-BNFs: theory Lebesgue_Measure
Containers-Benchmarks: theory Locale_Code
Containers-Benchmarks: theory Prio_List
Containers-Benchmarks: theory Benchmark_RBT
Containers-Benchmarks: theory Misc
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
Containers-Benchmarks: theory Benchmark_Bool
Containers-Benchmarks: theory Benchmark_LC
Containers-Benchmarks: theory Clauses
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
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 Assoc_List
Containers-Benchmarks: theory Param_Tool
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 SetIteratorGA
Containers-Benchmarks: theory Parametricity
Containers-Benchmarks: theory Autoref_Id_Ops
Containers-Benchmarks: theory Diff_Array
Containers-Benchmarks: theory It_to_It
Containers-Benchmarks: theory Autoref_Fix_Rel
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
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, 189.957s elapsed time, 709.128s cpu time, 11.444s GC time, factor 3.73)
Finished Probabilistic_System_Zoo-BNFs (0:03:14 elapsed time, 0:11:53 cpu time, factor 3.67)
Running Gabow_SCC ...
Gabow_SCC: theory Gabow_Skeleton
Gabow_SCC: theory Find_Path
Gabow_SCC: theory Find_Path_Impl
Timing Containers-Benchmarks (4 threads, 188.721s elapsed time, 599.760s cpu time, 38.020s GC time, factor 3.18)
Finished Containers-Benchmarks (0:03:25 elapsed time, 0:10:10 cpu time, factor 2.97)
Running List_Update ...
Gabow_SCC: theory Gabow_SCC
Gabow_SCC: theory Gabow_GBG
Gabow_SCC: theory Gabow_Skeleton_Code
List_Update: theory List_Index
List_Update: theory While_Combinator
List_Update: theory Regular_Set
List_Update: theory Regular_Exp
List_Update: theory NDerivative
List_Update: theory Equivalence_Checking
List_Update FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/List_Update)
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
### Rule already declared as elimination (elim)
### \<lbrakk>?w \<in> ?A @@ ?B;
###  \<And>u v.
###     \<lbrakk>u \<in> ?A; v \<in> ?B; ?w = u @ v\<rbrakk>
###     \<Longrightarrow> ?thesis\<rbrakk>
### \<Longrightarrow> ?thesis
### theory "Regular_Set"
### 5.477s elapsed time, 10.952s cpu time, 0.312s GC time
Loading theory "Regular_Exp" (required by "Equivalence_Checking" via "NDerivative")
instantiation
  rexp :: (order) order
  less_eq_rexp == less_eq ::
    'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool
  less_rexp == less :: 'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
instantiation
  rexp :: (linorder) linorder
### theory "Regular_Exp"
### 6.635s elapsed time, 19.960s cpu time, 0.580s GC time
Loading theory "NDerivative" (required by "Equivalence_Checking")
Found termination order:
  "(\<lambda>p. size (fst p)) <*mlex*>
   (\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
### theory "NDerivative"
### 4.565s elapsed time, 8.288s cpu time, 0.000s GC time
Loading theory "Equivalence_Checking"
Proofs for coinductive predicate(s) "bisimilar"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the simplification rules ...
### theory "Equivalence_Checking"
### 0.409s elapsed time, 1.160s cpu time, 0.000s GC time
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Running Probabilistic_Noninterference ...
Probabilistic_Noninterference: theory Lattice_Syntax
Probabilistic_Noninterference: theory Rewrite
Probabilistic_Noninterference: theory Simps_Case_Conv
Probabilistic_Noninterference: theory Prefix_Order
Probabilistic_Noninterference: theory Complete_Partial_Order2
Probabilistic_Noninterference: theory Coinductive_Nat
Probabilistic_Noninterference: theory Coinductive_List
Gabow_SCC: theory Gabow_GBG_Code
Gabow_SCC: theory Gabow_SCC_Code
Probabilistic_Noninterference: theory Coinductive_Stream
Probabilistic_Noninterference: theory Discrete_Time_Markov_Chain
Probabilistic_Noninterference: theory Interface
Probabilistic_Noninterference: theory Language_Semantics
Probabilistic_Noninterference: theory Resumption_Based
Probabilistic_Noninterference: theory Compositionality
Probabilistic_Noninterference: theory Trace_Based
Probabilistic_Noninterference: theory Syntactic_Criteria
Probabilistic_Noninterference: theory Concrete
Gabow_SCC: theory All_Of_Gabow_SCC
Timing Gabow_SCC (4 threads, 159.758s elapsed time, 406.064s cpu time, 8.796s GC time, factor 2.54)
Finished Gabow_SCC (0:02:51 elapsed time, 0:07:18 cpu time, factor 2.56)
Running Planarity_Certificates ...
Planarity_Certificates: theory Permutations
Planarity_Certificates: theory Eisbach
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 NonDetMonadLemmas
Planarity_Certificates: theory Liminf_Limsup
Planarity_Certificates: theory Transitive_Closure_Impl
Planarity_Certificates: theory OptionMonadND
Planarity_Certificates: theory WP
Planarity_Certificates: theory OptionMonadWP
Planarity_Certificates: theory Countable
Planarity_Certificates: theory Countable_Set
Planarity_Certificates: theory Countable_Complete_Lattices
Planarity_Certificates: theory Order_Continuity
Planarity_Certificates: theory Extended_Nat
Planarity_Certificates: theory Extended_Real
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
Timing Probabilistic_Noninterference (4 threads, 157.735s elapsed time, 568.864s cpu time, 8.640s GC time, factor 3.61)
Finished Probabilistic_Noninterference (0:02:43 elapsed time, 0:09:45 cpu time, factor 3.58)
Running Featherweight_OCL ...
Featherweight_OCL: theory UML_Types
Planarity_Certificates: theory Digraph_Component
Featherweight_OCL: theory UML_Logic
Featherweight_OCL: theory UML_PropertyProfiles
Featherweight_OCL: theory UML_Tools
Featherweight_OCL: theory UML_Boolean
Featherweight_OCL: theory UML_Integer
Featherweight_OCL: theory UML_Pair
Planarity_Certificates: theory Digraph_Component_Vwalk
Planarity_Certificates: theory Digraph_Isomorphism
Planarity_Certificates: theory Subdivision
Planarity_Certificates: theory Kuratowski
Planarity_Certificates: theory Euler
Featherweight_OCL: theory UML_Real
Featherweight_OCL: theory UML_String
Planarity_Certificates: theory Graph_Theory
Featherweight_OCL: theory UML_Sequence
Featherweight_OCL: theory UML_Void
Featherweight_OCL: theory UML_Bag
Featherweight_OCL: theory UML_Set
Featherweight_OCL: theory UML_Library
Planarity_Certificates FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/Planarity_Certificates)
### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
"LEAST x. P x"
  :: "'a"
### Rule already declared as elimination (elim)
### \<lbrakk>vwalk ?p ?G;
###  \<lbrakk>set ?p \<subseteq> verts ?G;
###   set (vwalk_arcs ?p) \<subseteq> arcs_ends ?G \<and>
###   ?p \<noteq> []\<rbrakk>
###  \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
### Rule already declared as elimination (elim)
### \<lbrakk>subgraph ?H ?G;
###  \<lbrakk>verts ?H \<subseteq> verts ?G; arcs ?H \<subseteq> arcs ?G;
###   compatible ?G ?H; wf_digraph ?H; wf_digraph ?G\<rbrakk>
###  \<Longrightarrow> ?thesis\<rbrakk>
### \<Longrightarrow> ?thesis
### Rule already declared as elimination (elim)
### \<lbrakk>vpath ?p ?G;
###  \<lbrakk>vwalk ?p ?G; distinct ?p\<rbrakk> \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
"True"
  :: "bool"
"- \<infinity>"
  :: "ereal"
"True"
  :: "bool"
"\<infinity>"
  :: "ereal"
"ereal (13 / 4)"
  :: "ereal"
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Running Markov_Models ...
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 IArray
Markov_Models: theory Code_Target_Numeral
Markov_Models: theory Quotient_Syntax
Markov_Models: theory Rewrite
Markov_Models: theory Quotient_Option
Markov_Models: theory Quotient_Product
Markov_Models: theory Quotient_Set
Markov_Models: theory Quotient_List
Markov_Models: theory Quotient_Sum
Markov_Models: theory Simps_Case_Conv
Markov_Models: theory Prefix_Order
Markov_Models: theory While_Combinator
Markov_Models: theory Coinductive_Nat
Markov_Models: theory Coinductive_List
Markov_Models: theory Coinductive_List_Prefix
Markov_Models: theory Quotient_Coinductive_List
Markov_Models: theory TLList
Markov_Models: theory Coinductive_Stream
Markov_Models: theory Quotient_TLList
Markov_Models: theory Coinductive
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
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
Featherweight_OCL: theory Analysis_OCL
Markov_Models: theory Zeroconf_Analysis
Markov_Models: theory Example_A
Markov_Models: theory Example_B
Markov_Models: theory MDP_Reachability_Problem
Markov_Models: theory PGCL
Markov_Models: theory PCTL
Markov_Models: theory MDP_RP_Certification
Markov_Models: theory Markov_Models
Featherweight_OCL: theory Design_OCL
Timing Featherweight_OCL (4 threads, 149.730s elapsed time, 474.984s cpu time, 11.572s GC time, factor 3.17)
Finished Featherweight_OCL (0:02:32 elapsed time, 0:07:57 cpu time, factor 3.14)
Running KBPs ...
KBPs: theory Extra
KBPs: theory List_local
Timing Markov_Models (4 threads, 130.168s elapsed time, 435.444s cpu time, 11.172s GC time, factor 3.35)
Finished Markov_Models (0:02:15 elapsed time, 0:07:42 cpu time, factor 3.40)
Running Gauss_Jordan ...
Gauss_Jordan: theory Code_Abstract_Nat
Gauss_Jordan: theory Bit
Gauss_Jordan: theory Dual_Order
Gauss_Jordan: theory Code_Target_Int
Gauss_Jordan: theory Code_Target_Nat
Gauss_Jordan: theory Generalizations
Gauss_Jordan: theory Mod_Type
Gauss_Jordan: theory Code_Target_Numeral
Gauss_Jordan: theory Miscellaneous
KBPs: theory Trie
KBPs: theory DFS
KBPs: theory MapOps
KBPs: theory Kripke
KBPs: theory Traces
KBPs: theory Transitive_Closure_Impl
Gauss_Jordan: theory Fundamental_Subspaces
KBPs: theory Transitive_Closure_List_Impl
KBPs: theory ODList
Gauss_Jordan: theory Dim_Formula
KBPs: theory KBPs
KBPs: theory Eval
KBPs: theory Trie2
KBPs: theory KBPsAuto
KBPs: theory KBPsAlg
KBPs: theory SPRView
KBPs: theory SPRViewNonDet
Gauss_Jordan: theory Code_Bit
Gauss_Jordan: theory Code_Real_Approx_By_Float
Gauss_Jordan: theory Code_Set
Gauss_Jordan: theory IArray
Gauss_Jordan: theory Rank
Gauss_Jordan: theory Code_Matrix
Gauss_Jordan: theory Rref
Gauss_Jordan: theory Code_Real_Approx_By_Float_Haskell
Gauss_Jordan: theory Elementary_Operations
Gauss_Jordan: theory IArray_Addenda
Gauss_Jordan: theory IArray_Haskell
KBPs: theory ClockView
KBPs: theory SPRViewDet
KBPs: theory SPRViewNonDetIndInit
Gauss_Jordan: theory Matrix_To_IArray
Gauss_Jordan: theory Gauss_Jordan
KBPs: theory SPRViewSingle
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 Inverse
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
KBPs: theory Robot
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
KBPs: theory MuddyChildren
KBPs: theory Views
KBPs: theory Examples
KBPs: theory KBPs_Main
Timing KBPs (4 threads, 132.730s elapsed time, 369.392s cpu time, 11.396s GC time, factor 2.78)
Finished KBPs (0:02:18 elapsed time, 0:06:15 cpu time, factor 2.71)
Running Density_Compiler ...
Density_Compiler: theory Density_Predicates
Density_Compiler: theory PDF_Transformations
Density_Compiler: theory PDF_Values
Density_Compiler: theory PDF_Semantics
Density_Compiler: theory PDF_Density_Contexts
Density_Compiler: theory PDF_Target_Semantics
Density_Compiler: theory PDF_Compiler_Pred
Timing Gauss_Jordan (4 threads, 131.738s elapsed time, 484.784s cpu time, 8.328s GC time, factor 3.68)
Finished Gauss_Jordan (0:02:15 elapsed time, 0:08:08 cpu time, factor 3.60)
Running PseudoHoops ...
Density_Compiler: theory PDF_Target_Density_Contexts
Density_Compiler: theory PDF_Compiler
PseudoHoops: theory Operations
PseudoHoops: theory LeftComplementedMonoid
PseudoHoops: theory PseudoWaisbergAlgebra
PseudoHoops: theory RightComplementedMonoid
PseudoHoops: theory PseudoHoops
PseudoHoops: theory PseudoHoopFilters
PseudoHoops: theory SpecialPseudoHoops
Timing Density_Compiler (4 threads, 127.140s elapsed time, 388.588s cpu time, 5.184s GC time, factor 3.06)
Finished Density_Compiler (0:02:12 elapsed time, 0:06:34 cpu time, factor 2.97)
Running LTL_to_DRA ...
PseudoHoops: theory Examples
LTL_to_DRA: theory List_Index
LTL_to_DRA: theory DFS
LTL_to_DRA: theory Boolean_Expression_Checkers
LTL_to_DRA: theory Boolean_Expression_Checkers_AList_Mapping
LTL_to_DRA FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/LTL_to_DRA)
    and isNode :: "'a \<Rightarrow> bool" 
    and invariant :: "'b \<Rightarrow> bool" 
    and ins :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
    and memb :: "'a \<Rightarrow> 'b \<Rightarrow> bool" 
    and empt :: "'b" 
    and nodeAbs :: "'a \<Rightarrow> 'c" 
  assumes "DFS succs isNode invariant ins memb empt nodeAbs"
locale DFS =
  fixes succs :: "'a \<Rightarrow> 'a list" 
    and isNode :: "'a \<Rightarrow> bool" 
    and invariant :: "'b \<Rightarrow> bool" 
    and ins :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
    and memb :: "'a \<Rightarrow> 'b \<Rightarrow> bool" 
    and empt :: "'b" 
    and nodeAbs :: "'a \<Rightarrow> 'c" 
  assumes "DFS succs isNode invariant ins memb empt nodeAbs"
### theory "DFS"
### 0.989s elapsed time, 3.396s cpu time, 0.000s GC time
### theory "List_Index"
### 1.201s elapsed time, 4.120s cpu time, 0.000s GC time
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
locale reduced_bdt_checkers =
  fixes ifex_of :: "'b \<Rightarrow> 'a ifex" 
    and
    val :: "'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
  assumes "reduced_bdt_checkers ifex_of val"
Found termination order: "size <*mlex*> {}"
### theory "Boolean_Expression_Checkers"
### 10.494s elapsed time, 33.736s cpu time, 0.984s GC time
Loading theory "Boolean_Expression_Checkers_AList_Mapping"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### theory "Boolean_Expression_Checkers_AList_Mapping"
### 0.509s elapsed time, 1.216s cpu time, 0.000s GC time
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Running Ergodic_Theory ...
Ergodic_Theory: theory SG_Library_Complement
Timing PseudoHoops (4 threads, 120.641s elapsed time, 178.308s cpu time, 3.568s GC time, factor 1.48)
Finished PseudoHoops (0:02:04 elapsed time, 0:03:00 cpu time, factor 1.45)
Running Random_Graph_Subgraph_Threshold ...
Ergodic_Theory: theory Banach_Density
Ergodic_Theory: theory Conditional_Expectation
Ergodic_Theory: theory Fekete
Ergodic_Theory: theory Measure_Preserving_Transformations
Ergodic_Theory: theory Recurrence
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
Random_Graph_Subgraph_Threshold: theory Code_Target_Nat
Random_Graph_Subgraph_Threshold: theory Girth_Chromatic_Misc
Random_Graph_Subgraph_Threshold: theory Code_Target_Numeral
Ergodic_Theory: theory Invariants
Random_Graph_Subgraph_Threshold: theory Ugraphs
Ergodic_Theory: theory Ergodicity
Ergodic_Theory: theory Kingman
Ergodic_Theory: theory Gouezel_Karlsson
Random_Graph_Subgraph_Threshold: theory Float
Random_Graph_Subgraph_Threshold: theory Approximation
Random_Graph_Subgraph_Threshold: theory Girth_Chromatic
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
Timing Ergodic_Theory (4 threads, 105.719s elapsed time, 401.240s cpu time, 5.220s GC time, factor 3.80)
Finished Ergodic_Theory (0:01:51 elapsed time, 0:06:46 cpu time, factor 3.66)
Running Consensus_Refined ...
Timing Random_Graph_Subgraph_Threshold (4 threads, 101.198s elapsed time, 287.212s cpu time, 5.968s GC time, factor 2.84)
Finished Random_Graph_Subgraph_Threshold (0:01:46 elapsed time, 0:04:52 cpu time, factor 2.74)
Running Girth_Chromatic ...
Consensus_Refined: theory Infinite_Set
Consensus_Refined: theory HOModel
Consensus_Refined: theory Majorities
Consensus_Refined: theory Omega_Words_Fun
Consensus_Refined: theory Samplers
Consensus_Refined: theory StutterEquivalence
Consensus_Refined: theory Reduction
Girth_Chromatic: theory Code_Target_Int
Girth_Chromatic: theory Dense_Linear_Order
Girth_Chromatic: theory Code_Abstract_Nat
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
Consensus_Refined: theory Consensus_Misc
Consensus_Refined: theory Consensus_Types
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
Consensus_Refined: theory Paxos_Defs
Consensus_Refined: theory Refinement
Girth_Chromatic: theory Float
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
Girth_Chromatic: theory Approximation
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
Consensus_Refined: theory Uv_Proofs
Girth_Chromatic: theory Girth_Chromatic
Timing Girth_Chromatic (4 threads, 83.152s elapsed time, 226.372s cpu time, 5.140s GC time, factor 2.72)
Finished Girth_Chromatic (0:01:28 elapsed time, 0:03:51 cpu time, factor 2.61)
Running SATSolverVerification ...
SATSolverVerification: theory MoreList
SATSolverVerification: theory CNF
SATSolverVerification: theory Trail
SATSolverVerification: theory SatSolverVerification
Timing Consensus_Refined (4 threads, 96.869s elapsed time, 210.832s cpu time, 5.868s GC time, factor 2.18)
Finished Consensus_Refined (0:01:39 elapsed time, 0:03:33 cpu time, factor 2.15)
Running Multirelations ...
SATSolverVerification: theory BasicDPLL
SATSolverVerification: theory KrsticGoel
SATSolverVerification: theory NieuwenhuisOliverasTinelli
SATSolverVerification: theory SatSolverCode
Multirelations: theory C_Algebras
SATSolverVerification: theory AssertLiteral
SATSolverVerification: theory ConflictAnalysis
SATSolverVerification: theory Decide
SATSolverVerification: theory UnitPropagate
SATSolverVerification: theory Initialization
SATSolverVerification: theory SolveLoop
SATSolverVerification: theory FunctionalImplementation
Multirelations: theory Multirelations
Timing Multirelations (4 threads, 93.431s elapsed time, 144.960s cpu time, 4.508s GC time, factor 1.55)
Finished Multirelations (0:01:37 elapsed time, 0:07:29 cpu time, factor 4.63)
Running Dijkstra_Shortest_Path ...
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
Timing SATSolverVerification (4 threads, 119.915s elapsed time, 355.696s cpu time, 5.716s GC time, factor 2.97)
Finished SATSolverVerification (0:02:06 elapsed time, 0:06:01 cpu time, factor 2.87)
Running Derangements ...
Derangements: theory Permutations
Derangements: theory Code_Abstract_Nat
Derangements: theory Code_Target_Int
Derangements: theory Dense_Linear_Order
Derangements: theory Code_Target_Nat
Derangements: theory Lattice_Algebras
Derangements: theory Code_Target_Numeral
Dijkstra_Shortest_Path: theory GraphGA
Dijkstra_Shortest_Path: theory GraphByMap
Dijkstra_Shortest_Path: theory HashGraphImpl
Derangements: theory Float
Dijkstra_Shortest_Path: theory Dijkstra_Impl
Dijkstra_Shortest_Path: theory Dijkstra_Impl_Adet
Derangements: theory Approximation
Dijkstra_Shortest_Path: theory Test
Timing Dijkstra_Shortest_Path (4 threads, 86.795s elapsed time, 151.904s cpu time, 4.112s GC time, factor 1.75)
Finished Dijkstra_Shortest_Path (0:01:37 elapsed time, 0:05:05 cpu time, factor 3.15)
MSO_Examples CANCELLED
Running Rep_Fin_Groups ...
Rep_Fin_Groups: theory Infinite_Set
Rep_Fin_Groups: theory Function_Algebras
Rep_Fin_Groups: theory More_List
Rep_Fin_Groups: theory Set_Algebras
Rep_Fin_Groups: theory Polynomial
Derangements: theory Derangements
Timing Derangements (4 threads, 85.473s elapsed time, 223.304s cpu time, 5.372s GC time, factor 2.61)
Finished Derangements (0:01:27 elapsed time, 0:03:45 cpu time, factor 2.57)
Running Knot_Theory ...
Rep_Fin_Groups: theory Rep_Fin_Groups
Knot_Theory: theory More_List
Knot_Theory: theory Fraction_Field
Knot_Theory: theory Polynomial
Knot_Theory: theory Preliminaries
Knot_Theory: theory Tangle_Relation
Knot_Theory: theory Tangles
Knot_Theory: theory Tangle_Algebra
Knot_Theory: theory Tangle_Moves
Knot_Theory: theory Link_Algebra
Knot_Theory: theory Example
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 Rep_Fin_Groups (4 threads, 80.213s elapsed time, 289.128s cpu time, 5.204s GC time, factor 3.60)
Finished Rep_Fin_Groups (0:01:22 elapsed time, 0:04:51 cpu time, factor 3.52)
Running LinearQuantifierElim ...
Timing Knot_Theory (4 threads, 68.290s elapsed time, 247.896s cpu time, 4.344s GC time, factor 3.63)
Finished Knot_Theory (0:01:15 elapsed time, 0:04:11 cpu time, factor 3.32)
Running LightweightJava ...
LightweightJava: theory Multiset
LightweightJava: theory Infinite_Set
LinearQuantifierElim: theory Logic
LinearQuantifierElim: theory QE
LightweightJava: theory Lightweight_Java_Definition
LinearQuantifierElim: theory PresArith
LinearQuantifierElim: theory DLO
LinearQuantifierElim: theory LinArith
LinearQuantifierElim: theory Cooper
LinearQuantifierElim: theory QEpres
LinearQuantifierElim: theory QEdlo
LinearQuantifierElim: theory QEdlo_fr
LinearQuantifierElim: theory QEdlo_inf
LinearQuantifierElim: theory FRE
LinearQuantifierElim: theory QEdlo_ex
LinearQuantifierElim: theory QElin
LinearQuantifierElim: theory QElin_inf
LinearQuantifierElim: theory QElin_opt
LightweightJava: theory Lightweight_Java_Equivalence
LightweightJava: theory Lightweight_Java_Proof
Timing LightweightJava (4 threads, 62.322s elapsed time, 139.840s cpu time, 3.888s GC time, factor 2.24)
Finished LightweightJava (0:01:04 elapsed time, 0:02:22 cpu time, factor 2.19)
Running ComponentDependencies ...
ComponentDependencies: theory DataDependenciesConcreteValues
LinearQuantifierElim: theory CertLin
LinearQuantifierElim: theory CertDlo
Timing LinearQuantifierElim (4 threads, 73.089s elapsed time, 224.604s cpu time, 15.184s GC time, factor 3.07)
Finished LinearQuantifierElim (0:01:19 elapsed time, 0:03:50 cpu time, factor 2.92)
Running Koenigsberg_Friendship ...
Koenigsberg_Friendship: theory MoreGraph
Koenigsberg_Friendship: theory FriendshipTheory
Koenigsberg_Friendship: theory KoenigsbergBridge
ComponentDependencies: theory DataDependencies
ComponentDependencies: theory DataDependenciesCaseStudy
Timing ComponentDependencies (4 threads, 60.799s elapsed time, 184.860s cpu time, 6.232s GC time, factor 3.04)
Finished ComponentDependencies (0:01:03 elapsed time, 0:03:07 cpu time, factor 2.96)
Running Tree-Automata ...
Timing Koenigsberg_Friendship (4 threads, 51.397s elapsed time, 187.348s cpu time, 3.952s GC time, factor 3.65)
Finished Koenigsberg_Friendship (0:00:56 elapsed time, 0:03:10 cpu time, factor 3.37)
Running DPT-SAT-Solver ...
DPT-SAT-Solver: theory DPT_SAT_Solver
DPT-SAT-Solver: theory DPT_SAT_Tests
Tree-Automata: theory Tree
Tree-Automata: theory Exploration
Timing DPT-SAT-Solver (4 threads, 3.630s elapsed time, 8.404s cpu time, 0.032s GC time, factor 2.32)
Finished DPT-SAT-Solver (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.80)
Running DataRefinementIBP ...
Tree-Automata: theory Ta
DataRefinementIBP: theory Conj_Disj
DataRefinementIBP: theory WellFoundedTransitive
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.913s elapsed time, 12.336s cpu time, 0.124s GC time, factor 2.51)
Finished DataRefinementIBP (0:00:07 elapsed time, 0:00:14 cpu time, factor 2.02)
Running Decreasing-Diagrams-II ...
Tree-Automata: theory AbsAlgo
Decreasing-Diagrams-II: theory Order_Union
Decreasing-Diagrams-II: theory Infinite_Sequences
Decreasing-Diagrams-II: theory Least_Enum
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
Decreasing-Diagrams-II: theory Almost_Full_Relations
Decreasing-Diagrams-II: theory Well_Quasi_Orders
Decreasing-Diagrams-II: theory Multiset_Extension
Tree-Automata: theory Ta_impl
Decreasing-Diagrams-II: theory Decreasing_Diagrams_II_Aux
Decreasing-Diagrams-II: theory Decreasing_Diagrams_II
Tree-Automata: theory Ta_impl_codegen
Timing Decreasing-Diagrams-II (4 threads, 31.216s elapsed time, 108.284s cpu time, 2.616s GC time, factor 3.47)
Finished Decreasing-Diagrams-II (0:00:34 elapsed time, 0:01:51 cpu time, factor 3.26)
Running Depth-First-Search ...
Depth-First-Search: theory DFS
Timing Tree-Automata (4 threads, 43.871s elapsed time, 120.504s cpu time, 2.952s GC time, factor 2.75)
Finished Tree-Automata (0:00:54 elapsed time, 0:02:10 cpu time, factor 2.41)
Running Descartes_Sign_Rule ...
Timing Depth-First-Search (4 threads, 1.544s elapsed time, 4.180s cpu time, 0.000s GC time, factor 2.71)
Finished Depth-First-Search (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.70)
Running DiskPaxos ...
DiskPaxos: theory DiskPaxos_Model
Descartes_Sign_Rule: theory Descartes_Sign_Rule
DiskPaxos: theory DiskPaxos_Inv1
DiskPaxos: theory DiskPaxos_Inv2
DiskPaxos: theory DiskPaxos_Inv3
DiskPaxos: theory DiskPaxos_Inv4
DiskPaxos: theory DiskPaxos_Inv5
DiskPaxos: theory DiskPaxos_Chosen
DiskPaxos: theory DiskPaxos_Inv6
DiskPaxos: theory DiskPaxos_Invariant
DiskPaxos: theory DiskPaxos
Timing Descartes_Sign_Rule (4 threads, 5.069s elapsed time, 15.656s cpu time, 0.164s GC time, factor 3.09)
Finished Descartes_Sign_Rule (0:00:10 elapsed time, 0:00:21 cpu time, factor 2.00)
Running Dynamic_Tables ...
Dynamic_Tables: theory Amor
Dynamic_Tables: theory Tables_real
Dynamic_Tables: theory Tables_nat
Timing Dynamic_Tables (4 threads, 21.134s elapsed time, 63.548s cpu time, 1.152s GC time, factor 3.01)
Finished Dynamic_Tables (0:00:23 elapsed time, 0:01:05 cpu time, factor 2.80)
Running Efficient-Mergesort ...
Efficient-Mergesort: theory Efficient_Sort
Timing DiskPaxos (4 threads, 36.757s elapsed time, 135.872s cpu time, 1.096s GC time, factor 3.70)
Finished DiskPaxos (0:00:39 elapsed time, 0:02:18 cpu time, factor 3.52)
Running Euler_Partition ...
Euler_Partition: theory Additions_to_Main
Euler_Partition: theory Number_Partition
Euler_Partition: theory Euler_Partition
Timing Euler_Partition (4 threads, 4.901s elapsed time, 19.000s cpu time, 0.148s GC time, factor 3.88)
Finished Euler_Partition (0:00:07 elapsed time, 0:00:21 cpu time, factor 2.97)
Running Example-Submission ...
Example-Submission: theory Submission
Timing Example-Submission (4 threads, 1.260s elapsed time, 1.380s cpu time, 0.000s GC time, factor 1.10)
Finished Example-Submission (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.02)
Running FFT ...
FFT: theory FFT
Timing Efficient-Mergesort (4 threads, 15.021s elapsed time, 28.528s cpu time, 0.648s GC time, factor 1.90)
Finished Efficient-Mergesort (0:00:20 elapsed time, 0:00:34 cpu time, factor 1.64)
Running FOL-Fitting ...
Timing FFT (4 threads, 2.464s elapsed time, 8.036s cpu time, 0.000s GC time, factor 3.26)
Finished FFT (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.19)
Running FeatherweightJava ...
FeatherweightJava: theory FJDefs
FOL-Fitting: theory FOL_Fitting
FeatherweightJava: theory FJAux
FeatherweightJava: theory FJSound
FeatherweightJava: theory Execute
FeatherweightJava: theory Featherweight_Java
Timing FeatherweightJava (4 threads, 16.586s elapsed time, 48.124s cpu time, 1.120s GC time, factor 2.90)
Finished FeatherweightJava (0:00:19 elapsed time, 0:00:50 cpu time, factor 2.65)
Running Fermat3_4 ...
Fermat3_4: theory IntNatAux
Fermat3_4: theory Fermat4
Fermat3_4: theory QuadForm
Fermat3_4: theory Fermat3
Timing FOL-Fitting (4 threads, 21.097s elapsed time, 39.760s cpu time, 2.056s GC time, factor 1.88)
Finished FOL-Fitting (0:00:26 elapsed time, 0:00:45 cpu time, factor 1.69)
Running FileRefinement ...
FileRefinement: theory ResizableArrays
FileRefinement: theory CArrays
FileRefinement: theory FileRefinement
Timing FileRefinement (4 threads, 10.586s elapsed time, 26.512s cpu time, 0.096s GC time, factor 2.50)
Finished FileRefinement (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.22)
Running FinFun ...
FinFun: theory Card_Univ
FinFun: theory FinFun
FinFun: theory FinFunPred
Timing Fermat3_4 (4 threads, 23.334s elapsed time, 89.424s cpu time, 1.048s GC time, factor 3.83)
Finished Fermat3_4 (0:00:26 elapsed time, 0:01:32 cpu time, factor 3.42)
Timing FinFun (4 threads, 5.994s elapsed time, 20.120s cpu time, 0.388s GC time, factor 3.36)
Finished FinFun (0:00:08 elapsed time, 0:00:22 cpu time, factor 2.68)
Running Finger-Trees ...
Running Finite_Automata_HF ...
Finite_Automata_HF: theory Nat_Bijection
Finite_Automata_HF: theory Regular_Set
Finite_Automata_HF: theory HF
Finger-Trees: theory FingerTree
Finite_Automata_HF: theory Ordinal
Finite_Automata_HF: theory Regular_Exp
Finite_Automata_HF: theory Finite_Automata_HF
Timing Finite_Automata_HF (4 threads, 17.102s elapsed time, 54.216s cpu time, 1.484s GC time, factor 3.17)
Finished Finite_Automata_HF (0:00:19 elapsed time, 0:01:01 cpu time, factor 3.11)
Running Free-Boolean-Algebra ...
Finger-Trees: theory Test
Free-Boolean-Algebra: theory Free_Boolean_Algebra
Timing Finger-Trees (4 threads, 21.622s elapsed time, 44.012s 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)
Timing Free-Boolean-Algebra (4 threads, 1.576s elapsed time, 4.892s cpu time, 0.000s GC time, factor 3.10)
Finished Free-Boolean-Algebra (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.45)
Running Free-Groups ...
Running FunWithFunctions ...
FunWithFunctions: theory FunWithFunctions
Free-Groups: theory Order_Union
Free-Groups: theory Commutation
Free-Groups: theory Cardinal_Notations
Free-Groups: theory Congruence
Free-Groups: theory Fun_More
Free-Groups: theory FuncSet
Free-Groups: theory Primes
Free-Groups: theory Order_Relation_More
Free-Groups: theory Wellfounded_More
Free-Groups: theory Wellorder_Relation
Free-Groups: theory Wellorder_Embedding
Free-Groups: theory Lattice
Free-Groups: theory Wellorder_Constructions
Timing FunWithFunctions (4 threads, 2.915s elapsed time, 8.544s cpu time, 0.000s GC time, factor 2.93)
Finished FunWithFunctions (0:00:05 elapsed time, 0:00:10 cpu time, factor 2.10)
Running FunWithTilings ...
Free-Groups: theory Cardinal_Order_Relation
FunWithTilings: theory Tilings
Free-Groups: theory Group
Free-Groups: theory Bij
Free-Groups: theory Coset
Free-Groups: theory FiniteProduct
Free-Groups: theory Ring
Free-Groups: theory AbelCoset
Free-Groups: theory Ideal
Timing FunWithTilings (4 threads, 21.822s elapsed time, 65.896s cpu time, 0.116s GC time, factor 3.02)
Finished FunWithTilings (0:00:24 elapsed time, 0:01:08 cpu time, factor 2.81)
Running Functional-Automata ...
Functional-Automata: theory Regular_Set
Free-Groups: theory RingHom
Functional-Automata: theory Regular_Exp
Free-Groups: theory QuotRing
Free-Groups: theory IntRing
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 Automata
Functional-Automata: theory RegExp2NA
Functional-Automata: theory RegExp2NAe
Functional-Automata: theory AutoMaxChop
Free-Groups: theory Cancelation
Free-Groups: theory Generators
Free-Groups: theory C2
Functional-Automata: theory AutoRegExp
Free-Groups: theory FreeGroups
Free-Groups: theory UnitGroup
Functional-Automata: theory Execute
Functional-Automata: theory Functional_Automata
Free-Groups: theory PingPongLemma
Free-Groups: theory Isomorphisms
Timing Functional-Automata (4 threads, 19.863s elapsed time, 40.740s cpu time, 0.984s GC time, factor 2.05)
Finished Functional-Automata (0:00:25 elapsed time, 0:00:51 cpu time, factor 2.00)
Running GPU_Kernel_PL ...
GPU_Kernel_PL: theory Misc
GPU_Kernel_PL: theory KPL_syntax
Timing Free-Groups (4 threads, 57.042s elapsed time, 196.020s cpu time, 6.556s GC time, factor 3.44)
Finished Free-Groups (0:00:59 elapsed time, 0:03:18 cpu time, factor 3.33)
Running Gauss-Jordan-Elim-Fun ...
Gauss-Jordan-Elim-Fun: theory Gauss_Jordan_Elim_Fun
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 Gauss-Jordan-Elim-Fun (4 threads, 4.049s elapsed time, 12.152s cpu time, 0.088s GC time, factor 3.00)
Finished Gauss-Jordan-Elim-Fun (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.28)
Running GenClock ...
GPU_Kernel_PL: theory Kernel_programming_language
GenClock: theory GenClock
Timing GPU_Kernel_PL (4 threads, 10.709s elapsed time, 19.304s cpu time, 0.464s GC time, factor 1.80)
Finished GPU_Kernel_PL (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.65)
Running General-Triangle ...
General-Triangle: theory GeneralTriangle
Timing General-Triangle (4 threads, 2.235s elapsed time, 4.268s cpu time, 0.000s GC time, factor 1.91)
Finished General-Triangle (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.45)
Running GraphMarkingIBP ...
Timing GenClock (4 threads, 5.383s elapsed time, 19.984s cpu time, 0.164s GC time, factor 3.71)
Finished GenClock (0:00:07 elapsed time, 0:00:22 cpu time, factor 2.90)
Running Heard_Of ...
GraphMarkingIBP: theory WellFoundedTransitive
GraphMarkingIBP: theory Conj_Disj
Heard_Of: theory Infinite_Set
GraphMarkingIBP: theory Complete_Lattice_Prop
GraphMarkingIBP: theory Preliminaries
Heard_Of: theory Omega_Words_Fun
GraphMarkingIBP: theory Statements
GraphMarkingIBP: theory Hoare
GraphMarkingIBP: theory Diagram
Heard_Of: theory Samplers
Heard_Of: theory StutterEquivalence
GraphMarkingIBP: theory DataRefinement
GraphMarkingIBP: theory Graph
GraphMarkingIBP: theory SetMark
Heard_Of: theory Majorities
Heard_Of: theory HOModel
GraphMarkingIBP: theory StackMark
GraphMarkingIBP: theory LinkMark
GraphMarkingIBP: theory DSWMark
Heard_Of: theory EigbyzDefs
Heard_Of: theory LastVotingDefs
Heard_Of: theory OneThirdRuleDefs
Heard_Of: theory AteDefs
Heard_Of: theory UteDefs
Heard_Of: theory UvDefs
Heard_Of: theory Reduction
Heard_Of: theory AteProof
Heard_Of: theory EigbyzProof
Heard_Of: theory LastVotingProof
Heard_Of: theory OneThirdRuleProof
Heard_Of: theory UteProof
Heard_Of: theory UvProof
Timing GraphMarkingIBP (4 threads, 26.268s elapsed time, 73.308s cpu time, 0.768s GC time, factor 2.79)
Finished GraphMarkingIBP (0:00:28 elapsed time, 0:01:15 cpu time, factor 2.64)
Running HereditarilyFinite ...
HereditarilyFinite: theory Nat_Bijection
HereditarilyFinite: theory HF
HereditarilyFinite: theory Ordinal
HereditarilyFinite: theory Finitary
HereditarilyFinite: theory Finite_Automata
HereditarilyFinite: theory Rank
Timing Heard_Of (4 threads, 38.658s elapsed time, 134.924s cpu time, 3.076s GC time, factor 3.49)
Finished Heard_Of (0:00:41 elapsed time, 0:02:17 cpu time, factor 3.34)
Running Hermite ...
Timing HereditarilyFinite (4 threads, 11.449s elapsed time, 36.904s cpu time, 0.544s GC time, factor 3.22)
Finished HereditarilyFinite (0:00:13 elapsed time, 0:00:39 cpu time, factor 2.81)
Running HotelKeyCards ...
HotelKeyCards: theory LaTeXsugar
HotelKeyCards: theory Notation
HotelKeyCards: theory Basis
HotelKeyCards: theory State
HotelKeyCards: theory Trace
HotelKeyCards: theory NewCard
HotelKeyCards: theory Equivalence
Hermite: theory Hermite
Timing HotelKeyCards (4 threads, 10.097s elapsed time, 27.124s cpu time, 0.392s GC time, factor 2.69)
Finished HotelKeyCards (0:00:12 elapsed time, 0:00:29 cpu time, factor 2.36)
Running Huffman ...
Huffman: theory Huffman
Hermite: theory Hermite_IArrays
Timing Huffman (4 threads, 13.755s elapsed time, 41.076s cpu time, 0.532s GC time, factor 2.99)
Finished Huffman (0:00:16 elapsed time, 0:00:43 cpu time, factor 2.68)
Running HyperCTL ...
HyperCTL: theory Nat_Bijection
HyperCTL: theory Stream
HyperCTL: theory Infinite_Set
HyperCTL: theory Prelim
HyperCTL: theory Shallow
HyperCTL: theory Deep
HyperCTL: theory Noninterference
Timing Hermite (4 threads, 36.768s elapsed time, 112.184s cpu time, 1.488s GC time, factor 3.05)
Finished Hermite (0:00:43 elapsed time, 0:01:57 cpu time, factor 2.73)
Running Impossible_Geometry ...
HyperCTL: theory Finite_Noninterference
Impossible_Geometry: theory Impossible_Geometry
HyperCTL: theory HyperCTL
Timing HyperCTL (4 threads, 18.093s elapsed time, 56.956s cpu time, 1.872s GC time, factor 3.15)
Finished HyperCTL (0:00:20 elapsed time, 0:00:59 cpu time, factor 2.88)
Running Inductive_Confidentiality ...
Inductive_Confidentiality: theory Message
Inductive_Confidentiality: theory MessageGA
Inductive_Confidentiality: theory EventGA
Inductive_Confidentiality: theory Event
Timing Impossible_Geometry (4 threads, 13.581s elapsed time, 32.708s cpu time, 0.532s GC time, factor 2.41)
Finished Impossible_Geometry (0:00:16 elapsed time, 0:00:35 cpu time, factor 2.17)
InformationFlowSlicing CANCELLED
InformationFlowSlicing_Intra CANCELLED
Running Integration ...
Inductive_Confidentiality: theory PublicGA
Inductive_Confidentiality: theory Public
Integration: theory Nat_Bijection
Integration: theory Old_Datatype
Integration: theory Sigma_Algebra
Integration: theory MonConv
Integration: theory Measure
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
Integration: theory Countable
Integration: theory RealRandVar
Integration: theory Failure
Integration: theory Integral
Timing Inductive_Confidentiality (4 threads, 16.916s elapsed time, 44.220s cpu time, 1.640s GC time, factor 2.61)
Finished Inductive_Confidentiality (0:00:19 elapsed time, 0:00:46 cpu time, factor 2.39)
Running Isabelle_Meta_Model ...
Isabelle_Meta_Model: theory Isabelle_code_target
Isabelle_Meta_Model: theory Isabelle_code_runtime
Isabelle_Meta_Model: theory Isabelle_Cartouche_Examples
Isabelle_Meta_Model: theory Isabelle_parse_spec
Isabelle_Meta_Model: theory Isabelle_function_common
Isabelle_Meta_Model: theory Isabelle_isar_syn
Isabelle_Meta_Model: theory Isabelle_fun
Isabelle_Meta_Model: theory Isabelle_typedecl
Isabelle_Meta_Model: theory Isabelle_Main0
Isabelle_Meta_Model: theory Isabelle_Main2
Isabelle_Meta_Model FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/Isabelle_Meta_Model)
    structure Data_code: THEORY_DATA
    val apply_code_printing: theory -> theory
    val apply_code_printing_reflect: theory -> theory
    val code_empty: string
    datatype code_printing
    =
         Code_printing of
             (string * (bstring * Code_Printer.raw_const_syntax option) list
              ,
             string * (bstring * Code_Printer.tyco_syntax option) list,
             string * (bstring * string option) list,
             (string * string) * (bstring * unit option) list,
             (xstring * string) * (bstring * unit option) list,
             bstring * (bstring * (string * string list) option) list)
             Code_Symbol.attr
             list
    val reflect_ml: Input.source -> theory -> theory
  end
### theory "Isabelle_code_target"
### 0.346s elapsed time, 1.208s cpu time, 0.000s GC time
structure Isabelle_Function_Fun: sig end
### theory "Isabelle_fun"
### 0.108s elapsed time, 0.376s cpu time, 0.000s GC time
structure Isabelle_Isar_Syn: sig end
### theory "Isabelle_isar_syn"
### 0.145s elapsed time, 0.492s cpu time, 0.000s GC time
Loading theory "Isabelle_Main0"
structure Isabelle_Typedecl:
  sig val abbrev_cmd0: binding option -> theory -> string -> typ end
### theory "Isabelle_typedecl"
### 0.115s elapsed time, 0.376s cpu time, 0.000s GC time
Loading theory "Isabelle_Main2"
### theory "Isabelle_Main2"
### 0.086s elapsed time, 0.252s cpu time, 0.000s GC time
### theory "Isabelle_Main0"
### 0.150s elapsed time, 0.396s cpu time, 0.000s GC time
*** Failed to load theory "Isabelle_Main1" (unresolved "Isabelle_code_runtime")
*** ML error (line 70 of "~~/afp/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_runtime.thy"):
*** Value or constructor (use_text) has not been declared in structure ML_Compiler0
*** At command "ML" (line 48 of "~~/afp/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_runtime.thy")
Running JiveDataStoreModel ...
JiveDataStoreModel: theory TypeIds
Timing Integration (4 threads, 19.693s elapsed time, 70.496s cpu time, 1.204s GC time, factor 3.58)
Finished Integration (0:00:22 elapsed time, 0:01:12 cpu time, factor 3.29)
Running Jordan_Hoelder ...
JiveDataStoreModel: theory JavaType
Jordan_Hoelder: theory GroupAction
Jordan_Hoelder: theory SubgroupConjugation
Jordan_Hoelder: theory SndSylow
JiveDataStoreModel: theory DirectSubtypes
JiveDataStoreModel: theory Subtype
JiveDataStoreModel: theory Attributes
JiveDataStoreModel: theory Value
JiveDataStoreModel: theory AttributesIndep
JiveDataStoreModel: theory Location
Jordan_Hoelder: theory GroupIsoClasses
Jordan_Hoelder: theory SndIsomorphismGrp
Jordan_Hoelder: theory SubgroupsAndNormalSubgroups
JiveDataStoreModel: theory Store
Jordan_Hoelder: theory SimpleGroups
JiveDataStoreModel: theory StoreProperties
JiveDataStoreModel: theory JML
JiveDataStoreModel: theory UnivSpec
Jordan_Hoelder: theory MaximalNormalSubgroups
Jordan_Hoelder: theory CompositionSeries
Jordan_Hoelder: theory JordanHolder
Timing JiveDataStoreModel (4 threads, 17.777s elapsed time, 46.924s cpu time, 1.088s GC time, factor 2.64)
Finished JiveDataStoreModel (0:00:20 elapsed time, 0:00:49 cpu time, factor 2.43)
Running KAT_and_DRA ...
KAT_and_DRA: theory KAT2
KAT_and_DRA: theory DRAT2
KAT_and_DRA: theory Test_Dioid
Timing Jordan_Hoelder (4 threads, 23.861s elapsed time, 84.568s cpu time, 1.584s GC time, factor 3.54)
Finished Jordan_Hoelder (0:00:27 elapsed time, 0:01:27 cpu time, factor 3.24)
Running Lam-ml-Normalization ...
Lam-ml-Normalization: theory LaTeXsugar
Lam-ml-Normalization: theory Lam_ml
KAT_and_DRA: theory Conway_Tests
KAT_and_DRA: theory KAT
KAT_and_DRA: theory DRAT
KAT_and_DRA: theory PHL_KAT
KAT_and_DRA: theory KAT_Models
KAT_and_DRA: theory DRA_Models
KAT_and_DRA: theory FolkTheorem
KAT_and_DRA: theory PHL_DRAT
Timing Lam-ml-Normalization (4 threads, 15.520s elapsed time, 35.296s cpu time, 0.972s GC time, factor 2.27)
Finished Lam-ml-Normalization (0:00:18 elapsed time, 0:00:37 cpu time, factor 2.08)
Running Landau_Symbols ...
Landau_Symbols: theory Group_Sort
Landau_Symbols: theory Landau_Library
Landau_Symbols: theory Landau_Symbols_Definition
Timing KAT_and_DRA (4 threads, 33.205s elapsed time, 108.976s cpu time, 2.476s GC time, factor 3.28)
Finished KAT_and_DRA (0:00:37 elapsed time, 0:01:56 cpu time, factor 3.14)
Running Latin_Square ...
Landau_Symbols: theory Landau_Real_Products
Latin_Square: theory Latin_Square
Landau_Symbols: theory Landau_Simprocs
Landau_Symbols: theory Landau_Symbols
Timing Latin_Square (4 threads, 8.067s elapsed time, 27.148s cpu time, 0.172s GC time, factor 3.37)
Finished Latin_Square (0:00:10 elapsed time, 0:00:29 cpu time, factor 2.71)
Running Liouville_Numbers ...
Liouville_Numbers: theory Infinite_Set
Liouville_Numbers: theory More_List
Timing Landau_Symbols (4 threads, 15.547s elapsed time, 54.692s cpu time, 1.352s GC time, factor 3.52)
Finished Landau_Symbols (0:00:21 elapsed time, 0:01:00 cpu time, factor 2.83)
Running List-Index ...
Liouville_Numbers: theory Polynomial
List-Index: theory List_Index
List-Index FAILED
(see also /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86_64-linux/log/List-Index)
Loading theory "List_Index"
### theory "List_Index"
### 1.214s elapsed time, 3.780s cpu time, 0.000s GC time
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** Undefined fact: "bij_betw_imageE" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
*** At command "by" (line 241 of "~~/afp/thys/List-Index/List_Index.thy")
Running List_Interleaving ...
Liouville_Numbers: theory Liouville_Numbers_Misc
List_Interleaving: theory ListInterleaving
Liouville_Numbers: theory Liouville_Numbers
Timing Liouville_Numbers (4 threads, 11.762s elapsed time, 39.632s cpu time, 0.756s GC time, factor 3.37)
Finished Liouville_Numbers (0:00:14 elapsed time, 0:00:42 cpu time, factor 2.95)
Running Locally-Nameless-Sigma ...
Timing List_Interleaving (4 threads, 5.555s elapsed time, 17.280s cpu time, 0.344s GC time, factor 3.11)
Finished List_Interleaving (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.49)
Running Lower_Semicontinuous ...
Locally-Nameless-Sigma: theory Commutation
Locally-Nameless-Sigma: theory Environments
Locally-Nameless-Sigma: theory ListPre
Locally-Nameless-Sigma: theory FMap
Locally-Nameless-Sigma: theory Sigma
Lower_Semicontinuous: theory Lower_Semicontinuous
Locally-Nameless-Sigma: theory ParRed
Locally-Nameless-Sigma: theory TypedSigma
Locally-Nameless-Sigma: theory Locally_Nameless_Sigma
Timing Lower_Semicontinuous (4 threads, 13.118s elapsed time, 50.808s cpu time, 0.420s GC time, factor 3.87)
Finished Lower_Semicontinuous (0:00:17 elapsed time, 0:00:54 cpu time, factor 3.19)
Running Max-Card-Matching ...
Max-Card-Matching: theory Matching
Timing Max-Card-Matching (4 threads, 2.529s elapsed time, 8.216s cpu time, 0.000s GC time, factor 3.25)
Finished Max-Card-Matching (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.18)
Running MiniML ...
MiniML: theory Maybe
MiniML: theory Type
MiniML: theory Instance
MiniML: theory Generalize
MiniML: theory MiniML
MiniML: theory W
Timing Locally-Nameless-Sigma (4 threads, 37.164s elapsed time, 129.140s cpu time, 3.256s GC time, factor 3.47)
Finished Locally-Nameless-Sigma (0:00:39 elapsed time, 0:02:11 cpu time, factor 3.31)
Running MonoBoolTranAlgebra ...
Timing MiniML (4 threads, 13.462s elapsed time, 28.680s cpu time, 0.684s GC time, factor 2.13)
Finished MiniML (0:00:15 elapsed time, 0:00:31 cpu time, factor 1.95)
Running MuchAdoAboutTwo ...
MonoBoolTranAlgebra: theory Mono_Bool_Tran
MonoBoolTranAlgebra: theory Mono_Bool_Tran_Algebra
MuchAdoAboutTwo: theory MuchAdoAboutTwo
MonoBoolTranAlgebra: theory Assertion_Algebra
MonoBoolTranAlgebra: theory Statements
Timing MonoBoolTranAlgebra (4 threads, 10.854s elapsed time, 22.572s cpu time, 0.272s GC time, factor 2.08)
Finished MonoBoolTranAlgebra (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.87)
Running Myhill-Nerode ...
Timing MuchAdoAboutTwo (4 threads, 7.634s elapsed time, 21.656s cpu time, 0.412s GC time, factor 2.84)
Finished MuchAdoAboutTwo (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.07)
Running Noninterference_Generic_Unwinding ...
Noninterference_Generic_Unwinding: theory GenericUnwinding
Myhill-Nerode: theory Regular_Set
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 Folds
Myhill-Nerode: theory Relation_Interpretation
Myhill-Nerode: theory Restricted_Predicates
Myhill-Nerode: theory Seq
Myhill-Nerode: theory Myhill_1
Myhill-Nerode: theory Minimal_Elements
Myhill-Nerode: theory Myhill_2
Myhill-Nerode: theory Myhill
Myhill-Nerode: theory Closures
Myhill-Nerode: theory Equivalence_Checking
Myhill-Nerode: theory Regexp_Method
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
Timing Noninterference_Generic_Unwinding (4 threads, 32.286s elapsed time, 42.664s cpu time, 0.364s GC time, factor 1.32)
Finished Noninterference_Generic_Unwinding (0:00:36 elapsed time, 0:00:45 cpu time, factor 1.25)
Running Noninterference_Inductive_Unwinding ...
Noninterference_Inductive_Unwinding: theory ListInterleaving
Noninterference_Inductive_Unwinding: theory CSPNoninterference
Timing Myhill-Nerode (4 threads, 34.166s elapsed time, 97.052s cpu time, 2.692s GC time, factor 2.84)
Finished Myhill-Nerode (0:00:39 elapsed time, 0:01:47 cpu time, factor 2.69)
Running NormByEval ...
NormByEval: theory NBE
Noninterference_Inductive_Unwinding: theory IpurgeUnwinding
Noninterference_Inductive_Unwinding: theory DeterministicProcesses
Noninterference_Inductive_Unwinding: theory InductiveUnwinding
Timing Noninterference_Inductive_Unwinding (4 threads, 17.396s elapsed time, 55.004s cpu time, 1.152s GC time, factor 3.16)
Finished Noninterference_Inductive_Unwinding (0:00:19 elapsed time, 0:00:57 cpu time, factor 2.90)
Running Old_Datatype_Show ...
Old_Datatype_Show: theory Old_Show
Old_Datatype_Show: theory Old_Show_Generator
Old_Datatype_Show: theory Old_Show_Instances
Timing NormByEval (4 threads, 26.350s elapsed time, 74.888s cpu time, 1.536s GC time, factor 2.84)
Finished NormByEval (0:00:28 elapsed time, 0:01:17 cpu time, factor 2.68)
Running Open_Induction ...
Old_Datatype_Show: theory Old_Show_Examples
Open_Induction: theory Restricted_Predicates
Open_Induction: theory Open_Induction
Timing Open_Induction (4 threads, 4.723s elapsed time, 12.852s cpu time, 0.164s GC time, factor 2.72)
Finished Open_Induction (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.17)
Running Ordinal ...
Ordinal: theory OrdinalDef
Ordinal: theory OrdinalInduct
Ordinal: theory OrdinalCont
Ordinal: theory OrdinalRec
Ordinal: theory OrdinalArith
Ordinal: theory OrdinalInverse
Timing Old_Datatype_Show (4 threads, 14.670s elapsed time, 19.160s cpu time, 0.224s GC time, factor 1.31)
Finished Old_Datatype_Show (0:00:24 elapsed time, 0:00:26 cpu time, factor 1.12)
Running Ordinals_and_Cardinals ...
Ordinal: theory OrdinalFix
Ordinal: theory OrdinalOmega
Ordinal: theory OrdinalVeblen
Ordinal: theory Ordinal
Ordinals_and_Cardinals: theory Cardinal_Order_Relation_discontinued
Timing Ordinal (4 threads, 5.203s elapsed time, 10.516s cpu time, 0.400s GC time, factor 2.02)
Finished Ordinal (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71)
Running Timed_Automata ...
Timing Ordinals_and_Cardinals (4 threads, 1.345s elapsed time, 1.416s cpu time, 0.000s GC time, factor 1.05)
Finished Ordinals_and_Cardinals (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
Running SequentInvertibility ...
Timed_Automata: theory Timed_Automata
Timed_Automata: theory Floyd_Warshall
Timed_Automata: theory Misc
SequentInvertibility: theory Multiset
Timed_Automata: theory DBM
Timed_Automata: theory Paths_Cycles
Timed_Automata: theory Regions
SequentInvertibility: theory SRCTransforms
SequentInvertibility: theory ModalSequents
SequentInvertibility: theory MultiSequents
SequentInvertibility: theory SingleSuccedent
Timed_Automata: theory Closure
Timed_Automata: theory DBM_Basics
Timed_Automata: theory DBM_Normalization
Timed_Automata: theory DBM_Operations
Timed_Automata: theory DBM_Zone_Semantics
Timed_Automata: theory Regions_Beta
SequentInvertibility: theory NominalSequents
Timed_Automata: theory Approx_Beta
Timed_Automata: theory Normalized_Zone_Semantics
SequentInvertibility: theory SequentInvertibility
Timing SequentInvertibility (4 threads, 78.114s elapsed time, 262.932s cpu time, 10.704s GC time, factor 3.37)
Finished SequentInvertibility (0:01:20 elapsed time, 0:04:25 cpu time, factor 3.29)
Running Separation_Logic_Imperative_HOL ...
Separation_Logic_Imperative_HOL: theory More_Bits_Int
Separation_Logic_Imperative_HOL: theory List_More
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
Separation_Logic_Imperative_HOL: theory Heap_Monad
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 Partial_Equivalence_Relation
Separation_Logic_Imperative_HOL: theory Assertions
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 List_Seg
Separation_Logic_Imperative_HOL: theory Imp_Map_Spec
Separation_Logic_Imperative_HOL: theory Imp_Set_Spec
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 Separation_Logic_Imperative_HOL (4 threads, 71.262s elapsed time, 183.852s cpu time, 6.132s GC time, factor 2.58)
Finished Separation_Logic_Imperative_HOL (0:01:17 elapsed time, 0:04:41 cpu time, factor 3.66)
Running Tarskis_Geometry ...
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 Timed_Automata (4 threads, 201.684s elapsed time, 720.168s cpu time, 12.816s GC time, factor 3.57)
Finished Timed_Automata (0:03:24 elapsed time, 0:12:02 cpu time, factor 3.54)
Running Vickrey_Clarke_Groves ...
Vickrey_Clarke_Groves: theory SetUtils
Vickrey_Clarke_Groves: theory Argmax
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 Tarskis_Geometry (4 threads, 59.733s elapsed time, 222.048s cpu time, 3.160s GC time, factor 3.72)
Finished Tarskis_Geometry (0:01:03 elapsed time, 0:03:46 cpu time, factor 3.54)
Running Regular-Sets ...
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 Vickrey_Clarke_Groves (4 threads, 58.649s elapsed time, 197.792s cpu time, 3.740s GC time, factor 3.37)
Finished Vickrey_Clarke_Groves (0:01:04 elapsed time, 0:03:23 cpu time, factor 3.16)
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
Timing Regular-Sets (4 threads, 58.112s elapsed time, 126.000s cpu time, 3.480s GC time, factor 2.17)
Finished Regular-Sets (0:01:04 elapsed time, 0:02:16 cpu time, factor 2.13)
Running UpDown_Scheme ...
UpDown_Scheme: theory List_More
UpDown_Scheme: theory Quicksort
UpDown_Scheme: theory Heap
UpDown_Scheme: theory Option_ord
UpDown_Scheme: theory Product_Lexorder
UpDown_Scheme: theory Syntax_Match
UpDown_Scheme: theory Misc
UpDown_Scheme: theory Heap_Monad
Probabilistic_System_Zoo: theory Probabilistic_Hierarchy
UpDown_Scheme: theory Array
UpDown_Scheme: theory Ref
UpDown_Scheme: theory Imperative_HOL
UpDown_Scheme: theory Imperative_HOL_Add
UpDown_Scheme: theory Run
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
Probabilistic_System_Zoo: theory Vardi
UpDown_Scheme: theory Grid
UpDown_Scheme: theory UpDown_Scheme
UpDown_Scheme: theory Triangular_Function
UpDown_Scheme: theory Imperative
UpDown_Scheme: theory Down
UpDown_Scheme: theory Up
UpDown_Scheme: theory Up_Down
Timing Probabilistic_System_Zoo (4 threads, 55.969s elapsed time, 149.260s cpu time, 4.492s GC time, factor 2.67)
Finished Probabilistic_System_Zoo (0:01:01 elapsed time, 0:02:34 cpu time, factor 2.52)
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 UpDown_Scheme (4 threads, 56.932s elapsed time, 192.964s cpu time, 4.296s GC time, factor 3.39)
Finished UpDown_Scheme (0:01:02 elapsed time, 0:03:20 cpu time, factor 3.19)
Running SumSquares ...
SumSquares: theory BijectionRel
SumSquares: theory Infinite_Set
SumSquares: theory Legacy_GCD
SumSquares: theory Multiset
SumSquares: theory Primes
SumSquares: theory IntPrimes
SumSquares: theory IntFact
SumSquares: theory EulerFermat
SumSquares: theory Finite2
SumSquares: theory WilsonRuss
SumSquares: theory Int2
SumSquares: theory Permutation
SumSquares: theory EvenOdd
SumSquares: theory Residues
SumSquares: theory Factorization
SumSquares: theory Euler
SumSquares: theory IntNatAux
SumSquares: theory Gauss
SumSquares: theory Quadratic_Reciprocity
SumSquares: theory FourSquares
SumSquares: theory TwoSquares
Timing SIFUM_Type_Systems (4 threads, 57.520s elapsed time, 182.604s cpu time, 4.996s GC time, factor 3.17)
Finished SIFUM_Type_Systems (0:00:59 elapsed time, 0:03:04 cpu time, factor 3.08)
Running RSAPSS ...
RSAPSS: theory Code_Abstract_Nat
RSAPSS: theory Code_Target_Int
RSAPSS: theory Primes
RSAPSS: theory Word
RSAPSS: theory Code_Target_Nat
RSAPSS: theory Code_Target_Numeral
Timing SumSquares (4 threads, 40.064s elapsed time, 147.548s cpu time, 2.512s GC time, factor 3.68)
Finished SumSquares (0:00:42 elapsed time, 0:02:30 cpu time, factor 3.52)
Running Prime_Harmonic_Series ...
Prime_Harmonic_Series: theory Fib
Prime_Harmonic_Series: theory Congruence
Prime_Harmonic_Series: theory Multiset
Prime_Harmonic_Series: theory Primes
Prime_Harmonic_Series: theory Cong
Prime_Harmonic_Series: theory Eratosthenes
Prime_Harmonic_Series: theory Lattice
RSAPSS: theory Congruence
RSAPSS: theory FuncSet
RSAPSS: theory Cong
RSAPSS: theory Mod
RSAPSS: theory Crypt
RSAPSS: theory Pdifference
RSAPSS: theory Productdivides
RSAPSS: theory Multiset
RSAPSS: theory WordOperations
RSAPSS: theory Lattice
Prime_Harmonic_Series: theory Group
Prime_Harmonic_Series: theory UniqueFactorization
RSAPSS: theory Group
RSAPSS: theory SHA1Padding
RSAPSS: theory SHA1
RSAPSS: theory Wordarith
Prime_Harmonic_Series: theory FiniteProduct
RSAPSS: theory EMSAPSS
RSAPSS: theory UniqueFactorization
Prime_Harmonic_Series: theory Ring
RSAPSS: theory FiniteProduct
RSAPSS: theory Ring
Prime_Harmonic_Series: theory MiscAlgebra
Prime_Harmonic_Series: theory Residues
RSAPSS: theory MiscAlgebra
RSAPSS: theory Residues
Prime_Harmonic_Series: theory Number_Theory
RSAPSS: theory Cryptinverts
RSAPSS: theory RSAPSS
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, 43.238s elapsed time, 154.364s cpu time, 3.684s GC time, factor 3.57)
Finished Prime_Harmonic_Series (0:00:47 elapsed time, 0:02:38 cpu time, factor 3.35)
Running Statecharts ...
Statecharts: theory Contrib
Statecharts: theory Kripke
Statecharts: theory DataSpace
Statecharts: theory Data
Statecharts: theory Update
Statecharts: theory Expr
Timing RSAPSS (4 threads, 55.343s elapsed time, 198.672s cpu time, 5.044s GC time, factor 3.59)
Finished RSAPSS (0:00:57 elapsed time, 0:03:21 cpu time, factor 3.48)
Running Splay_Tree ...
Splay_Tree: theory Tree
Statecharts: theory SA
Statecharts: theory HA
Splay_Tree: theory Splay_Tree
Statecharts: theory HAOps
Statecharts: theory HASem
Statecharts: theory HAKripke
Statecharts: theory CarAudioSystem
Timing Splay_Tree (4 threads, 41.531s elapsed time, 85.348s cpu time, 0.668s GC time, factor 2.06)
Finished Splay_Tree (0:00:44 elapsed time, 0:01:27 cpu time, factor 1.99)
Running Probabilistic_System_Zoo-Non_BNFs ...
Probabilistic_System_Zoo-Non_BNFs: theory Eisbach
Probabilistic_System_Zoo-Non_BNFs: theory Order_Union
Probabilistic_System_Zoo-Non_BNFs: theory Cardinal_Notations
Probabilistic_System_Zoo-Non_BNFs: theory Fun_More
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
Timing Statecharts (4 threads, 53.674s elapsed time, 187.900s cpu time, 2.828s GC time, factor 3.50)
Finished Statecharts (0:00:56 elapsed time, 0:03:10 cpu time, factor 3.39)
Running VectorSpace ...
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
VectorSpace: theory RingModuleFacts
VectorSpace: theory FunctionLemmas
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
VectorSpace: theory MonoidSums
Probabilistic_System_Zoo-Non_BNFs: theory Nonempty_Bounded_Set
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_Hierarchy
VectorSpace: theory LinearCombinations
VectorSpace: theory SumSpaces
VectorSpace: theory VectorSpace
Probabilistic_System_Zoo-Non_BNFs: theory Vardi
Probabilistic_System_Zoo-Non_BNFs: theory Vardi_Counterexample
Probabilistic_System_Zoo-Non_BNFs: theory Finitely_Bounded_Set_Counterexample
Timing Probabilistic_System_Zoo-Non_BNFs (4 threads, 51.724s elapsed time, 168.124s cpu time, 5.968s GC time, factor 3.25)
Finished Probabilistic_System_Zoo-Non_BNFs (0:00:57 elapsed time, 0:02:53 cpu time, factor 3.03)
Running pGCL ...
Timing VectorSpace (4 threads, 49.983s elapsed time, 148.168s cpu time, 3.536s GC time, factor 2.96)
Finished VectorSpace (0:00:53 elapsed time, 0:02:31 cpu time, factor 2.84)
Running PCF ...
pGCL: theory Misc
pGCL: theory Expectations
PCF: theory Dual_Lattice
PCF: theory Nat_Discrete
PCF: theory Product_plus
PCF: theory Product_Order
pGCL: theory Transformers
PCF: theory Basis
pGCL: theory Induction
PCF: theory Logical_Relations
pGCL: theory Embedding
pGCL: theory Healthiness
PCF: theory PCF
pGCL: theory Continuity
pGCL: theory LoopInduction
pGCL: theory Sublinearity
pGCL: theory WellDefined
pGCL: theory Algebra
pGCL: theory Determinism
pGCL: theory Loops
pGCL: theory StructuredReasoning
pGCL: theory Automation
pGCL: theory Termination
pGCL: theory pGCL
PCF: theory Continuations
pGCL: theory LoopExamples
pGCL: theory Monty
pGCL: theory Primitives
PCF: theory OpSem
Timing pGCL (4 threads, 49.119s elapsed time, 187.480s cpu time, 2.528s GC time, factor 3.82)
Finished pGCL (0:00:53 elapsed time, 0:03:11 cpu time, factor 3.60)
Timing PCF (4 threads, 48.240s elapsed time, 144.492s cpu time, 3.088s GC time, factor 3.00)
Finished PCF (0:00:51 elapsed time, 0:02:27 cpu time, factor 2.88)
Running POPLmark-deBruijn ...
Running Parity_Game ...
POPLmark-deBruijn: theory Basis
POPLmark-deBruijn: theory POPLmark
POPLmark-deBruijn: theory POPLmarkRecord
Parity_Game: theory MoreCoinductiveList
Parity_Game: theory ParityGame
Parity_Game: theory Strategy
Parity_Game: theory AttractingStrategy
Parity_Game: theory WellOrderedStrategy
Parity_Game: theory WinningStrategy
Parity_Game: theory WinningRegion
Parity_Game: theory Attractor
Parity_Game: theory UniformStrategy
Parity_Game: theory AttractorInductive
Parity_Game: theory AttractorStrategy
Parity_Game: theory PositionalDeterminacy
POPLmark-deBruijn: theory POPLmarkRecordCtxt
POPLmark-deBruijn: theory Execute
Timing POPLmark-deBruijn (4 threads, 22.966s elapsed time, 74.248s cpu time, 2.624s GC time, factor 3.23)
Finished POPLmark-deBruijn (0:00:28 elapsed time, 0:01:19 cpu time, factor 2.78)
Running Perfect-Number-Thm ...
Timing Parity_Game (4 threads, 23.352s elapsed time, 75.780s cpu time, 1.388s GC time, factor 3.25)
Finished Parity_Game (0:00:30 elapsed time, 0:01:22 cpu time, factor 2.72)
Running Polynomial_Interpolation ...
Perfect-Number-Thm: theory Primes
Perfect-Number-Thm: theory Infinite_Set
Perfect-Number-Thm: theory Exponent
Perfect-Number-Thm: theory PerfectBasics
Perfect-Number-Thm: theory Sigma
Polynomial_Interpolation: theory Adhoc_Overloading
Polynomial_Interpolation: theory Infinite_Set
Polynomial_Interpolation: theory More_List
Polynomial_Interpolation: theory Sqrt_Babylonian_Auxiliary
Polynomial_Interpolation: theory Monad_Syntax
Perfect-Number-Thm: theory Perfect
Polynomial_Interpolation: theory Polynomial
Timing Perfect-Number-Thm (4 threads, 7.859s elapsed time, 28.208s cpu time, 0.216s GC time, factor 3.59)
Finished Perfect-Number-Thm (0:00:10 elapsed time, 0:00:30 cpu time, factor 2.98)
Running Polynomials ...
Polynomial_Interpolation: theory Divmod_Int
Polynomial_Interpolation: theory Improved_Code_Equations
Polynomial_Interpolation: theory Neville_Aitken_Interpolation
Polynomial_Interpolation: theory Euclidean_Algorithm
Polynomial_Interpolation: theory Missing_Unsorted
Polynomials: theory Utility
Polynomial_Interpolation: theory Is_Rat_To_Rat
Polynomial_Interpolation: theory Ring_Hom
Polynomials: theory Polynomials
Polynomial_Interpolation: theory Missing_Polynomial
Polynomials: theory NZM
Polynomial_Interpolation: theory Lagrange_Interpolation
Polynomial_Interpolation: theory Ring_Hom_Poly
Polynomial_Interpolation: theory Newton_Interpolation
Polynomial_Interpolation: theory Polynomial_Interpolation
Timing Polynomials (4 threads, 19.696s elapsed time, 47.280s cpu time, 1.296s GC time, factor 2.40)
Finished Polynomials (0:00:22 elapsed time, 0:00:50 cpu time, factor 2.22)
Running Pop_Refinement ...
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 Polynomial_Interpolation (4 threads, 33.842s elapsed time, 111.684s cpu time, 2.584s GC time, factor 3.30)
Finished Polynomial_Interpolation (0:00:36 elapsed time, 0:01:54 cpu time, factor 3.14)
Running Possibilistic_Noninterference ...
Possibilistic_Noninterference: theory MyTactics
Possibilistic_Noninterference: theory Interface
Possibilistic_Noninterference: theory Bisim
Possibilistic_Noninterference: theory Language_Semantics
Possibilistic_Noninterference: theory During_Execution
Timing Pop_Refinement (4 threads, 11.266s elapsed time, 32.044s cpu time, 0.752s GC time, factor 2.84)
Finished Pop_Refinement (0:00:13 elapsed time, 0:00:34 cpu time, factor 2.50)
Running Presburger-Automata ...
Possibilistic_Noninterference: theory After_Execution
Possibilistic_Noninterference: theory Compositionality
Presburger-Automata: theory DFS
Presburger-Automata: theory Presburger_Automata
Possibilistic_Noninterference: theory Syntactic_Criteria
Possibilistic_Noninterference: theory Concrete
Timing Possibilistic_Noninterference (4 threads, 34.979s elapsed time, 110.932s cpu time, 3.180s GC time, factor 3.17)
Finished Possibilistic_Noninterference (0:00:37 elapsed time, 0:01:53 cpu time, factor 3.02)
Running Priority_Queue_Braun ...
Priority_Queue_Braun: theory Tree
Priority_Queue_Braun: theory Multiset
Presburger-Automata: theory Exec
Timing Presburger-Automata (4 threads, 31.908s elapsed time, 108.432s cpu time, 2.476s GC time, factor 3.40)
Finished Presburger-Automata (0:00:37 elapsed time, 0:01:54 cpu time, factor 3.03)
Running Program-Conflict-Analysis ...
Priority_Queue_Braun: theory Tree_Multiset
Priority_Queue_Braun: theory Priority_Queue_Braun
Program-Conflict-Analysis: theory Misc
Program-Conflict-Analysis: theory Interleave
Timing Priority_Queue_Braun (4 threads, 16.795s elapsed time, 50.704s cpu time, 1.412s GC time, factor 3.02)
Finished Priority_Queue_Braun (0:00:19 elapsed time, 0:00:53 cpu time, factor 2.75)
Running RIPEMD-160-SPARK ...
Program-Conflict-Analysis: theory LTS
Program-Conflict-Analysis: theory ConsInterleave
Program-Conflict-Analysis: theory Flowgraph
Program-Conflict-Analysis: theory ThreadTracking
Program-Conflict-Analysis: theory AcquisitionHistory
RIPEMD-160-SPARK: theory RIPEMD_160_SPARK
Timing RIPEMD-160-SPARK (4 threads, 2.001s elapsed time, 3.424s cpu time, 0.000s GC time, factor 1.71)
Finished RIPEMD-160-SPARK (0:00:10 elapsed time, 0:00:06 cpu time, factor 0.59)
Running Ramsey-Infinite ...
Program-Conflict-Analysis: theory Semantics
Ramsey-Infinite: theory Infinite_Set
Ramsey-Infinite: theory Ramsey
Program-Conflict-Analysis: theory Normalization
Program-Conflict-Analysis: theory ConstraintSystems
Timing Ramsey-Infinite (4 threads, 7.377s elapsed time, 11.700s cpu time, 0.156s GC time, factor 1.59)
Finished Ramsey-Infinite (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.43)
Running Rank_Nullity_Theorem ...
Program-Conflict-Analysis: theory MainResult
Rank_Nullity_Theorem: theory Bit
Rank_Nullity_Theorem: theory Dual_Order
Rank_Nullity_Theorem: theory Generalizations
Rank_Nullity_Theorem: theory Mod_Type
Rank_Nullity_Theorem: theory Miscellaneous
Rank_Nullity_Theorem: theory Fundamental_Subspaces
Timing Program-Conflict-Analysis (4 threads, 37.828s elapsed time, 105.576s cpu time, 3.832s GC time, factor 2.79)
Finished Program-Conflict-Analysis (0:00:43 elapsed time, 0:01:58 cpu time, factor 2.73)
Running Recursion-Theory-I ...
Rank_Nullity_Theorem: theory Dim_Formula
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
Timing Rank_Nullity_Theorem (4 threads, 19.651s elapsed time, 69.324s cpu time, 1.360s GC time, factor 3.53)
Finished Rank_Nullity_Theorem (0:00:23 elapsed time, 0:01:13 cpu time, factor 3.08)
Running RefinementReactive ...
Recursion-Theory-I: theory RecEnSet
RefinementReactive: theory Refinement
RefinementReactive: theory Temporal
RefinementReactive: theory Reactive
Timing RefinementReactive (4 threads, 13.637s elapsed time, 37.128s cpu time, 0.460s GC time, factor 2.72)
Finished RefinementReactive (0:00:16 elapsed time, 0:00:39 cpu time, factor 2.45)
Running Residuated_Lattices ...
Timing Recursion-Theory-I (4 threads, 25.905s elapsed time, 94.392s cpu time, 1.708s GC time, factor 3.64)
Finished Recursion-Theory-I (0:00:28 elapsed time, 0:01:36 cpu time, factor 3.40)
Running Ribbon_Proofs ...
Residuated_Lattices: theory Residuated_Lattices
Ribbon_Proofs: theory JHelper
Ribbon_Proofs: theory Finite_Map
Ribbon_Proofs: theory Ribbons_Basic
Ribbon_Proofs: theory Proofchain
Ribbon_Proofs: theory Ribbons_Interfaces
Ribbon_Proofs: theory Ribbons_Graphical
Ribbon_Proofs: theory Ribbons_Stratified
Ribbon_Proofs: theory Ribbons_Graphical_Soundness
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 Ribbon_Proofs (4 threads, 20.812s elapsed time, 45.276s cpu time, 1.860s GC time, factor 2.18)
Finished Ribbon_Proofs (0:00:26 elapsed time, 0:00:50 cpu time, factor 1.92)
Running Robbins-Conjecture ...
Robbins-Conjecture: theory Robbins_Conjecture
Timing Residuated_Lattices (4 threads, 32.484s elapsed time, 68.344s cpu time, 1.216s GC time, factor 2.10)
Finished Residuated_Lattices (0:00:37 elapsed time, 0:01:12 cpu time, factor 1.95)
Running Roy_Floyd_Warshall ...
Roy_Floyd_Warshall: theory Roy_Floyd_Warshall
Timing Roy_Floyd_Warshall (4 threads, 1.568s elapsed time, 3.560s cpu time, 0.000s GC time, factor 2.27)
Finished Roy_Floyd_Warshall (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.53)
Running SIFPL ...
Timing Robbins-Conjecture (4 threads, 10.225s elapsed time, 32.780s cpu time, 0.336s GC time, factor 3.21)
Finished Robbins-Conjecture (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.76)
Running Secondary_Sylow ...
SIFPL: theory IMP
SIFPL: theory Lattice
SIFPL: theory OBJ
Secondary_Sylow: theory GroupAction
Secondary_Sylow: theory SubgroupConjugation
Secondary_Sylow: theory SndSylow
SIFPL: theory VDM
SIFPL: theory VS
SIFPL: theory HuntSands
SIFPL: theory PBIJ
SIFPL: theory VDM_OBJ
Timing Secondary_Sylow (4 threads, 7.619s elapsed time, 26.980s cpu time, 0.332s GC time, factor 3.54)
Finished Secondary_Sylow (0:00:10 elapsed time, 0:00:30 cpu time, factor 2.79)
Running SenSocialChoice ...
SIFPL: theory VS_OBJ
SIFPL: theory ContextVS
SenSocialChoice: theory FSext
SenSocialChoice: theory RPRs
SenSocialChoice: theory SCFs
SenSocialChoice: theory Arrow
SenSocialChoice: theory May
SenSocialChoice: theory Sen
SIFPL: theory ContextOBJ
Timing SenSocialChoice (4 threads, 20.312s elapsed time, 67.624s cpu time, 0.720s GC time, factor 3.33)
Finished SenSocialChoice (0:00:22 elapsed time, 0:01:10 cpu time, factor 3.06)
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
Separation_Algebra: theory Abstract_Separation_D
Timing SIFPL (4 threads, 45.611s elapsed time, 126.740s cpu time, 3.892s GC time, factor 2.78)
Finished SIFPL (0:00:48 elapsed time, 0:02:09 cpu time, factor 2.68)
Running Shivers-CFA ...
Separation_Algebra: theory Separation_D
Shivers-CFA: theory Adhoc_Overloading
Shivers-CFA: theory CPSScheme
Shivers-CFA: theory FixTransform
Shivers-CFA: theory HOLCFUtils
Shivers-CFA: theory SetMap
Shivers-CFA: theory Utils
Shivers-CFA: theory Computability
Shivers-CFA: theory MapSets
Timing Separation_Algebra (4 threads, 19.591s elapsed time, 51.300s cpu time, 1.884s GC time, factor 2.62)
Finished Separation_Algebra (0:00:22 elapsed time, 0:00:54 cpu time, factor 2.40)
Running Show ...
Shivers-CFA: theory CPSUtils
Shivers-CFA: theory Eval
Shivers-CFA: theory AbsCF
Shivers-CFA: theory ExCF
Show: theory Show
Shivers-CFA: theory AbsCFComp
Shivers-CFA: theory AbsCFCorrect
Show: theory Show_Instances
Show: theory Show_Real
Show: theory Show_Complex
Shivers-CFA: theory ExCFSV
Show: theory Show_Real_Impl
Show: theory Show_Poly
Timing Show (4 threads, 6.378s elapsed time, 10.384s cpu time, 0.300s GC time, factor 1.63)
Finished Show (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.30)
Running Skew_Heap ...
Skew_Heap: theory Multiset
Skew_Heap: theory Tree
Timing Shivers-CFA (4 threads, 27.689s elapsed time, 86.912s cpu time, 2.648s GC time, factor 3.14)
Finished Shivers-CFA (0:00:30 elapsed time, 0:01:29 cpu time, factor 2.93)
Running Special_Function_Bounds ...
Skew_Heap: theory Tree_Multiset
Skew_Heap: theory Skew_Heap
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
Timing Skew_Heap (4 threads, 12.746s elapsed time, 40.968s cpu time, 1.076s GC time, factor 3.21)
Finished Skew_Heap (0:00:15 elapsed time, 0:00:43 cpu time, factor 2.83)
Running Stern_Brocot ...
Stern_Brocot: theory Cotree
Stern_Brocot: theory Cotree_Algebra
Stern_Brocot: theory Stern_Brocot_Tree
Stern_Brocot: theory Bird_Tree
Timing Stern_Brocot (4 threads, 10.056s elapsed time, 23.944s cpu time, 0.336s GC time, factor 2.38)
Finished Stern_Brocot (0:00:17 elapsed time, 0:00:30 cpu time, factor 1.75)
Running Stream-Fusion ...
Stream-Fusion: theory Int_Discrete
Stream-Fusion: theory LazyList
Stream-Fusion: theory Stream
Timing Special_Function_Bounds (4 threads, 25.042s elapsed time, 82.564s cpu time, 0.824s GC time, factor 3.30)
Finished Special_Function_Bounds (0:00:31 elapsed time, 0:01:28 cpu time, factor 2.82)
Running Strong_Security ...
Stream-Fusion: theory StreamFusion
Strong_Security: theory Types
Strong_Security: theory Expr
Strong_Security: theory MWLf
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
Strong_Security: theory Language_Composition
Strong_Security: theory Type_System
Strong_Security: theory Type_System_example
Timing Stream-Fusion (4 threads, 12.373s elapsed time, 20.252s cpu time, 0.240s GC time, factor 1.64)
Finished Stream-Fusion (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.51)
Running Sturm_Tarski ...
Sturm_Tarski: theory More_List
Sturm_Tarski: theory Infinite_Set
Sturm_Tarski: theory Polynomial
Sturm_Tarski: theory Polynomial_GCD_euclidean
Sturm_Tarski: theory PolyMisc
Sturm_Tarski: theory Sturm_Tarski
Timing Strong_Security (4 threads, 21.913s elapsed time, 66.900s cpu time, 1.816s GC time, factor 3.05)
Finished Strong_Security (0:00:24 elapsed time, 0:01:09 cpu time, factor 2.83)
Running Stuttering_Equivalence ...
Stuttering_Equivalence: theory Samplers
Stuttering_Equivalence: theory StutterEquivalence
Stuttering_Equivalence: theory PLTL
Timing Sturm_Tarski (4 threads, 23.909s elapsed time, 77.216s cpu time, 1.136s GC time, factor 3.23)
Finished Sturm_Tarski (0:00:26 elapsed time, 0:01:19 cpu time, factor 3.03)
Running TLA ...
TLA: theory Intensional
TLA: theory Sequence
Timing Stuttering_Equivalence (4 threads, 5.378s elapsed time, 19.348s cpu time, 0.256s GC time, factor 3.60)
Finished Stuttering_Equivalence (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.20)
Running Topology ...
TLA: theory Semantics
TLA: theory PreFormulas
TLA: theory Rules
TLA: theory Liveness
TLA: theory State
TLA: theory Buffer
TLA: theory Even
TLA: theory Inc
Topology: theory Topology
Topology: theory LList_Topology
Timing Topology (4 threads, 8.895s elapsed time, 31.932s cpu time, 0.472s GC time, factor 3.59)
Finished Topology (0:00:16 elapsed time, 0:00:38 cpu time, factor 2.32)
Running TortoiseHare ...
TortoiseHare: theory While_Combinator
Timing TLA (4 threads, 19.968s elapsed time, 67.868s cpu time, 1.364s GC time, factor 3.40)
Finished TLA (0:00:22 elapsed time, 0:01:10 cpu time, factor 3.12)
Running Transitive-Closure ...
TortoiseHare: theory Basis
TortoiseHare: theory Brent
TortoiseHare: theory TortoiseHare
Timing TortoiseHare (4 threads, 7.731s elapsed time, 22.528s cpu time, 0.144s GC time, factor 2.91)
Finished TortoiseHare (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.46)
Running Transitive-Closure-II ...
Transitive-Closure-II: theory While_Combinator
Transitive-Closure-II: theory Regular_Set
Transitive-Closure: theory Transitive_Closure_Impl
Transitive-Closure: theory Utility
Transitive-Closure-II: theory Regular_Exp
Transitive-Closure: theory RBT_Map_Set_Extension
Transitive-Closure: theory Transitive_Closure_List_Impl
Transitive-Closure: theory Finite_Transitive_Closure_Simprocs
Transitive-Closure: theory Transitive_Closure_RBT_Impl
Transitive-Closure-II: theory NDerivative
Transitive-Closure-II: theory Relation_Interpretation
Timing Transitive-Closure (4 threads, 7.584s elapsed time, 20.680s cpu time, 0.232s GC time, factor 2.73)
Finished Transitive-Closure (0:00:17 elapsed time, 0:00:30 cpu time, factor 1.74)
Running Triangle ...
Triangle: theory Angles
Triangle: theory Triangle
Transitive-Closure-II: theory Equivalence_Checking
Transitive-Closure-II: theory Regexp_Method
Transitive-Closure-II: theory RTrancl
Timing Triangle (4 threads, 6.460s elapsed time, 12.256s cpu time, 0.084s GC time, factor 1.90)
Finished Triangle (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.56)
Running Tycon ...
Timing Transitive-Closure-II (4 threads, 19.686s elapsed time, 44.372s cpu time, 1.412s GC time, factor 2.25)
Finished Transitive-Closure-II (0:00:22 elapsed time, 0:00:51 cpu time, factor 2.34)
Running Valuation ...
Tycon: theory Coerce
Tycon: theory TypeApp
Tycon: theory Functor
Tycon: theory Monad
Tycon: theory Binary_Tree_Monad
Tycon: theory Lift_Monad
Tycon: theory Monad_Zero
Tycon: theory Monad_Plus
Tycon: theory Writer_Monad
Tycon: theory Error_Monad
Tycon: theory Resumption_Transformer
Tycon: theory Monad_Zero_Plus
Tycon: theory Lazy_List_Monad
Tycon: theory Maybe_Monad
Tycon: theory Error_Transformer
Tycon: theory State_Transformer
Tycon: theory Writer_Transformer
Valuation: theory Valuation1
Timing Tycon (4 threads, 9.438s elapsed time, 28.656s cpu time, 0.268s GC time, factor 3.04)
Finished Tycon (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.55)
Running Verified-Prover ...
Verified-Prover: theory Prover
Valuation: theory Valuation2
Valuation: theory Valuation3
Timing Verified-Prover (4 threads, 10.034s elapsed time, 20.144s cpu time, 0.324s GC time, factor 2.01)
Finished Verified-Prover (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.81)
Running VolpanoSmith ...
VolpanoSmith: theory Semantics
VolpanoSmith: theory secTypes
VolpanoSmith: theory Execute
Timing VolpanoSmith (4 threads, 13.417s elapsed time, 35.692s cpu time, 0.780s GC time, factor 2.66)
Finished VolpanoSmith (0:00:15 elapsed time, 0:00:38 cpu time, factor 2.40)
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
Timing Valuation (4 threads, 44.096s elapsed time, 147.780s cpu time, 2.904s GC time, factor 3.35)
Finished Valuation (0:00:51 elapsed time, 0:02:34 cpu time, factor 2.98)
Running Well_Quasi_Orders ...
WHATandWHERE_Security: theory Type_System
WHATandWHERE_Security: theory Type_System_example
Well_Quasi_Orders: theory Regular_Set
Well_Quasi_Orders: theory Restricted_Predicates
Well_Quasi_Orders: theory Seq
Well_Quasi_Orders: theory Open_Induction
Well_Quasi_Orders: theory Regular_Exp
Well_Quasi_Orders: theory NDerivative
Well_Quasi_Orders: theory Relation_Interpretation
Well_Quasi_Orders: theory Equivalence_Checking
Well_Quasi_Orders: theory Regexp_Method
Well_Quasi_Orders: theory Infinite_Sequences
Well_Quasi_Orders: theory Least_Enum
Well_Quasi_Orders: theory Multiset_Extension
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 WHATandWHERE_Security (4 threads, 39.861s elapsed time, 137.680s cpu time, 3.300s GC time, factor 3.45)
Finished WHATandWHERE_Security (0:00:42 elapsed time, 0:02:20 cpu time, factor 3.31)
Running WorkerWrapper ...
WorkerWrapper: theory Maybe
WorkerWrapper: theory Nats
WorkerWrapper: theory LList
WorkerWrapper: theory FixedPointTheorems
Timing Well_Quasi_Orders (4 threads, 31.716s elapsed time, 97.144s cpu time, 2.940s GC time, factor 3.06)
Finished Well_Quasi_Orders (0:00:37 elapsed time, 0:01:48 cpu time, factor 2.87)
Running XML ...
WorkerWrapper: theory WorkerWrapper
WorkerWrapper: theory CounterExample
WorkerWrapper: theory Last
WorkerWrapper: theory Streams
WorkerWrapper: theory WorkerWrapperNew
WorkerWrapper: theory Accumulator
WorkerWrapper: theory Backtracking
WorkerWrapper: theory Continuations
WorkerWrapper: theory Nub
WorkerWrapper: theory UnboxedNats
XML: theory Adhoc_Overloading
XML: theory Char_ord
XML: theory Derive_Manager
XML: theory Generator_Aux
XML: theory Partial_Function_MR
XML: theory Error_Syntax
XML: theory Monad_Syntax
XML: theory Show
XML: theory Error_Monad
XML: theory Strict_Sum
XML: theory Parser_Monad
XML: theory Xml
XML: theory Xmlt
Timing WorkerWrapper (4 threads, 23.822s elapsed time, 55.492s cpu time, 1.232s GC time, factor 2.33)
Finished WorkerWrapper (0:00:26 elapsed time, 0:00:58 cpu time, factor 2.18)
Running Cartan_FP ...
Cartan_FP: theory Cartan
Timing Cartan_FP (4 threads, 4.944s elapsed time, 15.668s cpu time, 0.112s GC time, factor 3.17)
Finished Cartan_FP (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.21)
Running Lifting_Definition_Option ...
Timing XML (4 threads, 26.271s elapsed time, 47.572s cpu time, 2.408s GC time, factor 1.81)
Finished XML (0:00:28 elapsed time, 0:00:50 cpu time, factor 1.74)
Running Partial_Function_MR ...
Lifting_Definition_Option: theory Lifting_Definition_Option_Examples
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 Lifting_Definition_Option (4 threads, 3.741s elapsed time, 5.452s cpu time, 0.000s GC time, factor 1.46)
Finished Lifting_Definition_Option (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.27)
Running PropResPI ...
PropResPI: theory Propositional_Resolution
Timing Partial_Function_MR (4 threads, 9.087s elapsed time, 13.712s cpu time, 0.316s GC time, factor 1.51)
Finished Partial_Function_MR (0:00:11 elapsed time, 0:00:15 cpu time, factor 1.40)
Running Real_Impl ...
PropResPI: theory Prime_Implicates
Real_Impl: theory Primes
Real_Impl: theory Derive_Manager
Real_Impl: theory Generator_Aux
Real_Impl: theory Multiset
Real_Impl: theory Show
Real_Impl: theory Cong
Real_Impl: theory Show_Instances
Real_Impl: theory UniqueFactorization
Timing PropResPI (4 threads, 17.638s elapsed time, 55.180s cpu time, 1.132s GC time, factor 3.13)
Finished PropResPI (0:00:20 elapsed time, 0:00:57 cpu time, factor 2.86)
Running UPF ...
UPF: theory Monads
UPF: theory UPFCore
UPF: theory ElementaryPolicies
Real_Impl: theory Real_Impl_Auxiliary
Real_Impl: theory Real_Impl
Real_Impl: theory Show_Real
Real_Impl: theory Prime_Product
UPF: theory ParallelComposition
UPF: theory SeqComposition
Real_Impl: theory Real_Unique_Impl
UPF: theory Analysis
UPF: theory Normalisation
UPF: theory NormalisationTestSpecification
UPF: theory UPF
UPF: theory Service
UPF: theory ServiceExample
Timing UPF (4 threads, 31.337s elapsed time, 92.656s cpu time, 2.616s GC time, factor 2.96)
Finished UPF (0:00:33 elapsed time, 0:01:35 cpu time, factor 2.80)
Running Case_Labeling ...
Case_Labeling: theory Eisbach
Case_Labeling: theory Hoare_Logic
Timing Real_Impl (4 threads, 47.940s elapsed time, 153.172s cpu time, 2.628s GC time, factor 3.20)
Finished Real_Impl (0:00:51 elapsed time, 0:02:35 cpu time, factor 3.05)
Running Abstract_Completeness ...
Case_Labeling: theory Arith2
Case_Labeling: theory Case_Labeling
Abstract_Completeness: theory ICF_Tools
Abstract_Completeness: theory Code_Abstract_Nat
Abstract_Completeness: theory Infinite_Set
Abstract_Completeness: theory Nat_Bijection
Case_Labeling: theory Labeled_Hoare
Case_Labeling: theory Conditionals
Case_Labeling: theory Monadic_Language
Abstract_Completeness: theory Code_Target_Nat
Abstract_Completeness: theory Old_Datatype
Abstract_Completeness: theory Ord_Code_Preproc
Abstract_Completeness: theory Locale_Code
Case_Labeling: theory Labeled_Hoare_Examples
Abstract_Completeness: theory Sublist
Abstract_Completeness: theory Stream
Case_Labeling: theory Case_Labeling_Examples
Timing Case_Labeling (4 threads, 6.124s elapsed time, 17.004s cpu time, 0.256s GC time, factor 2.78)
Finished Case_Labeling (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.28)
Running Coinductive_Languages ...
Abstract_Completeness: theory Countable
Coinductive_Languages: theory Regular_Set
Abstract_Completeness: theory Countable_Set
Abstract_Completeness: theory Countable_Complete_Lattices
Coinductive_Languages: theory Coinductive_Language
Abstract_Completeness: theory Order_Continuity
Abstract_Completeness: theory Extended_Nat
Coinductive_Languages: theory CFG_Examples
Coinductive_Languages: theory Coinductive_Regular_Set
Abstract_Completeness: theory Linear_Temporal_Logic_on_Streams
Abstract_Completeness: theory FSet
Timing Coinductive_Languages (4 threads, 12.285s elapsed time, 32.724s cpu time, 0.524s GC time, factor 2.66)
Finished Coinductive_Languages (0:00:14 elapsed time, 0:00:39 cpu time, factor 2.69)
Running ConcurrentIMP ...
Abstract_Completeness: theory Abstract_Completeness
ConcurrentIMP: theory CIMP_pred
ConcurrentIMP: theory Prefix_Order
ConcurrentIMP: theory CIMP_lang
Abstract_Completeness: theory Propositional_Logic
Timing Abstract_Completeness (4 threads, 30.220s elapsed time, 88.024s cpu time, 2.316s GC time, factor 2.91)
Finished Abstract_Completeness (0:00:32 elapsed time, 0:01:30 cpu time, factor 2.77)
Running CryptoBasedCompositionalProperties ...
CryptoBasedCompositionalProperties: theory ListExtras
CryptoBasedCompositionalProperties: theory Secrecy_types
CryptoBasedCompositionalProperties: theory inout
ConcurrentIMP: theory CIMP_vcg
CryptoBasedCompositionalProperties: theory Secrecy
CryptoBasedCompositionalProperties: theory CompLocalSecrets
CryptoBasedCompositionalProperties: theory KnowledgeKeysSecrets
ConcurrentIMP: theory CIMP
ConcurrentIMP: theory CIMP_one_place_buffer_ex
ConcurrentIMP: theory CIMP_unbounded_buffer_ex
Timing CryptoBasedCompositionalProperties (4 threads, 15.810s elapsed time, 38.892s cpu time, 0.712s GC time, factor 2.46)
Finished CryptoBasedCompositionalProperties (0:00:18 elapsed time, 0:00:41 cpu time, factor 2.26)
Running FocusStreamsCaseStudies ...
FocusStreamsCaseStudies: theory ArithExtras
FocusStreamsCaseStudies: theory ListExtras
FocusStreamsCaseStudies: theory arith_hints
Timing ConcurrentIMP (4 threads, 26.857s elapsed time, 56.184s cpu time, 2.604s GC time, factor 2.09)
Finished ConcurrentIMP (0:00:32 elapsed time, 0:01:01 cpu time, factor 1.90)
Formula_Derivatives-Examples CANCELLED
Running GoedelGod ...
FocusStreamsCaseStudies: theory stream
GoedelGod: theory GoedelGod
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
FocusStreamsCaseStudies: theory Gateway
FocusStreamsCaseStudies: theory Gateway_proof_aux
FocusStreamsCaseStudies: theory Gateway_proof
Timing GoedelGod (4 threads, 10.870s elapsed time, 12.912s cpu time, 0.076s GC time, factor 1.19)
Finished GoedelGod (0:00:13 elapsed time, 0:00:16 cpu time, factor 1.27)
Running Imperative_Insertion_Sort ...
Imperative_Insertion_Sort: theory Imperative_Loops
Imperative_Insertion_Sort: theory Imperative_Insertion_Sort
Timing Imperative_Insertion_Sort (4 threads, 9.174s elapsed time, 26.052s cpu time, 0.148s GC time, factor 2.84)
Finished Imperative_Insertion_Sort (0:00:13 elapsed time, 0:00:29 cpu time, factor 2.13)
Running Nominal2 ...
Nominal2: theory Multiset
Nominal2: theory Old_Datatype
Nominal2: theory Phantom_Type
Nominal2: theory Infinite_Set
Timing FocusStreamsCaseStudies (4 threads, 28.293s elapsed time, 92.340s cpu time, 2.136s GC time, factor 3.26)
Finished FocusStreamsCaseStudies (0:00:30 elapsed time, 0:01:34 cpu time, factor 3.08)
Running Regex_Equivalence_Examples ...
Nominal2: theory Quotient_Syntax
Nominal2: theory Quotient_Option
Nominal2: theory Quotient_Product
Nominal2: theory Quotient_Set
Nominal2: theory Cardinality
Nominal2: theory Quotient_List
Nominal2: theory FinFun
Regex_Equivalence_Examples: theory Spec_Check
Regex_Equivalence_Examples: theory Examples
Nominal2: theory FSet
Regex_Equivalence_Examples: theory Benchmark
Nominal2: theory Nominal2_Base
Nominal2: theory Atoms
Nominal2: theory Eqvt
Nominal2: theory Nominal2_Abs
Nominal2: theory Nominal2_FCB
Nominal2: theory Nominal2
Timing Regex_Equivalence_Examples (4 threads, 17.510s elapsed time, 46.876s cpu time, 5.940s GC time, factor 2.68)
Finished Regex_Equivalence_Examples (0:00:25 elapsed time, 0:00:53 cpu time, factor 2.14)
Running Selection_Heap_Sort ...
Selection_Heap_Sort: theory Sort
Selection_Heap_Sort: theory RemoveMax
Timing Nominal2 (4 threads, 30.443s elapsed time, 109.084s cpu time, 3.432s GC time, factor 3.58)
Finished Nominal2 (0:00:32 elapsed time, 0:01:51 cpu time, factor 3.38)
Running Trie ...
Selection_Heap_Sort: theory Heap
Selection_Heap_Sort: theory SelectionSort_Functional
Trie: theory AList
Selection_Heap_Sort: theory HeapFunctional
Selection_Heap_Sort: theory HeapImperative
Trie: theory Trie
Trie: theory Tries
Timing Selection_Heap_Sort (4 threads, 15.019s elapsed time, 46.360s cpu time, 0.900s GC time, factor 3.09)
Finished Selection_Heap_Sort (0:00:20 elapsed time, 0:00:52 cpu time, factor 2.49)
Timing Trie (4 threads, 27.180s elapsed time, 41.264s cpu time, 0.792s GC time, factor 1.52)
Finished Trie (0:00:29 elapsed time, 0:00:43 cpu time, factor 1.47)
Unfinished session(s): Amortized_Complexity, Formula_Derivatives, Formula_Derivatives-Examples, HRB-Slicing, InformationFlowSlicing, InformationFlowSlicing_Inter, InformationFlowSlicing_Intra, Isabelle_Meta_Model, Jinja, LTL_to_DRA, List-Index, List_Update, MSO_Examples, MSO_Regex_Equivalence, Planarity_Certificates, Slicing
=== FAILED SESSIONS ===
List-Index: FAILED 2
Slicing: CANCELLED
Formula_Derivatives: FAILED 2
LTL_to_DRA: FAILED 2
Amortized_Complexity: FAILED 2
InformationFlowSlicing_Inter: CANCELLED
MSO_Regex_Equivalence: FAILED 2
InformationFlowSlicing: CANCELLED
Planarity_Certificates: FAILED 2
InformationFlowSlicing_Intra: CANCELLED
Formula_Derivatives-Examples: CANCELLED
HRB-Slicing: CANCELLED
Jinja: FAILED 2
MSO_Examples: CANCELLED
List_Update: FAILED 2
Isabelle_Meta_Model: FAILED 2
Build step 'Execute shell' marked build as failure
Finished: FAILURE