%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO052^2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/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:45:06 AM UTC 2026
% Result : Theorem 23.63s 6.91s
% Output : Refutation 23.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO052^2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.22 % Computer : n003.cluster.edu
% 0.12/0.22 % Model : x86_64 x86_64
% 0.12/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.22 % Memory : 8046.5625MB
% 0.12/0.22 % OS : Linux 6.8.0-71-generic
% 0.12/0.22 % CPULimit : 300
% 0.12/0.22 % WCLimit : 300
% 0.12/0.22 % DateTime : Tue Sep 29 16:26:44 UTC 2026
% 0.12/0.23 % CPUTime :
% 0.12/0.23 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.41/1.05 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.23/1.44 % [INFO] Parsing done (382ms).
% 2.23/1.46 % [INFO] Running in sequential loop mode.
% 3.03/2.04 % [INFO] eprover registered as external prover.
% 3.33/2.05 % [INFO] Scanning for conjecture ...
% 3.84/2.30 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 3.84/2.35 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 3.84/2.35 % [INFO] Problem is higher-order (TPTP THF).
% 3.84/2.35 % [INFO] Type checking passed.
% 3.84/2.36 % [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 ...
% 23.63/6.90 % [INFO] Killing All external provers ...
% 23.63/6.91 % Time passed: 6475ms (effective reasoning time: 5437ms)
% 23.63/6.91 % 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)>
% 23.63/6.91 % Axioms used in derivation (0):
% 23.63/6.91 % No. of inferences in proof: 29
% 23.63/6.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 6475 ms resp. 5437 ms w/o parsing
% 23.63/7.03 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.63/7.03 thf(mu_type, type, mu: $tType).
% 23.63/7.03 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 23.63/7.03 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 23.63/7.03 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 23.63/7.03 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 23.63/7.03 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 23.63/7.03 thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 23.63/7.03 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 23.63/7.03 thf(sk1_decl, type, sk1: ($i > (($i > ($i > $o)) > (($i > $o) > (($i > $o) > $o))))).
% 23.63/7.03 thf(sk2_decl, type, sk2: (($i > $o) > (($i > $o) > ($i > (($i > ($i > $o)) > $i))))).
% 23.63/7.03 thf(sk3_decl, type, sk3: (($i > $o) > (($i > $o) > ($i > (($i > ($i > $o)) > $i))))).
% 23.63/7.03 thf(sk4_decl, type, sk4: (($i > $o) > (($i > $o) > ($i > (($i > ($i > $o)) > $i))))).
% 23.63/7.03 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 23.63/7.03 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 23.63/7.03 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 23.63/7.03 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 23.63/7.03 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 23.63/7.03 thf(mdia_def, definition, mdia = (^ [A:($i > ($i > $o)),B:($i > $o)]: (mnot @ (mbox @ A @ (mnot @ B)))) ).
% 23.63/7.03 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 23.63/7.03 thf(sk2_def, definition, sk2 = (^ [A:($i > $o),B:($i > $o),C:$i,D:($i > ($i > $o))]: (@+ [E:$i]: ~ (~ (D @ C @ E) | ~ (B @ E) | (A @ E)))) ).
% 23.63/7.03 thf(sk3_def, definition, sk3 = (^ [A:($i > $o),B:($i > $o),C:$i,D:($i > ($i > $o))]: (@+ [E:$i]: ~ (~ (D @ C @ E) | (B @ E)))) ).
% 23.63/7.03 thf(sk4_def, definition, sk4 = (^ [A:($i > $o),B:($i > $o),C:$i,D:($i > ($i > $o))]: (@+ [E:$i]: ~ (~ (D @ C @ E) | ~ (A @ E)))) ).
% 23.63/7.03 thf(1,conjecture,((? [A:($i > ($i > $o))]: ~ (mvalid @ (mforall_prop @ (^ [B:($i > $o)]: (mforall_prop @ (^ [C:($i > $o)]: (mimplies @ (mbox @ A @ (mimplies @ B @ C)) @ (mimplies @ (mbox @ A @ B) @ (mdia @ A @ C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 23.63/7.03 thf(2,negated_conjecture,((~ (? [A:($i > ($i > $o))]: ~ (mvalid @ (mforall_prop @ (^ [B:($i > $o)]: (mforall_prop @ (^ [C:($i > $o)]: (mimplies @ (mbox @ A @ (mimplies @ B @ C)) @ (mimplies @ (mbox @ A @ B) @ (mdia @ A @ C))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 23.63/7.03 thf(3,plain,((~ (? [A:($i > ($i > $o))]: ~ (! [B:$i,C:($i > $o),D:($i > $o)]: (~ (! [E:$i]: (~ (A @ B @ E) | ~ (C @ E) | (D @ E))) | ~ (! [E:$i]: (~ (A @ B @ E) | (C @ E))) | ~ (! [E:$i]: (~ (A @ B @ E) | ~ (D @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 23.63/7.03 thf(4,plain,((~ (~ (! [A:($i > ($i > $o)),B:$i,C:($i > $o),D:($i > $o)]: (~ (! [E:$i]: (~ (A @ B @ E) | ~ (C @ E) | (D @ E))) | ~ (! [E:$i]: (~ (A @ B @ E) | (C @ E))) | ~ (! [E:$i]: (~ (A @ B @ E) | ~ (D @ E)))))))),inference(miniscope,[status(thm)],[3])).
% 23.63/7.03 thf(5,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((((A @ B @ (sk2 @ (D) @ (C) @ B @ (A))) | (sk1 @ B @ A @ C @ D)) & ((C @ (sk2 @ (D) @ (C) @ B @ (A))) | (sk1 @ B @ A @ C @ D)) & (~ (D @ (sk2 @ (D) @ (C) @ B @ (A))) | (sk1 @ B @ A @ C @ D)) & (~ (sk1 @ B @ A @ C @ D) | (A @ B @ (sk3 @ (D) @ (C) @ B @ (A))) | (A @ B @ (sk4 @ (D) @ (C) @ B @ (A)))) & (~ (sk1 @ B @ A @ C @ D) | (A @ B @ (sk3 @ (D) @ (C) @ B @ (A))) | (D @ (sk4 @ (D) @ (C) @ B @ (A)))) & (~ (sk1 @ B @ A @ C @ D) | ~ (C @ (sk3 @ (D) @ (C) @ B @ (A))) | (A @ B @ (sk4 @ (D) @ (C) @ B @ (A)))) & (~ (sk1 @ B @ A @ C @ D) | ~ (C @ (sk3 @ (D) @ (C) @ B @ (A))) | (D @ (sk4 @ (D) @ (C) @ B @ (A))))))),inference(cnf,[status(esa)],[4])).
% 23.63/7.03 thf(8,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((C @ (sk2 @ (D) @ (C) @ B @ (A))) | (sk1 @ B @ A @ C @ D))),inference(cnfConj,[status(thm)],[5])).
% 23.63/7.03 thf(7,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ C @ D)) | (~ (C @ (sk3 @ (D) @ (C) @ B @ (A)))) | (D @ (sk4 @ (D) @ (C) @ B @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 23.63/7.03 thf(71,plain,(! [C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ C @ (^ [D:$i]: (($false))))) | (~ (C @ (sk3 @ (^ [D:$i]: (($false))) @ (C) @ B @ (A)))) | ($false))),inference(prim_subst,[status(thm)],[7:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(^ [E:$i]: (($false))))]])).
% 23.63/7.03 thf(107,plain,(! [C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ C @ (^ [D:$i]: (($false))))) | (~ (C @ (sk3 @ (^ [D:$i]: (($false))) @ (C) @ B @ (A)))))),inference(simp,[status(thm)],[71])).
% 23.63/7.03 thf(169,plain,(! [B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ (^ [C:$i]: (($true))) @ (^ [C:$i]: (($false))))) | ~ (($true)))),inference(prim_subst,[status(thm)],[107:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [D:$i]: (($true))))]])).
% 23.63/7.03 thf(197,plain,(! [B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ (^ [C:$i]: (($true))) @ (^ [C:$i]: (($false))))))),inference(simp,[status(thm)],[169])).
% 23.63/7.03 thf(250,plain,(! [F:$i,E:($i > ($i > $o)),D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ (A) @ (C) @ (D)) | ~ (($true)) | ((C @ (sk2 @ (D) @ (C) @ B @ (A))) != (sk1 @ F @ (E) @ (^ [G:$i]: (($true))) @ (^ [G:$i]: (($false))))))),inference(paramod_ordered,[status(thm)],[8,197])).
% 23.63/7.03 thf(251,plain,(! [F:$i,E:($i > ($i > $o)),D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ (A) @ (C) @ (D)) | ((C @ (sk2 @ (D) @ (C) @ B @ (A))) != (sk1 @ F @ (E) @ (^ [G:$i]: (($true))) @ (^ [G:$i]: (($false))))))),inference(simp,[status(thm)],[250])).
% 23.63/7.03 thf(260,plain,(! [E:($i > ($i > ($i > $o))),D:($i > $i),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ (A) @ (^ [F:$i]: (sk1 @ (D @ F) @ (E @ F) @ (^ [G:$i]: (($true))) @ (^ [G:$i]: (($false))))) @ (C)))),inference(pre_uni,[status(thm)],[251:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [I:$i]: (sk1 @ (G @ I) @ (H @ I) @ (^ [J:$i]: (($true))) @ (^ [J:$i]: (($false)))))),bind(D, $thf(D)),bind(E, $thf(H @ (sk2 @ D @ (^ [I:$i]: (sk1 @ (G @ I) @ (H @ I) @ (^ [J:$i]: (($true))) @ (^ [J:$i]: (($false))))) @ B @ A))),bind(F, $thf(G @ (sk2 @ (D) @ (^ [I:$i]: (sk1 @ (G @ I) @ (H @ I) @ (^ [J:$i]: (($true))) @ (^ [J:$i]: (($false))))) @ B @ (A))))]])).
% 23.63/7.03 thf(268,plain,(! [E:($i > ($i > ($i > $o))),D:($i > $i),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ (A) @ (^ [F:$i]: (sk1 @ (D @ F) @ (E @ F) @ (^ [G:$i]: (($true))) @ (^ [G:$i]: (($false))))) @ (C)))),inference(simp,[status(thm)],[260])).
% 23.63/7.03 thf(17,plain,(! [C:($i > $o),B:$i,A:($i > ($i > $o))] : (($false) | (sk1 @ B @ A @ (^ [D:$i]: (($false))) @ C))),inference(prim_subst,[status(thm)],[8:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [E:$i]: (($false))))]])).
% 23.63/7.03 thf(26,plain,(! [C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ A @ (^ [D:$i]: (($false))) @ C))),inference(simp,[status(thm)],[17])).
% 23.63/7.03 thf(153,plain,(! [F:($i > $o),E:$i,D:($i > ($i > $o)),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ E @ (D) @ (F) @ (^ [G:$i]: (($false))))) | ~ (($true)) | ((sk1 @ B @ (A) @ (^ [G:$i]: (($false))) @ (C)) != (F @ (sk3 @ (^ [G:$i]: (($false))) @ (F) @ E @ (D)))))),inference(paramod_ordered,[status(thm)],[26,107])).
% 23.63/7.03 thf(154,plain,(! [F:($i > $o),E:$i,D:($i > ($i > $o)),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ E @ (D) @ (F) @ (^ [G:$i]: (($false))))) | ((sk1 @ B @ (A) @ (^ [G:$i]: (($false))) @ (C)) != (F @ (sk3 @ (^ [G:$i]: (($false))) @ (F) @ E @ (D)))))),inference(simp,[status(thm)],[153])).
% 23.63/7.03 thf(191,plain,(! [E:($i > ($i > $o)),D:($i > ($i > ($i > $o))),C:($i > $i),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ (A) @ (^ [F:$i]: (sk1 @ (C @ F) @ (D @ F) @ (^ [G:$i]: (($false))) @ (E @ F))) @ (^ [F:$i]: (($false))))))),inference(pre_uni,[status(thm)],[154:[bind(A, $thf(H @ (sk3 @ (^ [J:$i]: (($false))) @ (^ [J:$i]: (sk1 @ (G @ J) @ (H @ J) @ (^ [K:$i]: (($false))) @ (J @ J))) @ E @ D))),bind(B, $thf(G @ (sk3 @ (^ [J:$i]: (($false))) @ (^ [J:$i]: (sk1 @ (G @ J) @ (H @ J) @ (^ [K:$i]: (($false))) @ (J @ J))) @ E @ (D)))),bind(C, $thf(J @ (sk3 @ (^ [J:$i]: (($false))) @ (^ [J:$i]: (sk1 @ (G @ J) @ (H @ J) @ (^ [K:$i]: (($false))) @ (J @ J))) @ E @ D))),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(^ [J:$i]: (sk1 @ (G @ J) @ (H @ J) @ (^ [K:$i]: (($false))) @ (J @ J))))]])).
% 23.63/7.03 thf(215,plain,(! [E:($i > ($i > $o)),D:($i > ($i > ($i > $o))),C:($i > $i),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ (A) @ (^ [F:$i]: (sk1 @ (C @ F) @ (D @ F) @ (^ [G:$i]: (($false))) @ (E @ F))) @ (^ [F:$i]: (($false))))))),inference(simp,[status(thm)],[191])).
% 23.63/7.03 thf(438,plain,(! [B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ (A) @ (^ [C:$i]: (($true))) @ (^ [C:$i]: (($false))))))),inference(rewrite,[status(thm)],[215,26])).
% 23.63/7.03 thf(495,plain,(! [C:($i > $o),B:$i,A:($i > ($i > $o))] : ((sk1 @ B @ (A) @ (^ [D:$i]: (($false))) @ (C)))),inference(rewrite,[status(thm)],[268,438])).
% 23.63/7.03 thf(9,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:($i > ($i > $o))] : ((~ (sk1 @ B @ A @ C @ D)) | (A @ B @ (sk3 @ (D) @ (C) @ B @ (A))) | (A @ B @ (sk4 @ (D) @ (C) @ B @ (A))))),inference(cnfConj,[status(thm)],[5])).
% 23.63/7.03 thf(751,plain,(! [C:($i > $o),B:($i > $o),A:$i] : ((~ (sk1 @ A @ (^ [D:$i,E:$i]: (($false))) @ B @ C)) | ($false) | ($false))),inference(prim_subst,[status(thm)],[9:[bind(A, $thf(^ [E:$i,F:$i]: (($false))))]])).
% 23.63/7.03 thf(800,plain,(! [C:($i > $o),B:($i > $o),A:$i] : ((~ (sk1 @ A @ (^ [D:$i,E:$i]: (($false))) @ B @ C)))),inference(simp,[status(thm)],[751])).
% 23.63/7.03 thf(835,plain,(! [F:($i > $o),E:($i > $o),D:$i,C:($i > $o),B:$i,A:($i > ($i > $o))] : (~ (($true)) | ((sk1 @ B @ (A) @ (^ [G:$i]: (($false))) @ (C)) != (sk1 @ D @ (^ [G:$i,H:$i]: (($false))) @ (E) @ (F))))),inference(paramod_ordered,[status(thm)],[495,800])).
% 23.63/7.03 thf(836,plain,(! [F:($i > $o),E:($i > $o),D:$i,C:($i > $o),B:$i,A:($i > ($i > $o))] : (((sk1 @ B @ (A) @ (^ [G:$i]: (($false))) @ (C)) != (sk1 @ D @ (^ [G:$i,H:$i]: (($false))) @ (E) @ (F))))),inference(simp,[status(thm)],[835])).
% 23.63/7.03 thf(837,plain,(($false)),inference(pattern_uni,[status(thm)],[836:[bind(A, $thf(^ [G:$i,H:$i]: (($false)))),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(B)),bind(E, $thf(^ [G:$i]: (($false)))),bind(F, $thf(C))]])).
% 23.63/7.03 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.63/7.03 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------