%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV426^2 : TPTP v9.3.1. Released v3.6.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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:39:51 AM UTC 2026
% Result : Theorem 87.79s 17.19s
% Output : Refutation 74.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV426^2 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.09/0.21 % Computer : n018.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 16:05:03 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/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.68/0.52 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.05/0.66 % [INFO] Parsing done (140ms).
% 1.05/0.67 % [INFO] Running in sequential loop mode.
% 1.63/0.87 % [INFO] eprover registered as external prover.
% 1.63/0.88 % [INFO] Scanning for conjecture ...
% 1.86/0.95 % [INFO] Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ...
% 1.86/0.97 % [INFO] Axiom selection finished. Selected 2 axioms (removed 0 axioms).
% 1.86/0.97 % [INFO] Problem is higher-order (TPTP THF).
% 1.86/0.97 % [INFO] Type checking passed.
% 1.86/0.97 % [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 ...
% 87.79/17.18 % External prover 'e' found a proof!
% 87.79/17.19 % [INFO] Killing All external provers ...
% 87.79/17.19 % Time passed: 16887ms (effective reasoning time: 16516ms)
% 87.79/17.19 % 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)>
% 87.79/17.19 % Axioms used in derivation (2): trans_axiom, refl_axiom
% 87.79/17.19 % No. of inferences in proof: 316
% 87.79/17.19 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 16887 ms resp. 16516 ms w/o parsing
% 74.78/17.45 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 74.78/17.45 thf(individuals_type, type, individuals: $tType).
% 74.78/17.45 thf(prop_a_decl, type, prop_a: ($i > $o)).
% 74.78/17.45 thf(prop_c_decl, type, prop_c: ($i > $o)).
% 74.78/17.45 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 74.78/17.45 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.78/17.45 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.78/17.45 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 74.78/17.45 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 74.78/17.45 thf(rel_decl, type, rel: ($i > ($i > $o))).
% 74.78/17.45 thf(icl_atom_decl, type, icl_atom: (($i > $o) > ($i > $o))).
% 74.78/17.45 thf(icl_princ_decl, type, icl_princ: (($i > $o) > ($i > $o))).
% 74.78/17.45 thf(icl_impl_decl, type, icl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.78/17.45 thf(icl_says_decl, type, icl_says: (($i > $o) > (($i > $o) > ($i > $o)))).
% 74.78/17.45 thf(iclval_decl, type, iclval: (($i > $o) > $o)).
% 74.78/17.45 thf(s_decl, type, s: ($i > $o)).
% 74.78/17.45 thf(t_decl, type, t: ($i > $o)).
% 74.78/17.45 thf(a_decl, type, a: ($i > $o)).
% 74.78/17.45 thf(sk1_decl, type, sk1: $i).
% 74.78/17.45 thf(sk2_decl, type, sk2: $i).
% 74.78/17.45 thf(sk3_decl, type, sk3: ($i > ($i > $i))).
% 74.78/17.45 thf(sk4_decl, type, sk4: $i).
% 74.78/17.45 thf(sk5_decl, type, sk5: $i).
% 74.78/17.45 thf(sk6_decl, type, sk6: $i).
% 74.78/17.45 thf(sk7_decl, type, sk7: ($i > (($i > $o) > $i))).
% 74.78/17.45 thf(sk8_decl, type, sk8: ($i > (($i > $o) > $i))).
% 74.78/17.45 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 74.78/17.45 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 74.78/17.45 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 74.78/17.45 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 74.78/17.45 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 74.78/17.45 thf(icl_atom_def, definition, icl_atom = (mbox @ rel) ).
% 74.78/17.45 thf(icl_princ_def, definition, icl_princ = (^ [A:($i > $o)]: (A)) ).
% 74.78/17.45 thf(icl_impl_def, definition, icl_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 74.78/17.45 thf(icl_says_def, definition, icl_says = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mor @ A @ B))) ).
% 74.78/17.45 thf(iclval_def, definition, iclval = (mvalid) ).
% 74.78/17.45 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => ((a @ C) | ! [D:$i]: ((rel @ C @ D) => (~ (! [E:$i]: ((rel @ D @ E) => (s @ E))) | ! [E:$i]: ((rel @ D @ E) => (t @ E))))))) | ! [C:$i]: ((rel @ B @ C) => (~ (! [D:$i]: ((rel @ C @ D) => ((a @ D) | ! [E:$i]: ((rel @ D @ E) => (s @ E))))) | ! [D:$i]: ((rel @ C @ D) => ((a @ D) | ! [E:$i]: ((rel @ D @ E) => (t @ E)))))))))) ).
% 74.78/17.45 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ ((rel @ sk1 @ A) => (~ (! [B:$i]: ((rel @ A @ B) => ((a @ B) | ! [C:$i]: ((rel @ B @ C) => (~ (! [D:$i]: ((rel @ C @ D) => (s @ D))) | ! [D:$i]: ((rel @ C @ D) => (t @ D))))))) | ! [B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => ((a @ C) | ! [D:$i]: ((rel @ C @ D) => (s @ D))))) | ! [C:$i]: ((rel @ B @ C) => ((a @ C) | ! [D:$i]: ((rel @ C @ D) => (t @ D))))))))) ).
% 74.78/17.45 thf(sk3_def, definition, sk3 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ ((rel @ A @ C) => (s @ C)))) ).
% 74.78/17.45 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ ((rel @ sk2 @ A) => (~ (! [B:$i]: ((rel @ A @ B) => ((a @ B) | ! [C:$i]: ((rel @ B @ C) => (s @ C))))) | ! [B:$i]: ((rel @ A @ B) => ((a @ B) | ! [C:$i]: ((rel @ B @ C) => (t @ C))))))) ).
% 74.78/17.45 thf(sk5_def, definition, sk5 = (@+ [A:$i]: ~ ((rel @ sk4 @ A) => ((a @ A) | ! [B:$i]: ((rel @ A @ B) => (t @ B))))) ).
% 74.78/17.45 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ ((rel @ sk5 @ A) => (t @ A))) ).
% 74.78/17.45 thf(sk7_def, definition, sk7 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 74.78/17.45 thf(sk8_def, definition, sk8 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 74.78/17.45 thf(1,conjecture,((iclval @ (icl_impl @ (icl_says @ (icl_princ @ a) @ (icl_impl @ (icl_atom @ s) @ (icl_atom @ t))) @ (icl_impl @ (icl_says @ (icl_princ @ a) @ (icl_atom @ s)) @ (icl_says @ (icl_princ @ a) @ (icl_atom @ t)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cuc)).
% 74.78/17.45 thf(2,negated_conjecture,((~ (iclval @ (icl_impl @ (icl_says @ (icl_princ @ a) @ (icl_impl @ (icl_atom @ s) @ (icl_atom @ t))) @ (icl_impl @ (icl_says @ (icl_princ @ a) @ (icl_atom @ s)) @ (icl_says @ (icl_princ @ a) @ (icl_atom @ t))))))),inference(neg_conjecture,[status(cth)],[1])).
% 74.78/17.45 thf(5,plain,((~ (! [A:$i,B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => ((a @ C) | ! [D:$i]: ((rel @ C @ D) => (~ (! [E:$i]: ((rel @ D @ E) => (s @ E))) | ! [E:$i]: ((rel @ D @ E) => (t @ E))))))) | ! [C:$i]: ((rel @ B @ C) => (~ (! [D:$i]: ((rel @ C @ D) => ((a @ D) | ! [E:$i]: ((rel @ D @ E) => (s @ E))))) | ! [D:$i]: ((rel @ C @ D) => ((a @ D) | ! [E:$i]: ((rel @ D @ E) => (t @ E))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 74.78/17.45 thf(6,plain,(! [E:$i,D:$i,C:$i,B:$i,A:$i] : (((rel @ sk1 @ sk2) & (~ (rel @ sk2 @ A) | (a @ A) | ~ (rel @ A @ B) | (rel @ B @ (sk3 @ B @ A)) | ~ (rel @ B @ C) | (t @ C)) & (~ (rel @ sk2 @ A) | (a @ A) | ~ (rel @ A @ B) | ~ (s @ (sk3 @ B @ A)) | ~ (rel @ B @ C) | (t @ C)) & (rel @ sk2 @ sk4) & (~ (rel @ sk4 @ D) | (a @ D) | ~ (rel @ D @ E) | (s @ E)) & (rel @ sk4 @ sk5) & ~ (a @ sk5) & (rel @ sk5 @ sk6) & ~ (t @ sk6)))),inference(cnf,[status(esa)],[5])).
% 74.78/17.45 thf(12,plain,((rel @ sk5 @ sk6)),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ (mbox @ rel @ (mbox @ rel @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trans_axiom)).
% 74.78/17.45 thf(23,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | ! [C:$i]: ((rel @ B @ C) => (! [D:$i]: ((rel @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 74.78/17.45 thf(24,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((rel @ B @ (sk8 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D)) & (~ (A @ (sk8 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[23])).
% 74.78/17.45 thf(26,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[24])).
% 74.78/17.45 thf(14,plain,((~ (a @ sk5))),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(37,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ~ (($true)) | ((A @ D) != (a @ sk5)))),inference(paramod_ordered,[status(thm)],[26,14])).
% 74.78/17.45 thf(38,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((A @ D) != (a @ sk5)))),inference(simp,[status(thm)],[37])).
% 74.78/17.45 thf(103,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk5)))),inference(pre_uni,[status(thm)],[38:[bind(A, $thf(a)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk5))]])).
% 74.78/17.45 thf(146,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk5)))),inference(simp,[status(thm)],[103])).
% 74.78/17.45 thf(346,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ sk6) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,146])).
% 74.78/17.45 thf(347,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ sk6) != (rel @ A @ B)))),inference(simp,[status(thm)],[346])).
% 74.78/17.45 thf(348,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (rel @ sk6 @ sk5))),inference(pattern_uni,[status(thm)],[347:[bind(A, $thf(sk5)),bind(B, $thf(sk6))]])).
% 74.78/17.45 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',refl_axiom)).
% 74.78/17.45 thf(17,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 74.78/17.45 thf(18,plain,(! [B:$i,A:($i > $o)] : ((((rel @ B @ (sk7 @ B @ (A))) | (A @ B)) & (~ (A @ (sk7 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[17])).
% 74.78/17.45 thf(19,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[18])).
% 74.78/17.45 thf(363,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ A @ B)) | ((rel @ B @ sk5) != (rel @ A @ B)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[146])).
% 74.78/17.45 thf(371,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (rel @ sk5 @ sk5))),inference(pattern_uni,[status(thm)],[363:[bind(A, $thf(sk5)),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(1461,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((A @ B) != (rel @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[19,371])).
% 74.78/17.45 thf(1462,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk5 @ (a)))) | ((A @ B) != (rel @ sk5 @ sk5)))),inference(simp,[status(thm)],[1461])).
% 74.78/17.45 thf(1470,plain,((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) | (~ (a @ (sk8 @ sk5 @ (a))))),inference(pre_uni,[status(thm)],[1462:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(9569,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [C:$i]: (rel @ C @ C)))) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[1470,146])).
% 74.78/17.45 thf(9570,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [C:$i]: (rel @ C @ C)))) != (rel @ A @ B)))),inference(simp,[status(thm)],[9569])).
% 74.78/17.45 thf(9571,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (a @ (sk8 @ sk5 @ (a)))) | (~ (rel @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) @ sk5))),inference(pattern_uni,[status(thm)],[9570:[bind(A, $thf(sk5)),bind(B, $thf(sk7 @ sk5 @ (^ [C:$i]: (rel @ C @ C))))]])).
% 74.78/17.45 thf(9658,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (rel @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) @ sk5))),inference(simp,[status(thm)],[9571])).
% 74.78/17.45 thf(455,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(prop_c))]])).
% 74.78/17.45 thf(526,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[455])).
% 74.78/17.45 thf(461,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 74.78/17.45 thf(531,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[461])).
% 74.78/17.45 thf(7,plain,((rel @ sk4 @ sk5)),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(357,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk4 @ sk5) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[7,146])).
% 74.78/17.45 thf(358,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk4 @ sk5) != (rel @ A @ B)))),inference(simp,[status(thm)],[357])).
% 74.78/17.45 thf(359,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (~ (rel @ sk5 @ sk5))),inference(pattern_uni,[status(thm)],[358:[bind(A, $thf(sk4)),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(1279,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[531,359])).
% 74.78/17.45 thf(1280,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk5 @ sk5)))),inference(simp,[status(thm)],[1279])).
% 74.78/17.45 thf(1303,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk4 @ (a)))) | (A != sk5) | ((sk7 @ A @ (^ [B:$i]: (($false)))) != sk5))),inference(simp,[status(thm)],[1280])).
% 74.78/17.45 thf(1322,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (($false)))) != sk5)),inference(simp,[status(thm)],[1303])).
% 74.78/17.45 thf(13,plain,((rel @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(15,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (~ (rel @ A @ B)) | (s @ B))),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(16,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (~ (rel @ A @ B)) | (s @ B))),inference(simp,[status(thm)],[15])).
% 74.78/17.45 thf(1140,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | ~ (($true)) | (s @ B) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[13,16])).
% 74.78/17.45 thf(1141,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (s @ B) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(simp,[status(thm)],[1140])).
% 74.78/17.45 thf(1142,plain,((~ (rel @ sk4 @ sk1)) | (a @ sk1) | (s @ sk2)),inference(pattern_uni,[status(thm)],[1141:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 74.78/17.45 thf(4093,plain,(~ (($true)) | (a @ sk1) | (s @ sk2) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk1))),inference(paramod_ordered,[status(thm)],[7,1142])).
% 74.78/17.45 thf(4094,plain,((a @ sk1) | (s @ sk2) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk1))),inference(simp,[status(thm)],[4093])).
% 74.78/17.45 thf(4115,plain,((a @ sk1) | (s @ sk2) | (sk4 != sk4) | (sk5 != sk1)),inference(simp,[status(thm)],[4094])).
% 74.78/17.45 thf(4141,plain,((a @ sk1) | (s @ sk2) | (sk5 != sk1)),inference(simp,[status(thm)],[4115])).
% 74.78/17.45 thf(4171,plain,((s @ sk2) | (sk5 != sk1) | ~ (($true)) | ((a @ sk5) != (a @ sk1))),inference(paramod_ordered,[status(thm)],[4141,14])).
% 74.78/17.45 thf(4172,plain,((s @ sk2) | (sk5 != sk1) | ((a @ sk5) != (a @ sk1))),inference(simp,[status(thm)],[4171])).
% 74.78/17.45 thf(4245,plain,((s @ sk2) | (sk5 != sk1) | (sk5 != sk1)),inference(simp,[status(thm)],[4172])).
% 74.78/17.45 thf(4262,plain,((s @ sk2) | (sk5 != sk1)),inference(simp,[status(thm)],[4245])).
% 74.78/17.45 thf(44,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | ~ (($true)) | (A @ D) | ((rel @ sk4 @ sk5) != (rel @ C @ D)))),inference(paramod_ordered,[status(thm)],[7,26])).
% 74.78/17.45 thf(45,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (A @ D) | ((rel @ sk4 @ sk5) != (rel @ C @ D)))),inference(simp,[status(thm)],[44])).
% 74.78/17.45 thf(46,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ sk4)) | (A @ sk5))),inference(pattern_uni,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk4)),bind(D, $thf(sk5))]])).
% 74.78/17.45 thf(80,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk8 @ B @ (A)) = (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A))))) | (~ (rel @ B @ sk4)) | ((sk8 @ B @ (A)) = sk5))),inference(replace_leibeq,[status(thm)],[46:[bind(A, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 74.78/17.45 thf(88,plain,(! [B:$i,A:($i > $o)] : (((sk8 @ B @ (A)) != (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A)))) | ((sk8 @ B @ (A)) = sk5) | (~ (rel @ B @ sk4)))),inference(lifteq,[status(thm)],[80])).
% 74.78/17.45 thf(10,plain,((rel @ sk2 @ sk4)),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(336,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk2 @ sk4) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[10,146])).
% 74.78/17.45 thf(337,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk2 @ sk4) != (rel @ A @ B)))),inference(simp,[status(thm)],[336])).
% 74.78/17.45 thf(338,plain,((~ (a @ (sk8 @ sk2 @ (a)))) | (~ (rel @ sk4 @ sk5))),inference(pattern_uni,[status(thm)],[337:[bind(A, $thf(sk2)),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(381,plain,((~ (a @ (sk8 @ sk2 @ (a)))) | ~ (($true))),inference(rewrite,[status(thm)],[338,7])).
% 74.78/17.45 thf(382,plain,((~ (a @ (sk8 @ sk2 @ (a))))),inference(simp,[status(thm)],[381])).
% 74.78/17.45 thf(432,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | ((A @ B) != (a @ (sk8 @ sk2 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,382])).
% 74.78/17.45 thf(433,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ((A @ B) != (a @ (sk8 @ sk2 @ (a)))))),inference(simp,[status(thm)],[432])).
% 74.78/17.45 thf(481,plain,((rel @ (sk8 @ sk2 @ (a)) @ (sk7 @ (sk8 @ sk2 @ (a)) @ (a)))),inference(pre_uni,[status(thm)],[433:[bind(A, $thf(a)),bind(B, $thf(sk8 @ sk2 @ (a)))]])).
% 74.78/17.45 thf(391,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | ((A @ B) != (a @ sk5)))),inference(paramod_ordered,[status(thm)],[19,14])).
% 74.78/17.45 thf(392,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ((A @ B) != (a @ sk5)))),inference(simp,[status(thm)],[391])).
% 74.78/17.45 thf(490,plain,((rel @ sk5 @ (sk7 @ sk5 @ (a)))),inference(pre_uni,[status(thm)],[392:[bind(A, $thf(a)),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(341,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[13,146])).
% 74.78/17.45 thf(342,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(simp,[status(thm)],[341])).
% 74.78/17.45 thf(343,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (~ (rel @ sk2 @ sk5))),inference(pattern_uni,[status(thm)],[342:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 74.78/17.45 thf(985,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[490,343])).
% 74.78/17.45 thf(986,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[985])).
% 74.78/17.45 thf(1005,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk5 != sk2) | ((sk7 @ sk5 @ (a)) != sk5)),inference(simp,[status(thm)],[986])).
% 74.78/17.45 thf(983,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk4 @ sk5) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[7,343])).
% 74.78/17.45 thf(984,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk4 @ sk5) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[983])).
% 74.78/17.45 thf(1003,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk4 != sk2) | (sk5 != sk5)),inference(simp,[status(thm)],[984])).
% 74.78/17.45 thf(1021,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk4 != sk2)),inference(simp,[status(thm)],[1003])).
% 74.78/17.45 thf(1034,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk4 != sk2) | ((A @ B) != (a @ (sk8 @ sk1 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1021])).
% 74.78/17.45 thf(1035,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk4 != sk2) | ((A @ B) != (a @ (sk8 @ sk1 @ (a)))))),inference(simp,[status(thm)],[1034])).
% 74.78/17.45 thf(1041,plain,((rel @ sk1 @ (sk7 @ sk1 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk4 != sk2)),inference(pre_uni,[status(thm)],[1035:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk1))]])).
% 74.78/17.45 thf(1443,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk5) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[13,371])).
% 74.78/17.45 thf(1444,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk5 @ sk5) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[1443])).
% 74.78/17.45 thf(1486,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk5 != sk1) | (sk5 != sk2)),inference(simp,[status(thm)],[1444])).
% 74.78/17.45 thf(9540,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk5 @ sk5))),inference(paramod_ordered,[status(thm)],[1470,371])).
% 74.78/17.45 thf(9541,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk5 @ sk5))),inference(simp,[status(thm)],[9540])).
% 74.78/17.45 thf(9622,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk5 != sk5) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk5)),inference(simp,[status(thm)],[9541])).
% 74.78/17.45 thf(9644,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk5)),inference(simp,[status(thm)],[9622])).
% 74.78/17.45 thf(1135,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | ~ (($true)) | (s @ B) | ((rel @ sk2 @ sk4) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[10,16])).
% 74.78/17.45 thf(1136,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (s @ B) | ((rel @ sk2 @ sk4) != (rel @ A @ B)))),inference(simp,[status(thm)],[1135])).
% 74.78/17.45 thf(1137,plain,((~ (rel @ sk4 @ sk2)) | (a @ sk2) | (s @ sk4)),inference(pattern_uni,[status(thm)],[1136:[bind(A, $thf(sk2)),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(8,plain,((~ (t @ sk6))),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(430,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | ((A @ B) != (t @ sk6)))),inference(paramod_ordered,[status(thm)],[19,8])).
% 74.78/17.45 thf(431,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ((A @ B) != (t @ sk6)))),inference(simp,[status(thm)],[430])).
% 74.78/17.45 thf(506,plain,((rel @ sk6 @ (sk7 @ sk6 @ (t)))),inference(pre_uni,[status(thm)],[431:[bind(A, $thf(t)),bind(B, $thf(sk6))]])).
% 74.78/17.45 thf(979,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[506,343])).
% 74.78/17.45 thf(980,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[979])).
% 74.78/17.45 thf(1001,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk6 != sk2) | ((sk7 @ sk6 @ (t)) != sk5)),inference(simp,[status(thm)],[980])).
% 74.78/17.45 thf(25,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk8 @ B @ (A))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[24])).
% 74.78/17.45 thf(1075,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk6 @ sk5) != (rel @ sk5 @ sk6))),inference(paramod_ordered,[status(thm)],[12,348])).
% 74.78/17.45 thf(1076,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk6 @ sk5) != (rel @ sk5 @ sk6))),inference(simp,[status(thm)],[1075])).
% 74.78/17.45 thf(1105,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk5) | (sk6 != sk5)),inference(simp,[status(thm)],[1076])).
% 74.78/17.45 thf(1122,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk5)),inference(simp,[status(thm)],[1105])).
% 74.78/17.45 thf(1247,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk6 != sk5) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1122])).
% 74.78/17.45 thf(1248,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk6 != sk5) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(simp,[status(thm)],[1247])).
% 74.78/17.45 thf(1254,plain,((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk6 != sk5)),inference(pre_uni,[status(thm)],[1248:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(1271,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk5) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[13,359])).
% 74.78/17.45 thf(1272,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ sk5 @ sk5) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[1271])).
% 74.78/17.45 thf(1313,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk1) | (sk5 != sk2)),inference(simp,[status(thm)],[1272])).
% 74.78/17.45 thf(20,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk7 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[18])).
% 74.78/17.45 thf(1277,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk5 @ sk5))),inference(paramod_ordered,[status(thm)],[490,359])).
% 74.78/17.45 thf(1278,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk5 @ sk5))),inference(simp,[status(thm)],[1277])).
% 74.78/17.45 thf(1299,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk5) | ((sk7 @ sk5 @ (a)) != sk5)),inference(simp,[status(thm)],[1278])).
% 74.78/17.45 thf(1319,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((sk7 @ sk5 @ (a)) != sk5)),inference(simp,[status(thm)],[1299])).
% 74.78/17.45 thf(34,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | ~ (($true)) | (A @ D) | ((rel @ sk2 @ sk4) != (rel @ C @ D)))),inference(paramod_ordered,[status(thm)],[10,26])).
% 74.78/17.45 thf(35,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (A @ D) | ((rel @ sk2 @ sk4) != (rel @ C @ D)))),inference(simp,[status(thm)],[34])).
% 74.78/17.45 thf(36,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ sk2)) | (A @ sk4))),inference(pattern_uni,[status(thm)],[35:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk2)),bind(D, $thf(sk4))]])).
% 74.78/17.45 thf(86,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk8 @ B @ (A)) = (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A))))) | (~ (rel @ B @ sk2)) | ((sk8 @ B @ (A)) = sk4))),inference(replace_leibeq,[status(thm)],[36:[bind(A, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 74.78/17.45 thf(93,plain,(! [B:$i,A:($i > $o)] : (((sk8 @ B @ (A)) != (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A)))) | ((sk8 @ B @ (A)) = sk4) | (~ (rel @ B @ sk2)))),inference(lifteq,[status(thm)],[86])).
% 74.78/17.45 thf(1451,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk5 @ sk5))),inference(paramod_ordered,[status(thm)],[490,371])).
% 74.78/17.45 thf(1452,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ sk5 @ sk5))),inference(simp,[status(thm)],[1451])).
% 74.78/17.45 thf(1480,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk5 != sk5) | ((sk7 @ sk5 @ (a)) != sk5)),inference(simp,[status(thm)],[1452])).
% 74.78/17.45 thf(1494,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (a)) != sk5)),inference(simp,[status(thm)],[1480])).
% 74.78/17.45 thf(51,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk8 @ F @ (E)))) | (~ (rel @ F @ G)) | ~ (($true)) | (E @ H) | ((A @ D) != (rel @ G @ H)))),inference(paramod_ordered,[status(thm)],[26,26])).
% 74.78/17.45 thf(52,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk8 @ F @ (E)))) | (~ (rel @ F @ G)) | (E @ H) | ((A @ D) != (rel @ G @ H)))),inference(simp,[status(thm)],[51])).
% 74.78/17.45 thf(79,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ ((sk8 @ F @ (E)) = (sk8 @ F @ ((=) @ $i @ (sk8 @ F @ E))))) | (~ (rel @ F @ G)) | ((sk8 @ F @ (E)) = H) | ((A @ D) != (rel @ G @ H)))),inference(replace_leibeq,[status(thm)],[52:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf((=) @ $i @ (sk8 @ F @ E)))]])).
% 74.78/17.45 thf(89,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : (((sk8 @ F @ (E)) != (sk8 @ F @ ((=) @ $i @ (sk8 @ F @ E)))) | ((sk8 @ F @ (E)) = H) | (~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | ((A @ D) != (rel @ G @ H)))),inference(lifteq,[status(thm)],[79])).
% 74.78/17.45 thf(1065,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk6 @ sk5) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[13,348])).
% 74.78/17.45 thf(1066,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk6 @ sk5) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[1065])).
% 74.78/17.45 thf(1104,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk1) | (sk5 != sk2)),inference(simp,[status(thm)],[1066])).
% 74.78/17.45 thf(1081,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk6 @ sk5)))),inference(paramod_ordered,[status(thm)],[531,348])).
% 74.78/17.45 thf(1082,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk6 @ sk5)))),inference(simp,[status(thm)],[1081])).
% 74.78/17.45 thf(1098,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | (A != sk6) | ((sk7 @ A @ (^ [B:$i]: (($false)))) != sk5))),inference(simp,[status(thm)],[1082])).
% 74.78/17.45 thf(1119,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk6 @ (^ [A:$i]: (($false)))) != sk5)),inference(simp,[status(thm)],[1098])).
% 74.78/17.45 thf(1195,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (s @ B) | ((rel @ A @ B) != (rel @ sk4 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[16])).
% 74.78/17.45 thf(1206,plain,((~ (rel @ sk4 @ sk4)) | (a @ sk4) | (s @ sk4)),inference(pattern_uni,[status(thm)],[1195:[bind(A, $thf(sk4)),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(10193,plain,(~ (($true)) | (a @ sk4) | (s @ sk4) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[7,1206])).
% 74.78/17.45 thf(10194,plain,((a @ sk4) | (s @ sk4) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk4))),inference(simp,[status(thm)],[10193])).
% 74.78/17.45 thf(10253,plain,((a @ sk4) | (s @ sk4) | (sk4 != sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[10194])).
% 74.78/17.45 thf(10277,plain,((a @ sk4) | (s @ sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[10253])).
% 74.78/17.45 thf(11572,plain,((s @ sk4) | (sk5 != sk4) | ~ (($true)) | ((a @ sk5) != (a @ sk4))),inference(paramod_ordered,[status(thm)],[10277,14])).
% 74.78/17.45 thf(11573,plain,((s @ sk4) | (sk5 != sk4) | ((a @ sk5) != (a @ sk4))),inference(simp,[status(thm)],[11572])).
% 74.78/17.45 thf(11705,plain,((s @ sk4) | (sk5 != sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[11573])).
% 74.78/17.45 thf(11723,plain,((s @ sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[11705])).
% 74.78/17.45 thf(583,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[490,146])).
% 74.78/17.45 thf(584,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk5 @ (sk7 @ sk5 @ (a))) != (rel @ A @ B)))),inference(simp,[status(thm)],[583])).
% 74.78/17.45 thf(585,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (~ (rel @ (sk7 @ sk5 @ (a)) @ sk5))),inference(pattern_uni,[status(thm)],[584:[bind(A, $thf(sk5)),bind(B, $thf(sk7 @ sk5 @ (a)))]])).
% 74.78/17.45 thf(3237,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ (sk7 @ sk5 @ (a)) @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,585])).
% 74.78/17.45 thf(3238,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ (sk7 @ sk5 @ (a)) @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[3237])).
% 74.78/17.45 thf(3268,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (a)) != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[3238])).
% 74.78/17.45 thf(3303,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (a)) != sk4)),inference(simp,[status(thm)],[3268])).
% 74.78/17.45 thf(1165,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | ~ (($true)) | (s @ B) | ((rel @ sk4 @ sk5) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[7,16])).
% 74.78/17.45 thf(1166,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (s @ B) | ((rel @ sk4 @ sk5) != (rel @ A @ B)))),inference(simp,[status(thm)],[1165])).
% 74.78/17.45 thf(1167,plain,((~ (rel @ sk4 @ sk4)) | (a @ sk4) | (s @ sk5)),inference(pattern_uni,[status(thm)],[1166:[bind(A, $thf(sk4)),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(5406,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (a @ sk4) | (s @ sk5) | ((A @ B) != (rel @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[19,1167])).
% 74.78/17.45 thf(5407,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (a @ sk4) | (s @ sk5) | ((A @ B) != (rel @ sk4 @ sk4)))),inference(simp,[status(thm)],[5406])).
% 74.78/17.45 thf(5438,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (rel @ A @ A)))) | (a @ sk4) | (s @ sk5)),inference(pre_uni,[status(thm)],[5407:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(1273,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk6) != (rel @ sk5 @ sk5))),inference(paramod_ordered,[status(thm)],[12,359])).
% 74.78/17.45 thf(1274,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ sk5 @ sk6) != (rel @ sk5 @ sk5))),inference(simp,[status(thm)],[1273])).
% 74.78/17.45 thf(1291,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk5) | (sk6 != sk5)),inference(simp,[status(thm)],[1274])).
% 74.78/17.45 thf(1314,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk6 != sk5)),inference(simp,[status(thm)],[1291])).
% 74.78/17.45 thf(1331,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk6 != sk5) | ((A @ B) != (a @ (sk8 @ sk4 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1314])).
% 74.78/17.45 thf(1332,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk6 != sk5) | ((A @ B) != (a @ (sk8 @ sk4 @ (a)))))),inference(simp,[status(thm)],[1331])).
% 74.78/17.45 thf(1338,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk6 != sk5)),inference(pre_uni,[status(thm)],[1332:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(27,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk8 @ B @ (A)) = (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A))))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((sk8 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[26:[bind(A, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 74.78/17.45 thf(28,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk8 @ B @ (A)) != (sk8 @ B @ ((=) @ $i @ (sk8 @ B @ A)))) | ((sk8 @ B @ (A)) = D) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)))),inference(lifteq,[status(thm)],[27])).
% 74.78/17.45 thf(981,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk6) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[12,343])).
% 74.78/17.45 thf(982,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk5 @ sk6) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[981])).
% 74.78/17.45 thf(1017,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk5 != sk2) | (sk6 != sk5)),inference(simp,[status(thm)],[982])).
% 74.78/17.45 thf(9,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (a @ A) | (~ (rel @ A @ B)) | (~ (s @ (sk3 @ B @ A))) | (~ (rel @ B @ C)) | (t @ C))),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.45 thf(1713,plain,(~ (($true)) | (a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk2) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[13,1137])).
% 74.78/17.45 thf(1714,plain,((a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk2) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[1713])).
% 74.78/17.45 thf(1737,plain,((a @ sk2) | (s @ sk4) | (sk4 != sk1) | (sk2 != sk2)),inference(simp,[status(thm)],[1714])).
% 74.78/17.45 thf(1755,plain,((a @ sk2) | (s @ sk4) | (sk4 != sk1)),inference(simp,[status(thm)],[1737])).
% 74.78/17.45 thf(1073,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ sk6 @ sk5))),inference(paramod_ordered,[status(thm)],[506,348])).
% 74.78/17.45 thf(1074,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ sk6 @ sk5))),inference(simp,[status(thm)],[1073])).
% 74.78/17.45 thf(1096,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk6) | ((sk7 @ sk6 @ (t)) != sk5)),inference(simp,[status(thm)],[1074])).
% 74.78/17.45 thf(1118,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk6 @ (t)) != sk5)),inference(simp,[status(thm)],[1096])).
% 74.78/17.45 thf(993,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((A @ B) != (rel @ sk2 @ sk5)))),inference(paramod_ordered,[status(thm)],[19,343])).
% 74.78/17.45 thf(994,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk1 @ (a)))) | ((A @ B) != (rel @ sk2 @ sk5)))),inference(simp,[status(thm)],[993])).
% 74.78/17.45 thf(996,plain,((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (rel @ A @ sk5)))) | (~ (a @ (sk8 @ sk1 @ (a))))),inference(pre_uni,[status(thm)],[994:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk5))),bind(B, $thf(sk2))]])).
% 74.78/17.45 thf(10878,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (rel @ A @ sk5)))) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[996,343])).
% 74.78/17.45 thf(10879,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (rel @ A @ sk5)))) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[10878])).
% 74.78/17.45 thf(10967,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk2 != sk2) | ((sk7 @ sk2 @ (^ [A:$i]: (rel @ A @ sk5))) != sk5)),inference(simp,[status(thm)],[10879])).
% 74.78/17.45 thf(11019,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((sk7 @ sk2 @ (^ [A:$i]: (rel @ A @ sk5))) != sk5)),inference(simp,[status(thm)],[10967])).
% 74.78/17.45 thf(620,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | ~ (($true)) | (~ (rel @ B @ sk5)) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[506,146])).
% 74.78/17.45 thf(621,plain,(! [B:$i,A:$i] : ((~ (a @ (sk8 @ A @ (a)))) | (~ (rel @ B @ sk5)) | ((rel @ sk6 @ (sk7 @ sk6 @ (t))) != (rel @ A @ B)))),inference(simp,[status(thm)],[620])).
% 74.78/17.45 thf(622,plain,((~ (a @ (sk8 @ sk6 @ (a)))) | (~ (rel @ (sk7 @ sk6 @ (t)) @ sk5))),inference(pattern_uni,[status(thm)],[621:[bind(A, $thf(sk6)),bind(B, $thf(sk7 @ sk6 @ (t)))]])).
% 74.78/17.45 thf(1077,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk6 @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,348])).
% 74.78/17.45 thf(1078,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk6 @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[1077])).
% 74.78/17.45 thf(1092,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[1078])).
% 74.78/17.45 thf(1114,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk6 != sk4)),inference(simp,[status(thm)],[1092])).
% 74.78/17.45 thf(997,plain,((rel @ sk5 @ (sk7 @ sk5 @ (rel @ sk2))) | (~ (a @ (sk8 @ sk1 @ (a))))),inference(pre_uni,[status(thm)],[994:[bind(A, $thf(rel @ sk2)),bind(B, $thf(sk5))]])).
% 74.78/17.45 thf(969,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk2 @ sk5) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[13,343])).
% 74.78/17.45 thf(970,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk2 @ sk5) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[969])).
% 74.78/17.45 thf(1002,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk2 != sk1) | (sk5 != sk2)),inference(simp,[status(thm)],[970])).
% 74.78/17.45 thf(4111,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (a @ sk1) | (s @ sk2) | ((A @ B) != (rel @ sk4 @ sk1)))),inference(paramod_ordered,[status(thm)],[19,1142])).
% 74.78/17.45 thf(4112,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (a @ sk1) | (s @ sk2) | ((A @ B) != (rel @ sk4 @ sk1)))),inference(simp,[status(thm)],[4111])).
% 74.78/17.45 thf(4135,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (rel @ A @ sk1)))) | (a @ sk1) | (s @ sk2)),inference(pre_uni,[status(thm)],[4112:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk1))),bind(B, $thf(sk4))]])).
% 74.78/17.45 thf(5372,plain,(~ (($true)) | (a @ sk4) | (s @ sk5) | ((rel @ sk4 @ sk4) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[10,1167])).
% 74.78/17.45 thf(5373,plain,((a @ sk4) | (s @ sk5) | ((rel @ sk4 @ sk4) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[5372])).
% 74.78/17.45 thf(5416,plain,((a @ sk4) | (s @ sk5) | (sk4 != sk2) | (sk4 != sk4)),inference(simp,[status(thm)],[5373])).
% 74.78/17.45 thf(5451,plain,((a @ sk4) | (s @ sk5) | (sk4 != sk2)),inference(simp,[status(thm)],[5416])).
% 74.78/17.45 thf(5386,plain,(~ (($true)) | (a @ sk4) | (s @ sk5) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[7,1167])).
% 74.78/17.45 thf(5387,plain,((a @ sk4) | (s @ sk5) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk4))),inference(simp,[status(thm)],[5386])).
% 74.78/17.45 thf(5417,plain,((a @ sk4) | (s @ sk5) | (sk4 != sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[5387])).
% 74.78/17.45 thf(5452,plain,((a @ sk4) | (s @ sk5) | (sk5 != sk4)),inference(simp,[status(thm)],[5417])).
% 74.78/17.45 thf(7521,plain,((s @ sk5) | (sk5 != sk4) | ~ (($true)) | ((a @ sk5) != (a @ sk4))),inference(paramod_ordered,[status(thm)],[5452,14])).
% 74.78/17.45 thf(7522,plain,((s @ sk5) | (sk5 != sk4) | ((a @ sk5) != (a @ sk4))),inference(simp,[status(thm)],[7521])).
% 74.78/17.45 thf(7632,plain,((s @ sk5) | (sk5 != sk4) | (sk5 != sk4)),inference(simp,[status(thm)],[7522])).
% 74.78/17.45 thf(7639,plain,((s @ sk5) | (sk5 != sk4)),inference(simp,[status(thm)],[7632])).
% 74.78/17.45 thf(21,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk7 @ B @ (A)) = (sk7 @ B @ ((=) @ $i @ (sk7 @ B @ A))))) | ((sk7 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[20:[bind(A, $thf((=) @ $i @ (sk7 @ B @ A)))]])).
% 74.78/17.46 thf(22,plain,(! [B:$i,A:($i > $o)] : (((sk7 @ B @ (A)) != (sk7 @ B @ ((=) @ $i @ (sk7 @ B @ A)))) | ((sk7 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[21])).
% 74.78/17.46 thf(1453,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[531,371])).
% 74.78/17.46 thf(1454,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk5 @ sk5)))),inference(simp,[status(thm)],[1453])).
% 74.78/17.46 thf(1465,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk5 @ (a)))) | (A != sk5) | ((sk7 @ A @ (^ [B:$i]: (($false)))) != sk5))),inference(simp,[status(thm)],[1454])).
% 74.78/17.46 thf(1503,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (($false)))) != sk5)),inference(simp,[status(thm)],[1465])).
% 74.78/17.46 thf(1287,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((A @ B) != (rel @ sk5 @ sk5)))),inference(paramod_ordered,[status(thm)],[19,359])).
% 74.78/17.46 thf(1288,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (~ (a @ (sk8 @ sk4 @ (a)))) | ((A @ B) != (rel @ sk5 @ sk5)))),inference(simp,[status(thm)],[1287])).
% 74.78/17.46 thf(1307,plain,((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) | (~ (a @ (sk8 @ sk4 @ (a))))),inference(pre_uni,[status(thm)],[1288:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk5))]])).
% 74.78/17.46 thf(276,plain,(! [A:$i] : ((~ (t @ (sk7 @ A @ (t)))) | (t @ A))),inference(prim_subst,[status(thm)],[20:[bind(A, $thf(t))]])).
% 74.78/17.46 thf(303,plain,(! [A:$i] : ((~ (t @ (sk7 @ A @ (t)))) | (t @ A))),inference(simp,[status(thm)],[276])).
% 74.78/17.46 thf(7194,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk5 @ sk5))),inference(paramod_ordered,[status(thm)],[1307,359])).
% 74.78/17.46 thf(7195,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk5 @ sk5))),inference(simp,[status(thm)],[7194])).
% 74.78/17.46 thf(7261,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk5) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk5)),inference(simp,[status(thm)],[7195])).
% 74.78/17.46 thf(7292,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk5)),inference(simp,[status(thm)],[7261])).
% 74.78/17.46 thf(483,plain,((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (a @ (sk8 @ A @ a)))))),inference(pre_uni,[status(thm)],[433:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk2))]])).
% 74.78/17.46 thf(451,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (s))) | (s @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(s))]])).
% 74.78/17.46 thf(521,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (s))) | (s @ A))),inference(simp,[status(thm)],[451])).
% 74.78/17.46 thf(290,plain,(! [A:$i] : ((~ (a @ (sk7 @ A @ (a)))) | (a @ A))),inference(prim_subst,[status(thm)],[20:[bind(A, $thf(a))]])).
% 74.78/17.46 thf(299,plain,(! [A:$i] : ((~ (a @ (sk7 @ A @ (a)))) | (a @ A))),inference(simp,[status(thm)],[290])).
% 74.78/17.46 thf(4136,plain,((rel @ sk1 @ (sk7 @ sk1 @ (rel @ sk4))) | (a @ sk1) | (s @ sk2)),inference(pre_uni,[status(thm)],[4112:[bind(A, $thf(rel @ sk4)),bind(B, $thf(sk1))]])).
% 74.78/17.46 thf(1729,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (a @ sk2) | (s @ sk4) | ((A @ B) != (rel @ sk4 @ sk2)))),inference(paramod_ordered,[status(thm)],[19,1137])).
% 74.78/17.46 thf(1730,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (a @ sk2) | (s @ sk4) | ((A @ B) != (rel @ sk4 @ sk2)))),inference(simp,[status(thm)],[1729])).
% 74.78/17.46 thf(1748,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (rel @ A @ sk2)))) | (a @ sk2) | (s @ sk4)),inference(pre_uni,[status(thm)],[1730:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk2))),bind(B, $thf(sk4))]])).
% 74.78/17.46 thf(454,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (a))) | (a @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(a))]])).
% 74.78/17.46 thf(525,plain,(! [A:$i] : ((rel @ A @ (sk7 @ A @ (a))) | (a @ A))),inference(simp,[status(thm)],[454])).
% 74.78/17.46 thf(1447,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,371])).
% 74.78/17.46 thf(1448,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ sk5 @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[1447])).
% 74.78/17.46 thf(1481,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk5 != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[1448])).
% 74.78/17.46 thf(1495,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | (sk5 != sk4)),inference(simp,[status(thm)],[1481])).
% 74.78/17.46 thf(1509,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1495])).
% 74.78/17.46 thf(1510,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(simp,[status(thm)],[1509])).
% 74.78/17.46 thf(1516,plain,((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk5 != sk4)),inference(pre_uni,[status(thm)],[1510:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk5))]])).
% 74.78/17.46 thf(3390,plain,((~ (a @ (sk8 @ sk6 @ (a)))) | ~ (($true)) | ((rel @ (sk7 @ sk6 @ (t)) @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,622])).
% 74.78/17.46 thf(3391,plain,((~ (a @ (sk8 @ sk6 @ (a)))) | ((rel @ (sk7 @ sk6 @ (t)) @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[3390])).
% 74.78/17.46 thf(3432,plain,((~ (a @ (sk8 @ sk6 @ (a)))) | ((sk7 @ sk6 @ (t)) != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[3391])).
% 74.78/17.46 thf(3462,plain,((~ (a @ (sk8 @ sk6 @ (a)))) | ((sk7 @ sk6 @ (t)) != sk4)),inference(simp,[status(thm)],[3432])).
% 74.78/17.46 thf(1711,plain,(~ (($true)) | (a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk2) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[10,1137])).
% 74.78/17.46 thf(1712,plain,((a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk2) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[1711])).
% 74.78/17.46 thf(1750,plain,((a @ sk2) | (s @ sk4) | (sk4 != sk2) | (sk4 != sk2)),inference(simp,[status(thm)],[1712])).
% 74.78/17.46 thf(1763,plain,((a @ sk2) | (s @ sk4) | (sk4 != sk2)),inference(simp,[status(thm)],[1750])).
% 74.78/17.46 thf(967,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk2 @ sk5) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[10,343])).
% 74.78/17.46 thf(968,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk2 @ sk5) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[967])).
% 74.78/17.46 thf(1006,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk2 != sk2) | (sk5 != sk4)),inference(simp,[status(thm)],[968])).
% 74.78/17.46 thf(1023,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk5 != sk4)),inference(simp,[status(thm)],[1006])).
% 74.78/17.46 thf(1233,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk6 != sk4) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1114])).
% 74.78/17.46 thf(1234,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk6 != sk4) | ((A @ B) != (a @ (sk8 @ sk5 @ (a)))))),inference(simp,[status(thm)],[1233])).
% 74.78/17.46 thf(1240,plain,((rel @ sk5 @ (sk7 @ sk5 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk6 != sk4)),inference(pre_uni,[status(thm)],[1234:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk5))]])).
% 74.78/17.46 thf(1749,plain,((rel @ sk2 @ (sk7 @ sk2 @ (rel @ sk4))) | (a @ sk2) | (s @ sk4)),inference(pre_uni,[status(thm)],[1730:[bind(A, $thf(rel @ sk4)),bind(B, $thf(sk2))]])).
% 74.78/17.46 thf(11,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (a @ A) | (~ (rel @ A @ B)) | (rel @ B @ (sk3 @ B @ A)) | (~ (rel @ B @ C)) | (t @ C))),inference(cnfConj,[status(thm)],[6])).
% 74.78/17.46 thf(1159,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | ~ (($true)) | (s @ B) | ((rel @ sk5 @ sk6) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,16])).
% 74.78/17.46 thf(1160,plain,(! [B:$i,A:$i] : ((~ (rel @ sk4 @ A)) | (a @ A) | (s @ B) | ((rel @ sk5 @ sk6) != (rel @ A @ B)))),inference(simp,[status(thm)],[1159])).
% 74.78/17.46 thf(1161,plain,((~ (rel @ sk4 @ sk5)) | (a @ sk5) | (s @ sk6)),inference(pattern_uni,[status(thm)],[1160:[bind(A, $thf(sk5)),bind(B, $thf(sk6))]])).
% 74.78/17.46 thf(4762,plain,(~ (($true)) | ($false) | (s @ sk6)),inference(rewrite,[status(thm)],[1161,7,14])).
% 74.78/17.46 thf(4763,plain,((s @ sk6)),inference(simp,[status(thm)],[4762])).
% 74.78/17.46 thf(1275,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ~ (($true)) | ((rel @ sk5 @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,359])).
% 74.78/17.46 thf(1276,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | ((rel @ sk5 @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[1275])).
% 74.78/17.46 thf(1302,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[1276])).
% 74.78/17.46 thf(1321,plain,((~ (a @ (sk8 @ sk4 @ (a)))) | (sk5 != sk4)),inference(simp,[status(thm)],[1302])).
% 74.78/17.46 thf(1717,plain,(~ (($true)) | (a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk2))),inference(paramod_ordered,[status(thm)],[7,1137])).
% 74.78/17.46 thf(1718,plain,((a @ sk2) | (s @ sk4) | ((rel @ sk4 @ sk5) != (rel @ sk4 @ sk2))),inference(simp,[status(thm)],[1717])).
% 74.78/17.46 thf(1733,plain,((a @ sk2) | (s @ sk4) | (sk4 != sk4) | (sk5 != sk2)),inference(simp,[status(thm)],[1718])).
% 74.78/17.46 thf(1752,plain,((a @ sk2) | (s @ sk4) | (sk5 != sk2)),inference(simp,[status(thm)],[1733])).
% 74.78/17.46 thf(1764,plain,((s @ sk4) | (sk5 != sk2) | ~ (($true)) | ((a @ sk5) != (a @ sk2))),inference(paramod_ordered,[status(thm)],[1752,14])).
% 74.78/17.46 thf(1765,plain,((s @ sk4) | (sk5 != sk2) | ((a @ sk5) != (a @ sk2))),inference(simp,[status(thm)],[1764])).
% 74.78/17.46 thf(1820,plain,((s @ sk4) | (sk5 != sk2) | (sk5 != sk2)),inference(simp,[status(thm)],[1765])).
% 74.78/17.46 thf(1834,plain,((s @ sk4) | (sk5 != sk2)),inference(simp,[status(thm)],[1820])).
% 74.78/17.46 thf(10219,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (a @ sk4) | (s @ sk4) | ((A @ B) != (rel @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[19,1206])).
% 74.78/17.46 thf(10220,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (a @ sk4) | (s @ sk4) | ((A @ B) != (rel @ sk4 @ sk4)))),inference(simp,[status(thm)],[10219])).
% 74.78/17.46 thf(10268,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (rel @ A @ A)))) | (a @ sk4) | (s @ sk4)),inference(pre_uni,[status(thm)],[10220:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk4))]])).
% 74.78/17.46 thf(971,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) != (rel @ sk2 @ sk5))),inference(paramod_ordered,[status(thm)],[483,343])).
% 74.78/17.46 thf(972,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ sk2 @ (sk7 @ sk2 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) != (rel @ sk2 @ sk5))),inference(simp,[status(thm)],[971])).
% 74.78/17.46 thf(1013,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | (sk2 != sk2) | ((sk7 @ sk2 @ (^ [A:$i]: (a @ (sk8 @ A @ a)))) != sk5)),inference(simp,[status(thm)],[972])).
% 74.78/17.46 thf(1030,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((sk7 @ sk2 @ (^ [A:$i]: (a @ (sk8 @ A @ a)))) != sk5)),inference(simp,[status(thm)],[1013])).
% 74.78/17.46 thf(9790,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ~ (($true)) | ((rel @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) @ sk5) != (rel @ sk4 @ sk5))),inference(paramod_ordered,[status(thm)],[7,9658])).
% 74.78/17.46 thf(9791,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((rel @ (sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) @ sk5) != (rel @ sk4 @ sk5))),inference(simp,[status(thm)],[9790])).
% 74.78/17.46 thf(9855,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk4) | (sk5 != sk5)),inference(simp,[status(thm)],[9791])).
% 74.78/17.46 thf(9908,plain,((~ (a @ (sk8 @ sk5 @ (a)))) | ((sk7 @ sk5 @ (^ [A:$i]: (rel @ A @ A))) != sk4)),inference(simp,[status(thm)],[9855])).
% 74.78/17.46 thf(274,plain,(! [A:$i] : ((~ (prop_a @ (sk7 @ A @ (prop_a)))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[20:[bind(A, $thf(prop_a))]])).
% 74.78/17.46 thf(300,plain,(! [A:$i] : ((~ (prop_a @ (sk7 @ A @ (prop_a)))) | (prop_a @ A))),inference(simp,[status(thm)],[274])).
% 74.78/17.46 thf(47,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ~ (($true)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk8 @ F @ (E)))))),inference(paramod_ordered,[status(thm)],[26,26])).
% 74.78/17.46 thf(48,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk8 @ F @ (E)))))),inference(simp,[status(thm)],[47])).
% 74.78/17.46 thf(106,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk8 @ F @ (E)))))),inference(pre_uni,[status(thm)],[48:[]])).
% 74.78/17.46 thf(107,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((E @ H) | (~ (rel @ G @ H)) | (~ (rel @ F @ G)) | (~ (rel @ C @ D)) | (~ (rel @ B @ C)) | (~ (A @ (sk8 @ B @ (A)))) | ((A @ D) != (E @ (sk8 @ F @ (E)))))),inference(pre_uni,[status(thm)],[106:[]])).
% 74.78/17.46 thf(1049,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk1 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1023])).
% 74.78/17.46 thf(1050,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk1 @ (a)))))),inference(simp,[status(thm)],[1049])).
% 74.78/17.46 thf(1056,plain,((rel @ sk1 @ (sk7 @ sk1 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk5 != sk4)),inference(pre_uni,[status(thm)],[1050:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk1))]])).
% 74.78/17.46 thf(1345,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | ~ (($true)) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk4 @ (a)))))),inference(paramod_ordered,[status(thm)],[19,1321])).
% 74.78/17.46 thf(1346,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk7 @ B @ (A))) | (sk5 != sk4) | ((A @ B) != (a @ (sk8 @ sk4 @ (a)))))),inference(simp,[status(thm)],[1345])).
% 74.78/17.46 thf(1352,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (a @ (sk8 @ A @ a))))) | (sk5 != sk4)),inference(pre_uni,[status(thm)],[1346:[bind(A, $thf(^ [C:$i]: (a @ (sk8 @ C @ a)))),bind(B, $thf(sk4))]])).
% 74.78/17.46 thf(987,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk1 @ (a)))) | ~ (($true)) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk2 @ sk5)))),inference(paramod_ordered,[status(thm)],[531,343])).
% 74.78/17.46 thf(988,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk1 @ (a)))) | ((rel @ A @ (sk7 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk2 @ sk5)))),inference(simp,[status(thm)],[987])).
% 74.78/17.46 thf(999,plain,(! [A:$i] : ((~ (a @ (sk8 @ sk1 @ (a)))) | (A != sk2) | ((sk7 @ A @ (^ [B:$i]: (($false)))) != sk5))),inference(simp,[status(thm)],[988])).
% 74.78/17.46 thf(1019,plain,((~ (a @ (sk8 @ sk1 @ (a)))) | ((sk7 @ sk2 @ (^ [A:$i]: (($false)))) != sk5)),inference(simp,[status(thm)],[999])).
% 74.78/17.46 thf(49,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk8 @ F @ (E)))) | ~ (($true)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (rel @ F @ G)))),inference(paramod_ordered,[status(thm)],[26,26])).
% 74.78/17.46 thf(50,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk8 @ F @ (E)))) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (rel @ F @ G)))),inference(simp,[status(thm)],[49])).
% 74.78/17.46 thf(83,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ ((sk8 @ F @ (E)) = (sk8 @ F @ ((=) @ $i @ (sk8 @ F @ E))))) | (~ (rel @ G @ H)) | ((sk8 @ F @ (E)) = H) | ((A @ D) != (rel @ F @ G)))),inference(replace_leibeq,[status(thm)],[50:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf((=) @ $i @ (sk8 @ F @ E)))]])).
% 74.78/17.46 thf(90,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : (((sk8 @ F @ (E)) != (sk8 @ F @ ((=) @ $i @ (sk8 @ F @ E)))) | ((sk8 @ F @ (E)) = H) | (~ (A @ (sk8 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ G @ H)) | ((A @ D) != (rel @ F @ G)))),inference(lifteq,[status(thm)],[83])).
% 74.78/17.46 thf(5436,plain,((rel @ sk4 @ (sk7 @ sk4 @ (^ [A:$i]: (rel @ A @ sk4)))) | (a @ sk4) | (s @ sk5)),inference(pre_uni,[status(thm)],[5407:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk4))),bind(B, $thf(sk4))]])).
% 74.78/17.46 thf(18125,plain,(($false)),inference(e,[status(thm)],[348,9658,526,1322,4262,88,481,1005,5,1142,1041,1486,10,9644,1137,1001,25,1254,14,1313,20,1319,46,93,1494,89,1104,1119,11723,1206,3303,5438,1338,1470,1021,28,1017,9,1755,1118,11019,622,1114,997,13,1002,4135,371,343,1167,5451,17,7639,22,1503,12,382,996,7,1307,303,1122,7292,483,521,299,490,4136,531,1748,525,1516,3462,16,585,1763,359,1023,1240,1749,11,4763,1321,1834,26,23,10268,8,1030,9908,300,36,146,19,107,1314,1495,506,1056,1352,1019,90,5436])).
% 74.78/17.46 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 74.78/17.46 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------