Failed to finish proof (line 31 of "~~/dirs/AFP/thys/Arithmetic_Geometric_Mean/AGM_Theta.thy"): goal (1 subgoal): 1. (jacobi_theta_nw_00 q)⇧2 + (jacobi_theta_nw_01 q)⇧2 = 2 * (jacobi_theta_nw_00 (q⇧2))⇧2 ⟹ (1 / 2) *⇩R ((θ⇩3 q)⇧2 + (θ⇩4 q)⇧2) = (θ⇩3 (q⇧2))⇧2 At command "by" (line 31 of "~~/dirs/AFP/thys/Arithmetic_Geometric_Mean/AGM_Theta.thy")
Timeout
Undefined fact: "eqloops_reversepath_cong" (line 1536 of "~~/dirs/AFP/thys/Detour_Calculus/Detour_Calculus.thy") At command "by" (line 1536 of "~~/dirs/AFP/thys/Detour_Calculus/Detour_Calculus.thy")
Solver verit: Solver terminated abnormally with error code 127 At command "by" (line 834 of "~~/dirs/AFP/thys/Difference_Bound_Matrices/DBM_Constraint_Systems.thy")
Timeout
Timeout
Timeout
Timeout
Failed to load theory "Rademacher_Series.Rademacher_Series_Concrete_Bounds" (unresolved "Rademacher_Series.Rademacher_Series")
Failed to apply initial proof method (line 711 of "~~/dirs/AFP/thys/Rademacher_Series/Rademacher_Series.thy"):
goal (1 subgoal):
1. η (apply_modgrp f τ) =
ε f * csqrt (modgrp_factor f τ) *
η τ
At command "by" (line 711 of "~~/dirs/AFP/thys/Rademacher_Series/Rademacher_Series.thy")
Timeout
Timeout
Timeout
Timeout
Failed to load theory "AOT.AOT_Definitions" (unresolved "AOT.AOT_semantics")
Failed to load theory "AOT.AOT_Axioms" (unresolved "AOT.AOT_Definitions")
Failed to load theory "AOT.AOT_PLM" (unresolved "AOT.AOT_Axioms")
Failed to load theory "AOT.AOT_BasicLogicalObjects" (unresolved "AOT.AOT_PLM")
Failed to load theory "AOT.AOT_RestrictedVariables" (unresolved "AOT.AOT_PLM")
Failed to load theory "AOT.AOT_ExtendedRelationComprehension" (unresolved "AOT.AOT_RestrictedVariables")
Failed to load theory "AOT.AOT_PossibleWorlds" (unresolved "AOT.AOT_BasicLogicalObjects", "AOT.AOT_PLM", "AOT.AOT_RestrictedVariables")
Failed to load theory "AOT.AOT_NaturalNumbers" (unresolved "AOT.AOT_ExtendedRelationComprehension", "AOT.AOT_PossibleWorlds")
Failed to load theory "AOT.AOT_misc" (unresolved "AOT.AOT_NaturalNumbers")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1029 of "~~/dirs/AFP/thys/AOT/AOT_semantics.thy")
Failed to load theory "Abel_Limit_Theorem.Binomial_Sqrt_Series_Boundary" (unresolved "Abel_Limit_Theorem.Abel_Limit_Theorem")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 291 of "~~/dirs/AFP/thys/Abel_Limit_Theorem/Abel_Limit_Theorem.thy")
Failed to load theory "Abortable_Linearizable_Modules.Consensus" (unresolved "Abortable_Linearizable_Modules.RDR")
Failed to load theory "Abortable_Linearizable_Modules.SLin" (unresolved "Abortable_Linearizable_Modules.RDR")
Failed to load theory "Abortable_Linearizable_Modules.Idempotence" (unresolved "Abortable_Linearizable_Modules.SLin")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 133 of "~~/dirs/AFP/thys/Abortable_Linearizable_Modules/RDR.thy")
/tmp/isabelle-isatest/bash_script12527875675661472231: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Real" (unresolved "Akra_Bazzi.Akra_Bazzi_Asymptotics")
Failed to load theory "Akra_Bazzi.Akra_Bazzi" (unresolved "Akra_Bazzi.Akra_Bazzi_Real")
Failed to load theory "Akra_Bazzi.Master_Theorem" (unresolved "Akra_Bazzi.Akra_Bazzi")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Method" (unresolved "Akra_Bazzi.Akra_Bazzi", "Akra_Bazzi.Master_Theorem")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Approximation" (unresolved "Akra_Bazzi.Akra_Bazzi_Method")
Failed to load theory "Akra_Bazzi.Master_Theorem_Examples" (unresolved "Akra_Bazzi.Akra_Bazzi_Approximation", "Akra_Bazzi.Akra_Bazzi_Method")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 241 of "~~/dirs/AFP/thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy")
/tmp/isabelle-isatest/bash_script10142649498950011824: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "Approximate_Model_Counting.ApproxMCCoreAnalysis" (unresolved "Approximate_Model_Counting.ApproxMCCore")
Failed to load theory "Approximate_Model_Counting.RandomXORHashFamily" (unresolved "Approximate_Model_Counting.RandomXOR")
Failed to load theory "Approximate_Model_Counting.ApproxMCAnalysis" (unresolved "Approximate_Model_Counting.ApproxMCCoreAnalysis", "Approximate_Model_Counting.RandomXORHashFamily")
Failed to load theory "Approximate_Model_Counting.CertCheck" (unresolved "Approximate_Model_Counting.ApproxMCAnalysis")
Failed to load theory "Approximate_Model_Counting.CertCheck_CNF_XOR" (unresolved "Approximate_Model_Counting.ApproxMCAnalysis", "Approximate_Model_Counting.CertCheck")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1315 of "~~/dirs/AFP/thys/Approximate_Model_Counting/RandomXOR.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 236 of "~~/dirs/AFP/thys/Approximate_Model_Counting/ApproxMCCore.thy")
Failed to load theory "Attack_Trees.Infrastructure" (unresolved "Attack_Trees.AT")
Failed to load theory "Attack_Trees.GDPRhealthcare" (unresolved "Attack_Trees.Infrastructure")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 343 of "~~/dirs/AFP/thys/Attack_Trees/AT.thy")
Failed to load theory "Auto2_Imperative_HOL.Interval_Tree" (unresolved "Auto2_Imperative_HOL.Interval")
Failed to load theory "Auto2_Imperative_HOL.Rect_Intersect" (unresolved "Auto2_Imperative_HOL.Interval_Tree")
Failed to load theory "Auto2_Imperative_HOL.Arrays_Impl" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.DynamicArray" (unresolved "Auto2_Imperative_HOL.Arrays_Impl")
Failed to load theory "Auto2_Imperative_HOL.Indexed_PQueue_Impl" (unresolved "Auto2_Imperative_HOL.DynamicArray")
Failed to load theory "Auto2_Imperative_HOL.Dijkstra_Impl" (unresolved "Auto2_Imperative_HOL.Indexed_PQueue_Impl")
Failed to load theory "Auto2_Imperative_HOL.Quicksort_Impl" (unresolved "Auto2_Imperative_HOL.Arrays_Impl")
Failed to load theory "Auto2_Imperative_HOL.BST_Impl" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.GCD_Impl" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.IntervalTree_Impl" (unresolved "Auto2_Imperative_HOL.Interval_Tree", "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.Rect_Intersect_Impl" (unresolved "Auto2_Imperative_HOL.IntervalTree_Impl", "Auto2_Imperative_HOL.Quicksort_Impl", "Auto2_Imperative_HOL.Rect_Intersect")
Failed to load theory "Auto2_Imperative_HOL.LinkedList" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.RBTree_Impl" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.Union_Find_Impl" (unresolved "Auto2_Imperative_HOL.SepAuto")
Failed to load theory "Auto2_Imperative_HOL.Connectivity_Impl" (unresolved "Auto2_Imperative_HOL.Union_Find_Impl")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 447 of "~~/dirs/AFP/thys/Auto2_Imperative_HOL/Imperative/SepAuto.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 31 of "~~/dirs/AFP/thys/Auto2_Imperative_HOL/Functional/Interval.thy")
Failed to load theory "BNF_CC.DDS" (unresolved "BNF_CC.Concrete_Examples")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 435 of "~~/dirs/AFP/thys/BNF_CC/Concrete_Examples.thy")
Failed to load theory "BTree.BPlusTree_SplitCE" (unresolved "BTree.BPlusTree_Set")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 579 of "~~/dirs/AFP/thys/BTree/BPlusTree_Set.thy")
Failed to load theory "Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof" (unresolved "Balog_Szemeredi_Gowers.Graph_Theory_Preliminaries", "Balog_Szemeredi_Gowers.Sumset_Triangle_Inequality")
Failed to load theory "Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Supplementary" (unresolved "Balog_Szemeredi_Gowers.Balog_Szemeredi_Gowers_Main_Proof")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 231 of "~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Graph_Theory_Preliminaries.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 141 of "~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Sumset_Triangle_Inequality.thy")
Failed to load theory "BenOr_Kozen_Reif.BKR_Proofs" (unresolved "BenOr_Kozen_Reif.Matrix_Equation_Construction")
Failed to load theory "BenOr_Kozen_Reif.Renegar_Proofs" (unresolved "BenOr_Kozen_Reif.BKR_Proofs")
Failed to load theory "BenOr_Kozen_Reif.BKR_Decision" (unresolved "BenOr_Kozen_Reif.BKR_Proofs")
Failed to load theory "BenOr_Kozen_Reif.Renegar_Decision" (unresolved "BenOr_Kozen_Reif.BKR_Decision", "BenOr_Kozen_Reif.Renegar_Proofs")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 264 of "~~/dirs/AFP/thys/BenOr_Kozen_Reif/Matrix_Equation_Construction.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1165 of "~~/dirs/AFP/thys/Bisimulation_Logic/Bisimulation_Logic.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 86 of "~~/dirs/AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy")
Failed to load theory "Broadcast_Psi.Simulation" (unresolved "Broadcast_Psi.Semantics")
Failed to load theory "Broadcast_Psi.Bisimulation" (unresolved "Broadcast_Psi.Simulation")
Failed to load theory "Broadcast_Psi.Sim_Pres" (unresolved "Broadcast_Psi.Simulation")
Failed to load theory "Broadcast_Psi.Bisim_Pres" (unresolved "Broadcast_Psi.Bisimulation", "Broadcast_Psi.Sim_Pres")
Failed to load theory "Broadcast_Psi.Sim_Struct_Cong" (unresolved "Broadcast_Psi.Simulation")
Failed to load theory "Broadcast_Psi.Bisim_Struct_Cong" (unresolved "Broadcast_Psi.Bisim_Pres", "Broadcast_Psi.Sim_Struct_Cong")
Failed to load theory "Broadcast_Psi.Bisim_Subst" (unresolved "Broadcast_Psi.Bisim_Struct_Cong")
Failed to load theory "Broadcast_Psi.Broadcast_Thms" (unresolved "Broadcast_Psi.Bisim_Pres", "Broadcast_Psi.Bisim_Struct_Cong", "Broadcast_Psi.Bisim_Subst", "Broadcast_Psi.Bisimulation", "Broadcast_Psi.Semantics", "Broadcast_Psi.Sim_Pres", "Broadcast_Psi.Sim_Struct_Cong", "Broadcast_Psi.Simulation")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 12453 of "~~/dirs/AFP/thys/Broadcast_Psi/Semantics.thy")
/tmp/isabelle-isatest/bash_script6297308872919197949: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "CHERI-C_Memory_Model.CHERI_C_Global_Environment" (unresolved "CHERI-C_Memory_Model.CHERI_C_Concrete_Memory_Model")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 730 of "~~/dirs/AFP/thys/CHERI-C_Memory_Model/CHERI_C_Concrete_Memory_Model.thy")
Failed to load theory "CRYSTALS-Kyber.Mod_Plus_Minus" (unresolved "CRYSTALS-Kyber.Kyber_spec")
Failed to load theory "CRYSTALS-Kyber.Abs_Qr" (unresolved "CRYSTALS-Kyber.Kyber_spec", "CRYSTALS-Kyber.Mod_Plus_Minus")
Failed to load theory "CRYSTALS-Kyber.Compress" (unresolved "CRYSTALS-Kyber.Abs_Qr", "CRYSTALS-Kyber.Kyber_spec", "CRYSTALS-Kyber.Mod_Plus_Minus")
Failed to load theory "CRYSTALS-Kyber.Crypto_Scheme" (unresolved "CRYSTALS-Kyber.Abs_Qr", "CRYSTALS-Kyber.Compress", "CRYSTALS-Kyber.Kyber_spec")
Failed to load theory "CRYSTALS-Kyber.Kyber_Values" (unresolved "CRYSTALS-Kyber.Crypto_Scheme")
Failed to load theory "CRYSTALS-Kyber.Powers3844" (unresolved "CRYSTALS-Kyber.Kyber_Values")
Failed to load theory "Number_Theoretic_Transform.NTT" (unresolved "Number_Theoretic_Transform.Preliminary_Lemmas")
Failed to load theory "CRYSTALS-Kyber.NTT_Scheme" (unresolved "CRYSTALS-Kyber.Crypto_Scheme", "Number_Theoretic_Transform.NTT")
Failed to load theory "CRYSTALS-Kyber.Crypto_Scheme_NTT" (unresolved "CRYSTALS-Kyber.Crypto_Scheme", "CRYSTALS-Kyber.NTT_Scheme")
Failed to load theory "CRYSTALS-Kyber.Kyber_NTT_Values" (unresolved "CRYSTALS-Kyber.Kyber_Values", "CRYSTALS-Kyber.NTT_Scheme", "CRYSTALS-Kyber.Powers3844")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 294 of "~~/dirs/AFP/thys/CRYSTALS-Kyber/Kyber_spec.thy")
Failed to load theory "CRYSTALS-Kyber.Mod_Plus_Minus" (unresolved "CRYSTALS-Kyber.Kyber_spec")
Failed to load theory "CRYSTALS-Kyber.Abs_Qr" (unresolved "CRYSTALS-Kyber.Kyber_spec", "CRYSTALS-Kyber.Mod_Plus_Minus")
Failed to load theory "CRYSTALS-Kyber.Compress" (unresolved "CRYSTALS-Kyber.Abs_Qr", "CRYSTALS-Kyber.Kyber_spec", "CRYSTALS-Kyber.Mod_Plus_Minus")
Failed to load theory "CRYSTALS-Kyber.Crypto_Scheme" (unresolved "CRYSTALS-Kyber.Abs_Qr", "CRYSTALS-Kyber.Compress", "CRYSTALS-Kyber.Kyber_spec")
Failed to load theory "CRYSTALS-Kyber_Security.Crypto_Scheme_new" (unresolved "CRYSTALS-Kyber.Crypto_Scheme")
Failed to load theory "CRYSTALS-Kyber_Security.Kyber_new_Values" (unresolved "CRYSTALS-Kyber_Security.Crypto_Scheme_new")
Failed to load theory "CRYSTALS-Kyber_Security.Finite_UNIV" (unresolved "CRYSTALS-Kyber.Kyber_spec")
Failed to load theory "CRYSTALS-Kyber_Security.Lemmas_for_spmf" (unresolved "CRYSTALS-Kyber_Security.Finite_UNIV")
Failed to load theory "CRYSTALS-Kyber_Security.MLWE" (unresolved "CRYSTALS-Kyber_Security.Lemmas_for_spmf")
Failed to load theory "CRYSTALS-Kyber_Security.Correct" (unresolved "CRYSTALS-Kyber.Crypto_Scheme", "CRYSTALS-Kyber_Security.MLWE")
Failed to load theory "CRYSTALS-Kyber_Security.Correct_new" (unresolved "CRYSTALS-Kyber_Security.Crypto_Scheme_new", "CRYSTALS-Kyber_Security.MLWE")
Failed to load theory "CRYSTALS-Kyber_Security.Kyber_gpv_IND_CPA" (unresolved "CRYSTALS-Kyber_Security.Correct_new")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 294 of "~~/dirs/AFP/thys/CRYSTALS-Kyber/Kyber_spec.thy")
Failed to load theory "CVP_Hardness.CVP_p" (unresolved "CVP_Hardness.Lattice_int")
Failed to load theory "CVP_Hardness.Additional_Lemmas" (unresolved "CVP_Hardness.Digits_int", "CVP_Hardness.Lattice_int")
Failed to load theory "CVP_Hardness.BHLE" (unresolved "CVP_Hardness.Additional_Lemmas")
Failed to load theory "CVP_Hardness.SVP_vec" (unresolved "CVP_Hardness.BHLE")
Failed to load theory "CVP_Hardness.CVP_vec" (unresolved "CVP_Hardness.Lattice_int")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 351 of "~~/dirs/AFP/thys/CVP_Hardness/Lattice_int.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 138 of "~~/dirs/AFP/thys/CVP_Hardness/Digits_int.thy")
Failed to load theory "CakeML.Big_Step_Fun_Equiv" (unresolved "CakeML.Evaluate_Clock")
Failed to load theory "CakeML.Evaluate_Single" (unresolved "CakeML.Evaluate_Clock")
Failed to load theory "CakeML.Big_Step_Unclocked_Single" (unresolved "CakeML.Big_Step_Fun_Equiv", "CakeML.Evaluate_Single")
Failed to load theory "CakeML.CakeML_Code" (unresolved "CakeML.Evaluate_Single")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 68 of "~~/dirs/AFP/thys/CakeML/Evaluate_Clock.thy")
Failed to load theory "Category_Set.Product" (unresolved "Category_Set.Cfunc")
Failed to load theory "Category_Set.Terminal" (unresolved "Category_Set.Cfunc", "Category_Set.Product")
Failed to load theory "Category_Set.Equalizer" (unresolved "Category_Set.Terminal")
Failed to load theory "Category_Set.Truth" (unresolved "Category_Set.Equalizer")
Failed to load theory "Category_Set.Equivalence" (unresolved "Category_Set.Truth")
Failed to load theory "Category_Set.Coproduct" (unresolved "Category_Set.Equivalence")
Failed to load theory "Category_Set.Axiom_Of_Choice" (unresolved "Category_Set.Coproduct")
Failed to load theory "Category_Set.Initial" (unresolved "Category_Set.Coproduct")
Failed to load theory "Category_Set.Exponential_Objects" (unresolved "Category_Set.Initial")
Failed to load theory "Category_Set.Cardinality" (unresolved "Category_Set.Exponential_Objects")
Failed to load theory "Category_Set.Nats" (unresolved "Category_Set.Exponential_Objects")
Failed to load theory "Category_Set.Pred_Logic" (unresolved "Category_Set.Coproduct")
Failed to load theory "Category_Set.Fixed_Points" (unresolved "Category_Set.Axiom_Of_Choice", "Category_Set.Cardinality", "Category_Set.Pred_Logic")
Failed to load theory "Category_Set.Quant_Logic" (unresolved "Category_Set.Exponential_Objects", "Category_Set.Pred_Logic")
Failed to load theory "Category_Set.Nat_Parity" (unresolved "Category_Set.Nats", "Category_Set.Quant_Logic")
Failed to load theory "Category_Set.Countable" (unresolved "Category_Set.Axiom_Of_Choice", "Category_Set.Cardinality", "Category_Set.Nat_Parity", "Category_Set.Nats")
Failed to load theory "Category_Set.ETCS" (unresolved "Category_Set.Axiom_Of_Choice", "Category_Set.Countable", "Category_Set.Fixed_Points", "Category_Set.Nats", "Category_Set.Quant_Logic")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 130 of "~~/dirs/AFP/thys/Category_Set/Cfunc.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 101 of "~~/dirs/AFP/thys/Chandy_Lamport/Co_Snapshot.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 913 of "~~/dirs/AFP/thys/Chomsky_Schuetzenberger/Chomsky_Schuetzenberger.thy")
Failed to load theory "CoSMeDis.Friend_Openness" (unresolved "CoSMeDis.Friend_State_Indistinguishability")
Failed to load theory "CoSMeDis.Friend_Value_Setup" (unresolved "CoSMeDis.Friend_Openness")
Failed to load theory "CoSMeDis.Friend" (unresolved "CoSMeDis.Friend_Value_Setup")
Failed to load theory "CoSMeDis.Friend_Network" (unresolved "CoSMeDis.Friend")
Failed to load theory "CoSMeDis.Friend_All" (unresolved "CoSMeDis.Friend_Network")
Failed to load theory "CoSMeDis.Friend_Request_Intro" (unresolved "CoSMeDis.Friend_Openness", "CoSMeDis.Friend_State_Indistinguishability")
Failed to load theory "CoSMeDis.Friend_Request_Value_Setup" (unresolved "CoSMeDis.Friend_Request_Intro")
Failed to load theory "CoSMeDis.Friend_Request" (unresolved "CoSMeDis.Friend_Request_Value_Setup")
Failed to load theory "CoSMeDis.Friend_Request_Network" (unresolved "CoSMeDis.Friend_Request")
Failed to load theory "CoSMeDis.Friend_Request_All" (unresolved "CoSMeDis.Friend_Request_Network")
Failed to load theory "CoSMeDis.Outer_Friend_Network" (unresolved "CoSMeDis.Outer_Friend_Issuer")
Failed to load theory "CoSMeDis.Outer_Friend_All" (unresolved "CoSMeDis.Outer_Friend_Network")
Failed to load theory "CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER" (unresolved "CoSMeDis.Post_Unwinding_Helper_ISSUER")
Failed to load theory "CoSMeDis.DYNAMIC_Post_ISSUER" (unresolved "CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER")
Failed to load theory "CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER" (unresolved "CoSMeDis.Post_Unwinding_Helper_ISSUER")
Failed to load theory "CoSMeDis.Independent_DYNAMIC_Post_ISSUER" (unresolved "CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER")
Failed to load theory "CoSMeDis.Independent_Post_Value_Setup_RECEIVER" (unresolved "CoSMeDis.Post_Unwinding_Helper_RECEIVER")
Failed to load theory "CoSMeDis.Independent_Post_RECEIVER" (unresolved "CoSMeDis.Independent_Post_Value_Setup_RECEIVER")
Failed to load theory "CoSMeDis.Independent_DYNAMIC_Post_Network" (unresolved "CoSMeDis.Independent_DYNAMIC_Post_ISSUER", "CoSMeDis.Independent_Post_RECEIVER")
Failed to load theory "CoSMeDis.Independent_Posts_Network" (unresolved "CoSMeDis.Independent_DYNAMIC_Post_Network")
Failed to load theory "CoSMeDis.Post_Value_Setup_ISSUER" (unresolved "CoSMeDis.Post_Unwinding_Helper_ISSUER")
Failed to load theory "CoSMeDis.Post_ISSUER" (unresolved "CoSMeDis.Post_Value_Setup_ISSUER")
Failed to load theory "CoSMeDis.Post_Value_Setup_RECEIVER" (unresolved "CoSMeDis.Post_Unwinding_Helper_RECEIVER")
Failed to load theory "CoSMeDis.Post_RECEIVER" (unresolved "CoSMeDis.Post_Value_Setup_RECEIVER")
Failed to load theory "CoSMeDis.DYNAMIC_Post_COMPOSE2" (unresolved "CoSMeDis.DYNAMIC_Post_ISSUER", "CoSMeDis.Post_RECEIVER")
Failed to load theory "CoSMeDis.DYNAMIC_Post_Network" (unresolved "CoSMeDis.DYNAMIC_Post_ISSUER", "CoSMeDis.Post_RECEIVER")
Failed to load theory "CoSMeDis.Post_COMPOSE2" (unresolved "CoSMeDis.Post_ISSUER", "CoSMeDis.Post_RECEIVER")
Failed to load theory "CoSMeDis.Post_Network" (unresolved "CoSMeDis.Post_ISSUER", "CoSMeDis.Post_RECEIVER")
Failed to load theory "CoSMeDis.Post_All" (unresolved "CoSMeDis.DYNAMIC_Post_COMPOSE2", "CoSMeDis.DYNAMIC_Post_Network", "CoSMeDis.Independent_Posts_Network", "CoSMeDis.Post_COMPOSE2", "CoSMeDis.Post_Network")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 83 of "~~/dirs/AFP/thys/CoSMeDis/Post_Confidentiality/Post_Unwinding_Helper_RECEIVER.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 89 of "~~/dirs/AFP/thys/CoSMeDis/Post_Confidentiality/Post_Unwinding_Helper_ISSUER.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 361 of "~~/dirs/AFP/thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 226 of "~~/dirs/AFP/thys/CoSMeDis/Friend_Confidentiality/Friend_State_Indistinguishability.thy")
Failed to load theory "CoSMed.Friend" (unresolved "CoSMed.Friend_Value_Setup")
Failed to load theory "CoSMed.Friend_Request" (unresolved "CoSMed.Friend_Request_Value_Setup")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 171 of "~~/dirs/AFP/thys/CoSMed/Traceback_Properties/Post_Visibility_Traceback.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 826 of "~~/dirs/AFP/thys/CoSMed/Post_Confidentiality/Post.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 203 of "~~/dirs/AFP/thys/CoSMed/Friend_Request_Confidentiality/Friend_Request_Value_Setup.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 204 of "~~/dirs/AFP/thys/CoSMed/Friend_Confidentiality/Friend_Value_Setup.thy")
/tmp/isabelle-isatest/bash_script1418440259097517416: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "Completeness_Decreasing_Diagrams_for_N1.Main_Result_DCR_N1" (unresolved "Completeness_Decreasing_Diagrams_for_N1.DCR3_Method")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1639 of "~~/dirs/AFP/thys/Completeness_Decreasing_Diagrams_for_N1/DCR3_Method.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1359 of "~~/dirs/AFP/thys/Completeness_Decreasing_Diagrams_for_N1/DCR3_Optimality.thy")
Failed to load theory "Complex_Bounded_Operators.Extra_Vector_Spaces" (unresolved "Complex_Bounded_Operators.Extra_General")
Failed to load theory "Complex_Bounded_Operators.Extra_Operator_Norm" (unresolved "Complex_Bounded_Operators.Extra_General", "Complex_Bounded_Operators.Extra_Vector_Spaces")
Failed to load theory "Complex_Bounded_Operators.Complex_Vector_Spaces" (unresolved "Complex_Bounded_Operators.Extra_General", "Complex_Bounded_Operators.Extra_Operator_Norm", "Complex_Bounded_Operators.Extra_Ordered_Fields", "Complex_Bounded_Operators.Extra_Vector_Spaces")
Failed to load theory "Complex_Bounded_Operators.Complex_Inner_Product0" (unresolved "Complex_Bounded_Operators.Complex_Vector_Spaces", "Complex_Bounded_Operators.Extra_Ordered_Fields")
Failed to load theory "Complex_Bounded_Operators.Complex_Inner_Product" (unresolved "Complex_Bounded_Operators.Complex_Inner_Product0")
Failed to load theory "Complex_Bounded_Operators.Complex_Euclidean_Space0" (unresolved "Complex_Bounded_Operators.Complex_Inner_Product")
Failed to load theory "Complex_Bounded_Operators.Complex_Bounded_Linear_Function0" (unresolved "Complex_Bounded_Operators.Complex_Euclidean_Space0", "Complex_Bounded_Operators.Complex_Inner_Product")
Failed to load theory "Complex_Bounded_Operators.One_Dimensional_Spaces" (unresolved "Complex_Bounded_Operators.Complex_Inner_Product", "Complex_Bounded_Operators.Extra_Operator_Norm")
Failed to load theory "Complex_Bounded_Operators.Complex_Bounded_Linear_Function" (unresolved "Complex_Bounded_Operators.Complex_Bounded_Linear_Function0", "Complex_Bounded_Operators.Complex_Inner_Product", "Complex_Bounded_Operators.One_Dimensional_Spaces")
Failed to load theory "Complex_Bounded_Operators.Complex_L2" (unresolved "Complex_Bounded_Operators.Complex_Bounded_Linear_Function")
Failed to load theory "Complex_Bounded_Operators.Cblinfun_Matrix" (unresolved "Complex_Bounded_Operators.Complex_L2", "Complex_Bounded_Operators.Extra_Jordan_Normal_Form")
Failed to load theory "Complex_Bounded_Operators.Cblinfun_Code" (unresolved "Complex_Bounded_Operators.Cblinfun_Matrix")
Failed to load theory "Complex_Bounded_Operators.Cblinfun_Code_Examples" (unresolved "Complex_Bounded_Operators.Cblinfun_Code")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 313 of "~~/dirs/AFP/thys/Complex_Bounded_Operators/extra/Extra_Jordan_Normal_Form.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 264 of "~~/dirs/AFP/thys/Complex_Bounded_Operators/extra/Extra_General.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 603 of "~~/dirs/AFP/thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy")
Failed to load theory "Concentrated_Liquidity_Market_Making_Operations.CLMM_Description" (unresolved "Concentrated_Liquidity_Market_Making_Operations.Grid_Information")
Failed to load theory "Concentrated_Liquidity_Market_Making_Operations.CLMM_Transformation" (unresolved "Concentrated_Liquidity_Market_Making_Operations.CLMM_Description")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1271 of "~~/dirs/AFP/thys/Concentrated_Liquidity_Market_Making_Operations/Grid_Information.thy")
Failed to load theory "CondNormReasHOL.mere_addition_lewis" (unresolved "CondNormReasHOL.DDLcube")
Failed to load theory "CondNormReasHOL.mere_addition_max" (unresolved "CondNormReasHOL.DDLcube")
Failed to load theory "CondNormReasHOL.mere_addition_opt" (unresolved "CondNormReasHOL.DDLcube")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 457 of "~~/dirs/AFP/thys/CondNormReasHOL/DDLcube.thy")
Failed to load theory "Constructive_Cryptography_CM.One_Time_Pad" (unresolved "Sigma_Commit_Crypto.Xor")
Failed to load theory "Constructive_Cryptography_CM.DH_OTP" (unresolved "Constructive_Cryptography_CM.One_Time_Pad")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 132 of "~~/dirs/AFP/thys/Sigma_Commit_Crypto/Xor.thy")
Failed to load theory "Correctness_Algebras.Tests" (unresolved "Subset_Boolean_Algebras.Subset_Boolean_Algebras")
Failed to load theory "Correctness_Algebras.Complete_Tests" (unresolved "Correctness_Algebras.Tests")
Failed to load theory "Correctness_Algebras.Preconditions" (unresolved "Correctness_Algebras.Tests")
Failed to load theory "Correctness_Algebras.Hoare" (unresolved "Correctness_Algebras.Complete_Tests", "Correctness_Algebras.Preconditions")
Failed to load theory "Correctness_Algebras.Pre_Post" (unresolved "Correctness_Algebras.Preconditions")
Failed to load theory "Correctness_Algebras.Relative_Domain" (unresolved "Correctness_Algebras.Tests")
Failed to load theory "Correctness_Algebras.Complete_Domain" (unresolved "Correctness_Algebras.Complete_Tests", "Correctness_Algebras.Relative_Domain")
Failed to load theory "Correctness_Algebras.Relative_Modal" (unresolved "Correctness_Algebras.Relative_Domain")
Failed to load theory "Correctness_Algebras.Domain" (unresolved "Correctness_Algebras.Tests")
Failed to load theory "Correctness_Algebras.Boolean_Semirings" (unresolved "Correctness_Algebras.Lattice_Ordered_Semirings")
Failed to load theory "Correctness_Algebras.Binary_Iterings_Strict" (unresolved "Correctness_Algebras.Binary_Iterings")
Failed to load theory "Correctness_Algebras.N_Algebras" (unresolved "Correctness_Algebras.Lattice_Ordered_Semirings")
Failed to load theory "Correctness_Algebras.Recursion" (unresolved "Correctness_Algebras.N_Algebras")
Failed to load theory "Correctness_Algebras.Test_Iterings" (unresolved "Correctness_Algebras.Tests")
Failed to load theory "Correctness_Algebras.Hoare_Modal" (unresolved "Correctness_Algebras.Complete_Domain", "Correctness_Algebras.Hoare", "Correctness_Algebras.Relative_Modal")
Failed to load theory "Correctness_Algebras.Pre_Post_Modal" (unresolved "Correctness_Algebras.Hoare_Modal", "Correctness_Algebras.Pre_Post")
Failed to load theory "Correctness_Algebras.Binary_Iterings_Nonstrict" (unresolved "Correctness_Algebras.Binary_Iterings", "Correctness_Algebras.Omega_Algebras")
Failed to load theory "Correctness_Algebras.Capped_Omega_Algebras" (unresolved "Correctness_Algebras.Omega_Algebras")
Failed to load theory "Correctness_Algebras.Domain_Iterings" (unresolved "Correctness_Algebras.Domain", "Correctness_Algebras.Lattice_Ordered_Semirings", "Correctness_Algebras.Omega_Algebras")
Failed to load theory "Correctness_Algebras.Domain_Recursion" (unresolved "Correctness_Algebras.Domain_Iterings")
Failed to load theory "Correctness_Algebras.Extended_Designs" (unresolved "Correctness_Algebras.Domain", "Correctness_Algebras.Omega_Algebras")
Failed to load theory "Correctness_Algebras.General_Refinement_Algebras" (unresolved "Correctness_Algebras.Omega_Algebras")
Failed to load theory "Correctness_Algebras.Monotonic_Boolean_Transformers_Instances" (unresolved "Correctness_Algebras.General_Refinement_Algebras", "Correctness_Algebras.Monotonic_Boolean_Transformers", "Correctness_Algebras.Pre_Post_Modal")
Failed to load theory "Correctness_Algebras.N_Omega_Algebras" (unresolved "Correctness_Algebras.Omega_Algebras", "Correctness_Algebras.Recursion")
Failed to load theory "Correctness_Algebras.N_Omega_Binary_Iterings" (unresolved "Correctness_Algebras.Binary_Iterings_Strict", "Correctness_Algebras.N_Omega_Algebras")
Failed to load theory "Correctness_Algebras.N_Semirings" (unresolved "Correctness_Algebras.Omega_Algebras", "Correctness_Algebras.Test_Iterings")
Failed to load theory "Correctness_Algebras.N_Semirings_Boolean" (unresolved "Correctness_Algebras.N_Semirings")
Failed to load theory "Correctness_Algebras.N_Semirings_Modal" (unresolved "Correctness_Algebras.N_Semirings_Boolean")
Failed to load theory "Correctness_Algebras.Recursion_Strict" (unresolved "Correctness_Algebras.N_Semirings")
Failed to load theory "Correctness_Algebras.N_Relation_Algebras" (unresolved "Correctness_Algebras.N_Omega_Algebras", "Stone_Relation_Algebras.Relation_Algebras")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 591 of "~~/dirs/AFP/thys/Stone_Relation_Algebras/Relation_Algebras.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 130 of "~~/dirs/AFP/thys/Correctness_Algebras/Omega_Algebras.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 153 of "~~/dirs/AFP/thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 45 of "~~/dirs/AFP/thys/Correctness_Algebras/Monotonic_Boolean_Transformers.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 137 of "~~/dirs/AFP/thys/Correctness_Algebras/Binary_Iterings.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 33 of "~~/dirs/AFP/thys/Subset_Boolean_Algebras/Subset_Boolean_Algebras.thy")
Failed to load theory "Crypto_Standards.FIPS180_4" (unresolved "Crypto_Standards.Words")
Failed to load theory "Crypto_Standards.FIPS180_4_Test_Vectors" (unresolved "Crypto_Standards.FIPS180_4")
Failed to load theory "Crypto_Standards.PKCS1v2_2" (unresolved "Crypto_Standards.Words")
Failed to load theory "Crypto_Standards.Efficient_Mod_Exp" (unresolved "Crypto_Standards.PKCS1v2_2")
Failed to load theory "Crypto_Standards.PKCS1v2_2_Interpretations" (unresolved "Crypto_Standards.FIPS180_4", "Crypto_Standards.PKCS1v2_2")
Failed to load theory "Crypto_Standards.FIPS198_1" (unresolved "Crypto_Standards.PKCS1v2_2_Interpretations", "Crypto_Standards.Words")
Failed to load theory "Crypto_Standards.FIPS198_1_Test_Vectors" (unresolved "Crypto_Standards.FIPS198_1")
Failed to load theory "Crypto_Standards.PKCS1v2_2_Test_Vectors" (unresolved "Crypto_Standards.Efficient_Mod_Exp", "Crypto_Standards.PKCS1v2_2_Interpretations")
Failed to load theory "Crypto_Standards.SEC1v2_0" (unresolved "Crypto_Standards.Words")
Failed to load theory "Crypto_Standards.Crypto_Standards" (unresolved "Crypto_Standards.FIPS180_4", "Crypto_Standards.FIPS198_1", "Crypto_Standards.PKCS1v2_2", "Crypto_Standards.SEC1v2_0")
Failed to load theory "Crypto_Standards.Efficient_SEC1" (unresolved "Crypto_Standards.Efficient_Mod_Exp", "Crypto_Standards.SEC1v2_0")
Failed to load theory "Crypto_Standards.FIPS186_4_Curves" (unresolved "Crypto_Standards.Efficient_SEC1")
Failed to load theory "Crypto_Standards.SEC1v2_0_Test_Vectors" (unresolved "Crypto_Standards.FIPS180_4", "Crypto_Standards.FIPS186_4_Curves")
Failed to load theory "Crypto_Standards.Test_Vectors" (unresolved "Crypto_Standards.FIPS180_4_Test_Vectors", "Crypto_Standards.FIPS198_1_Test_Vectors", "Crypto_Standards.PKCS1v2_2_Test_Vectors", "Crypto_Standards.SEC1v2_0_Test_Vectors")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 149 of "~~/dirs/AFP/thys/Crypto_Standards/Words.thy")
Failed to load theory "CubicalCategories.ICatoids" (unresolved "Catoids.Catoid")
Failed to load theory "CubicalCategories.CubicalCategories" (unresolved "CubicalCategories.ICatoids")
Failed to load theory "CubicalCategories.CubicalCategoriesConnections" (unresolved "CubicalCategories.CubicalCategories")
Failed to load theory "CubicalCategories.CubicalOmegaZeroCategoriesConnections" (unresolved "CubicalCategories.CubicalCategoriesConnections")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 879 of "~~/dirs/AFP/thys/Catoids/Catoid.thy")
Failed to load theory "DPRM_Theorem.Diophantine_Relations" (unresolved "DPRM_Theorem.Assignments")
Failed to load theory "DPRM_Theorem.Existential_Quantifier" (unresolved "DPRM_Theorem.Diophantine_Relations")
Failed to load theory "DPRM_Theorem.Modulo_Divisibility" (unresolved "DPRM_Theorem.Existential_Quantifier")
Failed to load theory "DPRM_Theorem.Equation_Setup" (unresolved "DPRM_Theorem.Diophantine_Relations")
Failed to load theory "DPRM_Theorem.Register_Machine_Sums" (unresolved "DPRM_Theorem.Diophantine_Relations", "DPRM_Theorem.RegisterMachineSimulation")
Failed to load theory "DPRM_Theorem.SingleStepRegister" (unresolved "DPRM_Theorem.RegisterMachineSimulation")
Failed to load theory "DPRM_Theorem.MultipleStepRegister" (unresolved "DPRM_Theorem.SingleStepRegister")
Failed to load theory "DPRM_Theorem.SingleStepState" (unresolved "DPRM_Theorem.RegisterMachineSimulation")
Failed to load theory "DPRM_Theorem.MultipleStepState" (unresolved "DPRM_Theorem.SingleStepState")
Failed to load theory "DPRM_Theorem.Alpha_Sequence" (unresolved "DPRM_Theorem.Exponentiation", "DPRM_Theorem.Modulo_Divisibility")
Failed to load theory "DPRM_Theorem.Exponential_Relation" (unresolved "DPRM_Theorem.Alpha_Sequence", "DPRM_Theorem.Exponentiation")
Failed to load theory "DPRM_Theorem.Digit_Function" (unresolved "DPRM_Theorem.Exponential_Relation")
Failed to load theory "DPRM_Theorem.Binomial_Coefficient" (unresolved "DPRM_Theorem.Digit_Function")
Failed to load theory "DPRM_Theorem.Binary_Orthogonal" (unresolved "DPRM_Theorem.Binomial_Coefficient")
Failed to load theory "DPRM_Theorem.Binary_Masking" (unresolved "DPRM_Theorem.Binary_Orthogonal")
Failed to load theory "DPRM_Theorem.Binary_And" (unresolved "DPRM_Theorem.Binary_Masking", "DPRM_Theorem.Binary_Orthogonal")
Failed to load theory "DPRM_Theorem.MachineMasking" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.RegisterMachineSimulation")
Failed to load theory "DPRM_Theorem.Constants_Equations" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.Equation_Setup", "DPRM_Theorem.MachineMasking")
Failed to load theory "DPRM_Theorem.MachineEquations" (unresolved "DPRM_Theorem.MachineMasking", "DPRM_Theorem.MultipleStepRegister", "DPRM_Theorem.MultipleStepState")
Failed to load theory "DPRM_Theorem.CommutationRelations" (unresolved "DPRM_Theorem.MachineEquations", "DPRM_Theorem.RegisterMachineSimulation")
Failed to load theory "DPRM_Theorem.Mask_Equations" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.Equation_Setup", "DPRM_Theorem.MachineMasking")
Failed to load theory "DPRM_Theorem.MultipleToSingleSteps" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.CommutationRelations", "DPRM_Theorem.MachineEquations")
Failed to load theory "DPRM_Theorem.RM_Sums_Diophantine" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.Equation_Setup", "DPRM_Theorem.Register_Machine_Sums")
Failed to load theory "DPRM_Theorem.Register_Equations" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.Equation_Setup", "DPRM_Theorem.MultipleStepRegister", "DPRM_Theorem.Register_Machine_Sums")
Failed to load theory "DPRM_Theorem.State_0_Equation" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.MultipleStepState", "DPRM_Theorem.RM_Sums_Diophantine")
Failed to load theory "DPRM_Theorem.State_d_Equation" (unresolved "DPRM_Theorem.State_0_Equation")
Failed to load theory "DPRM_Theorem.State_Unique_Equations" (unresolved "DPRM_Theorem.Binary_And", "DPRM_Theorem.Equation_Setup", "DPRM_Theorem.MultipleStepState", "DPRM_Theorem.Register_Machine_Sums")
Failed to load theory "DPRM_Theorem.All_State_Equations" (unresolved "DPRM_Theorem.State_Unique_Equations", "DPRM_Theorem.State_d_Equation")
Failed to load theory "DPRM_Theorem.All_Equations_Invariance" (unresolved "DPRM_Theorem.All_State_Equations", "DPRM_Theorem.Constants_Equations", "DPRM_Theorem.Mask_Equations", "DPRM_Theorem.Register_Equations")
Failed to load theory "DPRM_Theorem.All_Equations" (unresolved "DPRM_Theorem.All_Equations_Invariance")
Failed to load theory "DPRM_Theorem.Machine_Equation_Equivalence" (unresolved "DPRM_Theorem.All_Equations", "DPRM_Theorem.MachineEquations", "DPRM_Theorem.MultipleToSingleSteps")
Failed to load theory "DPRM_Theorem.DPRM" (unresolved "DPRM_Theorem.Machine_Equation_Equivalence")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 93 of "~~/dirs/AFP/thys/DPRM_Theorem/Diophantine/Exponentiation.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 98 of "~~/dirs/AFP/thys/DPRM_Theorem/Register_Machine/RegisterMachineSimulation.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 115 of "~~/dirs/AFP/thys/DPRM_Theorem/Diophantine/Assignments.thy")
Failed to load theory "Diophantine_Universal_Pairs.Lucas_Diophantine" (unresolved "Diophantine_Universal_Pairs.Lucas_Sequences")
Failed to load theory "Diophantine_Universal_Pairs.Tau_Reduction" (unresolved "Diophantine_Universal_Pairs.Bit_Counting")
Failed to load theory "Diophantine_Universal_Pairs.Lemma_4_4" (unresolved "Diophantine_Universal_Pairs.Lucas_Sequences")
Failed to load theory "Diophantine_Universal_Pairs.Algebra_Basics" (unresolved "Diophantine_Universal_Pairs.Lucas_Sequences")
Failed to load theory "Diophantine_Universal_Pairs.Masking" (unresolved "Diophantine_Universal_Pairs.Bit_Counting")
Failed to load theory "Diophantine_Universal_Pairs.Total_Degree" (unresolved "Diophantine_Universal_Pairs.Variables")
Failed to load theory "Diophantine_Universal_Pairs.Poly_Expansions" (unresolved "Diophantine_Universal_Pairs.Total_Degree")
Failed to load theory "Diophantine_Universal_Pairs.Substitutions" (unresolved "Diophantine_Universal_Pairs.Poly_Expansions")
Failed to load theory "Diophantine_Universal_Pairs.Type_Casting" (unresolved "Diophantine_Universal_Pairs.Substitutions")
Failed to load theory "Diophantine_Universal_Pairs.Total_Degree_Env" (unresolved "Diophantine_Universal_Pairs.Substitutions", "Diophantine_Universal_Pairs.Total_Degree")
Failed to load theory "Diophantine_Universal_Pairs.More_More_MPoly_Type" (unresolved "Diophantine_Universal_Pairs.Poly_Expansions", "Diophantine_Universal_Pairs.Substitutions", "Diophantine_Universal_Pairs.Total_Degree", "Diophantine_Universal_Pairs.Type_Casting", "Diophantine_Universal_Pairs.Variables")
Failed to load theory "Diophantine_Universal_Pairs.Diophantine_Definition" (unresolved "Diophantine_Universal_Pairs.More_More_MPoly_Type")
Failed to load theory "Diophantine_Universal_Pairs.Suitable_For_Coding" (unresolved "Diophantine_Universal_Pairs.Diophantine_Definition", "Diophantine_Universal_Pairs.Total_Degree_Env")
Failed to load theory "Diophantine_Universal_Pairs.J3_Polynomial" (unresolved "Diophantine_Universal_Pairs.Algebra_Basics", "Diophantine_Universal_Pairs.More_More_MPoly_Type")
Failed to load theory "Diophantine_Universal_Pairs.J3_Relations" (unresolved "Diophantine_Universal_Pairs.J3_Polynomial")
Failed to load theory "Diophantine_Universal_Pairs.Pi_Relations" (unresolved "Diophantine_Universal_Pairs.J3_Relations")
Failed to load theory "Diophantine_Universal_Pairs.Lemma_1_8_Defs" (unresolved "Diophantine_Universal_Pairs.Bit_Counting", "Diophantine_Universal_Pairs.More_More_MPoly_Type")
Failed to load theory "Diophantine_Universal_Pairs.Lemma_1_8_Coding" (unresolved "Diophantine_Universal_Pairs.Lemma_1_8_Defs")
Failed to load theory "Diophantine_Universal_Pairs.Lemma_1_8" (unresolved "Diophantine_Universal_Pairs.Lemma_1_8_Coding")
Failed to load theory "Diophantine_Universal_Pairs.Poly_Extract" (unresolved "Diophantine_Universal_Pairs.More_More_MPoly_Type")
Failed to load theory "Diophantine_Universal_Pairs.Poly_Degree" (unresolved "Diophantine_Universal_Pairs.More_More_MPoly_Type", "Diophantine_Universal_Pairs.Poly_Extract", "Diophantine_Universal_Pairs.Total_Degree_Env")
Failed to load theory "Diophantine_Universal_Pairs.Coding_Theorem_Definitions" (unresolved "Diophantine_Universal_Pairs.Bit_Counting", "Diophantine_Universal_Pairs.More_More_MPoly_Type", "Diophantine_Universal_Pairs.Poly_Degree", "Diophantine_Universal_Pairs.Poly_Extract", "Diophantine_Universal_Pairs.Total_Degree_Env")
Failed to load theory "Diophantine_Universal_Pairs.Coding_Theorem" (unresolved "Diophantine_Universal_Pairs.Coding_Theorem_Definitions", "Diophantine_Universal_Pairs.Lemma_1_8", "Diophantine_Universal_Pairs.Masking", "Diophantine_Universal_Pairs.Tau_Reduction")
Failed to load theory "Diophantine_Universal_Pairs.Lower_Bounds" (unresolved "Diophantine_Universal_Pairs.Coding_Theorem_Definitions", "Diophantine_Universal_Pairs.Lemma_1_8_Coding", "Diophantine_Universal_Pairs.Suitable_For_Coding")
Failed to load theory "Diophantine_Universal_Pairs.Pell_Equation" (unresolved "Diophantine_Universal_Pairs.Lucas_Sequences")
Failed to load theory "Diophantine_Universal_Pairs.DFI_square_0" (unresolved "Diophantine_Universal_Pairs.Pell_Equation")
Failed to load theory "Diophantine_Universal_Pairs.Bridge_Theorem_Imp" (unresolved "Diophantine_Universal_Pairs.DFI_square_0", "Diophantine_Universal_Pairs.Lemma_4_4", "Diophantine_Universal_Pairs.Lucas_Diophantine", "Diophantine_Universal_Pairs.Poly_Extract")
Failed to load theory "Diophantine_Universal_Pairs.DFI_square_1" (unresolved "Diophantine_Universal_Pairs.DFI_square_0", "Diophantine_Universal_Pairs.Lucas_Diophantine")
Failed to load theory "Diophantine_Universal_Pairs.DFI_square_2" (unresolved "Diophantine_Universal_Pairs.DFI_square_1")
Failed to load theory "Diophantine_Universal_Pairs.DFI_square_3" (unresolved "Diophantine_Universal_Pairs.DFI_square_2")
Failed to load theory "Diophantine_Universal_Pairs.Bridge_Theorem_Rev" (unresolved "Diophantine_Universal_Pairs.Bridge_Theorem_Imp", "Diophantine_Universal_Pairs.DFI_square_3")
Failed to load theory "Diophantine_Universal_Pairs.Bridge_Theorem" (unresolved "Diophantine_Universal_Pairs.Bridge_Theorem_Rev")
Failed to load theory "Diophantine_Universal_Pairs.M3_Polynomial" (unresolved "Diophantine_Universal_Pairs.Pi_Relations", "Diophantine_Universal_Pairs.Poly_Degree", "Diophantine_Universal_Pairs.Poly_Extract")
Failed to load theory "Diophantine_Universal_Pairs.Nine_Unknowns_N_Z_Definitions" (unresolved "Diophantine_Universal_Pairs.Bridge_Theorem_Imp", "Diophantine_Universal_Pairs.Coding_Theorem_Definitions", "Diophantine_Universal_Pairs.M3_Polynomial", "Diophantine_Universal_Pairs.Poly_Degree", "Diophantine_Universal_Pairs.Suitable_For_Coding")
Failed to load theory "Diophantine_Universal_Pairs.Pi_to_M3_rat" (unresolved "Diophantine_Universal_Pairs.J3_Relations", "Diophantine_Universal_Pairs.M3_Polynomial", "Diophantine_Universal_Pairs.Pi_Relations")
Failed to load theory "Diophantine_Universal_Pairs.Matiyasevich_Polynomial" (unresolved "Diophantine_Universal_Pairs.M3_Polynomial", "Diophantine_Universal_Pairs.Pi_to_M3_rat")
Failed to load theory "Diophantine_Universal_Pairs.Nine_Unknowns_N_Z" (unresolved "Diophantine_Universal_Pairs.Bridge_Theorem", "Diophantine_Universal_Pairs.Coding_Theorem", "Diophantine_Universal_Pairs.Lemma_2_2", "Diophantine_Universal_Pairs.Lower_Bounds", "Diophantine_Universal_Pairs.Matiyasevich_Polynomial", "Diophantine_Universal_Pairs.Nine_Unknowns_N_Z_Definitions")
Failed to load theory "Diophantine_Universal_Pairs.Eleven_Unknowns_Z" (unresolved "Diophantine_Universal_Pairs.Nine_Unknowns_N_Z")
Failed to load theory "Diophantine_Universal_Pairs.Universal_Pairs" (unresolved "Diophantine_Universal_Pairs.Eleven_Unknowns_Z")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 77 of "~~/dirs/AFP/thys/Diophantine_Universal_Pairs/Coding_Theorem/Lemma_2_2.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 242 of "~~/dirs/AFP/thys/Diophantine_Universal_Pairs/MPoly_Utils/Variables.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 485 of "~~/dirs/AFP/thys/Diophantine_Universal_Pairs/Coding/Bit_Counting.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 214 of "~~/dirs/AFP/thys/Diophantine_Universal_Pairs/Lucas_Sequences/Lucas_Sequences.thy")
Failed to load theory "DiscretePricing.Infinite_Coin_Toss_Space" (unresolved "DiscretePricing.Disc_Cond_Expect")
Failed to load theory "DiscretePricing.Geometric_Random_Walk" (unresolved "DiscretePricing.Infinite_Coin_Toss_Space")
Failed to load theory "DiscretePricing.Fair_Price" (unresolved "DiscretePricing.Geometric_Random_Walk")
Failed to load theory "DiscretePricing.CRR_Model" (unresolved "DiscretePricing.Fair_Price")
Failed to load theory "DiscretePricing.Option_Price_Examples" (unresolved "DiscretePricing.CRR_Model")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1315 of "~~/dirs/AFP/thys/DiscretePricing/Disc_Cond_Expect.thy")
Failed to load theory "Elimination_Of_Repeated_Factors.ERF_Code_Test" (unresolved "Elimination_Of_Repeated_Factors.ERF_Algorithm")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 207 of "~~/dirs/AFP/thys/Elimination_Of_Repeated_Factors/ERF_Algorithm.thy")
/tmp/isabelle-isatest/bash_script7138619510657149558: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "Ergodic_Theory.Normalizing_Sequences" (unresolved "Ergodic_Theory.Transfer_Operator")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 691 of "~~/dirs/AFP/thys/Ergodic_Theory/Transfer_Operator.thy")
Failed to load theory "Euler_Exponential.HyperBinomial" (unresolved "Euler_Exponential.HyperSum")
Failed to load theory "Euler_Exponential.HyperrealPower" (unresolved "Euler_Exponential.HyperBinomial")
Failed to load theory "Euler_Exponential.HyperLog" (unresolved "Euler_Exponential.HyperrealPower")
Failed to load theory "Euler_Exponential.EulerExponential" (unresolved "Euler_Exponential.HyperBinomial", "Euler_Exponential.HyperLog")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 476 of "~~/dirs/AFP/thys/Euler_Exponential/HyperSum.thy")
Failed to load theory "Eval_FO.Ailamazyan_Code" (unresolved "Eval_FO.Ailamazyan")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 522 of "~~/dirs/AFP/thys/Eval_FO/Ailamazyan.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 13 of "~~/dirs/AFP/thys/FOL_Seq_Calc1/Sequent2.thy")
Failed to load theory "FO_Theory_Rewriting.Utils" (unresolved "First_Order_Terms.Term_Impl")
Failed to load theory "FO_Theory_Rewriting.Bot_Terms" (unresolved "FO_Theory_Rewriting.Utils")
Failed to load theory "FO_Theory_Rewriting.NF" (unresolved "FO_Theory_Rewriting.Bot_Terms")
Failed to load theory "FO_Theory_Rewriting.Multihole_Context_More" (unresolved "FO_Theory_Rewriting.Utils")
Failed to load theory "FO_Theory_Rewriting.Ground_MCtxt" (unresolved "FO_Theory_Rewriting.Multihole_Context_More", "FO_Theory_Rewriting.Utils")
Failed to load theory "FO_Theory_Rewriting.Context_Extensions" (unresolved "FO_Theory_Rewriting.Ground_MCtxt")
Failed to load theory "FO_Theory_Rewriting.Context_RR2" (unresolved "FO_Theory_Rewriting.Context_Extensions", "FO_Theory_Rewriting.Ground_MCtxt")
Failed to load theory "FO_Theory_Rewriting.Tree_Automata_Derivation_Split" (unresolved "FO_Theory_Rewriting.Ground_MCtxt")
Failed to load theory "FO_Theory_Rewriting.TA_Clousure_Const" (unresolved "FO_Theory_Rewriting.Tree_Automata_Derivation_Split")
Failed to load theory "FO_Theory_Rewriting.Rewriting" (unresolved "FO_Theory_Rewriting.Utils")
Failed to load theory "FO_Theory_Rewriting.FOR_Certificate" (unresolved "FO_Theory_Rewriting.Rewriting")
Failed to load theory "FO_Theory_Rewriting.LV_to_GTT" (unresolved "FO_Theory_Rewriting.Bot_Terms", "FO_Theory_Rewriting.Rewriting")
Failed to load theory "FO_Theory_Rewriting.Lift_Root_Step" (unresolved "FO_Theory_Rewriting.Context_Extensions", "FO_Theory_Rewriting.FOR_Certificate", "FO_Theory_Rewriting.Rewriting")
Failed to load theory "FO_Theory_Rewriting.FOR_Semantics" (unresolved "FO_Theory_Rewriting.FOR_Certificate", "FO_Theory_Rewriting.Lift_Root_Step")
Failed to load theory "FO_Theory_Rewriting.GTT_RRn" (unresolved "FO_Theory_Rewriting.Context_RR2", "FO_Theory_Rewriting.Lift_Root_Step", "FO_Theory_Rewriting.TA_Clousure_Const")
Failed to load theory "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl" (unresolved "First_Order_Terms.Term_Impl")
Failed to load theory "FO_Theory_Rewriting.Type_Instances_Impl" (unresolved "FO_Theory_Rewriting.Bot_Terms", "FO_Theory_Rewriting.TA_Clousure_Const", "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl")
Failed to load theory "FO_Theory_Rewriting.FOL_Extra" (unresolved "FO_Theory_Rewriting.Type_Instances_Impl")
Failed to load theory "FO_Theory_Rewriting.FOR_Check" (unresolved "FO_Theory_Rewriting.FOL_Extra", "FO_Theory_Rewriting.FOR_Semantics", "FO_Theory_Rewriting.GTT_RRn", "FO_Theory_Rewriting.LV_to_GTT", "FO_Theory_Rewriting.NF")
Failed to load theory "FO_Theory_Rewriting.NF_Impl" (unresolved "FO_Theory_Rewriting.NF", "FO_Theory_Rewriting.Type_Instances_Impl")
Failed to load theory "Regular_Tree_Relations.Tree_Automata_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl")
Failed to load theory "Regular_Tree_Relations.Regular_Relation_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Impl")
Failed to load theory "FO_Theory_Rewriting.FOR_Check_Impl" (unresolved "FO_Theory_Rewriting.FOR_Check", "FO_Theory_Rewriting.NF_Impl", "Regular_Tree_Relations.Regular_Relation_Impl")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 178 of "~~/dirs/AFP/thys/First_Order_Terms/Term_Impl.thy")
Failed to load theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code" (unresolved "Factor_Algebraic_Polynomial.MPoly_Divide")
Failed to load theory "Factor_Algebraic_Polynomial.Multivariate_Resultant" (unresolved "Factor_Algebraic_Polynomial.MPoly_Divide_Code")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly" (unresolved "Factor_Algebraic_Polynomial.Multivariate_Resultant")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl")
Failed to load theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly")
Failed to load theory "Factor_Algebraic_Polynomial.Factor_Real_Poly" (unresolved "Factor_Algebraic_Polynomial.Factor_Complex_Poly")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 42 of "~~/dirs/AFP/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy")
Failed to load theory "Factored_Transition_System_Bounding.ActionSeqProcess" (unresolved "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.Dependency" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.Invariants" (unresolved "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.TopologicalProps" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.SystemAbstraction" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.Dependency", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.TopologicalProps")
Failed to load theory "Factored_Transition_System_Bounding.AcycSspace" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.Acyclicity", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.SystemAbstraction")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 961 of "~~/dirs/AFP/thys/Factored_Transition_System_Bounding/FactoredSystem.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 79 of "~~/dirs/AFP/thys/Factored_Transition_System_Bounding/Acyclicity.thy")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_deep_further_tests" (unresolved "FaithfulPMLinHOL.PMLinHOL_deep_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_deep_further_tests_1" (unresolved "FaithfulPMLinHOL.PMLinHOL_deep_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_deep_further_tests_2" (unresolved "FaithfulPMLinHOL.PMLinHOL_deep_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_shallow_further_tests" (unresolved "FaithfulPMLinHOL.PMLinHOL_shallow_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_shallow_further_tests_1" (unresolved "FaithfulPMLinHOL.PMLinHOL_shallow_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_shallow_further_tests_2" (unresolved "FaithfulPMLinHOL.PMLinHOL_shallow_tests")
Failed to load theory "FaithfulPMLinHOL.PMLinHOL_shallow_minimal_further_tests" (unresolved "FaithfulPMLinHOL.PMLinHOL_shallow_minimal_tests")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 28 of "~~/dirs/AFP/thys/FaithfulPMLinHOL/PMLinHOL_shallow_minimal_tests.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 140 of "~~/dirs/AFP/thys/FaithfulPMLinHOL/PMLinHOL_shallow_minimal_further_tests_1.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/FaithfulPMLinHOL/PMLinHOL_faithfulness.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 35 of "~~/dirs/AFP/thys/FaithfulPMLinHOL/PMLinHOL_shallow_tests.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 49 of "~~/dirs/AFP/thys/FaithfulPMLinHOL/PMLinHOL_deep_tests.thy")
Failed to load theory "First_Order_Clause.IsaFoR_Ground_Term_Compatibility" (unresolved "First_Order_Clause.IsaFoR_Nonground_Context")
Failed to load theory "First_Order_Clause.IsaFoR_KBO" (unresolved "First_Order_Clause.IsaFoR_Nonground_Context")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 114 of "~~/dirs/AFP/thys/First_Order_Clause/IsaFoR_Nonground_Context.thy")
Failed to load theory "First_Order_Terms.Unification_More" (unresolved "First_Order_Terms.Term_Impl")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 178 of "~~/dirs/AFP/thys/First_Order_Terms/Term_Impl.thy")
Failed to load theory "Fishers_Inequality.Incidence_Matrices" (unresolved "Fishers_Inequality.Design_Extras", "Fishers_Inequality.Matrix_Vector_Extras")
Failed to load theory "Fishers_Inequality.Dual_Systems" (unresolved "Fishers_Inequality.Incidence_Matrices")
Failed to load theory "Fishers_Inequality.Rank_Argument_General" (unresolved "Fishers_Inequality.Dual_Systems")
Failed to load theory "Fishers_Inequality.Linear_Bound_Argument" (unresolved "Fishers_Inequality.Incidence_Matrices")
Failed to load theory "Fishers_Inequality.Fishers_Inequality" (unresolved "Fishers_Inequality.Linear_Bound_Argument", "Fishers_Inequality.Rank_Argument_General")
Failed to load theory "Fishers_Inequality.Vector_Matrix_Mod" (unresolved "Fishers_Inequality.Matrix_Vector_Extras")
Failed to load theory "Fishers_Inequality.Fishers_Inequality_Variations" (unresolved "Fishers_Inequality.Dual_Systems", "Fishers_Inequality.Linear_Bound_Argument", "Fishers_Inequality.Rank_Argument_General", "Fishers_Inequality.Vector_Matrix_Mod")
Failed to load theory "Fishers_Inequality.Fishers_Inequality_Root" (unresolved "Fishers_Inequality.Design_Extras", "Fishers_Inequality.Dual_Systems", "Fishers_Inequality.Fishers_Inequality", "Fishers_Inequality.Fishers_Inequality_Variations", "Fishers_Inequality.Incidence_Matrices", "Fishers_Inequality.Linear_Bound_Argument", "Fishers_Inequality.Matrix_Vector_Extras", "Fishers_Inequality.Rank_Argument_General", "Fishers_Inequality.Vector_Matrix_Mod")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 385 of "~~/dirs/AFP/thys/Fishers_Inequality/Matrix_Vector_Extras.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 320 of "~~/dirs/AFP/thys/Fishers_Inequality/Design_Extras.thy")
Failed to load theory "Functional_Ordered_Resolution_Prover.Executable_Subsumption" (unresolved "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
Failed to load theory "Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover" (unresolved "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover", "Functional_Ordered_Resolution_Prover.Executable_Subsumption", "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 138 of "~~/dirs/AFP/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 956 of "~~/dirs/AFP/thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")
Failed to load theory "Galois_Energy_Games.Update" (unresolved "Galois_Energy_Games.Energy_Order")
Failed to load theory "Galois_Energy_Games.Galois_Energy_Game" (unresolved "Galois_Energy_Games.Energy_Game")
Failed to load theory "Galois_Energy_Games.Decidability" (unresolved "Galois_Energy_Games.Galois_Energy_Game")
Failed to load theory "Galois_Energy_Games.Natural_Galois_Energy_Game" (unresolved "Galois_Energy_Games.Decidability", "Galois_Energy_Games.Energy_Game", "Galois_Energy_Games.Energy_Order", "Galois_Energy_Games.Update")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 162 of "~~/dirs/AFP/thys/Galois_Energy_Games/Energy_Order.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 128 of "~~/dirs/AFP/thys/Galois_Energy_Games/Energy_Game.thy")
Failed to load theory "Generalized_Cauchy_Davenport.Generalized_Cauchy_Davenport_main_proof" (unresolved "Generalized_Cauchy_Davenport.Generalized_Cauchy_Davenport_preliminaries")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 40 of "~~/dirs/AFP/thys/Generalized_Cauchy_Davenport/Generalized_Cauchy_Davenport_preliminaries.thy")
Failed to load theory "GewirthPGCProof.ExtendedDDL" (unresolved "GewirthPGCProof.CJDDLplus")
Failed to load theory "GewirthPGCProof.GewirthArgument" (unresolved "GewirthPGCProof.ExtendedDDL")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 68 of "~~/dirs/AFP/thys/GewirthPGCProof/CJDDLplus.thy")
Failed to load theory "Given_Clause_Loops.DISCOUNT_Loop" (unresolved "Given_Clause_Loops.Given_Clause_Loops_Util")
Failed to load theory "Given_Clause_Loops.Zipperposition_Loop" (unresolved "Given_Clause_Loops.DISCOUNT_Loop")
Failed to load theory "Given_Clause_Loops.Otter_Loop" (unresolved "Given_Clause_Loops.Given_Clause_Loops_Util")
Failed to load theory "Given_Clause_Loops.iProver_Loop" (unresolved "Given_Clause_Loops.Otter_Loop")
Failed to load theory "Given_Clause_Loops.Prover_Queue" (unresolved "Given_Clause_Loops.Given_Clause_Loops_Util")
Failed to load theory "Given_Clause_Loops.Fair_DISCOUNT_Loop" (unresolved "Given_Clause_Loops.DISCOUNT_Loop", "Given_Clause_Loops.Given_Clause_Loops_Util", "Given_Clause_Loops.Prover_Queue")
Failed to load theory "Given_Clause_Loops.Fair_Otter_Loop_Def" (unresolved "Given_Clause_Loops.Otter_Loop", "Given_Clause_Loops.Prover_Queue")
Failed to load theory "Given_Clause_Loops.Fair_iProver_Loop" (unresolved "Given_Clause_Loops.Fair_Otter_Loop_Def", "Given_Clause_Loops.Given_Clause_Loops_Util", "Given_Clause_Loops.iProver_Loop")
Failed to load theory "Given_Clause_Loops.Fair_Otter_Loop_Complete" (unresolved "Given_Clause_Loops.Fair_iProver_Loop")
Failed to load theory "Given_Clause_Loops.Prover_Lazy_List_Queue" (unresolved "Given_Clause_Loops.Prover_Queue")
Failed to load theory "Given_Clause_Loops.Fair_Zipperposition_Loop" (unresolved "Given_Clause_Loops.Given_Clause_Loops_Util", "Given_Clause_Loops.Prover_Lazy_List_Queue", "Given_Clause_Loops.Zipperposition_Loop")
Failed to load theory "Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts" (unresolved "Given_Clause_Loops.Fair_Zipperposition_Loop")
Failed to load theory "Given_Clause_Loops.Given_Clause_Loops" (unresolved "Given_Clause_Loops.Fair_DISCOUNT_Loop", "Given_Clause_Loops.Fair_Otter_Loop_Complete", "Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 83 of "~~/dirs/AFP/thys/Given_Clause_Loops/Given_Clause_Loops_Util.thy")
Failed to load theory "Graph_Algorithms.Pair_Graph_Specs" (unresolved "Graph_Algorithms.Vwalk")
Failed to load theory "Graph_Algorithms.DFS" (unresolved "Graph_Algorithms.Pair_Graph_Specs")
Failed to load theory "Graph_Algorithms.Dist" (unresolved "Graph_Algorithms.Vwalk")
Failed to load theory "Graph_Algorithms.BFS_2" (unresolved "Graph_Algorithms.Dist", "Graph_Algorithms.Pair_Graph_Specs")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 790 of "~~/dirs/AFP/thys/Graph_Algorithms/Vwalk.thy")
Failed to load theory "Green.Green" (unresolved "Green.Paths")
Failed to load theory "Green.SymmetricR2Shapes" (unresolved "Green.Green")
Failed to load theory "Green.CircExample" (unresolved "Green.Green", "Green.SymmetricR2Shapes")
Failed to load theory "Green.DiamExample" (unresolved "Green.Green", "Green.SymmetricR2Shapes")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 212 of "~~/dirs/AFP/thys/Green/Paths.thy")
Failed to load theory "Groebner_Macaulay.Poly_Fun" (unresolved "Groebner_Macaulay.Binomial_Int")
Failed to load theory "Groebner_Macaulay.Hilbert_Function" (unresolved "Groebner_Macaulay.Dube_Prelims")
Failed to load theory "Groebner_Macaulay.Cone_Decomposition" (unresolved "Groebner_Macaulay.Hilbert_Function")
Failed to load theory "Groebner_Macaulay.Dube_Bound" (unresolved "Groebner_Macaulay.Cone_Decomposition", "Groebner_Macaulay.Poly_Fun")
Failed to load theory "Groebner_Macaulay.Groebner_Macaulay_Examples" (unresolved "Groebner_Macaulay.Dube_Bound")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 147 of "~~/dirs/AFP/thys/Groebner_Macaulay/Dube_Prelims.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 107 of "~~/dirs/AFP/thys/Groebner_Macaulay/Binomial_Int.thy")
Failed to load theory "Gromov_Hyperbolicity.Metric_Completion" (unresolved "Gromov_Hyperbolicity.Isometries")
Failed to load theory "Gromov_Hyperbolicity.Gromov_Hyperbolicity" (unresolved "Gromov_Hyperbolicity.Isometries", "Gromov_Hyperbolicity.Metric_Completion")
Failed to load theory "Gromov_Hyperbolicity.Gromov_Boundary" (unresolved "Gromov_Hyperbolicity.Eexp_Eln", "Gromov_Hyperbolicity.Gromov_Hyperbolicity")
Failed to load theory "Gromov_Hyperbolicity.Morse_Gromov_Theorem" (unresolved "Gromov_Hyperbolicity.Gromov_Hyperbolicity")
Failed to load theory "Gromov_Hyperbolicity.Bonk_Schramm_Extension" (unresolved "Gromov_Hyperbolicity.Morse_Gromov_Theorem")
Failed to load theory "Gromov_Hyperbolicity.Boundary_Extension" (unresolved "Gromov_Hyperbolicity.Gromov_Boundary", "Gromov_Hyperbolicity.Morse_Gromov_Theorem")
Failed to load theory "Gromov_Hyperbolicity.Busemann_Function" (unresolved "Gromov_Hyperbolicity.Boundary_Extension")
Failed to load theory "Gromov_Hyperbolicity.Isometries_Classification" (unresolved "Gromov_Hyperbolicity.Busemann_Function", "Gromov_Hyperbolicity.Gromov_Boundary")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 932 of "~~/dirs/AFP/thys/Gromov_Hyperbolicity/Isometries.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 165 of "~~/dirs/AFP/thys/Gromov_Hyperbolicity/Eexp_Eln.thy")
Failed to load theory "Grothendieck_Schemes.Comm_Ring" (unresolved "Grothendieck_Schemes.Group_Extras")
Failed to load theory "Grothendieck_Schemes.Scheme" (unresolved "Grothendieck_Schemes.Comm_Ring")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 246 of "~~/dirs/AFP/thys/Grothendieck_Schemes/Group_Extras.thy")
Failed to load theory "HOL-CSP.CSP_Monotonies" (unresolved "HOL-CSP.Hiding")
Failed to load theory "HOL-CSP.Basic_CSP_Laws" (unresolved "HOL-CSP.CSP_Monotonies", "HOL-CSP.Hiding")
Failed to load theory "HOL-CSP.Events_Ticks_CSP_Laws" (unresolved "HOL-CSP.Hiding")
Failed to load theory "HOL-CSP.CSP_Assertions" (unresolved "HOL-CSP.Basic_CSP_Laws", "HOL-CSP.CSP_Monotonies", "HOL-CSP.Events_Ticks_CSP_Laws")
Failed to load theory "HOL-CSP.Non_Deterministic_CSP_Distributivity" (unresolved "HOL-CSP.Hiding")
Failed to load theory "HOL-CSP.Step_CSP_Laws" (unresolved "HOL-CSP.Hiding")
Failed to load theory "HOL-CSP.Step_CSP_Laws_Extended" (unresolved "HOL-CSP.Basic_CSP_Laws", "HOL-CSP.Non_Deterministic_CSP_Distributivity", "HOL-CSP.Step_CSP_Laws")
Failed to load theory "HOL-CSP.CSP_Laws" (unresolved "HOL-CSP.Basic_CSP_Laws", "HOL-CSP.Step_CSP_Laws_Extended")
Failed to load theory "HOL-CSP.Read_Write_CSP_Laws" (unresolved "HOL-CSP.Step_CSP_Laws_Extended")
Failed to load theory "HOL-CSP" (unresolved "HOL-CSP.CSP_Assertions", "HOL-CSP.CSP_Laws", "HOL-CSP.Read_Write_CSP_Laws")
Failed to load theory "HOL-CSP.Conclusion" (unresolved "HOL-CSP")
Failed to load theory "HOL-CSP.CopyBuffer" (unresolved "HOL-CSP")
Failed to load theory "HOL-CSP.MergeAnomaly" (unresolved "HOL-CSP")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 732 of "~~/dirs/AFP/thys/HOL-CSP/Hiding.thy")
Failed to load theory "Hidden_Markov_Models.HMM_Example" (unresolved "Hidden_Markov_Models.HMM_Implementation")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 201 of "~~/dirs/AFP/thys/Hidden_Markov_Models/HMM_Implementation.thy")
Failed to load theory "Hidden_Number_Problem.Hidden_Number_Problem" (unresolved "Babai_Nearest_Plane.Babai_Correct")
Failed to load theory "Hidden_Number_Problem.Ad_Codegen_Example" (unresolved "Hidden_Number_Problem.Hidden_Number_Problem")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 507 of "~~/dirs/AFP/thys/Babai_Nearest_Plane/Babai_Correct.thy")
Failed to load theory "Higher_Order_Terms.Nterm" (unresolved "Higher_Order_Terms.Term_Class")
Failed to load theory "Higher_Order_Terms.Term" (unresolved "Higher_Order_Terms.Term_Class")
Failed to load theory "Higher_Order_Terms.Pats" (unresolved "Higher_Order_Terms.Term")
Failed to load theory "Higher_Order_Terms.Unification_Compat" (unresolved "Higher_Order_Terms.Term_Class")
Failed to load theory "Higher_Order_Terms.Lambda_Free_Compat" (unresolved "Higher_Order_Terms.Unification_Compat")
Failed to load theory "Higher_Order_Terms.Term_to_Nterm" (unresolved "Higher_Order_Terms.Nterm", "Higher_Order_Terms.Term")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 528 of "~~/dirs/AFP/thys/Higher_Order_Terms/Term_Class.thy")
Failed to load theory "Hilbert_Basis.Weak_Hilbert_Basis" (unresolved "Padic_Field.Cring_Multivariable_Poly")
Failed to load theory "Hilbert_Basis.Hilbert_Basis" (unresolved "Hilbert_Basis.Weak_Hilbert_Basis")
Failed to load theory "Hilbert_Basis.Examples_Noetherian_Rings" (unresolved "Hilbert_Basis.Hilbert_Basis")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 140 of "~~/dirs/AFP/thys/Hilbert_Basis/Formal_Power_Series_Ring.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 3921 of "~~/dirs/AFP/thys/Padic_Field/Cring_Multivariable_Poly.thy")
Failed to load theory "Hoare_Time.Nielson_Examples" (unresolved "Hoare_Time.Nielson_VCG")
Failed to load theory "Hoare_Time.Nielson_VCGi_complete" (unresolved "Hoare_Time.Nielson_VCG")
Failed to load theory "Hoare_Time.DiscussionO" (unresolved "Hoare_Time.SepLogK_Hoare")
Failed to load theory "Hoare_Time.SepLogK_VCG" (unresolved "Hoare_Time.SepLogK_Hoare")
Failed to load theory "Hoare_Time.Discussion" (unresolved "Hoare_Time.SepLog_Hoare")
Failed to load theory "Hoare_Time.SepLog_Examples" (unresolved "Hoare_Time.SepLog_Hoare")
Failed to load theory "Hoare_Time.Hoare_Time" (unresolved "Hoare_Time.Discussion", "Hoare_Time.DiscussionO", "Hoare_Time.Nielson_Examples", "Hoare_Time.Nielson_Sqrt", "Hoare_Time.Nielson_VCG", "Hoare_Time.Nielson_VCGi_complete", "Hoare_Time.QuantK_Examples", "Hoare_Time.QuantK_Sqrt", "Hoare_Time.Quant_Examples", "Hoare_Time.SepLogK_Hoare", "Hoare_Time.SepLogK_VCG", "Hoare_Time.SepLog_Examples", "Hoare_Time.SepLog_Hoare")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 162 of "~~/dirs/AFP/thys/Hoare_Time/SepLog_Hoare.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 352 of "~~/dirs/AFP/thys/Hoare_Time/SepLogK_Hoare.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 31 of "~~/dirs/AFP/thys/Hoare_Time/Nielson_Sqrt.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 26 of "~~/dirs/AFP/thys/Hoare_Time/Quant_Examples.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 32 of "~~/dirs/AFP/thys/Hoare_Time/QuantK_Sqrt.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 29 of "~~/dirs/AFP/thys/Hoare_Time/QuantK_Examples.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 237 of "~~/dirs/AFP/thys/Hoare_Time/Nielson_VCG.thy")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_KAT_rel" (unresolved "Hybrid_Systems_VCs.HS_VC_KAT")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_KAT_Examples_rel" (unresolved "Hybrid_Systems_VCs.HS_VC_KAT_rel")
Failed to load theory "Quantales.Quantale_Star" (unresolved "Quantales.Quantales")
Failed to load theory "Transformer_Semantics.Isotone_Transformers" (unresolved "Quantales.Quantale_Star")
Failed to load theory "Transformer_Semantics.Sup_Inf_Preserving_Transformers" (unresolved "Transformer_Semantics.Isotone_Transformers")
Failed to load theory "Transformer_Semantics.Kleisli_Transformers" (unresolved "Transformer_Semantics.Sup_Inf_Preserving_Transformers")
Failed to load theory "Transformer_Semantics.Kleisli_Quantaloid" (unresolved "Transformer_Semantics.Kleisli_Transformers")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_PT" (unresolved "Transformer_Semantics.Kleisli_Quantaloid")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_PT_Examples" (unresolved "Hybrid_Systems_VCs.HS_VC_PT")
Failed to load theory "Transformer_Semantics.Kleisli_Quantale" (unresolved "Quantales.Quantale_Star", "Transformer_Semantics.Kleisli_Quantaloid")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_KA_ndfun" (unresolved "Transformer_Semantics.Kleisli_Quantale")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_KAT_ndfun" (unresolved "Hybrid_Systems_VCs.HS_VC_KAT", "Hybrid_Systems_VCs.HS_VC_KA_ndfun")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_KAT_Examples_ndfun" (unresolved "Hybrid_Systems_VCs.HS_VC_KAT_ndfun")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_MKA_ndfun" (unresolved "Hybrid_Systems_VCs.HS_VC_KA_ndfun")
Failed to load theory "Hybrid_Systems_VCs.HS_VC_MKA_Examples_ndfun" (unresolved "Hybrid_Systems_VCs.HS_VC_MKA_ndfun")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 45 of "~~/dirs/AFP/thys/Quantales/Quantales.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 145 of "~~/dirs/AFP/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT.thy")
Failed to load theory "Hyperdual.HyperdualFunctionExtension" (unresolved "Hyperdual.Hyperdual")
Failed to load theory "Hyperdual.AnalyticTestFunction" (unresolved "Hyperdual.HyperdualFunctionExtension")
Failed to load theory "Hyperdual.LogisticFunction" (unresolved "Hyperdual.HyperdualFunctionExtension")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 579 of "~~/dirs/AFP/thys/Hyperdual/Hyperdual.thy")
Failed to load theory "Hypergraph_Basics.Hypergraph" (unresolved "Fishers_Inequality.Design_Extras")
Failed to load theory "Hypergraph_Basics.Hypergraph_Variations" (unresolved "Hypergraph_Basics.Hypergraph")
Failed to load theory "Hypergraph_Basics.Hypergraph_Basics_Root" (unresolved "Hypergraph_Basics.Hypergraph", "Hypergraph_Basics.Hypergraph_Variations")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 320 of "~~/dirs/AFP/thys/Fishers_Inequality/Design_Extras.thy")
Failed to load theory "Hypergraph_Basics.Hypergraph" (unresolved "Fishers_Inequality.Design_Extras")
Failed to load theory "Hypergraph_Basics.Hypergraph_Variations" (unresolved "Hypergraph_Basics.Hypergraph")
Failed to load theory "Hypergraph_Colourings.Hypergraph_Colourings" (unresolved "Hypergraph_Basics.Hypergraph_Variations")
Failed to load theory "Hypergraph_Colourings.Basic_Bounds_Application" (unresolved "Hypergraph_Colourings.Hypergraph_Colourings")
Failed to load theory "Hypergraph_Colourings.LLL_Applications" (unresolved "Hypergraph_Colourings.Basic_Bounds_Application")
Failed to load theory "Hypergraph_Colourings.Hypergraph_Colourings_Root" (unresolved "Hypergraph_Colourings.Basic_Bounds_Application", "Hypergraph_Colourings.Hypergraph_Colourings", "Hypergraph_Colourings.LLL_Applications")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 320 of "~~/dirs/AFP/thys/Fishers_Inequality/Design_Extras.thy")
Failed to load theory "ILL.Proof" (unresolved "ILL.ILL")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 98 of "~~/dirs/AFP/thys/ILL/ILL.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 182 of "~~/dirs/AFP/thys/IMP2/lib/IMP2_Aux_Lemmas.thy")
Failed to load theory "Inductive_Inference.Universal" (unresolved "Inductive_Inference.Partial_Recursive")
Failed to load theory "Inductive_Inference.Standard_Results" (unresolved "Inductive_Inference.Universal")
Failed to load theory "Inductive_Inference.Inductive_Inference_Basics" (unresolved "Inductive_Inference.Standard_Results")
Failed to load theory "Inductive_Inference.CONS_LIM" (unresolved "Inductive_Inference.Inductive_Inference_Basics")
Failed to load theory "Inductive_Inference.CP_FIN_NUM" (unresolved "Inductive_Inference.Inductive_Inference_Basics")
Failed to load theory "Inductive_Inference.Lemma_R" (unresolved "Inductive_Inference.Inductive_Inference_Basics")
Failed to load theory "Inductive_Inference.LIM_BC" (unresolved "Inductive_Inference.Lemma_R")
Failed to load theory "Inductive_Inference.R1_BC" (unresolved "Inductive_Inference.CP_FIN_NUM", "Inductive_Inference.Lemma_R")
Failed to load theory "Inductive_Inference.TOTAL_CONS" (unresolved "Inductive_Inference.CONS_LIM", "Inductive_Inference.CP_FIN_NUM", "Inductive_Inference.Lemma_R")
Failed to load theory "Inductive_Inference.Union" (unresolved "Inductive_Inference.R1_BC", "Inductive_Inference.TOTAL_CONS")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 438 of "~~/dirs/AFP/thys/Inductive_Inference/Partial_Recursive.thy")
Failed to load theory "Interpreter_Optimizations.AList_Extra" (unresolved "Interpreter_Optimizations.List_util")
Failed to load theory "Interpreter_Optimizations.Global" (unresolved "Interpreter_Optimizations.AList_Extra", "Interpreter_Optimizations.List_util")
Failed to load theory "Interpreter_Optimizations.Unboxed" (unresolved "Interpreter_Optimizations.Global")
Failed to load theory "Interpreter_Optimizations.OpUbx" (unresolved "Interpreter_Optimizations.Unboxed")
Failed to load theory "Interpreter_Optimizations.Unboxed_lemmas" (unresolved "Interpreter_Optimizations.Unboxed")
Failed to load theory "Interpreter_Optimizations.Op_example" (unresolved "Interpreter_Optimizations.Global", "Interpreter_Optimizations.OpUbx", "Interpreter_Optimizations.Unboxed_lemmas")
Failed to load theory "Interpreter_Optimizations.Inca" (unresolved "Interpreter_Optimizations.Global")
Failed to load theory "Interpreter_Optimizations.Inca_Verification" (unresolved "Interpreter_Optimizations.Inca")
Failed to load theory "Interpreter_Optimizations.Std" (unresolved "Interpreter_Optimizations.Global", "Interpreter_Optimizations.List_util")
Failed to load theory "Interpreter_Optimizations.Ubx" (unresolved "Interpreter_Optimizations.Global", "Interpreter_Optimizations.OpUbx")
Failed to load theory "Interpreter_Optimizations.Ubx_Verification" (unresolved "Interpreter_Optimizations.Ubx")
Failed to load theory "Interpreter_Optimizations.Inca_to_Ubx_simulation" (unresolved "Interpreter_Optimizations.Inca", "Interpreter_Optimizations.List_util", "Interpreter_Optimizations.Ubx", "Interpreter_Optimizations.Ubx_Verification", "Interpreter_Optimizations.Unboxed_lemmas")
Failed to load theory "Interpreter_Optimizations.Std_to_Inca_simulation" (unresolved "Interpreter_Optimizations.Global", "Interpreter_Optimizations.Inca", "Interpreter_Optimizations.List_util", "Interpreter_Optimizations.Std")
Failed to load theory "Interpreter_Optimizations.Inca_to_Ubx_compiler" (unresolved "Interpreter_Optimizations.Inca_Verification", "Interpreter_Optimizations.Inca_to_Ubx_simulation")
Failed to load theory "Interpreter_Optimizations.Std_to_Inca_compiler" (unresolved "Interpreter_Optimizations.Std_to_Inca_simulation")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 216 of "~~/dirs/AFP/thys/Interpreter_Optimizations/List_util.thy")
Failed to load theory "Interval_Analysis.Interval_Division_Non_Zero" (unresolved "Interval_Analysis.Interval_Utilities")
Failed to load theory "Interval_Analysis.Extended_Interval_Division" (unresolved "Interval_Analysis.Interval_Division_Non_Zero")
Failed to load theory "Interval_Analysis.Interval_Division_Real" (unresolved "Interval_Analysis.Interval_Division_Non_Zero")
Failed to load theory "Interval_Analysis.Inclusion_Isotonicity" (unresolved "Interval_Analysis.Interval_Division_Non_Zero", "Interval_Analysis.Interval_Utilities")
Failed to load theory "Interval_Analysis.Lipschitz_Interval_Extension" (unresolved "Interval_Analysis.Inclusion_Isotonicity", "Interval_Analysis.Interval_Utilities")
Failed to load theory "Interval_Analysis.Multi_Interval_Preliminaries" (unresolved "Interval_Analysis.Inclusion_Isotonicity")
Failed to load theory "Interval_Analysis.Lipschitz_Subdivisions_Refinements" (unresolved "Interval_Analysis.Lipschitz_Interval_Extension", "Interval_Analysis.Multi_Interval_Preliminaries")
Failed to load theory "Interval_Analysis.Extended_Interval_Analysis" (unresolved "Interval_Analysis.Extended_Interval_Division", "Interval_Analysis.Lipschitz_Subdivisions_Refinements")
Failed to load theory "Interval_Analysis.Interval_Analysis" (unresolved "Interval_Analysis.Interval_Division_Real", "Interval_Analysis.Lipschitz_Subdivisions_Refinements")
Failed to load theory "Interval_Analysis.Multi_Interval_Adjacent" (unresolved "Interval_Analysis.Multi_Interval_Preliminaries")
Failed to load theory "Interval_Analysis.Multi_Interval_Non_Overlapping" (unresolved "Interval_Analysis.Multi_Interval_Preliminaries")
Failed to load theory "Interval_Analysis.Multi_Interval_Overlapping" (unresolved "Interval_Analysis.Multi_Interval_Preliminaries")
Failed to load theory "Interval_Analysis.Multi_Interval" (unresolved "Interval_Analysis.Lipschitz_Subdivisions_Refinements", "Interval_Analysis.Multi_Interval_Adjacent", "Interval_Analysis.Multi_Interval_Non_Overlapping", "Interval_Analysis.Multi_Interval_Overlapping")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Division_Core" (unresolved "Interval_Analysis.Interval_Division_Non_Zero", "Interval_Analysis.Multi_Interval")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Division_Adjacent" (unresolved "Interval_Analysis.Extended_Multi_Interval_Division_Core")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Division_Non_Overlapping" (unresolved "Interval_Analysis.Extended_Multi_Interval_Division_Core")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Division_Overlapping" (unresolved "Interval_Analysis.Extended_Multi_Interval_Division_Core")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Division" (unresolved "Interval_Analysis.Extended_Multi_Interval_Division_Adjacent", "Interval_Analysis.Extended_Multi_Interval_Division_Non_Overlapping", "Interval_Analysis.Extended_Multi_Interval_Division_Overlapping")
Failed to load theory "Interval_Analysis.Extended_Multi_Interval_Analysis" (unresolved "Interval_Analysis.Extended_Multi_Interval_Division")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 63 of "~~/dirs/AFP/thys/Interval_Analysis/Interval_Utilities.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 778 of "~~/dirs/AFP/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy")
Failed to load theory "IsaGeoCoq.Gupta_Neutral" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Gupta_Euclidean" (unresolved "IsaGeoCoq.Gupta_Neutral")
Failed to load theory "IsaGeoCoq.Gupta_Neutral_2D" (unresolved "IsaGeoCoq.Gupta_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Model_Gupta_Neutral" (unresolved "IsaGeoCoq.Gupta_Neutral")
Failed to load theory "IsaGeoCoq.Gupta_Neutral_Model_Tarski_Neutral" (unresolved "IsaGeoCoq.Gupta_Neutral", "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Highschool_Neutral" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral_2D" (unresolved "IsaGeoCoq.Hilbert_Neutral")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral_3D" (unresolved "IsaGeoCoq.Hilbert_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_2D" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Gupta_Neutral_2D_Model_Tarski_Neutral_2D" (unresolved "IsaGeoCoq.Gupta_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_2D")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_2D_Model_Gupta_Neutral_2D" (unresolved "IsaGeoCoq.Gupta_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_2D")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_2D_Model_Hilbert_Neutral_2D" (unresolved "IsaGeoCoq.Hilbert_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_2D")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_3D" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Archimedes" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Postulate_Parallels" (unresolved "IsaGeoCoq.Tarski_Neutral_Archimedes")
Failed to load theory "IsaGeoCoq.Tarski_Euclidean" (unresolved "IsaGeoCoq.Tarski_Neutral", "IsaGeoCoq.Tarski_Postulate_Parallels")
Failed to load theory "IsaGeoCoq.Gupta_Euclidean_Model_Tarski_Euclidean" (unresolved "IsaGeoCoq.Gupta_Euclidean", "IsaGeoCoq.Tarski_Euclidean")
Failed to load theory "IsaGeoCoq.Tarski_Euclidean_Model_Gupta_Euclidean" (unresolved "IsaGeoCoq.Gupta_Euclidean", "IsaGeoCoq.Tarski_Euclidean", "IsaGeoCoq.Tarski_Neutral_Model_Gupta_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Euclidean_2D" (unresolved "IsaGeoCoq.Tarski_Euclidean", "IsaGeoCoq.Tarski_Neutral", "IsaGeoCoq.Tarski_Neutral_2D", "IsaGeoCoq.Tarski_Postulate_Parallels")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Model_Hilbert_Neutral" (unresolved "IsaGeoCoq.Gupta_Neutral", "IsaGeoCoq.Hilbert_Neutral", "IsaGeoCoq.Tarski_Postulate_Parallels")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_3D_Model_Hilbert_Neutral_3D" (unresolved "IsaGeoCoq.Hilbert_Neutral_3D", "IsaGeoCoq.Tarski_Neutral_3D", "IsaGeoCoq.Tarski_Neutral_Model_Hilbert_Neutral")
Failed to load theory "IsaGeoCoq.Tarski_Non_Euclidean" (unresolved "IsaGeoCoq.Tarski_Postulate_Parallels")
Failed to load theory "IsaGeoCoq.Tarski_Non_Euclidean_Aristotle" (unresolved "IsaGeoCoq.Tarski_Non_Euclidean")
Failed to load theory "IsaGeoCoq.Tarski_Non_Euclidean_Archimedean" (unresolved "IsaGeoCoq.Tarski_Non_Euclidean_Aristotle")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Continuity" (unresolved "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Highschool_Euclidean" (unresolved "IsaGeoCoq.Highschool_Neutral", "IsaGeoCoq.Tarski_Euclidean", "IsaGeoCoq.Tarski_Neutral_Continuity")
Failed to load theory "IsaGeoCoq.Highschool_Euclidean_2D" (unresolved "IsaGeoCoq.Highschool_Euclidean", "IsaGeoCoq.Tarski_Euclidean_2D")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Archimedes_Continuity" (unresolved "IsaGeoCoq.Tarski_Neutral_Archimedes", "IsaGeoCoq.Tarski_Neutral_Continuity")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Continuity_2D" (unresolved "IsaGeoCoq.Tarski_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_Continuity")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Continuous" (unresolved "IsaGeoCoq.Tarski_Neutral_Continuity")
Failed to load theory "IsaGeoCoq.Tarski_Euclidean_2D_Continuous" (unresolved "IsaGeoCoq.Tarski_Euclidean_2D", "IsaGeoCoq.Tarski_Neutral_Continuous")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_Hilbert" (unresolved "IsaGeoCoq.Hilbert_Neutral", "IsaGeoCoq.Tarski_Neutral")
Failed to load theory "IsaGeoCoq.Hilbert_Euclidean" (unresolved "IsaGeoCoq.Hilbert_Neutral", "IsaGeoCoq.Tarski_Euclidean", "IsaGeoCoq.Tarski_Neutral_Hilbert")
Failed to load theory "IsaGeoCoq.Hilbert_Euclidean_Model_Tarski_Euclidean" (unresolved "IsaGeoCoq.Hilbert_Euclidean")
Failed to load theory "IsaGeoCoq.Tarski_Euclidean_Model_Hilbert_Euclidean" (unresolved "IsaGeoCoq.Hilbert_Euclidean", "IsaGeoCoq.Tarski_Neutral_3D_Model_Hilbert_Neutral_3D")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral_2D_Model_Tarski_Neutral_2D" (unresolved "IsaGeoCoq.Hilbert_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_2D", "IsaGeoCoq.Tarski_Neutral_Hilbert")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral_Model_Tarski_Neutral" (unresolved "IsaGeoCoq.Tarski_Neutral_Hilbert")
Failed to load theory "IsaGeoCoq.Tarski_Neutral_3D_Hilbert" (unresolved "IsaGeoCoq.Tarski_Neutral_3D", "IsaGeoCoq.Tarski_Neutral_Hilbert")
Failed to load theory "IsaGeoCoq.Hilbert_Neutral_3D_Model_Tarski_Neutral_3D" (unresolved "IsaGeoCoq.Hilbert_Neutral_3D", "IsaGeoCoq.Tarski_Neutral_3D_Hilbert")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 5235 of "~~/dirs/AFP/thys/IsaGeoCoq/Tarski_Neutral.thy")
Failed to load theory "Isabelle-Solidity.Unit_Tests" (unresolved "Isabelle-Solidity.Solidity")
Failed to load theory "Isabelle-Solidity.WP" (unresolved "Isabelle-Solidity.Solidity")
Failed to load theory "Isabelle-Solidity.Contract" (unresolved "Isabelle-Solidity.Solidity", "Isabelle-Solidity.WP")
Failed to load theory "Isabelle-Solidity.Solidity_Main" (unresolved "Isabelle-Solidity.Contract", "Isabelle-Solidity.WP")
Failed to load theory "Isabelle-Solidity.Bank" (unresolved "Isabelle-Solidity.Solidity_Main")
Failed to load theory "Isabelle-Solidity.Casino" (unresolved "Isabelle-Solidity.Solidity_Main")
Failed to load theory "Isabelle-Solidity.SimpleAuction" (unresolved "Isabelle-Solidity.Solidity_Main")
Failed to load theory "Isabelle-Solidity.Token" (unresolved "Isabelle-Solidity.Solidity_Main")
Failed to load theory "Isabelle-Solidity.Voting" (unresolved "Isabelle-Solidity.Solidity_Main")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 777 of "~~/dirs/AFP/thys/Isabelle-Solidity/Solidity.thy")
Failed to load theory "JinjaDCI.Value" (unresolved "JinjaDCI.TypeRel")
Failed to load theory "JinjaDCI.Objects" (unresolved "JinjaDCI.TypeRel", "JinjaDCI.Value")
Failed to load theory "JinjaDCI.Exceptions" (unresolved "JinjaDCI.Objects")
Failed to load theory "JinjaDCI.Conform" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.Expr" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.State" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.SystemClasses" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.JVMState" (unresolved "JinjaDCI.Objects")
Failed to load theory "JinjaDCI.JVMInstructions" (unresolved "JinjaDCI.JVMState")
Failed to load theory "JinjaDCI.JVMExceptions" (unresolved "JinjaDCI.Exceptions", "JinjaDCI.JVMInstructions")
Failed to load theory "JinjaDCI.JVMExecInstr" (unresolved "JinjaDCI.JVMExceptions", "JinjaDCI.JVMInstructions")
Failed to load theory "JinjaDCI.JVMExec" (unresolved "JinjaDCI.JVMExecInstr")
Failed to load theory "JinjaDCI.JVMDefensive" (unresolved "JinjaDCI.Conform", "JinjaDCI.JVMExec")
Failed to load theory "JinjaDCI.WellType" (unresolved "JinjaDCI.Expr", "JinjaDCI.Objects")
Failed to load theory "JinjaDCI.Annotate" (unresolved "JinjaDCI.WellType")
Failed to load theory "JinjaDCI.WellTypeRT" (unresolved "JinjaDCI.WellType")
Failed to load theory "JinjaDCI.WellForm" (unresolved "JinjaDCI.SystemClasses", "JinjaDCI.TypeRel")
Failed to load theory "JinjaDCI.PCompiler" (unresolved "JinjaDCI.WellForm")
Failed to load theory "JinjaDCI.SemiType" (unresolved "JinjaDCI.WellForm")
Failed to load theory "JinjaDCI.JVM_SemiType" (unresolved "JinjaDCI.SemiType")
Failed to load theory "JinjaDCI.Effect" (unresolved "JinjaDCI.JVMExceptions", "JinjaDCI.JVM_SemiType")
Failed to load theory "JinjaDCI.BVSpec" (unresolved "JinjaDCI.Effect")
Failed to load theory "JinjaDCI.BVConform" (unresolved "JinjaDCI.BVSpec", "JinjaDCI.Conform", "JinjaDCI.JVMExec")
Failed to load theory "JinjaDCI.ClassAdd" (unresolved "JinjaDCI.BVConform")
Failed to load theory "JinjaDCI.StartProg" (unresolved "JinjaDCI.ClassAdd")
Failed to load theory "JinjaDCI.BVSpecTypeSafe" (unresolved "JinjaDCI.BVConform", "JinjaDCI.StartProg")
Failed to load theory "JinjaDCI.BVNoTypeError" (unresolved "JinjaDCI.BVSpecTypeSafe", "JinjaDCI.JVMDefensive")
Failed to load theory "JinjaDCI.EffectMono" (unresolved "JinjaDCI.Effect")
Failed to load theory "JinjaDCI.TF_JVM" (unresolved "JinjaDCI.BVSpec", "JinjaDCI.EffectMono")
Failed to load theory "JinjaDCI.BVExec" (unresolved "JinjaDCI.TF_JVM")
Failed to load theory "JinjaDCI.LBVJVM" (unresolved "JinjaDCI.TF_JVM")
Failed to load theory "JinjaDCI.WWellForm" (unresolved "JinjaDCI.Expr", "JinjaDCI.WellForm")
Failed to load theory "JinjaDCI.BigStep" (unresolved "JinjaDCI.Expr", "JinjaDCI.State", "JinjaDCI.WWellForm")
Failed to load theory "JinjaDCI.DefAss" (unresolved "JinjaDCI.BigStep")
Failed to load theory "JinjaDCI.J1" (unresolved "JinjaDCI.BigStep")
Failed to load theory "JinjaDCI.Compiler2" (unresolved "JinjaDCI.J1", "JinjaDCI.JVMExec", "JinjaDCI.PCompiler")
Failed to load theory "JinjaDCI.JWellForm" (unresolved "JinjaDCI.DefAss", "JinjaDCI.WWellForm", "JinjaDCI.WellForm", "JinjaDCI.WellType")
Failed to load theory "JinjaDCI.J1WellForm" (unresolved "JinjaDCI.J1", "JinjaDCI.JWellForm")
Failed to load theory "JinjaDCI.SmallStep" (unresolved "JinjaDCI.Expr", "JinjaDCI.State", "JinjaDCI.WWellForm")
Failed to load theory "JinjaDCI.EConform" (unresolved "JinjaDCI.BigStep", "JinjaDCI.SmallStep")
Failed to load theory "JinjaDCI.Correctness2" (unresolved "JinjaDCI.Compiler2", "JinjaDCI.EConform", "JinjaDCI.J1WellForm")
Failed to load theory "JinjaDCI.Progress" (unresolved "JinjaDCI.Conform", "JinjaDCI.DefAss", "JinjaDCI.EConform", "JinjaDCI.WellTypeRT")
Failed to load theory "JinjaDCI.TypeSafe" (unresolved "JinjaDCI.BigStep", "JinjaDCI.JWellForm", "JinjaDCI.Progress", "JinjaDCI.SmallStep")
Failed to load theory "JinjaDCI.Equivalence" (unresolved "JinjaDCI.TypeSafe", "JinjaDCI.WWellForm")
Failed to load theory "JinjaDCI.Compiler1" (unresolved "JinjaDCI.J1", "JinjaDCI.PCompiler")
Failed to load theory "JinjaDCI.Correctness1" (unresolved "JinjaDCI.Compiler1", "JinjaDCI.J1WellForm")
Failed to load theory "JinjaDCI.Compiler" (unresolved "JinjaDCI.Correctness1", "JinjaDCI.Correctness2")
Failed to load theory "JinjaDCI.TypeComp" (unresolved "JinjaDCI.BVSpec", "JinjaDCI.Compiler")
Failed to load theory "JinjaDCI.JinjaDCI" (unresolved "JinjaDCI.Annotate", "JinjaDCI.BVExec", "JinjaDCI.BVNoTypeError", "JinjaDCI.Equivalence", "JinjaDCI.JVMDefensive", "JinjaDCI.LBVJVM", "JinjaDCI.TypeComp")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 682 of "~~/dirs/AFP/thys/JinjaDCI/Common/TypeRel.thy")
Failed to load theory "Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_main_proofs" (unresolved "Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_preliminaries")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 276 of "~~/dirs/AFP/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_preliminaries.thy")
Failed to load theory "Kolmogorov_Chentsov.Stochastic_Processes" (unresolved "Kolmogorov_Chentsov.Dyadic_Interval")
Failed to load theory "Kolmogorov_Chentsov.Kolmogorov_Chentsov" (unresolved "Kolmogorov_Chentsov.Dyadic_Interval", "Kolmogorov_Chentsov.Stochastic_Processes")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 185 of "~~/dirs/AFP/thys/Kolmogorov_Chentsov/Dyadic_Interval.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 254 of "~~/dirs/AFP/thys/Kruskal/UGraph_Impl.thy")
Failed to load theory "LLL_Basis_Reduction.FPLLL_Solver" (unresolved "LLL_Basis_Reduction.LLL_Certification")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 206 of "~~/dirs/AFP/thys/LLL_Basis_Reduction/LLL_Certification.thy")
Failed to load theory "LTL3_Semantics.LinearTemporalLogic" (unresolved "LTL3_Semantics.Traces")
Failed to load theory "LTL3_Semantics.LTL3" (unresolved "LTL3_Semantics.LinearTemporalLogic", "LTL3_Semantics.Traces")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 185 of "~~/dirs/AFP/thys/LTL3_Semantics/Traces.thy")
Failed to load theory "Lambda_Free_KBOs.Lambda_Free_KBOs" (unresolved "Lambda_Free_KBOs.Lambda_Encoding_KBO")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 99 of "~~/dirs/AFP/thys/Lambda_Free_KBOs/Lambda_Encoding_KBO.thy")
Failed to load theory "Lie_Groups.More_Manifolds" (unresolved "Lie_Groups.Groups_On_With")
Failed to load theory "Lie_Groups.Diff_PiE" (unresolved "Lie_Groups.More_Manifolds")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 224 of "~~/dirs/AFP/thys/Lie_Groups/Groups_On_With.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 146 of "~~/dirs/AFP/thys/Lie_Groups/Transfer_Cayley_Hamilton.thy")
Failed to load theory "Linear_Programming.LP_Preliminaries" (unresolved "Linear_Programming.More_Jordan_Normal_Forms")
Failed to load theory "Linear_Programming.Linear_Programming" (unresolved "Linear_Programming.LP_Preliminaries")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 360 of "~~/dirs/AFP/thys/Linear_Programming/More_Jordan_Normal_Forms.thy")
Failed to load theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code" (unresolved "Factor_Algebraic_Polynomial.MPoly_Divide")
Failed to load theory "Factor_Algebraic_Polynomial.Multivariate_Resultant" (unresolved "Factor_Algebraic_Polynomial.MPoly_Divide_Code")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly" (unresolved "Factor_Algebraic_Polynomial.Multivariate_Resultant")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly")
Failed to load theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl")
Failed to load theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly" (unresolved "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly")
Failed to load theory "Linear_Recurrences_Solver.Linear_Recurrences_Solver" (unresolved "Factor_Algebraic_Polynomial.Factor_Complex_Poly")
Failed to load theory "Linear_Recurrences_Solver.Linear_Recurrences_Test" (unresolved "Linear_Recurrences_Solver.Linear_Recurrences_Solver")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 42 of "~~/dirs/AFP/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy")
Failed to load theory "List_Update.BIT" (unresolved "List_Update.MTF2_Effects")
Failed to load theory "List_Update.List_Factoring" (unresolved "List_Update.MTF2_Effects")
Failed to load theory "List_Update.BIT_pairwise" (unresolved "List_Update.BIT", "List_Update.List_Factoring")
Failed to load theory "List_Update.BIT_2comp_on2" (unresolved "List_Update.BIT")
Failed to load theory "List_Update.TS" (unresolved "List_Update.List_Factoring")
Failed to load theory "List_Update.Comb" (unresolved "List_Update.BIT_2comp_on2", "List_Update.BIT_pairwise", "List_Update.TS")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 332 of "~~/dirs/AFP/thys/List_Update/MTF2_Effects.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 66 of "~~/dirs/AFP/thys/Localization_Ring/Localization.thy")
Failed to load theory "MDP-Algorithms.DiffArray_ST" (unresolved "MDP-Algorithms.DiffArray_Base")
Failed to load theory "MDP-Algorithms.Code_Setup" (unresolved "MDP-Algorithms.DiffArray_ST")
Failed to load theory "MDP-Algorithms.Fin_Code" (unresolved "MDP-Algorithms.Code_Setup")
Failed to load theory "MDP-Algorithms.Fin_Code_Export_Float" (unresolved "MDP-Algorithms.Fin_Code")
Failed to load theory "MDP-Algorithms.Fin_Code_Export_Rat" (unresolved "MDP-Algorithms.Fin_Code")
Failed to load theory "MDP-Algorithms.GS_Code" (unresolved "MDP-Algorithms.Code_Setup")
Failed to load theory "MDP-Algorithms.GS_Code_Export_Float" (unresolved "MDP-Algorithms.GS_Code")
Failed to load theory "MDP-Algorithms.GS_Code_Export_Rat" (unresolved "MDP-Algorithms.GS_Code")
Failed to load theory "MDP-Algorithms.MPI_Code" (unresolved "MDP-Algorithms.Code_Setup")
Failed to load theory "MDP-Algorithms.MPI_Code_Export_Float" (unresolved "MDP-Algorithms.MPI_Code")
Failed to load theory "MDP-Algorithms.MPI_Code_Export_Rat" (unresolved "MDP-Algorithms.MPI_Code")
Failed to load theory "MDP-Algorithms.VI_Code" (unresolved "MDP-Algorithms.Code_Setup")
Failed to load theory "MDP-Algorithms.VI_Code_Export_Float" (unresolved "MDP-Algorithms.VI_Code")
Failed to load theory "MDP-Algorithms.VI_Code_Export_Rat" (unresolved "MDP-Algorithms.VI_Code")
Failed to load theory "MDP-Algorithms.PI_Code" (unresolved "MDP-Algorithms.Code_Setup")
Failed to load theory "MDP-Algorithms.PI_Code_Export_Float" (unresolved "MDP-Algorithms.PI_Code")
Failed to load theory "MDP-Algorithms.PI_Code_Export_Rat" (unresolved "MDP-Algorithms.PI_Code")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 165 of "~~/dirs/AFP/thys/MDP-Algorithms/code/lib/DiffArray_Base.thy")
Failed to load theory "MLSSmf_to_MLSS.Place_Framework" (unresolved "MLSSmf_to_MLSS.MLSS_Extras")
Failed to load theory "MLSSmf_to_MLSS.MLSSmf_to_MLSS" (unresolved "MLSSmf_to_MLSS.MLSS_Extras")
Failed to load theory "MLSSmf_to_MLSS.Proper_Venn_Regions" (unresolved "MLSSmf_to_MLSS.MLSSmf_to_MLSS")
Failed to load theory "MLSSmf_to_MLSS.Place_Realisation" (unresolved "MLSSmf_to_MLSS.Place_Framework", "MLSSmf_to_MLSS.Proper_Venn_Regions")
Failed to load theory "MLSSmf_to_MLSS.Syntactic_Description" (unresolved "MLSSmf_to_MLSS.Place_Framework", "MLSSmf_to_MLSS.Proper_Venn_Regions")
Failed to load theory "MLSSmf_to_MLSS.MLSS_Decidable" (unresolved "MLSSmf_to_MLSS.Place_Realisation", "MLSSmf_to_MLSS.Syntactic_Description")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 33 of "~~/dirs/AFP/thys/MLSSmf_to_MLSS/MLSS_Extras.thy")
Failed to load theory "Matrices_for_ODEs.SQ_MTX" (unresolved "Matrices_for_ODEs.MTX_Norms")
Failed to load theory "Matrices_for_ODEs.MTX_Flows" (unresolved "Matrices_for_ODEs.SQ_MTX")
Failed to load theory "Matrices_for_ODEs.MTX_Examples" (unresolved "Matrices_for_ODEs.MTX_Flows")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 270 of "~~/dirs/AFP/thys/Matrices_for_ODEs/MTX_Norms.thy")
Failed to load theory "Metalogic_ProofChecker.BetaNorm" (unresolved "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.EtaNorm" (unresolved "Metalogic_ProofChecker.BetaNorm", "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.Instances" (unresolved "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.Name" (unresolved "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.Sorts" (unresolved "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.SortConstants" (unresolved "Metalogic_ProofChecker.Sorts")
Failed to load theory "Metalogic_ProofChecker.SortsExe" (unresolved "Metalogic_ProofChecker.Sorts")
Failed to load theory "Metalogic_ProofChecker.Term_Subst" (unresolved "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.Theory" (unresolved "Metalogic_ProofChecker.SortConstants", "Metalogic_ProofChecker.Sorts", "Metalogic_ProofChecker.Term")
Failed to load theory "Metalogic_ProofChecker.BetaNormProof" (unresolved "Metalogic_ProofChecker.BetaNorm", "Metalogic_ProofChecker.Theory")
Failed to load theory "Metalogic_ProofChecker.EtaNormProof" (unresolved "Metalogic_ProofChecker.BetaNormProof", "Metalogic_ProofChecker.EtaNorm", "Metalogic_ProofChecker.Theory")
Failed to load theory "Metalogic_ProofChecker.Logic" (unresolved "Metalogic_ProofChecker.BetaNormProof", "Metalogic_ProofChecker.EtaNormProof", "Metalogic_ProofChecker.Name", "Metalogic_ProofChecker.SortConstants", "Metalogic_ProofChecker.Term_Subst", "Metalogic_ProofChecker.Theory")
Failed to load theory "Metalogic_ProofChecker.EqualityProof" (unresolved "Metalogic_ProofChecker.Logic")
Failed to load theory "Metalogic_ProofChecker.ProofTerm" (unresolved "Metalogic_ProofChecker.EqualityProof", "Metalogic_ProofChecker.Logic", "Metalogic_ProofChecker.SortConstants", "Metalogic_ProofChecker.Term", "Metalogic_ProofChecker.Term_Subst")
Failed to load theory "Metalogic_ProofChecker.TheoryExe" (unresolved "Metalogic_ProofChecker.Instances", "Metalogic_ProofChecker.SortsExe", "Metalogic_ProofChecker.Theory")
Failed to load theory "Metalogic_ProofChecker.CheckerExe" (unresolved "Metalogic_ProofChecker.ProofTerm", "Metalogic_ProofChecker.TheoryExe")
Failed to load theory "Metalogic_ProofChecker.CodeGen" (unresolved "Metalogic_ProofChecker.CheckerExe", "Metalogic_ProofChecker.Instances", "Metalogic_ProofChecker.ProofTerm", "Metalogic_ProofChecker.TheoryExe")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 175 of "~~/dirs/AFP/thys/Metalogic_ProofChecker/Term.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 716 of "~~/dirs/AFP/thys/Mission_Time_LTL_Formula_Progression/MLTL_Formula_Progression.thy")
Failed to load theory "Mission_Time_LTL_to_Regular_Expression.WEST_Proofs" (unresolved "Mission_Time_LTL_to_Regular_Expression.WEST_Algorithms")
Failed to load theory "Mission_Time_LTL_to_Regular_Expression.Regex_Equivalence" (unresolved "Mission_Time_LTL_to_Regular_Expression.WEST_Algorithms", "Mission_Time_LTL_to_Regular_Expression.WEST_Proofs")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 692 of "~~/dirs/AFP/thys/Mission_Time_LTL_to_Regular_Expression/WEST_Algorithms.thy")
Failed to load theory "Monad_Memo_DP.Memory_Heap" (unresolved "Monad_Memo_DP.Pair_Memory")
Failed to load theory "Monad_Memo_DP.Heap_Main" (unresolved "Monad_Memo_DP.Memory_Heap")
Failed to load theory "Monad_Memo_DP.Heap_Default" (unresolved "Monad_Memo_DP.Heap_Main")
Failed to load theory "Monad_Memo_DP.CYK" (unresolved "Monad_Memo_DP.Heap_Default")
Failed to load theory "Monad_Memo_DP.Knapsack" (unresolved "Monad_Memo_DP.Heap_Default")
Failed to load theory "Monad_Memo_DP.OptBST" (unresolved "Monad_Memo_DP.Heap_Default")
Failed to load theory "Monad_Memo_DP.Tracing" (unresolved "Monad_Memo_DP.Heap_Main")
Failed to load theory "Monad_Memo_DP.Bellman_Ford" (unresolved "Monad_Memo_DP.Heap_Main", "Monad_Memo_DP.Tracing")
Failed to load theory "Monad_Memo_DP.Min_Ed_Dist0" (unresolved "Monad_Memo_DP.Heap_Main", "Monad_Memo_DP.Tracing")
Failed to load theory "Monad_Memo_DP.All_Examples" (unresolved "Monad_Memo_DP.Bellman_Ford", "Monad_Memo_DP.CYK", "Monad_Memo_DP.Knapsack", "Monad_Memo_DP.Min_Ed_Dist0", "Monad_Memo_DP.OptBST")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 278 of "~~/dirs/AFP/thys/Monad_Memo_DP/heap_monad/Pair_Memory.thy")
Failed to load theory "More_LazyLists.LazyList_Filtermap" (unresolved "More_LazyLists.LazyList_Operations")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 354 of "~~/dirs/AFP/thys/More_LazyLists/LazyList_Operations.thy")
Failed to load theory "Morley_Theorem.Complex_Triangles_Definitions" (unresolved "Morley_Theorem.Complex_Angles")
Failed to load theory "Morley_Theorem.Complex_Trigonometry" (unresolved "Morley_Theorem.Complex_Angles", "Morley_Theorem.Complex_Triangles_Definitions")
Failed to load theory "Morley_Theorem.Third_Unity_Root" (unresolved "Morley_Theorem.Complex_Angles")
Failed to load theory "Morley_Theorem.Complex_Triangles" (unresolved "Morley_Theorem.Complex_Trigonometry", "Morley_Theorem.Third_Unity_Root")
Failed to load theory "Morley_Theorem.Complex_Axial_Symmetry" (unresolved "Morley_Theorem.Complex_Angles", "Morley_Theorem.Complex_Triangles")
Failed to load theory "Morley_Theorem.Morley" (unresolved "Morley_Theorem.Complex_Axial_Symmetry")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 62 of "~~/dirs/AFP/thys/Morley_Theorem/Complex_Angles.thy")
/tmp/isabelle-isatest/bash_script13819404978295818444: line 2: lualatex: command not found
Failed to build document "document"
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 138 of "~~/dirs/AFP/thys/Multi_Party_Computation/Secure_Multiplication.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 251 of "~~/dirs/AFP/thys/Multi_Party_Computation/ETP_RSA_OT.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 582 of "~~/dirs/AFP/thys/Multi_Party_Computation/Malicious_OT.thy")
Failed to load theory "Multirelations_Heterogeneous.Multirelations_Basics" (unresolved "Multirelations_Heterogeneous.Power_Allegories_Properties")
Failed to load theory "Multirelations_Heterogeneous.Power_Allegories_Multirelations" (unresolved "Multirelations_Heterogeneous.Multirelations_Basics")
Failed to load theory "Multirelations_Heterogeneous.Multirelations" (unresolved "Multirelations_Heterogeneous.Power_Allegories_Multirelations")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 351 of "~~/dirs/AFP/thys/Multirelations_Heterogeneous/Power_Allegories_Properties.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 885 of "~~/dirs/AFP/thys/Multitape_To_Singletape_TM/Multi_Single_TM_Translation.thy")
Timeout
Failed to load theory "NREST.NREST" (unresolved "NREST.NREST_Auxiliaries")
Failed to load theory "NREST.DataRefinement" (unresolved "NREST.NREST")
Failed to load theory "NREST.SepLogic_Misc" (unresolved "NREST.DataRefinement")
Failed to load theory "NREST.RefineMonadicVCG" (unresolved "NREST.DataRefinement", "NREST.NREST")
Failed to load theory "NREST.Refine_Foreach" (unresolved "NREST.NREST", "NREST.RefineMonadicVCG", "NREST.SepLogic_Misc")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 74 of "~~/dirs/AFP/thys/NREST/NREST_Auxiliaries.thy")
Failed to load theory "Nagata-Factoriality.Localization_Interface" (unresolved "Localization_Ring.Localization")
Failed to load theory "Nagata-Factoriality.Nagata_Lemmas" (unresolved "Nagata-Factoriality.Localization_Interface")
Failed to load theory "Nagata-Factoriality.Polynomial_Applications" (unresolved "Nagata-Factoriality.Nagata_Lemmas")
Failed to load theory "Nagata-Factoriality.Fraction_Field_Applications" (unresolved "Nagata-Factoriality.Nagata_Lemmas", "Nagata-Factoriality.Polynomial_Applications")
Failed to load theory "Nagata-Factoriality.Nagata_Factoriality" (unresolved "Nagata-Factoriality.Fraction_Field_Applications", "Nagata-Factoriality.Nagata_Lemmas", "Nagata-Factoriality.Polynomial_Applications")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 66 of "~~/dirs/AFP/thys/Localization_Ring/Localization.thy")
/tmp/isabelle-isatest/bash_script9183565936241683808: line 2: lualatex: command not found
Failed to build document "document"
Failed to load theory "Notes_On_Goedels_Ontological_Argument.ThereIsNoEvil1" (unresolved "Notes_On_Goedels_Ontological_Argument.GoedelVariantHOML2")
Failed to load theory "Notes_On_Goedels_Ontological_Argument.ThereIsNoEvil2" (unresolved "Notes_On_Goedels_Ontological_Argument.GoedelVariantHOML3")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 36 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML3possInS4.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 32 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML3inS4.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 36 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML2possInS4.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 34 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML2inS4.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 28 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML1inS4.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 35 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/ScottVariantHOMLposs.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 13 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/ScottVariantHOMLAndersonQuant.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 38 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/ScottVariantHOML.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 30 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML3poss.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 29 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML3AndersonQuant.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 32 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML3.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 31 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML2poss.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 29 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML2AndersonQuant.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 32 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML2.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 36 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/EvilDerivable.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 30 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML1poss.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 30 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML1AndersonQuant.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 31 of "~~/dirs/AFP/thys/Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML1.thy")
Failed to load theory "Number_Theoretic_Transform.NTT" (unresolved "Number_Theoretic_Transform.Preliminary_Lemmas")
Failed to load theory "Number_Theoretic_Transform.Butterfly" (unresolved "Number_Theoretic_Transform.NTT")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy")
Failed to load theory "OmegaCatoidsQuantales.Two_Catoid" (unresolved "Catoids.Catoid")
Failed to load theory "OmegaCatoidsQuantales.Omega_Catoid" (unresolved "OmegaCatoidsQuantales.Two_Catoid")
Failed to load theory "OmegaCatoidsQuantales.Two_Catoid_Collapse" (unresolved "OmegaCatoidsQuantales.Two_Catoid")
Failed to load theory "Quantales.Quantale_Star" (unresolved "Quantales.Quantales")
Failed to load theory "Quantales_Converse.Modal_Quantale" (unresolved "Quantales.Quantale_Star")
Failed to load theory "Catoids.Catoid_Lifting" (unresolved "Catoids.Catoid", "Quantales_Converse.Modal_Quantale")
Failed to load theory "OmegaCatoidsQuantales.Omega_Quantale" (unresolved "OmegaCatoidsQuantales.Omega_Kleene_Algebra", "Quantales_Converse.Modal_Quantale")
Failed to load theory "OmegaCatoidsQuantales.Omega_Catoid_Lifting" (unresolved "OmegaCatoidsQuantales.Omega_Catoid", "OmegaCatoidsQuantales.Omega_Quantale")
Failed to load theory "OmegaCatoidsQuantales.Two_Quantale" (unresolved "Quantales_Converse.Modal_Quantale")
Failed to load theory "OmegaCatoidsQuantales.Two_Catoid_Lifting" (unresolved "Catoids.Catoid_Lifting", "OmegaCatoidsQuantales.Two_Catoid", "OmegaCatoidsQuantales.Two_Quantale")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 45 of "~~/dirs/AFP/thys/Quantales/Quantales.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 348 of "~~/dirs/AFP/thys/OmegaCatoidsQuantales/Omega_Kleene_Algebra.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 879 of "~~/dirs/AFP/thys/Catoids/Catoid.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 388 of "~~/dirs/AFP/thys/Order_Lattice_Props/Representations.thy")
Failed to load theory "Ordinal_Partitions.Erdos_Milner" (unresolved "Ordinal_Partitions.Partitions")
Failed to load theory "Ordinal_Partitions.Omega_Omega" (unresolved "Ordinal_Partitions.Erdos_Milner")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 122 of "~~/dirs/AFP/thys/Ordinal_Partitions/Partitions.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 372 of "~~/dirs/AFP/thys/Orient_Rewrite_Rule_Undecidable/Preliminaries_on_Polynomials_2.thy")
Failed to load theory "PAC_Checker.PAC_Checker_Synthesis" (unresolved "PAC_Checker.PAC_Checker_Init")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 116 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_Init.thy")
Failed to load theory "Padic_Field.Fraction_Field" (unresolved "Localization_Ring.Localization")
Failed to load theory "Padic_Field.Ring_Powers" (unresolved "Padic_Field.Cring_Multivariable_Poly", "Padic_Field.Indices")
Failed to load theory "Padic_Field.Padic_Fields" (unresolved "Padic_Field.Fraction_Field")
Failed to load theory "Padic_Field.Padic_Field_Polynomials" (unresolved "Padic_Field.Padic_Fields")
Failed to load theory "Padic_Field.Padic_Field_Topology" (unresolved "Padic_Field.Padic_Fields")
Failed to load theory "Padic_Field.Padic_Field_Powers" (unresolved "Padic_Field.Generated_Boolean_Algebra", "Padic_Field.Padic_Field_Polynomials", "Padic_Field.Padic_Field_Topology", "Padic_Field.Ring_Powers")
Failed to load theory "Padic_Field.Padic_Semialgebraic_Function_Ring" (unresolved "Padic_Field.Padic_Field_Powers")
Failed to load theory "Padic_Field.Padic_Field_Topology_Bridge" (unresolved "Padic_Field.Padic_Field_Topology")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 42 of "~~/dirs/AFP/thys/Padic_Field/Indices.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 411 of "~~/dirs/AFP/thys/Padic_Field/Generated_Boolean_Algebra.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 66 of "~~/dirs/AFP/thys/Localization_Ring/Localization.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 3921 of "~~/dirs/AFP/thys/Padic_Field/Cring_Multivariable_Poly.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 247 of "~~/dirs/AFP/thys/Paraconsistency/Paraconsistency_Validity_Infinite.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 138 of "~~/dirs/AFP/thys/Parikh/Pilling.thy")
Failed to load theory "Perron_Frobenius.Perron_Frobenius" (unresolved "Perron_Frobenius.Perron_Frobenius_Aux")
Failed to load theory "Perron_Frobenius.Perron_Frobenius_Irreducible" (unresolved "Perron_Frobenius.Perron_Frobenius", "Perron_Frobenius.Roots_Unity")
Failed to load theory "Perron_Frobenius.Perron_Frobenius_General" (unresolved "Perron_Frobenius.Perron_Frobenius_Irreducible")
Failed to load theory "Perron_Frobenius.Spectral_Radius_Theory" (unresolved "Perron_Frobenius.Perron_Frobenius")
Failed to load theory "Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block" (unresolved "Perron_Frobenius.Perron_Frobenius_General")
Failed to load theory "Perron_Frobenius.Spectral_Radius_Theory_2" (unresolved "Perron_Frobenius.Hom_Gauss_Jordan", "Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block")
Failed to load theory "Perron_Frobenius.Check_Matrix_Growth" (unresolved "Perron_Frobenius.Spectral_Radius_Theory_2")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 27 of "~~/dirs/AFP/thys/Perron_Frobenius/Hom_Gauss_Jordan.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 148 of "~~/dirs/AFP/thys/Perron_Frobenius/Perron_Frobenius_Aux.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/Perron_Frobenius/Roots_Unity.thy")
Failed to load theory "Planarity_Certificates.Permutations_2" (unresolved "Planarity_Certificates.Executable_Permutations")
Failed to load theory "Planarity_Certificates.Planar_Subdivision" (unresolved "Planarity_Certificates.Permutations_2")
Failed to load theory "Planarity_Certificates.Planar_Subgraph" (unresolved "Planarity_Certificates.Permutations_2")
Failed to load theory "Planarity_Certificates.Digraph_Map_Impl" (unresolved "Planarity_Certificates.Executable_Permutations")
Failed to load theory "Planarity_Certificates.Planar_Complete" (unresolved "Planarity_Certificates.Digraph_Map_Impl")
Failed to load theory "Planarity_Certificates.Kuratowski_Combinatorial" (unresolved "Planarity_Certificates.Planar_Complete", "Planarity_Certificates.Planar_Subdivision", "Planarity_Certificates.Planar_Subgraph")
Failed to load theory "Planarity_Certificates.Check_Non_Planarity_Verification" (unresolved "Planarity_Certificates.Kuratowski_Combinatorial")
Failed to load theory "Planarity_Certificates.Planarity_Certificates" (unresolved "Planarity_Certificates.Check_Non_Planarity_Verification", "Planarity_Certificates.Kuratowski_Combinatorial")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 1001 of "~~/dirs/AFP/thys/Planarity_Certificates/Planarity/Executable_Permutations.thy")
Failed to load theory "Poincare_Bendixson.ODE_Misc" (unresolved "Poincare_Bendixson.Analysis_Misc")
Failed to load theory "Poincare_Bendixson.Invariance" (unresolved "Poincare_Bendixson.ODE_Misc")
Failed to load theory "Poincare_Bendixson.Limit_Set" (unresolved "Poincare_Bendixson.Invariance")
Failed to load theory "Poincare_Bendixson.Periodic_Orbit" (unresolved "Poincare_Bendixson.Analysis_Misc", "Poincare_Bendixson.Limit_Set", "Poincare_Bendixson.ODE_Misc")
Failed to load theory "Poincare_Bendixson.Poincare_Bendixson" (unresolved "Poincare_Bendixson.Analysis_Misc", "Poincare_Bendixson.ODE_Misc", "Poincare_Bendixson.Periodic_Orbit")
Failed to load theory "Poincare_Bendixson.Examples" (unresolved "Poincare_Bendixson.Affine_Arithmetic_Misc", "Poincare_Bendixson.Poincare_Bendixson")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 119 of "~~/dirs/AFP/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 34 of "~~/dirs/AFP/thys/Poincare_Bendixson/Analysis_Misc.thy")
Failed to load theory "Poincare_Disc.Poincare_Lines_Ideal_Points" (unresolved "Poincare_Disc.Poincare_Lines")
Failed to load theory "Poincare_Disc.Poincare_Distance" (unresolved "Poincare_Disc.Hyperbolic_Functions", "Poincare_Disc.Poincare_Lines_Ideal_Points")
Failed to load theory "Poincare_Disc.Poincare_Between" (unresolved "Poincare_Disc.Poincare_Distance")
Failed to load theory "Poincare_Disc.Poincare_Lines_Axis_Intersections" (unresolved "Poincare_Disc.Poincare_Between")
Failed to load theory "Poincare_Disc.Poincare_Perpendicular" (unresolved "Poincare_Disc.Poincare_Lines_Axis_Intersections")
Failed to load theory "Poincare_Disc.Poincare_Circles" (unresolved "Poincare_Disc.Poincare_Distance")
Failed to load theory "Poincare_Disc.Poincare" (unresolved "Poincare_Disc.Poincare_Between", "Poincare_Disc.Poincare_Circles", "Poincare_Disc.Poincare_Distance", "Poincare_Disc.Poincare_Lines")
Failed to load theory "Poincare_Disc.Poincare_Tarski" (unresolved "Poincare_Disc.Poincare", "Poincare_Disc.Poincare_Lines_Axis_Intersections")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 83 of "~~/dirs/AFP/thys/Poincare_Disc/Hyperbolic_Functions.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 74 of "~~/dirs/AFP/thys/Poincare_Disc/Poincare_Lines.thy")
Failed to load theory "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss" (unresolved "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Lemmas")
Failed to load theory "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Cauchy" (unresolved "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss")
Failed to load theory "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Legendre" (unresolved "Polygonal_Number_Theorem.Polygonal_Number_Theorem_Gauss")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 483 of "~~/dirs/AFP/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 123 of "~~/dirs/AFP/thys/Prim_Dijkstra_Simple/Common.thy")
Failed to load theory "Timed_Automata.Approx_Beta" (unresolved "Timed_Automata.Regions_Beta")
Failed to load theory "Probabilistic_Timed_Automata.Lib" (unresolved "Timed_Automata.Approx_Beta")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 603 of "~~/dirs/AFP/thys/Timed_Automata/Regions_Beta.thy")
Failed to load theory "ProcessComposition.ResNormCompare" (unresolved "ProcessComposition.ResNormDirect", "ProcessComposition.ResNormRewrite")
Failed to load theory "ProcessComposition.Resource" (unresolved "ProcessComposition.ResNormCompare")
Failed to load theory "ProcessComposition.Process" (unresolved "ProcessComposition.Resource")
Failed to load theory "ProcessComposition.CopyableElimination" (unresolved "ProcessComposition.Process")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 127 of "~~/dirs/AFP/thys/ProcessComposition/ResNormRewrite.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 340 of "~~/dirs/AFP/thys/ProcessComposition/ResNormDirect.thy")
Failed to load theory "Progress_Tracking.Combined" (unresolved "Progress_Tracking.Exchange")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 980 of "~~/dirs/AFP/thys/Progress_Tracking/Exchange.thy")
Failed to load theory "Projective_Geometry.Desargues_2D" (unresolved "Projective_Geometry.Matroid_Rank_Properties")
Failed to load theory "Projective_Geometry.Desargues_3D" (unresolved "Projective_Geometry.Matroid_Rank_Properties")
Failed to load theory "Projective_Geometry.Pascal_Property" (unresolved "Projective_Geometry.Pappus_Property")
Failed to load theory "Projective_Geometry.Desargues_Property" (unresolved "Projective_Geometry.Pappus_Property", "Projective_Geometry.Pascal_Property")
Failed to load theory "Projective_Geometry.Pappus_Desargues" (unresolved "Projective_Geometry.Desargues_Property", "Projective_Geometry.Pappus_Property", "Projective_Geometry.Pascal_Property")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 110 of "~~/dirs/AFP/thys/Projective_Geometry/Pappus_Property.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 52 of "~~/dirs/AFP/thys/Projective_Geometry/Matroid_Rank_Properties.thy")
Timeout
Failed to load theory "Prpu_Maxflow.Fifo_Push_Relabel" (unresolved "Prpu_Maxflow.Generic_Push_Relabel")
Failed to load theory "Prpu_Maxflow.Prpu_Common_Inst" (unresolved "Prpu_Maxflow.Generic_Push_Relabel")
Failed to load theory "Prpu_Maxflow.Prpu_Common_Impl" (unresolved "Prpu_Maxflow.Prpu_Common_Inst")
Failed to load theory "Prpu_Maxflow.Fifo_Push_Relabel_Impl" (unresolved "Prpu_Maxflow.Fifo_Push_Relabel", "Prpu_Maxflow.Prpu_Common_Impl")
Failed to load theory "Prpu_Maxflow.Relabel_To_Front" (unresolved "Prpu_Maxflow.Prpu_Common_Inst")
Failed to load theory "Prpu_Maxflow.Relabel_To_Front_Impl" (unresolved "Prpu_Maxflow.Prpu_Common_Impl", "Prpu_Maxflow.Relabel_To_Front")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 439 of "~~/dirs/AFP/thys/Prpu_Maxflow/Generic_Push_Relabel.thy")
Failed to load theory "Pushdown_Systems.PDS" (unresolved "Pushdown_Systems.P_Automata")
Failed to load theory "Pushdown_Systems.PDS_Code" (unresolved "Pushdown_Systems.PDS")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 78 of "~~/dirs/AFP/thys/Pushdown_Systems/P_Automata.thy")
Failed to load theory "Q0_Soundness.HOLZF_Set_Theory" (unresolved "Q0_Soundness.Set_Theory")
Failed to load theory "Q0_Soundness.Q0" (unresolved "Q0_Soundness.Set_Theory")
Failed to load theory "Q0_Soundness.ZFC_in_HOL_Set_Theory" (unresolved "Q0_Soundness.Set_Theory")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 526 of "~~/dirs/AFP/thys/Q0_Soundness/Set_Theory.thy")
Failed to load theory "Quantales.Quantale_Star" (unresolved "Quantales.Quantales")
Failed to load theory "Quantales_Converse.Modal_Quantale" (unresolved "Quantales.Quantale_Star")
Failed to load theory "Quantales_Converse.Quantale_Converse" (unresolved "Quantales_Converse.Modal_Quantale")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 45 of "~~/dirs/AFP/thys/Quantales/Quantales.thy")
Failed to load theory "BenOr_Kozen_Reif.BKR_Proofs" (unresolved "BenOr_Kozen_Reif.Matrix_Equation_Construction")
Failed to load theory "BenOr_Kozen_Reif.Renegar_Proofs" (unresolved "BenOr_Kozen_Reif.BKR_Proofs")
Failed to load theory "Virtual_Substitution.PolyAtoms" (unresolved "Virtual_Substitution.ExecutiblePolyProps")
Failed to load theory "Virtual_Substitution.Debruijn" (unresolved "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Optimizations" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.OptimizationProofs" (unresolved "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.Reindex" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.UniAtoms" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.VSAlgos" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.DNF" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.Heuristic" (unresolved "Virtual_Substitution.Optimizations", "Virtual_Substitution.Reindex", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.LinearCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.NegInfinity" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.QuadraticCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.EliminateVariable" (unresolved "Virtual_Substitution.LinearCase", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.LuckyFind" (unresolved "Virtual_Substitution.EliminateVariable")
Failed to load theory "Virtual_Substitution.EqualityVS" (unresolved "Virtual_Substitution.EliminateVariable", "Virtual_Substitution.LuckyFind")
Failed to load theory "Virtual_Substitution.Infinitesimals" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.LinearCase", "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.NegInfinityUni" (unresolved "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.InfinitesimalsUni" (unresolved "Virtual_Substitution.Infinitesimals", "Virtual_Substitution.NegInfinityUni", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.DNFUni" (unresolved "Virtual_Substitution.InfinitesimalsUni", "Virtual_Substitution.QE")
Failed to load theory "Virtual_Substitution.GeneralVSProofs" (unresolved "Virtual_Substitution.DNFUni", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.VSQuad" (unresolved "Virtual_Substitution.DNF", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.GeneralVSProofs", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.Reindex")
Failed to load theory "Quantifier_Elimination_Hybrid.Multiv_Poly_Props" (unresolved "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.VSQuad")
Failed to load theory "Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments" (unresolved "Quantifier_Elimination_Hybrid.Multiv_Poly_Props")
Failed to load theory "Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence" (unresolved "Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments")
Failed to load theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix" (unresolved "Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence")
Failed to load theory "Quantifier_Elimination_Hybrid.Multiv_Tarski_Query" (unresolved "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix", "Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence")
Failed to load theory "Virtual_Substitution.HeuristicProofs" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.VSQuad")
Failed to load theory "Virtual_Substitution.PrettyPrinting" (unresolved "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Exports" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.Optimizations", "Virtual_Substitution.PrettyPrinting", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.ExportProofs" (unresolved "Virtual_Substitution.Exports", "Virtual_Substitution.HeuristicProofs", "Virtual_Substitution.PrettyPrinting")
Failed to load theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm" (unresolved "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix", "Virtual_Substitution.ExportProofs")
Failed to load theory "BenOr_Kozen_Reif.BKR_Decision" (unresolved "BenOr_Kozen_Reif.BKR_Proofs")
Failed to load theory "BenOr_Kozen_Reif.Renegar_Decision" (unresolved "BenOr_Kozen_Reif.BKR_Decision", "BenOr_Kozen_Reif.Renegar_Proofs")
Failed to load theory "Quantifier_Elimination_Hybrid.Renegar_Modified" (unresolved "BenOr_Kozen_Reif.Renegar_Decision")
Failed to load theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs" (unresolved "BenOr_Kozen_Reif.Matrix_Equation_Construction", "BenOr_Kozen_Reif.Renegar_Proofs", "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm", "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix", "Quantifier_Elimination_Hybrid.Multiv_Tarski_Query", "Quantifier_Elimination_Hybrid.Renegar_Modified")
Failed to load theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs" (unresolved "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm", "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs", "Virtual_Substitution.ExportProofs")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 249 of "~~/dirs/AFP/thys/Virtual_Substitution/QE.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 264 of "~~/dirs/AFP/thys/Virtual_Substitution/ExecutiblePolyProps.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 264 of "~~/dirs/AFP/thys/BenOr_Kozen_Reif/Matrix_Equation_Construction.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 3627 of "~~/dirs/AFP/thys/Quantum_Fourier_Transform/QFT.thy")
Failed to load theory "Query_Optimization.Directed_Tree_Additions" (unresolved "Query_Optimization.Graph_Additions")
Failed to load theory "Query_Optimization.Dtree" (unresolved "Query_Optimization.Directed_Tree_Additions")
Failed to load theory "Query_Optimization.List_Dtree" (unresolved "Query_Optimization.Dtree", "Query_Optimization.Graph_Additions")
Failed to load theory "Query_Optimization.QueryGraph" (unresolved "Query_Optimization.Graph_Additions")
Failed to load theory "Query_Optimization.IKKBZ" (unresolved "Query_Optimization.CostFunctions", "Query_Optimization.List_Dtree", "Query_Optimization.QueryGraph")
Failed to load theory "Query_Optimization.IKKBZ_Optimality" (unresolved "Query_Optimization.CostFunctions", "Query_Optimization.IKKBZ", "Query_Optimization.QueryGraph")
Failed to load theory "Query_Optimization.IKKBZ_Examples" (unresolved "Query_Optimization.IKKBZ_Optimality")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 255 of "~~/dirs/AFP/thys/Query_Optimization/Graph_Additions.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 838 of "~~/dirs/AFP/thys/Query_Optimization/CostFunctions.thy")
Failed to load theory "Approximate_Model_Counting.ApproxMCCoreAnalysis" (unresolved "Approximate_Model_Counting.ApproxMCCore")
Failed to load theory "Approximate_Model_Counting.RandomXORHashFamily" (unresolved "Approximate_Model_Counting.RandomXOR")
Failed to load theory "Approximate_Model_Counting.ApproxMCAnalysis" (unresolved "Approximate_Model_Counting.ApproxMCCoreAnalysis", "Approximate_Model_Counting.RandomXORHashFamily")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Real" (unresolved "Akra_Bazzi.Akra_Bazzi_Asymptotics")
Failed to load theory "Akra_Bazzi.Akra_Bazzi" (unresolved "Akra_Bazzi.Akra_Bazzi_Real")
Failed to load theory "Akra_Bazzi.Master_Theorem" (unresolved "Akra_Bazzi.Akra_Bazzi")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Method" (unresolved "Akra_Bazzi.Akra_Bazzi", "Akra_Bazzi.Master_Theorem")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Approximation" (unresolved "Akra_Bazzi.Akra_Bazzi_Method")
Failed to load theory "Closest_Pair_Points.Common" (unresolved "Akra_Bazzi.Akra_Bazzi_Approximation", "Akra_Bazzi.Akra_Bazzi_Method")
Failed to load theory "Randomized_Closest_Pair.Randomized_Closest_Pair" (unresolved "Closest_Pair_Points.Common")
Failed to load theory "Randomized_Closest_Pair.Randomized_Closest_Pair_Correct" (unresolved "Randomized_Closest_Pair.Randomized_Closest_Pair")
Failed to load theory "Randomized_Closest_Pair.Randomized_Closest_Pair_Growth" (unresolved "Randomized_Closest_Pair.Randomized_Closest_Pair_Correct")
Failed to load theory "Randomized_Closest_Pair.Randomized_Closest_Pair_Time" (unresolved "Approximate_Model_Counting.ApproxMCAnalysis", "Randomized_Closest_Pair.Randomized_Closest_Pair_Growth")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 241 of "~~/dirs/AFP/thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1315 of "~~/dirs/AFP/thys/Approximate_Model_Counting/RandomXOR.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 236 of "~~/dirs/AFP/thys/Approximate_Model_Counting/ApproxMCCore.thy")
Failed to load theory "Real_Time_Deque.RealTimeDeque_Dequeue_Proof" (unresolved "Real_Time_Deque.States_Proof")
Failed to load theory "Real_Time_Deque.RealTimeDeque_Enqueue_Proof" (unresolved "Real_Time_Deque.States_Proof")
Failed to load theory "Real_Time_Deque.RealTimeDeque_Proof" (unresolved "Real_Time_Deque.RealTimeDeque_Dequeue_Proof", "Real_Time_Deque.RealTimeDeque_Enqueue_Proof")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 834 of "~~/dirs/AFP/thys/Real_Time_Deque/States_Proof.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 219 of "~~/dirs/AFP/thys/Region_Quadtrees/Quad_Matrix.thy")
Failed to load theory "JinjaDCI.Value" (unresolved "JinjaDCI.TypeRel")
Failed to load theory "JinjaDCI.Objects" (unresolved "JinjaDCI.TypeRel", "JinjaDCI.Value")
Failed to load theory "JinjaDCI.Exceptions" (unresolved "JinjaDCI.Objects")
Failed to load theory "JinjaDCI.Conform" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.SystemClasses" (unresolved "JinjaDCI.Exceptions")
Failed to load theory "JinjaDCI.JVMState" (unresolved "JinjaDCI.Objects")
Failed to load theory "JinjaDCI.JVMInstructions" (unresolved "JinjaDCI.JVMState")
Failed to load theory "JinjaDCI.JVMExceptions" (unresolved "JinjaDCI.Exceptions", "JinjaDCI.JVMInstructions")
Failed to load theory "JinjaDCI.JVMExecInstr" (unresolved "JinjaDCI.JVMExceptions", "JinjaDCI.JVMInstructions")
Failed to load theory "JinjaDCI.JVMExec" (unresolved "JinjaDCI.JVMExecInstr")
Failed to load theory "Regression_Test_Selection.JVMExecStepInductive" (unresolved "JinjaDCI.JVMExec")
Failed to load theory "JinjaDCI.WellForm" (unresolved "JinjaDCI.SystemClasses", "JinjaDCI.TypeRel")
Failed to load theory "JinjaDCI.SemiType" (unresolved "JinjaDCI.WellForm")
Failed to load theory "JinjaDCI.JVM_SemiType" (unresolved "JinjaDCI.SemiType")
Failed to load theory "JinjaDCI.Effect" (unresolved "JinjaDCI.JVMExceptions", "JinjaDCI.JVM_SemiType")
Failed to load theory "JinjaDCI.BVSpec" (unresolved "JinjaDCI.Effect")
Failed to load theory "JinjaDCI.BVConform" (unresolved "JinjaDCI.BVSpec", "JinjaDCI.Conform", "JinjaDCI.JVMExec")
Failed to load theory "JinjaDCI.ClassAdd" (unresolved "JinjaDCI.BVConform")
Failed to load theory "JinjaDCI.StartProg" (unresolved "JinjaDCI.ClassAdd")
Failed to load theory "JinjaDCI.BVSpecTypeSafe" (unresolved "JinjaDCI.BVConform", "JinjaDCI.StartProg")
Failed to load theory "Regression_Test_Selection.Subcls" (unresolved "JinjaDCI.TypeRel")
Failed to load theory "Regression_Test_Selection.ClassesAbove" (unresolved "JinjaDCI.Exceptions", "Regression_Test_Selection.Subcls")
Failed to load theory "Regression_Test_Selection.JVMSemantics" (unresolved "JinjaDCI.JVMExec")
Failed to load theory "Regression_Test_Selection.JVMCollectionSemantics" (unresolved "Regression_Test_Selection.ClassesAbove", "Regression_Test_Selection.JVMSemantics")
Failed to load theory "Regression_Test_Selection.JVMCollectionBasedRTS" (unresolved "JinjaDCI.BVSpecTypeSafe", "Regression_Test_Selection.JVMCollectionSemantics", "Regression_Test_Selection.JVMExecStepInductive")
Failed to load theory "Regression_Test_Selection.RTS" (unresolved "Regression_Test_Selection.JVMCollectionBasedRTS")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 682 of "~~/dirs/AFP/thys/JinjaDCI/Common/TypeRel.thy")
Failed to load theory "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl" (unresolved "First_Order_Terms.Term_Impl")
Failed to load theory "Regular_Tree_Relations.Tree_Automata_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl")
Failed to load theory "Regular_Tree_Relations.Regular_Relation_Impl" (unresolved "Regular_Tree_Relations.Tree_Automata_Impl")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 178 of "~~/dirs/AFP/thys/First_Order_Terms/Term_Impl.thy")
Failed to load theory "Relational_Paths.Paths" (unresolved "Relational_Paths.More_Relation_Algebra")
Failed to load theory "Relational_Paths.Rooted_Paths" (unresolved "Relational_Paths.Paths")
Failed to load theory "Relational_Paths.Path_Algorithms" (unresolved "Relational_Paths.Rooted_Paths")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 588 of "~~/dirs/AFP/thys/Relational_Paths/More_Relation_Algebra.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1800 of "~~/dirs/AFP/thys/Rep_Fin_Groups/Rep_Fin_Groups.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 982 of "~~/dirs/AFP/thys/SCC_Bloemen_Sequential/SCC_Bloemen_Sequential.thy")
Failed to load theory "Safe_Distance.Evaluation" (unresolved "Safe_Distance.Safe_Distance")
Failed to load theory "Safe_Distance.Safe_Distance_Reaction" (unresolved "Safe_Distance.Safe_Distance")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 871 of "~~/dirs/AFP/thys/Safe_Distance/Safe_Distance.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 444 of "~~/dirs/AFP/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Real" (unresolved "Akra_Bazzi.Akra_Bazzi_Asymptotics")
Failed to load theory "Akra_Bazzi.Akra_Bazzi" (unresolved "Akra_Bazzi.Akra_Bazzi_Real")
Failed to load theory "Akra_Bazzi.Master_Theorem" (unresolved "Akra_Bazzi.Akra_Bazzi")
Failed to load theory "Akra_Bazzi.Akra_Bazzi_Method" (unresolved "Akra_Bazzi.Akra_Bazzi", "Akra_Bazzi.Master_Theorem")
Failed to load theory "Karatsuba.Karatsuba_Runtime_Lemmas" (unresolved "Akra_Bazzi.Akra_Bazzi_Method")
Failed to load theory "Karatsuba.Nat_LSBF_TM" (unresolved "Karatsuba.Karatsuba_Runtime_Lemmas")
Failed to load theory "Karatsuba.Karatsuba_TM" (unresolved "Karatsuba.Nat_LSBF_TM")
Failed to load theory "Schoenhage_Strassen.Z_mod_power_of_2" (unresolved "Karatsuba.Nat_LSBF_TM")
Failed to load theory "Schoenhage_Strassen.Z_mod_power_of_2_TM" (unresolved "Karatsuba.Nat_LSBF_TM", "Schoenhage_Strassen.Z_mod_power_of_2")
Failed to load theory "Schoenhage_Strassen.Schoenhage_Strassen_Runtime_Preliminaries" (unresolved "Akra_Bazzi.Akra_Bazzi", "Karatsuba.Nat_LSBF_TM")
Failed to load theory "Number_Theoretic_Transform.NTT" (unresolved "Number_Theoretic_Transform.Preliminary_Lemmas")
Failed to load theory "Number_Theoretic_Transform.Butterfly" (unresolved "Number_Theoretic_Transform.NTT")
Failed to load theory "Schoenhage_Strassen.NTT_Rings" (unresolved "Number_Theoretic_Transform.NTT")
Failed to load theory "Schoenhage_Strassen.FNTT_Rings" (unresolved "Number_Theoretic_Transform.Butterfly", "Schoenhage_Strassen.NTT_Rings")
Failed to load theory "Schoenhage_Strassen.Z_mod_Fermat" (unresolved "Schoenhage_Strassen.FNTT_Rings", "Schoenhage_Strassen.Z_mod_power_of_2")
Failed to load theory "Schoenhage_Strassen.Schoenhage_Strassen" (unresolved "Schoenhage_Strassen.Z_mod_Fermat", "Schoenhage_Strassen.Z_mod_power_of_2")
Failed to load theory "Schoenhage_Strassen.Z_mod_Fermat_TM" (unresolved "Schoenhage_Strassen.Schoenhage_Strassen_Runtime_Preliminaries", "Schoenhage_Strassen.Z_mod_Fermat", "Schoenhage_Strassen.Z_mod_power_of_2_TM")
Failed to load theory "Schoenhage_Strassen.Schoenhage_Strassen_TM" (unresolved "Karatsuba.Karatsuba_TM", "Schoenhage_Strassen.Schoenhage_Strassen", "Schoenhage_Strassen.Z_mod_Fermat_TM")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/Number_Theoretic_Transform/Preliminary_Lemmas.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 241 of "~~/dirs/AFP/thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 84 of "~~/dirs/AFP/thys/Schutz_Spacetime/Util.thy")
Failed to load theory "Set_Reconciliation.Factorisation" (unresolved "Elimination_Of_Repeated_Factors.ERF_Algorithm")
Failed to load theory "Set_Reconciliation.Set_Reconciliation" (unresolved "Set_Reconciliation.Factorisation")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 207 of "~~/dirs/AFP/thys/Elimination_Of_Repeated_Factors/ERF_Algorithm.thy")
Failed to load theory "Shadow_DOM.Shadow_DOM_BaseTest" (unresolved "Shadow_DOM.Shadow_DOM")
Failed to load theory "Shadow_DOM.Shadow_DOM_Document_adoptNode" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.Shadow_DOM_Document_getElementById" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.Shadow_DOM_Node_insertBefore" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.Shadow_DOM_Node_removeChild" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.slots" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.slots_fallback" (unresolved "Shadow_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_DOM.Shadow_DOM_Tests" (unresolved "Shadow_DOM.Shadow_DOM_Document_adoptNode", "Shadow_DOM.Shadow_DOM_Document_getElementById", "Shadow_DOM.Shadow_DOM_Node_insertBefore", "Shadow_DOM.Shadow_DOM_Node_removeChild", "Shadow_DOM.slots", "Shadow_DOM.slots_fallback")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 5171 of "~~/dirs/AFP/thys/Shadow_DOM/Shadow_DOM.thy")
Failed to load theory "Shadow_SC_DOM.ShadowRootMonad" (unresolved "Shadow_SC_DOM.ShadowRootClass")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM" (unresolved "Shadow_SC_DOM.ShadowRootMonad")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_BaseTest" (unresolved "Shadow_SC_DOM.Shadow_DOM")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_Document_adoptNode" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_Document_getElementById" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_Node_insertBefore" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_Node_removeChild" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.slots" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.slots_fallback" (unresolved "Shadow_SC_DOM.Shadow_DOM_BaseTest")
Failed to load theory "Shadow_SC_DOM.Shadow_DOM_Tests" (unresolved "Shadow_SC_DOM.Shadow_DOM_Document_adoptNode", "Shadow_SC_DOM.Shadow_DOM_Document_getElementById", "Shadow_SC_DOM.Shadow_DOM_Node_insertBefore", "Shadow_SC_DOM.Shadow_DOM_Node_removeChild", "Shadow_SC_DOM.slots", "Shadow_SC_DOM.slots_fallback")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 230 of "~~/dirs/AFP/thys/Shadow_SC_DOM/classes/ShadowRootClass.thy")
Failed to load theory "Sigma_Commit_Crypto.Discrete_Log" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext")
Failed to load theory "Sigma_Commit_Crypto.Sigma_AND" (unresolved "Sigma_Commit_Crypto.Sigma_Protocols", "Sigma_Commit_Crypto.Xor")
Failed to load theory "Sigma_Commit_Crypto.Sigma_OR" (unresolved "Sigma_Commit_Crypto.Sigma_Protocols", "Sigma_Commit_Crypto.Xor")
Failed to load theory "Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext", "Sigma_Commit_Crypto.Discrete_Log", "Sigma_Commit_Crypto.Sigma_Protocols")
Failed to load theory "Sigma_Commit_Crypto.Okamoto_Sigma_Commit" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext", "Sigma_Commit_Crypto.Discrete_Log", "Sigma_Commit_Crypto.Sigma_Protocols")
Failed to load theory "Sigma_Commit_Crypto.Pedersen" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext", "Sigma_Commit_Crypto.Discrete_Log")
Failed to load theory "Sigma_Commit_Crypto.Rivest" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext", "Sigma_Commit_Crypto.Discrete_Log")
Failed to load theory "Sigma_Commit_Crypto.Schnorr_Sigma_Commit" (unresolved "Sigma_Commit_Crypto.Cyclic_Group_Ext", "Sigma_Commit_Crypto.Discrete_Log", "Sigma_Commit_Crypto.Sigma_Protocols")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 350 of "~~/dirs/AFP/thys/Sigma_Commit_Crypto/Sigma_Protocols.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 238 of "~~/dirs/AFP/thys/Sigma_Commit_Crypto/Cyclic_Group_Ext.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 132 of "~~/dirs/AFP/thys/Sigma_Commit_Crypto/Xor.thy")
Failed to load theory "Sigmoid_Universal_Approximation.Derivative_Identities_Smoothness" (unresolved "Sigmoid_Universal_Approximation.Sigmoid_Definition")
Failed to load theory "Sigmoid_Universal_Approximation.Asymptotic_Qualitative_Properties" (unresolved "Sigmoid_Universal_Approximation.Derivative_Identities_Smoothness")
Failed to load theory "Sigmoid_Universal_Approximation.Universal_Approximation" (unresolved "Sigmoid_Universal_Approximation.Asymptotic_Qualitative_Properties")
Failed to load theory "Sigmoid_Universal_Approximation.Sigmoid_Universal_Approximation" (unresolved "Sigmoid_Universal_Approximation.Asymptotic_Qualitative_Properties", "Sigmoid_Universal_Approximation.Derivative_Identities_Smoothness", "Sigmoid_Universal_Approximation.Sigmoid_Definition", "Sigmoid_Universal_Approximation.Universal_Approximation")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 200 of "~~/dirs/AFP/thys/Sigmoid_Universal_Approximation/Sigmoid_Definition.thy")
Failed to load theory "Signature_Groebner.Signature_Examples" (unresolved "Signature_Groebner.Signature_Groebner")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 3905 of "~~/dirs/AFP/thys/Signature_Groebner/Signature_Groebner.thy")
Failed to load theory "Simplicial_complexes_and_boolean_functions.Bij_betw_simplicial_complex_bool_func" (unresolved "Simplicial_complexes_and_boolean_functions.Simplicial_complex")
Failed to load theory "Simplicial_complexes_and_boolean_functions.Binary_operations" (unresolved "Simplicial_complexes_and_boolean_functions.Bij_betw_simplicial_complex_bool_func")
Failed to load theory "Simplicial_complexes_and_boolean_functions.Evasive" (unresolved "Simplicial_complexes_and_boolean_functions.Bij_betw_simplicial_complex_bool_func")
Failed to load theory "Simplicial_complexes_and_boolean_functions.BDD" (unresolved "Simplicial_complexes_and_boolean_functions.Evasive")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 596 of "~~/dirs/AFP/thys/Simplicial_complexes_and_boolean_functions/Simplicial_complex.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 30 of "~~/dirs/AFP/thys/SimplifiedOntologicalArgument/SimpleVariantSEinT.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 26 of "~~/dirs/AFP/thys/SimplifiedOntologicalArgument/ScottVariant.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 31 of "~~/dirs/AFP/thys/SimplifiedOntologicalArgument/KanckosLethenNo2Possibilist.thy")
Failed to load theory "Smith_Normal_Form.Cauchy_Binet_HOL_Analysis" (unresolved "Smith_Normal_Form.Cauchy_Binet")
Failed to load theory "Smith_Normal_Form.Elementary_Divisor_Rings" (unresolved "Smith_Normal_Form.SNF_Algorithm")
Failed to load theory "Smith_Normal_Form.Alternative_Proofs" (unresolved "Smith_Normal_Form.Elementary_Divisor_Rings")
Failed to load theory "Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain" (unresolved "Smith_Normal_Form.Elementary_Divisor_Rings")
Failed to load theory "Smith_Normal_Form.Smith_Certified" (unresolved "Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain")
Failed to load theory "Smith_Normal_Form.SNF_Algorithm_HOL_Analysis" (unresolved "Smith_Normal_Form.SNF_Algorithm")
Failed to load theory "Smith_Normal_Form.SNF_Uniqueness" (unresolved "Smith_Normal_Form.Cauchy_Binet")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1584 of "~~/dirs/AFP/thys/Smith_Normal_Form/SNF_Algorithm.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 51 of "~~/dirs/AFP/thys/Smith_Normal_Form/SNF_Algorithm_Two_Steps_JNF.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 46 of "~~/dirs/AFP/thys/Smith_Normal_Form/SNF_Algorithm_Two_Steps.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 98 of "~~/dirs/AFP/thys/Smith_Normal_Form/Cauchy_Binet.thy")
Failed to load theory "Solidity.Valuetypes" (unresolved "Solidity.ReadShow")
Failed to load theory "Solidity.Accounts" (unresolved "Solidity.Valuetypes")
Failed to load theory "Solidity.Storage" (unresolved "Solidity.Valuetypes")
Failed to load theory "Solidity.Utils" (unresolved "Solidity.ReadShow")
Failed to load theory "Solidity.StateMonad" (unresolved "Solidity.Utils")
Failed to load theory "Solidity.Environment" (unresolved "Solidity.Accounts", "Solidity.StateMonad", "Solidity.Storage")
Failed to load theory "Solidity.Contracts" (unresolved "Solidity.Environment")
Failed to load theory "Solidity.Expressions" (unresolved "Solidity.Contracts", "Solidity.StateMonad")
Failed to load theory "Solidity.Statements" (unresolved "Solidity.Expressions", "Solidity.StateMonad")
Failed to load theory "Solidity.Solidity_Main" (unresolved "Solidity.Environment", "Solidity.Statements", "Solidity.Storage", "Solidity.Valuetypes")
Failed to load theory "Solidity.Constant_Folding" (unresolved "Solidity.Solidity_Main")
Failed to load theory "Solidity.Solidity_Evaluator" (unresolved "Solidity.Solidity_Main")
Failed to load theory "Solidity.Weakest_Precondition" (unresolved "Solidity.Solidity_Main")
Failed to load theory "Solidity.Reentrancy" (unresolved "Solidity.Solidity_Evaluator", "Solidity.Weakest_Precondition")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 142 of "~~/dirs/AFP/thys/Solidity/ReadShow.thy")
Failed to load theory "Splitting_Framework.Disjunctive_Consequence_Relations" (unresolved "Splitting_Framework.Lazy_List_Limsup")
Failed to load theory "Splitting_Framework.Calculi_And_Annotations" (unresolved "Splitting_Framework.Disjunctive_Consequence_Relations")
Failed to load theory "Splitting_Framework.Modular_Splitting_Calculus" (unresolved "Splitting_Framework.Calculi_And_Annotations", "Splitting_Framework.Light_Lifting_to_Non_Ground_Calculi")
Failed to load theory "Splitting_Framework.Lightweight_Avatar" (unresolved "Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited", "Splitting_Framework.Modular_Splitting_Calculus")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 86 of "~~/dirs/AFP/thys/Splitting_Framework/Light_Lifting_to_Non_Ground_Calculi.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 444 of "~~/dirs/AFP/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 233 of "~~/dirs/AFP/thys/Splitting_Framework/Lazy_List_Limsup.thy")
Failed to load theory "Perron_Frobenius.Perron_Frobenius" (unresolved "Perron_Frobenius.Perron_Frobenius_Aux")
Failed to load theory "Perron_Frobenius.Perron_Frobenius_Irreducible" (unresolved "Perron_Frobenius.Perron_Frobenius", "Perron_Frobenius.Roots_Unity")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 148 of "~~/dirs/AFP/thys/Perron_Frobenius/Perron_Frobenius_Aux.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 22 of "~~/dirs/AFP/thys/Perron_Frobenius/Roots_Unity.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1281 of "~~/dirs/AFP/thys/Stone_Algebras/Stone_Construction.thy")
Failed to load theory "Stratified_Datalog.Program_Graph" (unresolved "Stratified_Datalog.Datalog")
Failed to load theory "Stratified_Datalog.Bit_Vector_Framework" (unresolved "Stratified_Datalog.Program_Graph")
Failed to load theory "Stratified_Datalog.Reachable_Nodes" (unresolved "Stratified_Datalog.Bit_Vector_Framework")
Failed to load theory "Stratified_Datalog.Reaching_Definitions" (unresolved "Stratified_Datalog.Bit_Vector_Framework")
Failed to load theory "Stratified_Datalog.Available_Expressions" (unresolved "Stratified_Datalog.Reaching_Definitions")
Failed to load theory "Stratified_Datalog.Very_Busy_Expressions" (unresolved "Stratified_Datalog.Available_Expressions")
Failed to load theory "Stratified_Datalog.Live_Variables" (unresolved "Stratified_Datalog.Reaching_Definitions")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 565 of "~~/dirs/AFP/thys/Stratified_Datalog/Datalog.thy")
Timeout
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 168 of "~~/dirs/AFP/thys/Swap_Distance/Swap_Distance.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1617 of "~~/dirs/AFP/thys/Taylor_Models/Polynomial_Expression.thy")
Failed to load theory "Three_Circles.Bernstein_01" (unresolved "Three_Circles.RRI_Misc")
Failed to load theory "Three_Circles.Bernstein" (unresolved "Three_Circles.Bernstein_01")
Failed to load theory "Three_Circles.Normal_Poly" (unresolved "Three_Circles.RRI_Misc")
Failed to load theory "Three_Circles.Three_Circles" (unresolved "Three_Circles.Bernstein", "Three_Circles.Normal_Poly")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 248 of "~~/dirs/AFP/thys/Three_Circles/RRI_Misc.thy")
Failed to load theory "Timed_Automata.Approx_Beta" (unresolved "Timed_Automata.Regions_Beta")
Failed to load theory "Timed_Automata.Simulation_Graphs_TA" (unresolved "Timed_Automata.Approx_Beta", "Timed_Automata.Simulation_Graphs")
Failed to load theory "Timed_Automata.Normalized_Zone_Semantics" (unresolved "Timed_Automata.Approx_Beta", "Timed_Automata.Simulation_Graphs_TA")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1219 of "~~/dirs/AFP/thys/Timed_Automata/Simulation_Graphs.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 603 of "~~/dirs/AFP/thys/Timed_Automata/Regions_Beta.thy")
Failed to load theory "Topological_Semantics.logics_quantifiers" (unresolved "Topological_Semantics.boolean_algebra_infinitary")
Failed to load theory "Topological_Semantics.conditions_negative" (unresolved "Topological_Semantics.conditions_positive")
Failed to load theory "Topological_Semantics.conditions_relativized" (unresolved "Topological_Semantics.conditions_negative")
Failed to load theory "Topological_Semantics.conditions_positive_infinitary" (unresolved "Topological_Semantics.boolean_algebra_infinitary", "Topological_Semantics.conditions_positive")
Failed to load theory "Topological_Semantics.conditions_negative_infinitary" (unresolved "Topological_Semantics.conditions_negative", "Topological_Semantics.conditions_positive_infinitary")
Failed to load theory "Topological_Semantics.conditions_relativized_infinitary" (unresolved "Topological_Semantics.conditions_negative_infinitary", "Topological_Semantics.conditions_relativized")
Failed to load theory "Topological_Semantics.logics_quantifiers_example" (unresolved "Topological_Semantics.conditions_positive_infinitary", "Topological_Semantics.logics_quantifiers")
Failed to load theory "Topological_Semantics.logics_operators" (unresolved "Topological_Semantics.conditions_positive")
Failed to load theory "Topological_Semantics.logics_LFI" (unresolved "Topological_Semantics.conditions_relativized_infinitary")
Failed to load theory "Topological_Semantics.logics_LFU" (unresolved "Topological_Semantics.conditions_relativized_infinitary")
Failed to load theory "Topological_Semantics.logics_negation" (unresolved "Topological_Semantics.conditions_relativized")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 125 of "~~/dirs/AFP/thys/Topological_Semantics/conditions_positive.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 102 of "~~/dirs/AFP/thys/Topological_Semantics/boolean_algebra_infinitary.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 87 of "~~/dirs/AFP/thys/Transcendence_Series_Hancl_Rucki/Transcendence_Series.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 81 of "~~/dirs/AFP/thys/Turans_Graph_Theorem/Turan.thy")
Failed to load theory "Two_Hermitian_Results.Misc_Matrix_Results" (unresolved "Complex_Bounded_Operators.Extra_Jordan_Normal_Form", "Fishers_Inequality.Matrix_Vector_Extras")
Failed to load theory "Two_Hermitian_Results.Cauchy_Eigenvalue_Interlacing" (unresolved "Two_Hermitian_Results.Misc_Matrix_Results")
Failed to load theory "Two_Hermitian_Results.Sylvester_Criterion" (unresolved "Two_Hermitian_Results.Cauchy_Eigenvalue_Interlacing")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 385 of "~~/dirs/AFP/thys/Fishers_Inequality/Matrix_Vector_Extras.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 313 of "~~/dirs/AFP/thys/Complex_Bounded_Operators/extra/Extra_Jordan_Normal_Form.thy")
Failed to load theory "VYDRA_MDL.Temporal" (unresolved "VYDRA_MDL.Window")
Failed to load theory "VYDRA_MDL.Monitor" (unresolved "VYDRA_MDL.Temporal")
Failed to load theory "VYDRA_MDL.Monitor_Code" (unresolved "VYDRA_MDL.Monitor")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 279 of "~~/dirs/AFP/thys/VYDRA_MDL/Window.thy")
Failed to load theory "Valuation.Valuation2" (unresolved "Valuation.Valuation1")
Failed to load theory "Valuation.Valuation3" (unresolved "Valuation.Valuation2")
Solver z3: Solver terminated abnormally with error code 127 At command "apply" (line 257 of "~~/dirs/AFP/thys/Valuation/Valuation1.thy")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness" (unresolved "Van_Emde_Boas_Trees.VEBT_Delete")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_DeleteBounds" (unresolved "Van_Emde_Boas_Trees.VEBT_Delete", "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_Uniqueness" (unresolved "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_Intf_Functional" (unresolved "Van_Emde_Boas_Trees.VEBT_Delete", "Van_Emde_Boas_Trees.VEBT_DeleteBounds", "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness", "Van_Emde_Boas_Trees.VEBT_Uniqueness")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_BuildupMemImp" (unresolved "Van_Emde_Boas_Trees.VEBT_DeleteBounds")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_SuccPredImperative" (unresolved "Van_Emde_Boas_Trees.VEBT_BuildupMemImp")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_DelImperative" (unresolved "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness", "Van_Emde_Boas_Trees.VEBT_SuccPredImperative")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_Intf_Imperative" (unresolved "Van_Emde_Boas_Trees.VEBT_BuildupMemImp", "Van_Emde_Boas_Trees.VEBT_DelImperative", "Van_Emde_Boas_Trees.VEBT_Delete", "Van_Emde_Boas_Trees.VEBT_DeleteBounds", "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness", "Van_Emde_Boas_Trees.VEBT_Intf_Functional", "Van_Emde_Boas_Trees.VEBT_SuccPredImperative", "Van_Emde_Boas_Trees.VEBT_Uniqueness")
Failed to load theory "Van_Emde_Boas_Trees.VEBT_Example" (unresolved "Van_Emde_Boas_Trees.VEBT_Intf_Imperative")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 1470 of "~~/dirs/AFP/thys/Van_Emde_Boas_Trees/VEBT_Delete.thy")
Failed to load theory "Van_der_Waerden.Van_der_Waerden" (unresolved "Van_der_Waerden.Digits")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 132 of "~~/dirs/AFP/thys/Van_der_Waerden/Digits.thy")
Failed to load theory "Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions" (unresolved "Verified_SAT_Based_AI_Planning.SAT_Plan_Base")
Failed to load theory "Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus" (unresolved "Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions")
Failed to load theory "Verified_SAT_Based_AI_Planning.Solve_SASP" (unresolved "Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 351 of "~~/dirs/AFP/thys/Verified_SAT_Based_AI_Planning/SAT_Plan_Base.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 62 of "~~/dirs/AFP/thys/VerifyThis2018/Challenge1_short.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 253 of "~~/dirs/AFP/thys/VerifyThis2018/Challenge1.thy")
Failed to load theory "VerifyThis2019.Challenge1B" (unresolved "VerifyThis2019.Challenge1A")
Failed to load theory "VerifyThis2019.Challenge3" (unresolved "VerifyThis2019.Parallel_Multiset_Fold")
Failed to load theory "VerifyThis2019.Challenge2B" (unresolved "VerifyThis2019.Challenge2A")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 162 of "~~/dirs/AFP/thys/VerifyThis2019/Challenge2A.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 285 of "~~/dirs/AFP/thys/VerifyThis2019/Challenge1A.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 121 of "~~/dirs/AFP/thys/VerifyThis2019/Parallel_Multiset_Fold.thy")
Failed to load theory "Virtual_Substitution.PolyAtoms" (unresolved "Virtual_Substitution.ExecutiblePolyProps")
Failed to load theory "Virtual_Substitution.Debruijn" (unresolved "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Optimizations" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.OptimizationProofs" (unresolved "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.Reindex" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.UniAtoms" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.VSAlgos" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.DNF" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.Heuristic" (unresolved "Virtual_Substitution.Optimizations", "Virtual_Substitution.Reindex", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.LinearCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.NegInfinity" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.QuadraticCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.EliminateVariable" (unresolved "Virtual_Substitution.LinearCase", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.LuckyFind" (unresolved "Virtual_Substitution.EliminateVariable")
Failed to load theory "Virtual_Substitution.EqualityVS" (unresolved "Virtual_Substitution.EliminateVariable", "Virtual_Substitution.LuckyFind")
Failed to load theory "Virtual_Substitution.Infinitesimals" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.LinearCase", "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.NegInfinityUni" (unresolved "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.InfinitesimalsUni" (unresolved "Virtual_Substitution.Infinitesimals", "Virtual_Substitution.NegInfinityUni", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.DNFUni" (unresolved "Virtual_Substitution.InfinitesimalsUni", "Virtual_Substitution.QE")
Failed to load theory "Virtual_Substitution.GeneralVSProofs" (unresolved "Virtual_Substitution.DNFUni", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.VSQuad" (unresolved "Virtual_Substitution.DNF", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.GeneralVSProofs", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.Reindex")
Failed to load theory "Virtual_Substitution.HeuristicProofs" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.VSQuad")
Failed to load theory "Virtual_Substitution.PrettyPrinting" (unresolved "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Exports" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.Optimizations", "Virtual_Substitution.PrettyPrinting", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.ExportProofs" (unresolved "Virtual_Substitution.Exports", "Virtual_Substitution.HeuristicProofs", "Virtual_Substitution.PrettyPrinting")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 249 of "~~/dirs/AFP/thys/Virtual_Substitution/QE.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 264 of "~~/dirs/AFP/thys/Virtual_Substitution/ExecutiblePolyProps.thy")
Failed to load theory "Weak_Spectroscopy.Expressiveness_Price" (unresolved "Weak_Spectroscopy.Energy")
Failed to load theory "Weak_Spectroscopy.Eta_Bisimilarity" (unresolved "Weak_Spectroscopy.Expressiveness_Price")
Failed to load theory "Weak_Spectroscopy.Branching_Bisimilarity" (unresolved "Weak_Spectroscopy.Eta_Bisimilarity")
Failed to load theory "Weak_Spectroscopy.Spectroscopy_Game" (unresolved "Weak_Spectroscopy.Energy")
Failed to load theory "Weak_Spectroscopy.Distinction_Implies_Winning_Budgets" (unresolved "Weak_Spectroscopy.Expressiveness_Price", "Weak_Spectroscopy.Spectroscopy_Game")
Failed to load theory "Weak_Spectroscopy.Strategy_Formulas" (unresolved "Weak_Spectroscopy.Expressiveness_Price", "Weak_Spectroscopy.Spectroscopy_Game")
Failed to load theory "Weak_Spectroscopy.Silent_Step_Spectroscopy" (unresolved "Weak_Spectroscopy.Distinction_Implies_Winning_Budgets", "Weak_Spectroscopy.Strategy_Formulas")
Failed to load theory "Weak_Spectroscopy.Weak_Traces" (unresolved "Weak_Spectroscopy.Expressiveness_Price")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 49 of "~~/dirs/AFP/thys/Weak_Spectroscopy/Energy.thy")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 406 of "~~/dirs/AFP/thys/Weight_Balanced_Trees/Weight_Balanced_Trees.thy")
Failed to load theory "Worklist_Algorithms.Liveness_Subsumption" (unresolved "Worklist_Algorithms.Worklist_Algorithms_Subsumption_Graphs")
Failed to load theory "Worklist_Algorithms.Liveness_Subsumption_Map" (unresolved "Worklist_Algorithms.Liveness_Subsumption")
Failed to load theory "Worklist_Algorithms.Unified_PW" (unresolved "Worklist_Algorithms.Worklist_Algorithms_Subsumption_Graphs")
Failed to load theory "Worklist_Algorithms.Leadsto" (unresolved "Worklist_Algorithms.Liveness_Subsumption", "Worklist_Algorithms.Unified_PW")
Failed to load theory "Worklist_Algorithms.Worklist_Subsumption_Multiset" (unresolved "Worklist_Algorithms.Unified_PW")
Failed to load theory "Worklist_Algorithms.Worklist_Subsumption1" (unresolved "Worklist_Algorithms.Worklist_Subsumption_Multiset")
Failed to load theory "Worklist_Algorithms.Worklist_Subsumption_Impl1" (unresolved "Worklist_Algorithms.Worklist_Subsumption1")
Failed to load theory "Worklist_Algorithms.Liveness_Subsumption_Impl" (unresolved "Worklist_Algorithms.Liveness_Subsumption_Map")
Failed to load theory "Worklist_Algorithms.Unified_PW_Hashing" (unresolved "Worklist_Algorithms.Unified_PW")
Failed to load theory "Worklist_Algorithms.Leadsto_Map" (unresolved "Worklist_Algorithms.Leadsto", "Worklist_Algorithms.Liveness_Subsumption_Map", "Worklist_Algorithms.Unified_PW_Hashing")
Failed to load theory "Worklist_Algorithms.Unified_PW_Impl" (unresolved "Worklist_Algorithms.Unified_PW_Hashing")
Failed to load theory "Worklist_Algorithms.Leadsto_Impl" (unresolved "Worklist_Algorithms.Leadsto_Map", "Worklist_Algorithms.Liveness_Subsumption_Impl", "Worklist_Algorithms.Unified_PW_Impl")
Solver z3: Solver terminated abnormally with error code 127 At command "by" (line 303 of "~~/dirs/AFP/thys/Worklist_Algorithms/Worklist_Algorithms_Subsumption_Graphs.thy")
Timeout
Timeout
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2709601297191300396: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script14926494786981360330: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script4717765477935420625: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script11974281763836447925: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7291020129947628656: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script18337137811563069205: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script1333493124745189691: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script18092739115752671477: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script15778772525124327976: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16628289632059395756: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6417772405053233691: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8025035704704206658: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script18052240031742560461: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8701815534661077636: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6616158041272736710: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6796492998447524447: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13804986850996919806: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7113863987854411622: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13094478900641742114: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script5334197354717768027: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7491543642179116284: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7012950747939401802: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script3316399750669825166: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6297287224245888400: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13677150408978375276: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9346521860560004688: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12386650190718990198: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16328967727449372448: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8710406145498539419: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2508618659400797891: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
exception Match raised (line 389 of "term.ML") At command "interpret" (line 496 of "~~/src/HOL/Algebra/Algebraic_Closure_Type.thy")
Tactic failed
The error(s) above occurred for the goal statement (line 220 of "~~/src/HOL/Bali/Term.thy"):
⋀x f1 f2 f3 f4 g1 g2 g3 g4.
⟦⋀z1. z1 ∈ BNF_Composition.id_bnf (λx. {}) x ⟹ f1 z1 = g1 z1;
⋀z2. z2 ∈ BNF_Composition.id_bnf Basic_BNFs.setl x ⟹ f2 z2 = g2 z2;
⋀z3. z3 ∈ BNF_Composition.id_bnf
(λx. ⋃x∈Basic_BNFs.setr x.
⋃ (Basic_BNFs.fsts ` Basic_BNFs.fsts x) ∪
⋃ (Basic_BNFs.snds ` Basic_BNFs.snds x))
x ⟹
f3 z3 = g3 z3;
⋀z4. z4 ∈ BNF_Composition.id_bnf (λx. {}) x ⟹ f4 z4 = g4 z4⟧
⟹ compat_stmt.n2m_stmt.sum2.sum1.sum2.sum.map_raw_sum f1 f2 f3 f4 x =
compat_stmt.n2m_stmt.sum2.sum1.sum2.sum.map_raw_sum g1 g2 g3 g4 x
Tactic failed The error(s) above occurred for the goal statement (line 22 of "~~/src/HOL/Bali/State.thy"): obj_tag.alg_obj_tag (obj_tag.min_alg_obj_tag s) s
Session startup failed: standard_output terminated Assertion failed: (0), function RelocateAddress, file savestate.cpp, line 1065. /tmp/isabelle-isatest/bash_script9000750082971974857: line 1: 27362 Abort trap: 6 /Users/isatest/.isabelle/contrib/polyml-5.9.2-4/x86_64_32-darwin/poly -q --minheap 1500 --gcthreads 4 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/Users/isatest/.isabelle/build_history-mini1-monterey/heaps/polyml-5.9.2_x86_64_32-darwin/Pure\",\ \"/Users/isatest/.isabelle/build_history-mini1-monterey/heaps/polyml-5.9.2_x86_64_32-darwin/HOL\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_process_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\)\)\; Return code: 127 (COMMAND NOT FOUND)
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2642139396199481499: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8026747136194390402: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2256717445052439001: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8516258689367060464: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2055258239162784303: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script492549487721598586: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script5665513592759520266: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6982173037676426060: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13396528200129201798: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script1200038189636540125: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6747618611125523408: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script4258102644760740685: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9982905158929543356: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9324352623299733603: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script5905179648785629709: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10065837545248562114: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10531214042941620009: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12116594827210062675: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6120632355924425109: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9773765655697423146: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8349400755834099079: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script49390695774193027: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2687548974053868036: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script5289590062205747296: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6316437927993568861: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
Failed to load theory "HOL.Argo" (unresolved "HOL.HOL")
Failed to load theory "HOL.Ctr_Sugar" (unresolved "HOL.HOL")
Failed to load theory "HOL.Orderings" (unresolved "HOL.HOL")
Failed to load theory "HOL.SAT" (unresolved "HOL.Argo")
Failed to load theory "HOL.Groups" (unresolved "HOL.Orderings")
Failed to load theory "HOL.Lattices" (unresolved "HOL.Groups")
Failed to load theory "HOL.Boolean_Algebras" (unresolved "HOL.Lattices")
Failed to load theory "HOL.Set" (unresolved "HOL.Boolean_Algebras", "HOL.Lattices")
Failed to load theory "HOL.Fun" (unresolved "HOL.Set")
Failed to load theory "HOL.Typedef" (unresolved "HOL.Set")
Failed to load theory "HOL.Complete_Lattices" (unresolved "HOL.Fun")
Failed to load theory "HOL.Rings" (unresolved "HOL.Fun", "HOL.Groups", "HOL.Set")
Failed to load theory "HOL.Inductive" (unresolved "HOL.Complete_Lattices", "HOL.Ctr_Sugar")
Failed to load theory "HOL.Product_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")
Failed to load theory "HOL.Sum_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")
Failed to load theory "HOL.Nat" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Rings", "HOL.Typedef")
Failed to load theory "HOL.Complete_Partial_Order" (unresolved "HOL.Product_Type")
Failed to load theory "HOL.Fields" (unresolved "HOL.Nat")
Failed to load theory "HOL.Meson" (unresolved "HOL.Nat")
Failed to load theory "HOL.Relation" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Sum_Type")
Failed to load theory "HOL.Finite_Set" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Relation", "HOL.Sum_Type")
Failed to load theory "HOL.Transitive_Closure" (unresolved "HOL.Finite_Set")
Failed to load theory "HOL.Wellfounded" (unresolved "HOL.Transitive_Closure")
Failed to load theory "HOL.Fun_Def_Base" (unresolved "HOL.Ctr_Sugar", "HOL.Set", "HOL.Wellfounded")
Failed to load theory "HOL.Hilbert_Choice" (unresolved "HOL.Wellfounded")
Failed to load theory "HOL.Wfrec" (unresolved "HOL.Wellfounded")
Failed to load theory "HOL.ATP" (unresolved "HOL.Hilbert_Choice", "HOL.Meson")
Failed to load theory "HOL.Order_Relation" (unresolved "HOL.Wfrec")
Failed to load theory "HOL.BNF_Wellorder_Relation" (unresolved "HOL.Order_Relation")
Failed to load theory "HOL.Zorn" (unresolved "HOL.Hilbert_Choice", "HOL.Order_Relation")
Failed to load theory "HOL.Metis" (unresolved "HOL.ATP")
Failed to load theory "HOL.BNF_Wellorder_Embedding" (unresolved "HOL.BNF_Wellorder_Relation", "HOL.Hilbert_Choice")
Failed to load theory "HOL.BNF_Wellorder_Constructions" (unresolved "HOL.BNF_Wellorder_Embedding")
Failed to load theory "HOL.BNF_Cardinal_Order_Relation" (unresolved "HOL.BNF_Wellorder_Constructions", "HOL.Zorn")
Failed to load theory "HOL.BNF_Cardinal_Arithmetic" (unresolved "HOL.BNF_Cardinal_Order_Relation")
Failed to load theory "HOL.BNF_Def" (unresolved "HOL.BNF_Cardinal_Arithmetic", "HOL.Fun_Def_Base")
Failed to load theory "HOL.BNF_Composition" (unresolved "HOL.BNF_Def")
Failed to load theory "HOL.Basic_BNFs" (unresolved "HOL.BNF_Def")
Failed to load theory "HOL.BNF_Fixpoint_Base" (unresolved "HOL.BNF_Composition", "HOL.Basic_BNFs")
Failed to load theory "HOL.BNF_Least_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base")
Failed to load theory "HOL.Basic_BNF_LFPs" (unresolved "HOL.BNF_Least_Fixpoint")
Failed to load theory "HOL.Equiv_Relations" (unresolved "HOL.BNF_Least_Fixpoint")
Failed to load theory "HOL.Transfer" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Hilbert_Choice", "HOL.Metis")
Failed to load theory "HOL.Lifting" (unresolved "HOL.Equiv_Relations", "HOL.Transfer")
Failed to load theory "HOL.Num" (unresolved "HOL.BNF_Least_Fixpoint", "HOL.Transfer")
Failed to load theory "HOL.Power" (unresolved "HOL.Num")
Failed to load theory "HOL.Option" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Quotient" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Groups_Big" (unresolved "HOL.Equiv_Relations", "HOL.Power")
Failed to load theory "HOL.Lifting_Set" (unresolved "HOL.Groups_Big", "HOL.Lifting")
Failed to load theory "HOL.Extraction" (unresolved "HOL.Option")
Failed to load theory "HOL.Partial_Function" (unresolved "HOL.Complete_Partial_Order", "HOL.Option")
Failed to load theory "HOL.Lattices_Big" (unresolved "HOL.Groups_Big", "HOL.Option")
Failed to load theory "HOL.Fun_Def" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Partial_Function", "HOL.SAT")
Failed to load theory "HOL.Int" (unresolved "HOL.Fun_Def", "HOL.Groups_Big", "HOL.Quotient")
Failed to load theory "HOL.Euclidean_Rings" (unresolved "HOL.Int", "HOL.Lattices_Big")
Failed to load theory "HOL.Parity" (unresolved "HOL.Euclidean_Rings")
Failed to load theory "HOL.Numeral_Simprocs" (unresolved "HOL.Parity")
Failed to load theory "HOL.Set_Interval" (unresolved "HOL.Parity")
Failed to load theory "HOL.SMT" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Semiring_Normalization" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Groebner_Basis" (unresolved "HOL.Parity", "HOL.Semiring_Normalization")
Failed to load theory "HOL.Conditionally_Complete_Lattices" (unresolved "HOL.Finite_Set", "HOL.Lattices_Big", "HOL.Set_Interval")
Failed to load theory "HOL.Filter" (unresolved "HOL.Lifting_Set", "HOL.Set_Interval")
Failed to load theory "HOL.Presburger" (unresolved "HOL.Groebner_Basis", "HOL.Set_Interval")
Failed to load theory "HOL.Try0_HOL" (unresolved "HOL.Presburger")
Failed to load theory "HOL.Sledgehammer" (unresolved "HOL.Presburger", "HOL.SMT", "HOL.Try0_HOL")
Failed to load theory "HOL.List" (unresolved "HOL.Lifting_Set", "HOL.Sledgehammer")
Failed to load theory "HOL.Groups_List" (unresolved "HOL.List")
Failed to load theory "HOL.Bit_Operations" (unresolved "HOL.Groups_List", "HOL.Presburger")
Failed to load theory "HOL.Factorial" (unresolved "HOL.Groups_List")
Failed to load theory "HOL.Map" (unresolved "HOL.List")
Failed to load theory "HOL.Binomial" (unresolved "HOL.Factorial", "HOL.Presburger")
Failed to load theory "HOL.Code_Numeral" (unresolved "HOL.Bit_Operations", "HOL.Lifting")
Failed to load theory "HOL.Enum" (unresolved "HOL.Groups_List", "HOL.Map")
Failed to load theory "HOL.GCD" (unresolved "HOL.Code_Numeral", "HOL.Groups_List")
Failed to load theory "HOL.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")
Failed to load theory "HOL.String" (unresolved "HOL.Bit_Operations", "HOL.Code_Numeral", "HOL.Enum")
Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base", "HOL.String")
Failed to load theory "HOL.Predicate" (unresolved "HOL.String")
Failed to load theory "HOL.Typerep" (unresolved "HOL.String")
Failed to load theory "HOL.Lazy_Sequence" (unresolved "HOL.Predicate")
Failed to load theory "HOL.Limited_Sequence" (unresolved "HOL.Lazy_Sequence")
Failed to load theory "HOL.Code_Evaluation" (unresolved "HOL.Limited_Sequence", "HOL.Typerep")
Failed to load theory "HOL.Quickcheck_Random" (unresolved "HOL.Code_Evaluation", "HOL.Enum", "HOL.Random")
Failed to load theory "HOL.Quickcheck_Exhaustive" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Quickcheck_Narrowing" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Random_Pred" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Record" (unresolved "HOL.Quickcheck_Exhaustive")
Failed to load theory "HOL.Random_Sequence" (unresolved "HOL.Random_Pred")
Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")
Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")
Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")
Failed to load theory "HOL.Mirabelle" (unresolved "HOL.Predicate_Compile", "HOL.Presburger", "HOL.Sledgehammer")
Failed to load theory "Main" (unresolved "HOL.BNF_Greatest_Fixpoint", "HOL.Binomial", "HOL.Conditionally_Complete_Lattices", "HOL.Extraction", "HOL.Filter", "HOL.GCD", "HOL.Mirabelle", "HOL.Nunchaku", "HOL.Predicate_Compile", "HOL.Quickcheck_Narrowing")
Failed to load theory "HOL.Archimedean_Field" (unresolved "Main")
Failed to load theory "HOL.Hull" (unresolved "Main")
Failed to load theory "HOL.Rat" (unresolved "HOL.Archimedean_Field")
Failed to load theory "HOL.Topological_Spaces" (unresolved "Main")
Failed to load theory "HOL.Modules" (unresolved "HOL.Hull")
Failed to load theory "HOL.Real" (unresolved "HOL.Rat")
Failed to load theory "HOL.Vector_Spaces" (unresolved "HOL.Modules")
Failed to load theory "HOL.Binomial_Plus" (unresolved "HOL.Real")
Failed to load theory "HOL.Real_Vector_Spaces" (unresolved "HOL.Real", "HOL.Topological_Spaces", "HOL.Vector_Spaces")
Failed to load theory "HOL.Inequalities" (unresolved "HOL.Real_Vector_Spaces")
Failed to load theory "HOL.Limits" (unresolved "HOL.Real_Vector_Spaces")
Failed to load theory "HOL.Deriv" (unresolved "HOL.Limits")
Failed to load theory "HOL.Series" (unresolved "HOL.Inequalities", "HOL.Limits")
Failed to load theory "HOL.NthRoot" (unresolved "HOL.Deriv")
Failed to load theory "HOL.Transcendental" (unresolved "HOL.Deriv", "HOL.NthRoot", "HOL.Series")
Failed to load theory "HOL.Complex" (unresolved "HOL.Real_Vector_Spaces", "HOL.Transcendental")
Failed to load theory "HOL.MacLaurin" (unresolved "HOL.Transcendental")
Failed to load theory "Complex_Main" (unresolved "HOL.Binomial_Plus", "HOL.Complex", "HOL.MacLaurin")
Cheating requires interactive or quick_and_dirty mode! At command "ML_file" (line 797 of "~~/src/HOL/HOL.thy")
Cheating requires interactive or quick_and_dirty mode! At command "by" (line 16 of "~~/src/Pure/ex/Guess_Examples.thy")
Failed to load theory "ZF.IntDiv" (unresolved "ZF.Bin")
Failed to load theory "ZF" (unresolved "ZF.IntDiv")
Failed to load theory "ZF.AC" (unresolved "ZF")
Failed to load theory "ZF.Zorn" (unresolved "ZF.AC")
Failed to load theory "ZF.Cardinal_AC" (unresolved "ZF.Zorn")
Failed to load theory "ZF.InfDatatype" (unresolved "ZF.Cardinal_AC")
Failed to load theory "ZFC" (unresolved "ZF", "ZF.InfDatatype")
Cheating requires interactive or quick_and_dirty mode! At command "ML_file" (line 706 of "~~/src/ZF/Bin.thy")