Isabelle2023
exitCode=0
Started at Mon Oct 5 14:50:05 GMT 2026 (polyml-for-isabelle-2023_x86_64-linux on repl)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64-linux"
ML_HOME="/nix/store/zyg046jz3ci3cmnvl63qw0akfg5nk115-polyml-for-isabelle-2023/bin"
ML_SYSTEM="polyml-for-isabelle-2023"
ML_OPTIONS="--minheap 1000"

Session Pure/Pure
Session Misc/Tools
Session HOL/HOL (main)
Session Unsorted/HunterProofNetwork
Running HunterProofNetwork ...
HunterProofNetwork: theory HunterProofNetwork.ProofNetwork
Timing HunterProofNetwork (4 threads, 52.382s elapsed time, 82.461s cpu time, 9.293s GC time, factor 1.57)
Finished HunterProofNetwork (0:01:01 elapsed time, 0:01:26 cpu time, factor 1.39)

Finished at Mon Oct 5 14:51:17 GMT 2026
0:01:12 elapsed time, 0:01:26 cpu time, factor 1.19


Theory "HunterProofNetwork.ProofNetwork" (in HunterProofNetwork):

Output (line 32 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"

Output (line 49 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size <*mlex*> {}"

Output (line 54 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size <*mlex*> {}"

Output (line 61 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size <*mlex*> {}"

Output (line 68 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"

Output (line 73 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"

Output (line 78 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size <*mlex*> {}"

Output (line 83 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size_list (nat \<circ> abs) <*mlex*> {}"

Output (line 96 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "{}"

Output (line 99 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "length <*mlex*> {}"

Output (line 126 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "length <*mlex*> {}"

Output (line 141 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
Found termination order: "size <*mlex*> {}"

Output (line 6507 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
PROOF_NETWORK_WITNESSES=536 ORACLES=0 TYPE_ALIAS_IDENTITY=checked

Output (line 6507 of "~/workspace/formal/proof-network/translation-candidates/e00c185288bb53bef0cf9ec6/ProofNetwork.thy"):
val witnesses =
   ["bor (bnot
           (band
             (band (band ?v0.0 (beq ?v0.0 ?v1.0)) (bor (bnot ?v1.0) ?v2.0))
             (bor (bnot ?v2.0) ?v0.0)))
      (band (band ?v0.0 ?v1.0) ?v2.0) =
     True",
    "bor (bnot (beq ?v0.0 ?v1.0)) (beq ?v0.0 ?v1.0) = True",
    "bor (bnot (band (band ?v0.0 (bor (bnot ?v0.0) ?v1.0)) ?v1.0))
      (band ?v0.0 ?v1.0) =
     True",
    "?a = ?a",
    "bor (bnot
           (band
             (band (band (... ... ...) (... ... ...)) (bor (... ...) ?v4.0))
             (bor (bnot ?v4.0) ?v5.0)))
      (band (band (band (band ?v0.0 ?v1.0) (band ?v2.0 ?v3.0)) ?v4.0)
        ?v5.0) =
     True",
    "bor (bnot
           (band (band (band (...) (...)) (bor (...) ?v4.0))
             (bor (bnot ?v4.0) ?v5.0)))
      (band (band (band (band ?v0.0 ?v1.0) (band ?v2.0 ?v3.0)) ?v4.0)
        ?v5.0) =
     True",
    "bor (bnot
           (band (band (... ... ...) (... ... ...)) (bor (... ...) ?v5.0)))
      (band (band (band (... ... ...) (... ... ...)) ?v4.0) ?v5.0) =
     True",
    "?a = ?a",
    "bor (bnot (band (... ... ...) ?v3.0))
      (bor (bnot (... ... ...)) (bor (... ...) ?v3.0)) =
     True",
    "bor (bnot (band ?v0.0 (...))) ?v0.0 = True", "?a = ?a",
    "bor (bnot (...)) ?v3.0 = True", "bor (... ...) (... ... ...) = True",
    "bor (...) (...) = True", "... ... ... ... True", "... ... ...", "...",
    "...", "...", ..., ...]:
   thm list