%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV432^2 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n013.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:52 AM UTC 2026
% Result : Theorem 80.90s 16.94s
% Output : Refutation 80.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV432^2 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.22 % Computer : n013.cluster.edu
% 0.11/0.22 % Model : x86_64 x86_64
% 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.22 % Memory : 8046.5625MB
% 0.11/0.22 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Tue Sep 29 16:02:21 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.75/0.61 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.08/0.75 % [INFO] Parsing done (146ms).
% 1.08/0.76 % [INFO] Running in sequential loop mode.
% 1.81/0.96 % [INFO] eprover registered as external prover.
% 1.81/0.97 % [INFO] Scanning for conjecture ...
% 2.16/1.04 % [INFO] Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ...
% 2.16/1.06 % [INFO] Axiom selection finished. Selected 2 axioms (removed 0 axioms).
% 2.16/1.06 % [INFO] Problem is higher-order (TPTP THF).
% 2.16/1.06 % [INFO] Type checking passed.
% 2.16/1.07 % [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 ...
% 80.90/16.93 % External prover 'e' found a proof!
% 80.90/16.94 % [INFO] Killing All external provers ...
% 80.90/16.94 % Time passed: 16578ms (effective reasoning time: 16172ms)
% 80.90/16.94 % 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)>
% 80.90/16.94 % Axioms used in derivation (2): refl_axiom, trans_axiom
% 80.90/16.94 % No. of inferences in proof: 217
% 80.90/16.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 16578 ms resp. 16172 ms w/o parsing
% 80.90/17.02 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 80.90/17.02 thf(individuals_type, type, individuals: $tType).
% 80.90/17.02 thf(prop_a_decl, type, prop_a: ($i > $o)).
% 80.90/17.02 thf(prop_b_decl, type, prop_b: ($i > $o)).
% 80.90/17.02 thf(prop_c_decl, type, prop_c: ($i > $o)).
% 80.90/17.02 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 80.90/17.02 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 80.90/17.02 thf(rel_decl, type, rel: ($i > ($i > $o))).
% 80.90/17.02 thf(icl_princ_decl, type, icl_princ: (($i > $o) > ($i > $o))).
% 80.90/17.02 thf(icl_impl_decl, type, icl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(icl_says_decl, type, icl_says: (($i > $o) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(iclval_decl, type, iclval: (($i > $o) > $o)).
% 80.90/17.02 thf(icl_impl_princ_decl, type, icl_impl_princ: (($i > $o) > (($i > $o) > ($i > $o)))).
% 80.90/17.02 thf(a_decl, type, a: ($i > $o)).
% 80.90/17.02 thf(b_decl, type, b: ($i > $o)).
% 80.90/17.02 thf(sk1_decl, type, sk1: $i).
% 80.90/17.02 thf(sk2_decl, type, sk2: $i).
% 80.90/17.02 thf(sk3_decl, type, sk3: $i).
% 80.90/17.02 thf(sk4_decl, type, sk4: ($i > (($i > $o) > $i))).
% 80.90/17.02 thf(sk5_decl, type, sk5: ($i > (($i > $o) > $i))).
% 80.90/17.02 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 80.90/17.02 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 80.90/17.02 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 80.90/17.02 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 80.90/17.02 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 80.90/17.02 thf(icl_princ_def, definition, icl_princ = (^ [A:($i > $o)]: (A)) ).
% 80.90/17.02 thf(icl_impl_def, definition, icl_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 80.90/17.02 thf(icl_says_def, definition, icl_says = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mor @ A @ B))) ).
% 80.90/17.02 thf(iclval_def, definition, iclval = (mvalid) ).
% 80.90/17.02 thf(icl_impl_princ_def, definition, icl_impl_princ = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 80.90/17.02 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => ((b @ C) | ! [D:$i]: ((rel @ C @ D) => (~ (a @ D) | (b @ D)))))) | ! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (b @ C))))))) ).
% 80.90/17.02 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ ((rel @ sk1 @ A) => (~ (! [B:$i]: ((rel @ A @ B) => ((b @ B) | ! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (b @ C)))))) | ! [B:$i]: ((rel @ A @ B) => (~ (a @ B) | (b @ B)))))) ).
% 80.90/17.02 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ ((rel @ sk2 @ A) => (~ (a @ A) | (b @ A)))) ).
% 80.90/17.02 thf(sk4_def, definition, sk4 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 80.90/17.02 thf(sk5_def, definition, sk5 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 80.90/17.02 thf(1,conjecture,((iclval @ (icl_impl @ (icl_says @ (icl_princ @ b) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b))) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',handoff)).
% 80.90/17.02 thf(2,negated_conjecture,((~ (iclval @ (icl_impl @ (icl_says @ (icl_princ @ b) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b))) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b)))))),inference(neg_conjecture,[status(cth)],[1])).
% 80.90/17.02 thf(5,plain,((~ (! [A:$i,B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => ((b @ C) | ! [D:$i]: ((rel @ C @ D) => (~ (a @ D) | (b @ D)))))) | ! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (b @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 80.90/17.02 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',refl_axiom)).
% 80.90/17.02 thf(12,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 80.90/17.02 thf(13,plain,(! [B:$i,A:($i > $o)] : ((((rel @ B @ (sk4 @ B @ (A))) | (A @ B)) & (~ (A @ (sk4 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[12])).
% 80.90/17.02 thf(14,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[13])).
% 80.90/17.02 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ (mbox @ rel @ (mbox @ rel @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_axiom)).
% 80.90/17.02 thf(18,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])).
% 80.90/17.02 thf(19,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((rel @ B @ (sk5 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D)) & (~ (A @ (sk5 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[18])).
% 80.90/17.02 thf(21,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[19])).
% 80.90/17.02 thf(6,plain,(! [B:$i,A:$i] : (((rel @ sk1 @ sk2) & (~ (rel @ sk2 @ A) | (b @ A) | ~ (rel @ A @ B) | ~ (a @ B) | (b @ B)) & (rel @ sk2 @ sk3) & (a @ sk3) & ~ (b @ sk3)))),inference(cnf,[status(esa)],[5])).
% 80.90/17.02 thf(9,plain,((~ (b @ sk3))),inference(cnfConj,[status(thm)],[6])).
% 80.90/17.02 thf(30,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ~ (($true)) | ((A @ D) != (b @ sk3)))),inference(paramod_ordered,[status(thm)],[21,9])).
% 80.90/17.02 thf(31,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((A @ D) != (b @ sk3)))),inference(simp,[status(thm)],[30])).
% 80.90/17.02 thf(104,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk3)))),inference(pre_uni,[status(thm)],[31:[bind(A, $thf(b)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk3))]])).
% 80.90/17.02 thf(130,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk3)))),inference(simp,[status(thm)],[104])).
% 80.90/17.02 thf(469,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ A @ B)) | ((rel @ B @ sk3) != (rel @ A @ B)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[130])).
% 80.90/17.02 thf(482,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (rel @ sk3 @ sk3))),inference(pattern_uni,[status(thm)],[469:[bind(A, $thf(sk3)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(882,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(paramod_ordered,[status(thm)],[14,482])).
% 80.90/17.03 thf(883,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (b @ (sk5 @ sk3 @ (b)))) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(simp,[status(thm)],[882])).
% 80.90/17.03 thf(912,plain,((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3)))) | (~ (b @ (sk5 @ sk3 @ (b))))),inference(pre_uni,[status(thm)],[883:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk3))),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(15642,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3)))) != (rel @ sk3 @ sk3))),inference(paramod_ordered,[status(thm)],[912,482])).
% 80.90/17.03 thf(15643,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3)))) != (rel @ sk3 @ sk3))),inference(simp,[status(thm)],[15642])).
% 80.90/17.03 thf(15705,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (sk3 != sk3) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3))) != sk3)),inference(simp,[status(thm)],[15643])).
% 80.90/17.03 thf(15776,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3))) != sk3)),inference(simp,[status(thm)],[15705])).
% 80.90/17.03 thf(64,plain,(! [C:$i,B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (b @ C))),inference(prim_subst,[status(thm)],[21:[bind(A, $thf(b))]])).
% 80.90/17.03 thf(106,plain,(! [C:$i,B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (b @ C))),inference(simp,[status(thm)],[64])).
% 80.90/17.03 thf(7,plain,((rel @ sk2 @ sk3)),inference(cnfConj,[status(thm)],[6])).
% 80.90/17.03 thf(10,plain,(! [B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (b @ A) | (~ (rel @ A @ B)) | (~ (a @ B)) | (b @ B))),inference(cnfConj,[status(thm)],[6])).
% 80.90/17.03 thf(289,plain,(! [B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (b @ A) | ~ (($true)) | (~ (a @ B)) | (b @ B) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[7,10])).
% 80.90/17.03 thf(290,plain,(! [B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (b @ A) | (~ (a @ B)) | (b @ B) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(simp,[status(thm)],[289])).
% 80.90/17.03 thf(291,plain,((~ (rel @ sk2 @ sk2)) | (b @ sk2) | (~ (a @ sk3)) | (b @ sk3)),inference(pattern_uni,[status(thm)],[290:[bind(A, $thf(sk2)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(8,plain,((a @ sk3)),inference(cnfConj,[status(thm)],[6])).
% 80.90/17.03 thf(2868,plain,((~ (rel @ sk2 @ sk2)) | (b @ sk2) | ~ (($true)) | ($false)),inference(rewrite,[status(thm)],[291,8,9])).
% 80.90/17.03 thf(2869,plain,((~ (rel @ sk2 @ sk2)) | (b @ sk2)),inference(simp,[status(thm)],[2868])).
% 80.90/17.03 thf(2888,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | (b @ sk2) | ((A @ B) != (rel @ sk2 @ sk2)))),inference(paramod_ordered,[status(thm)],[14,2869])).
% 80.90/17.03 thf(2889,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (b @ sk2) | ((A @ B) != (rel @ sk2 @ sk2)))),inference(simp,[status(thm)],[2888])).
% 80.90/17.03 thf(2918,plain,((rel @ sk2 @ (sk4 @ sk2 @ (rel @ sk2))) | (b @ sk2)),inference(pre_uni,[status(thm)],[2889:[bind(A, $thf(rel @ sk2)),bind(B, $thf(sk2))]])).
% 80.90/17.03 thf(15,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk4 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[13])).
% 80.90/17.03 thf(4588,plain,(! [B:$i,A:($i > $o)] : ((b @ sk2) | ~ (($true)) | (A @ B) | ((rel @ sk2 @ (sk4 @ sk2 @ (rel @ sk2))) != (A @ (sk4 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[2918,15])).
% 80.90/17.03 thf(4589,plain,(! [B:$i,A:($i > $o)] : ((b @ sk2) | (A @ B) | ((rel @ sk2 @ (sk4 @ sk2 @ (rel @ sk2))) != (A @ (sk4 @ B @ (A)))))),inference(simp,[status(thm)],[4588])).
% 80.90/17.03 thf(4604,plain,((b @ sk2) | (rel @ sk2 @ sk2)),inference(pre_uni,[status(thm)],[4589:[bind(A, $thf(rel @ sk2)),bind(B, $thf(sk2))]])).
% 80.90/17.03 thf(4636,plain,((b @ sk2) | ~ (($true)) | (b @ sk2) | ((rel @ sk2 @ sk2) != (rel @ sk2 @ sk2))),inference(paramod_ordered,[status(thm)],[4604,2869])).
% 80.90/17.03 thf(4637,plain,((b @ sk2) | ((rel @ sk2 @ sk2) != (rel @ sk2 @ sk2))),inference(simp,[status(thm)],[4636])).
% 80.90/17.03 thf(4638,plain,((b @ sk2)),inference(pattern_uni,[status(thm)],[4637:[]])).
% 80.90/17.03 thf(15842,plain,(~ (($true)) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,15776])).
% 80.90/17.03 thf(15843,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[15842])).
% 80.90/17.03 thf(15873,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ sk3))) != sk3) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[15843])).
% 80.90/17.03 thf(160,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | ((A @ B) != (b @ sk3)))),inference(paramod_ordered,[status(thm)],[14,9])).
% 80.90/17.03 thf(161,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ((A @ B) != (b @ sk3)))),inference(simp,[status(thm)],[160])).
% 80.90/17.03 thf(189,plain,((rel @ sk3 @ (sk4 @ sk3 @ (b)))),inference(pre_uni,[status(thm)],[161:[bind(A, $thf(b)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(868,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ sk3 @ (sk4 @ sk3 @ (b))) != (rel @ sk3 @ sk3))),inference(paramod_ordered,[status(thm)],[189,482])).
% 80.90/17.03 thf(869,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ sk3 @ (sk4 @ sk3 @ (b))) != (rel @ sk3 @ sk3))),inference(simp,[status(thm)],[868])).
% 80.90/17.03 thf(908,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (sk3 != sk3) | ((sk4 @ sk3 @ (b)) != sk3)),inference(simp,[status(thm)],[869])).
% 80.90/17.03 thf(929,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (b)) != sk3)),inference(simp,[status(thm)],[908])).
% 80.90/17.03 thf(4906,plain,(~ (($true)) | ((sk4 @ sk3 @ (b)) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,929])).
% 80.90/17.03 thf(4907,plain,(((sk4 @ sk3 @ (b)) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4906])).
% 80.90/17.03 thf(4934,plain,(((sk4 @ sk3 @ (b)) != sk3) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[4907])).
% 80.90/17.03 thf(170,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (b))) | (b @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(b))]])).
% 80.90/17.03 thf(204,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (b))) | (b @ A))),inference(simp,[status(thm)],[170])).
% 80.90/17.03 thf(914,plain,((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A)))) | (~ (b @ (sk5 @ sk3 @ (b))))),inference(pre_uni,[status(thm)],[883:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(8484,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk3 @ sk3))),inference(paramod_ordered,[status(thm)],[914,482])).
% 80.90/17.03 thf(8485,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A)))) != (rel @ sk3 @ sk3))),inference(simp,[status(thm)],[8484])).
% 80.90/17.03 thf(8552,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (sk3 != sk3) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk3)),inference(simp,[status(thm)],[8485])).
% 80.90/17.03 thf(8612,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk3)),inference(simp,[status(thm)],[8552])).
% 80.90/17.03 thf(11,plain,((rel @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[6])).
% 80.90/17.03 thf(443,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | ~ (($true)) | (~ (rel @ B @ sk3)) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[7,130])).
% 80.90/17.03 thf(444,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ B @ sk3)) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(simp,[status(thm)],[443])).
% 80.90/17.03 thf(445,plain,((~ (b @ (sk5 @ sk2 @ (b)))) | (~ (rel @ sk3 @ sk3))),inference(pattern_uni,[status(thm)],[444:[bind(A, $thf(sk2)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(514,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (b @ (sk5 @ sk2 @ (b)))) | ~ (($true)) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(paramod_ordered,[status(thm)],[14,445])).
% 80.90/17.03 thf(515,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (b @ (sk5 @ sk2 @ (b)))) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(simp,[status(thm)],[514])).
% 80.90/17.03 thf(542,plain,((rel @ sk3 @ (sk4 @ sk3 @ (rel @ sk3))) | (~ (b @ (sk5 @ sk2 @ (b))))),inference(pre_uni,[status(thm)],[515:[bind(A, $thf(rel @ sk3)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(12493,plain,(! [B:$i,A:($i > $o)] : ((~ (b @ (sk5 @ sk2 @ (b)))) | ~ (($true)) | (A @ B) | ((rel @ sk3 @ (sk4 @ sk3 @ (rel @ sk3))) != (A @ (sk4 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[542,15])).
% 80.90/17.03 thf(12494,plain,(! [B:$i,A:($i > $o)] : ((~ (b @ (sk5 @ sk2 @ (b)))) | (A @ B) | ((rel @ sk3 @ (sk4 @ sk3 @ (rel @ sk3))) != (A @ (sk4 @ B @ (A)))))),inference(simp,[status(thm)],[12493])).
% 80.90/17.03 thf(12532,plain,((~ (b @ (sk5 @ sk2 @ (b)))) | (rel @ sk3 @ sk3)),inference(pre_uni,[status(thm)],[12494:[bind(A, $thf(rel @ sk3)),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(12720,plain,((~ (b @ (sk5 @ sk2 @ (b)))) | (~ (b @ (sk5 @ sk2 @ (b)))) | ~ (($true)) | ((rel @ sk3 @ sk3) != (rel @ sk3 @ sk3))),inference(paramod_ordered,[status(thm)],[12532,445])).
% 80.90/17.03 thf(12721,plain,((~ (b @ (sk5 @ sk2 @ (b)))) | ((rel @ sk3 @ sk3) != (rel @ sk3 @ sk3))),inference(simp,[status(thm)],[12720])).
% 80.90/17.03 thf(12722,plain,((~ (b @ (sk5 @ sk2 @ (b))))),inference(pattern_uni,[status(thm)],[12721:[]])).
% 80.90/17.03 thf(12939,plain,(~ (($true)) | ((b @ (sk5 @ sk2 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,12722])).
% 80.90/17.03 thf(12940,plain,(((b @ (sk5 @ sk2 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[12939])).
% 80.90/17.03 thf(12972,plain,(((sk5 @ sk2 @ (b)) != sk2)),inference(simp,[status(thm)],[12940])).
% 80.90/17.03 thf(66,plain,(! [C:$i,B:$i,A:$i] : ((~ (prop_c @ (sk5 @ A @ (prop_c)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (prop_c @ C))),inference(prim_subst,[status(thm)],[21:[bind(A, $thf(prop_c))]])).
% 80.90/17.03 thf(107,plain,(! [C:$i,B:$i,A:$i] : ((~ (prop_c @ (sk5 @ A @ (prop_c)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (prop_c @ C))),inference(simp,[status(thm)],[66])).
% 80.90/17.03 thf(8646,plain,(~ (($true)) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,8612])).
% 80.90/17.03 thf(8647,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[8646])).
% 80.90/17.03 thf(8663,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk3) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[8647])).
% 80.90/17.03 thf(26,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk5 @ F @ (E)))) | ~ (($true)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (rel @ F @ G)))),inference(paramod_ordered,[status(thm)],[21,21])).
% 80.90/17.03 thf(27,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk5 @ F @ (E)))) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (rel @ F @ G)))),inference(simp,[status(thm)],[26])).
% 80.90/17.03 thf(75,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ ((sk5 @ F @ (E)) = (sk5 @ F @ ((=) @ $i @ (sk5 @ F @ E))))) | (~ (rel @ G @ H)) | ((sk5 @ F @ (E)) = H) | ((A @ D) != (rel @ F @ G)))),inference(replace_leibeq,[status(thm)],[27:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf((=) @ $i @ (sk5 @ F @ E)))]])).
% 80.90/17.03 thf(88,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : (((sk5 @ F @ (E)) != (sk5 @ F @ ((=) @ $i @ (sk5 @ F @ E)))) | ((sk5 @ F @ (E)) = H) | (~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ G @ H)) | ((A @ D) != (rel @ F @ G)))),inference(lifteq,[status(thm)],[75])).
% 80.90/17.03 thf(306,plain,(! [B:$i,A:$i] : ((~ (rel @ sk2 @ A)) | (b @ A) | (~ (a @ B)) | (b @ B) | ((rel @ A @ B) != (rel @ sk2 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[10])).
% 80.90/17.03 thf(316,plain,((~ (rel @ sk2 @ sk2)) | (b @ sk2) | (~ (a @ sk2)) | (b @ sk2)),inference(pattern_uni,[status(thm)],[306:[bind(A, $thf(sk2)),bind(B, $thf(sk2))]])).
% 80.90/17.03 thf(332,plain,((~ (rel @ sk2 @ sk2)) | (b @ sk2) | (~ (a @ sk2))),inference(simp,[status(thm)],[316])).
% 80.90/17.03 thf(637,plain,(~ (($true)) | (b @ sk2) | (~ (a @ sk2)) | ((rel @ sk2 @ sk3) != (rel @ sk2 @ sk2))),inference(paramod_ordered,[status(thm)],[7,332])).
% 80.90/17.03 thf(638,plain,((b @ sk2) | (~ (a @ sk2)) | ((rel @ sk2 @ sk3) != (rel @ sk2 @ sk2))),inference(simp,[status(thm)],[637])).
% 80.90/17.03 thf(657,plain,((b @ sk2) | (~ (a @ sk2)) | (sk2 != sk2) | (sk3 != sk2)),inference(simp,[status(thm)],[638])).
% 80.90/17.03 thf(678,plain,((b @ sk2) | (~ (a @ sk2)) | (sk3 != sk2)),inference(simp,[status(thm)],[657])).
% 80.90/17.03 thf(1026,plain,((b @ sk2) | ~ (($true)) | (sk3 != sk2) | ((a @ sk3) != (a @ sk2))),inference(paramod_ordered,[status(thm)],[8,678])).
% 80.90/17.03 thf(1027,plain,((b @ sk2) | (sk3 != sk2) | ((a @ sk3) != (a @ sk2))),inference(simp,[status(thm)],[1026])).
% 80.90/17.03 thf(1032,plain,((b @ sk2) | (sk3 != sk2) | (sk3 != sk2)),inference(simp,[status(thm)],[1027])).
% 80.90/17.03 thf(1044,plain,((b @ sk2) | (sk3 != sk2)),inference(simp,[status(thm)],[1032])).
% 80.90/17.03 thf(1052,plain,((sk3 != sk2) | ~ (($true)) | ((b @ sk3) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[1044,9])).
% 80.90/17.03 thf(1053,plain,((sk3 != sk2) | ((b @ sk3) != (b @ sk2))),inference(simp,[status(thm)],[1052])).
% 80.90/17.03 thf(1071,plain,((sk3 != sk2) | (sk3 != sk2)),inference(simp,[status(thm)],[1053])).
% 80.90/17.03 thf(1078,plain,((sk3 != sk2)),inference(simp,[status(thm)],[1071])).
% 80.90/17.03 thf(449,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | ~ (($true)) | (~ (rel @ B @ sk3)) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[11,130])).
% 80.90/17.03 thf(450,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ B @ sk3)) | ((rel @ sk1 @ sk2) != (rel @ A @ B)))),inference(simp,[status(thm)],[449])).
% 80.90/17.03 thf(451,plain,((~ (b @ (sk5 @ sk1 @ (b)))) | (~ (rel @ sk2 @ sk3))),inference(pattern_uni,[status(thm)],[450:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 80.90/17.03 thf(779,plain,((~ (b @ (sk5 @ sk1 @ (b)))) | ~ (($true))),inference(rewrite,[status(thm)],[451,7])).
% 80.90/17.03 thf(780,plain,((~ (b @ (sk5 @ sk1 @ (b))))),inference(simp,[status(thm)],[779])).
% 80.90/17.03 thf(781,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | ((A @ B) != (b @ (sk5 @ sk1 @ (b)))))),inference(paramod_ordered,[status(thm)],[14,780])).
% 80.90/17.03 thf(782,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ((A @ B) != (b @ (sk5 @ sk1 @ (b)))))),inference(simp,[status(thm)],[781])).
% 80.90/17.03 thf(785,plain,((rel @ (sk5 @ sk1 @ (b)) @ (sk4 @ (sk5 @ sk1 @ (b)) @ (b)))),inference(pre_uni,[status(thm)],[782:[bind(A, $thf(b)),bind(B, $thf(sk5 @ sk1 @ (b)))]])).
% 80.90/17.03 thf(69,plain,(! [D:($i > $o),C:$i,B:$i,A:$i] : ((~ (~ (D @ (sk5 @ A @ (^ [E:$i]: ~ (D @ E)))))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (D @ C)))),inference(prim_subst,[status(thm)],[21:[bind(A, $thf(^ [F:$i]: ~ (E @ F)))]])).
% 80.90/17.03 thf(109,plain,(! [D:($i > $o),C:$i,B:$i,A:$i] : ((D @ (sk5 @ A @ (^ [E:$i]: ~ (D @ E)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (D @ C)))),inference(cnf,[status(esa)],[69])).
% 80.90/17.03 thf(110,plain,(! [D:($i > $o),C:$i,B:$i,A:$i] : ((D @ (sk5 @ A @ (^ [E:$i]: ~ (D @ E)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (~ (D @ C)))),inference(simp,[status(thm)],[109])).
% 80.90/17.03 thf(12941,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | ((A @ B) != (b @ (sk5 @ sk2 @ (b)))))),inference(paramod_ordered,[status(thm)],[14,12722])).
% 80.90/17.03 thf(12942,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ((A @ B) != (b @ (sk5 @ sk2 @ (b)))))),inference(simp,[status(thm)],[12941])).
% 80.90/17.03 thf(12961,plain,((rel @ sk2 @ (sk4 @ sk2 @ (^ [A:$i]: (b @ (sk5 @ A @ b)))))),inference(pre_uni,[status(thm)],[12942:[bind(A, $thf(^ [C:$i]: (b @ (sk5 @ C @ b)))),bind(B, $thf(sk2))]])).
% 80.90/17.03 thf(20,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[19])).
% 80.90/17.03 thf(427,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | ~ (($true)) | (~ (rel @ B @ sk3)) | ((rel @ sk3 @ (sk4 @ sk3 @ (b))) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[189,130])).
% 80.90/17.03 thf(428,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ B @ sk3)) | ((rel @ sk3 @ (sk4 @ sk3 @ (b))) != (rel @ A @ B)))),inference(simp,[status(thm)],[427])).
% 80.90/17.03 thf(429,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (rel @ (sk4 @ sk3 @ (b)) @ sk3))),inference(pattern_uni,[status(thm)],[428:[bind(A, $thf(sk3)),bind(B, $thf(sk4 @ sk3 @ (b)))]])).
% 80.90/17.03 thf(2008,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ (sk4 @ sk3 @ (b)) @ sk3) != (rel @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[7,429])).
% 80.90/17.03 thf(2009,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ (sk4 @ sk3 @ (b)) @ sk3) != (rel @ sk2 @ sk3))),inference(simp,[status(thm)],[2008])).
% 80.90/17.03 thf(2054,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (b)) != sk2) | (sk3 != sk3)),inference(simp,[status(thm)],[2009])).
% 80.90/17.03 thf(2058,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[2054])).
% 80.90/17.03 thf(4900,plain,(~ (($true)) | ((b @ (sk5 @ sk1 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,780])).
% 80.90/17.03 thf(4901,plain,(((b @ (sk5 @ sk1 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4900])).
% 80.90/17.03 thf(4935,plain,(((sk5 @ sk1 @ (b)) != sk2)),inference(simp,[status(thm)],[4901])).
% 80.90/17.03 thf(188,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (b @ sk3)))))),inference(pre_uni,[status(thm)],[161:[bind(A, $thf(^ [C:$i]: (b @ sk3))),bind(B, $thf(B))]])).
% 80.90/17.03 thf(217,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (b @ sk3)))))),inference(simp,[status(thm)],[188])).
% 80.90/17.03 thf(235,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (($false))))))),inference(rewrite,[status(thm)],[217,9])).
% 80.90/17.03 thf(892,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk3 @ sk3)))),inference(paramod_ordered,[status(thm)],[235,482])).
% 80.90/17.03 thf(893,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk3 @ sk3)))),inference(simp,[status(thm)],[892])).
% 80.90/17.03 thf(898,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | (A != sk3) | ((sk4 @ A @ (^ [B:$i]: (($false)))) != sk3))),inference(simp,[status(thm)],[893])).
% 80.90/17.03 thf(923,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (^ [A:$i]: (($false)))) != sk3)),inference(simp,[status(thm)],[898])).
% 80.90/17.03 thf(4912,plain,(~ (($true)) | ((sk4 @ sk3 @ (^ [A:$i]: (($false)))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,923])).
% 80.90/17.03 thf(4913,plain,(((sk4 @ sk3 @ (^ [A:$i]: (($false)))) != sk3) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4912])).
% 80.90/17.03 thf(4924,plain,(((sk4 @ sk3 @ (^ [A:$i]: (($false)))) != sk3) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[4913])).
% 80.90/17.03 thf(8427,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (rel @ sk3 @ (sk4 @ sk3 @ (^ [C:$i]: (rel @ C @ C)))) | ~ (($true)) | ((A @ B) != (b @ (sk5 @ sk3 @ (b)))))),inference(paramod_ordered,[status(thm)],[14,914])).
% 80.90/17.03 thf(8428,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (rel @ sk3 @ (sk4 @ sk3 @ (^ [C:$i]: (rel @ C @ C)))) | ((A @ B) != (b @ (sk5 @ sk3 @ (b)))))),inference(simp,[status(thm)],[8427])).
% 80.90/17.03 thf(8554,plain,((rel @ (sk5 @ sk3 @ (b)) @ (sk4 @ (sk5 @ sk3 @ (b)) @ (b))) | (rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))))),inference(pre_uni,[status(thm)],[8428:[bind(A, $thf(b)),bind(B, $thf(sk5 @ sk3 @ (b)))]])).
% 80.90/17.03 thf(4886,plain,(~ (($true)) | (~ (rel @ (sk4 @ sk3 @ (b)) @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,429])).
% 80.90/17.03 thf(4887,plain,((~ (rel @ (sk4 @ sk3 @ (b)) @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4886])).
% 80.90/17.03 thf(4920,plain,((~ (rel @ (sk4 @ sk3 @ (b)) @ sk3)) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[4887])).
% 80.90/17.03 thf(53,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((A @ D) != (~ (A @ (sk5 @ B @ (A))))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[21])).
% 80.90/17.03 thf(92,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((A @ D) != (~ (A @ (sk5 @ B @ (A))))))),inference(simp,[status(thm)],[53])).
% 80.90/17.03 thf(8479,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (b @ (sk5 @ A @ (b)))) | ~ (($true)) | (~ (rel @ B @ sk3)) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [C:$i]: (rel @ C @ C)))) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[914,130])).
% 80.90/17.03 thf(8480,plain,(! [B:$i,A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (b @ (sk5 @ A @ (b)))) | (~ (rel @ B @ sk3)) | ((rel @ sk3 @ (sk4 @ sk3 @ (^ [C:$i]: (rel @ C @ C)))) != (rel @ A @ B)))),inference(simp,[status(thm)],[8479])).
% 80.90/17.03 thf(8481,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (b @ (sk5 @ sk3 @ (b)))) | (~ (rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3))),inference(pattern_uni,[status(thm)],[8480:[bind(A, $thf(sk3)),bind(B, $thf(sk4 @ sk3 @ (^ [C:$i]: (rel @ C @ C))))]])).
% 80.90/17.03 thf(8577,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | (~ (rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3))),inference(simp,[status(thm)],[8481])).
% 80.90/17.03 thf(12959,plain,((rel @ (sk5 @ sk2 @ (b)) @ (sk4 @ (sk5 @ sk2 @ (b)) @ (b)))),inference(pre_uni,[status(thm)],[12942:[bind(A, $thf(b)),bind(B, $thf(sk5 @ sk2 @ (b)))]])).
% 80.90/17.03 thf(8921,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3) != (rel @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[7,8577])).
% 80.90/17.03 thf(8922,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3) != (rel @ sk2 @ sk3))),inference(simp,[status(thm)],[8921])).
% 80.90/17.03 thf(8965,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk2) | (sk3 != sk3)),inference(simp,[status(thm)],[8922])).
% 80.90/17.03 thf(9016,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk2)),inference(simp,[status(thm)],[8965])).
% 80.90/17.03 thf(4877,plain,(~ (($true)) | ((sk4 @ sk3 @ (b)) != sk2) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,2058])).
% 80.90/17.03 thf(4878,plain,(((sk4 @ sk3 @ (b)) != sk2) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4877])).
% 80.90/17.03 thf(4930,plain,(((sk4 @ sk3 @ (b)) != sk2) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[4878])).
% 80.90/17.03 thf(880,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | (~ (rel @ sk3 @ sk3)) | ((A @ B) != (b @ (sk5 @ sk3 @ (b)))))),inference(paramod_ordered,[status(thm)],[14,482])).
% 80.90/17.03 thf(881,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | (~ (rel @ sk3 @ sk3)) | ((A @ B) != (b @ (sk5 @ sk3 @ (b)))))),inference(simp,[status(thm)],[880])).
% 80.90/17.03 thf(906,plain,((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (b @ (sk5 @ A @ b))))) | (~ (rel @ sk3 @ sk3))),inference(pre_uni,[status(thm)],[881:[bind(A, $thf(^ [C:$i]: (b @ (sk5 @ C @ b)))),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(16,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk4 @ B @ (A)) = (sk4 @ B @ ((=) @ $i @ (sk4 @ B @ A))))) | ((sk4 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[15:[bind(A, $thf((=) @ $i @ (sk4 @ B @ A)))]])).
% 80.90/17.03 thf(17,plain,(! [B:$i,A:($i > $o)] : (((sk4 @ B @ (A)) != (sk4 @ B @ ((=) @ $i @ (sk4 @ B @ A)))) | ((sk4 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[16])).
% 80.90/17.03 thf(787,plain,((rel @ sk1 @ (sk4 @ sk1 @ (^ [A:$i]: (b @ (sk5 @ A @ b)))))),inference(pre_uni,[status(thm)],[782:[bind(A, $thf(^ [C:$i]: (b @ (sk5 @ C @ b)))),bind(B, $thf(sk1))]])).
% 80.90/17.03 thf(28,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk5 @ F @ (E)))) | (~ (rel @ F @ G)) | ~ (($true)) | (E @ H) | ((A @ D) != (rel @ G @ H)))),inference(paramod_ordered,[status(thm)],[21,21])).
% 80.90/17.03 thf(29,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (E @ (sk5 @ F @ (E)))) | (~ (rel @ F @ G)) | (E @ H) | ((A @ D) != (rel @ G @ H)))),inference(simp,[status(thm)],[28])).
% 80.90/17.03 thf(73,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ ((sk5 @ F @ (E)) = (sk5 @ F @ ((=) @ $i @ (sk5 @ F @ E))))) | (~ (rel @ F @ G)) | ((sk5 @ F @ (E)) = H) | ((A @ D) != (rel @ G @ H)))),inference(replace_leibeq,[status(thm)],[29:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf((=) @ $i @ (sk5 @ F @ E)))]])).
% 80.90/17.03 thf(81,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : (((sk5 @ F @ (E)) != (sk5 @ F @ ((=) @ $i @ (sk5 @ F @ E)))) | ((sk5 @ F @ (E)) = H) | (~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | ((A @ D) != (rel @ G @ H)))),inference(lifteq,[status(thm)],[73])).
% 80.90/17.03 thf(37,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | ~ (($true)) | (A @ D) | ((rel @ sk2 @ sk3) != (rel @ C @ D)))),inference(paramod_ordered,[status(thm)],[7,21])).
% 80.90/17.03 thf(38,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (A @ D) | ((rel @ sk2 @ sk3) != (rel @ C @ D)))),inference(simp,[status(thm)],[37])).
% 80.90/17.03 thf(39,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ sk2)) | (A @ sk3))),inference(pattern_uni,[status(thm)],[38:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk2)),bind(D, $thf(sk3))]])).
% 80.90/17.03 thf(174,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(prop_c))]])).
% 80.90/17.03 thf(208,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[174])).
% 80.90/17.03 thf(8556,plain,((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (b @ (sk5 @ A @ b))))) | (rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))))),inference(pre_uni,[status(thm)],[8428:[bind(A, $thf(^ [C:$i]: (b @ (sk5 @ C @ b)))),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(10193,plain,(~ (($true)) | ((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk2) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,9016])).
% 80.90/17.03 thf(10194,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk2) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[10193])).
% 80.90/17.03 thf(10219,plain,(((sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) != sk2) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[10194])).
% 80.90/17.03 thf(163,plain,(! [B:($i > $i),A:$i] : ((rel @ A @ (sk4 @ A @ (^ [C:$i]: (prop_c @ (B @ C))))) | (prop_c @ (B @ A)))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(^ [D:$i]: (prop_c @ (C @ D))))]])).
% 80.90/17.03 thf(198,plain,(! [B:($i > $i),A:$i] : ((rel @ A @ (sk4 @ A @ (^ [C:$i]: (prop_c @ (B @ C))))) | (prop_c @ (B @ A)))),inference(simp,[status(thm)],[163])).
% 80.90/17.03 thf(67,plain,(! [E:($i > $i),D:($i > $i),C:$i,B:$i,A:$i] : ((~ (rel @ (D @ (sk5 @ A @ (^ [F:$i]: (rel @ (D @ F) @ (E @ F))))) @ (E @ (sk5 @ A @ (^ [F:$i]: (rel @ (D @ F) @ (E @ F))))))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (rel @ (D @ C) @ (E @ C)))),inference(prim_subst,[status(thm)],[21:[bind(A, $thf(^ [G:$i]: (rel @ (E @ G) @ (F @ G))))]])).
% 80.90/17.03 thf(108,plain,(! [E:($i > $i),D:($i > $i),C:$i,B:$i,A:$i] : ((~ (rel @ (D @ (sk5 @ A @ (^ [F:$i]: (rel @ (D @ F) @ (E @ F))))) @ (E @ (sk5 @ A @ (^ [F:$i]: (rel @ (D @ F) @ (E @ F))))))) | (~ (rel @ A @ B)) | (~ (rel @ B @ C)) | (rel @ (D @ C) @ (E @ C)))),inference(simp,[status(thm)],[67])).
% 80.90/17.03 thf(8883,plain,(~ (($true)) | (~ (rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,8577])).
% 80.90/17.03 thf(8884,plain,((~ (rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[8883])).
% 80.90/17.03 thf(8990,plain,((~ (rel @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A))) @ sk3)) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[8884])).
% 80.90/17.03 thf(169,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_b))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(prop_b))]])).
% 80.90/17.03 thf(203,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[169])).
% 80.90/17.03 thf(4904,plain,(~ (($true)) | (~ (rel @ sk3 @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(paramod_ordered,[status(thm)],[4638,482])).
% 80.90/17.03 thf(4905,plain,((~ (rel @ sk3 @ sk3)) | ((b @ (sk5 @ sk3 @ (b))) != (b @ sk2))),inference(simp,[status(thm)],[4904])).
% 80.90/17.03 thf(4923,plain,((~ (rel @ sk3 @ sk3)) | ((sk5 @ sk3 @ (b)) != sk2)),inference(simp,[status(thm)],[4905])).
% 80.90/17.03 thf(5178,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ~ (($true)) | ((sk5 @ sk3 @ (b)) != sk2) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(paramod_ordered,[status(thm)],[14,4923])).
% 80.90/17.03 thf(5179,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk4 @ B @ (A))) | ((sk5 @ sk3 @ (b)) != sk2) | ((A @ B) != (rel @ sk3 @ sk3)))),inference(simp,[status(thm)],[5178])).
% 80.90/17.03 thf(5228,plain,((rel @ sk3 @ (sk4 @ sk3 @ (^ [A:$i]: (rel @ A @ A)))) | ((sk5 @ sk3 @ (b)) != sk2)),inference(pre_uni,[status(thm)],[5179:[bind(A, $thf(^ [C:$i]: (rel @ C @ C))),bind(B, $thf(sk3))]])).
% 80.90/17.03 thf(22,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk5 @ B @ (A)) = (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A))))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((sk5 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[21:[bind(A, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 80.90/17.03 thf(23,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk5 @ B @ (A)) != (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A)))) | ((sk5 @ B @ (A)) = D) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)))),inference(lifteq,[status(thm)],[22])).
% 80.90/17.03 thf(173,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (a))) | (a @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(a))]])).
% 80.90/17.03 thf(207,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (a))) | (a @ A))),inference(simp,[status(thm)],[173])).
% 80.90/17.03 thf(2014,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | ~ (($true)) | ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (($false))))) != (rel @ (sk4 @ sk3 @ (b)) @ sk3)))),inference(paramod_ordered,[status(thm)],[235,429])).
% 80.90/17.03 thf(2015,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | ((rel @ A @ (sk4 @ A @ (^ [B:$i]: (($false))))) != (rel @ (sk4 @ sk3 @ (b)) @ sk3)))),inference(simp,[status(thm)],[2014])).
% 80.90/17.03 thf(2027,plain,(! [A:$i] : ((~ (b @ (sk5 @ sk3 @ (b)))) | (A != (sk4 @ sk3 @ (b))) | ((sk4 @ A @ (^ [B:$i]: (($false)))) != sk3))),inference(simp,[status(thm)],[2015])).
% 80.90/17.03 thf(2066,plain,((~ (b @ (sk5 @ sk3 @ (b)))) | ((sk4 @ (sk4 @ sk3 @ (b)) @ (^ [A:$i]: (($false)))) != sk3)),inference(simp,[status(thm)],[2027])).
% 80.90/17.03 thf(72,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk5 @ B @ (A)) = (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A))))) | (~ (rel @ B @ sk2)) | ((sk5 @ B @ (A)) = sk3))),inference(replace_leibeq,[status(thm)],[39:[bind(A, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 80.90/17.03 thf(82,plain,(! [B:$i,A:($i > $o)] : (((sk5 @ B @ (A)) != (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A)))) | ((sk5 @ B @ (A)) = sk3) | (~ (rel @ B @ sk2)))),inference(lifteq,[status(thm)],[72])).
% 80.90/17.03 thf(45,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | ~ (($true)) | (A @ D) | ((rel @ sk1 @ sk2) != (rel @ C @ D)))),inference(paramod_ordered,[status(thm)],[11,21])).
% 80.90/17.03 thf(46,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (A @ D) | ((rel @ sk1 @ sk2) != (rel @ C @ D)))),inference(simp,[status(thm)],[45])).
% 80.90/17.03 thf(47,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ sk1)) | (A @ sk2))),inference(pattern_uni,[status(thm)],[46:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk1)),bind(D, $thf(sk2))]])).
% 80.90/17.03 thf(165,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_a))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[14:[bind(A, $thf(prop_a))]])).
% 80.90/17.03 thf(200,plain,(! [A:$i] : ((rel @ A @ (sk4 @ A @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[165])).
% 80.90/17.03 thf(24,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ~ (($true)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk5 @ F @ (E)))))),inference(paramod_ordered,[status(thm)],[21,21])).
% 80.90/17.03 thf(25,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk5 @ F @ (E)))))),inference(simp,[status(thm)],[24])).
% 80.90/17.03 thf(89,plain,(! [H:$i,G:$i,F:$i,E:($i > $o),D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (~ (rel @ F @ G)) | (~ (rel @ G @ H)) | (E @ H) | ((A @ D) != (E @ (sk5 @ F @ (E)))))),inference(pre_uni,[status(thm)],[25:[]])).
% 80.90/17.03 thf(90,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 @ (sk5 @ B @ (A)))) | ((A @ D) != (E @ (sk5 @ F @ (E)))))),inference(pre_uni,[status(thm)],[89:[]])).
% 80.90/17.03 thf(79,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk5 @ B @ (A)) = (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A))))) | (~ (rel @ B @ sk1)) | ((sk5 @ B @ (A)) = sk2))),inference(replace_leibeq,[status(thm)],[47:[bind(A, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 80.90/17.03 thf(83,plain,(! [B:$i,A:($i > $o)] : (((sk5 @ B @ (A)) != (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A)))) | ((sk5 @ B @ (A)) = sk2) | (~ (rel @ B @ sk1)))),inference(lifteq,[status(thm)],[79])).
% 80.90/17.03 thf(19418,plain,(($false)),inference(e,[status(thm)],[5,15776,106,15873,4934,204,18,8612,11,12972,107,8663,88,10,1078,4638,14,785,110,189,12961,20,2058,4935,4924,8554,4920,429,21,92,8577,12959,9016,9,4930,906,17,12,787,81,7,39,208,8556,10219,198,108,912,130,780,8990,12722,482,203,5228,23,8,914,235,207,929,2066,82,4923,47,15,200,90,83,923])).
% 80.90/17.03 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 80.90/17.03 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------