%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV382^5 : 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 : n006.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:37:12 AM UTC 2026
% Result : Theorem 9.36s 4.14s
% Output : Refutation 9.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV382^5 : 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.10/0.22 % Computer : n006.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 15:43:09 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 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.07/0.89 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.69/1.14 % [INFO] Parsing done (247ms).
% 1.69/1.16 % [INFO] Running in sequential loop mode.
% 2.35/1.65 % [INFO] eprover registered as external prover.
% 2.35/1.66 % [INFO] Scanning for conjecture ...
% 2.59/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.59/1.79 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.59/1.79 % [INFO] Problem is higher-order (TPTP THF).
% 2.77/1.80 % [INFO] Type checking passed.
% 2.77/1.81 % [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 ...
% 9.36/4.14 % External prover 'e' found a proof!
% 9.36/4.14 % [INFO] Killing All external provers ...
% 9.36/4.14 % Time passed: 3763ms (effective reasoning time: 2967ms)
% 9.36/4.14 % 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)>
% 9.36/4.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 3763 ms resp. 2967 ms w/o parsing
% 9.97/4.24 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.97/4.24 thf(a_type, type, a: $tType).
% 9.97/4.24 thf(sk1_decl, type, sk1: (a > (a > $o))).
% 9.97/4.24 thf(sk2_decl, type, sk2: (a > $o)).
% 9.97/4.24 thf(sk3_decl, type, sk3: ((a > $o) > a)).
% 9.97/4.24 thf(sk4_decl, type, sk4: (a > a)).
% 9.97/4.24 thf(sk5_decl, type, sk5: a).
% 9.97/4.24 thf(sk1_def, definition, sk1 = (@+ [A:(a > (a > $o))]: ~ (! [B:(a > $o)]: ((! [C:(a > $o)]: ((? [D:a]: (C @ D)) => (? [D:a]: ((C @ D) & ! [E:a]: ((A @ E @ D) => (~ (C @ E)))))) & ! [C:a]: ((! [D:a]: ((A @ D @ C) => (B @ D))) => (B @ C))) => (! [C:a]: (B @ C))))) ).
% 9.97/4.24 thf(sk2_def, definition, sk2 = (@+ [A:(a > $o)]: ~ ((! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (? [C:a]: ((B @ C) & ! [D:a]: ((sk1 @ D @ C) => (~ (B @ D)))))) & ! [B:a]: ((! [C:a]: ((sk1 @ C @ B) => (A @ C))) => (A @ B))) => (! [B:a]: (A @ B)))) ).
% 9.97/4.24 thf(sk3_def, definition, sk3 = (^ [A:(a > $o)]: (@+ [B:a]: ((A @ B) & ! [C:a]: ((sk1 @ C @ B) => (~ (A @ C)))))) ).
% 9.97/4.24 thf(sk4_def, definition, sk4 = (^ [A:a]: (@+ [B:a]: ~ ((sk1 @ B @ A) => (sk2 @ B)))) ).
% 9.97/4.24 thf(sk5_def, definition, sk5 = (@+ [A:a]: ~ (sk2 @ A)) ).
% 9.97/4.24 thf(1,conjecture,((! [A:(a > (a > $o)),B:(a > $o)]: ((! [C:(a > $o)]: ((? [D:a]: (C @ D)) => (? [D:a]: ((C @ D) & ! [E:a]: ((A @ E @ D) => (~ (C @ E)))))) & ! [C:a]: ((! [D:a]: ((A @ D @ C) => (B @ D))) => (B @ C))) => (! [C:a]: (B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTRANS_IND)).
% 9.97/4.24 thf(2,negated_conjecture,((~ (! [A:(a > (a > $o)),B:(a > $o)]: ((! [C:(a > $o)]: ((? [D:a]: (C @ D)) => (? [D:a]: ((C @ D) & ! [E:a]: ((A @ E @ D) => (~ (C @ E)))))) & ! [C:a]: ((! [D:a]: ((A @ D @ C) => (B @ D))) => (B @ C))) => (! [C:a]: (B @ C)))))),inference(neg_conjecture,[status(cth)],[1])).
% 9.97/4.24 thf(3,plain,((~ (! [A:(a > (a > $o)),B:(a > $o)]: ((! [C:(a > $o)]: ((? [D:a]: (C @ D)) => (? [D:a]: ((C @ D) & ! [E:a]: ((A @ E @ D) => (~ (C @ E)))))) & ! [C:a]: ((! [D:a]: ((A @ D @ C) => (B @ D))) => (B @ C))) => (! [C:a]: (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 9.97/4.24 thf(4,plain,(! [D:a,C:a,B:a,A:(a > $o)] : (((~ (A @ B) | (A @ (sk3 @ (A)))) & (~ (A @ B) | ~ (sk1 @ C @ (sk3 @ (A))) | ~ (A @ C)) & ((sk1 @ (sk4 @ D) @ D) | (sk2 @ D)) & (~ (sk2 @ (sk4 @ D)) | (sk2 @ D)) & ~ (sk2 @ sk5)))),inference(cnf,[status(esa)],[3])).
% 9.97/4.24 thf(5,plain,(! [C:a,B:a,A:(a > $o)] : ((~ (A @ B)) | (~ (sk1 @ C @ (sk3 @ (A)))) | (~ (A @ C)))),inference(cnfConj,[status(thm)],[4])).
% 9.97/4.24 thf(7,plain,(! [A:a] : ((sk1 @ (sk4 @ A) @ A) | (sk2 @ A))),inference(cnfConj,[status(thm)],[4])).
% 9.97/4.24 thf(10,plain,(! [A:a] : ((sk1 @ (sk4 @ A) @ A) | (sk2 @ A))),inference(simp,[status(thm)],[7])).
% 9.97/4.24 thf(9,plain,((~ (sk2 @ sk5))),inference(cnfConj,[status(thm)],[4])).
% 9.97/4.24 thf(21,plain,(! [C:a,B:a,A:(a > $o)] : ((~ (A @ B)) | (~ (sk1 @ C @ (sk3 @ (A)))) | (~ (A @ C)) | (~ (A @ B)))),inference(eqfactor_ordered,[status(thm)],[5])).
% 9.97/4.24 thf(41,plain,(! [A:a] : (~ (($true)) | (~ (sk1 @ A @ (sk3 @ (^ [B:a]: (($true)))))))),inference(pre_uni,[status(thm)],[21:[bind(A, $thf(^ [D:a]: (($true))))]])).
% 9.97/4.24 thf(48,plain,(! [A:a] : ((~ (sk1 @ A @ (sk3 @ (^ [B:a]: (($true)))))))),inference(simp,[status(thm)],[41])).
% 9.97/4.24 thf(62,plain,(! [B:a,A:a] : ((sk2 @ A) | ~ (($true)) | ((sk1 @ (sk4 @ A) @ A) != (sk1 @ B @ (sk3 @ (^ [C:a]: (($true)))))))),inference(paramod_ordered,[status(thm)],[10,48])).
% 9.97/4.24 thf(63,plain,(! [B:a,A:a] : ((sk2 @ A) | ((sk1 @ (sk4 @ A) @ A) != (sk1 @ B @ (sk3 @ (^ [C:a]: (($true)))))))),inference(simp,[status(thm)],[62])).
% 9.97/4.24 thf(64,plain,((sk2 @ (sk3 @ (^ [A:a]: (($true)))))),inference(pattern_uni,[status(thm)],[63:[bind(A, $thf(sk3 @ (^ [C:a]: (($true))))),bind(B, $thf(sk4 @ (sk3 @ (^ [C:a]: (($true))))))]])).
% 9.97/4.24 thf(27,axiom,((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 9.97/4.24 thf(90,plain,(! [A:a] : ((~ (sk2 @ A)) | (sk2 @ (sk3 @ (sk2))))),inference(choice,[status(esa)],[27])).
% 9.97/4.24 thf(103,plain,(! [A:a] : (~ (($true)) | (sk2 @ (sk3 @ (sk2))) | ((sk2 @ (sk3 @ (^ [B:a]: (($true))))) != (sk2 @ A)))),inference(paramod_ordered,[status(thm)],[64,90])).
% 9.97/4.24 thf(104,plain,(! [A:a] : ((sk2 @ (sk3 @ (sk2))) | ((sk2 @ (sk3 @ (^ [B:a]: (($true))))) != (sk2 @ A)))),inference(simp,[status(thm)],[103])).
% 9.97/4.24 thf(105,plain,((sk2 @ (sk3 @ (sk2)))),inference(pattern_uni,[status(thm)],[104:[bind(A, $thf(sk3 @ (^ [B:a]: (($true)))))]])).
% 9.97/4.24 thf(8,plain,(! [A:a] : ((~ (sk2 @ (sk4 @ A))) | (sk2 @ A))),inference(cnfConj,[status(thm)],[4])).
% 9.97/4.24 thf(11,plain,(! [A:a] : ((~ (sk2 @ (sk4 @ A))) | (sk2 @ A))),inference(simp,[status(thm)],[8])).
% 9.97/4.24 thf(23,plain,(! [C:(a > $o),B:a,A:a] : ((~ (~ (C @ A))) | (~ (sk1 @ B @ (sk3 @ (^ [D:a]: ~ (C @ D))))) | (~ (~ (C @ B))))),inference(prim_subst,[status(thm)],[5:[bind(A, $thf(^ [E:a]: ~ (D @ E)))]])).
% 9.97/4.24 thf(50,plain,(! [C:(a > $o),B:a,A:a] : ((C @ A) | (~ (sk1 @ B @ (sk3 @ (^ [D:a]: ~ (C @ D))))) | (C @ B))),inference(cnf,[status(esa)],[23])).
% 9.97/4.24 thf(51,plain,(! [C:(a > $o),B:a,A:a] : ((C @ A) | (~ (sk1 @ B @ (sk3 @ (^ [D:a]: ~ (C @ D))))) | (C @ B))),inference(simp,[status(thm)],[50])).
% 9.97/4.24 thf(71,plain,(~ (($true)) | ((sk2 @ (sk3 @ (^ [A:a]: (($true))))) != (sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[64,9])).
% 9.97/4.24 thf(72,plain,(((sk2 @ (sk3 @ (^ [A:a]: (($true))))) != (sk2 @ sk5))),inference(simp,[status(thm)],[71])).
% 9.97/4.24 thf(79,plain,(((sk3 @ (^ [A:a]: (($true)))) != sk5)),inference(simp,[status(thm)],[72])).
% 9.97/4.24 thf(69,plain,(! [C:a,B:a,A:(a > $o)] : ((~ (A @ B)) | (~ (sk1 @ C @ (sk3 @ (A)))) | ~ (($true)) | ((sk2 @ (sk3 @ (^ [D:a]: (($true))))) != (A @ C)))),inference(paramod_ordered,[status(thm)],[64,5])).
% 9.97/4.24 thf(70,plain,(! [C:a,B:a,A:(a > $o)] : ((~ (A @ B)) | (~ (sk1 @ C @ (sk3 @ (A)))) | ((sk2 @ (sk3 @ (^ [D:a]: (($true))))) != (A @ C)))),inference(simp,[status(thm)],[69])).
% 9.97/4.24 thf(77,plain,(! [A:a] : ((~ (sk2 @ A)) | (~ (sk1 @ (sk3 @ (^ [B:a]: (($true)))) @ (sk3 @ (sk2)))))),inference(pre_uni,[status(thm)],[70:[bind(A, $thf(sk2)),bind(B, $thf(B)),bind(C, $thf(sk3 @ (^ [D:a]: (($true)))))]])).
% 9.97/4.24 thf(83,plain,(! [A:a] : ((~ (sk2 @ A)) | (~ (sk1 @ (sk3 @ (^ [B:a]: (($true)))) @ (sk3 @ (sk2)))))),inference(simp,[status(thm)],[77])).
% 9.97/4.24 thf(87,plain,(! [A:a] : (~ (($true)) | (~ (sk1 @ (sk3 @ (^ [B:a]: (($true)))) @ (sk3 @ (sk2)))) | ((sk2 @ (sk3 @ (^ [B:a]: (($true))))) != (sk2 @ A)))),inference(paramod_ordered,[status(thm)],[64,83])).
% 9.97/4.24 thf(88,plain,(! [A:a] : ((~ (sk1 @ (sk3 @ (^ [B:a]: (($true)))) @ (sk3 @ (sk2)))) | ((sk2 @ (sk3 @ (^ [B:a]: (($true))))) != (sk2 @ A)))),inference(simp,[status(thm)],[87])).
% 9.97/4.24 thf(89,plain,((~ (sk1 @ (sk3 @ (^ [A:a]: (($true)))) @ (sk3 @ (sk2))))),inference(pattern_uni,[status(thm)],[88:[bind(A, $thf(sk3 @ (^ [B:a]: (($true)))))]])).
% 9.97/4.24 thf(125,plain,(~ (($true)) | ((sk2 @ (sk3 @ (sk2))) != (sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[105,9])).
% 9.97/4.24 thf(126,plain,(((sk2 @ (sk3 @ (sk2))) != (sk2 @ sk5))),inference(simp,[status(thm)],[125])).
% 9.97/4.24 thf(133,plain,(((sk3 @ (sk2)) != sk5)),inference(simp,[status(thm)],[126])).
% 9.97/4.24 thf(73,plain,(! [A:a] : (~ (($true)) | (sk2 @ A) | ((sk2 @ (sk4 @ A)) != (sk2 @ (sk3 @ (^ [B:a]: (($true)))))))),inference(paramod_ordered,[status(thm)],[64,11])).
% 9.97/4.24 thf(74,plain,(! [A:a] : ((sk2 @ A) | ((sk2 @ (sk4 @ A)) != (sk2 @ (sk3 @ (^ [B:a]: (($true)))))))),inference(simp,[status(thm)],[73])).
% 9.97/4.24 thf(80,plain,(! [A:a] : ((sk2 @ A) | ((sk4 @ A) != (sk3 @ (^ [B:a]: (($true))))))),inference(simp,[status(thm)],[74])).
% 9.97/4.24 thf(354,plain,(($false)),inference(e,[status(thm)],[5,10,9,105,64,48,11,51,79,89,133,3,80])).
% 9.97/4.24 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.97/4.24 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------