%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO560^1 : TPTP v9.3.1. Released v5.2.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 : n001.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:46:07 AM UTC 2026
% Result : Theorem 10.48s 3.89s
% Output : Refutation 9.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO560^1 : TPTP v9.3.1. Released v5.2.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.20 % Computer : n001.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % 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 17:21:06 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.92/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.57/1.04 % [INFO] Parsing done (248ms).
% 1.57/1.06 % [INFO] Running in sequential loop mode.
% 2.30/1.54 % [INFO] eprover registered as external prover.
% 2.30/1.55 % [INFO] Scanning for conjecture ...
% 2.56/1.61 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.56/1.65 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.56/1.67 % [INFO] Problem is higher-order (TPTP THF).
% 2.56/1.67 % [INFO] Type checking passed.
% 2.56/1.68 % [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 ...
% 10.48/3.88 % [INFO] Killing All external provers ...
% 10.48/3.88 % Time passed: 3556ms (effective reasoning time: 2805ms)
% 10.48/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)>
% 10.48/3.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3556 ms resp. 2805 ms w/o parsing
% 9.49/3.97 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.49/3.97 thf(epso_decl, type, epso: (($o > $o) > $o)).
% 9.49/3.97 thf(epsoo_decl, type, epsoo: ((($o > $o) > $o) > ($o > $o))).
% 9.49/3.97 thf(q_decl, type, q: (($o > $o) > $o)).
% 9.49/3.97 thf(sk1_decl, type, sk1: $o).
% 9.49/3.97 thf(sk2_decl, type, sk2: $o).
% 9.49/3.97 thf(sk3_decl, type, sk3: $o).
% 9.49/3.97 thf(sk5_decl, type, sk5: $o).
% 9.49/3.97 thf(3,axiom,((! [A:($o > $o)]: ((? [B:$o]: (A @ B)) => (A @ (epso @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',choiceaxo)).
% 9.49/3.97 thf(9,plain,((! [A:($o > $o)]: ((? [B:$o]: (A @ B)) => (A @ (epso @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 9.49/3.97 thf(12,plain,(((($true)) => (epso @ (^ [A:$o]: (A))))),inference(instance,[status(thm)],[9])).
% 9.49/3.97 thf(13,plain,((epso @ (^ [A:$o]: (A)))),inference(simp,[status(thm)],[12])).
% 9.49/3.97 thf(45,axiom,((? [A:((($o > $o) > $o) > ($o > $o))]: ! [B:(($o > $o) > $o)]: ((? [C:($o > $o)]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 9.49/3.97 thf(46,plain,(! [A:($o > $o)] : ((~ (epso @ (A))) | (epso @ (epsoo @ (epso))))),inference(choice,[status(esa)],[45])).
% 9.49/3.97 thf(141,plain,(! [A:($o > $o)] : (~ (($true)) | (epso @ (epsoo @ (epso))) | ((epso @ (^ [B:$o]: (B))) != (epso @ (A))))),inference(paramod_ordered,[status(thm)],[13,46])).
% 9.49/3.97 thf(142,plain,(! [A:($o > $o)] : ((epso @ (epsoo @ (epso))) | ((epso @ (^ [B:$o]: (B))) != (epso @ (A))))),inference(simp,[status(thm)],[141])).
% 9.49/3.97 thf(143,plain,((epso @ (epsoo @ (epso)))),inference(pattern_uni,[status(thm)],[142:[bind(A, $thf(^ [B:$o]: (B)))]])).
% 9.49/3.97 thf(14,plain,(((~ (($false))) => (~ (epso @ ((~)))))),inference(instance,[status(thm)],[9])).
% 9.49/3.97 thf(15,plain,((~ (epso @ ((~))))),inference(simp,[status(thm)],[14])).
% 9.49/3.97 thf(147,plain,(~ (($true)) | ((epso @ (epsoo @ (epso))) != (epso @ ((~))))),inference(paramod_ordered,[status(thm)],[143,15])).
% 9.49/3.97 thf(148,plain,(((epso @ (epsoo @ (epso))) != (epso @ ((~))))),inference(simp,[status(thm)],[147])).
% 9.49/3.97 thf(149,plain,(((epsoo @ (epso)) != ((~)))),inference(simp,[status(thm)],[148])).
% 9.49/3.97 thf(157,plain,(((epsoo @ (epso) @ sk5) != (~ (sk5)))),inference(func_ext,[status(esa)],[149])).
% 9.49/3.97 thf(159,plain,((epsoo @ (epso) @ sk5) | (~ (sk5))),inference(bool_ext,[status(thm)],[157])).
% 9.49/3.97 thf(173,plain,((epsoo @ (epso) @ sk5) | ~ (sk5)),inference(cnf,[status(esa)],[159])).
% 9.49/3.97 thf(6,axiom,((q @ (^ [A:$o]: (($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',qkf)).
% 9.49/3.97 thf(25,plain,((q @ (^ [A:$o]: (($false))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 9.49/3.97 thf(1,conjecture,((q @ (epsoo @ epso))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c)).
% 9.49/3.97 thf(2,negated_conjecture,((~ (q @ (epsoo @ epso)))),inference(neg_conjecture,[status(cth)],[1])).
% 9.49/3.97 thf(8,plain,((~ (q @ (epsoo @ (epso))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 9.49/3.97 thf(38,plain,(~ (($true)) | ((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (($false)))))),inference(paramod_ordered,[status(thm)],[25,8])).
% 9.49/3.97 thf(39,plain,(((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (($false)))))),inference(simp,[status(thm)],[38])).
% 9.49/3.97 thf(40,plain,(((epsoo @ (epso)) != (^ [A:$o]: (($false))))),inference(simp,[status(thm)],[39])).
% 9.49/3.97 thf(42,plain,((epsoo @ (epso) @ sk3)),inference(func_ext,[status(esa)],[40])).
% 9.49/3.97 thf(5,axiom,((q @ (^ [A:$o]: (($true))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',qkt)).
% 9.49/3.97 thf(24,plain,((q @ (^ [A:$o]: (($true))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 9.49/3.97 thf(31,plain,(~ (($true)) | ((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (($true)))))),inference(paramod_ordered,[status(thm)],[24,8])).
% 9.49/3.97 thf(32,plain,(((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (($true)))))),inference(simp,[status(thm)],[31])).
% 9.49/3.97 thf(35,plain,(((epsoo @ (epso)) != (^ [A:$o]: (($true))))),inference(simp,[status(thm)],[32])).
% 9.49/3.97 thf(41,plain,((~ (epsoo @ (epso) @ sk2))),inference(func_ext,[status(esa)],[35])).
% 9.49/3.97 thf(48,plain,(~ (($true)) | ((epsoo @ (epso) @ sk3) != (epsoo @ (epso) @ sk2))),inference(paramod_ordered,[status(thm)],[42,41])).
% 9.49/3.97 thf(49,plain,(((epsoo @ (epso) @ sk3) != (epsoo @ (epso) @ sk2))),inference(simp,[status(thm)],[48])).
% 9.49/3.97 thf(51,plain,(((epso) != (epso)) | (sk3 != sk2)),inference(simp,[status(thm)],[49])).
% 9.49/3.97 thf(53,plain,((sk3 != sk2)),inference(simp,[status(thm)],[51])).
% 9.49/3.97 thf(55,plain,(sk3 | sk2),inference(bool_ext,[status(thm)],[53])).
% 9.49/3.97 thf(7,axiom,((q @ (^ [A:$o]: (A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',qid)).
% 9.49/3.97 thf(26,plain,((q @ (^ [A:$o]: (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 9.49/3.97 thf(33,plain,(~ (($true)) | ((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (A))))),inference(paramod_ordered,[status(thm)],[26,8])).
% 9.49/3.97 thf(34,plain,(((q @ (epsoo @ (epso))) != (q @ (^ [A:$o]: (A))))),inference(simp,[status(thm)],[33])).
% 9.49/3.97 thf(36,plain,(((epsoo @ (epso)) != (^ [A:$o]: (A)))),inference(simp,[status(thm)],[34])).
% 9.49/3.97 thf(37,plain,(((epsoo @ (epso) @ sk1) != sk1)),inference(func_ext,[status(esa)],[36])).
% 9.49/3.97 thf(47,plain,(~ (sk1) | ((epsoo @ (epso) @ sk3) != (epsoo @ (epso) @ sk1))),inference(paramod_ordered,[status(thm)],[42,37])).
% 9.49/3.97 thf(50,plain,(~ (sk1) | ((epso) != (epso)) | (sk3 != sk1)),inference(simp,[status(thm)],[47])).
% 9.49/3.97 thf(52,plain,(~ (sk1) | (sk3 != sk1)),inference(simp,[status(thm)],[50])).
% 9.49/3.97 thf(59,plain,(sk2 | ~ (sk1) | ~ (sk1) | (sk3 != sk3)),inference(paramod_ordered,[status(thm)],[55,52])).
% 9.49/3.97 thf(60,plain,(sk2 | ~ (sk1) | (sk3 != sk3)),inference(simp,[status(thm)],[59])).
% 9.49/3.97 thf(61,plain,(sk2 | ~ (sk1)),inference(pattern_uni,[status(thm)],[60:[]])).
% 9.49/3.97 thf(75,plain,(~ (sk1) | (~ (epsoo @ (epso) @ ($true))) | (sk2 != sk2)),inference(paramod_ordered,[status(thm)],[61,41])).
% 9.49/3.97 thf(76,plain,(~ (sk1) | (~ (epsoo @ (epso) @ ($true)))),inference(pattern_uni,[status(thm)],[75:[]])).
% 9.49/3.97 thf(312,plain,(~ (sk5) | ~ (sk1) | ~ (($true)) | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ ($true)))),inference(paramod_ordered,[status(thm)],[173,76])).
% 9.49/3.97 thf(313,plain,(~ (sk5) | ~ (sk1) | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ ($true)))),inference(simp,[status(thm)],[312])).
% 9.49/3.97 thf(328,plain,(~ (sk5) | ~ (sk1) | ((epso) != (epso)) | ~ (sk5)),inference(simp,[status(thm)],[313])).
% 9.49/3.97 thf(337,plain,(~ (sk5) | ~ (sk1)),inference(simp,[status(thm)],[328])).
% 9.49/3.97 thf(44,plain,((epsoo @ (epso) @ sk1) | sk1),inference(bool_ext,[status(thm)],[37])).
% 9.49/3.97 thf(160,plain,(sk1 | (~ (~ (sk5))) | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ sk1))),inference(paramod_ordered,[status(thm)],[44,157])).
% 9.49/3.97 thf(161,plain,(sk1 | sk5 | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ sk1))),inference(simp,[status(thm)],[160])).
% 9.49/3.97 thf(167,plain,(sk1 | sk5 | ((epso) != (epso)) | (sk5 != sk1)),inference(simp,[status(thm)],[161])).
% 9.49/3.97 thf(170,plain,(sk1 | sk5 | (sk5 != sk1)),inference(simp,[status(thm)],[167])).
% 9.49/3.97 thf(213,plain,(sk1 | sk5 | sk5 | sk1),inference(bool_ext,[status(thm)],[170])).
% 9.49/3.97 thf(214,plain,(sk1 | sk5),inference(simp,[status(thm)],[213])).
% 9.49/3.97 thf(86,plain,(sk1 | ~ (($true)) | ((epsoo @ (epso) @ sk2) != (epsoo @ (epso) @ sk1))),inference(paramod_ordered,[status(thm)],[44,41])).
% 9.49/3.97 thf(87,plain,(sk1 | ((epsoo @ (epso) @ sk2) != (epsoo @ (epso) @ sk1))),inference(simp,[status(thm)],[86])).
% 9.49/3.97 thf(88,plain,(sk1 | ((epso) != (epso)) | (sk2 != sk1)),inference(simp,[status(thm)],[87])).
% 9.49/3.97 thf(89,plain,(sk1 | (sk2 != sk1)),inference(simp,[status(thm)],[88])).
% 9.49/3.97 thf(91,plain,(sk1 | sk2 | sk1),inference(bool_ext,[status(thm)],[89])).
% 9.49/3.97 thf(95,plain,(sk1 | sk2),inference(simp,[status(thm)],[91])).
% 9.49/3.97 thf(102,plain,(sk1 | (~ (epsoo @ (epso) @ ($true))) | (sk2 != sk2)),inference(paramod_ordered,[status(thm)],[95,41])).
% 9.49/3.97 thf(103,plain,(sk1 | (~ (epsoo @ (epso) @ ($true)))),inference(pattern_uni,[status(thm)],[102:[]])).
% 9.49/3.97 thf(292,plain,(~ (sk5) | sk1 | ~ (($true)) | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ ($true)))),inference(paramod_ordered,[status(thm)],[173,103])).
% 9.49/3.97 thf(293,plain,(~ (sk5) | sk1 | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ ($true)))),inference(simp,[status(thm)],[292])).
% 9.49/3.97 thf(326,plain,(sk1 | ~ (sk5) | ((epso) != (epso)) | ~ (sk5)),inference(simp,[status(thm)],[293])).
% 9.49/3.97 thf(335,plain,(sk1 | ~ (sk5)),inference(simp,[status(thm)],[326])).
% 9.49/3.97 thf(354,plain,(sk1 | sk1 | ~ (($true)) | (sk5 != sk5)),inference(paramod_ordered,[status(thm)],[214,335])).
% 9.49/3.97 thf(355,plain,(sk1 | (sk5 != sk5)),inference(simp,[status(thm)],[354])).
% 9.49/3.97 thf(356,plain,(sk1),inference(pattern_uni,[status(thm)],[355:[]])).
% 9.49/3.97 thf(162,plain,((~ (~ (sk5))) | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ sk3))),inference(paramod_ordered,[status(thm)],[42,157])).
% 9.49/3.97 thf(163,plain,(sk5 | ((epsoo @ (epso) @ sk5) != (epsoo @ (epso) @ sk3))),inference(simp,[status(thm)],[162])).
% 9.49/3.97 thf(168,plain,(sk5 | ((epso) != (epso)) | (sk5 != sk3)),inference(simp,[status(thm)],[163])).
% 9.49/3.97 thf(171,plain,(sk5 | (sk5 != sk3)),inference(simp,[status(thm)],[168])).
% 9.49/3.97 thf(219,plain,(sk5 | sk5 | sk3),inference(bool_ext,[status(thm)],[171])).
% 9.49/3.97 thf(222,plain,(sk5 | sk3),inference(simp,[status(thm)],[219])).
% 9.49/3.97 thf(360,plain,(~ (($true)) | ~ (sk3)),inference(rewrite,[status(thm)],[52,356])).
% 9.49/3.97 thf(361,plain,(~ (sk3)),inference(simp,[status(thm)],[360])).
% 9.49/3.97 thf(376,plain,(sk5 | ($false)),inference(rewrite,[status(thm)],[222,361])).
% 9.49/3.97 thf(377,plain,(sk5),inference(simp,[status(thm)],[376])).
% 9.49/3.97 thf(411,plain,(~ (($true)) | ~ (($true))),inference(rewrite,[status(thm)],[337,356,377])).
% 9.49/3.97 thf(412,plain,(($false)),inference(simp,[status(thm)],[411])).
% 9.49/3.97 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.49/3.97 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------