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 \ ?y then if ?x = ?y then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y = ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y \ ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?x < ?y then ?Q else ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x \ ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y \ ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x \ ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?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 \ ?y then if ?x = ?y then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y = ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y \ ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?x < ?y then ?Q else ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x \ ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y \ ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x \ ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?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: "(\p. length (snd p)) <*mlex*> (\p. length (fst p)) <*mlex*> {}" ### Rule already declared as elimination (elim) ### \?w \ ?A @@ ?B; ### \u v. ### \u \ ?A; v \ ?B; ?w = u @ v\ ### \ ?thesis\ ### \ ?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 \ 'a rexp \ bool less_rexp == less :: 'a rexp \ 'a rexp \ bool Found termination order: "(\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: "(\p. size (fst p)) <*mlex*> (\p. size (snd p)) <*mlex*> {}" Found termination order: "(\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) ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) "LEAST x. P x" :: "'a" ### Rule already declared as elimination (elim) ### \vwalk ?p ?G; ### \set ?p \ verts ?G; ### set (vwalk_arcs ?p) \ arcs_ends ?G \ ### ?p \ []\ ### \ ?P\ ### \ ?P ### Rule already declared as elimination (elim) ### \subgraph ?H ?G; ### \verts ?H \ verts ?G; arcs ?H \ arcs ?G; ### compatible ?G ?H; wf_digraph ?H; wf_digraph ?G\ ### \ ?thesis\ ### \ ?thesis ### Rule already declared as elimination (elim) ### \vpath ?p ?G; ### \vwalk ?p ?G; distinct ?p\ \ ?P\ ### \ ?P "True" :: "bool" "- \" :: "ereal" "True" :: "bool" "\" :: "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 \ bool" and invariant :: "'b \ bool" and ins :: "'a \ 'b \ 'b" and memb :: "'a \ 'b \ bool" and empt :: "'b" and nodeAbs :: "'a \ 'c" assumes "DFS succs isNode invariant ins memb empt nodeAbs" locale DFS = fixes succs :: "'a \ 'a list" and isNode :: "'a \ bool" and invariant :: "'b \ bool" and ins :: "'a \ 'b \ 'b" and memb :: "'a \ 'b \ bool" and empt :: "'b" and nodeAbs :: "'a \ '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: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" locale reduced_bdt_checkers = fixes ifex_of :: "'b \ 'a ifex" and val :: "'b \ ('a \ bool) \ 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: "(\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