Started by an SCM change
[EnvInject] - Loading node environment variables.
Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
searching for changes
no changes found
[isabelle-all] $ hg update --clean --rev default
1 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-all] $ hg log --rev . --template {node}
[isabelle-all] $ hg log --rev . --template {rev}
[isabelle-all] $ hg log --rev 2c48be88f84718fa75d0e09779dba679fcb7a26d --template exists\n
exists
[isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(2c48be88f84718fa75d0e09779dba679fcb7a26d)" --encoding UTF-8 --encodingmode replace
[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
469 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 51034f90c51c656ab647f5f8bc53dfcaefab41e3 --template exists\n
exists
[afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(51034f90c51c656ab647f5f8bc53dfcaefab41e3)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins595160143016447298.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ bin/isabelle ocaml_setup
The following actions will be performed:
∗ install base-bigarray base
∗ install ocaml-base-compiler 4.05.0 [required by ocaml]
∗ install base-threads base
∗ install conf-gmp 1
∗ install conf-perl 1
∗ install base-unix base
∗ install conf-m4 1
∗ install ocaml-config 1 [required by ocaml]
∗ install ocaml 4.05.0 [required by ocamlfind, zarith]
∗ install ocamlfind 1.8.0
∗ install zarith 1.7
===== ∗ 11 =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ocaml-base-compiler.4.05.0] found in cache
[ocamlfind.1.8.0] found in cache
[zarith.1.7] found in cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed conf-gmp.1
∗ installed conf-m4.1
∗ installed conf-perl.1
∗ installed ocaml-base-compiler.4.05.0
∗ installed ocaml-config.1
∗ installed ocaml.4.05.0
∗ installed ocamlfind.1.8.0
∗ installed zarith.1.7
Done.
# Run eval $(opam env) to update the current shell environment
[NOTE] Package zarith is already installed (current version is 1.7).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.4.4
+ bin/isabelle ci_build_all
=== CONFIGURATION ===
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 10, threads = 4, numa = false
=== BUILD ===
Build started at Thu, 21 Mar 2019 18:54:18 GMT
Isabelle id ab8aad4aa76e
AFP id 51034f90c51c
=== LOG ===
Session Pure/Pure
Session CTT/CTT
Session Cube/Cube
Session FOL/FOL
Session CCL/CCL
Session FOL/FOL-ex
Session FOLP/FOLP
Session FOLP/FOLP-ex
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/AnselmGod (AFP)
Session AFP/AxiomaticCategoryTheory (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/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session HOL/HOL-Eisbach
Session AFP/Allen_Calculus (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hoare
Session AFP/Case_Labeling (AFP)
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Efficient-Mergesort (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/FinFun (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Cardinals (timing)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Sort_Encodings (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/JNF-HOL-Lib (AFP)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Bernoulli (AFP)
Session AFP/Cartan_FP (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Topology (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Lp (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Isar_Examples
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Lehmer (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Induct
Session HOL/HOL-Matrix_LP
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mutabelle
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-TPTP
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Pell (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Matrix (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Farkas (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Mirabelle
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-NanoJava
Session HOL/HOL-Prolog
Session HOL/HOL-Real_Asymp
Session HOL/HOL-Real_Asymp-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-Types_To_Sets
Session AFP/Smooth_Manifolds (AFP)
Session HOL/HOL-Word (main timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Word-SMT_Examples (timing)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Show (AFP)
Session AFP/JNF-AFP-Lib (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/CakeML (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
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/Consensus_Refined (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IMP2 (AFP)
Session Doc/Implementation (doc)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/InfPathElimination (AFP)
Session Doc/Isar_Ref (doc)
Session Doc/JEdit (doc)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/KAD (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/Jinja (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/LTL_to_DRA (AFP)
Session AFP/List_Update (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Kruskal (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/Menger (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (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/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/XML (AFP)
Session AFP/Pre_Polynomial_Factorization (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Pre_BZ (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Stern_Brocot (AFP)
Session HOL/HOL-Proofs-ex
Session Tools/Haskell
Session Doc/Intro (doc)
Session LCF/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Tools/SML
Session Sequents/Sequents
Session Doc/Sledgehammer (doc)
Session Tools/Spec_Check
Session AFP/Regex_Equivalence (AFP)
Session Doc/System (doc)
Session ZF/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session ZF/ZF-AC
Session ZF/ZF-Coind
Session ZF/ZF-Constructible
Session ZF/ZF-IMP
Session ZF/ZF-Induct
Session ZF/ZF-UNITY (timing)
Session ZF/ZF-Resid
Session ZF/ZF-ex
Running Smooth_Manifolds ...
Running HOL-Data_Structures ...
Running Valuation ...
Running Verified-Prover ...
Running Higher_Order_Terms ...
Running Lambda_Free_EPO ...
Running Lambda_Free_KBOs ...
Running Lambda_Free_RPOs ...
HOL-Data_Structures: theory HOL-Data_Structures.Less_False
Running Functional_Ordered_Resolution_Prover ...
HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Cmp
HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less
HOL-Data_Structures: theory HOL-Data_Structures.Tree2
Running Noninterference_Generic_Unwinding ...
HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del
HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del
Smooth_Manifolds: theory HOL-Library.Function_Algebras
Smooth_Manifolds: theory HOL-Library.Quotient_Syntax
Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites
Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets
Verified-Prover: theory Verified-Prover.Prover
Smooth_Manifolds: theory HOL-Library.Quotient_Set
Higher_Order_Terms: theory HOL-Library.AList
Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading
Higher_Order_Terms: theory HOL-Library.Nat_Bijection
Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity
HOL-Data_Structures: theory HOL-Data_Structures.Tree23
HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs
Higher_Order_Terms: theory HOL-Library.Monad_Syntax
HOL-Data_Structures: theory HOL-Data_Structures.Trie
Higher_Order_Terms: theory HOL-Library.State_Monad
Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding
Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With
HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs
Valuation: theory Valuation.Valuation1
Lambda_Free_EPO: theory HOL-Cardinals.Order_Union
Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util
Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
HOL-Data_Structures: theory HOL-Data_Structures.Tree234
Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension
Higher_Order_Terms: theory HOL-Library.Old_Datatype
Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
Higher_Order_Terms: theory List-Index.List_Index
HOL-Data_Structures: theory HOL-Data_Structures.Isin2
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With
Higher_Order_Terms: theory HOL-Library.Countable
Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain
Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders
HOL-Data_Structures: theory HOL-Data_Structures.AA_Set
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On
Higher_Order_Terms: theory HOL-Library.FSet
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator
Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More
Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux
HOL-Data_Structures: theory HOL-Data_Structures.Lookup2
HOL-Data_Structures: theory HOL-Data_Structures.RBT
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension
HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad
HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set
HOL-Data_Structures: theory HOL-Data_Structures.AA_Map
Valuation: theory Valuation.Valuation2
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances
Functional_Ordered_Resolution_Prover: theory Nested_Multisets_Ordinals.Multiset_More
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq
HOL-Data_Structures: theory HOL-Library.Cancellation
Functional_Ordered_Resolution_Prover: theory Deriving.Compare
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator
Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Clausal_Logic
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
HOL-Data_Structures: theory HOL-Library.Multiset
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits
Lambda_Free_KBOs: theory HOL-Cardinals.Order_Union
Lambda_Free_KBOs: theory Abstract-Rewriting.Seq
Lambda_Free_KBOs: theory HOL-Library.While_Combinator
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Util
Lambda_Free_KBOs: theory HOL-Cardinals.Wellorder_Extension
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Bit
Lambda_Free_KBOs: theory Matrix.Utility
Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Numeric
Lambda_Free_KBOs: theory Regular-Sets.Regular_Set
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bit_Representation
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Herbrand_Interpretation
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ground_Resolution_Model
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Infinite_Chain
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Extension_Orders
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Inference_System
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Int
Functional_Ordered_Resolution_Prover: theory HOL-Word.Word_Miscellaneous
Valuation: theory Valuation.Valuation3
Lambda_Free_EPO: theory Lambda_Free_EPO.Chop
Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Typedef
Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator
Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_Nat
Higher_Order_Terms: theory HOL-Library.Finite_Map
Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO
HOL-Data_Structures: theory HOL-Library.Pattern_Aliases
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/outline.pdf
Verified-Prover FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Verified-Prover)
*** FEval (gs, g) e (NAtom p vs)\
*** \ FEval (gs, g) e (snd a) \
*** (\f\set list. FEval (gs, g) e (snd f))
*** 2. \n t gs g e a list p vs.
*** \init s; finite (deriv s); m \ fst ` deriv s;
*** \y.
*** (\u. (y, u) \ deriv s) \ y \ m;
*** (m, a # list) \ deriv s; n = m; is_env (gs, g) e; t = a # list;
*** snd a = PAtom p vs; NAtom p vs \ snd ` set list\
*** \ FEval (gs, g) e (PAtom p vs) \
*** FEval (gs, g) e (NAtom p vs)
*** 3. \n t gs g e a list.
*** \init s; finite (deriv s); m \ fst ` deriv s;
*** \y.
*** (\u. (y, u) \ deriv s) \ y \ m;
*** (m, a # list) \ deriv s; n = m; is_env (gs, g) e; t = a # list;
*** \p vs.
*** snd a = NAtom p vs \
*** PAtom p vs \ snd ` set list\
*** \ FEval (gs, g) e (snd a) \
*** (\f\set list. FEval (gs, g) e (snd f))
*** 4. \n t gs g e.
*** \init s; finite (deriv s); m \ fst ` deriv s;
*** \y.
*** (\u. (y, u) \ deriv s) \ y \ m;
*** (m, t) \ deriv s; n = m; is_env (gs, g) e;
*** \ is_axiom (s_of_ns t)\
*** \ \f.
*** f \ set (s_of_ns t) \ FEval (gs, g) e f
*** 5. \n.
*** \init s; finite (deriv s); m \ fst ` deriv s;
*** \y u. (y, u) \ deriv s \ y \ m;
*** \na t.
*** n = m - na \ (na, t) \ deriv s \
*** Svalid (s_of_ns t)\
*** \ \na t.
*** Suc n = m - na \
*** (na, t) \ deriv s \
*** Svalid (s_of_ns t)
*** At command "apply" (line 609 of "$AFP/Verified-Prover/Prover.thy")
Functional_Ordered_Resolution_Prover: theory Matrix.Utility
HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS
HOL-Data_Structures: theory HOL-Library.Tree
Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ordered_Ground_Resolution
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_List
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bool_List_Representation
Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates
Lambda_Free_KBOs: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Map2
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Abstract_Substitution
Functional_Ordered_Resolution_Prover: theory Native_Word.More_Bits_Int
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Encoding
HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set
Functional_Ordered_Resolution_Prover: theory HOL-Word.Word
HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap
Lambda_Free_KBOs: theory Regular-Sets.NDerivative
Lambda_Free_KBOs: theory Regular-Sets.Relation_Interpretation
Functional_Ordered_Resolution_Prover: theory Native_Word.Bits_Integer
HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map
HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map
Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set
HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline.pdf
Lambda_Free_RPOs FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_RPOs)
assumes "rpo_optim ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
Proofs for inductive predicate(s) "gt"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
locale rpo
fixes ground_heads_var :: "'v \ 's set"
and
gt_sym :: "'s \ 's \ bool"
(infix \>\<^sub>s\ 50)
and
extf ::
"'s \ (('s, 'v) tm
\ ('s, 'v) tm \ bool)
\ ('s, 'v) tm list
\ ('s, 'v) tm list \ bool"
and arity_sym :: "'s \ enat"
and arity_var :: "'v \ enat"
assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim"
### 0.466s elapsed time, 1.864s cpu time, 0.000s GC time
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
locale simple_rpo_instances
### theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
### 0.864s elapsed time, 3.432s cpu time, 0.204s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set
Lambda_Free_KBOs: theory Regular-Sets.Equivalence_Checking
Smooth_Manifolds: theory Smooth_Manifolds.Smooth
Smooth_Manifolds: theory Smooth_Manifolds.Chart
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp
Lambda_Free_KBOs: theory Regular-Sets.Regexp_Method
Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold
Lambda_Free_KBOs: theory Abstract-Rewriting.Abstract_Rewriting
Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function
Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Liminf
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Chain
Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Misc
HOL-Data_Structures: theory HOL-Data_Structures.Sorting
HOL-Data_Structures: theory HOL-Library.Tree_Real
Lambda_Free_KBOs: theory Abstract-Rewriting.SN_Orders
HOL-Data_Structures: theory HOL-Data_Structures.Balance
Higher_Order_Terms: theory Higher_Order_Terms.Term_Utils
Higher_Order_Terms: theory Higher_Order_Terms.Disjoint_Sets
Higher_Order_Terms: theory Higher_Order_Terms.Find_First
Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity
Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold
Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative
HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree
Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space
Smooth_Manifolds: theory Smooth_Manifolds.Sphere
HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map
Higher_Order_Terms: theory Deriving.Derive_Manager
Higher_Order_Terms: theory HOL-Library.Cancellation
Higher_Order_Terms: theory HOL-Library.Infinite_Set
Higher_Order_Terms: theory HOL-ex.Unification
Higher_Order_Terms: theory Datatype_Order_Generator.Derive_Aux
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation
Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space
Higher_Order_Terms: theory Datatype_Order_Generator.Order_Generator
HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT
Higher_Order_Terms: theory HOL-Library.Countable_Set
Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Monad
Higher_Order_Terms: theory HOL-Library.Multiset
Higher_Order_Terms: theory Higher_Order_Terms.Name
Higher_Order_Terms: theory HOL-Library.Countable_Complete_Lattices
Lambda_Free_KBOs: theory Polynomials.Polynomials
HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding
Noninterference_Generic_Unwinding FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Noninterference_Generic_Unwinding)
Loading theory "Noninterference_Generic_Unwinding.GenericUnwinding"
Proofs for inductive predicate(s) "rel_induct_auxp"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (ys @ [y']) \ {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (zs @ [z]) \ {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
### theory "Noninterference_Generic_Unwinding.GenericUnwinding"
### 1.837s elapsed time, 4.632s cpu time, 0.132s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/document -o pdf -n document
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline"
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (zs @ [z]) \ {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (ys @ [y']) \ {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Class
HOL-Data_Structures: theory HOL-Number_Theory.Fib
HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set
HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set
Higher_Order_Terms: theory Higher_Order_Terms.Term_Class
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline.pdf
Lambda_Free_EPO FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_EPO)
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_chop"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_diff"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_same"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory "Lambda_Free_EPO.Lambda_Free_EPO"
### 1.040s elapsed time, 3.800s cpu time, 0.160s GC time
\?X \ ?C; ?A \ ?X\
\ ?A \ \ ?C
?P ?a \ ?a \ {x. ?P x}
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking
Higher_Order_Terms: theory HOL-Library.Order_Continuity
HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method
Higher_Order_Terms: theory HOL-Library.Extended_Nat
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting
Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32
Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Proving_Process
Higher_Order_Terms: theory HOL-Library.Multiset_Order
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification
Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Util
Functional_Ordered_Resolution_Prover: theory Collections.HashCode
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Standard_Redundancy
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification
Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching
Functional_Ordered_Resolution_Prover: theory Deriving.Derive
Higher_Order_Terms: theory Higher_Order_Terms.Nterm
Higher_Order_Terms: theory Higher_Order_Terms.Term
Higher_Order_Terms: theory Higher_Order_Terms.Unification_Compat
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Encoding_KBO
Higher_Order_Terms: theory Higher_Order_Terms.Pats
Higher_Order_Terms: theory Higher_Order_Terms.Lambda_Free_Compat
Higher_Order_Terms: theory Higher_Order_Terms.Term_to_Nterm
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/outline.pdf
Valuation FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Valuation)
### ("_applC" ("_position" K) ("_position" P)) ("_position" j))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### an 0 \ 0
\Ring K; b\<^bsup>\ K\<^esup> \ carrier K;
?y \ carrier K; ?z \ carrier K\
\ (?y \ ?z) \\<^sub>r
b\<^bsup>\ K\<^esup> =
?y \\<^sub>r
b\<^bsup>\ K\<^esup> \
?z \\<^sub>r b\<^bsup>\ K\<^esup>
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/document -o pdf -n document
*** Failed to apply proof method (line 899 of "$AFP/Valuation/Valuation1.thy"):
*** goal (1 subgoal):
*** 1. \x.
*** \valuation K v; \x\carrier K. 0 < v x;
*** {x \ v ` carrier K. 0 < x} \ LBset 1;
*** AMin {x \ v ` carrier K. 0 < x} \ v ` carrier K \
*** 0 < AMin {x \ v ` carrier K. 0 < x};
*** \x.
*** x \ v ` carrier K \ 0 < x \
*** AMin {x \ v ` carrier K. 0 < x} \ x;
*** x \ carrier K; v x \ \; v x \ 0;
*** 0 < v x\
*** \ \a.
*** AMin {x \ v ` carrier K. 0 < x} = ant a
*** At command "apply" (line 899 of "$AFP/Valuation/Valuation1.thy")
*** Failed to apply proof method (line 947 of "$AFP/Valuation/Valuation1.thy"):
*** goal (1 subgoal):
*** 1. valuation K v \
*** \w\carrier K - {\}.
*** \z. v w = z *\<^sub>a AMin {x \ v ` carrier K. 0 < x}
*** At command "apply" (line 947 of "$AFP/Valuation/Valuation1.thy")
*** Failed to apply proof method (line 837 of "$AFP/Valuation/Valuation1.thy"):
*** goal (1 subgoal):
*** 1. valuation K v \
*** {x \ v ` carrier K. 0 < x} \ {}
*** At command "apply" (line 837 of "$AFP/Valuation/Valuation1.thy")
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline.pdf
Higher_Order_Terms FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Higher_Order_Terms)
### Introduced fixed type variable(s): 'd, 'e in "f__"
### Introduced fixed type variable(s): 'd in "X__"
### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__"
### Introduced fixed type variable(s): 'd, 'e in "R__"
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1)
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1)
### Introduced fixed type variable(s): 'd in "z__"
### Introduced fixed type variable(s): 'd in "P__"
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_2"
### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_1"
### Rule already declared as introduction (intro)
### \rel_option ?R ?x ?y;
### \a b. ?R a b \ rel_option ?R (?f a) (?g b)\
### \ rel_option ?R (?x \ ?f) (?y \ ?g)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline.pdf
Lambda_Free_KBOs FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_KBOs)
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_diff"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_same"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
consts
subst_zpassign ::
"('v \ ('s, 'v) tm)
\ ('v pvar \ zhmultiset)
\ 'v pvar \ zhmultiset"
### theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs"
### 3.647s elapsed time, 7.600s cpu time, 0.560s GC time
Loading theory "Lambda_Free_KBOs.Lambda_Free_KBOs"
locale simple_kbo_instances
### theory "Lambda_Free_KBOs.Lambda_Free_KBOs"
### 1.358s elapsed time, 2.720s cpu time, 0.000s GC time
Found termination order: "size <*mlex*> {}"
"(>\<^sub>h\<^sub>d)"
:: "('s, 'v) hd \ ('s, 'v) hd \ bool"
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline.pdf
Functional_Ordered_Resolution_Prover FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Functional_Ordered_Resolution_Prover)
compare_order: register types in class compare_order, options: (linorder) or ()
countable: register datatypes is class countable
equality: generate an equality function, options are () and (eq)
hash_code: generate a hash function, options are () and (hashcode)
hashable: register types in class hashable
linorder: register types in class linorder, options: (linorder) or ()
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")
### Ignoring duplicate rewrite rule:
### mset (filter ?P1 ?xs1) \ filter_mset ?P1 (mset ?xs1)
Testing conjecture with Quickcheck-narrowing...
[1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Data_Bits.hs.o )
[2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Typerep.hs.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Typerep.hs.o )
[3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Generated_Code.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Generated_Code.o )
[4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Narrowing_Engine.o )
[5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Main.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Main.o )
Linking /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/isabelle_quickcheck_narrowing ...
Quickcheck found no counterexample.
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document -o pdf -n document
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \