%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO542^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:05 AM UTC 2026
% Result : Theorem 3.02s 1.45s
% Output : Refutation 3.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO542^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 : n009.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.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Tue Sep 29 17:14:00 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.67/0.54 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.04/0.64 % [INFO] Parsing done (102ms).
% 1.04/0.65 % [INFO] Running in sequential loop mode.
% 1.34/0.85 % [INFO] eprover registered as external prover.
% 1.34/0.86 % [INFO] Scanning for conjecture ...
% 1.59/0.91 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 1.59/0.93 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 1.59/0.93 % [INFO] Problem is higher-order (TPTP THF).
% 1.59/0.93 % [INFO] Type checking passed.
% 1.59/0.94 % [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 ...
% 3.02/1.44 % [INFO] Killing All external provers ...
% 3.02/1.45 % Time passed: 1135ms (effective reasoning time: 789ms)
% 3.02/1.45 % 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)>
% 3.02/1.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 1135 ms resp. 789 ms w/o parsing
% 3.40/1.51 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.40/1.51 thf(epsii_decl, type, epsii: ((($i > $i) > $o) > ($i > $i))).
% 3.40/1.51 thf(if_decl, type, if: ($o > (($i > $i) > (($i > $i) > ($i > $i))))).
% 3.40/1.51 thf(sk1_decl, type, sk1: $o).
% 3.40/1.51 thf(sk2_decl, type, sk2: ($i > $i)).
% 3.40/1.51 thf(sk3_decl, type, sk3: ($i > $i)).
% 3.40/1.51 thf(if_def, definition, if = (^ [A:$o,B:($i > $i),C:($i > $i)]: (epsii @ (^ [D:($i > $i)]: (((A) & (D = B)) | (~ (A) & (D = C)))))) ).
% 3.40/1.51 thf(sk1_def, definition, sk1 = (@+ [A:$o]: ~ (! [B:($i > $i),C:($i > $i)]: (((epsii @ (^ [D:($i > $i)]: (((A) & (D = B)) | (~ (A) & (D = C))))) = (B)) | ((epsii @ (^ [D:($i > $i)]: (((A) & (D = B)) | (~ (A) & (D = C))))) = (C))))) ).
% 3.40/1.51 thf(sk2_def, definition, sk2 = (@+ [A:($i > $i)]: ~ (! [B:($i > $i)]: (((epsii @ (^ [C:($i > $i)]: (((sk1) & (C = A)) | (~ (sk1) & (C = B))))) = (A)) | ((epsii @ (^ [C:($i > $i)]: (((sk1) & (C = A)) | (~ (sk1) & (C = B))))) = (B))))) ).
% 3.40/1.51 thf(sk3_def, definition, sk3 = (@+ [A:($i > $i)]: ~ (((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = A))))) = (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = A))))) = (A)))) ).
% 3.40/1.51 thf(1,conjecture,((! [A:$o,B:($i > $i),C:($i > $i)]: (((if @ A @ B @ C) = B) | ((if @ A @ B @ C) = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 3.40/1.51 thf(2,negated_conjecture,((~ (! [A:$o,B:($i > $i),C:($i > $i)]: (((if @ A @ B @ C) = B) | ((if @ A @ B @ C) = C))))),inference(neg_conjecture,[status(cth)],[1])).
% 3.40/1.51 thf(4,plain,((~ (! [A:$o,B:($i > $i),C:($i > $i)]: (((epsii @ (^ [D:($i > $i)]: (((A) & (D = B)) | (~ (A) & (D = C))))) = (B)) | ((epsii @ (^ [D:($i > $i)]: (((A) & (D = B)) | (~ (A) & (D = C))))) = (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 3.40/1.51 thf(5,plain,((~ ((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk2)) & ~ ((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk3)))),inference(cnf,[status(esa)],[4])).
% 3.40/1.51 thf(7,plain,((~ ((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk3)))),inference(cnfConj,[status(thm)],[5])).
% 3.40/1.51 thf(9,plain,(((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (sk3))),inference(lifteq,[status(thm)],[7])).
% 3.40/1.51 thf(15,axiom,((? [A:((($i > $i) > $o) > ($i > $i))]: ! [B:(($i > $i) > $o)]: ((? [C:($i > $i)]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 3.40/1.51 thf(16,plain,(! [A:($i > $i)] : ((~ (((sk1) & ((A) = (sk2))) | (~ (sk1) & ((A) = (sk3))))) | (((sk1) & ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2))) | (~ (sk1) & ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3)))))),inference(choice,[status(esa)],[15])).
% 3.40/1.51 thf(17,plain,(! [A:($i > $i)] : (((~ (sk1) | ~ ((A) = (sk2)) | (sk1) | ~ (sk1)) & (~ (sk1) | ~ ((A) = (sk2)) | (sk1) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3))) & (~ (sk1) | ~ ((A) = (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ~ (sk1)) & (~ (sk1) | ~ ((A) = (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3))) & ((sk1) | ~ ((A) = (sk3)) | (sk1) | ~ (sk1)) & ((sk1) | ~ ((A) = (sk3)) | (sk1) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3))) & ((sk1) | ~ ((A) = (sk3)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ~ (sk1)) & ((sk1) | ~ ((A) = (sk3)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3)))))),inference(cnf,[status(esa)],[16])).
% 3.40/1.51 thf(23,plain,(! [A:($i > $i)] : (~ (sk1) | (~ ((A) = (sk2))) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ~ (sk1))),inference(cnfConj,[status(thm)],[17])).
% 3.40/1.51 thf(34,plain,(! [A:($i > $i)] : (((A) != (sk2)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk2)) | ~ (sk1) | ~ (sk1))),inference(lifteq,[status(thm)],[23])).
% 3.40/1.51 thf(35,plain,(((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk2)) | ~ (sk1)),inference(simp,[status(thm)],[34])).
% 3.40/1.51 thf(6,plain,((~ ((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk2)))),inference(cnfConj,[status(thm)],[5])).
% 3.40/1.51 thf(8,plain,(((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) != (sk2))),inference(lifteq,[status(thm)],[6])).
% 3.40/1.51 thf(42,plain,(~ (sk1)),inference(simplifyReflect,[status(thm)],[35,8])).
% 3.40/1.51 thf(45,plain,(((epsii @ (^ [A:($i > $i)]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))) != (sk3))),inference(rewrite,[status(thm)],[9,42])).
% 3.40/1.51 thf(46,plain,(((epsii @ (^ [A:($i > $i)]: (A = sk3))) != (sk3))),inference(simp,[status(thm)],[45])).
% 3.40/1.51 thf(18,plain,(! [A:($i > $i)] : (sk1 | (~ ((A) = (sk3))) | sk1 | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3)))),inference(cnfConj,[status(thm)],[17])).
% 3.40/1.51 thf(32,plain,(! [A:($i > $i)] : (((A) != (sk3)) | ((epsii @ (^ [B:($i > $i)]: (((sk1) & (B = sk2)) | (~ (sk1) & (B = sk3))))) = (sk3)) | sk1 | sk1)),inference(lifteq,[status(thm)],[18])).
% 3.40/1.51 thf(33,plain,(((epsii @ (^ [A:($i > $i)]: (((sk1) & (A = sk2)) | (~ (sk1) & (A = sk3))))) = (sk3)) | sk1),inference(simp,[status(thm)],[32])).
% 3.40/1.51 thf(52,plain,(((epsii @ (^ [A:($i > $i)]: (((($false)) & (A = sk2)) | (~ (($false)) & (A = sk3))))) = (sk3)) | ($false)),inference(rewrite,[status(thm)],[33,42])).
% 3.40/1.51 thf(53,plain,(((epsii @ (^ [A:($i > $i)]: (A = sk3))) = (sk3))),inference(simp,[status(thm)],[52])).
% 3.40/1.51 thf(57,plain,(((sk3) != (sk3))),inference(rewrite,[status(thm)],[46,53])).
% 3.40/1.51 thf(58,plain,(($false)),inference(simp,[status(thm)],[57])).
% 3.40/1.51 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.40/1.51 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------