%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI003^8 : TPTP v9.3.1. Released v9.0.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 : n020.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:13 AM UTC 2026
% Result : Theorem 11.97s 3.88s
% Output : Refutation 10.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI003^8 : TPTP v9.3.1. Released v9.0.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.11/0.21 % Computer : n020.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 13:18:04 UTC 2026
% 0.11/0.21 % CPUTime :
% 0.11/0.21 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.85/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.20/0.98 % [INFO] Parsing done (199ms).
% 1.20/1.00 % [INFO] Input problem is non-classical (logic $alethic_modal). Running HOL transformation from semantics specification contained in the problem file ...
% 1.67/1.14 % [INFO] Running in sequential loop mode.
% 2.49/1.52 % [INFO] eprover registered as external prover.
% 2.49/1.53 % [INFO] Scanning for conjecture ...
% 2.67/1.63 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.67/1.66 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.67/1.68 % [INFO] Problem is higher-order (TPTP THF).
% 2.67/1.69 % [INFO] Type checking passed.
% 2.67/1.69 % [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 ...
% 11.97/3.87 % [INFO] Killing All external provers ...
% 11.97/3.88 % Time passed: 3525ms (effective reasoning time: 2730ms)
% 11.97/3.88 % Solved by 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)>
% 11.97/3.88 % Axioms used in derivation (4): mrel_universal, a3, a2, a1
% 11.97/3.88 % No. of inferences in proof: 46
% 11.97/3.88 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3525 ms resp. 2730 ms w/o parsing
% 10.91/3.95 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.91/3.95 thf(mworld_type, type, mworld: $tType).
% 10.91/3.95 thf(mrel_decl, type, mrel: (mworld > (mworld > $o))).
% 10.91/3.95 thf(mbox_decl, type, mbox: ((mworld > $o) > (mworld > $o))).
% 10.91/3.95 thf(mdia_decl, type, mdia: ((mworld > $o) > (mworld > $o))).
% 10.91/3.95 thf(mactual_decl, type, mactual: mworld).
% 10.91/3.95 thf(mlocal_decl, type, mlocal: ((mworld > $o) > $o)).
% 10.91/3.95 thf(mglobal_decl, type, mglobal: ((mworld > $o) > $o)).
% 10.91/3.95 thf(positive_decl, type, positive: (mworld > (($i > $o) > $o))).
% 10.91/3.95 thf(godlike_decl, type, godlike: (mworld > ($i > $o))).
% 10.91/3.95 thf(sk1_decl, type, sk1: ($i > (mworld > ($i > $o)))).
% 10.91/3.95 thf(sk2_decl, type, sk2: (($i > $o) > (($i > $o) > (mworld > mworld)))).
% 10.91/3.95 thf(sk3_decl, type, sk3: (($i > $o) > (($i > $o) > (mworld > $i)))).
% 10.91/3.95 thf(sk15_decl, type, sk15: (mworld > $i)).
% 10.91/3.95 thf(mbox_def, definition, mbox = (^ [A:(mworld > $o),B:mworld]: ! [C:mworld]: ((mrel @ B @ C) => (A @ C))) ).
% 10.91/3.95 thf(mdia_def, definition, mdia = (^ [A:(mworld > $o),B:mworld]: ? [C:mworld]: ((mrel @ B @ C) & (A @ C))) ).
% 10.91/3.95 thf(mlocal_def, definition, mlocal = (^ [A:(mworld > $o)]: (A @ mactual)) ).
% 10.91/3.95 thf(mglobal_def, definition, mglobal = ((!) @ mworld) ).
% 10.91/3.95 thf(godlike_def, definition, godlike = (^ [A:mworld,B:$i]: ! [C:($i > $o)]: ((positive @ A @ C) => (C @ B))) ).
% 10.91/3.95 thf(sk1_def, definition, sk1 = (^ [A:$i,B:mworld]: (@+ [C:($i > $o)]: ~ ((positive @ B @ C) => (C @ A)))) ).
% 10.91/3.95 thf(sk2_def, definition, sk2 = (^ [A:($i > $o),B:($i > $o),C:mworld]: (@+ [D:mworld]: (mrel @ C @ D))) ).
% 10.91/3.95 thf(sk3_def, definition, sk3 = (^ [A:($i > $o),B:($i > $o),C:mworld]: (@+ [D:$i]: ~ ((B @ D) => (A @ D)))) ).
% 10.91/3.95 thf(1,conjecture,((mlocal @ (mdia @ (^ [A:mworld]: ? [B:$i]: (godlike @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c)).
% 10.91/3.95 thf(2,negated_conjecture,((~ (mlocal @ (mdia @ (^ [A:mworld]: ? [B:$i]: (godlike @ A @ B)))))),inference(neg_conjecture,[status(cth)],[1])).
% 10.91/3.95 thf(7,plain,((~ (? [A:mworld]: ((mrel @ mactual @ A) & ? [B:$i]: ! [C:($i > $o)]: ((positive @ A @ (C)) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 10.91/3.95 thf(8,plain,(! [B:$i,A:mworld] : (((~ (mrel @ mactual @ A) | (positive @ A @ (sk1 @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (sk1 @ B @ A @ B))))),inference(cnf,[status(esa)],[7])).
% 10.91/3.95 thf(9,plain,(! [B:$i,A:mworld] : ((~ (mrel @ mactual @ A)) | (positive @ A @ (sk1 @ B @ A)))),inference(cnfConj,[status(thm)],[8])).
% 10.91/3.95 thf(3,axiom,((! [A:mworld,B:mworld]: (mrel @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_universal)).
% 10.91/3.95 thf(11,plain,((! [A:mworld,B:mworld]: (mrel @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 10.91/3.95 thf(12,plain,(! [B:mworld,A:mworld] : ((mrel @ A @ B))),inference(cnf,[status(esa)],[11])).
% 10.91/3.95 thf(50,plain,(! [B:$i,A:mworld] : (~ (($true)) | (positive @ A @ (sk1 @ B @ A)))),inference(rewrite,[status(thm)],[9,12])).
% 10.91/3.95 thf(51,plain,(! [B:$i,A:mworld] : ((positive @ A @ (sk1 @ B @ A)))),inference(simp,[status(thm)],[50])).
% 10.91/3.95 thf(6,axiom,((mglobal @ (^ [A:mworld]: (positive @ A @ (godlike @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3)).
% 10.91/3.95 thf(22,plain,((! [A:mworld]: (positive @ A @ (^ [B:$i]: ! [C:($i > $o)]: ((positive @ A @ C) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 10.91/3.95 thf(23,plain,(! [A:mworld] : ((positive @ A @ (^ [B:$i]: ! [C:($i > $o)]: ((positive @ A @ C) => (C @ B)))))),inference(cnf,[status(esa)],[22])).
% 10.91/3.95 thf(5,axiom,((mglobal @ (^ [A:mworld]: ! [B:($i > $o),C:($i > $o)]: (((positive @ A @ B) & (mbox @ (^ [D:mworld]: ! [E:$i]: ((B @ E) => (C @ E))) @ A)) => (positive @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 10.91/3.95 thf(16,plain,((! [A:mworld,B:($i > $o),C:($i > $o)]: (((positive @ A @ (B)) & ! [D:mworld]: ((mrel @ A @ D) => (! [E:$i]: ((B @ E) => (C @ E))))) => (positive @ A @ (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 10.91/3.95 thf(17,plain,((! [A:mworld,B:($i > $o),C:($i > $o)]: (((positive @ A @ (B)) & ((? [D:mworld]: (mrel @ A @ D)) => (! [D:$i]: ((B @ D) => (C @ D))))) => (positive @ A @ (C))))),inference(miniscope,[status(thm)],[16])).
% 10.91/3.95 thf(18,plain,(! [C:($i > $o),B:($i > $o),A:mworld] : (((~ (positive @ A @ (B)) | (mrel @ A @ (sk2 @ (C) @ (B) @ A)) | (positive @ A @ (C))) & (~ (positive @ A @ (B)) | (B @ (sk3 @ (C) @ (B) @ A)) | (positive @ A @ (C))) & (~ (positive @ A @ (B)) | ~ (C @ (sk3 @ (C) @ (B) @ A)) | (positive @ A @ (C)))))),inference(cnf,[status(esa)],[17])).
% 10.91/3.95 thf(20,plain,(! [C:($i > $o),B:($i > $o),A:mworld] : ((~ (positive @ A @ (B))) | (B @ (sk3 @ (C) @ (B) @ A)) | (positive @ A @ (C)))),inference(cnfConj,[status(thm)],[18])).
% 10.91/3.95 thf(204,plain,(! [B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [C:$i]: (($false))))) | ($false) | (positive @ A @ (B)))),inference(prim_subst,[status(thm)],[20:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (($false))))]])).
% 10.91/3.95 thf(232,plain,(! [B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [C:$i]: (($false))))) | (positive @ A @ (B)))),inference(simp,[status(thm)],[204])).
% 10.91/3.95 thf(4,axiom,((mglobal @ (^ [A:mworld]: ! [B:($i > $o)]: ((positive @ A @ (^ [C:$i]: ~ (B @ C))) = (~ (positive @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 10.91/3.95 thf(13,plain,((! [A:mworld,B:($i > $o)]: ((positive @ A @ (^ [C:$i]: ~ (B @ C))) = (~ (positive @ A @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 10.91/3.95 thf(14,plain,(! [B:($i > $o),A:mworld] : (((positive @ A @ (^ [C:$i]: ~ (B @ C))) = (~ (positive @ A @ (B)))))),inference(cnf,[status(esa)],[13])).
% 10.91/3.95 thf(15,plain,(! [B:($i > $o),A:mworld] : (((positive @ A @ (^ [C:$i]: ~ (B @ C))) = (~ (positive @ A @ (B)))))),inference(lifteq,[status(thm)],[14])).
% 10.91/3.95 thf(328,plain,(! [D:($i > $o),C:mworld,B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [E:$i]: (($false))))) | (~ (positive @ C @ (D))) | ((positive @ A @ (B)) != (positive @ C @ (^ [E:$i]: ~ (D @ E)))))),inference(paramod_ordered,[status(thm)],[232,15])).
% 10.91/3.95 thf(329,plain,(! [D:($i > $o),C:mworld,B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [E:$i]: (($false))))) | (~ (positive @ C @ (D))) | ((positive @ A @ (B)) != (positive @ C @ (^ [E:$i]: ~ (D @ E)))))),inference(simp,[status(thm)],[328])).
% 10.91/3.95 thf(330,plain,(! [B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [C:$i]: (($false))))) | (~ (positive @ A @ (B))))),inference(pattern_uni,[status(thm)],[329:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: ~ (E @ F))),bind(C, $thf(A)),bind(D, $thf(E))]])).
% 10.91/3.95 thf(349,plain,(! [B:($i > $o),A:mworld] : ((~ (positive @ A @ (^ [C:$i]: (($false))))) | (~ (positive @ A @ (B))))),inference(simp,[status(thm)],[330])).
% 10.91/3.95 thf(366,plain,(! [D:($i > $o),C:mworld,B:$i,A:mworld] : ((~ (positive @ C @ (^ [E:$i]: (($false))))) | ~ (($true)) | ((positive @ A @ (sk1 @ B @ A)) != (positive @ C @ (D))))),inference(paramod_ordered,[status(thm)],[51,349])).
% 10.91/3.95 thf(367,plain,(! [D:($i > $o),C:mworld,B:$i,A:mworld] : ((~ (positive @ C @ (^ [E:$i]: (($false))))) | ((positive @ A @ (sk1 @ B @ A)) != (positive @ C @ (D))))),inference(simp,[status(thm)],[366])).
% 10.91/3.95 thf(368,plain,(! [A:mworld] : ((~ (positive @ A @ (^ [B:$i]: (($false))))))),inference(pattern_uni,[status(thm)],[367:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(A)),bind(D, $thf(sk1 @ B @ A))]])).
% 10.91/3.95 thf(421,plain,(! [B:mworld,A:mworld] : (~ (($true)) | ((positive @ A @ (^ [C:$i]: ! [D:($i > $o)]: ((positive @ A @ D) => (D @ C)))) != (positive @ B @ (^ [C:$i]: (($false))))))),inference(paramod_ordered,[status(thm)],[23,368])).
% 10.91/3.95 thf(422,plain,(! [B:mworld,A:mworld] : (((positive @ A @ (^ [C:$i]: ! [D:($i > $o)]: ((positive @ A @ D) => (D @ C)))) != (positive @ B @ (^ [C:$i]: (($false))))))),inference(simp,[status(thm)],[421])).
% 10.91/3.95 thf(432,plain,(! [B:mworld,A:mworld] : ((A != B) | ((^ [C:$i]: ! [D:($i > $o)]: ((positive @ A @ D) => (D @ C))) != (^ [C:$i]: (($false)))))),inference(simp,[status(thm)],[422])).
% 10.91/3.95 thf(434,plain,(! [A:mworld] : (((^ [B:$i]: ! [C:($i > $o)]: ((positive @ A @ C) => (C @ B))) != (^ [B:$i]: (($false)))))),inference(simp,[status(thm)],[432])).
% 10.91/3.95 thf(492,plain,(! [A:mworld] : ((! [B:($i > $o)]: ((positive @ A @ (B)) => (B @ (sk15 @ A)))))),inference(func_ext,[status(esa)],[434])).
% 10.91/3.95 thf(493,plain,(! [B:($i > $o),A:mworld] : ((~ (positive @ A @ (B))) | (B @ (sk15 @ A)))),inference(cnf,[status(esa)],[492])).
% 10.91/3.95 thf(716,plain,(! [D:($i > $o),C:mworld,B:$i,A:mworld] : (~ (($true)) | (D @ (sk15 @ C)) | ((positive @ A @ (sk1 @ B @ A)) != (positive @ C @ (D))))),inference(paramod_ordered,[status(thm)],[51,493])).
% 10.91/3.95 thf(717,plain,(! [D:($i > $o),C:mworld,B:$i,A:mworld] : ((D @ (sk15 @ C)) | ((positive @ A @ (sk1 @ B @ A)) != (positive @ C @ (D))))),inference(simp,[status(thm)],[716])).
% 10.91/3.95 thf(718,plain,(! [B:$i,A:mworld] : ((sk1 @ B @ A @ (sk15 @ A)))),inference(pattern_uni,[status(thm)],[717:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(A)),bind(D, $thf(sk1 @ B @ A))]])).
% 10.91/3.95 thf(10,plain,(! [B:$i,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (sk1 @ B @ A @ B)))),inference(cnfConj,[status(thm)],[8])).
% 10.91/3.95 thf(36,plain,(! [B:$i,A:mworld] : (~ (($true)) | (~ (sk1 @ B @ A @ B)))),inference(rewrite,[status(thm)],[10,12])).
% 10.91/3.95 thf(37,plain,(! [B:$i,A:mworld] : ((~ (sk1 @ B @ A @ B)))),inference(simp,[status(thm)],[36])).
% 10.91/3.95 thf(974,plain,(! [D:$i,C:mworld,B:$i,A:mworld] : (~ (($true)) | ((sk1 @ B @ A @ (sk15 @ A)) != (sk1 @ D @ C @ D)))),inference(paramod_ordered,[status(thm)],[718,37])).
% 10.91/3.95 thf(975,plain,(! [D:$i,C:mworld,B:$i,A:mworld] : (((sk1 @ B @ A @ (sk15 @ A)) != (sk1 @ D @ C @ D)))),inference(simp,[status(thm)],[974])).
% 10.91/3.95 thf(976,plain,(($false)),inference(pattern_uni,[status(thm)],[975:[bind(A, $thf(E)),bind(B, $thf(sk15 @ E)),bind(C, $thf(E)),bind(D, $thf(sk15 @ E))]])).
% 10.91/3.95 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.91/3.95 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------