%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI006^5 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:20:14 AM UTC 2026
% Result : ContradictoryAxioms 35.50s 11.33s
% Output : Refutation 35.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI006^5 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.25 % Computer : n003.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Tue Sep 29 13:21:28 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.81 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.36/1.05 % [INFO] Parsing done (238ms).
% 1.36/1.06 % [INFO] Running in sequential loop mode.
% 1.99/1.45 % [INFO] eprover registered as external prover.
% 1.99/1.46 % [INFO] Scanning for conjecture ...
% 2.39/1.60 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.39/1.63 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.39/1.63 % [INFO] Problem is higher-order (TPTP THF).
% 2.39/1.64 % [INFO] Type checking passed.
% 2.39/1.64 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 35.50/11.33 % [INFO] Killing All external provers ...
% 35.50/11.33 % Time passed: 10946ms (effective reasoning time: 10257ms)
% 35.50/11.33 % Axioms used in derivation (3): axA5, axA2, axA1a
% 35.50/11.33 % No. of inferences in proof: 27
% 35.50/11.33 % SZS status ContradictoryAxioms for /export/starexec/sandbox/benchmark/theBenchmark.p : 10946 ms resp. 10257 ms w/o parsing
% 35.50/11.37 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.50/11.37 thf(mu_type, type, mu: $tType).
% 35.50/11.37 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 35.50/11.37 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 35.50/11.37 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 35.50/11.37 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 35.50/11.37 thf(mforall_indset_decl, type, mforall_indset: (((mu > ($i > $o)) > ($i > $o)) > ($i > $o))).
% 35.50/11.37 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 35.50/11.37 thf(mbox_decl, type, mbox: (($i > $o) > ($i > $o))).
% 35.50/11.37 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 35.50/11.37 thf(positive_decl, type, positive: ((mu > ($i > $o)) > ($i > $o))).
% 35.50/11.37 thf(essence_decl, type, essence: ((mu > ($i > $o)) > (mu > ($i > $o)))).
% 35.50/11.37 thf(necessary_existence_decl, type, necessary_existence: (mu > ($i > $o))).
% 35.50/11.37 thf(sk1_decl, type, sk1: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > $i)))).
% 35.50/11.37 thf(sk2_decl, type, sk2: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > mu)))).
% 35.50/11.37 thf(sk9_decl, type, sk9: mu).
% 35.50/11.37 thf(sk10_decl, type, sk10: $i).
% 35.50/11.37 thf(sk11_decl, type, sk11: ((mu > ($i > $o)) > (mu > ($i > $o)))).
% 35.50/11.37 thf(sk12_decl, type, sk12: ((mu > ($i > $o)) > $i)).
% 35.50/11.37 thf(sk13_decl, type, sk13: ((mu > ($i > $o)) > mu)).
% 35.50/11.37 thf(sk14_decl, type, sk14: ($i > ((mu > ($i > $o)) > mu))).
% 35.50/11.37 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 35.50/11.37 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) & (B @ C))) ).
% 35.50/11.37 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) => (B @ C))) ).
% 35.50/11.37 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 35.50/11.37 thf(mforall_indset_def, definition, mforall_indset = (^ [A:((mu > ($i > $o)) > ($i > $o)),B:$i]: ! [C:(mu > ($i > $o))]: (A @ C @ B)) ).
% 35.50/11.37 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o)),B:$i]: ? [C:mu]: (A @ C @ B)) ).
% 35.50/11.37 thf(mbox_def, definition, mbox = (^ [A:($i > $o),B:$i]: ! [C:$i]: (A @ C)) ).
% 35.50/11.37 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 35.50/11.37 thf(essence_def, definition, essence = (^ [A:(mu > ($i > $o)),B:mu]: (mforall_indset @ (^ [C:(mu > ($i > $o))]: (mimplies @ (C @ B) @ (mbox @ (mforall_ind @ (^ [D:mu]: (mimplies @ (A @ D) @ (C @ D))))))))) ).
% 35.50/11.37 thf(necessary_existence_def, definition, necessary_existence = (^ [A:mu]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (essence @ B @ A) @ (mbox @ (mexists_ind @ B)))))) ).
% 35.50/11.37 thf(sk1_def, definition, sk1 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:$i]: ~ (! [E:mu]: ((B @ E @ D) => (A @ E @ D))))) ).
% 35.50/11.37 thf(sk2_def, definition, sk2 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:mu]: ~ ((B @ D @ (sk1 @ A @ B @ C)) => (A @ D @ (sk1 @ A @ B @ C))))) ).
% 35.50/11.37 thf(sk11_def, definition, sk11 = (^ [A:(mu > ($i > $o))]: (@+ [B:(mu > ($i > $o))]: ~ ((B @ sk9 @ sk10) => (! [C:$i,D:mu]: ((A @ D @ C) => (B @ D @ C)))))) ).
% 35.50/11.37 thf(sk12_def, definition, sk12 = (^ [A:(mu > ($i > $o))]: (@+ [B:$i]: ~ (! [C:mu]: ((A @ C @ B) => (sk11 @ A @ C @ B))))) ).
% 35.50/11.37 thf(sk13_def, definition, sk13 = (^ [A:(mu > ($i > $o))]: (@+ [B:mu]: ~ ((A @ B @ (sk12 @ A)) => (sk11 @ A @ B @ (sk12 @ A))))) ).
% 35.50/11.37 thf(sk14_def, definition, sk14 = (^ [A:$i,B:(mu > ($i > $o))]: (@+ [C:mu]: (B @ C @ A))) ).
% 35.50/11.37 thf(6,axiom,((mvalid @ (positive @ necessary_existence))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA5)).
% 35.50/11.37 thf(16,plain,((! [A:$i]: (positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i,G:mu]: ((D @ G @ F) => (E @ G @ F))))) => (! [E:$i]: ? [F:mu]: (D @ F @ E)))) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 35.50/11.37 thf(17,plain,(! [A:$i] : ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i,G:mu]: ((D @ G @ F) => (E @ G @ F))))) => (! [E:$i]: ? [F:mu]: (D @ F @ E)))) @ A))),inference(cnf,[status(esa)],[16])).
% 35.50/11.37 thf(5,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (mand @ (positive @ A) @ (mbox @ (mforall_ind @ (^ [C:mu]: (mimplies @ (A @ C) @ (B @ C)))))) @ (positive @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA2)).
% 35.50/11.37 thf(12,plain,((! [A:$i,B:(mu > ($i > $o)),C:(mu > ($i > $o))]: (((positive @ (B) @ A) & ! [D:$i,E:mu]: ((B @ E @ D) => (C @ E @ D))) => (positive @ (C) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 35.50/11.37 thf(13,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : (((~ (positive @ (B) @ A) | (B @ (sk2 @ (C) @ (B) @ A) @ (sk1 @ (C) @ (B) @ A)) | (positive @ (C) @ A)) & (~ (positive @ (B) @ A) | ~ (C @ (sk2 @ (C) @ (B) @ A) @ (sk1 @ (C) @ (B) @ A)) | (positive @ (C) @ A))))),inference(cnf,[status(esa)],[12])).
% 35.50/11.37 thf(14,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (B @ (sk2 @ (C) @ (B) @ A) @ (sk1 @ (C) @ (B) @ A)) | (positive @ (C) @ A))),inference(cnfConj,[status(thm)],[13])).
% 35.50/11.37 thf(98,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [C:mu,D:$i]: (($false))) @ A)) | ($false) | (positive @ (B) @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(A)),bind(B, $thf(^ [D:mu,E:$i]: (($false))))]])).
% 35.50/11.37 thf(112,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [C:mu,D:$i]: (($false))) @ A)) | (positive @ (B) @ A))),inference(simp,[status(thm)],[98])).
% 35.50/11.37 thf(3,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mimplies @ (positive @ (^ [B:mu]: (mnot @ (A @ B)))) @ (mnot @ (positive @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA1a)).
% 35.50/11.37 thf(8,plain,((! [A:$i,B:(mu > ($i > $o))]: ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) => (~ (positive @ (B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 35.50/11.37 thf(9,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A)) | (~ (positive @ (B) @ A)))),inference(cnf,[status(esa)],[8])).
% 35.50/11.37 thf(20,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)) | ~ (($true)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G)))) @ A) != (positive @ (C) @ B)))),inference(paramod_ordered,[status(thm)],[17,9])).
% 35.50/11.37 thf(21,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G)))) @ A) != (positive @ (C) @ B)))),inference(simp,[status(thm)],[20])).
% 35.50/11.37 thf(22,plain,(! [A:$i] : ((~ (positive @ (^ [B:mu,C:$i]: ~ (! [D:(mu > ($i > $o))]: ((! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i,G:mu]: ((D @ G @ F) => (E @ G @ F))))) => (! [E:$i]: ? [F:mu]: (D @ F @ E))))) @ A)))),inference(pattern_uni,[status(thm)],[21:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G)))))]])).
% 35.50/11.37 thf(159,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [D:mu,E:$i]: (($false))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G))))) @ C)))),inference(paramod_ordered,[status(thm)],[112,22])).
% 35.50/11.37 thf(160,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [D:mu,E:$i]: (($false))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G))))) @ C)))),inference(simp,[status(thm)],[159])).
% 35.50/11.37 thf(161,plain,(! [A:$i] : ((~ (positive @ (^ [B:mu,C:$i]: (($false))) @ A)))),inference(pattern_uni,[status(thm)],[160:[bind(A, $thf(A)),bind(B, $thf(^ [D:mu,E:$i]: ~ (! [F:(mu > ($i > $o))]: ((! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i,I:mu]: ((F @ I @ H) => (G @ I @ H))))) => (! [G:$i]: ? [H:mu]: (F @ H @ G)))))),bind(C, $thf(A))]])).
% 35.50/11.37 thf(181,plain,(! [B:$i,A:$i] : (~ (($true)) | ((positive @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i,H:mu]: ((E @ H @ G) => (F @ H @ G))))) => (! [F:$i]: ? [G:mu]: (E @ G @ F)))) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ B)))),inference(paramod_ordered,[status(thm)],[17,161])).
% 35.50/11.37 thf(182,plain,(! [B:$i,A:$i] : (((positive @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i,H:mu]: ((E @ H @ G) => (F @ H @ G))))) => (! [F:$i]: ? [G:mu]: (E @ G @ F)))) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ B)))),inference(simp,[status(thm)],[181])).
% 35.50/11.37 thf(186,plain,(! [B:$i,A:$i] : (((^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i,H:mu]: ((E @ H @ G) => (F @ H @ G))))) => (! [F:$i]: ? [G:mu]: (E @ G @ F)))) != (^ [C:mu,D:$i]: (($false)))) | (A != B))),inference(simp,[status(thm)],[182])).
% 35.50/11.37 thf(190,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((! [D:(mu > ($i > $o))]: ((D @ A @ B) => (! [E:$i,F:mu]: ((C @ F @ E) => (D @ F @ E))))) => (! [D:$i]: ? [E:mu]: (C @ E @ D)))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[186])).
% 35.50/11.37 thf(236,plain,((! [A:(mu > ($i > $o))]: ((! [B:(mu > ($i > $o))]: ((B @ sk9 @ sk10) => (! [C:$i,D:mu]: ((A @ D @ C) => (B @ D @ C))))) => (! [B:$i]: ? [C:mu]: (A @ C @ B))))),inference(func_ext,[status(esa)],[190])).
% 35.50/11.37 thf(237,plain,(! [B:$i,A:(mu > ($i > $o))] : ((((sk11 @ (A) @ sk9 @ sk10) | (A @ (sk14 @ B @ (A)) @ B)) & ((A @ (sk13 @ (A)) @ (sk12 @ (A))) | (A @ (sk14 @ B @ (A)) @ B)) & (~ (sk11 @ (A) @ (sk13 @ (A)) @ (sk12 @ (A))) | (A @ (sk14 @ B @ (A)) @ B))))),inference(cnf,[status(esa)],[236])).
% 35.50/11.37 thf(239,plain,(! [B:$i,A:(mu > ($i > $o))] : ((A @ (sk13 @ (A)) @ (sk12 @ (A))) | (A @ (sk14 @ B @ (A)) @ B))),inference(cnfConj,[status(thm)],[237])).
% 35.50/11.37 thf(1101,plain,(($false) | ($false)),inference(prim_subst,[status(thm)],[239:[bind(A, $thf(^ [C:mu,D:$i]: (($false))))]])).
% 35.50/11.37 thf(1136,plain,(($false)),inference(simp,[status(thm)],[1101])).
% 35.50/11.37 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.50/11.37 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------