22:32:22 Started by upstream project "afp-repo" build number 653

22:32:22 originally caused by:

22:32:22 Started by an SCM change

22:32:22 [EnvInject] - Loading node environment variables.

22:32:22 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/afp-repo-afp

22:32:22 [afp-repo-afp] $ hg showconfig paths.default

22:32:22 [afp-repo-afp] $ hg pull --rev default

22:32:23 pulling from http://isabelle.in.tum.de/repos/isabelle/

22:32:23 searching for changes

22:32:23 adding changesets

22:32:23 adding manifests

22:32:23 adding file changes

22:32:23 added 9 changesets with 17 changes to 17 files

22:32:23 (run 'hg update' to get a working copy)

22:32:23 [afp-repo-afp] $ hg update --clean --rev default

22:32:23 17 files updated, 0 files merged, 0 files removed, 0 files unresolved

22:32:23 [afp-repo-afp] $ hg log --rev . --template {node}

22:32:23 [afp-repo-afp] $ hg log --rev . --template {rev}

22:32:23 [afp] $ hg showconfig paths.default

22:32:23 [afp] $ hg pull --rev 924248d56075904e4b9fee16826d05db55959315

22:32:25 pulling from https://bitbucket.org/isa-afp/afp-devel/

22:32:25 searching for changes

22:32:25 adding changesets

22:32:25 adding manifests

22:32:25 adding file changes

22:32:25 added 1 changesets with 1 changes to 1 files

22:32:25 (run 'hg update' to get a working copy)

22:32:25 [afp] $ hg update --clean --rev 924248d56075904e4b9fee16826d05db55959315

22:32:25 326 files updated, 0 files merged, 0 files removed, 0 files unresolved

22:32:25 [afp] $ hg --config extensions.purge= clean --all

22:32:25 [afp] $ hg log --rev . --template {node}

22:32:25 [afp] $ hg log --rev . --template {rev}

22:32:25 [afp] $ hg id --branch

22:32:25 No emails were triggered.

22:32:25 [afp-repo-afp] $ /bin/sh -xe /tmp/hudson424510642759953243.sh

22:32:25 + Admin/jenkins/run_build afp

22:32:25 + set -e

22:32:25 + PROFILE=afp

22:32:25 + shift

22:32:25 + bin/isabelle components -a

22:32:25 + bin/isabelle jedit -bf

22:32:25 ### Building Isabelle/Scala ...

22:33:16 ### Building Isabelle/jEdit ...

22:33:34 + bin/isabelle ci_build_afp

22:33:40

22:33:40 === CONFIGURATION ===

22:33:40

22:33:40 ISABELLE_BUILD_OPTIONS=""

22:33:40

22:33:40 ML_PLATFORM="x86_64-linux"

22:33:40 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

22:33:40 ML_SYSTEM="polyml-5.6"

22:33:40 ML_OPTIONS="-H 4000 --maxheap 8G"

22:33:40

22:33:40 === BUILD ===

22:33:40

22:33:40 Build started at Sun, 18 Dec 2016 21:33:40 GMT

22:33:40 Isabelle id 8edca3465758

22:33:40 AFP id 924248d56075

22:33:40

22:33:40 === LOG ===

22:33:40

22:33:41 Session Pure/Pure

22:33:41 Session HOL/HOL (main)

22:33:42 Session AFP/AVL-Trees (AFP)

22:33:42 Session AFP/AWN (AFP)

22:33:42 Session AFP/Abortable_Linearizable_Modules (AFP)

22:33:42 Session AFP/Abstract-Hoare-Logics (AFP)

22:33:42 Session AFP/Abstract-Rewriting (AFP)

22:33:42 Session AFP/Decreasing-Diagrams (AFP)

22:33:42 Session AFP/Decreasing-Diagrams-II (AFP)

22:33:42 Session AFP/Matrix (AFP)

22:33:42 Session AFP/Matrix_Tensor (AFP)

22:33:42 Session AFP/Knot_Theory (AFP)

22:33:42 Session AFP/Polynomials (AFP)

22:33:42 Session AFP/Groebner_Bases (AFP)

22:33:42 Session AFP/Abstract_Completeness (AFP)

22:33:42 Session AFP/Allen_Calculus (AFP)

22:33:42 Session AFP/Automatic_Refinement (AFP)

22:33:43 Session AFP/Refine_Monadic (AFP)

22:33:43 Session AFP/Collections (AFP)

22:33:43 Session AFP/CAVA_Base (AFP)

22:33:43 Session AFP/CAVA_Automata (AFP)

22:33:43 Session AFP/DFS_Framework (AFP)

22:33:43 Session AFP/Gabow_SCC (AFP)

22:33:43 Session AFP/LTL_to_GBA (AFP)

22:33:43 Session AFP/CAVA_buildchain1 (AFP)

22:33:43 Session AFP/CAVA_buildchain3 (AFP)

22:33:43 Session AFP/CAVA_LTL_Modelchecker (AFP)

22:33:43 Session AFP/Promela (AFP)

22:33:43 Session AFP/Collections_Examples (AFP)

22:33:43 Session AFP/Dijkstra_Shortest_Path (AFP)

22:33:43 Session AFP/Formal_SSA (AFP)

22:33:43 Session AFP/Sepref_Prereq (AFP)

22:33:43 Session AFP/Refine_Imperative_HOL (AFP)

22:33:43 Session AFP/Sepref_Basic (AFP)

22:33:43 Session AFP/Sepref_IICF (AFP)

22:33:43 Session AFP/Edka_Base (AFP)

22:33:43 Session AFP/EdmondsKarp_Maxflow (AFP)

22:33:43 Session AFP/Transitive-Closure (AFP)

22:33:43 Session AFP/Tree-Automata (AFP)

22:33:43 Session AFP/BinarySearchTree (AFP)

22:33:43 Session AFP/Binomial-Queues (AFP)

22:33:43 Session AFP/Bondy (AFP)

22:33:43 Session AFP/Bounded_Deducibility_Security (AFP)

22:33:43 Session AFP/BytecodeLogicJmlTypes (AFP)

22:33:43 Session AFP/CISC-Kernel (AFP)

22:33:43 Session AFP/CYK (AFP)

22:33:43 Session AFP/Card_Number_Partitions (AFP)

22:33:44 Session AFP/Case_Labeling (AFP)

22:33:44 Session AFP/Cauchy (AFP)

22:33:44 Session AFP/Sqrt_Babylonian (AFP)

22:33:44 Session AFP/Real_Impl (AFP)

22:33:44 Session AFP/Certification_Monads (AFP)

22:33:44 Session AFP/ClockSynchInst (AFP)

22:33:44 Session AFP/Coinductive_Languages (AFP)

22:33:44 Session AFP/Compiling-Exceptions-Correctly (AFP)

22:33:44 Session AFP/Completeness (AFP)

22:33:44 Session AFP/ComponentDependencies (AFP)

22:33:44 Session AFP/Consensus_Refined (AFP)

22:33:44 Session AFP/CryptoBasedCompositionalProperties (AFP)

22:33:44 Session AFP/DPT-SAT-Solver (AFP)

22:33:44 Session AFP/DataRefinementIBP (AFP)

22:33:44 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

22:33:44 Session AFP/Dependent_SIFUM_Refinement (AFP)

22:33:44 Session AFP/Depth-First-Search (AFP)

22:33:44 Session AFP/Derangements (AFP)

22:33:44 Session AFP/Discrete_Summation (AFP)

22:33:44 Session AFP/Card_Partitions (AFP)

22:33:44 Session AFP/DiskPaxos (AFP)

22:33:44 Session AFP/Encodability_Process_Calculi (AFP)

22:33:44 Session AFP/Euler_Partition (AFP)

22:33:45 Session AFP/Example-Submission (AFP)

22:33:45 Session AFP/FFT (AFP)

22:33:45 Session AFP/FLP (AFP)

22:33:45 Session AFP/FeatherweightJava (AFP)

22:33:45 Session AFP/Featherweight_OCL (AFP)

22:33:45 Session AFP/FileRefinement (AFP)

22:33:45 Session AFP/FinFun (AFP)

22:33:45 Session AFP/Finite_Automata_HF (AFP)

22:33:45 Session AFP/FocusStreamsCaseStudies (AFP)

22:33:45 Session AFP/Free-Groups (AFP)

22:33:45 Session AFP/FunWithFunctions (AFP)

22:33:45 Session AFP/FunWithTilings (AFP)

22:33:45 Session AFP/GPU_Kernel_PL (AFP)

22:33:45 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

22:33:45 Session AFP/GenClock (AFP)

22:33:45 Session AFP/General-Triangle (AFP)

22:33:45 Session AFP/GoedelGod (AFP)

22:33:45 Session AFP/GraphMarkingIBP (AFP)

22:33:45 Session AFP/Graph_Theory (AFP)

22:33:45 Session AFP/ShortestPath (AFP)

22:33:45 Session HOL/HOL-Algebra (main timing)

22:33:45 Session AFP/JNF-HOL-Lib (AFP)

22:33:46 Session AFP/JNF-AFP-Lib (AFP)

22:33:46 Session AFP/Jordan_Normal_Form (AFP)

22:33:46 Session AFP/Pre_Perron_Frobenius (AFP)

22:33:46 Session AFP/Perron_Frobenius (AFP)

22:33:46 Session AFP/Pre_Polynomial_Factorization (AFP)

22:33:46 Session AFP/Polynomial_Factorization (AFP)

22:33:46 Session AFP/Pre_BZ (AFP)

22:33:46 Session AFP/Berlekamp_Zassenhaus (AFP)

22:33:46 Session AFP/Pre_Algebraic_Numbers (AFP)

22:33:46 Session AFP/Algebraic_Numbers (AFP)

22:33:46 Session AFP/Algebraic_Numbers_Lib (AFP)

22:33:46 Session AFP/Jordan_Hoelder (AFP)

22:33:46 Session AFP/Perfect-Number-Thm (AFP)

22:33:46 Session AFP/Secondary_Sylow (AFP)

22:33:46 Session AFP/VectorSpace (AFP)

22:33:46 Session HOL/HOL-Analysis (main timing)

22:33:47 Session AFP/Affine_Arithmetic (AFP)

22:33:47 Session AFP/Cartan_FP (AFP)

22:33:47 Session AFP/Cayley_Hamilton (AFP)

22:33:47 Session AFP/Chord_Segments (AFP)

22:33:47 Session AFP/Echelon_Form (AFP)

22:33:47 Session AFP/Hermite (AFP)

22:33:47 Session AFP/Gauss_Jordan (AFP)

22:33:47 Session HOL/HOL-Probability (timing)

22:33:47 Session AFP/Applicative_Lifting (AFP)

22:33:47 Session AFP/Stern_Brocot (AFP)

22:33:47 Session AFP/Deep_Learning_Lib (AFP)

22:33:47 Session AFP/Deep_Learning (AFP)

22:33:47 Session AFP/Density_Compiler (AFP)

22:33:47 Session AFP/Ergodic_Theory (AFP)

22:33:47 Session AFP/Fisher_Yates (AFP)

22:33:47 Session AFP/Girth_Chromatic (AFP)

22:33:47 Session AFP/List_Update (AFP)

22:33:47 Session AFP/Lp (AFP)

22:33:47 Session AFP/MFMC_Countable (AFP)

22:33:47 Session AFP/Markov_Models (AFP)

22:33:47 Session AFP/Probabilistic_Noninterference (AFP)

22:33:47 Session AFP/Probabilistic_System_Zoo (AFP)

22:33:47 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

22:33:48 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

22:33:48 Session AFP/Randomised_Social_Choice (AFP)

22:33:48 Session AFP/SDS_Impossibility (AFP)

22:33:48 Session AFP/Source_Coding_Theorem (AFP)

22:33:48 Session AFP/UpDown_Scheme (AFP)

22:33:48 Session AFP/Landau_Analysis (AFP)

22:33:48 Session AFP/Akra_Bazzi (AFP)

22:33:48 Session AFP/Catalan_Numbers (AFP)

22:33:48 Session AFP/Stirling_Formula (AFP)

22:33:48 Session AFP/Lower_Semicontinuous (AFP)

22:33:48 Session AFP/Ordinary_Differential_Equations (AFP)

22:33:48 Session AFP/HOL-ODE (AFP)

22:33:48 Session AFP/HOL-ODE-Refinement (AFP)

22:33:49 Session AFP/HOL-ODE-Numerics (AFP)

22:33:49 Session AFP/Prime_Harmonic_Series (AFP)

22:33:49 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

22:33:49 Session AFP/Ptolemys_Theorem (AFP)

22:33:49 Session AFP/QR_Decomposition (AFP)

22:33:49 Session AFP/Rank_Nullity_Theorem (AFP)

22:33:49 Session AFP/Tarskis_Geometry (AFP)

22:33:49 Session AFP/Triangle (AFP)

22:33:49 Session AFP/pGCL (AFP)

22:33:49 Session HOL/HOL-Cardinals (timing)

22:33:49 Session AFP/Ordinals_and_Cardinals (AFP)

22:33:49 Session AFP/Sort_Encodings (AFP)

22:33:49 Session HOL/HOL-Imperative_HOL

22:33:49 Session AFP/Imperative_Insertion_Sort (AFP)

22:33:49 Session HOL/HOL-Library (main timing)

22:33:49 Session AFP/Abs_Int_ITP2012 (AFP)

22:33:49 Session AFP/Amortized_Complexity (AFP)

22:33:49 Session AFP/Dynamic_Tables (AFP)

22:33:49 Session AFP/ArrowImpossibilityGS (AFP)

22:33:49 Session AFP/Bell_Numbers_Spivey (AFP)

22:33:49 Session AFP/Card_Equiv_Relations (AFP)

22:33:49 Session AFP/Binomial-Heaps (AFP)

22:33:49 Session AFP/Boolean_Expression_Checkers (AFP)

22:33:49 Session AFP/Buildings (AFP)

22:33:50 Session AFP/Card_Multisets (AFP)

22:33:50 Session AFP/Category (AFP)

22:33:50 Session AFP/Category2 (AFP)

22:33:50 Session AFP/Category3 (AFP)

22:33:50 Session AFP/CofGroups (AFP)

22:33:50 Session AFP/Coinductive (AFP)

22:33:50 Session AFP/Lazy-Lists-II (AFP)

22:33:50 Session AFP/Topology (AFP)

22:33:50 Session AFP/Parity_Game (AFP)

22:33:50 Session AFP/Stream_Fusion_Code (AFP)

22:33:50 Session AFP/ConcurrentIMP (AFP)

22:33:50 Session AFP/CoreC++ (AFP)

22:33:50 Session AFP/Datatype_Order_Generator (AFP)

22:33:50 Session AFP/Old_Datatype_Show (AFP)

22:33:50 Session AFP/Deriving (AFP)

22:33:50 Session AFP/Containers (AFP)

22:33:50 Session AFP/Containers-Benchmarks (AFP)

22:33:50 Session AFP/Show (AFP)

22:33:50 Session AFP/Descartes_Sign_Rule (AFP)

22:33:50 Session AFP/Efficient-Mergesort (AFP)

22:33:50 Session AFP/FOL-Fitting (AFP)

22:33:50 Session AFP/Finger-Trees (AFP)

22:33:50 Session AFP/Formula_Derivatives (AFP)

22:33:50 Session AFP/Formula_Derivatives-Examples (AFP)

22:33:50 Session AFP/Free-Boolean-Algebra (AFP)

22:33:50 Session AFP/Functional-Automata (AFP)

22:33:50 Session AFP/Group-Ring-Module (AFP)

22:33:50 Session AFP/Valuation (AFP)

22:33:50 Session AFP/Isabelle_Meta_Model (AFP)

22:33:50 Session AFP/KBPs (AFP)

22:33:50 Session AFP/LTL (AFP)

22:33:50 Session AFP/LTL_to_DRA (AFP)

22:33:50 Session AFP/Stuttering_Equivalence (AFP)

22:33:50 Session AFP/Landau_Symbols (AFP)

22:33:50 Session AFP/LinearQuantifierElim (AFP)

22:33:50 Session AFP/List-Infinite (AFP)

22:33:50 Session AFP/Nat-Interval-Logic (AFP)

22:33:50 Session AFP/AutoFocus-Stream (AFP)

22:33:50 Session AFP/MSO_Regex_Equivalence (AFP)

22:33:50 Session AFP/MSO_Examples (AFP)

22:33:50 Session AFP/MuchAdoAboutTwo (AFP)

22:33:50 Session AFP/Myhill-Nerode (AFP)

22:33:50 Session AFP/POPLmark-deBruijn (AFP)

22:33:50 Session AFP/Pairing_Heap (AFP)

22:33:50 Session AFP/Presburger-Automata (AFP)

22:33:50 Session AFP/Program-Conflict-Analysis (AFP)

22:33:50 Session AFP/Regex_Equivalence (AFP)

22:33:50 Session AFP/Regex_Equivalence_Examples (AFP)

22:33:50 Session AFP/Regular-Sets (AFP)

22:33:50 Session AFP/Posix-Lexing (AFP)

22:33:50 Session AFP/Ribbon_Proofs (AFP)

22:33:50 Session AFP/SATSolverVerification (AFP)

22:33:50 Session AFP/Selection_Heap_Sort (AFP)

22:33:50 Session AFP/Separation_Logic_Imperative_HOL (AFP)

22:33:51 Session AFP/Stable_Matching (AFP)

22:33:51 Session AFP/Sturm_Sequences (AFP)

22:33:51 Session AFP/Special_Function_Bounds (AFP)

22:33:51 Session AFP/SuperCalc (AFP)

22:33:51 Session AFP/Tail_Recursive_Functions (AFP)

22:33:51 Session AFP/Vickrey_Clarke_Groves (AFP)

22:33:51 Session AFP/Well_Quasi_Orders (AFP)

22:33:51 Session HOL/HOL-Nominal

22:33:51 Session AFP/CCS (AFP)

22:33:51 Session AFP/Lam-ml-Normalization (AFP)

22:33:51 Session AFP/Pi_Calculus (AFP)

22:33:51 Session AFP/Psi_Calculi (AFP)

22:33:51 Session AFP/SequentInvertibility (AFP)

22:33:51 Session HOL/HOL-Number_Theory (timing)

22:33:51 Session AFP/Fermat3_4 (AFP)

22:33:51 Session AFP/Lehmer (AFP)

22:33:51 Session AFP/Pratt_Certificate (AFP)

22:33:51 Session AFP/SumSquares (AFP)

22:33:51 Session HOL/HOL-Word (main timing)

22:33:51 Session HOL/HOL-SPARK (main)

22:33:52 Session HOL/HOL-SPARK-Examples

22:33:52 Session AFP/RIPEMD-160-SPARK (AFP)

22:33:52 Session AFP/Kleene_Algebra (AFP)

22:33:52 Session AFP/KAT_and_DRA (AFP)

22:33:52 Session AFP/Algebraic_VCs (AFP)

22:33:52 Session AFP/Multirelations (AFP)

22:33:52 Session AFP/Regular_Algebras (AFP)

22:33:52 Session AFP/Relation_Algebra (AFP)

22:33:52 Session AFP/Residuated_Lattices (AFP)

22:33:52 Session AFP/Native_Word (AFP)

22:33:52 Session AFP/SPARCv8 (AFP)

22:33:52 Session AFP/Separation_Algebra (AFP)

22:33:52 Session AFP/Word_Lib (AFP)

22:33:52 Session AFP/Complx (AFP)

22:33:52 Session AFP/IP_Addresses (AFP)

22:33:52 Session AFP/Simple_Firewall (AFP)

22:33:52 Session AFP/Routing (AFP)

22:33:52 Session AFP/Iptables_Semantics (AFP)

22:33:52 Session AFP/LOFT (AFP)

22:33:52 Session HOL/HOLCF (main timing)

22:33:52 Session AFP/Circus (AFP)

22:33:52 Session AFP/HOLCF-HOL-Library (AFP)

22:33:52 Session AFP/HOLCF-Nominal2 (AFP)

22:33:52 Session AFP/Launchbury (AFP)

22:33:52 Session AFP/Call_Arity (AFP)

22:33:53 Session AFP/PCF (AFP)

22:33:53 Session AFP/Shivers-CFA (AFP)

22:33:53 Session AFP/Stream-Fusion (AFP)

22:33:53 Session AFP/Tycon (AFP)

22:33:53 Session AFP/WorkerWrapper (AFP)

22:33:53 Session AFP/Heard_Of (AFP)

22:33:53 Session AFP/HereditarilyFinite (AFP)

22:33:53 Session AFP/HotelKeyCards (AFP)

22:33:53 Session AFP/Huffman (AFP)

22:33:53 Session AFP/HyperCTL (AFP)

22:33:53 Session AFP/IEEE_Floating_Point (AFP)

22:33:53 Session AFP/Impossible_Geometry (AFP)

22:33:53 Session AFP/Incompleteness (AFP)

22:33:53 Session AFP/Surprise_Paradox (AFP)

22:33:53 Session AFP/Incredible_Proof_Machine (AFP)

22:33:53 Session AFP/Inductive_Confidentiality (AFP)

22:33:53 Session AFP/InfPathElimination (AFP)

22:33:53 Session AFP/Integration (AFP)

22:33:53 Session AFP/Jinja (AFP)

22:33:53 Session AFP/HRB-Slicing (AFP)

22:33:53 Session AFP/InformationFlowSlicing_Inter (AFP)

22:33:53 Session AFP/Slicing (AFP)

22:33:53 Session AFP/InformationFlowSlicing (AFP)

22:33:53 Session AFP/JiveDataStoreModel (AFP)

22:33:53 Session AFP/KAD (AFP)

22:33:53 Session AFP/Koenigsberg_Friendship_Base (AFP)

22:33:53 Session AFP/Koenigsberg_Friendship (AFP)

22:33:53 Session AFP/Lambda_Free_KBOs (AFP)

22:33:54 Session AFP/Lambda_Free_RPOs (AFP)

22:33:54 Session AFP/LatticeProperties (AFP)

22:33:54 Session AFP/MonoBoolTranAlgebra (AFP)

22:33:54 Session AFP/PseudoHoops (AFP)

22:33:54 Session AFP/Lifting_Definition_Option (AFP)

22:33:54 Session AFP/LightweightJava (AFP)

22:33:54 Session AFP/Liouville_Numbers (AFP)

22:33:54 Session AFP/List-Index (AFP)

22:33:54 Session AFP/List_Interleaving (AFP)

22:33:54 Session AFP/Locally-Nameless-Sigma (AFP)

22:33:54 Session AFP/Marriage (AFP)

22:33:54 Session AFP/Latin_Square (AFP)

22:33:54 Session AFP/Max-Card-Matching (AFP)

22:33:54 Session AFP/MiniML (AFP)

22:33:54 Session AFP/Nested_Multisets_Ordinals (AFP)

22:33:54 Session AFP/Network_Security_Policy_Verification (AFP)

22:33:55 Session AFP/No_FTL_observers (AFP)

22:33:55 Session AFP/Nominal2 (AFP)

22:33:55 Session AFP/Modal_Logics_for_NTS (AFP)

22:33:55 Session AFP/Rewriting_Z (AFP)

22:33:55 Session AFP/Noninterference_CSP (AFP)

22:33:55 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

22:33:55 Session AFP/Noninterference_Generic_Unwinding (AFP)

22:33:55 Session AFP/Noninterference_Inductive_Unwinding (AFP)

22:33:55 Session AFP/Noninterference_Sequential_Composition (AFP)

22:33:55 Session AFP/Noninterference_Concurrent_Composition (AFP)

22:33:55 Session AFP/NormByEval (AFP)

22:33:55 Session AFP/Open_Induction (AFP)

22:33:55 Session AFP/Ordinal (AFP)

22:33:55 Session AFP/Paraconsistency (AFP)

22:33:55 Session AFP/Partial_Function_MR (AFP)

22:33:55 Session AFP/Polynomial_Interpolation (AFP)

22:33:55 Session AFP/Pop_Refinement (AFP)

22:33:55 Session AFP/Possibilistic_Noninterference (AFP)

22:33:55 Session AFP/Priority_Queue_Braun (AFP)

22:33:55 Session AFP/PropResPI (AFP)

22:33:55 Session AFP/ROBDD (AFP)

22:33:56 Session AFP/RSAPSS (AFP)

22:33:56 Session AFP/Ramsey-Infinite (AFP)

22:33:56 Session AFP/Recursion-Theory-I (AFP)

22:33:56 Session AFP/RefinementReactive (AFP)

22:33:56 Session AFP/Rep_Fin_Groups (AFP)

22:33:56 Session AFP/Resolution_FOL (AFP)

22:33:56 Session AFP/Robbins-Conjecture (AFP)

22:33:56 Session AFP/Roy_Floyd_Warshall (AFP)

22:33:56 Session AFP/SIFPL (AFP)

22:33:56 Session AFP/SIFUM_Type_Systems (AFP)

22:33:56 Session AFP/SenSocialChoice (AFP)

22:33:56 Session AFP/Separata (AFP)

22:33:56 Session AFP/Simpl (AFP)

22:33:56 Session AFP/BDD (AFP)

22:33:56 Session AFP/Planarity_Certificates (AFP)

22:33:57 Session AFP/Skew_Heap (AFP)

22:33:57 Session AFP/Splay_Tree (AFP)

22:33:57 Session AFP/Statecharts (AFP)

22:33:57 Session AFP/Stone_Algebras (AFP)

22:33:57 Session AFP/Strong_Security (AFP)

22:33:57 Session AFP/Sturm_Tarski (AFP)

22:33:57 Session AFP/TLA (AFP)

22:33:57 Session AFP/Timed_Automata (AFP)

22:33:57 Session AFP/TortoiseHare (AFP)

22:33:57 Session AFP/Transitive-Closure-II (AFP)

22:33:57 Session AFP/Tree_Decomposition (AFP)

22:33:57 Session AFP/Trie (AFP)

22:33:57 Session AFP/UPF (AFP)

22:33:57 Session AFP/Verified-Prover (AFP)

22:33:57 Session AFP/VolpanoSmith (AFP)

22:33:57 Session AFP/WHATandWHERE_Security (AFP)

22:33:57 Session AFP/XML (AFP)

22:33:59 Building Pure ...

22:34:10 Pure: theory Pure

22:34:10 Pure: theory ML_Bootstrap

22:34:13 Warning: missing document directory

22:34:13 Timing Pure (1 threads, 0.520s elapsed time, 0.520s cpu time, 0.000s GC time, factor 1.00)

22:34:13 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/Pure/Pure

22:34:13 Finished Pure (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.99)

22:34:13 Building HOL ...

22:34:14 HOL: theory Code_Generator

22:34:16 HOL: theory HOL

22:34:19 HOL: theory Argo

22:34:19 HOL: theory Ctr_Sugar

22:34:20 HOL: theory Orderings

22:34:20 HOL: theory SAT

22:34:21 HOL: theory Groups

22:34:23 HOL: theory Lattices

22:34:25 HOL: theory Set

22:34:26 HOL: theory Fun

22:34:27 HOL: theory Typedef

22:34:27 HOL: theory Rings

22:34:27 HOL: theory Complete_Lattices

22:34:29 HOL: theory Inductive

22:34:30 HOL: theory Product_Type

22:34:32 HOL: theory Complete_Partial_Order

22:34:32 HOL: theory Sum_Type

22:34:35 HOL: theory Nat

22:34:37 HOL: theory Fields

22:34:37 HOL: theory Meson

22:34:38 HOL: theory ATP

22:34:39 HOL: theory Metis

22:34:41 HOL: theory Finite_Set

22:34:42 HOL: theory Relation

22:34:43 HOL: theory Transitive_Closure

22:34:44 HOL: theory Wellfounded

22:34:44 HOL: theory Fun_Def_Base

22:34:44 HOL: theory Hilbert_Choice

22:34:45 HOL: theory Wfrec

22:34:45 HOL: theory Order_Relation

22:34:45 HOL: theory BNF_Wellorder_Relation

22:34:45 HOL: theory Zorn

22:34:45 HOL: theory BNF_Wellorder_Embedding

22:34:45 HOL: theory BNF_Wellorder_Constructions

22:34:46 HOL: theory BNF_Cardinal_Order_Relation

22:34:47 HOL: theory BNF_Cardinal_Arithmetic

22:34:47 HOL: theory BNF_Def

22:34:48 HOL: theory BNF_Composition

22:34:49 HOL: theory Basic_BNFs

22:34:49 HOL: theory BNF_Fixpoint_Base

22:34:52 HOL: theory BNF_Least_Fixpoint

22:34:53 HOL: theory Basic_BNF_LFPs

22:34:53 HOL: theory Transfer

22:34:54 HOL: theory Num

22:34:57 HOL: theory Power

22:34:59 HOL: theory Groups_Big

22:35:01 HOL: theory Equiv_Relations

22:35:01 HOL: theory Lifting

22:35:02 HOL: theory Lifting_Set

22:35:02 HOL: theory Option

22:35:03 HOL: theory Quotient

22:35:03 HOL: theory Extraction

22:35:04 HOL: theory Lattices_Big

22:35:05 HOL: theory Partial_Function

22:35:05 HOL: theory Fun_Def

22:35:07 HOL: theory Int

22:35:09 HOL: theory Nat_Transfer

22:35:09 HOL: theory Parity

22:35:11 HOL: theory Divides

22:35:16 HOL: theory Code_Numeral

22:35:16 HOL: theory Numeral_Simprocs

22:35:17 HOL: theory SMT

22:35:17 HOL: theory Semiring_Normalization

22:35:18 HOL: theory Set_Interval

22:35:19 HOL: theory Groebner_Basis

22:35:21 HOL: theory Conditionally_Complete_Lattices

22:35:21 HOL: theory Filter

22:35:22 HOL: theory Presburger

22:35:24 HOL: theory Sledgehammer

22:35:25 HOL: theory List

22:35:32 HOL: theory Groups_List

22:35:32 HOL: theory Map

22:35:32 HOL: theory Random

22:35:33 HOL: theory Enum

22:35:35 HOL: theory String

22:35:38 HOL: theory BNF_Greatest_Fixpoint

22:35:38 HOL: theory Predicate

22:35:40 HOL: theory Lazy_Sequence

22:35:40 HOL: theory Limited_Sequence

22:35:41 HOL: theory Typerep

22:35:42 HOL: theory Code_Evaluation

22:35:43 HOL: theory Quickcheck_Random

22:35:45 HOL: theory Quickcheck_Exhaustive

22:35:45 HOL: theory Quickcheck_Narrowing

22:35:51 HOL: theory Random_Pred

22:35:51 HOL: theory Record

22:35:51 HOL: theory Random_Sequence

22:35:52 HOL: theory Predicate_Compile

22:35:53 HOL: theory Nitpick

22:35:57 HOL: theory Main

22:35:58 HOL: theory Archimedean_Field

22:35:58 HOL: theory Binomial

22:35:59 HOL: theory GCD

22:36:02 HOL: theory Topological_Spaces

22:36:03 HOL: theory Rat

22:36:05 HOL: theory Real

22:36:08 HOL: theory Real_Vector_Spaces

22:36:18 HOL: theory Inequalities

22:36:18 HOL: theory Limits

22:36:21 HOL: theory Deriv

22:36:22 HOL: theory Series

22:36:22 HOL: theory NthRoot

22:36:23 HOL: theory Transcendental

22:36:26 HOL: theory Complex

22:36:26 HOL: theory MacLaurin

22:36:28 HOL: theory Complex_Main

22:39:03 Timing HOL (2 threads, 210.570s elapsed time, 397.532s cpu time, 37.212s GC time, factor 1.89)

22:39:03 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL

22:39:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL/document.pdf

22:39:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL/outline.pdf

22:39:03 Finished HOL (0:04:50 elapsed time, 0:08:45 cpu time, factor 1.81)

22:39:05 Building HOL-Library ...

22:39:06 Building HOL-Analysis ...

22:39:06 Building HOLCF ...

22:39:06 Building HOL-Word ...

22:39:06 Building HOL-Algebra ...

22:39:06 Building HOL-Nominal ...

22:39:06 Building Abstract-Rewriting ...

22:39:06 Building HOL-Number_Theory ...

22:39:08 HOLCF: theory Nat_Bijection

22:39:08 HOLCF: theory Old_Datatype

22:39:08 Abstract-Rewriting: theory Regular_Set

22:39:08 Abstract-Rewriting: theory While_Combinator

22:39:08 HOL-Nominal: theory Infinite_Set

22:39:08 HOL-Nominal: theory Old_Datatype

22:39:08 HOL-Word: theory Bit

22:39:08 HOL-Word: theory Bits

22:39:08 HOL-Number_Theory: theory Congruence

22:39:08 HOL-Number_Theory: theory FuncSet

22:39:08 HOL-Algebra: theory FuncSet

22:39:08 HOL-Algebra: theory Multiset

22:39:08 HOL-Word: theory Boolean_Algebra

22:39:08 HOL-Library: theory Adhoc_Overloading

22:39:08 HOL-Library: theory Lattice_Syntax

22:39:08 HOL-Library: theory AList

22:39:09 HOL-Library: theory BNF_Axiomatization

22:39:09 HOL-Library: theory BNF_Corec

22:39:09 HOL-Word: theory Bits_Bit

22:39:09 HOL-Word: theory Misc_Numeric

22:39:09 HOL-Number_Theory: theory Multiset

22:39:09 HOL-Word: theory Bit_Representation

22:39:09 HOL-Word: theory Misc_Typedef

22:39:09 HOL-Number_Theory: theory Lattice

22:39:09 HOL-Word: theory Phantom_Type

22:39:09 HOL-Analysis: theory FuncSet

22:39:09 HOL-Analysis: theory Disjoint_Sets

22:39:10 HOL-Word: theory Bits_Int

22:39:10 HOLCF: theory Countable

22:39:10 HOL-Nominal: theory Nominal

22:39:10 HOL-Analysis: theory Infinite_Set

22:39:10 HOL-Analysis: theory Multiset

22:39:10 HOL-Library: theory DAList

22:39:10 HOL-Analysis: theory Nat_Bijection

22:39:11 HOL-Word: theory Cardinality

22:39:11 Abstract-Rewriting: theory Regular_Exp

22:39:11 HOL-Analysis: theory Old_Datatype

22:39:11 HOLCF: theory Porder

22:39:11 HOL-Word: theory Bool_List_Representation

22:39:11 HOL-Library: theory Stirling

22:39:11 HOL-Number_Theory: theory Group

22:39:12 HOL-Word: theory Numeral_Type

22:39:12 HOLCF: theory Pcpo

22:39:12 HOL-Library: theory Bit

22:39:12 HOL-Word: theory Word_Miscellaneous

22:39:12 HOL-Analysis: theory Countable

22:39:13 HOL-Library: theory Bits

22:39:13 HOL-Word: theory Type_Length

22:39:13 HOL-Word: theory Word

22:39:13 HOLCF: theory Cont

22:39:13 HOL-Library: theory Bits_Bit

22:39:13 HOL-Algebra: theory Factorial_Ring

22:39:13 HOLCF: theory Adm

22:39:13 HOL-Number_Theory: theory FiniteProduct

22:39:13 HOL-Algebra: theory Permutation

22:39:13 HOLCF: theory Discrete

22:39:13 HOL-Library: theory Boolean_Algebra

22:39:14 HOLCF: theory Cpodef

22:39:14 HOL-Library: theory Cardinal_Notations

22:39:14 HOL-Library: theory Char_ord

22:39:14 HOLCF: theory Fun_Cpo

22:39:14 HOL-Library: theory Code_Abstract_Nat

22:39:14 HOL-Number_Theory: theory Ring

22:39:14 Abstract-Rewriting: theory NDerivative

22:39:14 Abstract-Rewriting: theory Relation_Interpretation

22:39:14 HOL-Analysis: theory Countable_Set

22:39:14 HOLCF: theory Product_Cpo

22:39:14 HOL-Library: theory Code_Binary_Nat

22:39:14 HOL-Library: theory Code_Target_Nat

22:39:14 HOLCF: theory Cfun

22:39:15 HOL-Library: theory Code_Char

22:39:15 HOL-Analysis: theory Countable_Complete_Lattices

22:39:15 HOL-Library: theory Code_Prolog

22:39:15 HOL-Library: theory Code_Test

22:39:15 HOL-Library: theory Combine_PER

22:39:15 HOL-Analysis: theory Permutations

22:39:15 HOLCF: theory Cprod

22:39:15 HOLCF: theory Fix

22:39:15 HOL-Library: theory Complete_Partial_Order2

22:39:16 HOLCF: theory Sfun

22:39:16 HOLCF: theory Sprod

22:39:16 HOLCF: theory Up

22:39:16 HOL-Library: theory Debug

22:39:16 HOL-Library: theory Disjoint_Sets

22:39:16 HOL-Library: theory Dlist

22:39:16 HOLCF: theory Lift

22:39:17 HOL-Analysis: theory Phantom_Type

22:39:17 HOLCF: theory One

22:39:17 HOLCF: theory Tr

22:39:17 HOLCF: theory Ssum

22:39:17 HOL-Library: theory FSet

22:39:17 HOL-Analysis: theory Cardinality

22:39:18 HOLCF: theory Plain_HOLCF

22:39:18 HOL-Analysis: theory Product_Plus

22:39:18 Abstract-Rewriting: theory Equivalence_Checking

22:39:18 HOL-Analysis: theory Product_Order

22:39:18 Abstract-Rewriting: theory Regexp_Method

22:39:18 HOLCF: theory Completion

22:39:18 HOLCF: theory Deflation

22:39:18 HOL-Analysis: theory Set_Algebras

22:39:18 HOL-Analysis: theory Numeral_Type

22:39:19 HOLCF: theory Map_Functions

22:39:19 HOLCF: theory Fixrec

22:39:19 HOL-Analysis: theory L2_Norm

22:39:19 HOL-Analysis: theory Continuum_Not_Denumerable

22:39:19 HOLCF: theory Bifinite

22:39:19 HOL-Library: theory Fraction_Field

22:39:19 HOLCF: theory Domain_Aux

22:39:20 HOL-Analysis: theory Discrete

22:39:20 HOL-Analysis: theory Indicator_Function

22:39:20 HOL-Analysis: theory Inner_Product

22:39:20 HOL-Library: theory Fun_Lexorder

22:39:20 HOL-Analysis: theory Liminf_Limsup

22:39:20 HOL-Library: theory FuncSet

22:39:20 HOLCF: theory Universal

22:39:21 HOL-Library: theory Finite_Map

22:39:21 HOL-Library: theory Function_Algebras

22:39:21 HOL-Library: theory Function_Division

22:39:21 HOL-Analysis: theory Nonpos_Ints

22:39:21 HOL-Library: theory Code_Target_Int

22:39:21 HOL-Analysis: theory Product_Vector

22:39:21 HOL-Analysis: theory Operator_Norm

22:39:22 HOL-Analysis: theory Order_Continuity

22:39:22 Abstract-Rewriting: theory Infinite_Set

22:39:22 HOLCF: theory Algebraic

22:39:22 HOLCF: theory Compact_Basis

22:39:22 HOL-Algebra: theory Euclidean_Algorithm

22:39:22 HOL-Library: theory Code_Target_Numeral

22:39:22 HOL-Analysis: theory Euclidean_Space

22:39:22 HOLCF: theory LowerPD

22:39:22 HOL-Library: theory Groups_Big_Fun

22:39:22 Abstract-Rewriting: theory Seq

22:39:22 HOLCF: theory UpperPD

22:39:22 HOL-Library: theory IArray

22:39:22 HOLCF: theory Representable

22:39:22 HOL-Analysis: theory Extended_Nat

22:39:22 Abstract-Rewriting: theory Abstract_Rewriting

22:39:22 HOLCF: theory ConvexPD

22:39:23 HOL-Library: theory Infinite_Set

22:39:23 HOL-Library: theory Omega_Words_Fun

22:39:23 HOL-Library: theory LaTeXsugar

22:39:23 HOL-Library: theory Lattice_Constructions

22:39:23 HOL-Library: theory ListVector

22:39:24 HOL-Analysis: theory Extended_Real

22:39:24 HOL-Library: theory List_lexord

22:39:24 HOL-Analysis: theory Finite_Cartesian_Product

22:39:24 HOL-Library: theory Mapping

22:39:24 Abstract-Rewriting: theory Relative_Rewriting

22:39:24 Abstract-Rewriting: theory SN_Orders

22:39:25 HOL-Analysis: theory Linear_Algebra

22:39:25 HOL-Library: theory AList_Mapping

22:39:25 HOLCF: theory Domain

22:39:26 HOL-Library: theory Misc_Numeric

22:39:26 HOL-Library: theory Bit_Representation

22:39:26 HOL-Library: theory Misc_Typedef

22:39:26 HOL-Library: theory Bits_Int

22:39:26 HOL-Library: theory Monad_Syntax

22:39:27 HOL-Library: theory More_List

22:39:27 HOLCF: theory Powerdomains

22:39:27 Abstract-Rewriting: theory SN_Order_Carrier

22:39:27 HOL-Library: theory Multiset

22:39:28 HOLCF: theory HOLCF

22:39:28 HOL-Analysis: theory Extended_Nonnegative_Real

22:39:28 HOL-Analysis: theory Periodic_Fun

22:39:28 HOL-Library: theory Bool_List_Representation

22:39:28 HOL-Analysis: theory Poly_Roots

22:39:29 HOL-Analysis: theory Sum_of_Squares

22:39:29 HOL-Library: theory Nat_Bijection

22:39:29 HOL-Library: theory Stream

22:39:30 HOL-Analysis: theory Sigma_Algebra

22:39:31 HOL-Library: theory Old_Datatype

22:39:31 HOL-Algebra: theory Primes

22:39:31 HOL-Analysis: theory Norm_Arith

22:39:32 HOL-Analysis: theory Topology_Euclidean_Space

22:39:32 HOL-Library: theory DAList_Multiset

22:39:32 HOL-Library: theory Factorial_Ring

22:39:33 Timing HOL-Nominal (2 threads, 8.623s elapsed time, 16.632s cpu time, 0.780s GC time, factor 1.93)

22:39:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Nominal

22:39:33 Finished HOL-Nominal (0:00:26 elapsed time, 0:00:42 cpu time, factor 1.62)

22:39:33 HOL-Library: theory Multiset_Order

22:39:33 Building Jinja ...

22:39:33 HOL-Library: theory Permutation

22:39:33 HOL-Library: theory Permutations

22:39:33 HOL-Analysis: theory Measurable

22:39:34 HOL-Analysis: theory Measure_Space

22:39:35 Jinja: theory Code_Target_Int

22:39:35 Jinja: theory Code_Abstract_Nat

22:39:35 Jinja: theory Code_Target_Nat

22:39:35 Jinja: theory Sublist

22:39:35 Jinja: theory Code_Target_Numeral

22:39:36 Jinja: theory While_Combinator

22:39:36 HOL-Algebra: theory Congruence

22:39:36 HOL-Algebra: theory Exponent

22:39:36 HOL-Library: theory Countable

22:39:37 HOL-Algebra: theory Lattice

22:39:37 HOL-Number_Theory: theory Factorial_Ring

22:39:37 HOL-Number_Theory: theory MiscAlgebra

22:39:37 HOL-Analysis: theory Caratheodory

22:39:38 HOL-Number_Theory: theory Fib

22:39:38 HOL-Analysis: theory Summation_Tests

22:39:38 HOL-Library: theory Countable_Set

22:39:39 HOL-Library: theory Countable_Complete_Lattices

22:39:39 HOL-Algebra: theory Group

22:39:40 HOL-Algebra: theory Bij

22:39:40 HOL-Algebra: theory Coset

22:39:41 Jinja: theory Auxiliary

22:39:41 Jinja: theory List_Index

22:39:41 Jinja: theory Type

22:39:42 HOL-Analysis: theory Bounded_Linear_Function

22:39:42 HOL-Analysis: theory Convex_Euclidean_Space

22:39:42 Jinja: theory Hidden

22:39:42 HOL-Library: theory Countable_Set_Type

22:39:42 HOL-Algebra: theory FiniteProduct

22:39:42 Jinja: theory Transitive_Closure_Table

22:39:42 Jinja: theory Decl

22:39:42 Jinja: theory Semilat

22:39:42 Jinja: theory TypeRel

22:39:42 HOL-Library: theory Euclidean_Algorithm

22:39:42 HOL-Algebra: theory Ring

22:39:43 Jinja: theory Err

22:39:43 HOL-Algebra: theory Sylow

22:39:43 HOL-Analysis: theory Extended_Real_Limits

22:39:44 Jinja: theory Listn

22:39:44 Jinja: theory Value

22:39:44 HOL-Library: theory Old_Recdef

22:39:44 Jinja: theory Opt

22:39:44 HOL-Algebra: theory Divisibility

22:39:44 Jinja: theory Product

22:39:44 HOL-Number_Theory: theory Euclidean_Algorithm

22:39:44 HOL-Analysis: theory Tagged_Division

22:39:45 HOL-Library: theory Option_ord

22:39:45 Jinja: theory Objects

22:39:45 Jinja: theory Semilattices

22:39:45 Jinja: theory Exceptions

22:39:45 Jinja: theory JVMState

22:39:45 HOL-Library: theory Parallel

22:39:45 Jinja: theory JVMInstructions

22:39:45 Jinja: theory Conform

22:39:45 Jinja: theory Expr

22:39:46 HOL-Library: theory Perm

22:39:46 HOL-Analysis: theory Uniform_Limit

22:39:46 HOL-Algebra: theory AbelCoset

22:39:47 HOL-Library: theory Phantom_Type

22:39:47 Jinja: theory State

22:39:47 Jinja: theory SystemClasses

22:39:47 HOL-Analysis: theory Continuous_Extension

22:39:47 HOL-Algebra: theory Module

22:39:48 HOL-Library: theory Cardinality

22:39:48 Jinja: theory JVMExceptions

22:39:48 HOL-Analysis: theory Path_Connected

22:39:48 Jinja: theory JVMExecInstr

22:39:49 Jinja: theory JVMExec

22:39:49 HOL-Library: theory FinFun

22:39:49 Jinja: theory JVMDefensive

22:39:51 HOL-Library: theory Numeral_Type

22:39:51 Timing HOL-Word (2 threads, 20.990s elapsed time, 40.248s cpu time, 1.744s GC time, factor 1.92)

22:39:51 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Word

22:39:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Word/document.pdf

22:39:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Word/outline.pdf

22:39:51 Finished HOL-Word (0:00:44 elapsed time, 0:01:16 cpu time, factor 1.71)

22:39:51 Jinja: theory JVMListExample

22:39:52 HOL-Library: theory Normalized_Fraction

22:39:52 Building Kleene_Algebra ...

22:39:52 Jinja: theory Examples

22:39:52 HOL-Analysis: theory Homeomorphism

22:39:52 Jinja: theory BigStep

22:39:52 HOL-Library: theory Predicate_Compile_Alternative_Defs

22:39:52 HOL-Analysis: theory Brouwer_Fixpoint

22:39:52 HOL-Library: theory Type_Length

22:39:52 HOL-Library: theory Predicate_Compile_Quickcheck

22:39:52 HOL-Library: theory Saturated

22:39:53 Timing HOLCF (2 threads, 20.122s elapsed time, 36.016s cpu time, 2.124s GC time, factor 1.79)

22:39:53 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF

22:39:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF/document.pdf

22:39:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF/outline.pdf

22:39:53 Finished HOLCF (0:00:46 elapsed time, 0:01:16 cpu time, factor 1.64)

22:39:53 HOL-Library: theory Product_Lexorder

22:39:53 HOL-Library: theory Product_Plus

22:39:53 Building Simpl ...

22:39:53 HOL-Library: theory Quotient_Syntax

22:39:53 HOL-Number_Theory: theory Primes

22:39:53 HOL-Library: theory Quotient_Option

22:39:53 HOL-Library: theory Product_Order

22:39:53 HOL-Library: theory Quotient_Product

22:39:53 HOL-Library: theory Quotient_Set

22:39:53 HOL-Library: theory Finite_Lattice

22:39:53 HOL-Library: theory Quotient_List

22:39:54 HOL-Algebra: theory Ideal

22:39:54 HOL-Number_Theory: theory Cong

22:39:54 HOL-Library: theory Quotient_Sum

22:39:54 Jinja: theory SmallStep

22:39:54 HOL-Library: theory Quotient_Type

22:39:54 HOL-Number_Theory: theory Eratosthenes

22:39:54 HOL-Analysis: theory Derivative

22:39:54 HOL-Library: theory RBT_Impl

22:39:54 Kleene_Algebra: theory Signatures

22:39:54 HOL-Number_Theory: theory Residues

22:39:55 Kleene_Algebra: theory Dioid

22:39:55 Simpl: theory DistinctTreeProver

22:39:55 Simpl: theory LaTeXsugar

22:39:56 Simpl: theory Multiset

22:39:56 Jinja: theory DefAss

22:39:56 Jinja: theory J1

22:39:56 HOL-Analysis: theory Cartesian_Euclidean_Space

22:39:57 HOL-Number_Theory: theory Euler_Criterion

22:39:57 HOL-Analysis: theory Weierstrass_Theorems

22:39:57 HOL-Number_Theory: theory Gauss

22:39:57 HOL-Library: theory Ramsey

22:39:57 Simpl: theory Generalise

22:39:57 HOL-Number_Theory: theory Quadratic_Reciprocity

22:39:57 HOL-Library: theory Reflection

22:39:57 HOL-Number_Theory: theory Pocklington

22:39:57 HOL-Library: theory Refute

22:39:57 Simpl: theory StateFun

22:39:57 Simpl: theory StateSpaceLocale

22:39:57 HOL-Number_Theory: theory Number_Theory

22:39:58 Simpl: theory StateSpaceSyntax

22:39:58 Simpl: theory Old_Recdef

22:39:58 HOL-Library: theory Rewrite

22:39:58 Jinja: theory execute_Bigstep

22:39:58 HOL-Algebra: theory RingHom

22:39:58 HOL-Library: theory Set_Algebras

22:39:59 HOL-Library: theory Simps_Case_Conv

22:39:59 Simpl: theory Language

22:39:59 HOL-Library: theory Extended

22:39:59 HOL-Analysis: theory Determinants

22:39:59 Jinja: theory WellType

22:40:00 HOL-Analysis: theory Fashoda_Theorem

22:40:00 HOL-Analysis: theory Ordered_Euclidean_Space

22:40:00 HOL-Analysis: theory Polytope

22:40:00 HOL-Algebra: theory QuotRing

22:40:00 Jinja: theory Annotate

22:40:00 HOL-Library: theory State_Monad

22:40:01 HOL-Library: theory Sublist

22:40:01 Jinja: theory WellTypeRT

22:40:01 HOL-Algebra: theory UnivPoly

22:40:01 Simpl: theory Permutation

22:40:01 Simpl: theory Simpl_Heap

22:40:01 HOL-Algebra: theory IntRing

22:40:01 Simpl: theory HeapList

22:40:02 HOL-Library: theory Prefix_Order

22:40:02 HOL-Library: theory Sublist_Order

22:40:02 HOL-Library: theory Polynomial

22:40:02 Jinja: theory execute_WellType

22:40:05 Jinja: theory WellForm

22:40:05 Jinja: theory PCompiler

22:40:05 Jinja: theory Compiler1

22:40:06 Jinja: theory Compiler2

22:40:06 HOL-Analysis: theory Borel_Space

22:40:06 Jinja: theory Correctness2

22:40:07 Simpl: theory Semantic

22:40:07 HOL-Library: theory BigO

22:40:08 Kleene_Algebra: theory Dioid_Models

22:40:08 Kleene_Algebra: theory Conway

22:40:08 HOL-Library: theory Code_Real_Approx_By_Float

22:40:08 Jinja: theory WWellForm

22:40:09 Jinja: theory Equivalence

22:40:09 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

22:40:09 HOL-Library: theory Diagonal_Subsequence

22:40:09 HOL-Library: theory Discrete

22:40:09 HOL-Library: theory Field_as_Ring

22:40:10 Jinja: theory Progress

22:40:11 HOL-Analysis: theory Regularity

22:40:11 Simpl: theory HoarePartialDef

22:40:11 Simpl: theory Termination

22:40:11 Timing Abstract-Rewriting (2 threads, 34.760s elapsed time, 63.220s cpu time, 3.128s GC time, factor 1.82)

22:40:11 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract-Rewriting

22:40:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract-Rewriting/document.pdf

22:40:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract-Rewriting/outline.pdf

22:40:11 Finished Abstract-Rewriting (0:01:04 elapsed time, 0:01:51 cpu time, factor 1.73)

22:40:11 HOL-Analysis: theory Binary_Product_Measure

22:40:11 HOL-Library: theory Formal_Power_Series

22:40:11 Building Word_Lib ...

22:40:11 Jinja: theory JWellForm

22:40:12 Simpl: theory HoarePartialProps

22:40:12 Simpl: theory HoareTotalDef

22:40:12 Jinja: theory J1WellForm

22:40:12 HOL-Analysis: theory Embed_Measure

22:40:12 HOL-Analysis: theory Finite_Product_Measure

22:40:13 Simpl: theory AlternativeSmallStep

22:40:13 Simpl: theory HoarePartial

22:40:13 Jinja: theory Correctness1

22:40:14 Jinja: theory Compiler

22:40:14 HOL-Analysis: theory Bochner_Integration

22:40:14 HOL-Analysis: theory Function_Topology

22:40:14 Word_Lib: theory Sublist

22:40:14 Word_Lib: theory WordBitwise

22:40:14 Jinja: theory TypeSafe

22:40:14 Simpl: theory SmallStep

22:40:15 Jinja: theory SemiType

22:40:15 Kleene_Algebra: theory Finite_Suprema

22:40:15 Word_Lib: theory Prefix_Order

22:40:15 Jinja: theory JVM_SemiType

22:40:15 Kleene_Algebra: theory Inf_Matrix

22:40:15 HOL-Library: theory Polynomial_FPS

22:40:15 Jinja: theory Effect

22:40:16 Kleene_Algebra: theory Matrix

22:40:16 Simpl: theory HoareTotalProps

22:40:16 HOL-Analysis: theory Complete_Measure

22:40:16 HOL-Analysis: theory Radon_Nikodym

22:40:16 HOL-Library: theory Fundamental_Theorem_Algebra

22:40:17 HOL-Analysis: theory Set_Integral

22:40:17 HOL-Analysis: theory Lebesgue_Measure

22:40:17 Kleene_Algebra: theory Kleene_Algebra

22:40:17 HOL-Library: theory Indicator_Function

22:40:17 Simpl: theory Compose

22:40:17 Simpl: theory HoareTotal

22:40:18 HOL-Library: theory Lattice_Algebras

22:40:19 HOL-Analysis: theory Henstock_Kurzweil_Integration

22:40:19 Simpl: theory Hoare

22:40:19 Simpl: theory Closure

22:40:19 Simpl: theory StateSpace

22:40:19 Word_Lib: theory Enumeration

22:40:19 Word_Lib: theory HOL_Lemmas

22:40:20 Word_Lib: theory More_Divides

22:40:20 Word_Lib: theory Hex_Words

22:40:20 Word_Lib: theory Signed_Words

22:40:20 Simpl: theory Vcg

22:40:20 Word_Lib: theory Norm_Words

22:40:20 Word_Lib: theory WordBitwise_Signed

22:40:20 Word_Lib: theory Word_Syntax

22:40:21 Word_Lib: theory Word_Lib

22:40:21 Word_Lib: theory Aligned

22:40:21 Word_Lib: theory Word_Enum

22:40:22 Word_Lib: theory Word_Setup_32

22:40:22 Word_Lib: theory Word_Setup_64

22:40:22 Word_Lib: theory Word_Lemmas

22:40:22 HOL-Analysis: theory Bounded_Continuous_Function

22:40:22 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

22:40:22 Simpl: theory ProcParEx

22:40:22 Simpl: theory ProcParExSP

22:40:23 HOL-Analysis: theory Integral_Test

22:40:23 Simpl: theory XVcg

22:40:23 Simpl: theory XVcgEx

22:40:23 HOL-Library: theory Liminf_Limsup

22:40:24 HOL-Analysis: theory Complex_Analysis_Basics

22:40:24 HOL-Analysis: theory Interval_Integral

22:40:24 Simpl: theory ClosureEx

22:40:24 Kleene_Algebra: theory DRA

22:40:24 Kleene_Algebra: theory Omega_Algebra

22:40:24 Simpl: theory ComposeEx

22:40:24 HOL-Library: theory Log_Nat

22:40:24 HOL-Library: theory Float

22:40:25 HOL-Analysis: theory Lebesgue_Integral_Substitution

22:40:25 Simpl: theory Quicksort

22:40:25 HOL-Analysis: theory Complex_Transcendental

22:40:25 Kleene_Algebra: theory PHL_KA

22:40:26 Simpl: theory SyntaxTest

22:40:27 Jinja: theory BVSpec

22:40:27 Simpl: theory UserGuide

22:40:27 Kleene_Algebra: theory PHL_DRA

22:40:27 Kleene_Algebra: theory Kleene_Algebra_Models

22:40:27 Simpl: theory VcgEx

22:40:27 Jinja: theory BVConform

22:40:27 Jinja: theory TypeComp

22:40:27 Word_Lib: theory Word_Lemmas_32

22:40:27 Kleene_Algebra: theory Formal_Power_Series

22:40:27 Word_Lib: theory Word_Lemmas_64

22:40:27 HOL-Library: theory Lub_Glb

22:40:28 Jinja: theory BVSpecTypeSafe

22:40:28 HOL-Library: theory Multiset_Permutations

22:40:28 HOL-Analysis: theory Generalised_Binomial_Theorem

22:40:28 HOL-Analysis: theory Harmonic_Numbers

22:40:28 HOL-Analysis: theory Cauchy_Integral_Theorem

22:40:28 HOL-Analysis: theory Gamma_Function

22:40:29 HOL-Library: theory Nonpos_Ints

22:40:29 Jinja: theory BVNoTypeError

22:40:29 HOL-Library: theory RBT

22:40:29 Jinja: theory EffectMono

22:40:29 Jinja: theory Typing_Framework

22:40:29 HOL-Library: theory OptionalSugar

22:40:29 Jinja: theory SemilatAlg

22:40:30 Jinja: theory Kildall

22:40:30 Jinja: theory LBVSpec

22:40:30 HOL-Library: theory RBT_Mapping

22:40:30 HOL-Library: theory RBT_Set

22:40:30 Simpl: theory VcgExSP

22:40:30 HOL-Library: theory Order_Continuity

22:40:30 Jinja: theory Typing_Framework_err

22:40:30 Jinja: theory LBVComplete

22:40:30 Jinja: theory LBVCorrect

22:40:30 Jinja: theory TF_JVM

22:40:30 Jinja: theory Abstract_BV

22:40:31 HOL-Library: theory Periodic_Fun

22:40:31 HOL-Library: theory Extended_Nat

22:40:31 HOL-Library: theory Polynomial_Factorial

22:40:31 Jinja: theory BVExec

22:40:31 Jinja: theory LBVJVM

22:40:31 Kleene_Algebra: theory Omega_Algebra_Models

22:40:31 Simpl: theory VcgExTotal

22:40:31 Jinja: theory BVExample

22:40:32 HOL-Library: theory Extended_Real

22:40:32 HOL-Analysis: theory Conformal_Mappings

22:40:32 HOL-Analysis: theory Further_Topology

22:40:33 Jinja: theory Jinja

22:40:34 Simpl: theory Simpl

22:40:35 HOL-Analysis: theory Analysis

22:40:36 HOL-Library: theory Extended_Nonnegative_Real

22:40:38 HOL-Library: theory Linear_Temporal_Logic_on_Streams

22:40:40 HOL-Library: theory Quadratic_Discriminant

22:40:40 HOL-Library: theory Sum_of_Squares

22:40:43 HOL-Library: theory Transitive_Closure_Table

22:40:43 HOL-Library: theory Tree

22:40:43 HOL-Library: theory While_Combinator

22:40:44 HOL-Library: theory Bourbaki_Witt_Fixpoint

22:40:44 HOL-Library: theory Word_Miscellaneous

22:40:44 HOL-Library: theory Word

22:40:46 HOL-Library: theory Tree_Multiset

22:40:47 HOL-Library: theory Preorder

22:40:47 HOL-Library: theory Function_Growth

22:40:48 HOL-Library: theory Library

22:40:50 HOL-Library: theory Old_SMT

22:41:10 Timing HOL-Number_Theory (2 threads, 91.106s elapsed time, 152.544s cpu time, 5.016s GC time, factor 1.67)

22:41:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory

22:41:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/document.pdf

22:41:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/outline.pdf

22:41:10 Finished HOL-Number_Theory (0:02:04 elapsed time, 0:03:23 cpu time, factor 1.64)

22:41:11 Building Nominal2 ...

22:41:13 Nominal2: theory FSet

22:41:13 Nominal2: theory Infinite_Set

22:41:13 Nominal2: theory Old_Datatype

22:41:15 Nominal2: theory Phantom_Type

22:41:15 Nominal2: theory Cardinality

22:41:16 Timing Kleene_Algebra (2 threads, 50.708s elapsed time, 84.188s cpu time, 3.560s GC time, factor 1.66)

22:41:16 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Kleene_Algebra

22:41:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Kleene_Algebra/document.pdf

22:41:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Kleene_Algebra/outline.pdf

22:41:16 Finished Kleene_Algebra (0:01:24 elapsed time, 0:02:16 cpu time, factor 1.61)

22:41:17 Nominal2: theory FinFun

22:41:17 Building HOL-Cardinals ...

22:41:18 Timing HOL-Algebra (2 threads, 88.261s elapsed time, 165.904s cpu time, 9.696s GC time, factor 1.88)

22:41:18 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra

22:41:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf

22:41:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf

22:41:18 Finished HOL-Algebra (0:02:11 elapsed time, 0:03:54 cpu time, factor 1.78)

22:41:19 HOL-Cardinals: theory Order_Union

22:41:19 HOL-Cardinals: theory Cardinal_Notations

22:41:19 Building LatticeProperties ...

22:41:19 HOL-Cardinals: theory Fun_More

22:41:19 HOL-Cardinals: theory Order_Relation_More

22:41:19 HOL-Cardinals: theory Wellorder_Extension

22:41:19 HOL-Cardinals: theory Wellfounded_More

22:41:19 HOL-Cardinals: theory Wellorder_Relation

22:41:20 HOL-Cardinals: theory Wellorder_Embedding

22:41:20 HOL-Cardinals: theory Wellorder_Constructions

22:41:21 LatticeProperties: theory Conj_Disj

22:41:21 LatticeProperties: theory Lattice_Prop

22:41:21 HOL-Cardinals: theory Cardinal_Order_Relation

22:41:21 HOL-Cardinals: theory Ordinal_Arithmetic

22:41:21 LatticeProperties: theory WellFoundedTransitive

22:41:21 LatticeProperties: theory Modular_Distrib_Lattice

22:41:22 LatticeProperties: theory Complete_Lattice_Prop

22:41:22 HOL-Cardinals: theory Cardinal_Arithmetic

22:41:22 HOL-Cardinals: theory Cardinals

22:41:23 HOL-Cardinals: theory Bounded_Set

22:41:23 LatticeProperties: theory Lattice_Ordered_Group

22:41:25 Nominal2: theory Multiset

22:41:25 Nominal2: theory Quotient_Syntax

22:41:25 Nominal2: theory Quotient_Option

22:41:25 Nominal2: theory Quotient_Product

22:41:25 Nominal2: theory Quotient_Set

22:41:26 Nominal2: theory Quotient_List

22:41:30 Nominal2: theory Nominal2_Base

22:41:35 Nominal2: theory Atoms

22:41:36 Nominal2: theory Eqvt

22:41:36 Nominal2: theory Nominal2_Abs

22:41:38 Nominal2: theory Nominal2_FCB

22:41:39 Nominal2: theory Nominal2

22:41:40 Timing LatticeProperties (2 threads, 3.629s elapsed time, 6.896s cpu time, 0.200s GC time, factor 1.90)

22:41:40 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LatticeProperties

22:41:40 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LatticeProperties/document.pdf

22:41:40 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LatticeProperties/outline.pdf

22:41:40 Finished LatticeProperties (0:00:21 elapsed time, 0:00:32 cpu time, factor 1.54)

22:41:40 Building Incompleteness ...

22:41:43 Incompleteness: theory FSet

22:41:43 Incompleteness: theory Infinite_Set

22:41:43 Timing Word_Lib (2 threads, 69.123s elapsed time, 130.184s cpu time, 3.036s GC time, factor 1.88)

22:41:43 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Word_Lib

22:41:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Word_Lib/document.pdf

22:41:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Word_Lib/outline.pdf

22:41:43 Finished Word_Lib (0:01:31 elapsed time, 0:02:43 cpu time, factor 1.78)

22:41:43 Building IP_Addresses ...

22:41:43 Incompleteness: theory Multiset

22:41:46 Incompleteness: theory Nat_Bijection

22:41:46 IP_Addresses: theory Char_ord

22:41:46 IP_Addresses: theory Code_Abstract_Nat

22:41:46 IP_Addresses: theory Code_Target_Nat

22:41:46 IP_Addresses: theory Code_Char

22:41:46 IP_Addresses: theory Code_Target_Int

22:41:47 IP_Addresses: theory Infinite_Set

22:41:47 IP_Addresses: theory Multiset

22:41:47 Incompleteness: theory HF

22:41:47 IP_Addresses: theory Option_ord

22:41:47 IP_Addresses: theory NumberWang_IPv4

22:41:48 IP_Addresses: theory NumberWang_IPv6

22:41:48 IP_Addresses: theory Word_More

22:41:48 Incompleteness: theory Ordinal

22:41:48 Incompleteness: theory Old_Datatype

22:41:49 Incompleteness: theory Rank

22:41:49 Incompleteness: theory OrdArith

22:41:49 Incompleteness: theory Phantom_Type

22:41:50 Incompleteness: theory Quotient_Syntax

22:41:50 Incompleteness: theory Quotient_Option

22:41:50 Incompleteness: theory Quotient_Product

22:41:50 Incompleteness: theory Quotient_Set

22:41:50 Incompleteness: theory Quotient_List

22:41:50 Incompleteness: theory Cardinality

22:41:51 Incompleteness: theory FinFun

22:41:52 IP_Addresses: theory List_More

22:41:52 IP_Addresses: theory Quicksort

22:41:53 IP_Addresses: theory Misc

22:41:54 Incompleteness: theory Nominal2_Base

22:41:58 Timing HOL-Cardinals (2 threads, 22.962s elapsed time, 42.000s cpu time, 1.672s GC time, factor 1.83)

22:41:58 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Cardinals

22:41:58 Finished HOL-Cardinals (0:00:41 elapsed time, 0:01:09 cpu time, factor 1.67)

22:41:58 Building Dependent_SIFUM_Type_Systems ...

22:41:59 Incompleteness: theory Nominal2_Abs

22:42:00 Dependent_SIFUM_Type_Systems: theory Preliminaries

22:42:01 Incompleteness: theory Nominal2_FCB

22:42:01 Incompleteness: theory Nominal2

22:42:02 Dependent_SIFUM_Type_Systems: theory Language

22:42:02 Dependent_SIFUM_Type_Systems: theory Security

22:42:06 Dependent_SIFUM_Type_Systems: theory Compositionality

22:42:08 Dependent_SIFUM_Type_Systems: theory LocallySoundModeUse

22:42:08 Dependent_SIFUM_Type_Systems: theory TypeSystem

22:42:11 IP_Addresses: theory Lib_Numbers_toString

22:42:11 IP_Addresses: theory Hs_Compat

22:42:11 IP_Addresses: theory Product_Lexorder

22:42:11 IP_Addresses: theory Lib_List_toString

22:42:11 IP_Addresses: theory Lib_Word_toString

22:42:11 IP_Addresses: theory Word_Next

22:42:12 IP_Addresses: theory WordInterval

22:42:15 Timing Nominal2 (2 threads, 33.178s elapsed time, 65.432s cpu time, 3.448s GC time, factor 1.97)

22:42:15 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nominal2

22:42:15 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nominal2/document.pdf

22:42:15 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nominal2/outline.pdf

22:42:15 Finished Nominal2 (0:01:04 elapsed time, 0:01:52 cpu time, factor 1.76)

22:42:15 Building HOL-Imperative_HOL ...

22:42:16 IP_Addresses: theory IP_Address

22:42:16 IP_Addresses: theory WordInterval_Sorted

22:42:17 HOL-Imperative_HOL: theory Adhoc_Overloading

22:42:17 HOL-Imperative_HOL: theory LaTeXsugar

22:42:17 HOL-Imperative_HOL: theory Monad_Syntax

22:42:17 HOL-Imperative_HOL: theory Nat_Bijection

22:42:18 HOL-Imperative_HOL: theory Old_Datatype

22:42:19 HOL-Imperative_HOL: theory Countable

22:42:21 IP_Addresses: theory IPv4

22:42:21 HOL-Imperative_HOL: theory Code_Abstract_Nat

22:42:21 HOL-Imperative_HOL: theory Code_Target_Int

22:42:21 HOL-Imperative_HOL: theory Code_Target_Nat

22:42:21 IP_Addresses: theory IPv6

22:42:21 HOL-Imperative_HOL: theory Multiset

22:42:21 HOL-Imperative_HOL: theory Code_Target_Numeral

22:42:21 HOL-Imperative_HOL: theory Heap

22:42:21 IP_Addresses: theory Prefix_Match

22:42:22 IP_Addresses: theory CIDR_Split

22:42:23 HOL-Imperative_HOL: theory Heap_Monad

22:42:26 HOL-Imperative_HOL: theory Array

22:42:26 HOL-Imperative_HOL: theory Ref

22:42:27 HOL-Imperative_HOL: theory List_Sublist

22:42:27 HOL-Imperative_HOL: theory Imperative_HOL

22:42:27 HOL-Imperative_HOL: theory Linked_Lists

22:42:27 HOL-Imperative_HOL: theory Overview

22:42:27 HOL-Imperative_HOL: theory Subarray

22:42:28 HOL-Imperative_HOL: theory Imperative_Quicksort

22:42:29 Incompleteness: theory SyntaxN

22:42:36 Incompleteness: theory Coding

22:42:36 Incompleteness: theory Predicates

22:42:38 Incompleteness: theory Sigma

22:42:44 Incompleteness: theory Coding_Predicates

22:42:49 HOL-Imperative_HOL: theory Imperative_Reverse

22:42:50 Incompleteness: theory Functions

22:42:50 Incompleteness: theory Pf_Predicates

22:42:52 HOL-Imperative_HOL: theory RBT_Impl

22:42:52 Incompleteness: theory Goedel_I

22:42:53 Incompleteness: theory II_Prelims

22:42:55 Incompleteness: theory Pseudo_Coding

22:42:56 Incompleteness: theory Quote

22:42:57 Incompleteness: theory Goedel_II

22:43:01 Timing Simpl (2 threads, 114.017s elapsed time, 209.352s cpu time, 12.960s GC time, factor 1.84)

22:43:01 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simpl

22:43:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simpl/document.pdf

22:43:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simpl/outline.pdf

22:43:01 Finished Simpl (0:03:07 elapsed time, 0:05:18 cpu time, factor 1.70)

22:43:01 Building Koenigsberg_Friendship_Base ...

22:43:04 Koenigsberg_Friendship_Base: theory AList

22:43:04 Koenigsberg_Friendship_Base: theory Congruence

22:43:06 Koenigsberg_Friendship_Base: theory Lattice

22:43:06 Koenigsberg_Friendship_Base: theory DAList

22:43:08 Koenigsberg_Friendship_Base: theory FuncSet

22:43:08 Koenigsberg_Friendship_Base: theory Graph

22:43:08 Koenigsberg_Friendship_Base: theory Group

22:43:09 Koenigsberg_Friendship_Base: theory Multiset

22:43:10 HOL-Imperative_HOL: theory Sorted_List

22:43:11 Koenigsberg_Friendship_Base: theory FiniteProduct

22:43:12 Koenigsberg_Friendship_Base: theory Ring

22:43:15 Koenigsberg_Friendship_Base: theory Factorial_Ring

22:43:16 Koenigsberg_Friendship_Base: theory MiscAlgebra

22:43:16 Koenigsberg_Friendship_Base: theory Fib

22:43:25 Koenigsberg_Friendship_Base: theory Euclidean_Algorithm

22:43:26 HOL-Imperative_HOL: theory SatChecker

22:43:35 Koenigsberg_Friendship_Base: theory Primes

22:43:35 HOL-Imperative_HOL: theory Imperative_HOL_ex

22:43:35 Koenigsberg_Friendship_Base: theory Cong

22:43:35 Koenigsberg_Friendship_Base: theory Eratosthenes

22:43:36 Koenigsberg_Friendship_Base: theory Residues

22:43:38 Koenigsberg_Friendship_Base: theory Euler_Criterion

22:43:38 Koenigsberg_Friendship_Base: theory Pocklington

22:43:39 Koenigsberg_Friendship_Base: theory Gauss

22:43:39 Koenigsberg_Friendship_Base: theory Quadratic_Reciprocity

22:43:39 Koenigsberg_Friendship_Base: theory Number_Theory

22:43:44 IP_Addresses: theory IP_Address_Parser

22:43:50 IP_Addresses: theory IP_Address_toString

22:44:05 Dependent_SIFUM_Type_Systems: theory Eisbach

22:44:05 Dependent_SIFUM_Type_Systems: theory Example

22:44:06 Dependent_SIFUM_Type_Systems: theory Eisbach_Tools

22:44:06 Dependent_SIFUM_Type_Systems: theory TypeSystemTactics

22:44:08 Dependent_SIFUM_Type_Systems: theory Example_Swap_Add

22:44:10 Dependent_SIFUM_Type_Systems: theory Example_TypeSystem

22:45:12 Timing Koenigsberg_Friendship_Base (2 threads, 97.060s elapsed time, 167.968s cpu time, 8.484s GC time, factor 1.73)

22:45:12 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship_Base

22:45:12 Finished Koenigsberg_Friendship_Base (0:02:10 elapsed time, 0:03:38 cpu time, factor 1.68)

22:45:13 Building JNF-HOL-Lib ...

22:45:16 JNF-HOL-Lib: theory Lattice_Syntax

22:45:16 JNF-HOL-Lib: theory Adhoc_Overloading

22:45:16 JNF-HOL-Lib: theory Order_Union

22:45:16 JNF-HOL-Lib: theory AList

22:45:17 JNF-HOL-Lib: theory Char_ord

22:45:17 JNF-HOL-Lib: theory Code_Abstract_Nat

22:45:17 JNF-HOL-Lib: theory Code_Binary_Nat

22:45:17 JNF-HOL-Lib: theory Code_Target_Nat

22:45:17 JNF-HOL-Lib: theory Code_Char

22:45:17 JNF-HOL-Lib: theory Disjoint_Sets

22:45:18 JNF-HOL-Lib: theory Fraction_Field

22:45:18 JNF-HOL-Lib: theory DAList

22:45:19 JNF-HOL-Lib: theory Code_Target_Int

22:45:19 JNF-HOL-Lib: theory Code_Target_Numeral

22:45:19 JNF-HOL-Lib: theory IArray

22:45:19 JNF-HOL-Lib: theory Infinite_Set

22:45:20 JNF-HOL-Lib: theory List_lexord

22:45:20 JNF-HOL-Lib: theory Mapping

22:45:20 JNF-HOL-Lib: theory Monad_Syntax

22:45:21 JNF-HOL-Lib: theory More_List

22:45:21 JNF-HOL-Lib: theory DAList_Multiset

22:45:22 JNF-HOL-Lib: theory Permutations

22:45:22 JNF-HOL-Lib: theory Phantom_Type

22:45:23 JNF-HOL-Lib: theory Cardinality

22:45:23 JNF-HOL-Lib: theory RBT_Impl

22:45:24 JNF-HOL-Lib: theory Ramsey

22:45:24 JNF-HOL-Lib: theory Simps_Case_Conv

22:45:24 JNF-HOL-Lib: theory Polynomial

22:45:30 Timing HOL-Imperative_HOL (2 threads, 144.812s elapsed time, 185.624s cpu time, 6.896s GC time, factor 1.28)

22:45:30 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Imperative_HOL

22:45:30 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Imperative_HOL/document.pdf

22:45:30 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

22:45:30 Finished HOL-Imperative_HOL (0:03:14 elapsed time, 0:08:25 cpu time, factor 2.60)

22:45:30 Building Graph_Theory ...

22:45:30 JNF-HOL-Lib: theory Fundamental_Theorem_Algebra

22:45:31 JNF-HOL-Lib: theory Wellorder_Extension

22:45:31 JNF-HOL-Lib: theory While_Combinator

22:45:32 Graph_Theory: theory Nat_Bijection

22:45:32 Graph_Theory: theory Infinite_Set

22:45:33 Graph_Theory: theory Old_Datatype

22:45:33 Graph_Theory: theory Liminf_Limsup

22:45:34 Graph_Theory: theory Countable

22:45:36 Graph_Theory: theory Countable_Set

22:45:36 Graph_Theory: theory Countable_Complete_Lattices

22:45:40 Graph_Theory: theory Order_Continuity

22:45:40 Graph_Theory: theory Extended_Nat

22:45:42 Graph_Theory: theory Extended_Real

22:45:47 Timing HOL-Library (2 threads, 280.415s elapsed time, 507.212s cpu time, 27.148s GC time, factor 1.81)

22:45:47 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Library

22:45:47 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Library/document.pdf

22:45:47 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Library/outline.pdf

22:45:47 Finished HOL-Library (0:06:40 elapsed time, 0:11:39 cpu time, factor 1.75)

22:45:48 Building Coinductive ...

22:45:56 Coinductive: theory Primes

22:45:56 Coinductive: theory L2_Norm

22:45:56 Coinductive: theory Inner_Product

22:45:57 Coinductive: theory Norm_Arith

22:45:58 Coinductive: theory Product_Vector

22:45:58 Graph_Theory: theory Disjoint_Sets

22:45:58 Graph_Theory: theory FuncSet

22:45:58 Coinductive: theory Euclidean_Space

22:45:59 Graph_Theory: theory Multiset

22:45:59 Graph_Theory: theory Rewrite

22:45:59 Graph_Theory: theory Rtrancl_On

22:45:59 Graph_Theory: theory Stuff

22:46:00 Graph_Theory: theory Digraph

22:46:00 Coinductive: theory Linear_Algebra

22:46:02 Graph_Theory: theory Arc_Walk

22:46:03 Graph_Theory: theory Permutations

22:46:03 Coinductive: theory Topology_Euclidean_Space

22:46:03 Graph_Theory: theory Vertex_Walk

22:46:04 Graph_Theory: theory Weighted_Graph

22:46:05 Graph_Theory: theory Funpow

22:46:05 Graph_Theory: theory Bidirected_Digraph

22:46:06 Graph_Theory: theory Pair_Digraph

22:46:06 Graph_Theory: theory Shortest_Path

22:46:06 Timing Dependent_SIFUM_Type_Systems (2 threads, 195.326s elapsed time, 288.320s cpu time, 10.264s GC time, factor 1.48)

22:46:06 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems

22:46:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/document.pdf

22:46:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/outline.pdf

22:46:06 Finished Dependent_SIFUM_Type_Systems (0:04:07 elapsed time, 0:06:10 cpu time, factor 1.50)

22:46:06 Building Deriving ...

22:46:12 Graph_Theory: theory Digraph_Component

22:46:13 Coinductive: theory Extended_Real_Limits

22:46:14 Deriving: theory More_Bits_Int

22:46:15 Graph_Theory: theory Digraph_Component_Vwalk

22:46:15 Graph_Theory: theory Digraph_Isomorphism

22:46:16 Graph_Theory: theory Subdivision

22:46:16 Deriving: theory Bits_Integer

22:46:16 Deriving: theory Word_Misc

22:46:17 Graph_Theory: theory Euler

22:46:17 Graph_Theory: theory Kuratowski

22:46:21 Graph_Theory: theory Graph_Theory

22:46:28 Deriving: theory Code_Target_Bits_Int

22:46:28 Deriving: theory Code_Target_ICF

22:46:28 Deriving: theory Uint32

22:46:30 Deriving: theory HashCode

22:46:33 Deriving: theory Comparator

22:46:34 Deriving: theory Compare

22:46:34 Deriving: theory Derive_Manager

22:46:34 Deriving: theory Generator_Aux

22:46:34 Deriving: theory Comparator_Generator

22:46:34 Deriving: theory Equality_Generator

22:46:35 Deriving: theory Equality_Instances

22:46:35 Deriving: theory Countable_Generator

22:46:35 Deriving: theory Compare_Generator

22:46:35 Deriving: theory RBT_Comparator_Impl

22:46:36 Deriving: theory Compare_Instances

22:46:36 Deriving: theory Compare_Rat

22:46:36 Deriving: theory Compare_Real

22:46:37 Deriving: theory Compare_Order_Instances

22:46:38 Deriving: theory RBT_Compare_Order_Impl

22:46:39 Deriving: theory Hash_Generator

22:46:39 Deriving: theory Hash_Instances

22:46:40 Deriving: theory Derive

22:46:41 Deriving: theory Derive_Examples

22:46:56 Coinductive: theory Resumption

22:46:56 Coinductive: theory Coinductive_Nat

22:46:57 Coinductive: theory Coinductive_List

22:46:57 Coinductive: theory CCPO_Topology

22:47:03 Coinductive: theory Coinductive_List_Prefix

22:47:03 Coinductive: theory Hamming_Stream

22:47:04 Coinductive: theory Koenigslemma

22:47:04 Coinductive: theory LMirror

22:47:04 Coinductive: theory Lazy_LList

22:47:05 Coinductive: theory Quotient_Coinductive_List

22:47:05 Coinductive: theory TLList

22:47:05 Coinductive: theory Coinductive_Stream

22:47:07 Coinductive: theory LList_CCPO_Topology

22:47:08 Coinductive: theory Lazy_TLList

22:47:08 Coinductive: theory Quotient_TLList

22:47:08 Coinductive: theory TLList_CCPO

22:47:09 Coinductive: theory TLList_CCPO_Examples

22:47:09 Coinductive: theory Coinductive

22:47:09 Coinductive: theory Coinductive_Examples

22:47:29 Timing JNF-HOL-Lib (2 threads, 88.198s elapsed time, 159.852s cpu time, 10.008s GC time, factor 1.81)

22:47:29 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/JNF-HOL-Lib

22:47:29 Finished JNF-HOL-Lib (0:02:16 elapsed time, 0:03:55 cpu time, factor 1.72)

22:47:30 Building JNF-AFP-Lib ...

22:47:35 Timing Jinja (2 threads, 401.875s elapsed time, 713.728s cpu time, 22.628s GC time, factor 1.78)

22:47:35 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jinja

22:47:35 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jinja/document.pdf

22:47:35 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jinja/outline.pdf

22:47:35 Finished Jinja (0:08:01 elapsed time, 0:14:03 cpu time, factor 1.75)

22:47:35 JNF-AFP-Lib: theory Derive_Manager

22:47:35 JNF-AFP-Lib: theory Comparator

22:47:35 JNF-AFP-Lib: theory Equal

22:47:36 JNF-AFP-Lib: theory Closure_Set

22:47:36 Timing Graph_Theory (2 threads, 86.187s elapsed time, 162.780s cpu time, 8.888s GC time, factor 1.89)

22:47:36 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Graph_Theory

22:47:36 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Graph_Theory/document.pdf

22:47:36 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Graph_Theory/outline.pdf

22:47:36 Finished Graph_Theory (0:02:05 elapsed time, 0:03:43 cpu time, factor 1.78)

22:47:36 JNF-AFP-Lib: theory Extend_Partial_Order

22:47:36 JNF-AFP-Lib: theory FunctionLemmas

22:47:36 JNF-AFP-Lib: theory Generator_Aux

22:47:36 Building LTL ...

22:47:36 Building MSO_Regex_Equivalence ...

22:47:36 JNF-AFP-Lib: theory Equality_Generator

22:47:36 JNF-AFP-Lib: theory Compare

22:47:37 JNF-AFP-Lib: theory Comparator_Generator

22:47:37 Timing Deriving (2 threads, 39.442s elapsed time, 60.940s cpu time, 3.316s GC time, factor 1.55)

22:47:37 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deriving

22:47:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deriving/document.pdf

22:47:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deriving/outline.pdf

22:47:37 Finished Deriving (0:01:30 elapsed time, 0:02:46 cpu time, factor 1.83)

22:47:37 JNF-AFP-Lib: theory Equality_Instances

22:47:37 JNF-AFP-Lib: theory IArray_Addenda

22:47:37 JNF-AFP-Lib: theory Compare_Generator

22:47:38 Building Formula_Derivatives ...

22:47:38 JNF-AFP-Lib: theory IArray_Haskell

22:47:38 JNF-AFP-Lib: theory List_Fusion

22:47:38 JNF-AFP-Lib: theory Compare_Instances

22:47:38 JNF-AFP-Lib: theory Containers_Auxiliary

22:47:39 JNF-AFP-Lib: theory Normalized_Fraction

22:47:39 JNF-AFP-Lib: theory Lexicographic_Order

22:47:39 JNF-AFP-Lib: theory Set_Linorder

22:47:39 JNF-AFP-Lib: theory Containers_Generator

22:47:40 JNF-AFP-Lib: theory Collection_Enum

22:47:41 JNF-AFP-Lib: theory Collection_Eq

22:47:42 JNF-AFP-Lib: theory DList_Set

22:47:42 JNF-AFP-Lib: theory RBT_Comparator_Impl

22:47:44 LTL: theory LTL

22:47:44 MSO_Regex_Equivalence: theory Comparator

22:47:44 MSO_Regex_Equivalence: theory Derive_Manager

22:47:44 MSO_Regex_Equivalence: theory Generator_Aux

22:47:44 MSO_Regex_Equivalence: theory List_Index

22:47:45 MSO_Regex_Equivalence: theory List_More

22:47:45 MSO_Regex_Equivalence: theory Compare

22:47:45 MSO_Regex_Equivalence: theory Comparator_Generator

22:47:45 Formula_Derivatives: theory Comparator

22:47:45 Formula_Derivatives: theory Coinductive_Language

22:47:46 MSO_Regex_Equivalence: theory Compare_Generator

22:47:46 MSO_Regex_Equivalence: theory Compare_Instances

22:47:46 Formula_Derivatives: theory Compare

22:47:47 Formula_Derivatives: theory Derive_Manager

22:47:47 Formula_Derivatives: theory FSet_More

22:47:47 Formula_Derivatives: theory Generator_Aux

22:47:47 JNF-AFP-Lib: theory RBT_ext

22:47:47 Formula_Derivatives: theory Comparator_Generator

22:47:47 Formula_Derivatives: theory List_Index

22:47:48 Formula_Derivatives: theory While_Default

22:47:48 Formula_Derivatives: theory Compare_Generator

22:47:48 Formula_Derivatives: theory Compare_Instances

22:47:49 JNF-AFP-Lib: theory Regular_Set

22:47:50 JNF-AFP-Lib: theory Collection_Order

22:47:51 MSO_Regex_Equivalence: theory Pi_Regular_Set

22:47:51 MSO_Regex_Equivalence: theory Pi_Regular_Exp

22:47:51 JNF-AFP-Lib: theory Regular_Exp

22:47:52 JNF-AFP-Lib: theory RBT_Mapping2

22:47:53 LTL: theory LTL_Rewrite

22:47:54 JNF-AFP-Lib: theory RBT_Set2

22:47:55 JNF-AFP-Lib: theory NDerivative

22:47:56 Formula_Derivatives: theory WS1S_Prelim

22:47:56 Formula_Derivatives: theory Automaton

22:47:56 JNF-AFP-Lib: theory Relation_Interpretation

22:47:56 JNF-AFP-Lib: theory RingModuleFacts

22:47:56 Formula_Derivatives: theory Abstract_Formula

22:47:58 JNF-AFP-Lib: theory MonoidSums

22:47:58 LTL: theory LTL_Example

22:47:58 JNF-AFP-Lib: theory LinearCombinations

22:47:59 JNF-AFP-Lib: theory Seq

22:48:00 JNF-AFP-Lib: theory Show

22:48:01 JNF-AFP-Lib: theory Show_Instances

22:48:03 JNF-AFP-Lib: theory Missing_Unsorted

22:48:05 JNF-AFP-Lib: theory Field_as_Ring

22:48:06 JNF-AFP-Lib: theory Polynomial_Factorial

22:48:08 JNF-AFP-Lib: theory SumSpaces

22:48:10 JNF-AFP-Lib: theory Set_Impl

22:48:18 JNF-AFP-Lib: theory Missing_Polynomial

22:48:19 JNF-AFP-Lib: theory Utility

22:48:20 JNF-AFP-Lib: theory VectorSpace

22:48:28 JNF-AFP-Lib: theory Equivalence_Checking

22:48:28 JNF-AFP-Lib: theory Regexp_Method

22:48:29 JNF-AFP-Lib: theory Abstract_Rewriting

22:48:30 JNF-AFP-Lib: theory Ring_Hom

22:48:30 JNF-AFP-Lib: theory Relative_Rewriting

22:48:31 JNF-AFP-Lib: theory SN_Orders

22:48:31 MSO_Regex_Equivalence: theory Pi_Derivatives

22:48:32 MSO_Regex_Equivalence: theory PNormalization

22:48:32 MSO_Regex_Equivalence: theory Pi_Regular_Exp_Dual

22:48:33 JNF-AFP-Lib: theory Ordered_Semiring

22:48:33 JNF-AFP-Lib: theory SN_Order_Carrier

22:48:34 Timing Coinductive (2 threads, 109.118s elapsed time, 185.144s cpu time, 7.752s GC time, factor 1.70)

22:48:34 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive

22:48:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive/document.pdf

22:48:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive/outline.pdf

22:48:34 Finished Coinductive (0:02:45 elapsed time, 0:04:35 cpu time, factor 1.67)

22:48:34 Building Slicing ...

22:48:38 Slicing: theory AuxLemmas

22:48:38 Slicing: theory BitVector

22:48:38 Slicing: theory BasicDefs

22:48:39 Slicing: theory Com

22:48:40 Slicing: theory CFG

22:48:40 Slicing: theory CFGExit

22:48:40 Slicing: theory Postdomination

22:48:41 Slicing: theory DynStandardControlDependence

22:48:41 Slicing: theory DynWeakControlDependence

22:48:41 Slicing: theory StandardControlDependence

22:48:41 Slicing: theory WeakControlDependence

22:48:41 Slicing: theory CFG_wf

22:48:41 Slicing: theory CFGExit_wf

22:48:42 Slicing: theory DynDataDependence

22:48:42 Slicing: theory DataDependence

22:48:42 Slicing: theory PDG

22:48:42 Slicing: theory DynPDG

22:48:43 MSO_Regex_Equivalence: theory Init_Normalization

22:48:43 Slicing: theory DependentLiveVariables

22:48:43 Slicing: theory Distance

22:48:44 Slicing: theory Observable

22:48:44 Slicing: theory SemanticsCFG

22:48:44 Slicing: theory WeakOrderDependence

22:48:44 Slicing: theory Slice

22:48:44 Slicing: theory ControlDependenceRelations

22:48:44 Slicing: theory DynSlice

22:48:46 Slicing: theory Labels

22:48:46 Slicing: theory Semantics

22:48:46 Slicing: theory CDepInstantiations

22:48:46 Slicing: theory WCFG

22:48:47 Slicing: theory JVMCFG

22:48:48 Slicing: theory Interpretation

22:48:48 Slicing: theory WellFormed

22:48:49 Slicing: theory AdditionalLemmas

22:48:49 Slicing: theory DynamicControlDependences

22:48:49 Slicing: theory WEquivalence

22:48:49 Slicing: theory SemanticsWellFormed

22:48:50 Slicing: theory StaticControlDependences

22:48:52 Timing LTL (2 threads, 30.537s elapsed time, 53.752s cpu time, 2.336s GC time, factor 1.76)

22:48:52 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL

22:48:52 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL/document.pdf

22:48:52 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL/outline.pdf

22:48:52 Finished LTL (0:01:15 elapsed time, 0:01:59 cpu time, factor 1.59)

22:48:52 Building HRB-Slicing ...

22:48:55 Slicing: theory JVMInterpretation

22:48:56 Slicing: theory JVMCFG_wf

22:48:56 HRB-Slicing: theory AuxLemmas

22:48:56 Slicing: theory JVMPostdomination

22:48:56 HRB-Slicing: theory BasicDefs

22:48:57 Slicing: theory SemanticsWF

22:48:57 Formula_Derivatives: theory Presburger_Formula

22:48:57 Formula_Derivatives: theory WS1S_Alt_Formula

22:48:58 Timing IP_Addresses (2 threads, 353.035s elapsed time, 682.760s cpu time, 33.980s GC time, factor 1.93)

22:48:58 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses

22:48:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses/document.pdf

22:48:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses/outline.pdf

22:48:58 Finished IP_Addresses (0:07:15 elapsed time, 0:13:39 cpu time, factor 1.88)

22:48:59 HRB-Slicing: theory CFG

22:48:59 HRB-Slicing: theory Com

22:48:59 Building Group-Ring-Module ...

22:49:01 Slicing: theory JVMControlDependences

22:49:01 Slicing: theory Slicing

22:49:03 HRB-Slicing: theory Labels

22:49:03 HRB-Slicing: theory ProcState

22:49:03 HRB-Slicing: theory PCFG

22:49:04 HRB-Slicing: theory CFGExit

22:49:05 HRB-Slicing: theory Postdomination

22:49:05 HRB-Slicing: theory CFG_wf

22:49:06 HRB-Slicing: theory Distance

22:49:06 HRB-Slicing: theory ReturnAndCallNodes

22:49:06 HRB-Slicing: theory CFGExit_wf

22:49:07 HRB-Slicing: theory Observable

22:49:07 Group-Ring-Module: theory Algebra1