%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU793^2 : TPTP v9.3.1. Released v3.7.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 : n008.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:29:19 AM UTC 2026
% Result : Theorem 21.32s 5.85s
% Output : Refutation 18.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU793^2 : TPTP v9.3.1. Released v3.7.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 : n008.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 14:30:54 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.84/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.15/0.98 % [INFO] Parsing done (185ms).
% 1.15/1.00 % [INFO] Running in sequential loop mode.
% 1.89/1.40 % [INFO] eprover registered as external prover.
% 1.89/1.41 % [INFO] Scanning for conjecture ...
% 2.05/1.52 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.05/1.55 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.05/1.55 % [INFO] Problem is higher-order (TPTP THF).
% 2.05/1.56 % [INFO] Type checking passed.
% 2.05/1.56 % [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 ...
% 21.32/5.85 % [INFO] Killing All external provers ...
% 21.32/5.85 % Time passed: 5493ms (effective reasoning time: 4846ms)
% 21.32/5.85 % 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)>
% 21.32/5.85 % Axioms used in derivation (0):
% 21.32/5.85 % No. of inferences in proof: 23
% 21.32/5.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5493 ms resp. 4846 ms w/o parsing
% 18.92/5.93 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.92/5.93 thf(in_decl, type, in: ($i > ($i > $o))).
% 18.92/5.93 thf(exu_decl, type, exu: (($i > $o) > $o)).
% 18.92/5.93 thf(replAx_decl, type, replAx: $o).
% 18.92/5.93 thf(sk1_decl, type, sk1: ($i > (($i > ($i > $o)) > $i))).
% 18.92/5.93 thf(sk2_decl, type, sk2: ($i > ($i > (($i > ($i > $o)) > $i)))).
% 18.92/5.93 thf(sk3_decl, type, sk3: ($i > (($i > ($i > $o)) > $i))).
% 18.92/5.93 thf(sk4_decl, type, sk4: $i).
% 18.92/5.93 thf(sk5_decl, type, sk5: ($i > $i)).
% 18.92/5.93 thf(sk6_decl, type, sk6: ($i > $i)).
% 18.92/5.93 thf(exu_def, definition, exu = (^ [A:($i > $o)]: ? [B:$i]: ((A @ B) & ! [C:$i]: ((A @ C) => (B = C)))) ).
% 18.92/5.93 thf(replAx_def, definition, replAx = (! [A:($i > ($i > $o)),B:$i]: ((! [C:$i]: ((in @ C @ B) => (exu @ (A @ C)))) => (? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D))))))) ).
% 18.92/5.93 thf(sk1_def, definition, sk1 = (^ [A:$i,B:($i > ($i > $o))]: (@+ [C:$i]: ~ ((in @ C @ A) => (? [D:$i]: ((B @ C @ D) & ! [E:$i]: ((B @ C @ E) => (D = E))))))) ).
% 18.92/5.93 thf(sk2_def, definition, sk2 = (^ [A:$i,B:$i,C:($i > ($i > $o))]: (@+ [D:$i]: ~ ((C @ (sk1 @ B @ C) @ D) => (A = D)))) ).
% 18.92/5.93 thf(sk3_def, definition, sk3 = (^ [A:$i,B:($i > ($i > $o))]: (@+ [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (B @ E @ D)))))) ).
% 18.92/5.93 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ (! [B:($i > $i)]: ? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (D = (B @ E))))))) ).
% 18.92/5.93 thf(sk5_def, definition, sk5 = (@+ [A:($i > $i)]: ~ (? [B:$i]: ! [C:$i]: ((in @ C @ B) = (? [D:$i]: ((in @ D @ sk4) & (C = (A @ D))))))) ).
% 18.92/5.93 thf(sk6_def, definition, sk6 = (^ [A:$i]: (@+ [B:$i]: ~ ((in @ B @ A) = (? [C:$i]: ((in @ C @ sk4) & (B = (sk5 @ C))))))) ).
% 18.92/5.93 thf(1,conjecture,(((replAx) => (! [A:$i,B:($i > $i)]: ? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (D = (B @ E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',image1Ex)).
% 18.92/5.93 thf(2,negated_conjecture,((~ ((replAx) => (! [A:$i,B:($i > $i)]: ? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (D = (B @ E))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 18.92/5.93 thf(3,plain,((~ ((! [A:($i > ($i > $o)),B:$i]: ((! [C:$i]: ((in @ C @ B) => (? [D:$i]: ((A @ C @ D) & ! [E:$i]: ((A @ C @ E) => (D = E)))))) => (? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D))))))) => (! [A:$i,B:($i > $i)]: ? [C:$i]: ! [D:$i]: ((in @ D @ C) = (? [E:$i]: ((in @ E @ A) & (D = (B @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 18.92/5.93 thf(4,plain,(! [E:$i,D:$i,C:$i,B:$i,A:($i > ($i > $o))] : ((((in @ (sk1 @ B @ (A)) @ B) | ((in @ D @ (sk3 @ B @ (A))) = (? [F:$i]: ((in @ F @ B) & (A @ F @ D))))) & (~ (A @ (sk1 @ B @ (A)) @ C) | (A @ (sk1 @ B @ (A)) @ (sk2 @ C @ B @ (A))) | ((in @ D @ (sk3 @ B @ (A))) = (? [F:$i]: ((in @ F @ B) & (A @ F @ D))))) & (~ (A @ (sk1 @ B @ (A)) @ C) | ~ (C = (sk2 @ C @ B @ (A))) | ((in @ D @ (sk3 @ B @ (A))) = (? [F:$i]: ((in @ F @ B) & (A @ F @ D))))) & ~ ((in @ (sk6 @ E) @ E) = (? [F:$i]: ((in @ F @ sk4) & ((sk6 @ E) = (sk5 @ F)))))))),inference(cnf,[status(esa)],[3])).
% 18.92/5.93 thf(6,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : ((~ (A @ (sk1 @ B @ (A)) @ C)) | (A @ (sk1 @ B @ (A)) @ (sk2 @ C @ B @ (A))) | ((in @ D @ (sk3 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))))),inference(cnfConj,[status(thm)],[4])).
% 18.92/5.93 thf(11,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((in @ D @ (sk3 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))) | (~ (A @ (sk1 @ B @ (A)) @ C)) | (A @ (sk1 @ B @ (A)) @ (sk2 @ C @ B @ (A))))),inference(lifteq,[status(thm)],[6])).
% 18.92/5.93 thf(8,plain,(! [A:$i] : ((~ ((in @ (sk6 @ A) @ A) = (? [B:$i]: ((in @ B @ sk4) & ((sk6 @ A) = (sk5 @ B)))))))),inference(cnfConj,[status(thm)],[4])).
% 18.92/5.93 thf(13,plain,(! [A:$i] : (((in @ (sk6 @ A) @ A) != (? [B:$i]: ((in @ B @ sk4) & ((sk6 @ A) = (sk5 @ B))))))),inference(lifteq,[status(thm)],[8])).
% 18.92/5.93 thf(14,plain,(! [A:$i] : (((in @ (sk6 @ A) @ A) != (? [B:$i]: ((in @ B @ sk4) & ((sk6 @ A) = (sk5 @ B))))))),inference(simp,[status(thm)],[13])).
% 18.92/5.93 thf(480,plain,(! [E:$i,D:$i,C:$i,B:$i,A:($i > ($i > $o))] : ((~ (A @ (sk1 @ B @ (A)) @ C)) | (A @ (sk1 @ B @ (A)) @ (sk2 @ C @ B @ (A))) | ((in @ D @ (sk3 @ B @ (A))) != (in @ (sk6 @ E) @ E)) | ((? [F:$i]: ((in @ F @ B) & (A @ F @ D))) != (? [F:$i]: ((in @ F @ sk4) & ((sk6 @ E) = (sk5 @ F))))))),inference(paramod_ordered,[status(thm)],[11,14])).
% 18.92/5.93 thf(556,plain,(! [C:$i,B:$i,A:$i] : ((~ (A = (sk5 @ (sk1 @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D))))))) | ((sk2 @ A @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D)))) = (sk5 @ (sk1 @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D)))))) | ((in @ (sk6 @ C) @ (sk3 @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D))))) != (in @ (sk6 @ B) @ B)) | ((^ [D:$i]: (C)) != (^ [D:$i]: (B))))),inference(pre_uni,[status(thm)],[480:[bind(A, $thf(^ [F:$i,G:$i]: (G = (sk5 @ F)))),bind(B, $thf(sk4)),bind(C, $thf(C)),bind(D, $thf(sk6 @ L)),bind(E, $thf(E))]])).
% 18.92/5.93 thf(557,plain,(! [A:$i] : (((sk2 @ A @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))) = (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))) | (~ (A = (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))))))),inference(pattern_uni,[status(thm)],[556:[bind(A, $thf(:)),bind(B, $thf(sk3 @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D))))),bind(C, $thf(sk3 @ sk4 @ (^ [D:$i,E:$i]: (E = (sk5 @ D)))))]])).
% 18.92/5.93 thf(675,plain,(! [A:$i] : (((sk2 @ A @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))) = (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))) | (A != (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))))),inference(lifteq,[status(thm)],[557])).
% 18.92/5.93 thf(676,plain,(((sk2 @ (sk5 @ (sk1 @ sk4 @ (^ [A:$i,B:$i]: (B = (sk5 @ A))))) @ sk4 @ (^ [A:$i,B:$i]: (B = (sk5 @ A)))) = (sk5 @ (sk1 @ sk4 @ (^ [A:$i,B:$i]: (B = (sk5 @ A))))))),inference(simp,[status(thm)],[675])).
% 18.92/5.93 thf(7,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : ((~ (A @ (sk1 @ B @ (A)) @ C)) | (~ (C = (sk2 @ C @ B @ (A)))) | ((in @ D @ (sk3 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))))),inference(cnfConj,[status(thm)],[4])).
% 18.92/5.93 thf(12,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((sk2 @ C @ B @ (A)) != C) | ((in @ D @ (sk3 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))) | (~ (A @ (sk1 @ B @ (A)) @ C)))),inference(lifteq,[status(thm)],[7])).
% 18.92/5.93 thf(1072,plain,(! [D:$i,C:$i,B:$i,A:($i > ($i > $o))] : (((sk5 @ (sk1 @ sk4 @ (^ [E:$i,F:$i]: (F = (sk5 @ E))))) != C) | ((in @ D @ (sk3 @ B @ (A))) = (? [E:$i]: ((in @ E @ B) & (A @ E @ D)))) | (~ (A @ (sk1 @ B @ (A)) @ C)) | ((sk2 @ (sk5 @ (sk1 @ sk4 @ (^ [E:$i,F:$i]: (F = (sk5 @ E))))) @ sk4 @ (^ [E:$i,F:$i]: (F = (sk5 @ E)))) != (sk2 @ C @ B @ (A))))),inference(paramod_ordered,[status(thm)],[676,12])).
% 18.92/5.93 thf(1073,plain,(! [A:$i] : (((sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) != (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))) | ((in @ A @ (sk3 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (? [B:$i]: ((in @ B @ sk4) & (A = (sk5 @ B))))) | (~ ((sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))))))),inference(pattern_uni,[status(thm)],[1072:[bind(A, $thf(^ [E:$i,F:$i]: (F = (sk5 @ E)))),bind(B, $thf(sk4)),bind(C, $thf(sk5 @ (sk1 @ sk4 @ (^ [E:$i,F:$i]: (F = (sk5 @ E)))))),bind(D, $thf(D))]])).
% 18.92/5.93 thf(1101,plain,(! [A:$i] : (((sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) != (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))) | ((sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) != (sk5 @ (sk1 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B)))))) | ((in @ A @ (sk3 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (? [B:$i]: ((in @ B @ sk4) & (A = (sk5 @ B))))))),inference(lifteq,[status(thm)],[1073])).
% 18.92/5.93 thf(1274,plain,(! [A:$i] : (((in @ A @ (sk3 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (? [B:$i]: ((in @ B @ sk4) & (A = (sk5 @ B))))))),inference(simp,[status(thm)],[1101])).
% 18.92/5.93 thf(1391,plain,(! [B:$i,A:$i] : (((? [C:$i]: ((in @ C @ sk4) & (A = (sk5 @ C)))) != (? [C:$i]: ((in @ C @ sk4) & ((sk6 @ B) = (sk5 @ C))))) | ((in @ A @ (sk3 @ sk4 @ (^ [C:$i,D:$i]: (D = (sk5 @ C))))) != (in @ (sk6 @ B) @ B)))),inference(paramod_ordered,[status(thm)],[1274,14])).
% 18.92/5.93 thf(1392,plain,(((? [A:$i]: ((in @ A @ sk4) & ((sk6 @ (sk3 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (sk5 @ A)))) != (? [A:$i]: ((in @ A @ sk4) & ((sk6 @ (sk3 @ sk4 @ (^ [B:$i,C:$i]: (C = (sk5 @ B))))) = (sk5 @ A)))))),inference(pattern_uni,[status(thm)],[1391:[bind(A, $thf(sk6 @ (sk3 @ sk4 @ (^ [C:$i,D:$i]: (D = (sk5 @ C)))))),bind(B, $thf(sk3 @ sk4 @ (^ [C:$i,D:$i]: (D = (sk5 @ C)))))]])).
% 18.92/5.93 thf(1579,plain,(($false)),inference(simp,[status(thm)],[1392])).
% 18.92/5.93 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.92/5.93 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------