%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI006^4 : 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 : n008.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 109.89s 37.62s
% Output : Refutation 109.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI006^4 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.07 % 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.15/0.26 % Computer : n008.cluster.edu
% 0.15/0.26 % Model : x86_64 x86_64
% 0.15/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.26 % Memory : 8046.5625MB
% 0.15/0.26 % OS : Linux 6.8.0-71-generic
% 0.15/0.26 % CPULimit : 300
% 0.15/0.26 % WCLimit : 300
% 0.15/0.26 % DateTime : Tue Sep 29 13:20:18 UTC 2026
% 0.15/0.27 % CPUTime :
% 0.15/0.27 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.93/0.85 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.36/1.11 % [INFO] Parsing done (254ms).
% 1.36/1.13 % [INFO] Running in sequential loop mode.
% 2.38/1.52 % [INFO] eprover registered as external prover.
% 2.38/1.53 % [INFO] Scanning for conjecture ...
% 2.56/1.69 % [INFO] Found a conjecture (or negated_conjecture) and 6 axioms. Running axiom selection ...
% 2.78/1.72 % [INFO] Axiom selection finished. Selected 6 axioms (removed 0 axioms).
% 2.78/1.73 % [INFO] Problem is higher-order (TPTP THF).
% 2.78/1.73 % [INFO] Type checking passed.
% 2.78/1.74 % [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 ...
% 109.89/37.62 % [INFO] Killing All external provers ...
% 109.89/37.62 % Time passed: 37218ms (effective reasoning time: 36489ms)
% 109.89/37.62 % Axioms used in derivation (4): axA4, axA1a, axA5, axA2
% 109.89/37.62 % No. of inferences in proof: 26
% 109.89/37.62 % SZS status ContradictoryAxioms for /export/starexec/sandbox/benchmark/theBenchmark.p : 37218 ms resp. 36489 ms w/o parsing
% 109.89/37.66 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 109.89/37.66 thf(mu_type, type, mu: $tType).
% 109.89/37.66 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 109.89/37.66 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 109.89/37.66 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 109.89/37.66 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 109.89/37.66 thf(mforall_indset_decl, type, mforall_indset: (((mu > ($i > $o)) > ($i > $o)) > ($i > $o))).
% 109.89/37.66 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 109.89/37.66 thf(mbox_decl, type, mbox: (($i > $o) > ($i > $o))).
% 109.89/37.66 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 109.89/37.66 thf(positive_decl, type, positive: ((mu > ($i > $o)) > ($i > $o))).
% 109.89/37.66 thf(essence_decl, type, essence: ((mu > ($i > $o)) > (mu > ($i > $o)))).
% 109.89/37.66 thf(necessary_existence_decl, type, necessary_existence: (mu > ($i > $o))).
% 109.89/37.66 thf(sk1_decl, type, sk1: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > $i)))).
% 109.89/37.66 thf(sk2_decl, type, sk2: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > mu)))).
% 109.89/37.66 thf(sk5_decl, type, sk5: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > (mu > ($i > $o)))))).
% 109.89/37.66 thf(sk6_decl, type, sk6: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > $i)))).
% 109.89/37.66 thf(sk7_decl, type, sk7: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > mu)))).
% 109.89/37.66 thf(sk8_decl, type, sk8: ($i > ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > mu))))).
% 109.89/37.66 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 109.89/37.66 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) & (B @ C))) ).
% 109.89/37.66 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) => (B @ C))) ).
% 109.89/37.66 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 109.89/37.66 thf(mforall_indset_def, definition, mforall_indset = (^ [A:((mu > ($i > $o)) > ($i > $o)),B:$i]: ! [C:(mu > ($i > $o))]: (A @ C @ B)) ).
% 109.89/37.66 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o)),B:$i]: ? [C:mu]: (A @ C @ B)) ).
% 109.89/37.66 thf(mbox_def, definition, mbox = (^ [A:($i > $o),B:$i]: ! [C:$i]: (A @ C)) ).
% 109.89/37.66 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 109.89/37.66 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))))))))) ).
% 109.89/37.66 thf(necessary_existence_def, definition, necessary_existence = (^ [A:mu]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (essence @ B @ A) @ (mbox @ (mexists_ind @ B)))))) ).
% 109.89/37.66 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))))) ).
% 109.89/37.66 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))))) ).
% 109.89/37.66 thf(sk5_def, definition, sk5 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:(mu > ($i > $o))]: ~ ((D @ (sk2 @ B @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ C) @ (sk1 @ B @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ C)) => (! [E:$i,F:mu]: ((A @ F @ E) => (D @ F @ E)))))) ).
% 109.89/37.66 thf(sk6_def, definition, sk6 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:$i]: ~ (! [E:mu]: ((A @ E @ D) => (sk5 @ A @ B @ C @ E @ D))))) ).
% 109.89/37.66 thf(sk7_def, definition, sk7 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:mu]: ~ ((A @ D @ (sk6 @ A @ B @ C)) => (sk5 @ A @ B @ C @ D @ (sk6 @ A @ B @ C))))) ).
% 109.89/37.66 thf(sk8_def, definition, sk8 = (^ [A:$i,B:(mu > ($i > $o)),C:(mu > ($i > $o)),D:$i]: (@+ [E:mu]: (B @ E @ A))) ).
% 109.89/37.66 thf(7,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mimplies @ (positive @ A) @ (mbox @ (positive @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA4)).
% 109.89/37.66 thf(20,plain,((! [A:$i,B:(mu > ($i > $o))]: ((positive @ (B) @ A) => (! [C:$i]: (positive @ (B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 109.89/37.66 thf(21,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (positive @ (B) @ C))),inference(cnf,[status(esa)],[20])).
% 109.89/37.66 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)).
% 109.89/37.66 thf(10,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])).
% 109.89/37.66 thf(11,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A)) | (~ (positive @ (B) @ A)))),inference(cnf,[status(esa)],[10])).
% 109.89/37.66 thf(44,plain,(! [E:(mu > ($i > $o)),D:$i,C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (~ (positive @ (^ [F:mu,G:$i]: ~ (E @ F @ G)) @ D)) | ~ (($true)) | ((positive @ (B) @ C) != (positive @ (E) @ D)))),inference(paramod_ordered,[status(thm)],[21,11])).
% 109.89/37.66 thf(45,plain,(! [E:(mu > ($i > $o)),D:$i,C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (~ (positive @ (^ [F:mu,G:$i]: ~ (E @ F @ G)) @ D)) | ((positive @ (B) @ C) != (positive @ (E) @ D)))),inference(simp,[status(thm)],[44])).
% 109.89/37.66 thf(46,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (~ (positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ C)))),inference(pattern_uni,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C)),bind(E, $thf(B))]])).
% 109.89/37.66 thf(8,axiom,((mvalid @ (positive @ necessary_existence))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA5)).
% 109.89/37.66 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(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 109.89/37.66 thf(23,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)],[22])).
% 109.89/37.66 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)).
% 109.89/37.66 thf(14,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])).
% 109.89/37.66 thf(15,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)],[14])).
% 109.89/37.66 thf(16,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)],[15])).
% 109.89/37.66 thf(197,plain,(! [D:(mu > ($i > $o)),C:(mu > ($i > $o)),B:$i,A:$i] : (~ (($true)) | (C @ (sk2 @ (D) @ (C) @ B) @ (sk1 @ (D) @ (C) @ B)) | (positive @ (D) @ B) | ((positive @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A) != (positive @ (C) @ B)))),inference(paramod_ordered,[status(thm)],[23,16])).
% 109.89/37.66 thf(198,plain,(! [D:(mu > ($i > $o)),C:(mu > ($i > $o)),B:$i,A:$i] : ((C @ (sk2 @ (D) @ (C) @ B) @ (sk1 @ (D) @ (C) @ B)) | (positive @ (D) @ B) | ((positive @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A) != (positive @ (C) @ B)))),inference(simp,[status(thm)],[197])).
% 109.89/37.66 thf(199,plain,(! [B:(mu > ($i > $o)),A:$i] : ((! [C:(mu > ($i > $o))]: ((! [D:(mu > ($i > $o))]: ((D @ (sk2 @ (B) @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A) @ (sk1 @ (B) @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A)) => (! [E:$i,F:mu]: ((C @ F @ E) => (D @ F @ E))))) => (! [D:$i]: ? [E:mu]: (C @ E @ D)))) | (positive @ (B) @ A))),inference(pattern_uni,[status(thm)],[198:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H))))),bind(D, $thf(D))]])).
% 109.89/37.66 thf(219,plain,(! [D:$i,C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((((sk5 @ (C) @ (B) @ A @ (sk2 @ (B) @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A) @ (sk1 @ (B) @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((! [H:(mu > ($i > $o))]: ((H @ E @ F) => (! [I:$i,J:mu]: ((G @ J @ I) => (H @ J @ I))))) => (! [H:$i]: ? [I:mu]: (G @ I @ H)))) @ A)) | (C @ (sk8 @ D @ (C) @ (B) @ A) @ D) | (positive @ (B) @ A)) & ((C @ (sk7 @ (C) @ (B) @ A) @ (sk6 @ (C) @ (B) @ A)) | (C @ (sk8 @ D @ (C) @ (B) @ A) @ D) | (positive @ (B) @ A)) & (~ (sk5 @ (C) @ (B) @ A @ (sk7 @ (C) @ (B) @ A) @ (sk6 @ (C) @ (B) @ A)) | (C @ (sk8 @ D @ (C) @ (B) @ A) @ D) | (positive @ (B) @ A))))),inference(cnf,[status(esa)],[199])).
% 109.89/37.66 thf(221,plain,(! [D:$i,C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((C @ (sk7 @ (C) @ (B) @ A) @ (sk6 @ (C) @ (B) @ A)) | (C @ (sk8 @ D @ (C) @ (B) @ A) @ D) | (positive @ (B) @ A))),inference(cnfConj,[status(thm)],[219])).
% 109.89/37.66 thf(224,plain,(! [D:$i,C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((C @ (sk7 @ (C) @ (B) @ A) @ (sk6 @ (C) @ (B) @ A)) | (C @ (sk8 @ D @ (C) @ (B) @ A) @ D) | (positive @ (B) @ A))),inference(simp,[status(thm)],[221])).
% 109.89/37.66 thf(6835,plain,(! [B:(mu > ($i > $o)),A:$i] : (($false) | ($false) | (positive @ (B) @ A))),inference(prim_subst,[status(thm)],[224:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [E:mu,F:$i]: (($false))))]])).
% 109.89/37.66 thf(6913,plain,(! [B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A))),inference(simp,[status(thm)],[6835])).
% 109.89/37.66 thf(7308,plain,(~ (($true)) | ~ (($true))),inference(rewrite,[status(thm)],[46,6913])).
% 109.89/37.66 thf(7309,plain,(($false)),inference(simp,[status(thm)],[7308])).
% 109.89/37.66 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 109.89/37.66 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------