%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO556^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 6.41s 2.12s
% Output : Refutation 6.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO556^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.21 % Computer : n001.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 17:20:36 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.65/0.52 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.87/0.62 % [INFO] Parsing done (98ms).
% 1.04/0.63 % [INFO] Running in sequential loop mode.
% 1.33/0.82 % [INFO] eprover registered as external prover.
% 1.33/0.83 % [INFO] Scanning for conjecture ...
% 1.33/0.88 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 1.58/0.90 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 1.58/0.90 % [INFO] Problem is higher-order (TPTP THF).
% 1.58/0.91 % [INFO] Type checking passed.
% 1.58/0.91 % [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 ...
% 6.41/2.11 % [INFO] Killing All external provers ...
% 6.41/2.12 % Time passed: 1809ms (effective reasoning time: 1483ms)
% 6.41/2.12 % 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)>
% 6.41/2.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 1809 ms resp. 1483 ms w/o parsing
% 6.34/2.21 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.34/2.21 thf(eps_decl, type, eps: (($i > $o) > $i)).
% 6.34/2.21 thf(if_decl, type, if: ($o > ($i > ($i > $i)))).
% 6.34/2.21 thf(sk1_decl, type, sk1: ($i > $o)).
% 6.34/2.21 thf(sk2_decl, type, sk2: ($i > $i)).
% 6.34/2.21 thf(sk3_decl, type, sk3: ($i > ($i > $i))).
% 6.34/2.21 thf(sk4_decl, type, sk4: $i).
% 6.34/2.21 thf(sk6_decl, type, sk6: $i).
% 6.34/2.21 thf(if_def, definition, if = (^ [A:$o,B:$i,C:$i]: (eps @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))) ).
% 6.34/2.21 thf(sk1_def, definition, sk1 = (@+ [A:($i > $o)]: ~ ((eps @ (A)) = (eps @ (^ [B:$i]: ((? [C:$i]: (A @ C) & (B = (eps @ A))) | (~ (? [C:$i]: (A @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))))) ).
% 6.34/2.21 thf(sk2_def, definition, sk2 = (^ [A:$i]: (@+ [B:$i]: (sk1 @ B))) ).
% 6.34/2.21 thf(sk3_def, definition, sk3 = (^ [A:$i,B:$i]: (@+ [C:$i]: (sk1 @ C))) ).
% 6.34/2.21 thf(sk6_def, definition, sk6 = (@+ [A:$i]: (sk1 @ A)) ).
% 6.34/2.21 thf(1,conjecture,((! [A:($i > $o)]: ((eps @ A) = (if @ (? [B:$i]: (A @ B)) @ (eps @ A) @ (eps @ (^ [B:$i]: (($false)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 6.34/2.21 thf(2,negated_conjecture,((~ (! [A:($i > $o)]: ((eps @ A) = (if @ (? [B:$i]: (A @ B)) @ (eps @ A) @ (eps @ (^ [B:$i]: (($false))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 6.34/2.21 thf(4,plain,((~ (! [A:($i > $o)]: ((eps @ (A)) = (eps @ (^ [B:$i]: ((? [C:$i]: (A @ C) & (B = (eps @ A))) | (~ (? [C:$i]: (A @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 6.34/2.21 thf(5,plain,((~ ((eps @ (sk1)) = (eps @ (^ [A:$i]: ((? [B:$i]: (sk1 @ B) & (A = (eps @ sk1))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false)))))))))))),inference(cnf,[status(esa)],[4])).
% 6.34/2.21 thf(6,plain,(((eps @ (^ [A:$i]: ((? [B:$i]: (sk1 @ B) & (A = (eps @ sk1))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false))))))))) != (eps @ (sk1)))),inference(lifteq,[status(thm)],[5])).
% 6.34/2.21 thf(11,axiom,((? [A:(($i > $o) > $i)]: ! [B:($i > $o)]: ((? [C:$i]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 6.34/2.21 thf(13,plain,(! [A:$i] : ((~ ((? [B:$i]: (sk1 @ B) & (A = (eps @ (sk1)))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false)))))))) | ((? [B:$i]: (sk1 @ B) & ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (sk1)))) | (~ (? [B:$i]: (sk1 @ B)) & ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (^ [B:$i]: (($false))))))))),inference(choice,[status(esa)],[11])).
% 6.34/2.21 thf(15,plain,(! [C:$i,B:$i,A:$i] : (((~ (sk1 @ B) | ~ (A = (eps @ (sk1))) | (sk1 @ (sk3 @ B @ A)) | ~ (sk1 @ C)) & (~ (sk1 @ B) | ~ (A = (eps @ (sk1))) | (sk1 @ (sk3 @ B @ A)) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (^ [D:$i]: (($false)))))) & (~ (sk1 @ B) | ~ (A = (eps @ (sk1))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | ~ (sk1 @ C)) & (~ (sk1 @ B) | ~ (A = (eps @ (sk1))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (^ [D:$i]: (($false)))))) & ((sk1 @ (sk2 @ A)) | ~ (A = (eps @ (^ [D:$i]: (($false))))) | (sk1 @ (sk3 @ B @ A)) | ~ (sk1 @ C)) & ((sk1 @ (sk2 @ A)) | ~ (A = (eps @ (^ [D:$i]: (($false))))) | (sk1 @ (sk3 @ B @ A)) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (^ [D:$i]: (($false)))))) & ((sk1 @ (sk2 @ A)) | ~ (A = (eps @ (^ [D:$i]: (($false))))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | ~ (sk1 @ C)) & ((sk1 @ (sk2 @ A)) | ~ (A = (eps @ (^ [D:$i]: (($false))))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (^ [D:$i]: (($false))))))))),inference(cnf,[status(esa)],[13])).
% 6.34/2.21 thf(21,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk1 @ B)) | (~ (A = (eps @ (sk1)))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | (~ (sk1 @ C)))),inference(cnfConj,[status(thm)],[15])).
% 6.34/2.21 thf(26,plain,(! [C:$i,B:$i,A:$i] : ((A != (eps @ (sk1))) | ((eps @ (^ [D:$i]: ((? [E:$i]: (sk1 @ E) & (D = (eps @ sk1))) | (~ (? [E:$i]: (sk1 @ E)) & (D = (eps @ (^ [E:$i]: (($false))))))))) = (eps @ (sk1))) | (~ (sk1 @ B)) | (~ (sk1 @ C)))),inference(lifteq,[status(thm)],[21])).
% 6.34/2.21 thf(27,plain,(! [B:$i,A:$i] : (((eps @ (^ [C:$i]: ((? [D:$i]: (sk1 @ D) & (C = (eps @ sk1))) | (~ (? [D:$i]: (sk1 @ D)) & (C = (eps @ (^ [D:$i]: (($false))))))))) = (eps @ (sk1))) | (~ (sk1 @ A)) | (~ (sk1 @ B)))),inference(simp,[status(thm)],[26])).
% 6.34/2.21 thf(473,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A)) | (~ (sk1 @ B)))),inference(simplifyReflect,[status(thm)],[27,6])).
% 6.34/2.21 thf(492,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A)) | ((sk1 @ B) != (sk1 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[473])).
% 6.34/2.21 thf(493,plain,(! [A:$i] : ((~ (sk1 @ A)))),inference(pattern_uni,[status(thm)],[492:[bind(A, $thf(B))]])).
% 6.34/2.21 thf(497,plain,(! [A:$i] : ((~ (sk1 @ A)))),inference(simp,[status(thm)],[493])).
% 6.34/2.21 thf(501,plain,(((eps @ (^ [A:$i]: ((? [B:$i]: (($false)) & (A = (eps @ (^ [B:$i]: (($false)))))) | (~ (? [B:$i]: (($false))) & (A = (eps @ (^ [B:$i]: (($false))))))))) != (eps @ (^ [A:$i]: (($false)))))),inference(rewrite,[status(thm)],[6,497])).
% 6.34/2.21 thf(502,plain,(((eps @ (^ [A:$i]: (A = (eps @ (^ [B:$i]: (($false))))))) != (eps @ (^ [A:$i]: (($false)))))),inference(simp,[status(thm)],[501])).
% 6.34/2.21 thf(10,plain,(((^ [A:$i]: ((? [B:$i]: (sk1 @ B) & (A = (eps @ sk1))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false)))))))) != (sk1))),inference(simp,[status(thm)],[6])).
% 6.34/2.21 thf(40,plain,((((? [A:$i]: (sk1 @ A) & (sk4 = (eps @ (sk1)))) | (~ (? [A:$i]: (sk1 @ A)) & (sk4 = (eps @ (^ [A:$i]: (($false))))))) != (sk1 @ sk4))),inference(func_ext,[status(esa)],[10])).
% 6.34/2.21 thf(42,plain,(((? [A:$i]: (sk1 @ A) & (sk4 = (eps @ (sk1)))) | (~ (? [A:$i]: (sk1 @ A)) & (sk4 = (eps @ (^ [A:$i]: (($false))))))) | (sk1 @ sk4)),inference(bool_ext,[status(thm)],[40])).
% 6.34/2.21 thf(48,plain,(! [A:$i] : ((((sk1 @ sk6) | ~ (sk1 @ A) | (sk1 @ sk4)) & ((sk1 @ sk6) | (sk4 = (eps @ (^ [B:$i]: (($false))))) | (sk1 @ sk4)) & ((sk4 = (eps @ (sk1))) | ~ (sk1 @ A) | (sk1 @ sk4)) & ((sk4 = (eps @ (sk1))) | (sk4 = (eps @ (^ [B:$i]: (($false))))) | (sk1 @ sk4))))),inference(cnf,[status(esa)],[42])).
% 6.34/2.21 thf(52,plain,((sk4 = (eps @ (sk1))) | (sk4 = (eps @ (^ [A:$i]: (($false))))) | (sk1 @ sk4)),inference(cnfConj,[status(thm)],[48])).
% 6.34/2.21 thf(55,plain,(((eps @ (sk1)) = sk4) | ((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4)),inference(lifteq,[status(thm)],[52])).
% 6.34/2.21 thf(50,plain,((sk1 @ sk6) | (sk4 = (eps @ (^ [A:$i]: (($false))))) | (sk1 @ sk4)),inference(cnfConj,[status(thm)],[48])).
% 6.34/2.21 thf(53,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk6) | (sk1 @ sk4)),inference(lifteq,[status(thm)],[50])).
% 6.34/2.21 thf(12,plain,(! [A:$i] : ((~ (sk1 @ A)) | (sk1 @ (eps @ (sk1))))),inference(choice,[status(esa)],[11])).
% 6.34/2.21 thf(81,plain,(! [A:$i] : (((eps @ (^ [B:$i]: (($false)))) = sk4) | (sk1 @ sk4) | ~ (($true)) | (sk1 @ (eps @ (sk1))) | ((sk1 @ sk6) != (sk1 @ A)))),inference(paramod_ordered,[status(thm)],[53,12])).
% 6.34/2.21 thf(82,plain,(! [A:$i] : (((eps @ (^ [B:$i]: (($false)))) = sk4) | (sk1 @ sk4) | (sk1 @ (eps @ (sk1))) | ((sk1 @ sk6) != (sk1 @ A)))),inference(simp,[status(thm)],[81])).
% 6.34/2.21 thf(83,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4) | (sk1 @ (eps @ (sk1)))),inference(pattern_uni,[status(thm)],[82:[bind(A, $thf(sk6))]])).
% 6.34/2.21 thf(403,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4) | ((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4) | (sk1 @ sk4) | ((eps @ (sk1)) != (eps @ (sk1)))),inference(paramod_ordered,[status(thm)],[55,83])).
% 6.34/2.22 thf(404,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4) | ((eps @ (sk1)) != (eps @ (sk1)))),inference(simp,[status(thm)],[403])).
% 6.34/2.22 thf(405,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | (sk1 @ sk4)),inference(pattern_uni,[status(thm)],[404:[]])).
% 6.34/2.22 thf(505,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4) | ($false)),inference(rewrite,[status(thm)],[405,497])).
% 6.34/2.22 thf(506,plain,(((eps @ (^ [A:$i]: (($false)))) = sk4)),inference(simp,[status(thm)],[505])).
% 6.34/2.22 thf(513,plain,(((eps @ (^ [A:$i]: (A = sk4))) != sk4)),inference(rewrite,[status(thm)],[502,506])).
% 6.34/2.22 thf(17,plain,(! [A:$i] : ((sk1 @ (sk2 @ A)) | (~ (A = (eps @ (^ [B:$i]: (($false)))))) | ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (sk1))) | ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (^ [B:$i]: (($false))))))),inference(cnfConj,[status(thm)],[15])).
% 6.34/2.22 thf(28,plain,(! [A:$i] : ((A != (eps @ (^ [B:$i]: (($false))))) | ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (sk1))) | ((eps @ (^ [B:$i]: ((? [C:$i]: (sk1 @ C) & (B = (eps @ sk1))) | (~ (? [C:$i]: (sk1 @ C)) & (B = (eps @ (^ [C:$i]: (($false))))))))) = (eps @ (^ [B:$i]: (($false))))) | (sk1 @ (sk2 @ A)))),inference(lifteq,[status(thm)],[17])).
% 6.34/2.22 thf(29,plain,(((eps @ (^ [A:$i]: ((? [B:$i]: (sk1 @ B) & (A = (eps @ sk1))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false))))))))) = (eps @ (sk1))) | ((eps @ (^ [A:$i]: ((? [B:$i]: (sk1 @ B) & (A = (eps @ sk1))) | (~ (? [B:$i]: (sk1 @ B)) & (A = (eps @ (^ [B:$i]: (($false))))))))) = (eps @ (^ [A:$i]: (($false))))) | (sk1 @ (sk2 @ (eps @ (^ [A:$i]: (($false))))))),inference(simp,[status(thm)],[28])).
% 6.34/2.22 thf(525,plain,(((eps @ (^ [A:$i]: ((? [B:$i]: (($false)) & (A = (eps @ (^ [B:$i]: (($false)))))) | (~ (? [B:$i]: (($false))) & (A = sk4))))) = (eps @ (^ [A:$i]: (($false))))) | ((eps @ (^ [A:$i]: ((? [B:$i]: (($false)) & (A = (eps @ (^ [B:$i]: (($false)))))) | (~ (? [B:$i]: (($false))) & (A = sk4))))) = sk4) | ($false)),inference(rewrite,[status(thm)],[29,497,506])).
% 6.34/2.22 thf(526,plain,(((eps @ (^ [A:$i]: (A = sk4))) = (eps @ (^ [A:$i]: (($false))))) | ((eps @ (^ [A:$i]: (A = sk4))) = sk4)),inference(simp,[status(thm)],[525])).
% 6.34/2.22 thf(527,plain,(((eps @ (^ [A:$i]: (A = sk4))) = (eps @ (^ [A:$i]: (($false)))))),inference(simplifyReflect,[status(thm)],[526,513])).
% 6.34/2.22 thf(528,plain,(((eps @ (^ [A:$i]: (($false)))) != sk4)),inference(rewrite,[status(thm)],[513,527])).
% 6.34/2.22 thf(533,plain,((sk4 != sk4)),inference(rewrite,[status(thm)],[528,506])).
% 6.34/2.22 thf(534,plain,(($false)),inference(simp,[status(thm)],[533])).
% 6.34/2.22 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.34/2.22 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------