Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : AGT027^2 : TPTP v9.3.1. Released v5.2.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 : n010.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 07:44:34 AM UTC 2026

% Result   : Theorem 178.33s 46.09s
% Output   : Refutation 166.64s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : AGT027^2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21  % Computer : n010.cluster.edu
% 0.10/0.21  % Model    : x86_64 x86_64
% 0.10/0.21  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21  % Memory   : 8046.5625MB
% 0.10/0.21  % OS       : Linux 6.8.0-71-generic
% 0.10/0.21  % CPULimit : 300
% 0.10/0.21  % WCLimit  : 300
% 0.10/0.21  % DateTime : Tue Sep 29 17:29:33 UTC 2026
% 0.10/0.21  % CPUTime  : 
% 0.10/0.21  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.86/0.78  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 1.50/1.05  % [INFO] 	 Parsing done (263ms). 
% 1.50/1.06  % [INFO] 	 Running in sequential loop mode. 
% 2.11/1.45  % [INFO] 	 eprover registered as external prover. 
% 2.11/1.45  % [INFO] 	 Scanning for conjecture ... 
% 2.51/1.63  % [INFO] 	 Found a conjecture (or negated_conjecture) and 9 axioms. Running axiom selection ... 
% 2.51/1.66  % [INFO] 	 Axiom selection finished. Selected 9 axioms (removed 0 axioms). 
% 2.51/1.68  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 2.51/1.68  % [INFO] 	 Type checking passed. 
% 2.51/1.69  % [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 ... 
% 178.33/46.08  % External prover 'e' found a proof!
% 178.33/46.08  % [INFO] 	 Killing All external provers ... 
% 178.33/46.08  % Time passed: 45739ms (effective reasoning time: 45013ms)
% 178.33/46.08  % 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)>
% 178.33/46.09  % Axioms used in derivation (9): axiom_4s_for_a2_a2, axiom_I_for_a2_a1, axiom_a1, axiom_a3, axiom_4s_for_a2_a1, axiom_4s_for_a1_a2, axiom_a4, axiom_4s_for_a1_a1, axiom_a2
% 178.33/46.09  % No. of inferences in proof: 427
% 178.33/46.09  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 45739 ms resp. 45013 ms w/o parsing
% 166.64/46.35  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 166.64/46.35  thf(mu_type, type, mu: $tType).
% 166.64/46.35  thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 166.64/46.35  thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 166.64/46.35  thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 166.64/46.35  thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 166.64/46.35  thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 166.64/46.35  thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 166.64/46.35  thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 166.64/46.35  thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 166.64/46.35  thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 166.64/46.35  thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 166.64/46.35  thf(a1_decl, type, a1: ($i > ($i > $o))).
% 166.64/46.35  thf(a2_decl, type, a2: ($i > ($i > $o))).
% 166.64/46.35  thf(a_decl, type, a: mu).
% 166.64/46.35  thf(p_decl, type, p: (mu > ($i > $o))).
% 166.64/46.35  thf(q_decl, type, q: (mu > ($i > $o))).
% 166.64/46.35  thf(r_decl, type, r: (mu > ($i > $o))).
% 166.64/46.35  thf(s_decl, type, s: (mu > ($i > $o))).
% 166.64/46.35  thf(sk1_decl, type, sk1: $i).
% 166.64/46.35  thf(sk2_decl, type, sk2: (mu > $i)).
% 166.64/46.35  thf(sk3_decl, type, sk3: ($i > $i)).
% 166.64/46.35  thf(sk4_decl, type, sk4: (($i > $o) > ($i > $i))).
% 166.64/46.35  thf(sk5_decl, type, sk5: (($i > $o) > ($i > $i))).
% 166.64/46.35  thf(sk6_decl, type, sk6: (($i > $o) > ($i > $i))).
% 166.64/46.35  thf(sk7_decl, type, sk7: (($i > $o) > ($i > $i))).
% 166.64/46.35  thf(sk8_decl, type, sk8: (($i > $o) > ($i > $i))).
% 166.64/46.35  thf(sk11_decl, type, sk11: (mu > $i)).
% 166.64/46.35  thf(sk12_decl, type, sk12: (mu > $i)).
% 166.64/46.35  thf(sk13_decl, type, sk13: (mu > $i)).
% 166.64/46.35  thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 166.64/46.35  thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 166.64/46.35  thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 166.64/46.35  thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 166.64/46.35  thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 166.64/46.35  thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 166.64/46.35  thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 166.64/46.35  thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 166.64/46.35  thf(mdia_def, definition, mdia = (^ [A:($i > ($i > $o)),B:($i > $o)]: (mnot @ (mbox @ A @ (mnot @ B)))) ).
% 166.64/46.35  thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 166.64/46.35  thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (? [B:mu]: ! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C)))) ).
% 166.64/46.35  thf(sk2_def, definition, sk2 = (^ [A:mu]: (@+ [B:$i]: ~ (~ (a1 @ sk1 @ B) | (p @ A @ B)))) ).
% 166.64/46.35  thf(sk3_def, definition, sk3 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (a1 @ A @ B) | ~ (s @ a @ B)))) ).
% 166.64/46.35  thf(sk4_def, definition, sk4 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | (A @ C)))) ).
% 166.64/46.35  thf(sk5_def, definition, sk5 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a1 @ B @ C) | (A @ C)))) ).
% 166.64/46.35  thf(sk6_def, definition, sk6 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a1 @ B @ C) | (A @ C)))) ).
% 166.64/46.35  thf(sk7_def, definition, sk7 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | (A @ C)))) ).
% 166.64/46.35  thf(sk8_def, definition, sk8 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | (A @ C)))) ).
% 166.64/46.35  thf(1,conjecture,((mvalid @ (mexists_ind @ (^ [A:mu]: (mbox @ a1 @ (p @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 166.64/46.35  thf(2,negated_conjecture,((~ (mvalid @ (mexists_ind @ (^ [A:mu]: (mbox @ a1 @ (p @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 166.64/46.35  thf(12,plain,((~ (! [A:$i]: ~ (! [B:mu]: ~ (! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 166.64/46.35  thf(13,plain,((~ (~ (~ (! [A:$i]: ? [B:mu]: ! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C))))))),inference(miniscope,[status(thm)],[12])).
% 166.64/46.35  thf(14,plain,(! [A:mu] : (((a1 @ sk1 @ (sk2 @ A)) & ~ (p @ A @ (sk2 @ A))))),inference(cnf,[status(esa)],[13])).
% 166.64/46.35  thf(15,plain,(! [A:mu] : ((a1 @ sk1 @ (sk2 @ A)))),inference(cnfConj,[status(thm)],[14])).
% 166.64/46.35  thf(7,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a1 @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_I_for_a2_a1)).
% 166.64/46.35  thf(28,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 166.64/46.35  thf(29,plain,(! [C:$i,B:($i > $o),A:$i] : ((((a2 @ A @ (sk4 @ (B) @ A)) | ~ (a1 @ A @ C) | (B @ C)) & (~ (B @ (sk4 @ (B) @ A)) | ~ (a1 @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[28])).
% 166.64/46.35  thf(31,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (~ (a1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[29])).
% 166.64/46.35  thf(731,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk4 @ (C) @ B))) | ~ (($true)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[15,31])).
% 166.64/46.35  thf(732,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk4 @ (C) @ B))) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[731])).
% 166.64/46.35  thf(733,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | (A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[732:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 166.64/46.35  thf(888,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | (A @ (sk2 @ B)))),inference(simp,[status(thm)],[733])).
% 166.64/46.35  thf(984,plain,(! [B:($i > $o),A:mu] : ((~ (~ (B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)))) | (~ (B @ (sk2 @ A))))),inference(prim_subst,[status(thm)],[888:[bind(A, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 166.64/46.35  thf(1068,plain,(! [B:($i > $o),A:mu] : ((B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(cnf,[status(esa)],[984])).
% 166.64/46.35  thf(1069,plain,(! [B:($i > $o),A:mu] : ((B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(simp,[status(thm)],[1068])).
% 166.64/46.35  thf(30,plain,(! [C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (~ (a1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[29])).
% 166.64/46.35  thf(100,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((a2 @ B @ (sk4 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[15,30])).
% 166.64/46.35  thf(101,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((a2 @ B @ (sk4 @ (C) @ B)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[100])).
% 166.64/46.35  thf(102,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | (A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[101:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 166.64/46.35  thf(135,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | (A @ (sk2 @ B)))),inference(simp,[status(thm)],[102])).
% 166.64/46.35  thf(925,plain,(! [D:mu,C:($i > $o),B:mu,A:($i > $o)] : ((A @ (sk2 @ B)) | ~ (($true)) | (C @ (sk2 @ D)) | ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[135,888])).
% 166.64/46.35  thf(926,plain,(! [D:mu,C:($i > $o),B:mu,A:($i > $o)] : ((A @ (sk2 @ B)) | (C @ (sk2 @ D)) | ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[925])).
% 166.64/46.35  thf(1030,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | (a2 @ sk1 @ (sk2 @ B)))),inference(pre_uni,[status(thm)],[926:[bind(A, $thf(a2 @ sk1)),bind(B, $thf(B)),bind(C, $thf(a2 @ sk1)),bind(D, $thf(D))]])).
% 166.64/46.35  thf(1057,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | (a2 @ sk1 @ (sk2 @ B)))),inference(simp,[status(thm)],[1030])).
% 166.64/46.35  thf(1423,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | ((a2 @ sk1 @ (sk2 @ B)) != (a2 @ sk1 @ (sk2 @ A))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[1057])).
% 166.64/46.35  thf(1444,plain,(! [A:mu] : ((a2 @ sk1 @ (sk2 @ A)))),inference(pattern_uni,[status(thm)],[1423:[bind(A, $thf(B))]])).
% 166.64/46.35  thf(1449,plain,(! [A:mu] : ((a2 @ sk1 @ (sk2 @ A)))),inference(simp,[status(thm)],[1444])).
% 166.64/46.35  thf(3106,plain,(! [C:($i > $o),B:mu,A:mu] : ((C @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[15,1069])).
% 166.64/46.35  thf(3107,plain,(! [C:($i > $o),B:mu,A:mu] : ((C @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[3106])).
% 166.64/46.35  thf(3210,plain,((a1 @ sk1 @ (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1))),inference(pre_uni,[status(thm)],[3107:[bind(A, $thf(B)),bind(B, $thf(B)),bind(C, $thf(a1 @ sk1))]])).
% 166.64/46.35  thf(3357,plain,(! [C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[3210,30])).
% 166.64/46.35  thf(3358,plain,(! [C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (B @ C) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(simp,[status(thm)],[3357])).
% 166.64/46.35  thf(3359,plain,(! [A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))),inference(pattern_uni,[status(thm)],[3358:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))]])).
% 166.64/46.35  thf(3392,plain,(! [A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))),inference(simp,[status(thm)],[3359])).
% 166.64/46.35  thf(6897,plain,(! [A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(prim_subst,[status(thm)],[3392:[bind(A, $thf(^ [C:$i]: ~ (B @ C)))]])).
% 166.64/46.35  thf(7139,plain,(! [A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(cnf,[status(esa)],[6897])).
% 166.64/46.35  thf(7140,plain,(! [A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(simp,[status(thm)],[7139])).
% 166.64/46.35  thf(8334,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ~ (($true)) | ((a2 @ sk1 @ (sk2 @ A)) != (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1))))),inference(paramod_ordered,[status(thm)],[1449,7140])).
% 166.64/46.35  thf(8335,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ((a2 @ sk1 @ (sk2 @ A)) != (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1))))),inference(simp,[status(thm)],[8334])).
% 166.64/46.35  thf(8385,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk2 @ (A @ B)))) @ sk1)))),inference(pre_uni,[status(thm)],[8335:[bind(A, $thf(E @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))),bind(B, $thf(^ [D:$i]: (a2 @ sk1 @ (sk2 @ (E @ D)))))]])).
% 166.64/46.35  thf(8479,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk2 @ (A @ B)))) @ sk1)))),inference(simp,[status(thm)],[8385])).
% 166.64/46.35  thf(8514,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: ~ (($true))) @ sk1))),inference(rewrite,[status(thm)],[8479,1449])).
% 166.64/46.35  thf(8515,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[8514])).
% 166.64/46.35  thf(8603,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk2 @ A))) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[1069,8515])).
% 166.64/46.35  thf(8607,plain,(! [A:mu] : ((~ ((sk2 @ A) = (sk2 @ A))) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk2 @ A) = (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)))),inference(replace_leibeq,[status(thm)],[8603:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk2 @ A)))]])).
% 166.64/46.35  thf(8626,plain,(! [A:mu] : (((sk2 @ A) != (sk2 @ A)) | ((sk2 @ A) = (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(lifteq,[status(thm)],[8607])).
% 166.64/46.35  thf(8641,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk2 @ A) = (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[8626:[]])).
% 166.64/46.35  thf(12353,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(paramod_ordered,[status(thm)],[8641,1449])).
% 166.64/46.35  thf(12354,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[12353:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(13938,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)) != (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[12354])).
% 166.64/46.35  thf(13970,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (sk1 != sk1) | ((sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[13938])).
% 166.64/46.35  thf(13980,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[13970])).
% 166.64/46.35  thf(17691,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((^ [B:$i]: ~ ((sk2 @ A) = B)) != (^ [B:$i]: (($true)))) | (sk1 != sk1))),inference(simp,[status(thm)],[13980])).
% 166.64/46.35  thf(17727,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((^ [B:$i]: ~ ((sk2 @ A) = B)) != (^ [B:$i]: (($true)))))),inference(simp,[status(thm)],[17691])).
% 166.64/46.35  thf(18143,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) != (^ [C:$i]: (($true)))) | ((sk2 @ A) != (sk2 @ B)))),inference(paramod_ordered,[status(thm)],[8641,17727])).
% 166.64/46.35  thf(18144,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) != (^ [C:$i]: (($true)))) | ((sk2 @ A) != (sk2 @ B)))),inference(simp,[status(thm)],[18143])).
% 166.64/46.35  thf(18145,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((^ [B:$i]: ~ ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) = B)) != (^ [B:$i]: (($true)))))),inference(pattern_uni,[status(thm)],[18144:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(20204,plain,(! [A:mu] : ((~ (~ ((sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1) = (sk12 @ A)))) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(func_ext,[status(esa)],[18145])).
% 166.64/46.35  thf(20519,plain,(! [A:mu] : (((sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1) = (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(cnf,[status(esa)],[20204])).
% 166.64/46.35  thf(20520,plain,(! [A:mu] : (((sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1) = (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(lifteq,[status(thm)],[20519])).
% 166.64/46.35  thf(23044,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ A)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,12354])).
% 166.64/46.35  thf(23045,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ A)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23044])).
% 166.64/46.35  thf(23046,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ A)))),inference(pattern_uni,[status(thm)],[23045:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(181,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(prim_subst,[status(thm)],[135:[bind(A, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 166.64/46.35  thf(213,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(cnf,[status(esa)],[181])).
% 166.64/46.35  thf(214,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(simp,[status(thm)],[213])).
% 166.64/46.35  thf(23580,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a2 @ sk1 @ (sk12 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[23046,214])).
% 166.64/46.35  thf(23581,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a2 @ sk1 @ (sk12 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[23580])).
% 166.64/46.35  thf(23728,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk12 @ (A @ B)))) @ sk1)))),inference(pre_uni,[status(thm)],[23581:[bind(A, $thf(F @ (sk2 @ B))),bind(B, $thf(B)),bind(C, $thf(^ [E:$i]: (a2 @ sk1 @ (sk12 @ (F @ E)))))]])).
% 166.64/46.35  thf(23832,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk12 @ (A @ B)))) @ sk1)))),inference(simp,[status(thm)],[23728])).
% 166.64/46.35  thf(3,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a2 @ (mimplies @ (mdia @ a2 @ (q @ A)) @ (p @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a1)).
% 166.64/46.35  thf(17,plain,((! [A:$i,B:mu,C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | ~ (q @ B @ D)) | (p @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 166.64/46.35  thf(18,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a2 @ A @ C)) | (~ (a2 @ C @ D)) | (~ (q @ B @ D)) | (p @ B @ C))),inference(cnf,[status(esa)],[17])).
% 166.64/46.35  thf(60,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a2 @ A @ C)) | (~ (q @ B @ D)) | (p @ B @ C) | ((a2 @ C @ D) != (a2 @ A @ C)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[18])).
% 166.64/46.35  thf(61,plain,(! [B:$i,A:mu] : ((~ (a2 @ B @ B)) | (~ (q @ A @ B)) | (p @ A @ B))),inference(pattern_uni,[status(thm)],[60:[bind(A, $thf(D)),bind(B, $thf(B)),bind(C, $thf(D))]])).
% 166.64/46.35  thf(62,plain,(! [B:$i,A:mu] : ((~ (a2 @ B @ B)) | (~ (q @ A @ B)) | (p @ A @ B))),inference(simp,[status(thm)],[61])).
% 166.64/46.35  thf(21266,plain,(! [B:$i,A:mu] : (~ (($true)) | (~ (q @ A @ B)) | (p @ A @ B) | ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($false))) @ sk1)) != (a2 @ B @ B)))),inference(paramod_ordered,[status(thm)],[8515,62])).
% 166.64/46.35  thf(21267,plain,(! [B:$i,A:mu] : ((~ (q @ A @ B)) | (p @ A @ B) | ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($false))) @ sk1)) != (a2 @ B @ B)))),inference(simp,[status(thm)],[21266])).
% 166.64/46.35  thf(21388,plain,(! [B:$i,A:mu] : ((p @ A @ B) | (~ (q @ A @ B)) | (sk1 != B) | ((sk4 @ (^ [C:$i]: (($false))) @ sk1) != B))),inference(simp,[status(thm)],[21267])).
% 166.64/46.35  thf(21439,plain,(! [A:mu] : ((p @ A @ sk1) | (~ (q @ A @ sk1)) | ((sk4 @ (^ [B:$i]: (($false))) @ sk1) != sk1))),inference(simp,[status(thm)],[21388])).
% 166.64/46.35  thf(187,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($false))) @ sk1)) | ($false)),inference(prim_subst,[status(thm)],[135:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 166.64/46.35  thf(219,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[187])).
% 166.64/46.35  thf(227,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a2 @ A @ C)) | ~ (($true)) | (~ (q @ B @ D)) | (p @ B @ C) | ((a2 @ sk1 @ (sk4 @ (^ [E:$i]: (($false))) @ sk1)) != (a2 @ C @ D)))),inference(paramod_ordered,[status(thm)],[219,18])).
% 166.64/46.35  thf(228,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a2 @ A @ C)) | (~ (q @ B @ D)) | (p @ B @ C) | ((a2 @ sk1 @ (sk4 @ (^ [E:$i]: (($false))) @ sk1)) != (a2 @ C @ D)))),inference(simp,[status(thm)],[227])).
% 166.64/46.35  thf(229,plain,(! [B:mu,A:$i] : ((~ (a2 @ A @ sk1)) | (~ (q @ B @ (sk4 @ (^ [C:$i]: (($false))) @ sk1))) | (p @ B @ sk1))),inference(pattern_uni,[status(thm)],[228:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk1)),bind(D, $thf(sk4 @ (^ [E:$i]: (($false))) @ sk1))]])).
% 166.64/46.35  thf(16353,plain,(! [C:mu,B:$i,A:mu] : (~ (($true)) | (~ (q @ C @ (sk4 @ (^ [D:$i]: (($false))) @ sk1))) | (p @ C @ sk1) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[1449,229])).
% 166.64/46.35  thf(16354,plain,(! [C:mu,B:$i,A:mu] : ((~ (q @ C @ (sk4 @ (^ [D:$i]: (($false))) @ sk1))) | (p @ C @ sk1) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ B @ sk1)))),inference(simp,[status(thm)],[16353])).
% 166.64/46.35  thf(16447,plain,(! [C:mu,B:$i,A:mu] : ((p @ C @ sk1) | (~ (q @ C @ (sk4 @ (^ [D:$i]: (($false))) @ sk1))) | (sk1 != B) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[16354])).
% 166.64/46.35  thf(16533,plain,(! [B:mu,A:mu] : ((p @ B @ sk1) | (~ (q @ B @ (sk4 @ (^ [C:$i]: (($false))) @ sk1))) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[16447])).
% 166.64/46.35  thf(319,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (~ (B @ C))) @ sk1)) | (~ (~ (B @ (sk2 @ A)))))),inference(prim_subst,[status(thm)],[214:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 166.64/46.35  thf(364,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (~ (B @ C))) @ sk1)) | (B @ (sk2 @ A)))),inference(cnf,[status(esa)],[319])).
% 166.64/46.35  thf(365,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (B) @ sk1)) | (B @ (sk2 @ A)))),inference(simp,[status(thm)],[364])).
% 166.64/46.35  thf(106,plain,(! [D:($i > $i),C:($i > $i),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [E:$i]: (a2 @ (C @ E) @ (D @ E))) @ A)) | (~ (a1 @ A @ B)) | (a2 @ (C @ B) @ (D @ B)))),inference(prim_subst,[status(thm)],[30:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (a2 @ (D @ F) @ (E @ F))))]])).
% 166.64/46.35  thf(138,plain,(! [D:($i > $i),C:($i > $i),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [E:$i]: (a2 @ (C @ E) @ (D @ E))) @ A)) | (~ (a1 @ A @ B)) | (a2 @ (C @ B) @ (D @ B)))),inference(simp,[status(thm)],[106])).
% 166.64/46.35  thf(23054,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk12 @ A) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,13980])).
% 166.64/46.35  thf(23055,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk12 @ A) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23054])).
% 166.64/46.35  thf(23056,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk12 @ A) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(pattern_uni,[status(thm)],[23055:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(3348,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | ~ (($true)) | (B @ C) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[3210,31])).
% 166.64/46.35  thf(3349,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (B @ C) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(simp,[status(thm)],[3348])).
% 166.64/46.35  thf(3350,plain,(! [A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))),inference(pattern_uni,[status(thm)],[3349:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))]])).
% 166.64/46.35  thf(3388,plain,(! [A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))),inference(simp,[status(thm)],[3350])).
% 166.64/46.35  thf(11353,plain,(! [A:($i > $o)] : ((~ (~ (A @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)))) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(prim_subst,[status(thm)],[3388:[bind(A, $thf(^ [C:$i]: ~ (B @ C)))]])).
% 166.64/46.35  thf(11602,plain,(! [A:($i > $o)] : ((A @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(cnf,[status(esa)],[11353])).
% 166.64/46.35  thf(11603,plain,(! [A:($i > $o)] : ((A @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)) | (~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))))),inference(simp,[status(thm)],[11602])).
% 166.64/46.35  thf(32,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk4 @ (B) @ A) = (sk4 @ ((=) @ $i @ (sk4 @ B @ A)) @ A))) | (~ (a1 @ A @ C)) | ((sk4 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[31:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk4 @ B @ A)))]])).
% 166.64/46.35  thf(33,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk4 @ (B) @ A) != (sk4 @ ((=) @ $i @ (sk4 @ B @ A)) @ A)) | ((sk4 @ (B) @ A) = C) | (~ (a1 @ A @ C)))),inference(lifteq,[status(thm)],[32])).
% 166.64/46.35  thf(751,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (~ (a1 @ A @ C)) | ((B @ C) != (~ (B @ (sk4 @ (B) @ A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[31])).
% 166.64/46.35  thf(798,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (~ (a1 @ A @ C)) | ((B @ C) != (~ (B @ (sk4 @ (B) @ A)))))),inference(simp,[status(thm)],[751])).
% 166.64/46.35  thf(3316,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | ~ (($true)) | ((B @ C) != (~ (B @ (sk4 @ (B) @ A)))) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(paramod_ordered,[status(thm)],[3210,798])).
% 166.64/46.35  thf(3317,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | ((B @ C) != (~ (B @ (sk4 @ (B) @ A)))) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ A @ C)))),inference(simp,[status(thm)],[3316])).
% 166.64/46.35  thf(3318,plain,(! [A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(pattern_uni,[status(thm)],[3317:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))]])).
% 166.64/46.35  thf(3387,plain,(! [A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(simp,[status(thm)],[3318])).
% 166.64/46.35  thf(3916,plain,(! [D:($i > $o),C:$i,B:($i > $o),A:$i] : (((sk4 @ (B) @ A) != (sk4 @ ((=) @ $i @ (sk4 @ B @ A)) @ A)) | (~ (a1 @ A @ C)) | (~ (D @ (sk4 @ (D) @ sk1))) | ((D @ C) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((sk4 @ (B) @ A) != (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)))),inference(paramod_ordered,[status(thm)],[33,3387])).
% 166.64/46.35  thf(3917,plain,(! [B:($i > $o),A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) @ sk1) != (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | (~ (a1 @ sk1 @ A)) | (~ (B @ (sk4 @ (B) @ sk1))) | ((B @ A) != (~ (B @ (sk4 @ (B) @ sk1)))))),inference(pattern_uni,[status(thm)],[3916:[bind(A, $thf(sk1)),bind(B, $thf(^ [E:$i]: ~ (a1 @ sk1 @ E))),bind(C, $thf(C)),bind(D, $thf(D))]])).
% 166.64/46.35  thf(4253,plain,(! [B:($i > $o),A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) @ sk1) != (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | (~ (a1 @ sk1 @ A)) | (~ (B @ (sk4 @ (B) @ sk1))) | ((B @ A) != (~ (B @ (sk4 @ (B) @ sk1)))))),inference(simp,[status(thm)],[3917])).
% 166.64/46.35  thf(7202,plain,(! [B:($i > $o),A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) @ sk1) != (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | ~ (($true)) | (~ (B @ (sk4 @ (B) @ sk1))) | ((B @ A) != (~ (B @ (sk4 @ (B) @ sk1)))) | ((a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (a1 @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[3210,4253])).
% 166.64/46.35  thf(7203,plain,(! [B:($i > $o),A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) @ sk1) != (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | (~ (B @ (sk4 @ (B) @ sk1))) | ((B @ A) != (~ (B @ (sk4 @ (B) @ sk1)))) | ((a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (a1 @ sk1 @ A)))),inference(simp,[status(thm)],[7202])).
% 166.64/46.35  thf(7204,plain,(! [A:($i > $o)] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) @ sk1) != (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) | (~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(pattern_uni,[status(thm)],[7203:[bind(A, $thf(sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)),bind(B, $thf(B))]])).
% 166.64/46.35  thf(7653,plain,(! [A:($i > $o)] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) @ sk1) != (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) | (~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(simp,[status(thm)],[7204])).
% 166.64/46.35  thf(13996,plain,(! [A:($i > $o)] : ((((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (^ [B:$i]: ~ (a1 @ sk1 @ B))) | (sk1 != sk1) | (~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(simp,[status(thm)],[7653])).
% 166.64/46.35  thf(14662,plain,(! [A:($i > $o)] : ((((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (^ [B:$i]: ~ (a1 @ sk1 @ B))) | (~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(simp,[status(thm)],[13996])).
% 166.64/46.35  thf(16,plain,(! [A:mu] : ((~ (p @ A @ (sk2 @ A))))),inference(cnfConj,[status(thm)],[14])).
% 166.64/46.35  thf(174,plain,(! [C:mu,B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | ~ (($true)) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[135,16])).
% 166.64/46.35  thf(175,plain,(! [C:mu,B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (A) @ sk1)) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(simp,[status(thm)],[174])).
% 166.64/46.35  thf(192,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[175:[bind(A, $thf(^ [E:$i]: (p @ (D @ E) @ E))),bind(B, $thf(B)),bind(C, $thf(D @ (sk2 @ B)))]])).
% 166.64/46.35  thf(194,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[192:[]])).
% 166.64/46.35  thf(202,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) | (A != (B @ (sk2 @ A))))),inference(simp,[status(thm)],[194])).
% 166.64/46.35  thf(16271,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (q @ B @ (sk4 @ (^ [C:$i]: (($false))) @ sk1))) | (p @ B @ sk1) | ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($false))) @ sk1)) != (a2 @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[8515,229])).
% 166.64/46.35  thf(16272,plain,(! [B:mu,A:$i] : ((~ (q @ B @ (sk4 @ (^ [C:$i]: (($false))) @ sk1))) | (p @ B @ sk1) | ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($false))) @ sk1)) != (a2 @ A @ sk1)))),inference(simp,[status(thm)],[16271])).
% 166.64/46.35  thf(16395,plain,(! [B:mu,A:$i] : ((p @ B @ sk1) | (~ (q @ B @ (sk4 @ (^ [C:$i]: (($false))) @ sk1))) | (sk1 != A) | ((sk4 @ (^ [C:$i]: (($false))) @ sk1) != sk1))),inference(simp,[status(thm)],[16272])).
% 166.64/46.35  thf(16481,plain,(! [A:mu] : ((p @ A @ sk1) | (~ (q @ A @ (sk4 @ (^ [B:$i]: (($false))) @ sk1))) | ((sk4 @ (^ [B:$i]: (($false))) @ sk1) != sk1))),inference(simp,[status(thm)],[16395])).
% 166.64/46.35  thf(6,axiom,((mvalid @ (mdia @ a1 @ (s @ a)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a4)).
% 166.64/46.35  thf(23,plain,((! [A:$i]: ~ (! [B:$i]: (~ (a1 @ A @ B) | ~ (s @ a @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 166.64/46.35  thf(24,plain,((~ (? [A:$i]: ! [B:$i]: (~ (a1 @ A @ B) | ~ (s @ a @ B))))),inference(miniscope,[status(thm)],[23])).
% 166.64/46.35  thf(25,plain,(! [A:$i] : (((a1 @ A @ (sk3 @ A)) & (s @ a @ (sk3 @ A))))),inference(cnf,[status(esa)],[24])).
% 166.64/46.35  thf(26,plain,(! [A:$i] : ((a1 @ A @ (sk3 @ A)))),inference(cnfConj,[status(thm)],[25])).
% 166.64/46.35  thf(27,plain,(! [A:$i] : ((s @ a @ (sk3 @ A)))),inference(cnfConj,[status(thm)],[25])).
% 166.64/46.35  thf(5,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (s @ A) @ (mbox @ a1 @ (r @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a3)).
% 166.64/46.35  thf(21,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ~ (s @ B @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (r @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 166.64/46.35  thf(22,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (s @ B @ C)) | (~ (a1 @ C @ D)) | (r @ B @ D))),inference(cnf,[status(esa)],[21])).
% 166.64/46.35  thf(259,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a1 @ B @ D)) | (~ (s @ C @ D)) | ~ (($true)) | (r @ C @ E) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ D @ E)))),inference(paramod_ordered,[status(thm)],[15,22])).
% 166.64/46.35  thf(260,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a1 @ B @ D)) | (~ (s @ C @ D)) | (r @ C @ E) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ D @ E)))),inference(simp,[status(thm)],[259])).
% 166.64/46.35  thf(261,plain,(! [C:mu,B:mu,A:$i] : ((~ (a1 @ A @ sk1)) | (~ (s @ B @ sk1)) | (r @ B @ (sk2 @ C)))),inference(pattern_uni,[status(thm)],[260:[bind(A, $thf(F)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk1)),bind(E, $thf(sk2 @ F))]])).
% 166.64/46.35  thf(274,plain,(! [C:mu,B:mu,A:$i] : ((~ (a1 @ A @ sk1)) | (~ (s @ B @ sk1)) | (r @ B @ (sk2 @ C)))),inference(simp,[status(thm)],[261])).
% 166.64/46.35  thf(18747,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ~ (($true)) | (r @ C @ (sk2 @ D)) | ((s @ a @ (sk3 @ A)) != (s @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[27,274])).
% 166.64/46.35  thf(18748,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | (r @ C @ (sk2 @ D)) | ((s @ a @ (sk3 @ A)) != (s @ C @ sk1)))),inference(simp,[status(thm)],[18747])).
% 166.64/46.35  thf(18945,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((r @ C @ (sk2 @ D)) | (~ (a1 @ B @ sk1)) | (a != C) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[18748])).
% 166.64/46.35  thf(18979,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | (~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[18945])).
% 166.64/46.35  thf(19194,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ~ (($true)) | ((sk3 @ B) != sk1) | ((a1 @ A @ (sk3 @ A)) != (a1 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[26,18979])).
% 166.64/46.35  thf(19195,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | ((a1 @ A @ (sk3 @ A)) != (a1 @ C @ sk1)))),inference(simp,[status(thm)],[19194])).
% 166.64/46.35  thf(19285,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | (A != C) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[19195])).
% 166.64/46.35  thf(19360,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | ((sk3 @ A) != sk1) | ((sk3 @ B) != sk1))),inference(simp,[status(thm)],[19285])).
% 166.64/46.35  thf(20917,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | ((sk3 @ A) != sk1) | ((sk3 @ B) != (sk3 @ A)) | (sk1 != sk1))),inference(eqfactor_ordered,[status(thm)],[19360])).
% 166.64/46.35  thf(20966,plain,(! [B:mu,A:$i] : ((r @ a @ (sk2 @ B)) | ((sk3 @ A) != sk1))),inference(pattern_uni,[status(thm)],[20917:[bind(A, $thf(B))]])).
% 166.64/46.35  thf(21011,plain,(! [B:mu,A:$i] : ((r @ a @ (sk2 @ B)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[20966])).
% 166.64/46.35  thf(21133,plain,(! [D:($i > $o),C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | (D @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ sk1)) | ~ (($true)) | ((r @ a @ (sk2 @ B)) != (D @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[21011,1069])).
% 166.64/46.35  thf(21134,plain,(! [D:($i > $o),C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | (D @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ sk1)) | ((r @ a @ (sk2 @ B)) != (D @ (sk2 @ C))))),inference(simp,[status(thm)],[21133])).
% 166.64/46.35  thf(21192,plain,(! [A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk4 @ (^ [B:$i]: ~ (r @ a @ B)) @ sk1)))),inference(pre_uni,[status(thm)],[21134:[bind(A, $thf(A)),bind(B, $thf(C)),bind(C, $thf(C)),bind(D, $thf(r @ a))]])).
% 166.64/46.35  thf(12351,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(paramod_ordered,[status(thm)],[8641,15])).
% 166.64/46.35  thf(12352,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk2 @ A) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[12351:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(13484,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(paramod_ordered,[status(thm)],[8641,12352])).
% 166.64/46.35  thf(13485,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(simp,[status(thm)],[13484])).
% 166.64/46.35  thf(13486,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[13485:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(23059,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk12 @ A) = C)) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,13486])).
% 166.64/46.35  thf(23060,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk12 @ A) = C)) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23059])).
% 166.64/46.35  thf(23061,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk12 @ A) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[23060:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(21350,plain,(! [C:$i,B:mu,A:mu] : (~ (($true)) | (~ (q @ B @ C)) | (p @ B @ C) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ C @ C)))),inference(paramod_ordered,[status(thm)],[1449,62])).
% 166.64/46.35  thf(21351,plain,(! [C:$i,B:mu,A:mu] : ((~ (q @ B @ C)) | (p @ B @ C) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ C @ C)))),inference(simp,[status(thm)],[21350])).
% 166.64/46.35  thf(21424,plain,(! [C:$i,B:mu,A:mu] : ((p @ B @ C) | (~ (q @ B @ C)) | (sk1 != C) | ((sk2 @ A) != C))),inference(simp,[status(thm)],[21351])).
% 166.64/46.35  thf(21467,plain,(! [B:mu,A:mu] : ((p @ B @ sk1) | (~ (q @ B @ sk1)) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[21424])).
% 166.64/46.35  thf(9,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a1 @ A) @ (mbox @ a2 @ (mbox @ a1 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a1_a2)).
% 166.64/46.35  thf(40,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a1 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 166.64/46.35  thf(41,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((a1 @ A @ (sk6 @ (B) @ A)) | ~ (a2 @ A @ C) | ~ (a1 @ C @ D) | (B @ D)) & (~ (B @ (sk6 @ (B) @ A)) | ~ (a2 @ A @ C) | ~ (a1 @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[40])).
% 166.64/46.35  thf(42,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((a1 @ A @ (sk6 @ (B) @ A)) | (~ (a2 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[41])).
% 166.64/46.35  thf(3118,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk4 @ (^ [C:$i]: ~ (~ (B @ C))) @ sk1))) | (~ (~ (B @ (sk2 @ A)))))),inference(prim_subst,[status(thm)],[1069:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 166.64/46.35  thf(3247,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk4 @ (^ [C:$i]: ~ (~ (B @ C))) @ sk1))) | (B @ (sk2 @ A)))),inference(cnf,[status(esa)],[3118])).
% 166.64/46.35  thf(3248,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk4 @ (B) @ sk1))) | (B @ (sk2 @ A)))),inference(simp,[status(thm)],[3247])).
% 166.64/46.35  thf(4451,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk4 @ (B) @ sk1))) | ((B @ (sk2 @ A)) != (~ (B @ (sk4 @ (B) @ sk1)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[3248])).
% 166.64/46.35  thf(4496,plain,(! [B:($i > $o),A:mu] : ((~ (B @ (sk4 @ (B) @ sk1))) | ((B @ (sk2 @ A)) != (~ (B @ (sk4 @ (B) @ sk1)))))),inference(simp,[status(thm)],[4451])).
% 166.64/46.35  thf(8,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a1 @ A) @ (mbox @ a1 @ (mbox @ a1 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a1_a1)).
% 166.64/46.35  thf(34,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a1 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 166.64/46.35  thf(35,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((a1 @ A @ (sk5 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a1 @ C @ D) | (B @ D)) & (~ (B @ (sk5 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a1 @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[34])).
% 166.64/46.35  thf(37,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk5 @ (B) @ A))) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[35])).
% 166.64/46.35  thf(2265,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk4 @ (C) @ B))) | ~ (($true)) | ((C @ D) != (~ (C @ (sk4 @ (C) @ B)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[26,798])).
% 166.64/46.35  thf(2266,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk4 @ (C) @ B))) | ((C @ D) != (~ (C @ (sk4 @ (C) @ B)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[2265])).
% 166.64/46.35  thf(2267,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ B))) | ((~ (A @ (sk4 @ (A) @ B))) != (A @ (sk3 @ B))))),inference(pattern_uni,[status(thm)],[2266:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk3 @ E))]])).
% 166.64/46.35  thf(2600,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ B))) | ((~ (A @ (sk4 @ (A) @ B))) != (A @ (sk3 @ B))))),inference(simp,[status(thm)],[2267])).
% 166.64/46.35  thf(21129,plain,(! [D:$i,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((~ (C @ (sk4 @ (C) @ D))) != (C @ (sk3 @ D))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ D))))),inference(paramod_ordered,[status(thm)],[21011,2600])).
% 166.64/46.35  thf(21130,plain,(! [D:$i,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((~ (C @ (sk4 @ (C) @ D))) != (C @ (sk3 @ D))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ D))))),inference(simp,[status(thm)],[21129])).
% 166.64/46.35  thf(21173,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B))))) != (r @ a @ (sk2 @ (C @ (sk3 @ B))))))),inference(pre_uni,[status(thm)],[21130:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ D))),bind(C, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F))))),bind(D, $thf(D))]])).
% 166.64/46.35  thf(21210,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B))))) != (r @ a @ (sk2 @ (C @ (sk3 @ B))))))),inference(simp,[status(thm)],[21173])).
% 166.64/46.35  thf(23112,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ A)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,12352])).
% 166.64/46.35  thf(23113,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ A)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23112])).
% 166.64/46.35  thf(23114,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ A)))),inference(pattern_uni,[status(thm)],[23113:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(24174,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ~ (($true)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1))))),inference(paramod_ordered,[status(thm)],[23114,7140])).
% 166.64/46.35  thf(24175,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1))))),inference(simp,[status(thm)],[24174])).
% 166.64/46.35  thf(24358,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ (sk12 @ (A @ B)))) @ sk1)))),inference(pre_uni,[status(thm)],[24175:[bind(A, $thf(E @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))),bind(B, $thf(^ [D:$i]: (a1 @ sk1 @ (sk12 @ (E @ D)))))]])).
% 166.64/46.35  thf(24418,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ (sk12 @ (A @ B)))) @ sk1)))),inference(simp,[status(thm)],[24358])).
% 166.64/46.35  thf(11,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a2 @ (mbox @ a2 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a2_a2)).
% 166.64/46.35  thf(52,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 166.64/46.35  thf(975,plain,(! [C:mu,B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ~ (($true)) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[888,16])).
% 166.64/46.35  thf(976,plain,(! [C:mu,B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(simp,[status(thm)],[975])).
% 166.64/46.35  thf(1006,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[976:[bind(A, $thf(^ [E:$i]: (p @ (D @ E) @ E))),bind(B, $thf(B)),bind(C, $thf(D @ (sk2 @ B)))]])).
% 166.64/46.35  thf(1008,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[1006:[]])).
% 166.64/46.35  thf(1087,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk4 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(simp,[status(thm)],[1008])).
% 166.64/46.35  thf(4,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (mand @ (r @ A) @ (s @ A)) @ (q @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a2)).
% 166.64/46.35  thf(19,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ~ (r @ B @ C) | ~ (s @ B @ C) | (q @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 166.64/46.35  thf(20,plain,(! [C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (r @ B @ C)) | (~ (s @ B @ C)) | (q @ B @ C))),inference(cnf,[status(esa)],[19])).
% 166.64/46.35  thf(10,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a1 @ (mbox @ a2 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a2_a1)).
% 166.64/46.35  thf(46,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 166.64/46.35  thf(983,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (~ (A @ (sk4 @ (A) @ sk1)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[888])).
% 166.64/46.35  thf(1038,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk4 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (~ (A @ (sk4 @ (A) @ sk1)))))),inference(simp,[status(thm)],[983])).
% 166.64/46.35  thf(19170,plain,(! [E:mu,D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ~ (($true)) | ((D @ (sk2 @ E)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(paramod_ordered,[status(thm)],[18979,1038])).
% 166.64/46.35  thf(19171,plain,(! [E:mu,D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((D @ (sk2 @ E)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(simp,[status(thm)],[19170])).
% 166.64/46.35  thf(19281,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[19171:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk4 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ sk1))),bind(D, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G))))),bind(E, $thf(E))]])).
% 166.64/46.35  thf(19355,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))))),inference(simp,[status(thm)],[19281])).
% 166.64/46.35  thf(53,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((a2 @ A @ (sk8 @ (B) @ A)) | ~ (a2 @ A @ C) | ~ (a2 @ C @ D) | (B @ D)) & (~ (B @ (sk8 @ (B) @ A)) | ~ (a2 @ A @ C) | ~ (a2 @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[52])).
% 166.64/46.35  thf(55,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a2 @ A @ C)) | (~ (a2 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[53])).
% 166.64/46.35  thf(56,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk8 @ (B) @ A) = (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A))) | (~ (a2 @ A @ C)) | (~ (a2 @ C @ D)) | ((sk8 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[55:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 166.64/46.35  thf(57,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk8 @ (B) @ A) != (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A)) | ((sk8 @ (B) @ A) = D) | (~ (a2 @ A @ C)) | (~ (a2 @ C @ D)))),inference(lifteq,[status(thm)],[56])).
% 166.64/46.35  thf(23009,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((^ [C:$i]: ~ ((sk12 @ A) = C)) != (^ [C:$i]: (($true)))) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,18145])).
% 166.64/46.35  thf(23010,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((^ [C:$i]: ~ ((sk12 @ A) = C)) != (^ [C:$i]: (($true)))) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23009])).
% 166.64/46.35  thf(23011,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((^ [B:$i]: ~ ((sk12 @ A) = B)) != (^ [B:$i]: (($true)))))),inference(pattern_uni,[status(thm)],[23010:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(13859,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(paramod_ordered,[status(thm)],[8641,12354])).
% 166.64/46.35  thf(13860,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk4 @ (^ [D:$i]: ~ ((sk2 @ A) = D)) @ sk1) = C)) @ sk1)) | ((sk2 @ A) != (sk2 @ B)))),inference(simp,[status(thm)],[13859])).
% 166.64/46.35  thf(13861,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[13860:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(23072,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk12 @ A) = C)) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,13861])).
% 166.64/46.35  thf(23073,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ ((sk12 @ A) = C)) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23072])).
% 166.64/46.35  thf(23074,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk12 @ A) = B)) @ sk1)))),inference(pattern_uni,[status(thm)],[23073:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(27591,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ ((sk12 @ A) = B)) @ sk1)) != (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[23074])).
% 166.64/46.35  thf(27644,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (sk1 != sk1) | ((sk4 @ (^ [B:$i]: ~ ((sk12 @ A) = B)) @ sk1) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[27591])).
% 166.64/46.35  thf(27675,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [B:$i]: ~ ((sk12 @ A) = B)) @ sk1) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[27644])).
% 166.64/46.35  thf(81,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (a1 @ A @ C)) | (B @ C) | ~ (($true)) | (~ (a2 @ F @ G)) | (~ (q @ E @ G)) | (p @ E @ F) | ((a2 @ A @ (sk4 @ (B) @ A)) != (a2 @ D @ F)))),inference(paramod_ordered,[status(thm)],[30,18])).
% 166.64/46.35  thf(82,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (a1 @ A @ C)) | (B @ C) | (~ (a2 @ F @ G)) | (~ (q @ E @ G)) | (p @ E @ F) | ((a2 @ A @ (sk4 @ (B) @ A)) != (a2 @ D @ F)))),inference(simp,[status(thm)],[81])).
% 166.64/46.35  thf(83,plain,(! [E:$i,D:($i > $o),C:$i,B:mu,A:$i] : ((~ (a1 @ E @ A)) | (D @ A) | (~ (a2 @ (sk4 @ (D) @ E) @ C)) | (~ (q @ B @ C)) | (p @ B @ (sk4 @ (D) @ E)))),inference(pattern_uni,[status(thm)],[82:[bind(A, $thf(I)),bind(B, $thf(H)),bind(C, $thf(C)),bind(D, $thf(I)),bind(E, $thf(E)),bind(F, $thf(sk4 @ (H) @ I))]])).
% 166.64/46.35  thf(132,plain,(! [E:$i,D:($i > $o),C:$i,B:mu,A:$i] : ((~ (a1 @ E @ A)) | (D @ A) | (~ (a2 @ (sk4 @ (D) @ E) @ C)) | (~ (q @ B @ C)) | (p @ B @ (sk4 @ (D) @ E)))),inference(simp,[status(thm)],[83])).
% 166.64/46.35  thf(84,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (a1 @ A @ C)) | (B @ C) | (~ (a2 @ D @ F)) | ~ (($true)) | (~ (q @ E @ G)) | (p @ E @ F) | ((a2 @ A @ (sk4 @ (B) @ A)) != (a2 @ F @ G)))),inference(paramod_ordered,[status(thm)],[30,18])).
% 166.64/46.35  thf(85,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((~ (a1 @ A @ C)) | (B @ C) | (~ (a2 @ D @ F)) | (~ (q @ E @ G)) | (p @ E @ F) | ((a2 @ A @ (sk4 @ (B) @ A)) != (a2 @ F @ G)))),inference(simp,[status(thm)],[84])).
% 166.64/46.35  thf(86,plain,(! [E:$i,D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ E @ A)) | (D @ A) | (~ (a2 @ B @ E)) | (~ (q @ C @ (sk4 @ (D) @ E))) | (p @ C @ E))),inference(pattern_uni,[status(thm)],[85:[bind(A, $thf(I)),bind(B, $thf(H)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(I)),bind(G, $thf(sk4 @ (H) @ I))]])).
% 166.64/46.35  thf(133,plain,(! [E:$i,D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ E @ A)) | (D @ A) | (~ (a2 @ B @ E)) | (~ (q @ C @ (sk4 @ (D) @ E))) | (p @ C @ E))),inference(simp,[status(thm)],[86])).
% 166.64/46.35  thf(69,plain,(! [D:$i,C:mu,B:$i,A:mu] : (~ (($true)) | (~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[15,20])).
% 166.64/46.35  thf(70,plain,(! [D:$i,C:mu,B:$i,A:mu] : ((~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[69])).
% 166.64/46.35  thf(71,plain,(! [B:mu,A:mu] : ((~ (r @ A @ (sk2 @ B))) | (~ (s @ A @ (sk2 @ B))) | (q @ A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[70:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 166.64/46.35  thf(74,plain,(! [B:mu,A:mu] : ((~ (r @ A @ (sk2 @ B))) | (~ (s @ A @ (sk2 @ B))) | (q @ A @ (sk2 @ B)))),inference(simp,[status(thm)],[71])).
% 166.64/46.35  thf(235,plain,(! [G:$i,F:mu,E:$i,D:$i,C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (s @ B @ C)) | (~ (a1 @ C @ D)) | (~ (a1 @ E @ G)) | ~ (($true)) | (~ (s @ F @ G)) | (q @ F @ G) | ((r @ B @ D) != (r @ F @ G)))),inference(paramod_ordered,[status(thm)],[22,20])).
% 166.64/46.35  thf(236,plain,(! [G:$i,F:mu,E:$i,D:$i,C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (s @ B @ C)) | (~ (a1 @ C @ D)) | (~ (a1 @ E @ G)) | (~ (s @ F @ G)) | (q @ F @ G) | ((r @ B @ D) != (r @ F @ G)))),inference(simp,[status(thm)],[235])).
% 166.64/46.35  thf(237,plain,(! [E:$i,D:$i,C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (s @ B @ C)) | (~ (a1 @ C @ D)) | (~ (a1 @ E @ D)) | (~ (s @ B @ D)) | (q @ B @ D))),inference(pattern_uni,[status(thm)],[236:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(B)),bind(G, $thf(D))]])).
% 166.64/46.35  thf(415,plain,(! [F:$i,E:$i,D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ D)) | ~ (($true)) | (~ (a1 @ D @ E)) | (~ (a1 @ F @ E)) | (~ (s @ C @ E)) | (q @ C @ E) | ((s @ a @ (sk3 @ A)) != (s @ C @ D)))),inference(paramod_ordered,[status(thm)],[27,237])).
% 166.64/46.35  thf(416,plain,(! [F:$i,E:$i,D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ D)) | (~ (a1 @ D @ E)) | (~ (a1 @ F @ E)) | (~ (s @ C @ E)) | (q @ C @ E) | ((s @ a @ (sk3 @ A)) != (s @ C @ D)))),inference(simp,[status(thm)],[415])).
% 166.64/46.35  thf(417,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (a1 @ A @ (sk3 @ D))) | (~ (a1 @ (sk3 @ D) @ B)) | (~ (a1 @ C @ B)) | (~ (s @ a @ B)) | (q @ a @ B))),inference(pattern_uni,[status(thm)],[416:[bind(A, $thf(G)),bind(B, $thf(B)),bind(C, $thf(a)),bind(D, $thf(sk3 @ G))]])).
% 166.64/46.35  thf(439,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (a1 @ A @ (sk3 @ D))) | (~ (a1 @ (sk3 @ D) @ B)) | (~ (a1 @ C @ B)) | (~ (s @ a @ B)) | (q @ a @ B))),inference(simp,[status(thm)],[417])).
% 166.64/46.35  thf(63,plain,(! [D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ D)) | (~ (r @ C @ D)) | ~ (($true)) | (q @ C @ D) | ((s @ a @ (sk3 @ A)) != (s @ C @ D)))),inference(paramod_ordered,[status(thm)],[27,20])).
% 166.64/46.35  thf(64,plain,(! [D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ D)) | (~ (r @ C @ D)) | (q @ C @ D) | ((s @ a @ (sk3 @ A)) != (s @ C @ D)))),inference(simp,[status(thm)],[63])).
% 166.64/46.35  thf(65,plain,(! [B:$i,A:$i] : ((~ (a1 @ A @ (sk3 @ B))) | (~ (r @ a @ (sk3 @ B))) | (q @ a @ (sk3 @ B)))),inference(pattern_uni,[status(thm)],[64:[bind(A, $thf(E)),bind(B, $thf(B)),bind(C, $thf(a)),bind(D, $thf(sk3 @ E))]])).
% 166.64/46.35  thf(72,plain,(! [B:$i,A:$i] : ((~ (a1 @ A @ (sk3 @ B))) | (~ (r @ a @ (sk3 @ B))) | (q @ a @ (sk3 @ B)))),inference(simp,[status(thm)],[65])).
% 166.64/46.35  thf(24570,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (r @ a @ (sk3 @ C))) | (q @ a @ (sk3 @ C)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ (sk3 @ C))))),inference(paramod_ordered,[status(thm)],[26,72])).
% 166.64/46.35  thf(24571,plain,(! [C:$i,B:$i,A:$i] : ((~ (r @ a @ (sk3 @ C))) | (q @ a @ (sk3 @ C)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ (sk3 @ C))))),inference(simp,[status(thm)],[24570])).
% 166.64/46.35  thf(24572,plain,(! [A:$i] : ((~ (r @ a @ (sk3 @ A))) | (q @ a @ (sk3 @ A)))),inference(pattern_uni,[status(thm)],[24571:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(A))]])).
% 166.64/46.35  thf(23618,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((a2 @ sk1 @ (sk12 @ A)) != (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[23046])).
% 166.64/46.35  thf(23703,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((a2 @ sk1 @ (sk12 @ A)) != (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1))))),inference(simp,[status(thm)],[23618])).
% 166.64/46.35  thf(105,plain,(! [C:($i > $o),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (a1 @ A @ B)) | (~ (C @ B)))),inference(prim_subst,[status(thm)],[30:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: ~ (D @ E)))]])).
% 166.64/46.35  thf(136,plain,(! [C:($i > $o),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (a1 @ A @ B)) | (~ (C @ B)))),inference(cnf,[status(esa)],[105])).
% 166.64/46.35  thf(137,plain,(! [C:($i > $o),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ A)) | (~ (a1 @ A @ B)) | (~ (C @ B)))),inference(simp,[status(thm)],[136])).
% 166.64/46.35  thf(21123,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,7140])).
% 166.64/46.35  thf(21124,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1))))),inference(simp,[status(thm)],[21123])).
% 166.64/46.35  thf(21169,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (r @ a @ (sk2 @ (B @ C)))) @ sk1)))),inference(pre_uni,[status(thm)],[21124:[bind(A, $thf(A)),bind(B, $thf(F @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1))),bind(C, $thf(^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))))]])).
% 166.64/46.35  thf(21206,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (r @ a @ (sk2 @ (B @ C)))) @ sk1)))),inference(simp,[status(thm)],[21169])).
% 166.64/46.35  thf(23535,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ~ (($true)) | (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | ((a2 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(paramod_ordered,[status(thm)],[23046,3388])).
% 166.64/46.35  thf(23536,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | ((a2 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(simp,[status(thm)],[23535])).
% 166.64/46.35  thf(23752,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))))),inference(pre_uni,[status(thm)],[23536:[bind(A, $thf(E @ (sk4 @ (^ [D:$i]: (a2 @ sk1 @ (sk12 @ (E @ D)))) @ sk1))),bind(B, $thf(^ [D:$i]: (a2 @ sk1 @ (sk12 @ (E @ D)))))]])).
% 166.64/46.35  thf(23853,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))))),inference(simp,[status(thm)],[23752])).
% 166.64/46.35  thf(19143,plain,(! [D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ~ (($true)) | ((D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(paramod_ordered,[status(thm)],[18979,3387])).
% 166.64/46.35  thf(19144,plain,(! [D:($i > $o),C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(simp,[status(thm)],[19143])).
% 166.64/46.35  thf(19297,plain,(! [C:($i > mu),B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[19144:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ sk1))),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 166.64/46.35  thf(19373,plain,(! [C:($i > mu),B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(simp,[status(thm)],[19297])).
% 166.64/46.35  thf(24021,plain,(! [C:mu,B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | ~ (($true)) | (B @ (sk2 @ C)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(paramod_ordered,[status(thm)],[23114,888])).
% 166.64/46.35  thf(24022,plain,(! [C:mu,B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | (B @ (sk2 @ C)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(simp,[status(thm)],[24021])).
% 166.64/46.35  thf(24350,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ (B @ (sk2 @ A)))))),inference(pre_uni,[status(thm)],[24022:[bind(A, $thf(F @ (sk4 @ (^ [E:$i]: (a1 @ sk1 @ (sk12 @ (F @ E)))) @ sk1))),bind(B, $thf(^ [E:$i]: (a1 @ sk1 @ (sk12 @ (F @ E))))),bind(C, $thf(C))]])).
% 166.64/46.35  thf(24412,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ (B @ (sk2 @ A)))))),inference(simp,[status(thm)],[24350])).
% 166.64/46.35  thf(95,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((a2 @ B @ (sk4 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[26,30])).
% 166.64/46.35  thf(96,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((a2 @ B @ (sk4 @ (C) @ B)) | (C @ D) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[95])).
% 166.64/46.35  thf(97,plain,(! [B:$i,A:($i > $o)] : ((a2 @ B @ (sk4 @ (A) @ B)) | (A @ (sk3 @ B)))),inference(pattern_uni,[status(thm)],[96:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk3 @ E))]])).
% 166.64/46.35  thf(134,plain,(! [B:$i,A:($i > $o)] : ((a2 @ B @ (sk4 @ (A) @ B)) | (A @ (sk3 @ B)))),inference(simp,[status(thm)],[97])).
% 166.64/46.35  thf(66,plain,(! [D:$i,C:mu,B:$i,A:$i] : (~ (($true)) | (~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[26,20])).
% 166.64/46.35  thf(67,plain,(! [D:$i,C:mu,B:$i,A:$i] : ((~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[66])).
% 166.64/46.35  thf(68,plain,(! [B:$i,A:mu] : ((~ (r @ A @ (sk3 @ B))) | (~ (s @ A @ (sk3 @ B))) | (q @ A @ (sk3 @ B)))),inference(pattern_uni,[status(thm)],[67:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk3 @ E))]])).
% 166.64/46.35  thf(73,plain,(! [B:$i,A:mu] : ((~ (r @ A @ (sk3 @ B))) | (~ (s @ A @ (sk3 @ B))) | (q @ A @ (sk3 @ B)))),inference(simp,[status(thm)],[68])).
% 166.64/46.35  thf(41157,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : (~ (($true)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | ((a1 @ sk1 @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (a1 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[3210,19355])).
% 166.64/46.35  thf(41158,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | ((a1 @ sk1 @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (a1 @ B @ sk1)))),inference(simp,[status(thm)],[41157])).
% 166.64/46.35  thf(41476,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | (sk1 != B) | ((sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1) != sk1))),inference(simp,[status(thm)],[41158])).
% 166.64/46.35  thf(41491,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk2 @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))) | ((sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1) != sk1))),inference(simp,[status(thm)],[41476])).
% 166.64/46.35  thf(24750,plain,(! [A:mu] : ((~ (~ ((sk12 @ A) = (sk13 @ A)))) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(func_ext,[status(esa)],[23011])).
% 166.64/46.35  thf(25042,plain,(! [A:mu] : (((sk12 @ A) = (sk13 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(cnf,[status(esa)],[24750])).
% 166.64/46.35  thf(25043,plain,(! [A:mu] : (((sk13 @ A) = (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(lifteq,[status(thm)],[25042])).
% 166.64/46.35  thf(110,plain,(! [B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [C:$i]: (($false))) @ A)) | (~ (a1 @ A @ B)) | ($false))),inference(prim_subst,[status(thm)],[30:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: (($false))))]])).
% 166.64/46.35  thf(142,plain,(! [B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [C:$i]: (($false))) @ A)) | (~ (a1 @ A @ B)))),inference(simp,[status(thm)],[110])).
% 166.64/46.35  thf(2120,plain,(! [C:$i,B:$i,A:$i] : ((a2 @ B @ (sk4 @ (^ [D:$i]: (($false))) @ B)) | ~ (($true)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[26,142])).
% 166.64/46.35  thf(2121,plain,(! [C:$i,B:$i,A:$i] : ((a2 @ B @ (sk4 @ (^ [D:$i]: (($false))) @ B)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[2120])).
% 166.64/46.35  thf(2122,plain,(! [A:$i] : ((a2 @ A @ (sk4 @ (^ [B:$i]: (($false))) @ A)))),inference(pattern_uni,[status(thm)],[2121:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk3 @ D))]])).
% 166.64/46.35  thf(2189,plain,(! [A:$i] : ((a2 @ A @ (sk4 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[2122])).
% 166.64/46.35  thf(21101,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((C @ (sk2 @ D)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,1038])).
% 166.64/46.35  thf(21102,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((C @ (sk2 @ D)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21101])).
% 166.64/46.35  thf(21188,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk2 @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[21102:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ sk1))),bind(C, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F))))),bind(D, $thf(D))]])).
% 166.64/46.35  thf(21226,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk2 @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(simp,[status(thm)],[21188])).
% 166.64/46.35  thf(43,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (~ (a2 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[41])).
% 166.64/46.35  thf(44,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | (~ (a2 @ A @ C)) | (~ (a1 @ C @ D)) | ((sk6 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[43:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 166.64/46.35  thf(45,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = D) | (~ (a2 @ A @ C)) | (~ (a1 @ C @ D)))),inference(lifteq,[status(thm)],[44])).
% 166.64/46.35  thf(38409,plain,(! [A:($i > $o)] : ((~ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1))) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (A @ (sk4 @ (^ [B:$i]: ~ (A @ B)) @ sk1)))),inference(paramod_ordered,[status(thm)],[11603,8515])).
% 166.64/46.35  thf(38859,plain,((~ ((sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1) = (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1))) | (a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1) = (sk4 @ (^ [A:$i]: ~ ((sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1) = A)) @ sk1))),inference(replace_leibeq,[status(thm)],[38409:[bind(A, $thf((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))]])).
% 166.64/46.35  thf(38893,plain,(((sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1) != (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1)) | ((sk4 @ (^ [A:$i]: ~ ((sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1) = A)) @ sk1) = (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($true))) @ sk1))),inference(lifteq,[status(thm)],[38859])).
% 166.64/46.35  thf(38955,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [A:$i]: ~ ((sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1) = A)) @ sk1) = (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1))),inference(pattern_uni,[status(thm)],[38893:[]])).
% 166.64/46.35  thf(21085,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,3387])).
% 166.64/46.35  thf(21086,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21085])).
% 166.64/46.35  thf(21181,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))) != (~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[21086:[bind(A, $thf(A)),bind(B, $thf(F @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))) @ sk1))),bind(C, $thf(^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))))]])).
% 166.64/46.35  thf(21218,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))) != (~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1)))))))),inference(simp,[status(thm)],[21181])).
% 166.64/46.35  thf(1467,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a2 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[1449,214])).
% 166.64/46.35  thf(1468,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a2 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[1467])).
% 166.64/46.35  thf(1488,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: ~ (a2 @ sk1 @ A)) @ sk1))),inference(pre_uni,[status(thm)],[1468:[bind(A, $thf(B)),bind(B, $thf(B)),bind(C, $thf(a2 @ sk1))]])).
% 166.64/46.35  thf(24131,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ~ (($true)) | (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(paramod_ordered,[status(thm)],[23114,3388])).
% 166.64/46.35  thf(24132,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) | ((a1 @ sk1 @ (sk12 @ A)) != (B @ (sk4 @ (B) @ sk1))))),inference(simp,[status(thm)],[24131])).
% 166.64/46.35  thf(24356,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))))),inference(pre_uni,[status(thm)],[24132:[bind(A, $thf(E @ (sk4 @ (^ [D:$i]: (a1 @ sk1 @ (sk12 @ (E @ D)))) @ sk1))),bind(B, $thf(^ [D:$i]: (a1 @ sk1 @ (sk12 @ (E @ D)))))]])).
% 166.64/46.35  thf(24415,plain,(! [A:($i > mu)] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | (a1 @ sk1 @ (sk12 @ (A @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)))))),inference(simp,[status(thm)],[24356])).
% 166.64/46.35  thf(54,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk8 @ (B) @ A)) | (~ (a2 @ A @ C)) | (~ (a2 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[53])).
% 166.64/46.35  thf(47,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((a2 @ A @ (sk7 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a2 @ C @ D) | (B @ D)) & (~ (B @ (sk7 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a2 @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[46])).
% 166.64/46.35  thf(49,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk7 @ (B) @ A))) | (~ (a1 @ A @ C)) | (~ (a2 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[47])).
% 166.64/46.35  thf(7253,plain,(! [C:($i > $o),B:$i,A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) @ sk1) != (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) | ~ (($true)) | (~ (C @ (sk4 @ (C) @ sk1))) | ((C @ B) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[26,4253])).
% 166.64/46.35  thf(7254,plain,(! [C:($i > $o),B:$i,A:$i] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) @ sk1) != (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) | (~ (C @ (sk4 @ (C) @ sk1))) | ((C @ B) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ sk1 @ B)))),inference(simp,[status(thm)],[7253])).
% 166.64/46.35  thf(7255,plain,(! [A:($i > $o)] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) @ sk1) != (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) | (~ (A @ (sk4 @ (A) @ sk1))) | ((~ (A @ (sk4 @ (A) @ sk1))) != (A @ (sk3 @ sk1))))),inference(pattern_uni,[status(thm)],[7254:[bind(A, $thf(sk1)),bind(B, $thf(sk3 @ sk1)),bind(C, $thf(C))]])).
% 166.64/46.35  thf(7659,plain,(! [A:($i > $o)] : (((sk4 @ ((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) @ sk1) != (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) | (~ (A @ (sk4 @ (A) @ sk1))) | ((~ (A @ (sk4 @ (A) @ sk1))) != (A @ (sk3 @ sk1))))),inference(simp,[status(thm)],[7255])).
% 166.64/46.35  thf(8692,plain,(! [A:($i > $o)] : ((((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (^ [B:$i]: ~ (a1 @ sk1 @ B))) | (sk1 != sk1) | (~ (A @ (sk4 @ (A) @ sk1))) | ((~ (A @ (sk4 @ (A) @ sk1))) != (A @ (sk3 @ sk1))))),inference(simp,[status(thm)],[7659])).
% 166.64/46.35  thf(9111,plain,(! [A:($i > $o)] : ((((=) @ $i @ (sk4 @ (^ [B:$i]: ~ (a1 @ sk1 @ B)) @ sk1)) != (^ [B:$i]: ~ (a1 @ sk1 @ B))) | (~ (A @ (sk4 @ (A) @ sk1))) | ((~ (A @ (sk4 @ (A) @ sk1))) != (A @ (sk3 @ sk1))))),inference(simp,[status(thm)],[8692])).
% 166.64/46.35  thf(21097,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (^ [D:$i]: ~ (a1 @ sk1 @ D))) | ~ (($true)) | ((~ (C @ (sk4 @ (C) @ sk1))) != (C @ (sk3 @ sk1))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,9111])).
% 166.64/46.35  thf(21098,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (^ [D:$i]: ~ (a1 @ sk1 @ D))) | ((~ (C @ (sk4 @ (C) @ sk1))) != (C @ (sk3 @ sk1))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21097])).
% 166.64/46.35  thf(21185,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (^ [C:$i]: ~ (a1 @ sk1 @ C))) | ((~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1))))) != (r @ a @ (sk2 @ (B @ (sk3 @ sk1))))))),inference(pre_uni,[status(thm)],[21098:[bind(A, $thf(A)),bind(B, $thf(F @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))) @ sk1))),bind(C, $thf(^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))))]])).
% 166.64/46.35  thf(21222,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (^ [C:$i]: ~ (a1 @ sk1 @ C))) | ((~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1))))) != (r @ a @ (sk2 @ (B @ (sk3 @ sk1))))))),inference(simp,[status(thm)],[21185])).
% 166.64/46.35  thf(38,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk5 @ (B) @ A) = (sk5 @ ((=) @ $i @ (sk5 @ B @ A)) @ A))) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | ((sk5 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[37:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 166.64/46.35  thf(39,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk5 @ (B) @ A) != (sk5 @ ((=) @ $i @ (sk5 @ B @ A)) @ A)) | ((sk5 @ (B) @ A) = D) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)))),inference(lifteq,[status(thm)],[38])).
% 166.64/46.35  thf(30921,plain,(! [C:($i > mu),B:$i,A:$i] : (~ (($true)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[3210,19373])).
% 166.64/46.35  thf(30922,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))) | ((a1 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (a1 @ B @ sk1)))),inference(simp,[status(thm)],[30921])).
% 166.64/46.35  thf(31197,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))) | (sk1 != B) | ((sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1) != sk1))),inference(simp,[status(thm)],[30922])).
% 166.64/46.35  thf(31384,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))) != (~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1)))))) | ((sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1) != sk1))),inference(simp,[status(thm)],[31197])).
% 166.64/46.35  thf(21121,plain,(! [D:($i > $o),C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ sk1)) | ~ (($true)) | ((r @ a @ (sk2 @ B)) != (D @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[21011,214])).
% 166.64/46.35  thf(21122,plain,(! [D:($i > $o),C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ sk1)) | ((r @ a @ (sk2 @ B)) != (D @ (sk2 @ C))))),inference(simp,[status(thm)],[21121])).
% 166.64/46.35  thf(21190,plain,(! [A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (r @ a @ B)) @ sk1)))),inference(pre_uni,[status(thm)],[21122:[bind(A, $thf(A)),bind(B, $thf(C)),bind(C, $thf(C)),bind(D, $thf(r @ a))]])).
% 166.64/46.35  thf(93,plain,(! [D:mu,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (~ (a1 @ A @ C)) | ~ (($true)) | ((B @ C) != (p @ D @ (sk2 @ D))))),inference(paramod_ordered,[status(thm)],[30,16])).
% 166.64/46.35  thf(94,plain,(! [D:mu,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (~ (a1 @ A @ C)) | ((B @ C) != (p @ D @ (sk2 @ D))))),inference(simp,[status(thm)],[93])).
% 166.64/46.35  thf(126,plain,(! [C:mu,B:($i > mu),A:$i] : ((a2 @ A @ (sk4 @ (^ [D:$i]: (p @ (B @ D) @ D)) @ A)) | (~ (a1 @ A @ (sk2 @ C))) | (C != (B @ (sk2 @ C))))),inference(pre_uni,[status(thm)],[94:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (p @ (E @ F) @ F))),bind(C, $thf(sk2 @ H)),bind(D, $thf(E @ (sk2 @ H)))]])).
% 166.64/46.35  thf(128,plain,(! [C:mu,B:($i > mu),A:$i] : ((~ (a1 @ A @ (sk2 @ C))) | (a2 @ A @ (sk4 @ (^ [D:$i]: (p @ (B @ D) @ D)) @ A)) | (C != (B @ (sk2 @ C))))),inference(pre_uni,[status(thm)],[126:[]])).
% 166.64/46.35  thf(130,plain,(! [C:mu,B:($i > mu),A:$i] : ((~ (a1 @ A @ (sk2 @ C))) | (a2 @ A @ (sk4 @ (^ [D:$i]: (p @ (B @ D) @ D)) @ A)) | (C != (B @ (sk2 @ C))))),inference(simp,[status(thm)],[128])).
% 166.64/46.35  thf(18088,plain,(! [A:mu] : ((~ (~ ((sk2 @ A) = (sk11 @ A)))) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(func_ext,[status(esa)],[17727])).
% 166.64/46.35  thf(18362,plain,(! [A:mu] : (((sk2 @ A) = (sk11 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(cnf,[status(esa)],[18088])).
% 166.64/46.35  thf(18363,plain,(! [A:mu] : (((sk11 @ A) = (sk2 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(lifteq,[status(thm)],[18362])).
% 166.64/46.35  thf(20824,plain,(! [E:($i > $o),D:mu,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ~ (($true)) | ((E @ (sk2 @ D)) != (~ (E @ (sk4 @ (E) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ sk1))))),inference(paramod_ordered,[status(thm)],[19360,4496])).
% 166.64/46.35  thf(20825,plain,(! [E:($i > $o),D:mu,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((E @ (sk2 @ D)) != (~ (E @ (sk4 @ (E) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ sk1))))),inference(simp,[status(thm)],[20824])).
% 166.64/46.35  thf(20972,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[20825:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk4 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ sk1))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 166.64/46.35  thf(21019,plain,(! [D:($i > mu),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))))),inference(simp,[status(thm)],[20972])).
% 166.64/46.35  thf(23383,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | ~ (($true)) | (C @ (sk2 @ B)) | ((a2 @ sk1 @ (sk12 @ A)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[23046,3248])).
% 166.64/46.35  thf(23384,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) | (C @ (sk2 @ B)) | ((a2 @ sk1 @ (sk12 @ A)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[23383])).
% 166.64/46.35  thf(23744,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ (B @ (sk2 @ A)))))),inference(pre_uni,[status(thm)],[23384:[bind(A, $thf(F @ (sk4 @ (^ [E:$i]: (a2 @ sk1 @ (sk12 @ (F @ E)))) @ sk1))),bind(B, $thf(B)),bind(C, $thf(^ [E:$i]: (a2 @ sk1 @ (sk12 @ (F @ E)))))]])).
% 166.64/46.35  thf(23847,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk12 @ (B @ (sk2 @ A)))))),inference(simp,[status(thm)],[23744])).
% 166.64/46.35  thf(29467,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((a2 @ sk1 @ (sk12 @ (B @ (sk2 @ A)))) != (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[23847])).
% 166.64/46.35  thf(29573,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (sk1 != sk1) | ((sk12 @ (B @ (sk2 @ A))) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[29467])).
% 166.64/46.35  thf(29698,plain,(! [B:($i > mu),A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk12 @ (B @ (sk2 @ A))) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)))),inference(simp,[status(thm)],[29573])).
% 166.64/46.35  thf(17702,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk2 @ A) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[8641,13980])).
% 166.64/46.35  thf(17703,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk2 @ A) != (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[17702])).
% 166.64/46.35  thf(17704,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk2 @ A) != (sk4 @ (^ [B:$i]: (($true))) @ sk1)))),inference(pattern_uni,[status(thm)],[17703:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(48,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk7 @ (B) @ A)) | (~ (a1 @ A @ C)) | (~ (a2 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[47])).
% 166.64/46.35  thf(46709,plain,(! [D:($i > $o),C:$i,B:$i,A:mu] : ((a2 @ B @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ B)) | ~ (($true)) | (~ (D @ C)) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[15,137])).
% 166.64/46.35  thf(46710,plain,(! [D:($i > $o),C:$i,B:$i,A:mu] : ((a2 @ B @ (sk4 @ (^ [E:$i]: ~ (D @ E)) @ B)) | (~ (D @ C)) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[46709])).
% 166.64/46.35  thf(46711,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (A @ C)) @ sk1)) | (~ (A @ (sk2 @ B))))),inference(pattern_uni,[status(thm)],[46710:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(sk2 @ E))]])).
% 166.64/46.35  thf(47174,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (A @ C)) @ sk1)) | (~ (A @ (sk2 @ B))))),inference(simp,[status(thm)],[46711])).
% 166.64/46.35  thf(31072,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (~ (($true)) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[15,19373])).
% 166.64/46.35  thf(31073,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(simp,[status(thm)],[31072])).
% 166.64/46.35  thf(31189,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | (sk1 != C) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[31073])).
% 166.64/46.35  thf(31375,plain,(! [C:($i > mu),B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[31189])).
% 166.64/46.35  thf(41301,plain,(! [E:($i > mu),D:mu,C:$i,B:$i,A:mu] : (~ (($true)) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (E @ (sk2 @ D)))) != (~ (r @ a @ (sk2 @ (E @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (E @ F)))) @ sk1)))))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[15,19355])).
% 166.64/46.35  thf(41302,plain,(! [E:($i > mu),D:mu,C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (E @ (sk2 @ D)))) != (~ (r @ a @ (sk2 @ (E @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (E @ F)))) @ sk1)))))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(simp,[status(thm)],[41301])).
% 166.64/46.35  thf(41322,plain,(! [E:($i > mu),D:mu,C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (E @ (sk2 @ D)))) != (~ (r @ a @ (sk2 @ (E @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (E @ F)))) @ sk1)))))) | (sk1 != C) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[41302])).
% 166.64/46.35  thf(41508,plain,(! [D:($i > mu),C:mu,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk2 @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ sk1)))))) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[41322])).
% 166.64/46.35  thf(18807,plain,(! [D:mu,C:mu,B:$i,A:$i] : (~ (($true)) | (~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[26,274])).
% 166.64/46.35  thf(18808,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ sk1)))),inference(simp,[status(thm)],[18807])).
% 166.64/46.35  thf(18974,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((r @ C @ (sk2 @ D)) | (~ (s @ C @ sk1)) | (A != B) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[18808])).
% 166.64/46.35  thf(19009,plain,(! [C:mu,B:mu,A:$i] : ((r @ B @ (sk2 @ C)) | (~ (s @ B @ sk1)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[18974])).
% 166.64/46.35  thf(107,plain,(! [D:($i > $i),C:($i > mu),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [E:$i]: (s @ (C @ E) @ (D @ E))) @ A)) | (~ (a1 @ A @ B)) | (s @ (C @ B) @ (D @ B)))),inference(prim_subst,[status(thm)],[30:[bind(A, $thf(A)),bind(B, $thf(^ [F:$i]: (s @ (D @ F) @ (E @ F))))]])).
% 166.64/46.35  thf(139,plain,(! [D:($i > $i),C:($i > mu),B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [E:$i]: (s @ (C @ E) @ (D @ E))) @ A)) | (~ (a1 @ A @ B)) | (s @ (C @ B) @ (D @ B)))),inference(simp,[status(thm)],[107])).
% 166.64/46.35  thf(21109,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,3388])).
% 166.64/46.35  thf(21110,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21109])).
% 166.64/46.35  thf(21171,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))))),inference(pre_uni,[status(thm)],[21110:[bind(A, $thf(A)),bind(B, $thf(F @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))) @ sk1))),bind(C, $thf(^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))))]])).
% 166.64/46.35  thf(21208,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))))),inference(simp,[status(thm)],[21171])).
% 166.64/46.35  thf(20865,plain,(! [D:($i > $o),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ~ (($true)) | ((D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(paramod_ordered,[status(thm)],[19360,3387])).
% 166.64/46.35  thf(20866,plain,(! [D:($i > $o),C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((D @ (sk4 @ (^ [E:$i]: ~ (a1 @ sk1 @ E)) @ sk1)) != (~ (D @ (sk4 @ (D) @ sk1)))) | ((r @ a @ (sk2 @ C)) != (D @ (sk4 @ (D) @ sk1))))),inference(simp,[status(thm)],[20865])).
% 166.64/46.35  thf(20962,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[20866:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ sk1))),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 166.64/46.35  thf(21005,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(simp,[status(thm)],[20962])).
% 166.64/46.35  thf(21042,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (^ [D:$i]: ~ (a1 @ sk1 @ D))) | ~ (($true)) | ((C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,14662])).
% 166.64/46.35  thf(21043,plain,(! [C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (^ [D:$i]: ~ (a1 @ sk1 @ D))) | ((C @ (sk4 @ (^ [D:$i]: ~ (a1 @ sk1 @ D)) @ sk1)) != (~ (C @ (sk4 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21042])).
% 166.64/46.35  thf(21180,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (^ [C:$i]: ~ (a1 @ sk1 @ C))) | ((r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))) != (~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[21043:[bind(A, $thf(A)),bind(B, $thf(F @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))) @ sk1))),bind(C, $thf(^ [E:$i]: (r @ a @ (sk2 @ (F @ E)))))]])).
% 166.64/46.35  thf(21217,plain,(! [B:($i > mu),A:$i] : (((sk3 @ A) != sk1) | (((=) @ $i @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (^ [C:$i]: ~ (a1 @ sk1 @ C))) | ((r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)))) != (~ (r @ a @ (sk2 @ (B @ (sk4 @ (^ [C:$i]: (r @ a @ (sk2 @ (B @ C)))) @ sk1)))))))),inference(simp,[status(thm)],[21180])).
% 166.64/46.35  thf(36,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((a1 @ A @ (sk5 @ (B) @ A)) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[35])).
% 166.64/46.35  thf(50,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk7 @ (B) @ A) = (sk7 @ ((=) @ $i @ (sk7 @ B @ A)) @ A))) | (~ (a1 @ A @ C)) | (~ (a2 @ C @ D)) | ((sk7 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[49:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk7 @ B @ A)))]])).
% 166.64/46.35  thf(51,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk7 @ (B) @ A) != (sk7 @ ((=) @ $i @ (sk7 @ B @ A)) @ A)) | ((sk7 @ (B) @ A) = D) | (~ (a1 @ A @ C)) | (~ (a2 @ C @ D)))),inference(lifteq,[status(thm)],[50])).
% 166.64/46.35  thf(308,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[15,214])).
% 166.64/46.35  thf(309,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[308])).
% 166.64/46.35  thf(341,plain,((a2 @ sk1 @ (sk4 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1))),inference(pre_uni,[status(thm)],[309:[bind(A, $thf(B)),bind(B, $thf(B)),bind(C, $thf(a1 @ sk1))]])).
% 166.64/46.35  thf(23578,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[23046,214])).
% 166.64/46.35  thf(23579,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[23578])).
% 166.64/46.35  thf(23765,plain,(! [A:mu] : ((a2 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1))) @ sk1)))),inference(pre_uni,[status(thm)],[23579:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [D:$i]: (a2 @ sk1 @ (sk4 @ (^ [E:$i]: (($true))) @ sk1))))]])).
% 166.64/46.35  thf(21077,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (C @ (sk2 @ D)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[21011,888])).
% 166.64/46.35  thf(21078,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | (C @ (sk2 @ D)) | ((r @ a @ (sk2 @ B)) != (C @ (sk4 @ (C) @ sk1))))),inference(simp,[status(thm)],[21077])).
% 166.64/46.35  thf(21184,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk2 @ B)))))),inference(pre_uni,[status(thm)],[21078:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ sk1))),bind(C, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F))))),bind(D, $thf(D))]])).
% 166.64/46.35  thf(21221,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk2 @ B)))))),inference(simp,[status(thm)],[21184])).
% 166.64/46.35  thf(89,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (~ (a1 @ A @ C)) | (~ (a2 @ D @ F)) | ~ (($true)) | (~ (q @ E @ G)) | (p @ E @ F) | ((B @ C) != (a2 @ F @ G)))),inference(paramod_ordered,[status(thm)],[30,18])).
% 166.64/46.35  thf(90,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk4 @ (B) @ A)) | (~ (a1 @ A @ C)) | (~ (a2 @ D @ F)) | (~ (q @ E @ G)) | (p @ E @ F) | ((B @ C) != (a2 @ F @ G)))),inference(simp,[status(thm)],[89])).
% 166.64/46.35  thf(129,plain,(! [F:($i > $i),E:($i > $i),D:mu,C:$i,B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [G:$i]: (a2 @ (E @ G) @ (F @ G))) @ A)) | (~ (a1 @ A @ B)) | (~ (a2 @ C @ (E @ B))) | (~ (q @ D @ (F @ B))) | (p @ D @ (E @ B)))),inference(pre_uni,[status(thm)],[90:[bind(A, $thf(A)),bind(B, $thf(^ [J:$i]: (a2 @ (H @ J) @ (I @ J)))),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(H @ C)),bind(G, $thf(I @ C))]])).
% 166.64/46.35  thf(131,plain,(! [F:($i > $i),E:($i > $i),D:mu,C:$i,B:$i,A:$i] : ((a2 @ A @ (sk4 @ (^ [G:$i]: (a2 @ (E @ G) @ (F @ G))) @ A)) | (~ (a1 @ A @ B)) | (~ (a2 @ C @ (E @ B))) | (~ (q @ D @ (F @ B))) | (p @ D @ (E @ B)))),inference(simp,[status(thm)],[129])).
% 166.64/46.35  thf(24172,plain,(! [B:($i > $o),A:mu] : ((a1 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ~ (($true)) | ((B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1))))),inference(paramod_ordered,[status(thm)],[23114,7140])).
% 166.64/46.35  thf(24173,plain,(! [B:($i > $o),A:mu] : ((a1 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | ((B @ (sk4 @ (^ [C:$i]: ~ (a1 @ sk1 @ C)) @ sk1)) != (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1))))),inference(simp,[status(thm)],[24172])).
% 166.64/46.35  thf(24310,plain,(! [A:mu] : ((a1 @ sk1 @ (sk12 @ A)) | (a2 @ sk1 @ (sk4 @ (^ [B:$i]: ~ (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1))) @ sk1)))),inference(pre_uni,[status(thm)],[24173:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (a2 @ sk1 @ (sk4 @ (^ [D:$i]: (($true))) @ sk1))))]])).
% 166.64/46.35  thf(1464,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a2 @ B @ D)) | ~ (($true)) | (~ (q @ C @ E)) | (p @ C @ D) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ D @ E)))),inference(paramod_ordered,[status(thm)],[1449,18])).
% 166.64/46.35  thf(1465,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a2 @ B @ D)) | (~ (q @ C @ E)) | (p @ C @ D) | ((a2 @ sk1 @ (sk2 @ A)) != (a2 @ D @ E)))),inference(simp,[status(thm)],[1464])).
% 166.64/46.35  thf(1466,plain,(! [C:mu,B:mu,A:$i] : ((~ (a2 @ A @ sk1)) | (~ (q @ B @ (sk2 @ C))) | (p @ B @ sk1))),inference(pattern_uni,[status(thm)],[1465:[bind(A, $thf(F)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk1)),bind(E, $thf(sk2 @ F))]])).
% 166.64/46.35  thf(1490,plain,(! [C:mu,B:mu,A:$i] : ((~ (a2 @ A @ sk1)) | (~ (q @ B @ (sk2 @ C))) | (p @ B @ sk1))),inference(simp,[status(thm)],[1466])).
% 166.64/46.35  thf(23020,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | (a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk12 @ A) = (sk2 @ B)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(paramod_ordered,[status(thm)],[20520,8641])).
% 166.64/46.35  thf(23021,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [C:$i]: (($true))) @ sk1)) | ((sk12 @ A) = (sk2 @ B)) | ((sk4 @ (^ [C:$i]: ~ ((sk2 @ A) = C)) @ sk1) != (sk4 @ (^ [C:$i]: ~ ((sk2 @ B) = C)) @ sk1)))),inference(simp,[status(thm)],[23020])).
% 166.64/46.35  thf(23022,plain,(! [A:mu] : ((a2 @ sk1 @ (sk4 @ (^ [B:$i]: (($true))) @ sk1)) | ((sk12 @ A) = (sk2 @ A)))),inference(pattern_uni,[status(thm)],[23021:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 166.64/46.35  thf(68871,plain,(($false)),inference(e,[status(thm)],[23832,21439,16533,365,138,23056,20520,11603,14662,202,16481,21192,23061,21467,42,4496,17727,37,21210,8515,24418,3248,52,1087,20,46,19355,57,4253,23011,23074,27675,132,133,74,439,18145,24572,798,23703,28,33,21,137,229,21206,23853,3210,19373,23046,24412,134,73,237,41491,25043,2189,888,21226,8641,34,45,17,38955,21218,3387,22,1488,27,24415,12,54,49,21222,274,12354,39,31384,13980,21190,13486,130,18363,135,21019,29698,9111,13861,17704,48,18,16,1038,31,47174,3388,43,7659,31375,41508,7653,40,26,19009,55,139,23114,23,21208,21011,23847,214,21005,21217,7140,36,30,51,19,341,12352,23765,21221,2600,15,62,3392,131,24310,1490,1449,23022,1069])).
% 166.64/46.35  % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 166.64/46.35  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------