%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL716^1 : TPTP v9.3.1. Bugfixed v5.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:14:11 AM UTC 2026
% Result : Theorem 86.77s 18.71s
% Output : Refutation 74.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL716^1 : TPTP v9.3.1. Bugfixed v5.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.09/0.22 % Computer : n016.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Tue Sep 29 09:56:04 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 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
% 1.07/0.82 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.49/1.10 % [INFO] Parsing done (277ms).
% 1.49/1.12 % [INFO] Running in sequential loop mode.
% 2.49/1.50 % [INFO] eprover registered as external prover.
% 2.49/1.51 % [INFO] Scanning for conjecture ...
% 2.71/1.69 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.93/1.72 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.93/1.72 % [INFO] Problem is higher-order (TPTP THF).
% 2.93/1.73 % [INFO] Type checking passed.
% 2.93/1.73 % [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 ...
% 86.77/18.71 % External prover 'e' found a proof!
% 86.77/18.71 % [INFO] Killing All external provers ...
% 86.77/18.71 % Time passed: 18343ms (effective reasoning time: 17589ms)
% 86.77/18.71 % 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)>
% 86.77/18.71 % Axioms used in derivation (0):
% 86.77/18.71 % No. of inferences in proof: 313
% 86.77/18.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 18343 ms resp. 17589 ms w/o parsing
% 74.67/18.91 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.67/18.91 thf(mu_type, type, mu: $tType).
% 74.67/18.91 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 74.67/18.91 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.67/18.91 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.67/18.91 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 74.67/18.91 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 74.67/18.91 thf(mweakly_dense_decl, type, mweakly_dense: (($i > ($i > $o)) > $o)).
% 74.67/18.91 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 74.67/18.91 thf(sk1_decl, type, sk1: ($i > ($i > $o))).
% 74.67/18.91 thf(sk2_decl, type, sk2: (($i > $o) > ($i > $i))).
% 74.67/18.91 thf(sk3_decl, type, sk3: (($i > $o) > ($i > $i))).
% 74.67/18.91 thf(sk4_decl, type, sk4: $i).
% 74.67/18.91 thf(sk5_decl, type, sk5: $i).
% 74.67/18.91 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 74.67/18.91 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 74.67/18.91 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 74.67/18.91 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 74.67/18.91 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 74.67/18.91 thf(mweakly_dense_def, definition, mweakly_dense = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: ((A @ B @ C) => (? [E:$i]: ((A @ B @ E) & (A @ E @ C))))) ).
% 74.67/18.91 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 74.67/18.91 thf(sk1_def, definition, sk1 = (@+ [A:($i > ($i > $o))]: ~ ((! [B:$i,C:($i > $o)]: (~ (! [D:$i]: (~ (A @ B @ D) | ! [E:$i]: (~ (A @ D @ E) | (C @ E)))) | ! [D:$i]: (~ (A @ B @ D) | (C @ D)))) => (! [B:$i,C:$i]: ((A @ B @ C) => (? [D:$i]: ((A @ B @ D) & (A @ D @ C))))))) ).
% 74.67/18.91 thf(sk2_def, definition, sk2 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (sk1 @ B @ C) | ! [D:$i]: (~ (sk1 @ C @ D) | (A @ D))))) ).
% 74.67/18.91 thf(sk3_def, definition, sk3 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (sk1 @ (sk2 @ A @ B) @ C) | (A @ C)))) ).
% 74.67/18.91 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ (! [B:$i]: ((sk1 @ A @ B) => (? [C:$i]: ((sk1 @ A @ C) & (sk1 @ C @ B)))))) ).
% 74.67/18.91 thf(sk5_def, definition, sk5 = (@+ [A:$i]: ~ ((sk1 @ sk4 @ A) => (? [B:$i]: ((sk1 @ sk4 @ B) & (sk1 @ B @ A))))) ).
% 74.67/18.91 thf(1,conjecture,((! [A:($i > ($i > $o))]: ((mvalid @ (mforall_prop @ (^ [B:($i > $o)]: (mimplies @ (mbox @ A @ (mbox @ A @ B)) @ (mbox @ A @ B))))) => (mweakly_dense @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 74.67/18.91 thf(2,negated_conjecture,((~ (! [A:($i > ($i > $o))]: ((mvalid @ (mforall_prop @ (^ [B:($i > $o)]: (mimplies @ (mbox @ A @ (mbox @ A @ B)) @ (mbox @ A @ B))))) => (mweakly_dense @ A))))),inference(neg_conjecture,[status(cth)],[1])).
% 74.67/18.91 thf(3,plain,((~ (! [A:($i > ($i > $o))]: ((! [B:$i,C:($i > $o)]: (~ (! [D:$i]: (~ (A @ B @ D) | ! [E:$i]: (~ (A @ D @ E) | (C @ E)))) | ! [D:$i]: (~ (A @ B @ D) | (C @ D)))) => (! [B:$i,C:$i]: ((A @ B @ C) => (? [D:$i]: ((A @ B @ D) & (A @ D @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 74.67/18.91 thf(4,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((sk1 @ A @ (sk2 @ (B) @ A)) | ~ (sk1 @ A @ C) | (B @ C)) & ((sk1 @ (sk2 @ (B) @ A) @ (sk3 @ (B) @ A)) | ~ (sk1 @ A @ C) | (B @ C)) & (~ (B @ (sk3 @ (B) @ A)) | ~ (sk1 @ A @ C) | (B @ C)) & (sk1 @ sk4 @ sk5) & (~ (sk1 @ sk4 @ D) | ~ (sk1 @ D @ sk5))))),inference(cnf,[status(esa)],[3])).
% 74.67/18.91 thf(7,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[4])).
% 74.67/18.91 thf(8,plain,((sk1 @ sk4 @ sk5)),inference(cnfConj,[status(thm)],[4])).
% 74.67/18.91 thf(5,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | (~ (sk1 @ A @ sk5)))),inference(cnfConj,[status(thm)],[4])).
% 74.67/18.91 thf(11,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | (~ (sk1 @ A @ sk5)))),inference(simp,[status(thm)],[5])).
% 74.67/18.91 thf(16,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | ~ (($true)) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[8,11])).
% 74.67/18.91 thf(17,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ sk5)))),inference(simp,[status(thm)],[16])).
% 74.67/18.91 thf(18,plain,((~ (sk1 @ sk4 @ sk4))),inference(pattern_uni,[status(thm)],[17:[bind(A, $thf(sk4))]])).
% 74.67/18.91 thf(39,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ~ (($true)) | ((B @ C) != (sk1 @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[7,18])).
% 74.67/18.91 thf(40,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ((B @ C) != (sk1 @ sk4 @ sk4)))),inference(simp,[status(thm)],[39])).
% 74.67/18.91 thf(73,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ A)) | (~ (sk1 @ A @ sk4)))),inference(pre_uni,[status(thm)],[40:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (sk1 @ D @ D))),bind(C, $thf(sk4))]])).
% 74.67/18.91 thf(35,plain,(! [F:$i,E:($i > $o),D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (sk1 @ D @ (sk2 @ (E) @ D)) | ~ (($true)) | (E @ F) | ((B @ C) != (sk1 @ D @ F)))),inference(paramod_ordered,[status(thm)],[7,7])).
% 74.67/18.91 thf(36,plain,(! [F:$i,E:($i > $o),D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (sk1 @ D @ (sk2 @ (E) @ D)) | (E @ F) | ((B @ C) != (sk1 @ D @ F)))),inference(simp,[status(thm)],[35])).
% 74.67/18.91 thf(76,plain,(! [E:($i > $i),D:($i > $i),C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [F:$i]: (sk1 @ (D @ F) @ (E @ F))) @ A)) | (~ (sk1 @ A @ B)) | (sk1 @ (D @ B) @ (sk2 @ (C) @ (D @ B))) | (C @ (E @ B)))),inference(pre_uni,[status(thm)],[36:[bind(A, $thf(A)),bind(B, $thf(^ [I:$i]: (sk1 @ (G @ I) @ (H @ I)))),bind(C, $thf(C)),bind(D, $thf(G @ C)),bind(E, $thf(E)),bind(F, $thf(H @ C))]])).
% 74.67/18.91 thf(87,plain,(! [E:($i > $i),D:($i > $i),C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [F:$i]: (sk1 @ (D @ F) @ (E @ F))) @ A)) | (~ (sk1 @ A @ B)) | (sk1 @ (D @ B) @ (sk2 @ (C) @ (D @ B))) | (C @ (E @ B)))),inference(simp,[status(thm)],[76])).
% 74.67/18.91 thf(62,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [E:$i]: ((C @ E) | (D @ E))) @ A)) | (~ (sk1 @ A @ B)) | ((C @ B) | (D @ B)))),inference(prim_subst,[status(thm)],[7:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: ((D @ F) | (E @ F))))]])).
% 74.67/18.91 thf(100,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [E:$i]: ((C @ E) | (D @ E))) @ A)) | (~ (sk1 @ A @ B)) | (C @ B) | (D @ B))),inference(cnf,[status(esa)],[62])).
% 74.67/18.91 thf(101,plain,(! [D:($i > $o),C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [E:$i]: ((C @ E) | (D @ E))) @ A)) | (~ (sk1 @ A @ B)) | (C @ B) | (D @ B))),inference(simp,[status(thm)],[100])).
% 74.67/18.91 thf(50,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[8,7])).
% 74.67/18.91 thf(51,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (B @ C) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ C)))),inference(simp,[status(thm)],[50])).
% 74.67/18.91 thf(52,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ sk5))),inference(pattern_uni,[status(thm)],[51:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(sk5))]])).
% 74.67/18.91 thf(96,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ sk5))),inference(simp,[status(thm)],[52])).
% 74.67/18.91 thf(13,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ sk5) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[8,11])).
% 74.67/18.91 thf(14,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ sk5) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[13])).
% 74.67/18.91 thf(15,plain,((~ (sk1 @ sk5 @ sk5))),inference(pattern_uni,[status(thm)],[14:[bind(A, $thf(sk5))]])).
% 74.67/18.91 thf(123,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | ((A @ sk5) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[96,15])).
% 74.67/18.91 thf(124,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[123])).
% 74.67/18.91 thf(139,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4))),inference(pre_uni,[status(thm)],[124:[bind(A, $thf(^ [B:$i]: (sk1 @ B @ B)))]])).
% 74.67/18.91 thf(161,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[139,11])).
% 74.67/18.91 thf(162,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[161])).
% 74.67/18.91 thf(163,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[162:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4))]])).
% 74.67/18.91 thf(313,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[96,163])).
% 74.67/18.91 thf(314,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4) @ sk5)))),inference(simp,[status(thm)],[313])).
% 74.67/18.91 thf(339,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[314:[bind(A, $thf(sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)))]])).
% 74.67/18.91 thf(939,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[339,11])).
% 74.67/18.91 thf(940,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[939])).
% 74.67/18.91 thf(941,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[940:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) @ sk4))]])).
% 74.67/18.91 thf(44,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | (~ (sk1 @ sk4 @ D)) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ D @ sk5)))),inference(paramod_ordered,[status(thm)],[7,11])).
% 74.67/18.91 thf(45,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | (~ (sk1 @ sk4 @ D)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ D @ sk5)))),inference(simp,[status(thm)],[44])).
% 74.67/18.91 thf(77,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((B @ C) | (~ (sk1 @ A @ C)) | (~ (sk1 @ sk4 @ D)) | (A != D) | ((sk2 @ (B) @ A) != sk5))),inference(simp,[status(thm)],[45])).
% 74.67/18.91 thf(88,plain,(! [C:$i,B:$i,A:($i > $o)] : ((A @ B) | (~ (sk1 @ C @ B)) | (~ (sk1 @ sk4 @ C)) | ((sk2 @ (A) @ C) != sk5))),inference(simp,[status(thm)],[77])).
% 74.67/18.91 thf(138,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4))),inference(pre_uni,[status(thm)],[124:[bind(A, $thf(sk1 @ sk5))]])).
% 74.67/18.91 thf(108,plain,(! [A:($i > $o)] : ((A @ sk5) | ~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[96,18])).
% 74.67/18.91 thf(109,plain,(! [A:($i > $o)] : ((A @ sk5) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ sk4)))),inference(simp,[status(thm)],[108])).
% 74.67/18.91 thf(135,plain,(! [A:($i > $o)] : ((A @ sk5) | (sk4 != sk4) | ((sk2 @ (A) @ sk4) != sk4))),inference(simp,[status(thm)],[109])).
% 74.67/18.91 thf(149,plain,(! [A:($i > $o)] : ((A @ sk5) | ((sk2 @ (A) @ sk4) != sk4))),inference(simp,[status(thm)],[135])).
% 74.67/18.91 thf(1145,plain,(! [A:($i > $o)] : ((~ (A @ sk5)) | ((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4))),inference(prim_subst,[status(thm)],[149:[bind(A, $thf(^ [C:$i]: ~ (B @ C)))]])).
% 74.67/18.91 thf(1189,plain,(! [A:($i > $o)] : ((~ (A @ sk5)) | ((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4))),inference(cnf,[status(esa)],[1145])).
% 74.67/18.91 thf(1190,plain,(! [A:($i > $o)] : ((~ (A @ sk5)) | ((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4))),inference(simp,[status(thm)],[1189])).
% 74.67/18.91 thf(137,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4))),inference(pre_uni,[status(thm)],[124:[bind(A, $thf(^ [B:$i]: (sk1 @ B @ sk5)))]])).
% 74.67/18.91 thf(397,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[137,11])).
% 74.67/18.91 thf(398,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[397])).
% 74.67/18.91 thf(399,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[398:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4))]])).
% 74.67/18.91 thf(677,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[96,399])).
% 74.67/18.91 thf(678,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4) @ sk5)))),inference(simp,[status(thm)],[677])).
% 74.67/18.91 thf(697,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4))),inference(pre_uni,[status(thm)],[678:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)))]])).
% 74.67/18.91 thf(1071,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[697,11])).
% 74.67/18.91 thf(1072,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[1071])).
% 74.67/18.91 thf(1073,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[1072:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)) @ sk4))]])).
% 74.67/18.91 thf(425,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[138,11])).
% 74.67/18.91 thf(426,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[425])).
% 74.67/18.91 thf(427,plain,((~ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[426:[bind(A, $thf(sk2 @ (sk1 @ sk5) @ sk4))]])).
% 74.67/18.91 thf(1139,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[149,427])).
% 74.67/18.91 thf(1140,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ((A @ sk5) != (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4) @ sk5)))),inference(simp,[status(thm)],[1139])).
% 74.67/18.91 thf(1173,plain,(((sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ A)) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[1140:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ B)))]])).
% 74.67/18.91 thf(127,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) | ($false)),inference(prim_subst,[status(thm)],[96:[bind(A, $thf(^ [B:$i]: (($false))))]])).
% 74.67/18.91 thf(155,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4))),inference(simp,[status(thm)],[127])).
% 74.67/18.91 thf(280,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[155,11])).
% 74.67/18.91 thf(281,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[280])).
% 74.67/18.91 thf(282,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[281:[bind(A, $thf(sk2 @ (^ [B:$i]: (($false))) @ sk4))]])).
% 74.67/18.91 thf(352,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[96,282])).
% 74.67/18.91 thf(353,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4) @ sk5)))),inference(simp,[status(thm)],[352])).
% 74.67/18.91 thf(384,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[353:[bind(A, $thf(sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)))]])).
% 74.67/18.91 thf(1122,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[149,399])).
% 74.67/18.91 thf(1123,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ((A @ sk5) != (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4) @ sk5)))),inference(simp,[status(thm)],[1122])).
% 74.67/18.91 thf(1164,plain,(((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4)) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[1123:[bind(A, $thf(sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)))]])).
% 74.67/18.91 thf(14164,plain,(! [A:($i > $o)] : (~ (($true)) | ((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (A @ sk5)))),inference(paramod_ordered,[status(thm)],[138,1190])).
% 74.67/18.91 thf(14165,plain,(! [A:($i > $o)] : (((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (A @ sk5)))),inference(simp,[status(thm)],[14164])).
% 74.67/18.91 thf(14301,plain,(((sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ (sk2 @ (sk1 @ A) @ sk4))) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[14165:[bind(A, $thf(^ [B:$i]: (sk1 @ sk4 @ (sk2 @ (sk1 @ B) @ sk4))))]])).
% 74.67/18.91 thf(58,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ((B @ C) != (~ (sk1 @ A @ C))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[7])).
% 74.67/18.91 thf(74,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((sk1 @ (B @ A) @ (sk2 @ (^ [D:$i]: ~ (sk1 @ (B @ D) @ (C @ D))) @ (B @ A))) | (~ (sk1 @ (B @ A) @ A)) | ((C @ A) != A))),inference(pre_uni,[status(thm)],[58:[bind(A, $thf(E @ C)),bind(B, $thf(^ [F:$i]: ~ (sk1 @ (E @ F) @ (F @ F)))),bind(C, $thf(C))]])).
% 74.67/18.91 thf(75,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((~ (sk1 @ (B @ A) @ A)) | (sk1 @ (B @ A) @ (sk2 @ (^ [D:$i]: ~ (sk1 @ (B @ D) @ (C @ D))) @ (B @ A))) | ((C @ A) != A))),inference(pre_uni,[status(thm)],[74:[]])).
% 74.67/18.91 thf(86,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((~ (sk1 @ (B @ A) @ A)) | (sk1 @ (B @ A) @ (sk2 @ (^ [D:$i]: ~ (sk1 @ (B @ D) @ (C @ D))) @ (B @ A))) | ((C @ A) != A))),inference(simp,[status(thm)],[75])).
% 74.67/18.91 thf(5149,plain,(! [C:($i > $i),B:($i > $i),A:$i] : (~ (($true)) | (sk1 @ (B @ A) @ (sk2 @ (^ [D:$i]: ~ (sk1 @ (B @ D) @ (C @ D))) @ (B @ A))) | ((C @ A) != A) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ (sk2 @ (^ [E:$i]: (sk1 @ E @ D)) @ sk4) @ D)) @ sk4)) != (sk1 @ (B @ A) @ A)))),inference(paramod_ordered,[status(thm)],[697,86])).
% 74.67/18.91 thf(5150,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((sk1 @ (B @ A) @ (sk2 @ (^ [D:$i]: ~ (sk1 @ (B @ D) @ (C @ D))) @ (B @ A))) | ((C @ A) != A) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ (sk2 @ (^ [E:$i]: (sk1 @ E @ D)) @ sk4) @ D)) @ sk4)) != (sk1 @ (B @ A) @ A)))),inference(simp,[status(thm)],[5149])).
% 74.67/18.91 thf(5276,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ (A @ B))) @ sk4)) | ((A @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)) @ sk4)) != (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ B)) @ sk4)))),inference(pre_uni,[status(thm)],[5150:[bind(A, $thf(sk2 @ (^ [D:$i]: (sk1 @ (sk2 @ (^ [E:$i]: (sk1 @ E @ D)) @ sk4) @ D)) @ sk4)),bind(B, $thf(^ [D:$i]: (sk4)))]])).
% 74.67/18.91 thf(5277,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4))),inference(pre_uni,[status(thm)],[5276:[bind(A, $thf(^ [B:$i]: (B)))]])).
% 74.67/18.91 thf(119,plain,(! [B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (~ (sk1 @ sk4 @ B)) | ~ (($true)) | ((A @ sk5) != (sk1 @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[96,11])).
% 74.67/18.91 thf(120,plain,(! [B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (~ (sk1 @ sk4 @ B)) | ((A @ sk5) != (sk1 @ B @ sk5)))),inference(simp,[status(thm)],[119])).
% 74.67/18.91 thf(131,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | (~ (sk1 @ sk4 @ (A @ sk5))))),inference(pre_uni,[status(thm)],[120:[bind(A, $thf(^ [D:$i]: (sk1 @ (C @ D) @ D))),bind(B, $thf(C @ sk5))]])).
% 74.67/18.91 thf(146,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | (~ (sk1 @ sk4 @ (A @ sk5))))),inference(simp,[status(thm)],[131])).
% 74.67/18.91 thf(18746,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | ~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) != (sk1 @ sk4 @ (A @ sk5))))),inference(paramod_ordered,[status(thm)],[5277,146])).
% 74.67/18.91 thf(18747,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) != (sk1 @ sk4 @ (A @ sk5))))),inference(simp,[status(thm)],[18746])).
% 74.67/18.91 thf(18933,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[18747:[bind(A, $thf(^ [B:$i]: (sk2 @ (^ [C:$i]: ~ (sk1 @ sk4 @ C)) @ sk4)))]])).
% 74.67/18.91 thf(274,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (($false))) @ sk4)) != (sk1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[155,7])).
% 74.67/18.91 thf(275,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (B @ C) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (($false))) @ sk4)) != (sk1 @ A @ C)))),inference(simp,[status(thm)],[274])).
% 74.67/18.91 thf(276,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)))),inference(pattern_uni,[status(thm)],[275:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(sk2 @ (^ [D:$i]: (($false))) @ sk4))]])).
% 74.67/18.91 thf(295,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)))),inference(simp,[status(thm)],[276])).
% 74.67/18.91 thf(125,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ sk4 @ (sk2 @ (A) @ sk4))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[96])).
% 74.67/18.91 thf(132,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ sk4 @ (sk2 @ (A) @ sk4))))),inference(simp,[status(thm)],[125])).
% 74.67/18.91 thf(15789,plain,(! [B:($i > $o),A:($i > $o)] : ((A @ (sk2 @ (^ [C:$i]: (($false))) @ sk4)) | (sk1 @ sk4 @ (sk2 @ (B) @ sk4)) | (~ (B @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ (sk2 @ (B) @ sk4))))),inference(paramod_ordered,[status(thm)],[295,132])).
% 74.67/18.91 thf(15790,plain,(! [A:($i > $o)] : ((A @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) | (sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (~ (A @ sk5)))),inference(pattern_uni,[status(thm)],[15789:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 74.67/18.91 thf(15825,plain,((sk5 = (sk2 @ (^ [A:$i]: (($false))) @ sk4)) | (sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) | (~ (sk5 = sk5))),inference(replace_leibeq,[status(thm)],[15790:[bind(A, $thf((=) @ $i @ sk5))]])).
% 74.67/18.91 thf(15829,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5) | (sk5 != sk5) | (sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4))),inference(lifteq,[status(thm)],[15825])).
% 74.67/18.91 thf(15881,plain,((sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) | ((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5)),inference(pattern_uni,[status(thm)],[15829:[]])).
% 74.67/18.91 thf(19,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | ((sk1 @ A @ sk5) != (sk1 @ sk4 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[11])).
% 74.67/18.91 thf(20,plain,(! [A:$i] : ((~ (sk1 @ sk4 @ A)) | ((sk1 @ A @ sk5) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[19])).
% 74.67/18.91 thf(46,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ~ (($true)) | (~ (sk1 @ D @ sk5)) | ((B @ C) != (sk1 @ sk4 @ D)))),inference(paramod_ordered,[status(thm)],[7,11])).
% 74.67/18.91 thf(47,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (~ (sk1 @ D @ sk5)) | ((B @ C) != (sk1 @ sk4 @ D)))),inference(simp,[status(thm)],[46])).
% 74.67/18.91 thf(82,plain,(! [B:($i > $i),A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ C @ (B @ C))) @ A)) | (~ (sk1 @ A @ sk4)) | (~ (sk1 @ (B @ sk4) @ sk5)))),inference(pre_uni,[status(thm)],[47:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (sk1 @ F @ (F @ F)))),bind(C, $thf(sk4)),bind(D, $thf(F @ sk4))]])).
% 74.67/18.91 thf(93,plain,(! [B:($i > $i),A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ C @ (B @ C))) @ A)) | (~ (sk1 @ A @ sk4)) | (~ (sk1 @ (B @ sk4) @ sk5)))),inference(simp,[status(thm)],[82])).
% 74.67/18.91 thf(402,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[137,18])).
% 74.67/18.91 thf(403,plain,(((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[402])).
% 74.67/18.91 thf(411,plain,((sk4 != sk4) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4) != sk4)),inference(simp,[status(thm)],[403])).
% 74.67/18.91 thf(416,plain,(((sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4) != sk4)),inference(simp,[status(thm)],[411])).
% 74.67/18.91 thf(112,plain,(! [B:$i,A:($i > $o)] : ((A @ sk5) | ~ (($true)) | (~ (sk1 @ B @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ B)))),inference(paramod_ordered,[status(thm)],[96,11])).
% 74.67/18.91 thf(113,plain,(! [B:$i,A:($i > $o)] : ((A @ sk5) | (~ (sk1 @ B @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ B)))),inference(simp,[status(thm)],[112])).
% 74.67/18.91 thf(114,plain,(! [A:($i > $o)] : ((A @ sk5) | (~ (sk1 @ (sk2 @ (A) @ sk4) @ sk5)))),inference(pattern_uni,[status(thm)],[113:[bind(A, $thf(C)),bind(B, $thf(sk2 @ (C) @ sk4))]])).
% 74.67/18.91 thf(152,plain,(! [A:($i > $o)] : ((A @ sk5) | (~ (sk1 @ (sk2 @ (A) @ sk4) @ sk5)))),inference(simp,[status(thm)],[114])).
% 74.67/18.91 thf(730,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | ((A @ sk5) != (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4) @ sk5)))),inference(paramod_ordered,[status(thm)],[96,427])).
% 74.67/18.91 thf(731,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ((A @ sk5) != (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4) @ sk5)))),inference(simp,[status(thm)],[730])).
% 74.67/18.91 thf(756,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[731:[bind(A, $thf(sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)))]])).
% 74.67/18.91 thf(37,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[7,18])).
% 74.67/18.91 thf(38,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk4 @ sk4)))),inference(simp,[status(thm)],[37])).
% 74.67/18.91 thf(69,plain,(! [C:$i,B:($i > $o),A:$i] : ((B @ C) | (~ (sk1 @ A @ C)) | (A != sk4) | ((sk2 @ (B) @ A) != sk4))),inference(simp,[status(thm)],[38])).
% 74.67/18.91 thf(84,plain,(! [B:$i,A:($i > $o)] : ((A @ B) | (~ (sk1 @ sk4 @ B)) | ((sk2 @ (A) @ sk4) != sk4))),inference(simp,[status(thm)],[69])).
% 74.67/18.91 thf(278,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[155,18])).
% 74.67/18.91 thf(279,plain,(((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[278])).
% 74.67/18.91 thf(288,plain,((sk4 != sk4) | ((sk2 @ (^ [A:$i]: (($false))) @ sk4) != sk4)),inference(simp,[status(thm)],[279])).
% 74.67/18.91 thf(293,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) != sk4)),inference(simp,[status(thm)],[288])).
% 74.67/18.91 thf(53,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[7,15])).
% 74.67/18.91 thf(54,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[53])).
% 74.67/18.91 thf(78,plain,(! [C:$i,B:($i > $o),A:$i] : ((B @ C) | (~ (sk1 @ A @ C)) | (A != sk5) | ((sk2 @ (B) @ A) != sk5))),inference(simp,[status(thm)],[54])).
% 74.67/18.91 thf(89,plain,(! [B:$i,A:($i > $o)] : ((A @ B) | (~ (sk1 @ sk5 @ B)) | ((sk2 @ (A) @ sk5) != sk5))),inference(simp,[status(thm)],[78])).
% 74.67/18.91 thf(3489,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ A)) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[73,15])).
% 74.67/18.91 thf(3490,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ A)) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[3489])).
% 74.67/18.91 thf(3528,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | (A != sk5) | ((sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ A) != sk5))),inference(simp,[status(thm)],[3490])).
% 74.67/18.91 thf(3582,plain,((~ (sk1 @ sk5 @ sk4)) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk5) != sk5)),inference(simp,[status(thm)],[3528])).
% 74.67/18.91 thf(6,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ (sk2 @ (B) @ A) @ (sk3 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[4])).
% 74.67/18.91 thf(1163,plain,(((sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ sk5)) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[1123:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ sk5)))]])).
% 74.67/18.91 thf(755,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ sk5)) @ sk4))),inference(pre_uni,[status(thm)],[731:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ sk5)))]])).
% 74.67/18.91 thf(2426,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[755,11])).
% 74.67/18.91 thf(2427,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[2426])).
% 74.67/18.91 thf(2428,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ sk5)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[2427:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ sk5)) @ sk4))]])).
% 74.67/18.91 thf(18566,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | ~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ (A @ sk5))))),inference(paramod_ordered,[status(thm)],[384,146])).
% 74.67/18.91 thf(18567,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ B)) @ sk4)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ (A @ sk5))))),inference(simp,[status(thm)],[18566])).
% 74.67/18.91 thf(18911,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[18567:[bind(A, $thf(^ [B:$i]: (sk2 @ (sk1 @ (sk2 @ (^ [C:$i]: (($false))) @ sk4)) @ sk4)))]])).
% 74.67/18.91 thf(19701,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[18911,11])).
% 74.67/18.91 thf(19702,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[19701])).
% 74.67/18.91 thf(19703,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[19702:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) @ sk4))]])).
% 74.67/18.91 thf(81,plain,(! [C:($i > $i),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: (sk1 @ sk4 @ (C @ D))) @ A)) | (~ (sk1 @ A @ B)) | (~ (sk1 @ (C @ B) @ sk5)))),inference(pre_uni,[status(thm)],[47:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (sk1 @ sk4 @ (F @ F)))),bind(C, $thf(C)),bind(D, $thf(F @ C))]])).
% 74.67/18.91 thf(92,plain,(! [C:($i > $i),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: (sk1 @ sk4 @ (C @ D))) @ A)) | (~ (sk1 @ A @ B)) | (~ (sk1 @ (C @ B) @ sk5)))),inference(simp,[status(thm)],[81])).
% 74.67/18.91 thf(71,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk4)) @ A)) | (~ (sk1 @ A @ sk4)))),inference(pre_uni,[status(thm)],[40:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (sk1 @ D @ sk4))),bind(C, $thf(sk4))]])).
% 74.67/18.91 thf(2690,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk4)) @ A)) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[71,15])).
% 74.67/18.91 thf(2691,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk4)) @ A)) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[2690])).
% 74.67/18.91 thf(2712,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | (A != sk5) | ((sk2 @ (^ [B:$i]: (sk1 @ B @ sk4)) @ A) != sk5))),inference(simp,[status(thm)],[2691])).
% 74.67/18.91 thf(2758,plain,((~ (sk1 @ sk5 @ sk4)) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ sk4)) @ sk5) != sk5)),inference(simp,[status(thm)],[2712])).
% 74.67/18.91 thf(55,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ~ (($true)) | ((B @ C) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[7,15])).
% 74.67/18.91 thf(56,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ((B @ C) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[55])).
% 74.67/18.91 thf(65,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (sk1 @ sk5) @ A)) | (~ (sk1 @ A @ sk5)))),inference(pre_uni,[status(thm)],[56:[bind(A, $thf(A)),bind(B, $thf(sk1 @ sk5)),bind(C, $thf(sk5))]])).
% 74.67/18.91 thf(757,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ A)) @ sk4))),inference(pre_uni,[status(thm)],[731:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ B)))]])).
% 74.67/18.91 thf(19201,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[18933,11])).
% 74.67/18.91 thf(19202,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[19201])).
% 74.67/18.91 thf(19203,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[19202:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) @ sk4))]])).
% 74.67/18.91 thf(9,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk3 @ (B) @ A))) | (~ (sk1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[4])).
% 74.67/18.91 thf(70,plain,(! [B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ sk4 @ sk4)) @ A)) | (~ (sk1 @ A @ B)))),inference(pre_uni,[status(thm)],[40:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (sk1 @ sk4 @ sk4))),bind(C, $thf(C))]])).
% 74.67/18.91 thf(85,plain,(! [B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ sk4 @ sk4)) @ A)) | (~ (sk1 @ A @ B)))),inference(simp,[status(thm)],[70])).
% 74.67/18.91 thf(4804,plain,(! [B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (($false))) @ A)) | (~ (sk1 @ A @ B)))),inference(rewrite,[status(thm)],[85,18])).
% 74.67/18.91 thf(156,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ D @ D)) @ sk4)) != (sk1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[139,7])).
% 74.67/18.91 thf(157,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (B @ C) | ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ D @ D)) @ sk4)) != (sk1 @ A @ C)))),inference(simp,[status(thm)],[156])).
% 74.67/18.91 thf(158,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)))),inference(pattern_uni,[status(thm)],[157:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(sk2 @ (^ [D:$i]: (sk1 @ D @ D)) @ sk4))]])).
% 74.67/18.91 thf(173,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)))),inference(simp,[status(thm)],[158])).
% 74.67/18.91 thf(17529,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5) | ~ (($true)) | ((sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[15881,18])).
% 74.67/18.91 thf(17530,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5) | ((sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[17529])).
% 74.67/18.91 thf(17655,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5) | (sk4 != sk4) | ((sk2 @ ((=) @ $i @ sk5) @ sk4) != sk4)),inference(simp,[status(thm)],[17530])).
% 74.67/18.91 thf(17858,plain,(((sk2 @ (^ [A:$i]: (($false))) @ sk4) = sk5) | ((sk2 @ ((=) @ $i @ sk5) @ sk4) != sk4)),inference(simp,[status(thm)],[17655])).
% 74.67/18.91 thf(1081,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[697,18])).
% 74.67/18.91 thf(1082,plain,(((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[1081])).
% 74.67/18.91 thf(1097,plain,((sk4 != sk4) | ((sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[1082])).
% 74.67/18.91 thf(1103,plain,(((sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[1097])).
% 74.67/18.91 thf(117,plain,(! [B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | ~ (($true)) | (~ (sk1 @ B @ sk5)) | ((A @ sk5) != (sk1 @ sk4 @ B)))),inference(paramod_ordered,[status(thm)],[96,11])).
% 74.67/18.91 thf(118,plain,(! [B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (~ (sk1 @ B @ sk5)) | ((A @ sk5) != (sk1 @ sk4 @ B)))),inference(simp,[status(thm)],[117])).
% 74.67/18.91 thf(134,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ sk4 @ (A @ B))) @ sk4)) | (~ (sk1 @ (A @ sk5) @ sk5)))),inference(pre_uni,[status(thm)],[118:[bind(A, $thf(^ [D:$i]: (sk1 @ sk4 @ (D @ D)))),bind(B, $thf(D @ sk5))]])).
% 74.67/18.91 thf(148,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ sk4 @ (A @ B))) @ sk4)) | (~ (sk1 @ (A @ sk5) @ sk5)))),inference(simp,[status(thm)],[134])).
% 74.67/18.91 thf(64,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ A)) | (~ (sk1 @ A @ sk5)))),inference(pre_uni,[status(thm)],[56:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (sk1 @ D @ sk5))),bind(C, $thf(sk5))]])).
% 74.67/18.91 thf(430,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[138,18])).
% 74.67/18.91 thf(431,plain,(((sk1 @ sk4 @ (sk2 @ (sk1 @ sk5) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[430])).
% 74.67/18.91 thf(439,plain,((sk4 != sk4) | ((sk2 @ (sk1 @ sk5) @ sk4) != sk4)),inference(simp,[status(thm)],[431])).
% 74.67/18.91 thf(444,plain,(((sk2 @ (sk1 @ sk5) @ sk4) != sk4)),inference(simp,[status(thm)],[439])).
% 74.67/18.91 thf(10,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk3 @ (B) @ A) = (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A))) | (~ (sk1 @ A @ C)) | ((sk3 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[9:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk3 @ B @ A)))]])).
% 74.67/18.91 thf(12,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk3 @ (B) @ A) != (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A)) | ((sk3 @ (B) @ A) = C) | (~ (sk1 @ A @ C)))),inference(lifteq,[status(thm)],[10])).
% 74.67/18.91 thf(129,plain,(! [B:($i > $o),A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [C:$i]: ((A @ C) | (B @ C))) @ sk4)) | ((A @ sk5) | (B @ sk5)))),inference(prim_subst,[status(thm)],[96:[bind(A, $thf(^ [D:$i]: ((B @ D) | (C @ D))))]])).
% 74.67/18.91 thf(143,plain,(! [B:($i > $o),A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [C:$i]: ((A @ C) | (B @ C))) @ sk4)) | (A @ sk5) | (B @ sk5))),inference(cnf,[status(esa)],[129])).
% 74.67/18.91 thf(144,plain,(! [B:($i > $o),A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [C:$i]: ((A @ C) | (B @ C))) @ sk4)) | (A @ sk5) | (B @ sk5))),inference(simp,[status(thm)],[143])).
% 74.67/18.91 thf(5517,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[5277,18])).
% 74.67/18.91 thf(5518,plain,(((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[5517])).
% 74.67/18.91 thf(5549,plain,((sk4 != sk4) | ((sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[5518])).
% 74.67/18.91 thf(5578,plain,(((sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[5549])).
% 74.67/18.91 thf(695,plain,((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ sk5)) @ sk4))),inference(pre_uni,[status(thm)],[678:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ sk5)))]])).
% 74.67/18.91 thf(2255,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[695,11])).
% 74.67/18.91 thf(2256,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ sk5)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[2255])).
% 74.67/18.91 thf(2257,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4) @ sk5)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[2256:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4) @ sk5)) @ sk4))]])).
% 74.67/18.91 thf(59,plain,(! [C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (sk1 @ A @ B)) | (~ (C @ B)))),inference(prim_subst,[status(thm)],[7:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: ~ (D @ E)))]])).
% 74.67/18.91 thf(97,plain,(! [C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (sk1 @ A @ B)) | (~ (C @ B)))),inference(cnf,[status(esa)],[59])).
% 74.67/18.91 thf(98,plain,(! [C:($i > $o),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (sk1 @ A @ B)) | (~ (C @ B)))),inference(simp,[status(thm)],[97])).
% 74.67/18.91 thf(72,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (sk1 @ sk4) @ A)) | (~ (sk1 @ A @ sk4)))),inference(pre_uni,[status(thm)],[40:[bind(A, $thf(A)),bind(B, $thf(sk1 @ sk4)),bind(C, $thf(sk4))]])).
% 74.67/18.91 thf(3078,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (sk1 @ sk4) @ A)) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[72,15])).
% 74.67/18.91 thf(3079,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | ((sk1 @ A @ (sk2 @ (sk1 @ sk4) @ A)) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[3078])).
% 74.67/18.91 thf(3110,plain,(! [A:$i] : ((~ (sk1 @ A @ sk4)) | (A != sk5) | ((sk2 @ (sk1 @ sk4) @ A) != sk5))),inference(simp,[status(thm)],[3079])).
% 74.67/18.91 thf(3160,plain,((~ (sk1 @ sk5 @ sk4)) | ((sk2 @ (sk1 @ sk4) @ sk5) != sk5)),inference(simp,[status(thm)],[3110])).
% 74.67/18.91 thf(696,plain,((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4)) @ sk4))),inference(pre_uni,[status(thm)],[678:[bind(A, $thf(sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)))]])).
% 74.67/18.91 thf(2341,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[696,11])).
% 74.67/18.91 thf(2342,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[2341])).
% 74.67/18.91 thf(2343,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ sk5)) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[2342:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) @ sk4))]])).
% 74.67/18.91 thf(48,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (~ (sk1 @ sk4 @ D)) | ~ (($true)) | ((B @ C) != (sk1 @ D @ sk5)))),inference(paramod_ordered,[status(thm)],[7,11])).
% 74.67/18.91 thf(49,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | (~ (sk1 @ sk4 @ D)) | ((B @ C) != (sk1 @ D @ sk5)))),inference(simp,[status(thm)],[48])).
% 74.67/18.91 thf(80,plain,(! [B:($i > $i),A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ (B @ C) @ C)) @ A)) | (~ (sk1 @ A @ sk5)) | (~ (sk1 @ sk4 @ (B @ sk5))))),inference(pre_uni,[status(thm)],[49:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (sk1 @ (E @ F) @ F))),bind(C, $thf(sk5)),bind(D, $thf(E @ sk5))]])).
% 74.67/18.91 thf(91,plain,(! [B:($i > $i),A:$i] : ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ (B @ C) @ C)) @ A)) | (~ (sk1 @ A @ sk5)) | (~ (sk1 @ sk4 @ (B @ sk5))))),inference(simp,[status(thm)],[80])).
% 74.67/18.91 thf(66,plain,(! [A:$i] : ((sk1 @ A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ A)) | (~ (sk1 @ A @ sk5)))),inference(pre_uni,[status(thm)],[56:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (sk1 @ D @ D))),bind(C, $thf(sk5))]])).
% 74.67/18.91 thf(1004,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[384,18])).
% 74.67/18.91 thf(1005,plain,(((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[1004])).
% 74.67/18.91 thf(1024,plain,((sk4 != sk4) | ((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[1005])).
% 74.67/18.91 thf(1029,plain,(((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[1024])).
% 74.67/18.91 thf(4968,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A @ B)) | ~ (($true)) | ((sk1 @ A @ (sk2 @ (^ [C:$i]: (($false))) @ A)) != (sk1 @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[4804,15])).
% 74.67/18.91 thf(4969,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A @ B)) | ((sk1 @ A @ (sk2 @ (^ [C:$i]: (($false))) @ A)) != (sk1 @ sk5 @ sk5)))),inference(simp,[status(thm)],[4968])).
% 74.67/18.91 thf(5023,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A @ B)) | (A != sk5) | ((sk2 @ (^ [C:$i]: (($false))) @ A) != sk5))),inference(simp,[status(thm)],[4969])).
% 74.67/18.91 thf(5060,plain,(! [A:$i] : ((~ (sk1 @ sk5 @ A)) | ((sk2 @ (^ [B:$i]: (($false))) @ sk5) != sk5))),inference(simp,[status(thm)],[5023])).
% 74.67/18.91 thf(7504,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A @ sk4)) | ~ (($true)) | ((sk2 @ (^ [C:$i]: (($false))) @ sk5) != sk5) | ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ C @ C)) @ A)) != (sk1 @ sk5 @ B)))),inference(paramod_ordered,[status(thm)],[73,5060])).
% 74.67/18.91 thf(7505,plain,(! [B:$i,A:$i] : ((~ (sk1 @ A @ sk4)) | ((sk2 @ (^ [C:$i]: (($false))) @ sk5) != sk5) | ((sk1 @ A @ (sk2 @ (^ [C:$i]: (sk1 @ C @ C)) @ A)) != (sk1 @ sk5 @ B)))),inference(simp,[status(thm)],[7504])).
% 74.67/18.91 thf(7506,plain,((~ (sk1 @ sk5 @ sk4)) | ((sk2 @ (^ [A:$i]: (($false))) @ sk5) != sk5)),inference(pattern_uni,[status(thm)],[7505:[bind(A, $thf(sk5)),bind(B, $thf(sk2 @ (^ [C:$i]: (sk1 @ C @ C)) @ sk5))]])).
% 74.67/18.91 thf(8997,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ~ (($true)) | ((sk2 @ (^ [B:$i]: (($false))) @ sk5) != sk5) | ((A @ sk5) != (sk1 @ sk5 @ sk4)))),inference(paramod_ordered,[status(thm)],[149,7506])).
% 74.67/18.91 thf(8998,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ((sk2 @ (^ [B:$i]: (($false))) @ sk5) != sk5) | ((A @ sk5) != (sk1 @ sk5 @ sk4)))),inference(simp,[status(thm)],[8997])).
% 74.67/18.91 thf(9074,plain,(((sk2 @ (^ [A:$i]: (sk1 @ A @ sk4)) @ sk4) != sk4) | ((sk2 @ (^ [A:$i]: (($false))) @ sk5) != sk5)),inference(pre_uni,[status(thm)],[8998:[bind(A, $thf(^ [B:$i]: (sk1 @ B @ sk4)))]])).
% 74.67/18.91 thf(1171,plain,(((sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ sk5)) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[1140:[bind(A, $thf(^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ sk5)))]])).
% 74.67/18.91 thf(998,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[384,11])).
% 74.67/18.91 thf(999,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[998])).
% 74.67/18.91 thf(1000,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[999:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (^ [B:$i]: (($false))) @ sk4)) @ sk4))]])).
% 74.67/18.91 thf(1411,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[757,11])).
% 74.67/18.91 thf(1412,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[1411])).
% 74.67/18.91 thf(1413,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ (sk2 @ (sk1 @ A) @ sk4) @ A)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[1412:[bind(A, $thf(sk2 @ (^ [B:$i]: (sk1 @ (sk2 @ (sk1 @ B) @ sk4) @ B)) @ sk4))]])).
% 74.67/18.91 thf(130,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ sk5)) @ sk4)) | (~ (sk1 @ sk4 @ (A @ sk5))))),inference(pre_uni,[status(thm)],[120:[bind(A, $thf(^ [D:$i]: (sk1 @ (C @ D) @ sk5))),bind(B, $thf(C @ sk5))]])).
% 74.67/18.91 thf(145,plain,(! [A:($i > $i)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ (A @ B) @ sk5)) @ sk4)) | (~ (sk1 @ sk4 @ (A @ sk5))))),inference(simp,[status(thm)],[130])).
% 74.67/18.91 thf(103,plain,(! [D:$i,C:($i > $o),B:$i,A:($i > $o)] : ((A @ sk5) | (sk1 @ B @ (sk2 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[96,7])).
% 74.67/18.91 thf(104,plain,(! [D:$i,C:($i > $o),B:$i,A:($i > $o)] : ((A @ sk5) | (sk1 @ B @ (sk2 @ (C) @ B)) | (C @ D) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ B @ D)))),inference(simp,[status(thm)],[103])).
% 74.67/18.91 thf(105,plain,(! [B:($i > $o),A:($i > $o)] : ((B @ sk5) | (sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (B) @ sk4)))),inference(pattern_uni,[status(thm)],[104:[bind(A, $thf(E)),bind(B, $thf(sk4)),bind(C, $thf(C)),bind(D, $thf(sk2 @ (E) @ sk4))]])).
% 74.67/18.91 thf(150,plain,(! [B:($i > $o),A:($i > $o)] : ((B @ sk5) | (sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (A @ (sk2 @ (B) @ sk4)))),inference(simp,[status(thm)],[105])).
% 74.67/18.91 thf(41,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | ~ (($true)) | (~ (sk1 @ D @ sk5)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk4 @ D)))),inference(paramod_ordered,[status(thm)],[7,11])).
% 74.67/18.91 thf(42,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | (~ (sk1 @ D @ sk5)) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ sk4 @ D)))),inference(simp,[status(thm)],[41])).
% 74.67/18.91 thf(43,plain,(! [B:($i > $o),A:$i] : ((~ (sk1 @ sk4 @ A)) | (B @ A) | (~ (sk1 @ (sk2 @ (B) @ sk4) @ sk5)))),inference(pattern_uni,[status(thm)],[42:[bind(A, $thf(sk4)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk2 @ (E) @ sk4))]])).
% 74.67/18.91 thf(95,plain,(! [B:($i > $o),A:$i] : ((~ (sk1 @ sk4 @ A)) | (B @ A) | (~ (sk1 @ (sk2 @ (B) @ sk4) @ sk5)))),inference(simp,[status(thm)],[43])).
% 74.67/18.91 thf(5521,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[5277,11])).
% 74.67/18.91 thf(5522,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[5521])).
% 74.67/18.91 thf(5523,plain,((~ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[5522:[bind(A, $thf(sk2 @ (^ [B:$i]: ~ (sk1 @ sk4 @ B)) @ sk4))]])).
% 74.67/18.91 thf(19686,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[18911,18])).
% 74.67/18.91 thf(19687,plain,(((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[19686])).
% 74.67/18.91 thf(19748,plain,((sk4 != sk4) | ((sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[19687])).
% 74.67/18.91 thf(19816,plain,(((sk2 @ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (($false))) @ sk4)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[19748])).
% 74.67/18.91 thf(15749,plain,(! [B:($i > $o),A:($i > $o)] : ((A @ (sk2 @ (^ [C:$i]: (sk1 @ C @ C)) @ sk4)) | (sk1 @ sk4 @ (sk2 @ (B) @ sk4)) | (~ (B @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) != (sk1 @ sk4 @ (sk2 @ (B) @ sk4))))),inference(paramod_ordered,[status(thm)],[173,132])).
% 74.67/18.91 thf(15750,plain,(! [A:($i > $o)] : ((A @ (sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk4)) | (sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (~ (A @ sk5)))),inference(pattern_uni,[status(thm)],[15749:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 74.67/18.91 thf(15824,plain,((sk5 = (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) | (sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) | (~ (sk5 = sk5))),inference(replace_leibeq,[status(thm)],[15750:[bind(A, $thf((=) @ $i @ sk5))]])).
% 74.67/18.91 thf(15827,plain,(((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4) = sk5) | (sk5 != sk5) | (sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4))),inference(lifteq,[status(thm)],[15824])).
% 74.67/18.91 thf(15846,plain,((sk1 @ sk4 @ (sk2 @ ((=) @ $i @ sk5) @ sk4)) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4) = sk5)),inference(pattern_uni,[status(thm)],[15827:[]])).
% 74.67/18.91 thf(126,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4)) | (~ (A @ sk5)))),inference(prim_subst,[status(thm)],[96:[bind(A, $thf(^ [C:$i]: ~ (B @ C)))]])).
% 74.67/18.91 thf(153,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4)) | (~ (A @ sk5)))),inference(cnf,[status(esa)],[126])).
% 74.67/18.91 thf(154,plain,(! [A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4)) | (~ (A @ sk5)))),inference(simp,[status(thm)],[153])).
% 74.67/18.91 thf(3644,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ~ (($true)) | ((sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk5) != sk5) | ((A @ sk5) != (sk1 @ sk5 @ sk4)))),inference(paramod_ordered,[status(thm)],[149,3582])).
% 74.67/18.91 thf(3645,plain,(! [A:($i > $o)] : (((sk2 @ (A) @ sk4) != sk4) | ((sk2 @ (^ [B:$i]: (sk1 @ B @ B)) @ sk5) != sk5) | ((A @ sk5) != (sk1 @ sk5 @ sk4)))),inference(simp,[status(thm)],[3644])).
% 74.67/18.91 thf(3684,plain,(((sk2 @ (^ [A:$i]: (sk1 @ A @ sk4)) @ sk4) != sk4) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk5) != sk5)),inference(pre_uni,[status(thm)],[3645:[bind(A, $thf(^ [B:$i]: (sk1 @ B @ sk4)))]])).
% 74.67/18.91 thf(23,plain,(~ (($true)) | ((sk1 @ sk5 @ sk5) != (sk1 @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[8,15])).
% 74.67/18.91 thf(24,plain,(((sk1 @ sk5 @ sk5) != (sk1 @ sk4 @ sk5))),inference(simp,[status(thm)],[23])).
% 74.67/18.91 thf(25,plain,((sk5 != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[24])).
% 74.67/18.91 thf(26,plain,((sk5 != sk4)),inference(simp,[status(thm)],[25])).
% 74.67/18.91 thf(159,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[139,18])).
% 74.67/18.91 thf(160,plain,(((sk1 @ sk4 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[159])).
% 74.67/18.91 thf(169,plain,((sk4 != sk4) | ((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[160])).
% 74.67/18.91 thf(171,plain,(((sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4) != sk4)),inference(simp,[status(thm)],[169])).
% 74.67/18.91 thf(14182,plain,(! [A:($i > $o)] : (~ (($true)) | ((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) != (A @ sk5)))),inference(paramod_ordered,[status(thm)],[137,1190])).
% 74.67/18.91 thf(14183,plain,(! [A:($i > $o)] : (((sk2 @ (^ [B:$i]: ~ (A @ B)) @ sk4) != sk4) | ((sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ sk5)) @ sk4)) != (A @ sk5)))),inference(simp,[status(thm)],[14182])).
% 74.67/18.91 thf(14289,plain,(((sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ (sk2 @ (^ [B:$i]: (sk1 @ B @ A)) @ sk4))) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[14183:[bind(A, $thf(^ [B:$i]: (sk1 @ sk4 @ (sk2 @ (^ [C:$i]: (sk1 @ C @ B)) @ sk4))))]])).
% 74.67/18.91 thf(106,plain,(! [D:$i,C:($i > $o),B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (sk1 @ B @ (sk2 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((A @ sk5) != (sk1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[96,7])).
% 74.67/18.91 thf(107,plain,(! [D:$i,C:($i > $o),B:$i,A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (A) @ sk4)) | (sk1 @ B @ (sk2 @ (C) @ B)) | (C @ D) | ((A @ sk5) != (sk1 @ B @ D)))),inference(simp,[status(thm)],[106])).
% 74.67/18.91 thf(140,plain,(! [C:($i > $i),B:($i > $i),A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ (B @ D) @ (C @ D))) @ sk4)) | (sk1 @ (B @ sk5) @ (sk2 @ (A) @ (B @ sk5))) | (A @ (C @ sk5)))),inference(pre_uni,[status(thm)],[107:[bind(A, $thf(^ [G:$i]: (sk1 @ (E @ G) @ (F @ G)))),bind(B, $thf(E @ sk5)),bind(C, $thf(C)),bind(D, $thf(F @ sk5))]])).
% 74.67/18.91 thf(151,plain,(! [C:($i > $i),B:($i > $i),A:($i > $o)] : ((sk1 @ sk4 @ (sk2 @ (^ [D:$i]: (sk1 @ (B @ D) @ (C @ D))) @ sk4)) | (sk1 @ (B @ sk5) @ (sk2 @ (A) @ (B @ sk5))) | (A @ (C @ sk5)))),inference(simp,[status(thm)],[140])).
% 74.67/18.92 thf(2515,plain,(! [A:$i] : (~ (($true)) | (~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[756,11])).
% 74.67/18.92 thf(2516,plain,(! [A:$i] : ((~ (sk1 @ A @ sk5)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4)) != (sk1 @ sk4 @ A)))),inference(simp,[status(thm)],[2515])).
% 74.67/18.92 thf(2517,plain,((~ (sk1 @ (sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4) @ sk5))),inference(pattern_uni,[status(thm)],[2516:[bind(A, $thf(sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4))]])).
% 74.67/18.92 thf(944,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[339,18])).
% 74.67/18.92 thf(945,plain,(((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[944])).
% 74.67/18.92 thf(956,plain,((sk4 != sk4) | ((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[945])).
% 74.67/18.92 thf(967,plain,(((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: (sk1 @ A @ A)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[956])).
% 74.67/18.92 thf(1172,plain,(((sk2 @ (sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)) @ sk4) != sk4)),inference(pre_uni,[status(thm)],[1140:[bind(A, $thf(sk1 @ (sk2 @ (sk1 @ sk5) @ sk4)))]])).
% 74.67/18.92 thf(505,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk3 @ (B) @ A))) | ~ (($true)) | (B @ C) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[8,9])).
% 74.67/18.92 thf(506,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk3 @ (B) @ A))) | (B @ C) | ((sk1 @ sk4 @ sk5) != (sk1 @ A @ C)))),inference(simp,[status(thm)],[505])).
% 74.67/18.92 thf(507,plain,(! [A:($i > $o)] : ((~ (A @ (sk3 @ (A) @ sk4))) | (A @ sk5))),inference(pattern_uni,[status(thm)],[506:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(sk5))]])).
% 74.67/18.92 thf(664,plain,(! [A:($i > $o)] : ((~ (A @ (sk3 @ (A) @ sk4))) | (A @ sk5))),inference(simp,[status(thm)],[507])).
% 74.67/18.92 thf(32,plain,(! [F:$i,E:($i > $o),D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | (sk1 @ D @ (sk2 @ (E) @ D)) | ~ (($true)) | (E @ F) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ D @ F)))),inference(paramod_ordered,[status(thm)],[7,7])).
% 74.67/18.92 thf(33,plain,(! [F:$i,E:($i > $o),D:$i,C:$i,B:($i > $o),A:$i] : ((~ (sk1 @ A @ C)) | (B @ C) | (sk1 @ D @ (sk2 @ (E) @ D)) | (E @ F) | ((sk1 @ A @ (sk2 @ (B) @ A)) != (sk1 @ D @ F)))),inference(simp,[status(thm)],[32])).
% 74.67/18.92 thf(34,plain,(! [D:$i,C:($i > $o),B:($i > $o),A:$i] : ((~ (sk1 @ D @ A)) | (C @ A) | (sk1 @ D @ (sk2 @ (B) @ D)) | (B @ (sk2 @ (C) @ D)))),inference(pattern_uni,[status(thm)],[33:[bind(A, $thf(H)),bind(B, $thf(G)),bind(C, $thf(C)),bind(D, $thf(H)),bind(E, $thf(E)),bind(F, $thf(sk2 @ (G) @ H))]])).
% 74.67/18.92 thf(94,plain,(! [D:$i,C:($i > $o),B:($i > $o),A:$i] : ((~ (sk1 @ D @ A)) | (C @ A) | (sk1 @ D @ (sk2 @ (B) @ D)) | (B @ (sk2 @ (C) @ D)))),inference(simp,[status(thm)],[34])).
% 74.67/18.92 thf(19188,plain,(~ (($true)) | ((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[18933,18])).
% 74.67/18.92 thf(19189,plain,(((sk1 @ sk4 @ (sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4)) != (sk1 @ sk4 @ sk4))),inference(simp,[status(thm)],[19188])).
% 74.67/18.92 thf(19260,plain,((sk4 != sk4) | ((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[19189])).
% 74.67/18.92 thf(19298,plain,(((sk2 @ (sk1 @ (sk2 @ (^ [A:$i]: ~ (sk1 @ sk4 @ A)) @ sk4)) @ sk4) != sk4)),inference(simp,[status(thm)],[19260])).
% 74.67/18.92 thf(79,plain,(! [C:($i > $i),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: (sk1 @ (C @ D) @ sk5)) @ A)) | (~ (sk1 @ A @ B)) | (~ (sk1 @ sk4 @ (C @ B))))),inference(pre_uni,[status(thm)],[49:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (sk1 @ (E @ F) @ sk5))),bind(C, $thf(C)),bind(D, $thf(E @ C))]])).
% 74.67/18.92 thf(90,plain,(! [C:($i > $i),B:$i,A:$i] : ((sk1 @ A @ (sk2 @ (^ [D:$i]: (sk1 @ (C @ D) @ sk5)) @ A)) | (~ (sk1 @ A @ B)) | (~ (sk1 @ sk4 @ (C @ B))))),inference(simp,[status(thm)],[79])).
% 74.67/18.92 thf(57,plain,(! [C:$i,B:($i > $o),A:$i] : ((sk1 @ A @ (sk2 @ (B) @ A)) | (~ (sk1 @ A @ C)) | ((B @ C) != (sk1 @ A @ (sk2 @ (B) @ A))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[7])).
% 74.67/18.92 thf(67,plain,(! [B:$i,A:($i > $i)] : ((sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)))) | (~ (sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))) | (B != (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))))),inference(pre_uni,[status(thm)],[57:[bind(A, $thf(D @ (sk2 @ (^ [F:$i]: (sk1 @ (D @ F) @ F)) @ K))),bind(B, $thf(^ [E:$i]: (sk1 @ (D @ E) @ E))),bind(C, $thf(sk2 @ (^ [F:$i]: (sk1 @ (D @ F) @ F)) @ K))]])).
% 74.67/18.92 thf(68,plain,(! [B:$i,A:($i > $i)] : ((~ (sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))) | (sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)))) | (B != (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))))),inference(pre_uni,[status(thm)],[67:[]])).
% 74.67/18.92 thf(83,plain,(! [B:$i,A:($i > $i)] : ((~ (sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))) | (sk1 @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)) @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B)))) | (B != (A @ (sk2 @ (^ [C:$i]: (sk1 @ (A @ C) @ C)) @ B))))),inference(simp,[status(thm)],[68])).
% 74.67/18.92 thf(25367,plain,(($false)),inference(e,[status(thm)],[73,87,101,941,88,138,1190,1073,1173,384,1164,14301,18933,15881,20,93,416,152,756,84,293,132,89,3582,6,1163,2428,19703,137,92,2758,65,757,697,19203,9,339,96,4804,173,17858,1103,148,64,444,149,71,12,144,5578,86,2257,7,98,3160,2343,91,66,1029,9074,155,1171,399,695,1000,3,1413,145,295,18,282,150,95,5523,19816,15846,5277,154,11,72,3684,26,171,139,8,18911,14289,151,2517,967,146,1172,664,696,94,427,7506,5060,15,163,19298,90,83,755])).
% 74.67/18.92 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.67/18.92 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------