%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL874^1 : TPTP v9.3.1. Bugfixed v5.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 : n005.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:14:16 AM UTC 2026
% Result : Theorem 95.62s 21.31s
% Output : Refutation 91.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL874^1 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.07 % 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.08/0.20 % Computer : n005.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 10:19:01 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 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
% 0.87/0.75 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/1.01 % [INFO] Parsing done (253ms).
% 1.22/1.02 % [INFO] Running in sequential loop mode.
% 2.09/1.32 % [INFO] eprover registered as external prover.
% 2.09/1.33 % [INFO] Scanning for conjecture ...
% 2.40/1.42 % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ...
% 2.40/1.43 % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms).
% 2.40/1.44 % [INFO] Problem is higher-order (TPTP THF).
% 2.40/1.44 % [INFO] Type checking passed.
% 2.40/1.44 % [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 ...
% 95.62/21.31 % External prover 'e' found a proof!
% 95.62/21.31 % [INFO] Killing All external provers ...
% 95.62/21.31 % Time passed: 20995ms (effective reasoning time: 20282ms)
% 95.62/21.31 % 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)>
% 95.62/21.31 % Axioms used in derivation (8): ax4, ax6, ax8, ax2, ax1, ax7, ax3, ax5
% 95.62/21.31 % No. of inferences in proof: 277
% 95.62/21.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 20995 ms resp. 20282 ms w/o parsing
% 91.84/21.48 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 91.84/21.48 thf(mu_type, type, mu: $tType).
% 91.84/21.48 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 91.84/21.48 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 91.84/21.48 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 91.84/21.48 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 91.84/21.48 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 91.84/21.48 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 91.84/21.48 thf(mserial_decl, type, mserial: (($i > ($i > $o)) > $o)).
% 91.84/21.48 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 91.84/21.48 thf(meuclidean_decl, type, meuclidean: (($i > ($i > $o)) > $o)).
% 91.84/21.48 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 91.84/21.48 thf(rk_decl, type, rk: ($i > ($i > $o))).
% 91.84/21.48 thf(rb_decl, type, rb: ($i > ($i > $o))).
% 91.84/21.48 thf(sk1_decl, type, sk1: $i).
% 91.84/21.48 thf(sk2_decl, type, sk2: ($i > $o)).
% 91.84/21.48 thf(sk3_decl, type, sk3: $i).
% 91.84/21.48 thf(sk4_decl, type, sk4: ($i > $i)).
% 91.84/21.48 thf(sk5_decl, type, sk5: (($i > $o) > ($i > $i))).
% 91.84/21.48 thf(sk6_decl, type, sk6: (($i > $o) > ($i > $i))).
% 91.84/21.48 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 91.84/21.48 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 91.84/21.48 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 91.84/21.48 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 91.84/21.48 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 91.84/21.48 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 91.84/21.48 thf(mserial_def, definition, mserial = (^ [A:($i > ($i > $o))]: ! [B:$i]: ? [C:$i]: (A @ B @ C)) ).
% 91.84/21.48 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 91.84/21.48 thf(meuclidean_def, definition, meuclidean = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ B @ D)) => (A @ C @ D))) ).
% 91.84/21.48 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 91.84/21.48 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:($i > $o)]: (~ (! [C:$i]: (~ (rb @ A @ C) | (B @ C))) | ! [C:$i]: (~ (rk @ A @ C) | (B @ C))))) ).
% 91.84/21.48 thf(sk2_def, definition, sk2 = (@+ [A:($i > $o)]: ~ (~ (! [B:$i]: (~ (rb @ sk1 @ B) | (A @ B))) | ! [B:$i]: (~ (rk @ sk1 @ B) | (A @ B)))) ).
% 91.84/21.48 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ (~ (rk @ sk1 @ A) | (sk2 @ A))) ).
% 91.84/21.48 thf(sk4_def, definition, sk4 = (^ [A:$i]: (@+ [B:$i]: (rb @ A @ B))) ).
% 91.84/21.48 thf(sk5_def, definition, sk5 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (rk @ B @ C) | (A @ C)))) ).
% 91.84/21.48 thf(sk6_def, definition, sk6 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (rb @ B @ C) | (A @ C)))) ).
% 91.84/21.48 thf(4,axiom,((mserial @ rb)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 91.84/21.48 thf(18,plain,((! [A:$i]: ? [B:$i]: (rb @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 91.84/21.48 thf(19,plain,(! [A:$i] : ((rb @ A @ (sk4 @ A)))),inference(cnf,[status(esa)],[18])).
% 91.84/21.48 thf(9,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ rk @ A) @ (mbox @ rb @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7)).
% 91.84/21.48 thf(28,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (rk @ A @ C) | (B @ C))) | ! [C:$i]: (~ (rb @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 91.84/21.48 thf(29,plain,(! [C:$i,B:($i > $o),A:$i] : ((((rk @ A @ (sk5 @ (B) @ A)) | ~ (rb @ A @ C) | (B @ C)) & (~ (B @ (sk5 @ (B) @ A)) | ~ (rb @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[28])).
% 91.84/21.48 thf(30,plain,(! [C:$i,B:($i > $o),A:$i] : ((rk @ A @ (sk5 @ (B) @ A)) | (~ (rb @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[29])).
% 91.84/21.48 thf(150,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((rk @ B @ (sk5 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ D)))),inference(paramod_ordered,[status(thm)],[19,30])).
% 91.84/21.48 thf(151,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((rk @ B @ (sk5 @ (C) @ B)) | (C @ D) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ D)))),inference(simp,[status(thm)],[150])).
% 91.84/21.48 thf(152,plain,(! [B:$i,A:($i > $o)] : ((rk @ B @ (sk5 @ (A) @ B)) | (A @ (sk4 @ B)))),inference(pattern_uni,[status(thm)],[151:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk4 @ E))]])).
% 91.84/21.48 thf(193,plain,(! [B:$i,A:($i > $o)] : ((rk @ B @ (sk5 @ (A) @ B)) | (A @ (sk4 @ B)))),inference(simp,[status(thm)],[152])).
% 91.84/21.48 thf(491,plain,(! [A:$i] : ((rk @ A @ (sk5 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[193:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 91.84/21.48 thf(538,plain,(! [A:$i] : ((rk @ A @ (sk5 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[491])).
% 91.84/21.48 thf(10,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ rb @ A) @ (mbox @ rb @ (mbox @ rk @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8)).
% 91.84/21.48 thf(34,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (rb @ A @ C) | (B @ C))) | ! [C:$i]: (~ (rb @ A @ C) | ! [D:$i]: (~ (rk @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 91.84/21.48 thf(35,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((rb @ A @ (sk6 @ (B) @ A)) | ~ (rb @ A @ C) | ~ (rk @ C @ D) | (B @ D)) & (~ (B @ (sk6 @ (B) @ A)) | ~ (rb @ A @ C) | ~ (rk @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[34])).
% 91.84/21.48 thf(37,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[35])).
% 91.84/21.48 thf(1,conjecture,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ rb @ A) @ (mbox @ rk @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 91.84/21.48 thf(2,negated_conjecture,((~ (mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ rb @ A) @ (mbox @ rk @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 91.84/21.48 thf(11,plain,((~ (! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (rb @ A @ C) | (B @ C))) | ! [C:$i]: (~ (rk @ A @ C) | (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 91.84/21.48 thf(12,plain,(! [A:$i] : (((~ (rb @ sk1 @ A) | (sk2 @ A)) & (rk @ sk1 @ sk3) & ~ (sk2 @ sk3)))),inference(cnf,[status(esa)],[11])).
% 91.84/21.48 thf(15,plain,((~ (sk2 @ sk3))),inference(cnfConj,[status(thm)],[12])).
% 91.84/21.48 thf(61,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ~ (($true)) | ((B @ D) != (sk2 @ sk3)))),inference(paramod_ordered,[status(thm)],[37,15])).
% 91.84/21.48 thf(62,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ((B @ D) != (sk2 @ sk3)))),inference(simp,[status(thm)],[61])).
% 91.84/21.48 thf(105,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | (~ (rk @ B @ sk3)))),inference(pre_uni,[status(thm)],[62:[bind(A, $thf(A)),bind(B, $thf(sk2)),bind(C, $thf(C)),bind(D, $thf(sk3))]])).
% 91.84/21.48 thf(130,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | (~ (rk @ B @ sk3)))),inference(simp,[status(thm)],[105])).
% 91.84/21.48 thf(382,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | (~ (rk @ C @ sk3)) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ C)))),inference(paramod_ordered,[status(thm)],[19,130])).
% 91.84/21.48 thf(383,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (~ (rk @ C @ sk3)) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ C)))),inference(simp,[status(thm)],[382])).
% 91.84/21.48 thf(384,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rk @ (sk4 @ A) @ sk3)))),inference(pattern_uni,[status(thm)],[383:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk4 @ D))]])).
% 91.84/21.48 thf(397,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rk @ (sk4 @ A) @ sk3)))),inference(simp,[status(thm)],[384])).
% 91.84/21.48 thf(14,plain,((rk @ sk1 @ sk3)),inference(cnfConj,[status(thm)],[12])).
% 91.84/21.48 thf(48,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | ~ (($true)) | (B @ D) | ((rk @ sk1 @ sk3) != (rk @ C @ D)))),inference(paramod_ordered,[status(thm)],[14,37])).
% 91.84/21.48 thf(49,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (B @ D) | ((rk @ sk1 @ sk3) != (rk @ C @ D)))),inference(simp,[status(thm)],[48])).
% 91.84/21.48 thf(50,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ sk1)) | (B @ sk3))),inference(pattern_uni,[status(thm)],[49:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk1)),bind(D, $thf(sk3))]])).
% 91.84/21.48 thf(79,plain,(! [B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | (~ (rb @ A @ sk1)) | ((sk6 @ (B) @ A) = sk3))),inference(replace_leibeq,[status(thm)],[50:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 91.84/21.48 thf(86,plain,(! [B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = sk3) | (~ (rb @ A @ sk1)))),inference(lifteq,[status(thm)],[79])).
% 91.84/21.48 thf(5,axiom,((mtransitive @ rk)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 91.84/21.48 thf(20,plain,((! [A:$i,B:$i,C:$i]: (((rk @ A @ B) & (rk @ B @ C)) => (rk @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 91.84/21.48 thf(21,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (~ (rk @ B @ C)) | (rk @ A @ C))),inference(cnf,[status(esa)],[20])).
% 91.84/21.48 thf(230,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (rk @ B @ C)) | (rk @ A @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ B)))),inference(paramod_ordered,[status(thm)],[14,21])).
% 91.84/21.48 thf(231,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ B @ C)) | (rk @ A @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ B)))),inference(simp,[status(thm)],[230])).
% 91.84/21.48 thf(232,plain,(! [A:$i] : ((~ (rk @ sk3 @ A)) | (rk @ sk1 @ A))),inference(pattern_uni,[status(thm)],[231:[bind(A, $thf(sk1)),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(270,plain,(! [A:$i] : ((~ (rk @ sk3 @ A)) | (rk @ sk1 @ A))),inference(simp,[status(thm)],[232])).
% 91.84/21.48 thf(453,plain,(! [C:$i,B:$i,A:($i > $o)] : ((A @ (sk4 @ B)) | ~ (($true)) | (rk @ sk1 @ C) | ((rk @ B @ (sk5 @ (A) @ B)) != (rk @ sk3 @ C)))),inference(paramod_ordered,[status(thm)],[193,270])).
% 91.84/21.48 thf(454,plain,(! [C:$i,B:$i,A:($i > $o)] : ((A @ (sk4 @ B)) | (rk @ sk1 @ C) | ((rk @ B @ (sk5 @ (A) @ B)) != (rk @ sk3 @ C)))),inference(simp,[status(thm)],[453])).
% 91.84/21.48 thf(455,plain,(! [A:($i > $o)] : ((A @ (sk4 @ sk3)) | (rk @ sk1 @ (sk5 @ (A) @ sk3)))),inference(pattern_uni,[status(thm)],[454:[bind(A, $thf(D)),bind(B, $thf(sk3)),bind(C, $thf(sk5 @ (D) @ sk3))]])).
% 91.84/21.48 thf(531,plain,(! [A:($i > $o)] : ((A @ (sk4 @ sk3)) | (rk @ sk1 @ (sk5 @ (A) @ sk3)))),inference(simp,[status(thm)],[455])).
% 91.84/21.48 thf(40,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ~ (($true)) | (~ (rb @ E @ G)) | (~ (rk @ G @ H)) | (F @ H) | ((B @ D) != (F @ (sk6 @ (F) @ E))))),inference(paramod_ordered,[status(thm)],[37,37])).
% 91.84/21.48 thf(41,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (rb @ E @ G)) | (~ (rk @ G @ H)) | (F @ H) | ((B @ D) != (F @ (sk6 @ (F) @ E))))),inference(simp,[status(thm)],[40])).
% 91.84/21.48 thf(93,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (rb @ E @ G)) | (~ (rk @ G @ H)) | (F @ H) | ((B @ D) != (F @ (sk6 @ (F) @ E))))),inference(pre_uni,[status(thm)],[41:[]])).
% 91.84/21.48 thf(94,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((F @ H) | (~ (rk @ G @ H)) | (~ (rb @ E @ G)) | (~ (rk @ C @ D)) | (~ (rb @ A @ C)) | (~ (B @ (sk6 @ (B) @ A))) | ((B @ D) != (F @ (sk6 @ (F) @ E))))),inference(pre_uni,[status(thm)],[93:[]])).
% 91.84/21.48 thf(3,axiom,((mreflexive @ rk)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1)).
% 91.84/21.48 thf(16,plain,((! [A:$i]: (rk @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 91.84/21.48 thf(17,plain,(! [A:$i] : ((rk @ A @ A))),inference(cnf,[status(esa)],[16])).
% 91.84/21.48 thf(53,plain,(! [E:$i,D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk6 @ (C) @ B))) | (~ (rb @ B @ D)) | ~ (($true)) | (C @ E) | ((rk @ A @ A) != (rk @ D @ E)))),inference(paramod_ordered,[status(thm)],[17,37])).
% 91.84/21.48 thf(54,plain,(! [E:$i,D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk6 @ (C) @ B))) | (~ (rb @ B @ D)) | (C @ E) | ((rk @ A @ A) != (rk @ D @ E)))),inference(simp,[status(thm)],[53])).
% 91.84/21.48 thf(55,plain,(! [C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk6 @ (C) @ B))) | (~ (rb @ B @ A)) | (C @ A))),inference(pattern_uni,[status(thm)],[54:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(A)),bind(E, $thf(A))]])).
% 91.84/21.48 thf(76,plain,(! [C:($i > $o),B:$i,A:$i] : ((~ ((sk6 @ (C) @ B) = (sk6 @ ((=) @ $i @ (sk6 @ C @ B)) @ B))) | (~ (rb @ B @ A)) | ((sk6 @ (C) @ B) = A))),inference(replace_leibeq,[status(thm)],[55:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf((=) @ $i @ (sk6 @ C @ B)))]])).
% 91.84/21.48 thf(83,plain,(! [C:($i > $o),B:$i,A:$i] : (((sk6 @ (C) @ B) != (sk6 @ ((=) @ $i @ (sk6 @ C @ B)) @ B)) | ((sk6 @ (C) @ B) = A) | (~ (rb @ B @ A)))),inference(lifteq,[status(thm)],[76])).
% 91.84/21.48 thf(1217,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((A @ (sk4 @ sk3)) != (rk @ (sk4 @ B) @ sk3)))),inference(paramod_ordered,[status(thm)],[531,397])).
% 91.84/21.48 thf(1218,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ (sk4 @ B) @ sk3)))),inference(simp,[status(thm)],[1217])).
% 91.84/21.48 thf(1268,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ sk3)))),inference(pre_uni,[status(thm)],[1218:[bind(A, $thf(^ [C:$i]: (rk @ C @ sk3))),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(7,axiom,((meuclidean @ rk)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5)).
% 91.84/21.48 thf(24,plain,((! [A:$i,B:$i,C:$i]: (((rk @ A @ B) & (rk @ A @ C)) => (rk @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 91.84/21.48 thf(25,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (~ (rk @ A @ C)) | (rk @ B @ C))),inference(cnf,[status(esa)],[24])).
% 91.84/21.48 thf(911,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | ~ (($true)) | (rk @ B @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ C)))),inference(paramod_ordered,[status(thm)],[14,25])).
% 91.84/21.48 thf(912,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (rk @ B @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ C)))),inference(simp,[status(thm)],[911])).
% 91.84/21.48 thf(913,plain,(! [A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ A @ sk3))),inference(pattern_uni,[status(thm)],[912:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk3))]])).
% 91.84/21.48 thf(1019,plain,(! [A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ A @ sk3))),inference(simp,[status(thm)],[913])).
% 91.84/21.48 thf(2320,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1268,1019])).
% 91.84/21.48 thf(2321,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[2320])).
% 91.84/21.48 thf(2322,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[2321:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3))]])).
% 91.84/21.48 thf(908,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (rk @ A @ C)) | (rk @ B @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ B)))),inference(paramod_ordered,[status(thm)],[14,25])).
% 91.84/21.48 thf(909,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ C)) | (rk @ B @ C) | ((rk @ sk1 @ sk3) != (rk @ A @ B)))),inference(simp,[status(thm)],[908])).
% 91.84/21.48 thf(910,plain,(! [A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ sk3 @ A))),inference(pattern_uni,[status(thm)],[909:[bind(A, $thf(sk1)),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(1017,plain,(! [A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ sk3 @ A))),inference(simp,[status(thm)],[910])).
% 91.84/21.48 thf(1060,plain,(! [B:$i,A:$i] : (~ (($true)) | (rk @ sk3 @ B) | ((rk @ A @ A) != (rk @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[17,1017])).
% 91.84/21.48 thf(1061,plain,(! [B:$i,A:$i] : ((rk @ sk3 @ B) | ((rk @ A @ A) != (rk @ sk1 @ B)))),inference(simp,[status(thm)],[1060])).
% 91.84/21.48 thf(1062,plain,((rk @ sk3 @ sk1)),inference(pattern_uni,[status(thm)],[1061:[bind(A, $thf(sk1)),bind(B, $thf(sk1))]])).
% 91.84/21.48 thf(1159,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | ~ (($true)) | (rk @ A @ C) | ((rk @ sk3 @ sk1) != (rk @ B @ C)))),inference(paramod_ordered,[status(thm)],[1062,21])).
% 91.84/21.48 thf(1160,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (rk @ A @ C) | ((rk @ sk3 @ sk1) != (rk @ B @ C)))),inference(simp,[status(thm)],[1159])).
% 91.84/21.48 thf(1161,plain,(! [A:$i] : ((~ (rk @ A @ sk3)) | (rk @ A @ sk1))),inference(pattern_uni,[status(thm)],[1160:[bind(A, $thf(A)),bind(B, $thf(sk3)),bind(C, $thf(sk1))]])).
% 91.84/21.48 thf(4186,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3) @ sk3) != (rk @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2322,1161])).
% 91.84/21.48 thf(4187,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3) @ sk3) != (rk @ A @ sk3)))),inference(simp,[status(thm)],[4186])).
% 91.84/21.48 thf(4188,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3) @ sk1)),inference(pattern_uni,[status(thm)],[4187:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3))]])).
% 91.84/21.48 thf(1153,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | ~ (($true)) | (rk @ B @ C) | ((rk @ sk3 @ sk1) != (rk @ A @ C)))),inference(paramod_ordered,[status(thm)],[1062,25])).
% 91.84/21.48 thf(1154,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (rk @ B @ C) | ((rk @ sk3 @ sk1) != (rk @ A @ C)))),inference(simp,[status(thm)],[1153])).
% 91.84/21.48 thf(1155,plain,(! [A:$i] : ((~ (rk @ sk3 @ A)) | (rk @ A @ sk1))),inference(pattern_uni,[status(thm)],[1154:[bind(A, $thf(sk3)),bind(B, $thf(B)),bind(C, $thf(sk1))]])).
% 91.84/21.48 thf(1173,plain,(! [A:$i] : ((~ (rk @ sk3 @ A)) | (rk @ A @ sk1))),inference(simp,[status(thm)],[1155])).
% 91.84/21.48 thf(233,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | ~ (($true)) | (rk @ A @ C) | ((rk @ sk1 @ sk3) != (rk @ B @ C)))),inference(paramod_ordered,[status(thm)],[14,21])).
% 91.84/21.48 thf(234,plain,(! [C:$i,B:$i,A:$i] : ((~ (rk @ A @ B)) | (rk @ A @ C) | ((rk @ sk1 @ sk3) != (rk @ B @ C)))),inference(simp,[status(thm)],[233])).
% 91.84/21.48 thf(235,plain,(! [A:$i] : ((~ (rk @ A @ sk1)) | (rk @ A @ sk3))),inference(pattern_uni,[status(thm)],[234:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(sk3))]])).
% 91.84/21.48 thf(1235,plain,(! [B:$i,A:$i] : ((~ (rk @ A @ sk1)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((rk @ A @ sk3) != (rk @ (sk4 @ B) @ sk3)))),inference(paramod_ordered,[status(thm)],[235,397])).
% 91.84/21.48 thf(1236,plain,(! [B:$i,A:$i] : ((~ (rk @ A @ sk1)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ sk3) != (rk @ (sk4 @ B) @ sk3)))),inference(simp,[status(thm)],[1235])).
% 91.84/21.48 thf(1237,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk1)) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(pattern_uni,[status(thm)],[1236:[bind(A, $thf(sk4 @ C)),bind(B, $thf(C))]])).
% 91.84/21.48 thf(1272,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk1)) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(simp,[status(thm)],[1237])).
% 91.84/21.48 thf(7083,plain,(! [B:$i,A:$i] : ((~ (rk @ sk3 @ A)) | ~ (($true)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ sk1) != (rk @ (sk4 @ B) @ sk1)))),inference(paramod_ordered,[status(thm)],[1173,1272])).
% 91.84/21.48 thf(7084,plain,(! [B:$i,A:$i] : ((~ (rk @ sk3 @ A)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ sk1) != (rk @ (sk4 @ B) @ sk1)))),inference(simp,[status(thm)],[7083])).
% 91.84/21.48 thf(7085,plain,(! [A:$i] : ((~ (rk @ sk3 @ (sk4 @ A))) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(pattern_uni,[status(thm)],[7084:[bind(A, $thf(sk4 @ C)),bind(B, $thf(C))]])).
% 91.84/21.48 thf(7177,plain,(! [A:$i] : ((~ (rk @ sk3 @ (sk4 @ A))) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(simp,[status(thm)],[7085])).
% 91.84/21.48 thf(7723,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | ~ (($true)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ sk3 @ (sk4 @ B))))),inference(paramod_ordered,[status(thm)],[531,7177])).
% 91.84/21.48 thf(7724,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ sk3 @ (sk4 @ B))))),inference(simp,[status(thm)],[7723])).
% 91.84/21.48 thf(7832,plain,((rk @ sk1 @ (sk5 @ (rk @ sk3) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ sk3)))),inference(pre_uni,[status(thm)],[7724:[bind(A, $thf(rk @ sk3)),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(10741,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (rk @ sk3) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[7832,1017])).
% 91.84/21.48 thf(10742,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (rk @ sk3) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[10741])).
% 91.84/21.48 thf(10743,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ (sk5 @ (rk @ sk3) @ sk3))),inference(pattern_uni,[status(thm)],[10742:[bind(A, $thf(sk5 @ (rk @ sk3) @ sk3))]])).
% 91.84/21.48 thf(3249,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | ~ (($true)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ (sk4 @ B) @ sk1)))),inference(paramod_ordered,[status(thm)],[531,1272])).
% 91.84/21.48 thf(3250,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ (sk4 @ B) @ sk1)))),inference(simp,[status(thm)],[3249])).
% 91.84/21.48 thf(3314,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk1)) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ sk3)))),inference(pre_uni,[status(thm)],[3250:[bind(A, $thf(^ [C:$i]: (rk @ C @ sk1))),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(9303,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[3314,1017])).
% 91.84/21.48 thf(9304,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[9303])).
% 91.84/21.48 thf(9305,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk1)) @ sk3))),inference(pattern_uni,[status(thm)],[9304:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3))]])).
% 91.84/21.48 thf(31,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk5 @ (B) @ A))) | (~ (rb @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[29])).
% 91.84/21.48 thf(1561,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk5 @ (B) @ A))) | (~ (rb @ A @ C)) | ~ (($true)) | ((B @ C) != (sk2 @ sk3)))),inference(paramod_ordered,[status(thm)],[31,15])).
% 91.84/21.48 thf(1562,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk5 @ (B) @ A))) | (~ (rb @ A @ C)) | ((B @ C) != (sk2 @ sk3)))),inference(simp,[status(thm)],[1561])).
% 91.84/21.48 thf(1755,plain,(! [A:$i] : ((~ (sk2 @ (sk5 @ (sk2) @ A))) | (~ (rb @ A @ sk3)))),inference(pre_uni,[status(thm)],[1562:[bind(A, $thf(A)),bind(B, $thf(sk2)),bind(C, $thf(sk3))]])).
% 91.84/21.48 thf(2051,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk5 @ (sk2) @ B))) | ~ (($true)) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[19,1755])).
% 91.84/21.48 thf(2052,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk5 @ (sk2) @ B))) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk3)))),inference(simp,[status(thm)],[2051])).
% 91.84/21.48 thf(2059,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk5 @ (sk2) @ B))) | (A != B) | ((sk4 @ A) != sk3))),inference(simp,[status(thm)],[2052])).
% 91.84/21.48 thf(2077,plain,(! [A:$i] : ((~ (sk2 @ (sk5 @ (sk2) @ A))) | ((sk4 @ A) != sk3))),inference(simp,[status(thm)],[2059])).
% 91.84/21.48 thf(3237,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ (sk4 @ B) @ sk1)))),inference(paramod_ordered,[status(thm)],[538,1272])).
% 91.84/21.48 thf(3238,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ (sk4 @ B) @ sk1)))),inference(simp,[status(thm)],[3237])).
% 91.84/21.48 thf(3348,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (A != (sk4 @ B)) | ((sk5 @ (^ [C:$i]: (($false))) @ A) != sk1))),inference(simp,[status(thm)],[3238])).
% 91.84/21.48 thf(3370,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ (sk4 @ A)) != sk1))),inference(simp,[status(thm)],[3348])).
% 91.84/21.48 thf(1044,plain,(! [B:$i,A:$i] : (~ (($true)) | (rk @ sk3 @ B) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[538,1017])).
% 91.84/21.48 thf(1045,plain,(! [B:$i,A:$i] : ((rk @ sk3 @ B) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk1 @ B)))),inference(simp,[status(thm)],[1044])).
% 91.84/21.48 thf(1046,plain,((rk @ sk3 @ (sk5 @ (^ [A:$i]: (($false))) @ sk1))),inference(pattern_uni,[status(thm)],[1045:[bind(A, $thf(sk1)),bind(B, $thf(sk5 @ (^ [C:$i]: (($false))) @ sk1))]])).
% 91.84/21.48 thf(70,plain,(! [E:($i > $o),D:($i > $o),C:$i,B:$i,A:$i] : ((~ ((D @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A)) | (E @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A)))) | (~ (rb @ A @ B)) | (~ (rk @ B @ C)) | ((D @ C) | (E @ C)))),inference(prim_subst,[status(thm)],[37:[bind(A, $thf(A)),bind(B, $thf(^ [G:$i]: ((E @ G) | (F @ G))))]])).
% 91.84/21.48 thf(107,plain,(! [E:($i > $o),D:($i > $o),C:$i,B:$i,A:$i] : (((~ (D @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A)) | ~ (rb @ A @ B) | ~ (rk @ B @ C) | (D @ C) | (E @ C)) & (~ (E @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A)) | ~ (rb @ A @ B) | ~ (rk @ B @ C) | (D @ C) | (E @ C))))),inference(cnf,[status(esa)],[70])).
% 91.84/21.48 thf(108,plain,(! [E:($i > $o),D:($i > $o),C:$i,B:$i,A:$i] : ((~ (D @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A))) | (~ (rb @ A @ B)) | (~ (rk @ B @ C)) | (D @ C) | (E @ C))),inference(cnfConj,[status(thm)],[107])).
% 91.84/21.48 thf(110,plain,(! [E:($i > $o),D:($i > $o),C:$i,B:$i,A:$i] : ((~ (D @ (sk6 @ (^ [F:$i]: ((D @ F) | (E @ F))) @ A))) | (~ (rb @ A @ B)) | (~ (rk @ B @ C)) | (D @ C) | (E @ C))),inference(simp,[status(thm)],[108])).
% 91.84/21.48 thf(2233,plain,(! [B:$i,A:$i] : (~ (($true)) | (rk @ B @ sk3) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[538,1019])).
% 91.84/21.48 thf(2234,plain,(! [B:$i,A:$i] : ((rk @ B @ sk3) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk1 @ B)))),inference(simp,[status(thm)],[2233])).
% 91.84/21.48 thf(2235,plain,((rk @ (sk5 @ (^ [A:$i]: (($false))) @ sk1) @ sk3)),inference(pattern_uni,[status(thm)],[2234:[bind(A, $thf(sk1)),bind(B, $thf(sk5 @ (^ [C:$i]: (($false))) @ sk1))]])).
% 91.84/21.48 thf(4177,plain,(! [A:$i] : (~ (($true)) | (rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk1) @ sk3) != (rk @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2235,1161])).
% 91.84/21.48 thf(4178,plain,(! [A:$i] : ((rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk1) @ sk3) != (rk @ A @ sk3)))),inference(simp,[status(thm)],[4177])).
% 91.84/21.48 thf(4179,plain,((rk @ (sk5 @ (^ [A:$i]: (($false))) @ sk1) @ sk1)),inference(pattern_uni,[status(thm)],[4178:[bind(A, $thf(sk5 @ (^ [B:$i]: (($false))) @ sk1))]])).
% 91.84/21.48 thf(1875,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1268,1017])).
% 91.84/21.48 thf(1876,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[1875])).
% 91.84/21.48 thf(1877,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3))),inference(pattern_uni,[status(thm)],[1876:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3))]])).
% 91.84/21.48 thf(1960,plain,(! [A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | ~ (($true)) | (rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ((A @ (sk4 @ sk3)) != (sk2 @ (sk6 @ (sk2) @ sk3))))),inference(paramod_ordered,[status(thm)],[531,1877])).
% 91.84/21.48 thf(1961,plain,(! [A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ((A @ (sk4 @ sk3)) != (sk2 @ (sk6 @ (sk2) @ sk3))))),inference(simp,[status(thm)],[1960])).
% 91.84/21.48 thf(2000,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) | (rk @ sk3 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3))),inference(pre_uni,[status(thm)],[1961:[bind(A, $thf(^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))))]])).
% 91.84/21.48 thf(4070,plain,(! [A:$i] : ((rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[2000,1019])).
% 91.84/21.48 thf(4071,plain,(! [A:$i] : ((rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[4070])).
% 91.84/21.48 thf(4072,plain,((rk @ sk3 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3)) | (rk @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[4071:[bind(A, $thf(sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))]])).
% 91.84/21.48 thf(68,plain,(! [E:($i > $i),D:($i > $i),C:$i,B:$i,A:$i] : ((~ (rb @ (D @ (sk6 @ (^ [F:$i]: (rb @ (D @ F) @ (E @ F))) @ A)) @ (E @ (sk6 @ (^ [F:$i]: (rb @ (D @ F) @ (E @ F))) @ A)))) | (~ (rb @ A @ B)) | (~ (rk @ B @ C)) | (rb @ (D @ C) @ (E @ C)))),inference(prim_subst,[status(thm)],[37:[bind(A, $thf(A)),bind(B, $thf(^ [G:$i]: (rb @ (E @ G) @ (F @ G))))]])).
% 91.84/21.48 thf(106,plain,(! [E:($i > $i),D:($i > $i),C:$i,B:$i,A:$i] : ((~ (rb @ (D @ (sk6 @ (^ [F:$i]: (rb @ (D @ F) @ (E @ F))) @ A)) @ (E @ (sk6 @ (^ [F:$i]: (rb @ (D @ F) @ (E @ F))) @ A)))) | (~ (rb @ A @ B)) | (~ (rk @ B @ C)) | (rb @ (D @ C) @ (E @ C)))),inference(simp,[status(thm)],[68])).
% 91.84/21.48 thf(42,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (F @ (sk6 @ (F) @ E))) | ~ (($true)) | (~ (rk @ G @ H)) | (F @ H) | ((B @ D) != (rb @ E @ G)))),inference(paramod_ordered,[status(thm)],[37,37])).
% 91.84/21.48 thf(43,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (F @ (sk6 @ (F) @ E))) | (~ (rk @ G @ H)) | (F @ H) | ((B @ D) != (rb @ E @ G)))),inference(simp,[status(thm)],[42])).
% 91.84/21.48 thf(80,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ ((sk6 @ (F) @ E) = (sk6 @ ((=) @ $i @ (sk6 @ F @ E)) @ E))) | (~ (rk @ G @ H)) | ((sk6 @ (F) @ E) = H) | ((B @ D) != (rb @ E @ G)))),inference(replace_leibeq,[status(thm)],[43:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf((=) @ $i @ (sk6 @ F @ E)))]])).
% 91.84/21.48 thf(84,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : (((sk6 @ (F) @ E) != (sk6 @ ((=) @ $i @ (sk6 @ F @ E)) @ E)) | ((sk6 @ (F) @ E) = H) | (~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (rk @ G @ H)) | ((B @ D) != (rb @ E @ G)))),inference(lifteq,[status(thm)],[80])).
% 91.84/21.48 thf(628,plain,(! [B:$i,A:$i] : (~ (($true)) | (rk @ sk1 @ B) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk3 @ B)))),inference(paramod_ordered,[status(thm)],[538,270])).
% 91.84/21.48 thf(629,plain,(! [B:$i,A:$i] : ((rk @ sk1 @ B) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ sk3 @ B)))),inference(simp,[status(thm)],[628])).
% 91.84/21.48 thf(630,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (($false))) @ sk3))),inference(pattern_uni,[status(thm)],[629:[bind(A, $thf(sk3)),bind(B, $thf(sk5 @ (^ [C:$i]: (($false))) @ sk3))]])).
% 91.84/21.48 thf(2283,plain,(! [A:$i] : (~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (($false))) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[630,1019])).
% 91.84/21.48 thf(2284,plain,(! [A:$i] : ((rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (($false))) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[2283])).
% 91.84/21.48 thf(2285,plain,((rk @ (sk5 @ (^ [A:$i]: (($false))) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[2284:[bind(A, $thf(sk5 @ (^ [B:$i]: (($false))) @ sk3))]])).
% 91.84/21.48 thf(4170,plain,(! [A:$i] : (~ (($true)) | (rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk3) @ sk3) != (rk @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2285,1161])).
% 91.84/21.48 thf(4171,plain,(! [A:$i] : ((rk @ A @ sk1) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk3) @ sk3) != (rk @ A @ sk3)))),inference(simp,[status(thm)],[4170])).
% 91.84/21.48 thf(4172,plain,((rk @ (sk5 @ (^ [A:$i]: (($false))) @ sk3) @ sk1)),inference(pattern_uni,[status(thm)],[4171:[bind(A, $thf(sk5 @ (^ [B:$i]: (($false))) @ sk3))]])).
% 91.84/21.48 thf(32,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk5 @ (B) @ A) = (sk5 @ ((=) @ $i @ (sk5 @ B @ A)) @ A))) | (~ (rb @ A @ C)) | ((sk5 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[31:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 91.84/21.48 thf(33,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk5 @ (B) @ A) != (sk5 @ ((=) @ $i @ (sk5 @ B @ A)) @ A)) | ((sk5 @ (B) @ A) = C) | (~ (rb @ A @ C)))),inference(lifteq,[status(thm)],[32])).
% 91.84/21.48 thf(65,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ((B @ D) != (~ (B @ (sk6 @ (B) @ A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[37])).
% 91.84/21.48 thf(92,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ((B @ D) != (~ (B @ (sk6 @ (B) @ A)))))),inference(simp,[status(thm)],[65])).
% 91.84/21.48 thf(4025,plain,(! [A:$i] : ((rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[2000,1017])).
% 91.84/21.48 thf(4026,plain,(! [A:$i] : ((rk @ sk3 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[4025])).
% 91.84/21.48 thf(4027,plain,((rk @ sk3 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3)) | (rk @ sk3 @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))),inference(pattern_uni,[status(thm)],[4026:[bind(A, $thf(sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))]])).
% 91.84/21.48 thf(2239,plain,(! [B:$i,A:$i] : ((~ (rk @ sk1 @ A)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((rk @ A @ sk3) != (rk @ (sk4 @ B) @ sk3)))),inference(paramod_ordered,[status(thm)],[1019,397])).
% 91.84/21.48 thf(2240,plain,(! [B:$i,A:$i] : ((~ (rk @ sk1 @ A)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ sk3) != (rk @ (sk4 @ B) @ sk3)))),inference(simp,[status(thm)],[2239])).
% 91.84/21.48 thf(2241,plain,(! [A:$i] : ((~ (rk @ sk1 @ (sk4 @ A))) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(pattern_uni,[status(thm)],[2240:[bind(A, $thf(sk4 @ C)),bind(B, $thf(C))]])).
% 91.84/21.48 thf(2343,plain,(! [A:$i] : ((~ (rk @ sk1 @ (sk4 @ A))) | (~ (sk2 @ (sk6 @ (sk2) @ A))))),inference(simp,[status(thm)],[2241])).
% 91.84/21.48 thf(4713,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | ~ (($true)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ sk1 @ (sk4 @ B))))),inference(paramod_ordered,[status(thm)],[531,2343])).
% 91.84/21.48 thf(4714,plain,(! [B:$i,A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ B))) | ((A @ (sk4 @ sk3)) != (rk @ sk1 @ (sk4 @ B))))),inference(simp,[status(thm)],[4713])).
% 91.84/21.48 thf(4817,plain,((rk @ sk1 @ (sk5 @ (rk @ sk1) @ sk3)) | (~ (sk2 @ (sk6 @ (sk2) @ sk3)))),inference(pre_uni,[status(thm)],[4714:[bind(A, $thf(rk @ sk1)),bind(B, $thf(sk3))]])).
% 91.84/21.48 thf(13,plain,(! [A:$i] : ((~ (rb @ sk1 @ A)) | (sk2 @ A))),inference(cnfConj,[status(thm)],[12])).
% 91.84/21.48 thf(203,plain,(! [B:$i,A:$i] : (~ (($true)) | (sk2 @ B) | ((rb @ A @ (sk4 @ A)) != (rb @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[19,13])).
% 91.84/21.48 thf(204,plain,(! [B:$i,A:$i] : ((sk2 @ B) | ((rb @ A @ (sk4 @ A)) != (rb @ sk1 @ B)))),inference(simp,[status(thm)],[203])).
% 91.84/21.48 thf(205,plain,((sk2 @ (sk4 @ sk1))),inference(pattern_uni,[status(thm)],[204:[bind(A, $thf(sk1)),bind(B, $thf(sk4 @ sk1))]])).
% 91.84/21.48 thf(2090,plain,(! [A:$i] : (~ (($true)) | ((sk4 @ A) != sk3) | ((sk2 @ (sk5 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,2077])).
% 91.84/21.48 thf(2091,plain,(! [A:$i] : (((sk4 @ A) != sk3) | ((sk2 @ (sk5 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[2090])).
% 91.84/21.48 thf(2108,plain,(! [A:$i] : (((sk4 @ A) != sk3) | ((sk5 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[2091])).
% 91.84/21.48 thf(1884,plain,(! [A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ~ (($true)) | ((A @ (sk4 @ sk3)) != (sk2 @ (sk6 @ (sk2) @ sk3))))),inference(paramod_ordered,[status(thm)],[531,1268])).
% 91.84/21.48 thf(1885,plain,(! [A:($i > $o)] : ((rk @ sk1 @ (sk5 @ (A) @ sk3)) | (rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ((A @ (sk4 @ sk3)) != (sk2 @ (sk6 @ (sk2) @ sk3))))),inference(simp,[status(thm)],[1884])).
% 91.84/21.48 thf(1932,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) | (rk @ sk1 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3))),inference(pre_uni,[status(thm)],[1885:[bind(A, $thf(^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))))]])).
% 91.84/21.48 thf(3247,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk1)) | ~ (($true)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,1272])).
% 91.84/21.48 thf(3248,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk1)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[3247])).
% 91.84/21.48 thf(3333,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk1)) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[3248])).
% 91.84/21.48 thf(10522,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (rk @ sk1) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[4817,1017])).
% 91.84/21.48 thf(10523,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (rk @ sk1) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[10522])).
% 91.84/21.48 thf(10524,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ sk3 @ (sk5 @ (rk @ sk1) @ sk3))),inference(pattern_uni,[status(thm)],[10523:[bind(A, $thf(sk5 @ (rk @ sk1) @ sk3))]])).
% 91.84/21.48 thf(1199,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ (sk4 @ B) @ sk3)))),inference(paramod_ordered,[status(thm)],[538,397])).
% 91.84/21.48 thf(1200,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rk @ A @ (sk5 @ (^ [C:$i]: (($false))) @ A)) != (rk @ (sk4 @ B) @ sk3)))),inference(simp,[status(thm)],[1199])).
% 91.84/21.48 thf(1244,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (A != (sk4 @ B)) | ((sk5 @ (^ [C:$i]: (($false))) @ A) != sk3))),inference(simp,[status(thm)],[1200])).
% 91.84/21.48 thf(1273,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ (sk4 @ A)) != sk3))),inference(simp,[status(thm)],[1244])).
% 91.84/21.48 thf(2668,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ~ (($true)) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk3) @ sk3) != (rk @ (sk4 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[2285,397])).
% 91.84/21.48 thf(2669,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk3) @ sk3) != (rk @ (sk4 @ A) @ sk3)))),inference(simp,[status(thm)],[2668])).
% 91.84/21.48 thf(2725,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ sk3) != (sk4 @ A)) | (sk3 != sk3))),inference(simp,[status(thm)],[2669])).
% 91.84/21.48 thf(2734,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ sk3) != (sk4 @ A)))),inference(simp,[status(thm)],[2725])).
% 91.84/21.48 thf(360,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ~ (($true)) | ((rk @ sk1 @ sk3) != (rk @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[14,130])).
% 91.84/21.48 thf(361,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ((rk @ sk1 @ sk3) != (rk @ B @ sk3)))),inference(simp,[status(thm)],[360])).
% 91.84/21.48 thf(362,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ sk1)))),inference(pattern_uni,[status(thm)],[361:[bind(A, $thf(A)),bind(B, $thf(sk1))]])).
% 91.84/21.48 thf(415,plain,(! [A:$i] : (~ (($true)) | (~ (rb @ A @ sk1)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,362])).
% 91.84/21.48 thf(416,plain,(! [A:$i] : ((~ (rb @ A @ sk1)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[415])).
% 91.84/21.48 thf(423,plain,(! [A:$i] : ((~ (rb @ A @ sk1)) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[416])).
% 91.84/21.48 thf(6,axiom,((mtransitive @ rb)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4)).
% 91.84/21.48 thf(22,plain,((! [A:$i,B:$i,C:$i]: (((rb @ A @ B) & (rb @ B @ C)) => (rb @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 91.84/21.48 thf(1211,plain,(! [A:$i] : (~ (($true)) | (~ (rk @ (sk4 @ A) @ sk3)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,397])).
% 91.84/21.48 thf(1212,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk3)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[1211])).
% 91.84/21.48 thf(1256,plain,(! [A:$i] : ((~ (rk @ (sk4 @ A) @ sk3)) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[1212])).
% 91.84/21.48 thf(8,axiom,((meuclidean @ rb)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6)).
% 91.84/21.48 thf(26,plain,((! [A:$i,B:$i,C:$i]: (((rb @ A @ B) & (rb @ A @ C)) => (rb @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 91.84/21.48 thf(27,plain,(! [C:$i,B:$i,A:$i] : ((~ (rb @ A @ B)) | (~ (rb @ A @ C)) | (rb @ B @ C))),inference(cnf,[status(esa)],[26])).
% 91.84/21.48 thf(216,plain,(~ (($true)) | ((sk2 @ (sk4 @ sk1)) != (sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[205,15])).
% 91.84/21.48 thf(217,plain,(((sk2 @ (sk4 @ sk1)) != (sk2 @ sk3))),inference(simp,[status(thm)],[216])).
% 91.84/21.48 thf(219,plain,(((sk4 @ sk1) != sk3)),inference(simp,[status(thm)],[217])).
% 91.84/21.48 thf(38,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | ((sk6 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[37:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 91.84/21.48 thf(39,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = D) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)))),inference(lifteq,[status(thm)],[38])).
% 91.84/21.48 thf(421,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[19,362])).
% 91.84/21.48 thf(422,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk1)))),inference(simp,[status(thm)],[421])).
% 91.84/21.48 thf(432,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (A != B) | ((sk4 @ A) != sk1))),inference(simp,[status(thm)],[422])).
% 91.84/21.48 thf(433,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk4 @ A) != sk1))),inference(simp,[status(thm)],[432])).
% 91.84/21.48 thf(751,plain,(! [A:$i] : (~ (($true)) | ((sk4 @ A) != sk1) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,433])).
% 91.84/21.48 thf(752,plain,(! [A:$i] : (((sk4 @ A) != sk1) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[751])).
% 91.84/21.48 thf(758,plain,(! [A:$i] : (((sk4 @ A) != sk1) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[752])).
% 91.84/21.48 thf(368,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (~ (rb @ B @ C)) | ~ (($true)) | ((rk @ A @ A) != (rk @ C @ sk3)))),inference(paramod_ordered,[status(thm)],[17,130])).
% 91.84/21.48 thf(369,plain,(! [C:$i,B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (~ (rb @ B @ C)) | ((rk @ A @ A) != (rk @ C @ sk3)))),inference(simp,[status(thm)],[368])).
% 91.84/21.48 thf(370,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ sk3)))),inference(pattern_uni,[status(thm)],[369:[bind(A, $thf(sk3)),bind(B, $thf(B)),bind(C, $thf(sk3))]])).
% 91.84/21.48 thf(410,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ sk3)))),inference(simp,[status(thm)],[370])).
% 91.84/21.48 thf(713,plain,(! [A:$i] : (~ (($true)) | (~ (rb @ A @ sk3)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,410])).
% 91.84/21.48 thf(714,plain,(! [A:$i] : ((~ (rb @ A @ sk3)) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[713])).
% 91.84/21.48 thf(726,plain,(! [A:$i] : ((~ (rb @ A @ sk3)) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[714])).
% 91.84/21.48 thf(9364,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[3314,1019])).
% 91.84/21.48 thf(9365,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[9364])).
% 91.84/21.48 thf(9366,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ (sk5 @ (^ [A:$i]: (rk @ A @ sk1)) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[9365:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk1)) @ sk3))]])).
% 91.84/21.48 thf(2027,plain,(! [A:$i] : (~ (($true)) | (~ (rb @ A @ sk3)) | ((sk2 @ (sk5 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,1755])).
% 91.84/21.48 thf(2028,plain,(! [A:$i] : ((~ (rb @ A @ sk3)) | ((sk2 @ (sk5 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[2027])).
% 91.84/21.48 thf(2060,plain,(! [A:$i] : ((~ (rb @ A @ sk3)) | ((sk5 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[2028])).
% 91.84/21.48 thf(722,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ~ (($true)) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[19,410])).
% 91.84/21.48 thf(723,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | ((rb @ A @ (sk4 @ A)) != (rb @ B @ sk3)))),inference(simp,[status(thm)],[722])).
% 91.84/21.48 thf(733,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ B))) | (A != B) | ((sk4 @ A) != sk3))),inference(simp,[status(thm)],[723])).
% 91.84/21.48 thf(744,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk4 @ A) != sk3))),inference(simp,[status(thm)],[733])).
% 91.84/21.48 thf(1178,plain,(! [A:$i] : (~ (($true)) | ((sk4 @ A) != sk3) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(paramod_ordered,[status(thm)],[205,744])).
% 91.84/21.48 thf(1179,plain,(! [A:$i] : (((sk4 @ A) != sk3) | ((sk2 @ (sk6 @ (sk2) @ A)) != (sk2 @ (sk4 @ sk1))))),inference(simp,[status(thm)],[1178])).
% 91.84/21.48 thf(1186,plain,(! [A:$i] : (((sk4 @ A) != sk3) | ((sk6 @ (sk2) @ A) != (sk4 @ sk1)))),inference(simp,[status(thm)],[1179])).
% 91.84/21.48 thf(2593,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ~ (($true)) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk1) @ sk3) != (rk @ (sk4 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[2235,397])).
% 91.84/21.48 thf(2594,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((rk @ (sk5 @ (^ [B:$i]: (($false))) @ sk1) @ sk3) != (rk @ (sk4 @ A) @ sk3)))),inference(simp,[status(thm)],[2593])).
% 91.84/21.48 thf(2643,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ sk1) != (sk4 @ A)) | (sk3 != sk3))),inference(simp,[status(thm)],[2594])).
% 91.84/21.48 thf(2656,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | ((sk5 @ (^ [B:$i]: (($false))) @ sk1) != (sk4 @ A)))),inference(simp,[status(thm)],[2643])).
% 91.84/21.48 thf(10583,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (rk @ sk1) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[4817,1019])).
% 91.84/21.48 thf(10584,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (rk @ sk1) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[10583])).
% 91.84/21.48 thf(10585,plain,((~ (sk2 @ (sk6 @ (sk2) @ sk3))) | (rk @ (sk5 @ (rk @ sk1) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[10584:[bind(A, $thf(sk5 @ (rk @ sk1) @ sk3))]])).
% 91.84/21.48 thf(2673,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ~ (($true)) | ((rk @ (sk5 @ (^ [C:$i]: (($false))) @ sk3) @ sk3) != (rk @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[2285,130])).
% 91.84/21.48 thf(2674,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ((rk @ (sk5 @ (^ [C:$i]: (($false))) @ sk3) @ sk3) != (rk @ B @ sk3)))),inference(simp,[status(thm)],[2673])).
% 91.84/21.48 thf(2675,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ (sk5 @ (^ [B:$i]: (($false))) @ sk3))))),inference(pattern_uni,[status(thm)],[2674:[bind(A, $thf(A)),bind(B, $thf(sk5 @ (^ [C:$i]: (($false))) @ sk3))]])).
% 91.84/21.48 thf(2303,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1932,1019])).
% 91.84/21.48 thf(2304,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[2303])).
% 91.84/21.48 thf(2305,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) | (rk @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[2304:[bind(A, $thf(sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3))]])).
% 91.84/21.48 thf(2172,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ~ (($true)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1932,1017])).
% 91.84/21.48 thf(2173,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | (rk @ sk3 @ A) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[2172])).
% 91.84/21.48 thf(2174,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3)) | (rk @ sk3 @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))),inference(pattern_uni,[status(thm)],[2173:[bind(A, $thf(sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))]])).
% 91.84/21.48 thf(23,plain,(! [C:$i,B:$i,A:$i] : ((~ (rb @ A @ B)) | (~ (rb @ B @ C)) | (rb @ A @ C))),inference(cnf,[status(esa)],[22])).
% 91.84/21.48 thf(44,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (F @ (sk6 @ (F) @ E))) | (~ (rb @ E @ G)) | ~ (($true)) | (F @ H) | ((B @ D) != (rk @ G @ H)))),inference(paramod_ordered,[status(thm)],[37,37])).
% 91.84/21.48 thf(45,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (F @ (sk6 @ (F) @ E))) | (~ (rb @ E @ G)) | (F @ H) | ((B @ D) != (rk @ G @ H)))),inference(simp,[status(thm)],[44])).
% 91.84/21.48 thf(77,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ ((sk6 @ (F) @ E) = (sk6 @ ((=) @ $i @ (sk6 @ F @ E)) @ E))) | (~ (rb @ E @ G)) | ((sk6 @ (F) @ E) = H) | ((B @ D) != (rk @ G @ H)))),inference(replace_leibeq,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf((=) @ $i @ (sk6 @ F @ E)))]])).
% 91.84/21.48 thf(82,plain,(! [H:$i,G:$i,F:($i > $o),E:$i,D:$i,C:$i,B:($i > $o),A:$i] : (((sk6 @ (F) @ E) != (sk6 @ ((=) @ $i @ (sk6 @ F @ E)) @ E)) | ((sk6 @ (F) @ E) = H) | (~ (B @ (sk6 @ (B) @ A))) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (~ (rb @ E @ G)) | ((B @ D) != (rk @ G @ H)))),inference(lifteq,[status(thm)],[77])).
% 91.84/21.48 thf(2300,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | ~ (($true)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[1932,1019])).
% 91.84/21.48 thf(2301,plain,(! [A:$i] : ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (rk @ B @ sk3)) @ sk3)) | (rk @ A @ sk3) | ((rk @ sk1 @ (sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3)) != (rk @ sk1 @ A)))),inference(simp,[status(thm)],[2300])).
% 91.84/21.48 thf(2302,plain,((rk @ sk1 @ (sk5 @ (^ [A:$i]: (rk @ A @ sk3)) @ sk3)) | (rk @ (sk5 @ (^ [A:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3) @ sk3)),inference(pattern_uni,[status(thm)],[2301:[bind(A, $thf(sk5 @ (^ [B:$i]: (sk2 @ (sk6 @ sk2 @ sk3))) @ sk3))]])).
% 91.84/21.48 thf(36,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((rb @ A @ (sk6 @ (B) @ A)) | (~ (rb @ A @ C)) | (~ (rk @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[35])).
% 91.84/21.48 thf(2598,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ~ (($true)) | ((rk @ (sk5 @ (^ [C:$i]: (($false))) @ sk1) @ sk3) != (rk @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[2235,130])).
% 91.84/21.48 thf(2599,plain,(! [B:$i,A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ B)) | ((rk @ (sk5 @ (^ [C:$i]: (($false))) @ sk1) @ sk3) != (rk @ B @ sk3)))),inference(simp,[status(thm)],[2598])).
% 91.84/21.48 thf(2600,plain,(! [A:$i] : ((~ (sk2 @ (sk6 @ (sk2) @ A))) | (~ (rb @ A @ (sk5 @ (^ [B:$i]: (($false))) @ sk1))))),inference(pattern_uni,[status(thm)],[2599:[bind(A, $thf(A)),bind(B, $thf(sk5 @ (^ [C:$i]: (($false))) @ sk1))]])).
% 91.84/21.48 thf(4204,plain,(! [B:$i,A:$i] : ((~ (rk @ sk1 @ A)) | ~ (($true)) | (rk @ B @ sk1) | ((rk @ A @ sk3) != (rk @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[1019,1161])).
% 91.84/21.48 thf(4205,plain,(! [B:$i,A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ B @ sk1) | ((rk @ A @ sk3) != (rk @ B @ sk3)))),inference(simp,[status(thm)],[4204])).
% 91.84/21.48 thf(4206,plain,(! [A:$i] : ((~ (rk @ sk1 @ A)) | (rk @ A @ sk1))),inference(pattern_uni,[status(thm)],[4205:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 91.84/21.48 thf(24725,plain,(($false)),inference(e,[status(thm)],[538,397,86,531,94,83,4188,10743,9305,2077,1173,3370,24,1046,37,25,14,110,20,4179,4072,106,84,270,4172,2000,28,630,21,33,92,3314,4027,1017,1755,4817,193,2108,2285,1932,13,3333,205,10524,2235,34,1273,2734,17,423,22,1256,27,219,362,39,1877,758,2343,726,130,9366,18,2060,7832,1186,2322,31,2656,50,10585,16,2675,744,11,1272,7177,2305,2174,55,23,1062,26,235,433,82,1161,2302,30,19,410,36,1268,2600,1019,15,4206])).
% 91.84/21.48 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 91.84/21.48 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------