%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV028^5 : TPTP v9.3.1. Released v4.0.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 : n016.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:36:44 AM UTC 2026
% Result : Theorem 9.07s 2.34s
% Output : Refutation 9.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV028^5 : TPTP v9.3.1. Released v4.0.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.20 % Computer : n016.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.21 % DateTime : Tue Sep 29 15:06:34 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.64/0.49 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.88/0.59 % [INFO] Parsing done (95ms).
% 0.88/0.60 % [INFO] Running in sequential loop mode.
% 1.23/0.78 % [INFO] eprover registered as external prover.
% 1.23/0.78 % [INFO] Scanning for conjecture ...
% 1.45/0.84 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.45/0.86 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.45/0.86 % [INFO] Problem is higher-order (TPTP THF).
% 1.45/0.86 % [INFO] Type checking passed.
% 1.45/0.86 % [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.07/2.34 % External prover 'e' found a proof!
% 9.07/2.34 % [INFO] Killing All external provers ...
% 9.07/2.34 % Time passed: 2045ms (effective reasoning time: 1737ms)
% 9.07/2.34 % 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.07/2.34 % Axioms used in derivation (0):
% 9.07/2.34 % No. of inferences in proof: 90
% 9.07/2.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 2045 ms resp. 1737 ms w/o parsing
% 9.07/2.39 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.07/2.39 thf(a_type, type, a: $tType).
% 9.07/2.39 thf(cQ_decl, type, cQ: (a > (a > $o))).
% 9.07/2.39 thf(sk1_decl, type, sk1: ((a > $o) > a)).
% 9.07/2.39 thf(sk2_decl, type, sk2: ((a > $o) > a)).
% 9.07/2.39 thf(sk3_decl, type, sk3: ((a > $o) > a)).
% 9.07/2.39 thf(sk4_decl, type, sk4: (a > (a > $o))).
% 9.07/2.39 thf(sk5_decl, type, sk5: (a > a)).
% 9.07/2.39 thf(sk6_decl, type, sk6: ((a > $o) > (a > a))).
% 9.07/2.39 thf(sk7_decl, type, sk7: ((a > $o) > (a > a))).
% 9.07/2.39 thf(sk8_decl, type, sk8: a).
% 9.07/2.39 thf(sk9_decl, type, sk9: a).
% 9.07/2.39 thf(sk10_decl, type, sk10: a).
% 9.07/2.39 thf(sk11_decl, type, sk11: a).
% 9.07/2.39 thf(sk12_decl, type, sk12: a).
% 9.07/2.39 thf(sk13_decl, type, sk13: a).
% 9.07/2.39 thf(sk1_def, definition, sk1 = (^ [A:(a > $o)]: (@+ [B:a]: ~ ((A @ B) => (! [C:a]: ((A @ C) = (cQ @ B @ C)))))) ).
% 9.07/2.39 thf(sk2_def, definition, sk2 = (^ [A:(a > $o)]: (@+ [B:a]: ~ ((A @ B) = (cQ @ (sk1 @ A) @ B)))) ).
% 9.07/2.39 thf(sk3_def, definition, sk3 = ((@+) @ a) ).
% 9.07/2.39 thf(sk4_def, definition, sk4 = (^ [A:a]: (@+ [B:(a > $o)]: (? [C:a]: (B @ C) & ! [C:a]: ((B @ C) => (! [D:a]: ((B @ D) = (cQ @ C @ D)))) & (B @ A) & ! [C:(a > $o)]: ((? [D:a]: (C @ D) & ! [D:a]: ((C @ D) => (! [E:a]: ((C @ E) = (cQ @ D @ E)))) & (C @ A)) => (C = B))))) ).
% 9.07/2.39 thf(sk5_def, definition, sk5 = (^ [A:a]: (@+ [B:a]: (sk4 @ A @ B))) ).
% 9.07/2.39 thf(sk6_def, definition, sk6 = (^ [A:(a > $o),B:a]: (@+ [C:a]: ~ ((A @ C) => (! [D:a]: ((A @ D) = (cQ @ C @ D)))))) ).
% 9.07/2.39 thf(sk7_def, definition, sk7 = (^ [A:(a > $o),B:a]: (@+ [C:a]: ~ ((A @ C) = (cQ @ (sk6 @ A @ B) @ C)))) ).
% 9.07/2.39 thf(sk8_def, definition, sk8 = (@+ [A:a]: ~ (cQ @ A @ A)) ).
% 9.07/2.39 thf(sk9_def, definition, sk9 = (@+ [A:a]: ~ (! [B:a]: ((cQ @ A @ B) => (cQ @ B @ A)))) ).
% 9.07/2.39 thf(sk10_def, definition, sk10 = (@+ [A:a]: ~ ((cQ @ sk9 @ A) => (cQ @ A @ sk9))) ).
% 9.07/2.39 thf(sk11_def, definition, sk11 = (@+ [A:a]: ~ (! [B:a,C:a]: (((cQ @ A @ B) & (cQ @ B @ C)) => (cQ @ A @ C)))) ).
% 9.07/2.39 thf(sk12_def, definition, sk12 = (@+ [A:a]: ~ (! [B:a]: (((cQ @ sk11 @ A) & (cQ @ A @ B)) => (cQ @ sk11 @ B)))) ).
% 9.07/2.39 thf(sk13_def, definition, sk13 = (@+ [A:a]: ~ (((cQ @ sk11 @ sk12) & (cQ @ sk12 @ A)) => (cQ @ sk11 @ A))) ).
% 9.07/2.39 thf(1,conjecture,(((! [A:(a > $o)]: ((? [B:a]: (A @ B) & ! [B:a]: ((A @ B) => (! [C:a]: ((A @ C) = (cQ @ B @ C))))) => (? [B:a]: (A @ B))) & ! [A:a]: ? [B:(a > $o)]: (? [C:a]: (B @ C) & ! [C:a]: ((B @ C) => (! [D:a]: ((B @ D) = (cQ @ C @ D)))) & (B @ A) & ! [C:(a > $o)]: ((? [D:a]: (C @ D) & ! [D:a]: ((C @ D) => (! [E:a]: ((C @ E) = (cQ @ D @ E)))) & (C @ A)) => (C = B)))) => (! [A:a]: (cQ @ A @ A) & ! [A:a,B:a]: ((cQ @ A @ B) => (cQ @ B @ A)) & ! [A:a,B:a,C:a]: (((cQ @ A @ B) & (cQ @ B @ C)) => (cQ @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM558_pme)).
% 9.07/2.39 thf(2,negated_conjecture,((~ ((! [A:(a > $o)]: ((? [B:a]: (A @ B) & ! [B:a]: ((A @ B) => (! [C:a]: ((A @ C) = (cQ @ B @ C))))) => (? [B:a]: (A @ B))) & ! [A:a]: ? [B:(a > $o)]: (? [C:a]: (B @ C) & ! [C:a]: ((B @ C) => (! [D:a]: ((B @ D) = (cQ @ C @ D)))) & (B @ A) & ! [C:(a > $o)]: ((? [D:a]: (C @ D) & ! [D:a]: ((C @ D) => (! [E:a]: ((C @ E) = (cQ @ D @ E)))) & (C @ A)) => (C = B)))) => (! [A:a]: (cQ @ A @ A) & ! [A:a,B:a]: ((cQ @ A @ B) => (cQ @ B @ A)) & ! [A:a,B:a,C:a]: (((cQ @ A @ B) & (cQ @ B @ C)) => (cQ @ A @ C)))))),inference(neg_conjecture,[status(cth)],[1])).
% 9.07/2.39 thf(3,plain,((~ ((! [A:(a > $o)]: ((? [B:a]: (A @ B) & ! [B:a]: ((A @ B) => (! [C:a]: ((A @ C) = (cQ @ B @ C))))) => (? [B:a]: (A @ B))) & ! [A:a]: ? [B:(a > $o)]: (? [C:a]: (B @ C) & ! [C:a]: ((B @ C) => (! [D:a]: ((B @ D) = (cQ @ C @ D)))) & (B @ A) & ! [C:(a > $o)]: ((? [D:a]: (C @ D) & ! [D:a]: ((C @ D) => (! [E:a]: ((C @ E) = (cQ @ D @ E)))) & (C @ A)) => ((C) = (B))))) => (! [A:a]: (cQ @ A @ A) & ! [A:a,B:a]: ((cQ @ A @ B) => (cQ @ B @ A)) & ! [A:a,B:a,C:a]: (((cQ @ A @ B) & (cQ @ B @ C)) => (cQ @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 9.07/2.39 thf(4,plain,(! [G:a,F:(a > $o),E:a,D:a,C:a,B:a,A:(a > $o)] : (((~ (A @ B) | (A @ (sk1 @ (A))) | (A @ (sk3 @ (A)))) & (~ (A @ B) | ~ ((A @ (sk2 @ (A))) = (cQ @ (sk1 @ (A)) @ (sk2 @ (A)))) | (A @ (sk3 @ (A)))) & (sk4 @ C @ (sk5 @ C)) & (~ (sk4 @ C @ D) | ((sk4 @ C @ E) = (cQ @ D @ E))) & (sk4 @ C @ C) & (~ (F @ G) | (F @ (sk6 @ (F) @ C)) | ~ (F @ C) | ((F) = (sk4 @ C))) & (~ (F @ G) | ~ ((F @ (sk7 @ (F) @ C)) = (cQ @ (sk6 @ (F) @ C) @ (sk7 @ (F) @ C))) | ~ (F @ C) | ((F) = (sk4 @ C))) & (~ (cQ @ sk8 @ sk8) | (cQ @ sk9 @ sk10) | (cQ @ sk11 @ sk12)) & (~ (cQ @ sk8 @ sk8) | (cQ @ sk9 @ sk10) | (cQ @ sk12 @ sk13)) & (~ (cQ @ sk8 @ sk8) | (cQ @ sk9 @ sk10) | ~ (cQ @ sk11 @ sk13)) & (~ (cQ @ sk8 @ sk8) | ~ (cQ @ sk10 @ sk9) | (cQ @ sk11 @ sk12)) & (~ (cQ @ sk8 @ sk8) | ~ (cQ @ sk10 @ sk9) | (cQ @ sk12 @ sk13)) & (~ (cQ @ sk8 @ sk8) | ~ (cQ @ sk10 @ sk9) | ~ (cQ @ sk11 @ sk13))))),inference(cnf,[status(esa)],[3])).
% 9.07/2.39 thf(12,plain,(! [A:a] : ((sk4 @ A @ (sk5 @ A)))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(28,plain,(! [A:a] : ((sk4 @ A @ (sk5 @ A)))),inference(simp,[status(thm)],[12])).
% 9.07/2.39 thf(14,plain,(! [A:a] : ((sk4 @ A @ A))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(23,plain,(! [A:a] : ((sk4 @ A @ A))),inference(simp,[status(thm)],[14])).
% 9.07/2.39 thf(8,plain,(! [C:a,B:a,A:a] : ((~ (sk4 @ A @ B)) | ((sk4 @ A @ C) = (cQ @ B @ C)))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(32,plain,(! [C:a,B:a,A:a] : (((sk4 @ A @ C) = (cQ @ B @ C)) | (~ (sk4 @ A @ B)))),inference(lifteq,[status(thm)],[8])).
% 9.07/2.39 thf(33,plain,(! [C:a,B:a,A:a] : (((sk4 @ A @ C) = (cQ @ B @ C)) | (~ (sk4 @ A @ B)))),inference(simp,[status(thm)],[32])).
% 9.07/2.39 thf(209,plain,(! [D:a,C:a,B:a,A:a] : (((sk4 @ B @ D) = (cQ @ C @ D)) | ~ (($true)) | ((sk4 @ A @ A) != (sk4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[23,33])).
% 9.07/2.39 thf(210,plain,(! [D:a,C:a,B:a,A:a] : (((sk4 @ B @ D) = (cQ @ C @ D)) | ((sk4 @ A @ A) != (sk4 @ B @ C)))),inference(simp,[status(thm)],[209])).
% 9.07/2.39 thf(211,plain,(! [B:a,A:a] : (((sk4 @ A @ B) = (cQ @ A @ B)))),inference(pattern_uni,[status(thm)],[210:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(A))]])).
% 9.07/2.39 thf(247,plain,(! [B:a,A:a] : (((sk4 @ A @ B) = (cQ @ A @ B)))),inference(simp,[status(thm)],[211])).
% 9.07/2.39 thf(253,plain,(! [A:a] : ((cQ @ A @ (sk5 @ A)))),inference(rewrite,[status(thm)],[28,247])).
% 9.07/2.39 thf(6,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (cQ @ sk11 @ sk12)),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(10,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (~ (cQ @ sk11 @ sk13))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(94,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | ~ (($true)) | ((cQ @ sk11 @ sk13) != (cQ @ sk11 @ sk12))),inference(paramod_ordered,[status(thm)],[6,10])).
% 9.07/2.39 thf(95,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | ((cQ @ sk11 @ sk13) != (cQ @ sk11 @ sk12))),inference(simp,[status(thm)],[94])).
% 9.07/2.39 thf(113,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (sk11 != sk11) | (sk13 != sk12)),inference(simp,[status(thm)],[95])).
% 9.07/2.39 thf(117,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (sk13 != sk12)),inference(simp,[status(thm)],[113])).
% 9.07/2.39 thf(251,plain,(! [A:a] : ((cQ @ A @ A))),inference(rewrite,[status(thm)],[23,247])).
% 9.07/2.39 thf(304,plain,(~ (($true)) | (~ (cQ @ sk10 @ sk9)) | (sk13 != sk12)),inference(rewrite,[status(thm)],[117,251])).
% 9.07/2.39 thf(305,plain,((~ (cQ @ sk10 @ sk9)) | (sk13 != sk12)),inference(simp,[status(thm)],[304])).
% 9.07/2.39 thf(327,plain,(! [A:a] : (~ (($true)) | (sk13 != sk12) | ((cQ @ A @ (sk5 @ A)) != (cQ @ sk10 @ sk9)))),inference(paramod_ordered,[status(thm)],[253,305])).
% 9.07/2.39 thf(328,plain,(! [A:a] : ((sk13 != sk12) | ((cQ @ A @ (sk5 @ A)) != (cQ @ sk10 @ sk9)))),inference(simp,[status(thm)],[327])).
% 9.07/2.39 thf(330,plain,(! [A:a] : ((sk13 != sk12) | (A != sk10) | ((sk5 @ A) != sk9))),inference(simp,[status(thm)],[328])).
% 9.07/2.39 thf(333,plain,((sk13 != sk12) | ((sk5 @ sk10) != sk9)),inference(simp,[status(thm)],[330])).
% 9.07/2.39 thf(9,plain,((~ (cQ @ sk8 @ sk8)) | (cQ @ sk9 @ sk10) | (~ (cQ @ sk11 @ sk13))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(315,plain,(~ (($true)) | (cQ @ sk9 @ sk10) | (~ (cQ @ sk11 @ sk13))),inference(rewrite,[status(thm)],[9,251])).
% 9.07/2.39 thf(316,plain,((cQ @ sk9 @ sk10) | (~ (cQ @ sk11 @ sk13))),inference(simp,[status(thm)],[315])).
% 9.07/2.39 thf(223,plain,(! [D:a,C:a,B:a,A:a] : (((sk4 @ B @ D) = (cQ @ C @ D)) | ~ (($true)) | ((sk4 @ A @ (sk5 @ A)) != (sk4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[28,33])).
% 9.07/2.39 thf(224,plain,(! [D:a,C:a,B:a,A:a] : (((sk4 @ B @ D) = (cQ @ C @ D)) | ((sk4 @ A @ (sk5 @ A)) != (sk4 @ B @ C)))),inference(simp,[status(thm)],[223])).
% 9.07/2.39 thf(225,plain,(! [B:a,A:a] : (((sk4 @ B @ A) = (cQ @ (sk5 @ B) @ A)))),inference(pattern_uni,[status(thm)],[224:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(sk5 @ E))]])).
% 9.07/2.39 thf(239,plain,(! [B:a,A:a] : (((sk4 @ B @ A) = (cQ @ (sk5 @ B) @ A)))),inference(simp,[status(thm)],[225])).
% 9.07/2.39 thf(334,plain,(! [B:a,A:a] : (((cQ @ (sk5 @ B) @ A) = (cQ @ B @ A)))),inference(rewrite,[status(thm)],[239,247])).
% 9.07/2.39 thf(292,plain,(~ (($true)) | (~ (cQ @ sk10 @ sk9)) | (~ (cQ @ sk11 @ sk13))),inference(rewrite,[status(thm)],[10,251])).
% 9.07/2.39 thf(293,plain,((~ (cQ @ sk10 @ sk9)) | (~ (cQ @ sk11 @ sk13))),inference(simp,[status(thm)],[292])).
% 9.07/2.39 thf(388,plain,(! [A:a] : (~ (($true)) | (~ (cQ @ sk11 @ sk13)) | ((cQ @ A @ A) != (cQ @ sk10 @ sk9)))),inference(paramod_ordered,[status(thm)],[251,293])).
% 9.07/2.39 thf(389,plain,(! [A:a] : ((~ (cQ @ sk11 @ sk13)) | ((cQ @ A @ A) != (cQ @ sk10 @ sk9)))),inference(simp,[status(thm)],[388])).
% 9.07/2.39 thf(402,plain,(! [A:a] : ((~ (cQ @ sk11 @ sk13)) | (A != sk10) | (A != sk9))),inference(simp,[status(thm)],[389])).
% 9.07/2.39 thf(412,plain,((~ (cQ @ sk11 @ sk13)) | (sk10 != sk9)),inference(simp,[status(thm)],[402])).
% 9.07/2.39 thf(470,plain,(! [A:a] : (~ (($true)) | (sk10 != sk9) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(paramod_ordered,[status(thm)],[251,412])).
% 9.07/2.39 thf(471,plain,(! [A:a] : ((sk10 != sk9) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(simp,[status(thm)],[470])).
% 9.07/2.39 thf(483,plain,(! [A:a] : ((sk10 != sk9) | (A != sk11) | (A != sk13))),inference(simp,[status(thm)],[471])).
% 9.07/2.39 thf(488,plain,((sk10 != sk9) | (sk13 != sk11)),inference(simp,[status(thm)],[483])).
% 9.07/2.39 thf(390,plain,(! [A:a] : ((~ (cQ @ sk10 @ sk9)) | ~ (($true)) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(paramod_ordered,[status(thm)],[251,293])).
% 9.07/2.39 thf(391,plain,(! [A:a] : ((~ (cQ @ sk10 @ sk9)) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(simp,[status(thm)],[390])).
% 9.07/2.39 thf(404,plain,(! [A:a] : ((~ (cQ @ sk10 @ sk9)) | (A != sk11) | (A != sk13))),inference(simp,[status(thm)],[391])).
% 9.07/2.39 thf(414,plain,((~ (cQ @ sk10 @ sk9)) | (sk13 != sk11)),inference(simp,[status(thm)],[404])).
% 9.07/2.39 thf(338,plain,(! [C:a,B:a,A:a] : ((cQ @ B @ A) | ((cQ @ (sk5 @ B) @ A) != (cQ @ C @ (sk5 @ C))))),inference(paramod_ordered,[status(thm)],[334,253])).
% 9.07/2.39 thf(339,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ A))))),inference(pattern_uni,[status(thm)],[338:[bind(A, $thf(sk5 @ (sk5 @ F))),bind(B, $thf(F)),bind(C, $thf(sk5 @ F))]])).
% 9.07/2.39 thf(351,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ A))))),inference(simp,[status(thm)],[339])).
% 9.07/2.39 thf(360,plain,(! [C:a,B:a,A:a] : ((cQ @ C @ B) | ((cQ @ A @ (sk5 @ (sk5 @ A))) != (cQ @ (sk5 @ C) @ B)))),inference(paramod_ordered,[status(thm)],[351,334])).
% 9.07/2.39 thf(361,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ A)))))),inference(pattern_uni,[status(thm)],[360:[bind(A, $thf(sk5 @ G)),bind(B, $thf(sk5 @ (sk5 @ (sk5 @ G)))),bind(C, $thf(G))]])).
% 9.07/2.39 thf(374,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ A)))))),inference(simp,[status(thm)],[361])).
% 9.07/2.39 thf(549,plain,(! [C:a,B:a,A:a] : ((cQ @ C @ B) | ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ A)))) != (cQ @ (sk5 @ C) @ B)))),inference(paramod_ordered,[status(thm)],[374,334])).
% 9.07/2.39 thf(550,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ A))))))),inference(pattern_uni,[status(thm)],[549:[bind(A, $thf(sk5 @ H)),bind(B, $thf(sk5 @ (sk5 @ (sk5 @ (sk5 @ H))))),bind(C, $thf(H))]])).
% 9.07/2.39 thf(576,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ A))))))),inference(simp,[status(thm)],[550])).
% 9.07/2.39 thf(7,plain,((~ (cQ @ sk8 @ sk8)) | (cQ @ sk9 @ sk10) | (cQ @ sk11 @ sk12)),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(298,plain,(~ (($true)) | (cQ @ sk9 @ sk10) | (cQ @ sk11 @ sk12)),inference(rewrite,[status(thm)],[7,251])).
% 9.07/2.39 thf(299,plain,((cQ @ sk9 @ sk10) | (cQ @ sk11 @ sk12)),inference(simp,[status(thm)],[298])).
% 9.07/2.39 thf(419,plain,((cQ @ sk9 @ sk10) | (cQ @ sk9 @ sk10) | ~ (($true)) | ((cQ @ sk11 @ sk13) != (cQ @ sk11 @ sk12))),inference(paramod_ordered,[status(thm)],[299,316])).
% 9.07/2.39 thf(420,plain,((cQ @ sk9 @ sk10) | ((cQ @ sk11 @ sk13) != (cQ @ sk11 @ sk12))),inference(simp,[status(thm)],[419])).
% 9.07/2.39 thf(435,plain,((cQ @ sk9 @ sk10) | (sk11 != sk11) | (sk13 != sk12)),inference(simp,[status(thm)],[420])).
% 9.07/2.39 thf(442,plain,((cQ @ sk9 @ sk10) | (sk13 != sk12)),inference(simp,[status(thm)],[435])).
% 9.07/2.39 thf(317,plain,(! [A:a] : ((cQ @ sk9 @ sk10) | ~ (($true)) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(paramod_ordered,[status(thm)],[251,316])).
% 9.07/2.39 thf(318,plain,(! [A:a] : ((cQ @ sk9 @ sk10) | ((cQ @ A @ A) != (cQ @ sk11 @ sk13)))),inference(simp,[status(thm)],[317])).
% 9.07/2.39 thf(321,plain,(! [A:a] : ((cQ @ sk9 @ sk10) | (A != sk11) | (A != sk13))),inference(simp,[status(thm)],[318])).
% 9.07/2.39 thf(322,plain,((cQ @ sk9 @ sk10) | (sk13 != sk11)),inference(simp,[status(thm)],[321])).
% 9.07/2.39 thf(309,plain,(! [A:a] : (~ (($true)) | (sk13 != sk12) | ((cQ @ A @ A) != (cQ @ sk10 @ sk9)))),inference(paramod_ordered,[status(thm)],[251,305])).
% 9.07/2.39 thf(310,plain,(! [A:a] : ((sk13 != sk12) | ((cQ @ A @ A) != (cQ @ sk10 @ sk9)))),inference(simp,[status(thm)],[309])).
% 9.07/2.39 thf(311,plain,(! [A:a] : ((sk13 != sk12) | (A != sk10) | (A != sk9))),inference(simp,[status(thm)],[310])).
% 9.07/2.39 thf(312,plain,((sk13 != sk12) | (sk10 != sk9)),inference(simp,[status(thm)],[311])).
% 9.07/2.39 thf(589,plain,(! [C:a,B:a,A:a] : ((cQ @ C @ B) | ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ A))))) != (cQ @ (sk5 @ C) @ B)))),inference(paramod_ordered,[status(thm)],[576,334])).
% 9.07/2.39 thf(590,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ A)))))))),inference(pattern_uni,[status(thm)],[589:[bind(A, $thf(sk5 @ I)),bind(B, $thf(sk5 @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ I)))))),bind(C, $thf(I))]])).
% 9.07/2.39 thf(625,plain,(! [A:a] : ((cQ @ A @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ (sk5 @ A)))))))),inference(simp,[status(thm)],[590])).
% 9.07/2.39 thf(15,plain,((~ (cQ @ sk8 @ sk8)) | (~ (cQ @ sk10 @ sk9)) | (cQ @ sk12 @ sk13)),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(492,plain,(~ (($true)) | (~ (cQ @ sk10 @ sk9)) | (cQ @ sk12 @ sk13)),inference(rewrite,[status(thm)],[15,251])).
% 9.07/2.39 thf(493,plain,((~ (cQ @ sk10 @ sk9)) | (cQ @ sk12 @ sk13)),inference(simp,[status(thm)],[492])).
% 9.07/2.39 thf(17,plain,(! [B:a,A:(a > $o)] : ((~ (A @ B)) | (A @ (sk1 @ (A))) | (A @ (sk3 @ (A))))),inference(cnfConj,[status(thm)],[4])).
% 9.07/2.39 thf(19,plain,(! [A:a] : ((~ (A = A)) | (A = (sk1 @ ((=) @ a @ A))) | (A = (sk3 @ ((=) @ a @ A))))),inference(replace_leibeq,[status(thm)],[17:[bind(A, $thf((=) @ a @ B))]])).
% 9.07/2.39 thf(34,plain,(! [A:a] : ((A != A) | (A = (sk1 @ ((=) @ a @ A))) | (A = (sk3 @ ((=) @ a @ A))))),inference(lifteq,[status(thm)],[19])).
% 9.07/2.39 thf(35,plain,(! [A:a] : ((A = (sk1 @ ((=) @ a @ A))) | (A = (sk3 @ ((=) @ a @ A))))),inference(simp,[status(thm)],[34])).
% 9.07/2.39 thf(467,plain,(! [A:a] : (~ (($true)) | (sk10 != sk9) | ((cQ @ A @ (sk5 @ A)) != (cQ @ sk11 @ sk13)))),inference(paramod_ordered,[status(thm)],[253,412])).
% 9.07/2.39 thf(468,plain,(! [A:a] : ((sk10 != sk9) | ((cQ @ A @ (sk5 @ A)) != (cQ @ sk11 @ sk13)))),inference(simp,[status(thm)],[467])).
% 9.07/2.39 thf(481,plain,(! [A:a] : ((sk10 != sk9) | (A != sk11) | ((sk5 @ A) != sk13))),inference(simp,[status(thm)],[468])).
% 9.07/2.39 thf(487,plain,((sk10 != sk9) | ((sk5 @ sk11) != sk13)),inference(simp,[status(thm)],[481])).
% 9.07/2.39 thf(1237,plain,(($false)),inference(e,[status(thm)],[333,247,316,253,334,488,412,251,414,576,351,305,442,322,293,312,625,493,299,3,35,374,487])).
% 9.07/2.39 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.07/2.39 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------