%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO555^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 : n009.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.18s 2.82s
% Output : Refutation 6.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO555^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08 % 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 : n009.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:14:45 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.86/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.17/0.99 % [INFO] Parsing done (191ms).
% 1.17/1.00 % [INFO] Running in sequential loop mode.
% 1.94/1.41 % [INFO] eprover registered as external prover.
% 1.94/1.42 % [INFO] Scanning for conjecture ...
% 2.12/1.52 % [INFO] Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ...
% 2.12/1.55 % [INFO] Axiom selection finished. Selected 2 axioms (removed 0 axioms).
% 2.12/1.56 % [INFO] Problem is higher-order (TPTP THF).
% 2.12/1.56 % [INFO] Type checking passed.
% 2.12/1.57 % [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.18/2.81 % [INFO] Killing All external provers ...
% 6.18/2.81 % Time passed: 2454ms (effective reasoning time: 1800ms)
% 6.18/2.81 % 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.18/2.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 2454 ms resp. 1800 ms w/o parsing
% 6.18/2.89 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.18/2.89 thf(eps1_decl, type, eps1: (($i > $o) > $i)).
% 6.18/2.89 thf(if1_decl, type, if1: ($o > ($i > ($i > $i)))).
% 6.18/2.89 thf(eps2_decl, type, eps2: (($i > $o) > $i)).
% 6.18/2.89 thf(if2_decl, type, if2: ($o > ($i > ($i > $i)))).
% 6.18/2.89 thf(sk1_decl, type, sk1: $o).
% 6.18/2.89 thf(sk2_decl, type, sk2: $i).
% 6.18/2.89 thf(sk3_decl, type, sk3: $i).
% 6.18/2.89 thf(if1_def, definition, if1 = (^ [A:$o,B:$i,C:$i]: (eps1 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))) ).
% 6.18/2.89 thf(if2_def, definition, if2 = (^ [A:$o,B:$i,C:$i]: (eps2 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))) ).
% 6.18/2.89 thf(1,conjecture,((if1 = if2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 6.18/2.89 thf(2,negated_conjecture,((~ (if1 = if2))),inference(neg_conjecture,[status(cth)],[1])).
% 6.18/2.89 thf(5,plain,((~ ((^ [A:$o,B:$i,C:$i]: (eps1 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))) = (^ [A:$o,B:$i,C:$i]: (eps2 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 6.18/2.89 thf(6,plain,(((^ [A:$o,B:$i,C:$i]: (eps2 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))) != (^ [A:$o,B:$i,C:$i]: (eps1 @ (^ [D:$i]: (((A) & (D = B)) | (~ (A) & (D = C)))))))),inference(lifteq,[status(thm)],[5])).
% 6.18/2.89 thf(13,plain,(((eps2 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))))),inference(func_ext,[status(esa)],[6])).
% 6.18/2.89 thf(14,axiom,((? [A:(($i > $o) > $i)]: ! [B:($i > $o)]: ((? [C:$i]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 6.18/2.89 thf(15,plain,(! [A:$i] : ((~ (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3)))) | (((sk1) & ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2)) | (~ (sk1) & ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))))),inference(choice,[status(esa)],[14])).
% 6.18/2.89 thf(42,plain,(! [A:$i] : (((~ (sk1) | ~ (A = sk2) | (sk1) | ~ (sk1)) & (~ (sk1) | ~ (A = sk2) | (sk1) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & (~ (sk1) | ~ (A = sk2) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1)) & (~ (sk1) | ~ (A = sk2) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & ((sk1) | ~ (A = sk3) | (sk1) | ~ (sk1)) & ((sk1) | ~ (A = sk3) | (sk1) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & ((sk1) | ~ (A = sk3) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1)) & ((sk1) | ~ (A = sk3) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))))),inference(cnf,[status(esa)],[15])).
% 6.18/2.89 thf(50,plain,(! [A:$i] : (~ (sk1) | (~ (A = sk2)) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1))),inference(cnfConj,[status(thm)],[42])).
% 6.18/2.89 thf(61,plain,(! [A:$i] : ((A != sk2) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1) | ~ (sk1))),inference(lifteq,[status(thm)],[50])).
% 6.18/2.89 thf(62,plain,(((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = sk2) | ~ (sk1)),inference(simp,[status(thm)],[61])).
% 6.18/2.89 thf(16,plain,(! [A:$i] : ((~ (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3)))) | (((sk1) & ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2)) | (~ (sk1) & ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))))),inference(choice,[status(esa)],[14])).
% 6.18/2.89 thf(17,plain,(! [A:$i] : (((~ (sk1) | ~ (A = sk2) | (sk1) | ~ (sk1)) & (~ (sk1) | ~ (A = sk2) | (sk1) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & (~ (sk1) | ~ (A = sk2) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1)) & (~ (sk1) | ~ (A = sk2) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & ((sk1) | ~ (A = sk3) | (sk1) | ~ (sk1)) & ((sk1) | ~ (A = sk3) | (sk1) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3)) & ((sk1) | ~ (A = sk3) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1)) & ((sk1) | ~ (A = sk3) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))))),inference(cnf,[status(esa)],[16])).
% 6.18/2.89 thf(24,plain,(! [A:$i] : (~ (sk1) | (~ (A = sk2)) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1))),inference(cnfConj,[status(thm)],[17])).
% 6.18/2.89 thf(38,plain,(! [A:$i] : ((A != sk2) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk2) | ~ (sk1) | ~ (sk1))),inference(lifteq,[status(thm)],[24])).
% 6.18/2.89 thf(39,plain,(((eps2 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = sk2) | ~ (sk1)),inference(simp,[status(thm)],[38])).
% 6.18/2.89 thf(67,plain,(~ (sk1) | ((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != sk2) | ((eps2 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (eps2 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))))),inference(paramod_ordered,[status(thm)],[39,13])).
% 6.18/2.89 thf(68,plain,(~ (sk1) | ((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != sk2)),inference(pattern_uni,[status(thm)],[67:[]])).
% 6.18/2.89 thf(75,plain,(~ (sk1) | ~ (sk1) | (sk2 != sk2) | ((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))))),inference(paramod_ordered,[status(thm)],[62,68])).
% 6.18/2.89 thf(76,plain,(~ (sk1) | ((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))))),inference(simp,[status(thm)],[75])).
% 6.18/2.89 thf(77,plain,(~ (sk1)),inference(pattern_uni,[status(thm)],[76:[]])).
% 6.18/2.89 thf(88,plain,(((eps2 @ (^ [A:$i]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))) != (eps1 @ (^ [A:$i]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))))),inference(rewrite,[status(thm)],[13,77])).
% 6.18/2.89 thf(89,plain,(((eps2 @ (^ [A:$i]: (A = sk3))) != (eps1 @ (^ [A:$i]: (A = sk3))))),inference(simp,[status(thm)],[88])).
% 6.18/2.89 thf(43,plain,(! [A:$i] : (sk1 | (~ (A = sk3)) | sk1 | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))),inference(cnfConj,[status(thm)],[42])).
% 6.18/2.89 thf(63,plain,(! [A:$i] : ((A != sk3) | ((eps1 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3) | sk1 | sk1)),inference(lifteq,[status(thm)],[43])).
% 6.18/2.89 thf(64,plain,(((eps1 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = sk3) | sk1),inference(simp,[status(thm)],[63])).
% 6.18/2.89 thf(84,plain,(((eps1 @ (^ [A:$i]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))) = sk3) | ($false)),inference(rewrite,[status(thm)],[64,77])).
% 6.18/2.89 thf(85,plain,(((eps1 @ (^ [A:$i]: (A = sk3))) = sk3)),inference(simp,[status(thm)],[84])).
% 6.18/2.89 thf(98,plain,(((eps2 @ (^ [A:$i]: (A = sk3))) != sk3)),inference(rewrite,[status(thm)],[89,85])).
% 6.18/2.89 thf(25,plain,(! [A:$i] : (sk1 | (~ (A = sk3)) | sk1 | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3))),inference(cnfConj,[status(thm)],[17])).
% 6.18/2.89 thf(40,plain,(! [A:$i] : ((A != sk3) | ((eps2 @ (^ [B:$i]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = sk3) | sk1 | sk1)),inference(lifteq,[status(thm)],[25])).
% 6.18/2.89 thf(41,plain,(((eps2 @ (^ [A:$i]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = sk3) | sk1),inference(simp,[status(thm)],[40])).
% 6.18/2.89 thf(86,plain,(((eps2 @ (^ [A:$i]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))) = sk3) | ($false)),inference(rewrite,[status(thm)],[41,77])).
% 6.18/2.89 thf(87,plain,(((eps2 @ (^ [A:$i]: (A = sk3))) = sk3)),inference(simp,[status(thm)],[86])).
% 6.18/2.89 thf(103,plain,((sk3 != sk3)),inference(rewrite,[status(thm)],[98,87])).
% 6.18/2.89 thf(104,plain,(($false)),inference(simp,[status(thm)],[103])).
% 6.18/2.89 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.18/2.89 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------